Revision 7130028e
Added by Pierre-Loïc Garoche over 10 years ago
| src/horn_backend.ml | ||
|---|---|---|
| 6 | 6 |
|
| 7 | 7 |
let pp_machine_init_name fmt id = fprintf fmt "%s_init" id |
| 8 | 8 |
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id |
| 9 |
let pp_machine_stateless_name fmt id = fprintf fmt "%s" id |
|
| 9 | 10 |
|
| 10 | 11 |
let pp_type fmt t = |
| 11 | 12 |
match (Types.repr t).Types.tdesc with |
| ... | ... | |
| 55 | 56 |
in |
| 56 | 57 |
aux true machine.mname.node_id machine |
| 57 | 58 |
|
| 58 |
let machine_vars machines m = |
|
| 59 |
(rename_machine_list m.mname.node_id m.mstep.step_inputs)@ |
|
| 60 |
(rename_machine_list m.mname.node_id m.mstep.step_outputs)@ |
|
| 61 |
(rename_current_list (full_memory_vars machines m)) @ |
|
| 62 |
(rename_next_list (full_memory_vars machines m)) |
|
| 63 |
|
|
| 59 |
let stateless_vars machines m = |
|
| 60 |
(rename_machine_list m.mname.node_id m.mstep.step_inputs)@ |
|
| 61 |
(rename_machine_list m.mname.node_id m.mstep.step_outputs) |
|
| 62 |
|
|
| 64 | 63 |
let step_vars machines m = |
| 65 |
(rename_machine_list m.mname.node_id m.mstep.step_inputs)@ |
|
| 66 |
(rename_machine_list m.mname.node_id m.mstep.step_outputs)@ |
|
| 64 |
(stateless_vars machines m)@ |
|
| 67 | 65 |
(rename_current_list (full_memory_vars machines m)) @ |
| 68 | 66 |
(rename_next_list (full_memory_vars machines m)) |
| 69 |
|
|
| 67 |
|
|
| 70 | 68 |
let init_vars machines m = |
| 71 |
(rename_machine_list m.mname.node_id m.mstep.step_inputs)@ |
|
| 72 |
(rename_machine_list m.mname.node_id m.mstep.step_outputs)@ |
|
| 73 |
(rename_next_list (full_memory_vars machines m)) |
|
| 74 |
|
|
| 69 |
(stateless_vars machines m) @ (rename_next_list (full_memory_vars machines m)) |
|
| 70 |
|
|
| 75 | 71 |
(********************************************************************************************) |
| 76 | 72 |
(* Instruction Printing functions *) |
| 77 | 73 |
(********************************************************************************************) |
| ... | ... | |
| 142 | 138 |
pp_assign |
| 143 | 139 |
m |
| 144 | 140 |
self |
| 145 |
(pp_horn_var m) |
|
| 146 |
(* (pp_horn_val self (pp_horn_var m) fmt o) *) fmt |
|
| 141 |
(pp_horn_var m) |
|
| 142 |
(* (pp_horn_val self (pp_horn_var m) fmt o) *) |
|
| 143 |
fmt |
|
| 147 | 144 |
o.var_type (LocalVar o) i1 |
| 148 | 145 |
else |
| 149 | 146 |
pp_assign |
| ... | ... | |
| 155 | 152 |
begin |
| 156 | 153 |
let target_machine = List.find (fun m -> m.mname.node_id = name) machines in |
| 157 | 154 |
if init then |
| 158 |
Format.fprintf fmt "(%s_init %a%t%a%t%a)" |
|
| 159 |
(node_name n) |
|
| 155 |
Format.fprintf fmt "(%a %a%t%a%t%a)" |
|
| 156 |
pp_machine_init_name (node_name n) |
|
| 157 |
(* inputs *) |
|
| 160 | 158 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs |
| 161 | 159 |
(Utils.pp_final_char_if_non_empty " " inputs) |
| 160 |
(* outputs *) |
|
| 162 | 161 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs) |
| 163 | 162 |
(Utils.pp_final_char_if_non_empty " " outputs) |
| 163 |
(* memories (next) *) |
|
| 164 | 164 |
(Utils.fprintf_list ~sep:" " pp_var) ( |
| 165 |
rename_machine_list (concat m.mname.node_id i) (rename_next_list (* concat m.mname.node_id i *) (full_memory_vars machines target_machine)) |
|
| 165 |
rename_machine_list |
|
| 166 |
(concat m.mname.node_id i) |
|
| 167 |
(rename_next_list (* concat m.mname.node_id i *) |
|
| 168 |
(full_memory_vars machines target_machine) |
|
| 169 |
) |
|
| 166 | 170 |
) |
| 167 | 171 |
else |
| 168 |
Format.fprintf fmt "(%s_step %a%t%a%t%a)"
|
|
| 169 |
(node_name n) |
|
| 172 |
Format.fprintf fmt "(%a %a%t%a%t%a)"
|
|
| 173 |
pp_machine_step_name (node_name n)
|
|
| 170 | 174 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs |
| 171 | 175 |
(Utils.pp_final_char_if_non_empty " " inputs) |
| 172 | 176 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs) |
| 173 | 177 |
(Utils.pp_final_char_if_non_empty " " outputs) |
| 174 | 178 |
(Utils.fprintf_list ~sep:" " pp_var) ( |
| 175 |
|
|
| 176 |
(rename_machine_list (concat m.mname.node_id i) (rename_current_list (* concat m.mname.node_id i *) (full_memory_vars machines target_machine))) @ |
|
| 177 |
(rename_machine_list (concat m.mname.node_id i) (rename_next_list (* concat m.mname.node_id i *) (full_memory_vars machines target_machine))) |
|
| 179 |
(rename_machine_list |
|
| 180 |
(concat m.mname.node_id i) |
|
| 181 |
(rename_current_list (* concat m.mname.node_id i *) |
|
| 182 |
(full_memory_vars machines target_machine)) |
|
| 183 |
) @ |
|
| 184 |
(rename_machine_list |
|
| 185 |
(concat m.mname.node_id i) |
|
| 186 |
(rename_next_list (* concat m.mname.node_id i *) |
|
| 187 |
(full_memory_vars machines target_machine)) |
|
| 188 |
) |
|
| 178 | 189 |
) |
| 179 | 190 |
|
| 180 |
end
|
|
| 191 |
end |
|
| 181 | 192 |
end |
| 182 | 193 |
with Not_found -> ( (* stateless node instance *) |
| 183 | 194 |
let (n,_) = List.assoc i m.mcalls in |
| 184 |
Format.fprintf fmt "(%s %a%t%a)" |
|
| 185 |
(node_name n) |
|
| 186 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs |
|
| 187 |
(Utils.pp_final_char_if_non_empty " " inputs) |
|
| 188 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) outputs |
|
| 195 |
Format.fprintf fmt "(%s %a%t%a)" |
|
| 196 |
(node_name n) |
|
| 197 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs |
|
| 198 |
(Utils.pp_final_char_if_non_empty " " inputs) |
|
| 199 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs) |
|
| 200 |
(* (Utils.fprintf_list ~sep:" " (pp_horn_var m)) outputs *) |
|
| 189 | 201 |
) |
| 190 | 202 |
|
| 191 | 203 |
let pp_machine_init (m: machine_t) self fmt inst = |
| ... | ... | |
| 217 | 229 |
pp_assign |
| 218 | 230 |
m self (pp_horn_var m) fmt |
| 219 | 231 |
i.var_type (StateVar i) v |
| 220 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i -> |
|
| 221 |
pp_machine_instr machines ~init:init m self fmt (MLocalAssign (i0, Fun (i, vl)))
|
|
| 232 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i -> assert false (* This should not happen anymore *)
|
|
| 233 |
(* pp_machine_instr machines ~init:init m self fmt (MLocalAssign (i0, Fun (i, vl))) *)
|
|
| 222 | 234 |
| MStep (il, i, vl) -> |
| 223 | 235 |
pp_instance_call machines ~init:init m self fmt i vl il |
| 224 | 236 |
| MBranch (g,hl) -> |
| ... | ... | |
| 241 | 253 |
*) |
| 242 | 254 |
let print_machine machines fmt m = |
| 243 | 255 |
let pp_instr init = pp_machine_instr machines ~init:init m in |
| 244 |
if m.mname.node_id = arrow_id then () |
|
| 256 |
if m.mname.node_id = arrow_id then |
|
| 257 |
(* We don't print arrow function *) |
|
| 258 |
() |
|
| 245 | 259 |
else |
| 246 |
( (* We don't print arrow function *) |
|
| 247 |
Format.fprintf fmt "; %s@." m.mname.node_id; |
|
| 260 |
begin |
|
| 261 |
Format.fprintf fmt "; %s@." m.mname.node_id; |
|
| 262 |
|
|
| 248 | 263 |
(* Printing variables *) |
| 249 | 264 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt |
| 250 |
((machine_vars machines m)@(rename_machine_list m.mname.node_id m.mstep.step_locals)); |
|
| 251 |
Format.pp_print_newline fmt (); |
|
| 252 |
(* Declaring predicate *) |
|
| 253 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
| 254 |
pp_machine_init_name m.mname.node_id |
|
| 255 |
(Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (init_vars machines m)); |
|
| 256 |
|
|
| 257 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
| 258 |
pp_machine_step_name m.mname.node_id |
|
| 259 |
(Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (step_vars machines m)); |
|
| 265 |
((step_vars machines m)@ |
|
| 266 |
(rename_machine_list m.mname.node_id m.mstep.step_locals)); |
|
| 260 | 267 |
Format.pp_print_newline fmt (); |
| 261 | 268 |
|
| 262 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%s_init %a)@]@.))@.@." |
|
| 263 |
(Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs |
|
| 264 |
m.mname.node_id |
|
| 265 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m); |
|
| 266 |
|
|
| 267 |
|
|
| 268 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%s_step %a)@]@.))@.@." |
|
| 269 |
(Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs |
|
| 270 |
m.mname.node_id |
|
| 271 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); |
|
| 272 |
|
|
| 273 |
match m.mspec with |
|
| 274 |
None -> () (* No node spec; we do nothing *) |
|
| 275 |
| Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} ->
|
|
| 276 |
( |
|
| 269 |
let stateless = m.minstances = [] && m.mmemory = [] in |
|
| 270 |
|
|
| 271 |
if stateless then |
|
| 272 |
begin |
|
| 273 |
(* Declaring single predicate *) |
|
| 274 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
| 275 |
pp_machine_stateless_name m.mname.node_id |
|
| 276 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
| 277 |
(List.map (fun v -> v.var_type) (stateless_vars machines m)); |
|
| 278 |
|
|
| 279 |
(* Rule for single predicate *) |
|
| 280 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@." |
|
| 281 |
(Utils.fprintf_list ~sep:"@ " |
|
| 282 |
(pp_instr |
|
| 283 |
true (* In this case, the boolean init can be set to true or false. |
|
| 284 |
The node is stateless. *) |
|
| 285 |
m.mname.node_id) |
|
| 286 |
) |
|
| 287 |
m.mstep.step_instrs |
|
| 288 |
pp_machine_stateless_name m.mname.node_id |
|
| 289 |
(Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m); |
|
| 290 |
end |
|
| 291 |
else |
|
| 292 |
begin |
|
| 293 |
(* Declaring predicate *) |
|
| 294 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
| 295 |
pp_machine_init_name m.mname.node_id |
|
| 296 |
(Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (init_vars machines m)); |
|
| 297 |
|
|
| 298 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
| 299 |
pp_machine_step_name m.mname.node_id |
|
| 300 |
(Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (step_vars machines m)); |
|
| 301 |
Format.pp_print_newline fmt (); |
|
| 302 |
|
|
| 303 |
(* Rule for init *) |
|
| 304 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@." |
|
| 305 |
(Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs |
|
| 306 |
pp_machine_init_name m.mname.node_id |
|
| 307 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m); |
|
| 308 |
|
|
| 309 |
(* Rule for step *) |
|
| 310 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@." |
|
| 311 |
(Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs |
|
| 312 |
pp_machine_step_name m.mname.node_id |
|
| 313 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); |
|
| 314 |
|
|
| 315 |
match m.mspec with |
|
| 316 |
None -> () (* No node spec; we do nothing *) |
|
| 317 |
| Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} ->
|
|
| 318 |
( |
|
| 277 | 319 |
(* For the moment, we only deal with simple case: single ensures, no other parameters *) |
| 278 |
() |
|
| 279 |
|
|
| 280 |
) |
|
| 281 |
| _ -> () (* Other cases give nothing *) |
|
| 282 |
) |
|
| 320 |
() |
|
| 321 |
|
|
| 322 |
) |
|
| 323 |
| _ -> () (* Other cases give nothing *) |
|
| 324 |
end |
|
| 325 |
end |
|
| 283 | 326 |
|
| 284 | 327 |
|
| 285 | 328 |
|
| ... | ... | |
| 312 | 355 |
Format.fprintf fmt "; Initial set@."; |
| 313 | 356 |
Format.fprintf fmt "(declare-rel INIT_STATE ())@."; |
| 314 | 357 |
Format.fprintf fmt "(rule INIT_STATE)@."; |
| 315 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%s_init %a@])@]@ )@ (MAIN %a)@]@.))@.@."
|
|
| 316 |
node |
|
| 358 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
|
|
| 359 |
pp_machine_init_name node
|
|
| 317 | 360 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine) |
| 318 | 361 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next ; |
| 319 | 362 |
|
| 320 | 363 |
Format.fprintf fmt "; Inductive def@."; |
| 321 | 364 |
(Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy; |
| 322 | 365 |
Format.fprintf fmt |
| 323 |
"@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%s_step %a@])@]@ )@ (MAIN %a)@]@.))@.@."
|
|
| 366 |
"@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
|
|
| 324 | 367 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_current |
| 325 |
node |
|
| 368 |
pp_machine_step_name node
|
|
| 326 | 369 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine) |
| 327 | 370 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next ; |
| 328 | 371 |
|
Also available in: Unified diff
Solved local var name bugs for stateless nodes as outlined by Teme