Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/backends/Horn/horn_backend_collecting_sem.ml | ||
---|---|---|
12 | 12 |
(* The compilation presented here was first defined in Garoche, Gurfinkel, |
13 | 13 |
Kahsai, HCSV'14. |
14 | 14 |
|
15 |
This is a modified version that handle reset |
|
16 |
*) |
|
15 |
This is a modified version that handle reset *) |
|
17 | 16 |
|
18 | 17 |
open Format |
19 | 18 |
open Lustre_types |
20 | 19 |
open Machine_code_types |
21 |
|
|
22 | 20 |
open Horn_backend_common |
23 | 21 |
open Horn_backend_printers |
24 | 22 |
|
... | ... | |
29 | 27 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
30 | 28 |
in |
31 | 29 |
let main_output_dummy = |
32 |
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs |
|
30 |
rename_machine_list |
|
31 |
("dummy" ^ machine.mname.node_id) |
|
32 |
machine.mstep.step_outputs |
|
33 | 33 |
in |
34 | 34 |
let main_memory_next = |
35 |
(rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @ |
|
36 |
main_output |
|
35 |
rename_next_list |
|
36 |
(* machine.mname.node_id *) |
|
37 |
(full_memory_vars machines machine) |
|
38 |
@ main_output |
|
37 | 39 |
in |
38 | 40 |
let main_memory_current = |
39 |
(rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @ |
|
40 |
main_output_dummy |
|
41 |
rename_current_list |
|
42 |
(* machine.mname.node_id *) |
|
43 |
(full_memory_vars machines machine) |
|
44 |
@ main_output_dummy |
|
41 | 45 |
in |
42 | 46 |
|
43 | 47 |
fprintf fmt "(declare-rel MAIN (%a))@." |
44 | 48 |
(Utils.fprintf_list ~sep:" " pp_type) |
45 | 49 |
(List.map (fun v -> v.var_type) main_memory_next); |
46 | 50 |
|
47 |
|
|
48 | 51 |
(* Init case *) |
49 |
let _ =
|
|
52 |
let _ = |
|
50 | 53 |
(* Special case when the main node is stateless *) |
51 | 54 |
if Machine_code_common.is_stateless machine then ( |
52 | 55 |
let step_name = pp_machine_stateless_name in |
... | ... | |
55 | 58 |
fprintf fmt "(rule INIT_STATE)@."; |
56 | 59 |
fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>"; |
57 | 60 |
fprintf fmt "INIT_STATE@ "; |
58 |
fprintf fmt "(@[<v 0>%a %a@])" |
|
59 |
step_name node
|
|
60 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine);
|
|
61 |
fprintf fmt "(@[<v 0>%a %a@])" step_name node
|
|
62 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine))
|
|
63 |
(step_vars_m_x machines machine);
|
|
61 | 64 |
fprintf fmt "@]@ )@ "; |
62 | 65 |
fprintf fmt "(MAIN %a)@]@.))@.@." |
63 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next ; |
|
64 |
) |
|
65 |
else ( |
|
66 |
let reset_name, step_name = |
|
67 |
pp_machine_reset_name, pp_machine_step_name |
|
68 |
in |
|
66 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) |
|
67 |
main_memory_next) |
|
68 |
else |
|
69 |
let reset_name, step_name = pp_machine_reset_name, pp_machine_step_name in |
|
69 | 70 |
fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @."; |
70 | 71 |
fprintf fmt "(declare-rel INIT_STATE ())@."; |
71 | 72 |
fprintf fmt "(rule INIT_STATE)@."; |
72 | 73 |
fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>"; |
73 | 74 |
fprintf fmt "INIT_STATE@ "; |
74 |
fprintf fmt "(@[<v 0>%a %a@])@ " |
|
75 |
reset_name node
|
|
76 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (reset_vars machines machine);
|
|
77 |
fprintf fmt "(@[<v 0>%a %a@])" |
|
78 |
step_name node
|
|
79 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine);
|
|
80 |
|
|
75 |
fprintf fmt "(@[<v 0>%a %a@])@ " reset_name node
|
|
76 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine))
|
|
77 |
(reset_vars machines machine);
|
|
78 |
fprintf fmt "(@[<v 0>%a %a@])" step_name node
|
|
79 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine))
|
|
80 |
(step_vars_m_x machines machine);
|
|
81 |
|
|
81 | 82 |
fprintf fmt "@]@ )@ "; |
82 | 83 |
fprintf fmt "(MAIN %a)@]@.))@.@." |
83 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next ;
|
|
84 |
)
|
|
84 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine))
|
|
85 |
main_memory_next
|
|
85 | 86 |
in |
86 | 87 |
|
87 |
let step_name = |
|
88 |
if Machine_code_common.is_stateless machine then |
|
89 |
pp_machine_stateless_name |
|
90 |
else |
|
91 |
pp_machine_step_name |
|
88 |
let step_name = |
|
89 |
if Machine_code_common.is_stateless machine then pp_machine_stateless_name |
|
90 |
else pp_machine_step_name |
|
92 | 91 |
in |
93 |
|
|
92 |
|
|
94 | 93 |
fprintf fmt "; Inductive def@."; |
95 |
(Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy; |
|
94 |
(Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) |
|
95 |
fmt main_output_dummy; |
|
96 | 96 |
fprintf fmt |
97 |
"@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@." |
|
98 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_current |
|
99 |
step_name node |
|
100 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine) |
|
101 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next |
|
102 |
|
|
97 |
"@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN \ |
|
98 |
%a)@]@.))@.@." |
|
99 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) |
|
100 |
main_memory_current step_name node |
|
101 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) |
|
102 |
(step_vars machines machine) |
|
103 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) |
|
104 |
main_memory_next |
|
103 | 105 |
|
104 | 106 |
let check_prop machines fmt machine = |
105 | 107 |
let main_output = |
106 | 108 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
107 | 109 |
in |
108 | 110 |
let main_memory_next = |
109 |
(rename_next_list (full_memory_vars machines machine)) @ main_output
|
|
111 |
rename_next_list (full_memory_vars machines machine) @ main_output
|
|
110 | 112 |
in |
111 | 113 |
fprintf fmt "; Property def@."; |
112 | 114 |
fprintf fmt "(declare-rel ERR ())@."; |
113 | 115 |
fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@." |
114 |
(pp_conj (pp_horn_var machine)) main_output
|
|
115 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next
|
|
116 |
;
|
|
117 |
if !Options.horn_query then fprintf fmt "(query ERR)@."
|
|
118 |
|
|
116 |
(pp_conj (pp_horn_var machine)) |
|
117 |
main_output
|
|
118 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine))
|
|
119 |
main_memory_next;
|
|
120 |
if !Options.horn_query then fprintf fmt "(query ERR)@." |
|
119 | 121 |
|
120 | 122 |
let cex_computation machines fmt node machine = |
121 | 123 |
fprintf fmt "; CounterExample computation for node %s@.@." node; |
122 |
(* We print the types of the cex node "memory tree" TODO: add the output *)
|
|
124 |
(* We print the types of the cex node "memory tree" TODO: add the output *) |
|
123 | 125 |
let cex_input = |
124 | 126 |
rename_machine_list machine.mname.node_id machine.mstep.step_inputs |
125 | 127 |
in |
126 | 128 |
let cex_input_dummy = |
127 |
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs |
|
129 |
rename_machine_list |
|
130 |
("dummy" ^ machine.mname.node_id) |
|
131 |
machine.mstep.step_inputs |
|
128 | 132 |
in |
129 | 133 |
let cex_output = |
130 | 134 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
131 | 135 |
in |
132 | 136 |
let cex_output_dummy = |
133 |
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs |
|
137 |
rename_machine_list |
|
138 |
("dummy" ^ machine.mname.node_id) |
|
139 |
machine.mstep.step_outputs |
|
134 | 140 |
in |
135 | 141 |
let cex_memory_next = |
136 |
cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output |
|
142 |
cex_input |
|
143 |
@ rename_next_list (full_memory_vars machines machine) |
|
144 |
@ cex_output |
|
137 | 145 |
in |
138 | 146 |
let cex_memory_current = |
139 |
cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy |
|
147 |
cex_input_dummy |
|
148 |
@ rename_current_list (full_memory_vars machines machine) |
|
149 |
@ cex_output_dummy |
|
140 | 150 |
in |
141 | 151 |
|
142 |
(* Special case when the cex node is stateless *)
|
|
152 |
(* Special case when the cex node is stateless *) |
|
143 | 153 |
let reset_name, step_name = |
144 | 154 |
if Machine_code_common.is_stateless machine then |
145 | 155 |
pp_machine_stateless_name, pp_machine_stateless_name |
146 |
else |
|
147 |
pp_machine_reset_name, pp_machine_step_name |
|
156 |
else pp_machine_reset_name, pp_machine_step_name |
|
148 | 157 |
in |
149 | 158 |
|
150 | 159 |
fprintf fmt "(declare-rel CEX (Int %a))@.@." |
... | ... | |
156 | 165 |
fprintf fmt "(rule INIT_STATE_CEX)@."; |
157 | 166 |
fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>"; |
158 | 167 |
fprintf fmt "INIT_STATE_CEX@ "; |
159 |
fprintf fmt "(@[<v 0>%a %a@])@ " |
|
160 |
reset_name node
|
|
161 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (reset_vars machines machine);
|
|
162 |
fprintf fmt "(@[<v 0>%a %a@])" |
|
163 |
step_name node
|
|
164 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine);
|
|
165 |
|
|
168 |
fprintf fmt "(@[<v 0>%a %a@])@ " reset_name node
|
|
169 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine))
|
|
170 |
(reset_vars machines machine); |
|
171 |
fprintf fmt "(@[<v 0>%a %a@])" step_name node
|
|
172 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine))
|
|
173 |
(step_vars_m_x machines machine); |
|
174 |
|
|
166 | 175 |
fprintf fmt "@]@ )@ "; |
167 | 176 |
fprintf fmt "(CEX 0 %a)@]@.))@.@." |
168 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next ; |
|
177 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) |
|
178 |
cex_memory_next; |
|
169 | 179 |
|
170 | 180 |
fprintf fmt "; Inductive def@."; |
171 |
(* Declare dummy inputs. Outputs should have been declared previously with collecting sem *) |
|
172 |
(Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy; |
|
181 |
(* Declare dummy inputs. Outputs should have been declared previously with |
|
182 |
collecting sem *) |
|
183 |
(Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) |
|
184 |
fmt cex_input_dummy; |
|
173 | 185 |
fprintf fmt "(declare-var cexcpt Int)@."; |
174 | 186 |
fprintf fmt |
175 |
"@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@." |
|
176 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_current |
|
177 |
step_name node |
|
178 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine) |
|
179 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next |
|
187 |
"@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ \ |
|
188 |
(CEX (+ 1 cexcpt) %a)@]@.))@.@." |
|
189 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) |
|
190 |
cex_memory_current step_name node |
|
191 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) |
|
192 |
(step_vars machines machine) |
|
193 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) |
|
194 |
cex_memory_next |
|
180 | 195 |
|
181 | 196 |
let get_cex machines fmt machine = |
182 |
let cex_input =
|
|
183 |
rename_machine_list machine.mname.node_id machine.mstep.step_inputs
|
|
184 |
in
|
|
185 |
let cex_output =
|
|
186 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs
|
|
187 |
in
|
|
197 |
let cex_input = |
|
198 |
rename_machine_list machine.mname.node_id machine.mstep.step_inputs |
|
199 |
in |
|
200 |
let cex_output = |
|
201 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
|
202 |
in |
|
188 | 203 |
let cex_memory_next = |
189 |
cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output |
|
204 |
cex_input |
|
205 |
@ rename_next_list (full_memory_vars machines machine) |
|
206 |
@ cex_output |
|
190 | 207 |
in |
191 | 208 |
fprintf fmt "; Property def@."; |
192 | 209 |
fprintf fmt "(declare-rel CEXTRACE ())@."; |
193 |
fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@." |
|
194 |
(pp_conj (pp_horn_var machine)) cex_output |
|
195 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next |
|
196 |
; |
|
210 |
fprintf fmt |
|
211 |
"@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@." |
|
212 |
(pp_conj (pp_horn_var machine)) |
|
213 |
cex_output |
|
214 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) |
|
215 |
cex_memory_next; |
|
197 | 216 |
fprintf fmt "(query CEXTRACE)@." |
198 | 217 |
|
199 | 218 |
(* Local Variables: *) |
Also available in: Unified diff
reformatting