From 07c73f3bf81298ab0d087ccdc12a6a25945b98e1 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Fri, 30 Jan 2009 16:41:30 +0100
Subject: [PATCH] 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...
---
src/structExpand.ml.save | 490 ---------------------------------------
src/uniqueOutput.ml | 35 ++-
2 files changed, 29 insertions(+), 496 deletions(-)
delete mode 100644 src/structExpand.ml.save
diff --git a/src/structExpand.ml.save b/src/structExpand.ml.save
deleted file mode 100644
index 32b62424..00000000
--- a/src/structExpand.ml.save
+++ /dev/null
@@ -1,490 +0,0 @@
-(** 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
-
diff --git a/src/uniqueOutput.ml b/src/uniqueOutput.ml
index bb62da81..6f665dd2 100644
--- a/src/uniqueOutput.ml
+++ b/src/uniqueOutput.ml
@@ -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
--
GitLab