Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/tools/zustre/zustre_analyze.ml | ||
---|---|---|
1 | 1 |
(* This module takes a main node (reset and step) and a property. It assumes |
2 |
that the system is properly defined and check that the property is valid.
|
|
2 |
that the system is properly defined and check that the property is valid. |
|
3 | 3 |
|
4 | 4 |
When valid, it returns a set of local invariants. Otherwise, it returns a cex |
5 |
expressed as a sequence of input values. |
|
6 |
|
|
7 |
*) |
|
5 |
expressed as a sequence of input values. *) |
|
8 | 6 |
open Lustre_types |
9 | 7 |
open Machine_code_types |
10 | 8 |
open Machine_code_common |
11 | 9 |
open Zustre_common |
12 | 10 |
open Zustre_data |
13 | 11 |
|
14 |
let idx_0 = Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 |
|
15 |
let uid_0 = Z3.Z3List.nil uid_sort |
|
16 |
|
|
17 |
let check machines node = |
|
12 |
let idx_0 = Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 |
|
13 |
|
|
14 |
let uid_0 = Z3.Z3List.nil uid_sort |
|
18 | 15 |
|
16 |
let check machines node = |
|
19 | 17 |
let machine = get_machine machines node in |
20 | 18 |
let node_id = machine.mname.node_id in |
19 |
|
|
21 | 20 |
(* Declaring collecting semantics *) |
22 |
|
|
23 |
let main_output = |
|
24 |
rename_machine_list node_id machine.mstep.step_outputs |
|
25 |
in |
|
21 |
let main_output = rename_machine_list node_id machine.mstep.step_outputs in |
|
26 | 22 |
let main_output_dummy = |
27 | 23 |
rename_machine_list ("dummy" ^ node_id) machine.mstep.step_outputs |
28 | 24 |
in |
29 |
let main_input = |
|
30 |
rename_machine_list node_id machine.mstep.step_inputs |
|
31 |
in |
|
32 |
let main_input_dummy = |
|
25 |
let main_input = rename_machine_list node_id machine.mstep.step_inputs in |
|
26 |
let main_input_dummy = |
|
33 | 27 |
rename_machine_list ("dummy" ^ node_id) machine.mstep.step_inputs |
34 |
in
|
|
28 |
in |
|
35 | 29 |
let main_memory_next = |
36 |
main_input @ (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @ |
|
37 |
main_output |
|
30 |
main_input |
|
31 |
@ rename_next_list |
|
32 |
(* machine.mname.node_id *) |
|
33 |
(full_memory_vars machines machine) |
|
34 |
@ main_output |
|
38 | 35 |
in |
39 | 36 |
let main_memory_current = |
40 |
main_input_dummy @ (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @ |
|
41 |
main_output_dummy |
|
37 |
main_input_dummy |
|
38 |
@ rename_current_list |
|
39 |
(* machine.mname.node_id *) |
|
40 |
(full_memory_vars machines machine) |
|
41 |
@ main_output_dummy |
|
42 | 42 |
in |
43 | 43 |
|
44 |
(* TODO: push/pop? donner un nom different par instance pour les garder dans le buffer ? |
|
45 |
Faut-il declarer les "rel" dans la hashtbl ? |
|
46 |
*) |
|
47 |
|
|
44 |
(* TODO: push/pop? donner un nom different par instance pour les garder dans |
|
45 |
le buffer ? Faut-il declarer les "rel" dans la hashtbl ? *) |
|
48 | 46 |
let main_name node_id = "MAIN" ^ "_" ^ node_id in |
49 |
|
|
47 |
|
|
50 | 48 |
let decl_main = |
51 |
decl_rel ~no_additional_vars:true |
|
52 |
(main_name node_id)
|
|
53 |
(int_sort::(List.map (fun v -> type_to_sort v.var_type) (main_memory_next))) in
|
|
49 |
decl_rel ~no_additional_vars:true (main_name node_id)
|
|
50 |
(int_sort :: List.map (fun v -> type_to_sort v.var_type) main_memory_next)
|
|
51 |
in |
|
54 | 52 |
|
55 |
|
|
56 |
|
|
57 | 53 |
(* Init case *) |
58 | 54 |
let decl_init = decl_rel ~no_additional_vars:true "INIT_STATE" [] in |
59 | 55 |
|
60 | 56 |
(* (special) rule INIT_STATE *) |
61 | 57 |
let init_expr = Z3.Expr.mk_app !ctx decl_init [] in |
62 | 58 |
Z3.Fixedpoint.add_rule !fp init_expr None; |
59 |
|
|
63 | 60 |
(* let _ = add_rule [] (Z3.Expr.mk_app *) |
64 | 61 |
(* !ctx *) |
65 | 62 |
(* decl_init *) |
... | ... | |
69 | 66 |
(* Re-declaring variables *) |
70 | 67 |
let _ = List.map decl_var main_memory_next in |
71 | 68 |
|
72 |
let horn_head = |
|
73 |
Z3.Expr.mk_app |
|
74 |
!ctx |
|
75 |
decl_main |
|
76 |
(idx_0::(* uid_0:: *)(List.map horn_var_to_expr main_memory_next)) |
|
69 |
let horn_head = |
|
70 |
Z3.Expr.mk_app !ctx decl_main |
|
71 |
(idx_0 :: (* uid_0:: *) |
|
72 |
List.map horn_var_to_expr main_memory_next) |
|
77 | 73 |
in |
78 | 74 |
(* Special case when the main node is stateless *) |
79 | 75 |
let _ = |
80 | 76 |
if Machine_code_common.is_stateless machine then |
81 |
begin |
|
82 |
|
|
83 |
(* Initial set: One Step(m,x) -- Stateless node *) |
|
84 |
(* rule => (INIT_STATE and step(mid, next)) MAIN(next) *) |
|
85 |
|
|
86 |
(* Note that vars here contains main_memory_next *) |
|
87 |
let vars = step_vars_m_x machines machine in |
|
88 |
(* Re-declaring variables *) |
|
89 |
let _ = List.map decl_var vars in |
|
90 |
|
|
91 |
let horn_body = |
|
92 |
Z3.Boolean.mk_and !ctx |
|
93 |
[ |
|
94 |
Z3.Expr.mk_app !ctx decl_init []; |
|
95 |
Z3.Expr.mk_app !ctx |
|
96 |
(get_fdecl (machine_stateless_name node)) |
|
97 |
(idx_0::uid_0::(List.map horn_var_to_expr vars)) |
|
98 |
] |
|
99 |
in |
|
100 |
add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head) |
|
101 |
|
|
102 |
|
|
103 |
end |
|
77 |
(* Initial set: One Step(m,x) -- Stateless node *) |
|
78 |
(* rule => (INIT_STATE and step(mid, next)) MAIN(next) *) |
|
79 |
|
|
80 |
(* Note that vars here contains main_memory_next *) |
|
81 |
let vars = step_vars_m_x machines machine in |
|
82 |
(* Re-declaring variables *) |
|
83 |
let _ = List.map decl_var vars in |
|
84 |
|
|
85 |
let horn_body = |
|
86 |
Z3.Boolean.mk_and !ctx |
|
87 |
[ |
|
88 |
Z3.Expr.mk_app !ctx decl_init []; |
|
89 |
Z3.Expr.mk_app !ctx |
|
90 |
(get_fdecl (machine_stateless_name node)) |
|
91 |
(idx_0 :: uid_0 :: List.map horn_var_to_expr vars); |
|
92 |
] |
|
93 |
in |
|
94 |
add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head) |
|
104 | 95 |
else |
105 |
begin |
|
106 |
(* Initial set: Reset(c,m) + One Step(m,x) @. *) |
|
107 |
|
|
108 |
(* Re-declaring variables *) |
|
109 |
let vars_reset = reset_vars machines machine in |
|
110 |
let vars_step = step_vars_m_x machines machine in |
|
111 |
let vars_step_all = step_vars_c_m_x machines machine in |
|
112 |
let _ = List.map decl_var (vars_reset @ vars_step @ vars_step_all ) in |
|
113 |
|
|
114 |
(* rule => (INIT_STATE and reset(mid) and step(mid, next)) MAIN(next) *) |
|
115 |
let horn_body = |
|
116 |
Z3.Boolean.mk_and !ctx |
|
117 |
[ |
|
118 |
Z3.Expr.mk_app !ctx decl_init []; |
|
119 |
Z3.Expr.mk_app !ctx |
|
120 |
(get_fdecl (machine_reset_name node)) |
|
121 |
(idx_0::uid_0::List.map horn_var_to_expr (reset_vars machines machine)); |
|
122 |
Z3.Expr.mk_app !ctx |
|
123 |
(get_fdecl (machine_step_name node)) |
|
124 |
(idx_0::uid_0::List.map horn_var_to_expr (step_vars_m_x machines machine)) |
|
125 |
] |
|
126 |
in |
|
127 |
|
|
128 |
(* Vars contains all vars: in_out, current, mid, neXt memories *) |
|
129 |
let vars = step_vars_c_m_x machines machine in |
|
130 |
add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head) |
|
131 |
|
|
132 |
|
|
133 |
end |
|
96 |
(* Initial set: Reset(c,m) + One Step(m,x) @. *) |
|
97 |
|
|
98 |
(* Re-declaring variables *) |
|
99 |
let vars_reset = reset_vars machines machine in |
|
100 |
let vars_step = step_vars_m_x machines machine in |
|
101 |
let vars_step_all = step_vars_c_m_x machines machine in |
|
102 |
let _ = List.map decl_var (vars_reset @ vars_step @ vars_step_all) in |
|
103 |
|
|
104 |
(* rule => (INIT_STATE and reset(mid) and step(mid, next)) MAIN(next) *) |
|
105 |
let horn_body = |
|
106 |
Z3.Boolean.mk_and !ctx |
|
107 |
[ |
|
108 |
Z3.Expr.mk_app !ctx decl_init []; |
|
109 |
Z3.Expr.mk_app !ctx |
|
110 |
(get_fdecl (machine_reset_name node)) |
|
111 |
(idx_0 |
|
112 |
:: |
|
113 |
uid_0 :: List.map horn_var_to_expr (reset_vars machines machine)); |
|
114 |
Z3.Expr.mk_app !ctx |
|
115 |
(get_fdecl (machine_step_name node)) |
|
116 |
(idx_0 |
|
117 |
:: |
|
118 |
uid_0 |
|
119 |
:: List.map horn_var_to_expr (step_vars_m_x machines machine)); |
|
120 |
] |
|
121 |
in |
|
122 |
|
|
123 |
(* Vars contains all vars: in_out, current, mid, neXt memories *) |
|
124 |
let vars = step_vars_c_m_x machines machine in |
|
125 |
add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head) |
|
134 | 126 |
in |
135 |
|
|
136 |
let step_name = |
|
137 |
if Machine_code_common.is_stateless machine then |
|
138 |
machine_stateless_name |
|
139 |
else |
|
140 |
machine_step_name |
|
127 |
|
|
128 |
let step_name = |
|
129 |
if Machine_code_common.is_stateless machine then machine_stateless_name |
|
130 |
else machine_step_name |
|
141 | 131 |
in |
142 |
|
|
143 |
(* ; Inductive def@. *) |
|
144 | 132 |
|
133 |
(* ; Inductive def@. *) |
|
145 | 134 |
List.iter (fun x -> ignore (decl_var x)) (main_output_dummy @ main_input_dummy); |
146 |
|
|
147 |
(* (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy; *) |
|
135 |
|
|
136 |
(* (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var |
|
137 |
v)) fmt main_output_dummy; *) |
|
148 | 138 |
|
149 | 139 |
(* fprintf fmt *) |
150 |
(* "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@." *) |
|
140 |
(* "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN |
|
141 |
%a)@]@.))@.@." *) |
|
151 | 142 |
(* (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_current *) |
152 | 143 |
(* step_name node *) |
153 |
(* (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine) *) |
|
154 |
|
|
155 |
let k = Corelang.dummy_var_decl "k" Type_predef.type_int (*Corelang.mktyp Location.dummy_loc Types.type_int*) in |
|
144 |
(* (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines |
|
145 |
machine) *) |
|
146 |
let k = |
|
147 |
Corelang.dummy_var_decl "k" Type_predef.type_int |
|
148 |
(*Corelang.mktyp Location.dummy_loc Types.type_int*) |
|
149 |
in |
|
156 | 150 |
let k_var = Z3.Expr.mk_const_f !ctx (decl_var k) in |
157 |
|
|
158 |
let horn_head = |
|
159 |
Z3.Expr.mk_app |
|
160 |
!ctx |
|
161 |
decl_main |
|
162 |
((Z3.Arithmetic.mk_add |
|
163 |
!ctx |
|
164 |
[k_var; Z3.Arithmetic.Integer.mk_numeral_i !ctx 1] |
|
165 |
)::(List.map horn_var_to_expr main_memory_next)) |
|
151 |
|
|
152 |
let horn_head = |
|
153 |
Z3.Expr.mk_app !ctx decl_main |
|
154 |
(Z3.Arithmetic.mk_add !ctx |
|
155 |
[ k_var; Z3.Arithmetic.Integer.mk_numeral_i !ctx 1 ] |
|
156 |
:: List.map horn_var_to_expr main_memory_next) |
|
166 | 157 |
in |
167 | 158 |
let horn_body = |
168 | 159 |
Z3.Boolean.mk_and !ctx |
169 | 160 |
[ |
170 |
Z3.Expr.mk_app !ctx decl_main (k_var::(List.map horn_var_to_expr main_memory_current)); |
|
171 |
Z3.Expr.mk_app !ctx (get_fdecl (step_name node)) (k_var::uid_0::List.map horn_var_to_expr (step_vars machines machine)) |
|
161 |
Z3.Expr.mk_app !ctx decl_main |
|
162 |
(k_var :: List.map horn_var_to_expr main_memory_current); |
|
163 |
Z3.Expr.mk_app !ctx |
|
164 |
(get_fdecl (step_name node)) |
|
165 |
(k_var |
|
166 |
:: uid_0 :: List.map horn_var_to_expr (step_vars machines machine)); |
|
172 | 167 |
] |
173 | 168 |
in |
174 | 169 |
(* Vars contains all vars: in_out, current, mid, neXt memories *) |
175 |
let vars = (step_vars_c_m_x machines machine) @ main_output_dummy @ main_input_dummy in |
|
170 |
let vars = |
|
171 |
step_vars_c_m_x machines machine @ main_output_dummy @ main_input_dummy |
|
172 |
in |
|
176 | 173 |
let _ = |
177 |
add_rule ~dont_touch:[decl_main] (k::vars) (Z3.Boolean.mk_implies !ctx horn_body horn_head)
|
|
178 |
|
|
174 |
add_rule ~dont_touch:[ decl_main ] (k :: vars)
|
|
175 |
(Z3.Boolean.mk_implies !ctx horn_body horn_head) |
|
179 | 176 |
in |
180 | 177 |
|
181 |
|
|
182 | 178 |
(* Property def *) |
183 | 179 |
let decl_err = decl_rel ~no_additional_vars:true "ERR" [] in |
184 | 180 |
|
185 |
let prop = |
|
186 |
Z3.Boolean.mk_and !ctx (List.map horn_var_to_expr main_output) |
|
187 |
in |
|
188 |
let not_prop = |
|
189 |
Z3.Boolean.mk_not !ctx prop |
|
190 |
in |
|
191 |
add_rule (*~dont_touch:[decl_main;decl_err]*) (k::main_memory_next) (Z3.Boolean.mk_implies !ctx |
|
192 |
( |
|
193 |
Z3.Boolean.mk_and !ctx |
|
194 |
[not_prop; |
|
195 |
Z3.Expr.mk_app !ctx decl_main (k_var::List.map horn_var_to_expr main_memory_next); |
|
196 |
] |
|
197 |
) |
|
198 |
(Z3.Expr.mk_app !ctx decl_err [])) |
|
199 |
; |
|
200 |
|
|
201 |
(* fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@." *) |
|
202 |
(* (pp_conj (pp_horn_var machine)) main_output *) |
|
203 |
(* (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next *) |
|
204 |
(* ; *) |
|
205 |
(* if !Options.horn_query then fprintf fmt "(query ERR)@." *) |
|
206 |
|
|
207 |
(* Debug instructions *) |
|
181 |
let prop = Z3.Boolean.mk_and !ctx (List.map horn_var_to_expr main_output) in |
|
182 |
let not_prop = Z3.Boolean.mk_not !ctx prop in |
|
183 |
add_rule |
|
184 |
(*~dont_touch:[decl_main;decl_err]*) |
|
185 |
(k :: main_memory_next) |
|
186 |
(Z3.Boolean.mk_implies !ctx |
|
187 |
(Z3.Boolean.mk_and !ctx |
|
188 |
[ |
|
189 |
not_prop; |
|
190 |
Z3.Expr.mk_app !ctx decl_main |
|
191 |
(k_var :: List.map horn_var_to_expr main_memory_next); |
|
192 |
]) |
|
193 |
(Z3.Expr.mk_app !ctx decl_err [])); |
|
194 |
|
|
195 |
(* fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ |
|
196 |
ERR))@." *) |
|
197 |
(* (pp_conj (pp_horn_var machine)) main_output *) |
|
198 |
(* (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next *) |
|
199 |
(* ; *) |
|
200 |
(* if !Options.horn_query then fprintf fmt "(query ERR)@." *) |
|
201 |
|
|
202 |
(* Debug instructions *) |
|
208 | 203 |
let rules_expr = Z3.Fixedpoint.get_rules !fp in |
209 | 204 |
if !debug then |
210 | 205 |
Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." |
211 |
(Utils.fprintf_list ~sep:"@ "
|
|
212 |
(fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) )
|
|
206 |
(Utils.fprintf_list ~sep:"@ " (fun fmt e ->
|
|
207 |
Format.pp_print_string fmt (Z3.Expr.to_string e)))
|
|
213 | 208 |
rules_expr; |
214 | 209 |
try |
215 |
let res_status = Z3.Fixedpoint.query_r !fp [decl_err] in
|
|
216 |
|
|
210 |
let res_status = Z3.Fixedpoint.query_r !fp [ decl_err ] in
|
|
211 |
|
|
217 | 212 |
Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status); |
218 | 213 |
match res_status with |
219 |
| Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex machine machines decl_err |
|
220 |
|
|
221 |
| Z3.Solver.UNSATISFIABLE -> (*build_inv*) ( |
|
214 |
| Z3.Solver.SATISFIABLE -> |
|
215 |
Zustre_cex.build_cex machine machines decl_err |
|
216 |
| Z3.Solver.UNSATISFIABLE -> ( |
|
217 |
(*build_inv*) |
|
222 | 218 |
let expr_opt = Z3.Fixedpoint.get_answer !fp in |
223 | 219 |
match expr_opt with |
224 |
None -> if !debug then Format.eprintf "Unsat No feedback@." |
|
225 |
| Some e -> if !debug then Format.eprintf "Unsat Result: %s@." (Z3.Expr.to_string e) |
|
226 |
) |
|
227 |
| Z3.Solver.UNKNOWN -> () |
|
228 |
with Z3.Error msg -> Format.eprintf "Z3 failure: %s@." msg; () |
|
220 |
| None -> |
|
221 |
if !debug then Format.eprintf "Unsat No feedback@." |
|
222 |
| Some e -> |
|
223 |
if !debug then Format.eprintf "Unsat Result: %s@." (Z3.Expr.to_string e) |
|
224 |
) |
|
225 |
| Z3.Solver.UNKNOWN -> |
|
226 |
() |
|
227 |
with Z3.Error msg -> |
|
228 |
Format.eprintf "Z3 failure: %s@." msg; |
|
229 |
() |
|
229 | 230 |
(* Local Variables: *) |
230 | 231 |
(* compile-command:"make -C ../.. lustrev" *) |
231 | 232 |
(* End: *) |
Also available in: Unified diff
reformatting