| 1 |
1 |
open Lustre_types
|
| 2 |
2 |
|
|
3 |
let expr_of_vars loc vl =
|
|
4 |
Corelang.expr_of_expr_list loc
|
|
5 |
(List.map Corelang.expr_of_vdecl vl)
|
|
6 |
|
|
7 |
|
| 3 |
8 |
(* Create a node that checks whether two other nodes have the same output *)
|
| 4 |
9 |
|
| 5 |
10 |
let check_eq nd1 nd2 =
|
|
11 |
(* TODO: check that nd1 and nd2 have the same signature *)
|
| 6 |
12 |
let check_nd = Corelang.copy_node nd1 in (* to keep the type info *)
|
| 7 |
13 |
let loc = Location.dummy_loc in
|
| 8 |
14 |
let ok_var =
|
| ... | ... | |
| 13 |
19 |
false,
|
| 14 |
20 |
None,
|
| 15 |
21 |
None)
|
| 16 |
|
in
|
|
22 |
in
|
|
23 |
let input_e = expr_of_vars loc check_nd.node_inputs in
|
|
24 |
let mk_stmt nd out_vars =
|
|
25 |
let call_e = Corelang.mkexpr loc (Expr_appl (nd.node_id, input_e , None)) in
|
|
26 |
Eq (
|
|
27 |
Corelang.mkeq loc
|
|
28 |
(List.map (fun v -> v.var_id) out_vars, call_e)) in
|
|
29 |
let copy_vars vl post =
|
|
30 |
let f v = { (Corelang.copy_var_decl v) with var_id = v.var_id ^ "_" ^ post } in
|
|
31 |
List.map f vl
|
|
32 |
in
|
|
33 |
let out_vars1 = copy_vars nd1.node_outputs "1" in
|
|
34 |
let out_vars2 = copy_vars nd1.node_outputs "2" in
|
|
35 |
let call_n1 = mk_stmt nd1 out_vars1 in
|
|
36 |
let call_n2 = mk_stmt nd2 out_vars2 in
|
|
37 |
let build_eq v1 v2 =
|
|
38 |
let pair = expr_of_vars loc [v1;v2] in
|
|
39 |
Corelang.mkexpr loc (Expr_appl ("=", pair, None))
|
|
40 |
in
|
|
41 |
let rec build_ok vl1 vl2 =
|
|
42 |
match vl1, vl2 with
|
|
43 |
| [v1], [v2] -> build_eq v1 v2
|
|
44 |
| hd1::tl1, hd2::tl2 ->
|
|
45 |
let e1 = (build_eq hd1 hd2) in
|
|
46 |
let e2 = build_ok tl1 tl2 in
|
|
47 |
let e = Corelang.mkexpr loc (Expr_tuple [e1; e2]) in
|
|
48 |
Corelang.mkexpr loc (Expr_appl ("&&", e, None))
|
|
49 |
| _ -> assert false
|
|
50 |
in
|
|
51 |
let ok_expr = build_ok out_vars1 out_vars2 in
|
|
52 |
let ok_stmt = Eq (Corelang.mkeq loc ([ok_var.var_id], ok_expr)) in
|
|
53 |
|
|
54 |
(* Building contract *)
|
|
55 |
let ok_e = Corelang.expr_of_vdecl ok_var in
|
|
56 |
let contract = {
|
|
57 |
consts = [];
|
|
58 |
locals = [];
|
|
59 |
stmts = [];
|
|
60 |
assume = [];
|
|
61 |
guarantees = [Corelang.mkeexpr loc ok_e];
|
|
62 |
modes = [];
|
|
63 |
imports = [];
|
|
64 |
spec_loc = loc;
|
|
65 |
|
|
66 |
}
|
|
67 |
in
|
| 17 |
68 |
let check_nd = { check_nd with
|
| 18 |
69 |
node_id = "check_eq_" ^ nd1.node_id ^ "_" ^ nd2.node_id;
|
| 19 |
|
node_outputs = [ok_var];
|
|
70 |
node_outputs = [ok_var];
|
|
71 |
node_locals = out_vars1 @ out_vars2;
|
|
72 |
node_stmts = [call_n1; call_n2; ok_stmt];
|
|
73 |
node_spec = Some (Contract contract);
|
| 20 |
74 |
}
|
| 21 |
75 |
in
|
| 22 |
|
check_nd
|
| 23 |
76 |
|
|
77 |
|
|
78 |
Global.type_env := Typing.type_node !Global.type_env check_nd loc;
|
|
79 |
Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc check_nd;
|
|
80 |
|
|
81 |
check_nd
|
| 24 |
82 |
(*
|
| 25 |
83 |
|
| 26 |
84 |
TODO:
|
| ... | ... | |
| 38 |
96 |
*)
|
| 39 |
97 |
|
| 40 |
98 |
(* (\* Build the contract: guarentee output = orig_node(input) *\)
|
| 41 |
|
* let expr_of_vars vl =
|
| 42 |
|
* Corelang.expr_of_expr_list loc
|
| 43 |
|
* (List.map Corelang.expr_of_vdecl vl)
|
| 44 |
|
* in
|
|
99 |
*
|
| 45 |
100 |
* let local_outputs = List.map (fun v -> { (Corelang.copy_var_decl v) with var_id = v.var_id ^ "_local" } ) copy_nd.node_outputs in
|
| 46 |
101 |
* let input_e = expr_of_vars copy_nd.node_inputs in
|
| 47 |
102 |
* let call_orig_e =
|
valid _verif node for seal-export lustre