Merge remote-tracking branch 'origin/develop'

runtimeverification · Oct 26, 2023 · debf3d0 · debf3d0
2 parents d4bbeb1 + 8334e31
commit debf3d0
Show file tree

Hide file tree

Showing 80 changed files with 158 additions and 212 deletions.
diff --git a/k-distribution/src/test/java/org/kframework/kore/convertors/BaseTest.java b/k-distribution/src/test/java/org/kframework/kore/convertors/BaseTest.java
@@ -54,7 +54,7 @@ protected File testResource(String baseName) {
     }
 
     // WARNING: only use this after checking the results manually
-    private static boolean forceFixAssertionFiles = false;
+    private static final boolean forceFixAssertionFiles = false;
 
     private void testConversion(Function<File, DefinitionWithContext> parse) throws IOException {
         File kilDefinitionFile = testResource("/convertor-tests/" + name.getMethodName() + ".k");

diff --git a/kernel/src/main/java/com/davekoelle/AlphanumComparator.java b/kernel/src/main/java/com/davekoelle/AlphanumComparator.java
@@ -83,8 +83,8 @@ public int compare(String o1, String o2)
         {
             return 0;
         }
-        String s1 = (String)o1;
-        String s2 = (String)o2;
+        String s1 = o1;
+        String s2 = o2;
 
         int thisMarker = 0;
         int thatMarker = 0;

diff --git a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
@@ -953,7 +953,7 @@ private void convertRule(RuleOrClaim rule, int ruleIndex, boolean heatCoolEq, St
         boolean constructorBased = constructorChecks.isConstructorBased(left);
         RuleInfo ruleInfo = getRuleInfo(rule, heatCoolEq, topCellSortStr);
         sb.append("// ");
-        sb.append(rule.toString());
+        sb.append(rule);
         sb.append("\n");
         if (ruleInfo.isCeil && options.disableCeilSimplificationRules) {
           return;
@@ -1561,11 +1561,7 @@ private Att addKoreAttributes(Production prod, SetMultimap<KLabel, Rule> functio
                 colors.append(conn).append(att.get(Att.COLOR()));
                 conn = ",";
               }
-              if (format.charAt(i) == '%') {
-                escape = true;
-              } else {
-                escape = false;
-              }
+                escape = format.charAt(i) == '%';
             }
             att = att.add(Att.COLORS(), colors.toString());
           }
@@ -1608,10 +1604,7 @@ private KList getAssoc(scala.collection.Set<Tuple2<Tag, Tag>> assoc, KLabel klab
     }
 
     private boolean isFunction(Production prod) {
-        if (!prod.att().contains(Att.FUNCTION())) {
-            return false;
-        }
-        return true;
+        return prod.att().contains(Att.FUNCTION());
     }
 
     // Assume that there is no quantifiers

diff --git a/kernel/src/main/java/org/kframework/compile/AddSortInjections.java b/kernel/src/main/java/org/kframework/compile/AddSortInjections.java
@@ -50,7 +50,7 @@ public class AddSortInjections {
     private final ConfigurationInfoFromModule configurationInfo;
 
     private int freshSortParamCounter = 0;
-    private Set<String> sortParams = new HashSet<>();
+    private final Set<String> sortParams = new HashSet<>();
     public static final String SORTPARAM_NAME = "#SortParam";
     private boolean isLHS = false;
 

diff --git a/kernel/src/main/java/org/kframework/compile/Backend.java b/kernel/src/main/java/org/kframework/compile/Backend.java
@@ -17,13 +17,13 @@
  */
 public interface Backend {
 
-    public class Holder {
+    class Holder {
         public CompiledDefinition def;
 
         public Holder(CompiledDefinition def) {
             this.def = def;
         }
-    };
+    }
 
     void accept(Holder def);
 

diff --git a/kernel/src/main/java/org/kframework/compile/CloseCells.java b/kernel/src/main/java/org/kframework/compile/CloseCells.java
@@ -78,7 +78,7 @@ public synchronized Sentence close(Sentence s) {
     }
 
     private int counter = 0;
-    private Set<KVariable> vars = Sets.newHashSet();
+    private final Set<KVariable> vars = Sets.newHashSet();
     private KRewrite rhsOf = null;
 
     void resetVars() {
@@ -173,10 +173,10 @@ protected KApply closeCell(KApply cell) {
                 } else {
                     if (requiredLeft.equals(requiredRight)) {
                         throw KEMException.compilerError("Closed parent cell missing " +
-                                "required children " + requiredLeft.toString(), cell);
+                                "required children " + requiredLeft, cell);
                     } else {
                         throw KEMException.compilerError("Closed parent cell missing " +
-                                "required children " + requiredLeft.toString() + " on left hand side and " + requiredRight.toString() + " on right hand side.", cell);
+                                "required children " + requiredLeft + " on left hand side and " + requiredRight + " on right hand side.", cell);
                     }
                 }
             }
@@ -206,15 +206,15 @@ protected KApply closeCell(KApply cell) {
         // Is a leaf cell
         if (contents.size() != 1) {
             throw KEMException.criticalError("Leaf cells should contain exactly 1 body term,"
-                    + " but there are " + contents.size() + " in " + cell.toString());
+                    + " but there are " + contents.size() + " in " + cell);
         }
 
         if (!openLeft && !openRight) {
             return KApply(label, KList(contents.get(0)));
         }
         if (rhsOf != null) {
             throw KEMException.criticalError("Leaf cells on right hand side of a rewrite" +
-                    " may not be open, but " + cell.toString() + " is right of " + rhsOf.toString());
+                    " may not be open, but " + cell + " is right of " + rhsOf.toString());
         }
 
         K body = contents.get(0);
@@ -244,14 +244,14 @@ protected KApply closeCell(KApply cell) {
             KLabel closeOperator = sortInfo.getCloseOperator(cellType);
             if (closeOperator == null) {
                 throw KEMException.criticalError("No operator registered for closing cells of sort "
-                        + cellType.toString() + " when closing cell " + cell.toString());
+                        + cellType + " when closing cell " + cell);
             }
             LabelInfo.AssocInfo info = labelInfo.getAssocInfo(closeOperator);
             if (!info.isAssoc() && openLeft && openRight) {
                 throw KEMException.criticalError(
-                        "Ambiguity closing a cell. Operator " + closeOperator.toString()
-                                + " for sort " + cellType.toString() + " is not associative, "
-                                + "but the cell has ellipses on both sides " + cell.toString());
+                        "Ambiguity closing a cell. Operator " + closeOperator
+                                + " for sort " + cellType + " is not associative, "
+                                + "but the cell has ellipses on both sides " + cell);
             }
             if (info.isComm() && (!openLeft || !openRight || info.isAssoc())) {
                 openLeft = false;

diff --git a/kernel/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java b/kernel/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java
@@ -106,5 +106,5 @@ public Set<KLabel> ancestors(Set<KLabel> labels) {
         return ancestors(labels, dependencies);
     }
 
-    private DirectedGraph<KLabel, Object> dependencies;
+    private final DirectedGraph<KLabel, Object> dependencies;
 }
diff --git a/kernel/src/main/java/org/kframework/compile/ConvertDataStructureToLookup.java b/kernel/src/main/java/org/kframework/compile/ConvertDataStructureToLookup.java
@@ -79,8 +79,8 @@
 public class ConvertDataStructureToLookup {
 
 
-    private Set<KApply> state = new HashSet<>();
-    private Multiset<KVariable> vars = HashMultiset.create();
+    private final Set<KApply> state = new HashSet<>();
+    private final Multiset<KVariable> vars = HashMultiset.create();
 
     void reset() {
         state.clear();
@@ -223,7 +223,7 @@ private Stream<KApply> getSortedLookups() {
                     }
                 }
             }
-        };
+        }
         List<KApply> topologicalSorted = mutable(TopologicalSort.tsort(immutable(edges)).toList());
         return state.stream().sorted((k1, k2) -> (topologicalSorted.indexOf(k1) - topologicalSorted.indexOf(k2)));
     }

diff --git a/kernel/src/main/java/org/kframework/compile/DeconstructIntegerAndFloatLiterals.java b/kernel/src/main/java/org/kframework/compile/DeconstructIntegerAndFloatLiterals.java
@@ -28,8 +28,8 @@
  */
 public class DeconstructIntegerAndFloatLiterals {
 
-    private Set<KApply> state = new HashSet<>();
-    private Set<KVariable> vars = new HashSet<>();
+    private final Set<KApply> state = new HashSet<>();
+    private final Set<KVariable> vars = new HashSet<>();
 
     void reset() {
         state.clear();

diff --git a/kernel/src/main/java/org/kframework/compile/ExpandMacros.java b/kernel/src/main/java/org/kframework/compile/ExpandMacros.java
@@ -128,7 +128,7 @@ private boolean isMacro(Att att, boolean reverse) {
         return att.contains(Att.ALIAS_REC()) || att.contains(Att.ALIAS()) || (!reverse && (att.contains(Att.MACRO()) || att.contains(Att.MACRO_REC())));
     }
 
-    private Set<KVariable> vars = new HashSet<>();
+    private final Set<KVariable> vars = new HashSet<>();
 
     void resetVars() {
         vars.clear();
@@ -250,7 +250,7 @@ private <T extends K> K applyMacros(T k, List<Rule> rules, Function<T, K> superA
                         final Map<KVariable, K> subst = new HashMap<>();
                         if (match(subst, left, applied, r) && (r.att().contains(Att.MACRO_REC()) || r.att().contains(Att.ALIAS_REC()) || !appliedRules.contains(r))) {
                             if (cover) {
-                                if (!r.att().contains(Att.UNIQUE_ID())) System.out.println(r.toString());
+                                if (!r.att().contains(Att.UNIQUE_ID())) System.out.println(r);
                                 coverage.println(r.att().get(Att.UNIQUE_ID()));
                             }
                             Set<Rule> oldAppliedRules = appliedRules;

diff --git a/kernel/src/main/java/org/kframework/compile/FloatBuiltin.java b/kernel/src/main/java/org/kframework/compile/FloatBuiltin.java
@@ -14,7 +14,7 @@
 public class FloatBuiltin {
 
     /* Token cache */
-    private static Map<Pair<BigFloat, Integer>, FloatBuiltin> tokenCache = new HashMap<>();
+    private static final Map<Pair<BigFloat, Integer>, FloatBuiltin> tokenCache = new HashMap<>();
 
     /**
      * Returns a {@link FloatBuiltin} representing the given {@link BigFloat} value
@@ -73,7 +73,7 @@ private FloatBuiltin(BigFloat value, int exponent) {
         this.exponent = exponent;
     }
 
-    private static Pattern precisionAndExponent = Pattern.compile("(.*)[pP](\\d+)[xX](\\d+)");
+    private static final Pattern precisionAndExponent = Pattern.compile("(.*)[pP](\\d+)[xX](\\d+)");
     public static Pair<BigFloat, Integer> parseKFloat(String s) {
         try {
             Matcher m = precisionAndExponent.matcher(s);
@@ -187,10 +187,7 @@ public boolean equals(Object object) {
         if (!value.equals(other.value)) {
             return false;
         }
-        if (exponent != other.exponent) {
-            return false;
-        }
-        return true;
+        return exponent == other.exponent;
     }
 
     @Override

diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java b/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java
@@ -277,7 +277,7 @@ public K apply(KToken k) {
         }.apply(leafContents), h.sentences);
     }
 
-    private static KVariable INIT = KVariable("Init", Att.empty().add(Sort.class, Sorts.Map()));
+    private static final KVariable INIT = KVariable("Init", Att.empty().add(Sort.class, Sorts.Map()));
 
     /**
      * Generates the sentences associated with a particular cell.
@@ -398,8 +398,8 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
                     fragmentItems.add(NonTerminal(childOptSort));
 
                     sentences.add(Production(Seq(), childOptSort, List(NonTerminal(childSort))));
-                    if (!m.definedKLabels().contains(KLabel("no"+childSort.toString()))) {
-                        sentences.add(Production(KLabel("no"+childSort.toString()), childOptSort, List(Terminal("no"+childSort.toString())),
+                    if (!m.definedKLabels().contains(KLabel("no" + childSort))) {
+                        sentences.add(Production(KLabel("no" + childSort), childOptSort, List(Terminal("no" + childSort)),
                                 Att().add(Att.CELL_OPT_ABSENT(),Sort.class,childSort)));
                     }
                 }

diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSortPredicateRules.java b/kernel/src/main/java/org/kframework/compile/GenerateSortPredicateRules.java
@@ -49,11 +49,11 @@ public Module gen(Module mod) {
 
     private Stream<? extends Sentence> gen(Sort sort) {
         if (sort.equals(Sorts.K())) {
-            return Stream.of(Rule(KRewrite(KApply(KLabel("is" + sort.toString()), KVariable("K")), BooleanUtils.TRUE), BooleanUtils.TRUE, BooleanUtils.TRUE));
+            return Stream.of(Rule(KRewrite(KApply(KLabel("is" + sort), KVariable("K")), BooleanUtils.TRUE), BooleanUtils.TRUE, BooleanUtils.TRUE));
         } else {
             List<Sentence> res = new ArrayList<>();
-            res.add(Rule(KRewrite(KApply(KLabel("is" + sort.toString()), KVariable(sort.name(), Att().add(Sort.class, sort))), BooleanUtils.TRUE), BooleanUtils.TRUE, BooleanUtils.TRUE));
-            res.add(Rule(KRewrite(KApply(KLabel("is" + sort.toString()), KVariable("K")), BooleanUtils.FALSE), BooleanUtils.TRUE, BooleanUtils.TRUE, Att().add(Att.OWISE())));
+            res.add(Rule(KRewrite(KApply(KLabel("is" + sort), KVariable(sort.name(), Att().add(Sort.class, sort))), BooleanUtils.TRUE), BooleanUtils.TRUE, BooleanUtils.TRUE));
+            res.add(Rule(KRewrite(KApply(KLabel("is" + sort), KVariable("K")), BooleanUtils.FALSE), BooleanUtils.TRUE, BooleanUtils.TRUE, Att().add(Att.OWISE())));
             return res.stream();
         }
     }

diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSortPredicateSyntax.java b/kernel/src/main/java/org/kframework/compile/GenerateSortPredicateSyntax.java
@@ -34,7 +34,7 @@ public Module gen(Module mod) {
 
     public Set<Sentence> gen(Module mod, Sort sort) {
         Production prod = Production(KLabel("is" + sort.toString()), Sorts.Bool(),
-                Seq(Terminal("is" + sort.toString()), Terminal("("), NonTerminal(Sorts.K()), Terminal(")")),
+                Seq(Terminal("is" + sort), Terminal("("), NonTerminal(Sorts.K()), Terminal(")")),
                 Att().add(Att.FUNCTION()).add(Att.TOTAL()).add(Att.PREDICATE(), Sort.class, sort));
         if (!mod.productions().contains(prod))
             return Collections.singleton(prod);

diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSortProjections.java b/kernel/src/main/java/org/kframework/compile/GenerateSortProjections.java
@@ -69,7 +69,7 @@ public Stream<? extends Sentence> gen(Sort sort) {
         }
         Production prod = Production(lbl, sort, Seq(Terminal(lbl.name()), Terminal("("), NonTerminal(Sorts.K()), Terminal(")")), Att().add(Att.FUNCTION()).add(Att.PROJECTION()));
         if (cover) {
-            KLabel sideEffectLbl = KLabel("sideEffect:" + sort.toString());
+            KLabel sideEffectLbl = KLabel("sideEffect:" + sort);
             Production sideEffect = Production(sideEffectLbl, sort, Seq(Terminal(sideEffectLbl.name()), Terminal("("), NonTerminal(Sorts.K()), Terminal(","), NonTerminal(sort), Terminal(")")), Att().add(Att.FUNCTION()));
             Rule sideEffectR = Rule(KRewrite(KApply(sideEffectLbl, KVariable("K2", Att.empty().add(Sort.class, Sorts.K())), var), var), BooleanUtils.TRUE, BooleanUtils.TRUE);
             return stream(Set(prod, r, sideEffect, sideEffectR));

diff --git a/kernel/src/main/java/org/kframework/compile/GuardOrPatterns.java b/kernel/src/main/java/org/kframework/compile/GuardOrPatterns.java
@@ -18,7 +18,7 @@
 
 public class GuardOrPatterns {
 
-    private Set<KVariable> vars = new HashSet<>();
+    private final Set<KVariable> vars = new HashSet<>();
 
     void resetVars() {
         vars.clear();
@@ -47,7 +47,7 @@ private Context resolve(Module m, Context context) {
     }
 
     public K resolveK(Module m, K k) {
-        resetVars();;
+        resetVars();
         gatherVars(k);
         return transform(k, m);
     }

diff --git a/kernel/src/main/java/org/kframework/compile/PropagateMacro.java b/kernel/src/main/java/org/kframework/compile/PropagateMacro.java
@@ -15,7 +15,7 @@
 public record PropagateMacro(Module m) {
 
     public Sentence propagate(Sentence s) {
-        if (s instanceof Rule && m.ruleLhsHasMacroKLabel((Rule) s) && !((Rule) s).att().contains(Att.SIMPLIFICATION())) {
+        if (s instanceof Rule && m.ruleLhsHasMacroKLabel((Rule) s) && !s.att().contains(Att.SIMPLIFICATION())) {
             Att macroAtt = m.attributesFor().apply(m.matchKLabel((Rule) s));
             return Rule.apply(((Rule) s).body(), ((Rule) s).requires(), ((Rule) s).ensures(), s.att().add(macroAtt.getMacro().get()));
         }

diff --git a/kernel/src/main/java/org/kframework/compile/RefreshRules.java b/kernel/src/main/java/org/kframework/compile/RefreshRules.java
@@ -28,7 +28,7 @@ public class RefreshRules {
 
     private final Set<String> avoidVars;
     private int counter = 0;
-    private Map<KVariable, String> vars = new HashMap<>();
+    private final Map<KVariable, String> vars = new HashMap<>();
 
     public RefreshRules(Set<String> avoidVars) {
         this.avoidVars = avoidVars;

diff --git a/kernel/src/main/java/org/kframework/compile/ResolveAnonVar.java b/kernel/src/main/java/org/kframework/compile/ResolveAnonVar.java
@@ -35,7 +35,7 @@ public static boolean isAnonVarOrNamedAnonVar(KVariable var) {
     }
 
 
-    private Set<KVariable> vars = new HashSet<>();
+    private final Set<KVariable> vars = new HashSet<>();
 
     void resetVars() {
         vars.clear();
@@ -75,7 +75,7 @@ private ContextAlias resolve(ContextAlias context) {
     }
 
     public K resolveK(K k) {
-        resetVars();;
+        resetVars();
         gatherVars(k);
         return transform(k);
     }

diff --git a/kernel/src/main/java/org/kframework/compile/ResolveContexts.java b/kernel/src/main/java/org/kframework/compile/ResolveContexts.java
@@ -91,8 +91,8 @@ private Stream<? extends Sentence> resolve(Context context, Module input) {
         K requiresHeat = context.requires();
         K requiresCool = BooleanUtils.TRUE;
 
-        int currentHolePosition[] = new int[] { 0 };
-        int finalHolePosition[] = new int[] { 0 };
+        int[] currentHolePosition = new int[] { 0 };
+        int[] finalHolePosition = new int[] { 0 };
         // does this context have a main cell?
         boolean hasMainCell = new FoldK<Boolean>() {
             @Override

diff --git a/kernel/src/main/java/org/kframework/compile/ResolveFreshConfigConstants.java b/kernel/src/main/java/org/kframework/compile/ResolveFreshConfigConstants.java
@@ -22,7 +22,7 @@
 
 public class ResolveFreshConfigConstants {
     private int currentFresh = 0;
-    private Map<KVariable, Integer> freshMap = new HashMap<>();
+    private final Map<KVariable, Integer> freshMap = new HashMap<>();
 
     /**
      * Replaces fresh variables in the RHS of cell initializer rules with a fresh constant.

diff --git a/kernel/src/main/java/org/kframework/compile/ResolveFreshConstants.java b/kernel/src/main/java/org/kframework/compile/ResolveFreshConstants.java
@@ -49,10 +49,10 @@ public class ResolveFreshConstants {
     private final Definition def;
     private final FileUtil files;
     private Module m;
-    private java.util.Set<KVariable> freshVars = new HashSet<>();
-    private Map<KVariable, Integer> offsets = new HashMap<>();
+    private final java.util.Set<KVariable> freshVars = new HashSet<>();
+    private final Map<KVariable, Integer> offsets = new HashMap<>();
     private final String manualTopCell;
-    private int initialFresh;
+    private final int initialFresh;
 
     private void reset() {
         freshVars.clear();
@@ -123,7 +123,7 @@ private void finishAnalysis() {
         }
     }
 
-    private static KVariable FRESH = KVariable("#Fresh", Att.empty().add(Sort.class, Sorts.Int()));
+    private static final KVariable FRESH = KVariable("#Fresh", Att.empty().add(Sort.class, Sorts.Int()));
 
     private K transform(K term) {
         return new TransformK() {

diff --git a/kernel/src/main/java/org/kframework/compile/ResolveFunctionWithConfig.java b/kernel/src/main/java/org/kframework/compile/ResolveFunctionWithConfig.java
@@ -76,10 +76,7 @@ public Boolean apply(KVariable k) {
                 return k.name().startsWith("!") || k.name().equals("#Configuration");
             }
         };
-        if (hasVarNeedsConfig.apply(RewriteToTop.toRight(r.body())) || hasVarNeedsConfig.apply(r.requires()) || hasVarNeedsConfig.apply(r.ensures())) {
-            return true;
-        }
-        return false;
+        return hasVarNeedsConfig.apply(RewriteToTop.toRight(r.body())) || hasVarNeedsConfig.apply(r.requires()) || hasVarNeedsConfig.apply(r.ensures());
     }
 
     public RuleOrClaim resolve(RuleOrClaim rule, Module m) {

diff --git a/kernel/src/main/java/org/kframework/compile/ResolveIOStreams.java b/kernel/src/main/java/org/kframework/compile/ResolveIOStreams.java
@@ -103,7 +103,7 @@ private void checkStreamName(String streamName) {
 
         if (!streams.contains(streamName)) {
             throw KEMException.compilerError("Make sure you give the correct stream names: " + streamName +
-                    "\nIt should be one of " + streams.toString());
+                    "\nIt should be one of " + streams);
         }
     }