code/ILP-joern-ey-into-aleph.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Aleph\n",
    "\n",
    "The aim of this notebook is to use the Aleph system to perform ILP and learn a rule to identify buffer overflows. The rule should be of the form:\n",
    "\n",
    "```\n",
    "bug(AllocNode, WriteNode) :- predictateA, predicateB, ..., predicateZ.\n",
    "```"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "import pandas as pd\n",
    "import tempfile\n",
    "import subprocess\n",
    "import graph_visualisation as gv"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Data Preparation\n",
    "\n",
    "We start by loading in our reduced set of buffer overflow examples, and their prolog representations. **If you're just reading, skip to the \"Running Examples with Aleph\" section.**"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>testcase_ID</th>\n",
       "      <th>filename</th>\n",
       "      <th>code</th>\n",
       "      <th>flaw</th>\n",
       "      <th>flaw_loc</th>\n",
       "      <th>bug</th>\n",
       "      <th>code_length</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>62804</td>\n",
       "      <td>000/062/804/CWE121_Stack_Based_Buffer_Overflow...</td>\n",
       "      <td>/* TEMPLATE GENERATED TESTCASE FILE\\nFilename:...</td>\n",
       "      <td>CWE-121</td>\n",
       "      <td>33</td>\n",
       "      <td>False</td>\n",
       "      <td>1722</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>62821</td>\n",
       "      <td>000/062/821/CWE121_Stack_Based_Buffer_Overflow...</td>\n",
       "      <td>/* TEMPLATE GENERATED TESTCASE FILE\\nFilename:...</td>\n",
       "      <td>CWE-121</td>\n",
       "      <td>35</td>\n",
       "      <td>False</td>\n",
       "      <td>1808</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>62852</td>\n",
       "      <td>000/062/852/CWE121_Stack_Based_Buffer_Overflow...</td>\n",
       "      <td>/* TEMPLATE GENERATED TESTCASE FILE\\nFilename:...</td>\n",
       "      <td>CWE-121</td>\n",
       "      <td>30</td>\n",
       "      <td>False</td>\n",
       "      <td>1674</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>62853</td>\n",
       "      <td>000/062/853/CWE121_Stack_Based_Buffer_Overflow...</td>\n",
       "      <td>/* TEMPLATE GENERATED TESTCASE FILE\\nFilename:...</td>\n",
       "      <td>CWE-121</td>\n",
       "      <td>33</td>\n",
       "      <td>False</td>\n",
       "      <td>2396</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>62854</td>\n",
       "      <td>000/062/854/CWE121_Stack_Based_Buffer_Overflow...</td>\n",
       "      <td>/* TEMPLATE GENERATED TESTCASE FILE\\nFilename:...</td>\n",
       "      <td>CWE-121</td>\n",
       "      <td>33</td>\n",
       "      <td>False</td>\n",
       "      <td>2414</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "   testcase_ID                                           filename  \\\n",
       "0        62804  000/062/804/CWE121_Stack_Based_Buffer_Overflow...   \n",
       "1        62821  000/062/821/CWE121_Stack_Based_Buffer_Overflow...   \n",
       "2        62852  000/062/852/CWE121_Stack_Based_Buffer_Overflow...   \n",
       "3        62853  000/062/853/CWE121_Stack_Based_Buffer_Overflow...   \n",
       "4        62854  000/062/854/CWE121_Stack_Based_Buffer_Overflow...   \n",
       "\n",
       "                                                code     flaw  flaw_loc  \\\n",
       "0  /* TEMPLATE GENERATED TESTCASE FILE\\nFilename:...  CWE-121        33   \n",
       "1  /* TEMPLATE GENERATED TESTCASE FILE\\nFilename:...  CWE-121        35   \n",
       "2  /* TEMPLATE GENERATED TESTCASE FILE\\nFilename:...  CWE-121        30   \n",
       "3  /* TEMPLATE GENERATED TESTCASE FILE\\nFilename:...  CWE-121        33   \n",
       "4  /* TEMPLATE GENERATED TESTCASE FILE\\nFilename:...  CWE-121        33   \n",
       "\n",
       "     bug  code_length  \n",
       "0  False         1722  \n",
       "1  False         1808  \n",
       "2  False         1674  \n",
       "3  False         2396  \n",
       "4  False         2414  "
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "ilp_data = pd.read_csv(\"../data/ilp_dataset.csv.gz\")\n",
    "ilp_data = ilp_data.drop(\"Unnamed: 0\", axis=1)\n",
    "ilp_data.head()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>testcase_ID</th>\n",
       "      <th>flaw</th>\n",
       "      <th>bug</th>\n",
       "      <th>code_length</th>\n",
       "      <th>tree</th>\n",
       "      <th>source_map</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>-232086</td>\n",
       "      <td>CWE-122</td>\n",
       "      <td>True</td>\n",
       "      <td>1625</td>\n",
       "      <td>% START: Generated Prolog\\n% NODE PROPERTIES \\...</td>\n",
       "      <td>% CODE\\nsource_code(bad_232086_id_1_f_l_c_, \"p...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>-232012</td>\n",
       "      <td>CWE-122</td>\n",
       "      <td>True</td>\n",
       "      <td>1619</td>\n",
       "      <td>% START: Generated Prolog\\n% NODE PROPERTIES \\...</td>\n",
       "      <td>% CODE\\nsource_code(bad_232012_id_0_f_l_c_, \"p...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>-62917</td>\n",
       "      <td>CWE-121</td>\n",
       "      <td>True</td>\n",
       "      <td>1622</td>\n",
       "      <td>% START: Generated Prolog\\n% NODE PROPERTIES \\...</td>\n",
       "      <td>% CODE\\nsource_code(bad_62917_id_0_f_l_c_, \"p1...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>-62916</td>\n",
       "      <td>CWE-121</td>\n",
       "      <td>True</td>\n",
       "      <td>1649</td>\n",
       "      <td>% START: Generated Prolog\\n% NODE PROPERTIES \\...</td>\n",
       "      <td>% CODE\\nsource_code(bad_62916_id_1_f_l_c_, \"p1...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>-62915</td>\n",
       "      <td>CWE-121</td>\n",
       "      <td>True</td>\n",
       "      <td>1638</td>\n",
       "      <td>% START: Generated Prolog\\n% NODE PROPERTIES \\...</td>\n",
       "      <td>% CODE\\nsource_code(bad_62915_id_0_f_l_c_, \"p1...</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "   testcase_ID     flaw   bug  code_length  \\\n",
       "0      -232086  CWE-122  True         1625   \n",
       "1      -232012  CWE-122  True         1619   \n",
       "2       -62917  CWE-121  True         1622   \n",
       "3       -62916  CWE-121  True         1649   \n",
       "4       -62915  CWE-121  True         1638   \n",
       "\n",
       "                                                tree  \\\n",
       "0  % START: Generated Prolog\\n% NODE PROPERTIES \\...   \n",
       "1  % START: Generated Prolog\\n% NODE PROPERTIES \\...   \n",
       "2  % START: Generated Prolog\\n% NODE PROPERTIES \\...   \n",
       "3  % START: Generated Prolog\\n% NODE PROPERTIES \\...   \n",
       "4  % START: Generated Prolog\\n% NODE PROPERTIES \\...   \n",
       "\n",
       "                                          source_map  \n",
       "0  % CODE\\nsource_code(bad_232086_id_1_f_l_c_, \"p...  \n",
       "1  % CODE\\nsource_code(bad_232012_id_0_f_l_c_, \"p...  \n",
       "2  % CODE\\nsource_code(bad_62917_id_0_f_l_c_, \"p1...  \n",
       "3  % CODE\\nsource_code(bad_62916_id_1_f_l_c_, \"p1...  \n",
       "4  % CODE\\nsource_code(bad_62915_id_0_f_l_c_, \"p1...  "
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "prolog = pd.read_csv(\"../data/ilp_prolog_data.csv.gz\")\n",
    "prolog = prolog.drop(\"Unnamed: 0\", axis=1)\n",
    "prolog.head()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Next, we do a bunch of nasty stuff to find the particular nodes where the alloc and write nodes are in each prolog tree. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "/usr/local/lib/python3.6/dist-packages/pandas/core/indexing.py:190: SettingWithCopyWarning: \n",
      "A value is trying to be set on a copy of a slice from a DataFrame\n",
      "\n",
      "See the caveats in the documentation: http://pandas.pydata.org/pandas-docs/stable/indexing.html#indexing-view-versus-copy\n",
      "  self._setitem_with_indexer(indexer, value)\n"
     ]
    }
   ],
   "source": [
    "juliet = pd.read_csv(\"../data/buffer_overflow_data.csv.gz\")\n",
    "juliet.drop(\"Unnamed: 0\", axis=1)\n",
    "\n",
    "prolog['source_code'] = ''\n",
    "prolog['flaw_loc'] = 0\n",
    "prolog['bad_code'] = ''\n",
    "\n",
    "for i in range(len(prolog)):\n",
    "    label = prolog.iloc[i].testcase_ID == juliet.testcase_ID\n",
    "    prolog['source_code'].iloc[i] = juliet.loc[label].iloc[0].code\n",
    "    prolog['flaw_loc'].iloc[i] = juliet.loc[label].iloc[0].flaw_loc\n",
    "    \n",
    "for i in range(len(prolog)):\n",
    "    loc =  prolog.iloc[i].flaw_loc\n",
    "    testcase_ID = prolog.iloc[i].testcase_ID\n",
    "    if testcase_ID < 0:\n",
    "        prolog['bad_code'].iloc[i] = prolog.iloc[i].source_code.split('\\n')[loc-1].strip()[0:-1]\n",
    "    else:\n",
    "        prolog['bad_code'].iloc[i] = prolog.loc[prolog.testcase_ID == -testcase_ID].iloc[0].bad_code\n",
    "        \n",
    "good_examples = prolog[prolog['bug'] == False]\n",
    "bad_examples = prolog[prolog['bug'] == True]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [],
   "source": [
    "def extract_node_ids(tree):\n",
    "    nodes = set()\n",
    "    \n",
    "    in_ast_section = False\n",
    "    \n",
    "    for line in tree.split('\\n'):\n",
    "        line = line.strip()\n",
    "        \n",
    "        if line == '% AST':\n",
    "            in_ast_section = True\n",
    "        \n",
    "        if line == '% CFG':\n",
    "            in_ast_section = False\n",
    "            \n",
    "        if line == '% REF':\n",
    "            in_ast_section = False\n",
    "        \n",
    "        if in_ast_section and not line.startswith(\"%\"):\n",
    "            parent, child = line[4:-2].split(\", \")\n",
    "            nodes.add(parent)\n",
    "            nodes.add(child)\n",
    "            \n",
    "    return nodes"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [],
   "source": [
    "# good nodes_g\n",
    "nodes_g = set()\n",
    "\n",
    "for i in range(len(good_examples)):\n",
    "    good_nodes = extract_node_ids(good_examples.iloc[i].tree)\n",
    "    nodes_g = set.union(nodes_g,good_nodes)\n",
    "\n",
    "    \n",
    "# bad nodes_b\n",
    "nodes_b = set()\n",
    "\n",
    "for i in range(len(bad_examples)):\n",
    "    bad_nodes = extract_node_ids(bad_examples.iloc[i].tree)\n",
    "    nodes_b = set.union(nodes_b,bad_nodes)\n",
    "\n",
    "nodes = set.union(nodes_g,nodes_b)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [],
   "source": [
    "def find_bug_id(good_examples, i = 0):\n",
    "    tree = good_examples.source_map.iloc[i]\n",
    "    parents = []\n",
    "    children = []\n",
    "    in_code_section = False\n",
    "    temp = 0\n",
    "    for line in tree.split('\\n'):\n",
    "        line = line.strip()\n",
    "        \n",
    "        if line == '% CODE':\n",
    "            in_code_section = True\n",
    "        \n",
    "        if in_code_section and not line.startswith(\"%\"):\n",
    "            try:\n",
    "                #import pdb; pdb.set_trace()\n",
    "                parent, child = line[12:-3].split(', \"')\n",
    "                parents.append(parent)\n",
    "                children.append(child)\n",
    "            except:\n",
    "                temp +=1\n",
    "    zipbObj = zip(children, parents)\n",
    "    bug_node = dict(zipbObj)\n",
    "    \n",
    "    loc = good_examples.iloc[i].flaw_loc\n",
    "    source_code = good_examples.iloc[i].bad_code\n",
    "\n",
    "    return bug_node[source_code]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [],
   "source": [
    "bad_node = []\n",
    "good_node = []\n",
    "for i in range(20):\n",
    "    bad_node.append(find_bug_id(bad_examples,i))\n",
    "    good_node.append(find_bug_id(good_examples,i))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "['(good_62913, good_62913_id_105_f_memmove_14_c_l_81_c_11_)',\n",
       " '(good_62854, good_62854_id_211_f_memcpy_03_c_l_24_c_0_)',\n",
       " '(bad_62867, bad_62867_id_32_f_l_c_)',\n",
       " '(good_62821, good_62821_id_126_f_loop_18_c_l_36_c_17_)',\n",
       " '(bad_62868, bad_62868_id_115_f_l_50_c_0_)']"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "node_and_tree = []\n",
    "for node in nodes:\n",
    "    start, end = node.split('_id')\n",
    "    node_and_tree.append('(' +start+ ', ' +node+ ')')\n",
    "\n",
    "node_and_tree[0:5]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [],
   "source": [
    "node_tree_types = [\n",
    "    'node_in_tree'+ node_tree +'.' for node_tree in node_and_tree\n",
    "]\n",
    "\n",
    "node_types = [\n",
    "    'node('+ node_id +').' for node_id in nodes\n",
    "]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [],
   "source": [
    "def extract_tree_ids(tree):\n",
    "    line = tree.split('\\n')[2]\n",
    "    line = line.strip()\n",
    "    line = line.split('(')[1]\n",
    "    tree_id = line.split('_id')[0]\n",
    "\n",
    "    return tree_id"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [],
   "source": [
    "tree_ids = []\n",
    "for tree in prolog.tree:\n",
    "    tree_ids.append(extract_tree_ids(tree))\n",
    "\n",
    "trees = [\n",
    "    'tree('+ tree_label +').' for tree_label in tree_ids\n",
    "]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Here we try to locate the buggy nodes. For each test case this will be:\n",
    "  1. Location where the memory is _allocated_.\n",
    "  2. Location where the memory is _written to_.\n",
    "  \n",
    "We already have code above to find the latter. Can we find the first as well?"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [],
   "source": [
    "bad_write_nodes = bad_node\n",
    "good_write_nodes = good_node"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [],
   "source": [
    "# this code is horrible sorry. if you need to figure out what it does speak to Dan.\n",
    "\n",
    "alloc_source_maps = [\n",
    "    line\n",
    "    for source_map in prolog['source_map']\n",
    "    for line in source_map.split(\"\\n\")\n",
    "    if 'data =' in line.lower() and 'alloc' in line.lower()\n",
    "]\n",
    "bad_alloc_nodes = [\n",
    "    source_map.strip(\"source_code(\").split(\",\")[0]\n",
    "    for source_map in alloc_source_maps\n",
    "    if 'bad' in source_map\n",
    "]\n",
    "\n",
    "good_alloc_nodes = [\n",
    "    source_map.strip(\"source_code(\").split(\",\")[0]\n",
    "    for source_map in alloc_source_maps\n",
    "    if 'good' in source_map\n",
    "]\n",
    "\n",
    "positive_examples = []\n",
    "for write_node in bad_write_nodes:\n",
    "    # find the alloc node which has a line number before the write\n",
    "    write_node_id = write_node.strip(\"source_code(\").split(\",\")[0] + \"_\"\n",
    "    write_line = int(write_node_id.split(\"_\")[-4])\n",
    "    \n",
    "    testcase_id = '_'.join(write_node_id.split(\"_\")[0:2])\n",
    "    \n",
    "    potential_alloc_nodes = [node for node in bad_alloc_nodes if testcase_id in node]\n",
    "    for alloc_node in potential_alloc_nodes:\n",
    "        alloc_node_id = alloc_node.strip(\"source_code(\").split(\",\")[0] + \"_\"\n",
    "        alloc_line = int(alloc_node_id.split(\"_\")[-4])\n",
    "        \n",
    "        if alloc_line <= write_line:\n",
    "            positive_examples.append(\n",
    "                \"bug({},{}).\".format(alloc_node_id, write_node_id)\n",
    "            )\n",
    "            \n",
    "negative_examples = []\n",
    "for write_node in good_write_nodes:\n",
    "    # find the alloc node which has a line number before the write\n",
    "    write_node_id = write_node.strip(\"source_code(\").split(\",\")[0] + \"_\"\n",
    "    write_line = int(write_node_id.split(\"_\")[-4])\n",
    "    \n",
    "    testcase_id = '_'.join(write_node_id.split(\"_\")[0:2])\n",
    "    \n",
    "    potential_alloc_nodes = [node for node in good_alloc_nodes if testcase_id in node]\n",
    "    for alloc_node in potential_alloc_nodes:\n",
    "        alloc_node_id = alloc_node.strip(\"source_code(\").split(\",\")[0] + \"_\"\n",
    "        alloc_line = int(alloc_node_id.split(\"_\")[-4])\n",
    "        \n",
    "        if alloc_line <= write_line:\n",
    "            negative_examples.append(\n",
    "                \"bug({},{}).\".format(alloc_node_id, write_node_id)\n",
    "            )"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Running Examples with Aleph\n",
    "\n",
    "**Now for the interesting part.** Below is our template to create our scripts for aleph to use."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [],
   "source": [
    "def filter_lines_by_testcase(string, testcases):\n",
    "    return '\\n'.join([\n",
    "        line for line in string.split(\"\\n\")  if any(\n",
    "            str(testcase) in line for testcase in testcases\n",
    "        ) or not (\"good_\" in line or \"bad_\" in line)\n",
    "    ])\n",
    "\n",
    "\n",
    "def make_aleph_scripts(header, positive_examples, negative_examples, testcases=None):\n",
    "    script_template = \"\"\"\n",
    "{header}\n",
    "\n",
    ":- discontiguous ast/2.\n",
    ":- discontiguous cfg/2.\n",
    ":- discontiguous ancestor/2.\n",
    ":- discontiguous runs_before/2.\n",
    ":- discontiguous assignment/1.\n",
    ":- discontiguous compMemberAccess/1.\n",
    ":- discontiguous ref/2.\n",
    ":- discontiguous sizeOf/1.\n",
    ":- discontiguous alloc/1.\n",
    ":- discontiguous writeToPointer/1.\n",
    ":- discontiguous alloc_doesnt_check_sizeOf/1.\n",
    ":- discontiguous pointer/1.\n",
    ":- discontiguous sizeOfInt/1.\n",
    ":- discontiguous array10/1.\n",
    ":- discontiguous voidPointer/1.\n",
    "\n",
    "%% Trees\n",
    "{trees}\n",
    "\n",
    "%% Types\n",
    "{types}\n",
    "\n",
    "%% Background knowledge\n",
    "{bg_knowledge}\n",
    "\n",
    "\n",
    "%% Rules for background knowledge\n",
    "writeToPointer(A) :- ast(A,B), assignment(A), compMemberAccess(B). \n",
    "\n",
    "ancestor(A,C) :- ast(A,B), ancestor(B,C).\n",
    "ancestor(A,C) :- ast(A,C).\n",
    "\n",
    "runs_before(A,C) :- cfg(A,B), runs_before(B,C).\n",
    "runs_before(A,C) :- cfg(A,C).\n",
    "\n",
    "contains_sizeOf_call(A) :- ancestor(A, B), sizeof(B).\n",
    "alloc_doesnt_check_sizeOf(A) :- alloc(A), not(contains_sizeOf_call(A)).\n",
    "\n",
    "same_tree(A,B) :- node_in_tree(T,A), node_in_tree(T,B).\n",
    "    \"\"\"\n",
    "    script_bg = script_template.format(\n",
    "        header = header,\n",
    "        trees =  '\\n'.join(trees),\n",
    "        types = '\\n'.join(node_tree_types + node_types),\n",
    "        bg_knowledge = '\\n'.join(prolog['tree'])\n",
    "    )\n",
    "\n",
    "    script_template_pos = \"\"\"\n",
    "\n",
    "%% positive examples\n",
    "{positive_examples}\n",
    "\n",
    "    \"\"\"\n",
    "    \n",
    "    script_template_neg = \"\"\"\n",
    "    \n",
    "%% negative examples\n",
    "{negative_examples}\n",
    "\n",
    "    \"\"\"\n",
    "    script_pos = script_template_pos.format(\n",
    "        positive_examples='\\n '.join(positive_examples)\n",
    "    )\n",
    "    \n",
    "    script_neg = script_template_neg.format(\n",
    "        negative_examples='\\n '.join(negative_examples)\n",
    "    )\n",
    "    \n",
    "    # keep all testcases unless a testcases set is given in fn call\n",
    "    if testcases:\n",
    "        # remove all lines not related to this testcase\n",
    "        script_bg = filter_lines_by_testcase(script_bg)\n",
    "        script_pos = filter_lines_by_testcase(script_pos)\n",
    "        script_neg = filter_lines_by_testcase(script_neg)\n",
    "        \n",
    "    return script_bg, script_pos, script_neg"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Experimenting with aleph:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "header = \"\"\"\n",
    "\n",
    "% body\n",
    ":- mode(*,runs_before(+node,+node)).\n",
    ":- mode(*,ancestor(+node,-node)).\n",
    ":- mode(*,ancestor(-node,+node)).\n",
    "\n",
    ":- mode(*, ref(+node,-node)).\n",
    ":- mode(*, ref(-node,+node)).\n",
    "\n",
    ":- mode(*, sizeOf(+node)).\n",
    ":- mode(*, alloc(+node)).\n",
    ":- mode(*, writeToPointer(+node)).\n",
    "\n",
    ":- mode(*, alloc_doesnt_check_sizeOf(+node)).\n",
    "\n",
    ":- mode(*, pointer(+node)).\n",
    ":- mode(*, sizeOfInt(+node)).\n",
    ":- mode(*, array10(+node)).\n",
    ":- mode(*, voidPointer(+node)).\n",
    "\n",
    "% determinations\n",
    ":- determination(bug/2, ancestor/2).\n",
    ":- determination(bug/2, runs_before/2).\n",
    ":- determination(bug/2, ref/2).\n",
    ":- determination(bug/2, sizeOf/1).\n",
    ":- determination(bug/2, alloc/1).\n",
    ":- determination(bug/2, writeToPointer/1).\n",
    ":- determination(bug/2, alloc_doesnt_check_sizeOf/1).\n",
    ":- determination(bug/2, pointer/1).\n",
    ":- determination(bug/2, sizeOfInt/1).\n",
    ":- determination(bug/2, array10/1).\n",
    ":- determination(bug/2, voidPointer/1).\n",
    "\n",
    "\"\"\"\n",
    "\n",
    "script_bg, script_pos, script_neg = make_aleph_scripts(\n",
    "    header,\n",
    "    positive_examples,\n",
    "    negative_examples,\n",
    ")\n",
    "\n",
    "runner_script = \"\"\"\n",
    ":- working_directory(_, \"/tmp/aleph_scripts\"),\n",
    "[library(acuity)],\n",
    "read_all(aleph_scripts),\n",
    "set(interactive,true),\n",
    "set(depth,30),\n",
    "set(clauselength,20),\n",
    "set(clauses,10),\n",
    "set(minpos,2),\n",
    "induce,\n",
    "halt.\n",
    "\"\"\"\n",
    "\n",
    "!mkdir -p /tmp/aleph_scripts\n",
    "\n",
    "\n",
    "with open(\"/tmp/runner.pl\", \"w\") as f:\n",
    "    f.write(runner_script)\n",
    "\n",
    "with open(\"/tmp/aleph_scripts/aleph_scripts.b\", \"w\") as f:\n",
    "    f.write(script_bg)\n",
    "\n",
    "with open(\"/tmp/aleph_scripts/aleph_scripts.f\", \"w\") as f:\n",
    "    f.write(script_pos)\n",
    "    \n",
    "with open(\"/tmp/aleph_scripts/aleph_scripts.n\", \"w\") as f:\n",
    "    f.write(script_neg)\n",
    "    \n",
    "!swipl -s /tmp/runner.pl > output.log"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "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"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}