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 Nov 2, 2023
1 parent ec09bd5 commit b40cc00
Show file tree
Hide file tree
Showing 8 changed files with 97 additions and 71 deletions.
34 changes: 18 additions & 16 deletions ...n/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -388,41 +388,43 @@ 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
*/
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
*/
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
)
);
}

Expand Down
3 changes: 2 additions & 1 deletion ...ects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<Decl<out Type>, MutableSet<ExprState>>) :
open class XcfaAasporLts(xcfa: XCFA,
private val ignoredVarRegistry: MutableMap<Decl<out Type>, MutableSet<ExprState>>) :
XcfaSporLts(xcfa) {

override fun <P : Prec> getEnabledActionsFor(state: XcfaState<*>, exploredActions: Collection<XcfaAction>,
Expand Down
4 changes: 3 additions & 1 deletion subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down Expand Up @@ -333,12 +333,14 @@ enum class ConeOfInfluenceMode(
XcfaAasporCoiLts(xcfa, ivr, ConeOfInfluence.lts)
})
;

var porLts: LTS<XcfaState<out ExprState>, XcfaAction>? = null
}

// TODO CexMonitor: disable for multi_seq
// TODO add new monitor to xsts cli
enum class CexMonitorOptions {

CHECK,
DISABLE
}
2 changes: 1 addition & 1 deletion subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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")
Expand Down
3 changes: 2 additions & 1 deletion subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -160,7 +160,8 @@ class XcfaCli(private val args: Array<String>) {
@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
Expand Down
10 changes: 6 additions & 4 deletions subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaToCTest.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
}

Expand Down
108 changes: 62 additions & 46 deletions subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/XcfaToC.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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()

Expand All @@ -156,18 +159,18 @@ fun XcfaProcedure.decl(parseContext: ParseContext): String =
}

private fun VarDecl<*>.unsafeBounds(parseContext: ParseContext) =
CComplexType.getType(ref, parseContext).accept(object: CComplexTypeVisitor<Unit, Expr<BoolType>?>() {
CComplexType.getType(ref, parseContext).accept(object : CComplexTypeVisitor<Unit, Expr<BoolType>?>() {
override fun visit(type: CInteger, param: Unit): Expr<BoolType>? {
return Or(Leq(ref, Int(-1_000_000_000)), Geq(ref, Int(1_000_000_000)))
}

override fun visit(type: CBool?, param: Unit?): Expr<BoolType>? {
return null
}
}, Unit)
override fun visit(type: CBool?, param: Unit?): Expr<BoolType>? {
return null
}
}, Unit)

private fun Set<VarDecl<*>>.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())
Expand All @@ -179,7 +182,7 @@ private fun Set<VarDecl<*>>.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) + ";" }}
Expand All @@ -189,21 +192,22 @@ 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 ""}
}
""".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()};"
Expand All @@ -213,23 +217,27 @@ 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()

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();
Expand All @@ -238,31 +246,37 @@ 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")
}

fun Pair<VarDecl<*>, 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"
Expand All @@ -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)
Expand All @@ -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()
Expand All @@ -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)})"
}
Expand All @@ -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 -> "||"
Expand All @@ -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")
Expand Down
4 changes: 3 additions & 1 deletion subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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))
) {
Expand Down

0 comments on commit b40cc00

Please sign in to comment.