Code Monkey home page Code Monkey logo

avr's Issues

Add Dockerfile/Docker compose

Hi,

It was not clear from the readme, what distributions avr works on, but I saw dependencies are installed with apt.

I am not sure how active this tool/repository is, but I propose the addition of a really simple dockerfile to make the tool easier to try locally. I attached the dockerfile and docker-compose I used, usage is the following:

  1. (have docker and docker-compose set up on your machine)
  2. docker-compose up -d
  3. docker exec -it avr-docker-avr-1 bash
  4. run ./build.sh manually, as it is interactive
  5. use the examples in this repository or put any input files into the input_files directory besides the docker files, it will be available under /app/input_files
  6. use avr

It is a simple container that could be improved in many ways, but it works. Maybe it will be useful for somebody else as well.

docker-compose.yml.txt
Dockerfile.txt
(remove .txt extension from both files)

Assertion failed when using MathSAT as backend solver

  • Version: dbc3371
  • Environment: Ubuntu 22.04 (Linux kernel 6.5.0-17-generic)
  • Command line: ./avr.py --bmc --bin ./build/bin-mathsat5 --timeout 900 --memout 15000 counter_v.btor2.txt
    • AVR was compiled with MathSAT, and binaries are put under ./build/bin-mathsat5/
    • Input file counter_v.btor2.txt attached
  • Result
Copyright (c) 2016 - Present  Aman Goel and Karem Sakallah, University of Michigan
	(output dir: output/work_test)
	(frontend: btor2)
	(property: all (1 assertions))
	(problem size: 4 bits)
	(abstraction: sa+uf)
  0s	(bmc: safe till step 0)
	(bmc: abstract mode disabled at step 1)
  0s	(bmc: safe till step 5)
  0s	(bmc: safe till step 10)
reach: reach_m5.cpp:1315: virtual int _m5::m5_API::s_check(long int, bool): Assertion `!MSAT_ERROR_MODEL(*m_model)' failed.

Error in Python3.12 

Traceback (most recent call last):
  File "/root/avr/./avr.py", line 18, in <module>
    from distutils import spawn
ModuleNotFoundError: No module named 'distutils'

Assertion failure for some btor models

for example for

https://github.com/makaimann/btor-benchmarks/blob/master/data-integrity/unsafe/btor2/arbitrated_top_n2_w16_d64_e0.btor2

I get

Copyright (c) 2016 - Present  Aman Goel and Karem Sakallah, University of Michigan            
        (output dir: output/work_test)                                                        
        (frontend: btor2)                                                                     
        (property: all (1 assertions))                                                        
        (problem size: 2131 bits)                                                             
        (abstraction: sa+uf)                                                                  
   0    : 0     : 0 s: 0    0s                                                                
   11   : 1     : 0 7 s: 7    0s                                                                                                                                                            
   2254 : 2     : 0 12 276 s: 288    102s                                                     
   2263 : 3     : 0 13 158 128 s: 299    103s                  reach: reach_coi.cpp:1163: bool reach::Reach::allowed_relation(Inst*, Inst*, OpInst::OpType): Assertion `opt != OpInst::Eq' f
ailed.                                         
   2263 : 3     : 0 13 159 128 s: 300    103s                                                 
      Result        Time        Mem.       #Refs                                              
                     sec          MB                                                          
       f_err      103.24         534        2263

The same error appears for other models from this benchmark, too.

Compile Error

passes/sat/freduce.cc:457:55: error: ‘numeric_limits’ is not a member of ‘std’

g++ (Ubuntu 13.2.0-4ubuntu3) 13.2.0

Assertion failed when using Boolector as backend solver

  • Version: dbc3371
  • Environment: Ubuntu 22.04 (Linux kernel 6.5.0-17-generic)
  • Command line: /avr.py --bmc --bin ./build/bin-boolector --timeout 900 --memout 15000 counter_v.btor2.txt
    • AVR was compiled with Boolector, and binaries are put under ./build/bin-boolector/
    • Input file counter_v.btor2.txt attached
  • Result
Copyright (c) 2016 - Present  Aman Goel and Karem Sakallah, University of Michigan
	(output dir: output/work_test)
	(frontend: btor2)
	(property: all (1 assertions))
	(problem size: 4 bits)
	(abstraction: sa+uf)
reach: reach_bt.cpp:1178: virtual void _bt::bt_API::assert_distinct_constants(): Assertion `0' failed.

Two small btor2 files that seem trigger bugs

We have verified the syntactic correctness of these cases with btro2tools/catbtor.
We use the following command to run AVR:

python3 avr.py -n tmp -o tmp ${BTOR2_FILE}

Case 1

1 sort bitvec 4
2 constd 1 -7
3 const 1 0110
4 state 1 bv2_4
5 sub 1 3 4
6 sort bitvec 5
7 constd 6 -11
8 slice 1 7 4 1
9 rol 1 5 8
10 const 1 0000
11 consth 1 0
12 ror 1 10 11
13 state 1 bv0_4
14 init 1 13 12
15 sort bitvec 1
16 const 15 0
17 rol 1 4 11
18 ite 1 16 4 17
19 nor 1 18 4
20 next 1 13 19
21 state 1 bv1_4
22 init 1 21 9
23 input 1 input1_4
24 neg 1 23
25 sort bitvec 3
26 input 25
27 sext 1 26 1
28 srem 1 24 27
29 next 1 21 28
30 init 1 4 2
31 input 1 input0_4
32 next 1 4 31
33 ror 1 13 21
34 and 1 33 33
35 and 1 13 21
36 sdiv 1 35 31
37 slte 15 34 36
38 bad 37

corresponding error message:

avr_word_netlist.cpp:912: static Inst* OpInst::create(OpInst::OpType, InstL, int, bool, Inst*, SORT): Assertion ‘0’ failed.

Case 2

1 sort bitvec 7
2 sort bitvec 4
3 const 2 1010
4 constd 2 -8
5 inc 2 4
6 ror 2 3 5
7 uext 1 6 3
8 state 1 bv2_7
9 neg 1 8
10 sort bitvec 6
11 zero 10
12 sext 1 11 1
13 state 1 bv0_7
14 sll 1 12 13
15 init 1 13 9
16 state 1 bv1_7
17 dec 1 16
18 consth 1 01
19 smod 1 13 18
20 srl 1 17 19
21 neg 1 20
22 next 1 13 21
23 init 1 16 14
24 and 1 8 13
25 next 1 16 24
26 init 1 8 7
27 sort bitvec 8
28 input 2 input1_4
29 sext 27 28 4
30 slice 1 29 6 0
31 next 1 8 30
32 sort bitvec 1
33 const 32 1
34 neg 32 33
35 sra 1 13 13
36 add 1 13 13
37 ult 32 35 36
38 neq 32 34 37
39 bad 38

corresponding error message:

reach: reach_y2.cpp:7367: void _y2::y2_API::inst2yices(Inst*, bool): Assertion ‘0’ failed.

Could you please help to confirm if these are bugs of AVR, or we didn't build AVR properly? (or some reasons else~~

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.