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
|
|
7
|
*)
|
8
|
open Lustre_types
|
9
|
open Machine_code_types
|
10
|
open Machine_code_common
|
11
|
open Zustre_common
|
12
|
open Zustre_data
|
13
|
|
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 =
|
18
|
|
19
|
let machine = get_machine machines node in
|
20
|
let node_id = machine.mname.node_id in
|
21
|
(* Declaring collecting semantics *)
|
22
|
|
23
|
let main_output =
|
24
|
rename_machine_list node_id machine.mstep.step_outputs
|
25
|
in
|
26
|
let main_output_dummy =
|
27
|
rename_machine_list ("dummy" ^ node_id) machine.mstep.step_outputs
|
28
|
in
|
29
|
let main_input =
|
30
|
rename_machine_list node_id machine.mstep.step_inputs
|
31
|
in
|
32
|
let main_input_dummy =
|
33
|
rename_machine_list ("dummy" ^ node_id) machine.mstep.step_inputs
|
34
|
in
|
35
|
let main_memory_next =
|
36
|
main_input @ (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
|
37
|
main_output
|
38
|
in
|
39
|
let main_memory_current =
|
40
|
main_input_dummy @ (rename_current_list (* machine.mname.node_id *) (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 le buffer ?
|
45
|
Faut-il declarer les "rel" dans la hashtbl ?
|
46
|
*)
|
47
|
|
48
|
let main_name node_id = "MAIN" ^ "_" ^ node_id in
|
49
|
|
50
|
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
|
54
|
|
55
|
|
56
|
|
57
|
(* Init case *)
|
58
|
let decl_init = decl_rel ~no_additional_vars:true "INIT_STATE" [] in
|
59
|
|
60
|
(* (special) rule INIT_STATE *)
|
61
|
let init_expr = Z3.Expr.mk_app !ctx decl_init [] in
|
62
|
Z3.Fixedpoint.add_rule !fp init_expr None;
|
63
|
(* let _ = add_rule [] (Z3.Expr.mk_app *)
|
64
|
(* !ctx *)
|
65
|
(* decl_init *)
|
66
|
(* [] *)
|
67
|
(* ) in *)
|
68
|
|
69
|
(* Re-declaring variables *)
|
70
|
let _ = List.map decl_var main_memory_next in
|
71
|
|
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))
|
77
|
in
|
78
|
(* Special case when the main node is stateless *)
|
79
|
let _ =
|
80
|
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
|
104
|
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
|
134
|
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
|
141
|
in
|
142
|
|
143
|
(* ; Inductive def@. *)
|
144
|
|
145
|
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; *)
|
148
|
|
149
|
(* fprintf fmt *)
|
150
|
(* "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@." *)
|
151
|
(* (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_current *)
|
152
|
(* 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
|
156
|
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))
|
166
|
in
|
167
|
let horn_body =
|
168
|
Z3.Boolean.mk_and !ctx
|
169
|
[
|
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))
|
172
|
]
|
173
|
in
|
174
|
(* 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
|
176
|
let _ =
|
177
|
add_rule ~dont_touch:[decl_main] (k::vars) (Z3.Boolean.mk_implies !ctx horn_body horn_head)
|
178
|
|
179
|
in
|
180
|
|
181
|
|
182
|
(* Property def *)
|
183
|
let decl_err = decl_rel ~no_additional_vars:true "ERR" [] in
|
184
|
|
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 *)
|
208
|
let rules_expr = Z3.Fixedpoint.get_rules !fp in
|
209
|
if !debug then
|
210
|
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)) )
|
213
|
rules_expr;
|
214
|
try
|
215
|
let res_status = Z3.Fixedpoint.query_r !fp [decl_err] in
|
216
|
|
217
|
Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status);
|
218
|
match res_status with
|
219
|
| Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex machine machines decl_err
|
220
|
|
221
|
| Z3.Solver.UNSATISFIABLE -> (*build_inv*) (
|
222
|
let expr_opt = Z3.Fixedpoint.get_answer !fp in
|
223
|
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; ()
|
229
|
(* Local Variables: *)
|
230
|
(* compile-command:"make -C ../.. lustrev" *)
|
231
|
(* End: *)
|