## lustrec / src / normalization.ml @ 81229f63

History | View | Annotate | Download (32.1 KB)

1 | a2d97a3e | ploc | (********************************************************************) |
---|---|---|---|

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 | 22fe1c93 | ploc | |

12 | open Utils |
||

13 | 8446bf03 | ploc | open Lustre_types |

14 | 22fe1c93 | ploc | open Corelang |

15 | open Format |
||

16 | |||

17 | 27dc3869 | ploc | (** Normalisation iters through the AST of expressions and bind fresh definition |

18 | when some criteria are met. This creation of fresh definition is performed by |
||

19 | the function mk_expr_alias_opt when the alias argument is on. |
||

20 | |||

21 | Initial expressions, ie expressions attached a variable in an equation |
||

22 | definition are not aliased. This non-alias feature is propagated in the |
||

23 | expression AST for array access and power construct, tuple, and some special |
||

24 | cases of arrows. |
||

25 | |||

26 | Two global variables may impact the normalization process: |
||

27 | - unfold_arrow_active |
||

28 | - force_alias_ite: when set, bind a fresh alias for then and else |
||

29 | definitions. |
||

30 | *) |
||

31 | |||

32 | ad4774b0 | ploc | type param_t = |

33 | { |
||

34 | unfold_arrow_active: bool; |
||

35 | force_alias_ite: bool; |
||

36 | force_alias_internal_fun: bool; |
||

37 | } |
||

38 | |||

39 | let params = ref |
||

40 | { |
||

41 | unfold_arrow_active = false; |
||

42 | force_alias_ite = false; |
||

43 | force_alias_internal_fun =false; |
||

44 | } |
||

45 | 27dc3869 | ploc | |

46 | 95944ba1 | ploc | type norm_ctx_t = |

47 | { |
||

48 | parentid: ident; |
||

49 | vars: var_decl list; |
||

50 | is_output: ident -> bool; |
||

51 | } |
||

52 | |||

53 | |||

54 | 2e6f9ba8 | xthirioux | let expr_true loc ck = |

55 | { expr_tag = Utils.new_tag (); |
||

56 | expr_desc = Expr_const (Const_tag tag_true); |
||

57 | expr_type = Type_predef.type_bool; |
||

58 | expr_clock = ck; |
||

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

60 | expr_annot = None; |
||

61 | expr_loc = loc } |
||

62 | |||

63 | let expr_false loc ck = |
||

64 | { expr_tag = Utils.new_tag (); |
||

65 | expr_desc = Expr_const (Const_tag tag_false); |
||

66 | expr_type = Type_predef.type_bool; |
||

67 | expr_clock = ck; |
||

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

69 | expr_annot = None; |
||

70 | expr_loc = loc } |
||

71 | |||

72 | let expr_once loc ck = |
||

73 | { expr_tag = Utils.new_tag (); |
||

74 | expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck); |
||

75 | expr_type = Type_predef.type_bool; |
||

76 | expr_clock = ck; |
||

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

78 | expr_annot = None; |
||

79 | expr_loc = loc } |
||

80 | |||

81 | let is_expr_once = |
||

82 | let dummy_expr_once = expr_once Location.dummy_loc (Clocks.new_var true) in |
||

83 | fun expr -> Corelang.is_eq_expr expr dummy_expr_once |
||

84 | |||

85 | let unfold_arrow expr = |
||

86 | match expr.expr_desc with |
||

87 | | Expr_arrow (e1, e2) -> |
||

88 | let loc = expr.expr_loc in |
||

89 | a38c681e | xthirioux | let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in |

90 | 2e6f9ba8 | xthirioux | { expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) } |

91 | | _ -> assert false |
||

92 | |||

93 | 22fe1c93 | ploc | |

94 | |||

95 | (* Get the equation in [defs] with [expr] as rhs, if any *) |
||

96 | let get_expr_alias defs expr = |
||

97 | 0bd19a92 | THIRIOUX Xavier | try Some (List.find (fun eq -> Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock && is_eq_expr eq.eq_rhs expr) defs) |

98 | 22fe1c93 | ploc | with |

99 | e49b6d55 | xavier.thirioux | | Not_found -> None |

100 | |||

101 | 22fe1c93 | ploc | (* Replace [expr] with (tuple of) [locals] *) |

102 | let replace_expr locals expr = |
||

103 | match locals with |
||

104 | | [] -> assert false |
||

105 | | [v] -> { expr with |
||

106 | expr_tag = Utils.new_tag (); |
||

107 | expr_desc = Expr_ident v.var_id } |
||

108 | | _ -> { expr with |
||

109 | expr_tag = Utils.new_tag (); |
||

110 | fc886259 | xthirioux | expr_desc = Expr_tuple (List.map expr_of_vdecl locals) } |

111 | 22fe1c93 | ploc | |

112 | let unfold_offsets e offsets = |
||

113 | let add_offset e d = |
||

114 | fc886259 | xthirioux | (*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d; |

115 | let res = *) |
||

116 | 22fe1c93 | ploc | { e with |

117 | expr_tag = Utils.new_tag (); |
||

118 | expr_loc = d.Dimension.dim_loc; |
||

119 | expr_type = Types.array_element_type e.expr_type; |
||

120 | fc886259 | xthirioux | expr_desc = Expr_access (e, d) } |

121 | (*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *) |
||

122 | in |
||

123 | 22fe1c93 | ploc | List.fold_left add_offset e offsets |

124 | |||

125 | 95944ba1 | ploc | (* IS IT USED ? TODO |

126 | 22fe1c93 | ploc | (* Create an alias for [expr], if none exists yet *) |

127 | 95944ba1 | ploc | let mk_expr_alias (parentid, vars) (defs, vars) expr = |

128 | a38c681e | xthirioux | (*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*) |

129 | 22fe1c93 | ploc | match get_expr_alias defs expr with |

130 | | Some eq -> |
||

131 | let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in |
||

132 | (defs, vars), replace_expr aliases expr |
||

133 | | None -> |
||

134 | let new_aliases = |
||

135 | List.map2 |
||

136 | 95944ba1 | ploc | (mk_fresh_var (parentid, vars) expr.expr_loc) |

137 | 22fe1c93 | ploc | (Types.type_list_of_type expr.expr_type) |

138 | (Clocks.clock_list_of_clock expr.expr_clock) in |
||

139 | let new_def = |
||

140 | mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr) |
||

141 | 3ca6d126 | ploc | in |

142 | fc886259 | xthirioux | (* Format.eprintf "Checking def of alias: %a -> %a@." (fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) new_aliases Printers.pp_expr expr; *) |

143 | 3ca6d126 | ploc | (new_def::defs, new_aliases@vars), replace_expr new_aliases expr |

144 | 95944ba1 | ploc | *) |

145 | |||

146 | d4807c3d | xthirioux | (* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident) |

147 | and [opt] is true *) |
||

148 | 95944ba1 | ploc | let mk_expr_alias_opt opt norm_ctx (defs, vars) expr = |

149 | 04a63d25 | xthirioux | (*Format.eprintf "mk_expr_alias_opt %B %a %a %a@." opt Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*) |

150 | d4807c3d | xthirioux | match expr.expr_desc with |

151 | | Expr_ident alias -> |
||

152 | 04a63d25 | xthirioux | (defs, vars), expr |

153 | 8deaa2dd | tkahsai | | _ -> |

154 | 04a63d25 | xthirioux | match get_expr_alias defs expr with |

155 | | Some eq -> |
||

156 | c35de73b | ploc | (* Format.eprintf "Found a preexisting definition@."; *) |

157 | 04a63d25 | xthirioux | let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in |

158 | (defs, vars), replace_expr aliases expr |
||

159 | | None -> |
||

160 | c35de73b | ploc | (* Format.eprintf "Didnt found a preexisting definition (opt=%b)@." opt; |

161 | * Format.eprintf "existing defs are: @[[%a@]]@." |
||

162 | * (fprintf_list ~sep:"@ "(fun fmt eq -> |
||

163 | * Format.fprintf fmt "ck:%a isckeq=%b, , iseq=%b, eq=%a" |
||

164 | * Clocks.print_ck eq.eq_rhs.expr_clock |
||

165 | * (Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock) |
||

166 | * (is_eq_expr eq.eq_rhs expr) |
||

167 | * Printers.pp_node_eq eq)) |
||

168 | * defs; *) |
||

169 | 04a63d25 | xthirioux | if opt |

170 | then |
||

171 | let new_aliases = |
||

172 | List.map2 |
||

173 | 59020713 | ploc | (mk_fresh_var (norm_ctx.parentid, (norm_ctx.vars@vars)) expr.expr_loc) |

174 | 04a63d25 | xthirioux | (Types.type_list_of_type expr.expr_type) |

175 | (Clocks.clock_list_of_clock expr.expr_clock) in |
||

176 | let new_def = |
||

177 | mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr) |
||

178 | 66359a5e | ploc | in |

179 | (* Typing and Registering machine type *) |
||

180 | 59020713 | ploc | let _ = if Machine_types.is_active then |

181 | Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr |
||

182 | in |
||

183 | 66359a5e | ploc | (new_def::defs, new_aliases@vars), replace_expr new_aliases expr |

184 | 04a63d25 | xthirioux | else |

185 | (defs, vars), expr |
||

186 | 22fe1c93 | ploc | |

187 | 8deaa2dd | tkahsai | (* Create a (normalized) expression from [ref_e], |

188 | 22fe1c93 | ploc | replacing description with [norm_d], |

189 | 8deaa2dd | tkahsai | taking propagated [offsets] into account |

190 | 22fe1c93 | ploc | in order to change expression type *) |

191 | let mk_norm_expr offsets ref_e norm_d = |
||

192 | e49b6d55 | xavier.thirioux | (*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*) |

193 | 22fe1c93 | ploc | let drop_array_type ty = |

194 | Types.map_tuple_type Types.array_element_type ty in |
||

195 | { ref_e with |
||

196 | expr_desc = norm_d; |
||

197 | expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type } |
||

198 | e49b6d55 | xavier.thirioux | |

199 | 22fe1c93 | ploc | (* normalize_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *) |

200 | 95944ba1 | ploc | let rec normalize_list alias norm_ctx offsets norm_element defvars elist = |

201 | 22fe1c93 | ploc | List.fold_right |

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

203 | 95944ba1 | ploc | let defvars, norm_t = norm_element alias norm_ctx offsets defvars t in |

204 | 22fe1c93 | ploc | (defvars, norm_t :: qlist) |

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

206 | |||

207 | 95944ba1 | ploc | let rec normalize_expr ?(alias=true) ?(alias_basic=false) norm_ctx offsets defvars expr = |

208 | e49b6d55 | xavier.thirioux | (*Format.eprintf "normalize %B %a:%a [%a]@." alias Printers.pp_expr expr Types.print_ty expr.expr_type (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*) |

209 | 22fe1c93 | ploc | match expr.expr_desc with |

210 | 8deaa2dd | tkahsai | | Expr_const _ |

211 | 22fe1c93 | ploc | | Expr_ident _ -> defvars, unfold_offsets expr offsets |

212 | | Expr_array elist -> |
||

213 | 95944ba1 | ploc | let defvars, norm_elist = normalize_list alias norm_ctx offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in |

214 | 0a10042e | ploc | let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in |

215 | 95944ba1 | ploc | mk_expr_alias_opt alias norm_ctx defvars norm_expr |

216 | 22fe1c93 | ploc | | Expr_power (e1, d) when offsets = [] -> |

217 | 95944ba1 | ploc | let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in |

218 | 0a10042e | ploc | let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in |

219 | 95944ba1 | ploc | mk_expr_alias_opt alias norm_ctx defvars norm_expr |

220 | 22fe1c93 | ploc | | Expr_power (e1, d) -> |

221 | 95944ba1 | ploc | normalize_expr ~alias:alias norm_ctx (List.tl offsets) defvars e1 |

222 | 22fe1c93 | ploc | | Expr_access (e1, d) -> |

223 | 95944ba1 | ploc | normalize_expr ~alias:alias norm_ctx (d::offsets) defvars e1 |

224 | 8deaa2dd | tkahsai | | Expr_tuple elist -> |

225 | 0a10042e | ploc | let defvars, norm_elist = |

226 | 95944ba1 | ploc | normalize_list alias norm_ctx offsets (fun alias -> normalize_expr ~alias:alias ~alias_basic:false) defvars elist in |

227 | 0a10042e | ploc | defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist) |

228 | 8deaa2dd | tkahsai | | Expr_appl (id, args, None) |

229 | 04a63d25 | xthirioux | when Basic_library.is_homomorphic_fun id |

230 | af5af1e8 | ploc | && Types.is_array_type expr.expr_type -> |

231 | 0a10042e | ploc | let defvars, norm_args = |

232 | normalize_list |
||

233 | alias |
||

234 | 95944ba1 | ploc | norm_ctx |

235 | 0a10042e | ploc | offsets |

236 | (fun _ -> normalize_array_expr ~alias:true) |
||

237 | defvars |
||

238 | (expr_list_of_expr args) |
||

239 | in |
||

240 | defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) |
||

241 | 3436d1a6 | ploc | | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr |

242 | ad4774b0 | ploc | && not (!params.force_alias_internal_fun || alias_basic) -> |

243 | 95944ba1 | ploc | let defvars, norm_args = normalize_expr ~alias:true norm_ctx offsets defvars args in |

244 | 0a10042e | ploc | defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None)) |

245 | 22fe1c93 | ploc | | Expr_appl (id, args, r) -> |

246 | 0a10042e | ploc | let defvars, r = |

247 | match r with |
||

248 | | None -> defvars, None |
||

249 | | Some r -> |
||

250 | 95944ba1 | ploc | let defvars, norm_r = normalize_expr ~alias_basic:true norm_ctx [] defvars r in |

251 | 0a10042e | ploc | defvars, Some norm_r |

252 | in |
||

253 | 95944ba1 | ploc | let defvars, norm_args = normalize_expr norm_ctx [] defvars args in |

254 | 0a10042e | ploc | let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in |

255 | if offsets <> [] |
||

256 | then |
||

257 | 95944ba1 | ploc | let defvars, norm_expr = normalize_expr norm_ctx [] defvars norm_expr in |

258 | normalize_expr ~alias:alias norm_ctx offsets defvars norm_expr |
||

259 | 0a10042e | ploc | else |

260 | ad4774b0 | ploc | mk_expr_alias_opt (alias && (!params.force_alias_internal_fun || alias_basic |

261 | 0a10042e | ploc | || not (Basic_library.is_expr_internal_fun expr))) |

262 | 95944ba1 | ploc | norm_ctx defvars norm_expr |

263 | ad4774b0 | ploc | | Expr_arrow (e1,e2) when !params.unfold_arrow_active && not (is_expr_once expr) -> |

264 | 0a10042e | ploc | (* Here we differ from Colaco paper: arrows are pushed to the top *) |

265 | 95944ba1 | ploc | normalize_expr ~alias:alias norm_ctx offsets defvars (unfold_arrow expr) |

266 | 2e6f9ba8 | xthirioux | | Expr_arrow (e1,e2) -> |

267 | 95944ba1 | ploc | let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in |

268 | let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in |
||

269 | 0a10042e | ploc | let norm_expr = mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) in |

270 | 95944ba1 | ploc | mk_expr_alias_opt alias norm_ctx defvars norm_expr |

271 | 22fe1c93 | ploc | | Expr_pre e -> |

272 | 95944ba1 | ploc | let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in |

273 | 0a10042e | ploc | let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in |

274 | 95944ba1 | ploc | mk_expr_alias_opt alias norm_ctx defvars norm_expr |

275 | 22fe1c93 | ploc | | Expr_fby (e1, e2) -> |

276 | 95944ba1 | ploc | let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in |

277 | let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in |
||

278 | 0a10042e | ploc | let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in |

279 | 95944ba1 | ploc | mk_expr_alias_opt alias norm_ctx defvars norm_expr |

280 | 22fe1c93 | ploc | | Expr_when (e, c, l) -> |

281 | 95944ba1 | ploc | let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in |

282 | 0a10042e | ploc | defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l)) |

283 | 22fe1c93 | ploc | | Expr_ite (c, t, e) -> |

284 | 95944ba1 | ploc | let defvars, norm_c = normalize_guard norm_ctx defvars c in |

285 | let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in |
||

286 | let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in |
||

287 | 0a10042e | ploc | let norm_expr = mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) in |

288 | 95944ba1 | ploc | mk_expr_alias_opt alias norm_ctx defvars norm_expr |

289 | 22fe1c93 | ploc | | Expr_merge (c, hl) -> |

290 | 95944ba1 | ploc | let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in |

291 | 0a10042e | ploc | let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in |

292 | 95944ba1 | ploc | mk_expr_alias_opt alias norm_ctx defvars norm_expr |

293 | 8deaa2dd | tkahsai | |

294 | 52cfee34 | xthirioux | (* Creates a conditional with a merge construct, which is more lazy *) |

295 | (* |
||

296 | 0a10042e | ploc | let norm_conditional_as_merge alias node norm_expr offsets defvars expr = |

297 | match expr.expr_desc with |
||

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

299 | let defvars, norm_t = norm_expr (alias node offsets defvars t in |
||

300 | | _ -> assert false |
||

301 | 52cfee34 | xthirioux | *) |

302 | 95944ba1 | ploc | and normalize_branches norm_ctx offsets defvars hl = |

303 | 0a10042e | ploc | List.fold_right |

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

305 | 95944ba1 | ploc | let (defvars, norm_h) = normalize_cond_expr norm_ctx offsets defvars h in |

306 | 0a10042e | ploc | defvars, (t, norm_h) :: norm_q |

307 | ) |
||

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

309 | 22fe1c93 | ploc | |

310 | 95944ba1 | ploc | and normalize_array_expr ?(alias=true) norm_ctx offsets defvars expr = |

311 | 04a63d25 | xthirioux | (*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*) |

312 | 22fe1c93 | ploc | match expr.expr_desc with |

313 | | Expr_power (e1, d) when offsets = [] -> |
||

314 | 95944ba1 | ploc | let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in |

315 | 0a10042e | ploc | defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d)) |

316 | 22fe1c93 | ploc | | Expr_power (e1, d) -> |

317 | 95944ba1 | ploc | normalize_array_expr ~alias:alias norm_ctx (List.tl offsets) defvars e1 |

318 | | Expr_access (e1, d) -> normalize_array_expr ~alias:alias norm_ctx (d::offsets) defvars e1 |
||

319 | 22fe1c93 | ploc | | Expr_array elist when offsets = [] -> |

320 | 95944ba1 | ploc | let defvars, norm_elist = normalize_list alias norm_ctx offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in |

321 | 0a10042e | ploc | defvars, mk_norm_expr offsets expr (Expr_array norm_elist) |

322 | 04a63d25 | xthirioux | | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr -> |

323 | 95944ba1 | ploc | let defvars, norm_args = normalize_list alias norm_ctx offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in |

324 | 0a10042e | ploc | defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) |

325 | 95944ba1 | ploc | | _ -> normalize_expr ~alias:alias norm_ctx offsets defvars expr |

326 | 22fe1c93 | ploc | |

327 | 95944ba1 | ploc | and normalize_cond_expr ?(alias=true) norm_ctx offsets defvars expr = |

328 | 22fe1c93 | ploc | (*Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*) |

329 | match expr.expr_desc with |
||

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

331 | 95944ba1 | ploc | normalize_cond_expr ~alias:alias norm_ctx (d::offsets) defvars e1 |

332 | 22fe1c93 | ploc | | Expr_ite (c, t, e) -> |

333 | 95944ba1 | ploc | let defvars, norm_c = normalize_guard norm_ctx defvars c in |

334 | let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in |
||

335 | let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in |
||

336 | 0a10042e | ploc | defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) |

337 | 22fe1c93 | ploc | | Expr_merge (c, hl) -> |

338 | 95944ba1 | ploc | let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in |

339 | 0a10042e | ploc | defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) |

340 | ad4774b0 | ploc | | _ when !params.force_alias_ite -> |

341 | 27dc3869 | ploc | (* Forcing alias creation for then/else expressions *) |

342 | let defvars, norm_expr = |
||

343 | 95944ba1 | ploc | normalize_expr ~alias:alias norm_ctx offsets defvars expr |

344 | 27dc3869 | ploc | in |

345 | 95944ba1 | ploc | mk_expr_alias_opt true norm_ctx defvars norm_expr |

346 | 27dc3869 | ploc | | _ -> (* default case without the force_alias_ite option *) |

347 | 95944ba1 | ploc | normalize_expr ~alias:alias norm_ctx offsets defvars expr |

348 | 0a10042e | ploc | |

349 | 95944ba1 | ploc | and normalize_guard norm_ctx defvars expr = |

350 | let defvars, norm_expr = normalize_expr ~alias_basic:true norm_ctx [] defvars expr in |
||

351 | mk_expr_alias_opt true norm_ctx defvars norm_expr |
||

352 | 22fe1c93 | ploc | |

353 | (* outputs cannot be memories as well. If so, introduce new local variable. |
||

354 | *) |
||

355 | 95944ba1 | ploc | let decouple_outputs norm_ctx defvars eq = |

356 | 22fe1c93 | ploc | let rec fold_lhs defvars lhs tys cks = |

357 | a742719e | ploc | match lhs, tys, cks with |

358 | | [], [], [] -> defvars, [] |
||

359 | | v::qv, t::qt, c::qc -> let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in |
||

360 | 95944ba1 | ploc | if norm_ctx.is_output v |

361 | a742719e | ploc | then |

362 | 95944ba1 | ploc | let newvar = mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) eq.eq_loc t c in |

363 | a742719e | ploc | let neweq = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in |

364 | (neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q |
||

365 | else |
||

366 | (defs_q, vars_q), v::lhs_q |
||

367 | | _ -> assert false in |
||

368 | 22fe1c93 | ploc | let defvars', lhs' = |

369 | fold_lhs |
||

370 | defvars |
||

371 | eq.eq_lhs |
||

372 | (Types.type_list_of_type eq.eq_rhs.expr_type) |
||

373 | (Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in |
||

374 | defvars', {eq with eq_lhs = lhs' } |
||

375 | |||

376 | 95944ba1 | ploc | let rec normalize_eq norm_ctx defvars eq = |

377 | 04a63d25 | xthirioux | (*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*) |

378 | 22fe1c93 | ploc | match eq.eq_rhs.expr_desc with |

379 | | Expr_pre _ |
||

380 | | Expr_fby _ -> |
||

381 | 95944ba1 | ploc | let (defvars', eq') = decouple_outputs norm_ctx defvars eq in |

382 | let (defs', vars'), norm_rhs = normalize_expr ~alias:false norm_ctx [] defvars' eq'.eq_rhs in |
||

383 | 22fe1c93 | ploc | let norm_eq = { eq' with eq_rhs = norm_rhs } in |

384 | (norm_eq::defs', vars') |
||

385 | | Expr_array _ -> |
||

386 | 95944ba1 | ploc | let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in |

387 | 22fe1c93 | ploc | let norm_eq = { eq with eq_rhs = norm_rhs } in |

388 | (norm_eq::defs', vars') |
||

389 | 04a63d25 | xthirioux | | Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type -> |

390 | 95944ba1 | ploc | let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in |

391 | 22fe1c93 | ploc | let norm_eq = { eq with eq_rhs = norm_rhs } in |

392 | (norm_eq::defs', vars') |
||

393 | | Expr_appl _ -> |
||

394 | 95944ba1 | ploc | let (defs', vars'), norm_rhs = normalize_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in |

395 | 22fe1c93 | ploc | let norm_eq = { eq with eq_rhs = norm_rhs } in |

396 | (norm_eq::defs', vars') |
||

397 | | _ -> |
||

398 | 95944ba1 | ploc | let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in |

399 | 22fe1c93 | ploc | let norm_eq = { eq with eq_rhs = norm_rhs } in |

400 | norm_eq::defs', vars' |
||

401 | |||

402 | 95944ba1 | ploc | let normalize_eq_split norm_ctx defvars eq = |

403 | 8fa4e28e | ploc | try |

404 | 95944ba1 | ploc | let defs, vars = normalize_eq norm_ctx defvars eq in |

405 | 59020713 | ploc | List.fold_right (fun eq (def, vars) -> |

406 | let eq_defs = Splitting.tuple_split_eq eq in |
||

407 | if eq_defs = [eq] then |
||

408 | eq::def, vars |
||

409 | else |
||

410 | List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs |
||

411 | ) defs ([], vars) |
||

412 | |||

413 | with ex -> ( |
||

414 | 8fa4e28e | ploc | Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq; |

415 | 59020713 | ploc | raise ex |

416 | 8fa4e28e | ploc | ) |

417 | |||

418 | 59020713 | ploc | (* Projecting an eexpr to an eexpr associated to a single |

419 | variable. Returns the updated ee, the bounded variable and the |
||

420 | associated statement *) |
||

421 | let normalize_pred_eexpr decls norm_ctx (def,vars) ee = |
||

422 | assert (ee.eexpr_quantifiers = []); (* We do not normalize quantifiers yet. This is for very far future. *) |
||

423 | (* don't do anything is eexpr is just a variable *) |
||

424 | let skip = |
||

425 | match ee.eexpr_qfexpr.expr_desc with |
||

426 | | Expr_ident _ | Expr_const _ -> true |
||

427 | | _ -> false |
||

428 | 949b2e1e | ploc | in |

429 | 59020713 | ploc | if skip then |

430 | ee, (def, vars) |
||

431 | else ( |
||

432 | (* New output variable *) |
||

433 | let output_id = "spec" ^ string_of_int ee.eexpr_tag in |
||

434 | let output_var = |
||

435 | mkvar_decl |
||

436 | ee.eexpr_loc |
||

437 | (output_id, |
||

438 | mktyp ee.eexpr_loc Tydec_bool, (* It is a predicate, hence a bool *) |
||

439 | mkclock ee.eexpr_loc Ckdec_any, |
||

440 | false (* not a constant *), |
||

441 | None, |
||

442 | None |
||

443 | ) |
||

444 | in |
||

445 | let output_expr = expr_of_vdecl output_var in |
||

446 | (* Rebuilding an eexpr with a silly expression, just a variable *) |
||

447 | let ee' = { ee with eexpr_qfexpr = output_expr } in |
||

448 | |||

449 | (* Now processing a fresh equation output_id = eexpr_qfexpr. We |
||

450 | inline possible calls within, normalize it and type/clock the |
||

451 | result. *) |
||

452 | let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in |
||

453 | 1fd3d002 | ploc | |

454 | |||

455 | (* (\* Inlining any calls *\) |
||

456 | * let nodes = get_nodes decls in |
||

457 | * let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in |
||

458 | * let vars, eqs = |
||

459 | * if calls = [] && not (eq_has_arrows eq) then |
||

460 | * vars, [eq] |
||

461 | * else |
||

462 | * assert false (\* TODO *\) |
||

463 | * in *) |
||

464 | 59020713 | ploc | |

465 | (* Normalizing expr and eqs *) |
||

466 | 1fd3d002 | ploc | let defs, vars = List.fold_left (normalize_eq_split norm_ctx) (def, vars) [eq] in |

467 | let vars = output_var :: vars in |
||

468 | 59020713 | ploc | (* let todefine = |

469 | List.fold_left |
||

470 | (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m) |
||

471 | (ISet.add output_id ISet.empty) vars in |
||

472 | *) |
||

473 | |||

474 | (* Typing / Clocking *) |
||

475 | try |
||

476 | ignore (Typing.type_var_decl_list vars !Global.type_env vars); |
||

477 | (* |
||

478 | let env = Typing.type_var_decl [] !Global.type_env xxxx output_var in (* typing the variable *) |
||

479 | (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *) |
||

480 | let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in |
||

481 | (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*) |
||

482 | let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in |
||

483 | (* check that table is empty *) |
||

484 | if (not (ISet.is_empty undefined_vars)) then |
||

485 | raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars)); |
||

486 | |||

487 | (*Format.eprintf "normalized eqs %a@.@?" |
||

488 | (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs; *) |
||

489 | *) |
||

490 | |||

491 | ee', (defs, vars) |
||

492 | |||

493 | with (Types.Error (loc,err)) as exc -> |
||

494 | eprintf "Typing error for eexpr %a: %a%a%a@." |
||

495 | Printers.pp_eexpr ee |
||

496 | Types.pp_error err |
||

497 | (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs |
||

498 | Location.pp_loc loc |
||

499 | |||

500 | |||

501 | ; |
||

502 | raise exc |
||

503 | |||

504 | ) |
||

505 | |||

506 | (* |
||

507 | 8fa4e28e | ploc | |

508 | 949b2e1e | ploc | let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in |

509 | (* Calls are first inlined *) |
||

510 | 59020713 | ploc | |

511 | 949b2e1e | ploc | (*Format.eprintf "eexpr %a@.calls: %a@.@?" Printers.pp_eexpr ee (Utils.fprintf_list ~sep:", " (fun fmt nd -> pp_print_string fmt nd.node_id)) calls; *) |

512 | let (new_locals, eqs) = |
||

513 | if calls = [] && not (eq_has_arrows eq) then |
||

514 | (locals, [eq]) |
||

515 | else ( (* TODO remettre le code. Je l'ai enleve pour des dependances cycliques *) |
||

516 | (* let new_locals, eqs, asserts = Inliner.inline_eq ~arrows:true eq locals calls in |
||

517 | (*Format.eprintf "eqs %a@.@?" |
||

518 | (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) eqs; *) |
||

519 | (new_locals, eqs) |
||

520 | *) |
||

521 | (locals, [eq]) |
||

522 | |||

523 | ) in |
||

524 | (* Normalizing expr and eqs *) |
||

525 | 8fa4e28e | ploc | let defs, vars = List.fold_left (normalize_eq_split node) ([], new_locals) eqs in |

526 | let todefine = List.fold_left |
||

527 | 949b2e1e | ploc | (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m) |

528 | (ISet.add output_id ISet.empty) vars in |
||

529 | 8fa4e28e | ploc | |

530 | 949b2e1e | ploc | try |

531 | 2d27eedd | ploc | let env = Typing.type_var_decl_list quant_vars !Global.type_env quant_vars in |

532 | 949b2e1e | ploc | let env = Typing.type_var_decl [] env output_var in (* typing the variable *) |

533 | (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *) |
||

534 | let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in |
||

535 | (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*) |
||

536 | let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in |
||

537 | (* check that table is empty *) |
||

538 | if (not (ISet.is_empty undefined_vars)) then |
||

539 | raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars)); |
||

540 | |||

541 | (*Format.eprintf "normalized eqs %a@.@?" |
||

542 | (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs; *) |
||

543 | ee.eexpr_normalized <- Some (output_var, defs, vars) |
||

544 | 8fa4e28e | ploc | |

545 | 949b2e1e | ploc | with (Types.Error (loc,err)) as exc -> |

546 | eprintf "Typing error for eexpr %a: %a%a%a@." |
||

547 | Printers.pp_eexpr ee |
||

548 | Types.pp_error err |
||

549 | (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs |
||

550 | Location.pp_loc loc |
||

551 | 8fa4e28e | ploc | |

552 | 949b2e1e | ploc | |

553 | 8fa4e28e | ploc | ; |

554 | 949b2e1e | ploc | raise exc |

555 | 95944ba1 | ploc | *) |

556 | 8fa4e28e | ploc | |

557 | 59020713 | ploc | |

558 | (* We use node local vars to make sure we are creating fresh variables *) |
||

559 | let normalize_spec decls parentid (in_vars, out_vars, l_vars) s = |
||

560 | f4cba4b8 | ploc | (* Original set of variables actually visible from here: in/out and |

561 | 59020713 | ploc | spec locals (no node locals) *) |

562 | let orig_vars = in_vars @ out_vars @ s.locals in |
||

563 | 1fd3d002 | ploc | (* Format.eprintf "NormSpec: init locals: %a@." Printers.pp_vars s.locals; *) |

564 | 95944ba1 | ploc | let not_is_orig_var v = |

565 | List.for_all ((!=) v) orig_vars in |
||

566 | 59020713 | ploc | let norm_ctx = { |

567 | parentid = parentid; |
||

568 | vars = in_vars @ out_vars @ l_vars; |
||

569 | is_output = (fun _ -> false) (* no need to introduce fresh variables for outputs *); |
||

570 | } |
||

571 | in |
||

572 | (* Normalizing existing stmts *) |
||

573 | let eqs, auts = List.fold_right (fun s (el,al) -> match s with Eq e -> e::el, al | Aut a -> el, a::al) s.stmts ([], []) in |
||

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

575 | let defsvars = |
||

576 | List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs |
||

577 | in |
||

578 | (* Iterate through predicates and normalize them on the go, creating |
||

579 | fresh variables for any guarantees/assumes/require/ensure *) |
||

580 | let process_predicates l defvars = |
||

581 | 1fd3d002 | ploc | (* Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd defvars); *) |

582 | let res = List.fold_right (fun ee (accu, defvars) -> |
||

583 | 59020713 | ploc | let ee', defvars = normalize_pred_eexpr decls norm_ctx defvars ee in |

584 | ee'::accu, defvars |
||

585 | ) l ([], defvars) |
||

586 | 1fd3d002 | ploc | in |

587 | (* Format.eprintf "ProcStmt: %a@." Printers.pp_node_eqs (fst (snd res)); |
||

588 | * Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd (snd res)); *) |
||

589 | res |
||

590 | 95944ba1 | ploc | in |

591 | |||

592 | 59020713 | ploc | |

593 | let assume', defsvars = process_predicates s.assume defsvars in |
||

594 | let guarantees', defsvars = process_predicates s.guarantees defsvars in |
||

595 | let modes', (defs, vars) = |
||

596 | List.fold_right ( |
||

597 | fun m (accu_m, defsvars) -> |
||

598 | let require', defsvars = process_predicates m.require defsvars in |
||

599 | let ensure', defsvars = process_predicates m.ensure defsvars in |
||

600 | { m with require = require'; ensure = ensure' }:: accu_m, defsvars |
||

601 | ) s.modes ([], defsvars) |
||

602 | in |
||

603 | |||

604 | let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *) |
||

605 | f4cba4b8 | ploc | new_locals, defs, |

606 | 95944ba1 | ploc | {s with |

607 | 1fd3d002 | ploc | (* locals = s.locals @ new_locals; *) |

608 | f4cba4b8 | ploc | stmts = []; |

609 | 59020713 | ploc | assume = assume'; |

610 | guarantees = guarantees'; |
||

611 | modes = modes' |
||

612 | } |
||

613 | (* let nee _ = () in |
||

614 | * (\*normalize_eexpr decls iovars in *\) |
||

615 | * List.iter nee s.assume; |
||

616 | * List.iter nee s.guarantees; |
||

617 | * List.iter (fun m -> |
||

618 | * List.iter nee m.require; |
||

619 | * List.iter nee m.ensure |
||

620 | * ) s.modes; *) |
||

621 | |||

622 | |||

623 | |||

624 | |||

625 | |||

626 | 949b2e1e | ploc | |

627 | (* The normalization phase introduces new local variables |
||

628 | - output cannot be memories. If this happen, new local variables acting as |
||

629 | memories are introduced. |
||

630 | - array constants, pre, arrow, fby, ite, merge, calls to node with index |
||

631 | access |
||

632 | Thoses values are shared, ie. no duplicate expressions are introduced. |
||

633 | |||

634 | Concerning specification, a similar process is applied, replacing an |
||

635 | expression by a list of local variables and definitions |
||

636 | *) |
||

637 | |||

638 | (** normalize_node node returns a normalized node, |
||

639 | ie. |
||

640 | af5af1e8 | ploc | - updated locals |

641 | - new equations |
||

642 | 8deaa2dd | tkahsai | - |

643 | af5af1e8 | ploc | *) |

644 | 949b2e1e | ploc | let normalize_node decls node = |

645 | 7065d912 | ploc | reset_cpt_fresh (); |

646 | 59020713 | ploc | let orig_vars = node.node_inputs@node.node_outputs@node.node_locals in |

647 | 50dadc21 | ploc | let not_is_orig_var v = |

648 | List.for_all ((!=) v) orig_vars in |
||

649 | 95944ba1 | ploc | let norm_ctx = { |

650 | parentid = node.node_id; |
||

651 | vars = get_node_vars node; |
||

652 | is_output = (fun vid -> List.exists (fun v -> v.var_id = vid) node.node_outputs); |
||

653 | } |
||

654 | in |
||

655 | f4cba4b8 | ploc | |

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

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

658 | let spec, new_vars, eqs = |
||

659 | begin |
||

660 | (* Update mutable fields of eexpr to perform normalization of |
||

661 | specification. |
||

662 | |||

663 | Careful: we do not normalize annotations, since they can have the form |
||

664 | x = (a, b, c) *) |
||

665 | match node.node_spec with |
||

666 | | None |
||

667 | | Some (NodeSpec _) -> node.node_spec, [], eqs |
||

668 | | Some (Contract s) -> |
||

669 | let new_locals, new_stmts, s' = normalize_spec |
||

670 | decls |
||

671 | node.node_id |
||

672 | (node.node_inputs, node.node_outputs, node.node_locals) |
||

673 | s |
||

674 | in |
||

675 | 1fd3d002 | ploc | (* Format.eprintf "Normalization bounded new locals: %a@." Printers.pp_vars new_locals; |

676 | * Format.eprintf "Normalization bounded stmts: %a@." Printers.pp_node_eqs new_stmts; *) |
||

677 | f4cba4b8 | ploc | Some (Contract s'), new_locals, new_stmts@eqs |

678 | end |
||

679 | in |
||

680 | 8deaa2dd | tkahsai | let defs, vars = |

681 | f4cba4b8 | ploc | List.fold_left (normalize_eq norm_ctx) ([], new_vars@orig_vars) eqs in |

682 | af5af1e8 | ploc | (* Normalize the asserts *) |

683 | 8deaa2dd | tkahsai | let vars, assert_defs, asserts = |

684 | af5af1e8 | ploc | List.fold_left ( |

685 | f4cba4b8 | ploc | fun (vars, def_accu, assert_accu) assert_ -> |

686 | 50dadc21 | ploc | let assert_expr = assert_.assert_expr in |

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

688 | normalize_expr |
||

689 | ~alias:true (* forcing introduction of new equations for fcn calls *) |
||

690 | 95944ba1 | ploc | norm_ctx |

691 | 50dadc21 | ploc | [] (* empty offset for arrays *) |

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

693 | assert_expr |
||

694 | in |
||

695 | f4cba4b8 | ploc | (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*) |

696 | 50dadc21 | ploc | vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu |

697 | f4cba4b8 | ploc | ) (vars, [], []) node.node_asserts in |

698 | 50dadc21 | ploc | let new_locals = List.filter not_is_orig_var vars in (* we filter out inout |

699 | vars and initial locals ones *) |
||

700 | 66359a5e | ploc | |

701 | let all_locals = node.node_locals @ new_locals in (* we add again, at the |
||

702 | 50dadc21 | ploc | beginning of the list the |

703 | local declared ones *) |
||

704 | 8deaa2dd | tkahsai | (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*) |

705 | f2b1c245 | ploc | |

706 | 66359a5e | ploc | |

707 | (* Updating annotations: traceability and machine types for fresh variables *) |
||

708 | |||

709 | (* Compute traceability info: |
||

710 | - gather newly bound variables |
||

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

712 | f4cba4b8 | ploc | *) |

713 | ea1c2906 | ploc | let new_annots = |

714 | if !Options.traces then |
||

715 | begin |
||

716 | 66359a5e | ploc | let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) all_locals in |

717 | ea1c2906 | ploc | let norm_traceability = { |

718 | f4cba4b8 | ploc | annots = List.map (fun v -> |

719 | let eq = |
||

720 | try |
||

721 | List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) |
||

722 | with Not_found -> |
||

723 | ( |
||

724 | Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; |
||

725 | assert false |
||

726 | ) |
||

727 | in |
||

728 | let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in |
||

729 | let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in |
||

730 | Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"]; |
||

731 | (["traceability"], pair) |
||

732 | ) diff_vars; |
||

733 | annot_loc = Location.dummy_loc |
||

734 | } |
||

735 | ea1c2906 | ploc | in |

736 | norm_traceability::node.node_annot |
||

737 | end |
||

738 | else |
||

739 | node.node_annot |
||

740 | af5af1e8 | ploc | in |

741 | ea1c2906 | ploc | |

742 | 66359a5e | ploc | let new_annots = |

743 | List.fold_left (fun annots v -> |
||

744 | f4cba4b8 | ploc | if Machine_types.is_active && Machine_types.is_exportable v then |

745 | let typ = Machine_types.get_specified_type v in |
||

746 | let typ_name = Machine_types.type_name typ in |
||

747 | |||

748 | let loc = v.var_loc in |
||

749 | let typ_as_string = |
||

750 | mkexpr |
||

751 | loc |
||

752 | (Expr_const |
||

753 | (Const_string typ_name)) |
||

754 | in |
||

755 | let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in |
||

756 | Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword; |
||

757 | {annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots |
||

758 | else |
||

759 | annots |
||

760 | ) new_annots new_locals |
||

761 | 95944ba1 | ploc | in |

762 | |||

763 | 949b2e1e | ploc | |

764 | 22fe1c93 | ploc | let node = |

765 | 50dadc21 | ploc | { node with |

766 | 66359a5e | ploc | node_locals = all_locals; |

767 | 50dadc21 | ploc | node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs); |

768 | node_asserts = asserts; |
||

769 | node_annot = new_annots; |
||

770 | 95944ba1 | ploc | node_spec = spec; |

771 | 50dadc21 | ploc | } |

772 | 8deaa2dd | tkahsai | in ((*Printers.pp_node Format.err_formatter node;*) |

773 | f4cba4b8 | ploc | node |

774 | ) |
||

775 | f2b1c245 | ploc | |

776 | 95944ba1 | ploc | let normalize_inode decls nd = |

777 | reset_cpt_fresh (); |
||

778 | match nd.nodei_spec with |
||

779 | f4cba4b8 | ploc | None | Some (NodeSpec _) -> nd |

780 | | Some (Contract _) -> assert false |
||

781 | |||

782 | 82906771 | ploc | let normalize_decl (decls: program_t) (decl: top_decl) : top_decl = |

783 | 22fe1c93 | ploc | match decl.top_decl_desc with |

784 | | Node nd -> |
||

785 | 95944ba1 | ploc | let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in |

786 | update_node nd.node_id decl'; |
||

787 | decl' |
||

788 | | ImportedNode nd -> |
||

789 | let decl' = {decl with top_decl_desc = ImportedNode (normalize_inode decls nd)} in |
||

790 | update_node nd.nodei_id decl'; |
||

791 | decl' |
||

792 | |||

793 | | Include _| Open _ | Const _ | TypeDef _ -> decl |
||

794 | 8deaa2dd | tkahsai | |

795 | ad4774b0 | ploc | let normalize_prog p decls = |

796 | 27dc3869 | ploc | (* Backend specific configurations for normalization *) |

797 | ad4774b0 | ploc | params := p; |

798 | 22fe1c93 | ploc | |

799 | 27dc3869 | ploc | (* Main algorithm: iterates over nodes *) |

800 | 82906771 | ploc | List.map (normalize_decl decls) decls |

801 | ad4774b0 | ploc | |

802 | 95944ba1 | ploc | |

803 | (* Fake interface for outside uses *) |
||

804 | let mk_expr_alias_opt opt (parentid, ctx_vars) (defs, vars) expr = |
||

805 | mk_expr_alias_opt |
||

806 | opt |
||

807 | {parentid = parentid; vars = ctx_vars; is_output = (fun _ -> false) } |
||

808 | (defs, vars) |
||

809 | expr |
||

810 | |||

811 | ad4774b0 | ploc | |

812 | (* Local Variables: *) |
||

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

814 | (* End: *) |
||

815 |