From e37b32302b2cb72893e26b52bc63d305e999a98f Mon Sep 17 00:00:00 2001 From: "ThetaBotMaintainer[bot]" <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> Date: Fri, 18 Oct 2024 18:24:37 +0000 Subject: [PATCH] Reformatted code --- .../bounded/BoundedCheckerBuilder.kt | 6 +++-- .../hu/bme/mit/theta/analysis/ptr/PtrUtils.kt | 3 ++- .../mit/theta/grammar/gson/StateAdapters.kt | 3 ++- .../hu/bme/mit/theta/grammar/gson/TestGson.kt | 18 +++++++++----- .../bme/mit/theta/xcfa/cli/ExecuteConfig.kt | 3 ++- .../bme/mit/theta/xcfa/cli/utils/GsonUtils.kt | 9 ++++--- .../xcfa/passes/FetchExecuteWriteback.kt | 24 ++++++++++++------- .../mit/theta/xcfa/passes/UnusedVarPass.kt | 3 ++- .../hu/bme/mit/theta/xcfa/gson/GsonTest.kt | 6 +++-- 9 files changed, 49 insertions(+), 26 deletions(-) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt index b54dc029aa..03de89fb27 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt @@ -34,7 +34,8 @@ fun buildBMC( bmcEnabled: () -> Boolean = { true }, lfPathOnly: () -> Boolean = { true }, ): BoundedChecker { - return BoundedChecker(monolithicExpr, shouldGiveUp, bmcSolver, bmcEnabled, lfPathOnly, null, { false }, null, + return BoundedChecker( + monolithicExpr, shouldGiveUp, bmcSolver, bmcEnabled, lfPathOnly, null, { false }, null, { false }, valToState, biValToAction, logger ) } @@ -71,7 +72,8 @@ fun buildIMC( lfPathOnly: () -> Boolean = { true }, imcEnabled: (Int) -> Boolean = { true }, ): BoundedChecker { - return BoundedChecker(monolithicExpr, shouldGiveUp, bmcSolver, bmcEnabled, lfPathOnly, itpSolver, imcEnabled, null, + return BoundedChecker( + monolithicExpr, shouldGiveUp, bmcSolver, bmcEnabled, lfPathOnly, itpSolver, imcEnabled, null, { false }, valToState, biValToAction, logger ) } \ No newline at end of file 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 d1748f2526..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 @@ -149,7 +149,8 @@ fun Expr.uniqueDereferences( Pair(ret, retDeref) } else { val ret = ArrayList() - Pair(ret, + Pair( + ret, this.withOps(this.ops.map { it.uniqueDereferences(vargen, lookup).also { ret.addAll(it.first) }.second }) ) } 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 1675ec639a..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,7 +89,8 @@ 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, + val preds = gson.fromJson>>( + reader, object : TypeToken>>() {}.type ) if (ret == null) ret = PredState.of(preds) diff --git a/subprojects/common/grammar/src/test/java/hu/bme/mit/theta/grammar/gson/TestGson.kt b/subprojects/common/grammar/src/test/java/hu/bme/mit/theta/grammar/gson/TestGson.kt index 026a4626ee..c4d39653a0 100644 --- a/subprojects/common/grammar/src/test/java/hu/bme/mit/theta/grammar/gson/TestGson.kt +++ b/subprojects/common/grammar/src/test/java/hu/bme/mit/theta/grammar/gson/TestGson.kt @@ -101,13 +101,16 @@ class TestGson { private fun getExplBuilder(gsonSuppl: () -> Gson): GsonBuilder { val gsonBuilder = GsonBuilder() - gsonBuilder.registerTypeHierarchyAdapter(ARG::class.java, + gsonBuilder.registerTypeHierarchyAdapter( + ARG::class.java, ArgAdapter(gsonSuppl, { ExplOrd.getInstance() }, { explArgAdapterHelper() }) ) - gsonBuilder.registerTypeHierarchyAdapter(Trace::class.java, + gsonBuilder.registerTypeHierarchyAdapter( + Trace::class.java, TraceAdapter(gsonSuppl, { ExplState::class.java }, SimpleStmtAction::class.java) ) - gsonBuilder.registerTypeHierarchyAdapter(SafetyResult::class.java, + gsonBuilder.registerTypeHierarchyAdapter( + SafetyResult::class.java, SafetyResultAdapter(gsonSuppl, { explArgHelper() }, { explTraceHelper() }) ) @@ -117,13 +120,16 @@ class TestGson { private fun getPredBuilder(gsonSuppl: () -> Gson): GsonBuilder { val gsonBuilder = GsonBuilder() - gsonBuilder.registerTypeHierarchyAdapter(ARG::class.java, + gsonBuilder.registerTypeHierarchyAdapter( + ARG::class.java, ArgAdapter(gsonSuppl, { PartialOrd { a, b -> true } }, { predArgAdapterHelper() }) ) - gsonBuilder.registerTypeHierarchyAdapter(Trace::class.java, + gsonBuilder.registerTypeHierarchyAdapter( + Trace::class.java, TraceAdapter(gsonSuppl, { PredState::class.java }, SimpleStmtAction::class.java) ) - gsonBuilder.registerTypeHierarchyAdapter(SafetyResult::class.java, + gsonBuilder.registerTypeHierarchyAdapter( + SafetyResult::class.java, SafetyResultAdapter(gsonSuppl, { predArgHelper() }, { predTraceHelper() }) ) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt index afb0bb997a..e835aaf239 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt @@ -181,7 +181,8 @@ fun frontend(config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger): Tr ) logger.write(RESULT, "ParsingResult Success\n") - logger.write(RESULT, + logger.write( + RESULT, "Alias graph size: ${xcfa.pointsToGraph.size} -> ${xcfa.pointsToGraph.values.map { it.size }.toList()}\n" ) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/GsonUtils.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/GsonUtils.kt index 72ddc379d7..8ef9ed0318 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/GsonUtils.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/GsonUtils.kt @@ -106,7 +106,8 @@ private fun getGson( StringTypeAdapter(xcfaLocationAdapter) ) gsonBuilder.registerTypeHierarchyAdapter(XCFA::class.java, XcfaAdapter { gson }) - gsonBuilder.registerTypeHierarchyAdapter(VarDecl::class.java, + gsonBuilder.registerTypeHierarchyAdapter( + VarDecl::class.java, VarDeclAdapter({ gson }, scope, env, !newScope) ) gsonBuilder.registerTypeHierarchyAdapter(Stmt::class.java, @@ -118,10 +119,12 @@ private fun getGson( gsonBuilder.registerTypeHierarchyAdapter(VarIndexing::class.java, StringTypeAdapter { BasicVarIndexing.fromString(it, scope, env) }) gsonBuilder.registerTypeHierarchyAdapter(ExplState::class.java, ExplStateAdapter(scope, env)) - gsonBuilder.registerTypeHierarchyAdapter(PredState::class.java, + gsonBuilder.registerTypeHierarchyAdapter( + PredState::class.java, PredStateAdapter({ gson }, scope, env) ) - gsonBuilder.registerTypeHierarchyAdapter(XcfaLabel::class.java, + gsonBuilder.registerTypeHierarchyAdapter( + XcfaLabel::class.java, XcfaLabelAdapter(scope, env, { gson }) ) gsonBuilder.registerTypeHierarchyAdapter(MetaData::class.java, MetaDataAdapter()) diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/FetchExecuteWriteback.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/FetchExecuteWriteback.kt index 89c11f3a78..894f89ccb2 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/FetchExecuteWriteback.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/FetchExecuteWriteback.kt @@ -73,9 +73,11 @@ class FetchExecuteWriteback(val parseContext: ParseContext) : ProcedurePass { is InvokeLabel -> { val lut = getDerefLut(dereferences, builder) SequenceLabel(lut.map { - StmtLabel(Assign(cast(it.value, it.value.type), - cast(it.key.map { it.replaceDerefs(lut) }, it.value.type) - ) + StmtLabel( + Assign( + cast(it.value, it.value.type), + cast(it.key.map { it.replaceDerefs(lut) }, it.value.type) + ) ) } + InvokeLabel( this.name, this.params.map { it.replaceDerefs(lut) }, metadata, @@ -87,9 +89,11 @@ class FetchExecuteWriteback(val parseContext: ParseContext) : ProcedurePass { is StartLabel -> { val lut = getDerefLut(dereferences, builder) SequenceLabel(lut.map { - StmtLabel(Assign(cast(it.value, it.value.type), - cast(it.key.map { it.replaceDerefs(lut) }, it.value.type) - ) + StmtLabel( + Assign( + cast(it.value, it.value.type), + cast(it.key.map { it.replaceDerefs(lut) }, it.value.type) + ) ) } + StartLabel(name, params.map { it.replaceDerefs(lut) }, pidVar, metadata, tempLookup), metadata) } @@ -129,9 +133,11 @@ class FetchExecuteWriteback(val parseContext: ParseContext) : ProcedurePass { val ret = ArrayList() val accessType = dereferencesWithAccessTypes.filter { dereferences.contains(it.first) } for (dereference in accessType.filter { it.second.isRead }.map { it.first }) { - ret.add(Assign(cast(lut[dereference]!!, dereference.type), - cast(dereference.map { it.replaceDerefs(lut.filter { it.key != dereference }) }, dereference.type) - ) + ret.add( + Assign( + cast(lut[dereference]!!, dereference.type), + cast(dereference.map { it.replaceDerefs(lut.filter { it.key != dereference }) }, dereference.type) + ) ) } ret.add(stmt) diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/UnusedVarPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/UnusedVarPass.kt index 8825144189..c8ed0b0c27 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/UnusedVarPass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/UnusedVarPass.kt @@ -62,7 +62,8 @@ class UnusedVarPass(private val uniqueWarningLogger: Logger) : ProcedurePass { val allVars = Sets.union(builder.getVars(), builder.parent.getVars().map { it.wrappedVar }.toSet()) val varsAndParams = Sets.union(allVars, builder.getParams().map { it.first }.toSet()) if (!varsAndParams.containsAll(usedVars)) { - uniqueWarningLogger.write(Logger.Level.INFO, + uniqueWarningLogger.write( + Logger.Level.INFO, "WARNING: There are some used variables not present as declarations: " + "${usedVars.filter { it !in varsAndParams }}\n" ) diff --git a/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/gson/GsonTest.kt b/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/gson/GsonTest.kt index 056ed4d9f0..b7b48eb5a4 100644 --- a/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/gson/GsonTest.kt +++ b/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/gson/GsonTest.kt @@ -51,7 +51,8 @@ class GsonTest { StringTypeAdapter(xcfaLocationAdapter) ) gsonBuilder.registerTypeHierarchyAdapter(XCFA::class.java, XcfaAdapter { gson }) - gsonBuilder.registerTypeHierarchyAdapter(VarDecl::class.java, + gsonBuilder.registerTypeHierarchyAdapter( + VarDecl::class.java, VarDeclAdapter({ gson }, scope, env, !newScope) ) gsonBuilder.registerTypeHierarchyAdapter(Stmt::class.java, @@ -62,7 +63,8 @@ class GsonTest { StringTypeAdapter { TypeWrapper(it).instantiate() }) gsonBuilder.registerTypeHierarchyAdapter(VarIndexing::class.java, StringTypeAdapter { BasicVarIndexing.fromString(it, scope, env) }) - gsonBuilder.registerTypeHierarchyAdapter(XcfaLabel::class.java, + gsonBuilder.registerTypeHierarchyAdapter( + XcfaLabel::class.java, XcfaLabelAdapter(scope, env, { gson }) ) gsonBuilder.registerTypeHierarchyAdapter(MetaData::class.java, MetaDataAdapter())