From 26a07366ab8624476f18dc767032b9a736ff04a4 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 23 Oct 2019 16:25:42 +0200
Subject: [PATCH] [Builtin] Flexible arrays fields for malloc/calloc
---
src/plugins/builtin/stdlib/basic_alloc.ml | 24 +++++++++++++++++++++-
src/plugins/builtin/stdlib/basic_alloc.mli | 2 ++
src/plugins/builtin/stdlib/calloc.ml | 16 +++++++++------
src/plugins/builtin/stdlib/malloc.ml | 7 +------
4 files changed, 36 insertions(+), 13 deletions(-)
diff --git a/src/plugins/builtin/stdlib/basic_alloc.ml b/src/plugins/builtin/stdlib/basic_alloc.ml
index 2d0252c539d..98de973cb61 100644
--- a/src/plugins/builtin/stdlib/basic_alloc.ml
+++ b/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 =
diff --git a/src/plugins/builtin/stdlib/basic_alloc.mli b/src/plugins/builtin/stdlib/basic_alloc.mli
index 0ff9e7864da..611b4c12634 100644
--- a/src/plugins/builtin/stdlib/basic_alloc.mli
+++ b/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
diff --git a/src/plugins/builtin/stdlib/calloc.ml b/src/plugins/builtin/stdlib/calloc.ml
index 996940ac155..a716c5cdbd4 100644
--- a/src/plugins/builtin/stdlib/calloc.ml
+++ b/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 [
diff --git a/src/plugins/builtin/stdlib/malloc.ml b/src/plugins/builtin/stdlib/malloc.ml
index 212f7b4a102..a696a6f6af1 100644
--- a/src/plugins/builtin/stdlib/malloc.ml
+++ b/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 [
--
GitLab