Newer
Older
(** Time-stamp: <modified the 26/05/2009 (at 10:14) by Erwan Jahier> *)
open Predef
open PredefEvalConst
open SyntaxTree
open SyntaxTreeCore
open Printf
open Lxm
open Errors
(**
** Foreword.
The clock mechanism of Lustre is a simple kind of type dependant
system. Indeed, clocks depend on program variables. More
precisely, and according to Pouzet&Colaco [emsoft03], the clock
type system of Lustre is equivalent to a "firt class abstract
type system".
Note however that here, things are simpler than in emsoft03,
since we are not interested in type reconstruction (or
inference), but only in checking types are provided in node
headers.
** clock checking of expression.
nb:
In the following, we speak about input/output arguments/parameters of an
expression because:
- the difficult case wrt clock checking concerns nodes
- other kind of expressions can be seen as nodes, as they take some input
arguments, and return some outputs.
The clock checking consists in verifying that expression arguments clocks
are compatible with the expression parameters clocks.
For instance, for a node of profile:
node toto(a; b when a) returns (x when a; y when x);
when it is called, e.g., like that:
(v1,v2) = toto(v3,v4);
we need to check that:
- the argument clocks are ok, i.e., v4 is on v3 (1)
cf the [check_arg] function below
- the result clocks are ok, i.e., v2 is on v1 + v1 is on v3 (2)
cf the [check_res] function below
** Checking expression arguments
--------------------------------
ok. So now, let us detail how we clock check expression arguments.
e.g., in the equation
we want to make sure that the clocks of the argument "a" and "b" are compatible
with the input clock profile of "toto".
To do that, we suppose we have already computed:
- "cil_par" the expected input clock profile (via "get_clock_profile")
- "cil_arg" the list of clocks of arguments (via a rec call to f)
In order to check that this call is correct, we check that both
terms are unifiable.
let (check_args : Lxm.t -> subst -> Eff.id_clock list -> Eff.id_clock list -> subst) =
fun lxm s cil_par cil_arg ->
assert (List.length cil_par = List.length cil_arg);
let idl_par,cil_par = List.split cil_par
and idl_arg,cil_arg = List.split cil_arg in
let s = List.fold_left2 (UnifyClock.f lxm) s cil_arg cil_par in
(** Checking expression result
--------------------------
It is the same thing, except that we have Eff.left list instead
of Eff.id_clock list.
e.g., in the equation:
we want to check that the clocks of "x" and "y" are compatible with
the output clock profile of node "toto".
To do that, we suppose we have:
- "rigth" the list of result clock. (via "get_clock_profile" again)
and we just need to check that both side are unifiable.
let rec (var_info_eff_of_left_eff: Eff.left -> Eff.var_info) =
function
| LeftVarEff (v, _) -> v
| LeftFieldEff (l, id,_) ->
let v = var_info_eff_of_left_eff l in
let new_name = (Ident.to_string v.var_name_eff) ^ "." ^ (Ident.to_string id) in
| LeftArrayEff (l,i,_) ->
let v = var_info_eff_of_left_eff l in
let new_name = (Ident.to_string v.var_name_eff) ^ "[" ^
| LeftSliceEff (l,si,_) ->
let v = var_info_eff_of_left_eff l in
let new_name = (Ident.to_string v.var_name_eff) ^ (string_of_slice_info_eff si)
in
let var_info_eff_to_clock_eff v = v.var_clock_eff
let (check_res : Lxm.t -> subst -> Eff.left list -> Eff.id_clock list -> unit) =
fun lxm (s1,s2) left rigth ->
let left_vi = List.map var_info_eff_of_left_eff left in
let left_ci = List.map var_info_eff_to_clock_eff left_vi in
if (List.length left_ci <> List.length rigth) then assert false;
let idl_rigth,rigth = List.split rigth
and idl_left, left_ci = List.split left_ci in
let s = (List.combine idl_rigth idl_left)@s1, s2 in
ignore(List.fold_left2 (UnifyClock.f lxm) s left_ci rigth)
(******************************************************************************)
(** In order to clock check "when" statements, we need to know if a clock [sc]
is a sub_clock of another one c (i.e., for all instants i, c(i) => sc(i))
If it is a sub_clock, we return the accumulator (the current substitution)
let rec (is_a_sub_clock :
Lxm.t -> subst -> Eff.id_clock -> Eff.id_clock -> subst option) =
fun lxm s (id_sc,sc) (id_c,c) ->
(* Check if [sc] is a sub-clock of [c] (in the large sense).
Returns Some updated substitution if it is the case, and None otherwise *)
let rec aux sc c =
match sc, c with
(* the base clock is a sub-clock of all clocks *)
| BaseEff, (BaseEff|On(_,_)|ClockVar _) -> Some s
| On(_,_), BaseEff -> None
| sc, On(_,c_clk) -> (
try Some(UnifyClock.f lxm s sc c)
with Compile_error _ -> aux sc c_clk
| _,_ ->
try Some(UnifyClock.f lxm s sc c)
with Compile_error _ -> None
type clock_profile = Eff.id_clock list * Eff.id_clock list
let (get_clock_profile : Eff.node_exp -> clock_profile) =
(List.map var_info_eff_to_clock_eff n.inlist_eff,
List.map var_info_eff_to_clock_eff n.outlist_eff)
let ci2str = LicDump.string_of_clock2
(******************************************************************************)
(** Now we can go on and define [f]. *)
let rec (f : Lxm.t -> Eff.id_solver -> subst -> Eff.val_exp -> Eff.clock list ->
Eff.val_exp * Eff.id_clock list * subst) =
fun lxm id_solver s ve exp_clks ->
(* we split f so that we can reinit the fresh clock var generator *)
let ve, inf_clks, s = f_aux id_solver s ve in
let s =
if exp_clks = [] then s else
List.fold_left2
(fun s eclk iclk -> UnifyClock.f lxm s eclk iclk)
s
exp_clks
(List.map (fun (_,clk) -> clk) inf_clks)
in
let inf_clks = List.map (fun (id,clk) -> id, apply_subst2 s clk) inf_clks in
let clks = snd (List.split inf_clks) in
let ve = { ve with clk = clks } in
Verbose.print_string ~level:3 (
"Clocking the expression '" ^ (LicDump.string_of_val_exp_eff ve) ^"': "^
(LicDump.string_of_clock2 (List.hd clks)) ^"\n");
ve, inf_clks, s
Erwan Jahier
committed
and f_aux id_solver s ve =
let (cel, s), lxm =
match ve.core with
| CallByPosEff ({it=posop; src=lxm}, OperEff args) ->
eval_by_pos_clock id_solver posop lxm args s, lxm
| CallByNameEff ({it=nmop; src=lxm}, nmargs ) ->
try eval_by_name_clock id_solver nmop lxm nmargs s, lxm
with EvalConst_error msg ->
raise (Compile_error(lxm, "\n*** can't eval constant: "^msg))
in
let new_clk = snd (List.split cel) in
let s, ve =
if ve.clk = [] then (s, { ve with clk = new_clk }) else
let s = List.fold_left2 (UnifyClock.f lxm) s ve.clk new_clk in
s, ve
in
apply_subst_val_exp s ve, cel, s
(* iterate f on a list of expressions *)
and (f_list : Eff.id_solver -> subst -> Eff.val_exp list ->
Eff.val_exp list * Eff.id_clock list list * subst) =
fun id_solver s args ->
let aux (args,acc,s) arg =
let arg, cil, s = f_aux id_solver s arg in
(arg::args, cil::acc, s)
let (args, cil, s) = List.fold_left aux ([],[],s) args in
let args = List.rev args in
let cil = List.rev cil in
let cil = List.map (List.map(fun (id,clk) -> id, apply_subst2 s clk)) cil in
args, cil, s
and (eval_by_pos_clock : Eff.id_solver -> Eff.by_pos_op -> Lxm.t -> Eff.val_exp list ->
subst -> Eff.id_clock list * subst) =
fun id_solver posop lxm args s ->
let apply_subst s (id,clk) = id, UnifyClock.apply_subst s clk in
match posop,args with
| Eff.CURRENT,args -> ( (* we return the clock of the argument *)
let _args, clocks_of_args, s = f_list id_solver s args in
let current_clock = function
| (id, BaseEff) -> (id, BaseEff)
| (id, On(_,clk)) -> (id, clk)
| (_, ClockVar _) -> assert false
in
List.map current_clock (List.flatten clocks_of_args), s
let c_clk, when_exp_clk =
match clk_exp with
| Base -> BaseEff, BaseEff
| NamedClock { it = (cc,c) ; src = lxm } ->
let id, c_clk =
(id_solver.id2var (Ident.to_idref c) lxm).var_clock_eff
in
c_clk, On((cc,c), c_clk)
(*
In order to clock check an expression such as
exp when C(c)
(1) we first need to check that the clock of c (c_clk)
is a sub-clock of the clock of exp (exp_clk).
(2)
*)
match is_a_sub_clock lxm s exp_clk (fst exp_clk,c_clk) with
let msg = "\n*** clock error: '" ^ (ci2str (snd exp_clk)) ^
"' is not a sub-clock of '" ^ (ci2str c_clk) ^ "'"
in
raise (Compile_error(lxm, msg))
| Some s ->
let id_when_exp_clk, s =
| id, On(var, _) -> (id, when_exp_clk), s
| id, BaseEff -> (id, when_exp_clk), s
| id, ClockVar i ->
let id_when_exp_clk = id, when_exp_clk in
id_when_exp_clk,
(s1, UnifyClock.add_subst2 i when_exp_clk s2)
id_when_exp_clk, s
(* XXX ce cas ne sert rien !!!
le traitement du cas ou la liste ne contient qu'un element
n'a aucun raison d'etre particulier, si ???
*)
| _args,[[exp_clk]], s ->
let (exp_clk,s) = aux_when exp_clk s in
([exp_clk], s)
| _args, [exp_clk_list], s ->
(* when on tuples *)
let exp_clk_list, s =
List.fold_left
(fun (acc,s) exp_clk ->
let (exp_clk,s) = aux_when exp_clk s in
exp_clk::acc, s
)
([],s)
exp_clk_list
in
(List.rev exp_clk_list, s)
| _ -> assert false (* "(x1,x2) when node (x,y)" *)
)
)
| Eff.MERGE _,args -> assert false (* TODO *)
| Eff.HAT(i,ve),args ->
let (_,clk,s) = f_aux id_solver s ve in
clk,s
(* nb: the args have been put inside the HAT_eff constructor *)
try ([var_info_eff_to_clock_eff (id_solver.id2var idref lxm)], s)
with Compile_error _ -> (* => it is a constant *)
let s, clk = UnifyClock.new_clock_var s in
[Ident.of_idref idref, clk], s
let (cil_arg, cil_res) = get_clock_profile node_exp_eff.it in
let s, rel_base = UnifyClock.new_clock_var s in
(* the value of the base clock of a node is actually relative
to the context into which the node is called.
Hence we create a fresh var clock, that will be instanciated
by the caller.
*)
let (replace_base : Eff.clock -> Eff.id_clock -> Eff.id_clock) =
fun rel_base (id,ci) ->
(* [replace_base rel_base ci ] replaces in [ci] any occurences of the
base clock by [rel_base] *)
let rec aux ci =
match ci with
| BaseEff -> rel_base
| On(v,clk) -> On(v, aux clk)
| ClockVar i -> ci
in
id, aux ci
in
let cil_arg = List.map (replace_base rel_base) cil_arg in
let cil_res = List.map (replace_base rel_base) cil_res in
let args, clk_args, s = f_list id_solver s args in
let s = check_args lxm s cil_arg (List.flatten clk_args) in
List.map (apply_subst s) cil_res, s
(* One argument. *)
| Eff.PRE,args
| Eff.STRUCT_ACCESS _,args
| Eff.ARRAY_ACCES (_),args
| Eff.ARRAY_SLICE (_),args ->
let (_,clk,s) = f_aux id_solver s (List.hd args) in
clk,s
let args, clk_args, s = f_list id_solver s args in
let flat_clk_args = List.flatten clk_args in (* => mono-clock! *)
let _,flat_clk_args = List.split flat_clk_args in
let clk_list, s =
if args = [] then [],s else
let _clk,s = UnifyClock.list lxm flat_clk_args s in
List.map (List.map (apply_subst s)) clk_args, s
in
PredefEvalClock.f op lxm sargs s clk_list
(* may have tuples as arguments *)
| Eff.TUPLE,args
| Eff.ARROW,args
| Eff.FBY ,args
| Eff.CONCAT,args
| Eff.ARRAY(args),_ -> (
(* Check that all args are of the same (unifiable) clocks.
XXX : we suppose that all those operators are
mono-clocks (i.e., when they return tuples, all elements
are on the same clock). It would be sensible to have,
e.g., arrows on multiple clocks. We'll refine later. *)
let args, clk_args, s = f_list id_solver s args in
let flat_clk_args = List.flatten clk_args in (* => mono-clock! *)
let idl,flat_clk_args = List.split flat_clk_args in
let clk,s = UnifyClock.list lxm flat_clk_args s in
let clk_list =
match posop with
| Eff.TUPLE ->
let clk_l = List.map (UnifyClock.apply_subst s) flat_clk_args in
List.combine idl clk_l
| _ -> List.map (apply_subst s) (List.hd clk_args)
in
clk_list, s
)
| Eff.WITH(ve),args ->
let (_,clk,s) = f_aux id_solver s ve in
clk, s
and (eval_by_name_clock : Eff.id_solver -> Eff.by_name_op -> Lxm.t ->
(Ident.t Lxm.srcflagged * Eff.val_exp) list -> subst ->
Eff.id_clock list * subst) =
fun id_solver namop lxm namargs s ->
| Eff.STRUCT_anonymous -> assert false (* cf EvalType.E *)
| Eff.STRUCT _ ->
let apply_subst s (id,clk) = id, UnifyClock.apply_subst s clk in
let args = List.map (fun (id,ve) -> ve) namargs in
(* XXX The 3 following lines duplicates the code of TUPLE_eff and co *)
let args, clk_args, s = f_list id_solver s args in
let flat_clk_args = List.flatten clk_args in (* => mono-clock! *)
let _,flat_clk_args = List.split flat_clk_args in
let clk,s = UnifyClock.list lxm flat_clk_args s in
let clk_list = List.map (apply_subst s) (List.hd clk_args) in
clk_list, s