{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": false,
    "run_control": {
     "read_only": false
    },
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "# Mining Function Specifications\n",
    "\n",
    "When testing a program, one not only needs to cover its several behaviors; one also needs to _check_ whether the result is as expected.  In this chapter, we introduce a technique that allows us to _mine_ function specifications from a set of given executions, resulting in abstract and formal _descriptions_ of what the function expects and what it delivers.  \n",
    "\n",
    "These so-called _dynamic invariants_ produce pre- and post-conditions over function arguments and variables from a set of executions.  They are useful in a variety of contexts:\n",
    "\n",
    "* Dynamic invariants provide important information for [symbolic fuzzing](SymbolicFuzzing.ipynb), such as types and ranges of function arguments.\n",
    "* Dynamic invariants provide pre- and postconditions for formal program proofs and verification.\n",
    "* Dynamic invariants provide a large number of assertions that can check whether function behavior has changed.\n",
    "\n",
    "Traditionally, dynamic invariants are dependent on the executions they are derived from.  However, when paired with comprehensive test generators, they quickly become very precise, as we show in this chapter."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": false,
    "run_control": {
     "read_only": false
    },
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "**Prerequisites**\n",
    "\n",
    "* You should be familiar with tracing program executions, as in the [chapter on coverage](Coverage.ipynb).\n",
    "* Later in this section, we make use of Python program transformations; some knowledge on the Python AST functions is helpful.\n",
    "* The interplay with symbolic testing builds on, well, [symbolic testing](SymbolicFuzzer.ipynb),"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "outputs": [],
   "source": [
    "import fuzzingbook_utils"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "outputs": [],
   "source": [
    "import Intro_Testing"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": true,
    "run_control": {
     "read_only": false
    },
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "## Specifications and Assertions\n",
    "\n",
    "When implementing a function or program, one usually works against a _specification_ – a set of documented requirements to be satisfied by the code.  Such specifications can come in natural language.  A formal specification, however, allows the computer to check whether the specification is satisfied.\n",
    "\n",
    "In the [introduction to testing](Intro_Testing.ipynb), we have seen how _preconditions_ and _postconditions_ can describe what a function does.  Consider the following (simple) square root function:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "def my_sqrt(x):\n",
    "    assert x >= 0  # Precondition\n",
    "    \n",
    "    ...\n",
    "    \n",
    "    assert result * result == x  # Postcondition\n",
    "    return result"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "The assertion `assert p` checks the condition `p`; if it does not hold, execution is aborted.  Here, the actual body is not yet written; we use the assertions as a specification of what `my_sqrt()` _expects_, and what it _delivers_.\n",
    "\n",
    "The topmost assertion is the _precondition_, stating the requirements on the function arguments.  The assertion at the end is the _postcondition_, stating the properties of the function result (including its relationship with the original arguments).  Using these pre- and postconditions as a specification, we can now go and implement a square root function that satisfies them.  Once implemented, we can have the assertions check at runtime whether `my_sqrt()` works as expected; a [symbolic](SymbolicFuzzer.ipynb) or [concolic](ConcolicFuzzer.ipynb) test generator will even specifically try to find inputs where the assertions do _not_ hold.  (An assertion can be seen as a conditional branch towards aborting the execution, and any technique that tries to cover all code branches will also try to invalidate as many assertions as possible.)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "However, not every piece of code is developed with explicit specifications in the first place; let alone does most code comes with formal pre- and post-conditions.  (Just take a look at the chapters in this book.)  This is a pity: As Ken Thompson famously said, \"Without specifications, there are no bugs – only surprises\".  It is also a problem for testing, since, of course, testing needs some specification to test against.  This raises the interesting question: Can we somehow _retrofit_ existing code with \"specifications\" that properly describe their behavior, allowing developers to simply _check_ them rather than having to write them from scratch?  This is what we do in this chapter.}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    },
    "toc-hr-collapsed": true
   },
   "source": [
    "## Mining Type Specifications\n",
    "\n",
    "For our Python code, one of the most important \"specifications\" we need is *types*.  Python being a \"dynamically\" typed language means that all data types are determined at run time; the code itself does not explicitly state whether a variable is an integer, a string, an array, a dictionary – or whatever.  As _writer_ of Python code, omitting explicit type declarations may save time (and allows for some fun hacks).  It is not sure whether a lack of types helps in _reading_ and _understanding_ code for humans.  For a _computer_ trying to analyze code, the lack of explicit types is detrimental.  If, say, a constraint solver, sees `if x:` and cannot know whether `x` is supposed to be a number or a string, this introduces an ambiguity which multiplies over the entire analysis in a combinatorial explosion.  Our first task thus will be to mine _static_ types (as part of the code) from _values_ we observe at run time."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "How can we mine types from executions?  The answer is simple: \n",
    "\n",
    "1. We observe a function during execution\n",
    "2. We track the _types_ of its arguments\n",
    "3. We include these types as annotations or assertions into the codee.\n",
    "\n",
    "To do so, we can make use of Python's tracing facility we already observed in the [chapter on coverage](Coverage.ipynb).  With every call to a function, we retrieve the arguments, their values, and their types."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "source": [
    "As an example, consider the full implementation of `my_sqrt()` from the [introduction to testing](Intro_Testing.ipynb):"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "outputs": [],
   "source": [
    "import fuzzingbook_utils"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "button": false,
    "new_sheet": false,
    "run_control": {
     "read_only": false
    },
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "def my_sqrt(x):\n",
    "    \"\"\"Computes the square root of x, using the Newton-Raphson method\"\"\"\n",
    "    approx = None\n",
    "    guess = x / 2\n",
    "    while approx != guess:\n",
    "        approx = guess\n",
    "        guess = (approx + x / approx) / 2\n",
    "    return approx"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "source": [
    "`my_sqrt()` does not come with any assertions that would check types or values:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "outputs": [],
   "source": [
    "from ExpectError import ExpectError, ExpectTimeout"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "with ExpectError():\n",
    "    my_sqrt(\"foo\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "with ExpectTimeout(1):\n",
    "    x = my_sqrt(-1)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "source": [
    "Our goal is to determine types from _normal_ invocations such as this one:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "my_sqrt(25)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "### Tracking Calls\n",
    "\n",
    "We can define a _tracer function_ that tracks the execution of `my_sqrt()`, listing its arguments and return values:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "outputs": [],
   "source": [
    "import sys"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "class Tracker(object):\n",
    "    def __init__(self, log=False):\n",
    "        self._log = log\n",
    "        self.reset()\n",
    "\n",
    "    def reset(self):\n",
    "        self._calls = {}\n",
    "        self._stack = []\n",
    "\n",
    "    # Start of `with` block\n",
    "    def __enter__(self):\n",
    "        self.original_trace_function = sys.gettrace()\n",
    "        sys.settrace(self.traceit)\n",
    "        return self\n",
    "\n",
    "    # End of `with` block\n",
    "    def __exit__(self, exc_type, exc_value, tb):\n",
    "        sys.settrace(self.original_trace_function)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "def get_arguments(frame):\n",
    "    \"\"\"Return call arguments in the given frame\"\"\"\n",
    "    # When called, all arguments are local variables\n",
    "    arguments = [(var, frame.f_locals[var]) for var in frame.f_locals]\n",
    "    arguments.reverse()  # Want same order as call\n",
    "    return arguments"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "def simple_call_string(function_name, argument_list):\n",
    "    \"\"\"Return function_name(arg[0], arg[1], ...) as a string\"\"\"\n",
    "    return function_name + \"(\" + \\\n",
    "        \", \".join([var + \"=\" + repr(value)\n",
    "                   for (var, value) in argument_list]) + \")\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "class CallTracker(Tracker):\n",
    "    def add_call(self, function_name, arguments, return_value=None):\n",
    "        \"\"\"Add given call to list of calls\"\"\"\n",
    "        if function_name not in self._calls:\n",
    "            self._calls[function_name] = []\n",
    "        self._calls[function_name].append((arguments, return_value))\n",
    "\n",
    "    # Tracking function: Record all calls and all args\n",
    "    def traceit(self, frame, event, arg):\n",
    "        if event == \"call\":\n",
    "            self.trace_call(frame, event, arg)\n",
    "        elif event == \"return\":\n",
    "            self.trace_return(frame, event, arg)\n",
    "            \n",
    "        return self.traceit\n",
    "        \n",
    "    def trace_call(self, frame, event, arg):\n",
    "        code = frame.f_code\n",
    "        function_name = code.co_name\n",
    "        arguments = get_arguments(frame)\n",
    "        self._stack.append((function_name, arguments))\n",
    "\n",
    "        if self._log:\n",
    "            print(simple_call_string(function_name, arguments))\n",
    "\n",
    "    def trace_return(self, frame, event, arg):\n",
    "        code = frame.f_code\n",
    "        function_name = code.co_name\n",
    "        return_value = arg\n",
    "        \n",
    "        called_function_name, called_arguments = self._stack.pop()\n",
    "        assert function_name == called_function_name\n",
    "        \n",
    "        if self._log:\n",
    "            print(simple_call_string(function_name, called_arguments), \"returns\", return_value)\n",
    "            \n",
    "        self.add_call(function_name, called_arguments, return_value)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "class CallTracker(CallTracker):\n",
    "    def calls(self, function_name=None):\n",
    "        if function_name is None:\n",
    "            return self._calls\n",
    "\n",
    "        return self._calls[function_name]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "with CallTracker(log=True) as tracker:\n",
    "    y = my_sqrt(25)\n",
    "    y = my_sqrt(2.0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "calls = tracker.calls('my_sqrt')\n",
    "calls"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "def simple_call_string(function_name, argument_list, return_value = None):\n",
    "    \"\"\"Return function_name(arg[0], arg[1], ...) as a string\"\"\"\n",
    "    call = function_name + \"(\" + \\\n",
    "        \", \".join([var + \"=\" + repr(value)\n",
    "                   for (var, value) in argument_list]) + \")\"\n",
    "\n",
    "    if return_value is not None:\n",
    "        call += \" = \" + repr(return_value)\n",
    "        \n",
    "    return call"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "source": [
    "\\todo{Import these into [Carver](Carver.ipynb)}"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "argument_list, return_value = calls[0]\n",
    "simple_call_string('my_sqrt', argument_list, return_value)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": false,
    "run_control": {
     "read_only": false
    },
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "### Getting Types\n",
    "\n",
    "Python has an elaborate type system:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "type(4)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "type(2.0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "type([4])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "source": [
    "We can retrieve the type of the first argument to `my_sqrt()`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "parameter, value = argument_list[0]\n",
    "parameter, type(value)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "source": [
    "as well as the type of the return value:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "type(return_value)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "source": [
    "Hence, we see that (so far), `my_sqrt()` is a function taking (among others) integers and returning floats.  We could declare `my_sqrt()` as:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "def my_sqrt_annotated(x: int) -> float:\n",
    "    return my_sqrt(x)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "source": [
    "This is a representation we could place in a static type checker, allowing to check whether calls to `my_sqrt()` actually pass a number.  A dynamic type checker could run such checks at runtime.  And of course, any symbolic interpretation will greatly profit from the additional annotations."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "source": [
    "By default, Python does not do anything with such annotations.  However, tools can access annotations from functions and other objects:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "my_sqrt_annotated.__annotations__"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "### Annotating Functions\n",
    "\n",
    "Let us go and annotate functions automatically, based on the types we have seen."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "outputs": [],
   "source": [
    "import ast\n",
    "import inspect\n",
    "import astunparse"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "source": [
    "We can get the source of a function (if it is in the same file)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "outputs": [],
   "source": [
    "from fuzzingbook_utils import print_content"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "outputs": [],
   "source": [
    "from pygments.lexers import PythonLexer"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "my_sqrt_source = inspect.getsource(my_sqrt)\n",
    "print_content(my_sqrt_source, '.py')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "source": [
    "Parsing this gives us an abstract syntax tree (AST):"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "my_sqrt_ast = ast.parse(my_sqrt_source)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "ast.dump(my_sqrt_ast)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "Printing this out as Python code is a bit more readable:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "print(astunparse.unparse(my_sqrt_ast))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "source": [
    "We want to transform this adding annotations."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "First, a helper function to parse type names:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "def parse_type(name):\n",
    "    class ValueVisitor(ast.NodeVisitor):\n",
    "        def visit_Expr(self, node):\n",
    "            self.value_node = node.value\n",
    "        \n",
    "    tree = ast.parse(name)\n",
    "    name_visitor = ValueVisitor()\n",
    "    name_visitor.visit(tree)\n",
    "    return name_visitor.value_node"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "ast.dump(parse_type('int'))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "ast.dump(parse_type('[Any]'))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "Now, a helper to actually add type annotations to a function AST.  This would be called as\n",
    "\n",
    "```python\n",
    "    TypeTransformer({'x': 'int'}, 'float').visit(ast)\n",
    "```\n",
    "\n",
    "to annotate the arguments of `my_sqrt()`: `x` with `int`, and the return type with `float`.  The returned AST can then be unparsed, compiled or analyzed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "class TypeTransformer(ast.NodeTransformer):\n",
    "    def __init__(self, argument_types, return_type=None):\n",
    "        self.argument_types = argument_types\n",
    "        self.return_type = return_type\n",
    "        super().__init__()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "class TypeTransformer(TypeTransformer):\n",
    "    def annotate_arg(self, arg):\n",
    "        \"\"\"Add annotation to single function argument\"\"\"\n",
    "        arg_name = arg.arg\n",
    "        if arg_name in self.argument_types:\n",
    "            arg.annotation = parse_type(self.argument_types[arg_name])\n",
    "        return arg"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "class TypeTransformer(TypeTransformer):\n",
    "    def visit_FunctionDef(self, node):\n",
    "        \"\"\"Add annotation to function\"\"\"\n",
    "        # Set argument types\n",
    "        new_args = []\n",
    "        for arg in node.args.args:\n",
    "            new_args.append(self.annotate_arg(arg))\n",
    "\n",
    "        new_arguments = ast.arguments(\n",
    "            new_args,\n",
    "            node.args.vararg,\n",
    "            node.args.kwonlyargs,\n",
    "            node.args.kw_defaults,\n",
    "            node.args.kwarg,\n",
    "            node.args.defaults\n",
    "        )\n",
    "\n",
    "        # Set return type\n",
    "        node.returns = parse_type(self.return_type)\n",
    "        \n",
    "        return ast.copy_location(ast.FunctionDef(node.name, new_arguments, \n",
    "                                                 node.body, node.decorator_list,\n",
    "                                                 node.returns), node)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "Does this work?  Yes!"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "new_ast = TypeTransformer({'x': 'int'}, 'float').visit(my_sqrt_ast)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "print_content(astunparse.unparse(new_ast), '.py')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "### All Together\n",
    "\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "button": false,
    "new_sheet": false,
    "run_control": {
     "read_only": false
    },
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "outputs": [],
   "source": [
    "with CallTracker() as tracker:\n",
    "    y = my_sqrt(25)\n",
    "    y = my_sqrt(2.0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "button": false,
    "code_folding": [],
    "new_sheet": false,
    "run_control": {
     "read_only": false
    },
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "tracker.calls()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "def type_string(value):\n",
    "    return type(value).__name__"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "type_string(4)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "type_string([])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "def annotate_types(calls):\n",
    "    annotated_functions = {}\n",
    "    \n",
    "    for function_name in calls:\n",
    "        annotated_functions[function_name] = annotate_types_function(function_name, calls[function_name])\n",
    "\n",
    "    return annotated_functions\n",
    "        \n",
    "def annotate_types_function(function_name, function_calls):\n",
    "    function = globals()[function_name]\n",
    "    function_code = inspect.getsource(function)\n",
    "    function_ast = ast.parse(function_code)\n",
    "    return annotate_types_function_ast(function_ast, function_calls)\n",
    "\n",
    "def annotate_types_function_ast(function_ast, function_calls):\n",
    "    parameter_types = {}\n",
    "    return_type = None\n",
    "        \n",
    "    for calls_seen in function_calls:\n",
    "        args, return_value = calls_seen\n",
    "        if return_value is not None:\n",
    "            return_type = type_string(return_value)\n",
    "        for parameter, value in args:\n",
    "            parameter_types[parameter] = type_string(value)\n",
    "        \n",
    "    annotated_function_ast = TypeTransformer(parameter_types, return_type).visit(function_ast)\n",
    "    return annotated_function_ast"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "print_content(astunparse.unparse(annotate_types(tracker.calls())['my_sqrt']), '.py')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "class TypeAnnotator(CallTracker):\n",
    "    def typed_functions_ast(self, function_name=None):\n",
    "        if function_name is None:\n",
    "            return annotate_types(self.calls())\n",
    "        \n",
    "        return annotate_types_function(function_name, self.calls(function_name))\n",
    "    \n",
    "    def typed_functions(self):\n",
    "        return ''.join([astunparse.unparse(self.typed_functions_ast(function_name))         \n",
    "                            for function_name in self.calls()])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "with TypeAnnotator() as annotator:\n",
    "    y = my_sqrt(25)\n",
    "    y = my_sqrt(2.0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "print_content(annotator.typed_functions(), '.py')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "def sum3(a, b, c):\n",
    "    return a + b + c"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "with TypeAnnotator() as annotator:\n",
    "    y = my_sqrt(1.0)\n",
    "    y = sum3(1.0, 2.0, 3.0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "print_content(annotator.typed_functions(), '.py')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "with TypeAnnotator() as annotator:\n",
    "    y = sum3(\"one\", \"two\", \"three\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "print_content(annotator.typed_functions(), '.py')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": false,
    "run_control": {
     "read_only": false
    },
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### Use in Symbolic Testing\n",
    "\n",
    "\\todo{add}"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "outputs": [],
   "source": [
    "import SymbolicFuzzer  # minor dependency"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "## Mining Specifications from Generated Tests"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "outputs": [],
   "source": [
    "import GrammarFuzzer  # minor dependency"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": false,
    "run_control": {
     "read_only": false
    },
    "slideshow": {
     "slide_type": "slide"
    },
    "toc-hr-collapsed": true
   },
   "source": [
    "## Mining Complex Invariants\n",
    "\n",
    "\\todo{add}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": false,
    "run_control": {
     "read_only": false
    },
    "slideshow": {
     "slide_type": "slide"
    },
    "toc-hr-collapsed": true
   },
   "source": [
    "### Mining Ranges\n",
    "\n",
    "\\todo{add}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": false,
    "run_control": {
     "read_only": false
    },
    "slideshow": {
     "slide_type": "slide"
    },
    "toc-hr-collapsed": true
   },
   "source": [
    "### Patterns for Pre- and Postconditions\n",
    "\n",
    "\\todo{add}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": true,
    "run_control": {
     "read_only": false
    },
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "## Lessons Learned\n",
    "\n",
    "* _Lesson one_\n",
    "* _Lesson two_\n",
    "* _Lesson three_"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": false,
    "run_control": {
     "read_only": false
    },
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "## Next Steps\n",
    "\n",
    "_Link to subsequent chapters (notebooks) here, as in:_\n",
    "\n",
    "* [use _mutations_ on existing inputs to get more valid inputs](MutationFuzzer.ipynb)\n",
    "* [use _grammars_ (i.e., a specification of the input format) to get even more valid inputs](Grammars.ipynb)\n",
    "* [reduce _failing inputs_ for efficient debugging](Reducer.ipynb)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "## Background\n",
    "\n",
    "_Cite relevant works in the literature and put them into context, as in:_\n",
    "\n",
    "The idea of ensuring that each expansion in the grammar is used at least once goes back to Burkhardt \\cite{Burkhardt1967}, to be later rediscovered by Paul Purdom \\cite{Purdom1972}."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": true,
    "run_control": {
     "read_only": false
    },
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "## Exercises\n",
    "\n",
    "_Close the chapter with a few exercises such that people have things to do.  To make the solutions hidden (to be revealed by the user), have them start with_\n",
    "\n",
    "```markdown\n",
    "**Solution.**\n",
    "```\n",
    "\n",
    "_Your solution can then extend up to the next title (i.e., any markdown cell starting with `#`)._\n",
    "\n",
    "_Running `make metadata` will automatically add metadata to the cells such that the cells will be hidden by default, and can be uncovered by the user.  The button will be introduced above the solution._"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": false,
    "run_control": {
     "read_only": false
    },
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "### Exercise 1: _Title_\n",
    "\n",
    "_Text of the exercise_"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "cell_style": "center",
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "# Some code that is part of the exercise\n",
    "pass"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    },
    "solution2": "hidden",
    "solution2_first": true
   },
   "source": [
    "_Some more text for the exercise_"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    },
    "solution2": "hidden"
   },
   "source": [
    "**Solution.** _Some text for the solution_"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "cell_style": "split",
    "slideshow": {
     "slide_type": "skip"
    },
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "# Some code for the solution\n",
    "2 + 2"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    },
    "solution2": "hidden"
   },
   "source": [
    "_Some more text for the solution_"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": false,
    "run_control": {
     "read_only": false
    },
    "slideshow": {
     "slide_type": "subslide"
    },
    "solution": "hidden",
    "solution2": "hidden",
    "solution2_first": true,
    "solution_first": true
   },
   "source": [
    "### Exercise 2: _Title_\n",
    "\n",
    "_Text of the exercise_"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": false,
    "run_control": {
     "read_only": false
    },
    "slideshow": {
     "slide_type": "skip"
    },
    "solution": "hidden",
    "solution2": "hidden"
   },
   "source": [
    "**Solution.** _Solution for the exercise_"
   ]
  }
 ],
 "metadata": {
  "ipub": {
   "bibliography": "fuzzingbook.bib",
   "toc": true
  },
  "kernelspec": {
   "display_name": "Python 3",
   "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.6.8"
  },
  "toc": {
   "base_numbering": 1,
   "nav_menu": {},
   "number_sections": true,
   "sideBar": true,
   "skip_h1_title": true,
   "title_cell": "",
   "title_sidebar": "Contents",
   "toc_cell": false,
   "toc_position": {},
   "toc_section_display": true,
   "toc_window_display": true
  },
  "toc-autonumbering": false
 },
 "nbformat": 4,
 "nbformat_minor": 2
}