[inferbo] Revise eval_locs for array blocks

Summary:
It renames `eval_locs` to `eval_arr` and we use it for getting array block values the given input expressions are pointing to.  For example, when given a program variable `x` as an input, `eval_arr` returns array blocks that `x` is pointing to, on the other hand, `eval` returns an abstract location of `x`.

Depends on D7471891

Reviewed By: mbouaziz

Differential Revision: D7471915

fbshipit-source-id: b994944

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -157,11 +157,9 @@ let inferbo_min e1 e2 =
 
 let inferbo_set_size e1 e2 =
   let exec _model_env mem =
-    let locs = Sem.eval_locs e1 mem |> Dom.Val.get_pow_loc in
+    let locs = Sem.eval e1 mem |> Dom.Val.get_pow_loc in
     let size = Sem.eval e2 mem |> Dom.Val.get_itv in
-    let arr = Dom.Mem.find_heap_set locs mem in
+    Dom.Mem.transform_mem ~f:(Dom.Val.set_array_size size) locs mem
-    let arr = Dom.Val.set_array_size size arr in
-    Dom.Mem.strong_update_heap locs arr mem
   and check = check_alloc_size e2 in
   {exec; check}
 

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -290,23 +290,28 @@ and eval_binop : Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Val.t =
       Val.lor_sem v1 v2
 
 
-let rec eval_locs : Exp.t -> Mem.astate -> Val.t =
+(* 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
+   abstract location of "x". *)
+let rec eval_arr : Exp.t -> Mem.astate -> Val.t =
  fun exp mem ->
   match exp with
   | Exp.Var id -> (
     match Mem.find_alias id mem with
     | Some AliasTarget.Simple loc ->
-        PowLoc.singleton loc |> Val.of_pow_loc
+        Mem.find_heap loc mem
     | Some AliasTarget.Empty _ | None ->
         Val.bot )
   | Exp.Lvar pvar ->
-      pvar |> Loc.of_pvar |> PowLoc.singleton |> Val.of_pow_loc
+      Mem.find_set (PowLoc.singleton (Loc.of_pvar pvar)) mem
   | Exp.BinOp (bop, e1, e2) ->
       eval_binop bop e1 e2 mem
   | Exp.Cast (_, e) ->
-      eval_locs e mem
+      eval_arr e mem
   | Exp.Lfield (e, fn, _) ->
-      eval e mem |> Val.get_all_locs |> PowLoc.append_field ~fn |> Val.of_pow_loc
+      let locs = eval e mem |> Val.get_all_locs |> PowLoc.append_field ~fn in
+      Mem.find_heap_set locs mem
   | Exp.Lindex (e1, e2) ->
       let arr = eval e1 mem in
       let idx = eval e2 mem in

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -159,8 +159,7 @@ module Check = struct
 
 
   let lindex ~array_exp ~index_exp mem pname location cond_set =
-    let locs = Sem.eval_locs array_exp mem |> Dom.Val.get_all_locs in
+    let arr = Sem.eval_arr array_exp mem in
-    let arr = Dom.Mem.find_set locs mem in
     let idx = Sem.eval index_exp mem in
     array_access ~arr ~idx ~is_plus:true pname location cond_set
 end

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

@@ -59,6 +59,8 @@ codetoanalyze/c/bufferoverrun/models.c, fgetc_m1_bad, 3, BUFFER_OVERRUN_L3, ERRO
 codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L4, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
+codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith3_Bad, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Call,Parameter: p,Parameter: x,ArrayAccess: Offset: [10, 10] Size: [5, 5] @ codetoanalyze/c/bufferoverrun/pointer_arith.c:33:3 by call to `pointer_arith3()` ]
+codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith4_Bad, 0, BUFFER_OVERRUN_L1, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: [10, 10] Size: [5, 5] @ codetoanalyze/c/bufferoverrun/pointer_arith.c:48:3 by call to `FN_pointer_arith4_Bad()` ]
 codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_arrblk_eq_Ok, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: x,ArrayAccess: Offset: [15, 5] Size: [5, 5] @ codetoanalyze/c/bufferoverrun/prune_alias.c:135:5 by call to `prune_arrblk_eq()` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [1, 1]]

infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c

@@ -19,3 +19,33 @@ void array_pointer_arith_Bad() {
   int* p = &arr[5];
   p[5] = 1;
 }
+
+void pointer_arith2_Ok(int x) {
+  int len = 5;
+  char p[5];
+  (p + x)[3 - x] = 0;
+}
+
+void call_pointer_arith2_Ok() { pointer_arith2_Ok(100); }
+
+void pointer_arith3(char* p, int x) {
+  int len = 5;
+  (p + x)[10 - x] = 0;
+}
+
+void call_pointer_arith3_Bad() {
+  char p[5];
+  pointer_arith3(p, 100);
+}
+
+/* It is better to raise an alarm here, rather than returning a safety
+   condition, since the buffer overrun occurs always without regard to
+   the input x.  Using symbols for variables, not only for bounds,
+   would help in this case. */
+void FN_pointer_arith4_Bad(int x) {
+  int len = 5;
+  char p[5];
+  (p + x)[10 - x] = 0;
+}
+
+void call_pointer_arith4_Bad() { FN_pointer_arith4_Bad(100); }