## lustrec / src / mpfr.ml @ 32614c2d

History | View | Annotate | Download (8.59 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 | 8446bf03 | ploc | open Lustre_types |

14 | open Machine_code_types |
||

15 | 66e25f0f | xthirioux | open Corelang |

16 | open Normalization |
||

17 | 2863281f | ploc | open Machine_code_common |

18 | 66e25f0f | xthirioux | |

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

20 | 089f94be | ploc | let cpt_fresh = ref 0 |

21 | |||

22 | 66e25f0f | xthirioux | 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 | 089f94be | ploc | let res = |

145 | 66e25f0f | xthirioux | 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 | 333e3a25 | ploc | 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 | 66e25f0f | xthirioux | (* 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 | (* compile-command:"make -C .." *) |
||

269 | (* End: *) |