Skip to content

Commit

Permalink
Add option modeling.mixedType .
Browse files Browse the repository at this point in the history 
Until switched-on, using just boolean and the archType for data.
  • Loading branch information
@xeren
xeren committed Aug 1, 2023
1 parent 4c8c81d commit 11f2fc1
Show file tree
Hide file tree
Showing 3 changed files with 27 additions and 16 deletions.
8 changes: 8 additions & 0 deletions dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@
import org.sosy_lab.common.configuration.Options;

import static com.dat3m.dartagnan.configuration.OptionNames.ARCH_PRECISION;
import static com.dat3m.dartagnan.configuration.OptionNames.MIXED_TYPE;

@Options
public class GlobalSettings {
Expand All @@ -24,8 +25,15 @@ private GlobalSettings() {}
secure = true)
private int arch_precision = -1;

@Option(name = MIXED_TYPE,
description = "If false, all non-boolean, non-aggregate data types are unified into one common integer type determined by " + ARCH_PRECISION + ".",
secure = true)
private boolean mixedType = false;

public static int getArchPrecision() { return instance.arch_precision; }

public static boolean isMixedType() { return instance.mixedType; }

public static void configure(Configuration config) throws InvalidConfigurationException {
config.inject(instance);
}
Expand Down
3 changes: 2 additions & 1 deletion dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ public class OptionNames {
public static final String THREAD_CREATE_ALWAYS_SUCCEEDS = "modeling.threadCreateAlwaysSucceeds";
public static final String ARCH_PRECISION = "modeling.precision";
public static final String RECURSION_BOUND = "modeling.recursionBound";
public static final String MIXED_TYPE = "modeling.mixedType";

// Compilation Options
public static final String USE_RC11_TO_ARCH_SCHEME = "compilation.rc11ToArch";
Expand All @@ -30,7 +31,7 @@ public class OptionNames {
public static final String BREAK_SYMMETRY_ON = "encoding.symmetry.breakOn";
public static final String BREAK_SYMMETRY_BY_SYNC_DEGREE = "encoding.symmetry.orderBySyncDegree";
public static final String IDL_TO_SAT = "encoding.wmm.idl2sat";

// Program Processing Options
public static final String DETERMINISTIC_REORDERING = "program.processing.detReordering";
public static final String REDUCE_SYMMETRY = "program.processing.reduceSymmetry";
Expand Down
32 changes: 17 additions & 15 deletions dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
package com.dat3m.dartagnan.parsers.program.visitors;

import com.dat3m.dartagnan.GlobalSettings;
import com.dat3m.dartagnan.exception.ParsingException;
import com.dat3m.dartagnan.expression.Expression;
import com.dat3m.dartagnan.expression.ExpressionFactory;
Expand Down Expand Up @@ -40,7 +41,9 @@ public class VisitorLlvm extends LLVMIRBaseVisitor<Expression> {
private final Program program = new Program(new Memory(), Program.SourceLanguage.LLVM);
private final TypeFactory types = TypeFactory.getInstance();
private final ExpressionFactory expressions = ExpressionFactory.getInstance();
private final Type pointerType = types.getArchType();
private final Type pointerType = GlobalSettings.getArchPrecision() == -1 ?
// Intentionally ignore the given precision for pointers
types.getIntegerType() : types.getIntegerType(64);
private final IntegerType integerType = types.getArchType();
private final Map<String, Expression> constantMap = new HashMap<>();
private final Map<String, Type> typeMap = new HashMap<>();
Expand Down Expand Up @@ -359,7 +362,7 @@ public Expression visitStoreInst(StoreInstContext ctx) {
final var atomic = ctx.atomic != null;
final Expression value = visitTypeValue(ctx.typeValue(0));
final Expression address = visitTypeValue(ctx.typeValue(1));
check(address.getType().equals(types.getArchType()), "Non-pointer type in %s.", ctx);
check(address.getType().equals(pointerType), "Non-pointer type in %s.", ctx);
final String mo = atomic ? parseMemoryOrder(ctx.atomicOrdering()) : "";
final Event store = atomic ? Llvm.newStore(address, value, mo) : newStore(address, value);
block.events.add(store);
Expand Down Expand Up @@ -445,7 +448,7 @@ public Expression visitICmpInst(ICmpInstContext ctx) {
default -> throw new ParsingException(String.format("Unknown predicate in %s.", ctx.getText()));
};
// LLVM does not support a distinct boolean type.
return assignToRegister(expressions.makeIntegerCast(compared, types.getIntegerType(1), false));
return assignToRegister(expressions.makeIntegerCast(compared, getIntegerType(1), false));
}

@Override
Expand Down Expand Up @@ -561,9 +564,9 @@ public Expression visitCmpXchgInst(CmpXchgInstContext ctx) {
final String mo = parseMemoryOrder(ctx.atomicOrdering(0));
block.events.add(newCompareExchange(value, asExpected, address, comparator, substitute, mo, weak));
final Register register = currentRegisterName == null ? null :
getOrNewCurrentRegister(types.getAggregateType(List.of(comparator.getType(), types.getIntegerType(1))));
getOrNewCurrentRegister(types.getAggregateType(List.of(comparator.getType(), getIntegerType(1))));
if (register != null) {
final Expression cast = expressions.makeIntegerCast(asExpected, types.getIntegerType(1), false);
final Expression cast = expressions.makeIntegerCast(asExpected, getIntegerType(1), false);
final Expression result = expressions.makeConstruct(List.of(value, cast));
block.events.add(newLocal(register, result));
}
Expand Down Expand Up @@ -657,7 +660,7 @@ public Expression visitConstant(ConstantContext ctx) {

@Override
public Expression visitNullConst(NullConstContext ctx) {
return expressions.makeZero(types.getArchType());
return expressions.makeZero((IntegerType) pointerType);
}

@Override
Expand Down Expand Up @@ -839,7 +842,7 @@ public Expression visitSelectExpr(SelectExprContext ctx) {
}

private Expression checkPointerExpression(ParserRuleContext context) {
return checkExpression(types.getArchType(), context);
return checkExpression(pointerType, context);
}

private Expression checkExpression(Type type, ParserRuleContext context) {
Expand Down Expand Up @@ -867,7 +870,7 @@ public Expression visitIntType(IntTypeContext ctx) {

@Override
public Expression visitPointerType(PointerTypeContext ctx) {
parsedType = types.getArchType();
parsedType = pointerType;
return null;
}

Expand Down Expand Up @@ -895,8 +898,9 @@ public Expression visitArrayType(ArrayTypeContext ctx) {

@Override
public Expression visitType(TypeContext ctx) {
// translate opaque pointer types
if (ctx.type() != null && ctx.params() == null || ctx.opaquePointerType() != null) {
parsedType = types.getArchType();
parsedType = pointerType;
return null;
}
return super.visitType(ctx);
Expand All @@ -912,7 +916,7 @@ public Expression visitNamedType(NamedTypeContext ctx) {

private Type parseIntType(TerminalNode t) {
assert t.getText().startsWith("i");
return types.getIntegerType(Integer.parseUnsignedInt(t.getText().substring(1)));
return getIntegerType(Integer.parseUnsignedInt(t.getText().substring(1)));
}

private Type parseType(ParserRuleContext context) {
Expand All @@ -925,10 +929,8 @@ private Type parseType(ParserRuleContext context) {
return type;
}

private void checkLabelType(FirstClassTypeContext context) {
if (context.concreteType() == null || context.concreteType().labelType() == null) {
throw new ParsingException(String.format("Expected label type, got %s.", context.getText()));
}
private IntegerType getIntegerType(int precision) {
return GlobalSettings.isMixedType() ? types.getIntegerType(precision) : types.getArchType();
}

// ----------------------------------------------------------------------------------------------------------------
Expand All @@ -953,7 +955,7 @@ private Type checkPointerType(TypeValueContext context) {
throw new ParsingException(
String.format("Expected pointer type, instead of %s.", context.firstClassType().getText()));
}
return types.getArchType();
return pointerType;
}

private boolean parseBoolean(TerminalNode node) {
Expand Down

0 comments on commit 11f2fc1

Please sign in to comment.