[inferbo] Forget only updated locations from latest prune at Store

Reviewed By: mbouaziz

Differential Revision: D13414636

fbshipit-source-id: 8dbe7ceb6

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -226,7 +226,7 @@ module TransferFunctions = struct
                 mem
           else mem
         in
-        let mem = Dom.Mem.update_latest_prune exp1 exp2 mem in
+        let mem = Dom.Mem.update_latest_prune ~updated_locs:locs exp1 exp2 mem in
         mem
     | Prune (exp, _, _, _) ->
         Sem.Prune.prune integer_type_widths exp mem

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -663,6 +663,9 @@ module PrunePairs = struct
       if is_empty_val v then raise Unreachable else v
     in
     match map subst1 x with x -> Some x | exception Unreachable -> None
+
+
+  let forget locs x = filter (fun l _ -> not (PowLoc.mem l locs)) x
 end
 
 module LatestPrune = struct
@@ -775,6 +778,22 @@ module LatestPrune = struct
             V (x, ptrue, pfalse) )
     | Top ->
         Some x
+
+
+  let forget locs =
+    let is_mem_locs x = PowLoc.mem (Loc.of_pvar x) locs in
+    function
+    | Latest p ->
+        Latest (PrunePairs.forget locs p)
+    | TrueBranch (x, p) ->
+        if is_mem_locs x then Top else TrueBranch (x, PrunePairs.forget locs p)
+    | FalseBranch (x, p) ->
+        if is_mem_locs x then Top else FalseBranch (x, PrunePairs.forget locs p)
+    | V (x, ptrue, pfalse) ->
+        if is_mem_locs x then Top
+        else V (x, PrunePairs.forget locs ptrue, PrunePairs.forget locs pfalse)
+    | Top ->
+        Top
 end
 
 module MemReach = struct
@@ -988,15 +1007,15 @@ module MemReach = struct
         m
 
 
-  let update_latest_prune : Exp.t -> Exp.t -> t -> t =
+  let update_latest_prune : updated_locs:PowLoc.t -> Exp.t -> Exp.t -> t -> t =
-   fun e1 e2 m ->
+   fun ~updated_locs e1 e2 m ->
     match (e1, e2, m.latest_prune) with
     | Lvar x, Const (Const.Cint i), LatestPrune.Latest p ->
         if IntLit.isone i then {m with latest_prune= LatestPrune.TrueBranch (x, p)}
         else if IntLit.iszero i then {m with latest_prune= LatestPrune.FalseBranch (x, p)}
-        else {m with latest_prune= LatestPrune.Top}
+        else {m with latest_prune= LatestPrune.forget updated_locs m.latest_prune}
     | _, _, _ ->
-        {m with latest_prune= LatestPrune.Top}
+        {m with latest_prune= LatestPrune.forget updated_locs m.latest_prune}
 
 
   let get_latest_prune : t -> LatestPrune.t = fun {latest_prune} -> latest_prune
@@ -1161,8 +1180,8 @@ module Mem = struct
 
   let apply_latest_prune : Exp.t -> t -> t = fun e -> map ~f:(MemReach.apply_latest_prune e)
 
-  let update_latest_prune : Exp.t -> Exp.t -> t -> t =
+  let update_latest_prune : updated_locs:PowLoc.t -> Exp.t -> Exp.t -> t -> t =
-   fun e1 e2 -> map ~f:(MemReach.update_latest_prune e1 e2)
+   fun ~updated_locs e1 e2 -> map ~f:(MemReach.update_latest_prune ~updated_locs e1 e2)
 
 
   let get_latest_prune : t -> LatestPrune.t =

infer/tests/codetoanalyze/c/bufferoverrun/issues.exp

@@ -197,8 +197,10 @@ codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVER
 codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_not_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
+codetoanalyze/c/bufferoverrun/prune_alias.c, call_forget_locs_latest_prune_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Array declaration,Array access: Offset: 10 Size: 5 by call to `forget_locs_latest_prune` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, call_latest_prune_join_3_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `n`,<Length trace>,Parameter `*a`,Array access: Offset: 3 Size: 2 by call to `latest_prune_join` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*x`,Array access: Offset: 5 Size: 5 by call to `prune_arrblk_ne` ]
+codetoanalyze/c/bufferoverrun/prune_alias.c, forget_locs_latest_prune, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/prune_alias.c, loop_prune2_Good_FP, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `length`,<Length trace>,Parameter `length`,Array declaration,Array access: Offset: [length - length + 1, length] Size: length]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]

infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c

@@ -264,3 +264,19 @@ void call_latest_prune_join_3_Bad() {
   int a[2];
   latest_prune_join(a, 3);
 }
+
+void forget_locs_latest_prune(unsigned int n) {
+  int x;
+  int* a[5];
+  if (n < 5) {
+    x = 1;
+  } else {
+    x = 0;
+    x = 2;
+  }
+  if (x) {
+    a[n] = 0;
+  }
+}
+
+void call_forget_locs_latest_prune_Bad() { forget_locs_latest_prune(10); }

infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp

@@ -26,7 +26,7 @@ void conditional_buffer_access(int* ptr, unsigned int size) {
   }
 }
 
-void call_conditional_buffer_access_Good_FP() {
+void call_conditional_buffer_access_Good() {
   int a[1];
   conditional_buffer_access(a, 1);
 }
@@ -41,13 +41,9 @@ void conditional_buffer_access2(unsigned int n) {
   conditional_buffer_access(a, n);
 }
 
-void call_conditional_buffer_access2_1_Good_FP() {
+void call_conditional_buffer_access2_1_Good() { conditional_buffer_access2(1); }
-  conditional_buffer_access2(1);
-}
 
-void call_conditional_buffer_access2_2_Good_FP() {
+void call_conditional_buffer_access2_2_Good() { conditional_buffer_access2(3); }
-  conditional_buffer_access2(3);
-}
 
 void conditional_minus(int* ptr, unsigned int size) {
   int i = 0;

infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp

@@ -28,11 +28,8 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload1_Bad, 3, BUFFE
 codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload2_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Call,Array access: Offset: 5 Size: 5]
 codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 32 Size: 30]
-codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access2_1_Good_FP, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter `n`,Array declaration,Call,<Length trace>,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 1 by call to `conditional_buffer_access2` ]
-codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access2_2_Good_FP, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter `n`,Array declaration,Call,<Length trace>,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 3 by call to `conditional_buffer_access2` ]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access3_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `size`,<Length trace>,Parameter `*ptr`,Array access: Offset: -1 Size: 1 by call to `conditional_buffer_access3` ]
-codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 1 by call to `conditional_buffer_access` ]
+codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*ptr`,Assignment,Assignment,Array access: Offset: 2 Size: 1 by call to `conditional_buffer_access` ]
-codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access_Good_FP, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 1 by call to `conditional_buffer_access` ]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus2_1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus2` ]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus2_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus2` ]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus_1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus` ]