From 2479c3ca68011fe7787fa256de87b10377561b32 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 22 Dec 2023 11:27:08 +0100
Subject: [PATCH] [eva] compute annotations
---
src/plugins/eva/Eva.mli | 8 ++++-
src/plugins/eva/parameters.ml | 15 +++++++++
src/plugins/eva/parameters.mli | 4 +++
src/plugins/eva/utils/annot.ml | 59 ++++++++++++++++++++++++++++++---
src/plugins/eva/utils/annot.mli | 8 ++++-
5 files changed, 88 insertions(+), 6 deletions(-)
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 753a55e2ec4..2df5d4aedad 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -993,5 +993,11 @@ module Annot: sig
{!generated} emitter. They are all assigned a valid status by
{!Analysis.emitter}.
*)
- val generator : unit -> Cil.cilVisitor
+ val generator : unit -> Visitor.frama_c_inplace
+
+ (**
+ Creates a visitor that can be used to remove all generated annotations from
+ {!generated} emitter. This will also remove their associated status.
+ *)
+ val cleaner : unit -> Visitor.frama_c_inplace
end
diff --git a/src/plugins/eva/parameters.ml b/src/plugins/eva/parameters.ml
index 620f41b7048..c706df45822 100644
--- a/src/plugins/eva/parameters.ml
+++ b/src/plugins/eva/parameters.ml
@@ -1276,6 +1276,21 @@ module MallocLevel =
let () = MallocLevel.set_range ~min:0 ~max:max_int
let () = add_precision_dep MallocLevel.parameter
+(* -------------------------------------------------------------------------- *)
+(* --- Annotations Generator options --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Annot =
+ Kernel_function_set
+ (struct
+ let option_name = "-eva-annot"
+ let arg_name = "f"
+ let help =
+ "Populate the specified functions with assertions \
+ representing the range of values computed by Eva \
+ on l-values read by the code, when available."
+ end)
+
(* -------------------------------------------------------------------------- *)
(* --- Deprecated options and aliases --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/eva/parameters.mli b/src/plugins/eva/parameters.mli
index 90225279e44..d43eed6b23c 100644
--- a/src/plugins/eva/parameters.mli
+++ b/src/plugins/eva/parameters.mli
@@ -170,6 +170,10 @@ val register_builtin: string -> unit
(** Registers available domain names for the -eva-domains option. *)
val register_domain: name:string -> descr:string -> unit
+(** Annotation Generator *)
+
+module Annot: Parameter_sig.Kernel_function_set
+
[@@@ api_start]
(** Configuration of the analysis. *)
diff --git a/src/plugins/eva/utils/annot.ml b/src/plugins/eva/utils/annot.ml
index c9901a5a86f..b89c06cc110 100644
--- a/src/plugins/eva/utils/annot.ml
+++ b/src/plugins/eva/utils/annot.ml
@@ -28,6 +28,7 @@ open Cil_types
module Ltype = Cil_datatype.Logic_type_ByName
module Exp = Cil_builder.Exp
+type visitor = Visitor.frama_c_visitor
type pred =
| True
@@ -166,7 +167,7 @@ module Slv = Cil_datatype.LvalStructEq.Set
class evaluator request =
object(self)
- inherit Visitor.generic_frama_c_visitor (Visitor_behavior.inplace ())
+ inherit Visitor.frama_c_inplace
val mutable locked = Slv.empty
val mutable domain : pred list = []
@@ -240,7 +241,7 @@ let eval_instr ?callstack ?name stmt =
| None -> r
| Some c -> Results.in_callstack c r in
let engine = new evaluator request in
- let _ = Cil.visitCilStmt (engine :> Cil.cilVisitor) stmt in
+ let _ = Visitor.visitFramacStmt (engine :> visitor) stmt in
List.map (predicate ?name ~loc:(Cil_datatype.Stmt.loc stmt)) engine#flush
(* -------------------------------------------------------------------------- *)
@@ -254,7 +255,7 @@ let generated = Emitter.create "Eva_domain"
class generator =
object(self)
- inherit Visitor.generic_frama_c_visitor (Visitor_behavior.inplace ())
+ inherit Visitor.frama_c_inplace
method! vlval _ = SkipChildren
method! vexpr _ = SkipChildren
@@ -278,6 +279,56 @@ class generator =
end
-let generator () = (new generator :> Cil.cilVisitor)
+let generator () = (new generator :> visitor)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Annotation Removal --- *)
+(* -------------------------------------------------------------------------- *)
+
+class cleaner =
+ object(self)
+ inherit Visitor.frama_c_inplace
+
+ method! vlval _ = SkipChildren
+ method! vexpr _ = SkipChildren
+
+ method !vstmt_aux stmt =
+ match self#current_kf with
+ | None -> Cil.SkipChildren
+ | Some kf ->
+ Annotations.iter_code_annot
+ (fun e ca ->
+ if Emitter.equal e generated then
+ Annotations.remove_code_annot e ~kf stmt ca
+ ) stmt ;
+ DoChildren
+
+ end
+
+let cleaner () = (new cleaner :> visitor)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Command Line Option --- *)
+(* -------------------------------------------------------------------------- *)
+
+let main () =
+ if Analysis.is_computed () then
+ let ast = Ast.get () in
+ let cleaner = cleaner () in
+ Self.feedback ~ontty:`Transient "Cleaning annotations..." ;
+ Visitor.visitFramacFile cleaner ast ;
+ let generator = new generator in
+ Parameters.Annot.iter
+ begin fun kf ->
+ if Kernel_function.has_definition kf then
+ let fundec = Kernel_function.get_definition kf in
+ Self.feedback "Annotate %a" Kernel_function.pretty kf ;
+ ignore @@ Visitor.visitFramacFunction generator fundec
+ else
+ Self.warning "Can not annotate %a (no definition)"
+ Kernel_function.pretty kf ;
+ end
+
+let () = Boot.Main.extend main
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/eva/utils/annot.mli b/src/plugins/eva/utils/annot.mli
index 119055ac515..2b322a32a0c 100644
--- a/src/plugins/eva/utils/annot.mli
+++ b/src/plugins/eva/utils/annot.mli
@@ -53,7 +53,13 @@ val generated : Emitter.t
{!generated} emitter. They are all assigned a valid status by
{!Analysis.emitter}.
*)
-val generator : unit -> Cil.cilVisitor
+val generator : unit -> Visitor.frama_c_inplace
+
+(**
+ Creates a visitor that can be used to remove all generated annotations from
+ {!generated} emitter. This will also remove their associated status.
+*)
+val cleaner : unit -> Visitor.frama_c_inplace
[@@@ api_end]
--
GitLab