From 14c2296dc727852ce0ca19c699e4b9647e8a0416 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Tue, 28 May 2024 14:27:08 +0200 Subject: [PATCH 1/9] Updated witness generation functions to return the generated File. Refactor of witness generation in Dartagnan.java --- .../java/com/dat3m/dartagnan/Dartagnan.java | 43 +++++++++++++------ .../graphviz/ExecutionGraphVisualizer.java | 8 ++-- .../dartagnan/witness/graphviz/Graphviz.java | 10 +++-- 3 files changed, 40 insertions(+), 21 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 1a066032b6..4533d49ae2 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -20,11 +20,16 @@ import com.dat3m.dartagnan.verification.VerificationTask; import com.dat3m.dartagnan.verification.VerificationTask.VerificationTaskBuilder; import com.dat3m.dartagnan.verification.model.ExecutionModel; -import com.dat3m.dartagnan.verification.solving.*; +import com.dat3m.dartagnan.verification.solving.AssumeSolver; +import com.dat3m.dartagnan.verification.solving.DataRaceSolver; +import com.dat3m.dartagnan.verification.solving.ModelChecker; +import com.dat3m.dartagnan.verification.solving.RefinementSolver; +import com.dat3m.dartagnan.witness.WitnessType; import com.dat3m.dartagnan.witness.graphml.WitnessBuilder; import com.dat3m.dartagnan.witness.graphml.WitnessGraph; import com.dat3m.dartagnan.wmm.Wmm; import com.dat3m.dartagnan.wmm.axiom.Axiom; +import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableSet; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; @@ -40,8 +45,10 @@ import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; + import java.io.File; import java.io.FileReader; +import java.io.IOException; import java.math.BigInteger; import java.util.*; @@ -54,7 +61,7 @@ import static com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis.*; import static com.dat3m.dartagnan.utils.GitInfo.*; import static com.dat3m.dartagnan.utils.Result.*; -import static com.dat3m.dartagnan.witness.WitnessType.*; +import static com.dat3m.dartagnan.witness.WitnessType.GRAPHML; import static com.dat3m.dartagnan.witness.graphviz.ExecutionGraphVisualizer.generateGraphvizFile; import static java.lang.Boolean.FALSE; import static java.lang.Boolean.TRUE; @@ -180,18 +187,8 @@ public static void main(String[] args) throws Exception { // Verification ended, we can interrupt the timeout Thread t.interrupt(); - if (modelChecker.hasModel() && o.getWitnessType().generateGraphviz()) { - final ExecutionModel m = ExecutionModel.withContext(modelChecker.getEncodingContext()); - m.initialize(prover.getModel()); - final SyntacticContextAnalysis synContext = newInstance(task.getProgram()); - final String name = task.getProgram().getName().substring(0, task.getProgram().getName().lastIndexOf('.')); - // RF edges give both ordering and data flow information, thus even when the pair is in PO - // we get some data flow information by observing the edge - // FR edges only give ordering information which is known if the pair is also in PO - // CO edges only give ordering information which is known if the pair is also in PO - generateGraphvizFile(m, 1, (x, y) -> true, (x, y) -> !x.getThread().equals(y.getThread()), - (x, y) -> !x.getThread().equals(y.getThread()), getOrCreateOutputDirectory() + "/", name, - synContext, o.getWitnessType().convertToPng()); + if (modelChecker.hasModel()) { + generateExecutionGraphFile(task, prover, modelChecker, o.getWitnessType()); } long endTime = System.currentTimeMillis(); @@ -215,6 +212,24 @@ public static void main(String[] args) throws Exception { } } + public static File generateExecutionGraphFile(VerificationTask task, ProverEnvironment prover, ModelChecker modelChecker, + WitnessType witnessType) + throws InvalidConfigurationException, SolverException, IOException { + Preconditions.checkArgument(modelChecker.hasModel(), "No model to generate."); + + final ExecutionModel m = ExecutionModel.withContext(modelChecker.getEncodingContext()); + m.initialize(prover.getModel()); + final SyntacticContextAnalysis synContext = newInstance(task.getProgram()); + final String name = task.getProgram().getName().substring(0, task.getProgram().getName().lastIndexOf('.')); + // RF edges give both ordering and data flow information, thus even when the pair is in PO + // we get some data flow information by observing the edge + // FR edges only give ordering information which is known if the pair is also in PO + // CO edges only give ordering information which is known if the pair is also in PO + return generateGraphvizFile(m, 1, (x, y) -> true, (x, y) -> !x.getThread().equals(y.getThread()), + (x, y) -> !x.getThread().equals(y.getThread()), getOrCreateOutputDirectory() + "/", name, + synContext, witnessType.convertToPng()); + } + private static void generateWitnessIfAble(VerificationTask task, ProverEnvironment prover, ModelChecker modelChecker, String summary) { // ------------------ Generate Witness, if possible ------------------ diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java index 4f535f402a..0bd5707727 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java @@ -9,7 +9,6 @@ import com.dat3m.dartagnan.program.event.metadata.MemoryOrder; import com.dat3m.dartagnan.verification.model.EventData; import com.dat3m.dartagnan.verification.model.ExecutionModel; - import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; @@ -225,7 +224,7 @@ private void appendEdge(EventData a, EventData b, String... options) { graphviz.addEdge(eventToNode(a), eventToNode(b), options); } - public static void generateGraphvizFile(ExecutionModel model, int iterationCount, + public static File generateGraphvizFile(ExecutionModel model, int iterationCount, BiPredicate rfFilter, BiPredicate frFilter, BiPredicate coFilter, String directoryName, String fileNameBase, SyntacticContextAnalysis synContext, @@ -243,11 +242,14 @@ public static void generateGraphvizFile(ExecutionModel model, int iterationCount writer.flush(); if (convert) { - Graphviz.convert(fileVio); + fileVio = Graphviz.convert(fileVio); } + return fileVio; } catch (Exception e) { logger.error(e); } + + return null; } public static void generateGraphvizFile(ExecutionModel model, int iterationCount, diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/Graphviz.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/Graphviz.java index b3385fc26a..bb95e22eb4 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/Graphviz.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/Graphviz.java @@ -96,11 +96,13 @@ public void generateOutput(Writer writer) throws IOException { * @throws IOException The program is not installed, or the directory of {@code dotFile} does not exist. * @throws InterruptedException The current thread is interrupted while waiting for the command to finish. */ - public static void convert(File dotFile) throws IOException, InterruptedException { - String fileName = dotFile.getName(); - String fileNameBase = fileName.substring(0, fileName.lastIndexOf('.')); + public static File convert(File dotFile) throws IOException, InterruptedException { + final String dotFileName = dotFile.getName(); + final String pngFileName = dotFileName.substring(0, dotFileName.lastIndexOf('.')) + ".png"; Process p = new ProcessBuilder().directory(dotFile.getParentFile()) - .command("dot", "-Tpng", fileName, "-o", fileNameBase + ".png").start(); + .command("dot", "-Tpng", dotFileName, "-o", pngFileName).start(); p.waitFor(1000, TimeUnit.MILLISECONDS); + + return new File(dotFile.getParentFile(), pngFileName); } } From 8901937f1b93e3477b72bc1fe516350b9115dfb5 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Tue, 28 May 2024 14:30:13 +0200 Subject: [PATCH 2/9] Improved UI: - can select property to check for (only one property at a time) - can generate and render the violation witness in the UI - UI can be scaled with 'ctrl' + '+/-' --- ui/src/main/java/com/dat3m/ui/Dat3M.java | 200 ++++++++++-------- .../main/java/com/dat3m/ui/editor/Editor.java | 37 +++- .../java/com/dat3m/ui/editor/EditorsPane.java | 6 +- .../com/dat3m/ui/options/OptionsPane.java | 94 ++++---- .../dat3m/ui/options/utils/ControlCode.java | 6 +- .../dat3m/ui/result/ReachabilityResult.java | 98 +++++---- .../java/com/dat3m/ui/utils/UiOptions.java | 44 +--- .../main/java/com/dat3m/ui/utils/Utils.java | 29 ++- 8 files changed, 278 insertions(+), 236 deletions(-) diff --git a/ui/src/main/java/com/dat3m/ui/Dat3M.java b/ui/src/main/java/com/dat3m/ui/Dat3M.java index c706aac778..6f7273c0d9 100644 --- a/ui/src/main/java/com/dat3m/ui/Dat3M.java +++ b/ui/src/main/java/com/dat3m/ui/Dat3M.java @@ -4,19 +4,18 @@ import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.wmm.Wmm; -import com.dat3m.ui.editor.EditorsPane; import com.dat3m.ui.editor.Editor; import com.dat3m.ui.editor.EditorCode; +import com.dat3m.ui.editor.EditorsPane; import com.dat3m.ui.listener.EditorListener; -import com.dat3m.ui.utils.UiOptions; import com.dat3m.ui.options.OptionsPane; import com.dat3m.ui.options.utils.ControlCode; import com.dat3m.ui.result.ReachabilityResult; -import javax.swing.*; - +import com.dat3m.ui.utils.UiOptions; import org.antlr.v4.runtime.InputMismatchException; import org.antlr.v4.runtime.Token; +import javax.swing.*; import java.awt.*; import java.awt.event.ActionEvent; import java.awt.event.ActionListener; @@ -27,88 +26,121 @@ public class Dat3M extends JFrame implements ActionListener { - private final OptionsPane optionsPane = new OptionsPane(); - private final EditorsPane editorsPane = new EditorsPane(); - - private ReachabilityResult testResult; - - private Dat3M() { - getDefaults().put("SplitPane.border", createEmptyBorder()); - - setTitle("Dat3M"); - setExtendedState(JFrame.MAXIMIZED_BOTH); - setDefaultCloseOperation(JFrame.EXIT_ON_CLOSE); - setLayout(new BorderLayout()); -// setIconImage(IconHelper.getIcon(IconCode.DAT3M).getImage()); - - JMenuBar menuBar = new JMenuBar(); - JMenu fileMenu = new JMenu("File"); - fileMenu.add(editorsPane.getMenuImporter()); - fileMenu.add(editorsPane.getMenuExporter()); - menuBar.add(fileMenu); - setJMenuBar(menuBar); - - JSplitPane mainPane = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT, optionsPane, editorsPane.getMainPane()); - mainPane.setDividerSize(2); - add(mainPane); - - // Start listening to button events - optionsPane.getTestButton().addActionListener(this); - - // optionsPane needs to listen to editor to clean the console - editorsPane.getEditor(EditorCode.PROGRAM).addActionListener(optionsPane); - editorsPane.getEditor(EditorCode.TARGET_MM).addActionListener(optionsPane); - - // The console shall be cleaned every time the program or MM is modified from the editor - EditorListener listener = new EditorListener(optionsPane.getConsolePane()); - editorsPane.getEditor(EditorCode.PROGRAM).getEditorPane().addKeyListener(listener); - editorsPane.getEditor(EditorCode.TARGET_MM).getEditorPane().addKeyListener(listener); - - pack(); - } - - public static void main(String[] args) { - EventQueue.invokeLater(() -> { - Dat3M app = new Dat3M(); - app.setVisible(true); - }); - } - - @Override - public void actionPerformed(ActionEvent event) { - String command = event.getActionCommand(); - if(ControlCode.TEST.actionCommand().equals(command)){ + private final OptionsPane optionsPane = new OptionsPane(); + private final EditorsPane editorsPane = new EditorsPane(); + + private ReachabilityResult testResult; + + private Dat3M() { + getDefaults().put("SplitPane.border", createEmptyBorder()); + + setTitle("Dat3M"); + setExtendedState(JFrame.MAXIMIZED_BOTH); + setDefaultCloseOperation(JFrame.EXIT_ON_CLOSE); + setLayout(new BorderLayout()); +// setIconImage(IconHelper.getIcon(IconCode.DAT3M).getImage()); + + JMenuBar menuBar = new JMenuBar(); + JMenu fileMenu = new JMenu("File"); + fileMenu.add(editorsPane.getMenuImporter()); + fileMenu.add(editorsPane.getMenuExporter()); + menuBar.add(fileMenu); + setJMenuBar(menuBar); + + JSplitPane mainPane = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT, optionsPane, editorsPane.getMainPane()); + mainPane.setDividerSize(2); + add(mainPane); + + // Start listening to button events + optionsPane.getTestButton().addActionListener(this); + + // optionsPane needs to listen to editor to clean the console + editorsPane.getEditor(EditorCode.PROGRAM).addActionListener(optionsPane); + editorsPane.getEditor(EditorCode.TARGET_MM).addActionListener(optionsPane); + + // The console shall be cleaned every time the program or MM is modified from the editor + EditorListener listener = new EditorListener(optionsPane.getConsolePane()); + editorsPane.getEditor(EditorCode.PROGRAM).getEditorPane().addKeyListener(listener); + editorsPane.getEditor(EditorCode.TARGET_MM).getEditorPane().addKeyListener(listener); + + pack(); + } + + public static void main(String[] args) { + EventQueue.invokeLater(() -> { + Dat3M app = new Dat3M(); + app.setVisible(true); + }); + } + + @Override + public void actionPerformed(ActionEvent event) { + String command = event.getActionCommand(); + if (ControlCode.TEST.actionCommand().equals(command)) { runTest(); - if(testResult != null){ + if (testResult != null) { optionsPane.getConsolePane().setText(testResult.getVerdict()); + if (optionsPane.getOptions().showViolationGraph() && testResult.hasViolationModel()) { + showViolation(testResult); + } + } + } + } + + private void showViolation(ReachabilityResult testResult) { + final String filePath = testResult.getViolationModelFile().getAbsolutePath(); + + // Generate scroll pane with image of violation + final ImageIcon imageIcon = new ImageIcon(filePath); + imageIcon.getImage().flush(); // Flush the caches for otherwise we might show a previously loaded file!!! + final JScrollPane scrollPane = new JScrollPane(new JLabel(imageIcon)); + + scrollPane.setHorizontalScrollBarPolicy(JScrollPane.HORIZONTAL_SCROLLBAR_AS_NEEDED); + scrollPane.setVerticalScrollBarPolicy(JScrollPane.VERTICAL_SCROLLBAR_AS_NEEDED); + + // Generate window frame at center of screen that embeds the scrollable image + final JFrame imageFrame = new JFrame(); + final Dimension screenSize = Toolkit.getDefaultToolkit().getScreenSize(); + final int x = (screenSize.width - imageFrame.getSize().width) / 2; + final int y = (screenSize.height - imageFrame.getSize().height) / 2; + final int extraFrameSize = 100; + + imageFrame.setSize(imageIcon.getIconWidth() + extraFrameSize, imageIcon.getIconHeight() + extraFrameSize); + imageFrame.getContentPane().add(scrollPane); + imageFrame.setLocation(x, y); + imageFrame.setVisible(true); + + optionsPane.getConsolePane().setText( + optionsPane.getConsolePane().getText() + "\n" + "Witness file: " + filePath + ); + } + + private void runTest() { + UiOptions options = optionsPane.getOptions(); + testResult = null; + try { + final Editor programEditor = editorsPane.getEditor(EditorCode.PROGRAM); + // We default to "c" code, if we do not know + final String format = programEditor.getLoadedFormat().isEmpty() ? "c" : programEditor.getLoadedFormat(); + final Program program = new ProgramParser().parse(programEditor.getEditorPane().getText(), + programEditor.getLoadedPath(), + format, + options.cflags()); + try { + final Wmm targetModel = new ParserCat().parse(editorsPane.getEditor(EditorCode.TARGET_MM).getEditorPane().getText()); + testResult = new ReachabilityResult(program, targetModel, options); + } catch (Exception e) { + final String msg = e.getMessage() == null ? "Memory model cannot be parsed" : e.getMessage(); + showError(msg, "Target memory model error"); + } + } catch (Exception e) { + final Throwable cause = e.getCause(); + String msg = e.getMessage() == null ? "Program cannot be parsed" : e.getMessage(); + if (cause instanceof InputMismatchException exception) { + Token token = exception.getOffendingToken(); + msg = "Problem with \"" + token.getText() + "\" at line " + token.getLine(); } + showError(msg, "Program error"); } - } - - private void runTest(){ - UiOptions options = optionsPane.getOptions(); - testResult = null; - try { - Editor programEditor = editorsPane.getEditor(EditorCode.PROGRAM); - Program program = new ProgramParser().parse(programEditor.getEditorPane().getText(), - programEditor.getLoadedPath(), - programEditor.getLoadedFormat(), - options.getCflags()); - try { - Wmm targetModel = new ParserCat().parse(editorsPane.getEditor(EditorCode.TARGET_MM).getEditorPane().getText()); - testResult = new ReachabilityResult(program, targetModel, options); - } catch (Exception e){ - String msg = e.getMessage() == null? "Memory model cannot be parsed" : e.getMessage(); - showError(msg, "Target memory model error"); - } - } catch (Exception e){ - String msg = e.getMessage() == null? "Program cannot be parsed" : e.getMessage(); - Throwable cause = e.getCause(); - if(cause instanceof InputMismatchException exception) { - Token token = exception.getOffendingToken(); - msg = "Problem with \"" + token.getText() + "\" at line " + token.getLine(); - } - showError(msg, "Program error"); - } - } + } } diff --git a/ui/src/main/java/com/dat3m/ui/editor/Editor.java b/ui/src/main/java/com/dat3m/ui/editor/Editor.java index b7a21e333d..e703a5d08d 100644 --- a/ui/src/main/java/com/dat3m/ui/editor/Editor.java +++ b/ui/src/main/java/com/dat3m/ui/editor/Editor.java @@ -1,23 +1,22 @@ package com.dat3m.ui.editor; import com.google.common.collect.ImmutableSet; - -import javax.swing.*; -import javax.swing.border.TitledBorder; -import javax.swing.filechooser.FileNameExtensionFilter; - import org.fife.ui.rsyntaxtextarea.RSyntaxTextArea; import org.fife.ui.rsyntaxtextarea.SyntaxConstants; import org.fife.ui.rtextarea.RTextScrollPane; +import javax.swing.*; +import javax.swing.border.TitledBorder; +import javax.swing.filechooser.FileNameExtensionFilter; +import java.awt.*; import java.awt.event.ActionEvent; import java.awt.event.ActionListener; -import java.io.File; -import java.io.FileInputStream; -import java.io.FileWriter; -import java.io.IOException; -import java.io.InputStreamReader; -import java.util.*; +import java.awt.event.KeyAdapter; +import java.awt.event.KeyEvent; +import java.io.*; +import java.util.Arrays; +import java.util.HashSet; +import java.util.Set; import static com.dat3m.ui.utils.Utils.showError; import static java.lang.System.getProperty; @@ -64,6 +63,22 @@ public class Editor extends RTextScrollPane implements ActionListener { TitledBorder border = createTitledBorder(code.toString()); border.setTitleJustification(TitledBorder.CENTER); setBorder(border); + + editorPane.addKeyListener(new KeyAdapter() { + @Override + public void keyPressed(KeyEvent e) { + if (e.isControlDown() && e.getKeyChar() == '+') { + changeFontSize(1); + } else if (e.isControlDown() && e.getKeyChar() == '-') { + changeFontSize(-1); + } + } + }); + } + + private void changeFontSize(int change) { + Font scaledFont = new Font(Font.DIALOG, Font.PLAIN, editorPane.getFont().getSize() + change); + editorPane.setFont(scaledFont); } public void addActionListener(ActionListener actionListener){ diff --git a/ui/src/main/java/com/dat3m/ui/editor/EditorsPane.java b/ui/src/main/java/com/dat3m/ui/editor/EditorsPane.java index 98556c8622..75aa116aef 100644 --- a/ui/src/main/java/com/dat3m/ui/editor/EditorsPane.java +++ b/ui/src/main/java/com/dat3m/ui/editor/EditorsPane.java @@ -1,18 +1,16 @@ package com.dat3m.ui.editor; import com.google.common.collect.ImmutableMap; +import org.fife.ui.rsyntaxtextarea.RSyntaxTextArea; import javax.swing.*; import javax.swing.border.TitledBorder; - -import org.fife.ui.rsyntaxtextarea.RSyntaxTextArea; - import java.awt.*; public class EditorsPane { private final ImmutableMap editors = ImmutableMap.of( - EditorCode.PROGRAM, new Editor(EditorCode.PROGRAM, new RSyntaxTextArea(), "litmus", "c", "ll"), + EditorCode.PROGRAM, new Editor(EditorCode.PROGRAM, new RSyntaxTextArea(), "litmus", "c", "bpl", "ll"), EditorCode.TARGET_MM, new Editor(EditorCode.TARGET_MM, new RSyntaxTextArea(), "cat") ); diff --git a/ui/src/main/java/com/dat3m/ui/options/OptionsPane.java b/ui/src/main/java/com/dat3m/ui/options/OptionsPane.java index 063d819891..126aae95a8 100644 --- a/ui/src/main/java/com/dat3m/ui/options/OptionsPane.java +++ b/ui/src/main/java/com/dat3m/ui/options/OptionsPane.java @@ -1,7 +1,8 @@ package com.dat3m.ui.options; -import com.dat3m.dartagnan.configuration.Method; import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.configuration.Method; +import com.dat3m.dartagnan.configuration.Property; import com.dat3m.ui.button.ClearButton; import com.dat3m.ui.button.TestButton; import com.dat3m.ui.options.utils.ControlCode; @@ -15,6 +16,7 @@ import java.awt.event.ActionEvent; import java.awt.event.ActionListener; import java.util.Arrays; +import java.util.EnumSet; import java.util.Iterator; import static com.dat3m.ui.options.utils.Helper.solversOrderedValues; @@ -24,42 +26,49 @@ public class OptionsPane extends JPanel implements ActionListener { - public final static int OPTWIDTH = 300; - + public final static int OPTWIDTH = 300; + private final JLabel iconPane; private final Selector methodPane; private final Selector solverPane; - + private final Selector propertyPane; + private final Selector targetPane; private final BoundField boundField; private final TimeoutField timeoutField; - + private final JTextField cflagsField; private final JButton testButton; private final JButton clearButton; + private final JRadioButton showViolationField; + private final JTextPane consolePane; - public OptionsPane(){ - super(new GridLayout(1,0)); + public OptionsPane() { + super(new GridLayout(1, 0)); iconPane = new JLabel(); methodPane = new Selector<>(Method.orderedValues(), ControlCode.METHOD); methodPane.setSelectedItem(Method.getDefault()); - + solverPane = new Selector<>(solversOrderedValues(), ControlCode.SOLVER); solverPane.setSelectedItem(Solvers.Z3); + propertyPane = new Selector<>(Property.orderedValues(), ControlCode.PROPERTY); + solverPane.setSelectedItem(Property.PROGRAM_SPEC); + targetPane = new Selector<>(Arch.orderedValues(), ControlCode.TARGET); targetPane.setSelectedItem(Arch.getDefault()); - + boundField = new BoundField(); timeoutField = new TimeoutField(); - + showViolationField = new JRadioButton(); + cflagsField = new JTextField(); cflagsField.setColumns(20); @@ -73,34 +82,37 @@ public OptionsPane(){ mkGrid(); } - private void bindListeners(){ - // optionsPane needs to listen to options to clean the console - // Alias and Mode do not change the result and thus we don't listen to them - targetPane.addActionListener(this); - boundField.addActionListener(this); - timeoutField.addActionListener(this); - clearButton.addActionListener(this); + private void bindListeners() { + // optionsPane needs to listen to options to clean the console + // Alias and Mode do not change the result and thus we don't listen to them + targetPane.addActionListener(this); + boundField.addActionListener(this); + timeoutField.addActionListener(this); + clearButton.addActionListener(this); + propertyPane.addActionListener(this); } - public JButton getTestButton(){ + public JButton getTestButton() { return testButton; } - public JTextPane getConsolePane(){ + public JTextPane getConsolePane() { return consolePane; } - public UiOptions getOptions(){ + public UiOptions getOptions() { int bound = Integer.parseInt(boundField.getText()); int timeout = Integer.parseInt(timeoutField.getText()); + boolean showViolationGraph = showViolationField.isSelected(); String cflags = cflagsField.getText(); - Arch target = (Arch)targetPane.getSelectedItem(); - Method method = (Method)methodPane.getSelectedItem(); - Solvers solver = (Solvers)solverPane.getSelectedItem(); - return new UiOptions(target, method, bound, solver, timeout, cflags); + Arch target = (Arch) targetPane.getSelectedItem(); + Method method = (Method) methodPane.getSelectedItem(); + Solvers solver = (Solvers) solverPane.getSelectedItem(); + EnumSet properties = EnumSet.of((Property) propertyPane.getSelectedItem()); + return new UiOptions(target, method, bound, solver, timeout, showViolationGraph, cflags, properties); } - private void mkGrid(){ + private void mkGrid() { JScrollPane scrollConsole = new JScrollPane(consolePane); scrollConsole.setMaximumSize(new Dimension(OPTWIDTH, 120)); @@ -120,23 +132,27 @@ private void mkGrid(){ cflagsPane.add(new JLabel("CFLAGS: ")); cflagsPane.add(cflagsField); + JPanel showViolationPane = new JPanel(new FlowLayout(LEFT)); + showViolationPane.add(new JLabel("Show violation graph")); + showViolationPane.add(showViolationField); + // Inner borders Border emptyBorder = BorderFactory.createEmptyBorder(); JSplitPane graphPane = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT); graphPane.setDividerSize(0); - JComponent[] panes = { targetPane, methodPane, solverPane, boundsPane, cflagsPane, testButton, clearButton, graphPane, scrollConsole }; + JComponent[] panes = {targetPane, methodPane, solverPane, propertyPane, boundsPane, showViolationPane, cflagsPane, testButton, clearButton, graphPane, scrollConsole}; Iterator it = Arrays.asList(panes).iterator(); JComponent current = iconPane; current.setBorder(emptyBorder); - while(it.hasNext()) { - JComponent next = it.next(); - current = new JSplitPane(JSplitPane.VERTICAL_SPLIT, current, next); - ((JSplitPane)current).setDividerSize(2); - current.setBorder(emptyBorder); - if(!(next instanceof JButton)) { - next.setBorder(emptyBorder); - } + while (it.hasNext()) { + JComponent next = it.next(); + current = new JSplitPane(JSplitPane.VERTICAL_SPLIT, current, next); + ((JSplitPane) current).setDividerSize(2); + current.setBorder(emptyBorder); + if (!(next instanceof JButton)) { + next.setBorder(emptyBorder); + } } add(current); @@ -146,9 +162,9 @@ private void mkGrid(){ setBorder(titledBorder); } - @Override - public void actionPerformed(ActionEvent e) { - // Any change in the (relevant) options clears the console - getConsolePane().setText(""); - } + @Override + public void actionPerformed(ActionEvent e) { + // Any change in the (relevant) options clears the console + getConsolePane().setText(""); + } } \ No newline at end of file diff --git a/ui/src/main/java/com/dat3m/ui/options/utils/ControlCode.java b/ui/src/main/java/com/dat3m/ui/options/utils/ControlCode.java index 23c4632bc0..03e09dbdad 100644 --- a/ui/src/main/java/com/dat3m/ui/options/utils/ControlCode.java +++ b/ui/src/main/java/com/dat3m/ui/options/utils/ControlCode.java @@ -2,7 +2,7 @@ public enum ControlCode { - TASK, TARGET, BOUND, TIMEOUT, TEST, CLEAR, METHOD, SOLVER; + TASK, TARGET, BOUND, TIMEOUT, TEST, CLEAR, METHOD, SOLVER, PROPERTY; @Override public String toString(){ @@ -23,6 +23,8 @@ public String toString(){ return "Method"; case SOLVER: return "Solver"; + case PROPERTY: + return "Property"; } return super.toString(); } @@ -45,6 +47,8 @@ public String actionCommand(){ return "control_command_method"; case SOLVER: return "control_command_solver"; + case PROPERTY: + return "control_command_property"; } throw new RuntimeException("Illegal EditorCode"); } diff --git a/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java b/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java index 00464c2df8..1953d9ee69 100644 --- a/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java +++ b/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java @@ -1,12 +1,14 @@ package com.dat3m.ui.result; import com.dat3m.dartagnan.Dartagnan; +import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.verification.VerificationTask; -import com.dat3m.dartagnan.verification.solving.*; +import com.dat3m.dartagnan.verification.solving.AssumeSolver; +import com.dat3m.dartagnan.verification.solving.ModelChecker; +import com.dat3m.dartagnan.verification.solving.RefinementSolver; +import com.dat3m.dartagnan.witness.WitnessType; import com.dat3m.dartagnan.wmm.Wmm; -import com.dat3m.dartagnan.configuration.Arch; -import com.dat3m.dartagnan.configuration.Property; import com.dat3m.ui.utils.UiOptions; import com.dat3m.ui.utils.Utils; import org.sosy_lab.common.ShutdownManager; @@ -16,6 +18,9 @@ import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; + +import java.io.File; + import static com.dat3m.dartagnan.configuration.OptionNames.PHANTOM_REFERENCES; public class ReachabilityResult { @@ -25,78 +30,87 @@ public class ReachabilityResult { private final UiOptions options; private String verdict; + private File violationModel; - public ReachabilityResult(Program program, Wmm wmm, UiOptions options){ + + public ReachabilityResult(Program program, Wmm wmm, UiOptions options) { this.program = program; this.wmm = wmm; this.options = options; run(); } - public String getVerdict(){ + public String getVerdict() { return verdict; } - private void run(){ - if(validate()){ + public boolean hasViolationModel() { + return violationModel != null; + } + + public File getViolationModelFile() { + return violationModel; + } + + private void run() { + if (validate()) { ShutdownManager sdm = ShutdownManager.create(); - Thread t = new Thread(() -> { - try { - if(options.getTimeout() > 0) { - // Converts timeout from secs to millisecs - Thread.sleep(1000L * options.getTimeout()); - sdm.requestShutdown("Shutdown Request"); - } - } catch (InterruptedException e) { - // Verification ended, nothing to be done. - }}); + Thread t = new Thread(() -> { + try { + if (options.timeout() > 0) { + // Converts timeout from secs to millisecs + Thread.sleep(1000L * options.timeout()); + sdm.requestShutdown("Shutdown Request"); + } + } catch (InterruptedException e) { + // Verification ended, nothing to be done. + } + }); try { ModelChecker modelChecker; - Arch arch = program.getArch() != null ? program.getArch() : options.getTarget(); + Arch arch = program.getArch() != null ? program.getArch() : options.target(); VerificationTask task = VerificationTask.builder() - .withBound(options.getBound()) - .withSolverTimeout(options.getTimeout()) + .withBound(options.bound()) + .withSolverTimeout(options.timeout()) .withTarget(arch) - .build(program, wmm, Property.getDefault()); + .build(program, wmm, options.properties()); - t.start(); + t.start(); Configuration config = Configuration.builder() - .setOption(PHANTOM_REFERENCES, "true") - .build(); - try (SolverContext ctx = SolverContextFactory.createSolverContext( + .setOption(PHANTOM_REFERENCES, "true") + .build(); + try (SolverContext ctx = SolverContextFactory.createSolverContext( config, BasicLogManager.create(config), sdm.getNotifier(), - options.getSolver()); + options.solver()); ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { - switch (options.getMethod()) { - case EAGER: - modelChecker = AssumeSolver.run(ctx, prover, task); - break; - case LAZY: - modelChecker = RefinementSolver.run(ctx, prover, task); - break; - default: - throw new IllegalArgumentException("method " + options.getMethod()); - } + modelChecker = switch (options.method()) { + case EAGER -> AssumeSolver.run(ctx, prover, task); + case LAZY -> RefinementSolver.run(ctx, prover, task); + }; // Verification ended, we can interrupt the timeout Thread t.interrupt(); verdict = Dartagnan.generateResultSummary(task, prover, modelChecker); + + if (modelChecker.hasModel()) { + violationModel = Dartagnan.generateExecutionGraphFile(task, prover, modelChecker, WitnessType.PNG); + } } - } catch (InterruptedException e){ - verdict = "TIMEOUT"; + } catch (InterruptedException e) { + verdict = "TIMEOUT"; } catch (Exception e) { - verdict = "ERROR: " + e.getMessage(); + verdict = "ERROR: " + e.getMessage(); } } } - private boolean validate(){ - Arch target = program.getArch() == null ? options.getTarget() : program.getArch(); - if(target == null) { + private boolean validate() { + Arch target = program.getArch() == null ? options.target() : program.getArch(); + if (target == null) { Utils.showError("Missing target architecture."); return false; } diff --git a/ui/src/main/java/com/dat3m/ui/utils/UiOptions.java b/ui/src/main/java/com/dat3m/ui/utils/UiOptions.java index bb76a0a1e3..1700056293 100644 --- a/ui/src/main/java/com/dat3m/ui/utils/UiOptions.java +++ b/ui/src/main/java/com/dat3m/ui/utils/UiOptions.java @@ -1,48 +1,14 @@ package com.dat3m.ui.utils; -import com.dat3m.dartagnan.configuration.Method; import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.configuration.Method; +import com.dat3m.dartagnan.configuration.Property; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; -public class UiOptions { - - private final Arch target; - private final Method method; - private final int bound; - private final Solvers solver; - private final int timeout; - private final String cflags; - - public UiOptions(Arch target, Method method, int bound, Solvers solver, int timeout, String cflags) { - this.target = target; - this.method = method; - this.bound = bound; - this.solver = solver; - this.timeout = timeout; - this.cflags = cflags; - } - - public Arch getTarget(){ - return target; - } - - public Method getMethod() { - return method; - } +import java.util.EnumSet; - public int getBound() { - return bound; - } +public record UiOptions(Arch target, Method method, int bound, Solvers solver, int timeout, boolean showViolationGraph, + String cflags, EnumSet properties) { - public Solvers getSolver() { - return solver; - } - public int getTimeout() { - return timeout; - } - - public String getCflags(){ - return cflags; - } } \ No newline at end of file diff --git a/ui/src/main/java/com/dat3m/ui/utils/Utils.java b/ui/src/main/java/com/dat3m/ui/utils/Utils.java index 8893b8d59c..707009f710 100644 --- a/ui/src/main/java/com/dat3m/ui/utils/Utils.java +++ b/ui/src/main/java/com/dat3m/ui/utils/Utils.java @@ -1,24 +1,21 @@ package com.dat3m.ui.utils; -import java.awt.Dimension; - -import javax.swing.JOptionPane; -import javax.swing.JScrollPane; -import javax.swing.JTextArea; +import javax.swing.*; +import java.awt.*; public class Utils { - - public static void showError(String msg, String title){ - JTextArea textArea = new JTextArea(msg); - JScrollPane scrollPane = new JScrollPane(textArea); - Dimension size = new Dimension( Math.min(textArea.getPreferredSize().width + 1, 1000) , - Math.min(textArea.getPreferredSize().height + 1, 500) ); - scrollPane.setPreferredSize( size ); - JOptionPane.showMessageDialog(null, scrollPane, title, - JOptionPane.ERROR_MESSAGE); + + public static void showError(String msg, String title) { + JTextArea textArea = new JTextArea(msg); + JScrollPane scrollPane = new JScrollPane(textArea); + Dimension size = new Dimension(Math.min(textArea.getPreferredSize().width + 1, 1000), + Math.min(textArea.getPreferredSize().height + 1, 500)); + scrollPane.setPreferredSize(size); + JOptionPane.showMessageDialog(null, scrollPane, title, + JOptionPane.ERROR_MESSAGE); } - public static void showError(String msg){ - showError(msg, "Error"); + public static void showError(String msg) { + showError(msg, "Error"); } } From 10065ffdf970b5e0560215704d2d20ae8af42f36 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Tue, 28 May 2024 15:02:03 +0200 Subject: [PATCH 3/9] Added ability to pass configuration options via the UI. Some refactoring --- .../main/java/com/dat3m/ui/editor/Editor.java | 56 +++++------ .../java/com/dat3m/ui/editor/EditorCode.java | 52 ++++------ .../java/com/dat3m/ui/editor/EditorsPane.java | 16 +-- .../com/dat3m/ui/options/OptionsPane.java | 18 +++- .../dat3m/ui/result/ReachabilityResult.java | 98 ++++++++++--------- .../java/com/dat3m/ui/utils/UiOptions.java | 2 +- 6 files changed, 122 insertions(+), 120 deletions(-) diff --git a/ui/src/main/java/com/dat3m/ui/editor/Editor.java b/ui/src/main/java/com/dat3m/ui/editor/Editor.java index e703a5d08d..671342e838 100644 --- a/ui/src/main/java/com/dat3m/ui/editor/Editor.java +++ b/ui/src/main/java/com/dat3m/ui/editor/Editor.java @@ -38,7 +38,7 @@ public class Editor extends RTextScrollPane implements ActionListener { private Set actionListeners = new HashSet<>(); - Editor(EditorCode code, RSyntaxTextArea editorPane, String... formats){ + Editor(EditorCode code, RSyntaxTextArea editorPane, String... formats) { super(editorPane); this.code = code; this.editorPane = editorPane; @@ -50,10 +50,10 @@ public class Editor extends RTextScrollPane implements ActionListener { this.exporterItem = new JMenuItem(code.toString()); exporterItem.setActionCommand(code.editorMenuExportActionCommand()); exporterItem.addActionListener(this); - + this.allowedFormats = ImmutableSet.copyOf(Arrays.asList(formats)); this.chooser = new JFileChooser(); - for(String format : allowedFormats) { + for (String format : allowedFormats) { chooser.addChoosableFileFilter(new FileNameExtensionFilter("*." + format, format)); } @@ -81,78 +81,78 @@ private void changeFontSize(int change) { editorPane.setFont(scaledFont); } - public void addActionListener(ActionListener actionListener){ + public void addActionListener(ActionListener actionListener) { actionListeners.add(actionListener); } - public String getLoadedFormat(){ + public String getLoadedFormat() { return loadedFormat; } - public String getLoadedPath(){ + public String getLoadedPath() { return loadedPath; } @Override public void actionPerformed(ActionEvent event) { - if(code.editorMenuImportActionCommand().equals(event.getActionCommand())){ + if (code.editorMenuImportActionCommand().equals(event.getActionCommand())) { chooser.setCurrentDirectory(new File(getProperty("user.dir") + "/..")); - if(chooser.showOpenDialog(null) == APPROVE_OPTION){ + if (chooser.showOpenDialog(null) == APPROVE_OPTION) { String path = chooser.getSelectedFile().getPath(); loadedPath = path.substring(0, path.lastIndexOf('/') + 1); String format = path.substring(path.lastIndexOf('.') + 1).trim(); - if(allowedFormats.contains(format)){ + if (allowedFormats.contains(format)) { loadedFormat = format; notifyListeners(); try { editorPane.read(new InputStreamReader(new FileInputStream(path)), null); } catch (IOException e) { - showError("Error reading input file"); + showError("Error reading input file"); } } else { - showError("Please select a *." + String.join(", *.", allowedFormats) + " file", + showError("Please select a *." + String.join(", *.", allowedFormats) + " file", "Invalid file format"); } } } - if(code.editorMenuExportActionCommand().equals(event.getActionCommand())){ + if (code.editorMenuExportActionCommand().equals(event.getActionCommand())) { chooser.setCurrentDirectory(new File(getProperty("user.dir") + "/..")); - if(chooser.showSaveDialog(null) == APPROVE_OPTION){ + if (chooser.showSaveDialog(null) == APPROVE_OPTION) { String path = chooser.getSelectedFile().getPath(); String format = path.substring(path.lastIndexOf('.') + 1).trim(); - if(allowedFormats.contains(format)){ + if (allowedFormats.contains(format)) { notifyListeners(); - try { - File newTextFile = new File(path); - FileWriter fw = new FileWriter(newTextFile); - fw.write(editorPane.getText()); - fw.close(); - } catch (IOException e) { - // This should never happen since the file is created above - } + try { + File newTextFile = new File(path); + FileWriter fw = new FileWriter(newTextFile); + fw.write(editorPane.getText()); + fw.close(); + } catch (IOException e) { + // This should never happen since the file is created above + } } else { - showError("Please select a *." + String.join(", *.", allowedFormats) + " file", + showError("Please select a *." + String.join(", *.", allowedFormats) + " file", "Invalid file format"); } } } } - JMenuItem getImporterItem(){ + JMenuItem getImporterItem() { return importerItem; } - JMenuItem getExporterItem(){ + JMenuItem getExporterItem() { return exporterItem; } - public RSyntaxTextArea getEditorPane(){ + public RSyntaxTextArea getEditorPane() { return editorPane; } - private void notifyListeners(){ + private void notifyListeners() { ActionEvent dataLoadedEvent = new ActionEvent(this, ActionEvent.ACTION_PERFORMED, code.editorActionCommand()); - for(ActionListener actionListener : actionListeners){ + for (ActionListener actionListener : actionListeners) { actionListener.actionPerformed(dataLoadedEvent); } } diff --git a/ui/src/main/java/com/dat3m/ui/editor/EditorCode.java b/ui/src/main/java/com/dat3m/ui/editor/EditorCode.java index 6b62380248..88c9566448 100644 --- a/ui/src/main/java/com/dat3m/ui/editor/EditorCode.java +++ b/ui/src/main/java/com/dat3m/ui/editor/EditorCode.java @@ -5,43 +5,31 @@ public enum EditorCode { PROGRAM, TARGET_MM; @Override - public String toString(){ - switch(this){ - case PROGRAM: - return "Program"; - case TARGET_MM: - return "Target Memory Model"; - } - return super.toString(); + public String toString() { + return switch (this) { + case PROGRAM -> "Program"; + case TARGET_MM -> "Target Memory Model"; + }; } - public String editorMenuImportActionCommand(){ - switch(this){ - case PROGRAM: - return "editor_menu_import_action_program"; - case TARGET_MM: - return "editor_menu_import_action_target_mm"; - } - throw new RuntimeException("Illegal EditorCode"); + public String editorMenuImportActionCommand() { + return switch (this) { + case PROGRAM -> "editor_menu_import_action_program"; + case TARGET_MM -> "editor_menu_import_action_target_mm"; + }; } - public String editorMenuExportActionCommand(){ - switch(this){ - case PROGRAM: - return "editor_menu_export_action_program"; - case TARGET_MM: - return "editor_menu_export_action_target_mm"; - } - throw new RuntimeException("Illegal EditorCode"); + public String editorMenuExportActionCommand() { + return switch (this) { + case PROGRAM -> "editor_menu_export_action_program"; + case TARGET_MM -> "editor_menu_export_action_target_mm"; + }; } - public String editorActionCommand(){ - switch(this){ - case PROGRAM: - return "editor_action_program"; - case TARGET_MM: - return "editor_action_target_mm"; - } - throw new RuntimeException("Illegal EditorCode"); + public String editorActionCommand() { + return switch (this) { + case PROGRAM -> "editor_action_program"; + case TARGET_MM -> "editor_action_target_mm"; + }; } } diff --git a/ui/src/main/java/com/dat3m/ui/editor/EditorsPane.java b/ui/src/main/java/com/dat3m/ui/editor/EditorsPane.java index 75aa116aef..24bf815f37 100644 --- a/ui/src/main/java/com/dat3m/ui/editor/EditorsPane.java +++ b/ui/src/main/java/com/dat3m/ui/editor/EditorsPane.java @@ -19,7 +19,7 @@ EditorCode.TARGET_MM, new Editor(EditorCode.TARGET_MM, new RSyntaxTextArea(), "c private final JMenu menuImporter; private final JMenu menuExporter; - public EditorsPane(){ + public EditorsPane() { menuImporter = new JMenu("Import"); menuImporter.add(editors.get(EditorCode.PROGRAM).getImporterItem()); menuImporter.add(editors.get(EditorCode.TARGET_MM).getImporterItem()); @@ -29,10 +29,10 @@ public EditorsPane(){ menuExporter.add(editors.get(EditorCode.TARGET_MM).getExporterItem()); Dimension screenDimension = Toolkit.getDefaultToolkit().getScreenSize(); - Dimension editorsDimension = new Dimension((int)(screenDimension.getWidth() *1/3), (int)screenDimension.getHeight()); - editors.get(EditorCode.PROGRAM).setPreferredSize(editorsDimension); + Dimension editorsDimension = new Dimension((int) (screenDimension.getWidth() * 1 / 3), (int) screenDimension.getHeight()); + editors.get(EditorCode.PROGRAM).setPreferredSize(editorsDimension); editors.get(EditorCode.TARGET_MM).setPreferredSize(editorsDimension); - + mmPane = new JSplitPane(JSplitPane.VERTICAL_SPLIT); mmPane.setBottomComponent(editors.get(EditorCode.TARGET_MM)); mmPane.setOneTouchExpandable(true); @@ -46,19 +46,19 @@ public EditorsPane(){ mainPane.setBorder(new TitledBorder("")); } - public JMenu getMenuImporter(){ + public JMenu getMenuImporter() { return menuImporter; } - public JMenu getMenuExporter(){ + public JMenu getMenuExporter() { return menuExporter; } - public JSplitPane getMainPane(){ + public JSplitPane getMainPane() { return mainPane; } - public Editor getEditor(EditorCode code){ + public Editor getEditor(EditorCode code) { return editors.get(code); } } diff --git a/ui/src/main/java/com/dat3m/ui/options/OptionsPane.java b/ui/src/main/java/com/dat3m/ui/options/OptionsPane.java index 126aae95a8..1404160a42 100644 --- a/ui/src/main/java/com/dat3m/ui/options/OptionsPane.java +++ b/ui/src/main/java/com/dat3m/ui/options/OptionsPane.java @@ -40,6 +40,7 @@ public class OptionsPane extends JPanel implements ActionListener { private final TimeoutField timeoutField; private final JTextField cflagsField; + private final JTextField configField; private final JButton testButton; private final JButton clearButton; @@ -72,6 +73,9 @@ public OptionsPane() { cflagsField = new JTextField(); cflagsField.setColumns(20); + configField = new JTextField(); + configField.setColumns(20); + testButton = new TestButton(); clearButton = new ClearButton(); @@ -84,7 +88,7 @@ public OptionsPane() { private void bindListeners() { // optionsPane needs to listen to options to clean the console - // Alias and Mode do not change the result and thus we don't listen to them + // Alias and Mode do not change the result, and thus we don't listen to them targetPane.addActionListener(this); boundField.addActionListener(this); timeoutField.addActionListener(this); @@ -104,12 +108,13 @@ public UiOptions getOptions() { int bound = Integer.parseInt(boundField.getText()); int timeout = Integer.parseInt(timeoutField.getText()); boolean showViolationGraph = showViolationField.isSelected(); - String cflags = cflagsField.getText(); + String cflags = cflagsField.getText().strip(); + String config = configField.getText().strip(); Arch target = (Arch) targetPane.getSelectedItem(); Method method = (Method) methodPane.getSelectedItem(); Solvers solver = (Solvers) solverPane.getSelectedItem(); EnumSet properties = EnumSet.of((Property) propertyPane.getSelectedItem()); - return new UiOptions(target, method, bound, solver, timeout, showViolationGraph, cflags, properties); + return new UiOptions(target, method, bound, solver, timeout, showViolationGraph, cflags, config, properties); } private void mkGrid() { @@ -132,6 +137,10 @@ private void mkGrid() { cflagsPane.add(new JLabel("CFLAGS: ")); cflagsPane.add(cflagsField); + JPanel configPane = new JPanel(new FlowLayout(LEFT)); + configPane.add(new JLabel("Config: ")); + configPane.add(configField); + JPanel showViolationPane = new JPanel(new FlowLayout(LEFT)); showViolationPane.add(new JLabel("Show violation graph")); showViolationPane.add(showViolationField); @@ -141,7 +150,8 @@ private void mkGrid() { JSplitPane graphPane = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT); graphPane.setDividerSize(0); - JComponent[] panes = {targetPane, methodPane, solverPane, propertyPane, boundsPane, showViolationPane, cflagsPane, testButton, clearButton, graphPane, scrollConsole}; + JComponent[] panes = { targetPane, methodPane, solverPane, propertyPane, boundsPane, showViolationPane, cflagsPane, + configPane, testButton, clearButton, graphPane, scrollConsole }; Iterator it = Arrays.asList(panes).iterator(); JComponent current = iconPane; current.setBorder(emptyBorder); diff --git a/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java b/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java index 1953d9ee69..561e722583 100644 --- a/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java +++ b/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java @@ -53,58 +53,62 @@ public File getViolationModelFile() { } private void run() { - if (validate()) { - - ShutdownManager sdm = ShutdownManager.create(); - Thread t = new Thread(() -> { - try { - if (options.timeout() > 0) { - // Converts timeout from secs to millisecs - Thread.sleep(1000L * options.timeout()); - sdm.requestShutdown("Shutdown Request"); - } - } catch (InterruptedException e) { - // Verification ended, nothing to be done. - } - }); + if (!validate()) { + return; + } + final ShutdownManager sdm = ShutdownManager.create(); + final Thread t = new Thread(() -> { try { - ModelChecker modelChecker; - Arch arch = program.getArch() != null ? program.getArch() : options.target(); - VerificationTask task = VerificationTask.builder() - .withBound(options.bound()) - .withSolverTimeout(options.timeout()) - .withTarget(arch) - .build(program, wmm, options.properties()); - - t.start(); - Configuration config = Configuration.builder() - .setOption(PHANTOM_REFERENCES, "true") - .build(); - try (SolverContext ctx = SolverContextFactory.createSolverContext( - config, - BasicLogManager.create(config), - sdm.getNotifier(), - options.solver()); - ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { - - modelChecker = switch (options.method()) { - case EAGER -> AssumeSolver.run(ctx, prover, task); - case LAZY -> RefinementSolver.run(ctx, prover, task); - }; - // Verification ended, we can interrupt the timeout Thread - t.interrupt(); - verdict = Dartagnan.generateResultSummary(task, prover, modelChecker); - - if (modelChecker.hasModel()) { - violationModel = Dartagnan.generateExecutionGraphFile(task, prover, modelChecker, WitnessType.PNG); - } + if (options.timeout() > 0) { + // Converts timeout from secs to millisecs + Thread.sleep(1000L * options.timeout()); + sdm.requestShutdown("Shutdown Request"); } } catch (InterruptedException e) { - verdict = "TIMEOUT"; - } catch (Exception e) { - verdict = "ERROR: " + e.getMessage(); + // Verification ended, nothing to be done. + } + }); + + try { + final Arch arch = program.getArch() != null ? program.getArch() : options.target(); + final Configuration config = options.config().isEmpty() ? + Configuration.defaultConfiguration() : + Configuration.fromCmdLineArguments(options.config().split(" ")); + final VerificationTask task = VerificationTask.builder() + .withConfig(config) + .withBound(options.bound()) + .withSolverTimeout(options.timeout()) + .withTarget(arch) + .build(program, wmm, options.properties()); + + t.start(); + final Configuration solverConfig = Configuration.builder() + .setOption(PHANTOM_REFERENCES, "true") + .build(); + try (SolverContext ctx = SolverContextFactory.createSolverContext( + solverConfig, + BasicLogManager.create(solverConfig), + sdm.getNotifier(), + options.solver()); + ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + + final ModelChecker modelChecker; modelChecker = switch (options.method()) { + case EAGER -> AssumeSolver.run(ctx, prover, task); + case LAZY -> RefinementSolver.run(ctx, prover, task); + }; + // Verification ended, we can interrupt the timeout Thread + t.interrupt(); + verdict = Dartagnan.generateResultSummary(task, prover, modelChecker); + + if (modelChecker.hasModel()) { + violationModel = Dartagnan.generateExecutionGraphFile(task, prover, modelChecker, WitnessType.PNG); + } } + } catch (InterruptedException e) { + verdict = "TIMEOUT"; + } catch (Exception e) { + verdict = "ERROR: " + e; } } diff --git a/ui/src/main/java/com/dat3m/ui/utils/UiOptions.java b/ui/src/main/java/com/dat3m/ui/utils/UiOptions.java index 1700056293..9bcf5665cd 100644 --- a/ui/src/main/java/com/dat3m/ui/utils/UiOptions.java +++ b/ui/src/main/java/com/dat3m/ui/utils/UiOptions.java @@ -8,7 +8,7 @@ import java.util.EnumSet; public record UiOptions(Arch target, Method method, int bound, Solvers solver, int timeout, boolean showViolationGraph, - String cflags, EnumSet properties) { + String cflags, String config, EnumSet properties) { } \ No newline at end of file From 97544490572253867497d4eaa24cbabb734a570f Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Tue, 28 May 2024 15:05:49 +0200 Subject: [PATCH 4/9] Formatting of UI code. Deleted unused UI class. --- .../java/com/dat3m/ui/button/ClearButton.java | 17 ++- .../java/com/dat3m/ui/button/TestButton.java | 17 ++- .../com/dat3m/ui/editor/LineNumbersView.java | 82 -------------- .../main/java/com/dat3m/ui/icon/IconCode.java | 29 ++--- .../com/dat3m/ui/listener/BoundListener.java | 100 +++++++++--------- .../com/dat3m/ui/listener/EditorListener.java | 39 ++++--- .../dat3m/ui/listener/TimeoutListener.java | 100 +++++++++--------- .../java/com/dat3m/ui/options/BoundField.java | 49 +++++---- .../java/com/dat3m/ui/options/BoundPane.java | 12 +-- .../com/dat3m/ui/options/TimeoutField.java | 49 +++++---- .../com/dat3m/ui/options/TimeoutPane.java | 12 +-- .../dat3m/ui/options/utils/ControlCode.java | 68 +++++------- .../com/dat3m/ui/options/utils/Helper.java | 16 +-- 13 files changed, 236 insertions(+), 354 deletions(-) delete mode 100644 ui/src/main/java/com/dat3m/ui/editor/LineNumbersView.java diff --git a/ui/src/main/java/com/dat3m/ui/button/ClearButton.java b/ui/src/main/java/com/dat3m/ui/button/ClearButton.java index 2176e77a9e..b085b6d696 100644 --- a/ui/src/main/java/com/dat3m/ui/button/ClearButton.java +++ b/ui/src/main/java/com/dat3m/ui/button/ClearButton.java @@ -1,18 +1,17 @@ package com.dat3m.ui.button; -import static com.dat3m.ui.options.OptionsPane.OPTWIDTH; - -import java.awt.Dimension; +import com.dat3m.ui.options.utils.ControlCode; -import javax.swing.JButton; +import javax.swing.*; +import java.awt.*; -import com.dat3m.ui.options.utils.ControlCode; +import static com.dat3m.ui.options.OptionsPane.OPTWIDTH; public class ClearButton extends JButton { - public ClearButton() { - super("Clear Console"); + public ClearButton() { + super("Clear Console"); setActionCommand(ControlCode.CLEAR.actionCommand()); - setMaximumSize(new Dimension(OPTWIDTH, 50)); - } + setMaximumSize(new Dimension(OPTWIDTH, 50)); + } } diff --git a/ui/src/main/java/com/dat3m/ui/button/TestButton.java b/ui/src/main/java/com/dat3m/ui/button/TestButton.java index 1626ea1895..bad7f7694a 100644 --- a/ui/src/main/java/com/dat3m/ui/button/TestButton.java +++ b/ui/src/main/java/com/dat3m/ui/button/TestButton.java @@ -1,18 +1,17 @@ package com.dat3m.ui.button; -import static com.dat3m.ui.options.OptionsPane.OPTWIDTH; - -import java.awt.Dimension; +import com.dat3m.ui.options.utils.ControlCode; -import javax.swing.JButton; +import javax.swing.*; +import java.awt.*; -import com.dat3m.ui.options.utils.ControlCode; +import static com.dat3m.ui.options.OptionsPane.OPTWIDTH; public class TestButton extends JButton { - public TestButton() { - super("Test"); + public TestButton() { + super("Test"); setActionCommand(ControlCode.TEST.actionCommand()); - setMaximumSize(new Dimension(OPTWIDTH, 50)); - } + setMaximumSize(new Dimension(OPTWIDTH, 50)); + } } diff --git a/ui/src/main/java/com/dat3m/ui/editor/LineNumbersView.java b/ui/src/main/java/com/dat3m/ui/editor/LineNumbersView.java deleted file mode 100644 index 74558dfa6e..0000000000 --- a/ui/src/main/java/com/dat3m/ui/editor/LineNumbersView.java +++ /dev/null @@ -1,82 +0,0 @@ -package com.dat3m.ui.editor; - -import static java.lang.String.valueOf; -import static javax.swing.text.Utilities.getRowEnd; - -import java.awt.Color; -import java.awt.Dimension; -import java.awt.Font; -import java.awt.Graphics; -import java.awt.Point; -import java.awt.Rectangle; -import java.awt.event.ActionEvent; -import java.awt.event.ActionListener; -import javax.swing.JComponent; -import javax.swing.event.CaretEvent; -import javax.swing.event.CaretListener; -import javax.swing.text.BadLocationException; -import javax.swing.text.Element; -import javax.swing.text.JTextComponent; - -class LineNumbersView extends JComponent implements CaretListener, ActionListener { - - private final JTextComponent editor; - - LineNumbersView(JTextComponent editor) { - this.editor = editor; - editor.addCaretListener(this); - Dimension size = new Dimension(28, editor.getHeight()); - setPreferredSize(size); - setSize(size); - } - - @Override - public void paintComponent(Graphics g) { - super.paintComponent(g); - - Rectangle clip = g.getClipBounds(); - int currentOffset = editor.viewToModel(new Point(0, clip.y)); - int endOffset = editor.viewToModel(new Point(0, clip.y + clip.height)); - - while (currentOffset <= endOffset) { - try { - // Computes the line number based on the offset - int lineNumber = editor.getDocument().getDefaultRootElement().getElementIndex(currentOffset) + 1; - // x position of the line number is fixed - int x = getInsets().left + 2; - // y position is different for each line number - int y = getOffsetY(currentOffset); - - g.setFont(new Font(Font.MONOSPACED, Font.BOLD, editor.getFont().getSize())); - g.setColor(isCurrentLine(currentOffset) ? Color.RED : Color.BLACK); - g.drawString(valueOf(lineNumber), x, y); - - // Update offset - currentOffset = getRowEnd(editor, currentOffset) + 1; - } catch (BadLocationException e) { - e.printStackTrace(); - } - } - } - - private int getOffsetY(int offset) throws BadLocationException { - int descent = editor.getFontMetrics(editor.getFont()).getDescent(); - Rectangle r = editor.modelToView(offset); - return r.y + r.height - descent; - } - - private boolean isCurrentLine(int offset) { - Element root = editor.getDocument().getDefaultRootElement(); - return root.getElementIndex(offset) == root.getElementIndex(editor.getCaretPosition()); - } - - @Override - public void caretUpdate(CaretEvent e) { - repaint(); - } - - @Override - public void actionPerformed(ActionEvent e) { - repaint(); - } -} \ No newline at end of file diff --git a/ui/src/main/java/com/dat3m/ui/icon/IconCode.java b/ui/src/main/java/com/dat3m/ui/icon/IconCode.java index b75b920535..c6e6d6a9f7 100644 --- a/ui/src/main/java/com/dat3m/ui/icon/IconCode.java +++ b/ui/src/main/java/com/dat3m/ui/icon/IconCode.java @@ -5,31 +5,24 @@ import java.net.URL; public enum IconCode { - DAT3M, DARTAGNAN; @Override - public String toString(){ - switch(this){ - case DAT3M: - return "Dat3M"; - case DARTAGNAN: - return "Dartagnan"; - } - return super.toString(); + public String toString() { + return switch (this) { + case DAT3M -> "Dat3M"; + case DARTAGNAN -> "Dartagnan"; + }; } - public URL getPath(){ - switch(this){ - case DAT3M: - return getResource("/dat3m.png"); - case DARTAGNAN: - return getResource("/dartagnan.jpg"); - } - throw new RuntimeException("Illegal IconCode option"); + public URL getPath() { + return switch (this) { + case DAT3M -> getResource("/dat3m.png"); + case DARTAGNAN -> getResource("/dartagnan.jpg"); + }; } - private URL getResource(String filename){ + private URL getResource(String filename) { return Dat3M.class.getResource(filename); } } diff --git a/ui/src/main/java/com/dat3m/ui/listener/BoundListener.java b/ui/src/main/java/com/dat3m/ui/listener/BoundListener.java index 57cea9c509..295f3b5ec3 100644 --- a/ui/src/main/java/com/dat3m/ui/listener/BoundListener.java +++ b/ui/src/main/java/com/dat3m/ui/listener/BoundListener.java @@ -1,66 +1,66 @@ package com.dat3m.ui.listener; -import static com.dat3m.ui.utils.Utils.showError; +import com.dat3m.ui.options.BoundField; import java.awt.event.FocusEvent; import java.awt.event.FocusListener; import java.awt.event.KeyEvent; import java.awt.event.KeyListener; -import com.dat3m.ui.options.BoundField; +import static com.dat3m.ui.utils.Utils.showError; public class BoundListener implements KeyListener, FocusListener { - - private BoundField boundPane; - public BoundListener(BoundField pane) { - this.boundPane = pane; - } - - @Override - public void keyPressed(KeyEvent e) { - runTest(); - } + private BoundField boundPane; + + public BoundListener(BoundField pane) { + this.boundPane = pane; + } + + @Override + public void keyPressed(KeyEvent e) { + runTest(); + } + + @Override + public void keyReleased(KeyEvent e) { + runTest(); + } - @Override - public void keyReleased(KeyEvent e) { - runTest(); - } + @Override + public void keyTyped(KeyEvent e) { + runTest(); + } - @Override - public void keyTyped(KeyEvent e) { - runTest(); - } - - private void runTest() { - String cText = boundPane.getText(); - try { - int cBound = Integer.parseInt(cText); - if(cBound <= 0) { - showError("The bound should be greater than 1", "Option error"); - boundPane.setText(boundPane.getStableBound()); - } - boundPane.setStableBound(cText); - } catch (Exception e) { - // Empty string is allowed here to allow deleting. It will be handled by focusLost - if(cText.isEmpty()) { - return; - } - boundPane.setText(boundPane.getStableBound()); - showError("The bound should be greater than 1", "Option error"); - } - } + private void runTest() { + String cText = boundPane.getText(); + try { + int cBound = Integer.parseInt(cText); + if (cBound <= 0) { + showError("The bound should be greater than 1", "Option error"); + boundPane.setText(boundPane.getStableBound()); + } + boundPane.setStableBound(cText); + } catch (Exception e) { + // Empty string is allowed here to allow deleting. It will be handled by focusLost + if (cText.isEmpty()) { + return; + } + boundPane.setText(boundPane.getStableBound()); + showError("The bound should be greater than 1", "Option error"); + } + } - @Override - public void focusGained(FocusEvent arg0) { - // Nothing t be done here - } + @Override + public void focusGained(FocusEvent arg0) { + // Nothing t be done here + } - @Override - public void focusLost(FocusEvent arg0) { - if(boundPane.getText().isEmpty()) { - boundPane.setText(boundPane.getStableBound()); - showError("The bound should be greater than 1", "Option error"); - } - } + @Override + public void focusLost(FocusEvent arg0) { + if (boundPane.getText().isEmpty()) { + boundPane.setText(boundPane.getStableBound()); + showError("The bound should be greater than 1", "Option error"); + } + } } diff --git a/ui/src/main/java/com/dat3m/ui/listener/EditorListener.java b/ui/src/main/java/com/dat3m/ui/listener/EditorListener.java index 8a3ca9f158..799dc7f5a8 100644 --- a/ui/src/main/java/com/dat3m/ui/listener/EditorListener.java +++ b/ui/src/main/java/com/dat3m/ui/listener/EditorListener.java @@ -1,30 +1,29 @@ package com.dat3m.ui.listener; +import javax.swing.*; import java.awt.event.KeyEvent; import java.awt.event.KeyListener; -import javax.swing.JTextPane; - public class EditorListener implements KeyListener { - - private JTextPane consolePane; - public EditorListener(JTextPane pane) { - this.consolePane = pane; - } - - @Override - public void keyPressed(KeyEvent e) { - // Nothing to be done - } + private JTextPane consolePane; + + public EditorListener(JTextPane pane) { + this.consolePane = pane; + } + + @Override + public void keyPressed(KeyEvent e) { + // Nothing to be done + } - @Override - public void keyReleased(KeyEvent e) { - // Nothing to be done - } + @Override + public void keyReleased(KeyEvent e) { + // Nothing to be done + } - @Override - public void keyTyped(KeyEvent e) { - consolePane.setText(""); - } + @Override + public void keyTyped(KeyEvent e) { + consolePane.setText(""); + } } diff --git a/ui/src/main/java/com/dat3m/ui/listener/TimeoutListener.java b/ui/src/main/java/com/dat3m/ui/listener/TimeoutListener.java index a0b1779cfc..903f3e0343 100644 --- a/ui/src/main/java/com/dat3m/ui/listener/TimeoutListener.java +++ b/ui/src/main/java/com/dat3m/ui/listener/TimeoutListener.java @@ -1,66 +1,66 @@ package com.dat3m.ui.listener; -import static com.dat3m.ui.utils.Utils.showError; +import com.dat3m.ui.options.TimeoutField; import java.awt.event.FocusEvent; import java.awt.event.FocusListener; import java.awt.event.KeyEvent; import java.awt.event.KeyListener; -import com.dat3m.ui.options.TimeoutField; +import static com.dat3m.ui.utils.Utils.showError; public class TimeoutListener implements KeyListener, FocusListener { - - private TimeoutField timeoutPane; - public TimeoutListener(TimeoutField pane) { - this.timeoutPane = pane; - } - - @Override - public void keyPressed(KeyEvent e) { - runTest(); - } + private TimeoutField timeoutPane; + + public TimeoutListener(TimeoutField pane) { + this.timeoutPane = pane; + } + + @Override + public void keyPressed(KeyEvent e) { + runTest(); + } + + @Override + public void keyReleased(KeyEvent e) { + runTest(); + } - @Override - public void keyReleased(KeyEvent e) { - runTest(); - } + @Override + public void keyTyped(KeyEvent e) { + runTest(); + } - @Override - public void keyTyped(KeyEvent e) { - runTest(); - } - - private void runTest() { - String cText = timeoutPane.getText(); - try { - int cBound = Integer.parseInt(cText); - if(cBound <= 0) { - showError("The timeout should be greater than 1", "Option error"); - timeoutPane.setText(timeoutPane.getStableBound()); - } - timeoutPane.setStableBound(cText); - } catch (Exception e) { - // Empty string is allowed here to allow deleting. It will be handled by focusLost - if(cText.isEmpty()) { - return; - } - timeoutPane.setText(timeoutPane.getStableBound()); - showError("The timeout should be greater than 1", "Option error"); - } - } + private void runTest() { + String cText = timeoutPane.getText(); + try { + int cBound = Integer.parseInt(cText); + if (cBound <= 0) { + showError("The timeout should be greater than 1", "Option error"); + timeoutPane.setText(timeoutPane.getStableBound()); + } + timeoutPane.setStableBound(cText); + } catch (Exception e) { + // Empty string is allowed here to allow deleting. It will be handled by focusLost + if (cText.isEmpty()) { + return; + } + timeoutPane.setText(timeoutPane.getStableBound()); + showError("The timeout should be greater than 1", "Option error"); + } + } - @Override - public void focusGained(FocusEvent arg0) { - // Nothing t be done here - } + @Override + public void focusGained(FocusEvent arg0) { + // Nothing t be done here + } - @Override - public void focusLost(FocusEvent arg0) { - if(timeoutPane.getText().isEmpty()) { - timeoutPane.setText(timeoutPane.getStableBound()); - showError("The timeout should be greater than 1", "Option error"); - } - } + @Override + public void focusLost(FocusEvent arg0) { + if (timeoutPane.getText().isEmpty()) { + timeoutPane.setText(timeoutPane.getStableBound()); + showError("The timeout should be greater than 1", "Option error"); + } + } } diff --git a/ui/src/main/java/com/dat3m/ui/options/BoundField.java b/ui/src/main/java/com/dat3m/ui/options/BoundField.java index e27e315153..e69ef1de04 100644 --- a/ui/src/main/java/com/dat3m/ui/options/BoundField.java +++ b/ui/src/main/java/com/dat3m/ui/options/BoundField.java @@ -1,46 +1,45 @@ package com.dat3m.ui.options; -import static com.dat3m.ui.options.utils.ControlCode.BOUND; +import com.dat3m.ui.listener.BoundListener; +import javax.swing.*; import java.awt.event.ActionEvent; import java.awt.event.ActionListener; import java.util.HashSet; import java.util.Set; -import javax.swing.JTextField; - -import com.dat3m.ui.listener.BoundListener; +import static com.dat3m.ui.options.utils.ControlCode.BOUND; public class BoundField extends JTextField { - private String stableBound; - + private String stableBound; + private Set actionListeners = new HashSet<>(); - public BoundField() { - this.stableBound = "1"; - this.setColumns(3); - this.setText("1"); - - BoundListener listener = new BoundListener(this); - this.addKeyListener(listener); - this.addFocusListener(listener); - } - - public void addActionListener(ActionListener actionListener){ + public BoundField() { + this.stableBound = "1"; + this.setColumns(3); + this.setText("1"); + + BoundListener listener = new BoundListener(this); + this.addKeyListener(listener); + this.addFocusListener(listener); + } + + public void addActionListener(ActionListener actionListener) { actionListeners.add(actionListener); } - public void setStableBound(String bound) { - this.stableBound = bound; - // Listeners are notified when a new stable bound is set + public void setStableBound(String bound) { + this.stableBound = bound; + // Listeners are notified when a new stable bound is set ActionEvent boundChanged = new ActionEvent(this, ActionEvent.ACTION_PERFORMED, BOUND.actionCommand()); - for(ActionListener actionListener : actionListeners){ + for (ActionListener actionListener : actionListeners) { actionListener.actionPerformed(boundChanged); } - } + } - public String getStableBound() { - return stableBound; - } + public String getStableBound() { + return stableBound; + } } diff --git a/ui/src/main/java/com/dat3m/ui/options/BoundPane.java b/ui/src/main/java/com/dat3m/ui/options/BoundPane.java index 46af8396fc..a3e00e0a5e 100644 --- a/ui/src/main/java/com/dat3m/ui/options/BoundPane.java +++ b/ui/src/main/java/com/dat3m/ui/options/BoundPane.java @@ -1,16 +1,14 @@ package com.dat3m.ui.options; -import static java.awt.FlowLayout.LEFT; - -import java.awt.FlowLayout; +import javax.swing.*; +import java.awt.*; -import javax.swing.JLabel; -import javax.swing.JPanel; +import static java.awt.FlowLayout.LEFT; public class BoundPane extends JPanel { - public BoundPane() { + public BoundPane() { super(new FlowLayout(LEFT)); add(new JLabel("Unrolling: ")); - } + } } diff --git a/ui/src/main/java/com/dat3m/ui/options/TimeoutField.java b/ui/src/main/java/com/dat3m/ui/options/TimeoutField.java index 49379c916e..ed43adf4f2 100644 --- a/ui/src/main/java/com/dat3m/ui/options/TimeoutField.java +++ b/ui/src/main/java/com/dat3m/ui/options/TimeoutField.java @@ -1,46 +1,45 @@ package com.dat3m.ui.options; -import static com.dat3m.ui.options.utils.ControlCode.BOUND; +import com.dat3m.ui.listener.TimeoutListener; +import javax.swing.*; import java.awt.event.ActionEvent; import java.awt.event.ActionListener; import java.util.HashSet; import java.util.Set; -import javax.swing.JTextField; - -import com.dat3m.ui.listener.TimeoutListener; +import static com.dat3m.ui.options.utils.ControlCode.BOUND; public class TimeoutField extends JTextField { - private String stableTimeout; - + private String stableTimeout; + private Set actionListeners = new HashSet<>(); - public TimeoutField() { - this.stableTimeout = "60"; - this.setColumns(3); - this.setText("60"); - - TimeoutListener listener = new TimeoutListener(this); - this.addKeyListener(listener); - this.addFocusListener(listener); - } - - public void addActionListener(ActionListener actionListener){ + public TimeoutField() { + this.stableTimeout = "60"; + this.setColumns(3); + this.setText("60"); + + TimeoutListener listener = new TimeoutListener(this); + this.addKeyListener(listener); + this.addFocusListener(listener); + } + + public void addActionListener(ActionListener actionListener) { actionListeners.add(actionListener); } - public void setStableBound(String bound) { - this.stableTimeout = bound; - // Listeners are notified when a new stable bound is set + public void setStableBound(String bound) { + this.stableTimeout = bound; + // Listeners are notified when a new stable bound is set ActionEvent boundChanged = new ActionEvent(this, ActionEvent.ACTION_PERFORMED, BOUND.actionCommand()); - for(ActionListener actionListener : actionListeners){ + for (ActionListener actionListener : actionListeners) { actionListener.actionPerformed(boundChanged); } - } + } - public String getStableBound() { - return stableTimeout; - } + public String getStableBound() { + return stableTimeout; + } } diff --git a/ui/src/main/java/com/dat3m/ui/options/TimeoutPane.java b/ui/src/main/java/com/dat3m/ui/options/TimeoutPane.java index b1e9a92da3..c5a8f7df00 100644 --- a/ui/src/main/java/com/dat3m/ui/options/TimeoutPane.java +++ b/ui/src/main/java/com/dat3m/ui/options/TimeoutPane.java @@ -1,16 +1,14 @@ package com.dat3m.ui.options; -import static java.awt.FlowLayout.LEFT; - -import java.awt.FlowLayout; +import javax.swing.*; +import java.awt.*; -import javax.swing.JLabel; -import javax.swing.JPanel; +import static java.awt.FlowLayout.LEFT; public class TimeoutPane extends JPanel { - public TimeoutPane() { + public TimeoutPane() { super(new FlowLayout(LEFT)); add(new JLabel("Solver timeout: ")); - } + } } diff --git a/ui/src/main/java/com/dat3m/ui/options/utils/ControlCode.java b/ui/src/main/java/com/dat3m/ui/options/utils/ControlCode.java index 03e09dbdad..0535a2ba67 100644 --- a/ui/src/main/java/com/dat3m/ui/options/utils/ControlCode.java +++ b/ui/src/main/java/com/dat3m/ui/options/utils/ControlCode.java @@ -5,51 +5,31 @@ public enum ControlCode { TASK, TARGET, BOUND, TIMEOUT, TEST, CLEAR, METHOD, SOLVER, PROPERTY; @Override - public String toString(){ - switch(this){ - case TASK: - return "Task"; - case TARGET: - return "Target"; - case BOUND: - return "Bound"; - case TIMEOUT: - return "Timeout"; - case TEST: - return "Test"; - case CLEAR: - return "Clear"; - case METHOD: - return "Method"; - case SOLVER: - return "Solver"; - case PROPERTY: - return "Property"; - } - return super.toString(); + public String toString() { + return switch (this) { + case TASK -> "Task"; + case TARGET -> "Target"; + case BOUND -> "Bound"; + case TIMEOUT -> "Timeout"; + case TEST -> "Test"; + case CLEAR -> "Clear"; + case METHOD -> "Method"; + case SOLVER -> "Solver"; + case PROPERTY -> "Property"; + }; } - public String actionCommand(){ - switch(this){ - case TASK: - return "control_command_task"; - case TARGET: - return "control_command_target"; - case BOUND: - return "control_command_bound"; - case TIMEOUT: - return "control_command_timeout"; - case TEST: - return "control_command_test"; - case CLEAR: - return "control_command_clear"; - case METHOD: - return "control_command_method"; - case SOLVER: - return "control_command_solver"; - case PROPERTY: - return "control_command_property"; - } - throw new RuntimeException("Illegal EditorCode"); + public String actionCommand() { + return switch (this) { + case TASK -> "control_command_task"; + case TARGET -> "control_command_target"; + case BOUND -> "control_command_bound"; + case TIMEOUT -> "control_command_timeout"; + case TEST -> "control_command_test"; + case CLEAR -> "control_command_clear"; + case METHOD -> "control_command_method"; + case SOLVER -> "control_command_solver"; + case PROPERTY -> "control_command_property"; + }; } } diff --git a/ui/src/main/java/com/dat3m/ui/options/utils/Helper.java b/ui/src/main/java/com/dat3m/ui/options/utils/Helper.java index e22e91845e..5b657e36f2 100644 --- a/ui/src/main/java/com/dat3m/ui/options/utils/Helper.java +++ b/ui/src/main/java/com/dat3m/ui/options/utils/Helper.java @@ -1,16 +1,16 @@ package com.dat3m.ui.options.utils; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; + import java.util.Arrays; import java.util.Comparator; -import org.sosy_lab.java_smt.SolverContextFactory.Solvers; - public class Helper { - // Used to decide the solvers order shown by the selector in the UI - public static Solvers[] solversOrderedValues() { - return Arrays.stream(Solvers.values()) - .sorted(Comparator.comparing(Solvers::toString)) - .toArray(Solvers[]::new); - } + // Used to decide the solvers order shown by the selector in the UI + public static Solvers[] solversOrderedValues() { + return Arrays.stream(Solvers.values()) + .sorted(Comparator.comparing(Solvers::toString)) + .toArray(Solvers[]::new); + } } From 189807b4ca6e54c54910862ea4927849553fe3c2 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Tue, 28 May 2024 15:57:05 +0200 Subject: [PATCH 5/9] Removed accidentally added .bpl file support. Formatting --- .../main/java/com/dat3m/ui/editor/EditorsPane.java | 2 +- ui/src/main/java/com/dat3m/ui/icon/IconHelper.java | 12 ++++++------ 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/ui/src/main/java/com/dat3m/ui/editor/EditorsPane.java b/ui/src/main/java/com/dat3m/ui/editor/EditorsPane.java index 24bf815f37..1601801b04 100644 --- a/ui/src/main/java/com/dat3m/ui/editor/EditorsPane.java +++ b/ui/src/main/java/com/dat3m/ui/editor/EditorsPane.java @@ -10,7 +10,7 @@ public class EditorsPane { private final ImmutableMap editors = ImmutableMap.of( - EditorCode.PROGRAM, new Editor(EditorCode.PROGRAM, new RSyntaxTextArea(), "litmus", "c", "bpl", "ll"), + EditorCode.PROGRAM, new Editor(EditorCode.PROGRAM, new RSyntaxTextArea(), "litmus", "c", "ll"), EditorCode.TARGET_MM, new Editor(EditorCode.TARGET_MM, new RSyntaxTextArea(), "cat") ); diff --git a/ui/src/main/java/com/dat3m/ui/icon/IconHelper.java b/ui/src/main/java/com/dat3m/ui/icon/IconHelper.java index 8ace82c641..1a1e61f2c5 100644 --- a/ui/src/main/java/com/dat3m/ui/icon/IconHelper.java +++ b/ui/src/main/java/com/dat3m/ui/icon/IconHelper.java @@ -9,27 +9,27 @@ public class IconHelper { private static Map> data = new HashMap<>(); - public static ImageIcon getIcon(IconCode code){ + public static ImageIcon getIcon(IconCode code) { return getIcon(code, -1); } - public static ImageIcon getIcon(IconCode code, int height){ + public static ImageIcon getIcon(IconCode code, int height) { data.putIfAbsent(code, new HashMap<>()); Map heightMap = data.get(code); height = Math.max(-1, height); - if(!heightMap.containsKey(height)){ + if (!heightMap.containsKey(height)) { heightMap.put(height, mkIcon(code, height)); } return heightMap.get(height); } - private static ImageIcon mkIcon(IconCode code, int height){ + private static ImageIcon mkIcon(IconCode code, int height) { ImageIcon origImage = new ImageIcon(code.getPath(), code.toString()); - if(height == -1){ + if (height == -1) { return origImage; } - if(height > origImage.getIconHeight()){ + if (height > origImage.getIconHeight()) { System.err.println("Warning: scaling image large its original size might degrade image quality"); } From a3d1e97e0ba923dca49b72b23726b1121035f4e3 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Tue, 28 May 2024 19:23:18 +0200 Subject: [PATCH 6/9] Minor fix in witness generation --- dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 4533d49ae2..2a8e32fbd0 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -187,7 +187,7 @@ public static void main(String[] args) throws Exception { // Verification ended, we can interrupt the timeout Thread t.interrupt(); - if (modelChecker.hasModel()) { + if (modelChecker.hasModel() && o.getWitnessType().generateGraphviz()) { generateExecutionGraphFile(task, prover, modelChecker, o.getWitnessType()); } From 9d98e06982917612b539362324e9c76169aca918 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Wed, 29 May 2024 17:40:47 +0200 Subject: [PATCH 7/9] Added simple zoom option to displayed witnesses --- ui/src/main/java/com/dat3m/ui/Dat3M.java | 18 +++++++- .../java/com/dat3m/ui/utils/ImageLabel.java | 42 +++++++++++++++++++ 2 files changed, 59 insertions(+), 1 deletion(-) create mode 100644 ui/src/main/java/com/dat3m/ui/utils/ImageLabel.java diff --git a/ui/src/main/java/com/dat3m/ui/Dat3M.java b/ui/src/main/java/com/dat3m/ui/Dat3M.java index 6f7273c0d9..18fc5bccc8 100644 --- a/ui/src/main/java/com/dat3m/ui/Dat3M.java +++ b/ui/src/main/java/com/dat3m/ui/Dat3M.java @@ -11,6 +11,7 @@ import com.dat3m.ui.options.OptionsPane; import com.dat3m.ui.options.utils.ControlCode; import com.dat3m.ui.result.ReachabilityResult; +import com.dat3m.ui.utils.ImageLabel; import com.dat3m.ui.utils.UiOptions; import org.antlr.v4.runtime.InputMismatchException; import org.antlr.v4.runtime.Token; @@ -19,6 +20,8 @@ import java.awt.*; import java.awt.event.ActionEvent; import java.awt.event.ActionListener; +import java.awt.event.KeyAdapter; +import java.awt.event.KeyEvent; import static com.dat3m.ui.utils.Utils.showError; import static javax.swing.BorderFactory.createEmptyBorder; @@ -93,7 +96,9 @@ private void showViolation(ReachabilityResult testResult) { // Generate scroll pane with image of violation final ImageIcon imageIcon = new ImageIcon(filePath); imageIcon.getImage().flush(); // Flush the caches for otherwise we might show a previously loaded file!!! - final JScrollPane scrollPane = new JScrollPane(new JLabel(imageIcon)); + + final ImageLabel imgLabel = new ImageLabel(imageIcon); + final JScrollPane scrollPane = new JScrollPane(imgLabel); scrollPane.setHorizontalScrollBarPolicy(JScrollPane.HORIZONTAL_SCROLLBAR_AS_NEEDED); scrollPane.setVerticalScrollBarPolicy(JScrollPane.VERTICAL_SCROLLBAR_AS_NEEDED); @@ -105,6 +110,17 @@ private void showViolation(ReachabilityResult testResult) { final int y = (screenSize.height - imageFrame.getSize().height) / 2; final int extraFrameSize = 100; + imageFrame.addKeyListener(new KeyAdapter() { + @Override + public void keyPressed(KeyEvent e) { + if (e.getKeyChar() == '+') { + imgLabel.zoom(1.05); + } else if (e.getKeyChar() == '-') { + imgLabel.zoom(0.95); + } + } + }); + imageFrame.setSize(imageIcon.getIconWidth() + extraFrameSize, imageIcon.getIconHeight() + extraFrameSize); imageFrame.getContentPane().add(scrollPane); imageFrame.setLocation(x, y); diff --git a/ui/src/main/java/com/dat3m/ui/utils/ImageLabel.java b/ui/src/main/java/com/dat3m/ui/utils/ImageLabel.java new file mode 100644 index 0000000000..6e089ff413 --- /dev/null +++ b/ui/src/main/java/com/dat3m/ui/utils/ImageLabel.java @@ -0,0 +1,42 @@ +package com.dat3m.ui.utils; + +import javax.swing.*; +import java.awt.*; +import java.awt.image.BufferedImage; + +public class ImageLabel extends JLabel { + final ImageIcon imageIcon; + final Image originalImage; + final int originalWidth, originalHeight; + double zoomLevel = 1.0; + + public ImageLabel(ImageIcon imageIcon) { + super(imageIcon); + this.imageIcon = imageIcon; + originalImage = imageIcon.getImage(); + originalWidth = originalImage.getWidth(null); + originalHeight = originalImage.getHeight(null); + } + + public void zoom(double zoom) { + this.zoomLevel *= zoom; + setDimensions((int)(originalWidth * zoomLevel), (int)(originalHeight * zoomLevel)); + } + + public void setDimensions(int width, int height) { + BufferedImage resizedImage = new BufferedImage(width, height, BufferedImage.TYPE_INT_RGB); + Graphics2D g = resizedImage.createGraphics(); + g.setRenderingHint(RenderingHints.KEY_INTERPOLATION, RenderingHints.VALUE_INTERPOLATION_BICUBIC); + g.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON); + g.drawImage(originalImage, 0, 0, width, height, null); + g.dispose(); + + imageIcon.setImage(resizedImage); + + Container parent = this.getParent(); + if (parent != null) { + parent.repaint(); + } + this.repaint(); + } +} \ No newline at end of file From 49a9eda5f9c8ad30c28cbd95d41c945b8cfe0786 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Thu, 30 May 2024 10:58:02 +0200 Subject: [PATCH 8/9] Minor fixes in comments. Refactor. UI programs now get a unified name. Fixed witness generation for programs without names or without file suffix. --- .../java/com/dat3m/dartagnan/Dartagnan.java | 19 ++++++++----------- ui/src/main/java/com/dat3m/ui/Dat3M.java | 6 ++++-- .../com/dat3m/ui/listener/BoundListener.java | 2 +- .../dat3m/ui/listener/TimeoutListener.java | 2 +- .../com/dat3m/ui/options/OptionsPane.java | 2 +- .../dat3m/ui/result/ReachabilityResult.java | 12 ++++++------ .../java/com/dat3m/ui/utils/UiOptions.java | 2 +- 7 files changed, 22 insertions(+), 23 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 2a8e32fbd0..7b2ec7ce26 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -172,16 +172,10 @@ public static void main(String[] args) throws Exception { modelChecker = DataRaceSolver.run(ctx, prover, task); } else { // Property is either PROGRAM_SPEC, LIVENESS, or CAT_SPEC - switch (o.getMethod()) { - case EAGER: - modelChecker = AssumeSolver.run(ctx, prover, task); - break; - case LAZY: - modelChecker = RefinementSolver.run(ctx, prover, task); - break; - default: - throw new InvalidConfigurationException("unsupported method " + o.getMethod()); - } + modelChecker = switch (o.getMethod()) { + case EAGER -> AssumeSolver.run(ctx, prover, task); + case LAZY -> RefinementSolver.run(ctx, prover, task); + }; } // Verification ended, we can interrupt the timeout Thread @@ -220,7 +214,10 @@ public static File generateExecutionGraphFile(VerificationTask task, ProverEnvir final ExecutionModel m = ExecutionModel.withContext(modelChecker.getEncodingContext()); m.initialize(prover.getModel()); final SyntacticContextAnalysis synContext = newInstance(task.getProgram()); - final String name = task.getProgram().getName().substring(0, task.getProgram().getName().lastIndexOf('.')); + final String progName = task.getProgram().getName(); + final int fileSuffixIndex = progName.lastIndexOf('.'); + final String name = progName.isEmpty() ? "unnamed_program" : + (fileSuffixIndex == - 1) ? progName : progName.substring(0, fileSuffixIndex); // RF edges give both ordering and data flow information, thus even when the pair is in PO // we get some data flow information by observing the edge // FR edges only give ordering information which is known if the pair is also in PO diff --git a/ui/src/main/java/com/dat3m/ui/Dat3M.java b/ui/src/main/java/com/dat3m/ui/Dat3M.java index 18fc5bccc8..fbeb33d53a 100644 --- a/ui/src/main/java/com/dat3m/ui/Dat3M.java +++ b/ui/src/main/java/com/dat3m/ui/Dat3M.java @@ -83,7 +83,7 @@ public void actionPerformed(ActionEvent event) { runTest(); if (testResult != null) { optionsPane.getConsolePane().setText(testResult.getVerdict()); - if (optionsPane.getOptions().showViolationGraph() && testResult.hasViolationModel()) { + if (optionsPane.getOptions().showWitness() && testResult.hasWitness()) { showViolation(testResult); } } @@ -91,7 +91,7 @@ public void actionPerformed(ActionEvent event) { } private void showViolation(ReachabilityResult testResult) { - final String filePath = testResult.getViolationModelFile().getAbsolutePath(); + final String filePath = testResult.getWitnessFile().getAbsolutePath(); // Generate scroll pane with image of violation final ImageIcon imageIcon = new ImageIcon(filePath); @@ -110,6 +110,7 @@ private void showViolation(ReachabilityResult testResult) { final int y = (screenSize.height - imageFrame.getSize().height) / 2; final int extraFrameSize = 100; + // Add zoomability to the witness imageFrame.addKeyListener(new KeyAdapter() { @Override public void keyPressed(KeyEvent e) { @@ -142,6 +143,7 @@ private void runTest() { programEditor.getLoadedPath(), format, options.cflags()); + program.setName("dat3mUI"); try { final Wmm targetModel = new ParserCat().parse(editorsPane.getEditor(EditorCode.TARGET_MM).getEditorPane().getText()); testResult = new ReachabilityResult(program, targetModel, options); diff --git a/ui/src/main/java/com/dat3m/ui/listener/BoundListener.java b/ui/src/main/java/com/dat3m/ui/listener/BoundListener.java index 295f3b5ec3..44209e2cac 100644 --- a/ui/src/main/java/com/dat3m/ui/listener/BoundListener.java +++ b/ui/src/main/java/com/dat3m/ui/listener/BoundListener.java @@ -53,7 +53,7 @@ private void runTest() { @Override public void focusGained(FocusEvent arg0) { - // Nothing t be done here + // Nothing to be done here } @Override diff --git a/ui/src/main/java/com/dat3m/ui/listener/TimeoutListener.java b/ui/src/main/java/com/dat3m/ui/listener/TimeoutListener.java index 903f3e0343..59ed45b3d5 100644 --- a/ui/src/main/java/com/dat3m/ui/listener/TimeoutListener.java +++ b/ui/src/main/java/com/dat3m/ui/listener/TimeoutListener.java @@ -53,7 +53,7 @@ private void runTest() { @Override public void focusGained(FocusEvent arg0) { - // Nothing t be done here + // Nothing to be done here } @Override diff --git a/ui/src/main/java/com/dat3m/ui/options/OptionsPane.java b/ui/src/main/java/com/dat3m/ui/options/OptionsPane.java index 1404160a42..47a54469af 100644 --- a/ui/src/main/java/com/dat3m/ui/options/OptionsPane.java +++ b/ui/src/main/java/com/dat3m/ui/options/OptionsPane.java @@ -142,7 +142,7 @@ private void mkGrid() { configPane.add(configField); JPanel showViolationPane = new JPanel(new FlowLayout(LEFT)); - showViolationPane.add(new JLabel("Show violation graph")); + showViolationPane.add(new JLabel("Show witness graph")); showViolationPane.add(showViolationField); // Inner borders diff --git a/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java b/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java index 561e722583..3eb4f37058 100644 --- a/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java +++ b/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java @@ -30,7 +30,7 @@ public class ReachabilityResult { private final UiOptions options; private String verdict; - private File violationModel; + private File witnessFile; public ReachabilityResult(Program program, Wmm wmm, UiOptions options) { @@ -44,12 +44,12 @@ public String getVerdict() { return verdict; } - public boolean hasViolationModel() { - return violationModel != null; + public boolean hasWitness() { + return witnessFile != null; } - public File getViolationModelFile() { - return violationModel; + public File getWitnessFile() { + return witnessFile; } private void run() { @@ -102,7 +102,7 @@ private void run() { verdict = Dartagnan.generateResultSummary(task, prover, modelChecker); if (modelChecker.hasModel()) { - violationModel = Dartagnan.generateExecutionGraphFile(task, prover, modelChecker, WitnessType.PNG); + witnessFile = Dartagnan.generateExecutionGraphFile(task, prover, modelChecker, WitnessType.PNG); } } } catch (InterruptedException e) { diff --git a/ui/src/main/java/com/dat3m/ui/utils/UiOptions.java b/ui/src/main/java/com/dat3m/ui/utils/UiOptions.java index 9bcf5665cd..993205b492 100644 --- a/ui/src/main/java/com/dat3m/ui/utils/UiOptions.java +++ b/ui/src/main/java/com/dat3m/ui/utils/UiOptions.java @@ -7,7 +7,7 @@ import java.util.EnumSet; -public record UiOptions(Arch target, Method method, int bound, Solvers solver, int timeout, boolean showViolationGraph, +public record UiOptions(Arch target, Method method, int bound, Solvers solver, int timeout, boolean showWitness, String cflags, String config, EnumSet properties) { From c4911dcf481c2e53dc6c4685496e71c89ede44ef Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Fri, 31 May 2024 11:09:39 +0200 Subject: [PATCH 9/9] No UI witnesses for UNKNOWN results Minor renaming --- dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java | 2 +- ui/src/main/java/com/dat3m/ui/options/OptionsPane.java | 6 +++--- .../main/java/com/dat3m/ui/result/ReachabilityResult.java | 3 ++- 3 files changed, 6 insertions(+), 5 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 7b2ec7ce26..91cf646429 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -209,7 +209,7 @@ public static void main(String[] args) throws Exception { public static File generateExecutionGraphFile(VerificationTask task, ProverEnvironment prover, ModelChecker modelChecker, WitnessType witnessType) throws InvalidConfigurationException, SolverException, IOException { - Preconditions.checkArgument(modelChecker.hasModel(), "No model to generate."); + Preconditions.checkArgument(modelChecker.hasModel(), "No execution graph to generate."); final ExecutionModel m = ExecutionModel.withContext(modelChecker.getEncodingContext()); m.initialize(prover.getModel()); diff --git a/ui/src/main/java/com/dat3m/ui/options/OptionsPane.java b/ui/src/main/java/com/dat3m/ui/options/OptionsPane.java index 47a54469af..6e4ff895a6 100644 --- a/ui/src/main/java/com/dat3m/ui/options/OptionsPane.java +++ b/ui/src/main/java/com/dat3m/ui/options/OptionsPane.java @@ -138,7 +138,7 @@ private void mkGrid() { cflagsPane.add(cflagsField); JPanel configPane = new JPanel(new FlowLayout(LEFT)); - configPane.add(new JLabel("Config: ")); + configPane.add(new JLabel("Extra options: ")); configPane.add(configField); JPanel showViolationPane = new JPanel(new FlowLayout(LEFT)); @@ -150,8 +150,8 @@ private void mkGrid() { JSplitPane graphPane = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT); graphPane.setDividerSize(0); - JComponent[] panes = { targetPane, methodPane, solverPane, propertyPane, boundsPane, showViolationPane, cflagsPane, - configPane, testButton, clearButton, graphPane, scrollConsole }; + JComponent[] panes = { targetPane, methodPane, solverPane, propertyPane, boundsPane, showViolationPane, configPane, + cflagsPane, testButton, clearButton, graphPane, scrollConsole }; Iterator it = Arrays.asList(panes).iterator(); JComponent current = iconPane; current.setBorder(emptyBorder); diff --git a/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java b/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java index 3eb4f37058..6f2f6e622b 100644 --- a/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java +++ b/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java @@ -3,6 +3,7 @@ import com.dat3m.dartagnan.Dartagnan; import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.program.Program; +import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.verification.VerificationTask; import com.dat3m.dartagnan.verification.solving.AssumeSolver; import com.dat3m.dartagnan.verification.solving.ModelChecker; @@ -101,7 +102,7 @@ private void run() { t.interrupt(); verdict = Dartagnan.generateResultSummary(task, prover, modelChecker); - if (modelChecker.hasModel()) { + if (modelChecker.hasModel() && modelChecker.getResult() != Result.UNKNOWN) { witnessFile = Dartagnan.generateExecutionGraphFile(task, prover, modelChecker, WitnessType.PNG); } }