Skip to content

Commit 1029e06

Browse files
ThomasHaashernanponcedeleon
ThomasHaas
authored and
hernanponcedeleon
committed
First commit for TBAA (contains almost all functionality)
1 parent bf457e3 commit 1029e06

File tree

2 files changed

+166
-0
lines changed

2 files changed

+166
-0
lines changed

‎dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
import com.dat3m.dartagnan.exception.ParsingException;
44
import com.dat3m.dartagnan.expression.*;
55
import com.dat3m.dartagnan.expression.integers.IntBinaryOp;
6+
import com.dat3m.dartagnan.expression.integers.IntLiteral;
67
import com.dat3m.dartagnan.expression.misc.ConstructExpr;
78
import com.dat3m.dartagnan.expression.type.*;
89
import com.dat3m.dartagnan.parsers.LLVMIRBaseVisitor;
@@ -11,6 +12,7 @@
1112
import com.dat3m.dartagnan.program.Function;
1213
import com.dat3m.dartagnan.program.Program;
1314
import com.dat3m.dartagnan.program.Register;
15+
import com.dat3m.dartagnan.program.analysis.alias.TBAA;
1416
import com.dat3m.dartagnan.program.event.Event;
1517
import com.dat3m.dartagnan.program.event.EventFactory;
1618
import com.dat3m.dartagnan.program.event.Tag;
@@ -50,6 +52,7 @@ public class VisitorLlvm extends LLVMIRBaseVisitor<Expression> {
5052
private final Map<String, TypeDefContext> typeDefinitionMap = new HashMap<>();
5153
private final Map<String, Type> typeMap = new HashMap<>();
5254
private final Map<String, MdNode> metadataSymbolTable = new LinkedHashMap<>();
55+
private final TBAABuilder tbaaBuilder = new TBAABuilder();
5356
private int functionCounter;
5457
// Nonnull, if the visitor is inside a function body.
5558
private Function function;
@@ -314,6 +317,22 @@ private List<Metadata> parseMetadataAttachment(List<MetadataAttachmentContext> m
314317
assert mdNode instanceof MdReference;
315318
mdNode = metadataSymbolTable.get(((MdReference) mdNode).mdName());
316319

320+
final String metaDatatype = metadataCtx.MetadataName().toString();
321+
322+
if (metaDatatype.equals("!tbaa")) {
323+
// We assume a tbaa access tag
324+
assert mdNode instanceof MdTuple;
325+
final MdTuple accessNode = (MdTuple) mdNode;
326+
final List<MdNode> children = accessNode.mdFields();
327+
328+
final TBAA.Type base = tbaaBuilder.getTBAATypeFromNode(children.get(0));
329+
final TBAA.Type access = tbaaBuilder.getTBAATypeFromNode(children.get(1));
330+
final int offset = ((MdGenericValue<IntLiteral>)children.get(2)).value().getValueAsInt();
331+
// final int isConstant = ((MdGenericValue<IntLiteral>)children.get(3)).value().getValueAsInt();
332+
333+
metadata.add(new TBAA.AccessTag(base, access, offset));
334+
}
335+
317336
if (mdNode instanceof SpecialMdTupleNode diLocationNode && diLocationNode.nodeType() == SpecialMdTupleNode.Type.DILocation) {
318337
SpecialMdTupleNode scope = diLocationNode;
319338
while (scope.getField("scope").isPresent()) {
@@ -1463,4 +1482,51 @@ public <T extends MdNode> Optional<T> getField(String fieldName) {
14631482
}
14641483
}
14651484

1485+
// ----------------------------------------------------------------------------------------------------------------
1486+
// TBAA-metadata
1487+
1488+
private class TBAABuilder {
1489+
private final Map<MdNode, TBAA.Type> md2tbaaMap = new HashMap<>();
1490+
1491+
private TBAA.Type getTBAATypeFromNode(MdNode node) {
1492+
if (node instanceof MdReference ref) {
1493+
node = metadataSymbolTable.get(ref.mdName());
1494+
}
1495+
assert node instanceof MdTuple;
1496+
1497+
if (!md2tbaaMap.containsKey(node)) {
1498+
final MdTuple tbaaTypeMdNode = (MdTuple) node;
1499+
final List<MdNode> children = tbaaTypeMdNode.mdFields();
1500+
if (children.size() <= 1) {
1501+
// Root
1502+
final String rootName = children.isEmpty() ? "root" : children.get(0).toString();
1503+
final TBAA.Type root = new TBAA.ScalarType(rootName, null);
1504+
md2tbaaMap.put(tbaaTypeMdNode, root);
1505+
} else if (children.size() == 3) {
1506+
// Scalar type node
1507+
final String name = children.get(0).toString();
1508+
final TBAA.Type parent = getTBAATypeFromNode(children.get(1));
1509+
assert children.get(2).toString().equals("0");
1510+
final TBAA.Type typeNode = new TBAA.ScalarType(name, parent);
1511+
md2tbaaMap.put(tbaaTypeMdNode, typeNode);
1512+
} else {
1513+
// Struct type node
1514+
final String name = children.get(0).toString();
1515+
final List<TBAA.TypeOffset> typeOffsets = new ArrayList<>();
1516+
for (int i = 1; i < children.size(); i += 2) {
1517+
final TBAA.Type innerType = getTBAATypeFromNode(children.get(i));
1518+
final int offset = ((MdGenericValue<IntLiteral>)children.get(i+1)).value().getValueAsInt();
1519+
typeOffsets.add(new TBAA.TypeOffset(innerType, offset));
1520+
}
1521+
final TBAA.StructType typeNode = new TBAA.StructType(name, typeOffsets);
1522+
md2tbaaMap.put(tbaaTypeMdNode, typeNode);
1523+
}
1524+
}
1525+
1526+
return md2tbaaMap.get(node);
1527+
}
1528+
1529+
}
1530+
1531+
14661532
}

‎dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/TBAA.java‎

Lines changed: 100 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,100 @@
1+
package com.dat3m.dartagnan.program.analysis.alias;
2+
3+
import com.dat3m.dartagnan.program.event.metadata.Metadata;
4+
5+
import java.util.List;
6+
import java.util.stream.Collectors;
7+
8+
public final class TBAA {
9+
10+
private TBAA() {}
11+
12+
public static boolean canAlias(AccessTag x, AccessTag y) {
13+
final TypeOffset xAccess = new TypeOffset(x.base(), x.offset());
14+
final TypeOffset yAccess = new TypeOffset(y.base(), y.offset());
15+
16+
TypeOffset xCheck = xAccess;
17+
while (xCheck != null) {
18+
if (xCheck.equals(yAccess)) {
19+
return true;
20+
}
21+
xCheck = getImmediateParent(xCheck);
22+
}
23+
24+
TypeOffset yCheck = yAccess;
25+
while (yCheck != null) {
26+
if (yCheck.equals(xAccess)) {
27+
return true;
28+
}
29+
yCheck = getImmediateParent(yCheck);
30+
}
31+
32+
return false;
33+
}
34+
35+
public static TypeOffset getImmediateParent(TypeOffset typeOffset) {
36+
if (typeOffset.type() instanceof ScalarType scalarType) {
37+
return scalarType.parent() == null ? null: new TypeOffset(scalarType.parent(), typeOffset.offset());
38+
} else if (typeOffset.type() instanceof StructType structType) {
39+
for (int i = 0; i < structType.offsets().size(); i++) {
40+
final TypeOffset cur = structType.offsets().get(i);
41+
final TypeOffset next = (i + 1) < structType.offsets().size() ? structType.offsets().get(i + 1) : null;
42+
43+
if (next == null || next.offset() < typeOffset.offset()) {
44+
return new TypeOffset(cur.type(), cur.offset() - typeOffset.offset());
45+
}
46+
}
47+
}
48+
assert false;
49+
return null;
50+
}
51+
52+
// ================================================================================================
53+
// Classes
54+
55+
public record AccessTag(Type base, Type access, int offset) implements Metadata {
56+
@Override
57+
public String toString() {
58+
return String.format("TBAA.Access( %s, %s, %d )", base.getName(), access.getName(), offset);
59+
}
60+
}
61+
62+
public interface Type {
63+
String getName();
64+
}
65+
66+
public record TypeOffset(Type type, int offset) {
67+
@Override
68+
public String toString() {
69+
return String.format("( %s, %s )", type.getName(), offset);
70+
}
71+
}
72+
73+
public record ScalarType(String name, Type parent) implements Type {
74+
@Override
75+
public String toString() {
76+
if (parent == null) {
77+
return name;
78+
}
79+
return String.format("{ %s, %s }", name, parent.getName());
80+
}
81+
82+
@Override
83+
public String getName() {
84+
return name;
85+
}
86+
}
87+
88+
public record StructType(String name, List<TypeOffset> offsets) implements Type {
89+
@Override
90+
public String getName() {
91+
return name;
92+
}
93+
94+
@Override
95+
public String toString() {
96+
return String.format("{ %s, %s }", name,
97+
offsets.stream().map(Object::toString).collect(Collectors.joining(", ")));
98+
}
99+
}
100+
}

0 commit comments

Comments
 (0)