1

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

2

(* *)

3

(* The LustreC compiler toolset / The LustreC Development Team *)

4

(* Copyright 2012   ONERA  CNRS  INPT *)

5

(* *)

6

(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)

7

(* under the terms of the GNU Lesser General Public License *)

8

(* version 2.1. *)

9

(* *)

10

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

11


12

open Lustrec.Utils

13

open Lustrec.Lustre_types

14

open Lustrec.Machine_code_types

15

open Lustrec.Corelang

16

open Lustrec.Normalization

17

open Lustrec.Machine_code_common

18


19

let report = Lustrec.Log.report ~plugin:"MPFR"

20


21

let mpfr_module = mktop (Open(false, "mpfr_lustre"))

22

let cpt_fresh = ref 0

23


24

let mpfr_rnd () = "MPFR_RNDN"

25


26

let mpfr_prec () = !Lustrec.Options.mpfr_prec

27


28

let inject_id = "MPFRId"

29


30

let inject_copy_id = "mpfr_set"

31


32

let inject_real_id = "mpfr_set_flt"

33


34

let inject_init_id = "mpfr_init2"

35


36

let inject_clear_id = "mpfr_clear"

37


38

let mpfr_t = "mpfr_t"

39


40

let unfoldable_value value =

41

not (Lustrec.Types.is_real_type value.value_type && is_const_value value)

42


43

let inject_id_id expr =

44

let e = mkpredef_call expr.expr_loc inject_id [expr] in

45

{ e with

46

expr_type = Lustrec.Type_predef.type_real;

47

expr_clock = expr.expr_clock;

48

}

49


50

let pp_inject_real pp_var pp_val fmt var value =

51

Format.fprintf fmt "%s(%a, %a, %s);"

52

inject_real_id

53

pp_var var

54

pp_val value

55

(mpfr_rnd ())

56


57

let inject_assign expr =

58

let e = mkpredef_call expr.expr_loc inject_copy_id [expr] in

59

{ e with

60

expr_type = Lustrec.Type_predef.type_real;

61

expr_clock = expr.expr_clock;

62

}

63


64

let pp_inject_copy pp_var fmt var value =

65

Format.fprintf fmt "%s(%a, %a, %s);"

66

inject_copy_id

67

pp_var var

68

pp_var value

69

(mpfr_rnd ())

70


71

let rec pp_inject_assign pp_var fmt var value =

72

if is_const_value value

73

then

74

pp_inject_real pp_var pp_var fmt var value

75

else

76

pp_inject_copy pp_var fmt var value

77


78

let pp_inject_init pp_var fmt var =

79

Format.fprintf fmt "%s(%a, %i);"

80

inject_init_id

81

pp_var var

82

(mpfr_prec ())

83


84

let pp_inject_clear pp_var fmt var =

85

Format.fprintf fmt "%s(%a);"

86

inject_clear_id

87

pp_var var

88


89

let base_inject_op id =

90

match id with

91

 "+" > "MPFRPlus"

92

 "" > "MPFRMinus"

93

 "*" > "MPFRTimes"

94

 "/" > "MPFRDiv"

95

 "uminus" > "MPFRUminus"

96

 "<=" > "MPFRLe"

97

 "<" > "MPFRLt"

98

 ">=" > "MPFRGe"

99

 ">" > "MPFRGt"

100

 "=" > "MPFREq"

101

 "!=" > "MPFRNeq"

102

(* Conv functions *)

103

 "int_to_real" > "MPFRint_to_real"

104

 "real_to_int" > "MPFRreal_to_int"

105

 "_floor" > "MPFRfloor"

106

 "_ceil" > "MPFRceil"

107

 "_round" > "MPFRround"

108

 "_Floor" > "MPFRFloor"

109

 "_Ceiling" > "MPFRCeiling"

110

 "_Round" > "MPFRRound"

111


112

(* Math library functions *)

113

 "acos" > "MPFRacos"

114

 "acosh" > "MPFRacosh"

115

 "asin" > "MPFRasin"

116

 "asinh" > "MPFRasinh"

117

 "atan" > "MPFRatan"

118

 "atan2" > "MPFRatan2"

119

 "atanh" > "MPFRatanh"

120

 "cbrt" > "MPFRcbrt"

121

 "cos" > "MPFRcos"

122

 "cosh" > "MPFRcosh"

123

 "ceil" > "MPFRceil"

124

 "erf" > "MPFRerf"

125

 "exp" > "MPFRexp"

126

 "fabs" > "MPFRfabs"

127

 "floor" > "MPFRfloor"

128

 "fmod" > "MPFRfmod"

129

 "log" > "MPFRlog"

130

 "log10" > "MPFRlog10"

131

 "pow" > "MPFRpow"

132

 "round" > "MPFRround"

133

 "sin" > "MPFRsin"

134

 "sinh" > "MPFRsinh"

135

 "sqrt" > "MPFRsqrt"

136

 "trunc" > "MPFRtrunc"

137

 "tan" > "MPFRtan"

138

 _ > raise Not_found

139


140

let inject_op id =

141

report ~level:3 (fun fmt > Format.fprintf fmt "trying to inject mpfr into function %s@." id);

142

try

143

base_inject_op id

144

with Not_found > id

145


146

let homomorphic_funs =

147

List.fold_right (fun id res > try base_inject_op id :: res with Not_found > res) Lustrec.Basic_library.internal_funs []

148


149

let is_homomorphic_fun id =

150

List.mem id homomorphic_funs

151


152

let inject_call expr =

153

match expr.expr_desc with

154

 Expr_appl (id, args, None) when not (Lustrec.Basic_library.is_expr_internal_fun expr) >

155

{ expr with expr_desc = Expr_appl (inject_op id, args, None) }

156

 _ > expr

157


158

let expr_of_const_array expr =

159

match expr.expr_desc with

160

 Expr_const (Const_array cl) >

161

let typ = Lustrec.Types.array_element_type expr.expr_type in

162

let expr_of_const c =

163

{ expr_desc = Expr_const c;

164

expr_type = typ;

165

expr_clock = expr.expr_clock;

166

expr_loc = expr.expr_loc;

167

expr_delay = Lustrec.Delay.new_var ();

168

expr_annot = None;

169

expr_tag = new_tag ();

170

}

171

in { expr with expr_desc = Expr_array (List.map expr_of_const cl) }

172

 _ > assert false

173


174

(* inject_<foo> : defs * used vars > <foo> > (updated defs * updated vars) * normalized <foo> *)

175

let rec inject_list alias node inject_element defvars elist =

176

List.fold_right

177

(fun t (defvars, qlist) >

178

let defvars, norm_t = inject_element alias node defvars t in

179

(defvars, norm_t :: qlist)

180

) elist (defvars, [])

181


182

let rec inject_expr ?(alias=true) node defvars expr =

183

let res =

184

match expr.expr_desc with

185

 Expr_const (Const_real _) > mk_expr_alias_opt alias node defvars expr

186

 Expr_const (Const_array _) > inject_expr ~alias:alias node defvars (expr_of_const_array expr)

187

 Expr_const (Const_struct _) > assert false

188

 Expr_ident _

189

 Expr_const _ > defvars, expr

190

 Expr_array elist >

191

let defvars, norm_elist = inject_list alias node (fun _ > inject_expr ~alias:true) defvars elist in

192

let norm_expr = { expr with expr_desc = Expr_array norm_elist } in

193

defvars, norm_expr

194

 Expr_power (e1, d) >

195

let defvars, norm_e1 = inject_expr node defvars e1 in

196

let norm_expr = { expr with expr_desc = Expr_power (norm_e1, d) } in

197

defvars, norm_expr

198

 Expr_access (e1, d) >

199

let defvars, norm_e1 = inject_expr node defvars e1 in

200

let norm_expr = { expr with expr_desc = Expr_access (norm_e1, d) } in

201

defvars, norm_expr

202

 Expr_tuple elist >

203

let defvars, norm_elist =

204

inject_list alias node (fun alias > inject_expr ~alias:alias) defvars elist in

205

let norm_expr = { expr with expr_desc = Expr_tuple norm_elist } in

206

defvars, norm_expr

207

 Expr_appl (id, args, r) >

208

let defvars, norm_args = inject_expr node defvars args in

209

let norm_expr = { expr with expr_desc = Expr_appl (id, norm_args, r) } in

210

mk_expr_alias_opt alias node defvars (inject_call norm_expr)

211

 Expr_arrow _ > defvars, expr

212

 Expr_pre e >

213

let defvars, norm_e = inject_expr node defvars e in

214

let norm_expr = { expr with expr_desc = Expr_pre norm_e } in

215

defvars, norm_expr

216

 Expr_fby (e1, e2) >

217

let defvars, norm_e1 = inject_expr node defvars e1 in

218

let defvars, norm_e2 = inject_expr node defvars e2 in

219

let norm_expr = { expr with expr_desc = Expr_fby (norm_e1, norm_e2) } in

220

defvars, norm_expr

221

 Expr_when (e, c, l) >

222

let defvars, norm_e = inject_expr node defvars e in

223

let norm_expr = { expr with expr_desc = Expr_when (norm_e, c, l) } in

224

defvars, norm_expr

225

 Expr_ite (c, t, e) >

226

let defvars, norm_c = inject_expr node defvars c in

227

let defvars, norm_t = inject_expr node defvars t in

228

let defvars, norm_e = inject_expr node defvars e in

229

let norm_expr = { expr with expr_desc = Expr_ite (norm_c, norm_t, norm_e) } in

230

defvars, norm_expr

231

 Expr_merge (c, hl) >

232

let defvars, norm_hl = inject_branches node defvars hl in

233

let norm_expr = { expr with expr_desc = Expr_merge (c, norm_hl) } in

234

defvars, norm_expr

235

in

236

(*Format.eprintf "inject_expr %B %a = %a@." alias Lustrec.Printers.pp_expr expr Lustrec.Printers.pp_expr (snd res);*)

237

res

238


239

and inject_branches node defvars hl =

240

List.fold_right

241

(fun (t, h) (defvars, norm_q) >

242

let (defvars, norm_h) = inject_expr node defvars h in

243

defvars, (t, norm_h) :: norm_q

244

)

245

hl (defvars, [])

246


247


248

let rec inject_eq node defvars eq =

249

let (defs', vars'), norm_rhs = inject_expr ~alias:false node defvars eq.eq_rhs in

250

let norm_eq = { eq with eq_rhs = norm_rhs } in

251

norm_eq::defs', vars'

252


253

(* let inject_eexpr ee =

254

* { ee with eexpr_qfexpr = inject_expr ee.eexpr_qfexpr }

255

*

256

* let inject_spec s =

257

* { s with

258

* assume = List.map inject_eexpr s.assume;

259

* guarantees = List.map inject_eexpr s.guarantees;

260

* modes = List.map (fun m >

261

* { m with

262

* require = List.map inject_eexpr m.require;

263

* ensure = List.map inject_eexpr m.ensure

264

* }

265

* ) s.modes

266

* } *)

267


268

(** normalize_node node returns a normalized node,

269

ie.

270

 updated locals

271

 new equations

272



273

*)

274

let inject_node node =

275

cpt_fresh := 0;

276

let inputs_outputs = node.node_inputs@node.node_outputs in

277

let norm_ctx = (node.node_id, get_node_vars node) in

278

let is_local v =

279

List.for_all ((!=) v) inputs_outputs in

280

let orig_vars = inputs_outputs@node.node_locals in

281

let defs, vars =

282

let eqs, auts = get_node_eqs node in

283

if auts != [] then assert false; (* Lustrec.Automata should be expanded by now. *)

284

List.fold_left (inject_eq norm_ctx) ([], orig_vars) eqs in

285

(* Normalize the asserts *)

286

let vars, assert_defs, asserts =

287

List.fold_left (

288

fun (vars, def_accu, assert_accu) assert_ >

289

let assert_expr = assert_.assert_expr in

290

let (defs, vars'), expr =

291

inject_expr

292

~alias:false

293

norm_ctx

294

([], vars) (* defvar only contains vars *)

295

assert_expr

296

in

297

vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu

298

) (vars, [], []) node.node_asserts in

299

let new_locals = List.filter is_local vars in

300

(* Compute traceability info:

301

 gather newly bound variables

302

 compute the associated expression without aliases

303

*)

304

(* let diff_vars = List.filter (fun v > not (List.mem v node.node_locals)) new_locals in *)

305

(* See comment below

306

* let spec = match node.node_spec with

307

*  None > None

308

*  Some spec > Some (inject_spec spec)

309

* in *)

310

let node =

311

{ node with

312

node_locals = new_locals;

313

node_stmts = List.map (fun eq > Eq eq) (defs @ assert_defs);

314

(* Incomplete work: TODO. Do we have to inject MPFR code here?

315

Does it make sense for annotations? For me, only if we produce

316

C code for annotations. Otherwise the various verification

317

backend should have their own understanding, but would not

318

necessarily require this additional normalization. *)

319

(*

320

node_spec = spec;

321

node_annot = List.map (fun ann > {ann with

322

annots = List.map (fun (ids, ee) > ids, inject_eexpr ee) ann.annots}

323

) node.node_annot *)

324

}

325

in ((*Lustrec.Printers.pp_node Format.err_formatter node;*) node)

326


327

let inject_decl decl =

328

match decl.top_decl_desc with

329

 Node nd >

330

{decl with top_decl_desc = Node (inject_node nd)}

331

 Include _  Open _  ImportedNode _  Const _  TypeDef _ > decl

332


333

let inject_prog decls =

334

List.map inject_decl decls

335


336


337

(* Local Variables: *)

338

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

339

(* End: *)
