## lustrec / src / mpfr.ml @ ef8a361a

History | View | Annotate | Download (8.43 KB)

1 | 66e25f0f | xthirioux | (********************************************************************) |
---|---|---|---|

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 | (* compile-command:"make -C .." *) |
||

265 | (* End: *) |