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.
|
3
|
|
4
|
When valid, it returns a set of local invariants. Otherwise, it returns a cex
|
5
|
expressed as a sequence of input values. *)
|
6
|
open Lustre_types
|
7
|
open Machine_code_types
|
8
|
open Machine_code_common
|
9
|
open Zustre_common
|
10
|
open Zustre_data
|
11
|
|
12
|
let idx_0 = Z3.Arithmetic.Integer.mk_numeral_i !ctx 0
|
13
|
|
14
|
let uid_0 = Z3.Z3List.nil uid_sort
|
15
|
|
16
|
let check machines node =
|
17
|
let machine = get_machine machines node in
|
18
|
let node_id = machine.mname.node_id in
|
19
|
|
20
|
(* Declaring collecting semantics *)
|
21
|
let main_output = rename_machine_list node_id machine.mstep.step_outputs in
|
22
|
let main_output_dummy =
|
23
|
rename_machine_list ("dummy" ^ node_id) machine.mstep.step_outputs
|
24
|
in
|
25
|
let main_input = rename_machine_list node_id machine.mstep.step_inputs in
|
26
|
let main_input_dummy =
|
27
|
rename_machine_list ("dummy" ^ node_id) machine.mstep.step_inputs
|
28
|
in
|
29
|
let main_memory_next =
|
30
|
main_input
|
31
|
@ rename_next_list
|
32
|
(* machine.mname.node_id *)
|
33
|
(full_memory_vars machines machine)
|
34
|
@ main_output
|
35
|
in
|
36
|
let main_memory_current =
|
37
|
main_input_dummy
|
38
|
@ rename_current_list
|
39
|
(* machine.mname.node_id *)
|
40
|
(full_memory_vars machines machine)
|
41
|
@ main_output_dummy
|
42
|
in
|
43
|
|
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 ? *)
|
46
|
let main_name node_id = "MAIN" ^ "_" ^ node_id in
|
47
|
|
48
|
let decl_main =
|
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
|
52
|
|
53
|
(* Init case *)
|
54
|
let decl_init = decl_rel ~no_additional_vars:true "INIT_STATE" [] in
|
55
|
|
56
|
(* (special) rule INIT_STATE *)
|
57
|
let init_expr = Z3.Expr.mk_app !ctx decl_init [] in
|
58
|
Z3.Fixedpoint.add_rule !fp init_expr None;
|
59
|
|
60
|
(* let _ = add_rule [] (Z3.Expr.mk_app *)
|
61
|
(* !ctx *)
|
62
|
(* decl_init *)
|
63
|
(* [] *)
|
64
|
(* ) in *)
|
65
|
|
66
|
(* Re-declaring variables *)
|
67
|
let _ = List.map decl_var main_memory_next in
|
68
|
|
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)
|
73
|
in
|
74
|
(* Special case when the main node is stateless *)
|
75
|
let _ =
|
76
|
if Machine_code_common.is_stateless machine then
|
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)
|
95
|
else
|
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)
|
126
|
in
|
127
|
|
128
|
let step_name =
|
129
|
if Machine_code_common.is_stateless machine then machine_stateless_name
|
130
|
else machine_step_name
|
131
|
in
|
132
|
|
133
|
(* ; Inductive def@. *)
|
134
|
List.iter (fun x -> ignore (decl_var x)) (main_output_dummy @ main_input_dummy);
|
135
|
|
136
|
(* (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var
|
137
|
v)) fmt main_output_dummy; *)
|
138
|
|
139
|
(* fprintf fmt *)
|
140
|
(* "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN
|
141
|
%a)@]@.))@.@." *)
|
142
|
(* (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_current *)
|
143
|
(* step_name node *)
|
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
|
150
|
let k_var = Z3.Expr.mk_const_f !ctx (decl_var k) in
|
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)
|
157
|
in
|
158
|
let horn_body =
|
159
|
Z3.Boolean.mk_and !ctx
|
160
|
[
|
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));
|
167
|
]
|
168
|
in
|
169
|
(* Vars contains all vars: in_out, current, mid, neXt memories *)
|
170
|
let vars =
|
171
|
step_vars_c_m_x machines machine @ main_output_dummy @ main_input_dummy
|
172
|
in
|
173
|
let _ =
|
174
|
add_rule ~dont_touch:[ decl_main ] (k :: vars)
|
175
|
(Z3.Boolean.mk_implies !ctx horn_body horn_head)
|
176
|
in
|
177
|
|
178
|
(* Property def *)
|
179
|
let decl_err = decl_rel ~no_additional_vars:true "ERR" [] in
|
180
|
|
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 *)
|
203
|
let rules_expr = Z3.Fixedpoint.get_rules !fp in
|
204
|
if !debug then
|
205
|
Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
|
206
|
(Utils.fprintf_list ~sep:"@ " (fun fmt e ->
|
207
|
Format.pp_print_string fmt (Z3.Expr.to_string e)))
|
208
|
rules_expr;
|
209
|
try
|
210
|
let res_status = Z3.Fixedpoint.query_r !fp [ decl_err ] in
|
211
|
|
212
|
Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status);
|
213
|
match res_status with
|
214
|
| Z3.Solver.SATISFIABLE ->
|
215
|
Zustre_cex.build_cex machine machines decl_err
|
216
|
| Z3.Solver.UNSATISFIABLE -> (
|
217
|
(*build_inv*)
|
218
|
let expr_opt = Z3.Fixedpoint.get_answer !fp in
|
219
|
match expr_opt with
|
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
|
()
|
230
|
(* Local Variables: *)
|
231
|
(* compile-command:"make -C ../.. lustrev" *)
|
232
|
(* End: *)
|