[Builtin] Calloc with flexible array member OK

src/plugins/builtin/basic_blocks.ml

@@ -75,8 +75,8 @@ let rec string_of_typ_aux = function
 and string_of_typ t = string_of_typ_aux (Cil.unrollType t)
 and string_of_exp e = Format.asprintf "%a" Cil_printer.pp_exp e
 
-let size_var t value = {
-  l_var_info = make_logic_var_local "__fc_len" t;
+let size_var ?(name_ext="") t value = {
+  l_var_info = make_logic_var_local ("__fc_" ^ name_ext ^ "len") t;
   l_type = Some t;
   l_tparams = [];
   l_labels = [];
@@ -154,19 +154,23 @@ let sizeofpointed = function
   | Ctype(TPtr(t, _)) | Ctype(TArray(t, _, _, _)) -> Cil.bytesSizeOf t
   | _ -> assert false
 
+let sizeof = function
+  | Ctype t -> Cil.bytesSizeOf t
+  | _ -> assert false
+
 let unroll_logic_type = function
   | Ctype t -> Ctype (Cil.unrollType t)
   | t -> t
 
 (** Features related to predicates *)
 
-let plet_len_div_size ?loc t bytes_len pred =
+let plet_len_div_size ?loc ?name_ext t bytes_len pred =
   let sizeof = sizeofpointed t in
   if sizeof = 1 then
     pred bytes_len
   else
     let len = tdivide ?loc bytes_len (tinteger ?loc sizeof) in
-    let len_var = size_var Linteger len in
+    let len_var = size_var ?name_ext Linteger len in
     plet ?loc len_var (pred (tvar len_var.l_var_info))
 
 let pgeneric_valid_buffer ?loc validity lbl ptr len =
@@ -217,23 +221,45 @@ and pall_elems_pred ?loc depth t1 len pred =
   let t1_acc = taccess ?loc t1 tind in
   let eq = punfold_pred ?loc depth t1_acc pred in
   pforall ?loc ([ind], (pimplies ?loc (bounds, eq)))
-and pall_fields_pred ?loc depth t1 ci pred =
-  let eq fi =
-    let lval = match t1.term_node with TLval(lv) -> lv | _ -> assert false in
-    let nlval = addTermOffsetLval (TField(fi, TNoOffset)) lval in
-    let term = term ?loc (TLval nlval) (Ctype fi.ftype) in
-    punfold_pred ?loc depth term pred
-  in
-  let eqs = List.map eq ci.cfields in
-  pands eqs
-and punfold_pred ?loc depth t1 pred =
+and punfold_pred ?loc ?(dyn_len = None) depth t1 pred =
   match unroll_logic_type t1.term_type with
-  | Ctype(TArray(_, Some len, _, _)) ->
-    let len = Logic_utils.expr_to_term ~cast:false len in
+  | Ctype(TArray(_, opt_len, _, _)) ->
+    let len = match opt_len, dyn_len with
+      | Some len, None -> Logic_utils.expr_to_term ~cast:false len
+      | _   , Some len -> len
+      | None, None -> assert false
+    in
     pall_elems_pred ?loc (depth+1) t1 len pred
   | Ctype(TComp(ci, _, _)) ->
     pall_fields_pred ?loc depth t1 ci pred
   | _ -> pred ?loc t1
+and pall_fields_pred ?loc ?(flex_mem_len=None) depth t1 ci pred =
+  let eq dyn_len fi =
+    let lval = match t1.term_node with TLval(lv) -> lv | _ -> assert false in
+    let nlval = addTermOffsetLval (TField(fi, TNoOffset)) lval in
+    let term = term ?loc (TLval nlval) (Ctype fi.ftype) in
+    punfold_pred ?loc ~dyn_len depth term pred
+  in
+  let rec eqs_fields = function
+    | [ x ] -> [ eq flex_mem_len x ]
+    | x :: l -> let x' = eq None x in x' :: (eqs_fields l)
+    | _ -> assert false
+  in
+  pands (eqs_fields ci.cfields)
+
+let punfold_flexible_struct_pred ?loc the_struct bytes_len pred =
+  let struct_len = tinteger ?loc (sizeof the_struct.term_type) in
+  let ci = match the_struct.term_type with
+    | Ctype(TComp(ci, _, _) as t) when Cil.has_flexible_array_member t -> ci
+    | _ -> assert false
+  in
+  let flex_type = Ctype (Extlib.last ci.cfields).ftype in
+  let flex_len = tminus bytes_len struct_len in
+  let pall_fields_pred len =
+    pall_fields_pred ?loc ~flex_mem_len:(Some len) 0 the_struct ci pred
+  in
+  plet_len_div_size ?loc ~name_ext:"flex" flex_type flex_len pall_fields_pred
+
 
 let pseparated_memories ?loc p1 len1 p2 len2 =
   let b1 = tbuffer_range ?loc p1 len1 in

src/plugins/builtin/basic_blocks.mli

@@ -49,12 +49,16 @@ val punfold_all_elems_eq: ?loc:location -> term -> term -> term -> predicate
 val punfold_all_elems_pred:
   ?loc:location -> term -> term ->
   (?loc: location -> term -> predicate) -> predicate
+val punfold_flexible_struct_pred:
+  ?loc:location -> term -> term ->
+  (?loc: location -> term -> predicate) -> predicate
 
 val pseparated_memories:
   ?loc:location -> term -> term -> term -> term -> predicate
 
 val plet_len_div_size:
-  ?loc:location -> logic_type -> term -> (term -> predicate) -> predicate
+  ?loc:location -> ?name_ext:string ->
+  logic_type -> term -> (term -> predicate) -> predicate
 
 val make_behavior:
   ?name:string ->

src/plugins/builtin/stdlib/calloc.ml

@@ -27,9 +27,8 @@ open Logic_const
 
 let function_name = "calloc"
 
-let pset_len_to_zero ?loc ptr_type len =
-  let result = tresult ?loc ptr_type in
-  let eq_value ?loc t =
+let pset_len_to_zero ?loc alloc_type num size =
+  let eq_simpl_value ?loc t =
     let value = match t.term_type with
       | Ctype(TPtr(_)) -> term Tnull t.term_type
       | Ctype(TFloat(_)) -> treal ?loc 0.
@@ -38,72 +37,91 @@ let pset_len_to_zero ?loc ptr_type len =
     in
     prel ?loc (Req, t, value)
   in
-  let p = punfold_all_elems_pred ?loc result len eq_value in
+  let ptr_type = ptr_of alloc_type in
+  let result = tresult ?loc ptr_type in
+  let p = if Cil.has_flexible_array_member alloc_type then
+      let access = Cil.mkTermMem ~addr:result ~off:TNoOffset in
+      let access = term ?loc (TLval access) (Ctype alloc_type) in
+      (* Note: calloc with flexible array member assumes num == 1 *)
+      punfold_flexible_struct_pred ?loc access size eq_simpl_value
+
+    else
+      punfold_all_elems_pred ?loc result num eq_simpl_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
+let generate_requires ?loc alloc_type num size =
+  let only_one = if Cil.has_flexible_array_member alloc_type 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)
+  [ valid_size ?loc alloc_type size ] @ (Extlib.list_of_opt only_one)
 
-let pinitialized_len ?loc ptr_type len =
-  let result = tresult ?loc ptr_type in
+let pinitialized_len ?loc alloc_type num size =
+  let result = tresult ?loc (ptr_of alloc_type) in
   let initialized ?loc t = pinitialized ?loc (here_label, t) in
-  let p = punfold_all_elems_pred ?loc result len initialized in
+  let p = if Cil.has_flexible_array_member alloc_type then
+      let access = Cil.mkTermMem ~addr:result ~off:TNoOffset in
+      let access = term ?loc (TLval access) (Ctype alloc_type) in
+      (* Note: calloc with flexible array member assumes num == 1 *)
+      punfold_flexible_struct_pred ?loc access size initialized
+    else
+      punfold_all_elems_pred ?loc result num initialized
+  in
   new_predicate { p with pred_name = [ "initialization" ] }
 
-let generate_global_assigns loc ptr_type num size =
-  let assigns_result = assigns_result ~loc ptr_type [ num ; size ] in
+let generate_global_assigns loc alloc_type num size =
+  let assigns_result = assigns_result ~loc (ptr_of alloc_type) [ num ; size ] in
   let assigns_heap = assigns_heap [ num ; size ] in
   Writes [ assigns_result ; assigns_heap ]
 
-let make_behavior_allocation loc ptr_type num size =
+let make_behavior_allocation loc alloc_type num size =
+  let ptr_type = ptr_of alloc_type in
   let len = term ~loc (TBinOp(Mult, num, size)) Linteger in
   let assumes = [ is_allocable ~loc len ] in
-  let assigns = generate_global_assigns loc ptr_type num size in
+  let assigns = generate_global_assigns loc alloc_type num size in
   let alloc   = allocates_result ~loc ptr_type in
   let ensures = [
     Normal, fresh_result ~loc ptr_type len ;
-    Normal, pset_len_to_zero ~loc ptr_type num ;
-    Normal, pinitialized_len ~loc ptr_type num
+    Normal, pset_len_to_zero ~loc alloc_type num size ;
+    Normal, pinitialized_len ~loc alloc_type num size
   ] in
   make_behavior ~name:"allocation" ~assumes ~assigns ~alloc ~ensures ()
 
-let make_behavior_no_allocation loc ptr_type num size =
+let make_behavior_no_allocation loc alloc_type num size =
   let len = term ~loc (TBinOp(Mult, num, size)) Linteger in
+  let ptr_type = ptr_of alloc_type in
   let assumes = [ isnt_allocable ~loc len ] in
   let assigns = Writes [assigns_result ~loc ptr_type []] in
   let ensures = [ Normal, null_result ~loc ptr_type ] in
   let alloc = allocates_nothing () in
   make_behavior ~name:"no_allocation" ~assumes ~assigns ~ensures ~alloc ()
 
-let generate_spec alloc_typ { svar = vi } loc =
+let generate_spec alloc_type { svar = vi } loc =
   let (cnum, csize) = match Cil.getFormalsDecl vi with
     | [ cnum ; csize ] -> cnum, csize
     | _ -> assert false
   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 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
+  let requires = generate_requires ~loc alloc_type num size in
+  let assigns = generate_global_assigns loc alloc_type num size in
+  let alloc = allocates_result ~loc (ptr_of alloc_type) in
   make_funspec [
     make_behavior ~requires ~assigns ~alloc () ;
-    make_behavior_allocation loc (ptr_of alloc_typ) num size ;
-    make_behavior_no_allocation loc (ptr_of alloc_typ) num size
+    make_behavior_allocation loc alloc_type num size ;
+    make_behavior_no_allocation loc alloc_type num size
   ] ()
 
-let generate_prototype alloc_t =
-  let name = function_name ^ "_" ^ (string_of_typ alloc_t) in
+let generate_prototype alloc_type =
+  let name = function_name ^ "_" ^ (string_of_typ alloc_type) in
   let params = [
     ("num", size_t (), []) ;
     ("size", size_t (), [])
   ] in
-  name, (TFun((ptr_of alloc_t), Some params, false, []))
+  name, (TFun((ptr_of alloc_type), Some params, false, []))
 
 let well_typed_call ret args =
   match ret, args with