diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java index fad0add96b..0158ebab15 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java @@ -3,6 +3,7 @@ import com.dat3m.dartagnan.exception.ParsingException; import com.dat3m.dartagnan.expression.*; import com.dat3m.dartagnan.expression.integers.IntBinaryOp; +import com.dat3m.dartagnan.expression.integers.IntLiteral; import com.dat3m.dartagnan.expression.misc.ConstructExpr; import com.dat3m.dartagnan.expression.type.*; import com.dat3m.dartagnan.parsers.LLVMIRBaseVisitor; @@ -11,6 +12,7 @@ import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.analysis.alias.TBAA; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.Tag; @@ -50,6 +52,7 @@ public class VisitorLlvm extends LLVMIRBaseVisitor { private final Map typeDefinitionMap = new HashMap<>(); private final Map typeMap = new HashMap<>(); private final Map metadataSymbolTable = new LinkedHashMap<>(); + private final TBAABuilder tbaaBuilder = new TBAABuilder(); private int functionCounter; // Nonnull, if the visitor is inside a function body. private Function function; @@ -307,23 +310,34 @@ private List parseMetadataAttachment(List m } final List metadata = new ArrayList<>(); - //FIXME: This code only looks for DILocation metadata, - // and it only extracts the information needed to construct SourceLocation metadata for (MetadataAttachmentContext metadataCtx: metadataAttachmentContexts) { MdNode mdNode = (MdNode) metadataCtx.accept(this); assert mdNode instanceof MdReference; mdNode = metadataSymbolTable.get(((MdReference) mdNode).mdName()); - if (mdNode instanceof SpecialMdTupleNode diLocationNode && diLocationNode.nodeType() == SpecialMdTupleNode.Type.DILocation) { - SpecialMdTupleNode scope = diLocationNode; - while (scope.getField("scope").isPresent()) { - scope = (SpecialMdTupleNode) metadataSymbolTable.get(scope.getField("scope").orElseThrow().mdName()); + final String metaDatatype = metadataCtx.MetadataName().toString(); + if (metaDatatype.equals("!tbaa")) { + // TBAA + metadata.add(tbaaBuilder.getTBAAAccessFromNode(mdNode)); + } else if (metaDatatype.equals("!dbg")) { + //FIXME: This code only looks for DILocation metadata + // and it only extracts the information needed to construct SourceLocation metadata + if (mdNode instanceof SpecialMdTupleNode diLocationNode && diLocationNode.nodeType() == SpecialMdTupleNode.Type.DILocation) { + SpecialMdTupleNode scope = diLocationNode; + while (scope.getField("scope").isPresent()) { + scope = (SpecialMdTupleNode) metadataSymbolTable.get(scope.getField("scope").orElseThrow().mdName()); + } + assert scope.nodeType() == SpecialMdTupleNode.Type.DIFile; + final String filename = scope.>getField("filename").orElseThrow().value(); + final String directory = scope.>getField("directory").orElseThrow().value(); + final int lineNumber = diLocationNode.>getField("line").orElseThrow().value().intValue(); + metadata.add(new SourceLocation((directory + "/" + filename).intern(), lineNumber)); + } + } else { + if (logger.isDebugEnabled()) { + final String optional = !metaDatatype.equals("!llvm.loop") ? " Potential for optimization?" : ""; + logger.debug("Skipped parsing of {} metadata.{}", metaDatatype, optional); } - assert scope.nodeType() == SpecialMdTupleNode.Type.DIFile; - final String filename = scope.>getField("filename").orElseThrow().value(); - final String directory = scope.>getField("directory").orElseThrow().value(); - final int lineNumber = diLocationNode.>getField("line").orElseThrow().value().intValue(); - metadata.add(new SourceLocation((directory + "/" + filename).intern(), lineNumber)); } } @@ -1463,4 +1477,72 @@ public Optional getField(String fieldName) { } } + // ---------------------------------------------------------------------------------------------------------------- + // TBAA-metadata + + private class TBAABuilder { + private final Map md2tbaaMap = new HashMap<>(); + private final Map md2accessMap = new HashMap<>(); + + private TBAA.AccessTag getTBAAAccessFromNode(MdNode node) { + if (node instanceof MdReference ref) { + node = metadataSymbolTable.get(ref.mdName()); + } + assert node instanceof MdTuple; + final MdTuple accessNode = (MdTuple) node; + + if (!md2accessMap.containsKey(accessNode)) { + // We assume a tbaa access tag + final List children = accessNode.mdFields(); + final TBAA.Type base = tbaaBuilder.getTBAATypeFromNode(children.get(0)); + final TBAA.Type access = tbaaBuilder.getTBAATypeFromNode(children.get(1)); + final int offset = ((MdGenericValue) children.get(2)).value().getValueAsInt(); + // final int isConstant = ((MdGenericValue)children.get(3)).value().getValueAsInt(); + md2accessMap.put(node, new TBAA.AccessTag(base, access, offset)); + } + + return md2accessMap.get(node); + } + + private TBAA.Type getTBAATypeFromNode(MdNode node) { + if (node instanceof MdReference ref) { + node = metadataSymbolTable.get(ref.mdName()); + } + assert node instanceof MdTuple; + + if (!md2tbaaMap.containsKey(node)) { + final MdTuple tbaaTypeMdNode = (MdTuple) node; + final List children = tbaaTypeMdNode.mdFields(); + if (children.size() <= 1) { + // Root + final String rootName = children.isEmpty() ? "root" : children.get(0).toString(); + final TBAA.Type root = new TBAA.ScalarType(rootName, null); + md2tbaaMap.put(tbaaTypeMdNode, root); + } else if (children.size() == 3) { + // Scalar type node + final String name = children.get(0).toString(); + final TBAA.Type parent = getTBAATypeFromNode(children.get(1)); + assert children.get(2).toString().equals("0"); + final TBAA.Type typeNode = new TBAA.ScalarType(name, parent); + md2tbaaMap.put(tbaaTypeMdNode, typeNode); + } else { + // Struct type node + final String name = children.get(0).toString(); + final List typeOffsets = new ArrayList<>(); + for (int i = 1; i < children.size(); i += 2) { + final TBAA.Type innerType = getTBAATypeFromNode(children.get(i)); + final int offset = ((MdGenericValue)children.get(i+1)).value().getValueAsInt(); + typeOffsets.add(new TBAA.TypeOffset(innerType, offset)); + } + final TBAA.StructType typeNode = new TBAA.StructType(name, typeOffsets); + md2tbaaMap.put(tbaaTypeMdNode, typeNode); + } + } + + return md2tbaaMap.get(node); + } + + } + + } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AliasAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AliasAnalysis.java index 05250dcbb6..f9d8d4775e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AliasAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AliasAnalysis.java @@ -47,6 +47,7 @@ static AliasAnalysis fromConfig(Program program, Configuration config) throws In throw new UnsupportedOperationException("Alias method not recognized"); } a = new CombinedAliasAnalysis(a, EqualityAliasAnalysis.fromConfig(program, config)); + a = new CombinedAliasAnalysis(a, TBAA.fromConfig(config)); if (Arch.supportsVirtualAddressing(program.getArch())) { a = VirtualAliasAnalysis.wrap(a); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/TBAA.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/TBAA.java new file mode 100644 index 0000000000..d073c4de97 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/TBAA.java @@ -0,0 +1,120 @@ +package com.dat3m.dartagnan.program.analysis.alias; + +import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; +import com.dat3m.dartagnan.program.event.metadata.Metadata; +import org.sosy_lab.common.configuration.Configuration; + +import java.util.List; +import java.util.stream.Collectors; + +/* + Type-based alias analysis that relies on type annotations provided by metadata (e.g., from LLVM). + This analysis does NOT(!) use the IR's internal type system. + */ +public final class TBAA implements AliasAnalysis { + + private TBAA() {} + + public static AliasAnalysis fromConfig(Configuration config) { + return new TBAA(); + } + + @Override + public boolean mustAlias(MemoryCoreEvent a, MemoryCoreEvent b) { + return false; + } + + @Override + public boolean mayAlias(MemoryCoreEvent a, MemoryCoreEvent b) { + final AccessTag aTag = a.getMetadata(AccessTag.class); + final AccessTag bTag = b.getMetadata(AccessTag.class); + return aTag == null || bTag == null || canAlias(aTag, bTag); + } + + // ================================================================================================ + // Helper methods + + public static boolean canAlias(AccessTag x, AccessTag y) { + if (x == y) { + return true; + } + final TypeOffset xAccess = new TypeOffset(x.base(), x.offset()); + final TypeOffset yAccess = new TypeOffset(y.base(), y.offset()); + + final TypeOffset upper = x.offset() <= y.offset() ? xAccess : yAccess; + TypeOffset lower = (upper == xAccess) ? yAccess : xAccess; + while (lower.offset() > upper.offset()) { + lower = getImmediateParent(lower); + assert lower != null; + } + + return lower.equals(upper); + } + + public static TypeOffset getImmediateParent(TypeOffset typeOffset) { + if (typeOffset.type() instanceof ScalarType scalarType) { + final boolean isRoot = scalarType.parent() == null; + return isRoot ? null : new TypeOffset(scalarType.parent(), typeOffset.offset()); + } else if (typeOffset.type() instanceof StructType structType) { + for (int i = 0; i < structType.offsets().size(); i++) { + final TypeOffset cur = structType.offsets().get(i); + final TypeOffset next = (i + 1) < structType.offsets().size() ? structType.offsets().get(i + 1) : null; + + if (next == null || next.offset() > typeOffset.offset()) { + return new TypeOffset(cur.type(), cur.offset() - typeOffset.offset()); + } + } + } + assert false; + return null; + } + + // ================================================================================================ + // Classes + + public record AccessTag(Type base, Type access, int offset) implements Metadata { + @Override + public String toString() { + return String.format("TBAA.Access( %s, %s, %d )", base.getName(), access.getName(), offset); + } + } + + public interface Type { + String getName(); + } + + public record TypeOffset(Type type, int offset) { + @Override + public String toString() { + return String.format("( %s, %s )", type.getName(), offset); + } + } + + public record ScalarType(String name, Type parent) implements Type { + @Override + public String getName() { + return name; + } + + @Override + public String toString() { + if (parent == null) { + return name; + } + return String.format("TBAA.Scalar{ %s, %s }", name, parent.getName()); + } + } + + public record StructType(String name, List offsets) implements Type { + @Override + public String getName() { + return name; + } + + @Override + public String toString() { + return String.format("TBAA.Struct{ %s, %s }", name, + offsets.stream().map(Object::toString).collect(Collectors.joining(", "))); + } + } +}