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  early

10

stage: limited typing, ie validity of operation are checked  a first version

11

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

12

uint8 is a valid subtype of int  a future implementation could ensures that

13

operations are valid  each standard or unspecified operation should be

14

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

15

real: op: t > t > t  specific nodes that explicitely defined subtypes

16

could be used to perform casts eg. a int2uint8 (i: int) returns (j: int) with

17

annotations specifying i as int and j as uint8  C backend: any print of a

18

typed variable should rely on the actual machine type when provided  EMF

19

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

20

the machine type or implement the cycling behavior for integer subtypes 

21

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

22

also imagine that results of the analysis could specify or substitute a type

23

by a subtype. Eg. the analysis detects that a float32 is enough for variable

24

z and the annotation is added to the node.

25


26

A posisble behavior could be  an option to ensure type checking  dedicated

27

conversion functions that, in C, would generate cast or calls to simple

28

identity functions (to be inlined)

29


30

TODO EMF: rajouter les memoires dans les caracteristiques du node gerer les

31

types plus finement: propager les types machines aux variables fraiches

32

creees par la normalisation *)

33

open Lustre_types

34


35

let is_active = false

36


37

let keyword = [ "machine_types" ]

38


39

module MT = struct

40

type int_typ =

41

 Tint8_t

42

 Tint16_t

43

 Tint32_t

44

 Tint64_t

45

 Tuint8_t

46

 Tuint16_t

47

 Tuint32_t

48

 Tuint64_t

49


50

let pp_int fmt t =

51

match t with

52

 Tint8_t >

53

Format.fprintf fmt "int8"

54

 Tint16_t >

55

Format.fprintf fmt "int16"

56

 Tint32_t >

57

Format.fprintf fmt "int32"

58

 Tint64_t >

59

Format.fprintf fmt "int64"

60

 Tuint8_t >

61

Format.fprintf fmt "uint8"

62

 Tuint16_t >

63

Format.fprintf fmt "uint16"

64

 Tuint32_t >

65

Format.fprintf fmt "uint32"

66

 Tuint64_t >

67

Format.fprintf fmt "uint64"

68


69

let pp_c_int fmt t =

70

match t with

71

 Tint8_t >

72

Format.fprintf fmt "int8_t"

73

 Tint16_t >

74

Format.fprintf fmt "int16_t"

75

 Tint32_t >

76

Format.fprintf fmt "int32_t"

77

 Tint64_t >

78

Format.fprintf fmt "int64_t"

79

 Tuint8_t >

80

Format.fprintf fmt "uint8_t"

81

 Tuint16_t >

82

Format.fprintf fmt "uint16_t"

83

 Tuint32_t >

84

Format.fprintf fmt "uint32_t"

85

 Tuint64_t >

86

Format.fprintf fmt "uint64_t"

87


88

type t =

89

 MTint of int_typ option

90

 MTreal of string option

91

 MTbool

92

 MTstring

93


94

open Format

95


96

let pp fmt t =

97

match t with

98

 MTint None >

99

fprintf fmt "int"

100

 MTint (Some s) >

101

fprintf fmt "%a" pp_int s

102

 MTreal None >

103

fprintf fmt "real"

104

 MTreal (Some s) >

105

fprintf fmt "%s" s

106

 MTbool >

107

fprintf fmt "bool"

108

 MTstring >

109

fprintf fmt "string"

110


111

let pp_c fmt t =

112

match t with

113

 MTint (Some s) >

114

fprintf fmt "%a" pp_c_int s

115

 MTreal (Some s) >

116

fprintf fmt "%s" s

117

 MTint None  MTreal None  MTbool  MTstring >

118

assert false

119


120

let is_scalar_type t =

121

match t with MTbool  MTint _  MTreal _ > true  _ > false

122


123

let is_numeric_type t = match t with MTint _  MTreal _ > true  _ > false

124


125

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

126


127

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

128


129

let is_bool_type t = t = MTbool

130


131

let is_dimension_type t = match t with MTint _  MTbool > true  _ > false

132


133

let type_int_builder = MTint None

134


135

let type_real_builder = MTreal None

136


137

let type_bool_builder = MTbool

138


139

let type_string_builder = MTstring

140


141

let unify _ _ = ()

142


143

let is_unifiable b1 b2 =

144

match b1, b2 with

145

 MTint _, MTint _

146

 MTreal _, MTreal _

147

 MTstring, MTstring

148

 MTbool, MTbool >

149

true

150

 _ >

151

false

152


153

let is_exportable b =

154

match b with

155

 MTstring  MTbool  MTreal None  MTint None >

156

false

157

 _ >

158

true

159

end

160


161

module MTypes = Types.Make (MT)

162


163

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

164


165

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

166


167

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

168


169

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

170


171

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

172


173

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

174


175

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

176


177

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

178


179

module ConvTypes = struct

180

type type_expr = MTypes.type_expr

181


182

let map_type_basic f_basic =

183

let rec map_type_basic e =

184

{

185

MTypes.tid = e.Types.tid;

186

MTypes.tdesc = map_type_basic_desc (Types.type_desc e);

187

}

188

and map_type_basic_desc td =

189

let mape = map_type_basic in

190

match td with

191

 Types.Tbasic b >

192

f_basic b

193

 Types.Tconst c >

194

MTypes.Tconst c

195

 Types.Tenum e >

196

MTypes.Tenum e

197

 Types.Tvar >

198

MTypes.Tvar

199

 Types.Tunivar >

200

MTypes.Tunivar

201

 Types.Tclock te >

202

MTypes.Tclock (mape te)

203

 Types.Tarrow (te1, te2) >

204

MTypes.Tarrow (mape te1, mape te2)

205

 Types.Ttuple tel >

206

MTypes.Ttuple (List.map mape tel)

207

 Types.Tstruct id_te_l >

208

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

209

 Types.Tarray (de, te) >

210

MTypes.Tarray (de, mape te)

211

 Types.Tstatic (de, te) >

212

MTypes.Tstatic (de, mape te)

213

 Types.Tlink te >

214

MTypes.Tlink (mape te)

215

in

216

map_type_basic

217


218

let import main_typ =

219

let import_basic b =

220

if Types.BasicT.is_int_type b then MTypes.type_int

221

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

222

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

223

else (

224

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

225

assert false)

226

in

227

map_type_basic import_basic main_typ

228


229

let map_mtype_basic f_basic =

230

let rec map_mtype_basic e =

231

{

232

Types.tid = e.MTypes.tid;

233

Types.tdesc = map_mtype_basic_desc (MTypes.type_desc e);

234

}

235

and map_mtype_basic_desc td =

236

let mape = map_mtype_basic in

237

match td with

238

 MTypes.Tbasic b >

239

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

240

f_basic b

241

 MTypes.Tconst c >

242

Types.Tconst c

243

 MTypes.Tenum e >

244

Types.Tenum e

245

 MTypes.Tvar >

246

Types.Tvar

247

 MTypes.Tunivar >

248

Types.Tunivar

249

 MTypes.Tclock te >

250

Types.Tclock (mape te)

251

 MTypes.Tarrow (te1, te2) >

252

Types.Tarrow (mape te1, mape te2)

253

 MTypes.Ttuple tel >

254

Types.Ttuple (List.map mape tel)

255

 MTypes.Tstruct id_te_l >

256

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

257

 MTypes.Tarray (de, te) >

258

Types.Tarray (de, mape te)

259

 MTypes.Tstatic (de, te) >

260

Types.Tstatic (de, mape te)

261

 MTypes.Tlink te >

262

Types.Tlink (mape te)

263

in

264

map_mtype_basic

265


266

let export machine_type =

267

let export_basic b =

268

if MTypes.BasicT.is_int_type b then Types.type_int

269

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

270

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

271

else (

272

Format.eprintf

273

"unhandled basic mtype is %a. Issues while dealing with basic type \

274

%a@.@?"

275

MTypes.print_ty machine_type MTypes.BasicT.pp b;

276

assert false)

277

in

278

map_mtype_basic export_basic machine_type

279

end

280


281

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

282


283

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

284

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

285

Hashtbl.create 13

286


287

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

288

let typing_env = ref Env.initial

289


290

let is_specified v =

291

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

292

Hashtbl.mem machine_type_table v

293


294

let pp_table fmt =

295

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

296

Hashtbl.iter

297

(fun v typ >

298

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

299

machine_type_table;

300

Format.fprintf fmt "@]"

301


302

let get_specified_type v =

303

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

304

(* Printers.pp_var v *)

305

(* pp_table; *)

306

Hashtbl.find machine_type_table v

307


308

let is_exportable v =

309

is_specified v

310

&&

311

let typ = get_specified_type v in

312

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

313

 MTypes.Tbasic b >

314

MT.is_exportable b

315

 MTypes.Tconst _ >

316

false (* Enumerated types are not "machine type" customizeable *)

317

 _ >

318

assert false

319


320

(* TODO deal with other constructs *)

321

(* could depend on the actual computed type *)

322


323

let type_name typ =

324

MTypes.print_ty Format.str_formatter typ;

325

Format.flush_str_formatter ()

326


327

let pp_var_type fmt v =

328

let typ = get_specified_type v in

329

MTypes.print_ty fmt typ

330


331

let pp_c_var_type fmt v =

332

let typ = get_specified_type v in

333

MTypes.print_ty_param MT.pp_c fmt typ

334


335

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

336


337

let erroneous_annotation loc =

338

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

339

Location.pp_loc loc;

340

assert false

341


342

let valid_subtype subtype typ =

343

let mismatch subtyp typ =

344

Format.eprintf "Subtype mismatch %a vs %a@." MTypes.print_ty subtyp

345

Types.print_ty typ;

346

false

347

in

348

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

349

 MTypes.Tconst c >

350

Types.is_const_type typ c

351

 MTypes.Tbasic (MT.MTint _) >

352

Types.is_int_type typ

353

 MTypes.Tbasic (MT.MTreal _) >

354

Types.is_real_type typ

355

 MTypes.Tbasic MT.MTbool >

356

Types.is_bool_type typ

357

 _ >

358

mismatch subtype typ

359


360

let type_of_name name =

361

match name with

362

 "uint8" >

363

type_uint8

364

 "uint16" >

365

type_uint16

366

 "uint32" >

367

type_uint32

368

 "uint64" >

369

type_uint64

370

 "int8" >

371

type_int8

372

 "int16" >

373

type_int16

374

 "int32" >

375

type_int32

376

 "int64" >

377

type_int64

378

 _ >

379

assert false

380

(* unknown custom machine type *)

381


382

let register_var var typ =

383

(* let typ = type_of_name type_name in *)

384

if valid_subtype typ var.var_type then Hashtbl.add machine_type_table var typ

385

else erroneous_annotation var.var_loc

386


387

(* let register_var_opt var type_name_opt = *)

388

(* match type_name_opt with *)

389

(*  None > () *)

390

(*  Some type_name > register_var var type_name *)

391


392

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

393


394

let register_node vars annots =

395

List.fold_left

396

(fun accu annot >

397

let annl = annot.annots in

398

List.fold_left

399

(fun accu (kwd, value) >

400

if kwd = keyword then

401

let expr = value.eexpr_qfexpr in

402

match Corelang.expr_list_of_expr expr with

403

 [ var_id; type_name ] > (

404

match var_id.expr_desc, type_name.expr_desc with

405

 Expr_ident var_id, Expr_const (Const_string type_name) >

406

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

407

Log.report ~level:2 (fun fmt >

408

Format.fprintf fmt

409

"Recorded type %s for variable %a (parent node is %s)@ "

410

type_name Printers.pp_var var

411

(match var.var_parent_nodeid with

412

 Some id >

413

id

414

 None >

415

"unknown"));

416

let typ = type_of_name type_name in

417

register_var var typ;

418

var :: accu

419

 _ >

420

erroneous_annotation expr.expr_loc)

421

 _ >

422

erroneous_annotation expr.expr_loc

423

else accu)

424

accu annl)

425

[] annots

426


427

let check_node nd vars =

428

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

429

()

430


431

let type_of_vlist vars =

432

let tyl =

433

List.map

434

(fun v >

435

if is_specified v then get_specified_type v

436

else ConvTypes.import v.var_type)

437

vars

438

in

439

MTypes.type_of_type_list tyl

440


441

let load prog =

442

let init_env =

443

Env.fold

444

(fun id typ env > Env.add_value env id (ConvTypes.import typ))

445

Basic_library.type_env Env.initial

446

in

447

let env =

448

List.fold_left

449

(fun type_env top >

450

match top.top_decl_desc with

451

 Node nd >

452

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

453

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

454

let constrained_vars = register_node vars nd.node_annot in

455

check_node nd constrained_vars;

456


457

(* Computing the node type *)

458

let ty_ins = type_of_vlist nd.node_inputs in

459

let ty_outs = type_of_vlist nd.node_outputs in

460

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

461

Typing.generalize ty_node;

462

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

463

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

464

env

465

 _ >

466

type_env

467

(*  ImportedNode ind > *)

468

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

469

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

470

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

471

init_env prog

472

in

473

typing_env := env

474


475

let type_expr (parentid, init_vars) expr =

476

let init_env = !typing_env in

477

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

478

(* Rebuilding the variables environment from accumulated knowledge *)

479

let env, vars =

480

(* First, we add non specified variables *)

481

List.fold_left

482

(fun (env, vars) v >

483

if not (is_specified v) then

484

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

485

env, v :: vars

486

else env, vars)

487

(init_env, []) init_vars

488

in

489


490

(* Then declared ones *)

491

let env, vars =

492

Hashtbl.fold

493

(fun vdecl machine_type (env, vds) >

494

if vdecl.var_parent_nodeid = Some parentid then

495

(* Format.eprintf "Adding variable %a to the environement@.@?"

496

Printers.pp_var vdecl; *)

497

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

498

env, vdecl :: vds

499

else env, vds)

500

machine_type_table (env, vars)

501

in

502


503

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

504

env; *)

505

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

506

(* let res = *)

507

Typing.type_expr (env, vars) false (* not in main node *) false

508

(* no a constant *) expr

509


510

(* in *)

511

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

512

(* res *)

513


514

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

515

let type_def node vars expr =

516

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

517

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

518

(* Printers.pp_expr expr *)

519

(* ; *)

520

let typ = type_expr node expr in

521

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

522

let typ = MTypes.type_list_of_type typ in

523

List.iter2 register_var vars typ

524


525

let has_machine_type () =

526

let annl = Annotations.get_expr_annotations keyword in

527

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

528

List.length annl > 0

529


530

(* Local Variables: *)

531

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

532

(* End: *)
