Revision 01c7d5e1
src/access.ml | ||
---|---|---|
71 | 71 |
| Expr_when (e1,_,_) -> check_expr checks e1 |
72 | 72 |
|
73 | 73 |
| Expr_merge (_,hl) -> List.fold_left (fun checks (l, h) -> check_expr checks h) checks hl |
74 |
| _ -> assert false |
|
75 | 74 |
in (*Format.eprintf "typing %B %a at %a = %a@." const Printers.pp_expr expr Location.pp_loc expr.expr_loc Types.print_ty res;*) res |
76 | 75 |
|
77 | 76 |
let rec check_var_decl_type loc checks ty = |
... | ... | |
90 | 89 |
let check_node nd = |
91 | 90 |
let checks = CSet.empty in |
92 | 91 |
let checks = |
93 |
List.fold_left check_var_decl checks (node_vars nd) in |
|
92 |
List.fold_left check_var_decl checks (get_node_vars nd) in
|
|
94 | 93 |
let checks = |
95 | 94 |
List.fold_left (fun checks eq -> check_expr checks eq.eq_rhs) checks nd.node_eqs in |
96 | 95 |
nd.node_checks <- CSet.elements checks |
src/backends/C/c_backend_common.ml | ||
---|---|---|
192 | 192 |
| Const_tag t -> pp_c_tag fmt t |
193 | 193 |
| Const_array ca -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " pp_c_const) ca |
194 | 194 |
| Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> pp_c_const fmt c)) fl |
195 |
| Const_string _ -> assert false (* string occurs in annotations not in C *) |
|
195 | 196 |
|
196 | 197 |
(* Prints a value expression [v], with internal function calls only. |
197 | 198 |
[pp_var] is a printer for variables (typically [pp_c_var_read]), |
src/backends/C/c_backend_makefile.ml | ||
---|---|---|
1 | 1 |
open Format |
2 |
open LustreSpec |
|
2 | 3 |
open Corelang |
3 | 4 |
|
4 | 5 |
let header_has_code header = |
... | ... | |
40 | 41 |
|
41 | 42 |
module type MODIFIERS_MKF = |
42 | 43 |
sig |
43 |
val other_targets: Format.formatter -> string -> string -> (string * bool * Corelang.top_decl list) list -> unit
|
|
44 |
val other_targets: Format.formatter -> string -> string -> (string * bool * top_decl list) list -> unit |
|
44 | 45 |
end |
45 | 46 |
|
46 | 47 |
module EmptyMod = |
src/backends/C/c_backend_spec.ml | ||
---|---|---|
2 | 2 |
open LustreSpec |
3 | 3 |
open Machine_code |
4 | 4 |
open C_backend_common |
5 |
open Utils |
|
5 | 6 |
|
6 | 7 |
(**************************************************************************) |
7 | 8 |
(* Printing spec for c *) |
8 | 9 |
|
9 | 10 |
(**************************************************************************) |
11 |
(* OLD STUFF ??? |
|
12 |
|
|
10 | 13 |
|
11 | 14 |
let pp_acsl_type var fmt t = |
12 | 15 |
let rec aux t pp_suffix = |
... | ... | |
121 | 124 |
pp_acsl_spec m.mstep.step_outputs fmt spec |
122 | 125 |
) |
123 | 126 |
|
127 |
*) |
|
128 |
|
|
124 | 129 |
(**************************************************************************) |
125 | 130 |
(* MAKEFILE *) |
126 | 131 |
(**************************************************************************) |
src/causality.ml | ||
---|---|---|
249 | 249 |
mashup_appl_dependencies f e g |
250 | 250 |
| Expr_appl (f, e, Some (r, _)) -> |
251 | 251 |
mashup_appl_dependencies f e (add_var lhs_is_mem lhs r g) |
252 |
| Expr_uclock (e, _) |
|
253 |
| Expr_dclock (e, _) |
|
254 |
| Expr_phclock (e, _) -> add_dep lhs_is_mem lhs e g |
|
255 | 252 |
in |
256 | 253 |
let g = |
257 | 254 |
List.fold_left |
... | ... | |
294 | 291 |
| Expr_arrow (e1,e2) -> ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2) |
295 | 292 |
| Expr_ite (c, t, e) -> ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e)) |
296 | 293 |
| Expr_pre e |
297 |
| Expr_when (e,_,_) |
|
298 |
| Expr_uclock (e,_) |
|
299 |
| Expr_dclock (e,_) |
|
300 |
| Expr_phclock (e,_) -> get_expr_calls prednode e |
|
294 |
| Expr_when (e,_,_) -> get_expr_calls prednode e |
|
301 | 295 |
| Expr_appl (id,e, _) -> |
302 | 296 |
if not (Basic_library.is_internal_fun id) && prednode id |
303 | 297 |
then ESet.add expr (get_expr_calls prednode e) |
... | ... | |
357 | 351 |
module Cycles = Graph.Components.Make (IdentDepGraph) |
358 | 352 |
|
359 | 353 |
let mk_copy_var n id = |
360 |
mk_new_name (node_vars n) id |
|
354 |
mk_new_name (get_node_vars n) id
|
|
361 | 355 |
|
362 | 356 |
let mk_copy_eq n var = |
363 |
let var_decl = node_var var n in |
|
357 |
let var_decl = get_node_var var n in
|
|
364 | 358 |
let cp_var = mk_copy_var n var in |
365 | 359 |
let expr = |
366 | 360 |
{ expr_tag = Utils.new_tag (); |
src/clock_calculus.ml | ||
---|---|---|
685 | 685 |
List.iter (fun (t, h) -> clock_subtyping_arg env h (new_ck (Con (cvar,cr,t)) true)) hl; |
686 | 686 |
expr.expr_clock <- cvar; |
687 | 687 |
cvar |
688 |
| Expr_uclock (e,k) -> |
|
689 |
let pck = clock_expr env e in |
|
690 |
if not (can_be_pck pck) then |
|
691 |
raise (Error (e.expr_loc, Not_pck)); |
|
692 |
if k = 0 then |
|
693 |
raise (Error (expr.expr_loc, Factor_zero)); |
|
694 |
(try |
|
695 |
subsume pck (CSet_pck (k,(0,1))) |
|
696 |
with Subsume (ck,cset) -> |
|
697 |
raise (Error (e.expr_loc, Clock_set_mismatch (ck,CSet_pck (k,(0,1)))))); |
|
698 |
let ck = new_ck (Pck_up (pck,k)) true in |
|
699 |
expr.expr_clock <- ck; |
|
700 |
ck |
|
701 |
| Expr_dclock (e,k) -> |
|
702 |
let pck = clock_expr env e in |
|
703 |
if not (can_be_pck pck) then |
|
704 |
raise (Error (e.expr_loc, Not_pck)); |
|
705 |
if k = 0 then |
|
706 |
raise (Error (expr.expr_loc, Factor_zero)); |
|
707 |
(try |
|
708 |
subsume pck (CSet_pck (1,(0,1))) |
|
709 |
with Subsume (ck,cset) -> |
|
710 |
raise (Error (e.expr_loc, Clock_set_mismatch (ck,CSet_pck (1,(0,1)))))); |
|
711 |
let ck = new_ck (Pck_down (pck,k)) true in |
|
712 |
expr.expr_clock <- ck; |
|
713 |
ck |
|
714 |
| Expr_phclock (e,(a,b)) -> |
|
715 |
let pck = clock_expr env e in |
|
716 |
if not (can_be_pck pck) then |
|
717 |
raise (Error (e.expr_loc, Not_pck)); |
|
718 |
let (a,b) = simplify_rat (a,b) in |
|
719 |
(try |
|
720 |
subsume pck (CSet_pck (b,(0,1))) |
|
721 |
with Subsume (ck,cset) -> |
|
722 |
raise (Error (e.expr_loc, Clock_set_mismatch (ck,CSet_pck (b,(0,1)))))); |
|
723 |
let ck = new_ck (Pck_phase (pck,(a,b))) true in |
|
724 |
expr.expr_clock <- ck; |
|
725 |
ck |
|
726 | 688 |
in |
727 | 689 |
Log.report ~level:4 (fun fmt -> Format.fprintf fmt "Clock of expr %a: %a@." Printers.pp_expr expr Clocks.print_ck resulting_ck); |
728 | 690 |
resulting_ck |
src/corelang.ml | ||
---|---|---|
23 | 23 |
open LustreSpec |
24 | 24 |
open Dimension |
25 | 25 |
|
26 |
(** The core language and its ast. Every element of the ast contains its |
|
27 |
location in the program text. The type and clock of an ast element |
|
28 |
is mutable (and initialized to dummy values). This avoids to have to |
|
29 |
duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *) |
|
30 |
|
|
31 |
type ident = Utils.ident |
|
32 |
type label = Utils.ident |
|
33 |
type rat = Utils.rat |
|
34 |
type tag = Utils.tag |
|
35 |
|
|
36 |
type constant = |
|
37 |
| Const_int of int |
|
38 |
| Const_real of string |
|
39 |
| Const_float of float |
|
40 |
| Const_array of constant list |
|
41 |
| Const_tag of label |
|
42 |
| Const_struct of (label * constant) list |
|
43 |
|
|
44 |
type type_dec = LustreSpec.type_dec |
|
45 |
|
|
46 |
let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc} |
|
47 |
|
|
48 |
|
|
49 |
type clock_dec = LustreSpec.clock_dec |
|
50 |
|
|
51 |
let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc} |
|
52 |
|
|
53 |
type var_decl = LustreSpec.var_decl |
|
54 |
|
|
55 |
(* The tag of an expression is a unique identifier used to distinguish |
|
56 |
different instances of the same node *) |
|
57 |
type expr = |
|
58 |
{expr_tag: tag; |
|
59 |
expr_desc: expr_desc; |
|
60 |
mutable expr_type: Types.type_expr; |
|
61 |
mutable expr_clock: Clocks.clock_expr; |
|
62 |
mutable expr_delay: Delay.delay_expr; |
|
63 |
mutable expr_annot: LustreSpec.expr_annot option; |
|
64 |
expr_loc: Location.t} |
|
65 |
|
|
66 |
and expr_desc = |
|
67 |
| Expr_const of constant |
|
68 |
| Expr_ident of ident |
|
69 |
| Expr_tuple of expr list |
|
70 |
| Expr_ite of expr * expr * expr |
|
71 |
| Expr_arrow of expr * expr |
|
72 |
| Expr_fby of expr * expr |
|
73 |
| Expr_array of expr list |
|
74 |
| Expr_access of expr * Dimension.dim_expr |
|
75 |
| Expr_power of expr * Dimension.dim_expr |
|
76 |
| Expr_pre of expr |
|
77 |
| Expr_when of expr * ident * label |
|
78 |
| Expr_merge of ident * (label * expr) list |
|
79 |
| Expr_appl of call_t |
|
80 |
| Expr_uclock of expr * int |
|
81 |
| Expr_dclock of expr * int |
|
82 |
| Expr_phclock of expr * rat |
|
83 |
and call_t = ident * expr * (ident * label) option (* The third part denotes the reseting clock label and value *) |
|
84 |
|
|
85 |
type eq = |
|
86 |
{eq_lhs: ident list; |
|
87 |
eq_rhs: expr; |
|
88 |
eq_loc: Location.t} |
|
89 |
|
|
90 |
type assert_t = |
|
91 |
{ |
|
92 |
assert_expr: expr; |
|
93 |
assert_loc: Location.t |
|
94 |
} |
|
95 |
|
|
96 |
type node_desc = |
|
97 |
{node_id: ident; |
|
98 |
mutable node_type: Types.type_expr; |
|
99 |
mutable node_clock: Clocks.clock_expr; |
|
100 |
node_inputs: var_decl list; |
|
101 |
node_outputs: var_decl list; |
|
102 |
node_locals: var_decl list; |
|
103 |
mutable node_gencalls: expr list; |
|
104 |
mutable node_checks: Dimension.dim_expr list; |
|
105 |
node_asserts: assert_t list; |
|
106 |
node_eqs: eq list; |
|
107 |
mutable node_dec_stateless: bool; |
|
108 |
mutable node_stateless: bool option; |
|
109 |
node_spec: LustreSpec.node_annot option; |
|
110 |
node_annot: LustreSpec.expr_annot option; |
|
111 |
} |
|
112 |
|
|
113 |
type imported_node_desc = |
|
114 |
{nodei_id: ident; |
|
115 |
mutable nodei_type: Types.type_expr; |
|
116 |
mutable nodei_clock: Clocks.clock_expr; |
|
117 |
nodei_inputs: var_decl list; |
|
118 |
nodei_outputs: var_decl list; |
|
119 |
nodei_stateless: bool; |
|
120 |
nodei_spec: LustreSpec.node_annot option; |
|
121 |
nodei_prototype: string option; |
|
122 |
nodei_in_lib: string option; |
|
123 |
} |
|
124 |
|
|
125 |
type const_desc = |
|
126 |
{const_id: ident; |
|
127 |
const_loc: Location.t; |
|
128 |
const_value: constant; |
|
129 |
mutable const_type: Types.type_expr; |
|
130 |
} |
|
131 |
|
|
132 |
type top_decl_desc = |
|
133 |
| Node of node_desc |
|
134 |
| Consts of const_desc list |
|
135 |
| ImportedNode of imported_node_desc |
|
136 |
| Open of bool * string (* the boolean set to true denotes a local |
|
137 |
lusi vs a lusi installed at system level *) |
|
138 |
|
|
139 |
type top_decl = |
|
140 |
{top_decl_desc: top_decl_desc; |
|
141 |
top_decl_loc: Location.t} |
|
142 |
|
|
143 |
type program = top_decl list |
|
144 |
|
|
145 |
type error = |
|
146 |
Main_not_found |
|
147 |
| Main_wrong_kind |
|
148 |
| No_main_specified |
|
149 |
| Unbound_symbol of ident |
|
150 |
| Already_bound_symbol of ident |
|
151 | 26 |
|
152 | 27 |
exception Error of Location.t * error |
153 | 28 |
|
... | ... | |
163 | 38 |
|
164 | 39 |
module VSet = Set.Make(VDeclModule) |
165 | 40 |
|
41 |
let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc} |
|
42 |
|
|
43 |
|
|
44 |
|
|
45 |
let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc} |
|
46 |
|
|
47 |
|
|
48 |
|
|
166 | 49 |
(************************************************************) |
167 | 50 |
(* *) |
168 | 51 |
|
... | ... | |
206 | 89 |
else name |
207 | 90 |
in new_name id 1 |
208 | 91 |
|
209 |
let update_expr_annot e annot = |
|
210 |
{ e with expr_annot = LustreSpec.merge_expr_annot e.expr_annot (Some annot) } |
|
211 |
|
|
212 | 92 |
let mkeq loc (lhs, rhs) = |
213 | 93 |
{ eq_lhs = lhs; |
214 | 94 |
eq_rhs = rhs; |
... | ... | |
225 | 105 |
let mkpredef_call loc funname args = |
226 | 106 |
mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None)) |
227 | 107 |
|
108 |
(************************************************************) |
|
109 |
(* Eexpr functions *) |
|
110 |
(************************************************************) |
|
111 |
|
|
112 |
let merge_node_annot ann1 ann2 = |
|
113 |
{ requires = ann1.requires @ ann2.requires; |
|
114 |
ensures = ann1.ensures @ ann2.ensures; |
|
115 |
behaviors = ann1.behaviors @ ann2.behaviors; |
|
116 |
spec_loc = ann1.spec_loc |
|
117 |
} |
|
118 |
|
|
119 |
let mkeexpr loc expr = |
|
120 |
{ eexpr_tag = Utils.new_tag (); |
|
121 |
eexpr_qfexpr = expr; |
|
122 |
eexpr_quantifiers = []; |
|
123 |
eexpr_type = Types.new_var (); |
|
124 |
eexpr_clock = Clocks.new_var true; |
|
125 |
eexpr_normalized = None; |
|
126 |
eexpr_loc = loc } |
|
127 |
|
|
128 |
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers } |
|
129 |
|
|
130 |
(* |
|
131 |
let mkepredef_call loc funname args = |
|
132 |
mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None)) |
|
133 |
|
|
134 |
let mkepredef_unary_call loc funname arg = |
|
135 |
mkeexpr loc (EExpr_appl (funname, arg, None)) |
|
136 |
*) |
|
137 |
|
|
138 |
let merge_expr_annot ann1 ann2 = |
|
139 |
match ann1, ann2 with |
|
140 |
| None, None -> assert false |
|
141 |
| Some _, None -> ann1 |
|
142 |
| None, Some _ -> ann2 |
|
143 |
| Some ann1, Some ann2 -> Some { |
|
144 |
annots = ann1.annots @ ann2.annots; |
|
145 |
annot_loc = ann1.annot_loc |
|
146 |
} |
|
147 |
|
|
148 |
let update_expr_annot e annot = |
|
149 |
{ e with expr_annot = merge_expr_annot e.expr_annot (Some annot) } |
|
150 |
|
|
151 |
|
|
228 | 152 |
(***********************************************************) |
229 | 153 |
(* Fast access to nodes, by name *) |
230 | 154 |
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30 |
... | ... | |
449 | 373 |
| Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e' |
450 | 374 |
| Expr_merge(i, hl), Expr_merge(i', hl') -> i=i' && List.for_all2 (fun (t, h) (t', h') -> t=t' && is_eq_expr h h') (sort_handlers hl) (sort_handlers hl') |
451 | 375 |
| Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e' |
452 |
| Expr_uclock(e, i), Expr_uclock(e', i') -> i=i' && is_eq_expr e e' |
|
453 |
| Expr_dclock(e, i), Expr_dclock(e', i') -> i=i' && is_eq_expr e e' |
|
454 |
| Expr_phclock(e, r), Expr_phclock(e', r') -> r=r' && is_eq_expr e e' |
|
455 | 376 |
| Expr_power (e1, i1), Expr_power (e2, i2) |
456 | 377 |
| Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2) |
457 | 378 |
| _ -> false |
458 | 379 |
|
459 |
let node_vars nd = |
|
380 |
let get_node_vars nd =
|
|
460 | 381 |
nd.node_inputs @ nd.node_locals @ nd.node_outputs |
461 | 382 |
|
462 |
let node_var id node =
|
|
463 |
List.find (fun v -> v.var_id = id) (node_vars node)
|
|
383 |
let get_var id var_list =
|
|
384 |
List.find (fun v -> v.var_id = id) var_list
|
|
464 | 385 |
|
465 |
let node_eq id node = |
|
386 |
let get_node_var id node = get_var id (get_node_vars node) |
|
387 |
|
|
388 |
let get_node_eq id node = |
|
466 | 389 |
List.find (fun eq -> List.mem id eq.eq_lhs) node.node_eqs |
467 | 390 |
|
468 | 391 |
let get_nodes prog = |
... | ... | |
505 | 428 |
| Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l) |
506 | 429 |
| Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl) |
507 | 430 |
| Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (fun (x, l) -> fvar x, l) i') |
508 |
| _ -> assert false |
|
509 | 431 |
|
510 | 432 |
(* Applies the renaming function [fvar] to every rhs |
511 | 433 |
only when the corresponding lhs satisfies predicate [pvar] *) |
... | ... | |
541 | 463 |
in Expr_when (replace lhs e', i', l) |
542 | 464 |
| Expr_merge (i, hl) -> let i' = if pvar lhs then fvar i else i |
543 | 465 |
in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl) |
544 |
| _ -> assert false)
|
|
466 |
) |
|
545 | 467 |
in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs } |
546 | 468 |
|
547 | 469 |
|
... | ... | |
565 | 487 |
Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl) |
566 | 488 |
| Expr_appl (i, e', i') -> |
567 | 489 |
Expr_appl (f_node i, re e', Utils.option_map (fun (x, l) -> f_var x, l) i') |
568 |
| _ -> assert false |
|
569 |
|
|
490 |
|
|
570 | 491 |
let rename_node_annot f_node f_var f_const expr = |
571 | 492 |
expr |
572 | 493 |
(* TODO assert false *) |
... | ... | |
599 | 520 |
nd.node_spec |
600 | 521 |
in |
601 | 522 |
let annot = |
602 |
Utils.option_map
|
|
523 |
List.map
|
|
603 | 524 |
(fun s -> rename_expr_annot f_node f_var f_const s) |
604 | 525 |
nd.node_annot |
605 | 526 |
in |
... | ... | |
724 | 645 |
(fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd) |
725 | 646 |
Basic_library.internal_funs |
726 | 647 |
|
648 |
|
|
649 |
let rec get_expr_calls nodes e = |
|
650 |
get_calls_expr_desc nodes e.expr_desc |
|
651 |
and get_calls_expr_desc nodes expr_desc = |
|
652 |
let get_calls = get_expr_calls nodes in |
|
653 |
match expr_desc with |
|
654 |
| Expr_const _ |
|
655 |
| Expr_ident _ -> Utils.ISet.empty |
|
656 |
| Expr_tuple el |
|
657 |
| Expr_array el -> List.fold_left (fun accu e -> Utils.ISet.union accu (get_calls e)) Utils.ISet.empty el |
|
658 |
| Expr_pre e1 |
|
659 |
| Expr_when (e1, _, _) |
|
660 |
| Expr_access (e1, _) |
|
661 |
| Expr_power (e1, _) -> get_calls e1 |
|
662 |
| Expr_ite (c, t, e) -> Utils.ISet.union (Utils.ISet.union (get_calls c) (get_calls t)) (get_calls e) |
|
663 |
| Expr_arrow (e1, e2) |
|
664 |
| Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2) |
|
665 |
| Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty hl |
|
666 |
| Expr_appl (i, e', i') -> |
|
667 |
if Basic_library.is_internal_fun i then |
|
668 |
(get_calls e') |
|
669 |
else |
|
670 |
let calls = Utils.ISet.add i (get_calls e') in |
|
671 |
let test = (fun n -> match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false) in |
|
672 |
if List.exists test nodes then |
|
673 |
match (List.find test nodes).top_decl_desc with |
|
674 |
| Node nd -> Utils.ISet.union (get_node_calls nodes nd) calls |
|
675 |
| _ -> assert false |
|
676 |
else |
|
677 |
calls |
|
678 |
|
|
679 |
and get_eq_calls nodes eq = |
|
680 |
get_expr_calls nodes eq.eq_rhs |
|
681 |
and get_node_calls nodes node = |
|
682 |
List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty node.node_eqs |
|
683 |
|
|
684 |
|
|
685 |
let rec expr_has_arrows e = |
|
686 |
expr_desc_has_arrows e.expr_desc |
|
687 |
and expr_desc_has_arrows expr_desc = |
|
688 |
match expr_desc with |
|
689 |
| Expr_const _ |
|
690 |
| Expr_ident _ -> false |
|
691 |
| Expr_tuple el |
|
692 |
| Expr_array el -> List.exists expr_has_arrows el |
|
693 |
| Expr_pre e1 |
|
694 |
| Expr_when (e1, _, _) |
|
695 |
| Expr_access (e1, _) |
|
696 |
| Expr_power (e1, _) -> expr_has_arrows e1 |
|
697 |
| Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e] |
|
698 |
| Expr_arrow (e1, e2) |
|
699 |
| Expr_fby (e1, e2) -> true |
|
700 |
| Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl |
|
701 |
| Expr_appl (i, e', i') -> expr_has_arrows e' |
|
702 |
|
|
703 |
and eq_has_arrows eq = |
|
704 |
expr_has_arrows eq.eq_rhs |
|
705 |
and node_has_arrows node = |
|
706 |
List.exists (fun eq -> eq_has_arrows eq) node.node_eqs |
|
707 |
|
|
727 | 708 |
(* Local Variables: *) |
728 | 709 |
(* compile-command:"make -C .." *) |
729 | 710 |
(* End: *) |
src/corelang.mli | ||
---|---|---|
21 | 21 |
*---------------------------------------------------------------------------- *) |
22 | 22 |
|
23 | 23 |
open LustreSpec |
24 |
|
|
24 |
(* |
|
25 | 25 |
(** The core language and its ast. *) |
26 | 26 |
type ident = Utils.ident |
27 | 27 |
type label = Utils.ident |
... | ... | |
161 | 161 |
| No_main_specified |
162 | 162 |
| Unbound_symbol of ident |
163 | 163 |
| Already_bound_symbol of ident |
164 |
|
|
164 |
*) |
|
165 | 165 |
exception Error of Location.t * error |
166 | 166 |
|
167 |
val dummy_type_dec: type_dec |
|
168 |
val dummy_clock_dec: clock_dec |
|
169 |
|
|
167 | 170 |
val mktyp: Location.t -> type_dec_desc -> type_dec |
168 | 171 |
val mkclock: Location.t -> clock_dec_desc -> clock_dec |
169 | 172 |
val mkvar_decl: Location.t -> ident * type_dec * clock_dec * bool (* is const *) -> var_decl |
... | ... | |
204 | 207 |
val const_xor: constant -> constant -> constant |
205 | 208 |
val const_impl: constant -> constant -> constant |
206 | 209 |
|
207 |
val node_vars: node_desc -> var_decl list |
|
208 |
val node_var: ident -> node_desc -> var_decl |
|
209 |
val node_eq: ident -> node_desc -> eq |
|
210 |
val get_node_vars: node_desc -> var_decl list
|
|
211 |
val get_node_var: ident -> node_desc -> var_decl
|
|
212 |
val get_node_eq: ident -> node_desc -> eq
|
|
210 | 213 |
|
211 | 214 |
(* val get_const: ident -> constant *) |
212 | 215 |
|
... | ... | |
248 | 251 |
val update_expr_annot: expr -> LustreSpec.expr_annot -> expr |
249 | 252 |
|
250 | 253 |
|
254 |
(** Annotation expression related functions *) |
|
255 |
val mkeexpr: Location.t -> expr -> eexpr |
|
256 |
val merge_node_annot: node_annot -> node_annot -> node_annot |
|
257 |
val extend_eexpr: (quantifier_type * var_decl list) list -> eexpr -> eexpr |
|
258 |
val update_expr_annot: expr -> expr_annot -> expr |
|
259 |
(* val mkpredef_call: Location.t -> ident -> eexpr list -> eexpr*) |
|
260 |
|
|
251 | 261 |
(* Local Variables: *) |
252 | 262 |
(* compile-command:"make -C .." *) |
253 | 263 |
(* End: *) |
src/horn_backend.ml | ||
---|---|---|
313 | 313 |
(Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs |
314 | 314 |
pp_machine_step_name m.mname.node_id |
315 | 315 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); |
316 |
|
|
316 |
(* |
|
317 | 317 |
match m.mspec with |
318 | 318 |
None -> () (* No node spec; we do nothing *) |
319 | 319 |
| Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} -> |
... | ... | |
323 | 323 |
|
324 | 324 |
) |
325 | 325 |
| _ -> () (* Other cases give nothing *) |
326 |
*) |
|
326 | 327 |
end |
327 | 328 |
end |
328 | 329 |
|
src/inliner.ml | ||
---|---|---|
134 | 134 |
let el, l', eqs' = inline_tuple (List.map snd branches) in |
135 | 135 |
let branches' = List.map2 (fun (label, _) v -> label, v) branches el in |
136 | 136 |
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs' |
137 |
| Expr_uclock _ |
|
138 |
| Expr_dclock _ |
|
139 |
| Expr_phclock _ -> assert false |
|
140 | 137 |
and inline_node nd nodes = |
141 | 138 |
let new_locals, eqs = |
142 | 139 |
List.fold_left (fun (locals, eqs) eq -> |
... | ... | |
244 | 241 |
node_stateless = None; |
245 | 242 |
node_spec = Some |
246 | 243 |
{requires = []; |
247 |
ensures = [EnsuresExpr (mkeexpr loc (EExpr_ident ok_ident))]; |
|
248 |
behaviors = [] |
|
244 |
ensures = [mkeexpr loc (mkexpr loc (Expr_ident ok_ident))]; |
|
245 |
behaviors = []; |
|
246 |
spec_loc = loc |
|
249 | 247 |
}; |
250 |
node_annot = None;
|
|
248 |
node_annot = [];
|
|
251 | 249 |
} |
252 | 250 |
in |
253 | 251 |
let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc }] in |
src/lexerLustreSpec.mll | ||
---|---|---|
1 | 1 |
{ |
2 | 2 |
|
3 |
open ParserLustreSpec |
|
3 |
(* open ParserLustreSpec *) |
|
4 |
open Parser_lustre |
|
4 | 5 |
open Utils |
5 | 6 |
|
6 | 7 |
let str_buf = Buffer.create 1024 |
... | ... | |
11 | 12 |
used to handle all the possible keywords. *) |
12 | 13 |
let keyword_table = |
13 | 14 |
create_hashtable 20 [ |
14 |
"true", TRUE;
|
|
15 |
"false", FALSE;
|
|
15 |
(* "true", TRUE; *)
|
|
16 |
(* "false", FALSE; *)
|
|
16 | 17 |
"stateless", STATELESS; |
17 | 18 |
"if", IF; |
18 | 19 |
"then", THEN; |
... | ... | |
44 | 45 |
"pre", PRE; |
45 | 46 |
"div", DIV; |
46 | 47 |
"const", CONST; |
47 |
"include", INCLUDE;
|
|
48 |
(* "include", INCLUDE; *)
|
|
48 | 49 |
"assert", ASSERT; |
49 | 50 |
"ensures", ENSURES; |
50 | 51 |
"requires", REQUIRES; |
... | ... | |
136 | 137 |
let annot s = |
137 | 138 |
let lb = Lexing.from_string s in |
138 | 139 |
try |
139 |
ParserLustreSpec.lustre_annot token lb
|
|
140 |
Parser_lustre.lustre_annot(* ParserLustreSpec.lustre_annot *) token lb
|
|
140 | 141 |
with Parsing.Parse_error as _e -> ( |
141 | 142 |
Format.eprintf "Lexing error at position %a:@.unexpected token %s@.@?" |
142 | 143 |
(fun fmt p -> Format.fprintf fmt "%s l%i c%i" p.Lexing.pos_fname p.Lexing.pos_lnum p.Lexing.pos_cnum) lb.Lexing.lex_curr_p |
... | ... | |
146 | 147 |
|
147 | 148 |
let spec s = |
148 | 149 |
let lb = Lexing.from_string s in |
149 |
ParserLustreSpec.lustre_spec token lb
|
|
150 |
Parser_lustre.lustre_spec (*ParserLustreSpec.lustre_spec*) token lb
|
|
150 | 151 |
|
151 | 152 |
} |
src/liveness.ml | ||
---|---|---|
186 | 186 |
|
187 | 187 |
let find_compatible_local node var dead = |
188 | 188 |
(*Format.eprintf "find_compatible_local %s %s %a@." node.node_id var pp_iset dead;*) |
189 |
let typ = (Corelang.node_var var node).var_type in
|
|
190 |
let eq_var = node_eq var node in |
|
189 |
let typ = (get_node_var var node).var_type in
|
|
190 |
let eq_var = get_node_eq var node in
|
|
191 | 191 |
let aliasable_inputs = |
192 | 192 |
match NodeDep.get_callee eq_var.eq_rhs with |
193 | 193 |
| None -> [] |
src/lustreSpec.ml | ||
---|---|---|
1 | 1 |
open Format |
2 | 2 |
|
3 |
|
|
4 |
let merge_expr_annot ann1 ann2 = |
|
5 |
match ann1, ann2 with |
|
6 |
| None, None -> assert false |
|
7 |
| Some _, None -> ann1 |
|
8 |
| None, Some _ -> ann2 |
|
9 |
| Some ann1, Some ann2 -> Some (ann1@ann2) |
|
10 |
|
|
11 |
|
|
12 | 3 |
type ident = Utils.ident |
4 |
type label = Utils.ident |
|
13 | 5 |
type rat = Utils.rat |
14 | 6 |
type tag = Utils.tag |
15 | 7 |
|
16 |
type constant = |
|
17 |
| EConst_int of int |
|
18 |
| EConst_real of string |
|
19 |
| EConst_float of float |
|
20 |
| EConst_bool of bool |
|
21 |
| EConst_string of string |
|
22 |
|
|
23 | 8 |
type type_dec = |
24 | 9 |
{ty_dec_desc: type_dec_desc; |
25 | 10 |
ty_dec_loc: Location.t} |
... | ... | |
54 | 39 |
mutable var_clock: Clocks.clock_expr; |
55 | 40 |
var_loc: Location.t} |
56 | 41 |
|
42 |
(** The core language and its ast. Every element of the ast contains its |
|
43 |
location in the program text. The type and clock of an ast element |
|
44 |
is mutable (and initialized to dummy values). This avoids to have to |
|
45 |
duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *) |
|
46 |
|
|
47 |
|
|
48 |
type constant = |
|
49 |
| Const_int of int |
|
50 |
| Const_real of string |
|
51 |
| Const_float of float |
|
52 |
| Const_array of constant list |
|
53 |
| Const_tag of label |
|
54 |
| Const_string of string (* used only for annotations *) |
|
55 |
| Const_struct of (label * constant) list |
|
56 |
|
|
57 |
type quantifier_type = Exists | Forall |
|
58 |
|
|
59 |
|
|
60 |
|
|
57 | 61 |
(* The tag of an expression is a unique identifier used to distinguish |
58 | 62 |
different instances of the same node *) |
59 |
type eexpr = |
|
63 |
type expr = |
|
64 |
{expr_tag: tag; |
|
65 |
expr_desc: expr_desc; |
|
66 |
mutable expr_type: Types.type_expr; |
|
67 |
mutable expr_clock: Clocks.clock_expr; |
|
68 |
mutable expr_delay: Delay.delay_expr; |
|
69 |
mutable expr_annot: expr_annot option; |
|
70 |
expr_loc: Location.t} |
|
71 |
|
|
72 |
and expr_desc = |
|
73 |
| Expr_const of constant |
|
74 |
| Expr_ident of ident |
|
75 |
| Expr_tuple of expr list |
|
76 |
| Expr_ite of expr * expr * expr |
|
77 |
| Expr_arrow of expr * expr |
|
78 |
| Expr_fby of expr * expr |
|
79 |
| Expr_array of expr list |
|
80 |
| Expr_access of expr * Dimension.dim_expr |
|
81 |
| Expr_power of expr * Dimension.dim_expr |
|
82 |
| Expr_pre of expr |
|
83 |
| Expr_when of expr * ident * label |
|
84 |
| Expr_merge of ident * (label * expr) list |
|
85 |
| Expr_appl of call_t |
|
86 |
and call_t = ident * expr * (ident * label) option |
|
87 |
(* The third part denotes the reseting clock label and value *) |
|
88 |
and |
|
89 |
(* The tag of an expression is a unique identifier used to distinguish |
|
90 |
different instances of the same node *) |
|
91 |
eexpr = |
|
60 | 92 |
{eexpr_tag: tag; |
61 |
eexpr_desc: eexpr_desc; |
|
93 |
eexpr_qfexpr: expr; |
|
94 |
eexpr_quantifiers: (quantifier_type * var_decl list) list; |
|
62 | 95 |
mutable eexpr_type: Types.type_expr; |
63 | 96 |
mutable eexpr_clock: Clocks.clock_expr; |
97 |
mutable eexpr_normalized: (var_decl * eq list * var_decl list) option; |
|
64 | 98 |
eexpr_loc: Location.t} |
65 | 99 |
|
66 |
and eexpr_desc = |
|
67 |
| EExpr_const of constant |
|
68 |
| EExpr_ident of ident |
|
69 |
| EExpr_tuple of eexpr list |
|
70 |
| EExpr_arrow of eexpr * eexpr |
|
71 |
| EExpr_fby of eexpr * eexpr |
|
72 |
(* | EExpr_concat of eexpr * eexpr *) |
|
73 |
(* | EExpr_tail of eexpr *) |
|
74 |
| EExpr_pre of eexpr |
|
75 |
| EExpr_when of eexpr * ident |
|
76 |
(* | EExpr_whennot of eexpr * ident *) |
|
77 |
| EExpr_merge of ident * eexpr * eexpr |
|
78 |
| EExpr_appl of ident * eexpr * ident option |
|
79 |
(* | EExpr_uclock of eexpr * int *) |
|
80 |
(* | EExpr_dclock of eexpr * int *) |
|
81 |
(* | EExpr_phclock of eexpr * rat *) |
|
82 |
| EExpr_exists of var_decl list * eexpr |
|
83 |
| EExpr_forall of var_decl list * eexpr |
|
84 |
|
|
85 |
type ensures_t = EnsuresExpr of eexpr | SpecObserverNode of (string * eexpr list) |
|
100 |
and expr_annot = { |
|
101 |
annots: (string list * eexpr) list; |
|
102 |
annot_loc: Location.t |
|
103 |
} |
|
104 |
and |
|
105 |
eq = |
|
106 |
{eq_lhs: ident list; |
|
107 |
eq_rhs: expr; |
|
108 |
eq_loc: Location.t} |
|
109 |
|
|
86 | 110 |
|
87 | 111 |
type node_annot = { |
88 | 112 |
requires: eexpr list; |
89 |
ensures: ensures_t list; |
|
90 |
behaviors: (string * eexpr list * ensures_t list) list |
|
113 |
ensures: eexpr list; |
|
114 |
behaviors: (string * eexpr list * eexpr list * Location.t) list; |
|
115 |
spec_loc: Location.t; |
|
91 | 116 |
} |
117 |
type assert_t = |
|
118 |
{ |
|
119 |
assert_expr: expr; |
|
120 |
assert_loc: Location.t |
|
121 |
} |
|
122 |
|
|
123 |
type node_desc = |
|
124 |
{node_id: ident; |
|
125 |
mutable node_type: Types.type_expr; |
|
126 |
mutable node_clock: Clocks.clock_expr; |
|
127 |
node_inputs: var_decl list; |
|
128 |
node_outputs: var_decl list; |
|
129 |
node_locals: var_decl list; |
|
130 |
mutable node_gencalls: expr list; |
|
131 |
mutable node_checks: Dimension.dim_expr list; |
|
132 |
node_asserts: assert_t list; |
|
133 |
node_eqs: eq list; |
|
134 |
mutable node_dec_stateless: bool; |
|
135 |
mutable node_stateless: bool option; |
|
136 |
node_spec: node_annot option; |
|
137 |
node_annot: expr_annot list; |
|
138 |
} |
|
139 |
|
|
140 |
type imported_node_desc = |
|
141 |
{nodei_id: ident; |
|
142 |
mutable nodei_type: Types.type_expr; |
|
143 |
mutable nodei_clock: Clocks.clock_expr; |
|
144 |
nodei_inputs: var_decl list; |
|
145 |
nodei_outputs: var_decl list; |
|
146 |
nodei_stateless: bool; |
|
147 |
nodei_spec: node_annot option; |
|
148 |
nodei_prototype: string option; |
|
149 |
nodei_in_lib: string option; |
|
150 |
} |
|
151 |
|
|
152 |
type const_desc = |
|
153 |
{const_id: ident; |
|
154 |
const_loc: Location.t; |
|
155 |
const_value: constant; |
|
156 |
mutable const_type: Types.type_expr; |
|
157 |
} |
|
158 |
|
|
159 |
type top_decl_desc = |
|
160 |
| Node of node_desc |
|
161 |
| Consts of const_desc list |
|
162 |
| ImportedNode of imported_node_desc |
|
163 |
| Open of bool * string (* the boolean set to true denotes a local |
|
164 |
lusi vs a lusi installed at system level *) |
|
165 |
|
|
166 |
type top_decl = |
|
167 |
{top_decl_desc: top_decl_desc; |
|
168 |
top_decl_loc: Location.t} |
|
169 |
|
|
170 |
type program = top_decl list |
|
171 |
|
|
172 |
type error = |
|
173 |
Main_not_found |
|
174 |
| Main_wrong_kind |
|
175 |
| No_main_specified |
|
176 |
| Unbound_symbol of ident |
|
177 |
| Already_bound_symbol of ident |
|
92 | 178 |
|
93 | 179 |
|
94 |
type expr_annot = (string list * eexpr) list |
|
95 |
|
|
96 |
let merge_node_annot ann1 ann2 = |
|
97 |
{ requires = ann1.requires @ ann2.requires; |
|
98 |
ensures = ann1.ensures @ ann2.ensures; |
|
99 |
behaviors = ann1.behaviors @ ann2.behaviors; |
|
100 |
} |
|
101 |
|
|
102 |
let mkeexpr loc d = |
|
103 |
{ eexpr_tag = Utils.new_tag (); |
|
104 |
eexpr_desc = d; |
|
105 |
eexpr_type = Types.new_var (); |
|
106 |
eexpr_clock = Clocks.new_var true; |
|
107 |
eexpr_loc = loc } |
|
108 |
|
|
109 |
let mkepredef_call loc funname args = |
|
110 |
mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None)) |
|
111 |
|
|
112 |
let mkepredef_unary_call loc funname arg = |
|
113 |
mkeexpr loc (EExpr_appl (funname, arg, None)) |
|
114 | 180 |
|
115 | 181 |
(* Local Variables: *) |
116 | 182 |
(* compile-command:"make -C .." *) |
src/machine_code.ml | ||
---|---|---|
99 | 99 |
mstatic: var_decl list; (* static inputs only *) |
100 | 100 |
mstep: step_t; |
101 | 101 |
mspec: node_annot option; |
102 |
mannot: expr_annot option;
|
|
102 |
mannot: expr_annot list;
|
|
103 | 103 |
} |
104 | 104 |
|
105 | 105 |
let pp_step fmt s = |
... | ... | |
170 | 170 |
node_dec_stateless = false; |
171 | 171 |
node_stateless = Some false; |
172 | 172 |
node_spec = None; |
173 |
node_annot = None; }
|
|
173 |
node_annot = []; }
|
|
174 | 174 |
|
175 | 175 |
let arrow_top_decl = |
176 | 176 |
{ |
... | ... | |
202 | 202 |
[MLocalAssign(var_output, LocalVar var_input2)] ] |
203 | 203 |
}; |
204 | 204 |
mspec = None; |
205 |
mannot = None;
|
|
205 |
mannot = [];
|
|
206 | 206 |
} |
207 | 207 |
|
208 | 208 |
let new_instance = |
... | ... | |
229 | 229 |
(* s : step instructions *) |
230 | 230 |
let translate_ident node (m, si, j, d, s) id = |
231 | 231 |
try (* id is a node var *) |
232 |
let var_id = node_var id node in |
|
232 |
let var_id = get_node_var id node in
|
|
233 | 233 |
if ISet.exists (fun v -> v.var_id = id) m |
234 | 234 |
then StateVar var_id |
235 | 235 |
else LocalVar var_id |
... | ... | |
351 | 351 |
(*Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;*) |
352 | 352 |
match eq.eq_lhs, eq.eq_rhs.expr_desc with |
353 | 353 |
| [x], Expr_arrow (e1, e2) -> |
354 |
let var_x = node_var x node in |
|
354 |
let var_x = get_node_var x node in
|
|
355 | 355 |
let o = new_instance node arrow_top_decl eq.eq_rhs.expr_tag in |
356 | 356 |
let c1 = translate_expr node args e1 in |
357 | 357 |
let c2 = translate_expr node args e2 in |
... | ... | |
360 | 360 |
Utils.IMap.add o (arrow_top_decl, []) j, |
361 | 361 |
d, |
362 | 362 |
(control_on_clock node args eq.eq_rhs.expr_clock (MStep ([var_x], o, [c1;c2]))) :: s) |
363 |
| [x], Expr_pre e1 when ISet.mem (node_var x node) d -> |
|
364 |
let var_x = node_var x node in |
|
363 |
| [x], Expr_pre e1 when ISet.mem (get_node_var x node) d ->
|
|
364 |
let var_x = get_node_var x node in
|
|
365 | 365 |
(ISet.add var_x m, |
366 | 366 |
si, |
367 | 367 |
j, |
368 | 368 |
d, |
369 | 369 |
control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e1)) :: s) |
370 |
| [x], Expr_fby (e1, e2) when ISet.mem (node_var x node) d -> |
|
371 |
let var_x = node_var x node in |
|
370 |
| [x], Expr_fby (e1, e2) when ISet.mem (get_node_var x node) d ->
|
|
371 |
let var_x = get_node_var x node in
|
|
372 | 372 |
(ISet.add var_x m, |
373 | 373 |
MStateAssign (var_x, translate_expr node args e1) :: si, |
374 | 374 |
j, |
... | ... | |
376 | 376 |
control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e2)) :: s) |
377 | 377 |
|
378 | 378 |
| p , Expr_appl (f, arg, r) when not (Basic_library.is_internal_fun f) -> |
379 |
let var_p = List.map (fun v -> node_var v node) p in |
|
379 |
let var_p = List.map (fun v -> get_node_var v node) p in
|
|
380 | 380 |
let el = |
381 | 381 |
match arg.expr_desc with |
382 | 382 |
| Expr_tuple el -> el |
... | ... | |
402 | 402 |
| [x], Expr_ite (c, t, e) |
403 | 403 |
when (match !Options.output with | "horn" -> true | "C" | "java" | _ -> false) |
404 | 404 |
-> |
405 |
let var_x = node_var x node in |
|
405 |
let var_x = get_node_var x node in
|
|
406 | 406 |
(m, |
407 | 407 |
si, |
408 | 408 |
j, |
... | ... | |
412 | 412 |
) |
413 | 413 |
|
414 | 414 |
| [x], _ -> ( |
415 |
let var_x = node_var x node in |
|
415 |
let var_x = get_node_var x node in
|
|
416 | 416 |
(m, si, j, d, |
417 | 417 |
control_on_clock |
418 | 418 |
node |
src/main_lustre_compiler.ml | ||
---|---|---|
26 | 26 |
open Format |
27 | 27 |
open Log |
28 | 28 |
|
29 |
open LustreSpec |
|
30 |
|
|
29 | 31 |
let usage = "Usage: lustrec [options] <source-file>" |
30 | 32 |
|
31 | 33 |
let extensions = [".ec"; ".lus"; ".lusi"] |
... | ... | |
170 | 172 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. extracting dependencies@,"); |
171 | 173 |
let dependencies = |
172 | 174 |
List.fold_right |
173 |
(fun d accu -> match d.Corelang.top_decl_desc with
|
|
174 |
| Corelang.Open (local, s) -> (s, local)::accu
|
|
175 |
(fun d accu -> match d.top_decl_desc with |
|
176 |
| Open (local, s) -> (s, local)::accu |
|
175 | 177 |
| _ -> accu) |
176 | 178 |
prog [] |
177 | 179 |
in |
src/normalization.ml | ||
---|---|---|
74 | 74 |
|
75 | 75 |
(* Generate a new local [node] variable *) |
76 | 76 |
let mk_fresh_var node loc ty ck = |
77 |
let vars = node_vars node in |
|
77 |
let vars = get_node_vars node in
|
|
78 | 78 |
let rec aux () = |
79 | 79 |
incr cpt_fresh; |
80 | 80 |
let s = Printf.sprintf "__%s_%d" node.node_id !cpt_fresh in |
... | ... | |
240 | 240 |
let defvars, norm_hl = normalize_branches node offsets defvars hl in |
241 | 241 |
let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in |
242 | 242 |
mk_expr_alias_opt alias node defvars norm_expr |
243 |
| Expr_uclock _ |
|
244 |
| Expr_dclock _ |
|
245 |
| Expr_phclock _ -> assert false (* Not handled yet *) |
|
243 |
|
|
246 | 244 |
(* Creates a conditional with a merge construct, which is more lazy *) |
247 | 245 |
(* |
248 | 246 |
let norm_conditional_as_merge alias node norm_expr offsets defvars expr = |
src/optimize_prog.ml | ||
---|---|---|
1 | 1 |
open Corelang |
2 |
open LustreSpec |
|
2 | 3 |
|
3 | 4 |
(* Consts unfoooolding *) |
4 | 5 |
let is_const i consts = |
... | ... | |
28 | 29 |
| Expr_pre e' -> Expr_pre (unfold e') |
29 | 30 |
| Expr_when (e', i, l)-> Expr_when (unfold e', i, l) |
30 | 31 |
| Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, unfold h)) hl) |
31 |
| Expr_appl (i, e', i') -> Expr_appl (i, unfold e', i') |
|
32 |
| Expr_uclock (e', i) -> Expr_uclock (unfold e', i) |
|
33 |
| Expr_dclock (e', i) -> Expr_dclock (unfold e', i) |
|
34 |
| Expr_phclock _ -> e |
|
32 |
| Expr_appl (i, e', i') -> Expr_appl (i, unfold e', i') |
|
35 | 33 |
|
36 | 34 |
let eq_unfold_consts consts eq = |
37 | 35 |
{ eq with eq_rhs = expr_unfold_consts consts eq.eq_rhs } |
... | ... | |
74 | 72 |
| Expr_when (e', i, l)-> distrib ((i, l)::stack) e' |
75 | 73 |
| Expr_merge (i, hl) -> { expr with expr_desc = Expr_merge (i, List.map (fun (t, h) -> (t, distrib stack h)) hl) } |
76 | 74 |
| Expr_appl (id, e', i') -> { expr with expr_desc = Expr_appl (id, distrib stack e', i')} |
77 |
| _ -> assert false |
|
78 | 75 |
in distrib [] expr |
79 | 76 |
|
80 | 77 |
let eq_distribute_when eq = |
src/parserLustreSpec.mly | ||
---|---|---|
3 | 3 |
open Corelang |
4 | 4 |
open LustreSpec |
5 | 5 |
|
6 |
let mkexpr x = mkexpr (Location.symbol_rloc ()) x |
|
7 |
let mkpredef_call x = mkpredef_call (Location.symbol_rloc ()) x |
|
8 |
let mkpredef_unary_call x = mkpredef_unary_call (Location.symbol_rloc ()) x |
|
9 |
|
|
6 | 10 |
let mkeexpr x = mkeexpr (Location.symbol_rloc ()) x |
11 |
(* |
|
7 | 12 |
let mkepredef_call x = mkepredef_call (Location.symbol_rloc ()) x |
8 | 13 |
let mkepredef_unary_call x = mkepredef_unary_call (Location.symbol_rloc ()) x |
9 |
|
|
14 |
*) |
|
15 |
|
|
10 | 16 |
let mktyp x = mktyp (Location.symbol_rloc ()) x |
11 | 17 |
let mkvar_decl x = mkvar_decl (Location.symbol_rloc ()) x |
12 | 18 |
let mkclock x = mkclock (Location.symbol_rloc ()) x |
... | ... | |
71 | 77 |
|
72 | 78 |
requires: |
73 | 79 |
{ [] } |
74 |
| REQUIRES expr SCOL requires { $2::$4 } |
|
80 |
| REQUIRES qexpr SCOL requires { $2::$4 }
|
|
75 | 81 |
|
76 | 82 |
ensures: |
77 | 83 |
{ [] } |
78 |
| ENSURES expr SCOL ensures { (EnsuresExpr $2) :: $4 } |
|
79 |
| OBSERVER IDENT LPAR tuple_expr RPAR SCOL ensures { (SpecObserverNode($2,$4)) :: $7 } |
|
84 |
| ENSURES qexpr SCOL ensures { (EnsuresExpr $2) :: $4 }
|
|
85 |
| OBSERVER IDENT LPAR tuple_qexpr RPAR SCOL ensures { (SpecObserverNode($2,$4)) :: $7 }
|
|
80 | 86 |
|
81 | 87 |
behaviors: |
82 | 88 |
{ [] } |
... | ... | |
84 | 90 |
|
85 | 91 |
assumes: |
86 | 92 |
{ [] } |
87 |
| ASSUMES expr SCOL assumes { $2::$4 } |
|
93 |
| ASSUMES qexpr SCOL assumes { $2::$4 } |
|
94 |
|
|
95 |
tuple_qexpr: |
|
96 |
| qexpr COMMA qexpr {[$3;$1]} |
|
97 |
| tuple_qexpr COMMA qexpr {$3::$1} |
|
98 |
|
|
88 | 99 |
|
89 | 100 |
tuple_expr: |
90 |
| expr COMMA expr {[$3;$1]}
|
|
101 |
expr COMMA expr {[$3;$1]}
|
|
91 | 102 |
| tuple_expr COMMA expr {$3::$1} |
92 | 103 |
|
104 |
// Same as tuple expr but accepting lists with single element |
|
105 |
array_expr: |
|
106 |
expr {[$1]} |
|
107 |
| expr COMMA array_expr {$1::$3} |
|
108 |
|
|
109 |
dim_list: |
|
110 |
dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) } |
|
111 |
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) } |
|
112 |
|
|
93 | 113 |
expr: |
94 |
| const {mkeexpr (EExpr_const $1)} |
|
95 |
| IDENT |
|
96 |
{mkeexpr (EExpr_ident $1)} |
|
114 |
/* constants */ |
|
115 |
INT {mkexpr (Expr_const (Const_int $1))} |
|
116 |
| REAL {mkexpr (Expr_const (Const_real $1))} |
|
117 |
| FLOAT {mkexpr (Expr_const (Const_float $1))} |
|
118 |
/* Idents or type enum tags */ |
|
119 |
| IDENT { |
|
120 |
if Hashtbl.mem tag_table $1 |
|
121 |
then mkexpr (Expr_const (Const_tag $1)) |
|
122 |
else mkexpr (Expr_ident $1)} |
|
123 |
| LPAR ANNOT expr RPAR |
|
124 |
{update_expr_annot $3 $2} |
|
97 | 125 |
| LPAR expr RPAR |
98 | 126 |
{$2} |
99 | 127 |
| LPAR tuple_expr RPAR |
100 |
{mkeexpr (EExpr_tuple (List.rev $2))} |
|
128 |
{mkexpr (Expr_tuple (List.rev $2))} |
|
129 |
|
|
130 |
/* Array expressions */ |
|
131 |
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) } |
|
132 |
| expr POWER dim { mkexpr (Expr_power ($1, $3)) } |
|
133 |
| expr LBRACKET dim_list { $3 $1 } |
|
134 |
|
|
135 |
/* Temporal operators */ |
|
136 |
| PRE expr |
|
137 |
{mkexpr (Expr_pre $2)} |
|
101 | 138 |
| expr ARROW expr |
102 |
{mkeexpr (EExpr_arrow ($1,$3))}
|
|
139 |
{mkexpr (Expr_arrow ($1,$3))}
|
|
103 | 140 |
| expr FBY expr |
104 |
{mkeexpr (EExpr_fby ($1,$3))} |
|
141 |
{(*mkexpr (Expr_fby ($1,$3))*) |
|
142 |
mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))} |
|
105 | 143 |
| expr WHEN IDENT |
106 |
{mkeexpr (EExpr_when ($1,$3))} |
|
107 |
| MERGE LPAR IDENT COMMA expr COMMA expr RPAR |
|
108 |
{mkeexpr (EExpr_merge ($3,$5,$7))} |
|
144 |
{mkexpr (Expr_when ($1,$3,tag_true))} |
|
145 |
| expr WHENNOT IDENT |
|
146 |
{mkexpr (Expr_when ($1,$3,tag_false))} |
|
147 |
| expr WHEN IDENT LPAR IDENT RPAR |
|
148 |
{mkexpr (Expr_when ($1, $5, $3))} |
|
149 |
| MERGE IDENT handler_expr_list |
|
150 |
{mkexpr (Expr_merge ($2,$3))} |
|
151 |
|
|
152 |
/* Applications */ |
|
109 | 153 |
| IDENT LPAR expr RPAR |
110 |
{mkeexpr (EExpr_appl ($1, $3, None))}
|
|
154 |
{mkexpr (Expr_appl ($1, $3, None))}
|
|
111 | 155 |
| IDENT LPAR expr RPAR EVERY IDENT |
112 |
{mkeexpr (EExpr_appl ($1, $3, Some $6))} |
|
156 |
{mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))} |
|
157 |
| IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR |
|
158 |
{mkexpr (Expr_appl ($1, $3, Some ($8, $6))) } |
|
113 | 159 |
| IDENT LPAR tuple_expr RPAR |
114 |
{mkeexpr (EExpr_appl ($1, mkeexpr (EExpr_tuple (List.rev $3)), None))}
|
|
160 |
{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}
|
|
115 | 161 |
| IDENT LPAR tuple_expr RPAR EVERY IDENT |
116 |
{mkeexpr (EExpr_appl ($1, mkeexpr (EExpr_tuple (List.rev $3)), Some $6)) } |
|
162 |
{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) } |
|
163 |
| IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR |
|
164 |
{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) } |
|
117 | 165 |
|
118 | 166 |
/* Boolean expr */ |
119 | 167 |
| expr AND expr |
120 |
{mkepredef_call "&&" [$1;$3]}
|
|
168 |
{mkpredef_call "&&" [$1;$3]} |
|
121 | 169 |
| expr AMPERAMPER expr |
122 |
{mkepredef_call "&&" [$1;$3]}
|
|
170 |
{mkpredef_call "&&" [$1;$3]} |
|
123 | 171 |
| expr OR expr |
124 |
{mkepredef_call "||" [$1;$3]}
|
|
172 |
{mkpredef_call "||" [$1;$3]} |
|
125 | 173 |
| expr BARBAR expr |
126 |
{mkepredef_call "||" [$1;$3]}
|
|
174 |
{mkpredef_call "||" [$1;$3]} |
|
127 | 175 |
| expr XOR expr |
128 |
{mkepredef_call "xor" [$1;$3]}
|
|
176 |
{mkpredef_call "xor" [$1;$3]} |
|
129 | 177 |
| NOT expr |
130 |
{mkepredef_unary_call "not" $2}
|
|
178 |
{mkpredef_unary_call "not" $2} |
|
131 | 179 |
| expr IMPL expr |
132 |
{mkepredef_call "impl" [$1;$3]}
|
|
180 |
{mkpredef_call "impl" [$1;$3]} |
|
133 | 181 |
|
134 | 182 |
/* Comparison expr */ |
135 | 183 |
| expr EQ expr |
136 |
{mkepredef_call "=" [$1;$3]}
|
|
184 |
{mkpredef_call "=" [$1;$3]} |
|
137 | 185 |
| expr LT expr |
138 |
{mkepredef_call "<" [$1;$3]}
|
|
186 |
{mkpredef_call "<" [$1;$3]} |
|
139 | 187 |
| expr LTE expr |
140 |
{mkepredef_call "<=" [$1;$3]}
|
|
188 |
{mkpredef_call "<=" [$1;$3]} |
|
141 | 189 |
| expr GT expr |
142 |
{mkepredef_call ">" [$1;$3]}
|
|
190 |
{mkpredef_call ">" [$1;$3]} |
|
143 | 191 |
| expr GTE expr |
144 |
{mkepredef_call ">=" [$1;$3]}
|
|
192 |
{mkpredef_call ">=" [$1;$3]} |
|
145 | 193 |
| expr NEQ expr |
146 |
{mkepredef_call "!=" [$1;$3]}
|
|
194 |
{mkpredef_call "!=" [$1;$3]} |
|
147 | 195 |
|
148 | 196 |
/* Arithmetic expr */ |
149 | 197 |
| expr PLUS expr |
150 |
{mkepredef_call "+" [$1;$3]}
|
|
198 |
{mkpredef_call "+" [$1;$3]} |
|
151 | 199 |
| expr MINUS expr |
152 |
{mkepredef_call "-" [$1;$3]}
|
|
200 |
{mkpredef_call "-" [$1;$3]} |
|
153 | 201 |
| expr MULT expr |
154 |
{mkepredef_call "*" [$1;$3]}
|
|
202 |
{mkpredef_call "*" [$1;$3]} |
|
155 | 203 |
| expr DIV expr |
156 |
{mkepredef_call "/" [$1;$3]}
|
|
204 |
{mkpredef_call "/" [$1;$3]} |
|
157 | 205 |
| MINUS expr %prec UMINUS |
158 |
{mkepredef_unary_call "uminus" $2}
|
|
206 |
{mkpredef_unary_call "uminus" $2}
|
|
159 | 207 |
| expr MOD expr |
160 |
{mkepredef_call "mod" [$1;$3]} |
|
161 |
|
|
162 |
/* Temp op */ |
|
163 |
| PRE expr |
|
164 |
{mkeexpr (EExpr_pre $2)} |
|
208 |
{mkpredef_call "mod" [$1;$3]} |
|
165 | 209 |
|
166 | 210 |
/* If */ |
167 | 211 |
| IF expr THEN expr ELSE expr |
168 |
{mkepredef_call "ite" [$2;$4;$6]} |
|
212 |
{mkexpr (Expr_ite ($2, $4, $6))} |
|
213 |
|
|
214 |
|
|
215 |
handler_expr_list: |
|
216 |
{ [] } |
|
217 |
| handler_expr handler_expr_list { $1 :: $2 } |
|
218 |
|
|
219 |
handler_expr: |
|
220 |
LPAR IDENT ARROW expr RPAR { ($2, $4) } |
|
169 | 221 |
|
170 |
/* Quantifiers */ |
|
171 |
| EXISTS vdecl SCOL expr %prec prec_exists {mkeexpr (EExpr_exists ($2, $4))} |
|
172 |
| FORALL vdecl SCOL expr %prec prec_forall {mkeexpr (EExpr_forall ($2, $4))} |
|
222 |
qexpr: |
|
223 |
| expr { mkeexpr [] $1 } |
|
224 |
/* Quantifiers */ |
|
225 |
| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eepxr (Exists, $2) $4 } |
|
226 |
| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eepxr (Forall, $2) $4 } |
|
173 | 227 |
|
174 | 228 |
vdecl: |
175 | 229 |
| ident_list COL typ clock |
... | ... | |
214 | 268 |
|
215 | 269 |
|
216 | 270 |
const: |
217 |
| INT {EConst_int $1}
|
|
218 |
| REAL {EConst_real $1}
|
|
219 |
| FLOAT {EConst_float $1}
|
|
220 |
| TRUE {EConst_bool true}
|
|
221 |
| FALSE {EConst_bool false}
|
|
222 |
| STRING {EConst_string $1}
|
|
271 |
| INT {Const_int $1} |
|
272 |
| REAL {Const_real $1} |
|
273 |
| FLOAT {Const_float $1} |
|
274 |
| TRUE {Const_bool true} |
|
275 |
| FALSE {Const_bool false} |
|
276 |
| STRING {Const_string $1} |
|
223 | 277 |
|
224 | 278 |
lustre_annot: |
225 | 279 |
lustre_annot_list EOF { $1 } |
src/parser_lustre.mly | ||
---|---|---|
26 | 26 |
open Dimension |
27 | 27 |
open Utils |
28 | 28 |
|
29 |
let mktyp x = mktyp (Location.symbol_rloc ()) x |
|
30 |
let mkclock x = mkclock (Location.symbol_rloc ()) x |
|
31 |
let mkvar_decl x = mkvar_decl (Location.symbol_rloc ()) x |
|
32 |
let mkexpr x = mkexpr (Location.symbol_rloc ()) x |
|
33 |
let mkeq x = mkeq (Location.symbol_rloc ()) x |
|
34 |
let mkassert x = mkassert (Location.symbol_rloc ()) x |
|
35 |
let mktop_decl x = mktop_decl (Location.symbol_rloc ()) x |
|
36 |
let mkpredef_call x = mkpredef_call (Location.symbol_rloc ()) x |
|
37 |
|
|
38 |
let mkdim_int i = mkdim_int (Location.symbol_rloc ()) i |
|
39 |
let mkdim_bool b = mkdim_bool (Location.symbol_rloc ()) b |
|
40 |
let mkdim_ident id = mkdim_ident (Location.symbol_rloc ()) id |
|
41 |
let mkdim_appl f args = mkdim_appl (Location.symbol_rloc ()) f args |
|
42 |
let mkdim_ite i t e = mkdim_ite (Location.symbol_rloc ()) i t e |
|
29 |
let get_loc () = Location.symbol_rloc () |
|
30 |
let mktyp x = mktyp (get_loc ()) x |
|
31 |
let mkclock x = mkclock (get_loc ()) x |
|
32 |
let mkvar_decl x = mkvar_decl (get_loc ()) x |
|
33 |
let mkexpr x = mkexpr (get_loc ()) x |
|
34 |
let mkeexpr x = mkeexpr (get_loc ()) x |
|
35 |
let mkeq x = mkeq (get_loc ()) x |
|
36 |
let mkassert x = mkassert (get_loc ()) x |
|
37 |
let mktop_decl x = mktop_decl (get_loc ()) x |
|
38 |
let mkpredef_call x = mkpredef_call (get_loc ()) x |
|
39 |
(*let mkpredef_unary_call x = mkpredef_unary_call (get_loc ()) x*) |
|
40 |
|
|
41 |
let mkdim_int i = mkdim_int (get_loc ()) i |
|
42 |
let mkdim_bool b = mkdim_bool (get_loc ()) b |
|
43 |
let mkdim_ident id = mkdim_ident (get_loc ()) id |
|
44 |
let mkdim_appl f args = mkdim_appl (get_loc ()) f args |
|
45 |
let mkdim_ite i t e = mkdim_ite (get_loc ()) i t e |
|
46 |
|
|
47 |
let mkannots annots = { annots = annots; annot_loc = get_loc () } |
|
43 | 48 |
|
44 | 49 |
let add_node loc own msg hashtbl name value = |
45 | 50 |
try |
46 | 51 |
match (Hashtbl.find hashtbl name).top_decl_desc, value.top_decl_desc with |
47 | 52 |
| Node _ , ImportedNode _ when own -> () |
48 | 53 |
| ImportedNode _, _ -> Hashtbl.add hashtbl name value |
49 |
| Node _ , _ -> raise (Corelang.Error (loc, Corelang.Already_bound_symbol msg))
|
|
54 |
| Node _ , _ -> raise (Error (loc, Already_bound_symbol msg))
|
|
50 | 55 |
| _ -> assert false |
51 | 56 |
with |
52 | 57 |
Not_found -> Hashtbl.add hashtbl name value |
... | ... | |
54 | 59 |
|
55 | 60 |
let add_symbol loc msg hashtbl name value = |
56 | 61 |
if Hashtbl.mem hashtbl name |
57 |
then raise (Corelang.Error (loc, Corelang.Already_bound_symbol msg))
|
|
62 |
then raise (Error (loc, Already_bound_symbol msg))
|
|
58 | 63 |
else Hashtbl.add hashtbl name value |
59 | 64 |
|
60 | 65 |
let check_symbol loc msg hashtbl name = |
61 | 66 |
if not (Hashtbl.mem hashtbl name) |
62 |
then raise (Corelang.Error (loc, Corelang.Unbound_symbol msg))
|
|
67 |
then raise (Error (loc, Unbound_symbol msg))
|
|
63 | 68 |
else () |
64 | 69 |
|
70 |
let check_node_symbol msg name value = |
|
71 |
if Hashtbl.mem node_table name |
|
72 |
then () (* TODO: should we check the types here ? *) |
|
73 |
else Hashtbl.add node_table name value |
|
74 |
|
|
65 | 75 |
%} |
66 | 76 |
|
67 | 77 |
%token <int> INT |
68 | 78 |
%token <string> REAL |
69 | 79 |
%token <float> FLOAT |
80 |
%token <string> STRING |
|
70 | 81 |
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST |
71 | 82 |
%token STATELESS ASSERT OPEN QUOTE FUNCTION |
72 | 83 |
%token <string> IDENT |
... | ... | |
86 | 97 |
%token MULT DIV MOD |
87 | 98 |
%token MINUS PLUS UMINUS |
88 | 99 |
%token PRE ARROW |
100 |
%token REQUIRES ENSURES OBSERVER |
|
101 |
%token INVARIANT BEHAVIOR ASSUMES |
|
102 |
%token EXISTS FORALL |
|
89 | 103 |
%token PROTOTYPE LIB |
90 | 104 |
%token EOF |
91 | 105 |
|
106 |
%nonassoc prec_exists prec_forall |
|
92 | 107 |
%nonassoc COMMA |
93 | 108 |
%left MERGE IF |
94 | 109 |
%nonassoc ELSE |
... | ... | |
110 | 125 |
%nonassoc LBRACKET |
111 | 126 |
|
112 | 127 |
%start prog |
113 |
%type <Corelang.top_decl list> prog |
|
128 |
%type <LustreSpec.top_decl list> prog |
|
129 |
|
|
114 | 130 |
%start header |
115 |
%type <bool -> Corelang.top_decl list> header |
|
131 |
%type <bool -> LustreSpec.top_decl list> header |
|
132 |
|
|
133 |
%start lustre_annot |
|
134 |
%type <LustreSpec.expr_annot> lustre_annot |
|
135 |
|
|
136 |
%start lustre_spec |
|
137 |
%type <LustreSpec.node_annot> lustre_spec |
|
116 | 138 |
|
117 | 139 |
%% |
118 | 140 |
|
... | ... | |
157 | 179 |
nodei_prototype = $13; |
158 | 180 |
nodei_in_lib = $14;}) |
159 | 181 |
in |
160 |
(let loc = Location.symbol_rloc () in |
|
161 |
fun own -> add_node loc own ("node " ^ $3) node_table $3 nd; nd) } |
|
182 |
check_node_symbol ("node " ^ $3) $3 nd; |
|
183 |
let loc = get_loc () in |
|
184 |
(fun own -> add_node loc own ("node " ^ $3) node_table $3 nd; nd) } |
|
162 | 185 |
|
163 | 186 |
prototype_opt: |
164 | 187 |
{ None } |
... | ... | |
186 | 209 |
node_dec_stateless = $2; |
187 | 210 |
node_stateless = None; |
188 | 211 |
node_spec = $1; |
189 |
node_annot = match annots with [] -> None | _ -> Some annots})
|
|
212 |
node_annot = annots}) |
|
190 | 213 |
in |
191 | 214 |
let loc = Location.symbol_rloc () in |
192 | 215 |
add_node loc true ("node " ^ $3) node_table $3 nd; nd} |
193 | 216 |
|
194 | 217 |
nodespec_list: |
195 | 218 |
{ None } |
196 |
| NODESPEC nodespec_list { (function None -> (fun s1 -> Some s1) | Some s2 -> (fun s1 -> Some (LustreSpec.merge_node_annot s1 s2))) $2 $1 } |
|
219 |
| NODESPEC nodespec_list { |
|
220 |
(function |
|
221 |
| None -> (fun s1 -> Some s1) |
|
222 |
| Some s2 -> (fun s1 -> Some (merge_node_annot s1 s2))) $2 $1 } |
|
197 | 223 |
|
198 | 224 |
typ_def_list: |
199 | 225 |
/* empty */ {} |
... | ... | |
203 | 229 |
TYPE IDENT EQ typeconst { |
204 | 230 |
try |
205 | 231 |
let loc = Location.symbol_rloc () in |
206 |
add_symbol loc ("type " ^ $2) type_table (Tydec_const $2) (Corelang.get_repr_type $4)
|
|
232 |
add_symbol loc ("type " ^ $2) type_table (Tydec_const $2) (get_repr_type $4) |
|
207 | 233 |
with Not_found-> assert false } |
208 | 234 |
| TYPE IDENT EQ ENUM LCUR tag_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_enum ($6 (Tydec_const $2))) } |
209 | 235 |
| TYPE IDENT EQ STRUCT LCUR field_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_struct ($6 (Tydec_const $2))) } |
... | ... | |
245 | 271 |
{ [], [], [] } |
246 | 272 |
| eq eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl} |
247 | 273 |
| assert_ eq_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl} |
248 |
| ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1@annotl}
|
|
274 |
| ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}
|
|
249 | 275 |
| automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl} |
250 | 276 |
|
251 | 277 |
automaton: |
... | ... | |
281 | 307 |
ident_list EQ expr SCOL {mkeq (List.rev $1,$3)} |
282 | 308 |
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev $2,$5)} |
283 | 309 |
|
310 |
lustre_spec: |
|
311 |
| contract EOF { $1 } |
|
312 |
|
|
313 |
contract: |
|
314 |
requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; spec_loc = get_loc () } } |
|
315 |
|
|
316 |
requires: |
|
317 |
{ [] } |
Also available in: Unified diff