Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support simple calls #246

Merged
merged 4 commits into from
Feb 7, 2025
Merged

Support simple calls #246

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
63b1df0
Support simple calls
Lipen Feb 7, 2025
ec38b52
Support simple calls
Lipen Feb 7, 2025
6c922fb
Add pre-saved sort information into nested calls
CaelmBleidd Feb 7, 2025
37e032a
Remove implemented TODO
CaelmBleidd Feb 7, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
315 changes: 212 additions & 103 deletions usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt
View file
Open in desktop

Large diffs are not rendered by default.

24 changes: 13 additions & 11 deletions usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TSInterpreter.kt
View file
Open in desktop
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