Skip to content

Commit

Permalink
Support simple calls (#246)
Browse files Browse the repository at this point in the history
Co-authored-by: Alexey Menshutin <[email protected]>
  • Loading branch information
Lipen and CaelmBleidd authored Feb 7, 2025
1 parent 54d248a commit 464fee8
Show file tree
Hide file tree
Showing 8 changed files with 502 additions and 170 deletions.
315 changes: 212 additions & 103 deletions usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
Expand Up @@ -89,16 +89,12 @@ class TSInterpreter(

private fun visitIfStmt(scope: TSStepScope, stmt: EtsIfStmt) {
val exprResolver = exprResolverWithScope(scope)
val expr = exprResolver.resolve(stmt.condition) ?: return

val conditionExpr = exprResolver.resolve(stmt.condition) ?: run {
logger.warn { "Failed to resolve condition: $stmt" }
return
}

val boolExpr = if (conditionExpr.sort == ctx.boolSort) {
conditionExpr.asExpr(ctx.boolSort)
val boolExpr = if (expr.sort == ctx.boolSort) {
expr.asExpr(ctx.boolSort)
} else {
ctx.mkTruthyExpr(conditionExpr, scope)
ctx.mkTruthyExpr(expr, scope)
}

val (negStmt, posStmt) = applicationGraph.successors(stmt).take(2).toList()
Expand Down Expand Up @@ -126,7 +122,6 @@ class TSInterpreter(

private fun visitAssignStmt(scope: TSStepScope, stmt: EtsAssignStmt) {
val exprResolver = exprResolverWithScope(scope)

val expr = exprResolver.resolve(stmt.rhv) ?: return

check(expr.sort != ctx.unresolvedSort) {
Expand All @@ -135,7 +130,7 @@ class TSInterpreter(

scope.doWithState {
val idx = mapLocalToIdx(lastEnteredMethod, stmt.lhv)
saveSortForLocal(lastEnteredMethod, idx, expr.sort)
saveSortForLocal(idx, expr.sort)

val lValue = URegisterStackLValue(expr.sort, idx)
memory.write(lValue, expr.asExpr(lValue.sort), guard = ctx.trueExpr)
Expand All @@ -146,10 +141,17 @@ class TSInterpreter(
}

private fun visitCallStmt(scope: TSStepScope, stmt: EtsCallStmt) {
TODO() // IMPORTANT do not forget to fill sorts of arguments map
val exprResolver = exprResolverWithScope(scope)
exprResolver.resolve(stmt.expr) ?: return

scope.doWithState {
val nextStmt = stmt.nextStmt ?: return@doWithState
newStmt(nextStmt)
}
}

private fun visitThrowStmt(scope: TSStepScope, stmt: EtsThrowStmt) {
// TODO do not forget to pop the sorts call stack in the state
TODO()
}

Expand Down
Loading

0 comments on commit 464fee8

Please sign in to comment.