Revision 36454535
Added by Pierre-Loïc Garoche over 10 years ago
src/backends/C/c_backend_spec.ml | ||
---|---|---|
31 | 31 |
pp_acsl_type id.var_id fmt id.var_type |
32 | 32 |
|
33 | 33 |
|
34 |
let pp_econst fmt c = |
|
35 |
match c with |
|
36 |
| EConst_int i -> pp_print_int fmt i |
|
37 |
| EConst_real r -> pp_print_string fmt r |
|
38 |
| EConst_float r -> pp_print_float fmt r |
|
39 |
| EConst_bool b -> pp_print_bool fmt b |
|
40 |
| EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"") |
|
41 |
|
|
42 | 34 |
let rec pp_eexpr is_output fmt eexpr = |
43 | 35 |
let pp_eexpr = pp_eexpr is_output in |
44 | 36 |
match eexpr.eexpr_desc with |
45 |
| EExpr_const c -> pp_econst fmt c |
|
37 |
| EExpr_const c -> Printers.pp_econst fmt c
|
|
46 | 38 |
| EExpr_ident id -> |
47 | 39 |
if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id |
48 | 40 |
| EExpr_tuple el -> Utils.fprintf_list ~sep:"," pp_eexpr fmt el |
src/corelang.ml | ||
---|---|---|
495 | 495 |
|
496 | 496 |
let rename_node f_node f_var f_const nd = |
497 | 497 |
let rename_var v = { v with var_id = f_var v.var_id } in |
498 |
let rename_eq eq = { eq with |
|
499 |
eq_lhs = List.map f_var eq.eq_lhs; |
|
500 |
eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs |
|
501 |
} |
|
502 |
in |
|
498 | 503 |
let inputs = List.map rename_var nd.node_inputs in |
499 | 504 |
let outputs = List.map rename_var nd.node_outputs in |
500 | 505 |
let locals = List.map rename_var nd.node_locals in |
... | ... | |
502 | 507 |
let node_checks = List.map (Dimension.expr_replace_var f_var) nd.node_checks in |
503 | 508 |
let node_asserts = List.map |
504 | 509 |
(fun a -> |
505 |
{ a with assert_expr = rename_expr f_node f_var f_const a.assert_expr } |
|
506 |
) nd.node_asserts |
|
507 |
in |
|
508 |
let eqs = List.map |
|
509 |
(fun eq -> { eq with |
|
510 |
eq_lhs = List.map f_var eq.eq_lhs; |
|
511 |
eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs |
|
512 |
} ) nd.node_eqs |
|
510 |
{a with assert_expr = |
|
511 |
let expr = a.assert_expr in |
|
512 |
rename_expr f_node f_var f_const expr}) |
|
513 |
nd.node_asserts |
|
513 | 514 |
in |
515 |
let eqs = List.map rename_eq nd.node_eqs in |
|
514 | 516 |
let spec = |
515 | 517 |
Utils.option_map |
516 | 518 |
(fun s -> rename_node_annot f_node f_var f_const s) |
... | ... | |
643 | 645 |
Basic_library.internal_funs |
644 | 646 |
|
645 | 647 |
|
648 |
|
|
649 |
(* Replace any occurence of a var in vars_to_replace by its associated |
|
650 |
expression in defs until e does not contain any such variables *) |
|
651 |
let rec substitute_expr vars_to_replace defs e = |
|
652 |
let se = substitute_expr vars_to_replace defs in |
|
653 |
{ e with expr_desc = |
|
654 |
let ed = e.expr_desc in |
|
655 |
match ed with |
|
656 |
| Expr_const _ -> ed |
|
657 |
| Expr_array el -> Expr_array (List.map se el) |
|
658 |
| Expr_access (e1, d) -> Expr_access (se e1, d) |
|
659 |
| Expr_power (e1, d) -> Expr_power (se e1, d) |
|
660 |
| Expr_tuple el -> Expr_tuple (List.map se el) |
|
661 |
| Expr_ite (c, t, e) -> Expr_ite (se c, se t, se e) |
|
662 |
| Expr_arrow (e1, e2)-> Expr_arrow (se e1, se e2) |
|
663 |
| Expr_fby (e1, e2) -> Expr_fby (se e1, se e2) |
|
664 |
| Expr_pre e' -> Expr_pre (se e') |
|
665 |
| Expr_when (e', i, l)-> Expr_when (se e', i, l) |
|
666 |
| Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, se h)) hl) |
|
667 |
| Expr_appl (i, e', i') -> Expr_appl (i, se e', i') |
|
668 |
| Expr_ident i -> |
|
669 |
if List.exists (fun v -> v.var_id = i) vars_to_replace then ( |
|
670 |
let eq_i eq = eq.eq_lhs = [i] in |
|
671 |
if List.exists eq_i defs then |
|
672 |
let sub = List.find eq_i defs in |
|
673 |
let sub' = se sub.eq_rhs in |
|
674 |
sub'.expr_desc |
|
675 |
else |
|
676 |
assert false |
|
677 |
) |
|
678 |
else |
|
679 |
ed |
|
680 |
|
|
681 |
} |
|
682 |
(* FAUT IL RETIRER ? |
|
683 |
|
|
684 |
let rec expr_to_eexpr expr = |
|
685 |
{ eexpr_tag = expr.expr_tag; |
|
686 |
eexpr_desc = expr_desc_to_eexpr_desc expr.expr_desc; |
|
687 |
eexpr_type = expr.expr_type; |
|
688 |
eexpr_clock = expr.expr_clock; |
|
689 |
eexpr_loc = expr.expr_loc |
|
690 |
} |
|
691 |
and expr_desc_to_eexpr_desc expr_desc = |
|
692 |
let conv = expr_to_eexpr in |
|
693 |
match expr_desc with |
|
694 |
| Expr_const c -> EExpr_const (match c with |
|
695 |
| Const_int x -> EConst_int x |
|
696 |
| Const_real x -> EConst_real x |
|
697 |
| Const_float x -> EConst_float x |
|
698 |
| Const_tag x -> EConst_tag x |
|
699 |
| _ -> assert false |
|
700 |
|
|
701 |
) |
|
702 |
| Expr_ident i -> EExpr_ident i |
|
703 |
| Expr_tuple el -> EExpr_tuple (List.map conv el) |
|
704 |
|
|
705 |
| Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2) |
|
706 |
| Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2) |
|
707 |
| Expr_pre e' -> EExpr_pre (conv e') |
|
708 |
| Expr_appl (i, e', i') -> |
|
709 |
EExpr_appl |
|
710 |
(i, conv e', match i' with None -> None | Some(id, _) -> Some id) |
|
711 |
|
|
712 |
| Expr_when _ |
|
713 |
| Expr_merge _ -> assert false |
|
714 |
| Expr_array _ |
|
715 |
| Expr_access _ |
|
716 |
| Expr_power _ -> assert false |
|
717 |
| Expr_ite (c, t, e) -> assert false |
|
718 |
| _ -> assert false |
|
719 |
|
|
720 |
*) |
|
646 | 721 |
let rec get_expr_calls nodes e = |
647 | 722 |
get_calls_expr_desc nodes e.expr_desc |
648 | 723 |
and get_calls_expr_desc nodes expr_desc = |
src/corelang.mli | ||
---|---|---|
80 | 80 |
| Expr_phclock of expr * rat |
81 | 81 |
and call_t = ident * expr * (ident * label) option (* The third part denotes the reseting clock label and value *) |
82 | 82 |
|
83 |
type assert_t = |
|
84 |
{ |
|
85 |
assert_expr: expr; |
|
86 |
assert_loc: Location.t |
|
87 |
} |
|
88 |
|
|
89 | 83 |
type eq = |
90 | 84 |
{eq_lhs: ident list; |
91 | 85 |
eq_rhs: expr; |
92 | 86 |
eq_loc: Location.t} |
93 | 87 |
|
88 |
type assert_t = |
|
89 |
{ |
|
90 |
assert_expr: expr * eq list; |
|
91 |
assert_loc: Location.t |
|
92 |
} |
|
93 |
|
|
94 | 94 |
type node_desc = |
95 | 95 |
{node_id: ident; |
96 | 96 |
mutable node_type: Types.type_expr; |
... | ... | |
250 | 250 |
|
251 | 251 |
val update_expr_annot: expr -> LustreSpec.expr_annot -> expr |
252 | 252 |
|
253 |
val substitute_expr: var_decl list -> eq list -> expr -> expr |
|
253 | 254 |
|
254 | 255 |
(** Annotation expression related functions *) |
255 | 256 |
val mkeexpr: Location.t -> expr -> eexpr |
src/horn_backend.ml | ||
---|---|---|
20 | 20 |
| Types.Tarrow _ |
21 | 21 |
| _ -> Format.eprintf "internal error: pp_type %a@." |
22 | 22 |
Types.print_ty t; assert false |
23 |
|
|
24 | 23 |
|
25 | 24 |
let pp_decl_var fmt id = |
26 | 25 |
Format.fprintf fmt "(declare-var %s %a)" |
... | ... | |
30 | 29 |
let pp_var fmt id = Format.pp_print_string fmt id.var_id |
31 | 30 |
|
32 | 31 |
|
32 |
let pp_conj pp fmt l = |
|
33 |
match l with |
|
34 |
[] -> assert false |
|
35 |
| [x] -> pp fmt x |
|
36 |
| _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:" " pp) l |
|
37 |
|
|
38 |
|
|
39 |
|
|
33 | 40 |
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x |
34 | 41 |
let rename f = (fun v -> {v with var_id = f v.var_id } ) |
35 | 42 |
let rename_machine p = rename (fun n -> concat p n) |
... | ... | |
134 | 141 |
let (n,_) = List.assoc i m.minstances in |
135 | 142 |
match node_name n, inputs, outputs with |
136 | 143 |
| "_arrow", [i1; i2], [o] -> begin |
137 |
if init then |
|
138 |
pp_assign |
|
139 |
m |
|
140 |
self |
|
141 |
(pp_horn_var m) |
|
142 |
(* (pp_horn_val self (pp_horn_var m) fmt o) *) |
|
143 |
fmt |
|
144 |
o.var_type (LocalVar o) i1 |
|
145 |
else |
|
146 |
pp_assign |
|
147 |
m self (pp_horn_var m) fmt |
|
148 |
o.var_type (LocalVar o) i2 |
|
149 |
|
|
144 |
if init then |
|
145 |
pp_assign |
|
146 |
m |
|
147 |
self |
|
148 |
(pp_horn_var m) |
|
149 |
fmt |
|
150 |
o.var_type (LocalVar o) i1 |
|
151 |
else |
|
152 |
pp_assign |
|
153 |
m self (pp_horn_var m) fmt |
|
154 |
o.var_type (LocalVar o) i2 |
|
155 |
|
|
150 | 156 |
end |
151 | 157 |
| name, _, _ -> |
152 | 158 |
begin |
153 | 159 |
let target_machine = List.find (fun m -> m.mname.node_id = name) machines in |
154 | 160 |
if init then |
155 |
Format.fprintf fmt "(%a %a%t%a%t%a)" |
|
156 |
pp_machine_init_name (node_name n) |
|
157 |
(* inputs *) |
|
158 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs |
|
159 |
(Utils.pp_final_char_if_non_empty " " inputs) |
|
160 |
(* outputs *) |
|
161 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs) |
|
162 |
(Utils.pp_final_char_if_non_empty " " outputs) |
|
163 |
(* memories (next) *) |
|
164 |
(Utils.fprintf_list ~sep:" " pp_var) ( |
|
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 |
) |
|
170 |
) |
|
161 |
Format.fprintf fmt "(%a %a%t%a%t%a)" |
|
162 |
pp_machine_init_name (node_name n) |
|
163 |
(* inputs *) |
|
164 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
165 |
inputs |
|
166 |
(Utils.pp_final_char_if_non_empty " " inputs) |
|
167 |
(* outputs *) |
|
168 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
169 |
(List.map (fun v -> LocalVar v) outputs) |
|
170 |
(Utils.pp_final_char_if_non_empty " " outputs) |
|
171 |
(* memories (next) *) |
|
172 |
(Utils.fprintf_list ~sep:" " pp_var) ( |
|
173 |
rename_machine_list |
|
174 |
(concat m.mname.node_id i) |
|
175 |
(rename_next_list (full_memory_vars machines target_machine) |
|
176 |
) |
|
177 |
) |
|
171 | 178 |
else |
172 | 179 |
Format.fprintf fmt "(%a %a%t%a%t%a)" |
173 | 180 |
pp_machine_step_name (node_name n) |
174 | 181 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs |
175 | 182 |
(Utils.pp_final_char_if_non_empty " " inputs) |
176 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs) |
|
183 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
184 |
(List.map (fun v -> LocalVar v) outputs) |
|
177 | 185 |
(Utils.pp_final_char_if_non_empty " " outputs) |
178 | 186 |
(Utils.fprintf_list ~sep:" " pp_var) ( |
179 | 187 |
(rename_machine_list |
180 | 188 |
(concat m.mname.node_id i) |
181 |
(rename_current_list (* concat m.mname.node_id i *) |
|
182 |
(full_memory_vars machines target_machine)) |
|
189 |
(rename_current_list (full_memory_vars machines target_machine)) |
|
183 | 190 |
) @ |
184 | 191 |
(rename_machine_list |
185 | 192 |
(concat m.mname.node_id i) |
186 |
(rename_next_list (* concat m.mname.node_id i *) |
|
187 |
(full_memory_vars machines target_machine)) |
|
193 |
(rename_next_list (full_memory_vars machines target_machine)) |
|
188 | 194 |
) |
189 | 195 |
) |
190 | 196 |
|
... | ... | |
194 | 200 |
let (n,_) = List.assoc i m.mcalls in |
195 | 201 |
Format.fprintf fmt "(%s %a%t%a)" |
196 | 202 |
(node_name n) |
197 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs |
|
203 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
204 |
inputs |
|
198 | 205 |
(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 *)
|
|
206 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
207 |
(List.map (fun v -> LocalVar v) outputs)
|
|
201 | 208 |
) |
202 | 209 |
|
203 | 210 |
let pp_machine_init (m: machine_t) self fmt inst = |
... | ... | |
229 | 236 |
pp_assign |
230 | 237 |
m self (pp_horn_var m) fmt |
231 | 238 |
i.var_type (StateVar i) v |
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))) *)
|
|
239 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i -> |
|
240 |
assert false (* This should not happen anymore *)
|
|
234 | 241 |
| MStep (il, i, vl) -> |
235 | 242 |
pp_instance_call machines ~init:init m self fmt i vl il |
236 | 243 |
| MBranch (g,hl) -> |
237 | 244 |
if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false |
238 | 245 |
then (* boolean case, needs special treatment in C because truth value is not unique *) |
239 |
(* may disappear if we optimize code by replacing last branch test with default *)
|
|
246 |
(* may disappear if we optimize code by replacing last branch test with default *)
|
|
240 | 247 |
let tl = try List.assoc tag_true hl with Not_found -> [] in |
241 | 248 |
let el = try List.assoc tag_false hl with Not_found -> [] in |
242 | 249 |
pp_conditional machines ~init:init m self fmt g tl el |
... | ... | |
279 | 286 |
(List.map (fun v -> v.var_type) (stateless_vars machines m)); |
280 | 287 |
|
281 | 288 |
(* Rule for single predicate *) |
282 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@." |
|
283 |
(Utils.fprintf_list ~sep:"@ " |
|
284 |
(pp_instr |
|
285 |
true (* In this case, the boolean init can be set to true or false. |
|
286 |
The node is stateless. *) |
|
287 |
m.mname.node_id) |
|
288 |
) |
|
289 |
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." |
|
290 |
(pp_conj (pp_instr |
|
291 |
true (* In this case, the boolean init can be set to true or false. |
|
292 |
The node is stateless. *) |
|
293 |
m.mname.node_id) |
|
294 |
) |
|
289 | 295 |
m.mstep.step_instrs |
290 | 296 |
pp_machine_stateless_name m.mname.node_id |
291 | 297 |
(Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m); |
... | ... | |
295 | 301 |
(* Declaring predicate *) |
296 | 302 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
297 | 303 |
pp_machine_init_name m.mname.node_id |
298 |
(Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (init_vars machines m)); |
|
304 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
305 |
(List.map (fun v -> v.var_type) (init_vars machines m)); |
|
299 | 306 |
|
300 | 307 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
301 | 308 |
pp_machine_step_name m.mname.node_id |
302 |
(Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (step_vars machines m)); |
|
309 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
310 |
(List.map (fun v -> v.var_type) (step_vars machines m)); |
|
311 |
|
|
303 | 312 |
Format.pp_print_newline fmt (); |
304 | 313 |
|
305 |
(* Rule for init *) |
|
306 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@."
|
|
307 |
(Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs
|
|
314 |
(* Rule for init *)
|
|
315 |
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
|
|
316 |
(pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
|
|
308 | 317 |
pp_machine_init_name m.mname.node_id |
309 | 318 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m); |
310 | 319 |
|
311 |
(* Rule for step *) |
|
312 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@."
|
|
313 |
(Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
|
|
320 |
(* Rule for step *)
|
|
321 |
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
|
|
322 |
(pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs
|
|
314 | 323 |
pp_machine_step_name m.mname.node_id |
315 | 324 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); |
325 |
|
|
326 |
(* Adding assertions *) |
|
327 |
(match m.mstep.step_asserts with |
|
328 |
| [] -> () |
|
329 |
| assertsl -> begin |
|
330 |
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in |
|
331 |
|
|
332 |
Format.fprintf fmt "; Asserts@."; |
|
333 |
Format.fprintf fmt "(assert @[<v 2>%a@]@ )@.@.@." |
|
334 |
(pp_conj pp_val) assertsl; |
|
335 |
|
|
336 |
(** TEME: the following code is the one we described. But it generates a segfault in z3 |
|
337 |
Format.fprintf fmt "; Asserts for init@."; |
|
338 |
Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@.@." |
|
339 |
(Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs |
|
340 |
pp_machine_init_name m.mname.node_id |
|
341 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m) |
|
342 |
(pp_conj pp_val) assertsl; |
|
343 |
|
|
344 |
Format.fprintf fmt "; Asserts for step@."; |
|
345 |
Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@." |
|
346 |
(Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs |
|
347 |
|
|
348 |
pp_machine_step_name m.mname.node_id |
|
349 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m) |
|
350 |
(pp_conj pp_val) assertsl |
|
351 |
*) |
|
352 |
end |
|
353 |
); |
|
354 |
|
|
316 | 355 |
(* |
317 | 356 |
match m.mspec with |
318 | 357 |
None -> () (* No node spec; we do nothing *) |
... | ... | |
329 | 368 |
|
330 | 369 |
|
331 | 370 |
|
332 |
let main_print machines fmt = |
|
333 |
if !Options.main_node <> "" then |
|
334 |
begin |
|
335 |
let node = !Options.main_node in |
|
336 |
let machine = get_machine machines node in |
|
337 |
|
|
371 |
let collecting_semantics machines fmt node machine = |
|
338 | 372 |
Format.fprintf fmt "; Collecting semantics for node %s@.@." node; |
339 | 373 |
(* We print the types of the main node "memory tree" TODO: add the output *) |
340 | 374 |
let main_output = |
... | ... | |
359 | 393 |
else |
360 | 394 |
pp_machine_init_name, pp_machine_step_name |
361 | 395 |
in |
362 |
|
|
396 |
|
|
363 | 397 |
Format.fprintf fmt "(declare-rel MAIN (%a))@." |
364 | 398 |
(Utils.fprintf_list ~sep:" " pp_type) |
365 | 399 |
(List.map (fun v -> v.var_type) main_memory_next); |
... | ... | |
379 | 413 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_current |
380 | 414 |
step_name node |
381 | 415 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine) |
382 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
|
|
416 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next |
|
383 | 417 |
|
384 |
Format.fprintf fmt "; Property def@."; |
|
385 |
Format.fprintf fmt "(declare-rel ERR ())@."; |
|
386 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not (and %a))@ (MAIN %a)@])@ ERR))@." |
|
387 |
(Utils.fprintf_list ~sep:" " pp_var) main_output |
|
388 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next |
|
418 |
let check_prop machines fmt node machine = |
|
419 |
let main_output = |
|
420 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
|
421 |
in |
|
422 |
let main_memory_next = |
|
423 |
(rename_next_list (full_memory_vars machines machine)) @ main_output |
|
424 |
in |
|
425 |
Format.fprintf fmt "; Property def@."; |
|
426 |
Format.fprintf fmt "(declare-rel ERR ())@."; |
|
427 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@." |
|
428 |
(pp_conj pp_var) main_output |
|
429 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next |
|
389 | 430 |
; |
390 |
Format.fprintf fmt "(query ERR)@."; |
|
431 |
if !Options.horn_queries then |
|
432 |
Format.fprintf fmt "(query ERR)@." |
|
391 | 433 |
|
392 |
() |
|
434 |
|
|
435 |
let cex_computation machines fmt node machine = |
|
436 |
Format.fprintf fmt "; CounterExample computation for node %s@.@." node; |
|
437 |
(* We print the types of the cex node "memory tree" TODO: add the output *) |
|
438 |
let cex_input = |
|
439 |
rename_machine_list machine.mname.node_id machine.mstep.step_inputs |
|
440 |
in |
|
441 |
let cex_input_dummy = |
|
442 |
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs |
|
443 |
in |
|
444 |
let cex_output = |
|
445 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
|
446 |
in |
|
447 |
let cex_output_dummy = |
|
448 |
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs |
|
449 |
in |
|
450 |
let cex_memory_next = |
|
451 |
cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output |
|
452 |
in |
|
453 |
let cex_memory_current = |
|
454 |
cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy |
|
455 |
in |
|
456 |
|
|
457 |
(* Special case when the cex node is stateless *) |
|
458 |
let init_name, step_name = |
|
459 |
if is_stateless machine then |
|
460 |
pp_machine_stateless_name, pp_machine_stateless_name |
|
461 |
else |
|
462 |
pp_machine_init_name, pp_machine_step_name |
|
463 |
in |
|
464 |
|
|
465 |
Format.fprintf fmt "(declare-rel CEX (Int %a))@.@." |
|
466 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
467 |
(List.map (fun v -> v.var_type) cex_memory_next); |
|
468 |
|
|
469 |
Format.fprintf fmt "; Initial set@."; |
|
470 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@." |
|
471 |
init_name node |
|
472 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine) |
|
473 |
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next ; |
|
474 |
|
|
475 |
Format.fprintf fmt "; Inductive def@."; |
|
476 |
(* Declare dummy inputs. Outputs should have been declared previously with collecting sem *) |
|
477 |
(Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy; |
|
478 |
Format.fprintf fmt "(declare-var cexcpt Int)@."; |
|
479 |
Format.fprintf fmt |
|
480 |
"@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@." |
|
481 |
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_current |
|
482 |
step_name node |
|
483 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine) |
|
484 |
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next |
|
485 |
|
|
486 |
let get_cex machines fmt node machine = |
|
487 |
let cex_input = |
|
488 |
rename_machine_list machine.mname.node_id machine.mstep.step_inputs |
|
489 |
in |
|
490 |
let cex_output = |
|
491 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
|
492 |
in |
|
493 |
let cex_memory_next = |
|
494 |
cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output |
|
495 |
in |
|
496 |
Format.fprintf fmt "; Property def@."; |
|
497 |
Format.fprintf fmt "(declare-rel CEXTRACE ())@."; |
|
498 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@." |
|
499 |
(pp_conj pp_var) cex_output |
|
500 |
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next |
|
501 |
; |
|
502 |
if !Options.horn_queries then |
|
503 |
Format.fprintf fmt "(query CEXTRACE)@." |
|
504 |
|
|
505 |
|
|
506 |
let main_print machines fmt = |
|
507 |
if !Options.main_node <> "" then |
|
508 |
begin |
|
509 |
let node = !Options.main_node in |
|
510 |
let machine = get_machine machines node in |
|
511 |
|
|
512 |
|
|
513 |
collecting_semantics machines fmt node machine; |
|
514 |
check_prop machines fmt node machine; |
|
515 |
|
|
516 |
cex_computation machines fmt node machine; |
|
517 |
get_cex machines fmt node machine |
|
393 | 518 |
end |
394 | 519 |
|
395 | 520 |
|
... | ... | |
399 | 524 |
main_print machines fmt |
400 | 525 |
|
401 | 526 |
|
527 |
let traces_file fmt basename prog machines = |
|
528 |
Format.fprintf fmt |
|
529 |
"; Horn code traceability generated by %s@.; SVN version number %s@.@." |
|
530 |
(Filename.basename Sys.executable_name) |
|
531 |
Version.number; |
|
532 |
|
|
533 |
(* We extract the annotation dealing with traceability *) |
|
534 |
let machines_traces = List.map (fun m -> |
|
535 |
let traces : (ident * expr) list= |
|
536 |
let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in |
|
537 |
let filtered = |
|
538 |
List.filter (fun (kwds, _) -> kwds = ["horn_backend";"trace"]) all_annots |
|
539 |
in |
|
540 |
let content = List.map snd filtered in |
|
541 |
(* Elements are supposed to be a pair (tuple): variable, expression *) |
|
542 |
List.map (fun ee -> |
|
543 |
match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with |
|
544 |
| [], Expr_tuple [v;e] -> ( |
|
545 |
match v.expr_desc with |
|
546 |
| Expr_ident vid -> vid, e |
|
547 |
| _ -> assert false ) |
|
548 |
| _ -> assert false) |
|
549 |
content |
|
550 |
in |
|
551 |
|
|
552 |
m, traces |
|
553 |
|
|
554 |
) machines |
|
555 |
in |
|
556 |
|
|
557 |
(* Compute memories associated to each machine *) |
|
558 |
let compute_mems m = |
|
559 |
let rec aux fst prefix m = |
|
560 |
(List.map (fun mem -> (prefix, mem)) m.mmemory) @ |
|
561 |
List.fold_left (fun accu (id, (n, _)) -> |
|
562 |
let name = node_name n in |
|
563 |
if name = "_arrow" then accu else |
|
564 |
let machine_n = get_machine machines name in |
|
565 |
( aux false ((id,machine_n)::prefix) machine_n ) |
|
566 |
@ accu |
|
567 |
) [] m.minstances |
|
568 |
in |
|
569 |
aux true [] m |
|
570 |
in |
|
571 |
|
|
572 |
List.iter (fun m -> |
|
573 |
Format.fprintf fmt "; Node %s@." m.mname.node_id; |
|
574 |
|
|
575 |
let memories_old = |
|
576 |
List.map (fun (p, v) -> |
|
577 |
let machine = match p with | [] -> m | (_,m')::_ -> m' in |
|
578 |
let traces = List.assoc machine machines_traces in |
|
579 |
if List.mem_assoc v.var_id traces then |
|
580 |
(* We take the expression associated to variable v in the trace info *) |
|
581 |
p, List.assoc v.var_id traces |
|
582 |
else |
|
583 |
(* We keep the variable as is: we create an expression v *) |
|
584 |
p, mkexpr Location.dummy_loc (Expr_ident v.var_id) |
|
585 |
|
|
586 |
) (compute_mems m) |
|
587 |
in |
|
588 |
let memories_next = (* We remove the topest pre in each expression *) |
|
589 |
List.map |
|
590 |
(fun (prefix, ee) -> |
|
591 |
match ee.expr_desc with |
|
592 |
| Expr_pre e -> prefix, e |
|
593 |
| _ -> Format.eprintf |
|
594 |
"Mem Failure: (prefix: %a, eexpr: %a)@.@?" |
|
595 |
(Utils.fprintf_list ~sep:"," |
|
596 |
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id )) |
|
597 |
(List.rev prefix) |
|
598 |
Printers.pp_expr ee; |
|
599 |
assert false) |
|
600 |
memories_old |
|
601 |
in |
|
602 |
|
|
603 |
let pp_prefix_rev fmt prefix = |
|
604 |
Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix) |
|
605 |
in |
|
606 |
|
|
607 |
Format.fprintf fmt "; Init predicate@."; |
|
608 |
|
|
609 |
Format.fprintf fmt "; horn encoding@."; |
|
610 |
Format.fprintf fmt "(%a %a)@." |
|
611 |
pp_machine_init_name m.mname.node_id |
|
612 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m); |
|
613 |
|
|
614 |
Format.fprintf fmt "; original expressions@."; |
|
615 |
Format.fprintf fmt "(%a %a%t%a)@." |
|
616 |
pp_machine_init_name m.mname.node_id |
|
617 |
(Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs) |
|
618 |
(fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt " ") |
|
619 |
(Utils.fprintf_list ~sep:" " (fun fmt (prefix, ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; |
|
620 |
|
|
621 |
Format.pp_print_newline fmt (); |
|
622 |
Format.fprintf fmt "; Step predicate@."; |
|
623 |
|
|
624 |
Format.fprintf fmt "; horn encoding@."; |
|
625 |
Format.fprintf fmt "(%a %a)@." |
|
626 |
pp_machine_step_name m.mname.node_id |
|
627 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); |
|
628 |
Format.fprintf fmt "; original expressions@."; |
|
629 |
Format.fprintf fmt "(%a %a%t%a)@." |
|
630 |
pp_machine_step_name m.mname.node_id |
|
631 |
(Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs) |
|
632 |
(fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt " ") |
|
633 |
(Utils.fprintf_list ~sep:" " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old@memories_next); |
|
634 |
Format.pp_print_newline fmt (); |
|
635 |
) (List.rev machines); |
|
636 |
|
|
637 |
|
|
402 | 638 |
(* Local Variables: *) |
403 | 639 |
(* compile-command:"make -C .." *) |
404 | 640 |
(* End: *) |
src/inliner.ml | ||
---|---|---|
7 | 7 |
| _ -> false) |
8 | 8 |
|
9 | 9 |
|
10 |
let rename_expr rename expr = expr_replace_var rename expr |
|
11 |
let rename_eq rename eq = |
|
12 |
{ eq with |
|
13 |
eq_lhs = List.map rename eq.eq_lhs; |
|
14 |
eq_rhs = rename_expr rename eq.eq_rhs |
|
15 |
} |
|
16 |
|
|
10 | 17 |
(* |
11 | 18 |
expr, locals', eqs = inline_call id args' reset locals nodes |
12 | 19 |
|
... | ... | |
27 | 34 |
node.node_id uid v; |
28 | 35 |
Format.flush_str_formatter () |
29 | 36 |
in |
30 |
let eqs' = List.map |
|
31 |
(fun eq -> { eq with |
|
32 |
eq_lhs = List.map rename eq.eq_lhs; |
|
33 |
eq_rhs = expr_replace_var rename eq.eq_rhs |
|
34 |
} ) node.node_eqs |
|
37 |
let eqs' = List.map (rename_eq rename) node.node_eqs |
|
35 | 38 |
in |
36 | 39 |
let rename_var v = { v with var_id = rename v.var_id } in |
37 | 40 |
let inputs' = List.map rename_var node.node_inputs in |
... | ... | |
51 | 54 |
loc |
52 | 55 |
(List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) outputs') |
53 | 56 |
in |
54 |
expr , inputs'@outputs'@locals'@locals, assign_inputs::eqs' |
|
57 |
let asserts' = (* We rename variables in assert expressions *) |
|
58 |
List.map |
|
59 |
(fun a -> |
|
60 |
{a with assert_expr = |
|
61 |
let expr = a.assert_expr in |
|
62 |
rename_expr rename expr |
|
63 |
}) |
|
64 |
node.node_asserts |
|
65 |
in |
|
66 |
expr, |
|
67 |
inputs'@outputs'@locals'@locals, |
|
68 |
assign_inputs::eqs', |
|
69 |
asserts' |
|
55 | 70 |
|
56 | 71 |
|
57 | 72 |
|
... | ... | |
65 | 80 |
*) |
66 | 81 |
let rec inline_expr expr locals nodes = |
67 | 82 |
let inline_tuple el = |
68 |
List.fold_right (fun e (el_tail, locals, eqs) -> |
|
69 |
let e', locals', eqs' = inline_expr e locals nodes in |
|
70 |
e'::el_tail, locals', eqs'@eqs |
|
71 |
) el ([], locals, []) |
|
83 |
List.fold_right (fun e (el_tail, locals, eqs, asserts) ->
|
|
84 |
let e', locals', eqs', asserts' = inline_expr e locals nodes in
|
|
85 |
e'::el_tail, locals', eqs'@eqs, asserts@asserts'
|
|
86 |
) el ([], locals, [], [])
|
|
72 | 87 |
in |
73 | 88 |
let inline_pair e1 e2 = |
74 |
let el', l', eqs' = inline_tuple [e1;e2] in |
|
89 |
let el', l', eqs', asserts' = inline_tuple [e1;e2] in
|
|
75 | 90 |
match el' with |
76 |
| [e1'; e2'] -> e1', e2', l', eqs' |
|
91 |
| [e1'; e2'] -> e1', e2', l', eqs', asserts'
|
|
77 | 92 |
| _ -> assert false |
78 | 93 |
in |
79 | 94 |
let inline_triple e1 e2 e3 = |
80 |
let el', l', eqs' = inline_tuple [e1;e2;e3] in |
|
95 |
let el', l', eqs', asserts' = inline_tuple [e1;e2;e3] in
|
|
81 | 96 |
match el' with |
82 |
| [e1'; e2'; e3'] -> e1', e2', e3', l', eqs' |
|
97 |
| [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts'
|
|
83 | 98 |
| _ -> assert false |
84 | 99 |
in |
85 | 100 |
|
86 | 101 |
match expr.expr_desc with |
87 | 102 |
| Expr_appl (id, args, reset) -> |
88 |
let args', locals', eqs' = inline_expr args locals nodes in |
|
103 |
let args', locals', eqs', asserts' = inline_expr args locals nodes in
|
|
89 | 104 |
if List.exists (check_node_name id) nodes then |
90 | 105 |
(* The node should be inlined *) |
91 |
(* let _ = Format.eprintf "Inlining call to %s@." id in
|
|
92 |
*) let node = try List.find (check_node_name id) nodes
|
|
106 |
(* let _ = Format.eprintf "Inlining call to %s@." id in *)
|
|
107 |
let node = try List.find (check_node_name id) nodes |
|
93 | 108 |
with Not_found -> (assert false) in |
94 |
let node = match node.top_decl_desc with Node nd -> nd | _ -> assert false in |
|
109 |
let node = |
|
110 |
match node.top_decl_desc with Node nd -> nd | _ -> assert false in |
|
95 | 111 |
let node = inline_node node nodes in |
96 |
let expr, locals', eqs'' = |
|
112 |
let expr, locals', eqs'', asserts'' =
|
|
97 | 113 |
inline_call expr args' reset locals' node in |
98 |
expr, locals', eqs'@eqs'' |
|
114 |
expr, locals', eqs'@eqs'', asserts'@asserts''
|
|
99 | 115 |
else |
100 | 116 |
(* let _ = Format.eprintf "Not inlining call to %s@." id in *) |
101 |
{ expr with expr_desc = Expr_appl(id, args', reset)}, locals', eqs' |
|
117 |
{ expr with expr_desc = Expr_appl(id, args', reset)}, |
|
118 |
locals', |
|
119 |
eqs', |
|
120 |
asserts' |
|
102 | 121 |
|
103 | 122 |
(* For other cases, we just keep the structure, but convert sub-expressions *) |
104 | 123 |
| Expr_const _ |
105 |
| Expr_ident _ -> expr, locals, [] |
|
124 |
| Expr_ident _ -> expr, locals, [], []
|
|
106 | 125 |
| Expr_tuple el -> |
107 |
let el', l', eqs' = inline_tuple el in |
|
108 |
{ expr with expr_desc = Expr_tuple el' }, l', eqs' |
|
126 |
let el', l', eqs', asserts' = inline_tuple el in
|
|
127 |
{ expr with expr_desc = Expr_tuple el' }, l', eqs', asserts'
|
|
109 | 128 |
| Expr_ite (g, t, e) -> |
110 |
let g', t', e', l', eqs' = inline_triple g t e in |
|
111 |
{ expr with expr_desc = Expr_ite (g', t', e') }, l', eqs' |
|
129 |
let g', t', e', l', eqs', asserts' = inline_triple g t e in
|
|
130 |
{ expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts'
|
|
112 | 131 |
| Expr_arrow (e1, e2) -> |
113 |
let e1', e2', l', eqs' = inline_pair e1 e2 in |
|
114 |
{ expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs' |
|
132 |
let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
|
|
133 |
{ expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts'
|
|
115 | 134 |
| Expr_fby (e1, e2) -> |
116 |
let e1', e2', l', eqs' = inline_pair e1 e2 in |
|
117 |
{ expr with expr_desc = Expr_fby (e1', e2') }, l', eqs' |
|
135 |
let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
|
|
136 |
{ expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts'
|
|
118 | 137 |
| Expr_array el -> |
119 |
let el', l', eqs' = inline_tuple el in |
|
120 |
{ expr with expr_desc = Expr_array el' }, l', eqs' |
|
138 |
let el', l', eqs', asserts' = inline_tuple el in
|
|
139 |
{ expr with expr_desc = Expr_array el' }, l', eqs', asserts'
|
|
121 | 140 |
| Expr_access (e, dim) -> |
122 |
let e', l', eqs' = inline_expr e locals nodes in |
|
123 |
{ expr with expr_desc = Expr_access (e', dim) }, l', eqs' |
|
141 |
let e', l', eqs', asserts' = inline_expr e locals nodes in
|
|
142 |
{ expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts'
|
|
124 | 143 |
| Expr_power (e, dim) -> |
125 |
let e', l', eqs' = inline_expr e locals nodes in |
|
126 |
{ expr with expr_desc = Expr_power (e', dim) }, l', eqs' |
|
144 |
let e', l', eqs', asserts' = inline_expr e locals nodes in
|
|
145 |
{ expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts'
|
|
127 | 146 |
| Expr_pre e -> |
128 |
let e', l', eqs' = inline_expr e locals nodes in |
|
129 |
{ expr with expr_desc = Expr_pre e' }, l', eqs' |
|
147 |
let e', l', eqs', asserts' = inline_expr e locals nodes in
|
|
148 |
{ expr with expr_desc = Expr_pre e' }, l', eqs', asserts'
|
|
130 | 149 |
| Expr_when (e, id, label) -> |
131 |
let e', l', eqs' = inline_expr e locals nodes in |
|
132 |
{ expr with expr_desc = Expr_when (e', id, label) }, l', eqs' |
|
150 |
let e', l', eqs', asserts' = inline_expr e locals nodes in
|
|
151 |
{ expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts'
|
|
133 | 152 |
| Expr_merge (id, branches) -> |
134 |
let el, l', eqs' = inline_tuple (List.map snd branches) in |
|
153 |
let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in
|
|
135 | 154 |
let branches' = List.map2 (fun (label, _) v -> label, v) branches el in |
136 |
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs' |
|
155 |
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts'
|
|
137 | 156 |
and inline_node nd nodes = |
138 |
let new_locals, eqs = |
|
139 |
List.fold_left (fun (locals, eqs) eq -> |
|
140 |
let eq_rhs', locals', new_eqs' = |
|
157 |
let new_locals, eqs, asserts =
|
|
158 |
List.fold_left (fun (locals, eqs, asserts) eq ->
|
|
159 |
let eq_rhs', locals', new_eqs', asserts' =
|
|
141 | 160 |
inline_expr eq.eq_rhs locals nodes |
142 | 161 |
in |
143 |
locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs
|
|
144 |
) (nd.node_locals, []) nd.node_eqs |
|
162 |
locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts
|
|
163 |
) (nd.node_locals, [], nd.node_asserts) nd.node_eqs
|
|
145 | 164 |
in |
146 | 165 |
{ nd with |
147 | 166 |
node_locals = new_locals; |
148 |
node_eqs = eqs |
|
167 |
node_eqs = eqs; |
|
168 |
node_asserts = asserts; |
|
149 | 169 |
} |
150 | 170 |
|
151 | 171 |
let inline_all_calls node nodes = |
src/lustreSpec.ml | ||
---|---|---|
1 | 1 |
open Format |
2 | 2 |
|
3 | 3 |
type ident = Utils.ident |
4 |
type label = Utils.ident |
|
5 | 4 |
type rat = Utils.rat |
6 | 5 |
type tag = Utils.tag |
6 |
type label = Utils.ident |
|
7 | 7 |
|
8 | 8 |
type type_dec = |
9 | 9 |
{ty_dec_desc: type_dec_desc; |
... | ... | |
117 | 117 |
type assert_t = |
118 | 118 |
{ |
119 | 119 |
assert_expr: expr; |
120 |
assert_loc: Location.t |
|
120 |
assert_loc: Location.t;
|
|
121 | 121 |
} |
122 | 122 |
|
123 | 123 |
type node_desc = |
... | ... | |
177 | 177 |
| Already_bound_symbol of ident |
178 | 178 |
|
179 | 179 |
|
180 |
|
|
181 | 180 |
(* Local Variables: *) |
182 | 181 |
(* compile-command:"make -C .." *) |
183 | 182 |
(* End: *) |
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; |
src/main_lustre_compiler.ml | ||
---|---|---|
356 | 356 |
let source_file = destname ^ ".smt2" in (* Could be changed *) |
357 | 357 |
let source_out = open_out source_file in |
358 | 358 |
let fmt = formatter_of_out_channel source_out in |
359 |
Horn_backend.translate fmt basename prog machine_code |
|
359 |
Horn_backend.translate fmt basename prog machine_code; |
|
360 |
(* Tracability file if option is activated *) |
|
361 |
if !Options.horntraces then ( |
|
362 |
let traces_file = destname ^ ".traces" in (* Could be changed *) |
|
363 |
let traces_out = open_out traces_file in |
|
364 |
let fmt = formatter_of_out_channel traces_out in |
|
365 |
Horn_backend.traces_file fmt basename prog machine_code |
|
366 |
) |
|
360 | 367 |
end |
361 | 368 |
| "lustre" -> |
362 | 369 |
begin |
src/normalization.ml | ||
---|---|---|
196 | 196 |
let defvars, norm_elist = |
197 | 197 |
normalize_list alias node offsets (fun alias -> normalize_expr ~alias:alias) defvars elist in |
198 | 198 |
defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist) |
199 |
| Expr_appl (id, args, None) when Basic_library.is_internal_fun id && Types.is_array_type expr.expr_type -> |
|
200 |
let defvars, norm_args = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in |
|
199 |
| Expr_appl (id, args, None) |
|
200 |
when Basic_library.is_internal_fun id |
|
201 |
&& Types.is_array_type expr.expr_type -> |
|
202 |
let defvars, norm_args = |
|
203 |
normalize_list |
|
204 |
alias |
|
205 |
node |
|
206 |
offsets |
|
207 |
(fun _ -> normalize_array_expr ~alias:true) |
|
208 |
defvars |
|
209 |
(expr_list_of_expr args) |
|
210 |
in |
|
201 | 211 |
defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) |
202 | 212 |
| Expr_appl (id, args, None) when Basic_library.is_internal_fun id -> |
203 | 213 |
let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in |
... | ... | |
341 | 351 |
let norm_eq = { eq with eq_rhs = norm_rhs } in |
342 | 352 |
norm_eq::defs', vars' |
343 | 353 |
|
354 |
(** normalize_node node returns a normalized node, |
|
355 |
ie. |
|
356 |
- updated locals |
|
357 |
- new equations |
|
358 |
- |
|
359 |
*) |
|
344 | 360 |
let normalize_node node = |
345 | 361 |
cpt_fresh := 0; |
346 | 362 |
let inputs_outputs = node.node_inputs@node.node_outputs in |
347 | 363 |
let is_local v = |
348 | 364 |
List.for_all ((!=) v) inputs_outputs in |
365 |
let orig_vars = inputs_outputs@node.node_locals in |
|
349 | 366 |
let defs, vars = |
350 |
List.fold_left (normalize_eq node) ([], inputs_outputs@node.node_locals) node.node_eqs in |
|
367 |
List.fold_left (normalize_eq node) ([], orig_vars) node.node_eqs in |
|
368 |
(* Normalize the asserts *) |
|
369 |
let vars, assert_defs, asserts = |
|
370 |
List.fold_left ( |
|
371 |
fun (vars, def_accu, assert_accu) assert_ -> |
|
372 |
let assert_expr = assert_.assert_expr in |
|
373 |
let (defs, vars'), expr = |
|
374 |
normalize_expr |
|
375 |
~alias:false |
|
376 |
node |
|
377 |
[] (* empty offset for arrays *) |
|
378 |
([], vars) (* defvar only contains vars *) |
|
379 |
assert_expr |
|
380 |
in |
|
381 |
vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu |
|
382 |
) (vars, [], []) node.node_asserts in |
|
351 | 383 |
let new_locals = List.filter is_local vars in |
384 |
(* Compute tracebaility info: |
|
385 |
- gather newly bound variables |
|
386 |
- compute the associated expression without aliases |
|
387 |
*) |
|
388 |
let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) new_locals in |
|
389 |
let norm_traceability = { |
|
390 |
annots = |
|
391 |
List.map |
|
392 |
(fun v -> |
|
393 |
let expr = substitute_expr diff_vars defs ( |
|
394 |
let eq = List.find (fun eq -> eq.eq_lhs = [v.var_id]) defs in |
|
395 |
eq.eq_rhs) in |
|
396 |
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in |
|
397 |
["horn_backend";"trace"], pair |
|
398 |
) |
|
399 |
diff_vars ; |
|
400 |
annot_loc = Location.dummy_loc |
|
401 |
} |
|
402 |
|
|
403 |
in |
|
352 | 404 |
let node = |
353 |
{ node with node_locals = new_locals; node_eqs = defs } |
|
405 |
{ node with |
|
406 |
node_locals = new_locals; |
|
407 |
node_eqs = defs @ assert_defs; |
|
408 |
node_asserts = asserts; |
|
409 |
node_annot = norm_traceability::node.node_annot; |
|
410 |
} |
|
354 | 411 |
in ((*Printers.pp_node Format.err_formatter node;*) node) |
355 | 412 |
|
356 | 413 |
let normalize_decl decl = |
src/options.ml | ||
---|---|---|
36 | 36 |
let global_inline = ref false |
37 | 37 |
let witnesses = ref false |
38 | 38 |
let optimization = ref 2 |
39 |
let horntraces = ref false |
|
40 |
let horn_queries = ref false |
|
39 | 41 |
|
40 | 42 |
let options = |
41 | 43 |
[ "-d", Arg.Set_string dest_dir, |
... | ... | |
51 | 53 |
"-c-spec", Arg.Unit (fun () -> spec := "c"), "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend"; |
52 | 54 |
"-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; |
53 | 55 |
"-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C"; |
56 |
"-horn-traces", Arg.Unit (fun () -> output := "horn"; horntraces:=true), "produce traceability file for Horn backend. Enable the horn backend."; |
|
57 |
"-horn-queries", Arg.Set horn_queries, "add the queries instructions at the end of the generated horn files"; |
|
54 | 58 |
"-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations"; |
55 | 59 |
"-inline", Arg.Set global_inline, "inline all node calls (require a main node)"; |
56 | 60 |
"-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation"; |
src/printers.ml | ||
---|---|---|
40 | 40 |
|
41 | 41 |
let pp_eq_lhs = fprintf_list ~sep:", " pp_print_string |
42 | 42 |
|
43 |
let pp_var fmt id = fprintf fmt "%s%s: %a" (if id.var_dec_const then "const " else "") id.var_id Types.print_ty id.var_type |
|
44 |
|
|
45 |
let pp_node_var fmt id = fprintf fmt "%s%s: %a%a" (if id.var_dec_const then "const " else "") id.var_id Types.print_node_ty id.var_type Clocks.print_ck_suffix id.var_clock |
|
46 |
|
|
47 |
let pp_node_args = fprintf_list ~sep:"; " pp_node_var |
|
48 |
|
|
49 |
let pp_quantifiers fmt (q, vars) = |
|
50 |
match q with |
|
51 |
| Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars |
|
52 |
| Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars |
|
53 |
|
|
54 |
(* |
|
55 |
let pp_econst fmt c = |
|
56 |
match c with |
|
57 |
| EConst_int i -> pp_print_int fmt i |
|
58 |
| EConst_real r -> pp_print_string fmt r |
|
59 |
| EConst_float r -> pp_print_float fmt r |
|
60 |
| EConst_tag t -> pp_print_string fmt t |
|
61 |
| EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"") |
|
62 |
|
|
63 |
|
|
64 |
let rec pp_eexpr fmt eexpr = |
|
65 |
match eexpr.eexpr_desc with |
|
66 |
| EExpr_const c -> pp_econst fmt c |
|
67 |
| EExpr_ident id -> pp_print_string fmt id |
|
68 |
| EExpr_tuple el -> fprintf_list ~sep:"," pp_eexpr fmt el |
|
69 |
| EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2 |
|
70 |
| EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2 |
|
71 |
(* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *) |
|
72 |
(* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *) |
|
73 |
| EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e |
|
74 |
| EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id |
|
75 |
| EExpr_merge (id, e1, e2) -> |
|
76 |
fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2 |
|
77 |
| EExpr_appl (id, e, r) -> pp_eapp fmt id e r |
|
78 |
| EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" pp_node_args vars pp_eexpr e |
|
79 |
| EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" pp_node_args vars pp_eexpr e |
|
80 |
|
|
81 |
|
|
82 |
(* | EExpr_whennot _ *) |
|
83 |
(* | EExpr_uclock _ *) |
|
84 |
(* | EExpr_dclock _ *) |
|
85 |
(* | EExpr_phclock _ -> assert false *) |
|
86 |
and pp_eapp fmt id e r = |
|
87 |
match r with |
|
88 |
| None -> |
|
89 |
(match id, e.eexpr_desc with |
|
90 |
| "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2 |
|
91 |
| "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e |
|
92 |
| "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2 |
|
93 |
| "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2 |
|
94 |
| "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2 |
|
95 |
| "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2 |
|
96 |
| "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2 |
|
97 |
| "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2 |
|
98 |
| "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2 |
|
99 |
| "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2 |
|
100 |
| "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2 |
|
101 |
| "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2 |
|
102 |
| ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2 |
|
103 |
| ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2 |
|
104 |
| "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2 |
|
105 |
| "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2 |
|
106 |
| "not", _ -> fprintf fmt "(! %a)" pp_eexpr e |
|
107 |
| "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3 |
|
108 |
| _ -> fprintf fmt "%s (%a)" id pp_eexpr e) |
|
109 |
| Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x |
|
110 |
*) |
|
111 |
|
|
112 |
|
|
43 | 113 |
let rec pp_struct_const_field fmt (label, c) = |
44 | 114 |
fprintf fmt "%a = %a;" pp_print_string label pp_const c |
45 | 115 |
and pp_const fmt c = |
... | ... | |
52 | 122 |
| Const_struct fl -> Format.fprintf fmt "{%a }" (Utils.fprintf_list ~sep:" " pp_struct_const_field) fl |
53 | 123 |
| Const_string s -> pp_print_string fmt ("\"" ^ s ^ "\"") |
54 | 124 |
|
55 |
and pp_var fmt id = fprintf fmt "%s%s: %a" (if id.var_dec_const then "const " else "") id.var_id Types.print_ty id.var_type |
|
56 |
|
|
57 |
and pp_node_var fmt id = fprintf fmt "%s%s: %a%a" (if id.var_dec_const then "const " else "") id.var_id Types.print_node_ty id.var_type Clocks.print_ck_suffix id.var_clock |
|
58 | 125 |
|
59 |
and pp_expr fmt expr = |
|
60 |
match expr.expr_desc with |
|
126 |
let rec pp_expr fmt expr = |
|
127 |
(match expr.expr_annot with |
|
128 |
| None -> fprintf fmt "%t" |
|
129 |
| Some ann -> fprintf fmt "(%a %t)" pp_expr_annot ann) |
|
130 |
(fun fmt -> |
|
131 |
match expr.expr_desc with |
|
61 | 132 |
| Expr_const c -> pp_const fmt c |
62 | 133 |
| Expr_ident id -> Format.fprintf fmt "%s" id |
63 | 134 |
| Expr_array a -> fprintf fmt "[%a]" pp_tuple a |
... | ... | |
72 | 143 |
| Expr_merge (id, hl) -> |
73 | 144 |
fprintf fmt "merge %s %a" id pp_handlers hl |
74 | 145 |
| Expr_appl (id, e, r) -> pp_app fmt id e r |
75 |
|
|
146 |
) |
|
76 | 147 |
and pp_tuple fmt el = |
77 | 148 |
fprintf_list ~sep:"," pp_expr fmt el |
78 | 149 |
|
... | ... | |
107 | 178 |
| _ -> fprintf fmt "%s (%a)" id pp_expr e |
108 | 179 |
) |
109 | 180 |
| Some (x, l) -> fprintf fmt "%s (%a) every %s(%s)" id pp_expr e l x |
181 |
|
|
182 |
|
|
183 |
|
|
184 |
and pp_eexpr fmt e = |
|
185 |
fprintf fmt "%a%t %a" |
|
186 |
(Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers |
|
187 |
(fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";") |
|
188 |
pp_expr e.eexpr_qfexpr |
|
189 |
|
|
190 |
|
|
191 |
and pp_expr_annot fmt expr_ann = |
|
192 |
let pp_annot fmt (kwds, ee) = |
|
193 |
Format.fprintf fmt "(*! %t: %a *)" |
|
194 |
(fun fmt -> match kwds with | [] -> assert false | [x] -> Format.pp_print_string fmt x | _ -> Format.fprintf fmt "/%a/" (fprintf_list ~sep:"/" Format.pp_print_string) kwds) |
|
195 |
pp_eexpr ee |
|
196 |
in |
|
197 |
fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots |
|
198 |
|
|
110 | 199 |
|
111 | 200 |
let pp_node_eq fmt eq = |
112 | 201 |
fprintf fmt "%a = %a;" |
... | ... | |
115 | 204 |
|
116 | 205 |
let pp_node_eqs = fprintf_list ~sep:"@ " pp_node_eq |
117 | 206 |
|
118 |
let pp_node_args = fprintf_list ~sep:"; " pp_node_var |
|
119 | 207 |
|
120 | 208 |
let pp_var_type_dec fmt ty = |
121 | 209 |
let rec pp_var_struct_type_field fmt (label, tdesc) = |
... | ... | |
146 | 234 |
(* ) *) |
147 | 235 |
|
148 | 236 |
|
149 |
|
|
150 |
let pp_quantifiers fmt (q, vars) = |
|
151 |
match q with |
|
152 |
| Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars |
|
153 |
| Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars |
|
154 |
|
|
155 |
let pp_eexpr fmt e = |
|
156 |
fprintf fmt "%a%t %a" |
|
157 |
(Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers |
|
158 |
(fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";") |
|
159 |
pp_expr e.eexpr_qfexpr |
|
160 |
|
|
161 | 237 |
let pp_spec fmt spec = |
162 | 238 |
fprintf fmt "@[<hov 2>(*@@ "; |
163 | 239 |
fprintf_list ~sep:"@;@@ " (fun fmt r -> fprintf fmt "requires %a;" pp_eexpr r) fmt spec.requires; |
... | ... | |
171 | 247 |
fprintf fmt "@]*)"; |
172 | 248 |
() |
173 | 249 |
|
250 |
|
|
251 |
let pp_asserts fmt asserts = |
|
252 |
match asserts with |
|
253 |
| _::_ -> ( |
|
254 |
fprintf fmt "(* Asserts definitions *)@ "; |
|
255 |
fprintf_list ~sep:"@ " (fun fmt assert_ -> |
|
256 |
let expr = assert_.assert_expr in |
|
257 |
fprintf fmt "assert %a;" pp_expr expr |
|
258 |
) fmt asserts |
|
259 |
) |
|
260 |
| _ -> () |
|
261 |
|
|
174 | 262 |
let pp_node fmt nd = |
175 |
fprintf fmt "@[<v 0>%a%t%s %s (%a) returns (%a)@.%a%alet@.@[<h 2> @ @[<v>%a@]@ @]@.tel@]@." |
|
263 |
fprintf fmt "@[<v 0>%a%t%s %s (%a) returns (%a)@.%a%alet@.@[<h 2> @ @[<v>%a@ %a@ %a@]@ @]@.tel@]@."
|
|
176 | 264 |
(fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec |
177 | 265 |
(fun fmt -> match nd.node_spec with None -> () | Some _ -> Format.fprintf fmt "@.") |
178 | 266 |
(if nd.node_dec_stateless then "function" else "node") |
... | ... | |
193 | 281 |
(fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d)) |
194 | 282 |
checks |
195 | 283 |
) nd.node_checks |
284 |
(fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot |
|
196 | 285 |
pp_node_eqs nd.node_eqs |
286 |
pp_asserts nd.node_asserts |
|
197 | 287 |
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*) |
198 | 288 |
|
199 | 289 |
let pp_imported_node fmt ind = |
src/typing.ml | ||
---|---|---|
647 | 647 |
let undefined_vars = |
648 | 648 |
List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs |
649 | 649 |
in |
650 |
(* Typing asserts *) |
|
651 |
List.iter (fun assert_ -> |
|
652 |
let assert_expr = assert_.assert_expr in |
|
653 |
type_subtyping_arg (new_env, vd_env) is_main false assert_expr Type_predef.type_bool |
|
654 |
) nd.node_asserts; |
|
655 |
|
|
650 | 656 |
(* check that table is empty *) |
651 | 657 |
if (not (IMap.is_empty undefined_vars)) then |
652 | 658 |
raise (Error (loc, Undefined_var undefined_vars)); |
test/test-compile.sh | ||
---|---|---|
151 | 151 |
else |
152 | 152 |
$LUSTREC -horn -d $build -verbose 0 $opts "$name".lus |
153 | 153 |
fi |
154 |
if [ $? -ne 0 ]; then |
|
155 |
rlustrec="INVALID"; |
|
156 |
else |
|
157 |
rlustrec="VALID" |
|
158 |
fi |
|
154 | 159 |
# echo "z3 $build/$name".smt2 |
155 | 160 |
# TODO: This part of the script has to be optimized |
156 | 161 |
z3 -T:10 "$build/$name".smt2 | grep unsat > /dev/null |
... | ... | |
160 | 165 |
rhorn="VALID" |
161 | 166 |
fi |
162 | 167 |
if [ $verbose -gt 0 ]; then |
163 |
echo "horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report; |
|
168 |
echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
|
|
164 | 169 |
else |
165 |
echo "horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN" |
|
170 |
echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
|
|
166 | 171 |
fi |
167 | 172 |
popd > /dev/null |
168 | 173 |
done < $file_list |
Also available in: Unified diff
Merged horn_traces branch