Tmp commit

CaelmBleidd · CaelmBleidd · commit 5ed9332da9db · 2025-05-30T16:28:36.000+03:00
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -663,15 +663,18 @@ class TsExprResolver(
             isSigned = true,
         ).asExpr(sizeSort)
 
+        // TODO add test for array as parameter and reading as parameter, seems like it produces not fake object
         val lValue = mkArrayIndexLValue(
             sort = addressSort,
             ref = array,
             index = bvIndex,
-            type = value.array.type as EtsArrayType
+            type = EtsArrayType(EtsUnknownType, 1)
         )
         val expr = scope.calcOnState { memory.read(lValue) }
 
-        check(expr.isFakeObject()) { "Only fake objects are allowed in arrays" }
+        check(expr.isFakeObject()) {
+            "Only fake objects are allowed in arrays"
+        }
 
         return expr
     }
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt
@@ -127,7 +127,12 @@ class TsInterpreter(
                 is EtsCallStmt -> visitCallStmt(scope, stmt)
                 is EtsThrowStmt -> visitThrowStmt(scope, stmt)
                 is EtsNopStmt -> visitNopStmt(scope, stmt)
-                else -> error("Unknown stmt: $stmt")
+                else -> {
+                    logger.error { "Unknown stmt: $stmt" }
+                    scope.doWithState {
+                        newStmt(graph.successors(stmt).single())
+                    }
+                }
             }
         } catch (e: Exception) {
             logger.error {
@@ -488,12 +493,14 @@ class TsInterpreter(
                                             expr.extractBool(scope)
                                         }
                                     }
+
                                     is EtsNumberType -> {
                                         scope.calcOnState {
                                             pathConstraints += expr.getFakeType(scope).fpTypeExpr
                                             expr.extractFp(scope)
                                         }
                                     }
+
                                     else -> {
                                         scope.calcOnState {
                                             pathConstraints += expr.getFakeType(scope).refTypeExpr

Original file line number	Diff line number	Diff line change
`@@ -127,7 +127,12 @@ class TsInterpreter(`
`127`	`127`	`is EtsCallStmt -> visitCallStmt(scope, stmt)`
`128`	`128`	`is EtsThrowStmt -> visitThrowStmt(scope, stmt)`
`129`	`129`	`is EtsNopStmt -> visitNopStmt(scope, stmt)`
`130`		`- else -> error("Unknown stmt: $stmt")`
	`130`	`+ else -> {`
	`131`	`+ logger.error { "Unknown stmt: $stmt" }`
	`132`	`+ scope.doWithState {`
	`133`	`+ newStmt(graph.successors(stmt).single())`
	`134`	`+ }`
	`135`	`+ }`
`131`	`136`	`}`
`132`	`137`	`} catch (e: Exception) {`
`133`	`138`	`logger.error {`
`@@ -488,12 +493,14 @@ class TsInterpreter(`
`488`	`493`	`expr.extractBool(scope)`
`489`	`494`	`}`
`490`	`495`	`}`
	`496`	`+`
`491`	`497`	`is EtsNumberType -> {`
`492`	`498`	`scope.calcOnState {`
`493`	`499`	`pathConstraints += expr.getFakeType(scope).fpTypeExpr`
`494`	`500`	`expr.extractFp(scope)`
`495`	`501`	`}`
`496`	`502`	`}`
	`503`	`+`
`497`	`504`	`else -> {`
`498`	`505`	`scope.calcOnState {`
`499`	`506`	`pathConstraints += expr.getFakeType(scope).refTypeExpr`