diff options
Diffstat (limited to 'cil/src/ext/pta/golf.ml')
| -rw-r--r-- | cil/src/ext/pta/golf.ml | 1657 |
1 files changed, 1657 insertions, 0 deletions
diff --git a/cil/src/ext/pta/golf.ml b/cil/src/ext/pta/golf.ml new file mode 100644 index 0000000..5ea47ff --- /dev/null +++ b/cil/src/ext/pta/golf.ml @@ -0,0 +1,1657 @@ +(* + * + * 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. + * + *) + +(***********************************************************************) +(* *) +(* Exceptions *) +(* *) +(***********************************************************************) + +exception Inconsistent (* raised if constraint system is inconsistent *) +exception WellFormed (* raised if types are not well-formed *) +exception NoContents +exception APFound (* raised if an alias pair is found, a control + flow exception *) + + +module U = Uref +module S = Setp +module H = Hashtbl +module Q = Queue + + +(** Subtyping kinds *) +type polarity = + Pos + | Neg + | Sub + +(** Path kinds, for CFL reachability *) +type pkind = + Positive + | Negative + | Match + | Seed + +(** Context kinds -- open or closed *) +type context = + Open + | Closed + +(* A configuration is a context (open or closed) coupled with a pair + of stamps representing a state in the cartesian product DFA. *) +type configuration = context * int * int + +module ConfigHash = +struct + type t = configuration + let equal t t' = t = t' + let hash t = Hashtbl.hash t +end + +module CH = H.Make (ConfigHash) + +type config_map = unit CH.t + +(** Generic bounds *) +type 'a bound = {index : int; info : 'a U.uref} + +(** For label paths. *) +type 'a path = { + kind : pkind; + reached_global : bool; + head : 'a U.uref; + tail : 'a U.uref +} + +module Bound = +struct + type 'a t = 'a bound + let compare (x : 'a t) (y : 'a t) = + if U.equal (x.info, y.info) then x.index - y.index + else Pervasives.compare (U.deref x.info) (U.deref y.info) +end + +module Path = +struct + type 'a t = 'a path + let compare (x : 'a t) (y : 'a t) = + if U.equal (x.head, y.head) then + begin + if U.equal (x.tail, y.tail) then + begin + if x.reached_global = y.reached_global then + Pervasives.compare x.kind y.kind + else Pervasives.compare x.reached_global y.reached_global + end + else Pervasives.compare (U.deref x.tail) (U.deref y.tail) + end + else Pervasives.compare (U.deref x.head) (U.deref y.head) +end + +module B = S.Make (Bound) + +module P = S.Make (Path) + +type 'a boundset = 'a B.t + +type 'a pathset = 'a P.t + +(** Constants, which identify elements in points-to sets *) +(** jk : I'd prefer to make this an 'a constant and specialize it to varinfo + for use with the Cil frontend, but for now, this will do *) +type constant = int * string * Cil.varinfo + +module Constant = +struct + type t = constant + let compare (xid, _, _) (yid, _, _) = 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; + (** either empty or a singleton, the initial location for this label *) + loc : constantset; + (** Name of this label *) + l_stamp : int; + (** Unique integer for this label *) + mutable l_global : bool; + (** True if this location is globally accessible *) + mutable aliases: constantset; + (** Set of constants (tags) for checking aliases *) + mutable p_lbounds: lblinfo boundset; + (** Set of umatched (p) lower bounds *) + mutable n_lbounds: lblinfo boundset; + (** Set of unmatched (n) lower bounds *) + mutable p_ubounds: lblinfo boundset; + (** Set of umatched (p) upper bounds *) + mutable n_ubounds: lblinfo boundset; + (** Set of unmatched (n) upper bounds *) + mutable m_lbounds: lblinfo boundset; + (** Set of matched (m) lower bounds *) + mutable m_ubounds: lblinfo boundset; + (** Set of matched (m) upper bounds *) + + mutable m_upath: lblinfo pathset; + mutable m_lpath: lblinfo pathset; + mutable n_upath: lblinfo pathset; + mutable n_lpath: lblinfo pathset; + mutable p_upath: lblinfo pathset; + mutable p_lpath: lblinfo pathset; + + mutable l_seeded : bool; + mutable l_ret : bool; + mutable l_param : bool; +} + +(** Constructor labels *) +and label = lblinfo U.uref + +(** The type of lvalues. *) +type lvalue = { + l: label; + contents: tau +} + +and vinfo = { + v_stamp : int; + v_name : string; + + mutable v_hole : (int,unit) H.t; + mutable v_global : bool; + mutable v_mlbs : tinfo boundset; + mutable v_mubs : tinfo boundset; + mutable v_plbs : tinfo boundset; + mutable v_pubs : tinfo boundset; + mutable v_nlbs : tinfo boundset; + mutable v_nubs : tinfo boundset +} + +and rinfo = { + r_stamp : int; + rl : label; + points_to : tau; + mutable r_global: bool; +} + +and finfo = { + f_stamp : int; + fl : label; + ret : tau; + mutable args : tau list; + mutable f_global : bool; +} + +and pinfo = { + p_stamp : int; + ptr : tau; + lam : tau; + mutable p_global : bool; +} + +and tinfo = Var of vinfo + | Ref of rinfo + | Fun of finfo + | Pair of pinfo + +and tau = tinfo U.uref + +type tconstraint = Unification of tau * tau + | Leq of tau * (int * polarity) * 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 + +module PathHash = +struct + type t = int list + let equal t t' = t = t' + let hash t = Hashtbl.hash t +end + +module PH = H.Make (PathHash) + +(***********************************************************************) +(* *) +(* Global Variables *) +(* *) +(***********************************************************************) + +(** Print the instantiations constraints. *) +let print_constraints : bool ref = ref false + +(** If true, print all constraints (including induced) and show + additional debug output. *) +let debug = ref false + +(** Just debug all the constraints (including induced) *) +let debug_constraints = ref false + +(** Debug smart alias queries *) +let debug_aliases = ref false + +let smart_aliases = ref false + +(** If true, make the flow step a no-op *) +let no_flow = ref false + +(** If true, disable subtyping (unification at all levels) *) +let no_sub = ref false + +(** If true, treat indexed edges as regular subtyping *) +let analyze_mono = ref true + +(** A list of equality constraints. *) +let eq_worklist : tconstraint Q.t = Q.create () + +(** A list of leq constraints. *) +let leq_worklist : tconstraint Q.t = Q.create () + +let path_worklist : (lblinfo path) Q.t = Q.create () + +let path_hash : (lblinfo path) PH.t = PH.create 32 + +(** A count of the constraints introduced from the AST. Used for debugging. *) +let toplev_count = ref 0 + +(** A hashtable containing stamp pairs of labels that must be aliased. *) +let cached_aliases : (int * int,unit) H.t = H.create 64 + +(** A hashtable mapping pairs of tau's to their join node. *) +let join_cache : (int * int, tau) H.t = H.create 64 + +(***********************************************************************) +(* *) +(* Utility Functions *) +(* *) +(***********************************************************************) + +let find = U.deref + +let die s = + Printf.printf "*******\nAssertion failed: %s\n*******\n" s; + assert false + +let fresh_appsite : (unit -> int) = + let appsite_index = ref 0 in + fun () -> + incr appsite_index; + !appsite_index + +(** Generate a unique integer. *) +let fresh_index : (unit -> int) = + let counter = ref 0 in + fun () -> + incr counter; + !counter + +let fresh_stamp : (unit -> int) = + let stamp = ref 0 in + fun () -> + incr stamp; + !stamp + +(** Return a unique integer representation of a tau *) +let get_stamp (t : tau) : int = + match find t with + Var v -> v.v_stamp + | Ref r -> r.r_stamp + | Pair p -> p.p_stamp + | Fun f -> f.f_stamp + +(** Negate a polarity. *) +let negate (p : polarity) : polarity = + match p with + Pos -> Neg + | Neg -> Pos + | Sub -> die "negate" + +(** Consistency checks for inferred types *) +let pair_or_var (t : tau) = + match find t with + Pair _ -> true + | Var _ -> true + | _ -> false + +let ref_or_var (t : tau) = + match find t with + Ref _ -> true + | Var _ -> true + | _ -> false + +let fun_or_var (t : tau) = + match find t with + Fun _ -> true + | Var _ -> true + | _ -> false + + + +(** Apply [f] structurally down [t]. Guaranteed to terminate, even if [t] + is recursive *) +let iter_tau f t = + let visited : (int,tau) H.t = H.create 4 in + let rec iter_tau' t = + if H.mem visited (get_stamp t) then () else + begin + f t; + H.add visited (get_stamp t) t; + match U.deref t with + Pair p -> + iter_tau' p.ptr; + iter_tau' p.lam + | Fun f -> + List.iter iter_tau' (f.args); + iter_tau' f.ret + | Ref r -> iter_tau' r.points_to + | _ -> () + end + in + iter_tau' t + +(* Extract a label's bounds according to [positive] and [upper]. *) +let get_bounds (p :polarity ) (upper : bool) (l : label) : lblinfo boundset = + let li = find l in + match p with + Pos -> if upper then li.p_ubounds else li.p_lbounds + | Neg -> if upper then li.n_ubounds else li.n_lbounds + | Sub -> if upper then li.m_ubounds else li.m_lbounds + +let equal_tau (t : tau) (t' : tau) = + get_stamp t = get_stamp t' + +let get_label_stamp (l : label) : int = + (find l).l_stamp + +(** Return true if [t] is global (treated monomorphically) *) +let get_global (t : tau) : bool = + match find t with + Var v -> v.v_global + | Ref r -> r.r_global + | Pair p -> p.p_global + | Fun f -> f.f_global + +let is_ret_label l = (find l).l_ret || (find l).l_global (* todo - check *) + +let is_param_label l = (find l).l_param || (find l).l_global + +let is_global_label l = (find l).l_global + +let is_seeded_label l = (find l).l_seeded + +let set_global_label (l : label) (b : bool) : unit = + assert ((not (is_global_label l)) || b); + (U.deref l).l_global <- b + +(** Aliases for set_global *) +let global_tau = get_global + + +(** Get_global for lvalues *) +let global_lvalue lv = get_global lv.contents + + + +(***********************************************************************) +(* *) +(* Printing Functions *) +(* *) +(***********************************************************************) + +let string_of_configuration (c, i, i') = + let context = match c with + Open -> "O" + | Closed -> "C" + in + Printf.sprintf "(%s,%d,%d)" context i i' + +let string_of_polarity p = + match p with + Pos -> "+" + | Neg -> "-" + | Sub -> "M" + +(** Convert a label to a string, short representation *) +let string_of_label (l : label) : string = + "\"" ^ (find l).l_name ^ "\"" + +(** Return true if the element [e] is present in the association list, + according to uref equality *) +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 find t with + Pair p -> "rvp" ^ string_of_int p.p_stamp + | Ref r -> "rvr" ^ string_of_int r.r_stamp + | Fun f -> "rvf" ^ string_of_int f.f_stamp + | _ -> die "fresh_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 -> + let rv = fresh_recvar_name t in + s := "u " ^ rv ^ "." ^ !s; + so := Some rv; + rv + | Some rv -> rv + end + | None -> (* type's not recursive. Add it to the assoc list and cont. *) + let s = ref "" + and so : string option ref = ref None in + tau_map := (t, s, so) :: !tau_map; + begin + match find t with + Var v -> s := v.v_name; + | Pair p -> + 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 ^"}" + | Ref r -> + 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 ^ ")" + | Fun f -> + assert (pair_or_var f.ret); + let rec string_of_args = function + h :: [] -> + assert (pair_or_var h); + s := !s ^ string_of_tau' h + | h :: t -> + assert (pair_or_var h); + s := !s ^ string_of_tau' h ^ ","; + string_of_args t + | [] -> () + 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 + 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 + and l = string_of_label lv.l in + assert (pair_or_var lv.contents); (* do a consistency check *) + Printf.sprintf "[%s]^(%s)" contents l + +let print_path (p : lblinfo path) : unit = + let string_of_pkind = function + Positive -> "p" + | Negative -> "n" + | Match -> "m" + | Seed -> "s" + in + Printf.printf + "%s --%s--> %s (%d) : " + (string_of_label p.head) + (string_of_pkind p.kind) + (string_of_label p.tail) + (PathHash.hash p) + +(** Print a list of tau elements, comma separated *) +let rec print_tau_list (l : tau list) : unit = + let rec print_t_strings = function + h :: [] -> print_endline h + | h :: t -> + print_string h; + print_string ", "; + print_t_strings t + | [] -> () + in + print_t_strings (List.map string_of_tau l) + +let print_constraint (c : tconstraint) = + match c with + Unification (t, t') -> + let lhs = string_of_tau t + and rhs = string_of_tau t' in + Printf.printf "%s == %s\n" lhs rhs + | Leq (t, (i, p), t') -> + let lhs = string_of_tau t + and rhs = string_of_tau t' in + Printf.printf "%s <={%d,%s} %s\n" lhs i (string_of_polarity p) rhs + +(***********************************************************************) +(* *) +(* Type Operations -- these do not create any constraints *) +(* *) +(***********************************************************************) + +(** Create an lvalue with label [lbl] and tau contents [t]. *) +let make_lval (lbl, t : label * tau) : lvalue = + {l = lbl; contents = t} + +let make_label_int (is_global : bool) (name :string) (vio : Cil.varinfo option) : label = + let locc = + match vio with + Some vi -> C.add (fresh_index (), name, vi) C.empty + | None -> C.empty + in + U.uref { + l_name = name; + l_global = is_global; + l_stamp = fresh_stamp (); + loc = locc; + aliases = locc; + p_ubounds = B.empty; + p_lbounds = B.empty; + n_ubounds = B.empty; + n_lbounds = B.empty; + m_ubounds = B.empty; + m_lbounds = B.empty; + m_upath = P.empty; + m_lpath = P.empty; + n_upath = P.empty; + n_lpath = P.empty; + p_upath = P.empty; + p_lpath = P.empty; + l_seeded = false; + l_ret = false; + l_param = false + } + +(** Create a new label with name [name]. Also adds a fresh constant + with name [name] to this label's aliases set. *) +let make_label (is_global : bool) (name : string) (vio : Cil.varinfo option) : label = + make_label_int is_global name vio + +(** Create a new label with an unspecified name and an empty alias set. *) +let fresh_label (is_global : bool) : label = + let index = fresh_index () in + make_label_int is_global ("l_" ^ string_of_int index) None + +(** Create a fresh bound (edge in the constraint graph). *) +let make_bound (i, a : int * label) : lblinfo bound = + {index = i; info = a} + +let make_tau_bound (i, a : int * tau) : tinfo 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_hole = H.create 8; + v_stamp = fresh_index (); + v_global = b; + v_mlbs = B.empty; + v_mubs = B.empty; + v_plbs = B.empty; + v_pubs = B.empty; + v_nlbs = B.empty; + v_nubs = B.empty}) + +(** Create a fresh unnamed variable (name will be 'fv). *) +let fresh_var (is_global : bool) : tau = + make_var is_global ("fv" ^ string_of_int (fresh_index ())) + +(** Create a fresh unnamed variable (name will be 'fi). *) +let fresh_var_i (is_global : bool) : tau = + make_var is_global ("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_stamp = fresh_index (); + f_global = false; + args = a; + ret = r }) + +(** Create a Ref constructor. *) +let make_ref (lbl,pt : label * tau) : tau = + U.uref (Ref {rl = lbl; + r_stamp = fresh_index (); + r_global = false; + points_to = pt}) + +(** Create a Pair constructor. *) +let make_pair (p,f : tau * tau) : tau = + U.uref (Pair {ptr = p; + p_stamp = fresh_index (); + p_global = false; + lam = f}) + +(** Copy the toplevel constructor of [t], putting fresh variables in each + argement of the constructor. *) +let copy_toplevel (t : tau) : tau = + match find t with + Pair _ -> make_pair (fresh_var_i false, fresh_var_i false) + | Ref _ -> make_ref (fresh_label false, fresh_var_i false) + | Fun f -> + let fresh_fn = fun _ -> fresh_var_i false in + make_fun (fresh_label false, + List.map fresh_fn f.args, fresh_var_i false) + | _ -> die "copy_toplevel" + + +let has_same_structure (t : tau) (t' : tau) = + match find t, find t' with + Pair _, Pair _ -> true + | Ref _, Ref _ -> true + | Fun _, Fun _ -> true + | Var _, Var _ -> true + | _ -> false + + +let pad_args (f, f' : finfo * finfo) : unit = + let padding = ref ((List.length f.args) - (List.length f'.args)) + in + if !padding == 0 then () + else + let to_pad = + if !padding > 0 then f' else (padding := -(!padding); f) + in + for i = 1 to !padding do + to_pad.args <- to_pad.args @ [fresh_var false] + done + + +let pad_args2 (fi, tlr : finfo * tau list ref) : unit = + let padding = ref (List.length fi.args - List.length !tlr) + in + if !padding == 0 then () + else + if !padding > 0 then + for i = 1 to !padding do + tlr := !tlr @ [fresh_var false] + done + else + begin + padding := -(!padding); + for i = 1 to !padding do + fi.args <- fi.args @ [fresh_var false] + done + end + +(***********************************************************************) +(* *) +(* Constraint Generation/ Resolution *) +(* *) +(***********************************************************************) + + +(** Make the type a global type *) +let set_global (t : tau) (b : bool) : unit = + let set_global_down t = + match find t with + Var v -> v.v_global <- true + | Ref r -> set_global_label r.rl true + | Fun f -> set_global_label f.fl true + | _ -> () + in + if !debug && b then Printf.printf "Set global: %s\n" (string_of_tau t); + assert ((not (get_global t)) || b); + if b then iter_tau set_global_down t; + match find t with + Var v -> v.v_global <- b + | Ref r -> r.r_global <- b + | Pair p -> p.p_global <- b + | Fun f -> f.f_global <- b + + +let rec unify_int (t, t' : tau * tau) : unit = + if equal_tau t t' then () + else + let ti, ti' = find t, find t' in + U.unify combine (t, t'); + match ti, ti' with + Var v, Var v' -> + set_global t' (v.v_global || get_global t'); + merge_vholes (v, v'); + merge_vlbs (v, v'); + merge_vubs (v, v') + | Var v, _ -> + set_global t' (v.v_global || get_global t'); + trigger_vhole v t'; + notify_vlbs t v; + notify_vubs t v + | _, Var v -> + set_global t (v.v_global || get_global t); + trigger_vhole v t; + notify_vlbs t' v; + notify_vubs t' v + | Ref r, Ref r' -> + set_global t (r.r_global || r'.r_global); + unify_ref (r, r') + | Fun f, Fun f' -> + set_global t (f.f_global || f'.f_global); + unify_fun (f, f') + | Pair p, Pair p' -> () + | _ -> raise Inconsistent +and notify_vlbs (t : tau) (vi : vinfo) : unit = + let notify p bounds = + List.iter + (fun b -> + add_constraint (Unification (b.info,copy_toplevel t)); + add_constraint (Leq (b.info, (b.index, p), t))) + bounds + in + notify Sub (B.elements vi.v_mlbs); + notify Pos (B.elements vi.v_plbs); + notify Neg (B.elements vi.v_nlbs) +and notify_vubs (t : tau) (vi : vinfo) : unit = + let notify p bounds = + List.iter + (fun b -> + add_constraint (Unification (b.info,copy_toplevel t)); + add_constraint (Leq (t, (b.index, p), b.info))) + bounds + in + notify Sub (B.elements vi.v_mubs); + notify Pos (B.elements vi.v_pubs); + notify Neg (B.elements vi.v_nubs) +and unify_ref (ri,ri' : rinfo * rinfo) : unit = + add_constraint (Unification (ri.points_to, ri'.points_to)) +and unify_fun (fi, fi' : finfo * finfo) : unit = + let rec union_args = function + _, [] -> false + | [], _ -> true + | h :: t, h' :: t' -> + add_constraint (Unification (h, h')); + union_args(t, t') + in + unify_label(fi.fl, fi'.fl); + add_constraint (Unification (fi.ret, fi'.ret)); + if union_args (fi.args, fi'.args) then fi.args <- fi'.args; +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 rm_self b = not (li.l_stamp = get_label_stamp b.info) + in + pick_name (li, li'); + li.l_global <- li.l_global || li'.l_global; + li.aliases <- C.union li.aliases li'.aliases; + li.p_ubounds <- B.union li.p_ubounds li'.p_ubounds; + li.p_lbounds <- B.union li.p_lbounds li'.p_lbounds; + li.n_ubounds <- B.union li.n_ubounds li'.n_ubounds; + li.n_lbounds <- B.union li.n_lbounds li'.n_lbounds; + li.m_ubounds <- B.union li.m_ubounds (B.filter rm_self li'.m_ubounds); + li.m_lbounds <- B.union li.m_lbounds (B.filter rm_self li'.m_lbounds); + li.m_upath <- P.union li.m_upath li'.m_upath; + li.m_lpath<- P.union li.m_lpath li'.m_lpath; + li.n_upath <- P.union li.n_upath li'.n_upath; + li.n_lpath <- P.union li.n_lpath li'.n_lpath; + li.p_upath <- P.union li.p_upath li'.p_upath; + li.p_lpath <- P.union li.p_lpath li'.p_lpath; + li.l_seeded <- li.l_seeded || li'.l_seeded; + li.l_ret <- li.l_ret || li'.l_ret; + li.l_param <- li.l_param || li'.l_param; + li + in + if !debug_constraints then + Printf.printf "%s == %s\n" (string_of_label l) (string_of_label l'); + U.unify combine_label (l, l') +and merge_vholes (vi, vi' : vinfo * vinfo) : unit = + H.iter + (fun i -> fun _ -> H.replace vi'.v_hole i ()) + vi.v_hole +and merge_vlbs (vi, vi' : vinfo * vinfo) : unit = + vi'.v_mlbs <- B.union vi.v_mlbs vi'.v_mlbs; + vi'.v_plbs <- B.union vi.v_plbs vi'.v_plbs; + vi'.v_nlbs <- B.union vi.v_nlbs vi'.v_nlbs +and merge_vubs (vi, vi' : vinfo * vinfo) : unit = + vi'.v_mubs <- B.union vi.v_mubs vi'.v_mubs; + vi'.v_pubs <- B.union vi.v_pubs vi'.v_pubs; + vi'.v_nubs <- B.union vi.v_nubs vi'.v_nubs +and trigger_vhole (vi : vinfo) (t : tau) = + let add_self_loops (t : tau) : unit = + match find t with + Var v -> + H.iter + (fun i -> fun _ -> H.replace v.v_hole i ()) + vi.v_hole + | Ref r -> + H.iter + (fun i -> fun _ -> + leq_label (r.rl, (i, Pos), r.rl); + leq_label (r.rl, (i, Neg), r.rl)) + vi.v_hole + | Fun f -> + H.iter + (fun i -> fun _ -> + leq_label (f.fl, (i, Pos), f.fl); + leq_label (f.fl, (i, Neg), f.fl)) + vi.v_hole + | _ -> () + in + iter_tau add_self_loops 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. + All other actions (e.g., updating the info) is done in unify_int *) +and combine (ti, ti' : tinfo * tinfo) : tinfo = + match ti, ti' with + Var _, _ -> ti' + | _, _ -> ti +and leq_int (t, (i, p), t') : unit = + if equal_tau t t' then () + else + let ti, ti' = find t, find t' in + match ti, ti' with + Var v, Var v' -> + begin + match p with + Pos -> + v.v_pubs <- B.add (make_tau_bound (i, t')) v.v_pubs; + v'.v_plbs <- B.add (make_tau_bound (i, t)) v'.v_plbs + | Neg -> + v.v_nubs <- B.add (make_tau_bound (i, t')) v.v_nubs; + v'.v_nlbs <- B.add (make_tau_bound (i, t)) v'.v_nlbs + | Sub -> + v.v_mubs <- B.add (make_tau_bound (i, t')) v.v_mubs; + v'.v_mlbs <- B.add (make_tau_bound (i, t)) v'.v_mlbs + end + | Var v, _ -> + add_constraint (Unification (t, copy_toplevel t')); + add_constraint (Leq (t, (i, p), t')) + | _, Var v -> + add_constraint (Unification (t', copy_toplevel t)); + add_constraint (Leq (t, (i, p), t')) + | Ref r, Ref r' -> leq_ref (r, (i, p), r') + | Fun f, Fun f' -> add_constraint (Unification (t, t')) + | Pair pr, Pair pr' -> + add_constraint (Leq (pr.ptr, (i, p), pr'.ptr)); + add_constraint (Leq (pr.lam, (i, p), pr'.lam)) + | _ -> raise Inconsistent +and leq_ref (ri, (i, p), ri') : unit = + let add_self_loops (t : tau) : unit = + match find t with + Var v -> H.replace v.v_hole i () + | Ref r -> + leq_label (r.rl, (i, Pos), r.rl); + leq_label (r.rl, (i, Neg), r.rl) + | Fun f -> + leq_label (f.fl, (i, Pos), f.fl); + leq_label (f.fl, (i, Neg), f.fl) + | _ -> () + in + iter_tau add_self_loops ri.points_to; + add_constraint (Unification (ri.points_to, ri'.points_to)); + leq_label(ri.rl, (i, p), ri'.rl) +and leq_label (l,(i, p), l') : unit = + if !debug_constraints then + Printf.printf + "%s <={%d,%s} %s\n" + (string_of_label l) i (string_of_polarity p) (string_of_label l'); + let li, li' = find l, find l' in + match p with + Pos -> + li.l_ret <- true; + li.p_ubounds <- B.add (make_bound (i, l')) li.p_ubounds; + li'.p_lbounds <- B.add (make_bound (i, l)) li'.p_lbounds + | Neg -> + li'.l_param <- true; + li.n_ubounds <- B.add (make_bound (i, l')) li.n_ubounds; + li'.n_lbounds <- B.add (make_bound (i, l)) li'.n_lbounds + | Sub -> + if U.equal (l, l') then () + else + begin + li.m_ubounds <- B.add (make_bound(0, l')) li.m_ubounds; + li'.m_lbounds <- B.add (make_bound(0, l)) li'.m_lbounds + end +and add_constraint_int (c : tconstraint) (toplev : bool) = + if !debug_constraints && toplev then + begin + Printf.printf "%d:>" !toplev_count; + print_constraint c; + incr toplev_count + end + else + if !debug_constraints then print_constraint c else (); + begin + match c with + Unification _ -> Q.add c eq_worklist + | Leq _ -> Q.add c leq_worklist + end; + solve_constraints () +and add_constraint (c : tconstraint) = + add_constraint_int c false +and add_toplev_constraint (c : tconstraint) = + if !print_constraints && not !debug_constraints then + begin + Printf.printf "%d:>" !toplev_count; + incr toplev_count; + print_constraint c + end + else (); + add_constraint_int c true +and fetch_constraint () : tconstraint option = + try Some (Q.take eq_worklist) + with Q.Empty -> (try Some (Q.take leq_worklist) + with Q.Empty -> None) +(** The main solver loop. *) +and solve_constraints () : unit = + match fetch_constraint () with + Some c -> + begin + match c with + Unification (t, t') -> unify_int (t, t') + | Leq (t, (i, p), t') -> + if !no_sub then unify_int (t, t') + else + if !analyze_mono then leq_int (t, (0, Sub), t') + else leq_int (t, (i, p), t') + end; + solve_constraints () + | 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 -> + begin + match U.deref p.ptr with + Var _ -> + let is_global = global_tau p.ptr in + let points_to = fresh_var is_global in + let l = fresh_label is_global in + let r = make_ref (l, points_to) + in + add_toplev_constraint (Unification (p.ptr, r)); + make_lval (l, points_to) + | Ref r -> make_lval (r.rl, r.points_to) + | _ -> raise WellFormed + end + | Var v -> + let is_global = global_tau t in + add_toplev_constraint + (Unification (t, make_pair (fresh_var is_global, + fresh_var is_global))); + deref t + | _ -> raise WellFormed + +(** Form the union of [t] and [t'], if it doesn't exist already. *) +let join (t : tau) (t' : tau) : tau = + try H.find join_cache (get_stamp t, get_stamp t') + with Not_found -> + let t'' = fresh_var false in + add_toplev_constraint (Leq (t, (0, Sub), t'')); + add_toplev_constraint (Leq (t', (0, Sub), t'')); + H.add join_cache (get_stamp t, get_stamp 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 false in + List.iter + (fun t -> add_toplev_constraint (Leq (t, (0, Sub), t'))) + tl; + t' + +(** 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 false) + +(** For this version of golf, instantiation is handled at [apply] *) +let instantiate (lv : lvalue) (i : int) : lvalue = + lv + +(** Constraint generated from assigning [t] to [lv]. *) +let assign (lv : lvalue) (t : tau) : unit = + add_toplev_constraint (Leq (t, (0, Sub), lv.contents)) + +let assign_ret (i : int) (lv : lvalue) (t : tau) : unit = + add_toplev_constraint (Leq (t, (i, Pos), lv.contents)) + +(** Project out the first (ref) component or a pair. If the argument [t] has + no discovered structure, raise NoContents. *) +let proj_ref (t : tau) : tau = + match U.deref t with + Pair p -> p.ptr + | Var v -> raise NoContents + | _ -> raise WellFormed + +(* 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 false, fresh_var false in + add_toplev_constraint (Unification (t, make_pair(p, f))); + f + | _ -> raise WellFormed + +let get_args (t : tau) : tau list = + match U.deref t with + Fun f -> f.args + | _ -> raise WellFormed + +let get_finfo (t : tau) : finfo = + match U.deref t with + Fun f -> f + | _ -> raise WellFormed + +(** 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 plus the index of this application site. *) +let apply (t : tau) (al : tau list) : (tau * int) = + let i = fresh_appsite () in + let f = proj_fun t in + let actuals = ref al in + let fi,ret = + match U.deref f with + Fun fi -> fi, fi.ret + | Var v -> + let new_l, new_ret, new_args = + fresh_label false, fresh_var false, + List.map (function _ -> fresh_var false) !actuals + in + let new_fun = make_fun (new_l, new_args, new_ret) in + add_toplev_constraint (Unification (new_fun, f)); + (get_finfo new_fun, new_ret) + | _ -> raise WellFormed + in + pad_args2 (fi, actuals); + List.iter2 + (fun actual -> fun formal -> + add_toplev_constraint (Leq (actual,(i, Neg), formal))) + !actuals fi.args; + (ret, i) + +(** 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 false name None, + List.map (fun x -> rvalue x) formals, + ret) + in + make_pair (fresh_var false, f) + +(** Create an lvalue. If [is_global] is true, the lvalue will be treated + monomorphically. *) +let make_lvalue (is_global : bool) (name : string) (vio : Cil.varinfo option) : lvalue = + if !debug && is_global then + Printf.printf "Making global lvalue : %s\n" name + else (); + make_lval (make_label is_global name vio, 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_toplev_constraint (Leq (t', (0, Sub), t)) + +(***********************************************************************) +(* *) +(* Query/Extract Solutions *) +(* *) +(***********************************************************************) + +let make_summary = leq_label + +let path_signature k l l' b : int list = + let ksig = + match k with + Positive -> 1 + | Negative -> 2 + | _ -> 3 + in + [ksig; + get_label_stamp l; + get_label_stamp l'; + if b then 1 else 0] + +let make_path (k, l, l', b) = + let psig = path_signature k l l' b in + if PH.mem path_hash psig then () + else + let new_path = {kind = k; head = l; tail = l'; reached_global = b} + and li, li' = find l, find l' in + PH.add path_hash psig new_path; + Q.add new_path path_worklist; + begin + match k with + Positive -> + li.p_upath <- P.add new_path li.p_upath; + li'.p_lpath <- P.add new_path li'.p_lpath + | Negative -> + li.n_upath <- P.add new_path li.n_upath; + li'.n_lpath <- P.add new_path li'.n_lpath + | _ -> + li.m_upath <- P.add new_path li.m_upath; + li'.m_lpath <- P.add new_path li'.m_lpath + end; + if !debug then + begin + print_string "Discovered path : "; + print_path new_path; + print_newline () + end + +let backwards_tabulate (l : label) : unit = + let rec loop () = + let rule1 p = + if !debug then print_endline "rule1"; + B.iter + (fun lb -> + make_path (Match, lb.info, p.tail, + p.reached_global || is_global_label p.head)) + (find p.head).m_lbounds + and rule2 p = + if !debug then print_endline "rule2"; + B.iter + (fun lb -> + make_path (Negative, lb.info, p.tail, + p.reached_global || is_global_label p.head)) + (find p.head).n_lbounds + and rule2m p = + if !debug then print_endline "rule2m"; + B.iter + (fun lb -> + make_path (Match, lb.info, p.tail, + p.reached_global || is_global_label p.head)) + (find p.head).n_lbounds + and rule3 p = + if !debug then print_endline "rule3"; + B.iter + (fun lb -> + make_path (Positive, lb.info, p.tail, + p.reached_global || is_global_label p.head)) + (find p.head).p_lbounds + and rule4 p = + if !debug then print_endline "rule4"; + B.iter + (fun lb -> + make_path(Negative, lb.info, p.tail, + p.reached_global || is_global_label p.head)) + (find p.head).m_lbounds + and rule5 p = + if !debug then print_endline "rule5"; + B.iter + (fun lb -> + make_path (Positive, lb.info, p.tail, + p.reached_global || is_global_label p.head)) + (find p.head).m_lbounds + and rule6 p = + if !debug then print_endline "rule6"; + B.iter + (fun lb -> + if is_seeded_label lb.info then () + else + begin + (find lb.info).l_seeded <- true; (* set seeded *) + make_path (Seed, lb.info, lb.info, + is_global_label lb.info) + end) + (find p.head).p_lbounds + and rule7 p = + if !debug then print_endline "rule7"; + if not (is_ret_label p.tail && is_param_label p.head) then () + else + B.iter + (fun lb -> + B.iter + (fun ub -> + if lb.index = ub.index then + begin + if !debug then + Printf.printf "New summary : %s %s\n" + (string_of_label lb.info) + (string_of_label ub.info); + make_summary (lb.info, (0, Sub), ub.info); + (* rules 1, 4, and 5 *) + P.iter + (fun ubp -> (* rule 1 *) + make_path (Match, lb.info, ubp.tail, + ubp.reached_global)) + (find ub.info).m_upath; + P.iter + (fun ubp -> (* rule 4 *) + make_path (Negative, lb.info, ubp.tail, + ubp.reached_global)) + (find ub.info).n_upath; + P.iter + (fun ubp -> (* rule 5 *) + make_path (Positive, lb.info, ubp.tail, + ubp.reached_global)) + (find ub.info).p_upath + end) + (find p.tail).p_ubounds) + (find p.head).n_lbounds + in + let matched_backward_rules p = + rule1 p; + if p.reached_global then rule2m p else rule2 p; + rule3 p; + rule6 p; + rule7 p + and negative_backward_rules p = + rule2 p; + rule3 p; + rule4 p; + rule6 p; + rule7 p + and positive_backward_rules p = + rule3 p; + rule5 p; + rule6 p; + rule7 p + in (* loop *) + if Q.is_empty path_worklist then () + else + let p = Q.take path_worklist in + if !debug then + begin + print_string "Processing path: "; + print_path p; + print_newline () + end; + begin + match p.kind with + Positive -> + if is_global_label p.tail then matched_backward_rules p + else positive_backward_rules p + | Negative -> negative_backward_rules p + | _ -> matched_backward_rules p + end; + loop () + in (* backwards_tabulate *) + if !debug then + begin + Printf.printf "Tabulating for %s..." (string_of_label l); + if is_global_label l then print_string "(global)"; + print_newline () + end; + make_path (Seed, l, l, is_global_label l); + loop () + +let collect_ptsets (l : label) : constantset = (* todo -- cache aliases *) + let li = find l + and collect init s = + P.fold (fun x a -> C.union a (find x.head).aliases) s init + in + backwards_tabulate l; + collect (collect (collect li.aliases li.m_lpath) li.n_lpath) li.p_lpath + +let extract_ptlabel (lv : lvalue) : label option = + try + match find (proj_ref lv.contents) with + Var v -> None + | Ref r -> Some r.rl; + | _ -> raise WellFormed + with NoContents -> None + +let points_to_aux (t : tau) : constant list = + try + match find (proj_ref t) with + Var v -> [] + | Ref r -> C.elements (collect_ptsets r.rl) + | _ -> raise WellFormed + with NoContents -> [] + +let points_to_names (lv : lvalue) : string list = + List.map (fun (_, str, _) -> str) (points_to_aux lv.contents) + +let points_to (lv : lvalue) : Cil.varinfo list = + let rec get_vinfos l : Cil.varinfo list = match l with + | (_, _, h) :: t -> h :: get_vinfos t + | [] -> [] + in + get_vinfos (points_to_aux lv.contents) + +let epoints_to (t : tau) : Cil.varinfo list = + let rec get_vinfos l : Cil.varinfo list = match l with + | (_, _, h) :: t -> h :: get_vinfos t + | [] -> [] + in + get_vinfos (points_to_aux t) + +let smart_alias_query (l : label) (l' : label) : bool = + (* Set of dead configurations *) + let dead_configs : config_map = CH.create 16 in + (* the set of discovered configurations *) + let discovered : config_map = CH.create 16 in + let rec filter_match (i : int) = + B.filter (fun (b : lblinfo bound) -> i = b.index) + in + let rec simulate c l l' = + let config = (c, get_label_stamp l, get_label_stamp l') in + if U.equal (l, l') then + begin + if !debug then + Printf.printf + "%s and %s are aliased\n" + (string_of_label l) + (string_of_label l'); + raise APFound + end + else if CH.mem discovered config then () + else + begin + if !debug_aliases then + Printf.printf + "Exploring configuration %s\n" + (string_of_configuration config); + CH.add discovered config (); + B.iter + (fun lb -> simulate c lb.info l') + (get_bounds Sub false l); (* epsilon closure of l *) + B.iter + (fun lb -> simulate c l lb.info) + (get_bounds Sub false l'); (* epsilon closure of l' *) + B.iter + (fun lb -> + let matching = + filter_match lb.index (get_bounds Pos false l') + in + B.iter + (fun b -> simulate Closed lb.info b.info) + matching; + if is_global_label l' then (* positive self-loops on l' *) + simulate Closed lb.info l') + (get_bounds Pos false l); (* positive transitions on l *) + if is_global_label l then + B.iter + (fun lb -> simulate Closed l lb.info) + (get_bounds Pos false l'); (* positive self-loops on l *) + begin + match c with (* negative transitions on l, only if Open *) + Open -> + B.iter + (fun lb -> + let matching = + filter_match lb.index (get_bounds Neg false l') + in + B.iter + (fun b -> simulate Open lb.info b.info) + matching ; + if is_global_label l' then (* neg self-loops on l' *) + simulate Open lb.info l') + (get_bounds Neg false l); + if is_global_label l then + B.iter + (fun lb -> simulate Open l lb.info) + (get_bounds Neg false l') (* negative self-loops on l *) + | _ -> () + end; + (* if we got this far, then the configuration was not used *) + CH.add dead_configs config (); + end + in + try + begin + if H.mem cached_aliases (get_label_stamp l, get_label_stamp l') then + true + else + begin + simulate Open l l'; + if !debug then + Printf.printf + "%s and %s are NOT aliased\n" + (string_of_label l) + (string_of_label l'); + false + end + end + with APFound -> + CH.iter + (fun config -> fun _ -> + if not (CH.mem dead_configs config) then + H.add + cached_aliases + (get_label_stamp l, get_label_stamp l') + ()) + discovered; + true + +(** todo : uses naive alias query for now *) +let may_alias (t1 : tau) (t2 : tau) : bool = + try + let l1 = + match find (proj_ref t1) with + Ref r -> r.rl + | Var v -> raise NoContents + | _ -> raise WellFormed + and l2 = + match find (proj_ref t2) with + Ref r -> r.rl + | Var v -> raise NoContents + | _ -> raise WellFormed + in + not (C.is_empty (C.inter (collect_ptsets l1) (collect_ptsets l2))) + with NoContents -> false + +let alias_query (b : bool) (lvl : lvalue list) : int * int = + let naive_count = ref 0 in + let smart_count = ref 0 in + let lbls = List.map extract_ptlabel lvl in (* label option list *) + let ptsets = + List.map + (function + Some l -> collect_ptsets l + | None -> C.empty) + lbls in + let record_alias s lo s' lo' = + match lo, lo' with + Some l, Some l' -> + if !debug_aliases then + Printf.printf + "Checking whether %s and %s are aliased...\n" + (string_of_label l) + (string_of_label l'); + if C.is_empty (C.inter s s') then () + else + begin + incr naive_count; + if !smart_aliases && smart_alias_query l l' then + incr smart_count + end + | _ -> () + in + let rec check_alias sets labels = + match sets,labels with + s :: st, l :: lt -> + List.iter2 (record_alias s l) ptsets lbls; + check_alias st lt + | [], [] -> () + | _ -> die "check_alias" + in + check_alias ptsets lbls; + (!naive_count, !smart_count) + +let alias_frequency (lvl : (lvalue * bool) list) : int * int = + let extract_lbl (lv, b : lvalue * bool) = (lv.l, b) in + let naive_count = ref 0 in + let smart_count = ref 0 in + let lbls = List.map extract_lbl lvl in + let ptsets = + List.map + (fun (lbl, b) -> + if b then (find lbl).loc (* symbol access *) + else collect_ptsets lbl) + lbls in + let record_alias s (l, b) s' (l', b') = + if !debug_aliases then + Printf.printf + "Checking whether %s and %s are aliased...\n" + (string_of_label l) + (string_of_label l'); + if C.is_empty (C.inter s s') then () + else + begin + if !debug_aliases then + Printf.printf + "%s and %s are aliased naively...\n" + (string_of_label l) + (string_of_label l'); + incr naive_count; + if !smart_aliases then + if b || b' || smart_alias_query l l' then incr smart_count + else + Printf.printf + "%s and %s are not aliased by smart queries...\n" + (string_of_label l) + (string_of_label l'); + end + in + let rec check_alias sets labels = + match sets, labels with + s :: st, l :: lt -> + List.iter2 (record_alias s l) ptsets lbls; + check_alias st lt + | [], [] -> () + | _ -> die "check_alias" + in + check_alias ptsets lbls; + (!naive_count, !smart_count) + + +(** an interface for extracting abstract locations from this analysis *) + +type absloc = label + +let absloc_of_lvalue (l : lvalue) : absloc = l.l +let absloc_eq (a1, a2) = smart_alias_query a1 a2 +let absloc_print_name = ref true +let d_absloc () (p : absloc) = + let a = find p in + if !absloc_print_name then Pretty.dprintf "%s" a.l_name + else Pretty.dprintf "%d" a.l_stamp + +let phonyAddrOf (lv : lvalue) : lvalue = + make_lval (fresh_label true, address lv) + +(* transitive closure of points to, starting from l *) +let rec tauPointsTo (l : tau) : absloc list = + match find l with + Var _ -> [] + | Ref r -> r.rl :: tauPointsTo r.points_to + | _ -> [] + +let rec absloc_points_to (l : lvalue) : absloc list = + tauPointsTo l.contents + + +(** The following definitions are only introduced for the + compatability with Olf. *) + +exception UnknownLocation + +let finished_constraints () = () +let apply_undefined (_ : tau list) = (fresh_var true, 0) +let assign_undefined (_ : lvalue) = () + +let absloc_epoints_to = tauPointsTo |