#!/usr/bin/env python

import argparse
import os
import subprocess
import sys

class Options:
    ToolPath = ""
    OutputPath = ""
    Solution = ""

class Benchmarks(object):
    default = ['BoundedAsync', 'German', 'BasicPaxos', 'TwoPhaseCommit', 'Chord', 'MultiPaxos',
               'Raft', 'ChainReplication']

    racy = ['BoundedAsyncRacy', 'GermanRacy', 'BasicPaxosRacy', 'TwoPhaseCommitRacy',
             'ChordRacy', 'MultiPaxosRacy', 'RaftRacy', 'ChainReplicationRacy']

    soter = ['Leader', 'Pi', 'Chameneos', 'Swordfish']

    defaultVerified = [ ]
    racyFoundBugs = [ ]
    soterVerified = [ ]

    defaultFalsePositivesWithoutXSA = [ ]
    defaultFalsePositivesXSA = [ ]
    soterFalsePositivesWithoutXSA = [ ]
    soterFalsePositivesXSA = [ ]

    defaultTotalTime = [ ]
    racyTotalTime = [ ]
    soterTotalTime = [ ]

def constructTable():
    print("Constructing LaTeX table with static analysis results ...")

    tableString = ""
    tableString += "& & & & & & \multicolumn{4}{c}{\\textbf{Non-racy versions}}\n"
    tableString += "& \multicolumn{2}{c}{\\textbf{Racy versions}}\\\\\n"
    tableString += "\cmidrule(lr){7-10}\n"
    tableString += "\cmidrule(lr){11-12}\n"
    tableString += "\n"

    tableString += "& & & &\n"
    tableString += "& & & \multicolumn{2}{c}{\\textbf{\# False positives}}\n"
    tableString += "& & & \multirow{2}{*}{\\textbf{Found all}}\\\\\n"
    tableString += "\cmidrule(lr){8-9}\n"
    tableString += "\n"

    tableString += "& \\textbf{Benchmarks}\n"
    tableString += "& \\textbf{LoC}\n"
    tableString += "& \\textbf{\#M}\n"
    tableString += "& \\textbf{\#ST}\n"
    tableString += "& \\textbf{\#AB}\n"
    tableString += "& \multicolumn{1}{r}{\\textbf{Time (s)}}\n"
    tableString += "& \multicolumn{1}{r}{\\textbf{(No xSA)}}\n"
    tableString += "& \multicolumn{1}{r}{\\textbf{(xSA)}}\n"
    tableString += "& \multicolumn{1}{r}{\\textbf{Verified?}}\n"
    tableString += "& \multicolumn{1}{r}{\\textbf{Time (s)}}\n"
    tableString += "& \multicolumn{1}{r}{\\textbf{data races?}}\\\\[0.3em]\n"
    tableString += "\n"

    tableString += "\\toprule\n"
    tableString += "\n"

    tableString += "& \caseStudy\n"
    tableString += "& -\n"
    tableString += "& -\n"
    tableString += "& -\n"
    tableString += "& -\n"
    tableString += "& \multicolumn{5}{r}{omitted because it is proprietary}\n"
    tableString += "& \multicolumn{1}{r}{-}\\\\\n"
    tableString += "\n"

    tableString += "\midrule\n"
    tableString += "\n"

    tableString += "\parbox[t]{2mm}{\multirow{8}{*}{\\rotatebox[origin=c]{90}{\\textbf{\\benchmarkSuite}}}}\n"
    tableString += "\n"

    iteration = 0
    for benchmark in Benchmarks.default:
        tableString += "& " + benchmark + "\n"
        tableString += "& -\n"
        tableString += "& -\n"
        tableString += "& -\n"
        tableString += "& -\n"

        tableString += "& \multicolumn{1}{r}{" + str(Benchmarks.defaultTotalTime[iteration]) + "}\n"

        if Benchmarks.defaultFalsePositivesWithoutXSA[iteration] == 0:
            tableString += "& \\multicolumn{1}{r}{\\xmark}\n"
        else:
            tableString += "& \\multicolumn{1}{r}{" + str(Benchmarks.defaultFalsePositivesWithoutXSA[iteration]) + "}\n"

        if Benchmarks.defaultFalsePositivesXSA[iteration] == 0:
            tableString += "& \\multicolumn{1}{r}{\\xmark}\n"
        else:
            tableString += "& \\multicolumn{1}{r}{" + str(Benchmarks.defaultFalsePositivesXSA[iteration]) + "}\n"

        if Benchmarks.defaultVerified[iteration]:
            tableString += "& \multicolumn{1}{r}{\\cmark}\n"
        else:
            tableString += "& \multicolumn{1}{r}{\\xmark}\n"

        tableString += "& \multicolumn{1}{r}{" + str(Benchmarks.racyTotalTime[iteration]) + "}\n"

        if (iteration == len(Benchmarks.default) - 1):
            if Benchmarks.racyFoundBugs[iteration]:
                tableString += "& \multicolumn{1}{r}{\\cmark}\\\\[0.2em]\n"
            else:
                tableString += "& \multicolumn{1}{r}{\\xmark}\\\\[0.2em]\n"
        else:
            if Benchmarks.racyFoundBugs[iteration]:
                tableString += "& \multicolumn{1}{r}{\\cmark}\\\\\n"
            else:
                tableString += "& \multicolumn{1}{r}{\\xmark}\\\\\n"

        tableString += "\n"
        iteration += 1

    tableString += "\\midrule\n"
    tableString += "\n"

    tableString += "\parbox[t]{2mm}{\multirow{4}{*}{\\rotatebox[origin=c]{90}{\\textbf{\\soterSuite}}}}\n"
    tableString += "\n"

    iteration = 0
    for benchmark in Benchmarks.soter:
        tableString += "& " + benchmark + "\n"
        tableString += "&\n"
        tableString += "&\n"
        tableString += "&\n"
        tableString += "&\n"

        tableString += "& \multicolumn{1}{r}{" + str(Benchmarks.soterTotalTime[iteration]) + "}\n"

        if Benchmarks.soterFalsePositivesWithoutXSA[iteration] == 0:
            tableString += "& \\multicolumn{1}{r}{\\xmark}\n"
        else:
            tableString += "& \\multicolumn{1}{r}{" + str(Benchmarks.soterFalsePositivesWithoutXSA[iteration]) + "}\n"

        if Benchmarks.soterFalsePositivesXSA[iteration] == 0:
            tableString += "& \\multicolumn{1}{r}{\\xmark}\n"
        else:
            tableString += "& \\multicolumn{1}{r}{" + str(Benchmarks.soterFalsePositivesXSA[iteration]) + "}\n"

        if Benchmarks.soterVerified[iteration]:
            tableString += "& \multicolumn{1}{r}{\\cmark}\n"
        else:
            tableString += "& \multicolumn{1}{r}{\\xmark}\n"

        tableString += "& \multicolumn{1}{r}{-}\n"
        if (iteration == len(Benchmarks.soter) - 1):
            tableString += "& \multicolumn{1}{r}{-}\\\\[0.2em]\n"
        else:
            tableString += "& \multicolumn{1}{r}{-}\\\\\n"

        tableString += "\n"
        iteration += 1

    Options.OutputPath = os.path.join('Output', 'analysis_table.tex')
    tableFile = open(Options.OutputPath, 'w+')
    tableFile.write(tableString)
    tableFile.close()

def crunchBenchmarks():
    Options.ToolPath = os.path.join('Binaries', 'PSharpStaticAnalyser.exe')
    Options.Solution = os.path.join('StaticAnalysisBenchmarks.sln')
    print(Options.Solution)

    print("Running experiment 1 (out of 8) - Analysing PSharpBench-default without xSA ...\n")
    for benchmark in Benchmarks.default:
        print("  Analysing (without xSA): " + benchmark + "\n")
        tool = subprocess.Popen([Options.ToolPath, "/s:" + Options.Solution, "/p:" + benchmark, '/nostatetransitionanalysis'],
            stdout=subprocess.PIPE, shell=True)
        out, err = tool.communicate()
        print(out)

        lines = out.split('\n')
        if lines[len(lines) - 3].strip() == "P# static analyser did not detect any errors.":
            Benchmarks.defaultFalsePositivesWithoutXSA += [ 0 ]
        else:
            Benchmarks.defaultFalsePositivesWithoutXSA += [ int(lines[len(lines) - 3].strip().split(' ')[4].translate(None, '\'')) ]

    print("Running experiment 2 (out of 8) - Analysing PSharpBench-default with xSA ...\n")
    for benchmark in Benchmarks.default:
        print("  Analysing (with xSA): " + benchmark + "\n")
        tool = subprocess.Popen([Options.ToolPath, "/s:" + Options.Solution, "/p:" + benchmark],
            stdout=subprocess.PIPE, shell=True)
        out, err = tool.communicate()
        print(out)

        lines = out.split('\n')
        if lines[len(lines) - 3].strip() == "P# static analyser did not detect any errors.":
            Benchmarks.defaultFalsePositivesXSA += [ 0 ]
            Benchmarks.defaultVerified += [ True ]
        else:
            Benchmarks.defaultFalsePositivesXSA += [ int(lines[len(lines) - 3].strip().split(' ')[4].translate(None, '\'')) ]
            Benchmarks.defaultVerified += [ False ]

    print("Running experiment 3 (out of 8) - Timing PSharpBench-default ...")
    for benchmark in Benchmarks.default:
        times = [ ]
        for iteration in range(0, 10):
            print("  [default] " + benchmark + " " + str(int(iteration + 1)) + "/10")
            tool = subprocess.Popen([Options.ToolPath, "/s:" + Options.Solution, "/p:" + benchmark, '/time'],
                stdout=subprocess.PIPE, shell=True)
            out, err = tool.communicate()

            lines = out.split('\n')
            times += [ float(lines[len(lines) - 2].strip().split(' ')[2]) ]

        average = 0
        for timing in times:
            average += timing
        Benchmarks.defaultTotalTime += [ round(average / 10, 3) ]

    print("Running experiment 4 (out of 8) - Analysing PSharpBench-racy ...\n")
    for benchmark in Benchmarks.racy:
        print("  Analysing: " + benchmark + "\n")
        tool = subprocess.Popen([Options.ToolPath, "/s:" + Options.Solution, "/p:" + benchmark],
            stdout=subprocess.PIPE, shell=True)
        out, err = tool.communicate()
        print(out)

        lines = out.split('\n')
        if lines[len(lines) - 3].strip() == "P# static analyser did not detect any errors.":
            Benchmarks.racyFoundBugs += [ False ]
        else:
            Benchmarks.racyFoundBugs += [ True ]

    print("Running experiment 5 (out of 8) - Timing PSharpBench-racy ...")
    for benchmark in Benchmarks.racy:
        times = [ ]
        for iteration in range(0, 10):
            print("  [racy] " + benchmark + " " + str(int(iteration + 1)) + "/10")
            tool = subprocess.Popen([Options.ToolPath, "/s:" + Options.Solution, "/p:" + benchmark, '/time'],
                stdout=subprocess.PIPE, shell=True)
            out, err = tool.communicate()

            lines = out.split('\n')
            times += [ float(lines[len(lines) - 2].strip().split(' ')[2]) ]

        average = 0
        for timing in times:
            average += timing
        Benchmarks.racyTotalTime += [ round(average / 10, 3) ]

    print("Running experiment 6 (out of 8) - Analysing SOTER benchmarks without xSA ...\n")
    for benchmark in Benchmarks.soter:
        print("  Analysing (without xSA): " + benchmark + "\n")
        tool = subprocess.Popen([Options.ToolPath, "/s:" + Options.Solution, "/p:" + benchmark, '/nostatetransitionanalysis'],
            stdout=subprocess.PIPE, shell=True)
        out, err = tool.communicate()
        print(out)

        lines = out.split('\n')
        if lines[len(lines) - 3].strip() == "P# static analyser did not detect any errors.":
            Benchmarks.soterFalsePositivesWithoutXSA += [ 0 ]
        else:
            Benchmarks.soterFalsePositivesWithoutXSA += [ int(lines[len(lines) - 3].strip().split(' ')[4].translate(None, '\'')) ]

    print("Running experiment 7 (out of 8) - Analysing SOTER benchmarks with xSA ...\n")
    for benchmark in Benchmarks.soter:
        print("  Analysing (with xSA): " + benchmark + "\n")
        tool = subprocess.Popen([Options.ToolPath, "/s:" + Options.Solution, "/p:" + benchmark],
            stdout=subprocess.PIPE, shell=True)
        out, err = tool.communicate()
        print(out)

        lines = out.split('\n')
        if lines[len(lines) - 3].strip() == "P# static analyser did not detect any errors.":
            Benchmarks.soterFalsePositivesXSA += [ 0 ]
            Benchmarks.soterVerified += [ True ]
        else:
            Benchmarks.soterFalsePositivesXSA += [ int(lines[len(lines) - 3].strip().split(' ')[4].translate(None, '\'')) ]
            Benchmarks.soterVerified += [ True ]

    print("Running experiment 8 (out of 8) - Timing SOTER benchmarks ...")
    for benchmark in Benchmarks.soter:
        times = [ ]
        for iteration in range(0, 10):
            print("  [soter] " + benchmark + " " + str(int(iteration + 1)) + "/10")
            tool = subprocess.Popen([Options.ToolPath, "/s:" + Options.Solution, "/p:" + benchmark, '/time'],
                stdout=subprocess.PIPE, shell=True)
            out, err = tool.communicate()

            lines = out.split('\n')
            times += [ float(lines[len(lines) - 2].strip().split(' ')[2]) ]

        average = 0
        for timing in times:
            average += timing
        Benchmarks.soterTotalTime += [ round(average / 10, 3) ]

if __name__ == '__main__':
    parser = argparse.ArgumentParser(description='Script for running the P# static analysis experiments.')
    args = vars(parser.parse_args())

    crunchBenchmarks()
    constructTable()

    print("Done.")

    sys.exit(0)
