From 00004849c6c276ac46fe54f9a8af780dde326608 Mon Sep 17 00:00:00 2001
From: Natalia Gavrilenko <natgavrilenko@gmail.com>
Date: Sun, 11 Aug 2024 18:02:07 +0200
Subject: [PATCH] Add memory effects to LLVM grammar and better error message

Co-authored-by: Natalia Gavrilenko <natalia.gavrilenko@huawei.com>
---
 dartagnan/src/main/antlr4/LLVMIR.g4              | 12 +++++++++++-
 .../parsers/program/visitors/VisitorLlvm.java    | 16 ++++++++++------
 2 files changed, 21 insertions(+), 7 deletions(-)

diff --git a/dartagnan/src/main/antlr4/LLVMIR.g4 b/dartagnan/src/main/antlr4/LLVMIR.g4
index 79c9168ee3..00b175b6c0 100644
--- 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
index 5e1170623c..71d2eadbf2 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
@@ -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