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