Skip to content

Commit

Permalink
Reformatted code
Browse files Browse the repository at this point in the history
  • Loading branch information
@thetabotmaintainer
thetabotmaintainer[bot] committed Jan 7, 2024
1 parent 139edf5 commit 6079958
Show file tree
Hide file tree
Showing 13 changed files with 63 additions and 47 deletions.
32 changes: 17 additions & 15 deletions ...mmon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ import hu.bme.mit.theta.solver.ItpSolver
import hu.bme.mit.theta.solver.Solver
import java.util.*

class BoundedChecker<S: ExprState, A: StmtAction>(
class BoundedChecker<S : ExprState, A : StmtAction>(
private val monolithicExpr: MonolithicExpr,
private val shouldGiveUp: (Int) -> Boolean = { false },
private val bmcSolver: Solver? = null,
Expand All @@ -47,38 +47,40 @@ class BoundedChecker<S: ExprState, A: StmtAction>(
private val valToState: (Valuation) -> S,
private val biValToAction: (Valuation, Valuation) -> A,
private val logger: Logger,
): SafetyChecker<S, A, UnitPrec> {
) : SafetyChecker<S, A, UnitPrec> {

private val vars = monolithicExpr.vars()
private val unfoldedInitExpr = PathUtils.unfold(monolithicExpr.initExpr, 0)
private val unfoldedPropExpr = {i: VarIndexing -> PathUtils.unfold(monolithicExpr.propExpr, i)}
private val unfoldedPropExpr = { i: VarIndexing -> PathUtils.unfold(monolithicExpr.propExpr, i) }
private val indices = mutableListOf(VarIndexingFactory.indexing(0))
private val exprs = mutableListOf<Expr<BoolType>>()

init {
check(bmcSolver != itpSolver || bmcSolver == null) {"Use distinct solvers for BMC and IMC!"}
check(bmcSolver != indSolver || bmcSolver == null) {"Use distinct solvers for BMC and KInd!"}
check(itpSolver != indSolver || itpSolver == null) {"Use distinct solvers for IMC and KInd!"}
check(bmcSolver != itpSolver || bmcSolver == null) { "Use distinct solvers for BMC and IMC!" }
check(bmcSolver != indSolver || bmcSolver == null) { "Use distinct solvers for BMC and KInd!" }
check(itpSolver != indSolver || itpSolver == null) { "Use distinct solvers for IMC and KInd!" }
}

override fun check(prec: UnitPrec?): SafetyResult<S, A> {
var iteration = 0;

while(!shouldGiveUp(iteration)) {
while (!shouldGiveUp(iteration)) {
iteration++
logger.write(Logger.Level.MAINSTEP, "Starting iteration $iteration\n")

exprs.add(PathUtils.unfold(monolithicExpr.transExpr, indices.last()))

indices.add(indices.last().add(monolithicExpr.offsetIndex))

if(bmcEnabled(iteration)) {
if (bmcEnabled(iteration)) {
bmc()?.let { return it }
}

if(kindEnabled(iteration)) {
if (kindEnabled(iteration)) {
kind()?.let { return it }
}

if(imcEnabled(iteration)) {
if (imcEnabled(iteration)) {
itp()?.let { return it }
}
}
Expand All @@ -94,7 +96,7 @@ class BoundedChecker<S: ExprState, A: StmtAction>(
bmcSolver.add(exprs)
bmcSolver.add(Not(unfoldedPropExpr(indices.last())))

val ret = if(bmcSolver.check().isSat) {
val ret = if (bmcSolver.check().isSat) {
val trace = getTrace(bmcSolver.model)
logger.write(Logger.Level.MAINSTEP, "CeX found in BMC step (length ${trace.length()})\n")
SafetyResult.unsafe(trace)
Expand All @@ -113,7 +115,7 @@ class BoundedChecker<S: ExprState, A: StmtAction>(
indSolver.add(exprs)
indSolver.add(Not(unfoldedPropExpr(indices.last())))

val ret = if(indSolver.check().isUnsat) {
val ret = if (indSolver.check().isUnsat) {
logger.write(Logger.Level.MAINSTEP, "Safety proven in k-induction step\n")
SafetyResult.safe<S, A>()
} else null
Expand Down Expand Up @@ -141,7 +143,7 @@ class BoundedChecker<S: ExprState, A: StmtAction>(

val status = itpSolver.check()

if(status.isSat) {
if (status.isSat) {
val trace = getTrace(itpSolver.model)
logger.write(Logger.Level.MAINSTEP, "CeX found in IMC/BMC step (length ${trace.length()})\n")
itpSolver.pop()
Expand All @@ -150,7 +152,7 @@ class BoundedChecker<S: ExprState, A: StmtAction>(
}

var img = unfoldedInitExpr
while(itpSolver.check().isUnsat) {
while (itpSolver.check().isUnsat) {
val interpolant = itpSolver.getInterpolant(pattern)
val itpFormula = PathUtils.unfold(PathUtils.foldin(interpolant.eval(a), indices[1]), indices[0])
itpSolver.pop()
Expand All @@ -159,7 +161,7 @@ class BoundedChecker<S: ExprState, A: StmtAction>(
itpSolver.add(a, itpFormula)
itpSolver.add(a, Not(img))
val itpStatus = itpSolver.check()
if(itpStatus.isUnsat) {
if (itpStatus.isUnsat) {
logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC step\n")
itpSolver.pop()
itpSolver.pop()
Expand Down
1 change: 1 addition & 0 deletions ...solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/GraphConstraint.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ package hu.bme.mit.theta.graphsolver.patterns.constraints
import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler

typealias MCM = Collection<GraphConstraint>

sealed interface GraphConstraint {

fun <T> accept(compiler: GraphPatternCompiler<T, *>): T
Expand Down
8 changes: 4 additions & 4 deletions subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ import java.io.File
import java.util.concurrent.TimeUnit
import kotlin.random.Random

fun runConfig(config: XcfaConfig<*,*>, logger: Logger, uniqueLogger: Logger): SafetyResult<*, *> {
fun runConfig(config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger): SafetyResult<*, *> {
propagateInputOptions(config, logger, uniqueLogger)

registerAllSolverManagers(config.backendConfig.solverHome, logger)
Expand All @@ -74,7 +74,7 @@ fun runConfig(config: XcfaConfig<*,*>, logger: Logger, uniqueLogger: Logger): Sa
}


private fun propagateInputOptions(config: XcfaConfig<*,*>, logger: Logger, uniqueLogger: Logger) {
private fun propagateInputOptions(config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger) {
config.inputConfig.property = determineProperty(config, logger)
LbePass.level = config.frontendConfig.lbeLevel
if (config.backendConfig.backend == Backend.CEGAR) {
Expand All @@ -93,7 +93,7 @@ private fun propagateInputOptions(config: XcfaConfig<*,*>, logger: Logger, uniqu
ARGWebDebugger.on = config.debugConfig.argdebug
}

private fun validateInputOptions(config: XcfaConfig<*,*>, logger: Logger, uniqueLogger: Logger) {
private fun validateInputOptions(config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger) {
rule("NoCoiWhenDataRace") {
(config.backendConfig.specConfig as? CegarConfig)?.coi != ConeOfInfluenceMode.NO_COI &&
config.inputConfig.property == ErrorDetection.DATA_RACE
Expand All @@ -102,7 +102,7 @@ private fun validateInputOptions(config: XcfaConfig<*,*>, logger: Logger, unique
}

fun frontend(config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger): Triple<XCFA, MCM, ParseContext> {
if(config.inputConfig.xcfaWCtx != null) {
if (config.inputConfig.xcfaWCtx != null) {
val xcfa = config.inputConfig.xcfaWCtx!!.first
ConeOfInfluence = if (config.inputConfig.xcfaWCtx!!.third.multiThreading) {
XcfaCoiMultiThread(xcfa)
Expand Down
9 changes: 6 additions & 3 deletions .../xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,11 +53,14 @@ fun getBoundedChecker(xcfa: XCFA, mcm: MCM,

return BoundedChecker(
monolithicExpr = getMonolithicExpr(xcfa),
bmcSolver = getSolver(boundedConfig.bmcConfig.bmcSolver, boundedConfig.bmcConfig.validateBMCSolver).createSolver(),
bmcSolver = getSolver(boundedConfig.bmcConfig.bmcSolver,
boundedConfig.bmcConfig.validateBMCSolver).createSolver(),
bmcEnabled = { !boundedConfig.bmcConfig.disable },
itpSolver = getSolver(boundedConfig.itpConfig.itpSolver, boundedConfig.itpConfig.validateItpSolver).createItpSolver(),
itpSolver = getSolver(boundedConfig.itpConfig.itpSolver,
boundedConfig.itpConfig.validateItpSolver).createItpSolver(),
imcEnabled = { !boundedConfig.itpConfig.disable },
indSolver = getSolver(boundedConfig.indConfig.indSolver, boundedConfig.indConfig.validateIndSolver).createSolver(),
indSolver = getSolver(boundedConfig.indConfig.indSolver,
boundedConfig.indConfig.validateIndSolver).createSolver(),
kindEnabled = { !boundedConfig.indConfig.disable },
valToState = { valToState(xcfa, it) },
biValToAction = { val1, val2 -> valToAction(xcfa, val1, val2) },
Expand Down
3 changes: 2 additions & 1 deletion ...ts/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,8 @@ fun getCegarChecker(xcfa: XCFA, mcm: MCM,
}

val abstractionSolverInstance = abstractionSolverFactory.createSolver()
val globalStatePartialOrd: PartialOrd<out ExprState> = cegarConfig.abstractorConfig.domain.partialOrd(abstractionSolverInstance)
val globalStatePartialOrd: PartialOrd<out ExprState> = cegarConfig.abstractorConfig.domain.partialOrd(
abstractionSolverInstance)
val corePartialOrd: PartialOrd<out XcfaState<out ExprState>> =
if (xcfa.isInlined) getPartialOrder(globalStatePartialOrd)
else getStackPartialOrder(globalStatePartialOrd)
Expand Down
4 changes: 2 additions & 2 deletions ...jects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToPortfolio.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,13 +46,13 @@ fun getPortfolioChecker(xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>,
val sw = Stopwatch.createStarted()
val portfolioName = (config.backendConfig.specConfig as PortfolioConfig).portfolio

val portfolioStm = when(portfolioName) {
val portfolioStm = when (portfolioName) {
"COMPLEX",
"COMPLEX24" -> complexPortfolio24(xcfa, mcm, parseContext, config, logger, uniqueLogger)

"COMPLEX23" -> complexPortfolio23(xcfa, mcm, parseContext, config, logger, uniqueLogger)
else -> {
if(File(portfolioName).exists()) {
if (File(portfolioName).exists()) {
val kotlinEngine: ScriptEngine = ScriptEngineManager().getEngineByExtension("kts")
val bindings: Bindings = SimpleBindings()
bindings["xcfa"] = xcfa
Expand Down
25 changes: 16 additions & 9 deletions ...ojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ import java.util.*
import java.util.concurrent.TimeUnit
import kotlin.io.path.createTempDirectory

class InProcessChecker<F: SpecFrontendConfig, B: SpecBackendConfig>(
class InProcessChecker<F : SpecFrontendConfig, B : SpecBackendConfig>(
val xcfa: XCFA,
val config: XcfaConfig<F, B>,
val parseContext: ParseContext,
Expand All @@ -55,7 +55,9 @@ class InProcessChecker<F: SpecFrontendConfig, B: SpecBackendConfig>(
val tempDir = createTempDirectory(config.outputConfig.resultFolder.toPath())

val xcfaJson = CachingFileSerializer.serialize("xcfa.json", xcfa) { getGson(xcfa).toJson(xcfa) }
val parseContextJson = CachingFileSerializer.serialize("parseContext.json", parseContext) { getGson(xcfa).toJson(parseContext) }
val parseContextJson = CachingFileSerializer.serialize("parseContext.json", parseContext) {
getGson(xcfa).toJson(parseContext)
}

val processConfig = config.copy(
inputConfig = config.inputConfig.copy(
Expand All @@ -74,7 +76,9 @@ class InProcessChecker<F: SpecFrontendConfig, B: SpecBackendConfig>(
)
)

val configJson = CachingFileSerializer.serialize("config.json", processConfig) { getGson(xcfa).toJson(processConfig) }
val configJson = CachingFileSerializer.serialize("config.json", processConfig) {
getGson(xcfa).toJson(processConfig)
}

val pb = NuProcessBuilder(listOf(
ProcessHandle.current().info().command().orElse("java"),
Expand All @@ -98,7 +102,8 @@ class InProcessChecker<F: SpecFrontendConfig, B: SpecBackendConfig>(
process.destroy(true)
throw ErrorCodeException(ExitCodes.TIMEOUT.code)
} else {
logger.write(Logger.Level.RESULT,"Config timed out but started writing result, trying to wait an additional 10%...")
logger.write(Logger.Level.RESULT,
"Config timed out but started writing result, trying to wait an additional 10%...")
val retCode = process.waitFor(config.backendConfig.timeoutMs / 10, TimeUnit.MILLISECONDS)
if (retCode != 0) {
throw ErrorCodeException(retCode)
Expand All @@ -120,24 +125,26 @@ class InProcessChecker<F: SpecFrontendConfig, B: SpecBackendConfig>(
return booleanSafetyResult as SafetyResult<XcfaState<*>, XcfaAction>
}

private class ProcessHandler: NuAbstractProcessHandler() {
private class ProcessHandler : NuAbstractProcessHandler() {

private val stdout = LinkedList<String>()
private var stdoutRemainder = ""
private val stderr = LinkedList<String>()
private var stderrRemainder = ""
var safetyResult: SafetyResult<*, *>? = null
private set

override fun onStdout(buffer: ByteBuffer, closed: Boolean) {
if(!closed) {
if (!closed) {
val bytes = ByteArray(buffer.remaining())
buffer[bytes]
val str = bytes.decodeToString()

stdoutRemainder += str
if(stdoutRemainder.contains("SafetyResult Safe")) {
if (stdoutRemainder.contains("SafetyResult Safe")) {
safetyResult = SafetyResult.safe<State, Action>()
}
if(stdoutRemainder.contains("SafetyResult Unsafe")) {
if (stdoutRemainder.contains("SafetyResult Unsafe")) {
safetyResult = SafetyResult.unsafe()
}

Expand All @@ -151,7 +158,7 @@ class InProcessChecker<F: SpecFrontendConfig, B: SpecBackendConfig>(
}

override fun onStderr(buffer: ByteBuffer, closed: Boolean) {
if(!closed) {
if (!closed) {
val bytes = ByteArray(buffer.remaining())
buffer[bytes]
val str = bytes.decodeToString()
Expand Down
8 changes: 4 additions & 4 deletions subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/TypeAdapters.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ import com.google.gson.stream.JsonToken
import com.google.gson.stream.JsonWriter
import hu.bme.mit.theta.xcfa.passes.LbePass

class SpecFrontendConfigTypeAdapter(val gsonSupplier: () -> Gson): TypeAdapter<FrontendConfig<*>>() {
class SpecFrontendConfigTypeAdapter(val gsonSupplier: () -> Gson) : TypeAdapter<FrontendConfig<*>>() {

private lateinit var gson: Gson

Expand All @@ -35,7 +35,7 @@ class SpecFrontendConfigTypeAdapter(val gsonSupplier: () -> Gson): TypeAdapter<F
writer.name("loopUnroll").value(value.loopUnroll)
writer.name("inputType").value(value.inputType.name)
writer.name("specConfig")
if(value.specConfig != null) {
if (value.specConfig != null) {
writer.beginObject()
writer.name("type").value(value.specConfig?.javaClass?.typeName)
writer.name("value")
Expand Down Expand Up @@ -92,7 +92,7 @@ class SpecFrontendConfigTypeAdapter(val gsonSupplier: () -> Gson): TypeAdapter<F
}
}

class SpecBackendConfigTypeAdapter(val gsonSupplier: () -> Gson): TypeAdapter<BackendConfig<*>>() {
class SpecBackendConfigTypeAdapter(val gsonSupplier: () -> Gson) : TypeAdapter<BackendConfig<*>>() {

private lateinit var gson: Gson

Expand All @@ -105,7 +105,7 @@ class SpecBackendConfigTypeAdapter(val gsonSupplier: () -> Gson): TypeAdapter<Ba
writer.name("timeoutMs").value(value.timeoutMs)
writer.name("inProcess").value(value.inProcess)
writer.name("specConfig")
if(value.specConfig != null) {
if (value.specConfig != null) {
writer.beginObject()
writer.name("type").value(value.specConfig?.javaClass?.typeName)
writer.name("value")
Expand Down
4 changes: 2 additions & 2 deletions subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/Validators.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,8 +18,8 @@ package hu.bme.mit.theta.xcfa.cli.params

import com.beust.jcommander.ParameterException

fun rule(name: String, test: ()->Boolean) {
if(test()) {
fun rule(name: String, test: () -> Boolean) {
if (test()) {
throw ParameterException("Validation failed for rule $name")
}
}
9 changes: 5 additions & 4 deletions subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ interface SpecializableConfig<T : Config> : Config {
override fun update(): Boolean = specConfig?.update() ?: createSpecConfig().let { specConfig != null }
}

data class XcfaConfig<F: SpecFrontendConfig, B: SpecBackendConfig>(
data class XcfaConfig<F : SpecFrontendConfig, B : SpecBackendConfig>(
val inputConfig: InputConfig = InputConfig(),
val frontendConfig: FrontendConfig<F> = FrontendConfig(),
val backendConfig: BackendConfig<B> = BackendConfig(),
Expand Down Expand Up @@ -77,15 +77,16 @@ data class InputConfig(
description = "XCFA and ParseContext (will overwrite --input and --parse-ctx when given)")
var xcfaWCtx: Triple<XCFA, MCM, ParseContext>? = null,

@Parameter(names = ["--property-file"], description = "Path of the property file (will overwrite --property when given)")
@Parameter(names = ["--property-file"],
description = "Path of the property file (will overwrite --property when given)")
var propertyFile: File? = null,

@Parameter(names = ["--property"], description = "Property")
var property: ErrorDetection = ErrorDetection.ERROR_LOCATION
) : Config

interface SpecFrontendConfig : Config
data class FrontendConfig<T: SpecFrontendConfig>(
data class FrontendConfig<T : SpecFrontendConfig>(
@Parameter(names = ["--lbe"], description = "Level of LBE (NO_LBE, LBE_LOCAL, LBE_SEQ, LBE_FULL)")
var lbeLevel: LbePass.LbeLevel = LbePass.LbeLevel.LBE_SEQ,

Expand Down Expand Up @@ -122,7 +123,7 @@ data class CHCFrontendConfig(

interface SpecBackendConfig : Config

data class BackendConfig<T: SpecBackendConfig>(
data class BackendConfig<T : SpecBackendConfig>(
@Parameter(names = ["--backend"], description = "Backend analysis to use")
var backend: Backend = Backend.CEGAR,

Expand Down
3 changes: 2 additions & 1 deletion ...ects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/CachingFileSerializer.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ package hu.bme.mit.theta.xcfa.cli.utils
import java.io.File

object CachingFileSerializer {

private val cache: MutableMap<Pair<String, Any>, File> = LinkedHashMap()

/**
Expand All @@ -27,7 +28,7 @@ object CachingFileSerializer {
* func: generator function if a cache miss occurs
*/
fun serialize(key: String, obj: Any, func: (Any) -> String): File =
if(cache.containsKey(Pair(key, obj))) {
if (cache.containsKey(Pair(key, obj))) {
cache[Pair(key, obj)]!!
} else {
val str = func(obj)
Expand Down
2 changes: 1 addition & 1 deletion subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/PropertyUtils.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ import hu.bme.mit.theta.common.logging.Logger
import hu.bme.mit.theta.xcfa.analysis.ErrorDetection
import hu.bme.mit.theta.xcfa.cli.params.XcfaConfig

fun determineProperty(config: XcfaConfig<*,*>, logger: Logger): ErrorDetection = config.inputConfig.propertyFile?.run {
fun determineProperty(config: XcfaConfig<*, *>, logger: Logger): ErrorDetection = config.inputConfig.propertyFile?.run {
val propertyFile = config.inputConfig.propertyFile!!
when {
propertyFile.name.endsWith("unreach-call.prp") -> {
Expand Down
2 changes: 1 addition & 1 deletion subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ import javax.script.ScriptEngineManager
import kotlin.system.exitProcess


fun getXcfa(config: XcfaConfig<*,*>, parseContext: ParseContext, logger: Logger, uniqueWarningLogger: Logger) =
fun getXcfa(config: XcfaConfig<*, *>, parseContext: ParseContext, logger: Logger, uniqueWarningLogger: Logger) =
try {
when (config.frontendConfig.inputType) {
InputType.CHC -> {
Expand Down

0 comments on commit 6079958

Please sign in to comment.