[inferbo] Avoid pruning on array elements

Summary: This diff tries to do weak update for the abstract locations by pointer arithmetic, e.g. `p[n]` or `p+n`, even if the type of `p` is declared as a simple pointer, not an array.

Reviewed By: ezgicicek

Differential Revision: D16458367

fbshipit-source-id: 3b4cdd7e4

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -161,6 +161,15 @@ module TransferFunctions = struct
     Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem
 
 
+  let rec is_array_access_exp = function
+    | Exp.BinOp ((PlusPI | MinusPI), _, _) | Exp.Lindex _ ->
+        true
+    | Exp.Cast (_, x) ->
+        is_array_access_exp x
+    | _ ->
+        false
+
+
   let exec_instr : Dom.Mem.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.t =
    fun mem {summary; tenv; extras= {get_proc_summary_and_formals; oenv= {integer_type_widths}}}
        node instr ->
@@ -184,7 +193,8 @@ module TransferFunctions = struct
             (Pvar.pp Pp.text) pvar ;
           Dom.Mem.add_unknown id ~location mem )
     | Load (id, exp, typ, _) ->
-        BoUtils.Exec.load_locs id typ (Sem.eval_locs exp mem) mem
+        let represents_multiple_values = is_array_access_exp exp in
+        BoUtils.Exec.load_locs ~represents_multiple_values id typ (Sem.eval_locs exp mem) mem
     | Store (exp1, _, Const (Const.Cstr s), location) ->
         let locs = Sem.eval_locs exp1 mem in
         let model_env =

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -580,6 +580,8 @@ module MVal = struct
     (Loc.represents_multiple_values l, Val.on_demand ~default ?typ oenv l)
 
 
+  let get_rep_multi (represents_multiple_values, _) = represents_multiple_values
+
   let get_val (_, v) = v
 end
 
@@ -637,6 +639,8 @@ module MemPure = struct
         prev next
 
 
+  let is_rep_multi_loc l m = Option.value_map ~default:false (find_opt l m) ~f:MVal.get_rep_multi
+
   let find_opt l m = Option.map (find_opt l m) ~f:MVal.get_val
 
   let add ?(represents_multiple_values = false) l v m =
@@ -685,10 +689,9 @@ module AliasTarget = struct
 
   let nullity l = Nullity l
 
-  let use l = function
-    | Simple l' | SimplePlusA (l', _) | Empty l' | Fgets l' | Nullity l' ->
-        Loc.equal l l'
+  let get_loc = function Simple l | SimplePlusA (l, _) | Empty l | Fgets l | Nullity l -> l
 
+  let use l x = Loc.equal l (get_loc x)
 
   let loc_map x ~f =
     match x with
@@ -713,9 +716,7 @@ module AliasTarget = struct
 
   let widen ~prev ~next ~num_iters:_ = join prev next
 
-  let is_unknown = function
-    | Simple l | SimplePlusA (l, _) | Empty l | Fgets l | Nullity l ->
-        Loc.is_unknown l
+  let is_unknown x = Loc.is_unknown (get_loc x)
 end
 
 (* Relations between values of logical variables(registers) and program variables
@@ -1292,6 +1293,8 @@ module MemReach = struct
 
   let is_stack_loc : Loc.t -> _ t0 -> bool = fun l m -> StackLocs.mem l m.stack_locs
 
+  let is_rep_multi_loc : Loc.t -> _ t0 -> bool = fun l m -> MemPure.is_rep_multi_loc l m.mem_pure
+
   let find_opt : Loc.t -> _ t0 -> Val.t option = fun l m -> MemPure.find_opt l m.mem_pure
 
   let find_stack : Loc.t -> _ t0 -> Val.t = fun l m -> Option.value (find_opt l m) ~default:Val.bot
@@ -1375,6 +1378,11 @@ module MemReach = struct
     {m with mem_pure= MemPure.add ?represents_multiple_values x v m.mem_pure}
 
 
+  let add_heap_set : ?represents_multiple_values:bool -> PowLoc.t -> Val.t -> t -> t =
+   fun ?represents_multiple_values locs v m ->
+    PowLoc.fold (fun l acc -> add_heap ?represents_multiple_values l v acc) locs m
+
+
   let add_unknown_from :
       Ident.t -> callee_pname:Typ.Procname.t option -> location:Location.t -> t -> t =
    fun id ~callee_pname ~location m ->
@@ -1604,6 +1612,10 @@ module Mem = struct
    fun k -> f_lift_default ~default:false (MemReach.is_stack_loc k)
 
 
+  let is_rep_multi_loc : Loc.t -> _ t0 -> bool =
+   fun k -> f_lift_default ~default:false (MemReach.is_rep_multi_loc k)
+
+
   let find : Loc.t -> _ t0 -> Val.t = fun k -> f_lift_default ~default:Val.bot (MemReach.find k)
 
   let find_stack : Loc.t -> _ t0 -> Val.t =
@@ -1666,6 +1678,11 @@ module Mem = struct
     map ~f:(MemReach.add_heap ?represents_multiple_values k v)
 
 
+  let add_heap_set : ?represents_multiple_values:bool -> PowLoc.t -> Val.t -> t -> t =
+   fun ?represents_multiple_values ploc v ->
+    map ~f:(MemReach.add_heap_set ?represents_multiple_values ploc v)
+
+
   let add_unknown_from : Ident.t -> callee_pname:Typ.Procname.t -> location:Location.t -> t -> t =
    fun id ~callee_pname ~location ->
     map ~f:(MemReach.add_unknown_from id ~callee_pname:(Some callee_pname) ~location)

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -30,7 +30,7 @@ let rec must_alias : Exp.t -> Exp.t -> Mem.t -> bool =
   | Exp.Var x1, Exp.Var x2 -> (
     match (Mem.find_alias x1 m, Mem.find_alias x2 m) with
     | Some x1', Some x2' ->
-        AliasTarget.equal x1' x2'
+        AliasTarget.equal x1' x2' && not (Mem.is_rep_multi_loc (AliasTarget.get_loc x1') m)
     | _, _ ->
         false )
   | Exp.UnOp (uop1, e1', _), Exp.UnOp (uop2, e2', _) ->

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -32,9 +32,14 @@ end
 module Exec = struct
   open ModelEnv
 
-  let load_locs id typ locs mem =
+  let load_locs ~represents_multiple_values id typ locs mem =
     let v = Dom.Mem.find_set ~typ locs mem in
     let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in
+    let mem =
+      if represents_multiple_values then
+        Dom.Mem.add_heap_set ~represents_multiple_values locs v mem
+      else mem
+    in
     match PowLoc.is_singleton_or_more locs with
     | IContainer.Singleton loc ->
         Dom.Mem.load_simple_alias id loc mem

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -24,7 +24,8 @@ module ModelEnv : sig
 end
 
 module Exec : sig
-  val load_locs : Ident.t -> Typ.t -> PowLoc.t -> Dom.Mem.t -> Dom.Mem.t
+  val load_locs :
+    represents_multiple_values:bool -> Ident.t -> Typ.t -> PowLoc.t -> Dom.Mem.t -> Dom.Mem.t
 
   val decl_local : ModelEnv.model_env -> Dom.Mem.t * int -> Loc.t * Typ.t -> Dom.Mem.t * int
 

infer/tests/codetoanalyze/c/bufferoverrun/array_content.c

@@ -6,7 +6,7 @@
  */
 #include <stdio.h>
 
-int check_sorted_arr_good_FP(int a[], int length) {
+int check_sorted_arr_good(int a[], int length) {
   for (int i = 1; i < length; i++) {
     if (a[i] < a[i - 1]) { // should not report CONDITION_ALWAYS_FALSE
       return 0;
@@ -15,7 +15,7 @@ int check_sorted_arr_good_FP(int a[], int length) {
   return 1;
 }
 
-int check_sorted_arr10_good_FP(int a[10], int length) {
+int check_sorted_arr10_good(int a[10], int length) {
   for (int i = 1; i < length; i++) {
     if (a[i] < a[i - 1]) { // should not report CONDITION_ALWAYS_FALSE
       return 0;
@@ -24,7 +24,7 @@ int check_sorted_arr10_good_FP(int a[10], int length) {
   return 1;
 }
 
-int check_sorted_ptr_good_FP(int* a, int length) {
+int check_sorted_ptr_good(int* a, int length) {
   for (int i = 1; i < length; i++) {
     if (a[i] < a[i - 1]) { // should not report CONDITION_ALWAYS_FALSE
       return 0;
@@ -33,7 +33,7 @@ int check_sorted_ptr_good_FP(int* a, int length) {
   return 1;
 }
 
-int array_min_index_from_one_FP(int* a, int length) {
+int array_min_index_from_one(int* a, int length) {
   int index_min = 1;
   for (int i = 2; i < length; i++) {
     if (a[i] < a[index_min]) { // should not report CONDITION_ALWAYS_FALSE
@@ -51,7 +51,7 @@ int array_min_index_from_one_FP(int* a, int length) {
 */
 void call_array_min_index_from_one_good() {
   int a[2];
-  a[array_min_index_from_one_FP(a, 2) - 1] = 0;
+  a[array_min_index_from_one(a, 2) - 1] = 0;
 }
 
 void weak_update_Good_FP() {

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

@@ -45,12 +45,8 @@ codetoanalyze/c/bufferoverrun/arith.c, unused_integer_underflow_Good_FP, 2, COND
 codetoanalyze/c/bufferoverrun/arith.c, unused_integer_underflow_Good_FP, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: (0 - 1):unsigned32]
 codetoanalyze/c/bufferoverrun/arith.c, use_int64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 15 Size: 10]
 codetoanalyze/c/bufferoverrun/arith.c, use_uint64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 15 Size: 10]
-codetoanalyze/c/bufferoverrun/array_content.c, array_min_index_from_one_FP, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/array_content.c, call_literal_string_parameter1_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,<Offset trace>,Parameter `*s`,<Length trace>,Array declaration,Array access: Offset: [0, 112] Size: 112 by call to `literal_string_parameter` ]
 codetoanalyze/c/bufferoverrun/array_content.c, call_literal_string_parameter2_Bad, 0, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,<Offset trace>,Parameter `*s`,<Length trace>,Array declaration,Array access: Offset: [0, 112] Size: 112 by call to `literal_string_parameter` ]
-codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr10_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
-codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
-codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/array_content.c, fgets_may_not_change_str_Bad, 9, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Array declaration,<Length trace>,Array declaration,Array access: Offset: [0, 5] Size: 5]
 codetoanalyze/c/bufferoverrun/array_content.c, fgets_may_not_change_str_Good_FP, 9, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Array declaration,<Length trace>,Array declaration,Array access: Offset: [4, 9] Size: 5]
 codetoanalyze/c/bufferoverrun/array_content.c, fgets_null_check_Bad, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Array declaration,<Length trace>,Array declaration,Array access: Offset: [-1, 97] Size: 100]
@@ -130,7 +126,6 @@ codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Bad, 3, BUFFER
 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]
@@ -247,6 +242,7 @@ codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_alias, 3, BUFFER_OVERRUN_L1,
 codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_not_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 codetoanalyze/c/bufferoverrun/prune_alias.c, call_forget_locs_latest_prune_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Array declaration,Array access: Offset: 10 Size: 5 by call to `forget_locs_latest_prune` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, call_latest_prune_join_3_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `n`,<Length trace>,Parameter `*a`,Array access: Offset: 3 Size: 2 by call to `latest_prune_join` ]
+codetoanalyze/c/bufferoverrun/prune_alias.c, call_not_prune_multiple2_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Assignment,Call,<Offset trace>,Parameter `*m`,<Length trace>,Array declaration,Array access: Offset: [0, 10] Size: 5 by call to `not_prune_multiple2` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*x`,Array access: Offset: 5 Size: 5 by call to `prune_arrblk_ne_CAT` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, forget_locs_latest_prune, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/prune_alias.c, loop_prune2_Good_FP, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `length`,<Length trace>,Parameter `length`,Array declaration,Array access: Offset: [1, length] Size: length]

infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c

@@ -309,7 +309,7 @@ void call_not_prune_multiple2_Good() {
   not_prune_multiple2(m);
 }
 
-void call_not_prune_multiple2_Bad_FN() {
+void call_not_prune_multiple2_Bad() {
   int m[2] = {0, 10};
   not_prune_multiple2(m);
 }