From be68e8c5395f50ff5862e4610bacd33a41bffcd0 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Mon, 23 Jun 2008 15:52:34 +0200
Subject: [PATCH] A new implementation of uniqueOutput that is more
efficient, more compact, cleaner, and correct wrt negative steps in array
slices.
---
src/Makefile | 1 +
src/test/should_work/Pascal/left.lus | 6 +-
src/test/test.res.exp | 2 +-
src/uniqueOutput.ml | 497 ++++++++++-----------------
src/uniqueOutput.mli | 6 +
5 files changed, 195 insertions(+), 317 deletions(-)
create mode 100644 src/uniqueOutput.mli
diff --git a/src/Makefile b/src/Makefile
index 982f1974..e5f82a44 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -50,6 +50,7 @@ SOURCES = \
./evalClock.ml \
./getEff.mli \
./getEff.ml \
+ ./uniqueOutput.mli \
./uniqueOutput.ml \
./lazyCompiler.ml \
./lazyCompiler.mli \
diff --git a/src/test/should_work/Pascal/left.lus b/src/test/should_work/Pascal/left.lus
index aa21f4f5..8d9d5415 100644
--- a/src/test/should_work/Pascal/left.lus
+++ b/src/test/should_work/Pascal/left.lus
@@ -7,12 +7,12 @@ type truc = struct {
node toto(x : bool) returns (t : truc^3);
let
--- t[0].a[0..98 step 2][48..0 step -2] = true^25;
- t[0].a[0..98 step 2][0..48 step 2] = true^25;
+ t[0].a[0..98 step 2][48..0 step -2] = true^25;
+-- t[0].a[0..98 step 2][0..48 step 2] = true^25;
t[0].a[0..98 step 2][1..49 step 2] = false^25;
t[0].a[1..99 step 2][0] = true;
t[0].a[1..99 step 2][1] = true;
t[0].a[5..99 step 2] = false^48;
- t[0].b = 42;
+ t[0].b = 42;
t[1..2] = (truc { a = true^100; b = 0 })^2;
tel
diff --git a/src/test/test.res.exp b/src/test/test.res.exp
index 3f22b15b..ad14bdd3 100644
--- a/src/test/test.res.exp
+++ b/src/test/test.res.exp
@@ -2960,7 +2960,7 @@ Opening file /home/jahier/lus2lic/src/test/should_work/Pascal/left.lus
type left::truc = left::truc {a : bool^100; b : int};
node left::toto(x:bool) returns (t:left::truc^3);
let
- t[0].a[0..98 step 2][0..48 step 2] = true^25;
+ t[0].a[0..98 step 2][48..0 step -2] = true^25;
t[0].a[0..98 step 2][1..49 step 2] = false^25;
t[0].a[1..99 step 2][0] = true;
t[0].a[1..99 step 2][1] = true;
diff --git a/src/uniqueOutput.ml b/src/uniqueOutput.ml
index 8c322759..e2adcb25 100644
--- a/src/uniqueOutput.ml
+++ b/src/uniqueOutput.ml
@@ -1,334 +1,205 @@
-
+(** Time-stamp: <modified the 23/06/2008 (at 15:51) by Erwan Jahier> *)
open CompiledData
open Lxm
open Errors
-(* given a list of (output) [var_info_eff] [vl], and a list of
- [left_eff] [lel], we want to check that each variable is defined
- exactly once by the [left_eff]. To do that, we first transform
- [vl] into a list of variable atoms.
-*)
-type atom = string
-(* | Var of (var_info_eff) *)
-(* | Field of (atom * Ident.t) *)
-(* | Array of (atom * int) *)
-
-let rec (var_info_eff_to_atoms: var_info_eff -> atom list) =
- fun v ->
- type_eff_to_atoms (Ident.to_string v.var_name_eff) v.var_type_eff
-
-and make_int_list acc i = if i < 0 then acc else make_int_list (i::acc) (i-1)
-
-and slice_info_to_int_list si i =
- if (
- (si.se_step > 0 && i > si.se_last)
- ||
- (si.se_step < 0 && i < si.se_last)
- )
- then
- []
- else
- i::(slice_info_to_int_list si (i + si.se_step))
-
-
-and (type_eff_to_atoms : atom -> type_eff -> atom list) =
- fun str type_eff ->
- let res =
- match type_eff with
- | Bool_type_eff
- | Int_type_eff
- | Real_type_eff
- | Any
- | Overload
- | External_type_eff _
- | Enum_type_eff(_,_) -> [str]
- | Array_type_eff(te,i) ->
- List.flatten
- (List.map
- (fun i -> type_eff_to_atoms (str ^ "[" ^(string_of_int i)^"]") te)
- (make_int_list [] (i-1)))
-
- | Struct_type_eff(name, fl) ->
- List.flatten
- (List.map
- (fun (id,(te,_)) ->
- type_eff_to_atoms (str ^ "." ^(Ident.to_string id)) te
- )
- fl)
- in
- res
-
-(* Generates the string corresponding to the [left_eff]. It returns
- a list of strings because of the slices. Indeed, when generating
- the string for the [left_eff] corresponding to "expr[2..3].a", we
- actually want to generate 2 strings:
-
- - "expr[2].a", and
- - "expr[3].a"
-
- le pb, c'est que pour "t[1..10][2..4]", je veux pas générer
- - "t[1][2]", etc.,
- mais "t[3]", "t[4]", "t[5]" ! arg... il me faut faire quelque chose
- pour les tranches de tranches.
-
-
- meme chose pour "T[1..4 step 2][1]" en fait (qui vaut t[3])
-
- il faudrait que je normalise tout ca avant. Il y a plein de facon de dire
- la même chose.
-
- -> rendre le step positif
- -> mise a plat des tranches de tranches
- -> mise a plat d'une tranche suivis d'un acces à un tableau
-
+(*********************************************************************************)
+(** [left_eff] is a kind of list, but which is in a « bad » order for
+ easy checking; [eff_left] contains just the same information, but
+ the list is made explicit and the infomartion (struct or array
+ accesses) is ordered in the « good » way.
*)
-and (left_eff_to_string : left_eff -> atom list) =
- fun le ->
- let res =
- match le with
- | LeftVarEff (v,_) -> [Ident.to_string v.var_name_eff]
- | LeftFieldEff(le,id,te) ->
- let strl = left_eff_to_string le in
- List.map (fun str -> str^"."^(Ident.to_string id)) strl
- | LeftArrayEff(le,i,te) ->
- let strl = left_eff_to_string le in
- List.map (fun str -> (str ^ "[" ^ (string_of_int i) ^ "]")) strl
-
- | LeftSliceEff(LeftSliceEff(le,si1,te1),si2,te2) ->
- assert false
+
+type eff_left = var_info_eff * Lxm.t * filter list
+and filter =
+ | Slice of int * int * int * type_eff
+ | Faccess of Ident.t * type_eff
+ | Aaccess of int * type_eff
+
+let rec (left_eff_to_eff_left: left_eff -> eff_left) =
+ fun le ->
+ let rec (aux : type_eff -> filter list -> left_eff -> eff_left) =
+ fun te_top acc le -> match le with
+ | LeftVarEff (v,lxm) -> v, lxm, acc
+ | LeftFieldEff(le,id,te) -> aux te (Faccess(id,te)::acc) le
+ | LeftArrayEff(le,i,te) -> aux te (Aaccess(i,te)::acc) le
| LeftSliceEff(le,si,te) ->
- let strl = left_eff_to_string le in
- List.flatten
- (List.map
- (fun i -> List.map
- (fun str -> (str^"["^(string_of_int i) ^ "]"))
- strl)
- (slice_info_to_int_list si si.se_first)
- )
+ aux te (Slice(si.se_first,si.se_last,si.se_step,te)::acc) le
in
- res
-
-and (left_eff_to_atoms : left_eff * Lxm.t -> (atom * Lxm.t) list) =
- fun (le,lxm) ->
- let res =
- match le with
- | LeftVarEff (v,lxm) -> List.map (fun a -> a,lxm) (var_info_eff_to_atoms v)
-
- | LeftArrayEff(LeftSliceEff(le1,si1,te1),l,te2) ->
- (* le1[i..j step k][l] = le1[i + k*l] *)
- let (i,j,k) =
- if si1.se_step > 0
- then (si1.se_first, si1.se_last,si1.se_step)
- else (si1.se_last, si1.se_first, - si1.se_step)
- in
- let new_l = i + l * k in
- left_eff_to_atoms (LeftArrayEff(le1, new_l, te2), lxm)
-
- | LeftSliceEff(LeftSliceEff(le1,si1,te1),si2,te2) ->
- (* we need we interpret on-the-fly slices of slices...
- le1[i1..j1 step k1][i2..j2 step k2] =
- le1[ i1+i2*k1
- .. i1+(j2+i2*(k1-1))*k2
- step k1*k2 ]
- if k1 and k2 are positive.
-
- k1<0, k2>0
-
- what happens if one (or both) are negative ?
-
- *)
- let (i1,j1,k1) = (si1.se_first, si1.se_last,si1.se_step) in
- let (i2,j2,k2) = (si2.se_first, si2.se_last,si2.se_step) in
- let si12 = {
- se_first = i1+i2*k1;
- se_last = i1+(j2+i2*(k1-1))*k2;
- se_step = k1 * k2; (* bug si < 0 ! *)
- se_width = -1;
- }
- in
- left_eff_to_atoms(LeftSliceEff(le1, si12,te2), lxm)
- | LeftFieldEff(le2,_,te)
- | LeftArrayEff(le2,_,te)
- | LeftSliceEff(le2,_,Array_type_eff(te,_)) ->
- let al = left_eff_to_string le in
- List.map (fun a -> a,lxm)
- (List.flatten (List.map (fun a -> type_eff_to_atoms a te) al))
+ let te_top = (var_info_of_left_eff le).var_type_eff in
+ let (v,lxm,f) = aux te_top [] le in
+ let (_,f) =
+ (* we don't want to associate to each accessors the type of the
+ « accessed elements », but its own type. E.g., if "t" is an
+ array of bool, we want to associate 't[0]' and an array of
+ bool, and not to a bool. *)
+ List.fold_left
+ (fun (te_top,acc) el ->
+ match el with
+ | Slice(i,j,k,te) -> te, (Slice(i,j,k,te_top))::acc
+ | Faccess(id,te) -> te, (Faccess(id,te_top))::acc
+ | Aaccess(i,te) -> te, (Aaccess(i,te_top))::acc
+ )
+ (te_top,[])
+ f
+ in
+ (v,lxm, List.rev f)
+
+(*********************************************************************************)
+(** Used to represent how much « defined » a variable is. *)
+type var_def_state =
+ | VDS_def
+ | VDS_undef
+ | VDS_struct of (Ident.t * var_def_state) list
+ | VDS_array of var_def_state array
+
+let id2str = Ident.to_string
+let int2str = string_of_int
+
+(* Returns the list of undefined variables *)
+let (vds_to_string : var_info_eff -> var_def_state -> string list) =
+ fun v vds ->
+ let rec aux vds v acc = match vds with
+ | VDS_def -> acc
+ | VDS_undef -> v::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
- res
-
-module StrSet = Set.Make(String)
+ aux vds (id2str v.var_name_eff) []
+
+(*********************************************************************************)
+(** This is main function: it computes a new [var_def_state] from an
+ [var_def_state] and a [eff_left]. *)
+let (update_var_def_state : var_def_state -> eff_left -> var_def_state) =
+ fun vds (v, lxm, filters) ->
+ 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
+ raise (Compile_error(lxm, msg))
+ else
+ match filters with
+ | [] -> VDS_def
+ | Slice(i,j,k,te)::tail -> update_slice v i j k tail
+ (match vds with
+ | VDS_array(a) -> a
+ | VDS_undef -> undef_array_of_type te
+ | _ -> assert false (* by type checking *)
+ )
+ | Aaccess(i,te)::tail -> update_array_access v i tail
+ (match vds with
+ | VDS_array(a) -> a
+ | VDS_undef -> undef_array_of_type te
+ | _ -> assert false (* by type checking *)
+ )
+ | Faccess(id,te)::tail -> update_field_access v id tail
+ (match vds with
+ | VDS_struct(fl) -> fl
+ | VDS_undef -> undef_struct_of_type te
+ | _ -> assert false (* by type checking *)
+ )
-let (check_aux : Lxm.t -> var_info_eff list -> (left_eff * Lxm.t) list -> unit) =
- fun lxm vl lel ->
- let l1 = List.flatten (List.map var_info_eff_to_atoms vl) in
- let l2 = List.flatten (List.map left_eff_to_atoms lel) in
-(* let _ = *)
-(* print_string ("\noutputs to be defined: "); *)
-(* List.iter (fun str -> print_string (str ^ ", ")) l1; *)
-(* print_string ("\ndefined left eff: "); *)
-(* List.iter (fun (str,_) -> print_string (str ^ ", ")) l2; *)
-(* print_string "\n checking...\n"; *)
-(* flush stdout *)
-(* in *)
- let set1 = List.fold_left (fun set x -> StrSet.add x set) StrSet.empty l1 in
- let set2 =
- List.fold_left
- (fun set (elt,lxm) ->
- if StrSet.mem elt set then StrSet.remove elt set else
- let msg =
- if StrSet.mem elt set1 then
- "\n*** This variable is defined twice: " ^ elt
- else
- "\n*** This variable is undeclared: " ^ elt
- in
- raise (Compile_error(lxm, msg))
- )
- set1
- l2
+ and undef_array_of_type = function
+ | Array_type_eff(_,size) -> Array.make size VDS_undef
+ | _ -> assert false
+
+ and undef_struct_of_type = function
+ | Struct_type_eff(_,fl) -> List.map (fun (id,_) -> id, VDS_undef) fl
+ | _ -> assert false
+
+ and array_for_all pred a = Array.fold_left (fun acc x -> acc && (pred x)) true a
+ and update_slice v i j k filters a =
+ let v = v^"["^(int2str i)^ ".."^(int2str j)^
+ (if k=1 then "]" else " step "^(int2str k)^"]")
+ in
+ let sub_size = ((j-i)/k+1) in
+ let sub_a = Array.make sub_size VDS_undef in
+ let vds =
+ for l=0 to sub_size-1 do sub_a.(l) <- a.(i+l*k) done;
+ update_vds v (VDS_array sub_a) filters
+ in
+ (match vds with
+ | VDS_undef
+ | VDS_struct(_) -> assert false
+ | VDS_def -> for l=0 to sub_size-1 do a.(i+l*k) <- VDS_def done
+ | VDS_array sa -> for l=0 to sub_size-1 do a.(i+l*k) <- sub_a.(l) done
+ );
+ if array_for_all (fun elt -> elt = VDS_def) a then VDS_def else VDS_array(a)
+
+ and update_array_access v i filters a =
+ let v = v ^ "[" ^ (int2str i) ^ "]" in
+ let vds_i = update_vds v a.(i) filters in
+ a.(i) <- vds_i;
+ if array_for_all (fun elt -> elt = VDS_def) a then VDS_def else VDS_array(a)
+
+ and update_field_access v id filters fl =
+ let vds_id = List.assoc id fl in
+ let v = v ^ "." ^ (id2str id) in
+ let vds = update_vds v vds_id filters in
+ let fl = replace_field id vds fl in
+ if List.for_all (fun (_,vds) -> vds = VDS_def) fl
+ then VDS_def
+ else VDS_struct(fl)
+
+ and replace_field fn new_fv l =
+ match l with
+ | (id,fv)::tail ->
+ if id = fn then (id,new_fv)::tail
+ else (id,fv)::(replace_field fn new_fv tail)
+ | [] -> assert false (* fn is necessarily in l *)
in
- if not (StrSet.is_empty set2) then
- let vars = (StrSet.fold (fun elt acc -> elt::acc) set2 []) in
- let msg =
- (if List.length vars = 1 then
- "\n*** The following variable is undefined: "
- else
- "\n*** The following variables are undefined: ") ^
- (String.concat ", " vars)
- in
- raise (Compile_error(lxm, msg))
+ let res = update_vds (id2str v.var_name_eff) vds filters in
+ res
-(* Check that each output is defined exactly once *)
+(*********************************************************************************)
+(** Sort out the left_eff according to the variable they define. *)
+module VarMap = Map.Make(struct type t = var_info_eff let compare = compare end)
+let (partition_var : left_eff list -> (left_eff list) VarMap.t) =
+ fun l ->
+ let f tab le =
+ let v = var_info_of_left_eff le in
+ try VarMap.add v (le::(VarMap.find v tab)) tab
+ with Not_found -> VarMap.add v [le] tab
+ in
+ List.fold_left f VarMap.empty l
+
+(*********************************************************************************)
+(* exported *)
let (check : CompiledData.node_exp_eff -> Lxm.t -> unit) =
fun node lxm ->
- let ol = match node.loclist_eff with
- None -> node.outlist_eff
+ let vars_to_check = match node.loclist_eff with
+ | None -> node.outlist_eff
| Some l -> node.outlist_eff @ l
+ in
+ let (check_one_var : Lxm.t -> var_info_eff -> left_eff list -> unit) =
+ fun lxm v lel ->
+ let ell = List.map left_eff_to_eff_left lel in
+ match List.fold_left update_var_def_state VDS_undef ell with
+ | VDS_def -> ()
+ | vds ->
+ let msg = "\n*** Undefined variable(s): " ^
+ (String.concat ", " (vds_to_string v vds))
+ in
+ raise (Compile_error(lxm, msg))
in
match node.def_eff with
| ExternEff
| AbstractEff -> ()
- | BodyEff{ eqs_eff = eql } ->
- let lpll =
- List.map
- (fun ({ it = (lel,_); src = lxm }) ->
- List.map (fun le -> (le,lxm)) lel
- )
- eql
- in
- let (lpl:(left_eff * Lxm.t) list) = List.flatten lpll in
-
- check_aux lxm ol lpl
-
-
-(* Then, for each chunk, we search in [lel] a element [le] that
- concerns v, and we compute the list of chunks that correspond to
- the part of a that is not covered by [le]. That new list of chunks
- is added to the list of chunks to be checked. And we continue
- until there are no more chunks or no more [left_eff].
-
- In order to reduce the complexity of that algo, we first partition
- the [lel] according to the variable they define.
-*)
-
-
-(* module VarMap = Map.Make(struct type t=var_info_eff let compare = compare end) *)
-(* *)
-(* let (partition_var : left_eff list -> (left_eff list) VarMap.t) = *)
-(* fun l -> *)
-(* List.fold_left *)
-(* (fun tab le -> *)
-(* let v = var_info_of_left_eff le in *)
-(* try VarMap.add v (le::(VarMap.find v tab)) tab *)
-(* with Not_found -> VarMap.add v [le] tab *)
-(* ) *)
-(* VarMap.empty *)
-(* l *)
-(* *)
-(* *)
-(* (* Hence, given a list of [left_eff] that all concerns v, it is less *)
-(* expensive (we operate on smaller lists) to check that [v] is *)
-(* completety and uniquely defined. *)
-(* *)
-(* The idea to perform that check is to, from a left_eff and from a var_info_eff, *)
-(* generates the list of atomic variables they defined. e.g., an array of *)
-(* size 10 will generated 10 atomic variables. Then, we just have to *)
-(* compare the list that comes from the left_eff, and the one that comes from *)
-(* the output variables. *)
-(* *)
-(* *) *)
-(* *)
-(* type atom = *)
-(* | Var of *)
-(* | Field of *)
-(* let ( *)
-(* *)
-(* *)
-(* *)
-(* *)
-(* *)
-(* *)
-(* *)
-(* *)
-(* *)
-(* *)
-(* *)
-(* *)
-(* *)
-(* let (check_one_chunk : chunk -> left_eff -> chunk list) = *)
-(* fun c le -> match c,le with *)
-(* | Var v -> ( *)
-(* match le with *)
-(* | LeftVarEff (_,_) -> [] *)
-(* | LeftFieldEff(le,id,Struct_type_eff(_,fl)) -> *)
-(* let fl = List.filter (fun f -> f <> id) fl in *)
-(* List.map (fun (id, (te,_)) -> ) fl *)
-(* | LeftArrayEff(le,i,_) -> *)
-(* | LeftSliceEff(le,si,_) -> *)
-(* ) *)
-(* *)
-(* | Field(c,id), LeftFieldEff(le,id,_) -> *)
-(* | Array(c,i), LeftArrayEff(le,i,_) -> *)
-(* | Slice(c, low, high),LeftSliceEff(le,si,_) -> *)
-(* ddd *)
-(* *)
-(* *)
-(* let (reconstruct : var_info_eff -> chunk list -> *)
-(* *)
-(* *)
-(* *)
-(* let (check_one_var : var_info_eff -> left_eff_list -> unit) = *)
-(* fun v lel -> *)
-(* let rec (aux : chunk list -> left_eff_list -> unit) = *)
-(* fun cl lel -> *)
-(* match cl with *)
-(* | [] -> if lel <> [] then failwith "output variable defined twice" *)
-(* | x::cl -> let new_chunks = check_one_chunk x lel *)
-(* in *)
-(* aux [Var v] lel *)
-(* *)
-(* let (check_one_chunk : chunk -> left_eff list -> chunk list) = *)
-(* fun al le -> *)
-(* (* checks that le is used in [lel]: *)
-(* Removes the part that is used, but it migth add some chunks *) *)
-(* match le with *)
-(* | LeftVarEff(v,_) -> ( *)
-(* let (al1, al2) = List.partition (fun a -> a = Var(v)) al in *)
-(* match al1 with *)
-(* | [] -> failwith "output variable undefined" *)
-(* | _::_ -> failwith "output variable defined twice" *)
-(* | [_] -> al2 *)
-(* ) *)
-(* | LeftFieldEff(le,id,_) -> ( *)
-(* let (al1, al2) = List.partition (fun a -> a = Field(_,id)) al in *)
-(* match al1 with *)
-(* | [] -> failwith "output variable undefined" *)
-(* | _::_ -> failwith "output variable defined twice" *)
-(* | [_] -> al2 *)
-(* ) *)
-(* | LeftArrayEff(le,i,_) -> *)
-(* | LeftSliceEff(le, si,_) -> *)
-(* *)
-(* (* (* (* *) *) *) *)
+ | BodyEff{ eqs_eff = eql } ->
+ let lel = List.flatten (List.map (fun {it=(left,_)} -> left) eql) in
+ let lel_map = partition_var lel in
+ List.iter
+ (fun v ->
+ try check_one_var lxm v (VarMap.find v lel_map)
+ with Not_found ->
+ let msg = "\n*** Undefined variable: " ^ (id2str v.var_name_eff)
+ in
+ raise (Compile_error(lxm, msg))
+ )
+ vars_to_check
diff --git a/src/uniqueOutput.mli b/src/uniqueOutput.mli
new file mode 100644
index 00000000..5bbab223
--- /dev/null
+++ b/src/uniqueOutput.mli
@@ -0,0 +1,6 @@
+(** Time-stamp: <modified the 23/06/2008 (at 15:48) by Erwan Jahier> *)
+
+(** Check that each output and each local variable is defined at most
+ and at least once. *)
+
+val check : CompiledData.node_exp_eff -> Lxm.t -> unit
--
GitLab