[inferbo] Resize array on casting

Summary:
It modifies sizes and offsets of array values on pointer castings.
Currently, it supports only simple castings of pointer-to-integers.

Reviewed By: mbouaziz

Differential Revision: D12920589

fbshipit-source-id: a5ba831b8

infer/src/bufferoverrun/arrayBlk.ml

@@ -93,6 +93,16 @@ module ArrInfo = struct
 
 
   let set_size : Itv.t -> t -> t = fun size arr -> {arr with size}
+
+  (* Set new stride only when the previous stride is a constant interval. *)
+  let set_stride : Z.t -> t -> t =
+   fun new_stride ({offset; size; stride} as arr) ->
+    Option.value_map (Itv.is_const stride) ~default:arr ~f:(fun stride ->
+        assert ((not Z.(equal stride zero)) && not Z.(equal new_stride zero)) ;
+        if Z.equal new_stride stride then arr
+        else
+          let set itv = Itv.div_const (Itv.mult_const itv stride) new_stride in
+          {offset= set offset; size= set size; stride= Itv.of_big_int new_stride} )
 end
 
 include AbstractDomain.Map (Allocsite) (ArrInfo)
@@ -111,6 +121,8 @@ let offsetof : astate -> Itv.t = fun a -> fold (fun _ arr -> Itv.join arr.ArrInf
 
 let sizeof : astate -> Itv.t = fun a -> fold (fun _ arr -> Itv.join arr.ArrInfo.size) a Itv.bot
 
+let strideof : astate -> Itv.t = fun a -> fold (fun _ arr -> Itv.join arr.ArrInfo.stride) a Itv.bot
+
 let sizeof_byte : astate -> Itv.t =
  fun a -> fold (fun _ arr -> Itv.join (Itv.mult arr.ArrInfo.size arr.ArrInfo.stride)) a Itv.bot
 
@@ -170,3 +182,5 @@ let prune_eq : astate -> astate -> astate = fun a1 a2 -> do_prune ArrInfo.prune_
 let prune_ne : astate -> astate -> astate = fun a1 a2 -> do_prune ArrInfo.prune_ne a1 a2
 
 let set_size : Itv.t -> astate -> astate = fun size a -> map (ArrInfo.set_size size) a
+
+let set_stride : Z.t -> astate -> astate = fun stride a -> map (ArrInfo.set_stride stride) a

infer/src/bufferoverrun/bounds.ml

@@ -430,11 +430,10 @@ module Bound = struct
 
   let xcompare = PartialOrder.of_le ~le
 
-  let is_const : t -> bool = function
-    | Linear (_, se) when SymLinear.is_zero se ->
-        true
-    | _ ->
-        false
+  let is_const : t -> bool = function Linear (_, se) -> SymLinear.is_zero se | _ -> false
+
+  let eq_const : Z.t -> t -> bool =
+   fun z -> function Linear (z', se) -> SymLinear.is_zero se && Z.(equal z' z) | _ -> false
 
 
   let neg : t -> t = function

infer/src/bufferoverrun/bounds.mli

@@ -91,6 +91,8 @@ module Bound : sig
 
   val is_const : t -> Z.t sexp_option
 
+  val eq_const : Z.t -> t -> bool
+
   val plus_l : t -> t -> t
 
   val plus_u : t -> t -> t

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -319,6 +319,13 @@ module Val = struct
    fun size v -> {v with arrayblk= ArrayBlk.set_size size v.arrayblk}
 
 
+  let set_array_stride : Z.t -> t -> t =
+   fun new_stride v ->
+    let stride = ArrayBlk.strideof (get_array_blk v) in
+    if Itv.eq_const new_stride stride then v
+    else {v with arrayblk= ArrayBlk.set_stride new_stride v.arrayblk}
+
+
   module Itv = struct
     let m1_255 = of_itv Itv.m1_255
 

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -131,6 +131,15 @@ let rec must_alias_cmp : Exp.t -> Mem.astate -> bool =
       false
 
 
+let set_array_stride integer_type_widths typ v =
+  match typ with
+  | Typ.({desc= Tptr ({desc= Tint ikind}, Pk_pointer)}) ->
+      let width = Typ.width_of_ikind integer_type_widths ikind in
+      Val.set_array_stride (Z.of_int (width / 8)) v
+  | _ ->
+      v
+
+
 let rec eval : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> Val.t =
  fun integer_type_widths exp mem ->
   if must_alias_cmp exp mem then Val.of_int 0
@@ -147,8 +156,9 @@ let rec eval : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> Val.t =
         eval_binop integer_type_widths bop e1 e2 mem
     | Exp.Const c ->
         eval_const c
-    | Exp.Cast (_, e) ->
-        eval integer_type_widths e mem
+    | Exp.Cast (t, e) ->
+        let v = eval integer_type_widths e mem in
+        set_array_stride integer_type_widths t v
     | Exp.Lfield (e, fn, _) ->
         eval integer_type_widths e mem |> Val.get_all_locs |> PowLoc.append_field ~fn
         |> Val.of_pow_loc
@@ -263,8 +273,9 @@ let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> Val.t =
       Mem.find_set (PowLoc.singleton (Loc.of_pvar pvar)) mem
   | Exp.BinOp (bop, e1, e2) ->
       eval_binop integer_type_widths bop e1 e2 mem
-  | Exp.Cast (_, e) ->
-      eval_arr integer_type_widths e mem
+  | Exp.Cast (t, e) ->
+      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
       Mem.find_set locs mem

infer/src/bufferoverrun/itv.ml

@@ -574,12 +574,14 @@ module ItvPure = struct
   let is_const : t -> Z.t option =
    fun (l, u) ->
     match (Bound.is_const l, Bound.is_const u) with
-    | Some n, Some m when Z.equal n m ->
-        Some n
+    | (Some n as z), Some m when Z.equal n m ->
+        z
     | _, _ ->
         None
 
 
+  let eq_const : Z.t -> t -> bool = fun z (l, u) -> Bound.eq_const z l && Bound.eq_const z u
+
   let is_zero : t -> bool = fun (l, u) -> Bound.is_zero l && Bound.is_zero u
 
   let is_one : t -> bool = fun (l, u) -> Bound.eq l Bound.one && Bound.eq u Bound.one
@@ -940,6 +942,10 @@ let bind1 : (ItvPure.t -> t) -> t -> t = bind1_gen ~bot:Bottom
 
 let bind1b : (ItvPure.t -> Boolean.t) -> t -> Boolean.t = bind1_gen ~bot:Boolean.Bottom
 
+let bind1bool : (ItvPure.t -> bool) -> t -> bool = bind1_gen ~bot:false
+
+let bind1zo : (ItvPure.t -> Z.t option) -> t -> Z.t option = bind1_gen ~bot:None
+
 let lift2 : (ItvPure.t -> ItvPure.t -> ItvPure.t) -> t -> t -> t =
  fun f x y ->
   match (x, y) with
@@ -972,14 +978,22 @@ let make_sym : ?unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t
   NonBottom (ItvPure.make_sym ~unsigned pname symbol_table path new_sym_num)
 
 
+let is_const : astate -> Z.t option = bind1zo ItvPure.is_const
+
+let eq_const : Z.t -> astate -> bool = fun z -> bind1bool (ItvPure.eq_const z)
+
 let neg : t -> t = lift1 ItvPure.neg
 
 let lnot : t -> Boolean.t = bind1b ItvPure.lnot
 
 let mult : t -> t -> t = lift2 ItvPure.mult
 
+let mult_const : t -> Z.t -> t = fun x z -> lift1 (fun x -> ItvPure.mult_const z x) x
+
 let div : t -> t -> t = lift2 ItvPure.div
 
+let div_const : t -> Z.t -> t = fun x z -> lift1 (fun x -> ItvPure.div_const x z) x
+
 let mod_sem : t -> t -> t = lift2 ItvPure.mod_sem
 
 let shiftlt : t -> t -> t = lift2 ItvPure.shiftlt

infer/src/bufferoverrun/itv.mli

@@ -172,6 +172,10 @@ val of_int_lit : IntLit.t -> t
 
 val of_int64 : Int64.t -> t
 
+val is_const : t -> Z.t option
+
+val eq_const : Z.t -> t -> bool
+
 val make_sym :
   ?unsigned:bool -> Typ.Procname.t -> Symb.SymbolTable.t -> Symb.SymbolPath.t -> Counter.t -> t
 
@@ -199,10 +203,14 @@ val range : t -> ItvRange.t
 
 val div : t -> t -> t
 
+val div_const : t -> Z.t -> t
+
 val minus : t -> t -> t
 
 val mult : t -> t -> t
 
+val mult_const : t -> Z.t -> t
+
 val plus : t -> t -> t
 
 val shiftlt : t -> t -> t

infer/tests/codetoanalyze/c/bufferoverrun/array_multidim.c

@@ -33,7 +33,7 @@ void multidim_arr3_Good() {
   };
 }
 
-void multidim_arr4_Good_FP() {
+void multidim_arr4_Good() {
   int a[3][2];
   int* p = a;
   *(p + 5) = 0;
@@ -56,3 +56,19 @@ void multidim_arr5_Bad() {
   a[0][0] = 0;
   a[0][10] = 0;
 }
+
+void multidim_arr6_Good() {
+  int a[3][2];
+  int b[10];
+  int* p = a;
+  *p = 5;
+  b[a[0][0]] = 1;
+}
+
+void multidim_arr6_Bad_FN() {
+  int a[3][2];
+  int b[5];
+  int* p = a;
+  *p = 5;
+  b[a[0][0]] = 1;
+}

infer/tests/codetoanalyze/c/bufferoverrun/cast.c

@@ -17,11 +17,16 @@ void cast_Bad_FN() {
   *(int32_t*)arr = 123;
 }
 
-void cast2_Good_FP() {
+void cast2_Good() {
   int32_t arr[4];
   *(((char*)arr) + 4) = 123;
 }
 
+void cast2_Bad() {
+  int32_t arr[4];
+  *(((char*)arr) + 20) = 123;
+}
+
 void cast_unsigned_to_signed_Good() {
   char arr[10];
   uint32_t x = 15;

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

@@ -38,8 +38,7 @@ codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_O
 codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Parameter: x[*].f,Assignment,Assignment,Assignment,ArrayAccess: Offset: -1 Size: 2]
 codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 2 Size: 2]
 codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 3 Size: 3]
-codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 6 Size: 3]
-codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr4_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 5 Size: 3]
+codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 6 Size: 6]
 codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr5_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/big_array.c, use_big_array_bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Assignment,Return,Assignment,ArrayAccess: Offset: 999999999 Size: 26460]
 codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
@@ -47,7 +46,7 @@ codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13
 codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10]
 codetoanalyze/c/bufferoverrun/calloc.c, calloc_bad1, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: -1 Size: 10]
 codetoanalyze/c/bufferoverrun/calloc.c, calloc_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 10 Size: 10]
-codetoanalyze/c/bufferoverrun/cast.c, cast2_Good_FP, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 4 Size: 4]
+codetoanalyze/c/bufferoverrun/cast.c, cast2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 20 Size: 16]
 codetoanalyze/c/bufferoverrun/cast.c, cast_float_to_int_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/cast.c, cast_float_to_int_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
@@ -191,9 +190,10 @@ codetoanalyze/c/bufferoverrun/relation.c, FP_array_access2_Ok, 4, BUFFER_OVERRUN
 codetoanalyze/c/bufferoverrun/relation.c, FP_array_access3_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 3 Size: 1]
 codetoanalyze/c/bufferoverrun/relation.c, FP_array_access4_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 3 Size: 1]
 codetoanalyze/c/bufferoverrun/relation.c, FP_call_array_access_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: -1 Size: 1 by call to `array_access_Ok` ]
-codetoanalyze/c/bufferoverrun/sizeof.c, FN_static_stride_bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 1 Size: 0]
+codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 5, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
+codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 1 Size: 0]
 codetoanalyze/c/bufferoverrun/trivial.c, malloc_zero_Bad, 2, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Alloc: Length: 0]
 codetoanalyze/c/bufferoverrun/trivial.c, trivial_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_once_intentional_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]

infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c

@@ -20,7 +20,7 @@ struct some_struct {
   int x1;
 };
 
-void FN_static_stride_bad() {
+void static_stride_bad() {
   struct some_struct a[10];
   char *x, *y;
   x = (char*)&(a[5]);

infer/tests/codetoanalyze/cpp/bufferoverrun/relation.cpp

@@ -116,6 +116,6 @@ size_t id(size_t s) {
 void FP_call_id_Ok() {
   size_t s1 = 5;
   size_t s2 = id(1 + s1);
-  char* arr = (char*)malloc(s2 * sizeof(char*));
+  char* arr = (char*)malloc(s2 * sizeof(char));
   arr[s1] = 0;
 }