Position information overhaul (#3049)

* Removes most manual passing of line, column and replaces it with `Location` * [Fix issue dialog pointing to the wrong line (at least on Windows)](9894f7a) * Fix many positioning issues coming from 0-based/1-based columns/lines * Fix position information of block contracts and the like Blocking on #3034. There are some usages in the `PrettyPrinter` I won't fix since it's deleted there. [Artiweb](https://keyproject.github.io/artiweb/3049/)
KeYProject · Mar 11, 2023 · 08c08a6 · 08c08a6
2 parents e0d78c6 + 0a8760c
commit 08c08a6
Show file tree

Hide file tree

Showing 190 changed files with 1,767 additions and 5,464 deletions.
diff --git a/...e.proof_references/src/main/java/de/uka/ilkd/key/proof_references/ProofReferenceUtil.java b/...e.proof_references/src/main/java/de/uka/ilkd/key/proof_references/ProofReferenceUtil.java
@@ -1,23 +1,16 @@
 package de.uka.ilkd.key.proof_references;
 
-import java.util.LinkedHashSet;
-
-import org.key_project.util.collection.ImmutableList;
-import org.key_project.util.collection.ImmutableSLList;
-import org.key_project.util.java.CollectionUtil;
-import org.key_project.util.java.IFilter;
-
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.ProofVisitor;
-import de.uka.ilkd.key.proof_references.analyst.ClassAxiomAndInvariantProofReferencesAnalyst;
-import de.uka.ilkd.key.proof_references.analyst.ContractProofReferencesAnalyst;
-import de.uka.ilkd.key.proof_references.analyst.IProofReferencesAnalyst;
-import de.uka.ilkd.key.proof_references.analyst.MethodBodyExpandProofReferencesAnalyst;
-import de.uka.ilkd.key.proof_references.analyst.MethodCallProofReferencesAnalyst;
-import de.uka.ilkd.key.proof_references.analyst.ProgramVariableReferencesAnalyst;
+import de.uka.ilkd.key.proof_references.analyst.*;
 import de.uka.ilkd.key.proof_references.reference.IProofReference;
+import org.key_project.util.collection.ImmutableList;
+import org.key_project.util.collection.ImmutableSLList;
+import org.key_project.util.java.CollectionUtil;
+
+import java.util.LinkedHashSet;
 
 /**
  * <p>
@@ -38,7 +31,7 @@
  *
  * @author Martin Hentschel
  * @see IProofReference
- * @see IProofReferencesAnalyst.
+ * @see IProofReferencesAnalyst
  */
 public final class ProofReferenceUtil {
     /**
@@ -96,31 +89,31 @@ public static LinkedHashSet<IProofReference<?>> computeProofReferences(Proof pro
             proof.breadthFirstSearch(proof.root(), visitor);
             return visitor.getResult();
         } else {
-            return new LinkedHashSet<IProofReference<?>>();
+            return new LinkedHashSet<>();
         }
     }
 
     /**
-     * Utility class used by
-     * {@link KeyProofReferenceUtil#analyzeProof(KeyConnection, Services, Proof)}.
+     * Utility class used by {@link ProofReferenceUtil}.
      *
      * @author Martin Hentschel
      */
     private static class ReferenceAnalaystProofVisitor implements ProofVisitor {
         /**
          * The {@link Services} to use.
          */
-        private Services services;
+        private final Services services;
 
         /**
          * The {@link IProofReferencesAnalyst}s to use.
          */
-        private ImmutableList<IProofReferencesAnalyst> analysts;
+        private final ImmutableList<IProofReferencesAnalyst> analysts;
 
         /**
          * The result.
          */
-        private LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<IProofReference<?>>();
+        private final LinkedHashSet<IProofReference<?>> result =
+            new LinkedHashSet<IProofReference<?>>();
 
         /**
          * Constructor.
@@ -209,14 +202,9 @@ public static void merge(LinkedHashSet<IProofReference<?>> target,
     public static void merge(LinkedHashSet<IProofReference<?>> target,
             final IProofReference<?> reference) {
         if (!target.add(reference)) {
-            // Reference exist before, so merge nodes of both references.
+            // Reference exists before, so merge nodes of both references.
             IProofReference<?> existingFirst =
-                CollectionUtil.search(target, new IFilter<IProofReference<?>>() {
-                    @Override
-                    public boolean select(IProofReference<?> element) {
-                        return element.equals(reference);
-                    }
-                });
+                CollectionUtil.search(target, element -> element.equals(reference));
             existingFirst.addNodes(reference.getNodes());
         }
     }

diff --git a/...ences/src/main/java/de/uka/ilkd/key/proof_references/reference/DefaultProofReference.java b/...ences/src/main/java/de/uka/ilkd/key/proof_references/reference/DefaultProofReference.java
@@ -1,13 +1,12 @@
 package de.uka.ilkd.key.proof_references.reference;
 
-import java.util.Collection;
-import java.util.LinkedHashSet;
-
-import org.key_project.util.java.ObjectUtil;
-
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 
+import java.util.Collection;
+import java.util.LinkedHashSet;
+import java.util.Objects;
+
 /**
  * Default implementation of {@link IProofReference}.
  *
@@ -95,9 +94,9 @@ public Proof getSource() {
     public boolean equals(Object obj) {
         if (obj instanceof IProofReference<?>) {
             IProofReference<?> other = (IProofReference<?>) obj;
-            return ObjectUtil.equals(getKind(), other.getKind())
-                    && ObjectUtil.equals(getSource(), other.getSource())
-                    && ObjectUtil.equals(getTarget(), other.getTarget());
+            return Objects.equals(getKind(), other.getKind())
+                    && Objects.equals(getSource(), other.getSource())
+                    && Objects.equals(getTarget(), other.getTarget());
         } else {
             return false;
         }

diff --git a/...c/test/java/de/uka/ilkd/key/proof_references/testcase/AbstractProofReferenceTestCase.java b/...c/test/java/de/uka/ilkd/key/proof_references/testcase/AbstractProofReferenceTestCase.java
@@ -24,12 +24,12 @@
 import org.key_project.util.collection.ImmutableSet;
 import org.key_project.util.helper.FindResources;
 import org.key_project.util.java.CollectionUtil;
-import org.key_project.util.java.IFilter;
 
 import java.io.File;
 import java.util.HashMap;
 import java.util.Iterator;
 import java.util.LinkedHashSet;
+import java.util.function.Predicate;
 
 import static org.junit.jupiter.api.Assertions.*;
 
@@ -74,13 +74,13 @@ protected void doReferenceFunctionTest(File baseDir, String javaPathInBaseDir,
      * @param targetName The target name to search.
      * @param useContracts Use contracts or inline method bodies instead.
      * @param analyst The {@link IProofReferencesAnalyst} to use.
-     * @param currentReferenceFilter An optional {@link IFilter} to limit the references to test.
+     * @param currentReferenceFilter An optional {@link Predicate} to limit the references to test.
      * @param expectedReferences The expected proof references.
      * @throws Exception Occurred Exception.
      */
     protected void doReferenceFunctionTest(File baseDir, String javaPathInBaseDir,
             String containerTypeName, String targetName, boolean useContracts,
-            IProofReferencesAnalyst analyst, IFilter<IProofReference<?>> currentReferenceFilter,
+            IProofReferencesAnalyst analyst, Predicate<IProofReference<?>> currentReferenceFilter,
             ExpectedProofReferences... expectedReferences) throws Exception {
         IProofTester tester =
             createReferenceMethodTester(analyst, currentReferenceFilter, expectedReferences);
@@ -117,13 +117,13 @@ protected void doReferenceMethodTest(File baseDir, String javaPathInBaseDir,
      * @param methodFullName The method name to search.
      * @param useContracts Use contracts or inline method bodies instead.
      * @param analyst The {@link IProofReferencesAnalyst} to use.
-     * @param currentReferenceFilter An optional {@link IFilter} to limit the references to test.
+     * @param currentReferenceFilter An optional {@link Predicate} to limit the references to test.
      * @param expectedReferences The expected proof references.
      * @throws Exception Occurred Exception.
      */
     protected void doReferenceMethodTest(File baseDir, String javaPathInBaseDir,
             String containerTypeName, String methodFullName, boolean useContracts,
-            IProofReferencesAnalyst analyst, IFilter<IProofReference<?>> currentReferenceFilter,
+            IProofReferencesAnalyst analyst, Predicate<IProofReference<?>> currentReferenceFilter,
             ExpectedProofReferences... expectedReferences) throws Exception {
         IProofTester tester =
             createReferenceMethodTester(analyst, currentReferenceFilter, expectedReferences);
@@ -137,12 +137,12 @@ protected void doReferenceMethodTest(File baseDir, String javaPathInBaseDir,
      * {@link #doProofMethodTest(File, String, String, String, boolean, IProofTester)}.
      *
      * @param analyst The {@link IProofReferencesAnalyst} to use.
-     * @param currentReferenceFilter An optional {@link IFilter} to limit the references to test.
+     * @param currentReferenceFilter An optional {@link Predicate} to limit the references to test.
      * @param expectedReferences The expected proof references.
      * @return The created {@link IProofTester}.
      */
     protected IProofTester createReferenceMethodTester(final IProofReferencesAnalyst analyst,
-            final IFilter<IProofReference<?>> currentReferenceFilter,
+            final Predicate<IProofReference<?>> currentReferenceFilter,
             final ExpectedProofReferences... expectedReferences) {
         return (environment, proof) -> {
             // Compute proof references
@@ -157,7 +157,7 @@ protected IProofTester createReferenceMethodTester(final IProofReferencesAnalyst
                 LinkedHashSet<IProofReference<?>> filteredReferences =
                     new LinkedHashSet<IProofReference<?>>();
                 for (IProofReference<?> reference : references) {
-                    if (currentReferenceFilter.select(reference)) {
+                    if (currentReferenceFilter.test(reference)) {
                         filteredReferences.add(reference);
                     }
                 }

diff --git a/...cution/src/main/java/de/uka/ilkd/key/rule/label/BlockContractValidityTermLabelUpdate.java b/...cution/src/main/java/de/uka/ilkd/key/rule/label/BlockContractValidityTermLabelUpdate.java
@@ -1,13 +1,5 @@
 package de.uka.ilkd.key.rule.label;
 
-import java.util.Set;
-
-import org.key_project.util.collection.ImmutableArray;
-import org.key_project.util.collection.ImmutableList;
-import org.key_project.util.collection.ImmutableSLList;
-import org.key_project.util.java.CollectionUtil;
-import org.key_project.util.java.IFilter;
-
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.JavaBlock;
 import de.uka.ilkd.key.logic.Name;
@@ -23,6 +15,12 @@
 import de.uka.ilkd.key.rule.Rule;
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
+import org.key_project.util.collection.ImmutableArray;
+import org.key_project.util.collection.ImmutableList;
+import org.key_project.util.collection.ImmutableSLList;
+import org.key_project.util.java.CollectionUtil;
+
+import java.util.Set;
 
 /**
  * Makes sure that {@link BlockContractValidityTermLabel} is introduced when a
@@ -52,12 +50,8 @@ public void updateLabels(TermLabelState state, Services services,
                 && ((BlockContractInternalRule.BlockContractHint) hint)
                         .getExceptionalVariable() != null
                 && SymbolicExecutionUtil.hasSymbolicExecutionLabel(modalityTerm)) {
-            if (CollectionUtil.search(labels, new IFilter<TermLabel>() {
-                @Override
-                public boolean select(TermLabel element) {
-                    return element instanceof BlockContractValidityTermLabel;
-                }
-            }) == null) {
+            if (CollectionUtil.search(labels,
+                element -> element instanceof BlockContractValidityTermLabel) == null) {
                 labels.add(new BlockContractValidityTermLabel(
                     ((BlockContractInternalRule.BlockContractHint) hint).getExceptionalVariable()));
             }

diff --git a/...bolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java b/...bolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java
@@ -1,17 +1,7 @@
 package de.uka.ilkd.key.rule.label;
 
-import java.util.*;
-
-import org.key_project.util.collection.ImmutableList;
-import org.key_project.util.java.CollectionUtil;
-import org.key_project.util.java.IFilter;
-
 import de.uka.ilkd.key.java.Services;
-import de.uka.ilkd.key.logic.Name;
-import de.uka.ilkd.key.logic.PosInOccurrence;
-import de.uka.ilkd.key.logic.Sequent;
-import de.uka.ilkd.key.logic.SequentFormula;
-import de.uka.ilkd.key.logic.Term;
+import de.uka.ilkd.key.logic.*;
 import de.uka.ilkd.key.logic.label.FormulaTermLabel;
 import de.uka.ilkd.key.logic.label.TermLabel;
 import de.uka.ilkd.key.logic.label.TermLabelState;
@@ -21,6 +11,10 @@
 import de.uka.ilkd.key.rule.SyntacticalReplaceVisitor;
 import de.uka.ilkd.key.rule.merge.CloseAfterMerge;
 import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil;
+import org.key_project.util.collection.ImmutableList;
+import org.key_project.util.java.CollectionUtil;
+
+import java.util.*;
 
 /**
  * The {@link TermLabelRefactoring} used to label predicates with a {@link FormulaTermLabel} on
@@ -249,12 +243,7 @@ protected void refactorBewlowUpdates(PosInOccurrence applicationPosInOccurrence,
     protected void refactorSequentFormulas(TermLabelState state, Services services, final Term term,
             List<TermLabel> labels) {
         Set<SequentFormula> sequentFormulas = getSequentFormulasToRefactor(state);
-        if (CollectionUtil.search(sequentFormulas, new IFilter<SequentFormula>() {
-            @Override
-            public boolean select(SequentFormula element) {
-                return element.formula() == term;
-            }
-        }) != null) {
+        if (CollectionUtil.search(sequentFormulas, element -> element.formula() == term) != null) {
             FormulaTermLabel termLabel = (FormulaTermLabel) term.getLabel(FormulaTermLabel.NAME);
             if (termLabel != null) {
                 labels.remove(termLabel);

diff --git a/...e.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java b/...e.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java
@@ -1,22 +1,7 @@
 package de.uka.ilkd.key.rule.label;
 
-import java.util.Collections;
-import java.util.LinkedHashMap;
-import java.util.Map;
-import java.util.Map.Entry;
-import java.util.Set;
-
-import org.key_project.util.collection.ImmutableArray;
-import org.key_project.util.collection.ImmutableList;
-import org.key_project.util.java.CollectionUtil;
-import org.key_project.util.java.IFilter;
-
 import de.uka.ilkd.key.java.Services;
-import de.uka.ilkd.key.logic.JavaBlock;
-import de.uka.ilkd.key.logic.Name;
-import de.uka.ilkd.key.logic.PosInOccurrence;
-import de.uka.ilkd.key.logic.SequentFormula;
-import de.uka.ilkd.key.logic.Term;
+import de.uka.ilkd.key.logic.*;
 import de.uka.ilkd.key.logic.label.FormulaTermLabel;
 import de.uka.ilkd.key.logic.label.TermLabel;
 import de.uka.ilkd.key.logic.label.TermLabelManager;
@@ -30,6 +15,15 @@
 import de.uka.ilkd.key.rule.Taclet.TacletLabelHint.TacletOperation;
 import de.uka.ilkd.key.rule.TacletApp;
 import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil;
+import org.key_project.util.collection.ImmutableArray;
+import org.key_project.util.collection.ImmutableList;
+import org.key_project.util.java.CollectionUtil;
+
+import java.util.Collections;
+import java.util.LinkedHashMap;
+import java.util.Map;
+import java.util.Map.Entry;
+import java.util.Set;
 
 /**
  * The {@link TermLabelUpdate} used to label predicates with a {@link FormulaTermLabel} of add
@@ -117,11 +111,7 @@ public void updateLabels(TermLabelState state, Services services,
      * @return The found {@link TermLabel} or {@code} null if no element was found.
      */
     protected TermLabel getTermLabel(Set<TermLabel> labels, final Name name) {
-        return CollectionUtil.search(labels, new IFilter<TermLabel>() {
-            @Override
-            public boolean select(TermLabel element) {
-                return element != null && element.name().equals(name);
-            }
-        });
+        return CollectionUtil.search(labels,
+            element -> element != null && element.name().equals(name));
     }
 }