[inferbo] Literal string on stack location

Summary:
It adds semantics of assignment of literal string to stack locations, e.g., `char s[] = "hello";`.

Depends on D13668414

Reviewed By: ezgicicek, mbouaziz

Differential Revision: D13668505

fbshipit-source-id: 72caf35c3

infer/src/bufferoverrun/absLoc.ml

@@ -182,7 +182,7 @@ module Loc = struct
 
   let of_allocsite a = Allocsite a
 
-  let of_c_strlen a = Field (of_allocsite a, BufferOverrunField.c_strlen)
+  let of_c_strlen loc = Field (loc, BufferOverrunField.c_strlen)
 
   let of_pvar pvar = Var (Var.of_pvar pvar)
 

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -176,7 +176,8 @@ module TransferFunctions = struct
           let node_hash = CFG.Node.hash node in
           BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths
         in
-        BoUtils.Exec.decl_string model_env locs s mem
+        let do_alloc = not (Sem.is_stack_exp exp1 mem) in
+        BoUtils.Exec.decl_string model_env ~do_alloc locs s mem
     | Store (exp1, typ, exp2, location) ->
         let locs = Sem.eval_locs exp1 mem in
         let v =

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -1183,19 +1183,19 @@ module MemReach = struct
 
 
   (* unsound *)
-  let set_first_idx_of_null : Allocsite.t -> Val.t -> t -> t =
-   fun allocsite idx m -> update_mem (PowLoc.singleton (Loc.of_c_strlen allocsite)) idx m
+  let set_first_idx_of_null : Loc.t -> Val.t -> t -> t =
+   fun loc idx m -> update_mem (PowLoc.singleton (Loc.of_c_strlen loc)) idx m
 
 
   (* unsound *)
-  let unset_first_idx_of_null : Allocsite.t -> Val.t -> t -> t =
-   fun allocsite idx m ->
-    let old_c_strlen = find_heap (Loc.of_c_strlen allocsite) m in
+  let unset_first_idx_of_null : Loc.t -> Val.t -> t -> t =
+   fun loc idx m ->
+    let old_c_strlen = find_heap (Loc.of_c_strlen loc) m in
     let idx_itv = Val.get_itv idx in
     if Boolean.is_true (Itv.lt_sem idx_itv (Val.get_itv old_c_strlen)) then m
     else
       let new_c_strlen = Val.of_itv ~traces:(Val.get_traces idx) (Itv.incr idx_itv) in
-      set_first_idx_of_null allocsite new_c_strlen m
+      set_first_idx_of_null loc new_c_strlen m
 end
 
 module Mem = struct
@@ -1349,15 +1349,13 @@ module Mem = struct
 
   let unset_oenv = map ~f:MemReach.unset_oenv
 
-  let set_first_idx_of_null allocsite idx = map ~f:(MemReach.set_first_idx_of_null allocsite idx)
-
-  let unset_first_idx_of_null allocsite idx =
-    map ~f:(MemReach.unset_first_idx_of_null allocsite idx)
+  let set_first_idx_of_null loc idx = map ~f:(MemReach.set_first_idx_of_null loc idx)
 
+  let unset_first_idx_of_null loc idx = map ~f:(MemReach.unset_first_idx_of_null loc idx)
 
   let get_c_strlen locs m =
     let get_c_strlen' loc acc =
-      match loc with Loc.Allocsite a -> Val.join acc (find (Loc.of_c_strlen a) m) | _ -> acc
+      match loc with Loc.Allocsite _ -> Val.join acc (find (Loc.of_c_strlen loc) m) | _ -> acc
     in
     PowLoc.fold get_c_strlen' locs Val.bot
 end

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -75,7 +75,8 @@ let fgets str_exp num_exp =
         let num = Dom.Val.get_itv num_v in
         Itv.plus offset (Itv.set_lb_zero (Itv.decr num))
       in
-      Dom.Mem.set_first_idx_of_null allocsite (Dom.Val.of_itv ~traces strlen) acc
+      Dom.Mem.set_first_idx_of_null (Loc.of_allocsite allocsite) (Dom.Val.of_itv ~traces strlen)
+        acc
     in
     mem
     |> Dom.Mem.update_mem (Sem.eval_locs str_exp mem) Dom.Val.Itv.zero_255
@@ -383,7 +384,7 @@ module StdBasicString = struct
       match src with
       | Exp.Const (Const.Cstr s) ->
           let locs = Sem.eval_locs tgt mem in
-          BoUtils.Exec.decl_string model_env locs s mem
+          BoUtils.Exec.decl_string model_env ~do_alloc:true locs s mem
       | _ ->
           let tgt_locs = Sem.eval_locs tgt mem in
           let v = Sem.eval integer_type_widths src mem in

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -324,6 +324,19 @@ let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t =
       Val.bot
 
 
+let rec is_stack_exp : Exp.t -> Mem.t -> bool =
+ fun exp mem ->
+  match exp with
+  | Var _ ->
+      true
+  | Lvar pvar ->
+      Mem.is_stack_loc (Loc.of_pvar pvar) mem
+  | Cast (_, e) ->
+      is_stack_exp e mem
+  | _ ->
+      false
+
+
 module ParamBindings = struct
   include PrettyPrintable.MakePPMap (struct
     include Pvar

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -169,25 +169,33 @@ module Exec = struct
 
   let get_max_char s = String.fold s ~init:0 ~f:(fun acc c -> max acc (Char.to_int c))
 
-  let decl_string {pname; node_hash; location; integer_type_widths} locs s mem =
+  let decl_string {pname; node_hash; location; integer_type_widths} ~do_alloc locs s mem =
     let stride = Some (Typ.width_of_ikind integer_type_widths IChar / 8) in
     let offset = Itv.zero in
     let size = Itv.of_int (String.length s + 1) in
     let traces = Trace.Set.singleton location Trace.ArrayDeclaration in
     let char_itv = Itv.join Itv.zero (Itv.of_int (get_max_char s)) in
     let decl loc mem =
-      let allocsite =
-        let deref_kind = Symb.SymbolPath.Deref_ArrayIndex in
-        let path = Loc.get_path loc in
-        let deref_path = Option.map ~f:(fun path -> Symb.SymbolPath.deref ~deref_kind path) path in
-        Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path:deref_path
-          ~represents_multiple_values:true
+      (* It doesn't allocate if the character pointer is in stack, because they are already
+         allocated at the entry of the function. *)
+      let deref_loc, mem =
+        if do_alloc then
+          let allocsite =
+            let deref_kind = Symb.SymbolPath.Deref_ArrayIndex in
+            let path = Loc.get_path loc in
+            let deref_path =
+              Option.map ~f:(fun path -> Symb.SymbolPath.deref ~deref_kind path) path
+            in
+            Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path:deref_path
+              ~represents_multiple_values:true
+          in
+          let v = Dom.Val.of_c_array_alloc allocsite ~stride ~offset ~size ~traces in
+          (Loc.of_allocsite allocsite, Dom.Mem.update_mem (PowLoc.singleton loc) v mem)
+        else (loc, mem)
       in
-      let v = Dom.Val.of_c_array_alloc allocsite ~stride ~offset ~size ~traces in
       mem
-      |> Dom.Mem.update_mem (PowLoc.singleton loc) v
-      |> Dom.Mem.add_heap (Loc.of_allocsite allocsite) (Dom.Val.of_itv char_itv)
-      |> Dom.Mem.set_first_idx_of_null allocsite
+      |> Dom.Mem.add_heap deref_loc (Dom.Val.of_itv char_itv)
+      |> Dom.Mem.set_first_idx_of_null deref_loc
            (Dom.Val.of_itv ~traces (Itv.of_int (String.length s)))
     in
     PowLoc.fold decl locs mem
@@ -197,9 +205,10 @@ module Exec = struct
     let traces = TraceSet.join (Dom.Val.get_traces tgt) (Dom.Val.get_traces src) in
     let src_itv = Dom.Val.get_itv src in
     let set_c_strlen1 allocsite arrinfo acc =
+      let loc = Loc.of_allocsite allocsite in
       let idx = Dom.Val.of_itv ~traces (ArrayBlk.ArrInfo.offsetof arrinfo) in
-      if Itv.( <= ) ~lhs:Itv.zero ~rhs:src_itv then Dom.Mem.set_first_idx_of_null allocsite idx acc
-      else Dom.Mem.unset_first_idx_of_null allocsite idx acc
+      if Itv.( <= ) ~lhs:Itv.zero ~rhs:src_itv then Dom.Mem.set_first_idx_of_null loc idx acc
+      else Dom.Mem.unset_first_idx_of_null loc idx acc
     in
     ArrayBlk.fold set_c_strlen1 (Dom.Val.get_array_blk tgt) mem
 end

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -41,7 +41,8 @@ module Exec : sig
 
   val set_dyn_length : ModelEnv.model_env -> Typ.t -> PowLoc.t -> Itv.t -> Dom.Mem.t -> Dom.Mem.t
 
-  val decl_string : ModelEnv.model_env -> PowLoc.t -> string -> Dom.Mem.t -> Dom.Mem.t
+  val decl_string :
+    ModelEnv.model_env -> do_alloc:bool -> PowLoc.t -> string -> Dom.Mem.t -> Dom.Mem.t
 
   val set_c_strlen : tgt:Dom.Val.t -> src:Dom.Val.t -> Dom.Mem.t -> Dom.Mem.t
 end

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

@@ -135,7 +135,7 @@ void literal_string2_Good() {
   }
 }
 
-void literal_string2_Bad_FN() {
+void literal_string2_bad() {
   int a[1];
   char s[] = "hello";
   for (int i = 0; i < 5; i++) {

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

@@ -58,6 +58,8 @@ codetoanalyze/c/bufferoverrun/array_content.c, fgets_null_check_Bad, 3, BUFFER_O
 codetoanalyze/c/bufferoverrun/array_content.c, fgets_null_check_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [<LHS trace>,Array declaration,Binary operation: ([0, 99] - 2):unsigned64]
 codetoanalyze/c/bufferoverrun/array_content.c, fgets_null_check_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Array declaration,<Length trace>,Array declaration,Array access: Offset: [-1, 98] Size: 100]
 codetoanalyze/c/bufferoverrun/array_content.c, fgets_null_check_Good_FP, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [<LHS trace>,Array declaration,Binary operation: ([0, 99] - 1):unsigned64]
+codetoanalyze/c/bufferoverrun/array_content.c, literal_string2_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/c/bufferoverrun/array_content.c, literal_string2_bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [0, 111] Size: 1]
 codetoanalyze/c/bufferoverrun/array_content.c, literal_string_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/array_content.c, literal_string_bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [0, 111] Size: 1]
 codetoanalyze/c/bufferoverrun/array_content.c, strlen_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Array declaration,<Length trace>,Array declaration,Array access: Offset: 5 Size: 5]