Skip to content

More fixes for real applications #283

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

Draft
wants to merge 16 commits into
base: main
Choose a base branch
from
Draft

More fixes for real applications #283

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
89ed53e
Hacks
CaelmBleidd May 29, 2025
069cb78
More hacks
CaelmBleidd May 29, 2025
f85ef55
Some more fixes
CaelmBleidd May 30, 2025
51f5b9f
Tmp commit
CaelmBleidd May 30, 2025
545887c
Input arrays support
CaelmBleidd Jun 6, 2025
f6c17c4
Format
Lipen Jun 9, 2025
db952f6
Operators implementation
CaelmBleidd Jun 10, 2025
911e8ca
Some hacks
CaelmBleidd Jun 10, 2025
a07c653
Fix a class signature lookup
CaelmBleidd Jun 11, 2025
201e5f4
Support simple casts
CaelmBleidd Jun 11, 2025
f8fd3fa
Clear logs
CaelmBleidd Jun 11, 2025
59393c2
Add todo
CaelmBleidd Jun 11, 2025
0f18a8c
Rebase fix
CaelmBleidd Jun 18, 2025
bb4df1f
Tmp changes
CaelmBleidd Jun 19, 2025
7b1bcd8
Some fixes
CaelmBleidd Jun 20, 2025
c3e5fe0
Fix mocker return value
CaelmBleidd Jun 20, 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
2 changes: 1 addition & 1 deletion buildSrc/src/main/kotlin/Dependencies.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ object Versions {
const val clikt = "5.0.0"
const val detekt = "1.23.7"
const val ini4j = "0.5.4"
const val jacodb = "4ff7243d3a"
const val jacodb = "77b83e4127"
const val juliet = "1.3.2"
const val junit = "5.9.3"
const val kotlin = "2.1.0"
Expand Down
4 changes: 3 additions & 1 deletion usvm-core/src/main/kotlin/org/usvm/StepScope.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,9 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, Type, Statement,
contract {
callsInPlace(block, InvocationKind.EXACTLY_ONCE)
}
check(canProcessFurtherOnCurrentStep) { "Caller should check before processing the current hop further" }
check(canProcessFurtherOnCurrentStep) {
"Caller should check before processing the current hop further"
}
return originalState.block()
}

Expand Down
14 changes: 13 additions & 1 deletion usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,8 @@ import org.jacodb.ets.model.EtsAliasType
import org.jacodb.ets.model.EtsAnyType
import org.jacodb.ets.model.EtsArrayType
import org.jacodb.ets.model.EtsBooleanType
import org.jacodb.ets.model.EtsEnumValueType
import org.jacodb.ets.model.EtsGenericType
import org.jacodb.ets.model.EtsNullType
import org.jacodb.ets.model.EtsNumberType
import org.jacodb.ets.model.EtsRefType
Expand Down Expand Up @@ -73,7 +75,17 @@ class TsContext(
is EtsAnyType -> unresolvedSort
is EtsUnknownType -> unresolvedSort
is EtsAliasType -> typeToSort(type.originalType)
else -> TODO("${type::class.simpleName} is not yet supported: $type")
is EtsGenericType -> {
if (type.constraint == null && type.defaultType == null) {
unresolvedSort
} else {
TODO("Not yet implemented")
}
}
is EtsEnumValueType -> unresolvedSort
else -> {
TODO("${type::class.simpleName} is not yet supported: $type")
}
}

fun arrayDescriptorOf(type: EtsArrayType): EtsType {
Expand Down
35 changes: 26 additions & 9 deletions usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@
import org.usvm.statistics.constraints.SoftConstraintsObserver
import org.usvm.statistics.distances.CfgStatisticsImpl
import org.usvm.statistics.distances.PlainCallGraphStatistics
import org.usvm.stopstrategies.StopStrategy
import org.usvm.stopstrategies.createStopStrategy
import org.usvm.util.humanReadableSignature
import kotlin.time.Duration.Companion.seconds
Expand Down Expand Up @@ -79,7 +80,7 @@
timeStatistics = timeStatistics,
coverageStatisticsFactory = { coverageStatistics },
cfgStatisticsFactory = { cfgStatistics },
callGraphStatisticsFactory = { callGraphStatistics },
callGraphStatisticsFactory = { callGraphStatistics }
)

val statesCollector =
Expand All @@ -101,14 +102,30 @@

val stepsStatistics = StepsStatistics<EtsMethod, TsState>()

val stopStrategy = createStopStrategy(
options,
targets,
timeStatisticsFactory = { timeStatistics },
stepsStatisticsFactory = { stepsStatistics },
coverageStatisticsFactory = { coverageStatistics },
getCollectedStatesCount = { statesCollector.collectedStates.size }
)
val stopStrategy = object : StopStrategy {
val strategy = createStopStrategy(
options,
targets,
timeStatisticsFactory =
{ timeStatistics },

Check warning

Code scanning / detekt

Reports mis-indented code Warning

Unexpected indentation (20) (should be 16)
stepsStatisticsFactory =
{ stepsStatistics },

Check warning

Code scanning / detekt

Reports mis-indented code Warning

Unexpected indentation (20) (should be 16)
coverageStatisticsFactory =
{ coverageStatistics },

Check warning

Code scanning / detekt

Reports mis-indented code Warning

Unexpected indentation (20) (should be 16)
getCollectedStatesCount =
{ statesCollector.collectedStates.size }

Check warning

Code scanning / detekt

Reports mis-indented code Warning

Unexpected indentation (20) (should be 16)
)

override fun shouldStop(): Boolean {
val result = strategy.shouldStop()

if (result) {
logger.warn { "Stop strategy finished execution $strategy" }
}

return result
}
}

observers.add(timeStatistics)
observers.add(stepsStatistics)
Expand Down
Loading
Loading