Added model for memcpy C function to inferBO

Reviewed By: mbouaziz

Differential Revision: D9768893

fbshipit-source-id: b0e2ed894

infer/src/bufferoverrun/arrayBlk.ml

@@ -112,6 +112,10 @@ 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 sizeof_byte : astate -> Itv.t =
+ fun a -> fold (fun _ arr -> Itv.join (Itv.mult arr.ArrInfo.size arr.ArrInfo.stride)) a Itv.bot
+
+
 let plus_offset : astate -> Itv.t -> astate =
  fun arr i -> map (fun a -> ArrInfo.plus_offset a i) arr
 

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -126,6 +126,15 @@ let malloc size_exp =
   {exec; check}
 
 
+let memcpy dest_exp src_exp size_exp =
+  let exec _ ~ret:_ mem = mem
+  and check {location} mem cond_set =
+    BoUtils.Check.lindex_byte ~array_exp:dest_exp ~byte_index_exp:size_exp mem location cond_set
+    |> BoUtils.Check.lindex_byte ~array_exp:src_exp ~byte_index_exp:size_exp mem location
+  in
+  {exec; check}
+
+
 let realloc src_exp size_exp =
   let exec {location; tenv} ~ret:(id, _) mem =
     let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in
@@ -461,6 +470,7 @@ module Call = struct
       ; -"__get_array_length" <>$ capt_exp $!--> get_array_length
       ; -"__set_array_length" <>$ capt_arg $+ capt_exp $!--> set_array_length
       ; -"strlen" <>--> by_value Dom.Val.Itv.nat
+      ; -"memcpy" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> memcpy
       ; -"boost" &:: "split"
         $ capt_arg_of_typ (-"std" &:: "vector")
         $+ any_arg $+ any_arg $+? any_arg $--> Boost.Split.std_vector

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -306,4 +306,24 @@ module Check = struct
     let idx_sym_exp = Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f mem) index_exp in
     let relation = Dom.Mem.get_relation mem in
     array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true location cond_set
+
+
+  let array_access_byte ~arr ~idx ~relation ~is_plus location cond_set =
+    let arr_blk = Dom.Val.get_array_blk arr in
+    let size = ArrayBlk.sizeof_byte arr_blk in
+    let offset = ArrayBlk.offsetof arr_blk in
+    let idx_itv = Dom.Val.get_itv idx in
+    let idx_traces = Dom.Val.get_traces idx in
+    let idx_in_blk = (if is_plus then Itv.plus else Itv.minus) offset idx_itv in
+    L.(debug BufferOverrun Verbose)
+      "@[<v 2>Add condition :@,array: %a@,  idx: %a@,@]@." ArrayBlk.pp arr_blk Itv.pp idx_in_blk ;
+    check_access ~size ~idx:idx_in_blk ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr
+      ~idx_traces location cond_set ~is_collection_add:true
+
+
+  let lindex_byte ~array_exp ~byte_index_exp mem location cond_set =
+    let idx = Sem.eval byte_index_exp mem in
+    let arr = Sem.eval_arr array_exp mem in
+    let relation = Dom.Mem.get_relation mem in
+    array_access_byte ~arr ~idx ~relation ~is_plus:true location cond_set
 end

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -139,6 +139,14 @@ module Check : sig
     -> PO.ConditionSet.t
     -> PO.ConditionSet.t
 
+  val lindex_byte :
+       array_exp:Exp.t
+    -> byte_index_exp:Exp.t
+    -> Dom.Mem.astate
+    -> Location.t
+    -> PO.ConditionSet.t
+    -> PO.ConditionSet.t
+
   val collection_access :
        array_exp:Exp.t
     -> index_exp:Exp.t

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

@@ -66,6 +66,10 @@ codetoanalyze/c/bufferoverrun/models.c, exit_bo_good_unreachable_bad, 2, UNREACH
 codetoanalyze/c/bufferoverrun/models.c, fgetc_255_bad, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 255] Size: 255]
 codetoanalyze/c/bufferoverrun/models.c, fgetc_256_bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 256] Size: 256]
 codetoanalyze/c/bufferoverrun/models.c, fgetc_m1_bad, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [-1, 255] Size: 10000]
+codetoanalyze/c/bufferoverrun/models.c, memcpy_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 44 Size: 40]
+codetoanalyze/c/bufferoverrun/models.c, memcpy_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 44 Size: 40]
+codetoanalyze/c/bufferoverrun/models.c, memcpy_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 40]
+codetoanalyze/c/bufferoverrun/models.c, memcpy_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 8 Size: 4]
 codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10]
 codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: 10]
 codetoanalyze/c/bufferoverrun/pointer_arith.c, FP_pointer_arith5_Ok, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [3, 2043] Size: 1024]

infer/tests/codetoanalyze/c/bufferoverrun/models.c

@@ -47,3 +47,52 @@ void fgetc_257_good(FILE* f) {
   int c = fgetc(f);
   arr[c + 1] = 42;
 }
+
+void memcpy_bad1() {
+  int arr1[10];
+  int arr2[20];
+  memcpy(arr1, arr2, 44);
+}
+
+void memcpy_bad2() {
+  int arr1[10];
+  int arr2[20];
+  memcpy(arr2, arr1, 44);
+}
+
+void memcpy_bad3() {
+  int arr1[10];
+  int arr2[20];
+  memcpy(arr1, arr2, -1);
+}
+
+void memcpy_bad4() {
+  int src[1];
+  int buff[1];
+  int* dst = &buff[0];
+  memcpy(dst, src, sizeof(dst));
+}
+
+void memcpy_good1() {
+  int arr1[10];
+  int arr2[20];
+  memcpy(arr2, arr1, 40);
+}
+
+void memcpy_good2() {
+  int arr1[10];
+  int arr2[20];
+  memcpy(arr2, arr1, 0);
+}
+
+void memcpy_good3() {
+  int arr1[10];
+  int arr2[20];
+  memcpy(arr2, arr1, 20);
+}
+
+void memcpy_good4() {
+  int src[3];
+  int dst[3];
+  memcpy(dst, src, sizeof(dst));
+}