Revision 36454535
Added by Pierre-Loïc Garoche over 10 years ago
src/machine_code.ml | ||
---|---|---|
86 | 86 |
step_outputs: var_decl list; |
87 | 87 |
step_locals: var_decl list; |
88 | 88 |
step_instrs: instr_t list; |
89 |
step_asserts: value_t list; |
|
89 | 90 |
} |
90 | 91 |
|
91 | 92 |
type static_call = top_decl * (Dimension.dim_expr list) |
... | ... | |
103 | 104 |
} |
104 | 105 |
|
105 | 106 |
let pp_step fmt s = |
106 |
Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@]@ " |
|
107 |
Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ "
|
|
107 | 108 |
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs |
108 | 109 |
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_outputs |
109 | 110 |
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_locals |
110 | 111 |
(Utils.fprintf_list ~sep:", " (fun fmt (_, c) -> pp_val fmt c)) s.step_checks |
111 | 112 |
(Utils.fprintf_list ~sep:"@ " pp_instr) s.step_instrs |
113 |
(Utils.fprintf_list ~sep:", " pp_val) s.step_asserts |
|
114 |
|
|
112 | 115 |
|
113 | 116 |
let pp_static_call fmt (node, args) = |
114 | 117 |
Format.fprintf fmt "%s<%a>" |
... | ... | |
117 | 120 |
|
118 | 121 |
let pp_machine fmt m = |
119 | 122 |
Format.fprintf fmt |
120 |
"@[<v 2>machine %s@ mem : %a@ instances: %a@ init : %a@ step :@ @[<v 2>%a@]@ @]@ " |
|
123 |
"@[<v 2>machine %s@ mem : %a@ instances: %a@ init : %a@ step :@ @[<v 2>%a@]@ @ spec : @[%t@]@ annot : @[%a@]@]@ "
|
|
121 | 124 |
m.mname.node_id |
122 | 125 |
(Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory |
123 | 126 |
(Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances |
124 | 127 |
(Utils.fprintf_list ~sep:"@ " pp_instr) m.minit |
125 | 128 |
pp_step m.mstep |
129 |
(fun fmt -> match m.mspec with | None -> () | Some spec -> Printers.pp_spec fmt spec) |
|
130 |
(Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot |
|
126 | 131 |
|
127 | 132 |
(* Returns the declared stateless status and the computed one. *) |
128 | 133 |
let get_stateless_status m = |
... | ... | |
199 | 204 |
step_instrs = [conditional (StateVar var_state) |
200 | 205 |
[MStateAssign(var_state, Cst (const_of_bool false)); |
201 | 206 |
MLocalAssign(var_output, LocalVar var_input1)] |
202 |
[MLocalAssign(var_output, LocalVar var_input2)] ] |
|
207 |
[MLocalAssign(var_output, LocalVar var_input2)] ]; |
|
208 |
step_asserts = []; |
|
203 | 209 |
}; |
204 | 210 |
mspec = None; |
205 | 211 |
mannot = []; |
... | ... | |
457 | 463 |
; |
458 | 464 |
|
459 | 465 |
let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l -> ISet.add l) nd.node_locals ISet.empty, [] in |
466 |
(* memories, init instructions, node calls, local variables (including memories), step instrs *) |
|
460 | 467 |
let m, init, j, locals, s = translate_eqs nd init_args (List.rev eqs_rev) in |
461 | 468 |
let mmap = Utils.IMap.fold (fun i n res -> (i, n)::res) j [] in |
462 | 469 |
{ |
... | ... | |
479 | 486 |
| "horn" -> s |
480 | 487 |
| "C" | "java" | _ -> join_guards_list s |
481 | 488 |
); |
489 |
step_asserts = |
|
490 |
let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in |
|
491 |
List.map (translate_expr nd init_args) exprl |
|
492 |
; |
|
482 | 493 |
}; |
483 | 494 |
mspec = nd.node_spec; |
484 | 495 |
mannot = nd.node_annot; |
Also available in: Unified diff
Merged horn_traces branch