UI update

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;
@@ -181,17 +188,7 @@ public static void main(String[] args) throws Exception {
                 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());
+                    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 ------------------

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<EventData, EventData> rfFilter, BiPredicate<EventData, EventData> frFilter,
                                             BiPredicate<EventData, EventData> 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,

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);
     }
 }

ui/src/main/java/com/dat3m/ui/Dat3M.java

@@ -4,111 +4,159 @@
 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.ImageLabel;
+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;
+import java.awt.event.KeyAdapter;
+import java.awt.event.KeyEvent;
 
 import static com.dat3m.ui.utils.Utils.showError;
 import static javax.swing.BorderFactory.createEmptyBorder;
 import static javax.swing.UIManager.getDefaults;
 
 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 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);
+
+        // 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.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);
+        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");
-		}
-	}
+    }
 }