aman-goel / avr Goto Github PK
View Code? Open in Web Editor NEWReads a state transition system and performs property checking
License: GNU General Public License v3.0
Reads a state transition system and performs property checking
License: GNU General Public License v3.0
Traceback (most recent call last):
File "/root/avr/./avr.py", line 18, in <module>
from distutils import spawn
ModuleNotFoundError: No module named 'distutils'
/avr.py --bmc --bin ./build/bin-boolector --timeout 900 --memout 15000 counter_v.btor2.txt
./build/bin-boolector/
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.
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:
docker-compose up -d
docker exec -it avr-docker-avr-1 bash
./build.sh
manually, as it is interactiveinput_files
directory besides the docker files, it will be available under /app/input_files
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)
for example for
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.
passes/sat/freduce.cc:457:55: error: ‘numeric_limits’ is not a member of ‘std’
g++ (Ubuntu 13.2.0-4ubuntu3) 13.2.0
Line 40 of ./src/reach/Makefile should be
BT_LIB += $(BT_DIR)/deps/btor2tools/build/lib/libbtor2parser.a
instead of
BT_LIB += $(BT_DIR)/deps/btor2tools/build/libbtor2parser.a
./avr.py --bmc --bin ./build/bin-mathsat5 --timeout 900 --memout 15000 counter_v.btor2.txt
./build/bin-mathsat5/
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.
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}
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.
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~~
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.