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

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

554

by its definition.

555

*)

556

let rec rewrite defs expr : elem_guarded_expr list =

557

let rewrite = rewrite defs in

558

let res =

559

match expr.expr_desc with

560

 Expr_appl (id, args, None) >

561

let args = rewrite args in

562

List.map (fun (guards, e) >

563

guards,

564

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

565

) args

566

 Expr_const _ > [[], Expr expr]

567

 Expr_ident id >

568

if Hashtbl.mem defs id then

569

Hashtbl.find defs id

570

else

571

(* id should be an input *)

572

[[], Expr expr]

573

 Expr_ite (g, e1, e2) >

574

let g = rewrite g and

575

e1 = rewrite e1 and

576

e2 = rewrite e2 in

577

let ok_then, g_then = concatenate_ge g true e1 in

578

let ok_else, g_else = concatenate_ge g false e2 in

579

(if ok_then then g_then else [])@

580

(if ok_else then g_else else [])

581

 Expr_merge (g, branches) >

582

assert false (* TODO: deal with merges *)

583


584

 Expr_when (e, _, _) > rewrite e

585

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

586

 Expr_tuple el >

587

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

588

let gell = List.map rewrite el in

589

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

590

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

591

match gell with

592

 [] > assert false (* Not happening *)

593

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

594

 gel::getl >

595

let getl = aux getl in

596

List.fold_left (

597

fun accu (g,e) >

598

List.fold_left (

599

fun accu (gl, minituple) >

600

let is_compat, guard_comb = combine_guards g gl in

601

if is_compat then

602

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

603

new_gt::accu

604

else

605

accu

606


607

) accu getl

608

) [] gel

609

in

610

let gtuples = aux gell in

611

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

612

List.map

613

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

614

gtuples

615

 Expr_fby _

616

 Expr_appl _

617

(* Should be removed by mormalization and inlining *)

618

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

619

 Expr_array _  Expr_access _  Expr_power _

620

(* Arrays not handled here yet *)

621

> assert false

622

 Expr_pre _ > (* Not rewriting mem assign *)

623

assert false

624

in

625

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

626

* Printers.pp_expr expr

627

* (Utils.fprintf_list ~sep:"@ "

628

* pp_guard_expr) res; *)

629

res

630

and add_def defs vid expr =

631

let vid_defs = rewrite defs expr in

632

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

633

* vid

634

* Printers.pp_expr expr

635

* (

636

* (Utils.fprintf_list ~sep:"@ "

637

* pp_guard_expr)) vid_defs; *)

638

Hashtbl.add defs vid vid_defs

639


640

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

641

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.

642


643

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

644

let split_mdefs elem (mdefs: elem_guarded_expr list) =

645

List.fold_left (

646

fun (selected, left_out)

647

((guards, expr) as ge) >

648

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

649

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

650

match sel with

651

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

652

appropriate list *)

653

 [_, sel_status] >

654

if sel_status then

655

(others_guards,expr)::selected, left_out

656

else selected, (others_guards,expr)::left_out

657

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

658

guard_expr in both lists *)

659

ge::selected, ge::left_out

660

 _ > (

661

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

662

pp_elem elem

663

(pp_mdefs pp_elem) mdefs;

664

assert false (* more then one element selected. Should

665

not happen , or trival dead code like if

666

x then if not x then dead code *)

667

)

668

) ([],[]) mdefs

669


670

let split_mem_defs

671

(elem: element)

672

(mem_defs: (ident * elem_guarded_expr list) list)

673

:

674

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

675


676

=

677

List.fold_right (fun (m,mdefs)

678

(accu_pos, accu_neg) >

679

let pos, neg =

680

split_mdefs elem mdefs

681

in

682

(m, pos)::accu_pos,

683

(m, neg)::accu_neg

684

) mem_defs ([],[])

685


686


687

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

688

expressions per memory. *)

689

let split_init mem_defs =

690

split_mem_defs IsInit mem_defs

691


692

(* Previous version of the function: way too costly

693

let pick_guard mem_defs : expr option =

694

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

695

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

696

let all_guards =

697

List.map (

698

(* selecting guards and getting rid of boolean *)

699

fun (e,b) >

700

match e with

701

 Expr e > e

702

 _ > assert false

703

(* should have been filtered out

704

yet *)

705

) gl

706

in

707

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

708

one *)

709

try

710

Some (List.hd all_guards)

711

with _ > None

712

*)

713


714

(* Returning the first non empty guard expression *)

715

let rec pick_guard mem_defs : expr option =

716

match mem_defs with

717

 [] > None

718

 (_, gel)::tl > (

719

let found =

720

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

721

if found = None then

722

match g with

723

 [] > None

724

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

725

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

726

else

727

found

728

) None gel

729

in

730

if found = None then pick_guard tl else found

731

)

732


733


734

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

735

*)

736

let rec build_switch_sys

737

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

738

prefix

739

:

740

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

741

if !seal_debug then

742

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

743

(Utils.fprintf_list ~sep:",@ "

744

(fun fmt (id, gel) > Format.fprintf fmt "%s > [@[<v 0>%a]@]"

745

id

746

(pp_mdefs pp_elem) gel))

747

mem_defs);

748

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

749

mem_defs expr.

750


751

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

752

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

753

status b, *)

754

let res =

755

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

756

(* All defs are unguarded *)

757

match mdefs with

758

 [[], _] > true

759

 _ > false

760

) mem_defs

761

then

762

[prefix ,

763

List.map (fun (m,gel) >

764

match gel with

765

 [_,e] >

766

let e =

767

match e with

768

 Expr e > e

769

 _ > assert false (* No IsInit expression *)

770

in

771

m,e

772

 _ > assert false

773

) mem_defs]

774

else

775

(* Picking a guard *)

776

let elem_opt : expr option = pick_guard mem_defs in

777

match elem_opt with

778

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

779

 Some elem > (

780

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

781

let pos, neg =

782

split_mem_defs

783

(Expr elem)

784

mem_defs

785

in

786

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

787

match elem.expr_desc with

788

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

789

 Expr_const (Const_tag tag) when tag = Corelang.tag_true

790

> build_switch_sys pos prefix

791

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

792

 Expr_const (Const_tag tag) when tag = Corelang.tag_false

793

> build_switch_sys neg prefix

794

 _ > (* Regular case *)

795

(* let _ = (

796

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

797

* match elem.expr_desc with

798

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

799

*

800

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

801

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

802

* )

803

* in *)

804

let clean l =

805

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

806

let ok, l = check_sat l in

807

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

808

ok, l

809

in

810

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

811

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

812

let ok_pos, pos_prefix = clean pos_prefix in

813

let ok_neg, neg_prefix = clean neg_prefix in

814

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

815

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

816

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

817

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

818

ok_l @ nok_l

819

)

820

in

821

if !seal_debug then (

822

report ~level:4 (fun fmt >

823

Format.fprintf fmt

824

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

825

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

826

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

827

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

828


829

));

830

res

831


832


833


834

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

835

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

836

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

837

let node_as_switched_sys consts (mems:var_decl list) nd =

838

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

839

the call to schedule_node *)

840

let nd_report = Scheduling.schedule_node nd in

841

let schedule = nd_report.Scheduling_type.schedule in

842

let eqs, auts = Corelang.get_node_eqs nd in

843

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

844

let sorted_eqs, unused = Scheduling.sort_equations_from_schedule eqs schedule in

845

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

846

let add_def = add_def defs in

847


848

let vars = Corelang.get_node_vars nd in

849

(* Filtering out unused vars *)

850

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

851

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

852

simplify the expansion *)

853

let _ =

854

List.iter (fun v >

855

let fdecl = Z3.FuncDecl.mk_func_decl_s

856

!ctx

857

v.var_id

858

[]

859

(Zustre_common.type_to_sort v.var_type)

860

in

861

ignore (Zustre_common.register_fdecl v.var_id fdecl)

862

) vars

863

in

864

let _ =

865

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

866

in

867


868


869

(* Registering node equations: identifying mem definitions and

870

storing others in the "defs" hashtbl.

871


872

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

873

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

874

list of guarded assigns. *)

875

let mem_defs, output_defs =

876

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

877

match eq.eq_lhs with

878

 [vid] >

879

(* Only focus on memory definitions *)

880

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

881

(

882

match eq.eq_rhs.expr_desc with

883

 Expr_pre def_m >

884

report ~level:3 (fun fmt >

885

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

886

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

887

 _ > assert false

888

)

889

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

890

report ~level:3 (fun fmt >

891

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

892

add_def vid eq.eq_rhs;

893

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

894


895

)

896

else

897

(

898

report ~level:3 (fun fmt >

899

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

900

add_def vid eq.eq_rhs;

901

accu_mems, accu_outputs

902

)

903

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

904

) ([], []) sorted_eqs

905

in

906


907


908

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

909

(* Printing memories definitions *)

910

report ~level:3

911

(fun fmt >

912

Format.fprintf fmt

913

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

914

(Utils.fprintf_list ~sep:"@ "

915

(fun fmt (m,mdefs) >

916

Format.fprintf fmt

917

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

918

m

919

(Utils.fprintf_list ~sep:"@ "

920

(pp_guard_expr pp_elem)) mdefs

921

))

922

mem_defs);

923

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

924

let init_defs, update_defs =

925

split_init mem_defs

926

in

927

let init_out, update_out =

928

split_init output_defs

929

in

930

report ~level:3

931

(fun fmt >

932

Format.fprintf fmt

933

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

934

(Utils.fprintf_list ~sep:"@ "

935

(fun fmt (m,mdefs) >

936

Format.fprintf fmt

937

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

938

m

939

(Utils.fprintf_list ~sep:"@ "

940

(pp_guard_expr pp_elem)) mdefs

941

))

942

init_defs);

943

report ~level:3

944

(fun fmt >

945

Format.fprintf fmt

946

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

947

(Utils.fprintf_list ~sep:"@ "

948

(fun fmt (m,mdefs) >

949

Format.fprintf fmt

950

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

951

m

952

(Utils.fprintf_list ~sep:"@ "

953

(pp_guard_expr pp_elem)) mdefs

954

))

955

update_defs);

956

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

957

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

958

let sw_init=

959

build_switch_sys init_defs []

960

in

961

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

962

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

963

let sw_sys =

964

build_switch_sys update_defs []

965

in

966


967

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

968

let init_out =

969

build_switch_sys init_out []

970

in

971

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

972


973

let update_out =

974

build_switch_sys update_out []

975

in

976


977

let sw_init = clean_sys sw_init in

978

let sw_sys = clean_sys sw_sys in

979

let init_out = clean_sys init_out in

980

let update_out = clean_sys update_out in

981


982

(* Some additional checks *)

983


984

if false then

985

begin

986

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

987

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

988


989

let sw_sys =

990

List.map (fun (gl, up) >

991

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

992

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

993

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

994

Printers.pp_expr e

995

Printers.pp_expr e'

996

);

997

res

998

) gl in

999

gl, up

1000

) sw_sys

1001

in

1002

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

1003

List.iter (fun (gl, _) >

1004

let rec aux hd l =

1005

match l with

1006

[] > ()

1007

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

1008

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

1009

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

1010

Printers.pp_expr e

1011

Printers.pp_expr e'

1012

)) others;

1013

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

1014

in

1015

aux [] gl

1016

) sw_sys;

1017

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

1018

let rec check_dup_up accu l =

1019

match l with

1020

 [] > ()

1021

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

1022

let others = accu@tl in

1023

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

1024

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

1025


1026

pp_gl_short gl

1027

pp_up up

1028

pp_gl_short gl'

1029

pp_up up'

1030


1031

) others;

1032


1033


1034


1035

check_dup_up (hd::accu) tl

1036


1037

in

1038

check_dup_up [] sw_sys;

1039

let sw_sys =

1040

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

1041

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

1042


1043

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

1044

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

1045

pp_gl_short gl1 pp_gl_short gl2

1046

;

1047

res

1048


1049

) sw_sys

1050


1051

in

1052

()

1053

end;

1054


1055


1056

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

1057

let process sys =

1058

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

1059

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

1060

disjunctive guards. Each set represents a conjunction of

1061

expressions. *)

1062

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

1063

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

1064

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

1065

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

1066


1067

(* We perform multiple pass to avoid errors *)

1068

let map =

1069

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

1070

(* creating a new set to describe gl *)

1071

let new_set =

1072

List.fold_left

1073

(fun set g > Guards.add g set)

1074

Guards.empty

1075

gl

1076

in

1077

(* updating the map with up > new_set *)

1078

if UpMap.mem up map then

1079

let guard_set = UpMap.find up map in

1080

UpMap.add up (new_set::guard_set) map

1081

else

1082

UpMap.add up [new_set] map

1083

) UpMap.empty sys

1084

in

1085

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

1086

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

1087

list of set of guards *)

1088

let map =

1089

UpMap.map (

1090

fun guards >

1091

match guards with

1092

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

1093

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

1094

 hd::tl >

1095

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

1096

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

1097

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

1098

if List.exists Guards.is_empty remaining then

1099

shared, []

1100

else

1101

shared, remaining

1102

) map

1103

in

1104

let rec mk_binop op l = match l with

1105

[] > assert false

1106

 [e] > e

1107

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

1108

in

1109

let gl_as_expr gl =

1110

let gl = Guards.elements gl in

1111

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

1112

match gl with

1113

[] > []

1114

 [e] > [export e]

1115

 _ >

1116

[mk_binop "&&"

1117

(List.map export gl)]

1118

in

1119

let rec clean_disj disj =

1120

match disj with

1121

 [] > []

1122

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

1123

 _::_::_ > (

1124

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

1125

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

1126

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

1127

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

1128

let or_expr = mk_binop "" elems in

1129

[or_expr]

1130


1131


1132

(* TODO disj*)

1133

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

1134

(* List.fold_left (fun accu s >

1135

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

1136

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

1137

* ) accu (Guards.elements s)

1138

* ) [] disj *)

1139


1140

)

1141

in

1142

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

1143

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

1144

if !seal_debug then

1145

Format.eprintf

1146

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

1147

Guards.pp_short common

1148

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

1149

UpMap.pp up;

1150

let disj = clean_disj disj in

1151

let guard_expr = (gl_as_expr common)@disj in

1152


1153

((match guard_expr with

1154

 [] > None

1155

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

1156

) map []

1157


1158

in

1159


1160


1161


1162

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

1163

let sw_init = process sw_init in

1164

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

1165

let sw_sys = process sw_sys in

1166

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

1167

let init_out = process init_out in

1168

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

1169

let update_out = process update_out in

1170

sw_init , sw_sys, init_out, update_out
