1

open Lustre_types

2

open Machine_code_types

3

open Machine_code_common

4


5

(* open Horn_backend_common

6

* open Horn_backend *)

7

open Zustre_data

8


9

let report = Log.report ~plugin:"z3 interface"

10


11

module HBC = Horn_backend_common

12


13

let node_name = HBC.node_name

14


15

let concat = HBC.concat

16


17

let rename_machine = HBC.rename_machine

18


19

let rename_machine_list = HBC.rename_machine_list

20


21

let rename_next = HBC.rename_next

22


23

let rename_mid = HBC.rename_mid

24


25

let rename_current = HBC.rename_current

26


27

let rename_current_list = HBC.rename_current_list

28


29

let rename_mid_list = HBC.rename_mid_list

30


31

let rename_next_list = HBC.rename_next_list

32


33

let full_memory_vars = HBC.full_memory_vars

34


35

let inout_vars = HBC.inout_vars

36


37

let reset_vars = HBC.reset_vars

38


39

let step_vars = HBC.step_vars

40


41

let local_memory_vars = HBC.local_memory_vars

42


43

let step_vars_m_x = HBC.step_vars_m_x

44


45

let step_vars_c_m_x = HBC.step_vars_c_m_x

46


47

let machine_reset_name = HBC.machine_reset_name

48


49

let machine_step_name = HBC.machine_step_name

50


51

let machine_stateless_name = HBC.machine_stateless_name

52


53

let preprocess = Horn_backend.preprocess

54


55

exception UnknownFunction of (string * (Format.formatter > unit))

56

(** Sorts

57


58

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

59


60

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

61

with a enumerated type name. *)

62


63

let bool_sort = Z3.Boolean.mk_sort !ctx

64


65

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

66


67

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

68


69

let get_const_sort = Hashtbl.find const_sorts

70


71

let get_sort_elems = Hashtbl.find sort_elems

72


73

let get_tag_sort id =

74

try Hashtbl.find const_tags id

75

with _ >

76

Format.eprintf "Unable to find sort for tag=%s@." id;

77

assert false

78


79

let decl_sorts () =

80

Hashtbl.iter

81

(fun typ decl >

82

match typ with

83

 Tydec_const var > (

84

match decl.top_decl_desc with

85

 TypeDef tdef > (

86

match tdef.tydef_desc with

87

 Tydec_enum tl >

88

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

89

Hashtbl.add const_sorts var new_sort;

90

Hashtbl.add sort_elems new_sort tl;

91

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

92

 _ >

93

Format.eprintf "Unknown type : %a@.@?" Printers.pp_var_type_dec_desc

94

typ;

95

assert false)

96

 _ >

97

assert false)

98

 _ >

99

())

100

Corelang.type_table

101


102

let rec type_to_sort t =

103

if Types.is_bool_type t then bool_sort

104

else if Types.is_int_type t then int_sort

105

else if Types.is_real_type t then real_sort

106

else

107

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

108

 Types.Tconst ty >

109

get_const_sort ty

110

 Types.Tclock t >

111

type_to_sort t

112

 Types.Tarray (_, ty) >

113

Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty)

114

 Types.Tstatic (_, ty) >

115

type_to_sort ty

116

 Types.Tarrow _  _ >

117

Format.eprintf "internal error: pp_type %a@." Types.print_ty t;

118

assert false

119


120

(* let idx_var = *)

121

(* Z3.FuncDecl.mk_func_decl_s !ctx "__idx__" [] idx_sort *)

122


123

(* let uid_var = *)

124

(* Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort *)

125


126

(** Func decls

127


128

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

129

proposed encoding introduces a 0ary fun_decl to model variables and

130

fun_decl with arguments to declare reset and step predicates. *)

131

let register_fdecl id fd = Hashtbl.add decls id fd

132


133

let get_fdecl id =

134

try Hashtbl.find decls id

135

with Not_found >

136

report ~level:3 (fun fmt >

137

Format.fprintf fmt "Unable to find func_decl %s@.@?" id);

138

raise Not_found

139


140

let pp_fdecls fmt =

141

Format.fprintf fmt "Registered fdecls: @[%a@]@ "

142

(Utils.fprintf_list ~sep:"@ " Format.pp_print_string)

143

(Hashtbl.fold (fun id _ accu > id :: accu) decls [])

144


145

let decl_var id =

146

(* Format.eprintf "Declaring var %s@." id.var_id; *)

147

let fdecl =

148

Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type)

149

in

150

register_fdecl id.var_id fdecl;

151

fdecl

152


153

(* Declaring the function used in expr *)

154

let decl_fun op args typ =

155

let args = List.map type_to_sort args in

156

let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx op args (type_to_sort typ) in

157

register_fdecl op fdecl;

158

fdecl

159


160

let idx_sort = int_sort

161


162

let uid_sort =

163

Z3.Z3List.mk_sort !ctx (Z3.Symbol.mk_string !ctx "uid_list") int_sort

164


165

let uid_conc =

166

let fd = Z3.Z3List.get_cons_decl uid_sort in

167

fun head tail > Z3.FuncDecl.apply fd [ head; tail ]

168


169

let get_instance_uid =

170

let hash : (string, int) Hashtbl.t = Hashtbl.create 13 in

171

let cpt = ref 0 in

172

fun i >

173

let id =

174

if Hashtbl.mem hash i then Hashtbl.find hash i

175

else (

176

incr cpt;

177

Hashtbl.add hash i !cpt;

178

!cpt)

179

in

180

Z3.Arithmetic.Integer.mk_numeral_i !ctx id

181


182

let decl_rel ?(no_additional_vars = false) name args_sorts =

183

(* Enriching arg_sorts with two new variables: a counting index and an uid *)

184

let args_sorts =

185

if no_additional_vars then args_sorts

186

else idx_sort :: uid_sort :: args_sorts

187

in

188


189

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

190

if !debug then

191

Format.eprintf "Registering fdecl %s (%a)@." name

192

(Utils.fprintf_list ~sep:"@ " (fun fmt sort >

193

Format.fprintf fmt "%s" (Z3.Sort.to_string sort)))

194

args_sorts;

195

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

196

Z3.Fixedpoint.register_relation !fp fdecl;

197

register_fdecl name fdecl;

198

fdecl

199


200

(* Shared variables to describe counter and uid *)

201


202

let idx = Corelang.dummy_var_decl "__idx__" Type_predef.type_int

203


204

let idx_var = Z3.Expr.mk_const_f !ctx (decl_var idx)

205


206

let uid = Corelang.dummy_var_decl "__uid__" Type_predef.type_int

207


208

let uid_fd = Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort

209


210

let _ = register_fdecl "__uid__" uid_fd

211


212

let uid_var = Z3.Expr.mk_const_f !ctx uid_fd

213


214

(** Conversion functions

215


216

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

217

rephrased from pp_xx to xx_to_expr and produces a Z3 value. *)

218


219

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

220

let horn_var_to_expr v = Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id)

221


222

(* Used to print boolean constants *)

223

let horn_tag_to_expr t =

224

if t = tag_true then Z3.Boolean.mk_true !ctx

225

else if t = tag_false then Z3.Boolean.mk_false !ctx

226

else

227

(* Finding the associated sort *)

228

let sort = get_tag_sort t in

229

let elems = get_sort_elems sort in

230

let res : Z3.Expr.expr option =

231

List.fold_left2

232

(fun res cst expr >

233

match res with

234

 Some _ >

235

res

236

 None >

237

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

238

None elems

239

(Z3.Enumeration.get_consts sort)

240

in

241

match res with None > assert false  Some s > s

242


243

(* Prints a constant value *)

244

let horn_const_to_expr c =

245

match c with

246

 Const_int i >

247

Z3.Arithmetic.Integer.mk_numeral_i !ctx i

248

 Const_real r >

249

Z3.Arithmetic.Real.mk_numeral_s !ctx (Real.to_string r)

250

 Const_tag t >

251

horn_tag_to_expr t

252

 _ >

253

assert false

254


255

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

256

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

257

for the type integer (arrays). *)

258

let horn_default_val t =

259

let t = Types.dynamic_type t in

260

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

261

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

262

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

263

else

264

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

265

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

266

* let valt = Types.array_element_type t in

267

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

268

* pp_type valt

269

* pp_default_val valt

270

*  Types.Tstruct(l) > assert false

271

*  Types.Ttuple(l) > assert false

272

* _ > *)

273

assert false

274


275

(* Conversion of basic library functions *)

276


277

let horn_basic_app i vl (vltyp, typ) =

278

match i, vl with

279

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

280

Z3.Boolean.mk_ite !ctx v1 v2 v3

281

 "uminus", [ v ] >

282

Z3.Arithmetic.mk_unary_minus !ctx v

283

 "not", [ v ] >

284

Z3.Boolean.mk_not !ctx v

285

 "=", [ v1; v2 ] >

286

Z3.Boolean.mk_eq !ctx v1 v2

287

 "&&", [ v1; v2 ] >

288

Z3.Boolean.mk_and !ctx [ v1; v2 ]

289

 "", [ v1; v2 ] >

290

Z3.Boolean.mk_or !ctx [ v1; v2 ]

291

 "impl", [ v1; v2 ] >

292

Z3.Boolean.mk_implies !ctx v1 v2

293

 "mod", [ v1; v2 ] >

294

Z3.Arithmetic.Integer.mk_mod !ctx v1 v2

295

 "equi", [ v1; v2 ] >

296

Z3.Boolean.mk_eq !ctx v1 v2

297

 "xor", [ v1; v2 ] >

298

Z3.Boolean.mk_xor !ctx v1 v2

299

 "!=", [ v1; v2 ] >

300

Z3.Boolean.mk_not !ctx (Z3.Boolean.mk_eq !ctx v1 v2)

301

 "/", [ v1; v2 ] >

302

Z3.Arithmetic.mk_div !ctx v1 v2

303

 "+", [ v1; v2 ] >

304

Z3.Arithmetic.mk_add !ctx [ v1; v2 ]

305

 "", [ v1; v2 ] >

306

Z3.Arithmetic.mk_sub !ctx [ v1; v2 ]

307

 "*", [ v1; v2 ] >

308

Z3.Arithmetic.mk_mul !ctx [ v1; v2 ]

309

 "<", [ v1; v2 ] >

310

Z3.Arithmetic.mk_lt !ctx v1 v2

311

 "<=", [ v1; v2 ] >

312

Z3.Arithmetic.mk_le !ctx v1 v2

313

 ">", [ v1; v2 ] >

314

Z3.Arithmetic.mk_gt !ctx v1 v2

315

 ">=", [ v1; v2 ] >

316

Z3.Arithmetic.mk_ge !ctx v1 v2

317

 "int_to_real", [ v1 ] >

318

Z3.Arithmetic.Integer.mk_int2real !ctx v1

319

 _ >

320

let fd =

321

try get_fdecl i

322

with Not_found >

323

report ~level:3 (fun fmt >

324

Format.fprintf fmt

325

"Registering function %s as uninterpreted function in Z3@.%s: \

326

(%a) > %a"

327

i i

328

(Utils.fprintf_list ~sep:"," Types.print_ty)

329

vltyp Types.print_ty typ);

330

decl_fun i vltyp typ

331

in

332

Z3.FuncDecl.apply fd vl

333


334

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

335

* !ctx

336

* (val_to_expr v1)

337

* (val_to_expr v2)

338

*

339

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

340


341

(*  _ > (

342

* let msg fmt = Format.fprintf fmt

343

* "internal error: zustre unkown function %s (nb args = %i)@."

344

* i (List.length vl)

345

* in

346

* raise (UnknownFunction(i, msg))

347

* ) *)

348


349

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

350

is a printer for variables (typically [pp_c_var_read]), but an offset suffix

351

may be added for array variables *)

352

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

353

(* Format.eprintf "h_v2e %a@." (Machine_code_common.pp_val m) v ; *)

354

match v.value_desc with

355

 Cst c >

356

horn_const_to_expr c

357

(* Code specific for arrays *)

358

 Array il >

359

(* An array definition: (store ( ... (store ( store ( default_val ) idx_n

360

val_n ) idx_n1 val_n1) ... idx_1 val_1 ) *)

361

let rec build_array (tab, x) =

362

match tab with

363

 [] >

364

horn_default_val v.value_type (* (get_type v) *)

365

 h :: t >

366

Z3.Z3Array.mk_store !ctx

367

(build_array (t, x + 1))

368

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

369

(horn_val_to_expr ~is_lhs m self h)

370

in

371

build_array (il, 0)

372

 Access (tab, index) >

373

Z3.Z3Array.mk_select !ctx

374

(horn_val_to_expr ~is_lhs m self tab)

375

(horn_val_to_expr ~is_lhs m self index)

376

(* Code specific for arrays *)

377

 Power _ >

378

assert false

379

 Var v >

380

if is_memory m v then

381

if Types.is_array_type v.var_type then assert false

382

else

383

horn_var_to_expr

384

(rename_machine self

385

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

386

else horn_var_to_expr (rename_machine self v)

387

 Fun (n, vl) >

388

horn_basic_app n

389

(List.map (horn_val_to_expr m self) vl)

390

(List.map (fun v > v.value_type) vl, v.value_type)

391


392

let no_reset_to_exprs machines m i =

393

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

394

let target_machine =

395

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

396

in

397


398

let m_list =

399

rename_machine_list (concat m.mname.node_id i)

400

(rename_mid_list (full_memory_vars machines target_machine))

401

in

402

let c_list =

403

rename_machine_list (concat m.mname.node_id i)

404

(rename_current_list (full_memory_vars machines target_machine))

405

in

406

match c_list, m_list with

407

 [ chd ], [ mhd ] >

408

let expr =

409

Z3.Boolean.mk_eq !ctx (horn_var_to_expr mhd) (horn_var_to_expr chd)

410

in

411

[ expr ]

412

 _ >

413

let exprs =

414

List.map2

415

(fun mhd chd >

416

Z3.Boolean.mk_eq !ctx (horn_var_to_expr mhd) (horn_var_to_expr chd))

417

m_list c_list

418

in

419

exprs

420


421

let instance_reset_to_exprs machines m i =

422

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

423

let target_machine =

424

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

425

in

426

let vars =

427

rename_machine_list (concat m.mname.node_id i)

428

(rename_current_list (full_memory_vars machines target_machine))

429

@ rename_mid_list (full_memory_vars machines target_machine)

430

in

431


432

let expr =

433

Z3.Expr.mk_app !ctx

434

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

435

(List.map horn_var_to_expr (idx :: uid :: vars))

436

in

437

[ expr ]

438


439

let instance_call_to_exprs machines reset_instances m i inputs outputs =

440

let self = m.mname.node_id in

441


442

(* Building call args *)

443

let idx_uid_inout =

444

(* Additional input to register step counters, and uid *)

445

let idx = horn_var_to_expr idx in

446

let uid = uid_conc (get_instance_uid i) (horn_var_to_expr uid) in

447

let inout =

448

List.map (horn_val_to_expr m self)

449

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

450

in

451

idx :: uid :: inout

452

in

453


454

try

455

(* stateful node instance *)

456

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

457

let target_machine =

458

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

459

in

460


461

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

462

let reset_exprs =

463

if not (List.mem i reset_instances) then

464

(* If not, declare mem_m = mem_c *)

465

no_reset_to_exprs machines m i

466

else []

467

(* Nothing to add yet *)

468

in

469


470

let mems = full_memory_vars machines target_machine in

471

let rename_mems f =

472

rename_machine_list (concat m.mname.node_id i) (f mems)

473

in

474

let mid_mems = rename_mems rename_mid_list in

475

let next_mems = rename_mems rename_next_list in

476


477

let call_expr =

478

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

479

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

480

let stmt1 =

481

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

482

Z3.Boolean.mk_eq !ctx

483

((* output var *)

484

horn_val_to_expr ~is_lhs:true m self

485

(mk_val (Var o) o.var_type))

486

(Z3.Boolean.mk_ite !ctx (horn_var_to_expr mem_m)

487

(horn_val_to_expr m self i1)

488

(horn_val_to_expr m self i2))

489

in

490

let stmt2 =

491

(* mem_X = false *)

492

Z3.Boolean.mk_eq !ctx (horn_var_to_expr mem_x)

493

(Z3.Boolean.mk_false !ctx)

494

in

495

[ stmt1; stmt2 ]

496

 _ >

497

let expr =

498

Z3.Expr.mk_app !ctx

499

(get_fdecl (machine_step_name (node_name n)))

500

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

501

idx_uid_inout

502

@ List.map horn_var_to_expr (mid_mems @ next_mems))

503

in

504

[ expr ]

505

in

506


507

reset_exprs @ call_expr

508

with Not_found >

509

(* stateless node instance *)

510

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

511

let expr =

512

Z3.Expr.mk_app !ctx

513

(get_fdecl (machine_stateless_name (node_name n)))

514

idx_uid_inout

515

(* Arguments are inputs, outputs *)

516

in

517

[ expr ]

518


519

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

520

(* let rec value_suffix_to_expr self value = *)

521

(* match value.value_desc with *)

522

(*  Fun (n, vl) > *)

523

(* horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *)

524


525

(*  _ > *)

526

(* horn_val_to_expr self value *)

527


528

(* type_directed assignment: array vs. statically sized type  [var_type]: type

529

of variable to be assigned  [var_name]: name of variable to be assigned 

530

[value]: assigned value  [pp_var]: printer for variables *)

531

let assign_to_exprs m var_name value =

532

let self = m.mname.node_id in

533

let e =

534

Z3.Boolean.mk_eq !ctx

535

(horn_val_to_expr ~is_lhs:true m self var_name)

536

(horn_val_to_expr m self value)

537

(* was: TODO deal with array accesses (value_suffix_to_expr self value) *)

538

in

539

[ e ]

540


541

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

542

let rec instr_to_exprs machines reset_instances (m : machine_t) instr :

543

Z3.Expr.expr list * ident list =

544

match Corelang.get_instr_desc instr with

545

 MComment _ >

546

[], reset_instances

547

 MNoReset i >

548

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

549

no_reset_to_exprs machines m i, i :: reset_instances

550

 MReset i >

551

(* we assign middle_mem with reset: reset(mem_m) *)

552

instance_reset_to_exprs machines m i, i :: reset_instances

553

 MLocalAssign (i, v) >

554

assign_to_exprs m (mk_val (Var i) i.var_type) v, reset_instances

555

 MStateAssign (i, v) >

556

assign_to_exprs m (mk_val (Var i) i.var_type) v, reset_instances

557

 MStep ([ _ ], i, vl)

558

when Basic_library.is_internal_fun i (List.map (fun v > v.value_type) vl)

559

>

560

assert false (* This should not happen anymore *)

561

 MStep (il, i, vl) >

562

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

563

mem_m = mem_c and print the call to mem_m *)

564

instance_call_to_exprs machines reset_instances m i vl il, reset_instances

565

(* Since this instance call will only happen once, we don't have to update

566

reset_instances *)

567

 MBranch (g, hl) >

568

(* (g = tag1 => expr1) and (g = tag2 => expr2) ... should not be produced

569

yet. Later, we will have to compare the reset_instances of each branch

570

and introduced the mem_m = mem_c for branches to do not address it while

571

other did. Am I clear ? *)

572

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

573

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

574

of the branch, then all others have to have the mem_m = mem_c statement. *)

575

let self = m.mname.node_id in

576

let branch_to_expr (tag, instrs) =

577

let branch_def, branch_resets =

578

instrs_to_expr machines reset_instances m instrs

579

in

580

let e =

581

Z3.Boolean.mk_implies !ctx

582

(Z3.Boolean.mk_eq !ctx

583

(horn_val_to_expr m self g)

584

(horn_tag_to_expr tag))

585

branch_def

586

in

587


588

[ e ], branch_resets

589

in

590


591

List.fold_left

592

(fun (instrs, resets) b >

593

let b_instrs, b_resets = branch_to_expr b in

594

instrs @ b_instrs, resets @ b_resets)

595

([], reset_instances) hl

596

 MSpec _ >

597

assert false

598


599

and instrs_to_expr machines reset_instances m instrs =

600

let instr_to_exprs rs i = instr_to_exprs machines rs m i in

601

let e_list, rs =

602

match instrs with

603

 [ x ] >

604

instr_to_exprs reset_instances x

605

 _ :: _ >

606

(* TODO: check whether we should compuyte a AND on the exprs (expr list)

607

built here. It was performed in the printer setting but seems to be

608

useless here since the output is a list of exprs *)

609

List.fold_left

610

(fun (exprs, rs) i >

611

let exprs_i, rs_i = instr_to_exprs rs i in

612

exprs @ exprs_i, rs @ rs_i)

613

([], reset_instances) instrs

614

 [] >

615

[], reset_instances

616

in

617

let e =

618

match e_list with

619

 [ e ] >

620

e

621

 [] >

622

Z3.Boolean.mk_true !ctx

623

 _ >

624

Z3.Boolean.mk_and !ctx e_list

625

in

626

e, rs

627


628

(*********************************************************)

629


630

(* Quantifiying universally all occuring variables *)

631

let add_rule ?(dont_touch = []) vars expr =

632

(* let fds = Z3.Expr.get_args expr in *)

633

(* Format.eprintf "Expr %s: args: [%a]@." *)

634

(* (Z3.Expr.to_string expr) *)

635

(* (Utils.fprintf_list ~sep:", " (fun fmt e > Format.pp_print_string fmt

636

(Z3.Expr.to_string e))) fds; *)

637


638

(* (\* Old code relying on provided vars *\) *)

639

(* let sorts = (List.map (fun id > type_to_sort id.var_type) vars) in *)

640

(* let symbols = (List.map (fun id > Z3.FuncDecl.get_name (get_fdecl

641

id.var_id)) vars) in *)

642


643

(* New code: we extract vars from expr *)

644

let module FDSet = Set.Make (struct

645

type t = Z3.FuncDecl.func_decl

646


647

let compare = compare

648

(* let hash = Hashtbl.hash *)

649

end) in

650

(* Fonction seems unused

651


652

let rec get_expr_vars e = let open Utils in let nb_args =

653

Z3.Expr.get_num_args e in if nb_args <= 0 then ( let fdecl =

654

Z3.Expr.get_func_decl e in (* let params = Z3.FuncDecl.get_parameters fdecl

655

in *) (* Format.eprintf "Extracting info about %s: @." (Z3.Expr.to_string

656

e); *) let dkind = Z3.FuncDecl.get_decl_kind fdecl in match dkind with

657

Z3enums.OP_UNINTERPRETED > ( (* Format.eprintf "kind = %s, " (match dkind

658

with Z3enums.OP_TRUE > "true"  Z3enums.OP_UNINTERPRETED > "uninter"); *)

659

(* let open Z3.FuncDecl.Parameter in *) (* List.iter (fun p > *) (* match

660

p with *) (* P_Int i > Format.eprintf "int %i" i *) (*  P_Dbl f >

661

Format.eprintf "dbl %f" f *) (*  P_Sym s > Format.eprintf "symb" *) (* 

662

P_Srt s > Format.eprintf "sort" *) (*  P_Ast _ >Format.eprintf "ast" *)

663

(*  P_Fdl f > Format.eprintf "fundecl" *) (*  P_Rat s > Format.eprintf

664

"rat %s" s *)

665


666

(* ) params; *) (* Format.eprintf "]@."; *) FDSet.singleton fdecl )  _ >

667

FDSet.empty ) else (*if nb_args > 0 then*) List.fold_left (fun accu e >

668

FDSet.union accu (get_expr_vars e)) FDSet.empty (Z3.Expr.get_args e) in *)

669

(* Unsed variable. Coul;d be reintroduced let extracted_vars = FDSet.elements

670

(FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in let

671

extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in let

672

extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in *)

673

if !debug then

674

Format.eprintf "Declaring rule: %s with variables @[<v 0>@ [%a@ ]@]@ @."

675

(Z3.Expr.to_string expr)

676

(Utils.fprintf_list ~sep:",@ " (fun fmt e >

677

Format.fprintf fmt "%s" (Z3.Expr.to_string e)))

678

(List.map horn_var_to_expr vars);

679

let expr =

680

Z3.Quantifier.mk_forall_const !ctx

681

(* context *)

682

(List.map horn_var_to_expr vars)

683

(* TODO provide bounded variables as expr *)

684

(* sorts (\* sort list*\) *)

685

(* symbols (\* symbol list *\) *)

686

expr (* expression *) None (* quantifier weight, None means 1 *) []

687

(* pattern list ? *) [] (* ? *) None (* ? *) None

688

(* ? *)

689

in

690


691

(* Format.eprintf "OK@.@?"; *)

692


693

(* TODO: bizarre la declaration de INIT tout seul semble poser pb. *)

694

Z3.Fixedpoint.add_rule !fp (Z3.Quantifier.expr_of_quantifier expr) None

695


696

(********************************************************)

697


698

let machine_reset machines m =

699

let locals = local_memory_vars m in

700


701

(* print "x_m = x_c" for each local memory *)

702

let mid_mem_def =

703

List.map

704

(fun v >

705

Z3.Boolean.mk_eq !ctx

706

(horn_var_to_expr (rename_mid v))

707

(horn_var_to_expr (rename_current v)))

708

locals

709

in

710


711

(* print "child_reset ( associated vars _ {c,m} )" for each subnode. Special

712

treatment for _arrow: _first = true *)

713

let reset_instances =

714

List.map

715

(fun (id, (n, _)) >

716

let name = node_name n in

717

if name = "_arrow" then

718

Z3.Boolean.mk_eq !ctx

719

(let vdecl =

720

get_fdecl (concat m.mname.node_id id ^ "._arrow._first_m")

721

in

722

Z3.Expr.mk_const_f !ctx vdecl)

723

(Z3.Boolean.mk_true !ctx)

724

else

725

let machine_n = get_machine machines name in

726


727

Z3.Expr.mk_app !ctx

728

(get_fdecl (name ^ "_reset"))

729

(List.map horn_var_to_expr

730

(idx

731

::

732

uid

733

::

734

(* Additional vars: counters, uid *)

735

rename_machine_list

736

(concat m.mname.node_id id)

737

(reset_vars machines machine_n))))

738

m.minstances

739

in

740


741

Z3.Boolean.mk_and !ctx (mid_mem_def @ reset_instances)

742


743

(* TODO: empty list means true statement *)

744

let decl_machine machines m =

745

if m.mname.node_id = Arrow.arrow_id then (* We don't do arrow function *)

746

()

747

else

748

let _ =

749

List.map decl_var

750

(inout_vars m

751

@ rename_current_list (full_memory_vars machines m)

752

@ rename_mid_list (full_memory_vars machines m)

753

@ rename_next_list (full_memory_vars machines m)

754

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

755

in

756

if is_stateless m then (

757

if !debug then

758

Format.eprintf "Declaring a stateless machine: %s@." m.mname.node_id;

759


760

(* Declaring single predicate *)

761

let vars = inout_vars m in

762

let vars_types = List.map (fun v > type_to_sort v.var_type) vars in

763

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

764


765

let horn_body, _ (* don't care for reset here *) =

766

instrs_to_expr machines [] (* No reset info for stateless nodes *) m

767

m.mstep.step_instrs

768

in

769

let horn_head =

770

Z3.Expr.mk_app !ctx

771

(get_fdecl (machine_stateless_name m.mname.node_id))

772

(List.map horn_var_to_expr

773

(idx :: uid :: (* Additional vars: counters, uid *)

774

vars))

775

in

776

(* this line seems useless *)

777

let vars =

778

idx :: uid :: vars

779

@ rename_machine_list m.mname.node_id m.mstep.step_locals

780

in

781

(* Format.eprintf "useless Vars: %a@." (Utils.fprintf_list ~sep:"@ "

782

Printers.pp_var) vars; *)

783

match m.mstep.step_asserts with

784

 [] >

785

(* Rule for single predicate : "; Stateless step rule @." *)

786

(*let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in*)

787

(* TODO clean code *)

788

(* Format.eprintf "used Vars: %a@." (Utils.fprintf_list ~sep:"@ "

789

Printers.pp_var) vars; *)

790

add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)

791

 assertsl >

792

(*Rule for step "; Stateless step rule with Assertions @.";*)

793

let body_with_asserts =

794

Z3.Boolean.mk_and !ctx

795

(horn_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl)

796

in

797

let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in

798

add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head))

799

else

800

(* Rule for reset *)

801

let vars = reset_vars machines m in

802

let vars_types = List.map (fun v > type_to_sort v.var_type) vars in

803

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

804

let horn_reset_body = machine_reset machines m in

805

let horn_reset_head =

806

Z3.Expr.mk_app !ctx

807

(get_fdecl (machine_reset_name m.mname.node_id))

808

(List.map horn_var_to_expr

809

(idx :: uid :: (* Additional vars: counters, uid *)

810

vars))

811

in

812


813

let _ =

814

add_rule (idx :: uid :: vars)

815

(Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)

816

in

817


818

(* Rule for step*)

819

let vars = step_vars machines m in

820

let vars_types = List.map (fun v > type_to_sort v.var_type) vars in

821

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

822

let horn_step_body, _ (* don't care for reset here *) =

823

instrs_to_expr machines [] m m.mstep.step_instrs

824

in

825

let horn_step_head =

826

Z3.Expr.mk_app !ctx

827

(get_fdecl (machine_step_name m.mname.node_id))

828

(List.map horn_var_to_expr

829

(idx :: uid :: (* Additional vars: counters, uid *)

830

vars))

831

in

832

match m.mstep.step_asserts with

833

 [] >

834

(* Rule for single predicate *)

835

let vars =

836

step_vars_c_m_x machines m

837

@ rename_machine_list m.mname.node_id m.mstep.step_locals

838

in

839

add_rule (idx :: uid :: vars)

840

(Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)

841

 assertsl >

842

(* Rule for step Assertions @.; *)

843

let body_with_asserts =

844

Z3.Boolean.mk_and !ctx

845

(horn_step_body

846

:: List.map (horn_val_to_expr m m.mname.node_id) assertsl)

847

in

848

let vars =

849

step_vars_c_m_x machines m

850

@ rename_machine_list m.mname.node_id m.mstep.step_locals

851

in

852

add_rule (idx :: uid :: vars)

853

(Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)

854


855

(* Debug functions *)

856

(* let rec extract_expr_fds e = (* Format.eprintf "@[<v 2>Extracting fundecls

857

from expr %s@ " *) (* (Z3.Expr.to_string e); *)

858


859

(* Removing quantifier is there are some *) let e = (* I didn't found a nicer

860

way to do it than with an exception. My bad *) try let eq =

861

Z3.Quantifier.quantifier_of_expr e in let e2 = Z3.Quantifier.get_body eq in

862

(* Format.eprintf "Extracted quantifier body@ "; *) e2

863


864

with _ > Format.eprintf "No quantifier info@ "; e in let _ = try ( let fd =

865

Z3.Expr.get_func_decl e in let fd_symbol = Z3.FuncDecl.get_name fd in let

866

fd_name = Z3.Symbol.to_string fd_symbol in if not (Hashtbl.mem decls fd_name)

867

then register_fdecl fd_name fd; (* Format.eprintf "fdecls (%s): %s@ " *) (*

868

fd_name *) (* (Z3.FuncDecl.to_string fd); *) try ( let args =

869

Z3.Expr.get_args e in (* Format.eprintf "@[<v>@ "; *) (* List.iter

870

extract_expr_fds args; *) (* Format.eprintf "@]@ "; *) () ) with _ >

871

Format.eprintf "Impossible to extract fundecl args for expression %s@ "

872

(Z3.Expr.to_string e) ) with _ > Format.eprintf "Impossible to extract

873

anything from expression %s@ " (Z3.Expr.to_string e) in (* Format.eprintf

874

"@]@ " *) () *)

875

(* Local Variables: *)

876

(* compilecommand:"make C ../.." *)

877

(* End: *)
