From 7c51e306239ec77379134380df03bd1460680de2 Mon Sep 17 00:00:00 2001 From: Yury Kamenev Date: Mon, 16 Jan 2023 12:11:03 +0300 Subject: [PATCH]  This is a combination of 2 commits.  This is the 1st commit message: Fixed copyOf, copyOfRange and asList failures  The commit message #2 will be skipped:  Added symbolic implementation for Arrays.copyOf and Arrays.copyOfRange --- .../org/utbot/engine/overrides/System.java | 5 +- .../utbot/engine/overrides/stream/Arrays.java | 9 +- .../kotlin/org/utbot/engine/ObjectWrappers.kt | 162 +++++++++++------- .../main/kotlin/org/utbot/engine/Traverser.kt | 72 ++++++++ .../org/utbot/engine/types/TypeResolver.kt | 2 + 5 files changed, 181 insertions(+), 69 deletions(-) diff --git a/utbot-framework/src/main/java/org/utbot/engine/overrides/System.java b/utbot-framework/src/main/java/org/utbot/engine/overrides/System.java index fb37ceed9e..f34ddd851b 100644 --- a/utbot-framework/src/main/java/org/utbot/engine/overrides/System.java +++ b/utbot-framework/src/main/java/org/utbot/engine/overrides/System.java @@ -210,7 +210,7 @@ public static void arraycopy(Object src, int srcPos, Object dest, int destPos, i } UtArrayMock.arraycopy(srcArray, srcPos, destArray, destPos, length); - } else { + } else if (src instanceof Object[]) { if (!(dest instanceof Object[])) { throw new ArrayStoreException(); } @@ -223,6 +223,9 @@ public static void arraycopy(Object src, int srcPos, Object dest, int destPos, i } UtArrayMock.arraycopy(srcArray, srcPos, destArray, destPos, length); + } else { + // From docs: if the src argument refers to an object that is not an array, an ArrayStoreException will be thrown + throw new ArrayStoreException(); } } } diff --git a/utbot-framework/src/main/java/org/utbot/engine/overrides/stream/Arrays.java b/utbot-framework/src/main/java/org/utbot/engine/overrides/stream/Arrays.java index 0935ad1925..10f337944e 100644 --- a/utbot-framework/src/main/java/org/utbot/engine/overrides/stream/Arrays.java +++ b/utbot-framework/src/main/java/org/utbot/engine/overrides/stream/Arrays.java @@ -1,6 +1,7 @@ package org.utbot.engine.overrides.stream; import org.utbot.api.annotation.UtClassMock; +import org.utbot.api.mock.UtMock; import org.utbot.engine.overrides.collections.UtArrayList; import java.util.List; @@ -21,7 +22,7 @@ public static Stream stream(T[] array, int startInclusive, int endExclusi return new UtStream<>(array, startInclusive, endExclusive); } - // from docs - array is assumed to be umnodified during use + // from docs - array is assumed to be unmodified during use public static IntStream stream(int[] array, int startInclusive, int endExclusive) { int size = array.length; @@ -37,7 +38,7 @@ public static IntStream stream(int[] array, int startInclusive, int endExclusive return new UtIntStream(data, startInclusive, endExclusive); } - // from docs - array is assumed to be umnodified during use + // from docs - array is assumed to be unmodified during use public static LongStream stream(long[] array, int startInclusive, int endExclusive) { int size = array.length; @@ -53,7 +54,7 @@ public static LongStream stream(long[] array, int startInclusive, int endExclusi return new UtLongStream(data, startInclusive, endExclusive); } - // from docs - array is assumed to be umnodified during use + // from docs - array is assumed to be unmodified during use public static DoubleStream stream(double[] array, int startInclusive, int endExclusive) { int size = array.length; @@ -75,6 +76,4 @@ public static List asList(T... a) { // TODO immutable collection https://github.com/UnitTestBot/UTBotJava/issues/398 return new UtArrayList<>(a); } - - // TODO primitive arrays https://github.com/UnitTestBot/UTBotJava/issues/146 } diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/ObjectWrappers.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/ObjectWrappers.kt index 5b3d47a613..bdb4632643 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/ObjectWrappers.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/ObjectWrappers.kt @@ -15,19 +15,36 @@ import org.utbot.engine.UtStreamClass.UT_LONG_STREAM import org.utbot.engine.UtStreamClass.UT_STREAM import org.utbot.engine.overrides.collections.AssociativeArray import org.utbot.engine.overrides.collections.RangeModifiableUnlimitedArray +import org.utbot.engine.overrides.collections.UtArrayList import org.utbot.engine.overrides.collections.UtHashMap import org.utbot.engine.overrides.collections.UtHashSet +import org.utbot.engine.overrides.collections.UtLinkedList +import org.utbot.engine.overrides.collections.UtLinkedListWithNullableCheck +import org.utbot.engine.overrides.collections.UtOptional +import org.utbot.engine.overrides.collections.UtOptionalDouble +import org.utbot.engine.overrides.collections.UtOptionalInt +import org.utbot.engine.overrides.collections.UtOptionalLong import org.utbot.engine.overrides.security.UtSecurityManager +import org.utbot.engine.overrides.stream.UtDoubleStream +import org.utbot.engine.overrides.stream.UtIntStream +import org.utbot.engine.overrides.stream.UtLongStream +import org.utbot.engine.overrides.stream.UtStream import org.utbot.engine.overrides.strings.UtString import org.utbot.engine.overrides.strings.UtStringBuffer import org.utbot.engine.overrides.strings.UtStringBuilder import org.utbot.engine.overrides.threads.UtCompletableFuture +import org.utbot.engine.overrides.threads.UtCountDownLatch +import org.utbot.engine.overrides.threads.UtExecutorService +import org.utbot.engine.overrides.threads.UtThread +import org.utbot.engine.overrides.threads.UtThreadGroup import org.utbot.engine.pc.UtAddrExpression +import org.utbot.framework.plugin.api.ClassId import org.utbot.framework.plugin.api.UtAssembleModel import org.utbot.framework.plugin.api.UtExecutableCallModel import org.utbot.framework.plugin.api.UtModel import org.utbot.framework.plugin.api.UtPrimitiveModel import org.utbot.framework.plugin.api.id +import org.utbot.framework.plugin.api.util.UtContext import org.utbot.framework.plugin.api.util.constructorId import org.utbot.framework.plugin.api.util.id import org.utbot.framework.plugin.api.util.stringClassId @@ -36,18 +53,6 @@ import soot.RefType import soot.Scene import soot.SootClass import soot.SootMethod -import java.util.Optional -import java.util.OptionalDouble -import java.util.OptionalInt -import java.util.OptionalLong -import java.util.concurrent.CompletableFuture -import java.util.concurrent.CompletionStage -import java.util.concurrent.CopyOnWriteArrayList -import java.util.concurrent.CountDownLatch -import java.util.concurrent.ExecutorService -import java.util.concurrent.ForkJoinPool -import java.util.concurrent.ScheduledThreadPoolExecutor -import java.util.concurrent.ThreadPoolExecutor import kotlin.reflect.KClass typealias TypeToBeWrapped = RefType @@ -60,39 +65,31 @@ typealias WrapperType = RefType val classToWrapper: MutableMap = mutableMapOf().apply { putSootClass(java.lang.StringBuilder::class, utStringBuilderClass) - putSootClass(UtStringBuilder::class, utStringBuilderClass) putSootClass(java.lang.StringBuffer::class, utStringBufferClass) - putSootClass(UtStringBuffer::class, utStringBufferClass) putSootClass(java.lang.CharSequence::class, utStringClass) putSootClass(java.lang.String::class, utStringClass) - putSootClass(UtString::class, utStringClass) - putSootClass(Optional::class, UT_OPTIONAL.className) - putSootClass(OptionalInt::class, UT_OPTIONAL_INT.className) - putSootClass(OptionalLong::class, UT_OPTIONAL_LONG.className) - putSootClass(OptionalDouble::class, UT_OPTIONAL_DOUBLE.className) + putSootClass(java.util.Optional::class, UT_OPTIONAL.className) + putSootClass(java.util.OptionalInt::class, UT_OPTIONAL_INT.className) + putSootClass(java.util.OptionalLong::class, UT_OPTIONAL_LONG.className) + putSootClass(java.util.OptionalDouble::class, UT_OPTIONAL_DOUBLE.className) // threads putSootClass(java.lang.Thread::class, utThreadClass) putSootClass(java.lang.ThreadGroup::class, utThreadGroupClass) // executors, futures and latches - putSootClass(ExecutorService::class, utExecutorServiceClass) - putSootClass(ThreadPoolExecutor::class, utExecutorServiceClass) - putSootClass(ForkJoinPool::class, utExecutorServiceClass) - putSootClass(ScheduledThreadPoolExecutor::class, utExecutorServiceClass) - putSootClass(CountDownLatch::class, utCountDownLatchClass) - putSootClass(CompletableFuture::class, utCompletableFutureClass) - putSootClass(CompletionStage::class, utCompletableFutureClass) - // A hack to be able to create UtCompletableFuture in its methods as a wrapper - putSootClass(UtCompletableFuture::class, utCompletableFutureClass) - - putSootClass(RangeModifiableUnlimitedArray::class, RangeModifiableUnlimitedArrayWrapper::class) - putSootClass(AssociativeArray::class, AssociativeArrayWrapper::class) + putSootClass(java.util.concurrent.ExecutorService::class, utExecutorServiceClass) + putSootClass(java.util.concurrent.ThreadPoolExecutor::class, utExecutorServiceClass) + putSootClass(java.util.concurrent.ForkJoinPool::class, utExecutorServiceClass) + putSootClass(java.util.concurrent.ScheduledThreadPoolExecutor::class, utExecutorServiceClass) + putSootClass(java.util.concurrent.CountDownLatch::class, utCountDownLatchClass) + putSootClass(java.util.concurrent.CompletableFuture::class, utCompletableFutureClass) + putSootClass(java.util.concurrent.CompletionStage::class, utCompletableFutureClass) putSootClass(java.util.List::class, UT_ARRAY_LIST.className) putSootClass(java.util.AbstractList::class, UT_ARRAY_LIST.className) putSootClass(java.util.ArrayList::class, UT_ARRAY_LIST.className) - putSootClass(CopyOnWriteArrayList::class, UT_ARRAY_LIST.className) + putSootClass(java.util.concurrent.CopyOnWriteArrayList::class, UT_ARRAY_LIST.className) putSootClass(java.util.LinkedList::class, UT_LINKED_LIST.className) putSootClass(java.util.AbstractSequentialList::class, UT_LINKED_LIST.className) @@ -120,6 +117,17 @@ val classToWrapper: MutableMap = putSootClass(java.util.stream.DoubleStream::class, UT_DOUBLE_STREAM.className) putSootClass(java.lang.SecurityManager::class, UtSecurityManager::class) + + putSootClass(RangeModifiableUnlimitedArray::class, RangeModifiableUnlimitedArrayWrapper::class) + putSootClass(AssociativeArray::class, AssociativeArray::class) + }.apply { + // Each wrapper has to wrap itself to make possible to create it (not an underlying class!) in UtMocks or in wrappers. + // We take this particular classloader because current classloader cannot load our classes + val applicationClassLoader = UtContext::class.java.classLoader + values.distinct().forEach { + val kClass = applicationClassLoader.loadClass(it.className).kotlin + putSootClass(kClass, it) + } } /** @@ -154,46 +162,32 @@ private fun MutableMap.putSootClass( value: RefType ) = put(Scene.v().getSootClass(key.java.canonicalName).type, value) -private val wrappers = mapOf( +private val wrappers: Map ObjectValue> = mutableMapOf( wrap(java.lang.StringBuilder::class) { type, addr -> objectValue(type, addr, UtStringBuilderWrapper()) }, - wrap(UtStringBuilder::class) { type, addr -> objectValue(type, addr, UtStringBuilderWrapper()) }, wrap(java.lang.StringBuffer::class) { type, addr -> objectValue(type, addr, UtStringBufferWrapper()) }, - wrap(UtStringBuffer::class) { type, addr -> objectValue(type, addr, UtStringBufferWrapper()) }, wrap(java.lang.CharSequence::class) { type, addr -> objectValue(type, addr, StringWrapper()) }, wrap(java.lang.String::class) { type, addr -> objectValue(type, addr, StringWrapper()) }, - wrap(UtString::class) { type, addr -> objectValue(type, addr, StringWrapper()) }, - wrap(Optional::class) { type, addr -> objectValue(type, addr, OptionalWrapper(UT_OPTIONAL)) }, - wrap(OptionalInt::class) { type, addr -> objectValue(type, addr, OptionalWrapper(UT_OPTIONAL_INT)) }, - wrap(OptionalLong::class) { type, addr -> objectValue(type, addr, OptionalWrapper(UT_OPTIONAL_LONG)) }, - wrap(OptionalDouble::class) { type, addr -> objectValue(type, addr, OptionalWrapper(UT_OPTIONAL_DOUBLE)) }, + wrap(java.util.Optional::class) { type, addr -> objectValue(type, addr, OptionalWrapper(UT_OPTIONAL)) }, + wrap(java.util.OptionalInt::class) { type, addr -> objectValue(type, addr, OptionalWrapper(UT_OPTIONAL_INT)) }, + wrap(java.util.OptionalLong::class) { type, addr -> objectValue(type, addr, OptionalWrapper(UT_OPTIONAL_LONG)) }, + wrap(java.util.OptionalDouble::class) { type, addr -> objectValue(type, addr, OptionalWrapper(UT_OPTIONAL_DOUBLE)) }, // threads - wrap(Thread::class) { type, addr -> objectValue(type, addr, ThreadWrapper()) }, - wrap(ThreadGroup::class) { type, addr -> objectValue(type, addr, ThreadGroupWrapper()) }, - wrap(ExecutorService::class) { type, addr -> objectValue(type, addr, ExecutorServiceWrapper()) }, - wrap(ThreadPoolExecutor::class) { type, addr -> objectValue(type, addr, ExecutorServiceWrapper()) }, - wrap(ForkJoinPool::class) { type, addr -> objectValue(type, addr, ExecutorServiceWrapper()) }, - wrap(ScheduledThreadPoolExecutor::class) { type, addr -> objectValue(type, addr, ExecutorServiceWrapper()) }, - wrap(CountDownLatch::class) { type, addr -> objectValue(type, addr, CountDownLatchWrapper()) }, - wrap(CompletableFuture::class) { type, addr -> objectValue(type, addr, CompletableFutureWrapper()) }, - wrap(CompletionStage::class) { type, addr -> objectValue(type, addr, CompletableFutureWrapper()) }, - // A hack to be able to create UtCompletableFuture in its methods as a wrapper - wrap(UtCompletableFuture::class) { type, addr -> objectValue(type, addr, CompletableFutureWrapper()) }, - - wrap(RangeModifiableUnlimitedArray::class) { type, addr -> - objectValue(type, addr, RangeModifiableUnlimitedArrayWrapper()) - }, - wrap(AssociativeArray::class) { type, addr -> - objectValue(type, addr, AssociativeArrayWrapper()) - }, + wrap(java.lang.Thread::class) { type, addr -> objectValue(type, addr, ThreadWrapper()) }, + wrap(java.lang.ThreadGroup::class) { type, addr -> objectValue(type, addr, ThreadGroupWrapper()) }, + wrap(java.util.concurrent.ExecutorService::class) { type, addr -> objectValue(type, addr, ExecutorServiceWrapper()) }, + wrap(java.util.concurrent.ThreadPoolExecutor::class) { type, addr -> objectValue(type, addr, ExecutorServiceWrapper()) }, + wrap(java.util.concurrent.ForkJoinPool::class) { type, addr -> objectValue(type, addr, ExecutorServiceWrapper()) }, + wrap(java.util.concurrent.ScheduledThreadPoolExecutor::class) { type, addr -> objectValue(type, addr, ExecutorServiceWrapper()) }, + wrap(java.util.concurrent.CountDownLatch::class) { type, addr -> objectValue(type, addr, CountDownLatchWrapper()) }, + wrap(java.util.concurrent.CompletableFuture::class) { type, addr -> objectValue(type, addr, CompletableFutureWrapper()) }, + wrap(java.util.concurrent.CompletionStage::class) { type, addr -> objectValue(type, addr, CompletableFutureWrapper()) }, // list wrappers wrap(java.util.List::class) { _, addr -> objectValue(ARRAY_LIST_TYPE, addr, ListWrapper(UT_ARRAY_LIST)) }, wrap(java.util.AbstractList::class) { _, addr -> objectValue(ARRAY_LIST_TYPE, addr, ListWrapper(UT_ARRAY_LIST)) }, wrap(java.util.ArrayList::class) { _, addr -> objectValue(ARRAY_LIST_TYPE, addr, ListWrapper(UT_ARRAY_LIST)) }, - - - wrap(CopyOnWriteArrayList::class) { type, addr -> objectValue(type, addr, ListWrapper(UT_ARRAY_LIST)) }, + wrap(java.util.concurrent.CopyOnWriteArrayList::class) { type, addr -> objectValue(type, addr, ListWrapper(UT_ARRAY_LIST)) }, wrap(java.util.LinkedList::class) { _, addr -> objectValue(LINKED_LIST_TYPE, addr, ListWrapper(UT_LINKED_LIST)) }, wrap(java.util.AbstractSequentialList::class) { _, addr -> objectValue(LINKED_LIST_TYPE, addr, ListWrapper(UT_LINKED_LIST)) }, @@ -236,8 +230,50 @@ private val wrappers = mapOf( wrap(java.util.stream.DoubleStream::class) { _, addr -> objectValue(DOUBLE_STREAM_TYPE, addr, DoubleStreamWrapper()) }, // Security-related wrappers - wrap(SecurityManager::class) { type, addr -> objectValue(type, addr, SecurityManagerWrapper()) }, -).also { + wrap(java.lang.SecurityManager::class) { type, addr -> objectValue(type, addr, SecurityManagerWrapper()) }, +).apply { + // Each wrapper has to wrap itself to make possible to create it (not an underlying class!) in UtMocks or in wrappers + arrayOf( + wrap(UtStringBuilder::class) { type, addr -> objectValue(type, addr, UtStringBuilderWrapper()) }, + wrap(UtStringBuffer::class) { type, addr -> objectValue(type, addr, UtStringBufferWrapper()) }, + wrap(UtString::class) { type, addr -> objectValue(type, addr, StringWrapper()) }, + + wrap(UtOptional::class) { type, addr -> objectValue(type, addr, OptionalWrapper(UT_OPTIONAL)) }, + wrap(UtOptionalInt::class) { type, addr -> objectValue(type, addr, OptionalWrapper(UT_OPTIONAL_INT)) }, + wrap(UtOptionalLong::class) { type, addr -> objectValue(type, addr, OptionalWrapper(UT_OPTIONAL_LONG)) }, + wrap(UtOptionalDouble::class) { type, addr -> objectValue(type, addr, OptionalWrapper(UT_OPTIONAL_DOUBLE)) }, + + wrap(UtThread::class) { type, addr -> objectValue(type, addr, ThreadWrapper()) }, + wrap(UtThreadGroup::class) { type, addr -> objectValue(type, addr, ThreadGroupWrapper()) }, + wrap(UtExecutorService::class) { type, addr -> objectValue(type, addr, ExecutorServiceWrapper()) }, + wrap(UtCountDownLatch::class) { type, addr -> objectValue(type, addr, CountDownLatchWrapper()) }, + wrap(UtCompletableFuture::class) { type, addr -> objectValue(type, addr, CompletableFutureWrapper()) }, + + wrap(UtArrayList::class) { type, addr -> objectValue(type, addr, ListWrapper(UT_ARRAY_LIST)) }, + wrap(UtLinkedList::class) { _, addr -> objectValue(LINKED_LIST_TYPE, addr, ListWrapper(UT_LINKED_LIST)) }, + wrap(UtLinkedListWithNullableCheck::class) { type, addr -> + objectValue(type, addr, ListWrapper(UT_LINKED_LIST_WITH_NULLABLE_CHECK)) + }, + + wrap(UtHashSet::class) { _, addr -> objectValue(LINKED_HASH_SET_TYPE, addr, SetWrapper()) }, + + wrap(UtHashMap::class) { _, addr -> objectValue(LINKED_HASH_MAP_TYPE, addr, MapWrapper()) }, + + wrap(UtStream::class) { _, addr -> objectValue(STREAM_TYPE, addr, CommonStreamWrapper()) }, + wrap(UtIntStream::class) { _, addr -> objectValue(INT_STREAM_TYPE, addr, IntStreamWrapper()) }, + wrap(UtLongStream::class) { _, addr -> objectValue(LONG_STREAM_TYPE, addr, LongStreamWrapper()) }, + wrap(UtDoubleStream::class) { _, addr -> objectValue(DOUBLE_STREAM_TYPE, addr, DoubleStreamWrapper()) }, + + wrap(UtSecurityManager::class) { type, addr -> objectValue(type, addr, SecurityManagerWrapper()) }, + + wrap(RangeModifiableUnlimitedArray::class) { type, addr -> + objectValue(type, addr, RangeModifiableUnlimitedArrayWrapper()) + }, + wrap(AssociativeArray::class) { type, addr -> + objectValue(type, addr, AssociativeArrayWrapper()) + }, + ).let { putAll(it) } +}.also { // check every `wrapped` class has a corresponding value in [classToWrapper] val missedWrappers = it.keys.filterNot { key -> Scene.v().getSootClass(key.name).type in classToWrapper.keys diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt index 4faffa970c..ef4c6f7af9 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt @@ -89,6 +89,7 @@ import org.utbot.engine.symbolic.asUpdate import org.utbot.engine.simplificators.MemoryUpdateSimplificator import org.utbot.engine.simplificators.simplifySymbolicStateUpdate import org.utbot.engine.simplificators.simplifySymbolicValue +import org.utbot.engine.types.ARRAYS_SOOT_CLASS import org.utbot.engine.types.CLASS_REF_SOOT_CLASS import org.utbot.engine.types.CLASS_REF_TYPE import org.utbot.engine.types.ENUM_ORDINAL @@ -3162,6 +3163,14 @@ class Traverser( return OverrideResult(success = true, cloneArray(instance)) } + if (instance == null && invocation.method.declaringClass == ARRAYS_SOOT_CLASS && invocation.method.name == "copyOf") { + return OverrideResult(success = true, copyOf(invocation.parameters)) + } + + if (instance == null && invocation.method.declaringClass == ARRAYS_SOOT_CLASS && invocation.method.name == "copyOfRange") { + return OverrideResult(success = true, copyOfRange(invocation.parameters)) + } + instanceAsWrapperOrNull?.run { // For methods with concrete implementation (for example, RangeModifiableUnlimitedArray.toCastedArray) // we should not return successful override result. @@ -3215,6 +3224,69 @@ class Traverser( return MethodResult(clone, constraints.asHardConstraint(), memoryUpdates = memoryUpdate) } + private fun TraversalContext.copyOf(parameters: List): MethodResult { + val src = parameters[0] as ArrayValue + val length = parameters[1] as PrimitiveValue + + val isNegativeLength = Lt(length, 0) + implicitlyThrowException(NegativeArraySizeException("Length is less than zero"), setOf(isNegativeLength)) + queuedSymbolicStateUpdates += mkNot(isNegativeLength).asHardConstraint() + + val arrayType = src.type + val newArray = createNewArray(length, arrayType, arrayType.elementType) + + return MethodResult( + newArray, + memoryUpdates = arrayUpdateWithValue(newArray.addr, arrayType, selectArrayExpressionFromMemory(src)) + ) + } + + private fun TraversalContext.copyOfRange(parameters: List): MethodResult { + val original = parameters[0] as ArrayValue + val from = parameters[1] as PrimitiveValue + val to = parameters[2] as PrimitiveValue + + val originalLength = memory.findArrayLength(original.addr) + + val isNegativeFrom = Lt(from, 0) + implicitlyThrowException(ArrayIndexOutOfBoundsException("From is less than zero"), setOf(isNegativeFrom)) + queuedSymbolicStateUpdates += mkNot(isNegativeFrom).asHardConstraint() + + val isFromBiggerThanLength = Gt(from, originalLength) + implicitlyThrowException(ArrayIndexOutOfBoundsException("From is bigger than original length"), setOf(isFromBiggerThanLength)) + queuedSymbolicStateUpdates += mkNot(isFromBiggerThanLength).asHardConstraint() + + val isFromBiggerThanTo = Gt(from, to) + implicitlyThrowException(IllegalArgumentException("From is bigger than to"), setOf(isFromBiggerThanTo)) + queuedSymbolicStateUpdates += mkNot(isFromBiggerThanTo).asHardConstraint() + + val newLength = Sub(to, from) + val newLengthValue = PrimitiveValue(IntType.v(), newLength) + + val originalLengthDifference = Sub(originalLength, from) + val originalLengthDifferenceValue = PrimitiveValue(IntType.v(), originalLengthDifference) + + val resultedLength = + UtIteExpression(Lt(originalLengthDifferenceValue, newLengthValue), originalLengthDifference, newLength) + val resultedLengthValue = PrimitiveValue(IntType.v(), resultedLength) + + val arrayType = original.type + val newArray = createNewArray(newLengthValue, arrayType, arrayType.elementType) + val destPos = 0.toPrimitiveValue() + val copyValue = UtArraySetRange( + selectArrayExpressionFromMemory(newArray), + destPos, + selectArrayExpressionFromMemory(original), + from, + resultedLengthValue + ) + + return MethodResult( + voidValue, + memoryUpdates = arrayUpdateWithValue(newArray.addr, newArray.type, copyValue) + ) + } + // For now, we just create unbounded symbolic variable as a result. private fun processNativeMethod(target: InvocationTarget): List = listOf(unboundedVariable(name = "nativeConst", target.method)) diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/types/TypeResolver.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/types/TypeResolver.kt index 39c1f90b46..ef1453446c 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/types/TypeResolver.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/types/TypeResolver.kt @@ -349,6 +349,8 @@ internal val CLASS_REF_NUM_DIMENSIONS_DESCRIPTOR: MemoryChunkDescriptor internal val CLASS_REF_SOOT_CLASS: SootClass get() = Scene.v().getSootClass(CLASS_REF_CLASSNAME) +internal val ARRAYS_SOOT_CLASS: SootClass + get() = Scene.v().getSootClass("java.util.Arrays") internal val OBJECT_TYPE: RefType get() = Scene.v().getSootClass(Object::class.java.canonicalName).type