Revision a0c92fa8
src/compiler_stages.ml | ||
---|---|---|
123 | 123 |
|
124 | 124 |
|
125 | 125 |
(* Generating a .lusi header file only *) |
126 |
if !Options.lusi then |
|
126 |
if !Options.lusi || !Options.print_nodes then
|
|
127 | 127 |
(* We stop here the processing and produce the current prog. It will be |
128 | 128 |
exported as a lusi *) |
129 | 129 |
raise (StopPhase1 prog); |
src/main_lustre_compiler.ml | ||
---|---|---|
47 | 47 |
|
48 | 48 |
(* Parsing source *) |
49 | 49 |
let prog = parse source_name extension in |
50 |
|
|
50 |
|
|
51 | 51 |
let prog = |
52 | 52 |
if !Options.mpfr && |
53 | 53 |
extension = ".lus" (* trying to avoid the injection of the module for lusi files *) |
... | ... | |
71 | 71 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@."); |
72 | 72 |
exit 0 |
73 | 73 |
end |
74 |
else if !Options.print_nodes then ( |
|
75 |
Format.printf "%a@.@?" Printers.pp_node_list prog; |
|
76 |
exit 0 |
|
77 |
) |
|
74 | 78 |
else |
75 | 79 |
assert false |
76 | 80 |
) |
src/main_lustre_testgen.ml | ||
---|---|---|
46 | 46 |
(* Parsing source *) |
47 | 47 |
let prog = parse source_name extension in |
48 | 48 |
let params = Backends.get_normalization_params () in |
49 |
let prog, dependencies = Compiler_stages.stage1 params prog dirname basename extension in |
|
50 |
|
|
49 |
let prog, dependencies = |
|
50 |
try |
|
51 |
Compiler_stages.stage1 params prog dirname basename extension |
|
52 |
with Compiler_stages.StopPhase1 prog -> ( |
|
53 |
if !Options.print_nodes then ( |
|
54 |
Format.printf "%a@.@?" Printers.pp_node_list prog; |
|
55 |
exit 0 |
|
56 |
) |
|
57 |
else |
|
58 |
assert false |
|
59 |
) |
|
60 |
in |
|
61 |
|
|
51 | 62 |
(* Two cases |
52 | 63 |
- generation of coverage conditions |
53 | 64 |
- generation of mutants: a number of mutated lustre files |
src/main_lustre_verifier.ml | ||
---|---|---|
65 | 65 |
decr Options.verbose_level; |
66 | 66 |
Compiler_stages.stage1 params prog dirname basename extension |
67 | 67 |
with Compiler_stages.StopPhase1 prog -> ( |
68 |
if !Options.print_nodes then ( |
|
69 |
Format.printf "%a@.@?" Printers.pp_node_list prog; |
|
70 |
exit 0 |
|
71 |
) |
|
72 |
else |
|
68 | 73 |
assert false |
69 | 74 |
) |
70 | 75 |
in |
src/options.ml | ||
---|---|---|
29 | 29 |
let witnesses = ref false |
30 | 30 |
let optimization = ref 2 |
31 | 31 |
let lusi = ref false |
32 |
let print_nodes = ref false |
|
32 | 33 |
let print_reuse = ref false |
33 | 34 |
let const_unfold = ref false |
34 | 35 |
let mpfr = ref false |
src/options_management.ml | ||
---|---|---|
92 | 92 |
"-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node"; |
93 | 93 |
"-print-types", Arg.Set print_types, "prints node types"; |
94 | 94 |
"-print-clocks", Arg.Set print_clocks, "prints node clocks"; |
95 |
"-print-nodes", Arg.Set print_nodes, "prints node list"; |
|
95 | 96 |
"-algebraic-loop-solve", Arg.Set solve_al, "try to solve algebraic loops"; |
96 | 97 |
"-algebraic-loop-max", Arg.Set_int al_nb_max, "try to solve \x1b[4mnb\x1b[0m number of algebraic loops <default: 15>"; |
97 | 98 |
"-kind2", Arg.Set kind2_print, "active kind2 output"; |
src/printers.ml | ||
---|---|---|
601 | 601 |
| Index i -> fprintf fmt "[%a]" Dimension.pp_dimension i |
602 | 602 |
| Field f -> fprintf fmt ".%s" f |
603 | 603 |
|
604 |
let pp_node_list fmt prog = |
|
605 |
Format.fprintf fmt "@[<h 2>%a@]" |
|
606 |
(fprintf_list |
|
607 |
~sep:"@ " |
|
608 |
(fun fmt decl -> |
|
609 |
match decl.top_decl_desc with |
|
610 |
| Node nd -> Format.fprintf fmt "%s" nd.node_id |
|
611 |
| _ -> () |
|
612 |
)) |
|
613 |
prog |
|
614 |
|
|
604 | 615 |
(* Local Variables: *) |
605 | 616 |
(* compile-command:"make -C .." *) |
606 | 617 |
(* End: *) |
src/tools/seal/seal_export.ml | ||
---|---|---|
62 | 62 |
match g_opt with |
63 | 63 |
| None -> ( |
64 | 64 |
Format.eprintf "SEAL issue: process_sw with %a" |
65 |
pp_sys sw
|
|
65 |
(pp_sys Printers.pp_expr) sw
|
|
66 | 66 |
; |
67 | 67 |
assert false (* How could this happen anyway ? *) |
68 | 68 |
) |
... | ... | |
117 | 117 |
in |
118 | 118 |
new_nd, orig_nd |
119 | 119 |
|
120 |
|
|
121 |
let funsw_to_lustre m update_out = |
|
122 |
let orig_nd = m.mname in |
|
123 |
let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in |
|
124 |
let output_eq = |
|
125 |
let e_update_out = process_sw copy_nd.node_outputs (fun x -> x) update_out in |
|
126 |
[ |
|
127 |
Eq |
|
128 |
{ eq_loc = Location.dummy_loc; |
|
129 |
eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs; |
|
130 |
eq_rhs = e_update_out |
|
131 |
}; |
|
132 |
] |
|
133 |
in |
|
134 |
let new_nd = |
|
135 |
{ copy_nd with |
|
136 |
node_id = copy_nd.node_id ^ "_seal"; |
|
137 |
node_locals = []; |
|
138 |
node_stmts = output_eq; |
|
139 |
} |
|
140 |
in |
|
141 |
new_nd, orig_nd |
|
142 |
|
|
120 | 143 |
|
121 |
let to_lustre basename prog m sw_init sw_step init_out update_out = |
|
144 |
|
|
145 |
let to_lustre basename prog new_node orig_node = |
|
122 | 146 |
let loc = Location.dummy_loc in |
123 |
let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in |
|
124 | 147 |
Global.type_env := Typing.type_node !Global.type_env new_node loc; |
125 | 148 |
Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc new_node; |
126 | 149 |
|
... | ... | |
139 | 162 |
let output_file_verif = !Options.dest_dir ^ "/" ^ basename ^ "_seal_verif.lus" in |
140 | 163 |
let out_verif = open_out output_file_verif in |
141 | 164 |
let fmt_verif = Format.formatter_of_out_channel out_verif in |
142 |
let check_nd = Lustre_utils.check_eq new_node orig_nd in
|
|
165 |
let check_nd = Lustre_utils.check_eq new_node orig_node in
|
|
143 | 166 |
let check_top = |
144 | 167 |
Corelang.mktop_decl Location.dummy_loc output_file_verif false (Node check_nd) |
145 | 168 |
in |
146 |
Format.fprintf fmt_verif "%a@." Printers.pp_prog (prog@[new_top;check_top]); |
|
169 |
Format.fprintf fmt_verif "%a@." Printers.pp_prog (prog@[new_top;check_top]) |
|
170 |
|
|
171 |
let node_to_lustre basename prog m sw_init sw_step init_out update_out = |
|
172 |
let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in |
|
173 |
to_lustre basename prog new_node orig_nd |
|
174 |
|
|
175 |
let fun_to_lustre basename prog m update_out = |
|
176 |
let new_node, orig_nd = funsw_to_lustre m update_out in |
|
177 |
to_lustre basename prog new_node orig_nd |
|
178 |
|
src/tools/seal/seal_extract.ml | ||
---|---|---|
91 | 91 |
* let comp_zexpr ze (_, ze') = Z3.Expr.equal ze ze' in *) |
92 | 92 |
|
93 | 93 |
let rec e2ze e = |
94 |
(* Format.eprintf "e2ze %a: %a@." Printers.pp_expr e Types.print_ty e.expr_type; *) |
|
94 | 95 |
if mem_expr e then ( |
95 | 96 |
get_zexpr e |
96 | 97 |
) |
... | ... | |
121 | 122 |
) |
122 | 123 |
) |
123 | 124 |
| Expr_appl (id,args, None) (* no reset *) -> |
124 |
let z3e = Zustre_common.horn_basic_app id e2ze (Corelang.expr_list_of_expr args) in |
|
125 |
let el = Corelang.expr_list_of_expr args in |
|
126 |
|
|
127 |
let eltyp = List.map (fun e -> e.expr_type) el in |
|
128 |
let elv = List.map e2ze el in |
|
129 |
let z3e = Zustre_common.horn_basic_app id elv (eltyp, e.expr_type) in |
|
125 | 130 |
add_expr e z3e; |
126 | 131 |
z3e |
127 | 132 |
| Expr_tuple [e] -> |
... | ... | |
597 | 602 |
expr.expr_loc |
598 | 603 |
(Expr_appl(id, deelem e, None)) |
599 | 604 |
in |
605 |
let new_e = { new_e with expr_type = expr.expr_type; expr_clock = expr.expr_clock } in |
|
600 | 606 |
guards, |
601 | 607 |
Expr (Corelang.partial_eval new_e) |
602 | 608 |
) args |
... | ... | |
905 | 911 |
"@[<v 2>===> @[%t@ @]@]@ @]@ " |
906 | 912 |
(fun fmt -> List.iter (fun (gl,up) -> |
907 | 913 |
Format.fprintf fmt "[@[%a@]] -> (%a)@ " |
908 |
(pp_guard_list Printers.pp_expr) gl pp_up up) res);
|
|
914 |
(pp_guard_list Printers.pp_expr) gl (pp_up Printers.pp_expr) up) res);
|
|
909 | 915 |
|
910 | 916 |
)); |
911 | 917 |
res |
912 | 918 |
|
913 | 919 |
|
914 |
|
|
915 |
(* Take a normalized node and extract a list of switches: (cond, |
|
916 |
update) meaning "if cond then update" where update shall define all |
|
917 |
node memories. Everything as to be expressed over inputs or memories, intermediate variables are removed through inlining *) |
|
918 |
let node_as_switched_sys consts (mems:var_decl list) nd = |
|
919 |
Z3.Params.update_param_value !ctx "timeout" "10000"; |
|
920 |
let build_environement consts (mems:var_decl list) nd = |
|
921 |
|
|
922 |
Z3.Params.update_param_value !ctx "timeout" "10000"; |
|
920 | 923 |
|
921 | 924 |
|
922 | 925 |
(* rescheduling node: has been scheduled already, no need to protect |
... | ... | |
1018 | 1021 |
(pp_guard_expr pp_elem)) mdefs |
1019 | 1022 |
)) |
1020 | 1023 |
mem_defs); |
1021 |
(* Format.eprintf "Split init@."; *) |
|
1022 |
let init_defs, update_defs = |
|
1023 |
split_init mem_defs |
|
1024 |
mem_defs, output_defs |
|
1025 |
|
|
1026 |
|
|
1027 |
(* Iter through the elements and gather them by updates *) |
|
1028 |
let merge_updates sys = |
|
1029 |
(* The map will associate to each update up the pair (set, set |
|
1030 |
list) where set is the share guards and set list a list of |
|
1031 |
disjunctive guards. Each set represents a conjunction of |
|
1032 |
expressions. *) |
|
1033 |
|
|
1034 |
(* We perform multiple pass to avoid errors *) |
|
1035 |
let map = |
|
1036 |
List.fold_left (fun map (gl,up) -> |
|
1037 |
(* creating a new set to describe gl *) |
|
1038 |
let new_set = |
|
1039 |
List.fold_left |
|
1040 |
(fun set g -> Guards.add g set) |
|
1041 |
Guards.empty |
|
1042 |
gl |
|
1043 |
in |
|
1044 |
(* updating the map with up -> new_set *) |
|
1045 |
if UpMap.mem up map then |
|
1046 |
let guard_set = UpMap.find up map in |
|
1047 |
UpMap.add up (new_set::guard_set) map |
|
1048 |
else |
|
1049 |
UpMap.add up [new_set] map |
|
1050 |
) UpMap.empty sys |
|
1024 | 1051 |
in |
1025 |
let init_out, update_out = |
|
1026 |
split_init output_defs |
|
1052 |
|
|
1053 |
(* Processing the set of guards leading to the same update: return |
|
1054 |
conj, disj with conf is a set of guards, and disj a DNF, ie a |
|
1055 |
list of set of guards *) |
|
1056 |
let map = |
|
1057 |
UpMap.map ( |
|
1058 |
fun guards -> |
|
1059 |
match guards with |
|
1060 |
| [] -> Guards.empty, [] (* Nothing *) |
|
1061 |
| [s]-> s, [] (* basic case *) |
|
1062 |
| hd::tl -> |
|
1063 |
let shared = List.fold_left (fun shared s -> Guards.inter shared s) hd tl in |
|
1064 |
let remaining = List.map (fun s -> Guards.diff s shared) guards in |
|
1065 |
(* If one of them is empty, we can remove the others, otherwise keep them *) |
|
1066 |
if List.exists Guards.is_empty remaining then |
|
1067 |
shared, [] |
|
1068 |
else |
|
1069 |
shared, remaining |
|
1070 |
) map |
|
1027 | 1071 |
in |
1028 |
report ~level:3 |
|
1029 |
(fun fmt -> |
|
1030 |
Format.fprintf fmt |
|
1031 |
"@[<v 0>Init:@ %a@]@." |
|
1032 |
(Utils.fprintf_list ~sep:"@ " |
|
1033 |
(fun fmt (m,mdefs) -> |
|
1034 |
Format.fprintf fmt |
|
1035 |
"%s -> @[<v 0>[%a@] ]@ " |
|
1036 |
m |
|
1037 |
(Utils.fprintf_list ~sep:"@ " |
|
1038 |
(pp_guard_expr pp_elem)) mdefs |
|
1039 |
)) |
|
1040 |
init_defs); |
|
1041 |
report ~level:3 |
|
1042 |
(fun fmt -> |
|
1043 |
Format.fprintf fmt |
|
1044 |
"@[<v 0>Step:@ %a@]@." |
|
1045 |
(Utils.fprintf_list ~sep:"@ " |
|
1046 |
(fun fmt (m,mdefs) -> |
|
1047 |
Format.fprintf fmt |
|
1048 |
"%s -> @[<v 0>[%a@] ]@ " |
|
1049 |
m |
|
1050 |
(Utils.fprintf_list ~sep:"@ " |
|
1051 |
(pp_guard_expr pp_elem)) mdefs |
|
1052 |
)) |
|
1053 |
update_defs); |
|
1054 |
(* Format.eprintf "Build init@."; *) |
|
1055 |
|
|
1056 |
report ~level:1 (fun fmt -> Format.fprintf fmt "init/step as a switched system ...@."); |
|
1057 |
let sw_init= |
|
1058 |
build_switch_sys init_defs [] |
|
1072 |
let rec mk_binop op l = match l with |
|
1073 |
[] -> assert false |
|
1074 |
| [e] -> e |
|
1075 |
| hd::tl -> Corelang.mkpredef_call hd.expr_loc op [hd; mk_binop op tl] |
|
1059 | 1076 |
in |
1060 |
(* Format.eprintf "Build step@."; *) |
|
1061 |
let sw_sys = |
|
1062 |
build_switch_sys update_defs [] |
|
1077 |
let gl_as_expr gl = |
|
1078 |
let gl = Guards.elements gl in |
|
1079 |
let export (e,b) = if b then e else Corelang.push_negations ~neg:true e in |
|
1080 |
match gl with |
|
1081 |
[] -> [] |
|
1082 |
| [e] -> [export e] |
|
1083 |
| _ -> |
|
1084 |
[mk_binop "&&" |
|
1085 |
(List.map export gl)] |
|
1063 | 1086 |
in |
1064 |
report ~level:1 (fun fmt -> Format.fprintf fmt "init/step as a switched system ... done@."); |
|
1087 |
let rec clean_disj disj = |
|
1088 |
match disj with |
|
1089 |
| [] -> [] |
|
1090 |
| [_] -> assert false (* A disjunction with a single case can be ignored *) |
|
1091 |
| _::_::_ -> ( |
|
1092 |
(* First basic version: producing a DNF One can later, (1) |
|
1093 |
simplify it with z3, or (2) build the compact tree with |
|
1094 |
maximum shared subexpression (and simplify it with z3) *) |
|
1095 |
let elems = List.fold_left (fun accu gl -> (gl_as_expr gl) @ accu) [] disj in |
|
1096 |
let or_expr = mk_binop "||" elems in |
|
1097 |
[or_expr] |
|
1065 | 1098 |
|
1066 |
report ~level:1 (fun fmt -> Format.fprintf fmt "output function as a switched system ...@."); |
|
1067 |
let init_out = |
|
1068 |
build_switch_sys init_out [] |
|
1069 |
in |
|
1070 |
(* report ~level:1 (fun fmt -> Format.fprintf fmt "Build step out@."); *) |
|
1071 | 1099 |
|
1072 |
let update_out = |
|
1073 |
build_switch_sys update_out [] |
|
1100 |
(* TODO disj*) |
|
1101 |
(* get the item that occurs in most case *) |
|
1102 |
(* List.fold_left (fun accu s -> |
|
1103 |
* List.fold_left (fun accu (e,b) -> |
|
1104 |
* if List.mem_assoc (e.expr_tag, b) |
|
1105 |
* ) accu (Guards.elements s) |
|
1106 |
* ) [] disj *) |
|
1107 |
|
|
1108 |
) |
|
1074 | 1109 |
in |
1075 |
report ~level:1 (fun fmt -> Format.fprintf fmt "output function as a switched system ... done@."); |
|
1110 |
if !seal_debug then Format.eprintf "Map: %i elements@ " (UpMap.cardinal map); |
|
1111 |
UpMap.fold (fun up (common, disj) accu -> |
|
1112 |
if !seal_debug then |
|
1113 |
report ~level:6 (fun fmt -> Format.fprintf fmt |
|
1114 |
"Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@." |
|
1115 |
Guards.pp_short common |
|
1116 |
(fprintf_list ~sep:";@ " Guards.pp_long) disj |
|
1117 |
UpMap.pp up); |
|
1118 |
let disj = clean_disj disj in |
|
1119 |
let guard_expr = (gl_as_expr common)@disj in |
|
1120 |
|
|
1121 |
((match guard_expr with |
|
1122 |
| [] -> None |
|
1123 |
| _ -> Some (mk_binop "&&" guard_expr)), up)::accu |
|
1124 |
) map [] |
|
1125 |
|
|
1126 |
|
|
1127 |
|
|
1076 | 1128 |
|
1077 |
report ~level:1 (fun fmt -> Format.fprintf fmt "removing dead branches and merging remaining ...@."); |
|
1129 |
(* Take a normalized node and extract a list of switches: (cond, |
|
1130 |
update) meaning "if cond then update" where update shall define all |
|
1131 |
node memories. Everything as to be expressed over inputs or |
|
1132 |
memories, intermediate variables are removed through inlining *) |
|
1133 |
let node_as_switched_sys consts (mems:var_decl list) nd = |
|
1134 |
let mem_defs, output_defs = build_environement consts mems nd in |
|
1135 |
|
|
1136 |
let init_defs, update_defs = split_init mem_defs in |
|
1137 |
let init_out, update_out = split_init output_defs in |
|
1138 |
|
|
1139 |
report ~level:3 (fun fmt -> Format.fprintf fmt "@[<v 0>Init:@ %a@ Step:@ %a@]@." |
|
1140 |
(pp_assign_map pp_elem) init_defs |
|
1141 |
(pp_assign_map pp_elem) update_defs); |
|
1142 |
|
|
1143 |
|
|
1144 |
report ~level:1 (fun fmt -> Format.fprintf fmt |
|
1145 |
"init/step as a switched system ...@."); |
|
1146 |
let sw_init= build_switch_sys init_defs [] in |
|
1147 |
let sw_sys = build_switch_sys update_defs [] in |
|
1148 |
report ~level:1 (fun fmt -> Format.fprintf fmt |
|
1149 |
"init/step as a switched system ... done@."); |
|
1150 |
|
|
1151 |
|
|
1152 |
report ~level:1 (fun fmt -> Format.fprintf fmt |
|
1153 |
"output function as a switched system ...@."); |
|
1154 |
let init_out = build_switch_sys init_out [] in |
|
1155 |
let update_out = build_switch_sys update_out [] in |
|
1156 |
|
|
1157 |
report ~level:1 (fun fmt -> Format.fprintf fmt |
|
1158 |
"output function as a switched system ... done@."); |
|
1159 |
|
|
1160 |
report ~level:1 (fun fmt -> Format.fprintf fmt |
|
1161 |
"removing dead branches and merging remaining ...@."); |
|
1078 | 1162 |
|
1079 | 1163 |
let sw_init = clean_sys sw_init in |
1080 | 1164 |
let sw_sys = clean_sys sw_sys in |
1081 | 1165 |
let init_out = clean_sys init_out in |
1082 | 1166 |
let update_out = clean_sys update_out in |
1083 |
report ~level:1 (fun fmt -> Format.fprintf fmt "removing dead branches and merging remaining ... done@."); |
|
1167 |
|
|
1168 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_init:@."); |
|
1169 |
let sw_init = merge_updates sw_init in |
|
1170 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_sys:@."); |
|
1171 |
let sw_sys = merge_updates sw_sys in |
|
1172 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Process init_out:@."); |
|
1173 |
let init_out = merge_updates init_out in |
|
1174 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Process update_out:@."); |
|
1175 |
let update_out = merge_updates update_out in |
|
1176 |
report ~level:1 (fun fmt -> |
|
1177 |
Format.fprintf fmt "removing dead branches and merging remaining ... done@."); |
|
1178 |
|
|
1179 |
sw_init , sw_sys, init_out, update_out |
|
1180 |
|
|
1181 |
|
|
1182 |
let fun_as_switched_sys consts nd = |
|
1183 |
let _, update_out = build_environement consts [] nd in |
|
1184 |
|
|
1185 |
report ~level:1 (fun fmt -> Format.fprintf fmt |
|
1186 |
"output function as a switched system ...@."); |
|
1187 |
let update_out = build_switch_sys update_out [] in |
|
1188 |
report ~level:1 (fun fmt -> Format.fprintf fmt |
|
1189 |
"output function as a switched system ... done@."); |
|
1190 |
|
|
1191 |
report ~level:1 (fun fmt -> Format.fprintf fmt |
|
1192 |
"removing dead branches and merging remaining ...@."); |
|
1193 |
let update_out = clean_sys update_out in |
|
1194 |
let update_out = merge_updates update_out in |
|
1195 |
report ~level:1 (fun fmt -> |
|
1196 |
Format.fprintf fmt "removing dead branches and merging remaining ... done@."); |
|
1197 |
|
|
1198 |
update_out |
|
1199 |
|
|
1200 |
|
|
1201 |
|
|
1202 |
|
|
1203 |
|
|
1204 |
(* Some code that was used to check for duplicate entries in guards. |
|
1205 |
|
|
1084 | 1206 |
|
1085 | 1207 |
(* Some additional checks *) |
1086 | 1208 |
|
... | ... | |
1156 | 1278 |
end; |
1157 | 1279 |
|
1158 | 1280 |
|
1159 |
(* Iter through the elements and gather them by updates *) |
|
1160 |
let process sys = |
|
1161 |
(* The map will associate to each update up the pair (set, set |
|
1162 |
list) where set is the share guards and set list a list of |
|
1163 |
disjunctive guards. Each set represents a conjunction of |
|
1164 |
expressions. *) |
|
1165 |
report ~level:3 (fun fmt -> Format.fprintf fmt "%t@." |
|
1166 |
(fun fmt -> List.iter (fun (gl,up) -> |
|
1167 |
Format.fprintf fmt "[@[%a@]] -> (%a)@ " |
|
1168 |
(pp_guard_list Printers.pp_expr) gl pp_up up) sw_init)); |
|
1169 |
|
|
1170 |
(* We perform multiple pass to avoid errors *) |
|
1171 |
let map = |
|
1172 |
List.fold_left (fun map (gl,up) -> |
|
1173 |
(* creating a new set to describe gl *) |
|
1174 |
let new_set = |
|
1175 |
List.fold_left |
|
1176 |
(fun set g -> Guards.add g set) |
|
1177 |
Guards.empty |
|
1178 |
gl |
|
1179 |
in |
|
1180 |
(* updating the map with up -> new_set *) |
|
1181 |
if UpMap.mem up map then |
|
1182 |
let guard_set = UpMap.find up map in |
|
1183 |
UpMap.add up (new_set::guard_set) map |
|
1184 |
else |
|
1185 |
UpMap.add up [new_set] map |
|
1186 |
) UpMap.empty sys |
|
1187 |
in |
|
1188 |
(* Processing the set of guards leading to the same update: return |
|
1189 |
conj, disj with conf is a set of guards, and disj a DNF, ie a |
|
1190 |
list of set of guards *) |
|
1191 |
let map = |
|
1192 |
UpMap.map ( |
|
1193 |
fun guards -> |
|
1194 |
match guards with |
|
1195 |
| [] -> Guards.empty, [] (* Nothing *) |
|
1196 |
| [s]-> s, [] (* basic case *) |
|
1197 |
| hd::tl -> |
|
1198 |
let shared = List.fold_left (fun shared s -> Guards.inter shared s) hd tl in |
|
1199 |
let remaining = List.map (fun s -> Guards.diff s shared) guards in |
|
1200 |
(* If one of them is empty, we can remove the others, otherwise keep them *) |
|
1201 |
if List.exists Guards.is_empty remaining then |
|
1202 |
shared, [] |
|
1203 |
else |
|
1204 |
shared, remaining |
|
1205 |
) map |
|
1206 |
in |
|
1207 |
let rec mk_binop op l = match l with |
|
1208 |
[] -> assert false |
|
1209 |
| [e] -> e |
|
1210 |
| hd::tl -> Corelang.mkpredef_call hd.expr_loc op [hd; mk_binop op tl] |
|
1211 |
in |
|
1212 |
let gl_as_expr gl = |
|
1213 |
let gl = Guards.elements gl in |
|
1214 |
let export (e,b) = if b then e else Corelang.push_negations ~neg:true e in |
|
1215 |
match gl with |
|
1216 |
[] -> [] |
|
1217 |
| [e] -> [export e] |
|
1218 |
| _ -> |
|
1219 |
[mk_binop "&&" |
|
1220 |
(List.map export gl)] |
|
1221 |
in |
|
1222 |
let rec clean_disj disj = |
|
1223 |
match disj with |
|
1224 |
| [] -> [] |
|
1225 |
| [_] -> assert false (* A disjunction was a single case can be ignored *) |
|
1226 |
| _::_::_ -> ( |
|
1227 |
(* First basic version: producing a DNF One can later, (1) |
|
1228 |
simplify it with z3, or (2) build the compact tree with |
|
1229 |
maximum shared subexpression (and simplify it with z3) *) |
|
1230 |
let elems = List.fold_left (fun accu gl -> (gl_as_expr gl) @ accu) [] disj in |
|
1231 |
let or_expr = mk_binop "||" elems in |
|
1232 |
[or_expr] |
|
1233 |
|
|
1234 |
|
|
1235 |
(* TODO disj*) |
|
1236 |
(* get the item that occurs in most case *) |
|
1237 |
(* List.fold_left (fun accu s -> |
|
1238 |
* List.fold_left (fun accu (e,b) -> |
|
1239 |
* if List.mem_assoc (e.expr_tag, b) |
|
1240 |
* ) accu (Guards.elements s) |
|
1241 |
* ) [] disj *) |
|
1242 |
|
|
1243 |
) |
|
1244 |
in |
|
1245 |
if !seal_debug then Format.eprintf "Map: %i elements@ " (UpMap.cardinal map); |
|
1246 |
UpMap.fold (fun up (common, disj) accu -> |
|
1247 |
if !seal_debug then |
|
1248 |
report ~level:6 (fun fmt -> Format.fprintf fmt |
|
1249 |
"Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@." |
|
1250 |
Guards.pp_short common |
|
1251 |
(fprintf_list ~sep:";@ " Guards.pp_long) disj |
|
1252 |
UpMap.pp up); |
|
1253 |
let disj = clean_disj disj in |
|
1254 |
let guard_expr = (gl_as_expr common)@disj in |
|
1255 |
|
|
1256 |
((match guard_expr with |
|
1257 |
| [] -> None |
|
1258 |
| _ -> Some (mk_binop "&&" guard_expr)), up)::accu |
|
1259 |
) map [] |
|
1260 |
|
|
1261 |
in |
|
1262 |
|
|
1263 |
|
|
1264 |
|
|
1265 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_init:@."); |
|
1266 |
let sw_init = process sw_init in |
|
1267 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_sys:@."); |
|
1268 |
let sw_sys = process sw_sys in |
|
1269 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Process init_out:@."); |
|
1270 |
let init_out = process init_out in |
|
1271 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Process update_out:@."); |
|
1272 |
let update_out = process update_out in |
|
1273 |
sw_init , sw_sys, init_out, update_out |
|
1281 |
*) |
src/tools/seal/seal_utils.ml | ||
---|---|---|
28 | 28 |
(fun fmt (e,b) -> if b then pp_elem fmt e else Format.fprintf fmt "not(%a)" pp_elem e)) fmt gl |
29 | 29 |
|
30 | 30 |
let pp_guard_expr pp_elem fmt (gl,e) = |
31 |
Format.fprintf fmt "@[%a@] -> @[<hov 2>%a@]"
|
|
31 |
Format.fprintf fmt "@[<v 2>@[%a@] ->@ @[<hov 2>%a@]@]"
|
|
32 | 32 |
(pp_guard_list pp_elem) gl |
33 | 33 |
pp_elem e |
34 | 34 |
|
35 | 35 |
let pp_mdefs pp_elem fmt gel = fprintf_list ~sep:"@ " (pp_guard_expr pp_elem) fmt gel |
36 | 36 |
|
37 |
|
|
37 |
let pp_assign_map pp_elem = |
|
38 |
fprintf_list ~sep:"@ " |
|
39 |
(fun fmt (m, mdefs) -> |
|
40 |
Format.fprintf fmt |
|
41 |
"%s -> @[<v 0>[%a@] ]@ " |
|
42 |
m |
|
43 |
(pp_mdefs pp_elem) mdefs |
|
44 |
) |
|
38 | 45 |
|
39 | 46 |
let deelem e = match e with |
40 | 47 |
Expr e -> e |
... | ... | |
53 | 60 |
fprintf_list ~sep:", " (fun fmt (e,b) -> Format.fprintf fmt "%s%a" (if b then "" else "NOT ") pp_expr e) |
54 | 61 |
|
55 | 62 |
let pp_gl_short = pp_gl (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag) |
56 |
let pp_up fmt up = List.iter (fun (id,e) -> Format.fprintf fmt "%s->%i; " id e.expr_tag) up |
|
57 | 63 |
|
58 |
let pp_sys fmt sw = List.iter (fun (gl,up) -> |
|
59 |
match gl with |
|
60 |
| None -> |
|
61 |
pp_up fmt up |
|
62 |
| Some gl -> |
|
63 |
Format.fprintf fmt "[@[%a@]] -> (%a)@ " |
|
64 |
Printers.pp_expr gl pp_up up) sw |
|
64 |
let pp_up pp_elem fmt up = |
|
65 |
fprintf_list ~sep:"@ " |
|
66 |
(fun fmt (id,e) -> Format.fprintf fmt "%s == %a;@ " id pp_elem e) |
|
67 |
fmt |
|
68 |
up |
|
69 |
|
|
70 |
let pp_sys pp_elem fmt sw = |
|
71 |
fprintf_list ~sep:"@ " |
|
72 |
(fun fmt (gl,up) -> |
|
73 |
match gl with |
|
74 |
| None -> |
|
75 |
(pp_up pp_elem) fmt up |
|
76 |
| Some gl -> |
|
77 |
Format.fprintf fmt "@[<v 2>[@[%a@]]:@ %a@]" |
|
78 |
Printers.pp_expr gl (pp_up pp_elem) up) |
|
79 |
fmt |
|
80 |
sw |
|
81 |
|
|
65 | 82 |
let pp_all_defs = |
66 | 83 |
(Utils.fprintf_list ~sep:",@ " |
67 | 84 |
(fun fmt (id, gel) -> Format.fprintf fmt "%s -> [@[<v 0>%a]@]" |
... | ... | |
76 | 93 |
let proj l = List.map (fun (s,e) -> s, e.expr_tag) l in |
77 | 94 |
compare (proj l1) (proj l2) |
78 | 95 |
end) |
79 |
let pp = pp_up |
|
96 |
let pp = pp_up Printers.pp_expr
|
|
80 | 97 |
end |
81 | 98 |
|
82 | 99 |
module Guards = struct |
src/tools/seal/seal_verifier.ml | ||
---|---|---|
1 |
open Seal_slice |
|
2 |
open Seal_extract |
|
3 |
open Seal_utils |
|
4 |
|
|
5 |
let active = ref false |
|
6 |
let seal_export = ref None |
|
7 |
|
|
8 |
let set_export s = match s with |
|
9 |
| "lustre" | "lus" | "m" | "matlab" -> seal_export := Some s |
|
10 |
| _ -> (Format.eprintf "Unrecognized seal export: %s@.@?" s; exit 1) |
|
11 | 1 |
(* TODO |
12 | 2 |
|
13 | 3 |
- build the output function: for the moment we slice the node with |
... | ... | |
35 | 25 |
the property to prove |
36 | 26 |
|
37 | 27 |
*) |
28 |
|
|
29 |
|
|
30 |
open Seal_slice |
|
31 |
open Seal_extract |
|
32 |
open Seal_utils |
|
33 |
|
|
34 |
let active = ref false |
|
35 |
let seal_export = ref None |
|
36 |
|
|
37 |
let set_export s = match s with |
|
38 |
| "lustre" | "lus" | "m" | "matlab" -> seal_export := Some s |
|
39 |
| _ -> (Format.eprintf "Unrecognized seal export: %s@.@?" s; exit 1) |
|
38 | 40 |
|
39 | 41 |
(* Select the appropriate node, should have been inlined already and |
40 | 42 |
extract update/output functions. *) |
... | ... | |
64 | 66 |
in |
65 | 67 |
let m = Machine_code_common.get_machine machines node_name in |
66 | 68 |
let nd = m.mname in |
67 |
(* Format.eprintf "Node %a@." Printers.pp_node nd; *) |
|
68 | 69 |
let mems = m.mmemory in |
70 |
|
|
69 | 71 |
report ~level:1 (fun fmt -> Format.fprintf fmt "Node %s compiled: %i memories@." nd.node_id (List.length mems)); |
70 |
(* Format.eprintf "Mems: %a@." (Utils.fprintf_list ~sep:"; " Printers.pp_var) mems; *) |
|
72 |
|
|
73 |
(* Slicing node *) |
|
71 | 74 |
let msch = Utils.desome m.msch in |
72 |
(* Format.eprintf "graph: %a@." Causality.pp_dep_graph deps; *) |
|
73 | 75 |
let sliced_nd = slice_node (mems@nd.node_outputs) msch nd in |
74 |
if false then Format.eprintf "Sliced Node %a@." Printers.pp_node sliced_nd; |
|
75 | 76 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@."); |
77 |
report ~level:10 (fun fmt -> Format.fprintf fmt "Sliced Node %a@." Printers.pp_node sliced_nd); |
|
76 | 78 |
|
77 | 79 |
let consts = Corelang.(List.map const_of_top (get_consts prog)) in |
78 |
let sw_init, sw_sys, init_out, update_out = node_as_switched_sys consts mems sliced_nd in |
|
79 |
let pp_res pp_expr =
|
|
80 |
(Utils.fprintf_list ~sep:"@ "
|
|
81 |
(fun fmt (g, up) ->
|
|
82 |
Format.fprintf fmt "@[<v 2>[%t]:@ %a@]" |
|
83 |
(fun fmt -> match g with None -> () | Some g -> pp_expr fmt g)
|
|
84 |
|
|
85 |
(* (Utils.fprintf_list ~sep:"; "
|
|
86 |
* (fun fmt (e,b) ->
|
|
87 |
* if b then pp_expr fmt e
|
|
88 |
* else Format.fprintf fmt "not(%a)"
|
|
89 |
* pp_expr e)) gel *)
|
|
90 |
(Utils.fprintf_list ~sep:";@ "
|
|
91 |
(fun fmt (id, e) -> |
|
92 |
Format.fprintf fmt "%s = @[<hov 0>%a@]"
|
|
93 |
id
|
|
94 |
pp_expr e)) up
|
|
95 |
))
|
|
96 |
in
|
|
97 |
report ~level:1 (
|
|
98 |
fun fmt -> Format.fprintf fmt
|
|
99 |
"%i memories, %i init, %i step switch cases@."
|
|
100 |
(List.length mems)
|
|
101 |
(List.length sw_init)
|
|
102 |
(List.length sw_sys)
|
|
103 |
|
|
104 |
);
|
|
105 |
report ~level:1 (fun fmt -> |
|
106 |
(*let pp_res = pp_res (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag) in*)
|
|
107 |
let pp_res = pp_res Printers.pp_expr in
|
|
108 |
Format.fprintf fmt "DynSys:@ @[<v 0>@[<v 3>Init:@ %a@]@ "
|
|
109 |
pp_res sw_init;
|
|
110 |
Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@."
|
|
111 |
pp_res sw_sys
|
|
112 |
);
|
|
113 |
|
|
114 |
|
|
115 |
|
|
116 |
report ~level:1 (fun fmt -> |
|
117 |
(*let pp_res = pp_res (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag) in*)
|
|
118 |
let pp_res = pp_res Printers.pp_expr in
|
|
119 |
Format.fprintf fmt "Output (%i init, %i step switch cases):@ @[<v 0>@[<v 3>Init:@ %a@]@ "
|
|
120 |
(List.length init_out)
|
|
121 |
(List.length update_out)
|
|
122 |
pp_res init_out;
|
|
123 |
Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@."
|
|
124 |
pp_res update_out |
|
125 |
);
|
|
126 |
let _ = match !seal_export with
|
|
127 |
| Some "lustre" | Some "lus" ->
|
|
128 |
Seal_export.to_lustre basename prog m sw_init sw_sys init_out update_out
|
|
129 |
| Some "matlab" | Some "m" -> assert false (* TODO *)
|
|
130 |
| Some _ -> assert false
|
|
131 |
| None -> ()
|
|
132 |
in
|
|
133 |
()
|
|
80 |
|
|
81 |
let pp_sys = pp_sys Printers.pp_expr in
|
|
82 |
if List.length mems = 0 then
|
|
83 |
begin (* A stateless node = a function ! *)
|
|
84 |
|
|
85 |
let update_out = fun_as_switched_sys consts sliced_nd in
|
|
86 |
|
|
87 |
report ~level:1 (fun fmt ->
|
|
88 |
Format.fprintf fmt
|
|
89 |
"Output (%i step switch cases):@ @[<v 0>%a@]@."
|
|
90 |
(List.length update_out)
|
|
91 |
pp_sys update_out
|
|
92 |
);
|
|
93 |
|
|
94 |
let _ = match !seal_export with
|
|
95 |
| Some "lustre" | Some "lus" ->
|
|
96 |
Seal_export.fun_to_lustre basename prog m update_out
|
|
97 |
| Some "matlab" | Some "m" -> assert false (* TODO *)
|
|
98 |
| Some _ -> assert false
|
|
99 |
| None -> ()
|
|
100 |
in
|
|
101 |
()
|
|
102 |
end
|
|
103 |
else
|
|
104 |
begin (* A stateful node *)
|
|
105 |
|
|
106 |
let sw_init, sw_sys, init_out, update_out = node_as_switched_sys consts mems sliced_nd in
|
|
107 |
|
|
108 |
report ~level:1 (fun fmt ->
|
|
109 |
Format.fprintf fmt
|
|
110 |
"DynSys: (%i memories, %i init, %i step switch cases)@ @[<v 0>@[<v 3>Init:@ %a@]@ @[<v 3>Step:@ %a@]@]@."
|
|
111 |
(List.length mems)
|
|
112 |
(List.length sw_init)
|
|
113 |
(List.length sw_sys)
|
|
114 |
pp_sys sw_init
|
|
115 |
pp_sys sw_sys |
|
116 |
); |
|
117 |
|
|
118 |
report ~level:1 (fun fmt ->
|
|
119 |
Format.fprintf fmt
|
|
120 |
"Output (%i init, %i step switch cases):@ @[<v 0>@[<v 3>Init:@ %a@]@ @[<v 3>Step:@ %a@]@]@."
|
|
121 |
(List.length init_out)
|
|
122 |
(List.length update_out)
|
|
123 |
pp_sys init_out
|
|
124 |
pp_sys update_out
|
|
125 |
);
|
|
126 |
|
|
127 |
let _ = match !seal_export with
|
|
128 |
| Some "lustre" | Some "lus" ->
|
|
129 |
Seal_export.node_to_lustre basename prog m sw_init sw_sys init_out update_out
|
|
130 |
| Some "matlab" | Some "m" -> assert false (* TODO *)
|
|
131 |
| Some _ -> assert false
|
|
132 |
| None -> ()
|
|
133 |
in
|
|
134 |
()
|
|
135 |
end
|
|
134 | 136 |
|
135 | 137 |
module Verifier = |
136 | 138 |
(struct |
... | ... | |
151 | 153 |
|
152 | 154 |
let is_active () = !active |
153 | 155 |
let run = seal_run |
154 |
|
|
155 |
|
|
156 |
|
|
157 |
|
|
156 | 158 |
end: VerifierType.S) |
157 | 159 |
|
src/tools/zustre/zustre_common.ml | ||
---|---|---|
5 | 5 |
(* open Horn_backend_common |
6 | 6 |
* open Horn_backend *) |
7 | 7 |
open Zustre_data |
8 |
|
|
8 |
|
|
9 |
let report = Log.report ~plugin:"z3 interface" |
|
10 |
|
|
9 | 11 |
module HBC = Horn_backend_common |
10 | 12 |
let node_name = HBC.node_name |
11 | 13 |
|
... | ... | |
111 | 113 |
let get_fdecl id = |
112 | 114 |
try |
113 | 115 |
Hashtbl.find decls id |
114 |
with Not_found -> (Format.eprintf "Unable to find func_decl %s@.@?" id; raise Not_found)
|
|
116 |
with Not_found -> (report ~level:3 (fun fmt -> Format.fprintf fmt "Unable to find func_decl %s@.@?" id); raise Not_found)
|
|
115 | 117 |
|
116 | 118 |
let pp_fdecls fmt = |
117 | 119 |
Format.fprintf fmt "Registered fdecls: @[%a@]@ " |
... | ... | |
124 | 126 |
register_fdecl id.var_id fdecl; |
125 | 127 |
fdecl |
126 | 128 |
|
129 |
(* Declaring the function used in expr *) |
|
130 |
let decl_fun op args typ = |
|
131 |
let args = List.map type_to_sort args in |
|
132 |
let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx op args (type_to_sort typ) in |
|
133 |
register_fdecl op fdecl; |
|
134 |
fdecl |
|
135 |
|
|
127 | 136 |
let idx_sort = int_sort |
128 | 137 |
let uid_sort = Z3.Z3List.mk_sort !ctx (Z3.Symbol.mk_string !ctx "uid_list") int_sort |
129 | 138 |
let uid_conc = |
... | ... | |
242 | 251 |
|
243 | 252 |
(* Conversion of basic library functions *) |
244 | 253 |
|
245 |
let horn_basic_app i val_to_expr vl =
|
|
254 |
let horn_basic_app i vl (vltyp, typ) =
|
|
246 | 255 |
match i, vl with |
247 |
| "ite", [v1; v2; v3] -> |
|
248 |
Z3.Boolean.mk_ite |
|
249 |
!ctx |
|
250 |
(val_to_expr v1) |
|
251 |
(val_to_expr v2) |
|
252 |
(val_to_expr v3) |
|
253 |
|
|
254 |
| "uminus", [v] -> |
|
255 |
Z3.Arithmetic.mk_unary_minus |
|
256 |
!ctx |
|
257 |
(val_to_expr v) |
|
256 |
| "ite", [v1; v2; v3] -> Z3.Boolean.mk_ite !ctx v1 v2 v3 |
|
257 |
| "uminus", [v] -> Z3.Arithmetic.mk_unary_minus |
|
258 |
!ctx v |
|
258 | 259 |
| "not", [v] -> |
259 | 260 |
Z3.Boolean.mk_not |
260 |
!ctx |
|
261 |
(val_to_expr v) |
|
261 |
!ctx v |
|
262 | 262 |
| "=", [v1; v2] -> |
263 | 263 |
Z3.Boolean.mk_eq |
264 |
!ctx |
|
265 |
(val_to_expr v1) |
|
266 |
(val_to_expr v2) |
|
264 |
!ctx v1 v2 |
|
267 | 265 |
| "&&", [v1; v2] -> |
268 | 266 |
Z3.Boolean.mk_and |
269 | 267 |
!ctx |
270 |
[val_to_expr v1; |
|
271 |
val_to_expr v2] |
|
268 |
[v1; v2] |
|
272 | 269 |
| "||", [v1; v2] -> |
273 | 270 |
Z3.Boolean.mk_or |
274 | 271 |
!ctx |
275 |
[val_to_expr v1;
|
|
276 |
val_to_expr v2]
|
|
272 |
[v1; |
|
273 |
v2] |
|
277 | 274 |
|
278 | 275 |
| "impl", [v1; v2] -> |
279 | 276 |
Z3.Boolean.mk_implies |
280 |
!ctx |
|
281 |
(val_to_expr v1) |
|
282 |
(val_to_expr v2) |
|
277 |
!ctx v1 v2 |
|
283 | 278 |
| "mod", [v1; v2] -> |
284 | 279 |
Z3.Arithmetic.Integer.mk_mod |
285 |
!ctx |
|
286 |
(val_to_expr v1) |
|
287 |
(val_to_expr v2) |
|
280 |
!ctx v1 v2 |
|
288 | 281 |
| "equi", [v1; v2] -> |
289 | 282 |
Z3.Boolean.mk_eq |
290 | 283 |
!ctx |
291 |
(val_to_expr v1) |
|
292 |
(val_to_expr v2) |
|
284 |
v1 v2 |
|
293 | 285 |
| "xor", [v1; v2] -> |
294 | 286 |
Z3.Boolean.mk_xor |
295 |
!ctx |
|
296 |
(val_to_expr v1) |
|
297 |
(val_to_expr v2) |
|
287 |
!ctx v1 v2 |
|
298 | 288 |
| "!=", [v1; v2] -> |
299 | 289 |
Z3.Boolean.mk_not |
300 | 290 |
!ctx |
301 | 291 |
( |
302 | 292 |
Z3.Boolean.mk_eq |
303 |
!ctx |
|
304 |
(val_to_expr v1) |
|
305 |
(val_to_expr v2) |
|
293 |
!ctx v1 v2 |
|
306 | 294 |
) |
307 | 295 |
| "/", [v1; v2] -> |
308 | 296 |
Z3.Arithmetic.mk_div |
309 |
!ctx |
|
310 |
(val_to_expr v1) |
|
311 |
(val_to_expr v2) |
|
297 |
!ctx v1 v2 |
|
312 | 298 |
|
313 | 299 |
| "+", [v1; v2] -> |
314 | 300 |
Z3.Arithmetic.mk_add |
315 | 301 |
!ctx |
316 |
[val_to_expr v1; val_to_expr v2] |
|
317 |
|
|
302 |
[v1; v2] |
|
318 | 303 |
| "-", [v1; v2] -> |
319 | 304 |
Z3.Arithmetic.mk_sub |
320 | 305 |
!ctx |
321 |
[val_to_expr v1 ; val_to_expr v2]
|
|
306 |
[v1 ; v2]
|
|
322 | 307 |
|
323 | 308 |
| "*", [v1; v2] -> |
324 | 309 |
Z3.Arithmetic.mk_mul |
325 | 310 |
!ctx |
326 |
[val_to_expr v1; val_to_expr v2]
|
|
311 |
[ v1; v2]
|
|
327 | 312 |
|
328 | 313 |
|
329 | 314 |
| "<", [v1; v2] -> |
330 | 315 |
Z3.Arithmetic.mk_lt |
331 |
!ctx |
|
332 |
(val_to_expr v1) |
|
333 |
(val_to_expr v2) |
|
334 |
|
|
316 |
!ctx v1 v2 |
|
335 | 317 |
| "<=", [v1; v2] -> |
336 | 318 |
Z3.Arithmetic.mk_le |
337 |
!ctx |
|
338 |
(val_to_expr v1) |
|
339 |
(val_to_expr v2) |
|
340 |
|
|
319 |
!ctx v1 v2 |
|
341 | 320 |
| ">", [v1; v2] -> |
342 | 321 |
Z3.Arithmetic.mk_gt |
343 |
!ctx |
|
344 |
(val_to_expr v1) |
|
345 |
(val_to_expr v2) |
|
346 |
|
|
322 |
!ctx v1 v2 |
|
347 | 323 |
| ">=", [v1; v2] -> |
348 | 324 |
Z3.Arithmetic.mk_ge |
349 |
!ctx |
|
350 |
(val_to_expr v1) |
|
351 |
(val_to_expr v2) |
|
352 |
|
|
325 |
!ctx v1 v2 |
|
353 | 326 |
| "int_to_real", [v1] -> |
354 | 327 |
Z3.Arithmetic.Integer.mk_int2real |
355 |
!ctx |
|
356 |
(val_to_expr v1) |
|
357 |
|
|
328 |
!ctx v1 |
|
329 |
| _ -> |
|
330 |
let fd = |
|
331 |
try |
|
332 |
get_fdecl i |
|
333 |
with Not_found -> begin |
|
334 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Registering function %s as uninterpreted function in Z3@.%s: (%a) -> %a" i i (Utils.fprintf_list ~sep:"," Types.print_ty) vltyp Types.print_ty typ); |
|
335 |
decl_fun i vltyp typ |
|
336 |
end |
|
337 |
in |
|
338 |
Z3.FuncDecl.apply fd vl |
|
358 | 339 |
|
340 |
|
|
359 | 341 |
(* | _, [v1; v2] -> Z3.Boolean.mk_and |
360 | 342 |
* !ctx |
361 | 343 |
* (val_to_expr v1) |
362 | 344 |
* (val_to_expr v2) |
363 | 345 |
* |
364 | 346 |
* Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *) |
365 |
| _ -> ( |
|
366 |
let msg fmt = Format.fprintf fmt |
|
367 |
"internal error: zustre unkown function %s (nb args = %i)@." |
|
368 |
i (List.length vl) |
|
369 |
in |
|
370 |
raise (UnknownFunction(i, msg)) |
|
371 |
) |
|
347 |
|
|
348 |
(* | _ -> ( |
|
349 |
* let msg fmt = Format.fprintf fmt |
|
350 |
* "internal error: zustre unkown function %s (nb args = %i)@." |
|
351 |
* i (List.length vl) |
|
352 |
* in |
|
353 |
* raise (UnknownFunction(i, msg)) |
|
354 |
* ) *) |
|
372 | 355 |
|
373 | 356 |
|
374 | 357 |
(* Convert a value expression [v], with internal function calls only. [pp_var] |
... | ... | |
376 | 359 |
may be added for array variables |
377 | 360 |
*) |
378 | 361 |
let rec horn_val_to_expr ?(is_lhs=false) m self v = |
362 |
(* Format.eprintf "h_v2e %a@." (Machine_code_common.pp_val m) v ; *) |
|
379 | 363 |
match v.value_desc with |
380 | 364 |
| Cst c -> horn_const_to_expr c |
381 | 365 |
|
... | ... | |
425 | 409 |
(rename_machine |
426 | 410 |
self |
427 | 411 |
v) |
428 |
| Fun (n, vl) -> horn_basic_app n (horn_val_to_expr m self) vl
|
|
412 |
| Fun (n, vl) -> horn_basic_app n (List.map (horn_val_to_expr m self) vl) (List.map (fun v -> v.value_type) vl, v.value_type)
|
|
429 | 413 |
|
430 | 414 |
let no_reset_to_exprs machines m i = |
431 | 415 |
let (n,_) = List.assoc i m.minstances in |
Also available in: Unified diff