Revision ca7ff3f7
Added by LĂ©lio Brun over 1 year ago
src/lustre_utils.ml  

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 
let expr_of_vars loc vl = 

4 
Corelang.expr_of_expr_list loc (List.map Corelang.expr_of_vdecl vl) 

5  
8  6 
(* Create a node that checks whether two other nodes have the same output *) 
9  7  
10  8 
let check_eq nd1 nd2 = 
11  9 
(* 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 

10 
let check_nd = Corelang.copy_node nd1 in 

11 
(* to keep the type info *) 

12 
let loc = Location.dummy_loc in 

14  13 
let ok_var = 
15  14 
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)


15 
( "__OK",


16 
Corelang.mktyp loc Tydec_bool,


17 
Corelang.mkclock loc Ckdec_any,


18 
false, 

19 
None,


20 
None )


22  21 
in 
23  22 
let input_e = expr_of_vars loc check_nd.node_inputs in 
24  23 
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 

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 

29  27 
let copy_vars vl post = 
30 
let f v = { (Corelang.copy_var_decl v) with var_id = v.var_id ^ "_" ^ post } in 

28 
let f v = 

29 
{ (Corelang.copy_var_decl v) with var_id = v.var_id ^ "_" ^ post } 

30 
in 

31  31 
List.map f vl 
32  32 
in 
33  33 
let out_vars1 = copy_vars nd1.node_outputs "1" in 
...  ...  
35  35 
let call_n1 = mk_stmt nd1 out_vars1 in 
36  36 
let call_n2 = mk_stmt nd2 out_vars2 in 
37  37 
let build_eq v1 v2 = 
38 
let pair = expr_of_vars loc [v1;v2] in


38 
let pair = expr_of_vars loc [ v1; v2 ] in


39  39 
Corelang.mkexpr loc (Expr_appl ("=", pair, None)) 
40  40 
in 
41  41 
let rec build_ok vl1 vl2 = 
42  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 

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 

50  52 
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 
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


53  55  
54  56 
(* 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 
}


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 
} 

67  69 
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 
} 

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 
} 

75  79 
in 
76  80  
77 


78  81 
Global.type_env := Typing.type_node !Global.type_env check_nd loc; 
79  82 
Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc check_nd; 
80 


81 
check_nd 

82 
(* 

83  83  
84 
TODO: 

84 
check_nd 

85 
(* TODO: 

85  86  
86 
construire


87 
construire 

87  88  
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) 

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  91  
92 
et on ajoute le contrat guarantee ok 

93 
in 

94 
check_nd 

92 
et on ajoute le contrat guarantee ok in check_nd *) 

95  93  
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 


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 *) 
Also available in: Unified diff
reformatting