[inferbo] Accumulate LatestPrune in sequential prunings

Summary:
This diff accumulates LatestPrune in sequential prunings. It should be sound since Inferbo invalidates some data of LatestPrune if they are updated.

Depends on D14321534

Reviewed By: mbouaziz

Differential Revision: D14321575

fbshipit-source-id: 233dbae32

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -1342,7 +1342,7 @@ module MemReach = struct
    fun prune_pairs m -> {m with latest_prune= LatestPrune.Latest prune_pairs}
 
 
-  let apply_latest_prune : Exp.t -> t -> t =
+  let apply_latest_prune : Exp.t -> t -> t * PrunePairs.t =
     let apply1 l v acc = update_mem (PowLoc.singleton l) (PrunedVal.get_val v) acc in
     fun e m ->
       match (m.latest_prune, e) with
@@ -1350,11 +1350,11 @@ module MemReach = struct
       | LatestPrune.V (x, _, prunes), Exp.UnOp (Unop.LNot, Exp.Var r, _) -> (
         match find_simple_alias r m with
         | Some (Loc.Var (Var.ProgramVar y), None) when Pvar.equal x y ->
-            PrunePairs.fold apply1 prunes m
+            (PrunePairs.fold apply1 prunes m, prunes)
         | _ ->
-            m )
+            (m, PrunePairs.empty) )
       | _ ->
-          m
+          (m, PrunePairs.empty)
 
 
   let update_latest_prune : updated_locs:PowLoc.t -> Exp.t -> Exp.t -> t -> t =
@@ -1563,14 +1563,21 @@ module Mem = struct
    fun prune_pairs -> map ~f:(MemReach.set_prune_pairs prune_pairs)
 
 
-  let apply_latest_prune : Exp.t -> t -> t = fun e -> map ~f:(MemReach.apply_latest_prune e)
+  let apply_latest_prune : Exp.t -> t -> t * PrunePairs.t =
+   fun e -> function
+    | Bottom ->
+        (Bottom, PrunePairs.empty)
+    | NonBottom m ->
+        let m, prune_pairs = MemReach.apply_latest_prune e m in
+        (NonBottom m, prune_pairs)
+
 
   let update_latest_prune : updated_locs:PowLoc.t -> Exp.t -> Exp.t -> t -> t =
    fun ~updated_locs e1 e2 -> map ~f:(MemReach.update_latest_prune ~updated_locs e1 e2)
 
 
   let get_latest_prune : t -> LatestPrune.t =
-    f_lift_default ~default:LatestPrune.Top MemReach.get_latest_prune
+   fun m -> f_lift_default ~default:LatestPrune.Top MemReach.get_latest_prune m
 
 
   let get_relation : t -> Relation.t =

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -657,14 +657,12 @@ module Prune = struct
 
   let prune : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Mem.t =
    fun integer_type_widths e mem ->
-    let mem = Mem.apply_latest_prune e mem in
+    let mem, prune_pairs = Mem.apply_latest_prune e mem in
     let mem =
       let constrs = Relation.Constraints.of_exp e ~get_sym_f:(get_sym_f integer_type_widths mem) in
       Mem.meet_constraints constrs mem
     in
-    let {mem; prune_pairs} =
+    let {mem; prune_pairs} = prune_helper integer_type_widths e {mem; prune_pairs} in
-      prune_helper integer_type_widths e {mem; prune_pairs= PrunePairs.empty}
-    in
     Mem.set_prune_pairs prune_pairs mem
 end
 

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

@@ -118,9 +118,7 @@ codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_b
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 6 Size: 5]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_2, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 4 Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Call,Parameter `__n`,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Call,Unknown value from: std::distance<std::__wrap_iter<const_Int_no_copy_*>_>,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Call,Unknown value from: std::distance<std::__wrap_iter<const_Int_no_copy_*>_>,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,<RHS trace>,Parameter `__n`,Binary operation: ([3, +oo] + 42):unsigned64]

infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp

@@ -165,7 +165,7 @@ void assert_Good() {
   v[4] = 1;
 }
 
-void assert_Good_FP(int x) {
+void assert_Good_2(int x) {
   std::vector<int> v;
   for (int i = 0; i < 5; i++) {
     v.push_back(1);