Merge pull request #1659 from goblint/issue_1658

Consider pointees separately for refinement

Author: michael-schwarz

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

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;
+}

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;
+}