TBAA

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<Expression> {
     private final Map<String, TypeDefContext> typeDefinitionMap = new HashMap<>();
     private final Map<String, Type> typeMap = new HashMap<>();
     private final Map<String, MdNode> 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<Metadata> parseMetadataAttachment(List<MetadataAttachmentContext> m
         }
 
         final List<Metadata> 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.<MdReference>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.<MdReference>getField("scope").orElseThrow().mdName());
+                    }
+                    assert scope.nodeType() == SpecialMdTupleNode.Type.DIFile;
+                    final String filename = scope.<MdGenericValue<String>>getField("filename").orElseThrow().value();
+                    final String directory = scope.<MdGenericValue<String>>getField("directory").orElseThrow().value();
+                    final int lineNumber = diLocationNode.<MdGenericValue<BigInteger>>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.<MdGenericValue<String>>getField("filename").orElseThrow().value();
-                final String directory = scope.<MdGenericValue<String>>getField("directory").orElseThrow().value();
-                final int lineNumber = diLocationNode.<MdGenericValue<BigInteger>>getField("line").orElseThrow().value().intValue();
-                metadata.add(new SourceLocation((directory + "/" + filename).intern(), lineNumber));
             }
         }
 
@@ -1463,4 +1477,72 @@ public <T extends MdNode> Optional<T> getField(String fieldName) {
         }
     }
 
+    // ----------------------------------------------------------------------------------------------------------------
+    // TBAA-metadata
+
+    private class TBAABuilder {
+        private final Map<MdNode, TBAA.Type> md2tbaaMap = new HashMap<>();
+        private final Map<MdNode, TBAA.AccessTag> 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<MdNode> 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<IntLiteral>) children.get(2)).value().getValueAsInt();
+                // final int isConstant = ((MdGenericValue<IntLiteral>)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<MdNode> 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<TBAA.TypeOffset> typeOffsets = new ArrayList<>();
+                    for (int i = 1; i < children.size(); i += 2) {
+                        final TBAA.Type innerType = getTBAATypeFromNode(children.get(i));
+                        final int offset = ((MdGenericValue<IntLiteral>)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);
+        }
+
+    }
+
+
 }

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);
         }

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<TypeOffset> 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(", ")));
+        }
+    }
+}