Newer
Older
(** Time-stamp: <modified the 21/08/2008 (at 18:15) 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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
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)
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
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 *)
)
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
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 *)
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