From e9cef177c3e85b97bf8f5b9d1748201b7c91e1a9 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 22 Oct 2019 17:52:34 +0200
Subject: [PATCH] [Builtin] Adds malloc
---
headers/header_spec.txt | 2 +
src/plugins/builtin/Makefile.in | 2 +-
src/plugins/builtin/builtin_builder.ml | 6 ++
src/plugins/builtin/malloc.ml | 131 +++++++++++++++++++++++++
src/plugins/builtin/malloc.mli | 21 ++++
src/plugins/builtin/transform.ml | 18 ++--
6 files changed, 172 insertions(+), 8 deletions(-)
create mode 100644 src/plugins/builtin/malloc.ml
create mode 100644 src/plugins/builtin/malloc.mli
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 9cf5277d18f..093fdc6dc87 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/malloc.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/malloc.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/builtin/memcmp.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/builtin/memcmp.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/builtin/memcpy.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/builtin/Makefile.in b/src/plugins/builtin/Makefile.in
index 70d49bb5ece..09306b9c327 100644
--- a/src/plugins/builtin/Makefile.in
+++ b/src/plugins/builtin/Makefile.in
@@ -38,7 +38,7 @@ PLUGIN_ENABLE := @ENABLE_BUILTIN@
PLUGIN_NAME := Builtin
PLUGIN_CMI :=
PLUGIN_CMO := basic_blocks options builtin_builder transform \
- memcpy memcmp memmove memset \
+ malloc memcpy memcmp memmove memset \
register
PLUGIN_DISTRIBUTED := $(PLUGIN_ENABLE)
PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
diff --git a/src/plugins/builtin/builtin_builder.ml b/src/plugins/builtin/builtin_builder.ml
index c3c201351ed..05294da6d68 100644
--- a/src/plugins/builtin/builtin_builder.ml
+++ b/src/plugins/builtin/builtin_builder.ml
@@ -92,6 +92,12 @@ module Make_builtin (G: Generator_sig) = struct
let kf = Globals.Functions.get fd.svar in
let spec = generate_spec key fd loc in
Annotations.add_behaviors Options.emitter kf spec.spec_behavior ;
+ List.iter
+ (Annotations.add_complete Options.emitter kf)
+ spec.spec_complete_behaviors ;
+ List.iter
+ (Annotations.add_disjoint Options.emitter kf)
+ spec.spec_disjoint_behaviors ;
fd
let get_override key =
diff --git a/src/plugins/builtin/malloc.ml b/src/plugins/builtin/malloc.ml
new file mode 100644
index 00000000000..465d4bc817f
--- /dev/null
+++ b/src/plugins/builtin/malloc.ml
@@ -0,0 +1,131 @@
+(**************************************************************************)
+(* *)
+(* 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 Basic_blocks
+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 =
+ [ new_predicate
+ { (pcorrect_len_bytes ~loc ptr_type len)
+ 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
+ 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
+ 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
+ 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
+ | _ -> 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
+ 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
+ ] ()
+
+let generate_prototype alloc_t =
+ let name = function_name ^ "_" ^ (string_of_typ alloc_t) in
+ let params = [
+ ("len", size_t (), [])
+ ] in
+ name, (TFun((ptr_of alloc_t), Some params, false, []))
+
+let well_typed_call ret args =
+ match ret, args with
+ | Some ret, [ _ ] -> Cil.isPointerType (Cil.typeOfLval ret)
+ | _ -> false
+
+let key_from_call ret _ =
+ match ret with
+ | Some ret ->
+ let ret_t = Cil.unrollTypeDeep (Cil.typeOfLval ret) in
+ let ret_t = Cil.type_remove_qualifier_attributes_deep ret_t in
+ Cil.typeOf_pointed ret_t
+ | None -> assert false
+
+let retype_args _typ args = args
+let args_for_original _typ fd =
+ List.map Cil.evar fd.sformals
+
+let () = Transform.register (module struct
+ module Hashtbl = Cil_datatype.Typ.Hashtbl
+ type override_key = typ
+
+ let function_name = function_name
+ let well_typed_call = well_typed_call
+ let key_from_call = key_from_call
+ let retype_args = retype_args
+ let generate_prototype = generate_prototype
+ let generate_spec = generate_spec
+ let args_for_original = args_for_original
+ end)
diff --git a/src/plugins/builtin/malloc.mli b/src/plugins/builtin/malloc.mli
new file mode 100644
index 00000000000..fa8f3783c35
--- /dev/null
+++ b/src/plugins/builtin/malloc.mli
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
diff --git a/src/plugins/builtin/transform.ml b/src/plugins/builtin/transform.ml
index c501c73ee29..71942f21e45 100644
--- a/src/plugins/builtin/transform.ml
+++ b/src/plugins/builtin/transform.ml
@@ -139,20 +139,24 @@ let compute_call_preconditions_statuses kf =
| _ -> assert false
let compute_postconditions_statuses kf =
- let open Extlib in
let posts bhv =
- let active = [] in
- let ensures = Property.ip_ensures_of_behavior kf Kglobal bhv in
- let assigns = Property.ip_assigns_of_behavior ~active kf Kglobal bhv in
- let froms = Property.ip_from_of_behavior ~active kf Kglobal bhv in
- List.iter validate_property (ensures @ (list_of_opt assigns) @ froms)
+ List.iter validate_property
+ (Property.ip_post_cond_of_behavior kf ~active:[] Kglobal bhv)
in
Annotations.iter_behaviors (fun _ -> posts) kf
+let compute_comp_disj_statuses kf =
+ let open Property in
+ let comps c = validate_property (ip_of_complete kf Kglobal ~active:[] c) in
+ let disjs d = validate_property (ip_of_disjoint kf Kglobal ~active:[] d) in
+ Annotations.iter_complete (fun _ -> comps) kf ;
+ Annotations.iter_disjoint (fun _ -> disjs) kf
+
let compute_statuses_all_kfs () =
let kfs = get_kfs () in
List.iter compute_call_preconditions_statuses kfs ;
- List.iter compute_postconditions_statuses kfs
+ List.iter compute_postconditions_statuses kfs ;
+ List.iter compute_comp_disj_statuses kfs
let transform file =
Visitor.visitFramacFile (new transformer) file ;
--
GitLab