notebooks/calculator.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "d5adce86-289b-440e-ab1b-434d311a2064",
   "metadata": {},
   "source": [
    "# Avicenna: A Semantic Debugging Tool\n",
    "\n",
    "**Avicenna** is a debugging tool designed to automatically determine the causes and conditions of program failures. This notebook provides an overview and demonstration of its capabilities.\n",
    "\n",
    "**Avicenna** leverages both generative and predictive models to satisfy constraints over grammar elements and detect relations of input elements.\n",
    "Our tool uses the [ISLa](https://github.com/rindPHI/isla) specification language to express complex failure circumstances as predicates over input elements.\n",
    "**Avicenna** learns input properties that are common across failing inputs and employs a feedback loop to refine the current debugging diagnoses by systematic experimentation.\n",
    "The result is crisp and precise diagnoses that closely match those determined by human experts, offering a significant advancement in the realm of automated debugging.\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "04a99f0c",
   "metadata": {
    "collapsed": false,
    "jupyter": {
     "outputs_hidden": false
    }
   },
   "source": [
    "### Example Subject: The Calculator"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b00eaed3-902c-4ad0-9cfa-3c9035b1e0c4",
   "metadata": {},
   "source": [
    "To illustrate **Avicenna**’s capabilities, we start with a quick motivating example. First, let us introduce our program under test: The Calculator.\n",
    "\n",
    "The Calculator is a Python program designed to evaluate various mathematical expressions, including arithmetic equations and trigonometric functions:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "919e8138",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2023-08-14T11:57:51.786291Z",
     "start_time": "2023-08-14T11:57:51.784851Z"
    },
    "collapsed": false,
    "jupyter": {
     "outputs_hidden": false
    }
   },
   "outputs": [],
   "source": [
    "import math\n",
    "\n",
    "def calculator(inp: str) -> float:\n",
    "    \"\"\"\n",
    "        A simple calculator function that can evaluate arithmetic expressions\n",
    "        and perform basic trigonometric functions and square root calculations.\n",
    "    \"\"\"\n",
    "    return eval(\n",
    "        str(inp), {\"sqrt\": math.sqrt, \"sin\": math.sin, \"cos\": math.cos, \"tan\": math.tan}\n",
    "    )"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7413a804-e669-47a9-b214-3f7e616c01c6",
   "metadata": {},
   "source": [
    "We can test the calculator with some sample inputs:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "dca1c28f",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2023-08-14T11:57:52.337069Z",
     "start_time": "2023-08-14T11:57:52.332936Z"
    },
    "collapsed": false,
    "jupyter": {
     "outputs_hidden": false
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "0.999993677717667\n"
     ]
    }
   ],
   "source": [
    "# Evaluating the cosine of 2π\n",
    "print(calculator('cos(6*3.141)'))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "35836c3f",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2023-08-14T11:57:52.525719Z",
     "start_time": "2023-08-14T11:57:52.517857Z"
    },
    "collapsed": false,
    "jupyter": {
     "outputs_hidden": false
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "6.0\n"
     ]
    }
   ],
   "source": [
    "# Calculating the square root of 36\n",
    "print(calculator('sqrt(6*6)'))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3201ede8-258d-46a0-be3a-89b29bb5ce45",
   "metadata": {
    "collapsed": false,
    "jupyter": {
     "outputs_hidden": false
    }
   },
   "source": [
    "Each of these calls to the calculator will evaluate the provided string as a mathematical expression, and print the result."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "852fcda1-b517-472b-a385-17398dc98032",
   "metadata": {},
   "source": [
    "### Defining an Oracle to classify failure-inducing Inputs"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "99f946a8-b409-4468-a1c5-a22e7ae290cd",
   "metadata": {
    "collapsed": false,
    "jupyter": {
     "outputs_hidden": false
    }
   },
   "source": [
    "To identify bugs in The Calculator, we'll implement an oracle function. This function tests inputs and categorizes them as producing expected behavior (`OracleResult.NO_BUG`) or a bug (`OracleResult.BUG`):\n",
    "\n",
    "We import the `OracleResult` enumerated type from the `avicenna` library."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "c7597350",
   "metadata": {
    "collapsed": false,
    "jupyter": {
     "outputs_hidden": false
    }
   },
   "outputs": [],
   "source": [
    "from avicenna.oracle import OracleResult"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ec2c07c6-1b8a-4fd9-b1ed-a3706856bb2e",
   "metadata": {},
   "source": [
    "This allows us to define a function called **oracle**, which acts as an intermediary to handle and classify exceptions produced by the calculator function when given a certain input."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "aeeea7a6-fdeb-4190-ad94-c6b32a0fee0a",
   "metadata": {},
   "outputs": [],
   "source": [
    "# Make sure you use the OracleResult from the evogfuzz library\n",
    "from avicenna.oracle import OracleResult\n",
    "\n",
    "def oracle(inp: str):\n",
    "    \"\"\"\n",
    "    This function serves as an oracle or intermediary that catches and handles exceptions \n",
    "    generated by the 'calculator' function.\n",
    "    It aims to determine whether an input triggers a bug in the 'calculator' function.\n",
    "\n",
    "    Args:\n",
    "        inp (str): The input string to be passed to the 'calculator' function.\n",
    "\n",
    "    Returns:\n",
    "        OracleResult: An enumerated type 'OracleResult' indicating the outcome of the function execution.\n",
    "            - OracleResult.NO_BUG: Returned if the calculator function executes without any exception\n",
    "            - OracleResult.BUG: Returned if the calculator function raises a ValueError exception, indicating a potential bug.\n",
    "    \"\"\"\n",
    "    try:\n",
    "        calculator(inp)\n",
    "    except ValueError as e:\n",
    "        return OracleResult.BUG\n",
    "    return OracleResult.NO_BUG"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "28be7de0-b444-42fa-af27-d376290b3992",
   "metadata": {},
   "source": [
    "This **oracle** function is used in the context of debugging to determine the behavior of various inputs on the program under test (in our case the _calculator_). When the calculator function behaves as expected (i.e., no exceptions occur), the **oracle** function returns `OracleResult.NO_BUG`. However, when the `calculator` function raises an unexpected exception, the **oracle** interprets this as a potential bug in the `calculator` and returns `OracleResult.BUG`."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "899d3f00-bd2c-47d9-a72a-12a2cf8eed05",
   "metadata": {},
   "source": [
    "We can see this in action by testing a few initial inputs:\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "6169db57-19f0-41b2-bdca-6c57778da5fc",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "sqrt(1)                        NO_BUG\n",
      "cos(912)                       NO_BUG\n",
      "tan(4)                         NO_BUG\n",
      "sqrt(-3)                       BUG\n"
     ]
    }
   ],
   "source": [
    "initial_inputs = ['sqrt(1)', 'cos(912)', 'tan(4)', 'sqrt(-3)']\n",
    "\n",
    "for inp in initial_inputs:\n",
    "    print(inp.ljust(30), oracle(inp))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3e027cc5-4e49-46d0-bb5e-55fb85bd9451",
   "metadata": {},
   "source": [
    "We see that `sqrt(-3)` results in the failure of our calculator program. \n",
    "\n",
    "In the following steps, we'll leverage Avicenna to pinpoint the root cause of this bug.\n",
    "We'll employ Avicenna's capabilities to identify the root cause of the bug and provide potential fixes.\n",
    "This will involve defining the input structure for our calculator and initializing Avicenna with the appropriate grammar, sample inputs, and oracle function."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bd7ff24f-c7dc-4452-8ae0-152a87940e5e",
   "metadata": {},
   "source": [
    "### Defining the Input Format\n",
    "\n",
    "First, we need to define the input format of the calculator with a grammar:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "49b05a17-b35b-4288-80c5-da6b17aa1085",
   "metadata": {},
   "outputs": [],
   "source": [
    "import string\n",
    "\n",
    "grammar = {\n",
    "    \"<start>\": [\"<arith_expr>\"],\n",
    "    \"<arith_expr>\": [\"<function>(<number>)\"],\n",
    "    \"<function>\": [\"sqrt\", \"sin\", \"cos\", \"tan\"],\n",
    "    \"<number>\": [\"<maybe_minus><onenine><maybe_digits><maybe_frac>\"],\n",
    "    \"<maybe_minus>\": [\"\", \"-\"],\n",
    "    \"<onenine>\": [str(num) for num in range(1, 10)],\n",
    "    \"<digit>\": list(string.digits),\n",
    "    \"<maybe_digits>\": [\"\", \"<digits>\"],\n",
    "    \"<digits>\": [\"<digit>\", \"<digit><digits>\"],\n",
    "    \"<maybe_frac>\": [\"\", \".<digits>\"],\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "46fea60f-1174-4503-84de-5c6f5f7a2b4a",
   "metadata": {
    "jp-MarkdownHeadingCollapsed": true
   },
   "source": [
    "The grammar provides a structured way to generate valid input strings for our calculator program. It defines patterns and rules that dictate how different elements can be combined to form syntactically correct mathematical expressions. Here's a breakdown of the key components of the grammar:\n",
    "\n",
    "- `<start>`: The entry point for generating an expression. It signifies where the creation of an arithmetic expression begins.\n",
    "\n",
    "- `<arith_expr>`: Represents a general arithmetic expression. For simplicity in this example, it's defined to consist of a function applied to a number, like `sin(3)` or `sqrt(9)`.\n",
    "\n",
    "- `<function>`: Enumerates the mathematical functions our calculator can handle, including square root and trigonometric operations like sine, cosine, and tangent.\n",
    "\n",
    "- `<number>`: Describes valid numbers for our calculator. This includes:\n",
    "  - Negative values (denoted by `<maybe_minus>` which can be an empty string or a minus sign).\n",
    "  - Whole numbers ranging from 1 to 9 (given by `<onenine>`).\n",
    "  - Sequences of digits (represented by `<maybe_digits>` and `<digits>`).\n",
    "  - Fractions or decimal numbers (expressed by `<maybe_frac>`).\n",
    "\n",
    "This grammar acts as a blueprint, guiding the systematic generation of test cases for our calculator. By defining the rules and structures of valid inputs, it ensures that the generated expressions are meaningful and relevant for our debugging exercise."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7e6a4039-f196-4d9e-a78e-297a5bc31587",
   "metadata": {},
   "source": [
    "### Using Avicenna"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d8eb8ae0-d771-4dd7-ac01-3c7498b3e428",
   "metadata": {},
   "source": [
    "With the oracle, the grammar, and a failure-inducing input, we can use **Avicenna** to automatically infer properties over inputs, validate hypotheses, generate additional test cases, and finally producing precise and expressive diagnoses for the failure conditions."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "fde0b640-6478-4cdc-830b-767320106784",
   "metadata": {},
   "outputs": [],
   "source": [
    "from avicenna.avicenna import Avicenna\n",
    "\n",
    "avicenna = Avicenna(\n",
    "    grammar,\n",
    "    oracle,\n",
    "    initial_inputs,\n",
    ")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "05c470a6-8379-4356-bf15-3d62356ea776",
   "metadata": {},
   "outputs": [],
   "source": [
    "from typing import List, Tuple\n",
    "from isla.language import Formula\n",
    "\n",
    "diagnosis: Tuple[Formula, float, float] = avicenna.explain()\n",
    "# Avicenna returns a List of learned ISla Formula and the corresponding precision and recall"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5764aa74-d964-47f0-8fbd-1e869209b320",
   "metadata": {},
   "source": [
    "In the code above, we've created an instance of the Avicenna class and executed the debugging process by invoking the `explain()` method.\n",
    "Avicenna will utilize its feedback loop to systematically probe and test the Calculator program, identify the root cause of the bug on the analysis of the bug's behavior."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3840e61e-424d-42d7-8a9b-d75b6d80ef91",
   "metadata": {},
   "source": [
    "This output is a symbolic representation -- ISLa Constraints -- of the root cause of the failure detected by Avicenna in the Calculator program. Here's a breakdown of what it means:\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "3442a3f0-c61e-4ebe-9dd6-453047817c28",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Avicenna determined the following constraints to describe the failure circumstances:\n",
      "\n",
      "(forall <number> elem in start:\n",
      "   (<= (str.to.int elem) (str.to.int \"-1\")) and\n",
      "exists <function> elem_0 in start:\n",
      "  (= elem_0 \"sqrt\"))\n",
      "Avicenna calculated a precision of 100.00% and a recall of 100.00%\n",
      "\n"
     ]
    }
   ],
   "source": [
    "from isla.language import ISLaUnparser\n",
    "\n",
    "print(f\"Avicenna determined the following constraints to describe the failure circumstances:\\n\")\n",
    "\n",
    "print(ISLaUnparser(diagnosis[0]).unparse())\n",
    "print(f\"Avicenna calculated a precision of {diagnosis[1]*100:.2f}% and a recall of {diagnosis[2]*100:.2f}%\", end=\"\\n\\n\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "74dd0647-83a2-4a6d-bab0-7d0ca367c1c0",
   "metadata": {},
   "source": [
    "This output, expressed in first-order logic, is saying:\n",
    "\n",
    "- For all numbers (elements of type `<number>` in the grammar), if the integer representation of the number is less than or equal to -1 (`<= (str.to.int elem) (str.to.int \"-1\")`), and\n",
    "- There exists a function (an element of type `<function>` in the grammar) that equals to \"sqrt\" (`= elem_0 \"sqrt\"`),\n",
    "\n",
    "then a bug is likely to occur.\n",
    "\n",
    "In plain English, the output is indicating that the failure in our Calculator program occurs when trying to take the square root (`sqrt`) of a negative number (a number less than or equal to -1). \n",
    "\n",
    "This is consistent with our expectations, since the square root of a negative number is not defined in the realm of real numbers. Consequently, Python's `math.sqrt()` function, which we've used in our Calculator program, throws a `ValueError` when given a negative number as input.\n",
    "\n",
    "With this information, we can address the issue in our Calculator program to prevent crashes when dealing with such inputs. We might decide to handle such errors gracefully or implement support for complex numbers, depending on the requirements of our program.\n",
    "\n",
    "Remember, these results are generated based on the information provided to Avicenna, such as the grammar and the oracle function, as well as the results of Avicenna's systematic testing of the Calculator program. So the more accurate and comprehensive these inputs are, the more helpful Avicenna's outputs will be.\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "00ae2217-8489-44e4-944a-acbfacbdfcf9",
   "metadata": {},
   "source": [
    "## Generating More Inputs from the diagnoses"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "25defc1b-7ece-431c-be62-8753cf5e9c05",
   "metadata": {},
   "source": [
    "Now that we obtained the ISLa formulas that describe the failure circumstances, we can use them to generate more inputs triggering that exact same behavior. To do so, we use the ISLaSolver:"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "549f2f94-7d6f-40c6-ad38-b3f30a9093f9",
   "metadata": {},
   "source": [
    "The function `ISLaSolver.solve()` attempts to compute a solution to the given ISLa formula. It returns that solution, if any. This function can be called repeatedly to obtain more solutions until one of two exception types is raised: A `StopIteration` indicates that no more solution can be found; a `TimeoutError` is raised if a timeout occurred. After that, an exception will be raised every time."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b7a6eb3b-adf6-4f9a-867f-7fc50bf5154d",
   "metadata": {},
   "source": [
    "<div class=\"alert alert-info\">\n",
    "[Info]: For more information about the <a href=\"https://github.com/rindPHI/isla\">ISLa Sepcification language</a> and the <b>ISLaSolver</b>, have a look at the extensive <a href=\"https://isla.readthedocs.io/en/latest/index.html\">Documentation</a>.\n",
    "</div>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "99d942ad-a59c-46c5-aa06-33a0b9ff7487",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "sqrt(-93.92)                   BUG\n",
      "sqrt(-5)                       BUG\n",
      "sqrt(-268057.4)                BUG\n",
      "sqrt(-616)                     BUG\n",
      "sqrt(-12)                      BUG\n",
      "sqrt(-70.0)                    BUG\n",
      "sqrt(-32.4)                    BUG\n",
      "sqrt(-4.0)                     BUG\n",
      "sqrt(-8)                       BUG\n",
      "sqrt(-6)                       BUG\n",
      "sqrt(-94.0)                    BUG\n",
      "sqrt(-61.7)                    BUG\n",
      "sqrt(-3.2)                     BUG\n",
      "sqrt(-70)                      BUG\n",
      "sqrt(-7.8569)                  BUG\n",
      "sqrt(-6)                       BUG\n",
      "sqrt(-1.0)                     BUG\n",
      "sqrt(-43.37)                   BUG\n",
      "sqrt(-3.1819496)               BUG\n",
      "sqrt(-887)                     BUG\n",
      "sqrt(-1.4)                     BUG\n",
      "sqrt(-812987)                  BUG\n",
      "sqrt(-93.5)                    BUG\n",
      "sqrt(-760)                     BUG\n",
      "sqrt(-6.4540)                  BUG\n",
      "sqrt(-3.71361)                 BUG\n",
      "sqrt(-51.3)                    BUG\n",
      "sqrt(-2419.902)                BUG\n",
      "sqrt(-4)                       BUG\n",
      "sqrt(-87427)                   BUG\n",
      "sqrt(-101)                     BUG\n",
      "sqrt(-7.6)                     BUG\n",
      "sqrt(-4010)                    BUG\n",
      "sqrt(-455)                     BUG\n",
      "sqrt(-7)                       BUG\n",
      "sqrt(-6.6)                     BUG\n",
      "sqrt(-4)                       BUG\n",
      "sqrt(-798)                     BUG\n",
      "sqrt(-4.0)                     BUG\n",
      "sqrt(-3)                       BUG\n",
      "sqrt(-275)                     BUG\n",
      "sqrt(-3.94)                    BUG\n",
      "sqrt(-520.6)                   BUG\n",
      "sqrt(-81.348)                  BUG\n",
      "sqrt(-744)                     BUG\n",
      "sqrt(-4.4588)                  BUG\n",
      "sqrt(-1)                       BUG\n",
      "sqrt(-903.73909)               BUG\n",
      "sqrt(-6.26)                    BUG\n",
      "sqrt(-8.7)                     BUG\n",
      "sqrt(-6.7)                     BUG\n",
      "sqrt(-46)                      BUG\n",
      "sqrt(-8)                       BUG\n",
      "sqrt(-9.1315)                  BUG\n",
      "sqrt(-6.894)                   BUG\n",
      "sqrt(-8.2)                     BUG\n",
      "sqrt(-86.12)                   BUG\n",
      "sqrt(-149)                     BUG\n",
      "sqrt(-1.67)                    BUG\n",
      "sqrt(-3.3406)                  BUG\n"
     ]
    }
   ],
   "source": [
    "from isla.solver import ISLaSolver\n",
    "\n",
    "for diagnosis in avicenna.get_equivalent_best_formulas():\n",
    "    solver = ISLaSolver(\n",
    "        grammar,\n",
    "        formula=diagnosis[0],\n",
    "        enable_optimized_z3_queries=False)\n",
    "    \n",
    "    for _ in range(20):\n",
    "        try:\n",
    "            inp = solver.solve()\n",
    "            print(str(inp).ljust(30), oracle(inp))\n",
    "        except StopIteration:\n",
    "            continue"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "29c6b2fe-5fea-4674-8277-45c1a63afaa2",
   "metadata": {},
   "source": [
    "## Summary:\n",
    "\n",
    "In this notebook, we introduced **Avicenna**, a powerful semantic debugging tool designed to automatically determine the causes and conditions of program failures. Through the example of a simple calculator program, we showcased the following:\n",
    "\n",
    "1. **Setting Up an Oracle**: We defined an intermediary function, termed as an 'oracle', which classifies the exceptions produced by our program into expected and unexpected categories.\n",
    "2. **Grammar Definition**: A structured blueprint for generating valid inputs to the calculator was established.\n",
    "3. **Automated Debugging with Avicenna**: Using the provided grammar, initial test cases, and the oracle, Avicenna systematically probed our calculator program and identified potential root causes for observed failures.\n",
    "4. **Interpreting Results**: We decoded Avicenna's output, learning that the failure in our calculator program is triggered when computing the square root of a negative number."
   ]
  }
 ],
 "metadata": {
  "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.9"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}