]> granicus.if.org Git - clang/blobdiff - include/clang/Analysis/Analyses/ThreadSafetyTIL.h
Header guard canonicalization, clang part.
[clang] / include / clang / Analysis / Analyses / ThreadSafetyTIL.h
index 48d9fd386f56d0e32ebbd5bad5f7338ace1b9459..4b7b092708e1653ed819670f4b7d467fe56d10bf 100644 (file)
@@ -3,13 +3,17 @@
 //                     The LLVM Compiler Infrastructure
 //
 // This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
+// License. See LICENSE.TXT in the llvm repository for details.
 //
 //===----------------------------------------------------------------------===//
 //
-// This file defines a simple intermediate language that is used by the
-// thread safety analysis (See ThreadSafety.cpp).  The thread safety analysis
-// works by comparing mutex expressions, e.g.
+// This file defines a simple Typed Intermediate Language, or TIL, that is used
+// by the thread safety analysis (See ThreadSafety.cpp).  The TIL is intended
+// to be largely independent of clang, in the hope that the analysis can be
+// reused for other non-C++ languages.  All dependencies on clang/llvm should
+// go in ThreadSafetyUtil.h.
+//
+// Thread safety analysis works by comparing mutex expressions, e.g.
 //
 // class A { Mutex mu; int dat GUARDED_BY(this->mu); }
 // class B { A a; }
@@ -31,7 +35,7 @@
 // (3) wildcards and pattern matching over expressions
 // (4) hash-based expression lookup
 //
-// The IL is currently very experimental, is intended only for use within
+// The TIL is currently very experimental, is intended only for use within
 // the thread safety analysis, and is subject to change without notice.
 // After the API stabilizes and matures, it may be appropriate to make this
 // more generally available to other analyses.
 //
 //===----------------------------------------------------------------------===//
 
-#ifndef LLVM_CLANG_THREAD_SAFETY_TIL_H
-#define LLVM_CLANG_THREAD_SAFETY_TIL_H
+#ifndef LLVM_CLANG_ANALYSIS_ANALYSES_THREADSAFETYTIL_H
+#define LLVM_CLANG_ANALYSIS_ANALYSES_THREADSAFETYTIL_H
 
-#include "clang/AST/DeclCXX.h"
-#include "clang/AST/ExprCXX.h"
-#include "clang/AST/StmtCXX.h"
-#include "clang/AST/Type.h"
-#include "llvm/ADT/StringRef.h"
-#include "llvm/Support/AlignOf.h"
-#include "llvm/Support/Allocator.h"
+// All clang include dependencies for this file must be put in
+// ThreadSafetyUtil.h.
+#include "ThreadSafetyUtil.h"
 
+#include <stdint.h>
+#include <algorithm>
 #include <cassert>
 #include <cstddef>
+#include <utility>
+
 
 namespace clang {
 namespace threadSafety {
 namespace til {
 
 
-// Simple wrapper class to abstract away from the details of memory management.
-// SExprs are allocated in pools, and deallocated all at once.
-class MemRegionRef {
-private:
-  union AlignmentType {
-    double d;
-    void *p;
-    long double dd;
-    long long ii;
-  };
-
-public:
-  MemRegionRef() : Allocator(0) {}
-  MemRegionRef(llvm::BumpPtrAllocator *A) : Allocator(A) {}
-
-  void *allocate(size_t Sz) {
-    return Allocator->Allocate(Sz, llvm::AlignOf<AlignmentType>::Alignment);
-  }
+enum TIL_Opcode {
+#define TIL_OPCODE_DEF(X) COP_##X,
+#include "ThreadSafetyOps.def"
+#undef TIL_OPCODE_DEF
+};
 
-  template <typename T> T *allocateT() { return Allocator->Allocate<T>(); }
+enum TIL_UnaryOpcode : unsigned char {
+  UOP_Minus,        //  -
+  UOP_BitNot,       //  ~
+  UOP_LogicNot      //  !
+};
 
-  template <typename T> T *allocateT(size_t NumElems) {
-    return Allocator->Allocate<T>(NumElems);
-  }
+enum TIL_BinaryOpcode : unsigned char {
+  BOP_Mul,          //  *
+  BOP_Div,          //  /
+  BOP_Rem,          //  %
+  BOP_Add,          //  +
+  BOP_Sub,          //  -
+  BOP_Shl,          //  <<
+  BOP_Shr,          //  >>
+  BOP_BitAnd,       //  &
+  BOP_BitXor,       //  ^
+  BOP_BitOr,        //  |
+  BOP_Eq,           //  ==
+  BOP_Neq,          //  !=
+  BOP_Lt,           //  <
+  BOP_Leq,          //  <=
+  BOP_LogicAnd,     //  &&
+  BOP_LogicOr       //  ||
+};
 
-private:
-  llvm::BumpPtrAllocator *Allocator;
+enum TIL_CastOpcode : unsigned char {
+  CAST_none = 0,
+  CAST_extendNum,   // extend precision of numeric type
+  CAST_truncNum,    // truncate precision of numeric type
+  CAST_toFloat,     // convert to floating point type
+  CAST_toInt,       // convert to integer type
+  CAST_objToPtr     // convert smart pointer to pointer  (C++ only)
 };
 
+const TIL_Opcode       COP_Min  = COP_Future;
+const TIL_Opcode       COP_Max  = COP_Branch;
+const TIL_UnaryOpcode  UOP_Min  = UOP_Minus;
+const TIL_UnaryOpcode  UOP_Max  = UOP_LogicNot;
+const TIL_BinaryOpcode BOP_Min  = BOP_Mul;
+const TIL_BinaryOpcode BOP_Max  = BOP_LogicOr;
+const TIL_CastOpcode   CAST_Min = CAST_none;
+const TIL_CastOpcode   CAST_Max = CAST_toInt;
+
+StringRef getUnaryOpcodeString(TIL_UnaryOpcode Op);
+StringRef getBinaryOpcodeString(TIL_BinaryOpcode Op);
+
+
+// ValueTypes are data types that can actually be held in registers.
+// All variables and expressions must have a vBNF_Nonealue type.
+// Pointer types are further subdivided into the various heap-allocated
+// types, such as functions, records, etc.
+// Structured types that are passed by value (e.g. complex numbers)
+// require special handling; they use BT_ValueRef, and size ST_0.
+struct ValueType {
+  enum BaseType : unsigned char {
+    BT_Void = 0,
+    BT_Bool,
+    BT_Int,
+    BT_Float,
+    BT_String,    // String literals
+    BT_Pointer,
+    BT_ValueRef
+  };
 
-} // end namespace til
-} // end namespace threadSafety
-} // end namespace clang
+  enum SizeType : unsigned char {
+    ST_0 = 0,
+    ST_1,
+    ST_8,
+    ST_16,
+    ST_32,
+    ST_64,
+    ST_128
+  };
 
+  inline static SizeType getSizeType(unsigned nbytes);
 
-inline void *operator new(size_t Sz,
-                          clang::threadSafety::til::MemRegionRef &R) {
-  return R.allocate(Sz);
-}
+  template <class T>
+  inline static ValueType getValueType();
 
+  ValueType(BaseType B, SizeType Sz, bool S, unsigned char VS)
+      : Base(B), Size(Sz), Signed(S), VectSize(VS)
+  { }
 
-namespace clang {
-namespace threadSafety {
-namespace til {
+  BaseType      Base;
+  SizeType      Size;
+  bool          Signed;
+  unsigned char VectSize;  // 0 for scalar, otherwise num elements in vector
+};
 
-using llvm::StringRef;
 
-// A simple fixed size array class that does not manage its own memory,
-// suitable for use with bump pointer allocation.
-template <class T> class SimpleArray {
-public:
-  SimpleArray() : Data(0), Size(0), Capacity(0) {}
-  SimpleArray(T *Dat, size_t Cp, size_t Sz = 0)
-      : Data(Dat), Size(0), Capacity(Cp) {}
-  SimpleArray(MemRegionRef A, size_t Cp)
-      : Data(A.allocateT<T>(Cp)), Size(0), Capacity(Cp) {}
-  SimpleArray(SimpleArray<T> &A, bool Steal)
-      : Data(A.Data), Size(A.Size), Capacity(A.Capacity) {
-    A.Data = 0;
-    A.Size = 0;
-    A.Capacity = 0;
+inline ValueType::SizeType ValueType::getSizeType(unsigned nbytes) {
+  switch (nbytes) {
+    case 1: return ST_8;
+    case 2: return ST_16;
+    case 4: return ST_32;
+    case 8: return ST_64;
+    case 16: return ST_128;
+    default: return ST_0;
   }
+}
 
-  T *resize(size_t Ncp, MemRegionRef A) {
-    T *Odata = Data;
-    Data = A.allocateT<T>(Ncp);
-    memcpy(Data, Odata, sizeof(T) * Size);
-    return Odata;
-  }
 
-  typedef T *iterator;
-  typedef const T *const_iterator;
+template<>
+inline ValueType ValueType::getValueType<void>() {
+  return ValueType(BT_Void, ST_0, false, 0);
+}
+
+template<>
+inline ValueType ValueType::getValueType<bool>() {
+  return ValueType(BT_Bool, ST_1, false, 0);
+}
+
+template<>
+inline ValueType ValueType::getValueType<int8_t>() {
+  return ValueType(BT_Int, ST_8, true, 0);
+}
 
-  size_t size() const { return Size; }
-  size_t capacity() const { return Capacity; }
+template<>
+inline ValueType ValueType::getValueType<uint8_t>() {
+  return ValueType(BT_Int, ST_8, false, 0);
+}
 
-  T &operator[](unsigned I) { return Data[I]; }
-  const T &operator[](unsigned I) const { return Data[I]; }
+template<>
+inline ValueType ValueType::getValueType<int16_t>() {
+  return ValueType(BT_Int, ST_16, true, 0);
+}
 
-  iterator begin() { return Data; }
-  iterator end() { return Data + Size; }
+template<>
+inline ValueType ValueType::getValueType<uint16_t>() {
+  return ValueType(BT_Int, ST_16, false, 0);
+}
 
-  const_iterator cbegin() const { return Data; }
-  const_iterator cend() const { return Data + Size; }
+template<>
+inline ValueType ValueType::getValueType<int32_t>() {
+  return ValueType(BT_Int, ST_32, true, 0);
+}
 
-  void push_back(const T &Elem) {
-    assert(Size < Capacity);
-    Data[Size++] = Elem;
-  }
+template<>
+inline ValueType ValueType::getValueType<uint32_t>() {
+  return ValueType(BT_Int, ST_32, false, 0);
+}
 
-  template <class Iter> unsigned append(Iter I, Iter E) {
-    size_t Osz = Size;
-    size_t J = Osz;
-    for (; J < Capacity && I != E; ++J, ++I)
-      Data[J] = *I;
-    Size = J;
-    return J - Osz;
-  }
+template<>
+inline ValueType ValueType::getValueType<int64_t>() {
+  return ValueType(BT_Int, ST_64, true, 0);
+}
 
-private:
-  T *Data;
-  size_t Size;
-  size_t Capacity;
-};
+template<>
+inline ValueType ValueType::getValueType<uint64_t>() {
+  return ValueType(BT_Int, ST_64, false, 0);
+}
 
+template<>
+inline ValueType ValueType::getValueType<float>() {
+  return ValueType(BT_Float, ST_32, true, 0);
+}
 
-enum TIL_Opcode {
-#define TIL_OPCODE_DEF(X) COP_##X,
-#include "clang/Analysis/Analyses/ThreadSafetyOps.def"
-#undef TIL_OPCODE_DEF
-  COP_MAX
-};
+template<>
+inline ValueType ValueType::getValueType<double>() {
+  return ValueType(BT_Float, ST_64, true, 0);
+}
 
+template<>
+inline ValueType ValueType::getValueType<long double>() {
+  return ValueType(BT_Float, ST_128, true, 0);
+}
 
-typedef clang::BinaryOperatorKind TIL_BinaryOpcode;
-typedef clang::UnaryOperatorKind TIL_UnaryOpcode;
-typedef clang::CastKind TIL_CastOpcode;
+template<>
+inline ValueType ValueType::getValueType<StringRef>() {
+  return ValueType(BT_String, getSizeType(sizeof(StringRef)), false, 0);
+}
 
+template<>
+inline ValueType ValueType::getValueType<void*>() {
+  return ValueType(BT_Pointer, getSizeType(sizeof(void*)), false, 0);
+}
 
-enum TIL_TraversalKind {
-  TRV_Normal,
-  TRV_Lazy, // subexpression may need to be traversed lazily
-  TRV_Tail  // subexpression occurs in a tail position
-};
 
 
 // Base class for AST nodes in the typed intermediate language.
@@ -196,14 +259,24 @@ public:
   //   copy constructor: construct copy of E, with some additional arguments.
   // }
   //
-  // template <class V> typename V::R_SExpr traverse(V &Visitor) {
-  //   traverse all subexpressions, following the traversal/rewriter interface
+  // template <class V>
+  // typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+  //   traverse all subexpressions, following the traversal/rewriter interface.
   // }
   //
   // template <class C> typename C::CType compare(CType* E, C& Cmp) {
   //   compare all subexpressions, following the comparator interface
   // }
 
+  void *operator new(size_t S, MemRegionRef &R) {
+    return ::operator new(S, R);
+  }
+
+  // SExpr objects cannot be deleted.
+  // This declaration is public to workaround a gcc bug that breaks building
+  // with REQUIRES_EH=1.
+  void operator delete(void *) LLVM_DELETED_FUNCTION;
+
 protected:
   SExpr(TIL_Opcode Op) : Opcode(Op), Reserved(0), Flags(0) {}
   SExpr(const SExpr &E) : Opcode(E.Opcode), Reserved(0), Flags(E.Flags) {}
@@ -213,26 +286,144 @@ protected:
   unsigned short Flags;
 
 private:
-  SExpr();
+  SExpr() LLVM_DELETED_FUNCTION;
+
+  // SExpr objects must be created in an arena.
+  void *operator new(size_t) LLVM_DELETED_FUNCTION;
 };
 
-typedef SExpr* SExprRef;
+
+// Class for owning references to SExprs.
+// Includes attach/detach logic for counting variable references and lazy
+// rewriting strategies.
+class SExprRef {
+public:
+  SExprRef() : Ptr(nullptr) { }
+  SExprRef(std::nullptr_t P) : Ptr(nullptr) { }
+  SExprRef(SExprRef &&R) : Ptr(R.Ptr) { R.Ptr = nullptr; }
+
+  // Defined after Variable and Future, below.
+  inline SExprRef(SExpr *P);
+  inline ~SExprRef();
+
+  SExpr       *get()       { return Ptr; }
+  const SExpr *get() const { return Ptr; }
+
+  SExpr       *operator->()       { return get(); }
+  const SExpr *operator->() const { return get(); }
+
+  SExpr       &operator*()        { return *Ptr; }
+  const SExpr &operator*() const  { return *Ptr; }
+
+  bool operator==(const SExprRef &R) const { return Ptr == R.Ptr; }
+  bool operator!=(const SExprRef &R) const { return !operator==(R); }
+  bool operator==(const SExpr *P)    const { return Ptr == P; }
+  bool operator!=(const SExpr *P)    const { return !operator==(P); }
+  bool operator==(std::nullptr_t)    const { return Ptr == nullptr; }
+  bool operator!=(std::nullptr_t)    const { return Ptr != nullptr; }
+
+  inline void reset(SExpr *E);
+
+private:
+  inline void attach();
+  inline void detach();
+
+  SExpr *Ptr;
+};
 
 
 // Contains various helper functions for SExprs.
-class ThreadSafetyTIL {
+namespace ThreadSafetyTIL {
+  inline bool isTrivial(const SExpr *E) {
+    unsigned Op = E->opcode();
+    return Op == COP_Variable || Op == COP_Literal || Op == COP_LiteralPtr;
+  }
+}
+
+// Nodes which declare variables
+class Function;
+class SFunction;
+class BasicBlock;
+class Let;
+
+
+// A named variable, e.g. "x".
+//
+// There are two distinct places in which a Variable can appear in the AST.
+// A variable declaration introduces a new variable, and can occur in 3 places:
+//   Let-expressions:           (Let (x = t) u)
+//   Functions:                 (Function (x : t) u)
+//   Self-applicable functions  (SFunction (x) t)
+//
+// If a variable occurs in any other location, it is a reference to an existing
+// variable declaration -- e.g. 'x' in (x * y + z). To save space, we don't
+// allocate a separate AST node for variable references; a reference is just a
+// pointer to the original declaration.
+class Variable : public SExpr {
 public:
-  static const int MaxOpcode = COP_MAX;
+  static bool classof(const SExpr *E) { return E->opcode() == COP_Variable; }
 
-  static inline bool isTrivial(SExpr *E) {
-    unsigned Op = E->opcode();
-    return Op == COP_Variable || Op == COP_Literal;
+  // Let-variable, function parameter, or self-variable
+  enum VariableKind {
+    VK_Let,
+    VK_LetBB,
+    VK_Fun,
+    VK_SFun
+  };
+
+  // These are defined after SExprRef contructor, below
+  inline Variable(SExpr *D, const clang::ValueDecl *Cvd = nullptr);
+  inline Variable(StringRef s, SExpr *D = nullptr);
+  inline Variable(const Variable &Vd, SExpr *D);
+
+  VariableKind kind() const { return static_cast<VariableKind>(Flags); }
+
+  const StringRef name() const { return Name; }
+  const clang::ValueDecl *clangDecl() const { return Cvdecl; }
+
+  // Returns the definition (for let vars) or type (for parameter & self vars)
+  SExpr *definition() { return Definition.get(); }
+  const SExpr *definition() const { return Definition.get(); }
+
+  void attachVar() const { ++NumUses; }
+  void detachVar() const { assert(NumUses > 0); --NumUses; }
+
+  unsigned getID() const { return Id; }
+  unsigned getBlockID() const { return BlockID; }
+
+  void setName(StringRef S) { Name = S; }
+  void setID(unsigned Bid, unsigned I) {
+    BlockID = static_cast<unsigned short>(Bid);
+    Id = static_cast<unsigned short>(I);
   }
+  void setClangDecl(const clang::ValueDecl *VD) { Cvdecl = VD; }
+  void setDefinition(SExpr *E);
+  void setKind(VariableKind K) { Flags = K; }
 
-  static inline bool isLargeValue(SExpr *E) {
-    unsigned Op = E->opcode();
-    return (Op >= COP_Function && Op <= COP_Code);
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    // This routine is only called for variable references.
+    return Vs.reduceVariableRef(this);
+  }
+
+  template <class C>
+  typename C::CType compare(const Variable* E, C& Cmp) const {
+    return Cmp.compareVariableRefs(this, E);
   }
+
+private:
+  friend class Function;
+  friend class SFunction;
+  friend class BasicBlock;
+  friend class Let;
+
+  StringRef Name;                  // The name of the variable.
+  SExprRef  Definition;            // The TIL type or definition
+  const clang::ValueDecl *Cvdecl;  // The clang declaration for this variable.
+
+  unsigned short BlockID;
+  unsigned short Id;
+  mutable unsigned NumUses;
 };
 
 
@@ -248,21 +439,25 @@ public:
     FS_done
   };
 
-  Future() : SExpr(COP_Future), Status(FS_pending), Result(0), Location(0) {}
-  virtual ~Future() {}
+  Future() :
+    SExpr(COP_Future), Status(FS_pending), Result(nullptr), Location(nullptr)
+  {}
+private:
+  virtual ~Future() LLVM_DELETED_FUNCTION;
+public:
 
   // Registers the location in the AST where this future is stored.
   // Forcing the future will automatically update the AST.
-  static inline void registerLocation(SExpr **Member) {
-    if (Future *F = dyn_cast_or_null<Future>(*Member))
+  static inline void registerLocation(SExprRef *Member) {
+    if (Future *F = dyn_cast_or_null<Future>(Member->get()))
       F->Location = Member;
   }
 
   // A lazy rewriting strategy should subclass Future and override this method.
-  virtual SExpr *create() { return 0; }
+  virtual SExpr *create() { return nullptr; }
 
   // Return the result of this future if it exists, otherwise return null.
-  SExpr *maybeGetResult() {
+  SExpr *maybeGetResult() const {
     return Result;
   }
 
@@ -273,18 +468,20 @@ public:
       force();
       return Result;
     case FS_evaluating:
-      return 0; // infinite loop; illegal recursion.
+      return nullptr; // infinite loop; illegal recursion.
     case FS_done:
       return Result;
     }
   }
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
     assert(Result && "Cannot traverse Future that has not been forced.");
-    return Visitor.traverse(Result);
+    return Vs.traverse(Result, Ctx);
   }
 
-  template <class C> typename C::CType compare(Future* E, C& Cmp) {
+  template <class C>
+  typename C::CType compare(const Future* E, C& Cmp) const {
     if (!Result || !E->Result)
       return Cmp.comparePointers(this, E);
     return Cmp.compare(Result, E->Result);
@@ -292,36 +489,95 @@ public:
 
 private:
   // Force the future.
-  void force() {
-    Status = FS_evaluating;
-    SExpr *R = create();
-    Result = R;
-    if (Location) {
-      *Location = R;
-    }
-    Status = FS_done;
-  }
+  inline void force();
 
   FutureStatus Status;
   SExpr *Result;
-  SExpr **Location;
+  SExprRef *Location;
 };
 
 
+inline void SExprRef::attach() {
+  if (!Ptr)
+    return;
+
+  TIL_Opcode Op = Ptr->opcode();
+  if (Op == COP_Variable) {
+    cast<Variable>(Ptr)->attachVar();
+  } else if (Op == COP_Future) {
+    cast<Future>(Ptr)->registerLocation(this);
+  }
+}
+
+inline void SExprRef::detach() {
+  if (Ptr && Ptr->opcode() == COP_Variable) {
+    cast<Variable>(Ptr)->detachVar();
+  }
+}
+
+inline SExprRef::SExprRef(SExpr *P) : Ptr(P) {
+  attach();
+}
+
+inline SExprRef::~SExprRef() {
+  detach();
+}
+
+inline void SExprRef::reset(SExpr *P) {
+  detach();
+  Ptr = P;
+  attach();
+}
+
+
+inline Variable::Variable(StringRef s, SExpr *D)
+    : SExpr(COP_Variable), Name(s), Definition(D), Cvdecl(nullptr),
+      BlockID(0), Id(0), NumUses(0) {
+  Flags = VK_Let;
+}
+
+inline Variable::Variable(SExpr *D, const clang::ValueDecl *Cvd)
+    : SExpr(COP_Variable), Name(Cvd ? Cvd->getName() : "_x"),
+      Definition(D), Cvdecl(Cvd), BlockID(0), Id(0), NumUses(0) {
+  Flags = VK_Let;
+}
+
+inline Variable::Variable(const Variable &Vd, SExpr *D) // rewrite constructor
+    : SExpr(Vd), Name(Vd.Name), Definition(D), Cvdecl(Vd.Cvdecl),
+      BlockID(0), Id(0), NumUses(0) {
+  Flags = Vd.kind();
+}
+
+inline void Variable::setDefinition(SExpr *E) {
+  Definition.reset(E);
+}
+
+void Future::force() {
+  Status = FS_evaluating;
+  SExpr *R = create();
+  Result = R;
+  if (Location)
+    Location->reset(R);
+  Status = FS_done;
+}
+
+
 // Placeholder for C++ expressions that cannot be represented in the TIL.
 class Undefined : public SExpr {
 public:
   static bool classof(const SExpr *E) { return E->opcode() == COP_Undefined; }
 
-  Undefined(const clang::Stmt *S = 0) : SExpr(COP_Undefined), Cstmt(S) {}
+  Undefined(const clang::Stmt *S = nullptr) : SExpr(COP_Undefined), Cstmt(S) {}
   Undefined(const Undefined &U) : SExpr(U), Cstmt(U.Cstmt) {}
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
-    return Visitor.reduceUndefined(*this);
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    return Vs.reduceUndefined(*this);
   }
 
-  template <class C> typename C::CType compare(Undefined* E, C& Cmp) {
-    return Cmp.comparePointers(Cstmt, E->Cstmt);
+  template <class C>
+  typename C::CType compare(const Undefined* E, C& Cmp) const {
+    return Cmp.trueResult();
   }
 
 private:
@@ -337,150 +593,153 @@ public:
   Wildcard() : SExpr(COP_Wildcard) {}
   Wildcard(const Wildcard &W) : SExpr(W) {}
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
-    return Visitor.reduceWildcard(*this);
+  template <class V> typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    return Vs.reduceWildcard(*this);
   }
 
-  template <class C> typename C::CType compare(Wildcard* E, C& Cmp) {
+  template <class C>
+  typename C::CType compare(const Wildcard* E, C& Cmp) const {
     return Cmp.trueResult();
   }
 };
 
 
+template <class T> class LiteralT;
+
 // Base class for literal values.
 class Literal : public SExpr {
 public:
   static bool classof(const SExpr *E) { return E->opcode() == COP_Literal; }
 
-  Literal(const clang::Expr *C) : SExpr(COP_Literal), Cexpr(C) {}
-  Literal(const Literal &L) : SExpr(L), Cexpr(L.Cexpr) {}
+  Literal(const clang::Expr *C)
+     : SExpr(COP_Literal), ValType(ValueType::getValueType<void>()), Cexpr(C)
+  { }
+  Literal(ValueType VT) : SExpr(COP_Literal), ValType(VT), Cexpr(nullptr) {}
+  Literal(const Literal &L) : SExpr(L), ValType(L.ValType), Cexpr(L.Cexpr) {}
 
   // The clang expression for this literal.
-  const clang::Expr *clangExpr() { return Cexpr; }
+  const clang::Expr *clangExpr() const { return Cexpr; }
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
-    return Visitor.reduceLiteral(*this);
+  ValueType valueType() const { return ValType; }
+
+  template<class T> const LiteralT<T>& as() const {
+    return *static_cast<const LiteralT<T>*>(this);
+  }
+  template<class T> LiteralT<T>& as() {
+    return *static_cast<LiteralT<T>*>(this);
   }
 
-  template <class C> typename C::CType compare(Literal* E, C& Cmp) {
-    // TODO -- use value, not pointer equality
-    return Cmp.comparePointers(Cexpr, E->Cexpr);
+  template <class V> typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx);
+
+  template <class C>
+  typename C::CType compare(const Literal* E, C& Cmp) const {
+    // TODO: defer actual comparison to LiteralT
+    return Cmp.trueResult();
   }
 
 private:
+  const ValueType ValType;
   const clang::Expr *Cexpr;
 };
 
 
-// Literal pointer to an object allocated in memory.
-// At compile time, pointer literals are represented by symbolic names.
-class LiteralPtr : public SExpr {
+// Derived class for literal values, which stores the actual value.
+template<class T>
+class LiteralT : public Literal {
 public:
-  static bool classof(const SExpr *E) { return E->opcode() == COP_LiteralPtr; }
-
-  LiteralPtr(const clang::ValueDecl *D) : SExpr(COP_LiteralPtr), Cvdecl(D) {}
-  LiteralPtr(const LiteralPtr &R) : SExpr(R), Cvdecl(R.Cvdecl) {}
-
-  // The clang declaration for the value that this pointer points to.
-  const clang::ValueDecl *clangDecl() { return Cvdecl; }
-
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
-    return Visitor.reduceLiteralPtr(*this);
-  }
+  LiteralT(T Dat) : Literal(ValueType::getValueType<T>()), Val(Dat) { }
+  LiteralT(const LiteralT<T> &L) : Literal(L), Val(L.Val) { }
 
-  template <class C> typename C::CType compare(LiteralPtr* E, C& Cmp) {
-    return Cmp.comparePointers(Cvdecl, E->Cvdecl);
-  }
+  T  value() const { return Val;}
+  T& value() { return Val; }
 
 private:
-  const clang::ValueDecl *Cvdecl;
+  T Val;
 };
 
 
-// A named variable, e.g. "x".
-//
-// There are two distinct places in which a Variable can appear in the AST.
-// A variable declaration introduces a new variable, and can occur in 3 places:
-//   Let-expressions:           (Let (x = t) u)
-//   Functions:                 (Function (x : t) u)
-//   Self-applicable functions  (SFunction (x) t)
-//
-// If a variable occurs in any other location, it is a reference to an existing
-// variable declaration -- e.g. 'x' in (x * y + z). To save space, we don't
-// allocate a separate AST node for variable references; a reference is just a
-// pointer to the original declaration.
-class Variable : public SExpr {
-public:
-  static bool classof(const SExpr *E) { return E->opcode() == COP_Variable; }
-
-  // Let-variable, function parameter, or self-variable
-  enum VariableKind {
-    VK_Let,
-    VK_Fun,
-    VK_SFun
-  };
 
-  Variable(VariableKind K, SExpr *D = 0, const clang::ValueDecl *Cvd = 0)
-      : SExpr(COP_Variable), Definition(D), Cvdecl(Cvd),
-        BlockID(0), Id(0),  NumUses(0) {
-    Flags = K;
-    Future::registerLocation(&Definition);
+template <class V>
+typename V::R_SExpr Literal::traverse(V &Vs, typename V::R_Ctx Ctx) {
+  if (Cexpr)
+    return Vs.reduceLiteral(*this);
+
+  switch (ValType.Base) {
+  case ValueType::BT_Void:
+    break;
+  case ValueType::BT_Bool:
+    return Vs.reduceLiteralT(as<bool>());
+  case ValueType::BT_Int: {
+    switch (ValType.Size) {
+    case ValueType::ST_8:
+      if (ValType.Signed)
+        return Vs.reduceLiteralT(as<int8_t>());
+      else
+        return Vs.reduceLiteralT(as<uint8_t>());
+    case ValueType::ST_16:
+      if (ValType.Signed)
+        return Vs.reduceLiteralT(as<int16_t>());
+      else
+        return Vs.reduceLiteralT(as<uint16_t>());
+    case ValueType::ST_32:
+      if (ValType.Signed)
+        return Vs.reduceLiteralT(as<int32_t>());
+      else
+        return Vs.reduceLiteralT(as<uint32_t>());
+    case ValueType::ST_64:
+      if (ValType.Signed)
+        return Vs.reduceLiteralT(as<int64_t>());
+      else
+        return Vs.reduceLiteralT(as<uint64_t>());
+    default:
+      break;
+    }
   }
-  Variable(const clang::ValueDecl *Cvd, SExpr *D = 0)
-      : SExpr(COP_Variable), Definition(D), Cvdecl(Cvd),
-        BlockID(0), Id(0),  NumUses(0) {
-    Flags = VK_Let;
-    Future::registerLocation(&Definition);
+  case ValueType::BT_Float: {
+    switch (ValType.Size) {
+    case ValueType::ST_32:
+      return Vs.reduceLiteralT(as<float>());
+    case ValueType::ST_64:
+      return Vs.reduceLiteralT(as<double>());
+    default:
+      break;
+    }
   }
-  Variable(const Variable &Vd, SExpr *D) // rewrite constructor
-      : SExpr(Vd), Definition(D), Cvdecl(Vd.Cvdecl),
-        BlockID(0), Id(0), NumUses(0) {
-    Flags = Vd.kind();
-    Future::registerLocation(&Definition);
+  case ValueType::BT_String:
+    return Vs.reduceLiteralT(as<StringRef>());
+  case ValueType::BT_Pointer:
+    return Vs.reduceLiteralT(as<void*>());
+  case ValueType::BT_ValueRef:
+    break;
   }
+  return Vs.reduceLiteral(*this);
+}
 
-  VariableKind kind() const { return static_cast<VariableKind>(Flags); }
-
-  StringRef name() const { return Cvdecl ? Cvdecl->getName() : "_x"; }
-  const clang::ValueDecl *clangDecl() const { return Cvdecl; }
-
-  // Returns the definition (for let vars) or type (for parameter & self vars)
-  SExpr *definition() const { return Definition; }
 
-  void attachVar() const { ++NumUses; }
-  void detachVar() const { --NumUses; }
+// Literal pointer to an object allocated in memory.
+// At compile time, pointer literals are represented by symbolic names.
+class LiteralPtr : public SExpr {
+public:
+  static bool classof(const SExpr *E) { return E->opcode() == COP_LiteralPtr; }
 
-  unsigned getID() { return Id; }
-  unsigned getBlockID() { return BlockID; }
+  LiteralPtr(const clang::ValueDecl *D) : SExpr(COP_LiteralPtr), Cvdecl(D) {}
+  LiteralPtr(const LiteralPtr &R) : SExpr(R), Cvdecl(R.Cvdecl) {}
 
-  void setID(unsigned Bid, unsigned I) {
-    BlockID = static_cast<unsigned short>(Bid);
-    Id = static_cast<unsigned short>(I);
-  }
+  // The clang declaration for the value that this pointer points to.
+  const clang::ValueDecl *clangDecl() const { return Cvdecl; }
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
-    // This routine is only called for variable references.
-    return Visitor.reduceVariableRef(this);
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    return Vs.reduceLiteralPtr(*this);
   }
 
-  template <class C> typename C::CType compare(Variable* E, C& Cmp) {
-    return Cmp.compareVariableRefs(this, E);
+  template <class C>
+  typename C::CType compare(const LiteralPtr* E, C& Cmp) const {
+    return Cmp.comparePointers(Cvdecl, E->Cvdecl);
   }
 
 private:
-  friend class Function;
-  friend class SFunction;
-  friend class BasicBlock;
-
-  // Function, SFunction, and BasicBlock will reset the kind.
-  void setKind(VariableKind K) { Flags = K; }
-
-  SExpr *Definition;               // The TIL type or definition
-  const clang::ValueDecl *Cvdecl;  // The clang declaration for this variable.
-
-  unsigned short BlockID;
-  unsigned short Id;
-  mutable int NumUses;
+  const clang::ValueDecl *Cvdecl;
 };
 
 
@@ -500,33 +759,38 @@ public:
     Vd->setKind(Variable::VK_Fun);
   }
 
-  Variable *variableDecl() const { return VarDecl; }
-  SExpr *body() const { return Body; }
+  Variable *variableDecl()  { return VarDecl; }
+  const Variable *variableDecl() const { return VarDecl; }
+
+  SExpr *body() { return Body.get(); }
+  const SExpr *body() const { return Body.get(); }
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
     // This is a variable declaration, so traverse the definition.
-    typename V::R_SExpr E0 = Visitor.traverse(VarDecl->Definition, TRV_Lazy);
+    auto E0 = Vs.traverse(VarDecl->Definition, Vs.typeCtx(Ctx));
     // Tell the rewriter to enter the scope of the function.
-    Variable *Nvd = Visitor.enterScope(*VarDecl, E0);
-    typename V::R_SExpr E1 = Visitor.traverse(Body);
-    Visitor.exitScope(*VarDecl);
-    return Visitor.reduceFunction(*this, Nvd, E1);
+    Variable *Nvd = Vs.enterScope(*VarDecl, E0);
+    auto E1 = Vs.traverse(Body, Vs.declCtx(Ctx));
+    Vs.exitScope(*VarDecl);
+    return Vs.reduceFunction(*this, Nvd, E1);
   }
 
-  template <class C> typename C::CType compare(Function* E, C& Cmp) {
+  template <class C>
+  typename C::CType compare(const Function* E, C& Cmp) const {
     typename C::CType Ct =
       Cmp.compare(VarDecl->definition(), E->VarDecl->definition());
     if (Cmp.notTrue(Ct))
       return Ct;
-    Cmp.enterScope(VarDecl, E->VarDecl);
-    Ct = Cmp.compare(Body, E->Body);
+    Cmp.enterScope(variableDecl(), E->variableDecl());
+    Ct = Cmp.compare(body(), E->body());
     Cmp.leaveScope();
     return Ct;
   }
 
 private:
   Variable *VarDecl;
-  SExpr *Body;
+  SExprRef Body;
 };
 
 
@@ -539,43 +803,46 @@ public:
 
   SFunction(Variable *Vd, SExpr *B)
       : SExpr(COP_SFunction), VarDecl(Vd), Body(B) {
-    assert(Vd->Definition == 0);
+    assert(Vd->Definition == nullptr);
     Vd->setKind(Variable::VK_SFun);
-    Vd->Definition = this;
+    Vd->Definition.reset(this);
   }
   SFunction(const SFunction &F, Variable *Vd, SExpr *B) // rewrite constructor
-      : SExpr(F),
-        VarDecl(Vd),
-        Body(B) {
-    assert(Vd->Definition == 0);
+      : SExpr(F), VarDecl(Vd), Body(B) {
+    assert(Vd->Definition == nullptr);
     Vd->setKind(Variable::VK_SFun);
-    Vd->Definition = this;
+    Vd->Definition.reset(this);
   }
 
-  Variable *variableDecl() const { return VarDecl; }
-  SExpr *body() const { return Body; }
+  Variable *variableDecl() { return VarDecl; }
+  const Variable *variableDecl() const { return VarDecl; }
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
+  SExpr *body() { return Body.get(); }
+  const SExpr *body() const { return Body.get(); }
+
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
     // A self-variable points to the SFunction itself.
     // A rewrite must introduce the variable with a null definition, and update
     // it after 'this' has been rewritten.
-    Variable *Nvd = Visitor.enterScope(*VarDecl, 0 /* def */);
-    typename V::R_SExpr E1 = Visitor.traverse(Body);
-    Visitor.exitScope(*VarDecl);
+    Variable *Nvd = Vs.enterScope(*VarDecl, nullptr);
+    auto E1 = Vs.traverse(Body, Vs.declCtx(Ctx));
+    Vs.exitScope(*VarDecl);
     // A rewrite operation will call SFun constructor to set Vvd->Definition.
-    return Visitor.reduceSFunction(*this, Nvd, E1);
+    return Vs.reduceSFunction(*this, Nvd, E1);
   }
 
-  template <class C> typename C::CType compare(SFunction* E, C& Cmp) {
-    Cmp.enterScope(VarDecl, E->VarDecl);
-    typename C::CType Ct = Cmp.compare(Body, E->Body);
+  template <class C>
+  typename C::CType compare(const SFunction* E, C& Cmp) const {
+    Cmp.enterScope(variableDecl(), E->variableDecl());
+    typename C::CType Ct = Cmp.compare(body(), E->body());
     Cmp.leaveScope();
     return Ct;
   }
 
 private:
   Variable *VarDecl;
-  SExpr *Body;
+  SExprRef Body;
 };
 
 
@@ -584,103 +851,146 @@ class Code : public SExpr {
 public:
   static bool classof(const SExpr *E) { return E->opcode() == COP_Code; }
 
-  Code(SExpr *T, SExpr *B) : SExpr(COP_Code), ReturnType(T), Body(B) {
-    Future::registerLocation(&ReturnType);
-    Future::registerLocation(&Body);
-  }
+  Code(SExpr *T, SExpr *B) : SExpr(COP_Code), ReturnType(T), Body(B) {}
   Code(const Code &C, SExpr *T, SExpr *B) // rewrite constructor
-      : SExpr(C),
-        ReturnType(T),
-        Body(B) {
-    Future::registerLocation(&ReturnType);
-    Future::registerLocation(&Body);
-  }
+      : SExpr(C), ReturnType(T), Body(B) {}
+
+  SExpr *returnType() { return ReturnType.get(); }
+  const SExpr *returnType() const { return ReturnType.get(); }
 
-  SExpr *returnType() { return ReturnType; }
-  SExpr *body() { return Body; }
+  SExpr *body() { return Body.get(); }
+  const SExpr *body() const { return Body.get(); }
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
-    typename V::R_SExpr Nt = Visitor.traverse(ReturnType, TRV_Lazy);
-    typename V::R_SExpr Nb = Visitor.traverse(Body, TRV_Lazy);
-    return Visitor.reduceCode(*this, Nt, Nb);
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    auto Nt = Vs.traverse(ReturnType, Vs.typeCtx(Ctx));
+    auto Nb = Vs.traverse(Body,       Vs.lazyCtx(Ctx));
+    return Vs.reduceCode(*this, Nt, Nb);
   }
 
-  template <class C> typename C::CType compare(Code* E, C& Cmp) {
-    typename C::CType Ct = Cmp.compare(ReturnType, E->ReturnType);
+  template <class C>
+  typename C::CType compare(const Code* E, C& Cmp) const {
+    typename C::CType Ct = Cmp.compare(returnType(), E->returnType());
     if (Cmp.notTrue(Ct))
       return Ct;
-    return Cmp.compare(Body, E->Body);
+    return Cmp.compare(body(), E->body());
   }
 
 private:
-  SExpr *ReturnType;
-  SExpr *Body;
+  SExprRef ReturnType;
+  SExprRef Body;
 };
 
 
-// Apply an argument to a function
-class Apply : public SExpr {
+// A typed, writable location in memory
+class Field : public SExpr {
 public:
-  static bool classof(const SExpr *E) { return E->opcode() == COP_Apply; }
+  static bool classof(const SExpr *E) { return E->opcode() == COP_Field; }
 
-  Apply(SExpr *F, SExpr *A) : SExpr(COP_Apply), Fun(F), Arg(A) {}
-  Apply(const Apply &A, SExpr *F, SExpr *Ar)  // rewrite constructor
-      : SExpr(A), Fun(F), Arg(Ar)
-  {}
+  Field(SExpr *R, SExpr *B) : SExpr(COP_Field), Range(R), Body(B) {}
+  Field(const Field &C, SExpr *R, SExpr *B) // rewrite constructor
+      : SExpr(C), Range(R), Body(B) {}
+
+  SExpr *range() { return Range.get(); }
+  const SExpr *range() const { return Range.get(); }
 
-  SExpr *fun() const { return Fun; }
-  SExpr *arg() const { return Arg; }
+  SExpr *body() { return Body.get(); }
+  const SExpr *body() const { return Body.get(); }
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
-    typename V::R_SExpr Nf = Visitor.traverse(Fun);
-    typename V::R_SExpr Na = Visitor.traverse(Arg);
-    return Visitor.reduceApply(*this, Nf, Na);
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    auto Nr = Vs.traverse(Range, Vs.typeCtx(Ctx));
+    auto Nb = Vs.traverse(Body,  Vs.lazyCtx(Ctx));
+    return Vs.reduceField(*this, Nr, Nb);
   }
 
-  template <class C> typename C::CType compare(Apply* E, C& Cmp) {
-    typename C::CType Ct = Cmp.compare(Fun, E->Fun);
+  template <class C>
+  typename C::CType compare(const Field* E, C& Cmp) const {
+    typename C::CType Ct = Cmp.compare(range(), E->range());
     if (Cmp.notTrue(Ct))
       return Ct;
-    return Cmp.compare(Arg, E->Arg);
+    return Cmp.compare(body(), E->body());
   }
 
 private:
-  SExpr *Fun;
-  SExpr *Arg;
+  SExprRef Range;
+  SExprRef Body;
 };
 
 
-// Apply a self-argument to a self-applicable function
-class SApply : public SExpr {
+// Apply an argument to a function
+class Apply : public SExpr {
 public:
-  static bool classof(const SExpr *E) { return E->opcode() == COP_SApply; }
+  static bool classof(const SExpr *E) { return E->opcode() == COP_Apply; }
 
-  SApply(SExpr *Sf, SExpr *A = 0) : SExpr(COP_SApply), Sfun(Sf), Arg(A) {}
-  SApply(SApply &A, SExpr *Sf, SExpr *Ar = 0)  // rewrite constructor
-      : SExpr(A),  Sfun(Sf), Arg(Ar)
+  Apply(SExpr *F, SExpr *A) : SExpr(COP_Apply), Fun(F), Arg(A) {}
+  Apply(const Apply &A, SExpr *F, SExpr *Ar)  // rewrite constructor
+      : SExpr(A), Fun(F), Arg(Ar)
   {}
 
-  SExpr *sfun() const { return Sfun; }
-  SExpr *arg() const { return Arg ? Arg : Sfun; }
+  SExpr *fun() { return Fun.get(); }
+  const SExpr *fun() const { return Fun.get(); }
+
+  SExpr *arg() { return Arg.get(); }
+  const SExpr *arg() const { return Arg.get(); }
+
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    auto Nf = Vs.traverse(Fun, Vs.subExprCtx(Ctx));
+    auto Na = Vs.traverse(Arg, Vs.subExprCtx(Ctx));
+    return Vs.reduceApply(*this, Nf, Na);
+  }
+
+  template <class C>
+  typename C::CType compare(const Apply* E, C& Cmp) const {
+    typename C::CType Ct = Cmp.compare(fun(), E->fun());
+    if (Cmp.notTrue(Ct))
+      return Ct;
+    return Cmp.compare(arg(), E->arg());
+  }
+
+private:
+  SExprRef Fun;
+  SExprRef Arg;
+};
+
+
+// Apply a self-argument to a self-applicable function
+class SApply : public SExpr {
+public:
+  static bool classof(const SExpr *E) { return E->opcode() == COP_SApply; }
+
+  SApply(SExpr *Sf, SExpr *A = nullptr) : SExpr(COP_SApply), Sfun(Sf), Arg(A) {}
+  SApply(SApply &A, SExpr *Sf, SExpr *Ar = nullptr) // rewrite constructor
+      : SExpr(A), Sfun(Sf), Arg(Ar) {}
+
+  SExpr *sfun() { return Sfun.get(); }
+  const SExpr *sfun() const { return Sfun.get(); }
+
+  SExpr *arg() { return Arg.get() ? Arg.get() : Sfun.get(); }
+  const SExpr *arg() const { return Arg.get() ? Arg.get() : Sfun.get(); }
 
-  bool isDelegation() const { return Arg == 0; }
+  bool isDelegation() const { return Arg != nullptr; }
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
-    typename V::R_SExpr Nf = Visitor.traverse(Sfun);
-    typename V::R_SExpr Na = Arg ? Visitor.traverse(Arg) : 0;
-    return Visitor.reduceSApply(*this, Nf, Na);
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    auto Nf = Vs.traverse(Sfun, Vs.subExprCtx(Ctx));
+    typename V::R_SExpr Na = Arg.get() ? Vs.traverse(Arg, Vs.subExprCtx(Ctx))
+                                       : nullptr;
+    return Vs.reduceSApply(*this, Nf, Na);
   }
 
-  template <class C> typename C::CType compare(SApply* E, C& Cmp) {
-    typename C::CType Ct = Cmp.compare(Sfun, E->Sfun);
-    if (Cmp.notTrue(Ct) || (!Arg && !E->Arg))
+  template <class C>
+  typename C::CType compare(const SApply* E, C& Cmp) const {
+    typename C::CType Ct = Cmp.compare(sfun(), E->sfun());
+    if (Cmp.notTrue(Ct) || (!arg() && !E->arg()))
       return Ct;
     return Cmp.compare(arg(), E->arg());
   }
 
 private:
-  SExpr *Sfun;
-  SExpr *Arg;
+  SExprRef Sfun;
+  SExprRef Arg;
 };
 
 
@@ -689,30 +999,52 @@ class Project : public SExpr {
 public:
   static bool classof(const SExpr *E) { return E->opcode() == COP_Project; }
 
-  Project(SExpr *R, clang::ValueDecl *Cvd)
-      : SExpr(COP_Project), Rec(R), Cvdecl(Cvd) {}
-  Project(const Project &P, SExpr *R) : SExpr(P), Rec(R), Cvdecl(P.Cvdecl) {}
+  Project(SExpr *R, StringRef SName)
+      : SExpr(COP_Project), Rec(R), SlotName(SName), Cvdecl(nullptr)
+  { }
+  Project(SExpr *R, const clang::ValueDecl *Cvd)
+      : SExpr(COP_Project), Rec(R), SlotName(Cvd->getName()), Cvdecl(Cvd)
+  { }
+  Project(const Project &P, SExpr *R)
+      : SExpr(P), Rec(R), SlotName(P.SlotName), Cvdecl(P.Cvdecl)
+  { }
 
-  SExpr *record() const { return Rec; }
-  clang::ValueDecl *clangValueDecl() const { return Cvdecl; }
+  SExpr *record() { return Rec.get(); }
+  const SExpr *record() const { return Rec.get(); }
 
-  StringRef slotName() const { return Cvdecl->getName(); }
+  const clang::ValueDecl *clangDecl() const { return Cvdecl; }
+
+  bool isArrow() const { return (Flags & 0x01) != 0; }
+  void setArrow(bool b) {
+    if (b) Flags |= 0x01;
+    else Flags &= 0xFFFE;
+  }
+
+  StringRef slotName() const {
+    if (Cvdecl)
+      return Cvdecl->getName();
+    else
+      return SlotName;
+  }
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
-    typename V::R_SExpr Nr = Visitor.traverse(Rec);
-    return Visitor.reduceProject(*this, Nr);
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    auto Nr = Vs.traverse(Rec, Vs.subExprCtx(Ctx));
+    return Vs.reduceProject(*this, Nr);
   }
 
-  template <class C> typename C::CType compare(Project* E, C& Cmp) {
-    typename C::CType Ct = Cmp.compare(Rec, E->Rec);
+  template <class C>
+  typename C::CType compare(const Project* E, C& Cmp) const {
+    typename C::CType Ct = Cmp.compare(record(), E->record());
     if (Cmp.notTrue(Ct))
       return Ct;
     return Cmp.comparePointers(Cvdecl, E->Cvdecl);
   }
 
 private:
-  SExpr *Rec;
-  clang::ValueDecl *Cvdecl;
+  SExprRef Rec;
+  StringRef SlotName;
+  const clang::ValueDecl *Cvdecl;
 };
 
 
@@ -721,24 +1053,28 @@ class Call : public SExpr {
 public:
   static bool classof(const SExpr *E) { return E->opcode() == COP_Call; }
 
-  Call(SExpr *T, const clang::CallExpr *Ce = 0)
+  Call(SExpr *T, const clang::CallExpr *Ce = nullptr)
       : SExpr(COP_Call), Target(T), Cexpr(Ce) {}
   Call(const Call &C, SExpr *T) : SExpr(C), Target(T), Cexpr(C.Cexpr) {}
 
-  SExpr *target() const { return Target; }
-  const clang::CallExpr *clangCallExpr() { return Cexpr; }
+  SExpr *target() { return Target.get(); }
+  const SExpr *target() const { return Target.get(); }
+
+  const clang::CallExpr *clangCallExpr() const { return Cexpr; }
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
-    typename V::R_SExpr Nt = Visitor.traverse(Target);
-    return Visitor.reduceCall(*this, Nt);
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    auto Nt = Vs.traverse(Target, Vs.subExprCtx(Ctx));
+    return Vs.reduceCall(*this, Nt);
   }
 
-  template <class C> typename C::CType compare(Call* E, C& Cmp) {
-    return Cmp.compare(Target, E->Target);
+  template <class C>
+  typename C::CType compare(const Call* E, C& Cmp) const {
+    return Cmp.compare(target(), E->target());
   }
 
 private:
-  SExpr *Target;
+  SExprRef Target;
   const clang::CallExpr *Cexpr;
 };
 
@@ -753,30 +1089,30 @@ public:
     AK_Heap
   };
 
-  Alloc(SExpr* D, AllocKind K) : SExpr(COP_Alloc), Dtype(D) {
-    Flags = K;
-  }
-  Alloc(const Alloc &A, SExpr* Dt) : SExpr(A), Dtype(Dt) {
-    Flags = A.kind();
-  }
+  Alloc(SExpr *D, AllocKind K) : SExpr(COP_Alloc), Dtype(D) { Flags = K; }
+  Alloc(const Alloc &A, SExpr *Dt) : SExpr(A), Dtype(Dt) { Flags = A.kind(); }
 
   AllocKind kind() const { return static_cast<AllocKind>(Flags); }
-  SExpr*    dataType() const { return Dtype; }
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
-    typename V::R_SExpr Nd = Visitor.traverse(Dtype);
-    return Visitor.reduceAlloc(*this, Nd);
+  SExpr *dataType() { return Dtype.get(); }
+  const SExpr *dataType() const { return Dtype.get(); }
+
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    auto Nd = Vs.traverse(Dtype, Vs.declCtx(Ctx));
+    return Vs.reduceAlloc(*this, Nd);
   }
 
-  template <class C> typename C::CType compare(Alloc* E, C& Cmp) {
+  template <class C>
+  typename C::CType compare(const Alloc* E, C& Cmp) const {
     typename C::CType Ct = Cmp.compareIntegers(kind(), E->kind());
     if (Cmp.notTrue(Ct))
       return Ct;
-    return Cmp.compare(Dtype, E->Dtype);
+    return Cmp.compare(dataType(), E->dataType());
   }
 
 private:
-  SExpr* Dtype;
+  SExprRef Dtype;
 };
 
 
@@ -788,48 +1124,133 @@ public:
   Load(SExpr *P) : SExpr(COP_Load), Ptr(P) {}
   Load(const Load &L, SExpr *P) : SExpr(L), Ptr(P) {}
 
-  SExpr *pointer() { return Ptr; }
+  SExpr *pointer() { return Ptr.get(); }
+  const SExpr *pointer() const { return Ptr.get(); }
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
-    typename V::R_SExpr Np = Visitor.traverse(Ptr);
-    return Visitor.reduceLoad(*this, Np);
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    auto Np = Vs.traverse(Ptr, Vs.subExprCtx(Ctx));
+    return Vs.reduceLoad(*this, Np);
   }
 
-  template <class C> typename C::CType compare(Load* E, C& Cmp) {
-    return Cmp.compare(Ptr, E->Ptr);
+  template <class C>
+  typename C::CType compare(const Load* E, C& Cmp) const {
+    return Cmp.compare(pointer(), E->pointer());
   }
 
 private:
-  SExpr *Ptr;
+  SExprRef Ptr;
 };
 
 
 // Store a value to memory.
+// Source is a pointer, destination is the value to store.
 class Store : public SExpr {
 public:
   static bool classof(const SExpr *E) { return E->opcode() == COP_Store; }
 
-  Store(SExpr *P, SExpr *V) : SExpr(COP_Store), Ptr(P) {}
-  Store(const Store &S, SExpr *P, SExpr *V) : SExpr(S), Ptr(P) {}
+  Store(SExpr *P, SExpr *V) : SExpr(COP_Store), Dest(P), Source(V) {}
+  Store(const Store &S, SExpr *P, SExpr *V) : SExpr(S), Dest(P), Source(V) {}
+
+  SExpr *destination() { return Dest.get(); }  // Address to store to
+  const SExpr *destination() const { return Dest.get(); }
 
-  SExpr *pointer() const { return Ptr; }
-  SExpr *value() const { return Value; }
+  SExpr *source() { return Source.get(); }     // Value to store
+  const SExpr *source() const { return Source.get(); }
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
-    typename V::R_SExpr Np = Visitor.traverse(Ptr);
-    typename V::R_SExpr Nv = Visitor.traverse(Value);
-    return Visitor.reduceStore(*this, Np, Nv);
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    auto Np = Vs.traverse(Dest,   Vs.subExprCtx(Ctx));
+    auto Nv = Vs.traverse(Source, Vs.subExprCtx(Ctx));
+    return Vs.reduceStore(*this, Np, Nv);
   }
 
-  template <class C> typename C::CType compare(Store* E, C& Cmp) {
-    typename C::CType Ct = Cmp.compare(Ptr, E->Ptr);
+  template <class C>
+  typename C::CType compare(const Store* E, C& Cmp) const {
+    typename C::CType Ct = Cmp.compare(destination(), E->destination());
     if (Cmp.notTrue(Ct))
       return Ct;
-    return Cmp.compare(Value, E->Value);
+    return Cmp.compare(source(), E->source());
   }
 
-  SExpr *Ptr;
-  SExpr *Value;
+private:
+  SExprRef Dest;
+  SExprRef Source;
+};
+
+
+// If p is a reference to an array, then first(p) is a reference to the first
+// element.  The usual array notation p[i]  becomes first(p + i).
+class ArrayIndex : public SExpr {
+public:
+  static bool classof(const SExpr *E) { return E->opcode() == COP_ArrayIndex; }
+
+  ArrayIndex(SExpr *A, SExpr *N) : SExpr(COP_ArrayIndex), Array(A), Index(N) {}
+  ArrayIndex(const ArrayIndex &E, SExpr *A, SExpr *N)
+    : SExpr(E), Array(A), Index(N) {}
+
+  SExpr *array() { return Array.get(); }
+  const SExpr *array() const { return Array.get(); }
+
+  SExpr *index() { return Index.get(); }
+  const SExpr *index() const { return Index.get(); }
+
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    auto Na = Vs.traverse(Array, Vs.subExprCtx(Ctx));
+    auto Ni = Vs.traverse(Index, Vs.subExprCtx(Ctx));
+    return Vs.reduceArrayIndex(*this, Na, Ni);
+  }
+
+  template <class C>
+  typename C::CType compare(const ArrayIndex* E, C& Cmp) const {
+    typename C::CType Ct = Cmp.compare(array(), E->array());
+    if (Cmp.notTrue(Ct))
+      return Ct;
+    return Cmp.compare(index(), E->index());
+  }
+
+private:
+  SExprRef Array;
+  SExprRef Index;
+};
+
+
+// Pointer arithmetic, restricted to arrays only.
+// If p is a reference to an array, then p + n, where n is an integer, is
+// a reference to a subarray.
+class ArrayAdd : public SExpr {
+public:
+  static bool classof(const SExpr *E) { return E->opcode() == COP_ArrayAdd; }
+
+  ArrayAdd(SExpr *A, SExpr *N) : SExpr(COP_ArrayAdd), Array(A), Index(N) {}
+  ArrayAdd(const ArrayAdd &E, SExpr *A, SExpr *N)
+    : SExpr(E), Array(A), Index(N) {}
+
+  SExpr *array() { return Array.get(); }
+  const SExpr *array() const { return Array.get(); }
+
+  SExpr *index() { return Index.get(); }
+  const SExpr *index() const { return Index.get(); }
+
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    auto Na = Vs.traverse(Array, Vs.subExprCtx(Ctx));
+    auto Ni = Vs.traverse(Index, Vs.subExprCtx(Ctx));
+    return Vs.reduceArrayAdd(*this, Na, Ni);
+  }
+
+  template <class C>
+  typename C::CType compare(const ArrayAdd* E, C& Cmp) const {
+    typename C::CType Ct = Cmp.compare(array(), E->array());
+    if (Cmp.notTrue(Ct))
+      return Ct;
+    return Cmp.compare(index(), E->index());
+  }
+
+private:
+  SExprRef Array;
+  SExprRef Index;
 };
 
 
@@ -841,27 +1262,32 @@ public:
   UnaryOp(TIL_UnaryOpcode Op, SExpr *E) : SExpr(COP_UnaryOp), Expr0(E) {
     Flags = Op;
   }
-  UnaryOp(const UnaryOp &U, SExpr *E) : SExpr(U) { Flags = U.Flags; }
+  UnaryOp(const UnaryOp &U, SExpr *E) : SExpr(U), Expr0(E) { Flags = U.Flags; }
 
-  TIL_UnaryOpcode unaryOpcode() { return static_cast<TIL_UnaryOpcode>(Flags); }
+  TIL_UnaryOpcode unaryOpcode() const {
+    return static_cast<TIL_UnaryOpcode>(Flags);
+  }
 
-  SExpr *expr() const { return Expr0; }
+  SExpr *expr() { return Expr0.get(); }
+  const SExpr *expr() const { return Expr0.get(); }
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
-    typename V::R_SExpr Ne = Visitor.traverse(Expr0);
-    return Visitor.reduceUnaryOp(*this, Ne);
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    auto Ne = Vs.traverse(Expr0, Vs.subExprCtx(Ctx));
+    return Vs.reduceUnaryOp(*this, Ne);
   }
 
-  template <class C> typename C::CType compare(UnaryOp* E, C& Cmp) {
+  template <class C>
+  typename C::CType compare(const UnaryOp* E, C& Cmp) const {
     typename C::CType Ct =
       Cmp.compareIntegers(unaryOpcode(), E->unaryOpcode());
     if (Cmp.notTrue(Ct))
       return Ct;
-    return Cmp.compare(Expr0, E->Expr0);
+    return Cmp.compare(expr(), E->expr());
   }
 
 private:
-  SExpr *Expr0;
+  SExprRef Expr0;
 };
 
 
@@ -879,33 +1305,38 @@ public:
     Flags = B.Flags;
   }
 
-  TIL_BinaryOpcode binaryOpcode() {
+  TIL_BinaryOpcode binaryOpcode() const {
     return static_cast<TIL_BinaryOpcode>(Flags);
   }
 
-  SExpr *expr0() const { return Expr0; }
-  SExpr *expr1() const { return Expr1; }
+  SExpr *expr0() { return Expr0.get(); }
+  const SExpr *expr0() const { return Expr0.get(); }
+
+  SExpr *expr1() { return Expr1.get(); }
+  const SExpr *expr1() const { return Expr1.get(); }
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
-    typename V::R_SExpr Ne0 = Visitor.traverse(Expr0);
-    typename V::R_SExpr Ne1 = Visitor.traverse(Expr1);
-    return Visitor.reduceBinaryOp(*this, Ne0, Ne1);
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    auto Ne0 = Vs.traverse(Expr0, Vs.subExprCtx(Ctx));
+    auto Ne1 = Vs.traverse(Expr1, Vs.subExprCtx(Ctx));
+    return Vs.reduceBinaryOp(*this, Ne0, Ne1);
   }
 
-  template <class C> typename C::CType compare(BinaryOp* E, C& Cmp) {
+  template <class C>
+  typename C::CType compare(const BinaryOp* E, C& Cmp) const {
     typename C::CType Ct =
       Cmp.compareIntegers(binaryOpcode(), E->binaryOpcode());
     if (Cmp.notTrue(Ct))
       return Ct;
-    Ct = Cmp.compare(Expr0, E->Expr0);
+    Ct = Cmp.compare(expr0(), E->expr0());
     if (Cmp.notTrue(Ct))
       return Ct;
-    return Cmp.compare(Expr1, E->Expr1);
+    return Cmp.compare(expr1(), E->expr1());
   }
 
 private:
-  SExpr *Expr0;
-  SExpr *Expr1;
+  SExprRef Expr0;
+  SExprRef Expr1;
 };
 
 
@@ -917,78 +1348,81 @@ public:
   Cast(TIL_CastOpcode Op, SExpr *E) : SExpr(COP_Cast), Expr0(E) { Flags = Op; }
   Cast(const Cast &C, SExpr *E) : SExpr(C), Expr0(E) { Flags = C.Flags; }
 
-  TIL_BinaryOpcode castOpcode() { return static_cast<TIL_BinaryOpcode>(Flags); }
+  TIL_CastOpcode castOpcode() const {
+    return static_cast<TIL_CastOpcode>(Flags);
+  }
 
-  SExpr *expr() const { return Expr0; }
+  SExpr *expr() { return Expr0.get(); }
+  const SExpr *expr() const { return Expr0.get(); }
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
-    typename V::R_SExpr Ne = Visitor.traverse(Expr0);
-    return Visitor.reduceCast(*this, Ne);
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    auto Ne = Vs.traverse(Expr0, Vs.subExprCtx(Ctx));
+    return Vs.reduceCast(*this, Ne);
   }
 
-  template <class C> typename C::CType compare(Cast* E, C& Cmp) {
+  template <class C>
+  typename C::CType compare(const Cast* E, C& Cmp) const {
     typename C::CType Ct =
       Cmp.compareIntegers(castOpcode(), E->castOpcode());
     if (Cmp.notTrue(Ct))
       return Ct;
-    return Cmp.compare(Expr0, E->Expr0);
+    return Cmp.compare(expr(), E->expr());
   }
 
 private:
-  SExpr *Expr0;
+  SExprRef Expr0;
 };
 
 
+class SCFG;
 
 
-class BasicBlock;
-
-
-// An SCFG is a control-flow graph.  It consists of a set of basic blocks, each
-// of which terminates in a branch to another basic block.  There is one
-// entry point, and one exit point.
-class SCFG : public SExpr {
+class Phi : public SExpr {
 public:
-  typedef SimpleArray<BasicBlock*> BlockArray;
-
-  static bool classof(const SExpr *E) { return E->opcode() == COP_SCFG; }
+  // TODO: change to SExprRef
+  typedef SimpleArray<SExpr *> ValArray;
 
-  SCFG(MemRegionRef A, unsigned Nblocks)
-      : SExpr(COP_SCFG), Blocks(A, Nblocks), Entry(0), Exit(0) {}
-  SCFG(const SCFG &Cfg, BlockArray &Ba) // steals memory from ba
-      : SExpr(COP_SCFG),
-        Blocks(Ba, true),
-        Entry(0),
-        Exit(0) { /* TODO: set entry and exit! */
-  }
+  // In minimal SSA form, all Phi nodes are MultiVal.
+  // During conversion to SSA, incomplete Phi nodes may be introduced, which
+  // are later determined to be SingleVal, and are thus redundant.
+  enum Status {
+    PH_MultiVal = 0, // Phi node has multiple distinct values.  (Normal)
+    PH_SingleVal,    // Phi node has one distinct value, and can be eliminated
+    PH_Incomplete    // Phi node is incomplete
+  };
 
-  typedef BlockArray::iterator iterator;
-  typedef BlockArray::const_iterator const_iterator;
+  static bool classof(const SExpr *E) { return E->opcode() == COP_Phi; }
 
-  iterator begin() { return Blocks.begin(); }
-  iterator end() { return Blocks.end(); }
+  Phi() : SExpr(COP_Phi) {}
+  Phi(MemRegionRef A, unsigned Nvals) : SExpr(COP_Phi), Values(A, Nvals) {}
+  Phi(const Phi &P, ValArray &&Vs)    : SExpr(P), Values(std::move(Vs)) {}
 
-  const_iterator cbegin() const { return Blocks.cbegin(); }
-  const_iterator cend() const { return Blocks.cend(); }
+  const ValArray &values() const { return Values; }
+  ValArray &values() { return Values; }
 
-  BasicBlock *entry() const { return Entry; }
-  BasicBlock *exit() const { return Exit; }
+  Status status() const { return static_cast<Status>(Flags); }
+  void setStatus(Status s) { Flags = s; }
 
-  void add(BasicBlock *BB) { Blocks.push_back(BB); }
-  void setEntry(BasicBlock *BB) { Entry = BB; }
-  void setExit(BasicBlock *BB) { Exit = BB; }
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    typename V::template Container<typename V::R_SExpr>
+      Nvs(Vs, Values.size());
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor);
+    for (auto *Val : Values) {
+      Nvs.push_back( Vs.traverse(Val, Vs.subExprCtx(Ctx)) );
+    }
+    return Vs.reducePhi(*this, Nvs);
+  }
 
-  template <class C> typename C::CType compare(SCFG* E, C& Cmp) {
-    // TODO -- implement CFG comparisons
+  template <class C>
+  typename C::CType compare(const Phi *E, C &Cmp) const {
+    // TODO: implement CFG comparisons
     return Cmp.comparePointers(this, E);
   }
 
 private:
-  BlockArray Blocks;
-  BasicBlock *Entry;
-  BasicBlock *Exit;
+  ValArray Values;
 };
 
 
@@ -997,19 +1431,31 @@ private:
 // are "arguments" to the function, followed by a sequence of instructions.
 // Both arguments and instructions define new variables.  It ends with a
 // branch or goto to another basic block in the same SCFG.
-class BasicBlock {
+class BasicBlock : public SExpr {
 public:
-  typedef SimpleArray<Variable*> VarArray;
+  typedef SimpleArray<Variable*>   VarArray;
+  typedef SimpleArray<BasicBlock*> BlockArray;
 
-  BasicBlock(MemRegionRef A, unsigned Nargs, unsigned Nins, SExpr *Term = 0)
-      : BlockID(0), Parent(0), Args(A, Nargs), Instrs(A, Nins),
-        Terminator(Term) {}
-  BasicBlock(const BasicBlock &B, VarArray &As, VarArray &Is, SExpr *T)
-      : BlockID(0), Parent(0), Args(As, true), Instrs(Is, true), Terminator(T)
-  {}
+  static bool classof(const SExpr *E) { return E->opcode() == COP_BasicBlock; }
+
+  explicit BasicBlock(MemRegionRef A, BasicBlock* P = nullptr)
+      : SExpr(COP_BasicBlock), Arena(A), CFGPtr(nullptr), BlockID(0),
+        Parent(P), Terminator(nullptr)
+  { }
+  BasicBlock(BasicBlock &B, VarArray &&As, VarArray &&Is, SExpr *T)
+      : SExpr(COP_BasicBlock), Arena(B.Arena), CFGPtr(nullptr), BlockID(0),
+        Parent(nullptr), Args(std::move(As)), Instrs(std::move(Is)),
+        Terminator(T)
+  { }
 
   unsigned blockID() const { return BlockID; }
-  BasicBlock *parent() const { return Parent; }
+  unsigned numPredecessors() const { return Predecessors.size(); }
+
+  const SCFG* cfg() const { return CFGPtr; }
+  SCFG* cfg() { return CFGPtr; }
+
+  const BasicBlock *parent() const { return Parent; }
+  BasicBlock *parent() { return Parent; }
 
   const VarArray &arguments() const { return Args; }
   VarArray &arguments() { return Args; }
@@ -1017,100 +1463,175 @@ public:
   const VarArray &instructions() const { return Instrs; }
   VarArray &instructions() { return Instrs; }
 
-  const SExpr *terminator() const { return Terminator; }
-  SExpr *terminator() { return Terminator; }
+  const BlockArray &predecessors() const { return Predecessors; }
+  BlockArray &predecessors() { return Predecessors; }
+
+  const SExpr *terminator() const { return Terminator.get(); }
+  SExpr *terminator() { return Terminator.get(); }
+
+  void setBlockID(unsigned i)   { BlockID = i; }
+  void setParent(BasicBlock *P) { Parent = P;  }
+  void setTerminator(SExpr *E)  { Terminator.reset(E); }
 
-  void setParent(BasicBlock *P) { Parent = P; }
-  void setBlockID(unsigned i) { BlockID = i; }
-  void setTerminator(SExpr *E) { Terminator = E; }
-  void addArgument(Variable *V) { Args.push_back(V); }
-  void addInstr(Variable *V) { Args.push_back(V); }
+  // Add a new argument.  V must define a phi-node.
+  void addArgument(Variable *V) {
+    V->setKind(Variable::VK_LetBB);
+    Args.reserveCheck(1, Arena);
+    Args.push_back(V);
+  }
+  // Add a new instruction.
+  void addInstruction(Variable *V) {
+    V->setKind(Variable::VK_LetBB);
+    Instrs.reserveCheck(1, Arena);
+    Instrs.push_back(V);
+  }
+  // Add a new predecessor, and return the phi-node index for it.
+  // Will add an argument to all phi-nodes, initialized to nullptr.
+  unsigned addPredecessor(BasicBlock *Pred);
+
+  // Reserve space for Nargs arguments.
+  void reserveArguments(unsigned Nargs)   { Args.reserve(Nargs, Arena); }
+
+  // Reserve space for Nins instructions.
+  void reserveInstructions(unsigned Nins) { Instrs.reserve(Nins, Arena); }
+
+  // Reserve space for NumPreds predecessors, including space in phi nodes.
+  void reservePredecessors(unsigned NumPreds);
 
-  template <class V> BasicBlock *traverse(V &Visitor) {
-    typename V::template Container<Variable*> Nas(Visitor, Args.size());
-    typename V::template Container<Variable*> Nis(Visitor, Instrs.size());
+  // Return the index of BB, or Predecessors.size if BB is not a predecessor.
+  unsigned findPredecessorIndex(const BasicBlock *BB) const {
+    auto I = std::find(Predecessors.cbegin(), Predecessors.cend(), BB);
+    return std::distance(Predecessors.cbegin(), I);
+  }
+
+  // Set id numbers for variables.
+  void renumberVars();
+
+  template <class V>
+  typename V::R_BasicBlock traverse(V &Vs, typename V::R_Ctx Ctx) {
+    typename V::template Container<Variable*> Nas(Vs, Args.size());
+    typename V::template Container<Variable*> Nis(Vs, Instrs.size());
 
-    for (unsigned I = 0; I < Args.size(); ++I) {
-      typename V::R_SExpr Ne = Visitor.traverse(Args[I]->Definition);
-      Variable *Nvd = Visitor.enterScope(*Args[I], Ne);
+    // Entering the basic block should do any scope initialization.
+    Vs.enterBasicBlock(*this);
+
+    for (auto *A : Args) {
+      auto Ne = Vs.traverse(A->Definition, Vs.subExprCtx(Ctx));
+      Variable *Nvd = Vs.enterScope(*A, Ne);
       Nas.push_back(Nvd);
     }
-    for (unsigned J = 0; J < Instrs.size(); ++J) {
-      typename V::R_SExpr Ne = Visitor.traverse(Instrs[J]->Definition);
-      Variable *Nvd = Visitor.enterScope(*Instrs[J], Ne);
+    for (auto *I : Instrs) {
+      auto Ne = Vs.traverse(I->Definition, Vs.subExprCtx(Ctx));
+      Variable *Nvd = Vs.enterScope(*I, Ne);
       Nis.push_back(Nvd);
     }
-    typename V::R_SExpr Nt = Visitor.traverse(Terminator);
+    auto Nt = Vs.traverse(Terminator, Ctx);
 
-    for (unsigned J = 0, JN = Instrs.size(); J < JN; ++J)
-      Visitor.exitScope(*Instrs[JN-J]);
-    for (unsigned I = 0, IN = Instrs.size(); I < IN; ++I)
-      Visitor.exitScope(*Args[IN-I]);
+    // Exiting the basic block should handle any scope cleanup.
+    Vs.exitBasicBlock(*this);
 
-    return Visitor.reduceBasicBlock(*this, Nas, Nis, Nt);
+    return Vs.reduceBasicBlock(*this, Nas, Nis, Nt);
   }
 
-  template <class C> typename C::CType compare(BasicBlock* E, C& Cmp) {
-    // TODO -- implement CFG comparisons
+  template <class C>
+  typename C::CType compare(const BasicBlock *E, C &Cmp) const {
+    // TODO: implement CFG comparisons
     return Cmp.comparePointers(this, E);
   }
 
 private:
   friend class SCFG;
 
-  unsigned BlockID;
-  BasicBlock *Parent;   // The parent block is the enclosing lexical scope.
-                        // The parent dominates this block.
-  VarArray Args;        // Phi nodes
-  VarArray Instrs;
-  SExpr *Terminator;
+  MemRegionRef Arena;
+
+  SCFG       *CFGPtr;       // The CFG that contains this block.
+  unsigned   BlockID;       // unique id for this BB in the containing CFG
+  BasicBlock *Parent;       // The parent block is the enclosing lexical scope.
+                            // The parent dominates this block.
+  BlockArray Predecessors;  // Predecessor blocks in the CFG.
+  VarArray   Args;          // Phi nodes.  One argument per predecessor.
+  VarArray   Instrs;        // Instructions.
+  SExprRef   Terminator;    // Branch or Goto
 };
 
 
-template <class V>
-typename V::R_SExpr SCFG::traverse(V &Visitor) {
-  Visitor.enterCFG(*this);
-  typename V::template Container<BasicBlock *> Bbs(Visitor, Blocks.size());
-  for (unsigned I = 0; I < Blocks.size(); ++I) {
-    BasicBlock *Nbb = Blocks[I]->traverse(Visitor);
-    Bbs.push_back(Nbb);
-  }
-  Visitor.exitCFG(*this);
-  return Visitor.reduceSCFG(*this, Bbs);
-}
+// An SCFG is a control-flow graph.  It consists of a set of basic blocks, each
+// of which terminates in a branch to another basic block.  There is one
+// entry point, and one exit point.
+class SCFG : public SExpr {
+public:
+  typedef SimpleArray<BasicBlock *> BlockArray;
+  typedef BlockArray::iterator iterator;
+  typedef BlockArray::const_iterator const_iterator;
 
+  static bool classof(const SExpr *E) { return E->opcode() == COP_SCFG; }
 
+  SCFG(MemRegionRef A, unsigned Nblocks)
+    : SExpr(COP_SCFG), Arena(A), Blocks(A, Nblocks),
+      Entry(nullptr), Exit(nullptr) {
+    Entry = new (A) BasicBlock(A, nullptr);
+    Exit  = new (A) BasicBlock(A, Entry);
+    auto *V = new (A) Variable(new (A) Phi());
+    Exit->addArgument(V);
+    add(Entry);
+    add(Exit);
+  }
+  SCFG(const SCFG &Cfg, BlockArray &&Ba) // steals memory from Ba
+      : SExpr(COP_SCFG), Arena(Cfg.Arena), Blocks(std::move(Ba)),
+        Entry(nullptr), Exit(nullptr) {
+    // TODO: set entry and exit!
+  }
 
-class Phi : public SExpr {
-public:
-  typedef SimpleArray<SExpr *> ValArray;
+  iterator begin() { return Blocks.begin(); }
+  iterator end() { return Blocks.end(); }
 
-  static bool classof(const SExpr *E) { return E->opcode() == COP_Phi; }
+  const_iterator begin() const { return cbegin(); }
+  const_iterator end() const { return cend(); }
 
-  Phi(MemRegionRef A, unsigned Nvals) : SExpr(COP_Phi), Values(A, Nvals) {}
-  Phi(const Phi &P, ValArray &Vs)  // steals memory of vs
-      : SExpr(COP_Phi), Values(Vs, true) {}
+  const_iterator cbegin() const { return Blocks.cbegin(); }
+  const_iterator cend() const { return Blocks.cend(); }
 
-  const ValArray &values() const { return Values; }
-  ValArray &values() { return Values; }
+  const BasicBlock *entry() const { return Entry; }
+  BasicBlock *entry() { return Entry; }
+  const BasicBlock *exit() const { return Exit; }
+  BasicBlock *exit() { return Exit; }
+
+  inline void add(BasicBlock *BB) {
+    assert(BB->CFGPtr == nullptr || BB->CFGPtr == this);
+    BB->setBlockID(Blocks.size());
+    BB->CFGPtr = this;
+    Blocks.reserveCheck(1, Arena);
+    Blocks.push_back(BB);
+  }
+
+  void setEntry(BasicBlock *BB) { Entry = BB; }
+  void setExit(BasicBlock *BB)  { Exit = BB;  }
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
-    typename V::template Container<typename V::R_SExpr> Nvs(Visitor,
-                                                            Values.size());
-    for (ValArray::iterator I = Values.begin(), E = Values.end(); I != E; ++I) {
-      typename V::R_SExpr Nv = Visitor.traverse(*I);
-      Nvs.push_back(Nv);
+  // Set varable ids in all blocks.
+  void renumberVars();
+
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    Vs.enterCFG(*this);
+    typename V::template Container<BasicBlock *> Bbs(Vs, Blocks.size());
+    for (auto *B : Blocks) {
+      Bbs.push_back( B->traverse(Vs, Vs.subExprCtx(Ctx)) );
     }
-    return Visitor.reducePhi(*this, Nvs);
+    Vs.exitCFG(*this);
+    return Vs.reduceSCFG(*this, Bbs);
   }
 
-  template <class C> typename C::CType compare(Phi* E, C& Cmp) {
+  template <class C>
+  typename C::CType compare(const SCFG *E, C &Cmp) const {
     // TODO -- implement CFG comparisons
     return Cmp.comparePointers(this, E);
   }
 
 private:
-  ValArray Values;
+  MemRegionRef Arena;
+  BlockArray   Blocks;
+  BasicBlock   *Entry;
+  BasicBlock   *Exit;
 };
 
 
@@ -1118,21 +1639,24 @@ class Goto : public SExpr {
 public:
   static bool classof(const SExpr *E) { return E->opcode() == COP_Goto; }
 
-  Goto(BasicBlock *B, unsigned Index)
-      : SExpr(COP_Goto), TargetBlock(B) {}
-  Goto(const Goto &G, BasicBlock *B, unsigned Index)
-      : SExpr(COP_Goto), TargetBlock(B) {}
+  Goto(BasicBlock *B, unsigned I)
+      : SExpr(COP_Goto), TargetBlock(B), Index(I) {}
+  Goto(const Goto &G, BasicBlock *B, unsigned I)
+      : SExpr(COP_Goto), TargetBlock(B), Index(I) {}
+
+  const BasicBlock *targetBlock() const { return TargetBlock; }
+  BasicBlock *targetBlock() { return TargetBlock; }
 
-  BasicBlock *targetBlock() const { return TargetBlock; }
   unsigned index() const { return Index; }
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
-    // TODO -- rewrite indices properly
-    BasicBlock *Ntb = Visitor.reduceBasicBlockRef(TargetBlock);
-    return Visitor.reduceGoto(*this, Ntb, Index);
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    BasicBlock *Ntb = Vs.reduceBasicBlockRef(TargetBlock);
+    return Vs.reduceGoto(*this, Ntb);
   }
 
-  template <class C> typename C::CType compare(Goto* E, C& Cmp) {
+  template <class C>
+  typename C::CType compare(const Goto *E, C &Cmp) const {
     // TODO -- implement CFG comparisons
     return Cmp.comparePointers(this, E);
   }
@@ -1147,23 +1671,38 @@ class Branch : public SExpr {
 public:
   static bool classof(const SExpr *E) { return E->opcode() == COP_Branch; }
 
-  Branch(SExpr *C, BasicBlock *T, BasicBlock *E)
-      : SExpr(COP_Branch), Condition(C), ThenBlock(T), ElseBlock(E) {}
-  Branch(const Branch &Br, SExpr *C, BasicBlock *T, BasicBlock *E)
-      : SExpr(COP_Branch), Condition(C), ThenBlock(T), ElseBlock(E) {}
+  Branch(SExpr *C, BasicBlock *T, BasicBlock *E, unsigned TI, unsigned EI)
+      : SExpr(COP_Branch), Condition(C), ThenBlock(T), ElseBlock(E),
+        ThenIndex(TI), ElseIndex(EI)
+  {}
+  Branch(const Branch &Br, SExpr *C, BasicBlock *T, BasicBlock *E,
+         unsigned TI, unsigned EI)
+      : SExpr(COP_Branch), Condition(C), ThenBlock(T), ElseBlock(E),
+        ThenIndex(TI), ElseIndex(EI)
+  {}
 
+  const SExpr *condition() const { return Condition; }
   SExpr *condition() { return Condition; }
+
+  const BasicBlock *thenBlock() const { return ThenBlock; }
   BasicBlock *thenBlock() { return ThenBlock; }
+
+  const BasicBlock *elseBlock() const { return ElseBlock; }
   BasicBlock *elseBlock() { return ElseBlock; }
 
-  template <class V> typename V::R_SExpr traverse(V &Visitor) {
-    typename V::R_SExpr Nc = Visitor.traverse(Condition);
-    BasicBlock *Ntb = Visitor.reduceBasicBlockRef(ThenBlock);
-    BasicBlock *Nte = Visitor.reduceBasicBlockRef(ElseBlock);
-    return Visitor.reduceBranch(*this, Nc, Ntb, Nte);
+  unsigned thenIndex() const { return ThenIndex; }
+  unsigned elseIndex() const { return ElseIndex; }
+
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    auto Nc = Vs.traverse(Condition, Vs.subExprCtx(Ctx));
+    BasicBlock *Ntb = Vs.reduceBasicBlockRef(ThenBlock);
+    BasicBlock *Nte = Vs.reduceBasicBlockRef(ElseBlock);
+    return Vs.reduceBranch(*this, Nc, Ntb, Nte);
   }
 
-  template <class C> typename C::CType compare(Branch* E, C& Cmp) {
+  template <class C>
+  typename C::CType compare(const Branch *E, C &Cmp) const {
     // TODO -- implement CFG comparisons
     return Cmp.comparePointers(this, E);
   }
@@ -1172,660 +1711,141 @@ private:
   SExpr *Condition;
   BasicBlock *ThenBlock;
   BasicBlock *ElseBlock;
+  unsigned ThenIndex;
+  unsigned ElseIndex;
 };
 
 
-
-// Defines an interface used to traverse SExprs.  Traversals have been made as
-// generic as possible, and are intended to handle any kind of pass over the
-// AST, e.g. visiters, copying, non-destructive rewriting, destructive
-// (in-place) rewriting, hashing, typing, etc.
-//
-// Traversals implement the functional notion of a "fold" operation on SExprs.
-// Each SExpr class provides a traverse method, which does the following:
-//   * e->traverse(v):
-//       // compute a result r_i for each subexpression e_i
-//       for (i = 1..n)  r_i = v.traverse(e_i);
-//       // combine results into a result for e,  where X is the class of e
-//       return v.reduceX(*e, r_1, .. r_n).
-//
-// A visitor can control the traversal by overriding the following methods:
-//   * v.traverse(e):
-//       return v.traverseByCase(e), which returns v.traverseX(e)
-//   * v.traverseX(e):   (X is the class of e)
-//       return e->traverse(v).
-//   * v.reduceX(*e, r_1, .. r_n):
-//       compute a result for a node of type X
-//
-// The reduceX methods control the kind of traversal (visitor, copy, etc.).
-// These are separated into a separate class R for the purpose of code reuse.
-// The full reducer interface also has methods to handle scopes
-template <class Self, class R> class TILTraversal : public R {
-public:
-  Self *self() { return reinterpret_cast<Self *>(this); }
-
-  // Traverse an expression -- returning a result of type R_SExpr.
-  // Override this method to do something for every expression, regardless
-  // of which kind it is.  TIL_TraversalKind indicates the context in which
-  // the expression occurs, and can be:
-  //   TRV_Normal
-  //   TRV_Lazy   -- e may need to be traversed lazily, using a Future.
-  //   TRV_Tail   -- e occurs in a tail position
-  typename R::R_SExpr traverse(SExpr *E, TIL_TraversalKind K = TRV_Normal) {
-    return traverseByCase(E);
-  }
-
-  // Helper method to call traverseX(e) on the appropriate type.
-  typename R::R_SExpr traverseByCase(SExpr *E) {
-    switch (E->opcode()) {
-#define TIL_OPCODE_DEF(X)                                                   \
-    case COP_##X:                                                           \
-      return self()->traverse##X(cast<X>(E));
-#include "clang/Analysis/Analyses/ThreadSafetyOps.def"
-#undef TIL_OPCODE_DEF
-    case COP_MAX:
-      return self()->reduceNull();
-    }
-  }
-
-// Traverse e, by static dispatch on the type "X" of e.
-// Override these methods to do something for a particular kind of term.
-#define TIL_OPCODE_DEF(X)                                                   \
-  typename R::R_SExpr traverse##X(X *e) { return e->traverse(*self()); }
-#include "clang/Analysis/Analyses/ThreadSafetyOps.def"
-#undef TIL_OPCODE_DEF
-};
-
-
-// Implements a Reducer that makes a deep copy of an SExpr.
-// The default behavior of reduce##X(...) is to create a copy of the original.
-// Subclasses can override reduce##X to implement non-destructive rewriting
-// passes.
-class TILCopyReducer {
-public:
-  TILCopyReducer() {}
-
-  void setArena(MemRegionRef A) { Arena = A; }
-
-  // R_SExpr is the result type for a traversal.
-  // A copy or non-destructive rewrite returns a newly allocated term.
-  typedef SExpr *R_SExpr;
-
-  // Container is a minimal interface used to store results when traversing
-  // SExprs of variable arity, such as Phi, Goto, and SCFG.
-  template <class T> class Container {
-  public:
-    // Allocate a new container with a capacity for n elements.
-    Container(TILCopyReducer &R, unsigned N) : Elems(R.Arena, N) {}
-
-    // Push a new element onto the container.
-    void push_back(T E) { Elems.push_back(E); }
-
-  private:
-    friend class TILCopyReducer;
-    SimpleArray<T> Elems;
-  };
-
+// An identifier, e.g. 'foo' or 'x'.
+// This is a pseduo-term; it will be lowered to a variable or projection.
+class Identifier : public SExpr {
 public:
-  R_SExpr reduceNull() {
-    return 0;
-  }
-  // R_SExpr reduceFuture(...)  is never used.
-
-  R_SExpr reduceUndefined(Undefined &Orig) {
-    return new (Arena) Undefined(Orig);
-  }
-  R_SExpr reduceWildcard(Wildcard &Orig) {
-    return new (Arena) Wildcard(Orig);
-  }
-
-  R_SExpr reduceLiteral(Literal &Orig) {
-    return new (Arena) Literal(Orig);
-  }
-  R_SExpr reduceLiteralPtr(LiteralPtr &Orig) {
-    return new (Arena) LiteralPtr(Orig);
-  }
-
-  R_SExpr reduceFunction(Function &Orig, Variable *Nvd, R_SExpr E0) {
-    return new (Arena) Function(Orig, Nvd, E0);
-  }
-  R_SExpr reduceSFunction(SFunction &Orig, Variable *Nvd, R_SExpr E0) {
-    return new (Arena) SFunction(Orig, Nvd, E0);
-  }
-  R_SExpr reduceCode(Code &Orig, R_SExpr E0, R_SExpr E1) {
-    return new (Arena) Code(Orig, E0, E1);
-  }
-
-  R_SExpr reduceApply(Apply &Orig, R_SExpr E0, R_SExpr E1) {
-    return new (Arena) Apply(Orig, E0, E1);
-  }
-  R_SExpr reduceSApply(SApply &Orig, R_SExpr E0, R_SExpr E1) {
-    return new (Arena) SApply(Orig, E0, E1);
-  }
-  R_SExpr reduceProject(Project &Orig, R_SExpr E0) {
-    return new (Arena) Project(Orig, E0);
-  }
-  R_SExpr reduceCall(Call &Orig, R_SExpr E0) {
-    return new (Arena) Call(Orig, E0);
-  }
+  static bool classof(const SExpr *E) { return E->opcode() == COP_Identifier; }
 
-  R_SExpr reduceAlloc(Alloc &Orig, R_SExpr E0) {
-    return new (Arena) Alloc(Orig, E0);
-  }
-  R_SExpr reduceLoad(Load &Orig, R_SExpr E0) {
-    return new (Arena) Load(Orig, E0);
-  }
-  R_SExpr reduceStore(Store &Orig, R_SExpr E0, R_SExpr E1) {
-    return new (Arena) Store(Orig, E0, E1);
-  }
-  R_SExpr reduceUnaryOp(UnaryOp &Orig, R_SExpr E0) {
-    return new (Arena) UnaryOp(Orig);
-  }
-  R_SExpr reduceBinaryOp(BinaryOp &Orig, R_SExpr E0, R_SExpr E1) {
-    return new (Arena) BinaryOp(Orig, E0, E1);
-  }
-  R_SExpr reduceCast(Cast &Orig, R_SExpr E0) {
-    return new (Arena) Cast(Orig, E0);
-  }
+  Identifier(StringRef Id): SExpr(COP_Identifier), Name(Id) { }
+  Identifier(const Identifier& I) : SExpr(I), Name(I.Name)  { }
 
-  R_SExpr reduceSCFG(SCFG &Orig, Container<BasicBlock *> Bbs) {
-    return new (Arena) SCFG(Orig, Bbs.Elems);
-  }
-  R_SExpr reducePhi(Phi &Orig, Container<R_SExpr> As) {
-    return new (Arena) Phi(Orig, As.Elems);
-  }
-  R_SExpr reduceGoto(Goto &Orig, BasicBlock *B, unsigned Index) {
-    return new (Arena) Goto(Orig, B, Index);
-  }
-  R_SExpr reduceBranch(Branch &O, R_SExpr C, BasicBlock *B0, BasicBlock *B1) {
-    return new (Arena) Branch(O, C, B0, B1);
-  }
+  StringRef name() const { return Name; }
 
-  BasicBlock *reduceBasicBlock(BasicBlock &Orig, Container<Variable *> &As,
-                               Container<Variable *> &Is, R_SExpr T) {
-    return new (Arena) BasicBlock(Orig, As.Elems, Is.Elems, T);
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    return Vs.reduceIdentifier(*this);
   }
 
-  // Create a new variable from orig, and push it onto the lexical scope.
-  Variable *enterScope(Variable &Orig, R_SExpr E0) {
-    return new (Arena) Variable(Orig, E0);
+  template <class C>
+  typename C::CType compare(const Identifier* E, C& Cmp) const {
+    return Cmp.compareStrings(name(), E->name());
   }
-  // Exit the lexical scope of orig.
-  void exitScope(const Variable &Orig) {}
-
-  void enterCFG(SCFG &Cfg) {}
-  void exitCFG(SCFG &Cfg) {}
-
-  // Map Variable references to their rewritten definitions.
-  Variable *reduceVariableRef(Variable *Ovd) { return Ovd; }
-
-  // Map BasicBlock references to their rewritten defs.
-  BasicBlock *reduceBasicBlockRef(BasicBlock *Obb) { return Obb; }
 
 private:
-  MemRegionRef Arena;
+  StringRef Name;
 };
 
 
-class SExprCopier : public TILTraversal<SExprCopier, TILCopyReducer> {
+// An if-then-else expression.
+// This is a pseduo-term; it will be lowered to a branch in a CFG.
+class IfThenElse : public SExpr {
 public:
-  SExprCopier(MemRegionRef A) { setArena(A); }
-
-  // Create a copy of e in region a.
-  static SExpr *copy(SExpr *E, MemRegionRef A) {
-    SExprCopier Copier(A);
-    return Copier.traverse(E);
-  }
-};
-
-
-// Implements a Reducer that visits each subexpression, and returns either
-// true or false.
-class TILVisitReducer {
-public:
-  TILVisitReducer() {}
-
-  // A visitor returns a bool, representing success or failure.
-  typedef bool R_SExpr;
-
-  // A visitor "container" is a single bool, which accumulates success.
-  template <class T> class Container {
-  public:
-    Container(TILVisitReducer &R, unsigned N) : Success(true) {}
-    void push_back(bool E) { Success = Success && E; }
-
-  private:
-    friend class TILVisitReducer;
-    bool Success;
-  };
+  static bool classof(const SExpr *E) { return E->opcode() == COP_IfThenElse; }
 
-public:
-  R_SExpr reduceNull() { return true; }
-  R_SExpr reduceUndefined(Undefined &Orig) { return true; }
-  R_SExpr reduceWildcard(Wildcard &Orig) { return true; }
+  IfThenElse(SExpr *C, SExpr *T, SExpr *E)
+    : SExpr(COP_IfThenElse), Condition(C), ThenExpr(T), ElseExpr(E)
+  { }
+  IfThenElse(const IfThenElse &I, SExpr *C, SExpr *T, SExpr *E)
+    : SExpr(I), Condition(C), ThenExpr(T), ElseExpr(E)
+  { }
 
-  R_SExpr reduceLiteral(Literal &Orig) { return true; }
-  R_SExpr reduceLiteralPtr(Literal &Orig) { return true; }
+  SExpr *condition() { return Condition.get(); }   // Address to store to
+  const SExpr *condition() const { return Condition.get(); }
 
-  R_SExpr reduceFunction(Function &Orig, Variable *Nvd, R_SExpr E0) {
-    return Nvd && E0;
-  }
-  R_SExpr reduceSFunction(SFunction &Orig, Variable *Nvd, R_SExpr E0) {
-    return Nvd && E0;
-  }
-  R_SExpr reduceCode(Code &Orig, R_SExpr E0, R_SExpr E1) {
-    return E0 && E1;
-  }
-  R_SExpr reduceApply(Apply &Orig, R_SExpr E0, R_SExpr E1) {
-    return E0 && E1;
-  }
-  R_SExpr reduceSApply(SApply &Orig, R_SExpr E0, R_SExpr E1) {
-    return E0 && E1;
-  }
-  R_SExpr reduceProject(Project &Orig, R_SExpr E0) { return E0; }
-  R_SExpr reduceCall(Call &Orig, R_SExpr E0) { return E0; }
-  R_SExpr reduceAlloc(Alloc &Orig, R_SExpr E0) { return E0; }
-  R_SExpr reduceLoad(Load &Orig, R_SExpr E0) { return E0; }
-  R_SExpr reduceStore(Store &Orig, R_SExpr E0, R_SExpr E1) { return E0 && E1; }
-  R_SExpr reduceUnaryOp(UnaryOp &Orig, R_SExpr E0) { return E0; }
-  R_SExpr reduceBinaryOp(BinaryOp &Orig, R_SExpr E0, R_SExpr E1) {
-    return E0 && E1;
-  }
-  R_SExpr reduceCast(Cast &Orig, R_SExpr E0) { return E0; }
+  SExpr *thenExpr() { return ThenExpr.get(); }     // Value to store
+  const SExpr *thenExpr() const { return ThenExpr.get(); }
 
-  R_SExpr reduceSCFG(SCFG &Orig, Container<BasicBlock *> Bbs) {
-    return Bbs.Success;
-  }
-   R_SExpr reducePhi(Phi &Orig, Container<R_SExpr> As) {
-    return As.Success;
-  }
-  R_SExpr reduceGoto(Goto &Orig, BasicBlock *B, Container<R_SExpr> As) {
-    return As.Success;
-  }
-  R_SExpr reduceBranch(Branch &O, R_SExpr C, BasicBlock *B0, BasicBlock *B1) {
-    return C;
-  }
+  SExpr *elseExpr() { return ElseExpr.get(); }     // Value to store
+  const SExpr *elseExpr() const { return ElseExpr.get(); }
 
-  BasicBlock *reduceBasicBlock(BasicBlock &Orig, Container<Variable *> &As,
-                               Container<Variable *> &Is, R_SExpr T) {
-    return (As.Success && Is.Success && T) ? &Orig : 0;
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    auto Nc = Vs.traverse(Condition, Vs.subExprCtx(Ctx));
+    auto Nt = Vs.traverse(ThenExpr,  Vs.subExprCtx(Ctx));
+    auto Ne = Vs.traverse(ElseExpr,  Vs.subExprCtx(Ctx));
+    return Vs.reduceIfThenElse(*this, Nc, Nt, Ne);
   }
 
-  Variable *enterScope(Variable &Orig, R_SExpr E0) { return E0 ? &Orig : 0; }
-  void exitScope(const Variable &Orig) {}
-
-  void enterCFG(SCFG &Cfg) {}
-  void exitCFG(SCFG &Cfg) {}
-
-  Variable *reduceVariableRef(Variable *Ovd) { return Ovd; }
-
-  BasicBlock *reduceBasicBlockRef(BasicBlock *Obb) { return Obb; }
-};
-
-
-// A visitor will visit each node, and halt if any reducer returns false.
-template <class Self>
-class SExprVisitor : public TILTraversal<Self, TILVisitReducer> {
-public:
-  SExprVisitor() : Success(true) {}
-
-  bool traverse(SExpr *E, TIL_TraversalKind K = TRV_Normal) {
-    Success = Success && this->traverseByCase(E);
-    return Success;
-  }
-
-  static bool visit(SExpr *E) {
-    SExprVisitor Visitor;
-    return Visitor.traverse(E);
+  template <class C>
+  typename C::CType compare(const IfThenElse* E, C& Cmp) const {
+    typename C::CType Ct = Cmp.compare(condition(), E->condition());
+    if (Cmp.notTrue(Ct))
+      return Ct;
+    Ct = Cmp.compare(thenExpr(), E->thenExpr());
+    if (Cmp.notTrue(Ct))
+      return Ct;
+    return Cmp.compare(elseExpr(), E->elseExpr());
   }
 
 private:
-  bool Success;
-};
-
-
-// Basic class for comparison operations over expressions.
-template <typename Self>
-class TILComparator {
-public:
-  Self *self() { return reinterpret_cast<Self *>(this); }
-
-  bool compareByCase(SExpr *E1, SExpr* E2) {
-    switch (E1->opcode()) {
-#define TIL_OPCODE_DEF(X)                                                     \
-    case COP_##X:                                                             \
-      return cast<X>(E1)->compare(cast<X>(E2), *self());
-#include "clang/Analysis/Analyses/ThreadSafetyOps.def"
-#undef TIL_OPCODE_DEF
-    case COP_MAX:
-      return false;
-    }
-  }
-};
-
-
-class TILEqualsComparator : public TILComparator<TILEqualsComparator> {
-public:
-  // Result type for the comparison, e.g. bool for simple equality,
-  // or int for lexigraphic comparison (-1, 0, 1).  Must have one value which
-  // denotes "true".
-  typedef bool CType;
-
-  CType trueResult() { return true; }
-  bool notTrue(CType ct) { return !ct; }
-
-  bool compareIntegers(unsigned i, unsigned j) { return i == j; }
-  bool comparePointers(const void* P, const void* Q) { return P == Q; }
-
-  bool compare(SExpr *E1, SExpr* E2) {
-    if (E1->opcode() != E2->opcode())
-      return false;
-    return compareByCase(E1, E2);
-  }
-
-  // TODO -- handle alpha-renaming of variables
-  void enterScope(Variable* V1, Variable* V2) { }
-  void leaveScope() { }
-
-  bool compareVariableRefs(Variable* V1, Variable* V2) {
-    return V1 == V2;
-  }
-
-  static bool compareExprs(SExpr *E1, SExpr* E2) {
-    TILEqualsComparator Eq;
-    return Eq.compare(E1, E2);
-  }
+  SExprRef Condition;
+  SExprRef ThenExpr;
+  SExprRef ElseExpr;
 };
 
 
-// Pretty printer for TIL expressions
-template <typename Self, typename StreamType>
-class TILPrettyPrinter {
+// A let-expression,  e.g.  let x=t; u.
+// This is a pseduo-term; it will be lowered to instructions in a CFG.
+class Let : public SExpr {
 public:
-  static void print(SExpr *E, StreamType &SS) {
-    Self printer;
-    printer.printSExpr(E, SS, Prec_MAX);
-  }
-
-protected:
-  Self *self() { return reinterpret_cast<Self *>(this); }
-
-  void newline(StreamType &SS) {
-    SS << "\n";
-  }
-
-  // TODO: further distinguish between binary operations.
-  static const unsigned Prec_Atom = 0;
-  static const unsigned Prec_Postfix = 1;
-  static const unsigned Prec_Unary = 2;
-  static const unsigned Prec_Binary = 3;
-  static const unsigned Prec_Other = 4;
-  static const unsigned Prec_Decl = 5;
-  static const unsigned Prec_MAX = 6;
-
-  // Return the precedence of a given node, for use in pretty printing.
-  unsigned precedence(SExpr *E) {
-    switch (E->opcode()) {
-      case COP_Future:     return Prec_Atom;
-      case COP_Undefined:  return Prec_Atom;
-      case COP_Wildcard:   return Prec_Atom;
-
-      case COP_Literal:    return Prec_Atom;
-      case COP_LiteralPtr: return Prec_Atom;
-      case COP_Variable:   return Prec_Atom;
-      case COP_Function:   return Prec_Decl;
-      case COP_SFunction:  return Prec_Decl;
-      case COP_Code:       return Prec_Decl;
-
-      case COP_Apply:      return Prec_Postfix;
-      case COP_SApply:     return Prec_Postfix;
-      case COP_Project:    return Prec_Postfix;
-
-      case COP_Call:       return Prec_Postfix;
-      case COP_Alloc:      return Prec_Other;
-      case COP_Load:       return Prec_Postfix;
-      case COP_Store:      return Prec_Other;
-
-      case COP_UnaryOp:    return Prec_Unary;
-      case COP_BinaryOp:   return Prec_Binary;
-      case COP_Cast:       return Prec_Unary;
-
-      case COP_SCFG:       return Prec_Decl;
-      case COP_Phi:        return Prec_Atom;
-      case COP_Goto:       return Prec_Atom;
-      case COP_Branch:     return Prec_Atom;
-      case COP_MAX:        return Prec_MAX;
-    }
-    return Prec_MAX;
-  }
+  static bool classof(const SExpr *E) { return E->opcode() == COP_Let; }
 
-  void printSExpr(SExpr *E, StreamType &SS, unsigned P) {
-    if (!E) {
-      self()->printNull(SS);
-      return;
-    }
-    if (self()->precedence(E) > P) {
-      // Wrap expr in () if necessary.
-      SS << "(";
-      self()->printSExpr(E, SS, Prec_MAX);
-      SS << ")";
-      return;
-    }
-
-    switch (E->opcode()) {
-#define TIL_OPCODE_DEF(X)                                                  \
-    case COP_##X:                                                          \
-      self()->print##X(cast<X>(E), SS);                                    \
-      return;
-#include "clang/Analysis/Analyses/ThreadSafetyOps.def"
-#undef TIL_OPCODE_DEF
-    case COP_MAX:
-      return;
-    }
+  Let(Variable *Vd, SExpr *Bd) : SExpr(COP_Let), VarDecl(Vd), Body(Bd) {
+    Vd->setKind(Variable::VK_Let);
   }
-
-  void printNull(StreamType &SS) {
-    SS << "#null";
+  Let(const Let &L, Variable *Vd, SExpr *Bd) : SExpr(L), VarDecl(Vd), Body(Bd) {
+    Vd->setKind(Variable::VK_Let);
   }
 
-  void printFuture(Future *E, StreamType &SS) {
-    self()->printSExpr(E->maybeGetResult(), SS, Prec_Atom);
-  }
+  Variable *variableDecl()  { return VarDecl; }
+  const Variable *variableDecl() const { return VarDecl; }
 
-  void printUndefined(Undefined *E, StreamType &SS) {
-    SS << "#undefined";
-  }
-
-  void printWildcard(Wildcard *E, StreamType &SS) {
-    SS << "_";
-  }
+  SExpr *body() { return Body.get(); }
+  const SExpr *body() const { return Body.get(); }
 
-  void printLiteral(Literal *E, StreamType &SS) {
-    // TODO: actually pretty print the literal.
-    SS << "#lit";
-  }
-
-  void printLiteralPtr(LiteralPtr *E, StreamType &SS) {
-    SS << E->clangDecl()->getName();
-  }
-
-  void printVariable(Variable *E, StreamType &SS) {
-    SS << E->name() << E->getBlockID() << "_" << E->getID();
-  }
-
-  void printFunction(Function *E, StreamType &SS, unsigned sugared = 0) {
-    switch (sugared) {
-      default:
-        SS << "\\(";   // Lambda
-      case 1:
-        SS << "(";     // Slot declarations
-        break;
-      case 2:
-        SS << ", ";    // Curried functions
-        break;
-    }
-    self()->printVariable(E->variableDecl(), SS);
-    SS << ": ";
-    self()->printSExpr(E->variableDecl()->definition(), SS, Prec_MAX);
-
-    SExpr *B = E->body();
-    if (B && B->opcode() == COP_Function)
-      self()->printFunction(cast<Function>(B), SS, 2);
-    else
-      self()->printSExpr(B, SS, Prec_Decl);
-  }
-
-  void printSFunction(SFunction *E, StreamType &SS) {
-    SS << "@";
-    self()->printVariable(E->variableDecl(), SS);
-    SS << " ";
-    self()->printSExpr(E->body(), SS, Prec_Decl);
-  }
-
-  void printCode(Code *E, StreamType &SS) {
-    SS << ": ";
-    self()->printSExpr(E->returnType(), SS, Prec_Decl-1);
-    SS << " = ";
-    self()->printSExpr(E->body(), SS, Prec_Decl);
-  }
-
-  void printApply(Apply *E, StreamType &SS, bool sugared = false) {
-    SExpr *F = E->fun();
-    if (F->opcode() == COP_Apply) {
-      printApply(cast<Apply>(F), SS, true);
-      SS << ", ";
-    } else {
-      self()->printSExpr(F, SS, Prec_Postfix);
-      SS << "(";
-    }
-    self()->printSExpr(E->arg(), SS, Prec_MAX);
-    if (!sugared)
-      SS << ")$";
+  template <class V>
+  typename V::R_SExpr traverse(V &Vs, typename V::R_Ctx Ctx) {
+    // This is a variable declaration, so traverse the definition.
+    auto E0 = Vs.traverse(VarDecl->Definition, Vs.subExprCtx(Ctx));
+    // Tell the rewriter to enter the scope of the let variable.
+    Variable *Nvd = Vs.enterScope(*VarDecl, E0);
+    auto E1 = Vs.traverse(Body, Ctx);
+    Vs.exitScope(*VarDecl);
+    return Vs.reduceLet(*this, Nvd, E1);
   }
 
-  void printSApply(SApply *E, StreamType &SS) {
-    self()->printSExpr(E->sfun(), SS, Prec_Postfix);
-    SS << "@(";
-    self()->printSExpr(E->arg(), SS, Prec_MAX);
-    SS << ")";
+  template <class C>
+  typename C::CType compare(const Let* E, C& Cmp) const {
+    typename C::CType Ct =
+      Cmp.compare(VarDecl->definition(), E->VarDecl->definition());
+    if (Cmp.notTrue(Ct))
+      return Ct;
+    Cmp.enterScope(variableDecl(), E->variableDecl());
+    Ct = Cmp.compare(body(), E->body());
+    Cmp.leaveScope();
+    return Ct;
   }
 
-  void printProject(Project *E, StreamType &SS) {
-    self()->printSExpr(E->record(), SS, Prec_Postfix);
-    SS << ".";
-    SS << E->slotName();
-  }
+private:
+  Variable *VarDecl;
+  SExprRef Body;
+};
 
-  void printCall(Call *E, StreamType &SS) {
-    SExpr *T = E->target();
-    if (T->opcode() == COP_Apply) {
-      self()->printApply(cast<Apply>(T), SS, true);
-      SS << ")";
-    }
-    else {
-      self()->printSExpr(T, SS, Prec_Postfix);
-      SS << "()";
-    }
-  }
 
-  void printAlloc(Alloc *E, StreamType &SS) {
-    SS << "#alloc ";
-    self()->printSExpr(E->dataType(), SS, Prec_Other-1);
-  }
-
-  void printLoad(Load *E, StreamType &SS) {
-    self()->printSExpr(E->pointer(), SS, Prec_Postfix);
-    SS << "^";
-  }
-
-  void printStore(Store *E, StreamType &SS) {
-    self()->printSExpr(E->pointer(), SS, Prec_Other-1);
-    SS << " = ";
-    self()->printSExpr(E->value(), SS, Prec_Other-1);
-  }
-
-  void printUnaryOp(UnaryOp *E, StreamType &SS) {
-    self()->printSExpr(E->expr(), SS, Prec_Unary);
-  }
-
-  void printBinaryOp(BinaryOp *E, StreamType &SS) {
-    self()->printSExpr(E->expr0(), SS, Prec_Binary-1);
-    SS << " " << clang::BinaryOperator::getOpcodeStr(E->binaryOpcode()) << " ";
-    self()->printSExpr(E->expr1(), SS, Prec_Binary-1);
-  }
-
-  void printCast(Cast *E, StreamType &SS) {
-    SS << "~";
-    self()->printSExpr(E->expr(), SS, Prec_Unary);
-  }
-
-  void printSCFG(SCFG *E, StreamType &SS) {
-    SS << "#CFG {\n";
-    for (auto BBI : *E) {
-      SS << "BB_" << BBI->blockID() << ":";
-      newline(SS);
-      for (auto I : BBI->arguments()) {
-        SS << "let ";
-        self()->printVariable(I, SS);
-        SS << " = ";
-        self()->printSExpr(I->definition(), SS, Prec_MAX);
-        SS << ";";
-        newline(SS);
-      }
-      for (auto I : BBI->instructions()) {
-        SS << "let ";
-        self()->printVariable(I, SS);
-        SS << " = ";
-        self()->printSExpr(I->definition(), SS, Prec_MAX);
-        SS << ";";
-        newline(SS);
-      }
-      SExpr *T = BBI->terminator();
-      if (T) {
-        self()->printSExpr(T, SS, Prec_MAX);
-        SS << ";";
-        newline(SS);
-      }
-      newline(SS);
-    }
-    SS << "}";
-    newline(SS);
-  }
-
-  void printPhi(Phi *E, StreamType &SS) {
-    SS << "#phi(";
-    unsigned i = 0;
-    for (auto V : E->values()) {
-      ++i;
-      if (i > 0)
-        SS << ", ";
-      self()->printSExpr(V, SS, Prec_MAX);
-    }
-    SS << ")";
-  }
 
-  void printGoto(Goto *E, StreamType &SS) {
-    SS << "#goto BB_";
-    SS << E->targetBlock()->blockID();
-    SS << ":";
-    SS << E->index();
-  }
+const SExpr *getCanonicalVal(const SExpr *E);
+SExpr* simplifyToCanonicalVal(SExpr *E);
+void simplifyIncompleteArg(Variable *V, til::Phi *Ph);
 
-  void printBranch(Branch *E, StreamType &SS) {
-    SS << "#branch (";
-    self()->printSExpr(E->condition(), SS, Prec_MAX);
-    SS << ") BB_";
-    SS << E->thenBlock()->blockID();
-    SS << " BB_";
-    SS << E->elseBlock()->blockID();
-  }
-};
 
 } // end namespace til
-
-
-
 } // end namespace threadSafety
 } // end namespace clang
 
-#endif // THREAD_SAFETY_TIL_H
+#endif