diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java index b38050af8c5..b4a63d7eac5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java @@ -64,7 +64,7 @@ public class Node implements Iterable { private final ArrayList children = new ArrayList<>(1); - private RuleApp appliedRuleApp; + private @Nullable RuleApp appliedRuleApp; private NameRecorder nameRecorder; @@ -221,7 +221,8 @@ public ImmutableList getRenamingTable() { return renamings; } - public RuleApp getAppliedRuleApp() { + /// Get the applied rule (null for open/closed goals). + public @Nullable RuleApp getAppliedRuleApp() { return appliedRuleApp; } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java index c8efaf15a22..f6589d29a5a 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java @@ -12,18 +12,11 @@ import java.util.stream.Stream; import de.uka.ilkd.key.proof.BranchLocation; -import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; -import de.uka.ilkd.key.proof.ProofEvent; import de.uka.ilkd.key.proof.ProofTreeEvent; import de.uka.ilkd.key.proof.ProofTreeListener; -import de.uka.ilkd.key.proof.RuleAppListener; import de.uka.ilkd.key.proof.mgt.RuleJustificationByAddRules; -import de.uka.ilkd.key.proof.proofevent.NodeChangeAddFormula; -import de.uka.ilkd.key.proof.proofevent.NodeChangeRemoveFormula; -import de.uka.ilkd.key.proof.proofevent.NodeReplacement; -import de.uka.ilkd.key.proof.proofevent.RuleAppInfo; import de.uka.ilkd.key.rule.NoPosTacletApp; import de.uka.ilkd.key.rule.RuleAppUtil; import de.uka.ilkd.key.rule.Taclet; @@ -44,16 +37,13 @@ import org.key_project.slicing.graph.PseudoOutput; import org.key_project.slicing.graph.TrackedFormula; import org.key_project.util.collection.IdentityHashSet; -import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.Pair; -/** - * Tracks proof steps as they are applied on the proof. - * Each proof step is recorded in the dependency graph ({@link DependencyGraph}). - * - * @author Arne Keller - */ -public class DependencyTracker implements RuleAppListener, ProofTreeListener { +/// Constructs the [DependencyGraph] based on a proof's nodes. +/// Also provides a wrapper around the [DependencyAnalyzer]. +/// +/// @author Arne Keller +public class DependencyTracker implements ProofTreeListener { /** * The proof this tracker monitors. */ @@ -73,16 +63,11 @@ public class DependencyTracker implements RuleAppListener, ProofTreeListener { * @see DependencyAnalyzer */ private AnalysisResults analysisResults = null; - /** - * Set once tracking failed with an exception (after which {@link Proof} unregisters this - * tracker, see {@link #ruleApplied(ProofEvent)}). The dependency graph is then incomplete, so - * {@link #analyze} no longer returns results. - */ - private boolean trackingDisabled = false; /** * Construct a new tracker for a proof. - * This tracker is added as a RuleAppListener and ProofTreeListener to the proof. + * This tracker is added as a ProofTreeListener to the proof. + * If the proof already contains some nodes, they are added to the dependency graph. * * @param proof the proof to track */ @@ -90,15 +75,10 @@ public DependencyTracker(Proof proof) { this.proof = proof; proof.addProofTreeListener(this); proof.register(this, DependencyTracker.class); - // skip further tracking if disabled - if (!SlicingSettingsProvider.getSlicingSettings().getAlwaysTrack()) { - return; - } // exotic use case: registering a dependency tracker after the proof is loaded if (proof.countNodes() > 1) { graph.ensureProofIsTracked(proof); } - proof.addRuleAppListener(this); } /** @@ -182,25 +162,12 @@ private List> inputsOfNode(Node n, } /** - * Get all formulas removed by the provided rule application, i.e. all formulas not present - * in the replacement nodes. + * Get all formulas removed by the preceding rule application, i.e. all formulas not present + * in the provided node compared to the parent node. * - * @param ruleAppInfo some rule application + * @param node the proof step * @return formulas removed by that rule application */ - private Set formulasRemovedBy( - RuleAppInfo ruleAppInfo) { - Set removed = new HashSet<>(); - for (NodeReplacement newNode : ruleAppInfo.getReplacementNodes()) { - newNode.getNodeChanges().forEachRemaining(nodeChange -> { - if (nodeChange instanceof NodeChangeRemoveFormula) { - removed.add(nodeChange.getPos()); - } - }); - } - return removed; - } - private Set formulasRemovedBy(Node node) { Set removed = new HashSet<>(); // compare parent sequent to new sequent @@ -225,26 +192,9 @@ private Set formulasRemovedBy(Node node) { * Get the formulas added by this rule application. Each returned pair is one formula * and the ID of the branch it is added to (-1 if the node doesn't branch). * - * @param ruleAppInfo rule application info + * @param node the proof step * @return formulas added */ - private List> outputsOfNode( - RuleAppInfo ruleAppInfo) { - List> outputs = - new ArrayList<>(); - int sibling = ruleAppInfo.getReplacementNodes().size() - 1; - for (NodeReplacement b : ruleAppInfo.getReplacementNodes()) { - int id = ruleAppInfo.getReplacementNodes().size() > 1 ? sibling : -1; - b.getNodeChanges().forEachRemaining(c -> { - if (c instanceof NodeChangeAddFormula) { - outputs.add(new Pair<>(c.getPos(), id)); - } - }); - sibling--; - } - return outputs; - } - private List> outputsOfNode( Node node) { List> outputs = @@ -268,110 +218,10 @@ private List> outputsOfNode( return outputs; } - @Override - public void ruleApplied(ProofEvent e) { - if (trackingDisabled) { - return; - } - try { - trackRuleApplication(e); - } catch (RuntimeException ex) { - // Proof.fireRuleApplied isolates listeners: it logs this failure and unregisters the - // tracker, so a tracking error cannot break the ongoing proof search. Here we only - // record that tracking became incomplete, so that a later analyze() does not return a - // slice computed from the partial dependency graph; then rethrow for the proof to - // handle. - trackingDisabled = true; - analysisResults = null; - throw ex; - } - } - - private void trackRuleApplication(ProofEvent e) { - if (e.getSource() != proof) { - throw new IllegalStateException( - "dependency tracker received rule application on wrong proof"); - } - RuleAppInfo ruleAppInfo = e.getRuleAppInfo(); - RuleApp ruleApp = ruleAppInfo.getRuleApp(); - ImmutableList goalList = e.getNewGoals(); - Node n = ruleAppInfo.getOriginalNode(); - - // outputs: new graph nodes - List output = new ArrayList<>(); - - // record any rules added by this rule application - for (NodeReplacement newNode : ruleAppInfo.getReplacementNodes()) { - for (NoPosTacletApp newRule : newNode.getNode().getLocalIntroducedRules()) { - final var justification = - newNode.getNode().proof().getInitConfig().getJustifInfo() - .getJustification(newRule.taclet()); - if (justification instanceof RuleJustificationByAddRules justAddRule && - justAddRule.node() == n) { - AddedRule ruleNode = new AddedRule(newRule.rule().name().toString()); - output.add(ruleNode); - dynamicRules.put(newRule.rule(), ruleNode); - } - } - } - - // record removed (replaced) input formulas - // (these are the same for each new branch) - Set removed = formulasRemovedBy(ruleAppInfo); - - // inputs: (graph node, whether that graph node was replaced) - List> input = inputsOfNode(n, removed); - - // Newly created sequent formulas and the index of the branch they are created in. - // If no new branches are created, use index -1. - List> outputs = - outputsOfNode(ruleAppInfo); - - for (Pair out : outputs) { - BranchLocation loc = n.getBranchLocation(); - if (out.second != -1) { - // this is a branching proof step: set correct branch location of new formulas - loc = loc.append(new Pair<>(n, out.second)); - } - TrackedFormula formula = new TrackedFormula( - out.first.sequentFormula(), - loc, - out.first.isInAntec(), - proof.getServices()); - output.add(formula); - } - - // add closed goals to output nodes - if (goalList.isEmpty() || (ruleApp instanceof TacletApp tacletApp && - tacletApp.taclet().closeGoal())) { - // closed goal is always the next node - // (or the current node, if the goal was closed by SMT) - Node closedGoal = n.childrenCount() > 0 ? n.child(0) : n; - output.add( - new ClosedGoal(closedGoal.serialNr(), n.getBranchLocation())); - } - - n.register(new DependencyNodeData( - input, - output, - ruleApp.rule().displayName() + "_" + n.serialNr()), DependencyNodeData.class); - - // add pseudo nodes so the rule application is always included in the graph - if (input.isEmpty()) { - input.add(new Pair<>(new PseudoInput(), true)); - } - if (output.isEmpty()) { - output.add(new PseudoOutput()); - } - - // add new edges to graph - graph.addRuleApplication(n, input, output); - } - /** * Track the specified node. - * Either this method or {@link #ruleApplied(ProofEvent)} needs to be called to track - * a node in the dependency graph. + * To fully construct the dependency graph for a proof, this method must be called with each + * node of the proof in order of application (!) * * @param n the node */ @@ -380,6 +230,9 @@ public void trackNode(Node n) { throw new IllegalStateException("dependency tracker received node of wrong proof"); } RuleApp ruleApp = n.getAppliedRuleApp(); + if (ruleApp == null) { + return; // closed goal (always tracked as part of the previous node) + } var goalList = n.children(); // outputs: new graph nodes @@ -495,10 +348,6 @@ public String exportDotAround(boolean abbreviateFormulas, boolean omitBranch, Gr * @return analysis results (null if proof is not closed) */ public AnalysisResults analyze(boolean doDependencyAnalysis, boolean doDeduplicateRuleApps) { - if (trackingDisabled) { - // the dependency graph is incomplete after a tracking failure; do not return a slice - return null; - } if (analysisResults != null && analysisResults.didDependencyAnalysis == doDependencyAnalysis && analysisResults.didDeduplicateRuleApps == doDeduplicateRuleApps diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java index cbea0acfafd..98705994789 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java @@ -136,7 +136,6 @@ private void createTrackerForProof(Proof newProof) { proof.addProofDisposedListener(this); DependencyTracker tracker = new DependencyTracker(proof); if (leftPanel != null) { - proof.addRuleAppListener(e -> leftPanel.ruleAppliedOnProof(proof, tracker)); proof.addProofTreeListener(leftPanel); if (enableSafeModeForNextProof) { SlicingSettingsProvider.getSlicingSettings() diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingSettings.java b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingSettings.java index 65969427808..5a733263ecc 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingSettings.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingSettings.java @@ -18,10 +18,6 @@ public class SlicingSettings extends AbstractPropertiesSettings { public static final String CATEGORY = "ProofSlicing"; - /** - * Config key for {@link #alwaysTrack}. - */ - private static final String KEY_ALWAYS_TRACK = "alwaysTrack"; /** * Config key for {@link #aggressiveDeduplicate}. */ @@ -31,12 +27,6 @@ public class SlicingSettings extends AbstractPropertiesSettings { */ private static final String KEY_DOT_EXECUTABLE = "dotExecutable"; - /** - * Always track dependencies config key. - */ - private final PropertyEntry alwaysTrack = - createBooleanProperty(KEY_ALWAYS_TRACK, true); - /** * Aggressive rule deduplication config key. */ @@ -59,14 +49,6 @@ public SlicingSettings() { super(CATEGORY); } - public boolean getAlwaysTrack() { - return alwaysTrack.get(); - } - - public void setAlwaysTrack(boolean value) { - alwaysTrack.set(value); - } - /** * @param proof proof * @return whether aggressive deduplication is turned on for this proof diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingSettingsProvider.java b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingSettingsProvider.java index ad5c4ac1891..a1b10723f16 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingSettingsProvider.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingSettingsProvider.java @@ -27,18 +27,6 @@ public class SlicingSettingsProvider extends SettingsPanel implements SettingsPr * Text for introductory explanation */ private static final String INTRO_LABEL = "Adjust proof analysis algorithm options here."; - /** - * Label for always track option. - */ - private static final String ALWAYS_TRACK = "Always track dependencies"; - /** - * Explanatory text for always track option. - */ - private static final String ALWAYS_TRACK_INFO = - """ - If enabled, the dependency tracker will construct the dependency graph as the proof - is created. When disabled, the dependency graph is created only when needed, and - the 'Show proof step that created this formula' action is not available."""; /** * Label for aggressive deduplicate option. */ @@ -55,7 +43,6 @@ public class SlicingSettingsProvider extends SettingsPanel implements SettingsPr private static final String DOT_EXECUTABLE_INFO = "Path to dot executable from the graphviz package."; - private final JCheckBox alwaysTrack; /** * Checkbox for first option. */ @@ -71,8 +58,6 @@ public SlicingSettingsProvider() { pCenter.add(new JLabel(INTRO_LABEL), new CC().span().alignX("left")); addSeparator("Dependency graph"); - alwaysTrack = addCheckBox(ALWAYS_TRACK, ALWAYS_TRACK_INFO, true, e -> { - }); dotExecutable = addTextField(DOT_EXECUTABLE, "dot", DOT_EXECUTABLE_INFO, e -> { }); @@ -98,7 +83,6 @@ public static SlicingSettings getSlicingSettings() { @Override public JPanel getPanel(MainWindow window) { SlicingSettings ss = getSlicingSettings(); - alwaysTrack.setSelected(ss.getAlwaysTrack()); dotExecutable.setText(ss.getDotExecutable()); aggressiveDeduplicate.setSelected(ss.getAggressiveDeduplicate(null)); return this; @@ -107,7 +91,6 @@ public JPanel getPanel(MainWindow window) { @Override public void applySettings(MainWindow window) { SlicingSettings ss = getSlicingSettings(); - ss.setAlwaysTrack(alwaysTrack.isSelected()); ss.setDotExecutable(dotExecutable.getText()); ss.setAggressiveDeduplicate(aggressiveDeduplicate.isSelected()); } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java index 45059b3619c..eabc5c12cd3 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java @@ -69,10 +69,13 @@ public void ensureProofIsTracked(Proof p) { throw new IllegalStateException("tried to use DependencyGraph with wrong proof"); } DependencyTracker tracker = p.lookup(DependencyTracker.class); + if (tracker == null) { + throw new IllegalStateException("proof is missing dependency tracker"); + } var nodeIterator = p.root().subtreeIterator(); while (nodeIterator.hasNext()) { var node = nodeIterator.next(); - if (node.getAppliedRuleApp() == null || edgeDataReversed.containsKey(node)) { + if (edgeDataReversed.containsKey(node)) { continue; } tracker.trackNode(node); diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java b/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java index f8c408348fc..edec3296998 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java @@ -41,6 +41,7 @@ import org.key_project.slicing.SlicingProofReplayer; import org.key_project.slicing.SlicingSettingsProvider; import org.key_project.slicing.analysis.AnalysisResults; +import org.key_project.slicing.graph.DependencyGraph; import org.key_project.slicing.util.GenericWorker; import org.key_project.slicing.util.GraphvizDotExecutor; @@ -157,22 +158,10 @@ public class SlicingLeftPanel extends JPanel implements TabPanel, KeYSelectionLi private JPanel timings = null; /** - * Number of nodes in the dependency graph. + * Timer to regularly update dependency graph statistics and other UI state when loading a + * proof. */ - private int graphNodesNr = 0; - /** - * Number of edges in the dependency graph. - */ - private int graphEdgesNr = 0; - /** - * Indicates whether graph statistics ({@link #graphNodes}, {@link #graphEdges}) need to be - * updated based on {@link #graphNodesNr} and {@link #graphEdgesNr}. - */ - private boolean updateGraphLabels = false; - /** - * Timer to regularly update dependency graph statistics when loading a proof. - */ - private Timer updateGraphLabelsTimer; + private Timer updateUiStateTimer; /** * Construct a new panel for this extension. @@ -194,11 +183,15 @@ public SlicingLeftPanel(KeYMediator mediator, SlicingExtension extension) { this.mediator = mediator; this.extension = extension; - updateGraphLabelsTimer = new Timer(100, e -> { - if (updateGraphLabels) { - displayGraphLabels(); - updateGraphLabelsTimer.stop(); + updateUiStateTimer = new Timer(500, e -> { + var tracker = extension.trackers.get(currentProof); + if (tracker != null) { + displayGraphLabels(tracker.getDependencyGraph()); + } else { + resetGraphLabels(); } + updateUIState(); + updateUiStateTimer.stop(); }); } @@ -351,6 +344,9 @@ private void exportDot(ActionEvent event) { if (currentProof == null) { return; } + var tracker = extension.trackers.get(currentProof); + tracker.getDependencyGraph().ensureProofIsTracked(currentProof); + displayGraphLabels(tracker.getDependencyGraph()); KeYFileChooser fileChooser = KeYFileChooser.getFileChooser( "Choose filename to save dot file"); fileChooser.setFileFilter(KeYFileChooser.DOT_FILTER); @@ -360,7 +356,7 @@ private void exportDot(ActionEvent event) { File file = fileChooser.getSelectedFile(); try (BufferedWriter writer = new BufferedWriter( new OutputStreamWriter(new FileOutputStream(file), StandardCharsets.UTF_8))) { - String text = extension.trackers.get(currentProof) + String text = tracker .exportDot(abbreviateFormulas.isSelected(), abbreviateChains.isSelected()); writer.write(text); } catch (IOException e) { @@ -386,7 +382,10 @@ private void previewGraph(ActionEvent e) { if (currentProof == null) { return; } - String text = extension.trackers.get(currentProof) + var tracker = extension.trackers.get(currentProof); + tracker.getDependencyGraph().ensureProofIsTracked(currentProof); + displayGraphLabels(tracker.getDependencyGraph()); + String text = tracker .exportDot(abbreviateFormulas.isSelected(), abbreviateChains.isSelected()); new PreviewDialog(MainWindow.getInstance(), text); } @@ -484,6 +483,7 @@ private void displayResults(AnalysisResults results) { resetLabels(); return; } + displayGraphLabels(results.dependencyGraph); totalSteps.setText("Total steps: " + results.totalSteps); usefulSteps.setText("Useful steps: " + results.usefulStepsNr); totalBranches.setText("Total branches: " + results.proof.countBranches()); @@ -509,9 +509,15 @@ private void resetGraphLabels() { graphEdges.setText("Graph edges: ?"); } - private void displayGraphLabels() { - graphNodes.setText("Graph nodes: " + graphNodesNr); - graphEdges.setText("Graph edges: " + graphEdgesNr); + private void displayGraphLabels(DependencyGraph graph) { + int graphNodesNr = graph.countNodes(); + int graphEdgesNr = graph.countEdges(); + if (graphNodesNr != 0 && graphEdgesNr != 0) { + graphNodes.setText("Graph nodes: " + graphNodesNr); + graphEdges.setText("Graph edges: " + graphEdgesNr); + } else { + resetGraphLabels(); // no dependency graph computed yet + } } @Override @@ -543,31 +549,24 @@ public void selectedProofChanged(KeYSelectionEvent e) { displayResults(tracker.getAnalysisResults()); } if (tracker.getDependencyGraph() != null) { - graphNodesNr = tracker.getDependencyGraph().countNodes(); - graphEdgesNr = tracker.getDependencyGraph().countEdges(); - displayGraphLabels(); + displayGraphLabels(tracker.getDependencyGraph()); } } /** - * Notify the panel that a rule has been applied on the currently opened proof. + * Notify the panel that the dependency graph of the provided proof has been updated. * - * @param proof proof - * @param tracker dependency tracker of that proof + * @param proof currently opened proof */ - public void ruleAppliedOnProof(Proof proof, DependencyTracker tracker) { + public void dependencyGraphUpdated(Proof proof) { currentProof = proof; - graphNodesNr = tracker.getDependencyGraph().countNodes(); - graphEdgesNr = tracker.getDependencyGraph().countEdges(); - updateGraphLabels = true; - updateGraphLabelsTimer.start(); - - updateUIState(); + updateUiStateTimer.start(); } @Override public void proofPruned(ProofTreeEvent e) { - ruleAppliedOnProof(e.getSource(), extension.trackers.get(e.getSource())); + // this is called after the dependency graph is updated using proofIsBeingPruned + dependencyGraphUpdated(e.getSource()); } private void updateUIState() {