Fix tests

UnitTestBot · Feb 20, 2024 · 6d1ab8c · 6d1ab8c
1 parent 0ee649d
commit 6d1ab8c
Show file tree

Hide file tree

Showing 2 changed files with 35 additions and 11 deletions.
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTransformer.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTransformer.kt
@@ -1,24 +1,21 @@
 package org.usvm.machine
 
 import io.ksmt.expr.KExpr
-import io.ksmt.solver.KModel
 import io.ksmt.sort.KBoolSort
 import io.ksmt.utils.mkConst
 import org.jacodb.api.JcField
 import org.jacodb.api.JcType
 import org.usvm.UComposer
-import org.usvm.UConcreteHeapRef
 import org.usvm.UContext
 import org.usvm.UExpr
-import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.UTransformer
 import org.usvm.machine.interpreter.statics.JcStaticFieldLValue
 import org.usvm.machine.interpreter.statics.JcStaticFieldReading
 import org.usvm.machine.interpreter.statics.JcStaticFieldRegionId
 import org.usvm.memory.UReadOnlyMemory
 import org.usvm.memory.UReadOnlyMemoryRegion
-import org.usvm.model.mapAddress
+import org.usvm.model.UModelEvaluator
 import org.usvm.solver.UExprTranslator
 import org.usvm.solver.URegionDecoder
 import org.usvm.solver.USoftConstraintsProvider
@@ -54,16 +51,14 @@ class JcStaticFieldDecoder<Sort : USort>(
         }
 
     override fun decodeLazyRegion(
-        model: KModel,
-        mapping: Map<UHeapRef, UConcreteHeapRef>,
+        model: UModelEvaluator<*>,
         assertions: List<KExpr<KBoolSort>>,
     ): UReadOnlyMemoryRegion<JcStaticFieldLValue<Sort>, Sort> =
-        JcStaticFieldModel(model, mapping, translated, translator)
+        JcStaticFieldModel(model, translated, translator)
 }
 
 class JcStaticFieldModel<Sort : USort>(
-    private val model: KModel,
-    private val mapping: Map<UHeapRef, UConcreteHeapRef>,
+    private val model: UModelEvaluator<*>,
     private val translatedFields: Map<JcField, UExpr<Sort>>,
     private val translator: UExprTranslator<*, *>
 ) : UReadOnlyMemoryRegion<JcStaticFieldLValue<Sort>, Sort> {
@@ -72,7 +67,7 @@ class JcStaticFieldModel<Sort : USort>(
             ?: translator.translate(
                 key.sort.jctx.mkStaticFieldReading(key.memoryRegionId as JcStaticFieldRegionId, key.field, key.sort)
             )
-        return model.eval(translated, isComplete = true).mapAddress(mapping)
+        return model.evalAndComplete(translated)
     }
 }
 

diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/casts/ArrayCastExample.java b/usvm-jvm/src/samples/java/org/usvm/samples/casts/ArrayCastExample.java
@@ -1,9 +1,16 @@
 package org.usvm.samples.casts;
 
-import static org.usvm.api.mock.UMockKt.assume;
+import org.jetbrains.annotations.NotNull;
+import org.usvm.api.Engine;
 
+import java.util.ArrayList;
 import java.util.Collection;
+import java.util.Iterator;
 import java.util.List;
+import java.util.Spliterator;
+import java.util.function.Consumer;
+
+import static org.usvm.api.mock.UMockKt.assume;
 
 public class ArrayCastExample {
     @SuppressWarnings("RedundantCast")
@@ -101,11 +108,33 @@ public List<ColoredPoint> castFromIterable(Iterable<ColoredPoint> iterable) {
         return (List<ColoredPoint>) iterable;
     }
 
+    private static class NonCollectionIterable<T> implements Iterable<T> {
+        private final List<T> collection = new ArrayList<>();
+
+        @NotNull
+        @Override
+        public Iterator<T> iterator() {
+            return collection.iterator();
+        }
+
+        @Override
+        public void forEach(Consumer<? super T> action) {
+            collection.forEach(action);
+        }
+
+        @Override
+        public Spliterator<T> spliterator() {
+            return collection.spliterator();
+        }
+    }
+
     public Collection<ColoredPoint> castFromIterableToCollection(Iterable<ColoredPoint> iterable) {
         if (iterable == null) {
             return null;
         }
 
+        Engine.assume(iterable instanceof Collection<?> | iterable instanceof NonCollectionIterable<?>);
+
         return (Collection<ColoredPoint>) iterable;
     }
 }