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

type element = IsInit  Expr of expr

11


12

type guard = (element * bool) list

13

type guarded_expr = guard * element

14

type mdef_t = guarded_expr list

15


16

let pp_elem fmt e =

17

match e with

18

 IsInit > Format.fprintf fmt "init"

19

 Expr e > Format.fprintf fmt "%a" Printers.pp_expr e

20


21

let pp_guard_list fmt gl =

22

(fprintf_list ~sep:"; "

23

(fun fmt (e,b) > if b then pp_elem fmt e else Format.fprintf fmt "not(%a)" pp_elem e)) fmt gl

24


25

let pp_guard_expr fmt (gl,e) =

26

Format.fprintf fmt "%a > %a"

27

pp_guard_list gl

28

pp_elem e

29


30

let pp_mdefs fmt gel = fprintf_list ~sep:"@ " pp_guard_expr fmt gel

31


32


33

let add_init defs vid =

34

Hashtbl.add defs vid [[], IsInit]

35


36

let deelem e = match e with

37

Expr e > e

38

 IsInit > assert false (* Wasn't expecting isinit here: we are building values! *)

39


40

let is_eq_elem elem elem' =

41

match elem, elem' with

42

 IsInit, IsInit > true

43

 Expr e, Expr e' > e = e' (*

44

Corelang.is_eq_expr e e' *)

45

 _ > false

46


47

let select_elem elem (gelem, _) =

48

is_eq_elem elem gelem

49


50


51

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

52

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

53

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

54

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

55


56

let is_init_name = "__is_init"

57


58

let const_defs = Hashtbl.create 13

59

let is_const id = Hashtbl.mem const_defs id

60

let get_const id = Hashtbl.find const_defs id

61


62

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

63

arrows, fby, ... *)

64


65

(* Set of hash to support memoization *)

66

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

67

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

68

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

69

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

70

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

71

let pp_ze_hash fmt = pp_hash

72

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

73

Format.pp_print_int

74

fmt

75

ze_hash

76

let pp_e_hash fmt = pp_hash

77

Format.pp_print_int

78

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

79

fmt

80

e_hash

81

let mem_expr e =

82

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

83

* Printers.pp_expr e

84

* pp_e_map; *)

85

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

86

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

87

res

88


89

let mem_zexpr ze =

90

Hashtbl.mem ze_hash ze

91

let get_zexpr e =

92

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

93

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

94

Hashtbl.find e_hash uid

95

let get_expr ze =

96

let uid = Hashtbl.find ze_hash ze in

97

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

98

e

99


100

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

101

let is_init_z3e =

102

Z3.Expr.mk_const_s !ctx is_init_name Zustre_common.bool_sort

103


104

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

105

try

106

if Z3.Expr.equal ze is_init_z3e then 1 else

107

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

108

Hashtbl.find ze_hash ze

109

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

110

(Z3.Expr.to_string ze)

111

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

112

assert false)

113

let add_expr =

114

let cpt = ref 0 in

115

fun e ze >

116

incr cpt;

117

let uid = !cpt in

118

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

119

Hashtbl.add e_hash uid ze;

120

Hashtbl.add ze_hash ze uid

121


122


123

let expr_to_z3_expr, zexpr_to_expr =

124

(* List to store converted expression. *)

125

(* let hash = ref [] in

126

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

127

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

128


129

let rec e2ze e =

130

if mem_expr e then (

131

get_zexpr e

132

)

133

else (

134

let res =

135

match e.expr_desc with

136

 Expr_const c >

137

let z3e = Zustre_common.horn_const_to_expr c in

138

add_expr e z3e;

139

z3e

140

 Expr_ident id > (

141

if is_const id then (

142

let c = get_const id in

143

let z3e = Zustre_common.horn_const_to_expr c in

144

add_expr e z3e;

145

z3e

146

)

147

else (

148

let fdecl_id = Zustre_common.get_fdecl id in

149

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

150

add_expr e z3e;

151

z3e

152

)

153

)

154

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

155

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

156

add_expr e z3e;

157

z3e

158

 Expr_tuple [e] >

159

let z3e = e2ze e in

160

add_expr e z3e;

161

z3e

162

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

163

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

164

; assert false

165

in

166

res

167

)

168

in

169

let rec ze2e ze =

170

let ze_name ze =

171

let fd = Z3.Expr.get_func_decl ze in

172

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

173

in

174

if mem_zexpr ze then

175

None, Some (get_expr ze)

176

else

177

let open Corelang in

178

let fd = Z3.Expr.get_func_decl ze in

179

let zel = Z3.Expr.get_args ze in

180

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

181

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

182


183

(* Extracting IsInit status *)

184

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

185

Some false, None

186

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

187

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

188

 op, _ > (

189


190


191

if Z3.Expr.is_numeral ze then

192

let e =

193

if Z3.Arithmetic.is_real ze then

194

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

195

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

196

mkexpr

197

Location.dummy_loc

198

(Expr_const

199

(Const_real

200

(num, 0, s)))

201

else if Z3.Arithmetic.is_int ze then

202

mkexpr

203

Location.dummy_loc

204

(Expr_const

205

(Const_int

206

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

207

else if Z3.Expr.is_const ze then

208

match Z3.Expr.to_string ze with

209

 "true" > mkexpr Location.dummy_loc

210

(Expr_const (Const_tag (tag_true)))

211

 "false" >

212

mkexpr Location.dummy_loc

213

(Expr_const (Const_tag (tag_false)))

214

 _ > assert false

215

else

216

(

217

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

218

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

219

)

220

in

221

None, Some e

222

else

223

match op with

224

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

225

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

226

>

227

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

228

None, Some (mkpredef_call Location.dummy_loc op args)

229

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

230

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

231

let e = match args with

232

[] > assert false

233

 [hd] > hd

234

 e1::e2::tl >

235

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

236

if tl = [] then first_binary_and else

237

List.fold_left (fun e e_new >

238

mkpredef_call Location.dummy_loc op [e;e_new]

239

) first_binary_and tl

240


241

in

242

None, Some e

243

)

244

 "and"  "or" > (

245

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

246

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

247

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

248

match args with

249

 [] > assert false

250

 [hd] > hd

251

 hd::tl >

252

List.fold_left

253

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

254

(match is_init_opt1, is_init_opt2 with

255

None, x  x, None > x

256

 Some _, Some _ > assert false),

257

(match expr_opt1, expr_opt2 with

258

 None, x  x, None > x

259

 Some e1, Some e2 >

260

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

261

))

262

hd tl

263

)

264

 op >

265

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

266

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

267

)

268

in

269

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

270


271


272

let zexpr_to_guard_list ze =

273

let init_opt, expr_opt = zexpr_to_expr ze in

274

(match init_opt with

275

 None > []

276

Some b > [IsInit, b]

277

) @ (match expr_opt with

278

 None > []

279

 Some e > [Expr e, true]

280

)

281


282


283

let simplify_neg_guard l =

284

List.map (fun (g,posneg) >

285

match g with

286

 IsInit > g, posneg

287

 Expr g >

288

if posneg then

289

Expr (Corelang.push_negations g),

290

true

291

else

292

(* Pushing the negation in the expression *)

293

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

294

true

295

) l

296


297

(* TODO:

298

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

299

*)

300

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

301

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

302

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

303

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

304

(*

305

let goal_simplify zl =

306

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

307

Z3.Goal.add goal zl;

308

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

309

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

310

* (Z3.Goal.to_string goal)

311

* (Z3.Goal.to_string goal')

312

* (Z3.Solver.string_of_status status_res)

313

* ; *)

314

let ze = Z3.Goal.as_expr goal' in

315

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

316

zexpr_to_guard_list ze

317

*)

318


319

let implies =

320

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

321

fun ze1 ze2 >

322

let ze1_uid = get_zid ze1 in

323

let ze2_uid = get_zid ze2 in

324

if Hashtbl.mem ze_implies_hash (ze1_uid, ze2_uid) then

325

Hashtbl.find ze_implies_hash (ze1_uid, ze2_uid)

326

else

327

begin

328

if !debug then (

329

Format.eprintf "Checking implication: %s => %s? "

330

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

331

);

332

let solver = Z3.Solver.mk_simple_solver !ctx in

333

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

334

let res =

335

try

336

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

337

match status_res with

338

 Z3.Solver.UNSATISFIABLE > if !debug then Format.eprintf "Valid!@.";

339

true

340

 _ > if !debug then Format.eprintf "not proved valid@.";

341

false

342

with Zustre_common.UnknownFunction(id, msg) > (

343

report ~level:1 msg;

344

false

345

)

346

in

347

Hashtbl.add ze_implies_hash (ze1_uid,ze2_uid) res ;

348

res

349

end

350


351

let rec simplify zl =

352

match zl with

353

 []  [_] > zl

354

 hd::tl > (

355

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

356

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

357

let tl = simplify tl in

358

let keep_hd, tl =

359

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

360

if implies hd e then

361

true, accu (* throwing away e *)

362

else if implies e hd then

363

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

364

else

365

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

366

) (true,[]) tl

367

in

368

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

369

* keep_hd

370

* (Z3.Expr.to_string hd)

371

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

372

* ; *)

373

if keep_hd then

374

hd::tl

375

else

376

tl

377

)

378


379

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

380

(* Syntactic simplification *)

381

if false then

382

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

383

let l = simplify_neg_guard l in

384

if false then (

385

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

386

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

387

);

388

let solver = Z3.Solver.mk_simple_solver !ctx in

389

try (

390

let zl =

391

List.map (fun (e, posneg) >

392

let ze =

393

match e with

394

 IsInit > is_init_z3e

395

 Expr e > expr_to_z3_expr e

396

in

397

if posneg then

398

ze

399

else

400

neg_ze ze

401

) l

402

in

403

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

404

let zl = simplify zl in

405

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

406

let status_res = Z3.Solver.check solver zl in

407

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

408

match status_res with

409

 Z3.Solver.UNSATISFIABLE > false, []

410

 _ > (

411

if false && just_check then

412

true, l

413

else

414

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

415

(* let l = goal_simplify zl in *)

416

let l = List.fold_left

417

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

418

[]

419

zl

420

in

421

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

422

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

423

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

424

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

425


426


427

true, l

428


429


430

)

431


432

)

433

with Zustre_common.UnknownFunction(id, msg) > (

434

report ~level:1 msg;

435

true, l (* keeping everything. *)

436

)

437


438


439


440


441

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

442


443


444

let clean_sys sys =

445

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

446

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

447

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

448

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

449

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

450

sat

451


452

;*)

453

if sat then

454

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

455

else

456

accu

457

)

458

[] sys

459


460

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

461

registered guards are initially produced by the call to

462

combine_guards. We csan normalize the guards to ease the

463

comparisons.

464


465

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

466

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

467

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

468

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

469

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

470

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

471

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

472

rthat elong is somehow reduced with respect to other elements of

473

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

474

not store elong.

475


476

After iterating through llong, we have a shortened version of

477

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

478

them to this new consolidated list.

479


480

*)

481


482

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

483

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

484

version of it. *)

485

let combine_guards ?(fresh=None) gl1 gl2 =

486

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

487

addressed later *)

488

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

489

let ok, _ = check_sat e in

490

ok

491

in

492

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

493

let e2z e pn =

494

match e with

495

 IsInit > if pn then is_init_z3e else neg_ze is_init_z3e

496

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

497

in

498

implies (e2z e1 pn1) (e2z e2 pn2)

499

in

500

let lshort, llong =

501

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

502

in

503

let merge long short =

504

let short, long_sel, ok =

505

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

506

if not ok then

507

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

508

else if check_sat (long_e::short) then

509

let short, keep_long_e =

510

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

511

if not keep_long_e then (* shorten the algo *)

512

eshort_i :: accu_short, false

513

else (* keep_long_e = true in the following *)

514

if implies eshort_i long_e then

515

(* First case is trying to remove long_e!

516


517

Since short is already normalized, we can remove

518

long_e. If later long_e is stronger than another

519

element of short, then necessarily eshort_i =>

520

long_e >

521

that_other_element_of_short. Contradiction. *)

522

eshort_i::accu_short, false

523

else if implies long_e eshort_i then

524

(* removing eshort_i, keeping long_e. *)

525

accu_short, true

526

else (* Not comparable, keeping both *)

527

eshort_i::accu_short, true

528

)

529

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

530

short

531

in

532

if keep_long_e then

533

short, long_e::long_sel, true

534

else

535

short, long_sel, true

536

else

537

[],[],false

538

) (short, [], true) long

539

in

540

ok, long_sel@short

541

in

542

let ok, l = match fresh with

543

 None > true, []

544

 Some g > merge [g] []

545

in

546

if not ok then

547

false, []

548

else

549

let ok, lshort = merge lshort l in

550

if not ok then

551

false, []

552

else

553

merge llong lshort

554


555


556

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

557

 Compute the combination of guarded exprs in gel1 and gel2:

558

 Each guarded_expr in gel1 is transformed as a guard: the

559

expression is associated to posneg.

560

 Existing guards in gel2 are concatenated to that list of guards

561

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

562

*)

563

let concatenate_ge gel1 posneg gel2 =

564

let l, all_invalid =

565

List.fold_left (

566

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

567

List.fold_left (

568

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

569

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

570

* pp_elem e1

571

* posneg

572

* pp_guard_list g1

573

* pp_guard_list g2; *)

574


575

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

576

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

577

* pp_guard_list gl; *)

578


579

if ok then

580

(gl, e2)::accu, false

581

else (

582

accu, all_invalid

583

)

584

) (accu, all_invalid) gel1

585

) ([], true) gel2

586

in

587

not all_invalid, l

588


589

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

590

by its definition.

591

*)

592

let rec rewrite defs expr : guarded_expr list =

593

let rewrite = rewrite defs in

594

let res =

595

match expr.expr_desc with

596

 Expr_appl (id, args, None) >

597

let args = rewrite args in

598

List.map (fun (guards, e) >

599

guards,

600

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

601

) args

602

 Expr_const _ > [[], Expr expr]

603

 Expr_ident id >

604

if Hashtbl.mem defs id then

605

Hashtbl.find defs id

606

else

607

(* id should be an input *)

608

[[], Expr expr]

609

 Expr_ite (g, e1, e2) >

610

let g = rewrite g and

611

e1 = rewrite e1 and

612

e2 = rewrite e2 in

613

let ok_then, g_then = concatenate_ge g true e1 in

614

let ok_else, g_else = concatenate_ge g false e2 in

615

(if ok_then then g_then else [])@

616

(if ok_else then g_else else [])

617

 Expr_merge (g, branches) >

618

assert false (* TODO: deal with merges *)

619


620

 Expr_when (e, _, _) > rewrite e

621

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

622

 Expr_tuple el >

623

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

624

let gell = List.map rewrite el in

625

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

626

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

627

match gell with

628

 [] > assert false (* Not happening *)

629

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

630

 gel::getl >

631

let getl = aux getl in

632

List.fold_left (

633

fun accu (g,e) >

634

List.fold_left (

635

fun accu (gl, minituple) >

636

let is_compat, guard_comb = combine_guards g gl in

637

if is_compat then

638

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

639

new_gt::accu

640

else

641

accu

642


643

) accu getl

644

) [] gel

645

in

646

let gtuples = aux gell in

647

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

648

List.map

649

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

650

gtuples

651

 Expr_fby _

652

 Expr_appl _

653

(* Should be removed by mormalization and inlining *)

654

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

655

 Expr_array _  Expr_access _  Expr_power _

656

(* Arrays not handled here yet *)

657

> assert false

658

 Expr_pre _ > (* Not rewriting mem assign *)

659

assert false

660

in

661

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

662

* Printers.pp_expr expr

663

* (Utils.fprintf_list ~sep:"@ "

664

* pp_guard_expr) res; *)

665

res

666

and add_def defs vid expr =

667

let vid_defs = rewrite defs expr in

668

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

669

* vid

670

* Printers.pp_expr expr

671

* (

672

* (Utils.fprintf_list ~sep:"@ "

673

* pp_guard_expr)) vid_defs; *)

674

Hashtbl.add defs vid vid_defs

675


676

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

677

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.

678


679

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

680

let split_mdefs elem (mdefs: guarded_expr list) =

681

List.fold_left (

682

fun (selected, left_out)

683

((guards, expr) as ge) >

684

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

685

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

686

match sel with

687

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

688

appropriate list *)

689

 [_, sel_status] >

690

if sel_status then

691

(others_guards,expr)::selected, left_out

692

else selected, (others_guards,expr)::left_out

693

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

694

guard_expr in both lists *)

695

ge::selected, ge::left_out

696

 _ > (

697

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

698

pp_elem elem

699

pp_mdefs mdefs;

700

assert false (* more then one element selected. Should

701

not happen , or trival dead code like if

702

x then if not x then dead code *)

703

)

704

) ([],[]) mdefs

705


706

let split_mem_defs

707

(elem: element)

708

(mem_defs: (ident * guarded_expr list) list)

709

:

710

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

711


712

=

713

List.fold_right (fun (m,mdefs)

714

(accu_pos, accu_neg) >

715

let pos, neg =

716

split_mdefs elem mdefs

717

in

718

(m, pos)::accu_pos,

719

(m, neg)::accu_neg

720

) mem_defs ([],[])

721


722


723

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

724

expressions per memory. *)

725

let split_init mem_defs =

726

split_mem_defs IsInit mem_defs

727


728

(* Previous version of the function: way too costly

729

let pick_guard mem_defs : expr option =

730

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

731

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

732

let all_guards =

733

List.map (

734

(* selecting guards and getting rid of boolean *)

735

fun (e,b) >

736

match e with

737

 Expr e > e

738

 _ > assert false

739

(* should have been filtered out

740

yet *)

741

) gl

742

in

743

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

744

one *)

745

try

746

Some (List.hd all_guards)

747

with _ > None

748

*)

749


750

(* Returning the first non empty guard expression *)

751

let rec pick_guard mem_defs : expr option =

752

match mem_defs with

753

 [] > None

754

 (_, gel)::tl > (

755

let found =

756

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

757

if found = None then

758

match g with

759

 [] > None

760

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

761

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

762

else

763

found

764

) None gel

765

in

766

if found = None then pick_guard tl else found

767

)

768


769


770

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

771

*)

772

let rec build_switch_sys

773

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

774

prefix

775

:

776

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

777

if !debug then

778

Format.eprintf "Build_switch with %a@."

779

(Utils.fprintf_list ~sep:",@ "

780

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

781

id

782

pp_mdefs gel))

783

mem_defs;

784

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

785

mem_defs expr.

786


787

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

788

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

789

status b, *)

790

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

791

(* All defs are unguarded *)

792

match mdefs with

793

 [[], _] > true

794

 _ > false

795

) mem_defs

796

then

797

[prefix ,

798

List.map (fun (m,gel) >

799

match gel with

800

 [_,e] >

801

let e =

802

match e with

803

 Expr e > e

804

 _ > assert false (* No IsInit expression *)

805

in

806

m,e

807

 _ > assert false

808

) mem_defs]

809

else

810

(* Picking a guard *)

811

let elem_opt : expr option = pick_guard mem_defs in

812

match elem_opt with

813

None > []

814

 Some elem > (

815

let pos, neg =

816

split_mem_defs

817

(Expr elem)

818

mem_defs

819

in

820

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

821

match elem.expr_desc with

822

 Expr_ident "true" > build_switch_sys pos prefix

823

 Expr_const (Const_tag tag) when tag = Corelang.tag_true

824

> build_switch_sys pos prefix

825

 Expr_ident "false" > build_switch_sys neg prefix

826

 Expr_const (Const_tag tag) when tag = Corelang.tag_false

827

> build_switch_sys neg prefix

828

 _ > (* Regular case *)

829

(* let _ = (

830

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

831

* match elem.expr_desc with

832

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

833

*

834

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

835

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

836

* )

837

* in *)

838

let clean l =

839

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

840

let ok, l = check_sat l in

841

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

842

ok, l

843

in

844

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

845

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

846

let ok_pos, pos_prefix = clean pos_prefix in

847

let ok_neg, neg_prefix = clean neg_prefix in

848

(if ok_pos then build_switch_sys pos pos_prefix else [])

849

@

850

(if ok_neg then build_switch_sys neg neg_prefix else [])

851

)

852


853


854


855

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

856

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

857

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

858

let node_as_switched_sys consts (mems:var_decl list) nd =

859

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

860

the call to schedule_node *)

861

let nd_report = Scheduling.schedule_node nd in

862

let schedule = nd_report.Scheduling_type.schedule in

863

let eqs, auts = Corelang.get_node_eqs nd in

864

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

865

let sorted_eqs = Scheduling.sort_equations_from_schedule eqs schedule in

866

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

867

let add_def = add_def defs in

868


869

let vars = Corelang.get_node_vars nd in

870

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

871

simplify the expansion *)

872

let _ =

873

List.iter (fun v >

874

let fdecl = Z3.FuncDecl.mk_func_decl_s

875

!ctx

876

v.var_id

877

[]

878

(Zustre_common.type_to_sort v.var_type)

879

in

880

ignore (Zustre_common.register_fdecl v.var_id fdecl)

881

) vars

882

in

883

let _ =

884

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

885

in

886


887


888

(* Registering node equations: identifying mem definitions and

889

storing others in the "defs" hashtbl.

890


891

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

892

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

893

list of guarded assigns. *)

894

let mem_defs, output_defs =

895

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

896

match eq.eq_lhs with

897

 [vid] >

898

(* Only focus on memory definitions *)

899

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

900

(

901

match eq.eq_rhs.expr_desc with

902

 Expr_pre def_m >

903

report ~level:3 (fun fmt >

904

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

905

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

906

 _ > assert false

907

)

908

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

909

report ~level:3 (fun fmt >

910

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

911

add_def vid eq.eq_rhs;

912

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

913


914

)

915

else

916

(

917

report ~level:3 (fun fmt >

918

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

919

add_def vid eq.eq_rhs;

920

accu_mems, accu_outputs

921

)

922

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

923

) ([], []) sorted_eqs

924

in

925


926


927

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

928

(* Printing memories definitions *)

929

report ~level:3

930

(fun fmt >

931

Format.fprintf fmt

932

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

933

(Utils.fprintf_list ~sep:"@ "

934

(fun fmt (m,mdefs) >

935

Format.fprintf fmt

936

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

937

m

938

(Utils.fprintf_list ~sep:"@ "

939

pp_guard_expr) mdefs

940

))

941

mem_defs);

942

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

943

let init_defs, update_defs =

944

split_init mem_defs

945

in

946

let init_out, update_out =

947

split_init output_defs

948

in

949

report ~level:3

950

(fun fmt >

951

Format.fprintf fmt

952

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

953

(Utils.fprintf_list ~sep:"@ "

954

(fun fmt (m,mdefs) >

955

Format.fprintf fmt

956

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

957

m

958

(Utils.fprintf_list ~sep:"@ "

959

pp_guard_expr) mdefs

960

))

961

init_defs

962

(Utils.fprintf_list ~sep:"@ "

963

(fun fmt (m,mdefs) >

964

Format.fprintf fmt

965

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

966

m

967

(Utils.fprintf_list ~sep:"@ "

968

pp_guard_expr) mdefs

969

))

970

update_defs);

971

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

972


973

let sw_init=

974

build_switch_sys init_defs []

975

in

976

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

977

let sw_sys =

978

build_switch_sys update_defs []

979

in

980


981

let init_out =

982

build_switch_sys init_out []

983

in

984

let update_out =

985

build_switch_sys update_out []

986

in

987


988

let sw_init = clean_sys sw_init in

989

let sw_sys = clean_sys sw_sys in

990

let init_out = clean_sys init_out in

991

let update_out = clean_sys update_out in

992


993

(* Some additional checks *)

994

let pp_gl pp_expr =

995

fprintf_list ~sep:", " (fun fmt (e,b) > Format.fprintf fmt "%s%a" (if b then "" else "NOT ") pp_expr e)

996

in

997

let pp_gl_short = pp_gl (fun fmt e > Format.fprintf fmt "%i" e.Lustre_types.expr_tag) in

998

let pp_up fmt up = List.iter (fun (id,e) > Format.fprintf fmt "%s>%i; " id e.expr_tag) up in

999


1000

if false then

1001

begin

1002

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

1003

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

1004


1005

let sw_sys =

1006

List.map (fun (gl, up) >

1007

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

1008

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

1009

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

1010

Printers.pp_expr e

1011

Printers.pp_expr e'

1012

);

1013

res

1014

) gl in

1015

gl, up

1016

) sw_sys

1017

in

1018

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

1019

List.iter (fun (gl, _) >

1020

let rec aux hd l =

1021

match l with

1022

[] > ()

1023

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

1024

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

1025

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

1026

Printers.pp_expr e

1027

Printers.pp_expr e'

1028

)) others;

1029

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

1030

in

1031

aux [] gl

1032

) sw_sys;

1033

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

1034

let rec check_dup_up accu l =

1035

match l with

1036

 [] > ()

1037

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

1038

let others = accu@tl in

1039

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

1040

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

1041


1042

pp_gl_short gl

1043

pp_up up

1044

pp_gl_short gl'

1045

pp_up up'

1046


1047

) others;

1048


1049


1050


1051

check_dup_up (hd::accu) tl

1052


1053

in

1054

check_dup_up [] sw_sys;

1055

let sw_sys =

1056

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

1057

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

1058


1059

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

1060

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

1061

pp_gl_short gl1 pp_gl_short gl2

1062

;

1063

res

1064


1065

) sw_sys

1066


1067

in

1068

()

1069

end;

1070


1071


1072

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

1073

let module UpMap =

1074

struct

1075

include Map.Make (

1076

struct

1077

type t = (ident * expr) list

1078

let compare l1 l2 =

1079

let proj l = List.map (fun (s,e) > s, e.expr_tag) l in

1080

compare (proj l1) (proj l2)

1081

end)

1082

let pp = pp_up

1083

end

1084

in

1085

let module Guards = struct

1086

include Set.Make (

1087

struct

1088

type t = (expr * bool)

1089

let compare l1 l2 =

1090

let proj (e,b) = e.expr_tag, b in

1091

compare (proj l1) (proj l2)

1092

end)

1093

let pp_short fmt s = pp_gl_short fmt (elements s)

1094

let pp_long fmt s = pp_gl Printers.pp_expr fmt (elements s)

1095

end

1096

in

1097

let process sys =

1098

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

1099

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

1100

disjunctive guards. Each set represents a conjunction of

1101

expressions. *)

1102

let map =

1103

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

1104

(* creating a new set to describe gl *)

1105

let new_set =

1106

List.fold_left

1107

(fun set g > Guards.add g set)

1108

Guards.empty

1109

gl

1110

in

1111

(* updating the map with up > new_set *)

1112

if UpMap.mem up map then

1113

let (shared, disj) = UpMap.find up map in

1114

let new_shared = Guards.inter shared new_set in

1115

let remaining_shared = Guards.diff shared new_shared in

1116

let remaining_new_set = Guards.diff new_set new_shared in

1117

(* Adding remaining_shared to all elements of disj *)

1118

let disj' = List.map (fun gs > Guards.union remaining_shared gs) disj in

1119

UpMap.add up (new_shared, remaining_new_set::disj') map

1120

else

1121

UpMap.add up (new_set, []) map

1122

) UpMap.empty sys

1123

in

1124

let rec mk_binop op l = match l with

1125

[] > assert false

1126

 [e] > e

1127

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

1128

in

1129

let gl_as_expr gl =

1130

let gl = Guards.elements gl in

1131

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

1132

match gl with

1133

[] > []

1134

 [e] > [export e]

1135

 _ >

1136

[mk_binop "&&"

1137

(List.map export gl)]

1138

in

1139

let rec clean_disj disj =

1140

match disj with

1141

 []  [_] > []

1142

 _::_::_ > (

1143

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

1144

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

1145

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

1146

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

1147

let or_expr = mk_binop "" elems in

1148

[or_expr]

1149


1150


1151

(* TODO disj*)

1152

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

1153

(* List.fold_left (fun accu s >

1154

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

1155

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

1156

* ) accu (Guards.elements s)

1157

* ) [] disj *)

1158


1159

)

1160

in

1161

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

1162

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

1163

if !debug then

1164

Format.eprintf

1165

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

1166

Guards.pp_short common

1167

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

1168

UpMap.pp up;

1169

let disj = clean_disj disj in

1170

let guard_expr = (gl_as_expr common)@disj in

1171


1172

((match guard_expr with

1173

 [] > None

1174

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

1175

) map []

1176


1177

in

1178

process sw_init, process sw_sys, process init_out, process update_out
