, ThreeVL>
+) {
}
\ No newline at end of file
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/ItpRefToPtrPrec.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/ItpRefToPtrPrec.kt
index c3ec804041..6b17827bf2 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/ItpRefToPtrPrec.kt
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/ItpRefToPtrPrec.kt
@@ -30,8 +30,10 @@ class ItpRefToPtrPrec(private val innerRefToPrec: RefutationToPrec {
val newDerefs = refutation[index].dereferences
val innerPrec = innerRefToPrec.toPrec(refutation, index).repatch()
- return PtrPrec(innerPrec, newDerefs.flatMap { it.ops }.toSet(),
- if (newDerefs.isEmpty()) 0 else refutation.size() - index)
+ return PtrPrec(
+ innerPrec, newDerefs.flatMap { it.ops }.toSet(),
+ if (newDerefs.isEmpty()) 0 else refutation.size() - index
+ )
}
override fun join(prec1: PtrPrec, prec2: PtrPrec
): PtrPrec
{
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrAction.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrAction.kt
index 015084a889..4dee747bb0 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrAction.kt
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrAction.kt
@@ -61,19 +61,30 @@ abstract class PtrAction(writeTriples: WriteTriples = emptyMap(), val inCnt: Int
val postList = ArrayList()
for ((deref, type) in stmt.dereferencesWithAccessTypes) {
- Preconditions.checkState(deref.uniquenessIdx.isPresent,
- "Incomplete dereferences (missing uniquenessIdx) are not handled properly.")
+ Preconditions.checkState(
+ deref.uniquenessIdx.isPresent,
+ "Incomplete dereferences (missing uniquenessIdx) are not handled properly."
+ )
val expr = deref.getIte(nextWriteTriples)
if (type == AccessType.WRITE) {
val writeExpr = ExprUtils.simplify(IntExprs.Add(expr, IntExprs.Int(1)))
nextWriteTriples.getOrPut(deref.type) { ArrayList() }
.add(Triple(lookup[deref]!!.first, lookup[deref]!!.second, deref.uniquenessIdx.get()))
- postList.add(Stmts.Assume(ExprUtils.simplify(BoolExprs.And(listOf(
- AbstractExprs.Eq(writeExpr, deref.uniquenessIdx.get()),
- )))))
+ postList.add(
+ Stmts.Assume(
+ ExprUtils.simplify(
+ BoolExprs.And(
+ listOf(
+ AbstractExprs.Eq(writeExpr, deref.uniquenessIdx.get()),
+ )
+ )
+ )
+ )
+ )
} else {
preList.add(
- Stmts.Assume(ExprUtils.simplify(AbstractExprs.Eq(expr, deref.uniquenessIdx.get()))))
+ Stmts.Assume(ExprUtils.simplify(AbstractExprs.Eq(expr, deref.uniquenessIdx.get())))
+ )
}
// postList.add(Stmts.Assume(Eq(vargen("value", deref.type).ref, deref))) // debug mode
}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrAnalysis.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrAnalysis.kt
index 4eb29ec625..881fecb5bb 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrAnalysis.kt
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrAnalysis.kt
@@ -35,16 +35,20 @@ import hu.bme.mit.theta.core.stmt.Stmt
*
*/
-class PtrAnalysis(private val innerAnalysis: Analysis,
- private val isHavoc: Boolean = false) :
+class PtrAnalysis(
+ private val innerAnalysis: Analysis,
+ private val isHavoc: Boolean = false
+) :
Analysis, PtrAction, PtrPrec> {
override fun getPartialOrd(): PartialOrd> = innerAnalysis.partialOrd.getPtrPartialOrd()
override fun getInitFunc(): InitFunc, PtrPrec> = innerAnalysis.initFunc.getPtrInitFunc()
- override fun getTransFunc(): TransFunc, PtrAction, PtrPrec> = innerAnalysis.transFunc.getPtrTransFunc(
- isHavoc)
+ override fun getTransFunc(): TransFunc, PtrAction, PtrPrec> =
+ innerAnalysis.transFunc.getPtrTransFunc(
+ isHavoc
+ )
}
fun PartialOrd.getPtrPartialOrd(): PartialOrd> = PartialOrd { state1, state2 ->
@@ -56,7 +60,8 @@ fun InitFunc.getPtrInitFunc(): InitFunc TransFunc.getPtrTransFunc(
- isHavoc: Boolean = false): TransFunc, PtrAction, PtrPrec> = TransFunc { state, action, prec ->
+ isHavoc: Boolean = false
+): TransFunc, PtrAction, PtrPrec> = TransFunc { state, action, prec ->
val writeTriples = action.nextWriteTriples()
val patchedPrec = prec.innerPrec.patch(writeTriples)
val exprAction: ExprAction = if (isHavoc) {
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrUtils.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrUtils.kt
index 3cc08a0cf1..e051625334 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrUtils.kt
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrUtils.kt
@@ -53,7 +53,8 @@ enum class AccessType {
val Stmt.dereferencesWithAccessTypes: List, AccessType>>
get() = when (this) {
is MemoryAssignStmt<*, *, *> -> expr.dereferences.map { Pair(it, AccessType.READ) } + listOf(
- Pair(deref, AccessType.WRITE)) + deref.ops.flatMap { it.dereferences }.map { Pair(it, AccessType.READ) }
+ Pair(deref, AccessType.WRITE)
+ ) + deref.ops.flatMap { it.dereferences }.map { Pair(it, AccessType.READ) }
is AssignStmt<*> -> expr.dereferences.map { Pair(it, AccessType.READ) }
is AssumeStmt -> cond.dereferences.map { Pair(it, AccessType.READ) }
@@ -83,19 +84,23 @@ fun SequenceStmt.collapse(): Stmt =
this
}
-fun Stmt.uniqueDereferences(vargen: (String, Type) -> VarDecl<*>,
- lookup: MutableMap, Pair, Expr<*>>>): Stmt {
+fun Stmt.uniqueDereferences(
+ vargen: (String, Type) -> VarDecl<*>,
+ lookup: MutableMap, Pair, Expr<*>>>
+): Stmt {
val ret = ArrayList()
val newStmt = when (this) {
is MemoryAssignStmt<*, *, *> -> {
MemoryAssignStmt.create(
deref.uniqueDereferences(vargen, lookup).also { ret.addAll(it.first) }.second as Dereference<*, *, *>,
- expr.uniqueDereferences(vargen, lookup).also { ret.addAll(it.first) }.second)
+ expr.uniqueDereferences(vargen, lookup).also { ret.addAll(it.first) }.second
+ )
}
is AssignStmt<*> -> AssignStmt.of(
TypeUtils.cast(varDecl, varDecl.type),
- TypeUtils.cast(expr.uniqueDereferences(vargen, lookup).also { ret.addAll(it.first) }.second, varDecl.type))
+ TypeUtils.cast(expr.uniqueDereferences(vargen, lookup).also { ret.addAll(it.first) }.second, varDecl.type)
+ )
is AssumeStmt -> AssumeStmt.of(cond.uniqueDereferences(vargen, lookup).also { ret.addAll(it.first) }.second)
is SequenceStmt -> Stmts.SequenceStmt(stmts.map { it.uniqueDereferences(vargen, lookup) })
@@ -109,13 +114,16 @@ fun Stmt.uniqueDereferences(vargen: (String, Type) -> VarDecl<*>,
return SequenceStmt.of(ret + newStmt).collapse()
}
-fun Expr.uniqueDereferences(vargen: (String, Type) -> VarDecl<*>,
- lookup: MutableMap, Pair, Expr<*>>>): Pair, Expr> =
+fun Expr.uniqueDereferences(
+ vargen: (String, Type) -> VarDecl<*>,
+ lookup: MutableMap, Pair, Expr<*>>>
+): Pair, Expr> =
if (this is Dereference<*, *, T>) {
val ret = ArrayList()
Preconditions.checkState(this.uniquenessIdx.isEmpty, "Only non-pretransformed dereferences should be here")
val arrayExpr = ExprUtils.simplify(
- array.uniqueDereferences(vargen, lookup).also { ret.addAll(it.first) }.second)
+ array.uniqueDereferences(vargen, lookup).also { ret.addAll(it.first) }.second
+ )
val arrayLaterRef = if (arrayExpr !is LitExpr<*>) {
val arrayConst = vargen("a", array.type).ref
ret.add(Assume(Eq(arrayConst, arrayExpr)))
@@ -124,7 +132,8 @@ fun Expr.uniqueDereferences(vargen: (String, Type) -> VarDecl<*>,
arrayExpr
}
val offsetExpr = ExprUtils.simplify(
- offset.uniqueDereferences(vargen, lookup).also { ret.addAll(it.first) }.second)
+ offset.uniqueDereferences(vargen, lookup).also { ret.addAll(it.first) }.second
+ )
val offsetLaterRef = if (offsetExpr !is LitExpr<*>) {
val offsetConst = vargen("o", offset.type).ref
ret.add(Assume(Eq(offsetConst, offsetExpr)))
@@ -140,8 +149,10 @@ fun Expr.uniqueDereferences(vargen: (String, Type) -> VarDecl<*>,
Pair(ret, retDeref)
} else {
val ret = ArrayList()
- Pair(ret,
- this.withOps(this.ops.map { it.uniqueDereferences(vargen, lookup).also { ret.addAll(it.first) }.second }))
+ Pair(
+ ret,
+ this.withOps(this.ops.map { it.uniqueDereferences(vargen, lookup).also { ret.addAll(it.first) }.second })
+ )
}
object TopCollection : Set> {
@@ -168,8 +179,11 @@ enum class PtrTracking {
fun Dereference.getIte(writeTriples: WriteTriples): Expr {
val list = writeTriples[type] ?: emptyList()
return list.fold(Int(0) as Expr) { elze, (arr, off, value) ->
- IteExpr.of(BoolExprs.And(
- listOf(Eq(arr, array), Eq(off, offset))), value, elze)
+ IteExpr.of(
+ BoolExprs.And(
+ listOf(Eq(arr, array), Eq(off, offset))
+ ), value, elze
+ )
}
}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/runtimemonitor/CexMonitor.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/runtimemonitor/CexMonitor.kt
index 32c78c9b0e..95069ed1c1 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/runtimemonitor/CexMonitor.kt
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/runtimemonitor/CexMonitor.kt
@@ -39,8 +39,10 @@ class CexMonitor constructor(
fun checkIfNewCexFound(): Boolean {
return if (arg.cexs.anyMatch { cex -> !cexHashStorage.contains(cex) }) {
- logger.write(Logger.Level.VERBOSE,
- "Counterexample hash check: new cex found successfully\n")
+ logger.write(
+ Logger.Level.VERBOSE,
+ "Counterexample hash check: new cex found successfully\n"
+ )
true
} else {
logger.write(Logger.Level.INFO, "Counterexample hash check: NO new cex found\n")
@@ -65,7 +67,8 @@ class CexMonitor constructor(
when (checkpointName) {
"CegarChecker.unsafeARG" -> if (checkIfNewCexFound()) addNewCounterexample() else throwNotSolvable()
else -> throw RuntimeException(
- "Unknown checkpoint name in CexMonitor execution: $checkpointName")
+ "Unknown checkpoint name in CexMonitor execution: $checkpointName"
+ )
}
}
}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/runtimemonitor/MonitorCheckpoint.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/runtimemonitor/MonitorCheckpoint.kt
index 0e1faccd73..7ddfe7adec 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/runtimemonitor/MonitorCheckpoint.kt
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/runtimemonitor/MonitorCheckpoint.kt
@@ -52,7 +52,8 @@ class MonitorCheckpoint internal constructor(private val name: String) {
assert(registeredCheckpoints.contains(checkpointName))
{ "Checkpoint name $checkpointName was not registered (add it in MonitorCheckpoint.kt)" } // see checkpointNames above
registeredCheckpoints[checkpointName]?.registerMonitor(m) ?: error(
- "Checkpoint with name $checkpointName not found.")
+ "Checkpoint with name $checkpointName not found."
+ )
}
fun execute(name: String) {
diff --git a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/MultiInitFunc.kt b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/MultiInitFunc.kt
index 4d7e740082..f3c1ab15ec 100644
--- a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/MultiInitFunc.kt
+++ b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/MultiInitFunc.kt
@@ -22,7 +22,7 @@ import hu.bme.mit.theta.analysis.State
class MultiInitFunc>
-(
+ (
private val createInitialState: (LControl, RControl, DataState) -> MState,
private val dataInitFunc: InitFunc,
private val extractLeftControlPrec: (LPrec) -> LControlPrec,
diff --git a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/MultiPartialOrd.kt b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/MultiPartialOrd.kt
index 68b3c77b27..b48b564c28 100644
--- a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/MultiPartialOrd.kt
+++ b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/MultiPartialOrd.kt
@@ -20,7 +20,7 @@ import hu.bme.mit.theta.analysis.State
class MultiPartialOrd>
-(
+ (
private val leftPartOrd: PartialOrd,
private val leftCombineStates: (LControl, DataState) -> LState,
private val rightPartOrd: PartialOrd,
diff --git a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/MultiTransFunc.kt b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/MultiTransFunc.kt
index ffe72c9757..02021807d9 100644
--- a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/MultiTransFunc.kt
+++ b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/MultiTransFunc.kt
@@ -24,7 +24,7 @@ class MultiTransFunc, MAction : MultiAction>
-(
+ (
private val defineNextSide: (MState) -> MultiSide,
private val createState: (LControl, RControl, DataState, MultiSide) -> MState,
private val leftTransFunc: TransFunc,
diff --git a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/builder/MultiBuilderResult.kt b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/builder/MultiBuilderResult.kt
index eea37fb1ce..d090ac8cb4 100644
--- a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/builder/MultiBuilderResult.kt
+++ b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/builder/MultiBuilderResult.kt
@@ -33,7 +33,7 @@ import hu.bme.mit.theta.analysis.unit.UnitState
* the whole IDE. For this reason, a POJO has to be used instead
*/
private data class MultiBuilderResult, MControlState : MultiState, MAction : MultiAction, MLts : MultiLts>
-(
+ (
val side: MultiAnalysisSide, MultiPrec>,
val lts: MLts
)
diff --git a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/builder/MultiControlInitFunc.kt b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/builder/MultiControlInitFunc.kt
index d094692eac..6aa4f6614a 100644
--- a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/builder/MultiControlInitFunc.kt
+++ b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/builder/MultiControlInitFunc.kt
@@ -28,7 +28,7 @@ import hu.bme.mit.theta.analysis.unit.UnitState
* Serves as a control initial function for a multi analysis if the product is nested and this analysis is going to be a part of a larger product.
*/
internal class MultiControlInitFunc, MPrec : MultiPrec>
-(
+ (
private val leftControlInitFunc: InitFunc,
private val rightControlInitFunc: InitFunc,
private val createState: (lState: LControl, rState: RControl) -> MState
diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt
index c1a49e333e..5156908c26 100644
--- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt
+++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt
@@ -43,7 +43,8 @@ class BoundedTest {
}
private val biValToAction = { valuation: Valuation?, valuation2: Valuation? ->
ExprActionStub(
- emptyList())
+ emptyList()
+ )
}
init {
@@ -76,7 +77,8 @@ class BoundedTest {
indSolver = indSolver,
valToState = valToState,
biValToAction = biValToAction,
- logger = ConsoleLogger(Logger.Level.VERBOSE))
+ logger = ConsoleLogger(Logger.Level.VERBOSE)
+ )
val safetyResult: SafetyResult<*, *> = checker.check()
Assert.assertTrue(safetyResult.isUnsafe())
}
@@ -93,7 +95,8 @@ class BoundedTest {
indSolver = indSolver,
valToState = valToState,
biValToAction = biValToAction,
- logger = ConsoleLogger(Logger.Level.VERBOSE))
+ logger = ConsoleLogger(Logger.Level.VERBOSE)
+ )
val safetyResult: SafetyResult<*, *> = checker.check()
Assert.assertTrue(safetyResult.isSafe())
}
diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/ptr/PtrAnalysisTest.kt b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/ptr/PtrAnalysisTest.kt
index 9379846676..6c2a0a179c 100644
--- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/ptr/PtrAnalysisTest.kt
+++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/ptr/PtrAnalysisTest.kt
@@ -43,31 +43,44 @@ class PtrAnalysisTest {
private val explTop1 = PtrState(ExplState.top(), nextCnt = 1)
private val emptyAction = PtrActionStub(listOf(), emptyMap())
- private val readLiteralOnly = PtrActionStub(listOf(Assume(Eq(Dereference(Int(0), Int(1), Int()), Int(0)))),
- emptyMap())
- private val writeLiteralOnly = PtrActionStub(listOf(MemoryAssign(Dereference(Int(0), Int(1), Int()), Int(0))),
- emptyMap())
+ private val readLiteralOnly = PtrActionStub(
+ listOf(Assume(Eq(Dereference(Int(0), Int(1), Int()), Int(0)))),
+ emptyMap()
+ )
+ private val writeLiteralOnly = PtrActionStub(
+ listOf(MemoryAssign(Dereference(Int(0), Int(1), Int()), Int(0))),
+ emptyMap()
+ )
private val emptyPrec = PtrPrec(ExplPrec.empty(), emptySet())
@JvmStatic
fun testInputs(): Collection {
return listOf(
- Arguments.of(explTop0, emptyAction, emptyPrec,
- listOf(explTop0)),
- Arguments.of(explTop0, readLiteralOnly, emptyPrec,
- listOf(explTop1)),
- Arguments.of(explTop0, writeLiteralOnly, emptyPrec,
+ Arguments.of(
+ explTop0, emptyAction, emptyPrec,
+ listOf(explTop0)
+ ),
+ Arguments.of(
+ explTop0, readLiteralOnly, emptyPrec,
+ listOf(explTop1)
+ ),
+ Arguments.of(
+ explTop0, writeLiteralOnly, emptyPrec,
listOf(
- PtrState(ExplState.top(), 1))),
+ PtrState(ExplState.top(), 1)
+ )
+ ),
)
}
}
@ParameterizedTest
@MethodSource("testInputs")
- fun transFuncTest(state: PtrState, action: PtrAction, prec: PtrPrec,
- expectedResult: Collection>) {
+ fun transFuncTest(
+ state: PtrState, action: PtrAction, prec: PtrPrec,
+ expectedResult: Collection>
+ ) {
val analysis =
PtrAnalysis(ExplAnalysis.create(Z3LegacySolverFactory.getInstance().createSolver(), True()))
val result = analysis.transFunc.getSuccStates(state, action, prec)
diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/ChcUtils.kt b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/ChcUtils.kt
index 5b7789b350..1f3d2ee7c5 100644
--- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/ChcUtils.kt
+++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/ChcUtils.kt
@@ -61,8 +61,10 @@ open class Relation(val name: String, vararg paramTypes: Type) {
open operator fun invoke(vararg params: Expr<*>) = RelationApp(this, params.toList())
}
-data class RelationApp(val relation: Relation, val params: List>,
- val constraints: List> = emptyList()) {
+data class RelationApp(
+ val relation: Relation, val params: List>,
+ val constraints: List> = emptyList()
+) {
init {
checkArgument(params.size == relation.arity)
diff --git a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/dsl/Utils.kt b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/dsl/Utils.kt
index 488fe3330b..665121a5cd 100644
--- a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/dsl/Utils.kt
+++ b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/dsl/Utils.kt
@@ -33,8 +33,10 @@ fun ParserRuleContext.textWithWS(): String {
object ThrowingErrorListener : BaseErrorListener() {
@Throws(ParseCancellationException::class)
- override fun syntaxError(recognizer: Recognizer<*, *>?, offendingSymbol: Any?, line: Int,
- charPositionInLine: Int, msg: String, e: RecognitionException?) {
+ override fun syntaxError(
+ recognizer: Recognizer<*, *>?, offendingSymbol: Any?, line: Int,
+ charPositionInLine: Int, msg: String, e: RecognitionException?
+ ) {
throw ParseCancellationException("line $line:$charPositionInLine $msg")
}
}
\ No newline at end of file
diff --git a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/dsl/expr/ExprParser.kt b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/dsl/expr/ExprParser.kt
index f896e6265a..adfdcc3f80 100644
--- a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/dsl/expr/ExprParser.kt
+++ b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/dsl/expr/ExprParser.kt
@@ -118,8 +118,10 @@ class ExpressionWrapper(scope: Scope, content: String) {
}
private fun pop() {
- Preconditions.checkState(currentScope.enclosingScope().isPresent,
- "Enclosing scope is not present.")
+ Preconditions.checkState(
+ currentScope.enclosingScope().isPresent,
+ "Enclosing scope is not present."
+ )
currentScope = currentScope.enclosingScope().get()
env.pop()
}
@@ -127,8 +129,10 @@ class ExpressionWrapper(scope: Scope, content: String) {
////
override fun visitFuncLitExpr(ctx: FuncLitExprContext): Expr {
return if (ctx.result != null) {
- val param = Decls.Param(ctx.param.name.text,
- TypeWrapper(ctx.param.type().textWithWS()).instantiate())
+ val param = Decls.Param(
+ ctx.param.name.text,
+ TypeWrapper(ctx.param.type().textWithWS()).instantiate()
+ )
push(listOf(param))
val result = ctx.result.accept>(this) as Expr
pop()
@@ -144,8 +148,10 @@ class ExpressionWrapper(scope: Scope, content: String) {
} else {
ctx.decls.stream()
.map { d: DeclContext ->
- Decls.Param(d.name.getText(),
- TypeWrapper(d.ttype.textWithWS()).instantiate())
+ Decls.Param(
+ d.name.getText(),
+ TypeWrapper(d.ttype.textWithWS()).instantiate()
+ )
}.collect(Collectors.toList())
}
}
@@ -153,8 +159,10 @@ class ExpressionWrapper(scope: Scope, content: String) {
////
override fun visitIteExpr(ctx: IteExprContext): Expr {
return if (ctx.cond != null) {
- val cond: Expr = TypeUtils.cast(ctx.cond.accept>(this),
- BoolExprs.Bool())
+ val cond: Expr = TypeUtils.cast(
+ ctx.cond.accept>(this),
+ BoolExprs.Bool()
+ )
val then: Expr<*> = ctx.then.accept>(this)
val elze: Expr<*> = ctx.elze.accept>(this)
AbstractExprs.Ite(cond, then, elze)
@@ -165,10 +173,14 @@ class ExpressionWrapper(scope: Scope, content: String) {
override fun visitIffExpr(ctx: IffExprContext): Expr {
return if (ctx.rightOp != null) {
- val leftOp: Expr = TypeUtils.cast(ctx.leftOp.accept>(this),
- BoolExprs.Bool())
- val rightOp: Expr = TypeUtils.cast(ctx.rightOp.accept>(this),
- BoolExprs.Bool())
+ val leftOp: Expr = TypeUtils.cast(
+ ctx.leftOp.accept>(this),
+ BoolExprs.Bool()
+ )
+ val rightOp: Expr = TypeUtils.cast(
+ ctx.rightOp.accept>(this),
+ BoolExprs.Bool()
+ )
BoolExprs.Iff(leftOp, rightOp)
} else {
visitChildren(ctx)
@@ -177,10 +189,14 @@ class ExpressionWrapper(scope: Scope, content: String) {
override fun visitImplyExpr(ctx: ImplyExprContext): Expr {
return if (ctx.rightOp != null) {
- val leftOp: Expr = TypeUtils.cast(ctx.leftOp.accept>(this),
- BoolExprs.Bool())
- val rightOp: Expr = TypeUtils.cast(ctx.rightOp.accept>(this),
- BoolExprs.Bool())
+ val leftOp: Expr = TypeUtils.cast(
+ ctx.leftOp.accept>(this),
+ BoolExprs.Bool()
+ )
+ val rightOp: Expr = TypeUtils.cast(
+ ctx.rightOp.accept>(this),
+ BoolExprs.Bool()
+ )
BoolExprs.Imply(leftOp, rightOp)
} else {
visitChildren(ctx)
@@ -191,8 +207,10 @@ class ExpressionWrapper(scope: Scope, content: String) {
return if (ctx.paramDecls != null) {
val paramDecls = createParamList(ctx.paramDecls)
push(paramDecls)
- val op: Expr = TypeUtils.cast(ctx.op.accept>(this),
- BoolExprs.Bool())
+ val op: Expr = TypeUtils.cast(
+ ctx.op.accept>(this),
+ BoolExprs.Bool()
+ )
pop()
BoolExprs.Forall(paramDecls, op)
} else {
@@ -204,8 +222,10 @@ class ExpressionWrapper(scope: Scope, content: String) {
return if (ctx.paramDecls != null) {
val paramDecls = createParamList(ctx.paramDecls)
push(paramDecls)
- val op: Expr = TypeUtils.cast(ctx.op.accept>(this),
- BoolExprs.Bool())
+ val op: Expr = TypeUtils.cast(
+ ctx.op.accept>(this),
+ BoolExprs.Bool()
+ )
pop()
BoolExprs.Exists(paramDecls, op)
} else {
@@ -228,10 +248,14 @@ class ExpressionWrapper(scope: Scope, content: String) {
override fun visitXorExpr(ctx: XorExprContext): Expr {
return if (ctx.rightOp != null) {
- val leftOp: Expr = TypeUtils.cast(ctx.leftOp.accept>(this),
- BoolExprs.Bool())
- val rightOp: Expr = TypeUtils.cast(ctx.rightOp.accept>(this),
- BoolExprs.Bool())
+ val leftOp: Expr = TypeUtils.cast(
+ ctx.leftOp.accept>(this),
+ BoolExprs.Bool()
+ )
+ val rightOp: Expr = TypeUtils.cast(
+ ctx.rightOp.accept>(this),
+ BoolExprs.Bool()
+ )
BoolExprs.Xor(leftOp, rightOp)
} else {
visitChildren(ctx)
@@ -253,8 +277,10 @@ class ExpressionWrapper(scope: Scope, content: String) {
override fun visitNotExpr(ctx: NotExprContext): Expr {
return if (ctx.op != null) {
- val op: Expr = TypeUtils.cast(ctx.op.accept>(this),
- BoolExprs.Bool())
+ val op: Expr = TypeUtils.cast(
+ ctx.op.accept>(this),
+ BoolExprs.Bool()
+ )
BoolExprs.Not(op)
} else {
visitChildren(ctx)
@@ -386,8 +412,10 @@ class ExpressionWrapper(scope: Scope, content: String) {
}
}
- private fun createAdditiveExpr(opsHead: Expr<*>, opsTail: List>,
- oper: Token, ctx: AdditiveExprContext): Expr {
+ private fun createAdditiveExpr(
+ opsHead: Expr<*>, opsTail: List>,
+ oper: Token, ctx: AdditiveExprContext
+ ): Expr {
return if (opsTail.isEmpty()) {
opsHead
} else {
@@ -398,18 +426,24 @@ class ExpressionWrapper(scope: Scope, content: String) {
}
}
- private fun createAdditiveSubExpr(leftOp: Expr<*>, rightOp: Expr<*>, oper: Token,
- ctx: AdditiveExprContext): Expr {
+ private fun createAdditiveSubExpr(
+ leftOp: Expr<*>, rightOp: Expr<*>, oper: Token,
+ ctx: AdditiveExprContext
+ ): Expr {
return when (oper.type) {
PLUS -> createAddExpr(leftOp, rightOp)
MINUS -> createSubExpr(leftOp, rightOp)
BV_ADD -> createBvAddExpr(TypeUtils.castBv(leftOp), TypeUtils.castBv(rightOp))
BV_SUB -> createBvSubExpr(TypeUtils.castBv(leftOp), TypeUtils.castBv(rightOp))
- FPADD -> FpExprs.Add(getRoundingMode(ctx.oper.text),
- java.util.List.of(TypeUtils.castFp(leftOp), TypeUtils.castFp(rightOp)))
+ FPADD -> FpExprs.Add(
+ getRoundingMode(ctx.oper.text),
+ java.util.List.of(TypeUtils.castFp(leftOp), TypeUtils.castFp(rightOp))
+ )
- FPSUB -> FpExprs.Sub(getRoundingMode(ctx.oper.text), TypeUtils.castFp(leftOp),
- TypeUtils.castFp(rightOp))
+ FPSUB -> FpExprs.Sub(
+ getRoundingMode(ctx.oper.text), TypeUtils.castFp(leftOp),
+ TypeUtils.castFp(rightOp)
+ )
else -> throw ParseException(ctx, "Unknown operator '" + oper.text + "'")
}
@@ -459,8 +493,10 @@ class ExpressionWrapper(scope: Scope, content: String) {
}
}
- private fun createMutliplicativeExpr(opsHead: Expr<*>, opsTail: List>,
- oper: Token, ctx: MultiplicativeExprContext): Expr {
+ private fun createMutliplicativeExpr(
+ opsHead: Expr<*>, opsTail: List>,
+ oper: Token, ctx: MultiplicativeExprContext
+ ): Expr {
return if (opsTail.isEmpty()) {
opsHead
} else {
@@ -471,8 +507,10 @@ class ExpressionWrapper(scope: Scope, content: String) {
}
}
- private fun createMultiplicativeSubExpr(leftOp: Expr<*>, rightOp: Expr<*>, oper: Token,
- ctx: MultiplicativeExprContext): Expr {
+ private fun createMultiplicativeSubExpr(
+ leftOp: Expr<*>, rightOp: Expr<*>, oper: Token,
+ ctx: MultiplicativeExprContext
+ ): Expr {
return when (oper.type) {
MUL -> createMulExpr(leftOp, rightOp)
BV_MUL -> createBvMulExpr(TypeUtils.castBv(leftOp), TypeUtils.castBv(rightOp))
@@ -485,11 +523,15 @@ class ExpressionWrapper(scope: Scope, content: String) {
BV_UREM -> createBvURemExpr(TypeUtils.castBv(leftOp), TypeUtils.castBv(rightOp))
BV_SREM -> createBvSRemExpr(TypeUtils.castBv(leftOp), TypeUtils.castBv(rightOp))
FPREM -> FpExprs.Rem(leftOp as Expr, rightOp as Expr)
- FPMUL -> FpExprs.Mul(getRoundingMode(ctx.oper.text),
- java.util.List.of(leftOp as Expr, rightOp as Expr))
+ FPMUL -> FpExprs.Mul(
+ getRoundingMode(ctx.oper.text),
+ java.util.List.of(leftOp as Expr, rightOp as Expr)
+ )
- FPDIV -> FpExprs.Div(getRoundingMode(ctx.oper.text), leftOp as Expr,
- rightOp as Expr)
+ FPDIV -> FpExprs.Div(
+ getRoundingMode(ctx.oper.text), leftOp as Expr,
+ rightOp as Expr
+ )
else -> throw ParseException(ctx, "Unknown operator '" + oper.text + "'")
}
@@ -563,8 +605,10 @@ class ExpressionWrapper(scope: Scope, content: String) {
}
}
- private fun createConcatExpr(opsHead: Expr<*>, opsTail: List>,
- oper: Token): Expr {
+ private fun createConcatExpr(
+ opsHead: Expr<*>, opsTail: List>,
+ oper: Token
+ ): Expr {
return if (opsTail.isEmpty()) {
opsHead
} else {
@@ -575,8 +619,10 @@ class ExpressionWrapper(scope: Scope, content: String) {
}
}
- private fun createConcatSubExpr(leftOp: Expr<*>, rightOp: Expr<*>,
- oper: Token): Expr {
+ private fun createConcatSubExpr(
+ leftOp: Expr<*>, rightOp: Expr<*>,
+ oper: Token
+ ): Expr {
return when (oper.type) {
BV_CONCAT -> createBvConcatExpr(TypeUtils.castBv(leftOp), TypeUtils.castBv(rightOp))
else -> throw AssertionError()
@@ -599,10 +645,12 @@ class ExpressionWrapper(scope: Scope, content: String) {
val extendType = BvExprs.BvType(ctx.rightOp.size.getText().toInt())
when (ctx.oper.getType()) {
BV_ZERO_EXTEND -> BvExprs.ZExt(
- TypeUtils.castBv(ctx.leftOp.accept>(this)), extendType)
+ TypeUtils.castBv(ctx.leftOp.accept>(this)), extendType
+ )
BV_SIGN_EXTEND -> BvExprs.SExt(
- TypeUtils.castBv(ctx.leftOp.accept>(this)), extendType)
+ TypeUtils.castBv(ctx.leftOp.accept>(this)), extendType
+ )
else -> throw AssertionError()
}
@@ -621,20 +669,28 @@ class ExpressionWrapper(scope: Scope, content: String) {
FP_ABS -> FpExprs.Abs(op as Expr)
FP_IS_INF -> FpExprs.IsInfinite(op as Expr)
FP_IS_NAN -> FpExprs.IsNan(op as Expr)
- FPROUNDTOINT -> FpExprs.RoundToIntegral(getRoundingMode(ctx.oper.text),
- op as Expr)
+ FPROUNDTOINT -> FpExprs.RoundToIntegral(
+ getRoundingMode(ctx.oper.text),
+ op as Expr
+ )
FPSQRT -> FpExprs.Sqrt(getRoundingMode(ctx.oper.text), op as Expr)
- FPTOFP -> FpExprs.ToFp(getRoundingMode(ctx.oper.text), op as Expr,
- getExp(ctx.oper.getText()), getSignificand(ctx.oper.getText()))
-
- FPTOBV -> FpExprs.ToBv(getRoundingMode(ctx.oper.text), op as Expr,
- getBvSize(ctx.oper.getText()), isSignedBv(ctx.oper.getText()))
-
- FP_FROM_BV -> FpExprs.FromBv(getRoundingMode(ctx.oper.text),
+ FPTOFP -> FpExprs.ToFp(
+ getRoundingMode(ctx.oper.text), op as Expr,
+ getExp(ctx.oper.getText()), getSignificand(ctx.oper.getText())
+ )
+
+ FPTOBV -> FpExprs.ToBv(
+ getRoundingMode(ctx.oper.text), op as Expr,
+ getBvSize(ctx.oper.getText()), isSignedBv(ctx.oper.getText())
+ )
+
+ FP_FROM_BV -> FpExprs.FromBv(
+ getRoundingMode(ctx.oper.text),
op as Expr,
FpType.of(getExp(ctx.oper.getText()), getSignificand(ctx.oper.getText())),
- isSignedFp(ctx.oper.getText()))
+ isSignedFp(ctx.oper.getText())
+ )
FPNEG -> FpExprs.Neg(op as Expr)
FPPOS -> FpExprs.Pos(op as Expr)
@@ -717,7 +773,8 @@ class ExpressionWrapper(scope: Scope, content: String) {
return if (ctx.array != null) {
ArrayReadExpr.create(
ctx.array.accept(this),
- ctx.index.accept(this))
+ ctx.index.accept(this)
+ )
} else {
visitChildren(ctx)
}
@@ -728,7 +785,8 @@ class ExpressionWrapper(scope: Scope, content: String) {
ArrayWriteExpr.create(
ctx.array.accept(this),
ctx.index.accept(this),
- ctx.elem.accept(this))
+ ctx.elem.accept(this)
+ )
} else {
visitChildren(ctx)
}
@@ -746,8 +804,10 @@ class ExpressionWrapper(scope: Scope, content: String) {
return if (ctx.op != null) {
val op = ctx.op.accept(this)
val bitvec = TypeUtils.castBv(op)
- return BvExprs.Extract(bitvec, Int(ctx.from.getText()),
- IntExprs.Int(ctx.until.getText()))
+ return BvExprs.Extract(
+ bitvec, Int(ctx.from.getText()),
+ IntExprs.Int(ctx.until.getText())
+ )
} else {
visitChildren(ctx)
}
@@ -804,14 +864,19 @@ class ExpressionWrapper(scope: Scope, content: String) {
override fun visitArrLitExpr(ctx: ArrLitExprContext): Expr {
Preconditions.checkNotNull(ctx.elseExpr)
val indexType = if (ctx.indexExpr.size > 0) ctx.indexExpr[0].accept(
- this).type else Int()
+ this
+ ).type else Int()
val elseElem = ctx.elseExpr.accept(this)
val valueType = elseElem.type
val elems = ctx.indexExpr.mapIndexed { idx, it ->
Tuple2.of(it.accept(this), ctx.valueExpr[idx].accept(this))
}
- return ExprUtils.simplify(ArrayInitExpr.create(elems, elseElem,
- ArrayType.of(indexType, valueType)))
+ return ExprUtils.simplify(
+ ArrayInitExpr.create(
+ elems, elseElem,
+ ArrayType.of(indexType, valueType)
+ )
+ )
}
override fun visitBvLitExpr(ctx: BvLitExprContext): Expr {
@@ -822,7 +887,8 @@ class ExpressionWrapper(scope: Scope, content: String) {
decodeBinaryBvContent(content.substring(1))
} else if (content.startsWith("d")) {
check(
- sizeAndContent.size == 2) { "Decimal value is only parseable if size is given." }
+ sizeAndContent.size == 2
+ ) { "Decimal value is only parseable if size is given." }
decodeDecimalBvContent(content.substring(1), sizeAndContent[0].toInt())
} else if (content.startsWith("x")) {
decodeHexadecimalBvContent(content.substring(1))
@@ -843,7 +909,8 @@ class ExpressionWrapper(scope: Scope, content: String) {
'0' -> value[i] = false
'1' -> value[i] = true
else -> throw IllegalArgumentException(
- "Binary literal can contain only 0 and 1")
+ "Binary literal can contain only 0 and 1"
+ )
}
}
return value
@@ -853,7 +920,8 @@ class ExpressionWrapper(scope: Scope, content: String) {
var value = BigInteger(lit)
Preconditions.checkArgument(
value.compareTo(
- BigInteger.TWO.pow(size - 1).multiply(BigInteger.valueOf(-1))) >= 0 &&
+ BigInteger.TWO.pow(size - 1).multiply(BigInteger.valueOf(-1))
+ ) >= 0 &&
value.compareTo(BigInteger.TWO.pow(size)) < 0,
"Decimal literal is not in range"
)
@@ -892,8 +960,10 @@ class ExpressionWrapper(scope: Scope, content: String) {
override fun visitIdExpr(ctx: IdExprContext): RefExpr<*> {
val optSymbol = currentScope.resolve(ctx.id.getText())
if (optSymbol.isEmpty) {
- throw ParseException(ctx,
- "Identifier '" + ctx.id.getText() + "' cannot be resolved")
+ throw ParseException(
+ ctx,
+ "Identifier '" + ctx.id.getText() + "' cannot be resolved"
+ )
}
val symbol = optSymbol.get()
val decl = env.eval(symbol) as Decl<*>
diff --git a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/dsl/stmt/StmtParser.kt b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/dsl/stmt/StmtParser.kt
index 09ea6e8f9d..d11ca4187c 100644
--- a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/dsl/stmt/StmtParser.kt
+++ b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/dsl/stmt/StmtParser.kt
@@ -108,7 +108,8 @@ class StatementWrapper(val content: String, scope: Scope) {
override fun visitMemAssignStmt(ctx: MemAssignStmtContext): Stmt {
val derefExpr: Dereference<*, *, *> = ExpressionWrapper(scope, ctx.derefExpr().textWithWS()).instantiate(
- env) as Dereference<*, *, *>
+ env
+ ) as Dereference<*, *, *>
val value = ExpressionWrapper(scope, ctx.value.textWithWS())
val valueE: Expr<*> = value.instantiate(env)
return if (derefExpr.type == valueE.type) {
diff --git a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/ArgAdapter.kt b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/ArgAdapter.kt
index a05598f87e..eaad49e3e0 100644
--- a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/ArgAdapter.kt
+++ b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/ArgAdapter.kt
@@ -26,9 +26,11 @@ import hu.bme.mit.theta.analysis.State
import hu.bme.mit.theta.analysis.algorithm.arg.ARG
import java.lang.reflect.Type
-class ArgAdapter(val gsonSupplier: () -> Gson,
+class ArgAdapter(
+ val gsonSupplier: () -> Gson,
private val partialOrdSupplier: () -> PartialOrd,
- private val argTypeSupplier: () -> Type) : TypeAdapter>() {
+ private val argTypeSupplier: () -> Type
+) : TypeAdapter>() {
private lateinit var gson: Gson
private lateinit var partialOrd: PartialOrd
diff --git a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/ArgAdapterHelper.kt b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/ArgAdapterHelper.kt
index f00ff2ac89..05e193a195 100644
--- a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/ArgAdapterHelper.kt
+++ b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/ArgAdapterHelper.kt
@@ -54,11 +54,14 @@ data class ArgAdapterHelper(
while (waitSet.isNotEmpty()) {
val entry = waitSet.firstOrNull { lut.keys.contains(checkNotNull(edges[it]).source) }
check(
- entry != null) { "Unreachable node(s) present: $waitSet\nedges: $edges\nlut: $lut" }
+ entry != null
+ ) { "Unreachable node(s) present: $waitSet\nedges: $edges\nlut: $lut" }
waitSet.remove(entry)
val edge = checkNotNull(edges[entry])
- lut[entry] = arg.createSuccNode(lut[edge.source], edge.action, checkNotNull(nodes[entry]).state,
- checkNotNull(nodes[entry]).target)
+ lut[entry] = arg.createSuccNode(
+ lut[edge.source], edge.action, checkNotNull(nodes[entry]).state,
+ checkNotNull(nodes[entry]).target
+ )
.also { n -> if (checkNotNull(nodes[entry]).expanded) n.expanded = true }
}
coveringEdges.forEach { checkNotNull(lut[it.key]).cover(lut[it.value]) }
diff --git a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/SafetyResultAdapter.kt b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/SafetyResultAdapter.kt
index 6829d577c0..271417ea04 100644
--- a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/SafetyResultAdapter.kt
+++ b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/SafetyResultAdapter.kt
@@ -40,8 +40,10 @@ class SafetyResultAdapter(
private lateinit var argType: Type
private lateinit var traceType: Type
- override fun write(writer: JsonWriter,
- value: SafetyResult, Trace>) {
+ override fun write(
+ writer: JsonWriter,
+ value: SafetyResult, Trace>
+ ) {
initGson()
writer.beginObject()
writer.name("arg")
@@ -80,8 +82,10 @@ class SafetyResultAdapter(
return if (stats.isEmpty)
if (safe == true) SafetyResult.safe(arg) else SafetyResult.unsafe(trace, arg)
else
- if (safe == false) SafetyResult.safe(arg, stats.get()) else SafetyResult.unsafe(trace,
- arg, stats.get())
+ if (safe == false) SafetyResult.safe(arg, stats.get()) else SafetyResult.unsafe(
+ trace,
+ arg, stats.get()
+ )
}
private fun initGson() {
diff --git a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/StateAdapters.kt b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/StateAdapters.kt
index a75f2133cb..30031d82e0 100644
--- a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/StateAdapters.kt
+++ b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/StateAdapters.kt
@@ -89,8 +89,10 @@ class PredStateAdapter(val gsonSupplier: () -> Gson, val scope: Scope, val env:
check(reader.nextName() == "bottom")
if (reader.nextBoolean()) ret = PredState.bottom()
check(reader.nextName() == "preds")
- val preds = gson.fromJson>>(reader,
- object : TypeToken>>() {}.type)
+ val preds = gson.fromJson>>(
+ reader,
+ object : TypeToken>>() {}.type
+ )
if (ret == null) ret = PredState.of(preds)
reader.endObject()
return ret!!
diff --git a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/TraceAdapter.kt b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/TraceAdapter.kt
index 0571800b23..649ec9d72c 100644
--- a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/TraceAdapter.kt
+++ b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/TraceAdapter.kt
@@ -26,8 +26,10 @@ import hu.bme.mit.theta.analysis.State
import hu.bme.mit.theta.analysis.Trace
import java.lang.reflect.Type
-class TraceAdapter(val gsonSupplier: () -> Gson, private val stateTypeSupplier: () -> Type,
- private val actionType: Type) : TypeAdapter>() {
+class TraceAdapter(
+ val gsonSupplier: () -> Gson, private val stateTypeSupplier: () -> Type,
+ private val actionType: Type
+) : TypeAdapter>() {
private lateinit var gson: Gson
private lateinit var stateType: Type
@@ -47,11 +49,15 @@ class TraceAdapter(val gsonSupplier: () -> Gson, private val stateTypeSupplier:
if (!this::stateType.isInitialized) stateType = stateTypeSupplier()
reader.beginObject()
check(reader.nextName() == "states")
- val stateList: List = gson.fromJson(reader,
- TypeToken.getParameterized(TypeToken.get(List::class.java).type, stateType).type)
+ val stateList: List = gson.fromJson(
+ reader,
+ TypeToken.getParameterized(TypeToken.get(List::class.java).type, stateType).type
+ )
check(reader.nextName() == "actions")
- val actionList: List = gson.fromJson(reader,
- TypeToken.getParameterized(TypeToken.get(List::class.java).type, actionType).type)
+ val actionList: List = gson.fromJson(
+ reader,
+ TypeToken.getParameterized(TypeToken.get(List::class.java).type, actionType).type
+ )
reader.endObject()
return Trace.of(stateList, actionList)
}
diff --git a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/VarDeclAdapter.kt b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/VarDeclAdapter.kt
index 8e0ea55885..2dc571788f 100644
--- a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/VarDeclAdapter.kt
+++ b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/VarDeclAdapter.kt
@@ -29,8 +29,10 @@ import hu.bme.mit.theta.core.decl.Decls.Var
import hu.bme.mit.theta.core.decl.VarDecl
import hu.bme.mit.theta.core.type.Type
-class VarDeclAdapter(val gsonSupplier: () -> Gson, val scope: MutableScope, val env: Env,
- val throwIfNotInScope: Boolean = false) : TypeAdapter>() {
+class VarDeclAdapter(
+ val gsonSupplier: () -> Gson, val scope: MutableScope, val env: Env,
+ val throwIfNotInScope: Boolean = false
+) : TypeAdapter>() {
private lateinit var gson: Gson
diff --git a/subprojects/common/grammar/src/test/java/hu/bme/mit/theta/grammar/dsl/ExprTest.kt b/subprojects/common/grammar/src/test/java/hu/bme/mit/theta/grammar/dsl/ExprTest.kt
index ff72c48eb5..b647fb75c2 100644
--- a/subprojects/common/grammar/src/test/java/hu/bme/mit/theta/grammar/dsl/ExprTest.kt
+++ b/subprojects/common/grammar/src/test/java/hu/bme/mit/theta/grammar/dsl/ExprTest.kt
@@ -91,36 +91,57 @@ class ExprTest {
arrayOf(fpLit1, "(#b1 #b1010 #b101010)", emptyMap>()),
arrayOf(fpLit2, "(#b0 #b1010 #b101010)", emptyMap>()),
- arrayOf(ArrayLitExpr.of(listOf(), Int(2), ArrayType.of(Int(), Int())),
- "(array (default 2))", emptyMap>()),
- arrayOf(ArrayLitExpr.of(listOf(Tuple2.of(Int(0), Int(1))), Int(2),
- ArrayType.of(Int(), Int())), "(array (0 1) (default 2))",
- emptyMap>()),
arrayOf(
- ArrayLitExpr.of(listOf(Tuple2.of(Int(0), Int(1)), Tuple2.of(Int(1), Int(2))),
- Int(3), ArrayType.of(Int(), Int())), "(array (0 1) (1 2) (default 3))",
- emptyMap>()),
+ ArrayLitExpr.of(listOf(), Int(2), ArrayType.of(Int(), Int())),
+ "(array (default 2))", emptyMap>()
+ ),
+ arrayOf(
+ ArrayLitExpr.of(
+ listOf(Tuple2.of(Int(0), Int(1))), Int(2),
+ ArrayType.of(Int(), Int())
+ ), "(array (0 1) (default 2))",
+ emptyMap>()
+ ),
+ arrayOf(
+ ArrayLitExpr.of(
+ listOf(Tuple2.of(Int(0), Int(1)), Tuple2.of(Int(1), Int(2))),
+ Int(3), ArrayType.of(Int(), Int())
+ ), "(array (0 1) (1 2) (default 3))",
+ emptyMap>()
+ ),
arrayOf(RefExpr.of(x), "x", mapOf(Pair(NamedSymbol("x"), x))),
- arrayOf(Ite(True(), Int(1), Int(2)), "(ite true 1 2)",
- emptyMap>()),
+ arrayOf(
+ Ite(True(), Int(1), Int(2)), "(ite true 1 2)",
+ emptyMap>()
+ ),
arrayOf(Iff(True(), False()), "(iff true false)", emptyMap>()),
arrayOf(Imply(True(), False()), "(=> true false)", emptyMap>()),
- arrayOf(Forall(listOf(p), True()), "(forall ((p Int)) true)",
- mapOf(Pair(NamedSymbol("p"), p))),
- arrayOf(Exists(listOf(p), True()), "(exists ((p Int)) true)",
- mapOf(Pair(NamedSymbol("p"), p))),
+ arrayOf(
+ Forall(listOf(p), True()), "(forall ((p Int)) true)",
+ mapOf(Pair(NamedSymbol("p"), p))
+ ),
+ arrayOf(
+ Exists(listOf(p), True()), "(exists ((p Int)) true)",
+ mapOf(Pair(NamedSymbol("p"), p))
+ ),
- arrayOf(Max(fpLit1, fpLit2), "(fpmax (#b1 #b1010 #b101010) (#b0 #b1010 #b101010))",
- emptyMap>()),
- arrayOf(Min(fpLit1, fpLit2), "(fpmin (#b1 #b1010 #b101010) (#b0 #b1010 #b101010))",
- emptyMap>()),
+ arrayOf(
+ Max(fpLit1, fpLit2), "(fpmax (#b1 #b1010 #b101010) (#b0 #b1010 #b101010))",
+ emptyMap>()
+ ),
+ arrayOf(
+ Min(fpLit1, fpLit2), "(fpmin (#b1 #b1010 #b101010) (#b0 #b1010 #b101010))",
+ emptyMap>()
+ ),
arrayOf(Or(True(), False()), "(or true false)", emptyMap>()),
arrayOf(Xor(True(), False()), "(xor true false)", emptyMap>()),
- arrayOf(And(True(), False(), False()), "(and true false false)",
- emptyMap>()),
+ arrayOf(
+ And(True(), False(), False()), "(and true false false)",
+ emptyMap>()
+ ),
arrayOf(Not(True()), "(not true)", emptyMap>()),
arrayOf(Eq(Int(1), Int(2)), "(= 1 2)", emptyMap>()),
@@ -129,80 +150,142 @@ class ExprTest {
arrayOf(Gt(Int(1), Int(2)), "(> 1 2)", emptyMap>()),
arrayOf(Geq(Int(1), Int(2)), "(>= 1 2)", emptyMap>()),
- arrayOf(BvExprs.ULt(bvLit1, bvLit1), "(bvult #b1010 #b1010)",
- emptyMap>()),
- arrayOf(BvExprs.ULeq(bvLit1, bvLit1), "(bvule #b1010 #b1010)",
- emptyMap>()),
- arrayOf(BvExprs.UGt(bvLit1, bvLit1), "(bvugt #b1010 #b1010)",
- emptyMap