[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.

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;
+
 /* ------------------------------------- */

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

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 *)
 

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 *)