Introduce the aux data field to Symbolic Value (#50)

This is determined statically in the type of the symbolic value,
allowing us to encode additional information in the values for different
stages of the analyzer.

In particular, it is designed to ensure that during execution we use
semantic equality for values, while during type checking we use
identity equality for values, where that identity equality is based on
the associated type variable.

This means that our type checker will no longer equate values that are
structurally equal but semantically different for typing purposes, and
hopefully give us more accurate results.

asset/UniswapDebug.sol

@@ -0,0 +1,117 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity =0.6.12;
+
+library Math {
+    function min(uint x, uint y) internal pure returns (uint z) {
+        z = x < y ? x : y;
+    }
+
+    function sqrt(uint y) internal pure returns (uint z) {
+        if (y > 3) {
+            z = y;
+            uint x = y / 2 + 1;
+            while (x < z) {
+                z = x;
+                x = (y / x + x) / 2;
+            }
+        } else if (y != 0) {
+            z = 1;
+        }
+    }
+}
+
+library SafeMathUniswap {
+    function add(uint x, uint y) internal pure returns (uint z) {
+        require((z = x + y) >= x, 'ds-math-add-overflow');
+    }
+
+    function sub(uint x, uint y) internal pure returns (uint z) {
+        require((z = x - y) <= x, 'ds-math-sub-underflow');
+    }
+
+    function mul(uint x, uint y) internal pure returns (uint z) {
+        require(y == 0 || (z = x * y) / y == x, 'ds-math-mul-overflow');
+    }
+}
+
+contract UniswapV2ERC20 {
+    using SafeMathUniswap for uint;
+
+    uint  public totalSupply;
+    mapping(address => uint) public balanceOf;
+    mapping(address => mapping(address => uint)) public allowance;
+
+    bytes32 public DOMAIN_SEPARATOR;
+    // keccak256("Permit(address owner,address spender,uint256 value,uint256 nonce,uint256 deadline)");
+    bytes32 public constant PERMIT_TYPEHASH = 0x6e71edae12b1b97f4d1f60370fef10105fa2faae0126114a169c64845d6126c9;
+    mapping(address => uint) public nonces;
+
+    function _mint(address to, uint value) internal {
+        totalSupply = totalSupply.add(value);
+        balanceOf[to] = balanceOf[to].add(value);
+    }
+
+    function _burn(address from, uint value) internal {
+        balanceOf[from] = balanceOf[from].sub(value);
+        totalSupply = totalSupply.sub(value);
+    }
+
+    function _approve(address owner, address spender, uint value) private {
+        allowance[owner][spender] = value;
+    }
+
+    function _transfer(address from, address to, uint value) private {
+        balanceOf[from] = balanceOf[from].sub(value);
+        balanceOf[to] = balanceOf[to].add(value);
+    }
+
+    function approve(address spender, uint value) external returns (bool) {
+        _approve(msg.sender, spender, value);
+        return true;
+    }
+
+    function transfer(address to, uint value) external returns (bool) {
+        _transfer(msg.sender, to, value);
+        return true;
+    }
+
+    function transferFrom(address from, address to, uint value) external returns (bool) {
+        if (allowance[from][msg.sender] != uint(-1)) {
+            allowance[from][msg.sender] = allowance[from][msg.sender].sub(value);
+        }
+        _transfer(from, to, value);
+        return true;
+    }
+
+    function permit(address owner, address spender, uint value, uint deadline, uint8 v, bytes32 r, bytes32 s) external {
+        address recoveredAddress = ecrecover(0, v, r, s);
+        _approve(owner, spender, value);
+    }
+}
+
+interface IMigrator {
+    // Return the desired amount of liquidity token that the migrator wants.
+    function desiredLiquidity() external view returns (uint256);
+}
+
+contract UniswapDebug is UniswapV2ERC20 {
+    uint public constant MINIMUM_LIQUIDITY = 10**3;
+
+    // this low-level function should be called from a contract which performs important safety checks
+    function mint(address to) external returns (uint liquidity) {
+        (uint112 _reserve0, uint112 _reserve1,) = (0, 1, 2); // gas savings
+        uint balance0 = uint(address(this));
+        uint balance1 = uint(address(this));
+        uint amount0 = balance0.sub(_reserve0);
+        uint amount1 = balance1.sub(_reserve1);
+
+        _mint(to, liquidity);
+    }
+
+    // this low-level function should be called from a contract which performs important safety checks
+    function burn(address to) external returns (uint amount0, uint amount1) {
+        uint liquidity = balanceOf[address(this)];
+        _burn(address(this), liquidity);
+    }
+}

src/error/unification.rs

@@ -9,15 +9,15 @@ use crate::{
         expression::{InferenceSet, TypeExpression},
         state::TypeVariable,
     },
-    vm::value::BoxedVal,
+    vm::value::TCBoxedVal,
 };
 
 /// Errors that occur during unification and type inference process in the
 /// [`crate::inference::InferenceEngine`].
 #[derive(Clone, Debug, Eq, Error, PartialEq)]
 pub enum Error {
     #[error("Invalid tree {value:?} encountered during unification: {reason}")]
-    InvalidTree { value: BoxedVal, reason: String },
+    InvalidTree { value: TCBoxedVal, reason: String },
 
     #[error("Invalid typing expression {value:?} encountered during unification: {reason}")]
     InvalidInference { value: TypeExpression, reason: String },

src/inference/debug.rs

@@ -0,0 +1,84 @@
+//! This module contains utilities for debugging the state of the type checker.
+
+use std::collections::HashSet;
+
+use crate::inference::{
+    expression::TE,
+    state::{InferenceState, TypeVariable},
+};
+
+/// Debug prints the inference tree for each variable in the `state`.
+///
+/// It also prints the associated value for each type variable when it
+/// encounters them.
+///
+/// # Recursion and Cycles
+///
+/// Note that this is recursive, but will not follow cycles in inferences.
+pub fn print_state(state: &InferenceState) {
+    for ty in state.variables() {
+        print_tv(ty, state);
+    }
+}
+
+/// Debug prints the inference tree for an individual type variable in the
+/// inference state.
+///
+/// It also prints the associated value for each type variable when it
+/// encounters them.
+///
+/// # Recursion and Cycles
+///
+/// Note that this is recursive, but will not follow cycles in inferences.
+pub fn print_tv(ty: TypeVariable, state: &InferenceState) {
+    print_tv_impl(ty, state, 0, &mut HashSet::new());
+}
+
+/// The implementation of the debug printer for an individual type
+/// variable's inference tree in the inference state.
+///
+/// It exists to provide a nicer interface on the output.
+fn print_tv_impl(
+    ty: TypeVariable,
+    state: &InferenceState,
+    indent: usize,
+    seen: &mut HashSet<TypeVariable>,
+) {
+    let this_indent = " ".repeat(indent);
+    let half_indent_level = indent + 2;
+    let half_indent = " ".repeat(half_indent_level);
+    let next_indent_level = indent + 4;
+    let value = state.value_unchecked(ty);
+    println!("{this_indent}↳ {value}");
+    println!("{half_indent}: {ty}");
+    for inf in state.inferences(ty) {
+        seen.insert(ty);
+        println!("{half_indent}= {inf}");
+        match inf {
+            TE::Equal { id } => {
+                if !seen.contains(id) {
+                    print_tv_impl(*id, state, next_indent_level, seen);
+                }
+            }
+            TE::Mapping { key, value } => {
+                if !seen.contains(key) {
+                    print_tv_impl(*key, state, next_indent_level, seen);
+                }
+                if !seen.contains(value) {
+                    print_tv_impl(*value, state, next_indent_level, seen);
+                }
+            }
+            TE::FixedArray { element, .. } | TE::DynamicArray { element } => {
+                if !seen.contains(element) {
+                    print_tv_impl(*element, state, next_indent_level, seen);
+                }
+            }
+            TE::Packed { types, .. } => types.iter().for_each(|span| {
+                if !seen.contains(&span.typ) {
+                    print_tv_impl(span.typ, state, next_indent_level, seen);
+                }
+            }),
+            _ => (),
+        }
+    }
+}

src/inference/expression.rs

@@ -4,7 +4,10 @@
 //! It is intentionally kept separate from the [`crate::inference::state`] to
 //! ensure that you cannot create new type variables for it.
 
-use std::collections::HashSet;
+use std::{
+    collections::HashSet,
+    fmt::{Display, Formatter},
+};
 
 use ethnum::U256;
 use itertools::Itertools;
@@ -213,6 +216,49 @@ impl TypeExpression {
     }
 }
 
+impl Display for TypeExpression {
+    /// A pretty printer for typing expressions.
+    ///
+    /// For full details, please use the debug implementation instead. This is
+    /// meant for higher-level observation and reasoning, and as such does not
+    /// print full type variable identifiers, or the details of conflicted
+    /// types.
+    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+        match self {
+            Self::Any => write!(f, "Any"),
+            Self::Equal { id } => write!(f, "Eq<{id}>"),
+            Self::Word { width, usage } => {
+                if let Some(width) = width {
+                    write!(f, "Word<{usage}, {width}>")
+                } else {
+                    write!(f, "Word<{usage}, ???>")
+                }
+            }
+            Self::FixedArray { element, length } => write!(f, "Array<{element}>[{length}]"),
+            Self::Mapping { key, value } => write!(f, "Mapping<{key}, {value}>"),
+            Self::DynamicArray { element } => write!(f, "Array<{element}>"),
+            Self::Packed { types, is_struct } => {
+                if *is_struct {
+                    write!(f, "Struct(")?;
+                } else {
+                    write!(f, "Packed(")?;
+                }
+
+                for (i, typ) in types.iter().enumerate() {
+                    write!(f, "{typ}")?;
+
+                    if i + 1 != types.len() {
+                        write!(f, ", ")?;
+                    }
+                }
+
+                write!(f, ")")
+            }
+            Self::Conflict { .. } => write!(f, "Conflicted"),
+        }
+    }
+}
+
 /// A set of typing judgements.
 pub type InferenceSet = HashSet<TypeExpression>;
 
@@ -298,6 +344,22 @@ impl Default for WordUse {
     }
 }
 
+impl Display for WordUse {
+    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+        let str = match self {
+            Self::Address => "address",
+            Self::Bool => "bool",
+            Self::Function => "function",
+            Self::Bytes => "bytes",
+            Self::Selector => "selector",
+            Self::Numeric => "number",
+            Self::UnsignedNumeric => "unsigned",
+            Self::SignedNumeric => "signed",
+        };
+        write!(f, "{str}")
+    }
+}
+
 /// A representation of a type being at a specific position _inside_ an EVM
 /// word.
 ///
@@ -383,6 +445,12 @@ impl Span {
     }
 }
 
+impl Display for Span {
+    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+        write!(f, "span({}, {}, {})", self.offset, self.size, self.typ)
+    }
+}
+
 impl From<&Span> for Span {
     fn from(value: &Span) -> Self {
         *value