(** 
    Functions to optimize vine expressions.
    
    Basically, constant_fold will only perform constant folding, whereas
    simplify() will also perform alpha substitution.
    
    Original author: Ivan Jager
 *)

open ExtList
open Vine
open Vine_util

module D = Debug.Make(struct let name = "Vine_opt" and default=`NoDebug end)
open D

module VH = Vine.VarHash


type alias = MayAlias | DoesAlias | PartialAlias | NoAlias


(* some helper functions *)

(* These fix* functions are duplicated from
   Execution.exec_utils. That's not ideal, but I'm not sure of a better
   place. *)
let fix_u1  x = Int64.logand x 0x1L
let fix_u8  x = Int64.logand x 0xffL
let fix_u16 x = Int64.logand x 0xffffL
let fix_u32 x = Int64.logand x 0xffffffffL

let fix_s1  x = Int64.shift_right (Int64.shift_left x 63) 63
let fix_s8  x = Int64.shift_right (Int64.shift_left x 56) 56
let fix_s16 x = Int64.shift_right (Int64.shift_left x 48) 48
let fix_s32 x = Int64.shift_right (Int64.shift_left x 32) 32

(* drop high bits *)
let to64 v =
    match v with
	Int(t,i) ->   let bits = 64 - bits_of_width t in
	  Int64.shift_right_logical (Int64.shift_left i bits) bits
      | _ -> raise (Invalid_argument "to64 is only for integers")

(* sign extend to 64 bits*)
let tos64 v =
    match v with
	Int(t,i) ->   let bits = 64 - bits_of_width t in
	  Int64.shift_right (Int64.shift_left i bits) bits
      | _ -> raise (Invalid_argument "tos64 is only for integers")
  
(* shifting by more than the number of bits or by negative values
 * will be the same as shifting by the number of bits. *)
let toshift max t v =
  let i = to64  v in
    if i <= Int64.of_int max && i >= 0L
    then Int64.to_int i
    else
      (prerr_endline("Warning: shifting "^string_of_int max^"-bit value by "
		    ^Int64.to_string i);
       max)

(* "cast" an int64 to a value *)
let to_val t v =
  let mask = Int64.shift_right_logical (-1L) (64-bits_of_width t) in
    Constant(Int(t,Int64.logand mask v))

(* Combine two bitvectors into a longer one. *)
let bv_concat t v1 v2 =
  Int64.logor v2 (Int64.shift_left v1 (bits_of_width t))

(* flatten an expression to make it easier to rearange binops
 * Note: Should only be used with associative binops. *)
let rec flatten_binop op exp =
  match exp with
      BinOp(o, e1, e2) when o = op ->
	flatten_binop op e1 @ flatten_binop op e2
    | _ -> [exp]



(* exp_eq : exp -> exp -> bool option *)
(** Check if two expression are equal

    Note: When this function says two expressions are equivalent, it means they
    are equivalent if they appear in the same context or equivalent contexts.

    FIXME: This function could be more accurate if it also took the two
    contexts as arguments. (Eg, when e1 references x, and e2 references y, but
    in e1's context x is the same as the y is in e2's context.

    @return Some true if e1 \equiv e2,
    Some false, if e1 is never = e2,
    or None if we can't determine it yet. *)
let exp_eq e1 e2 =
  (* FIXME: canonicalize expressions so that they can be compared better *)
  match (e1, e2) with
      (Constant(v1), Constant(v2)) when v1 = v2 -> Some true
    | (Constant _, Constant _) -> Some false
    | _ when e1 = e2 -> Some true
    | _ -> None
    
let flip_bool e =
  match e with
    | UnOp(NOT, e) -> e
    | _ -> UnOp(NOT, e)
      
(** Performs simple contstant folding without recursing.
    (ie. only on the toplevel expression)
    Use constant_simplify instead if you want to also rearange expressions.
    @param ctx The context is a function from lval to exp option. When it
    return some, the lval will be replaced by the returned expression. Be
    careful to make sure that said expression does not reference any shadowed
    variables.
    @param e The expression to preform constant folding on.
    @return an equivalent, but usually smaller expression.
*)
let rec constant_fold ctx e =
  match e with
      BinOp(MINUS, e1, e2) ->
	constant_fold ctx (BinOp(PLUS, e1, constant_fold ctx (UnOp(NEG, e2))))

    | BinOp(bop, Constant(Int(t,_) as v1), Constant(Int(t2,_) as v2)) ->
	(* let () = assert (t = t2) in *)
	(* let _ = Vine_typecheck.infer_type None e in *)
	  (match bop with
	      PLUS -> to_val t (Int64.add (to64 v1) (to64 v2))
	    | MINUS -> to_val t (Int64.sub (to64 v1) (to64 v2))
	    | TIMES -> to_val t (Int64.mul (to64  v1) (to64  v2))
	    | BITAND -> to_val t (Int64.logand (to64  v1) (to64  v2))
	    | BITOR -> to_val t (Int64.logor (to64  v1) (to64  v2))
	    | XOR -> to_val t (Int64.logxor (to64  v1) (to64  v2))
	    | EQ ->
		exp_bool((to64 v1) = (to64 v2))
	    | NEQ ->
		exp_bool((to64 v1) <> (to64 v2))
	    | LSHIFT ->
		to_val t (Int64.shift_left
			    (to64 v1) 
			    (toshift (bits_of_width t) t2 v2) )
	    | RSHIFT ->
		to_val t (Int64.shift_right_logical
			    (to64 v1)
			    (toshift (bits_of_width t) t2 v2) )
	    | ARSHIFT ->
		to_val t (Int64.shift_right
			    (tos64  v1)
			    (toshift (bits_of_width t) t2 v2) )
   (* Int64.div rounds towards zero. What do we want? *)
	    | DIVIDE -> to_val t (int64_udiv (tos64  v1) (tos64 v2))
	    | SDIVIDE -> to_val t (Int64.div (tos64 v1) (tos64  v2))
	    | MOD -> to_val t (int64_urem (tos64 v1) (tos64 v2))
	    | SMOD -> to_val t (Int64.rem (tos64 v1) (tos64 v2))
	    | CONCAT -> to_val (double_width t)
		(bv_concat t (to64 v1) (to64 v2))
	    | SLT -> exp_bool(tos64  v1 < tos64 v2)
	    | SLE -> exp_bool(tos64  v1 <= tos64  v2)
	    | LT -> exp_bool(int64_ucompare (to64 v1) (to64 v2) < 0)
	    | LE -> exp_bool(int64_ucompare (to64 v1) (to64 v2) <= 0)
	 )
    (* Lots of things (Vine_ceval, FuzzBALL, etc.) assume that constant
       folding can simplify (evaluate) any expression using constants. So
       fail if we run into a missing case. *)
    | BinOp(_, Constant(_), Constant(_)) ->
	failwith "Constant folding failed for BinOp"
    | UnOp(op, Constant(Int(t,_) as v)) ->
	(match op with
	    NEG -> to_val t (Int64.neg (to64  v))
	  | NOT -> to_val t (Int64.lognot (to64  v))
	)
    | UnOp(_, Constant(_)) ->
	failwith "Constant folding failed for UnOp"
    | FBinOp((FPLUS|FMINUS|FTIMES|FDIVIDE) as bop, rm,
	     Constant(Int(REG_32,v1)), Constant(Int(REG_32,v2))) ->
	let f32_op =
	  match bop with
	    | FPLUS   -> f32_add
	    | FMINUS  -> f32_sub
	    | FTIMES  -> f32_mul
	    | FDIVIDE -> f32_div
	    | (FEQ|FNEQ|FLT|FLE) -> failwith "Can't happen"
	in
	let vr = Int64.of_int32 (f32_op rm (Int64.to_int32 v1)
				   (Int64.to_int32 v2))
	in
	  Constant(Int(REG_32, vr))
    | FBinOp((FEQ|FNEQ|FLT|FLE) as bop, rm,
	     Constant(Int(REG_32,v1)), Constant(Int(REG_32,v2))) ->
	let f32_op =
	  match bop with
	    | FEQ  -> f32_eq
	    | FNEQ -> f32_ne
	    | FLT  -> f32_lt
	    | FLE  -> f32_le
	    | (FPLUS|FMINUS|FTIMES|FDIVIDE) -> failwith "Can't happen"
	in
	  exp_bool (f32_op rm (Int64.to_int32 v1) (Int64.to_int32 v2))

    | FBinOp((FPLUS|FMINUS|FTIMES|FDIVIDE) as bop, rm,
	     Constant(Int(REG_64,v1)), Constant(Int(REG_64,v2))) ->
	let f64_op =
	  match bop with
	    | FPLUS   -> f64_add
	    | FMINUS  -> f64_sub
	    | FTIMES  -> f64_mul
	    | FDIVIDE -> f64_div
	    | (FEQ|FNEQ|FLT|FLE) -> failwith "Can't happen"
	in
	  Constant(Int(REG_64, (f64_op rm v1 v2)))
    | FBinOp((FEQ|FNEQ|FLT|FLE) as bop, rm,
	     Constant(Int(REG_64,v1)), Constant(Int(REG_64,v2))) ->
	let f64_op =
	  match bop with
	    | FEQ  -> f64_eq
	    | FNEQ -> f64_ne
	    | FLT  -> f64_lt
	    | FLE  -> f64_le
	    | (FPLUS|FMINUS|FTIMES|FDIVIDE) -> failwith "Can't happen"
	in
	  exp_bool (f64_op rm v1 v2)
    | FBinOp(_, _, Constant(_), Constant(_)) ->
	failwith "Constant folding failed for FBinOp"
    | FUnOp(uop, rm, Constant(Int((REG_32|REG_64) as ty, v))) ->
	(match (uop, ty) with
	   | (FNEG, REG_64) -> Constant(Int(REG_64, (f64_neg rm v)))
	   | (FNEG, REG_32) ->
	       let vr = Int64.of_int32 (f32_neg rm (Int64.to_int32 v)) in
		 Constant(Int(ty, vr))
	   | (FNEG, _) -> failwith "Can't happen")
    | FUnOp(_, _, Constant(_)) ->
	failwith "Constant folding failed for FUnOp"
    | Cast(ct, t2, Constant(Int(t,_) as v)) ->
	let bits1 = bits_of_width t in
	let bits = bits_of_width t2 in
	(match ct with
	    CAST_UNSIGNED ->
	      to_val t2 (to64  v)
	  | CAST_SIGNED ->
	      to_val t2 (tos64  v)
	  | CAST_HIGH ->
     	      to_val t2
		(Int64.shift_right 
		    (Int64.logand (to64  v)
			(Int64.shift_left (-1L) (bits1-bits)) )
		    (bits1-bits) )
	  | CAST_LOW ->
	      to_val t2
		(Int64.logand (to64  v)
		    ((Int64.lognot(Int64.shift_left (-1L) bits))) )
	)
    | Cast(_, _, Constant(_)) ->
	failwith "Constant folding failed for Cast"
    | FCast((CAST_SFLOAT|CAST_UFLOAT) as ct,
	    rm, ((REG_32|REG_64) as ty2), Constant(Int(ty1, i) as v)) ->
	let signed = (ct = CAST_SFLOAT) in
	let i64 = (if signed then tos64 else to64) v in
	let f = (if signed then Int64.to_float else int64_u_to_float) i64 in
	let i2 =
	  match ty2 with
	    | REG_32 -> Int64.of_int32 (Int32.bits_of_float f)
	    | REG_64 -> Int64.bits_of_float f
	    | _ -> failwith "Can't happen"
	in
	  Constant(Int(ty2, i2))
    | FCast((CAST_SFIX|CAST_UFIX) as ct, rm, ty2,
	    Constant(Int((REG_32|REG_64) as ty1, i))) ->
	let signed = (ct = CAST_SFIX) in
	let f = match ty1 with
	  | REG_32 -> Int32.float_of_bits (Int64.to_int32 i)
	  | REG_64 -> Int64.float_of_bits i
	  | _ -> failwith "Can't happen"
	in
	let i64 = (if signed then Int64.of_float else int64_u_of_float) f in
	  to_val ty2 i64
    | FCast(CAST_FWIDEN, rm, REG_64, Constant(Int(REG_32, i))) ->
	ignore(rm);
	let f = Int32.float_of_bits (Int64.to_int32 i) in
	let i2 = Int64.bits_of_float f in
	  Constant(Int(REG_64, i2))
    | FCast(CAST_FNARROW, rm, REG_32, Constant(Int(REG_64, i))) ->
	ignore(rm);
	let f = Int64.float_of_bits i in
	let i2 = Int64.of_int32 (Int32.bits_of_float f) in
	  Constant(Int(REG_32, i2))
    | FCast(_, _, _, Constant(_)) ->
	failwith "Constant folding failed for FCast"
    (*  some identities *)
    | BinOp(BITAND, _, (Constant(Int(_, 0L)) as c)) ->
	c
    | BinOp(BITAND, x, Constant(v)) when tos64 v = -1L ->
	x
    | BinOp(BITOR, x, (Constant(Int(_, 0L)))) ->
	x
    | BinOp(BITOR, _, (Constant(v) as c)) when tos64 v = -1L ->
	c
    | BinOp(XOR, x, (Constant(Int(_, 0L)))) ->
	x
    | BinOp(PLUS, x, (Constant(Int(_, 0L)))) ->
	x
    | BinOp(LSHIFT, x, (Constant(Int(_, 0L)))) ->
	x
    | BinOp(RSHIFT, x, (Constant(Int(_, 0L)))) ->
	x
    | BinOp(ARSHIFT, x, (Constant(Int(_, 0L)))) ->
	x
    | BinOp(TIMES, x, (Constant(Int(_, 1L)))) ->
	x
    | BinOp((DIVIDE|SDIVIDE), x, (Constant(Int(_, 1L)))) ->
	x
    | BinOp((MOD|SMOD), x, (Constant(Int(ty, 1L)))) ->
	Constant(Int(ty, 0L))
    | UnOp(NOT, BinOp(PLUS, e1, Constant(Int(_, -1L)))) ->
	UnOp(NEG, e1)
    | UnOp(NEG, UnOp(NEG, x)) ->
	x
    | UnOp(NOT, UnOp(NOT, x)) ->
	x

    | Cast(ct2, w2, Cast(ct1, w1, e1)) when ct1 = ct2 ->
	Cast(ct1, w2, e1) (* no redundant double casts *)
    (* Widening cast followed by narrowing cast with same type *)
    | Cast(CAST_LOW,t2,Cast(CAST_UNSIGNED,_,e)) 
	when ((Vine_typecheck.infer_type None e) = t2) -> e
    | Cast(CAST_LOW,t2,Cast(CAST_SIGNED,_,e)) 
	when ((Vine_typecheck.infer_type None e) = t2) -> e
    (* Redundant widening inside narrowing *)
    | Cast(CAST_LOW, t2, Cast((CAST_SIGNED|CAST_UNSIGNED), t1, e))
	when (let w_e = bits_of_width (Vine_typecheck.infer_type None e) and
		  w_2 = bits_of_width t2 in
		w_2 < w_e) ->
	Cast(CAST_LOW, t2, e)
    (* Widening followed by narrowing equivalent to narrower widening *)
    | Cast(CAST_LOW, t1, Cast((CAST_SIGNED|CAST_UNSIGNED) as cast_ty, t2, e))
	when (let w1 = bits_of_width t1 and
		  w3 = bits_of_width (Vine_typecheck.infer_type None e) in
		w3 <= w1) ->
	Cast(cast_ty, t1, e)
    (* High cast selects only the zero bits from of an unsigned cast *)
    | Cast(CAST_HIGH, t1, Cast(CAST_UNSIGNED, t2, e3))
	when (let w1 = bits_of_width t1 and
		  w2 = bits_of_width t2 and
		  w3 = bits_of_width (Vine_typecheck.infer_type None e3) in
		w1 <= (w2 - w3))
	  -> Constant(Int(t1, 0L))
    (* U widen then S widen same as single U widen *)
    | Cast(CAST_SIGNED, t1, Cast(CAST_UNSIGNED, t2, e3))
	when (let w2 = bits_of_width t2 and
		  w3 = bits_of_width (Vine_typecheck.infer_type None e3) in
		w3 < w2)
	-> Cast(CAST_UNSIGNED, t1, e3)
    (* Boolean -> integer -> boolean conversion with == 0 *)
    | BinOp(EQ, Cast((CAST_SIGNED|CAST_UNSIGNED), _, e),
	    Constant(Int(_, 0L)))
	when ((Vine_typecheck.infer_type None e) = REG_1)
      -> (flip_bool e)
    (* Cast followed by AND operation that cancels effect of cast *)
    | BinOp(BITAND,Cast(CAST_UNSIGNED, REG_32, e),Constant(Int(REG_32,0xffL))) 
	when ((Vine_typecheck.infer_type None e) = REG_8) ->
	  Cast(CAST_UNSIGNED, REG_32, e)
    | BinOp(BITAND,Cast(CAST_UNSIGNED, REG_32, e),Constant(Int(REG_32,0xffffL))) 
	when ((Vine_typecheck.infer_type None e) = REG_16) ->
	  Cast(CAST_UNSIGNED, REG_32, e)
    | BinOp(BITAND,Cast(CAST_SIGNED, REG_32, e),Constant(Int(REG_32,0xffL))) 
	when ((Vine_typecheck.infer_type None e) = REG_8) ->
	  Cast(CAST_UNSIGNED, REG_32, e)
    | BinOp(BITAND,Cast(CAST_SIGNED, REG_32, e),Constant(Int(REG_32,0xffffL))) 
	when ((Vine_typecheck.infer_type None e) = REG_16) ->
	  Cast(CAST_UNSIGNED, REG_32, e)
    (* Cast followed by left shift followed by unnecessary AND operation *)
    | BinOp(BITAND,(BinOp(LSHIFT,Cast(CAST_UNSIGNED, REG_32, e),
	Constant(Int(REG_8,0x8L)))),Constant(Int(REG_32,0xff00L))) 
	when ((Vine_typecheck.infer_type None e) = REG_8) ->
	  BinOp(LSHIFT,Cast(CAST_UNSIGNED, REG_32, e),
	    Constant(Int(REG_32,0x8L))) 
    | BinOp(BITAND,(BinOp(LSHIFT,Cast(CAST_UNSIGNED, REG_32, e),
	Constant(Int(REG_8,0x10L)))),Constant(Int(REG_32,0xff0000L))) 
	when ((Vine_typecheck.infer_type None e) = REG_8) ->
	  BinOp(LSHIFT,Cast(CAST_UNSIGNED, REG_32, e),
	    Constant(Int(REG_32,0x10L))) 
    | BinOp(BITAND,(BinOp(LSHIFT,Cast(CAST_UNSIGNED, REG_32, e),
	Constant(Int(REG_8,0x18L)))),Constant(Int(REG_32,0xff000000L))) 
	when ((Vine_typecheck.infer_type None e) = REG_8) ->
	  BinOp(LSHIFT,Cast(CAST_UNSIGNED, REG_32, e),
	    Constant(Int(REG_32,0x18L))) 
    (* Redundat cast and AND *)
    | Cast(CAST_LOW, REG_8, BinOp(BITAND, e, Constant(Int(_,0xffL)))) ->
	Cast(CAST_LOW, REG_8, e)
    | Cast(CAST_LOW, REG_16, BinOp(BITAND, e, Constant(Int(_,0xffffL)))) ->
	Cast(CAST_LOW, REG_16, e)
    | Cast(CAST_LOW, REG_32, BinOp(BITAND, e, Constant(Int(_,0xffffffffL)))) ->
	Cast(CAST_LOW, REG_32, e)
    (* Low cast gets only 0 due to left shift *)
    | Cast(CAST_LOW, cty, BinOp(LSHIFT, e, Constant(Int(_, amt))))
	when amt >= Int64.of_int (bits_of_width cty) ->
	Constant(Int(cty, 0L))
    (* A different way a mask can be redundant with a cast *)
    | BinOp(BITAND,
	    (Cast(CAST_UNSIGNED, (REG_16|REG_32|REG_64), e) as thecast),
            Constant(Int(_, mask)))
	when ((Vine_typecheck.infer_type None e) = REG_8) &&
          (Int64.logand mask 0xffL) = 0xffL ->
	thecast
    | BinOp(BITAND,
	    (Cast(CAST_UNSIGNED, (REG_32|REG_64), e) as thecast),
            Constant(Int(_, mask)))
	when ((Vine_typecheck.infer_type None e) = REG_16) &&
          (Int64.logand mask 0xffffL) = 0xffffL ->
	thecast
    | BinOp(BITAND,
	    (Cast(CAST_UNSIGNED, REG_64, e) as thecast),
            Constant(Int(_, mask)))
	when ((Vine_typecheck.infer_type None e) = REG_32) &&
          (Int64.logand mask 0xffffffffL) = 0xffffffffL ->
	thecast
    (* A more complex way of writing sign extension *)
    | BinOp(BITOR, Cast(CAST_UNSIGNED, REG_64, e1),
	    BinOp(LSHIFT,
		  Cast(CAST_UNSIGNED, REG_64,
		       BinOp(ARSHIFT, e2, Constant(Int(_, 31L)))),
		  Constant(Int(_, 32L))))
	when e1 = e2 && ((Vine_typecheck.infer_type None e1) = REG_32)
	  -> Cast(CAST_SIGNED, REG_64, e1)
    | BinOp(BITOR, Cast(CAST_UNSIGNED, REG_32, e1),
	    BinOp(LSHIFT,
		  Cast(CAST_UNSIGNED, REG_32,
		       BinOp(ARSHIFT, e2, Constant(Int(_, 15L)))),
		  Constant(Int(_, 16L))))
	when e1 = e2 && ((Vine_typecheck.infer_type None e1) = REG_16)
	  -> Cast(CAST_SIGNED, REG_32, e1)
    | BinOp(BITOR, Cast(CAST_UNSIGNED, REG_16, e1),
	    BinOp(LSHIFT,
		  Cast(CAST_UNSIGNED, REG_16,
		       BinOp(ARSHIFT, e2, Constant(Int(_, 7L)))),
		  Constant(Int(_, 8L))))
	when e1 = e2 && ((Vine_typecheck.infer_type None e1) = REG_8)
	  -> Cast(CAST_SIGNED, REG_16, e1)
    (* Impossible equalities with extension casts *)
    | BinOp(EQ, Cast(CAST_UNSIGNED, (REG_16|REG_32|REG_64), e1),
	    Constant(Int(_, c)))
	when (Vine_typecheck.infer_type None e1) = REG_8
	  && c <> fix_u8 c
	  -> exp_false
    | BinOp(EQ, Cast(CAST_SIGNED, REG_16, e1),
	    Constant(Int(_, c)))
	when (Vine_typecheck.infer_type None e1) = REG_8
	  && c <> fix_u16 (fix_s8 c)
	  -> exp_false
    | BinOp(EQ, Cast(CAST_SIGNED, REG_32, e1),
	    Constant(Int(_, c)))
	when (Vine_typecheck.infer_type None e1) = REG_8
	  && c <> fix_u32 (fix_s8 c)
	  -> exp_false
    | BinOp(EQ, Cast(CAST_SIGNED, REG_64, e1),
	    Constant(Int(_, c)))
	when (Vine_typecheck.infer_type None e1) = REG_8
	  && c <> fix_s8 c
	  -> exp_false
    | BinOp(EQ, Cast(CAST_UNSIGNED, (REG_32|REG_64), e1),
	    Constant(Int(_, c)))
	when (Vine_typecheck.infer_type None e1) = REG_16
	  && c <> fix_u16 c
	  -> exp_false
    | BinOp(EQ, Cast(CAST_SIGNED, REG_32, e1),
	    Constant(Int(_, c)))
	when (Vine_typecheck.infer_type None e1) = REG_16
	  && c <> fix_u32 (fix_s16 c)
	  -> exp_false
    | BinOp(EQ, Cast(CAST_SIGNED, REG_64, e1),
	    Constant(Int(_, c)))
	when (Vine_typecheck.infer_type None e1) = REG_16
	  && c <> fix_s16 c
	  -> exp_false
    | BinOp(EQ, Cast(CAST_UNSIGNED, REG_64, e1),
	    Constant(Int(_, c)))
	when (Vine_typecheck.infer_type None e1) = REG_32
	  && c <> fix_u32 c
	  -> exp_false
    | BinOp(EQ, Cast(CAST_SIGNED, REG_64, e1),
	    Constant(Int(_, c)))
	when (Vine_typecheck.infer_type None e1) = REG_32
	  && c <> fix_s32 c
	  -> exp_false
    | Cast(ct, ty, e) when (Vine_typecheck.infer_type None e) = ty ->
	e
    | Lval l ->
	(match ctx l with
	    Some c -> c
	   | None -> e
	)
    | Ite(((Constant(Int(_,_))) as cond), e1, e2) ->
	if (bool_of_const cond) then e1 else e2
    | Ite(cond, e1, e1') when e1 = e1' -> e1
    | Ite(UnOp(NOT, c), x, y) -> Ite(c, y, x)
    | Ite(cond, Constant(Int(REG_1, 1L)), Constant(Int(REG_1, 0L))) -> cond
    | Ite(cond, Constant(Int(REG_1, 0L)), Constant(Int(REG_1, 1L))) ->
        UnOp(NOT, cond)
    | Ite(cond, Constant(Int(REG_1, 1L)), cond2) ->
        BinOp(BITOR, cond, cond2)
    | Ite(cond, cond2, Constant(Int(REG_1, 0L))) ->
        BinOp(BITAND, cond, cond2)
    (* These next two rules seem questionable. We've seen cases where
       they help, but it's risky that they make the tree bigger. The
       binop one with + also can interfere with symbolic address
       parsing. *)
    | Cast(ct, ty, Ite(cond, e1, e2)) ->
        Ite(cond, Cast(ct, ty, e1), Cast(ct, ty, e2))
    | BinOp(op, Ite(cond, e1, e2), (Constant(_) as k)) when op <> PLUS ->
        Ite(cond, BinOp(op, e1, k), BinOp(op, e2, k))
    (* Rules involving CONCAT: *)
    | Cast(CAST_LOW, REG_8, BinOp(CONCAT, e_h, e_l))
	when (Vine_typecheck.infer_type None e_l) = REG_8 -> e_l
    | Cast(CAST_LOW, REG_16, BinOp(CONCAT, e_h, e_l))
	when (Vine_typecheck.infer_type None e_l) = REG_16 -> e_l
    | Cast(CAST_LOW, REG_32, BinOp(CONCAT, e_h, e_l))
	when (Vine_typecheck.infer_type None e_l) = REG_32 -> e_l
    | Cast(CAST_HIGH, REG_8, BinOp(CONCAT, e_h, e_l))
	when (Vine_typecheck.infer_type None e_h) = REG_8 -> e_h
    | Cast(CAST_HIGH, REG_16, BinOp(CONCAT, e_h, e_l))
	when (Vine_typecheck.infer_type None e_h) = REG_16 -> e_h
    | Cast(CAST_HIGH, REG_32, BinOp(CONCAT, e_h, e_l))
	when (Vine_typecheck.infer_type None e_h) = REG_32 -> e_h
    | Cast(CAST_LOW, REG_1, BinOp(CONCAT, e_h, e_l)) ->
	Cast(CAST_LOW, REG_1, e_l)
    | Cast(CAST_HIGH, REG_1, BinOp(CONCAT, e_h, e_l)) ->
	Cast(CAST_HIGH, REG_1, e_h)
    | BinOp(CONCAT, Constant(Int(REG_8, 0L)), x) ->
       Cast(CAST_UNSIGNED, REG_16, x)
    | BinOp(CONCAT, Constant(Int(REG_16, 0L)), x) ->
       Cast(CAST_UNSIGNED, REG_32, x)
    | BinOp(CONCAT, Constant(Int(REG_32, 0L)), x) ->
       Cast(CAST_UNSIGNED, REG_64, x)
    (* AND / OR with itself *)
    | BinOp(BITOR, x, y)
    | BinOp(BITAND, x, y)
	when x = y ->
	x
    | BinOp((EQ|LE|SLE), x, y)
	when x = y ->
	exp_true 
    | BinOp((NEQ|LT|SLT), x, y)
	when x = y ->
	exp_false
    (* Repeated shifts of the same type *)
    | BinOp(LSHIFT, BinOp(LSHIFT, x, Constant(Int(ty1, s1))),
	    Constant(Int(ty2, s2)))
	when ty1 = ty2 && s1 >= 0L && s2 >= 0L ->
	BinOp(LSHIFT, x, (Constant(Int(ty1, (Int64.add s1 s2)))))
    | BinOp(RSHIFT, BinOp(RSHIFT, x, Constant(Int(ty1, s1))),
	    Constant(Int(ty2, s2)))
	when ty1 = ty2 && s1 >= 0L && s2 >= 0L ->
	BinOp(RSHIFT, x, (Constant(Int(ty1, (Int64.add s1 s2)))))
    | BinOp(ARSHIFT, BinOp(ARSHIFT, x, Constant(Int(ty1, s1))),
	    Constant(Int(ty2, s2)))
	when ty1 = ty2 && s1 >= 0L && s2 >= 0L ->
	BinOp(ARSHIFT, x, (Constant(Int(ty1, (Int64.add s1 s2)))))
    (* Common compiler optimization of x /u 10 *)
    | BinOp(RSHIFT,
	    Cast(CAST_HIGH, REG_32,
		 BinOp(TIMES, Cast(CAST_UNSIGNED, REG_64, x),
		       Constant(Int(_, 0xcccccccdL)))),
	    Constant(Int(_, 3L)))
	when (Vine_typecheck.infer_type None x) = REG_32 ->
	BinOp(DIVIDE, x, Constant(Int(REG_32, 10L)))

    (* Left shift combined with multiplication *)
    | BinOp(LSHIFT,
	    BinOp(TIMES, x, Constant(Int(ty, factor))),
	    Constant(Int(_, shift)))
	when let factor2 = Int64.shift_left factor (Int64.to_int shift) in
	  Constant(Int(ty, factor2)) = to_val ty factor2
      ->
	let factor2 = Int64.shift_left factor (Int64.to_int shift) in
	  BinOp(TIMES, x, Constant(Int(ty, factor2)))

    (* Modulo as the remainder after integer division *)
    | BinOp(PLUS, x1, UnOp(NEG, BinOp(TIMES, BinOp(DIVIDE, x2, k1), k2)))
	when x1 = x2 && k1 = k2 ->
	BinOp(MOD, x1, k1)
    | BinOp(PLUS, UnOp(NEG, BinOp(TIMES, BinOp(DIVIDE, x2, k1), k2)), x1)
	when x1 = x2 && k1 = k2 ->
	BinOp(MOD, x1, k1)
    | BinOp(PLUS, UnOp(NEG, BinOp(TIMES, BinOp(DIVIDE, x2, k1), k2)),
	    BinOp(PLUS, x1, y))
	when x1 = x2 && k1 = k2 ->
	BinOp(PLUS, BinOp(MOD, x1, k1), y)
    (* byte & 0xffffff00 = 0 *)
    | BinOp(BITAND,
	    Cast(CAST_UNSIGNED, REG_32, e),
	    Constant(Int(REG_32, 0xffffff00L)))
	when (Vine_typecheck.infer_type None e) = REG_8 ->
	Constant(Int(REG_32, 0L))
    (* zero-extend shift by at least reg size gives zero *)
    | BinOp((LSHIFT|RSHIFT), e, Constant(Int(_, amt)))
	when (Vine_typecheck.infer_type None e) = REG_8 && amt >= 8L ->
	Constant(Int(REG_8, 0L))
    | BinOp((LSHIFT|RSHIFT), e, Constant(Int(_, amt)))
	when (Vine_typecheck.infer_type None e) = REG_16 && amt >= 16L ->
	Constant(Int(REG_16, 0L))
    | BinOp((LSHIFT|RSHIFT), e, Constant(Int(_, amt)))
	when (Vine_typecheck.infer_type None e) = REG_32 && amt >= 32L ->
	Constant(Int(REG_32, 0L))
    | BinOp((LSHIFT|RSHIFT), e, Constant(Int(_, amt)))
	when (Vine_typecheck.infer_type None e) = REG_64 && amt >= 64L ->
	Constant(Int(REG_64, 0L))
    (* byte >> amt = 0  when amt >= 8: special case of above within larger word *)
    | BinOp(RSHIFT,
	    Cast(CAST_UNSIGNED, REG_32, e),
	    Constant(Int(_, amt)))
	when (Vine_typecheck.infer_type None e) = REG_8 && amt >= 8L ->
	Constant(Int(REG_32, 0L))
    | BinOp(RSHIFT,
	    Cast(CAST_UNSIGNED, REG_64, e),
	    Constant(Int(_, amt)))
	when (Vine_typecheck.infer_type None e) = REG_8 && amt >= 8L ->
	Constant(Int(REG_64, 0L))
    (* (c ? k : k + 1) = (k + (int)c) *)
    | BinOp(BITOR,
	    BinOp(BITAND, Cast(CAST_SIGNED, REG_32, c1),
		  Constant(Int(REG_32, k1))),
	    BinOp(BITAND, UnOp(NOT, Cast(CAST_SIGNED, REG_32, c2)),
		  Constant(Int(REG_32, k2))))
	when c1 = c2 && k2 = (Int64.add k1 1L) ->
	BinOp(PLUS, Constant(Int(REG_32, k1)),
	      Cast(CAST_UNSIGNED, REG_32, c1))
    (* x + -x = 0 *)
    | BinOp(PLUS, x, UnOp(NEG, y)) when x = y ->
	Constant(Int((Vine_typecheck.infer_type None x), 0L))
    (* -x + x = 0 *)
    | BinOp(PLUS, UnOp(NEG, x), y) when x = y ->
	Constant(Int((Vine_typecheck.infer_type None x), 0L))
    (* x + x = x << 1 *)
    | BinOp(PLUS, x, y) when x = y ->
	BinOp(LSHIFT, x, Constant(Int(REG_8, 1L)))
    (* x + (x << 1) = 3 * x *)
    | BinOp(PLUS, x, BinOp(LSHIFT, y, Constant(Int(_, 1L))))
	when x = y ->
	BinOp(TIMES,
	      Constant(Int((Vine_typecheck.infer_type None x), 3L)),
	      x)
    (* x + (x << 2) = 5 * x *)
    | BinOp(PLUS, x, BinOp(LSHIFT, y, Constant(Int(_, 2L))))
	when x = y ->
	BinOp(TIMES,
	      Constant(Int((Vine_typecheck.infer_type None x), 5L)),
	      x)
    (* x + -x + y  = y *)
    | BinOp(PLUS, x, BinOp(PLUS, UnOp(NEG, y), z)) when x = y ->
	z
    (* x & !x = 0 *)
    | BinOp(BITAND, x, UnOp(NOT, y)) when x = y ->
	Constant(Int((Vine_typecheck.infer_type None x), 0L))
    (* (x & y) | (x & !y) == x *)
    | BinOp(BITOR, BinOp(BITAND, x1, y1),
	    BinOp(BITAND, x2, (UnOp(NOT, y2)))) when x1 = x2 && y1 = y2 ->
	x1
    (* x | (!x & y) == x | y *)
    | BinOp(BITOR, x1,
	    BinOp(BITAND, UnOp(NOT, x2), y)) when x1 = x2 ->
	BinOp(BITOR, x1, y)
    (* x ^ x = 0 *)
    | BinOp(XOR, x, y) when x = y ->
	Constant(Int((Vine_typecheck.infer_type None x), 0L))
    (* x ^ x ^ y = y *)
    | BinOp(XOR, x, BinOp(XOR, y, z)) when x = y ->
	z
    (* x + c = 0 -> x = -c, for c constant *)
    | BinOp(EQ, BinOp(PLUS, x, (Constant(_) as c)),
	    Constant(Int(ty, 0L))) ->
	BinOp(EQ, x, (constant_fold ctx (UnOp(NEG, c))))
    (* a + -b = 0 ==> a == b *)
    | BinOp(EQ, BinOp(PLUS, a, UnOp(NEG, b)),
	    Constant(Int(ty, 0L))) ->
	BinOp(EQ, a, b)
    (* a ^ b = 0 ==> a == b *)
    | BinOp(EQ, BinOp(XOR, a, b), Constant(Int(ty, 0L))) ->
	BinOp(EQ, a, b)
    (* a < b | a == b ==> a <= b*)
    | BinOp(BITOR, BinOp(LT, a1, b1), BinOp(EQ, a2, b2))
	 when a1 = a2 && b1 = b2 ->
	BinOp(LE, a1, b1)
    (* a <$ b | a == b ==> a <=$ b*)
    | BinOp(BITOR, BinOp(SLT, a1, b1), BinOp(EQ, a2, b2))
	 when a1 = a2 && b1 = b2 ->
	BinOp(SLE, a1, b1)
    (* (a | c) == 0 ==> false, if c is a non-zero constant *)
    | BinOp(EQ, BinOp(BITOR, a, Constant(Int(_, c))), Constant(Int(_, 0L)))
	when c <> 0L ->
	exp_false
    (* ((a | c) << 32) == 0 ==> false, if c is a non-low32-zero constant *)
    | BinOp(EQ, BinOp(LSHIFT, BinOp(BITOR, a, Constant(Int(_, c))),
		      Constant(Int(_, 32L))),
	    Constant(Int(_, 0L)))
	when (Int64.logand 0xffffffffL c) <> 0L ->
	exp_false
    (* ((a | c) << 32) <> 0 ==> true, if c is a non-low32-zero constant *)
    | BinOp(NEQ, BinOp(LSHIFT, BinOp(BITOR, a, Constant(Int(_, c))),
		       Constant(Int(_, 32L))),
	    Constant(Int(_, 0L)))
	when (Int64.logand 0xffffffffL c) <> 0L ->
	exp_true
    | _ -> e (* leave other expressions as they are *)


(** Performs constant folding, and canonicalizes commutative, associative
    operations to have constants on the right and be right associated. *)
let constant_fold_more ctx e =
  match e with
    | BinOp(bop, e1, e2) ->
	(match bop with
	    (* canonicalize commutative and associative binops so that constants
	       are on the right, and expressions are right associative *)
	    (* FIXME: check that the operands are not floats *)
	    (* associative and commutative binops, only on integer types *)
	    PLUS | TIMES | BITAND | BITOR | XOR
		->
		  let sort_fun a b =
		    match (a,b) with
			(Constant _, Constant _) -> compare a b
		      | (Constant _, _) -> -1
		      | (_, Constant _) -> 1
		      | _ -> compare a b
		  in
		  let l = flatten_binop bop e in
		    (match List.stable_sort sort_fun l with
		       | (x::xs) ->
			  List.fold_left
			    (fun x y -> constant_fold ctx (BinOp(bop, y, x)))
			    x xs
		      | _ -> failwith "flatten_binop returned []."
		    )
	  | EQ ->
	      (match exp_eq e1 e2 with
		  Some b -> exp_bool b
		| None -> constant_fold ctx e)
	  | NEQ ->
	      (match exp_eq e1 e2 with
		  Some b -> exp_bool (not b)
		| None -> constant_fold ctx e)
	  | _ -> constant_fold ctx e
	)
    | _ -> constant_fold ctx e

(* This was ok for arrays, but doesn't isn't really sufficient for memories.
   Eg, what should it return for x[y]:reg32_t x[y+1]:reg8_t
(** Check if two memory references alias each other *)
let rec mem_alias m1 m2 =
  let is_array_var (_,_,t) = 
    match (unwind_type t) with
	Array _ -> true
      | _ -> false
  in
  match (m1,m2) with
    | Mem(m1, a1, t1), Mem(m2,a2,t2) 
	when is_array_var m1 && is_array_var m2 -> 
	if not(Var.equal m1 m2) then NoAlias else
	(match exp_eq a1 a2 with
	    Some true -> DoesAlias
	  | Some false  -> NoAlias 
	  | None -> MayAlias
	)
    |  (Mem(m1, a1,t1), Mem(m2 ,a2,t2)) ->
	if (Var.equal m1 m2) && t1 = t2 then DoesAlias
	  else MayAlias
    | _ -> invalid_arg "mem alias requires Mem expressions"

and  substitute_mem enew mfor ein =
  let freemems = freemems_exp enew in
  let subvis =
    object
      inherit nop_vine_visitor
      method visit_exp e =
	match e with
	    Lval(Mem _ as t) when t = mfor ->
	      ChangeTo enew
	  | Let(Mem _ as t, _, _) when mem_alias t mfor <> NoAlias ->
	      SkipChildren (* be conservative *)
	  | Let(Mem _ as t, _, _)
	      when List.exists (fun x->mem_alias t x <> NoAlias) freemems ->
	      SkipChildren (* be conservative *)
	  | _ -> DoChildren
    end
  in
    exp_accept subvis ein
*)
      
let splitname = function
    Temp name  -> (name,None)
  | Mem(name,index,_) -> (name, Some index)


(** Returns a list of variable names that are shadowed within the given
    expression *)
let find_shadowed_vars e =
  let vis = object (self)
    inherit nop_vine_visitor
    val ctx = Hashtbl.create 10
    val mutable found = []

    method shadowed = found
    method visit_exp = function
	Let(l,e1,e2) ->
	  let (name,_) =  splitname l in
	    found <- name::found;
	    DoChildren
      | _ -> DoChildren
  end
  in
    ignore(exp_accept vis e);
    List.unique(vis#shadowed)

let find_freevars e =
  List.map (function Mem(v,_,_) | Temp v -> v) (freerefs_exp e)


(* Helper function for count_bindings and count_refs *)
let add_to_refcounts counts l =
      let (name,idx) = splitname l in
      let delta (dir,indir) = match idx with
	  Some _ -> (dir, indir+1)
	| None -> (dir+1, indir)
      in
      let count =
	try VH.find counts name
	with Not_found -> (0,0)
      in
	VH.replace counts name (delta count)
  

let count_bindings e =
  let bindings = VH.create 100 in
  let vis = object
    inherit nop_vine_visitor
    method visit_binding (l,e) =
      add_to_refcounts bindings l;
      DoChildren
  end in
    ignore(exp_accept vis e);
    bindings

let count_refs e =
  let refs = VH.create 100 in
  let vis = object
    inherit nop_vine_visitor
    method visit_rlvalue l =
      add_to_refcounts refs l;
      DoChildren
  end in
    ignore(exp_accept vis e);
    refs


class simplifying_visitor simplify (subst_single: lvalue -> exp -> bool) =
  let simplify_alvalue =
    let vis = object
      inherit nop_vine_visitor
      method visit_exp e = ChangeTo(simplify e)
    end
    in
      alvalue_accept vis
  in
object (self)
  inherit nop_vine_visitor

  (* variables that we can force substitution on as soon as we see them,
     because they only appear once in the entire expression, and aren't
     shadowed. Others may require more analysis. *)
  val forced_vars = VH.create 64

  method compute_forced e =
    VH.clear forced_vars;
    let refs = count_refs e in
    let binds = count_bindings e in
      VH.iter
	(fun name -> function 
	     (1,0) -> (
	       if try VH.find refs name = (1,0) with Not_found -> false
	       then VH.add forced_vars name ()
	       else ()
	     )
	   | (dir,indir) ->
	       dprintf
		 "Not marking '%s' for substitution yet, because it is bound in %d + %d places."
		 (var_to_string name) dir indir
	)
	binds
  (* context containing bound variables *)
  val ctx = VH.create 64

  (* Extend the context.
     Returns a function to put the old context back, and wrap a Let
     around it's argument if needed, in additon to visiting the
     subexpressions. *)
  method extend lval e1 =
    let (name,idx) = splitname lval in
    let refcount = ref 0 in
    let indref = ref 0 in (* number of indirect references *)
    let force =  idx = None && VH.mem forced_vars name  in
    let (lval,e1) = 
      if force then (alvalue_accept self lval, exp_accept self e1)
      else (lval, e1)
    in
    let unextend x =
      VH.remove ctx name;
      match (!refcount, !indref, force) with
	  (0,0,false) -> (* drop let expression *)
	    dprintf "Dropping unused binding of '%s'" (lval_to_string lval);
	    x
	| (0,0,true) ->
	    x
	| (1,0,false)
	    when subst_single lval e1  &&
	      not(list_does_intersect (find_freevars e1) (find_shadowed_vars x))
	      ->
	    (* force substitution *)
	    (* This can't be forced when variables are shadowed,
	       in particular, note that memory is very often shadowed
	    *)
	    let () = dprintf "Forcing substitution of '%s' with 1 ref" (lval_to_string lval) in
	    let (name,idx) = splitname(alvalue_accept self lval) in
	    let e1 = exp_accept self e1 in
	    let () = VH.add ctx name (idx, e1, refcount, indref, true) in
	    let res = exp_accept self x in
	      VH.remove ctx name;
	      res
	| (_,_,false) ->
	    Let(alvalue_accept self lval, exp_accept self e1, x)
	| (r,ir,true) -> 
	    Printf.printf "Forced, but got back %d %d\n%!" r ir;
	    failwith "Forced substitution, but refcount not 0"
    in
      VH.add ctx name (idx, e1, refcount, indref, force);
      unextend

  (* look up a replacement for the lval, and mark it/them as being referenced
     so that they are not dropped *)
  method lookup lval =
    let ((_,_,t) as name, index) = splitname lval in
    let relevant_ctx = VH.find_all ctx name in
      (* for debugging
    let () = print_string("Looking up '"^name^"' this relevant context:\n") in
    let () =
      List.iter (fun (idx,e1,drop) ->
		   print_string("  ["^ (match idx with None -> ""
					 | Some e -> exp_to_string e)
				^"] "^(if !drop then "drop" else "keep")^ "\n"))
	relevant_ctx
    in
      *)
      (* If lval is a temp, we need to flag the temp itself, as well as any
	 assignments into indices in it. (in the case that is an array).
	 If lval is a mem, we need to flag all assignments that may be aliases,
	 as well as the array itself. *)
    let rec find_subst res l = match l with
      | [] -> res
      | (idx,e1,refcount,indref,force)::ls ->
	  let get_result () =
	    match res with
		None ->
		  (match e1 with
		       Constant _ -> Some(Some e1)
		    (* | Some(oldctx, Temp _ as new_t) -> new_t  FIXME: alpha vary *)
		     | _ when force ->
			 dprintf "Forced substitution of %s" (lval_to_string lval);
			 Some(Some e1)
		     | _ ->
			 inc refcount;
			 Some None
		  )
	      | x -> x
	  in
	  match (idx,index) with
	      (None,None) -> 
		get_result();
	    | (None,Some _) ->
		inc indref;
		res (* Stop looking *)
	    | (Some idx, Some index) ->
		(* if both have indices, then we can only substitute if
		   we are sure this value wasn't shadowed by a subsequent
		   write. *)
		(* for now, we only attempt alias analysis on Arrays. For
		   memories, we always assume they may be aliased. *)
		(match (exp_eq idx index, unwind_type t) with
		     (Some true, Array _) ->
		       find_subst (get_result()) ls
		   | (Some false, Array _) ->
		       find_subst res ls
		   | (None, Array _)
		   | (_, TMem _) ->
		       let res = match res with
			   (* This assignment may or may not shadow
			      previous ones, so we can't substitute
			      unless we found one earlier. *)
			   None -> Some None
			 | x -> x
		       in
			 inc indref;
			 find_subst res ls
		   | _ ->
		       failwith "unexpected type with indices"
		)
	    | (Some idx, None) -> inc indref; find_subst res ls
    in
      match find_subst None relevant_ctx with
	  Some x -> x
	| None -> None
(* Eww, that was overly long and complicated, and it doesn't even handle cases
   like "let m[1] = 1 in let m2 = m in m2[1]" *)

  (* Whether we are at the toplevel of the expression *)
  val mutable at_toplevel = true

  method visit_exp e =
    let getres() = match e with
	Let(l, e1, e2) ->
	  (* these simplifications must not use self, because that would
	     artificially increase the reference count for our context *)
	  let e1 = simplify e1 in
	  let l = simplify_alvalue l in
	    (* drop the let binding *)
	    (* can't use ChangeDoChildrenPost, because we want to visit
	     * e2, not only it's children *)
	  let unextend = self#extend l e1 in
	    ChangeTo(unextend(exp_accept self e2))
      | _ ->
	  ChangeDoChildrenPost(e, constant_fold_more (self#lookup))
    in
      if at_toplevel
      then (at_toplevel <- false;
	    self#compute_forced e;
	    let res = getres() in
	      at_toplevel<-true;
	      res
	   )
      else getres()

  method visit_binding _ = SkipChildren (* already done in visit_exp *)
end

(** This should maybe not be exposed, but is used in vine_indepclauses.ml *)
let rec simplify_rec subst_more e =
  let passes = ref 0 in
  let simpler1 x =
    inc passes;
    if !passes > 2
    then dprintf "Going on to simplification pass #%d" !passes;
    exp_accept (new simplifying_visitor (simplify_rec subst_more) subst_more) x
  in
  let rec simpler x =
    let x' = simpler1 x in
      (* FIXME: this comparison is slow. Having a function that returs None
       * when it doesn't change anything might be better. *)
      if x = x' 
      then
	x
      else (
	(* prerr_endline "Note: Simplified to: ";
	pp_exp prerr_string x';	prerr_newline();
	prerr_endline "Note: Simplifying again..."; *)
	simpler x')
  in
    simpler e

(** Simplify an expression as much as possible.
    This function performs all supported simplification steps on the given
    expression.
    @return the simplified expression.
*)
let simplify = simplify_rec (fun _ _ -> true)


(** Like [simplify], but does not perform the slower variable substitution.
    Alpha varying the expression before calling this function will likely result
    in better simplification.
*)
let simplify_faster = simplify_rec (fun _ _ -> false)

(** Simplifies all subexpressions inside a statement *)
let simplify_stmt =
  let stmt_simplifier = object
    inherit nop_vine_visitor
    method visit_exp e =
      ChangeTo(simplify e)
  end
  in
  stmt_accept (stmt_simplifier :> vine_visitor)

(** make expressions bigger by doing back-substitution *)
let coalesce_stmts stmts maxtimes = 
  (* this is broken. It should be doing substitution backwards. *)
  stmts
(*
  let vis = 
object(self)
  inherit nop_vine_visitor
    
  val mutable ctx = Hashtbl.create 13
  val subst_cntr_ctx = Hashtbl.create 13

  method clear_subst_cntr_ctx () = 
    Hashtbl.clear subst_cntr_ctx

  method clear_ctx () = 
    Hashtbl.clear ctx

  method visit_exp e = 
    match e with
	Let(lv,e1,e2) ->
	  ChangeDoChildrenPost(e, 
			       (fun x -> Hashtbl.remove ctx lv; x))
      | Lval((Temp(v) as lv)) when Vine.is_not_memory v  ->  (
	    try
	      let (e':exp) = Hashtbl.find ctx lv in 
	      let cntr = 
		try
		  Hashtbl.find subst_cntr_ctx lv 
		with
		    Not_found -> 0
	      in
		if cntr < maxtimes then (
		  Hashtbl.replace subst_cntr_ctx lv (cntr+1);
		  ChangeTo(e') 
		) else SkipChildren

	    with
		Not_found ->  SkipChildren
	)
      | _ -> DoChildren
	  
  method visit_binding ((lv,e) as b) =
    ChangeDoChildrenPost(b, (fun x -> Hashtbl.add ctx lv e; x) )
    
  method insert_stmt_to_ctx = function
      Move(lv, e) -> Hashtbl.replace ctx lv e
    | _ -> ()
	
  method visit_stmt s = 
    ChangeDoChildrenPost(s, (fun s -> self#insert_stmt_to_ctx s; s))
      
end
  in
  List.map 
    (fun s -> 
       vis#clear_subst_cntr_ctx;
       let s' = stmt_accept vis s in 
	 simplify_stmt s' 
    ) stmts
*)
