From b40cc00225a173a085a06625cc2280b45523f07c Mon Sep 17 00:00:00 2001 From: "ThetaBotMaintainer[bot]" <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> Date: Thu, 2 Nov 2023 12:33:38 +0000 Subject: [PATCH] Reformatted code --- .../grammar/expression/ExpressionVisitor.java | 34 +++--- .../theta/xcfa/analysis/por/XcfaAasporLts.kt | 3 +- .../bme/mit/theta/xcfa/cli/ConfigOptions.kt | 4 +- .../bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt | 2 +- .../java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt | 3 +- .../hu/bme/mit/theta/xcfa/cli/XcfaToCTest.kt | 10 +- .../java/hu/bme/mit/theta/xcfa/XcfaToC.kt | 108 ++++++++++-------- .../hu/bme/mit/theta/xcfa/passes/LbePass.kt | 4 +- 8 files changed, 97 insertions(+), 71 deletions(-) diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java index e6a214ef61..4fcd245c6a 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java @@ -388,6 +388,7 @@ public Expr visitMultiplicativeExpression(CParser.MultiplicativeExpressionCon /** * Conversion from C (/) semantics to solver (div) semantics. + * * @param a dividend * @param b divisor * @return expression representing C division semantics with solver operations @@ -395,21 +396,22 @@ public Expr visitMultiplicativeExpression(CParser.MultiplicativeExpressionCon private Expr createIntDiv(Expr a, Expr b) { DivExpr aDivB = Div(a, b); return Ite(Geq(a, Int(0)), // if (a >= 0) - aDivB, // a div b - // else - Ite(Neq(Mod(a, b), Int(0)), // if (a mod b != 0) - Ite(Geq(b, Int(0)), // if (b >= 0) - Add(aDivB, Int(1)), // a div b + 1 - // else - Sub(aDivB, Int(1)) // a div b - 1 - ), // else - aDivB // a div b - ) + aDivB, // a div b + // else + Ite(Neq(Mod(a, b), Int(0)), // if (a mod b != 0) + Ite(Geq(b, Int(0)), // if (b >= 0) + Add(aDivB, Int(1)), // a div b + 1 + // else + Sub(aDivB, Int(1)) // a div b - 1 + ), // else + aDivB // a div b + ) ); } /** * Conversion from C (%) semantics to solver (mod) semantics. + * * @param a dividend * @param b divisor * @return expression representing C modulo semantics with solver operations @@ -417,12 +419,12 @@ private Expr createIntDiv(Expr a, Expr b) { private Expr createIntMod(Expr a, Expr b) { ModExpr aModB = Mod(a, b); return Ite(Geq(a, Int(0)), // if (a >= 0) - aModB, // a mod b - // else - Ite(Geq(b, Int(0)), // if (b >= 0) - Sub(aModB, b), // a mod b - b - Add(aModB, b) // a mod b + b - ) + aModB, // a mod b + // else + Ite(Geq(b, Int(0)), // if (b >= 0) + Sub(aModB, b), // a mod b - b + Add(aModB, b) // a mod b + b + ) ); } diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt index ee5bcc5e21..893f902b55 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt @@ -23,7 +23,8 @@ import hu.bme.mit.theta.xcfa.analysis.XcfaAction import hu.bme.mit.theta.xcfa.analysis.XcfaState import hu.bme.mit.theta.xcfa.model.XCFA -open class XcfaAasporLts(xcfa: XCFA, private val ignoredVarRegistry: MutableMap, MutableSet>) : +open class XcfaAasporLts(xcfa: XCFA, + private val ignoredVarRegistry: MutableMap, MutableSet>) : XcfaSporLts(xcfa) { override fun

getEnabledActionsFor(state: XcfaState<*>, exploredActions: Collection, diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt index 5dda459fa4..e015dca75e 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt @@ -181,7 +181,7 @@ enum class Refinement( ), MULTI_SEQ( refiner = { s, m -> - if(m == CexMonitorOptions.CHECK) error("CexMonitor is not implemented for MULTI_SEQ") + if (m == CexMonitorOptions.CHECK) error("CexMonitor is not implemented for MULTI_SEQ") ExprTraceSeqItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver()) }, stopCriterion = StopCriterions.fullExploration() @@ -333,12 +333,14 @@ enum class ConeOfInfluenceMode( XcfaAasporCoiLts(xcfa, ivr, ConeOfInfluence.lts) }) ; + var porLts: LTS, XcfaAction>? = null } // TODO CexMonitor: disable for multi_seq // TODO add new monitor to xsts cli enum class CexMonitorOptions { + CHECK, DISABLE } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt index 13b080036f..04f274e821 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt @@ -92,7 +92,7 @@ data class XcfaCegarConfig( var pruneStrategy: PruneStrategy = PruneStrategy.LAZY, @Parameter(names = ["--cex-monitor"], description = "Warning: With some configurations (e.g. lazy pruning) it is POSSIBLE (but rare) that analysis is stopped, " + - "even though it could still progress. If in doubt, disable this monitor and check results.") + "even though it could still progress. If in doubt, disable this monitor and check results.") var cexMonitor: CexMonitorOptions = CexMonitorOptions.DISABLE, @Parameter(names = ["--timeout-ms"], description = "Timeout for verification (only valid with --strategy SERVER), use 0 for no timeout") diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt index 01585f3605..5ef76b82ea 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt @@ -160,7 +160,8 @@ class XcfaCli(private val args: Array) { @Parameter(names = ["--seed"], description = "Random seed used for DPOR") var randomSeed: Int = -1 - @Parameter(names = ["--arg-to-file"], description = "Visualize the resulting file here: https://ftsrg-edu.github.io/student-sisak-argviz/") + @Parameter(names = ["--arg-to-file"], + description = "Visualize the resulting file here: https://ftsrg-edu.github.io/student-sisak-argviz/") var argToFile: Boolean = false @Parameter diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaToCTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaToCTest.kt index 47518b1742..7eb9c2b6d6 100644 --- a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaToCTest.kt +++ b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaToCTest.kt @@ -49,16 +49,18 @@ class XcfaToCTest { } } - @ParameterizedTest @MethodSource("chcFiles") fun testRoundTrip(filePath: String, chcTransformation: ChcTransformation) { val chcFrontend = ChcFrontend(chcTransformation) - val xcfa = chcFrontend.buildXcfa(CharStreams.fromStream(FileInputStream(javaClass.getResource(filePath)!!.path)), ChcPasses( + val xcfa = chcFrontend.buildXcfa( + CharStreams.fromStream(FileInputStream(javaClass.getResource(filePath)!!.path)), ChcPasses( ParseContext())).build() val temp = createTempDirectory() - val file = temp.resolve("${filePath.split("/").last()}.c").also { it.toFile().writeText(xcfa.toC(ParseContext(), - useArr, useExArr, useRange))} + val file = temp.resolve("${filePath.split("/").last()}.c").also { + it.toFile().writeText(xcfa.toC(ParseContext(), + useArr, useExArr, useRange)) + } System.err.println(file) } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/XcfaToC.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/XcfaToC.kt index 610e7978c0..a36d92a35b 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/XcfaToC.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/XcfaToC.kt @@ -55,13 +55,15 @@ import hu.bme.mit.theta.xcfa.model.* private const val arraySize = 10; -fun XCFA.toC(parseContext: ParseContext, arraySupport: Boolean, exactArraySupport: Boolean, intRangeConstraint: Boolean): String = """ +fun XCFA.toC(parseContext: ParseContext, arraySupport: Boolean, exactArraySupport: Boolean, + intRangeConstraint: Boolean): String = """ extern void abort(); extern int __VERIFIER_nondet_int(); extern _Bool __VERIFIER_nondet__Bool(); extern void reach_error(); - ${if(procedures.any { it.vars.any { it.type is ArrayType<*, *> } } ) if(arraySupport) if(exactArraySupport) """ + ${ + if (procedures.any { it.vars.any { it.type is ArrayType<*, *> } }) if (arraySupport) if (exactArraySupport) """ // "exact" array support typedef long unsigned int size_t; @@ -127,21 +129,22 @@ fun XCFA.toC(parseContext: ParseContext, arraySupport: Boolean, exactArraySuppor } return 1; } - """.trimIndent() else error("Array support not enabled") else ""} + """.trimIndent() else error("Array support not enabled") else "" +} ${procedures.joinToString("\n\n") { it.decl(parseContext) + ";" }} ${procedures.joinToString("\n\n") { it.def(parseContext, intRangeConstraint) }} - ${ if(initProcedures.size != 1) error("Exactly one initial procedure is supported.") else - { - val proc = initProcedures[0] - val procName = proc.first.name.toC() - if (procName != "main") - "int main() { $procName(${proc.second.joinToString(", ") { it.toC(parseContext) } }); }" - else "" - } + ${ + if (initProcedures.size != 1) error("Exactly one initial procedure is supported.") else { + val proc = initProcedures[0] + val procName = proc.first.name.toC() + if (procName != "main") + "int main() { $procName(${proc.second.joinToString(", ") { it.toC(parseContext) }}); }" + else "" } +} """.trimIndent() @@ -156,18 +159,18 @@ fun XcfaProcedure.decl(parseContext: ParseContext): String = } private fun VarDecl<*>.unsafeBounds(parseContext: ParseContext) = - CComplexType.getType(ref, parseContext).accept(object: CComplexTypeVisitor?>() { + CComplexType.getType(ref, parseContext).accept(object : CComplexTypeVisitor?>() { override fun visit(type: CInteger, param: Unit): Expr? { return Or(Leq(ref, Int(-1_000_000_000)), Geq(ref, Int(1_000_000_000))) } - override fun visit(type: CBool?, param: Unit?): Expr? { - return null - } - }, Unit) + override fun visit(type: CBool?, param: Unit?): Expr? { + return null + } + }, Unit) private fun Set>.unsafeBounds(parseContext: ParseContext, intRangeConstraint: Boolean): String { - if(!intRangeConstraint) return "" + if (!intRangeConstraint) return "" val conditions = this.map { (it.unsafeBounds(parseContext))?.toC(parseContext) }.filterNotNull() return if (conditions.isNotEmpty()) @@ -179,7 +182,7 @@ private fun Set>.unsafeBounds(parseContext: ParseContext, intRangeCon fun XcfaProcedure.def(parseContext: ParseContext, intRangeConstraint: Boolean): String = """ ${decl(parseContext)} { // return parameter - ${if(params.isNotEmpty()) params[0].decl(parseContext) + ";" else ""} + ${if (params.isNotEmpty()) params[0].decl(parseContext) + ";" else ""} // variables ${(vars - params.map { it.first }.toSet()).joinToString("\n") { it.decl(parseContext) + ";" }} @@ -189,13 +192,14 @@ fun XcfaProcedure.def(parseContext: ParseContext, intRangeConstraint: Boolean): // main logic goto ${initLoc.name.toC()}; - ${locs.joinToString("\n") { - """ + ${ + locs.joinToString("\n") { + """ ${it.name.toC()}: ${it.toC(parseContext, intRangeConstraint)} """.trimIndent() - } - } + } +} // return expression ${if (params.isNotEmpty()) "return " + params[0].first.name.toC() + ";" else ""} @@ -203,7 +207,7 @@ fun XcfaProcedure.def(parseContext: ParseContext, intRangeConstraint: Boolean): """.trimIndent() private fun XcfaLocation.toC(parseContext: ParseContext, intRangeConstraint: Boolean): String = - if(this.error) { + if (this.error) { "reach_error();" } else when (outgoingEdges.size) { 0 -> "goto ${name.toC()};" @@ -213,12 +217,14 @@ private fun XcfaLocation.toC(parseContext: ParseContext, intRangeConstraint: Boo 2 -> """ switch(__VERIFIER_nondet__Bool()) { - ${outgoingEdges.mapIndexed { index, xcfaEdge -> - "case $index: \n" + - xcfaEdge.getFlatLabels().joinToString("\n", postfix="\n") { it.toC(parseContext, intRangeConstraint) } + + ${ + outgoingEdges.mapIndexed { index, xcfaEdge -> + "case $index: \n" + + xcfaEdge.getFlatLabels() + .joinToString("\n", postfix = "\n") { it.toC(parseContext, intRangeConstraint) } + "goto ${xcfaEdge.target.name.toC()};\n" - }.joinToString("\n") - } + }.joinToString("\n") + } default: abort(); } """.trimIndent() @@ -226,10 +232,12 @@ private fun XcfaLocation.toC(parseContext: ParseContext, intRangeConstraint: Boo else -> """ switch(__VERIFIER_nondet_int()) { - ${outgoingEdges.mapIndexed { index, xcfaEdge -> - "case $index: \n" + - xcfaEdge.getFlatLabels().joinToString("\n", postfix="\n") { it.toC(parseContext, intRangeConstraint) } + - "goto ${xcfaEdge.target.name.toC()};\n" + ${ + outgoingEdges.mapIndexed { index, xcfaEdge -> + "case $index: \n" + + xcfaEdge.getFlatLabels() + .joinToString("\n", postfix = "\n") { it.toC(parseContext, intRangeConstraint) } + + "goto ${xcfaEdge.target.name.toC()};\n" }.joinToString("\n") } default: abort(); @@ -238,16 +246,22 @@ private fun XcfaLocation.toC(parseContext: ParseContext, intRangeConstraint: Boo } private fun XcfaLabel.toC(parseContext: ParseContext, intRangeConstraint: Boolean): String = - when(this) { + when (this) { is StmtLabel -> this.toC(parseContext, intRangeConstraint) is SequenceLabel -> labels.joinToString("\n") { it.toC(parseContext, intRangeConstraint) } - is InvokeLabel -> "${params[0].toC(parseContext)} = ${name.toC()}(${params.subList(1, params.size).map { it.toC(parseContext) }.joinToString(", ")});" + is InvokeLabel -> "${params[0].toC(parseContext)} = ${name.toC()}(${ + params.subList(1, params.size).map { it.toC(parseContext) }.joinToString(", ") + });" + else -> TODO("Not yet supported: $this") } private fun StmtLabel.toC(parseContext: ParseContext, intRangeConstraint: Boolean): String = - when(stmt) { - is HavocStmt<*> -> "${stmt.varDecl.name.toC()} = __VERIFIER_nondet_${CComplexType.getType(stmt.varDecl.ref, parseContext).toC()}(); ${setOf(stmt.varDecl).unsafeBounds(parseContext, intRangeConstraint)}" + when (stmt) { + is HavocStmt<*> -> "${stmt.varDecl.name.toC()} = __VERIFIER_nondet_${ + CComplexType.getType(stmt.varDecl.ref, parseContext).toC() + }(); ${setOf(stmt.varDecl).unsafeBounds(parseContext, intRangeConstraint)}" + is AssignStmt<*> -> "${stmt.varDecl.name.toC()} = ${stmt.expr.toC(parseContext)};" is AssumeStmt -> "if(!${stmt.cond.toC(parseContext)}) abort();" else -> TODO("Not yet supported: $stmt") @@ -255,14 +269,14 @@ private fun StmtLabel.toC(parseContext: ParseContext, intRangeConstraint: Boolea fun Pair, ParamDirection>.decl(parseContext: ParseContext): String = // if(second == ParamDirection.IN) { - first.decl(parseContext) + first.decl(parseContext) // } else error("Only IN params are supported right now") fun VarDecl<*>.decl(parseContext: ParseContext): String = "${CComplexType.getType(ref, parseContext).toC()} ${name.toC()}" private fun CComplexType.toC(): String = - when(this) { + when (this) { is CArray -> "${this.embeddedType.toC()}_arr" is CSignedInt -> "int" is CUnsignedInt -> "unsigned int" @@ -273,7 +287,7 @@ private fun CComplexType.toC(): String = // below functions implement the serialization of expressions to C-style expressions fun Expr<*>.toC(parseContext: ParseContext) = - when(this) { + when (this) { is NullaryExpr<*> -> this.toC(parseContext) is UnaryExpr<*, *> -> this.toC(parseContext) is BinaryExpr<*, *> -> this.toC(parseContext) @@ -295,14 +309,14 @@ fun IteExpr<*>.toC(parseContext: ParseContext): String = // nullary: ref + lit fun NullaryExpr<*>.toC(parseContext: ParseContext): String = - when(this) { + when (this) { is RefExpr<*> -> this.decl.name.toC() is LitExpr<*> -> (this as LitExpr<*>).toC(parseContext) else -> TODO("Not yet supported: $this") } fun LitExpr<*>.toC(parseContext: ParseContext): String = - when(this) { + when (this) { is FalseExpr -> "0" is TrueExpr -> "1" is IntLitExpr -> this.value.toString() @@ -317,10 +331,12 @@ fun UnaryExpr<*, *>.toC(parseContext: ParseContext): String = "(${this.cOperator()} ${op.toC(parseContext)})" fun BinaryExpr<*, *>.toC(parseContext: ParseContext): String = - if(leftOp.type is ArrayType<*, *>) { + if (leftOp.type is ArrayType<*, *>) { "${this.arrayCOperator()}(${leftOp.toC(parseContext)}, ${rightOp.toC(parseContext)})" - } else if(this is ModExpr<*>) { - "( (${leftOp.toC(parseContext)} % ${rightOp.toC(parseContext)} + ${rightOp.toC(parseContext)}) % ${rightOp.toC(parseContext)} )" + } else if (this is ModExpr<*>) { + "( (${leftOp.toC(parseContext)} % ${rightOp.toC(parseContext)} + ${rightOp.toC(parseContext)}) % ${ + rightOp.toC(parseContext) + } )" } else { "(${leftOp.toC(parseContext)} ${this.cOperator()} ${rightOp.toC(parseContext)})" } @@ -329,7 +345,7 @@ fun MultiaryExpr<*, *>.toC(parseContext: ParseContext): String = ops.joinToString(separator = " ${this.cOperator()} ", prefix = "(", postfix = ")") { it.toC(parseContext) } fun Expr<*>.cOperator() = - when(this) { + when (this) { is EqExpr<*> -> "==" is NeqExpr<*> -> "!=" is OrExpr -> "||" @@ -345,7 +361,7 @@ fun Expr<*>.cOperator() = } fun Expr<*>.arrayCOperator() = - when(this) { + when (this) { is EqExpr<*> -> "array_equals" is NeqExpr<*> -> "!array_equals" else -> TODO("Not yet implemented array operator label for expr: $this") diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt index 4889fc3a18..677094835e 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt @@ -278,7 +278,9 @@ class LbePass(val parseContext: ParseContext) : ProcedurePass { if (location.outgoingEdges.size != 1) return false val outEdge = location.outgoingEdges.first() if ( - location.incomingEdges.any { edge -> edge.getFlatLabels().any { it is InvokeLabel || (it is StmtLabel && it.stmt is AssumeStmt) } } + location.incomingEdges.any { edge -> + edge.getFlatLabels().any { it is InvokeLabel || (it is StmtLabel && it.stmt is AssumeStmt) } + } || location.outgoingEdges.any { edge -> edge.getFlatLabels().any { it is InvokeLabel } } || (level == LbeLevel.LBE_LOCAL && !atomicPhase && isNotLocal(outEdge)) ) {