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.
 */

// 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'
// Use default Z3 version
def Z3_PATH = null

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

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

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

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


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

final DAFNY4_BUILD_FLAGS = [
    'build',
    '--no-verify',
    '--allow-warnings',
    '--target','java',
    '--output','build/libs/evm',
    '--function-syntax','4',
    '--quantifier-syntax','4',
]

final DAFNY4_VERIFY_FLAGS = [
    'verify',
    '--allow-warnings',    
    '--resource-limit','1000000',
    '--verify-included-files',
    '--log-format','csv;LogFileName=build/logs/verify.csv',
    '--function-syntax','4',
    '--quantifier-syntax','4',
] + Z3_OPTION + BOOGIE_FLAGS

final DAFNY4_TEST_FLAGS = [
    'test',
    '--allow-warnings',    
    '--target','java',
    '--function-syntax','4',
    '--quantifier-syntax','4'
]  + Z3_OPTION

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

// Verify the DafnyEVM, whilst producing suitable logs
task verifyDafny {
    // 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"
        // Generate Dafny Source
        exec {
            executable DAFNY_EXE
            args DAFNY4_VERIFY_FLAGS + ['src/dafny/evm.dfy']
        }
    }
}

// Translate Dafny source into Java source
task compileDafny {
    // Specify inputs
    inputs.files(fileTree('src/dafny/').include('**/*.dfy'))
    // Specify outputs
    outputs.files(fileTree('build/').include('libs/evm.jar'))
    // Enable caching
    outputs.cacheIf { true }
    // Specify actions
    doLast {
        // Generate Dafny Source
        exec {
            executable DAFNY_EXE
            args DAFNY4_BUILD_FLAGS + ['src/dafny/evm.dfy']
        }
    }
}

task cleanDafny {
    doLast {
        delete "build/evm-java"
    }
}

clean.dependsOn cleanDafny

// ======================================================================
// Dafny Tests
// ======================================================================

task testDafny {
    // Specify inputs
    inputs.files(fileTree('src').include('**/*.dfy'))
    // Specify outputs
    outputs.files(fileTree('build/logs').include('**/test_*.csv'))
    // Require code gen
    dependsOn verifyDafny
    // Specify actions
    doLast {
        // Verify and execute all Dafny tests found in the test
        // directory.
        fileTree("src/test/dafny").include('**/*.dfy').each {
            File file -> {
                // Construct logging option
                def name = file.name.take(file.name.lastIndexOf('.'))
                def logging = '--log-format:csv;LogFileName=build/logs/test_' + name + '.csv'
                // Run test
                exec {
                    executable DAFNY_EXE
                    args DAFNY4_TEST_FLAGS + [logging,file]
                }
            }
        }
    }
}

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

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

test {
    dependsOn testDafny
    // 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.30")
    //implementation files('build/libs/EvmTools-0.3.30.jar')        
    implementation("org.dafny:DafnyRuntime:4.4.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")
}

// ======================================================================
// Trace Generation
// ======================================================================

// A default task for convert reference tests into the trace format
// required for testing the Dafny evm.
task testgen(type: JavaExec) {
    // Specify inputs
    inputs.files("tests/includes.txt", "tests/excludes.txt",
                 fileTree('fixtures/').include('**/*.json'))
    // Specify outputs
    outputs.files(fileTree('tests').include('**/*.json'))
    // Enable caching
    outputs.cacheIf { true }
    // Specify actions
    classpath = sourceSets.main.runtimeClasspath
    mainClass = 'evmtools.Main'
    // Ensure enough memory
    jvmArgs '-Xmx8G','-Xss4m'
    // arguments to pass to the application
    args '-incremental'
    args '-forks'
    args 'Berlin,London,Shanghai,Cancun'
    args '-dir'
    args 'fixtures'
    args '-out'
    args 'tests'
    args '-includes'
    args 'tests/includes.txt'
    args '-excludes'
    args 'tests/excludes.txt'
}

/// A task which summarises generated verification logs in a useful
/// manner.
task debug(type: JavaExec) {
    // Specify actions
    classpath = sourceSets.main.runtimeClasspath
    mainClass = 'dafnyevm.util.DafnyLogSummariser'
    // Report 20 entries
    args '-entries'
    args '20'
    // Identify log files
    args 'build/logs/*.csv'
}

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

application {
    mainClass = 'dafnyevm.Main'
    applicationName = 'dafnyevm'
}