diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 83778ae18e..e86f78855f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -35,7 +35,6 @@ import com.dat3m.dartagnan.witness.graphml.WitnessGraph; import com.dat3m.dartagnan.wmm.Wmm; import com.dat3m.dartagnan.wmm.axiom.Axiom; - import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableSet; import com.google.common.io.CharSource; @@ -83,6 +82,11 @@ private Dartagnan(Configuration config) throws InvalidConfigurationException { config.recursiveInject(this); } + static { + // Register type converters globally + Configuration.getDefaultConverters().put(ProgressModel.Hierarchy.class, ProgressModel.HIERARCHY_CONVERTER); + } + private static Configuration loadConfiguration(String[] args) throws InvalidConfigurationException, IOException { final var preamble = new StringBuilder(); final var options = new StringBuilder(); @@ -95,7 +99,6 @@ private static Configuration loadConfiguration(String[] args) throws InvalidConf } final CharSource source = CharSource.concat(CharSource.wrap(preamble), CharSource.wrap(options)); return Configuration.builder() - .addConverter(ProgressModel.Hierarchy.class, ProgressModel.HIERARCHY_CONVERTER) .loadFromSource(source, ".", ".") .build(); } @@ -146,10 +149,11 @@ public static void main(String[] args) throws Exception { p.setEntrypoint(new Entrypoint.Simple(p.getFunctionByName(o.getEntryFunction()).orElseThrow( () -> new MalformedProgramException(String.format("Program has no function named %s. Select a different entry point.", o.getEntryFunction()))))); } + p.injectConfig(config); + final Wmm mcm = new ParserCat(Path.of(o.getCatIncludePath())).parse(fileModel); final VerificationTaskBuilder builder = VerificationTask.builder() .withConfig(config) - .withProgressModel(o.getProgressModel()) .withWitness(witness); // If the arch has been set during parsing (this only happens for litmus tests) // and the user did not explicitly add the target option, we use the one diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/ProgressModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/ProgressModel.java index e0fb195e3f..5740ccbd90 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/ProgressModel.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/ProgressModel.java @@ -6,6 +6,7 @@ import com.google.common.collect.Maps; import com.google.common.reflect.TypeToken; import org.checkerframework.checker.nullness.qual.Nullable; +import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.configuration.converters.TypeConverter; import org.sosy_lab.common.log.LogManager; @@ -78,12 +79,27 @@ public ProgressModel getDefaultProgress() { @Override public String toString() { - if (scope2Progress.isEmpty()) { + if (isUniform()) { return defaultProgress.toString(); } else { return scope2Progress + " with default=" + defaultProgress; } } + + public String toOptionString() { + if (isUniform()) { + return defaultProgress.toString(); + } else { + StringBuilder builder = new StringBuilder(); + builder.append("["); + scope2Progress.entrySet().stream() + .map(e -> e.getKey() + "=" + e.getValue().toString()) + .forEach(builder::append); + builder.append(", default=").append(defaultProgress.toString()); + builder.append("]"); + return builder.toString(); + } + } } // ================================================================================================================ @@ -141,4 +157,9 @@ public String toString() { return value; } }; + + static { + // Register type converter globally + Configuration.getDefaultConverters().put(ProgressModel.Hierarchy.class, ProgressModel.HIERARCHY_CONVERTER); + } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java index 55768372ba..a16cd52653 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java @@ -24,7 +24,6 @@ import com.dat3m.dartagnan.wmm.axiom.Acyclicity; import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; import com.google.common.collect.Iterables; - import org.slf4j.Logger; import org.slf4j.LoggerFactory; import org.sosy_lab.common.configuration.InvalidConfigurationException; @@ -32,20 +31,14 @@ import org.sosy_lab.common.configuration.Options; import org.sosy_lab.java_smt.api.*; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; -import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; -import java.util.Collection; -import java.util.HashMap; -import java.util.LinkedHashSet; -import java.util.List; -import java.util.Map; +import java.util.*; import static com.dat3m.dartagnan.configuration.OptionNames.*; import static com.dat3m.dartagnan.program.event.Tag.INIT; import static com.dat3m.dartagnan.program.event.Tag.WRITE; import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkNotNull; -import static org.sosy_lab.java_smt.api.FloatingPointRoundingMode.*; @Options public final class EncodingContext { @@ -80,13 +73,6 @@ public final class EncodingContext { secure = true) boolean useIntegers = false; - // TODO: If we ever simplify floats, this option will play a role there besides than the encoding. - // If that is the case we need to move this option outside of this encoding class. - @Option(name = ROUNDING_MODE_FLOATS, - description = "Rounding mode for floating point operations.", - secure = true) - FloatingPointRoundingMode roundingModeFloats = NEAREST_TIES_TO_EVEN; - private final Map controlFlowVariables = new HashMap<>(); private final Map executionVariables = new HashMap<>(); private final Map syncVariables = new HashMap<>(); @@ -128,7 +114,7 @@ public static EncodingContext of(VerificationTask task, Context analysisContext, task.getConfig().inject(context); logger.info("{}: {}", IDL_TO_SAT, context.useSATEncoding); logger.info("{}: {}", MERGE_CF_VARS, context.shouldMergeCFVars); - logger.info("{}: {}", ROUNDING_MODE_FLOATS, context.roundingModeFloats); + logger.info("{}: {}", ROUNDING_MODE_FLOATS, context.getTask().getProgram().getFloatRoundingMode()); context.initialize(); if (logger.isInfoEnabled()) { logger.info("Number of encoded edges for acyclicity: {}", @@ -336,7 +322,7 @@ private void initialize() { // Only for the standard fair progress model we can merge CF variables. // TODO: It would also be possible for OBE/HSA in some cases if we refine the cf-equivalence classes // to classes per thread. - final boolean mergeCFVars = shouldMergeCFVars && verificationTask.getProgressModel().isFair(); + final boolean mergeCFVars = shouldMergeCFVars && verificationTask.getProgram().getProgressModel().isFair(); if (mergeCFVars) { for (BranchEquivalence.Class cls : analysisContext.get(BranchEquivalence.class).getAllEquivalenceClasses()) { BooleanFormula v = booleanFormulaManager.makeVariable("cf " + cls.getRepresentative().getGlobalId()); 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 2c922b6a5d..6a167eb3be 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java @@ -45,11 +45,15 @@ public class ExpressionEncoder { private final FormulaManagerExt fmgr; private final BooleanFormulaManager bmgr; private final Visitor visitor = new Visitor(); + + private final FloatingPointRoundingMode roundingMode; ExpressionEncoder(EncodingContext context) { this.context = context; this.fmgr = context.getFormulaManager(); this.bmgr = fmgr.getBooleanFormulaManager(); + + this.roundingMode = context.getTask().getProgram().getFloatRoundingMode(); } private IntegerFormulaManager integerFormulaManager() { @@ -543,7 +547,7 @@ public TypedFormula visitIntCmpExpression(IntCmpExp final Formula operand = encodeIntegerExpr(expr.getOperand()).formula(); final FloatType fType = expr.getTargetType(); final FloatingPointType targetType = getFloatFormulaType(fType); - final Formula enc = floatingPointFormulaManager().castFrom(operand, true, targetType, context.roundingModeFloats); + final Formula enc = floatingPointFormulaManager().castFrom(operand, true, targetType, roundingMode); return new TypedFormula<>(fType, enc); } @@ -561,7 +565,7 @@ public TypedFormula visitIntCmpExpression(IntCmpExp } else if (floatLiteral.isMinusInf()) { result = floatingPointFormulaManager().makeMinusInfinity(fFType); } else { - result = floatingPointFormulaManager().makeNumber(floatLiteral.getValue(), fFType, context.roundingModeFloats); + result = floatingPointFormulaManager().makeNumber(floatLiteral.getValue(), fFType, roundingMode); } return new TypedFormula<>(floatLiteral.getType(), result); } @@ -575,10 +579,10 @@ public TypedFormula visitIntCmpExpression(IntCmpExp final FloatingPointFormulaManager fpmgr = floatingPointFormulaManager(); final FloatingPointFormula result = switch (fBin.getKind()) { - case FADD -> fpmgr.add(fp1, fp2, context.roundingModeFloats); - case FSUB -> fpmgr.subtract(fp1, fp2, context.roundingModeFloats); - case FMUL -> fpmgr.multiply(fp1, fp2, context.roundingModeFloats); - case FDIV -> fpmgr.divide(fp1, fp2, context.roundingModeFloats); + case FADD -> fpmgr.add(fp1, fp2, roundingMode); + case FSUB -> fpmgr.subtract(fp1, fp2, roundingMode); + case FMUL -> fpmgr.multiply(fp1, fp2, roundingMode); + case FDIV -> fpmgr.divide(fp1, fp2, roundingMode); case FREM -> fpmgr.remainder(fp1, fp2); case FMAX -> fpmgr.max(fp1, fp2); case FMIN -> fpmgr.min(fp1, fp2); @@ -644,7 +648,7 @@ private BooleanFormula fromUnordToOrd(FloatingPointFormula l, FloatingPointFormu final FloatingPointFormulaManager fpmgr = floatingPointFormulaManager(); final FloatingPointType fType = getFloatFormulaType(expr.getTargetType()); - final Formula enc = fpmgr.castFrom(inner.formula(), true, fType, context.roundingModeFloats); + final Formula enc = fpmgr.castFrom(inner.formula(), true, fType, roundingMode); return new TypedFormula<>(expr.getType(), enc); } 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 916b9f39cb..4b742cc61f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java @@ -22,7 +22,6 @@ import com.dat3m.dartagnan.program.memory.Memory; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.program.misc.NonDetValue; - import com.google.common.base.Preconditions; import com.google.common.base.Verify; import com.google.common.collect.ImmutableList; @@ -192,9 +191,11 @@ private int getWorkgroupId(Thread thread) { } public BooleanFormula encodeControlFlow() { - logger.info("Encoding program control flow with progress model {}", context.getTask().getProgressModel()); - final Program program = context.getTask().getProgram(); + final ProgressModel.Hierarchy progressModel = program.getProgressModel(); + + logger.info("Encoding program control flow with progress model {}", progressModel); + final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); final ForwardProgressEncoder progressEncoder = new ForwardProgressEncoder(); List enc = new ArrayList<>(); @@ -207,7 +208,7 @@ public BooleanFormula encodeControlFlow() { } // Actual forward progress - enc.add(progressEncoder.encodeForwardProgress(program, context.getTask().getProgressModel())); + enc.add(progressEncoder.encodeForwardProgress(program, progressModel)); return bmgr.and(enc); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java index a9fe96555c..b6542d586c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.program; import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.configuration.ProgressModel; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.expression.Type; @@ -12,10 +13,19 @@ import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.program.misc.NonDetValue; import com.google.common.base.Preconditions; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; +import org.sosy_lab.common.configuration.Option; +import org.sosy_lab.common.configuration.Options; +import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; import java.util.*; import java.util.stream.Collectors; +import static com.dat3m.dartagnan.configuration.OptionNames.PROGRESSMODEL; +import static com.dat3m.dartagnan.configuration.OptionNames.ROUNDING_MODE_FLOATS; +import static org.sosy_lab.java_smt.api.FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN; + public class Program { private static final TypeFactory types = TypeFactory.getInstance(); @@ -25,19 +35,45 @@ public enum SourceLanguage { LITMUS, LLVM, SPV } public enum SpecificationType { EXISTS, FORALL, NOT_EXISTS, ASSERT } - private String name; - private SpecificationType specificationType = SpecificationType.ASSERT; - private Expression spec; - private Expression filterSpec; // Acts like "assume" statements, filtering out executions + @Options + private static class SemanticConfig { + @Option(name = ROUNDING_MODE_FLOATS, + description = "Default rounding mode for floating point operations (default NEAREST_TIES_TO_EVEN).", + secure = true) + private FloatingPointRoundingMode floatRoundingMode = NEAREST_TIES_TO_EVEN; + + @Option( + name = PROGRESSMODEL, + description = """ + The progress model to assume: fair (default), hsa, obe, lobe, hsa_obe, unfair. + To specify progress models per scope, use [=,...]. + Defaults to "fair" for unspecified scopes unless "default=" is specified. + """, + toUppercase = true) + private ProgressModel.Hierarchy progressModel = ProgressModel.defaultHierarchy(); + } + + // Shape private final List threads; private final List functions; private final List constants = new ArrayList<>(); private final Memory memory; private Entrypoint entrypoint = new Entrypoint.None(); + + // Semantic options + private final SemanticConfig semanticConfig = new SemanticConfig(); + + // Spec + private SpecificationType specificationType = SpecificationType.ASSERT; + private Expression spec; + private Expression filterSpec; // Acts like "assume" statements, filtering out executions + + // Metadata + private String name; + private final SourceLanguage format; private Arch arch; - private int unrollingBound = 0; private boolean isCompiled; - private final SourceLanguage format; + private int unrollingBound = 0; private int nextThreadId = 0; private int nextConstantId = 0; @@ -128,6 +164,28 @@ public void setFilterSpecification(Expression spec) { this.filterSpec = spec; } + public FloatingPointRoundingMode getFloatRoundingMode() { + return semanticConfig.floatRoundingMode; + } + + public void setFloatRoundingMode(FloatingPointRoundingMode roundingMode) { + this.semanticConfig.floatRoundingMode = roundingMode; + } + + public ProgressModel.Hierarchy getProgressModel() { + return semanticConfig.progressModel; + } + + public void setProgressModel(ProgressModel.Hierarchy progressModel) { + semanticConfig.progressModel = progressModel; + } + + public void injectConfig(Configuration configuration) throws InvalidConfigurationException { + configuration.inject(semanticConfig); + } + + // ----------------------------------------------------------------------------------------------------------------- + public void addThread(Thread t) { threads.add(t); t.setProgram(this); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ExecutionAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ExecutionAnalysis.java index 735d12f110..5c5356d774 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ExecutionAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ExecutionAnalysis.java @@ -18,10 +18,10 @@ public interface ExecutionAnalysis { - static ExecutionAnalysis fromConfig(Program program, ProgressModel.Hierarchy progressModel, Context context, Configuration config) + static ExecutionAnalysis fromConfig(Program program, Context context, Configuration config) throws InvalidConfigurationException { final BranchEquivalence eq = context.requires(BranchEquivalence.class); - return new DefaultExecutionAnalysis(program, eq, progressModel); + return new DefaultExecutionAnalysis(program, eq); } } @@ -35,9 +35,9 @@ class DefaultExecutionAnalysis implements ExecutionAnalysis { private final ProgressModel.Hierarchy progressModel; private final Thread lowestIdThread; // For HSA - public DefaultExecutionAnalysis(Program program, BranchEquivalence eq, ProgressModel.Hierarchy progressModel) { + public DefaultExecutionAnalysis(Program program, BranchEquivalence eq) { this.eq = eq; - this.progressModel = progressModel; + this.progressModel = program.getProgressModel(); this.lowestIdThread = program.getThreads().stream().min(Comparator.comparingInt(Thread::getId)).get(); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Tearing.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Tearing.java index 9350cb4ddc..780696b2c6 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Tearing.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Tearing.java @@ -1,6 +1,5 @@ package com.dat3m.dartagnan.program.processing; -import com.dat3m.dartagnan.configuration.ProgressModel; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.expression.Type; @@ -19,12 +18,10 @@ import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.*; -import com.dat3m.dartagnan.program.event.core.InstructionBoundary; import com.dat3m.dartagnan.program.event.metadata.SourceLocation; import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.verification.Context; - import com.google.common.collect.Ordering; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -58,8 +55,7 @@ public void run(Program program) { try { final Context analysisContext = Context.create(); analysisContext.register(BranchEquivalence.class, BranchEquivalence.fromConfig(program, configuration)); - analysisContext.register(ExecutionAnalysis.class, ExecutionAnalysis.fromConfig(program, - ProgressModel.defaultHierarchy(), analysisContext, configuration)); + analysisContext.register(ExecutionAnalysis.class, ExecutionAnalysis.fromConfig(program, analysisContext, configuration)); analysisContext.register(ReachingDefinitionsAnalysis.class, ReachingDefinitionsAnalysis.fromConfig(program, analysisContext, configuration)); alias = AliasAnalysis.fromConfig(program, analysisContext, configuration, true); 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 4324259a67..c78ba864b2 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 @@ -2,7 +2,6 @@ import com.dat3m.dartagnan.GlobalSettings; import com.dat3m.dartagnan.configuration.Method; -import com.dat3m.dartagnan.configuration.ProgressModel; import com.dat3m.dartagnan.configuration.Property; import com.dat3m.dartagnan.witness.WitnessType; import org.sosy_lab.common.configuration.Option; @@ -25,20 +24,6 @@ public EnumSet getProperty() { return property; } - @Option( - name = PROGRESSMODEL, - description = """ - The progress model to assume: fair (default), hsa, obe, unfair. - To specify progress models per scope, use [=,...]. - Defaults to "fair" for unspecified scopes unless "default=" is specified. - """, - toUppercase = true) - private ProgressModel.Hierarchy progressModel = ProgressModel.defaultHierarchy(); - - public ProgressModel.Hierarchy getProgressModel() { - return this.progressModel; - } - @Option( name = VALIDATE, description = "Performs violation witness validation. Argument is the path to the witness 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 d44a89f156..793a515aa0 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/VerificationTask.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/VerificationTask.java @@ -1,7 +1,6 @@ package com.dat3m.dartagnan.verification; import com.dat3m.dartagnan.configuration.Arch; -import com.dat3m.dartagnan.configuration.ProgressModel; import com.dat3m.dartagnan.configuration.Property; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.witness.graphml.WitnessGraph; @@ -25,17 +24,15 @@ public class VerificationTask { // Data objects private final Program program; private final Wmm memoryModel; - private final ProgressModel.Hierarchy progressModel; private final EnumSet property; private final WitnessGraph witness; private final Configuration config; - protected VerificationTask(Program program, Wmm memoryModel, ProgressModel.Hierarchy progressModel, + protected VerificationTask(Program program, Wmm memoryModel, EnumSet property, WitnessGraph witness, Configuration config) throws InvalidConfigurationException { this.program = checkNotNull(program); this.memoryModel = checkNotNull(memoryModel); - this.progressModel = checkNotNull(progressModel); this.property = checkNotNull(property); this.witness = checkNotNull(witness); this.config = checkNotNull(config); @@ -47,7 +44,6 @@ public static VerificationTaskBuilder builder() { public Program getProgram() { return program; } public Wmm getMemoryModel() { return memoryModel; } - public ProgressModel.Hierarchy getProgressModel() { return progressModel; } public Configuration getConfig() { return this.config; } public WitnessGraph getWitness() { return witness; } public EnumSet getProperty() { return property; } @@ -58,7 +54,6 @@ public static VerificationTaskBuilder builder() { public static class VerificationTaskBuilder { protected WitnessGraph witness = new WitnessGraph(); protected ConfigurationBuilder config = Configuration.builder(); - protected ProgressModel.Hierarchy progressModel = ProgressModel.defaultHierarchy(); protected VerificationTaskBuilder() { } @@ -79,11 +74,6 @@ public VerificationTaskBuilder withBound(int k) { return this; } - public VerificationTaskBuilder withProgressModel(ProgressModel.Hierarchy progressModel) { - this.progressModel = progressModel; - return this; - } - public VerificationTaskBuilder withSolverTimeout(int t) { this.config.setOption(TIMEOUT, Integer.toString(t)); return this; @@ -100,7 +90,7 @@ public VerificationTaskBuilder withConfig(Configuration config) { } public VerificationTask build(Program program, Wmm memoryModel, EnumSet property) throws InvalidConfigurationException { - return new VerificationTask(program, memoryModel, progressModel, property, witness, config.build()); + return new VerificationTask(program, memoryModel, property, witness, config.build()); } } } \ No newline at end of file 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 8aeb8db62e..db80c2bd3a 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 @@ -25,7 +25,6 @@ import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; import com.dat3m.dartagnan.wmm.analysis.WmmAnalysis; import com.dat3m.dartagnan.wmm.processing.WmmProcessingManager; - import com.google.common.base.Preconditions; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -218,7 +217,7 @@ public static void preprocessMemoryModel(VerificationTask task, Configuration co public static void performStaticProgramAnalyses(VerificationTask task, Context analysisContext, Configuration config) throws InvalidConfigurationException { final Program program = task.getProgram(); analysisContext.register(BranchEquivalence.class, BranchEquivalence.fromConfig(program, config)); - analysisContext.register(ExecutionAnalysis.class, ExecutionAnalysis.fromConfig(program, task.getProgressModel(), + analysisContext.register(ExecutionAnalysis.class, ExecutionAnalysis.fromConfig(program, analysisContext, config)); analysisContext.register(ReachingDefinitionsAnalysis.class, ReachingDefinitionsAnalysis.fromConfig(program, analysisContext, config)); 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 a010011afd..b157c5c582 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java @@ -79,6 +79,7 @@ protected final Configuration getConfiguration() throws InvalidConfigurationExce .setOption(BOUND, boundProvider.get().toString()) .setOption(TARGET, targetProvider.get().name()) .setOption(PHANTOM_REFERENCES, "true") + .setOption(PROGRESSMODEL, progressModelProvider.get().toOptionString()) .setOption(INITIALIZE_REGISTERS, "true"); return additionalConfig(configBase).build(); @@ -117,13 +118,13 @@ protected long getTimeout() { protected final Provider filePathProvider = () -> path; protected final Provider nameProvider = Provider.fromSupplier(() -> getNameWithoutExtension(Path.of(path).getFileName().toString())); protected final Provider boundProvider = getBoundProvider(); - protected final Provider programProvider = Providers.createProgramFromPath(filePathProvider); - protected final Provider wmmProvider = getWmmProvider(); protected final Provider progressModelProvider = getProgressModelProvider(); + protected final Provider configProvider = Provider.fromSupplier(this::getConfiguration); + protected final Provider programProvider = Providers.createProgramFromPath(filePathProvider, configProvider); + protected final Provider wmmProvider = getWmmProvider(); protected final Provider> propertyProvider = getPropertyProvider(); protected final Provider expectedResultProvider = Provider.fromSupplier(() -> expectedResults.get(filePathProvider.get().substring(filePathProvider.get().indexOf("/") + 1))); - protected final Provider configProvider = Provider.fromSupplier(this::getConfiguration); - protected final Provider taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, progressModelProvider, configProvider); + protected final Provider taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, configProvider); private final Timeout timeout = Timeout.millis(getTimeout()); private final RequestShutdownOnError shutdownOnError = RequestShutdownOnError.create(shutdownManagerProvider); @@ -134,11 +135,11 @@ protected long getTimeout() { .around(filePathProvider) .around(nameProvider) .around(boundProvider) + .around(progressModelProvider) + .around(configProvider) .around(programProvider) .around(wmmProvider) - .around(progressModelProvider) .around(propertyProvider) - .around(configProvider) .around(taskProvider) .around(expectedResultProvider) .around(timeout); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/comparison/AbstractComparisonTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/comparison/AbstractComparisonTest.java index 5d2341dfc8..b05bdf2373 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/comparison/AbstractComparisonTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/comparison/AbstractComparisonTest.java @@ -2,7 +2,6 @@ import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.configuration.Method; -import com.dat3m.dartagnan.configuration.ProgressModel; import com.dat3m.dartagnan.configuration.Property; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.utils.ResourceHelper; @@ -98,8 +97,8 @@ protected ConfigurationBuilder additionalConfig(ConfigurationBuilder builder) { protected final Provider wmm2Provider = getTargetWmmProvider(); protected final Provider> propertyProvider = getPropertyProvider(); protected final Provider configProvider = Provider.fromSupplier(this::getConfiguration); - protected final Provider task1Provider = Providers.createTask(program1Provider, wmm1Provider, propertyProvider, sourceProvider, ProgressModel::defaultHierarchy, () -> 1, configProvider); - protected final Provider task2Provider = Providers.createTask(program2Provider, wmm2Provider, propertyProvider, targetProvider, ProgressModel::defaultHierarchy, () -> 1, configProvider); + protected final Provider task1Provider = Providers.createTask(program1Provider, wmm1Provider, propertyProvider, sourceProvider, () -> 1, configProvider); + protected final Provider task2Provider = Providers.createTask(program2Provider, wmm2Provider, propertyProvider, targetProvider, () -> 1, configProvider); 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/compilation/AbstractCompilationTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/compilation/AbstractCompilationTest.java index e4f250c8f5..2b27b58fd6 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/compilation/AbstractCompilationTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/compilation/AbstractCompilationTest.java @@ -2,7 +2,6 @@ import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.configuration.Method; -import com.dat3m.dartagnan.configuration.ProgressModel; import com.dat3m.dartagnan.configuration.Property; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.event.Event; @@ -105,8 +104,8 @@ protected ConfigurationBuilder additionalConfig(ConfigurationBuilder builder) { protected final Provider wmm2Provider = getTargetWmmProvider(); protected final Provider> propertyProvider = getPropertyProvider(); protected final Provider configProvider = Provider.fromSupplier(this::getConfiguration); - protected final Provider task1Provider = Providers.createTask(program1Provider, wmm1Provider, propertyProvider, sourceProvider, ProgressModel::defaultHierarchy, () -> 1, configProvider); - protected final Provider task2Provider = Providers.createTask(program2Provider, wmm2Provider, propertyProvider, targetProvider, ProgressModel::defaultHierarchy, () -> 1, configProvider); + protected final Provider task1Provider = Providers.createTask(program1Provider, wmm1Provider, propertyProvider, sourceProvider, () -> 1, configProvider); + protected final Provider task2Provider = Providers.createTask(program2Provider, wmm2Provider, propertyProvider, targetProvider, () -> 1, configProvider); private final Timeout timeout = Timeout.millis(getTimeout()); private final RequestShutdownOnError shutdownOnError = RequestShutdownOnError.create(shutdownManagerProvider); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/llvm/AbstractCTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/llvm/AbstractCTest.java index 09ce0ff5f2..c0396f805e 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/llvm/AbstractCTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/llvm/AbstractCTest.java @@ -44,6 +44,7 @@ protected final Configuration getBaseConfiguration() throws InvalidConfiguration .setOption(OptionNames.SOLVER, getSolverProvider().get().name()) .setOption(OptionNames.BOUND, getBoundProvider().get().toString()) .setOption(OptionNames.TARGET, targetProvider.get().name()) + .setOption(OptionNames.PROGRESSMODEL, progressModelProvider.get().toOptionString()) .setOption(OptionNames.PHANTOM_REFERENCES, "true"); return additionalConfig(configBase).build(); @@ -84,13 +85,13 @@ protected Provider getProgressModelProvider() { protected final Provider targetProvider = () -> target; protected final Provider filePathProvider = getProgramPathProvider(); protected final Provider boundProvider = getBoundProvider(); - protected final Provider programProvider = Providers.createProgramFromPath(filePathProvider); + protected final Provider configurationProvider = Provider.fromSupplier(this::getBaseConfiguration); + protected final Provider programProvider = Providers.createProgramFromPath(filePathProvider, configurationProvider); protected final Provider wmmProvider = getWmmProvider(); protected final Provider progressModelProvider = getProgressModelProvider(); protected final Provider solverProvider = getSolverProvider(); protected final Provider> propertyProvider = getPropertyProvider(); - protected final Provider configurationProvider = Provider.fromSupplier(this::getBaseConfiguration); - protected final Provider taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, progressModelProvider, configurationProvider); + protected final Provider taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, configurationProvider); // Special rules protected final Timeout timeout = Timeout.millis(getTimeout()); @@ -102,12 +103,12 @@ protected Provider getProgressModelProvider() { .around(shutdownOnError) .around(filePathProvider) .around(boundProvider) + .around(configurationProvider) .around(programProvider) .around(wmmProvider) .around(progressModelProvider) .around(solverProvider) .around(propertyProvider) - .around(configurationProvider) .around(taskProvider) .around(timeout); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/others/miscellaneous/AnalysisTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/others/miscellaneous/AnalysisTest.java index 28c654bd66..c769774e1b 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/others/miscellaneous/AnalysisTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/others/miscellaneous/AnalysisTest.java @@ -2,7 +2,6 @@ import com.dat3m.dartagnan.configuration.Alias; import com.dat3m.dartagnan.configuration.Arch; -import com.dat3m.dartagnan.configuration.ProgressModel; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.expression.type.IntegerType; @@ -106,7 +105,7 @@ private void reachingDefinitionMustOverride(ReachingDefinitionsAnalysis.Method m Configuration config = Configuration.builder().setOption(REACHING_DEFINITIONS_METHOD, method.name()).build(); Context context = Context.create(); context.register(BranchEquivalence.class, BranchEquivalence.fromConfig(program, config)); - context.register(ExecutionAnalysis.class, ExecutionAnalysis.fromConfig(program, ProgressModel.uniform(ProgressModel.FAIR), context, config)); + context.register(ExecutionAnalysis.class, ExecutionAnalysis.fromConfig(program, context, config)); final ReachingDefinitionsAnalysis rd = ReachingDefinitionsAnalysis.fromConfig(program, context, config); var me0 = (RegReader) findMatchingEventAfterProcessing(program, e0); var me1 = (RegReader) findMatchingEventAfterProcessing(program, e1); @@ -655,7 +654,7 @@ private AliasAnalysis analyze(Program program, Alias method) throws InvalidConfi ProcessingManager.fromConfig(configuration).run(program); Context analysisContext = Context.create(); analysisContext.register(BranchEquivalence.class, BranchEquivalence.fromConfig(program, configuration)); - analysisContext.register(ExecutionAnalysis.class, ExecutionAnalysis.fromConfig(program, ProgressModel.uniform(ProgressModel.FAIR), analysisContext, configuration)); + analysisContext.register(ExecutionAnalysis.class, ExecutionAnalysis.fromConfig(program, analysisContext, configuration)); analysisContext.register(ReachingDefinitionsAnalysis.class, ReachingDefinitionsAnalysis.fromConfig(program, analysisContext, configuration)); return AliasAnalysis.fromConfig(program, analysisContext, configuration, false); } @@ -769,8 +768,7 @@ public void allKindsOfMixedSizeAccesses() throws Exception { Context analysisContext = Context.create(); analysisContext.register(BranchEquivalence.class, BranchEquivalence.fromConfig(program, config)); - analysisContext.register(ExecutionAnalysis.class, ExecutionAnalysis.fromConfig(program, - ProgressModel.defaultHierarchy(), analysisContext, config)); + analysisContext.register(ExecutionAnalysis.class, ExecutionAnalysis.fromConfig(program, analysisContext, config)); analysisContext.register(ReachingDefinitionsAnalysis.class, ReachingDefinitionsAnalysis.fromConfig(program, analysisContext, config)); assertTrue(program.getThreadEvents(Init.class).isEmpty()); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/vulkan/termination/SpirvLivenessTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/vulkan/termination/SpirvLivenessTest.java index 213733bd90..9bfbf6c5d2 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/vulkan/termination/SpirvLivenessTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/vulkan/termination/SpirvLivenessTest.java @@ -107,9 +107,9 @@ private VerificationTask mkTask() throws Exception { VerificationTask.VerificationTaskBuilder builder = VerificationTask.builder() .withConfig(TestHelper.getBasicConfig()) .withBound(bound) - .withProgressModel(progressModel) .withTarget(Arch.VULKAN); Program program = new ProgramParser().parse(new File(programPath)); + program.setProgressModel(progressModel); Wmm mcm = new ParserCat().parse(new File(modelPath)); return builder.build(program, mcm, EnumSet.of(TERMINATION)); } 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 a1fa23998a..a6c07c6e3d 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 @@ -1,7 +1,6 @@ package com.dat3m.dartagnan.utils.rules; import com.dat3m.dartagnan.configuration.Arch; -import com.dat3m.dartagnan.configuration.ProgressModel; import com.dat3m.dartagnan.configuration.Property; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; @@ -47,31 +46,40 @@ public static Provider createWmmFromName(Supplier nameSupplier) { // =========================== Program providers ============================== public static Provider createProgramFromPath(Supplier pathSupplier) { - return createProgramFromFile(() -> new File(pathSupplier.get())); + return createProgramFromPath(pathSupplier, Configuration::defaultConfiguration); + } + + public static Provider createProgramFromPath(Supplier pathSupplier, Supplier configSupplier) { + return createProgramFromFile(() -> new File(pathSupplier.get()), configSupplier); } public static Provider createProgramFromFile(Supplier fileSupplier) { - return Provider.fromSupplier(() -> new ProgramParser().parse(fileSupplier.get())); + return createProgramFromFile(fileSupplier, Configuration::defaultConfiguration); + } + + public static Provider createProgramFromFile(Supplier fileSupplier, Supplier configSupplier) { + return Provider.fromSupplier(() -> { + Program p = new ProgramParser().parse(fileSupplier.get()); + p.injectConfig(configSupplier.get()); + return p; + }); } // =========================== Task related providers ============================== - public static Provider createTask(Supplier programSupplier, Supplier wmmSupplier, Supplier> propertySupplier, - Supplier progressModelSupplier, Supplier config) { + public static Provider createTask(Supplier programSupplier, Supplier wmmSupplier, Supplier> propertySupplier, Supplier config) { return Provider.fromSupplier(() -> VerificationTask.builder(). withConfig(config.get()). - withProgressModel(progressModelSupplier.get()). build(programSupplier.get(), wmmSupplier.get(), propertySupplier.get()) ); } public static Provider createTask(Supplier programSupplier, Supplier wmmSupplier, Supplier> propertySupplier, - Supplier targetSupplier, Supplier progressModelSupplier, Supplier boundSupplier, Supplier config) { + Supplier targetSupplier, Supplier boundSupplier, Supplier config) { return Provider.fromSupplier(() -> VerificationTask.builder(). withConfig(config.get()). withTarget(targetSupplier.get()). withBound(boundSupplier.get()). - withProgressModel(progressModelSupplier.get()). build(programSupplier.get(), wmmSupplier.get(), propertySupplier.get())); } 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 71caee56bc..af1d175f0e 100644 --- a/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java +++ b/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java @@ -29,6 +29,7 @@ public ReachabilityResult(Program program, Wmm wmm, UiOptions options) { this.program = program; this.wmm = wmm; this.options = options; + run(); } @@ -50,6 +51,7 @@ private void run() { } try { + program.setProgressModel(ProgressModel.uniform(options.progress())); final Arch arch = program.getArch() != null ? program.getArch() : options.target(); final Configuration config = Configuration.builder().setOptions(options.config()).build(); final VerificationTask task = VerificationTask.builder() @@ -58,7 +60,6 @@ private void run() { .withSolverTimeout(options.timeout()) .withSolver(options.solver()) .withTarget(arch) - .withProgressModel(ProgressModel.uniform(options.progress())) .build(program, wmm, options.properties()); try (ModelChecker modelChecker = ModelChecker.create(task, options.method())) { long startTime = System.currentTimeMillis();