Added missing num dimension constraints for generics

Author: Kamenev Yury

utbot-framework/src/main/kotlin/org/utbot/engine/Memory.kt

@@ -431,7 +431,6 @@ class TypeRegistry {
 
     private val genericAddrToNumDimensionsArrays = mutableMapOf<Int, UtArrayExpressionBase>()
 
-    @Suppress("unused")
     private fun genericAddrToNumDimensions(i: Int) = genericAddrToNumDimensionsArrays.getOrPut(i) {
         mkArrayConst(
             "genericAddrToNumDimensions_$i",
@@ -562,6 +561,8 @@ class TypeRegistry {
      */
     fun symNumDimensions(addr: UtAddrExpression) = addrToNumDimensions.select(addr)
 
+    fun genericNumDimensions(addr: UtAddrExpression, i: Int) = genericAddrToNumDimensions(i).select(addr)
+
     /**
      * Returns a constraint stating that number of dimensions for the given address is zero
      */

utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt

@@ -226,10 +226,13 @@ open class Z3TranslatorVisitor(
     override fun visit(expr: UtGenericExpression): Expr = expr.run {
         val constraints = mutableListOf<BoolExpr>()
         for (i in types.indices) {
+            val symNumDimensions = translate(typeRegistry.genericNumDimensions(addr, i)) as BitVecExpr
             val symType = translate(typeRegistry.genericTypeId(addr, i))
+
             if (types[i].leastCommonType.isJavaLangObject()) {
                  continue
             }
+
             val possibleBaseTypes = types[i].possibleConcreteTypes.map { it.baseType }
 
             val typeConstraint = z3Context.mkOr(
@@ -241,6 +244,22 @@ open class Z3TranslatorVisitor(
                 }.toTypedArray()
             )
             constraints += typeConstraint
+
+            val numDimensionsConstraint = z3Context.mkAnd(
+                *possibleBaseTypes.map {
+                    val numDimensions = z3Context.mkBV(it.numDimensions, Int.SIZE_BITS)
+
+                    if (it.isJavaLangObject()) {
+                        z3Context.mkBVSGE(symNumDimensions, numDimensions)
+                    } else {
+                        z3Context.mkEq(symNumDimensions, numDimensions)
+                    }
+                }.toTypedArray()
+            )
+
+            constraints += numDimensionsConstraint
+
+            z3Context.mkAnd(*constraints.toTypedArray())
         }
         z3Context.mkOr(
             z3Context.mkAnd(*constraints.toTypedArray()),
@@ -250,11 +269,19 @@ open class Z3TranslatorVisitor(
 
     override fun visit(expr: UtIsGenericTypeExpression): Expr = expr.run {
         val symType = translate(typeRegistry.symTypeId(addr))
+        val symNumDimensions = translate(typeRegistry.symNumDimensions(addr))
+
         val genericSymType = translate(typeRegistry.genericTypeId(baseAddr, parameterTypeIndex))
-        z3Context.mkOr(
+        val genericNumDimensions = translate(typeRegistry.genericNumDimensions(baseAddr, parameterTypeIndex))
+
+        val typeConstraint = z3Context.mkOr(
             z3Context.mkEq(symType, genericSymType),
             z3Context.mkEq(translate(expr.addr), translate(nullObjectAddr))
         )
+
+        val dimensionsConstraint = z3Context.mkEq(symNumDimensions, genericNumDimensions)
+
+        z3Context.mkAnd(typeConstraint, dimensionsConstraint)
     }
 
     override fun visit(expr: UtEqGenericTypeParametersExpression): Expr = expr.run {
@@ -263,6 +290,10 @@ open class Z3TranslatorVisitor(
             val firstSymType = translate(typeRegistry.genericTypeId(firstAddr, i))
             val secondSymType = translate(typeRegistry.genericTypeId(secondAddr, j))
             constraints += z3Context.mkEq(firstSymType, secondSymType)
+
+            val firstSymNumDimensions = translate(typeRegistry.genericNumDimensions(firstAddr, i))
+            val secondSymNumDimensions = translate(typeRegistry.genericNumDimensions(secondAddr, j))
+            constraints += z3Context.mkEq(firstSymNumDimensions, secondSymNumDimensions)
         }
         z3Context.mkAnd(*constraints.toTypedArray())
     }