(* Partially known dynamic values for array indexing To make sure that the generated code has no array bound errors, we need at the code generation time some information about dynamic values that are to be used as indices of an array. Specifically, we need the lower (lwb) and the upper (upb) bounds of the value. We always assume that lwb < upb and the value v with the bounds (lwb,upb) satisfies lwb <= b < upb In our application -- stencil computations -- all arrays have the same length and are 0-indexed (that is, the smallest valid index into the array is zero). The length of the array is not statically known. We do assume that it is at least min_high (which we must check, see make_fun below). Bounds are treated as abstract outside this module. The constant min_bounded gives the value corresponding to the smallest index of the array, and wrappers like make_fun produce the corresponding bounded value for the upper bound of the array. The loop generators like forloop annotate the loop variable with the loop bounds. *) (* Configuration data *) let min_high = 4;; (* Minimal upper bound for an array *) (* The bounds themselves come in the form of an offset from min array bound and max array bound. *) type bound = | Low of int (* offset *) | High of int ;; type fuzzy_bool = True | False | Undecided;; (* Partial order on bounds *) let leq_bound : bound -> bound -> fuzzy_bool = fun lb ub -> match (lb,ub) with | (Low x, Low y) -> if x <= y then True else False | (High x, High y) -> if x <= y then True else False | (Low x, High y) -> if x <= min_high + y then True else Undecided | (High x, Low y) -> if min_high + x > y then False else Undecided ;; let offset_bound : int -> bound -> bound = fun n -> function | Low x -> Low (x+n) | High x -> High (x+n) ;; let string_of_bound : bound -> string = function | Low 0 -> "L" | Low n when n > 0 -> "L+" ^ string_of_int n | Low n when n < 0 -> "L-" ^ string_of_int (-n) | High 0 -> "H" | High n when n > 0 -> "H+" ^ string_of_int n | High n when n < 0 -> "H-" ^ string_of_int (-n) ;; type bounds = bound * bound;; (* Lower and higher bounds *) let string_of_bounds : bounds -> string = fun (lwb,upb) -> "[" ^ string_of_bound lwb ^ "," ^ string_of_bound upb ^ ")" ;; (* A bounded dynamic value of the type int *) (* Hereafter, the type variable 'c stands for the environment classifier. *) type 'c bounded = Bounded of bounds * (* lower and the upper bound *) ('c,int) code (* the value itself *) ;; let offset_bounded : int -> 'c bounded -> 'c bounded = function | 0 -> fun bv -> bv | n -> function Bounded ((lwb,upb),c) -> Bounded ((offset_bound n lwb, offset_bound n upb),.<.~c + n>.) ;; (* Extract the dynamic value from bounded *) let dyn_of_bounded = function | Bounded ((Low n,Low m),_) when n+1 = m -> .. | Bounded (_,c) -> c ;; let string_of_bounded : 'c bounded -> string = function Bounded (bounds,_) -> "B" ^ string_of_bounds bounds;; (* Compare bounded: we compare bounds rather than code values *) let same_bounded : 'c bounded -> 'c bounded -> bool = fun (Bounded (ab,_)) (Bounded (bb,_)) -> ab = bb;; (* Check to see if one bounded immediately precedes the other. That is, the upper bound of one matches with the lower bound of the other. *) let successive_bounded : 'c bounded -> 'c bounded -> bool = fun (Bounded ((_,ab),_)) (Bounded ((bb,_),_)) -> ab = bb;; let min_bounded = Bounded ((Low 0, Low 1),.<0>.);; let array_bounds = (Low 0, High 0);; (* Full bounds of an array *) (* Check to see if a given bounded value is within the given bounds. Return: - None if it is definitely out of bounds - Some c where c is the code (dynamic value) if it is definitely within the bounds - raise an error if cannot decide *) let within_bounds : 'c bounded -> bounds -> ('c,int) code option = fun (Bounded ((vl,vh),c)) (lwb, upb) -> if leq_bound vh lwb = True || leq_bound upb vl = True then None else if leq_bound lwb vl = True && leq_bound vh upb = True then Some c else failwith ("Can't decide if " ^ string_of_bounds (vl,vh) ^ " is within " ^ string_of_bounds (lwb,upb)) ;; (* A sample wrapper for our problems, which checks the upper bounds and generates the corresponding bounded value *) let make_fun gen = . assert (n >= min_high); .~(gen (Bounded ((High 0, High 1),..)) .. ..)>. ;; (* Generate the for-loop *) (* The loop variable i satisfies lwb <= i < upb *) let forloop' lwb upb body = ..) done>.;; (* The same, with bounded index bounds *) let forloop : 'c bounded -> 'c bounded -> ('c bounded -> ('c,unit) code) -> ('c,unit) code = fun (Bounded ((lwb,_),_) as lv) (Bounded ((upb,_),_) as uv) body -> forloop' (dyn_of_bounded lv) (dyn_of_bounded uv) (fun j -> body (Bounded ((lwb,upb),j))) ;;