From 953597ea9b17827fd4d7a5facfe9c942fe191598 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 27 Aug 2024 20:06:49 +0200 Subject: [PATCH 01/31] Add option to dump encoding to smtlib2 file --- .../java/com/dat3m/dartagnan/Dartagnan.java | 14 ++-- .../dartagnan/configuration/OptionNames.java | 1 + .../dartagnan/encoding/ProverWithTracker.java | 82 +++++++++++++++++++ .../processing/compilation/VisitorLKMM.java | 2 - .../dartagnan/utils/options/BaseOptions.java | 7 ++ .../verification/solving/AssumeSolver.java | 6 +- .../verification/solving/DataRaceSolver.java | 8 +- .../verification/solving/ModelChecker.java | 4 +- .../solving/RefinementSolver.java | 8 +- .../witness/graphml/WitnessBuilder.java | 8 +- .../com/dat3m/dartagnan/wmm/Assumption.java | 6 -- .../com/dat3m/dartagnan/wmm/Constraint.java | 1 - .../com/dat3m/dartagnan/c/AbstractCTest.java | 4 +- .../compilation/AbstractCompilationTest.java | 5 +- .../dartagnan/litmus/AbstractLitmusTest.java | 6 +- .../miscellaneous/ArrayValidTest.java | 4 +- .../dartagnan/miscellaneous/BranchTest.java | 4 +- .../spirv/basic/SpirvAssertionsTest.java | 8 +- .../spirv/benchmarks/SpirvAssertionsTest.java | 8 +- .../spirv/benchmarks/SpirvChecksTest.java | 8 +- .../spirv/benchmarks/SpirvRacesTest.java | 8 +- .../spirv/gpuverify/SpirvChecksTest.java | 8 +- .../spirv/gpuverify/SpirvRacesTest.java | 8 +- .../dartagnan/utils/rules/Providers.java | 8 +- .../dartagnan/witness/BuildWitnessTest.java | 4 +- 25 files changed, 158 insertions(+), 72 deletions(-) create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 3ccab85b38..f8e0765223 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -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) { @@ -207,7 +211,7 @@ public static void main(String[] args) throws Exception { } } - public static File generateExecutionGraphFile(VerificationTask task, ProverEnvironment prover, ModelChecker modelChecker, + public static File generateExecutionGraphFile(VerificationTask task, ProverWithTracker prover, ModelChecker modelChecker, WitnessType witnessType) throws InvalidConfigurationException, SolverException, IOException { Preconditions.checkArgument(modelChecker.hasModel(), "No execution graph to generate."); @@ -228,7 +232,7 @@ public static File generateExecutionGraphFile(VerificationTask task, ProverEnvir synContext, witnessType.convertToPng()); } - private static void generateWitnessIfAble(VerificationTask task, ProverEnvironment prover, + private static void generateWitnessIfAble(VerificationTask task, ProverWithTracker prover, ModelChecker modelChecker, String summary) { // ------------------ Generate Witness, if possible ------------------ final EnumSet properties = task.getProperty(); @@ -247,7 +251,7 @@ private static void generateWitnessIfAble(VerificationTask task, ProverEnvironme } } - public static String generateResultSummary(VerificationTask task, ProverEnvironment prover, + public static String generateResultSummary(VerificationTask task, ProverWithTracker prover, ModelChecker modelChecker) throws SolverException { // ----------------- Generate output of verification result ----------------- final Program p = task.getProgram(); @@ -385,7 +389,7 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm return summary.toString(); } - private static void printWarningIfThreadStartFailed(Program p, EncodingContext encoder, ProverEnvironment prover) + private static void printWarningIfThreadStartFailed(Program p, EncodingContext encoder, ProverWithTracker prover) throws SolverException { for (Event e : p.getThreadEvents()) { if (e.hasTag(Tag.STARTLOAD) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java index 3cec00bf75..18a0ca89fc 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java @@ -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"; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java new file mode 100644 index 0000000000..6737036aaa --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -0,0 +1,82 @@ +package com.dat3m.dartagnan.encoding; + +import java.io.File; +import java.io.FileWriter; +import java.io.IOException; +import java.io.PrintWriter; +import java.util.Collection; + +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.FormulaManager; +import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.ProverEnvironment; +import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; + +import com.google.common.collect.ImmutableMap; + +public class ProverWithTracker implements AutoCloseable { + + private final FormulaManager fmgr; + private final ProverEnvironment prover; + private final String fileName; + private BooleanFormula enc; + + public ProverWithTracker(SolverContext ctx, String filename, ProverOptions... options) { + this.fmgr = ctx.getFormulaManager(); + this.prover = ctx.newProverEnvironment(options); + this.enc = ctx.getFormulaManager().getBooleanFormulaManager().makeTrue(); + this.fileName = filename; + } + + @Override + public void close() throws Exception { + if(!fileName.isEmpty()) { + File file = new File(fileName); + FileWriter writer; + try { + writer = new FileWriter(file, true); + PrintWriter printer = new PrintWriter(writer); + printer.append("(set-logic ALL)\n"); + printer.append(fmgr.dumpFormula(enc).toString()); + printer.append("(check-sat)"); + printer.close(); + } catch (IOException e) { + e.printStackTrace(); + } + } + prover.close(); + } + + public void addConstraint(BooleanFormula f) throws InterruptedException { + if(!fileName.isEmpty()) { + enc = fmgr.getBooleanFormulaManager().and(f, enc); + } + prover.addConstraint(f); + } + + public boolean isUnsatWithAssumptions(Collection f) throws SolverException, InterruptedException { + return prover.isUnsatWithAssumptions(f); + } + + public boolean isUnsat() throws SolverException, InterruptedException { + return prover.isUnsat(); + } + + public ImmutableMap getStatistics() { + return prover.getStatistics(); + } + + public Model getModel() throws SolverException { + return prover.getModel(); + } + + public void push() throws InterruptedException { + prover.push(); + } + + public void pop() { + prover.pop(); + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java index b448471580..d858308a5f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java @@ -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; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java index 32cfec175a..fd166a38e0 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java @@ -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; } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java index cc0200630b..38b18925ec 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java @@ -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(); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java index 5190ef5d4c..c0d9b136ca 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java @@ -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; @@ -25,16 +25,16 @@ public class DataRaceSolver extends ModelChecker { private static final Logger logger = LogManager.getLogger(DataRaceSolver.class); private final SolverContext ctx; - private final ProverEnvironment prover; + private final ProverWithTracker prover; private final VerificationTask task; - private DataRaceSolver(SolverContext c, ProverEnvironment p, VerificationTask 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) + public static DataRaceSolver run(SolverContext ctx, ProverWithTracker prover, VerificationTask task) throws InterruptedException, SolverException, InvalidConfigurationException { DataRaceSolver s = new DataRaceSolver(ctx, prover, task); s.run(); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java index cac688c576..3b657a1ff3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java @@ -2,6 +2,7 @@ import com.dat3m.dartagnan.configuration.Property; import com.dat3m.dartagnan.encoding.EncodingContext; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.encoding.WmmEncoder; import com.dat3m.dartagnan.exception.UnsatisfiedRequirementException; import com.dat3m.dartagnan.program.Program; @@ -21,7 +22,6 @@ import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.java_smt.api.Model; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverException; import java.util.Optional; @@ -109,7 +109,7 @@ public static void performStaticWmmAnalyses(VerificationTask task, Context analy analysisContext.register(RelationAnalysis.class, RelationAnalysis.fromConfig(task, analysisContext, config)); } - protected void saveFlaggedPairsOutput(Wmm wmm, WmmEncoder encoder, ProverEnvironment prover, EncodingContext ctx, Program program) throws SolverException { + protected void saveFlaggedPairsOutput(Wmm wmm, WmmEncoder encoder, ProverWithTracker prover, EncodingContext ctx, Program program) throws SolverException { if (!ctx.getTask().getProperty().contains(CAT_SPEC)) { return; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java index bebb12fd78..2be1835018 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java @@ -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(); @@ -358,7 +358,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 trace = new ArrayList<>(); @@ -418,7 +418,7 @@ private boolean checkProgress(List 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; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java index 7e71e3baac..e00580645e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.witness.graphml; import com.dat3m.dartagnan.encoding.EncodingContext; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.expression.booleans.BoolLiteral; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Thread; @@ -16,7 +17,6 @@ import org.sosy_lab.common.configuration.Option; import org.sosy_lab.common.configuration.Options; import org.sosy_lab.java_smt.api.Model; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverException; import java.io.File; @@ -40,7 +40,7 @@ public class WitnessBuilder { private final EncodingContext context; - private final ProverEnvironment prover; + private final ProverWithTracker prover; private final String type; private final String ltlProperty; @@ -60,14 +60,14 @@ public boolean canBeBuilt() { private final Map eventThreadMap = new HashMap<>(); - private WitnessBuilder(EncodingContext c, ProverEnvironment p, Result r, String summary) { + private WitnessBuilder(EncodingContext c, ProverWithTracker p, Result r, String summary) { context = checkNotNull(c); prover = checkNotNull(p); type = r.equals(FAIL) ? "violation" : "correctness"; ltlProperty = getLtlPropertyFromSummary(summary); } - public static WitnessBuilder of(EncodingContext context, ProverEnvironment prover, Result result, + public static WitnessBuilder of(EncodingContext context, ProverWithTracker prover, Result result, String ltlProperty) throws InvalidConfigurationException { WitnessBuilder b = new WitnessBuilder(context, prover, result, ltlProperty); context.getTask().getConfig().inject(b); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java index 2da9f984e9..788a3b8f09 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java @@ -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; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java index 1a674d9626..4c5ef52794 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java @@ -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; diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java index 8593902783..39d4ef879d 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java @@ -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 getConfigurationProvider() { protected final Provider configurationProvider = getConfigurationProvider(); protected final Provider taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, boundProvider, configurationProvider); protected final Provider contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider, solverProvider); - protected final Provider proverProvider = Providers.createProverWithFixedOptions(contextProvider, SolverContext.ProverOptions.GENERATE_MODELS); + protected final Provider proverProvider = Providers.createProverWithFixedOptions(contextProvider, SolverContext.ProverOptions.GENERATE_MODELS); // Special rules protected final Timeout timeout = Timeout.millis(getTimeout()); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java index b92e1209f5..4ca30a5d84 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java @@ -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; @@ -99,8 +100,8 @@ protected Provider getConfigurationProvider() { protected final Provider task2Provider = Providers.createTask(program2Provider, wmm2Provider, propertyProvider, targetProvider, () -> 1, configProvider); protected final Provider context1Provider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3); protected final Provider context2Provider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3); - protected final Provider prover1Provider = Providers.createProverWithFixedOptions(context1Provider, ProverOptions.GENERATE_MODELS); - protected final Provider prover2Provider = Providers.createProverWithFixedOptions(context2Provider, ProverOptions.GENERATE_MODELS); + protected final Provider prover1Provider = Providers.createProverWithFixedOptions(context1Provider, ProverOptions.GENERATE_MODELS); + protected final Provider prover2Provider = Providers.createProverWithFixedOptions(context2Provider, ProverOptions.GENERATE_MODELS); private final Timeout timeout = Timeout.millis(getTimeout()); private final RequestShutdownOnError shutdownOnError = RequestShutdownOnError.create(shutdownManagerProvider); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java index 1e86058312..3316d114eb 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java @@ -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 configProvider = getConfigurationProvider(); protected final Provider taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, boundProvider, configProvider); protected final Provider contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3); - protected final Provider proverProvider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS); - protected final Provider prover2Provider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS); + protected final Provider proverProvider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS); + protected final Provider prover2Provider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS); private final Timeout timeout = Timeout.millis(getTimeout()); private final RequestShutdownOnError shutdownOnError = RequestShutdownOnError.create(shutdownManagerProvider); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/ArrayValidTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/ArrayValidTest.java index fa2d573259..e8ba520d5c 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/ArrayValidTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/ArrayValidTest.java @@ -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) diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/BranchTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/BranchTest.java index 05d84eb465..588dc3cdb0 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/BranchTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/BranchTest.java @@ -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) diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java index 18878d7f92..3c08d4319b 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java @@ -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; @@ -16,7 +17,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; @@ -124,7 +124,7 @@ 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(); ProverEnvironment prover = mkProver(ctx)) { + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } } @@ -138,8 +138,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 { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java index 96acad8bbc..a7fb3760e3 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java @@ -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; @@ -16,7 +17,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; @@ -117,7 +117,7 @@ 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(); 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 { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java index 6043e53303..11f0472834 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java @@ -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; @@ -16,7 +17,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; @@ -121,7 +121,7 @@ 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(); 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 { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java index 5f4ac94440..e5dc3c4c22 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java @@ -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; @@ -16,7 +17,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; @@ -122,7 +122,7 @@ 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(); 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 { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java index 6124efb5b0..7ade7546f8 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java @@ -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; @@ -16,7 +17,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; @@ -349,7 +349,7 @@ 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(); 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 { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java index 29b7ad7990..4344f1a67e 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java @@ -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; @@ -16,7 +17,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; @@ -349,7 +349,7 @@ 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(); 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 { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java b/dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java index 0b8c06b449..f31db39a13 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java @@ -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 createSolverContextFromManager(Supplier TestHelper.createContextWithShutdownNotifier(shutdownManagerSupplier.get().getNotifier(), solverSupplier.get())); } - public static Provider createProver(Supplier contextSupplier, Supplier optionsSupplier) { - return Provider.fromSupplier(() -> contextSupplier.get().newProverEnvironment(optionsSupplier.get())); + public static Provider createProver(Supplier contextSupplier, Supplier optionsSupplier) { + return Provider.fromSupplier(() -> new ProverWithTracker(contextSupplier.get(), "", optionsSupplier.get())); } - public static Provider createProverWithFixedOptions(Supplier contextSupplier, SolverContext.ProverOptions... options) { + public static Provider createProverWithFixedOptions(Supplier contextSupplier, SolverContext.ProverOptions... options) { return createProver(contextSupplier, () -> options); } } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java index 98b1d7d9ee..7b4d135cb4 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java @@ -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"); From 61381f3210eced4d1cf4084a68a44c7348447cd6 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Wed, 28 Aug 2024 17:15:59 +0200 Subject: [PATCH 02/31] Dump formula in each access to the prover --- .../java/com/dat3m/dartagnan/Dartagnan.java | 1 - .../dartagnan/encoding/ProverWithTracker.java | 106 +++++++++++++----- 2 files changed, 78 insertions(+), 29 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index f8e0765223..fae62e2651 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -43,7 +43,6 @@ import org.sosy_lab.common.log.BasicLogManager; import org.sosy_lab.java_smt.SolverContextFactory; import org.sosy_lab.java_smt.api.Model; -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 org.sosy_lab.java_smt.api.SolverException; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index 6737036aaa..d30496a3a5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -1,17 +1,18 @@ package com.dat3m.dartagnan.encoding; +import java.io.BufferedReader; +import java.io.BufferedWriter; import java.io.File; +import java.io.FileReader; import java.io.FileWriter; import java.io.IOException; import java.io.PrintWriter; +import java.nio.file.Files; +import java.nio.file.Paths; +import java.util.ArrayList; import java.util.Collection; - -import org.sosy_lab.java_smt.api.BooleanFormula; -import org.sosy_lab.java_smt.api.FormulaManager; -import org.sosy_lab.java_smt.api.Model; -import org.sosy_lab.java_smt.api.ProverEnvironment; -import org.sosy_lab.java_smt.api.SolverContext; -import org.sosy_lab.java_smt.api.SolverException; +import java.util.List; +import org.sosy_lab.java_smt.api.*; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import com.google.common.collect.ImmutableMap; @@ -21,46 +22,76 @@ public class ProverWithTracker implements AutoCloseable { private final FormulaManager fmgr; private final ProverEnvironment prover; private final String fileName; - private BooleanFormula enc; - public ProverWithTracker(SolverContext ctx, String filename, ProverOptions... options) { + public ProverWithTracker(SolverContext ctx, String fileName, ProverOptions... options) { this.fmgr = ctx.getFormulaManager(); this.prover = ctx.newProverEnvironment(options); - this.enc = ctx.getFormulaManager().getBooleanFormulaManager().makeTrue(); - this.fileName = filename; + this.fileName = fileName; + init(); + } + + private void init() { + try { + Files.deleteIfExists(Paths.get(fileName)); + write("(set-logic ALL)\n"); + } catch (IOException e) { + e.printStackTrace(); + } } @Override public void close() throws Exception { - if(!fileName.isEmpty()) { - File file = new File(fileName); - FileWriter writer; - try { - writer = new FileWriter(file, true); - PrintWriter printer = new PrintWriter(writer); - printer.append("(set-logic ALL)\n"); - printer.append(fmgr.dumpFormula(enc).toString()); - printer.append("(check-sat)"); - printer.close(); - } catch (IOException e) { - e.printStackTrace(); - } - } + removeDuplicatedDeclarations(fileName); prover.close(); } + private void removeDuplicatedDeclarations(String fileName) { + try { + BufferedReader reader = new BufferedReader(new FileReader(fileName)); + List newLines = new ArrayList<>(); + String line; + while ((line = reader.readLine()) != null) { + // We only skip repeated declarations + if (!line.contains("declare-fun") || !newLines.contains(line)) { + newLines.add(line); + } + } + reader.close(); + + BufferedWriter writer = new BufferedWriter(new FileWriter(fileName)); + for (String newLine : newLines) { + writer.write(newLine); + writer.newLine(); + } + writer.close(); + } catch (IOException e) { + e.printStackTrace(); + } + } + public void addConstraint(BooleanFormula f) throws InterruptedException { if(!fileName.isEmpty()) { - enc = fmgr.getBooleanFormulaManager().and(f, enc); + write(fmgr.dumpFormula(f).toString()); } prover.addConstraint(f); } - public boolean isUnsatWithAssumptions(Collection f) throws SolverException, InterruptedException { - return prover.isUnsatWithAssumptions(f); + public boolean isUnsatWithAssumptions(Collection fs) throws SolverException, InterruptedException { + if(!fileName.isEmpty()) { + write("(push)\n"); + for(BooleanFormula f : fs) { + write(fmgr.dumpFormula(f).toString()); + } + write("(check-sat)\n"); + write("(pop)\n"); + } + return prover.isUnsatWithAssumptions(fs); } public boolean isUnsat() throws SolverException, InterruptedException { + if(!fileName.isEmpty()) { + write("(check-sat)\n"); + } return prover.isUnsat(); } @@ -73,10 +104,29 @@ public Model getModel() throws SolverException { } public void push() throws InterruptedException { + if(!fileName.isEmpty()) { + write("(push)\n"); + } prover.push(); } public void pop() { + if(!fileName.isEmpty()) { + write("(pop)\n"); + } prover.pop(); } + + private void write(String content) { + File file = new File(fileName); + FileWriter writer; + try { + writer = new FileWriter(file, true); + PrintWriter printer = new PrintWriter(writer); + printer.append(content); + printer.close(); + } catch (IOException e) { + e.printStackTrace(); + } + } } From f0053859aa2afa7ccaf052254e51c7e7cddc0605 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Wed, 28 Aug 2024 17:28:32 +0200 Subject: [PATCH 03/31] Minor changes --- .../java/com/dat3m/dartagnan/Dartagnan.java | 2 +- .../dartagnan/encoding/ProverWithTracker.java | 26 ++++++++++++++----- 2 files changed, 20 insertions(+), 8 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index fae62e2651..3cb97bdef5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -164,7 +164,7 @@ public static void main(String[] args) throws Exception { sdm.getNotifier(), o.getSolver()); ProverWithTracker prover = new ProverWithTracker(ctx, - o.getDumpSmtLib() ? + o.getDumpSmtLib() ? System.getenv("DAT3M_OUTPUT") + String.format("/%s.smt2", p.getName()) : "", ProverOptions.GENERATE_MODELS)) { ModelChecker modelChecker; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index d30496a3a5..1dba0afb64 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -18,10 +18,10 @@ import com.google.common.collect.ImmutableMap; public class ProverWithTracker implements AutoCloseable { - + private final FormulaManager fmgr; private final ProverEnvironment prover; - private final String fileName; + private final String fileName; public ProverWithTracker(SolverContext ctx, String fileName, ProverOptions... options) { this.fmgr = ctx.getFormulaManager(); @@ -30,6 +30,11 @@ public ProverWithTracker(SolverContext ctx, String fileName, ProverOptions... op init(); } + // An empty filename means there is no need to dump the encoding + private boolean dump() { + return !fileName.isEmpty(); + } + private void init() { try { Files.deleteIfExists(Paths.get(fileName)); @@ -45,8 +50,14 @@ public void close() throws Exception { prover.close(); } + // Each call to fmgr.dumpFormula(f) defines all variables used in f. + // We might end up with several definitions of the declarations. + // This might not be the most performant implementation, but duming the + // smtlib2 file is intended only for debugging or trying to understand + // how to optimize the encoding, thus performance is not an issue. private void removeDuplicatedDeclarations(String fileName) { try { + BufferedReader reader = new BufferedReader(new FileReader(fileName)); List newLines = new ArrayList<>(); String line; @@ -64,20 +75,21 @@ private void removeDuplicatedDeclarations(String fileName) { writer.newLine(); } writer.close(); + } catch (IOException e) { e.printStackTrace(); } } public void addConstraint(BooleanFormula f) throws InterruptedException { - if(!fileName.isEmpty()) { + if(dump()) { write(fmgr.dumpFormula(f).toString()); } prover.addConstraint(f); } public boolean isUnsatWithAssumptions(Collection fs) throws SolverException, InterruptedException { - if(!fileName.isEmpty()) { + if(dump()) { write("(push)\n"); for(BooleanFormula f : fs) { write(fmgr.dumpFormula(f).toString()); @@ -89,7 +101,7 @@ public boolean isUnsatWithAssumptions(Collection fs) throws Solv } public boolean isUnsat() throws SolverException, InterruptedException { - if(!fileName.isEmpty()) { + if(dump()) { write("(check-sat)\n"); } return prover.isUnsat(); @@ -104,14 +116,14 @@ public Model getModel() throws SolverException { } public void push() throws InterruptedException { - if(!fileName.isEmpty()) { + if(dump()) { write("(push)\n"); } prover.push(); } public void pop() { - if(!fileName.isEmpty()) { + if(dump()) { write("(pop)\n"); } prover.pop(); From a9e5524169f1e402e30aacba8a76af409e755fc3 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Thu, 29 Aug 2024 10:05:57 +0200 Subject: [PATCH 04/31] Remove duplicates in every call to write --- .../dartagnan/encoding/ProverWithTracker.java | 51 +++++++------------ 1 file changed, 18 insertions(+), 33 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index 1dba0afb64..a6950fe5db 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -11,7 +11,10 @@ import java.nio.file.Paths; import java.util.ArrayList; import java.util.Collection; +import java.util.HashSet; import java.util.List; +import java.util.Set; + import org.sosy_lab.java_smt.api.*; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; @@ -21,12 +24,14 @@ public class ProverWithTracker implements AutoCloseable { private final FormulaManager fmgr; private final ProverEnvironment prover; - private final String fileName; + private final String fileName; + private final Set 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(); } @@ -50,37 +55,6 @@ public void close() throws Exception { prover.close(); } - // Each call to fmgr.dumpFormula(f) defines all variables used in f. - // We might end up with several definitions of the declarations. - // This might not be the most performant implementation, but duming the - // smtlib2 file is intended only for debugging or trying to understand - // how to optimize the encoding, thus performance is not an issue. - private void removeDuplicatedDeclarations(String fileName) { - try { - - BufferedReader reader = new BufferedReader(new FileReader(fileName)); - List newLines = new ArrayList<>(); - String line; - while ((line = reader.readLine()) != null) { - // We only skip repeated declarations - if (!line.contains("declare-fun") || !newLines.contains(line)) { - newLines.add(line); - } - } - reader.close(); - - BufferedWriter writer = new BufferedWriter(new FileWriter(fileName)); - for (String newLine : newLines) { - writer.write(newLine); - writer.newLine(); - } - writer.close(); - - } catch (IOException e) { - e.printStackTrace(); - } - } - public void addConstraint(BooleanFormula f) throws InterruptedException { if(dump()) { write(fmgr.dumpFormula(f).toString()); @@ -135,10 +109,21 @@ private void write(String content) { try { writer = new FileWriter(file, true); PrintWriter printer = new PrintWriter(writer); - printer.append(content); + printer.append(removeDuplicatedDeclarations(content)); printer.close(); } catch (IOException e) { e.printStackTrace(); } } + + private String removeDuplicatedDeclarations(String content) { + String output = ""; + for(String line : content.split("\n")) { + if(line.contains("declare-fun") && !declarations.add(line)) { + continue; + } + output += line + "\n"; + } + return output; + } } From 589ad2e87a74d183e8457db32f3b0ea73174bc03 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Thu, 29 Aug 2024 10:49:25 +0200 Subject: [PATCH 05/31] Remove unused imports --- .../java/com/dat3m/dartagnan/encoding/ProverWithTracker.java | 5 ----- 1 file changed, 5 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index a6950fe5db..a5eb2832f5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -1,18 +1,13 @@ package com.dat3m.dartagnan.encoding; -import java.io.BufferedReader; -import java.io.BufferedWriter; import java.io.File; -import java.io.FileReader; import java.io.FileWriter; import java.io.IOException; import java.io.PrintWriter; import java.nio.file.Files; import java.nio.file.Paths; -import java.util.ArrayList; import java.util.Collection; import java.util.HashSet; -import java.util.List; import java.util.Set; import org.sosy_lab.java_smt.api.*; From 8aac80b5356d296ee6cdfe98c52252eff48a9c73 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 3 Sep 2024 19:28:30 +0200 Subject: [PATCH 06/31] Use StringBuilder --- .../com/dat3m/dartagnan/encoding/ProverWithTracker.java | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index a5eb2832f5..4ff6a2e0e8 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -111,14 +111,14 @@ private void write(String content) { } } - private String removeDuplicatedDeclarations(String content) { - String output = ""; + private StringBuilder removeDuplicatedDeclarations(String content) { + StringBuilder builder = new StringBuilder(); for(String line : content.split("\n")) { if(line.contains("declare-fun") && !declarations.add(line)) { continue; } - output += line + "\n"; + builder.append(line + "\n"); } - return output; + return builder; } } From 381530cba78e8361586544d3ecfe72281f843ae7 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 3 Sep 2024 20:01:13 +0200 Subject: [PATCH 07/31] Add some entries for SMT-COMP --- .../dartagnan/encoding/ProverWithTracker.java | 29 +++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index 4ff6a2e0e8..c55cc5d3e1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -6,6 +6,8 @@ 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.Set; @@ -36,9 +38,25 @@ private boolean dump() { } private void init() { + 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)" + ); try { Files.deleteIfExists(Paths.get(fileName)); + 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"); } catch (IOException e) { e.printStackTrace(); } @@ -47,6 +65,7 @@ private void init() { @Override public void close() throws Exception { removeDuplicatedDeclarations(fileName); + write("(exit)\n"); prover.close(); } @@ -58,22 +77,28 @@ public void addConstraint(BooleanFormula f) throws InterruptedException { } public boolean isUnsatWithAssumptions(Collection fs) throws SolverException, InterruptedException { + boolean result = prover.isUnsatWithAssumptions(fs); + String resultString = result ? "unsat" : "sat"; if(dump()) { write("(push)\n"); for(BooleanFormula f : fs) { write(fmgr.dumpFormula(f).toString()); } + write("(set-info :status " + resultString + ")\n"); write("(check-sat)\n"); write("(pop)\n"); } - return prover.isUnsatWithAssumptions(fs); + return result; } public boolean isUnsat() throws SolverException, InterruptedException { + boolean result = prover.isUnsat(); + String resultString = result ? "unsat" : "sat"; if(dump()) { + write("(set-info :status " + resultString + ")\n"); write("(check-sat)\n"); } - return prover.isUnsat(); + return result; } public ImmutableMap getStatistics() { From 3591c79d3912e5e567709c3caa9f2b072d070a20 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 3 Sep 2024 20:37:05 +0200 Subject: [PATCH 08/31] Add mome entries for SMT-COMP --- .../java/com/dat3m/dartagnan/encoding/ProverWithTracker.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index c55cc5d3e1..505f0b339c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -55,8 +55,9 @@ private void init() { Files.deleteIfExists(Paths.get(fileName)); write("(set-info :smt-lib-version 2.6)\n"); write("(set-logic ALL)\n"); - write("(set-info :category industrial)\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"); } catch (IOException e) { e.printStackTrace(); } From 02915db3e9f0a831a70bc682a025e633f3a06339 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 3 Sep 2024 20:56:58 +0200 Subject: [PATCH 09/31] Add comments to the formula for debugging --- .../com/dat3m/dartagnan/encoding/ProverWithTracker.java | 8 +++++++- .../dartagnan/verification/solving/AssumeSolver.java | 6 ++++++ .../dartagnan/verification/solving/DataRaceSolver.java | 6 +++++- .../dartagnan/verification/solving/RefinementSolver.java | 7 +++++++ 4 files changed, 25 insertions(+), 2 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index 505f0b339c..bbcd533914 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -78,7 +78,9 @@ public void addConstraint(BooleanFormula f) throws InterruptedException { } public boolean isUnsatWithAssumptions(Collection fs) throws SolverException, InterruptedException { + long start = System.currentTimeMillis(); boolean result = prover.isUnsatWithAssumptions(fs); + long end = System.currentTimeMillis(); String resultString = result ? "unsat" : "sat"; if(dump()) { write("(push)\n"); @@ -87,17 +89,21 @@ public boolean isUnsatWithAssumptions(Collection fs) throws Solv } write("(set-info :status " + resultString + ")\n"); write("(check-sat)\n"); + write("; Original solving time: " + (end - start) + " ms"); write("(pop)\n"); } return result; } public boolean isUnsat() throws SolverException, InterruptedException { + long start = System.currentTimeMillis(); boolean result = prover.isUnsat(); + long end = System.currentTimeMillis(); String resultString = result ? "unsat" : "sat"; if(dump()) { write("(set-info :status " + resultString + ")\n"); write("(check-sat)\n"); + write("; Original solving time: " + (end - start) + " ms"); } return result; } @@ -124,7 +130,7 @@ public void pop() { prover.pop(); } - private void write(String content) { + public void write(String content) { File file = new File(fileName); FileWriter writer; try { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java index 38b18925ec..1be7c04431 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java @@ -55,21 +55,27 @@ private void run() throws InterruptedException, SolverException, InvalidConfigur SymmetryEncoder symmetryEncoder = SymmetryEncoder.withContext(context); logger.info("Starting encoding using " + ctx.getVersion()); + prover.write("; Program encoding"); prover.addConstraint(programEncoder.encodeFullProgram()); + prover.write("; Memory model encoding"); prover.addConstraint(wmmEncoder.encodeFullMemoryModel()); // For validation this contains information. // For verification graph.encode() just returns ctx.mkTrue() + prover.write("; Witness encoding"); prover.addConstraint(task.getWitness().encode(context)); + prover.write("; 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.write("; Property encoding"); prover.addConstraint(assumedSpec); logger.info("Starting first solver.check()"); if(prover.isUnsatWithAssumptions(singletonList(assumptionLiteral))) { + prover.write("; Bound encoding"); prover.addConstraint(propertyEncoder.encodeBoundEventExec()); logger.info("Starting second solver.check()"); res = prover.isUnsat()? PASS : Result.UNKNOWN; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java index c0d9b136ca..f65ee724a2 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java @@ -59,16 +59,20 @@ private void run() throws InterruptedException, SolverException, InvalidConfigur SymmetryEncoder symmetryEncoder = SymmetryEncoder.withContext(context); logger.info("Starting encoding using " + ctx.getVersion()); + prover.write("; Program encoding"); prover.addConstraint(programEncoder.encodeFullProgram()); + prover.write("; Memory model encoding"); prover.addConstraint(wmmEncoder.encodeFullMemoryModel()); + prover.write("; Symmetry breaking encoding"); prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking()); prover.push(); - + prover.write("; Property encoding"); prover.addConstraint(propertyEncoder.encodeProperties(EnumSet.of(Property.DATARACEFREEDOM))); logger.info("Starting first solver.check()"); if(prover.isUnsat()) { prover.pop(); + prover.write("; Bound encoding"); prover.addConstraint(propertyEncoder.encodeBoundEventExec()); logger.info("Starting second solver.check()"); res = prover.isUnsat() ? PASS : UNKNOWN; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java index 2be1835018..5e3cfa192d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java @@ -224,8 +224,11 @@ private void runInternal(SolverContext ctx, ProverWithTracker prover, Verificati final Property.Type propertyType = Property.getCombinedType(task.getProperty(), task); logger.info("Starting encoding using " + ctx.getVersion()); + prover.write("; Program encoding"); prover.addConstraint(programEncoder.encodeFullProgram()); + prover.write("; Memory model (baseline) encoding"); prover.addConstraint(baselineEncoder.encodeFullMemoryModel()); + prover.write("; Symmetry breaking encoding"); prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking()); // ------------------------ Solving ------------------------ @@ -233,6 +236,7 @@ private void runInternal(SolverContext ctx, ProverWithTracker prover, Verificati logger.info("Checking target property."); prover.push(); + prover.write("; 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, ProverWithTracker prover, Verificati logger.info("Checking unrolling bounds."); final long lastTime = System.currentTimeMillis(); prover.pop(); + prover.write("; Bound encoding"); prover.addConstraint(propertyEncoder.encodeBoundEventExec()); // Add back the refinement clauses we already found, hoping that this improves the performance. + prover.write("; Refinement encoding"); prover.addConstraint(bmgr.and(propertyTrace.getRefinementFormulas())); final RefinementTrace boundTrace = runRefinement(task, prover, solver, refiner); boundCheckTime = System.currentTimeMillis() - lastTime; @@ -455,6 +461,7 @@ private RefinementIteration doRefinementIteration(ProverWithTracker prover, WMMS inconsistencyReasons = solverResult.getCoreReasons(); lastTime = System.currentTimeMillis(); refinementFormula = refiner.refine(inconsistencyReasons, context); + prover.write("; Refinement encoding"); prover.addConstraint(refinementFormula); refineTime = (System.currentTimeMillis() - lastTime); } From 6326445a3923987549c4299678a6fc5cc3d4c9a8 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Tue, 3 Sep 2024 21:12:46 +0200 Subject: [PATCH 10/31] Improved liveness detection for store exclusives (#722) --- .../dartagnan/encoding/PropertyEncoder.java | 163 +++++++++++------- .../dat3m/dartagnan/program/event/Tag.java | 8 +- .../processing/DynamicSpinLoopDetection.java | 19 +- .../program/processing/Inlining.java | 2 +- .../program/processing/Intrinsics.java | 2 +- .../program/processing/LoopUnrolling.java | 2 +- 6 files changed, 125 insertions(+), 71 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java index fa7ed2b267..36427a5adf 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java @@ -21,7 +21,6 @@ import com.dat3m.dartagnan.wmm.utils.EventGraph; import com.google.common.base.Preconditions; import com.google.common.collect.Lists; -import com.google.common.collect.Maps; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.sosy_lab.common.configuration.InvalidConfigurationException; @@ -36,8 +35,8 @@ import java.util.stream.Collectors; import static com.dat3m.dartagnan.configuration.Property.*; -import static com.dat3m.dartagnan.wmm.RelationNameRepository.CO; import static com.dat3m.dartagnan.program.Program.SourceLanguage.LLVM; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.CO; public class PropertyEncoder implements Encoder { @@ -66,7 +65,7 @@ public class PropertyEncoder implements Encoder { Since we encode a lot of potential violations, and we want to trace back which one lead to our query being SAT, we use trackable formulas. */ - private static class TrackableFormula { + public static class TrackableFormula { private final BooleanFormula trackingLiteral; private final BooleanFormula trackedFormula; @@ -304,7 +303,7 @@ public List encodeCATSpecificationViolations() { final EncodingContext ctx = this.context; final Wmm memoryModel = this.memoryModel; final List flaggedAxioms = memoryModel.getAxioms().stream() - .filter(Axiom::isFlagged).collect(Collectors.toList()); + .filter(Axiom::isFlagged).toList(); if (flaggedAxioms.isEmpty()) { logger.info("No CAT specification in the WMM. Skipping encoding."); @@ -402,22 +401,30 @@ public TrackableFormula encodeDataRaces() { private TrackableFormula encodeDeadlocks() { logger.info("Encoding dead locks"); - return new LivenessEncoder().encodeDeadlocks(); + return new LivenessEncoder().encodeLivenessBugs(); } /* Encoder for the liveness property. We have a liveness violation in some execution if - - At least one thread is stuck inside a loop (*) + - At least one thread is stuck (*) - All other threads are either stuck or terminated normally (**) - (*) A thread is stuck if it finishes a loop iteration - - without causing side-effects (e.g., visible stores) - - while reading only from co-maximal stores - => Without external help, a stuck thread will never be able to exit the loop. + (*) A thread is stuck if + (1) it performs a loop iteration without causing side-effects (e.g., visible stores) + while satisfying fairness conditions + => Without external help, a stuck thread will never be able to exit the loop. + OR (2) the thread is blocked by a control barrier. + + Fairness conditions for loops: + - Memory fairness: the loop iteration reads only co-maximal values + - Excl-Store progress: all exclusive stores in the iteration succeed (infinite spurious failures are unfair) + NOTE: Here we assume strong progress. Under weak fairness, a loop with two exclusive stores that need + to succeed in the same iteration could fail liveness if they succeed in alternation. - (**) A thread terminates normally IFF it does not terminate early (denoted by EARLYTERMINATION-tagged jumps) + (**) A thread terminates normally IFF it does terminate (no NONTERMINATION-tagged jumps) non-exceptionally + (no EXCEPTIONAL_TERMINATION-tagged jumps) due to e.g., - violating an assertion - reaching the loop unrolling bound @@ -429,36 +436,19 @@ in a deadlock without satisfying the stated conditions (e.g., while producing si */ private class LivenessEncoder { - private static class SpinIteration { - public final List containedLoads = new ArrayList<>(); - // Execution of the means the loop performed a side-effect-free - // iteration without exiting. If such a jump is executed + all loads inside the loop - // were co-maximal, then we have a deadlock condition. - public final List spinningJumps = new ArrayList<>(); - } - - public TrackableFormula encodeDeadlocks() { + public TrackableFormula encodeLivenessBugs() { final Program program = PropertyEncoder.this.program; final EncodingContext context = PropertyEncoder.this.context; final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); - final LoopAnalysis loopAnalysis = LoopAnalysis.newInstance(program); - - // Find spin loops of all threads - final Map> spinloopsMap = - Maps.toMap(program.getThreads(), t -> this.findSpinLoopsInThread(t, loopAnalysis)); - // Compute "stuckness" encoding for all threads - final Map isStuckMap = Maps.toMap(program.getThreads(), t -> - bmgr.or(generateBarrierStucknessEncoding(t, context), - this.generateSpinloopStucknessEncoding(spinloopsMap.get(t), context))); // Deadlock <=> allStuckOrDone /\ atLeastOneStuck BooleanFormula allStuckOrDone = bmgr.makeTrue(); BooleanFormula atLeastOneStuck = bmgr.makeFalse(); for (Thread thread : program.getThreads()) { - final BooleanFormula isStuck = isStuckMap.get(thread); + final BooleanFormula isStuck = isStuckEncoding(thread, context); final BooleanFormula isTerminatingNormally = thread .getEvents().stream() - .filter(e -> e.hasTag(Tag.EARLYTERMINATION)) + .filter(e -> e.hasTag(Tag.EXCEPTIONAL_TERMINATION) || e.hasTag(Tag.NONTERMINATION)) .map(CondJump.class::cast) .map(j -> bmgr.not(bmgr.and(context.execution(j), context.jumpCondition(j)))) .reduce(bmgr.makeTrue(), bmgr::and); @@ -471,6 +461,16 @@ public TrackableFormula encodeDeadlocks() { return new TrackableFormula(bmgr.not(LIVENESS.getSMTVariable(context)), hasDeadlock); } + private BooleanFormula isStuckEncoding(Thread thread, EncodingContext context) { + return context.getBooleanFormulaManager().or( + generateSpinloopStucknessEncoding(thread, context), + generateBarrierStucknessEncoding(thread, context) + ); + } + + // ------------------------------------------------------------------------------ + // Liveness issue due to blocked execution (due to ControlBarrier) + private BooleanFormula generateBarrierStucknessEncoding(Thread thread, EncodingContext context) { final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); return bmgr.or(thread.getEvents().stream() @@ -479,37 +479,85 @@ private BooleanFormula generateBarrierStucknessEncoding(Thread thread, EncodingC .toList()); } - // Compute "stuckness": A thread is stuck if it reaches a spin loop bound event - // while only reading from co-maximal stores. - private BooleanFormula generateSpinloopStucknessEncoding(List loops, EncodingContext context) { + // ------------------------------------------------------------------------------ + // Liveness issue due to non-terminating loops (~ deadlocks) + + private record SpinIteration(List body, List spinningJumps) { + // Execution of the means the loop performed a side-effect-free + // iteration without exiting. If such a jump is executed + all loads inside the loop + // were co-maximal, then we have a deadlock condition. + } + + private BooleanFormula generateSpinloopStucknessEncoding(Thread thread, EncodingContext context) { + final LoopAnalysis loopAnalysis = LoopAnalysis.onFunction(thread); + final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); + + return this.findSpinLoopsInThread(thread, loopAnalysis).stream() + .map(loop -> generateSpinloopStucknessEncoding(loop, context)) + .reduce(bmgr.makeFalse(), bmgr::or); + } + + private BooleanFormula generateSpinloopStucknessEncoding(SpinIteration loop, EncodingContext context) { + return context.getBooleanFormulaManager().and( + isSideEffectFreeEncoding(loop, context), + fairnessEncoding(loop, context) + ); + } + + private BooleanFormula isSideEffectFreeEncoding(SpinIteration loop, EncodingContext context) { + // Note that we assume (for now) that a SPINLOOP-tagged jump is executed only if the loop iteration + // was side-effect free. + final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); + final BooleanFormula isSideEffectFree = loop.spinningJumps.stream() + .map(j -> bmgr.and(context.execution(j), context.jumpCondition(j))) + .reduce(bmgr.makeFalse(), bmgr::or); + return isSideEffectFree; + } + + private BooleanFormula fairnessEncoding(SpinIteration loop, EncodingContext context) { + return context.getBooleanFormulaManager().and( + memoryFairnessEncoding(loop, context), + exclStoreFairnessEncoding(loop, context) + ); + } + + private BooleanFormula memoryFairnessEncoding(SpinIteration loop, EncodingContext context) { final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); final RelationAnalysis ra = PropertyEncoder.this.ra; final Relation rf = memoryModel.getRelation(RelationNameRepository.RF); final EncodingContext.EdgeEncoder rfEncoder = context.edge(rf); final Map> rfMayIn = ra.getKnowledge(rf).getMaySet().getInMap(); - if (loops.isEmpty()) { - return bmgr.makeFalse(); - } + final List loads = loop.body.stream() + .filter(Load.class::isInstance) + .map(Load.class::cast) + .toList(); - BooleanFormula isStuck = bmgr.makeFalse(); - for (SpinIteration loop : loops) { - BooleanFormula allLoadsAreCoMaximal = bmgr.makeTrue(); - for (Load load : loop.containedLoads) { - final BooleanFormula readsCoMaximalStore = rfMayIn.getOrDefault(load, Set.of()).stream() - .map(store -> bmgr.and(rfEncoder.encode(store, load), lastCoVar(store))) - .reduce(bmgr.makeFalse(), bmgr::or); - final BooleanFormula isCoMaximalLoad = bmgr.implication(context.execution(load), readsCoMaximalStore); - allLoadsAreCoMaximal = bmgr.and(allLoadsAreCoMaximal, isCoMaximalLoad); - } - // Note that we assume (for now) that a SPINLOOP-tagged jump is executed only if the loop iteration - // was side-effect free. - final BooleanFormula isSideEffectFree = loop.spinningJumps.stream() - .map(j -> bmgr.and(context.execution(j), context.jumpCondition(j))) + BooleanFormula allLoadsAreCoMaximal = bmgr.makeTrue(); + for (Load load : loads) { + final BooleanFormula readsCoMaximalStore = rfMayIn.getOrDefault(load, Set.of()).stream() + .map(store -> bmgr.and(rfEncoder.encode(store, load), lastCoVar(store))) .reduce(bmgr.makeFalse(), bmgr::or); - isStuck = bmgr.or(isStuck, bmgr.and(isSideEffectFree, allLoadsAreCoMaximal)); + final BooleanFormula isCoMaximalLoad = bmgr.implication(context.execution(load), readsCoMaximalStore); + allLoadsAreCoMaximal = bmgr.and(allLoadsAreCoMaximal, isCoMaximalLoad); + } + + return allLoadsAreCoMaximal; + } + + private BooleanFormula exclStoreFairnessEncoding(SpinIteration loop, EncodingContext context) { + final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); + final List exclStores = loop.body.stream() + .filter(RMWStoreExclusive.class::isInstance) + .map(RMWStoreExclusive.class::cast) + .toList(); + BooleanFormula allExclStoresExecuted = bmgr.makeTrue(); + for (RMWStoreExclusive exclStore : exclStores) { + final BooleanFormula executedIfPossible = bmgr.implication(context.controlFlow(exclStore), context.execution(exclStore)); + allExclStoresExecuted = bmgr.and(allExclStoresExecuted, executedIfPossible); } - return isStuck; + + return allExclStoresExecuted; } private List findSpinLoopsInThread(Thread thread, LoopAnalysis loopAnalysis) { @@ -525,14 +573,7 @@ private List findSpinLoopsInThread(Thread thread, LoopAnalysis lo .toList(); if (!spinningJumps.isEmpty()) { - final List loads = iterBody.stream() - .filter(Load.class::isInstance) - .map(Load.class::cast) - .toList(); - - final SpinIteration spinIter = new SpinIteration(); - spinIter.spinningJumps.addAll(spinningJumps); - spinIter.containedLoads.addAll(loads); + final SpinIteration spinIter = new SpinIteration(iterBody, spinningJumps); spinIterations.add(spinIter); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java index b4cb282558..03cacda223 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java @@ -27,9 +27,11 @@ private Tag() { } public static final String EXCL = "__EXCL"; // Marks the event that is reachable IFF a loop has not been fully unrolled. public static final String BOUND = "__BOUND"; - // Marks jumps that somehow terminate a thread earlier than "normally" - // This can be bound events, spinning events, assertion violations, etc. - public static final String EARLYTERMINATION = "__EARLYTERMINATION"; + // Marks jumps that designate an exceptional termination, typically due to assertion failures + public static final String EXCEPTIONAL_TERMINATION = "__EXCEPTIONAL_TERMINATION"; + // Marks jumps that designate non-termination, typically spinloops and bound events + // (and control barriers in the future) + public static final String NONTERMINATION = "__NONTERMINATION"; // Marks jumps that terminate a thread due to spinning behaviour, i.e. side-effect-free loop iterations public static final String SPINLOOP = "__SPINLOOP"; // Some events should not be optimized (e.g. fake dependencies) or deleted (e.g. bounds) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java index 1c65201ce4..1a002d6b52 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java @@ -132,6 +132,7 @@ private void reduceToDominatingSideEffects(LoopData loop) { final List sideEffects = loop.sideEffects; final Event start = loop.getStart(); final Event end = loop.getEnd(); + final Predicate isAlwaysSideEffectful = (e -> e.cfImpliesExec() && sideEffects.contains(e)); final DominatorTree preDominatorTree = DominatorAnalysis.computePreDominatorTree(start, end); final DominatorTree postDominatorTree = DominatorAnalysis.computePostDominatorTree(start, end); @@ -144,7 +145,7 @@ private void reduceToDominatingSideEffects(LoopData loop) { // (2) Check if always side-effect-full at the end of an iteration directly before entering the next one. // This is an approximation: If the end of the iteration is predominated by some side effect // then we always observe side effects. - loop.isAlwaysSideEffectful = Streams.stream(preDominatorTree.getDominators(end)).anyMatch(sideEffects::contains); + loop.isAlwaysSideEffectful = Streams.stream(preDominatorTree.getDominators(end)).anyMatch(isAlwaysSideEffectful); if (loop.isAlwaysSideEffectful) { return; } @@ -157,7 +158,7 @@ private void reduceToDominatingSideEffects(LoopData loop) { preDominatorTree.getStrictDominators(sideEffect), postDominatorTree.getStrictDominators(sideEffect) ); - final boolean isDominated = Iterables.tryFind(dominators, sideEffects::contains).isPresent(); + final boolean isDominated = Iterables.tryFind(dominators, isAlwaysSideEffectful::test).isPresent(); if (isDominated) { sideEffects.remove(i); } @@ -173,12 +174,22 @@ private void instrumentLoop(LoopData loop) { final ExpressionFactory expressions = ExpressionFactory.getInstance(); final Function func = loop.loopInfo.function(); final int loopNum = loop.loopInfo.loopNumber(); + final Register tempReg = func.newRegister("__possiblySideEffectless#" + loopNum, types.getBooleanType()); final Register trackingReg = func.newRegister("__sideEffect#" + loopNum, types.getBooleanType()); final Event init = EventFactory.newLocal(trackingReg, expressions.makeFalse()); loop.getStart().insertAfter(init); for (Event sideEffect : loop.sideEffects) { - final Event updateSideEffect = EventFactory.newLocal(trackingReg, expressions.makeTrue()); + final List updateSideEffect = new ArrayList<>(); + if (sideEffect.cfImpliesExec()) { + updateSideEffect.add(EventFactory.newLocal(trackingReg, expressions.makeTrue())); + } else { + updateSideEffect.addAll(List.of( + EventFactory.newExecutionStatus(tempReg, sideEffect), + EventFactory.newLocal(trackingReg, expressions.makeOr(trackingReg, expressions.makeNot(tempReg))) + )); + + } sideEffect.getPredecessor().insertAfter(updateSideEffect); } @@ -197,7 +208,7 @@ private Event newSpinTerminator(Expression guard, Function func) { final Event terminator = func instanceof Thread thread ? EventFactory.newJump(guard, (Label) thread.getExit()) : EventFactory.newAbortIf(guard); - terminator.addTags(Tag.SPINLOOP, Tag.EARLYTERMINATION, Tag.NOOPT); + terminator.addTags(Tag.SPINLOOP, Tag.NONTERMINATION, Tag.NOOPT); return terminator; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java index 38b2e1814f..a755d09f1e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java @@ -88,7 +88,7 @@ private void inlineAllCalls(Function function, Map snapshots if (depth > bound) { final AbortIf boundEvent = newAbortIf(ExpressionFactory.getInstance().makeTrue()); boundEvent.copyAllMetadataFrom(call); - boundEvent.addTags(Tag.BOUND, Tag.EARLYTERMINATION, Tag.NOOPT); + boundEvent.addTags(Tag.BOUND, Tag.NONTERMINATION, Tag.NOOPT); call.replaceBy(boundEvent); event = boundEvent; } else { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java index db2871e546..b81f2a43e5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java @@ -901,7 +901,7 @@ private List inlineAssert(FunctionCall call, AssertionType skip, String e final Expression condition = expressions.makeFalse(); final Event assertion = EventFactory.newAssert(condition, errorMsg); final Event abort = EventFactory.newAbortIf(expressions.makeTrue()); - abort.addTags(Tag.EARLYTERMINATION); + abort.addTags(Tag.EXCEPTIONAL_TERMINATION); return List.of(assertion, abort); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java index 7b6bca60a9..293f15f489 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java @@ -191,7 +191,7 @@ private Event newBoundEvent(Function func) { final Event boundEvent = func instanceof Thread thread ? EventFactory.newGoto((Label) thread.getExit()) : EventFactory.newAbortIf(ExpressionFactory.getInstance().makeTrue()); - boundEvent.addTags(Tag.BOUND, Tag.EARLYTERMINATION, Tag.NOOPT); + boundEvent.addTags(Tag.BOUND, Tag.NONTERMINATION, Tag.NOOPT); return boundEvent; } From 5e10cda3235bf920317d5764fc247645ae0ce3d5 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Tue, 3 Sep 2024 22:28:12 +0200 Subject: [PATCH 11/31] Renamed Location to FinalMemoryValue. (#725) --- .../dartagnan/encoding/ExpressionEncoder.java | 10 +++---- .../dartagnan/expression/Expression.java | 8 ++--- .../dartagnan/expression/ExpressionKind.java | 1 + .../expression/ExpressionVisitor.java | 4 +-- .../visitors/VisitorLitmusAssertions.java | 4 +-- .../visitors/spirv/VisitorSpirvOutput.java | 30 ++++++++----------- .../{Location.java => FinalMemoryValue.java} | 25 +++++++--------- .../processing/RemoveUnusedMemory.java | 8 ++--- 8 files changed, 41 insertions(+), 49 deletions(-) rename dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/{Location.java => FinalMemoryValue.java} (59%) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java index f82fdea03b..914fb9c383 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java @@ -11,7 +11,7 @@ import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.Event; -import com.dat3m.dartagnan.program.memory.Location; +import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.program.misc.NonDetValue; import org.sosy_lab.java_smt.api.*; @@ -298,9 +298,9 @@ public Formula visitMemoryObject(MemoryObject memObj) { } @Override - public Formula visitLocation(Location location) { - checkState(event == null, "Cannot evaluate %s at event %s.", location, event); - int size = types.getMemorySizeInBits(location.getType()); - return context.lastValue(location.getMemoryObject(), location.getOffset(), size); + public Formula visitFinalMemoryValue(FinalMemoryValue val) { + checkState(event == null, "Cannot evaluate final memory value of %s at event %s.", val, event); + int size = types.getMemorySizeInBits(val.getType()); + return context.lastValue(val.getMemoryObject(), val.getOffset(), size); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/Expression.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/Expression.java index afc86451c1..a2891b877c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/Expression.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/Expression.java @@ -2,7 +2,7 @@ import com.dat3m.dartagnan.expression.processing.ExpressionInspector; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.memory.Location; +import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.google.common.collect.ImmutableSet; @@ -40,9 +40,9 @@ public MemoryObject visitMemoryObject(MemoryObject memObj) { } @Override - public Expression visitLocation(Location location) { - objects.add(location.getMemoryObject()); - return location; + public Expression visitFinalMemoryValue(FinalMemoryValue val) { + objects.add(val.getMemoryObject()); + return val; } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionKind.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionKind.java index 57e26ad293..9abbc42896 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionKind.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionKind.java @@ -16,6 +16,7 @@ enum Other implements ExpressionKind { NONDET, FUNCTION_ADDR, MEMORY_ADDR, + FINAL_MEM_VAL, REGISTER, GEP, CONSTRUCT, diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionVisitor.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionVisitor.java index b72021dd0a..1e4640b963 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionVisitor.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionVisitor.java @@ -11,7 +11,7 @@ import com.dat3m.dartagnan.expression.misc.ITEExpr; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.memory.Location; +import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.program.misc.NonDetValue; @@ -59,7 +59,7 @@ public interface ExpressionVisitor { default TRet visitRegister(Register reg) { return visitLeafExpression(reg); } default TRet visitFunction(Function function) { return visitLeafExpression(function); } default TRet visitMemoryObject(MemoryObject memObj) { return visitLeafExpression(memObj); } - default TRet visitLocation(Location loc) { return visitLeafExpression(loc); } + default TRet visitFinalMemoryValue(FinalMemoryValue val) { return visitLeafExpression(val); } default TRet visitNonDetValue(NonDetValue nonDet) { return visitLeafExpression(nonDet); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java index c8ce2ca1d4..5f720d48b9 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java @@ -8,7 +8,7 @@ import com.dat3m.dartagnan.parsers.LitmusAssertionsLexer; import com.dat3m.dartagnan.parsers.LitmusAssertionsParser; import com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder; -import com.dat3m.dartagnan.program.memory.Location; +import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.MemoryObject; import org.antlr.v4.runtime.CharStream; import org.antlr.v4.runtime.CharStreams; @@ -115,6 +115,6 @@ private Expression acceptAssertionValue(LitmusAssertionsParser.AssertionValueCon checkState(base != null, "uninitialized location %s", name); TerminalNode offset = ctx.DigitSequence(); int o = offset == null ? 0 : Integer.parseInt(offset.getText()); - return right && offset == null ? base : new Location(name, archType, base, o); + return right && offset == null ? base : new FinalMemoryValue(name, archType, base, o); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorSpirvOutput.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorSpirvOutput.java index 1fbf076f80..6185fc6933 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorSpirvOutput.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorSpirvOutput.java @@ -4,7 +4,6 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.expression.Type; -import com.dat3m.dartagnan.expression.base.LiteralExpressionBase; import com.dat3m.dartagnan.expression.integers.IntCmpOp; import com.dat3m.dartagnan.expression.integers.IntLiteral; import com.dat3m.dartagnan.expression.type.AggregateType; @@ -13,15 +12,13 @@ import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.parsers.SpirvBaseVisitor; import com.dat3m.dartagnan.parsers.SpirvParser; -import com.dat3m.dartagnan.parsers.program.visitors.spirv.helpers.HelperTypes; import com.dat3m.dartagnan.parsers.program.visitors.spirv.builders.ProgramBuilder; +import com.dat3m.dartagnan.parsers.program.visitors.spirv.helpers.HelperTypes; import com.dat3m.dartagnan.program.Program; -import com.dat3m.dartagnan.program.memory.Location; +import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.ScopedPointerVariable; -import java.util.HashMap; import java.util.List; -import java.util.Map; import static com.dat3m.dartagnan.expression.integers.IntCmpOp.*; import static com.dat3m.dartagnan.program.Program.SpecificationType.*; @@ -30,7 +27,6 @@ public class VisitorSpirvOutput extends SpirvBaseVisitor { private static final TypeFactory types = TypeFactory.getInstance(); private static final ExpressionFactory expressions = ExpressionFactory.getInstance(); - private final Map locationTypes = new HashMap<>(); private final ProgramBuilder builder; private Program.SpecificationType type; private Expression condition; @@ -48,7 +44,7 @@ public Expression visitSpvHeaders(SpirvParser.SpvHeadersContext ctx) { } if (type == null) { type = FORALL; - condition = ExpressionFactory.getInstance().makeTrue(); + condition = expressions.makeTrue(); } builder.setSpecification(type, condition); return null; @@ -103,7 +99,7 @@ public Expression visitAssertionValue(SpirvParser.AssertionValueContext ctx) { List indexes = ctx.indexValue().stream() .map(c -> Integer.parseInt(c.ModeHeader_PositiveInteger().getText())) .toList(); - return createLocation(base, indexes); + return createFinalMemoryValue(base, indexes); } throw new ParsingException("Uninitialized location %s", name); } @@ -114,9 +110,9 @@ private void appendAssertion(Program.SpecificationType newType, Expression expre condition = expression; } else if (newType.equals(type)) { if (type.equals(FORALL)) { - condition = ExpressionFactory.getInstance().makeAnd(condition, expression); + condition = expressions.makeAnd(condition, expression); } else if (type.equals(NOT_EXISTS)) { - condition = ExpressionFactory.getInstance().makeOr(condition, expression); + condition = expressions.makeOr(condition, expression); } else { throw new ParsingException("Multiline assertion is not supported for type " + newType); } @@ -126,15 +122,15 @@ private void appendAssertion(Program.SpecificationType newType, Expression expre } private Expression normalize(Expression target, Expression other) { - Type targetType = target instanceof Location ? locationTypes.get(target) : target.getType(); - Type otherType = other instanceof Location ? locationTypes.get(other) : other.getType(); + Type targetType = target.getType(); + Type otherType = other.getType(); if (targetType.equals(otherType)) { return target; } - if (target instanceof Location && other instanceof LiteralExpressionBase) { + if (target instanceof FinalMemoryValue && other.getKind() == Other.LITERAL) { return target; } - if (target instanceof IntLiteral iValue && other instanceof Location) { + if (target instanceof IntLiteral iValue && other instanceof FinalMemoryValue) { int size = types.getMemorySizeInBits(otherType); IntegerType newType = types.getIntegerType(size); return new IntLiteral(newType, iValue.getValue()); @@ -178,7 +174,7 @@ private IntCmpOp parseOperand(SpirvParser.AssertionCompareContext ctx) { throw new ParsingException("Unrecognised comparison operator"); } - private Location createLocation(ScopedPointerVariable base, List indexes) { + private FinalMemoryValue createFinalMemoryValue(ScopedPointerVariable base, List indexes) { String name = indexes.isEmpty() ? base.getId() : base.getId() + "[" + String.join("][", indexes.stream().map(Object::toString).toArray(String[]::new)) + "]"; Type elType = HelperTypes.getMemberType(base.getId(), base.getInnerType(), indexes); @@ -186,8 +182,6 @@ private Location createLocation(ScopedPointerVariable base, List indexe throw new ParsingException("Index is not deep enough for variable '%s'", name); } int offset = HelperTypes.getMemberOffset(base.getId(), 0, base.getInnerType(), indexes); - Location location = new Location(name, elType, base.getAddress(), offset); - locationTypes.put(location, elType); - return location; + return new FinalMemoryValue(name, elType, base.getAddress(), offset); } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Location.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/FinalMemoryValue.java similarity index 59% rename from dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Location.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/FinalMemoryValue.java index 094ecf5592..051152c72f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Location.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/FinalMemoryValue.java @@ -5,15 +5,17 @@ import com.dat3m.dartagnan.expression.Type; import com.dat3m.dartagnan.expression.base.LeafExpressionBase; -// TODO: Should be replaced with a Pointer class -public class Location extends LeafExpressionBase { +// TODO: Should work with an arbitrary pointer rather than "base + offset" +// Represents the final (co-maximal) value at a memory address as if read by a load instruction +// that observed the final store. +public class FinalMemoryValue extends LeafExpressionBase { private final String name; private final MemoryObject base; private final int offset; - public Location(String name, Type type, MemoryObject base, int offset) { - super(type); + public FinalMemoryValue(String name, Type loadType, MemoryObject base, int offset) { + super(loadType); this.name = name; this.base = base; this.offset = offset; @@ -33,12 +35,12 @@ public int getOffset() { @Override public ExpressionKind getKind() { - return ExpressionKind.Other.MEMORY_ADDR; + return ExpressionKind.Other.FINAL_MEM_VAL; } @Override public T accept(ExpressionVisitor visitor) { - return visitor.visitLocation(this); + return visitor.visitFinalMemoryValue(this); } @Override @@ -48,17 +50,12 @@ public String toString() { @Override public int hashCode() { - return base.hashCode() + offset; + return base.hashCode() + 31 * offset; } @Override public boolean equals(Object obj) { - if (this == obj) { - return true; - } else if (obj == null || getClass() != obj.getClass()) { - return false; - } - Location o = (Location) obj; - return base.equals(o.base) && offset == o.offset; + return (obj instanceof FinalMemoryValue o) && + base.equals(o.base) && offset == o.offset; } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java index 6feca6db62..0aeea91d3d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java @@ -4,7 +4,7 @@ import com.dat3m.dartagnan.expression.processing.ExpressionInspector; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.event.RegReader; -import com.dat3m.dartagnan.program.memory.Location; +import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.Memory; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.google.common.collect.Sets; @@ -52,9 +52,9 @@ public Expression visitMemoryObject(MemoryObject address) { } @Override - public Expression visitLocation(Location location) { - memoryObjects.add(location.getMemoryObject()); - return location; + public Expression visitFinalMemoryValue(FinalMemoryValue val) { + memoryObjects.add(val.getMemoryObject()); + return val; } } } From 0de6d15276097d921e851fe60617d5bd84311106 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 3 Sep 2024 23:29:20 +0200 Subject: [PATCH 12/31] Guard operations --- .../dartagnan/encoding/ProverWithTracker.java | 78 ++++++++++--------- 1 file changed, 41 insertions(+), 37 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index bbcd533914..0edebd38d5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -38,35 +38,39 @@ private boolean dump() { } private void init() { - 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)" - ); - try { - Files.deleteIfExists(Paths.get(fileName)); - 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"); - } catch (IOException e) { - e.printStackTrace(); + if(dump()) { + 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)" + ); + try { + Files.deleteIfExists(Paths.get(fileName)); + 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"); + } catch (IOException e) { + e.printStackTrace(); + } } } @Override public void close() throws Exception { - removeDuplicatedDeclarations(fileName); - write("(exit)\n"); + if(dump()) { + removeDuplicatedDeclarations(fileName); + write("(exit)\n"); + } prover.close(); } @@ -81,13 +85,12 @@ public boolean isUnsatWithAssumptions(Collection fs) throws Solv long start = System.currentTimeMillis(); boolean result = prover.isUnsatWithAssumptions(fs); long end = System.currentTimeMillis(); - String resultString = result ? "unsat" : "sat"; if(dump()) { write("(push)\n"); for(BooleanFormula f : fs) { write(fmgr.dumpFormula(f).toString()); } - write("(set-info :status " + resultString + ")\n"); + write("(set-info :status " + (result ? "unsat" : "sat") + ")\n"); write("(check-sat)\n"); write("; Original solving time: " + (end - start) + " ms"); write("(pop)\n"); @@ -99,9 +102,8 @@ public boolean isUnsat() throws SolverException, InterruptedException { long start = System.currentTimeMillis(); boolean result = prover.isUnsat(); long end = System.currentTimeMillis(); - String resultString = result ? "unsat" : "sat"; if(dump()) { - write("(set-info :status " + resultString + ")\n"); + write("(set-info :status " + (result ? "unsat" : "sat") + ")\n"); write("(check-sat)\n"); write("; Original solving time: " + (end - start) + " ms"); } @@ -131,15 +133,17 @@ public void pop() { } public void write(String content) { - File file = new File(fileName); - FileWriter writer; - try { - writer = new FileWriter(file, true); - PrintWriter printer = new PrintWriter(writer); - printer.append(removeDuplicatedDeclarations(content)); - printer.close(); - } catch (IOException e) { - e.printStackTrace(); + if(dump()) { + File file = new File(fileName); + FileWriter writer; + try { + writer = new FileWriter(file, true); + PrintWriter printer = new PrintWriter(writer); + printer.append(removeDuplicatedDeclarations(content)); + printer.close(); + } catch (IOException e) { + e.printStackTrace(); + } } } From f8d73ca44d10e3330f86811c8d7ebbc6b133f8b0 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Wed, 4 Sep 2024 09:42:52 +0200 Subject: [PATCH 13/31] Fix ui package --- ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 6f2f6e622b..890aa30d4b 100644 --- a/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java +++ b/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java @@ -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); From a1f543e9ae5a8c3ba5efe738e5c813818c2a04fb Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Thu, 5 Sep 2024 10:43:35 +0200 Subject: [PATCH 14/31] Feedback implemented --- .../java/com/dat3m/dartagnan/Dartagnan.java | 9 +- .../dartagnan/encoding/ProverWithTracker.java | 65 ++++++++---- .../verification/solving/AssumeSolver.java | 12 +-- .../verification/solving/DataRaceSolver.java | 100 +++++++++--------- .../verification/solving/ModelChecker.java | 4 +- .../solving/RefinementSolver.java | 14 +-- .../witness/graphml/WitnessBuilder.java | 8 +- .../compilation/AbstractCompilationTest.java | 1 - 8 files changed, 119 insertions(+), 94 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 3cb97bdef5..161486f7cd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -43,6 +43,7 @@ import org.sosy_lab.common.log.BasicLogManager; import org.sosy_lab.java_smt.SolverContextFactory; import org.sosy_lab.java_smt.api.Model; +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 org.sosy_lab.java_smt.api.SolverException; @@ -210,7 +211,7 @@ public static void main(String[] args) throws Exception { } } - public static File generateExecutionGraphFile(VerificationTask task, ProverWithTracker prover, ModelChecker modelChecker, + 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."); @@ -231,7 +232,7 @@ public static File generateExecutionGraphFile(VerificationTask task, ProverWithT synContext, witnessType.convertToPng()); } - private static void generateWitnessIfAble(VerificationTask task, ProverWithTracker prover, + private static void generateWitnessIfAble(VerificationTask task, ProverEnvironment prover, ModelChecker modelChecker, String summary) { // ------------------ Generate Witness, if possible ------------------ final EnumSet properties = task.getProperty(); @@ -250,7 +251,7 @@ private static void generateWitnessIfAble(VerificationTask task, ProverWithTrack } } - public static String generateResultSummary(VerificationTask task, ProverWithTracker prover, + public static String generateResultSummary(VerificationTask task, ProverEnvironment prover, ModelChecker modelChecker) throws SolverException { // ----------------- Generate output of verification result ----------------- final Program p = task.getProgram(); @@ -388,7 +389,7 @@ public static String generateResultSummary(VerificationTask task, ProverWithTrac return summary.toString(); } - private static void printWarningIfThreadStartFailed(Program p, EncodingContext encoder, ProverWithTracker prover) + private static void printWarningIfThreadStartFailed(Program p, EncodingContext encoder, ProverEnvironment prover) throws SolverException { for (Event e : p.getThreadEvents()) { if (e.hasTag(Tag.STARTLOAD) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index 0edebd38d5..d2d007d9f7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -10,6 +10,8 @@ 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.*; @@ -17,7 +19,7 @@ import com.google.common.collect.ImmutableMap; -public class ProverWithTracker implements AutoCloseable { +public class ProverWithTracker implements ProverEnvironment { private final FormulaManager fmgr; private final ProverEnvironment prover; @@ -39,6 +41,11 @@ private boolean dump() { 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"); @@ -52,21 +59,16 @@ private void init() { "- Thomas Haas, Roland Meyer, Hernán Ponce de León: " + "CAAT: consistency as a theory. Proc. ACM Program. Lang. 6(OOPSLA2): 114-144 (2022)" ); - try { - Files.deleteIfExists(Paths.get(fileName)); - 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"); - } catch (IOException e) { - e.printStackTrace(); - } + 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() throws Exception { + public void close() { if(dump()) { removeDuplicatedDeclarations(fileName); write("(exit)\n"); @@ -74,11 +76,11 @@ public void close() throws Exception { prover.close(); } - public void addConstraint(BooleanFormula f) throws InterruptedException { + public Void addConstraint(BooleanFormula f) throws InterruptedException { if(dump()) { write(fmgr.dumpFormula(f).toString()); } - prover.addConstraint(f); + return prover.addConstraint(f); } public boolean isUnsatWithAssumptions(Collection fs) throws SolverException, InterruptedException { @@ -132,13 +134,11 @@ public void pop() { prover.pop(); } - public void write(String content) { - if(dump()) { + private void write(String content) { + if (dump()) { File file = new File(fileName); - FileWriter writer; - try { - writer = new FileWriter(file, true); - PrintWriter printer = new PrintWriter(writer); + try (FileWriter writer = new FileWriter(file, true); + PrintWriter printer = new PrintWriter(writer)) { printer.append(removeDuplicatedDeclarations(content)); printer.close(); } catch (IOException e) { @@ -147,6 +147,10 @@ public void write(String content) { } } + public void writeComment(String content) { + write("; " + content); + } + private StringBuilder removeDuplicatedDeclarations(String content) { StringBuilder builder = new StringBuilder(); for(String line : content.split("\n")) { @@ -157,4 +161,25 @@ private StringBuilder removeDuplicatedDeclarations(String content) { } return builder; } + + @Override + public R allSat(AllSatCallback arg0, List arg1) throws InterruptedException, SolverException { + return prover.allSat(arg0, arg1); + } + + @Override + public List getUnsatCore() { + return prover.getUnsatCore(); + } + + @Override + public int size() { + return prover.size(); + } + + @Override + public Optional> unsatCoreOverAssumptions(Collection arg0) + throws SolverException, InterruptedException { + return prover.unsatCoreOverAssumptions(arg0); + } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java index 1be7c04431..a8108aa9f1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java @@ -55,27 +55,27 @@ private void run() throws InterruptedException, SolverException, InvalidConfigur SymmetryEncoder symmetryEncoder = SymmetryEncoder.withContext(context); logger.info("Starting encoding using " + ctx.getVersion()); - prover.write("; Program encoding"); + prover.writeComment("Program encoding"); prover.addConstraint(programEncoder.encodeFullProgram()); - prover.write("; Memory model encoding"); + prover.writeComment("Memory model encoding"); prover.addConstraint(wmmEncoder.encodeFullMemoryModel()); // For validation this contains information. // For verification graph.encode() just returns ctx.mkTrue() - prover.write("; Witness encoding"); + prover.writeComment("Witness encoding"); prover.addConstraint(task.getWitness().encode(context)); - prover.write("; Symmetry breaking encoding"); + 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.write("; Property encoding"); + prover.writeComment("Property encoding"); prover.addConstraint(assumedSpec); logger.info("Starting first solver.check()"); if(prover.isUnsatWithAssumptions(singletonList(assumptionLiteral))) { - prover.write("; Bound encoding"); + prover.writeComment("Bound encoding"); prover.addConstraint(propertyEncoder.encodeBoundEventExec()); logger.info("Starting second solver.check()"); res = prover.isUnsat()? PASS : Result.UNKNOWN; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java index f65ee724a2..0941215cc3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java @@ -18,67 +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 ProverWithTracker prover; - private final VerificationTask task; + private final SolverContext ctx; + private final ProverWithTracker prover; + private final VerificationTask task; - private DataRaceSolver(SolverContext c, ProverWithTracker 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, ProverWithTracker 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.write("; Program encoding"); - prover.addConstraint(programEncoder.encodeFullProgram()); - prover.write("; Memory model encoding"); - prover.addConstraint(wmmEncoder.encodeFullMemoryModel()); - prover.write("; Symmetry breaking encoding"); - prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking()); - prover.push(); - prover.write("; Property encoding"); - 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.write("; Bound encoding"); - 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); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java index 3b657a1ff3..cac688c576 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java @@ -2,7 +2,6 @@ import com.dat3m.dartagnan.configuration.Property; import com.dat3m.dartagnan.encoding.EncodingContext; -import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.encoding.WmmEncoder; import com.dat3m.dartagnan.exception.UnsatisfiedRequirementException; import com.dat3m.dartagnan.program.Program; @@ -22,6 +21,7 @@ import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverException; import java.util.Optional; @@ -109,7 +109,7 @@ public static void performStaticWmmAnalyses(VerificationTask task, Context analy analysisContext.register(RelationAnalysis.class, RelationAnalysis.fromConfig(task, analysisContext, config)); } - protected void saveFlaggedPairsOutput(Wmm wmm, WmmEncoder encoder, ProverWithTracker prover, EncodingContext ctx, Program program) throws SolverException { + protected void saveFlaggedPairsOutput(Wmm wmm, WmmEncoder encoder, ProverEnvironment prover, EncodingContext ctx, Program program) throws SolverException { if (!ctx.getTask().getProperty().contains(CAT_SPEC)) { return; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java index 5e3cfa192d..6a6bfda3ba 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java @@ -224,11 +224,11 @@ private void runInternal(SolverContext ctx, ProverWithTracker prover, Verificati final Property.Type propertyType = Property.getCombinedType(task.getProperty(), task); logger.info("Starting encoding using " + ctx.getVersion()); - prover.write("; Program encoding"); + prover.writeComment("Program encoding"); prover.addConstraint(programEncoder.encodeFullProgram()); - prover.write("; Memory model (baseline) encoding"); + prover.writeComment("Memory model (baseline) encoding"); prover.addConstraint(baselineEncoder.encodeFullMemoryModel()); - prover.write("; Symmetry breaking encoding"); + prover.writeComment("Symmetry breaking encoding"); prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking()); // ------------------------ Solving ------------------------ @@ -236,7 +236,7 @@ private void runInternal(SolverContext ctx, ProverWithTracker prover, Verificati logger.info("Checking target property."); prover.push(); - prover.write("; Property encoding"); + prover.writeComment("Property encoding"); prover.addConstraint(propertyEncoder.encodeProperties(task.getProperty())); final RefinementTrace propertyTrace = runRefinement(task, prover, solver, refiner); @@ -269,10 +269,10 @@ private void runInternal(SolverContext ctx, ProverWithTracker prover, Verificati logger.info("Checking unrolling bounds."); final long lastTime = System.currentTimeMillis(); prover.pop(); - prover.write("; Bound encoding"); + prover.writeComment("Bound encoding"); prover.addConstraint(propertyEncoder.encodeBoundEventExec()); // Add back the refinement clauses we already found, hoping that this improves the performance. - prover.write("; Refinement encoding"); + prover.writeComment("Refinement encoding"); prover.addConstraint(bmgr.and(propertyTrace.getRefinementFormulas())); final RefinementTrace boundTrace = runRefinement(task, prover, solver, refiner); boundCheckTime = System.currentTimeMillis() - lastTime; @@ -461,7 +461,7 @@ private RefinementIteration doRefinementIteration(ProverWithTracker prover, WMMS inconsistencyReasons = solverResult.getCoreReasons(); lastTime = System.currentTimeMillis(); refinementFormula = refiner.refine(inconsistencyReasons, context); - prover.write("; Refinement encoding"); + prover.writeComment("Refinement encoding"); prover.addConstraint(refinementFormula); refineTime = (System.currentTimeMillis() - lastTime); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java index e00580645e..7e71e3baac 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java @@ -1,7 +1,6 @@ package com.dat3m.dartagnan.witness.graphml; import com.dat3m.dartagnan.encoding.EncodingContext; -import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.expression.booleans.BoolLiteral; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Thread; @@ -17,6 +16,7 @@ import org.sosy_lab.common.configuration.Option; import org.sosy_lab.common.configuration.Options; import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverException; import java.io.File; @@ -40,7 +40,7 @@ public class WitnessBuilder { private final EncodingContext context; - private final ProverWithTracker prover; + private final ProverEnvironment prover; private final String type; private final String ltlProperty; @@ -60,14 +60,14 @@ public boolean canBeBuilt() { private final Map eventThreadMap = new HashMap<>(); - private WitnessBuilder(EncodingContext c, ProverWithTracker p, Result r, String summary) { + private WitnessBuilder(EncodingContext c, ProverEnvironment p, Result r, String summary) { context = checkNotNull(c); prover = checkNotNull(p); type = r.equals(FAIL) ? "violation" : "correctness"; ltlProperty = getLtlPropertyFromSummary(summary); } - public static WitnessBuilder of(EncodingContext context, ProverWithTracker prover, Result result, + public static WitnessBuilder of(EncodingContext context, ProverEnvironment prover, Result result, String ltlProperty) throws InvalidConfigurationException { WitnessBuilder b = new WitnessBuilder(context, prover, result, ltlProperty); context.getTask().getConfig().inject(b); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java index 4ca30a5d84..f0d6f31d2a 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java @@ -20,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; From 7887589f634344384acfa274a4f0d5ebc745d896 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Thu, 5 Sep 2024 10:46:00 +0200 Subject: [PATCH 15/31] Add support to CAAT for SyncBar, SyncFence and Vloc relations (#724) --- .../verification/solving/RefinementSolver.java | 15 ++++++++++++--- .../spirv/basic/SpirvAssertionsTest.java | 4 ++-- .../spirv/benchmarks/SpirvAssertionsTest.java | 4 ++-- .../spirv/benchmarks/SpirvChecksTest.java | 4 ++-- .../spirv/benchmarks/SpirvRacesTest.java | 4 ++-- .../spirv/gpuverify/SpirvChecksTest.java | 4 ++-- .../dartagnan/spirv/gpuverify/SpirvRacesTest.java | 4 ++-- 7 files changed, 24 insertions(+), 15 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java index bebb12fd78..f432c68d0f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java @@ -469,6 +469,13 @@ private RefinementIteration doRefinementIteration(ProverEnvironment prover, WMMS // ================================================================================================================ // Special memory model processing + private static boolean isUnknownDefinitionForCAAT(Definition def) { + // TODO: We should probably automatically cut all "unknown relation", + // i.e., use a white-list of known relations instead of a blacklist of unknown one's. + return def instanceof LinuxCriticalSections // LKMM + || def instanceof SyncFence || def instanceof SyncBar || def instanceof SameVirtualLocation; // GPUs + } + private static RefinementModel generateRefinementModel(Wmm original) { // We cut (i) negated axioms, (ii) negated relations (if derived), // and (iii) some special relations because they are derived from internal relations (like data/addr/ctrl) @@ -492,7 +499,7 @@ private static RefinementModel generateRefinementModel(Wmm original) { } else if (c instanceof Definition def && def.getDefinedRelation().hasName()) { // (iii) Special relations final String name = def.getDefinedRelation().getName().get(); - if (name.equals(DATA) || name.equals(CTRL) || name.equals(ADDR) || name.equals(CRIT)) { + if (name.equals(DATA) || name.equals(CTRL) || name.equals(ADDR) || isUnknownDefinitionForCAAT(def)) { constraintsToCut.add(c); } } else if (c instanceof Definition def && def instanceof Fences) { @@ -516,7 +523,8 @@ private static void addBiases(Wmm memoryModel, EnumSet biases) { memoryModel.getOrCreatePredefinedRelation(POLOC), rf, memoryModel.getOrCreatePredefinedRelation(CO), - memoryModel.getOrCreatePredefinedRelation(FR))))); + memoryModel.getOrCreatePredefinedRelation(FR) + )))); } if (biases.contains(Baseline.NO_OOTA)) { // ---- acyclic (dep | rf) ---- @@ -524,7 +532,8 @@ private static void addBiases(Wmm memoryModel, EnumSet biases) { memoryModel.getOrCreatePredefinedRelation(CTRL), memoryModel.getOrCreatePredefinedRelation(DATA), memoryModel.getOrCreatePredefinedRelation(ADDR), - rf)))); + rf) + ))); } if (biases.contains(Baseline.ATOMIC_RMW)) { // ---- empty (rmw & fre;coe) ---- diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java index 18878d7f92..9c2f3fa06c 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java @@ -7,6 +7,7 @@ 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.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; import org.junit.Test; import org.junit.runner.RunWith; @@ -120,10 +121,9 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - /* TODO: Implementation try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); - }*/ + } try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java index 96acad8bbc..9006c1b99f 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java @@ -7,6 +7,7 @@ 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.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; import org.junit.Test; import org.junit.runner.RunWith; @@ -113,10 +114,9 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - /* TODO: Implementation try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); - }*/ + } try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java index 6043e53303..c217abd6f7 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java @@ -7,6 +7,7 @@ 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.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; import org.junit.Test; import org.junit.runner.RunWith; @@ -117,10 +118,9 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - /* TODO: Implementation try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); - }*/ + } try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java index 5f4ac94440..a5c88e5f77 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java @@ -7,6 +7,7 @@ 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.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; import org.junit.Test; import org.junit.runner.RunWith; @@ -118,10 +119,9 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - /* TODO: Implementation try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); - }*/ + } try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java index 6124efb5b0..b682b3505e 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java @@ -7,6 +7,7 @@ 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.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; import org.junit.Test; import org.junit.runner.RunWith; @@ -345,10 +346,9 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - /* TODO: Implementation try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); - }*/ + } try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java index 29b7ad7990..da21d9fb30 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java @@ -7,6 +7,7 @@ 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.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; import org.junit.Test; import org.junit.runner.RunWith; @@ -345,10 +346,9 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - /* TODO: Implementation try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); - }*/ + } try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } From 1bd4bd02171badff84a45d9789afe058e9621266 Mon Sep 17 00:00:00 2001 From: natgavrilenko Date: Thu, 5 Sep 2024 16:17:29 +0200 Subject: [PATCH 16/31] Add unrolling bound to program spec encoding (#727) --- .../dartagnan/encoding/PropertyEncoder.java | 6 +++-- .../spirv/basic/SpirvAssertionsTest.java | 24 +++++++------------ 2 files changed, 12 insertions(+), 18 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java index 36427a5adf..994f9da6bd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java @@ -36,6 +36,7 @@ import static com.dat3m.dartagnan.configuration.Property.*; import static com.dat3m.dartagnan.program.Program.SourceLanguage.LLVM; +import static com.dat3m.dartagnan.program.Program.SpecificationType.ASSERT; import static com.dat3m.dartagnan.wmm.RelationNameRepository.CO; public class PropertyEncoder implements Encoder { @@ -275,7 +276,7 @@ private TrackableFormula encodeProgramSpecification() { case FORALL, NOT_EXISTS, ASSERT -> bmgr.not(PROGRAM_SPEC.getSMTVariable(context)); case EXISTS -> PROGRAM_SPEC.getSMTVariable(context); }; - if (!program.getFormat().equals(LLVM)) { + if (!ASSERT.equals(program.getSpecificationType())) { encoding = bmgr.and(encoding, encodeProgramTermination()); } return new TrackableFormula(trackingLiteral, encoding); @@ -283,9 +284,10 @@ private TrackableFormula encodeProgramSpecification() { private BooleanFormula encodeProgramTermination() { final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); - return bmgr.and(program.getThreads().stream() + BooleanFormula exitReached = bmgr.and(program.getThreads().stream() .map(t -> bmgr.equivalence(context.execution(t.getEntry()), context.execution(t.getExit()))) .toList()); + return bmgr.and(exitReached, bmgr.not(encodeBoundEventExec())); } // ====================================================================== diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java index 9c2f3fa06c..e86077b009 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java @@ -28,8 +28,7 @@ import static com.dat3m.dartagnan.configuration.Property.PROGRAM_SPEC; import static com.dat3m.dartagnan.utils.ResourceHelper.getRootPath; import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath; -import static com.dat3m.dartagnan.utils.Result.FAIL; -import static com.dat3m.dartagnan.utils.Result.PASS; +import static com.dat3m.dartagnan.utils.Result.*; import static org.junit.Assert.assertEquals; @RunWith(Parameterized.class) @@ -79,30 +78,23 @@ public static Iterable data() throws IOException { {"builtin-all-321.spv.dis", 1, PASS}, {"branch-cond-ff.spv.dis", 1, PASS}, {"branch-cond-ff-inverted.spv.dis", 1, PASS}, - {"branch-cond-bf.spv.dis", 1, FAIL}, + {"branch-cond-bf.spv.dis", 1, UNKNOWN}, {"branch-cond-bf.spv.dis", 2, PASS}, - {"branch-cond-bf.spv.dis", 3, PASS}, - {"branch-cond-fb.spv.dis", 1, FAIL}, + {"branch-cond-fb.spv.dis", 1, UNKNOWN}, {"branch-cond-fb.spv.dis", 2, PASS}, - {"branch-cond-fb.spv.dis", 3, PASS}, {"branch-cond-struct.spv.dis", 1, PASS}, {"branch-cond-struct-read-write.spv.dis", 1, PASS}, {"branch-race.spv.dis", 1, PASS}, - {"branch-loop.spv.dis", 2, FAIL}, + {"branch-loop.spv.dis", 2, UNKNOWN}, {"branch-loop.spv.dis", 3, PASS}, - {"branch-loop.spv.dis", 4, PASS}, - {"loop-struct-cond.spv.dis", 1, FAIL}, + {"loop-struct-cond.spv.dis", 1, UNKNOWN}, {"loop-struct-cond.spv.dis", 2, PASS}, - {"loop-struct-cond.spv.dis", 3, PASS}, - {"loop-struct-cond-suffix.spv.dis", 1, FAIL}, + {"loop-struct-cond-suffix.spv.dis", 1, UNKNOWN}, {"loop-struct-cond-suffix.spv.dis", 2, PASS}, - {"loop-struct-cond-suffix.spv.dis", 3, PASS}, - {"loop-struct-cond-sequence.spv.dis", 2, FAIL}, + {"loop-struct-cond-sequence.spv.dis", 2, UNKNOWN}, {"loop-struct-cond-sequence.spv.dis", 3, PASS}, - {"loop-struct-cond-sequence.spv.dis", 4, PASS}, - {"loop-struct-cond-nested.spv.dis", 2, FAIL}, + {"loop-struct-cond-nested.spv.dis", 2, UNKNOWN}, {"loop-struct-cond-nested.spv.dis", 3, PASS}, - {"loop-struct-cond-nested.spv.dis", 4, PASS}, {"phi.spv.dis", 1, PASS}, {"phi-unstruct-true.spv.dis", 1, PASS}, {"phi-unstruct-false.spv.dis", 1, PASS}, From 0b42ed330fef87e21d4fc4b622eaa66999286425 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Thu, 5 Sep 2024 17:20:05 +0200 Subject: [PATCH 17/31] Feedback implemented --- .../dartagnan/encoding/ProverWithTracker.java | 67 ++++++++++++------- 1 file changed, 41 insertions(+), 26 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index d2d007d9f7..c9046bdb16 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -76,6 +76,7 @@ public void close() { prover.close(); } + @Override public Void addConstraint(BooleanFormula f) throws InterruptedException { if(dump()) { write(fmgr.dumpFormula(f).toString()); @@ -83,23 +84,31 @@ public Void addConstraint(BooleanFormula f) throws InterruptedException { return prover.addConstraint(f); } + @Override public boolean isUnsatWithAssumptions(Collection fs) throws SolverException, InterruptedException { - long start = System.currentTimeMillis(); - boolean result = prover.isUnsatWithAssumptions(fs); - long end = System.currentTimeMillis(); + 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"); - write("; Original solving time: " + (end - start) + " ms"); + 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(); @@ -107,19 +116,22 @@ public boolean isUnsat() throws SolverException, InterruptedException { if(dump()) { write("(set-info :status " + (result ? "unsat" : "sat") + ")\n"); write("(check-sat)\n"); - write("; Original solving time: " + (end - start) + " ms"); + writeComment("Original solving time: " + (end - start) + " ms"); } return result; } + @Override public ImmutableMap getStatistics() { return prover.getStatistics(); } + @Override public Model getModel() throws SolverException { return prover.getModel(); } + @Override public void push() throws InterruptedException { if(dump()) { write("(push)\n"); @@ -127,6 +139,7 @@ public void push() throws InterruptedException { prover.push(); } + @Override public void pop() { if(dump()) { write("(pop)\n"); @@ -134,6 +147,27 @@ public void pop() { prover.pop(); } + @Override + public R allSat(AllSatCallback arg0, List arg1) throws InterruptedException, SolverException { + return prover.allSat(arg0, arg1); + } + + @Override + public List getUnsatCore() { + return prover.getUnsatCore(); + } + + @Override + public int size() { + return prover.size(); + } + + @Override + public Optional> unsatCoreOverAssumptions(Collection arg0) + throws SolverException, InterruptedException { + return prover.unsatCoreOverAssumptions(arg0); + } + private void write(String content) { if (dump()) { File file = new File(fileName); @@ -151,6 +185,8 @@ 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")) { @@ -161,25 +197,4 @@ private StringBuilder removeDuplicatedDeclarations(String content) { } return builder; } - - @Override - public R allSat(AllSatCallback arg0, List arg1) throws InterruptedException, SolverException { - return prover.allSat(arg0, arg1); - } - - @Override - public List getUnsatCore() { - return prover.getUnsatCore(); - } - - @Override - public int size() { - return prover.size(); - } - - @Override - public Optional> unsatCoreOverAssumptions(Collection arg0) - throws SolverException, InterruptedException { - return prover.unsatCoreOverAssumptions(arg0); - } } From c0f2eb5cb8e3f1756b95458e49c878ed6c00bed5 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 27 Aug 2024 20:06:49 +0200 Subject: [PATCH 18/31] Add option to dump encoding to smtlib2 file --- .../java/com/dat3m/dartagnan/Dartagnan.java | 14 ++-- .../dartagnan/configuration/OptionNames.java | 1 + .../dartagnan/encoding/ProverWithTracker.java | 82 +++++++++++++++++++ .../processing/compilation/VisitorLKMM.java | 2 - .../dartagnan/utils/options/BaseOptions.java | 7 ++ .../verification/solving/AssumeSolver.java | 6 +- .../verification/solving/DataRaceSolver.java | 8 +- .../verification/solving/ModelChecker.java | 4 +- .../solving/RefinementSolver.java | 8 +- .../witness/graphml/WitnessBuilder.java | 8 +- .../com/dat3m/dartagnan/wmm/Assumption.java | 6 -- .../com/dat3m/dartagnan/wmm/Constraint.java | 1 - .../com/dat3m/dartagnan/c/AbstractCTest.java | 4 +- .../compilation/AbstractCompilationTest.java | 5 +- .../dartagnan/litmus/AbstractLitmusTest.java | 6 +- .../miscellaneous/ArrayValidTest.java | 4 +- .../dartagnan/miscellaneous/BranchTest.java | 4 +- .../spirv/basic/SpirvAssertionsTest.java | 13 +-- .../spirv/benchmarks/SpirvAssertionsTest.java | 11 +-- .../spirv/benchmarks/SpirvChecksTest.java | 13 +-- .../spirv/benchmarks/SpirvRacesTest.java | 13 +-- .../spirv/gpuverify/SpirvChecksTest.java | 13 +-- .../spirv/gpuverify/SpirvRacesTest.java | 13 +-- .../dartagnan/utils/rules/Providers.java | 8 +- .../dartagnan/witness/BuildWitnessTest.java | 4 +- 25 files changed, 175 insertions(+), 83 deletions(-) create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 3ccab85b38..f8e0765223 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -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) { @@ -207,7 +211,7 @@ public static void main(String[] args) throws Exception { } } - public static File generateExecutionGraphFile(VerificationTask task, ProverEnvironment prover, ModelChecker modelChecker, + public static File generateExecutionGraphFile(VerificationTask task, ProverWithTracker prover, ModelChecker modelChecker, WitnessType witnessType) throws InvalidConfigurationException, SolverException, IOException { Preconditions.checkArgument(modelChecker.hasModel(), "No execution graph to generate."); @@ -228,7 +232,7 @@ public static File generateExecutionGraphFile(VerificationTask task, ProverEnvir synContext, witnessType.convertToPng()); } - private static void generateWitnessIfAble(VerificationTask task, ProverEnvironment prover, + private static void generateWitnessIfAble(VerificationTask task, ProverWithTracker prover, ModelChecker modelChecker, String summary) { // ------------------ Generate Witness, if possible ------------------ final EnumSet properties = task.getProperty(); @@ -247,7 +251,7 @@ private static void generateWitnessIfAble(VerificationTask task, ProverEnvironme } } - public static String generateResultSummary(VerificationTask task, ProverEnvironment prover, + public static String generateResultSummary(VerificationTask task, ProverWithTracker prover, ModelChecker modelChecker) throws SolverException { // ----------------- Generate output of verification result ----------------- final Program p = task.getProgram(); @@ -385,7 +389,7 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm return summary.toString(); } - private static void printWarningIfThreadStartFailed(Program p, EncodingContext encoder, ProverEnvironment prover) + private static void printWarningIfThreadStartFailed(Program p, EncodingContext encoder, ProverWithTracker prover) throws SolverException { for (Event e : p.getThreadEvents()) { if (e.hasTag(Tag.STARTLOAD) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java index 3cec00bf75..18a0ca89fc 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java @@ -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"; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java new file mode 100644 index 0000000000..6737036aaa --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -0,0 +1,82 @@ +package com.dat3m.dartagnan.encoding; + +import java.io.File; +import java.io.FileWriter; +import java.io.IOException; +import java.io.PrintWriter; +import java.util.Collection; + +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.FormulaManager; +import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.ProverEnvironment; +import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; + +import com.google.common.collect.ImmutableMap; + +public class ProverWithTracker implements AutoCloseable { + + private final FormulaManager fmgr; + private final ProverEnvironment prover; + private final String fileName; + private BooleanFormula enc; + + public ProverWithTracker(SolverContext ctx, String filename, ProverOptions... options) { + this.fmgr = ctx.getFormulaManager(); + this.prover = ctx.newProverEnvironment(options); + this.enc = ctx.getFormulaManager().getBooleanFormulaManager().makeTrue(); + this.fileName = filename; + } + + @Override + public void close() throws Exception { + if(!fileName.isEmpty()) { + File file = new File(fileName); + FileWriter writer; + try { + writer = new FileWriter(file, true); + PrintWriter printer = new PrintWriter(writer); + printer.append("(set-logic ALL)\n"); + printer.append(fmgr.dumpFormula(enc).toString()); + printer.append("(check-sat)"); + printer.close(); + } catch (IOException e) { + e.printStackTrace(); + } + } + prover.close(); + } + + public void addConstraint(BooleanFormula f) throws InterruptedException { + if(!fileName.isEmpty()) { + enc = fmgr.getBooleanFormulaManager().and(f, enc); + } + prover.addConstraint(f); + } + + public boolean isUnsatWithAssumptions(Collection f) throws SolverException, InterruptedException { + return prover.isUnsatWithAssumptions(f); + } + + public boolean isUnsat() throws SolverException, InterruptedException { + return prover.isUnsat(); + } + + public ImmutableMap getStatistics() { + return prover.getStatistics(); + } + + public Model getModel() throws SolverException { + return prover.getModel(); + } + + public void push() throws InterruptedException { + prover.push(); + } + + public void pop() { + prover.pop(); + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java index b448471580..d858308a5f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java @@ -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; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java index 32cfec175a..fd166a38e0 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java @@ -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; } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java index cc0200630b..38b18925ec 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java @@ -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(); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java index 5190ef5d4c..c0d9b136ca 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java @@ -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; @@ -25,16 +25,16 @@ public class DataRaceSolver extends ModelChecker { private static final Logger logger = LogManager.getLogger(DataRaceSolver.class); private final SolverContext ctx; - private final ProverEnvironment prover; + private final ProverWithTracker prover; private final VerificationTask task; - private DataRaceSolver(SolverContext c, ProverEnvironment p, VerificationTask 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) + public static DataRaceSolver run(SolverContext ctx, ProverWithTracker prover, VerificationTask task) throws InterruptedException, SolverException, InvalidConfigurationException { DataRaceSolver s = new DataRaceSolver(ctx, prover, task); s.run(); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java index cac688c576..3b657a1ff3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java @@ -2,6 +2,7 @@ import com.dat3m.dartagnan.configuration.Property; import com.dat3m.dartagnan.encoding.EncodingContext; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.encoding.WmmEncoder; import com.dat3m.dartagnan.exception.UnsatisfiedRequirementException; import com.dat3m.dartagnan.program.Program; @@ -21,7 +22,6 @@ import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.java_smt.api.Model; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverException; import java.util.Optional; @@ -109,7 +109,7 @@ public static void performStaticWmmAnalyses(VerificationTask task, Context analy analysisContext.register(RelationAnalysis.class, RelationAnalysis.fromConfig(task, analysisContext, config)); } - protected void saveFlaggedPairsOutput(Wmm wmm, WmmEncoder encoder, ProverEnvironment prover, EncodingContext ctx, Program program) throws SolverException { + protected void saveFlaggedPairsOutput(Wmm wmm, WmmEncoder encoder, ProverWithTracker prover, EncodingContext ctx, Program program) throws SolverException { if (!ctx.getTask().getProperty().contains(CAT_SPEC)) { return; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java index f432c68d0f..94684794f8 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java @@ -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(); @@ -358,7 +358,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 trace = new ArrayList<>(); @@ -418,7 +418,7 @@ private boolean checkProgress(List 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; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java index 7e71e3baac..e00580645e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.witness.graphml; import com.dat3m.dartagnan.encoding.EncodingContext; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.expression.booleans.BoolLiteral; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Thread; @@ -16,7 +17,6 @@ import org.sosy_lab.common.configuration.Option; import org.sosy_lab.common.configuration.Options; import org.sosy_lab.java_smt.api.Model; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverException; import java.io.File; @@ -40,7 +40,7 @@ public class WitnessBuilder { private final EncodingContext context; - private final ProverEnvironment prover; + private final ProverWithTracker prover; private final String type; private final String ltlProperty; @@ -60,14 +60,14 @@ public boolean canBeBuilt() { private final Map eventThreadMap = new HashMap<>(); - private WitnessBuilder(EncodingContext c, ProverEnvironment p, Result r, String summary) { + private WitnessBuilder(EncodingContext c, ProverWithTracker p, Result r, String summary) { context = checkNotNull(c); prover = checkNotNull(p); type = r.equals(FAIL) ? "violation" : "correctness"; ltlProperty = getLtlPropertyFromSummary(summary); } - public static WitnessBuilder of(EncodingContext context, ProverEnvironment prover, Result result, + public static WitnessBuilder of(EncodingContext context, ProverWithTracker prover, Result result, String ltlProperty) throws InvalidConfigurationException { WitnessBuilder b = new WitnessBuilder(context, prover, result, ltlProperty); context.getTask().getConfig().inject(b); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java index 2da9f984e9..788a3b8f09 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java @@ -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; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java index 1a674d9626..4c5ef52794 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java @@ -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; diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java index 8593902783..39d4ef879d 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java @@ -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 getConfigurationProvider() { protected final Provider configurationProvider = getConfigurationProvider(); protected final Provider taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, boundProvider, configurationProvider); protected final Provider contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider, solverProvider); - protected final Provider proverProvider = Providers.createProverWithFixedOptions(contextProvider, SolverContext.ProverOptions.GENERATE_MODELS); + protected final Provider proverProvider = Providers.createProverWithFixedOptions(contextProvider, SolverContext.ProverOptions.GENERATE_MODELS); // Special rules protected final Timeout timeout = Timeout.millis(getTimeout()); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java index b92e1209f5..4ca30a5d84 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java @@ -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; @@ -99,8 +100,8 @@ protected Provider getConfigurationProvider() { protected final Provider task2Provider = Providers.createTask(program2Provider, wmm2Provider, propertyProvider, targetProvider, () -> 1, configProvider); protected final Provider context1Provider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3); protected final Provider context2Provider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3); - protected final Provider prover1Provider = Providers.createProverWithFixedOptions(context1Provider, ProverOptions.GENERATE_MODELS); - protected final Provider prover2Provider = Providers.createProverWithFixedOptions(context2Provider, ProverOptions.GENERATE_MODELS); + protected final Provider prover1Provider = Providers.createProverWithFixedOptions(context1Provider, ProverOptions.GENERATE_MODELS); + protected final Provider prover2Provider = Providers.createProverWithFixedOptions(context2Provider, ProverOptions.GENERATE_MODELS); private final Timeout timeout = Timeout.millis(getTimeout()); private final RequestShutdownOnError shutdownOnError = RequestShutdownOnError.create(shutdownManagerProvider); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java index 1e86058312..3316d114eb 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java @@ -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 configProvider = getConfigurationProvider(); protected final Provider taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, boundProvider, configProvider); protected final Provider contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3); - protected final Provider proverProvider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS); - protected final Provider prover2Provider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS); + protected final Provider proverProvider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS); + protected final Provider prover2Provider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS); private final Timeout timeout = Timeout.millis(getTimeout()); private final RequestShutdownOnError shutdownOnError = RequestShutdownOnError.create(shutdownManagerProvider); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/ArrayValidTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/ArrayValidTest.java index fa2d573259..e8ba520d5c 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/ArrayValidTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/ArrayValidTest.java @@ -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) diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/BranchTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/BranchTest.java index 05d84eb465..588dc3cdb0 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/BranchTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/BranchTest.java @@ -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) diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java index e86077b009..3cb16dab13 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java @@ -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,14 +113,15 @@ public static Iterable 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()); } } + private SolverContext mkCtx() throws InvalidConfigurationException { Configuration cfg = Configuration.builder().build(); return SolverContextFactory.createSolverContext( @@ -130,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 { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java index 9006c1b99f..feebf420e5 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java @@ -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,14 +114,15 @@ public static Iterable 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()); } } + private SolverContext mkCtx() throws InvalidConfigurationException { Configuration cfg = Configuration.builder().build(); return SolverContextFactory.createSolverContext( @@ -131,8 +132,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 { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java index c217abd6f7..31f123e500 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java @@ -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,14 +118,15 @@ public static Iterable 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()); } } + private SolverContext mkCtx() throws InvalidConfigurationException { Configuration cfg = Configuration.builder().build(); return SolverContextFactory.createSolverContext( @@ -135,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 { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java index a5c88e5f77..c466911c43 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java @@ -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,14 +119,15 @@ public static Iterable 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()); } } + private SolverContext mkCtx() throws InvalidConfigurationException { Configuration cfg = Configuration.builder().build(); return SolverContextFactory.createSolverContext( @@ -136,8 +137,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 { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java index b682b3505e..2870b77f1b 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java @@ -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,14 +346,15 @@ public static Iterable 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()); } } + private SolverContext mkCtx() throws InvalidConfigurationException { Configuration cfg = Configuration.builder().build(); return SolverContextFactory.createSolverContext( @@ -363,8 +364,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 { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java index da21d9fb30..5708ce4525 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java @@ -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,14 +346,15 @@ public static Iterable 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()); } } + private SolverContext mkCtx() throws InvalidConfigurationException { Configuration cfg = Configuration.builder().build(); return SolverContextFactory.createSolverContext( @@ -363,8 +364,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 { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java b/dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java index 0b8c06b449..f31db39a13 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java @@ -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 createSolverContextFromManager(Supplier TestHelper.createContextWithShutdownNotifier(shutdownManagerSupplier.get().getNotifier(), solverSupplier.get())); } - public static Provider createProver(Supplier contextSupplier, Supplier optionsSupplier) { - return Provider.fromSupplier(() -> contextSupplier.get().newProverEnvironment(optionsSupplier.get())); + public static Provider createProver(Supplier contextSupplier, Supplier optionsSupplier) { + return Provider.fromSupplier(() -> new ProverWithTracker(contextSupplier.get(), "", optionsSupplier.get())); } - public static Provider createProverWithFixedOptions(Supplier contextSupplier, SolverContext.ProverOptions... options) { + public static Provider createProverWithFixedOptions(Supplier contextSupplier, SolverContext.ProverOptions... options) { return createProver(contextSupplier, () -> options); } } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java index 98b1d7d9ee..7b4d135cb4 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java @@ -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"); From 9aaf067a07d032f670304a078bd15299072b8d35 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Wed, 28 Aug 2024 17:15:59 +0200 Subject: [PATCH 19/31] Dump formula in each access to the prover --- .../java/com/dat3m/dartagnan/Dartagnan.java | 1 - .../dartagnan/encoding/ProverWithTracker.java | 106 +++++++++++++----- 2 files changed, 78 insertions(+), 29 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index f8e0765223..fae62e2651 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -43,7 +43,6 @@ import org.sosy_lab.common.log.BasicLogManager; import org.sosy_lab.java_smt.SolverContextFactory; import org.sosy_lab.java_smt.api.Model; -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 org.sosy_lab.java_smt.api.SolverException; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index 6737036aaa..d30496a3a5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -1,17 +1,18 @@ package com.dat3m.dartagnan.encoding; +import java.io.BufferedReader; +import java.io.BufferedWriter; import java.io.File; +import java.io.FileReader; import java.io.FileWriter; import java.io.IOException; import java.io.PrintWriter; +import java.nio.file.Files; +import java.nio.file.Paths; +import java.util.ArrayList; import java.util.Collection; - -import org.sosy_lab.java_smt.api.BooleanFormula; -import org.sosy_lab.java_smt.api.FormulaManager; -import org.sosy_lab.java_smt.api.Model; -import org.sosy_lab.java_smt.api.ProverEnvironment; -import org.sosy_lab.java_smt.api.SolverContext; -import org.sosy_lab.java_smt.api.SolverException; +import java.util.List; +import org.sosy_lab.java_smt.api.*; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import com.google.common.collect.ImmutableMap; @@ -21,46 +22,76 @@ public class ProverWithTracker implements AutoCloseable { private final FormulaManager fmgr; private final ProverEnvironment prover; private final String fileName; - private BooleanFormula enc; - public ProverWithTracker(SolverContext ctx, String filename, ProverOptions... options) { + public ProverWithTracker(SolverContext ctx, String fileName, ProverOptions... options) { this.fmgr = ctx.getFormulaManager(); this.prover = ctx.newProverEnvironment(options); - this.enc = ctx.getFormulaManager().getBooleanFormulaManager().makeTrue(); - this.fileName = filename; + this.fileName = fileName; + init(); + } + + private void init() { + try { + Files.deleteIfExists(Paths.get(fileName)); + write("(set-logic ALL)\n"); + } catch (IOException e) { + e.printStackTrace(); + } } @Override public void close() throws Exception { - if(!fileName.isEmpty()) { - File file = new File(fileName); - FileWriter writer; - try { - writer = new FileWriter(file, true); - PrintWriter printer = new PrintWriter(writer); - printer.append("(set-logic ALL)\n"); - printer.append(fmgr.dumpFormula(enc).toString()); - printer.append("(check-sat)"); - printer.close(); - } catch (IOException e) { - e.printStackTrace(); - } - } + removeDuplicatedDeclarations(fileName); prover.close(); } + private void removeDuplicatedDeclarations(String fileName) { + try { + BufferedReader reader = new BufferedReader(new FileReader(fileName)); + List newLines = new ArrayList<>(); + String line; + while ((line = reader.readLine()) != null) { + // We only skip repeated declarations + if (!line.contains("declare-fun") || !newLines.contains(line)) { + newLines.add(line); + } + } + reader.close(); + + BufferedWriter writer = new BufferedWriter(new FileWriter(fileName)); + for (String newLine : newLines) { + writer.write(newLine); + writer.newLine(); + } + writer.close(); + } catch (IOException e) { + e.printStackTrace(); + } + } + public void addConstraint(BooleanFormula f) throws InterruptedException { if(!fileName.isEmpty()) { - enc = fmgr.getBooleanFormulaManager().and(f, enc); + write(fmgr.dumpFormula(f).toString()); } prover.addConstraint(f); } - public boolean isUnsatWithAssumptions(Collection f) throws SolverException, InterruptedException { - return prover.isUnsatWithAssumptions(f); + public boolean isUnsatWithAssumptions(Collection fs) throws SolverException, InterruptedException { + if(!fileName.isEmpty()) { + write("(push)\n"); + for(BooleanFormula f : fs) { + write(fmgr.dumpFormula(f).toString()); + } + write("(check-sat)\n"); + write("(pop)\n"); + } + return prover.isUnsatWithAssumptions(fs); } public boolean isUnsat() throws SolverException, InterruptedException { + if(!fileName.isEmpty()) { + write("(check-sat)\n"); + } return prover.isUnsat(); } @@ -73,10 +104,29 @@ public Model getModel() throws SolverException { } public void push() throws InterruptedException { + if(!fileName.isEmpty()) { + write("(push)\n"); + } prover.push(); } public void pop() { + if(!fileName.isEmpty()) { + write("(pop)\n"); + } prover.pop(); } + + private void write(String content) { + File file = new File(fileName); + FileWriter writer; + try { + writer = new FileWriter(file, true); + PrintWriter printer = new PrintWriter(writer); + printer.append(content); + printer.close(); + } catch (IOException e) { + e.printStackTrace(); + } + } } From acf6de822e8a58937e6c9bcc1ae06c811e805455 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Wed, 28 Aug 2024 17:28:32 +0200 Subject: [PATCH 20/31] Minor changes --- .../java/com/dat3m/dartagnan/Dartagnan.java | 2 +- .../dartagnan/encoding/ProverWithTracker.java | 26 ++++++++++++++----- 2 files changed, 20 insertions(+), 8 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index fae62e2651..3cb97bdef5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -164,7 +164,7 @@ public static void main(String[] args) throws Exception { sdm.getNotifier(), o.getSolver()); ProverWithTracker prover = new ProverWithTracker(ctx, - o.getDumpSmtLib() ? + o.getDumpSmtLib() ? System.getenv("DAT3M_OUTPUT") + String.format("/%s.smt2", p.getName()) : "", ProverOptions.GENERATE_MODELS)) { ModelChecker modelChecker; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index d30496a3a5..1dba0afb64 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -18,10 +18,10 @@ import com.google.common.collect.ImmutableMap; public class ProverWithTracker implements AutoCloseable { - + private final FormulaManager fmgr; private final ProverEnvironment prover; - private final String fileName; + private final String fileName; public ProverWithTracker(SolverContext ctx, String fileName, ProverOptions... options) { this.fmgr = ctx.getFormulaManager(); @@ -30,6 +30,11 @@ public ProverWithTracker(SolverContext ctx, String fileName, ProverOptions... op init(); } + // An empty filename means there is no need to dump the encoding + private boolean dump() { + return !fileName.isEmpty(); + } + private void init() { try { Files.deleteIfExists(Paths.get(fileName)); @@ -45,8 +50,14 @@ public void close() throws Exception { prover.close(); } + // Each call to fmgr.dumpFormula(f) defines all variables used in f. + // We might end up with several definitions of the declarations. + // This might not be the most performant implementation, but duming the + // smtlib2 file is intended only for debugging or trying to understand + // how to optimize the encoding, thus performance is not an issue. private void removeDuplicatedDeclarations(String fileName) { try { + BufferedReader reader = new BufferedReader(new FileReader(fileName)); List newLines = new ArrayList<>(); String line; @@ -64,20 +75,21 @@ private void removeDuplicatedDeclarations(String fileName) { writer.newLine(); } writer.close(); + } catch (IOException e) { e.printStackTrace(); } } public void addConstraint(BooleanFormula f) throws InterruptedException { - if(!fileName.isEmpty()) { + if(dump()) { write(fmgr.dumpFormula(f).toString()); } prover.addConstraint(f); } public boolean isUnsatWithAssumptions(Collection fs) throws SolverException, InterruptedException { - if(!fileName.isEmpty()) { + if(dump()) { write("(push)\n"); for(BooleanFormula f : fs) { write(fmgr.dumpFormula(f).toString()); @@ -89,7 +101,7 @@ public boolean isUnsatWithAssumptions(Collection fs) throws Solv } public boolean isUnsat() throws SolverException, InterruptedException { - if(!fileName.isEmpty()) { + if(dump()) { write("(check-sat)\n"); } return prover.isUnsat(); @@ -104,14 +116,14 @@ public Model getModel() throws SolverException { } public void push() throws InterruptedException { - if(!fileName.isEmpty()) { + if(dump()) { write("(push)\n"); } prover.push(); } public void pop() { - if(!fileName.isEmpty()) { + if(dump()) { write("(pop)\n"); } prover.pop(); From 2ec7e7b5139a4a371fc642e9433fcb64f4f4901c Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Thu, 29 Aug 2024 10:05:57 +0200 Subject: [PATCH 21/31] Remove duplicates in every call to write --- .../dartagnan/encoding/ProverWithTracker.java | 51 +++++++------------ 1 file changed, 18 insertions(+), 33 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index 1dba0afb64..a6950fe5db 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -11,7 +11,10 @@ import java.nio.file.Paths; import java.util.ArrayList; import java.util.Collection; +import java.util.HashSet; import java.util.List; +import java.util.Set; + import org.sosy_lab.java_smt.api.*; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; @@ -21,12 +24,14 @@ public class ProverWithTracker implements AutoCloseable { private final FormulaManager fmgr; private final ProverEnvironment prover; - private final String fileName; + private final String fileName; + private final Set 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(); } @@ -50,37 +55,6 @@ public void close() throws Exception { prover.close(); } - // Each call to fmgr.dumpFormula(f) defines all variables used in f. - // We might end up with several definitions of the declarations. - // This might not be the most performant implementation, but duming the - // smtlib2 file is intended only for debugging or trying to understand - // how to optimize the encoding, thus performance is not an issue. - private void removeDuplicatedDeclarations(String fileName) { - try { - - BufferedReader reader = new BufferedReader(new FileReader(fileName)); - List newLines = new ArrayList<>(); - String line; - while ((line = reader.readLine()) != null) { - // We only skip repeated declarations - if (!line.contains("declare-fun") || !newLines.contains(line)) { - newLines.add(line); - } - } - reader.close(); - - BufferedWriter writer = new BufferedWriter(new FileWriter(fileName)); - for (String newLine : newLines) { - writer.write(newLine); - writer.newLine(); - } - writer.close(); - - } catch (IOException e) { - e.printStackTrace(); - } - } - public void addConstraint(BooleanFormula f) throws InterruptedException { if(dump()) { write(fmgr.dumpFormula(f).toString()); @@ -135,10 +109,21 @@ private void write(String content) { try { writer = new FileWriter(file, true); PrintWriter printer = new PrintWriter(writer); - printer.append(content); + printer.append(removeDuplicatedDeclarations(content)); printer.close(); } catch (IOException e) { e.printStackTrace(); } } + + private String removeDuplicatedDeclarations(String content) { + String output = ""; + for(String line : content.split("\n")) { + if(line.contains("declare-fun") && !declarations.add(line)) { + continue; + } + output += line + "\n"; + } + return output; + } } From f9dd7393dd22a686eef128a58b3144548ee4d96e Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Thu, 29 Aug 2024 10:49:25 +0200 Subject: [PATCH 22/31] Remove unused imports --- .../java/com/dat3m/dartagnan/encoding/ProverWithTracker.java | 5 ----- 1 file changed, 5 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index a6950fe5db..a5eb2832f5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -1,18 +1,13 @@ package com.dat3m.dartagnan.encoding; -import java.io.BufferedReader; -import java.io.BufferedWriter; import java.io.File; -import java.io.FileReader; import java.io.FileWriter; import java.io.IOException; import java.io.PrintWriter; import java.nio.file.Files; import java.nio.file.Paths; -import java.util.ArrayList; import java.util.Collection; import java.util.HashSet; -import java.util.List; import java.util.Set; import org.sosy_lab.java_smt.api.*; From 744ca8f85e06eea4e9dc6986a6dbe44549fd72dc Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 3 Sep 2024 19:28:30 +0200 Subject: [PATCH 23/31] Use StringBuilder --- .../com/dat3m/dartagnan/encoding/ProverWithTracker.java | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index a5eb2832f5..4ff6a2e0e8 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -111,14 +111,14 @@ private void write(String content) { } } - private String removeDuplicatedDeclarations(String content) { - String output = ""; + private StringBuilder removeDuplicatedDeclarations(String content) { + StringBuilder builder = new StringBuilder(); for(String line : content.split("\n")) { if(line.contains("declare-fun") && !declarations.add(line)) { continue; } - output += line + "\n"; + builder.append(line + "\n"); } - return output; + return builder; } } From cfcd5ad4335fd223180364addccb299d2ea6f67d Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 3 Sep 2024 20:01:13 +0200 Subject: [PATCH 24/31] Add some entries for SMT-COMP --- .../dartagnan/encoding/ProverWithTracker.java | 29 +++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index 4ff6a2e0e8..c55cc5d3e1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -6,6 +6,8 @@ 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.Set; @@ -36,9 +38,25 @@ private boolean dump() { } private void init() { + 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)" + ); try { Files.deleteIfExists(Paths.get(fileName)); + 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"); } catch (IOException e) { e.printStackTrace(); } @@ -47,6 +65,7 @@ private void init() { @Override public void close() throws Exception { removeDuplicatedDeclarations(fileName); + write("(exit)\n"); prover.close(); } @@ -58,22 +77,28 @@ public void addConstraint(BooleanFormula f) throws InterruptedException { } public boolean isUnsatWithAssumptions(Collection fs) throws SolverException, InterruptedException { + boolean result = prover.isUnsatWithAssumptions(fs); + String resultString = result ? "unsat" : "sat"; if(dump()) { write("(push)\n"); for(BooleanFormula f : fs) { write(fmgr.dumpFormula(f).toString()); } + write("(set-info :status " + resultString + ")\n"); write("(check-sat)\n"); write("(pop)\n"); } - return prover.isUnsatWithAssumptions(fs); + return result; } public boolean isUnsat() throws SolverException, InterruptedException { + boolean result = prover.isUnsat(); + String resultString = result ? "unsat" : "sat"; if(dump()) { + write("(set-info :status " + resultString + ")\n"); write("(check-sat)\n"); } - return prover.isUnsat(); + return result; } public ImmutableMap getStatistics() { From 3e63c14c2b27c50f014ac7055d48d5c25c1e2e06 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 3 Sep 2024 20:37:05 +0200 Subject: [PATCH 25/31] Add mome entries for SMT-COMP --- .../java/com/dat3m/dartagnan/encoding/ProverWithTracker.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index c55cc5d3e1..505f0b339c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -55,8 +55,9 @@ private void init() { Files.deleteIfExists(Paths.get(fileName)); write("(set-info :smt-lib-version 2.6)\n"); write("(set-logic ALL)\n"); - write("(set-info :category industrial)\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"); } catch (IOException e) { e.printStackTrace(); } From 9e02b8106609eeb8e4e06c521eaa0efe3eb32697 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 3 Sep 2024 20:56:58 +0200 Subject: [PATCH 26/31] Add comments to the formula for debugging --- .../com/dat3m/dartagnan/encoding/ProverWithTracker.java | 8 +++++++- .../dartagnan/verification/solving/AssumeSolver.java | 6 ++++++ .../dartagnan/verification/solving/DataRaceSolver.java | 6 +++++- .../dartagnan/verification/solving/RefinementSolver.java | 7 +++++++ 4 files changed, 25 insertions(+), 2 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index 505f0b339c..bbcd533914 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -78,7 +78,9 @@ public void addConstraint(BooleanFormula f) throws InterruptedException { } public boolean isUnsatWithAssumptions(Collection fs) throws SolverException, InterruptedException { + long start = System.currentTimeMillis(); boolean result = prover.isUnsatWithAssumptions(fs); + long end = System.currentTimeMillis(); String resultString = result ? "unsat" : "sat"; if(dump()) { write("(push)\n"); @@ -87,17 +89,21 @@ public boolean isUnsatWithAssumptions(Collection fs) throws Solv } write("(set-info :status " + resultString + ")\n"); write("(check-sat)\n"); + write("; Original solving time: " + (end - start) + " ms"); write("(pop)\n"); } return result; } public boolean isUnsat() throws SolverException, InterruptedException { + long start = System.currentTimeMillis(); boolean result = prover.isUnsat(); + long end = System.currentTimeMillis(); String resultString = result ? "unsat" : "sat"; if(dump()) { write("(set-info :status " + resultString + ")\n"); write("(check-sat)\n"); + write("; Original solving time: " + (end - start) + " ms"); } return result; } @@ -124,7 +130,7 @@ public void pop() { prover.pop(); } - private void write(String content) { + public void write(String content) { File file = new File(fileName); FileWriter writer; try { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java index 38b18925ec..1be7c04431 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java @@ -55,21 +55,27 @@ private void run() throws InterruptedException, SolverException, InvalidConfigur SymmetryEncoder symmetryEncoder = SymmetryEncoder.withContext(context); logger.info("Starting encoding using " + ctx.getVersion()); + prover.write("; Program encoding"); prover.addConstraint(programEncoder.encodeFullProgram()); + prover.write("; Memory model encoding"); prover.addConstraint(wmmEncoder.encodeFullMemoryModel()); // For validation this contains information. // For verification graph.encode() just returns ctx.mkTrue() + prover.write("; Witness encoding"); prover.addConstraint(task.getWitness().encode(context)); + prover.write("; 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.write("; Property encoding"); prover.addConstraint(assumedSpec); logger.info("Starting first solver.check()"); if(prover.isUnsatWithAssumptions(singletonList(assumptionLiteral))) { + prover.write("; Bound encoding"); prover.addConstraint(propertyEncoder.encodeBoundEventExec()); logger.info("Starting second solver.check()"); res = prover.isUnsat()? PASS : Result.UNKNOWN; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java index c0d9b136ca..f65ee724a2 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java @@ -59,16 +59,20 @@ private void run() throws InterruptedException, SolverException, InvalidConfigur SymmetryEncoder symmetryEncoder = SymmetryEncoder.withContext(context); logger.info("Starting encoding using " + ctx.getVersion()); + prover.write("; Program encoding"); prover.addConstraint(programEncoder.encodeFullProgram()); + prover.write("; Memory model encoding"); prover.addConstraint(wmmEncoder.encodeFullMemoryModel()); + prover.write("; Symmetry breaking encoding"); prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking()); prover.push(); - + prover.write("; Property encoding"); prover.addConstraint(propertyEncoder.encodeProperties(EnumSet.of(Property.DATARACEFREEDOM))); logger.info("Starting first solver.check()"); if(prover.isUnsat()) { prover.pop(); + prover.write("; Bound encoding"); prover.addConstraint(propertyEncoder.encodeBoundEventExec()); logger.info("Starting second solver.check()"); res = prover.isUnsat() ? PASS : UNKNOWN; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java index 94684794f8..87a33ea18a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java @@ -224,8 +224,11 @@ private void runInternal(SolverContext ctx, ProverWithTracker prover, Verificati final Property.Type propertyType = Property.getCombinedType(task.getProperty(), task); logger.info("Starting encoding using " + ctx.getVersion()); + prover.write("; Program encoding"); prover.addConstraint(programEncoder.encodeFullProgram()); + prover.write("; Memory model (baseline) encoding"); prover.addConstraint(baselineEncoder.encodeFullMemoryModel()); + prover.write("; Symmetry breaking encoding"); prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking()); // ------------------------ Solving ------------------------ @@ -233,6 +236,7 @@ private void runInternal(SolverContext ctx, ProverWithTracker prover, Verificati logger.info("Checking target property."); prover.push(); + prover.write("; 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, ProverWithTracker prover, Verificati logger.info("Checking unrolling bounds."); final long lastTime = System.currentTimeMillis(); prover.pop(); + prover.write("; Bound encoding"); prover.addConstraint(propertyEncoder.encodeBoundEventExec()); // Add back the refinement clauses we already found, hoping that this improves the performance. + prover.write("; Refinement encoding"); prover.addConstraint(bmgr.and(propertyTrace.getRefinementFormulas())); final RefinementTrace boundTrace = runRefinement(task, prover, solver, refiner); boundCheckTime = System.currentTimeMillis() - lastTime; @@ -455,6 +461,7 @@ private RefinementIteration doRefinementIteration(ProverWithTracker prover, WMMS inconsistencyReasons = solverResult.getCoreReasons(); lastTime = System.currentTimeMillis(); refinementFormula = refiner.refine(inconsistencyReasons, context); + prover.write("; Refinement encoding"); prover.addConstraint(refinementFormula); refineTime = (System.currentTimeMillis() - lastTime); } From 9bf96e20e82c997fc8d2f8a0b60e0dacbf4c10f8 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 3 Sep 2024 23:29:20 +0200 Subject: [PATCH 27/31] Guard operations --- .../dartagnan/encoding/ProverWithTracker.java | 78 ++++++++++--------- 1 file changed, 41 insertions(+), 37 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index bbcd533914..0edebd38d5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -38,35 +38,39 @@ private boolean dump() { } private void init() { - 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)" - ); - try { - Files.deleteIfExists(Paths.get(fileName)); - 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"); - } catch (IOException e) { - e.printStackTrace(); + if(dump()) { + 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)" + ); + try { + Files.deleteIfExists(Paths.get(fileName)); + 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"); + } catch (IOException e) { + e.printStackTrace(); + } } } @Override public void close() throws Exception { - removeDuplicatedDeclarations(fileName); - write("(exit)\n"); + if(dump()) { + removeDuplicatedDeclarations(fileName); + write("(exit)\n"); + } prover.close(); } @@ -81,13 +85,12 @@ public boolean isUnsatWithAssumptions(Collection fs) throws Solv long start = System.currentTimeMillis(); boolean result = prover.isUnsatWithAssumptions(fs); long end = System.currentTimeMillis(); - String resultString = result ? "unsat" : "sat"; if(dump()) { write("(push)\n"); for(BooleanFormula f : fs) { write(fmgr.dumpFormula(f).toString()); } - write("(set-info :status " + resultString + ")\n"); + write("(set-info :status " + (result ? "unsat" : "sat") + ")\n"); write("(check-sat)\n"); write("; Original solving time: " + (end - start) + " ms"); write("(pop)\n"); @@ -99,9 +102,8 @@ public boolean isUnsat() throws SolverException, InterruptedException { long start = System.currentTimeMillis(); boolean result = prover.isUnsat(); long end = System.currentTimeMillis(); - String resultString = result ? "unsat" : "sat"; if(dump()) { - write("(set-info :status " + resultString + ")\n"); + write("(set-info :status " + (result ? "unsat" : "sat") + ")\n"); write("(check-sat)\n"); write("; Original solving time: " + (end - start) + " ms"); } @@ -131,15 +133,17 @@ public void pop() { } public void write(String content) { - File file = new File(fileName); - FileWriter writer; - try { - writer = new FileWriter(file, true); - PrintWriter printer = new PrintWriter(writer); - printer.append(removeDuplicatedDeclarations(content)); - printer.close(); - } catch (IOException e) { - e.printStackTrace(); + if(dump()) { + File file = new File(fileName); + FileWriter writer; + try { + writer = new FileWriter(file, true); + PrintWriter printer = new PrintWriter(writer); + printer.append(removeDuplicatedDeclarations(content)); + printer.close(); + } catch (IOException e) { + e.printStackTrace(); + } } } From 42244ada37af8e0b07317b01e1e20fe6a38263e1 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Wed, 4 Sep 2024 09:42:52 +0200 Subject: [PATCH 28/31] Fix ui package --- ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 6f2f6e622b..890aa30d4b 100644 --- a/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java +++ b/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java @@ -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); From 562d1747627501c3aa9b37f25e22225878a5aabc Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Thu, 5 Sep 2024 10:43:35 +0200 Subject: [PATCH 29/31] Feedback implemented --- .../java/com/dat3m/dartagnan/Dartagnan.java | 9 +- .../dartagnan/encoding/ProverWithTracker.java | 65 ++++++++---- .../verification/solving/AssumeSolver.java | 12 +-- .../verification/solving/DataRaceSolver.java | 100 +++++++++--------- .../verification/solving/ModelChecker.java | 4 +- .../solving/RefinementSolver.java | 14 +-- .../witness/graphml/WitnessBuilder.java | 8 +- .../compilation/AbstractCompilationTest.java | 1 - 8 files changed, 119 insertions(+), 94 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 3cb97bdef5..161486f7cd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -43,6 +43,7 @@ import org.sosy_lab.common.log.BasicLogManager; import org.sosy_lab.java_smt.SolverContextFactory; import org.sosy_lab.java_smt.api.Model; +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 org.sosy_lab.java_smt.api.SolverException; @@ -210,7 +211,7 @@ public static void main(String[] args) throws Exception { } } - public static File generateExecutionGraphFile(VerificationTask task, ProverWithTracker prover, ModelChecker modelChecker, + 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."); @@ -231,7 +232,7 @@ public static File generateExecutionGraphFile(VerificationTask task, ProverWithT synContext, witnessType.convertToPng()); } - private static void generateWitnessIfAble(VerificationTask task, ProverWithTracker prover, + private static void generateWitnessIfAble(VerificationTask task, ProverEnvironment prover, ModelChecker modelChecker, String summary) { // ------------------ Generate Witness, if possible ------------------ final EnumSet properties = task.getProperty(); @@ -250,7 +251,7 @@ private static void generateWitnessIfAble(VerificationTask task, ProverWithTrack } } - public static String generateResultSummary(VerificationTask task, ProverWithTracker prover, + public static String generateResultSummary(VerificationTask task, ProverEnvironment prover, ModelChecker modelChecker) throws SolverException { // ----------------- Generate output of verification result ----------------- final Program p = task.getProgram(); @@ -388,7 +389,7 @@ public static String generateResultSummary(VerificationTask task, ProverWithTrac return summary.toString(); } - private static void printWarningIfThreadStartFailed(Program p, EncodingContext encoder, ProverWithTracker prover) + private static void printWarningIfThreadStartFailed(Program p, EncodingContext encoder, ProverEnvironment prover) throws SolverException { for (Event e : p.getThreadEvents()) { if (e.hasTag(Tag.STARTLOAD) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index 0edebd38d5..d2d007d9f7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -10,6 +10,8 @@ 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.*; @@ -17,7 +19,7 @@ import com.google.common.collect.ImmutableMap; -public class ProverWithTracker implements AutoCloseable { +public class ProverWithTracker implements ProverEnvironment { private final FormulaManager fmgr; private final ProverEnvironment prover; @@ -39,6 +41,11 @@ private boolean dump() { 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"); @@ -52,21 +59,16 @@ private void init() { "- Thomas Haas, Roland Meyer, Hernán Ponce de León: " + "CAAT: consistency as a theory. Proc. ACM Program. Lang. 6(OOPSLA2): 114-144 (2022)" ); - try { - Files.deleteIfExists(Paths.get(fileName)); - 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"); - } catch (IOException e) { - e.printStackTrace(); - } + 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() throws Exception { + public void close() { if(dump()) { removeDuplicatedDeclarations(fileName); write("(exit)\n"); @@ -74,11 +76,11 @@ public void close() throws Exception { prover.close(); } - public void addConstraint(BooleanFormula f) throws InterruptedException { + public Void addConstraint(BooleanFormula f) throws InterruptedException { if(dump()) { write(fmgr.dumpFormula(f).toString()); } - prover.addConstraint(f); + return prover.addConstraint(f); } public boolean isUnsatWithAssumptions(Collection fs) throws SolverException, InterruptedException { @@ -132,13 +134,11 @@ public void pop() { prover.pop(); } - public void write(String content) { - if(dump()) { + private void write(String content) { + if (dump()) { File file = new File(fileName); - FileWriter writer; - try { - writer = new FileWriter(file, true); - PrintWriter printer = new PrintWriter(writer); + try (FileWriter writer = new FileWriter(file, true); + PrintWriter printer = new PrintWriter(writer)) { printer.append(removeDuplicatedDeclarations(content)); printer.close(); } catch (IOException e) { @@ -147,6 +147,10 @@ public void write(String content) { } } + public void writeComment(String content) { + write("; " + content); + } + private StringBuilder removeDuplicatedDeclarations(String content) { StringBuilder builder = new StringBuilder(); for(String line : content.split("\n")) { @@ -157,4 +161,25 @@ private StringBuilder removeDuplicatedDeclarations(String content) { } return builder; } + + @Override + public R allSat(AllSatCallback arg0, List arg1) throws InterruptedException, SolverException { + return prover.allSat(arg0, arg1); + } + + @Override + public List getUnsatCore() { + return prover.getUnsatCore(); + } + + @Override + public int size() { + return prover.size(); + } + + @Override + public Optional> unsatCoreOverAssumptions(Collection arg0) + throws SolverException, InterruptedException { + return prover.unsatCoreOverAssumptions(arg0); + } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java index 1be7c04431..a8108aa9f1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java @@ -55,27 +55,27 @@ private void run() throws InterruptedException, SolverException, InvalidConfigur SymmetryEncoder symmetryEncoder = SymmetryEncoder.withContext(context); logger.info("Starting encoding using " + ctx.getVersion()); - prover.write("; Program encoding"); + prover.writeComment("Program encoding"); prover.addConstraint(programEncoder.encodeFullProgram()); - prover.write("; Memory model encoding"); + prover.writeComment("Memory model encoding"); prover.addConstraint(wmmEncoder.encodeFullMemoryModel()); // For validation this contains information. // For verification graph.encode() just returns ctx.mkTrue() - prover.write("; Witness encoding"); + prover.writeComment("Witness encoding"); prover.addConstraint(task.getWitness().encode(context)); - prover.write("; Symmetry breaking encoding"); + 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.write("; Property encoding"); + prover.writeComment("Property encoding"); prover.addConstraint(assumedSpec); logger.info("Starting first solver.check()"); if(prover.isUnsatWithAssumptions(singletonList(assumptionLiteral))) { - prover.write("; Bound encoding"); + prover.writeComment("Bound encoding"); prover.addConstraint(propertyEncoder.encodeBoundEventExec()); logger.info("Starting second solver.check()"); res = prover.isUnsat()? PASS : Result.UNKNOWN; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java index f65ee724a2..0941215cc3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java @@ -18,67 +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 ProverWithTracker prover; - private final VerificationTask task; + private final SolverContext ctx; + private final ProverWithTracker prover; + private final VerificationTask task; - private DataRaceSolver(SolverContext c, ProverWithTracker 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, ProverWithTracker 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.write("; Program encoding"); - prover.addConstraint(programEncoder.encodeFullProgram()); - prover.write("; Memory model encoding"); - prover.addConstraint(wmmEncoder.encodeFullMemoryModel()); - prover.write("; Symmetry breaking encoding"); - prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking()); - prover.push(); - prover.write("; Property encoding"); - 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.write("; Bound encoding"); - 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); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java index 3b657a1ff3..cac688c576 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java @@ -2,7 +2,6 @@ import com.dat3m.dartagnan.configuration.Property; import com.dat3m.dartagnan.encoding.EncodingContext; -import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.encoding.WmmEncoder; import com.dat3m.dartagnan.exception.UnsatisfiedRequirementException; import com.dat3m.dartagnan.program.Program; @@ -22,6 +21,7 @@ import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverException; import java.util.Optional; @@ -109,7 +109,7 @@ public static void performStaticWmmAnalyses(VerificationTask task, Context analy analysisContext.register(RelationAnalysis.class, RelationAnalysis.fromConfig(task, analysisContext, config)); } - protected void saveFlaggedPairsOutput(Wmm wmm, WmmEncoder encoder, ProverWithTracker prover, EncodingContext ctx, Program program) throws SolverException { + protected void saveFlaggedPairsOutput(Wmm wmm, WmmEncoder encoder, ProverEnvironment prover, EncodingContext ctx, Program program) throws SolverException { if (!ctx.getTask().getProperty().contains(CAT_SPEC)) { return; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java index 87a33ea18a..bce614c3ba 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java @@ -224,11 +224,11 @@ private void runInternal(SolverContext ctx, ProverWithTracker prover, Verificati final Property.Type propertyType = Property.getCombinedType(task.getProperty(), task); logger.info("Starting encoding using " + ctx.getVersion()); - prover.write("; Program encoding"); + prover.writeComment("Program encoding"); prover.addConstraint(programEncoder.encodeFullProgram()); - prover.write("; Memory model (baseline) encoding"); + prover.writeComment("Memory model (baseline) encoding"); prover.addConstraint(baselineEncoder.encodeFullMemoryModel()); - prover.write("; Symmetry breaking encoding"); + prover.writeComment("Symmetry breaking encoding"); prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking()); // ------------------------ Solving ------------------------ @@ -236,7 +236,7 @@ private void runInternal(SolverContext ctx, ProverWithTracker prover, Verificati logger.info("Checking target property."); prover.push(); - prover.write("; Property encoding"); + prover.writeComment("Property encoding"); prover.addConstraint(propertyEncoder.encodeProperties(task.getProperty())); final RefinementTrace propertyTrace = runRefinement(task, prover, solver, refiner); @@ -269,10 +269,10 @@ private void runInternal(SolverContext ctx, ProverWithTracker prover, Verificati logger.info("Checking unrolling bounds."); final long lastTime = System.currentTimeMillis(); prover.pop(); - prover.write("; Bound encoding"); + prover.writeComment("Bound encoding"); prover.addConstraint(propertyEncoder.encodeBoundEventExec()); // Add back the refinement clauses we already found, hoping that this improves the performance. - prover.write("; Refinement encoding"); + prover.writeComment("Refinement encoding"); prover.addConstraint(bmgr.and(propertyTrace.getRefinementFormulas())); final RefinementTrace boundTrace = runRefinement(task, prover, solver, refiner); boundCheckTime = System.currentTimeMillis() - lastTime; @@ -461,7 +461,7 @@ private RefinementIteration doRefinementIteration(ProverWithTracker prover, WMMS inconsistencyReasons = solverResult.getCoreReasons(); lastTime = System.currentTimeMillis(); refinementFormula = refiner.refine(inconsistencyReasons, context); - prover.write("; Refinement encoding"); + prover.writeComment("Refinement encoding"); prover.addConstraint(refinementFormula); refineTime = (System.currentTimeMillis() - lastTime); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java index e00580645e..7e71e3baac 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java @@ -1,7 +1,6 @@ package com.dat3m.dartagnan.witness.graphml; import com.dat3m.dartagnan.encoding.EncodingContext; -import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.expression.booleans.BoolLiteral; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Thread; @@ -17,6 +16,7 @@ import org.sosy_lab.common.configuration.Option; import org.sosy_lab.common.configuration.Options; import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverException; import java.io.File; @@ -40,7 +40,7 @@ public class WitnessBuilder { private final EncodingContext context; - private final ProverWithTracker prover; + private final ProverEnvironment prover; private final String type; private final String ltlProperty; @@ -60,14 +60,14 @@ public boolean canBeBuilt() { private final Map eventThreadMap = new HashMap<>(); - private WitnessBuilder(EncodingContext c, ProverWithTracker p, Result r, String summary) { + private WitnessBuilder(EncodingContext c, ProverEnvironment p, Result r, String summary) { context = checkNotNull(c); prover = checkNotNull(p); type = r.equals(FAIL) ? "violation" : "correctness"; ltlProperty = getLtlPropertyFromSummary(summary); } - public static WitnessBuilder of(EncodingContext context, ProverWithTracker prover, Result result, + public static WitnessBuilder of(EncodingContext context, ProverEnvironment prover, Result result, String ltlProperty) throws InvalidConfigurationException { WitnessBuilder b = new WitnessBuilder(context, prover, result, ltlProperty); context.getTask().getConfig().inject(b); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java index 4ca30a5d84..f0d6f31d2a 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java @@ -20,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; From 0fdb1945f0505d715e499e1c94675f37663d397d Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Thu, 5 Sep 2024 17:20:05 +0200 Subject: [PATCH 30/31] Feedback implemented --- .../dartagnan/encoding/ProverWithTracker.java | 67 ++++++++++++------- 1 file changed, 41 insertions(+), 26 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index d2d007d9f7..c9046bdb16 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -76,6 +76,7 @@ public void close() { prover.close(); } + @Override public Void addConstraint(BooleanFormula f) throws InterruptedException { if(dump()) { write(fmgr.dumpFormula(f).toString()); @@ -83,23 +84,31 @@ public Void addConstraint(BooleanFormula f) throws InterruptedException { return prover.addConstraint(f); } + @Override public boolean isUnsatWithAssumptions(Collection fs) throws SolverException, InterruptedException { - long start = System.currentTimeMillis(); - boolean result = prover.isUnsatWithAssumptions(fs); - long end = System.currentTimeMillis(); + 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"); - write("; Original solving time: " + (end - start) + " ms"); + 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(); @@ -107,19 +116,22 @@ public boolean isUnsat() throws SolverException, InterruptedException { if(dump()) { write("(set-info :status " + (result ? "unsat" : "sat") + ")\n"); write("(check-sat)\n"); - write("; Original solving time: " + (end - start) + " ms"); + writeComment("Original solving time: " + (end - start) + " ms"); } return result; } + @Override public ImmutableMap getStatistics() { return prover.getStatistics(); } + @Override public Model getModel() throws SolverException { return prover.getModel(); } + @Override public void push() throws InterruptedException { if(dump()) { write("(push)\n"); @@ -127,6 +139,7 @@ public void push() throws InterruptedException { prover.push(); } + @Override public void pop() { if(dump()) { write("(pop)\n"); @@ -134,6 +147,27 @@ public void pop() { prover.pop(); } + @Override + public R allSat(AllSatCallback arg0, List arg1) throws InterruptedException, SolverException { + return prover.allSat(arg0, arg1); + } + + @Override + public List getUnsatCore() { + return prover.getUnsatCore(); + } + + @Override + public int size() { + return prover.size(); + } + + @Override + public Optional> unsatCoreOverAssumptions(Collection arg0) + throws SolverException, InterruptedException { + return prover.unsatCoreOverAssumptions(arg0); + } + private void write(String content) { if (dump()) { File file = new File(fileName); @@ -151,6 +185,8 @@ 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")) { @@ -161,25 +197,4 @@ private StringBuilder removeDuplicatedDeclarations(String content) { } return builder; } - - @Override - public R allSat(AllSatCallback arg0, List arg1) throws InterruptedException, SolverException { - return prover.allSat(arg0, arg1); - } - - @Override - public List getUnsatCore() { - return prover.getUnsatCore(); - } - - @Override - public int size() { - return prover.size(); - } - - @Override - public Optional> unsatCoreOverAssumptions(Collection arg0) - throws SolverException, InterruptedException { - return prover.unsatCoreOverAssumptions(arg0); - } } From f88df3cd1620252dc391877f9a45b8fc22cd3498 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Thu, 5 Sep 2024 18:55:34 +0200 Subject: [PATCH 31/31] Fix merge problems --- .../java/com/dat3m/dartagnan/encoding/ProverWithTracker.java | 2 +- .../com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java | 2 -- .../dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java | 2 -- .../com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java | 2 -- .../com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java | 2 -- .../com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java | 2 -- .../com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java | 2 -- 7 files changed, 1 insertion(+), 13 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index c9046bdb16..24d6ad8be4 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -38,7 +38,7 @@ public ProverWithTracker(SolverContext ctx, String fileName, ProverOptions... op private boolean dump() { return !fileName.isEmpty(); } - + private void init() { if(dump()) { try { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java index 12c1ee3472..24fa6af270 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java @@ -121,8 +121,6 @@ public void testAllSolvers() throws Exception { } } - - private SolverContext mkCtx() throws InvalidConfigurationException { Configuration cfg = Configuration.builder().build(); return SolverContextFactory.createSolverContext( diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java index e6bad36190..6625246101 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java @@ -122,8 +122,6 @@ public void testAllSolvers() throws Exception { } } - - private SolverContext mkCtx() throws InvalidConfigurationException { Configuration cfg = Configuration.builder().build(); return SolverContextFactory.createSolverContext( diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java index 6a48e623b8..0efe8060ed 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java @@ -126,8 +126,6 @@ public void testAllSolvers() throws Exception { } } - - private SolverContext mkCtx() throws InvalidConfigurationException { Configuration cfg = Configuration.builder().build(); return SolverContextFactory.createSolverContext( diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java index 220ff58563..b6ee1d618c 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java @@ -127,8 +127,6 @@ public void testAllSolvers() throws Exception { } } - - private SolverContext mkCtx() throws InvalidConfigurationException { Configuration cfg = Configuration.builder().build(); return SolverContextFactory.createSolverContext( diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java index 6193a237ff..0cbb610e7d 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java @@ -354,8 +354,6 @@ public void testAllSolvers() throws Exception { } } - - private SolverContext mkCtx() throws InvalidConfigurationException { Configuration cfg = Configuration.builder().build(); return SolverContextFactory.createSolverContext( diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java index 6e40026aa9..2493d31e92 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java @@ -354,8 +354,6 @@ public void testAllSolvers() throws Exception { } } - - private SolverContext mkCtx() throws InvalidConfigurationException { Configuration cfg = Configuration.builder().build(); return SolverContextFactory.createSolverContext(