Rebase fixes

UnitTestBot · Sep 27, 2023 · f257d7d · f257d7d
1 parent 03b4d9c
commit f257d7d
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 27 deletions.
diff --git a/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt b/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt
@@ -226,13 +226,14 @@ internal fun <Method, Statement, Target, State> createTargetedPathSelector(
 
     fun calculateDistanceToTargets(state: State) =
         state.targets.minOfOrNull { target ->
-            if (target.location == null) {
+            val location = target.location
+            if (location == null) {
                 0u
             } else {
                 distanceCalculator.calculateDistance(
                     state.currentStatement,
                     state.callStack,
-                    target.location
+                    location
                 )
             }
         } ?: UInt.MAX_VALUE
@@ -289,13 +290,14 @@ internal fun <Method, Statement, Target, State> createTargetedPathSelector(
 
     fun calculateWeight(state: State) =
         state.targets.minOfOrNull { target ->
-            if (target.location == null) {
+            val location = target.location
+            if (location == null) {
                 0u
             } else {
                 distanceCalculator.calculateDistance(
                     state.currentStatement,
                     state.callStack,
-                    target.location
+                    location
                 ).logWeight()
             }
         } ?: UInt.MAX_VALUE

diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt
@@ -197,9 +197,7 @@ class JcMethodApproximationResolver(
 
             val primitive = predefinedTypeNames[classNameRef] ?: return false
 
-            val classRef = with(exprResolver.simpleValueResolver) {
-                resolveClassRef(primitive)
-            }
+            val classRef = exprResolver.simpleValueResolver.resolveClassRef(primitive)
 
             scope.doWithState {
                 skipMethodInvocationWithValue(methodCall, classRef)
@@ -232,12 +230,8 @@ class JcMethodApproximationResolver(
             val result = scope.calcOnState {
                 mapTypeStream(instance) { _, types ->
                     val type = types.singleOrNull()
-                    type?.let {
-                        with(exprResolver.simpleValueResolver) {
-                            resolveClassRef(it)
-                        }
-                    }
-                } // TODO fix here
+                    type?.let { exprResolver.simpleValueResolver.resolveClassRef(it) }
+                }
             } ?: return false
 
             scope.doWithState {
@@ -271,9 +265,7 @@ class JcMethodApproximationResolver(
             )
 
             val primitiveArrayRefScale = primitiveArrayScale.mapKeys { (type, _) ->
-                with(exprResolver.simpleValueResolver) {
-                    resolveClassRef(ctx.cp.arrayTypeOf(type))
-                }
+                exprResolver.simpleValueResolver.resolveClassRef(ctx.cp.arrayTypeOf(type))
             }
 
             val arrayTypeRef = arguments.last().asExpr(ctx.addressSort)
@@ -320,7 +312,7 @@ class JcMethodApproximationResolver(
         srcPos: USizeExpr,
         dstRef: UHeapRef,
         dstPos: USizeExpr,
-        length: USizeExpr
+        length: USizeExpr,
     ) {
         checkNullPointer(srcRef) ?: return
         checkNullPointer(dstRef) ?: return
@@ -372,7 +364,7 @@ class JcMethodApproximationResolver(
     private fun JcExprResolver.resolveArrayClone(
         methodCall: JcMethodCall,
         instance: UConcreteHeapRef,
-        arrayType: JcArrayType
+        arrayType: JcArrayType,
     ) = with(ctx) {
         scope.doWithState {
             checkNullPointer(instance) ?: return@doWithState
@@ -410,7 +402,7 @@ class JcMethodApproximationResolver(
         srcPos: USizeExpr,
         dstRef: UHeapRef,
         dstPos: USizeExpr,
-        length: USizeExpr
+        length: USizeExpr,
     ) = with(ctx) {
         val arrayDescriptor = arrayDescriptorOf(type)
         val elementType = requireNotNull(type.ifArrayGetElementType)
@@ -796,7 +788,7 @@ class JcMethodApproximationResolver(
 
     private fun MutableMap<String, (JcMethodCall) -> UExpr<*>?>.dispatchUsvmApiMethod(
         apiMethod: KFunction<*>,
-        body: (JcMethodCall) -> UExpr<*>?
+        body: (JcMethodCall) -> UExpr<*>?,
     ) {
         val methodName = apiMethod.javaMethod?.name
             ?: error("No name for $apiMethod")
@@ -805,22 +797,22 @@ class JcMethodApproximationResolver(
 
     private fun MutableMap<String, (JcMethodCall) -> UExpr<*>?>.dispatchMkRef(
         apiMethod: KFunction1<Nothing, Any>,
-        body: (JcMethodCall) -> UExpr<*>?
+        body: (JcMethodCall) -> UExpr<*>?,
     ) = dispatchUsvmApiMethod(apiMethod, body)
 
     private fun MutableMap<String, (JcMethodCall) -> UExpr<*>?>.dispatchMkRef2(
         apiMethod: KFunction2<Nothing, Nothing, Array<Any>>,
-        body: (JcMethodCall) -> UExpr<*>?
+        body: (JcMethodCall) -> UExpr<*>?,
     ) = dispatchUsvmApiMethod(apiMethod, body)
 
     private fun MutableMap<String, (JcMethodCall) -> UExpr<*>?>.dispatchMkList(
         apiMethod: KFunction0<SymbolicList<Any>>,
-        body: (JcMethodCall) -> UExpr<*>?
+        body: (JcMethodCall) -> UExpr<*>?,
     ) = dispatchUsvmApiMethod(apiMethod, body)
 
     private fun MutableMap<String, (JcMethodCall) -> UExpr<*>?>.dispatchMkMap(
         apiMethod: KFunction0<SymbolicMap<Any, Any>>,
-        body: (JcMethodCall) -> UExpr<*>?
+        body: (JcMethodCall) -> UExpr<*>?,
     ) = dispatchUsvmApiMethod(apiMethod, body)
 
     private fun makeSymbolicArray(elementType: JcType, size: UExpr<*>): UHeapRef? {

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
@@ -666,9 +666,7 @@ class JcExprResolver(
             return body()
         }
 
-        val classRef = with(simpleValueResolver) {
-            resolveClassRef(type)
-        }
+        val classRef = simpleValueResolver.resolveClassRef(type)
 
         val initializedFlag = staticFieldsInitializedFlag(type, classRef)