From 5f2c3f5afde6aa1f9c47204764f6efc20c683189 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Fri, 13 Sep 2024 12:27:57 +0200 Subject: [PATCH] Implemented feedback --- .../java/com/dat3m/dartagnan/Dartagnan.java | 2 - .../dartagnan/configuration/OptionNames.java | 2 +- .../dartagnan/encoding/ProgramEncoder.java | 7 +- .../dartagnan/utils/options/BaseOptions.java | 102 +++++++++++------- .../verification/VerificationTask.java | 2 +- 5 files changed, 67 insertions(+), 48 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 0f1e66ce09..11d0695819 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -118,8 +118,6 @@ public static void main(String[] args) throws Exception { .orElseThrow(() -> new IllegalArgumentException("CAT model not given or format not recognized"))); logger.info("CAT file path: " + fileModel); - logger.info("Progress model: " + o.getProgressModel()); - Wmm mcm = new ParserCat().parse(fileModel); Program p = new ProgramParser().parse(fileProgram); EnumSet properties = o.getProperty(); 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 bc92c82af1..b4aeef42c3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java @@ -8,7 +8,6 @@ public class OptionNames { public static final String TARGET = "target"; public static final String METHOD = "method"; public static final String SOLVER = "solver"; - public static final String PROGRESSMODEL = "progressModel"; public static final String TIMEOUT = "timeout"; public static final String VALIDATE = "validate"; public static final String COVERAGE = "coverage"; @@ -16,6 +15,7 @@ public class OptionNames { public static final String SMTLIB2 = "smtlib2"; // Modeling Options + public static final String PROGRESSMODEL = "modeling.progress"; public static final String THREAD_CREATE_ALWAYS_SUCCEEDS = "modeling.threadCreateAlwaysSucceeds"; public static final String RECURSION_BOUND = "modeling.recursionBound"; public static final String MEMORY_IS_ZEROED = "modeling.memoryIsZeroed"; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java index 8752954361..2836d3cf57 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java @@ -133,10 +133,8 @@ private BooleanFormula threadHasStarted(Thread thread) { private BooleanFormula threadHasTerminated(Thread thread) { final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); return bmgr.and( - context.execution(thread.getExit()), + context.execution(thread.getExit()), // Also guarantees that we are not stuck in a barrier bmgr.not(threadIsStuckInLoop(thread)) - // The following is not needed since the first condition already implies this - // bmgr.not(threadIsStuckInBarrier(thread)) ); } @@ -445,8 +443,7 @@ private BooleanFormula encodeFairForwardProgress(Thread thread) { // For every event in the cf a successor will be in the cf (unless a barrier is blocking). for (Event cur : thread.getEvents()) { - if (cur.getSuccessor() == null) { - assert cur == thread.getExit(); + if (cur == thread.getExit()) { break; } final List succs = new ArrayList<>(); 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 049e3cbab6..c121bd263d 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 @@ -16,71 +16,95 @@ public abstract class BaseOptions { @Option( - name=PROPERTY, - description="The property to check for: reachability (default), liveness, races.", - toUppercase=true) + name = PROPERTY, + description = "A combination of properties to check for: program_spec, liveness, cat_spec (defaults to all).", + toUppercase = true) private EnumSet property = Property.getDefault(); - public EnumSet getProperty() { return property; } + public EnumSet getProperty() { + return property; + } @Option( - name=PROGRESSMODEL, - description="The progress model to assume: fair (default), HSA, OBE, unfair", - toUppercase=true) + name = PROGRESSMODEL, + description = "The progress model to assume: fair (default), hsa, obe, unfair", + toUppercase = true) private ProgressModel progressModel = ProgressModel.getDefault(); - public ProgressModel getProgressModel() { return progressModel; } + public ProgressModel getProgressModel() { + return progressModel; + } @Option( - name=VALIDATE, - description="Performs violation witness validation. Argument is the path to the witness file.") + name = VALIDATE, + description = "Performs violation witness validation. Argument is the path to the witness file.") private String witnessPath; - public boolean runValidator() { return witnessPath != null; } - public String getWitnessPath() { return witnessPath; } + public boolean runValidator() { + return witnessPath != null; + } + + public String getWitnessPath() { + return witnessPath; + } @Option( - name=METHOD, - description="Solver method to be used.", - toUppercase=true) - private Method method=Method.getDefault(); + name = METHOD, + description = "Solver method to be used.", + toUppercase = true) + private Method method = Method.getDefault(); - public Method getMethod() { return method; } + public Method getMethod() { + return method; + } @Option( - name=SOLVER, - description="Uses the specified SMT solver as a backend.", - toUppercase=true) - private Solvers solver=Solvers.Z3; + name = SOLVER, + description = "Uses the specified SMT solver as a backend.", + toUppercase = true) + private Solvers solver = Solvers.Z3; - public Solvers getSolver() { return solver; } + public Solvers getSolver() { + return solver; + } @Option( - name=TIMEOUT, - description="Timeout (in secs) before interrupting the SMT solver.") - private int timeout=0; + name = TIMEOUT, + description = "Timeout (in secs) before interrupting the SMT solver.") + private int timeout = 0; + + public boolean hasTimeout() { + return timeout > 0; + } - public boolean hasTimeout() { return timeout > 0; } - public int getTimeout() { return timeout; } + public int getTimeout() { + return timeout; + } @Option( - name=PHANTOM_REFERENCES, - description="Decrease references on Z3 formula objects once they are no longer referenced.") - private boolean phantomReferences=true; + name = PHANTOM_REFERENCES, + description = "Decrease references on Z3 formula objects once they are no longer referenced.") + private boolean phantomReferences = true; - public boolean usePhantomReferences() { return phantomReferences; } + public boolean usePhantomReferences() { + return phantomReferences; + } @Option( - name=WITNESS, - description="Type of the violation graph to generate in the output directory.") - private WitnessType witnessType=WitnessType.getDefault(); + name = WITNESS, + description = "Type of the violation graph to generate in the output directory.") + private WitnessType witnessType = WitnessType.getDefault(); - public WitnessType getWitnessType() { return witnessType; } + public WitnessType getWitnessType() { + return witnessType; + } @Option( - name=SMTLIB2, - description="Dump encoding to an SMTLIB2 file.") - private boolean smtlib=false; + name = SMTLIB2, + description = "Dump encoding to an SMTLIB2 file.") + private boolean smtlib = false; - public boolean getDumpSmtLib() { return smtlib; } + public boolean getDumpSmtLib() { + return smtlib; + } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/VerificationTask.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/VerificationTask.java index 3e4430bc8b..f4556354fd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/VerificationTask.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/VerificationTask.java @@ -34,7 +34,7 @@ protected VerificationTask(Program program, Wmm memoryModel, ProgressModel progr throws InvalidConfigurationException { this.program = checkNotNull(program); this.memoryModel = checkNotNull(memoryModel); - this.progressModel = progressModel; + this.progressModel = checkNotNull(progressModel); this.property = checkNotNull(property); this.witness = checkNotNull(witness); this.config = checkNotNull(config);