1

open Lustre_types

2

open Machine_code_types

3

open Machine_code_common

4

open Format

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

let node_name = HBC.node_name

13


14

let concat = HBC.concat

15


16

let rename_machine = HBC.rename_machine

17

let rename_machine_list = HBC.rename_machine_list

18


19

let rename_next = HBC.rename_next

20

let rename_mid = HBC.rename_mid

21

let rename_current = HBC.rename_current

22


23

let rename_current_list = HBC.rename_current_list

24

let rename_mid_list = HBC.rename_mid_list

25

let rename_next_list = HBC.rename_next_list

26


27

let full_memory_vars = HBC.full_memory_vars

28

let inout_vars = HBC.inout_vars

29

let reset_vars = HBC.reset_vars

30

let step_vars = HBC.step_vars

31

let local_memory_vars = HBC.local_memory_vars

32

let step_vars_m_x = HBC.step_vars_m_x

33

let step_vars_c_m_x = HBC.step_vars_c_m_x

34


35

let machine_reset_name = HBC.machine_reset_name

36

let machine_step_name = HBC.machine_step_name

37

let machine_stateless_name = HBC.machine_stateless_name

38


39

let preprocess = Horn_backend.preprocess

40


41


42

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

43

(** Sorts

44


45

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

46


47

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

48

provided with a enumerated type name.

49


50

*)

51


52

let bool_sort = Z3.Boolean.mk_sort !ctx

53

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

54

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

55


56


57

let get_const_sort = Hashtbl.find const_sorts

58

let get_sort_elems = Hashtbl.find sort_elems

59

let get_tag_sort id = try Hashtbl.find const_tags id with _ > Format.eprintf "Unable to find sort for tag=%s@." id; assert false

60


61


62


63

let decl_sorts () =

64

Hashtbl.iter (fun typ decl >

65

match typ with

66

 Tydec_const var >

67

(match decl.top_decl_desc with

68

 TypeDef tdef > (

69

match tdef.tydef_desc with

70

 Tydec_enum tl >

71

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

72

Hashtbl.add const_sorts var new_sort;

73

Hashtbl.add sort_elems new_sort tl;

74

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

75


76

 _ > Format.eprintf "Unknown type : %a@.@?" Printers.pp_var_type_dec_desc typ; assert false

77

)

78

 _ > assert false

79

)

80

 _ > ()) Corelang.type_table

81


82


83

let rec type_to_sort t =

84

if Types.is_bool_type t then bool_sort else

85

if Types.is_int_type t then int_sort else

86

if Types.is_real_type t then real_sort else

87

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

88

 Types.Tconst ty > get_const_sort ty

89

 Types.Tclock t > type_to_sort t

90

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

91

 Types.Tstatic(d, ty)> type_to_sort ty

92

 Types.Tarrow _

93

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

94

Types.print_ty t; assert false

95


96


97

(* let idx_var = *)

98

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

99


100

(* let uid_var = *)

101

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

102


103

(** Func decls

104


105

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

106

proposed encoding introduces a 0ary fun_decl to model variables and

107

fun_decl with arguments to declare reset and step predicates.

108


109


110


111

*)

112

let register_fdecl id fd = Hashtbl.add decls id fd

113

let get_fdecl id =

114

try

115

Hashtbl.find decls id

116

with Not_found > (report ~level:3 (fun fmt > Format.fprintf fmt "Unable to find func_decl %s@.@?" id); raise Not_found)

117


118

let pp_fdecls fmt =

119

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

120

(Utils.fprintf_list ~sep:"@ " Format.pp_print_string) (Hashtbl.fold (fun id _ accu > id::accu) decls [])

121


122


123

let decl_var id =

124

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

125

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

126

register_fdecl id.var_id fdecl;

127

fdecl

128


129

(* Declaring the function used in expr *)

130

let decl_fun op args typ =

131

let args = List.map type_to_sort args in

132

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

133

register_fdecl op fdecl;

134

fdecl

135


136

let idx_sort = int_sort

137

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

138

let uid_conc =

139

let fd = Z3.Z3List.get_cons_decl uid_sort in

140

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

141


142

let get_instance_uid =

143

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

144

let cpt = ref 0 in

145

fun i >

146

let id =

147

if Hashtbl.mem hash i then

148

Hashtbl.find hash i

149

else (

150

incr cpt;

151

Hashtbl.add hash i !cpt;

152

!cpt

153

)

154

in

155

Z3.Arithmetic.Integer.mk_numeral_i !ctx id

156


157


158


159

let decl_rel ?(no_additional_vars=false) name args_sorts =

160

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

161

uid *)

162

let args_sorts =

163

if no_additional_vars then args_sorts else idx_sort::uid_sort::args_sorts in

164


165

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

166

if !debug then

167

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

168

name

169

(Utils.fprintf_list ~sep:"@ "

170

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

171

args_sorts

172

;

173

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

174

Z3.Fixedpoint.register_relation !fp fdecl;

175

register_fdecl name fdecl;

176

fdecl

177


178


179


180

(* Shared variables to describe counter and uid *)

181


182

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

183

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

184

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

185

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

186

let _ = register_fdecl "__uid__" uid_fd

187

let uid_var = Z3.Expr.mk_const_f !ctx uid_fd

188


189

(** Conversion functions

190


191

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

192

rephrased from pp_xx to xx_to_expr and produces a Z3 value.

193


194

*)

195


196


197

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

198

let horn_var_to_expr v =

199

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

200


201


202


203


204

(* Used to print boolean constants *)

205

let horn_tag_to_expr t =

206

if t = tag_true then

207

Z3.Boolean.mk_true !ctx

208

else if t = tag_false then

209

Z3.Boolean.mk_false !ctx

210

else

211

(* Finding the associated sort *)

212

let sort = get_tag_sort t in

213

let elems = get_sort_elems sort in

214

let res : Z3.Expr.expr option =

215

List.fold_left2 (fun res cst expr >

216

match res with

217

 Some _ > res

218

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

219

) None elems (Z3.Enumeration.get_consts sort)

220

in

221

match res with None > assert false  Some s > s

222


223

(* Prints a constant value *)

224

let rec horn_const_to_expr c =

225

match c with

226

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

227

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

228

 Const_tag t > horn_tag_to_expr t

229

 _ > assert false

230


231


232


233

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

234

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

235

for the type integer (arrays).

236

*)

237

let rec horn_default_val t =

238

let t = Types.dynamic_type t in

239

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

240

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

241

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

242

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

243

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

244

* let valt = Types.array_element_type t in

245

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

246

* pp_type valt

247

* pp_default_val valt

248

*  Types.Tstruct(l) > assert false

249

*  Types.Ttuple(l) > assert false

250

* _ > *) assert false

251


252

(* Conversion of basic library functions *)

253


254

let horn_basic_app i vl (vltyp, typ) =

255

match i, vl with

256

 "ite", [v1; v2; v3] > Z3.Boolean.mk_ite !ctx v1 v2 v3

257

 "uminus", [v] > Z3.Arithmetic.mk_unary_minus

258

!ctx v

259

 "not", [v] >

260

Z3.Boolean.mk_not

261

!ctx v

262

 "=", [v1; v2] >

263

Z3.Boolean.mk_eq

264

!ctx v1 v2

265

 "&&", [v1; v2] >

266

Z3.Boolean.mk_and

267

!ctx

268

[v1; v2]

269

 "", [v1; v2] >

270

Z3.Boolean.mk_or

271

!ctx

272

[v1;

273

v2]

274


275

 "impl", [v1; v2] >

276

Z3.Boolean.mk_implies

277

!ctx v1 v2

278

 "mod", [v1; v2] >

279

Z3.Arithmetic.Integer.mk_mod

280

!ctx v1 v2

281

 "equi", [v1; v2] >

282

Z3.Boolean.mk_eq

283

!ctx

284

v1 v2

285

 "xor", [v1; v2] >

286

Z3.Boolean.mk_xor

287

!ctx v1 v2

288

 "!=", [v1; v2] >

289

Z3.Boolean.mk_not

290

!ctx

291

(

292

Z3.Boolean.mk_eq

293

!ctx v1 v2

294

)

295

 "/", [v1; v2] >

296

Z3.Arithmetic.mk_div

297

!ctx v1 v2

298


299

 "+", [v1; v2] >

300

Z3.Arithmetic.mk_add

301

!ctx

302

[v1; v2]

303

 "", [v1; v2] >

304

Z3.Arithmetic.mk_sub

305

!ctx

306

[v1 ; v2]

307


308

 "*", [v1; v2] >

309

Z3.Arithmetic.mk_mul

310

!ctx

311

[ v1; v2]

312


313


314

 "<", [v1; v2] >

315

Z3.Arithmetic.mk_lt

316

!ctx v1 v2

317

 "<=", [v1; v2] >

318

Z3.Arithmetic.mk_le

319

!ctx v1 v2

320

 ">", [v1; v2] >

321

Z3.Arithmetic.mk_gt

322

!ctx v1 v2

323

 ">=", [v1; v2] >

324

Z3.Arithmetic.mk_ge

325

!ctx v1 v2

326

 "int_to_real", [v1] >

327

Z3.Arithmetic.Integer.mk_int2real

328

!ctx v1

329

 _ >

330

let fd =

331

try

332

get_fdecl i

333

with Not_found > begin

334

report ~level:3 (fun fmt > Format.fprintf fmt "Registering function %s as uninterpreted function in Z3@.%s: (%a) > %a" i i (Utils.fprintf_list ~sep:"," Types.print_ty) vltyp Types.print_ty typ);

335

decl_fun i vltyp typ

336

end

337

in

338

Z3.FuncDecl.apply fd vl

339


340


341

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

342

* !ctx

343

* (val_to_expr v1)

344

* (val_to_expr v2)

345

*

346

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

347


348

(*  _ > (

349

* let msg fmt = Format.fprintf fmt

350

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

351

* i (List.length vl)

352

* in

353

* raise (UnknownFunction(i, msg))

354

* ) *)

355


356


357

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

358

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

359

may be added for array variables

360

*)

361

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

362

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

363

match v.value_desc with

364

 Cst c > horn_const_to_expr c

365


366

(* Code specific for arrays *)

367

 Array il >

368

(* An array definition:

369

(store (

370

...

371

(store (

372

store (

373

default_val

374

)

375

idx_n val_n

376

)

377

idx_n1 val_n1)

378

...

379

idx_1 val_1

380

) *)

381

let rec build_array (tab, x) =

382

match tab with

383

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

384

 h::t >

385

Z3.Z3Array.mk_store

386

!ctx

387

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

388

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

389

(horn_val_to_expr ~is_lhs:is_lhs m self h)

390

in

391

build_array (il, 0)

392


393

 Access(tab,index) >

394

Z3.Z3Array.mk_select !ctx

395

(horn_val_to_expr ~is_lhs:is_lhs m self tab)

396

(horn_val_to_expr ~is_lhs:is_lhs m self index)

397


398

(* Code specific for arrays *)

399


400

 Power (v, n) > assert false

401

 Var v >

402

if is_memory m v then

403

if Types.is_array_type v.var_type

404

then assert false

405

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

406


407

else

408

horn_var_to_expr

409

(rename_machine

410

self

411

v)

412

 Fun (n, vl) > horn_basic_app n (List.map (horn_val_to_expr m self) vl) (List.map (fun v > v.value_type) vl, v.value_type)

413


414

let no_reset_to_exprs machines m i =

415

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

416

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

417


418

let m_list =

419

rename_machine_list

420

(concat m.mname.node_id i)

421

(rename_mid_list (full_memory_vars machines target_machine))

422

in

423

let c_list =

424

rename_machine_list

425

(concat m.mname.node_id i)

426

(rename_current_list (full_memory_vars machines target_machine))

427

in

428

match c_list, m_list with

429

 [chd], [mhd] >

430

let expr =

431

Z3.Boolean.mk_eq !ctx

432

(horn_var_to_expr mhd)

433

(horn_var_to_expr chd)

434

in

435

[expr]

436

 _ > (

437

let exprs =

438

List.map2 (fun mhd chd >

439

Z3.Boolean.mk_eq !ctx

440

(horn_var_to_expr mhd)

441

(horn_var_to_expr chd)

442

)

443

m_list

444

c_list

445

in

446

exprs

447

)

448


449

let instance_reset_to_exprs machines m i =

450

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

451

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

452

let vars =

453

(rename_machine_list

454

(concat m.mname.node_id i)

455

(rename_current_list (full_memory_vars machines target_machine))@ (rename_mid_list (full_memory_vars machines target_machine))

456

)

457


458

in

459

let expr =

460

Z3.Expr.mk_app

461

!ctx

462

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

463

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

464

in

465

[expr]

466


467

let instance_call_to_exprs machines reset_instances m i inputs outputs =

468

let self = m.mname.node_id in

469


470

(* Building call args *)

471

let idx_uid_inout =

472

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

473

let idx = horn_var_to_expr idx in

474

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

475

let inout =

476

List.map (horn_val_to_expr m self)

477

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

478

in

479

idx::uid::inout

480

in

481


482

try (* stateful node instance *)

483

begin

484

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

485

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

486


487

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

488

let reset_exprs =

489

if not (List.mem i reset_instances) then

490

(* If not, declare mem_m = mem_c *)

491

no_reset_to_exprs machines m i

492

else

493

[] (* Nothing to add yet *)

494

in

495


496

let mems = full_memory_vars machines target_machine in

497

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

498

let mid_mems = rename_mems rename_mid_list in

499

let next_mems = rename_mems rename_next_list in

500


501

let call_expr =

502

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

503

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

504

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

505

Z3.Boolean.mk_eq !ctx

506

( (* output var *)

507

horn_val_to_expr

508

~is_lhs:true

509

m self

510

(mk_val (Var o) o.var_type)

511

)

512

(

513

Z3.Boolean.mk_ite !ctx

514

(horn_var_to_expr mem_m)

515

(horn_val_to_expr m self i1)

516

(horn_val_to_expr m self i2)

517

)

518

in

519

let stmt2 = (* mem_X = false *)

520

Z3.Boolean.mk_eq !ctx

521

(horn_var_to_expr mem_x)

522

(Z3.Boolean.mk_false !ctx)

523

in

524

[stmt1; stmt2]

525

end

526


527

 node_name_n >

528

let expr =

529

Z3.Expr.mk_app

530

!ctx

531

(get_fdecl (machine_step_name (node_name n)))

532

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

533

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

534


535

)

536

in

537

[expr]

538

in

539


540

reset_exprs@call_expr

541

end

542

with Not_found > ( (* stateless node instance *)

543

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

544

let expr =

545

Z3.Expr.mk_app

546

!ctx

547

(get_fdecl (machine_stateless_name (node_name n)))

548

idx_uid_inout (* Arguments are inputs, outputs *)

549

in

550

[expr]

551

)

552


553


554


555

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

556

(* let rec value_suffix_to_expr self value = *)

557

(* match value.value_desc with *)

558

(*  Fun (n, vl) > *)

559

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

560


561

(*  _ > *)

562

(* horn_val_to_expr self value *)

563


564


565

(* type_directed assignment: array vs. statically sized type

566

 [var_type]: type of variable to be assigned

567

 [var_name]: name of variable to be assigned

568

 [value]: assigned value

569

 [pp_var]: printer for variables

570

*)

571

let assign_to_exprs m var_name value =

572

let self = m.mname.node_id in

573

let e =

574

Z3.Boolean.mk_eq

575

!ctx

576

(horn_val_to_expr ~is_lhs:true m self var_name)

577

(horn_val_to_expr m self value)

578

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

579

in

580

[e]

581


582


583

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

584

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

585

match Corelang.get_instr_desc instr with

586

 MComment _ > [], reset_instances

587

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

588

no_reset_to_exprs machines m i,

589

i::reset_instances

590

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

591

instance_reset_to_exprs machines m i,

592

i::reset_instances

593

 MLocalAssign (i,v) >

594

assign_to_exprs

595

m

596

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

597

reset_instances

598

 MStateAssign (i,v) >

599

assign_to_exprs

600

m

601

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

602

reset_instances

603

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

604

assert false (* This should not happen anymore *)

605

 MStep (il, i, vl) >

606

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

607

mem_c and print the call to mem_m *)

608

instance_call_to_exprs machines reset_instances m i vl il,

609

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

610

don't have to update reset_instances *)

611


612

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

613

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

614

compare the reset_instances of each branch and

615

introduced the mem_m = mem_c for branches to do not

616

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

617

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

618

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

619

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

620

statement. *)

621

let self = m.mname.node_id in

622

let branch_to_expr (tag, instrs) =

623

let branch_def, branch_resets = instrs_to_expr machines reset_instances m instrs in

624

let e =

625

Z3.Boolean.mk_implies !ctx

626

(Z3.Boolean.mk_eq !ctx

627

(horn_val_to_expr m self g)

628

(horn_tag_to_expr tag))

629

branch_def in

630


631

[e], branch_resets

632


633

in

634

List.fold_left (fun (instrs, resets) b >

635

let b_instrs, b_resets = branch_to_expr b in

636

instrs@b_instrs, resets@b_resets

637

) ([], reset_instances) hl

638

 MSpec _ > assert false

639


640

and instrs_to_expr machines reset_instances m instrs =

641

let instr_to_exprs rs i = instr_to_exprs machines rs m i in

642

let e_list, rs =

643

match instrs with

644

 [x] > instr_to_exprs reset_instances x

645

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

646


647

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

648

let exprs_i, rs_i = instr_to_exprs rs i in

649

exprs@exprs_i, rs@rs_i

650

)

651

([], reset_instances) instrs

652


653


654

 [] > [], reset_instances

655

in

656

let e =

657

match e_list with

658

 [e] > e

659

 [] > Z3.Boolean.mk_true !ctx

660

 _ > Z3.Boolean.mk_and !ctx e_list

661

in

662

e, rs

663


664


665

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

666


667

(* Quantifiying universally all occuring variables *)

668

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

669

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

670

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

671

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

672

(* (Utils.fprintf_list ~sep:", " (fun fmt e > Format.pp_print_string fmt (Z3.Expr.to_string e))) fds; *)

673


674

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

675

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

676

(* let symbols = (List.map (fun id > Z3.FuncDecl.get_name (get_fdecl id.var_id)) vars) in *)

677


678

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

679

let module FDSet = Set.Make (struct type t = Z3.FuncDecl.func_decl

680

let compare = compare

681

let hash = Hashtbl.hash

682

end)

683

in

684

(* Fonction seems unused

685


686

let rec get_expr_vars e =

687

let open Utils in

688

let nb_args = Z3.Expr.get_num_args e in

689

if nb_args <= 0 then (

690

let fdecl = Z3.Expr.get_func_decl e in

691

(* let params = Z3.FuncDecl.get_parameters fdecl in *)

692

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

693

let dkind = Z3.FuncDecl.get_decl_kind fdecl in

694

match dkind with Z3enums.OP_UNINTERPRETED > (

695

(* Format.eprintf "kind = %s, " (match dkind with Z3enums.OP_TRUE > "true"  Z3enums.OP_UNINTERPRETED > "uninter"); *)

696

(* let open Z3.FuncDecl.Parameter in *)

697

(* List.iter (fun p > *)

698

(* match p with *)

699

(* P_Int i > Format.eprintf "int %i" i *)

700

(*  P_Dbl f > Format.eprintf "dbl %f" f *)

701

(*  P_Sym s > Format.eprintf "symb" *)

702

(*  P_Srt s > Format.eprintf "sort" *)

703

(*  P_Ast _ >Format.eprintf "ast" *)

704

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

705

(*  P_Rat s > Format.eprintf "rat %s" s *)

706


707

(* ) params; *)

708

(* Format.eprintf "]@."; *)

709

FDSet.singleton fdecl

710

)

711

 _ > FDSet.empty

712

)

713

else (*if nb_args > 0 then*)

714

List.fold_left

715

(fun accu e > FDSet.union accu (get_expr_vars e))

716

FDSet.empty (Z3.Expr.get_args e)

717

in

718

*)

719

(* Unsed variable. Coul;d be reintroduced

720

let extracted_vars = FDSet.elements (FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in

721

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

722

let extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in

723

*)

724

if !debug then (

725

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

726

(Z3.Expr.to_string expr)

727

(Utils.fprintf_list ~sep:",@ " (fun fmt e > Format.fprintf fmt "%s" (Z3.Expr.to_string e))) (List.map horn_var_to_expr vars)

728

)

729

;

730

let expr = Z3.Quantifier.mk_forall_const

731

!ctx (* context *)

732

(List.map horn_var_to_expr vars) (* TODO provide bounded variables as expr *)

733

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

734

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

735

expr (* expression *)

736

None (* quantifier weight, None means 1 *)

737

[] (* pattern list ? *)

738

[] (* ? *)

739

None (* ? *)

740

None (* ? *)

741

in

742

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

743


744

(*

745

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

746

*)

747

Z3.Fixedpoint.add_rule !fp

748

(Z3.Quantifier.expr_of_quantifier expr)

749

None

750


751


752

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

753


754

let machine_reset machines m =

755

let locals = local_memory_vars machines m in

756


757

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

758

let mid_mem_def =

759

List.map (fun v >

760

Z3.Boolean.mk_eq !ctx

761

(horn_var_to_expr (rename_mid v))

762

(horn_var_to_expr (rename_current v))

763

) locals

764

in

765


766

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

767

Special treatment for _arrow: _first = true

768

*)

769


770

let reset_instances =

771


772

List.map (fun (id, (n, _)) >

773

let name = node_name n in

774

if name = "_arrow" then (

775

Z3.Boolean.mk_eq !ctx

776

(

777

let vdecl = get_fdecl ((concat m.mname.node_id id) ^ "._arrow._first_m") in

778

Z3.Expr.mk_const_f !ctx vdecl

779

)

780

(Z3.Boolean.mk_true !ctx)

781


782

) else (

783

let machine_n = get_machine machines name in

784


785

Z3.Expr.mk_app

786

!ctx

787

(get_fdecl (name ^ "_reset"))

788

(List.map (horn_var_to_expr)

789

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

790

(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))

791

))

792


793

)

794

) m.minstances

795


796


797

in

798


799

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

800


801


802


803

(* TODO: empty list means true statement *)

804

let decl_machine machines m =

805

if m.mname.node_id = Arrow.arrow_id then

806

(* We don't do arrow function *)

807

()

808

else

809

begin

810

let _ =

811

List.map decl_var

812

(

813

(inout_vars machines m)@

814

(rename_current_list (full_memory_vars machines m)) @

815

(rename_mid_list (full_memory_vars machines m)) @

816

(rename_next_list (full_memory_vars machines m)) @

817

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

818

)

819

in

820

if is_stateless m then

821

begin

822

if !debug then

823

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

824


825

(* Declaring single predicate *)

826

let vars = inout_vars machines m in

827

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

828

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

829


830

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

831

instrs_to_expr

832

machines

833

([] (* No reset info for stateless nodes *) )

834

m

835

m.mstep.step_instrs

836

in

837

let horn_head =

838

Z3.Expr.mk_app

839

!ctx

840

(get_fdecl (machine_stateless_name m.mname.node_id))

841

( List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars))

842

in

843

(* this line seems useless *)

844

let vars = idx::uid::vars@(rename_machine_list m.mname.node_id m.mstep.step_locals) in

845

(* Format.eprintf "useless Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *)

846

match m.mstep.step_asserts with

847

 [] >

848

begin

849

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

850

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

851

(* TODO clean code *)

852

(* Format.eprintf "used Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *)

853

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

854


855

end

856

 assertsl >

857

begin

858

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

859

let body_with_asserts =

860

Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl)

861

in

862

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

863

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

864

end

865

end

866

else

867

begin

868


869

(* Rule for reset *)

870


871

let vars = reset_vars machines m in

872

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

873

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

874

let horn_reset_body = machine_reset machines m in

875

let horn_reset_head =

876

Z3.Expr.mk_app

877

!ctx

878

(get_fdecl (machine_reset_name m.mname.node_id))

879

( List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars))

880

in

881


882


883

let _ =

884

add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)

885


886

in

887


888

(* Rule for step*)

889

let vars = step_vars machines m in

890

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

891

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

892

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

893

instrs_to_expr

894

machines

895

[]

896

m

897

m.mstep.step_instrs

898

in

899

let horn_step_head =

900

Z3.Expr.mk_app

901

!ctx

902

(get_fdecl (machine_step_name m.mname.node_id))

903

( List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars))

904

in

905

match m.mstep.step_asserts with

906

 [] >

907

begin

908

(* Rule for single predicate *)

909

let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in

910

add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)

911


912

end

913

 assertsl >

914

begin

915

(* Rule for step Assertions @.; *)

916

let body_with_asserts =

917

Z3.Boolean.mk_and !ctx

918

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

919

in

920

let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in

921

add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)

922


923

end

924


925

end

926

end

927


928


929


930

(* Debug functions *)

931

(*

932

let rec extract_expr_fds e =

933

(* Format.eprintf "@[<v 2>Extracting fundecls from expr %s@ " *)

934

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

935


936

(* Removing quantifier is there are some *)

937

let e = (* I didn't found a nicer way to do it than with an exception. My

938

bad *)

939

try

940

let eq = Z3.Quantifier.quantifier_of_expr e in

941

let e2 = Z3.Quantifier.get_body eq in

942

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

943

e2

944


945

with _ > Format.eprintf "No quantifier info@ "; e

946

in

947

let _ =

948

try

949

(

950

let fd = Z3.Expr.get_func_decl e in

951

let fd_symbol = Z3.FuncDecl.get_name fd in

952

let fd_name = Z3.Symbol.to_string fd_symbol in

953

if not (Hashtbl.mem decls fd_name) then

954

register_fdecl fd_name fd;

955

(* Format.eprintf "fdecls (%s): %s@ " *)

956

(* fd_name *)

957

(* (Z3.FuncDecl.to_string fd); *)

958

try

959

(

960

let args = Z3.Expr.get_args e in

961

(* Format.eprintf "@[<v>@ "; *)

962

(* List.iter extract_expr_fds args; *)

963

(* Format.eprintf "@]@ "; *)

964

()

965

)

966

with _ >

967

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

968

(Z3.Expr.to_string e)

969

)

970

with _ >

971

Format.eprintf "Impossible to extract anything from expression %s@ "

972

(Z3.Expr.to_string e)

973

in

974

(* Format.eprintf "@]@ " *)

975

()

976

*)

977

(* Local Variables: *)

978

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

979

(* End: *)
