[inferbo] Propagate LatestPrune on function calls

Summary:
This diff propagates LatestPrune on function calls.

Depends on D14321605

Reviewed By: mbouaziz

Differential Revision: D14321618

fbshipit-source-id: cb2e1b547

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -59,6 +59,19 @@ module TransferFunctions = struct
 
   type nonrec extras = extras
 
+  let instantiate_latest_prune ~ret_id ~callee_exit_mem eval_sym_trace location mem =
+    match
+      Dom.Mem.get_latest_prune callee_exit_mem
+      |> Dom.LatestPrune.subst ~ret_id eval_sym_trace location
+    with
+    | Ok latest_prune' ->
+        Dom.Mem.set_latest_prune latest_prune' mem
+    | Error `SubstBottom ->
+        Dom.Mem.bottom
+    | Error `SubstFail ->
+        mem
+
+
   let instantiate_mem_reachable (ret_id, _) callee_formals callee_pname ~callee_exit_mem
       ({Dom.eval_locpath} as eval_sym_trace) mem location =
     let formal_locs =
@@ -104,6 +117,7 @@ module TransferFunctions = struct
     Dom.Mem.add_stack ret_var (Dom.Val.subst ret_val eval_sym_trace location) mem
     |> instantiate_ret_alias
     |> copy_reachable_locs_from (PowLoc.join formal_locs (Dom.Val.get_all_locs ret_val))
+    |> instantiate_latest_prune ~ret_id ~callee_exit_mem eval_sym_trace location
 
 
   let forget_ret_relation ret callee_pname mem =

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -980,6 +980,22 @@ module PrunePairs = struct
 
   let forget locs x = filter (fun l _ -> not (PowLoc.mem l locs)) x
 
+  let subst x ({eval_locpath} as eval_sym_trace) location =
+    let open Result.Monad_infix in
+    let subst1 l pruned_val acc =
+      acc
+      >>= fun acc ->
+      match PowLoc.is_singleton_or_more (PowLoc.subst_loc l eval_locpath) with
+      | Singleton loc ->
+          Ok (add loc (PrunedVal.subst pruned_val eval_sym_trace location) acc)
+      | Empty ->
+          Error `SubstBottom
+      | More ->
+          Error `SubstFail
+    in
+    fold subst1 x (Ok empty)
+
+
   let is_reachable x = not (exists (fun _ v -> PrunedVal.is_empty v) x)
 end
 
@@ -999,12 +1015,16 @@ module LatestPrune = struct
      respectively.  There is no other memory updates after the latest
      prunings.
 
+     VRet (x, ptrue, pfalse): Similar to V, but this is for return
+     values of functions.
+
      Top: No information about the latest pruning. *)
   type t =
     | Latest of PrunePairs.t
     | TrueBranch of Pvar.t * PrunePairs.t
     | FalseBranch of Pvar.t * PrunePairs.t
     | V of Pvar.t * PrunePairs.t * PrunePairs.t
+    | VRet of Ident.t * PrunePairs.t * PrunePairs.t
     | Top
 
   let pvar_pp = Pvar.pp Pp.text
@@ -1020,6 +1040,8 @@ module LatestPrune = struct
         F.fprintf fmt "LatestPrune: false(%a) %a" pvar_pp v PrunePairs.pp p
     | V (v, p1, p2) ->
         F.fprintf fmt "LatestPrune: v(%a) %a / %a" pvar_pp v PrunePairs.pp p1 PrunePairs.pp p2
+    | VRet (v, p1, p2) ->
+        F.fprintf fmt "LatestPrune: ret(%a) %a / %a" Ident.pp v PrunePairs.pp p1 PrunePairs.pp p2
 
 
   let ( <= ) ~lhs ~rhs =
@@ -1041,6 +1063,10 @@ module LatestPrune = struct
           Pvar.equal x1 x2
           && PrunePairs.( <= ) ~lhs:ptrue1 ~rhs:ptrue2
           && PrunePairs.( <= ) ~lhs:pfalse1 ~rhs:pfalse2
+      | VRet (x1, ptrue1, pfalse1), VRet (x2, ptrue2, pfalse2) ->
+          Ident.equal x1 x2
+          && PrunePairs.( <= ) ~lhs:ptrue1 ~rhs:ptrue2
+          && PrunePairs.( <= ) ~lhs:pfalse1 ~rhs:pfalse2
       | _, _ ->
           false
 
@@ -1071,6 +1097,8 @@ module LatestPrune = struct
         V (x1, ptrue, PrunePairs.join pfalse1 pfalse2)
     | V (x1, ptrue1, pfalse1), V (x2, ptrue2, pfalse2) when Pvar.equal x1 x2 ->
         V (x1, PrunePairs.join ptrue1 ptrue2, PrunePairs.join pfalse1 pfalse2)
+    | VRet (x1, ptrue1, pfalse1), VRet (x2, ptrue2, pfalse2) when Ident.equal x1 x2 ->
+        VRet (x1, PrunePairs.join ptrue1 ptrue2, PrunePairs.join pfalse1 pfalse2)
     | _, _ ->
         Top
 
@@ -1091,6 +1119,8 @@ module LatestPrune = struct
     | V (x, ptrue, pfalse) ->
         if is_mem_locs x then Top
         else V (x, PrunePairs.forget locs ptrue, PrunePairs.forget locs pfalse)
+    | VRet (x, ptrue, pfalse) ->
+        VRet (x, PrunePairs.forget locs ptrue, PrunePairs.forget locs pfalse)
     | Top ->
         Top
 
@@ -1105,6 +1135,41 @@ module LatestPrune = struct
         V (to_, ptrue, pfalse)
     | _ ->
         x
+
+
+  let subst ~ret_id ({eval_locpath} as eval_sym_trace) location =
+    let open Result.Monad_infix in
+    let subst_pvar x =
+      match PowLoc.is_singleton_or_more (PowLoc.subst_loc (Loc.of_pvar x) eval_locpath) with
+      | Empty ->
+          Error `SubstBottom
+      | Singleton (Loc.Var (Var.ProgramVar x')) ->
+          Ok x'
+      | Singleton _ | More ->
+          Error `SubstFail
+    in
+    function
+    | Latest p ->
+        PrunePairs.subst p eval_sym_trace location >>| fun p' -> Latest p'
+    | TrueBranch (x, p) ->
+        subst_pvar x
+        >>= fun x' -> PrunePairs.subst p eval_sym_trace location >>| fun p' -> TrueBranch (x', p')
+    | FalseBranch (x, p) ->
+        subst_pvar x
+        >>= fun x' -> PrunePairs.subst p eval_sym_trace location >>| fun p' -> FalseBranch (x', p')
+    | V (x, ptrue, pfalse) when Pvar.is_return x ->
+        PrunePairs.subst ptrue eval_sym_trace location
+        >>= fun ptrue' ->
+        PrunePairs.subst pfalse eval_sym_trace location
+        >>| fun pfalse' -> VRet (ret_id, ptrue', pfalse')
+    | V (x, ptrue, pfalse) ->
+        subst_pvar x
+        >>= fun x' ->
+        PrunePairs.subst ptrue eval_sym_trace location
+        >>= fun ptrue' ->
+        PrunePairs.subst pfalse eval_sym_trace location >>| fun pfalse' -> V (x', ptrue', pfalse')
+    | VRet _ | Top ->
+        Ok Top
 end
 
 module Reachability = struct
@@ -1125,7 +1190,7 @@ module Reachability = struct
     match latest_prune with
     | LatestPrune.Latest p | LatestPrune.TrueBranch (_, p) | LatestPrune.FalseBranch (_, p) ->
         of_prune_pairs p
-    | LatestPrune.V (_, ptrue, pfalse) ->
+    | LatestPrune.V (_, ptrue, pfalse) | LatestPrune.VRet (_, ptrue, pfalse) ->
         M.inter (of_prune_pairs ptrue) (of_prune_pairs pfalse)
     | LatestPrune.Top ->
         M.empty
@@ -1366,6 +1431,10 @@ module MemReach = struct
             (PrunePairs.fold apply1 prunes m, prunes)
         | _ ->
             (m, PrunePairs.empty) )
+      | LatestPrune.VRet (x, prunes, _), Exp.Var r
+      | LatestPrune.VRet (x, _, prunes), Exp.UnOp (Unop.LNot, Exp.Var r, _) ->
+          if Ident.equal x r then (PrunePairs.fold apply1 prunes m, prunes)
+          else (m, PrunePairs.empty)
       | _ ->
           (m, PrunePairs.empty)
 
@@ -1387,7 +1456,9 @@ module MemReach = struct
         {m with latest_prune= LatestPrune.forget updated_locs m.latest_prune}
 
 
-  let get_latest_prune : t -> LatestPrune.t = fun {latest_prune} -> latest_prune
+  let get_latest_prune : _ t0 -> LatestPrune.t = fun {latest_prune} -> latest_prune
+
+  let set_latest_prune : LatestPrune.t -> t -> t = fun latest_prune x -> {x with latest_prune}
 
   let get_reachable_locs_from : (Pvar.t * Typ.t) list -> PowLoc.t -> _ t0 -> PowLoc.t =
     let add_reachable1 ~root loc v acc =
@@ -1589,10 +1660,14 @@ module Mem = struct
    fun ~updated_locs e1 e2 -> map ~f:(MemReach.update_latest_prune ~updated_locs e1 e2)
 
 
-  let get_latest_prune : t -> LatestPrune.t =
+  let get_latest_prune : _ t0 -> LatestPrune.t =
    fun m -> f_lift_default ~default:LatestPrune.Top MemReach.get_latest_prune m
 
 
+  let set_latest_prune : LatestPrune.t -> t -> t =
+   fun latest_prune m -> map ~f:(MemReach.set_latest_prune latest_prune) m
+
+
   let get_relation : t -> Relation.t =
    fun m -> f_lift_default ~default:Relation.bot MemReach.get_relation m
 

infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c

@@ -59,7 +59,7 @@ void l1_symbolic_widened_Bad(int n) {
   }
 }
 
-void l1_symbolic_widened_Good_FP(int n) {
+void l1_symbolic_widened_Good(int n) {
   int a[n];
   for (int i = n; less_than(i, n); i++) {
     a[i] = 0;

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

@@ -161,7 +161,7 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun2_Bad, 2, BUFFER
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `i`,<Length trace>,Array declaration,Array access: Offset: [max(10, i), i] Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_underrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `i`,<Length trace>,Array declaration,Array access: Offset: [i, min(-1, i)] Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_widened_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Parameter `n`,Array declaration,Array access: Offset: [n, +oo] Size: n]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Parameter `n`,Array declaration,Array access: Offset: [n, +oo] Size: n]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_widened_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: unknown_function,Binary operation: ([-oo, +oo] × 10):signed32]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Unknown value from: unknown_function,Assignment,<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_overrun_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 10] Size: 10]
@@ -270,7 +270,7 @@ codetoanalyze/c/bufferoverrun/prune_alias.c, unknown_alias_Bad, 6, BUFFER_OVERRU
 codetoanalyze/c/bufferoverrun/prune_alias.c, unknown_alias_Good, 4, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: unknown1,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_200_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Call,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-28, 16] Size: 17]
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_sym_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Call,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-28, 16] Size: 17]
-codetoanalyze/c/bufferoverrun/prune_constant.c, call_greater_than_Good_FP, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: (0 - 1):unsigned32]
+codetoanalyze/c/bufferoverrun/prune_constant.c, call_greater_than_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_null_pruning_symbols_3_Good_FP, 7, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Assignment,Call,<Offset trace>,Parameter `a`,Assignment,<Length trace>,Parameter `a`,Assignment,Array declaration,Array access: Offset: [-1, 9] Size: [0, 10] by call to `null_pruning_symbols` ]
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_null_pruning_symbols_3_Good_FP, 7, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Assignment,Call,<LHS trace>,Parameter `a`,Assignment,Binary operation: ([0, 10] - 1):unsigned32 by call to `null_pruning_symbols` ]
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_prune_add2_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 10 Size: 10 by call to `prune_add2` ]

infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c

@@ -167,7 +167,7 @@ void null_pruning2_Bad(int* p) {
 
 int greater_than(unsigned int x, unsigned int y) { return (x > y); }
 
-void call_greater_than_Good_FP() {
+void call_greater_than_Good() {
   unsigned int idx = 0;
   if (greater_than(idx, 0)) {
     idx = idx - 1;