1

(* 

2

* SchedMCore  A MultiCore Scheduling Framework

3

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

4

* Copyright (C) 20122013, INPT, Toulouse, FRANCE

5

*

6

* This file is part of Prelude

7

*

8

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

9

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

10

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

11

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

12

*

13

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

14

* WITHOUT ANY WARRANTY ; without even the implied warranty of

15

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

16

* Lesser General Public License for more details.

17

*

18

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

19

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

20

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

21

* USA

22

* *)

23


24

(* This module is used for the lustre to C compiler *)

25


26

open Format

27


28

type dim_expr =

29

{mutable dim_desc: dim_desc;

30

dim_loc: Location.t;

31

dim_id: int}

32


33

and dim_desc =

34

 Dbool of bool

35

 Dint of int

36

 Dident of Utils.ident

37

 Dappl of Utils.ident * dim_expr list

38

 Dite of dim_expr * dim_expr * dim_expr

39

 Dlink of dim_expr

40

 Dvar

41

 Dunivar

42


43

exception Unify of dim_expr * dim_expr

44

exception InvalidDimension

45


46

let new_id = ref (1)

47


48

let mkdim loc dim =

49

incr new_id;

50

{ dim_loc = loc;

51

dim_id = !new_id;

52

dim_desc = dim;}

53


54

let mkdim_var () =

55

incr new_id;

56

{ dim_loc = Location.dummy_loc;

57

dim_id = !new_id;

58

dim_desc = Dvar;}

59


60

let mkdim_ident loc id =

61

incr new_id;

62

{ dim_loc = loc;

63

dim_id = !new_id;

64

dim_desc = Dident id;}

65


66

let mkdim_bool loc b =

67

incr new_id;

68

{ dim_loc = loc;

69

dim_id = !new_id;

70

dim_desc = Dbool b;}

71


72

let mkdim_int loc i =

73

incr new_id;

74

{ dim_loc = loc;

75

dim_id = !new_id;

76

dim_desc = Dint i;}

77


78

let mkdim_appl loc f args =

79

incr new_id;

80

{ dim_loc = loc;

81

dim_id = !new_id;

82

dim_desc = Dappl (f, args);}

83


84

let mkdim_ite loc i t e =

85

incr new_id;

86

{ dim_loc = loc;

87

dim_id = !new_id;

88

dim_desc = Dite (i, t, e);}

89


90

let rec pp_dimension fmt dim =

91

(*fprintf fmt "<%d>" (Obj.magic dim: int);*)

92

match dim.dim_desc with

93

 Dident id >

94

fprintf fmt "%s" id

95

 Dint i >

96

fprintf fmt "%d" i

97

 Dbool b >

98

fprintf fmt "%B" b

99

 Dite (i, t, e) >

100

fprintf fmt "if %a then %a else %a"

101

pp_dimension i pp_dimension t pp_dimension e

102

 Dappl (f, [arg]) >

103

fprintf fmt "(%s%a)" f pp_dimension arg

104

 Dappl (f, [arg1; arg2]) >

105

fprintf fmt "(%a%s%a)" pp_dimension arg1 f pp_dimension arg2

106

 Dappl (_, _) > assert false

107

 Dlink dim' > fprintf fmt "%a" pp_dimension dim'

108

 Dvar > fprintf fmt "_%s" (Utils.name_of_dimension dim.dim_id)

109

 Dunivar > fprintf fmt "'%s" (Utils.name_of_dimension dim.dim_id)

110


111

let rec multi_dimension_product loc dim_list =

112

match dim_list with

113

 [] > mkdim_int loc 1

114

 [d] > d

115

 d::q > mkdim_appl loc "*" [d; multi_dimension_product loc q]

116


117

(* Builds a dimension expr representing 0<=d *)

118

let check_bound loc d =

119

mkdim_appl loc "<=" [mkdim_int loc 0; d]

120


121

(* Builds a dimension expr representing 0<=i<d *)

122

let check_access loc d i =

123

mkdim_appl loc "&&"

124

[mkdim_appl loc "<=" [mkdim_int loc 0; i];

125

mkdim_appl loc "<" [i; d]]

126


127

let rec repr dim =

128

match dim.dim_desc with

129

 Dlink dim' > repr dim'

130

 _ > dim

131


132

let rec is_eq_dimension d1 d2 =

133

let d1 = repr d1 in

134

let d2 = repr d2 in

135

d1.dim_id = d2.dim_id 

136

match d1.dim_desc, d2.dim_desc with

137

 Dappl (f1, args1), Dappl (f2, args2) >

138

f1 = f2 && List.length args1 = List.length args2 && List.for_all2 is_eq_dimension args1 args2

139

 Dite (c1, t1, e1), Dite (c2, t2, e2) >

140

is_eq_dimension c1 c2 && is_eq_dimension t1 t2 && is_eq_dimension e1 e2

141

 Dvar, _

142

 _, Dvar

143

 Dunivar, _

144

 _, Dunivar > false

145

 _ > d1 = d2

146


147

let is_dimension_const dim =

148

match (repr dim).dim_desc with

149

 Dint _

150

 Dbool _ > true

151

 _ > false

152


153

let size_const_dimension dim =

154

match (repr dim).dim_desc with

155

 Dint i > i

156

 Dbool b > if b then 1 else 0

157

 _ > (Format.eprintf "internal error: size_const_dimension %a@." pp_dimension dim; assert false)

158


159

let rec is_polymorphic dim =

160

match dim.dim_desc with

161

 Dident _

162

 Dint _

163

 Dbool _

164

 Dvar > false

165

 Dite (i, t, e) >

166

is_polymorphic i  is_polymorphic t  is_polymorphic e

167

 Dappl (_, args) > List.exists is_polymorphic args

168

 Dlink dim' > is_polymorphic dim'

169

 Dunivar > true

170


171

(* Normalizes a dimension expression, i.e. canonicalize all polynomial

172

subexpressions, where unsupported operations (eg. '/') are treated

173

as variables.

174

*)

175


176

let rec factors dim =

177

match dim.dim_desc with

178

 Dappl (f, args) when f = "*" > List.flatten (List.map factors args)

179

 _ > [dim]

180


181

let rec factors_constant fs =

182

match fs with

183

 [] > 1

184

 f::q >

185

match f.dim_desc with

186

 Dint i > i * (factors_constant q)

187

 _ > factors_constant q

188


189

let norm_factors fs =

190

let k = factors_constant fs in

191

let nk = List.filter (fun d > not (is_dimension_const d)) fs in

192

(k, List.sort Pervasives.compare nk)

193


194

let rec terms dim =

195

match dim.dim_desc with

196

 Dappl (f, args) when f = "+" > List.flatten (List.map terms args)

197

 _ > [dim]

198


199

let rec normalize dim =

200

dim

201

(*

202

let rec unnormalize loc l =

203

let l = List.sort (fun (k, l) (k', l') > compare l l') (List.map (fun (k, l) > (k, List.sort compare l)) l) in

204

match l with

205

 [] > mkdim_int loc 0

206

 t::q >

207

List.fold_left (fun res (k, l) > mkdim_appl loc "+" res (mkdim_appl loc "*" (mkdim_int loc k) l)) t q

208

*)

209

let copy copy_dim_vars dim =

210

let rec cp dim =

211

match dim.dim_desc with

212

 Dbool _

213

 Dint _ > dim

214

 Dident id > mkdim_ident dim.dim_loc id

215

 Dite (c, t, e) > mkdim_ite dim.dim_loc (cp c) (cp t) (cp e)

216

 Dappl (id, args) > mkdim_appl dim.dim_loc id (List.map cp args)

217

 Dlink dim' > cp dim'

218

 Dunivar > assert false

219

 Dvar >

220

try

221

List.assoc dim.dim_id !copy_dim_vars

222

with Not_found >

223

let var = mkdim dim.dim_loc Dvar in

224

copy_dim_vars := (dim.dim_id, var)::!copy_dim_vars;

225

var

226

in cp dim

227


228

(* Partially evaluates a 'simple' dimension expr [dim], i.e. an expr containing only int and bool

229

constructs, with conditionals. [eval_const] is a typing environment for static values. [eval_op] is an evaluation env for basic operators. The argument [dim] is modified inplace.

230

*)

231

let rec eval eval_op eval_const dim =

232

match dim.dim_desc with

233

 Dbool _

234

 Dint _ > ()

235

 Dident id >

236

(match eval_const id with

237

 Some val_dim > dim.dim_desc < Dlink val_dim

238

 None > raise InvalidDimension)

239

 Dite (c, t, e) >

240

begin

241

eval eval_op eval_const c;

242

eval eval_op eval_const t;

243

eval eval_op eval_const e;

244

match (repr c).dim_desc with

245

 Dbool b > dim.dim_desc < Dlink (if b then t else e)

246

 _ > ()

247

end

248

 Dappl (id, args) >

249

begin

250

List.iter (eval eval_op eval_const) args;

251

if List.for_all is_dimension_const args

252

then dim.dim_desc < Env.lookup_value eval_op id (List.map (fun d > (repr d).dim_desc) args)

253

end

254

 Dlink dim' >

255

begin

256

eval eval_op eval_const dim';

257

dim.dim_desc < Dlink (repr dim')

258

end

259

 Dvar > ()

260

 Dunivar > assert false

261


262

let uneval const univar =

263

let univar = repr univar in

264

match univar.dim_desc with

265

 Dunivar > univar.dim_desc < Dident const

266

 _ > assert false

267


268

(** [occurs dvar dim] returns true if the dimension variable [dvar] occurs in

269

dimension expression [dim]. False otherwise. *)

270

let rec occurs dvar dim =

271

let dim = repr dim in

272

match dim.dim_desc with

273

 Dvar > dim.dim_id = dvar.dim_id

274

 Dident _

275

 Dint _

276

 Dbool _

277

 Dunivar > false

278

 Dite (i, t, e) >

279

occurs dvar i  occurs dvar t  occurs dvar e

280

 Dappl (_, args) > List.exists (occurs dvar) args

281

 Dlink _ > assert false

282


283

(* Promote monomorphic dimension variables to polymorphic variables.

284

Generalize by sideeffects *)

285

let rec generalize dim =

286

match dim.dim_desc with

287

 Dvar > dim.dim_desc < Dunivar

288

 Dident _

289

 Dint _

290

 Dbool _

291

 Dunivar > ()

292

 Dite (i, t, e) >

293

generalize i; generalize t; generalize e

294

 Dappl (_, args) > List.iter generalize args

295

 Dlink dim' > generalize dim'

296


297

(* Instantiate polymorphic dimension variables to monomorphic variables.

298

Also duplicates the whole term structure (but the constant subterms).

299

*)

300

let rec instantiate inst_dim_vars dim =

301

let dim = repr dim in

302

match dim.dim_desc with

303

 Dvar _

304

 Dident _

305

 Dint _

306

 Dbool _ > dim

307

 Dite (i, t, e) >

308

mkdim_ite dim.dim_loc

309

(instantiate inst_dim_vars i)

310

(instantiate inst_dim_vars t)

311

(instantiate inst_dim_vars e)

312

 Dappl (f, args) > mkdim_appl dim.dim_loc f (List.map (instantiate inst_dim_vars) args)

313

 Dlink dim' > assert false (*mkdim dim.dim_loc (Dlink (instantiate inst_dim_vars dim'))*)

314

 Dunivar >

315

try

316

List.assoc dim.dim_id !inst_dim_vars

317

with Not_found >

318

let var = mkdim dim.dim_loc Dvar in

319

inst_dim_vars := (dim.dim_id, var)::!inst_dim_vars;

320

var

321


322

let rec unify dim1 dim2 =

323

let dim1 = repr dim1 in

324

let dim2 = repr dim2 in

325

if dim1.dim_id = dim2.dim_id then () else

326

match dim1.dim_desc, dim2.dim_desc with

327

 Dunivar, _

328

 _ , Dunivar > assert false

329

 Dvar , Dvar >

330

if dim1.dim_id < dim2.dim_id

331

then dim2.dim_desc < Dlink dim1

332

else dim1.dim_desc < Dlink dim2

333

 Dvar , _ when not (occurs dim1 dim2) >

334

dim1.dim_desc < Dlink dim2

335

 _ , Dvar when not (occurs dim2 dim1) >

336

dim2.dim_desc < Dlink dim1

337

 Dite(i1, t1, e1), Dite(i2, t2, e2) >

338

begin

339

unify i1 i2;

340

unify t1 t2;

341

unify e1 e2

342

end

343

 Dappl(f1, args1), Dappl(f2, args2) when f1 = f2 && List.length args1 = List.length args2 >

344

List.iter2 unify args1 args2

345

 Dbool b1, Dbool b2 when b1 = b2 > ()

346

 Dint i1 , Dint i2 when i1 = i2 > ()

347

 Dident id1, Dident id2 when id1 = id2 > ()

348

 _ > raise (Unify (dim1, dim2))

349


350

let rec semi_unify dim1 dim2 =

351

let dim1 = repr dim1 in

352

let dim2 = repr dim2 in

353

if dim1.dim_id = dim2.dim_id then () else

354

match dim1.dim_desc, dim2.dim_desc with

355

 Dunivar, _

356

 _ , Dunivar > assert false

357

 Dvar , Dvar >

358

if dim1.dim_id < dim2.dim_id

359

then dim2.dim_desc < Dlink dim1

360

else dim1.dim_desc < Dlink dim2

361

 Dvar , _ > raise (Unify (dim1, dim2))

362

 _ , Dvar when not (occurs dim2 dim1) >

363

dim2.dim_desc < Dlink dim1

364

 Dite(i1, t1, e1), Dite(i2, t2, e2) >

365

begin

366

semi_unify i1 i2;

367

semi_unify t1 t2;

368

semi_unify e1 e2

369

end

370

 Dappl(f1, args1), Dappl(f2, args2) when f1 = f2 && List.length args1 = List.length args2 >

371

List.iter2 semi_unify args1 args2

372

 Dbool b1, Dbool b2 when b1 = b2 > ()

373

 Dint i1 , Dint i2 when i1 = i2 > ()

374

 Dident id1, Dident id2 when id1 = id2 > ()

375

 _ > raise (Unify (dim1, dim2))

376


377

let rec expr_replace_var fvar e =

378

{ e with dim_desc = expr_replace_desc fvar e.dim_desc }

379

and expr_replace_desc fvar e =

380

let re = expr_replace_var fvar in

381

match e with

382

 Dvar

383

 Dunivar

384

 Dbool _

385

 Dint _ > e

386

 Dident v > Dident (fvar v)

387

 Dappl (id, el) > Dappl (id, List.map re el)

388

 Dite (g,t,e) > Dite (re g, re t, re e)

389

 Dlink e > Dlink (re e)
