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

(** Sorts

41


42

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

43


44

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

45

provided with a enumerated type name.

46


47

*)

48


49

let bool_sort = Z3.Boolean.mk_sort !ctx

50

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

51

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

52


53


54

let get_const_sort = Hashtbl.find const_sorts

55

let get_sort_elems = Hashtbl.find sort_elems

56

let get_tag_sort = Hashtbl.find const_tags

57


58


59


60

let decl_sorts () =

61

Hashtbl.iter (fun typ decl >

62

match typ with

63

 Tydec_const var >

64

(match decl.top_decl_desc with

65

 TypeDef tdef > (

66

match tdef.tydef_desc with

67

 Tydec_enum tl >

68

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

69

Hashtbl.add const_sorts var new_sort;

70

Hashtbl.add sort_elems new_sort tl;

71

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

72


73

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

74

)

75

 _ > assert false

76

)

77

 _ > ()) Corelang.type_table

78


79


80

let rec type_to_sort t =

81

if Types.is_bool_type t then bool_sort else

82

if Types.is_int_type t then int_sort else

83

if Types.is_real_type t then real_sort else

84

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

85

 Types.Tconst ty > get_const_sort ty

86

 Types.Tclock t > type_to_sort t

87

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

88

 Types.Tstatic(d, ty)> type_to_sort ty

89

 Types.Tarrow _

90

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

91

Types.print_ty t; assert false

92


93

(** Func decls

94


95

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

96

proposed encoding introduces a 0ary fun_decl to model variables

97

and fun_decl with arguments to declare reset and step predicates.

98


99


100


101

*)

102

let register_fdecl id fd = Hashtbl.add decls id fd

103

let get_fdecl id =

104

try

105

Hashtbl.find decls id

106

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

107


108

let pp_fdecls fmt =

109

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

110

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

111


112


113

let decl_var id =

114

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

115

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

116

register_fdecl id.var_id fdecl;

117

fdecl

118


119

let decl_rel name args =

120

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

121

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

122

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

123

Z3.Fixedpoint.register_relation !fp fdecl;

124

register_fdecl name fdecl;

125

fdecl

126


127


128

(** Conversion functions

129


130

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

131

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

132


133

*)

134


135


136

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

137

let horn_var_to_expr v =

138

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

139


140


141


142


143

(* Used to print boolean constants *)

144

let horn_tag_to_expr t =

145

if t = Corelang.tag_true then

146

Z3.Boolean.mk_true !ctx

147

else if t = Corelang.tag_false then

148

Z3.Boolean.mk_false !ctx

149

else

150

(* Finding the associated sort *)

151

let sort = get_tag_sort t in

152

let elems = get_sort_elems sort in

153

let res : Z3.Expr.expr option =

154

List.fold_left2 (fun res cst expr >

155

match res with

156

 Some _ > res

157

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

158

) None elems (Z3.Enumeration.get_consts sort)

159

in

160

match res with None > assert false  Some s > s

161


162

(* Prints a constant value *)

163

let rec horn_const_to_expr c =

164

match c with

165

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

166

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

167

 Const_tag t > horn_tag_to_expr t

168

 _ > assert false

169


170


171


172

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

173

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

174

for the type integer (arrays).

175

*)

176

let rec horn_default_val t =

177

let t = Types.dynamic_type t in

178

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

179

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

180

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

181

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

182

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

183

* let valt = Types.array_element_type t in

184

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

185

* pp_type valt

186

* pp_default_val valt

187

*  Types.Tstruct(l) > assert false

188

*  Types.Ttuple(l) > assert false

189

* _ > *) assert false

190


191

(* Conversion of basic library functions *)

192


193

let horn_basic_app i val_to_expr vl =

194

match i, vl with

195

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

196

Z3.Boolean.mk_ite

197

!ctx

198

(val_to_expr v1)

199

(val_to_expr v2)

200

(val_to_expr v3)

201


202

 "uminus", [v] >

203

Z3.Arithmetic.mk_unary_minus

204

!ctx

205

(val_to_expr v)

206

 "not", [v] >

207

Z3.Boolean.mk_not

208

!ctx

209

(val_to_expr v)

210

 "=", [v1; v2] >

211

Z3.Boolean.mk_eq

212

!ctx

213

(val_to_expr v1)

214

(val_to_expr v2)

215

 "&&", [v1; v2] >

216

Z3.Boolean.mk_and

217

!ctx

218

[val_to_expr v1;

219

val_to_expr v2]

220

 "", [v1; v2] >

221

Z3.Boolean.mk_or

222

!ctx

223

[val_to_expr v1;

224

val_to_expr v2]

225


226

 "impl", [v1; v2] >

227

Z3.Boolean.mk_implies

228

!ctx

229

(val_to_expr v1)

230

(val_to_expr v2)

231

 "mod", [v1; v2] >

232

Z3.Arithmetic.Integer.mk_mod

233

!ctx

234

(val_to_expr v1)

235

(val_to_expr v2)

236

 "equi", [v1; v2] >

237

Z3.Boolean.mk_eq

238

!ctx

239

(val_to_expr v1)

240

(val_to_expr v2)

241

 "xor", [v1; v2] >

242

Z3.Boolean.mk_xor

243

!ctx

244

(val_to_expr v1)

245

(val_to_expr v2)

246

 "!=", [v1; v2] >

247

Z3.Boolean.mk_not

248

!ctx

249

(

250

Z3.Boolean.mk_eq

251

!ctx

252

(val_to_expr v1)

253

(val_to_expr v2)

254

)

255

 "/", [v1; v2] >

256

Z3.Arithmetic.mk_div

257

!ctx

258

(val_to_expr v1)

259

(val_to_expr v2)

260


261

 "+", [v1; v2] >

262

Z3.Arithmetic.mk_add

263

!ctx

264

[val_to_expr v1; val_to_expr v2]

265


266

 "", [v1; v2] >

267

Z3.Arithmetic.mk_sub

268

!ctx

269

[val_to_expr v1 ; val_to_expr v2]

270


271

 "*", [v1; v2] >

272

Z3.Arithmetic.mk_mul

273

!ctx

274

[val_to_expr v1; val_to_expr v2]

275


276


277

 "<", [v1; v2] >

278

Z3.Arithmetic.mk_lt

279

!ctx

280

(val_to_expr v1)

281

(val_to_expr v2)

282


283

 "<=", [v1; v2] >

284

Z3.Arithmetic.mk_le

285

!ctx

286

(val_to_expr v1)

287

(val_to_expr v2)

288


289

 ">", [v1; v2] >

290

Z3.Arithmetic.mk_gt

291

!ctx

292

(val_to_expr v1)

293

(val_to_expr v2)

294


295

 ">=", [v1; v2] >

296

Z3.Arithmetic.mk_ge

297

!ctx

298

(val_to_expr v1)

299

(val_to_expr v2)

300


301


302

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

303

* !ctx

304

* (val_to_expr v1)

305

* (val_to_expr v2)

306

*

307

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

308

 _ > (

309

Format.eprintf

310

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

311

assert false)

312


313


314

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

315

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

316

but an offset suffix may be added for array variables

317

*)

318

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

319

match v.value_desc with

320

 Cst c > horn_const_to_expr c

321


322

(* Code specific for arrays *)

323

 Array il >

324

(* An array definition:

325

(store (

326

...

327

(store (

328

store (

329

default_val

330

)

331

idx_n val_n

332

)

333

idx_n1 val_n1)

334

...

335

idx_1 val_1

336

) *)

337

let rec build_array (tab, x) =

338

match tab with

339

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

340

 h::t >

341

Z3.Z3Array.mk_store

342

!ctx

343

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

344

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

345

(horn_val_to_expr ~is_lhs:is_lhs self h)

346

in

347

build_array (il, 0)

348


349

 Access(tab,index) >

350

Z3.Z3Array.mk_select !ctx

351

(horn_val_to_expr ~is_lhs:is_lhs self tab)

352

(horn_val_to_expr ~is_lhs:is_lhs self index)

353


354

(* Code specific for arrays *)

355


356

 Power (v, n) > assert false

357

 LocalVar v >

358

horn_var_to_expr

359

(rename_machine

360

self

361

v)

362

 StateVar v >

363

if Types.is_array_type v.var_type

364

then assert false

365

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

366

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

367


368

let no_reset_to_exprs machines m i =

369

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

370

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

371


372

let m_list =

373

rename_machine_list

374

(concat m.mname.node_id i)

375

(rename_mid_list (full_memory_vars machines target_machine))

376

in

377

let c_list =

378

rename_machine_list

379

(concat m.mname.node_id i)

380

(rename_current_list (full_memory_vars machines target_machine))

381

in

382

match c_list, m_list with

383

 [chd], [mhd] >

384

let expr =

385

Z3.Boolean.mk_eq !ctx

386

(horn_var_to_expr mhd)

387

(horn_var_to_expr chd)

388

in

389

[expr]

390

 _ > (

391

let exprs =

392

List.map2 (fun mhd chd >

393

Z3.Boolean.mk_eq !ctx

394

(horn_var_to_expr mhd)

395

(horn_var_to_expr chd)

396

)

397

m_list

398

c_list

399

in

400

exprs

401

)

402


403

let instance_reset_to_exprs machines m i =

404

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

405

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

406

let vars =

407

(

408

(rename_machine_list

409

(concat m.mname.node_id i)

410

(rename_current_list (full_memory_vars machines target_machine))

411

)

412

@

413

(rename_machine_list

414

(concat m.mname.node_id i)

415

(rename_mid_list (full_memory_vars machines target_machine))

416

)

417

)

418

in

419

let expr =

420

Z3.Expr.mk_app

421

!ctx

422

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

423

(List.map (horn_var_to_expr) vars)

424

in

425

[expr]

426


427

let instance_call_to_exprs machines reset_instances m i inputs outputs =

428

let self = m.mname.node_id in

429

try (* stateful node instance *)

430

begin

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

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

435

let reset_exprs =

436

if not (List.mem i reset_instances) then

437

(* If not, declare mem_m = mem_c *)

438

no_reset_to_exprs machines m i

439

else

440

[] (* Nothing to add yet *)

441

in

442


443

let mems = full_memory_vars machines target_machine in

444

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

445

let mid_mems = rename_mems rename_mid_list in

446

let next_mems = rename_mems rename_next_list in

447


448

let call_expr =

449

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

450

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

451

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

452

Z3.Boolean.mk_eq !ctx

453

( (* output var *)

454

horn_val_to_expr

455

~is_lhs:true

456

self

457

(mk_val (LocalVar o) o.var_type)

458

)

459

(

460

Z3.Boolean.mk_ite !ctx

461

(horn_var_to_expr mem_m)

462

(horn_val_to_expr self i1)

463

(horn_val_to_expr self i2)

464

)

465

in

466

let stmt2 = (* mem_X = false *)

467

Z3.Boolean.mk_eq !ctx

468

(horn_var_to_expr mem_x)

469

(Z3.Boolean.mk_false !ctx)

470

in

471

[stmt1; stmt2]

472

end

473


474

 node_name_n >

475

let expr =

476

Z3.Expr.mk_app

477

!ctx

478

(get_fdecl (machine_step_name (node_name n)))

479

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

480

(

481

List.map (horn_val_to_expr self) (

482

inputs @

483

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

484

)

485

) @ (

486

List.map (horn_var_to_expr) (mid_mems@next_mems)

487

)

488

)

489

in

490

[expr]

491

in

492


493

reset_exprs@call_expr

494

end

495

with Not_found > ( (* stateless node instance *)

496

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

497

let expr =

498

Z3.Expr.mk_app

499

!ctx

500

(get_fdecl (machine_stateless_name (node_name n)))

501

((* Arguments are inputs, outputs *)

502

List.map (horn_val_to_expr self)

503

(

504

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

505

)

506

)

507

in

508

[expr]

509

)

510


511


512


513

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

514

(* let rec value_suffix_to_expr self value = *)

515

(* match value.value_desc with *)

516

(*  Fun (n, vl) > *)

517

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

518


519

(*  _ > *)

520

(* horn_val_to_expr self value *)

521


522


523

(* type_directed assignment: array vs. statically sized type

524

 [var_type]: type of variable to be assigned

525

 [var_name]: name of variable to be assigned

526

 [value]: assigned value

527

 [pp_var]: printer for variables

528

*)

529

let assign_to_exprs m var_name value =

530

let self = m.mname.node_id in

531

let e =

532

Z3.Boolean.mk_eq

533

!ctx

534

(horn_val_to_expr ~is_lhs:true self var_name)

535

(horn_val_to_expr self value)

536

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

537

in

538

[e]

539


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 : Z3.Expr.expr list * ident list =

543

match Corelang.get_instr_desc instr with

544

 MComment _ > [], reset_instances

545

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

546

no_reset_to_exprs machines m i,

547

i::reset_instances

548

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

549

instance_reset_to_exprs machines m i,

550

i::reset_instances

551

 MLocalAssign (i,v) >

552

assign_to_exprs

553

m

554

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

555

reset_instances

556

 MStateAssign (i,v) >

557

assign_to_exprs

558

m

559

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

560

reset_instances

561

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

562

assert false (* This should not happen anymore *)

563

 MStep (il, i, vl) >

564

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

565

mem_c and print the call to mem_m *)

566

instance_call_to_exprs machines reset_instances m i vl il,

567

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

568

don't have to update reset_instances *)

569


570

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

571

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

572

compare the reset_instances of each branch and

573

introduced the mem_m = mem_c for branches to do not

574

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

575

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

576

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

577

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

578

statement. *)

579

let self = m.mname.node_id in

580

let branch_to_expr (tag, instrs) =

581

let branch_def, branch_resets = instrs_to_expr machines reset_instances m instrs in

582

let e =

583

Z3.Boolean.mk_implies !ctx

584

(Z3.Boolean.mk_eq !ctx

585

(horn_val_to_expr self g)

586

(horn_tag_to_expr tag))

587

branch_def in

588


589

[e], branch_resets

590


591

in

592

List.fold_left (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


597

and instrs_to_expr machines reset_instances m instrs =

598

let instr_to_exprs rs i = instr_to_exprs machines rs m i in

599

let e_list, rs =

600

match instrs with

601

 [x] > instr_to_exprs reset_instances x

602

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

603


604

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

605

let exprs_i, rs_i = instr_to_exprs rs i in

606

exprs@exprs_i, rs@rs_i

607

)

608

([], reset_instances) instrs

609


610


611

 [] > [], reset_instances

612

in

613

let e =

614

match e_list with

615

 [e] > e

616

 [] > Z3.Boolean.mk_true !ctx

617

 _ > Z3.Boolean.mk_and !ctx e_list

618

in

619

e, rs

620


621


622

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

623


624

(* Quantifiying universally all occuring variables *)

625

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

626

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

627

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

628

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

629

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

630


631

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

632

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

633

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

634


635

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

636

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

637

let compare = compare

638

let hash = Hashtbl.hash

639

end)

640

in

641

let rec get_expr_vars e =

642

let open Utils in

643

let nb_args = Z3.Expr.get_num_args e in

644

if nb_args <= 0 then (

645

let fdecl = Z3.Expr.get_func_decl e in

646

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

647

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

648

let dkind = Z3.FuncDecl.get_decl_kind fdecl in

649

match dkind with Z3enums.OP_UNINTERPRETED > (

650

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

651

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

652

(* List.iter (fun p > *)

653

(* match p with *)

654

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

655

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

656

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

657

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

658

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

659

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

660

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

661


662

(* ) params; *)

663

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

664

FDSet.singleton fdecl

665

)

666

 _ > FDSet.empty

667

)

668

else (*if nb_args > 0 then*)

669

List.fold_left

670

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

671

FDSet.empty (Z3.Expr.get_args e)

672

in

673

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

674

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

675

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

676


677

Format.eprintf "Declaring rule: %s with variables %a@."

678

(Z3.Expr.to_string expr)

679

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

680

;

681

let expr = Z3.Quantifier.mk_forall_const

682

!ctx (* context *)

683

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

684

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

685

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

686

expr (* expression *)

687

None (* quantifier weight, None means 1 *)

688

[] (* pattern list ? *)

689

[] (* ? *)

690

None (* ? *)

691

None (* ? *)

692

in

693

Format.eprintf "OK@.@?";

694


695


696

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

697


698

Z3.Fixedpoint.add_rule !fp

699

(Z3.Quantifier.expr_of_quantifier expr)

700

None

701


702

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

703


704

let machine_reset machines m =

705

let locals = local_memory_vars machines m in

706


707

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

708

let mid_mem_def =

709

List.map (fun v >

710

Z3.Boolean.mk_eq !ctx

711

(horn_var_to_expr (rename_mid v))

712

(horn_var_to_expr (rename_current v))

713

) locals

714

in

715


716

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

717

Special treatment for _arrow: _first = true

718

*)

719


720

let reset_instances =

721


722

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

723

let name = node_name n in

724

if name = "_arrow" then (

725

Z3.Boolean.mk_eq !ctx

726

(

727

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

728

Z3.Expr.mk_const_f !ctx vdecl

729

)

730

(Z3.Boolean.mk_true !ctx)

731


732

) else (

733

let machine_n = get_machine machines name in

734


735

Z3.Expr.mk_app

736

!ctx

737

(get_fdecl (name ^ "_reset"))

738

(List.map (horn_var_to_expr)

739

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

740

)

741


742

)

743

) m.minstances

744


745


746

in

747


748

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

749


750


751


752

(* TODO: empty list means true statement *)

753

let decl_machine machines m =

754

if m.mname.node_id = Arrow.arrow_id then

755

(* We don't do arrow function *)

756

()

757

else

758

begin

759

let _ =

760

List.map decl_var

761

(

762

(inout_vars machines m)@

763

(rename_current_list (full_memory_vars machines m)) @

764

(rename_mid_list (full_memory_vars machines m)) @

765

(rename_next_list (full_memory_vars machines m)) @

766

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

767

)

768

in

769


770

if is_stateless m then

771

begin

772

(* Declaring single predicate *)

773

let vars = inout_vars machines m in

774

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

775

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

776

instrs_to_expr

777

machines

778

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

779

m

780

m.mstep.step_instrs

781

in

782

let horn_head =

783

Z3.Expr.mk_app

784

!ctx

785

(get_fdecl (machine_stateless_name m.mname.node_id))

786

(List.map (horn_var_to_expr) vars)

787

in

788

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

789

match m.mstep.step_asserts with

790

 [] >

791

begin

792

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

793

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

794

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

795


796

end

797

 assertsl >

798

begin

799

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

800

let body_with_asserts =

801

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

802

in

803

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

804

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

805

end

806

end

807

else

808

begin

809


810

(* Rule for reset *)

811


812

let vars = reset_vars machines m in

813

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

814

let horn_reset_body = machine_reset machines m in

815

let horn_reset_head =

816

Z3.Expr.mk_app

817

!ctx

818

(get_fdecl (machine_reset_name m.mname.node_id))

819

(List.map (horn_var_to_expr) vars)

820

in

821


822


823

let _ =

824

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

825


826

in

827


828

(* Rule for step*)

829

let vars = step_vars machines m in

830

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

831

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

832

instrs_to_expr

833

machines

834

[]

835

m

836

m.mstep.step_instrs

837

in

838

let horn_step_head =

839

Z3.Expr.mk_app

840

!ctx

841

(get_fdecl (machine_step_name m.mname.node_id))

842

(List.map (horn_var_to_expr) vars)

843

in

844

match m.mstep.step_asserts with

845

 [] >

846

begin

847

(* Rule for single predicate *)

848

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

849

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

850


851

end

852

 assertsl >

853

begin

854

(* Rule for step Assertions @.; *)

855

let body_with_asserts =

856

Z3.Boolean.mk_and !ctx

857

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

858

in

859

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

860

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

861


862

end

863


864

end

865

end

866


867


868


869

(* Debug functions *)

870


871

let rec extract_expr_fds e =

872

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

873

(Z3.Expr.to_string e);

874


875

(* Removing quantifier is there are some *)

876

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

877

bad *)

878

try

879

let eq = Z3.Quantifier.quantifier_of_expr e in

880

let e2 = Z3.Quantifier.get_body eq in

881

Format.eprintf "Extracted quantifier body@ ";

882

e2

883


884

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

885

in

886

let _ =

887

try

888

(

889

let fd = Z3.Expr.get_func_decl e in

890

let fd_symbol = Z3.FuncDecl.get_name fd in

891

let fd_name = Z3.Symbol.to_string fd_symbol in

892

if not (Hashtbl.mem decls fd_name) then

893

register_fdecl fd_name fd;

894

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

895

fd_name

896

(Z3.FuncDecl.to_string fd);

897

try

898

(

899

let args = Z3.Expr.get_args e in

900

Format.eprintf "@[<v>@ ";

901

List.iter extract_expr_fds args;

902

Format.eprintf "@]@ ";

903

)

904

with _ >

905

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

906

(Z3.Expr.to_string e)

907

)

908

with _ >

909

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

910

(Z3.Expr.to_string e)

911

in

912

Format.eprintf "@]@ "

913


914


915

(* Local Variables: *)

916

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

917

(* End: *)
