10 Symbolic Execution.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "6c50f412",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "# (Dynamic) Symbolic Execution"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e653c102",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "This chapter is an exerpt of Andreas Zeller's excellent [Fuzzing Book](https://www.fuzzingbook.org/html/ConcolicFuzzer.html), cutting some corners."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "b258985d",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "outputs": [],
   "source": [
    "def factorial(n):\n",
    "    if n < 0:\n",
    "        return None\n",
    "\n",
    "    if n == 0:\n",
    "        return 1\n",
    "\n",
    "    if n == 1:\n",
    "        return 1\n",
    "\n",
    "    v = 1\n",
    "    while n != 0:\n",
    "        v = v * n\n",
    "        n = n - 1\n",
    "\n",
    "    return v"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "de760402",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "factorial(5)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6f29d542",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "## SMT Solver"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "92bbac90",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "Dynamic Symbolic Execution uses modern contraint solving techniques to derive input values, in particular it is usually built using Satisfiability Modulo Theories (SMT) solvers. These are built on top of regular SAT solvers, which determine whether first order logic formulas are satisfiable. SMT solvers extend these with additional background theories, such as the theory of integers."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d7b3ea0e",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "One of the best SMT solvers available is (https://github.com/Z3Prover/z3)[https://github.com/Z3Prover/z3]."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "6f449cc5",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "outputs": [],
   "source": [
    "import z3"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "721e8747",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "z3.set_option('timeout', 30 * 1000)  # milliseconds"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c19b7b5f",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "Constraints are formulas using symbolic variables. For example, to create a symbolc variable representing integer `n`, we can use the Z3-API as follows."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "55fabb14",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "zn = z3.Int('n')"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "757f980f",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "Symbolic variables can be used to construct constraints."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "7daa25da",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "zn < 0"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "008a336f",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "z3.Not(zn < 0)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a4b87429",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "A constraint is solved by finding an assignment of values to the symbolic variables such that the formula is satisfied."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "afc7e148",
   "metadata": {
    "scrolled": false,
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "z3.solve(z3.Not(zn < 0))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "98853364",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "z3.solve(zn < 0)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bc41b5ed",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "## A Concolic Tracer"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "464784fe",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "DSE, or concolic execution (concolic = concrete+symbolic), consists of collecting symbolic path conditions during concrete executions. This means that during execution we need to track (1) the symbolic context, consisting of the symbolic variables and their symbolic values, and (2) the path conditions that describe the control flow decisions made along an execution."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "51fb364b",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "Let us now define a class to collect symbolic variables and path conditions during an execution. The idea is to have a ConcolicTracer class that is invoked in a with block. To execute a function while tracing its path conditions, we need to transform its arguments, which we do by invoking functions through a [] item access."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "464d65f6",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "source": [
    "This is a typical usage of a ConcolicTracer:\n",
    "```\n",
    "with ConcolicTracer as _:\n",
    "    _.[function](args, ...)\n",
    "```\n",
    "\n",
    "After execution, we can access the symbolic variables in the decls attribute:\n",
    "```\n",
    "_.decls\n",
    "```\n",
    "\n",
    "whereas the path attribute lists the precondition paths encountered:\n",
    "```\n",
    "_.path\n",
    "```\n",
    "\n",
    "The context attribute contains a pair of declarations and paths:\n",
    "```\n",
    "_.context\n",
    "```"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "f1bb8c89",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "outputs": [],
   "source": [
    "import inspect"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b25d16f0",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "Let us now implement ConcolicTracer constructor of a accepts a single context argument which contains the declarations for the symbolic variables seen so far, and path conditions seen so far. We only need this in case of nested contexts."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "9d45a2db",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "class ConcolicTracer:\n",
    "    \"\"\"Trace function execution, tracking variables and path conditions\"\"\"\n",
    "\n",
    "    def __init__(self, context=None):\n",
    "        \"\"\"Constructor.\"\"\"\n",
    "        self.context = context if context is not None else ({}, [])\n",
    "        self.decls, self.path = self.context"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "985285ad",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "We add the enter and exit methods for the with block."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "b140aed9",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "class ConcolicTracer(ConcolicTracer):\n",
    "    def __enter__(self):\n",
    "        return self\n",
    "\n",
    "    def __exit__(self, exc_type, exc_value, tb):\n",
    "        return"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "56491099",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "We use introspection to determine the arguments to the function, which is hooked into the getitem() method."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "226b441f",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "class ConcolicTracer(ConcolicTracer):\n",
    "    def __getitem__(self, fn):\n",
    "        self.fn = fn\n",
    "        self.fn_args = {i: None for i in inspect.signature(fn).parameters}\n",
    "        return self"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "84b7730a",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "Finally, the function itself is invoked using the call method."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "a9e30b19",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "outputs": [],
   "source": [
    "class ConcolicTracer(ConcolicTracer):\n",
    "    def __call__(self, *args):\n",
    "        self.result = self.fn(*self.concolic(args))\n",
    "        return self.result"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "65171cdd",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "For now, we define concolic() as a transparent function. It will be modified to produce symbolic variables later."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "22fd3801",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "class ConcolicTracer(ConcolicTracer):\n",
    "    def concolic(self, args):\n",
    "        return args"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e2f5465a",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "We now have things in place for tracing functions:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "a880ff90",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "outputs": [],
   "source": [
    "with ConcolicTracer() as _:\n",
    "    _[factorial](1)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ee735275",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "And for retrieving results (but not actually computing them):"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "2e324824",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "_.decls"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "bceebd19",
   "metadata": {
    "scrolled": true,
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "_.path"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "974b9c52",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "Both decls and path attributes will be set by concolic proxy objects, which we define next."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "edf9714a",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "## Concolic Proxy Objects"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "dae39932",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "We now define the concolic proxy objects that can be used for concolic tracing. First, we define the `zproxy_create()` method that given a class name, correctly creates an instance of that class, and the symbolic corresponding variable, and registers the symbolic variable in the context information context."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "c1ed1c51",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "def zproxy_create(cls, z_type, z3var, context, z_name, v=None):\n",
    "    z_value = cls(context, z3var(z_name), v)\n",
    "    context[0][z_name] = z_type  # add to decls\n",
    "    return z_value"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2810af33",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### A Proxy Class for Booleans"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d7eed001",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "First, we define the zbool class which is used to track the predicates encountered. It is a wrapper class that contains both symbolic (z) as well as concrete (v) values. The concrete value is used to determine which path to take, and the symbolic value is used to collect the predicates encountered."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "11956342",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "The initialization is done in two parts. The first one is using `zproxy_create()` to correctly initialize and register the shadow symbolic variable corresponding to the passed argument. This is used exclusively when the symbolic variable needs to be initialized first. In all other cases, the constructor is called with the preexisting symbolic value."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "cbf991e3",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "class zbool:\n",
    "    @classmethod\n",
    "    def create(cls, context, z_name, v):\n",
    "        return zproxy_create(cls, 'Bool', z3.Bool, context, z_name, v)\n",
    "\n",
    "    def __init__(self, context, z, v=None):\n",
    "        self.context = context\n",
    "        self.z = z\n",
    "        self.v = v\n",
    "        self.decl, self.path = self.context"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "cd79203a",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "Here is how it is used. We create a symbolic variable my_bool_arg with a value of True in the current context of the concolic tracer:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "8ed02d46",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "with ConcolicTracer() as _:\n",
    "    val = zbool.create(_.context, 'my_bool_arg', True)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d3988711",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "We can now access the symbolic name in the z attribute:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "5e54fa16",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "val.z"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "76069169",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "The value is in the v attribute:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "5d197382",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "val.v"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "679e94a0",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "Note that the context of the enclosing `ConcolicTracer()` is automatically updated (via `zproxy_create()`) to hold the variable declarations and types:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "6a1cec00",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "_.context"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "29cb400a",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "The context can also be reached through the context attribute; both point to the same data structure."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "75a6e104",
   "metadata": {
    "scrolled": false,
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "outputs": [],
   "source": [
    "val.context"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "28fd5a41",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### Negation of Encoded formula"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "20846539",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "The zbool class allows negation of its concrete and symbolic values."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "a36ee095",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "class zbool(zbool):\n",
    "    def __not__(self):\n",
    "        return zbool(self.context, z3.Not(self.z), not self.v)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "fba70f42",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "Here is how it can be used."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "f1f3a760",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "with ConcolicTracer() as _:\n",
    "    val = zbool.create(_.context, 'my_bool_arg', True).__not__()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "fedcd9e4",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "val.z"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "b5ad8caf",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "val.v"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "4a593451",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "_.context"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "180f31e3",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### Registering Predicates on Conditionals"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "594b9787",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "The `zbool` class is being used to track Boolean conditions that arise during program execution. It tracks such conditions by registering the corresponding symbolic expressions in the context as soon as it is evaluated. On evaluation, the `__bool__()` method is called; so we can hook into this one:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "e15e5167",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "class zbool(zbool):\n",
    "    def __bool__(self):\n",
    "        r, pred = (True, self.z) if self.v else (False, z3.Not(self.z))\n",
    "        self.path.append(pred)\n",
    "        return r"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c1e4e51f",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "The `zbool` class can be used to keep track of Boolean values and conditions encountered during the execution. For example, we can encode the conditions encountered by Line 6 in `factorial()` as follows:"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2c1e835c",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "First, we define the concrete value (ca), and its shadow symbolic variable (za)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "ea8f2dbe",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "ca = 5\n",
    "za = z3.Int('a')"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "073a3c35",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "Then, we wrap it in zbool, and use it in a conditional, forcing the conditional to be registered in the context."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "59e65c70",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "with ConcolicTracer() as _:\n",
    "    if zbool(_.context, za == z3.IntVal(5), ca == 5):\n",
    "        print('success')"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "92fa3806",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "We can retrieve the registered conditional as follows."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "29670b81",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "_.path"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "25a86478",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### A Proxy Class for Integers"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "da06fde4",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "Next, we define a symbolic wrapper zint for int. This class keeps track of the int variables used and the predicates encountered in context. Finally, it also keeps the concrete value so that it can be used to determine the path to take. As the zint extends the primitive int class, we have to define a new method to open it for extension."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "b50de7cf",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "class zint(int):\n",
    "    def __new__(cls, context, zn, v, *args, **kw):\n",
    "        return int.__new__(cls, v, *args, **kw)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c1849126",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "As in the case of zbool, the initialization takes place in two parts. The first using create() if a new symbolic argument is being registered, and then the usual initialization."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "9d7e0cc7",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "class zint(zint):\n",
    "    @classmethod\n",
    "    def create(cls, context, zn, v=None):\n",
    "        return zproxy_create(cls, 'Int', z3.Int, context, zn, v)\n",
    "\n",
    "    def __init__(self, context, z, v=None):\n",
    "        self.z, self.v = z, v\n",
    "        self.context = context"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c00ce280",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "The int value of a zint object is its concrete value."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "2fd119f2",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "class zint(zint):\n",
    "    def __int__(self):\n",
    "        return self.v\n",
    "\n",
    "    def __pos__(self):\n",
    "        return self.v"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d08d6267",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "Using these proxies is as follows."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "212cc58b",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "outputs": [],
   "source": [
    "with ConcolicTracer() as _:\n",
    "    val = zint.create(_.context, 'int_arg', 0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "dae02488",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "val.z"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "505b7386",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "val.v"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "eaa5806e",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "_.context"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a87a9117",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "The zint class is often used to do arithmetic with, or compare to other ints. These ints can be either a variable or a constant value. We define a helper method _zv() that checks what kind of int a given value is, and produces the correct symbolic equivalent."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "975e977b",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "outputs": [],
   "source": [
    "class zint(zint):\n",
    "    def _zv(self, o):\n",
    "        return (o.z, o.v) if isinstance(o, zint) else (z3.IntVal(o), o)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "85738e5d",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "It can be used as follows"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "76f834dd",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "with ConcolicTracer() as _:\n",
    "    val = zint.create(_.context, 'int_arg', 0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "2ff82c37",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "val._zv(0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "ceaf993b",
   "metadata": {
    "scrolled": false,
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "val._zv(val)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "21c4017c",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### Equality between Integers"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a5f0b0a7",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "Two integers can be compared for equality using ne and eq."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "02df5cd2",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "class zint(zint):\n",
    "    def __ne__(self, other):\n",
    "        z, v = self._zv(other)\n",
    "        return zbool(self.context, self.z != z, self.v != v)\n",
    "\n",
    "    def __eq__(self, other):\n",
    "        z, v = self._zv(other)\n",
    "        return zbool(self.context, self.z == z, self.v == v)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4f457fa9",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "We also define req using eq in case the int being compared is on the left hand side."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "343a67a9",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "class zint(zint):\n",
    "    def __req__(self, other):\n",
    "        return self.__eq__(other)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "65039a5a",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "It can be used as follows."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "e49b4a48",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "with ConcolicTracer() as _:\n",
    "    ia = zint.create(_.context, 'int_a', 0)\n",
    "    ib = zint.create(_.context, 'int_b', 0)\n",
    "    v1 = ia == ib\n",
    "    v2 = ia != ib\n",
    "    v3 = 0 != ib\n",
    "    print(v1.z, v2.z, v3.z)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b0a894e7",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### Comparisons between Integers"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d6ad3ac7",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "Integers can also be compared for ordering, and the methods for this are defined below."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "ba46ae0c",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "class zint(zint):\n",
    "    def __lt__(self, other):\n",
    "        z, v = self._zv(other)\n",
    "        return zbool(self.context, self.z < z, self.v < v)\n",
    "\n",
    "    def __gt__(self, other):\n",
    "        z, v = self._zv(other)\n",
    "        return zbool(self.context, self.z > z, self.v > v)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e3f93c7c",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "We use the comparisons and equality operators to provide the other missing operators."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "cef1bdde",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "class zint(zint):\n",
    "    def __le__(self, other):\n",
    "        z, v = self._zv(other)\n",
    "        return zbool(self.context, z3.Or(self.z < z, self.z == z),\n",
    "                     self.v < v or self.v == v)\n",
    "\n",
    "    def __ge__(self, other):\n",
    "        z, v = self._zv(other)\n",
    "        return zbool(self.context, z3.Or(self.z > z, self.z == z),\n",
    "                     self.v > v or self.v == v)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bb43c447",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "These functions can be used as follows."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "d8fe9a75",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "with ConcolicTracer() as _:\n",
    "    ia = zint.create(_.context, 'int_a', 0)\n",
    "    ib = zint.create(_.context, 'int_b', 1)\n",
    "    v1 = ia > ib\n",
    "    v2 = ia < ib\n",
    "    print(v1.z, v2.z)\n",
    "    v3 = ia >= ib\n",
    "    v4 = ia <= ib\n",
    "    print(v3.z, v4.z)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "47875d8a",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### Binary Operators for Integers"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "10f8dce6",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "We implement relevant arithmetic operators for integers as described in the Python documentation. (The commented out operators are not directly available for z3.ArithRef. They need to be implemented separately if needed.)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "08a4d8bd",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "INT_BINARY_OPS = [\n",
    "    '__add__',\n",
    "    '__sub__',\n",
    "    '__mul__',\n",
    "    '__truediv__',\n",
    "    # '__div__',\n",
    "    '__mod__',\n",
    "    # '__divmod__',\n",
    "    '__pow__',\n",
    "    # '__lshift__',\n",
    "    # '__rshift__',\n",
    "    # '__and__',\n",
    "    # '__xor__',\n",
    "    # '__or__',\n",
    "    '__radd__',\n",
    "    '__rsub__',\n",
    "    '__rmul__',\n",
    "    '__rtruediv__',\n",
    "    # '__rdiv__',\n",
    "    '__rmod__',\n",
    "    # '__rdivmod__',\n",
    "    '__rpow__',\n",
    "    # '__rlshift__',\n",
    "    # '__rrshift__',\n",
    "    # '__rand__',\n",
    "    # '__rxor__',\n",
    "    # '__ror__',\n",
    "]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "e6335a4e",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "outputs": [],
   "source": [
    "def make_int_binary_wrapper(fname, fun, zfun):\n",
    "    def proxy(self, other):\n",
    "        z, v = self._zv(other)\n",
    "        z_ = zfun(self.z, z)\n",
    "        v_ = fun(self.v, v)\n",
    "        if isinstance(v_, float):\n",
    "            # we do not implement float results yet.\n",
    "            assert round(v_) == v_\n",
    "            v_ = round(v_)\n",
    "        return zint(self.context, z_, v_)\n",
    "\n",
    "    return proxy"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "52de7764",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "INITIALIZER_LIST = []"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "204f4032",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "def initialize():\n",
    "    for fn in INITIALIZER_LIST:\n",
    "        fn()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "5d197603",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "outputs": [],
   "source": [
    "def init_concolic_1():\n",
    "    for fname in INT_BINARY_OPS:\n",
    "        fun = getattr(int, fname)\n",
    "        zfun = getattr(z3.ArithRef, fname)\n",
    "        setattr(zint, fname, make_int_binary_wrapper(fname, fun, zfun))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "79575ab8",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "INITIALIZER_LIST.append(init_concolic_1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "5641fe69",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "init_concolic_1()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "ddfdca23",
   "metadata": {
    "scrolled": true,
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "outputs": [],
   "source": [
    "with ConcolicTracer() as _:\n",
    "    ia = zint.create(_.context, 'int_a', 0)\n",
    "    ib = zint.create(_.context, 'int_b', 1)\n",
    "    print((ia + ib).z)\n",
    "    print((ia + 10).z)\n",
    "    print((11 + ib).z)\n",
    "    print((ia - ib).z)\n",
    "    print((ia * ib).z)\n",
    "    print((ia / ib).z)\n",
    "    print((ia ** ib).z)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "35729648",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### Integer Unary Operators"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bd01cd67",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "We also implement the relevant unary operators as below."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "527c2300",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "INT_UNARY_OPS = [\n",
    "    '__neg__',\n",
    "    '__pos__',\n",
    "    # '__abs__',\n",
    "    # '__invert__',\n",
    "    # '__round__',\n",
    "    # '__ceil__',\n",
    "    # '__floor__',\n",
    "    # '__trunc__',\n",
    "]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "4e17b29b",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "def make_int_unary_wrapper(fname, fun, zfun):\n",
    "    def proxy(self):\n",
    "        return zint(self.context, zfun(self.z), fun(self.v))\n",
    "\n",
    "    return proxy"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "97d1633a",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "def init_concolic_2():\n",
    "    for fname in INT_UNARY_OPS:\n",
    "        fun = getattr(int, fname)\n",
    "        zfun = getattr(z3.ArithRef, fname)\n",
    "        setattr(zint, fname, make_int_unary_wrapper(fname, fun, zfun))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "d82b8584",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "outputs": [],
   "source": [
    "INITIALIZER_LIST.append(init_concolic_2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "006a2b2d",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "init_concolic_2()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a7b948e5",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "We can use the unary operators we defined above as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "b3ecb235",
   "metadata": {
    "scrolled": true,
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "with ConcolicTracer() as _:\n",
    "    ia = zint.create(_.context, 'int_a', 0)\n",
    "    print((-ia).z)\n",
    "    print((+ia).z)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "10247054",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### Using an Integer in a Boolean Context"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9240255b",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "An integer may be converted to a boolean context in conditionals or as part of boolean predicates such as or, and and not. In these cases, the __bool__() method gets called. Unfortunately, this method requires a primitive boolean value. Hence, we force the current integer formula to a boolean predicate and register it in the current context."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "1e62db39",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "class zint(zint):\n",
    "    def __bool__(self):\n",
    "        # return zbool(self.context, self.z, self.v) <-- not allowed\n",
    "        # force registering boolean condition\n",
    "        if self != 0:\n",
    "            return True\n",
    "        return False"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "95115812",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "It is used as follows"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "834ac061",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "with ConcolicTracer() as _:\n",
    "    za = zint.create(_.context, 'int_a', 1)\n",
    "    zb = zint.create(_.context, 'int_b', 0)\n",
    "    if za and zb:\n",
    "        print(1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "82166e51",
   "metadata": {
    "scrolled": true,
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "_.context"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3b81cbec",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### Generating fresh names"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "955a1f89",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "While using the proxy classes, we often will have to generate new symbolic variables, with names that have not been used before. For this, we define fresh_name() that always generates unique integers for names."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "8160540d",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "COUNTER = 0"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "c9920434",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "def fresh_name():\n",
    "    global COUNTER\n",
    "    COUNTER += 1\n",
    "    return COUNTER"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bdca26de",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "It can be used as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "495bd565",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "fresh_name()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "6a18adf7",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "def reset_counter():\n",
    "    global COUNTER\n",
    "    COUNTER = 0"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "5547b4b8",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "class ConcolicTracer(ConcolicTracer):\n",
    "    def __enter__(self):\n",
    "        reset_counter()\n",
    "        return self\n",
    "\n",
    "    def __exit__(self, exc_type, exc_value, tb):\n",
    "        return"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d498f538",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### Translating Arguments to Concolic Proxies"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9ef06f21",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "We had previously defined concolic() as a transparent function. We now provide the full implementation of this function. It inspects a given function's parameters, and infers the parameter types from the concrete arguments passed in. It then uses this information to instantiate the correct proxy classes for each argument."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "d698ba2b",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "class ConcolicTracer(ConcolicTracer):\n",
    "    def concolic(self, args):\n",
    "        my_args = []\n",
    "        for name, arg in zip(self.fn_args, args):\n",
    "            t = type(arg).__name__\n",
    "            zwrap = globals()['z' + t]\n",
    "            vname = \"%s_%s_%s_%s\" % (self.fn.__name__, name, t, fresh_name())\n",
    "            my_args.append(zwrap.create(self.context, vname, arg))\n",
    "            self.fn_args[name] = vname\n",
    "        return my_args"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "df0418f3",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "This is how it gets used:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "0a65afec",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "with ConcolicTracer() as _:\n",
    "    _[factorial](5)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4d1f73c8",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "With the new concolic() method, the arguments to the factorial are correctly associated with symbolic variables, which allows us to retrieve the predicates encountered."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "9eaf16b3",
   "metadata": {
    "scrolled": true,
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "_.context"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "cea4a98e",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### Evaluating the Concolic Expressions"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b525a375",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "We define zeval() to solve the predicates in a context, and return results."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "65b91e8f",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "class ConcolicTracer(ConcolicTracer):\n",
    "    def zeval(self, predicates=None, *,log=False):\n",
    "        if predicates is None:\n",
    "            path = self.path\n",
    "        else:\n",
    "            path = list(self.path)\n",
    "            for i in sorted(predicates):\n",
    "                if len(path) > i:\n",
    "                    path[i] = predicates[i]\n",
    "                else:\n",
    "                    path.append(predicates[i])\n",
    "        if log:\n",
    "            print('Predicates in path:')\n",
    "            for i, p in enumerate(path):\n",
    "                print(i, p)\n",
    "            print()\n",
    "\n",
    "        r, sol = zeval_py(path, self)\n",
    "        if r == 'sat':\n",
    "            return r, {k: sol.get(self.fn_args[k], None) for k in self.fn_args}\n",
    "        else:\n",
    "            return r, None"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a91bb499",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "Given a set of predicates that the function encountered, and the tracer under which the function was executed, the zeval_py() function first declares the relevant symbolic variables, and uses the z3.Solver() to provide a set of inputs that would trace the same path through the function."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "e2ebfe96",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "outputs": [],
   "source": [
    "def zeval_py(path, cc):\n",
    "    for decl in cc.decls:\n",
    "        if cc.decls[decl] == 'BitVec':\n",
    "            v = \"z3.%s('%s', 8)\" % (cc.decls[decl], decl)\n",
    "        else:\n",
    "            v = \"z3.%s('%s')\" % (cc.decls[decl], decl)\n",
    "        exec(v)\n",
    "    s = z3.Solver()\n",
    "    s.add(z3.And(path))\n",
    "    if s.check() == z3.unsat:\n",
    "        return 'No Solutions', {}\n",
    "    elif s.check() == z3.unknown:\n",
    "        return 'Gave up', None\n",
    "    assert s.check() == z3.sat\n",
    "    m = s.model()\n",
    "    return 'sat', {d.name(): m[d] for d in m.decls()}"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "34e41f06",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "It can be used as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "a26ab009",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "with ConcolicTracer() as _:\n",
    "    _[factorial](5)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "5bb02c74",
   "metadata": {
    "scrolled": false,
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "_.zeval()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "af9f6a24",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "That is, given the set of constraints, the assignment n == 5 conforms to all constraints."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "065f8119",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### DSE"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "53c59bfa",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "Let's now see how we can explore an example program using DSE."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "24411c3d",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "def triangle(a, b, c):\n",
    "    if a == b:\n",
    "        if b == c:\n",
    "            return 'equilateral'\n",
    "        else:\n",
    "            return 'isosceles1'\n",
    "    else:\n",
    "        if b == c:\n",
    "            return 'isosceles2'\n",
    "        else:\n",
    "            if a == c:\n",
    "                return 'isosceles3'\n",
    "            else:\n",
    "                return 'scalene'"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "e1f4cf3d",
   "metadata": {
    "scrolled": true,
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "triangle(1, 2, 1)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b953ea59",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "DSE would start with arbitrary inputs, which are executed concolically."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "5c469607",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "outputs": [],
   "source": [
    "with ConcolicTracer() as _:\n",
    "    print(_[triangle](1, 2, 3))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "695ece13",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "The symbolic variables are as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "0f0d6456",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "_.decls"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2144c968",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "The predicates are as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "6fc05111",
   "metadata": {
    "scrolled": true,
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "_.path"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "380797d3",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "Using zeval(), we solve these path conditions and obtain a solution. We find that Z3 gives us three distinct integer values:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "913c9724",
   "metadata": {
    "scrolled": true,
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "_.zeval()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "fc5fc5ef",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "If we invoke triangle() with these very values, we take the exact same path as the original input:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "6748dca8",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "triangle(0, -2, 1)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "59a11f71",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "The next step consists of picking one of the conditions of the path condition, and negating it."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "07cb88db",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "outputs": [],
   "source": [
    "z3.Not(_.path[2])"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "62b87828",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "A solution to the negated path condition is a new test input that will follow a different execution path."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "0e1f9ce9",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "_.zeval({2: z3.Not(_.path[2])})"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "86995a36",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "with ConcolicTracer() as _:\n",
    "    print(_[triangle](1, 0, 1))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "bfb4ce33",
   "metadata": {
    "scrolled": true,
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "_.path"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0930e894",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "DSE now continues replacing and negating individual conditions."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "c682fc6f",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "outputs": [],
   "source": [
    "_.path.pop()\n",
    "_.zeval({1: z3.Not(_.path[1])})"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "a7c895bc",
   "metadata": {
    "scrolled": true,
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "with ConcolicTracer() as _:\n",
    "    print(_[triangle](1, 0, 0))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "4a4660af",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "_.path"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "1551ad38",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "_.zeval({0: z3.Not(_.path[0])})"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "f66a5429",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "triangle(0, 0, 0)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3f1af0f1",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "To do this systematically we need a (random) starting point:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "2f37389c",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "outputs": [],
   "source": [
    "import random\n",
    "\n",
    "fn = triangle\n",
    "args = []\n",
    "for param in inspect.signature(fn).parameters:\n",
    "    args.append(random.randrange(1000))\n",
    "    \n",
    "print(args)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e47f3d71",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "Now we can iteratively explore the paths of the program."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "c70e5797",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "outputs": [],
   "source": [
    "import copy\n",
    "\n",
    "def dse(fn, args):\n",
    "    explored_paths = set()\n",
    "    tests = []\n",
    "    worklist = [args]\n",
    "    while worklist:\n",
    "        args = worklist.pop()\n",
    "        with ConcolicTracer() as _:\n",
    "            ret = _[fn](*args)\n",
    "            if str(_.path) in explored_paths:\n",
    "                continue\n",
    "            explored_paths.add(str(_.path))\n",
    "            tests.append((args, ret))\n",
    "\n",
    "            for index, cond in enumerate(_.path):\n",
    "                new_path = copy.copy(_.path)\n",
    "                new_path[index] = z3.Not(_.path[index])\n",
    "                if str(new_path) not in explored_paths:\n",
    "                    r, result = zeval_py(new_path, _)\n",
    "                    if r == 'sat':\n",
    "                        args = [ result.get(_.fn_args[k]).as_long() for k in _.fn_args]\n",
    "                        worklist.append(args)\n",
    "                    \n",
    "    return tests"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "2d05dbf1",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "outputs": [],
   "source": [
    "dse(triangle, args)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a4c4458a",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "You can find more details on how to do this in the [Fuzzing Book](https://www.fuzzingbook.org/html/ConcolicFuzzer.html)."
   ]
  }
 ],
 "metadata": {
  "celltoolbar": "Slideshow",
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.10.5"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}