1
|
open Lustre_types
|
2
|
|
3
|
let expr_of_vars loc vl =
|
4
|
Corelang.expr_of_expr_list loc (List.map Corelang.expr_of_vdecl vl)
|
5
|
|
6
|
(* Create a node that checks whether two other nodes have the same output *)
|
7
|
|
8
|
let check_eq nd1 nd2 =
|
9
|
(* TODO: check that nd1 and nd2 have the same signature *)
|
10
|
let check_nd = Corelang.copy_node nd1 in
|
11
|
(* to keep the type info *)
|
12
|
let loc = Location.dummy_loc in
|
13
|
let ok_var =
|
14
|
Corelang.mkvar_decl loc ~orig:false
|
15
|
( "__OK",
|
16
|
Corelang.mktyp loc Tydec_bool,
|
17
|
Corelang.mkclock loc Ckdec_any,
|
18
|
false,
|
19
|
None,
|
20
|
None )
|
21
|
in
|
22
|
let input_e = expr_of_vars loc check_nd.node_inputs in
|
23
|
let mk_stmt nd out_vars =
|
24
|
let call_e = Corelang.mkexpr loc (Expr_appl (nd.node_id, input_e, None)) in
|
25
|
Eq (Corelang.mkeq loc (List.map (fun v -> v.var_id) out_vars, call_e))
|
26
|
in
|
27
|
let copy_vars vl post =
|
28
|
let f v =
|
29
|
{ (Corelang.copy_var_decl v) with var_id = v.var_id ^ "_" ^ post }
|
30
|
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 ] ->
|
44
|
build_eq v1 v2
|
45
|
| hd1 :: tl1, hd2 :: tl2 ->
|
46
|
let e1 = build_eq hd1 hd2 in
|
47
|
let e2 = build_ok tl1 tl2 in
|
48
|
let e = Corelang.mkexpr loc (Expr_tuple [ e1; e2 ]) in
|
49
|
Corelang.mkexpr loc (Expr_appl ("&&", e, None))
|
50
|
| _ ->
|
51
|
assert false
|
52
|
in
|
53
|
let ok_expr = build_ok out_vars1 out_vars2 in
|
54
|
let ok_stmt = Eq (Corelang.mkeq loc ([ ok_var.var_id ], ok_expr)) in
|
55
|
|
56
|
(* Building contract *)
|
57
|
let ok_e = Corelang.expr_of_vdecl ok_var in
|
58
|
let contract =
|
59
|
{
|
60
|
consts = [];
|
61
|
locals = [];
|
62
|
stmts = [];
|
63
|
assume = [];
|
64
|
guarantees = [ Corelang.mkeexpr loc ok_e ];
|
65
|
modes = [];
|
66
|
imports = [];
|
67
|
spec_loc = loc;
|
68
|
}
|
69
|
in
|
70
|
let check_nd =
|
71
|
{
|
72
|
check_nd with
|
73
|
node_id = "check_eq_" ^ nd1.node_id ^ "_" ^ nd2.node_id;
|
74
|
node_outputs = [ ok_var ];
|
75
|
node_locals = out_vars1 @ out_vars2;
|
76
|
node_stmts = [ call_n1; call_n2; ok_stmt ];
|
77
|
node_spec = Some (Contract contract);
|
78
|
}
|
79
|
in
|
80
|
|
81
|
Global.type_env := Typing.type_node !Global.type_env check_nd loc;
|
82
|
Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc check_nd;
|
83
|
|
84
|
check_nd
|
85
|
(* TODO:
|
86
|
|
87
|
construire
|
88
|
|
89
|
les variables temporaires pour les outputs de l'un et de l'autre les
|
90
|
statements d'appels de nodes ok = and (o1 = o2)
|
91
|
|
92
|
et on ajoute le contrat guarantee ok in check_nd *)
|
93
|
|
94
|
(* (\* Build the contract: guarentee output = orig_node(input) *\) * * let
|
95
|
local_outputs = List.map (fun v -> { (Corelang.copy_var_decl v) with var_id =
|
96
|
v.var_id ^ "_local" } ) copy_nd.node_outputs in * let input_e = expr_of_vars
|
97
|
copy_nd.node_inputs in * let call_orig_e = * Corelang.mkexpr loc (Expr_appl
|
98
|
(orig_nd.node_id, input_e , None)) in * let build_orig_outputs = * Eq ( *
|
99
|
Corelang.mkeq loc * (List.map (fun v -> v.var_id) local_outputs,
|
100
|
call_orig_e)) in * let eq_expr = Corelang.expr_of_expr_list loc ( * List.map2
|
101
|
(fun v1 v2 -> * let args = expr_of_vars [v1;v2] in * Corelang.mkexpr loc
|
102
|
(Expr_appl ("=", args, None))) * copy_nd.node_outputs local_outputs * ) * in
|
103
|
* let contract = { * consts = []; * locals = local_outputs; * stmts =
|
104
|
[build_orig_outputs]; * assume = []; * guarantees = [Corelang.mkeexpr loc
|
105
|
eq_expr]; * modes = []; * imports = []; * spec_loc = loc; * * } * in *)
|