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

Linear Two-Variable Equalities Analysis #1297

Merged
merged 274 commits into from
Mar 25, 2024
Merged
Changes from 1 commit
Commits
Show all changes
274 commits
Select commit Hold shift + click to select a range
2a96d13
test cases
jennieliangga Dec 5, 2023
63b602c
test cases
jennieliangga Dec 6, 2023
2f7ec03
meet_tcons first draft
Dec 6, 2023
8d0337d
Merge branch 'relational-domains' into test
jennieliangga Dec 6, 2023
63b45a5
adjustments in meet_tcons and incorporated meet but not tested yet
Dec 6, 2023
953599f
moved number_vars to get_coeff
reb-ddm Dec 6, 2023
1179feb
Merge branch 'relational-domains' of github.com:reb-ddm/analyzer into…
jennieliangga Dec 6, 2023
14670a7
meet_tcons finished
Dec 6, 2023
ab43a2b
meet_tcons small refinement
Dec 6, 2023
6752716
First quick test
Dec 6, 2023
f69a922
added preliminary implementation for leq
nicolaifrech Dec 6, 2023
a375509
fuer rebecca
Dec 6, 2023
c46a8ca
Merge branch 'relational-domains' of github.com:reb-ddm/analyzer into…
Dec 6, 2023
d672d45
added preliminary version of join
nicolaifrech Dec 6, 2023
eed4dfe
changed returned value in join
nicolaifrech Dec 6, 2023
20cd10e
Fixed bug in abstract_exists
reb-ddm Dec 6, 2023
9ef83bd
Merge branch 'relational-domains' of github.com:reb-ddm/analyzer into…
reb-ddm Dec 6, 2023
384223e
testing in analysis file, test2 shows error in meet, but likely cause…
Dec 6, 2023
af3fd6a
Added comment explaining overflow flag in assign_exp and fixed indent…
reb-ddm Dec 8, 2023
6e501e4
Merge goblint main branch into relational-domains branch
reb-ddm Dec 8, 2023
8d2f9d5
Debugged functions to change dimension of the array
reb-ddm Dec 10, 2023
0a5eb8e
changed leq in linearTwoVarEqualityDomain.apron.ml
nicolaifrech Dec 13, 2023
d8111b8
Adjustments meet_tcons
Dec 13, 2023
504f05b
fixed top and bug in assign_texpr
reb-ddm Dec 13, 2023
4178745
fixed bug in join where it returned an empty array instead of the top…
reb-ddm Dec 13, 2023
b2e6515
Update linearTwoVarEqualityDomain.apron.ml
nicolaifrech Dec 13, 2023
e1a7d4d
fixed bug in meet_tcons
reb-ddm Dec 13, 2023
e2e3dca
This time really fixed the bug in meet_tcons
reb-ddm Dec 13, 2023
de1c517
Merge master into relational-domains
reb-ddm Dec 13, 2023
d0018b9
revert unwanted changes
reb-ddm Dec 13, 2023
22e146c
### Bot_env vs. Bot
Dec 13, 2023
469fd4d
Update linearTwoVarEqualityDomain.apron.ml
nicolaifrech Dec 13, 2023
89b47a5
test cases adapted
jennieliangga Dec 14, 2023
9251332
Restored previous version
reb-ddm Dec 14, 2023
0d099d6
REmoved a few comments
reb-ddm Dec 14, 2023
61ae1f7
test cases adapted
jennieliangga Dec 14, 2023
b8374c0
test cases updated
jennieliangga Dec 14, 2023
ee2f7d7
test cases updated
jennieliangga Dec 14, 2023
1cf7115
test cases updated
jennieliangga Dec 15, 2023
97d57b1
test cases updated
jennieliangga Dec 15, 2023
f32d554
test cases updated
jennieliangga Dec 15, 2023
8616237
Pull request comment Rebecca
Dec 15, 2023
395b688
Merge branch 'linear-two-var-equality' of github.com:reb-ddm/analyzer…
jennieliangga Dec 15, 2023
44fe307
Added comment about extension to pull request
Dec 15, 2023
d4519a1
Adapted the get_coeff and get_coeff_vec functions to recognize more e…
reb-ddm Dec 15, 2023
1c242ad
removed a test
reb-ddm Dec 17, 2023
60922f3
typo
Dec 17, 2023
cb9e86e
Merge branch 'linear-two-var-equality' of github.com:reb-ddm/analyzer…
Dec 17, 2023
521cbcf
Merge branch 'master' into linear-two-var-equality
alina-weber Dec 17, 2023
bd7e5c5
Merge branch 'master' into linear-two-var-equality
reb-ddm Dec 17, 2023
239c945
Merge branch 'linear-two-var-equality' of github.com:reb-ddm/analyzer…
reb-ddm Dec 17, 2023
7371a34
Update src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
alina-weber Dec 20, 2023
0d42a74
Fixed semgrep warnings
reb-ddm Dec 20, 2023
3e9605f
changed line ending in affineEqualityAnalysis.apron.ml
reb-ddm Dec 20, 2023
7ed2d38
revert changed line ending in affineEqualityAnalysis.apron.ml
reb-ddm Dec 20, 2023
ca8bf91
added line ending in affineEqualityAnalysis.apron.ml
reb-ddm Dec 20, 2023
561ee06
Removed notes and added whitespace
reb-ddm Dec 20, 2023
e1841b0
Adjusted meet_tcons according to pull_request review
Dec 20, 2023
b5c4bf6
removed pull request file
reb-ddm Dec 20, 2023
314137b
fixed submodule
reb-ddm Dec 21, 2023
211ba13
added named arguments for add and del
reb-ddm Dec 21, 2023
976b338
removed a match statement
reb-ddm Dec 21, 2023
4e0ecf0
Small fix
Dec 21, 2023
cab810a
improve code style
reb-ddm Dec 21, 2023
1736379
Incorporated some change requests
Jan 2, 2024
0b6ca62
suggested changes and bug fix, added corresponding test case
reb-ddm Jan 3, 2024
7e0e261
Worked in comments of pull request
Jan 3, 2024
58a68f9
Added names to Tests
Jan 3, 2024
eab72d6
adjustments according to comments
Jan 3, 2024
d911458
small adjustment
Jan 3, 2024
667261f
Implemented oerflow handling and added corresponding tests
reb-ddm Jan 3, 2024
2845adf
bug fix
reb-ddm Jan 3, 2024
968232e
new and shorter Join function
Jan 4, 2024
7c5dd9e
Added some comments
Jan 4, 2024
c8393ff
fix format
Jan 4, 2024
3764ad7
Small fix in join
Jan 4, 2024
9922c5c
replaced identity with top_of
Jan 4, 2024
ad7fd1e
added GobArray patch by Michael Schwarz
reb-ddm Jan 4, 2024
f872e55
bug fix and refactored meet_tcons
reb-ddm Jan 4, 2024
46802dd
Added two test cases for join
reb-ddm Jan 4, 2024
5f56257
Fix trailing whitespace and newlines
reb-ddm Jan 4, 2024
4584f8c
simplified join further
reb-ddm Jan 4, 2024
89ab4ba
Update src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
alina-weber Jan 4, 2024
e326fe1
small adjustion
Jan 4, 2024
edb93b3
remove type annotation
reb-ddm Jan 4, 2024
debcdc1
test cases adapted
jennieliangga Jan 7, 2024
13d38ad
fixed a bug in join and also a bug in del_cols. Adapted corresponding…
reb-ddm Jan 7, 2024
844e249
Removed commented out code
reb-ddm Jan 7, 2024
9fb3e60
Merge branch 'master' into linear-two-var-equality
reb-ddm Jan 7, 2024
ce415e5
Small adjustment in Join
Jan 8, 2024
c332c00
Beautification of test and join
Jan 8, 2024
26e602f
Join Optimization
Jan 8, 2024
b12cabc
fix tests naming issue
reb-ddm Jan 8, 2024
d5bfcdd
simplify a bit leq and meet
reb-ddm Jan 8, 2024
c9d0442
divided meet function into meet and meet_with_one_conj and fixed bug …
reb-ddm Jan 8, 2024
48a45cb
invariant function
jennieliangga Jan 8, 2024
2333aba
remove an indirection
reb-ddm Jan 9, 2024
0b5cb5c
fix spelling
reb-ddm Jan 9, 2024
e4034b3
function call test
Jan 10, 2024
68c42f6
fix test
Jan 10, 2024
0b3e1e5
fix invariant function
jennieliangga Jan 10, 2024
324758a
fix invariant functio
jennieliangga Jan 10, 2024
26340f4
fixed big in del_cols
reb-ddm Jan 10, 2024
f4e1495
fix invariant function
jennieliangga Jan 10, 2024
1bfdb88
Test for simple pointers
Jan 11, 2024
f091430
fix invariant function
jennieliangga Jan 11, 2024
fc61cbc
Test case for sum of variables with the same reference variable
reb-ddm Jan 11, 2024
38a8ed2
merge with master branch
reb-ddm Jan 11, 2024
3b9ad39
fix invariant function
jennieliangga Jan 11, 2024
97f25be
add unsound test case so that we can debug
reb-ddm Jan 12, 2024
51359ef
add test
reb-ddm Jan 12, 2024
8767785
add same test to affeq because it also fails there
reb-ddm Jan 12, 2024
c2f4136
remove unused function
reb-ddm Jan 15, 2024
9d441f9
optimized reduce_col_with as suggested by Michael Petter
reb-ddm Jan 15, 2024
8b92e55
fix test order
reb-ddm Jan 15, 2024
ce0fd2e
Merge branch 'master' into linear-two-var-equality
reb-ddm Jan 15, 2024
72f811d
add failing tests with casts
reb-ddm Jan 17, 2024
9878cb5
delete duplicated tests
jennieliangga Jan 17, 2024
35a2fcf
optimized assignment such that it also understands sums of multiple d…
reb-ddm Jan 17, 2024
25f8296
refactor VarManagement s.t. the names of del_cols and add_empty_colum…
reb-ddm Jan 18, 2024
2c792e6
modified add_cols and del_cols as suggested by Michael Petter
reb-ddm Jan 18, 2024
e080da4
modified subtract_const_from_var as suggested
reb-ddm Jan 18, 2024
acf258a
show more readable now
Jan 18, 2024
9949d98
many small adjustments that were requested
reb-ddm Jan 18, 2024
5c7ba60
adjusted configuration for svcomp-tests to run properly
Jan 19, 2024
605d03e
proper sorting of files
Jan 19, 2024
f59246f
test cases adapted
jennieliangga Jan 19, 2024
c439043
test cases adapted
jennieliangga Jan 19, 2024
189f6eb
adapted some tests
reb-ddm Jan 21, 2024
1c7d625
added test with return value
reb-ddm Jan 21, 2024
f0e1f8a
added semicolon to the show function
reb-ddm Jan 21, 2024
8dbed52
test cases adapted
jennieliangga Jan 23, 2024
80ab209
implement MaySignedOverflow query in base analysis
reb-ddm Jan 28, 2024
30a42cd
use new MaySignedOverflow query in relationAnalysis
reb-ddm Jan 28, 2024
7b05557
add MaySignedOverflow query to queries.ml
reb-ddm Jan 28, 2024
4136efe
remove all the old overflow analysis from affeq and lin2vareq and mov…
reb-ddm Jan 28, 2024
f5a287f
move apron overflow analysis to apronDomain.apron.ml. Before it was i…
reb-ddm Jan 28, 2024
80dc45f
fixed problem with affeq tests that was caused by 2 variables having …
reb-ddm Jan 28, 2024
e19827f
fixed MaySignedOverflow and apron overflow analysis and no_overflow f…
reb-ddm Jan 28, 2024
813127b
reverted all overflow handling of the apron domain to its original st…
reb-ddm Jan 28, 2024
46940b2
moved conversion to texpr of apron back to shared functions, because …
reb-ddm Jan 29, 2024
760baa3
narrowing and casting tests
jennieliangga Jan 29, 2024
1edbfe7
added tests for overflow
reb-ddm Jan 29, 2024
6a96afd
made overflow check in shared functions more readable and with less c…
reb-ddm Jan 29, 2024
10ba24a
fix indentation and one of the affeq tests
reb-ddm Jan 31, 2024
edfec58
Overflow handling in `lin2vareq` and `affeq`
reb-ddm Jan 31, 2024
4806036
Added Cast Analysis and merged with Overflow Analysis
Jan 31, 2024
63455d8
changed ov to no_ov in some functions
reb-ddm Jan 31, 2024
395cab6
merged with master
reb-ddm Jan 31, 2024
b385153
fixed conflict in base.ml
reb-ddm Jan 31, 2024
b362951
fix semgrep warning
reb-ddm Jan 31, 2024
93dcd3c
fixed indentation
reb-ddm Jan 31, 2024
4fa7042
Narrowing test (not working though, but should)
Jan 31, 2024
61124e7
Merge branch 'linear-two-var-equality' of github.com:reb-ddm/analyzer…
Jan 31, 2024
0e7a2e9
unfinished adjustment of maySignedOverflow
Feb 1, 2024
6dc7ddd
fix the overflow analysis
reb-ddm Feb 1, 2024
f483830
fix overflow analysis
reb-ddm Feb 1, 2024
3a0318a
fix overflow analysis
reb-ddm Feb 1, 2024
118064b
new tests for better overflow checking
Feb 1, 2024
ea4cdce
add a thorough overflow test
reb-ddm Feb 1, 2024
b0cda4f
next try narrow test
Feb 1, 2024
2b0ad77
tracing for narrow and widen as well as a narrow test showing that me…
Feb 1, 2024
26bafba
small changes requested in the pull request
reb-ddm Feb 2, 2024
7b303de
fix compare Z
Feb 5, 2024
a01a7c9
Merge branch 'linear-two-var-equality' of github.com:reb-ddm/analyzer…
Feb 5, 2024
9e160a0
Some requested adjsutments
Feb 5, 2024
65fbe08
removed unnecessary test
Feb 5, 2024
e2fe8c0
some requested changes
reb-ddm Feb 5, 2024
fb0d57e
revert changes to affeq test
reb-ddm Feb 5, 2024
7425b7d
merge with main
reb-ddm Feb 5, 2024
d8459ff
Remove intermediate module definition in lin2vareq, the same as jerha…
reb-ddm Feb 5, 2024
e07608f
Test meet_tcons
Feb 5, 2024
418b7a6
fixed cast exception for non integer types
Feb 5, 2024
860eb5e
Some more fixes for get_ikind_exp
Feb 5, 2024
82db782
Some more fixes for get_ikind_exp
Feb 5, 2024
746ade0
Some more fixes for get_ikind_exp
Feb 5, 2024
91623fc
Fix Z.Overflow
Feb 6, 2024
61a5ab7
delete unused tests
jennieliangga Feb 6, 2024
ce98fc3
merge do_overflow_check structure with allow_globl structure
reb-ddm Feb 6, 2024
0fb929b
delete duplicated tests
jennieliangga Feb 6, 2024
8892f3b
revert unrelated changes in base.ml
reb-ddm Feb 6, 2024
5b51a01
use ctx.ask
reb-ddm Feb 6, 2024
3e6367f
remove redundant preprocessing for no_overflow
reb-ddm Feb 6, 2024
7295742
Adjusted comment
Feb 6, 2024
4bf9101
Merge branch 'master' into linear-two-var-equality
michael-schwarz Feb 8, 2024
61e2bce
Add CI jobs
michael-schwarz Feb 8, 2024
f798867
Rewrite `show`
michael-schwarz Feb 8, 2024
a076907
Rewrite `invariant`
michael-schwarz Feb 8, 2024
e352e2a
Doc comments
michael-schwarz Feb 8, 2024
1e3a52d
Make code a bit more idiomatic
michael-schwarz Feb 8, 2024
c3f099e
indent
michael-schwarz Feb 8, 2024
14a24b8
Simplify
michael-schwarz Feb 8, 2024
cc36e35
Replace unused arguments with `_` in `no_ov_overflow_handling`
michael-schwarz Feb 8, 2024
094f886
Some simplifications
michael-schwarz Feb 8, 2024
7d4676a
Simp
michael-schwarz Feb 8, 2024
643bb79
Simplify
michael-schwarz Feb 8, 2024
faf75a9
Simplify
michael-schwarz Feb 8, 2024
ed81c0d
cleaned up shift and indexlist creation in add_variables_to_domain
DrMichaelPetter Feb 9, 2024
2515fa0
satisfy ocp-indent
DrMichaelPetter Feb 9, 2024
5ecacbe
Add failing test
michael-schwarz Feb 9, 2024
7b88d21
ocp-indent again
DrMichaelPetter Feb 9, 2024
bb48962
Simplify
michael-schwarz Feb 9, 2024
1b4ac71
Rm unused function
michael-schwarz Feb 9, 2024
506ab22
Rm unneeded code
michael-schwarz Feb 9, 2024
428e2ee
Simplify assign_texpr
michael-schwarz Feb 9, 2024
b50e9c7
Skip detour
michael-schwarz Feb 9, 2024
6388bb5
Add TODOs
michael-schwarz Feb 9, 2024
84f39b6
gotten rid of the reference
DrMichaelPetter Feb 10, 2024
81d5106
forgot about the option
DrMichaelPetter Feb 10, 2024
c851641
got rid of count_matching and findi
DrMichaelPetter Feb 12, 2024
a1582e4
next ref removed
DrMichaelPetter Feb 13, 2024
dab1cf2
get_coeff_vec renovated
DrMichaelPetter Feb 13, 2024
fcaa3a8
minor tweaks
DrMichaelPetter Feb 13, 2024
8b6b68a
refactored and renamed
DrMichaelPetter Feb 13, 2024
453a1bb
bot_env treatment more explicit
DrMichaelPetter Feb 15, 2024
cf5b193
small tweaks
DrMichaelPetter Feb 19, 2024
017bd4f
Merge branch 'master' into linear-two-var-equality
DrMichaelPetter Feb 22, 2024
b19df55
Merge remote-tracking branch 'upstream/master' into linear-two-var-eq…
DrMichaelPetter Feb 26, 2024
ec9d3d3
with dunefile for lin2vareq
DrMichaelPetter Feb 26, 2024
b514242
pushed test to the back
DrMichaelPetter Feb 26, 2024
b6e7741
Merge branch 'master' into linear-two-var-equality
DrMichaelPetter Feb 27, 2024
6961d73
typo in filename
DrMichaelPetter Feb 27, 2024
25407b5
fixed bug in base analysis' int evaluation wrt. comparison of address…
DrMichaelPetter Mar 1, 2024
8595c19
Merge branch 'master' into linear-two-var-equality
DrMichaelPetter Mar 1, 2024
e9ce7a8
Update src/analyses/mCP.ml
DrMichaelPetter Mar 1, 2024
694811d
Merge branch 'master' into linear-two-var-equality
DrMichaelPetter Mar 4, 2024
48bacb5
fixed overaggressive simplification of constraints via texpr1_expr_of…
DrMichaelPetter Mar 5, 2024
4781cf0
Merge branch 'master' into linear-two-var-equality
DrMichaelPetter Mar 5, 2024
f71a966
gotten rid of _old versions of *_of_cil_exp
DrMichaelPetter Mar 5, 2024
99c1be4
find_one_var is dead code after removal of meet_tcons_one_var_eq
DrMichaelPetter Mar 5, 2024
550bb0a
constFold is literally the first thing that is done straight down the…
DrMichaelPetter Mar 5, 2024
e50ad8d
Unify overflow handling for relational domains
michael-schwarz Mar 6, 2024
d44b026
unnecessary trace
DrMichaelPetter Mar 6, 2024
0818be8
Simplify a few expressions in lin2vareq
sim642 Mar 8, 2024
678b833
Add TODOs to lin2vareq
sim642 Mar 8, 2024
bdc62e7
Sort Goblint_std alphabetically
sim642 Mar 8, 2024
8908b7a
implemented change requests; more docs and some refactoring
DrMichaelPetter Mar 11, 2024
d20414f
Merge branch 'master' into linear-two-var-equality
DrMichaelPetter Mar 11, 2024
96ccd4a
Add soundness check for unsigned overflows
michael-schwarz Mar 11, 2024
56ee1a6
overflow caching bug
DrMichaelPetter Mar 19, 2024
d9bd428
removed state-dependency from query_evalint
DrMichaelPetter Mar 19, 2024
5750801
reestablished bottom-free arithmetics on final solution
DrMichaelPetter Mar 19, 2024
3a95b07
Merge remote-tracking branch 'upstream/master' into linear-two-var-eq…
DrMichaelPetter Mar 19, 2024
d290f19
adapted linearTwoVariableEqualityDomain to new top handling
DrMichaelPetter Mar 19, 2024
3e42bbb
77: Explain why tests that pass with base only are helpful
michael-schwarz Mar 23, 2024
90334ae
Add TODO for comment left over from review
michael-schwarz Mar 23, 2024
a9b0b44
Remove resolved TODO
michael-schwarz Mar 23, 2024
76aad67
Make tracing output consistent
michael-schwarz Mar 23, 2024
e267f74
Use deriving where possible
sim642 Mar 20, 2024
9a1486b
this is not at all reachable
DrMichaelPetter Mar 25, 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
Prev Previous commit
Next Next commit
Rewrite show
michael-schwarz committed Feb 8, 2024

Unverified

This commit is not signed, but one or more authors requires that any commit attributed to them is signed.
commit f7988678599e6da0e14f094c3ea8fe87993a06e3
30 changes: 18 additions & 12 deletions src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
Original file line number Diff line number Diff line change
@@ -291,24 +291,30 @@ struct
(*this shows "top" for a specific environment to enable the calculations. It is the top_of of all equalities*)
let top_of env = {d = Some (EArray.make_empty_array (Environment.size env)); env = env}

(*Is not expected to be called but implemented for completeness *)
(** Is not expected to be called but implemented for completeness *)
let top () = {d = Some (EArray.empty()); env = empty_env}

(*is_top returns true for top_of array and empty array *)
(** is_top returns true for top_of array and empty array *)
let is_top t = GobOption.exists EArray.is_top_array t.d

(* prints the current variable equalities with resolved variable names *)
(** prints the current variable equalities with resolved variable names *)
let show varM =
let lookup i = Var.to_string (Environment.var_of_dim varM.env i) in
let show_var i tuple =
match tuple with
| (None, offset) -> (lookup i) ^ " = " ^ Z.to_string offset ^ ";\n"
| (Some index, offset) -> (lookup i) ^ " = " ^ lookup index ^
(if offset <> Z.zero then " + " ^ Z.to_string offset else "") ^ ";\n"
in if is_top varM then "⊤\n" else
match varM.d with
| None -> "⊥\n"
| Some arr -> if is_bot varM then "Bot \n" else Array.fold_left (fun acc elem -> acc ^ elem ) "" (Array.mapi show_var arr)
let show_offs o = if Z.equal o Z.zero then "" else " + " ^ Z.to_string o in
let show_var i = function
| (None, o) -> (lookup i) ^ " = " ^ Z.to_string o ^ ";\n"
| (Some index, o) when i <> index ->
(lookup i) ^ " = " ^ lookup index ^ show_offs o ^ ";\n"
| _ -> ""
in
match varM.d with
| None -> "⊥\n"
| Some arr when EArray.is_top_array arr -> "⊤\n"
| Some arr ->
if is_bot varM then
"Bot \n"
else
Array.fold_lefti (fun acc i elem -> acc ^ show_var i elem) "" arr

let pretty () (x:t) = text (show x)
let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nequalities-array\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%s</value>\n</map>\n</value>\n" (XmlUtil.escape (Format.asprintf "%s" (show x) )) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (x.env)))