1

/* 

2

* SchedMCore  A MultiCore Scheduling Framework

3

* Copyright (C) 20092011, ONERA, Toulouse, FRANCE  LIFL, Lille, FRANCE

4

*

5

* This file is part of Prelude

6

*

7

* Prelude is free software; you can redistribute it and/or

8

* modify it under the terms of the GNU Lesser General Public License

9

* as published by the Free Software Foundation ; either version 2 of

10

* the License, or (at your option) any later version.

11

*

12

* Prelude is distributed in the hope that it will be useful, but

13

* WITHOUT ANY WARRANTY ; without even the implied warranty of

14

* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU

15

* Lesser General Public License for more details.

16

*

17

* You should have received a copy of the GNU Lesser General Public

18

* License along with this program ; if not, write to the Free Software

19

* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 021111307

20

* USA

21

* */

22


23

%{

24

open LustreSpec

25

open Corelang

26

open Dimension

27

open Utils

28


29

let mktyp x = mktyp (Location.symbol_rloc ()) x

30

let mkclock x = mkclock (Location.symbol_rloc ()) x

31

let mkvar_decl x = mkvar_decl (Location.symbol_rloc ()) x

32

let mkexpr x = mkexpr (Location.symbol_rloc ()) x

33

let mkeq x = mkeq (Location.symbol_rloc ()) x

34

let mkassert x = mkassert (Location.symbol_rloc ()) x

35

let mktop_decl x = mktop_decl (Location.symbol_rloc ()) x

36

let mkpredef_call x = mkpredef_call (Location.symbol_rloc ()) x

37


38

let mkdim_int i = mkdim_int (Location.symbol_rloc ()) i

39

let mkdim_bool b = mkdim_bool (Location.symbol_rloc ()) b

40

let mkdim_ident id = mkdim_ident (Location.symbol_rloc ()) id

41

let mkdim_appl f args = mkdim_appl (Location.symbol_rloc ()) f args

42

let mkdim_ite i t e = mkdim_ite (Location.symbol_rloc ()) i t e

43


44

let add_node loc own msg hashtbl name value =

45

try

46

match (Hashtbl.find hashtbl name).top_decl_desc, value.top_decl_desc with

47

 Node _ , ImportedNode _ when own > ()

48

 ImportedNode _, _ > Hashtbl.add hashtbl name value

49

 Node _ , _ > raise (Corelang.Error (loc, Corelang.Already_bound_symbol msg))

50

 _ > assert false

51

with

52

Not_found > Hashtbl.add hashtbl name value

53


54


55

let add_symbol loc msg hashtbl name value =

56

if Hashtbl.mem hashtbl name

57

then raise (Corelang.Error (loc, Corelang.Already_bound_symbol msg))

58

else Hashtbl.add hashtbl name value

59


60

let check_symbol loc msg hashtbl name =

61

if not (Hashtbl.mem hashtbl name)

62

then raise (Corelang.Error (loc, Corelang.Unbound_symbol msg))

63

else ()

64


65

%}

66


67

%token <int> INT

68

%token <string> REAL

69

%token <float> FLOAT

70

%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST

71

%token STATELESS ASSERT OPEN QUOTE FUNCTION

72

%token <string> IDENT

73

%token <LustreSpec.expr_annot> ANNOT

74

%token <LustreSpec.node_annot> NODESPEC

75

%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL

76

%token AMPERAMPER BARBAR NOT POWER

77

%token IF THEN ELSE

78

%token UCLOCK DCLOCK PHCLOCK TAIL

79

%token MERGE FBY WHEN WHENNOT EVERY

80

%token NODE LET TEL RETURNS VAR IMPORTED SENSOR ACTUATOR WCET TYPE CONST

81

%token STRUCT ENUM

82

%token TINT TFLOAT TREAL TBOOL TCLOCK

83

%token RATE DUE

84

%token EQ LT GT LTE GTE NEQ

85

%token AND OR XOR IMPL

86

%token MULT DIV MOD

87

%token MINUS PLUS UMINUS

88

%token PRE ARROW

89

%token PROTOTYPE LIB

90

%token EOF

91


92

%nonassoc COMMA

93

%left MERGE IF

94

%nonassoc ELSE

95

%right ARROW FBY

96

%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK

97

%right COLCOL

98

%right IMPL

99

%left OR XOR BARBAR

100

%left AND AMPERAMPER

101

%left NOT

102

%nonassoc INT

103

%nonassoc EQ LT GT LTE GTE NEQ

104

%left MINUS PLUS

105

%left MULT DIV MOD

106

%left UMINUS

107

%left POWER

108

%left PRE LAST

109

%nonassoc RBRACKET

110

%nonassoc LBRACKET

111


112

%start prog

113

%type <Corelang.top_decl list> prog

114

%start header

115

%type <bool > Corelang.top_decl list> header

116


117

%%

118


119

prog:

120

open_list typ_def_list top_decl_list EOF { $1 @ (List.rev $3) }

121


122

header:

123

open_list typ_def_list top_decl_header_list EOF { (fun own > ($1 @ (List.rev ($3 own)))) }

124


125

open_list:

126

{ [] }

127

 open_lusi open_list { $1 :: $2 }

128


129

open_lusi:

130

 OPEN QUOTE IDENT QUOTE { mktop_decl (Open (true, $3))}

131

 OPEN LT IDENT GT { mktop_decl (Open (false, $3)) }

132


133

top_decl_list:

134

top_decl {[$1]}

135

 top_decl_list top_decl {$2::$1}

136


137


138

top_decl_header_list:

139

top_decl_header {(fun own > [$1 own]) }

140

 top_decl_header_list top_decl_header {(fun own > ($2 own)::($1 own)) }

141


142

state_annot:

143

FUNCTION { true }

144

 NODE { false }

145


146

top_decl_header:

147

 CONST cdecl_list { let top = mktop_decl (Consts (List.rev $2)) in fun _ > top }

148

 nodespec_list state_annot IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR prototype_opt in_lib_opt SCOL

149

{let nd = mktop_decl (ImportedNode

150

{nodei_id = $3;

151

nodei_type = Types.new_var ();

152

nodei_clock = Clocks.new_var true;

153

nodei_inputs = List.rev $5;

154

nodei_outputs = List.rev $10;

155

nodei_stateless = $2;

156

nodei_spec = $1;

157

nodei_prototype = $13;

158

nodei_in_lib = $14;})

159

in

160

(let loc = Location.symbol_rloc () in

161

fun own > add_node loc own ("node " ^ $3) node_table $3 nd; nd) }

162


163

prototype_opt:

164

{ None }

165

 PROTOTYPE IDENT { Some $2}

166


167

in_lib_opt:

168

{ None }

169

 LIB IDENT {Some $2}

170


171

top_decl:

172

 CONST cdecl_list { mktop_decl (Consts (List.rev $2)) }

173

 nodespec_list state_annot IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL

174

{let eqs, asserts, annots = $16 in

175

let nd = mktop_decl (Node

176

{node_id = $3;

177

node_type = Types.new_var ();

178

node_clock = Clocks.new_var true;

179

node_inputs = List.rev $5;

180

node_outputs = List.rev $10;

181

node_locals = List.rev $14;

182

node_gencalls = [];

183

node_checks = [];

184

node_asserts = asserts;

185

node_eqs = eqs;

186

node_dec_stateless = $2;

187

node_stateless = None;

188

node_spec = $1;

189

node_annot = match annots with [] > None  _ > Some annots})

190

in

191

let loc = Location.symbol_rloc () in

192

add_node loc true ("node " ^ $3) node_table $3 nd; nd}

193


194

nodespec_list:

195

{ None }

196

 NODESPEC nodespec_list { (function None > (fun s1 > Some s1)  Some s2 > (fun s1 > Some (LustreSpec.merge_node_annot s1 s2))) $2 $1 }

197


198

typ_def_list:

199

/* empty */ {}

200

 typ_def SCOL typ_def_list {$1;$3}

201


202

typ_def:

203

TYPE IDENT EQ typeconst {

204

try

205

let loc = Location.symbol_rloc () in

206

add_symbol loc ("type " ^ $2) type_table (Tydec_const $2) (Corelang.get_repr_type $4)

207

with Not_found> assert false }

208

 TYPE IDENT EQ ENUM LCUR tag_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_enum ($6 (Tydec_const $2))) }

209

 TYPE IDENT EQ STRUCT LCUR field_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_struct ($6 (Tydec_const $2))) }

210


211

array_typ_decl:

212

{ fun typ > typ }

213

 POWER dim array_typ_decl { fun typ > $3 (Tydec_array ($2, typ)) }

214


215

typeconst:

216

TINT array_typ_decl { $2 Tydec_int }

217

 TBOOL array_typ_decl { $2 Tydec_bool }

218

 TREAL array_typ_decl { $2 Tydec_real }

219

 TFLOAT array_typ_decl { $2 Tydec_float }

220

 IDENT array_typ_decl {

221

let loc = Location.symbol_rloc () in

222

check_symbol loc ("type " ^ $1) type_table (Tydec_const $1); $2 (Tydec_const $1) }

223

 TBOOL TCLOCK { Tydec_clock Tydec_bool }

224

 IDENT TCLOCK { Tydec_clock (Tydec_const $1) }

225


226

tag_list:

227

IDENT

228

{ let loc = Location.symbol_rloc () in

229

(fun t >

230

add_symbol loc ("tag " ^ $1) tag_table $1 t; $1 :: []) }

231

 tag_list COMMA IDENT

232

{

233

let loc = Location.symbol_rloc () in

234

(fun t > add_symbol loc ("tag " ^ $3)tag_table $3 t; $3 :: ($1 t))

235

}

236


237

field_list:

238

{ (fun t > []) }

239

 field_list IDENT COL typeconst SCOL

240

{

241

let loc = Location.symbol_rloc () in

242

(fun t > add_symbol loc ("field " ^ $2) field_table $2 t; ($1 t) @ [ ($2, $4) ]) }

243


244

eq_list:

245

{ [], [], [] }

246

 eq eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}

247

 assert_ eq_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}

248

 ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1@annotl}

249

 automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}

250


251

automaton:

252

AUTOMATON IDENT handler_list { failwith "not implemented" }

253


254

handler_list:

255

{ [] }

256

 handler handler_list { $1::$2 }

257


258

handler:

259

STATE IDENT ARROW unless_list locals LET eq_list TEL until_list { () }

260


261

unless_list:

262

{ [] }

263

 unless unless_list { $1::$2 }

264


265

until_list:

266

{ [] }

267

 until until_list { $1::$2 }

268


269

unless:

270

UNLESS expr RESTART IDENT { }

271

 UNLESS expr RESUME IDENT { }

272


273

until:

274

UNTIL expr RESTART IDENT { }

275

 UNTIL expr RESUME IDENT { }

276


277

assert_:

278

 ASSERT expr SCOL {mkassert ($2)}

279


280

eq:

281

ident_list EQ expr SCOL {mkeq (List.rev $1,$3)}

282

 LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev $2,$5)}

283


284

tuple_expr:

285

expr COMMA expr {[$3;$1]}

286

 tuple_expr COMMA expr {$3::$1}

287


288

// Same as tuple expr but accepting lists with single element

289

array_expr:

290

expr {[$1]}

291

 expr COMMA array_expr {$1::$3}

292


293

dim_list:

294

dim RBRACKET { fun base > mkexpr (Expr_access (base, $1)) }

295

 dim RBRACKET LBRACKET dim_list { fun base > $4 (mkexpr (Expr_access (base, $1))) }

296


297

expr:

298

/* constants */

299

INT {mkexpr (Expr_const (Const_int $1))}

300

 REAL {mkexpr (Expr_const (Const_real $1))}

301

 FLOAT {mkexpr (Expr_const (Const_float $1))}

302

/* Idents or type enum tags */

303

 IDENT {

304

if Hashtbl.mem tag_table $1

305

then mkexpr (Expr_const (Const_tag $1))

306

else mkexpr (Expr_ident $1)}

307

 LPAR ANNOT expr RPAR

308

{update_expr_annot $3 $2}

309

 LPAR expr RPAR

310

{$2}

311

 LPAR tuple_expr RPAR

312

{mkexpr (Expr_tuple (List.rev $2))}

313


314

/* Array expressions */

315

 LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }

316

 expr POWER dim { mkexpr (Expr_power ($1, $3)) }

317

 expr LBRACKET dim_list { $3 $1 }

318


319

/* Temporal operators */

320

 PRE expr

321

{mkexpr (Expr_pre $2)}

322

 expr ARROW expr

323

{mkexpr (Expr_arrow ($1,$3))}

324

 expr FBY expr

325

{(*mkexpr (Expr_fby ($1,$3))*)

326

mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}

327

 expr WHEN IDENT

328

{mkexpr (Expr_when ($1,$3,tag_true))}

329

 expr WHENNOT IDENT

330

{mkexpr (Expr_when ($1,$3,tag_false))}

331

 expr WHEN IDENT LPAR IDENT RPAR

332

{mkexpr (Expr_when ($1, $5, $3))}

333

 MERGE IDENT handler_expr_list

334

{mkexpr (Expr_merge ($2,$3))}

335


336

/* Applications */

337

 IDENT LPAR expr RPAR

338

{mkexpr (Expr_appl ($1, $3, None))}

339

 IDENT LPAR expr RPAR EVERY IDENT

340

{mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))}

341

 IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR

342

{mkexpr (Expr_appl ($1, $3, Some ($8, $6))) }

343

 IDENT LPAR tuple_expr RPAR

344

{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}

345

 IDENT LPAR tuple_expr RPAR EVERY IDENT

346

{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) }

347

 IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR

348

{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) }

349


350

/* Boolean expr */

351

 expr AND expr

352

{mkpredef_call "&&" [$1;$3]}

353

 expr AMPERAMPER expr

354

{mkpredef_call "&&" [$1;$3]}

355

 expr OR expr

356

{mkpredef_call "" [$1;$3]}

357

 expr BARBAR expr

358

{mkpredef_call "" [$1;$3]}

359

 expr XOR expr

360

{mkpredef_call "xor" [$1;$3]}

361

 NOT expr

362

{mkpredef_call "not" [$2]}

363

 expr IMPL expr

364

{mkpredef_call "impl" [$1;$3]}

365


366

/* Comparison expr */

367

 expr EQ expr

368

{mkpredef_call "=" [$1;$3]}

369

 expr LT expr

370

{mkpredef_call "<" [$1;$3]}

371

 expr LTE expr

372

{mkpredef_call "<=" [$1;$3]}

373

 expr GT expr

374

{mkpredef_call ">" [$1;$3]}

375

 expr GTE expr

376

{mkpredef_call ">=" [$1;$3]}

377

 expr NEQ expr

378

{mkpredef_call "!=" [$1;$3]}

379


380

/* Arithmetic expr */

381

 expr PLUS expr

382

{mkpredef_call "+" [$1;$3]}

383

 expr MINUS expr

384

{mkpredef_call "" [$1;$3]}

385

 expr MULT expr

386

{mkpredef_call "*" [$1;$3]}

387

 expr DIV expr

388

{mkpredef_call "/" [$1;$3]}

389

 MINUS expr %prec UMINUS

390

{mkpredef_call "uminus" [$2]}

391

 expr MOD expr

392

{mkpredef_call "mod" [$1;$3]}

393


394

/* If */

395

 IF expr THEN expr ELSE expr

396

{mkexpr (Expr_ite ($2, $4, $6))}

397


398

handler_expr_list:

399

{ [] }

400

 handler_expr handler_expr_list { $1 :: $2 }

401


402

handler_expr:

403

LPAR IDENT ARROW expr RPAR { ($2, $4) }

404


405

signed_const_array:

406

 signed_const { [$1] }

407

 signed_const COMMA signed_const_array { $1 :: $3 }

408


409

signed_const_struct:

410

 IDENT EQ signed_const { [ ($1, $3) ] }

411

 IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 }

412


413

signed_const:

414

INT {Const_int $1}

415

 REAL {Const_real $1}

416

 FLOAT {Const_float $1}

417

 IDENT {Const_tag $1}

418

 MINUS INT {Const_int (1 * $2)}

419

 MINUS REAL {Const_real ("" ^ $2)}

420

 MINUS FLOAT {Const_float (1. *. $2)}

421

 LCUR signed_const_struct RCUR { Const_struct $2 }

422

 LBRACKET signed_const_array RBRACKET { Const_array $2 }

423


424

dim:

425

INT { mkdim_int $1 }

426

 LPAR dim RPAR { $2 }

427

 IDENT { mkdim_ident $1 }

428

 dim AND dim

429

{mkdim_appl "&&" [$1;$3]}

430

 dim AMPERAMPER dim

431

{mkdim_appl "&&" [$1;$3]}

432

 dim OR dim

433

{mkdim_appl "" [$1;$3]}

434

 dim BARBAR dim

435

{mkdim_appl "" [$1;$3]}

436

 dim XOR dim

437

{mkdim_appl "xor" [$1;$3]}

438

 NOT dim

439

{mkdim_appl "not" [$2]}

440

 dim IMPL dim

441

{mkdim_appl "impl" [$1;$3]}

442


443

/* Comparison dim */

444

 dim EQ dim

445

{mkdim_appl "=" [$1;$3]}

446

 dim LT dim

447

{mkdim_appl "<" [$1;$3]}

448

 dim LTE dim

449

{mkdim_appl "<=" [$1;$3]}

450

 dim GT dim

451

{mkdim_appl ">" [$1;$3]}

452

 dim GTE dim

453

{mkdim_appl ">=" [$1;$3]}

454

 dim NEQ dim

455

{mkdim_appl "!=" [$1;$3]}

456


457

/* Arithmetic dim */

458

 dim PLUS dim

459

{mkdim_appl "+" [$1;$3]}

460

 dim MINUS dim

461

{mkdim_appl "" [$1;$3]}

462

 dim MULT dim

463

{mkdim_appl "*" [$1;$3]}

464

 dim DIV dim

465

{mkdim_appl "/" [$1;$3]}

466

 MINUS dim %prec UMINUS

467

{mkdim_appl "uminus" [$2]}

468

 dim MOD dim

469

{mkdim_appl "mod" [$1;$3]}

470

/* If */

471

 IF dim THEN dim ELSE dim

472

{mkdim_ite $2 $4 $6}

473


474

locals:

475

{[]}

476

 VAR vdecl_list SCOL {$2}

477


478

vdecl_list:

479

vdecl {$1}

480

 vdecl_list SCOL vdecl {$3 @ $1}

481


482

vdecl:

483

/* Useless no ?*/ ident_list

484

{List.map mkvar_decl

485

(List.map (fun id > (id, mktyp Tydec_any, mkclock Ckdec_any, false)) $1)}

486


487

 ident_list COL typeconst clock

488

{List.map mkvar_decl (List.map (fun id > (id, mktyp $3, $4, false)) $1)}

489

 CONST ident_list COL typeconst /* static parameters don't have clocks */

490

{List.map mkvar_decl (List.map (fun id > (id, mktyp $4, mkclock Ckdec_any, true)) $2)}

491


492

cdecl_list:

493

cdecl SCOL { [$1] }

494

 cdecl_list cdecl SCOL { $2::$1 }

495


496

cdecl:

497

IDENT EQ signed_const {

498

let c = {

499

const_id = $1;

500

const_loc = Location.symbol_rloc ();

501

const_type = Types.new_var ();

502

const_value = $3;

503

} in

504

Hashtbl.add consts_table $1 c; c

505

}

506


507

clock:

508

{mkclock Ckdec_any}

509

 when_list

510

{mkclock (Ckdec_bool (List.rev $1))}

511


512

when_cond:

513

WHEN IDENT {($2, tag_true)}

514

 WHENNOT IDENT {($2, tag_false)}

515

 WHEN IDENT LPAR IDENT RPAR {($4, $2)}

516


517

when_list:

518

when_cond {[$1]}

519

 when_list when_cond {$2::$1}

520


521

ident_list:

522

IDENT {[$1]}

523

 ident_list COMMA IDENT {$3::$1}

524


525

SCOL_opt:

526

SCOL {}  {}
