Skip to content

Commit

Permalink
UI update (#684)
Browse files Browse the repository at this point in the history 
* Updated witness generation functions to return the generated File.

* 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' + '+/-'
- Added simple zoom option to displayed witnesses

* Added ability to pass configuration options via the UI.

* UI programs now get a unified name.
Fixed witness generation for programs without names or without file suffix.
  • Loading branch information
@ThomasHaas @hernan-poncedeleon
ThomasHaas authored and hernan-poncedeleon committed Aug 26, 2024
1 parent c8bc162 commit 6069f1f
Show file tree
Hide file tree
Showing 26 changed files with 709 additions and 706 deletions.
58 changes: 35 additions & 23 deletions dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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.*;

Expand All @@ -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;
Expand Down Expand Up @@ -165,33 +172,17 @@ 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
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();
Expand All @@ -215,6 +206,27 @@ 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 execution graph to generate.");

final ExecutionModel m = ExecutionModel.withContext(modelChecker.getEncodingContext());
m.initialize(prover.getModel());
final SyntacticContextAnalysis synContext = newInstance(task.getProgram());
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
// 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 ------------------
Expand Down
8 changes: 5 additions & 3 deletions dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down Expand Up @@ -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,
Expand All @@ -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,
Expand Down
10 changes: 6 additions & 4 deletions dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/Graphviz.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
}
Loading

0 comments on commit 6069f1f

Please sign in to comment.