Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/tools/zustre/zustre_verifier.ml | ||
---|---|---|
1 |
|
|
2 | 1 |
(* |
3 | 2 |
TODO |
4 | 3 |
|
... | ... | |
34 | 33 |
|
35 | 34 |
*) |
36 | 35 |
|
37 |
|
|
38 | 36 |
open Zustre_common |
39 | 37 |
open Zustre_data |
40 | 38 |
|
41 | 39 |
let param_stat = ref false |
40 |
|
|
42 | 41 |
let param_eldarica = ref false |
42 |
|
|
43 | 43 |
let param_utvpi = ref false |
44 |
|
|
44 | 45 |
let param_tosmt = ref false |
46 |
|
|
45 | 47 |
let param_pp = ref false |
46 | 48 |
|
47 | 49 |
let active = ref false |
48 | 50 |
|
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 |
|
|
239 |
( |
|
240 |
|
|
241 |
|
|
242 |
decl_sorts (); |
|
243 |
|
|
244 |
List.iter (decl_machine machines) (List.rev machines); |
|
245 |
|
|
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 |
|
|
254 |
if !Options.main_node <> "" then |
|
255 |
begin |
|
256 |
Zustre_analyze.check machines !Options.main_node |
|
257 |
|
|
258 |
end |
|
259 |
else |
|
260 |
failwith "Require main node"; |
|
261 |
|
|
262 |
() |
|
263 |
) |
|
264 |
|
|
265 |
|
|
266 |
end: VerifierType.S) |
|
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"; |
|
267 | 256 |
|
257 |
() |
|
258 |
end |
|
268 | 259 |
|
269 | 260 |
let () = |
270 |
VerifierList.registered := (module Verifier : VerifierType.S) ::
|
|
271 |
!VerifierList.registered
|
|
261 |
VerifierList.registered := |
|
262 |
(module Verifier : VerifierType.S) :: !VerifierList.registered
|
|
272 | 263 |
|
273 | 264 |
(* Local Variables: *) |
274 | 265 |
(* compile-command:"make -C ../.. lustrev" *) |
Also available in: Unified diff
reformatting