Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Slhv encoding #7

Merged
merged 133 commits into from
Oct 11, 2024
Merged

Slhv encoding #7

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
133 commits
Select commit Hold shift + click to select a range
db24bfa
update slhv encoding and refactor
zhuyutian57 Jul 10, 2024
617aec2
heap update encoding
zhuyutian57 Jul 11, 2024
e4c7df9
finish encoding(pending for locadd)
zhuyutian57 Jul 12, 2024
f4d7d55
encoding and dump smt2
zhuyutian57 Jul 12, 2024
596fde0
add tests
SpencerL-Y Jul 16, 2024
63a952b
Merge branch 'slhv_encoding' of github.com:SpencerL-Y/esbmc into slhv…
SpencerL-Y Jul 16, 2024
5c843a9
add z3-slhv dec_check
zhuyutian57 Jul 19, 2024
adaa3f7
add print smt, using --output
SpencerL-Y Jul 19, 2024
f63115a
update
SpencerL-Y Jul 19, 2024
f004652
update
zhuyutian57 Jul 21, 2024
da171cb
make hvar and lvar via specific api
zhuyutian57 Jul 22, 2024
1c1df80
use z3_conv get_bool
zhuyutian57 Jul 24, 2024
06d8caf
adjust to byte-level points-to
zhuyutian57 Jul 25, 2024
c9ce912
update
SpencerL-Y Jul 25, 2024
ec27cb3
write vccs and its smt formulas in file
zhuyutian57 Jul 25, 2024
6850b76
add symex_assign on heap_load = val
zhuyutian57 Jul 25, 2024
293124d
set default points-to bytes(4)
zhuyutian57 Jul 25, 2024
52cc112
add definition of heap append
SpencerL-Y Jul 26, 2024
734fb5c
add create value for heap append
SpencerL-Y Jul 26, 2024
460c196
add encoding of heap_append and slicing
zhuyutian57 Jul 27, 2024
e754e5e
update for merge
SpencerL-Y Jul 28, 2024
f5b3ed7
Merge branch 'slhv_encoding' of github.com:SpencerL-Y/esbmc into slhv…
SpencerL-Y Jul 28, 2024
e56a982
add heap free
SpencerL-Y Jul 28, 2024
481c3a6
add heap delete
SpencerL-Y Jul 29, 2024
8e148f3
add heap delete, change bug check encoding
SpencerL-Y Jul 29, 2024
581e99e
heap_delete encoding
zhuyutian57 Jul 29, 2024
1e9bbd0
add slicing
zhuyutian57 Jul 29, 2024
1335839
add heap_region and adjust some exprs for SLHV
zhuyutian57 Jul 31, 2024
82e49f7
encoding same_object in SLHV
zhuyutian57 Jul 31, 2024
739a605
update
zhuyutian57 Jul 31, 2024
708a6a0
update slicing and fix build_goto_trace in --multi-property
zhuyutian57 Aug 1, 2024
4a3c86a
update slicing(fix)
zhuyutian57 Aug 1, 2024
2100b7f
commit for merge
SpencerL-Y Aug 1, 2024
cc00c86
add
SpencerL-Y Aug 1, 2024
3a7e949
fix typo
zhuyutian57 Aug 1, 2024
7d4bd22
update heap_region
zhuyutian57 Aug 2, 2024
b83e430
update regions(at most one time) when dereferencing
zhuyutian57 Aug 6, 2024
51f83b7
fix: do not adjust emp
zhuyutian57 Aug 6, 2024
98667aa
fix update regions
zhuyutian57 Aug 7, 2024
1b2fe4d
replace heap load with its flag
zhuyutian57 Aug 8, 2024
20b5a70
fix: flag of heap_load should be connected
zhuyutian57 Aug 8, 2024
521021d
update encoding of valid_check
zhuyutian57 Aug 12, 2024
5652b2a
invalid pointer encoding
zhuyutian57 Aug 12, 2024
bb3b67d
fix: check heap region access, constant propagation and encoding of s…
zhuyutian57 Aug 14, 2024
48ca98e
fix: dereferencing emp
zhuyutian57 Aug 14, 2024
e6c25f3
deref nil pointer
zhuyutian57 Aug 14, 2024
d896720
fix: merge goto
zhuyutian57 Aug 15, 2024
d7ae1d6
for merge
SpencerL-Y Aug 15, 2024
538584c
Merge branch 'slhv_encoding' of github.com:SpencerL-Y/esbmc into slhv…
SpencerL-Y Aug 15, 2024
cc48b7e
fix: splitting region
zhuyutian57 Aug 15, 2024
b35cc69
fix rename
zhuyutian57 Aug 16, 2024
0d7f635
change output stdout
SpencerL-Y Aug 16, 2024
a02f264
Merge branch 'slhv_encoding' of github.com:SpencerL-Y/esbmc into slhv…
SpencerL-Y Aug 16, 2024
fbd6603
turn all form of pointer arithmetic to locadd
zhuyutian57 Aug 19, 2024
1a199d2
fix encoding of heap_load
zhuyutian57 Aug 20, 2024
15e9725
add locationof and fieldof, replacing pwr and heap_load
zhuyutian57 Aug 22, 2024
f68e3f3
update encoding of same-object
zhuyutian57 Aug 23, 2024
4fab9da
turn pointer arithmetic to locadd
zhuyutian57 Aug 23, 2024
072fea2
trunc output file before show vcc
zhuyutian57 Aug 24, 2024
19e4eb8
correct dereferencing a pointer
zhuyutian57 Aug 24, 2024
cc24ac3
fix heap region size, propagating and renaming heap region's flag
zhuyutian57 Aug 24, 2024
5ce5584
fix encoding of check heap region size
zhuyutian57 Aug 25, 2024
2bc8a45
make points-to for heap_contain
zhuyutian57 Aug 27, 2024
c98663e
add flagof
zhuyutian57 Aug 29, 2024
d182cd3
adjust condition for symex_free
zhuyutian57 Aug 30, 2024
99541ca
move region info to intheap type
zhuyutian57 Aug 30, 2024
890837e
fix heap_update assignment and encoding
zhuyutian57 Aug 31, 2024
9433615
convert struct type to heap region type
zhuyutian57 Sep 1, 2024
62bcea3
set base loc for each heap variable
zhuyutian57 Sep 2, 2024
77631e5
fix symex nondet
zhuyutian57 Sep 4, 2024
759023b
fix object offset when dereferencing and project
zhuyutian57 Sep 4, 2024
f1d0b45
add script
zhuyutian57 Sep 4, 2024
5a12ee7
fix compute offset by from locadd
zhuyutian57 Sep 4, 2024
cc9210b
fix build deref for a whole region and fix project for field_of
zhuyutian57 Sep 5, 2024
cc18ad8
fix pointer analysis
zhuyutian57 Sep 6, 2024
ec34794
fix offset for object field_of
zhuyutian57 Sep 7, 2024
eeb61f1
fix symex free ptr(not finish)
zhuyutian57 Sep 7, 2024
f152f9b
use heapvar = emp to encode valid object
zhuyutian57 Sep 9, 2024
caeeb89
turn assign with subh to disj
zhuyutian57 Sep 10, 2024
58bc157
output truncate
SpencerL-Y Sep 10, 2024
b110e85
delete some debug info
zhuyutian57 Sep 10, 2024
28ff082
encode disjointness
zhuyutian57 Sep 10, 2024
303c6e7
fix slice for disjh
zhuyutian57 Sep 10, 2024
966c861
add property info
zhuyutian57 Sep 11, 2024
d6abd68
slice for disjointness
zhuyutian57 Sep 12, 2024
7b46dc9
fix heap state encoding
zhuyutian57 Sep 12, 2024
cd1c220
fix bound check
zhuyutian57 Sep 12, 2024
6d71238
fix l2 name of location_of
zhuyutian57 Sep 12, 2024
d0cc437
fit slhv load operation
zhuyutian57 Sep 13, 2024
2258cf9
fix encoding of load operation
zhuyutian57 Sep 18, 2024
265dafb
use heap read/write to encoding field_of and heap_update
zhuyutian57 Sep 20, 2024
974d6a5
remove redundant functions
zhuyutian57 Sep 20, 2024
6314fcf
pretty result for multi-property-check
zhuyutian57 Sep 20, 2024
69eef54
fix encoding load
zhuyutian57 Sep 20, 2024
27c799a
fix property info
zhuyutian57 Sep 20, 2024
ee50919
update expriment script
zhuyutian57 Sep 22, 2024
efdcf36
fix encoding
zhuyutian57 Sep 24, 2024
2441e08
fix: assign locaiton when assigning heap variable
zhuyutian57 Sep 25, 2024
04c11b7
do some optimization
zhuyutian57 Sep 25, 2024
c3307a2
fix: dot not assign loc
zhuyutian57 Sep 26, 2024
58f0f67
handle alloc struct, automatically free
zhuyutian57 Sep 26, 2024
16707ce
esbmc-slhv svcomp scripts
zhuyutian57 Sep 26, 2024
20dfa4c
update script
zhuyutian57 Sep 26, 2024
24644f1
use verbosity to turn on(off) debug info
zhuyutian57 Sep 28, 2024
373c014
support alloca
zhuyutian57 Sep 28, 2024
e71d340
update svcomp script
zhuyutian57 Sep 28, 2024
00d1d4a
remove pthread program
zhuyutian57 Sep 29, 2024
8c21b86
fix: removing pthread
zhuyutian57 Sep 29, 2024
d777778
encoding dead semantic in SLHV
zhuyutian57 Sep 29, 2024
d0ed292
fix alignment
zhuyutian57 Sep 29, 2024
4bd4267
remove padded field and record its width
zhuyutian57 Sep 30, 2024
8667aac
fix if expr in pt
zhuyutian57 Sep 30, 2024
e71c108
fix ite in pt
zhuyutian57 Sep 30, 2024
0414e1d
fix script typo
zhuyutian57 Sep 30, 2024
98196d7
update script
zhuyutian57 Sep 30, 2024
db41e67
calculate totaltime for each case
zhuyutian57 Sep 30, 2024
4caf359
support loc2int
zhuyutian57 Sep 30, 2024
1ae4e49
update script
zhuyutian57 Sep 30, 2024
cbb29bb
disable building error trace
zhuyutian57 Oct 1, 2024
d8a8635
update x.py for running esbmc
zhuyutian57 Oct 1, 2024
7d48529
support constant struct
zhuyutian57 Oct 1, 2024
65bb089
support location_of a stack variable
zhuyutian57 Oct 1, 2024
8af081d
fix renaming location_of
zhuyutian57 Oct 1, 2024
9c3a044
fix disjointness
zhuyutian57 Oct 3, 2024
cc7efe6
support struct assignment
zhuyutian57 Oct 3, 2024
62a03d1
update x.py
zhuyutian57 Oct 4, 2024
347852a
add statistic of atomic heap terms
zhuyutian57 Oct 4, 2024
a4a2533
save aht svg correctly
zhuyutian57 Oct 6, 2024
025a44d
add theory solving statistics
zhuyutian57 Oct 8, 2024
f121f00
add bench-0125
zhuyutian57 Oct 11, 2024
9424186
stage for merge
SpencerL-Y Oct 11, 2024
e5bcfc3
Merge branch 'slhv_encoding' of github.com:SpencerL-Y/esbmc into slhv…
SpencerL-Y Oct 11, 2024
4936e4c
merge with main
SpencerL-Y Oct 11, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,4 +14,5 @@ __pycache__
.DS_Store
tags
.cache
release
release
*.zip
Loading
Loading