diff --git a/src/clocks.ml b/src/clocks.ml
index 1197b584cebd0fa5897eb93e0849d1f0ef536525..ec734ffd952c437361c2107f1b18a9350b9d0fac 100755
--- a/src/clocks.ml
+++ b/src/clocks.ml
@@ -72,6 +72,55 @@ exception Scope_carrier of carrier_expr
exception Scope_clock of clock_expr
exception Error of Location.t * error
+let print_ckset fmt s =
+ match s with
+ | CSet_all -> ()
+ | CSet_pck (k,q) ->
+ let (a,b) = simplify_rat q in
+ if k = 1 && a = 0 then
+ fprintf fmt "<:P"
+ else
+ fprintf fmt "<:P_(%i,%a)" k print_rat (a,b)
+
+let rec print_carrier fmt cr =
+ (* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt -> *)
+ match cr.carrier_desc with
+ | Carry_const id -> fprintf fmt "%s" id
+ | Carry_name ->
+ fprintf fmt "_%s" (name_of_carrier cr.carrier_id)
+ | Carry_var ->
+ fprintf fmt "'%s" (name_of_carrier cr.carrier_id)
+ | Carry_link cr' ->
+ print_carrier fmt cr'
+
+(* Simple pretty-printing, performs no simplifications. Linear
+ complexity. For debug mainly. *)
+let rec print_ck_long fmt ck =
+ match ck.cdesc with
+ | Carrow (ck1,ck2) ->
+ fprintf fmt "%a->%a" print_ck_long ck1 print_ck_long ck2
+ | Ctuple cklist ->
+ fprintf fmt "(%a)"
+ (fprintf_list ~sep:" * " print_ck_long) cklist
+ | Con (ck,c,l) ->
+ fprintf fmt "%a on %s(%a)" print_ck_long ck l print_carrier c
+ | Pck_up (ck,k) ->
+ fprintf fmt "%a*^%i" print_ck_long ck k
+ | Pck_down (ck,k) ->
+ fprintf fmt "%a/^%i" print_ck_long ck k
+ | Pck_phase (ck,q) ->
+ fprintf fmt "%a~>%a" print_ck_long ck print_rat (simplify_rat q)
+ | Pck_const (n,p) ->
+ fprintf fmt "(%i,%a)" n print_rat (simplify_rat p)
+ | Cvar cset ->
+ fprintf fmt "'_%i%a" ck.cid print_ckset cset
+ | Cunivar cset ->
+ fprintf fmt "'%i%a" ck.cid print_ckset cset
+ | Clink ck' ->
+ fprintf fmt "link %a" print_ck_long ck'
+ | Ccarrying (cr,ck') ->
+ fprintf fmt "(%a:%a)" print_carrier cr print_ck_long ck'
+
let new_id = ref (-1)
let new_ck desc scoped =
@@ -117,6 +166,17 @@ let get_carrier_name ck =
| Ccarrying (cr, _) -> Some cr
| _ -> None
+let rename_carrier_static rename cr =
+ match (carrier_repr cr).carrier_desc with
+ | Carry_const id -> { cr with carrier_desc = Carry_const (rename id) }
+ | _ -> (Format.eprintf "internal error: Clocks.rename_carrier_static %a@." print_carrier cr; assert false)
+
+let rec rename_static rename ck =
+ match (repr ck).cdesc with
+ | Ccarrying (cr, ck') -> { ck with cdesc = Ccarrying (rename_carrier_static rename cr, rename_static rename ck') }
+ | Con (ck', cr, l) -> { ck with cdesc = Con (rename_static rename ck', rename_carrier_static rename cr, l) }
+ | _ -> ck
+
let uncarrier ck =
match ck.cdesc with
| Ccarrying (_, ck') -> ck'
@@ -257,55 +317,6 @@ let rec constrained_vars_of_clock ck =
in
aux [] ck
-let print_ckset fmt s =
- match s with
- | CSet_all -> ()
- | CSet_pck (k,q) ->
- let (a,b) = simplify_rat q in
- if k = 1 && a = 0 then
- fprintf fmt "<:P"
- else
- fprintf fmt "<:P_(%i,%a)" k print_rat (a,b)
-
-let rec print_carrier fmt cr =
- (* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt -> *)
- match cr.carrier_desc with
- | Carry_const id -> fprintf fmt "%s" id
- | Carry_name ->
- fprintf fmt "_%s" (name_of_carrier cr.carrier_id)
- | Carry_var ->
- fprintf fmt "'%s" (name_of_carrier cr.carrier_id)
- | Carry_link cr' ->
- print_carrier fmt cr'
-
-(* Simple pretty-printing, performs no simplifications. Linear
- complexity. For debug mainly. *)
-let rec print_ck_long fmt ck =
- match ck.cdesc with
- | Carrow (ck1,ck2) ->
- fprintf fmt "%a->%a" print_ck_long ck1 print_ck_long ck2
- | Ctuple cklist ->
- fprintf fmt "(%a)"
- (fprintf_list ~sep:" * " print_ck_long) cklist
- | Con (ck,c,l) ->
- fprintf fmt "%a on %s(%a)" print_ck_long ck l print_carrier c
- | Pck_up (ck,k) ->
- fprintf fmt "%a*^%i" print_ck_long ck k
- | Pck_down (ck,k) ->
- fprintf fmt "%a/^%i" print_ck_long ck k
- | Pck_phase (ck,q) ->
- fprintf fmt "%a~>%a" print_ck_long ck print_rat (simplify_rat q)
- | Pck_const (n,p) ->
- fprintf fmt "(%i,%a)" n print_rat (simplify_rat p)
- | Cvar cset ->
- fprintf fmt "'_%i%a" ck.cid print_ckset cset
- | Cunivar cset ->
- fprintf fmt "'%i%a" ck.cid print_ckset cset
- | Clink ck' ->
- fprintf fmt "link %a" print_ck_long ck'
- | Ccarrying (cr,ck') ->
- fprintf fmt "(%a:%a)" print_carrier cr print_ck_long ck'
-
(** [period ck] returns the period of [ck]. Expects a constant pclock
expression belonging to the correct clock set. *)
let rec period ck =
diff --git a/src/corelang.ml b/src/corelang.ml
index b7a89dbbb4769cc0d255c49af523e29517b85889..973f44decd5728b7bde260434d8c38e6ad8d55e5 100755
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -376,6 +376,16 @@ let ident_of_expr expr =
| Expr_ident id -> id
| _ -> assert false
+(* Generate a new ident expression from a declared variable *)
+let expr_of_vdecl v =
+ { expr_tag = Utils.new_tag ();
+ expr_desc = Expr_ident v.var_id;
+ expr_type = v.var_type;
+ expr_clock = v.var_clock;
+ expr_delay = Delay.new_var ();
+ expr_annot = None;
+ expr_loc = v.var_loc }
+
(* Caution, returns an untyped and unclocked expression *)
let expr_of_ident id loc =
{expr_tag = Utils.new_tag ();
@@ -429,7 +439,7 @@ let rec expr_of_dimension dim =
mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None))
| Dlink dim' -> expr_of_dimension dim'
| Dvar
- | Dunivar -> (Format.eprintf "internal error: expr_of_dimension %a@." Dimension.pp_dimension dim;
+ | Dunivar -> (Format.eprintf "internal error: Corelang.expr_of_dimension %a@." Dimension.pp_dimension dim;
assert false)
let dimension_of_const loc const =
@@ -478,6 +488,11 @@ let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with
let get_node_vars nd =
nd.node_inputs @ nd.node_locals @ nd.node_outputs
+let mk_new_node_name nd id =
+ let used_vars = get_node_vars nd in
+ let used v = List.exists (fun vdecl -> vdecl.var_id = v) used_vars in
+ mk_new_name used id
+
let get_var id var_list =
List.find (fun v -> v.var_id = id) var_list
diff --git a/src/corelang.mli b/src/corelang.mli
index 7c7ebe3d20fc12f8b1b22465d9a9b632bb0fda66..a0eaa6cf253498016d8ad39d2c6c9861cb7850c8 100755
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -27,7 +27,7 @@ val mkassert: Location.t -> expr -> assert_t
val mktop_decl: Location.t -> ident -> bool -> top_decl_desc -> top_decl
val mkpredef_call: Location.t -> ident -> expr list -> expr
val mk_new_name: (ident -> bool) -> ident -> ident
-
+val mk_new_node_name: node_desc -> ident -> ident
val node_table : (ident, top_decl) Hashtbl.t
val print_node_table: Format.formatter -> unit -> unit
@@ -81,6 +81,7 @@ val pp_error : Format.formatter -> error -> unit
(* Caution, returns an untyped, unclocked, etc, expression *)
val is_tuple_expr : expr -> bool
val ident_of_expr : expr -> ident
+val expr_of_vdecl : var_decl -> expr
val expr_of_ident : ident -> Location.t -> expr
val expr_list_of_expr : expr -> expr list
val expr_of_expr_list : Location.t -> expr list -> expr
diff --git a/src/dimension.ml b/src/dimension.ml
index d61f2fb3315c5fb09e8849d4fd3c996648d2fc3b..e703905ac52fce6ca6e88e5b5208e817936236f5 100644
--- a/src/dimension.ml
+++ b/src/dimension.ml
@@ -339,8 +339,8 @@ let unify ?(semi=false) dim1 dim2 =
in unif dim1 dim2
let rec expr_replace_var fvar e =
- { e with dim_desc = expr_replace_desc fvar e.dim_desc }
-and expr_replace_desc fvar e =
+ { e with dim_desc = expr_replace_var_desc fvar e.dim_desc }
+and expr_replace_var_desc fvar e =
let re = expr_replace_var fvar in
match e with
| Dvar
@@ -351,3 +351,17 @@ and expr_replace_desc fvar e =
| Dappl (id, el) -> Dappl (id, List.map re el)
| Dite (g,t,e) -> Dite (re g, re t, re e)
| Dlink e -> Dlink (re e)
+
+let rec expr_replace_expr fvar e =
+ { e with dim_desc = expr_replace_expr_desc fvar e.dim_desc }
+and expr_replace_expr_desc fvar e =
+ let re = expr_replace_expr fvar in
+ match e with
+ | Dvar
+ | Dunivar
+ | Dbool _
+ | Dint _ -> e
+ | Dident v -> (fvar v).dim_desc
+ | Dappl (id, el) -> Dappl (id, List.map re el)
+ | Dite (g,t,e) -> Dite (re g, re t, re e)
+ | Dlink e -> Dlink (re e)
diff --git a/src/inliner.ml b/src/inliner.ml
index 0756ee85ac9358f5a84039be706a2509abed124b..29b008baef787c49cd3e3bff0c9171aa318cc37f 100644
--- a/src/inliner.ml
+++ b/src/inliner.ml
@@ -27,8 +27,27 @@ let check_node_name id = (fun t ->
| Node nd -> nd.node_id = id
| _ -> false)
+let get_static_inputs node args =
+ List.fold_right2 (fun vdecl arg static ->
+ if vdecl.var_dec_const then (vdecl.var_id, Corelang.dimension_of_expr arg) :: static else static)
+ node.node_inputs
+ (Corelang.expr_list_of_expr args)
+ []
+
+let get_carrier_inputs node args =
+ List.fold_right2 (fun vdecl arg carrier ->
+ if Types.get_clock_base_type vdecl.var_type <> None then (vdecl.var_id, ident_of_expr arg) :: carrier else carrier)
+ node.node_inputs
+ (Corelang.expr_list_of_expr args)
+ []
+
+let is_node_var node v =
+ try
+ ignore (Corelang.get_node_var v node); true
+ with Not_found -> false
let rename_expr rename expr = expr_replace_var rename expr
+
let rename_eq rename eq =
{ eq with
eq_lhs = List.map rename eq.eq_lhs;
@@ -36,7 +55,7 @@ let rename_eq rename eq =
}
(*
- expr, locals', eqs = inline_call id args' reset locals nodes
+ expr, locals', eqs = inline_call id args' reset locals node nodes
We select the called node equations and variables.
renamed_inputs = args
@@ -47,22 +66,37 @@ the resulting expression is tuple_of_renamed_outputs
TODO: convert the specification/annotation/assert and inject them
TODO: deal with reset
*)
-let inline_call orig_expr args reset locals node =
+let inline_call node orig_expr args reset locals caller =
let loc = orig_expr.expr_loc in
let uid = orig_expr.expr_tag in
let rename v =
- if v = tag_true || v = tag_false then v else
- (Format.fprintf Format.str_formatter "%s_%i_%s"
- node.node_id uid v;
- Format.flush_str_formatter ())
+ if v = tag_true || v = tag_false || not (is_node_var node v) then v else
+ Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v)
in
let eqs' = List.map (rename_eq rename) (get_node_eqs node)
in
- let rename_var v = { v with var_id = rename v.var_id } in
+ let static_inputs = get_static_inputs node args in
+ let carrier_inputs = get_carrier_inputs node args in
+ let rename_static v =
+ try
+ List.assoc v static_inputs
+ with Not_found -> Dimension.mkdim_ident loc v
+ (*Format.eprintf "Inliner.rename_static %s = %a@." v Dimension.pp_dimension res; res*)
+ in
+ let rename_carrier v =
+ try
+ List.assoc v carrier_inputs
+ with Not_found -> v in
+ let rename_var v =
+ (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
+ { v with
+ var_id = rename v.var_id;
+ var_type = Types.rename_static rename_static v.var_type;
+ var_clock = Clocks.rename_static rename_carrier v.var_clock;
+ } in
let inputs' = List.map rename_var node.node_inputs in
let outputs' = List.map rename_var node.node_outputs in
let locals' = List.map rename_var node.node_locals in
-
(* checking we are at the appropriate (early) step: node_checks and
node_gencalls should be empty (not yet assigned) *)
assert (node.node_checks = []);
@@ -72,9 +106,7 @@ let inline_call orig_expr args reset locals node =
assert (reset = None);
let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', args) in
- let expr = expr_of_expr_list
- loc
- (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) outputs')
+ let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs')
in
let asserts' = (* We rename variables in assert expressions *)
List.map
@@ -92,20 +124,21 @@ let inline_call orig_expr args reset locals node =
+let inline_table = Hashtbl.create 23
(*
- new_expr, new_locals, new_eqs = inline_expr expr locals nodes
+ new_expr, new_locals, new_eqs = inline_expr expr locals node nodes
Each occurence of a node in nodes in the expr should be replaced by fresh
variables and the code of called node instance added to new_eqs
*)
-let rec inline_expr ?(selection_on_annotation=false) expr locals nodes =
+let rec inline_expr ?(selection_on_annotation=false) expr locals node nodes =
let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in
let inline_tuple el =
List.fold_right (fun e (el_tail, locals, eqs, asserts) ->
- let e', locals', eqs', asserts' = inline_expr e locals nodes in
+ let e', locals', eqs', asserts' = inline_expr e locals node nodes in
e'::el_tail, locals', eqs'@eqs, asserts@asserts'
) el ([], locals, [], [])
in
@@ -124,20 +157,20 @@ let rec inline_expr ?(selection_on_annotation=false) expr locals nodes =
match expr.expr_desc with
| Expr_appl (id, args, reset) ->
- let args', locals', eqs', asserts' = inline_expr args locals nodes in
+ let args', locals', eqs', asserts' = inline_expr args locals node nodes in
if List.exists (check_node_name id) nodes && (* the current node call is provided
as arguments nodes *)
(not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated,
it is explicitely inlined here *)
then
(* The node should be inlined *)
- let _ = Format.eprintf "Inlining call to %s@." id in
- let node = try List.find (check_node_name id) nodes
+ (* let _ = Format.eprintf "Inlining call to %s@." id in *)
+ let called = try List.find (check_node_name id) nodes
with Not_found -> (assert false) in
- let node = node_of_top node in
- let node = inline_node node nodes in
+ let called = node_of_top called in
+ let called' = inline_node called nodes in
let expr, locals', eqs'', asserts'' =
- inline_call expr args' reset locals' node in
+ inline_call called' expr args' reset locals' node in
expr, locals', eqs'@eqs'', asserts'@asserts''
else
(* let _ = Format.eprintf "Not inlining call to %s@." id in *)
@@ -165,36 +198,46 @@ let rec inline_expr ?(selection_on_annotation=false) expr locals nodes =
let el', l', eqs', asserts' = inline_tuple el in
{ expr with expr_desc = Expr_array el' }, l', eqs', asserts'
| Expr_access (e, dim) ->
- let e', l', eqs', asserts' = inline_expr e locals nodes in
+ let e', l', eqs', asserts' = inline_expr e locals node nodes in
{ expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts'
| Expr_power (e, dim) ->
- let e', l', eqs', asserts' = inline_expr e locals nodes in
+ let e', l', eqs', asserts' = inline_expr e locals node nodes in
{ expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts'
| Expr_pre e ->
- let e', l', eqs', asserts' = inline_expr e locals nodes in
+ let e', l', eqs', asserts' = inline_expr e locals node nodes in
{ expr with expr_desc = Expr_pre e' }, l', eqs', asserts'
| Expr_when (e, id, label) ->
- let e', l', eqs', asserts' = inline_expr e locals nodes in
+ let e', l', eqs', asserts' = inline_expr e locals node nodes in
{ expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts'
| Expr_merge (id, branches) ->
let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in
let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts'
-and inline_node ?(selection_on_annotation=false) nd nodes =
+
+and inline_node ?(selection_on_annotation=false) node nodes =
+ try Hashtbl.find inline_table node.node_id
+ with Not_found ->
let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
let new_locals, eqs, asserts =
List.fold_left (fun (locals, eqs, asserts) eq ->
let eq_rhs', locals', new_eqs', asserts' =
- inline_expr eq.eq_rhs locals nodes
+ inline_expr eq.eq_rhs locals node nodes
in
locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts
- ) (nd.node_locals, [], nd.node_asserts) (get_node_eqs nd)
+ ) (node.node_locals, [], node.node_asserts) (get_node_eqs node)
in
- { nd with
+ let inlined =
+ { node with
node_locals = new_locals;
node_stmts = List.map (fun eq -> Eq eq) eqs;
node_asserts = asserts;
}
+ in
+ begin
+ (*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*)
+ Hashtbl.add inline_table node.node_id inlined;
+ inlined
+ end
let inline_all_calls node nodes =
let nd = match node.top_decl_desc with Node nd -> nd | _ -> assert false in
@@ -299,6 +342,7 @@ let witness filename main_name orig inlined type_env clock_env =
in
let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in
let new_prog = others@nodes_origs@nodes_inlined@main in
+
let _ = Typing.type_prog type_env new_prog in
let _ = Clock_calculus.clock_prog clock_env new_prog in
diff --git a/src/main_lustre_compiler.ml b/src/main_lustre_compiler.ml
index bfa11970a0175617f57ac01f5043216e453e3ce3..0ce60512414cf2533e9adcc331038f445e57cf03 100644
--- a/src/main_lustre_compiler.ml
+++ b/src/main_lustre_compiler.ml
@@ -123,15 +123,6 @@ let rec compile_source dirname basename extension =
exit 0
end;
- (* Perform global inlining *)
- let prog =
- if !Options.global_inline &&
- (match !Options.main_node with | "" -> false | _ -> true) then
- Inliner.global_inline basename prog type_env clock_env
- else (* if !Option.has_local_inline *)
- Inliner.local_inline basename prog type_env clock_env
- in
-
(* Delay calculus *)
(* TO BE DONE LATER (Xavier)
if(!Options.delay_calculus)
@@ -159,6 +150,15 @@ let rec compile_source dirname basename extension =
Typing.uneval_prog_generics prog;
Clock_calculus.uneval_prog_generics prog;
+ (* Perform global inlining *)
+ let prog =
+ if !Options.global_inline &&
+ (match !Options.main_node with | "" -> false | _ -> true) then
+ Inliner.global_inline basename prog type_env clock_env
+ else (* if !Option.has_local_inline *)
+ Inliner.local_inline basename prog type_env clock_env
+ in
+(*Format.eprintf "Inliner.global_inline<<@.%a@.>>@." Printers.pp_prog prog;*)
(* Computes and stores generic calls for each node,
only useful for ANSI C90 compliant generic node compilation *)
if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
@@ -170,6 +170,7 @@ let rec compile_source dirname basename extension =
if !Options.output = "lustre" then
Normalization.unfold_arrow_active := false;
let prog = Normalization.normalize_prog prog in
+
Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
(* Checking array accesses *)
if !Options.check then
diff --git a/src/normalization.ml b/src/normalization.ml
index 666c7973e010f4ac7213d7d4ab2743890b6bec8b..cd4be955b66233131e784855aa33b74cc66a0883 100644
--- a/src/normalization.ml
+++ b/src/normalization.ml
@@ -75,16 +75,6 @@ let mk_fresh_var node loc ty ck =
}
in aux ()
-(* Generate a new ident expression from a declared variable *)
-let mk_ident_expr v =
- { expr_tag = new_tag ();
- expr_desc = Expr_ident v.var_id;
- expr_type = v.var_type;
- expr_clock = v.var_clock;
- expr_delay = Delay.new_var ();
- expr_annot = None;
- expr_loc = v.var_loc }
-
(* Get the equation in [defs] with [expr] as rhs, if any *)
let get_expr_alias defs expr =
try Some (List.find (fun eq -> is_eq_expr eq.eq_rhs expr) defs)
@@ -100,16 +90,19 @@ let replace_expr locals expr =
expr_desc = Expr_ident v.var_id }
| _ -> { expr with
expr_tag = Utils.new_tag ();
- expr_desc = Expr_tuple (List.map mk_ident_expr locals) }
+ expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }
let unfold_offsets e offsets =
let add_offset e d =
-(*Format.eprintf "add_offset %a %a@." Dimension.pp_dimension (Types.array_type_dimension e.expr_type) Dimension.pp_dimension d;*)
+(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d;
+ let res = *)
{ e with
expr_tag = Utils.new_tag ();
expr_loc = d.Dimension.dim_loc;
expr_type = Types.array_element_type e.expr_type;
- expr_desc = Expr_access (e, d) } in
+ expr_desc = Expr_access (e, d) }
+(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
+ in
List.fold_left add_offset e offsets
(* Create an alias for [expr], if none exists yet *)
@@ -128,7 +121,7 @@ let mk_expr_alias node (defs, vars) expr =
let new_def =
mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
in
- (* Format.eprintf "Checkign def of alias: %a -> %a@." (fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) new_aliases Printers.pp_expr expr; *)
+ (* Format.eprintf "Checking def of alias: %a -> %a@." (fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) new_aliases Printers.pp_expr expr; *)
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
@@ -149,6 +142,7 @@ let mk_expr_alias_opt opt node defvars expr =
taking propagated [offsets] into account
in order to change expression type *)
let mk_norm_expr offsets ref_e norm_d =
+(*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*)
let drop_array_type ty =
Types.map_tuple_type Types.array_element_type ty in
{ ref_e with
@@ -301,7 +295,7 @@ let decouple_outputs node defvars eq =
if List.exists (fun o -> o.var_id = v) node.node_outputs
then
let newvar = mk_fresh_var node eq.eq_loc t c in
- let neweq = mkeq eq.eq_loc ([v], mk_ident_expr newvar) in
+ let neweq = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in
(neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q
else
(defs_q, vars_q), v::lhs_q
diff --git a/src/types.ml b/src/types.ml
index 04d17a74c92ab151fff36a40c5f4900499e69c12..7b13fa4ed5918f3ef93abb782961c5c60536e371 100755
--- a/src/types.ml
+++ b/src/types.ml
@@ -193,6 +193,13 @@ let get_static_value ty =
| Tstatic (d, _) -> Some d
| _ -> None
+let rec rename_static rename ty =
+ match (repr ty).tdesc with
+ | Tstatic (d, ty') -> { ty with tdesc = Tstatic (Dimension.expr_replace_expr rename d, rename_static rename ty') }
+ | Tarray (d, ty') -> { ty with tdesc = Tarray (Dimension.expr_replace_expr rename d, rename_static rename ty') }
+ | _ -> ty
+(*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*)
+
let get_field_type ty label =
match (repr ty).tdesc with
| Tstruct fl -> (try Some (List.assoc label fl) with Not_found -> None)
@@ -254,7 +261,7 @@ let rec is_array_type ty =
let array_type_dimension ty =
match (dynamic_type ty).tdesc with
| Tarray (d, _) -> d
- | _ -> assert false
+ | _ -> (Format.eprintf "internal error: Types.array_type_dimension %a@." print_ty ty; assert false)
let rec array_type_multi_dimension ty =
match (dynamic_type ty).tdesc with
@@ -264,7 +271,7 @@ let rec array_type_multi_dimension ty =
let array_element_type ty =
match (dynamic_type ty).tdesc with
| Tarray (_, ty') -> ty'
- | _ -> assert false
+ | _ -> (Format.eprintf "internal error: Types.array_element_type %a@." print_ty ty; assert false)
let rec array_base_type ty =
let ty = repr ty in
diff --git a/src/typing.ml b/src/typing.ml
index 3321c1239dea24c3d98d6c36760ce43f2e2fdf24..5545ddc7fe7815618cd205d437057394639b5529 100755
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -566,6 +566,7 @@ let rec check_type_declaration loc cty =
| _ -> ()
let type_var_decl vd_env env vdecl =
+(*Format.eprintf "Typing.type_var_decl START %a@." Printers.pp_var vdecl;*)
check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
let eval_const id = Types.get_static_value (Env.lookup_value env id) in
let type_dim d =
@@ -581,6 +582,7 @@ let type_var_decl vd_env env vdecl =
let new_env = Env.add_value env vdecl.var_id ty_status in
type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
vdecl.var_type <- ty_status;
+(*Format.eprintf "END@.";*)
new_env
let type_var_decl_list vd_env env l =
diff --git a/test/test-compile.sh b/test/test-compile.sh
index a9e2f3fef295675208bc6fe924d6774a5da524be..ceafcdd05e5c58cd76f85a3f8f96b010c283cf8d 100755
--- a/test/test-compile.sh
+++ b/test/test-compile.sh
@@ -14,6 +14,23 @@ LUSTREC=lustrec
mkdir -p build
build=`pwd`"/build"
+gcc_compile() {
+ gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$1".c > /dev/null;
+ if [ $? -ne 0 ]; then
+ rgcc="INVALID";
+ else
+ rgcc="VALID"
+ fi
+}
+
+lustrec_compile() {
+ $LUSTREC "$@";
+ if [ $? -ne 0 ]; then
+ rlustrec="INVALID";
+ else
+ rlustrec="VALID"
+ fi
+}
base_compile() {
while IFS=, read -r file main opts
@@ -26,51 +43,27 @@ base_compile() {
fi
dir=${SRC_PREFIX}/`dirname "$file"`
pushd $dir > /dev/null
- if [ "$main" != "" ]; then
- $LUSTREC -d $build -verbose 0 $opts -node $main "$name""$ext";
- if [ $? -ne 0 ]; then
- rlustrec1="INVALID";
- else
- rlustrec1="VALID"
- fi
- pushd $build > /dev/null
- if [ $ext = ".lus" ]; then
- gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
- if [ $? -ne 0 ]; then
- rgcc1="INVALID";
- else
- rgcc1="VALID"
- fi
+
+ if [ "$main" != "" ]; then
+ lustrec_compile -d $build -verbose 0 $opts -node $main $name$ext;
else
- rgcc1="NONE"
+ lustrec_compile -d $build -verbose 0 $opts $name$ext
fi
- popd > /dev/null
- else
- $LUSTREC -d $build -verbose 0 $opts "$name""$ext";
- if [ $? -ne 0 ]; then
- rlustrec1="INVALID";
- else
- rlustrec1="VALID"
- fi
pushd $build > /dev/null
+
if [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
- gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
- if [ $? -ne 0 ]; then
- rgcc1="INVALID";
- else
- rgcc1="VALID"
- fi
+ gcc_compile "$name";
else
- rgcc1="NONE"
+ rgcc="NONE"
fi
popd > /dev/null
- fi
- popd > /dev/null
- if [ $verbose -gt 0 ]; then
- echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
- else
- echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
- fi;
+ popd > /dev/null
+
+ if [ $verbose -gt 0 ]; then
+ echo "lustrec ($rlustrec), gcc($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
+ else
+ echo "lustrec ($rlustrec), gcc($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
+ fi;
done < $file_list
}
@@ -78,35 +71,40 @@ inline_compile () {
while IFS=, read -r file main opts
do
name=`basename "$file" .lus`
+ ext=".lus"
if [ `dirname "$file"`/"$name" = "$file" ]; then
- return 0
+ name=`basename "$file" .lusi`
+ ext=".lusi"
fi
dir=${SRC_PREFIX}/`dirname "$file"`
-
pushd $dir > /dev/null
-# Checking inlining
- $LUSTREC -d $build -verbose 0 $opts -inline -witnesses -node $main "$name".lus;
- if [ $? -ne 0 ]; then
- rlustrec2="INVALID";
- else
- rlustrec2="VALID"
- fi
- pushd $build > /dev/null
- gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
- if [ $? -ne 0 ]; then
- rgcc2="INVALID";
- else
- rgcc2="VALID"
- fi
- popd > /dev/null
- if [ $verbose -gt 0 ]; then
- echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
- else
- echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
- fi;
- popd > /dev/null
-done < $file_list
+ if [ "$main" != "" ]; then
+ lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name$ext;
+ else
+ if [ "$ext" = ".lusi" ]; then
+ lustrec_compile -d $build -verbose 0 $opts $name$ext;
+ else
+ rlustrec="NONE"
+ rgcc="NONE"
+ fi
+ fi
+ pushd $build > /dev/null
+
+ if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
+ gcc_compile "$name";
+ else
+ rgcc="NONE"
+ fi
+ popd > /dev/null
+ popd > /dev/null
+
+ if [ $verbose -gt 0 ]; then
+ echo "lustrec inlined ($rlustrec), gcc ($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
+ else
+ echo "lustrec inlined ($rlustrec), gcc ($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
+ fi;
+ done < $file_list
}
inline_compile_with_check () {
@@ -119,23 +117,15 @@ inline_compile_with_check () {
fi
dir=${SRC_PREFIX}/`dirname "$file"`
pushd $dir > /dev/null
- $LUSTREC -d $build -verbose 0 $opts -inline -witnesses -node $main "$name".lus;
- if [ $? -ne 0 ]; then
- rlustrec2="INVALID";
- else
- rlustrec2="VALID"
- fi
+ lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name".lus"
+
pushd $build > /dev/null
- gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
- if [ $? -ne 0 ]; then
- rgcc2="INVALID";
- else
- rgcc2="VALID"
- fi
+ gcc_compile "$name"
+
popd > /dev/null
# Cheching witness
pushd $build > /dev/null
- $LUSTREC -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus
+ lustrec_compile -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus
popd > /dev/null
z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"
if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
@@ -148,9 +138,9 @@ inline_compile_with_check () {
rinlining="INVALID/TIMEOUT"
fi
if [ $verbose -gt 0 ]; then
- echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
+ echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
else
- echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
+ echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
fi
popd > /dev/null
done < $file_list
@@ -169,15 +159,11 @@ check_prop () {
# Checking horn backend
if [ "$main" != "" ]; then
- $LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main "$name".lus;
+ lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main $name".lus";
else
- $LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts "$name".lus
- fi
- if [ $? -ne 0 ]; then
- rlustrec="INVALID";
- else
- rlustrec="VALID"
+ lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts $name".lus"
fi
+
# echo "z3 $build/$name".smt2
# TODO: This part of the script has to be optimized
z3 -T:10 "$build/$name".smt2 | grep unsat > /dev/null
@@ -231,6 +217,12 @@ if [ ${#files} -eq 0 ] ; then
exit 1
fi
+# cleaning directory $build
+
+rm -f "$build"/* 2> /dev/null
+
+# executing tests
+
[ ! -z "$c" ] && base_compile
[ ! -z "$i" ] && inline_compile
[ ! -z "$w" ] && inline_compile_with_check
diff --git a/test/tests_ok.list b/test/tests_ok.list
index 0d2a2b8c26f43ad97ab063e7e150d278799b7d5f..b8264891ddf957cf81be39542f0570bc64b59a15 100644
--- a/test/tests_ok.list
+++ b/test/tests_ok.list
@@ -904,7 +904,6 @@
./tests/arrays_arnaud/generic1.lusi
./tests/arrays_arnaud/generic1.lus
./tests/arrays_arnaud/generic2.lus
-./tests/arrays_arnaud/generic3.lus,top,-dynamic -check-access
./tests/clocks/clocks1.lus,,-lusi
./tests/clocks/clocks1.lusi
./tests/clocks/clocks1.lus