(** Time-stamp: <modified the 25/06/2008 (at 16:40) by Erwan Jahier> *) open CompiledData open Lxm open Errors (*********************************************************************************) (** [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. *) 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) -> aux te (Slice(si.se_first,si.se_last,si.se_step,te)::acc) le in 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 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 *) ) 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 let res = update_vds (id2str v.var_name_eff) vds filters in res (*********************************************************************************) (** 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 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 lel = List.flatten (List.map (fun {it=(left,_)} -> left) eql) in let lel_map = partition_var lel in (* Check that one does not define an input *) VarMap.iter (fun v _ -> if v.var_nature_eff = SyntaxTreeCore.VarInput then let msg = "\n*** Error; " ^(id2str v.var_name_eff) ^ " is an input, and thus cannot be defined." in raise (Compile_error(lxm, msg)) ) lel_map; 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