1

(* Extension du deal with machine types annotation

2


3

In each node, node local annotations can specify the actual type of the

4

implementation uintXX, intXX, floatXX ...

5


6

The module provide utility functions to query the model:

7

 get_var_machine_type varid nodeid returns the string denoting the actual type

8


9

The actual type is used at different stages of the coompilation

10

 early stage: limited typing, ie validity of operation are checked

11

 a first version ensures that the actual type is a subtype of the declared/infered ones

12

eg uint8 is a valid subtype of int

13

 a future implementation could ensures that operations are valid

14

 each standard or unspecified operation should be homogeneous :

15

op: real > real > real is valid for any same subtype t of real: op: t > t > t

16

 specific nodes that explicitely defined subtypes could be used to perform casts

17

eg. a int2uint8 (i: int) returns (j: int) with annotations specifying i as int and j as uint8

18

 C backend: any print of a typed variable should rely on the actual machine type when provided

19

 EMF backend: idem

20

 Horn backend: an option could enforce the bounds provided by the machine

21

type or implement the cycling behavior for integer subtypes

22

 Salsa plugin: the information should be propagated to the plugin.

23

One can also imagine that results of the analysis could specify or

24

substitute a type by a subtype. Eg. the analysis detects that a float32 is enough for variable z and

25

the annotation is added to the node.

26


27


28

A posisble behavior could be

29

 an option to ensure type checking

30

 dedicated conversion functions that, in C, would generate cast or calls to simple identity functions (to be inlined)

31


32


33


34

TODO

35

EMF: rajouter les memoires dans les caracteristiques du node

36

gerer les types plus finement:

37

propager les types machines aux variables fraiches creees par la normalisation

38


39

*)

40

open Lustre_types

41


42

let is_active = false

43


44

let keyword = ["machine_types"]

45


46

module MT =

47

struct

48


49

type int_typ =

50

 Tint8_t

51

 Tint16_t

52

 Tint32_t

53

 Tint64_t

54

 Tuint8_t

55

 Tuint16_t

56

 Tuint32_t

57

 Tuint64_t

58


59

let pp_int fmt t =

60

match t with

61

 Tint8_t > Format.fprintf fmt "int8"

62

 Tint16_t > Format.fprintf fmt "int16"

63

 Tint32_t > Format.fprintf fmt "int32"

64

 Tint64_t > Format.fprintf fmt "int64"

65

 Tuint8_t > Format.fprintf fmt "uint8"

66

 Tuint16_t > Format.fprintf fmt "uint16"

67

 Tuint32_t > Format.fprintf fmt "uint32"

68

 Tuint64_t > Format.fprintf fmt "uint64"

69


70

let pp_c_int fmt t =

71

match t with

72

 Tint8_t > Format.fprintf fmt "int8_t"

73

 Tint16_t > Format.fprintf fmt "int16_t"

74

 Tint32_t > Format.fprintf fmt "int32_t"

75

 Tint64_t > Format.fprintf fmt "int64_t"

76

 Tuint8_t > Format.fprintf fmt "uint8_t"

77

 Tuint16_t > Format.fprintf fmt "uint16_t"

78

 Tuint32_t > Format.fprintf fmt "uint32_t"

79

 Tuint64_t > Format.fprintf fmt "uint64_t"

80


81

type t =

82

 MTint of int_typ option

83

 MTreal of string option

84

 MTbool

85

 MTstring

86


87

open Format

88

let pp fmt t =

89

match t with

90

 MTint None >

91

fprintf fmt "int"

92

 MTint (Some s) >

93

fprintf fmt "%a" pp_int s

94

 MTreal None >

95

fprintf fmt "real"

96

 MTreal (Some s) >

97

fprintf fmt "%s" s

98

 MTbool >

99

fprintf fmt "bool"

100

 MTstring >

101

fprintf fmt "string"

102


103

let pp_c fmt t =

104

match t with

105

 MTint (Some s) >

106

fprintf fmt "%a" pp_c_int s

107

 MTreal (Some s) >

108

fprintf fmt "%s" s

109

 MTint None

110

 MTreal None

111

 MTbool

112

 MTstring > assert false

113


114


115

let is_scalar_type t =

116

match t with

117

 MTbool

118

 MTint _

119

 MTreal _ > true

120

 _ > false

121


122


123

let is_numeric_type t =

124

match t with

125

 MTint _

126

 MTreal _ > true

127

 _ > false

128


129

let is_int_type t = match t with MTint _ > true  _ > false

130

let is_real_type t = match t with MTreal _ > true  _ > false

131

let is_bool_type t = t = MTbool

132


133

let is_dimension_type t =

134

match t with

135

 MTint _

136

 MTbool > true

137

 _ > false

138


139

let type_int_builder = MTint None

140

let type_real_builder = MTreal None

141

let type_bool_builder = MTbool

142

let type_string_builder = MTstring

143


144

let unify _ _ = ()

145

let is_unifiable b1 b2 =

146

match b1, b2 with

147

 MTint _ , MTint _

148

 MTreal _, MTreal _

149

 MTstring, MTstring

150

 MTbool, MTbool > true

151

 _ > false

152


153

let is_exportable b =

154

match b with

155

 MTstring

156

 MTbool

157

 MTreal None

158

 MTint None > false

159

 _ > true

160

end

161


162

module MTypes = Types.Make (MT)

163


164

let type_uint8 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tuint8_t)))

165

let type_uint16 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tuint16_t)))

166

let type_uint32 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tuint32_t)))

167

let type_uint64 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tuint64_t)))

168

let type_int8 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tint8_t)))

169

let type_int16 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tint16_t)))

170

let type_int32 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tint32_t)))

171

let type_int64 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tint64_t)))

172


173


174

module ConvTypes =

175

struct

176

type type_expr = MTypes.type_expr

177


178

let map_type_basic f_basic =

179

let rec map_type_basic e =

180

{ MTypes.tid = e.Types.tid;

181

MTypes.tdesc = map_type_basic_desc (Types.type_desc e)

182

}

183

and map_type_basic_desc td =

184

let mape = map_type_basic in

185

match td with

186

 Types.Tbasic b > f_basic b

187

 Types.Tconst c > MTypes.Tconst c

188

 Types.Tenum e > MTypes.Tenum e

189

 Types.Tvar > MTypes.Tvar

190

 Types.Tunivar > MTypes.Tunivar

191


192

 Types.Tclock te > MTypes.Tclock (mape te)

193

 Types.Tarrow (te1, te2) > MTypes.Tarrow (mape te1, mape te2)

194

 Types.Ttuple tel > MTypes.Ttuple (List.map mape tel)

195

 Types.Tstruct id_te_l > MTypes.Tstruct (List.map (fun (id, te) > id, mape te) id_te_l)

196

 Types.Tarray (de, te) > MTypes.Tarray (de, mape te)

197

 Types.Tstatic (de, te) > MTypes.Tstatic (de, mape te)

198

 Types.Tlink te > MTypes.Tlink (mape te)

199

in

200

map_type_basic

201


202

let import main_typ =

203

let import_basic b =

204

if Types.BasicT.is_int_type b then MTypes.type_int else

205

if Types.BasicT.is_real_type b then MTypes.type_real else

206

if Types.BasicT.is_bool_type b then MTypes.type_bool else

207

(Format.eprintf "importing %a with issues!@.@?" Types.print_ty main_typ; assert false)

208

in

209

map_type_basic import_basic main_typ

210


211


212

let map_mtype_basic f_basic =

213

let rec map_mtype_basic e =

214

{ Types.tid = e.MTypes.tid;

215

Types.tdesc = map_mtype_basic_desc (MTypes.type_desc e)

216

}

217

and map_mtype_basic_desc td =

218

let mape = map_mtype_basic in

219

match td with

220

 MTypes.Tbasic b >

221

(* Format.eprintf "supposely basic mtype: %a@." MTypes.BasicT.pp b; *)

222

f_basic b

223

 MTypes.Tconst c > Types.Tconst c

224

 MTypes.Tenum e > Types.Tenum e

225

 MTypes.Tvar > Types.Tvar

226

 MTypes.Tunivar > Types.Tunivar

227


228

 MTypes.Tclock te > Types.Tclock (mape te)

229

 MTypes.Tarrow (te1, te2) > Types.Tarrow (mape te1, mape te2)

230

 MTypes.Ttuple tel > Types.Ttuple (List.map mape tel)

231

 MTypes.Tstruct id_te_l > Types.Tstruct (List.map (fun (id, te) > id, mape te) id_te_l)

232

 MTypes.Tarray (de, te) > Types.Tarray (de, mape te)

233

 MTypes.Tstatic (de, te) > Types.Tstatic (de, mape te)

234

 MTypes.Tlink te > Types.Tlink (mape te)

235

in

236

map_mtype_basic

237


238

let export machine_type =

239

let export_basic b =

240

if MTypes.BasicT.is_int_type b then Types.type_int else

241

if MTypes.BasicT.is_real_type b then Types.type_real else

242

if MTypes.BasicT.is_bool_type b then Types.type_bool else

243

(

244

Format.eprintf "unhandled basic mtype is %a. Issues while dealing with basic type %a@.@?" MTypes.print_ty machine_type MTypes.BasicT.pp b;

245

assert false

246

)

247

in

248

map_mtype_basic export_basic machine_type

249


250

end

251


252

module Typing = Typing.Make (MTypes) (ConvTypes)

253


254

(* Associate to each (node_id, var_id) its machine type *)

255

let machine_type_table : (var_decl, MTypes.type_expr) Hashtbl.t = Hashtbl.create 13

256


257

(* Store the node signatures, with machine types when available *)

258

let typing_env = ref Env.initial

259


260

let is_specified v =

261

(* Format.eprintf "looking for var %a@." Printers.pp_var v; *)

262

Hashtbl.mem machine_type_table v

263


264

let pp_table fmt =

265

Format.fprintf fmt "@[<v 0>[";

266

Hashtbl.iter

267

(fun v typ > Format.fprintf fmt "%a > %a,@ " Printers.pp_var v MTypes.print_ty typ )

268

machine_type_table;

269

Format.fprintf fmt "@]"

270


271


272

let get_specified_type v =

273

(* Format.eprintf "Looking for variable %a in table [%t]@.@?" *)

274

(* Printers.pp_var v *)

275

(* pp_table; *)

276

Hashtbl.find machine_type_table v

277


278

let is_exportable v =

279

is_specified v && (

280

let typ = get_specified_type v in

281

match (MTypes.dynamic_type typ).MTypes.tdesc with

282

 MTypes.Tbasic b > MT.is_exportable b

283

 MTypes.Tconst _ > false (* Enumerated types are not "machine type" customizeable *)

284

 _ > assert false (* TODO deal with other constructs *)

285

)

286

(* could depend on the actual computed type *)

287


288

let type_name typ =

289

MTypes.print_ty Format.str_formatter typ;

290

Format.flush_str_formatter ()

291


292

let pp_var_type fmt v =

293

let typ = get_specified_type v in

294

MTypes.print_ty fmt typ

295


296

let pp_c_var_type fmt v =

297

let typ = get_specified_type v in

298

MTypes.print_ty_param MT.pp_c fmt typ

299


300

(************** Checking types ******************)

301


302

let erroneous_annotation loc =

303

Format.eprintf "Invalid annotation for machine_type at loc %a@."

304

Location.pp_loc loc;

305

assert false

306


307


308

let valid_subtype subtype typ =

309

let mismatch subtyp typ =

310

Format.eprintf "Subtype mismatch %a vs %a@." MTypes.print_ty subtyp Types.print_ty typ; false

311

in

312

match (MTypes.dynamic_type subtype).MTypes.tdesc with

313

 MTypes.Tconst c > Types.is_const_type typ c

314

 MTypes.Tbasic MT.MTint _ > Types.is_int_type typ

315

 MTypes.Tbasic MT.MTreal _ > Types.is_real_type typ

316

 MTypes.Tbasic MT.MTbool > Types.is_bool_type typ

317

 _ > mismatch subtype typ

318


319

let type_of_name name =

320

match name with

321

 "uint8" > type_uint8

322

 "uint16" > type_uint16

323

 "uint32" > type_uint32

324

 "uint64" > type_uint64

325

 "int8" > type_int8

326

 "int16" > type_int16

327

 "int32" > type_int32

328

 "int64" > type_int64

329

 _ > assert false (* unknown custom machine type *)

330


331

let register_var var typ =

332

(* let typ = type_of_name type_name in *)

333

if valid_subtype typ var.var_type then (

334

Hashtbl.add machine_type_table var typ

335

)

336

else

337

erroneous_annotation var.var_loc

338


339

(* let register_var_opt var type_name_opt = *)

340

(* match type_name_opt with *)

341

(*  None > () *)

342

(*  Some type_name > register_var var type_name *)

343


344

(************** Registering annotations ******************)

345


346


347

let register_node node_id vars annots =

348

List.fold_left (fun accu annot >

349

let annl = annot.annots in

350

List.fold_left (fun accu (kwd, value) >

351

if kwd = keyword then

352

let expr = value.eexpr_qfexpr in

353

match Corelang.expr_list_of_expr expr with

354

 [var_id; type_name] > (

355

match var_id.expr_desc, type_name.expr_desc with

356

 Expr_ident var_id, Expr_const (Const_string type_name) >

357

let var = List.find (fun v > v.var_id = var_id) vars in

358

Log.report ~level:2 (fun fmt >

359

Format.fprintf fmt "Recorded type %s for variable %a (parent node is %s)@ "

360

type_name

361

Printers.pp_var var

362

(match var.var_parent_nodeid with Some id > id  None > "unknown")

363

);

364

let typ = type_of_name type_name in

365

register_var var typ;

366

var::accu

367

 _ > erroneous_annotation expr.expr_loc

368

)

369

 _ > erroneous_annotation expr.expr_loc

370

else

371

accu

372

) accu annl

373

) [] annots

374


375


376

let check_node nd vars =

377

(* TODO check that all access to vars are valid *)

378

()

379


380

let type_of_vlist vars =

381

let tyl = List.map (fun v > if is_specified v then get_specified_type v else

382

ConvTypes.import v.var_type

383

) vars in

384

MTypes.type_of_type_list tyl

385


386


387

let load prog =

388

let init_env =

389

Env.fold (fun id typ env >

390

Env.add_value env id (ConvTypes.import typ)

391

)

392

Basic_library.type_env Env.initial in

393

let env =

394

List.fold_left (fun type_env top >

395

match top.top_decl_desc with

396

 Node nd >

397

(* Format.eprintf "Registeing node %s@." nd.node_id; *)

398

let vars = nd.node_inputs @ nd.node_outputs @ nd.node_locals in

399

let constrained_vars = register_node nd.node_id vars nd.node_annot in

400

check_node nd constrained_vars;

401


402

(* Computing the node type *)

403

let ty_ins = type_of_vlist nd.node_inputs in

404

let ty_outs = type_of_vlist nd.node_outputs in

405

let ty_node = MTypes.new_ty (MTypes.Tarrow (ty_ins,ty_outs)) in

406

Typing.generalize ty_node;

407

let env = Env.add_value type_env nd.node_id ty_node in

408

(* Format.eprintf "Env: %a" (Env.pp_env MTypes.print_ty) env; *)

409

env

410


411

 _ > type_env

412

(*  ImportedNode ind > *)

413

(* let vars = ind.nodei_inputs @ ind.nodei_outputs in *)

414

(* register_node ind.nodei_id vars ind.nodei_annot *)

415

(*  _ > () TODO: shall we load something for Open statements? *)

416

) init_env prog

417

in

418

typing_env := env

419


420

let type_expr (parentid, init_vars) expr =

421

let init_env = !typing_env in

422

(* Format.eprintf "Init env: %a@." (Env.pp_env MTypes.print_ty) init_env; *)

423

(* Rebuilding the variables environment from accumulated knowledge *)

424

let env,vars = (* First, we add non specified variables *)

425

List.fold_left (fun (env, vars) v >

426

if not (is_specified v) then

427

let env = Env.add_value env v.var_id (ConvTypes.import v.var_type) in

428

env, v::vars

429

else

430

env, vars

431

) (init_env, []) init_vars

432

in

433


434

(* Then declared ones *)

435

let env, vars =

436

Hashtbl.fold (fun vdecl machine_type (env, vds) >

437

if vdecl.var_parent_nodeid = Some parentid then (

438

(* Format.eprintf "Adding variable %a to the environement@.@?" Printers.pp_var vdecl; *)

439

let env = Env.add_value env vdecl.var_id machine_type in

440

env, vdecl::vds

441

)

442

else

443

env, vds

444

) machine_type_table (env, vars)

445

in

446


447


448

(* Format.eprintf "env with local vars: %a@." (Env.pp_env MTypes.print_ty) env; *)

449

(* Format.eprintf "expr = %a@." Printers.pp_expr expr; *)

450

(* let res = *)

451

Typing.type_expr

452

(env,vars)

453

false (* not in main node *)

454

false (* no a constant *)

455

expr

456

(* in *)

457

(* Format.eprintf "typing ok = %a@." MTypes.print_ty res; *)

458

(* res *)

459


460

(* Typing the expression (vars = expr) in node

461


462

*)

463

let type_def node vars expr =

464

(* Format.eprintf "Typing def %a = %a@.@." *)

465

(* (Utils.fprintf_list ~sep:", " Printers.pp_var) vars *)

466

(* Printers.pp_expr expr *)

467

(* ; *)

468

let typ = type_expr node expr in

469

(* Format.eprintf "Type is %a. Saving stuff@.@." MTypes.print_ty typ; *)

470

let typ = MTypes.type_list_of_type typ in

471

List.iter2 register_var vars typ

472


473

let has_machine_type () =

474

let annl = Annotations.get_expr_annotations keyword in

475

(* Format.eprintf "has _mchine _type annotations: %i@." (List.length annl); *)

476

List.length annl > 0

477


478

(* Local Variables: *)

479

(* compilecommand:"make C ../.." *)

480

(* End: *)

481

