-
Erwan Jahier authoredErwan Jahier authored
evalClock.ml 14.31 KiB
(** Time-stamp: <modified the 01/09/2008 (at 11:48) by jahier> *)
open Predef
open PredefEvalConst
open SyntaxTree
open SyntaxTreeCore
open Eff
open LicDump
open Printf
open Lxm
open Errors
open UnifyClock
(** 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
(x,y)=toto(a,b);
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.clock list -> Eff.clock list -> subst) =
fun lxm s cil_par cil_arg ->
assert (List.length cil_par = List.length cil_arg);
let s = List.fold_left2 (UnifyClock.f lxm) s cil_par cil_arg in
s
(** Checking expression result
--------------------------
It is the same thing, except that we have Eff.left list instead
of Eff.clock list.
e.g., in the equation:
(x,y)=toto(a,b);
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:
- "left" the list of Eff.left
- "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
{ v with var_name_eff = Ident.of_string new_name }
| LeftArrayEff (l,i,_) ->
let v = var_info_eff_of_left_eff l in
let new_name = (Ident.to_string v.var_name_eff) ^ "[" ^
(string_of_int i) ^ "]"
in
{ v with var_name_eff = Ident.of_string new_name }
| 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
{ v with var_name_eff = Ident.of_string new_name }
let var_info_eff_to_clock_eff v = v.var_clock_eff
(* exported *)
let (check_res : Lxm.t -> subst -> Eff.left list -> Eff.clock list -> unit) =
fun lxm s 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;
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))
*)
let rec (is_a_sub_clock : Lxm.t -> subst -> Eff.clock -> Eff.clock -> subst option) =
fun lxm s sc c ->
(* check if [sc] is a sub-clock of [c] (in the large
sens). Returns Some updated substitution if it is the case,
and None otherwise *)
match sc,c with
(* the base clock is a sub-clock of all clocks *)
| BaseEff, (BaseEff|On(_,_)|ClockVar _) -> Some s
| On(v,clk), BaseEff -> None
| On(v,clk), On(v2,clk2) -> (
try Some(UnifyClock.f lxm s clk clk2)
with _ -> is_a_sub_clock lxm s sc clk2
) | ClockVar j, BaseEff -> assert false
| ClockVar i, On(_,_)
| ClockVar i, ClockVar _ ->
(* XXX can it occur? if yes, something should be done
the problem being that several things are possible
(there is no unique sub-clock of a clock...
Well, ok, let's suppose that they are equal for the time being,
which seems wrong in the general case.
*)
let s1,s2 = s in
Some (s1,(i,c)::s2)
| On(_,_), ClockVar i -> (* Ditto *)
let s1,s2 = s in
Some (s1,(i,sc)::s2)
type clock_profile = Eff.clock list * Eff.clock list
let (get_clock_profile : Eff.node_exp -> clock_profile) =
fun n ->
(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
let cpt_var_name = ref 0
let (make_dummy_var: string -> Ident.t) =
fun str ->
Ident.of_string (str ^ (string_of_int !cpt_var_name))
(* On(make_dummy_var "const",ClockVar (get_var_type ())) *)
let concat_subst (s11,s12) (s21,s22) = (s11 @ s21, s12@s22)
(******************************************************************************)
(* We tabulate the result of the Eff.val_exp clock ckecking. Note,
that there is no clash in that table because all var_exp_eff are
srcflagged.
*)
let val_exp_eff_clk_tab = Hashtbl.create 0
let tabulate_res vef clock_eff_list =
(* print_string "*** '"; *)
(* print_string (LicDump.string_of_val_exp_eff vef); *)
(* print_string "' -> "; *)
(* print_string (String.concat "," (List.map LicDump.string_of_clock2 clock_eff_list)); *)
(* print_string "\n"; *)
(* flush stdout; *)
Hashtbl.add val_exp_eff_clk_tab vef clock_eff_list
let (get_val_exp_eff : Eff.val_exp -> Eff.clock list) =
fun vef ->
try
let res = Hashtbl.find val_exp_eff_clk_tab vef in
let var_clock_to_base = function
(* Some expressions migth be infered to be a variable clock
(e.g., constants). In that case, it is ok to consider that such
expressions are on the base clock.*)
(* XXX 'm pretty sure this is wrong! *)
| ClockVar _
| On(_,ClockVar _) -> BaseEff
| x -> x
in
List.map var_clock_to_base res with _ ->
print_string "*** No entry for '";
print_string (LicDump.string_of_val_exp_eff vef);
print_string "'\n ";
flush stdout;
assert false
(******************************************************************************)
(** Now we can go on and define [f]. *)
let rec (f : Eff.id_solver -> subst -> Eff.val_exp -> Eff.clock list * subst) =
fun id_solver s ve ->
cpt_var_name := 0;
UnifyClock.reset_var_type ();
(* we split f so that we can reinit the fresh clock var generator *)
let res = f_aux id_solver s ve in
let s = snd res in
(* during the inner call to f_aux, some intermediary clock variables
may remain. *)
Hashtbl.iter
(fun ve cel ->
let cel2 = List.map (apply_subst2 s) cel in
if cel <> cel2 then
Hashtbl.replace val_exp_eff_clk_tab ve cel2)
val_exp_eff_clk_tab;
res
and f_aux id_solver s ve =
let cel, s =
match ve with
| CallByPosEff ({it=posop; src=lxm}, OperEff args) ->
eval_by_pos_clock id_solver posop lxm args s
| CallByNameEff ({it=nmop; src=lxm}, nmargs ) ->
try eval_by_name_clock id_solver nmop lxm nmargs s
with EvalConst_error msg ->
raise (Compile_error(lxm, "\n*** can't eval constant: "^msg))
in
tabulate_res ve cel;
cel, s
(* iterate f on a list of expressions *)
and (f_list : Eff.id_solver -> subst -> Eff.val_exp list -> Eff.clock list list * subst) =
fun id_solver s args ->
let aux (acc,s) arg =
let cil, s = f_aux id_solver s arg in
(cil::acc, s)
in
let (cil, s) = List.fold_left aux ([],s) args in
let cil = List.rev cil in
cil, s
and (eval_by_pos_clock : Eff.id_solver -> Eff.by_pos_op -> Lxm.t -> Eff.val_exp list ->
subst -> Eff.clock list * subst) =
fun id_solver posop lxm args s ->
match posop with
| Eff.CURRENT -> ( (* we return the clock of the argument *)
let clocks_of_args, s = f_list id_solver s args in
match List.flatten clocks_of_args with
| [BaseEff] -> [BaseEff],s
| [On(_,clk)] -> [clk],s
| _ -> assert false
)
| Eff.WHENOT clk_var -> assert false (* use merge when it is implemented *)
| Eff.WHEN clk_var -> (
let clk = var_info_eff_to_clock_eff clk_var in
let aux_when exp_clk s =
match is_a_sub_clock lxm s exp_clk clk with
| None -> let msg = "\n*** clock error: '" ^ (ci2str (exp_clk)) ^
"' is not a sub-clock of '" ^ (ci2str (clk)) ^ "'"
in
raise (Compile_error(lxm, msg))
| Some s ->
let clk_of_exp_clk,s =
match exp_clk with
| BaseEff -> assert false
| On(var,_) -> On(var, clk), s
| ClockVar i ->
let cexp_clk = On(make_dummy_var "const",clk) in
let (s1,s2) = s in
cexp_clk, (s1,(i,cexp_clk)::s2)
in
clk_of_exp_clk, s
in
(match f_list id_solver s args with
| [[exp_clk]], s ->
let (exp_clk,s) = aux_when exp_clk s in
([exp_clk], s)
| [exp_clk_list], s ->
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 _ -> assert false
(* f_aux id_solver (List.hd args) *)
| Eff.HAT(i,ve) -> f_aux id_solver s ve
(* nb: the args have been put inside the HAT_eff constructor *)
| Eff.CONST (idref,_) -> [get_constant_clock ()],s
| Eff.IDENT idref -> (
try ([var_info_eff_to_clock_eff (id_solver.id2var idref lxm)], s)
with _ -> (* => it is a constant *) [get_constant_clock ()],s
)
| Eff.CALL node_exp_eff ->
let (cil_arg, cil_res) = get_clock_profile node_exp_eff.it 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 rel_base = ClockVar (UnifyClock.get_var_type ()) in
let rec (replace_base : Eff.clock -> Eff.clock -> Eff.clock) =
fun rel_base ci ->
(* [replace_base rel_base ci ] replaces in [ci] any occurences of the
base clock by [rel_base] *)
match ci with
| BaseEff -> rel_base
| On(v,clk) -> On(v, replace_base rel_base clk)
| ClockVar i -> 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 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
| Eff.STRUCT_ACCESS _
| Eff.ARRAY_ACCES (_, _)
| Eff.ARRAY_SLICE (_,_) ->
assert(List.length args = 1);
f_aux id_solver s (List.hd args)
| Eff.Predef (op,sargs) ->
let clk_args, s = f_list id_solver s args in
let flat_clk_args = List.flatten clk_args in (* => mono-clock! *)
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 clk_list, s
(* may have tuples as arguments *)
| Eff.TUPLE
| Eff.ARROW
| Eff.FBY
| Eff.CONCAT
| Eff.ARRAY -> (
(* 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 clk_args, s = f_list id_solver s args in
let flat_clk_args = List.flatten clk_args in (* => mono-clock! *)
let clk,s = UnifyClock.list lxm flat_clk_args s in
let clk_list =
match posop with
| Eff.TUPLE -> List.map (apply_subst s) flat_clk_args
| _ -> List.map (apply_subst s) (List.hd clk_args)
in
clk_list, s
)
| Eff.WITH(ve) -> f_aux id_solver s ve
and (eval_by_name_clock : Eff.id_solver -> Eff.by_name_op -> Lxm.t ->
(Ident.t Lxm.srcflagged * Eff.val_exp) list -> subst ->
Eff.clock list * subst) =
fun id_solver namop lxm namargs s ->
match namop with
| Eff.STRUCT_anonymous -> assert false (* cf EvalType.E *)
| Eff.STRUCT _ ->
let args = List.map (fun (id,ve) -> ve) namargs in
(* XXX The 3 following lines duplicates the code of TUPLE_eff and co *)
let clk_args, s = f_list id_solver s args in
let flat_clk_args = List.flatten clk_args in (* => mono-clock! *)
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