[inferbo] eval_locs

Summary:
`eval_locs` is like `eval |> get_all_locs` but avoids computing things that aren't necessary.

The goal was not to be an optimization but is needed for Java where array blocks don't have offsets.

Reviewed By: skcho

Differential Revision: D13190939

fbshipit-source-id: 1cc0e6338

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -219,11 +219,10 @@ module TransferFunctions = struct
     |> copy_reachable_new_locs_from (Dom.Val.get_all_locs ret_val)
 
 
-  let instantiate_param tenv integer_type_widths pdesc params callee_exit_mem eval_sym_trace
-      location mem =
+  let instantiate_param tenv pdesc params callee_exit_mem eval_sym_trace location mem =
     let formals = Dom.get_formals pdesc in
-    let actuals = List.map ~f:(fun (a, _) -> Sem.eval integer_type_widths a mem) params in
-    let f mem formal actual =
+    let actuals_locs = List.map ~f:(fun (a, _) -> Sem.eval_locs a mem) params in
+    let f mem formal actual_locs =
       match (snd formal).Typ.desc with
       | Typ.Tptr (typ, _) -> (
         match typ.Typ.desc with
@@ -237,7 +236,7 @@ module TransferFunctions = struct
               let instantiate_fld mem (fn, _, _) =
                 let formal_fields = PowLoc.append_field formal_locs ~fn in
                 let v = Dom.Mem.find_set formal_fields callee_exit_mem in
-                let actual_fields = PowLoc.append_field (Dom.Val.get_all_locs actual) ~fn in
+                let actual_fields = PowLoc.append_field actual_locs ~fn in
                 Dom.Val.subst v eval_sym_trace location
                 |> Fn.flip (Dom.Mem.strong_update actual_fields) mem
               in
@@ -250,13 +249,12 @@ module TransferFunctions = struct
               |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc
             in
             let v = Dom.Mem.find_set formal_locs callee_exit_mem in
-            let actual_locs = Dom.Val.get_all_locs actual in
             Dom.Val.subst v eval_sym_trace location
             |> Fn.flip (Dom.Mem.strong_update actual_locs) mem )
       | _ ->
           mem
     in
-    try List.fold2_exn formals actuals ~init:mem ~f with Invalid_argument _ -> mem
+    try List.fold2_exn formals actuals_locs ~init:mem ~f with Invalid_argument _ -> mem
 
 
   let forget_ret_relation ret callee_pname mem =
@@ -294,8 +292,7 @@ module TransferFunctions = struct
     in
     let caller_mem =
       instantiate_ret ret callee_pname ~callee_exit_mem eval_sym_trace caller_mem location
-      |> instantiate_param tenv integer_type_widths callee_pdesc params callee_exit_mem
-           eval_sym_trace location
+      |> instantiate_param tenv callee_pdesc params callee_exit_mem eval_sym_trace location
       |> forget_ret_relation ret callee_pname
     in
     Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem
@@ -329,9 +326,9 @@ module TransferFunctions = struct
             (Pvar.pp Pp.text) pvar ;
           Dom.Mem.add_unknown id ~location mem )
     | Load (id, exp, _, _) ->
-        BoUtils.Exec.load_val id (Sem.eval integer_type_widths exp mem) mem
+        BoUtils.Exec.load_locs id (Sem.eval_locs exp mem) mem
     | Store (exp1, _, exp2, location) ->
-        let locs = Sem.eval integer_type_widths exp1 mem |> Dom.Val.get_all_locs in
+        let locs = Sem.eval_locs exp1 mem in
         let v = Sem.eval integer_type_widths exp2 mem |> Dom.Val.add_assign_trace_elem location in
         let mem =
           let sym_exps =

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -268,15 +268,11 @@ let set_array_length array length_exp =
 
 
 module Split = struct
-  let std_vector integer_type_widths ~adds_at_least_one (vector_exp, vector_typ) location mem =
+  let std_vector ~adds_at_least_one (vector_exp, vector_typ) location mem =
     let increment = if adds_at_least_one then Dom.Val.Itv.pos else Dom.Val.Itv.nat in
     let vector_type_name = Option.value_exn (vector_typ |> Typ.strip_ptr |> Typ.name) in
     let size_field = Typ.Fieldname.Clang.from_class_name vector_type_name "infer_size" in
-    let vector_size_locs =
-      Sem.eval integer_type_widths vector_exp mem
-      |> Dom.Val.get_all_locs
-      |> PowLoc.append_field ~fn:size_field
-    in
+    let vector_size_locs = Sem.eval_locs vector_exp mem |> PowLoc.append_field ~fn:size_field in
     let f_trace _ traces = Trace.(Set.add_elem location Through) traces in
     Dom.Mem.transform_mem ~f:(Dom.Val.plus_a ~f_trace increment) vector_size_locs mem
 end
@@ -284,8 +280,8 @@ end
 module Boost = struct
   module Split = struct
     let std_vector vector_arg =
-      let exec {location; integer_type_widths} ~ret:_ mem =
-        Split.std_vector integer_type_widths ~adds_at_least_one:true vector_arg location mem
+      let exec {location} ~ret:_ mem =
+        Split.std_vector ~adds_at_least_one:true vector_arg location mem
       in
       {exec; check= no_check}
   end
@@ -303,7 +299,7 @@ module Folly = struct
               (* default: ignore_empty is false *)
               true
         in
-        Split.std_vector integer_type_widths ~adds_at_least_one vector_arg location mem
+        Split.std_vector ~adds_at_least_one vector_arg location mem
       in
       {exec; check= no_check}
   end

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -266,6 +266,31 @@ and eval_binop : Typ.IntegerWidths.t -> Binop.t -> Exp.t -> Exp.t -> Mem.t -> Va
       Val.lor_sem v1 v2
 
 
+(**
+  [eval_locs exp mem] is like [eval_locs exp mem |> Val.get_all_locs]
+  but takes some shortcuts to avoid computing useless and/or problematic intermediate values
+*)
+let rec eval_locs : Exp.t -> Mem.t -> PowLoc.t =
+ fun exp mem ->
+  match exp with
+  | Var id ->
+      Mem.find_stack (Var.of_id id |> Loc.of_var) mem |> Val.get_all_locs
+  | Lvar pvar ->
+      let loc = Loc.of_pvar pvar in
+      if Mem.is_stack_loc loc mem then Mem.find loc mem |> Val.get_all_locs
+      else PowLoc.singleton loc
+  | BinOp ((Binop.MinusPI | Binop.PlusPI), e, _) | Cast (_, e) ->
+      eval_locs e mem
+  | BinOp _ | Closure _ | Const _ | Exn _ | Sizeof _ | UnOp _ ->
+      PowLoc.empty
+  | Lfield (e, fn, _) ->
+      eval_locs e mem |> PowLoc.append_field ~fn
+  | Lindex (((Lfield _ | Lindex _) as e), _) ->
+      Mem.find_set (eval_locs e mem) mem |> Val.get_all_locs
+  | Lindex (e, _) ->
+      eval_locs e mem
+
+
 (* It returns the array value of the input expression.  For example,
    when "x" is a program variable, (eval_arr "x") returns array blocks
    the "x" is pointing to, on the other hand, (eval "x") returns the
@@ -287,10 +312,10 @@ let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t =
       let v = eval_arr integer_type_widths e mem in
       set_array_stride integer_type_widths t v
   | Exp.Lfield (e, fn, _) ->
-      let locs = eval integer_type_widths e mem |> Val.get_all_locs |> PowLoc.append_field ~fn in
+      let locs = eval_locs e mem |> PowLoc.append_field ~fn in
       Mem.find_set locs mem
   | Exp.Lindex (e, _) ->
-      let locs = eval integer_type_widths e mem |> Val.get_all_locs in
+      let locs = eval_locs e mem in
       Mem.find_set locs mem
   | Exp.Const _ | Exp.UnOp _ | Exp.Sizeof _ | Exp.Exn _ | Exp.Closure _ ->
       Val.bot

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -22,8 +22,7 @@ module Exec = struct
     Dom.Mem.find_set size_powloc mem
 
 
-  let load_val id val_ mem =
-    let locs = val_ |> Dom.Val.get_all_locs in
+  let load_locs id locs mem =
     let v = Dom.Mem.find_set locs mem in
     let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in
     if not v.represents_multiple_values then
@@ -35,6 +34,8 @@ module Exec = struct
     else mem
 
 
+  let load_val id v mem = load_locs id (Dom.Val.get_all_locs v) mem
+
   type decl_local =
        Typ.Procname.t
     -> node_hash:int

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -14,6 +14,8 @@ module PO = BufferOverrunProofObligations
 module Exec : sig
   val get_alist_size : Dom.Val.t -> Dom.Mem.t -> Dom.Val.t
 
+  val load_locs : Ident.t -> PowLoc.t -> Dom.Mem.t -> Dom.Mem.t
+
   val load_val : Ident.t -> Dom.Val.t -> Dom.Mem.t -> Dom.Mem.t
 
   type decl_local =

infer/tests/codetoanalyze/c/bufferoverrun/global.c

@@ -39,3 +39,17 @@ void use_global_const_ten_Bad() {
   char arr[5];
   arr[global_const_ten] = 0;
 }
+
+static const char global_arr[] = {1, 0, 1};
+
+static void copyfilter_Good_FP(const char* s, const char* z, int b) {
+  int i;
+  int n = strlen(s);
+  for (i = 0; z[i]; i++) { // We need to infer that z[i] means i < strlen(z)
+    if (global_arr[z[i]] || // We need a weak update here
+        (z[i] == s[0] && (n == 1 || memcmp(z, s, n) == 0))) {
+      i = 0;
+      break;
+    }
+  }
+}

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

@@ -89,6 +89,8 @@ codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 4, BUFFER_OV
 codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
+codetoanalyze/c/bufferoverrun/global.c, copyfilter_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
+codetoanalyze/c/bufferoverrun/global.c, copyfilter_Good_FP, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/global.c, use_global_const_ten_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]