lustrec / src / backends / Horn / horn_backend_collecting_sem.ml @ 0d54d8a8
History | View | Annotate | Download (7.66 KB)
| 1 | 0dee2bc1 | ploc | (********************************************************************) |
|---|---|---|---|
| 2 | (* *) |
||
| 3 | (* The LustreC compiler toolset / The LustreC Development Team *) |
||
| 4 | (* Copyright 2012 - -- ONERA - CNRS - INPT *) |
||
| 5 | (* *) |
||
| 6 | (* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
||
| 7 | (* under the terms of the GNU Lesser General Public License *) |
||
| 8 | (* version 2.1. *) |
||
| 9 | (* *) |
||
| 10 | (********************************************************************) |
||
| 11 | |||
| 12 | (* The compilation presented here was first defined in Garoche, Gurfinkel, |
||
| 13 | Kahsai, HCSV'14. |
||
| 14 | |||
| 15 | This is a modified version that handle reset |
||
| 16 | *) |
||
| 17 | |||
| 18 | open Format |
||
| 19 | 8446bf03 | ploc | open Lustre_types |
| 20 | 0dee2bc1 | ploc | open Corelang |
| 21 | 089f94be | ploc | open Machine_code_types |
| 22 | 0dee2bc1 | ploc | |
| 23 | open Horn_backend_common |
||
| 24 | open Horn_backend_printers |
||
| 25 | |||
| 26 | let collecting_semantics machines fmt node machine = |
||
| 27 | fprintf fmt "; Collecting semantics for node %s@.@." node; |
||
| 28 | (* We print the types of the main node "memory tree" TODO: add the output *) |
||
| 29 | let main_output = |
||
| 30 | rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
||
| 31 | in |
||
| 32 | let main_output_dummy = |
||
| 33 | rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
|
||
| 34 | in |
||
| 35 | let main_memory_next = |
||
| 36 | (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @ |
||
| 37 | main_output |
||
| 38 | in |
||
| 39 | let main_memory_current = |
||
| 40 | (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @ |
||
| 41 | main_output_dummy |
||
| 42 | in |
||
| 43 | |||
| 44 | fprintf fmt "(declare-rel MAIN (%a))@." |
||
| 45 | (Utils.fprintf_list ~sep:" " pp_type) |
||
| 46 | (List.map (fun v -> v.var_type) main_memory_next); |
||
| 47 | |||
| 48 | 07ceae4c | ploc | |
| 49 | (* Init case *) |
||
| 50 | let _ = |
||
| 51 | (* Special case when the main node is stateless *) |
||
| 52 | if is_stateless machine then ( |
||
| 53 | let step_name = pp_machine_stateless_name in |
||
| 54 | fprintf fmt "; Initial set: One Step(m,x) -- Stateless node! @."; |
||
| 55 | fprintf fmt "(declare-rel INIT_STATE ())@."; |
||
| 56 | fprintf fmt "(rule INIT_STATE)@."; |
||
| 57 | fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>"; |
||
| 58 | fprintf fmt "INIT_STATE@ "; |
||
| 59 | fprintf fmt "(@[<v 0>%a %a@])" |
||
| 60 | step_name node |
||
| 61 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine); |
||
| 62 | fprintf fmt "@]@ )@ "; |
||
| 63 | fprintf fmt "(MAIN %a)@]@.))@.@." |
||
| 64 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next ; |
||
| 65 | ) |
||
| 66 | else ( |
||
| 67 | let reset_name, step_name = |
||
| 68 | pp_machine_reset_name, pp_machine_step_name |
||
| 69 | in |
||
| 70 | fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @."; |
||
| 71 | fprintf fmt "(declare-rel INIT_STATE ())@."; |
||
| 72 | fprintf fmt "(rule INIT_STATE)@."; |
||
| 73 | fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>"; |
||
| 74 | fprintf fmt "INIT_STATE@ "; |
||
| 75 | fprintf fmt "(@[<v 0>%a %a@])@ " |
||
| 76 | reset_name node |
||
| 77 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (reset_vars machines machine); |
||
| 78 | fprintf fmt "(@[<v 0>%a %a@])" |
||
| 79 | step_name node |
||
| 80 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine); |
||
| 81 | |||
| 82 | fprintf fmt "@]@ )@ "; |
||
| 83 | fprintf fmt "(MAIN %a)@]@.))@.@." |
||
| 84 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next ; |
||
| 85 | ) |
||
| 86 | in |
||
| 87 | 0dee2bc1 | ploc | |
| 88 | 07ceae4c | ploc | let step_name = |
| 89 | if is_stateless machine then |
||
| 90 | pp_machine_stateless_name |
||
| 91 | else |
||
| 92 | pp_machine_step_name |
||
| 93 | in |
||
| 94 | |||
| 95 | 0dee2bc1 | ploc | fprintf fmt "; Inductive def@."; |
| 96 | (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy; |
||
| 97 | fprintf fmt |
||
| 98 | "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@." |
||
| 99 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_current |
||
| 100 | step_name node |
||
| 101 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine) |
||
| 102 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next |
||
| 103 | |||
| 104 | |||
| 105 | let check_prop machines fmt node machine = |
||
| 106 | let main_output = |
||
| 107 | rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
||
| 108 | in |
||
| 109 | let main_memory_next = |
||
| 110 | (rename_next_list (full_memory_vars machines machine)) @ main_output |
||
| 111 | in |
||
| 112 | fprintf fmt "; Property def@."; |
||
| 113 | fprintf fmt "(declare-rel ERR ())@."; |
||
| 114 | fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@." |
||
| 115 | (pp_conj (pp_horn_var machine)) main_output |
||
| 116 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next |
||
| 117 | ; |
||
| 118 | d2d9d4cb | ploc | if !Options.horn_query then fprintf fmt "(query ERR)@." |
| 119 | 0dee2bc1 | ploc | |
| 120 | |||
| 121 | let cex_computation machines fmt node machine = |
||
| 122 | fprintf fmt "; CounterExample computation for node %s@.@." node; |
||
| 123 | (* We print the types of the cex node "memory tree" TODO: add the output *) |
||
| 124 | let cex_input = |
||
| 125 | rename_machine_list machine.mname.node_id machine.mstep.step_inputs |
||
| 126 | in |
||
| 127 | let cex_input_dummy = |
||
| 128 | rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
|
||
| 129 | in |
||
| 130 | let cex_output = |
||
| 131 | rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
||
| 132 | in |
||
| 133 | let cex_output_dummy = |
||
| 134 | rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
|
||
| 135 | in |
||
| 136 | let cex_memory_next = |
||
| 137 | cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output |
||
| 138 | in |
||
| 139 | let cex_memory_current = |
||
| 140 | cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy |
||
| 141 | in |
||
| 142 | |||
| 143 | (* Special case when the cex node is stateless *) |
||
| 144 | let reset_name, step_name = |
||
| 145 | if is_stateless machine then |
||
| 146 | pp_machine_stateless_name, pp_machine_stateless_name |
||
| 147 | else |
||
| 148 | pp_machine_reset_name, pp_machine_step_name |
||
| 149 | in |
||
| 150 | |||
| 151 | fprintf fmt "(declare-rel CEX (Int %a))@.@." |
||
| 152 | (Utils.fprintf_list ~sep:" " pp_type) |
||
| 153 | (List.map (fun v -> v.var_type) cex_memory_next); |
||
| 154 | |||
| 155 | fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @."; |
||
| 156 | fprintf fmt "(declare-rel INIT_STATE_CEX ())@."; |
||
| 157 | fprintf fmt "(rule INIT_STATE_CEX)@."; |
||
| 158 | fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>"; |
||
| 159 | fprintf fmt "INIT_STATE_CEX@ "; |
||
| 160 | fprintf fmt "(@[<v 0>%a %a@])@ " |
||
| 161 | reset_name node |
||
| 162 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (reset_vars machines machine); |
||
| 163 | fprintf fmt "(@[<v 0>%a %a@])" |
||
| 164 | step_name node |
||
| 165 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine); |
||
| 166 | |||
| 167 | fprintf fmt "@]@ )@ "; |
||
| 168 | fprintf fmt "(CEX 0 %a)@]@.))@.@." |
||
| 169 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next ; |
||
| 170 | |||
| 171 | fprintf fmt "; Inductive def@."; |
||
| 172 | (* Declare dummy inputs. Outputs should have been declared previously with collecting sem *) |
||
| 173 | (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy; |
||
| 174 | fprintf fmt "(declare-var cexcpt Int)@."; |
||
| 175 | fprintf fmt |
||
| 176 | "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@." |
||
| 177 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_current |
||
| 178 | step_name node |
||
| 179 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine) |
||
| 180 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next |
||
| 181 | |||
| 182 | let get_cex machines fmt node machine = |
||
| 183 | let cex_input = |
||
| 184 | rename_machine_list machine.mname.node_id machine.mstep.step_inputs |
||
| 185 | in |
||
| 186 | let cex_output = |
||
| 187 | rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
||
| 188 | in |
||
| 189 | let cex_memory_next = |
||
| 190 | cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output |
||
| 191 | in |
||
| 192 | fprintf fmt "; Property def@."; |
||
| 193 | fprintf fmt "(declare-rel CEXTRACE ())@."; |
||
| 194 | fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@." |
||
| 195 | (pp_conj (pp_horn_var machine)) cex_output |
||
| 196 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next |
||
| 197 | ; |
||
| 198 | fprintf fmt "(query CEXTRACE)@." |
||
| 199 | |||
| 200 | (* Local Variables: *) |
||
| 201 | (* compile-command:"make -C ../.." *) |
||
| 202 | (* End: *) |