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 Utils

13

open Lustre_types

14

open Machine_code_types

15

open Corelang

16

open Normalization

17

open Machine_code_common

18


19

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

20

let cpt_fresh = ref 0

21


22

let mpfr_rnd () = "MPFR_RNDN"

23


24

let mpfr_prec () = !Options.mpfr_prec

25


26

let inject_id = "MPFRId"

27


28

let inject_copy_id = "mpfr_set"

29


30

let inject_real_id = "mpfr_set_flt"

31


32

let inject_init_id = "mpfr_init2"

33


34

let inject_clear_id = "mpfr_clear"

35


36

let mpfr_t = "mpfr_t"

37


38

let unfoldable_value value =

39

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

40


41

let inject_id_id expr =

42

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

43

{ e with

44

expr_type = Type_predef.type_real;

45

expr_clock = expr.expr_clock;

46

}

47


48

let pp_inject_real pp_var pp_val fmt var value =

49

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

50

inject_real_id

51

pp_var var

52

pp_val value

53

(mpfr_rnd ())

54


55

let inject_assign expr =

56

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

57

{ e with

58

expr_type = Type_predef.type_real;

59

expr_clock = expr.expr_clock;

60

}

61


62

let pp_inject_copy pp_var fmt var value =

63

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

64

inject_copy_id

65

pp_var var

66

pp_var value

67

(mpfr_rnd ())

68


69

let rec pp_inject_assign pp_var fmt var value =

70

if is_const_value value

71

then

72

pp_inject_real pp_var pp_var fmt var value

73

else

74

pp_inject_copy pp_var fmt var value

75


76

let pp_inject_init pp_var fmt var =

77

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

78

inject_init_id

79

pp_var var

80

(mpfr_prec ())

81


82

let pp_inject_clear pp_var fmt var =

83

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

84

inject_clear_id

85

pp_var var

86


87

let base_inject_op id =

88

match id with

89

 "+" > "MPFRPlus"

90

 "" > "MPFRMinus"

91

 "*" > "MPFRTimes"

92

 "/" > "MPFRDiv"

93

 "uminus" > "MPFRUminus"

94

 "<=" > "MPFRLe"

95

 "<" > "MPFRLt"

96

 ">=" > "MPFRGe"

97

 ">" > "MPFRGt"

98

 "=" > "MPFREq"

99

 "!=" > "MPFRNeq"

100

 _ > raise Not_found

101


102

let inject_op id =

103

try

104

base_inject_op id

105

with Not_found > id

106


107

let homomorphic_funs =

108

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

109


110

let is_homomorphic_fun id =

111

List.mem id homomorphic_funs

112


113

let inject_call expr =

114

match expr.expr_desc with

115

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

116

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

117

 _ > expr

118


119

let expr_of_const_array expr =

120

match expr.expr_desc with

121

 Expr_const (Const_array cl) >

122

let typ = Types.array_element_type expr.expr_type in

123

let expr_of_const c =

124

{ expr_desc = Expr_const c;

125

expr_type = typ;

126

expr_clock = expr.expr_clock;

127

expr_loc = expr.expr_loc;

128

expr_delay = Delay.new_var ();

129

expr_annot = None;

130

expr_tag = new_tag ();

131

}

132

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

133

 _ > assert false

134


135

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

136

let rec inject_list alias node inject_element defvars elist =

137

List.fold_right

138

(fun t (defvars, qlist) >

139

let defvars, norm_t = inject_element alias node defvars t in

140

(defvars, norm_t :: qlist)

141

) elist (defvars, [])

142


143

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

144

let res =

145

match expr.expr_desc with

146

 Expr_const (Const_real _) > mk_expr_alias_opt alias node defvars expr

147

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

148

 Expr_const (Const_struct _) > assert false

149

 Expr_ident _

150

 Expr_const _ > defvars, expr

151

 Expr_array elist >

152

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

153

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

154

defvars, norm_expr

155

 Expr_power (e1, d) >

156

let defvars, norm_e1 = inject_expr node defvars e1 in

157

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

158

defvars, norm_expr

159

 Expr_access (e1, d) >

160

let defvars, norm_e1 = inject_expr node defvars e1 in

161

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

162

defvars, norm_expr

163

 Expr_tuple elist >

164

let defvars, norm_elist =

165

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

166

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

167

defvars, norm_expr

168

 Expr_appl (id, args, r) >

169

let defvars, norm_args = inject_expr node defvars args in

170

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

171

mk_expr_alias_opt alias node defvars (inject_call norm_expr)

172

 Expr_arrow _ > defvars, expr

173

 Expr_pre e >

174

let defvars, norm_e = inject_expr node defvars e in

175

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

176

defvars, norm_expr

177

 Expr_fby (e1, e2) >

178

let defvars, norm_e1 = inject_expr node defvars e1 in

179

let defvars, norm_e2 = inject_expr node defvars e2 in

180

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

181

defvars, norm_expr

182

 Expr_when (e, c, l) >

183

let defvars, norm_e = inject_expr node defvars e in

184

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

185

defvars, norm_expr

186

 Expr_ite (c, t, e) >

187

let defvars, norm_c = inject_expr node defvars c in

188

let defvars, norm_t = inject_expr node defvars t in

189

let defvars, norm_e = inject_expr node defvars e in

190

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

191

defvars, norm_expr

192

 Expr_merge (c, hl) >

193

let defvars, norm_hl = inject_branches node defvars hl in

194

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

195

defvars, norm_expr

196

in

197

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

198

res

199


200

and inject_branches node defvars hl =

201

List.fold_right

202

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

203

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

204

defvars, (t, norm_h) :: norm_q

205

)

206

hl (defvars, [])

207


208


209

let rec inject_eq node defvars eq =

210

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

211

let norm_eq = { eq with eq_rhs = norm_rhs } in

212

norm_eq::defs', vars'

213


214

(** normalize_node node returns a normalized node,

215

ie.

216

 updated locals

217

 new equations

218



219

*)

220

let inject_node node =

221

cpt_fresh := 0;

222

let inputs_outputs = node.node_inputs@node.node_outputs in

223

let is_local v =

224

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

225

let orig_vars = inputs_outputs@node.node_locals in

226

let defs, vars =

227

let eqs, auts = get_node_eqs node in

228

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

229

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

230

(* Normalize the asserts *)

231

let vars, assert_defs, asserts =

232

List.fold_left (

233

fun (vars, def_accu, assert_accu) assert_ >

234

let assert_expr = assert_.assert_expr in

235

let (defs, vars'), expr =

236

inject_expr

237

~alias:false

238

node

239

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

240

assert_expr

241

in

242

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

243

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

244

let new_locals = List.filter is_local vars in

245

(* Compute traceability info:

246

 gather newly bound variables

247

 compute the associated expression without aliases

248

*)

249

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

250

let node =

251

{ node with

252

node_locals = new_locals;

253

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

254

}

255

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

256


257

let inject_decl decl =

258

match decl.top_decl_desc with

259

 Node nd >

260

{decl with top_decl_desc = Node (inject_node nd)}

261

 Open _  ImportedNode _  Const _  TypeDef _ > decl

262


263

let inject_prog decls =

264

List.map inject_decl decls

265


266


267

(* Local Variables: *)

268

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

269

(* End: *)
