(*
 *
 * 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
*)