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 get_const id = Hashtbl.find const_defs id

24


25

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

26

arrows, fby, ... *)

27


28

(* Set of hash to support memoization *)

29

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

30

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

31

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

32

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

33

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

34

let pp_ze_hash fmt = pp_hash

35

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

36

Format.pp_print_int

37

fmt

38

ze_hash

39

let pp_e_hash fmt = pp_hash

40

Format.pp_print_int

41

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

42

fmt

43

e_hash

44

let mem_expr e =

45

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

46

* Printers.pp_expr e

47

* pp_e_map; *)

48

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

49

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

50

res

51


52

let mem_zexpr ze =

53

Hashtbl.mem ze_hash ze

54

let get_zexpr e =

55

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

56

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

57

Hashtbl.find e_hash uid

58

let get_expr ze =

59

let uid = Hashtbl.find ze_hash ze in

60

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

61

e

62


63

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

64

let is_init_z3e =

65

Z3.Expr.mk_const_s !ctx is_init_name Zustre_common.bool_sort

66


67

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

68

try

69

if Z3.Expr.equal ze is_init_z3e then 1 else

70

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

71

Hashtbl.find ze_hash ze

72

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

73

(Z3.Expr.to_string ze)

74

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

75

assert false)

76

let add_expr =

77

let cpt = ref 0 in

78

fun e ze >

79

incr cpt;

80

let uid = !cpt in

81

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

82

Hashtbl.add e_hash uid ze;

83

Hashtbl.add ze_hash ze uid

84


85


86

let expr_to_z3_expr, zexpr_to_expr =

87

(* List to store converted expression. *)

88

(* let hash = ref [] in

89

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

90

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

91


92

let rec e2ze e =

93

if mem_expr e then (

94

get_zexpr e

95

)

96

else (

97

let res =

98

match e.expr_desc with

99

 Expr_const c >

100

let z3e = Zustre_common.horn_const_to_expr c in

101

add_expr e z3e;

102

z3e

103

 Expr_ident id > (

104

if is_const id then (

105

let c = get_const id in

106

let z3e = Zustre_common.horn_const_to_expr c in

107

add_expr e z3e;

108

z3e

109

)

110

else (

111

let fdecl_id = Zustre_common.get_fdecl id in

112

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

113

add_expr e z3e;

114

z3e

115

)

116

)

117

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

118

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

119

add_expr e z3e;

120

z3e

121

 Expr_tuple [e] >

122

let z3e = e2ze e in

123

add_expr e z3e;

124

z3e

125

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

126

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

127

; assert false

128

in

129

res

130

)

131

in

132

let rec ze2e ze =

133

let ze_name ze =

134

let fd = Z3.Expr.get_func_decl ze in

135

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

136

in

137

if mem_zexpr ze then

138

None, Some (get_expr ze)

139

else

140

let open Corelang in

141

let fd = Z3.Expr.get_func_decl ze in

142

let zel = Z3.Expr.get_args ze in

143

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

144

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

145


146

(* Extracting IsInit status *)

147

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

148

Some false, None

149

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

150

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

151

 op, _ > (

152


153


154

if Z3.Expr.is_numeral ze then

155

let e =

156

if Z3.Arithmetic.is_real ze then

157

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

158

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

159

mkexpr

160

Location.dummy_loc

161

(Expr_const

162

(Const_real

163

(num, 0, s)))

164

else if Z3.Arithmetic.is_int ze then

165

mkexpr

166

Location.dummy_loc

167

(Expr_const

168

(Const_int

169

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

170

else if Z3.Expr.is_const ze then

171

match Z3.Expr.to_string ze with

172

 "true" > mkexpr Location.dummy_loc

173

(Expr_const (Const_tag (tag_true)))

174

 "false" >

175

mkexpr Location.dummy_loc

176

(Expr_const (Const_tag (tag_false)))

177

 _ > assert false

178

else

179

(

180

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

181

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

182

)

183

in

184

None, Some e

185

else

186

match op with

187

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

188

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

189

>

190

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

191

None, Some (mkpredef_call Location.dummy_loc op args)

192

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

193

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

194

let e = match args with

195

[] > assert false

196

 [hd] > hd

197

 e1::e2::tl >

198

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

199

if tl = [] then first_binary_and else

200

List.fold_left (fun e e_new >

201

mkpredef_call Location.dummy_loc op [e;e_new]

202

) first_binary_and tl

203


204

in

205

None, Some e

206

)

207

 "and"  "or" > (

208

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

209

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

210

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

211

match args with

212

 [] > assert false

213

 [hd] > hd

214

 hd::tl >

215

List.fold_left

216

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

217

(match is_init_opt1, is_init_opt2 with

218

None, x  x, None > x

219

 Some _, Some _ > assert false),

220

(match expr_opt1, expr_opt2 with

221

 None, x  x, None > x

222

 Some e1, Some e2 >

223

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

224

))

225

hd tl

226

)

227

 op >

228

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

229

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

230

)

231

in

232

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

233


234


235

let zexpr_to_guard_list ze =

236

let init_opt, expr_opt = zexpr_to_expr ze in

237

(match init_opt with

238

 None > []

239

Some b > [IsInit, b]

240

) @ (match expr_opt with

241

 None > []

242

 Some e > [Expr e, true]

243

)

244


245


246

let simplify_neg_guard l =

247

List.map (fun (g,posneg) >

248

match g with

249

 IsInit > g, posneg

250

 Expr g >

251

if posneg then

252

Expr (Corelang.push_negations g),

253

true

254

else

255

(* Pushing the negation in the expression *)

256

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

257

true

258

) l

259


260

(* TODO:

261

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

262

*)

263

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

264

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

265

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

266

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

267

(*

268

let goal_simplify zl =

269

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

270

Z3.Goal.add goal zl;

271

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

272

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

273

* (Z3.Goal.to_string goal)

274

* (Z3.Goal.to_string goal')

275

* (Z3.Solver.string_of_status status_res)

276

* ; *)

277

let ze = Z3.Goal.as_expr goal' in

278

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

279

zexpr_to_guard_list ze

280

*)

281


282

let implies =

283

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

284

fun ze1 ze2 >

285

let ze1_uid = get_zid ze1 in

286

let ze2_uid = get_zid ze2 in

287

if Hashtbl.mem ze_implies_hash (ze1_uid, ze2_uid) then

288

Hashtbl.find ze_implies_hash (ze1_uid, ze2_uid)

289

else

290

begin

291

if !seal_debug then (

292

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

293

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

294

));

295

let solver = Z3.Solver.mk_simple_solver !ctx in

296

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

297

let res =

298

try

299

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

300

match status_res with

301

 Z3.Solver.UNSATISFIABLE > if !seal_debug then

302

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

303

true

304

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

305

false

306

with Zustre_common.UnknownFunction(id, msg) > (

307

report ~level:1 msg;

308

false

309

)

310

in

311

Hashtbl.add ze_implies_hash (ze1_uid,ze2_uid) res ;

312

res

313

end

314


315

let rec simplify zl =

316

match zl with

317

 []  [_] > zl

318

 hd::tl > (

319

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

320

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

321

let tl = simplify tl in

322

let keep_hd, tl =

323

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

324

if implies hd e then

325

true, accu (* throwing away e *)

326

else if implies e hd then

327

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

328

else

329

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

330

) (true,[]) tl

331

in

332

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

333

* keep_hd

334

* (Z3.Expr.to_string hd)

335

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

336

* ; *)

337

if keep_hd then

338

hd::tl

339

else

340

tl

341

)

342


343

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

344

(* Syntactic simplification *)

345

if false then

346

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

347

let l = simplify_neg_guard l in

348

if false then (

349

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

350

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

351

);

352

let solver = Z3.Solver.mk_simple_solver !ctx in

353

try (

354

let zl =

355

List.map (fun (e, posneg) >

356

let ze =

357

match e with

358

 IsInit > is_init_z3e

359

 Expr e > expr_to_z3_expr e

360

in

361

if posneg then

362

ze

363

else

364

neg_ze ze

365

) l

366

in

367

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

368

let zl = simplify zl in

369

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

370

let status_res = Z3.Solver.check solver zl in

371

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

372

match status_res with

373

 Z3.Solver.UNSATISFIABLE > false, []

374

 _ > (

375

if false && just_check then

376

true, l

377

else

378

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

379

(* let l = goal_simplify zl in *)

380

let l = List.fold_left

381

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

382

[]

383

zl

384

in

385

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

386

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

387

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

388

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

389


390


391

true, l

392


393


394

)

395


396

)

397

with Zustre_common.UnknownFunction(id, msg) > (

398

report ~level:1 msg;

399

true, l (* keeping everything. *)

400

)

401


402


403


404


405

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

406


407


408

let clean_sys sys =

409

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

410

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

411

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

412

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

413

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

414

sat

415


416

;*)

417

if sat then

418

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

419

else

420

accu

421

)

422

[] sys

423


424

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

425

registered guards are initially produced by the call to

426

combine_guards. We csan normalize the guards to ease the

427

comparisons.

428


429

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

430

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

431

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

432

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

433

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

434

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

435

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

436

rthat elong is somehow reduced with respect to other elements of

437

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

438

not store elong.

439


440

After iterating through llong, we have a shortened version of

441

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

442

them to this new consolidated list.

443


444

*)

445


446

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

447

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

448

version of it. *)

449

let combine_guards ?(fresh=None) gl1 gl2 =

450

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

451

addressed later *)

452

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

453

let ok, _ = check_sat e in

454

ok

455

in

456

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

457

let e2z e pn =

458

match e with

459

 IsInit > if pn then is_init_z3e else neg_ze is_init_z3e

460

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

461

in

462

implies (e2z e1 pn1) (e2z e2 pn2)

463

in

464

let lshort, llong =

465

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

466

in

467

let merge long short =

468

let short, long_sel, ok =

469

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

470

if not ok then

471

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

472

else if check_sat (long_e::short) then

473

let short, keep_long_e =

474

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

475

if not keep_long_e then (* shorten the algo *)

476

eshort_i :: accu_short, false

477

else (* keep_long_e = true in the following *)

478

if implies eshort_i long_e then

479

(* First case is trying to remove long_e!

480


481

Since short is already normalized, we can remove

482

long_e. If later long_e is stronger than another

483

element of short, then necessarily eshort_i =>

484

long_e >

485

that_other_element_of_short. Contradiction. *)

486

eshort_i::accu_short, false

487

else if implies long_e eshort_i then

488

(* removing eshort_i, keeping long_e. *)

489

accu_short, true

490

else (* Not comparable, keeping both *)

491

eshort_i::accu_short, true

492

)

493

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

494

short

495

in

496

if keep_long_e then

497

short, long_e::long_sel, true

498

else

499

short, long_sel, true

500

else

501

[],[],false

502

) (short, [], true) long

503

in

504

ok, long_sel@short

505

in

506

let ok, l = match fresh with

507

 None > true, []

508

 Some g > merge [g] []

509

in

510

if not ok then

511

false, []

512

else

513

let ok, lshort = merge lshort l in

514

if not ok then

515

false, []

516

else

517

merge llong lshort

518


519


520

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

521

 Compute the combination of guarded exprs in gel1 and gel2:

522

 Each guarded_expr in gel1 is transformed as a guard: the

523

expression is associated to posneg.

524

 Existing guards in gel2 are concatenated to that list of guards

525

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

526

*)

527

let concatenate_ge gel1 posneg gel2 =

528

let l, all_invalid =

529

List.fold_left (

530

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

531

List.fold_left (

532

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

533

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

534

* pp_elem e1

535

* posneg

536

* pp_guard_list g1

537

* pp_guard_list g2; *)

538


539

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

540

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

541

* pp_guard_list gl; *)

542


543

if ok then

544

(gl, e2)::accu, false

545

else (

546

accu, all_invalid

547

)

548

) (accu, all_invalid) gel1

549

) ([], true) gel2

550

in

551

not all_invalid, l

552


553

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

554

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

555

let mk_ge_eq_id ge id =

556

List.map

557

(fun (gl, g_e) >

558

gl,

559

if id = "true" then

560

g_e

561

else

562

match g_e with

563

 Expr g_e >

564

if id = "false" then

565

Expr (Corelang.push_negations ~neg:true g_e)

566

else

567

let loc = g_e.expr_loc in

568

Expr(Corelang.mk_eq loc

569

g_e

570

(Corelang.expr_of_ident id loc))

571

 _ > assert false

572

) ge

573


574

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

575

by its definition.

576

*)

577

let rec rewrite defs expr : elem_guarded_expr list =

578

let rewrite = rewrite defs in

579

let res =

580

match expr.expr_desc with

581

 Expr_appl (id, args, None) >

582

let args = rewrite args in

583

List.map (fun (guards, e) >

584

guards,

585

Expr (Corelang.mkexpr expr.expr_loc (Expr_appl(id, deelem e, None)))

586

) args

587

 Expr_const _ > [[], Expr expr]

588

 Expr_ident id >

589

if Hashtbl.mem defs id then

590

Hashtbl.find defs id

591

else

592

(* id should be an input *)

593

[[], Expr expr]

594

 Expr_ite (g, e1, e2) >

595

let g = rewrite g and

596

e1 = rewrite e1 and

597

e2 = rewrite e2 in

598

let ok_then, g_then = concatenate_ge g true e1 in

599

let ok_else, g_else = concatenate_ge g false e2 in

600

(if ok_then then g_then else [])@

601

(if ok_else then g_else else [])

602

 Expr_merge (g_id, branches) >

603

if Hashtbl.mem defs g_id then

604

let g = Hashtbl.find defs g_id in

605

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

606

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

607

let g = mk_ge_eq_id g id in

608

let e = rewrite e in

609

let ok, g_eq_id = concatenate_ge g true e in

610

if ok then g_eq_id@accu else accu

611

) [] branches

612

else

613

assert false (* g should be defined already *)

614

 Expr_when (e, id, l) >

615

let e = rewrite e in

616

let id_def = Hashtbl.find defs id in

617

let clock = mk_ge_eq_id id_def l in

618

let ok, new_ge = concatenate_ge clock true e in

619

if ok then new_ge else []

620

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

621

 Expr_tuple el >

622

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

623

let gell = List.map rewrite el in

624

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

625

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

626

match gell with

627

 [] > assert false (* Not happening *)

628

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

629

 gel::getl >

630

let getl = aux getl in

631

List.fold_left (

632

fun accu (g,e) >

633

List.fold_left (

634

fun accu (gl, minituple) >

635

let is_compat, guard_comb = combine_guards g gl in

636

if is_compat then

637

let new_gt : elem_boolexpr guard * expr list = (guard_comb, (deelem e)::minituple) in

638

new_gt::accu

639

else

640

accu

641


642

) accu getl

643

) [] gel

644

in

645

let gtuples = aux gell in

646

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

647

List.map

648

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

649

gtuples

650

 Expr_fby _

651

 Expr_appl _

652

(* Should be removed by mormalization and inlining *)

653

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

654

 Expr_array _  Expr_access _  Expr_power _

655

(* Arrays not handled here yet *)

656

> assert false

657

 Expr_pre _ > (* Not rewriting mem assign *)

658

assert false

659

in

660

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

661

* Printers.pp_expr expr

662

* (Utils.fprintf_list ~sep:"@ "

663

* pp_guard_expr) res; *)

664

res

665

and add_def defs vid expr =

666

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

667

* vid

668

* Printers.pp_expr expr; *)

669

let vid_defs = rewrite defs expr in

670

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

671

* (Utils.fprintf_list ~sep:"@ "

672

* (pp_guard_expr pp_elem)) vid_defs; *)

673

(* Format.eprintf "Add_def: %s = %a@. > @[<v 0>%a@]@."

674

* vid

675

* Printers.pp_expr expr

676

* (

677

* (Utils.fprintf_list ~sep:"@ "

678

* pp_guard_expr)) vid_defs; *)

679

Hashtbl.add defs vid vid_defs

680


681

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

682

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.

683


684

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

685

let split_mdefs elem (mdefs: elem_guarded_expr list) =

686

List.fold_left (

687

fun (selected, left_out)

688

((guards, expr) as ge) >

689

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

690

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

691

match sel with

692

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

693

appropriate list *)

694

 [_, sel_status] >

695

if sel_status then

696

(others_guards,expr)::selected, left_out

697

else selected, (others_guards,expr)::left_out

698

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

699

guard_expr in both lists *)

700

ge::selected, ge::left_out

701

 _ > (

702

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

703

pp_elem elem

704

(pp_mdefs pp_elem) mdefs;

705

assert false (* more then one element selected. Should

706

not happen , or trival dead code like if

707

x then if not x then dead code *)

708

)

709

) ([],[]) mdefs

710


711

let split_mem_defs

712

(elem: element)

713

(mem_defs: (ident * elem_guarded_expr list) list)

714

:

715

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

716


717

=

718

List.fold_right (fun (m,mdefs)

719

(accu_pos, accu_neg) >

720

let pos, neg =

721

split_mdefs elem mdefs

722

in

723

(m, pos)::accu_pos,

724

(m, neg)::accu_neg

725

) mem_defs ([],[])

726


727


728

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

729

expressions per memory. *)

730

let split_init mem_defs =

731

split_mem_defs IsInit mem_defs

732


733

(* Previous version of the function: way too costly

734

let pick_guard mem_defs : expr option =

735

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

736

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

737

let all_guards =

738

List.map (

739

(* selecting guards and getting rid of boolean *)

740

fun (e,b) >

741

match e with

742

 Expr e > e

743

 _ > assert false

744

(* should have been filtered out

745

yet *)

746

) gl

747

in

748

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

749

one *)

750

try

751

Some (List.hd all_guards)

752

with _ > None

753

*)

754


755

(* Returning the first non empty guard expression *)

756

let rec pick_guard mem_defs : expr option =

757

match mem_defs with

758

 [] > None

759

 (_, gel)::tl > (

760

let found =

761

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

762

if found = None then

763

match g with

764

 [] > None

765

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

766

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

767

else

768

found

769

) None gel

770

in

771

if found = None then pick_guard tl else found

772

)

773


774


775

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

776

*)

777

let rec build_switch_sys

778

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

779

prefix

780

:

781

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

782

if !seal_debug then

783

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

784

pp_all_defs

785

mem_defs);

786

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

787

mem_defs expr.

788


789

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

790

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

791

status b, *)

792

let res =

793

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

794

(* All defs are unguarded *)

795

match mdefs with

796

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

797

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

798

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

799

 _ > false

800

) mem_defs

801

then

802

[prefix ,

803

List.map (fun (m,gel) >

804

match gel with

805

 [_,e] >

806

let e =

807

match e with

808

 Expr e > e

809

 _ > assert false (* No IsInit expression *)

810

in

811

m,e

812

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

813

 _ > assert false

814

) mem_defs]

815

else

816

(* Picking a guard *)

817

let elem_opt : expr option = pick_guard mem_defs in

818

match elem_opt with

819

None > (

820

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

821

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

822

)

823

 Some elem > (

824

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

825

let pos, neg =

826

split_mem_defs

827

(Expr elem)

828

mem_defs

829

in

830

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

831

match elem.expr_desc with

832

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

833

 Expr_const (Const_tag tag) when tag = Corelang.tag_true

834

> build_switch_sys pos prefix

835

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

836

 Expr_const (Const_tag tag) when tag = Corelang.tag_false

837

> build_switch_sys neg prefix

838

 _ > (* Regular case *)

839

(* let _ = (

840

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

841

* match elem.expr_desc with

842

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

843

*

844

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

845

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

846

* )

847

* in *)

848

let clean l =

849

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

850

let ok, l = check_sat l in

851

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

852

ok, l

853

in

854

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

855

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

856

let ok_pos, pos_prefix = clean pos_prefix in

857

let ok_neg, neg_prefix = clean neg_prefix in

858

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

859

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

860

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

861

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

862

ok_l @ nok_l

863

)

864

in

865

if !seal_debug then (

866

report ~level:4 (fun fmt >

867

Format.fprintf fmt

868

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

869

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

870

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

871

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

872


873

));

874

res

875


876


877


878

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

879

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

880

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

881

let node_as_switched_sys consts (mems:var_decl list) nd =

882

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

883

the call to schedule_node *)

884

let nd_report = Scheduling.schedule_node nd in

885

let schedule = nd_report.Scheduling_type.schedule in

886

let eqs, auts = Corelang.get_node_eqs nd in

887

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

888

let sorted_eqs, unused = Scheduling.sort_equations_from_schedule eqs schedule in

889

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

890

let add_def = add_def defs in

891


892

let vars = Corelang.get_node_vars nd in

893

(* Filtering out unused vars *)

894

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

895

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

896

simplify the expansion *)

897

let _ =

898

List.iter (fun v >

899

let fdecl = Z3.FuncDecl.mk_func_decl_s

900

!ctx

901

v.var_id

902

[]

903

(Zustre_common.type_to_sort v.var_type)

904

in

905

ignore (Zustre_common.register_fdecl v.var_id fdecl)

906

) vars

907

in

908

let _ =

909

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

910

in

911


912


913

(* Registering node equations: identifying mem definitions and

914

storing others in the "defs" hashtbl.

915


916

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

917

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

918

list of guarded assigns. *)

919

let mem_defs, output_defs =

920

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

921

match eq.eq_lhs with

922

 [vid] >

923

(* Only focus on memory definitions *)

924

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

925

(

926

match eq.eq_rhs.expr_desc with

927

 Expr_pre def_m >

928

report ~level:3 (fun fmt >

929

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

930

(vid, rewrite defs def_m)::accu_mems, accu_outputs

931

 _ > assert false

932

)

933

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

934

report ~level:3 (fun fmt >

935

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

936

add_def vid eq.eq_rhs;

937

accu_mems, (vid, rewrite defs eq.eq_rhs)::accu_outputs

938


939

)

940

else

941

(

942

report ~level:3 (fun fmt >

943

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

944

add_def vid eq.eq_rhs;

945

accu_mems, accu_outputs

946

)

947

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

948

) ([], []) sorted_eqs

949

in

950


951


952

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

953

(* Printing memories definitions *)

954

report ~level:3

955

(fun fmt >

956

Format.fprintf fmt

957

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

958

(Utils.fprintf_list ~sep:"@ "

959

(fun fmt (m,mdefs) >

960

Format.fprintf fmt

961

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

962

m

963

(Utils.fprintf_list ~sep:"@ "

964

(pp_guard_expr pp_elem)) mdefs

965

))

966

mem_defs);

967

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

968

let init_defs, update_defs =

969

split_init mem_defs

970

in

971

let init_out, update_out =

972

split_init output_defs

973

in

974

report ~level:3

975

(fun fmt >

976

Format.fprintf fmt

977

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

978

(Utils.fprintf_list ~sep:"@ "

979

(fun fmt (m,mdefs) >

980

Format.fprintf fmt

981

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

982

m

983

(Utils.fprintf_list ~sep:"@ "

984

(pp_guard_expr pp_elem)) mdefs

985

))

986

init_defs);

987

report ~level:3

988

(fun fmt >

989

Format.fprintf fmt

990

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

991

(Utils.fprintf_list ~sep:"@ "

992

(fun fmt (m,mdefs) >

993

Format.fprintf fmt

994

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

995

m

996

(Utils.fprintf_list ~sep:"@ "

997

(pp_guard_expr pp_elem)) mdefs

998

))

999

update_defs);

1000

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

1001

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

1002

let sw_init=

1003

build_switch_sys init_defs []

1004

in

1005

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

1006

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

1007

let sw_sys =

1008

build_switch_sys update_defs []

1009

in

1010


1011

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

1012

let init_out =

1013

build_switch_sys init_out []

1014

in

1015

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

1016


1017

let update_out =

1018

build_switch_sys update_out []

1019

in

1020


1021

let sw_init = clean_sys sw_init in

1022

let sw_sys = clean_sys sw_sys in

1023

let init_out = clean_sys init_out in

1024

let update_out = clean_sys update_out in

1025


1026

(* Some additional checks *)

1027


1028

if false then

1029

begin

1030

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

1031

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

1032


1033

let sw_sys =

1034

List.map (fun (gl, up) >

1035

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

1036

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

1037

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

1038

Printers.pp_expr e

1039

Printers.pp_expr e'

1040

);

1041

res

1042

) gl in

1043

gl, up

1044

) sw_sys

1045

in

1046

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

1047

List.iter (fun (gl, _) >

1048

let rec aux hd l =

1049

match l with

1050

[] > ()

1051

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

1052

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

1053

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

1054

Printers.pp_expr e

1055

Printers.pp_expr e'

1056

)) others;

1057

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

1058

in

1059

aux [] gl

1060

) sw_sys;

1061

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

1062

let rec check_dup_up accu l =

1063

match l with

1064

 [] > ()

1065

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

1066

let others = accu@tl in

1067

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

1068

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

1069


1070

pp_gl_short gl

1071

pp_up up

1072

pp_gl_short gl'

1073

pp_up up'

1074


1075

) others;

1076


1077


1078


1079

check_dup_up (hd::accu) tl

1080


1081

in

1082

check_dup_up [] sw_sys;

1083

let sw_sys =

1084

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

1085

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

1086


1087

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

1088

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

1089

pp_gl_short gl1 pp_gl_short gl2

1090

;

1091

res

1092


1093

) sw_sys

1094


1095

in

1096

()

1097

end;

1098


1099


1100

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

1101

let process sys =

1102

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

1103

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

1104

disjunctive guards. Each set represents a conjunction of

1105

expressions. *)

1106

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

1107

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

1108

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

1109

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

1110


1111

(* We perform multiple pass to avoid errors *)

1112

let map =

1113

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

1114

(* creating a new set to describe gl *)

1115

let new_set =

1116

List.fold_left

1117

(fun set g > Guards.add g set)

1118

Guards.empty

1119

gl

1120

in

1121

(* updating the map with up > new_set *)

1122

if UpMap.mem up map then

1123

let guard_set = UpMap.find up map in

1124

UpMap.add up (new_set::guard_set) map

1125

else

1126

UpMap.add up [new_set] map

1127

) UpMap.empty sys

1128

in

1129

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

1130

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

1131

list of set of guards *)

1132

let map =

1133

UpMap.map (

1134

fun guards >

1135

match guards with

1136

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

1137

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

1138

 hd::tl >

1139

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

1140

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

1141

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

1142

if List.exists Guards.is_empty remaining then

1143

shared, []

1144

else

1145

shared, remaining

1146

) map

1147

in

1148

let rec mk_binop op l = match l with

1149

[] > assert false

1150

 [e] > e

1151

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

1152

in

1153

let gl_as_expr gl =

1154

let gl = Guards.elements gl in

1155

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

1156

match gl with

1157

[] > []

1158

 [e] > [export e]

1159

 _ >

1160

[mk_binop "&&"

1161

(List.map export gl)]

1162

in

1163

let rec clean_disj disj =

1164

match disj with

1165

 [] > []

1166

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

1167

 _::_::_ > (

1168

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

1169

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

1170

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

1171

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

1172

let or_expr = mk_binop "" elems in

1173

[or_expr]

1174


1175


1176

(* TODO disj*)

1177

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

1178

(* List.fold_left (fun accu s >

1179

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

1180

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

1181

* ) accu (Guards.elements s)

1182

* ) [] disj *)

1183


1184

)

1185

in

1186

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

1187

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

1188

if !seal_debug then

1189

Format.eprintf

1190

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

1191

Guards.pp_short common

1192

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

1193

UpMap.pp up;

1194

let disj = clean_disj disj in

1195

let guard_expr = (gl_as_expr common)@disj in

1196


1197

((match guard_expr with

1198

 [] > None

1199

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

1200

) map []

1201


1202

in

1203


1204


1205


1206

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

1207

let sw_init = process sw_init in

1208

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

1209

let sw_sys = process sw_sys in

1210

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

1211

let init_out = process init_out in

1212

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

1213

let update_out = process update_out in

1214

sw_init , sw_sys, init_out, update_out
