Skip to content
Snippets Groups Projects
Commit 07c73f3b authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Fix a bug in the UniqueOutput module; I was missing some double definitions. 

For example, that kind of set of equations didn't trigger any error:

  x [1 .. 2][0][0].f1 = z ;
  x=y;

nb : it was working if equations were ordered differently tough...
parent 063baaf1
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/structExpand.ml.save deleted 100644 → 0
+ 0
− 490
View file @ 063baaf1
(** Time-stamp: <modified the 29/01/2009 (at 16:56) by Erwan Jahier> *)
(* Replace structures by as many variables as necessary.
Since structures can be recursive, it migth be a lot of new variables...
For instance, a variable
v : Toto { f1 : int ; f2 : int ^ 3 ; f3 : t^2
where
type t = T { x:int ; y:int }
will be expanded into
_v_f1 : int;
_v_f2 : int ^ 3;
_v_f3_1_x : int;
_v_f3_1_y : int;
_v_f3_2_x : int;
_v_f3_3_y : int;
nb : if 't' was a type that does not contain any struct type, we would just
have 3 variables.
nb : I needed to be quite clever to program that module, but I'm not...
so it's certainly buggy.
*)
open Lxm
open Eff
open Predef
type acc =
Eff.val_exp srcflagged list (* assertions *)
* (Eff.eq_info srcflagged) list (* equations *)
* Eff.var_info list (* new local vars *)
(********************************************************************************)
(* stuff to create fresh var names.
XXX code dupl. with Split.new_var
*)
let new_var str node_env type_eff clock_eff =
let id = Ident.of_string (Name.new_local_var str) in
(* let id = Ident.of_string (Name.new_local_var "h") in *)
let var =
{
var_name_eff = id;
var_nature_eff = SyntaxTreeCore.VarLocal;
var_number_eff = -1; (* this field is used only for i/o.
Should i rather put something sensible there ? *)
var_type_eff = type_eff;
var_clock_eff = clock_eff;
}
in
Hashtbl.add node_env.lenv_vars id var;
var
(* returns a new var based on [vi] with type [type_eff]. *)
let clone_var str vi node_env type_eff =
let str = (Ident.to_string vi.var_name_eff) ^ str in
(* let id = Ident.of_string (if str.[0] = '_' then str else "_" ^ str) in *)
let id = Ident.of_string (str) in
let var =
{
var_name_eff = id;
var_nature_eff = vi.var_nature_eff;
var_number_eff = vi.var_number_eff; (* this field is useless: to be removed. *)
var_type_eff = type_eff;
var_clock_eff = vi.var_clock_eff;
}
in
(* Hashtbl.add node_env.lenv_vars id var; *)
var
let rec (is_a_basic_type : Eff.type_ -> bool) =
function
| Array_type_eff _ | Struct_type_eff _ -> false
| _ -> true
let soi = string_of_int
(* [expand_var "toto" acc type]
adds in [acc] all the strings corresponding to the set of atomic variables
defined by "toto". For instance, if "toto" is of type "s^2" where s is a structure
with two integer fields f1 and f2, expand var returns :
["toto_0_f1",int ; "toto_0_f2",int ;"toto_1_f1",int ; "toto_1_f2",int ] @ acc
This function is used to expand left val_exp expressions.
*)
let (expand_var : string -> Eff.type_ -> (string * Eff.type_) list) =
fun prefix teff ->
let rec aux prefix acc teff =
match teff with
| Bool_type_eff
| Int_type_eff
| Real_type_eff
| External_type_eff _
| Enum_type_eff(_) -> (prefix,teff)::acc
| Any -> assert false (* should not occur *)
| Overload -> assert false (* should not occur *)
| Array_type_eff(teff_elt,i) ->
let rec unfold acc cpt =
if cpt = i then acc else
let acc = aux (prefix^"_"^(soi cpt)) acc teff_elt in
unfold acc (cpt+1)
in
unfold acc 0
| Struct_type_eff(l, fl) ->
List.fold_left
(fun acc (fn, (teff_elt,opt)) ->
aux (prefix^"_"^(Ident.to_string fn)) acc teff_elt)
acc
fl
in
List.rev (aux prefix [] teff)
(* XXX code dupl!! j'ai deja ecrit ce genre de chose... Bon. *)
let (index_list_of_slice_info : Eff.slice_info -> int list) =
fun si ->
let sign = if si.se_step > 0 then 1 else -1 in
let rec aux acc cpt =
if cpt > si.se_last*sign then acc else
aux (cpt::acc) (cpt + si.se_step)
in
List.rev (aux [] si.se_first)
(*
for ex, t of type int^3 is expanded into [t_0,t_1,t_2]
*)
type 'a var_tree = A of 'a var_tree list | S of (Ident.t * 'a var_tree) list | L of 'a
let (expand_left : Eff.local_env -> left -> left list) =
fun nenv left ->
(* First step: recursively traverse the left structure to compute the variable
prefix (e.g., "X.f2[4]" -> "X_f2_4")
But because of slices, things are not so simple...
The algo is the following:
- when we find a left leave, we generate all the possible names
corresponding to that var, in a data structure (a tree) that reflect
the lustre data structure (array and struct)
- Then, struct or array accesses just remove some branches of that tree
*)
let rec (gen_var_trees :
Lxm.t -> Eff.var_info -> string -> Eff.type_ -> left var_tree) =
fun lxm vi prefix teff -> match teff with
| Bool_type_eff
| Int_type_eff
| Real_type_eff
| External_type_eff _
| Enum_type_eff(_)
| Any (* should not occur *)
| Overload (* should not occur *)
->
let new_left = LeftVarEff (clone_var prefix vi nenv teff, lxm) in
L new_left
| Array_type_eff(teff_elt,i) ->
let rec unfold acc cpt =
if cpt < 0 then acc else
let prefix = prefix ^ "_" ^ (soi cpt) in
let vt = gen_var_trees lxm vi prefix teff_elt in
unfold (vt::acc) (cpt-1)
in
let lvt = unfold [] (i-1) in
A lvt
| Struct_type_eff(_, fl) ->
S (List.map
(fun (fn, (steff,_)) ->
let prefix = prefix^"_"^(Ident.to_string fn) in
(fn, gen_var_trees lxm vi prefix steff)
)
fl)
in
let rec (var_trees_of_left : left -> left var_tree) =
fun left ->
match left with
| LeftVarEff (vi,lxm) ->
gen_var_trees lxm vi (Ident.to_string vi.var_name_eff) vi.var_type_eff
| LeftFieldEff (l,id,t) ->
(match var_trees_of_left l with
| S fl -> (try List.assoc id fl with _ -> assert false)
| A _ | L _ -> assert false
)
| LeftArrayEff (l,i,t) ->
(match var_trees_of_left l with
| A array -> List.nth array i
| S _ | L _ -> assert false
)
| LeftSliceEff (l,si,t) ->
(match var_trees_of_left l with
| A array ->
let index_list = index_list_of_slice_info si in
let l = List.map (fun i -> List.nth array i) index_list in
A l
| S _ | L _ -> assert false
)
in
let rec (flatten_var_tree : 'a var_tree -> 'a list) =
function
| A array -> List.flatten (List.map flatten_var_tree array)
| S fl -> List.flatten (List.map (fun (id,vt) -> flatten_var_tree vt) fl)
| L str -> [str]
in
let vt = var_trees_of_left left in
flatten_var_tree vt
(********************************************************************************)
let rec (make_new_loc : Eff.local_env -> Eff.id_solver -> Lxm.t -> acc ->
Eff.val_exp -> acc * string list) =
fun nenv id_solver lxm acc ve -> (* build a new loc that will alias ve *)
let teff = List.hd (EvalType.val_exp_eff ve) in
let ceff = List.hd (EvalClock.get_val_exp_eff ve) in
let nv = new_var "v" nenv teff ceff in
let neq = [LeftVarEff(nv,lxm)], ve in
let neq = flagit neq lxm in
let nvl, (asserts,eqs,locs) = expand_var_info nenv id_solver ([],acc) nv in
let acc = (asserts,eqs, List.rev_append nvl locs) in
expand_eq nenv id_solver acc neq, [Ident.to_string nv.var_name_eff]
and (step1_val_exp : Eff.local_env -> Eff.id_solver -> Lxm.t -> acc -> Eff.val_exp ->
acc * string list) =
fun nenv id_solver lxm acc ve ->
(* First step: recursively traverse the val_exp structure to compute the variable
prefix (e.g., "X.f2[4]" -> "X_f2_4") *)
let rec aux acc ve prefix =
match ve with
| CallByPosEff (by_pos_op, OperEff vel) ->
let lxm = by_pos_op.src in
let by_pos_op = by_pos_op.it in
(match by_pos_op with
| STRUCT_ACCESS (id,teff) ->
(match vel with
| [ve] ->
let prefix = "_" ^ (Ident.of_string id) ^ prefix in
aux acc ve prefix
| _ -> assert false (* should not occur *)
)
| ARRAY_ACCES (i,teff) ->
(match vel with
| [ve] ->
let prefix = "_" ^ (soi i) ^ prefix in
aux acc ve prefix
| _ -> assert false (* should not occur *)
)
| ARRAY_SLICE (si,t) ->
(match vel with
| [ve] ->
(*
Non. Je dois,
- generer tous les elements du tableau
- jeter ceux qui ne sont pas dans la tranche
*)
(* let ve_elt, ve_size = *)
(* match EvalType.val_exp_eff ve with *)
(* | Array_type_eff(t,s) -> t,s *)
(* | _ -> assert false *)
(* in *)
let index_list = index_list_of_slice_info si in
let acc,ll =
List.fold_left
(fun (acc, ll) i ->
let prefix = "_" ^ (soi i) ^ prefix in
let (acc, l) = aux acc ve prefix in
acc, l::ll)
(acc,[])
index_list
in
let l = List.flatten ll in
acc, l
| _ -> assert false (* should not occur *)
)
| IDENT idref ->
let prefix = (Ident.string_of_idref idref) ^ prefix in
acc, [prefix]
| WITH(_) | HAT(_) | CONCAT | ARRAY(_)
| Predef _ | CALL _ | MERGE _ | CONST _
| PRE | ARROW | FBY | CURRENT | WHEN _ | TUPLE
->
(* Create a new loc var to alias such expressions *)
let acc, nv_str_list = make_new_loc nenv id_solver lxm acc ve in
acc, List.map (fun nv_str -> nv_str ^ prefix) nv_str_list
)
| CallByNameEff(by_name_op, fl) -> make_new_loc nenv id_solver lxm acc ve
in
aux acc ve ""
and (step2_val_exp : string -> Lxm.t -> Eff.type_ -> acc -> acc * Eff.val_exp list) =
fun prefix lxm teff acc ->
(* compute the expansion from the type using the prefix computed in step1 *)
let name_list = expand_var prefix teff in
let vel = List.map
(fun (str, teff) ->
let idref = Ident.idref_of_string str in
CallByPosEff({src=lxm;it=(IDENT idref)}, OperEff [])
)
name_list
in
acc, vel
(********************************************************************************)
and (expand_eq :
Eff.local_env -> Eff.id_solver -> acc -> Eff.eq_info srcflagged -> acc) =
fun nenv id_solver acc eqf ->
let { src = lxm_eq ; it = (left_list, ve) } = eqf in
let left_list = List.flatten (List.map (expand_left nenv) left_list) in
let ve,acc = expand_val_exp nenv id_solver acc ve in
let eqf = { src = lxm_eq ; it = (left_list, ve) } in
let (asserts, eqs, locs) = acc in
(asserts, eqf::eqs, locs)
and expand_val_exp_list n_env id_solver acc vel =
List.fold_left
(fun (vel,acc) ve ->
let ve,acc = expand_val_exp n_env id_solver acc ve in
ve::vel, acc
)
([],acc) (List.rev vel)
and (expand_val_exp: Eff.local_env -> Eff.id_solver -> acc -> val_exp ->
val_exp * acc) =
fun n_env id_solver acc ve ->
match ve with
| CallByPosEff (by_pos_op, OperEff vel) ->
let lxm = by_pos_op.src in
let by_pos_op = by_pos_op.it in
let by_pos_op, acc, vel = match by_pos_op with
| WITH(ve) ->
let ve, acc = expand_val_exp n_env id_solver acc ve in
let vel,acc = expand_val_exp_list n_env id_solver acc vel in
WITH(ve), acc, vel
| HAT(i,ve) ->
let ve, acc = expand_val_exp n_env id_solver acc ve in
let rec unfold cpt =
if cpt = 0 then [] else ve::(unfold (cpt-1))
in
TUPLE, acc, unfold i
| CONCAT ->
let vel,acc = expand_val_exp_list n_env id_solver acc vel in
TUPLE, acc, vel
| ARRAY(vel) ->
let vel,acc = expand_val_exp_list n_env id_solver acc vel in
TUPLE, acc, vel
| STRUCT_ACCESS (_,teff)
| ARRAY_ACCES (_,teff)
| ARRAY_SLICE (_,teff) ->
let acc,prefix_list = step1_val_exp n_env id_solver lxm acc ve in
let acc,vel =
List.fold_left
(fun (acc,vel_acc) prefix ->
let acc, vel = step2_val_exp prefix lxm teff acc in
acc, List.append vel vel_acc
)
(acc,[])
prefix_list
in
TUPLE, acc, vel
| IDENT idref ->
let prefix = Ident.string_of_idref idref in
let teff = (id_solver.id2var idref lxm).var_type_eff in
let acc,vel = step2_val_exp prefix lxm teff acc in
TUPLE, acc, vel
| Predef _ | CALL _ | MERGE _ | CONST _
| PRE | ARROW | FBY | CURRENT | WHEN _ | TUPLE
->
let vel,acc = expand_val_exp_list n_env id_solver acc vel in
by_pos_op, acc, vel
in
CallByPosEff(Lxm.flagit by_pos_op lxm, OperEff vel), acc
| CallByNameEff(by_name_op, fl) ->
let lxm = by_name_op.src in
let vel,acc = List.fold_left
(fun (vel,acc) (id,ve) ->
let ve,acc = expand_val_exp n_env id_solver acc ve in
ve::vel, acc
)
([],acc)
fl
in
CallByPosEff({ src = lxm ; it = TUPLE}, OperEff (List.rev vel)), acc
and (expand_val_exp_flag: Eff.local_env -> Eff.id_solver -> acc ->
val_exp srcflagged -> val_exp srcflagged * acc) =
fun n_env id_solver acc { src = lxm ; it = ve } ->
let ve,acc = expand_val_exp n_env id_solver acc ve in
{ src = lxm ; it = ve }, acc
and (expand_assert:
Eff.local_env -> Eff.id_solver -> acc -> val_exp srcflagged -> acc) =
fun n_env id_solver acc ve ->
let (ve, (asserts, eqs, locs)) = expand_val_exp_flag n_env id_solver acc ve in
(ve::asserts, eqs, locs)
and (expand_var_info: Eff.local_env -> Eff.id_solver -> var_info list * acc ->
var_info -> var_info list * acc) =
fun nenv id_solver (vil, acc) vi ->
match vi.var_type_eff with
| Struct_type_eff (name, fl) ->
List.fold_left
(fun (vil,acc) (fn, (ft,_)) ->
let new_var = clone_var ("_" ^ Ident.to_string fn) vi nenv ft in
let new_vil, new_acc = expand_var_info nenv id_solver (vil,acc) new_var in
if new_vil = new_var::vil then (
(* [new_var] type is not made of structure *)
assert (is_a_basic_type ft);
Hashtbl.add nenv.lenv_vars new_var.var_name_eff new_var);
new_vil, new_acc
)
(vil, acc)
fl
| Array_type_eff(at,size) ->
let rec aux i (vil,acc) =
if i=size then (vil,acc) else
let new_var = clone_var ("_" ^ soi i) vi nenv at in
let new_vil, new_acc = expand_var_info nenv id_solver (vil,acc) new_var in
if new_vil = new_var::vil then (
(* [new_var] type is not made of structure *)
assert (is_a_basic_type at);
Hashtbl.add nenv.lenv_vars new_var.var_name_eff new_var);
aux (i+1) (new_vil, new_acc)
in
aux 0 (vil,acc)
| _ -> vi::vil, acc
let (node : Eff.local_env -> Eff.id_solver -> Eff.node_exp -> Eff.node_exp) =
fun n_env is n ->
match n.def_eff with
| ExternEff
| AbstractEff -> n
| BodyEff b ->
let loclist = match n.loclist_eff with None -> [] | Some l -> l in
let inlist = n.inlist_eff in
let outlist = n.outlist_eff in
let acc = ([],[],[]) in
let inlist, acc = List.fold_left (expand_var_info n_env is) ([],acc) inlist in
let outlist, acc = List.fold_left (expand_var_info n_env is) ([],acc) outlist in
let loclist, acc = List.fold_left (expand_var_info n_env is) ([],acc) loclist in
let acc = List.fold_left (expand_eq n_env is) acc b.eqs_eff in
let acc = List.fold_left (expand_assert n_env is) acc b.asserts_eff in
let (asserts,neqs, nv) = acc in
let nb = {
eqs_eff = neqs ;
asserts_eff = asserts
}
in
let res =
{ n with
inlist_eff = List.rev inlist;
outlist_eff = List.rev outlist;
loclist_eff = Some (List.rev_append loclist nv);
def_eff = BodyEff nb
}
in
res
src/uniqueOutput.ml
+ 29
− 6
View file @ 07c73f3b
......@@ -61,7 +61,7 @@ let id2str = Ident.to_string
let int2str = string_of_int
(* Returns the list of undefined variables *)
let (vds_to_string : Eff.var_info -> var_def_state -> string list) =
let (vds_to_undefined_vars : string -> var_def_state -> string list) =
fun v vds ->
let rec aux vds v acc = match vds with
| VDS_def -> acc
......@@ -72,7 +72,21 @@ let (vds_to_string : Eff.var_info -> var_def_state -> string list) =
(Array.fold_left
(fun (acc,i) vds -> aux vds (v^"["^(int2str i) ^"]") acc, i+1) (acc,0) a)
in
aux vds (id2str v.var_name_eff) []
aux vds v []
(* Returns the list of defined variables *)
let (vds_to_defined_vars : string -> var_def_state -> string list) =
fun v vds ->
let rec aux vds v acc = match vds with
| VDS_def -> v::acc
| VDS_undef -> acc
| VDS_struct(fl) ->
List.fold_left (fun acc (id,vds) -> aux vds (v^"."^(id2str id)) acc) acc fl
| VDS_array(a) -> fst
(Array.fold_left
(fun (acc,i) vds -> aux vds (v^"["^(int2str i) ^"]") acc, i+1) (acc,0) a)
in
aux vds v []
(*********************************************************************************)
(** This is main function: it computes a new [var_def_state] from an
......@@ -82,11 +96,20 @@ let (update_var_def_state : var_def_state -> filtered_left -> var_def_state) =
let rec (update_vds : string -> var_def_state -> filter list -> var_def_state) =
fun v vds filters ->
if vds = VDS_def then
let msg = "\n*** Variable " ^ v ^ " is defined twice." in
let msg = "\n*** Variable " ^ v ^ " is already defined." in
raise (Compile_error(lxm, msg))
else
match filters with
| [] -> VDS_def
| [] ->
let already_def_vars = vds_to_defined_vars v vds in
if already_def_vars <> [] then
let msg =
"\n*** Variable " ^ v ^ " is already partly defined (" ^
(String.concat "," (already_def_vars)) ^ ")."
in
raise (Compile_error(lxm, msg))
else
VDS_def
| Slice(i,j,k,te)::tail -> update_slice v i j k tail
(match vds with
| VDS_array(a) -> a
......@@ -182,11 +205,11 @@ let (check : Eff.node_exp -> Lxm.t -> unit) =
let (check_one_var : Lxm.t -> Eff.var_info -> Eff.left list -> unit) =
fun lxm v lel ->
let ell = List.map left_eff_to_filtered_left lel in
match List.fold_left update_var_def_state VDS_undef ell with
match List.fold_left update_var_def_state VDS_undef (List.rev ell) with
| VDS_def -> ()
| vds ->
let msg = "\n*** Undefined variable(s): " ^
(String.concat ", " (vds_to_string v vds))
(String.concat ", " (vds_to_undefined_vars (id2str v.var_name_eff) vds))
in
raise (Compile_error(lxm, msg))
in
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment