Skip to content

Commit

Permalink
Add option to dump encoding to smtlib2 file (#721)
Browse files Browse the repository at this point in the history
hernanponcedeleon authored and hernan-poncedeleon committed Sep 16, 2024
1 parent 8e80d6a commit 2a0ed59
Showing 24 changed files with 339 additions and 119 deletions.
6 changes: 5 additions & 1 deletion dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java
Original file line number Diff line number Diff line change
@@ -3,6 +3,7 @@
import com.dat3m.dartagnan.configuration.OptionNames;
import com.dat3m.dartagnan.configuration.Property;
import com.dat3m.dartagnan.encoding.EncodingContext;
import com.dat3m.dartagnan.encoding.ProverWithTracker;
import com.dat3m.dartagnan.expression.ExpressionPrinter;
import com.dat3m.dartagnan.parsers.cat.ParserCat;
import com.dat3m.dartagnan.parsers.program.ProgramParser;
@@ -163,7 +164,10 @@ public static void main(String[] args) throws Exception {
BasicLogManager.create(solverConfig),
sdm.getNotifier(),
o.getSolver());
ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
ProverWithTracker prover = new ProverWithTracker(ctx,
o.getDumpSmtLib() ?
System.getenv("DAT3M_OUTPUT") + String.format("/%s.smt2", p.getName()) : "",
ProverOptions.GENERATE_MODELS)) {
ModelChecker modelChecker;
if (properties.contains(DATARACEFREEDOM)) {
if (properties.size() > 1) {
Original file line number Diff line number Diff line change
@@ -12,6 +12,7 @@ public class OptionNames {
public static final String VALIDATE = "validate";
public static final String COVERAGE = "coverage";
public static final String WITNESS = "witness";
public static final String SMTLIB2 = "smtlib2";

// Modeling Options
public static final String THREAD_CREATE_ALWAYS_SUCCEEDS = "modeling.threadCreateAlwaysSucceeds";
Original file line number Diff line number Diff line change
@@ -0,0 +1,200 @@
package com.dat3m.dartagnan.encoding;

import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.io.PrintWriter;
import java.nio.file.Files;
import java.nio.file.Paths;
import java.time.LocalDate;
import java.time.format.DateTimeFormatter;
import java.util.Collection;
import java.util.HashSet;
import java.util.List;
import java.util.Optional;
import java.util.Set;

import org.sosy_lab.java_smt.api.*;
import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;

import com.google.common.collect.ImmutableMap;

public class ProverWithTracker implements ProverEnvironment {

private final FormulaManager fmgr;
private final ProverEnvironment prover;
private final String fileName;
private final Set<String> declarations;

public ProverWithTracker(SolverContext ctx, String fileName, ProverOptions... options) {
this.fmgr = ctx.getFormulaManager();
this.prover = ctx.newProverEnvironment(options);
this.fileName = fileName;
this.declarations = new HashSet<>();
init();
}

// An empty filename means there is no need to dump the encoding
private boolean dump() {
return !fileName.isEmpty();
}

private void init() {
if(dump()) {
try {
Files.deleteIfExists(Paths.get(fileName));
} catch (IOException e) {
e.printStackTrace();
}
StringBuilder description = new StringBuilder();
LocalDate currentDate = LocalDate.now();
DateTimeFormatter formatter = DateTimeFormatter.ofPattern("YYYY-MM-DD");
description.append("Generated on: " + currentDate.format(formatter) + "\n");
description.append("Generator: Dartagnan\n");
description.append("Application: Bounded model checking for weak memory models\n");
description.append("Publications: \n" +
"- Hernán Ponce de León, Florian Furbach, Keijo Heljanko, " +
"Roland Meyer: Dartagnan: Bounded Model Checking for Weak Memory Models " +
"(Competition Contribution). TACAS (2) 2020: 378-382\n" +
"- Thomas Haas, Roland Meyer, Hernán Ponce de León: " +
"CAAT: consistency as a theory. Proc. ACM Program. Lang. 6(OOPSLA2): 114-144 (2022)"
);
write("(set-info :smt-lib-version 2.6)\n");
write("(set-logic ALL)\n");
write("(set-info :category \"industrial\")\n");
write("(set-info :source |\n" + description + "\n|)\n");
write("(set-info :license \"https://creativecommons.org/licenses/by/4.0/\")\n");
}
}

@Override
public void close() {
if(dump()) {
removeDuplicatedDeclarations(fileName);
write("(exit)\n");
}
prover.close();
}

@Override
public Void addConstraint(BooleanFormula f) throws InterruptedException {
if(dump()) {
write(fmgr.dumpFormula(f).toString());
}
return prover.addConstraint(f);
}

@Override
public boolean isUnsatWithAssumptions(Collection<BooleanFormula> fs) throws SolverException, InterruptedException {

if(dump()) {
write("(push)\n");
for(BooleanFormula f : fs) {
write(fmgr.dumpFormula(f).toString());
}
}

long start = System.currentTimeMillis();
boolean result = prover.isUnsatWithAssumptions(fs);
long end = System.currentTimeMillis();

if(dump()) {
write("(set-info :status " + (result ? "unsat" : "sat") + ")\n");
write("(check-sat)\n");
writeComment("Original solving time: " + (end - start) + " ms");
write("(pop)\n");
}

return result;
}

@Override
public boolean isUnsat() throws SolverException, InterruptedException {
long start = System.currentTimeMillis();
boolean result = prover.isUnsat();
long end = System.currentTimeMillis();
if(dump()) {
write("(set-info :status " + (result ? "unsat" : "sat") + ")\n");
write("(check-sat)\n");
writeComment("Original solving time: " + (end - start) + " ms");
}
return result;
}

@Override
public ImmutableMap<String, String> getStatistics() {
return prover.getStatistics();
}

@Override
public Model getModel() throws SolverException {
return prover.getModel();
}

@Override
public void push() throws InterruptedException {
if(dump()) {
write("(push)\n");
}
prover.push();
}

@Override
public void pop() {
if(dump()) {
write("(pop)\n");
}
prover.pop();
}

@Override
public <R> R allSat(AllSatCallback<R> arg0, List<BooleanFormula> arg1) throws InterruptedException, SolverException {
return prover.allSat(arg0, arg1);
}

@Override
public List<BooleanFormula> getUnsatCore() {
return prover.getUnsatCore();
}

@Override
public int size() {
return prover.size();
}

@Override
public Optional<List<BooleanFormula>> unsatCoreOverAssumptions(Collection<BooleanFormula> arg0)
throws SolverException, InterruptedException {
return prover.unsatCoreOverAssumptions(arg0);
}

private void write(String content) {
if (dump()) {
File file = new File(fileName);
try (FileWriter writer = new FileWriter(file, true);
PrintWriter printer = new PrintWriter(writer)) {
printer.append(removeDuplicatedDeclarations(content));
printer.close();
} catch (IOException e) {
e.printStackTrace();
}
}
}

public void writeComment(String content) {
write("; " + content);
}

// FIXME: This is only correct as long as no declarations are popped and then
// later redeclared (which is currently guarenteed by the way we use the solver)
private StringBuilder removeDuplicatedDeclarations(String content) {
StringBuilder builder = new StringBuilder();
for(String line : content.split("\n")) {
if(line.contains("declare-fun") && !declarations.add(line)) {
continue;
}
builder.append(line + "\n");
}
return builder;
}
}
Original file line number Diff line number Diff line change
@@ -2,10 +2,8 @@

import com.dat3m.dartagnan.expression.Expression;
import com.dat3m.dartagnan.expression.ExpressionFactory;
import com.dat3m.dartagnan.expression.Type;
import com.dat3m.dartagnan.expression.type.IntegerType;
import com.dat3m.dartagnan.program.Register;
import com.dat3m.dartagnan.program.Program.SourceLanguage;
import com.dat3m.dartagnan.program.event.Event;
import com.dat3m.dartagnan.program.event.EventFactory;
import com.dat3m.dartagnan.program.event.Tag;
Original file line number Diff line number Diff line change
@@ -68,4 +68,11 @@ public abstract class BaseOptions {
private WitnessType witnessType=WitnessType.getDefault();

public WitnessType getWitnessType() { return witnessType; }

@Option(
name=SMTLIB2,
description="Dump encoding to an SMTLIB2 file.")
private boolean smtlib=false;

public boolean getDumpSmtLib() { return smtlib; }
}
Original file line number Diff line number Diff line change
@@ -21,16 +21,16 @@ public class AssumeSolver extends ModelChecker {
private static final Logger logger = LogManager.getLogger(AssumeSolver.class);

private final SolverContext ctx;
private final ProverEnvironment prover;
private final ProverWithTracker prover;
private final VerificationTask task;

private AssumeSolver(SolverContext c, ProverEnvironment p, VerificationTask t) {
private AssumeSolver(SolverContext c, ProverWithTracker p, VerificationTask t) {
ctx = c;
prover = p;
task = t;
}

public static AssumeSolver run(SolverContext ctx, ProverEnvironment prover, VerificationTask task)
public static AssumeSolver run(SolverContext ctx, ProverWithTracker prover, VerificationTask task)
throws InterruptedException, SolverException, InvalidConfigurationException {
AssumeSolver s = new AssumeSolver(ctx, prover, task);
s.run();
@@ -55,21 +55,27 @@ private void run() throws InterruptedException, SolverException, InvalidConfigur
SymmetryEncoder symmetryEncoder = SymmetryEncoder.withContext(context);

logger.info("Starting encoding using " + ctx.getVersion());
prover.writeComment("Program encoding");
prover.addConstraint(programEncoder.encodeFullProgram());
prover.writeComment("Memory model encoding");
prover.addConstraint(wmmEncoder.encodeFullMemoryModel());
// For validation this contains information.
// For verification graph.encode() just returns ctx.mkTrue()
prover.writeComment("Witness encoding");
prover.addConstraint(task.getWitness().encode(context));
prover.writeComment("Symmetry breaking encoding");
prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking());

BooleanFormulaManager bmgr = ctx.getFormulaManager().getBooleanFormulaManager();
BooleanFormula assumptionLiteral = bmgr.makeVariable("DAT3M_spec_assumption");
BooleanFormula propertyEncoding = propertyEncoder.encodeProperties(task.getProperty());
BooleanFormula assumedSpec = bmgr.implication(assumptionLiteral, propertyEncoding);
prover.writeComment("Property encoding");
prover.addConstraint(assumedSpec);

logger.info("Starting first solver.check()");
if(prover.isUnsatWithAssumptions(singletonList(assumptionLiteral))) {
prover.writeComment("Bound encoding");
prover.addConstraint(propertyEncoder.encodeBoundEventExec());
logger.info("Starting second solver.check()");
res = prover.isUnsat()? PASS : Result.UNKNOWN;
Original file line number Diff line number Diff line change
@@ -9,7 +9,7 @@
import org.apache.logging.log4j.Logger;
import org.sosy_lab.common.configuration.Configuration;
import org.sosy_lab.common.configuration.InvalidConfigurationException;
import org.sosy_lab.java_smt.api.ProverEnvironment;
import com.dat3m.dartagnan.encoding.ProverWithTracker;
import org.sosy_lab.java_smt.api.SolverContext;
import org.sosy_lab.java_smt.api.SolverException;

@@ -18,63 +18,67 @@
import static com.dat3m.dartagnan.utils.Result.*;

public class DataRaceSolver extends ModelChecker {
// This analysis assumes that CAT file defining the memory model has a happens-before
// relation named hb: it should contain the following axiom "acyclic hb"

// This analysis assumes that CAT file defining the memory model has a happens-before
// relation named hb: it should contain the following axiom "acyclic hb"

private static final Logger logger = LogManager.getLogger(DataRaceSolver.class);

private final SolverContext ctx;
private final ProverEnvironment prover;
private final VerificationTask task;
private final SolverContext ctx;
private final ProverWithTracker prover;
private final VerificationTask task;

private DataRaceSolver(SolverContext c, ProverEnvironment p, VerificationTask t) {
ctx = c;
prover = p;
task = t;
}
private DataRaceSolver(SolverContext c, ProverWithTracker p, VerificationTask t) {
ctx = c;
prover = p;
task = t;
}

public static DataRaceSolver run(SolverContext ctx, ProverEnvironment prover, VerificationTask task)
throws InterruptedException, SolverException, InvalidConfigurationException {
DataRaceSolver s = new DataRaceSolver(ctx, prover, task);
s.run();
return s;
}
public static DataRaceSolver run(SolverContext ctx, ProverWithTracker prover, VerificationTask task)
throws InterruptedException, SolverException, InvalidConfigurationException {
DataRaceSolver s = new DataRaceSolver(ctx, prover, task);
s.run();
return s;
}

private void run() throws InterruptedException, SolverException, InvalidConfigurationException {
Wmm memoryModel = task.getMemoryModel();
Context analysisContext = Context.create();
Configuration config = task.getConfig();
private void run() throws InterruptedException, SolverException, InvalidConfigurationException {
Wmm memoryModel = task.getMemoryModel();
Context analysisContext = Context.create();
Configuration config = task.getConfig();

memoryModel.configureAll(config);
preprocessProgram(task, config);
preprocessMemoryModel(task, config);
performStaticProgramAnalyses(task, analysisContext, config);
performStaticWmmAnalyses(task, analysisContext, config);
memoryModel.configureAll(config);
preprocessProgram(task, config);
preprocessMemoryModel(task, config);
performStaticProgramAnalyses(task, analysisContext, config);
performStaticWmmAnalyses(task, analysisContext, config);

context = EncodingContext.of(task, analysisContext, ctx.getFormulaManager());
ProgramEncoder programEncoder = ProgramEncoder.withContext(context);
PropertyEncoder propertyEncoder = PropertyEncoder.withContext(context);
WmmEncoder wmmEncoder = WmmEncoder.withContext(context);
SymmetryEncoder symmetryEncoder = SymmetryEncoder.withContext(context);
context = EncodingContext.of(task, analysisContext, ctx.getFormulaManager());
ProgramEncoder programEncoder = ProgramEncoder.withContext(context);
PropertyEncoder propertyEncoder = PropertyEncoder.withContext(context);
WmmEncoder wmmEncoder = WmmEncoder.withContext(context);
SymmetryEncoder symmetryEncoder = SymmetryEncoder.withContext(context);

logger.info("Starting encoding using " + ctx.getVersion());
prover.addConstraint(programEncoder.encodeFullProgram());
prover.addConstraint(wmmEncoder.encodeFullMemoryModel());
prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking());
prover.push();

prover.addConstraint(propertyEncoder.encodeProperties(EnumSet.of(Property.DATARACEFREEDOM)));
prover.writeComment("Program encoding");
prover.addConstraint(programEncoder.encodeFullProgram());
prover.writeComment("Memory model encoding");
prover.addConstraint(wmmEncoder.encodeFullMemoryModel());
prover.writeComment("Symmetry breaking encoding");
prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking());
prover.push();
prover.writeComment("Property encoding");
prover.addConstraint(propertyEncoder.encodeProperties(EnumSet.of(Property.DATARACEFREEDOM)));

logger.info("Starting first solver.check()");
if(prover.isUnsat()) {
prover.pop();
prover.addConstraint(propertyEncoder.encodeBoundEventExec());
logger.info("Starting second solver.check()");
res = prover.isUnsat() ? PASS : UNKNOWN;
} else {
res = FAIL;
}
logger.info("Starting first solver.check()");
if (prover.isUnsat()) {
prover.pop();
prover.writeComment("Bound encoding");
prover.addConstraint(propertyEncoder.encodeBoundEventExec());
logger.info("Starting second solver.check()");
res = prover.isUnsat() ? PASS : UNKNOWN;
} else {
res = FAIL;
}

logger.info("Verification finished with result " + res);
}
Original file line number Diff line number Diff line change
@@ -162,7 +162,7 @@ private RefinementSolver() {
//TODO: We do not yet use Witness information. The problem is that WitnessGraph.encode() generates
// constraints on hb, which is not encoded in Refinement.
//TODO (2): Add possibility for Refinement to handle CAT-properties (it ignores them for now).
public static RefinementSolver run(SolverContext ctx, ProverEnvironment prover, VerificationTask task)
public static RefinementSolver run(SolverContext ctx, ProverWithTracker prover, VerificationTask task)
throws InterruptedException, SolverException, InvalidConfigurationException {
RefinementSolver solver = new RefinementSolver();
task.getConfig().inject(solver);
@@ -171,7 +171,7 @@ public static RefinementSolver run(SolverContext ctx, ProverEnvironment prover,
return solver;
}

private void runInternal(SolverContext ctx, ProverEnvironment prover, VerificationTask task)
private void runInternal(SolverContext ctx, ProverWithTracker prover, VerificationTask task)
throws InterruptedException, SolverException, InvalidConfigurationException {
final Program program = task.getProgram();
final Wmm memoryModel = task.getMemoryModel();
@@ -224,15 +224,19 @@ private void runInternal(SolverContext ctx, ProverEnvironment prover, Verificati
final Property.Type propertyType = Property.getCombinedType(task.getProperty(), task);

logger.info("Starting encoding using " + ctx.getVersion());
prover.writeComment("Program encoding");
prover.addConstraint(programEncoder.encodeFullProgram());
prover.writeComment("Memory model (baseline) encoding");
prover.addConstraint(baselineEncoder.encodeFullMemoryModel());
prover.writeComment("Symmetry breaking encoding");
prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking());

// ------------------------ Solving ------------------------
logger.info("Refinement procedure started.");

logger.info("Checking target property.");
prover.push();
prover.writeComment("Property encoding");
prover.addConstraint(propertyEncoder.encodeProperties(task.getProperty()));

final RefinementTrace propertyTrace = runRefinement(task, prover, solver, refiner);
@@ -265,8 +269,10 @@ private void runInternal(SolverContext ctx, ProverEnvironment prover, Verificati
logger.info("Checking unrolling bounds.");
final long lastTime = System.currentTimeMillis();
prover.pop();
prover.writeComment("Bound encoding");
prover.addConstraint(propertyEncoder.encodeBoundEventExec());
// Add back the refinement clauses we already found, hoping that this improves the performance.
prover.writeComment("Refinement encoding");
prover.addConstraint(bmgr.and(propertyTrace.getRefinementFormulas()));
final RefinementTrace boundTrace = runRefinement(task, prover, solver, refiner);
boundCheckTime = System.currentTimeMillis() - lastTime;
@@ -358,7 +364,7 @@ private void analyzeInconclusiveness(VerificationTask task, Context analysisCont
// Refinement core algorithm

// TODO: We could expose the following method(s) to allow for more general application of refinement.
private RefinementTrace runRefinement(VerificationTask task, ProverEnvironment prover, WMMSolver solver, Refiner refiner)
private RefinementTrace runRefinement(VerificationTask task, ProverWithTracker prover, WMMSolver solver, Refiner refiner)
throws SolverException, InterruptedException {

final List<RefinementIteration> trace = new ArrayList<>();
@@ -418,7 +424,7 @@ private boolean checkProgress(List<RefinementIteration> trace) {
return !last.inconsistencyReasons.equals(prev.inconsistencyReasons);
}

private RefinementIteration doRefinementIteration(ProverEnvironment prover, WMMSolver solver, Refiner refiner)
private RefinementIteration doRefinementIteration(ProverWithTracker prover, WMMSolver solver, Refiner refiner)
throws SolverException, InterruptedException {

long nativeTime = 0;
@@ -455,6 +461,7 @@ private RefinementIteration doRefinementIteration(ProverEnvironment prover, WMMS
inconsistencyReasons = solverResult.getCoreReasons();
lastTime = System.currentTimeMillis();
refinementFormula = refiner.refine(inconsistencyReasons, context);
prover.writeComment("Refinement encoding");
prover.addConstraint(refinementFormula);
refineTime = (System.currentTimeMillis() - lastTime);
}
Original file line number Diff line number Diff line change
@@ -1,21 +1,15 @@
package com.dat3m.dartagnan.wmm;

import com.dat3m.dartagnan.verification.Context;
import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis;
import com.dat3m.dartagnan.wmm.utils.EventGraph;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;

import java.util.Map;
import java.util.Set;

import static com.dat3m.dartagnan.wmm.utils.EventGraph.difference;
import static com.google.common.base.Preconditions.checkNotNull;

public final class Assumption implements Constraint {

private static final Logger logger = LogManager.getLogger(Assumption.class);

private final Relation rel;
private final EventGraph may;
private final EventGraph must;
Original file line number Diff line number Diff line change
@@ -3,7 +3,6 @@
import com.dat3m.dartagnan.encoding.EncodingContext;
import com.dat3m.dartagnan.verification.Context;
import com.dat3m.dartagnan.verification.VerificationTask;
import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis;
import com.dat3m.dartagnan.wmm.axiom.*;
import com.dat3m.dartagnan.wmm.definition.*;
import com.dat3m.dartagnan.wmm.utils.EventGraph;
Original file line number Diff line number Diff line change
@@ -3,6 +3,7 @@
import com.dat3m.dartagnan.configuration.Arch;
import com.dat3m.dartagnan.configuration.OptionNames;
import com.dat3m.dartagnan.configuration.Property;
import com.dat3m.dartagnan.encoding.ProverWithTracker;
import com.dat3m.dartagnan.program.Program;
import com.dat3m.dartagnan.utils.Result;
import com.dat3m.dartagnan.utils.rules.Provider;
@@ -17,7 +18,6 @@
import org.sosy_lab.common.configuration.Configuration;
import org.sosy_lab.common.configuration.InvalidConfigurationException;
import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
import org.sosy_lab.java_smt.api.ProverEnvironment;
import org.sosy_lab.java_smt.api.SolverContext;

import java.util.EnumSet;
@@ -84,7 +84,7 @@ protected Provider<Configuration> getConfigurationProvider() {
protected final Provider<Configuration> configurationProvider = getConfigurationProvider();
protected final Provider<VerificationTask> taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, boundProvider, configurationProvider);
protected final Provider<SolverContext> contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider, solverProvider);
protected final Provider<ProverEnvironment> proverProvider = Providers.createProverWithFixedOptions(contextProvider, SolverContext.ProverOptions.GENERATE_MODELS);
protected final Provider<ProverWithTracker> proverProvider = Providers.createProverWithFixedOptions(contextProvider, SolverContext.ProverOptions.GENERATE_MODELS);

// Special rules
protected final Timeout timeout = Timeout.millis(getTimeout());
Original file line number Diff line number Diff line change
@@ -2,6 +2,7 @@

import com.dat3m.dartagnan.configuration.Arch;
import com.dat3m.dartagnan.configuration.Property;
import com.dat3m.dartagnan.encoding.ProverWithTracker;
import com.dat3m.dartagnan.program.Program;
import com.dat3m.dartagnan.program.event.Event;
import com.dat3m.dartagnan.program.event.Tag;
@@ -19,7 +20,6 @@
import org.sosy_lab.common.ShutdownManager;
import org.sosy_lab.common.configuration.Configuration;
import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
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;

@@ -99,8 +99,8 @@ protected Provider<Configuration> getConfigurationProvider() {
protected final Provider<VerificationTask> task2Provider = Providers.createTask(program2Provider, wmm2Provider, propertyProvider, targetProvider, () -> 1, configProvider);
protected final Provider<SolverContext> context1Provider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3);
protected final Provider<SolverContext> context2Provider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3);
protected final Provider<ProverEnvironment> prover1Provider = Providers.createProverWithFixedOptions(context1Provider, ProverOptions.GENERATE_MODELS);
protected final Provider<ProverEnvironment> prover2Provider = Providers.createProverWithFixedOptions(context2Provider, ProverOptions.GENERATE_MODELS);
protected final Provider<ProverWithTracker> prover1Provider = Providers.createProverWithFixedOptions(context1Provider, ProverOptions.GENERATE_MODELS);
protected final Provider<ProverWithTracker> prover2Provider = Providers.createProverWithFixedOptions(context2Provider, ProverOptions.GENERATE_MODELS);

private final Timeout timeout = Timeout.millis(getTimeout());
private final RequestShutdownOnError shutdownOnError = RequestShutdownOnError.create(shutdownManagerProvider);
Original file line number Diff line number Diff line change
@@ -2,6 +2,7 @@

import com.dat3m.dartagnan.configuration.Arch;
import com.dat3m.dartagnan.configuration.Property;
import com.dat3m.dartagnan.encoding.ProverWithTracker;
import com.dat3m.dartagnan.program.Program;
import com.dat3m.dartagnan.utils.ResourceHelper;
import com.dat3m.dartagnan.utils.Result;
@@ -19,7 +20,6 @@
import org.sosy_lab.common.ShutdownManager;
import org.sosy_lab.common.configuration.Configuration;
import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
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;

@@ -110,8 +110,8 @@ protected long getTimeout() {
protected final Provider<Configuration> configProvider = getConfigurationProvider();
protected final Provider<VerificationTask> taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, boundProvider, configProvider);
protected final Provider<SolverContext> contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3);
protected final Provider<ProverEnvironment> proverProvider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS);
protected final Provider<ProverEnvironment> prover2Provider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS);
protected final Provider<ProverWithTracker> proverProvider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS);
protected final Provider<ProverWithTracker> prover2Provider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS);

private final Timeout timeout = Timeout.millis(getTimeout());
private final RequestShutdownOnError shutdownOnError = RequestShutdownOnError.create(shutdownManagerProvider);
Original file line number Diff line number Diff line change
@@ -2,6 +2,7 @@

import com.dat3m.dartagnan.configuration.Arch;
import com.dat3m.dartagnan.configuration.Property;
import com.dat3m.dartagnan.encoding.ProverWithTracker;
import com.dat3m.dartagnan.parsers.cat.ParserCat;
import com.dat3m.dartagnan.parsers.program.ProgramParser;
import com.dat3m.dartagnan.program.Program;
@@ -12,7 +13,6 @@
import org.junit.Test;
import org.junit.runner.RunWith;
import org.junit.runners.Parameterized;
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;

@@ -56,7 +56,7 @@ public ArrayValidTest(String path, Wmm wmm) {
@Test
public void test() {
try (SolverContext ctx = TestHelper.createContext();
ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
ProverWithTracker prover = new ProverWithTracker(ctx, "", ProverOptions.GENERATE_MODELS)) {
Program program = new ProgramParser().parse(new File(path));
VerificationTask task = VerificationTask.builder()
.withSolverTimeout(60)
Original file line number Diff line number Diff line change
@@ -2,6 +2,7 @@

import com.dat3m.dartagnan.configuration.Arch;
import com.dat3m.dartagnan.configuration.Property;
import com.dat3m.dartagnan.encoding.ProverWithTracker;
import com.dat3m.dartagnan.parsers.cat.ParserCat;
import com.dat3m.dartagnan.parsers.program.ProgramParser;
import com.dat3m.dartagnan.program.Program;
@@ -14,7 +15,6 @@
import org.junit.Test;
import org.junit.runner.RunWith;
import org.junit.runners.Parameterized;
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;

@@ -95,7 +95,7 @@ public BranchTest(String path, Result expected, Wmm wmm) {
@Test
public void test() {
try (SolverContext ctx = TestHelper.createContext();
ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
ProverWithTracker prover = new ProverWithTracker(ctx, "", ProverOptions.GENERATE_MODELS)) {
Program program = new ProgramParser().parse(new File(path));
VerificationTask task = VerificationTask.builder()
.withSolverTimeout(60)
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
package com.dat3m.dartagnan.spirv.basic;

import com.dat3m.dartagnan.configuration.Arch;
import com.dat3m.dartagnan.encoding.ProverWithTracker;
import com.dat3m.dartagnan.parsers.cat.ParserCat;
import com.dat3m.dartagnan.parsers.program.ProgramParser;
import com.dat3m.dartagnan.program.Program;
@@ -17,7 +18,6 @@
import org.sosy_lab.common.configuration.InvalidConfigurationException;
import org.sosy_lab.common.log.BasicLogManager;
import org.sosy_lab.java_smt.SolverContextFactory;
import org.sosy_lab.java_smt.api.ProverEnvironment;
import org.sosy_lab.java_smt.api.SolverContext;

import java.io.File;
@@ -113,10 +113,10 @@ public static Iterable<Object[]> data() throws IOException {

@Test
public void testAllSolvers() throws Exception {
try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult());
try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) {
assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult());
}
try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) {
assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult());
}
}
@@ -130,8 +130,8 @@ private SolverContext mkCtx() throws InvalidConfigurationException {
SolverContextFactory.Solvers.Z3);
}

private ProverEnvironment mkProver(SolverContext ctx) {
return ctx.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS);
private ProverWithTracker mkProver(SolverContext ctx) {
return new ProverWithTracker(ctx, "", SolverContext.ProverOptions.GENERATE_MODELS);
}

private VerificationTask mkTask() throws Exception {
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
package com.dat3m.dartagnan.spirv.benchmarks;

import com.dat3m.dartagnan.configuration.Arch;
import com.dat3m.dartagnan.encoding.ProverWithTracker;
import com.dat3m.dartagnan.parsers.cat.ParserCat;
import com.dat3m.dartagnan.parsers.program.ProgramParser;
import com.dat3m.dartagnan.program.Program;
@@ -17,7 +18,6 @@
import org.sosy_lab.common.configuration.InvalidConfigurationException;
import org.sosy_lab.common.log.BasicLogManager;
import org.sosy_lab.java_smt.SolverContextFactory;
import org.sosy_lab.java_smt.api.ProverEnvironment;
import org.sosy_lab.java_smt.api.SolverContext;

import java.io.File;
@@ -114,10 +114,10 @@ public static Iterable<Object[]> data() throws IOException {

@Test
public void testAllSolvers() throws Exception {
try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) {
assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult());
}
try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) {
assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult());
}
}
@@ -131,8 +131,8 @@ private SolverContext mkCtx() throws InvalidConfigurationException {
SolverContextFactory.Solvers.Z3);
}

private ProverEnvironment mkProver(SolverContext ctx) {
return ctx.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS);
private ProverWithTracker mkProver(SolverContext ctx) {
return new ProverWithTracker(ctx, "", SolverContext.ProverOptions.GENERATE_MODELS);
}

private VerificationTask mkTask() throws Exception {
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
package com.dat3m.dartagnan.spirv.benchmarks;

import com.dat3m.dartagnan.configuration.Arch;
import com.dat3m.dartagnan.encoding.ProverWithTracker;
import com.dat3m.dartagnan.parsers.cat.ParserCat;
import com.dat3m.dartagnan.parsers.program.ProgramParser;
import com.dat3m.dartagnan.program.Program;
@@ -17,7 +18,6 @@
import org.sosy_lab.common.configuration.InvalidConfigurationException;
import org.sosy_lab.common.log.BasicLogManager;
import org.sosy_lab.java_smt.SolverContextFactory;
import org.sosy_lab.java_smt.api.ProverEnvironment;
import org.sosy_lab.java_smt.api.SolverContext;

import java.io.File;
@@ -118,10 +118,10 @@ public static Iterable<Object[]> data() throws IOException {

@Test
public void testAllSolvers() throws Exception {
try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult());
try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) {
assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult());
}
try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) {
assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult());
}
}
@@ -135,8 +135,8 @@ private SolverContext mkCtx() throws InvalidConfigurationException {
SolverContextFactory.Solvers.Z3);
}

private ProverEnvironment mkProver(SolverContext ctx) {
return ctx.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS);
private ProverWithTracker mkProver(SolverContext ctx) {
return new ProverWithTracker(ctx, "", SolverContext.ProverOptions.GENERATE_MODELS);
}

private VerificationTask mkTask() throws Exception {
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
package com.dat3m.dartagnan.spirv.benchmarks;

import com.dat3m.dartagnan.configuration.Arch;
import com.dat3m.dartagnan.encoding.ProverWithTracker;
import com.dat3m.dartagnan.parsers.cat.ParserCat;
import com.dat3m.dartagnan.parsers.program.ProgramParser;
import com.dat3m.dartagnan.program.Program;
@@ -17,7 +18,6 @@
import org.sosy_lab.common.configuration.InvalidConfigurationException;
import org.sosy_lab.common.log.BasicLogManager;
import org.sosy_lab.java_smt.SolverContextFactory;
import org.sosy_lab.java_smt.api.ProverEnvironment;
import org.sosy_lab.java_smt.api.SolverContext;

import java.io.File;
@@ -119,10 +119,10 @@ public static Iterable<Object[]> data() throws IOException {

@Test
public void testAllSolvers() throws Exception {
try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult());
try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) {
assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult());
}
try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) {
assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult());
}
}
@@ -136,8 +136,8 @@ private SolverContext mkCtx() throws InvalidConfigurationException {
SolverContextFactory.Solvers.Z3);
}

private ProverEnvironment mkProver(SolverContext ctx) {
return ctx.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS);
private ProverWithTracker mkProver(SolverContext ctx) {
return new ProverWithTracker(ctx, "", SolverContext.ProverOptions.GENERATE_MODELS);
}

private VerificationTask mkTask() throws Exception {
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
package com.dat3m.dartagnan.spirv.gpuverify;

import com.dat3m.dartagnan.configuration.Arch;
import com.dat3m.dartagnan.encoding.ProverWithTracker;
import com.dat3m.dartagnan.parsers.cat.ParserCat;
import com.dat3m.dartagnan.parsers.program.ProgramParser;
import com.dat3m.dartagnan.program.Program;
@@ -17,7 +18,6 @@
import org.sosy_lab.common.configuration.InvalidConfigurationException;
import org.sosy_lab.common.log.BasicLogManager;
import org.sosy_lab.java_smt.SolverContextFactory;
import org.sosy_lab.java_smt.api.ProverEnvironment;
import org.sosy_lab.java_smt.api.SolverContext;

import java.io.File;
@@ -346,10 +346,10 @@ public static Iterable<Object[]> data() throws IOException {

@Test
public void testAllSolvers() throws Exception {
try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult());
try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) {
assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult());
}
try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) {
assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult());
}
}
@@ -363,8 +363,8 @@ private SolverContext mkCtx() throws InvalidConfigurationException {
SolverContextFactory.Solvers.Z3);
}

private ProverEnvironment mkProver(SolverContext ctx) {
return ctx.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS);
private ProverWithTracker mkProver(SolverContext ctx) {
return new ProverWithTracker(ctx, "", SolverContext.ProverOptions.GENERATE_MODELS);
}

private VerificationTask mkTask() throws Exception {
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
package com.dat3m.dartagnan.spirv.gpuverify;

import com.dat3m.dartagnan.configuration.Arch;
import com.dat3m.dartagnan.encoding.ProverWithTracker;
import com.dat3m.dartagnan.parsers.cat.ParserCat;
import com.dat3m.dartagnan.parsers.program.ProgramParser;
import com.dat3m.dartagnan.program.Program;
@@ -17,7 +18,6 @@
import org.sosy_lab.common.configuration.InvalidConfigurationException;
import org.sosy_lab.common.log.BasicLogManager;
import org.sosy_lab.java_smt.SolverContextFactory;
import org.sosy_lab.java_smt.api.ProverEnvironment;
import org.sosy_lab.java_smt.api.SolverContext;

import java.io.File;
@@ -346,10 +346,10 @@ public static Iterable<Object[]> data() throws IOException {

@Test
public void testAllSolvers() throws Exception {
try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult());
try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) {
assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult());
}
try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) {
assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult());
}
}
@@ -363,8 +363,8 @@ private SolverContext mkCtx() throws InvalidConfigurationException {
SolverContextFactory.Solvers.Z3);
}

private ProverEnvironment mkProver(SolverContext ctx) {
return ctx.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS);
private ProverWithTracker mkProver(SolverContext ctx) {
return new ProverWithTracker(ctx, "", SolverContext.ProverOptions.GENERATE_MODELS);
}

private VerificationTask mkTask() throws Exception {
Original file line number Diff line number Diff line change
@@ -8,12 +8,12 @@
import com.dat3m.dartagnan.wmm.Wmm;
import com.dat3m.dartagnan.configuration.Arch;
import com.dat3m.dartagnan.configuration.Property;
import com.dat3m.dartagnan.encoding.ProverWithTracker;

import org.sosy_lab.common.ShutdownManager;
import org.sosy_lab.common.ShutdownNotifier;
import org.sosy_lab.common.configuration.Configuration;
import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
import org.sosy_lab.java_smt.api.ProverEnvironment;
import org.sosy_lab.java_smt.api.SolverContext;

import java.io.File;
@@ -81,11 +81,11 @@ public static Provider<SolverContext> createSolverContextFromManager(Supplier<Sh
return Provider.fromSupplier(() -> TestHelper.createContextWithShutdownNotifier(shutdownManagerSupplier.get().getNotifier(), solverSupplier.get()));
}

public static Provider<ProverEnvironment> createProver(Supplier<SolverContext> contextSupplier, Supplier<SolverContext.ProverOptions[]> optionsSupplier) {
return Provider.fromSupplier(() -> contextSupplier.get().newProverEnvironment(optionsSupplier.get()));
public static Provider<ProverWithTracker> createProver(Supplier<SolverContext> contextSupplier, Supplier<SolverContext.ProverOptions[]> optionsSupplier) {
return Provider.fromSupplier(() -> new ProverWithTracker(contextSupplier.get(), "", optionsSupplier.get()));
}

public static Provider<ProverEnvironment> createProverWithFixedOptions(Supplier<SolverContext> contextSupplier, SolverContext.ProverOptions... options) {
public static Provider<ProverWithTracker> createProverWithFixedOptions(Supplier<SolverContext> contextSupplier, SolverContext.ProverOptions... options) {
return createProver(contextSupplier, () -> options);
}
}
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
package com.dat3m.dartagnan.witness;

import com.dat3m.dartagnan.configuration.Property;
import com.dat3m.dartagnan.encoding.ProverWithTracker;
import com.dat3m.dartagnan.parsers.cat.ParserCat;
import com.dat3m.dartagnan.parsers.program.ProgramParser;
import com.dat3m.dartagnan.program.Program;
@@ -15,7 +16,6 @@
import org.sosy_lab.common.configuration.Configuration;
import org.sosy_lab.java_smt.api.BooleanFormula;
import org.sosy_lab.java_smt.api.BooleanFormulaManager;
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;

@@ -43,7 +43,7 @@ public void BuildWriteEncode() throws Exception {
Wmm wmm = new ParserCat().parse(new File(getRootPath("cat/svcomp.cat")));
VerificationTask task = VerificationTask.builder().withConfig(config).build(p, wmm, Property.getDefault());
try (SolverContext ctx = TestHelper.createContext();
ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
ProverWithTracker prover = new ProverWithTracker(ctx, "", ProverOptions.GENERATE_MODELS)) {
AssumeSolver modelChecker = AssumeSolver.run(ctx, prover, task);
Result res = modelChecker.getResult();
WitnessBuilder witnessBuilder = WitnessBuilder.of(modelChecker.getEncodingContext(), prover, res, "user assertion");
4 changes: 2 additions & 2 deletions ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java
Original file line number Diff line number Diff line change
@@ -10,13 +10,13 @@
import com.dat3m.dartagnan.verification.solving.RefinementSolver;
import com.dat3m.dartagnan.witness.WitnessType;
import com.dat3m.dartagnan.wmm.Wmm;
import com.dat3m.dartagnan.encoding.ProverWithTracker;
import com.dat3m.ui.utils.UiOptions;
import com.dat3m.ui.utils.Utils;
import org.sosy_lab.common.ShutdownManager;
import org.sosy_lab.common.configuration.Configuration;
import org.sosy_lab.common.log.BasicLogManager;
import org.sosy_lab.java_smt.SolverContextFactory;
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;

@@ -92,7 +92,7 @@ private void run() {
BasicLogManager.create(solverConfig),
sdm.getNotifier(),
options.solver());
ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
ProverWithTracker prover = new ProverWithTracker(ctx, "", ProverOptions.GENERATE_MODELS)) {

final ModelChecker modelChecker; modelChecker = switch (options.method()) {
case EAGER -> AssumeSolver.run(ctx, prover, task);

0 comments on commit 2a0ed59

Please sign in to comment.