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 0-ary 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_n-1 val_n-1) |
|
| 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_n-1 val_n-1) ... 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