diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml index 4bcf935..b495b2c 100644 --- a/.github/workflows/gradle.yml +++ b/.github/workflows/gradle.yml @@ -1,81 +1,85 @@ -# This workflow uses actions that are not certified by GitHub. -# They are provided by a third-party and are governed by -# separate terms of service, privacy policy, and support -# documentation. -# This workflow will build a Java project with Gradle and cache/restore any dependencies to improve the workflow execution time -# For more information see: https://docs.github.com/en/actions/automating-builds-and-tests/building-and-testing-java-with-gradle - name: Java CI with Gradle on: push: - branches: [ "main" ] pull_request: - branches: [ "main" ] jobs: build: - runs-on: ubuntu-latest permissions: contents: read - steps: - - uses: actions/checkout@v4 + - uses: actions/checkout@v5 - name: Set up JDK 17 uses: actions/setup-java@v4 with: java-version: '17' distribution: 'temurin' - - # Configure Gradle for optimal use in GiHub Actions, including caching of downloaded dependencies. - # See: https://github.com/gradle/actions/blob/main/setup-gradle/README.md - name: Setup Gradle - uses: gradle/actions/setup-gradle@ec92e829475ac0c2315ea8f9eced72db85bb337a # v3.0.0 - + uses: gradle/actions/setup-gradle@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4 - name: Build run: ./gradlew build -x test + test: + needs: build + runs-on: ubuntu-latest + permissions: + contents: read + steps: + - uses: actions/checkout@v5 + - name: Set up JDK 17 + uses: actions/setup-java@v4 + with: + java-version: '17' + distribution: 'temurin' + - name: Setup Gradle + uses: gradle/actions/setup-gradle@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4 - name: Copy Z3 run: ./gradlew copyNativeLibs - - name: Test run: ./gradlew test - - - name: Upload test reports if failed + - name: Upload test reports if: failure() - uses: actions/upload-artifact@v3 + uses: actions/upload-artifact@v4 with: name: test-reports - path: /home/runner/work/SWAT/SWAT/symbolic-executor/build/reports/tests + path: symbolic-executor/build/reports/tests - - - name: Test + javadoc: + needs: build + if: github.event_name == 'push' && github.ref == 'refs/heads/main' + runs-on: ubuntu-latest + permissions: + contents: read + steps: + - uses: actions/checkout@v5 + - name: Set up JDK 17 + uses: actions/setup-java@v4 + with: + java-version: '17' + distribution: 'temurin' + - name: Setup Gradle + uses: gradle/actions/setup-gradle@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4 + - name: Generate Javadoc run: ./gradlew javadoc - - - - name: Upload javadoc - uses: actions/upload-artifact@v3 + - name: Upload Javadoc + uses: actions/upload-artifact@v4 with: name: javadoc - path: /home/runner/work/SWAT/SWAT/symbolic-executor/build/docs/javadoc - + path: symbolic-executor/build/docs/javadoc dependency-submission: - + if: github.event_name == 'push' && github.ref == 'refs/heads/main' runs-on: ubuntu-latest permissions: contents: write - steps: - - uses: actions/checkout@v4 + - uses: actions/checkout@v5 - name: Set up JDK 17 uses: actions/setup-java@v4 with: java-version: '17' distribution: 'temurin' - - # Generates and submits a dependency graph, enabling Dependabot Alerts for all project dependencies. - # See: https://github.com/gradle/actions/blob/main/dependency-submission/README.md - name: Generate and submit dependency graph - uses: gradle/actions/dependency-submission@ec92e829475ac0c2315ea8f9eced72db85bb337a # v3.0.0 + uses: gradle/actions/dependency-submission@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4 diff --git a/settings.gradle b/settings.gradle index 2861754..defcd23 100644 --- a/settings.gradle +++ b/settings.gradle @@ -67,7 +67,7 @@ dependencyResolutionManagement { library('asm-util', 'org.ow2.asm','asm-util').versionRef('asm') library('asm-tree', 'org.ow2.asm','asm-tree').versionRef('asm') library('jackson-databind', 'com.fasterxml.jackson.core:jackson-databind:2.14.1') - library('java-smt', 'org.sosy-lab:java-smt:5.0.1') + library('java-smt', 'org.sosy-lab:java-smt:6.0.0') library('spock-core', 'org.spockframework:spock-core:2.2-M1-groovy-4.0') library('mockito-core', 'org.mockito:mockito-core:3.12.4') library('logback-classic', 'ch.qos.logback:logback-classic:1.5.3') diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/metadata/ClassDepot.java b/symbolic-executor/src/main/java/de/uzl/its/swat/metadata/ClassDepot.java index b1f69d3..ee0bee3 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/metadata/ClassDepot.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/metadata/ClassDepot.java @@ -66,12 +66,20 @@ public static ClassDepotInstrumentation getInstrumentationInstance() { /** * Registers type metadata (parent and interface names) for a class. + * Idempotent: silently returns if the class is already registered with identical metadata. + * Asserts if the class is already registered with different metadata. */ public synchronized void registerTypeInfoForClass(String className, List parents, List interfaces) { String normalized = Util.formatClassName(className); + if (ancestorBaseCache.containsKey(normalized)) { + SWATAssert.enforce( + parents.equals(classToParents.get(normalized)) + && interfaces.equals(classToInterfaces.get(normalized)), + "Class " + normalized + " already registered in ancestorBaseCache with different metadata"); + return; + } classToParents.put(normalized, parents); classToInterfaces.put(normalized, interfaces); - SWATAssert.enforce(!ancestorBaseCache.containsKey(normalized), "Class " + normalized + " already registered in ancestorBaseCache"); } public synchronized List getParentsForClass(String className) { diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/instrument/AbstractMethodAdapterTest.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/instrument/AbstractMethodAdapterTest.groovy deleted file mode 100644 index 32b1230..0000000 --- a/symbolic-executor/src/test/groovy/de/uzl/its/swat/instrument/AbstractMethodAdapterTest.groovy +++ /dev/null @@ -1,228 +0,0 @@ -package de.uzl.its.swat.instrument - -import org.objectweb.asm.MethodVisitor -import spock.lang.Shared -import spock.lang.Specification -import spock.lang.Unroll - -import static org.mockito.Mockito.mock - -import org.objectweb.asm.Opcodes - -class AbstractMethodAdapterTest extends Specification { - - - MethodVisitor mv = Mock(MethodVisitor) - - def "splitParameters should return correct parameter types"() { - given: - AbstractMethodAdapter adapter = new ConcreteMethodAdapter(mv, "someMethod", "(IZLjava/lang/String;)[I") - - when: - def result = adapter.splitParameters("(IZLjava/lang/String;)[I") - - then: - result == ["I", "Z", "Ljava/lang/String;"] - } - - def "splitParameters should return empty list when no parameters are provided"() { - given: - AbstractMethodAdapter adapter = new ConcreteMethodAdapter(mv, "someMethod", "(IZLjava/lang/String;)[I") - when: - def result = adapter.splitParameters("()V") - - then: - result.isEmpty() - } - - def "splitParameters should correctly identify single primitive type"() { - given: - AbstractMethodAdapter adapter = new ConcreteMethodAdapter(mv, "someMethod", "(IZLjava/lang/String;)[I") - when: - def result = adapter.splitParameters("(I)V") - - then: - result == ['I'] - } - - def "splitParameters should correctly identify single object type"() { - given: - AbstractMethodAdapter adapter = new ConcreteMethodAdapter(mv, "someMethod", "(IZLjava/lang/String;)[I") - when: - def result = adapter.splitParameters("(Ljava/lang/String;)V") - - then: - result == ['Ljava/lang/String;'] - } - - def "splitParameters should correctly identify array types"() { - given: - AbstractMethodAdapter adapter = new ConcreteMethodAdapter(mv, "someMethod", "(IZLjava/lang/String;)[I") - when: - def result = adapter.splitParameters("(I[Ljava/lang/String;[[Z)V") - - then: - result == ['I', '[Ljava/lang/String;', '[[Z'] - } - - def "splitParameters should correctly identify mixed types"() { - given: - AbstractMethodAdapter adapter = new ConcreteMethodAdapter(mv, "someMethod", "(IZLjava/lang/String;)[I") - when: - def result = adapter.splitParameters("(IZLjava/lang/Object;[I)V") - - then: - result == ['I', 'Z', 'Ljava/lang/Object;', '[I'] - } - - def "splitParameters should correctly identify parameters regardless of return value"() { - given: - AbstractMethodAdapter adapter = new ConcreteMethodAdapter(mv, "someMethod", "(IZLjava/lang/String;)[I") - when: - def result = adapter.splitParameters("(IZLjava/lang/Object;[I)[[Ljava/lang/Object;") - - then: - result == ['I', 'Z', 'Ljava/lang/Object;', '[I'] - } - - def "splitParameters should return empty list when descriptor does not match pattern"() { - given: - AbstractMethodAdapter adapter = new ConcreteMethodAdapter(mv, "someMethod", "(IZLjava/lang/String;)[I") - when: - def result = adapter.splitParameters("IV") - - then: - result.isEmpty() - } - - def "symbolicInt should invoke the correct sequence of visit methods"() { - given: - AbstractMethodAdapter adapter = new ConcreteMethodAdapter(mv, "someMethod", "(I)V") - - when: - adapter.symbolicInt(1) - - then: - 1 * mv.visitVarInsn(Opcodes.ILOAD, 1) - 1 * mv.visitMethodInsn(Opcodes.INVOKESTATIC, "de/uzl/its/swat/Main", "MakeSymbolic", "(I)I", false) - 1 * mv.visitVarInsn(Opcodes.ISTORE, 1) - } - def "symbolicByte should invoke the correct sequence of visit methods"() { - given: - AbstractMethodAdapter adapter = new ConcreteMethodAdapter(mv, "someMethod", "(I)V") - - when: - adapter.symbolicByte(1) - - then: - 1 * mv.visitVarInsn(Opcodes.ILOAD, 1) - 1 * mv.visitMethodInsn(Opcodes.INVOKESTATIC, "de/uzl/its/swat/Main", "MakeSymbolic", "(B)B", false) - 1 * mv.visitVarInsn(Opcodes.ISTORE, 1) - } - def "symbolicShort should invoke the correct sequence of visit methods"() { - given: - AbstractMethodAdapter adapter = new ConcreteMethodAdapter(mv, "someMethod", "(I)V") - - when: - adapter.symbolicShort(1) - - then: - 1 * mv.visitVarInsn(Opcodes.ILOAD, 1) - 1 * mv.visitMethodInsn(Opcodes.INVOKESTATIC, "de/uzl/its/swat/Main", "MakeSymbolic", "(S)S", false) - 1 * mv.visitVarInsn(Opcodes.ISTORE, 1) - } - def "symbolicLong should invoke the correct sequence of visit methods"() { - given: - AbstractMethodAdapter adapter = new ConcreteMethodAdapter(mv, "someMethod", "(I)V") - - when: - adapter.symbolicLong(1) - - then: - 1 * mv.visitVarInsn(Opcodes.LLOAD, 1) - 1 * mv.visitMethodInsn(Opcodes.INVOKESTATIC, "de/uzl/its/swat/Main", "MakeSymbolic", "(J)J", false) - 1 * mv.visitVarInsn(Opcodes.LSTORE, 1) - } - - def "symbolicFloat should invoke the correct sequence of visit methods"() { - given: - AbstractMethodAdapter adapter = new ConcreteMethodAdapter(mv, "someMethod", "(I)V") - - when: - adapter.symbolicFloat(1) - - then: - 1 * mv.visitVarInsn(Opcodes.FLOAD, 1) - 1 * mv.visitMethodInsn(Opcodes.INVOKESTATIC, "de/uzl/its/swat/Main", "MakeSymbolic", "(F)F", false) - 1 * mv.visitVarInsn(Opcodes.FSTORE, 1) - } - def "symbolicDouble should invoke the correct sequence of visit methods"() { - given: - AbstractMethodAdapter adapter = new ConcreteMethodAdapter(mv, "someMethod", "(I)V") - - when: - adapter.symbolicDouble(1) - - then: - 1 * mv.visitVarInsn(Opcodes.DLOAD, 1) - 1 * mv.visitMethodInsn(Opcodes.INVOKESTATIC, "de/uzl/its/swat/Main", "MakeSymbolic", "(D)D", false) - 1 * mv.visitVarInsn(Opcodes.DSTORE, 1) - } - def "symbolicBoolean should invoke the correct sequence of visit methods"() { - given: - AbstractMethodAdapter adapter = new ConcreteMethodAdapter(mv, "someMethod", "(I)V") - - when: - adapter.symbolicBoolean(1) - - then: - 1 * mv.visitVarInsn(Opcodes.ILOAD, 1) - 1 * mv.visitMethodInsn(Opcodes.INVOKESTATIC, "de/uzl/its/swat/Main", "MakeSymbolic", "(Z)Z", false) - 1 * mv.visitVarInsn(Opcodes.ISTORE, 1) - } - - def "symbolicChar should invoke the correct sequence of visit methods"() { - given: - AbstractMethodAdapter adapter = new ConcreteMethodAdapter(mv, "someMethod", "(I)V") - - when: - adapter.symbolicChar(1) - - then: - 1 * mv.visitVarInsn(Opcodes.ILOAD, 1) - 1 * mv.visitMethodInsn(Opcodes.INVOKESTATIC, "de/uzl/its/swat/Main", "MakeSymbolic", "(C)C", false) - 1 * mv.visitVarInsn(Opcodes.ISTORE, 1) - } - - def "symbolicString should invoke the correct sequence of visit methods"() { - given: - AbstractMethodAdapter adapter = new ConcreteMethodAdapter(mv, "someMethod", "(I)V") - - when: - adapter.symbolicString(1) - - then: - 1 * mv.visitVarInsn(Opcodes.ALOAD, 1) - 1 * mv.visitMethodInsn(Opcodes.INVOKESTATIC, "de/uzl/its/swat/Main", "MakeSymbolic", "(Ljava/lang/String;)Ljava/lang/String;", false) - 1 * mv.visitVarInsn(Opcodes.ASTORE, 1) - } - def "symbolicLongObject should invoke the correct sequence of visit methods"() { - given: - AbstractMethodAdapter adapter = new ConcreteMethodAdapter(mv, "someMethod", "(I)V") - - when: - adapter.symbolicLongObject(1) - - then: - 1 * mv.visitVarInsn(Opcodes.ALOAD, 1) - 1 * mv.visitMethodInsn(Opcodes.INVOKESTATIC, "de/uzl/its/swat/Main", "MakeSymbolic", "(Ljava/lang/Long;)Ljava/lang/Long;", false) - 1 * mv.visitVarInsn(Opcodes.ASTORE, 1) - } - -} - -class ConcreteMethodAdapter extends AbstractMethodAdapter { - ConcreteMethodAdapter(MethodVisitor mv, String name, String desc) { - super(mv, name, desc) - } -}