transformer that adds basic invariants every time

vorpal-research · Jul 28, 2023 · 81ca8c2 · 81ca8c2
1 parent e5ed69a
commit 81ca8c2
Show file tree

Hide file tree

Showing 9 changed files with 67 additions and 34 deletions.
diff --git a/core/src/main/kotlin/org/vorpal/research/kex/state/transformer/BasicInvariantsTransformer.kt b/core/src/main/kotlin/org/vorpal/research/kex/state/transformer/BasicInvariantsTransformer.kt
@@ -0,0 +1,33 @@
+package org.vorpal.research.kex.state.transformer
+
+import org.vorpal.research.kex.ktype.KexRtManager.rtMapped
+import org.vorpal.research.kex.ktype.kexType
+import org.vorpal.research.kex.state.PredicateState
+import org.vorpal.research.kex.state.StateBuilder
+import org.vorpal.research.kex.state.predicate.assume
+import org.vorpal.research.kex.state.term.term
+import org.vorpal.research.kfg.ir.Method
+import org.vorpal.research.kthelper.collection.dequeOf
+
+class BasicInvariantsTransformer(
+    val method: Method
+) : RecollectingTransformer<BasicInvariantsTransformer> {
+    override val builders = dequeOf(StateBuilder())
+
+    override fun apply(ps: PredicateState): PredicateState {
+        val thisType = method.klass.kexType.rtMapped
+        val thisTerm = run {
+            val (thisTerm, _) = collectArguments(ps)
+            when {
+                thisTerm != null -> thisTerm
+                !method.isStatic -> term { `this`(thisType) }
+                else -> null
+            }
+        }
+        if (thisTerm != null) {
+            currentBuilder += assume { thisTerm inequality null }
+            currentBuilder += assume { (thisTerm `is` thisType) equality true }
+        }
+        return super.apply(ps)
+    }
+}
diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/defect/CallCiteChecker.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/defect/CallCiteChecker.kt
@@ -23,6 +23,7 @@ import org.vorpal.research.kex.state.term.FieldTerm
 import org.vorpal.research.kex.state.term.Term
 import org.vorpal.research.kex.state.term.term
 import org.vorpal.research.kex.state.transformer.AnnotationAdapter
+import org.vorpal.research.kex.state.transformer.BasicInvariantsTransformer
 import org.vorpal.research.kex.state.transformer.BoolTypeAdapter
 import org.vorpal.research.kex.state.transformer.ClassMethodAdapter
 import org.vorpal.research.kex.state.transformer.ConcreteImplInliner
@@ -212,7 +213,7 @@ class CallCiteChecker(
         id: String? = null
     ): Boolean {
         log.debug("Checking for assertion failure: ${inst.print()} at ${callCite.print()}")
-        log.debug("State: $state")
+        log.debug("State: {}", state)
         val assertionQuery = assertions.map {
             when (it.type) {
                 is KexBool -> require { it equality true }
@@ -250,6 +251,7 @@ class CallCiteChecker(
         +KexIntrinsicsAdapter()
         +EqualsTransformer()
         +DoubleTypeAdapter()
+        +BasicInvariantsTransformer(method)
         +ReflectionInfoAdapter(method, ctx.loader)
         +Optimizer()
         +ConstantPropagator
@@ -315,14 +317,14 @@ class CallCiteChecker(
         state = Optimizer().apply(state)
         query = Optimizer().apply(query)
         if (logQuery) {
-            log.debug("Simplified state: $state")
-            log.debug("Query: $query")
+            log.debug("Simplified state: {}", state)
+            log.debug("Query: {}", query)
         }
 
         val result = SMTProxySolver(ctx).use {
             it.isViolated(state, query)
         }
-        log.debug("Acquired $result")
+        log.debug("Acquired {}", result)
         return state to result
     }
 

diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/defect/DefectChecker.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/defect/DefectChecker.kt
@@ -20,6 +20,7 @@ import org.vorpal.research.kex.state.term.FieldTerm
 import org.vorpal.research.kex.state.term.Term
 import org.vorpal.research.kex.state.term.term
 import org.vorpal.research.kex.state.transformer.AnnotationAdapter
+import org.vorpal.research.kex.state.transformer.BasicInvariantsTransformer
 import org.vorpal.research.kex.state.transformer.BoolTypeAdapter
 import org.vorpal.research.kex.state.transformer.ClassMethodAdapter
 import org.vorpal.research.kex.state.transformer.ConcreteImplInliner
@@ -103,7 +104,7 @@ class DefectChecker
         this.method = method
         if (!method.hasBody) return
 
-        log.debug("Checking method $method")
+        log.debug("Checking method {}", method)
         log.debug(method.print())
 
         initializeGenerator()
@@ -187,7 +188,7 @@ class DefectChecker
     private fun checkNullity(inst: Instruction, state: PredicateState, `object`: Value): Boolean {
         if (`object` in nonNulls) return true
         log.debug("Checking for null pointer exception: ${inst.print()}")
-        log.debug("State: $state")
+        log.debug("State: {}", state)
         val objectTerm = term { value(`object`) }
         val refQuery = require { objectTerm inequality null }.wrap()
 
@@ -209,7 +210,7 @@ class DefectChecker
 
     private fun checkOutOfBounds(inst: Instruction, state: PredicateState, length: Term, index: Term): Boolean {
         log.debug("Checking for out of bounds exception: ${inst.print()}")
-        log.debug("State: $state")
+        log.debug("State: {}", state)
         var indexQuery = require { (index ge 0) equality true }.wrap()
         indexQuery += require { (index lt length) equality true }
 
@@ -231,8 +232,8 @@ class DefectChecker
         assertions: Set<Term>,
         id: String? = null
     ): Boolean {
-        log.debug("Checking for assertion failure: ${inst.print()}")
-        log.debug("State: $state")
+        log.debug("Checking for assertion failure: {}", inst.print())
+        log.debug("State: {}", state)
         val assertionQuery = assertions.map {
             when (it.type) {
                 is KexBool -> require { it equality true }
@@ -274,6 +275,7 @@ class DefectChecker
         +EqualsTransformer()
         +NullityAnnotator(nonNulls.mapTo(mutableSetOf()) { term { value(it) } })
         +DoubleTypeAdapter()
+        +BasicInvariantsTransformer(method)
         +ReflectionInfoAdapter(method, loader)
         +Optimizer()
         +ConstantPropagator
@@ -328,14 +330,14 @@ class DefectChecker
         state = Optimizer().apply(state)
         query = Optimizer().apply(query)
         if (logQuery) {
-            log.debug("Simplified state: $state")
-            log.debug("Query: $query")
+            log.debug("Simplified state: {}", state)
+            log.debug("Query: {}", query)
         }
 
         val result = SMTProxySolver(ctx).use {
             it.isViolated(state, query)
         }
-        log.debug("Acquired $result")
+        log.debug("Acquired {}", result)
         return state to result
     }
 }
diff --git a/...in/kotlin/org/vorpal/research/kex/reanimator/actionsequence/generator/GeneratorContext.kt b/...in/kotlin/org/vorpal/research/kex/reanimator/actionsequence/generator/GeneratorContext.kt
@@ -41,6 +41,7 @@ import org.vorpal.research.kex.state.term.Term
 import org.vorpal.research.kex.state.term.term
 import org.vorpal.research.kex.state.transformer.AnnotationAdapter
 import org.vorpal.research.kex.state.transformer.ArrayBoundsAdapter
+import org.vorpal.research.kex.state.transformer.BasicInvariantsTransformer
 import org.vorpal.research.kex.state.transformer.BoolTypeAdapter
 import org.vorpal.research.kex.state.transformer.CastTypeInfo
 import org.vorpal.research.kex.state.transformer.ClassAdapter
@@ -65,8 +66,8 @@ import org.vorpal.research.kex.state.transformer.TypeInfo
 import org.vorpal.research.kex.state.transformer.TypeInfoMap
 import org.vorpal.research.kex.state.transformer.TypeNameAdapter
 import org.vorpal.research.kex.state.transformer.collectArguments
-import org.vorpal.research.kex.state.transformer.collectFieldTerms
 import org.vorpal.research.kex.state.transformer.collectFieldAccesses
+import org.vorpal.research.kex.state.transformer.collectFieldTerms
 import org.vorpal.research.kex.state.transformer.collectPlainTypeInfos
 import org.vorpal.research.kex.state.transformer.collectStaticTypeInfo
 import org.vorpal.research.kex.state.transformer.generateInitialDescriptors
@@ -133,6 +134,7 @@ class GeneratorContext(
         +IntrinsicAdapter
         +KexIntrinsicsAdapter()
         +EqualsTransformer()
+        +BasicInvariantsTransformer(method)
         +ReflectionInfoAdapter(method, context.loader, ignores)
         +Optimizer()
         +ConstantPropagator

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
@@ -12,6 +12,7 @@ import org.vorpal.research.kex.state.term.FieldTerm
 import org.vorpal.research.kex.state.term.Term
 import org.vorpal.research.kex.state.term.ValueTerm
 import org.vorpal.research.kex.state.transformer.AnnotationAdapter
+import org.vorpal.research.kex.state.transformer.BasicInvariantsTransformer
 import org.vorpal.research.kex.state.transformer.BoolTypeAdapter
 import org.vorpal.research.kex.state.transformer.ClassAdapter
 import org.vorpal.research.kex.state.transformer.ClassMethodAdapter
@@ -91,6 +92,7 @@ class AsyncChecker(
         +IntrinsicAdapter
         +KexIntrinsicsAdapter()
         +EqualsTransformer()
+        +BasicInvariantsTransformer(method)
         +ReflectionInfoAdapter(method, ctx.loader)
         +Optimizer()
         +ConstantPropagator

diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/Checker.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/Checker.kt
@@ -12,6 +12,7 @@ import org.vorpal.research.kex.state.term.Term
 import org.vorpal.research.kex.state.term.ValueTerm
 import org.vorpal.research.kex.state.transformer.AnnotationAdapter
 import org.vorpal.research.kex.state.transformer.ArrayBoundsAdapter
+import org.vorpal.research.kex.state.transformer.BasicInvariantsTransformer
 import org.vorpal.research.kex.state.transformer.BoolTypeAdapter
 import org.vorpal.research.kex.state.transformer.ClassAdapter
 import org.vorpal.research.kex.state.transformer.ClassMethodAdapter
@@ -34,11 +35,11 @@ import org.vorpal.research.kex.state.transformer.StaticFieldInliner
 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.transform
 import org.vorpal.research.kfg.ir.Method
 import org.vorpal.research.kfg.ir.value.instruction.Instruction
 import org.vorpal.research.kthelper.logging.log
@@ -85,6 +86,7 @@ class Checker(
         +IntrinsicAdapter
         +KexIntrinsicsAdapter()
         +EqualsTransformer()
+        +BasicInvariantsTransformer(method)
         +ReflectionInfoAdapter(method, loader)
         +Optimizer()
         +ConstantPropagator
@@ -110,6 +112,7 @@ class Checker(
         +IntrinsicAdapter
         +KexIntrinsicsAdapter()
         +EqualsTransformer()
+        +BasicInvariantsTransformer(method)
         +ReflectionInfoAdapter(method, loader)
         +Optimizer()
         +ConstantPropagator
@@ -131,7 +134,7 @@ class Checker(
     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 (isMemspacingEnabled) {
             log.debug("Memspacing started...")
@@ -169,16 +172,16 @@ class Checker(
         state = Optimizer().apply(state)
         query = Optimizer().apply(query)
         if (logQuery) {
-            log.debug("Simplified state: $state")
+            log.debug("Simplified state: {}", state)
             log.debug("State size: ${state.size}")
-            log.debug("Query: $query")
+            log.debug("Query: {}", query)
             log.debug("Query size: ${query.size}")
         }
 
         val result = SMTProxySolver(ctx).use {
             it.isPathPossible(state, query)
         }
-        log.debug("Acquired $result")
+        log.debug("Acquired {}", result)
         return result
     }
 }
diff --git a/...runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/ReflectionInfoAdapter.kt b/...runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/ReflectionInfoAdapter.kt
@@ -5,7 +5,6 @@ import org.vorpal.research.kex.ktype.KexArray
 import org.vorpal.research.kex.ktype.KexClass
 import org.vorpal.research.kex.ktype.KexPointer
 import org.vorpal.research.kex.ktype.KexReference
-import org.vorpal.research.kex.ktype.KexRtManager.rtMapped
 import org.vorpal.research.kex.ktype.kexType
 import org.vorpal.research.kex.state.PredicateState
 import org.vorpal.research.kex.state.StateBuilder
@@ -20,7 +19,6 @@ import org.vorpal.research.kex.state.term.CallTerm
 import org.vorpal.research.kex.state.term.FieldLoadTerm
 import org.vorpal.research.kex.state.term.FieldTerm
 import org.vorpal.research.kex.state.term.Term
-import org.vorpal.research.kex.state.term.term
 import org.vorpal.research.kex.util.getKFunction
 import org.vorpal.research.kex.util.getKProperty
 import org.vorpal.research.kex.util.isElementNullable
@@ -50,21 +48,10 @@ class ReflectionInfoAdapter(
         val useReflectionInfo = kexConfig.getBooleanValue("kex", "useReflectionInfo", true)
         if (!useReflectionInfo) return ps
 
-        val (`this`, arguments) = collectArguments(ps)
-
-        if (`this` != null) {
-            currentBuilder += assume { `this` inequality null }
-        } else if (!method.isStatic) {
-            val nThis = term { `this`(method.klass.kexType.rtMapped) }
-            currentBuilder += assume { nThis inequality null }
-        }
-
+        val (_, arguments) = collectArguments(ps)
         val methodClassType = KexClass(method.klass.fullName).getKfgType(types)
         val klass = `try` { loader.loadKClass(methodClassType) }.getOrNull() ?: return super.apply(ps)
-        val kFunction = klass.getKFunction(method) ?: run {
-//            log.warn("Could not load kFunction for $method")
-            return super.apply(ps)
-        }
+        val kFunction = klass.getKFunction(method) ?: return super.apply(ps)
 
         val parameters = when {
             method.isAbstract -> kFunction.parameters.map { it.index to it }

diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/StaticFieldInliner.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/StaticFieldInliner.kt
@@ -65,6 +65,7 @@ class StaticFieldInliner(
             +IntrinsicAdapter
             +KexIntrinsicsAdapter()
             +EqualsTransformer()
+            +BasicInvariantsTransformer(method)
             +ReflectionInfoAdapter(method, ctx.loader, ignores)
             +Optimizer()
             +ConstantPropagator
@@ -112,7 +113,7 @@ class StaticFieldInliner(
             val checker = Checker(staticInit, ctx, psa)
             val params = when (val result = checker.check(state + query)) {
                 is Result.SatResult -> {
-                    log.debug("Model: ${result.model}")
+                    log.debug("Model: {}", result.model)
                     generateFinalDescriptors(staticInit, ctx, result.model, checker.state)
                 }
                 else -> return null

diff --git a/kex-test/src/main/kotlin/org/vorpal/research/kex/test/javadebug/Stack.java b/kex-test/src/main/kotlin/org/vorpal/research/kex/test/javadebug/Stack.java
@@ -1,5 +1,6 @@
 package org.vorpal.research.kex.test.javadebug;
 
+@SuppressWarnings("ALL")
 public class Stack {
 
     private Stack() {}