camera_pipe.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "d72d21b7",
   "metadata": {},
   "source": [
    "# Section 4: Memory safety results: `camera_pipe`\n",
    "In Section 4 on the memory safety results, we talk about the `camera_pipe` experiment:\n",
    "> For camera_pipe, VerCors gives a verification failure. It could not prove a\n",
    "> loop_invariant, but after simplifying parts of the generated C program not related\n",
    "> to this specific invariant, it leads to a successful verification. This indicates\n",
    "> that the program is too complex for the underlying solvers. We also coded this\n",
    "> example in similar Pvl code instead of C, which verifies in 193s.\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f5a2f47b",
   "metadata": {},
   "source": [
    "# Logfile of `camera_pipe`\n",
    "If you look you look at the log file  you will see the following (`logs/camera_pipe_mem.c.txt`, after running the experiments)\n",
    "```    \n",
    "[------------------------------------------------------------------\n",
    "  504            loop_invariant (\\forall* int _f3_s0_v0_v6_forall, int _f3_s0_v1_v3_forall, int _f3_s0_v0_v0_forall, int _f3_s0_v1_v1_forall; ((((((((0 <= _f3_s0_v1_v1_forall) && (_f3_s0_v1_v1_forall < 5)) && (0 <= _f3_s0_v0_v0_forall)) && (_f3_s0_v0_v0_forall < 161)) && (0 <= _f3_s0_v1_v3_forall)) && (_f3_s0_v1_v3_forall < 2)) && (0 <= _f3_s0_v0_v6_forall)) && (_f3_s0_v0_v6_forall < 16)) && (((_f3_s0_v0_v0_forall*16) + _f3_s0_v0_v6_forall) <= 2567); Perm(&_f3[((((_f3_s0_v1_v1_forall + _processed_s0_v1_v3_v3)*2) + _f3_s0_v1_v3_forall)*2568) + ((_f3_s0_v0_v0_forall*16) + _f3_s0_v0_v6_forall)], 1\\1));\n",
    "------------------------------------------------------------------------------------------------------]\n",
    "...\n",
    "The offset to the pointer may be outside the bounds of the allocated memory area that the pointer is in. (https://utwente.nl/vercors#ptrBlock)\n",
    "======================================\n",
    "```\n",
    "\n",
    "Indicating that line 504 is incorrect. In the file `camera_pipe/camera_pipe_mem_v2.c` we altered the file from `camera_pipe/camera_pipe_mem.c`, to comment out some annotations, and some removed some parts of the code, irrelevant for this annotation. Below we verify this file"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "72aa3c7e",
   "metadata": {},
   "outputs": [],
   "source": [
    "# This leads to `[INFO] Verification completed successfully.`\n",
    "!/vercors/vct --dev-assert-timeout 0 --backend-option --prover=Z3-API --silicon-quiet --no-infer-heap-context-into-frame --dev-total-timeout 600 camera_pipe/camera_pipe_mem_v2.c"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "33f512d5",
   "metadata": {},
   "source": [
    "Additionally, we also encoded the same program directly in PVL, instead of C. This can be found in `camera_pipe/camera_pipe_mem.pvl`. Simarly, this file does verify:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "607849c9",
   "metadata": {},
   "outputs": [],
   "source": [
    "# Leads to succesfull verification\n",
    "!time /vercors/vct --dev-assert-timeout 0 --backend-option --prover=Z3-API --silicon-quiet --no-infer-heap-context-into-frame --dev-total-timeout 600 camera_pipe/camera_pipe_mem.pvl"
   ]
  }
 ],
 "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.12"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}