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.

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

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
Show file tree
Hide file tree
Changes from 250 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
240 changes: 240 additions & 0 deletions src/analyses/c2poAnalysis.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,240 @@
(** C-2PO: A Weakly-Relational Pointer Analysis for C based on 2 Pointer Logic. The analysis can infer equalities and disequalities between terms which are built from pointer variables, with the addition of constants and dereferencing. ([c2po])*)

open Analyses
open GoblintCil
open C2poDomain
open CongruenceClosure
open Batteries
open SingleThreadedLifter
open DuplicateVars

module Spec =
struct
include DefaultSpec
include Analyses.IdentitySpec
module D = D
module C = D

let name () = "c2po"
let startcontext () = D.top ()

(** Find reachable variables in a function *)
let reachable_from_args ctx args =
let res =
List.fold (fun vs e -> vs @ (ctx.ask (ReachableFrom e) |> Queries.AD.to_var_may)) [] args in
if M.tracing then M.tracel "c2po-reachable" "reachable vars: %s\n" (List.fold_left (fun s v -> s ^v.vname ^"; ") "" res); res

(* Returns Some true if we know for sure that it is true,
and Some false if we know for sure that it is false,
and None if we don't know anyhing. *)
let eval_guard ask t e ik =
let open Queries in
let prop_list = T.prop_of_cil ask e true in
match split prop_list with
| [], [], [] -> ID.top()
| x::xs, _, [] -> if fst (eq_query t x) then ID.of_bool ik true else if neq_query t x then ID.of_bool ik false else ID.top()
| _, y::ys, [] -> if neq_query t y then ID.of_bool ik true else if fst (eq_query t y) then ID.of_bool ik false else ID.top()
| _ -> ID.top() (*there should never be block disequalities here...*)

(**Convert a conjunction to an invariant.*)
let conj_to_invariant ask conjs t =
List.fold (fun a prop -> match T.prop_to_cil prop with
| exception (T.UnsupportedCilExpression _) -> a
| exp ->
if M.tracing then M.trace "c2po-invariant" "Adding invariant: %a" d_exp exp;
Invariant.(a && of_exp exp))
(Invariant.top()) conjs

let query ctx (type a) (q: a Queries.t): a Queries.result =
let open Queries in
match ctx.local with
| `Bot -> Result.top q
| `Lifted cc ->
match q with
| EvalInt e -> let ik = Cilfacade.get_ikind_exp e in
eval_guard (ask_of_ctx ctx) cc e ik
| Queries.Invariant context ->
let scope = Node.find_fundec ctx.node in
let t = D.remove_vars_not_in_scope scope cc in
(conj_to_invariant (ask_of_ctx ctx) (get_conjunction t) t)
| _ -> Result.top q

(** Assign the term `lterm` to the right hand side rhs, that is already
converted to a C-2PO term. *)
let assign_term t ask lterm rhs lval_t =
(* ignore assignments to values that are not 64 bits *)
match T.get_element_size_in_bits lval_t, rhs with
(* Indefinite assignment *)
| s, (None, _) -> (D.remove_may_equal_terms ask s lterm t)
(* Definite assignment *)
| s, (Some term, Some offset) ->
let dummy_var = MayBeEqual.dummy_var lval_t in
if M.tracing then M.trace "c2po-assign" "assigning: var: %s; expr: %s + %s. \nTo_cil: lval: %a; expr: %a\n" (T.show lterm) (T.show term) (Z.to_string offset) d_exp (T.to_cil lterm) d_exp (T.to_cil term);
t |> meet_conjs_opt [Equal (dummy_var, term, offset)] |>
D.remove_may_equal_terms ask s lterm |>
meet_conjs_opt [Equal (lterm, dummy_var, Z.zero)] |>
D.remove_terms_containing_variable @@ AssignAux lval_t
| _ -> (* this is impossible *) C2PODomain.top ()

(** Assign Cil Lval to a right hand side that is already converted to
C-2PO terms.*)
let assign_lval t ask lval expr =
let lval_t = typeOfLval lval in
match T.of_lval ask lval with
| lterm -> assign_term t ask lterm expr lval_t
| exception (T.UnsupportedCilExpression _) ->
(* the assigned variables couldn't be parsed, so we don't know which addresses were written to.
We have to forget all the information we had.
This should almost never happen.
Except if the left hand side is a complicated expression like myStruct.field1[i]->field2[z+k], and Goblint can't infer the offset.*)
if M.tracing then M.trace
"c2po-invalidate" "INVALIDATE lval: %a" d_lval lval;
C2PODomain.top ()

let assign ctx lval expr =
let ask = (ask_of_ctx ctx) in
match ctx.local with
| `Bot -> `Bot
| `Lifted cc ->
let res = `Lifted (reset_normal_form @@ assign_lval cc ask lval (T.of_cil ask expr)) in
if M.tracing then M.trace "c2po-assign" "ASSIGN: var: %a; expr: %a; result: %s.\n" d_lval lval d_plainexp expr (D.show res); res

let branch ctx e pos =
let props = T.prop_of_cil (ask_of_ctx ctx) e pos in
let valid_props = T.filter_valid_pointers props in
let res =
match ctx.local with
| `Bot -> `Bot
| `Lifted t ->
if List.is_empty valid_props then `Lifted t else
match (reset_normal_form (meet_conjs_opt valid_props t)) with
| exception Unsat -> `Bot
| t -> `Lifted t
in
if M.tracing then M.trace "c2po" "BRANCH:\n Actual equality: %a; pos: %b; valid_prop_list: %s; is_bot: %b\n"
d_exp e pos (show_conj valid_props) (D.is_bot res);
if D.is_bot res then raise Deadcode;
res

let body ctx f = ctx.local

let assign_return ask t return_var expr =
(* the return value is not stored on the heap, therefore we don't need to remove any terms *)
match T.of_cil ask expr with
| (Some term, Some offset) -> reset_normal_form (meet_conjs_opt [Equal (return_var, term, offset)] t)
| _ -> t

let return ctx exp_opt f =
let res = match exp_opt with
| Some e -> begin match ctx.local with
| `Bot -> `Bot
| `Lifted t ->
`Lifted (assign_return (ask_of_ctx ctx) t (MayBeEqual.return_var (typeOf e)) e)
end
| None -> ctx.local
in if M.tracing then M.trace "c2po-function" "RETURN: exp_opt: %a; state: %s; result: %s\n" d_exp (BatOption.default (MayBeEqual.dummy_lval_print (TVoid [])) exp_opt) (D.show ctx.local) (D.show res);res

(** var_opt is the variable we assign to. It has type lval. v=malloc.*)
let special ctx var_opt v exprs =
let desc = LibraryFunctions.find v in
let ask = ask_of_ctx ctx in
match ctx.local with
| `Bot -> `Bot
| `Lifted cc ->
let t = begin match var_opt with
| None ->
cc
| Some varin ->
(* forget information about var,
but ignore assignments to values that are not 64 bits *)
try
(let s, lterm = T.get_element_size_in_bits (typeOfLval varin), T.of_lval ask varin in
let t = D.remove_may_equal_terms ask s lterm cc in
begin match desc.special exprs with
| Malloc _ | Calloc _ | Alloca _ ->
add_block_diseqs t lterm
| _ -> t
end)
with (T.UnsupportedCilExpression _) -> C2PODomain.top ()
end
in
match desc.special exprs with
| Assert { exp; refine; _ } -> if not refine then
ctx.local
else
branch ctx exp true
| _ -> `Lifted (reset_normal_form t)

(**First all local variables of the function are duplicated (by negating their ID),
then we remember the value of each local variable at the beginning of the function
by using the analysis startState. This way we can infer the relations between the
local variables of the caller and the pointers that were modified by the function. *)
let enter ctx var_opt f args =
(* add duplicated variables, and set them equal to the original variables *)
match ctx.local with
| `Bot -> [`Bot, `Bot]
| `Lifted cc ->
let added_equalities = T.filter_valid_pointers (List.map (fun v -> Equal (T.term_of_varinfo (DuplicVar v), T.term_of_varinfo (NormalVar v), Z.zero)) f.sformals) in
let state_with_duplicated_vars = meet_conjs_opt added_equalities cc in
if M.tracing then M.trace "c2po-function" "ENTER1: var_opt: %a; state: %s; state_with_duplicated_vars: %s\n" d_lval (BatOption.default (Var (Var.dummy_varinfo (TVoid [])), NoOffset) var_opt) (D.show ctx.local) (C2PODomain.show state_with_duplicated_vars);
(* remove callee vars that are not reachable and not global *)
let reachable_variables =
Var.from_varinfo (f.sformals @ f.slocals @ reachable_from_args ctx args) f.sformals
in
let new_state = D.remove_terms_not_containing_variables reachable_variables state_with_duplicated_vars in
if M.tracing then M.trace "c2po-function" "ENTER2: result: %s\n" (C2PODomain.show new_state);
[ctx.local, `Lifted (reset_normal_form new_state)]

let remove_out_of_scope_vars t f =
let local_vars = f.sformals @ f.slocals in
let duplicated_vars = f.sformals in
D.remove_terms_containing_variables (ReturnAux (TVoid [])::Var.from_varinfo local_vars duplicated_vars) t

let combine_env ctx var_opt expr f args t_context_opt t (ask: Queries.ask) =
match ctx.local with
| `Bot -> `Bot
| `Lifted cc ->
let og_t = t in
(* assign function parameters to duplicated values *)
let arg_assigns = GobList.combine_short f.sformals args in
let state_with_assignments = List.fold_left (fun st (var, exp) -> assign_term st (ask_of_ctx ctx) (T.term_of_varinfo (DuplicVar var)) (T.of_cil ask exp) var.vtype) cc arg_assigns in
if M.tracing then M.trace "c2po-function" "COMBINE_ASSIGN0: state_with_assignments: %s\n" (C2PODomain.show state_with_assignments);
(*remove all variables that were tainted by the function*)
let tainted = ask.f (MayBeTainted)
in
if M.tracing then M.trace "c2po-tainted" "combine_env: %a\n" MayBeEqual.AD.pretty tainted;
let local = D.remove_tainted_terms (ask_of_ctx ctx) tainted state_with_assignments in
match D.meet (`Lifted local) t with
| `Bot -> `Bot
| `Lifted t ->
let t = reset_normal_form @@ remove_out_of_scope_vars t f in
if M.tracing then M.trace "c2po-function" "COMBINE_ASSIGN1: var_opt: %a; local_state: %s; t_state: %s; meeting everything: %s\n" d_lval (BatOption.default (Var (Var.dummy_varinfo (TVoid[])), NoOffset) var_opt) (D.show ctx.local) (D.show og_t) (C2PODomain.show t);
`Lifted t

let combine_assign ctx var_opt expr f args t_context_opt t (ask: Queries.ask) =
match ctx.local with
| `Bot -> `Bot
| `Lifted cc ->
(* assign function parameters to duplicated values *)
let arg_assigns = GobList.combine_short f.sformals args in
let state_with_assignments = List.fold_left (fun st (var, exp) -> assign_term st (ask_of_ctx ctx) (T.term_of_varinfo (DuplicVar var)) (T.of_cil ask exp) var.vtype) cc arg_assigns in
match D.meet (`Lifted state_with_assignments) t with
| `Bot -> `Bot
| `Lifted t ->
let t = match var_opt with
| None -> t
| Some var -> assign_lval t ask var (Some (MayBeEqual.return_var (typeOfLval var)), Some Z.zero)
in
if M.tracing then M.trace "c2po-function" "COMBINE_ASSIGN2: assigning return value: %s\n" (C2PODomain.show t);
let t = reset_normal_form @@ remove_out_of_scope_vars t f
in if M.tracing then M.trace "c2po-function" "COMBINE_ASSIGN3: result: %s\n" (C2PODomain.show t); `Lifted t

let startstate v = D.top ()
let threadenter ctx ~multiple lval f args = [D.top ()]
let threadspawn ctx ~multiple lval f args fctx = D.top()
let exitstate v = D.top ()

end

let _ =
MCP.register_analysis ~dep:["startState"; "taintPartialContexts"] (module SingleThreadedLifter(Spec) : MCPSpec)
59 changes: 59 additions & 0 deletions src/analyses/singleThreadedLifter.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
(** This lifter takes an analysis that only works for single-threaded code and allows it to run on multi-threaded programs by returning top when the code might be multi-threaded.
*)

open Analyses

module SingleThreadedLifter (S: MCPSpec) =
struct
include S

let is_multithreaded (ask:Queries.ask) = not @@ ask.f (MustBeSingleThreaded {since_start = true})

let query ctx =
if is_multithreaded (ask_of_ctx ctx) then
(fun (type a) (q: a Queries.t): a Queries.result -> Queries.Result.top q) else
query ctx

let assign ctx lval expr =
if is_multithreaded (ask_of_ctx ctx) then
D.top () else
assign ctx lval expr

let branch ctx e pos =
if is_multithreaded (ask_of_ctx ctx) then
D.top () else
branch ctx e pos

let body ctx f =
if is_multithreaded (ask_of_ctx ctx) then
D.top () else
body ctx f

let return ctx exp_opt f =
if is_multithreaded (ask_of_ctx ctx) then
D.top () else
return ctx exp_opt f

let special ctx var_opt v exprs =
if is_multithreaded (ask_of_ctx ctx) then
D.top () else
special ctx var_opt v exprs

let enter ctx var_opt f args =
if is_multithreaded (ask_of_ctx ctx) then
[D.top (),D.top ()] else
enter ctx var_opt f args

let combine_env ctx var_opt expr f exprs t_context_opt t (ask: Queries.ask) =
if is_multithreaded (ask_of_ctx ctx) then
D.top () else
combine_env ctx var_opt expr f exprs t_context_opt t ask

let combine_assign ctx var_opt expr f args t_context_opt t (ask: Queries.ask) =
if is_multithreaded (ask_of_ctx ctx) then
D.top () else
combine_assign ctx var_opt expr f args t_context_opt t ask

let threadenter ctx ~multiple lval f args = [D.top ()]
let threadspawn ctx ~multiple lval f args fctx = D.top()
end
58 changes: 58 additions & 0 deletions src/analyses/startStateAnalysis.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
(** Remembers the abstract address value of each parameter at the beginning of each function by adding a ghost variable for each parameter.
Used by the c2po analysis. *)

open GoblintCil
open Batteries
open Analyses
open DuplicateVars.Var

(**First all parameters (=formals) of the function are duplicated (by using DuplicateVars),
then we remember the value of each local variable at the beginning of the function
in this new duplicated variable. *)
module Spec : Analyses.MCPSpec =
struct
let name () = "startState"
module VD = BaseDomain.VD
module AD = ValueDomain.AD
module Value = AD
module D = MapDomain.MapBot (Basetype.Variables) (Value)
module C = D

include Analyses.IdentitySpec

let ask_may_point_to (ask: Queries.ask) exp =
match ask.f (MayPointTo exp) with
| exception (IntDomain.ArithmeticOnIntegerBot _) -> AD.top()
| res -> res

let get_value (ask: Queries.ask) exp = ask_may_point_to ask exp

(** If e is a known variable (=one of the duplicated variables), then it returns the value for this variable.
If e is an unknown variable or an expression that is not simply a variable, then it returns top. *)
let eval (ask: Queries.ask) (d: D.t) (exp: exp): Value.t = match exp with
| Lval (Var x, NoOffset) -> begin match D.find_opt x d with
| Some v -> if M.tracing then M.trace "c2po-tainted" "QUERY %a : res = %a\n" d_exp exp AD.pretty v;v
| None -> Value.top()
end
| _ -> Value.top ()

let startcontext () = D.empty ()
let startstate v = D.bot ()
let exitstate = startstate

let query ctx (type a) (q: a Queries.t): a Queries.result =
let open Queries in
match q with
| MayPointTo e -> eval (ask_of_ctx ctx) ctx.local e
| _ -> Result.top q

let body ctx (f:fundec) =
(* assign function parameters *)
List.fold_left (fun st var -> let value = get_value (ask_of_ctx ctx) (Lval (Var var, NoOffset)) in
let duplicated_var = to_varinfo (DuplicVar var) in
if M.tracing then M.trace "startState" "added value: var: %a; value: %a" d_lval (Var duplicated_var, NoOffset) Value.pretty value;
D.add duplicated_var value st) (D.empty()) f.sformals
end

let _ =
MCP.register_analysis (module Spec : MCPSpec)
Loading
Loading