[inferbo][bugfix] Declare parameter of flexible array member

Summary:
The `may_last_field` boolean value in the `decl_sym_val` function presents that the location *may* (not *must*) be a flexible array member.

By the modular analysis nature, it is impossible to determine whether a given argument is a flexible array member or not---because of lack of calling context.  For example, there are two function calls of `foo` below: (2) passes a flexible array member as an argument and (1) passes a non-flexible array, however it is hard to notice when analyzing the `foo` function.

```
struct T {
  int c[1];
};

struct S {
  struct T a;
  struct T b;
};

void foo(struct T x) { ... }

void goo () {
  struct S* x = (struct S*)malloc(sizeof(struct S) + 10 * sizeof(int));
  foo(&(x->a));  // (1)
  foo(&(x->b));  // (2)
}
```

We assume that any given arguments may stem from the last field of struct, i.e., flexible array member.  (This is why `decl_sym_val` is called with `may_last_field:true` at the first time.) With some tests, we noticed that the assumption does not harm the analysis precision, because whether regarding a parameter as a flexible array member or not is about using a symbolic array size instead of a constant array size written in the type during the analysis of callee. Therefore still it can raise correct alarms if the actual parameter is given in its caller.

Reviewed By: mbouaziz

Differential Revision: D7081295

fbshipit-source-id: a4d57a0

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -44,7 +44,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
    fun pname tenv node location loc typ ~inst_num ~new_sym_num mem ->
     let max_depth = 2 in
     let new_alloc_num = BoUtils.counter_gen 1 in
-    let rec decl_sym_val pname tenv node location ~depth ~is_last_field loc typ mem =
+    let rec decl_sym_val pname tenv node location ~depth ~may_last_field loc typ mem =
       if depth > max_depth then mem
       else
         let depth = depth + 1 in
@@ -64,35 +64,35 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             Dom.Mem.add_heap loc v mem
         | Typ.Tptr (typ, _) ->
             BoUtils.Exec.decl_sym_arr
-              ~decl_sym_val:(decl_sym_val ~is_last_field:false)
+              ~decl_sym_val:(decl_sym_val ~may_last_field)
               pname tenv node location ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem
         | Typ.Tarray {elt; length} ->
             let size =
               match length with
-              | Some length when is_last_field && (IntLit.iszero length || IntLit.isone length) ->
+              | Some length when may_last_field && (IntLit.iszero length || IntLit.isone length) ->
                   Some (Itv.make_sym pname new_sym_num)
               | _ ->
                   Option.map ~f:Itv.of_int_lit length
             in
             let offset = Itv.zero in
             BoUtils.Exec.decl_sym_arr
-              ~decl_sym_val:(decl_sym_val ~is_last_field:false)
+              ~decl_sym_val:(decl_sym_val ~may_last_field:false)
               pname tenv node location ~depth loc elt ~offset ?size ~inst_num ~new_sym_num
               ~new_alloc_num mem
         | Typ.Tstruct typename -> (
           match Models.TypName.dispatch typename with
           | Some {Models.declare_symbolic} ->
               let model_env = Models.mk_model_env pname node location tenv in
-              declare_symbolic ~decl_sym_val:(decl_sym_val ~is_last_field) model_env ~depth loc
+              declare_symbolic ~decl_sym_val:(decl_sym_val ~may_last_field) model_env ~depth loc
                 ~inst_num ~new_sym_num ~new_alloc_num mem
           | None ->
-              let decl_fld ~is_last_field mem (fn, typ, _) =
+              let decl_fld ~may_last_field mem (fn, typ, _) =
                 let loc_fld = Loc.append_field loc ~fn in
-                decl_sym_val pname tenv node location ~depth loc_fld typ ~is_last_field mem
+                decl_sym_val pname tenv node location ~depth loc_fld typ ~may_last_field mem
               in
               let decl_flds str =
-                IList.fold_last ~f:(decl_fld ~is_last_field:false)
+                IList.fold_last ~f:(decl_fld ~may_last_field:false)
-                  ~f_last:(decl_fld ~is_last_field) ~init:mem str.Typ.Struct.fields
+                  ~f_last:(decl_fld ~may_last_field) ~init:mem str.Typ.Struct.fields
               in
               let opt_struct = Tenv.lookup tenv typename in
               Option.value_map opt_struct ~default:mem ~f:decl_flds )
@@ -103,7 +103,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                 (CFG.loc node) ;
             mem
     in
-    decl_sym_val pname tenv node location ~depth:0 ~is_last_field:false loc typ mem
+    decl_sym_val pname tenv node location ~depth:0 ~may_last_field:true loc typ mem
 
 
   let declare_symbolic_parameters

infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp

@@ -150,14 +150,26 @@ class Tree {
   Tree* children[1];
 };
 
-void flexible_array5_Good_FP() {
+void flexible_array5_Good() {
   Tree* t = Tree::NewNode(3);
   t->set_child(Tree::NewLeaf(), 0);
   t->set_child(Tree::NewLeaf(), 1);
   t->set_child(Tree::NewLeaf(), 2);
 }
 
-void flexible_array5_Bad() {
+void flexible_array5_Bad_FN() {
   Tree* t = Tree::NewNode(3);
   t->set_child(Tree::NewLeaf(), 5);
 }
+
+void flexible_array_param_access(my_class4* x) { x->b[3] = 0; }
+
+void flexible_array_param_Good() {
+  my_class4* x = (my_class4*)malloc(sizeof(my_class4) + 4 * sizeof(int));
+  flexible_array_param_access(x);
+}
+
+void flexible_array_param_Bad() {
+  my_class4* x = (my_class4*)malloc(sizeof(my_class4) + 2 * sizeof(int));
+  flexible_array_param_access(x);
+}

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

@@ -3,8 +3,7 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc2_Bad, 2, BUFFER_O
 codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc_Bad, 2, BUFFER_OVERRUN_L1, [Offset: [10, 10] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array1_Bad, 3, BUFFER_OVERRUN_L1, [Offset: [5, 5] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array4_Bad, 3, BUFFER_OVERRUN_L1, [Offset: [5, 5] Size: [5, 5]]
-codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array5_Bad, 2, BUFFER_OVERRUN_L1, [Call,ArrayAccess: Offset: [5, 5] Size: [1, 1] @ codetoanalyze/cpp/bufferoverrun/class.cpp:139:51 by call `Tree_set_child()` ]
+codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_param_Bad, 2, BUFFER_OVERRUN_L1, [Call,ArrayAccess: Offset: [3, 3] Size: [3, 3] @ codetoanalyze/cpp/bufferoverrun/class.cpp:165:50 by call `flexible_array_param_access()` ]
-codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array5_Good_FP, 4, BUFFER_OVERRUN_L1, [Call,ArrayAccess: Offset: [2, 2] Size: [1, 1] @ codetoanalyze/cpp/bufferoverrun/class.cpp:139:51 by call `Tree_set_child()` ]
 codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, [Call,Assignment,Call,Assignment,Return,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
 codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, [Call,Call,Assignment,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
 codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_Bad, 3, BUFFER_OVERRUN_L1, [Offset: [10, 10] Size: [5, 5]]