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