Add memory effects to LLVM grammar and better error message

Co-authored-by: Natalia Gavrilenko <[email protected]>
hernanponcedeleon · Aug 11, 2024 · 0000484 · 0000484
1 parent 6582d4a
commit 0000484
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 7 deletions.
diff --git a/dartagnan/src/main/antlr4/LLVMIR.g4 b/dartagnan/src/main/antlr4/LLVMIR.g4
@@ -740,7 +740,17 @@ funcAttr:
 	| 'sspstrong'
 	| 'strictfp'
 	| 'willreturn'
-	| 'writeonly';
+	| 'writeonly'
+	| 'memory(' memoryEffect+ ')';
+memoryEffect
+    : accessKind
+    | 'argmem:' accessKind
+    | 'inaccessiblemem:' accessKind;
+accessKind
+    : 'none'
+    | 'readwrite'
+    | 'read'
+    | 'write';
 distinct: 'distinct';
 inBounds: 'inbounds';
 returnAttr:

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
@@ -241,13 +241,17 @@ public void visitGlobalDeclaration(GlobalDefContext ctx) {
         final String name = globalIdent(ctx.GlobalIdent());
         check(!constantMap.containsKey(name), "Redeclared constant in %s.", ctx);
         final int size = types.getMemorySizeInBytes(parseType(ctx.type()));
-        final MemoryObject globalObject = program.getMemory().allocate(size);
-        globalObject.setName(name);
-        if (ctx.threadLocal() != null) {
-            globalObject.setIsThreadLocal(true);
+        if (size > 0) {
+            final MemoryObject globalObject = program.getMemory().allocate(size);
+            globalObject.setName(name);
+            if (ctx.threadLocal() != null) {
+                globalObject.setIsThreadLocal(true);
+            }
+            // TODO: mark the global as constant, if possible.
+            constantMap.put(name, globalObject);
+            return;
         }
-        // TODO: mark the global as constant, if possible.
-        constantMap.put(name, globalObject);
+        throw new ParsingException(String.format("Cannot compute memory size for '%s'", name));
     }
 
     @Override