diff options
Diffstat (limited to 'cil/src/ext/pta/steensgaard.ml')
| -rw-r--r-- | cil/src/ext/pta/steensgaard.ml | 1417 |
1 files changed, 0 insertions, 1417 deletions
diff --git a/cil/src/ext/pta/steensgaard.ml b/cil/src/ext/pta/steensgaard.ml deleted file mode 100644 index 6368693..0000000 --- a/cil/src/ext/pta/steensgaard.ml +++ /dev/null @@ -1,1417 +0,0 @@ -(* - * - * Copyright (c) 2001-2002, - * John Kodumal <jkodumal@eecs.berkeley.edu> - * All rights reserved. - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * 1. Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * - * 2. Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in the - * documentation and/or other materials provided with the distribution. - * - * 3. The names of the contributors may not be used to endorse or promote - * products derived from this software without specific prior written - * permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS - * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED - * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A - * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER - * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, - * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, - * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR - * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF - * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING - * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS - * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. - * - *) - -(***********************************************************************) -(* *) -(* *) -(* This file is currently unused by CIL. It is included in the *) -(* distribution for reference only. *) -(* *) -(* *) -(***********************************************************************) - - -(***********************************************************************) -(* *) -(* Type Declarations *) -(* *) -(***********************************************************************) - -exception Inconsistent of string -exception Bad_cache -exception No_contents -exception Bad_proj -exception Bad_type_copy -exception Instantiation_cycle - -module U = Uref -module S = Setp -module H = Hashtbl -module Q = Queue - -(** Polarity kinds-- positive, negative, or nonpolar. *) -type polarity = Pos - | Neg - | Non - -(** Label bounds. The polymorphic type is a hack for recursive modules *) -type 'a bound = {index : int; info : 'a} - -(** The 'a type may in general contain urefs, which makes Pervasives.compare - incorrect. However, the bounds will always be correct because if two tau's - get unified, their cached instantiations will be re-entered into the - worklist, ensuring that any labels find the new bounds *) -module Bound = -struct - type 'a t = 'a bound - let compare (x : 'a t) (y : 'a t) = - Pervasives.compare x y -end - -module B = S.Make(Bound) - -type 'a boundset = 'a B.t - -(** Constants, which identify elements in points-to sets *) -type constant = int * string - -module Constant = -struct - type t = constant - - let compare ((xid,_) : t) ((yid,_) : t) = - Pervasives.compare xid yid -end - -module C = Set.Make(Constant) - -(** Sets of constants. Set union is used when two labels containing - constant sets are unified *) -type constantset = C.t - -type lblinfo = { - mutable l_name: string; - (** Name of this label *) - mutable aliases: constantset; - (** Set of constants (tags) for checking aliases *) - p_bounds: label boundset U.uref; - (** Set of umatched (p) lower bounds *) - n_bounds: label boundset U.uref; - (** Set of unmatched (n) lower bounds *) - mutable p_cached: bool; - (** Flag indicating whether all reachable p edges have been locally cached *) - mutable n_cached: bool; - (** Flag indicating whether all reachable n edges have been locally cached *) - mutable on_path: bool; - (** For cycle detection during reachability queries *) -} - -(** Constructor labels *) -and label = lblinfo U.uref - -(** The type of lvalues. *) -type lvalue = { - l: label; - contents: tau -} - -(** Data for variables. *) -and vinfo = { - v_name: string; - mutable v_global: bool; - v_cache: cache -} - -(** Data for ref constructors. *) -and rinfo = { - rl: label; - mutable r_global: bool; - points_to: tau; - r_cache: cache -} - -(** Data for fun constructors. *) -and finfo = { - fl: label; - mutable f_global: bool; - args: tau list ref; - ret: tau; - f_cache: cache -} - -(* Data for pairs. Note there is no label. *) -and pinfo = { - mutable p_global: bool; - ptr: tau; - lam: tau; - p_cache: cache -} - -(** Type constructors discovered by type inference *) -and tinfo = Wild - | Var of vinfo - | Ref of rinfo - | Fun of finfo - | Pair of pinfo - -(** The top-level points-to type. *) -and tau = tinfo U.uref - -(** The instantiation constraint cache. The index is used as a key. *) -and cache = (int,polarity * tau) H.t - -(* Type of semi-unification constraints *) -type su_constraint = Instantiation of tau * (int * polarity) * tau - | Unification of tau * tau - -(** Association lists, used for printing recursive types. The first element - is a type that has been visited. The second element is the string - representation of that type (so far). If the string option is set, then - this type occurs within itself, and is associated with the recursive var - name stored in the option. When walking a type, add it to an association - list. - - Example : suppose we have the constraint 'a = ref('a). The type is unified - via cyclic unification, and would loop infinitely if we attempted to print - it. What we want to do is print the type u rv. ref(rv). This is accomplished - in the following manner: - - -- ref('a) is visited. It is not in the association list, so it is added - and the string "ref(" is stored in the second element. We recurse to print - the first argument of the constructor. - - -- In the recursive call, we see that 'a (or ref('a)) is already in the - association list, so the type is recursive. We check the string option, - which is None, meaning that this is the first recurrence of the type. We - create a new recursive variable, rv and set the string option to 'rv. Next, - we prepend u rv. to the string representation we have seen before, "ref(", - and return "rv" as the string representation of this type. - - -- The string so far is "u rv.ref(". The recursive call returns, and we - complete the type by printing the result of the call, "rv", and ")" - - In a type where the recursive variable appears twice, e.g. 'a = pair('a,'a), - the second time we hit 'a, the string option will be set, so we know to - reuse the same recursive variable name. -*) -type association = tau * string ref * string option ref - -(***********************************************************************) -(* *) -(* Global Variables *) -(* *) -(***********************************************************************) - -(** Print the instantiations constraints (loops with cyclic structures). *) -let print_constraints : bool ref = ref false - -(** Solve constraints as they are introduced. If this is false, constraints - are solved in batch fashion at calls to solveConstraints. *) -let solve_online : bool ref = ref true - -(** If true, print all constraints (including induced) and show additional - debug output. *) -let debug = ref false -let debug_constraints = debug - -(** If true, print out extra verbose debug information (including contents - of label sets *) -let verbose_debug = ref false - - -(** If true, make the flow step a no-op *) -let no_flow = ref false - -let no_sub = ref false - -(** If true, do not add instantiation constraints *) -let analyze_mono = ref false - -(** A counter for generating unique integers. *) -let counter : int ref = ref 0 - -(** A list of equality constraints. *) -let eq_worklist : su_constraint Q.t = Q.create() - -(** A list of instantiation constraints. *) -let inst_worklist : su_constraint Q.t = Q.create() - -(***********************************************************************) -(* *) -(* Utility Functions *) -(* *) -(***********************************************************************) - -(** Consistency check for inferred types *) -let pair_or_var (t : tau) = - match (U.deref t) with - | Pair _ -> true - | Var _ -> true - | _ -> false - -let ref_or_var (t : tau) = - match (U.deref t) with - | Ref _ -> true - | Var _ -> true - | _ -> false - -let fun_or_var (t : tau) = - match (U.deref t) with - | Fun _ -> true - | Var _ -> true - | _ -> false - -(** Generate a unique integer. *) -let fresh_index () : int = - incr counter; - !counter - -(** Negate a polarity. *) -let negate (p : polarity) : polarity = - match p with - | Pos -> Neg - | Neg -> Pos - | Non -> Non - -(** Compute the least-upper-bounds of two polarities. *) -let lub (p,p' : polarity * polarity) : polarity = - match p with - | Pos -> - begin - match p' with - | Pos -> Pos - | _ -> Non - end - | Neg -> - begin - match p' with - | Neg -> Neg - | _ -> Non - end - | Non -> Non - -(** Extract the cache from a type *) -let get_cache (t : tau) : cache = - match U.deref t with - | Wild -> raise Bad_cache - | Var v -> v.v_cache - | Ref r -> r.r_cache - | Pair p -> p.p_cache - | Fun f -> f.f_cache - -(** Determine whether or not a type is global *) -let get_global (t : tau) : bool = - match U.deref t with - | Wild -> false - | Var v -> v.v_global - | Ref r -> r.r_global - | Pair p -> p.p_global - | Fun f -> f.f_global - -(** Return true if a type is monomorphic (global). *) -let global_tau = get_global - -let global_lvalue lv = get_global lv.contents - -(** Return true if e is a member of l (according to uref equality) *) -let rec ulist_mem e l = - match l with - | [] -> false - | h :: t -> if (U.equal(h,e)) then true else ulist_mem e t - -(** Convert a polarity to a string *) -let string_of_polarity p = - match p with - | Pos -> "+" - | Neg -> "-" - | Non -> "T" - -(** Convert a label to a string, short representation *) -let string_of_label2 (l : label) : string = - "\"" ^ (U.deref l).l_name ^ "\"" - -(** Convert a label to a string, long representation *) -let string_of_label (l : label ) : string = - let rec constset_to_string = function - | (_,s) :: [] -> s - | (_,s) :: t -> s ^ "," ^ (constset_to_string t) - | [] -> "" - in - let aliases = constset_to_string (C.elements ((U.deref l).aliases)) - in - if ( (aliases = "") || (not !verbose_debug)) - then string_of_label2 l - else aliases - -(** Return true if the element [e] is present in the association list *) -let rec assoc_list_mem (e : tau) (l : association list) = - match l with - | [] -> None - | (h,s,so) :: t -> - if (U.equal(h,e)) then (Some (s,so)) else assoc_list_mem e t - -(** Given a tau, create a unique recursive variable name. This should always - return the same name for a given tau *) -let fresh_recvar_name (t : tau) : string = - match U.deref t with - | Pair p -> "rvp" ^ string_of_int((Hashtbl.hash p)) - | Ref r -> "rvr" ^ string_of_int((Hashtbl.hash r)) - | Fun f -> "rvf" ^ string_of_int((Hashtbl.hash f)) - | _ -> raise (Inconsistent ("recvar_name")) - -(** Return a string representation of a tau, using association lists. *) -let string_of_tau (t : tau ) : string = - let tau_map : association list ref = ref [] in - let rec string_of_tau' t = - match (assoc_list_mem t (!tau_map)) with - | Some (s,so) -> (* recursive type. see if a var name has been set *) - begin - match (!so) with - | None -> - begin - let rv = fresh_recvar_name(t) in - s := "u " ^ rv ^ "." ^ (!s); - so := Some (rv); - rv - end - | Some rv -> rv - end - | None -> (* type's not recursive. Add it to the assoc list and cont. *) - let s = ref "" in - let so : string option ref = ref None in - begin - tau_map := (t,s,so) :: (!tau_map); - - (match (U.deref t) with - | Wild -> s := "_"; - | Var v -> s := v.v_name; - | Pair p -> - begin - assert (ref_or_var(p.ptr)); - assert (fun_or_var(p.lam)); - s := "{"; - s := (!s) ^ (string_of_tau' p.ptr); - s := (!s) ^ ","; - s := (!s) ^ (string_of_tau' p.lam); - s := (!s) ^"}" - - end - | Ref r -> - begin - assert(pair_or_var(r.points_to)); - s := "ref(|"; - s := (!s) ^ (string_of_label r.rl); - s := (!s) ^ "|,"; - s := (!s) ^ (string_of_tau' r.points_to); - s := (!s) ^ ")" - - end - | Fun f -> - begin - assert(pair_or_var(f.ret)); - let rec string_of_args = function - | h :: [] -> - begin - assert(pair_or_var(h)); - s := (!s) ^ (string_of_tau' h) - end - | h :: t -> - begin - assert(pair_or_var(h)); - s := (!s) ^ (string_of_tau' h) ^ ","; - string_of_args t - end - | [] -> () - in - s := "fun(|"; - s := (!s) ^ (string_of_label f.fl); - s := (!s) ^ "|,"; - s := (!s) ^ "<"; - if (List.length !(f.args) > 0) - then - string_of_args !(f.args) - else - s := (!s) ^ "void"; - s := (!s) ^">,"; - s := (!s) ^ (string_of_tau' f.ret); - s := (!s) ^ ")" - end); - tau_map := List.tl (!tau_map); - !s - end - in - string_of_tau' t - -(** Convert an lvalue to a string *) -let rec string_of_lvalue (lv : lvalue) : string = - let contents = (string_of_tau(lv.contents)) in - let l = (string_of_label lv.l) in - assert(pair_or_var(lv.contents)); - Printf.sprintf "[%s]^(%s)" contents l - -(** Print a list of tau elements, comma separated *) -let rec print_tau_list (l : tau list) : unit = - let t_strings = List.map string_of_tau l in - let rec print_t_strings = function - | h :: [] -> print_string h; print_newline(); - | h :: t -> print_string h; print_string ", "; print_t_strings t - | [] -> () - in - print_t_strings t_strings - -(** Print a constraint. *) -let print_constraint (c : su_constraint) = - match c with - | Unification (t,t') -> - let lhs = string_of_tau t in - let rhs = string_of_tau t' in - Printf.printf "%s == %s\n" lhs rhs - | Instantiation (t,(i,p),t') -> - let lhs = string_of_tau t in - let rhs = string_of_tau t' in - let index = string_of_int i in - let pol = string_of_polarity p in - Printf.printf "%s <={%s,%s} %s\n" lhs index pol rhs - -(* If [positive] is true, return the p-edge bounds, otherwise, return - the n-edge bounds. *) -let get_bounds (positive : bool) (l : label) : label boundset U.uref = - if (positive) then - (U.deref l).p_bounds - else - (U.deref l).n_bounds - -(** Used for cycle detection during the flow step. Returns true if the - label [l] is found on the current path. *) -let on_path (l : label) : bool = - (U.deref l).on_path - -(** Used for cycle detection during the flow step. Identifies [l] as being - on/off the current path. *) -let set_on_path (l : label) (b : bool) : unit = - (U.deref l).on_path <- b - -(** Make the type a global type *) -let set_global (t : tau) (b : bool) : bool = - if (!debug && b) - then - Printf.printf "Setting a new global : %s\n" (string_of_tau t); - begin - assert ( (not (get_global(t)) ) || b ); - (match U.deref t with - | Wild -> () - | Var v -> v.v_global <- b - | Ref r -> r.r_global <- b - | Pair p -> p.p_global <- b - | Fun f -> f.f_global <- b); - b - end - -(** Return a label's bounds as a string *) -let string_of_bounds (is_pos : bool) (l : label) : string = - let bounds = - if (is_pos) then - U.deref ((U.deref l).p_bounds) - else - U.deref ((U.deref l).n_bounds) - in - B.fold (fun b -> fun res -> res ^ (string_of_label2 b.info) ^ " " - ) bounds "" - -(***********************************************************************) -(* *) -(* Type Operations -- these do not create any constraints *) -(* *) -(***********************************************************************) - -let wild_val = U.uref Wild - -(** The wild (don't care) value. *) -let wild () : tau = - wild_val - -(** Create an lvalue with label [lbl] and tau contents [t]. *) -let make_lval (lbl,t : label * tau) : lvalue = - {l = lbl; contents = t} - -(** Create a new label with name [name]. Also adds a fresh constant - with name [name] to this label's aliases set. *) -let make_label (name : string) : label = - U.uref { - l_name = name; - aliases = (C.add (fresh_index(),name) C.empty); - p_bounds = U.uref (B.empty); - n_bounds = U.uref (B.empty); - p_cached = false; - n_cached = false; - on_path = false - } - -(** Create a new label with an unspecified name and an empty alias set. *) -let fresh_label () : label = - U.uref { - l_name = "l_" ^ (string_of_int (fresh_index())); - aliases = (C.empty); - p_bounds = U.uref (B.empty); - n_bounds = U.uref (B.empty); - p_cached = false; - n_cached = false; - on_path = false - } - -(** Create a fresh bound. *) -let make_bound (i,a : int * 'a) : 'a bound = - {index = i; info = a } - -(** Create a fresh named variable with name '[name]. *) -let make_var (b: bool) (name : string) : tau = - U.uref (Var {v_name = ("'" ^name); - v_global = b; - v_cache = H.create 4}) - -(** Create a fresh unnamed variable (name will be 'fv). *) -let fresh_var () : tau = - make_var false ("fv" ^ (string_of_int (fresh_index())) ) - -(** Create a fresh unnamed variable (name will be 'fi). *) -let fresh_var_i () : tau = - make_var false ("fi" ^ (string_of_int (fresh_index())) ) - -(** Create a Fun constructor. *) -let make_fun (lbl,a,r : label * (tau list) * tau) : tau = - U.uref (Fun {fl = lbl ; - f_global = false; - args = ref a; - ret = r; - f_cache = H.create 4}) - -(** Create a Ref constructor. *) -let make_ref (lbl,pt : label * tau) : tau = - U.uref (Ref {rl = lbl ; - r_global = false; - points_to = pt; - r_cache = H.create 4}) - -(** Create a Pair constructor. *) -let make_pair (p,f : tau * tau) : tau = - U.uref (Pair {ptr = p; - p_global = false; - lam = f; - p_cache = H.create 4}) - -(** Copy the toplevel constructor of [t], putting fresh variables in each - argement of the constructor. *) -let copy_toplevel (t : tau) : tau = - match U.deref t with - | Pair _ -> - make_pair (fresh_var_i(), fresh_var_i()) - | Ref _ -> - make_ref (fresh_label(),fresh_var_i()) - | Fun f -> - let fresh_fn = fun _ -> fresh_var_i() - in - make_fun (fresh_label(), List.map fresh_fn !(f.args) , fresh_var_i()) - | _ -> raise Bad_type_copy - -let pad_args (l,l' : (tau list ref) * (tau list ref)) : unit = - let padding = ref ((List.length (!l)) - (List.length (!l'))) - in - if (!padding == 0) then () - else - let to_pad = - if (!padding > 0) then l' else (padding := -(!padding);l) - in - for i = 1 to (!padding) do - to_pad := (!to_pad) @ [fresh_var()] - done - -(***********************************************************************) -(* *) -(* Constraint Generation/ Resolution *) -(* *) -(***********************************************************************) - -(** Returns true if the constraint has no effect, i.e. either the left-hand - side or the right-hand side is wild. *) -let wild_constraint (t,t' : tau * tau) : bool = - let ti,ti' = U.deref t, U.deref t' in - match ti,ti' with - | Wild, _ -> true - | _, Wild -> true - | _ -> false - -exception Cycle_found - -(** Cycle detection between instantiations. Returns true if there is a cycle - from t to t' *) -let exists_cycle (t,t' : tau * tau) : bool = - let visited : tau list ref = ref [] in - let rec exists_cycle' t = - if (ulist_mem t (!visited)) - then - begin (* - print_string "Instantiation cycle found :"; - print_tau_list (!visited); - print_newline(); - print_string (string_of_tau t); - print_newline(); *) - (* raise Instantiation_cycle *) - (* visited := List.tl (!visited) *) (* check *) - end - else - begin - visited := t :: (!visited); - if (U.equal(t,t')) - then raise Cycle_found - else - H.iter (fun _ -> fun (_,t'') -> - if (U.equal (t,t'')) then () - else - ignore (exists_cycle' t'') - ) (get_cache t) ; - visited := List.tl (!visited) - end - in - try - exists_cycle' t; - false - with - | Cycle_found -> true - -exception Subterm - -(** Returns true if [t'] is a proper subterm of [t] *) -let proper_subterm (t,t') = - let visited : tau list ref = ref [] in - let rec proper_subterm' t = - if (ulist_mem t (!visited)) - then () (* recursive type *) - else - if (U.equal (t,t')) - then raise Subterm - else - begin - visited := t :: (!visited); - ( - match (U.deref t) with - | Wild -> () - | Var _ -> () - | Ref r -> - proper_subterm' r.points_to - | Pair p -> - proper_subterm' p.ptr; - proper_subterm' p.lam - | Fun f -> - proper_subterm' f.ret; - List.iter (proper_subterm') !(f.args) - ); - visited := List.tl (!visited) - end - in - try - if (U.equal(t,t')) then false - else - begin - proper_subterm' t; - false - end - with - | Subterm -> true - -(** The extended occurs check. Search for a cycle of instantiations from [t] - to [t']. If such a cycle exists, check to see that [t'] is a proper subterm - of [t]. If it is, then return true *) -let eoc (t,t') : bool = - if (exists_cycle(t,t') && proper_subterm(t,t')) - then - begin - if (!debug) - then - Printf.printf "Occurs check : %s occurs within %s\n" (string_of_tau t') - (string_of_tau t) - else - (); - true - end - else - false - -(** Resolve an instantiation constraint *) -let rec instantiate_int (t,(i,p),t' : tau * (int * polarity) * tau) = - if ( wild_constraint(t,t') || (not (store(t,(i,p),t'))) || - U.equal(t,t') ) - then () - else - let ti,ti' = U.deref t, U.deref t' in - match ti,ti' with - | Ref r, Ref r' -> - instantiate_ref(r,(i,p),r') - | Fun f, Fun f' -> - instantiate_fun(f,(i,p),f') - | Pair pr, Pair pr' -> - begin - add_constraint_int (Instantiation (pr.ptr,(i,p),pr'.ptr)); - add_constraint_int (Instantiation (pr.lam,(i,p),pr'.lam)) - end - | Var v, _ -> () - | _,Var v' -> - if eoc(t,t') - then - add_constraint_int (Unification (t,t')) - else - begin - unstore(t,i); - add_constraint_int (Unification ((copy_toplevel t),t')); - add_constraint_int (Instantiation (t,(i,p),t')) - end - | _ -> raise (Inconsistent("instantiate")) - -(** Apply instantiations to the ref's label, and structurally down the type. - Contents of ref constructors are instantiated with polarity Non. *) -and instantiate_ref (ri,(i,p),ri') : unit = - add_constraint_int (Instantiation(ri.points_to,(i,Non),ri'.points_to)); - instantiate_label (ri.rl,(i,p),ri'.rl) - -(** Apply instantiations to the fun's label, and structurally down the type. - Flip the polarity for the function's args. If the lengths of the argument - lists don't match, extend the shorter list as necessary. *) -and instantiate_fun (fi,(i,p),fi') : unit = - pad_args (fi.args, fi'.args); - assert(List.length !(fi.args) == List.length !(fi'.args)); - add_constraint_int (Instantiation (fi.ret,(i,p),fi'.ret)); - List.iter2 (fun t ->fun t' -> - add_constraint_int (Instantiation(t,(i,negate p),t'))) - !(fi.args) !(fi'.args); - instantiate_label (fi.fl,(i,p),fi'.fl) - -(** Instantiate a label. Update the label's bounds with new flow edges. - *) -and instantiate_label (l,(i,p),l' : label * (int * polarity) * label) : unit = - if (!debug) then - Printf.printf "%s <= {%d,%s} %s\n" (string_of_label l) i - (string_of_polarity p) (string_of_label l'); - let li,li' = U.deref l, U.deref l' in - match p with - | Pos -> - U.update (li'.p_bounds, - B.add(make_bound (i,l)) (U.deref li'.p_bounds) - ) - | Neg -> - U.update (li.n_bounds, - B.add(make_bound (i,l')) (U.deref li.n_bounds) - ) - | Non -> - begin - U.update (li'.p_bounds, - B.add(make_bound (i,l)) (U.deref li'.p_bounds) - ); - U.update (li.n_bounds, - B.add(make_bound (i,l')) (U.deref li.n_bounds) - ) - end - -(** Resolve a unification constraint. Does the uref unification after grabbing - a copy of the information before the two infos are unified. The other - interesting feature of this function is the way 'globalness' is propagated. - If a non-global is unified with a global, the non-global becomes global. - If the ecr became global, there is a problem because none of its cached - instantiations know that the type became monomorphic. In this case, they - must be re-inserted via merge-cache. Merge-cache always reinserts cached - instantiations from the non-ecr type, i.e. the type that was 'killed' by the - unification. *) -and unify_int (t,t' : tau * tau) : unit = - if (wild_constraint(t,t') || U.equal(t,t')) - then () - else - let ti, ti' = U.deref t, U.deref t' in - begin - U.unify combine (t,t'); - match ti,ti' with - | Var v, _ -> - begin - if (set_global t' (v.v_global || (get_global t'))) - then (H.iter (merge_cache t') (get_cache t')) - else (); - H.iter (merge_cache t') v.v_cache - end - | _, Var v -> - begin - if (set_global t (v.v_global || (get_global t))) - then (H.iter (merge_cache t) (get_cache t)) - else (); - H.iter (merge_cache t) v.v_cache - end - | Ref r, Ref r' -> - begin - if (set_global t (r.r_global || r'.r_global)) - then (H.iter (merge_cache t) (get_cache t)) - else (); - H.iter (merge_cache t) r'.r_cache; - unify_ref(r,r') - end - | Fun f, Fun f' -> - begin - if (set_global t (f.f_global || f'.f_global)) - then (H.iter (merge_cache t) (get_cache t)) - else (); - H.iter (merge_cache t) f'.f_cache; - unify_fun (f,f'); - end - | Pair p, Pair p' -> - begin - if (set_global t (p.p_global || p'.p_global)) - then (H.iter (merge_cache t) (get_cache t)) - else (); - H.iter (merge_cache t) p'.p_cache; - add_constraint_int (Unification (p.ptr,p'.ptr)); - add_constraint_int (Unification (p.lam,p'.lam)) - end - | _ -> raise (Inconsistent("unify")) - end - -(** Unify the ref's label, and apply unification structurally down the type. *) -and unify_ref (ri,ri' : rinfo * rinfo) : unit = - add_constraint_int (Unification (ri.points_to,ri'.points_to)); - unify_label(ri.rl,ri'.rl) - -(** Unify the fun's label, and apply unification structurally down the type, - at arguments and return value. When combining two lists of different lengths, - always choose the longer list for the representative. *) -and unify_fun (li,li' : finfo * finfo) : unit = - let rec union_args = function - | _, [] -> false - | [], _ -> true - | h :: t, h' :: t' -> - add_constraint_int (Unification (h,h')); union_args(t,t') - in - begin - unify_label(li.fl,li'.fl); - add_constraint_int (Unification (li.ret,li'.ret)); - if (union_args(!(li.args),!(li'.args))) - then li.args := !(li'.args); - end - -(** Unify two labels, combining the set of constants denoting aliases. *) -and unify_label (l,l' : label * label) : unit = - let pick_name (li,li' : lblinfo * lblinfo) = - if ( (String.length li.l_name) > 1 && (String.sub (li.l_name) 0 2) = "l_") - then - li.l_name <- li'.l_name - else () - in - let combine_label (li,li' : lblinfo *lblinfo) : lblinfo = - let p_bounds = U.deref (li.p_bounds) in - let p_bounds' = U.deref (li'.p_bounds) in - let n_bounds = U.deref (li.n_bounds) in - let n_bounds' = U.deref (li'.n_bounds) in - begin - pick_name(li,li'); - li.aliases <- C.union (li.aliases) (li'.aliases); - U.update (li.p_bounds, (B.union p_bounds p_bounds')); - U.update (li.n_bounds, (B.union n_bounds n_bounds')); - li - end - in(* - if (!debug) then - begin - Printf.printf "Unifying %s with %s...\n" - (string_of_label l) (string_of_label l'); - Printf.printf "pbounds : %s\n" (string_of_bounds true l); - Printf.printf "nbounds : %s\n" (string_of_bounds false l); - Printf.printf "pbounds : %s\n" (string_of_bounds true l'); - Printf.printf "nbounds : %s\n\n" (string_of_bounds false l') - end; *) - U.unify combine_label (l,l') - (* if (!debug) then - begin - Printf.printf "pbounds : %s\n" (string_of_bounds true l); - Printf.printf "nbounds : %s\n" (string_of_bounds false l) - end *) - -(** Re-assert a cached instantiation constraint, since the old type was - killed by a unification *) -and merge_cache (rep : tau) (i : int) (p,t' : polarity * tau) : unit = - add_constraint_int (Instantiation (rep,(i,p),t')) - -(** Pick the representative info for two tinfo's. This function prefers the - first argument when both arguments are the same structure, but when - one type is a structure and the other is a var, it picks the structure. *) -and combine (ti,ti' : tinfo * tinfo) : tinfo = - match ti,ti' with - | Var _, _ -> ti' - | _,_ -> ti - -(** Add a new constraint induced by other constraints. *) -and add_constraint_int (c : su_constraint) = - if (!print_constraints && !debug) then print_constraint c else (); - begin - match c with - | Instantiation _ -> - Q.add c inst_worklist - | Unification _ -> - Q.add c eq_worklist - end; - if (!debug) then solve_constraints() else () - -(** Add a new constraint introduced through this module's interface (a - top-level constraint). *) -and add_constraint (c : su_constraint) = - begin - add_constraint_int (c); - if (!print_constraints && not (!debug)) then print_constraint c else (); - if (!solve_online) then solve_constraints() else () - end - - -(* Fetch constraints, preferring equalities. *) -and fetch_constraint () : su_constraint option = - if (Q.length eq_worklist > 0) - then - Some (Q.take eq_worklist) - else if (Q.length inst_worklist > 0) - then - Some (Q.take inst_worklist) - else - None - -(** Returns the target of a cached instantiation, if it exists. *) -and target (t,i,p : tau * int * polarity) : (polarity * tau) option = - let cache = get_cache t in - if (global_tau t) then Some (Non,t) - else - try - Some (H.find cache i) - with - | Not_found -> None - -(** Caches a new instantiation, or applies well-formedness. *) -and store ( t,(i,p),t' : tau * (int * polarity) * tau) : bool = - let cache = get_cache t in - match target(t,i,p) with - | Some (p'',t'') -> - if (U.equal (t',t'') && (lub(p,p'') = p'')) - then - false - else - begin - add_constraint_int (Unification (t',t'')); - H.replace cache i (lub(p,p''),t''); - (* add a new forced instantiation as well *) - if (lub(p,p'') = p'') - then () - else - begin - unstore(t,i); - add_constraint_int (Instantiation (t,(i,lub(p,p'')),t'')) - end; - false - end - | None -> - begin - H.add cache i (p,t'); - true - end - -(** Remove a cached instantiation. Used when type structure changes *) -and unstore (t,i : tau * int) = -let cache = get_cache t in - H.remove cache i - -(** The main solver loop. *) -and solve_constraints () : unit = - match fetch_constraint () with - | Some c -> - begin - (match c with - | Instantiation (t,(i,p),t') -> instantiate_int (t,(i,p),t') - | Unification (t,t') -> unify_int (t,t') - ); - solve_constraints() - end - | None -> () - - -(***********************************************************************) -(* *) -(* Interface Functions *) -(* *) -(***********************************************************************) - -(** Return the contents of the lvalue. *) -let rvalue (lv : lvalue) : tau = - lv.contents - -(** Dereference the rvalue. If it does not have enough structure to support - the operation, then the correct structure is added via new unification - constraints. *) -let rec deref (t : tau) : lvalue = - match U.deref t with - | Pair p -> - ( - match U.deref (p.ptr) with - | Var _ -> - begin - (* let points_to = make_pair(fresh_var(),fresh_var()) in *) - let points_to = fresh_var() in - let l = fresh_label() in - let r = make_ref(l,points_to) - in - add_constraint (Unification (p.ptr,r)); - make_lval(l, points_to) - end - | Ref r -> make_lval(r.rl, r.points_to) - | _ -> raise (Inconsistent("deref")) - ) - | Var v -> - begin - add_constraint (Unification (t,make_pair(fresh_var(),fresh_var()))); - deref t - end - | _ -> raise (Inconsistent("deref -- no top level pair")) - -(** Form the union of [t] and [t']. *) -let join (t : tau) (t' : tau) : tau = - let t'' = fresh_var() in - add_constraint (Unification (t,t'')); - add_constraint (Unification (t',t'')); - t'' - -(** Form the union of a list [tl], expected to be the initializers of some - structure or array type. *) -let join_inits (tl : tau list) : tau = - let t' = fresh_var() in - begin - List.iter (function t'' -> add_constraint (Unification(t',t''))) tl; - t' - end - -(** Take the address of an lvalue. Does not add constraints. *) -let address (lv : lvalue) : tau = - make_pair (make_ref (lv.l, lv.contents), fresh_var() ) - -(** Instantiate a type with index i. By default, uses positive polarity. - Adds an instantiation constraint. *) -let instantiate (lv : lvalue) (i : int) : lvalue = - if (!analyze_mono) then lv - else - begin - let l' = fresh_label () in - let t' = fresh_var_i () in - instantiate_label(lv.l,(i,Pos),l'); - add_constraint (Instantiation (lv.contents,(i,Pos),t')); - make_lval(l',t') (* check -- fresh label ?? *) - end - -(** Constraint generated from assigning [t] to [lv]. *) -let assign (lv : lvalue) (t : tau) : unit = - add_constraint (Unification (lv.contents,t)) - - -(** Project out the first (ref) component or a pair. If the argument [t] has - no discovered structure, raise No_contents. *) -let proj_ref (t : tau) : tau = - match U.deref t with - | Pair p -> p.ptr - | Var v -> raise No_contents - | _ -> raise Bad_proj - -(* Project out the second (fun) component of a pair. If the argument [t] has - no discovered structure, create it on the fly by adding constraints. *) -let proj_fun (t : tau) : tau = - match U.deref t with - | Pair p -> p.lam - | Var v -> - let p,f = fresh_var(), fresh_var() in - add_constraint (Unification (t,make_pair(p,f))); - f - | _ -> raise Bad_proj - -let get_args (t : tau) : tau list ref = - match U.deref t with - | Fun f -> f.args - | _ -> raise (Inconsistent("get_args")) - -(** Function type [t] is applied to the arguments [actuals]. Unifies the - actuals with the formals of [t]. If no functions have been discovered for - [t] yet, create a fresh one and unify it with t. The result is the return - value of the function. *) -let apply (t : tau) (al : tau list) : tau = - let f = proj_fun(t) in - let actuals = ref al in - let formals,ret = - match U.deref f with - | Fun fi -> (fi.args),fi.ret - | Var v -> - let new_l,new_ret,new_args = - fresh_label(), fresh_var (), - List.map (function _ -> fresh_var()) (!actuals) - in - let new_fun = make_fun(new_l,new_args,new_ret) in - add_constraint (Unification(new_fun,f)); - (get_args new_fun,new_ret) - | Ref _ -> raise (Inconsistent ("apply_ref")) - | Pair _ -> raise (Inconsistent ("apply_pair")) - | Wild -> raise (Inconsistent("apply_wild")) - in - pad_args(formals,actuals); - List.iter2 (fun actual -> fun formal -> - add_constraint (Unification (actual,formal)) - ) !actuals !formals; - ret - -(** Create a new function type with name [name], list of formal arguments - [formals], and return value [ret]. Adds no constraints. *) -let make_function (name : string) (formals : lvalue list) (ret : tau) : tau = - let - f = make_fun(make_label(name),List.map (fun x -> rvalue x) formals, ret) - in - make_pair(fresh_var(),f) - -(** Create an lvalue. If [is_global] is true, the lvalue will be treated - monomorphically. *) -let make_lvalue (is_global : bool) (name : string) : lvalue = - if (!debug && is_global) - then - Printf.printf "Making global lvalue : %s\n" name - else (); - make_lval(make_label(name), make_var is_global name) - - -(** Create a fresh non-global named variable. *) -let make_fresh (name : string) : tau = - make_var false (name) - -(** The default type for constants. *) -let bottom () : tau = - make_var false ("bottom") - -(** Unify the result of a function with its return value. *) -let return (t : tau) (t' : tau) = - add_constraint (Unification (t,t')) - - -(***********************************************************************) -(* *) -(* Query/Extract Solutions *) -(* *) -(***********************************************************************) - -(** Unify the data stored in two label bounds. *) -let combine_lbounds (s,s' : label boundset * label boundset) = - B.union s s' - -(** Truncates a list of urefs [l] to those elements up to and including the - first occurence of the specified element [elt]. *) -let truncate l elt = - let keep = ref true in - List.filter - (fun x -> - if (not (!keep)) - then - false - else - begin - if (U.equal(x,elt)) - then - keep := false - else (); - true - end - ) l - -let debug_cycle_bounds is_pos c = - let rec debug_cycle_bounds' = function - | h :: [] -> - Printf.printf "%s --> %s\n" (string_of_bounds is_pos h) - (string_of_label2 h) - | h :: t -> - begin - Printf.printf "%s --> %s\n" (string_of_bounds is_pos h) - (string_of_label2 h); - debug_cycle_bounds' t - end - | [] -> () - in - debug_cycle_bounds' c - -(** For debugging, print a cycle of instantiations *) -let debug_cycle (is_pos,c,l,p) = - let kind = if is_pos then "P" else "N" in - let rec string_of_cycle = function - | h :: [] -> string_of_label2 h - | [] -> "" - | h :: t -> Printf.sprintf "%s,%s" (string_of_label2 h) (string_of_cycle t) - in - Printf.printf "Collapsing %s cycle around %s:\n" kind (string_of_label2 l); - Printf.printf "Elements are: %s\n" (string_of_cycle c); - Printf.printf "Per-element bounds:\n"; - debug_cycle_bounds is_pos c; - Printf.printf "Full path is: %s" (string_of_cycle p); - print_newline() - -(** Compute pos or neg flow, depending on [is_pos]. Searches for cycles in the - instantiations (can these even occur?) and unifies either the positive or - negative edge sets for the labels on the cycle. Note that this does not - ever unify the labels themselves. The return is the new bounds of the - argument label *) -let rec flow (is_pos : bool) (path : label list) (l : label) : label boundset = - let collapse_cycle () = - let cycle = truncate path l in - debug_cycle (is_pos,cycle,l,path); - List.iter (fun x -> U.unify combine_lbounds - ((get_bounds is_pos x),get_bounds is_pos l) - ) cycle - in - if (on_path l) - then - begin - collapse_cycle (); - (* set_on_path l false; *) - B.empty - end - else - if ( (is_pos && (U.deref l).p_cached) || - ( (not is_pos) && (U.deref l).n_cached) ) then - begin - U.deref (get_bounds is_pos l) - end - else - begin - let newbounds = ref B.empty in - let base = get_bounds is_pos l in - set_on_path l true; - if (is_pos) then - (U.deref l).p_cached <- true - else - (U.deref l).n_cached <- true; - B.iter - (fun x -> - if (U.equal(x.info,l)) then () - else - (newbounds := - (B.union (!newbounds) (flow is_pos (l :: path) x.info))) - ) (U.deref base); - set_on_path l false; - U.update (base,(B.union (U.deref base) !newbounds)); - U.deref base - end - -(** Compute and cache any positive flow. *) -let pos_flow l : constantset = - let result = ref C.empty in - begin - ignore (flow true [] l); - B.iter (fun x -> result := C.union (!result) (U.deref(x.info)).aliases ) - (U.deref (get_bounds true l)); - !result - end - -(** Compute and cache any negative flow. *) -let neg_flow l : constantset = - let result = ref C.empty in - begin - ignore (flow false [] l); - B.iter (fun x -> result := C.union (!result) (U.deref(x.info)).aliases ) - (U.deref (get_bounds false l)); - !result - end - -(** Compute and cache any pos-neg flow. Assumes that both pos_flow and - neg_flow have been computed for the label [l]. *) -let pos_neg_flow(l : label) : constantset = - let result = ref C.empty in - begin - B.iter (fun x -> result := C.union (!result) (pos_flow x.info)) - (U.deref (get_bounds false l)); - !result - end - -(** Compute a points-to set by computing positive, then negative, then - positive-negative flow for a label. *) -let points_to_int (lv : lvalue) : constantset = - let visited_caches : cache list ref = ref [] in - let rec points_to_tau (t : tau) : constantset = - try - begin - match U.deref (proj_ref t) with - | Var v -> C.empty - | Ref r -> - begin - let pos = pos_flow r.rl in - let neg = neg_flow r.rl in - let interproc = C.union (pos_neg_flow r.rl) (C.union pos neg) - in - C.union ((U.deref(r.rl)).aliases) interproc - end - | _ -> raise (Inconsistent ("points_to")) - end - with - | No_contents -> - begin - match (U.deref t) with - | Var v -> rebuild_flow v.v_cache - | _ -> raise (Inconsistent ("points_to")) - end - and rebuild_flow (c : cache) : constantset = - if (List.mem c (!visited_caches) ) (* cyclic instantiations *) - then - begin - (* visited_caches := List.tl (!visited_caches); *) (* check *) - C.empty - end - else - begin - visited_caches := c :: (!visited_caches); - let result = ref (C.empty) in - H.iter (fun _ -> fun(p,t) -> - match p with - | Pos -> () - | _ -> result := C.union (!result) (points_to_tau t) - ) c; - visited_caches := List.tl (!visited_caches); - !result - end - in - if (!no_flow) then - (U.deref lv.l).aliases - else - points_to_tau (lv.contents) - -let points_to (lv : lvalue) : string list = - List.map snd (C.elements (points_to_int lv)) - -let alias_query (a_progress : bool) (lv : lvalue list) : int * int = - (0,0) (* todo *) -(* - let a_count = ref 0 in - let ptsets = List.map points_to_int lv in - let total_sets = List.length ptsets in - let counted_sets = ref 0 in - let record_alias s s' = - if (C.is_empty (C.inter s s')) - then () - else (incr a_count) - in - let rec check_alias = function - | h :: t -> - begin - List.iter (record_alias h) ptsets; - check_alias t - end - | [] -> () - in - check_alias ptsets; - !a_count -*) |