[Builtin] Flexible arrays fields for malloc/calloc

src/plugins/builtin/stdlib/basic_alloc.ml

@@ -21,11 +21,33 @@
 (**************************************************************************)
 
 open Logic_const
+open Basic_blocks
 open Cil_types
+open Extlib
+
+let valid_size ?loc typ size =
+  let p = match typ with
+    | TComp (ci, _, _) when Cil.has_flexible_array_member typ ->
+      let elem = match (last ci.cfields).ftype with
+        | TArray(t, _ , _, _) -> tinteger ?loc (Cil.bytesSizeOf t)
+        | _ -> assert false
+      in
+      let base = tinteger ?loc (Cil.bytesSizeOf typ) in
+      let flex = tminus ?loc size base in
+      let flex_mod = term ?loc (TBinOp(Mod, flex, elem)) Linteger in
+      let flex_at_least_zero = prel ?loc (Rle, Cil.lzero (), flex) in
+      let aligned_flex = prel ?loc (Req, Cil.lzero (), flex_mod) in
+      pand ?loc (flex_at_least_zero, aligned_flex)
+    | _ ->
+      let elem = tinteger ?loc (Cil.bytesSizeOf typ) in
+      let modulo = term ?loc (TBinOp(Mod, size, elem)) Linteger in
+      prel(Req, Cil.lzero (), modulo)
+  in
+  new_predicate { p with pred_name = ["correct_size"] }
 
 let pis_allocable ?loc size =
   let is_allocable = Logic_env.find_all_logic_functions "is_allocable" in
-  let is_allocable = Extlib.as_singleton is_allocable in
+  let is_allocable = as_singleton is_allocable in
   papp ?loc (is_allocable, [here_label], [size])
 
 let is_allocable ?loc size =

src/plugins/builtin/stdlib/basic_alloc.mli

@@ -22,6 +22,8 @@
 
 open Cil_types
 
+val valid_size: ?loc:location -> typ -> term -> identified_predicate
+
 val is_allocable: ?loc:location -> term -> identified_predicate
 val isnt_allocable: ?loc:location -> term -> identified_predicate
 

src/plugins/builtin/stdlib/calloc.ml

@@ -41,17 +41,21 @@ let pset_len_to_zero ?loc ptr_type len =
   let p = punfold_all_elems_pred ?loc result len eq_value in
   new_predicate { p with pred_name = [ "zero_initialization" ] }
 
+let generate_requires ?loc alloc_typ num size =
+  let only_one = if Cil.has_flexible_array_member alloc_typ then
+    let p = prel ?loc (Req, num, Cil.lone ?loc ()) in
+    Some (new_predicate { p with pred_name = ["only_one"] })
+  else
+    None
+  in
+  [ valid_size ?loc alloc_typ size ] @ (Extlib.list_of_opt only_one)
+
 let pinitialized_len ?loc ptr_type len =
   let result = tresult ?loc ptr_type in
   let initialized ?loc t = pinitialized ?loc (here_label, t) in
   let p = punfold_all_elems_pred ?loc result len initialized in
   new_predicate { p with pred_name = [ "initialization" ] }
 
-let generate_requires loc ptr_type len =
-  [ new_predicate
-      { (pcorrect_len_bytes ~loc ptr_type len)
-        with pred_name = ["aligned_end"] } ]
-
 let generate_global_assigns loc ptr_type num size =
   let assigns_result = assigns_result ~loc ptr_type [ num ; size ] in
   let assigns_heap = assigns_heap [ num ; size ] in
@@ -84,7 +88,7 @@ let generate_spec alloc_typ { svar = vi } loc =
   in
   let num = tlogic_coerce ~loc (cvar_to_tvar cnum) Linteger in
   let size = tlogic_coerce ~loc (cvar_to_tvar csize) Linteger in
-  let requires = generate_requires loc (Ctype (ptr_of alloc_typ)) size in
+  let requires = generate_requires ~loc alloc_typ num size in
   let assigns = generate_global_assigns loc (ptr_of alloc_typ) num size in
   let alloc = allocates_result ~loc (ptr_of alloc_typ) in
   make_funspec [

src/plugins/builtin/stdlib/malloc.ml

@@ -27,11 +27,6 @@ open Logic_const
 
 let function_name = "malloc"
 
-let generate_requires loc ptr_type size =
-  [ new_predicate
-      { (pcorrect_len_bytes ~loc ptr_type size)
-        with pred_name = ["aligned_end"] } ]
-
 let generate_global_assigns loc ptr_type size =
   let assigns_result = assigns_result ~loc ptr_type [ size ] in
   let assigns_heap = assigns_heap [ size ] in
@@ -57,7 +52,7 @@ let generate_spec alloc_typ { svar = vi } loc =
     | _ -> assert false
   in
   let size = tlogic_coerce ~loc (cvar_to_tvar csize) Linteger in
-  let requires = generate_requires loc (Ctype (ptr_of alloc_typ)) size in
+  let requires = [ valid_size ~loc alloc_typ size ] in
   let assigns = generate_global_assigns loc (ptr_of alloc_typ) size in
   let alloc = allocates_result ~loc (ptr_of alloc_typ) in
   make_funspec [