tmp

hernanponcedeleon · Nov 20, 2024 · b43a52c · b43a52c
1 parent 207053d
commit b43a52c
Show file tree

Hide file tree

Showing 2 changed files with 97 additions and 127 deletions.
diff --git a/.../src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvVulkan.java b/.../src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvVulkan.java
@@ -1,5 +1,6 @@
 package com.dat3m.dartagnan.program.processing.compilation;
 
+import com.dat3m.dartagnan.exception.ParsingException;
 import com.dat3m.dartagnan.program.event.Event;
 import com.dat3m.dartagnan.program.event.EventFactory;
 import com.dat3m.dartagnan.program.event.Tag;
@@ -46,6 +47,7 @@ public List<Event> visitSpirvLoad(SpirvLoad e) {
         load.addTags(Tag.Vulkan.ATOM);
         load.addTags(toVulkanTags(e.getTags()));
         replaceAcqRelTag(load, Tag.Vulkan.ACQUIRE);
+        validateSemanticsTags(load.getTags());
         return eventSequence(load);
     }
 
@@ -58,6 +60,7 @@ public List<Event> visitSpirvStore(SpirvStore e) {
         store.addTags(Tag.Vulkan.ATOM);
         store.addTags(toVulkanTags(e.getTags()));
         replaceAcqRelTag(store, Tag.Vulkan.RELEASE);
+        validateSemanticsTags(store.getTags());
         return eventSequence(store);
     }
 
@@ -70,6 +73,7 @@ public List<Event> visitSpirvXchg(SpirvXchg e) {
                 e.getValue(), mo, scope);
         rmw.addTags(toVulkanTags(e.getTags()));
         replaceAcqRelTag(rmw, Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE);
+        validateSemanticsTags(rmw.getTags());
         rmw.setFunction(e.getFunction());
         return visitVulkanRMW(rmw);
     }
@@ -81,9 +85,10 @@ public List<Event> visitSpirvRMW(SpirvRmw e) {
         String scope = toVulkanTag(Tag.Spirv.getScopeTag(e.getTags()));
         VulkanRMWOp rmwOp = EventFactory.Vulkan.newRMWOp(e.getAddress(), e.getResultRegister(),
                 e.getOperand(), e.getOperator(), mo, scope);
-        rmwOp.setFunction(e.getFunction());
         rmwOp.addTags(toVulkanTags(e.getTags()));
         replaceAcqRelTag(rmwOp, Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE);
+        validateSemanticsTags(rmwOp.getTags());
+        rmwOp.setFunction(e.getFunction());
         return visitVulkanRMWOp(rmwOp);
     }
 
@@ -108,6 +113,7 @@ public List<Event> visitSpirvCmpXchg(SpirvCmpXchg e) {
         cmpXchg.setFunction(e.getFunction());
         cmpXchg.addTags(toVulkanTags(eqTags));
         replaceAcqRelTag(cmpXchg, Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE);
+        validateSemanticsTags(cmpXchg.getTags());
 
         return visitVulkanCmpXchg(cmpXchg);
     }
@@ -122,6 +128,7 @@ public List<Event> visitSpirvRmwExtremum(SpirvRmwExtremum e) {
         rmw.setFunction(e.getFunction());
         rmw.addTags(toVulkanTags(e.getTags()));
         replaceAcqRelTag(rmw, Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE);
+        validateSemanticsTags(rmw.getTags());
         return visitVulkanRMWExtremum(rmw);
     }
 
@@ -131,6 +138,7 @@ public List<Event> visitGenericVisibleEvent(GenericVisibleEvent e) {
         fence.removeTags(fence.getTags());
         fence.addTags(toVulkanTags(e.getTags()));
         replaceAcqRelTag(fence, Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE);
+        validateSemanticsTags(fence.getTags());
         return eventSequence(fence);
     }
 
@@ -140,6 +148,7 @@ public List<Event> visitControlBarrier(ControlBarrier e) {
         barrier.removeTags(barrier.getTags());
         barrier.addTags(toVulkanTags(e.getTags()));
         replaceAcqRelTag(barrier, Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE);
+        validateSemanticsTags(barrier.getTags());
         return eventSequence(barrier);
     }
 
@@ -158,6 +167,23 @@ private Set<String> toVulkanTags(Set<String> tags) {
         return vTags;
     }
 
+    private void validateSemanticsTags(Set<String> tags) {
+        boolean hasMoTags = tags.contains(Tag.Vulkan.ACQUIRE) || tags.contains(Tag.Vulkan.RELEASE) || tags.contains(Tag.Vulkan.ACQ_REL);
+        boolean hasSemScTags = tags.contains(Tag.Vulkan.SEMSC0) || tags.contains(Tag.Vulkan.SEMSC1);
+        if (hasMoTags && !hasSemScTags) {
+            throw new ParsingException("Non-relaxed semantics must have storage class semantics tags");
+        }
+        if (hasSemScTags && !hasMoTags) {
+            throw new ParsingException("Storage class semantics requires memory order tags");
+        }
+        if (tags.contains(Tag.Vulkan.SEM_AVAILABLE) && !tags.contains(Tag.Vulkan.RELEASE) && !tags.contains(Tag.Vulkan.ACQ_REL)) {
+            throw new ParsingException("Available semantics must have release tag");
+        }
+        if (tags.contains(Tag.Vulkan.SEM_VISIBLE) && !tags.contains(Tag.Vulkan.ACQUIRE) && !tags.contains(Tag.Vulkan.ACQ_REL)) {
+            throw new ParsingException("Visible semantics must have acquire tag");
+        }
+    }
+
     private void replaceAcqRelTag(Event e, String... tags) {
         if (e.getTags().contains(Tag.Vulkan.ACQ_REL)) {
             e.addTags(tags);