Skip to content

Commit

Permalink
Minor refactoring
Browse files Browse the repository at this point in the history
  • Loading branch information
@natgavrilenko
natgavrilenko committed Jul 10, 2024
1 parent e8a98f3 commit 2b61dc4
Show file tree
Hide file tree
Showing 8 changed files with 38 additions and 39 deletions.
5 changes: 1 addition & 4 deletions dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@
import com.dat3m.dartagnan.expression.integers.IntCmpOp;
import com.dat3m.dartagnan.expression.type.BooleanType;
import com.dat3m.dartagnan.expression.type.IntegerType;
import com.dat3m.dartagnan.expression.type.TypeFactory;
import com.dat3m.dartagnan.program.Register;
import com.dat3m.dartagnan.program.analysis.BranchEquivalence;
import com.dat3m.dartagnan.program.analysis.ExecutionAnalysis;
Expand Down Expand Up @@ -46,7 +45,6 @@
public final class EncodingContext {

private static final Logger logger = LogManager.getLogger(EncodingContext.class);
private static final TypeFactory types = TypeFactory.getInstance();

private final VerificationTask verificationTask;
private final Context analysisContext;
Expand Down Expand Up @@ -215,13 +213,12 @@ public BooleanFormula dependency(Event first, Event second) {
return booleanFormulaManager.makeVariable("idd " + first.getGlobalId() + " " + second.getGlobalId());
}

public Formula lastValue(MemoryObject base, int offset) {
public Formula lastValue(MemoryObject base, int offset, int size) {
checkArgument(0 <= offset && offset < base.size(), "array index out of bounds");
final String name = String.format("last_val_at_%s_%d", base, offset);
if (useIntegers) {
return formulaManager.getIntegerFormulaManager().makeVariable(name);
}
final int size = types.getMemorySizeInBits(base.getInitialValue(offset).getType());
return formulaManager.getBitvectorFormulaManager().makeVariable(size, name);
}

Expand Down
6 changes: 5 additions & 1 deletion dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
import com.dat3m.dartagnan.expression.booleans.BoolUnaryExpr;
import com.dat3m.dartagnan.expression.integers.*;
import com.dat3m.dartagnan.expression.misc.ITEExpr;
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;
Expand All @@ -23,6 +24,8 @@

class ExpressionEncoder implements ExpressionVisitor<Formula> {

private static final TypeFactory typeFactory = TypeFactory.getInstance();

private final EncodingContext context;
private final FormulaManager formulaManager;
private final BooleanFormulaManager booleanFormulaManager;
Expand Down Expand Up @@ -297,6 +300,7 @@ public Formula visitMemoryObject(MemoryObject memObj) {
@Override
public Formula visitLocation(Location location) {
checkState(event == null, "Cannot evaluate %s at event %s.", location, event);
return context.lastValue(location.getMemoryObject(), location.getOffset());
int size = typeFactory.getMemorySizeInBits(location.getType());
return context.lastValue(location.getMemoryObject(), location.getOffset(), size);
}
}
9 changes: 6 additions & 3 deletions dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@

import com.dat3m.dartagnan.configuration.Arch;
import com.dat3m.dartagnan.configuration.Property;
import com.dat3m.dartagnan.expression.type.TypeFactory;
import com.dat3m.dartagnan.program.Program;
import com.dat3m.dartagnan.program.Thread;
import com.dat3m.dartagnan.program.analysis.ExecutionAnalysis;
Expand Down Expand Up @@ -41,6 +42,7 @@
public class PropertyEncoder implements Encoder {

private static final Logger logger = LogManager.getLogger(PropertyEncoder.class);
private static final TypeFactory typeFactory = TypeFactory.getInstance();

private final EncodingContext context;
private final Program program;
Expand Down Expand Up @@ -205,7 +207,8 @@ private BooleanFormula encodeLastCoConstraints() {
continue;
}
BooleanFormula sameAddress = context.sameAddress(init, w1);
Formula v2 = context.lastValue(init.getBase(), init.getOffset());
int size = typeFactory.getMemorySizeInBits(init.getValue().getType());
Formula v2 = context.lastValue(init.getBase(), init.getOffset(), size);
BooleanFormula sameValue = context.equal(context.value(w1), v2);
enc.add(bmgr.implication(bmgr.and(lastCoExpr, sameAddress), sameValue));
}
Expand All @@ -219,7 +222,8 @@ private BooleanFormula encodeLastCoConstraints() {
for (Init init : program.getThreadEvents(Init.class)) {
BooleanFormula lastValueEnc = bmgr.makeFalse();
BooleanFormula lastStoreExistsEnc = bmgr.makeFalse();
Formula v2 = context.lastValue(init.getBase(), init.getOffset());
int size = typeFactory.getMemorySizeInBits(init.getValue().getType());
Formula v2 = context.lastValue(init.getBase(), init.getOffset(), size);
BooleanFormula readFromInit = context.equal(context.value(init), v2);
for (Store w : program.getThreadEvents(Store.class)) {
if (!alias.mayAlias(w, init)) {
Expand Down Expand Up @@ -444,7 +448,6 @@ public TrackableFormula encodeDeadlocks() {
final Map<Thread, List<SpinIteration>> spinloopsMap =
Maps.toMap(program.getThreads(), t -> this.findSpinLoopsInThread(t, loopAnalysis));
// Compute "stuckness" encoding for all threads

final Map<Thread, BooleanFormula> isStuckMap = Maps.toMap(program.getThreads(), t -> {
List<BooleanFormula> stuckAtBarrier = t.getEvents().stream()
.filter(FenceWithId.class::isInstance)
Expand Down
34 changes: 17 additions & 17 deletions dartagnan/src/main/java/com/dat3m/dartagnan/expression/type/TypeFactory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -139,50 +139,50 @@ public Map<Integer, Type> decomposeIntoPrimitives(Type type) {
return decomposition;
}

public static boolean isExactType(Type type) {
public static boolean isStaticType(Type type) {
if (type instanceof BooleanType || type instanceof IntegerType || type instanceof FloatType) {
return true;
}
if (type instanceof ArrayType aType) {
return aType.hasKnownNumElements() && isExactType(aType.getElementType());
return aType.hasKnownNumElements() && isStaticType(aType.getElementType());
}
if (type instanceof AggregateType aType) {
for (Type elType : aType.getDirectFields()) {
if (!isExactType(elType)) {
if (!isStaticType(elType)) {
return false;
}
}
return true;
}
throw new UnsupportedOperationException("Cannot deduce fixed size of type " + type);
throw new UnsupportedOperationException("Cannot compute if type '" + type + "' is static");
}

public static boolean isExactTypeOf(Type exactType, Type genericType) {
if (exactType.equals(genericType)) {
public static boolean isStaticTypeOf(Type staticType, Type genericType) {
if (staticType.equals(genericType)) {
return true;
}
if (exactType instanceof AggregateType elExactType && genericType instanceof AggregateType elGenericSizeType) {
int size = elExactType.getDirectFields().size();
if (size != elGenericSizeType.getDirectFields().size()) {
if (staticType instanceof AggregateType aStaticType && genericType instanceof AggregateType aGenericSizeType) {
int size = aStaticType.getDirectFields().size();
if (size != aGenericSizeType.getDirectFields().size()) {
return false;
}
for (int i = 0; i < size; i++) {
if (!isExactTypeOf(elExactType.getDirectFields().get(i), elGenericSizeType.getDirectFields().get(i))) {
if (!isStaticTypeOf(aStaticType.getDirectFields().get(i), aGenericSizeType.getDirectFields().get(i))) {
return false;
}
}
return true;
}
if (exactType instanceof ArrayType elExactType && genericType instanceof ArrayType elGenericType) {
int countExact = elExactType.getNumElements();
int countGeneric = elGenericType.getNumElements();
if (countExact != countGeneric && (countGeneric != -1 || countExact <= 0)) {
if (staticType instanceof ArrayType aStaticType && genericType instanceof ArrayType aGenericType) {
int countStatic = aStaticType.getNumElements();
int countGeneric = aGenericType.getNumElements();
if (countStatic != countGeneric && (countGeneric != -1 || countStatic <= 0)) {
return false;
}
return isExactTypeOf(elExactType.getElementType(), elGenericType.getElementType());
return isStaticTypeOf(aStaticType.getElementType(), aGenericType.getElementType());
}
if (exactType instanceof ScopedPointerType pExactType && genericType instanceof ScopedPointerType pGenericType) {
return isExactTypeOf(pExactType.getPointedType(), pGenericType.getPointedType());
if (staticType instanceof ScopedPointerType pStaticType && genericType instanceof ScopedPointerType pGenericType) {
return isStaticTypeOf(pStaticType.getPointedType(), pGenericType.getPointedType());
}
return false;
}
Expand Down
6 changes: 3 additions & 3 deletions ...an/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsMemory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,12 +83,12 @@ public Event visitOpVariable(SpirvParser.OpVariableContext ctx) {
Type type = pType.getPointedType();
Expression value = getOpVariableInitialValue(ctx, type);
if (value != null) {
if (!TypeFactory.isExactTypeOf(value.getType(), type)) {
if (!TypeFactory.isStaticTypeOf(value.getType(), type)) {
throw new ParsingException("Mismatching value type for variable '%s', " +
"expected '%s' but received '%s'", id, type, value.getType());
}
type = value.getType();
} else if (!TypeFactory.isExactType(type)) {
} else if (!TypeFactory.isStaticType(type)) {
throw new ParsingException("Missing initial value for runtime variable '%s'", id);
} else {
value = builder.newUndefinedValue(type);
Expand Down Expand Up @@ -188,7 +188,7 @@ private void visitOpAccessChain(String id, String typeId, String baseId,
.map(c -> builder.getExpression(c.getText()))
.toList();
Type exactResultType = HelperAccessChain.getMemberType(id, baseType, indexes);
if (!TypeFactory.isExactTypeOf(exactResultType, resultType)) {
if (!TypeFactory.isStaticTypeOf(exactResultType, resultType)) {
throw new ParsingException("Invalid result type in access chain '%s', " +
"expected '%s' but received '%s'", id, resultType, exactResultType);
}
Expand Down
14 changes: 6 additions & 8 deletions dartagnan/src/main/java/com/dat3m/dartagnan/program/event/TagSet.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,14 +28,12 @@ public boolean contains(Object o) {

@Override
public boolean remove(Object o) {
if (!(o instanceof String tag)) {
return false;
}

final int index = Collections.binarySearch(sortedTags, tag);
if (index >= 0) {
sortedTags.remove(index);
return true;
if (o instanceof String tag) {
final int index = Collections.binarySearch(sortedTags, tag);
if (index >= 0) {
sortedTags.remove(index);
return true;
}
}
return false;
}
Expand Down
1 change: 0 additions & 1 deletion dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/spirv/SpirvCmpXchg.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,6 @@ private Set<String> mkEqTags(Set<String> eqTags) {
}

private void validateMemoryOrder() {
// TODO: It allows illegal combination eq RELEASE and neq ACQUIRE
if (mo.equals(RELEASE) || mo.equals(ACQ_REL)) {
throw new IllegalArgumentException(
String.format("%s cannot have unequal memory order '%s'",
Expand Down
2 changes: 0 additions & 2 deletions dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Location.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,6 @@
import com.dat3m.dartagnan.expression.ExpressionVisitor;
import com.dat3m.dartagnan.expression.Type;
import com.dat3m.dartagnan.expression.base.LeafExpressionBase;
import com.dat3m.dartagnan.expression.type.IntegerType;
import com.dat3m.dartagnan.expression.type.TypeFactory;

public class Location extends LeafExpressionBase<Type> {

Expand Down

0 comments on commit 2b61dc4

Please sign in to comment.