Skip to content

Moved floating point rounding mode into Program #1019

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hernanponcedeleon merged 4 commits into from
Apr 7, 2026
Merged

Moved floating point rounding mode into Program #1019

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
bd7e84f
Moved floating point rounding mode into Program
ThomasHaas Mar 28, 2026
4918f9c
Moved code
ThomasHaas Mar 28, 2026
b4b058c
Moved code again
ThomasHaas Mar 28, 2026
619dd39
Refactor
ThomasHaas Mar 28, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -294,7 +294,7 @@ private static ResultSummary summaryFromResult(VerificationTask task, ModelCheck
StringBuilder details = new StringBuilder();
// We only show the condition if this is the reason of the failure
String condition = "";
final boolean ignoreFilter = task.getConfig().hasProperty(IGNORE_FILTER_SPECIFICATION) && task.getConfig().getProperty(IGNORE_FILTER_SPECIFICATION).equals("true");
final boolean ignoreFilter = Objects.equals(task.getConfig().getProperty(IGNORE_FILTER_SPECIFICATION), "true");
Copy link
Copy Markdown
Owner

@hernanponcedeleon hernanponcedeleon Mar 28, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does this now handle the case where we do not have the property?

Copy link
Copy Markdown
Collaborator Author

@ThomasHaas ThomasHaas Mar 28, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, it seems getProperty just returns NULL in that case.

final boolean nonEmptyFilter = !(p.getFilterSpecification() instanceof BoolLiteral bLit) || !bLit.getValue();
final String filter = !ignoreFilter && nonEmptyFilter ? p.getFilterSpecification().toString() : "";

Expand Down
8 changes: 0 additions & 8 deletions dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,13 +68,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<Event, BooleanFormula> controlFlowVariables = new HashMap<>();
private final Map<Event, BooleanFormula> executionVariables = new HashMap<>();
private final Map<NamedBarrier, BooleanFormula> syncVariables = new HashMap<>();
Expand Down Expand Up @@ -117,7 +110,6 @@ public static EncodingContext of(VerificationTask task, Context analysisContext,
EncodingContext context = new EncodingContext(task, analysisContext, formulaManager, constraintsToEncode);
task.getConfig().inject(context);
logger.info("{}: {}", MERGE_CF_VARS, context.shouldMergeCFVars);
logger.info("{}: {}", ROUNDING_MODE_FLOATS, context.roundingModeFloats);
context.initialize();

return context;
Expand Down
18 changes: 11 additions & 7 deletions dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,10 +47,14 @@ public class ExpressionEncoder {
private final ExprSimplifier simplifier = new ExprSimplifier(true);
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() {
Expand Down Expand Up @@ -583,7 +587,7 @@ public TypedFormula<BooleanType, BooleanFormula> 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);
}

Expand All @@ -603,7 +607,7 @@ public TypedFormula<BooleanType, BooleanFormula> visitIntCmpExpression(IntCmpExp
result = fpmgr.makeMinusInfinity(fFType);
} else {
assert floatLiteral.hasFiniteValue();
final FloatingPointFormula absVal = fpmgr.makeNumber(floatLiteral.getAbsValue(), fFType, context.roundingModeFloats);
final FloatingPointFormula absVal = fpmgr.makeNumber(floatLiteral.getAbsValue(), fFType, roundingMode);
result = floatLiteral.isNegative() ? fpmgr.negate(absVal) : absVal;
}
return new TypedFormula<>(floatLiteral.getType(), result);
Expand All @@ -618,10 +622,10 @@ public TypedFormula<BooleanType, BooleanFormula> 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);
Expand Down Expand Up @@ -687,7 +691,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);
}

Expand Down
56 changes: 46 additions & 10 deletions dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,10 +12,18 @@
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.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();
Expand All @@ -25,19 +33,35 @@ 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
private final List<Thread> threads;
private final List<Function> functions;
@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;
}

// Shape
private final List<Function> functions = new ArrayList<>();
private final List<Thread> threads = new ArrayList<>();
private final List<NonDetValue> constants = new ArrayList<>();
private final Memory memory;
private Entrypoint entrypoint = new Entrypoint.None();
private Arch arch;

// Spec
private SpecificationType specificationType = SpecificationType.ASSERT;
private Expression spec;
private Expression filterSpec; // Acts like "assume" statements, filtering out executions

// Semantic options
private final SemanticConfig semanticConfig = new SemanticConfig();

// Metadata
private final SourceLanguage format;
private String name;
private int unrollingBound = 0;
private Arch arch;
private boolean isCompiled;
private final SourceLanguage format;

private int nextThreadId = 0;
private int nextConstantId = 0;
Expand All @@ -51,8 +75,6 @@ public Program(Memory memory, SourceLanguage format) {
public Program(String name, Memory memory, SourceLanguage format) {
this.name = name;
this.memory = memory;
this.threads = new ArrayList<>();
this.functions = new ArrayList<>();
this.format = format;

this.filterSpec = ExpressionFactory.getInstance().makeTrue();
Expand Down Expand Up @@ -128,6 +150,20 @@ public void setFilterSpecification(Expression spec) {
this.filterSpec = spec;
}

public FloatingPointRoundingMode getFloatRoundingMode() {
return semanticConfig.floatRoundingMode;
}

public void setFloatRoundingMode(FloatingPointRoundingMode roundingMode) {
this.semanticConfig.floatRoundingMode = roundingMode;
}

public void injectConfig(Configuration configuration) throws InvalidConfigurationException {
configuration.inject(semanticConfig);
}

// -----------------------------------------------------------------------------------------------------------------

public void addThread(Thread t) {
threads.add(t);
t.setProgram(this);
Expand Down
3 changes: 3 additions & 0 deletions dartagnan/src/main/java/com/dat3m/dartagnan/verification/VerificationTask.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,9 @@ protected VerificationTask(Program program, Wmm memoryModel, ProgressModel.Hiera
this.property = checkNotNull(property);
this.witness = checkNotNull(witness);
this.config = checkNotNull(config);

// TODO: Is it a good idea to inject configs into the program here?
Copy link
Copy Markdown
Owner

@hernanponcedeleon hernanponcedeleon Mar 28, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What would be the alternative?

Copy link
Copy Markdown
Collaborator Author

@ThomasHaas ThomasHaas Mar 28, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Inject it right after parsing the program.

Copy link
Copy Markdown
Owner

@hernanponcedeleon hernanponcedeleon Mar 28, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Code-wise that would be bad, because we have different "places" where program is parsed (CLI, UI, unit tests) and we would have to inject it in all of them.

One could claim that we do not care the rounding mode unless we are doing the verification (and thus having the inject the VerificationTask is ok), but then this raises the question if the rounding mode should then indeed be part of the Program.

Copy link
Copy Markdown
Collaborator Author

@ThomasHaas ThomasHaas Mar 28, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well, we have a central ProgramParser that is always used to parse the program. If that class was configurable via a Configuration, we could inject the settings there. Generally, making the parsers configurable would be a good idea and allow us to give options like ignore inline assembly or throw on unknown inline assembly etc.

If the rounding mode was part of the verification task, we would need to lift all program passes to verification task passes (at least in principle) for otherwise the rounding mode was inaccessible.

But for now, I think having the injection in VerificationTask is okayish.

program.injectConfig(config);
}

public static VerificationTaskBuilder builder() {
Expand Down
Loading