Basic USVM TS type system with type coercion #215
Conversation
…rgeyl/ts_typecoercion
# Conflicts: # usvm-core/src/main/kotlin/org/usvm/StateForker.kt # usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
There was a problem hiding this comment.
detekt found more than 20 potential problems in the proposed changes. Check the Files changed tab for more details.
|
This PR indirectly introduces a bug |
|
|
||
| class TSTestResolver { | ||
| class TSTestResolver( | ||
| private val state: TSState |
There was a problem hiding this comment.
Why? Resolver should be able to resolve many states independently
There was a problem hiding this comment.
TSTestResolver was instantiated for each returned state, and I needed access to state.typeStorage.
So I decided to add state as private constructor param.
| private fun approximateParam(expr: UConcreteHeapRef, idx: Int, model: UModelBase<EtsType>): TSObject = | ||
| with(expr.ctx as TSContext) { | ||
| val suggestedType = state.getSuggestedType(idx) | ||
| return suggestedType?.let { newType -> |
There was a problem hiding this comment.
Something odd is happening here. You can always access all required information using symbolic values and symbolic values only, otherwise you will encounter path divergence. This map cannot be built from concrete values to type info, only from symbolic ones
There was a problem hiding this comment.
I believe different types of ref entities (reg readings, etc.) have unique ways to generate a key. For example, reg readings can use its' idx field as a key, and this key leads to correct list of types from any model.
There was a problem hiding this comment.
But you might store it with another key -- if I resolve something from registerReading(1), it doesn't mean that I always accessed this value using this key. Probably, I could do it with registerReading(2).getByIndex(3), i could have accessed it with RR(3) (because of aliasing) and many many other ways
| // TODO: draft | ||
| override fun internEquals(other: Any): Boolean = structurallyEqual(other) |
There was a problem hiding this comment.
Why is it a draft? Seems like we can implement it
| 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) { | ||
| addressSort -> addedExprCache.putOrNull(mkEq(fpToBoolSort(asFp64()), asBool())) |
There was a problem hiding this comment.
Why don't we need to add a connection between baseSort expr and them? If it already exists for baseSort <-> fp and bool, it exists for bool and fp by transitivity as well
| private fun approximateParam(expr: UConcreteHeapRef, idx: Int, model: UModelBase<EtsType>): TSObject = | ||
| with(expr.ctx as TSContext) { | ||
| val suggestedType = state.getSuggestedType(idx) | ||
| return suggestedType?.let { newType -> |
There was a problem hiding this comment.
But you might store it with another key -- if I resolve something from registerReading(1), it doesn't mean that I always accessed this value using this key. Probably, I could do it with registerReading(2).getByIndex(3), i could have accessed it with RR(3) (because of aliasing) and many many other ways
| // (primitives can't be cast to ref in TypeScript type coercion) | ||
| addressSort -> { | ||
| val fpToBoolLink = mkEq(fpToBoolSort(asFp64()), asBool()) | ||
| val boolToRefLink = mkEq(asBool(), (baseExpr as UExpr<UAddressSort>).neq(mkNullRef())) |
Check warning
Code scanning / detekt
Reports multiple space usages Warning
| @@ -6,7 +6,9 @@ | |||
| import org.usvm.PathNode | |||
| import org.usvm.TSContext | |||
| import org.usvm.TSTarget | |||
| import org.usvm.UAddressSort | |||
Check warning
Code scanning / detekt
Detects unused imports Warning
| import org.usvm.UCallStack | ||
| import org.usvm.UExpr |
Check warning
Code scanning / detekt
Detects unused imports Warning
|
|
||
| private fun approximateParam(expr: UConcreteHeapRef, idx: Int, model: UModelBase<EtsType>): TSObject = | ||
| when (val tr = model.typeStreamOf(expr).take(1)) { | ||
| is TypesResult.SuccessfulTypesResult -> with (expr.tctx) { |
Check warning
Code scanning / detekt
Reports spaces around parentheses Warning test
No description provided.