From 3fc7c696f3f1996a8f072102fb6d8570acdb1569 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 24 Oct 2019 10:13:56 +0200
Subject: [PATCH] [Builtin] Calloc with flexible array member OK
---
src/plugins/builtin/basic_blocks.ml | 58 +++++++++++++++------
src/plugins/builtin/basic_blocks.mli | 6 ++-
src/plugins/builtin/stdlib/calloc.ml | 78 +++++++++++++++++-----------
3 files changed, 95 insertions(+), 47 deletions(-)
diff --git a/src/plugins/builtin/basic_blocks.ml b/src/plugins/builtin/basic_blocks.ml
index 2cebff12702..ac48f23160f 100644
--- a/src/plugins/builtin/basic_blocks.ml
+++ b/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
diff --git a/src/plugins/builtin/basic_blocks.mli b/src/plugins/builtin/basic_blocks.mli
index 60d7d22cc0f..890cd71cab3 100644
--- a/src/plugins/builtin/basic_blocks.mli
+++ b/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 ->
diff --git a/src/plugins/builtin/stdlib/calloc.ml b/src/plugins/builtin/stdlib/calloc.ml
index a716c5cdbd4..8d11849cc72 100644
--- a/src/plugins/builtin/stdlib/calloc.ml
+++ b/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
--
GitLab