Incorrect negation of `UtIsExpression` due to inconsistent type storage processing

[dtim]

Description

Currently the negation of UtIsExpression seems to work incorrectly for java.lang.Object.

It is related to org.utbot.engine.pc.Z3TranslatorVisitor.filterInappropriateTypes that removes internal engine classes for java.lang.Object type storage, and this logic is not fully consistent with the negation.

Another source of inconsistency is org.utbot.engine.TypeStorage#isObjectTypeStorage function. It checks that the type storage corresponds to java.lang.Object by comparing the number of subtypes in the storage with the number of subtypes in the predefined storage org.utbot.engine.TypeRegistry.Companion#getObjectTypeStorage initialized in TypeRegistry init block. This predefined storage is constructed directly from Soot classes and does not involve any logic that TypeResolver implements for all other type storage. As a result, no type storage is considered a storage for java.lang.Object at all.

The function org.utbot.engine.TypeConstraint#isConstraint contains an optimization that should return UtTrue for the is Object constraint. This optimization could fix the incorrect negation issue, but it does not, as no type storage matches the isObjectTypeStorage condition.

To fix this issue, we should:

• Remove the filtering logic from the Z3 translator and make sure that all inappropriate classes are always removed using the same algorithm (we need to be especially careful with out wrapper classes). Maybe we could always use type resolver to create all type storages, including the type storage for java.lang.Object.

To Reproduce

It is a deep internal issue, I suspect that there is no user-visible way to check for it.

An example: in org.utbot.engine.Traverser#arrayStoreExceptionCheck, inconsistent type storage initialization for Object is fixed by a special check:

if (!arrayElementType.isJavaLangObject()) {
    implicitlyThrowException(ArrayStoreException(), setOf(notIsExpression, notNull))
}

When the issue is fixed, the if expression would not be necessary anymore, as notIsExpression would be UtFalse for assignments to Object[], while now Z3 can find a model where it is true due to incorrect type storage handling.

Additional context

SAT-1321