Refactoring + code documentation

usvm-core/src/main/kotlin/org/usvm/Expressions.kt

@@ -331,14 +331,20 @@ class UJoinedBoolExpr(
 
     private val joinedExprs = ctx.mkAnd(exprs)
 
+    // Size of exprs is not big since it generates from all sorts supported by machine [n]
+    // (small number even when finished)
+    // plus possible additional constraints which are C(n - 1, 2) in size,
+    // so no need to cache this value as its use is also limited.
     fun not(): UBoolExpr = ctx.mkAnd(exprs.map(ctx::mkNot))
 
     override fun accept(transformer: KTransformerBase): KExpr<UBoolSort> {
         return transformer.apply(joinedExprs)
     }
 
+    // TODO: draft
     override fun internEquals(other: Any): Boolean = structurallyEqual(other)
 
+    // TODO: draft
     override fun internHashCode(): Int = hash()
 
     override fun print(printer: ExpressionPrinter) {

usvm-ts/src/main/kotlin/org/usvm/TSBinaryOperator.kt

@@ -2,51 +2,81 @@ package org.usvm
 
 import io.ksmt.utils.cast
 
+/**
+ * @param[desiredSort] accepts two [USort] instances of the expression operands.
+ * It defines a desired [USort] for the binary operator to cast both of its operands to.
+ *
+ * @param[banSorts] accepts two [UExpr] instances of the expression operands.
+ * It returns a [Set] of [USort] that are restricted to be coerced to.
+ */
+
+// TODO: desiredSort and banSorts achieve the same goal, although have different semantics. Possible to merge them.
 sealed class TSBinaryOperator(
     val onBool: TSContext.(UExpr<UBoolSort>, UExpr<UBoolSort>) -> UExpr<out USort> = shouldNotBeCalled,
     val onBv: TSContext.(UExpr<UBvSort>, UExpr<UBvSort>) -> UExpr<out USort> = shouldNotBeCalled,
     val onFp: TSContext.(UExpr<UFpSort>, UExpr<UFpSort>) -> UExpr<out USort> = shouldNotBeCalled,
     val onRef: TSContext.(UExpr<UAddressSort>, UExpr<UAddressSort>) -> UExpr<out USort> = shouldNotBeCalled,
+    // Some binary operations like '==' and '!=' can operate on any pair of equal sorts.
+    // However, '+' casts both operands to Number in TypeScript (no considering string currently),
+    // so fp64sort is required for both sides.
+    // This function allows to filter out excess expressions in type coercion.
     val desiredSort: TSContext.(USort, USort) -> USort = { _, _ -> error("Should not be called") },
+    // This function specifies a set of banned sorts pre-coercion.
+    // Usage of it is limited and was introduced for Neq operation.
+    // Generally designed to filter out excess expressions in type coercion.
     val banSorts: TSContext.(UExpr<out USort>, UExpr<out USort>) -> Set<USort> = {_, _ -> emptySet() },
 ) {
 
     object Eq : TSBinaryOperator(
         onBool = UContext<TSSizeSort>::mkEq,
         onBv = UContext<TSSizeSort>::mkEq,
         onFp = UContext<TSSizeSort>::mkFpEqualExpr,
-        onRef = UContext<TSSizeSort>::mkEq,
+        onRef = UContext<TSSizeSort>::mkHeapRefEq,
         desiredSort = { lhs, _ -> lhs }
     )
 
-    // Neq must not be applied to a pair of expressions generated while initial Neq application.
+    // Neq must not be applied to a pair of expressions
+    // containing generated ones during coercion initialization (exprCache intersection).
     // For example,
-    // "a (untyped arg) != 1.0 (fp64 number)"
-    // can't yield
-    // "a (bool reg reading) != true", since "1.0.toBool() = true" is a new value for 1.0.
+    // "a (ref reg reading) != 1.0 (fp64 number)"
+    // can't yield a list of type coercion bool expressions containing:
+    // "a (bool reg reading) != true (bool)",
+    // since "1.0.toBool() = true" is a new value for TSExprTransformer(1.0) exprCache.
     //
     // So, that's the reason why banSorts in Neq throws out all primitive types except one of the expressions' one.
+    // (because obviously we must be able to coerce to expression's base sort)
+
+    // TODO: banSorts is still draft here, it only handles specific operands' configurations. General solution required.
     object Neq : TSBinaryOperator(
         onBool = { lhs, rhs -> lhs.neq(rhs) },
         onBv = { lhs, rhs -> lhs.neq(rhs) },
         onFp = { lhs, rhs -> mkFpEqualExpr(lhs, rhs).not() },
-        onRef = { lhs, rhs -> lhs.neq(rhs) },
+        onRef = { lhs, rhs -> mkHeapRefEq(lhs, rhs).not() },
         desiredSort = { lhs, _ -> lhs },
         banSorts = { lhs, rhs ->
             when {
                 lhs is TSWrappedValue ->
                     // rhs.sort == addressSort is a mock not to cause undefined
                     // behaviour with support of new language features.
-                    if (rhs is TSWrappedValue || rhs.sort == addressSort) emptySet() else
+                    // For example, supporting language structures could produce
+                    // incorrect additional sort constraints here if addressSort expressions
+                    // do not return empty set.
+                    if (rhs is TSWrappedValue || rhs.sort == addressSort) {
+                        emptySet()
+                    } else {
                         TSTypeSystem.primitiveTypes
-                        .map(::typeToSort).toSet()
-                        .minus(rhs.sort)
+                            .map(::typeToSort).toSet()
+                            .minus(rhs.sort)
+                    }
                 rhs is TSWrappedValue ->
                     // lhs.sort == addressSort explained as above.
-                    if (lhs.sort == addressSort) emptySet() else
+                    if (lhs.sort == addressSort) {
+                        emptySet()
+                    } else {
                         TSTypeSystem.primitiveTypes
-                        .map(::typeToSort).toSet()
-                        .minus(lhs.sort)
+                            .map(::typeToSort).toSet()
+                            .minus(lhs.sort)
+                    }
                 else -> emptySet()
             }
         }
@@ -55,6 +85,7 @@ sealed class TSBinaryOperator(
     object Add : TSBinaryOperator(
         onFp = { lhs, rhs -> mkFpAddExpr(fpRoundingModeSortDefaultValue(), lhs, rhs) },
         onBv = UContext<TSSizeSort>::mkBvAddExpr,
+        // TODO: support string concatenation here by resolving stringSort.
         desiredSort = { _, _ -> fp64Sort },
     )
 
@@ -70,9 +101,11 @@ sealed class TSBinaryOperator(
             val ctx = lhs.tctx
             val lhsSort = lhs.sort
             val rhsSort = rhs.sort
-            assert(lhsSort == rhsSort)
+            if (lhsSort != rhsSort) error("Sorts must be equal: $lhsSort != $rhsSort")
 
+            // banSorts filtering.
             if (lhsSort in bannedSorts) return null
+            // desiredSort filtering.
             if (ctx.desiredSort(lhsSort, rhsSort) != lhsSort) return null
 
             return when (lhs.sort) {
@@ -88,6 +121,8 @@ sealed class TSBinaryOperator(
         val rhsSort = rhs.sort
 
         val ctx = lhs.tctx
+        // Chosen sort is only used to intersect both exprCaches and have at least one sort to apply binary operation to.
+        // All sorts are examined in TSExprTransformer class and not limited by this "chosen one".
         val sort = ctx.desiredSort(lhsSort, rhsSort)
 
         return when {

usvm-ts/src/main/kotlin/org/usvm/TSExprTransformer.kt

@@ -14,7 +14,7 @@ class TSExprTransformer(
     private val scope: TSStepScope,
 ) {
 
-    private val exprCache: MutableMap<USort, UExpr<out USort>?> = mutableMapOf(baseExpr.sort to baseExpr)
+    private val exprCache: MutableMap<USort, UExpr<out USort>?> = hashMapOf(baseExpr.sort to baseExpr)
     private val ctx = baseExpr.tctx
 
     init {
@@ -27,8 +27,9 @@ class TSExprTransformer(
         val (result, type) = when (sort) {
             fp64Sort -> asFp64() to EtsNumberType
             boolSort -> asBool() to EtsBooleanType
+            // No primitive type can be suggested from ref -- null is returned.
             addressSort -> asRef() to null
-            else -> error("")
+            else -> error("Unknown sort: $sort")
         }
 
         if (modifyConstraints && type != null) suggestType(type)
@@ -47,17 +48,21 @@ class TSExprTransformer(
             val rhv = other.transform(sort)
             if (lhv != null && rhv != null) {
                 action(lhv, rhv)
-            } else null
+            } else {
+                null
+            }
         }
 
         val innerCoercionExprs = this.generateAdditionalExprs(rawExprs) + other.generateAdditionalExprs(rawExprs)
 
         val exprs = rawExprs + innerCoercionExprs
 
         return if (exprs.size > 1) {
-            assert(exprs.all { it.sort == ctx.boolSort })
+            if (!exprs.all { it.sort == ctx.boolSort }) error("All expressions must be of bool sort.")
             UJoinedBoolExpr(ctx, exprs.cast())
-        } else exprs.single()
+        } else {
+            exprs.single()
+        }
     }
 
     private fun intersect(other: TSExprTransformer) {
@@ -69,7 +74,7 @@ class TSExprTransformer(
         }
     }
 
-    private val addedExprCache: MutableSet<UExpr<out USort>> = mutableSetOf()
+    private val addedExprCache: MutableSet<UExpr<out USort>> = hashSetOf()
 
     /**
      * Generates and caches additional constraints for coercion expression list.
@@ -81,6 +86,7 @@ class TSExprTransformer(
     private fun generateAdditionalExprs(rawExprs: List<UExpr<out USort>>): List<UExpr<out USort>> = with(ctx) {
         if (!rawExprs.all { it.sort == boolSort }) return emptyList()
         val newExpr = when (baseExpr.sort) {
+            // Saves link in constraints between asFp64(ref) and asBool(ref) since they were instantiated separately.
             addressSort -> addedExprCache.putOrNull(mkEq(fpToBoolSort(asFp64()), asBool()))
             else -> null
         }
@@ -96,7 +102,7 @@ class TSExprTransformer(
                 TSRefTransformer(ctx, fp64Sort).apply(baseExpr.cast()).cast()
             }
 
-            else -> ctx.mkFp64(0.0)
+            else -> error("Unsupported sort: ${baseExpr.sort}")
         }
     }.cast()
 
@@ -109,15 +115,15 @@ class TSExprTransformer(
                 TSRefTransformer(ctx, boolSort).apply(baseExpr.cast()).cast()
             }
 
-            else -> ctx.mkFalse()
+            else -> error("Unsupported sort: ${baseExpr.sort}")
         }
     }.cast()
 
     fun asRef(): UExpr<UAddressSort>? = exprCache.getOrPut(ctx.addressSort) {
         when (baseExpr.sort) {
             ctx.addressSort -> baseExpr
-            /* ctx.mkTrackedSymbol(ctx.addressSort) is possible here, but
-               no constraint-wise benefits of using it instead of null were currently found. */
+            // ctx.mkTrackedSymbol(ctx.addressSort) is possible here, but
+            // no constraint-wise benefits of using it instead of null were currently found.
             else -> null
         }
     }.cast()
@@ -131,7 +137,7 @@ class TSExprTransformer(
 /**
  * Transforms [UExpr] with [UAddressSort]:
  *
- * UExpr(address sort) -> UExpr'(sort).
+ * UExpr(address sort) -> UExpr'([sort]).
  *
  * TODO: Implement other expressions with address sort.
  */

usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt

@@ -82,8 +82,10 @@ class TSWrappedValue(
         return value.cast()
     }
 
+    // TODO: draft
     override fun internEquals(other: Any): Boolean = structurallyEqual(other)
 
+    // TODO: draft
     override fun internHashCode(): Int = hash()
 
     override fun print(printer: ExpressionPrinter) {

usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt

@@ -77,6 +77,7 @@ class TSInterpreter(
         val exprResolver = exprResolverWithScope(scope)
 
         val boolExpr = exprResolver
+            // Don't want to lose UJoinedBoolExpr here for further fork.
             .resolveTSExprNoUnwrap(stmt.condition)
             ?.asExpr(ctx.boolSort)
             ?: return

usvm-ts/src/main/kotlin/org/usvm/TSTypeStorage.kt

@@ -14,10 +14,10 @@ class TSTypeStorage(
 ) {
 
     fun storeSuggestedType(ref: UExpr<UAddressSort>, type: EtsType) {
-        // TODO: finalize implementation and remove this assert
-        assert(ref is URegisterReading)
+        // TODO: finalize implementation and remove this.
+        if (ref !is URegisterReading) error("Unsupported yet!")
 
-        keyToTypes.getOrPut((ref as URegisterReading).idx) {
+        keyToTypes.getOrPut(ref.idx) {
             mutableSetOf()
         }.add(type)
     }