{ "cells": [ { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "slide" } }, "source": [ "# Prototyping with Python\n", "\n", "_This is the manuscript of Andreas Zeller's keynote\n", "\"Coding Effective Testing Tools Within Minutes\" at the TAIC PART 2020 conference._" ] }, { "attachments": {}, "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "In our [Fuzzing Book](index.ipynb), we use Python to implement automated testing techniques, and also as the language for most of our test subjects. Why Python? The short answer is\n", "\n", "> Python made us amazingly _productive_. Most techniques in this book took **2-3 days** to implement. This is about **10-20 times faster** than for \"classic\" languages like C or Java.\n", "\n", "A factor of 10–20 in productivity is enormous, almost ridiculous. Why is that so, and which consequences does this have for research and teaching?\n", "\n", "In this essay, we will explore some reasons, prototyping a _symbolic test generator_ from scratch. This normally would be considered a very difficult task, taking months to build. Yet, developing the code in this chapter took less than two hours – and explaining it takes less than 20 minutes." ] }, { "cell_type": "code", "execution_count": 1, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:50.432189Z", "iopub.status.busy": "2024-01-18T17:30:50.431421Z", "iopub.status.idle": "2024-01-18T17:30:50.490607Z", "shell.execute_reply": "2024-01-18T17:30:50.490312Z" }, "slideshow": { "slide_type": "skip" } }, "outputs": [ { "data": { "text/html": [ "\n", " \n", " " ], "text/plain": [ "" ] }, "execution_count": 1, "metadata": {}, "output_type": "execute_result" } ], "source": [ "from bookutils import YouTubeVideo\n", "YouTubeVideo(\"IAreRIID9lM\")" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "slide" } }, "source": [ "## Python is Easy\n", "\n", "Python is a high-level language that allows one to focus on the actual _algorithms_ rather than how individual bits and bytes are passed around in memory. For this book, this is important: We want to focus on how individual techniques work, and not so much their optimization. Focusing on algorithms allows you to toy and tinker with them, and quickly develop your own. Once you have found out how to do things, you can still port your approach to some other language or specialized setting." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "As an example, take the (in)famous _triangle_ program, which classifies a triangle of lengths $a$, $b$, $c$ into one of three categories. It reads like pseudocode; yet, we can easily execute it." ] }, { "cell_type": "code", "execution_count": 2, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:50.511999Z", "iopub.status.busy": "2024-01-18T17:30:50.511839Z", "iopub.status.idle": "2024-01-18T17:30:50.513988Z", "shell.execute_reply": "2024-01-18T17:30:50.513713Z" }, "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "def triangle(a, b, c):\n", " if a == b:\n", " if b == c:\n", " return 'equilateral'\n", " else:\n", " return 'isosceles #1'\n", " else:\n", " if b == c:\n", " return 'isosceles #2'\n", " else:\n", " if a == c:\n", " return 'isosceles #3'\n", " else:\n", " return 'scalene'" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Here's an example of executing the `triangle()` function:" ] }, { "cell_type": "code", "execution_count": 3, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:50.515551Z", "iopub.status.busy": "2024-01-18T17:30:50.515448Z", "iopub.status.idle": "2024-01-18T17:30:50.517468Z", "shell.execute_reply": "2024-01-18T17:30:50.517216Z" }, "slideshow": { "slide_type": "subslide" } }, "outputs": [ { "data": { "text/plain": [ "'scalene'" ] }, "execution_count": 3, "metadata": {}, "output_type": "execute_result" } ], "source": [ "triangle(2, 3, 4)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "For the remainder of this chapter, we will use the `triangle()` function as ongoing example for a program to be tested. Of course, the complexity of `triangle()` is a far cry from large systems, and what we show in this chapter will not apply to, say, an ecosystem of thousands of intertwined microservices. Its point, however, is to show how easy certain techniques can be – if you have the right language and environment." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "slide" } }, "source": [ "## Fuzzing is as Easy as Always" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "If you want to test `triangle()` with random values, that's fairly easy to do. Just bring along one of the Python random number generators and throw them into `triangle()`." ] }, { "cell_type": "code", "execution_count": 4, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:50.519087Z", "iopub.status.busy": "2024-01-18T17:30:50.518982Z", "iopub.status.idle": "2024-01-18T17:30:50.520599Z", "shell.execute_reply": "2024-01-18T17:30:50.520337Z" }, "slideshow": { "slide_type": "skip" } }, "outputs": [], "source": [ "from random import randrange" ] }, { "cell_type": "code", "execution_count": 5, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:50.522054Z", "iopub.status.busy": "2024-01-18T17:30:50.521970Z", "iopub.status.idle": "2024-01-18T17:30:50.524167Z", "shell.execute_reply": "2024-01-18T17:30:50.523944Z" }, "slideshow": { "slide_type": "subslide" } }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "triangle(4, 9, 4) = 'isosceles #3'\n", "triangle(8, 1, 6) = 'scalene'\n", "triangle(3, 9, 2) = 'scalene'\n", "triangle(6, 9, 4) = 'scalene'\n", "triangle(7, 4, 5) = 'scalene'\n", "triangle(7, 7, 5) = 'isosceles #1'\n", "triangle(2, 8, 1) = 'scalene'\n", "triangle(8, 2, 5) = 'scalene'\n", "triangle(8, 8, 2) = 'isosceles #1'\n", "triangle(5, 2, 6) = 'scalene'\n" ] } ], "source": [ "for i in range(10):\n", " a = randrange(1, 10)\n", " b = randrange(1, 10)\n", " c = randrange(1, 10)\n", "\n", " t = triangle(a, b, c)\n", " print(f\"triangle({a}, {b}, {c}) = {repr(t)}\")" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "So far, so good – but that's something you can do in pretty much any programming language. What is it that makes Python special?" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "slide" } }, "source": [ "## Dynamic Analysis in Python: So Easy it Hurts\n", "\n", "Dynamic analysis is the ability to track what is happening during program execution. The Python `settrace()` mechanism allows you to track all code lines, all variables, all values, as the program executes – and all this in a handful of lines of code. Our `Coverage` class from [the chapter on coverage](Coverage.ipynb) shows how to capture a trace of all lines executed in five lines of code; such a trace easily converts into sets of lines or branches executed. With two more lines, you can easily track all functions, arguments, variable values, too – see for instance our [chapter on dynamic invariants](DynamicInvariants). And you can even access the source code of individual functions (and print it out, too!) All this takes 10, maybe 20 minutes to implement." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "Here is a piece of Python that does it all. We track lines executed, and for every line, we print its source codes and the current values of all local variables:" ] }, { "cell_type": "code", "execution_count": 6, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:50.525712Z", "iopub.status.busy": "2024-01-18T17:30:50.525617Z", "iopub.status.idle": "2024-01-18T17:30:50.527067Z", "shell.execute_reply": "2024-01-18T17:30:50.526844Z" }, "slideshow": { "slide_type": "skip" } }, "outputs": [], "source": [ "import sys\n", "import inspect" ] }, { "cell_type": "code", "execution_count": 7, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:50.528415Z", "iopub.status.busy": "2024-01-18T17:30:50.528335Z", "iopub.status.idle": "2024-01-18T17:30:50.530625Z", "shell.execute_reply": "2024-01-18T17:30:50.530369Z" }, "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "def traceit(frame, event, arg):\n", " function_code = frame.f_code\n", " function_name = function_code.co_name\n", " lineno = frame.f_lineno\n", " vars = frame.f_locals\n", "\n", " source_lines, starting_line_no = inspect.getsourcelines(frame.f_code)\n", " loc = f\"{function_name}:{lineno} {source_lines[lineno - starting_line_no].rstrip()}\"\n", " vars = \", \".join(f\"{name} = {vars[name]}\" for name in vars)\n", "\n", " print(f\"{loc:50} ({vars})\")\n", "\n", " return traceit" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "The function `sys.settrace()` registers `traceit()` as a trace function; it will then trace the given invocation of `triangle()`:" ] }, { "cell_type": "code", "execution_count": 8, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:50.532065Z", "iopub.status.busy": "2024-01-18T17:30:50.531987Z", "iopub.status.idle": "2024-01-18T17:30:50.533667Z", "shell.execute_reply": "2024-01-18T17:30:50.533437Z" }, "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "def triangle_traced():\n", " sys.settrace(traceit)\n", " triangle(2, 2, 1)\n", " sys.settrace(None)" ] }, { "cell_type": "code", "execution_count": 9, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:50.535027Z", "iopub.status.busy": "2024-01-18T17:30:50.534944Z", "iopub.status.idle": "2024-01-18T17:30:50.576866Z", "shell.execute_reply": "2024-01-18T17:30:50.576630Z" }, "slideshow": { "slide_type": "fragment" } }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "triangle:1 def triangle(a, b, c): (a = 2, b = 2, c = 1)\n", "triangle:2 if a == b: (a = 2, b = 2, c = 1)\n", "triangle:3 if b == c: (a = 2, b = 2, c = 1)\n", "triangle:6 return 'isosceles #1' (a = 2, b = 2, c = 1)\n", "triangle:6 return 'isosceles #1' (a = 2, b = 2, c = 1)\n" ] } ], "source": [ "triangle_traced()" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "In comparison, try to build such a dynamic analysis for, say, C. You can either _instrument_ the code to track all lines executed and record variable values, storing the resulting info in some database. This will take you _weeks,_ if not _months_ to implement. You can also run your code through a debugger (step-print-step-print-step-print); but again, programming the interaction can take days. And once you have the first results, you'll probably realize you need something else or better, so you go back to the drawing board. Not fun." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Together with a dynamic analysis such as the one above, you can make fuzzing much smarter. Search-based testing, for instance, evolves a population of inputs towards a particular goal, such as coverage. With a good dynamic analysis, you can quickly implement search-based strategies for arbitrary goals." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "slide" } }, "source": [ "## Static Analysis in Python: Still Easy\n", "\n", "Static analysis refers to the ability to analyze _program code_ without actually executing it. Statically analyzing Python code to deduce any property can be a nightmare, because the language is so highly dynamic. (More on that below.)\n", "\n", "If your static analysis does not have to be _sound_, – for instance, because you only use it to _support_ and _guide_ another technique such as testing – then a static analysis in Python can be very simple. The `ast` module allows you to turn any Python function into an abstract syntax tree (AST), which you then can traverse as you like. Here's the AST for our `triangle()` function:" ] }, { "cell_type": "code", "execution_count": 10, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:50.578457Z", "iopub.status.busy": "2024-01-18T17:30:50.578376Z", "iopub.status.idle": "2024-01-18T17:30:50.580056Z", "shell.execute_reply": "2024-01-18T17:30:50.579835Z" }, "slideshow": { "slide_type": "skip" } }, "outputs": [], "source": [ "from bookutils import rich_output" ] }, { "cell_type": "code", "execution_count": 11, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:50.581619Z", "iopub.status.busy": "2024-01-18T17:30:50.581532Z", "iopub.status.idle": "2024-01-18T17:30:50.583188Z", "shell.execute_reply": "2024-01-18T17:30:50.582947Z" }, "slideshow": { "slide_type": "skip" } }, "outputs": [], "source": [ "import ast" ] }, { "cell_type": "code", "execution_count": 12, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:50.584719Z", "iopub.status.busy": "2024-01-18T17:30:50.584639Z", "iopub.status.idle": "2024-01-18T17:30:50.586812Z", "shell.execute_reply": "2024-01-18T17:30:50.586567Z" }, "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "if rich_output():\n", " # Normally, this will do\n", " from showast import show_ast\n", "else:\n", " def show_ast(tree):\n", " ast.dump(tree, indent=4)" ] }, { "cell_type": "code", "execution_count": 13, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:50.588269Z", "iopub.status.busy": "2024-01-18T17:30:50.588187Z", "iopub.status.idle": "2024-01-18T17:30:51.015752Z", "shell.execute_reply": "2024-01-18T17:30:51.015433Z" }, "slideshow": { "slide_type": "fragment" } }, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "0\n", "FunctionDef\n", "\n", "\n", "\n", "1\n", ""triangle"\n", "\n", "\n", "\n", "0--1\n", "\n", "\n", "\n", "\n", "2\n", "arguments\n", "\n", "\n", "\n", "0--2\n", "\n", "\n", "\n", "\n", "9\n", "If\n", "\n", "\n", "\n", "0--9\n", "\n", "\n", "\n", "\n", "3\n", "arg\n", "\n", "\n", "\n", "2--3\n", "\n", "\n", "\n", "\n", "5\n", "arg\n", "\n", "\n", "\n", "2--5\n", "\n", "\n", "\n", "\n", "7\n", "arg\n", "\n", "\n", "\n", "2--7\n", "\n", "\n", "\n", "\n", "4\n", ""a"\n", "\n", "\n", "\n", "3--4\n", "\n", "\n", "\n", "\n", "6\n", ""b"\n", "\n", "\n", "\n", "5--6\n", "\n", "\n", "\n", "\n", "8\n", ""c"\n", "\n", "\n", "\n", "7--8\n", "\n", "\n", "\n", "\n", "10\n", "Compare\n", "\n", "\n", "\n", "9--10\n", "\n", "\n", "\n", "\n", "18\n", "If\n", "\n", "\n", "\n", "9--18\n", "\n", "\n", "\n", "\n", "33\n", "If\n", "\n", "\n", "\n", "9--33\n", "\n", "\n", "\n", "\n", "11\n", "Name\n", "\n", "\n", "\n", "10--11\n", "\n", "\n", "\n", "\n", "14\n", "Eq\n", "\n", "\n", "\n", "10--14\n", "\n", "\n", "\n", "\n", "15\n", "Name\n", "\n", "\n", "\n", "10--15\n", "\n", "\n", "\n", "\n", "12\n", ""a"\n", "\n", "\n", "\n", "11--12\n", "\n", "\n", "\n", "\n", "13\n", "Load\n", "\n", "\n", "\n", "11--13\n", "\n", "\n", "\n", "\n", "16\n", ""b"\n", "\n", "\n", "\n", "15--16\n", "\n", "\n", "\n", "\n", "17\n", "Load\n", "\n", "\n", "\n", "15--17\n", "\n", "\n", "\n", "\n", "19\n", "Compare\n", "\n", "\n", "\n", "18--19\n", "\n", "\n", "\n", "\n", "27\n", "Return\n", "\n", "\n", "\n", "18--27\n", "\n", "\n", "\n", "\n", "30\n", "Return\n", "\n", "\n", "\n", "18--30\n", "\n", "\n", "\n", "\n", "20\n", "Name\n", "\n", "\n", "\n", "19--20\n", "\n", "\n", "\n", "\n", "23\n", "Eq\n", "\n", "\n", "\n", "19--23\n", "\n", "\n", "\n", "\n", "24\n", "Name\n", "\n", "\n", "\n", "19--24\n", "\n", "\n", "\n", "\n", "21\n", ""b"\n", "\n", "\n", "\n", "20--21\n", "\n", "\n", "\n", "\n", "22\n", "Load\n", "\n", "\n", "\n", "20--22\n", "\n", "\n", "\n", "\n", "25\n", ""c"\n", "\n", "\n", "\n", "24--25\n", "\n", "\n", "\n", "\n", "26\n", "Load\n", "\n", "\n", "\n", "24--26\n", "\n", "\n", "\n", "\n", "28\n", "Constant\n", "\n", "\n", "\n", "27--28\n", "\n", "\n", "\n", "\n", "29\n", ""equilateral"\n", "\n", "\n", "\n", "28--29\n", "\n", "\n", "\n", "\n", "31\n", "Constant\n", "\n", "\n", "\n", "30--31\n", "\n", "\n", "\n", "\n", "32\n", ""isosceles #1"\n", "\n", "\n", "\n", "31--32\n", "\n", "\n", "\n", "\n", "34\n", "Compare\n", "\n", "\n", "\n", "33--34\n", "\n", "\n", "\n", "\n", "42\n", "Return\n", "\n", "\n", "\n", "33--42\n", "\n", "\n", "\n", "\n", "45\n", "If\n", "\n", "\n", "\n", "33--45\n", "\n", "\n", "\n", "\n", "35\n", "Name\n", "\n", "\n", "\n", "34--35\n", "\n", "\n", "\n", "\n", "38\n", "Eq\n", "\n", "\n", "\n", "34--38\n", "\n", "\n", "\n", "\n", "39\n", "Name\n", "\n", "\n", "\n", "34--39\n", "\n", "\n", "\n", "\n", "36\n", ""b"\n", "\n", "\n", "\n", "35--36\n", "\n", "\n", "\n", "\n", "37\n", "Load\n", "\n", "\n", "\n", "35--37\n", "\n", "\n", "\n", "\n", "40\n", ""c"\n", "\n", "\n", "\n", "39--40\n", "\n", "\n", "\n", "\n", "41\n", "Load\n", "\n", "\n", "\n", "39--41\n", "\n", "\n", "\n", "\n", "43\n", "Constant\n", "\n", "\n", "\n", "42--43\n", "\n", "\n", "\n", "\n", "44\n", ""isosceles #2"\n", "\n", "\n", "\n", "43--44\n", "\n", "\n", "\n", "\n", "46\n", "Compare\n", "\n", "\n", "\n", "45--46\n", "\n", "\n", "\n", "\n", "54\n", "Return\n", "\n", "\n", "\n", "45--54\n", "\n", "\n", "\n", "\n", "57\n", "Return\n", "\n", "\n", "\n", "45--57\n", "\n", "\n", "\n", "\n", "47\n", "Name\n", "\n", "\n", "\n", "46--47\n", "\n", "\n", "\n", "\n", "50\n", "Eq\n", "\n", "\n", "\n", "46--50\n", "\n", "\n", "\n", "\n", "51\n", "Name\n", "\n", "\n", "\n", "46--51\n", "\n", "\n", "\n", "\n", "48\n", ""a"\n", "\n", "\n", "\n", "47--48\n", "\n", "\n", "\n", "\n", "49\n", "Load\n", "\n", "\n", "\n", "47--49\n", "\n", "\n", "\n", "\n", "52\n", ""c"\n", "\n", "\n", "\n", "51--52\n", "\n", "\n", "\n", "\n", "53\n", "Load\n", "\n", "\n", "\n", "51--53\n", "\n", "\n", "\n", "\n", "55\n", "Constant\n", "\n", "\n", "\n", "54--55\n", "\n", "\n", "\n", "\n", "56\n", ""isosceles #3"\n", "\n", "\n", "\n", "55--56\n", "\n", "\n", "\n", "\n", "58\n", "Constant\n", "\n", "\n", "\n", "57--58\n", "\n", "\n", "\n", "\n", "59\n", ""scalene"\n", "\n", "\n", "\n", "58--59\n", "\n", "\n", "\n", "" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "triangle_source = inspect.getsource(triangle)\n", "triangle_ast = ast.parse(triangle_source)\n", "show_ast(triangle_ast)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Now suppose one wants to identify all `triangle` branches and their conditions using static analysis. You would traverse the AST, searching for `If` nodes, and take their first child (the condition). This is easy as well:" ] }, { "cell_type": "code", "execution_count": 14, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:51.017507Z", "iopub.status.busy": "2024-01-18T17:30:51.017375Z", "iopub.status.idle": "2024-01-18T17:30:51.019934Z", "shell.execute_reply": "2024-01-18T17:30:51.019396Z" }, "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "def collect_conditions(tree):\n", " conditions = []\n", "\n", " def traverse(node):\n", " if isinstance(node, ast.If):\n", " cond = ast.unparse(node.test).strip()\n", " conditions.append(cond)\n", "\n", " for child in ast.iter_child_nodes(node):\n", " traverse(child)\n", "\n", " traverse(tree)\n", " return conditions" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Here are the four `if` conditions occurring in the `triangle()` code:" ] }, { "cell_type": "code", "execution_count": 15, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:51.021582Z", "iopub.status.busy": "2024-01-18T17:30:51.021442Z", "iopub.status.idle": "2024-01-18T17:30:51.024105Z", "shell.execute_reply": "2024-01-18T17:30:51.023769Z" }, "slideshow": { "slide_type": "subslide" } }, "outputs": [ { "data": { "text/plain": [ "['a == b', 'b == c', 'b == c', 'a == c']" ] }, "execution_count": 15, "metadata": {}, "output_type": "execute_result" } ], "source": [ "collect_conditions(triangle_ast)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Not only can we extract individual program elements, we can also change them at will and convert the tree back into source code. Program transformations (say, for instrumentation or mutation analysis) are a breeze. The above code took five minutes to write. Again, try that in Java or C." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "slide" } }, "source": [ "## Symbolic Reasoning in Python: There's a Package for That\n", "\n", "Let's get back to testing. We have shown how to extract conditions from code. To reach a particular location in the `triangle()` function, one needs to find a solution for the _path conditions_ leading to that branch. To reach the last line in `triangle()` (the `'scalene'` branch), we have to find a solution for \n", "$$a \\ne b \\land b \\ne c \\land a \\ne c$$\n", "\n", "\n", "We can make use of a _constraint_ solver for this, such as Microsoft's [_Z3_ solver](https://github.com/Z3Prover/z3):" ] }, { "cell_type": "code", "execution_count": 16, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:51.025835Z", "iopub.status.busy": "2024-01-18T17:30:51.025717Z", "iopub.status.idle": "2024-01-18T17:30:51.037576Z", "shell.execute_reply": "2024-01-18T17:30:51.037208Z" }, "slideshow": { "slide_type": "skip" } }, "outputs": [], "source": [ "import z3 # type: ignore" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "Let us use Z3 to find a solution for the `'scalene'` branch condition:" ] }, { "cell_type": "code", "execution_count": 17, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:51.039337Z", "iopub.status.busy": "2024-01-18T17:30:51.039243Z", "iopub.status.idle": "2024-01-18T17:30:51.043006Z", "shell.execute_reply": "2024-01-18T17:30:51.042679Z" }, "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "a = z3.Int('a')\n", "b = z3.Int('b')\n", "c = z3.Int('c')" ] }, { "cell_type": "code", "execution_count": 18, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:51.044521Z", "iopub.status.busy": "2024-01-18T17:30:51.044434Z", "iopub.status.idle": "2024-01-18T17:30:51.054626Z", "shell.execute_reply": "2024-01-18T17:30:51.054245Z" }, "slideshow": { "slide_type": "fragment" } }, "outputs": [ { "data": { "text/html": [ "sat" ], "text/plain": [ "sat" ] }, "execution_count": 18, "metadata": {}, "output_type": "execute_result" } ], "source": [ "s = z3.Solver()\n", "s.add(z3.And(a > 0, b > 0, c > 0)) # Triangle edges are positive\n", "s.add(z3.And(a != b, b != c, a != c)) # Our condition\n", "s.check()" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Z3 has shown us that there is a solution (\"sat\" = \"satisfiable\"). Let us get one:" ] }, { "cell_type": "code", "execution_count": 19, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:51.056404Z", "iopub.status.busy": "2024-01-18T17:30:51.056279Z", "iopub.status.idle": "2024-01-18T17:30:51.059082Z", "shell.execute_reply": "2024-01-18T17:30:51.058843Z" }, "slideshow": { "slide_type": "fragment" } }, "outputs": [ { "data": { "text/html": [ "[a = 1, c = 3, b = 2]" ], "text/plain": [ "[a = 1, c = 3, b = 2]" ] }, "execution_count": 19, "metadata": {}, "output_type": "execute_result" } ], "source": [ "m = s.model()\n", "m" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "We can use this solution right away for testing the `triangle()` function and find that it indeed covers the `'scalene'` branch. The method `as_long()` converts the Z3 results into numerical values." ] }, { "cell_type": "code", "execution_count": 20, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:51.060476Z", "iopub.status.busy": "2024-01-18T17:30:51.060375Z", "iopub.status.idle": "2024-01-18T17:30:51.062644Z", "shell.execute_reply": "2024-01-18T17:30:51.062366Z" }, "slideshow": { "slide_type": "fragment" } }, "outputs": [ { "data": { "text/plain": [ "'scalene'" ] }, "execution_count": 20, "metadata": {}, "output_type": "execute_result" } ], "source": [ "triangle(m[a].as_long(), m[b].as_long(), m[c].as_long())" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "slide" } }, "source": [ "## A Symbolic Test Generator\n", "\n", "With what we have seen, we can now build a _symbolic test generator_ – a tool that attempts to systematically create test inputs that cover all paths. Let us find all conditions we need to solve, by exploring all paths in the tree. We turn these paths to Z3 format right away:" ] }, { "cell_type": "code", "execution_count": 21, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:51.064053Z", "iopub.status.busy": "2024-01-18T17:30:51.063951Z", "iopub.status.idle": "2024-01-18T17:30:51.066738Z", "shell.execute_reply": "2024-01-18T17:30:51.066506Z" }, "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "def collect_path_conditions(tree):\n", " paths = []\n", "\n", " def traverse_if_children(children, context, cond):\n", " old_paths = len(paths)\n", " for child in children:\n", " traverse(child, context + [cond])\n", " if len(paths) == old_paths:\n", " paths.append(context + [cond])\n", "\n", " def traverse(node, context):\n", " if isinstance(node, ast.If):\n", " cond = ast.unparse(node.test).strip()\n", " not_cond = \"z3.Not(\" + cond + \")\"\n", "\n", " traverse_if_children(node.body, context, cond)\n", " traverse_if_children(node.orelse, context, not_cond)\n", "\n", " else:\n", " for child in ast.iter_child_nodes(node):\n", " traverse(child, context)\n", "\n", " traverse(tree, [])\n", "\n", " return [\"z3.And(\" + \", \".join(path) + \")\" for path in paths]" ] }, { "cell_type": "code", "execution_count": 22, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:51.068193Z", "iopub.status.busy": "2024-01-18T17:30:51.068081Z", "iopub.status.idle": "2024-01-18T17:30:51.070328Z", "shell.execute_reply": "2024-01-18T17:30:51.070072Z" }, "slideshow": { "slide_type": "subslide" } }, "outputs": [ { "data": { "text/plain": [ "['z3.And(a == b, b == c)',\n", " 'z3.And(a == b, z3.Not(b == c))',\n", " 'z3.And(z3.Not(a == b), b == c)',\n", " 'z3.And(z3.Not(a == b), z3.Not(b == c), a == c)',\n", " 'z3.And(z3.Not(a == b), z3.Not(b == c), z3.Not(a == c))']" ] }, "execution_count": 22, "metadata": {}, "output_type": "execute_result" } ], "source": [ "path_conditions = collect_path_conditions(triangle_ast)\n", "path_conditions" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Now all we need to do is to feed these constraints into Z3. We see that we easily cover all branches:" ] }, { "cell_type": "code", "execution_count": 23, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:51.071779Z", "iopub.status.busy": "2024-01-18T17:30:51.071674Z", "iopub.status.idle": "2024-01-18T17:30:51.093566Z", "shell.execute_reply": "2024-01-18T17:30:51.093252Z" }, "slideshow": { "slide_type": "subslide" } }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "[a = 1, c = 1, b = 1] equilateral\n", "[c = 2, a = 1, b = 1] isosceles #1\n", "[c = 2, a = 1, b = 2] isosceles #2\n", "[c = 1, a = 1, b = 2] isosceles #3\n", "[c = 3, a = 1, b = 2] scalene\n" ] } ], "source": [ "for path_condition in path_conditions:\n", " s = z3.Solver()\n", " s.add(a > 0, b > 0, c > 0)\n", " eval(f\"s.check({path_condition})\")\n", " m = s.model()\n", " print(m, triangle(m[a].as_long(), m[b].as_long(), m[c].as_long()))" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Success! We have covered all branches of the triangle program!" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "Now, the above is still very limited – and tailored to the capabilities of the `triangle()` code. A full implementation would actually\n", "\n", "* translate entire Python conditions into Z3 syntax (if possible),\n", "* handle more control flow constructs such as returns, assertions, exceptions\n", "* and half a million things more (loops, calls, you name it)\n", "\n", "Some of these may not be supported by the Z3 theories." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "To make it easier for a constraint solver to find solutions, you could also provide _concrete values_ observed from earlier executions that already are known to reach specific paths in the program. Such concrete values would be gathered from the tracing mechanisms above, and boom: you would have a pretty powerful and scalable concolic (concrete-symbolic) test generator." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Now, the above might take you a day or two, and as you expand your test generator beyond `triangle()`, you will add more and more features. The nice part is that every of these features you will invent might actually be a research contribution – something nobody has thought of before. Whatever idea you might have: you can quickly implement it and try it out in a prototype. And again, this will be orders of magnitude faster than for conventional languages." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "slide" } }, "source": [ "## Things that will not work\n", "\n", "Python has a reputation for being hard to analyze statically, and this is true; its dynamic nature makes it hard for traditional static analysis to exclude specific behaviors. \n", "\n", "We see Python as a great language for prototyping automated testing and dynamic analysis techniques, and as a good language to illustrate _lightweight_ static and symbolic analysis techniques that would be used to _guide_ and _support_ other techniques (say, generating software tests).\n", "\n", "But if you want to _prove_ specific properties (or the absence thereof) by static analysis of code only, Python is a challenge, to say the least; and there are areas for which we would definitely _warn_ against using it. " ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "### (No) Type Checking\n", "\n", "Using Python to demonstrate _static type checking_ will be suboptimal (to say the least) because, well, Python programs typically do not come with type annotations. You _can_, of course, annotate variables with types, as we assume in the [chapter on Symbolic Fuzzing](SymbolicFuzzer.ipynb):" ] }, { "cell_type": "code", "execution_count": 24, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:51.095263Z", "iopub.status.busy": "2024-01-18T17:30:51.095142Z", "iopub.status.idle": "2024-01-18T17:30:51.096937Z", "shell.execute_reply": "2024-01-18T17:30:51.096681Z" }, "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "def typed_triangle(a: int, b: int, c: int) -> str:\n", " return triangle(a, b, c)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Most real-world Python code will not be annotated with types, though. While you can also _retrofit them_, as discussed in [our chapter on dynamic invariants](DynamicInvariants.ipynb), Python simply is not a good domain to illustrate type checking. If you want to show the beauty and usefulness of type checking, use a strongly typed language like Java, ML, or Haskell." ] }, { "attachments": {}, "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "### (No) Program Proofs\n", "\n", "Python is a highly dynamic language in which you can change _anything_ at runtime. It is no problem assigning different types to a variable, as in" ] }, { "cell_type": "code", "execution_count": 25, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:51.098581Z", "iopub.status.busy": "2024-01-18T17:30:51.098473Z", "iopub.status.idle": "2024-01-18T17:30:51.100011Z", "shell.execute_reply": "2024-01-18T17:30:51.099775Z" }, "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "x = 42\n", "x = \"a string\" # type: ignore" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "or change the existence (and scope) of a variable depending on some runtime condition:" ] }, { "cell_type": "code", "execution_count": 26, "metadata": { "execution": { "iopub.execute_input": "2024-01-18T17:30:51.101409Z", "iopub.status.busy": "2024-01-18T17:30:51.101316Z", "iopub.status.idle": "2024-01-18T17:30:51.103124Z", "shell.execute_reply": "2024-01-18T17:30:51.102875Z" }, "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "p1, p2 = True, False\n", "\n", "if p1:\n", " x = 42\n", "if p2:\n", " del x\n", "\n", "# Does x exist at this point?" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "Such properties make symbolic reasoning on code (including static analysis and type checking) much harder, if not outright impossible. If you need lightweight static and symbolic analysis techniques to _guide_ other techniques (say, test generation), then imprecision may not hurt much. But if you want to derive _guarantees_ from your code, do not use Python as test subject; again, strongly statically typed languages like Java/ML/Haskell (or some very restricted toy language) are much better grounds for experimentation." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "This does not mean that languages like Python should _not_ be statically checked. On the contrary, the widespread usage of Python calls loudly for better static checking tools. But if you want to teach or research static and symbolic techniques, we definitely would not use Python as our language of choice." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "slide" } }, "source": [ "## The Virtues of Prototyping\n", "\n", "One neat thing about prototyping (with Python or whatever) is that it allows you to fully focus on your _approach_, rather than on the infrastructure. Very obviously, this is useful for _teaching_ – you can use examples as the ones above in a lecture to very quickly communicate essential techniques of program analysis and test generation.\n", "\n", "But prototyping has more advantages. A Jupyter Notebook (like this one) documents how you developed your approach, together with examples, experiments, and rationales – and still focusing on the essentials. If you write a tool the \"classical\" way, you will eventually deliver thousands of lines of code that do everything under the sun, but only once you have implemented everything will you know whether things actually work. This is a huge risk, and if you still have to change things, you will have to refactor things again and again. Furthermore, for anyone who will work on that code later, it will take days, if not weeks, to re-extract the basic idea of the approach, as it will be buried under loads and loads of infrastructure and refactorings.\n", "\n", "Our consequence at this point is that we now implement new ideas _twice_:\n", "\n", "* First, we implement things as a notebook (as this one), experimenting with various approaches and parameters until we get them right.\n", "\n", "* Only once we have the approach right, and if we have confidence that it works, we reimplement it in a tool that works on large scale programs. This can still take weeks to months, but at least we know we are on a good path.\n", "\n", "Incidentally, it may well be that the original notebooks will have a longer life, as they are simpler, better documented, and capture the gist of our novel idea. And this is how several of the notebooks in this book came to be." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "slide" } }, "source": [ "## Try it out!\n", "\n", "All the code examples above can be run by you – and changed as you like! From the Web page, the easiest way is to go to \"Resources $\\rightarrow$ Edit as Notebook\", and you can experiment with the original Jupyter Notebook right within your browser. (Use `Shift` + `Return` to execute code.)\n", "\n", "From the \"Resources\" menu, you can also download the Python code (`.py`) to run it within a Python environment, or download the notebook (`.ipynb`) to run it within Jupyter – and again, change them as you like. If you want to run this code on your own machine, you will need the following packages:\n", "\n", "```\n", "pip install showast\n", "pip install z3-solver\n", "```\n", "\n", "Enjoy!" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "slide" } }, "source": [ "## Lessons Learned\n", "\n", "**Python** is a great language for prototyping testing and debugging tools:\n", "\n", "* In Python, dynamic analysis and static analysis are extremely easy to implement.\n", "* Python provides an enormous infrastructure for parsing, handling programs as trees, and constraint solving.\n", "* These can make you develop new techniques within _hours_ instead of weeks.\n", "\n", "Python is _not_ recommended as a domain for pure symbolic code analysis, though.\n", "\n", "* There is little to no static typing\n", "* The language is highly dynamic with little to no static guarantees\n", "\n", "However, even a potentially _unsound_ symbolic analysis can still guide test generation – and this again is very easy to build.\n", "\n", "**Jupyter Notebooks** (using Python or other languages) are great for _prototyping_:\n", "\n", "* Notebooks document the gist of your approach, including examples and experiments.\n", "* This is great for teaching, communication, and even documentation.\n", "* Doing experiments on prototypes early reduces risks for later large-scale implementations.\n" ] }, { "cell_type": "markdown", "metadata": { "button": false, "new_sheet": false, "run_control": { "read_only": false }, "slideshow": { "slide_type": "slide" } }, "source": [ "## Next Steps\n", "\n", "If you want to see more examples of us using Python for prototyping – have a look at [this book](index.ipynb)! Specifically,\n", "\n", "* see how we develop [fuzzers](Fuzzer.ipynb) step by step;\n", "* see how we use [dynamic analysis to check coverage](Coverage.ipynb); or\n", "* see how we analyze Python code for [concolic](ConcolicFuzzer.ipynb) and [symbolic](SymbolicFuzzer.ipynb) and fuzzing.\n", "\n", "There's lots to learn – enjoy the read!" ] }, { "attachments": {}, "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "slide" } }, "source": [ "## Background\n", "\n", "The _triangle problem_ is adapted from \"The Art of Software Testing\" by Myers and Sandler \\cite{Myers2004}. It is an allegedly simple problem but which reveals a surprising depth when you think about all the things that might go wrong.\n", "\n", "The _Z3 solver_ we use in this chapter was developed at Microsoft Research under the lead of Leonardo de Moura and Nikolaj Bjørner \\cite{z3}. It is one of the most powerful and most popular solvers." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "slide" } }, "source": [ "## Exercises" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "### Exercise 1: Features! Features!\n", "\n", "Our path collector is still very limited. Things that do not work include\n", "\n", "* Complex conditions, such as boolean operators. Python operators `a and b` need to be translated to Z3 syntax `z3.And(a, b)`.\n", "* Early returns. After `if A: return`, the condition `not A` must hold for the following statements.\n", "* Assignments.\n", "* Loops.\n", "* Function calls.\n", "\n", "The more of these you implement, the closer you will get to a full-fledged symbolic test generator for Python. But at some point, _your prototype may not be a prototype anymore_, and then, Python may no longer be the best language to use. Find a good moment when it is time to switch from a prototypical to a production tool." ] } ], "metadata": { "ipub": { "bibliography": "fuzzingbook.bib" }, "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.2" }, "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": 4 }