Revision 3ca6d126
src/backends/Horn/horn_backend.ml | ||
---|---|---|
564 | 564 |
|
565 | 565 |
let translate fmt basename prog machines = |
566 | 566 |
List.iter (print_machine machines fmt) (List.rev machines); |
567 |
|
|
568 | 567 |
main_print machines fmt |
569 | 568 |
|
570 | 569 |
|
... | ... | |
579 | 578 |
let traces : (ident * expr) list= |
580 | 579 |
let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in |
581 | 580 |
let filtered = |
582 |
List.filter (fun (kwds, _) -> kwds = ["horn_backend";"trace"]) all_annots
|
|
581 |
List.filter (fun (kwds, _) -> kwds = ["traceability"]) all_annots
|
|
583 | 582 |
in |
584 | 583 |
let content = List.map snd filtered in |
585 | 584 |
(* Elements are supposed to be a pair (tuple): variable, expression *) |
... | ... | |
620 | 619 |
List.map (fun (p, v) -> |
621 | 620 |
let machine = match p with | [] -> m | (_,m')::_ -> m' in |
622 | 621 |
let traces = List.assoc machine machines_traces in |
623 |
if List.mem_assoc v.var_id traces then |
|
622 |
if List.mem_assoc v.var_id traces then (
|
|
624 | 623 |
(* We take the expression associated to variable v in the trace info *) |
624 |
(* Format.eprintf "Found variable %a in traces: %a@." pp_var v Printers.pp_expr (List.assoc v.var_id traces); *) |
|
625 | 625 |
p, List.assoc v.var_id traces |
626 |
else |
|
626 |
) |
|
627 |
else ( |
|
627 | 628 |
(* We keep the variable as is: we create an expression v *) |
629 |
(* Format.eprintf "Unable to found variable %a in traces (%a)@." pp_var v (Utils.fprintf_list ~sep:", " Format.pp_print_string) (List.map fst traces); *) |
|
628 | 630 |
p, mkexpr Location.dummy_loc (Expr_ident v.var_id) |
631 |
) |
|
629 | 632 |
|
630 | 633 |
) (compute_mems m) |
631 | 634 |
in |
632 | 635 |
let memories_next = (* We remove the topest pre in each expression *) |
633 | 636 |
List.map |
634 |
(fun (prefix, ee) -> |
|
635 |
match ee.expr_desc with |
|
636 |
| Expr_pre e -> prefix, e |
|
637 |
| _ -> Format.eprintf |
|
638 |
"Mem Failure: (prefix: %a, eexpr: %a)@.@?" |
|
639 |
(Utils.fprintf_list ~sep:"," |
|
640 |
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id )) |
|
641 |
(List.rev prefix) |
|
642 |
Printers.pp_expr ee; |
|
643 |
assert false) |
|
637 |
(fun (prefix, ee) ->
|
|
638 |
match ee.expr_desc with
|
|
639 |
| Expr_pre e -> prefix, e
|
|
640 |
| _ -> Format.eprintf
|
|
641 |
"Mem Failure: (prefix: %a, eexpr: %a)@.@?"
|
|
642 |
(Utils.fprintf_list ~sep:","
|
|
643 |
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
|
|
644 |
(List.rev prefix)
|
|
645 |
Printers.pp_expr ee;
|
|
646 |
assert false)
|
|
644 | 647 |
memories_old |
645 | 648 |
in |
646 | 649 |
|
... | ... | |
680 | 683 |
|
681 | 684 |
|
682 | 685 |
(* Local Variables: *) |
683 |
(* compile-command:"make -C .." *) |
|
686 |
(* compile-command:"make -C ../.." *)
|
|
684 | 687 |
(* End: *) |
src/normalization.ml | ||
---|---|---|
127 | 127 |
(Clocks.clock_list_of_clock expr.expr_clock) in |
128 | 128 |
let new_def = |
129 | 129 |
mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr) |
130 |
in (new_def::defs, new_aliases@vars), replace_expr new_aliases expr |
|
130 |
in |
|
131 |
(* Format.eprintf "Checkign def of alias: %a -> %a@." (fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) new_aliases Printers.pp_expr expr; *) |
|
132 |
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr |
|
131 | 133 |
|
132 | 134 |
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident) |
133 | 135 |
and [opt] is true *) |
... | ... | |
383 | 385 |
with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in |
384 | 386 |
let expr = substitute_expr diff_vars defs eq.eq_rhs in |
385 | 387 |
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in |
386 |
(["horn_backend";"trace"], pair)
|
|
387 |
) [] (*diff_vars*);
|
|
388 |
(["traceability"], pair)
|
|
389 |
) diff_vars;
|
|
388 | 390 |
annot_loc = Location.dummy_loc |
389 | 391 |
} |
390 | 392 |
|
test/test-compile.sh | ||
---|---|---|
135 | 135 |
popd > /dev/null |
136 | 136 |
# Cheching witness |
137 | 137 |
pushd $build > /dev/null |
138 |
$LUSTREC -verbose 0 -horn -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus |
|
138 |
$LUSTREC -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus
|
|
139 | 139 |
popd > /dev/null |
140 | 140 |
z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`" |
141 | 141 |
if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then |
... | ... | |
169 | 169 |
|
170 | 170 |
# Checking horn backend |
171 | 171 |
if [ "$main" != "" ]; then |
172 |
$LUSTREC -horn -d $build -verbose 0 $opts -node $main "$name".lus; |
|
172 |
$LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main "$name".lus;
|
|
173 | 173 |
else |
174 |
$LUSTREC -horn -d $build -verbose 0 $opts "$name".lus |
|
174 |
$LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts "$name".lus
|
|
175 | 175 |
fi |
176 | 176 |
if [ $? -ne 0 ]; then |
177 | 177 |
rlustrec="INVALID"; |
Also available in: Unified diff