Skip to content

Commit 57856b7

Browse files
CaelmBleiddCaelmBleidd
authored
Rename TS to Ts prefix (#249)
1 parent 9fab1d1 commit 57856b7

37 files changed

+547
-550
lines changed

‎usvm-ts/src/main/kotlin/org/usvm/api/TSTest.kt‎

Lines changed: 0 additions & 57 deletions
This file was deleted.

‎usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
package org.usvm.api
2+
3+
import org.jacodb.ets.base.EtsStmt
4+
5+
data class TsTest(
6+
val parameters: List<TsObject>,
7+
val returnValue: TsObject,
8+
val trace: List<EtsStmt>? = null,
9+
)
10+
11+
open class TsMethodCoverage
12+
13+
object NoCoverage : TsMethodCoverage()
14+
15+
sealed interface TsObject {
16+
sealed interface TsNumber : org.usvm.api.TsObject {
17+
data class Integer(val value: Int) : TsNumber
18+
19+
data class Double(val value: kotlin.Double) : TsNumber
20+
21+
val number: kotlin.Double
22+
get() = when (this) {
23+
is Integer -> value.toDouble()
24+
is Double -> value
25+
}
26+
27+
val truthyValue: Boolean
28+
get() = number != 0.0 && !number.isNaN()
29+
}
30+
31+
data class TsString(val value: String) : org.usvm.api.TsObject
32+
33+
data class TsBoolean(val value: Boolean) : org.usvm.api.TsObject {
34+
val number: Double
35+
get() = if (value) 1.0 else 0.0
36+
}
37+
38+
data class TsBigInt(val value: String) : org.usvm.api.TsObject
39+
40+
data class TsClass(val name: String, val properties: Map<String, org.usvm.api.TsObject>) :
41+
org.usvm.api.TsObject
42+
43+
data object TsAny : org.usvm.api.TsObject
44+
45+
data object TsUndefinedObject : org.usvm.api.TsObject
46+
47+
data class TsArray(val values: List<org.usvm.api.TsObject>) :
48+
org.usvm.api.TsObject
49+
50+
data class TsObject(val addr: Int) : org.usvm.api.TsObject
51+
52+
data object TsUnknown : org.usvm.api.TsObject
53+
54+
data object TsNull : org.usvm.api.TsObject
55+
56+
data object TsException : org.usvm.api.TsObject
57+
}

usvm-ts/src/main/kotlin/org/usvm/api/targets/TSTarget.kt renamed to usvm-ts/src/main/kotlin/org/usvm/api/targets/TsTarget.kt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,4 @@ package org.usvm.api.targets
33
import org.jacodb.ets.base.EtsStmt
44
import org.usvm.targets.UTarget
55

6-
class TSTarget : UTarget<EtsStmt, TSTarget>()
6+
class TsTarget : UTarget<EtsStmt, TsTarget>()

usvm-ts/src/main/kotlin/org/usvm/machine/TSApplicationGraph.kt renamed to usvm-ts/src/main/kotlin/org/usvm/machine/TsApplicationGraph.kt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ import org.usvm.dataflow.ts.graph.EtsApplicationGraph
77
import org.usvm.dataflow.ts.graph.EtsApplicationGraphImpl
88
import org.usvm.statistics.ApplicationGraph
99

10-
class TSApplicationGraph(scene: EtsScene) : ApplicationGraph<EtsMethod, EtsStmt> {
10+
class TsApplicationGraph(scene: EtsScene) : ApplicationGraph<EtsMethod, EtsStmt> {
1111
private val applicationGraph: EtsApplicationGraph = EtsApplicationGraphImpl(scene)
1212

1313
override fun predecessors(node: EtsStmt): Sequence<EtsStmt> =

usvm-ts/src/main/kotlin/org/usvm/machine/TSComponents.kt renamed to usvm-ts/src/main/kotlin/org/usvm/machine/TsComponents.kt

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -19,40 +19,40 @@ import org.usvm.solver.USolverBase
1919
import org.usvm.solver.UTypeSolver
2020
import org.usvm.types.UTypeSystem
2121

22-
class TSComponents(
23-
private val typeSystem: TSTypeSystem,
22+
class TsComponents(
23+
private val typeSystem: TsTypeSystem,
2424
private val options: UMachineOptions,
25-
) : UComponents<EtsType, TSSizeSort> {
25+
) : UComponents<EtsType, TsSizeSort> {
2626
private val closeableResources = mutableListOf<AutoCloseable>()
2727

2828
override val useSolverForForks: Boolean
2929
get() = options.useSolverForForks
3030

31-
override fun <Context : UContext<TSSizeSort>> buildTranslatorAndLazyDecoder(
31+
override fun <Context : UContext<TsSizeSort>> buildTranslatorAndLazyDecoder(
3232
ctx: Context,
33-
): Pair<UExprTranslator<EtsType, TSSizeSort>, ULazyModelDecoder<EtsType>> {
34-
val translator = TSExprTranslator(ctx)
33+
): Pair<UExprTranslator<EtsType, TsSizeSort>, ULazyModelDecoder<EtsType>> {
34+
val translator = TsExprTranslator(ctx)
3535
val decoder = ULazyModelDecoder(translator)
3636

3737
return translator to decoder
3838
}
3939

40-
override fun <Context : UContext<TSSizeSort>> mkSizeExprProvider(ctx: Context): USizeExprProvider<TSSizeSort> {
40+
override fun <Context : UContext<TsSizeSort>> mkSizeExprProvider(ctx: Context): USizeExprProvider<TsSizeSort> {
4141
return UBv32SizeExprProvider(ctx)
4242
}
4343

44-
override fun <Context : UContext<TSSizeSort>> mkComposer(
44+
override fun <Context : UContext<TsSizeSort>> mkComposer(
4545
ctx: Context,
46-
): (UReadOnlyMemory<EtsType>, MutabilityOwnership) -> UComposer<EtsType, TSSizeSort> =
46+
): (UReadOnlyMemory<EtsType>, MutabilityOwnership) -> UComposer<EtsType, TsSizeSort> =
4747
{ memory: UReadOnlyMemory<EtsType>, ownership: MutabilityOwnership ->
48-
TSComposer(ctx, memory, ownership)
48+
TsComposer(ctx, memory, ownership)
4949
}
5050

5151
override fun mkTypeSystem(
52-
ctx: UContext<TSSizeSort>,
52+
ctx: UContext<TsSizeSort>,
5353
): UTypeSystem<EtsType> = typeSystem
5454

55-
override fun <Context : UContext<TSSizeSort>> mkSolver(ctx: Context): USolverBase<EtsType> {
55+
override fun <Context : UContext<TsSizeSort>> mkSolver(ctx: Context): USolverBase<EtsType> {
5656
val (translator, decoder) = buildTranslatorAndLazyDecoder(ctx)
5757

5858
val smtSolver = when (options.solverType) {

usvm-ts/src/main/kotlin/org/usvm/machine/TSContext.kt renamed to usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -17,20 +17,20 @@ import org.usvm.UContext
1717
import org.usvm.UExpr
1818
import org.usvm.USort
1919
import org.usvm.collection.field.UFieldLValue
20-
import org.usvm.machine.expr.TSUndefinedSort
21-
import org.usvm.machine.expr.TSUnresolvedSort
20+
import org.usvm.machine.expr.TsUndefinedSort
21+
import org.usvm.machine.expr.TsUnresolvedSort
2222
import kotlin.contracts.ExperimentalContracts
2323
import kotlin.contracts.contract
2424

25-
typealias TSSizeSort = UBv32Sort
25+
typealias TsSizeSort = UBv32Sort
2626

27-
class TSContext(
27+
class TsContext(
2828
val scene: EtsScene,
29-
components: TSComponents,
30-
) : UContext<TSSizeSort>(components) {
31-
val undefinedSort: TSUndefinedSort by lazy { TSUndefinedSort(this) }
29+
components: TsComponents,
30+
) : UContext<TsSizeSort>(components) {
31+
val undefinedSort: TsUndefinedSort by lazy { TsUndefinedSort(this) }
3232

33-
val unresolvedSort: TSUnresolvedSort = TSUnresolvedSort(this)
33+
val unresolvedSort: TsUnresolvedSort = TsUnresolvedSort(this)
3434

3535
/**
3636
* In TS we treat undefined value as a null reference in other objects.
@@ -65,7 +65,7 @@ class TSContext(
6565

6666
fun mkUndefinedValue(): UExpr<UAddressSort> = undefinedValue
6767

68-
fun mkTSNullValue(): UConcreteHeapRef = nullValue
68+
fun mkTsNullValue(): UConcreteHeapRef = nullValue
6969
private val nullValue: UConcreteHeapRef = mkConcreteHeapRef(addressCounter.freshStaticAddress())
7070

7171
fun getIntermediateBoolLValue(addr: Int): UFieldLValue<IntermediateLValueField, UBoolSort> {

usvm-ts/src/main/kotlin/org/usvm/machine/TSMachine.kt renamed to usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -7,10 +7,10 @@ import org.usvm.CoverageZone
77
import org.usvm.StateCollectionStrategy
88
import org.usvm.UMachine
99
import org.usvm.UMachineOptions
10-
import org.usvm.api.targets.TSTarget
11-
import org.usvm.machine.interpreter.TSInterpreter
12-
import org.usvm.machine.state.TSMethodResult
13-
import org.usvm.machine.state.TSState
10+
import org.usvm.api.targets.TsTarget
11+
import org.usvm.machine.interpreter.TsInterpreter
12+
import org.usvm.machine.state.TsMethodResult
13+
import org.usvm.machine.state.TsState
1414
import org.usvm.ps.createPathSelector
1515
import org.usvm.statistics.CompositeUMachineObserver
1616
import org.usvm.statistics.CoverageStatistics
@@ -25,22 +25,22 @@ import org.usvm.statistics.distances.PlainCallGraphStatistics
2525
import org.usvm.stopstrategies.createStopStrategy
2626
import kotlin.time.Duration.Companion.seconds
2727

28-
class TSMachine(
28+
class TsMachine(
2929
private val project: EtsScene,
3030
private val options: UMachineOptions,
31-
) : UMachine<TSState>() {
32-
private val typeSystem = TSTypeSystem(typeOperationsTimeout = 1.seconds, project)
33-
private val components = TSComponents(typeSystem, options)
34-
private val ctx = TSContext(project, components)
35-
private val applicationGraph = TSApplicationGraph(project)
36-
private val interpreter = TSInterpreter(ctx, applicationGraph)
31+
) : UMachine<TsState>() {
32+
private val typeSystem = TsTypeSystem(typeOperationsTimeout = 1.seconds, project)
33+
private val components = TsComponents(typeSystem, options)
34+
private val ctx = TsContext(project, components)
35+
private val applicationGraph = TsApplicationGraph(project)
36+
private val interpreter = TsInterpreter(ctx, applicationGraph)
3737
private val cfgStatistics = CfgStatisticsImpl(applicationGraph)
3838

3939
fun analyze(
4040
methods: List<EtsMethod>,
41-
targets: List<TSTarget> = emptyList(),
42-
): List<TSState> {
43-
val initialStates = mutableMapOf<EtsMethod, TSState>()
41+
targets: List<TsTarget> = emptyList(),
42+
): List<TsState> {
43+
val initialStates = mutableMapOf<EtsMethod, TsState>()
4444
methods.forEach { initialStates[it] = interpreter.getInitialState(it, targets) }
4545

4646
val methodsToTrackCoverage =
@@ -49,7 +49,7 @@ class TSMachine(
4949
CoverageZone.CLASS -> TODO("Unsupported yet")
5050
}
5151

52-
val coverageStatistics = CoverageStatistics<EtsMethod, EtsStmt, TSState>(
52+
val coverageStatistics = CoverageStatistics<EtsMethod, EtsStmt, TsState>(
5353
methodsToTrackCoverage,
5454
applicationGraph
5555
)
@@ -60,7 +60,7 @@ class TSMachine(
6060
else -> TODO("Unsupported yet")
6161
}
6262

63-
val timeStatistics = TimeStatistics<EtsMethod, TSState>()
63+
val timeStatistics = TimeStatistics<EtsMethod, TsState>()
6464

6565
val pathSelector = createPathSelector(
6666
initialStates,
@@ -74,18 +74,18 @@ class TSMachine(
7474

7575
val statesCollector =
7676
when (options.stateCollectionStrategy) {
77-
StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector<TSState>(coverageStatistics) {
78-
it.methodResult is TSMethodResult.TSException
77+
StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector<TsState>(coverageStatistics) {
78+
it.methodResult is TsMethodResult.TsException
7979
}
8080

8181
StateCollectionStrategy.REACHED_TARGET -> TargetsReachedStatesCollector()
8282
StateCollectionStrategy.ALL -> AllStatesCollector()
8383
}
8484

85-
val observers = mutableListOf<UMachineObserver<TSState>>(coverageStatistics)
85+
val observers = mutableListOf<UMachineObserver<TsState>>(coverageStatistics)
8686
observers.add(statesCollector)
8787

88-
val stepsStatistics = StepsStatistics<EtsMethod, TSState>()
88+
val stepsStatistics = StepsStatistics<EtsMethod, TsState>()
8989

9090
val stopStrategy = createStopStrategy(
9191
options,

usvm-ts/src/main/kotlin/org/usvm/machine/TSTransformer.kt renamed to usvm-ts/src/main/kotlin/org/usvm/machine/TsTransformer.kt

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -8,13 +8,13 @@ import org.usvm.collections.immutable.internal.MutabilityOwnership
88
import org.usvm.memory.UReadOnlyMemory
99
import org.usvm.solver.UExprTranslator
1010

11-
interface TSTransformer : UTransformer<EtsType, TSSizeSort>
11+
interface TsTransformer : UTransformer<EtsType, TsSizeSort>
1212

13-
class TSComposer(
14-
ctx: UContext<TSSizeSort>,
13+
class TsComposer(
14+
ctx: UContext<TsSizeSort>,
1515
memory: UReadOnlyMemory<EtsType>,
1616
ownership: MutabilityOwnership,
17-
) : UComposer<EtsType, TSSizeSort>(ctx, memory, ownership), TSTransformer
17+
) : UComposer<EtsType, TsSizeSort>(ctx, memory, ownership), TsTransformer
1818

19-
class TSExprTranslator(ctx: UContext<TSSizeSort>) : UExprTranslator<EtsType, TSSizeSort>(ctx), TSTransformer
19+
class TsExprTranslator(ctx: UContext<TsSizeSort>) : UExprTranslator<EtsType, TsSizeSort>(ctx), TsTransformer
2020

usvm-ts/src/main/kotlin/org/usvm/machine/TSTypeSystem.kt renamed to usvm-ts/src/main/kotlin/org/usvm/machine/TsTypeSystem.kt

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ import org.usvm.types.emptyTypeStream
1616
import kotlin.time.Duration
1717

1818
// TODO this is draft, should be replaced with real implementation
19-
class TSTypeSystem(
19+
class TsTypeSystem(
2020
override val typeOperationsTimeout: Duration,
2121
val project: EtsScene,
2222
) : UTypeSystem<EtsType> {
@@ -58,17 +58,17 @@ class TSTypeSystem(
5858
else -> emptySequence()
5959
}
6060

61-
private val topTypeStream by lazy { TSTopTypeStream(this) }
61+
private val topTypeStream by lazy { TsTopTypeStream(this) }
6262

6363
override fun topTypeStream(): UTypeStream<EtsType> = topTypeStream
6464
}
6565

66-
class TSTopTypeStream(
67-
private val typeSystem: TSTypeSystem,
68-
private val primitiveTypes: List<EtsType> = TSTypeSystem.primitiveTypes.toList(),
66+
class TsTopTypeStream(
67+
private val typeSystem: TsTypeSystem,
68+
private val primitiveTypes: List<EtsType> = TsTypeSystem.primitiveTypes.toList(),
6969
// Currently only EtsUnknownType was encountered and viewed as any type.
7070
// However, there is EtsAnyType that represents any type.
71-
// TODO: replace EtsUnknownType with further TSTypeSystem implementation.
71+
// TODO: replace EtsUnknownType with further TsTypeSystem implementation.
7272
private val anyTypeStream: UTypeStream<EtsType> = USupportTypeStream.from(typeSystem, EtsUnknownType),
7373
) : UTypeStream<EtsType> {
7474

@@ -88,10 +88,10 @@ class TSTopTypeStream(
8888

8989
if (updatedPrimitiveTypes.isEmpty()) return anyTypeStream
9090

91-
return TSTopTypeStream(typeSystem, updatedPrimitiveTypes, anyTypeStream)
91+
return TsTopTypeStream(typeSystem, updatedPrimitiveTypes, anyTypeStream)
9292
}
9393

94-
return TSTopTypeStream(typeSystem, primitiveTypes, anyTypeStream.filterByNotSupertype(type))
94+
return TsTopTypeStream(typeSystem, primitiveTypes, anyTypeStream.filterByNotSupertype(type))
9595
}
9696

9797
override fun filterByNotSubtype(type: EtsType): UTypeStream<EtsType> {
@@ -100,10 +100,10 @@ class TSTopTypeStream(
100100

101101
if (updatedPrimitiveTypes.isEmpty()) return anyTypeStream
102102

103-
return TSTopTypeStream(typeSystem, updatedPrimitiveTypes, anyTypeStream)
103+
return TsTopTypeStream(typeSystem, updatedPrimitiveTypes, anyTypeStream)
104104
}
105105

106-
return TSTopTypeStream(typeSystem, primitiveTypes, anyTypeStream.filterByNotSubtype(type))
106+
return TsTopTypeStream(typeSystem, primitiveTypes, anyTypeStream.filterByNotSubtype(type))
107107
}
108108

109109
override fun take(n: Int): TypesResult<EtsType> {

0 commit comments

Comments
 (0)