papers/lux-symbolic-execution-halmos/sections/01-what-is-symbolic-execution.tex

\section{What Is Symbolic Execution}


\subsection{Concrete vs.\ Symbolic}

In concrete execution, a function \texttt{f(x)} runs with a specific value of \texttt{x}
(say, \texttt{x = 42}). One execution, one path, one result. Testing is concrete
execution: you provide inputs and check outputs.

In symbolic execution, \texttt{x} is a \emph{symbol}---a variable that represents all
possible values simultaneously. The executor tracks a \emph{path constraint}: a logical
formula describing which values of \texttt{x} lead to the current execution path.

Consider:

\begin{lstlisting}[language=Solidity,caption={A simple function with two paths}]
function abs(int256 x) public pure returns (int256) {
    if (x >= 0) {
        return x;
    } else {
        return -x;
    }
}
\end{lstlisting}

Symbolic execution explores both branches:
\begin{enumerate}[nosep]
  \item Path 1: constraint $x \geq 0$, result $= x$.
  \item Path 2: constraint $x < 0$, result $= -x$.
\end{enumerate}

To check the property ``\texttt{abs(x) >= 0} for all \texttt{x}'', the symbolic executor
asks an SMT solver: is there a value of $x$ satisfying path~2's constraint ($x < 0$)
where $-x < 0$? For \texttt{int256}, yes: $x = -2^{255}$ (the minimum value) because
$-(-2^{255})$ overflows. The symbolic executor returns this as a concrete counterexample.

\subsection{The Three Components}

A symbolic executor has three components:

\begin{enumerate}
  \item \textbf{Symbolic interpreter}: Executes the program with symbolic values, forking
    at each branch.
  \item \textbf{Path constraint collector}: Accumulates constraints along each path.
  \item \textbf{SMT solver}: Decides satisfiability of path constraints (typically Z3 or
    CVC5).
\end{enumerate}

\subsection{Why It Works for Smart Contracts}

Smart contracts are ideal targets for symbolic execution:

\begin{itemize}[nosep]
  \item \textbf{Bounded}: No dynamic memory allocation, no unbounded recursion, finite
    storage.
  \item \textbf{Deterministic}: Same inputs always produce same outputs (no filesystem,
    no network).
  \item \textbf{Small}: Most contracts are hundreds of lines, not millions.
  \item \textbf{High stakes}: A single bug can lose millions of dollars. The cost of
    verification is justified.
\end{itemize}

%% ============================================================