Fixed bugs from SonarLint #2

ftsrg · Jul 22, 2023 · 8e496a8 · 8e496a8
1 parent 083b266
commit 8e496a8
Show file tree

Hide file tree

Showing 6 changed files with 27 additions and 21 deletions.
diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpFromBvExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpFromBvExpr.java
@@ -85,7 +85,7 @@ public FpLitExpr eval(Valuation val) {
     public boolean equals(final Object obj) {
         if (this == obj) {
             return true;
-        } else if (obj.getClass() == this.getClass()) {
+        } else if (obj != null && obj.getClass() == this.getClass()) {
             final FpFromBvExpr that = (FpFromBvExpr) obj;
             return this.getOp().equals(that.getOp()) && fpType.equals(that.fpType)
                     && roundingMode.equals(that.roundingMode);

diff --git a/...n/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java b/...n/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java
@@ -489,8 +489,9 @@ public Expr<?> visitUnaryExpressionCast(CParser.UnaryExpressionCastContext ctx)
                 parseContext.getMetadata().create(expr, "cType", smallestCommonType);
                 return expr;
             case "&":
-                checkState(accept instanceof RefExpr<?> && ((RefExpr<?>) accept).getDecl() instanceof VarDecl, "Referencing non-variable expressions is not allowed!");
-                return reference((RefExpr<?>) accept);
+                final Expr<?> localAccept = accept;
+                checkState(localAccept instanceof RefExpr<?> && ((RefExpr<?>) localAccept).getDecl() instanceof VarDecl, "Referencing non-variable expressions is not allowed!");
+                return reference((RefExpr<?>) localAccept);
             case "*":
                 type = CComplexType.getType(accept, parseContext);
                 checkState(type instanceof CPointer, "Dereferencing non-pointer expression is not allowed!");

diff --git a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt
@@ -59,7 +59,7 @@ class FrontendXcfaBuilder(val parseContext: ParseContext, val checkOverflow: Boo
         if (name == null) return getAnonymousLoc(builder, metadata = metadata)
         locationLut.putIfAbsent(name, XcfaLocation(name, metadata = metadata))
         val location = locationLut[name]
-        builder.addLoc(location!!)
+        builder.addLoc(checkNotNull(location))
         return location
     }
 
@@ -199,7 +199,7 @@ class FrontendXcfaBuilder(val parseContext: ParseContext, val checkOverflow: Boo
                 memoryMaps[type] = toAdd
                 parseContext.metadata.create(toAdd, "defaultElement", CComplexType.getType(op, parseContext).nullValue)
             }
-            val memoryMap = memoryMaps[type]!!
+            val memoryMap = checkNotNull(memoryMaps[type])
             parseContext.metadata.create(op, "dereferenced", true)
             parseContext.metadata.create(op, "refSubstitute", memoryMap)
             val write = ArrayExprs.Write(cast(memoryMap.ref, ArrayType.of(ptrType, type)),
@@ -690,7 +690,7 @@ class FrontendXcfaBuilder(val parseContext: ParseContext, val checkOverflow: Boo
             }
             if (cStatement is CCase) {
                 val afterGuard = buildPostStatement(testValue,
-                    ParamPack(builder, endInit!!, breakLoc, continueLoc, returnLoc))
+                    ParamPack(builder, checkNotNull(endInit), breakLoc, continueLoc, returnLoc))
                 val assume = StmtLabel(
                     Stmts.Assume(
                         AbstractExprs.Eq(testValue.expression, cStatement.expr.expression)),

diff --git a/subprojects/xcfa/litmus-cli/src/main/java/hu/bme/mit/theta/xcfa/litmus/cli/LitmusCli.java b/subprojects/xcfa/litmus-cli/src/main/java/hu/bme/mit/theta/xcfa/litmus/cli/LitmusCli.java
@@ -117,16 +117,16 @@ private void run() {
 
         final Stopwatch sw = Stopwatch.createStarted();
         try {
-            final Solver solver = SolverManager.resolveSolverFactory(this.solver).createSolver();
+            try (Solver solver = SolverManager.resolveSolverFactory(this.solver).createSolver()) {
 
-            final MCM mcm = CatDslManager.createMCM(cat);
-            logger.write(Logger.Level.MAINSTEP, "CAT model parsed successfully\n");
-            final XCFA xcfa = LitmusInterpreter.getXcfa(litmus);
-            logger.write(Logger.Level.MAINSTEP, "Litmus test parsed successfully\n");
+                final MCM mcm = CatDslManager.createMCM(cat);
+                logger.write(Logger.Level.MAINSTEP, "CAT model parsed successfully\n");
+                final XCFA xcfa = LitmusInterpreter.getXcfa(litmus);
+                logger.write(Logger.Level.MAINSTEP, "Litmus test parsed successfully\n");
 
-            if (printxcfa) {
-                System.out.println(toDot(xcfa));
-            }
+                if (printxcfa) {
+                    System.out.println(toDot(xcfa));
+                }
 
 //            final List<Integer> processIds = listToRange(processes, -1, -1);
 //
@@ -151,6 +151,7 @@ private void run() {
 //                    mcmSafetyResult.visualize();
 //                }
 //            }
+            }
         } catch (final Throwable t) {
             t.printStackTrace();
             System.exit(-1);
@@ -180,4 +181,4 @@ public static void registerAllSolverManagers(String home, Logger logger) throws
         }
     }
 
-}
+}
diff --git a/.../xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/ExtensionProperty.kt b/.../xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/ExtensionProperty.kt
@@ -25,7 +25,7 @@ fun <R, T> nullableExtension() = NullableExtensionProperty<R, T?>()
 class ExtensionProperty<R, T> : ReadWriteProperty<R, T> {
 
     private val map = IdentityHashMap<R, T>()
-    override fun getValue(thisRef: R, property: KProperty<*>) = map[thisRef]!!
+    override fun getValue(thisRef: R, property: KProperty<*>) = checkNotNull(map[thisRef])
     override fun setValue(thisRef: R, property: KProperty<*>, value: T) {
         map[thisRef] = value
     }

diff --git a/.../xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaDistToErrComparator.java b/.../xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaDistToErrComparator.java
@@ -33,7 +33,8 @@
 import java.util.Map;
 import java.util.Optional;
 
-import static com.google.common.base.Preconditions.*;
+import static com.google.common.base.Preconditions.checkArgument;
+import static com.google.common.base.Preconditions.checkNotNull;
 
 /**
  * A comparator for ArgNodes that is based on the distance from the error
@@ -71,9 +72,12 @@ public int compare(final ArgNode<? extends State, ? extends Action> n1,
     }
 
     private int getWeightedDistance(final ArgNode<? extends State, ? extends Action> node) {
-        checkArgument(node.getState() instanceof XcfaState && ((XcfaState) node.getState()).getProcesses().size() <= 1, "XcfaState expected with a single process.");
-        if (((XcfaState) node.getState()).getProcesses().size() == 0) return Integer.MAX_VALUE;
-        final XcfaState<?> state = (XcfaState<?>) node.getState();
+        final var localState = node.getState();
+        checkArgument(localState instanceof XcfaState && ((XcfaState) localState).getProcesses().size() <= 1, "XcfaState expected with a single process.");
+        if (((XcfaState) localState).getProcesses().size() == 0) {
+            return Integer.MAX_VALUE;
+        }
+        final XcfaState<?> state = (XcfaState<?>) localState;
         final int distanceToError = getDistanceToError(state.getProcesses().get(0).component1().peek());
         if (distanceToError == Integer.MAX_VALUE) {
             return distanceToError;
@@ -119,4 +123,4 @@ static Map<XcfaLocation, Integer> calculateDistancesToError(final XCFA cfa, fina
     public String toString() {
         return getClass().getSimpleName();
     }
-}
+}