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

module HBC = Horn_backend_common

10

let node_name = HBC.node_name

11


12

let concat = HBC.concat

13


14

let rename_machine = HBC.rename_machine

15

let rename_machine_list = HBC.rename_machine_list

16


17

let rename_next = HBC.rename_next

18

let rename_mid = HBC.rename_mid

19

let rename_current = HBC.rename_current

20


21

let rename_current_list = HBC.rename_current_list

22

let rename_mid_list = HBC.rename_mid_list

23

let rename_next_list = HBC.rename_next_list

24


25

let full_memory_vars = HBC.full_memory_vars

26

let inout_vars = HBC.inout_vars

27

let reset_vars = HBC.reset_vars

28

let step_vars = HBC.step_vars

29

let local_memory_vars = HBC.local_memory_vars

30

let step_vars_m_x = HBC.step_vars_m_x

31

let step_vars_c_m_x = HBC.step_vars_c_m_x

32


33

let machine_reset_name = HBC.machine_reset_name

34

let machine_step_name = HBC.machine_step_name

35

let machine_stateless_name = HBC.machine_stateless_name

36


37

let preprocess = Horn_backend.preprocess

38


39


40

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

41

(** Sorts

42


43

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

44


45

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

46

provided with a enumerated type name.

47


48

*)

49


50

let bool_sort = Z3.Boolean.mk_sort !ctx

51

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

52

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

53


54


55

let get_const_sort = Hashtbl.find const_sorts

56

let get_sort_elems = Hashtbl.find sort_elems

57

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

58


59


60


61

let decl_sorts () =

62

Hashtbl.iter (fun typ decl >

63

match typ with

64

 Tydec_const var >

65

(match decl.top_decl_desc with

66

 TypeDef tdef > (

67

match tdef.tydef_desc with

68

 Tydec_enum tl >

69

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

70

Hashtbl.add const_sorts var new_sort;

71

Hashtbl.add sort_elems new_sort tl;

72

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

73


74

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

75

)

76

 _ > assert false

77

)

78

 _ > ()) Corelang.type_table

79


80


81

let rec type_to_sort t =

82

if Types.is_bool_type t then bool_sort else

83

if Types.is_int_type t then int_sort else

84

if Types.is_real_type t then real_sort else

85

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

86

 Types.Tconst ty > get_const_sort ty

87

 Types.Tclock t > type_to_sort t

88

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

89

 Types.Tstatic(d, ty)> type_to_sort ty

90

 Types.Tarrow _

91

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

92

Types.print_ty t; assert false

93


94


95

(* let idx_var = *)

96

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

97


98

(* let uid_var = *)

99

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

100


101

(** Func decls

102


103

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

104

proposed encoding introduces a 0ary fun_decl to model variables and

105

fun_decl with arguments to declare reset and step predicates.

106


107


108


109

*)

110

let register_fdecl id fd = Hashtbl.add decls id fd

111

let get_fdecl id =

112

try

113

Hashtbl.find decls id

114

with Not_found > (Format.eprintf "Unable to find func_decl %s@.@?" id; raise Not_found)

115


116

let pp_fdecls fmt =

117

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

118

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

119


120


121

let decl_var id =

122

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

123

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

124

register_fdecl id.var_id fdecl;

125

fdecl

126


127

let idx_sort = int_sort

128

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

129

let uid_conc =

130

let fd = Z3.Z3List.get_cons_decl uid_sort in

131

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

132


133

let get_instance_uid =

134

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

135

let cpt = ref 0 in

136

fun i >

137

let id =

138

if Hashtbl.mem hash i then

139

Hashtbl.find hash i

140

else (

141

incr cpt;

142

Hashtbl.add hash i !cpt;

143

!cpt

144

)

145

in

146

Z3.Arithmetic.Integer.mk_numeral_i !ctx id

147


148


149


150

let decl_rel ?(no_additional_vars=false) name args_sorts =

151

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

152

uid *)

153

let args_sorts =

154

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

155


156

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

157

if !debug then

158

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

159

name

160

(Utils.fprintf_list ~sep:"@ "

161

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

162

args_sorts

163

;

164

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

165

Z3.Fixedpoint.register_relation !fp fdecl;

166

register_fdecl name fdecl;

167

fdecl

168


169


170


171

(* Shared variables to describe counter and uid *)

172


173

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

174

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

175

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

176

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

177

let _ = register_fdecl "__uid__" uid_fd

178

let uid_var = Z3.Expr.mk_const_f !ctx uid_fd

179


180

(** Conversion functions

181


182

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

183

rephrased from pp_xx to xx_to_expr and produces a Z3 value.

184


185

*)

186


187


188

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

189

let horn_var_to_expr v =

190

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

191


192


193


194


195

(* Used to print boolean constants *)

196

let horn_tag_to_expr t =

197

if t = tag_true then

198

Z3.Boolean.mk_true !ctx

199

else if t = tag_false then

200

Z3.Boolean.mk_false !ctx

201

else

202

(* Finding the associated sort *)

203

let sort = get_tag_sort t in

204

let elems = get_sort_elems sort in

205

let res : Z3.Expr.expr option =

206

List.fold_left2 (fun res cst expr >

207

match res with

208

 Some _ > res

209

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

210

) None elems (Z3.Enumeration.get_consts sort)

211

in

212

match res with None > assert false  Some s > s

213


214

(* Prints a constant value *)

215

let rec horn_const_to_expr c =

216

match c with

217

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

218

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

219

 Const_tag t > horn_tag_to_expr t

220

 _ > assert false

221


222


223


224

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

225

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

226

for the type integer (arrays).

227

*)

228

let rec horn_default_val t =

229

let t = Types.dynamic_type t in

230

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

231

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

232

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

233

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

234

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

235

* let valt = Types.array_element_type t in

236

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

237

* pp_type valt

238

* pp_default_val valt

239

*  Types.Tstruct(l) > assert false

240

*  Types.Ttuple(l) > assert false

241

* _ > *) assert false

242


243

(* Conversion of basic library functions *)

244


245

let horn_basic_app i val_to_expr vl =

246

match i, vl with

247

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

248

Z3.Boolean.mk_ite

249

!ctx

250

(val_to_expr v1)

251

(val_to_expr v2)

252

(val_to_expr v3)

253


254

 "uminus", [v] >

255

Z3.Arithmetic.mk_unary_minus

256

!ctx

257

(val_to_expr v)

258

 "not", [v] >

259

Z3.Boolean.mk_not

260

!ctx

261

(val_to_expr v)

262

 "=", [v1; v2] >

263

Z3.Boolean.mk_eq

264

!ctx

265

(val_to_expr v1)

266

(val_to_expr v2)

267

 "&&", [v1; v2] >

268

Z3.Boolean.mk_and

269

!ctx

270

[val_to_expr v1;

271

val_to_expr v2]

272

 "", [v1; v2] >

273

Z3.Boolean.mk_or

274

!ctx

275

[val_to_expr v1;

276

val_to_expr v2]

277


278

 "impl", [v1; v2] >

279

Z3.Boolean.mk_implies

280

!ctx

281

(val_to_expr v1)

282

(val_to_expr v2)

283

 "mod", [v1; v2] >

284

Z3.Arithmetic.Integer.mk_mod

285

!ctx

286

(val_to_expr v1)

287

(val_to_expr v2)

288

 "equi", [v1; v2] >

289

Z3.Boolean.mk_eq

290

!ctx

291

(val_to_expr v1)

292

(val_to_expr v2)

293

 "xor", [v1; v2] >

294

Z3.Boolean.mk_xor

295

!ctx

296

(val_to_expr v1)

297

(val_to_expr v2)

298

 "!=", [v1; v2] >

299

Z3.Boolean.mk_not

300

!ctx

301

(

302

Z3.Boolean.mk_eq

303

!ctx

304

(val_to_expr v1)

305

(val_to_expr v2)

306

)

307

 "/", [v1; v2] >

308

Z3.Arithmetic.mk_div

309

!ctx

310

(val_to_expr v1)

311

(val_to_expr v2)

312


313

 "+", [v1; v2] >

314

Z3.Arithmetic.mk_add

315

!ctx

316

[val_to_expr v1; val_to_expr v2]

317


318

 "", [v1; v2] >

319

Z3.Arithmetic.mk_sub

320

!ctx

321

[val_to_expr v1 ; val_to_expr v2]

322


323

 "*", [v1; v2] >

324

Z3.Arithmetic.mk_mul

325

!ctx

326

[val_to_expr v1; val_to_expr v2]

327


328


329

 "<", [v1; v2] >

330

Z3.Arithmetic.mk_lt

331

!ctx

332

(val_to_expr v1)

333

(val_to_expr v2)

334


335

 "<=", [v1; v2] >

336

Z3.Arithmetic.mk_le

337

!ctx

338

(val_to_expr v1)

339

(val_to_expr v2)

340


341

 ">", [v1; v2] >

342

Z3.Arithmetic.mk_gt

343

!ctx

344

(val_to_expr v1)

345

(val_to_expr v2)

346


347

 ">=", [v1; v2] >

348

Z3.Arithmetic.mk_ge

349

!ctx

350

(val_to_expr v1)

351

(val_to_expr v2)

352


353

 "int_to_real", [v1] >

354

Z3.Arithmetic.Integer.mk_int2real

355

!ctx

356

(val_to_expr v1)

357


358


359

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

360

* !ctx

361

* (val_to_expr v1)

362

* (val_to_expr v2)

363

*

364

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

365

 _ > (

366

let msg fmt = Format.fprintf fmt

367

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

368

i (List.length vl)

369

in

370

raise (UnknownFunction(i, msg))

371

)

372


373


374

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

375

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

376

may be added for array variables

377

*)

378

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

379

match v.value_desc with

380

 Cst c > horn_const_to_expr c

381


382

(* Code specific for arrays *)

383

 Array il >

384

(* An array definition:

385

(store (

386

...

387

(store (

388

store (

389

default_val

390

)

391

idx_n val_n

392

)

393

idx_n1 val_n1)

394

...

395

idx_1 val_1

396

) *)

397

let rec build_array (tab, x) =

398

match tab with

399

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

400

 h::t >

401

Z3.Z3Array.mk_store

402

!ctx

403

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

404

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

405

(horn_val_to_expr ~is_lhs:is_lhs m self h)

406

in

407

build_array (il, 0)

408


409

 Access(tab,index) >

410

Z3.Z3Array.mk_select !ctx

411

(horn_val_to_expr ~is_lhs:is_lhs m self tab)

412

(horn_val_to_expr ~is_lhs:is_lhs m self index)

413


414

(* Code specific for arrays *)

415


416

 Power (v, n) > assert false

417

 Var v >

418

if is_memory m v then

419

if Types.is_array_type v.var_type

420

then assert false

421

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

422


423

else

424

horn_var_to_expr

425

(rename_machine

426

self

427

v)

428

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

429


430

let no_reset_to_exprs machines m i =

431

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

432

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

433


434

let m_list =

435

rename_machine_list

436

(concat m.mname.node_id i)

437

(rename_mid_list (full_memory_vars machines target_machine))

438

in

439

let c_list =

440

rename_machine_list

441

(concat m.mname.node_id i)

442

(rename_current_list (full_memory_vars machines target_machine))

443

in

444

match c_list, m_list with

445

 [chd], [mhd] >

446

let expr =

447

Z3.Boolean.mk_eq !ctx

448

(horn_var_to_expr mhd)

449

(horn_var_to_expr chd)

450

in

451

[expr]

452

 _ > (

453

let exprs =

454

List.map2 (fun mhd chd >

455

Z3.Boolean.mk_eq !ctx

456

(horn_var_to_expr mhd)

457

(horn_var_to_expr chd)

458

)

459

m_list

460

c_list

461

in

462

exprs

463

)

464


465

let instance_reset_to_exprs machines m i =

466

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

467

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

468

let vars =

469

(rename_machine_list

470

(concat m.mname.node_id i)

471

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

472

)

473


474

in

475

let expr =

476

Z3.Expr.mk_app

477

!ctx

478

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

479

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

480

in

481

[expr]

482


483

let instance_call_to_exprs machines reset_instances m i inputs outputs =

484

let self = m.mname.node_id in

485


486

(* Building call args *)

487

let idx_uid_inout =

488

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

489

let idx = horn_var_to_expr idx in

490

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

491

let inout =

492

List.map (horn_val_to_expr m self)

493

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

494

in

495

idx::uid::inout

496

in

497


498

try (* stateful node instance *)

499

begin

500

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

501

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

502


503

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

504

let reset_exprs =

505

if not (List.mem i reset_instances) then

506

(* If not, declare mem_m = mem_c *)

507

no_reset_to_exprs machines m i

508

else

509

[] (* Nothing to add yet *)

510

in

511


512

let mems = full_memory_vars machines target_machine in

513

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

514

let mid_mems = rename_mems rename_mid_list in

515

let next_mems = rename_mems rename_next_list in

516


517

let call_expr =

518

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

519

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

520

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

521

Z3.Boolean.mk_eq !ctx

522

( (* output var *)

523

horn_val_to_expr

524

~is_lhs:true

525

m self

526

(mk_val (Var o) o.var_type)

527

)

528

(

529

Z3.Boolean.mk_ite !ctx

530

(horn_var_to_expr mem_m)

531

(horn_val_to_expr m self i1)

532

(horn_val_to_expr m self i2)

533

)

534

in

535

let stmt2 = (* mem_X = false *)

536

Z3.Boolean.mk_eq !ctx

537

(horn_var_to_expr mem_x)

538

(Z3.Boolean.mk_false !ctx)

539

in

540

[stmt1; stmt2]

541

end

542


543

 node_name_n >

544

let expr =

545

Z3.Expr.mk_app

546

!ctx

547

(get_fdecl (machine_step_name (node_name n)))

548

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

549

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

550


551

)

552

in

553

[expr]

554

in

555


556

reset_exprs@call_expr

557

end

558

with Not_found > ( (* stateless node instance *)

559

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

560

let expr =

561

Z3.Expr.mk_app

562

!ctx

563

(get_fdecl (machine_stateless_name (node_name n)))

564

idx_uid_inout (* Arguments are inputs, outputs *)

565

in

566

[expr]

567

)

568


569


570


571

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

572

(* let rec value_suffix_to_expr self value = *)

573

(* match value.value_desc with *)

574

(*  Fun (n, vl) > *)

575

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

576


577

(*  _ > *)

578

(* horn_val_to_expr self value *)

579


580


581

(* type_directed assignment: array vs. statically sized type

582

 [var_type]: type of variable to be assigned

583

 [var_name]: name of variable to be assigned

584

 [value]: assigned value

585

 [pp_var]: printer for variables

586

*)

587

let assign_to_exprs m var_name value =

588

let self = m.mname.node_id in

589

let e =

590

Z3.Boolean.mk_eq

591

!ctx

592

(horn_val_to_expr ~is_lhs:true m self var_name)

593

(horn_val_to_expr m self value)

594

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

595

in

596

[e]

597


598


599

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

600

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

601

match Corelang.get_instr_desc instr with

602

 MComment _ > [], reset_instances

603

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

604

no_reset_to_exprs machines m i,

605

i::reset_instances

606

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

607

instance_reset_to_exprs machines m i,

608

i::reset_instances

609

 MLocalAssign (i,v) >

610

assign_to_exprs

611

m

612

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

613

reset_instances

614

 MStateAssign (i,v) >

615

assign_to_exprs

616

m

617

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

618

reset_instances

619

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

620

assert false (* This should not happen anymore *)

621

 MStep (il, i, vl) >

622

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

623

mem_c and print the call to mem_m *)

624

instance_call_to_exprs machines reset_instances m i vl il,

625

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

626

don't have to update reset_instances *)

627


628

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

629

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

630

compare the reset_instances of each branch and

631

introduced the mem_m = mem_c for branches to do not

632

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

633

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

634

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

635

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

636

statement. *)

637

let self = m.mname.node_id in

638

let branch_to_expr (tag, instrs) =

639

let branch_def, branch_resets = instrs_to_expr machines reset_instances m instrs in

640

let e =

641

Z3.Boolean.mk_implies !ctx

642

(Z3.Boolean.mk_eq !ctx

643

(horn_val_to_expr m self g)

644

(horn_tag_to_expr tag))

645

branch_def in

646


647

[e], branch_resets

648


649

in

650

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

651

let b_instrs, b_resets = branch_to_expr b in

652

instrs@b_instrs, resets@b_resets

653

) ([], reset_instances) hl

654


655

and instrs_to_expr machines reset_instances m instrs =

656

let instr_to_exprs rs i = instr_to_exprs machines rs m i in

657

let e_list, rs =

658

match instrs with

659

 [x] > instr_to_exprs reset_instances x

660

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

661


662

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

663

let exprs_i, rs_i = instr_to_exprs rs i in

664

exprs@exprs_i, rs@rs_i

665

)

666

([], reset_instances) instrs

667


668


669

 [] > [], reset_instances

670

in

671

let e =

672

match e_list with

673

 [e] > e

674

 [] > Z3.Boolean.mk_true !ctx

675

 _ > Z3.Boolean.mk_and !ctx e_list

676

in

677

e, rs

678


679


680

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

681


682

(* Quantifiying universally all occuring variables *)

683

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

684

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

685

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

686

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

687

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

688


689

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

690

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

691

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

692


693

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

694

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

695

let compare = compare

696

let hash = Hashtbl.hash

697

end)

698

in

699

let rec get_expr_vars e =

700

let open Utils in

701

let nb_args = Z3.Expr.get_num_args e in

702

if nb_args <= 0 then (

703

let fdecl = Z3.Expr.get_func_decl e in

704

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

705

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

706

let dkind = Z3.FuncDecl.get_decl_kind fdecl in

707

match dkind with Z3enums.OP_UNINTERPRETED > (

708

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

709

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

710

(* List.iter (fun p > *)

711

(* match p with *)

712

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

713

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

714

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

715

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

716

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

717

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

718

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

719


720

(* ) params; *)

721

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

722

FDSet.singleton fdecl

723

)

724

 _ > FDSet.empty

725

)

726

else (*if nb_args > 0 then*)

727

List.fold_left

728

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

729

FDSet.empty (Z3.Expr.get_args e)

730

in

731

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

732

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

733

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

734


735

if !debug then (

736

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

737

(Z3.Expr.to_string expr)

738

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

739

)

740

;

741

let expr = Z3.Quantifier.mk_forall_const

742

!ctx (* context *)

743

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

744

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

745

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

746

expr (* expression *)

747

None (* quantifier weight, None means 1 *)

748

[] (* pattern list ? *)

749

[] (* ? *)

750

None (* ? *)

751

None (* ? *)

752

in

753

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

754


755

(*

756

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

757

*)

758

Z3.Fixedpoint.add_rule !fp

759

(Z3.Quantifier.expr_of_quantifier expr)

760

None

761


762


763

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

764


765

let machine_reset machines m =

766

let locals = local_memory_vars machines m in

767


768

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

769

let mid_mem_def =

770

List.map (fun v >

771

Z3.Boolean.mk_eq !ctx

772

(horn_var_to_expr (rename_mid v))

773

(horn_var_to_expr (rename_current v))

774

) locals

775

in

776


777

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

778

Special treatment for _arrow: _first = true

779

*)

780


781

let reset_instances =

782


783

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

784

let name = node_name n in

785

if name = "_arrow" then (

786

Z3.Boolean.mk_eq !ctx

787

(

788

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

789

Z3.Expr.mk_const_f !ctx vdecl

790

)

791

(Z3.Boolean.mk_true !ctx)

792


793

) else (

794

let machine_n = get_machine machines name in

795


796

Z3.Expr.mk_app

797

!ctx

798

(get_fdecl (name ^ "_reset"))

799

(List.map (horn_var_to_expr)

800

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

801

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

802

))

803


804

)

805

) m.minstances

806


807


808

in

809


810

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

811


812


813


814

(* TODO: empty list means true statement *)

815

let decl_machine machines m =

816

if m.mname.node_id = Arrow.arrow_id then

817

(* We don't do arrow function *)

818

()

819

else

820

begin

821

let _ =

822

List.map decl_var

823

(

824

(inout_vars machines m)@

825

(rename_current_list (full_memory_vars machines m)) @

826

(rename_mid_list (full_memory_vars machines m)) @

827

(rename_next_list (full_memory_vars machines m)) @

828

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

829

)

830

in

831

if is_stateless m then

832

begin

833

if !debug then

834

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

835


836

(* Declaring single predicate *)

837

let vars = inout_vars machines m in

838

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

839

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

840


841

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

842

instrs_to_expr

843

machines

844

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

845

m

846

m.mstep.step_instrs

847

in

848

let horn_head =

849

Z3.Expr.mk_app

850

!ctx

851

(get_fdecl (machine_stateless_name m.mname.node_id))

852

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

853

in

854

(* this line seems useless *)

855

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

856

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

857

match m.mstep.step_asserts with

858

 [] >

859

begin

860

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

861

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

862

(* TODO clean code *)

863

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

864

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

865


866

end

867

 assertsl >

868

begin

869

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

870

let body_with_asserts =

871

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

872

in

873

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

874

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

875

end

876

end

877

else

878

begin

879


880

(* Rule for reset *)

881


882

let vars = reset_vars machines m in

883

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

884

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

885

let horn_reset_body = machine_reset machines m in

886

let horn_reset_head =

887

Z3.Expr.mk_app

888

!ctx

889

(get_fdecl (machine_reset_name m.mname.node_id))

890

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

891

in

892


893


894

let _ =

895

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

896


897

in

898


899

(* Rule for step*)

900

let vars = step_vars machines m in

901

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

902

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

903

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

904

instrs_to_expr

905

machines

906

[]

907

m

908

m.mstep.step_instrs

909

in

910

let horn_step_head =

911

Z3.Expr.mk_app

912

!ctx

913

(get_fdecl (machine_step_name m.mname.node_id))

914

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

915

in

916

match m.mstep.step_asserts with

917

 [] >

918

begin

919

(* Rule for single predicate *)

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 horn_step_body horn_step_head)

922


923

end

924

 assertsl >

925

begin

926

(* Rule for step Assertions @.; *)

927

let body_with_asserts =

928

Z3.Boolean.mk_and !ctx

929

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

930

in

931

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

932

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

933


934

end

935


936

end

937

end

938


939


940


941

(* Debug functions *)

942


943

let rec extract_expr_fds e =

944

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

945

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

946


947

(* Removing quantifier is there are some *)

948

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

949

bad *)

950

try

951

let eq = Z3.Quantifier.quantifier_of_expr e in

952

let e2 = Z3.Quantifier.get_body eq in

953

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

954

e2

955


956

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

957

in

958

let _ =

959

try

960

(

961

let fd = Z3.Expr.get_func_decl e in

962

let fd_symbol = Z3.FuncDecl.get_name fd in

963

let fd_name = Z3.Symbol.to_string fd_symbol in

964

if not (Hashtbl.mem decls fd_name) then

965

register_fdecl fd_name fd;

966

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

967

(* fd_name *)

968

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

969

try

970

(

971

let args = Z3.Expr.get_args e in

972

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

973

(* List.iter extract_expr_fds args; *)

974

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

975

()

976

)

977

with _ >

978

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

979

(Z3.Expr.to_string e)

980

)

981

with _ >

982

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

983

(Z3.Expr.to_string e)

984

in

985

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

986

()

987


988

(* Local Variables: *)

989

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

990

(* End: *)
