[inferbo] Prune by assert

Summary:
It prunes abstract memories on `assert` commands.

Problem: Since the assert command is sometimes translated to two
sequential `if` statments, it was not able to prune the memory
precisely at `assert` commands in Inferbo---the pruned memory at the
first branch was joined before the second branch.

Solution: To avoid losing the pruning information at the first branch,
now, it records which locations are pruned at the first branch and
applies the same pruning at the next branch if they have
semantically the same condition.

Reviewed By: mbouaziz

Differential Revision: D6895919

fbshipit-source-id: 15ac1cb

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -204,19 +204,23 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             let locs = Sem.eval exp1 mem |> Dom.Val.get_all_locs in
             let v = Sem.eval exp2 mem |> Dom.Val.add_trace_elem (Trace.Assign location) in
             let mem = Dom.Mem.update_mem locs v mem in
-            if PowLoc.is_singleton locs then
+            let mem =
-              let loc_v = PowLoc.min_elt locs in
+              if PowLoc.is_singleton locs then
-              match Typ.Procname.get_method pname with
+                let loc_v = PowLoc.min_elt locs in
-              | "__inferbo_empty" when Loc.is_return loc_v -> (
+                match Typ.Procname.get_method pname with
-                match Sem.get_formals pdesc with
+                | "__inferbo_empty" when Loc.is_return loc_v -> (
-                | [(formal, _)] ->
+                  match Sem.get_formals pdesc with
-                    let formal_v = Dom.Mem.find_heap (Loc.of_pvar formal) mem in
+                  | [(formal, _)] ->
-                    Dom.Mem.store_empty_alias formal_v loc_v exp2 mem
+                      let formal_v = Dom.Mem.find_heap (Loc.of_pvar formal) mem in
+                      Dom.Mem.store_empty_alias formal_v loc_v exp2 mem
+                  | _ ->
+                      assert false )
                 | _ ->
-                    assert false )
+                    Dom.Mem.store_simple_alias loc_v exp2 mem
-              | _ ->
+              else mem
-                  Dom.Mem.store_simple_alias loc_v exp2 mem
+            in
-            else mem
+            let mem = Dom.Mem.update_latest_prune exp1 exp2 mem in
+            mem
         | Prune (exp, _, _, _) ->
             Sem.prune exp mem
         | Call (ret, Const Cfun callee_pname, params, location, _) -> (

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -49,6 +49,8 @@ module Val = struct
       && ArrayBlk.( <= ) ~lhs:lhs.arrayblk ~rhs:rhs.arrayblk
 
 
+  let equal x y = phys_equal x y || ( <= ) ~lhs:x ~rhs:y && ( <= ) ~lhs:y ~rhs:x
+
   let widen ~prev ~next ~num_iters =
     if phys_equal prev next then prev
     else
@@ -494,18 +496,102 @@ module Alias = struct
     fun temps a -> (AliasMap.remove_temps temps (fst a), snd a)
 end
 
+module PrunePairs = struct
+  module PrunePair = struct
+    (* PrunePair.t is a pair of an abstract location and an abstract
+       value where the abstract location was updated with the abstract
+       value in the latest pruning. *)
+    type t = Loc.t * Val.t
+
+    let equal ((l1, v1) as x) ((l2, v2) as y) =
+      phys_equal x y || Loc.equal l1 l2 && Val.equal v1 v2
+  end
+
+  type t = PrunePair.t list
+
+  let empty = []
+
+  let equal x y = List.equal x y ~equal:PrunePair.equal
+end
+
+module LatestPrune = struct
+  (* Latest p: The pruned pairs 'p' has pruning information (which
+     abstract locations are updated by which abstract values) in the
+     latest pruning.
+
+     TrueBranch (x, p): After a pruning, the variable 'x' is assigned
+     by 1.  There is no other memory updates after the latest pruning.
+
+     FalseBranch (x, p): After a pruning, the variable 'x' is assigned
+     by 0.  There is no other memory updates after the latest pruning.
+
+     V (x, ptrue, pfalse): After two non-sequential prunings ('ptrue'
+     and 'pfalse'), the variable 'x' is assigned by 1 and 0,
+     respectively.  There is no other memory updates after the latest
+     prunings.
+
+     Top: No information about the latest pruning. *)
+  type astate =
+    | Latest of PrunePairs.t
+    | TrueBranch of Pvar.t * PrunePairs.t
+    | FalseBranch of Pvar.t * PrunePairs.t
+    | V of Pvar.t * PrunePairs.t * PrunePairs.t
+    | Top
+
+  let ( <= ) ~lhs ~rhs =
+    if phys_equal lhs rhs then true
+    else
+      match (lhs, rhs) with
+      | _, Top ->
+          true
+      | Top, _ ->
+          false
+      | Latest p1, Latest p2 ->
+          PrunePairs.equal p1 p2
+      | TrueBranch (x1, p1), TrueBranch (x2, p2)
+      | FalseBranch (x1, p1), FalseBranch (x2, p2)
+      | TrueBranch (x1, p1), V (x2, p2, _)
+      | FalseBranch (x1, p1), V (x2, _, p2) ->
+          Pvar.equal x1 x2 && PrunePairs.equal p1 p2
+      | V (x1, ptrue1, pfalse1), V (x2, ptrue2, pfalse2) ->
+          Pvar.equal x1 x2 && PrunePairs.equal ptrue1 ptrue2 && PrunePairs.equal pfalse1 pfalse2
+      | _, _ ->
+          false
+
+
+  let join x y =
+    match (x, y) with
+    | _, _ when ( <= ) ~lhs:x ~rhs:y ->
+        y
+    | _, _ when ( <= ) ~lhs:y ~rhs:x ->
+        x
+    | FalseBranch (x', pfalse), TrueBranch (y', ptrue)
+    | TrueBranch (x', ptrue), FalseBranch (y', pfalse)
+      when Pvar.equal x' y' ->
+        V (x', ptrue, pfalse)
+    | _, _ ->
+        Top
+
+
+  let widen ~prev ~next ~num_iters:_ = join prev next
+
+  let top = Top
+end
+
 module MemReach = struct
-  type astate = {stack: Stack.astate; heap: Heap.astate; alias: Alias.astate}
+  type astate =
+    {stack: Stack.astate; heap: Heap.astate; alias: Alias.astate; latest_prune: LatestPrune.astate}
 
   type t = astate
 
-  let bot : t = {stack= Stack.bot; heap= Heap.bot; alias= Alias.bot}
+  let init : t = {stack= Stack.bot; heap= Heap.bot; alias= Alias.bot; latest_prune= LatestPrune.top}
 
   let ( <= ) ~lhs ~rhs =
     if phys_equal lhs rhs then true
     else
       Stack.( <= ) ~lhs:lhs.stack ~rhs:rhs.stack && Heap.( <= ) ~lhs:lhs.heap ~rhs:rhs.heap
       && Alias.( <= ) ~lhs:lhs.alias ~rhs:rhs.alias
+      && LatestPrune.( <= ) ~lhs:lhs.latest_prune ~rhs:rhs.latest_prune
 
 
   let widen ~prev ~next ~num_iters =
@@ -513,14 +599,17 @@ module MemReach = struct
     else
       { stack= Stack.widen ~prev:prev.stack ~next:next.stack ~num_iters
       ; heap= Heap.widen ~prev:prev.heap ~next:next.heap ~num_iters
-      ; alias= Alias.widen ~prev:prev.alias ~next:next.alias ~num_iters }
+      ; alias= Alias.widen ~prev:prev.alias ~next:next.alias ~num_iters
+      ; latest_prune= LatestPrune.widen ~prev:prev.latest_prune ~next:next.latest_prune ~num_iters
+      }
 
 
   let join : t -> t -> t =
     fun x y ->
       { stack= Stack.join x.stack y.stack
       ; heap= Heap.join x.heap y.heap
-      ; alias= Alias.join x.alias y.alias }
+      ; alias= Alias.join x.alias y.alias
+      ; latest_prune= LatestPrune.join x.latest_prune y.latest_prune }
 
 
   let pp : F.formatter -> t -> unit =
@@ -617,6 +706,36 @@ module MemReach = struct
   let remove_temps : Ident.t list -> t -> t =
     fun temps m ->
       {m with stack= Stack.remove_temps temps m.stack; alias= Alias.remove_temps temps m.alias}
+
+
+  let set_prune_pairs : PrunePairs.t -> t -> t =
+    fun prune_pairs m -> {m with latest_prune= LatestPrune.Latest prune_pairs}
+
+
+  let apply_latest_prune : Exp.t -> t -> t =
+    fun e m ->
+      match (m.latest_prune, e) with
+      | LatestPrune.V (x, prunes, _), Exp.Var r
+      | LatestPrune.V (x, _, prunes), Exp.UnOp (Unop.LNot, Exp.Var r, _) -> (
+        match find_simple_alias r m with
+        | Some Loc.Var Var.ProgramVar y when Pvar.equal x y ->
+            List.fold_left prunes ~init:m ~f:(fun acc (l, v) ->
+                update_mem (PowLoc.singleton l) v acc )
+        | _ ->
+            m )
+      | _ ->
+          m
+
+
+  let update_latest_prune : Exp.t -> Exp.t -> t -> t =
+    fun 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}
+      | _, _, _ ->
+          {m with latest_prune= LatestPrune.Top}
 end
 
 module Mem = struct
@@ -626,7 +745,7 @@ module Mem = struct
 
   let bot : t = Bottom
 
-  let init : t = NonBottom MemReach.bot
+  let init : t = NonBottom MemReach.init
 
   let f_lift_default : 'a -> (MemReach.t -> 'a) -> t -> 'a =
     fun default f m -> match m with Bottom -> default | NonBottom m' -> f m'
@@ -706,6 +825,21 @@ module Mem = struct
 
 
   let remove_temps : Ident.t list -> t -> t = fun temps -> f_lift (MemReach.remove_temps temps)
+
+  let set_prune_pairs : PrunePairs.t -> t -> t =
+    fun prune_pairs -> f_lift (MemReach.set_prune_pairs prune_pairs)
+
+
+  let apply_latest_prune : Exp.t -> t -> t = fun e -> f_lift (MemReach.apply_latest_prune e)
+
+  let update_latest_prune : Exp.t -> Exp.t -> t -> t =
+    fun e1 e2 -> f_lift (MemReach.update_latest_prune e1 e2)
+
+
+  let update_mem_in_prune : PrunePairs.t ref -> Loc.t -> Val.t -> t -> t =
+    fun prune_pairs lv v m ->
+      prune_pairs := (lv, v) :: !prune_pairs ;
+      update_mem (PowLoc.singleton lv) v m
 end
 
 module Summary = struct

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -326,20 +326,20 @@ module Make (CFG : ProcCfg.S) = struct
       ArrayBlk.make allocsite offset size stride |> Val.of_array_blk
 
 
-  let prune_unop : Exp.t -> Mem.astate -> Mem.astate =
+  let prune_unop : PrunePairs.t ref -> Exp.t -> Mem.astate -> Mem.astate =
-    fun e mem ->
+    fun prune_pairs e mem ->
       match e with
       | Exp.Var x -> (
         match Mem.find_alias x mem with
         | Some AliasTarget.Simple lv ->
             let v = Mem.find_heap lv mem in
             let v' = Val.prune_zero v in
-            Mem.update_mem (PowLoc.singleton lv) v' mem
+            Mem.update_mem_in_prune prune_pairs lv v' mem
         | Some AliasTarget.Empty lv ->
             let v = Mem.find_heap lv mem in
             let itv_v = Itv.prune_eq (Val.get_itv v) Itv.zero in
             let v' = Val.modify_itv itv_v v in
-            Mem.update_mem (PowLoc.singleton lv) v' mem
+            Mem.update_mem_in_prune prune_pairs lv v' mem
         | None ->
             mem )
       | Exp.UnOp (Unop.LNot, Exp.Var x, _) -> (
@@ -348,20 +348,20 @@ module Make (CFG : ProcCfg.S) = struct
             let v = Mem.find_heap lv mem in
             let itv_v = Itv.prune_eq (Val.get_itv v) Itv.false_sem in
             let v' = Val.modify_itv itv_v v in
-            Mem.update_mem (PowLoc.singleton lv) v' mem
+            Mem.update_mem_in_prune prune_pairs lv v' mem
         | Some AliasTarget.Empty lv ->
             let v = Mem.find_heap lv mem in
             let itv_v = Itv.prune_comp Binop.Ge (Val.get_itv v) Itv.one in
             let v' = Val.modify_itv itv_v v in
-            Mem.update_mem (PowLoc.singleton lv) v' mem
+            Mem.update_mem_in_prune prune_pairs lv v' mem
         | None ->
             mem )
       | _ ->
           mem
 
 
-  let prune_binop_left : Exp.t -> Mem.astate -> Mem.astate =
+  let prune_binop_left : PrunePairs.t ref -> Exp.t -> Mem.astate -> Mem.astate =
-    fun e mem ->
+    fun prune_pairs e mem ->
       match e with
       | Exp.BinOp ((Binop.Lt as comp), Exp.Var x, e')
       | Exp.BinOp ((Binop.Gt as comp), Exp.Var x, e')
@@ -371,7 +371,7 @@ module Make (CFG : ProcCfg.S) = struct
         | Some lv ->
             let v = Mem.find_heap lv mem in
             let v' = Val.prune_comp comp v (eval e' mem) in
-            Mem.update_mem (PowLoc.singleton lv) v' mem
+            Mem.update_mem_in_prune prune_pairs lv v' mem
         | None ->
             mem )
       | Exp.BinOp (Binop.Eq, Exp.Var x, e') -> (
@@ -379,7 +379,7 @@ module Make (CFG : ProcCfg.S) = struct
         | Some lv ->
             let v = Mem.find_heap lv mem in
             let v' = Val.prune_eq v (eval e' mem) in
-            Mem.update_mem (PowLoc.singleton lv) v' mem
+            Mem.update_mem_in_prune prune_pairs lv v' mem
         | None ->
             mem )
       | Exp.BinOp (Binop.Ne, Exp.Var x, e') -> (
@@ -387,15 +387,15 @@ module Make (CFG : ProcCfg.S) = struct
         | Some lv ->
             let v = Mem.find_heap lv mem in
             let v' = Val.prune_ne v (eval e' mem) in
-            Mem.update_mem (PowLoc.singleton lv) v' mem
+            Mem.update_mem_in_prune prune_pairs lv v' mem
         | None ->
             mem )
       | _ ->
           mem
 
 
-  let prune_binop_right : Exp.t -> Mem.astate -> Mem.astate =
+  let prune_binop_right : PrunePairs.t ref -> Exp.t -> Mem.astate -> Mem.astate =
-    fun e mem ->
+    fun prune_pairs e mem ->
       match e with
       | Exp.BinOp ((Binop.Lt as c), e', Exp.Var x)
       | Exp.BinOp ((Binop.Gt as c), e', Exp.Var x)
@@ -403,7 +403,7 @@ module Make (CFG : ProcCfg.S) = struct
       | Exp.BinOp ((Binop.Ge as c), e', Exp.Var x)
       | Exp.BinOp ((Binop.Eq as c), e', Exp.Var x)
       | Exp.BinOp ((Binop.Ne as c), e', Exp.Var x) ->
-          prune_binop_left (Exp.BinOp (comp_rev c, Exp.Var x, e')) mem
+          prune_binop_left prune_pairs (Exp.BinOp (comp_rev c, Exp.Var x, e')) mem
       | _ ->
           mem
 
@@ -416,31 +416,39 @@ module Make (CFG : ProcCfg.S) = struct
     fun e mem -> if is_unreachable_constant e mem then Mem.bot else mem
 
 
-  let rec prune : Exp.t -> Mem.astate -> Mem.astate =
+  let prune : Exp.t -> Mem.astate -> Mem.astate =
     fun e mem ->
-      let mem =
+      let prune_pairs = ref PrunePairs.empty in
-        mem |> prune_unreachable e |> prune_unop e |> prune_binop_left e |> prune_binop_right e
+      let rec prune_helper e mem =
+        let mem =
+          mem |> prune_unreachable e |> prune_unop prune_pairs e |> prune_binop_left prune_pairs e
+          |> prune_binop_right prune_pairs e
+        in
+        match e with
+        | Exp.BinOp (Binop.Ne, e, Exp.Const Const.Cint i) when IntLit.iszero i ->
+            prune_helper e mem
+        | Exp.BinOp (Binop.Eq, e, Exp.Const Const.Cint i) when IntLit.iszero i ->
+            prune_helper (Exp.UnOp (Unop.LNot, e, None)) mem
+        | Exp.UnOp (Unop.Neg, Exp.Var x, _) ->
+            prune_helper (Exp.Var x) mem
+        | Exp.BinOp (Binop.LAnd, e1, e2) ->
+            mem |> prune_helper e1 |> prune_helper e2
+        | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) ->
+            mem |> prune_helper (Exp.UnOp (Unop.LNot, e1, t))
+            |> prune_helper (Exp.UnOp (Unop.LNot, e2, t))
+        | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Lt as c), e1, e2), _)
+        | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Gt as c), e1, e2), _)
+        | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Le as c), e1, e2), _)
+        | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ge as c), e1, e2), _)
+        | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Eq as c), e1, e2), _)
+        | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ne as c), e1, e2), _) ->
+            prune_helper (Exp.BinOp (comp_not c, e1, e2)) mem
+        | _ ->
+            mem
       in
-      match e with
+      let mem = Mem.apply_latest_prune e mem in
-      | Exp.BinOp (Binop.Ne, e, Exp.Const Const.Cint i) when IntLit.iszero i ->
+      let mem = prune_helper e mem in
-          prune e mem
+      Mem.set_prune_pairs !prune_pairs mem
-      | Exp.BinOp (Binop.Eq, e, Exp.Const Const.Cint i) when IntLit.iszero i ->
-          prune (Exp.UnOp (Unop.LNot, e, None)) mem
-      | Exp.UnOp (Unop.Neg, Exp.Var x, _) ->
-          prune (Exp.Var x) mem
-      | Exp.BinOp (Binop.LAnd, e1, e2) ->
-          mem |> prune e1 |> prune e2
-      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) ->
-          mem |> prune (Exp.UnOp (Unop.LNot, e1, t)) |> prune (Exp.UnOp (Unop.LNot, e2, t))
-      | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Lt as c), e1, e2), _)
-      | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Gt as c), e1, e2), _)
-      | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Le as c), e1, e2), _)
-      | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ge as c), e1, e2), _)
-      | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Eq as c), e1, e2), _)
-      | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ne as c), e1, e2), _) ->
-          prune (Exp.BinOp (comp_not c, e1, e2)) mem
-      | _ ->
-          mem
 
 
   let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list =

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

@@ -17,6 +17,8 @@ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [42, 42] Size: [42, 42]]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [42, 42] Size: [42, 42]]
 codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [6, 6] Size: [5, 5]]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [4, 4] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L1, [Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [10, 10] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_L5, [Call,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_L3, [Call,Call,Call,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [0, +oo]]

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

@@ -8,6 +8,7 @@
  */
 #include <vector>
 #include <list>
+#include <assert.h>
 
 void out_of_bound_Bad(std::vector<int> v) {
   unsigned int n = v.size();
@@ -156,3 +157,30 @@ void data_Bad() {
   p[4] = 10;
   p[v[4]] = 1;
 }
+
+void assert_Good() {
+  std::vector<int> v;
+  for (int i = 0; i < 5; i++) {
+    v.push_back(1);
+  }
+  assert(v.size() == 5);
+  v[4] = 1;
+}
+
+void assert_Good_FP(int x) {
+  std::vector<int> v;
+  for (int i = 0; i < 5; i++) {
+    v.push_back(1);
+  }
+  assert(((v.size() == 5) ? 1 : 0) ? 1 : 0);
+  v[4] = 1;
+}
+
+void assert_Bad() {
+  std::vector<int> v;
+  for (int i = 0; i < 5; i++) {
+    v.push_back(1);
+  }
+  assert(v.size() == 5);
+  v[6] = 1;
+}