Source file `analysis_requests.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

open Server
open Cil_types

let package =
  let title = "Eva Analysis" in
  Package.package ~plugin:"eva" ~name:"analysis" ~title ()


(* ----- Computation state -------------------------------------------------- *)

module ComputationState = struct
  type t = Self.computation_state
  let jtype =
    Data.declare ~package
      ~name:"computationStateType"
      ~descr:(Markdown.plain "State of the computation of Eva Analysis.")
      Package.(Junion [
          Jtag "not_computed" ;
          Jtag "computing" ;
          Jtag "computed" ;
          Jtag "aborted" ])
  let to_json = function
    | Self.NotComputed -> `String "not_computed"
    | Computing -> `String "computing"
    | Computed -> `String "computed"
    | Aborted -> `String "aborted"
end

let _signal =
  States.register_framac_value ~package
    ~name:"computationState"
    ~descr:(Markdown.plain "The current computation state of the analysis.")
    ~output:(module ComputationState)
    (module Self.ComputationState)

let () = Request.register ~package
    ~kind:`EXEC
    ~name:"compute"
    ~descr:(Markdown.plain "run eva analysis")
    ~input:(module Data.Junit)
    ~output:(module Data.Junit)
    Analysis.compute

let () = Request.register ~package
    ~kind:`GET (* able to interrupt the EXEC compute request *)
    ~name:"abort"
    ~descr:(Markdown.plain "abort eva analysis")
    ~input:(module Data.Junit)
    ~output:(module Data.Junit)
    Analysis.abort

let clear () =
  if Self.ComputationState.get () <> Computing then
    begin
      Self.clear_results ();
      Emitter.clear Eva_utils.emitter;
      Emitter.clear Eva_utils.export_emitter;
    end

let () = Request.register ~package
    ~kind:`SET
    ~name:"clear"
    ~descr:(Markdown.plain "removes all results from previous Eva analyses, \
                            including emitted alarms, annotations and statuses")
    ~input:(module Data.Junit)
    ~output:(module Data.Junit)
    clear


(* ----- Domains states ----------------------------------------------------- *)

let compute_lval_deps request lval =
  let zone = Results.lval_deps lval request in
  Memory_zone.get_bases zone

let compute_expr_deps request expr =
  let zone = Results.expr_deps expr request in
  Memory_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_state filter request marker =
  if filter
  then get_filtered_state request marker
  else Results.print_states request

let get_states (marker, filter) =
  let kinstr = Printer_tag.ki_of_localizable marker in
  match kinstr with
  | Kglobal -> []
  | Kstmt stmt ->
    let states_before = get_state filter (Results.before stmt) marker in
    let states_after = get_state filter (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 Data.Jpair (Kernel_ast.Marker) (Data.Jbool))
    ~output:(module Data.Jlist
          (Data.Jtriple (Data.Jstring) (Data.Jstring) (Data.Jstring)))
    ~signals:Update.signals
    get_states