diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 484d7bac62..fd52d099bf 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,17 +111,36 @@ struct if M.tracing then M.tracel "inv" "st from %a to %a" D.pretty st D.pretty r; r ) + | Mem (Lval lv), off -> + let lvals = eval_lv ~man st (Mem (Lval lv), off) in + let res = AD.fold (fun a acc -> + Option.bind acc (fun acc -> + 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 "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 *) + (* 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 + Some (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'; + Some (D.join acc (set' x v st)) + ) + | _ -> None + ) + ) lvals (Some (D.bot ())) + in + BatOption.map_default_delayed (fun d -> if D.is_bot d then raise Analyses.Deadcode else d) default 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 new file mode 100644 index 0000000000..495371efe7 --- /dev/null +++ b/tests/regression/27-inv_invariants/24-ptr.c @@ -0,0 +1,32 @@ +// PARAM: --enable ana.int.interval + +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; +} 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; +}