From 64261156442de8f81680c1bffb4231653e10441a Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 19 Jan 2025 21:49:11 +0100 Subject: [PATCH 1/5] Consider pointees separately for refinement --- src/analyses/baseInvariant.ml | 19 +++++++++++++++++++ tests/regression/27-inv_invariants/24-ptr.c | 21 +++++++++++++++++++++ 2 files changed, 40 insertions(+) create mode 100644 tests/regression/27-inv_invariants/24-ptr.c diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 19a9999ecf..99a101c24b 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -100,6 +100,25 @@ struct if M.tracing then M.tracel "inv" "st from %a to %a" D.pretty st D.pretty r; r ) + | Mem (Lval lv), NoOffset -> + let lvals = eval_lv ~man st x in + let res = AD.fold (fun a acc -> + if M.tracing then M.tracel "inv" "Consider case of lval %a = %a" d_lval lv VD.pretty (Address (AD.singleton a)); + let st = set' lv (Address (AD.singleton a)) st in + let old_val = get ~man st (AD.singleton a) None in + let old_val = VD.cast (Cilfacade.typeOfLval lv) old_val in (* needed as the type of this pointer may be different *) + (* this what I would originally have liked to do, but eval_rv_lval_refine uses queries and thus stale values *) + (* let old_val = eval_rv_lval_refine ~man st exp x in *) + let old_val = map_oldval old_val (Cilfacade.typeOfLval x) in + let v = apply_invariant ~old_val ~new_val:c' in + if is_some_bot v then + D.join acc (try contra st with Analyses.Deadcode -> D.bot ()) + else ( + if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)" d_lval x VD.pretty old_val VD.pretty v pretty c VD.pretty c'; + D.join acc (set' x v st) + ) + ) lvals (D.bot ()) in + res | Var _, _ | Mem _, _ -> (* For accesses via pointers, not yet *) diff --git a/tests/regression/27-inv_invariants/24-ptr.c b/tests/regression/27-inv_invariants/24-ptr.c new file mode 100644 index 0000000000..f9d01be2a9 --- /dev/null +++ b/tests/regression/27-inv_invariants/24-ptr.c @@ -0,0 +1,21 @@ +// PARAM: --enable ana.int.interval + +int two = 2; +int three = 3; + +int main() { + int* ptr; + int top; + + if(top) { + ptr = &two; + } else { + ptr = &three; + } + + if(*ptr == 2) { + __goblint_check(ptr == &two); + } + + return 0; +} From 939cec3eaf0d4a1cda863bc00aaf85786fe8cb10 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 19 Jan 2025 22:10:14 +0100 Subject: [PATCH 2/5] Fix cast --- src/analyses/baseInvariant.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 99a101c24b..f77f9804d3 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -106,7 +106,7 @@ struct if M.tracing then M.tracel "inv" "Consider case of lval %a = %a" d_lval lv VD.pretty (Address (AD.singleton a)); let st = set' lv (Address (AD.singleton a)) st in let old_val = get ~man st (AD.singleton a) None in - let old_val = VD.cast (Cilfacade.typeOfLval lv) old_val in (* needed as the type of this pointer may be different *) + let old_val = VD.cast (Cilfacade.typeOfLval x) old_val in (* needed as the type of this pointer may be different *) (* this what I would originally have liked to do, but eval_rv_lval_refine uses queries and thus stale values *) (* let old_val = eval_rv_lval_refine ~man st exp x in *) let old_val = map_oldval old_val (Cilfacade.typeOfLval x) in From 8eb3d7294cf74475a6d4fa5c6caad2caa79b0502 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 13 Feb 2025 10:42:13 +0100 Subject: [PATCH 3/5] Do not swallow dead code and add example --- src/analyses/baseInvariant.ml | 14 ++++++---- .../27-inv_invariants/25-deadcode.c | 27 +++++++++++++++++++ 2 files changed, 36 insertions(+), 5 deletions(-) create mode 100644 tests/regression/27-inv_invariants/25-deadcode.c diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index f77f9804d3..38e09cb1d8 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -102,7 +102,7 @@ struct ) | Mem (Lval lv), NoOffset -> let lvals = eval_lv ~man st x in - let res = AD.fold (fun a acc -> + let res = AD.fold (fun a acc -> if M.tracing then M.tracel "inv" "Consider case of lval %a = %a" d_lval lv VD.pretty (Address (AD.singleton a)); let st = set' lv (Address (AD.singleton a)) st in let old_val = get ~man st (AD.singleton a) None in @@ -111,14 +111,18 @@ struct (* let old_val = eval_rv_lval_refine ~man st exp x in *) let old_val = map_oldval old_val (Cilfacade.typeOfLval x) in let v = apply_invariant ~old_val ~new_val:c' in - if is_some_bot v then + if is_some_bot v then D.join acc (try contra st with Analyses.Deadcode -> D.bot ()) else ( if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)" d_lval x VD.pretty old_val VD.pretty v pretty c VD.pretty c'; D.join acc (set' x v st) - ) - ) lvals (D.bot ()) in - res + ) + ) lvals (D.bot ()) + in + if D.is_bot res then + raise Analyses.Deadcode + else + res | Var _, _ | Mem _, _ -> (* For accesses via pointers, not yet *) diff --git a/tests/regression/27-inv_invariants/25-deadcode.c b/tests/regression/27-inv_invariants/25-deadcode.c new file mode 100644 index 0000000000..902c83ea92 --- /dev/null +++ b/tests/regression/27-inv_invariants/25-deadcode.c @@ -0,0 +1,27 @@ +// PARAM: --enable ana.int.interval + +int two = 2; +int three = 5; + +int main() { + int* ptr; + int top; + + int indicator = 1; + + if(top) { + ptr = &two; + } else { + ptr = &three; + } + + // Evaluating this in the interval domain yields [2,5] + // Only trying to optimize per-pointer discovers that this in fact dead code (https://github.com/goblint/analyzer/pull/1659) + if(*ptr == 3) { + // Dead + indicator = 0; + } + + __goblint_check(indicator == 1); + return 0; +} From bed35267ddfa7dfc577d976054052d4a41920985 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 13 Feb 2025 11:21:57 +0100 Subject: [PATCH 4/5] Generalize to arbitrary offsets --- src/analyses/baseInvariant.ml | 59 ++++++++++++--------- tests/regression/27-inv_invariants/24-ptr.c | 11 ++++ 2 files changed, 45 insertions(+), 25 deletions(-) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 38e09cb1d8..d69a190c0b 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -85,6 +85,17 @@ struct let refine_lv man st c x c' pretty exp = let set' lval v st = set st (eval_lv ~man st lval) (Cilfacade.typeOfLval lval) ~lval_raw:lval v ~man in + let default () = + (* For accesses via pointers in complicated case, no refinement yet *) + let old_val = eval_rv_lval_refine ~man st exp x in + let old_val = map_oldval old_val (Cilfacade.typeOfLval x) in + let v = apply_invariant ~old_val ~new_val:c' in + if is_some_bot v then contra st + else ( + if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)" d_lval x VD.pretty old_val VD.pretty v pretty c VD.pretty c'; + set' x v st + ) + in match x with | Var var, o when refine_entire_var -> (* For variables, this is done at to the level of entire variables to benefit e.g. from disjunctive struct domains *) @@ -100,23 +111,28 @@ struct if M.tracing then M.tracel "inv" "st from %a to %a" D.pretty st D.pretty r; r ) - | Mem (Lval lv), NoOffset -> - let lvals = eval_lv ~man st x in + | Mem (Lval lv), off -> + let lvals = eval_lv ~man st (Mem (Lval lv), off) in let res = AD.fold (fun a acc -> - if M.tracing then M.tracel "inv" "Consider case of lval %a = %a" d_lval lv VD.pretty (Address (AD.singleton a)); - let st = set' lv (Address (AD.singleton a)) st in - let old_val = get ~man st (AD.singleton a) None in - let old_val = VD.cast (Cilfacade.typeOfLval x) old_val in (* needed as the type of this pointer may be different *) - (* this what I would originally have liked to do, but eval_rv_lval_refine uses queries and thus stale values *) - (* let old_val = eval_rv_lval_refine ~man st exp x in *) - let old_val = map_oldval old_val (Cilfacade.typeOfLval x) in - let v = apply_invariant ~old_val ~new_val:c' in - if is_some_bot v then - D.join acc (try contra st with Analyses.Deadcode -> D.bot ()) - else ( - if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)" d_lval x VD.pretty old_val VD.pretty v pretty c VD.pretty c'; - D.join acc (set' x v st) - ) + match a with + | Addr (base, _) as orig -> + let (a:VD.t) = Address (AD.singleton (AD.Addr.of_var base)) in + if M.tracing then M.tracel "invo" "Consider case of lval %a = %a" d_lval lv VD.pretty a; + let st = set' lv a st in + let old_val = get ~man st (AD.singleton orig) None in + let old_val = VD.cast (Cilfacade.typeOfLval x) old_val in (* needed as the type of this pointer may be different *) + (* this what I would originally have liked to do, but eval_rv_lval_refine uses queries and thus stale values *) + (* let old_val = eval_rv_lval_refine ~man st exp x in *) + let old_val = map_oldval old_val (Cilfacade.typeOfLval x) in + let v = apply_invariant ~old_val ~new_val:c' in + if is_some_bot v then + D.join acc (try contra st with Analyses.Deadcode -> D.bot ()) + else ( + if M.tracing then M.tracel "invo" "improve lval %a from %a to %a (c = %a, c' = %a)" d_lval x VD.pretty old_val VD.pretty v pretty c VD.pretty c'; + D.join acc (set' x v st) + ) + | _ -> + default () ) lvals (D.bot ()) in if D.is_bot res then @@ -125,15 +141,8 @@ struct res | Var _, _ | Mem _, _ -> - (* For accesses via pointers, not yet *) - let old_val = eval_rv_lval_refine ~man st exp x in - let old_val = map_oldval old_val (Cilfacade.typeOfLval x) in - let v = apply_invariant ~old_val ~new_val:c' in - if is_some_bot v then contra st - else ( - if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)" d_lval x VD.pretty old_val VD.pretty v pretty c VD.pretty c'; - set' x v st - ) + default () + let invariant_fallback man st exp tv = (* We use a recursive helper function so that x != 0 is false can be handled diff --git a/tests/regression/27-inv_invariants/24-ptr.c b/tests/regression/27-inv_invariants/24-ptr.c index f9d01be2a9..495371efe7 100644 --- a/tests/regression/27-inv_invariants/24-ptr.c +++ b/tests/regression/27-inv_invariants/24-ptr.c @@ -3,19 +3,30 @@ int two = 2; int three = 3; +struct s { int content; }; +struct s twostruct = {2}; +struct s threestruct = {3}; + int main() { int* ptr; + struct s* ptrstruct; int top; if(top) { ptr = &two; + ptrstruct = &twostruct; } else { ptr = &three; + ptrstruct = &threestruct; } if(*ptr == 2) { __goblint_check(ptr == &two); } + if(ptrstruct->content == 2) { + __goblint_check(ptrstruct == &twostruct); + } + return 0; } From 513ebb57939759127bca021b1b9714cf2532dbf4 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 13 Feb 2025 11:33:02 +0100 Subject: [PATCH 5/5] Switch back to default tracing --- src/analyses/baseInvariant.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index d69a190c0b..a28c09e621 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -117,7 +117,7 @@ struct match a with | Addr (base, _) as orig -> let (a:VD.t) = Address (AD.singleton (AD.Addr.of_var base)) in - if M.tracing then M.tracel "invo" "Consider case of lval %a = %a" d_lval lv VD.pretty a; + if M.tracing then M.tracel "inv" "Consider case of lval %a = %a" d_lval lv VD.pretty a; let st = set' lv a st in let old_val = get ~man st (AD.singleton orig) None in let old_val = VD.cast (Cilfacade.typeOfLval x) old_val in (* needed as the type of this pointer may be different *) @@ -128,7 +128,7 @@ struct if is_some_bot v then D.join acc (try contra st with Analyses.Deadcode -> D.bot ()) else ( - if M.tracing then M.tracel "invo" "improve lval %a from %a to %a (c = %a, c' = %a)" d_lval x VD.pretty old_val VD.pretty v pretty c VD.pretty c'; + if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)" d_lval x VD.pretty old_val VD.pretty v pretty c VD.pretty c'; D.join acc (set' x v st) ) | _ ->