Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / zustre / zustre_verifier.ml @ 57d61d67

History | View | Annotate | Download (8.28 KB)

1

    
2
(*
3
TODO
4

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

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

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

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

    
35
*)
36

    
37

    
38
open Zustre_common
39
open Zustre_data
40

    
41
let param_stat = ref false
42
let param_eldarica = ref false
43
let param_utvpi = ref false
44
let param_tosmt = ref false
45
let param_pp = ref false
46

    
47
let active = ref false
48

    
49
module Verifier =
50
  (struct
51
    include VerifierType.Default
52
    let name = "zustre"
53
    let options = [
54
        "-stat", Arg.Set param_stat, "print statistics";
55
        "-eldarica", Arg.Set param_eldarica, "deactivate fixedpoint extensions when printing rules";
56
        "-no_utvpi", Arg.Set param_utvpi, "Deactivate UTVPI strategy";
57
        "-tosmt", Arg.Set param_tosmt, "Print low-level (possibly unreadable) SMT2 statements";
58
        "-timeout", Arg.Set_int timeout, "Set timeout in ms (default 10000 = 10 s)";
59
        "-no-pp", Arg.Set param_pp, "No preprocessing (inlining and slicing)";
60
        "-debug", Arg.Set debug, "Debug mode";
61
      ]
62
                
63
    let activate () = (
64
        active := true;
65
        Options.output := "horn";
66
      )
67

    
68
    let is_active () = !active
69

    
70
    let get_normalization_params () =
71
      (* make sure the output is "Horn" *)
72
      assert(!Options.output = "horn");
73
      Backends.get_normalization_params ()
74

    
75
    let setup_solver () =
76
      fp := Z3.Fixedpoint.mk_fixedpoint !ctx;
77
      (* let help = Z3.Fixedpoint.get_help fp in
78
       * Format.eprintf "Fp help : %s@." help;
79
       * 
80
       * let solver =Z3.Solver.mk_solver !ctx None in
81
       * let help = Z3.Solver.get_help solver in
82
       * Format.eprintf "Z3 help : %s@." help; *)
83

    
84
      let module P = Z3.Params in
85
      let module S = Z3.Symbol in
86
      let mks = S.mk_string !ctx in
87
      
88
      (* Fixpoint Engine parameters *)
89
      
90
      let fp_params = P.mk_params !ctx in
91

    
92
      (* (\* self.fp.set (engine='spacer') *\) *)
93
      P.add_symbol fp_params (mks "engine") (mks "spacer");
94
      (* P.add_symbol fp_params (mks "engine") (mks "pdr");  *)
95
      
96
       (* #z3.set_option(rational_to_decimal=True) *)
97
       (* #self.fp.set('precision',30) *)
98
      if !param_stat then 
99
        (* self.fp.set('print_statistics',True) *)
100
        P.add_bool fp_params (mks "print_statistics") true;
101

    
102
      (* Dont know where to find this parameter *)
103
      (* if !param_spacer_verbose then
104
         *   if self.args.spacer_verbose: 
105
         *        z3.set_option (verbose=1) *)
106

    
107
      (* The option is not recogined*)
108
      (* self.fp.set('use_heavy_mev',True) *)
109
      (* P.add_bool fp_params (mks "use_heavy_mev") true; *)
110
      
111
      (* self.fp.set('pdr.flexible_trace',True) *)
112
      P.add_bool fp_params (mks "pdr.flexible_trace") true;
113

    
114
      (* self.fp.set('reset_obligation_queue',False) *)
115
      P.add_bool fp_params (mks "spacer.reset_obligation_queue") false;
116

    
117
      (* self.fp.set('spacer.elim_aux',False) *)
118
      P.add_bool fp_params (mks "spacer.elim_aux") false;
119

    
120
      (* if self.args.eldarica:
121
        *     self.fp.set('print_fixedpoint_extensions', False) *)
122
      if !param_eldarica then
123
        P.add_bool fp_params (mks "print_fixedpoint_extensions") false;
124
      
125
      (* if self.args.utvpi: self.fp.set('pdr.utvpi', False) *)
126
      if !param_utvpi then
127
        P.add_bool fp_params (mks "pdr.utvpi") false;
128

    
129
      (* if self.args.tosmt:
130
       *        self.log.info("Setting low level printing")
131
       *        self.fp.set ('print.low_level_smt2',True) *)
132
      if !param_tosmt then
133
        P.add_bool fp_params (mks "print.low_level_smt2") true;
134

    
135
      (* if not self.args.pp:
136
       *        self.log.info("No pre-processing")
137
       *        self.fp.set ('xform.slice', False)
138
       *        self.fp.set ('xform.inline_linear',False)
139
       *        self.fp.set ('xform.inline_eager',False) *\) *)
140
      if not !param_pp then (
141
	(* Mandatory to print all steps and recover cex *)
142
        P.add_bool fp_params (mks "xform.slice") false;
143
        P.add_bool fp_params (mks "xform.inline_linear") false;
144
        P.add_bool fp_params (mks "xform.inline_eager") false
145
      );
146

    
147

    
148
      (* Ploc's options. Do not seem to have any effect yet *)
149
      P.add_bool fp_params (mks "print_answer") true;
150
      (* P.add_bool fp_params (mks "print_certificate") true; *)
151
      P.add_bool fp_params (mks "xform.slice") false ; (* required to preserve signatures *)
152

    
153
      (* P.add_bool fp_params (mks "print_statistics") true; *)
154
      (* P.add_bool fp_params (mks "print_certificate") true;  *)
155

    
156
      (* Adding a timeout *)
157
      P.add_int fp_params (mks "timeout") !timeout;
158

    
159
      Z3.Fixedpoint.set_parameters !fp fp_params
160
      
161
    let run basename prog machines =
162
      let machines = Machine_code_common.arrow_machine::machines in
163
      let machines = preprocess machines in
164
      setup_solver ();
165

    
166

    
167
      (* TODO
168
	 load deps: cf print_dep in horn_backend.ml
169

    
170
      *)
171
      if false then (
172
	
173
	let queries = Z3.Fixedpoint.parse_file !fp "nstep.smt2" in
174

    
175
	(* Debug instructions *)
176
	
177

    
178
	
179
	let rules_expr = Z3.Fixedpoint.get_rules !fp in
180
	Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
181
      	  (Utils.fprintf_list ~sep:"@ "
182
      	     (fun fmt e ->
183
	       (* let e2 = Z3.Quantifier.get_body eq in *)
184
	       (* let fd = Z3.Expr.get_func_decl e in *)
185
	       Format.fprintf fmt "Rule: %s@."
186
		 (Z3.Expr.to_string e);
187
	     )) rules_expr;
188
	
189
	let _ = List.map extract_expr_fds rules_expr in
190
	Format.eprintf "%t" pp_fdecls;
191

    
192
	let decl_err = List.hd queries in
193
      	let res_status = Z3.Fixedpoint.query !fp decl_err in
194
	
195
	Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status);
196
	(* let _ =  *)
197
	(*   match res_status with *)
198
	(*   | Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex machine machines decl_err *)
199
	(*   | _ -> () *)
200
	(* in *)
201
	exit 0
202
      )
203
      else if false then (
204

    
205
	(* No queries here *)
206
	let _ = Z3.Fixedpoint.parse_file !fp "mini_decl.smt2" in
207

    
208
	(* Debug instructions *)
209
	
210

    
211
	
212
	let rules_expr = Z3.Fixedpoint.get_rules !fp in
213
	Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
214
      	  (Utils.fprintf_list ~sep:"@ "
215
      	     (fun fmt e ->
216
	       (* let e2 = Z3.Quantifier.get_body eq in *)
217
	       (* let fd = Z3.Expr.get_func_decl e in *)
218
	       Format.fprintf fmt "Rule: %s@."
219
		 (Z3.Expr.to_string e);
220
	     )) rules_expr;
221
	
222
	let _ = List.map extract_expr_fds rules_expr in
223
	Format.eprintf "%t" pp_fdecls;
224

    
225
	if !Options.main_node <> "" then
226
      	  begin
227
      	    Zustre_analyze.check machines !Options.main_node
228

    
229
      	  end
230
	else
231
      	  failwith "Require main node";
232

    
233
	()	
234
      )
235
      else (
236
	
237
	
238
	decl_sorts ();
239
	
240
	List.iter (decl_machine machines) (List.rev machines);
241

    
242

    
243
	(* (\* Debug instructions *\) *)
244
	(* let rules_expr = Z3.Fixedpoint.get_rules !fp in *)
245
	(* Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." *)
246
	(* 	(Utils.fprintf_list ~sep:"@ " *)
247
	(* 	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *)
248
	(* 	rules_expr; *)
249

    
250
	if !Options.main_node <> "" then
251
      	  begin
252
      	    Zustre_analyze.check machines !Options.main_node
253

    
254
      	  end
255
	else
256
      	  failwith "Require main node";
257
	
258
	()
259
      )
260
	
261

    
262
	    end: VerifierType.S)
263
    
264
(* Local Variables: *)
265
(* compile-command:"make -C ../.. lustrev" *)
266
(* End: *)