String concat transformer (#214)

UnitTestBot · Nov 18, 2024 · d9ed8c0 · d9ed8c0
1 parent 158ad96
commit d9ed8c0
Show file tree

Hide file tree

Showing 9 changed files with 631 additions and 251 deletions.
diff --git a/usvm-jvm/build.gradle.kts b/usvm-jvm/build.gradle.kts
@@ -10,6 +10,12 @@ val samples by sourceSets.creating {
     }
 }
 
+val `samples-jdk11` by sourceSets.creating {
+    java {
+        srcDir("src/samples-jdk11/java")
+    }
+}
+
 val `sample-approximations` by sourceSets.creating {
     java {
         srcDir("src/sample-approximations/java")
@@ -92,9 +98,20 @@ val `usvm-api-jar` = tasks.register<Jar>("usvm-api-jar") {
 val testSamples by configurations.creating
 val testSamplesWithApproximations by configurations.creating
 
+val compileSamplesJdk11 = tasks.register<JavaCompile>("compileSamplesJdk11") {
+    sourceCompatibility = JavaVersion.VERSION_11.toString()
+    targetCompatibility = JavaVersion.VERSION_11.toString()
+
+    source = `samples-jdk11`.java
+    classpath = `samples-jdk11`.compileClasspath
+    options.sourcepath = `samples-jdk11`.java
+    destinationDirectory = `samples-jdk11`.java.destinationDirectory
+}
+
 dependencies {
     testSamples(samples.output)
     testSamples(`usvm-api`.output)
+    testSamples(files(`samples-jdk11`.java.destinationDirectory))
 
     testSamplesWithApproximations(samples.output)
     testSamplesWithApproximations(`usvm-api`.output)
@@ -104,7 +121,7 @@ dependencies {
 
 tasks.withType<Test> {
     dependsOn(`usvm-api-jar`)
-    dependsOn(testSamples, testSamplesWithApproximations)
+    dependsOn(compileSamplesJdk11, testSamples, testSamplesWithApproximations)
 
     val usvmApiJarPath = `usvm-api-jar`.get().outputs.files.singleFile
     val usvmApproximationJarPath = approximations.resolvedConfiguration.files.single()

diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcExprResolver.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcExprResolver.kt
@@ -103,6 +103,9 @@ import org.usvm.machine.interpreter.statics.JcStaticFieldRegionId
 import org.usvm.machine.interpreter.statics.JcStaticFieldsMemoryRegion
 import org.usvm.machine.interpreter.statics.isInitialized
 import org.usvm.machine.interpreter.statics.markAsInitialized
+import org.usvm.machine.interpreter.transformers.JcMultiDimArrayAllocationTransformer
+import org.usvm.machine.interpreter.transformers.JcStringConcatTransformer
+import org.usvm.machine.logger
 import org.usvm.machine.operator.JcBinaryOperator
 import org.usvm.machine.operator.JcUnaryOperator
 import org.usvm.machine.operator.ensureBvExpr
@@ -408,7 +411,11 @@ class JcExprResolver(
         }
 
     override fun visitJcDynamicCallExpr(expr: JcDynamicCallExpr): UExpr<out USort>? =
-        resolveInvoke(
+        apply {
+            if (JcStringConcatTransformer.methodIsStringConcat(expr.method.method)) {
+                logger.warn { "JcStringConcatTransformer should be used to process string concatenation" }
+            }
+        }.resolveInvoke(
             expr.method,
             instanceExpr = null,
             argumentExprs = { expr.callSiteArgs },

diff --git a/...-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcMultiDimArrayAllocationTransformer.kt b/...-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcMultiDimArrayAllocationTransformer.kt