From e7bee952d3d63316c0b8b938b48ab922b80deb17 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 23 Oct 2019 11:36:11 +0200
Subject: [PATCH] [Builtin] Module for allocation contracts components
---
headers/header_spec.txt | 2 +
src/plugins/builtin/Makefile.in | 1 +
src/plugins/builtin/stdlib/basic_alloc.ml | 70 ++++++++++++++++++++
src/plugins/builtin/stdlib/basic_alloc.mli | 35 ++++++++++
src/plugins/builtin/stdlib/malloc.ml | 77 +++++++---------------
5 files changed, 133 insertions(+), 52 deletions(-)
create mode 100644 src/plugins/builtin/stdlib/basic_alloc.ml
create mode 100644 src/plugins/builtin/stdlib/basic_alloc.mli
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 7eb1cb9bbec..fefa4de4484 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -937,6 +937,8 @@ src/plugins/builtin/builtin_builder.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/builtin/builtin_builder.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/builtin/configure.ac: CEA_LGPL_OR_PROPRIETARY
src/plugins/builtin/Makefile.in: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/stdlib/basic_alloc.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/stdlib/basic_alloc.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/builtin/stdlib/malloc.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/builtin/stdlib/malloc.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/builtin/string/memcmp.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/builtin/Makefile.in b/src/plugins/builtin/Makefile.in
index ec3691bfd99..d631ccb7f8f 100644
--- a/src/plugins/builtin/Makefile.in
+++ b/src/plugins/builtin/Makefile.in
@@ -37,6 +37,7 @@ SRC_STRING:= \
SRC_STRING:=$(addprefix string/, $(SRC_STRING))
SRC_STDLIB:= \
+ basic_alloc \
malloc
SRC_STDLIB:=$(addprefix stdlib/, $(SRC_STDLIB))
diff --git a/src/plugins/builtin/stdlib/basic_alloc.ml b/src/plugins/builtin/stdlib/basic_alloc.ml
new file mode 100644
index 00000000000..6e38a02f6bb
--- /dev/null
+++ b/src/plugins/builtin/stdlib/basic_alloc.ml
@@ -0,0 +1,70 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Logic_const
+open Cil_types
+
+let pis_allocable ?loc size =
+ pallocable ?loc (here_label, size)
+
+let is_allocable ?loc size =
+ let p = pis_allocable ?loc size in
+ new_predicate { p with pred_name = [ "allocable" ]}
+
+let isnt_allocable ?loc size =
+ let p = pnot ?loc (pis_allocable ?loc size) in
+ new_predicate { p with pred_name = [ "allocable" ]}
+
+let heap_status () =
+ let heap_status = Globals.Vars.find_from_astinfo "__fc_heap_status" VGlobal in
+ Basic_blocks.cvar_to_tvar (heap_status)
+
+let assigns_result ?loc typ deps =
+ let heap_status = new_identified_term (heap_status ()) in
+ let deps = match deps with
+ | [] -> []
+ | l -> heap_status :: (List.map new_identified_term l)
+ in
+ let result = new_identified_term (tresult ?loc typ) in
+ result, From deps
+
+let assigns_heap deps =
+ let heap_status = new_identified_term (heap_status ()) in
+ let deps = List.map new_identified_term deps in
+ heap_status, From (heap_status :: deps)
+
+let allocates_nothing () =
+ FreeAlloc([],[])
+
+let allocates_result ?loc t =
+ FreeAlloc ([], [new_identified_term (tresult ?loc t)])
+
+let fresh_result ?loc typ size =
+ let result = tresult ?loc typ in
+ let p = pfresh ?loc (old_label, here_label, result, size) in
+ new_predicate { p with pred_name = [ "fresh_result" ] }
+
+let null_result ?loc typ =
+ let tresult = tresult ?loc typ in
+ let tnull = term ?loc Tnull (Ctype typ) in
+ let p = prel ?loc (Req, tresult, tnull) in
+ new_predicate { p with pred_name = [ "null_result" ] }
diff --git a/src/plugins/builtin/stdlib/basic_alloc.mli b/src/plugins/builtin/stdlib/basic_alloc.mli
new file mode 100644
index 00000000000..0ff9e7864da
--- /dev/null
+++ b/src/plugins/builtin/stdlib/basic_alloc.mli
@@ -0,0 +1,35 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+val is_allocable: ?loc:location -> term -> identified_predicate
+val isnt_allocable: ?loc:location -> term -> identified_predicate
+
+val assigns_result: ?loc:location -> typ -> term list -> from
+val assigns_heap: term list -> from
+
+val allocates_nothing: unit -> allocation
+val allocates_result: ?loc:location -> typ -> allocation
+
+val fresh_result: ?loc:location -> typ -> term -> identified_predicate
+val null_result: ?loc:location -> typ -> identified_predicate
diff --git a/src/plugins/builtin/stdlib/malloc.ml b/src/plugins/builtin/stdlib/malloc.ml
index 465d4bc817f..212f7b4a102 100644
--- a/src/plugins/builtin/stdlib/malloc.ml
+++ b/src/plugins/builtin/stdlib/malloc.ml
@@ -21,82 +21,55 @@
(**************************************************************************)
open Basic_blocks
+open Basic_alloc
open Cil_types
open Logic_const
let function_name = "malloc"
-let fc_heap_status () =
- Globals.Vars.find_from_astinfo "__fc_heap_status" VGlobal
-
-let generate_requires loc ptr_type len =
+let generate_requires loc ptr_type size =
[ new_predicate
- { (pcorrect_len_bytes ~loc ptr_type len)
+ { (pcorrect_len_bytes ~loc ptr_type size)
with pred_name = ["aligned_end"] } ]
-let generate_global_assigns loc ptr_type len =
- let len = new_identified_term len in
- let res = new_identified_term (tresult ~loc ptr_type) in
- let hs = new_identified_term (cvar_to_tvar (fc_heap_status ())) in
- let assigns_result = res, From [ len ; hs ] in
- let assigns_heap = hs, From [ len ; hs ] in
+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
Writes [ assigns_result ; assigns_heap ]
-let is_allocable loc len =
- pallocable ~loc (here_label, len)
-
-let allocation_assumes loc len =
- [ new_predicate (is_allocable loc len) ]
-
-let allocation loc ptr_type =
- FreeAlloc ([], [new_identified_term (tresult ~loc ptr_type)])
-
-let allocation_ensures loc ptr_type len =
- let result = tresult ~loc ptr_type in
- let fresh = pfresh ~loc (old_label, here_label, result, len) in
- [ Normal, new_predicate fresh ]
-
-let make_behavior_allocation loc ptr_type len =
- let assumes = allocation_assumes loc len in
- let assigns = generate_global_assigns loc ptr_type len in
- let alloc = allocation loc ptr_type in
- let ensures = allocation_ensures loc ptr_type len in
+let make_behavior_allocation loc ptr_type size =
+ let assumes = [ is_allocable ~loc size ] in
+ let assigns = generate_global_assigns loc ptr_type size in
+ let alloc = allocates_result ~loc ptr_type in
+ let ensures = [ Normal, fresh_result ~loc ptr_type size ] in
make_behavior ~name:"allocation" ~assumes ~assigns ~alloc ~ensures ()
-let no_allocation_assumes loc len =
- [ new_predicate (pnot ~loc (is_allocable loc len)) ]
-
-let no_allocation_result loc ptr_type =
- let tresult = tresult ~loc ptr_type in
- let tnull = term ~loc Tnull (Ctype ptr_type) in
- [ Normal, new_predicate (prel ~loc (Req, tresult, tnull)) ]
-
-let make_behavior_no_allocation loc ptr_type len =
- let assumes = no_allocation_assumes loc len in
- let assigns = Writes [new_identified_term (tresult ~loc ptr_type), From []] in
- let ensures = no_allocation_result loc ptr_type in
- let alloc = FreeAlloc([],[]) in
+let make_behavior_no_allocation loc ptr_type size =
+ let assumes = [ isnt_allocable ~loc size ] 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 (clen) = match Cil.getFormalsDecl vi with
- | [ len ] -> len
+ let (csize) = match Cil.getFormalsDecl vi with
+ | [ size ] -> size
| _ -> assert false
in
- let len = tlogic_coerce ~loc (cvar_to_tvar clen) Linteger in
- let requires = generate_requires loc (Ctype (ptr_of alloc_typ)) len in
- let assigns = generate_global_assigns loc (ptr_of alloc_typ) len in
- let alloc = allocation loc (ptr_of alloc_typ) 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 assigns = generate_global_assigns loc (ptr_of alloc_typ) size in
+ let alloc = allocates_result ~loc (ptr_of alloc_typ) in
make_funspec [
make_behavior ~requires ~assigns ~alloc () ;
- make_behavior_allocation loc (ptr_of alloc_typ) len ;
- make_behavior_no_allocation loc (ptr_of alloc_typ) len
+ make_behavior_allocation loc (ptr_of alloc_typ) size ;
+ make_behavior_no_allocation loc (ptr_of alloc_typ) size
] ()
let generate_prototype alloc_t =
let name = function_name ^ "_" ^ (string_of_typ alloc_t) in
let params = [
- ("len", size_t (), [])
+ ("size", size_t (), [])
] in
name, (TFun((ptr_of alloc_t), Some params, false, []))
--
GitLab