From ad88a3e1c569a44171beba3d388cdd59efae57dd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 3 Apr 2020 20:46:59 +0200
Subject: [PATCH] [Eva] New annotation eva_allocate to configure allocation
builtins.
---
src/plugins/value/utils/eva_annotations.ml | 55 +++++++++++++++++++++
src/plugins/value/utils/eva_annotations.mli | 3 ++
2 files changed, 58 insertions(+)
diff --git a/src/plugins/value/utils/eva_annotations.ml b/src/plugins/value/utils/eva_annotations.ml
index 042ea9ac98a..59d82523218 100644
--- a/src/plugins/value/utils/eva_annotations.ml
+++ b/src/plugins/value/utils/eva_annotations.ml
@@ -34,6 +34,7 @@ type flow_annotation =
| FlowSplit of term
| FlowMerge of term
+type allocation_kind = By_stack | Fresh | Fresh_weak | Imprecise
(* We use two representations for annotations :
- the high level representation (HL) which is exported from this module
@@ -248,3 +249,57 @@ module Subdivision = Register (struct
let get_subdivision_annot = Subdivision.get
let add_subdivision_annot = Subdivision.add
+
+
+module Allocation = struct
+ let of_string = function
+ | "by_stack" -> Some By_stack
+ | "fresh" -> Some Fresh
+ | "fresh_weak" -> Some Fresh_weak
+ | "imprecise" -> Some Imprecise
+ | _ -> None
+
+ let to_string = function
+ | By_stack -> "by_stack"
+ | Fresh -> "fresh"
+ | Fresh_weak -> "fresh_weak"
+ | Imprecise -> "imprecise"
+
+ include Register (struct
+ type t = allocation_kind
+ let name = "eva_allocate"
+ let is_loop_annot = false
+
+ let parse ~typing_context:_ = function
+ | [{lexpr_node = PLvar s}] -> Extlib.the ~exn:Parse_error (of_string s)
+ | _ -> raise Parse_error
+
+ let export alloc_kind =
+ Ext_terms [Logic_const.tstring (to_string alloc_kind)]
+
+ let import = function
+ | Ext_terms [{term_node}] ->
+ (* Be kind and return By_stack by default. Someone is bound to write a
+ visitor that will simplify our term into something unrecognizable. *)
+ begin match term_node with
+ | TConst (LStr s) -> Extlib.opt_conv By_stack (of_string s)
+ | _ -> By_stack
+ end
+ | _ -> assert false
+
+ let print fmt alloc_kind =
+ Format.pp_print_string fmt (to_string alloc_kind)
+ end)
+
+ let get stmt =
+ match get stmt with
+ | [] -> Extlib.the (of_string (Value_parameters.AllocBuiltin.get ()))
+ | [x] -> x
+ | x :: _ ->
+ Value_parameters.warning ~current:true ~once:true
+ "Several eva_allocate annotations at the same statement; selecting %s\
+ and ignoring the others." (to_string x);
+ x
+end
+
+let get_allocation = Allocation.get
diff --git a/src/plugins/value/utils/eva_annotations.mli b/src/plugins/value/utils/eva_annotations.mli
index db6cbf66799..6a7ba48f7be 100644
--- a/src/plugins/value/utils/eva_annotations.mli
+++ b/src/plugins/value/utils/eva_annotations.mli
@@ -39,10 +39,13 @@ type flow_annotation =
| FlowSplit of Cil_types.term
| FlowMerge of Cil_types.term
+type allocation_kind = By_stack | Fresh | Fresh_weak | Imprecise
+
val get_slevel_annot : Cil_types.stmt -> slevel_annotation option
val get_unroll_annot : Cil_types.stmt -> unroll_annotation list
val get_flow_annot : Cil_types.stmt -> flow_annotation list
val get_subdivision_annot : Cil_types.stmt -> int list
+val get_allocation: Cil_types.stmt -> allocation_kind
val add_slevel_annot : emitter:Emitter.t -> loc:Cil_types.location ->
Cil_types.stmt -> slevel_annotation -> unit
--
GitLab