Removed commented out code

usvm-python/usvm-python-main/src/main/java/org/usvm/interpreter/CPythonAdapter.java

@@ -553,6 +553,7 @@ public static SymbolForCPython handlerPOSFloat(ConcolicRunContext context, Symbo
     }
 
     @CPythonAdapterJavaMethod(cName = "bool_and")
+    // might be useful in the future, but now this annotation leads to warning during compilation, and that is treated as error
     /*@CPythonFunction(
             argCTypes = {CType.PyObject, CType.PyObject},
             argConverters = {ObjectConverter.StandardConverter, ObjectConverter.StandardConverter},

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/language/Program.kt

@@ -67,7 +67,6 @@ class StructuredPyProgram(val roots: Set<File>): PyProgram(roots) {
             "$acc$name."
         }
         val resultAsObj = ConcretePythonInterpreter.eval(namespace, "$module.__dict__")
-        //println(module)
         if (ConcretePythonInterpreter.getPythonObjectTypeName(resultAsObj) != "dict")
             return null
         return PyNamespace(resultAsObj.address)

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/language/types/ElementConstraints.kt

@@ -10,7 +10,6 @@ import org.usvm.machine.symbolicobjects.TimeOfCreation
 import org.usvm.machine.PyContext
 import org.usvm.machine.model.PyModel
 import org.usvm.machine.symbolicobjects.UninterpretedSymbolicPythonObject
-import org.usvm.model.nullAddress
 
 abstract class ElementConstraint {
     abstract fun applyUninterpreted(

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyComponents.kt

@@ -19,9 +19,7 @@ class PyComponents(
     override val useSolverForForks: Boolean = true
     override fun <Context : UContext<KIntSort>> mkSolver(ctx: Context): USolverBase<PythonType> {
         val (translator, decoder) = buildTranslatorAndLazyDecoder(ctx)
-        // val softConstraintsProvider = USoftConstraintsProvider<PythonType, KIntSort>(ctx)
         val solver = KZ3Solver(ctx)
-//        solver.configure { setZ3Option("timeout", 1) }
         return PySolver(ctx, solver, UTypeSolver(typeSystem),  translator, decoder)
     }
 

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyContext.kt

@@ -25,7 +25,6 @@ class PyContext(
 
     fun intToFloat(intValue: UExpr<KIntSort>): UExpr<KRealSort> {
         return mkIntToReal(intValue)
-        //return mkRealToFpExpr(fp64Sort, floatRoundingMode, realValue)
     }
 
 

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyMachine.kt

@@ -116,11 +116,6 @@ class PyMachine(
                 PyPinnedCallable(substituted)
             }
             val pyObserver = PythonMachineObserver(saver.newStateObserver)
-            /*val coverageStatistics =
-                CoverageStatistics<PyCallable, PyInstruction, PyState>(
-                    setOf(pinnedCallable),
-                    PyApplicationGraph()
-                )*/
             val observer = CompositeUMachineObserver(pyObserver)
             val startTime = System.currentTimeMillis()
             val stopTime = timeoutMs?.let { startTime + it }

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyState.kt

@@ -9,17 +9,12 @@ import org.usvm.language.*
 import org.usvm.language.types.*
 import org.usvm.machine.interpreters.symbolic.operations.tracing.SymbolicHandlerEvent
 import org.usvm.machine.model.PyModel
-import org.usvm.machine.ps.strategies.TypeRating
 import org.usvm.machine.symbolicobjects.PreallocatedObjects
-import org.usvm.machine.ps.types.SymbolTypeTree
-import org.usvm.machine.ps.types.prioritizeTypes
 import org.usvm.memory.UMemory
 import org.usvm.targets.UTarget
 import org.usvm.types.UTypeStream
-import org.usvm.machine.utils.MAX_CONCRETE_TYPES_TO_CONSIDER
 import org.usvm.model.UModelBase
 import org.usvm.targets.UTargetsSet
-import org.usvm.types.TypesResult
 
 object PyTarget: UTarget<PyInstruction, PyTarget>()
 private val targets = UTargetsSet.empty<PyTarget, PyInstruction>()
@@ -82,7 +77,6 @@ class PyState(
         val cached = mocks[what]
         if (cached != null)
             return MockResult(UninterpretedSymbolicPythonObject(cached, typeSystem), false, cached)
-        // println("what.args: ${what.args}")
         val result = memory.mocker.call(what.method, what.args.map { it.address }.asSequence(), ctx.addressSort)
         mocks[what] = result
         what.methodOwner?.let { mockedObjects.add(it) }

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/symbolic/operations/basic/Common.kt

@@ -156,7 +156,6 @@ fun handlerStandardTpGetattroKt(
     if (ctx.curState == null)
         return null
     val concreteStr = ctx.curState!!.preAllocatedObjects.concreteString(name) ?: return null
-    // println("Attr: $concreteStr")
     val type = obj.getTypeIfDefined(ctx) as? ConcretePythonType ?: return null
     val concreteDescriptor = ConcretePythonInterpreter.typeLookup(type.asObject, concreteStr)
     var defaultValue: UninterpretedSymbolicPythonObject? = null
@@ -172,7 +171,6 @@ fun handlerStandardTpGetattroKt(
     if (!ConcretePythonInterpreter.typeHasStandardDict(type.asObject))
         return null
     val containsFieldCond = obj.containsField(ctx, name)
-    // println("Attr result: ${ctx.modelHolder.model.eval(containsFieldCond).isTrue}")
     val result = obj.getFieldValue(ctx, name)
 
     val typeSystem = ctx.typeSystem

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/symbolic/operations/basic/Long.kt

@@ -31,8 +31,6 @@ private fun <RES_SORT: KSort> createBinaryIntOp(
         null
     else with (ctx.ctx) {
         val typeSystem = ctx.typeSystem
-        // val possibleTypes = listOf(typeSystem.pythonInt, typeSystem.pythonBool)
-        // addPossibleSupertypes(ctx, listOf(left, right), possibleTypes)
         if (left.getTypeIfDefined(ctx) != typeSystem.pythonInt) {
             myFork(ctx, left.evalIs(ctx, typeSystem.pythonInt))
         } else {

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/symbolic/operations/basic/MethodNotifications.kt

@@ -7,7 +7,6 @@ import org.usvm.language.types.*
 @Suppress("unused_parameter")
 fun nbBoolKt(context: ConcolicRunContext, on: UninterpretedSymbolicPythonObject) {
     context.curState ?: return
-    // on.addSupertypeSoft(context, HasNbBool)  // TODO
 }
 
 fun nbIntKt(context: ConcolicRunContext, on: UninterpretedSymbolicPythonObject) {

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/PyModel.kt

@@ -14,10 +14,8 @@ import org.usvm.collection.set.primitive.USetRegionId
 import org.usvm.collection.set.ref.URefSetEntryLValue
 import org.usvm.collection.set.ref.URefSetRegionId
 import org.usvm.constraints.UPathConstraints
-import org.usvm.interpreter.ConcolicRunContext
 import org.usvm.language.types.*
 import org.usvm.machine.PyContext
-import org.usvm.machine.PyState
 import org.usvm.machine.model.regions.*
 import org.usvm.memory.UMemoryRegionId
 import org.usvm.memory.UReadOnlyMemoryRegion

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/Utils.kt

@@ -14,7 +14,6 @@ import org.usvm.machine.PyState
 import org.usvm.model.UModelBase
 import org.usvm.types.TypesResult
 
-
 fun UModelBase<PythonType>.toPyModel(
     ctx: PyContext,
     ps: UPathConstraints<PythonType>,
@@ -55,7 +54,6 @@ fun PyModel.getFirstType(address: UConcreteHeapRef): PythonType? {
             logger.error("TypeStream starting with $first instead of mock")  // TODO: supports mocks with different sets of methods
             return null
         }
-        // require(first is MockType)
     }
     return first
 }

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/ps/types/SymbolTypeTree.kt

@@ -32,7 +32,7 @@ class SymbolTypeTree(
                     NbSubtractMethod ->
                         { returnType: UtType -> createBinaryProtocol("__sub__", pythonAnyType, returnType) }
                     NbBoolMethod ->
-                        { _: UtType -> pythonAnyType /* createUnaryProtocol("__bool__", typeHintsStorage.pythonBool) */ }
+                        { _: UtType -> createUnaryProtocol("__bool__", typeHintsStorage.pythonBool) }
                     NbIntMethod ->
                         { _: UtType -> createUnaryProtocol("__int__", typeHintsStorage.pythonInt) }
                     NbNegativeMethod ->

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/symbolicobjects/SymbolicObjectConstruction.kt

@@ -21,8 +21,7 @@ fun constructInputObject(
     ctx: PyContext,
     memory: UMemory<PythonType, PyCallable>,
     pathConstraints: UPathConstraints<PythonType>,
-    typeSystem: PythonTypeSystem,
-    // preallocatedObjects: PreallocatedObjects
+    typeSystem: PythonTypeSystem
 ): UninterpretedSymbolicPythonObject {
     @Suppress("unchecked_cast")
     val address = memory.read(URegisterStackLValue(ctx.addressSort, stackIndex)) as UExpr<UAddressSort>

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/symbolicobjects/memory/ArrayLike.kt

@@ -12,13 +12,9 @@ import org.usvm.language.types.HasElementConstraint
 import org.usvm.machine.PyContext
 import org.usvm.machine.PyState
 import org.usvm.machine.interpreters.symbolic.operations.basic.myAssert
-import org.usvm.machine.model.getConcreteType
 import org.usvm.machine.symbolicobjects.*
 import org.usvm.types.first
 
-
-const val DEFAULT_ELEMENT_INDEX = -1
-
 fun UninterpretedSymbolicPythonObject.readArrayLength(ctx: ConcolicRunContext): UExpr<KIntSort> {
     val type = getTypeIfDefined(ctx)
     require(type != null && type is ArrayLikeConcretePythonType)
@@ -32,34 +28,6 @@ fun InterpretedInputSymbolicPythonObject.readArrayLength(ctx: PyContext): UExpr<
     return modelHolder.model.readArrayLength(address, ArrayType, ctx.intSort)
 }
 
-fun UninterpretedSymbolicPythonObject.defaultElement(ctx: ConcolicRunContext): UHeapRef {
-    val type = getTypeIfDefined(ctx)
-    require(ctx.curState != null && type != null && type is ArrayLikeConcretePythonType && type.innerType != null)
-    val result = ctx.curState!!.memory.readArrayIndex(
-        address,
-        ctx.ctx.mkIntNum(DEFAULT_ELEMENT_INDEX),
-        ArrayType,
-        ctx.ctx.addressSort
-    )
-    val obj = UninterpretedSymbolicPythonObject(result, ctx.typeSystem)
-    val array = this
-    val cond = with(ctx.ctx) {
-        type.elementConstraints.fold(trueExpr as UBoolExpr) { acc, constraint ->
-            acc and constraint.applyUninterpreted(array, obj, ctx)
-        }
-    }
-    myAssert(ctx, cond)
-    return result
-}
-
-fun InterpretedInputSymbolicPythonObject.defaultElement(ctx: PyContext): UConcreteHeapRef =
-    modelHolder.model.readArrayIndex(
-        address,
-        ctx.mkIntNum(DEFAULT_ELEMENT_INDEX),
-        ArrayType,
-        ctx.addressSort
-    ) as UConcreteHeapRef
-
 fun UninterpretedSymbolicPythonObject.readArrayElement(
     ctx: ConcolicRunContext,
     index: UExpr<KIntSort>
@@ -75,14 +43,7 @@ fun UninterpretedSymbolicPythonObject.readArrayElement(
         ctx.ctx.mkAnd(acc, constraint.applyUninterpreted(this, elem, ctx))
     }
     myAssert(ctx, cond)
-    val actualAddress = if (type.innerType != null) {
-        with(ctx.ctx) {
-            mkIte(mkHeapRefEq(elemAddress, nullRef), defaultElement(ctx), elemAddress)
-        }
-    } else {
-        elemAddress
-    }
-    return UninterpretedSymbolicPythonObject(actualAddress, typeSystem)
+    return UninterpretedSymbolicPythonObject(elemAddress, typeSystem)
 }
 
 fun InterpretedInputSymbolicPythonObject.readArrayElement(
@@ -96,22 +57,12 @@ fun InterpretedInputSymbolicPythonObject.readArrayElement(
         ArrayType,
         ctx.addressSort
     ) as UConcreteHeapRef
-    val actualAddress = if (element.address == 0) {
-        val type = modelHolder.model.getConcreteType(address)
-        if (type != null && type is ArrayLikeConcretePythonType && type.innerType != null) {
-            defaultElement(ctx)
-        } else {
-            element
-        }
-    } else {
-        element
-    }
-    return if (isStaticHeapRef(actualAddress)) {
-        val type = state.memory.typeStreamOf(actualAddress).first()
+    return if (isStaticHeapRef(element)) {
+        val type = state.memory.typeStreamOf(element).first()
         require(type is ConcretePythonType)
-        InterpretedAllocatedOrStaticSymbolicPythonObject(actualAddress, type, typeSystem)
+        InterpretedAllocatedOrStaticSymbolicPythonObject(element, type, typeSystem)
     } else {
-        InterpretedInputSymbolicPythonObject(actualAddress, modelHolder, typeSystem)
+        InterpretedInputSymbolicPythonObject(element, modelHolder, typeSystem)
     }
 }
 
@@ -129,12 +80,6 @@ fun UninterpretedSymbolicPythonObject.writeArrayElement(
         }
         myAssert(ctx, cond)
     }
-    if (type.innerType != null) {
-        myAssert(
-            ctx,
-            with(ctx.ctx) { mkHeapRefEq(value.address, nullRef).not() or mkHeapRefEq(defaultElement(ctx), nullRef) }
-        )
-    }
     ctx.curState!!.memory.writeArrayIndex(
         address,
         index,

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/symbolicobjects/memory/Bool.kt

@@ -12,7 +12,6 @@ import org.usvm.machine.PyContext
 import org.usvm.machine.symbolicobjects.*
 import org.usvm.memory.UMemory
 
-
 fun UninterpretedSymbolicPythonObject.getBoolContent(ctx: ConcolicRunContext): UExpr<KBoolSort> {
     require(ctx.curState != null)
     addSupertype(ctx, typeSystem.pythonBool)

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/symbolicobjects/memory/Dict.kt

@@ -25,7 +25,6 @@ import org.usvm.memory.UMemory
 import org.usvm.memory.key.USizeExprKeyInfo
 import org.usvm.types.first
 
-
 fun UninterpretedSymbolicPythonObject.dictIsEmpty(ctx: ConcolicRunContext): UBoolExpr {
     require(ctx.curState != null)
     val typeSystem = ctx.typeSystem

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/symbolicobjects/memory/Enumerate.kt

@@ -8,7 +8,6 @@ import org.usvm.interpreter.ConcolicRunContext
 import org.usvm.machine.symbolicobjects.EnumerateContents
 import org.usvm.machine.symbolicobjects.UninterpretedSymbolicPythonObject
 
-
 fun UninterpretedSymbolicPythonObject.initializeEnumerate(
     ctx: ConcolicRunContext,
     arg: UninterpretedSymbolicPythonObject

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/symbolicobjects/memory/Float.kt

@@ -14,7 +14,6 @@ import org.usvm.machine.model.PyModel
 import org.usvm.machine.symbolicobjects.*
 import org.usvm.memory.UMemory
 
-
 sealed class FloatInterpretedContent
 object FloatNan: FloatInterpretedContent()
 object FloatPlusInfinity: FloatInterpretedContent()

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/symbolicobjects/memory/Int.kt

@@ -11,7 +11,6 @@ import org.usvm.machine.PyContext
 import org.usvm.machine.symbolicobjects.*
 import org.usvm.memory.UMemory
 
-
 fun UninterpretedSymbolicPythonObject.setIntContent(ctx: ConcolicRunContext, expr: UExpr<KIntSort>) {
     require(ctx.curState != null)
     addSupertypeSoft(ctx, typeSystem.pythonInt)

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/symbolicobjects/memory/Range.kt

@@ -7,7 +7,6 @@ import org.usvm.interpreter.ConcolicRunContext
 import org.usvm.machine.symbolicobjects.RangeContents
 import org.usvm.machine.symbolicobjects.UninterpretedSymbolicPythonObject
 
-
 fun UninterpretedSymbolicPythonObject.setRangeContent(
     ctx: ConcolicRunContext,
     start: UExpr<KIntSort>,

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/symbolicobjects/memory/RangeIterator.kt

@@ -9,7 +9,6 @@ import org.usvm.machine.symbolicobjects.RangeContents
 import org.usvm.machine.symbolicobjects.RangeIteratorContents
 import org.usvm.machine.symbolicobjects.UninterpretedSymbolicPythonObject
 
-
 fun UninterpretedSymbolicPythonObject.setRangeIteratorContent(
     ctx: ConcolicRunContext,
     range: UninterpretedSymbolicPythonObject

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/symbolicobjects/memory/Set.kt

@@ -20,7 +20,6 @@ import org.usvm.machine.symbolicobjects.SetContents
 import org.usvm.machine.symbolicobjects.UninterpretedSymbolicPythonObject
 import org.usvm.memory.key.USizeExprKeyInfo
 
-
 fun UninterpretedSymbolicPythonObject.setIsEmpty(ctx: ConcolicRunContext): UBoolExpr {
     require(ctx.curState != null)
     val typeSystem = ctx.typeSystem

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/symbolicobjects/memory/Slice.kt

@@ -15,7 +15,6 @@ import org.usvm.machine.symbolicobjects.PropertyOfPythonObject
 import org.usvm.machine.symbolicobjects.SliceContents
 import org.usvm.machine.symbolicobjects.UninterpretedSymbolicPythonObject
 
-
 data class SliceInterpretedContent(
     val start: KInterpretedValue<KIntSort>?,
     val stop: KInterpretedValue<KIntSort>?,

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/symbolicobjects/memory/Str.kt

@@ -3,6 +3,5 @@ package org.usvm.machine.symbolicobjects.memory
 import org.usvm.machine.symbolicobjects.PreallocatedObjects
 import org.usvm.machine.symbolicobjects.UninterpretedSymbolicPythonObject
 
-
 fun UninterpretedSymbolicPythonObject.getConcreteStrIfDefined(preallocatedObjects: PreallocatedObjects): String? =
     preallocatedObjects.concreteString(this)

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/symbolicobjects/memory/TupleIterator.kt

@@ -9,7 +9,6 @@ import org.usvm.interpreter.ConcolicRunContext
 import org.usvm.machine.symbolicobjects.TupleIteratorContents
 import org.usvm.machine.symbolicobjects.UninterpretedSymbolicPythonObject
 
-
 fun UninterpretedSymbolicPythonObject.setTupleIteratorContent(ctx: ConcolicRunContext, tuple: UninterpretedSymbolicPythonObject) = with(ctx.ctx) {
     require(ctx.curState != null)
     addSupertypeSoft(ctx, typeSystem.pythonTupleIteratorType)

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/symbolicobjects/rendering/PyObjectRenderer.kt

@@ -53,28 +53,22 @@ class PyObjectRenderer(private val useNoneInsteadOfMock: Boolean = false) {
         val result = ConcretePythonInterpreter.eval(namespace, repr)
         converted[model] = result
         ConcretePythonInterpreter.addObjectToNamespace(namespace, result, "result")
-        if (model.listItems != null) {
-            model.listItems!!.forEach {
-                val elemRef = convert(it)
-                ConcretePythonInterpreter.addObjectToNamespace(namespace, elemRef, "elem")
-                ConcretePythonInterpreter.concreteRun(namespace, "result.append(elem)")
-            }
+        model.listItems?.forEach {
+            val elemRef = convert(it)
+            ConcretePythonInterpreter.addObjectToNamespace(namespace, elemRef, "elem")
+            ConcretePythonInterpreter.concreteRun(namespace, "result.append(elem)")
         }
-        if (model.dictItems != null) {
-            model.dictItems!!.forEach { (key, elem) ->
-                val keyRef = convert(key)
-                val elemRef = convert(elem)
-                ConcretePythonInterpreter.addObjectToNamespace(namespace, keyRef, "key")
-                ConcretePythonInterpreter.addObjectToNamespace(namespace, elemRef, "elem")
-                ConcretePythonInterpreter.concreteRun(namespace, "result[key] = elem")
-            }
+        model.dictItems?.forEach { (key, elem) ->
+            val keyRef = convert(key)
+            val elemRef = convert(elem)
+            ConcretePythonInterpreter.addObjectToNamespace(namespace, keyRef, "key")
+            ConcretePythonInterpreter.addObjectToNamespace(namespace, elemRef, "elem")
+            ConcretePythonInterpreter.concreteRun(namespace, "result[key] = elem")
         }
-        if (model.fieldDict != null) {
-            model.fieldDict!!.forEach { (name, value) ->
-                val valueRef = convert(value)
-                ConcretePythonInterpreter.addObjectToNamespace(namespace, valueRef, "value")
-                ConcretePythonInterpreter.concreteRun(namespace, "result.$name = value")
-            }
+        model.fieldDict?.forEach { (name, value) ->
+            val valueRef = convert(value)
+            ConcretePythonInterpreter.addObjectToNamespace(namespace, valueRef, "value")
+            ConcretePythonInterpreter.concreteRun(namespace, "result.$name = value")
         }
         ConcretePythonInterpreter.decref(namespace)
         return result