Revision 518951ed
Added by Pierre-Loïc Garoche over 5 years ago
src/tools/seal/seal_export.ml | ||
---|---|---|
8 | 8 |
|
9 | 9 |
let verbose = true |
10 | 10 |
|
11 |
let to_lustre m sw_init sw_step init_out update_out = |
|
11 |
let sw_to_lustre m sw_init sw_step init_out update_out =
|
|
12 | 12 |
let orig_nd = m.mname in |
13 | 13 |
let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in |
14 | 14 |
let vl = (* memories *) |
... | ... | |
66 | 66 |
let e_init_out = process_sw (fun x -> x) init_out in |
67 | 67 |
let e_update_out = process_sw (Corelang.add_pre_expr vl) update_out in |
68 | 68 |
let loc = Location.dummy_loc in |
69 |
(* Build the contract: guarentee output = orig_node(input) *) |
|
70 |
let expr_of_vars vl = |
|
71 |
Corelang.expr_of_expr_list loc |
|
72 |
(List.map Corelang.expr_of_vdecl vl) |
|
73 |
in |
|
74 |
let input_e = expr_of_vars copy_nd.node_inputs in |
|
75 |
let output_e = expr_of_vars copy_nd.node_outputs in |
|
76 |
let call_orig_e = |
|
77 |
Corelang.mkexpr loc (Expr_appl (orig_nd.node_id, input_e , None)) in |
|
78 |
let args = Corelang.mkexpr loc (Expr_tuple([output_e; call_orig_e])) in |
|
79 |
let eq_expr = (Corelang.mkexpr loc (Expr_appl ("=", args, None))) in |
|
80 |
let contract = { |
|
81 |
consts = []; |
|
82 |
locals = []; |
|
83 |
stmts = []; |
|
84 |
assume = []; |
|
85 |
guarantees = [Corelang.mkeexpr loc eq_expr]; |
|
86 |
modes = []; |
|
87 |
imports = []; |
|
88 |
spec_loc = loc; |
|
89 |
|
|
90 |
} |
|
91 |
in |
|
92 |
{ copy_nd with |
|
69 |
let new_nd = |
|
70 |
{ copy_nd with |
|
93 | 71 |
node_id = copy_nd.node_id ^ "_seal"; |
94 | 72 |
node_locals = m.mmemory; |
95 | 73 |
node_stmts = [Eq |
... | ... | |
103 | 81 |
eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init_out, e_update_out)) |
104 | 82 |
}; |
105 | 83 |
]; |
106 |
node_spec = Some (Contract contract);
|
|
84 |
(*node_spec = Some (Contract contract);*)
|
|
107 | 85 |
|
108 | 86 |
(* |
109 | 87 |
il faut mettre un pre devant chaque memoire dans les updates comme dans les gardes par contre pas besoin de mettre de pre devant les entrees, ni dans les updates, ni dans les gardes |
... | ... | |
117 | 95 |
|
118 | 96 |
out1,out2 = if garde1 then e1,e2 else if garde2 .... |
119 | 97 |
*) |
120 |
} |
|
98 |
} |
|
99 |
in |
|
100 |
new_nd, orig_nd |
|
101 |
|
|
102 |
|
|
103 |
let to_lustre basename prog m sw_init sw_step init_out update_out = |
|
104 |
let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in |
|
105 |
|
|
106 |
(* Format.eprintf "%a@." Printers.pp_node new_node; *) |
|
107 |
|
|
108 |
(* Main output *) |
|
109 |
let output_file = !Options.dest_dir ^ "/" ^ basename ^ "_seal.lus" in |
|
110 |
let new_top = |
|
111 |
Corelang.mktop_decl Location.dummy_loc output_file false (Node new_node) |
|
112 |
in |
|
113 |
let out = open_out output_file in |
|
114 |
let fmt = Format.formatter_of_out_channel out in |
|
115 |
Format.fprintf fmt "%a@." Printers.pp_prog [new_top]; |
|
116 |
|
|
117 |
(* Verif output *) |
|
118 |
let output_file_verif = !Options.dest_dir ^ "/" ^ basename ^ "_seal_verif.lus" in |
|
119 |
let out_verif = open_out output_file_verif in |
|
120 |
let fmt_verif = Format.formatter_of_out_channel out_verif in |
|
121 |
let check_nd = Lustre_utils.check_eq new_node orig_nd in |
|
122 |
let check_top = |
|
123 |
Corelang.mktop_decl Location.dummy_loc output_file_verif false (Node check_nd) |
|
124 |
in |
|
125 |
Format.fprintf fmt_verif "%a@." Printers.pp_prog (prog@[new_top;check_top]); |
Also available in: Unified diff
Seal export lustre