1

open Lustre_types

2

open Utils

3

open Seal_utils

4

open Zustre_data (* Access to Z3 context *)

5


6


7

(* Switched system extraction: expression are memoized *)

8

(*let expr_mem = Hashtbl.create 13*)

9


10

let add_init defs vid =

11

Hashtbl.add defs vid [[], IsInit]

12


13


14

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

15

(* Convert from Lustre expressions to Z3 expressions and back *)

16

(* All (free) variables have to be declared in the Z3 context *)

17

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

18


19

let is_init_name = "__is_init"

20


21

let const_defs = Hashtbl.create 13

22

let is_const id = Hashtbl.mem const_defs id

23

let is_enum_const id = Hashtbl.mem Zustre_data.const_tags id

24

let get_const id = Hashtbl.find const_defs id

25


26

(* expressions are only basic constructs here, no more ite, tuples,

27

arrows, fby, ... *)

28


29

(* Set of hash to support memoization *)

30

let expr_hash: (expr * Utils.tag) list ref = ref []

31

let ze_hash: (Z3.Expr.expr, Utils.tag) Hashtbl.t = Hashtbl.create 13

32

let e_hash: (Utils.tag, Z3.Expr.expr) Hashtbl.t = Hashtbl.create 13

33

let pp_hash pp_key pp_v fmt h = Hashtbl.iter (fun key v > Format.fprintf fmt "%a > %a@ " pp_key key pp_v v) h

34

let pp_e_map fmt = List.iter (fun (e,t) > Format.fprintf fmt "%i > %a@ " t Printers.pp_expr e) !expr_hash

35

let pp_ze_hash fmt = pp_hash

36

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

37

Format.pp_print_int

38

fmt

39

ze_hash

40

let pp_e_hash fmt = pp_hash

41

Format.pp_print_int

42

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

43

fmt

44

e_hash

45

let mem_expr e =

46

(* Format.eprintf "Searching for %a in map: @[<v 0>%t@]"

47

* Printers.pp_expr e

48

* pp_e_map; *)

49

let res = List.exists (fun (e',_) > Corelang.is_eq_expr e e') !expr_hash in

50

(* Format.eprintf "found?%b@." res; *)

51

res

52


53

let mem_zexpr ze =

54

Hashtbl.mem ze_hash ze

55

let get_zexpr e =

56

let eref, uid = List.find (fun (e',_) > Corelang.is_eq_expr e e') !expr_hash in

57

(* Format.eprintf "found expr=%a id=%i@." Printers.pp_expr eref eref.expr_tag; *)

58

Hashtbl.find e_hash uid

59

let get_expr ze =

60

let uid = Hashtbl.find ze_hash ze in

61

let e,_ = List.find (fun (e,t) > t = uid) !expr_hash in

62

e

63


64

let neg_ze z3e = Z3.Boolean.mk_not !ctx z3e

65

let is_init_z3e =

66

Z3.Expr.mk_const_s !ctx is_init_name Zustre_common.bool_sort

67


68

let get_zid (ze:Z3.Expr.expr) : Utils.tag =

69

try

70

if Z3.Expr.equal ze is_init_z3e then 1 else

71

if Z3.Expr.equal ze (neg_ze is_init_z3e) then 2 else

72

Hashtbl.find ze_hash ze

73

with _ > (Format.eprintf "Looking for ze %s in Hash %a"

74

(Z3.Expr.to_string ze)

75

(fun fmt hash > Hashtbl.iter (fun ze uid > Format.fprintf fmt "%s > %i@ " (Z3.Expr.to_string ze) uid) hash ) ze_hash;

76

assert false)

77

let add_expr =

78

let cpt = ref 0 in

79

fun e ze >

80

incr cpt;

81

let uid = !cpt in

82

expr_hash := (e, uid)::!expr_hash;

83

Hashtbl.add e_hash uid ze;

84

Hashtbl.add ze_hash ze uid

85


86


87

let expr_to_z3_expr, zexpr_to_expr =

88

(* List to store converted expression. *)

89

(* let hash = ref [] in

90

* let comp_expr e (e', _) = Corelang.is_eq_expr e e' in

91

* let comp_zexpr ze (_, ze') = Z3.Expr.equal ze ze' in *)

92


93

let rec e2ze e =

94

if mem_expr e then (

95

get_zexpr e

96

)

97

else (

98

let res =

99

match e.expr_desc with

100

 Expr_const c >

101

let z3e = Zustre_common.horn_const_to_expr c in

102

add_expr e z3e;

103

z3e

104

 Expr_ident id > (

105

if is_const id then (

106

let c = get_const id in

107

let z3e = Zustre_common.horn_const_to_expr c in

108

add_expr e z3e;

109

z3e

110

)

111

else if is_enum_const id then (

112

let z3e = Zustre_common.horn_tag_to_expr id in

113

add_expr e z3e;

114

z3e

115

)

116

else (

117

let fdecl_id = Zustre_common.get_fdecl id in

118

let z3e = Z3.Expr.mk_const_f !ctx fdecl_id in

119

add_expr e z3e;

120

z3e

121

)

122

)

123

 Expr_appl (id,args, None) (* no reset *) >

124

let z3e = Zustre_common.horn_basic_app id e2ze (Corelang.expr_list_of_expr args) in

125

add_expr e z3e;

126

z3e

127

 Expr_tuple [e] >

128

let z3e = e2ze e in

129

add_expr e z3e;

130

z3e

131

 _ > ( match e.expr_desc with Expr_tuple _ > Format.eprintf "tuple e2ze(%a)@.@?" Printers.pp_expr e

132

 _ > Format.eprintf "e2ze(%a)@.@?" Printers.pp_expr e)

133

; assert false

134

in

135

res

136

)

137

in

138

let rec ze2e ze =

139

let ze_name ze =

140

let fd = Z3.Expr.get_func_decl ze in

141

Z3.Symbol.to_string (Z3.FuncDecl.get_name fd)

142

in

143

if mem_zexpr ze then

144

None, Some (get_expr ze)

145

else

146

let open Corelang in

147

let fd = Z3.Expr.get_func_decl ze in

148

let zel = Z3.Expr.get_args ze in

149

match Z3.Symbol.to_string (Z3.FuncDecl.get_name fd), zel with

150

(*  var, [] > (* should be in env *) get_e *)

151


152

(* Extracting IsInit status *)

153

 "not", [ze] when ze_name ze = is_init_name >

154

Some false, None

155

 name, [] when name = is_init_name > Some true, None

156

(* Other constructs are converted to a lustre expression *)

157

 op, _ > (

158


159


160

if Z3.Expr.is_numeral ze then

161

let e =

162

if Z3.Arithmetic.is_real ze then

163

let num = Num.num_of_ratio (Z3.Arithmetic.Real.get_ratio ze) in

164

let s = Z3.Arithmetic.Real.numeral_to_string ze in

165

mkexpr

166

Location.dummy_loc

167

(Expr_const

168

(Const_real

169

(Real.create_num num s)))

170

else if Z3.Arithmetic.is_int ze then

171

mkexpr

172

Location.dummy_loc

173

(Expr_const

174

(Const_int

175

(Big_int.int_of_big_int (Z3.Arithmetic.Integer.get_big_int ze))))

176

else if Z3.Expr.is_const ze then

177

match Z3.Expr.to_string ze with

178

 "true" > mkexpr Location.dummy_loc

179

(Expr_const (Const_tag (tag_true)))

180

 "false" >

181

mkexpr Location.dummy_loc

182

(Expr_const (Const_tag (tag_false)))

183

 _ > assert false

184

else

185

(

186

Format.eprintf "Const err: %s %b@." (Z3.Expr.to_string ze) (Z3.Expr.is_const ze);

187

assert false (* a numeral but no int nor real *)

188

)

189

in

190

None, Some e

191

else

192

match op with

193

 "not"  "="  ""  "*"  "/"

194

 ">="  "<="  ">"  "<"

195

>

196

let args = List.map (fun ze > Utils.desome (snd (ze2e ze))) zel in

197

None, Some (mkpredef_call Location.dummy_loc op args)

198

 "+" > ( (* Special treatment of + for 2+ args *)

199

let args = List.map (fun ze > Utils.desome (snd (ze2e ze))) zel in

200

let e = match args with

201

[] > assert false

202

 [hd] > hd

203

 e1::e2::tl >

204

let first_binary_and = mkpredef_call Location.dummy_loc op [e1;e2] in

205

if tl = [] then first_binary_and else

206

List.fold_left (fun e e_new >

207

mkpredef_call Location.dummy_loc op [e;e_new]

208

) first_binary_and tl

209


210

in

211

None, Some e

212

)

213

 "and"  "or" > (

214

(* Special case since it can contain is_init pred *)

215

let args = List.map (fun ze > ze2e ze) zel in

216

let op = if op = "and" then "&&" else if op = "or" then "" else assert false in

217

match args with

218

 [] > assert false

219

 [hd] > hd

220

 hd::tl >

221

List.fold_left

222

(fun (is_init_opt1, expr_opt1) (is_init_opt2, expr_opt2) >

223

(match is_init_opt1, is_init_opt2 with

224

None, x  x, None > x

225

 Some _, Some _ > assert false),

226

(match expr_opt1, expr_opt2 with

227

 None, x  x, None > x

228

 Some e1, Some e2 >

229

Some (mkpredef_call Location.dummy_loc op [e1; e2])

230

))

231

hd tl

232

)

233

 op >

234

let args = List.map (fun ze > (snd (ze2e ze))) zel in

235

Format.eprintf "deal with op %s (nb args: %i). Expr is %s@." op (List.length args) (Z3.Expr.to_string ze); assert false

236

)

237

in

238

(fun e > e2ze e), (fun ze > ze2e ze)

239


240


241

let zexpr_to_guard_list ze =

242

let init_opt, expr_opt = zexpr_to_expr ze in

243

(match init_opt with

244

 None > []

245

Some b > [IsInit, b]

246

) @ (match expr_opt with

247

 None > []

248

 Some e > [Expr e, true]

249

)

250


251


252

let simplify_neg_guard l =

253

List.map (fun (g,posneg) >

254

match g with

255

 IsInit > g, posneg

256

 Expr g >

257

if posneg then

258

Expr (Corelang.push_negations g),

259

true

260

else

261

(* Pushing the negation in the expression *)

262

Expr(Corelang.push_negations ~neg:true g),

263

true

264

) l

265


266

(* TODO:

267

individuellement demander si g1 => g2. Si c'est le cas, on peut ne garder que g1 dans la liste

268

*)

269

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

270

(* Checking sat(isfiability) of an expression and simplifying it *)

271

(* All (free) variables have to be declared in the Z3 context *)

272

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

273

(*

274

let goal_simplify zl =

275

let goal = Z3.Goal.mk_goal !ctx false false false in

276

Z3.Goal.add goal zl;

277

let goal' = Z3.Goal.simplify goal None in

278

(* Format.eprintf "Goal before: %s@.Goal after : %s@.Sat? %s@."

279

* (Z3.Goal.to_string goal)

280

* (Z3.Goal.to_string goal')

281

* (Z3.Solver.string_of_status status_res)

282

* ; *)

283

let ze = Z3.Goal.as_expr goal' in

284

(* Format.eprintf "as an expr: %s@." (Z3.Expr.to_string ze); *)

285

zexpr_to_guard_list ze

286

*)

287


288

let implies =

289

let ze_implies_hash : ((Utils.tag * Utils.tag), bool) Hashtbl.t = Hashtbl.create 13 in

290

fun ze1 ze2 >

291

let ze1_uid = get_zid ze1 in

292

let ze2_uid = get_zid ze2 in

293

if Hashtbl.mem ze_implies_hash (ze1_uid, ze2_uid) then

294

Hashtbl.find ze_implies_hash (ze1_uid, ze2_uid)

295

else

296

begin

297

if !seal_debug then (

298

report ~level:6 (fun fmt > Format.fprintf fmt "Checking implication: %s => %s?@ "

299

(Z3.Expr.to_string ze1) (Z3.Expr.to_string ze2)

300

));

301

let solver = Z3.Solver.mk_simple_solver !ctx in

302

let tgt = Z3.Boolean.mk_not !ctx (Z3.Boolean.mk_implies !ctx ze1 ze2) in

303

let res =

304

try

305

let status_res = Z3.Solver.check solver [tgt] in

306

match status_res with

307

 Z3.Solver.UNSATISFIABLE > if !seal_debug then

308

report ~level:6 (fun fmt > Format.fprintf fmt "Valid!@ ");

309

true

310

 _ > if !seal_debug then report ~level:6 (fun fmt > Format.fprintf fmt "not proved valid@ ");

311

false

312

with Zustre_common.UnknownFunction(id, msg) > (

313

report ~level:1 msg;

314

false

315

)

316

in

317

Hashtbl.add ze_implies_hash (ze1_uid,ze2_uid) res ;

318

res

319

end

320


321

let rec simplify zl =

322

match zl with

323

 []  [_] > zl

324

 hd::tl > (

325

(* Forall e in tl, checking whether hd => e or e => hd, to keep hd

326

in the first case and e in the second one *)

327

let tl = simplify tl in

328

let keep_hd, tl =

329

List.fold_left (fun (keep_hd, accu) e >

330

if implies hd e then

331

true, accu (* throwing away e *)

332

else if implies e hd then

333

false, e::accu (* throwing away hd *)

334

else

335

keep_hd, e::accu (* keeping both *)

336

) (true,[]) tl

337

in

338

(* Format.eprintf "keep_hd?%b hd=%s, tl=[%a]@."

339

* keep_hd

340

* (Z3.Expr.to_string hd)

341

* (Utils.fprintf_list ~sep:"; " (fun fmt e > Format.fprintf fmt "%s" (Z3.Expr.to_string e))) tl

342

* ; *)

343

if keep_hd then

344

hd::tl

345

else

346

tl

347

)

348


349

let check_sat ?(just_check=false) (l: elem_boolexpr guard) : bool * (elem_boolexpr guard) =

350

(* Syntactic simplification *)

351

if false then

352

Format.eprintf "Before simplify: %a@." (pp_guard_list pp_elem) l;

353

let l = simplify_neg_guard l in

354

if false then (

355

Format.eprintf "After simplify: %a@." (pp_guard_list pp_elem) l;

356

Format.eprintf "@[<v 2>Z3 check sat: [%a]@ " (pp_guard_list pp_elem)l;

357

);

358


359

let solver = Z3.Solver.mk_simple_solver !ctx in

360

try (

361

let zl =

362

List.map (fun (e, posneg) >

363

let ze =

364

match e with

365

 IsInit > is_init_z3e

366

 Expr e > expr_to_z3_expr e

367

in

368

if posneg then

369

ze

370

else

371

neg_ze ze

372

) l

373

in

374

if false then Format.eprintf "Z3 exprs1: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e > Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl;

375

let zl = simplify zl in

376

if false then Format.eprintf "Z3 exprs2: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e > Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl;

377

let status_res = Z3.Solver.check solver zl in

378

if false then Format.eprintf "Z3 status: %s@ @]@. " (Z3.Solver.string_of_status status_res);

379

match status_res with

380

 Z3.Solver.UNSATISFIABLE > false, []

381

 _ > (

382

if false && just_check then

383

true, l

384

else

385

(* TODO: may be reactivate but it may create new expressions *)

386

(* let l = goal_simplify zl in *)

387

let l = List.fold_left

388

(fun accu ze > accu @ (zexpr_to_guard_list ze))

389

[]

390

zl

391

in

392

(* Format.eprintf "@.@[<v 2>Check_Sat:@ before: %a@ after:

393

%a@. Goal precise? %b/%b@]@.@. " * pp_guard_list l

394

pp_guard_list l' * (Z3.Goal.is_precise goal) *

395

(Z3.Goal.is_precise goal'); *)

396


397


398

true, l

399


400


401

)

402


403

)

404

with Zustre_common.UnknownFunction(id, msg) > (

405

report ~level:1 msg;

406

true, l (* keeping everything. *)

407

)

408


409


410


411


412

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

413


414


415

let clean_sys sys =

416

List.fold_left (fun accu (guards, updates) >

417

let sat, guards' = check_sat (List.map (fun (g, pn) > Expr g, pn) guards) in

418

(*Format.eprintf "Guard: %a@.Guard cleaned: %a@.Sat? %b@."

419

(fprintf_list ~sep:"@ " (pp_guard_expr Printers.pp_expr)) guards

420

(fprintf_list ~sep:"@ " (pp_guard_expr Printers.pp_expr)) guards'

421

sat

422


423

;*)

424

if sat then

425

(List.map (fun (e, b) > (deelem e, b)) guards', updates)::accu

426

else

427

accu

428

)

429

[] sys

430


431

(* Most costly function: has the be efficiently implemented. All

432

registered guards are initially produced by the call to

433

combine_guards. We csan normalize the guards to ease the

434

comparisons.

435


436

We assume that gl1 and gl2 are already both satisfiable and in a

437

kind of reduced form. Let lshort and llong be the short and long

438

list of gl1, gl2. We check whether each element elong of llong is

439

satisfiable with lshort. If no, stop. If yes, we search to reduce

440

the list. If elong => eshort_i, we can remove eshort_i from

441

lshort. we can continue with this lshort shortened, lshort'; it is

442

not necessary to add yet elong in lshort' since we already know

443

rthat elong is somehow reduced with respect to other elements of

444

llong. If eshort_i => elong, then we keep ehosrt_i in lshort and do

445

not store elong.

446


447

After iterating through llong, we have a shortened version of

448

lshort + some elements of llong that have to be remembered. We add

449

them to this new consolidated list.

450


451

*)

452


453

(* combine_guards ~fresh:Some(e,b) gl1 gl2 returns ok, gl with ok=true

454

when (e=b) ang gl1 and gl2 is satisfiable and gl is a consilidated

455

version of it. *)

456

let combine_guards ?(fresh=None) gl1 gl2 =

457

(* Filtering out trivial cases. More semantics ones would have to be

458

addressed later *)

459

let check_sat e = (* temp function before we clean the original one *)

460

(* Format.eprintf "CheckSAT? %a@." (pp_guard_list pp_elem) e; *)

461

let ok, _ = check_sat e in

462

(* Format.eprintf "CheckSAT DONE@."; *)

463

ok

464

in

465

let implies (e1,pn1) (e2,pn2) =

466

let e2z e pn =

467

match e with

468

 IsInit > if pn then is_init_z3e else neg_ze is_init_z3e

469

 Expr e > expr_to_z3_expr (if pn then e else (Corelang.push_negations ~neg:true e))

470

in

471

implies (e2z e1 pn1) (e2z e2 pn2)

472

in

473

let lshort, llong =

474

if List.length gl1 > List.length gl2 then gl2, gl1 else gl1, gl2

475

in

476

let merge long short =

477

let short, long_sel, ok =

478

List.fold_left (fun (short,long_sel, ok) long_e >

479

if not ok then

480

[],[], false (* Propagating unsat case *)

481

else if check_sat (long_e::short) then

482

let short, keep_long_e =

483

List.fold_left (fun (accu_short, keep_long_e) eshort_i >

484

if not keep_long_e then (* shorten the algo *)

485

eshort_i :: accu_short, false

486

else (* keep_long_e = true in the following *)

487

if implies eshort_i long_e then

488

(* First case is trying to remove long_e!

489


490

Since short is already normalized, we can remove

491

long_e. If later long_e is stronger than another

492

element of short, then necessarily eshort_i =>

493

long_e >

494

that_other_element_of_short. Contradiction. *)

495

eshort_i::accu_short, false

496

else if implies long_e eshort_i then

497

(* removing eshort_i, keeping long_e. *)

498

accu_short, true

499

else (* Not comparable, keeping both *)

500

eshort_i::accu_short, true

501

)

502

([],true) (* Initially we assume that we will keep long_e *)

503

short

504

in

505

if keep_long_e then

506

short, long_e::long_sel, true

507

else

508

short, long_sel, true

509

else

510

[],[],false

511

) (short, [], true) long

512

in

513

ok, long_sel@short

514

in

515

let ok, l = match fresh with

516

 None > true, []

517

 Some g > merge [g] []

518

in

519

if not ok then

520

false, []

521

else

522

let ok, lshort = merge lshort l in

523

if not ok then

524

false, []

525

else

526

merge llong lshort

527


528


529

(* Encode "If gel1=posneg then gel2":

530

 Compute the combination of guarded exprs in gel1 and gel2:

531

 Each guarded_expr in gel1 is transformed as a guard: the

532

expression is associated to posneg.

533

 Existing guards in gel2 are concatenated to that list of guards

534

 We keep expr in the ge of gel2 as the legitimate expression

535

*)

536

let concatenate_ge gel1 posneg gel2 =

537

let l, all_invalid =

538

List.fold_left (

539

fun (accu, all_invalid) (g2,e2) >

540

List.fold_left (

541

fun (accu, all_invalid) (g1,e1) >

542

(* Format.eprintf "@[<v 2>Combining guards: (%a=%b) AND [%a] AND [%a]@ "

543

* pp_elem e1

544

* posneg

545

* pp_guard_list g1

546

* pp_guard_list g2; *)

547


548

let ok, gl = combine_guards ~fresh:(Some(e1,posneg)) g1 g2 in

549

(* Format.eprintf "@]@ Result is [%a]@ "

550

* pp_guard_list gl; *)

551


552

if ok then

553

(gl, e2)::accu, false

554

else (

555

accu, all_invalid

556

)

557

) (accu, all_invalid) gel1

558

) ([], true) gel2

559

in

560

not all_invalid, l

561


562

(* Transform the guard expressions ge = [gl1, e1; gl2, e2;...] as

563

[gl1, e1=id; gl2, e2=id; ...] *)

564

let mk_ge_eq_id ge id =

565

List.map

566

(fun (gl, g_e) >

567

gl,

568

if id = "true" then

569

g_e

570

else

571

match g_e with

572

 Expr g_e >

573

if id = "false" then

574

Expr (Corelang.push_negations ~neg:true g_e)

575

else

576

let loc = g_e.expr_loc in

577

Expr(Corelang.mk_eq loc

578

g_e

579

(Corelang.expr_of_ident id loc))

580

 _ > assert false

581

) ge

582


583

(* Rewrite the expression expr, replacing any occurence of a variable

584

by its definition.

585

*)

586

let rec rewrite defs expr : elem_guarded_expr list =

587

let rewrite = rewrite defs in

588

let res =

589

match expr.expr_desc with

590

 Expr_appl (id, args, None) >

591

let args = rewrite args in

592

List.map (fun (guards, e) >

593

let new_e =

594

Corelang.mkexpr

595

expr.expr_loc

596

(Expr_appl(id, deelem e, None))

597

in

598

guards,

599

Expr (Corelang.partial_eval new_e)

600

) args

601

 Expr_const _ > [[], Expr expr]

602

 Expr_ident id >

603

if Hashtbl.mem defs id then

604

Hashtbl.find defs id

605

else

606

(* id should be an input *)

607

[[], Expr expr]

608

 Expr_ite (g, e1, e2) >

609

let g = rewrite g and

610

e1 = rewrite e1 and

611

e2 = rewrite e2 in

612

let ok_then, g_then = concatenate_ge g true e1 in

613

let ok_else, g_else = concatenate_ge g false e2 in

614

(if ok_then then g_then else [])@

615

(if ok_else then g_else else [])

616

 Expr_merge (g_id, branches) >

617

if Hashtbl.mem defs g_id then

618

let g = Hashtbl.find defs g_id in

619

(* Format.eprintf "Expr_merge %s = %a@." g_id (pp_mdefs pp_elem) g ; *)

620

List.fold_left (fun accu (id, e) >

621

let g = mk_ge_eq_id g id in

622

let e = rewrite e in

623

let ok, g_eq_id = concatenate_ge g true e in

624

if ok then g_eq_id@accu else accu

625

) [] branches

626

else

627

assert false (* g should be defined already *)

628

 Expr_when (e, id, l) >

629

let e = rewrite e in

630

let id_def = Hashtbl.find defs id in

631

let clock = mk_ge_eq_id id_def l in

632

let ok, new_ge = concatenate_ge clock true e in

633

if ok then new_ge else []

634

 Expr_arrow _ > [[], IsInit] (* At this point the only arrow should be true > false *)

635

 Expr_tuple el >

636

(* Each expr is associated to its flatten guarded expr list *)

637

let gell = List.map rewrite el in

638

(* Computing all combinations: we obtain a list of guarded tuple *)

639

let rec aux gell : (elem_boolexpr guard * expr list) list =

640

match gell with

641

 [] > assert false (* Not happening *)

642

 [gel] > List.map (fun (g,e) > g, [deelem e]) gel

643

 gel::getl >

644

let getl = aux getl in

645

List.fold_left (

646

fun accu (g,e) >

647

List.fold_left (

648

fun accu (gl, minituple) >

649

let is_compat, guard_comb = combine_guards g gl in

650

if is_compat then

651

let new_gt : elem_boolexpr guard * expr list =

652

(guard_comb, (deelem e)::minituple) in

653

new_gt::accu

654

else

655

accu

656


657

) accu getl

658

) [] gel

659

in

660

let gtuples = aux gell in

661

(* Rebuilding the valid type: guarded expr list (with tuple exprs) *)

662

List.map

663

(fun (g,tuple) > g, Expr (Corelang.mkexpr expr.expr_loc (Expr_tuple tuple)))

664

gtuples

665

 Expr_fby _

666

 Expr_appl _

667

(* Should be removed by normalization and inlining *)

668

> Format.eprintf "Pb expr: %a@.@?" Printers.pp_expr expr; assert false

669

 Expr_array _  Expr_access _  Expr_power _

670

(* Arrays not handled here yet *)

671

> assert false

672

 Expr_pre _ > (* Not rewriting mem assign *)

673

assert false

674

in

675

(* Format.eprintf "Rewriting %a as [@[<v 0>%a@]]@ "

676

* Printers.pp_expr expr

677

* (Utils.fprintf_list ~sep:"@ "

678

* pp_guard_expr) res; *)

679

res

680


681

and add_def defs vid expr =

682

(* Format.eprintf "Add_def: %s = %a@."

683

* vid

684

* Printers.pp_expr expr; *)

685

let vid_defs = rewrite defs expr in

686

(* Format.eprintf "> @[<v 0>%a@]@."

687

* (Utils.fprintf_list ~sep:"@ "

688

* (pp_guard_expr pp_elem)) vid_defs; *)

689

report ~level:6 (fun fmt > Format.fprintf fmt "Add_def: %s = %a@. > @[<v 0>%a@]@."

690

vid

691

Printers.pp_expr expr

692


693

(

694

(Utils.fprintf_list ~sep:"@ "

695

(pp_guard_expr pp_elem))) vid_defs);

696

Hashtbl.add defs vid vid_defs;

697

vid_defs

698


699

(* Takes a list of guarded exprs (ge) and a guard

700

returns the same list of ge splited into the ones where the guard is true and the ones where it is false. In both lists the associated ge do not mention that guard anymore.

701


702

When a given ge doesn't mention positively or negatively such guards, it is duplicated in both lists *)

703

let split_mdefs elem (mdefs: elem_guarded_expr list) =

704

List.fold_left (

705

fun (selected, left_out)

706

((guards, expr) as ge) >

707

(* select the element of guards that match the argument elem *)

708

let sel, others_guards = List.partition (select_elem elem) guards in

709

match sel with

710

(* we extract the element from the list and add it to the

711

appropriate list *)

712

 [_, sel_status] >

713

if sel_status then

714

(others_guards,expr)::selected, left_out

715

else selected, (others_guards,expr)::left_out

716

 [] > (* no such guard exists, we have to duplicate the

717

guard_expr in both lists *)

718

ge::selected, ge::left_out

719

 _ > (

720

Format.eprintf "@.Spliting list on elem %a.@.List:%a@."

721

pp_elem elem

722

(pp_mdefs pp_elem) mdefs;

723

assert false (* more then one element selected. Should

724

not happen , or trival dead code like if

725

x then if not x then dead code *)

726

)

727

) ([],[]) mdefs

728


729

let split_mem_defs

730

(elem: element)

731

(mem_defs: (ident * elem_guarded_expr list) list)

732

:

733

((ident * elem_guarded_expr mdef_t) list) * ((ident * elem_guarded_expr mdef_t) list)

734


735

=

736

List.fold_right (fun (m,mdefs)

737

(accu_pos, accu_neg) >

738

let pos, neg =

739

split_mdefs elem mdefs

740

in

741

(m, pos)::accu_pos,

742

(m, neg)::accu_neg

743

) mem_defs ([],[])

744


745


746

(* Split a list of mem_defs into init and step lists of guarded

747

expressions per memory. *)

748

let split_init mem_defs =

749

split_mem_defs IsInit mem_defs

750


751

(* Previous version of the function: way too costly

752

let pick_guard mem_defs : expr option =

753

let gel = List.flatten (List.map snd mem_defs) in

754

let gl = List.flatten (List.map fst gel) in

755

let all_guards =

756

List.map (

757

(* selecting guards and getting rid of boolean *)

758

fun (e,b) >

759

match e with

760

 Expr e > e

761

 _ > assert false

762

(* should have been filtered out

763

yet *)

764

) gl

765

in

766

(* TODO , one could sort by occurence and provided the most common

767

one *)

768

try

769

Some (List.hd all_guards)

770

with _ > None

771

*)

772


773

(* Returning the first non empty guard expression *)

774

let rec pick_guard mem_defs : expr option =

775

match mem_defs with

776

 [] > None

777

 (_, gel)::tl > (

778

let found =

779

List.fold_left (fun found (g,_) >

780

if found = None then

781

match g with

782

 [] > None

783

 (Expr e, _)::_ > Some e

784

 (IsInit, _)::_ > assert false (* should be removed already *)

785

else

786

found

787

) None gel

788

in

789

if found = None then pick_guard tl else found

790

)

791


792


793

(* Transform a list of variable * guarded exprs into a list of guarded pairs (variable, expressions)

794

*)

795

let rec build_switch_sys

796

(mem_defs : (Utils.ident * elem_guarded_expr list) list )

797

prefix

798

:

799

((expr * bool) list * (ident * expr) list ) list =

800

if !seal_debug then

801

report ~level:4 (fun fmt > Format.fprintf fmt "@[<v 2>Build_switch with@ %a@]@."

802

pp_all_defs

803

mem_defs);

804

(* if all mem_defs have empty guards, we are done, return prefix,

805

mem_defs expr.

806


807

otherwise pick a guard in one of the mem, eg (g, b) then for each

808

other mem, one need to select the same guard g with the same

809

status b, *)

810

let res =

811

if List.for_all (fun (m,mdefs) >

812

(* All defs are unguarded *)

813

match mdefs with

814

 [[], _] > true (* Regular unguarded expression *)

815

 [] > true (* A unbalanced definition of the memory. Here

816

we have m_{k+1} > m_k *)

817

 _ > false

818

) mem_defs

819

then

820

[prefix ,

821

List.map (fun (m,gel) >

822

match gel with

823

 [_,e] >

824

let e =

825

match e with

826

 Expr e > e

827

 _ > assert false (* No IsInit expression *)

828

in

829

m,e

830

 [] > m, Corelang.expr_of_ident m Location.dummy_loc

831

 _ > assert false

832

) mem_defs]

833

else

834

(* Picking a guard *)

835

let elem_opt : expr option = pick_guard mem_defs in

836

match elem_opt with

837

None > (

838

Format.eprintf "Issues picking guard in mem_defs: %a@." pp_all_defs mem_defs;

839

assert false (* Otherwise the first case should have matched *)

840

)

841

 Some elem > (

842

report ~level:4 (fun fmt > Format.fprintf fmt "selecting guard %a@." Printers.pp_expr elem);

843

let pos, neg =

844

split_mem_defs

845

(Expr elem)

846

mem_defs

847

in

848

(* Format.eprintf "Selected item %a in@.%a@.POS=%a@.NEG=%a@."

849

Printers.pp_expr elem

850

pp_all_defs mem_defs

851

pp_all_defs pos

852

pp_all_defs neg

853

;

854

*)

855

(* Special cases to avoid useless computations: true, false conditions *)

856

match elem.expr_desc with

857

(* Expr_ident "true" > build_switch_sys pos prefix *)

858

 Expr_const (Const_tag tag) when tag = tag_true

859

> build_switch_sys pos prefix

860

(* Expr_ident "false" > build_switch_sys neg prefix *)

861

 Expr_const (Const_tag tag) when tag = tag_false

862

> build_switch_sys neg prefix

863

 _ > (* Regular case *)

864

(* let _ = (

865

* Format.eprintf "Expr is %a@." Printers.pp_expr elem;

866

* match elem.expr_desc with

867

*  Expr_const _ > Format.eprintf "a const@."

868

*

869

*  Expr_ident _ > Format.eprintf "an ident@."

870

*  _ > Format.eprintf "something else@."

871

* )

872

* in *)

873

let clean l =

874

let l = List.map (fun (e,b) > (Expr e), b) l in

875

let ok, l = check_sat l in

876

let l = List.map (fun (e,b) > deelem e, b) l in

877

ok, l

878

in

879

let pos_prefix = (elem, true)::prefix in

880

let neg_prefix = (elem, false)::prefix in

881

let ok_pos, pos_prefix = clean pos_prefix in

882

let ok_neg, neg_prefix = clean neg_prefix in

883

report ~level:4 (fun fmt > Format.fprintf fmt "Enforcing %a@." Printers.pp_expr elem);

884

let ok_l = if ok_pos then build_switch_sys pos pos_prefix else [] in

885

report ~level:4 (fun fmt > Format.fprintf fmt "Enforcing not(%a)@." Printers.pp_expr elem);

886

let nok_l = if ok_neg then build_switch_sys neg neg_prefix else [] in

887

ok_l @ nok_l

888

)

889

in

890

if !seal_debug then (

891

report ~level:4 (fun fmt >

892

Format.fprintf fmt

893

"@[<v 2>===> @[%t@ @]@]@ @]@ "

894

(fun fmt > List.iter (fun (gl,up) >

895

Format.fprintf fmt "[@[%a@]] > (%a)@ "

896

(pp_guard_list Printers.pp_expr) gl pp_up up) res);

897


898

));

899

res

900


901


902


903

(* Take a normalized node and extract a list of switches: (cond,

904

update) meaning "if cond then update" where update shall define all

905

node memories. Everything as to be expressed over inputs or memories, intermediate variables are removed through inlining *)

906

let node_as_switched_sys consts (mems:var_decl list) nd =

907

(* rescheduling node: has been scheduled already, no need to protect

908

the call to schedule_node *)

909

let nd_report = Scheduling.schedule_node nd in

910

let schedule = nd_report.Scheduling_type.schedule in

911

let eqs, auts = Corelang.get_node_eqs nd in

912

assert (auts = []); (* Automata should be expanded by now *)

913

let sorted_eqs, unused = Scheduling.sort_equations_from_schedule eqs schedule in

914

let defs : (ident, elem_guarded_expr list) Hashtbl.t = Hashtbl.create 13 in

915

let add_def = add_def defs in

916


917

let vars = Corelang.get_node_vars nd in

918

(* Filtering out unused vars *)

919

let vars = List.filter (fun v > not (List.mem v.var_id unused)) vars in

920

(* Registering all locals variables as Z3 predicates. Will be use to

921

simplify the expansion *)

922

Zustre_common.decl_sorts ();

923

let _ =

924

List.iter (fun v >

925

let fdecl = Z3.FuncDecl.mk_func_decl_s

926

!ctx

927

v.var_id

928

[]

929

(Zustre_common.type_to_sort v.var_type)

930

in

931

ignore (Zustre_common.register_fdecl v.var_id fdecl)

932

) vars

933

in

934

let _ =

935

List.iter (fun c > Hashtbl.add const_defs c.const_id c.const_value) consts

936

in

937


938

report ~level:4 (fun fmt > Format.fprintf fmt "Computing definitions for equations@.%a@."

939

Printers.pp_node_eqs sorted_eqs

940

);

941


942


943

(* Registering node equations: identifying mem definitions and

944

storing others in the "defs" hashtbl.

945


946

Each assign is stored in a hash tbl as list of guarded

947

expressions. The memory definition is also "rewritten" as such a

948

list of guarded assigns. *)

949

let mem_defs, output_defs =

950

List.fold_left (fun (accu_mems, accu_outputs) eq >

951

match eq.eq_lhs with

952

 [vid] >

953

(* Only focus on memory definitions *)

954

if List.exists (fun v > v.var_id = vid) mems then

955

(

956

match eq.eq_rhs.expr_desc with

957

 Expr_pre def_m >

958

report ~level:3 (fun fmt >

959

Format.fprintf fmt "Preparing mem %s@." vid);

960

let def_vid = rewrite defs def_m in

961

report ~level:4 (fun fmt >

962

Format.fprintf fmt "%s = %a@." vid

963

(

964

(Utils.fprintf_list ~sep:"@ "

965

(pp_guard_expr pp_elem)))

966

def_vid);

967

(vid, def_vid)::accu_mems, accu_outputs

968

 _ > assert false

969

)

970

else if List.exists (fun v > v.var_id = vid) nd.node_outputs then (

971

report ~level:3 (fun fmt >

972

Format.fprintf fmt "Output variable %s@." vid);

973

let def_vid = add_def vid eq.eq_rhs in

974

accu_mems, (vid, def_vid)::accu_outputs

975


976

)

977

else

978

(

979

report ~level:3 (fun fmt >

980

Format.fprintf fmt "Registering variable %s@." vid);

981

let _ = add_def vid eq.eq_rhs in

982

accu_mems, accu_outputs

983

)

984

 _ > assert false (* should have been removed by normalization *)

985

) ([], []) sorted_eqs

986

in

987


988


989

report ~level:2 (fun fmt > Format.fprintf fmt "Printing out (guarded) memories definitions (may takes time)@.");

990

(* Printing memories definitions *)

991

report ~level:3

992

(fun fmt >

993

Format.fprintf fmt

994

"@[<v 0>%a@]@."

995

(Utils.fprintf_list ~sep:"@ "

996

(fun fmt (m,mdefs) >

997

Format.fprintf fmt

998

"%s > [@[<v 0>%a@] ]@ "

999

m

1000

(Utils.fprintf_list ~sep:"@ "

1001

(pp_guard_expr pp_elem)) mdefs

1002

))

1003

mem_defs);

1004

(* Format.eprintf "Split init@."; *)

1005

let init_defs, update_defs =

1006

split_init mem_defs

1007

in

1008

let init_out, update_out =

1009

split_init output_defs

1010

in

1011

report ~level:3

1012

(fun fmt >

1013

Format.fprintf fmt

1014

"@[<v 0>Init:@ %a@]@."

1015

(Utils.fprintf_list ~sep:"@ "

1016

(fun fmt (m,mdefs) >

1017

Format.fprintf fmt

1018

"%s > @[<v 0>[%a@] ]@ "

1019

m

1020

(Utils.fprintf_list ~sep:"@ "

1021

(pp_guard_expr pp_elem)) mdefs

1022

))

1023

init_defs);

1024

report ~level:3

1025

(fun fmt >

1026

Format.fprintf fmt

1027

"@[<v 0>Step:@ %a@]@."

1028

(Utils.fprintf_list ~sep:"@ "

1029

(fun fmt (m,mdefs) >

1030

Format.fprintf fmt

1031

"%s > @[<v 0>[%a@] ]@ "

1032

m

1033

(Utils.fprintf_list ~sep:"@ "

1034

(pp_guard_expr pp_elem)) mdefs

1035

))

1036

update_defs);

1037

(* Format.eprintf "Build init@."; *)

1038

report ~level:4 (fun fmt > Format.fprintf fmt "Build init@.");

1039

let sw_init=

1040

build_switch_sys init_defs []

1041

in

1042

(* Format.eprintf "Build step@."; *)

1043

report ~level:4 (fun fmt > Format.fprintf fmt "Build step@.");

1044

let sw_sys =

1045

build_switch_sys update_defs []

1046

in

1047


1048

report ~level:4 (fun fmt > Format.fprintf fmt "Build init out@.");

1049

let init_out =

1050

build_switch_sys init_out []

1051

in

1052

report ~level:4 (fun fmt > Format.fprintf fmt "Build step out@.");

1053


1054

let update_out =

1055

build_switch_sys update_out []

1056

in

1057


1058

let sw_init = clean_sys sw_init in

1059

let sw_sys = clean_sys sw_sys in

1060

let init_out = clean_sys init_out in

1061

let update_out = clean_sys update_out in

1062


1063

(* Some additional checks *)

1064


1065

if false then

1066

begin

1067

Format.eprintf "@.@.CHECKING!!!!!!!!!!!@.";

1068

Format.eprintf "Any duplicate expression in guards?@.";

1069


1070

let sw_sys =

1071

List.map (fun (gl, up) >

1072

let gl = List.sort (fun (e,b) (e',b') >

1073

let res = compare e.expr_tag e'.expr_tag in

1074

if res = 0 then (Format.eprintf "Same exprs?@.%a@.%a@.@."

1075

Printers.pp_expr e

1076

Printers.pp_expr e'

1077

);

1078

res

1079

) gl in

1080

gl, up

1081

) sw_sys

1082

in

1083

Format.eprintf "Another check for duplicates in guard list@.";

1084

List.iter (fun (gl, _) >

1085

let rec aux hd l =

1086

match l with

1087

[] > ()

1088

 (e,b)::tl > let others = hd@tl in

1089

List.iter (fun (e',_) > if Corelang.is_eq_expr e e' then

1090

(Format.eprintf "Same exprs?@.%a@.%a@.@."

1091

Printers.pp_expr e

1092

Printers.pp_expr e'

1093

)) others;

1094

aux ((e,b)::hd) tl

1095

in

1096

aux [] gl

1097

) sw_sys;

1098

Format.eprintf "Checking duplicates in updates@.";

1099

let rec check_dup_up accu l =

1100

match l with

1101

 [] > ()

1102

 ((gl, up) as hd)::tl >

1103

let others = accu@tl in

1104

List.iter (fun (gl',up') > if up = up' then

1105

Format.eprintf "Same updates?@.%a@.%a@.%a@.%a@.@."

1106


1107

pp_gl_short gl

1108

pp_up up

1109

pp_gl_short gl'

1110

pp_up up'

1111


1112

) others;

1113


1114


1115


1116

check_dup_up (hd::accu) tl

1117


1118

in

1119

check_dup_up [] sw_sys;

1120

let _ (* sw_sys *) =

1121

List.sort (fun (gl1, _) (gl2, _) >

1122

let glid gl = List.map (fun (e,_) > e.expr_tag) gl in

1123


1124

let res = compare (glid gl1) (glid gl2) in

1125

if res = 0 then Format.eprintf "Same guards?@.%a@.%a@.@."

1126

pp_gl_short gl1 pp_gl_short gl2

1127

;

1128

res

1129


1130

) sw_sys

1131


1132

in

1133

()

1134

end;

1135


1136


1137

(* Iter through the elements and gather them by updates *)

1138

let process sys =

1139

(* The map will associate to each update up the pair (set, set

1140

list) where set is the share guards and set list a list of

1141

disjunctive guards. Each set represents a conjunction of

1142

expressions. *)

1143

report ~level:3 (fun fmt > Format.fprintf fmt "%t@."

1144

(fun fmt > List.iter (fun (gl,up) >

1145

Format.fprintf fmt "[@[%a@]] > (%a)@ "

1146

(pp_guard_list Printers.pp_expr) gl pp_up up) sw_init));

1147


1148

(* We perform multiple pass to avoid errors *)

1149

let map =

1150

List.fold_left (fun map (gl,up) >

1151

(* creating a new set to describe gl *)

1152

let new_set =

1153

List.fold_left

1154

(fun set g > Guards.add g set)

1155

Guards.empty

1156

gl

1157

in

1158

(* updating the map with up > new_set *)

1159

if UpMap.mem up map then

1160

let guard_set = UpMap.find up map in

1161

UpMap.add up (new_set::guard_set) map

1162

else

1163

UpMap.add up [new_set] map

1164

) UpMap.empty sys

1165

in

1166

(* Processing the set of guards leading to the same update: return

1167

conj, disj with conf is a set of guards, and disj a DNF, ie a

1168

list of set of guards *)

1169

let map =

1170

UpMap.map (

1171

fun guards >

1172

match guards with

1173

 [] > Guards.empty, [] (* Nothing *)

1174

 [s]> s, [] (* basic case *)

1175

 hd::tl >

1176

let shared = List.fold_left (fun shared s > Guards.inter shared s) hd tl in

1177

let remaining = List.map (fun s > Guards.diff s shared) guards in

1178

(* If one of them is empty, we can remove the others, otherwise keep them *)

1179

if List.exists Guards.is_empty remaining then

1180

shared, []

1181

else

1182

shared, remaining

1183

) map

1184

in

1185

let rec mk_binop op l = match l with

1186

[] > assert false

1187

 [e] > e

1188

 hd::tl > Corelang.mkpredef_call hd.expr_loc op [hd; mk_binop op tl]

1189

in

1190

let gl_as_expr gl =

1191

let gl = Guards.elements gl in

1192

let export (e,b) = if b then e else Corelang.push_negations ~neg:true e in

1193

match gl with

1194

[] > []

1195

 [e] > [export e]

1196

 _ >

1197

[mk_binop "&&"

1198

(List.map export gl)]

1199

in

1200

let rec clean_disj disj =

1201

match disj with

1202

 [] > []

1203

 [_] > assert false (* A disjunction was a single case can be ignored *)

1204

 _::_::_ > (

1205

(* First basic version: producing a DNF One can later, (1)

1206

simplify it with z3, or (2) build the compact tree with

1207

maximum shared subexpression (and simplify it with z3) *)

1208

let elems = List.fold_left (fun accu gl > (gl_as_expr gl) @ accu) [] disj in

1209

let or_expr = mk_binop "" elems in

1210

[or_expr]

1211


1212


1213

(* TODO disj*)

1214

(* get the item that occurs in most case *)

1215

(* List.fold_left (fun accu s >

1216

* List.fold_left (fun accu (e,b) >

1217

* if List.mem_assoc (e.expr_tag, b)

1218

* ) accu (Guards.elements s)

1219

* ) [] disj *)

1220


1221

)

1222

in

1223

if !seal_debug then Format.eprintf "Map: %i elements@ " (UpMap.cardinal map);

1224

UpMap.fold (fun up (common, disj) accu >

1225

if !seal_debug then

1226

report ~level:6 (fun fmt > Format.fprintf fmt

1227

"Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@."

1228

Guards.pp_short common

1229

(fprintf_list ~sep:";@ " Guards.pp_long) disj

1230

UpMap.pp up);

1231

let disj = clean_disj disj in

1232

let guard_expr = (gl_as_expr common)@disj in

1233


1234

((match guard_expr with

1235

 [] > None

1236

 _ > Some (mk_binop "&&" guard_expr)), up)::accu

1237

) map []

1238


1239

in

1240


1241


1242


1243

report ~level:3 (fun fmt > Format.fprintf fmt "Process sw_init:@.");

1244

let sw_init = process sw_init in

1245

report ~level:3 (fun fmt > Format.fprintf fmt "Process sw_sys:@.");

1246

let sw_sys = process sw_sys in

1247

report ~level:3 (fun fmt > Format.fprintf fmt "Process init_out:@.");

1248

let init_out = process init_out in

1249

report ~level:3 (fun fmt > Format.fprintf fmt "Process update_out:@.");

1250

let update_out = process update_out in

1251

sw_init , sw_sys, init_out, update_out
