fixes in SMT and inlining

vorpal-research · Jul 6, 2023 · f2eddf2 · f2eddf2
1 parent a233ce0
commit f2eddf2
Show file tree

Hide file tree

Showing 6 changed files with 87 additions and 70 deletions.
diff --git a/kex-annotation-processor/src/main/resources/SMTConverter.vm b/kex-annotation-processor/src/main/resources/SMTConverter.vm
@@ -446,12 +446,14 @@ class ${solver}Converter(
 
         val typeVar = ef.getTypeVar(newarray.lhv.type.getKfgType(executionContext.types))
         val initialType = ctx.readBitvectorInitialProperty(lhv, memspace, "type")
+        val initialLength = ctx.readWordInitialProperty(lhv, memspace, "length")
 
         val lengthProperty = ctx.readWordProperty(lhv, memspace, "length")
         return lhv
             .withPtrAxioms(ef, ctx, TermType.LOCAL_PTR)
             .withAxiom(lengthProperty ge ef.makeIntConst(0)) eq ptr
             .withAxiom(initialType eq typeVar)
+            .withAxiom(initialLength eq length)
             .withAxiom(initialArrayMemory eq array)
     }
 

diff --git a/...c/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt b/...c/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt
@@ -112,7 +112,7 @@ class InstructionConcolicChecker(
     }
 
     private suspend fun check(method: Method, state: SymbolicState): ExecutionResult? = tryOrNull {
-        method.checkAsync(ctx, state)?.let { collectTrace(method, it) }
+        method.checkAsync(ctx, state, enableInlining = true)?.let { collectTrace(method, it) }
     }
 
     private fun buildPathSelector() = when (searchStrategy) {

diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/util/extensions.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/util/extensions.kt
@@ -49,7 +49,11 @@ suspend fun Method.analyzeOrTimeout(
     }
 }
 
-suspend fun Method.checkAsync(ctx: ExecutionContext, state: SymbolicState): Parameters<Descriptor>? {
+suspend fun Method.checkAsync(
+    ctx: ExecutionContext,
+    state: SymbolicState,
+    enableInlining: Boolean = false
+): Parameters<Descriptor>? {
     val checker = AsyncChecker(this, ctx)
     val clauses = state.clauses.asState()
     val query = state.path.asState()
@@ -58,7 +62,7 @@ suspend fun Method.checkAsync(ctx: ExecutionContext, state: SymbolicState): Para
         .filterValues { it.isJavaRt }
         .mapValues { it.value.rtMapped }
         .toTypeMap()
-    val result = checker.prepareAndCheck(this, clauses + query, concreteTypeInfo)
+    val result = checker.prepareAndCheck(this, clauses + query, concreteTypeInfo, enableInlining)
     if (result !is Result.SatResult) {
         return null
     }
@@ -79,7 +83,8 @@ suspend fun Method.checkAsync(ctx: ExecutionContext, state: SymbolicState): Para
 @Suppress("unused")
 suspend fun Method.checkAsyncAndSlice(
     ctx: ExecutionContext,
-    state: SymbolicState
+    state: SymbolicState,
+    enableInlining: Boolean = false
 ): Pair<Parameters<Descriptor>, ConstraintExceptionPrecondition>? {
     val checker = AsyncChecker(this, ctx)
     val clauses = state.clauses.asState()
@@ -89,7 +94,7 @@ suspend fun Method.checkAsyncAndSlice(
         .filterValues { it.isJavaRt }
         .mapValues { it.value.rtMapped }
         .toTypeMap()
-    val result = checker.prepareAndCheck(this, clauses + query, concreteTypeInfo)
+    val result = checker.prepareAndCheck(this, clauses + query, concreteTypeInfo, enableInlining)
     if (result !is Result.SatResult) {
         return null
     }
@@ -121,7 +126,8 @@ suspend fun Method.checkAsyncAndSlice(
 suspend fun Method.checkAsyncIncremental(
     ctx: ExecutionContext,
     state: SymbolicState,
-    queries: List<SymbolicState>
+    queries: List<SymbolicState>,
+    enableInlining: Boolean = false
 ): List<Parameters<Descriptor>?> {
     val checker = AsyncIncrementalChecker(this, ctx)
     val clauses = state.clauses.asState()
@@ -138,7 +144,8 @@ suspend fun Method.checkAsyncIncremental(
             clauses + query,
             queries.map { PredicateQuery(it.clauses.asState() + it.path.asState()) }.toPersistentList()
         ),
-        concreteTypeInfo
+        concreteTypeInfo,
+        enableInlining
     )
 
     return results.mapIndexed { index, result ->
@@ -166,7 +173,8 @@ suspend fun Method.checkAsyncIncremental(
 suspend fun Method.checkAsyncIncrementalAndSlice(
     ctx: ExecutionContext,
     state: SymbolicState,
-    queries: List<SymbolicState>
+    queries: List<SymbolicState>,
+    enableInlining: Boolean = false
 ): List<Pair<Parameters<Descriptor>, ConstraintExceptionPrecondition>?> {
     val checker = AsyncIncrementalChecker(this, ctx)
     val clauses = state.clauses.asState()
@@ -183,7 +191,8 @@ suspend fun Method.checkAsyncIncrementalAndSlice(
             clauses + query,
             queries.map { PredicateQuery(it.clauses.asState() + it.path.asState()) }.toPersistentList()
         ),
-        concreteTypeInfo
+        concreteTypeInfo,
+        enableInlining
     )
 
     return results.mapIndexed { index, result ->

diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/launcher/CrashReproductionLauncher.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/launcher/CrashReproductionLauncher.kt
@@ -98,7 +98,7 @@ class CrashReproductionLauncher(
         executePipeline(context.cm, Package.defaultPackage) {
             +ClassInstantiationDetector(context, context.accessLevel)
         }
-        val testCases = CrashReproductionChecker.runWithConstraintPreconditions(context, stackTrace)
+        val testCases = CrashReproductionChecker.runWithDescriptorPreconditions(context, stackTrace)
         if (testCases.isNotEmpty()) {
             log.info("Reproducing test cases:\n${testCases.joinToString("\n")}")
         }

diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncChecker.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncChecker.kt
@@ -33,12 +33,12 @@ import org.vorpal.research.kex.state.transformer.Slicer
 import org.vorpal.research.kex.state.transformer.StensgaardAA
 import org.vorpal.research.kex.state.transformer.StringMethodAdapter
 import org.vorpal.research.kex.state.transformer.TermCollector
-import org.vorpal.research.kex.state.transformer.transform
 import org.vorpal.research.kex.state.transformer.TypeInfoMap
 import org.vorpal.research.kex.state.transformer.TypeNameAdapter
 import org.vorpal.research.kex.state.transformer.collectRequiredTerms
 import org.vorpal.research.kex.state.transformer.collectVariables
 import org.vorpal.research.kex.state.transformer.toTypeMap
+import org.vorpal.research.kex.state.transformer.transform
 import org.vorpal.research.kfg.ir.Method
 import org.vorpal.research.kthelper.logging.debug
 import org.vorpal.research.kthelper.logging.log
@@ -60,28 +60,31 @@ class AsyncChecker(
     fun prepareState(
         method: Method,
         state: PredicateState,
-        typeMap: TypeInfoMap
+        typeMap: TypeInfoMap,
+        enableInlining: Boolean
     ): PredicateState = transform(state) {
         +KexRtAdapter(ctx.cm)
-        +RecursiveInliner(psa) { index, psa ->
-            ConcolicInliner(
-                ctx,
-                typeMap,
-                psa,
-                inlineSuffix = "inlined",
-                inlineIndex = index,
-                kexRtOnly = false
-            )
-        }
-        +RecursiveInliner(psa) { index, psa ->
-            ConcolicInliner(
-                ctx,
-                typeMap,
-                psa,
-                inlineSuffix = "rt.inlined",
-                inlineIndex = index,
-                kexRtOnly = true
-            )
+        if (enableInlining) {
+            +RecursiveInliner(psa) { index, psa ->
+                ConcolicInliner(
+                    ctx,
+                    typeMap,
+                    psa,
+                    inlineSuffix = "inlined",
+                    inlineIndex = index,
+                    kexRtOnly = false
+                )
+            }
+            +RecursiveInliner(psa) { index, psa ->
+                ConcolicInliner(
+                    ctx,
+                    typeMap,
+                    psa,
+                    inlineSuffix = "rt.inlined",
+                    inlineIndex = index,
+                    kexRtOnly = true
+                )
+            }
         }
         +ClassAdapter(ctx.cm)
         +AnnotationAdapter(method, AnnotationManager.defaultLoader)
@@ -105,17 +108,18 @@ class AsyncChecker(
     suspend fun prepareAndCheck(
         method: Method,
         state: PredicateState,
-        typeMap: TypeInfoMap = emptyMap<Term, KexType>().toTypeMap()
+        typeMap: TypeInfoMap = emptyMap<Term, KexType>().toTypeMap(),
+        enableInlining: Boolean = false
     ): Result {
-        val preparedState = prepareState(method, state, typeMap)
+        val preparedState = prepareState(method, state, typeMap, enableInlining)
         log.debug { "Prepared state: $preparedState" }
         return check(preparedState)
     }
 
     suspend fun check(ps: PredicateState, qry: PredicateState = emptyState()): Result {
         state = ps
         query = qry
-        if (logQuery) log.debug("State: $state")
+        if (logQuery) log.debug("State: {}", state)
 
         if (isSlicingEnabled) {
             log.debug("Slicing started...")
@@ -145,16 +149,16 @@ class AsyncChecker(
         state = Optimizer().apply(state)
         query = Optimizer().apply(query)
         if (logQuery) {
-            log.debug("Simplified state: $state")
-            log.debug("State size: ${state.size}")
-            log.debug("Query: $query")
-            log.debug("Query size: ${query.size}")
+            log.debug("Simplified state: {}", state)
+            log.debug("State size: {}", state.size)
+            log.debug("Query: {}", query)
+            log.debug("Query size: {}", query.size)
         }
 
         val result = AsyncSMTProxySolver(ctx).use {
             it.isPathPossibleAsync(state, query)
         }
-        log.debug("Acquired $result")
+        log.debug("Acquired {}", result)
         return result
     }
 }
diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncIncrementalChecker.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncIncrementalChecker.kt
@@ -1,15 +1,13 @@
 package org.vorpal.research.kex.smt
 
 import org.vorpal.research.kex.ExecutionContext
-import org.vorpal.research.kex.annotations.AnnotationManager
 import org.vorpal.research.kex.asm.state.PredicateStateAnalysis
 import org.vorpal.research.kex.config.kexConfig
 import org.vorpal.research.kex.ktype.KexType
 import org.vorpal.research.kex.state.IncrementalPredicateState
 import org.vorpal.research.kex.state.PredicateQuery
 import org.vorpal.research.kex.state.PredicateState
 import org.vorpal.research.kex.state.term.Term
-import org.vorpal.research.kex.state.transformer.AnnotationAdapter
 import org.vorpal.research.kex.state.transformer.BoolTypeAdapter
 import org.vorpal.research.kex.state.transformer.ClassAdapter
 import org.vorpal.research.kex.state.transformer.ClassMethodAdapter
@@ -50,28 +48,31 @@ class AsyncIncrementalChecker(
     private fun prepareState(
         method: Method,
         state: IncrementalPredicateState,
-        typeMap: TypeInfoMap
+        typeMap: TypeInfoMap,
+        enableInlining: Boolean
     ): IncrementalPredicateState = transformIncremental(state) {
         +KexRtAdapter(ctx.cm)
-        +RecursiveInliner(psa) { index, psa ->
-            ConcolicInliner(
-                ctx,
-                typeMap,
-                psa,
-                inlineSuffix = "inlined",
-                inlineIndex = index,
-                kexRtOnly = false
-            )
-        }
-        +RecursiveInliner(psa) { index, psa ->
-            ConcolicInliner(
-                ctx,
-                typeMap,
-                psa,
-                inlineSuffix = "rt.inlined",
-                inlineIndex = index,
-                kexRtOnly = true
-            )
+        if (enableInlining) {
+            +RecursiveInliner(psa) { index, psa ->
+                ConcolicInliner(
+                    ctx,
+                    typeMap,
+                    psa,
+                    inlineSuffix = "inlined",
+                    inlineIndex = index,
+                    kexRtOnly = false
+                )
+            }
+            +RecursiveInliner(psa) { index, psa ->
+                ConcolicInliner(
+                    ctx,
+                    typeMap,
+                    psa,
+                    inlineSuffix = "rt.inlined",
+                    inlineIndex = index,
+                    kexRtOnly = true
+                )
+            }
         }
         +ClassAdapter(ctx.cm)
 //        +AnnotationAdapter(method, AnnotationManager.defaultLoader)
@@ -94,9 +95,10 @@ class AsyncIncrementalChecker(
     suspend fun prepareAndCheck(
         method: Method,
         state: IncrementalPredicateState,
-        typeMap: TypeInfoMap = emptyMap<Term, KexType>().toTypeMap()
+        typeMap: TypeInfoMap = emptyMap<Term, KexType>().toTypeMap(),
+        enableInlining: Boolean = false
     ): List<Result> {
-        val preparedState = prepareState(method, state, typeMap)
+        val preparedState = prepareState(method, state, typeMap, enableInlining)
         log.debug { "Prepared state: $preparedState" }
         return check(preparedState.state, preparedState.queries)
     }
@@ -108,8 +110,8 @@ class AsyncIncrementalChecker(
         state = ps
         queries = query
         if (logQuery) {
-            log.debug("State: $state")
-            log.debug("Queries: $queries")
+            log.debug("State: {}", state)
+            log.debug("Queries: {}", queries)
         }
 
         state = Optimizer().apply(state)
@@ -122,16 +124,16 @@ class AsyncIncrementalChecker(
             }
         }
         if (logQuery) {
-            log.debug("Simplified state: $state")
-            log.debug("State size: ${state.size}")
-            log.debug("Query: $query")
-            log.debug("Query size: ${query.size}")
+            log.debug("Simplified state: {}", state)
+            log.debug("State size: {}", state.size)
+            log.debug("Query: {}", query)
+            log.debug("Query size: {}", query.size)
         }
 
         val results = AsyncIncrementalSMTProxySolver(ctx).use {
             it.isSatisfiableAsync(state, queries)
         }
-        log.debug("Acquired $results")
+        log.debug("Acquired {}", results)
         return results
     }
 }