## lustrec / src / plugins / mpfr / mpfr.ml @ 95944ba1

History | View | Annotate | Download (10.5 KB)

1 | 52016bbb | 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 | 05ca2715 | ploc | open Lustre_types |

14 | open Machine_code_types |
||

15 | 52016bbb | xthirioux | open Corelang |

16 | open Normalization |
||

17 | 05ca2715 | ploc | open Machine_code_common |

18 | 52016bbb | xthirioux | |

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

20 | 05ca2715 | ploc | let cpt_fresh = ref 0 |

21 | |||

22 | 52016bbb | 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 | 05ca2715 | ploc | let pp_inject_real pp_var pp_val fmt var value = |

49 | 52016bbb | xthirioux | Format.fprintf fmt "%s(%a, %a, %s);" |

50 | inject_real_id |
||

51 | pp_var var |
||

52 | 05ca2715 | ploc | pp_val value |

53 | 52016bbb | xthirioux | (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 | 05ca2715 | ploc | pp_inject_real pp_var pp_var fmt var value |

73 | 52016bbb | xthirioux | 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 | d948c0bd | ploc | (* Math library functions *) |

101 | | "acos" -> "MPFRacos" |
||

102 | | "acosh" -> "MPFRacosh" |
||

103 | | "asin" -> "MPFRasin" |
||

104 | | "asinh" -> "MPFRasinh" |
||

105 | | "atan" -> "MPFRatan" |
||

106 | | "atan2" -> "MPFRatan2" |
||

107 | | "atanh" -> "MPFRatanh" |
||

108 | | "cbrt" -> "MPFRcbrt" |
||

109 | | "cos" -> "MPFRcos" |
||

110 | | "cosh" -> "MPFRcosh" |
||

111 | | "ceil" -> "MPFRceil" |
||

112 | | "erf" -> "MPFRerf" |
||

113 | | "exp" -> "MPFRexp" |
||

114 | | "fabs" -> "MPFRfabs" |
||

115 | | "floor" -> "MPFRfloor" |
||

116 | | "fmod" -> "MPFRfmod" |
||

117 | | "log" -> "MPFRlog" |
||

118 | | "log10" -> "MPFRlog10" |
||

119 | | "pow" -> "MPFRpow" |
||

120 | | "round" -> "MPFRround" |
||

121 | | "sin" -> "MPFRsin" |
||

122 | | "sinh" -> "MPFRsinh" |
||

123 | | "sqrt" -> "MPFRsqrt" |
||

124 | | "trunc" -> "MPFRtrunc" |
||

125 | | "tan" -> "MPFRtan" |
||

126 | 52016bbb | xthirioux | | _ -> raise Not_found |

127 | |||

128 | let inject_op id = |
||

129 | d948c0bd | ploc | Format.eprintf "trying to inject mpfr into function %s@." id; |

130 | 52016bbb | xthirioux | try |

131 | base_inject_op id |
||

132 | with Not_found -> id |
||

133 | |||

134 | let homomorphic_funs = |
||

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

136 | |||

137 | let is_homomorphic_fun id = |
||

138 | List.mem id homomorphic_funs |
||

139 | |||

140 | let inject_call expr = |
||

141 | match expr.expr_desc with |
||

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

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

144 | | _ -> expr |
||

145 | |||

146 | let expr_of_const_array expr = |
||

147 | match expr.expr_desc with |
||

148 | | Expr_const (Const_array cl) -> |
||

149 | let typ = Types.array_element_type expr.expr_type in |
||

150 | let expr_of_const c = |
||

151 | { expr_desc = Expr_const c; |
||

152 | expr_type = typ; |
||

153 | expr_clock = expr.expr_clock; |
||

154 | expr_loc = expr.expr_loc; |
||

155 | expr_delay = Delay.new_var (); |
||

156 | expr_annot = None; |
||

157 | expr_tag = new_tag (); |
||

158 | } |
||

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

160 | | _ -> assert false |
||

161 | |||

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

163 | let rec inject_list alias node inject_element defvars elist = |
||

164 | List.fold_right |
||

165 | (fun t (defvars, qlist) -> |
||

166 | let defvars, norm_t = inject_element alias node defvars t in |
||

167 | (defvars, norm_t :: qlist) |
||

168 | ) elist (defvars, []) |
||

169 | |||

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

171 | 05ca2715 | ploc | let res = |

172 | 52016bbb | xthirioux | match expr.expr_desc with |

173 | | Expr_const (Const_real _) -> mk_expr_alias_opt alias node defvars expr |
||

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

175 | | Expr_const (Const_struct _) -> assert false |
||

176 | | Expr_ident _ |
||

177 | | Expr_const _ -> defvars, expr |
||

178 | | Expr_array elist -> |
||

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

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

181 | defvars, norm_expr |
||

182 | | Expr_power (e1, d) -> |
||

183 | let defvars, norm_e1 = inject_expr node defvars e1 in |
||

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

185 | defvars, norm_expr |
||

186 | | Expr_access (e1, d) -> |
||

187 | let defvars, norm_e1 = inject_expr node defvars e1 in |
||

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

189 | defvars, norm_expr |
||

190 | | Expr_tuple elist -> |
||

191 | let defvars, norm_elist = |
||

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

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

194 | defvars, norm_expr |
||

195 | | Expr_appl (id, args, r) -> |
||

196 | let defvars, norm_args = inject_expr node defvars args in |
||

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

198 | mk_expr_alias_opt alias node defvars (inject_call norm_expr) |
||

199 | | Expr_arrow _ -> defvars, expr |
||

200 | | Expr_pre e -> |
||

201 | let defvars, norm_e = inject_expr node defvars e in |
||

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

203 | defvars, norm_expr |
||

204 | | Expr_fby (e1, e2) -> |
||

205 | let defvars, norm_e1 = inject_expr node defvars e1 in |
||

206 | let defvars, norm_e2 = inject_expr node defvars e2 in |
||

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

208 | defvars, norm_expr |
||

209 | | Expr_when (e, c, l) -> |
||

210 | let defvars, norm_e = inject_expr node defvars e in |
||

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

212 | defvars, norm_expr |
||

213 | | Expr_ite (c, t, e) -> |
||

214 | let defvars, norm_c = inject_expr node defvars c in |
||

215 | let defvars, norm_t = inject_expr node defvars t in |
||

216 | let defvars, norm_e = inject_expr node defvars e in |
||

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

218 | defvars, norm_expr |
||

219 | | Expr_merge (c, hl) -> |
||

220 | let defvars, norm_hl = inject_branches node defvars hl in |
||

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

222 | defvars, norm_expr |
||

223 | in |
||

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

225 | res |
||

226 | |||

227 | and inject_branches node defvars hl = |
||

228 | List.fold_right |
||

229 | (fun (t, h) (defvars, norm_q) -> |
||

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

231 | defvars, (t, norm_h) :: norm_q |
||

232 | ) |
||

233 | hl (defvars, []) |
||

234 | |||

235 | |||

236 | let rec inject_eq node defvars eq = |
||

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

238 | let norm_eq = { eq with eq_rhs = norm_rhs } in |
||

239 | norm_eq::defs', vars' |
||

240 | |||

241 | 05ca2715 | ploc | (* let inject_eexpr ee = |

242 | * { ee with eexpr_qfexpr = inject_expr ee.eexpr_qfexpr } |
||

243 | * |
||

244 | * let inject_spec s = |
||

245 | * { s with |
||

246 | * assume = List.map inject_eexpr s.assume; |
||

247 | * guarantees = List.map inject_eexpr s.guarantees; |
||

248 | * modes = List.map (fun m -> |
||

249 | * { m with |
||

250 | * require = List.map inject_eexpr m.require; |
||

251 | * ensure = List.map inject_eexpr m.ensure |
||

252 | * } |
||

253 | * ) s.modes |
||

254 | * } *) |
||

255 | |||

256 | 52016bbb | xthirioux | (** normalize_node node returns a normalized node, |

257 | ie. |
||

258 | - updated locals |
||

259 | - new equations |
||

260 | - |
||

261 | *) |
||

262 | let inject_node node = |
||

263 | cpt_fresh := 0; |
||

264 | let inputs_outputs = node.node_inputs@node.node_outputs in |
||

265 | 95944ba1 | ploc | let norm_ctx = (node.node_id, get_node_vars node) in |

266 | 52016bbb | xthirioux | let is_local v = |

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

268 | let orig_vars = inputs_outputs@node.node_locals in |
||

269 | 05ca2715 | ploc | let defs, vars = |

270 | let eqs, auts = get_node_eqs node in |
||

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

272 | 95944ba1 | ploc | List.fold_left (inject_eq norm_ctx) ([], orig_vars) eqs in |

273 | 52016bbb | xthirioux | (* Normalize the asserts *) |

274 | let vars, assert_defs, asserts = |
||

275 | List.fold_left ( |
||

276 | fun (vars, def_accu, assert_accu) assert_ -> |
||

277 | let assert_expr = assert_.assert_expr in |
||

278 | let (defs, vars'), expr = |
||

279 | inject_expr |
||

280 | ~alias:false |
||

281 | 95944ba1 | ploc | norm_ctx |

282 | 52016bbb | xthirioux | ([], vars) (* defvar only contains vars *) |

283 | assert_expr |
||

284 | in |
||

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

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

287 | let new_locals = List.filter is_local vars in |
||

288 | (* Compute traceability info: |
||

289 | - gather newly bound variables |
||

290 | - compute the associated expression without aliases |
||

291 | *) |
||

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

293 | 05ca2715 | ploc | (* See comment below |

294 | * let spec = match node.node_spec with |
||

295 | * | None -> None |
||

296 | * | Some spec -> Some (inject_spec spec) |
||

297 | * in *) |
||

298 | 52016bbb | xthirioux | let node = |

299 | { node with |
||

300 | node_locals = new_locals; |
||

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

302 | 05ca2715 | ploc | (* Incomplete work: TODO. Do we have to inject MPFR code here? |

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

304 | C code for annotations. Otherwise the various verification |
||

305 | backend should have their own understanding, but would not |
||

306 | necessarily require this additional normalization. *) |
||

307 | (* |
||

308 | node_spec = spec; |
||

309 | node_annot = List.map (fun ann -> {ann with |
||

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

311 | ) node.node_annot *) |
||

312 | 52016bbb | xthirioux | } |

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

314 | |||

315 | let inject_decl decl = |
||

316 | match decl.top_decl_desc with |
||

317 | | Node nd -> |
||

318 | {decl with top_decl_desc = Node (inject_node nd)} |
||

319 | 19a1e66b | ploc | | Include _ | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl |

320 | 52016bbb | xthirioux | |

321 | let inject_prog decls = |
||

322 | List.map inject_decl decls |
||

323 | |||

324 | |||

325 | (* Local Variables: *) |
||

326 | (* compile-command:"make -C .." *) |
||

327 | (* End: *) |