Revision c1785a55
Added by PierreLoïc Garoche about 6 years ago
src/tools/zustre_verifier.ml  

1  1 
open LustreSpec 
2  2 
open Machine_code 
3  3 
open Format 
4 
open Horn_backend_common 

5 
open Horn_backend 

4 
(* open Horn_backend_common 

5 
* open Horn_backend *) 

6  
7 
module HBC = Horn_backend_common 

8 
let machine_step_name = HBC.machine_step_name 

9 
let node_name = HBC.node_name 

10 
let concat = HBC.concat 

11 
let rename_machine = HBC.rename_machine 

12 
let rename_machine_list = HBC.rename_machine_list 

13 
let rename_next = HBC.rename_next 

14 
let rename_current = HBC.rename_current 

15 
let rename_current_list = HBC.rename_current_list 

16 
let rename_mid_list = HBC.rename_mid_list 

17 
let rename_next_list = HBC.rename_next_list 

18 
let full_memory_vars = HBC.full_memory_vars 

6  19 

7  20 
let active = ref false 
8  21 
let ctx = ref (Z3.mk_context []) 
22 
let machine_reset_name = HBC.machine_reset_name 

23  
24 
(** Sorts 

25  
26 
A sort is introduced for each basic type and each enumerated type. 

9  27  
28 
A hashtbl records these and allow easy access to sort values, when 

29 
provided with a enumerated type name. 

30  
31 
*) 

32 


10  33 
let bool_sort = Z3.Boolean.mk_sort !ctx 
11  34 
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx 
12  35 
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx 
13  36  
14  37 
let const_sorts = Hashtbl.create 13 
15 
let get_const_sort ty_name = 

16 
Hashtbl.find const_sorts ty_name 

38 
let const_tags = Hashtbl.create 13 

39 
let sort_elems = Hashtbl.create 13 

40  
41 
let get_const_sort = Hashtbl.find const_sorts 

42 
let get_sort_elems = Hashtbl.find sort_elems 

43 
let get_tag_sort = Hashtbl.find const_tags 

44 


17  45  
46 


18  47 
let decl_sorts () = 
19  48 
Hashtbl.iter (fun typ decl > 
20  49 
match typ with 
...  ...  
24  53 
match tdef.tydef_desc with 
25  54 
 Tydec_enum tl > 
26  55 
let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in 
27 
Hashtbl.add const_sorts var new_sort 

56 
Hashtbl.add const_sorts var new_sort; 

57 
Hashtbl.add sort_elems new_sort tl; 

58 
List.iter (fun t > Hashtbl.add const_tags t new_sort) tl 

59 


28  60 
 _ > assert false 
29  61 
) 
30  62 
 _ > assert false 
31  63 
) 
32  64 
 _ > ()) Corelang.type_table 
33  65  
34  
66 


35  67 
let rec type_to_sort t = 
36  68 
if Types.is_bool_type t then bool_sort else 
37  69 
if Types.is_int_type t then int_sort else 
...  ...  
45  77 
 _ > Format.eprintf "internal error: pp_type %a@." 
46  78 
Types.print_ty t; assert false 
47  79  
48 


80 
(** Func decls 

81  
82 
Similarly fun_decls are registerd, by their name, into a hashtbl. The 

83 
proposed encoding introduces a 0ary fun_decl to model variables 

84 
and fun_decl with arguments to declare reset and step predicates. 

85  
86  
87  
88 
*) 

89 
let decls = Hashtbl.create 13 

90 
let register_fdecl id fd = Hashtbl.add decls id fd 

91 
let get_fdecl id = Hashtbl.find decls id 

92 


49  93 
let decl_var id = 
50 
Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) 

94 
let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) in 

95 
register_fdecl id.var_id fdecl; 

96 
fdecl 

97  
98 
let decl_rel name args = 

99 
(*verifier ce qui est construit. On veut un declarerel *) 

100 
let args_sorts = List.map (fun v > type_to_sort v.var_type) args in 

101 
let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in 

102 
register_fdecl name fdecl; 

103 
fdecl 

104 


105  
106  
107 
(** conversion functions 

108  
109 
The following is similar to the Horn backend. Each printing function 

110 
is rephrased from pp_xx to xx_to_expr and produces a Z3 value. 

111  
112 
*) 

113  
114  
115 
(* Returns the f_decl associated to the variable v *) 

116 
let horn_var_to_expr v = 

117 
Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id) 

118  
119  
120  
121  
122 
(* Used to print boolean constants *) 

123 
let horn_tag_to_expr t = 

124 
if t = Corelang.tag_true then 

125 
Z3.Boolean.mk_true !ctx 

126 
else if t = Corelang.tag_false then 

127 
Z3.Boolean.mk_false !ctx 

128 
else 

129 
(* Finding the associated sort *) 

130 
let sort = get_tag_sort t in 

131 
let elems = get_sort_elems sort in 

132 
let res : Z3.Expr.expr option = 

133 
List.fold_left2 (fun res cst expr > 

134 
match res with 

135 
 Some _ > res 

136 
 None > if t = cst then Some (expr:Z3.Expr.expr) else None 

137 
) None elems (Z3.Enumeration.get_consts sort) 

138 
in 

139 
match res with None > assert false  Some s > s 

140 


141 
(* Prints a constant value *) 

142 
let rec horn_const_to_expr c = 

143 
match c with 

144 
 Const_int i > Z3.Arithmetic.Integer.mk_numeral_i !ctx i 

145 
 Const_real (_,_,s) > Z3.Arithmetic.Real.mk_numeral_i !ctx 0 

146 
 Const_tag t > horn_tag_to_expr t 

147 
 _ > assert false 

148  
149  
150  
151 
(* Default value for each type, used when building arrays. Eg integer array 

152 
[2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value 

153 
for the type integer (arrays). 

154 
*) 

155 
let rec horn_default_val t = 

156 
let t = Types.dynamic_type t in 

157 
if Types.is_bool_type t then Z3.Boolean.mk_true !ctx else 

158 
if Types.is_int_type t then Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 else 

159 
if Types.is_real_type t then Z3.Arithmetic.Real.mk_numeral_i !ctx 0 else 

160 
(* match (Types.dynamic_type t).Types.tdesc with 

161 
*  Types.Tarray(dim, l) > (\* TODO PL: this strange code has to be (heavily) checked *\) 

162 
* let valt = Types.array_element_type t in 

163 
* fprintf fmt "((as const (Array Int %a)) %a)" 

164 
* pp_type valt 

165 
* pp_default_val valt 

166 
*  Types.Tstruct(l) > assert false 

167 
*  Types.Ttuple(l) > assert false 

168 
* _ > *) assert false 

169  
170  
171 
let horn_basic_app i val_to_expr vl = 

172 
match i, vl with 

173 
 "ite", [v1; v2; v3] > 

174 
Z3.Boolean.mk_ite 

175 
!ctx 

176 
(val_to_expr v1) 

177 
(val_to_expr v2) 

178 
(val_to_expr v3) 

179  
180 
 "uminus", [v] > 

181 
Z3.Arithmetic.mk_unary_minus 

182 
!ctx 

183 
(val_to_expr v) 

184 
 "not", [v] > 

185 
Z3.Boolean.mk_not 

186 
!ctx 

187 
(val_to_expr v) 

188 
 "=", [v1; v2] > 

189 
Z3.Boolean.mk_eq 

190 
!ctx 

191 
(val_to_expr v1) 

192 
(val_to_expr v2) 

193 
 "&&", [v1; v2] > 

194 
Z3.Boolean.mk_and 

195 
!ctx 

196 
[val_to_expr v1; 

197 
val_to_expr v2] 

198 
 "", [v1; v2] > 

199 
Z3.Boolean.mk_or 

200 
!ctx 

201 
[val_to_expr v1; 

202 
val_to_expr v2] 

203  
204 
 "impl", [v1; v2] > 

205 
Z3.Boolean.mk_implies 

206 
!ctx 

207 
(val_to_expr v1) 

208 
(val_to_expr v2) 

209 
 "mod", [v1; v2] > 

210 
Z3.Arithmetic.Integer.mk_mod 

211 
!ctx 

212 
(val_to_expr v1) 

213 
(val_to_expr v2) 

214 
 "equi", [v1; v2] > 

215 
Z3.Boolean.mk_eq 

216 
!ctx 

217 
(val_to_expr v1) 

218 
(val_to_expr v2) 

219 
 "xor", [v1; v2] > 

220 
Z3.Boolean.mk_xor 

221 
!ctx 

222 
(val_to_expr v1) 

223 
(val_to_expr v2) 

224 
 "!=", [v1; v2] > 

225 
Z3.Boolean.mk_not 

226 
!ctx 

227 
( 

228 
Z3.Boolean.mk_eq 

229 
!ctx 

230 
(val_to_expr v1) 

231 
(val_to_expr v2) 

232 
) 

233 
 "/", [v1; v2] > 

234 
Z3.Arithmetic.mk_div 

235 
!ctx 

236 
(val_to_expr v1) 

237 
(val_to_expr v2) 

238  
239 
(*  _, [v1; v2] > Z3.Boolean.mk_and 

240 
* !ctx 

241 
* (val_to_expr v1) 

242 
* (val_to_expr v2) 

243 
* 

244 
* Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *) 

245 
 _ > ( 

246 
Format.eprintf 

247 
"internal error: zustre unkown function %s@." i; 

248 
assert false) 

249  
250 


251 
(* Convert a value expression [v], with internal function calls only. 

252 
[pp_var] is a printer for variables (typically [pp_c_var_read]), 

253 
but an offset suffix may be added for array variables 

254 
*) 

255 
let rec horn_val_to_expr ?(is_lhs=false) self v = 

256 
match v.value_desc with 

257 
 Cst c > horn_const_to_expr c 

258  
259 
(* Code specific for arrays *) 

260 
 Array il > 

261 
(* An array definition: 

262 
(store ( 

263 
... 

264 
(store ( 

265 
store ( 

266 
default_val 

267 
) 

268 
idx_n val_n 

269 
) 

270 
idx_n1 val_n1) 

271 
... 

272 
idx_1 val_1 

273 
) *) 

274 
let rec build_array (tab, x) = 

275 
match tab with 

276 
 [] > horn_default_val v.value_type(* (get_type v) *) 

277 
 h::t > 

278 
Z3.Z3Array.mk_store 

279 
!ctx 

280 
(build_array (t, (x+1))) 

281 
(Z3.Arithmetic.Integer.mk_numeral_i !ctx x) 

282 
(horn_val_to_expr ~is_lhs:is_lhs self h) 

283 
in 

284 
build_array (il, 0) 

285 


286 
 Access(tab,index) > 

287 
Z3.Z3Array.mk_select !ctx 

288 
(horn_val_to_expr ~is_lhs:is_lhs self tab) 

289 
(horn_val_to_expr ~is_lhs:is_lhs self index) 

290  
291 
(* Code specific for arrays *) 

292 


293 
 Power (v, n) > assert false 

294 
 LocalVar v > 

295 
horn_var_to_expr 

296 
(rename_machine 

297 
self 

298 
v) 

299 
 StateVar v > 

300 
if Types.is_array_type v.var_type 

301 
then assert false 

302 
else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) 

303 
 Fun (n, vl) > horn_basic_app n (horn_val_to_expr self) vl 

304  
305 
let no_reset_to_exprs machines m i = 

306 
let (n,_) = List.assoc i m.minstances in 

307 
let target_machine = List.find (fun m > m.mname.node_id = (Corelang.node_name n)) machines in 

51  308  
309 
let m_list = 

310 
rename_machine_list 

311 
(concat m.mname.node_id i) 

312 
(rename_mid_list (full_memory_vars machines target_machine)) 

313 
in 

314 
let c_list = 

315 
rename_machine_list 

316 
(concat m.mname.node_id i) 

317 
(rename_current_list (full_memory_vars machines target_machine)) 

318 
in 

319 
match c_list, m_list with 

320 
 [chd], [mhd] > 

321 
let expr = 

322 
Z3.Boolean.mk_eq !ctx 

323 
(horn_var_to_expr mhd) 

324 
(horn_var_to_expr chd) 

325 
in 

326 
[expr] 

327 
 _ > ( 

328 
let exprs = 

329 
List.map2 (fun mhd chd > 

330 
Z3.Boolean.mk_eq !ctx 

331 
(horn_var_to_expr mhd) 

332 
(horn_var_to_expr chd) 

333 
) 

334 
m_list 

335 
c_list 

336 
in 

337 
exprs 

338 
) 

339  
340 
let instance_reset_to_exprs machines m i = 

341 
let (n,_) = List.assoc i m.minstances in 

342 
let target_machine = List.find (fun m > m.mname.node_id = (Corelang.node_name n)) machines in 

343 
let vars = 

344 
( 

345 
(rename_machine_list 

346 
(concat m.mname.node_id i) 

347 
(rename_current_list (full_memory_vars machines target_machine)) 

348 
) 

349 
@ 

350 
(rename_machine_list 

351 
(concat m.mname.node_id i) 

352 
(rename_mid_list (full_memory_vars machines target_machine)) 

353 
) 

354 
) 

355 
in 

356 
let expr = 

357 
Z3.Expr.mk_app 

358 
!ctx 

359 
(get_fdecl (machine_reset_name (Corelang.node_name n))) 

360 
(List.map (horn_var_to_expr) vars) 

361 
in 

362 
[expr] 

363  
364 
let instance_call_to_exprs machines reset_instances m i inputs outputs = 

365 
let self = m.mname.node_id in 

366 
try (* stateful node instance *) 

367 
begin 

368 
let (n,_) = List.assoc i m.minstances in 

369 
let target_machine = List.find (fun m > m.mname.node_id = Corelang.node_name n) machines in 

370  
371 
(* Checking whether this specific instances has been reset yet *) 

372 
let reset_exprs = 

373 
if not (List.mem i reset_instances) then 

374 
(* If not, declare mem_m = mem_c *) 

375 
no_reset_to_exprs machines m i 

376 
else 

377 
[] (* Nothing to add yet *) 

378 
in 

379 


380 
let mems = full_memory_vars machines target_machine in 

381 
let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in 

382 
let mid_mems = rename_mems rename_mid_list in 

383 
let next_mems = rename_mems rename_next_list in 

384  
385 
let call_expr = 

386 
match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with 

387 
 "_arrow", [i1; i2], [o], [mem_m], [mem_x] > begin 

388 
let stmt1 = (* out = ite mem_m then i1 else i2 *) 

389 
Z3.Boolean.mk_eq !ctx 

390 
( (* output var *) 

391 
horn_val_to_expr 

392 
~is_lhs:true 

393 
self 

394 
(mk_val (LocalVar o) o.var_type) 

395 
) 

396 
( 

397 
Z3.Boolean.mk_ite !ctx 

398 
(horn_var_to_expr mem_m) 

399 
(horn_val_to_expr self i1) 

400 
(horn_val_to_expr self i2) 

401 
) 

402 
in 

403 
let stmt2 = (* mem_X = false *) 

404 
Z3.Boolean.mk_eq !ctx 

405 
(horn_var_to_expr mem_x) 

406 
(Z3.Boolean.mk_false !ctx) 

407 
in 

408 
[stmt1; stmt2] 

409 
end 

410  
411 
 node_name_n > 

412 
let expr = 

413 
Z3.Expr.mk_app 

414 
!ctx 

415 
(get_fdecl (machine_step_name (node_name n))) 

416 
( (* Arguments are input, output, mid_mems, next_mems *) 

417 
( 

418 
List.map (horn_val_to_expr self (pp_horn_var m)) ( 

419 
inputs @ 

420 
(List.map (fun v > mk_val (LocalVar v) v.var_type) outputs) 

421 
) 

422 
) @ ( 

423 
List.map (horn_var_to_expr) (mid_mems@next_mems) 

424 
) 

425 
) 

426 
in 

427 
[expr] 

428 
in 

429  
430 
reset_exprs@call_expr 

431 
end 

432 
with Not_found > ( (* stateless node instance *) 

433 
let (n,_) = List.assoc i m.mcalls in 

434 
let expr = 

435 
Z3.Expr.mk_app 

436 
!ctx 

437 
(get_fdecl (machine_stateless_name (node_name n))) 

438 
((* Arguments are inputs, outputs *) 

439 
List.map (horn_val_to_expr self) 

440 
( 

441 
inputs @ (List.map (fun v > mk_val (LocalVar v) v.var_type) outputs) 

442 
) 

443 
) 

444 
in 

445 
[expr] 

446 
) 

447 


448  
449 
(* Convert instruction to Z3.Expr and update the set of reset instances *) 

450 
let rec instr_to_expr machines reset_instances (m: machine_t) instr : expr list * ident list = 

451 
match get_instr_desc instr with 

452 
 MComment _ > [], reset_instances 

453 
 MNoReset i > (* we assign middle_mem with mem_m. And declare i as reset *) 

454 
no_reset_to_exprs machines m i, 

455 
i::reset_instances 

456 
 MReset i > (* we assign middle_mem with reset: reset(mem_m) *) 

457 
instance_reset_to_exprs machines m i, 

458 
i::reset_instances 

459 
 MLocalAssign (i,v) > 

460 
assign_to_exprs 

461 
m (horn_var_to_expr) 

462 
(mk_val (LocalVar i) i.var_type) v, 

463 
reset_instances 

464 
 MStateAssign (i,v) > 

465 
assign_to_exprs 

466 
m (horn_var_to_expr) 

467 
(mk_val (StateVar i) i.var_type) v, 

468 
reset_instances 

469 
 MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v > v.value_type) vl) > 

470 
assert false (* This should not happen anymore *) 

471 
 MStep (il, i, vl) > 

472 
(* if reset instance, just print the call over mem_m , otherwise declare mem_m = 

473 
mem_c and print the call to mem_m *) 

474 
instance_call_to_exprs machines reset_instances m i vl il, 

475 
reset_instances (* Since this instance call will only happen once, we 

476 
don't have to update reset_instances *) 

477  
478 
 MBranch (g,hl) > (* (g = tag1 => expr1) and (g = tag2 => expr2) ... 

479 
should not be produced yet. Later, we will have to 

480 
compare the reset_instances of each branch and 

481 
introduced the mem_m = mem_c for branches to do not 

482 
address it while other did. Am I clear ? *) 

483 
(* For each branch we obtain the logical encoding, and the information 

484 
whether a sub node has been reset or not. If a node has been reset in one 

485 
of the branch, then all others have to have the mem_m = mem_c 

486 
statement. *) 

487 
let self = m.mname.node_id in 

488 
let branch_to_expr (tag, instrs) = 

489 
Z3.Boolean.mk_implies 

490 
(Z3.Boolean.mk_eq !ctx 

491 
(horn_val_to_expr self g) 

492 
(horn_tag_to_expr tag)) 

493 
(machine_instrs_to_exprs machines reset_instances m instrs) 

494 
in 

495 
List.map branch_to_expr hl, 

496 
reset_instances 

497  
498 
and instrs_to_expr machines reset_instances m instrs = 

499 
let instr_to_expr rs i = instr_to_expr machines rs m i in 

500 
match instrs with 

501 
 [x] > instr_to_expres reset_instances x 

502 
 _::_ > (* TODO: check whether we should compuyte a AND on the exprs (expr list) built here. It was performed in the printer setting but seems to be useless here since the output is a list of exprs *) 

503  
504 
List.fold_left (fun (exprs, rs) i > 

505 
let exprs_i, rs = ppi rs i in 

506 
expr@exprs_i, rs 

507 
) 

508 
([], reset_instances) instrs 

509 


510 


511 
 [] > [], reset_instances 

512  
513  
514 
(* TODO: empty list means true statement *) 

52  515 
let decl_machine machines m = 
53  516 
if m.Machine_code.mname.node_id = Machine_code.arrow_id then 
54  517 
(* We don't print arrow function *) 
55  518 
() 
56  519 
else 
57  520 
begin 
58 
let _ = List.map decl_var 

59 
( 

60 
(inout_vars machines m)@ 

61 
(rename_current_list (full_memory_vars machines m)) @ 

62 
(rename_mid_list (full_memory_vars machines m)) @ 

63 
(rename_next_list (full_memory_vars machines m)) @ 

64 
(rename_machine_list m.mname.node_id m.mstep.step_locals) 

65 
) 

521 
let vars = 

522 
List.map decl_var 

523 
( 

524 
(inout_vars machines m)@ 

525 
(rename_current_list (full_memory_vars machines m)) @ 

526 
(rename_mid_list (full_memory_vars machines m)) @ 

527 
(rename_next_list (full_memory_vars machines m)) @ 

528 
(rename_machine_list m.mname.node_id m.mstep.step_locals) 

529 
) 

66  530 
in 
67 
() 

68 
(* 

531 


69  532 
if is_stateless m then 
70  533 
begin 
71  534 
(* Declaring single predicate *) 
72 
fprintf fmt "(declarerel %a (%a))@." 

73 
pp_machine_stateless_name m.mname.node_id 

74 
(Utils.fprintf_list ~sep:" " pp_type) 

75 
(List.map (fun v > v.var_type) (inout_vars machines m)); 

76  
535 
let _ = decl_rel (machine_stateless_name m.mname.node_id) (inout_vars machines m) in 

77  536 
match m.mstep.step_asserts with 
78  537 
 [] > 
79  538 
begin 
...  ...  
84  543 
ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) ) m fmt m.mstep.step_instrs); 
85  544 
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." 
86  545 
pp_machine_stateless_name m.mname.node_id 
87 
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars machines m);


546 
(Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (inout_vars machines m);


88  547 
end 
89  548 
 assertsl > 
90  549 
begin 
91 
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in


550 
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (horn_var_to_expr) in


92  551 

93  552 
fprintf fmt "; Stateless step rule with Assertions @."; 
94  553 
(*Rule for step*) 
...  ...  
96  555 
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); 
97  556 
fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl 
98  557 
pp_machine_stateless_name m.mname.node_id 
99 
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);


558 
(Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (step_vars machines m);


100  559 

101  560 
end 
102  561 

...  ...  
104  563 
else 
105  564 
begin 
106  565 
(* Declaring predicate *) 
107 
fprintf fmt "(declarerel %a (%a))@." 

108 
pp_machine_reset_name m.mname.node_id 

109 
(Utils.fprintf_list ~sep:" " pp_type) 

110 
(List.map (fun v > v.var_type) (reset_vars machines m)); 

111  
112 
fprintf fmt "(declarerel %a (%a))@." 

113 
pp_machine_step_name m.mname.node_id 

114 
(Utils.fprintf_list ~sep:" " pp_type) 

115 
(List.map (fun v > v.var_type) (step_vars machines m)); 

116  
117 
pp_print_newline fmt (); 

566 
let _ = decl_rel (machine_reset_name m.mname.node_id) (reset_vars machines m) in 

567 
let _ = decl_rel (machine_step_name m.mname.node_id) (step_vars machines m) in 

118  568  
119  569 
(* Rule for reset *) 
120  570 
fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@." 
121  571 
(pp_machine_reset machines) m 
122  572 
pp_machine_reset_name m.mname.node_id 
123 
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m);


573 
(Utils.fprintf_list ~sep:"@ " (horn_var_to_expr)) (reset_vars machines m);


124  574  
125  575 
match m.mstep.step_asserts with 
126  576 
 [] > 
...  ...  
131  581 
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); 
132  582 
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." 
133  583 
pp_machine_step_name m.mname.node_id 
134 
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);


584 
(Utils.fprintf_list ~sep:"@ " (horn_var_to_expr)) (step_vars machines m);


135  585 
end 
136  586 
 assertsl > 
137  587 
begin 
138 
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in


588 
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (horn_var_to_expr) in


139  589 
(* print_string pp_val; *) 
140  590 
fprintf fmt "; Step rule with Assertions @."; 
141  591 

...  ...  
144  594 
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); 
145  595 
fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl 
146  596 
pp_machine_step_name m.mname.node_id 
147 
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);


597 
(Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (step_vars machines m);


148  598 
end 
149  599 

150  600 

151  601 
end 
152 
*) end


602 
end 

153  603  
154 


604 
let param_stat = ref false 

605 
let param_eldarica = ref false 

606 
let param_utvpi = ref false 

607 
let param_tosmt = ref false 

608 
let param_pp = ref false 

609 


155  610 
module Verifier = 
156  611 
(struct 
157  612 
include VerifierType.Default 
158  613 
let name = "zustre" 
159 
let options = [] 

614 
let options = [ 

615 
"stat", Arg.Set param_stat, "print statistics"; 

616 
"eldarica", Arg.Set param_eldarica, "deactivate fixedpoint extensions when printing rules"; 

617 
"no_utvpi", Arg.Set param_utvpi, "Deactivate UTVPI strategy"; 

618 
"tosmt", Arg.Set param_tosmt, "Print lowlevel (possibly unreadable) SMT2 statements"; 

619 
"nopp", Arg.Set param_pp, "No preprocessing (inlining and slicing)"; 

620 
] 

621 


160  622 
let activate () = ( 
161  623 
active := true; 
162  624 
Options.output := "horn"; 
...  ...  
168  630 
assert(!Options.output = "horn"); 
169  631 
Backends.get_normalization_params () 
170  632  
633 
let setup_solver () = 

634 
let fp = Z3.Fixedpoint.mk_fixedpoint !ctx in 

635 
(* let help = Z3.Fixedpoint.get_help fp in 

636 
* Format.eprintf "Fp help : %s@." help; 

637 
* 

638 
* let solver =Z3.Solver.mk_solver !ctx None in 

639 
* let help = Z3.Solver.get_help solver in 

640 
* Format.eprintf "Z3 help : %s@." help; *) 

641 


642 
let module P = Z3.Params in 

643 
let module S = Z3.Symbol in 

644 
let mks = S.mk_string !ctx in 

645 
let params = P.mk_params !ctx in 

646  
647 
(* self.fp.set (engine='spacer') *) 

648 
P.add_symbol params (mks "engine") (mks "spacer"); 

649 


650 
(* #z3.set_option(rational_to_decimal=True) *) 

651 
(* #self.fp.set('precision',30) *) 

652 
if !param_stat then 

653 
(* self.fp.set('print_statistics',True) *) 

654 
P.add_bool params (mks "print_statistics") true; 

655  
656 
(* Dont know where to find this parameter *) 

657 
(* if !param_spacer_verbose then 

658 
* if self.args.spacer_verbose: 

659 
* z3.set_option (verbose=1) *) 

660  
661 
(* The option is not recogined*) 

662 
(* self.fp.set('use_heavy_mev',True) *) 

663 
(* P.add_bool params (mks "use_heavy_mev") true; *) 

664 


665 
(* self.fp.set('pdr.flexible_trace',True) *) 

666 
P.add_bool params (mks "pdr.flexible_trace") true; 

667  
668 
(* self.fp.set('reset_obligation_queue',False) *) 

669 
P.add_bool params (mks "spacer.reset_obligation_queue") false; 

670  
671 
(* self.fp.set('spacer.elim_aux',False) *) 

672 
P.add_bool params (mks "spacer.elim_aux") false; 

673  
674 
(* if self.args.eldarica: 

675 
* self.fp.set('print_fixedpoint_extensions', False) *) 

676 
if !param_eldarica then 

677 
P.add_bool params (mks "print_fixedpoint_extensions") false; 

678 


679 
(* if self.args.utvpi: self.fp.set('pdr.utvpi', False) *) 

680 
if !param_utvpi then 

681 
P.add_bool params (mks "pdr.utvpi") false; 

682  
683 
(* if self.args.tosmt: 

684 
* self.log.info("Setting low level printing") 

685 
* self.fp.set ('print.low_level_smt2',True) *) 

686 
if !param_tosmt then 

687 
P.add_bool params (mks "print.low_level_smt2") true; 

688  
689 
(* if not self.args.pp: 

690 
* self.log.info("No preprocessing") 

691 
* self.fp.set ('xform.slice', False) 

692 
* self.fp.set ('xform.inline_linear',False) 

693 
* self.fp.set ('xform.inline_eager',False) *\) *) 

694 
if !param_pp then ( 

695 
P.add_bool params (mks "xform.slice") false; 

696 
P.add_bool params (mks "xform.inline_linear") false; 

697 
P.add_bool params (mks "xform.inline_eager") false 

698 
); 

699 
Z3.Fixedpoint.set_parameters fp params 

700 


701 


171  702 
let run basename prog machines = 
172  703 
let machines = Machine_code.arrow_machine::machines in 
173  704 
let machines = preprocess machines in 
705 
setup_solver (); 

174  706 
decl_sorts (); 
175  707 
List.iter (decl_machine machines) (List.rev machines); 
176  708 
Also available in: Unified diff
ongoing work on zustre backend