Revision ca7ff3f7
Added by Lélio Brun 8 months 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