1

open LustreSpec

2

open Machine_code

3

open Format

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

19


20

let active = ref false

21

let ctx = ref (Z3.mk_context [])

22

let machine_reset_name = HBC.machine_reset_name

23

let machine_stateless_name = HBC.machine_stateless_name

24


25

(** Sorts

26


27

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

28


29

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

30

provided with a enumerated type name.

31


32

*)

33


34

let bool_sort = Z3.Boolean.mk_sort !ctx

35

let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx

36

let real_sort = Z3.Arithmetic.Real.mk_sort !ctx

37


38

let const_sorts = Hashtbl.create 13

39

let const_tags = Hashtbl.create 13

40

let sort_elems = Hashtbl.create 13

41


42

let get_const_sort = Hashtbl.find const_sorts

43

let get_sort_elems = Hashtbl.find sort_elems

44

let get_tag_sort = Hashtbl.find const_tags

45


46


47


48

let decl_sorts () =

49

Hashtbl.iter (fun typ decl >

50

match typ with

51

 Tydec_const var >

52

(match decl.top_decl_desc with

53

 TypeDef tdef > (

54

match tdef.tydef_desc with

55

 Tydec_enum tl >

56

let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in

57

Hashtbl.add const_sorts var new_sort;

58

Hashtbl.add sort_elems new_sort tl;

59

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

60


61

 _ > assert false

62

)

63

 _ > assert false

64

)

65

 _ > ()) Corelang.type_table

66


67


68

let rec type_to_sort t =

69

if Types.is_bool_type t then bool_sort else

70

if Types.is_int_type t then int_sort else

71

if Types.is_real_type t then real_sort else

72

match (Types.repr t).Types.tdesc with

73

 Types.Tconst ty > get_const_sort ty

74

 Types.Tclock t > type_to_sort t

75

 Types.Tarray(dim,ty) > Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty)

76

 Types.Tstatic(d, ty)> type_to_sort ty

77

 Types.Tarrow _

78

 _ > Format.eprintf "internal error: pp_type %a@."

79

Types.print_ty t; assert false

80


81

(** Func decls

82


83

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

84

proposed encoding introduces a 0ary fun_decl to model variables

85

and fun_decl with arguments to declare reset and step predicates.

86


87


88


89

*)

90

let decls = Hashtbl.create 13

91

let register_fdecl id fd = Hashtbl.add decls id fd

92

let get_fdecl id = Hashtbl.find decls id

93


94

let decl_var id =

95

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

96

register_fdecl id.var_id fdecl;

97

fdecl

98


99

let decl_rel name args =

100

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

101

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

102

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

103

register_fdecl name fdecl;

104

fdecl

105


106


107


108

(** conversion functions

109


110

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

111

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

112


113

*)

114


115


116

(* Returns the f_decl associated to the variable v *)

117

let horn_var_to_expr v =

118

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

119


120


121


122


123

(* Used to print boolean constants *)

124

let horn_tag_to_expr t =

125

if t = Corelang.tag_true then

126

Z3.Boolean.mk_true !ctx

127

else if t = Corelang.tag_false then

128

Z3.Boolean.mk_false !ctx

129

else

130

(* Finding the associated sort *)

131

let sort = get_tag_sort t in

132

let elems = get_sort_elems sort in

133

let res : Z3.Expr.expr option =

134

List.fold_left2 (fun res cst expr >

135

match res with

136

 Some _ > res

137

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

138

) None elems (Z3.Enumeration.get_consts sort)

139

in

140

match res with None > assert false  Some s > s

141


142

(* Prints a constant value *)

143

let rec horn_const_to_expr c =

144

match c with

145

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

146

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

147

 Const_tag t > horn_tag_to_expr t

148

 _ > assert false

149


150


151


152

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

153

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

154

for the type integer (arrays).

155

*)

156

let rec horn_default_val t =

157

let t = Types.dynamic_type t in

158

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

159

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

160

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

161

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

162

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

163

* let valt = Types.array_element_type t in

164

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

165

* pp_type valt

166

* pp_default_val valt

167

*  Types.Tstruct(l) > assert false

168

*  Types.Ttuple(l) > assert false

169

* _ > *) assert false

170


171


172

let horn_basic_app i val_to_expr vl =

173

match i, vl with

174

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

175

Z3.Boolean.mk_ite

176

!ctx

177

(val_to_expr v1)

178

(val_to_expr v2)

179

(val_to_expr v3)

180


181

 "uminus", [v] >

182

Z3.Arithmetic.mk_unary_minus

183

!ctx

184

(val_to_expr v)

185

 "not", [v] >

186

Z3.Boolean.mk_not

187

!ctx

188

(val_to_expr v)

189

 "=", [v1; v2] >

190

Z3.Boolean.mk_eq

191

!ctx

192

(val_to_expr v1)

193

(val_to_expr v2)

194

 "&&", [v1; v2] >

195

Z3.Boolean.mk_and

196

!ctx

197

[val_to_expr v1;

198

val_to_expr v2]

199

 "", [v1; v2] >

200

Z3.Boolean.mk_or

201

!ctx

202

[val_to_expr v1;

203

val_to_expr v2]

204


205

 "impl", [v1; v2] >

206

Z3.Boolean.mk_implies

207

!ctx

208

(val_to_expr v1)

209

(val_to_expr v2)

210

 "mod", [v1; v2] >

211

Z3.Arithmetic.Integer.mk_mod

212

!ctx

213

(val_to_expr v1)

214

(val_to_expr v2)

215

 "equi", [v1; v2] >

216

Z3.Boolean.mk_eq

217

!ctx

218

(val_to_expr v1)

219

(val_to_expr v2)

220

 "xor", [v1; v2] >

221

Z3.Boolean.mk_xor

222

!ctx

223

(val_to_expr v1)

224

(val_to_expr v2)

225

 "!=", [v1; v2] >

226

Z3.Boolean.mk_not

227

!ctx

228

(

229

Z3.Boolean.mk_eq

230

!ctx

231

(val_to_expr v1)

232

(val_to_expr v2)

233

)

234

 "/", [v1; v2] >

235

Z3.Arithmetic.mk_div

236

!ctx

237

(val_to_expr v1)

238

(val_to_expr v2)

239


240

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

241

* !ctx

242

* (val_to_expr v1)

243

* (val_to_expr v2)

244

*

245

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

246

 _ > (

247

Format.eprintf

248

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

249

assert false)

250


251


252

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

253

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

254

but an offset suffix may be added for array variables

255

*)

256

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

257

match v.value_desc with

258

 Cst c > horn_const_to_expr c

259


260

(* Code specific for arrays *)

261

 Array il >

262

(* An array definition:

263

(store (

264

...

265

(store (

266

store (

267

default_val

268

)

269

idx_n val_n

270

)

271

idx_n1 val_n1)

272

...

273

idx_1 val_1

274

) *)

275

let rec build_array (tab, x) =

276

match tab with

277

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

278

 h::t >

279

Z3.Z3Array.mk_store

280

!ctx

281

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

282

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

283

(horn_val_to_expr ~is_lhs:is_lhs self h)

284

in

285

build_array (il, 0)

286


287

 Access(tab,index) >

288

Z3.Z3Array.mk_select !ctx

289

(horn_val_to_expr ~is_lhs:is_lhs self tab)

290

(horn_val_to_expr ~is_lhs:is_lhs self index)

291


292

(* Code specific for arrays *)

293


294

 Power (v, n) > assert false

295

 LocalVar v >

296

horn_var_to_expr

297

(rename_machine

298

self

299

v)

300

 StateVar v >

301

if Types.is_array_type v.var_type

302

then assert false

303

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

304

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

305


306

let no_reset_to_exprs machines m i =

307

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

308

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

309


310

let m_list =

311

rename_machine_list

312

(concat m.mname.node_id i)

313

(rename_mid_list (full_memory_vars machines target_machine))

314

in

315

let c_list =

316

rename_machine_list

317

(concat m.mname.node_id i)

318

(rename_current_list (full_memory_vars machines target_machine))

319

in

320

match c_list, m_list with

321

 [chd], [mhd] >

322

let expr =

323

Z3.Boolean.mk_eq !ctx

324

(horn_var_to_expr mhd)

325

(horn_var_to_expr chd)

326

in

327

[expr]

328

 _ > (

329

let exprs =

330

List.map2 (fun mhd chd >

331

Z3.Boolean.mk_eq !ctx

332

(horn_var_to_expr mhd)

333

(horn_var_to_expr chd)

334

)

335

m_list

336

c_list

337

in

338

exprs

339

)

340


341

let instance_reset_to_exprs machines m i =

342

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

343

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

344

let vars =

345

(

346

(rename_machine_list

347

(concat m.mname.node_id i)

348

(rename_current_list (full_memory_vars machines target_machine))

349

)

350

@

351

(rename_machine_list

352

(concat m.mname.node_id i)

353

(rename_mid_list (full_memory_vars machines target_machine))

354

)

355

)

356

in

357

let expr =

358

Z3.Expr.mk_app

359

!ctx

360

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

361

(List.map (horn_var_to_expr) vars)

362

in

363

[expr]

364


365

let instance_call_to_exprs machines reset_instances m i inputs outputs =

366

let self = m.mname.node_id in

367

try (* stateful node instance *)

368

begin

369

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

370

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

371


372

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

373

let reset_exprs =

374

if not (List.mem i reset_instances) then

375

(* If not, declare mem_m = mem_c *)

376

no_reset_to_exprs machines m i

377

else

378

[] (* Nothing to add yet *)

379

in

380


381

let mems = full_memory_vars machines target_machine in

382

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

383

let mid_mems = rename_mems rename_mid_list in

384

let next_mems = rename_mems rename_next_list in

385


386

let call_expr =

387

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

388

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

389

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

390

Z3.Boolean.mk_eq !ctx

391

( (* output var *)

392

horn_val_to_expr

393

~is_lhs:true

394

self

395

(mk_val (LocalVar o) o.var_type)

396

)

397

(

398

Z3.Boolean.mk_ite !ctx

399

(horn_var_to_expr mem_m)

400

(horn_val_to_expr self i1)

401

(horn_val_to_expr self i2)

402

)

403

in

404

let stmt2 = (* mem_X = false *)

405

Z3.Boolean.mk_eq !ctx

406

(horn_var_to_expr mem_x)

407

(Z3.Boolean.mk_false !ctx)

408

in

409

[stmt1; stmt2]

410

end

411


412

 node_name_n >

413

let expr =

414

Z3.Expr.mk_app

415

!ctx

416

(get_fdecl (machine_step_name (node_name n)))

417

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

418

(

419

List.map (horn_val_to_expr self) (

420

inputs @

421

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

422

)

423

) @ (

424

List.map (horn_var_to_expr) (mid_mems@next_mems)

425

)

426

)

427

in

428

[expr]

429

in

430


431

reset_exprs@call_expr

432

end

433

with Not_found > ( (* stateless node instance *)

434

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

435

let expr =

436

Z3.Expr.mk_app

437

!ctx

438

(get_fdecl (machine_stateless_name (node_name n)))

439

((* Arguments are inputs, outputs *)

440

List.map (horn_val_to_expr self)

441

(

442

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

443

)

444

)

445

in

446

[expr]

447

)

448


449


450

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

451

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

452

match Corelang.get_instr_desc instr with

453

 MComment _ > [], reset_instances

454

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

455

no_reset_to_exprs machines m i,

456

i::reset_instances

457

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

458

instance_reset_to_exprs machines m i,

459

i::reset_instances

460

 MLocalAssign (i,v) >

461

assign_to_exprs

462

m (horn_var_to_expr)

463

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

464

reset_instances

465

 MStateAssign (i,v) >

466

assign_to_exprs

467

m (horn_var_to_expr)

468

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

469

reset_instances

470

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

471

assert false (* This should not happen anymore *)

472

 MStep (il, i, vl) >

473

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

474

mem_c and print the call to mem_m *)

475

instance_call_to_exprs machines reset_instances m i vl il,

476

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

477

don't have to update reset_instances *)

478


479

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

480

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

481

compare the reset_instances of each branch and

482

introduced the mem_m = mem_c for branches to do not

483

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

484

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

485

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

486

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

487

statement. *)

488

let self = m.mname.node_id in

489

let branch_to_expr (tag, instrs) =

490

Z3.Boolean.mk_implies

491

(Z3.Boolean.mk_eq !ctx

492

(horn_val_to_expr self g)

493

(horn_tag_to_expr tag))

494

(machine_instrs_to_exprs machines reset_instances m instrs)

495

in

496

List.map branch_to_expr hl,

497

reset_instances

498


499

and instrs_to_expr machines reset_instances m instrs =

500

let instr_to_expr rs i = instr_to_expr machines rs m i in

501

match instrs with

502

 [x] > instr_to_expres reset_instances x

503

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

504


505

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

506

let exprs_i, rs = ppi rs i in

507

expr@exprs_i, rs

508

)

509

([], reset_instances) instrs

510


511


512

 [] > [], reset_instances

513


514


515

let basic_library_to_horn_expr i vl =

516

match i, vl with

517

 "ite", [v1; v2; v3] > Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3

518


519

 "uminus", [v] > Format.fprintf fmt "( %a)" pp_val v

520

 "not", [v] > Format.fprintf fmt "(not %a)" pp_val v

521

 "=", [v1; v2] > Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2

522

 "&&", [v1; v2] > Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2

523

 "", [v1; v2] > Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2

524

 "impl", [v1; v2] > Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2

525

 "mod", [v1; v2] > Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2

526

 "equi", [v1; v2] > Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2

527

 "xor", [v1; v2] > Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2

528

 "!=", [v1; v2] > Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2

529

 "/", [v1; v2] > Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2

530

 _, [v1; v2] > Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2

531

 _ > (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false)

532

(*  "mod", [v1; v2] > Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2

533


534

*)

535


536


537

(* Prints a [value] indexed by the suffix list [loop_vars] *)

538

let rec value_suffix_to_expr self value =

539

match value.value_desc with

540

 Fun (n, vl) >

541

basic_library_to_horn_expr n (value_suffix_to_expr self vl)

542

 _ >

543

horn_val_to_expr self value

544


545


546

(* type_directed assignment: array vs. statically sized type

547

 [var_type]: type of variable to be assigned

548

 [var_name]: name of variable to be assigned

549

 [value]: assigned value

550

 [pp_var]: printer for variables

551

*)

552

let assign_to_exprs m var_name value =

553

let self = m.mname.node_id in

554

let e =

555

Z3.Boolean.mk_eq

556

!ctx

557

(horn_val_to_expr ~is_lhs:true self var_name)

558

(value_suffix_to_expr self value)

559

in

560

[e]

561


562

(* TODO: empty list means true statement *)

563

let decl_machine machines m =

564

if m.Machine_code.mname.node_id = Machine_code.arrow_id then

565

(* We don't print arrow function *)

566

()

567

else

568

begin

569

let vars =

570

List.map decl_var

571

(

572

(inout_vars machines m)@

573

(rename_current_list (full_memory_vars machines m)) @

574

(rename_mid_list (full_memory_vars machines m)) @

575

(rename_next_list (full_memory_vars machines m)) @

576

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

577

)

578

in

579


580

if is_stateless m then

581

begin

582

(* Declaring single predicate *)

583

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

584

match m.mstep.step_asserts with

585

 [] >

586

begin

587


588

(* Rule for single predicate *)

589

fprintf fmt "; Stateless step rule @.";

590

fprintf fmt "@[<v 2>(rule (=> @ ";

591

ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) ) m fmt m.mstep.step_instrs);

592

fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."

593

pp_machine_stateless_name m.mname.node_id

594

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

595

end

596

 assertsl >

597

begin

598

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

599


600

fprintf fmt "; Stateless step rule with Assertions @.";

601

(*Rule for step*)

602

fprintf fmt "@[<v 2>(rule (=> @ (and @ ";

603

ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);

604

fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl

605

pp_machine_stateless_name m.mname.node_id

606

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

607


608

end

609


610

end

611

else

612

begin

613

(* Declaring predicate *)

614

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

615

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

616


617

(* Rule for reset *)

618

fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."

619

(pp_machine_reset machines) m

620

pp_machine_reset_name m.mname.node_id

621

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

622


623

match m.mstep.step_asserts with

624

 [] >

625

begin

626

fprintf fmt "; Step rule @.";

627

(* Rule for step*)

628

fprintf fmt "@[<v 2>(rule (=> @ ";

629

ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);

630

fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."

631

pp_machine_step_name m.mname.node_id

632

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

633

end

634

 assertsl >

635

begin

636

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

637

(* print_string pp_val; *)

638

fprintf fmt "; Step rule with Assertions @.";

639


640

(*Rule for step*)

641

fprintf fmt "@[<v 2>(rule (=> @ (and @ ";

642

ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);

643

fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl

644

pp_machine_step_name m.mname.node_id

645

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

646

end

647


648


649

end

650

end

651


652

let param_stat = ref false

653

let param_eldarica = ref false

654

let param_utvpi = ref false

655

let param_tosmt = ref false

656

let param_pp = ref false

657


658

module Verifier =

659

(struct

660

include VerifierType.Default

661

let name = "zustre"

662

let options = [

663

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

664

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

665

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

666

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

667

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

668

]

669


670

let activate () = (

671

active := true;

672

Options.output := "horn";

673

)

674

let is_active () = !active

675


676

let get_normalization_params () =

677

(* make sure the output is "Horn" *)

678

assert(!Options.output = "horn");

679

Backends.get_normalization_params ()

680


681

let setup_solver () =

682

let fp = Z3.Fixedpoint.mk_fixedpoint !ctx in

683

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

684

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

685

*

686

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

687

* let help = Z3.Solver.get_help solver in

688

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

689


690

let module P = Z3.Params in

691

let module S = Z3.Symbol in

692

let mks = S.mk_string !ctx in

693

let params = P.mk_params !ctx in

694


695

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

696

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

697


698

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

699

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

700

if !param_stat then

701

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

702

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

703


704

(* Dont know where to find this parameter *)

705

(* if !param_spacer_verbose then

706

* if self.args.spacer_verbose:

707

* z3.set_option (verbose=1) *)

708


709

(* The option is not recogined*)

710

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

711

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

712


713

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

714

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

715


716

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

717

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

718


719

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

720

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

721


722

(* if self.args.eldarica:

723

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

724

if !param_eldarica then

725

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

726


727

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

728

if !param_utvpi then

729

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

730


731

(* if self.args.tosmt:

732

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

733

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

734

if !param_tosmt then

735

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

736


737

(* if not self.args.pp:

738

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

739

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

740

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

741

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

742

if !param_pp then (

743

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

744

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

745

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

746

);

747

Z3.Fixedpoint.set_parameters fp params

748


749


750

let run basename prog machines =

751

let machines = Machine_code.arrow_machine::machines in

752

let machines = preprocess machines in

753

setup_solver ();

754

decl_sorts ();

755

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

756


757


758

()

759


760

end: VerifierType.S)

761

