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

Jump to bottom

C-2PO: Thesis About a Weakly-Relational Pointer Analysis #1485

Open
wants to merge 337 commits into
base: master
Choose a base branch
from
Open

C-2PO: Thesis About a Weakly-Relational Pointer Analysis #1485

Show file tree
Hide file tree
Changes from 20 commits
Commits
Show all changes
337 commits
Select commit Hold shift + click to select a range
f22f4f3
modified a comment
reb-ddm Apr 29, 2024
69b0031
minor style choices
reb-ddm Apr 29, 2024
69dc1ff
simplify cil conversion by using to_index
reb-ddm May 1, 2024
72d689e
fix small thing
reb-ddm May 1, 2024
70c273f
removed code for invertible assignments, as it is not necessary
reb-ddm May 1, 2024
31ae30d
add size parameter to may_be_equal for the ize of the lvalue
reb-ddm May 1, 2024
8b427c4
changed Congruence closure to not be generic, but only work for for v…
reb-ddm May 1, 2024
addf77b
added type information to terms
reb-ddm May 1, 2024
d8c484a
added size of variables to the data structure;
reb-ddm May 3, 2024
5889a94
modified some tests
reb-ddm May 3, 2024
6b2cacd
first draft of join, haven't tested it yet
reb-ddm May 3, 2024
615453c
finishe implementing join, calculate offsets correctly in join
reb-ddm May 6, 2024
5a6d177
fix bug in equal
reb-ddm May 6, 2024
4e27d5f
better dereferencing
reb-ddm May 7, 2024
40d0038
added tests for join
reb-ddm May 7, 2024
4216b06
implemented disequalities
reb-ddm May 7, 2024
d34c252
implemented remove with disequalities
reb-ddm May 9, 2024
b5e94a9
only dereference disequalities if they have the same size
reb-ddm May 9, 2024
1fa4e66
add test for disequalities
reb-ddm May 9, 2024
4da20a6
implemented join for disequalities
reb-ddm May 9, 2024
ad80a19
fixed bugs in startState analysis and remembered tainted variables in…
reb-ddm May 13, 2024
0882a0a
remove tainted variables in wrpointer analysis in combine_env
reb-ddm May 13, 2024
4d5a966
add function to remove tainted variables to the wrpointer domain
reb-ddm May 13, 2024
4532e5b
add taintPartialContext analysis to tests
reb-ddm May 13, 2024
c167abe
add test for tainted variables n a function
reb-ddm May 13, 2024
9bd512d
adapted the comments
reb-ddm May 14, 2024
2807b01
fixed bug in join and added corresponding test
reb-ddm May 17, 2024
23213b3
made join more precise and made widen = top
reb-ddm May 20, 2024
61058ea
handle unknown left hand sides of assignments
reb-ddm May 21, 2024
4a253db
better calculation of dereferenced expression. Give up when it is not…
reb-ddm May 21, 2024
69464f7
check validity of dereferenced expressions
reb-ddm May 21, 2024
b60a9a1
adapt enter and combine to follow the goblint assumptions
reb-ddm May 21, 2024
6c4b78e
modify comments
reb-ddm May 21, 2024
9fae17f
keep all global and all reachable variables in enter
reb-ddm May 21, 2024
26a51a8
added tests for structs and recursive functions
reb-ddm May 21, 2024
63216df
remove a raise Failure
reb-ddm May 21, 2024
4cba626
make sure that the min_repr is always defined in any case, even when …
reb-ddm May 21, 2024
2d8cd98
add descriptions
reb-ddm May 24, 2024
a1b8a36
adapted some tests
reb-ddm May 24, 2024
9e4a4f9
fix bug when computing minimal representatives
reb-ddm May 24, 2024
f034b0a
fix linter warnings
reb-ddm May 24, 2024
3d49ddb
Merge branch 'master' into thesis-weakly-relational-pointer
reb-ddm May 24, 2024
975aa46
add startcontext
reb-ddm May 24, 2024
e342e38
rename tests
reb-ddm May 24, 2024
534eb11
added conf file for svcomp and fixed a bug
reb-ddm May 24, 2024
5f0dbe5
fixed invalid widen bug
reb-ddm Jun 10, 2024
d093177
added constant bitsSizeOfPtr
reb-ddm Jun 11, 2024
9d1be23
Merge branch 'temp' into thesis-weakly-relational-pointer
reb-ddm Jun 11, 2024
d5b9b03
check for each term, if it is a valid pointer
reb-ddm Jun 11, 2024
cf1869a
remove types from data structure
reb-ddm Jun 11, 2024
1ef4887
check for propositions *x = *y if the pointers x and y are equal (suc…
reb-ddm Jun 11, 2024
a06c9c9
adapt test case to new type handling
reb-ddm Jun 11, 2024
b49995d
fix error: top of IntDomTuple not supported
reb-ddm Jun 12, 2024
e48d0be
fix error: cil sizeoferror
reb-ddm Jun 12, 2024
966d6b3
better way of fixing the error
reb-ddm Jun 12, 2024
a0d49ec
fix out of memory error. It was because I used < instead of T.compare
reb-ddm Jun 12, 2024
ccf43ba
fix error when there s an array of non-constant length
reb-ddm Jun 13, 2024
76fd7e8
fixed bug with disequations
reb-ddm Jun 13, 2024
d10394b
fix sizeoferror and not_found error
reb-ddm Jun 13, 2024
d46c5b3
fixed bug where the auxiliary variable is not completely removed from…
reb-ddm Jun 13, 2024
e8d9224
fixed division by zero error and some wrong comparisons
reb-ddm Jun 13, 2024
b7d8931
add small test for disequalities
reb-ddm Jun 17, 2024
9dca5e1
properly update the disequalities after a union operation. Use the mi…
reb-ddm Jun 17, 2024
a0fd9a2
solved last remaining SizeOfErrors
reb-ddm Jun 17, 2024
061f2b6
use correct compare function
reb-ddm Jun 17, 2024
fd95f86
add regressio test for the compare function bug
reb-ddm Jun 17, 2024
8fed940
fixed inconsistency in disequalities
reb-ddm Jun 18, 2024
83bb4cf
removed warning for Field on a non-compound
reb-ddm Jun 18, 2024
0c41a16
fix issue where startstate answers queries about variables that were …
reb-ddm Jun 18, 2024
b4b6712
I'm not sure what to write for the thread functions
reb-ddm Jun 18, 2024
101e247
catch sizeOfError
reb-ddm Jun 18, 2024
0182296
made Lookup Map with just one successor, as it was in the beginning
reb-ddm Jun 18, 2024
06f31d8
new method of restricting the automaton
reb-ddm Jun 19, 2024
8dbbe48
ignore floats and catch an exception
reb-ddm Jun 20, 2024
afaf409
fix bugs with offsets
reb-ddm Jun 21, 2024
104360c
add conf file for base analysis with which we can compare wrpointer
reb-ddm Jun 24, 2024
50f9671
add tracing for get_normal_form
reb-ddm Jun 24, 2024
b98d18f
Merge branch 'thesis-weakly-relational-pointer' into thesis-wrpointer…
reb-ddm Jun 24, 2024
e758b5e
made sure to always just add pointers to the data structure
reb-ddm Jun 24, 2024
9e8c10b
fixed bug in find of union-find
reb-ddm Jun 25, 2024
12f64f2
properly update offset of long integers
reb-ddm Jun 25, 2024
d72d622
add regression test for widen
reb-ddm Jun 25, 2024
2b4fdd1
revert wrong fix
reb-ddm Jun 25, 2024
2135fea
adapt test case
reb-ddm Jun 25, 2024
944bc95
replace Z.of_int 1 with Z.one
reb-ddm Jun 25, 2024
e297335
remove var-eq analysis from conf file
reb-ddm Jun 25, 2024
babee14
intersect answers of MayPointTo query for equal pointers
reb-ddm Jun 25, 2024
267294c
implicitly assume that &x != &y
reb-ddm Jun 28, 2024
0e647d2
implicitly assume that &x != &y
reb-ddm Jun 28, 2024
c2f704b
Merge branch 'thesis-weakly-relational-pointer' of github.com:reb-ddm…
reb-ddm Jun 28, 2024
da7cdb4
started implementing auxiliaries, but it doesn't quite work yet
reb-ddm Jun 28, 2024
8d04d60
solved exception, maybe not in the best possible way
reb-ddm Jun 28, 2024
bce1a8c
don't answer maypointto query any more
reb-ddm Jun 30, 2024
f45c6c2
only add valid terms when we add successor terms
reb-ddm Jun 30, 2024
27f11b5
fix regression test
reb-ddm Jul 1, 2024
9152fc0
fix compare function of propositions and is_struct_type function
reb-ddm Jul 2, 2024
99ae3c1
Merge branch 'thesis-weakly-relational-pointer' into thesis-wrpointer…
reb-ddm Jul 2, 2024
2f91d09
add auxiliaries to to_cil
reb-ddm Jul 2, 2024
e5431b2
Shortcut equal
michael-schwarz Jul 3, 2024
049aa07
Shortcut join
michael-schwarz Jul 3, 2024
9b97233
Short circuit meet
michael-schwarz Jul 3, 2024
3397e3b
Reuse var
michael-schwarz Jul 3, 2024
990af99
Optimize some calls
michael-schwarz Jul 3, 2024
31ff5fb
New `find_successor_in_set`
michael-schwarz Jul 3, 2024
55ec005
support an additional type of dereferencing
reb-ddm Jul 4, 2024
35c846c
Merge branch 'thesis-weakly-relational-pointer' of github.com:reb-ddm…
reb-ddm Jul 4, 2024
fd8ae21
fixed indentation
reb-ddm Jul 4, 2024
176dc42
add first code for block disequalities
reb-ddm Jul 4, 2024
acc5060
added block diseq handling for malloc
reb-ddm Jul 4, 2024
57c50d7
add remove for block disequalities
reb-ddm Jul 4, 2024
769df6b
implemented equal for block diseqs
reb-ddm Jul 4, 2024
376fe87
add join for block disequalities
reb-ddm Jul 4, 2024
a01bead
update the representatives of block disequalities
reb-ddm Jul 4, 2024
97584b2
add meet for block disequalities
reb-ddm Jul 5, 2024
c6f0e63
add meet for block disequalities
reb-ddm Jul 5, 2024
31e009b
Merge branch 'thesis-weakly-relational-pointer' into thesis-wrpointer…
reb-ddm Jul 5, 2024
8642eeb
may point to query for all elements in the equivalence class
reb-ddm Jul 5, 2024
354e4a0
fixed bug with Casts and auxiliaries and made join more elegant
reb-ddm Jul 5, 2024
814446f
fixed may_point_to and implemented query for all elements in equivale…
reb-ddm Jul 5, 2024
4d2f750
fix bug that comes from the fact that block disequalities can possibl…
reb-ddm Jul 5, 2024
d8baa37
removed some unused rec flags
reb-ddm Jul 5, 2024
a5ffa24
Merge branch 'master' into thesis-weakly-relational-pointer
reb-ddm Jul 5, 2024
3dd5c5c
moved union find to another file
reb-ddm Jul 5, 2024
1ed0bd5
copy the whole wrpointer analysis and give it another name
reb-ddm Jul 5, 2024
3629d9d
removed everything that has to do woth minimal representatives from c2po
reb-ddm Jul 5, 2024
0eca795
added exactly the same tests as the wrpointer tests also to c2po. The…
reb-ddm Jul 5, 2024
d139d80
simplified the jooin operation
reb-ddm Jul 5, 2024
1c59fc6
I think I implemented the simplified restriction. I'll have to look a…
reb-ddm Jul 5, 2024
e3c71e8
implemented equality for c2po
reb-ddm Jul 6, 2024
e64541b
replaced wrpointer with c2po for the tracing
reb-ddm Jul 6, 2024
9ace51b
updated tests for c2po
reb-ddm Jul 6, 2024
f89d0b2
added conf file for c2po
reb-ddm Jul 6, 2024
9e3ad40
update comments and make some order
reb-ddm Jul 6, 2024
55f7d5f
fixed name of test folder
reb-ddm Jul 6, 2024
e251e19
make it configurable if we want to use maypointto for c2po or not. Up…
reb-ddm Jul 6, 2024
ea433bb
made a single-threaded analysis lifter
reb-ddm Jul 6, 2024
4dbe6c0
fix equality function of c2po
reb-ddm Jul 6, 2024
1d476df
(really) fixed equality
reb-ddm Jul 6, 2024
83bf565
put back old version of restriction, where we add successors, because…
reb-ddm Jul 6, 2024
d2600d7
is_root now works also with elements that are not in the uf
reb-ddm Jul 6, 2024
e64d502
implemented widen and narrow
reb-ddm Jul 7, 2024
530f9ef
some shortcuts, maybe they help
reb-ddm Jul 7, 2024
807eefe
reswitched to the new version of restricting. Because the prof wrote …
reb-ddm Jul 7, 2024
286d1be
removed all code duplication, but I also removed min_repr, so I will …
reb-ddm Jul 7, 2024
f484cd2
use MustBeSingleThreaded instead of IsEverMultithreaded
reb-ddm Jul 7, 2024
0b8305c
move the short-circuit after the match
reb-ddm Jul 7, 2024
2b2e0a2
fix is_top: now it takes into account the disequalities
reb-ddm Jul 7, 2024
79bbc07
fix code
reb-ddm Jul 7, 2024
965be40
moved MayBeEqual to CongruenceClosure.ml
reb-ddm Jul 8, 2024
cbd7bf6
merged wrpointerDomain with c2poDomain
reb-ddm Jul 8, 2024
abeb2a2
merge wrpointerAnalysis and c2poAnalysis
reb-ddm Jul 8, 2024
2b4fc1f
rename everything to c2po
reb-ddm Jul 8, 2024
eb09f11
add configurations for choosing which join and which equal algorithm …
reb-ddm Jul 8, 2024
da0ea4a
update tracing
reb-ddm Jul 8, 2024
dc2a4be
fix the join and widen etc. It was because I didn't explicitly write …
reb-ddm Jul 8, 2024
40678f6
use --enable instead of --set
reb-ddm Jul 8, 2024
c665548
fix unsound behaviour
reb-ddm Jul 9, 2024
2840b4c
fix arithmeticonintegerbot and invalid_widen
reb-ddm Jul 9, 2024
ba0c28e
change tracing a bit
reb-ddm Jul 9, 2024
cb6bc2a
fix block disequality query
reb-ddm Jul 9, 2024
0df379e
implemented Invariant
reb-ddm Jul 9, 2024
ada5779
implemented Invariant
reb-ddm Jul 9, 2024
700017f
remove unused rec flag
reb-ddm Jul 9, 2024
8173b99
Horrible, horrible fix. May the gods forgive us!
michael-schwarz Jul 9, 2024
af4e693
add conf file for the tests with witnesses
reb-ddm Jul 10, 2024
5169a97
changed my mind
reb-ddm Jul 10, 2024
887ab98
now I'm the only one that answers the invariant query
reb-ddm Jul 10, 2024
6f64f8f
fix invariant
reb-ddm Jul 14, 2024
0568de8
Revert "now I'm the only one that answers the invariant query"
reb-ddm Jul 15, 2024
be00c1d
removed unused function and added tracing
reb-ddm Jul 15, 2024
dbf30c9
merge changes
reb-ddm Jul 15, 2024
249e595
fix name of function
reb-ddm Jul 15, 2024
18b3c10
use get_conjunction instead of get_noemal_form for meet
reb-ddm Jul 15, 2024
b08fa56
fix indentation
reb-ddm Jul 15, 2024
82a5cca
re-add min_repr, but it doesn't quite work yet
reb-ddm Jul 16, 2024
690eb44
remove init_congruence
reb-ddm Jul 16, 2024
d1f4f89
add some tracing
reb-ddm Jul 17, 2024
17f0954
fix bug when adding disequalities
reb-ddm Jul 17, 2024
35f4b05
fix join; less code duplication
reb-ddm Jul 17, 2024
d10a49f
always first update block disequalities and then normal disequalities
reb-ddm Jul 17, 2024
c3479f4
remove some TODOs
reb-ddm Jul 17, 2024
28ba650
make code for element_closure a bit better
reb-ddm Jul 17, 2024
79dacf2
simplify removal of block disequalities
reb-ddm Jul 17, 2024
b2b75a2
maybe fixed combine_env?
reb-ddm Jul 17, 2024
b95e2c6
optimize minimal representatives
reb-ddm Jul 17, 2024
44668a4
less code duplication for get_normal_form
reb-ddm Jul 18, 2024
5f2b938
simplify insertion a bit
reb-ddm Jul 18, 2024
2af0179
add calloc and alloca and realloc to special
reb-ddm Jul 18, 2024
fbe1310
removed unused things
reb-ddm Jul 18, 2024
6a35b05
forget var information in special
reb-ddm Jul 18, 2024
96916bb
no need to calculate the closure of disequalities after an insertion …
reb-ddm Jul 25, 2024
94d2896
fixed enter/combine
reb-ddm Jul 29, 2024
9f6cd4b
fixed realloc
reb-ddm Jul 29, 2024
c1f8942
Merge with the other branch where I have been coding
reb-ddm Jul 29, 2024
b4028a1
rename module to c2po
reb-ddm Jul 29, 2024
b77fec3
made normal form a lazy record field
reb-ddm Jul 29, 2024
407d8cf
fixed warning
reb-ddm Jul 29, 2024
2255dc0
recompute min_repr in the appropriate places
reb-ddm Jul 29, 2024
d155b89
indentation
reb-ddm Jul 29, 2024
fe6e9d0
add tracing
reb-ddm Jul 29, 2024
cd48307
a bit more path compression
reb-ddm Jul 29, 2024
0576b89
restore find_no_pc
reb-ddm Jul 29, 2024
13c4de6
Timing.wrap
reb-ddm Jul 29, 2024
4527ece
solved invariant bug in a better way
reb-ddm Jul 30, 2024
a25ef22
ask MayBeTainted in combine_env instead of start State
reb-ddm Jul 30, 2024
1ea9488
remove the weird hack I put in startState
reb-ddm Jul 30, 2024
cc148ef
simplify redundant definitions in startState
reb-ddm Jul 30, 2024
6de5039
Merge branch 'master' into thesis-weakly-relational-pointer
reb-ddm Jul 30, 2024
82d3802
disable unknown_function.call for c2po conf
reb-ddm Jul 31, 2024
b55075f
added different conf files for the 4 possibilities of c2po
reb-ddm Jul 31, 2024
1dc5301
fixed lazy computation and added timings.wrap
reb-ddm Jul 31, 2024
d46b4b7
added a widen operator for the join with automaton as described in my…
reb-ddm Aug 1, 2024
f58d2bd
fixed bug in normal form
reb-ddm Aug 2, 2024
1653e28
fix invalid_widen bug
reb-ddm Aug 5, 2024
6ba1cc7
outsource variable handling
reb-ddm Aug 7, 2024
d963273
make everything compatible with the new duplicated vars
reb-ddm Aug 7, 2024
ecb67da
replace wrpointer with c2po
reb-ddm Aug 7, 2024
6edd0ac
fixed bugs. Needs to be tested
reb-ddm Aug 7, 2024
8efe09c
fix some things
reb-ddm Aug 7, 2024
e561383
add Var.
reb-ddm Aug 7, 2024
b0ce431
I think this is not necessary
reb-ddm Aug 7, 2024
cfd155e
use the other method for variable duplication
reb-ddm Aug 7, 2024
c28f503
rename shadow to duplicated
reb-ddm Aug 7, 2024
d9de485
fix indentation
reb-ddm Aug 7, 2024
85ad21d
remove some unused functions and add some comments
reb-ddm Aug 7, 2024
498cd40
remove useless module
reb-ddm Aug 7, 2024
c16366c
add some comments and adapt the structure of the code
reb-ddm Aug 7, 2024
89ec5e2
update comments
reb-ddm Aug 8, 2024
5d940cd
adress -> address
reb-ddm Aug 8, 2024
924ccc2
Merge branch 'master' into thesis-weakly-relational-pointer
reb-ddm Aug 8, 2024
30949fd
remove unused polymorphism
reb-ddm Aug 13, 2024
b3ea845
remove redundant compare
reb-ddm Aug 13, 2024
da75386
use Cilfacade.isFloatType snf Cil.unrollType
reb-ddm Aug 13, 2024
448768e
change error to TypoOfError
reb-ddm Aug 13, 2024
eabeec9
explain better what singleThreadedLifter is for
reb-ddm Aug 13, 2024
1e5e645
do not recompute compare
reb-ddm Aug 13, 2024
f6133c9
fix invariant generation bug
reb-ddm Sep 9, 2024
599dfd4
remove confs
reb-ddm Sep 9, 2024
0d1470a
Revert "Horrible, horrible fix. May the gods forgive us!"
reb-ddm Sep 9, 2024
85c08ec
derive equality of propositions
reb-ddm Sep 9, 2024
6b269fd
use Lattice.LiftBot
reb-ddm Sep 10, 2024
03fca72
catch exception
reb-ddm Sep 10, 2024
07ab99a
implemented pretty_diff
reb-ddm Sep 10, 2024
e22a989
remove debug print
reb-ddm Sep 10, 2024
addbbd4
make precise_join an enum
reb-ddm Sep 10, 2024
80f68fc
make normal_form an enum
reb-ddm Sep 10, 2024
39b2261
fix bug
reb-ddm Sep 10, 2024
c9a7e04
change the location od c2poAnalysis in Goblint_lib
reb-ddm Sep 10, 2024
cb9dc2f
modify richvarinfo to make it possible to change all the other fields…
reb-ddm Sep 11, 2024
f787e67
Merge branch 'master' into thesis-weakly-relational-pointer
michael-schwarz Sep 22, 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
152 changes: 0 additions & 152 deletions conf/svcomp-c2po-no-maypointto.json
View file
Open in desktop
reb-ddm marked this conversation as resolved.
Outdated Show resolved Hide resolved

This file was deleted.

154 changes: 0 additions & 154 deletions conf/svcomp-c2po1_join_nform.json
View file
Open in desktop

This file was deleted.

Loading
Loading