Revision ca7ff3f7
Added by Lélio Brun 8 months 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