Project

General

Profile

Download (8.43 KB) Statistics
| Branch: | Tag: | Revision:
1
(*
2
TODO
3

    
4
A property/contract is attached to a node foo and could be analyzed
5
- while considering the exact semantics
6
- while substituting some callee by their definition (doing it incrementaly ?)
7
- the returned cex could be given at node level
8
- or while considering a main node and producing the output at the main node level
9

    
10
One can consider the following algorithm:
11
- main node foo, local node bar, with a target property/contract
12
- declare bar using only the contract of its subnodes (callee)
13
- if the property is valid, 
14
  - check the validity status of the subnode contracts used
15
    - if one is not proved, perform the analysis again (of bar contract) using
16
      the actual definition of the unproven contract
17
  - return the computed invariants with the dependencies (subcontracts assumed, subcontracts proved)
18
- if the property is invalid
19
  - check invalidity wrt to full definition of the node bar (with the actual definition of its subnodes)
20
  - return the cex
21
  - try to see if the cex (or a similar violation of the contract) is reachable from its parents 
22
    (up to main node foo)
23
    
24

    
25
Other features:
26
- check equivalence btw two nodes, provided an equivalence map on some callee
27
  (A equiv B) with map (A id equiv B id) 
28
  - substitute each callee appearing B nodes 
29

    
30
Analysis:
31
  - take a main definition, a boolean proposition, and build the collecting semantics
32
  - then check that the proposition remains valid
33

    
34
*)
35

    
36
open Zustre_common
37
open Zustre_data
38

    
39
let param_stat = ref false
40

    
41
let param_eldarica = ref false
42

    
43
let param_utvpi = ref false
44

    
45
let param_tosmt = ref false
46

    
47
let param_pp = ref false
48

    
49
let active = ref false
50

    
51
module Verifier : VerifierType.S = struct
52
  include VerifierType.Default
53

    
54
  let name = "zustre"
55

    
56
  let options =
57
    [
58
      "-stat", Arg.Set param_stat, "print statistics";
59
      ( "-eldarica",
60
        Arg.Set param_eldarica,
61
        "deactivate fixedpoint extensions when printing rules" );
62
      "-no_utvpi", Arg.Set param_utvpi, "Deactivate UTVPI strategy";
63
      ( "-tosmt",
64
        Arg.Set param_tosmt,
65
        "Print low-level (possibly unreadable) SMT2 statements" );
66
      ( "-timeout",
67
        Arg.Set_int timeout,
68
        "Set timeout in ms (default 10000 = 10 s)" );
69
      "-no-pp", Arg.Set param_pp, "No preprocessing (inlining and slicing)";
70
      "-debug", Arg.Set debug, "Debug mode";
71
    ]
72

    
73
  let activate () =
74
    active := true;
75
    Options.output := "horn"
76

    
77
  let is_active () = !active
78

    
79
  let get_normalization_params () =
80
    (* make sure the output is "Horn" *)
81
    assert (!Options.output = "horn");
82
    Backends.get_normalization_params ()
83

    
84
  let setup_solver () =
85
    fp := Z3.Fixedpoint.mk_fixedpoint !ctx;
86

    
87
    (* let help = Z3.Fixedpoint.get_help fp in
88
     * Format.eprintf "Fp help : %s@." help;
89
     * 
90
     * let solver =Z3.Solver.mk_solver !ctx None in
91
     * let help = Z3.Solver.get_help solver in
92
     * Format.eprintf "Z3 help : %s@." help; *)
93
    let module P = Z3.Params in
94
    let module S = Z3.Symbol in
95
    let mks = S.mk_string !ctx in
96

    
97
    (* Fixpoint Engine parameters *)
98
    let fp_params = P.mk_params !ctx in
99

    
100
    (* (\* self.fp.set (engine='spacer') *\) *)
101
    P.add_symbol fp_params (mks "engine") (mks "spacer");
102

    
103
    (* P.add_symbol fp_params (mks "engine") (mks "pdr");  *)
104

    
105
    (* #z3.set_option(rational_to_decimal=True) *)
106
    (* #self.fp.set('precision',30) *)
107
    if !param_stat then
108
      (* self.fp.set('print_statistics',True) *)
109
      P.add_bool fp_params (mks "print_statistics") true;
110

    
111
    (* Dont know where to find this parameter *)
112
    (* if !param_spacer_verbose then
113
       *   if self.args.spacer_verbose:
114
       *        z3.set_option (verbose=1) *)
115

    
116
    (* The option is not recogined*)
117
    (* self.fp.set('use_heavy_mev',True) *)
118
    (* P.add_bool fp_params (mks "use_heavy_mev") true; *)
119

    
120
    (* self.fp.set('pdr.flexible_trace',True) *)
121
    P.add_bool fp_params (mks "pdr.flexible_trace") true;
122

    
123
    (* self.fp.set('reset_obligation_queue',False) *)
124
    P.add_bool fp_params (mks "spacer.reset_obligation_queue") false;
125

    
126
    (* self.fp.set('spacer.elim_aux',False) *)
127
    P.add_bool fp_params (mks "spacer.elim_aux") false;
128

    
129
    (* if self.args.eldarica:
130
       *     self.fp.set('print_fixedpoint_extensions', False) *)
131
    if !param_eldarica then
132
      P.add_bool fp_params (mks "print_fixedpoint_extensions") false;
133

    
134
    (* if self.args.utvpi: self.fp.set('pdr.utvpi', False) *)
135
    if !param_utvpi then P.add_bool fp_params (mks "pdr.utvpi") false;
136

    
137
    (* if self.args.tosmt:
138
     *        self.log.info("Setting low level printing")
139
     *        self.fp.set ('print.low_level_smt2',True) *)
140
    if !param_tosmt then P.add_bool fp_params (mks "print.low_level_smt2") true;
141

    
142
    (* if not self.args.pp:
143
     *        self.log.info("No pre-processing")
144
     *        self.fp.set ('xform.slice', False)
145
     *        self.fp.set ('xform.inline_linear',False)
146
     *        self.fp.set ('xform.inline_eager',False) *\) *)
147
    if not !param_pp then (
148
      (* Mandatory to print all steps and recover cex *)
149
      P.add_bool fp_params (mks "xform.slice") false;
150
      P.add_bool fp_params (mks "xform.inline_linear") false;
151
      P.add_bool fp_params (mks "xform.inline_eager") false);
152

    
153
    (* Ploc's options. Do not seem to have any effect yet *)
154
    P.add_bool fp_params (mks "print_answer") true;
155
    (* P.add_bool fp_params (mks "print_certificate") true; *)
156
    P.add_bool fp_params (mks "xform.slice") false;
157

    
158
    (* required to preserve signatures *)
159

    
160
    (* P.add_bool fp_params (mks "print_statistics") true; *)
161
    (* P.add_bool fp_params (mks "print_certificate") true;  *)
162

    
163
    (* Adding a timeout *)
164
    P.add_int fp_params (mks "timeout") !timeout;
165

    
166
    Z3.Fixedpoint.set_parameters !fp fp_params
167

    
168
  let run ~basename _prog machines =
169
    let machines = Machine_code_common.arrow_machine :: machines in
170
    let machines = preprocess machines in
171
    setup_solver ();
172

    
173
    (* TODO
174
        load deps: cf print_dep in horn_backend.ml
175

    
176

    
177
            if false then (
178

    
179
       let queries = Z3.Fixedpoint.parse_file !fp "nstep.smt2" in
180

    
181
       (* Debug instructions *)
182

    
183

    
184

    
185
       let rules_expr = Z3.Fixedpoint.get_rules !fp in
186
       Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
187
            	  (Utils.fprintf_list ~sep:"@ "
188
            	     (fun fmt e ->
189
              (* let e2 = Z3.Quantifier.get_body eq in *)
190
              (* let fd = Z3.Expr.get_func_decl e in *)
191
              Format.fprintf fmt "Rule: %s@."
192
       	 (Z3.Expr.to_string e);
193
            )) rules_expr;
194

    
195
       let _ = List.map extract_expr_fds rules_expr in
196
       Format.eprintf "%t" pp_fdecls;
197

    
198
       let decl_err = List.hd queries in
199
            	let res_status = Z3.Fixedpoint.query !fp decl_err in
200

    
201
       Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status);
202
       (* let _ =  *)
203
       (*   match res_status with *)
204
       (*   | Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex machine machines decl_err *)
205
       (*   | _ -> () *)
206
       (* in *)
207
       exit 0
208
            )
209
            else if false then (
210

    
211
       (* No queries here *)
212
       let _ = Z3.Fixedpoint.parse_file !fp "mini_decl.smt2" in
213

    
214
       (* Debug instructions *)
215

    
216

    
217

    
218
       let rules_expr = Z3.Fixedpoint.get_rules !fp in
219
       Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
220
            	  (Utils.fprintf_list ~sep:"@ "
221
            	     (fun fmt e ->
222
              (* let e2 = Z3.Quantifier.get_body eq in *)
223
              (* let fd = Z3.Expr.get_func_decl e in *)
224
              Format.fprintf fmt "Rule: %s@."
225
       	 (Z3.Expr.to_string e);
226
            )) rules_expr;
227

    
228
       let _ = List.map extract_expr_fds rules_expr in
229
       Format.eprintf "%t" pp_fdecls;
230

    
231
       if !Options.main_node <> "" then
232
            	  begin
233
            	    Zustre_analyze.check machines !Options.main_node
234

    
235
            	  end
236
       else
237
            	  failwith "Require main node";
238

    
239
       ()
240
            )
241
            else
242
    *)
243
    decl_sorts ();
244

    
245
    List.iter (decl_machine machines) (List.rev machines);
246

    
247
    (* (\* Debug instructions *\) *)
248
    (* let rules_expr = Z3.Fixedpoint.get_rules !fp in *)
249
    (* Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." *)
250
    (* 	(Utils.fprintf_list ~sep:"@ " *)
251
    (* 	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *)
252
    (* 	rules_expr; *)
253
    if !Options.main_node <> "" then
254
      Zustre_analyze.check machines !Options.main_node
255
    else failwith "Require main node";
256

    
257
    ()
258
end
259

    
260
let () =
261
  VerifierList.registered :=
262
    (module Verifier : VerifierType.S) :: !VerifierList.registered
263

    
264
(* Local Variables: *)
265
(* compile-command:"make -C ../.. lustrev" *)
266
(* End: *)
(7-7/7)