Log failed asserts and forks

UnitTestBot · Feb 14, 2024 · 644a9e5 · 644a9e5
1 parent 3b83106
commit 644a9e5
Show file tree

Hide file tree

Showing 7 changed files with 39 additions and 10 deletions.
diff --git a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt
@@ -104,7 +104,7 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, Type, Statement,
      *
      * NOTE: always sets the [stepScopeState] to the [CANNOT_BE_PROCESSED] value.
      */
-    fun forkMulti(conditionsWithBlockOnStates: List<Pair<UBoolExpr, T.() -> Unit>>) {
+    fun forkMulti(conditionsWithBlockOnStates: List<Pair<UBoolExpr, T.() -> Unit>>): Unit? {
         check(canProcessFurtherOnCurrentStep)
 
         val conditions = conditionsWithBlockOnStates.map { it.first }
@@ -120,7 +120,7 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, Type, Statement,
         stepScopeState = CANNOT_BE_PROCESSED
         if (forkedStates.isEmpty()) {
             stepScopeState = DEAD
-            return
+            return null
         }
 
         val firstForkedState = forkedStates.first()
@@ -130,6 +130,7 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, Type, Statement,
 
         // Interpret the first state as original and others as forked
         this.forkedStates += forkedStates.subList(1, forkedStates.size)
+        return Unit
     }
 
     fun assert(
@@ -190,7 +191,7 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, Type, Statement,
      * [forkMultiWithBlackList] version which doesn't fork to the branches with statements
      * banned by underlying [forkBlackList].
      */
-    fun forkMultiWithBlackList(forkCases: List<ForkCase<T, Statement>>) {
+    fun forkMultiWithBlackList(forkCases: List<ForkCase<T, Statement>>): Unit? {
         check(canProcessFurtherOnCurrentStep)
 
         val filteredConditionsWithBlockOnStates = forkCases
@@ -203,7 +204,7 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, Type, Statement,
 
         if (filteredConditionsWithBlockOnStates.isEmpty()) {
             stepScopeState = DEAD
-            return
+            return null
         }
 
         return forkMulti(filteredConditionsWithBlockOnStates)

diff --git a/usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt
@@ -7,6 +7,7 @@ import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.UState
 import org.usvm.uctx
+import org.usvm.utils.logAssertFailure
 
 // TODO: special mock api for variables
 
@@ -39,7 +40,7 @@ private inline fun <Type, Method, State> StepScope<State, Type, *, *>.mockSymbol
         mkTypeConstraint(ref)
     }
 
-    assert(typeConstraint) ?: return null
+    assert(typeConstraint).logAssertFailure { "Type constraint in mockSymbolicRef" } ?: return null
 
     return ref
 }

diff --git a/usvm-core/src/main/kotlin/org/usvm/api/collection/ListCollectionApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/collection/ListCollectionApi.kt
@@ -17,6 +17,7 @@ import org.usvm.mkSizeExpr
 import org.usvm.mkSizeGeExpr
 import org.usvm.mkSizeSubExpr
 import org.usvm.sizeSort
+import org.usvm.utils.logAssertFailure
 
 object ListCollectionApi {
     fun <ListType, USizeSort : USort, Ctx: UContext<USizeSort>> UState<ListType, *, *, Ctx, *, *>.mkSymbolicList(
@@ -51,7 +52,9 @@ object ListCollectionApi {
                 with(ctx) {
                     val boundConstraint = mkSizeGeExpr(length, mkSizeExpr(0))
                     // List size must be correct regardless of guard
-                    assert(boundConstraint) ?: return null
+                    assert(boundConstraint)
+                        .logAssertFailure { "SymbolicList size correctness constraint" }
+                        ?: return null
                 }
                 symbolicListRef
             }

diff --git a/usvm-core/src/main/kotlin/org/usvm/api/collection/ObjectMapCollectionApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/collection/ObjectMapCollectionApi.kt
@@ -25,6 +25,7 @@ import org.usvm.mkSizeGeExpr
 import org.usvm.mkSizeSubExpr
 import org.usvm.sizeSort
 import org.usvm.uctx
+import org.usvm.utils.logAssertFailure
 
 object ObjectMapCollectionApi {
     fun <MapType, USizeSort : USort, Ctx: UContext<USizeSort>> UState<MapType, *, *, Ctx, *, *>.mkSymbolicObjectMap(
@@ -61,7 +62,9 @@ object ObjectMapCollectionApi {
                 with(ctx) {
                     val boundConstraint = mkSizeGeExpr(length, mkSizeExpr(0))
                     // Map size must be correct regardless of guard
-                    assert(boundConstraint) ?: return null
+                    assert(boundConstraint)
+                        .logAssertFailure { "SymbolicMap size correctness constraint" }
+                        ?: return null
                 }
                 symbolicMapRef
             }

diff --git a/usvm-core/src/main/kotlin/org/usvm/utils/StateUtils.kt b/usvm-core/src/main/kotlin/org/usvm/utils/StateUtils.kt
@@ -3,6 +3,7 @@ package org.usvm.utils
 import org.usvm.UBoolExpr
 import org.usvm.UState
 import org.usvm.isTrue
+import org.usvm.logger
 import org.usvm.model.UModelBase
 import org.usvm.solver.USatResult
 import org.usvm.solver.USolverResult
@@ -97,3 +98,11 @@ fun <T : UState<Type, *, *, *, *, T>, Type> T.applySoftConstraints() {
         }
     }
 }
+
+inline fun Unit?.onStateDeath(crossinline body: () -> Unit) = apply {
+    if (this == null) body()
+}
+
+inline fun Unit?.logAssertFailure(crossinline message: () -> String) = onStateDeath {
+    logger.info { "Assert failed: ${message()}" }
+}
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
@@ -119,6 +119,7 @@ import org.usvm.sizeSort
 import org.usvm.util.allocHeapRef
 import org.usvm.util.enumValuesField
 import org.usvm.util.write
+import org.usvm.utils.logAssertFailure
 
 /**
  * An expression resolver based on JacoDb 3-address code. A result of resolving is `null`, iff
@@ -333,7 +334,11 @@ class JcExprResolver(
         val lengthRef = UArrayLengthLValue(ref, arrayDescriptor, sizeSort)
         val length = scope.calcOnState { memory.read(lengthRef).asExpr(sizeSort) }
         assertHardMaxArrayLength(length) ?: return null
-        scope.assert(mkBvSignedLessOrEqualExpr(mkBv(0), length)) ?: return null
+
+        scope.assert(mkBvSignedLessOrEqualExpr(mkBv(0), length))
+            .logAssertFailure { "JcExprResolver: array length >= 0" }
+            ?: return null
+
         length
     }
 
@@ -505,7 +510,9 @@ class JcExprResolver(
         if (type is JcRefType) {
             val heapRef = expr.asExpr(ctx.addressSort)
             val isExpr = scope.calcOnState { memory.types.evalIsSubtype(heapRef, type) }
-            scope.assert(isExpr) ?: return false
+            scope.assert(isExpr)
+                .logAssertFailure { "JcExprResolver: subtype constraint ${type.typeName}" }
+                ?: return false
         }
 
         return true
@@ -604,6 +611,7 @@ class JcExprResolver(
 
 
         scope.assert(invariantsConstraint)
+            .logAssertFailure { "JcExprResolver: enum correctness constraint" }
     }
 
     /**
@@ -804,6 +812,7 @@ class JcExprResolver(
     private fun assertHardMaxArrayLength(length: UExpr<USizeSort>): Unit? = with(ctx) {
         val lengthLeThanMaxLength = mkBvSignedLessOrEqualExpr(length, mkBv(hardMaxArrayLength))
         scope.assert(lengthLeThanMaxLength)
+            .logAssertFailure { "JcExprResolver: array length max" }
     }
 
     // endregion

diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt
@@ -78,6 +78,8 @@ import org.usvm.types.singleOrNull
 import org.usvm.util.name
 import org.usvm.util.outerClassInstanceField
 import org.usvm.util.write
+import org.usvm.utils.logAssertFailure
+import org.usvm.utils.onStateDeath
 
 typealias JcStepScope = StepScope<JcState, JcType, JcInst, JcContext>
 
@@ -483,7 +485,7 @@ class JcInterpreter(
             negStmt,
             blockOnTrueState = { newStmt(posStmt) },
             blockOnFalseState = { newStmt(negStmt) }
-        )
+        ).onStateDeath { logger.info { "State death on fork with blacklist" } }
     }
 
     private fun visitReturnStmt(scope: JcStepScope, stmt: JcReturnInst) {
@@ -549,6 +551,7 @@ class JcInterpreter(
                 )
 
             scope.forkMultiWithBlackList(cases + defaultCase)
+                .onStateDeath { logger.info { "State death on fork with blacklist" } }
         }
     }