lustrec / src / lustre_utils.ml @ e6b644f4
History  View  Annotate  Download (3.99 KB)
1 
open Lustre_types 

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 

8 
(* Create a node that checks whether two other nodes have the same output *) 
9  
10 
let check_eq nd1 nd2 = 
11 
(* TODO: check that nd1 and nd2 have the same signature *) 
12 
let check_nd = Corelang.copy_node nd1 in (* to keep the type info *) 
13 
let loc = Location.dummy_loc in 
14 
let ok_var = 
15 
Corelang.mkvar_decl loc ~orig:false 
16 
("__OK", 
17 
Corelang.mktyp loc Tydec_bool, 
18 
Corelang.mkclock loc Ckdec_any, 
19 
false, 
20 
None, 
21 
None) 
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 
68 
let check_nd = { check_nd with 
69 
node_id = "check_eq_" ^ nd1.node_id ^ "_" ^ nd2.node_id; 
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); 
74 
} 
75 
in 
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 
82 
(* 
83  
84 
TODO: 
85  
86 
construire 
87  
88 
les variables temporaires pour les outputs de l'un et de l'autre 
89 
les statements d'appels de nodes 
90 
ok = and (o1 = o2) 
91  
92 
et on ajoute le contrat guarantee ok 
93 
in 
94 
check_nd 
95  
96 
*) 
97 

98 
(* (\* Build the contract: guarentee output = orig_node(input) *\) 
99 
* 
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 
101 
* let input_e = expr_of_vars copy_nd.node_inputs in 
102 
* let call_orig_e = 
103 
* Corelang.mkexpr loc (Expr_appl (orig_nd.node_id, input_e , None)) in 
104 
* let build_orig_outputs = 
105 
* Eq ( 
106 
* Corelang.mkeq loc 
107 
* (List.map (fun v > v.var_id) local_outputs, call_orig_e)) in 
108 
* let eq_expr = Corelang.expr_of_expr_list loc ( 
109 
* List.map2 (fun v1 v2 > 
110 
* let args = expr_of_vars [v1;v2] in 
111 
* Corelang.mkexpr loc (Expr_appl ("=", args, None))) 
112 
* copy_nd.node_outputs local_outputs 
113 
* ) 
114 
* in 
115 
* let contract = { 
116 
* consts = []; 
117 
* locals = local_outputs; 
118 
* stmts = [build_orig_outputs]; 
119 
* assume = []; 
120 
* guarantees = [Corelang.mkeexpr loc eq_expr]; 
121 
* modes = []; 
122 
* imports = []; 
123 
* spec_loc = loc; 
124 
* 
125 
* } 
126 
* in *) 
127 
