Reformatted code

ftsrg · Oct 18, 2024 · e37b323 · e37b323
1 parent 185dc7a
commit e37b323
Show file tree

Hide file tree

Showing 9 changed files with 49 additions and 26 deletions.
diff --git a/...alysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt b/...alysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt
@@ -34,7 +34,8 @@ fun <S : ExprState, A : ExprAction> buildBMC(
     bmcEnabled: () -> Boolean = { true },
     lfPathOnly: () -> Boolean = { true },
 ): BoundedChecker<S, A> {
-    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 <S : ExprState, A : ExprAction> buildIMC(
     lfPathOnly: () -> Boolean = { true },
     imcEnabled: (Int) -> Boolean = { true },
 ): BoundedChecker<S, A> {
-    return BoundedChecker(monolithicExpr, shouldGiveUp, bmcSolver, bmcEnabled, lfPathOnly, itpSolver, imcEnabled, null,
+    return BoundedChecker(
+        monolithicExpr, shouldGiveUp, bmcSolver, bmcEnabled, lfPathOnly, itpSolver, imcEnabled, null,
         { false }, valToState, biValToAction, logger
     )
 }
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
@@ -149,7 +149,8 @@ fun <T : Type> Expr<T>.uniqueDereferences(
         Pair(ret, retDeref)
     } else {
         val ret = ArrayList<Stmt>()
-        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
@@ -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<Set<Expr<BoolType>>>(reader,
+        val preds = gson.fromJson<Set<Expr<BoolType>>>(
+            reader,
             object : TypeToken<Set<Expr<BoolType>>>() {}.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
@@ -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<PredState> { 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
@@ -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
@@ -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
@@ -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<Stmt>()
         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
@@ -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
@@ -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())