Revision ca7ff3f7
Added by LĂ©lio Brun over 1 year ago
src/normalization.ml  

16  16  
17  17 
(* To update thank to some command line options *) 
18  18 
let debug = ref false 
19 


19  
20  20 
(** Normalisation iters through the AST of expressions and bind fresh definition 
21  21 
when some criteria are met. This creation of fresh definition is performed by 
22  22 
the function mk_expr_alias_opt when the alias argument is on. 
...  ...  
32  32 
definitions. 
33  33 
*) 
34  34  
35 
type param_t = 

36 
{ 

37 
unfold_arrow_active: bool; 

38 
force_alias_ite: bool; 

39 
force_alias_internal_fun: bool; 

40 
} 

35 
type param_t = { 

36 
unfold_arrow_active : bool; 

37 
force_alias_ite : bool; 

38 
force_alias_internal_fun : bool; 

39 
} 

40  
41 
let params = 

42 
ref 

43 
{ 

44 
unfold_arrow_active = false; 

45 
force_alias_ite = false; 

46 
force_alias_internal_fun = false; 

47 
} 

41  48  
42 
let params = ref 

43 
{ 

44 
unfold_arrow_active = false; 

45 
force_alias_ite = false; 

46 
force_alias_internal_fun =false; 

47 
} 

49 
type norm_ctx_t = { 

50 
parentid : ident; 

51 
vars : var_decl list; 

52 
is_output : ident > bool; 

53 
} 

48  54  
49 
type norm_ctx_t =


55 
let expr_true loc ck =


50  56 
{ 
51 
parentid: ident; 

52 
vars: var_decl list; 

53 
is_output: ident > bool; 

57 
expr_tag = Utils.new_tag (); 

58 
expr_desc = Expr_const (Const_tag tag_true); 

59 
expr_type = Type_predef.type_bool; 

60 
expr_clock = ck; 

61 
expr_delay = Delay.new_var (); 

62 
expr_annot = None; 

63 
expr_loc = loc; 

54  64 
} 
55  65  
56 


57 
let expr_true loc ck = 

58 
{ expr_tag = Utils.new_tag (); 

59 
expr_desc = Expr_const (Const_tag tag_true); 

60 
expr_type = Type_predef.type_bool; 

61 
expr_clock = ck; 

62 
expr_delay = Delay.new_var (); 

63 
expr_annot = None; 

64 
expr_loc = loc } 

65  
66  66 
let expr_false loc ck = 
67 
{ expr_tag = Utils.new_tag (); 

68 
expr_desc = Expr_const (Const_tag tag_false); 

69 
expr_type = Type_predef.type_bool; 

70 
expr_clock = ck; 

71 
expr_delay = Delay.new_var (); 

72 
expr_annot = None; 

73 
expr_loc = loc } 

67 
{ 

68 
expr_tag = Utils.new_tag (); 

69 
expr_desc = Expr_const (Const_tag tag_false); 

70 
expr_type = Type_predef.type_bool; 

71 
expr_clock = ck; 

72 
expr_delay = Delay.new_var (); 

73 
expr_annot = None; 

74 
expr_loc = loc; 

75 
} 

74  76  
75  77 
let expr_once loc ck = 
76 
{ expr_tag = Utils.new_tag (); 

77 
expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck); 

78 
expr_type = Type_predef.type_bool; 

79 
expr_clock = ck; 

80 
expr_delay = Delay.new_var (); 

81 
expr_annot = None; 

82 
expr_loc = loc } 

78 
{ 

79 
expr_tag = Utils.new_tag (); 

80 
expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck); 

81 
expr_type = Type_predef.type_bool; 

82 
expr_clock = ck; 

83 
expr_delay = Delay.new_var (); 

84 
expr_annot = None; 

85 
expr_loc = loc; 

86 
} 

83  87  
84  88 
let is_expr_once = 
85  89 
let dummy_expr_once = expr_once Location.dummy_loc (Clocks.new_var true) in 
86  90 
fun expr > Corelang.is_eq_expr expr dummy_expr_once 
87  91  
88  92 
let unfold_arrow expr = 
89 
match expr.expr_desc with 

90 
 Expr_arrow (e1, e2) > 

91 
let loc = expr.expr_loc in 

92 
let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in 

93 
{ expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) } 

94 
 _ > assert false 

95  
96  
93 
match expr.expr_desc with 

94 
 Expr_arrow (e1, e2) > 

95 
let loc = expr.expr_loc in 

96 
let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in 

97 
{ expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) } 

98 
 _ > assert false 

97  99  
98  100 
(* Get the equation in [defs] with [expr] as rhs, if any *) 
99  101 
let get_expr_alias defs expr = 
100 
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) 

101 
with 

102 
 Not_found > None 

103 


102 
try 

103 
Some 

104 
(List.find 

105 
(fun eq > 

106 
Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock 

107 
&& is_eq_expr eq.eq_rhs expr) 

108 
defs) 

109 
with Not_found > None 

110  
104  111 
(* Replace [expr] with (tuple of) [locals] *) 
105  112 
let replace_expr locals expr = 
106 
match locals with 

107 
 [] > assert false 

108 
 [v] > { expr with 

109 
expr_tag = Utils.new_tag (); 

110 
expr_desc = Expr_ident v.var_id } 

111 
 _ > { expr with 

112 
expr_tag = Utils.new_tag (); 

113 
expr_desc = Expr_tuple (List.map expr_of_vdecl locals) } 

113 
match locals with 

114 
 [] > assert false 

115 
 [ v ] > 

116 
{ expr with expr_tag = Utils.new_tag (); expr_desc = Expr_ident v.var_id } 

117 
 _ > 

118 
{ 

119 
expr with 

120 
expr_tag = Utils.new_tag (); 

121 
expr_desc = Expr_tuple (List.map expr_of_vdecl locals); 

122 
} 

114  123  
115 


116  124 
(* IS IT USED ? TODO 
117  125 
(* Create an alias for [expr], if none exists yet *) 
118  126 
let mk_expr_alias (parentid, vars) (defs, vars) expr = 
...  ...  
133  141 
(* 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; *) 
134  142 
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr 
135  143 
*) 
136 


144  
137  145 
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident) 
138  146 
and [opt] is true 
139  147  
...  ...  
141  149 
*) 
142  150 
let mk_expr_alias_opt opt norm_ctx (defs, vars) expr = 
143  151 
if !debug then 
144 
Log.report ~plugin:"normalization" ~level:2 

145 
(fun fmt > Format.fprintf fmt "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); 

152 
Log.report ~plugin:"normalization" ~level:2 (fun fmt > 

153 
Format.fprintf fmt "mk_expr_alias_opt %B %a %a %a@." opt 

154 
Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck 

155 
expr.expr_clock); 

146  156 
match expr.expr_desc with 
147 
 Expr_ident _ > 

148 
(defs, vars), expr 

149 
 _ > 

150 
match get_expr_alias defs expr with 

151 
 Some eq > 

152 
(* Format.eprintf "Found a preexisting definition@."; *) 

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

154 
(defs, vars), replace_expr aliases expr 

155 
 None > 

156 
(* Format.eprintf "Didnt found a preexisting definition (opt=%b)@." opt; 

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

158 
* (fprintf_list ~sep:"@ "(fun fmt eq > 

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

160 
* Clocks.print_ck eq.eq_rhs.expr_clock 

161 
* (Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock) 

162 
* (is_eq_expr eq.eq_rhs expr) 

163 
* Printers.pp_node_eq eq)) 

164 
* defs; *) 

165 
if opt 

166 
then 

167 
let new_aliases = 

168 
List.map2 

169 
(mk_fresh_var (norm_ctx.parentid, (norm_ctx.vars@vars)) expr.expr_loc) 

170 
(Types.type_list_of_type expr.expr_type) 

171 
(Clocks.clock_list_of_clock expr.expr_clock) in 

172 
let new_def = 

173 
mkeq expr.expr_loc (List.map (fun v > v.var_id) new_aliases, expr) 

174 
in 

175 
(* Typing and Registering machine type *) 

176 
let _ = if Machine_types.is_active then 

177 
Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr 

178 
in 

179 
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr 

180 
else 

181 
(defs, vars), expr 

182  
183 
(* Similar fonctions for dimensions *) 

157 
 Expr_ident _ > (defs, vars), expr 

158 
 _ > ( 

159 
match get_expr_alias defs expr with 

160 
 Some eq > 

161 
(* Format.eprintf "Found a preexisting definition@."; *) 

162 
let aliases = 

163 
List.map 

164 
(fun id > List.find (fun v > v.var_id = id) vars) 

165 
eq.eq_lhs 

166 
in 

167 
(defs, vars), replace_expr aliases expr 

168 
 None > 

169 
(* 

170 
Format.eprintf "Didnt found a preexisting definition (opt=%b)@." opt; 

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

172 
* (fprintf_list ~sep:"@ "(fun fmt eq > 

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

174 
* Clocks.print_ck eq.eq_rhs.expr_clock 

175 
* (Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock) 

176 
* (is_eq_expr eq.eq_rhs expr) 

177 
* Printers.pp_node_eq eq)) 

178 
* defs; *) 

179 
if opt then 

180 
let new_aliases = 

181 
List.map2 

182 
(mk_fresh_var 

183 
(norm_ctx.parentid, norm_ctx.vars @ vars) 

184 
expr.expr_loc) 

185 
(Types.type_list_of_type expr.expr_type) 

186 
(Clocks.clock_list_of_clock expr.expr_clock) 

187 
in 

188 
let new_def = 

189 
mkeq expr.expr_loc (List.map (fun v > v.var_id) new_aliases, expr) 

190 
in 

191 
(* Typing and Registering machine type *) 

192 
let _ = 

193 
if Machine_types.is_active then 

194 
Machine_types.type_def 

195 
(norm_ctx.parentid, norm_ctx.vars) 

196 
new_aliases expr 

197 
in 

198 
(new_def :: defs, new_aliases @ vars), replace_expr new_aliases expr 

199 
else (defs, vars), expr) 

200  
201 
(* Similar fonctions for dimensions *) 

184  202 
let mk_dim_alias opt norm_ctx (defs, vars) dim = 
185  203 
match dim.Dimension.dim_desc with 
186 
 Dimension.Dbool _  Dint _ 

187 
 Dident _ > (defs, vars), dim (* Keep the same *)


188 
 _ when opt > (* Cast to expression, normalizing *)


189 
let e = expr_of_dimension dim in


190 
let defvars, e = mk_expr_alias_opt true norm_ctx (defs, vars) e in


191 
defvars, dimension_of_expr e


192  
193 
 _ > (defs, vars), dim (* Keep the same *)


194  
204 
 Dimension.Dbool _  Dint _  Dident _ >


205 
(defs, vars), dim (* Keep the same *)


206 
 _ when opt > 

207 
(* Cast to expression, normalizing *)


208 
let e = expr_of_dimension dim in


209 
let defvars, e = mk_expr_alias_opt true norm_ctx (defs, vars) e in


210 
defvars, dimension_of_expr e 

211 
 _ > (defs, vars), dim 

212 
(* Keep the same *) 

195  213  
196  214 
let unfold_offsets norm_ctx defvars e offsets = 
197  215 
let add_offset (defvars, e) d = 
198  216 
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d; *) 
199 
let defvars, d = mk_dim_alias !params.force_alias_internal_fun norm_ctx defvars d in 

200 
let new_e = 

201 
{ e with 

217 
let defvars, d = 

218 
mk_dim_alias !params.force_alias_internal_fun norm_ctx defvars d 

219 
in 

220 
let new_e = 

221 
{ 

222 
e with 

202  223 
expr_tag = Utils.new_tag (); 
203  224 
expr_loc = d.Dimension.dim_loc; 
204  225 
expr_type = Types.array_element_type e.expr_type; 
205 
expr_desc = Expr_access (e, d) } 

226 
expr_desc = Expr_access (e, d); 

227 
} 

206  228 
in 
207  229 
defvars, new_e 
208 
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *) 

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


209  231 
in 
210 
List.fold_left add_offset (defvars, e) offsets


232 
List.fold_left add_offset (defvars, e) offsets 

211  233  
212 


213  234 
(* Create a (normalized) expression from [ref_e], 
214  235 
replacing description with [norm_d], 
215  236 
taking propagated [offsets] into account 
216  237 
in order to change expression type *) 
217  238 
let mk_norm_expr offsets ref_e norm_d = 
218  239 
(*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*) 
219 
let drop_array_type ty = 

220 
Types.map_tuple_type Types.array_element_type ty in


221 
{ ref_e with


240 
let drop_array_type ty = Types.map_tuple_type Types.array_element_type ty in


241 
{


242 
ref_e with


222  243 
expr_desc = norm_d; 
223 
expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type } 

224 


244 
expr_type = 

245 
Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type; 

246 
} 

247  
225  248 
(* normalize_<foo> : defs * used vars > <foo> > (updated defs * updated vars) * normalized <foo> *) 
226  249 
let normalize_list alias norm_ctx offsets norm_element defvars elist = 
227  250 
List.fold_right 
228  251 
(fun t (defvars, qlist) > 
229  252 
let defvars, norm_t = norm_element alias norm_ctx offsets defvars t in 
230 
(defvars, norm_t :: qlist)


231 
) elist (defvars, [])


253 
defvars, norm_t :: qlist) 

254 
elist (defvars, []) 

232  255  
233 
let rec normalize_expr ?(alias=true) ?(alias_basic=false) norm_ctx offsets defvars expr = 

256 
let rec normalize_expr ?(alias = true) ?(alias_basic = false) norm_ctx offsets 

257 
defvars expr = 

234  258 
(* 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; *) 
235  259 
match expr.expr_desc with 
236 
 Expr_const _ 

237 
 Expr_ident _ > 

238 
unfold_offsets norm_ctx defvars expr offsets 

260 
 Expr_const _  Expr_ident _ > unfold_offsets norm_ctx defvars expr offsets 

239  261 
 Expr_array elist > 
240 
let defvars, norm_elist = normalize_list alias norm_ctx offsets (fun _ > normalize_array_expr ~alias:true) defvars elist in 

241 
let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in 

242 
mk_expr_alias_opt alias norm_ctx defvars norm_expr 

262 
let defvars, norm_elist = 

263 
normalize_list alias norm_ctx offsets 

264 
(fun _ > normalize_array_expr ~alias:true) 

265 
defvars elist 

266 
in 

267 
let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in 

268 
mk_expr_alias_opt alias norm_ctx defvars norm_expr 

243  269 
 Expr_power (e1, d) when offsets = [] > 
244 
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in 

245 
let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in 

246 
mk_expr_alias_opt alias norm_ctx defvars norm_expr 

270 
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in


271 
let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in


272 
mk_expr_alias_opt alias norm_ctx defvars norm_expr


247  273 
 Expr_power (e1, _) > 
248 
normalize_expr ~alias:alias norm_ctx (List.tl offsets) defvars e1


274 
normalize_expr ~alias norm_ctx (List.tl offsets) defvars e1


249  275 
 Expr_access (e1, d) > 
250 
normalize_expr ~alias:alias norm_ctx (d::offsets) defvars e1 

251 


276 
normalize_expr ~alias norm_ctx (d :: offsets) defvars e1 

252  277 
 Expr_tuple elist > 
253 
let defvars, norm_elist = 

254 
normalize_list alias norm_ctx offsets (fun alias > normalize_expr ~alias:alias ~alias_basic:false) defvars elist in 

255 
defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist) 

278 
let defvars, norm_elist = 

279 
normalize_list alias norm_ctx offsets 

280 
(fun alias > normalize_expr ~alias ~alias_basic:false) 

281 
defvars elist 

282 
in 

283 
defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist) 

256  284 
 Expr_appl (id, args, None) 
257 
when Basic_library.is_homomorphic_fun id 

258 
&& Types.is_array_type expr.expr_type > 

259 
let defvars, norm_args = 

260 
normalize_list 

261 
alias 

262 
norm_ctx 

263 
offsets 

264 
(fun _ > normalize_array_expr ~alias:true) 

265 
defvars 

266 
(expr_list_of_expr args) 

267 
in 

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

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

270 
&& not (!params.force_alias_internal_fun  alias_basic) > 

271 
let defvars, norm_args = normalize_expr ~alias:true norm_ctx offsets defvars args in 

272 
defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None)) 

285 
when Basic_library.is_homomorphic_fun id 

286 
&& Types.is_array_type expr.expr_type > 

287 
let defvars, norm_args = 

288 
normalize_list alias norm_ctx offsets 

289 
(fun _ > normalize_array_expr ~alias:true) 

290 
defvars (expr_list_of_expr args) 

291 
in 

292 
( defvars, 

293 
mk_norm_expr offsets expr 

294 
(Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) ) 

295 
 Expr_appl (id, args, None) 

296 
when Basic_library.is_expr_internal_fun expr 

297 
&& not (!params.force_alias_internal_fun  alias_basic) > 

298 
let defvars, norm_args = 

299 
normalize_expr ~alias:true norm_ctx offsets defvars args 

300 
in 

301 
defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None)) 

273  302 
 Expr_appl (id, args, r) > 
274 
let defvars, r = 

275 
match r with 

276 
 None > defvars, None 

277 
 Some r > 

278 
let defvars, norm_r = normalize_expr ~alias_basic:true norm_ctx [] defvars r in 

279 
defvars, Some norm_r 

280 
in 

281 
let defvars, norm_args = normalize_expr norm_ctx [] defvars args in 

282 
let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in 

283 
if offsets <> [] 

284 
then 

285 
let defvars, norm_expr = normalize_expr norm_ctx [] defvars norm_expr in 

286 
normalize_expr ~alias:alias norm_ctx offsets defvars norm_expr 

287 
else 

288 
mk_expr_alias_opt (alias && (!params.force_alias_internal_fun  alias_basic 

289 
 not (Basic_library.is_expr_internal_fun expr))) 

290 
norm_ctx defvars norm_expr 

303 
let defvars, r = 

304 
match r with 

305 
 None > defvars, None 

306 
 Some r > 

307 
let defvars, norm_r = 

308 
normalize_expr ~alias_basic:true norm_ctx [] defvars r 

309 
in 

310 
defvars, Some norm_r 

311 
in 

312 
let defvars, norm_args = normalize_expr norm_ctx [] defvars args in 

313 
let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in 

314 
if offsets <> [] then 

315 
let defvars, norm_expr = normalize_expr norm_ctx [] defvars norm_expr in 

316 
normalize_expr ~alias norm_ctx offsets defvars norm_expr 

317 
else 

318 
mk_expr_alias_opt 

319 
(alias 

320 
&& (!params.force_alias_internal_fun  alias_basic 

321 
 not (Basic_library.is_expr_internal_fun expr))) 

322 
norm_ctx defvars norm_expr 

291  323 
 Expr_arrow _ when !params.unfold_arrow_active && not (is_expr_once expr) > 
292 
(* Here we differ from Colaco paper: arrows are pushed to the top *) 

293 
normalize_expr ~alias:alias norm_ctx offsets defvars (unfold_arrow expr) 

294 
 Expr_arrow (e1,e2) > 

295 
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in 

296 
let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in 

297 
let norm_expr = mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) in 

298 
mk_expr_alias_opt alias norm_ctx defvars norm_expr 

324 
(* Here we differ from Colaco paper: arrows are pushed to the top *) 

325 
normalize_expr ~alias norm_ctx offsets defvars (unfold_arrow expr) 

326 
 Expr_arrow (e1, e2) > 

327 
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in 

328 
let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in 

329 
let norm_expr = 

330 
mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) 

331 
in 

332 
mk_expr_alias_opt alias norm_ctx defvars norm_expr 

299  333 
 Expr_pre e > 
300 
let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in 

301 
let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in 

302 
mk_expr_alias_opt alias norm_ctx defvars norm_expr 

334 
let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in


335 
let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in


336 
mk_expr_alias_opt alias norm_ctx defvars norm_expr


303  337 
 Expr_fby (e1, e2) > 
304 
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in 

305 
let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in 

306 
let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in 

307 
mk_expr_alias_opt alias norm_ctx defvars norm_expr 

338 
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in


339 
let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in


340 
let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in


341 
mk_expr_alias_opt alias norm_ctx defvars norm_expr


308  342 
 Expr_when (e, c, l) > 
309 
let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in 

310 
defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l)) 

343 
let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in


344 
defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l))


311  345 
 Expr_ite (c, t, e) > 
312 
let defvars, norm_c = normalize_guard norm_ctx defvars c in 

313 
let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in 

314 
let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in 

315 
let norm_expr = mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) in 

316 
mk_expr_alias_opt alias norm_ctx defvars norm_expr 

346 
let defvars, norm_c = normalize_guard norm_ctx defvars c in 

347 
let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in 

348 
let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in 

349 
let norm_expr = 

350 
mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) 

351 
in 

352 
mk_expr_alias_opt alias norm_ctx defvars norm_expr 

317  353 
 Expr_merge (c, hl) > 
318 
let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in 

319 
let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in 

320 
mk_expr_alias_opt alias norm_ctx defvars norm_expr 

354 
let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in


355 
let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in


356 
mk_expr_alias_opt alias norm_ctx defvars norm_expr


321  357  
322  358 
(* Creates a conditional with a merge construct, which is more lazy *) 
323  359 
(* 
...  ...  
330  366 
and normalize_branches norm_ctx offsets defvars hl = 
331  367 
List.fold_right 
332  368 
(fun (t, h) (defvars, norm_q) > 
333 
let (defvars, norm_h) = normalize_cond_expr norm_ctx offsets defvars h in 

334 
defvars, (t, norm_h) :: norm_q 

335 
) 

369 
let defvars, norm_h = normalize_cond_expr norm_ctx offsets defvars h in 

370 
defvars, (t, norm_h) :: norm_q) 

336  371 
hl (defvars, []) 
337  372  
338 
and normalize_array_expr ?(alias=true) norm_ctx offsets defvars expr =


373 
and normalize_array_expr ?(alias = true) norm_ctx offsets defvars expr =


339  374 
(*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*) 
340  375 
match expr.expr_desc with 
341  376 
 Expr_power (e1, d) when offsets = [] > 
342 
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in 

343 
defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d)) 

377 
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in


378 
defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))


344  379 
 Expr_power (e1, _) > 
345 
normalize_array_expr ~alias:alias norm_ctx (List.tl offsets) defvars e1 

346 
 Expr_access (e1, d) > normalize_array_expr ~alias:alias norm_ctx (d::offsets) defvars e1 

380 
normalize_array_expr ~alias norm_ctx (List.tl offsets) defvars e1 

381 
 Expr_access (e1, d) > 

382 
normalize_array_expr ~alias norm_ctx (d :: offsets) defvars e1 

347  383 
 Expr_array elist when offsets = [] > 
348 
let defvars, norm_elist = normalize_list alias norm_ctx offsets (fun _ > normalize_array_expr ~alias:true) defvars elist in 

349 
defvars, mk_norm_expr offsets expr (Expr_array norm_elist) 

384 
let defvars, norm_elist = 

385 
normalize_list alias norm_ctx offsets 

386 
(fun _ > normalize_array_expr ~alias:true) 

387 
defvars elist 

388 
in 

389 
defvars, mk_norm_expr offsets expr (Expr_array norm_elist) 

350  390 
 Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr > 
351 
let defvars, norm_args = normalize_list alias norm_ctx offsets (fun _ > normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in 

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

353 
 _ > normalize_expr ~alias:alias norm_ctx offsets defvars expr 

354  
355 
and normalize_cond_expr ?(alias=true) norm_ctx offsets defvars expr = 

391 
let defvars, norm_args = 

392 
normalize_list alias norm_ctx offsets 

393 
(fun _ > normalize_array_expr ~alias:true) 

394 
defvars (expr_list_of_expr args) 

395 
in 

396 
( defvars, 

397 
mk_norm_expr offsets expr 

398 
(Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) ) 

399 
 _ > normalize_expr ~alias norm_ctx offsets defvars expr 

400  
401 
and normalize_cond_expr ?(alias = true) norm_ctx offsets defvars expr = 

356  402 
(* Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets; *) 
357  403 
match expr.expr_desc with 
358  404 
 Expr_access (e1, d) > 
359 
normalize_cond_expr ~alias:alias norm_ctx (d::offsets) defvars e1


405 
normalize_cond_expr ~alias norm_ctx (d :: offsets) defvars e1


360  406 
 Expr_ite (c, t, e) > 
361 
let defvars, norm_c = normalize_guard norm_ctx defvars c in 

362 
let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in 

363 
let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in 

364 
defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) 

407 
let defvars, norm_c = normalize_guard norm_ctx defvars c in


408 
let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in


409 
let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in


410 
defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e))


365  411 
 Expr_merge (c, hl) > 
366 
let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in 

367 
defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) 

412 
let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in


413 
defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl))


368  414 
 _ when !params.force_alias_ite > 
369 
(* Forcing alias creation for then/else expressions *) 

370 
let defvars, norm_expr = 

371 
normalize_expr ~alias:alias norm_ctx offsets defvars expr 

372 
in 

373 
mk_expr_alias_opt true norm_ctx defvars norm_expr 

374 
 _ > (* default case without the force_alias_ite option *) 

375 
normalize_expr ~alias:alias norm_ctx offsets defvars expr 

376 


415 
(* Forcing alias creation for then/else expressions *) 

416 
let defvars, norm_expr = 

417 
normalize_expr ~alias norm_ctx offsets defvars expr 

418 
in 

419 
mk_expr_alias_opt true norm_ctx defvars norm_expr 

420 
 _ > 

421 
(* default case without the force_alias_ite option *) 

422 
normalize_expr ~alias norm_ctx offsets defvars expr 

423  
377  424 
and normalize_guard norm_ctx defvars expr = 
378 
let defvars, norm_expr = normalize_expr ~alias_basic:true norm_ctx [] defvars expr in 

425 
let defvars, norm_expr = 

426 
normalize_expr ~alias_basic:true norm_ctx [] defvars expr 

427 
in 

379  428 
mk_expr_alias_opt true norm_ctx defvars norm_expr 
380  429  
381  430 
(* outputs cannot be memories as well. If so, introduce new local variable. 
...  ...  
383  432 
let decouple_outputs norm_ctx defvars eq = 
384  433 
let rec fold_lhs defvars lhs tys cks = 
385  434 
match lhs, tys, cks with 
386 
 [], [], [] > defvars, [] 

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

388 
if norm_ctx.is_output v 

389 
then 

390 
let newvar = mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) eq.eq_loc t c in 

391 
let neweq = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in 

392 
(neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q 

393 
else 

394 
(defs_q, vars_q), v::lhs_q 

395 
 _ > assert false in 

435 
 [], [], [] > defvars, [] 

436 
 v :: qv, t :: qt, c :: qc > 

437 
let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in 

438 
if norm_ctx.is_output v then 

439 
let newvar = 

440 
mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) eq.eq_loc t c 

441 
in 

442 
let neweq = mkeq eq.eq_loc ([ v ], expr_of_vdecl newvar) in 

443 
(neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q 

444 
else (defs_q, vars_q), v :: lhs_q 

445 
 _ > assert false 

446 
in 

396  447 
let defvars', lhs' = 
397 
fold_lhs 

398 
defvars 

399 
eq.eq_lhs 

448 
fold_lhs defvars eq.eq_lhs 

400  449 
(Types.type_list_of_type eq.eq_rhs.expr_type) 
401 
(Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in 

402 
defvars', {eq with eq_lhs = lhs' } 

450 
(Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) 

451 
in 

452 
defvars', { eq with eq_lhs = lhs' } 

403  453  
404  454 
let normalize_eq norm_ctx defvars eq = 
405 
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*) 

455 
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)


406  456 
match eq.eq_rhs.expr_desc with 
407 
 Expr_pre _ 

408 
 Expr_fby _ > 

409 
let (defvars', eq') = decouple_outputs norm_ctx defvars eq in 

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

411 
let norm_eq = { eq' with eq_rhs = norm_rhs } in 

412 
(norm_eq::defs', vars') 

457 
 Expr_pre _  Expr_fby _ > 

458 
let defvars', eq' = decouple_outputs norm_ctx defvars eq in 

459 
let (defs', vars'), norm_rhs = 

460 
normalize_expr ~alias:false norm_ctx [] defvars' eq'.eq_rhs 

461 
in 

462 
let norm_eq = { eq' with eq_rhs = norm_rhs } in 

463 
norm_eq :: defs', vars' 

413  464 
 Expr_array _ > 
414 
let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in 

415 
let norm_eq = { eq with eq_rhs = norm_rhs } in 

416 
(norm_eq::defs', vars') 

417 
 Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type > 

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

419 
let norm_eq = { eq with eq_rhs = norm_rhs } in 

420 
(norm_eq::defs', vars') 

465 
let (defs', vars'), norm_rhs = 

466 
normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs 

467 
in 

468 
let norm_eq = { eq with eq_rhs = norm_rhs } in 

469 
norm_eq :: defs', vars' 

470 
 Expr_appl (id, _, None) 

471 
when Basic_library.is_homomorphic_fun id 

472 
&& Types.is_array_type eq.eq_rhs.expr_type > 

473 
let (defs', vars'), norm_rhs = 

474 
normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs 

475 
in 

476 
let norm_eq = { eq with eq_rhs = norm_rhs } in 

477 
norm_eq :: defs', vars' 

421  478 
 Expr_appl _ > 
422 
let (defs', vars'), norm_rhs = normalize_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in 

423 
let norm_eq = { eq with eq_rhs = norm_rhs } in 

424 
(norm_eq::defs', vars') 

479 
let (defs', vars'), norm_rhs = 

480 
normalize_expr ~alias:false norm_ctx [] defvars eq.eq_rhs 

481 
in 

482 
let norm_eq = { eq with eq_rhs = norm_rhs } in 

483 
norm_eq :: defs', vars' 

425  484 
 _ > 
426 
let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in 

427 
let norm_eq = { eq with eq_rhs = norm_rhs } in 

428 
norm_eq::defs', vars' 

485 
let (defs', vars'), norm_rhs = 

486 
normalize_cond_expr ~alias:false norm_ctx [] defvars eq.eq_rhs 

487 
in 

488 
let norm_eq = { eq with eq_rhs = norm_rhs } in 

489 
norm_eq :: defs', vars' 

429  490  
430  491 
let normalize_eq_split norm_ctx defvars eq = 
431  492 
try 
432  493 
let defs, vars = normalize_eq norm_ctx defvars eq in 
433 
List.fold_right (fun eq (def, vars) > 

494 
List.fold_right 

495 
(fun eq (def, vars) > 

434  496 
let eq_defs = Splitting.tuple_split_eq eq in 
435 
if eq_defs = [eq] then 

436 
eq::def, vars 

437 
else 

438 
List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs 

439 
) defs ([], vars) 

440 


441 
with ex > ( 

497 
if eq_defs = [ eq ] then eq :: def, vars 

498 
else List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs) 

499 
defs ([], vars) 

500 
with ex > 

442  501 
Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq; 
443  502 
raise ex 
444 
) 

445  503  
446  504 
(* Projecting an eexpr to an eexpr associated to a single 
447  505 
variable. Returns the updated ee, the bounded variable and the 
448  506 
associated statement *) 
449 
let normalize_pred_eexpr norm_ctx (def,vars) ee = 

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

507 
let normalize_pred_eexpr norm_ctx (def, vars) ee = 

508 
assert (ee.eexpr_quantifiers = []); 

509 
(* We do not normalize quantifiers yet. This is for very far future. *) 

451  510 
(* don't do anything is eexpr is just a variable *) 
452  511 
let skip = 
453  512 
match ee.eexpr_qfexpr.expr_desc with 
454  513 
 Expr_ident _  Expr_const _ > true 
455  514 
 _ > false 
456  515 
in 
457 
if skip then 

458 
ee, (def, vars) 

459 
else ( 

516 
if skip then ee, (def, vars) 

517 
else 

460  518 
(* New output variable *) 
461  519 
let output_id = "spec" ^ string_of_int ee.eexpr_tag in 
462 
let output_var = 

463 
mkvar_decl 

464 
ee.eexpr_loc 

465 
(output_id, 

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

467 
mkclock ee.eexpr_loc Ckdec_any, 

468 
false (* not a constant *), 

469 
None, 

470 
None 

471 
) 

520 
let output_var = 

521 
mkvar_decl ee.eexpr_loc 

522 
( output_id, 

523 
mktyp ee.eexpr_loc Tydec_bool, 

524 
(* It is a predicate, hence a bool *) 

525 
mkclock ee.eexpr_loc Ckdec_any, 

526 
false (* not a constant *), 

527 
None, 

528 
None ) 

472  529 
in 
473  530 
let output_expr = expr_of_vdecl output_var in 
474  531 
(* Rebuilding an eexpr with a silly expression, just a variable *) 
...  ...  
476  533  
477  534 
(* Now processing a fresh equation output_id = eexpr_qfexpr. We 
478  535 
inline possible calls within, normalize it and type/clock the 
479 
result. *) 

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

481  
536 
result. *) 

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

482  538  
483  539 
(* (\* Inlining any calls *\) 
484  540 
* let nodes = get_nodes decls in 
...  ...  
489  545 
* else 
490  546 
* assert false (\* TODO *\) 
491  547 
* in *) 
492 


548  
493  549 
(* Normalizing expr and eqs *) 
494 
let defs, vars = List.fold_left (normalize_eq_split norm_ctx) (def, vars) [eq] in 

495 
let vars = output_var :: vars in 

496 
(* let todefine = 

497 
List.fold_left 

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

499 
(ISet.add output_id ISet.empty) vars in 

500 
*) 

550 
let defs, vars = 

551 
List.fold_left (normalize_eq_split norm_ctx) (def, vars) [ eq ] 

552 
in 

553 
let vars = output_var :: vars in 

554  
555 
(* let todefine = 

556 
List.fold_left 

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

558 
(ISet.add output_id ISet.empty) vars in 

559 
*) 

501  560  
502  561 
(* Typing / Clocking *) 
503  562 
try 
504  563 
ignore (Typing.type_var_decl_list vars !Global.type_env vars); 
505 
(* 

564  
565 
(* 

506  566 
let env = Typing.type_var_decl [] !Global.type_env xxxx output_var in (* typing the variable *) 
507  567 
(* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *) 
508  568 
let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in 
...  ...  
515  575 
(*Format.eprintf "normalized eqs %a@.@?" 
516  576 
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs; *) 
517  577 
*) 
578 
ee', (defs, vars) 

579 
with Types.Error (loc, err) as exc > 

580 
eprintf "Typing error for eexpr %a: %a%a%a@." Printers.pp_eexpr ee 

581 
Types.pp_error err 

582 
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) 

583 
defs Location.pp_loc loc; 

518  584  
519 
ee', (defs, vars) 

520 


521 
with (Types.Error (loc,err)) as exc > 

522 
eprintf "Typing error for eexpr %a: %a%a%a@." 

523 
Printers.pp_eexpr ee 

524 
Types.pp_error err 

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

526 
Location.pp_loc loc 

527 


528 


529 
; 

530 
raise exc 

531 


532 
) 

533 


534 
(* 

585 
raise exc 

586  
587 
(* 

535  588 

536  589 
let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in 
537  590 
(* Calls are first inlined *) 
...  ...  
580  633 

581  634 
; 
582  635 
raise exc 
583 
*) 

584 


636 
*) 

585  637  
586 
(* We use node local vars to make sure we are creating fresh variables *)


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

587  639 
let normalize_spec parentid (in_vars, out_vars, l_vars) s = 
588  640 
(* Original set of variables actually visible from here: in/out and 
589  641 
spec locals (no node locals) *) 
590  642 
let orig_vars = in_vars @ out_vars @ s.locals in 
591  643 
(* Format.eprintf "NormSpec: init locals: %a@." Printers.pp_vars s.locals; *) 
592 
let not_is_orig_var v = 

593 
List.for_all ((!=) v) orig_vars in


594 
let norm_ctx = {


595 
parentid = parentid;


644 
let not_is_orig_var v = List.for_all (( != ) v) orig_vars in


645 
let norm_ctx =


646 
{


647 
parentid; 

596  648 
vars = in_vars @ out_vars @ l_vars; 
597 
is_output = (fun _ > false) (* no need to introduce fresh variables for outputs *); 

649 
is_output = 

650 
(fun _ > false) (* no need to introduce fresh variables for outputs *); 

598  651 
} 
599  652 
in 
600  653 
(* Normalizing existing stmts *) 
601 
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 

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

603 
let defsvars = 

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

654 
let eqs, auts = 

655 
List.fold_right 

656 
(fun s (el, al) > 

657 
match s with Eq e > e :: el, al  Aut a > el, a :: al) 

658 
s.stmts ([], []) 

605  659 
in 
660 
if auts != [] then assert false; 

661 
(* Automata should be expanded by now. *) 

662 
let defsvars = List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs in 

606  663 
(* Iterate through predicates and normalize them on the go, creating 
607  664 
fresh variables for any guarantees/assumes/require/ensure *) 
608  665 
let process_predicates l defvars = 
609  666 
(* Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd defvars); *) 
610 
let res = List.fold_right (fun ee (accu, defvars) > 

611 
let ee', defvars = normalize_pred_eexpr norm_ctx defvars ee in 

612 
ee'::accu, defvars 

613 
) l ([], defvars) 

667 
let res = 

668 
List.fold_right 

669 
(fun ee (accu, defvars) > 

670 
let ee', defvars = normalize_pred_eexpr norm_ctx defvars ee in 

671 
ee' :: accu, defvars) 

672 
l ([], defvars) 

614  673 
in 
615  674 
(* Format.eprintf "ProcStmt: %a@." Printers.pp_node_eqs (fst (snd res)); 
616  675 
* Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd (snd res)); *) 
617  676 
res 
618  677 
in 
619  678  
620 


621  679 
let assume', defsvars = process_predicates s.assume defsvars in 
622  680 
let guarantees', defsvars = process_predicates s.guarantees defsvars in 
623  681 
let modes', (defs, vars) = 
624 
List.fold_right (


625 
fun m (accu_m, defsvars) >


682 
List.fold_right 

683 
(fun m (accu_m, defsvars) >


626  684 
let require', defsvars = process_predicates m.require defsvars in 
627  685 
let ensure', defsvars = process_predicates m.ensure defsvars in 
628 
{ m with require = require'; ensure = ensure' }:: accu_m, defsvars


629 
) s.modes ([], defsvars)


686 
{ m with require = require'; ensure = ensure' } :: accu_m, defsvars)


687 
s.modes ([], defsvars) 

630  688 
in 
631 


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

633 
new_locals, defs, 

634 
{s with 

635 
(* locals = s.locals @ new_locals; *) 

636 
stmts = []; 

637 
assume = assume'; 

638 
guarantees = guarantees'; 

639 
modes = modes' 

640 
} 

689  
690 
let new_locals = List.filter not_is_orig_var vars in 

691 
(* removing inouts and initial locals ones *) 

692 
( new_locals, 

693 
defs, 

694 
{ 

695 
s with 

696 
(* locals = s.locals @ new_locals; *) 

697 
stmts = []; 

698 
assume = assume'; 

699 
guarantees = guarantees'; 

700 
modes = modes'; 

701 
} ) 

641  702 
(* let nee _ = () in 
642  703 
* (\*normalize_eexpr decls iovars in *\) 
643  704 
* List.iter nee s.assume; 
...  ...  
646  707 
* List.iter nee m.require; 
647  708 
* List.iter nee m.ensure 
648  709 
* ) s.modes; *) 
649 


650  710  
651 


652 


653 


654 


655  711 
(* The normalization phase introduces new local variables 
656  712 
 output cannot be memories. If this happen, new local variables acting as 
657  713 
memories are introduced. 
...  ...  
671  727 
*) 
672  728 
let normalize_node node = 
673  729 
reset_cpt_fresh (); 
674 
let orig_vars = node.node_inputs@node.node_outputs@node.node_locals in


675 
let not_is_orig_var v = 

676 
List.for_all ((!=) v) orig_vars in


677 
let norm_ctx = {


730 
let orig_vars = node.node_inputs @ node.node_outputs @ node.node_locals in


731 
let not_is_orig_var v = List.for_all (( != ) v) orig_vars in


732 
let norm_ctx =


733 
{


678  734 
parentid = node.node_id; 
679  735 
vars = get_node_vars node; 
680 
is_output = (fun vid > List.exists (fun v > v.var_id = vid) node.node_outputs); 

736 
is_output = 

737 
(fun vid > List.exists (fun v > v.var_id = vid) node.node_outputs); 

681  738 
} 
682  739 
in 
683  740  
684  741 
let eqs, auts = get_node_eqs node in 
685 
if auts != [] then assert false; (* Automata should be expanded by now. *) 

742 
if auts != [] then assert false; 

743 
(* Automata should be expanded by now. *) 

686  744 
let spec, new_vars, eqs = 
687 
begin 

688 
(* Update mutable fields of eexpr to perform normalization of 

689 
specification. 

690  
691 
Careful: we do not normalize annotations, since they can have the form 

692 
x = (a, b, c) *) 

693 
match node.node_spec with 

694 
 None 

695 
 Some (NodeSpec _) > node.node_spec, [], eqs 

696 
 Some (Contract s) > 

697 
let new_locals, new_stmts, s' = normalize_spec 

698 
node.node_id 

699 
(node.node_inputs, node.node_outputs, node.node_locals) 

700 
s 

701 
in 

702 
(* Format.eprintf "Normalization bounded new locals: %a@." Printers.pp_vars new_locals; 

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

704 
Some (Contract s'), new_locals, new_stmts@eqs 

705 
end 

745 
(* Update mutable fields of eexpr to perform normalization of 

746 
specification. 

747  
748 
Careful: we do not normalize annotations, since they can have the form 

749 
x = (a, b, c) *) 

750 
match node.node_spec with 

751 
 None  Some (NodeSpec _) > node.node_spec, [], eqs 

752 
 Some (Contract s) > 

753 
let new_locals, new_stmts, s' = 

754 
normalize_spec node.node_id 

755 
(node.node_inputs, node.node_outputs, node.node_locals) 

756 
s 

757 
in 

758 
(* Format.eprintf "Normalization bounded new locals: %a@." Printers.pp_vars new_locals; 

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

760 
Some (Contract s'), new_locals, new_stmts @ eqs 

706  761 
in 
707  762 
let defs, vars = 
708 
List.fold_left (normalize_eq norm_ctx) ([], new_vars@orig_vars) eqs in 

763 
List.fold_left (normalize_eq norm_ctx) ([], new_vars @ orig_vars) eqs 

764 
in 

709  765 
(* Normalize the asserts *) 
710  766 
let vars, assert_defs, asserts = 
711 
List.fold_left ( 

712 
fun (vars, def_accu, assert_accu) assert_ > 

713 
let assert_expr = assert_.assert_expr in 

714 
let (defs, vars'), expr = 

715 
normalize_expr 

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

717 
norm_ctx 

718 
[] (* empty offset for arrays *) 

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

720 
assert_expr 

721 
in 

767 
List.fold_left 

768 
(fun (vars, def_accu, assert_accu) assert_ > 

769 
let assert_expr = assert_.assert_expr in 

770 
let (defs, vars'), expr = 

771 
normalize_expr ~alias:true 

772 
(* forcing introduction of new equations for fcn calls *) 

773 
norm_ctx [] 

774 
(* empty offset for arrays *) 

775 
([], vars) 

776 
(* defvar only contains vars *) 

777 
assert_expr 

778 
in 

722  779 
(*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*) 
723 
vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu 

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

725 
let new_locals = List.filter not_is_orig_var vars in (* we filter out inout 

726 
vars and initial locals ones *) 

727 


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

729 
beginning of the list the 

730 
local declared ones *) 

731 
(*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*) 

780 
( vars', 

781 
defs @ def_accu, 

782 
{ assert_ with assert_expr = expr } :: assert_accu )) 

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

784 
in 

785 
let new_locals = List.filter not_is_orig_var vars in 

786  
787 
(* we filter out inout 

788 
vars and initial locals ones *) 

789 
let all_locals = node.node_locals @ new_locals in 

732  790  
791 
(* we add again, at the 

792 
beginning of the list the 

793 
local declared ones *) 

794 
(*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*) 

733  795  
734  796 
(* Updating annotations: traceability and machine types for fresh variables *) 
735 


797  
736  798 
(* Compute traceability info: 
737  799 
 gather newly bound variables 
738  800 
 compute the associated expression without aliases 
739 
*)


801 
*) 

740  802 
let new_annots = 
741  803 
if !Options.traces then 
742 
begin 

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

744 
let norm_traceability = { 

745 
annots = List.map (fun v > 

746 
let eq = 

747 
try 

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

749 
with Not_found > 

750 
( 

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

752 
assert false 

753 
) 

754 
in 

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

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

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

758 
(["traceability"], pair) 

759 
) diff_vars; 

760 
annot_loc = Location.dummy_loc 

761 
} 

762 
in 

763 
norm_traceability::node.node_annot 

764 
end 

765 
else 

766 
node.node_annot 

804 
let diff_vars = 

805 
List.filter (fun v > not (List.mem v node.node_locals)) all_locals 

806 
in 

807 
let norm_traceability = 

808 
{ 

809 
annots = 

810 
List.map 

811 
(fun v > 

812 
let eq = 

813 
try 

814 
List.find 

815 
(fun eq > 

816 
List.exists (fun v' > v' = v.var_id) eq.eq_lhs) 

817 
(defs @ assert_defs) 

818 
with Not_found > 

819 
Format.eprintf 

820 
"Traceability annotation generation: var %s not found@." 

821 
v.var_id; 

822 
assert false 

823 
in 

824 
let expr = 

825 
substitute_expr diff_vars (defs @ assert_defs) eq.eq_rhs 

826 
in 

827 
let pair = 

828 
mkeexpr expr.expr_loc 

829 
(mkexpr expr.expr_loc 

830 
(Expr_tuple 

831 
[ expr_of_ident v.var_id expr.expr_loc; expr ])) 

832 
in 

833 
Annotations.add_expr_ann node.node_id pair.eexpr_tag 

834 
[ "traceability" ]; 

835 
[ "traceability" ], pair) 

836 
diff_vars; 

837 
annot_loc = Location.dummy_loc; 

838 
} 

839 
in 

840 
norm_traceability :: node.node_annot 

841 
else node.node_annot 

767  842 
in 
768  843  
769  844 
let new_annots = 
770 
List.fold_left (fun annots v >


771 
if Machine_types.is_active && Machine_types.is_exportable v then


772 
let typ = Machine_types.get_specified_type v in


773 
let typ_name = Machine_types.type_name typ in


774  
775 
let loc = v.var_loc in 

776 
let typ_as_string =


777 
mkexpr


778 
loc


779 
(Expr_const


780 
(Const_string typ_name))


781 
in


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


783 
Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;


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


785 
else


786 
annots


787 
) new_annots new_locals


845 
List.fold_left 

846 
(fun annots v >


847 
if Machine_types.is_active && Machine_types.is_exportable v then (


848 
let typ = Machine_types.get_specified_type v in


849 
let typ_name = Machine_types.type_name typ in 

850  
851 
let loc = v.var_loc in


852 
let typ_as_string = mkexpr loc (Expr_const (Const_string typ_name)) in


853 
let pair =


854 
expr_to_eexpr


855 
(expr_of_expr_list loc [ expr_of_vdecl v; typ_as_string ])


856 
in


857 
Annotations.add_expr_ann node.node_id pair.eexpr_tag


858 
Machine_types.keyword;


859 
{ annots = [ Machine_types.keyword, pair ]; annot_loc = loc }


860 
:: annots)


861 
else annots)


862 
new_annots new_locals 

788  863 
in 
789 


790 


864  
791  865 
let node = 
792 
{ node with 

866 
{ 

867 
node with 

793  868 
node_locals = all_locals; 
794  869 
node_stmts = List.map (fun eq > Eq eq) (defs @ assert_defs); 
795  870 
node_asserts = asserts; 
796  871 
node_annot = new_annots; 
797  872 
node_spec = spec; 
798  873 
} 
799 
in ((*Printers.pp_node Format.err_formatter node;*)


800 
node


801 
)


874 
in 

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


876 
node


802  877  
803  878 
let normalize_inode nd = 
804  879 
reset_cpt_fresh (); 
805  880 
match nd.nodei_spec with 
806 
None  Some (NodeSpec _) > nd


807 
 Some (Contract _) > assert false


808 


809 
let normalize_decl (decl: top_decl) : top_decl = 

881 
 None  Some (NodeSpec _) > nd


882 
 Some (Contract _) > assert false 

883  
884 
let normalize_decl (decl : top_decl) : top_decl =


810  885 
match decl.top_decl_desc with 
811  886 
 Node nd > 
812 
let decl' = {decl with top_decl_desc = Node (normalize_node nd)} in


813 
update_node nd.node_id decl'; 

814 
decl' 

887 
let decl' = { decl with top_decl_desc = Node (normalize_node nd) } in


888 
update_node nd.node_id decl';


889 
decl'


815  890 
 ImportedNode nd > 
816 
let decl' = {decl with top_decl_desc = ImportedNode (normalize_inode nd)} in 

817 
update_node nd.nodei_id decl'; 

818 
decl' 

819 


820 
 Include _ Open _  Const _  TypeDef _ > decl 

891 
let decl' = 

892 
{ decl with top_decl_desc = ImportedNode (normalize_inode nd) } 

893 
in 

894 
update_node nd.nodei_id decl'; 

895 
decl' 

896 
 Include _  Open _  Const _  TypeDef _ > decl 

821  897  
822  898 
let normalize_prog p decls = 
823  899 
(* Backend specific configurations for normalization *) 
...  ...  
826  902 
(* Main algorithm: iterates over nodes *) 
827  903 
List.map normalize_decl decls 
828  904  
829  
830  905 
(* Fake interface for outside uses *) 
831  906 
let mk_expr_alias_opt opt (parentid, ctx_vars) (defs, vars) expr = 
832 
mk_expr_alias_opt 

833 
opt 

834 
{parentid = parentid; vars = ctx_vars; is_output = (fun _ > false) } 

835 
(defs, vars) 

836 
expr 

907 
mk_expr_alias_opt opt 

908 
{ parentid; vars = ctx_vars; is_output = (fun _ > false) } 

909 
(defs, vars) expr 

837  910  
838 


839 
(* Local Variables: *) 

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

841 
(* End: *) 

842 


911 
(* Local Variables: *) 

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

913 
(* End: *) 
Also available in: Unified diff
reformatting