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 LustreSpec

14

open Corelang

15

open Normalization

16

open Machine_code

17


18

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

19


20

let mpfr_rnd () = "MPFR_RNDN"

21


22

let mpfr_prec () = !Options.mpfr_prec

23


24

let inject_id = "MPFRId"

25


26

let inject_copy_id = "mpfr_set"

27


28

let inject_real_id = "mpfr_set_flt"

29


30

let inject_init_id = "mpfr_init2"

31


32

let inject_clear_id = "mpfr_clear"

33


34

let mpfr_t = "mpfr_t"

35


36

let unfoldable_value value =

37

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

38


39

let inject_id_id expr =

40

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

41

{ e with

42

expr_type = Type_predef.type_real;

43

expr_clock = expr.expr_clock;

44

}

45


46

let pp_inject_real pp_var pp_val fmt var value =

47

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

48

inject_real_id

49

pp_var var

50

pp_val value

51

(mpfr_rnd ())

52


53

let inject_assign expr =

54

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

55

{ e with

56

expr_type = Type_predef.type_real;

57

expr_clock = expr.expr_clock;

58

}

59


60

let pp_inject_copy pp_var fmt var value =

61

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

62

inject_copy_id

63

pp_var var

64

pp_var value

65

(mpfr_rnd ())

66


67

let rec pp_inject_assign pp_var fmt var value =

68

if is_const_value value

69

then

70

pp_inject_real pp_var pp_var fmt var value

71

else

72

pp_inject_copy pp_var fmt var value

73


74

let pp_inject_init pp_var fmt var =

75

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

76

inject_init_id

77

pp_var var

78

(mpfr_prec ())

79


80

let pp_inject_clear pp_var fmt var =

81

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

82

inject_clear_id

83

pp_var var

84


85

let base_inject_op id =

86

match id with

87

 "+" > "MPFRPlus"

88

 "" > "MPFRMinus"

89

 "*" > "MPFRTimes"

90

 "/" > "MPFRDiv"

91

 "uminus" > "MPFRUminus"

92

 "<=" > "MPFRLe"

93

 "<" > "MPFRLt"

94

 ">=" > "MPFRGe"

95

 ">" > "MPFRGt"

96

 "=" > "MPFREq"

97

 "!=" > "MPFRNeq"

98

 _ > raise Not_found

99


100

let inject_op id =

101

try

102

base_inject_op id

103

with Not_found > id

104


105

let homomorphic_funs =

106

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

107


108

let is_homomorphic_fun id =

109

List.mem id homomorphic_funs

110


111

let inject_call expr =

112

match expr.expr_desc with

113

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

114

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

115

 _ > expr

116


117

let expr_of_const_array expr =

118

match expr.expr_desc with

119

 Expr_const (Const_array cl) >

120

let typ = Types.array_element_type expr.expr_type in

121

let expr_of_const c =

122

{ expr_desc = Expr_const c;

123

expr_type = typ;

124

expr_clock = expr.expr_clock;

125

expr_loc = expr.expr_loc;

126

expr_delay = Delay.new_var ();

127

expr_annot = None;

128

expr_tag = new_tag ();

129

}

130

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

131

 _ > assert false

132


133

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

134

let rec inject_list alias node inject_element defvars elist =

135

List.fold_right

136

(fun t (defvars, qlist) >

137

let defvars, norm_t = inject_element alias node defvars t in

138

(defvars, norm_t :: qlist)

139

) elist (defvars, [])

140


141

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

142

let res=

143

match expr.expr_desc with

144

 Expr_const (Const_real _) > mk_expr_alias_opt alias node defvars expr

145

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

146

 Expr_const (Const_struct _) > assert false

147

 Expr_ident _

148

 Expr_const _ > defvars, expr

149

 Expr_array elist >

150

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

151

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

152

defvars, norm_expr

153

 Expr_power (e1, d) >

154

let defvars, norm_e1 = inject_expr node defvars e1 in

155

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

156

defvars, norm_expr

157

 Expr_access (e1, d) >

158

let defvars, norm_e1 = inject_expr node defvars e1 in

159

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

160

defvars, norm_expr

161

 Expr_tuple elist >

162

let defvars, norm_elist =

163

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

164

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

165

defvars, norm_expr

166

 Expr_appl (id, args, r) >

167

let defvars, norm_args = inject_expr node defvars args in

168

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

169

mk_expr_alias_opt alias node defvars (inject_call norm_expr)

170

 Expr_arrow _ > defvars, expr

171

 Expr_pre e >

172

let defvars, norm_e = inject_expr node defvars e in

173

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

174

defvars, norm_expr

175

 Expr_fby (e1, e2) >

176

let defvars, norm_e1 = inject_expr node defvars e1 in

177

let defvars, norm_e2 = inject_expr node defvars e2 in

178

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

179

defvars, norm_expr

180

 Expr_when (e, c, l) >

181

let defvars, norm_e = inject_expr node defvars e in

182

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

183

defvars, norm_expr

184

 Expr_ite (c, t, e) >

185

let defvars, norm_c = inject_expr node defvars c in

186

let defvars, norm_t = inject_expr node defvars t in

187

let defvars, norm_e = inject_expr node defvars e in

188

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

189

defvars, norm_expr

190

 Expr_merge (c, hl) >

191

let defvars, norm_hl = inject_branches node defvars hl in

192

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

193

defvars, norm_expr

194

in

195

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

196

res

197


198

and inject_branches node defvars hl =

199

List.fold_right

200

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

201

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

202

defvars, (t, norm_h) :: norm_q

203

)

204

hl (defvars, [])

205


206


207

let rec inject_eq node defvars eq =

208

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

209

let norm_eq = { eq with eq_rhs = norm_rhs } in

210

norm_eq::defs', vars'

211


212

(** normalize_node node returns a normalized node,

213

ie.

214

 updated locals

215

 new equations

216



217

*)

218

let inject_node node =

219

cpt_fresh := 0;

220

let inputs_outputs = node.node_inputs@node.node_outputs in

221

let is_local v =

222

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

223

let orig_vars = inputs_outputs@node.node_locals in

224

let defs, vars =

225

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

226

(* Normalize the asserts *)

227

let vars, assert_defs, asserts =

228

List.fold_left (

229

fun (vars, def_accu, assert_accu) assert_ >

230

let assert_expr = assert_.assert_expr in

231

let (defs, vars'), expr =

232

inject_expr

233

~alias:false

234

node

235

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

236

assert_expr

237

in

238

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

239

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

240

let new_locals = List.filter is_local vars in

241

(* Compute traceability info:

242

 gather newly bound variables

243

 compute the associated expression without aliases

244

*)

245

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

246

let node =

247

{ node with

248

node_locals = new_locals;

249

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

250

}

251

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

252


253

let inject_decl decl =

254

match decl.top_decl_desc with

255

 Node nd >

256

{decl with top_decl_desc = Node (inject_node nd)}

257

 Open _  ImportedNode _  Const _  TypeDef _ > decl

258


259

let inject_prog decls =

260

List.map inject_decl decls

261


262


263

(* Local Variables: *)

264

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

265

(* End: *)
