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

1  1 
open Lustre_types 
2  2 
open Machine_code_types 
3  3 
open Machine_code_common 
4  
4  5 
(* open Horn_backend_common 
5  6 
* open Horn_backend *) 
6  7 
open Zustre_data 
7 


8  
8  9 
let report = Log.report ~plugin:"z3 interface" 
9 


10  
10  11 
module HBC = Horn_backend_common 
12  
11  13 
let node_name = HBC.node_name 
12  14  
13  15 
let concat = HBC.concat 
14  16  
15  17 
let rename_machine = HBC.rename_machine 
18  
16  19 
let rename_machine_list = HBC.rename_machine_list 
17  20  
18  21 
let rename_next = HBC.rename_next 
22  
19  23 
let rename_mid = HBC.rename_mid 
24  
20  25 
let rename_current = HBC.rename_current 
21  26  
22  27 
let rename_current_list = HBC.rename_current_list 
28  
23  29 
let rename_mid_list = HBC.rename_mid_list 
30  
24  31 
let rename_next_list = HBC.rename_next_list 
25  32  
26  33 
let full_memory_vars = HBC.full_memory_vars 
34  
27  35 
let inout_vars = HBC.inout_vars 
36  
28  37 
let reset_vars = HBC.reset_vars 
38  
29  39 
let step_vars = HBC.step_vars 
40  
30  41 
let local_memory_vars = HBC.local_memory_vars 
42  
31  43 
let step_vars_m_x = HBC.step_vars_m_x 
44  
32  45 
let step_vars_c_m_x = HBC.step_vars_c_m_x 
33 


34 
let machine_reset_name = HBC.machine_reset_name 

35 
let machine_step_name = HBC.machine_step_name 

36 
let machine_stateless_name = HBC.machine_stateless_name 

46  
47 
let machine_reset_name = HBC.machine_reset_name 

48  
49 
let machine_step_name = HBC.machine_step_name 

50  
51 
let machine_stateless_name = HBC.machine_stateless_name 

37  52  
38  53 
let preprocess = Horn_backend.preprocess 
39 


40  54  
41  55 
exception UnknownFunction of (string * (Format.formatter > unit)) 
42  56 
(** Sorts 
43  57  
44 
A sort is introduced for each basic type and each enumerated type. 

58 
A sort is introduced for each basic type and each enumerated type.


45  59  
46 
A hashtbl records these and allow easy access to sort values, when


47 
provided with a enumerated type name.


60 
A hashtbl records these and allow easy access to sort values, when provided


61 
with a enumerated type name. *)


48  62  
49 
*) 

50 


51  63 
let bool_sort = Z3.Boolean.mk_sort !ctx 
64  
52  65 
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx 
66  
53  67 
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx 
54  68  
69 
let get_const_sort = Hashtbl.find const_sorts 

55  70  
56 
let get_const_sort = Hashtbl.find const_sorts 

57  71 
let get_sort_elems = Hashtbl.find sort_elems 
58 
let get_tag_sort id = try Hashtbl.find const_tags id with _ > Format.eprintf "Unable to find sort for tag=%s@." id; assert false 

59 


60  72  
61 


73 
let get_tag_sort id = 

74 
try Hashtbl.find const_tags id 

75 
with _ > 

76 
Format.eprintf "Unable to find sort for tag=%s@." id; 

77 
assert false 

78  
62  79 
let decl_sorts () = 
63 
Hashtbl.iter (fun typ decl > 

64 
match typ with 

65 
 Tydec_const var > 

66 
(match decl.top_decl_desc with 

67 
 TypeDef tdef > ( 

68 
match tdef.tydef_desc with 

69 
 Tydec_enum tl > 

70 
let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in 

71 
Hashtbl.add const_sorts var new_sort; 

72 
Hashtbl.add sort_elems new_sort tl; 

73 
List.iter (fun t > Hashtbl.add const_tags t new_sort) tl 

74 


75 
 _ > Format.eprintf "Unknown type : %a@.@?" Printers.pp_var_type_dec_desc typ; assert false 

76 
) 

77 
 _ > assert false 

78 
) 

79 
 _ > ()) Corelang.type_table 

80  
81 


82 
let rec type_to_sort t = 

83 
if Types.is_bool_type t then bool_sort else 

84 
if Types.is_int_type t then int_sort else 

85 
if Types.is_real_type t then real_sort else 

86 
match (Types.repr t).Types.tdesc with 

87 
 Types.Tconst ty > get_const_sort ty 

88 
 Types.Tclock t > type_to_sort t 

89 
 Types.Tarray(_, ty) > Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty) 

90 
 Types.Tstatic(_, ty) > type_to_sort ty 

91 
 Types.Tarrow _ 

92 
 _ > Format.eprintf "internal error: pp_type %a@." 

93 
Types.print_ty t; assert false 

80 
Hashtbl.iter 

81 
(fun typ decl > 

82 
match typ with 

83 
 Tydec_const var > ( 

84 
match decl.top_decl_desc with 

85 
 TypeDef tdef > ( 

86 
match tdef.tydef_desc with 

87 
 Tydec_enum tl > 

88 
let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in 

89 
Hashtbl.add const_sorts var new_sort; 

90 
Hashtbl.add sort_elems new_sort tl; 

91 
List.iter (fun t > Hashtbl.add const_tags t new_sort) tl 

92 
 _ > 

93 
Format.eprintf "Unknown type : %a@.@?" Printers.pp_var_type_dec_desc 

94 
typ; 

95 
assert false) 

96 
 _ > 

97 
assert false) 

98 
 _ > 

99 
()) 

100 
Corelang.type_table 

94  101  
102 
let rec type_to_sort t = 

103 
if Types.is_bool_type t then bool_sort 

104 
else if Types.is_int_type t then int_sort 

105 
else if Types.is_real_type t then real_sort 

106 
else 

107 
match (Types.repr t).Types.tdesc with 

108 
 Types.Tconst ty > 

109 
get_const_sort ty 

110 
 Types.Tclock t > 

111 
type_to_sort t 

112 
 Types.Tarray (_, ty) > 

113 
Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty) 

114 
 Types.Tstatic (_, ty) > 

115 
type_to_sort ty 

116 
 Types.Tarrow _  _ > 

117 
Format.eprintf "internal error: pp_type %a@." Types.print_ty t; 

118 
assert false 

95  119  
96  120 
(* let idx_var = *) 
97  121 
(* Z3.FuncDecl.mk_func_decl_s !ctx "__idx__" [] idx_sort *) 
98 


122  
99  123 
(* let uid_var = *) 
100  124 
(* Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort *) 
101  125  
...  ...  
103  127  
104  128 
Similarly fun_decls are registerd, by their name, into a hashtbl. The 
105  129 
proposed encoding introduces a 0ary fun_decl to model variables and 
106 
fun_decl with arguments to declare reset and step predicates. 

107  
108  
109  
110 
*) 

130 
fun_decl with arguments to declare reset and step predicates. *) 

111  131 
let register_fdecl id fd = Hashtbl.add decls id fd 
132  
112  133 
let get_fdecl id = 
113 
try 

114 
Hashtbl.find decls id 

115 
with Not_found > (report ~level:3 (fun fmt > Format.fprintf fmt "Unable to find func_decl %s@.@?" id); raise Not_found) 

134 
try Hashtbl.find decls id 

135 
with Not_found > 

136 
report ~level:3 (fun fmt > 

137 
Format.fprintf fmt "Unable to find func_decl %s@.@?" id); 

138 
raise Not_found 

116  139  
117  140 
let pp_fdecls fmt = 
118  141 
Format.fprintf fmt "Registered fdecls: @[%a@]@ " 
119 
(Utils.fprintf_list ~sep:"@ " Format.pp_print_string) (Hashtbl.fold (fun id _ accu > id::accu) decls []) 

142 
(Utils.fprintf_list ~sep:"@ " Format.pp_print_string) 

143 
(Hashtbl.fold (fun id _ accu > id :: accu) decls []) 

120  144  
121 


122  145 
let decl_var id = 
123  146 
(* Format.eprintf "Declaring var %s@." id.var_id; *) 
124 
let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) in 

147 
let fdecl = 

148 
Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) 

149 
in 

125  150 
register_fdecl id.var_id fdecl; 
126  151 
fdecl 
127  152  
128 
(* Declaring the function used in expr *)


153 
(* Declaring the function used in expr *) 

129  154 
let decl_fun op args typ = 
130  155 
let args = List.map type_to_sort args in 
131  156 
let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx op args (type_to_sort typ) in 
...  ...  
133  158 
fdecl 
134  159  
135  160 
let idx_sort = int_sort 
136 
let uid_sort = Z3.Z3List.mk_sort !ctx (Z3.Symbol.mk_string !ctx "uid_list") int_sort 

137 
let uid_conc = 

161  
162 
let uid_sort = 

163 
Z3.Z3List.mk_sort !ctx (Z3.Symbol.mk_string !ctx "uid_list") int_sort 

164  
165 
let uid_conc = 

138  166 
let fd = Z3.Z3List.get_cons_decl uid_sort in 
139 
fun head tail > Z3.FuncDecl.apply fd [head;tail]


167 
fun head tail > Z3.FuncDecl.apply fd [ head; tail ]


140  168  
141  169 
let get_instance_uid = 
142  170 
let hash : (string, int) Hashtbl.t = Hashtbl.create 13 in 
143  171 
let cpt = ref 0 in 
144  172 
fun i > 
145  173 
let id = 
146 
if Hashtbl.mem hash i then 

147 
Hashtbl.find hash i 

174 
if Hashtbl.mem hash i then Hashtbl.find hash i 

148  175 
else ( 
149 
incr cpt; 

150 
Hashtbl.add hash i !cpt; 

151 
!cpt 

152 
) 

176 
incr cpt; 

177 
Hashtbl.add hash i !cpt; 

178 
!cpt) 

153  179 
in 
154  180 
Z3.Arithmetic.Integer.mk_numeral_i !ctx id 
155 


156  181  
157 


158 
let decl_rel ?(no_additional_vars=false) name args_sorts = 

159 
(* Enriching arg_sorts with two new variables: a counting index and an 

160 
uid *) 

182 
let decl_rel ?(no_additional_vars = false) name args_sorts = 

183 
(* Enriching arg_sorts with two new variables: a counting index and an uid *) 

161  184 
let args_sorts = 
162 
if no_additional_vars then args_sorts else idx_sort::uid_sort::args_sorts in 

163 


185 
if no_additional_vars then args_sorts 

186 
else idx_sort :: uid_sort :: args_sorts 

187 
in 

188  
164  189 
(* let args_sorts = List.map (fun v > type_to_sort v.var_type) args in *) 
165  190 
if !debug then 
166 
Format.eprintf "Registering fdecl %s (%a)@." 

167 
name 

168 
(Utils.fprintf_list ~sep:"@ " 

169 
(fun fmt sort > Format.fprintf fmt "%s" (Z3.Sort.to_string sort))) 

170 
args_sorts 

171 
; 

191 
Format.eprintf "Registering fdecl %s (%a)@." name 

192 
(Utils.fprintf_list ~sep:"@ " (fun fmt sort > 

193 
Format.fprintf fmt "%s" (Z3.Sort.to_string sort))) 

194 
args_sorts; 

172  195 
let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in 
173  196 
Z3.Fixedpoint.register_relation !fp fdecl; 
174  197 
register_fdecl name fdecl; 
175  198 
fdecl 
176 


177  
178  199  
179  200 
(* Shared variables to describe counter and uid *) 
180  201  
181  202 
let idx = Corelang.dummy_var_decl "__idx__" Type_predef.type_int 
182 
let idx_var = Z3.Expr.mk_const_f !ctx (decl_var idx) 

183 
let uid = Corelang.dummy_var_decl "__uid__" Type_predef.type_int 

184 
let uid_fd = Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort 

185 
let _ = register_fdecl "__uid__" uid_fd 

186 
let uid_var = Z3.Expr.mk_const_f !ctx uid_fd 

187  203  
188 
(** Conversion functions


204 
let idx_var = Z3.Expr.mk_const_f !ctx (decl_var idx)


189  205  
190 
The following is similar to the Horn backend. Each printing function is 

191 
rephrased from pp_xx to xx_to_expr and produces a Z3 value. 

206 
let uid = Corelang.dummy_var_decl "__uid__" Type_predef.type_int 

192  207  
193 
*)


208 
let uid_fd = Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort


194  209  
210 
let _ = register_fdecl "__uid__" uid_fd 

195  211  
196 
(* Returns the f_decl associated to the variable v *) 

197 
let horn_var_to_expr v = 

198 
Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id) 

212 
let uid_var = Z3.Expr.mk_const_f !ctx uid_fd 

199  213  
214 
(** Conversion functions 

200  215  
216 
The following is similar to the Horn backend. Each printing function is 

217 
rephrased from pp_xx to xx_to_expr and produces a Z3 value. *) 

201  218  
219 
(* Returns the f_decl associated to the variable v *) 

220 
let horn_var_to_expr v = Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id) 

202  221  
203 
(* Used to print boolean constants *)


222 
(* Used to print boolean constants *) 

204  223 
let horn_tag_to_expr t = 
205 
if t = tag_true then 

206 
Z3.Boolean.mk_true !ctx 

207 
else if t = tag_false then 

208 
Z3.Boolean.mk_false !ctx 

224 
if t = tag_true then Z3.Boolean.mk_true !ctx 

225 
else if t = tag_false then Z3.Boolean.mk_false !ctx 

209  226 
else 
210  227 
(* Finding the associated sort *) 
211  228 
let sort = get_tag_sort t in 
212 
let elems = get_sort_elems sort in


229 
let elems = get_sort_elems sort in 

213  230 
let res : Z3.Expr.expr option = 
214 
List.fold_left2 (fun res cst expr > 

231 
List.fold_left2 

232 
(fun res cst expr > 

215  233 
match res with 
216 
 Some _ > res 

217 
 None > if t = cst then Some (expr:Z3.Expr.expr) else None 

218 
) None elems (Z3.Enumeration.get_consts sort) 

234 
 Some _ > 

235 
res 

236 
 None > 

237 
if t = cst then Some (expr : Z3.Expr.expr) else None) 

238 
None elems 

239 
(Z3.Enumeration.get_consts sort) 

219  240 
in 
220  241 
match res with None > assert false  Some s > s 
221 


242  
222  243 
(* Prints a constant value *) 
223  244 
let horn_const_to_expr c = 
224  245 
match c with 
225 
 Const_int i > Z3.Arithmetic.Integer.mk_numeral_i !ctx i 

226 
 Const_real r > Z3.Arithmetic.Real.mk_numeral_s !ctx (Real.to_string r) 

227 
 Const_tag t > horn_tag_to_expr t 

228 
 _ > assert false 

229  
230  
246 
 Const_int i > 

247 
Z3.Arithmetic.Integer.mk_numeral_i !ctx i 

248 
 Const_real r > 

249 
Z3.Arithmetic.Real.mk_numeral_s !ctx (Real.to_string r) 

250 
 Const_tag t > 

251 
horn_tag_to_expr t 

252 
 _ > 

253 
assert false 

231  254  
232  255 
(* Default value for each type, used when building arrays. Eg integer array 
233  256 
[2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value 
234 
for the type integer (arrays). 

235 
*) 

257 
for the type integer (arrays). *) 

236  258 
let horn_default_val t = 
237  259 
let t = Types.dynamic_type t in 
238 
if Types.is_bool_type t then Z3.Boolean.mk_true !ctx else 

239 
if Types.is_int_type t then Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 else 

240 
if Types.is_real_type t then Z3.Arithmetic.Real.mk_numeral_i !ctx 0 else 

241 
(* match (Types.dynamic_type t).Types.tdesc with 

242 
*  Types.Tarray(dim, l) > (\* TODO PL: this strange code has to be (heavily) checked *\) 

243 
* let valt = Types.array_element_type t in 

244 
* fprintf fmt "((as const (Array Int %a)) %a)" 

245 
* pp_type valt 

246 
* pp_default_val valt 

247 
*  Types.Tstruct(l) > assert false 

248 
*  Types.Ttuple(l) > assert false 

249 
* _ > *) assert false 

260 
if Types.is_bool_type t then Z3.Boolean.mk_true !ctx 

261 
else if Types.is_int_type t then Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 

262 
else if Types.is_real_type t then Z3.Arithmetic.Real.mk_numeral_i !ctx 0 

263 
else 

264 
(* match (Types.dynamic_type t).Types.tdesc with 

265 
*  Types.Tarray(dim, l) > (\* TODO PL: this strange code has to be (heavily) checked *\) 

266 
* let valt = Types.array_element_type t in 

267 
* fprintf fmt "((as const (Array Int %a)) %a)" 

268 
* pp_type valt 

269 
* pp_default_val valt 

270 
*  Types.Tstruct(l) > assert false 

271 
*  Types.Ttuple(l) > assert false 

272 
* _ > *) 

273 
assert false 

250  274  
251  275 
(* Conversion of basic library functions *) 
252 


276  
253  277 
let horn_basic_app i vl (vltyp, typ) = 
254  278 
match i, vl with 
255 
 "ite", [v1; v2; v3] > Z3.Boolean.mk_ite !ctx v1 v2 v3 

256 
 "uminus", [v] > Z3.Arithmetic.mk_unary_minus 

257 
!ctx v 

258 
 "not", [v] > 

259 
Z3.Boolean.mk_not 

260 
!ctx v 

261 
 "=", [v1; v2] > 

262 
Z3.Boolean.mk_eq 

263 
!ctx v1 v2 

264 
 "&&", [v1; v2] > 

265 
Z3.Boolean.mk_and 

266 
!ctx 

267 
[v1; v2] 

268 
 "", [v1; v2] > 

269 
Z3.Boolean.mk_or 

270 
!ctx 

271 
[v1; 

272 
v2] 

273  
274 
 "impl", [v1; v2] > 

275 
Z3.Boolean.mk_implies 

276 
!ctx v1 v2 

277 
 "mod", [v1; v2] > 

278 
Z3.Arithmetic.Integer.mk_mod 

279 
!ctx v1 v2 

280 
 "equi", [v1; v2] > 

281 
Z3.Boolean.mk_eq 

282 
!ctx 

283 
v1 v2 

284 
 "xor", [v1; v2] > 

285 
Z3.Boolean.mk_xor 

286 
!ctx v1 v2 

287 
 "!=", [v1; v2] > 

288 
Z3.Boolean.mk_not 

289 
!ctx 

290 
( 

291 
Z3.Boolean.mk_eq 

292 
!ctx v1 v2 

293 
) 

294 
 "/", [v1; v2] > 

295 
Z3.Arithmetic.mk_div 

296 
!ctx v1 v2 

297  
298 
 "+", [v1; v2] > 

299 
Z3.Arithmetic.mk_add 

300 
!ctx 

301 
[v1; v2] 

302 
 "", [v1; v2] > 

303 
Z3.Arithmetic.mk_sub 

304 
!ctx 

305 
[v1 ; v2] 

306 


307 
 "*", [v1; v2] > 

308 
Z3.Arithmetic.mk_mul 

309 
!ctx 

310 
[ v1; v2] 

311  
312  
313 
 "<", [v1; v2] > 

314 
Z3.Arithmetic.mk_lt 

315 
!ctx v1 v2 

316 
 "<=", [v1; v2] > 

317 
Z3.Arithmetic.mk_le 

318 
!ctx v1 v2 

319 
 ">", [v1; v2] > 

320 
Z3.Arithmetic.mk_gt 

321 
!ctx v1 v2 

322 
 ">=", [v1; v2] > 

323 
Z3.Arithmetic.mk_ge 

324 
!ctx v1 v2 

325 
 "int_to_real", [v1] > 

326 
Z3.Arithmetic.Integer.mk_int2real 

327 
!ctx v1 

279 
 "ite", [ v1; v2; v3 ] > 

280 
Z3.Boolean.mk_ite !ctx v1 v2 v3 

281 
 "uminus", [ v ] > 

282 
Z3.Arithmetic.mk_unary_minus !ctx v 

283 
 "not", [ v ] > 

284 
Z3.Boolean.mk_not !ctx v 

285 
 "=", [ v1; v2 ] > 

286 
Z3.Boolean.mk_eq !ctx v1 v2 

287 
 "&&", [ v1; v2 ] > 

288 
Z3.Boolean.mk_and !ctx [ v1; v2 ] 

289 
 "", [ v1; v2 ] > 

290 
Z3.Boolean.mk_or !ctx [ v1; v2 ] 

291 
 "impl", [ v1; v2 ] > 

292 
Z3.Boolean.mk_implies !ctx v1 v2 

293 
 "mod", [ v1; v2 ] > 

294 
Z3.Arithmetic.Integer.mk_mod !ctx v1 v2 

295 
 "equi", [ v1; v2 ] > 

296 
Z3.Boolean.mk_eq !ctx v1 v2 

297 
 "xor", [ v1; v2 ] > 

298 
Z3.Boolean.mk_xor !ctx v1 v2 

299 
 "!=", [ v1; v2 ] > 

300 
Z3.Boolean.mk_not !ctx (Z3.Boolean.mk_eq !ctx v1 v2) 

301 
 "/", [ v1; v2 ] > 

302 
Z3.Arithmetic.mk_div !ctx v1 v2 

303 
 "+", [ v1; v2 ] > 

304 
Z3.Arithmetic.mk_add !ctx [ v1; v2 ] 

305 
 "", [ v1; v2 ] > 

306 
Z3.Arithmetic.mk_sub !ctx [ v1; v2 ] 

307 
 "*", [ v1; v2 ] > 

308 
Z3.Arithmetic.mk_mul !ctx [ v1; v2 ] 

309 
 "<", [ v1; v2 ] > 

310 
Z3.Arithmetic.mk_lt !ctx v1 v2 

311 
 "<=", [ v1; v2 ] > 

312 
Z3.Arithmetic.mk_le !ctx v1 v2 

313 
 ">", [ v1; v2 ] > 

314 
Z3.Arithmetic.mk_gt !ctx v1 v2 

315 
 ">=", [ v1; v2 ] > 

316 
Z3.Arithmetic.mk_ge !ctx v1 v2 

317 
 "int_to_real", [ v1 ] > 

318 
Z3.Arithmetic.Integer.mk_int2real !ctx v1 

328  319 
 _ > 
329 
let fd = 

330 
try 

331 
get_fdecl i 

332 
with Not_found > begin 

333 
report ~level:3 (fun fmt > Format.fprintf fmt "Registering function %s as uninterpreted function in Z3@.%s: (%a) > %a" i i (Utils.fprintf_list ~sep:"," Types.print_ty) vltyp Types.print_ty typ); 

334 
decl_fun i vltyp typ 

335 
end 

336 
in 

337 
Z3.FuncDecl.apply fd vl 

338 


339 


340 
(*  _, [v1; v2] > Z3.Boolean.mk_and 

341 
* !ctx 

342 
* (val_to_expr v1) 

343 
* (val_to_expr v2) 

344 
* 

345 
* Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *) 

320 
let fd = 

321 
try get_fdecl i 

322 
with Not_found > 

323 
report ~level:3 (fun fmt > 

324 
Format.fprintf fmt 

325 
"Registering function %s as uninterpreted function in Z3@.%s: \ 

326 
(%a) > %a" 

327 
i i 

328 
(Utils.fprintf_list ~sep:"," Types.print_ty) 

329 
vltyp Types.print_ty typ); 

330 
decl_fun i vltyp typ 

331 
in 

332 
Z3.FuncDecl.apply fd vl 

333  
334 
(*  _, [v1; v2] > Z3.Boolean.mk_and 

335 
* !ctx 

336 
* (val_to_expr v1) 

337 
* (val_to_expr v2) 

338 
* 

339 
* Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *) 

346  340  
347  341 
(*  _ > ( 
348  342 
* let msg fmt = Format.fprintf fmt 
...  ...  
352  346 
* raise (UnknownFunction(i, msg)) 
353  347 
* ) *) 
354  348  
355 


356 
(* Convert a value expression [v], with internal function calls only. [pp_var] 

349 
(* Convert a value expression [v], with internal function calls only. [pp_var] 

357  350 
is a printer for variables (typically [pp_c_var_read]), but an offset suffix 
358 
may be added for array variables 

359 
*) 

360 
let rec horn_val_to_expr ?(is_lhs=false) m self v = 

351 
may be added for array variables *) 

352 
let rec horn_val_to_expr ?(is_lhs = false) m self v = 

361  353 
(* Format.eprintf "h_v2e %a@." (Machine_code_common.pp_val m) v ; *) 
362  354 
match v.value_desc with 
363 
 Cst c > horn_const_to_expr c


364  
355 
 Cst c >


356 
horn_const_to_expr c 

365  357 
(* Code specific for arrays *) 
366 
 Array il > 

367 
(* An array definition: 

368 
(store ( 

369 
... 

370 
(store ( 

371 
store ( 

372 
default_val 

373 
) 

374 
idx_n val_n 

375 
) 

376 
idx_n1 val_n1) 

377 
... 

378 
idx_1 val_1 

379 
) *) 

380 
let rec build_array (tab, x) = 

381 
match tab with 

382 
 [] > horn_default_val v.value_type(* (get_type v) *) 

383 
 h::t > 

384 
Z3.Z3Array.mk_store 

385 
!ctx 

386 
(build_array (t, (x+1))) 

387 
(Z3.Arithmetic.Integer.mk_numeral_i !ctx x) 

388 
(horn_val_to_expr ~is_lhs:is_lhs m self h) 

389 
in 

390 
build_array (il, 0) 

391 


392 
 Access(tab,index) > 

393 
Z3.Z3Array.mk_select !ctx 

394 
(horn_val_to_expr ~is_lhs:is_lhs m self tab) 

395 
(horn_val_to_expr ~is_lhs:is_lhs m self index) 

396  
358 
 Array il > 

359 
(* An array definition: (store ( ... (store ( store ( default_val ) idx_n 

360 
val_n ) idx_n1 val_n1) ... idx_1 val_1 ) *) 

361 
let rec build_array (tab, x) = 

362 
match tab with 

363 
 [] > 

364 
horn_default_val v.value_type (* (get_type v) *) 

365 
 h :: t > 

366 
Z3.Z3Array.mk_store !ctx 

367 
(build_array (t, x + 1)) 

368 
(Z3.Arithmetic.Integer.mk_numeral_i !ctx x) 

369 
(horn_val_to_expr ~is_lhs m self h) 

370 
in 

371 
build_array (il, 0) 

372 
 Access (tab, index) > 

373 
Z3.Z3Array.mk_select !ctx 

374 
(horn_val_to_expr ~is_lhs m self tab) 

375 
(horn_val_to_expr ~is_lhs m self index) 

397  376 
(* Code specific for arrays *) 
398 


399 
 Power _ > assert false


400 
 Var v >


401 
if is_memory m v then


402 
if Types.is_array_type v.var_type


403 
then assert false


404 
else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))


405 


406 
else


407 
horn_var_to_expr


408 
(rename_machine


409 
self


410 
v)


411 
 Fun (n, vl) > horn_basic_app n (List.map (horn_val_to_expr m self) vl) (List.map (fun v > v.value_type) vl, v.value_type)


377 
 Power _ > 

378 
assert false


379 
 Var v > 

380 
if is_memory m v then 

381 
if Types.is_array_type v.var_type then assert false


382 
else


383 
horn_var_to_expr


384 
(rename_machine self 

385 
((if is_lhs then rename_next else rename_current (* self *)) v))


386 
else horn_var_to_expr (rename_machine self v)


387 
 Fun (n, vl) >


388 
horn_basic_app n


389 
(List.map (horn_val_to_expr m self) vl)


390 
(List.map (fun v > v.value_type) vl, v.value_type)


412  391  
413  392 
let no_reset_to_exprs machines m i = 
414 
let (n,_) = List.assoc i m.minstances in 

415 
let target_machine = List.find (fun m > m.mname.node_id = (Corelang.node_name n)) machines in 

393 
let n, _ = List.assoc i m.minstances in 

394 
let target_machine = 

395 
List.find (fun m > m.mname.node_id = Corelang.node_name n) machines 

396 
in 

416  397  
417 
let m_list = 

418 
rename_machine_list 

419 
(concat m.mname.node_id i) 

398 
let m_list = 

399 
rename_machine_list (concat m.mname.node_id i) 

420  400 
(rename_mid_list (full_memory_vars machines target_machine)) 
421  401 
in 
422  402 
let c_list = 
423 
rename_machine_list 

424 
(concat m.mname.node_id i) 

403 
rename_machine_list (concat m.mname.node_id i) 

425  404 
(rename_current_list (full_memory_vars machines target_machine)) 
426  405 
in 
427  406 
match c_list, m_list with 
428 
 [chd], [mhd] > 

429 
let expr = 

430 
Z3.Boolean.mk_eq !ctx 

431 
(horn_var_to_expr mhd) 

432 
(horn_var_to_expr chd) 

433 
in 

434 
[expr] 

435 
 _ > ( 

407 
 [ chd ], [ mhd ] > 

408 
let expr = 

409 
Z3.Boolean.mk_eq !ctx (horn_var_to_expr mhd) (horn_var_to_expr chd) 

410 
in 

411 
[ expr ] 

412 
 _ > 

436  413 
let exprs = 
437 
List.map2 (fun mhd chd > 

438 
Z3.Boolean.mk_eq !ctx 

439 
(horn_var_to_expr mhd) 

440 
(horn_var_to_expr chd) 

441 
) 

442 
m_list 

443 
c_list 

414 
List.map2 

415 
(fun mhd chd > 

416 
Z3.Boolean.mk_eq !ctx (horn_var_to_expr mhd) (horn_var_to_expr chd)) 

417 
m_list c_list 

444  418 
in 
445  419 
exprs 
446 
) 

447  420  
448  421 
let instance_reset_to_exprs machines m i = 
449 
let (n,_) = List.assoc i m.minstances in 

450 
let target_machine = List.find (fun m > m.mname.node_id = (Corelang.node_name n)) machines in 

422 
let n, _ = List.assoc i m.minstances in 

423 
let target_machine = 

424 
List.find (fun m > m.mname.node_id = Corelang.node_name n) machines 

425 
in 

451  426 
let vars = 
452 
(rename_machine_list 

453 
(concat m.mname.node_id i) 

454 
(rename_current_list (full_memory_vars machines target_machine))@ (rename_mid_list (full_memory_vars machines target_machine)) 

455 
) 

456 


427 
rename_machine_list (concat m.mname.node_id i) 

428 
(rename_current_list (full_memory_vars machines target_machine)) 

429 
@ rename_mid_list (full_memory_vars machines target_machine) 

457  430 
in 
431  
458  432 
let expr = 
459 
Z3.Expr.mk_app 

460 
!ctx 

433 
Z3.Expr.mk_app !ctx 

461  434 
(get_fdecl (machine_reset_name (Corelang.node_name n))) 
462 
(List.map (horn_var_to_expr) (idx::uid::vars))


435 
(List.map horn_var_to_expr (idx :: uid :: vars))


463  436 
in 
464 
[expr]


437 
[ expr ]


465  438  
466  439 
let instance_call_to_exprs machines reset_instances m i inputs outputs = 
467  440 
let self = m.mname.node_id in 
...  ...  
471  444 
(* Additional input to register step counters, and uid *) 
472  445 
let idx = horn_var_to_expr idx in 
473  446 
let uid = uid_conc (get_instance_uid i) (horn_var_to_expr uid) in 
474 
let inout =


447 
let inout = 

475  448 
List.map (horn_val_to_expr m self) 
476 
(inputs @ (List.map (fun v > mk_val (Var v) v.var_type) outputs))


449 
(inputs @ List.map (fun v > mk_val (Var v) v.var_type) outputs)


477  450 
in 
478 
idx::uid::inout


451 
idx :: uid :: inout


479  452 
in 
480 


481 
try (* stateful node instance *) 

482 
begin 

483 
let (n,_) = List.assoc i m.minstances in 

484 
let target_machine = List.find (fun m > m.mname.node_id = Corelang.node_name n) machines in 

485  
486 
(* Checking whether this specific instances has been reset yet *) 

487 
let reset_exprs = 

488 
if not (List.mem i reset_instances) then 

489 
(* If not, declare mem_m = mem_c *) 

490 
no_reset_to_exprs machines m i 

491 
else 

492 
[] (* Nothing to add yet *) 

493 
in 

494 


495 
let mems = full_memory_vars machines target_machine in 

496 
let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in 

497 
let mid_mems = rename_mems rename_mid_list in 

498 
let next_mems = rename_mems rename_next_list in 

499  
500 
let call_expr = 

501 
match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with 

502 
 "_arrow", [i1; i2], [o], [mem_m], [mem_x] > begin 

503 
let stmt1 = (* out = ite mem_m then i1 else i2 *) 

504 
Z3.Boolean.mk_eq !ctx 

505 
( (* output var *) 

506 
horn_val_to_expr 

507 
~is_lhs:true 

508 
m self 

509 
(mk_val (Var o) o.var_type) 

510 
) 

511 
( 

512 
Z3.Boolean.mk_ite !ctx 

513 
(horn_var_to_expr mem_m) 

514 
(horn_val_to_expr m self i1) 

515 
(horn_val_to_expr m self i2) 

516 
) 

517 
in 

518 
let stmt2 = (* mem_X = false *) 

519 
Z3.Boolean.mk_eq !ctx 

520 
(horn_var_to_expr mem_x) 

521 
(Z3.Boolean.mk_false !ctx) 

522 
in 

523 
[stmt1; stmt2] 

524 
end 

525  
526 
 _ > 

527 
let expr = 

528 
Z3.Expr.mk_app 

529 
!ctx 

530 
(get_fdecl (machine_step_name (node_name n))) 

531 
( (* Arguments are input, output, mid_mems, next_mems *) 

532 
idx_uid_inout @ List.map (horn_var_to_expr) (mid_mems@next_mems) 

533 


534 
) 

535 
in 

536 
[expr] 

537 
in 

538  453  
539 
reset_exprs@call_expr 

540 
end 

541 
with Not_found > ( (* stateless node instance *) 

542 
let (n,_) = List.assoc i m.mcalls in 

543 
let expr = 

544 
Z3.Expr.mk_app 

545 
!ctx 

546 
(get_fdecl (machine_stateless_name (node_name n))) 

547 
idx_uid_inout (* Arguments are inputs, outputs *) 

454 
try 

455 
(* stateful node instance *) 

456 
let n, _ = List.assoc i m.minstances in 

457 
let target_machine = 

458 
List.find (fun m > m.mname.node_id = Corelang.node_name n) machines 

548  459 
in 
549 
[expr] 

550 
) 

551  460  
461 
(* Checking whether this specific instances has been reset yet *) 

462 
let reset_exprs = 

463 
if not (List.mem i reset_instances) then 

464 
(* If not, declare mem_m = mem_c *) 

465 
no_reset_to_exprs machines m i 

466 
else [] 

467 
(* Nothing to add yet *) 

468 
in 

469  
470 
let mems = full_memory_vars machines target_machine in 

471 
let rename_mems f = 

472 
rename_machine_list (concat m.mname.node_id i) (f mems) 

473 
in 

474 
let mid_mems = rename_mems rename_mid_list in 

475 
let next_mems = rename_mems rename_next_list in 

476  
477 
let call_expr = 

478 
match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with 

479 
 "_arrow", [ i1; i2 ], [ o ], [ mem_m ], [ mem_x ] > 

480 
let stmt1 = 

481 
(* out = ite mem_m then i1 else i2 *) 

482 
Z3.Boolean.mk_eq !ctx 

483 
((* output var *) 

484 
horn_val_to_expr ~is_lhs:true m self 

485 
(mk_val (Var o) o.var_type)) 

486 
(Z3.Boolean.mk_ite !ctx (horn_var_to_expr mem_m) 

487 
(horn_val_to_expr m self i1) 

488 
(horn_val_to_expr m self i2)) 

489 
in 

490 
let stmt2 = 

491 
(* mem_X = false *) 

492 
Z3.Boolean.mk_eq !ctx (horn_var_to_expr mem_x) 

493 
(Z3.Boolean.mk_false !ctx) 

494 
in 

495 
[ stmt1; stmt2 ] 

496 
 _ > 

497 
let expr = 

498 
Z3.Expr.mk_app !ctx 

499 
(get_fdecl (machine_step_name (node_name n))) 

500 
((* Arguments are input, output, mid_mems, next_mems *) 

501 
idx_uid_inout 

502 
@ List.map horn_var_to_expr (mid_mems @ next_mems)) 

503 
in 

504 
[ expr ] 

505 
in 

506  
507 
reset_exprs @ call_expr 

508 
with Not_found > 

509 
(* stateless node instance *) 

510 
let n, _ = List.assoc i m.mcalls in 

511 
let expr = 

512 
Z3.Expr.mk_app !ctx 

513 
(get_fdecl (machine_stateless_name (node_name n))) 

514 
idx_uid_inout 

515 
(* Arguments are inputs, outputs *) 

516 
in 

517 
[ expr ] 

552  518  
553 


554  519 
(* (\* Prints a [value] indexed by the suffix list [loop_vars] *\) *) 
555  520 
(* let rec value_suffix_to_expr self value = *) 
556  521 
(* match value.value_desc with *) 
557  522 
(*  Fun (n, vl) > *) 
558  523 
(* horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *) 
559 


524  
560  525 
(*  _ > *) 
561  526 
(* horn_val_to_expr self value *) 
562  527  
563  
564 
(* type_directed assignment: array vs. statically sized type 

565 
 [var_type]: type of variable to be assigned 

566 
 [var_name]: name of variable to be assigned 

567 
 [value]: assigned value 

568 
 [pp_var]: printer for variables 

569 
*) 

528 
(* type_directed assignment: array vs. statically sized type  [var_type]: type 

529 
of variable to be assigned  [var_name]: name of variable to be assigned  

530 
[value]: assigned value  [pp_var]: printer for variables *) 

570  531 
let assign_to_exprs m var_name value = 
571  532 
let self = m.mname.node_id in 
572  533 
let e = 
573 
Z3.Boolean.mk_eq 

574 
!ctx 

534 
Z3.Boolean.mk_eq !ctx 

575  535 
(horn_val_to_expr ~is_lhs:true m self var_name) 
576  536 
(horn_val_to_expr m self value) 
577 
(* was: TODO deal with array accesses (value_suffix_to_expr self value) *)


537 
(* was: TODO deal with array accesses (value_suffix_to_expr self value) *)


578  538 
in 
579 
[e]


539 
[ e ]


580  540  
581 


582  541 
(* Convert instruction to Z3.Expr and update the set of reset instances *) 
583 
let rec instr_to_exprs machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list = 

542 
let rec instr_to_exprs machines reset_instances (m : machine_t) instr : 

543 
Z3.Expr.expr list * ident list = 

584  544 
match Corelang.get_instr_desc instr with 
585 
 MComment _ > [], reset_instances 

586 
 MNoReset i > (* we assign middle_mem with mem_m. And declare i as reset *) 

587 
no_reset_to_exprs machines m i, 

588 
i::reset_instances 

589 
 MReset i > (* we assign middle_mem with reset: reset(mem_m) *) 

590 
instance_reset_to_exprs machines m i, 

591 
i::reset_instances 

592 
 MLocalAssign (i,v) > 

593 
assign_to_exprs 

594 
m 

595 
(mk_val (Var i) i.var_type) v, 

596 
reset_instances 

597 
 MStateAssign (i,v) > 

598 
assign_to_exprs 

599 
m 

600 
(mk_val (Var i) i.var_type) v, 

601 
reset_instances 

602 
 MStep ([_], i, vl) when Basic_library.is_internal_fun i (List.map (fun v > v.value_type) vl) > 

545 
 MComment _ > 

546 
[], reset_instances 

547 
 MNoReset i > 

548 
(* we assign middle_mem with mem_m. And declare i as reset *) 

549 
no_reset_to_exprs machines m i, i :: reset_instances 

550 
 MReset i > 

551 
(* we assign middle_mem with reset: reset(mem_m) *) 

552 
instance_reset_to_exprs machines m i, i :: reset_instances 

553 
 MLocalAssign (i, v) > 

554 
assign_to_exprs m (mk_val (Var i) i.var_type) v, reset_instances 

555 
 MStateAssign (i, v) > 

556 
assign_to_exprs m (mk_val (Var i) i.var_type) v, reset_instances 

557 
 MStep ([ _ ], i, vl) 

558 
when Basic_library.is_internal_fun i (List.map (fun v > v.value_type) vl) 

559 
> 

603  560 
assert false (* This should not happen anymore *) 
604  561 
 MStep (il, i, vl) > 
605 
(* if reset instance, just print the call over mem_m , otherwise declare mem_m = 

606 
mem_c and print the call to mem_m *) 

607 
instance_call_to_exprs machines reset_instances m i vl il, 

608 
reset_instances (* Since this instance call will only happen once, we 

609 
don't have to update reset_instances *) 

610  
611 
 MBranch (g,hl) > (* (g = tag1 => expr1) and (g = tag2 => expr2) ... 

612 
should not be produced yet. Later, we will have to 

613 
compare the reset_instances of each branch and 

614 
introduced the mem_m = mem_c for branches to do not 

615 
address it while other did. Am I clear ? *) 

562 
(* if reset instance, just print the call over mem_m , otherwise declare 

563 
mem_m = mem_c and print the call to mem_m *) 

564 
instance_call_to_exprs machines reset_instances m i vl il, reset_instances 

565 
(* Since this instance call will only happen once, we don't have to update 

566 
reset_instances *) 

567 
 MBranch (g, hl) > 

568 
(* (g = tag1 => expr1) and (g = tag2 => expr2) ... should not be produced 

569 
yet. Later, we will have to compare the reset_instances of each branch 

570 
and introduced the mem_m = mem_c for branches to do not address it while 

571 
other did. Am I clear ? *) 

616  572 
(* For each branch we obtain the logical encoding, and the information 
617  573 
whether a sub node has been reset or not. If a node has been reset in one 
618 
of the branch, then all others have to have the mem_m = mem_c 

619 
statement. *) 

574 
of the branch, then all others have to have the mem_m = mem_c statement. *) 

620  575 
let self = m.mname.node_id in 
621  576 
let branch_to_expr (tag, instrs) = 
622 
let branch_def, branch_resets = instrs_to_expr machines reset_instances m instrs in 

577 
let branch_def, branch_resets = 

578 
instrs_to_expr machines reset_instances m instrs 

579 
in 

623  580 
let e = 
624 
Z3.Boolean.mk_implies !ctx


625 
(Z3.Boolean.mk_eq !ctx


581 
Z3.Boolean.mk_implies !ctx


582 
(Z3.Boolean.mk_eq !ctx 

626  583 
(horn_val_to_expr m self g) 
627 
(horn_tag_to_expr tag)) 

628 
branch_def in 

584 
(horn_tag_to_expr tag)) 

585 
branch_def 

586 
in 

629  587  
630 
[e], branch_resets 

631 


588 
[ e ], branch_resets 

632  589 
in 
633 
List.fold_left (fun (instrs, resets) b > 

634 
let b_instrs, b_resets = branch_to_expr b in 

635 
instrs@b_instrs, resets@b_resets 

636 
) ([], reset_instances) hl 

637 
 MSpec _ > assert false 

638  590  
639 
and instrs_to_expr machines reset_instances m instrs = 

591 
List.fold_left 

592 
(fun (instrs, resets) b > 

593 
let b_instrs, b_resets = branch_to_expr b in 

594 
instrs @ b_instrs, resets @ b_resets) 

595 
([], reset_instances) hl 

596 
 MSpec _ > 

597 
assert false 

598  
599 
and instrs_to_expr machines reset_instances m instrs = 

640  600 
let instr_to_exprs rs i = instr_to_exprs machines rs m i in 
641 
let e_list, rs =


601 
let e_list, rs = 

642  602 
match instrs with 
643 
 [x] > instr_to_exprs reset_instances x 

644 
 _::_ > (* TODO: check whether we should compuyte a AND on the exprs (expr list) built here. It was performed in the printer setting but seems to be useless here since the output is a list of exprs *) 

645 


646 
List.fold_left (fun (exprs, rs) i > 

647 
let exprs_i, rs_i = instr_to_exprs rs i in 

648 
exprs@exprs_i, rs@rs_i 

649 
) 

650 
([], reset_instances) instrs 

651 


652 


653 
 [] > [], reset_instances 

603 
 [ x ] > 

604 
instr_to_exprs reset_instances x 

605 
 _ :: _ > 

606 
(* TODO: check whether we should compuyte a AND on the exprs (expr list) 

607 
built here. It was performed in the printer setting but seems to be 

608 
useless here since the output is a list of exprs *) 

609 
List.fold_left 

610 
(fun (exprs, rs) i > 

611 
let exprs_i, rs_i = instr_to_exprs rs i in 

612 
exprs @ exprs_i, rs @ rs_i) 

613 
([], reset_instances) instrs 

614 
 [] > 

615 
[], reset_instances 

654  616 
in 
655 
let e =


617 
let e = 

656  618 
match e_list with 
657 
 [e] > e 

658 
 [] > Z3.Boolean.mk_true !ctx 

659 
 _ > Z3.Boolean.mk_and !ctx e_list 

619 
 [ e ] > 

620 
e 

621 
 [] > 

622 
Z3.Boolean.mk_true !ctx 

623 
 _ > 

624 
Z3.Boolean.mk_and !ctx e_list 

660  625 
in 
661  626 
e, rs 
662  627  
663  
664  628 
(*********************************************************) 
665  629  
666  630 
(* Quantifiying universally all occuring variables *) 
667 
let add_rule ?(dont_touch=[]) vars expr =


631 
let add_rule ?(dont_touch = []) vars expr =


668  632 
(* let fds = Z3.Expr.get_args expr in *) 
669  633 
(* Format.eprintf "Expr %s: args: [%a]@." *) 
670  634 
(* (Z3.Expr.to_string expr) *) 
671 
(* (Utils.fprintf_list ~sep:", " (fun fmt e > Format.pp_print_string fmt (Z3.Expr.to_string e))) fds; *) 

635 
(* (Utils.fprintf_list ~sep:", " (fun fmt e > Format.pp_print_string fmt 

636 
(Z3.Expr.to_string e))) fds; *) 

672  637  
673  638 
(* (\* Old code relying on provided vars *\) *) 
674  639 
(* let sorts = (List.map (fun id > type_to_sort id.var_type) vars) in *) 
675 
(* let symbols = (List.map (fun id > Z3.FuncDecl.get_name (get_fdecl id.var_id)) vars) in *) 

676 


640 
(* let symbols = (List.map (fun id > Z3.FuncDecl.get_name (get_fdecl 

641 
id.var_id)) vars) in *) 

642  
677  643 
(* New code: we extract vars from expr *) 
678  644 
let module FDSet = Set.Make (struct 
679 
type t = Z3.FuncDecl.func_decl 

680 
let compare = compare 

681 
(* let hash = Hashtbl.hash *) 

682 
end) 

683 
in 

684 
(* Fonction seems unused 

685  
686 
let rec get_expr_vars e = 

687 
let open Utils in 

688 
let nb_args = Z3.Expr.get_num_args e in 

689 
if nb_args <= 0 then ( 

690 
let fdecl = Z3.Expr.get_func_decl e in 

691 
(* let params = Z3.FuncDecl.get_parameters fdecl in *) 

692 
(* Format.eprintf "Extracting info about %s: @." (Z3.Expr.to_string e); *) 

693 
let dkind = Z3.FuncDecl.get_decl_kind fdecl in 

694 
match dkind with Z3enums.OP_UNINTERPRETED > ( 

695 
(* Format.eprintf "kind = %s, " (match dkind with Z3enums.OP_TRUE > "true"  Z3enums.OP_UNINTERPRETED > "uninter"); *) 

696 
(* let open Z3.FuncDecl.Parameter in *) 

697 
(* List.iter (fun p > *) 

698 
(* match p with *) 

699 
(* P_Int i > Format.eprintf "int %i" i *) 

700 
(*  P_Dbl f > Format.eprintf "dbl %f" f *) 

701 
(*  P_Sym s > Format.eprintf "symb" *) 

702 
(*  P_Srt s > Format.eprintf "sort" *) 

703 
(*  P_Ast _ >Format.eprintf "ast" *) 

704 
(*  P_Fdl f > Format.eprintf "fundecl" *) 

705 
(*  P_Rat s > Format.eprintf "rat %s" s *) 

706 


707 
(* ) params; *) 

708 
(* Format.eprintf "]@."; *) 

709 
FDSet.singleton fdecl 

710 
) 

711 
 _ > FDSet.empty 

712 
) 

713 
else (*if nb_args > 0 then*) 

714 
List.fold_left 

715 
(fun accu e > FDSet.union accu (get_expr_vars e)) 

716 
FDSet.empty (Z3.Expr.get_args e) 

717 
in 

718 
*) 

719 
(* Unsed variable. Coul;d be reintroduced 

720 
let extracted_vars = FDSet.elements (FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in 

721 
let extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in 

722 
let extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in 

723 
*) 

724 
if !debug then ( 

645 
type t = Z3.FuncDecl.func_decl 

646  
647 
let compare = compare 

648 
(* let hash = Hashtbl.hash *) 

649 
end) in 

650 
(* Fonction seems unused 

651  
652 
let rec get_expr_vars e = let open Utils in let nb_args = 

653 
Z3.Expr.get_num_args e in if nb_args <= 0 then ( let fdecl = 

654 
Z3.Expr.get_func_decl e in (* let params = Z3.FuncDecl.get_parameters fdecl 

655 
in *) (* Format.eprintf "Extracting info about %s: @." (Z3.Expr.to_string 

656 
e); *) let dkind = Z3.FuncDecl.get_decl_kind fdecl in match dkind with 

657 
Z3enums.OP_UNINTERPRETED > ( (* Format.eprintf "kind = %s, " (match dkind 

658 
with Z3enums.OP_TRUE > "true"  Z3enums.OP_UNINTERPRETED > "uninter"); *) 

659 
(* let open Z3.FuncDecl.Parameter in *) (* List.iter (fun p > *) (* match 

660 
p with *) (* P_Int i > Format.eprintf "int %i" i *) (*  P_Dbl f > 

661 
Format.eprintf "dbl %f" f *) (*  P_Sym s > Format.eprintf "symb" *) (*  

662 
P_Srt s > Format.eprintf "sort" *) (*  P_Ast _ >Format.eprintf "ast" *) 

663 
(*  P_Fdl f > Format.eprintf "fundecl" *) (*  P_Rat s > Format.eprintf 

664 
"rat %s" s *) 

665  
666 
(* ) params; *) (* Format.eprintf "]@."; *) FDSet.singleton fdecl )  _ > 

667 
FDSet.empty ) else (*if nb_args > 0 then*) List.fold_left (fun accu e > 

668 
FDSet.union accu (get_expr_vars e)) FDSet.empty (Z3.Expr.get_args e) in *) 

669 
(* Unsed variable. Coul;d be reintroduced let extracted_vars = FDSet.elements 

670 
(FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in let 

671 
extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in let 

672 
extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in *) 

673 
if !debug then 

725  674 
Format.eprintf "Declaring rule: %s with variables @[<v 0>@ [%a@ ]@]@ @." 
726  675 
(Z3.Expr.to_string expr) 
727 
(Utils.fprintf_list ~sep:",@ " (fun fmt e > Format.fprintf fmt "%s" (Z3.Expr.to_string e))) (List.map horn_var_to_expr vars) 

728 
) 

729 
; 

730 
let expr = Z3.Quantifier.mk_forall_const 

731 
!ctx (* context *) 

732 
(List.map horn_var_to_expr vars) (* TODO provide bounded variables as expr *) 

733 
(* sorts (\* sort list*\) *) 

734 
(* symbols (\* symbol list *\) *) 

735 
expr (* expression *) 

736 
None (* quantifier weight, None means 1 *) 

737 
[] (* pattern list ? *) 

738 
[] (* ? *) 

739 
None (* ? *) 

740 
None (* ? *) 

676 
(Utils.fprintf_list ~sep:",@ " (fun fmt e > 

677 
Format.fprintf fmt "%s" (Z3.Expr.to_string e))) 

678 
(List.map horn_var_to_expr vars); 

679 
let expr = 

680 
Z3.Quantifier.mk_forall_const !ctx 

681 
(* context *) 

682 
(List.map horn_var_to_expr vars) 

683 
(* TODO provide bounded variables as expr *) 

684 
(* sorts (\* sort list*\) *) 

685 
(* symbols (\* symbol list *\) *) 

686 
expr (* expression *) None (* quantifier weight, None means 1 *) [] 

687 
(* pattern list ? *) [] (* ? *) None (* ? *) None 

688 
(* ? *) 

741  689 
in 
690  
742  691 
(* Format.eprintf "OK@.@?"; *) 
743  692  
744 
(* 

745 
TODO: bizarre la declaration de INIT tout seul semble poser pb. 

746 
*) 

747 
Z3.Fixedpoint.add_rule !fp 

748 
(Z3.Quantifier.expr_of_quantifier expr) 

749 
None 

693 
(* TODO: bizarre la declaration de INIT tout seul semble poser pb. *) 

694 
Z3.Fixedpoint.add_rule !fp (Z3.Quantifier.expr_of_quantifier expr) None 

750  695  
751 


752  696 
(********************************************************) 
753 


697  
754  698 
let machine_reset machines m = 
755  699 
let locals = local_memory_vars m in 
756 


700  
757  701 
(* print "x_m = x_c" for each local memory *) 
758  702 
let mid_mem_def = 
759 
List.map (fun v > 

760 
Z3.Boolean.mk_eq !ctx 

761 
(horn_var_to_expr (rename_mid v)) 

762 
(horn_var_to_expr (rename_current v)) 

763 
) locals 

703 
List.map 

704 
(fun v > 

705 
Z3.Boolean.mk_eq !ctx 

706 
(horn_var_to_expr (rename_mid v)) 

707 
(horn_var_to_expr (rename_current v))) 

708 
locals 

764  709 
in 
765  710  
766 
(* print "child_reset ( associated vars _ {c,m} )" for each subnode. 

767 
Special treatment for _arrow: _first = true 

768 
*) 

769  
711 
(* print "child_reset ( associated vars _ {c,m} )" for each subnode. Special 

712 
treatment for _arrow: _first = true *) 

770  713 
let reset_instances = 
771 


772 
List.map (fun (id, (n, _)) > 

773 
let name = node_name n in 

774 
if name = "_arrow" then ( 

775 
Z3.Boolean.mk_eq !ctx 

776 
( 

777 
let vdecl = get_fdecl ((concat m.mname.node_id id) ^ "._arrow._first_m") in 

778 
Z3.Expr.mk_const_f !ctx vdecl 

779 
) 

780 
(Z3.Boolean.mk_true !ctx) 

781 


782 
) else ( 

783 
let machine_n = get_machine machines name in 

784 


785 
Z3.Expr.mk_app 

786 
!ctx 

787 
(get_fdecl (name ^ "_reset")) 

788 
(List.map (horn_var_to_expr) 

789 
(idx::uid:: (* Additional vars: counters, uid *) 

790 
(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n)) 

791 
)) 

792 


793 
) 

794 
) m.minstances 

795 


796 


714 
List.map 

715 
(fun (id, (n, _)) > 

716 
let name = node_name n in 

717 
if name = "_arrow" then 

718 
Z3.Boolean.mk_eq !ctx 

719 
(let vdecl = 

720 
get_fdecl (concat m.mname.node_id id ^ "._arrow._first_m") 

721 
in 

722 
Z3.Expr.mk_const_f !ctx vdecl) 

723 
(Z3.Boolean.mk_true !ctx) 

724 
else 

725 
let machine_n = get_machine machines name in 

726  
727 
Z3.Expr.mk_app !ctx 

728 
(get_fdecl (name ^ "_reset")) 

729 
(List.map horn_var_to_expr 

730 
(idx 

731 
:: 

732 
uid 

733 
:: 

734 
(* Additional vars: counters, uid *) 

735 
rename_machine_list 

736 
(concat m.mname.node_id id) 

737 
(reset_vars machines machine_n)))) 

738 
m.minstances 

797  739 
in 
798 


740  
799  741 
Z3.Boolean.mk_and !ctx (mid_mem_def @ reset_instances) 
800 


801 


802  742  
803 
(* TODO: empty list means true statement *)


743 
(* TODO: empty list means true statement *) 

804  744 
let decl_machine machines m = 
805 
if m.mname.node_id = Arrow.arrow_id then 

806 
(* We don't do arrow function *) 

745 
if m.mname.node_id = Arrow.arrow_id then (* We don't do arrow function *) 

807  746 
() 
808  747 
else 
809 
begin 

810 
let _ = 

811 
List.map decl_var 

812 
( 

813 
(inout_vars m)@ 

814 
(rename_current_list (full_memory_vars machines m)) @ 

815 
(rename_mid_list (full_memory_vars machines m)) @ 

816 
(rename_next_list (full_memory_vars machines m)) @ 

817 
(rename_machine_list m.mname.node_id m.mstep.step_locals) 

818 
) 

748 
let _ = 

749 
List.map decl_var 

750 
(inout_vars m 

751 
@ rename_current_list (full_memory_vars machines m) 

752 
@ rename_mid_list (full_memory_vars machines m) 

753 
@ rename_next_list (full_memory_vars machines m) 

754 
@ rename_machine_list m.mname.node_id m.mstep.step_locals) 

755 
in 

756 
if is_stateless m then ( 

757 
if !debug then 

758 
Format.eprintf "Declaring a stateless machine: %s@." m.mname.node_id; 

759  
760 
(* Declaring single predicate *) 

761 
let vars = inout_vars m in 

762 
let vars_types = List.map (fun v > type_to_sort v.var_type) vars in 

763 
let _ = decl_rel (machine_stateless_name m.mname.node_id) vars_types in 

764  
765 
let horn_body, _ (* don't care for reset here *) = 

766 
instrs_to_expr machines [] (* No reset info for stateless nodes *) m 

767 
m.mstep.step_instrs 

768 
in 

769 
let horn_head = 

770 
Z3.Expr.mk_app !ctx 

771 
(get_fdecl (machine_stateless_name m.mname.node_id)) 

772 
(List.map horn_var_to_expr 

773 
(idx :: uid :: (* Additional vars: counters, uid *) 

774 
vars)) 

775 
in 

776 
(* this line seems useless *) 

777 
let vars = 

778 
idx :: uid :: vars 

779 
@ rename_machine_list m.mname.node_id m.mstep.step_locals 

780 
in 

781 
(* Format.eprintf "useless Vars: %a@." (Utils.fprintf_list ~sep:"@ " 

782 
Printers.pp_var) vars; *) 

783 
match m.mstep.step_asserts with 

784 
 [] > 

785 
(* Rule for single predicate : "; Stateless step rule @." *) 

786 
(*let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in*) 

787 
(* TODO clean code *) 

788 
(* Format.eprintf "used Vars: %a@." (Utils.fprintf_list ~sep:"@ " 

789 
Printers.pp_var) vars; *) 

790 
add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head) 

791 
 assertsl > 

792 
(*Rule for step "; Stateless step rule with Assertions @.";*) 

793 
let body_with_asserts = 

794 
Z3.Boolean.mk_and !ctx 

795 
(horn_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl) 

796 
in 

797 
let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in 

798 
add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head)) 

799 
else 

800 
(* Rule for reset *) 

801 
let vars = reset_vars machines m in 

802 
let vars_types = List.map (fun v > type_to_sort v.var_type) vars in 

803 
let _ = decl_rel (machine_reset_name m.mname.node_id) vars_types in 

804 
let horn_reset_body = machine_reset machines m in 

805 
let horn_reset_head = 

806 
Z3.Expr.mk_app !ctx 

807 
(get_fdecl (machine_reset_name m.mname.node_id)) 

808 
(List.map horn_var_to_expr 

809 
(idx :: uid :: (* Additional vars: counters, uid *) 

810 
vars)) 

819  811 
in 
820 
if is_stateless m then 

821 
begin 

822 
if !debug then 

823 
Format.eprintf "Declaring a stateless machine: %s@." m.mname.node_id; 

824  
825 
(* Declaring single predicate *) 

826 
let vars = inout_vars m in 

827 
let vars_types = List.map (fun v > type_to_sort v.var_type) vars in 

828 
let _ = decl_rel (machine_stateless_name m.mname.node_id) vars_types in 

829 


830 
let horn_body, _ (* don't care for reset here *) = 

831 
instrs_to_expr 

832 
machines 

833 
([] (* No reset info for stateless nodes *) ) 

834 
m 

835 
m.mstep.step_instrs 

836 
in 

837 
let horn_head = 

838 
Z3.Expr.mk_app 

839 
!ctx 

840 
(get_fdecl (machine_stateless_name m.mname.node_id)) 

841 
( List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars)) 

842 
in 

843 
(* this line seems useless *) 

844 
let vars = idx::uid::vars@(rename_machine_list m.mname.node_id m.mstep.step_locals) in 

845 
(* Format.eprintf "useless Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *) 

846 
match m.mstep.step_asserts with 

847 
 [] > 

848 
begin 

849 
(* Rule for single predicate : "; Stateless step rule @." *) 

850 
(*let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in*) 

851 
(* TODO clean code *) 

852 
(* Format.eprintf "used Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *) 

853 
add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head) 

854 


855 
end 

856 
 assertsl > 

857 
begin 

858 
(*Rule for step "; Stateless step rule with Assertions @.";*) 

859 
let body_with_asserts = 

860 
Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl) 

861 
in 

862 
let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in 

863 
add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head) 

864 
end 

865 
end 

866 
else 

867 
begin 

868  
869 
(* Rule for reset *) 

870  
871 
let vars = reset_vars machines m in 

872 
let vars_types = List.map (fun v > type_to_sort v.var_type) vars in 

873 
let _ = decl_rel (machine_reset_name m.mname.node_id) vars_types in 

874 
let horn_reset_body = machine_reset machines m in 

875 
let horn_reset_head = 

876 
Z3.Expr.mk_app 

877 
!ctx 

878 
(get_fdecl (machine_reset_name m.mname.node_id)) 

879 
( List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars)) 

880 
in 

881  
882 


883 
let _ = 

884 
add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head) 

885 


886 
in 

887  
888 
(* Rule for step*) 

889 
let vars = step_vars machines m in 

890 
let vars_types = List.map (fun v > type_to_sort v.var_type) vars in 

891 
let _ = decl_rel (machine_step_name m.mname.node_id) vars_types in 

892 
let horn_step_body, _ (* don't care for reset here *) = 

893 
instrs_to_expr 

894 
machines 

895 
[] 

896 
m 

897 
m.mstep.step_instrs 

898 
in 

899 
let horn_step_head = 

900 
Z3.Expr.mk_app 

901 
!ctx 

902 
(get_fdecl (machine_step_name m.mname.node_id)) 

903 
( List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars)) 

904 
in 

905 
match m.mstep.step_asserts with 

906 
 [] > 

907 
begin 

908 
(* Rule for single predicate *) 

909 
let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in 

910 
add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head) 

911 


912 
end 

913 
 assertsl > 

914 
begin 

915 
(* Rule for step Assertions @.; *) 

916 
let body_with_asserts = 

917 
Z3.Boolean.mk_and !ctx 

918 
(horn_step_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl) 

919 
in 

920 
let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in 

921 
add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head) 

922 


923 
end 

924 


925 
end 

926 
end 
Also available in: Unified diff
reformatting