KeY 2.12.2 Summary PR (#3328)

It contains the following fixes: #3323,#3287 Z3 QF #3326 ClassCastException in LogicPrinter #3307 Fix Nullable/non_null modifier model methods #3312 Corrupt Term...Indexes #3343 Fix stuck CounterExample Dialog #3344 Fix consistency of proof status and tasktree icon
KeYProject · Nov 10, 2023 · 7de8f96 · 7de8f96
2 parents d750928 + 4f5a25b
commit 7de8f96
Show file tree

Hide file tree

Showing 23 changed files with 321 additions and 348 deletions.
diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties
@@ -1,5 +1,5 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-8.1.1-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.4-bin.zip
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists
diff --git a/...xecution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java b/...xecution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java
@@ -6,7 +6,6 @@
 import java.util.LinkedHashSet;
 import java.util.List;
 import java.util.Set;
-import javax.annotation.Nonnull;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.Name;
@@ -133,7 +132,6 @@ public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) {
     /**
      * {@inheritDoc}
      */
-    @Nonnull
     @Override
     public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
             throws RuleAbortException {

diff --git a/...gen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractCounterExampleGenerator.java b/...gen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractCounterExampleGenerator.java
@@ -68,14 +68,12 @@ public void searchCounterExample(UserInterfaceControl ui, Proof oldProof, Sequen
             throw new IllegalStateException(
                 "Can't find SMT solver " + SolverTypes.Z3_CE_SOLVER.getName());
         }
-
         final Proof proof =
             createProof(ui, oldProof, oldSequent, "Semantics Blasting: " + oldProof.name());
         final SemanticsBlastingMacro macro = new SemanticsBlastingMacro();
         TaskFinishedInfo info = ProofMacroFinishedInfo.getDefaultInfo(macro, proof);
         final ProverTaskListener ptl = ui.getProofControl().getDefaultProverTaskListener();
         ptl.taskStarted(new DefaultTaskStartedInfo(TaskKind.Macro, macro.getName(), 0));
-
         try {
             synchronized (macro) { // TODO: Useless? No other thread has access to macro wait for
                                    // macro to terminate
@@ -99,8 +97,6 @@ public void searchCounterExample(UserInterfaceControl ui, Proof oldProof, Sequen
         solvers.add(SolverTypes.Z3_CE_SOLVER);
 
         launcher.launch(solvers, SMTProblem.createSMTProblems(proof), proof.getServices());
-
-
     }
 
     /**

diff --git a/key.core/build.gradle b/key.core/build.gradle
@@ -71,6 +71,10 @@ task generateSMTListings {
     def resourcesDir = "${project.projectDir}/src/main/resources"
     def outputDir = resourcesDir // in the future that should be "${project.buildDir}/resources/main"
     // ${project.buildDir}
+    inputs.files fileTree("$resourcesDir/$pack", {
+        exclude "$resourcesDir/$pack/DefinedSymbolsHandler.preamble.xml"
+    })
+    outputs.files file("$outputDir/$pack/DefinedSymbolsHandler.preamble.xml")
     doLast {
         new File("$outputDir/$pack/DefinedSymbolsHandler.preamble.xml").withWriter { list ->
             list.writeLine '<?xml version="1.0" encoding="UTF-8" standalone="no"?>'
@@ -92,6 +96,10 @@ task generateSolverPropsList {
     def resourcesDir = "${project.projectDir}/src/main/resources"
     def outputDir = resourcesDir // in the future that should be "${project.buildDir}/resources/main"
     // ${project.buildDir}
+    inputs.files fileTree("$outputDir/$pack/", {
+        exclude "./solvers.txt"
+    })
+    outputs.files file("$outputDir/$pack/solvers.txt")
     doLast {
         def list = []
         def dir = new File("$outputDir/$pack/")
@@ -101,14 +109,12 @@ task generateSolverPropsList {
             }
         })
         list.sort()
-        if (!file("$outputDir/$pack/solvers.txt").exists()) {
-            String files = ''
-            for (String propsFile : list) {
-                files += propsFile + System.lineSeparator()
-            }
-            new File("$outputDir/$pack/solvers.txt").withWriter { listSolvers ->
-                listSolvers.write files
-            }
+        String files = ''
+        for (String propsFile : list) {
+            files += propsFile + System.lineSeparator()
+        }
+        new File("$outputDir/$pack/solvers.txt").withWriter { listSolvers ->
+            listSolvers.write files
         }
     }
 }
@@ -196,7 +202,7 @@ static def gitRevParse(String args) {
 }
 
 // @AW: Say something here. From POV this explain by itself.
-processResources.dependsOn generateVersionFiles
+processResources.dependsOn generateVersionFiles, generateSolverPropsList, generateSMTListings
 
 def antlr4OutputKey = "$projectDir/build/generated-src/antlr4/main/de/uka/ilkd/key/nparser"
 task runAntlr4Key(type: JavaExec) {

diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java b/key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java
@@ -144,7 +144,6 @@ public boolean isEmpty() {
      */
     private SemisequentChangeInfo insertAndRemoveRedundancyHelper(int idx,
             SequentFormula sequentFormula, SemisequentChangeInfo semiCI, FormulaChangeInfo fci) {
-        assert idx >= 0;
 
         // Search for equivalent formulas and weakest constraint
         ImmutableList<SequentFormula> searchList = semiCI.getFormulaList();
@@ -260,7 +259,6 @@ private SemisequentChangeInfo removeRedundance(int idx, SequentFormula sequentFo
      */
     public SemisequentChangeInfo replace(PosInOccurrence pos, SequentFormula sequentFormula) {
         final int idx = indexOf(pos.sequentFormula());
-        assert idx >= 0;
         final FormulaChangeInfo fci = new FormulaChangeInfo(pos, sequentFormula);
         return insertAndRemoveRedundancyHelper(idx, sequentFormula, remove(idx), fci);
     }
@@ -424,9 +422,6 @@ public ImmutableList<SequentFormula> asList() {
 
     @Override
     public boolean equals(Object o) {
-        if (this == o) {
-            return true;
-        }
         if (!(o instanceof Semisequent)) {
             return false;
         }

diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java
@@ -405,10 +405,11 @@ protected void printNewVarcond(NewVarcond sv) {
         printSchemaVariable(sv.getSchemaVariable());
         layouter.print(",").brk();
         if (sv.isDefinedByType()) {
-            if (sv.getType() instanceof ArrayType) {
-                layouter.print(((ArrayType) sv.getType()).getAlternativeNameRepresentation());
+            final var type = sv.getType();
+            if (type.getJavaType() instanceof ArrayType) {
+                layouter.print(((ArrayType) type.getJavaType()).getAlternativeNameRepresentation());
             } else {
-                layouter.print(sv.getType().getFullName());
+                layouter.print(type.getFullName());
             }
         } else {
             layouter.print("\\typeof(").brk(0);

diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/BuiltInRuleAppIndex.java b/key.core/src/main/java/de/uka/ilkd/key/proof/BuiltInRuleAppIndex.java
@@ -3,8 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.proof;
 
-import java.util.concurrent.atomic.AtomicLong;
-
 import de.uka.ilkd.key.logic.*;
 import de.uka.ilkd.key.rule.BuiltInRule;
 import de.uka.ilkd.key.rule.IBuiltInRuleApp;
@@ -13,25 +11,27 @@
 import org.key_project.util.collection.ImmutableSLList;
 
 public class BuiltInRuleAppIndex {
-    public static final AtomicLong PERF_CREATE_ALL = new AtomicLong();
-    public static final AtomicLong PERF_UPDATE = new AtomicLong();
+
     private final BuiltInRuleIndex index;
 
-    private SequentChangeInfo sequentChangeInfo = null;
+    private NewRuleListener newRuleListener = NullNewRuleListener.INSTANCE;
 
     public BuiltInRuleAppIndex(BuiltInRuleIndex index) {
         this.index = index;
     }
 
-    private BuiltInRuleAppIndex(BuiltInRuleIndex index, SequentChangeInfo sequentChangeInfo) {
+
+    public BuiltInRuleAppIndex(BuiltInRuleIndex index, NewRuleListener p_newRuleListener) {
         this.index = index;
-        this.sequentChangeInfo = sequentChangeInfo;
+        this.newRuleListener = p_newRuleListener;
     }
 
+
     /**
      * returns a list of built-in rules application applicable for the given goal and position
      */
     public ImmutableList<IBuiltInRuleApp> getBuiltInRule(Goal goal, PosInOccurrence pos) {
+
         ImmutableList<IBuiltInRuleApp> result = ImmutableSLList.nil();
 
         ImmutableList<BuiltInRule> rules = index.rules();
@@ -51,8 +51,11 @@ public ImmutableList<IBuiltInRuleApp> getBuiltInRule(Goal goal, PosInOccurrence
      * returns a copy of this index
      */
     public BuiltInRuleAppIndex copy() {
-        return new BuiltInRuleAppIndex(index.copy(),
-            sequentChangeInfo == null ? null : sequentChangeInfo.copy());
+        return new BuiltInRuleAppIndex(index.copy());
+    }
+
+    public void setNewRuleListener(NewRuleListener p_newRuleListener) {
+        newRuleListener = p_newRuleListener;
     }
 
     public BuiltInRuleIndex builtInRuleIndex() {
@@ -79,8 +82,7 @@ private void scanSimplificationRule(Goal goal, NewRuleListener listener) {
         }
     }
 
-    private static void scanSimplificationRule(ImmutableList<BuiltInRule> rules, Goal goal,
-            boolean antec,
+    private void scanSimplificationRule(ImmutableList<BuiltInRule> rules, Goal goal, boolean antec,
             NewRuleListener listener) {
         final Node node = goal.node();
         final Sequent seq = node.sequent();
@@ -90,8 +92,7 @@ private static void scanSimplificationRule(ImmutableList<BuiltInRule> rules, Goa
         }
     }
 
-    private static void scanSimplificationRule(ImmutableList<BuiltInRule> rules, Goal goal,
-            boolean antec,
+    private void scanSimplificationRule(ImmutableList<BuiltInRule> rules, Goal goal, boolean antec,
             SequentFormula cfma, NewRuleListener listener) {
         final PosInOccurrence pos = new PosInOccurrence(cfma, PosInTerm.getTopLevel(), antec);
         ImmutableList<BuiltInRule> subrules = ImmutableSLList.nil();
@@ -109,7 +110,7 @@ private static void scanSimplificationRule(ImmutableList<BuiltInRule> rules, Goa
     }
 
     // TODO: optimise?
-    private static void scanSimplificationRule(ImmutableList<BuiltInRule> rules, Goal goal,
+    private void scanSimplificationRule(ImmutableList<BuiltInRule> rules, Goal goal,
             PosInOccurrence pos, NewRuleListener listener) {
         ImmutableList<BuiltInRule> it = rules;
         while (!it.isEmpty()) {
@@ -125,44 +126,21 @@ private static void scanSimplificationRule(ImmutableList<BuiltInRule> rules, Goa
         }
     }
 
-    public void reportRuleApps(Goal goal, NewRuleListener l) {
-        var time = System.nanoTime();
+    public void reportRuleApps(NewRuleListener l, Goal goal) {
         scanSimplificationRule(goal, l);
-        sequentChangeInfo = null;
-        PERF_CREATE_ALL.getAndAdd(System.nanoTime() - time);
     }
 
     /**
      * called if a formula has been replaced
      *
      * @param sci SequentChangeInfo describing the change of the sequent
      */
-    public void sequentChanged(SequentChangeInfo sci) {
-        if (sequentChangeInfo == null) {
-            // Nothing stored, store change
-            sequentChangeInfo = sci.copy();
-        } else {
-            assert sequentChangeInfo.sequent() == sci.getOriginalSequent();
-            sequentChangeInfo.combine(sci);
-        }
-    }
+    public void sequentChanged(Goal goal, SequentChangeInfo sci, NewRuleListener listener) {
+        scanAddedFormulas(goal, true, sci, listener);
+        scanAddedFormulas(goal, false, sci, listener);
 
-    public void resetSequentChanges() {
-        sequentChangeInfo = null;
-    }
-
-    public void flushSequentChanges(Goal goal, NewRuleListener listener) {
-        if (sequentChangeInfo == null) {
-            return;
-        }
-        var time = System.nanoTime();
-        scanAddedFormulas(goal, true, sequentChangeInfo, listener);
-        scanAddedFormulas(goal, false, sequentChangeInfo, listener);
-
-        scanModifiedFormulas(goal, true, sequentChangeInfo, listener);
-        scanModifiedFormulas(goal, false, sequentChangeInfo, listener);
-        sequentChangeInfo = null;
-        PERF_UPDATE.getAndAdd(System.nanoTime() - time);
+        scanModifiedFormulas(goal, true, sci, listener);
+        scanModifiedFormulas(goal, false, sci, listener);
     }
 
     private void scanAddedFormulas(Goal goal, boolean antec, SequentChangeInfo sci,

diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java
@@ -366,12 +366,6 @@ public void setSequent(SequentChangeInfo sci) {
             assert sci.sequent().equals(sci.getOriginalSequent());
             return;
         }
-        // sci.hasChanged() can be true for added: f, removed: f
-        // This afaik only ever happens in TestApplyTaclet.testBugBrokenApply
-        // Since SequentChangeInfo does not filter this we have to
-        // work with maybe sci.original.equals(sci.sequent)
-        // Checking this is probably too expensive for what it's worth
-        assert sci.sequent() != sci.getOriginalSequent();
         node().setSequent(sci.sequent());
         node().getNodeInfo().setSequentChangeInfo(sci);
         var time = System.nanoTime();

diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/RuleAppIndex.java b/key.core/src/main/java/de/uka/ilkd/key/proof/RuleAppIndex.java
@@ -91,6 +91,7 @@ private RuleAppIndex(TacletIndex tacletIndex, TacletAppIndex interactiveTacletAp
     private void setNewRuleListeners() {
         interactiveTacletAppIndex.setNewRuleListener(newRuleListener);
         automatedTacletAppIndex.setNewRuleListener(newRuleListener);
+        builtInRuleAppIndex.setNewRuleListener(newRuleListener);
     }
 
     /**
@@ -235,7 +236,8 @@ public ImmutableList<NoPosTacletApp> getRewriteTaclet(TacletFilter filter,
      * constraint and position
      */
     public ImmutableList<IBuiltInRuleApp> getBuiltInRules(Goal g, PosInOccurrence pos) {
-        return builtInRuleAppIndex.getBuiltInRule(g, pos);
+
+        return builtInRuleAppIndex().getBuiltInRule(g, pos);
     }
 
 
@@ -293,9 +295,11 @@ public void removeNoPosTacletApp(NoPosTacletApp tacletApp) {
      * @param sci SequentChangeInfo describing the change of the sequent
      */
     public void sequentChanged(SequentChangeInfo sci) {
-        interactiveTacletAppIndex.sequentChanged(sci);
+        if (!autoMode) {
+            interactiveTacletAppIndex.sequentChanged(sci);
+        }
         automatedTacletAppIndex.sequentChanged(sci);
-        builtInRuleAppIndex.sequentChanged(sci);
+        builtInRuleAppIndex.sequentChanged(goal, sci, newRuleListener);
     }
 
     /**
@@ -314,7 +318,6 @@ public void clearIndexes() {
         // Currently this only applies to the taclet index
         interactiveTacletAppIndex.clearIndexes();
         automatedTacletAppIndex.clearIndexes();
-        builtInRuleAppIndex.resetSequentChanges();
     }
 
     /**
@@ -325,16 +328,18 @@ public void fillCache() {
             interactiveTacletAppIndex.fillCache();
         }
         automatedTacletAppIndex.fillCache();
-        builtInRuleAppIndex.flushSequentChanges(goal, newRuleListener);
     }
 
     /**
      * Report all rule applications that are supposed to be applied automatically, and that are
      * currently stored by the index
+     *
+     * @param l the NewRuleListener
+     * @param services the Services
      */
-    public void reportAutomatedRuleApps() {
-        automatedTacletAppIndex.reportRuleApps(newRuleListener, goal.proof().getServices());
-        builtInRuleAppIndex.reportRuleApps(goal, newRuleListener);
+    public void reportAutomatedRuleApps(NewRuleListener l, Services services) {
+        automatedTacletAppIndex.reportRuleApps(l, services);
+        builtInRuleAppIndex.reportRuleApps(l, goal);
     }
 
     /**
@@ -343,7 +348,7 @@ public void reportAutomatedRuleApps() {
      * @param p_goal the Goal which to scan
      */
     public void scanBuiltInRules(Goal p_goal) {
-        builtInRuleAppIndex.scanApplicableRules(p_goal, newRuleListener);
+        builtInRuleAppIndex().scanApplicableRules(p_goal, newRuleListener);
     }
 
     /**
@@ -377,7 +382,7 @@ public RuleAppIndex copy(Goal goal) {
         TacletAppIndex copiedAutomatedTacletAppIndex =
             automatedTacletAppIndex.copyWith(copiedTacletIndex, goal);
         return new RuleAppIndex(copiedTacletIndex, copiedInteractiveTacletAppIndex,
-            copiedAutomatedTacletAppIndex, builtInRuleAppIndex.copy(), goal, autoMode);
+            copiedAutomatedTacletAppIndex, builtInRuleAppIndex().copy(), goal, autoMode);
     }