SmartPulseTool/SmartPulse.py at master · utopia-group/SmartPulseTool · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
#!/usr/bin/python

import os
import sys
import subprocess
import platform

argTrans = {"-modArith": "/useModularArithmetic",
            "-instrumentGas": "/instrumentGas",
            "-noReentrancy": "/stubModel:skip",
            "-singleCallback": "/stubModel:callback",
            "-powerfulAdversary": "/stubModel:multipleCallbacks",
            "-txnsOnFields": "/txnsOnFields",
            "-checkPrePost:": "/prePostHarness /SliceFunctions:"}

solFile = ""
contractName = ""
specification = ""
verisolFlags = "/modelReverts /omitSourceLineInfo /LazyAllocNoMod /omitAxioms /doModSet /noPrf /noChk /omitDataValuesInTrace /QuantFreeAllocs /instrumentSums /omitBoogieHarness /createMainHarness /noCustomTypes /alias  /noNonlinearArith /useNumericOperators /omitUnsignedSemantics /generateGetters /modelAssemblyAsHavoc /useMultiDim"
smartpulseDir = os.path.dirname(os.path.realpath(__file__))

def printUsage():
    print("Usage: ./SmartPulse.py [args] contract.sol contractName spec.spec")
    print("args:")
    print(" Behavioral Models:")
    print("  -modArith                   | Model integers using modular arithmetic rather than as mathematical integers")
    print("  -instrumentGas              | Instrument gas usage using model (assumes model comes from solc)")
    print(" Adversary Models:")
    print("  -noReentrancy               | Assume attacker cannot make reentrant calls ")
    print("  -singleCallback             | Assume attacker will only make one reentrant call")
    print("  -powerfulAdversary          | Assume attacker can make arbitrary reentrant calls")
    print(" Harness Modifiers:")
    print("  -tnxsOnFields               | Allow transactions to be issued to contracts in fields of main contract")
    print("  -checkPrePost:<fn1,fn2,...> | Check pre/post conditions of the specified functions")


def processArgs(args):
    global solFile
    global contractName
    global specification
    global verisolFlags

    if len(args) < 4:
        return
    for i in range(1,len(args)):
        if i == len(args) - 3:
            solFile = args[i]

            if("CYGWIN" in platform.system()):
                stream = os.popen('cygpath -m ' + solFile);
                solFile = stream.read().strip()
            elif("Linux" in platform.system() and "Microsoft" in platform.release()):
                stream = os.popen('wslpath -m ' + solFile);
                solFile = stream.read().strip()
        elif i == len(args) - 2:
            contractName = args[i]
        elif i == len(args) - 1:
            specification = args[i]
        else:
            for key, value in argTrans.iteritems():
                if key in args[i]:
                    verisolFlags += " " + args[i].replace(key, value)


def solToBoogie():
    veriSolName = 'VeriSol'
    if("Linux" in platform.system() and "Microsoft" in platform.release()):
        veriSolName = 'VeriSol.exe'
    verisolCall = [veriSolName, solFile, contractName]
    verisolCall.append(verisolFlags)

    print(verisolCall)
    verisolLog = open("verisolOutput.log", "w")
    verisolLog.write(" ".join(verisolCall))
    verisolLog.write(os.linesep)
    verisolLog.flush()

    print("Translating contract to Boogie...")

    try:
        process = subprocess.Popen(" ".join(verisolCall), stdin=None, stdout=verisolLog, stderr=subprocess.STDOUT, shell=True)
    except:
        print("Cannot open subprocess")
        sys.exit(1)

    process.wait()
    verisolLog.close()

    if process.returncode != 0:
        print("Could not translate with VeriSol, see verisolOutput.log for details")
        sys.exit(1)

def check():
    boogieFile = open("__SolToBoogieTest_out.bpl", "a")
    specFile = open(specification, "r")
    for line in specFile.readlines():
        boogieFile.write(line + os.linesep)

    boogieFile.close()
    specFile.close()

    try:
        process = subprocess.Popen("{0}/SmartPulse.sh __SolToBoogieTest_out.bpl".format(smartpulseDir), shell=True)
    except:
        print("Cannot open subprocess")
        sys.exit(1)

    process.wait()


processArgs(sys.argv)

if solFile == "":
    printUsage()
    sys.exit(1)

solToBoogie()
check()