Skip to content

Commit

Permalink
Detekt fix + code documentation
Browse files Browse the repository at this point in the history
  • Loading branch information
zishkaz committed Oct 8, 2024
1 parent a75a753 commit 9b7b106
Show file tree
Hide file tree
Showing 9 changed files with 23 additions and 27 deletions.
2 changes: 1 addition & 1 deletion usvm-core/src/main/kotlin/org/usvm/Expressions.kt
Original file line number Diff line number Diff line change
Expand Up @@ -324,7 +324,7 @@ class UIsSupertypeExpr<Type> internal constructor(
*/
class UJoinedBoolExpr(
ctx: UContext<*>,
val exprs: List<UBoolExpr>
val exprs: List<UBoolExpr>,
) : UBoolExpr(ctx) {
override val sort: UBoolSort
get() = ctx.boolSort
Expand Down
5 changes: 3 additions & 2 deletions usvm-ts/src/main/kotlin/org/usvm/TSBinaryOperator.kt
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ sealed class TSBinaryOperator(
// This function specifies a set of banned sorts pre-coercion.
// Usage of it is limited and was introduced for Neq operation.
// Generally designed to filter out excess expressions in type coercion.
val banSorts: TSContext.(UExpr<out USort>, UExpr<out USort>) -> Set<USort> = {_, _ -> emptySet() },
val banSorts: TSContext.(UExpr<out USort>, UExpr<out USort>) -> Set<USort> = { _, _ -> emptySet() },
) {

object Eq : TSBinaryOperator(
Expand Down Expand Up @@ -121,7 +121,8 @@ sealed class TSBinaryOperator(
val rhsSort = rhs.sort

val ctx = lhs.tctx
// Chosen sort is only used to intersect both exprCaches and have at least one sort to apply binary operation to.
// Chosen sort is only used to intersect both exprCaches and
// have at least one sort to apply binary operation to.
// All sorts are examined in TSExprTransformer class and not limited by this "chosen one".
val sort = ctx.desiredSort(lhsSort, rhsSort)

Expand Down
4 changes: 2 additions & 2 deletions usvm-ts/src/main/kotlin/org/usvm/TSExprTransformer.kt
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ class TSExprTransformer(

fun intersectWithTypeCoercion(
other: TSExprTransformer,
action: CoerceAction
action: CoerceAction,
): UExpr<out USort> {
intersect(other)

Expand Down Expand Up @@ -91,7 +91,7 @@ class TSExprTransformer(
else -> null
}

return newExpr?.let { listOf(it) } ?: emptyList()
return newExpr?.let { listOf(it) }.orEmpty()
}

fun asFp64(): UExpr<KFp64Sort> = exprCache.getOrPut(ctx.fp64Sort) {
Expand Down
5 changes: 2 additions & 3 deletions usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ class TSUndefinedValue(ctx: TSContext) : UExpr<TSUndefinedSort>(ctx) {
class TSWrappedValue(
ctx: TSContext,
val value: UExpr<out USort>,
private val scope: TSStepScope
private val scope: TSStepScope,
) : USymbol<USort>(ctx) {
override val sort: USort
get() = value.sort
Expand All @@ -55,7 +55,7 @@ class TSWrappedValue(

private fun coerce(
other: UExpr<out USort>,
action: CoerceAction
action: CoerceAction,
): UExpr<out USort> = when (other) {
is UIntepretedValue -> {
val otherTransformer = TSExprTransformer(other, scope)
Expand Down Expand Up @@ -93,7 +93,6 @@ class TSWrappedValue(
value.print(printer)
printer.append(")")
}

}

fun extractBool(expr: UExpr<out USort>): Boolean = when (expr) {
Expand Down
1 change: 1 addition & 0 deletions usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt
Original file line number Diff line number Diff line change
Expand Up @@ -158,6 +158,7 @@ class TSInterpreter(

// (method, localName) -> idx
private val localVarToIdx = mutableMapOf<EtsMethod, MutableMap<String, Int>>()

// (method, localIdx) -> sort
private val localVarToSort = mutableMapOf<EtsMethod, MutableMap<Int, USort>>()

Expand Down
8 changes: 3 additions & 5 deletions usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt
Original file line number Diff line number Diff line change
Expand Up @@ -65,11 +65,9 @@ class TSTypeSystem(
class TSTopTypeStream(
private val typeSystem: TSTypeSystem,
private val primitiveTypes: List<EtsType> = TSTypeSystem.primitiveTypes.toList(),
/* Currently only EtsUnknownType was encountered and viewed as any type.
However, there is EtsAnyType that represents any type.
TODO: replace EtsUnknownType with further TSTypeSystem implementation.
*/
// Currently only EtsUnknownType was encountered and viewed as any type.
// However, there is EtsAnyType that represents any type.
// TODO: replace EtsUnknownType with further TSTypeSystem implementation.
private val anyTypeStream: UTypeStream<EtsType> = USupportTypeStream.from(typeSystem, EtsUnknownType),
) : UTypeStream<EtsType> {

Expand Down
7 changes: 5 additions & 2 deletions usvm-ts/src/main/kotlin/org/usvm/TSUnaryOperator.kt
Original file line number Diff line number Diff line change
Expand Up @@ -17,14 +17,17 @@ sealed class TSUnaryOperator(

internal operator fun invoke(operand: UExpr<out USort>, scope: TSStepScope): UExpr<out USort> = with(operand.tctx) {
val sort = this.desiredSort(operand.sort)
val expr = if (operand is TSWrappedValue) operand.asSort(sort) else
val expr = if (operand is TSWrappedValue) {
operand.asSort(sort)
} else {
TSExprTransformer(operand, scope).transform(sort)
}

when (expr?.sort) {
is UBoolSort -> onBool(expr.cast())
is UBvSort -> onBv(expr.cast())
is UFpSort -> onFp(expr.cast())
null -> mkNullRef()
null -> error("Expression is null")
else -> error("Expressions mismatch: $expr")
}
}
Expand Down
12 changes: 2 additions & 10 deletions usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt
Original file line number Diff line number Diff line change
Expand Up @@ -174,21 +174,12 @@ open class TSMethodTestRunner : TestRunner<TSTest, MethodDescriptor, EtsType?, T
TSObject.TSNumber.Integer::class -> EtsNumberType
TSObject.UndefinedObject::class -> EtsUndefinedType
TSObject.Object::class -> EtsUnknownType
// For untyped tests, not to limit objects serialized from models after type coercion.
TSObject::class -> EtsUnknownType
else -> error("Should not be called")
}
}

private fun getProject(fileName: String): EtsFile {
val jsonWithoutExtension = "/ir/$fileName.json"
val sampleFilePath = javaClass.getResourceAsStream(jsonWithoutExtension)
?: error("Resource not found: $jsonWithoutExtension")

val etsFileDto = EtsFileDto.loadFromJson(sampleFilePath)

return convertToEtsFile(etsFileDto)
}

private fun EtsFile.getMethodByDescriptor(desc: MethodDescriptor): EtsMethod {
val cls = classes.find { it.name == desc.className }
?: error("No class ${desc.className} in project $name")
Expand All @@ -209,6 +200,7 @@ open class TSMethodTestRunner : TestRunner<TSTest, MethodDescriptor, EtsType?, T
val filePath = Paths.get(fileURL.toURI())
val scene = EtsScene(listOf(loadEtsFileAutoConvert(filePath)))

// TODO: draft implementation
val method = scene.files.single().getMethodByDescriptor(id)

TSMachine(scene, options).use { machine ->
Expand Down
6 changes: 4 additions & 2 deletions usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ import org.usvm.state.TSState
import org.usvm.types.first

class TSTestResolver(
private val state: TSState
private val state: TSState,
) {

fun resolve(method: EtsMethod): TSTest = with(state.ctx) {
Expand Down Expand Up @@ -70,7 +70,9 @@ class TSTestResolver(
val expr = model.read(lValue).extractOrThis()
if (type is EtsUnknownType) {
approximateParam(expr.cast(), idx, model)
} else resolveExpr(expr, type, model)
} else {
resolveExpr(expr, type, model)
}
}
}

Expand Down

0 comments on commit 9b7b106

Please sign in to comment.