diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-03-29 09:47:11 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-03-29 09:47:11 +0000 |
commit | a5f03d96eee482cd84861fc8cefff9eb451c0cad (patch) | |
tree | cbc66cbc183a7c5ef2c044ed9ed04b8011df9cd4 /cil/src/ext/pta | |
parent | a9621943087a5578c995d88b06f87c5158eb5d00 (diff) | |
download | compcert-a5f03d96eee482cd84861fc8cefff9eb451c0cad.tar.gz compcert-a5f03d96eee482cd84861fc8cefff9eb451c0cad.zip |
Cleaned up configure script.
Distribution of CIL as an expanded source tree with changes applied
(instead of original .tar.gz + patches to be applied at config time).
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1020 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cil/src/ext/pta')
-rw-r--r-- | cil/src/ext/pta/golf.ml | 1657 | ||||
-rw-r--r-- | cil/src/ext/pta/golf.mli | 83 | ||||
-rw-r--r-- | cil/src/ext/pta/olf.ml | 1108 | ||||
-rw-r--r-- | cil/src/ext/pta/olf.mli | 80 | ||||
-rw-r--r-- | cil/src/ext/pta/ptranal.ml | 597 | ||||
-rw-r--r-- | cil/src/ext/pta/ptranal.mli | 156 | ||||
-rw-r--r-- | cil/src/ext/pta/setp.ml | 342 | ||||
-rw-r--r-- | cil/src/ext/pta/setp.mli | 180 | ||||
-rw-r--r-- | cil/src/ext/pta/steensgaard.ml | 1417 | ||||
-rw-r--r-- | cil/src/ext/pta/steensgaard.mli | 71 | ||||
-rw-r--r-- | cil/src/ext/pta/uref.ml | 94 | ||||
-rw-r--r-- | cil/src/ext/pta/uref.mli | 65 |
12 files changed, 5850 insertions, 0 deletions
diff --git a/cil/src/ext/pta/golf.ml b/cil/src/ext/pta/golf.ml new file mode 100644 index 00000000..5ea47ff1 --- /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 diff --git a/cil/src/ext/pta/golf.mli b/cil/src/ext/pta/golf.mli new file mode 100644 index 00000000..569855c5 --- /dev/null +++ b/cil/src/ext/pta/golf.mli @@ -0,0 +1,83 @@ +(* + * + * 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. + * + *) +type lvalue +type tau +type absloc + +(* only for compatability with Olf *) +exception UnknownLocation + +val debug : bool ref +val debug_constraints : bool ref +val debug_aliases : bool ref +val smart_aliases : bool ref +val finished_constraints : unit -> unit (* only for compatability with Olf *) +val print_constraints : bool ref +val no_flow : bool ref +val no_sub : bool ref +val analyze_mono : bool ref +val solve_constraints : unit -> unit +val rvalue : lvalue -> tau +val deref : tau -> lvalue +val join : tau -> tau -> tau +val join_inits : tau list -> tau +val address : lvalue -> tau +val instantiate : lvalue -> int -> lvalue +val assign : lvalue -> tau -> unit +val assign_ret : int -> lvalue -> tau -> unit +val apply : tau -> tau list -> (tau * int) +val apply_undefined : tau list -> (tau * int) (* only for compatability with Olf *) +val assign_undefined : lvalue -> unit (* only for compatability with Olf *) +val make_function : string -> lvalue list -> tau -> tau +val make_lvalue : bool -> string -> (Cil.varinfo option) -> lvalue +val bottom : unit -> tau +val return : tau -> tau -> unit +val make_fresh : string -> tau +val points_to_names : lvalue -> string list +val points_to : lvalue -> Cil.varinfo list +val epoints_to : tau -> Cil.varinfo list +val string_of_lvalue : lvalue -> string +val global_lvalue : lvalue -> bool +val alias_query : bool -> lvalue list -> int * int +val alias_frequency : (lvalue * bool) list -> int * int + +val may_alias : tau -> tau -> bool + +val absloc_points_to : lvalue -> absloc list +val absloc_epoints_to : tau -> absloc list +val absloc_of_lvalue : lvalue -> absloc +val absloc_eq : (absloc * absloc) -> bool +val d_absloc : unit -> absloc -> Pretty.doc +val phonyAddrOf : lvalue -> lvalue diff --git a/cil/src/ext/pta/olf.ml b/cil/src/ext/pta/olf.ml new file mode 100644 index 00000000..0d770028 --- /dev/null +++ b/cil/src/ext/pta/olf.ml @@ -0,0 +1,1108 @@ +(* + * + * 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 *) +exception ReachedTop (* raised if top (from an undefined function) + flows to a c_absloc during the flow step *) +exception UnknownLocation + +let solve_constraints () = () (* only for compatability with Golf *) + +open Cil + +module U = Uref +module S = Setp +module H = Hashtbl +module Q = Queue + +(** Generic bounds *) +type 'a bound = {info : 'a U.uref} + +module Bound = +struct + type 'a t = 'a bound + let compare (x : 'a t) (y : 'a t) = + Pervasives.compare (U.deref x.info) (U.deref y.info) +end + +module B = S.Make (Bound) + +type 'a boundset = 'a B.t + +(** Abslocs, which identify elements in points-to sets *) +(** jk : I'd prefer to make this an 'a absloc and specialize it to + varinfo for use with the Cil frontend, but for now, this will do *) +type absloc = int * string * Cil.varinfo option + +module Absloc = +struct + type t = absloc + let compare (xid, _, _) (yid, _, _) = xid - yid +end + +module C = Set.Make (Absloc) + +(** Sets of abslocs. Set union is used when two c_abslocs containing + absloc sets are unified *) +type abslocset = C.t + +let d_absloc () (a: absloc) : Pretty.doc = + let i,s,_ = a in + Pretty.dprintf "<%d, %s>" i s + +type c_abslocinfo = { + mutable l_name: string; (** name of the location *) + loc : absloc; + l_stamp : int; + mutable l_top : bool; + mutable aliases : abslocset; + mutable lbounds : c_abslocinfo boundset; + mutable ubounds : c_abslocinfo boundset; + mutable flow_computed : bool +} +and c_absloc = c_abslocinfo U.uref + +(** The type of lvalues. *) +type lvalue = { + l: c_absloc; + contents: tau +} +and vinfo = { + v_stamp : int; + v_name : string; + mutable v_top : bool; + mutable v_lbounds : tinfo boundset; + mutable v_ubounds : tinfo boundset +} +and rinfo = { + r_stamp : int; + rl : c_absloc; + points_to : tau +} +and finfo = { + f_stamp : int; + fl : c_absloc; + ret : tau; + mutable args : tau list +} +and pinfo = { + p_stamp : int; + ptr : tau; + lam : tau +} +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 * 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 + +(** The current state of the solver engine either adding more + constraints, or finished adding constraints and querying graph *) +type state = + AddingConstraints + | FinishedConstraints + +(***********************************************************************) +(* *) +(* Global Variables *) +(* *) +(***********************************************************************) + +(** A count of the constraints introduced from the AST. Used for + debugging. *) +let toplev_count = ref 0 + +let solver_state : state ref = ref AddingConstraints + +(** 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 the flow step *) +let debug_flow_step = ref false + +(** Compatibility with GOLF *) +let debug_aliases = ref false +let smart_aliases = ref false +let no_flow = ref false +let analyze_mono = ref false + +(** If true, disable subtyping (unification at all levels) *) +let no_sub = ref false + +(** 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 () + +(** A hashtable containing stamp pairs of c_abslocs 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 + +(** *) +let label_prefix = "l_" + + +(***********************************************************************) +(* *) +(* Utility Functions *) +(* *) +(***********************************************************************) + +let starts_with s p = + let n = String.length p in + if String.length s < n then false + else String.sub s 0 n = p + + +let die s = + Printf.printf "*******\nAssertion failed: %s\n*******\n" s; + assert false + +let insist b s = + if not b then die s else () + + +let can_add_constraints () = + !solver_state = AddingConstraints + +let can_query_graph () = + !solver_state = FinishedConstraints + +let finished_constraints () = + insist (!solver_state = AddingConstraints) "inconsistent states"; + solver_state := FinishedConstraints + +let find = U.deref + +(** return the prefix of the list up to and including the first + element satisfying p. if no element satisfies p, return the empty + list *) +let rec keep_until p l = + match l with + [] -> [] + | x :: xs -> if p x then [x] else x :: keep_until p xs + + +(** 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 + +(** 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 find 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 + +let equal_absloc = function + (i, _, _), (i', _, _) -> i = i' + +let equal_c_absloc l l' = + (find l).l_stamp = (find l').l_stamp + +let equal_tau (t : tau) (t' : tau) = + get_stamp t = get_stamp t' + +let top_c_absloc l = + (find l).l_top + +let get_flow_computed l = + (find l).flow_computed + +let set_flow_computed l = + (find l).flow_computed <- true + +let rec top_tau (t : tau) = + match find t with + Pair p -> top_tau p.ptr || top_tau p.lam + | Ref r -> top_c_absloc r.rl + | Fun f -> top_c_absloc f.fl + | Var v -> v.v_top + +let get_c_absloc_stamp (l : c_absloc) : int = + (find l).l_stamp + +let set_top_c_absloc (l : c_absloc) (b: bool) : unit = + (find l).l_top <- b + +let get_aliases (l : c_absloc) = + if top_c_absloc l then raise ReachedTop + else (find l).aliases + +(***********************************************************************) +(* *) +(* Printing Functions *) +(* *) +(***********************************************************************) + +(** Convert a c_absloc to a string, short representation *) +let string_of_c_absloc (l : c_absloc) : string = + "\"" ^ + (find l).l_name ^ + if top_c_absloc l then "(top)" else "" ^ + "\"" + +(** 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 -> + insist (ref_or_var p.ptr) "wellformed"; + insist (fun_or_var p.lam) "wellformed"; + s := "{"; + s := !s ^ string_of_tau' p.ptr; + s := !s ^ ","; + s := !s ^ string_of_tau' p.lam; + s := !s ^ "}" + | Ref r -> + insist (pair_or_var r.points_to) "wellformed"; + s := "ref(|"; + s := !s ^ string_of_c_absloc r.rl; + s := !s ^ "|,"; + s := !s ^ string_of_tau' r.points_to; + s := !s ^ ")" + | Fun f -> + let rec string_of_args = function + [] -> () + | h :: [] -> + insist (pair_or_var h) "wellformed"; + s := !s ^ string_of_tau' h + | h :: t -> + insist (pair_or_var h) "wellformed"; + s := !s ^ string_of_tau' h ^ ","; + string_of_args t + in + insist (pair_or_var f.ret) "wellformed"; + s := "fun(|"; + s := !s ^ string_of_c_absloc 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_c_absloc lv.l + in + insist (pair_or_var lv.contents) "inconsistency at string_of_lvalue"; + (* do a consistency check *) + Printf.sprintf "[%s]^(%s)" contents l + +(** 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 in + let rhs = string_of_tau t' in + Printf.printf "%s == %s\n" lhs rhs + | Leq (t, t') -> + let lhs = string_of_tau t in + let rhs = string_of_tau t' in + Printf.printf "%s <= %s\n" lhs rhs + +(***********************************************************************) +(* *) +(* Type Operations -- these do not create any constraints *) +(* *) +(***********************************************************************) + +(** Create an lvalue with c_absloc [lbl] and tau contents [t]. *) +let make_lval (loc, t : c_absloc * tau) : lvalue = + {l = loc; contents = t} + +let make_c_absloc_int (is_top : bool) (name : string) (vio : Cil.varinfo option) : c_absloc = + let my_absloc = (fresh_index (), name, vio) in + let locc = C.add my_absloc C.empty + in + U.uref { + l_name = name; + l_top = is_top; + l_stamp = fresh_stamp (); + loc = my_absloc; + aliases = locc; + ubounds = B.empty; + lbounds = B.empty; + flow_computed = false + } + +(** Create a new c_absloc with name [name]. Also adds a fresh absloc + with name [name] to this c_absloc's aliases set. *) +let make_c_absloc (is_top : bool) (name : string) (vio : Cil.varinfo option) = + make_c_absloc_int is_top name vio + +let fresh_c_absloc (is_top : bool) : c_absloc = + let index = fresh_index () in + make_c_absloc_int is_top (label_prefix ^ string_of_int index) None + +(** Create a fresh bound (edge in the constraint graph). *) +let make_bound (a : c_absloc) : c_abslocinfo bound = + {info = a} + +let make_tau_bound (t : tau) : tinfo bound = + {info = t} + +(** Create a fresh named variable with name '[name]. *) +let make_var (is_top : bool) (name : string) : tau = + U.uref (Var {v_name = ("'" ^ name); + v_top = is_top; + v_stamp = fresh_index (); + v_lbounds = B.empty; + v_ubounds = B.empty}) + +let fresh_var (is_top : bool) : tau = + make_var is_top ("fi" ^ string_of_int (fresh_index ())) + +(** Create a fresh unnamed variable (name will be 'fi). *) +let fresh_var_i (is_top : bool) : tau = + make_var is_top ("fi" ^ string_of_int (fresh_index ())) + +(** Create a Fun constructor. *) +let make_fun (lbl, a, r : c_absloc * (tau list) * tau) : tau = + U.uref (Fun {fl = lbl; + f_stamp = fresh_index (); + args = a; + ret = r}) + +(** Create a Ref constructor. *) +let make_ref (lbl, pt : c_absloc * tau) : tau = + U.uref (Ref {rl = lbl; + r_stamp = fresh_index (); + points_to = pt}) + +(** Create a Pair constructor. *) +let make_pair (p, f : tau * tau) : tau = + U.uref (Pair {ptr = p; + p_stamp = fresh_index (); + 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_c_absloc false, fresh_var_i false) + | Fun f -> + make_fun (fresh_c_absloc false, + List.map (fun _ -> fresh_var_i false) 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 (fi, tlr : finfo * tau list ref) : unit = + let padding = 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 + for i = 1 to -padding do + fi.args <- fi.args @ [fresh_var false] + done + +(***********************************************************************) +(* *) +(* Constraint Generation/ Resolution *) +(* *) +(***********************************************************************) + +let set_top (b : bool) (t : tau) : unit = + let set_top_down t = + match find t with + Var v -> v.v_top <- b + | Ref r -> set_top_c_absloc r.rl b + | Fun f -> set_top_c_absloc f.fl b + | Pair p -> () + in + iter_tau set_top_down t + +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_top (v.v_top || v'.v_top) t'; + merge_v_lbounds (v, v'); + merge_v_ubounds (v, v') + | Var v, _ -> + set_top (v.v_top || top_tau t') t'; + notify_vlbounds t v; + notify_vubounds t v + | _, Var v -> + set_top (v.v_top || top_tau t) t; + notify_vlbounds t' v; + notify_vubounds t' v + | Ref r, Ref r' -> unify_ref (r, r') + | Fun f, Fun f' -> unify_fun (f, f') + | Pair p, Pair p' -> unify_pair (p, p') + | _ -> raise Inconsistent +and notify_vlbounds (t : tau) (vi : vinfo) : unit = + let notify bounds = + List.iter + (fun b -> + add_constraint (Unification (b.info, copy_toplevel t)); + add_constraint (Leq (b.info, t))) + bounds + in + notify (B.elements vi.v_lbounds) +and notify_vubounds (t : tau) (vi : vinfo) : unit = + let notify bounds = + List.iter + (fun b -> + add_constraint (Unification (b.info, copy_toplevel t)); + add_constraint (Leq (t, b.info))) + bounds + in + notify (B.elements vi.v_ubounds) +and unify_ref (ri, ri' : rinfo * rinfo) : unit = + unify_c_abslocs (ri.rl, ri'.rl); + 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_c_abslocs (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_pair (pi, pi' : pinfo * pinfo) : unit = + add_constraint (Unification (pi.ptr, pi'.ptr)); + add_constraint (Unification (pi.lam, pi'.lam)) +and unify_c_abslocs (l, l' : c_absloc * c_absloc) : unit = + let pick_name (li, li' : c_abslocinfo * c_abslocinfo) = + if starts_with li.l_name label_prefix then li.l_name <- li'.l_name + else () in + let combine_c_absloc (li, li' : c_abslocinfo * c_abslocinfo) : c_abslocinfo = + pick_name (li, li'); + li.l_top <- li.l_top || li'.l_top; + li.aliases <- C.union li.aliases li'.aliases; + li.ubounds <- B.union li.ubounds li'.ubounds; + li.lbounds <- B.union li.lbounds li'.lbounds; + li + in + if !debug_constraints then + Printf.printf + "%s == %s\n" + (string_of_c_absloc l) + (string_of_c_absloc l'); + U.unify combine_c_absloc (l, l') +and merge_v_lbounds (vi, vi' : vinfo * vinfo) : unit = + vi'.v_lbounds <- B.union vi.v_lbounds vi'.v_lbounds; +and merge_v_ubounds (vi, vi' : vinfo * vinfo) : unit = + vi'.v_ubounds <- B.union vi.v_ubounds vi'.v_ubounds; +(** 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, 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' -> + v.v_ubounds <- B.add (make_tau_bound t') v.v_ubounds; + v'.v_lbounds <- B.add (make_tau_bound t) v'.v_lbounds + | Var v, _ -> + add_constraint (Unification (t, copy_toplevel t')); + add_constraint (Leq (t, t')) + | _, Var v -> + add_constraint (Unification (t', copy_toplevel t)); + add_constraint (Leq (t, t')) + | Ref r, Ref r' -> leq_ref (r, r') + | Fun f, Fun f' -> + (* TODO: check, why not do subtyping here? *) + add_constraint (Unification (t, t')) + | Pair pr, Pair pr' -> + add_constraint (Leq (pr.ptr, pr'.ptr)); + add_constraint (Leq (pr.lam, pr'.lam)) + | _ -> raise Inconsistent +and leq_ref (ri, ri') : unit = + leq_c_absloc (ri.rl, ri'.rl); + add_constraint (Unification (ri.points_to, ri'.points_to)) +and leq_c_absloc (l, l') : unit = + let li, li' = find l, find l' in + if !debug_constraints then + Printf.printf + "%s <= %s\n" + (string_of_c_absloc l) + (string_of_c_absloc l'); + if U.equal (l, l') then () + else + begin + li.ubounds <- B.add (make_bound l') li.ubounds; + li'.lbounds <- B.add (make_bound l) li'.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 (); + insist (can_add_constraints ()) + "can't add constraints after compute_results is called"; + begin + match c with + Unification _ -> Q.add c eq_worklist + | Leq _ -> Q.add c leq_worklist + end; + solve_constraints () (* solve online *) +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 -> + begin + try Some (Q.take leq_worklist) + with Q.Empty -> None + end +(** The main solver loop. *) +and solve_constraints () : unit = + match fetch_constraint () with + None -> () + | Some c -> + begin + match c with + Unification (t, t') -> unify_int (t, t') + | Leq (t, t') -> + if !no_sub then unify_int (t, t') + else leq_int (t, t') + end; + solve_constraints () + +(***********************************************************************) +(* *) +(* 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 find t with + Pair p -> + begin + match find p.ptr with + | Var _ -> + let is_top = top_tau p.ptr in + let points_to = fresh_var is_top in + let l = fresh_c_absloc is_top 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_top = top_tau t in + add_toplev_constraint + (Unification (t, make_pair (fresh_var is_top, fresh_var is_top))); + deref t + | _ -> raise WellFormed + + +(** Form the union of [t] and [t'], if it doesn't exist already. *) +let join (t : tau) (t' : tau) : tau = + let s, s' = get_stamp t, get_stamp t' in + try H.find join_cache (s, s') + with Not_found -> + let t'' = fresh_var false in + add_toplev_constraint (Leq (t, t'')); + add_toplev_constraint (Leq (t', t'')); + H.add join_cache (s, s') 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 (function t -> add_toplev_constraint (Leq (t, 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 ) + +(** No instantiation in this analysis *) +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, lv.contents)) + +let assign_ret (i : int) (lv : lvalue) (t : tau) : unit = + add_toplev_constraint (Leq (t, 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 find 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 find 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 find t with + Fun f -> f.args + | _ -> raise WellFormed + +let get_finfo (t : tau) : finfo = + match find 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. + + For this analysis, the application site is always 0 *) +let apply (t : tau) (al : tau list) : (tau * int) = + let f = proj_fun t in + let actuals = ref al in + let fi, ret = + match find f with + Fun fi -> fi, fi.ret + | Var v -> + let new_l, new_ret, new_args = + fresh_c_absloc 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_args (fi, actuals); + List.iter2 + (fun actual -> fun formal -> + add_toplev_constraint (Leq (actual, formal))) + !actuals fi.args; + (ret, 0) + +let make_undefined_lvalue () = + make_lval (make_c_absloc false "undefined" None, + make_var true "undefined") + +let make_undefined_rvalue () = + make_var true "undefined" + +let assign_undefined (lv : lvalue) : unit = + assign lv (make_undefined_rvalue ()) + +let apply_undefined (al : tau list) : (tau * int) = + List.iter + (fun actual -> assign (make_undefined_lvalue ()) actual) + al; + (fresh_var true, 0) + +(** 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_c_absloc false name None, + List.map (fun x -> rvalue x) formals, + ret) + in + make_pair (fresh_var false, f) + +(** Create an lvalue. *) +let make_lvalue (b : bool ) (name : string) (vio : Cil.varinfo option) = + make_lval (make_c_absloc false name vio, + make_var false name) + +(** Create a fresh named variable. *) +let make_fresh (name : string) : tau = + make_var false name + +(** The default type for abslocs. *) +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', t)) + +(***********************************************************************) +(* *) +(* Query/Extract Solutions *) +(* *) +(***********************************************************************) + +module IntHash = Hashtbl.Make (struct + type t = int + let equal x y = x = y + let hash x = x + end) + +(** todo : reached_top !! *) +let collect_ptset_fast (l : c_absloc) : abslocset = + let onpath : unit IntHash.t = IntHash.create 101 in + let path : c_absloc list ref = ref [] in + let compute_path (i : int) = + keep_until (fun l -> i = get_c_absloc_stamp l) !path in + let collapse_cycle (cycle : c_absloc list) = + match cycle with + l :: ls -> + List.iter (fun l' -> unify_c_abslocs (l, l')) ls; + C.empty + | [] -> die "collapse cycle" in + let rec flow_step (l : c_absloc) : abslocset = + let stamp = get_c_absloc_stamp l in + if IntHash.mem onpath stamp then (* already seen *) + collapse_cycle (compute_path stamp) + else + let li = find l in + IntHash.add onpath stamp (); + path := l :: !path; + B.iter + (fun lb -> li.aliases <- C.union li.aliases (flow_step lb.info)) + li.lbounds; + path := List.tl !path; + IntHash.remove onpath stamp; + li.aliases + in + insist (can_query_graph ()) "collect_ptset_fast can't query graph"; + if get_flow_computed l then get_aliases l + else + begin + set_flow_computed l; + flow_step l + end + +(** this is a quadratic flow step. keep it for debugging the fast + version above. *) +let collect_ptset_slow (l : c_absloc) : abslocset = + let onpath : unit IntHash.t = IntHash.create 101 in + let rec flow_step (l : c_absloc) : abslocset = + if top_c_absloc l then raise ReachedTop + else + let stamp = get_c_absloc_stamp l in + if IntHash.mem onpath stamp then C.empty + else + let li = find l in + IntHash.add onpath stamp (); + B.iter + (fun lb -> li.aliases <- C.union li.aliases (flow_step lb.info)) + li.lbounds; + li.aliases + in + insist (can_query_graph ()) "collect_ptset_slow can't query graph"; + if get_flow_computed l then get_aliases l + else + begin + set_flow_computed l; + flow_step l + end + +let collect_ptset = + collect_ptset_slow + (* if !debug_flow_step then collect_ptset_slow + else collect_ptset_fast *) + +let may_alias (t1 : tau) (t2 : tau) : bool = + let get_l (t : tau) : c_absloc = + match find (proj_ref t) with + Ref r -> r.rl + | Var v -> raise NoContents + | _ -> raise WellFormed + in + try + let l1 = get_l t1 + and l2 = get_l t2 in + equal_c_absloc l1 l2 || + not (C.is_empty (C.inter (collect_ptset l1) (collect_ptset l2))) + with + NoContents -> false + | ReachedTop -> raise UnknownLocation + +let points_to_aux (t : tau) : absloc list = + try + match find (proj_ref t) with + Var v -> [] + | Ref r -> C.elements (collect_ptset r.rl) + | _ -> raise WellFormed + with + NoContents -> [] + | ReachedTop -> raise UnknownLocation + +let points_to (lv : lvalue) : Cil.varinfo list = + let rec get_vinfos l : Cil.varinfo list = + match l with + [] -> [] + | (_, _, Some h) :: t -> h :: get_vinfos t + | (_, _, None) :: t -> 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 + [] -> [] + | (_, _, Some h) :: t -> h :: get_vinfos t + | (_, _, None) :: t -> get_vinfos t + in + get_vinfos (points_to_aux t) + +let points_to_names (lv : lvalue) : string list = + List.map (fun v -> v.vname) (points_to lv) + +let absloc_points_to (lv : lvalue) : absloc list = + points_to_aux lv.contents + +let absloc_epoints_to (t : tau) : absloc list = + points_to_aux t + +let absloc_of_lvalue (lv : lvalue) : absloc = + (find lv.l).loc + +let absloc_eq = equal_absloc diff --git a/cil/src/ext/pta/olf.mli b/cil/src/ext/pta/olf.mli new file mode 100644 index 00000000..43794825 --- /dev/null +++ b/cil/src/ext/pta/olf.mli @@ -0,0 +1,80 @@ +(* + * + * 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. + * + *) +type lvalue +type tau +type absloc + +(** Raised if a pointer flows to an undefined function. + We assume that such a function can have any effect on the pointer's contents +*) +exception UnknownLocation + +val debug : bool ref +val debug_constraints : bool ref +val debug_aliases : bool ref +val smart_aliases : bool ref +val finished_constraints : unit -> unit +val print_constraints : bool ref +val no_flow : bool ref +val no_sub : bool ref +val analyze_mono : bool ref +val solve_constraints : unit -> unit (* only for compatability with Golf *) +val rvalue : lvalue -> tau +val deref : tau -> lvalue +val join : tau -> tau -> tau +val join_inits : tau list -> tau +val address : lvalue -> tau +val instantiate : lvalue -> int -> lvalue +val assign : lvalue -> tau -> unit +val assign_ret : int -> lvalue -> tau -> unit +val apply : tau -> tau list -> (tau * int) +val apply_undefined : tau list -> (tau * int) +val assign_undefined : lvalue -> unit +val make_function : string -> lvalue list -> tau -> tau +val make_lvalue : bool -> string -> (Cil.varinfo option) -> lvalue +val bottom : unit -> tau +val return : tau -> tau -> unit +val make_fresh : string -> tau +val points_to_names : lvalue -> string list +val points_to : lvalue -> Cil.varinfo list +val epoints_to : tau -> Cil.varinfo list +val string_of_lvalue : lvalue -> string +val may_alias : tau -> tau -> bool + +val absloc_points_to : lvalue -> absloc list +val absloc_epoints_to : tau -> absloc list +val absloc_of_lvalue : lvalue -> absloc +val absloc_eq : (absloc * absloc) -> bool +val d_absloc : unit -> absloc -> Pretty.doc diff --git a/cil/src/ext/pta/ptranal.ml b/cil/src/ext/pta/ptranal.ml new file mode 100644 index 00000000..c91bda81 --- /dev/null +++ b/cil/src/ext/pta/ptranal.ml @@ -0,0 +1,597 @@ +(* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *) + +(* + * + * 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. + * + *) + +exception Bad_return +exception Bad_function + + +open Cil + +module H = Hashtbl + +module A = Olf +exception UnknownLocation = A.UnknownLocation + +type access = A.lvalue * bool + +type access_map = (lval, access) H.t + +(** a mapping from varinfo's back to fundecs *) +module VarInfoKey = +struct + type t = varinfo + let compare v1 v2 = v1.vid - v2.vid +end + +module F = Map.Make (VarInfoKey) + + +(***********************************************************************) +(* *) +(* Global Variables *) +(* *) +(***********************************************************************) + +let model_strings = ref false +let print_constraints = A.print_constraints +let debug_constraints = A.debug_constraints +let debug_aliases = A.debug_aliases +let smart_aliases = A.smart_aliases +let debug = A.debug +let analyze_mono = A.analyze_mono +let no_flow = A.no_flow +let no_sub = A.no_sub +let fun_ptrs_as_funs = ref false +let show_progress = ref false +let debug_may_aliases = ref false + +let found_undefined = ref false + +let conservative_undefineds = ref false + +let current_fundec : fundec option ref = ref None + +let fun_access_map : (fundec, access_map) H.t = H.create 64 + +(* A mapping from varinfos to fundecs *) +let fun_varinfo_map = ref F.empty + +let current_ret : A.tau option ref = ref None + +let lvalue_hash : (varinfo,A.lvalue) H.t = H.create 64 + +let expressions : (exp,A.tau) H.t = H.create 64 + +let lvalues : (lval,A.lvalue) H.t = H.create 64 + +let fresh_index : (unit -> int) = + let count = ref 0 in + fun () -> + incr count; + !count + +let alloc_names = [ + "malloc"; + "calloc"; + "realloc"; + "xmalloc"; + "__builtin_alloca"; + "alloca"; + "kmalloc" +] + +let all_globals : varinfo list ref = ref [] +let all_functions : fundec list ref = ref [] + + +(***********************************************************************) +(* *) +(* Utility Functions *) +(* *) +(***********************************************************************) + +let is_undefined_fun = function + Lval (lh, o) -> + if isFunctionType (typeOfLval (lh, o)) then + match lh with + Var v -> v.vstorage = Extern + | _ -> false + else false + | _ -> false + +let is_alloc_fun = function + Lval (lh, o) -> + if isFunctionType (typeOfLval (lh, o)) then + match lh with + Var v -> List.mem v.vname alloc_names + | _ -> false + else false + | _ -> false + +let next_alloc = function + Lval (Var v, o) -> + let name = Printf.sprintf "%s@%d" v.vname (fresh_index ()) + in + A.address (A.make_lvalue false name (Some v)) (* check *) + | _ -> raise Bad_return + +let is_effect_free_fun = function + Lval (lh, o) when isFunctionType (typeOfLval (lh, o)) -> + begin + match lh with + Var v -> + begin + try ("CHECK_" = String.sub v.vname 0 6) + with Invalid_argument _ -> false + end + | _ -> false + end + | _ -> false + + +(***********************************************************************) +(* *) +(* AST Traversal Functions *) +(* *) +(***********************************************************************) + +(* should do nothing, might need to worry about Index case *) +(* let analyzeOffset (o : offset ) : A.tau = A.bottom () *) + +let analyze_var_decl (v : varinfo ) : A.lvalue = + try H.find lvalue_hash v + with Not_found -> + let lv = A.make_lvalue false v.vname (Some v) + in + H.add lvalue_hash v lv; + lv + +let isFunPtrType (t : typ) : bool = + match t with + TPtr (t, _) -> isFunctionType t + | _ -> false + +let rec analyze_lval (lv : lval ) : A.lvalue = + let find_access (l : A.lvalue) (is_var : bool) : A.lvalue = + match !current_fundec with + None -> l + | Some f -> + let accesses = H.find fun_access_map f in + if H.mem accesses lv then l + else + begin + H.add accesses lv (l, is_var); + l + end in + let result = + match lv with + Var v, _ -> (* instantiate every syntactic occurrence of a function *) + let alv = + if isFunctionType (typeOfLval lv) then + A.instantiate (analyze_var_decl v) (fresh_index ()) + else analyze_var_decl v + in + find_access alv true + | Mem e, _ -> + (* assert (not (isFunctionType(typeOf(e))) ); *) + let alv = + if !fun_ptrs_as_funs && isFunPtrType (typeOf e) then + analyze_expr_as_lval e + else A.deref (analyze_expr e) + in + find_access alv false + in + H.replace lvalues lv result; + result +and analyze_expr_as_lval (e : exp) : A.lvalue = + match e with + Lval l -> analyze_lval l + | _ -> assert false (* todo -- other kinds of expressions? *) +and analyze_expr (e : exp ) : A.tau = + let result = + match e with + Const (CStr s) -> + if !model_strings then + A.address (A.make_lvalue + false + s + (Some (makeVarinfo false s charConstPtrType))) + else A.bottom () + | Const c -> A.bottom () + | Lval l -> A.rvalue (analyze_lval l) + | SizeOf _ -> A.bottom () + | SizeOfStr _ -> A.bottom () + | AlignOf _ -> A.bottom () + | UnOp (op, e, t) -> analyze_expr e + | BinOp (op, e, e', t) -> A.join (analyze_expr e) (analyze_expr e') + | CastE (t, e) -> analyze_expr e + | AddrOf l -> + if !fun_ptrs_as_funs && isFunctionType (typeOfLval l) then + A.rvalue (analyze_lval l) + else A.address (analyze_lval l) + | StartOf l -> A.address (analyze_lval l) + | AlignOfE _ -> A.bottom () + | SizeOfE _ -> A.bottom () + in + H.add expressions e result; + result + + +(* check *) +let rec analyze_init (i : init ) : A.tau = + match i with + SingleInit e -> analyze_expr e + | CompoundInit (t, oi) -> + A.join_inits (List.map (function (_, i) -> analyze_init i) oi) + +let analyze_instr (i : instr ) : unit = + match i with + Set (lval, rhs, l) -> + A.assign (analyze_lval lval) (analyze_expr rhs) + | Call (res, fexpr, actuals, l) -> + if not (isFunctionType (typeOf fexpr)) then + () (* todo : is this a varargs? *) + else if is_alloc_fun fexpr then + begin + if !debug then print_string "Found allocation function...\n"; + match res with + Some r -> A.assign (analyze_lval r) (next_alloc fexpr) + | None -> () + end + else if is_effect_free_fun fexpr then + List.iter (fun e -> ignore (analyze_expr e)) actuals + else (* todo : check to see if the thing is an undefined function *) + let fnres, site = + if is_undefined_fun fexpr & !conservative_undefineds then + A.apply_undefined (List.map analyze_expr actuals) + else + A.apply (analyze_expr fexpr) (List.map analyze_expr actuals) + in + begin + match res with + Some r -> + begin + A.assign_ret site (analyze_lval r) fnres; + found_undefined := true; + end + | None -> () + end + | Asm _ -> () + +let rec analyze_stmt (s : stmt ) : unit = + match s.skind with + Instr il -> List.iter analyze_instr il + | Return (eo, l) -> + begin + match eo with + Some e -> + begin + match !current_ret with + Some ret -> A.return ret (analyze_expr e) + | None -> raise Bad_return + end + | None -> () + end + | Goto (s', l) -> () (* analyze_stmt(!s') *) + | If (e, b, b', l) -> + (* ignore the expression e; expressions can't be side-effecting *) + analyze_block b; + analyze_block b' + | Switch (e, b, sl, l) -> + analyze_block b; + List.iter analyze_stmt sl +(* + | Loop (b, l, _, _) -> analyze_block b +*) + | While (_, b, _) -> analyze_block b + | DoWhile (_, b, _) -> analyze_block b + | For (bInit, _, bIter, b, _) -> + analyze_block bInit; + analyze_block bIter; + analyze_block b + | Block b -> analyze_block b + | TryFinally (b, h, _) -> + analyze_block b; + analyze_block h + | TryExcept (b, (il, _), h, _) -> + analyze_block b; + List.iter analyze_instr il; + analyze_block h + | Break l -> () + | Continue l -> () + + +and analyze_block (b : block ) : unit = + List.iter analyze_stmt b.bstmts + +let analyze_function (f : fundec ) : unit = + let oldlv = analyze_var_decl f.svar in + let ret = A.make_fresh (f.svar.vname ^ "_ret") in + let formals = List.map analyze_var_decl f.sformals in + let newf = A.make_function f.svar.vname formals ret in + if !show_progress then + Printf.printf "Analyzing function %s\n" f.svar.vname; + fun_varinfo_map := F.add f.svar f (!fun_varinfo_map); + current_fundec := Some f; + H.add fun_access_map f (H.create 8); + A.assign oldlv newf; + current_ret := Some ret; + analyze_block f.sbody + +let analyze_global (g : global ) : unit = + match g with + GVarDecl (v, l) -> () (* ignore (analyze_var_decl(v)) -- no need *) + | GVar (v, init, l) -> + all_globals := v :: !all_globals; + begin + match init.init with + Some i -> A.assign (analyze_var_decl v) (analyze_init i) + | None -> ignore (analyze_var_decl v) + end + | GFun (f, l) -> + all_functions := f :: !all_functions; + analyze_function f + | _ -> () + +let analyze_file (f : file) : unit = + iterGlobals f analyze_global + + +(***********************************************************************) +(* *) +(* High-level Query Interface *) +(* *) +(***********************************************************************) + +(* Same as analyze_expr, but no constraints. *) +let rec traverse_expr (e : exp) : A.tau = + H.find expressions e + +and traverse_expr_as_lval (e : exp) : A.lvalue = + match e with + | Lval l -> traverse_lval l + | _ -> assert false (* todo -- other kinds of expressions? *) + +and traverse_lval (lv : lval ) : A.lvalue = + H.find lvalues lv + +let may_alias (e1 : exp) (e2 : exp) : bool = + let tau1,tau2 = traverse_expr e1, traverse_expr e2 in + let result = A.may_alias tau1 tau2 in + if !debug_may_aliases then + begin + let doc1 = d_exp () e1 in + let doc2 = d_exp () e2 in + let s1 = Pretty.sprint ~width:30 doc1 in + let s2 = Pretty.sprint ~width:30 doc2 in + Printf.printf + "%s and %s may alias? %s\n" + s1 + s2 + (if result then "yes" else "no") + end; + result + +let resolve_lval (lv : lval) : varinfo list = + A.points_to (traverse_lval lv) + +let resolve_exp (e : exp) : varinfo list = + A.epoints_to (traverse_expr e) + +let resolve_funptr (e : exp) : fundec list = + let varinfos = A.epoints_to (traverse_expr e) in + List.fold_left + (fun fdecs -> fun vinf -> + try F.find vinf !fun_varinfo_map :: fdecs + with Not_found -> fdecs) + [] + varinfos + +let count_hash_elts h = + let result = ref 0 in + H.iter (fun _ -> fun _ -> incr result) lvalue_hash; + !result + +let compute_may_aliases (b : bool) : unit = + let rec compute_may_aliases_aux (exps : exp list) = + match exps with + [] -> () + | h :: t -> + ignore (List.map (may_alias h) t); + compute_may_aliases_aux t + and exprs : exp list ref = ref [] in + H.iter (fun e -> fun _ -> exprs := e :: !exprs) expressions; + compute_may_aliases_aux !exprs + + +let compute_results (show_sets : bool) : unit = + let total_pointed_to = ref 0 + and total_lvalues = H.length lvalue_hash + and counted_lvalues = ref 0 + and lval_elts : (string * (string list)) list ref = ref [] in + let print_result (name, set) = + let rec print_set s = + match s with + [] -> () + | h :: [] -> print_string h + | h :: t -> + print_string (h ^ ", "); + print_set t + and ptsize = List.length set in + total_pointed_to := !total_pointed_to + ptsize; + if ptsize > 0 then + begin + print_string (name ^ "(" ^ (string_of_int ptsize) ^ ") -> "); + print_set set; + print_newline () + end + in + (* Make the most pessimistic assumptions about globals if an + undefined function is present. Such a function can write to every + global variable *) + let hose_globals () : unit = + List.iter + (fun vd -> A.assign_undefined (analyze_var_decl vd)) + !all_globals + in + let show_progress_fn (counted : int ref) (total : int) : unit = + incr counted; + if !show_progress then + Printf.printf "Computed flow for %d of %d sets\n" !counted total + in + if !conservative_undefineds && !found_undefined then hose_globals (); + A.finished_constraints (); + if show_sets then + begin + print_endline "Computing points-to sets..."; + Hashtbl.iter + (fun vinf -> fun lv -> + show_progress_fn counted_lvalues total_lvalues; + try lval_elts := (vinf.vname, A.points_to_names lv) :: !lval_elts + with A.UnknownLocation -> ()) + lvalue_hash; + List.iter print_result !lval_elts; + Printf.printf + "Total number of things pointed to: %d\n" + !total_pointed_to + end; + if !debug_may_aliases then + begin + Printf.printf "Printing may alias relationships\n"; + compute_may_aliases true + end + +let print_types () : unit = + print_string "Printing inferred types of lvalues...\n"; + Hashtbl.iter + (fun vi -> fun lv -> + Printf.printf "%s : %s\n" vi.vname (A.string_of_lvalue lv)) + lvalue_hash + + + +(** Alias queries. For each function, gather sets of locals, formals, and + globals. Do n^2 work for each of these functions, reporting whether or not + each pair of values is aliased. Aliasing is determined by taking points-to + set intersections. +*) +let compute_aliases = compute_may_aliases + + +(***********************************************************************) +(* *) +(* Abstract Location Interface *) +(* *) +(***********************************************************************) + +type absloc = A.absloc + +let rec lvalue_of_varinfo (vi : varinfo) : A.lvalue = + H.find lvalue_hash vi + +let lvalue_of_lval = traverse_lval +let tau_of_expr = traverse_expr + +(** return an abstract location for a varinfo, resp. lval *) +let absloc_of_varinfo vi = + A.absloc_of_lvalue (lvalue_of_varinfo vi) + +let absloc_of_lval lv = + A.absloc_of_lvalue (lvalue_of_lval lv) + +let absloc_e_points_to e = + A.absloc_epoints_to (tau_of_expr e) + +let absloc_lval_aliases lv = + A.absloc_points_to (lvalue_of_lval lv) + +(* all abslocs that e transitively points to *) +let absloc_e_transitive_points_to (e : Cil.exp) : absloc list = + let rec lv_trans_ptsto (worklist : varinfo list) (acc : varinfo list) : absloc list = + match worklist with + [] -> List.map absloc_of_varinfo acc + | vi :: wklst'' -> + if List.mem vi acc then lv_trans_ptsto wklst'' acc + else + lv_trans_ptsto + (List.rev_append + (A.points_to (lvalue_of_varinfo vi)) + wklst'') + (vi :: acc) + in + lv_trans_ptsto (A.epoints_to (tau_of_expr e)) [] + +let absloc_eq a b = A.absloc_eq (a, b) + +let d_absloc: unit -> absloc -> Pretty.doc = A.d_absloc + + +let ptrAnalysis = ref false +let ptrResults = ref false +let ptrTypes = ref false + + + +(** Turn this into a CIL feature *) +let feature : featureDescr = { + fd_name = "ptranal"; + fd_enabled = ptrAnalysis; + fd_description = "alias analysis"; + fd_extraopt = [ + ("--ptr_may_aliases", + Arg.Unit (fun _ -> debug_may_aliases := true), + "Print out results of may alias queries"); + ("--ptr_unify", Arg.Unit (fun _ -> no_sub := true), + "Make the alias analysis unification-based"); + ("--ptr_model_strings", Arg.Unit (fun _ -> model_strings := true), + "Make the alias analysis model string constants"); + ("--ptr_conservative", + Arg.Unit (fun _ -> conservative_undefineds := true), + "Treat undefineds conservatively in alias analysis"); + ("--ptr_results", Arg.Unit (fun _ -> ptrResults := true), + "print the results of the alias analysis"); + ("--ptr_mono", Arg.Unit (fun _ -> analyze_mono := true), + "run alias analysis monomorphically"); + ("--ptr_types",Arg.Unit (fun _ -> ptrTypes := true), + "print inferred points-to analysis types") + ]; + fd_doit = (function (f: file) -> + analyze_file f; + compute_results !ptrResults; + if !ptrTypes then print_types ()); + fd_post_check = false (* No changes *) +} diff --git a/cil/src/ext/pta/ptranal.mli b/cil/src/ext/pta/ptranal.mli new file mode 100644 index 00000000..36eb7a54 --- /dev/null +++ b/cil/src/ext/pta/ptranal.mli @@ -0,0 +1,156 @@ +(* + * + * 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. + * + *) + +(***********************************************************************) +(* *) +(* Flags *) +(* *) +(***********************************************************************) + +(** Print extra debugging info *) +val debug : bool ref + +(** Debug constraints (print all constraints) *) +val debug_constraints : bool ref + +(** Debug smart alias queries *) +val debug_aliases : bool ref + +(** Debug may alias queries *) +val debug_may_aliases : bool ref + +val smart_aliases : bool ref + +(** Print out the top level constraints *) +val print_constraints : bool ref + +(** Make the analysis monomorphic *) +val analyze_mono : bool ref + +(** Disable subtyping *) +val no_sub : bool ref + +(** Make the flow step a no-op *) +val no_flow : bool ref + +(** Show the progress of the flow step *) +val show_progress : bool ref + +(** Treat undefined functions conservatively *) +val conservative_undefineds : bool ref + +(***********************************************************************) +(* *) +(* Building the Points-to Graph *) +(* *) +(***********************************************************************) + +(** Analyze a file *) +val analyze_file : Cil.file -> unit + +(** Print the type of each lvalue in the program *) +val print_types : unit -> unit + +(***********************************************************************) +(* *) +(* High-level Query Interface *) +(* *) +(***********************************************************************) + +(** If undefined functions are analyzed conservatively, any of the + high-level queries may raise this exception *) +exception UnknownLocation + +val may_alias : Cil.exp -> Cil.exp -> bool + +val resolve_lval : Cil.lval -> (Cil.varinfo list) + +val resolve_exp : Cil.exp -> (Cil.varinfo list) + +val resolve_funptr : Cil.exp -> (Cil.fundec list) + +(***********************************************************************) +(* *) +(* Low-level Query Interface *) +(* *) +(***********************************************************************) + +(** type for abstract locations *) +type absloc + +(** Give an abstract location for a varinfo *) +val absloc_of_varinfo : Cil.varinfo -> absloc + +(** Give an abstract location for an Cil lvalue *) +val absloc_of_lval : Cil.lval -> absloc + +(** may the two abstract locations be aliased? *) +val absloc_eq : absloc -> absloc -> bool + +val absloc_e_points_to : Cil.exp -> absloc list +val absloc_e_transitive_points_to : Cil.exp -> absloc list + +val absloc_lval_aliases : Cil.lval -> absloc list + +(** Print a string representing an absloc, for debugging. *) +val d_absloc : unit -> absloc -> Pretty.doc + + +(***********************************************************************) +(* *) +(* Printing results *) +(* *) +(***********************************************************************) + +(** Compute points to sets for variables. If true is passed, print the sets. *) +val compute_results : bool -> unit + +(* + +Deprecated these. -- jk + +(** Compute alias relationships. If true is passed, print all alias pairs. *) + val compute_aliases : bool -> unit + +(** Compute alias frequncy *) +val compute_alias_frequency : unit -> unit + + +*) + +val compute_aliases : bool -> unit + + +val feature: Cil.featureDescr diff --git a/cil/src/ext/pta/setp.ml b/cil/src/ext/pta/setp.ml new file mode 100644 index 00000000..a39b9722 --- /dev/null +++ b/cil/src/ext/pta/setp.ml @@ -0,0 +1,342 @@ +(* + * + * 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. + * + *) +(***********************************************************************) +(* *) +(* Objective Caml *) +(* *) +(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *) +(* *) +(* Copyright 1996 Institut National de Recherche en Informatique et *) +(* en Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU Library General Public License, with *) +(* the special exception on linking described in file ../LICENSE. *) +(* *) +(***********************************************************************) + +(* $Id: setp.ml,v 1.3 2003-02-19 19:26:31 jkodumal Exp $ *) + +(* Sets over ordered types *) + +module type PolyOrderedType = + sig + type 'a t + val compare: 'a t -> 'a t -> int + end + +module type S = + sig + type 'a elt + type 'a t + val empty: 'a t + val is_empty: 'a t -> bool + val mem: 'a elt -> 'a t -> bool + val add: 'a elt -> 'a t -> 'a t + val singleton: 'a elt -> 'a t + val remove: 'a elt -> 'a t -> 'a t + val union: 'a t -> 'a t -> 'a t + val inter: 'a t -> 'a t -> 'a t + val diff: 'a t -> 'a t -> 'a t + val compare: 'a t -> 'a t -> int + val equal: 'a t -> 'a t -> bool + val subset: 'a t -> 'a t -> bool + val iter: ('a elt -> unit) -> 'a t -> unit + val fold: ('a elt -> 'b -> 'b) -> 'a t -> 'b -> 'b + val for_all: ('a elt -> bool) -> 'a t -> bool + val exists: ('a elt -> bool) -> 'a t -> bool + val filter: ('a elt -> bool) -> 'a t -> 'a t + val partition: ('a elt -> bool) -> 'a t -> 'a t * 'a t + val cardinal: 'a t -> int + val elements: 'a t -> 'a elt list + val min_elt: 'a t -> 'a elt + val max_elt: 'a t -> 'a elt + val choose: 'a t -> 'a elt + end + +module Make(Ord: PolyOrderedType) = + struct + type 'a elt = 'a Ord.t + type 'a t = Empty | Node of 'a t * 'a elt * 'a t * int + + (* Sets are represented by balanced binary trees (the heights of the + children differ by at most 2 *) + + let height = function + Empty -> 0 + | Node(_, _, _, h) -> h + + (* Creates a new node with left son l, value x and right son r. + l and r must be balanced and | height l - height r | <= 2. + Inline expansion of height for better speed. *) + + let create l x r = + let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in + let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in + Node(l, x, r, (if hl >= hr then hl + 1 else hr + 1)) + + (* Same as create, but performs one step of rebalancing if necessary. + Assumes l and r balanced. + Inline expansion of create for better speed in the most frequent case + where no rebalancing is required. *) + + let bal l x r = + let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in + let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in + if hl > hr + 2 then begin + match l with + Empty -> invalid_arg "Set.bal" + | Node(ll, lv, lr, _) -> + if height ll >= height lr then + create ll lv (create lr x r) + else begin + match lr with + Empty -> invalid_arg "Set.bal" + | Node(lrl, lrv, lrr, _)-> + create (create ll lv lrl) lrv (create lrr x r) + end + end else if hr > hl + 2 then begin + match r with + Empty -> invalid_arg "Set.bal" + | Node(rl, rv, rr, _) -> + if height rr >= height rl then + create (create l x rl) rv rr + else begin + match rl with + Empty -> invalid_arg "Set.bal" + | Node(rll, rlv, rlr, _) -> + create (create l x rll) rlv (create rlr rv rr) + end + end else + Node(l, x, r, (if hl >= hr then hl + 1 else hr + 1)) + + (* Same as bal, but repeat rebalancing until the final result + is balanced. *) + + let rec join l x r = + match bal l x r with + Empty -> invalid_arg "Set.join" + | Node(l', x', r', _) as t' -> + let d = height l' - height r' in + if d < -2 || d > 2 then join l' x' r' else t' + + (* Merge two trees l and r into one. + All elements of l must precede the elements of r. + Assumes | height l - height r | <= 2. *) + + let rec merge t1 t2 = + match (t1, t2) with + (Empty, t) -> t + | (t, Empty) -> t + | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) -> + bal l1 v1 (bal (merge r1 l2) v2 r2) + + (* Same as merge, but does not assume anything about l and r. *) + + let rec concat t1 t2 = + match (t1, t2) with + (Empty, t) -> t + | (t, Empty) -> t + | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) -> + join l1 v1 (join (concat r1 l2) v2 r2) + + (* Splitting *) + + let rec split x = function + Empty -> + (Empty, None, Empty) + | Node(l, v, r, _) -> + let c = Ord.compare x v in + if c = 0 then (l, Some v, r) + else if c < 0 then + let (ll, vl, rl) = split x l in (ll, vl, join rl v r) + else + let (lr, vr, rr) = split x r in (join l v lr, vr, rr) + + (* Implementation of the set operations *) + + let empty = Empty + + let is_empty = function Empty -> true | _ -> false + + let rec mem x = function + Empty -> false + | Node(l, v, r, _) -> + let c = Ord.compare x v in + c = 0 || mem x (if c < 0 then l else r) + + let rec add x = function + Empty -> Node(Empty, x, Empty, 1) + | Node(l, v, r, _) as t -> + let c = Ord.compare x v in + if c = 0 then t else + if c < 0 then bal (add x l) v r else bal l v (add x r) + + let singleton x = Node(Empty, x, Empty, 1) + + let rec remove x = function + Empty -> Empty + | Node(l, v, r, _) -> + let c = Ord.compare x v in + if c = 0 then merge l r else + if c < 0 then bal (remove x l) v r else bal l v (remove x r) + + let rec union s1 s2 = + match (s1, s2) with + (Empty, t2) -> t2 + | (t1, Empty) -> t1 + | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) -> + if h1 >= h2 then + if h2 = 1 then add v2 s1 else begin + let (l2, _, r2) = split v1 s2 in + join (union l1 l2) v1 (union r1 r2) + end + else + if h1 = 1 then add v1 s2 else begin + let (l1, _, r1) = split v2 s1 in + join (union l1 l2) v2 (union r1 r2) + end + + let rec inter s1 s2 = + match (s1, s2) with + (Empty, t2) -> Empty + | (t1, Empty) -> Empty + | (Node(l1, v1, r1, _), t2) -> + match split v1 t2 with + (l2, None, r2) -> + concat (inter l1 l2) (inter r1 r2) + | (l2, Some _, r2) -> + join (inter l1 l2) v1 (inter r1 r2) + + let rec diff s1 s2 = + match (s1, s2) with + (Empty, t2) -> Empty + | (t1, Empty) -> t1 + | (Node(l1, v1, r1, _), t2) -> + match split v1 t2 with + (l2, None, r2) -> + join (diff l1 l2) v1 (diff r1 r2) + | (l2, Some _, r2) -> + concat (diff l1 l2) (diff r1 r2) + + let rec compare_aux l1 l2 = + match (l1, l2) with + ([], []) -> 0 + | ([], _) -> -1 + | (_, []) -> 1 + | (Empty :: t1, Empty :: t2) -> + compare_aux t1 t2 + | (Node(Empty, v1, r1, _) :: t1, Node(Empty, v2, r2, _) :: t2) -> + let c = Ord.compare v1 v2 in + if c <> 0 then c else compare_aux (r1::t1) (r2::t2) + | (Node(l1, v1, r1, _) :: t1, t2) -> + compare_aux (l1 :: Node(Empty, v1, r1, 0) :: t1) t2 + | (t1, Node(l2, v2, r2, _) :: t2) -> + compare_aux t1 (l2 :: Node(Empty, v2, r2, 0) :: t2) + + let compare s1 s2 = + compare_aux [s1] [s2] + + let equal s1 s2 = + compare s1 s2 = 0 + + let rec subset s1 s2 = + match (s1, s2) with + Empty, _ -> + true + | _, Empty -> + false + | Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) -> + let c = Ord.compare v1 v2 in + if c = 0 then + subset l1 l2 && subset r1 r2 + else if c < 0 then + subset (Node (l1, v1, Empty, 0)) l2 && subset r1 t2 + else + subset (Node (Empty, v1, r1, 0)) r2 && subset l1 t2 + + let rec iter f = function + Empty -> () + | Node(l, v, r, _) -> iter f l; f v; iter f r + + let rec fold f s accu = + match s with + Empty -> accu + | Node(l, v, r, _) -> fold f l (f v (fold f r accu)) + + let rec for_all p = function + Empty -> true + | Node(l, v, r, _) -> p v && for_all p l && for_all p r + + let rec exists p = function + Empty -> false + | Node(l, v, r, _) -> p v || exists p l || exists p r + + let filter p s = + let rec filt accu = function + | Empty -> accu + | Node(l, v, r, _) -> + filt (filt (if p v then add v accu else accu) l) r in + filt Empty s + + let partition p s = + let rec part (t, f as accu) = function + | Empty -> accu + | Node(l, v, r, _) -> + part (part (if p v then (add v t, f) else (t, add v f)) l) r in + part (Empty, Empty) s + + let rec cardinal = function + Empty -> 0 + | Node(l, v, r, _) -> cardinal l + 1 + cardinal r + + let rec elements_aux accu = function + Empty -> accu + | Node(l, v, r, _) -> elements_aux (v :: elements_aux accu r) l + + let elements s = + elements_aux [] s + + let rec min_elt = function + Empty -> raise Not_found + | Node(Empty, v, r, _) -> v + | Node(l, v, r, _) -> min_elt l + + let rec max_elt = function + Empty -> raise Not_found + | Node(l, v, Empty, _) -> v + | Node(l, v, r, _) -> max_elt r + + let choose = min_elt + + end diff --git a/cil/src/ext/pta/setp.mli b/cil/src/ext/pta/setp.mli new file mode 100644 index 00000000..a3b30313 --- /dev/null +++ b/cil/src/ext/pta/setp.mli @@ -0,0 +1,180 @@ +(* + * + * 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. + * + *) +(***********************************************************************) +(* *) +(* Objective Caml *) +(* *) +(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *) +(* *) +(* Copyright 1996 Institut National de Recherche en Informatique et *) +(* en Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU Library General Public License, with *) +(* the special exception on linking described in file ../LICENSE. *) +(* *) +(***********************************************************************) + +(* $Id: setp.mli,v 1.3 2003-02-19 19:26:31 jkodumal Exp $ *) + +(** Sets over ordered types. + + This module implements the set data structure, given a total ordering + function over the set elements. All operations over sets + are purely applicative (no side-effects). + The implementation uses balanced binary trees, and is therefore + reasonably efficient: insertion and membership take time + logarithmic in the size of the set, for instance. +*) + +module type PolyOrderedType = + sig + type 'a t + (** The type of the set elements. *) + val compare : 'a t -> 'a t -> int + (** A total ordering function over the set elements. + This is a two-argument function [f] such that + [f e1 e2] is zero if the elements [e1] and [e2] are equal, + [f e1 e2] is strictly negative if [e1] is smaller than [e2], + and [f e1 e2] is strictly positive if [e1] is greater than [e2]. + Example: a suitable ordering function is + the generic structural comparison function {!Pervasives.compare}. *) + end +(** Input signature of the functor {!Set.Make}. *) + +module type S = + sig + type 'a elt + (** The type of the set elements. *) + + type 'a t + (** The type of sets. *) + + val empty: 'a t + (** The empty set. *) + + val is_empty: 'a t -> bool + (** Test whether a set is empty or not. *) + + val mem: 'a elt -> 'a t -> bool + (** [mem x s] tests whether [x] belongs to the set [s]. *) + + val add: 'a elt -> 'a t -> 'a t + (** [add x s] returns a set containing all elements of [s], + plus [x]. If [x] was already in [s], [s] is returned unchanged. *) + + val singleton: 'a elt -> 'a t + (** [singleton x] returns the one-element set containing only [x]. *) + + val remove: 'a elt -> 'a t -> 'a t + (** [remove x s] returns a set containing all elements of [s], + except [x]. If [x] was not in [s], [s] is returned unchanged. *) + + val union: 'a t -> 'a t -> 'a t + (** Set union. *) + + val inter: 'a t -> 'a t -> 'a t + (** Set interseection. *) + + (** Set difference. *) + val diff: 'a t -> 'a t -> 'a t + + val compare: 'a t -> 'a t -> int + (** Total ordering between sets. Can be used as the ordering function + for doing sets of sets. *) + + val equal: 'a t -> 'a t -> bool + (** [equal s1 s2] tests whether the sets [s1] and [s2] are + equal, that is, contain equal elements. *) + + val subset: 'a t -> 'a t -> bool + (** [subset s1 s2] tests whether the set [s1] is a subset of + the set [s2]. *) + + val iter: ('a elt -> unit) -> 'a t -> unit + (** [iter f s] applies [f] in turn to all elements of [s]. + The order in which the elements of [s] are presented to [f] + is unspecified. *) + + val fold: ('a elt -> 'b -> 'b) -> 'a t -> 'b -> 'b + (** [fold f s a] computes [(f xN ... (f x2 (f x1 a))...)], + where [x1 ... xN] are the elements of [s]. + The order in which elements of [s] are presented to [f] is + unspecified. *) + + val for_all: ('a elt -> bool) -> 'a t -> bool + (** [for_all p s] checks if all elements of the set + satisfy the predicate [p]. *) + + val exists: ('a elt -> bool) -> 'a t -> bool + (** [exists p s] checks if at least one element of + the set satisfies the predicate [p]. *) + + val filter: ('a elt -> bool) -> 'a t -> 'a t + (** [filter p s] returns the set of all elements in [s] + that satisfy predicate [p]. *) + + val partition: ('a elt -> bool) -> 'a t -> 'a t * 'a t + (** [partition p s] returns a pair of sets [(s1, s2)], where + [s1] is the set of all the elements of [s] that satisfy the + predicate [p], and [s2] is the set of all the elements of + [s] that do not satisfy [p]. *) + + val cardinal: 'a t -> int + (** Return the number of elements of a set. *) + + val elements: 'a t -> 'a elt list + (** Return the list of all elements of the given set. + The returned list is sorted in increasing order with respect + to the ordering [Ord.compare], where [Ord] is the argument + given to {!Set.Make}. *) + + val min_elt: 'a t -> 'a elt + (** Return the smallest element of the given set + (with respect to the [Ord.compare] ordering), or raise + [Not_found] if the set is empty. *) + + val max_elt: 'a t -> 'a elt + (** Same as {!Set.S.min_elt}, but returns the largest element of the + given set. *) + + val choose: 'a t -> 'a elt + (** Return one element of the given set, or raise [Not_found] if + the set is empty. Which element is chosen is unspecified, + but equal elements will be chosen for equal sets. *) + end +(** Output signature of the functor {!Set.Make}. *) + +module Make (Ord : PolyOrderedType) : S with type 'a elt = 'a Ord.t +(** Functor building an implementation of the set structure + given a totally ordered type. *) diff --git a/cil/src/ext/pta/steensgaard.ml b/cil/src/ext/pta/steensgaard.ml new file mode 100644 index 00000000..63686934 --- /dev/null +++ b/cil/src/ext/pta/steensgaard.ml @@ -0,0 +1,1417 @@ +(* + * + * 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 +*) diff --git a/cil/src/ext/pta/steensgaard.mli b/cil/src/ext/pta/steensgaard.mli new file mode 100644 index 00000000..f009e7e0 --- /dev/null +++ b/cil/src/ext/pta/steensgaard.mli @@ -0,0 +1,71 @@ +(* + * + * 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 lvalue +type tau +val debug : bool ref +val debug_constraints : bool ref +val print_constraints : bool ref +val no_flow : bool ref +val no_sub : bool ref +val analyze_mono : bool ref +val solve_online : bool ref +val solve_constraints : unit -> unit +val rvalue : lvalue -> tau +val deref : tau -> lvalue +val join : tau -> tau -> tau +val join_inits : tau list -> tau +val address : lvalue -> tau +val instantiate : lvalue -> int -> lvalue +val assign : lvalue -> tau -> unit +val apply : tau -> tau list -> tau +val make_function : string -> lvalue list -> tau -> tau +val make_lvalue : bool -> string -> lvalue +val bottom : unit -> tau +val return : tau -> tau -> unit +val make_fresh : string -> tau +val points_to : lvalue -> string list +val string_of_lvalue : lvalue -> string +val global_lvalue : lvalue -> bool +val alias_query : bool -> lvalue list -> int * int diff --git a/cil/src/ext/pta/uref.ml b/cil/src/ext/pta/uref.ml new file mode 100644 index 00000000..53f36400 --- /dev/null +++ b/cil/src/ext/pta/uref.ml @@ -0,0 +1,94 @@ +(* + * + * 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. + * + *) +exception Bad_find + +type 'a urefC = + Ecr of 'a * int + | Link of 'a uref +and 'a uref = 'a urefC ref + +let rec find p = + match !p with + | Ecr _ -> p + | Link p' -> + let p'' = find p' + in p := Link p''; p'' + +let uref x = ref (Ecr(x,0)) + +let equal (p,p') = (find p == find p') + +let deref p = + match ! (find p) with + | Ecr (x,_) -> x + | _ -> raise Bad_find + +let update (p,x) = + let p' = find p + in + match !p' with + | Ecr (_,rank) -> p' := Ecr(x,rank) + | _ -> raise Bad_find + +let unify f (p,q) = + let p',q' = find p, find q in + match (!p',!q') with + | (Ecr(px,pr),Ecr(qx,qr)) -> + let x = f(px,qx) in + if (p' == q') then + p' := Ecr(x,pr) + else if pr == qr then + (q' := Ecr(x,qr+1); p' := Link q') + else if pr < qr then + (q' := Ecr(x,qr); p' := Link q') + else (* pr > qr *) + (p' := Ecr(x,pr); q' := Link p') + | _ -> raise Bad_find + +let union (p,q) = + let p',q' = find p, find q in + match (!p',!q') with + | (Ecr(px,pr),Ecr(qx,qr)) -> + if (p' == q') then + () + else if pr == qr then + (q' := Ecr(qx, qr+1); p' := Link q') + else if pr < qr then + p' := Link q' + else (* pr > qr *) + q' := Link p' + | _ -> raise Bad_find + + diff --git a/cil/src/ext/pta/uref.mli b/cil/src/ext/pta/uref.mli new file mode 100644 index 00000000..1dee5036 --- /dev/null +++ b/cil/src/ext/pta/uref.mli @@ -0,0 +1,65 @@ +(* + * + * 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. + * + *) +type 'a uref + +(** Union-find with union by rank and path compression + + This is an implementation of Tarjan's union-find data structure using + generics. The interface is analagous to standard references, with the + addition of a union operation which makes two references indistinguishable. + +*) + +val uref: 'a -> 'a uref + (** Create a new uref *) + +val equal: 'a uref * 'a uref -> bool + (** Test whether two urefs share the same equivalence class *) + +val deref: 'a uref -> 'a + (** Extract the contents of this reference *) + +val update: 'a uref * 'a -> unit + (** Update the value stored in this reference *) + +val unify: ('a * 'a -> 'a) -> 'a uref * 'a uref -> unit + (** [unify f (p,q)] unifies references [p] and [q], making them + indistinguishable. The contents of the reference are the result of + [f] *) + +val union: 'a uref * 'a uref -> unit + (** [unify (p,q)] unifies references [p] and [q], making them + indistinguishable. The contents of the reference are the contents of + one of the first or second arguments (unspecified) *) |