getStats.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "/*\n",
    " * Copyright 2021 ConsenSys AG.\n",
    " *\n",
    " * Licensed under the Apache License, Version 2.0 (the \"License\"); you may \n",
    " * not use this file except in compliance with the License. You may obtain \n",
    " * a copy of the License at http://www.apache.org/licenses/LICENSE-2.0\n",
    " *\n",
    " * Unless required by applicable law or agreed to in writing, software dis-\n",
    " * tributed under the License is distributed on an \"AS IS\" BASIS, WITHOUT \n",
    " * WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the \n",
    " * License for the specific language governing permissions and limitations \n",
    " * under the License.\n",
    " */"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Notebook description\n",
    "\n",
    "This notebook contains some basic processing to automate the collection of statistics relating to the Dafny files.\n",
    "By creating functions to perform analysis of Dafny files, additional results can easily be added to the pandas dataframe.\n",
    "The use of a pandas dataframe provides many options for visualisation and the data can easily by stored in a csv.\n",
    "The data can also easily be supplemented with timestamps to faciliate time series analysis.\n",
    "\n",
    "This file is a working file and will be converted to a python script in due course."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# TODO: Reformat function documentation to standard style used within this repo"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Libraries"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [],
   "source": [
    "# import libraries\n",
    "import os\n",
    "import subprocess\n",
    "\n",
    "import pandas as pd\n",
    "import re\n",
    "import numpy as np\n",
    "\n",
    "import time\n",
    "import shutil"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "# find *.dfy files, within a given local repo path\n",
    "# this function will search all subfolders of dirName\n",
    "# a sorted list of files is returned\n",
    "def getListOfDafnyFiles(dirName,exclude_folders=[]):\n",
    "    listOfFile = os.listdir(dirName)\n",
    "    allFiles = list()\n",
    "    for entry in listOfFile:\n",
    "        fullPath = os.path.join(dirName, entry)\n",
    "        # if entry is a directory then append the list of files in this directory to allFiles\n",
    "        if os.path.isdir(fullPath):\n",
    "            if os.path.abspath(fullPath) not in exclude_folders:\n",
    "                allFiles = allFiles + getListOfDafnyFiles(fullPath, exclude_folders)\n",
    "        # else append file only if it is a Dafny file\n",
    "        else:\n",
    "            if entry.endswith(\".dfy\"):\n",
    "                allFiles.append(fullPath)\n",
    "    return sorted(allFiles)   "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [],
   "source": [
    "# find folders within the repo that have *.dfy files\n",
    "# a sorted list of folders is returned (i.e. full path of each folder)\n",
    "def getListOfDafnyFolders(dafnyFiles):\n",
    "    listOfDirectories = list()\n",
    "    for file in dafnyFiles:\n",
    "        listOfDirectories.append(os.path.dirname(file))\n",
    "    return sorted(list(set(listOfDirectories)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [],
   "source": [
    "# get folder for an individual dafny file\n",
    "# i.e. for the full path of a dafny file, the filename and repo path are striped\n",
    "def getFolder(repo, dafny_file):\n",
    "    repo_path, folder = os.path.dirname(dafny_file).split(repo,1)\n",
    "    return folder"
   ]
  },
  {
   "source": [
    "## File processing functions"
   ],
   "cell_type": "code",
   "metadata": {},
   "execution_count": 3,
   "outputs": []
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "tags": []
   },
   "outputs": [],
   "source": [
    "# test the getListOfDafnyFiles, getListOfDafnyFolders and getFolder functions\n",
    "# local repo path needs to be set prior to running the tests and `if False` \n",
    "# must be changed to `if True`\n",
    "if False:\n",
    "    repo_directory = \"/home/roberto/projects_offline/lavoro/consensys/content/eth2.0-dafny-for-stats\"\n",
    "    exclude_folders_rel_path = [\"src/dafny/libraries/integers\"]\n",
    "\n",
    "    exclude_folders_full_path = [os.path.join(repo_directory,f) for f in exclude_folders]\n",
    "\n",
    "    print(\"Test getListOfDafnyFiles: \")\n",
    "    files = getListOfDafnyFiles(repo_directory, exclude_folders_full_path)\n",
    "    for i in files:\n",
    "        print(i)\n",
    "    print(\"Length of returned list: \", len(files))\n",
    "\n",
    "    print(\"Test getListOfDafnyFolders: \")\n",
    "    directories = getListOfDafnyFolders(files)\n",
    "    for i in directories:\n",
    "        print(i)\n",
    "    print(\"Length of returned list: \", len(directories))\n",
    "\n",
    "    print(\"Test getFolder for each file in files: \")\n",
    "    for file in files:\n",
    "        print(getFolder(repo_directory, file))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Functions to collect statistics"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Test file processing functions"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [],
   "source": [
    "# count the number of \"function methods\" in a given dafny file\n",
    "# this function uses a subprocess call\n",
    "# an alternative method would be to read and search the file directly\n",
    "def getFunctions(dafny_file):\n",
    "    cmd = \"cat \" + dafny_file +\"| grep function | grep method | wc -l\"\n",
    "    result = subprocess.run(['/bin/bash', '-i', '-c', cmd], stdout=subprocess.PIPE)\n",
    "    return result.stdout.strip().decode('ascii')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [],
   "source": [
    "# count the number of \"lemmas\" in a given dafny file\n",
    "# this function uses a subprocess call\n",
    "# an alternative method would be to read and search the file directly\n",
    "def getLemmas(dafny_file):\n",
    "    cmd = \"cat \" + dafny_file +\"| grep lemma | wc -l\"\n",
    "    result = subprocess.run(['/bin/bash', '-i', '-c', cmd], stdout=subprocess.PIPE)\n",
    "    return result.stdout.strip().decode('ascii')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [],
   "source": [
    "# count the number of ghost (= function and lemmas) processes\n",
    "# ignores function methods\n",
    "# to be referred to as \"Theorems\" in the data display\n",
    "def getGhost(dafny_file):\n",
    "    tmp_file = open(dafny_file, \"r\")\n",
    "    count = 0\n",
    "    for line in tmp_file.readlines():\n",
    "        if line.strip().startswith((\"function\", \"lemma\")):\n",
    "            if not line.strip().startswith(\"function method\"):\n",
    "                count += 1\n",
    "                #print(line)\n",
    "    tmp_file.close()\n",
    "    return count"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [],
   "source": [
    "# count the number of non-ghost ()= function methods and methods and predicates) processes\n",
    "# to be referred to as \"Implementations\" in the data display\n",
    "def getNonGhost(dafny_file):\n",
    "    tmp_file = open(dafny_file, \"r\")\n",
    "    count = 0\n",
    "    for line in tmp_file.readlines():\n",
    "        if line.strip().startswith((\"function method\", \"method\", \"predicate\")):\n",
    "            count += 1\n",
    "            #print(line)\n",
    "\n",
    "    tmp_file.close()\n",
    "    return count"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [],
   "source": [
    "# count the number of lines of code\n",
    "# the count occurs after the dafny file is printed used the compiler\n",
    "# the count also occurs after this output has been cleaned\n",
    "def getLoC(dafny_file):\n",
    "    show_ghost = True\n",
    "    executable = \"dafny\"\n",
    "    args  = [] \n",
    "    args += ['/rprint:-']\n",
    "    args += [\"/noAutoReq\"]\n",
    "    args += [\"/noVerify\"]\n",
    "    args += [\"/nologo\"]\n",
    "    args += [\"/env:0\"]\n",
    "    if show_ghost:\n",
    "        args += [\"/printMode:NoIncludes\"]\n",
    "    else:\n",
    "        args += [\"/printMode:NoGhost\"]\n",
    "    args += [dafny_file]\n",
    "    cmd = ' '.join([executable] + args)\n",
    "    result = subprocess.run(['/bin/bash', '-i', '-c', cmd], stdout=subprocess.PIPE)\n",
    "    output = result.stdout.decode('ascii')\n",
    "    #print(type(result.stdout.decode('ascii')))\n",
    "    #print(result.stdout.decode('ascii'))\n",
    "\n",
    "    #remove this section once code has be tested OR comment out\n",
    "    #tmp_file = open(\"tmp.txt\", \"w\")\n",
    "    #tmp_file.write(result.stdout.decode('ascii'))\n",
    "    #tmp_file.close()\n",
    "    ######---------------------\n",
    "\n",
    "    count = 0\n",
    "    for line in output.splitlines():\n",
    "        # clean output i.e. remove comment at start and verifier status\n",
    "        if line.startswith((\"Dafny program verifier finished\", \"//\")):\n",
    "            #print(i)\n",
    "            pass\n",
    "        else:\n",
    "            if line.strip():\n",
    "                count += 1\n",
    "                #print(line)\n",
    "    #print(\"#LoC: \", count)\n",
    "    return count"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [],
   "source": [
    "# count the number of lines included in the license comment\n",
    "# assumes license comment is at the start of the file and is of format /* ... */\n",
    "# assumes that it has been confirmed that the file has a license comment\n",
    "def getLicenseLineCount(dafny_file):\n",
    "    tmp_file = open(dafny_file, \"r\")\n",
    "    count = 0\n",
    "    flag = 0\n",
    "    for line in tmp_file.readlines():\n",
    "        tmp_line = line.strip()\n",
    "        cleaned = ' '.join(i for i in tmp_line.split() if i not in [\"//\", \"/*\", \"/**\", \"*\", \"*/\"])\n",
    "        if (not flag) and (tmp_line.startswith(\"/*\")):\n",
    "            if cleaned:\n",
    "                count += 1\n",
    "            flag = 1\n",
    "        elif flag:\n",
    "            if cleaned:\n",
    "                count += 1\n",
    "            if tmp_line.startswith(\"*/\"):\n",
    "                tmp_file.close()\n",
    "                return count"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [],
   "source": [
    "# count the number of lines of documentation\n",
    "# don't include license comment or empty comment lines\n",
    "def getDocumentation(dafny_file):\n",
    "    tmp_file = open(dafny_file, \"r\")\n",
    "    count = 0\n",
    "    license_flag = 0\n",
    "    for line in tmp_file.readlines():\n",
    "        tmp_line = line.strip()\n",
    "        if tmp_line.startswith((\"//\", \"/*\", \"/**\", \"*\", \"*/\")):\n",
    "            cleaned = ' '.join(i for i in tmp_line.split() if i not in [\"//\", \"/*\", \"/**\", \"*\", \"*/\"])\n",
    "            if cleaned:\n",
    "                #print(cleaned)\n",
    "                count += 1\n",
    "                #print(line)\n",
    "        if tmp_line.startswith(\"* Copyright 2021 ConsenSys Software Inc.\"):\n",
    "            license_flag = 1\n",
    "\n",
    "    tmp_file.close()\n",
    "    if license_flag:\n",
    "        count -= getLicenseLineCount(dafny_file)\n",
    "        #print(getLicenseLineCount(dafny_file))\n",
    "    return count"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [],
   "source": [
    "# count the number of theorems (getGhost) and implementations (getNonGhost) proved\n",
    "# i.e. check that the number of errors when verified is zero\n",
    "# TODO: include arguments for getGhost and getNonGhost to reduce duplicate processing\n",
    "def getProved(dafny_file):\n",
    "    cmd = \"dafny /dafnyVerify:1 /compile:0 \" + dafny_file\n",
    "    result = subprocess.run(['/bin/bash', '-i', '-c', cmd], stdout=subprocess.PIPE)\n",
    "    output = result.stdout.decode('ascii')\n",
    "    for line in output.splitlines():\n",
    "        if line.startswith(\"Dafny program verifier finished with \"):\n",
    "            # check no errors\n",
    "            #print(line, re.findall(r'\\d+', line)[1], type(re.findall(r'\\d+', line)[1]))\n",
    "            if not int(re.findall(r'\\d+', line)[1]):\n",
    "                return (getGhost(dafny_file) + getNonGhost(dafny_file))\n",
    "        else:\n",
    "            pass\n",
    "    # if the verifier doesn't finish, return -1\n",
    "    return 0"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Test statistics functions"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [],
   "source": [
    "# s/False/True if need to run the tests\n",
    "if False:\n",
    "    # test file options:\n",
    "    test_file = \"/Users/joannefuller/Documents/vscode/eth2.0-dafny/src/dafny/ssz/BytesAndBits.dfy\"\n",
    "    #test_file = \"/Users/joannefuller/Documents/vscode/eth2.0-dafny/test/dafny/merkle/Merkleise.test.dfy\"\n",
    "    #test_file = \"/Users/joannefuller/Documents/vscode/eth2.0-dafny/test/dafny/ssz/BitListSeDes.tests.dfy\"\n",
    "    #test_file = \"/Users/joannefuller/Documents/vscode/eth2.0-dafny/src/dafny/ssz/BitListSeDes.dfy\"\n",
    "    #test_file = \"/Users/joannefuller/Documents/vscode/eth2.0-dafny/src/dafny/merkle/Merkleise.dfy\"\n",
    "\n",
    "    #print(\"Lemmas ...\")\n",
    "    #print(getLemmas(test_file))\n",
    "\n",
    "    #print(\"Function methods ...\")\n",
    "    #print(getFunctions(test_file))\n",
    "\n",
    "    #print(\"LoC ...\")\n",
    "    #print(getLoC(test_file))\n",
    "\n",
    "    #print(\"Documentation ...\")\n",
    "    #print(getDocumentation(test_file))\n",
    "\n",
    "    print(\"Proved (verified from compile) ...\")\n",
    "    print(getProved(test_file))\n",
    "\n",
    "    #print(\"Ghost ...\")\n",
    "    #rint(getGhost(test_file))\n",
    "\n",
    "    #print(\"NonGhost ...\")\n",
    "    #print(getNonGhost(test_file))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Collate results into a pandas dataframe\n",
    "\n",
    "One row per Dafny file."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "                                Files                          Folder  #LoC  \\\n",
       "0                    DepositSmart.dfy                 src/dafny/smart   163   \n",
       "1                    CommuteProof.dfy      src/dafny/smart/algorithms    73   \n",
       "2             IndexBasedAlgorithm.dfy      src/dafny/smart/algorithms    96   \n",
       "3                   MainAlgorithm.dfy      src/dafny/smart/algorithms    66   \n",
       "4                OptimalAlgorithm.dfy      src/dafny/smart/algorithms    24   \n",
       "5                         Helpers.dfy         src/dafny/smart/helpers    51   \n",
       "6                      SeqHelpers.dfy         src/dafny/smart/helpers   137   \n",
       "7   NextPathInCompleteTreesLemmas.dfy           src/dafny/smart/paths   262   \n",
       "8             PathInCompleteTrees.dfy           src/dafny/smart/paths   408   \n",
       "9                       SeqOfBits.dfy       src/dafny/smart/seqofbits   527   \n",
       "10                ComputeRootPath.dfy  src/dafny/smart/synthattribute   305   \n",
       "11             GenericComputation.dfy  src/dafny/smart/synthattribute   148   \n",
       "12                  RightSiblings.dfy  src/dafny/smart/synthattribute   210   \n",
       "13                       Siblings.dfy  src/dafny/smart/synthattribute   124   \n",
       "14                   SiblingsPlus.dfy  src/dafny/smart/synthattribute   556   \n",
       "15                  CompleteTrees.dfy           src/dafny/smart/trees    89   \n",
       "16                    MerkleTrees.dfy           src/dafny/smart/trees   208   \n",
       "17                          Trees.dfy           src/dafny/smart/trees    91   \n",
       "18                                                              TOTAL  3538   \n",
       "\n",
       "    Theorems  Implementations  Documentation  #Doc/#LoC (%)  Proved  \n",
       "0          0                5             92             56       5  \n",
       "1          2                0             31             42       2  \n",
       "2          3                2             59             61       5  \n",
       "3          2                0             38             58       2  \n",
       "4          2                0             15             62       2  \n",
       "5          5                1             10             20       6  \n",
       "6         10                6             34             25      16  \n",
       "7          3                2             99             38       5  \n",
       "8         15                0             60             15      15  \n",
       "9         19                0            100             19      19  \n",
       "10        11                0            116             38      11  \n",
       "11         6                0             75             51       6  \n",
       "12         5                1             57             27       6  \n",
       "13         2                0             31             25       2  \n",
       "14         4                0             52              9       4  \n",
       "15         8                1             19             21       9  \n",
       "16         6                3            101             49       9  \n",
       "17         3                5             41             45       8  \n",
       "18       106               26           1030             29     132  "
      ],
      "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>Files</th>\n      <th>Folder</th>\n      <th>#LoC</th>\n      <th>Theorems</th>\n      <th>Implementations</th>\n      <th>Documentation</th>\n      <th>#Doc/#LoC (%)</th>\n      <th>Proved</th>\n    </tr>\n  </thead>\n  <tbody>\n    <tr>\n      <th>0</th>\n      <td>DepositSmart.dfy</td>\n      <td>src/dafny/smart</td>\n      <td>163</td>\n      <td>0</td>\n      <td>5</td>\n      <td>92</td>\n      <td>56</td>\n      <td>5</td>\n    </tr>\n    <tr>\n      <th>1</th>\n      <td>CommuteProof.dfy</td>\n      <td>src/dafny/smart/algorithms</td>\n      <td>73</td>\n      <td>2</td>\n      <td>0</td>\n      <td>31</td>\n      <td>42</td>\n      <td>2</td>\n    </tr>\n    <tr>\n      <th>2</th>\n      <td>IndexBasedAlgorithm.dfy</td>\n      <td>src/dafny/smart/algorithms</td>\n      <td>96</td>\n      <td>3</td>\n      <td>2</td>\n      <td>59</td>\n      <td>61</td>\n      <td>5</td>\n    </tr>\n    <tr>\n      <th>3</th>\n      <td>MainAlgorithm.dfy</td>\n      <td>src/dafny/smart/algorithms</td>\n      <td>66</td>\n      <td>2</td>\n      <td>0</td>\n      <td>38</td>\n      <td>58</td>\n      <td>2</td>\n    </tr>\n    <tr>\n      <th>4</th>\n      <td>OptimalAlgorithm.dfy</td>\n      <td>src/dafny/smart/algorithms</td>\n      <td>24</td>\n      <td>2</td>\n      <td>0</td>\n      <td>15</td>\n      <td>62</td>\n      <td>2</td>\n    </tr>\n    <tr>\n      <th>5</th>\n      <td>Helpers.dfy</td>\n      <td>src/dafny/smart/helpers</td>\n      <td>51</td>\n      <td>5</td>\n      <td>1</td>\n      <td>10</td>\n      <td>20</td>\n      <td>6</td>\n    </tr>\n    <tr>\n      <th>6</th>\n      <td>SeqHelpers.dfy</td>\n      <td>src/dafny/smart/helpers</td>\n      <td>137</td>\n      <td>10</td>\n      <td>6</td>\n      <td>34</td>\n      <td>25</td>\n      <td>16</td>\n    </tr>\n    <tr>\n      <th>7</th>\n      <td>NextPathInCompleteTreesLemmas.dfy</td>\n      <td>src/dafny/smart/paths</td>\n      <td>262</td>\n      <td>3</td>\n      <td>2</td>\n      <td>99</td>\n      <td>38</td>\n      <td>5</td>\n    </tr>\n    <tr>\n      <th>8</th>\n      <td>PathInCompleteTrees.dfy</td>\n      <td>src/dafny/smart/paths</td>\n      <td>408</td>\n      <td>15</td>\n      <td>0</td>\n      <td>60</td>\n      <td>15</td>\n      <td>15</td>\n    </tr>\n    <tr>\n      <th>9</th>\n      <td>SeqOfBits.dfy</td>\n      <td>src/dafny/smart/seqofbits</td>\n      <td>527</td>\n      <td>19</td>\n      <td>0</td>\n      <td>100</td>\n      <td>19</td>\n      <td>19</td>\n    </tr>\n    <tr>\n      <th>10</th>\n      <td>ComputeRootPath.dfy</td>\n      <td>src/dafny/smart/synthattribute</td>\n      <td>305</td>\n      <td>11</td>\n      <td>0</td>\n      <td>116</td>\n      <td>38</td>\n      <td>11</td>\n    </tr>\n    <tr>\n      <th>11</th>\n      <td>GenericComputation.dfy</td>\n      <td>src/dafny/smart/synthattribute</td>\n      <td>148</td>\n      <td>6</td>\n      <td>0</td>\n      <td>75</td>\n      <td>51</td>\n      <td>6</td>\n    </tr>\n    <tr>\n      <th>12</th>\n      <td>RightSiblings.dfy</td>\n      <td>src/dafny/smart/synthattribute</td>\n      <td>210</td>\n      <td>5</td>\n      <td>1</td>\n      <td>57</td>\n      <td>27</td>\n      <td>6</td>\n    </tr>\n    <tr>\n      <th>13</th>\n      <td>Siblings.dfy</td>\n      <td>src/dafny/smart/synthattribute</td>\n      <td>124</td>\n      <td>2</td>\n      <td>0</td>\n      <td>31</td>\n      <td>25</td>\n      <td>2</td>\n    </tr>\n    <tr>\n      <th>14</th>\n      <td>SiblingsPlus.dfy</td>\n      <td>src/dafny/smart/synthattribute</td>\n      <td>556</td>\n      <td>4</td>\n      <td>0</td>\n      <td>52</td>\n      <td>9</td>\n      <td>4</td>\n    </tr>\n    <tr>\n      <th>15</th>\n      <td>CompleteTrees.dfy</td>\n      <td>src/dafny/smart/trees</td>\n      <td>89</td>\n      <td>8</td>\n      <td>1</td>\n      <td>19</td>\n      <td>21</td>\n      <td>9</td>\n    </tr>\n    <tr>\n      <th>16</th>\n      <td>MerkleTrees.dfy</td>\n      <td>src/dafny/smart/trees</td>\n      <td>208</td>\n      <td>6</td>\n      <td>3</td>\n      <td>101</td>\n      <td>49</td>\n      <td>9</td>\n    </tr>\n    <tr>\n      <th>17</th>\n      <td>Trees.dfy</td>\n      <td>src/dafny/smart/trees</td>\n      <td>91</td>\n      <td>3</td>\n      <td>5</td>\n      <td>41</td>\n      <td>45</td>\n      <td>8</td>\n    </tr>\n    <tr>\n      <th>18</th>\n      <td></td>\n      <td>TOTAL</td>\n      <td>3538</td>\n      <td>106</td>\n      <td>26</td>\n      <td>1030</td>\n      <td>29</td>\n      <td>132</td>\n    </tr>\n  </tbody>\n</table>\n</div>"
     },
     "metadata": {},
     "execution_count": 16
    }
   ],
   "source": [
    "import tempfile\n",
    "\n",
    "# create a pandas dataframe to store stats relating to the dafny files\n",
    "column_list = ['Files', 'Folder', '#LoC', 'Theorems', 'Implementations', \"Documentation\", \"#Doc/#LoC (%)\", \"Proved\"]\n",
    "\n",
    "# list here all the directory not to include in the stat collection with path relative to the root of the repo\n",
    "exclude_folders_rel_path = [\"src/dafny/.\", \"src/dafny/synthattribute\", \"src/dafny/paths\"]\n",
    "\n",
    "repo_directory = \"/Users/franck/development/deposit-sc-dafny/\"\n",
    "\n",
    "# performs a clean checkout from GitHub before collecting the stats\n",
    "# with tempfile.TemporaryDirectory() as repo_directory: \n",
    "#     subprocess.run(['/bin/bash','-c','git clone git@github.com:PegaSysEng/deposit-sc-dafny.git ' + repo_directory], stdout=subprocess.PIPE)\n",
    "\n",
    "exclude_folders_full_path = [os.path.join(repo_directory,f) for f in exclude_folders_rel_path]\n",
    "\n",
    "files = getListOfDafnyFiles(repo_directory, exclude_folders_full_path)   \n",
    "\n",
    "df = pd.DataFrame(columns=column_list)\n",
    "\n",
    "# collect data for each dafny file\n",
    "for file in files:\n",
    "    loc = getLoC(file)\n",
    "    ghost = getGhost(file)\n",
    "    nonghost = getNonGhost(file)\n",
    "    doc = getDocumentation(file)\n",
    "    proved = getProved(file)\n",
    "    df2 = pd.DataFrame([[os.path.basename(file), \n",
    "                        getFolder(repo_directory, file), \n",
    "                        loc ,\n",
    "                        ghost, \n",
    "                        nonghost,\n",
    "                        doc,\n",
    "                        round(doc/loc * 100),\n",
    "                        proved]], \n",
    "                        columns=column_list)\n",
    "    df = df.append(df2, ignore_index=True)\n",
    "\n",
    "# create and append totals for numeric columns\n",
    "totals = pd.DataFrame([[\"\", \n",
    "                        \"TOTAL\", \n",
    "                        df['#LoC'].sum(),\n",
    "                        df['Theorems'].sum(), \n",
    "                        df['Implementations'].sum(),\n",
    "                        df['Documentation'].sum(),\n",
    "                        round(df['Documentation'].sum()/df['#LoC'].sum() * 100),\n",
    "                        df['Proved'].sum()]], \n",
    "                        columns=column_list)\n",
    "df = df.append(totals, ignore_index=True)\n",
    "\n",
    "# convert numeric columns to int64\n",
    "numCols = ['#LoC', 'Theorems', 'Implementations', \"Documentation\", \"#Doc/#LoC (%)\", \"Proved\"]\n",
    "df[numCols] = df[numCols].astype(\"int64\")\n",
    "\n",
    "#display a sample of rows\n",
    "df.head(len(df))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Alternative format\n",
    "\n",
    "May be useful for github"
   ]
  },
  {
   "source": [
    "from tabulate import tabulate\n",
    "\n",
    "print(tabulate(df, headers='keys', tablefmt='github'))\n",
    "\n",
    "print(tabulate(df_grouped, headers='keys', tablefmt='github'))\n",
    "\n"
   ],
   "cell_type": "code",
   "metadata": {
    "tags": []
   },
   "execution_count": 25,
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "|    | Files                             | Folder                         |   #LoC |   Theorems |   Implementations |   Documentation |   #Doc/#LoC (%) |   Proved |\n|----|-----------------------------------|--------------------------------|--------|------------|-------------------|-----------------|-----------------|----------|\n|  0 | DepositSmart.dfy                  | src/dafny/smart                |    163 |          0 |                 5 |              92 |              56 |        5 |\n|  1 | CommuteProof.dfy                  | src/dafny/smart/algorithms     |     73 |          2 |                 0 |              31 |              42 |        2 |\n|  2 | IndexBasedAlgorithm.dfy           | src/dafny/smart/algorithms     |     96 |          3 |                 2 |              59 |              61 |        5 |\n|  3 | MainAlgorithm.dfy                 | src/dafny/smart/algorithms     |     66 |          2 |                 0 |              38 |              58 |        2 |\n|  4 | OptimalAlgorithm.dfy              | src/dafny/smart/algorithms     |     24 |          2 |                 0 |              15 |              62 |        2 |\n|  5 | Helpers.dfy                       | src/dafny/smart/helpers        |     51 |          5 |                 1 |              10 |              20 |        6 |\n|  6 | SeqHelpers.dfy                    | src/dafny/smart/helpers        |    137 |         10 |                 6 |              34 |              25 |       16 |\n|  7 | NextPathInCompleteTreesLemmas.dfy | src/dafny/smart/paths          |    262 |          3 |                 2 |              99 |              38 |        5 |\n|  8 | PathInCompleteTrees.dfy           | src/dafny/smart/paths          |    408 |         15 |                 0 |              60 |              15 |       15 |\n|  9 | SeqOfBits.dfy                     | src/dafny/smart/seqofbits      |    527 |         19 |                 0 |             100 |              19 |       19 |\n| 10 | ComputeRootPath.dfy               | src/dafny/smart/synthattribute |    305 |         11 |                 0 |             116 |              38 |       11 |\n| 11 | GenericComputation.dfy            | src/dafny/smart/synthattribute |    148 |          6 |                 0 |              75 |              51 |        6 |\n| 12 | RightSiblings.dfy                 | src/dafny/smart/synthattribute |    210 |          5 |                 1 |              57 |              27 |        6 |\n| 13 | Siblings.dfy                      | src/dafny/smart/synthattribute |    124 |          2 |                 0 |              31 |              25 |        2 |\n| 14 | SiblingsPlus.dfy                  | src/dafny/smart/synthattribute |    556 |          4 |                 0 |              52 |               9 |        4 |\n| 15 | CompleteTrees.dfy                 | src/dafny/smart/trees          |     89 |          8 |                 1 |              19 |              21 |        9 |\n| 16 | MerkleTrees.dfy                   | src/dafny/smart/trees          |    208 |          6 |                 3 |             101 |              49 |        9 |\n| 17 | Trees.dfy                         | src/dafny/smart/trees          |     91 |          3 |                 5 |              41 |              45 |        8 |\n| 18 |                                   | TOTAL                          |   3538 |        106 |                26 |            1030 |              29 |      132 |\n|    | Folder                         |   #Files |   #LoC |   Theorems |   Implementations |   Documentation |   #Doc/#LoC (%) |   Proved |\n|----|--------------------------------|----------|--------|------------|-------------------|-----------------|-----------------|----------|\n|  0 | src/dafny/smart/trees          |       18 |   3538 |        106 |                26 |            1030 |              29 |      132 |\n|  1 | src/dafny/smart/algorithms     |        4 |    259 |          9 |                 2 |             143 |              55 |       11 |\n|  2 | src/dafny/smart/helpers        |        2 |    188 |         15 |                 7 |              44 |              23 |       22 |\n|  3 | src/dafny/smart/paths          |        2 |    670 |         18 |                 2 |             159 |              24 |       20 |\n|  4 | src/dafny/smart/seqofbits      |        1 |    527 |         19 |                 0 |             100 |              19 |       19 |\n|  5 | src/dafny/smart/synthattribute |        5 |   1343 |         28 |                 1 |             331 |              25 |       29 |\n|  6 | src/dafny/smart/trees          |        3 |    388 |         17 |                 9 |             161 |              41 |       26 |\n"
     ]
    }
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Group data\n",
    "\n",
    "One row per folder."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "metadata": {},
   "outputs": [],
   "source": [
    "# create a pandas dataframe to store stats relating to the dafny files\n",
    "# stats grouped by folder\n",
    "column_list = ['Folder', '#Files', '#LoC', 'Theorems', 'Implementations', \"Documentation\", \"#Doc/#LoC (%)\", \"Proved\"]\n",
    "df_grouped = pd.DataFrame(columns=column_list)\n",
    "\n",
    "# with tempfile.TemporaryDirectory() as repo_directory:\n",
    "#     subprocess.run(['/bin/bash','-c','git clone git@github.com:PegaSysEng/eth2.0-dafny.git ' + repo_directory], stdout=subprocess.PIPE)\n",
    "\n",
    "exclude_folders_full_path = [os.path.join(repo_directory,f) for f in exclude_folders_rel_path]\n",
    "repo_directory = \"/Users/franck/development/deposit-sc-dafny/\"\n",
    "\n",
    "# TODO: We currently get the list of folders out of the list of files and then in the `for` loop\n",
    "# we retrieve the list of files again for each folder. We may want to think of a more elegant \n",
    "# implementation.\n",
    "allFiles = getListOfDafnyFiles(repo_directory, exclude_folders_full_path)  \n",
    "\n",
    "folders = getListOfDafnyFolders(allFiles)\n",
    "\n",
    "for folder in folders:\n",
    "    files = getListOfDafnyFiles(folder)\n",
    "    \n",
    "    nFiles = 0\n",
    "    nLoc = 0\n",
    "    nGhost = 0\n",
    "    nNonGhost = 0\n",
    "    nDoc = 0\n",
    "    nProved = 0\n",
    "    for file in files:\n",
    "        nFiles += 1\n",
    "        nLoc += getLoC(file)\n",
    "        nGhost += getGhost(file)\n",
    "        nNonGhost += getNonGhost(file)\n",
    "        nDoc += getDocumentation(file)\n",
    "        nProved += getProved(file)\n",
    "    \n",
    "\n",
    "    df2 = pd.DataFrame([[getFolder(repo_directory, file), \n",
    "                        nFiles, \n",
    "                        nLoc ,\n",
    "                        nGhost, \n",
    "                        nNonGhost,\n",
    "                        nDoc,\n",
    "                        round(nDoc/nLoc * 100),\n",
    "                        nProved]], \n",
    "                        columns=column_list)\n",
    "    df_grouped = df_grouped.append(df2, ignore_index=True)\n",
    "\n",
    "    #display a sample of rows\n",
    "    # df_grouped.head(len(df_grouped))\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Print dataframe to .csv, .tex and .pdf"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "'data/data20201013.pdf'"
      ]
     },
     "metadata": {},
     "execution_count": 28
    }
   ],
   "source": [
    "# create filenames that include the current data string\n",
    "timestr = time.strftime(\"%Y%m%d\")\n",
    "rawfile = 'data' + timestr + '.csv'\n",
    "grouped_rawfile = 'dataGrouped' + timestr + '.csv'\n",
    "filename = 'data' + timestr + '.tex'\n",
    "pdffile = 'data' + timestr + '.pdf'\n",
    "\n",
    "# check if data directory already exists and create if necessary\n",
    "if not os.path.exists('data'):\n",
    "    os.makedirs('data')\n",
    "\n",
    "#print to csv file without an index\n",
    "df.to_csv(\"data/\" + rawfile, index = False)\n",
    "df_grouped.to_csv(\"data/\" + grouped_rawfile, index = False)\n",
    "\n",
    "#print to pdf via latex\n",
    "template = r'''\\documentclass[a4paper, 12pt]{{article}}\n",
    "\\usepackage[landscape]{{geometry}}\n",
    "\\usepackage{{booktabs}}\n",
    "\\begin{{document}}\n",
    "\\section*{{https://github.com/PegaSysEng/-dafny}}\n",
    "\\subsection*{{Data collected: {}}}\n",
    "\\scriptsize\n",
    "{}\n",
    "\\vspace{{2em}}\n",
    "{}\n",
    "\\end{{document}}\n",
    "'''\n",
    "\n",
    "with open(filename, 'w') as f:\n",
    "    f.write(template.format(time.strftime(\"%Y-%m-%d\"), df.to_latex(index=False), df_grouped.to_latex(index=False)))\n",
    "\n",
    "subprocess.call(['pdflatex', filename])\n",
    "\n",
    "# remove surplus files and move .csv, .tex and .pdf files to the data folder\n",
    "os.remove('data' + timestr + '.log')\n",
    "os.remove('data' + timestr + '.aux')\n",
    "\n",
    "shutil.move(filename, \"data/\" + filename)\n",
    "shutil.move(pdffile, \"data/\" + pdffile)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "language_info": {
   "name": "python",
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "version": "3.8.6-final"
  },
  "orig_nbformat": 2,
  "file_extension": ".py",
  "mimetype": "text/x-python",
  "name": "python",
  "npconvert_exporter": "python",
  "pygments_lexer": "ipython3",
  "version": 3,
  "kernelspec": {
   "name": "Python 3.8.6 64-bit",
   "display_name": "Python 3.8.6 64-bit",
   "metadata": {
    "interpreter": {
     "hash": "1ee38ef4a5a9feb55287fd749643f13d043cb0a7addaab2a9c224cbe137c0062"
    }
   }
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}