From 8d16aaed380f85483faa4cb652759ea2ae9c9e66 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 8 Jun 2022 09:40:22 +0200
Subject: [PATCH] [Eva] New request to print the internal domain states for a
given marker.
Results: new function print_states returning a textual representation of the
internal domain states, as a list for all available domains.
---
.../frama-c/plugins/eva/api/general/index.ts | 22 ++++++
src/plugins/value/api/general_requests.ml | 71 ++++++++++++++++++-
src/plugins/value/utils/results.ml | 24 +++++++
src/plugins/value/utils/results.mli | 5 ++
4 files changed, 120 insertions(+), 2 deletions(-)
diff --git a/ivette/src/frama-c/plugins/eva/api/general/index.ts b/ivette/src/frama-c/plugins/eva/api/general/index.ts
index 55d8b6b7768..9d3579ba0b3 100644
--- a/ivette/src/frama-c/plugins/eva/api/general/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/general/index.ts
@@ -580,4 +580,26 @@ export const functionStats: State.Array<
functionStatsData
> = functionStats_internal;
+const getStates_internal: Server.GetRequest<
+ marker,
+ [ string, string, string ][]
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getStates',
+ input: jMarker,
+ output: Json.jList(
+ Json.jTry(
+ Json.jTriple(
+ Json.jFail(Json.jString,'String expected'),
+ Json.jFail(Json.jString,'String expected'),
+ Json.jFail(Json.jString,'String expected'),
+ ))),
+ signals: [],
+};
+/** Get the domain states about the given marker */
+export const getStates: Server.GetRequest<
+ marker,
+ [ string, string, string ][]
+ >= getStates_internal;
+
/* ------------------------------------- */
diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml
index 8a6068698cb..0a981edd276 100644
--- a/src/plugins/value/api/general_requests.ml
+++ b/src/plugins/value/api/general_requests.ml
@@ -261,7 +261,7 @@ let _array =
model
-(* ----- Analysis statistics -------------------------------------------- *)
+(* ----- Analysis statistics ------------------------------------------------ *)
module AlarmCategory = struct
open Server.Data
@@ -470,4 +470,71 @@ let _array =
model
-(**************************************************************************)
+(* ----- Domains states ----------------------------------------------------- *)
+
+let compute_lval_deps request lval =
+ let zone = Results.lval_deps lval request in
+ Locations.Zone.get_bases zone
+
+let compute_expr_deps request expr =
+ let zone = Results.expr_deps expr request in
+ Locations.Zone.get_bases zone
+
+let compute_instr_deps request = function
+ | Set (lval, expr, _) ->
+ Base.SetLattice.join
+ (compute_lval_deps request lval)
+ (compute_expr_deps request expr)
+ | Local_init (vi, AssignInit (SingleInit expr), _) ->
+ Base.SetLattice.join
+ (Base.SetLattice.inject_singleton (Base.of_varinfo vi))
+ (compute_expr_deps request expr)
+ | _ -> Base.SetLattice.empty
+
+let compute_stmt_deps request stmt =
+ match stmt.skind with
+ | Instr (instr) -> compute_instr_deps request instr
+ | If (expr, _, _, _) -> compute_expr_deps request expr
+ | _ -> Base.SetLattice.empty
+
+let compute_marker_deps request = function
+ | Printer_tag.PStmt (_, stmt)
+ | PStmtStart (_, stmt) -> compute_stmt_deps request stmt
+ | PLval (_, _, lval) -> compute_lval_deps request lval
+ | PExp (_, _, expr) -> compute_expr_deps request expr
+ | PVDecl (_, _, vi) -> Base.SetLattice.inject_singleton (Base.of_varinfo vi)
+ | _ -> Base.SetLattice.empty
+
+let get_filtered_state request marker =
+ let bases = compute_marker_deps request marker in
+ match bases with
+ | Base.SetLattice.Top -> Results.print_states request
+ | Base.SetLattice.Set bases ->
+ if Base.Hptset.is_empty bases
+ then []
+ else Results.print_states ~filter:bases request
+
+let get_states marker =
+ let kinstr = Printer_tag.ki_of_localizable marker in
+ match kinstr with
+ | Kglobal -> []
+ | Kstmt stmt ->
+ let states_before = get_filtered_state (Results.before stmt) marker in
+ let states_after = get_filtered_state (Results.after stmt) marker in
+ match states_before, states_after with
+ | [], _ -> List.map (fun (name, after) -> name, "", after) states_after
+ | _, [] -> List.map (fun (name, before) -> name, before, "") states_before
+ | _, _ ->
+ let join (name, before) (name', after) =
+ assert (name = name');
+ name, before, after
+ in
+ List.rev_map2 join states_before states_after
+
+let () = Request.register ~package
+ ~kind:`GET ~name:"getStates"
+ ~descr:(Markdown.plain "Get the domain states about the given marker")
+ ~input:(module Kernel_ast.Marker)
+ ~output:(module Data.Jlist
+ (Data.Jtriple (Data.Jstring) (Data.Jstring) (Data.Jstring)))
+ get_states
diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml
index 540bc32142a..56935b6b228 100644
--- a/src/plugins/value/utils/results.ml
+++ b/src/plugins/value/utils/results.ml
@@ -293,6 +293,26 @@ struct
| Some extract ->
convert (Response.map_join extract Cvalue.Model.join (get req))
+ let print_states ?filter req =
+ let state = Response.map_join (fun x -> x) A.Dom.join (get req) in
+ let print (type s)
+ (key: s Abstract.Domain.key)
+ (module Domain: Abstract_domain.S with type state = s)
+ (state: s) acc =
+ let name = Structure.Key_Domain.name key in
+ let state =
+ match filter with
+ | None -> state
+ | Some bases -> Domain.filter `Print bases state
+ in
+ let str = Format.asprintf "%a" Domain.pretty state in
+ (name, str) :: acc
+ in
+ let polymorphic_fold_fun = A.Dom.{ fold = print } in
+ match state with
+ | `Top | `Bottom -> []
+ | `Value state -> A.Dom.fold polymorphic_fold_fun state []
+
(* Evaluation *)
let eval_lval lval req =
@@ -487,6 +507,10 @@ let get_cvalue_model req =
| Error Bottom -> Cvalue.Model.bottom
| Error (Top | DisabledDomain) -> Cvalue.Model.top
+let print_states ?filter req =
+ let module E = Make () in
+ E.print_states ?filter req
+
(* Depedencies *)
diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli
index e6c0678569a..e18f41a0325 100644
--- a/src/plugins/value/utils/results.mli
+++ b/src/plugins/value/utils/results.mli
@@ -161,6 +161,11 @@ val get_cvalue_model : request -> Cvalue.Model.t
(** Returns the Cvalue model. *)
val get_cvalue_model_result : request -> Cvalue.Model.t result
+(** Returns a textual representation of the internal domain states for the given
+ request. If [filter] is provided, states are filtered on the given bases
+ (for domains that support this feature).
+ Returns a list of pair (name, state) for all available domains. *)
+val print_states: ?filter:Base.Hptset.t -> request -> (string * string) list
(** Dependencies *)
--
GitLab