build.gradle

/*
 * Copyright 2022 ConsenSys Software Inc.
 *
 * Licensed under the Apache License, Version 2.0 (the "License"); you may
 * not use this file except in compliance with the License. You may obtain
 * a copy of the License at http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software dis-
 * tributed under the License is distributed on an "AS IS" BASIS, WITHOUT
 * WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
 * License for the specific language governing permissions and limitations
 * under the License.
 */

//  Taken from the EVM dafny repo, and slightly modified.

// Apply the java plugin to add support for Java
apply plugin: 'java'
// Apply eclipse plugin to add support for Eclipse
apply plugin: 'eclipse'
// Apply application plugin for generating start scripts
apply plugin: 'application'

// ======================================================================
// Randomisation
// ======================================================================
final RANDOM_ITERATIONS = project.properties["randomize"]

// Configure randomisation (if applicable)
final RANDOMIZE_FLAG = project.hasProperty("randomize") ? ['--boogie','/randomSeedIterations:' + RANDOM_ITERATIONS] : []
// Report whether randomisation is enabled.
if(project.hasProperty("randomize")) {
    project.logger.lifecycle('Randomize verification with ' + RANDOM_ITERATIONS + ' iterations.')
}

// ======================================================================
// Configure Z3
// ======================================================================

def DAFNY_HOME = System.env.'DAFNY_HOME'
// Configure Z3_PATH based on DAFNY_HOME
def Z3_PATH = DAFNY_HOME != null ? DAFNY_HOME + "/z3/bin/z3-4.12.1" : null
def JAVA_HOME = System.env.'JAVA_HOME'

if(project.hasProperty("solver-path")) {
  Z3_PATH = project.properties["solver-path"]
}

// Configure option for use with dafny command
final Z3_OPTION = DAFNY_HOME != null ? ['--solver-path',Z3_PATH] : []

// Report what happened
def DAFNY_HOME_STR = DAFNY_HOME != null ? DAFNY_HOME : "(unset)"
def Z3_PATH_STR = Z3_PATH != null ? Z3_PATH : "(unset)"
def JAVA_HOME_STR = JAVA_HOME != null ? JAVA_HOME : "(unset)"
println "DAFNY_HOME: $DAFNY_HOME_STR"
println "Z3_PATH   : $Z3_PATH_STR"

println "JAVA_HOME: $JAVA_HOME_STR"

// ======================================================================
// Constants (Dafny 4)
// ======================================================================


// Configure boogie-specific flags.
final BOOGIE_FLAGS = RANDOMIZE_FLAG

final DAFNY4_JAVA_BUILD_FLAGS = [
    'build',
    '--no-verify',
    '--target','java',
    '--output','build/libs/Driver-java/evmdis.jar',
     '--function-syntax','4',
    '--quantifier-syntax','4',
]

final DAFNY4_JAVA_BUILD_FLAGS2 = [
    'translate',
    '--no-verify',
    'java',
    '--output','build/libs/Driver'
    // '--function-syntax','4',
    // '--quantifier-syntax','4',
]

final DAFNY4_PY_BUILD_FLAGS = [
    'build',
    '--no-verify',
    '--target','py',
    '--output','build/libs/driver',
    '--function-syntax','4',
    '--quantifier-syntax','4',
]

final DAFNY4_CS_DOTNET_BUILD_FLAGS = [
    'build',
    '--no-verify',
    '--target','cs',
    '--output','build/libs/driver-cs/driver',
    '--function-syntax','4',
    '--quantifier-syntax','4',
]

final DAFNY4_RUST_BUILD_FLAGS = [
    'build',
    '--no-verify',
    '--target','rs',
    '--output','build/libs/driver',
    '--function-syntax','4',
    '--quantifier-syntax','4',
]

final DAFNY4_GO_BUILD_FLAGS = [
    'build',
    '--no-verify',
    '--target','go',
    '--output','build/libs/driver',
]

final DAFNY4_JS_BUILD_FLAGS = [
    'build',
    '--no-verify',
    '--target','js',
    '--output','build/libs/driver',
]

final DAFNY4_VERIFY_FLAGS = [
    'verify',
    '--verification-time-limit', '20',
    // '/dafnyVerify:1',
    // '--isolate-assertions'
    // '/compile:0',
    // '/rlimit:100000000',
    // '/timeLimit:20',
    // '--resource-limit','100000000',
    '--allow-warnings',
    '--cores','8',
    // '--verify-included-files',
    // '--log-format','csv;LogFileName=build/logs/verify.csv',
    // '--relax-definite-assignment',
    // '--function-syntax','4',
    // '--quantifier-syntax','4',
    // '/vcsCores:12', 
] 
// + Z3_OPTION + BOOGIE_FLAGS

final DAFNY4_TEST_FLAGS = [
    'test',
    '--verification-time-limit', '20',
    '--allow-warnings',
    '--output', 'build/tests/bin/test.cs', 
    // '--no-verify',
    // '--target','java',
    // '--function-syntax','4',
    // '--quantifier-syntax','4'
] // + Z3_OPTION

// ======================================================================
// Dafny Build
// ======================================================================

// Verify the DafnyEVM, whilst producing suitable logs
task verify {
    // Specify inputs
    inputs.files(fileTree('src/dafny/').include('**/*.dfy'))
    // Specify outputs
    outputs.files(fileTree('build/logs/').include('verify.csv'))
    // Enable caching
    outputs.cacheIf { true }
    // Specify actions
    doLast {
        // Create build directory (Dafny doesn't do this for us)
        mkdir "build/logs"
        //
        fileTree("src/dafny").include('**/*.dfy').exclude('tests/src/**/*.dfy').each {
            file -> 
            
                // Construct logging option
                def name = file.name.take(file.name.lastIndexOf('.'))
                def logging = '--log-format:csv;LogFileName=build/logs/' + name + '.csv'
                // def logging = '/verificationLogger:csv;LogFileName=build/logs/' + name + '.csv'
                // Run test
                // project.logger.info('my info message')
                project.logger.lifecycle('Verifying ' + [file])
                exec {
                    executable DAFNY_HOME + '/dafny'
                    args DAFNY4_VERIFY_FLAGS + logging + [file]
                }
            
        }
    }
}

task testDafny {
    // Specify inputs
    inputs.files(fileTree('test/dafny/').include('**/*.dfy'))
    // Specify outputs
    outputs.files(fileTree('build/logs/tests').include('verify.csv'))
    // Enable caching
    outputs.cacheIf { true }
    // Specify actions
    doLast {
        // Create build directory (Dafny doesn't do this for us)
        mkdir "build/logs"
        // Verify and execute all Dafny tests found in the test
        // directory.
        fileTree("test/dafny").include('**/*.dfy').each {
            file -> 
                // Construct logging option
                def name = file.name.take(file.name.lastIndexOf('.'))
                // def logging = '--log-format:csv;LogFileName=build/logs/' + name + '.csv'
                // def logging = '/verificationLogger:csv;LogFileName=build/logs/' + name + '.csv'
                // Run test
                // project.logger.info('my info message')
                project.logger.lifecycle('Testing ' + [file])
                exec {
                    executable DAFNY_HOME + '/dafny'
                    args DAFNY4_TEST_FLAGS + [file]
                }
        }
    }

}


// Translate Dafny source into Java source
task compileToJava {
    // Specify inputs
    inputs.files(fileTree('src/dafny/').include('**/*.dfy'))
    // Specify outputs
    outputs.files(fileTree('build/').include('libs/Driver-java/evmdis.jar'))
    // Enable caching
    outputs.cacheIf { true }  
    
    // Specify actions
    doLast {
        // Generate Dafny Source
        exec {
            // executable DAFNY_HOME + '/dafny'
            executable '/Users/franck/local/dafny-4.6/dafny'
            args DAFNY4_JAVA_BUILD_FLAGS + ['src/dafny/Driver.dfy']
        }
    }
}

task compileToPy {
    // Specify inputs
    inputs.files(fileTree('src/dafny/').include('**/*.dfy'))
    // Specify outputs
    outputs.files(fileTree('build/').include('libs/evmdis.py'))
    // Enable caching
    outputs.cacheIf { true }
    // Specify actions
    doLast {
        // Generate Dafny Source
        exec {
            executable DAFNY_HOME + '/dafny'
            args DAFNY4_PY_BUILD_FLAGS + ['src/dafny/Driver.dfy']
        }
        // copy {
        //     from "src/main/python"
        //     into "build/libs/Driver-py"
        //     include "*.py"
        // }
    }
}

task compileToCs {
    // Specify inputs
    inputs.files(fileTree('src/dafny/').include('**/*.dfy'))
    // Specify outputs
    // outputs.files(fileTree('build/').include('libs/evmdis.py'))
    // Enable caching
    outputs.cacheIf { true }
    // Specify actions
    doLast {
        // Generate Dafny Source
        exec {
            executable DAFNY_HOME + '/dafny'
            args DAFNY4_CS_DOTNET_BUILD_FLAGS + ['src/dafny/Driver.dfy']
        }
        // copy {
        //     from "src/main/python"
        //     into "build/libs/Driver-py"
        //     include "*.py"
        // }
    }
}

task compileToRust {
    // Specify inputs
    inputs.files(fileTree('src/dafny/').include('**/*.dfy'))
    // Specify outputs
    outputs.files(fileTree('build/').include('libs/rust/driver.rs'))
    // Enable caching
    outputs.cacheIf { true }
    // Specify actions
    doLast {
        // Generate Dafny Source
        exec {
            executable DAFNY_HOME + '/dafny'
            args DAFNY4_RUST_BUILD_FLAGS + ['src/dafny/Driver.dfy']
        }
    }
}

task compileToGo {
    // Specify inputs
    inputs.files(fileTree('src/dafny/').include('**/*.dfy'))
    // Specify outputs
    outputs.files(fileTree('build/').include('libs/go/driver.go'))
    // Enable caching
    outputs.cacheIf { true }
    // Specify actions
    doLast {
        // Generate Dafny Source
        exec {
            executable DAFNY_HOME + '/dafny'
            args DAFNY4_GO_BUILD_FLAGS + ['src/dafny/Driver.dfy']
        }
    }
}

task compileToJs {
    // Specify inputs
    inputs.files(fileTree('src/dafny/').include('**/*.dfy'))
    // Specify outputs
    outputs.files(fileTree('build/').include('libs/js/driver.js'))
    // Enable caching
    outputs.cacheIf { true }
    // Specify actions
    doLast {
        // Generate Dafny Source
        exec {
            // executable DAFNY_HOME + '/dafny'
            executable '/Users/franck/local/dafny-4.4/dafny'
            args DAFNY4_JS_BUILD_FLAGS + ['src/dafny/Driver.dfy']
        }
    }
}

task generateTestCFGs {
    // Specify inputs
    inputs.files(fileTree('src/dafny/').include('**/*.bin'))
    doLast {
        fileTree("src/dafny/tests/src/").include('**/*.bin').exclude('strings/**','vyper/harmony/CurveCryptoSwapHarmony.vy.bin', 'fibonacci/**').each {
            file -> 
                exec {
                    executable = './makeCFG.sh' 
                    args = [file]
                }
        }
    }
}

task verifyTestCFGs {
    // Specify inputs
    inputs.files(fileTree('src/dafny/').include('**/*.bin'))
    doLast {
        fileTree("src/dafny/tests/src/").include('**/*.bin').exclude('strings/**','vyper/harmony/CurveCryptoSwapHarmony.vy.bin', 'fibonacci/**').each {
            file -> 
                exec {
                    executable = './verifyCFG.sh' 
                    args = [file, 10]
                }
        }
    }
}

// generateTestCFGs.dependsOn compileToJava

task deleteTestBuild(type: Delete) {
    delete fileTree('test/dafny') {
        include '**/*.dll',  '**/*.json', '**/*.cs' , '**/*.csproj', '**/*.pdb'
    }
}

task deleteTestCFG(type: Delete) {
    delete fileTree('src/dafny/tests/src') {
        include '**/*.dot', '**/*.svg', '**/*.dfy'
    }
}

task cleanDafny(type: Delete) {
    delete fileTree('src/dafny') {
        include '**/*.dll',  '**/*.json'
    }
    delete "build/logs"
}

task cleanEtherscan(type: Delete) {
    delete fileTree('etherscan/') {
        include '**/*.dot',  '**/*.svg', '**/*.dfy'
    }
    // delete "build/logs"
}

task buildArtefacts 
buildArtefacts.dependsOn compileToJava, compileToPy, compileToCs 
// compileToJs

clean.dependsOn cleanDafny, deleteTestBuild



// ======================================================================
// Java Build
// ======================================================================

// repositories {
//     // Use MavenCentral for resolving dependencies
//     mavenCentral()
// }

// test {
//     dependsOn verify
//     // Specify inputs
//     inputs.files(fileTree('tests').include('**/*.json'))
//     // Ensure can see stdout
//     testLogging.showStandardStreams = true
//     // Ensure enough memory
//     jvmArgs '-Xmx2G','-Xss4m'
//     //
//     useJUnitPlatform()
//     filter {
//         includeTestsMatching('dafnyevm.Tests')
//         includeTestsMatching('dafnyevm.GeneralStateTests')
//     }
// }

// Specify that should run compileDafny before compileJava.
// Otherwise, the Java compiler cannot find up-to-date Dafny tests!
// compileJava.dependsOn compileDafny

// In this section you declare the dependencies for your production and test code
// dependencies {
//     implementation("commons-cli:commons-cli:1.5.0")
//     implementation("org.apache.commons:commons-lang3:3.12.0")
//     implementation("org.json:org.json:chargebee-1.0")
//     implementation("org.web3j:utils:5.0.0")
//     implementation("org.web3j:rlp:5.0.0")
//     implementation("org.web3j:crypto:5.0.0")
//     implementation("org.whiley:evmtools:0.3.27")
//     implementation("org.dafny:DafnyRuntime:4.2.0")
//     implementation files('build/libs/evm.jar')
//     //
//     testImplementation("org.junit.jupiter:junit-jupiter-api:5.7.0")
//     testImplementation("org.junit.jupiter:junit-jupiter-params:5.7.0")
//     testRuntimeOnly("org.junit.jupiter:junit-jupiter-engine:5.7.0")
// }


// ======================================================================
// Java Application
// ======================================================================

// application {
//     mainClass = 'driver.Main'
//     applicationName = 'driver'
// }