-
Notifications
You must be signed in to change notification settings - Fork 16
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.
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 of UTypeStream
s and casts in JcInterpreter
#34
Conversation
e13ca83
to
659d9f2
Compare
c568a19
to
eeb1168
Compare
This reverts commit c224edf.
UTypeStream
s, casts and instanceof
UTypeStream
s and casts in JcInterpreter
usvm-jvm/src/test/kotlin/org/usvm/samples/primitives/DoubleExamplesTest.kt
Outdated
Show resolved
Hide resolved
usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt
Outdated
Show resolved
Hide resolved
usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt
Outdated
Show resolved
Hide resolved
usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt
Outdated
Show resolved
Hide resolved
usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt
Outdated
Show resolved
Hide resolved
usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt
Outdated
Show resolved
Hide resolved
private set | ||
|
||
private val topTypeRegion by lazy { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We store this field for each type constraint although it depends only on the type system. Isn't it better to keep it in a type system, for memory optimization purposes?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hm, I'd prefer keeping it as it is, because UTypeRegion
is something internal, whereas UTypeSystem
is an open interface for target languages.
usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt
Outdated
Show resolved
Hide resolved
) : Region<UTypeRegion<Type>> { | ||
val isContradicting get() = typeStream.isEmpty |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What about using by lazy
instead of getter?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Don't want to have extra memory allocations. Evaluation of typeStream.isEmpty
for subsequent calls works fast
824b022
to
bc5436c
Compare
8b9d7bf
to
5131269
Compare
5131269
to
7209949
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
807592d
to
b53cccf
Compare
Co-authored-by: Yury Kamenev <yurkam447@gmail.com> (cherry picked from commit 34e6503)
This PR introduces an initial support of types in
JcInterpreter
. Also, some other improvements were made, including fix of binary operations for integral types. The Java tests were revised, some of them were enabled. Disabling reasons were updated.Details
UIsExpr
Represents a constraint that either some ref is null, or it's not null and its type is a subtype of some other type. This corresponds to a reference cast in Java, but not to
instanceof
. It brings confusion, so maybe we should rename it, or change its semantics.UTypeSystem
A base interface, instantiated in target machines. Provides information about types and
topTypeStream
, representing all possible types in the system.UTypeStream
A base interface representing persistent type constraints and a way to access types satisfying them. Consists of a conjunction of constraints of four kinds:
It doesn't have references to an actual ref expression.
USupportTypeStream
A generic implementation of
UTypeStream
interface based on support type. It works as follows:object
in the beginningType constraints solving
It's a DPLL(T)-like procedure. Briefly, getting complete
UModelBase
with type assignment, satisfyingpc: UPathConstraints
, works as follows:KModel
model: UModelBase
without any type informationmodel
satisfies the type constraints. There could be 4 results:model
with a type model and return the completeUModelBase
pc
is unsatisfiableUTypeStream
evaluation didn't finish, so we return unknown result.The disequality constraints determined as follows:
Example:
Suppose we have the single cluster, so we process it as follows:
a
. The current region is empty, so it becomesT1 | T2
. Potential conflicting refs ={a}
.b
. The current region becomesT2
. Potential conflicting refs ={a, b}
.c
. The intersection of the current region withT3 | T1
is empty, so we add the following constraint:a != c || b != c || a == null || b == null || c == null
. The region becomesT3 | T1
. Potential conflicting refs = `{c}.d
. The current region becomesT1
. Potential conflicting refs ={c, d}
.e
. The intersection of the current region withT2
is empty, so we add the following constraint:c != e || d != e || c == null || d == null || e == null
.Note that symbolic objects of definitely incomparable types resolve to different concrete references thanks to
UEqualityConstraints
.UTypeModel
It's a storage for types of input values. We assume, that no allocated references can leak to the
UModelBase
, so it throws in such case. For every input reference, it stores aUTypeStream
. Resolution of theevalIs(ref: UHeapRef, type: Type)
processes in the next steps:(ref as UConcreteHeapRef).address
in the cache. If noUTypeStream
found, take the top type stream.<: type
.This lazy procedure allows reducing the number of requests to the solver.
UReadOnlyTypedMemory
To unify types handling in a memory and in a model, I introduced
UReadOnlyTypedMemory
interface with a single method:JcTestResolver
It was noticeably improved to support the type resolution. Also fixed some problems with arrays. The type resolution works as follows:
Further work
(a instanceof T).not()
Questions
isTerminated
flag as a return value inUTypeStream
? (No, let's assumetake
works negligibly little time.)UIsExpr
, because it isn'tinstanceof
?JcTestResolver
? (MakeUTypedReadOnlyMemory
)Other
JcTestResolver
PR TODO