add support to show source location in witness graph for spirv

Signed-off-by: Tianrui Zheng <[email protected]>
hernanponcedeleon · Sep 16, 2024 · cc43073 · cc43073
1 parent 9a23ab0
commit cc43073
Show file tree

Hide file tree

Showing 3 changed files with 67 additions and 2 deletions.
diff --git a/...nan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsDebug.java b/...nan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsDebug.java
@@ -1,15 +1,44 @@
 package com.dat3m.dartagnan.parsers.program.visitors.spirv;
 
 import com.dat3m.dartagnan.parsers.SpirvBaseVisitor;
+import com.dat3m.dartagnan.parsers.SpirvParser;
 import com.dat3m.dartagnan.parsers.program.visitors.spirv.builders.ProgramBuilder;
+import com.dat3m.dartagnan.parsers.program.visitors.spirv.builders.ControlFlowBuilder;
+import com.dat3m.dartagnan.program.event.metadata.SourceLocation;
 
 import java.util.Set;
 
 public class VisitorOpsDebug extends SpirvBaseVisitor<Void> {
 
+    private final ProgramBuilder builder;
+    private final ControlFlowBuilder cfBuilder;
+
     public VisitorOpsDebug(ProgramBuilder builder) {
-        // TODO: Implement mapping to original variable names
-        //  and lines of code (readability for human users)
+        this.builder = builder;
+        this.cfBuilder = builder.getControlFlowBuilder();
+    }
+
+    @Override
+    public Void visitOpString(SpirvParser.OpStringContext ctx) {
+        String id = ctx.idResult().getText();
+        String str = ctx.string().getText();
+        builder.addDebugInfo(id, str);
+        return null;
+    }
+
+    @Override
+    public Void visitOpLine(SpirvParser.OpLineContext ctx) {
+        String file = builder.getDebugInfo(ctx.file().getText());
+        int line = Integer.parseInt(ctx.line().getText());
+        SourceLocation loc = new SourceLocation(file, line);
+        cfBuilder.setCurrentLocation(loc);
+        return null;
+    }
+
+    @Override
+    public Void visitOpNoLine(SpirvParser.OpNoLineContext ctx) {
+        cfBuilder.removeCurrentLocation();
+        return null;
     }
 
     public Set<String> getSupportedOps() {

diff --git a/.../java/com/dat3m/dartagnan/parsers/program/visitors/spirv/builders/ControlFlowBuilder.java b/.../java/com/dat3m/dartagnan/parsers/program/visitors/spirv/builders/ControlFlowBuilder.java
@@ -6,6 +6,7 @@
 import com.dat3m.dartagnan.program.event.Event;
 import com.dat3m.dartagnan.program.event.EventFactory;
 import com.dat3m.dartagnan.program.event.core.Label;
+import com.dat3m.dartagnan.program.event.metadata.SourceLocation;
 import com.google.common.collect.Sets;
 
 import java.util.*;
@@ -18,6 +19,7 @@ public class ControlFlowBuilder {
     protected final Deque<String> blockStack = new ArrayDeque<>();
     protected final Map<String, Map<Register, String>> phiDefinitions = new HashMap<>();
     protected final Map<String, Expression> expressions;
+    protected SourceLocation currentLocation;
 
     public ControlFlowBuilder(Map<String, Expression> expressions) {
         this.expressions = expressions;
@@ -54,6 +56,7 @@ public Event endBlock(Event event) {
             throw new ParsingException("Attempt to exit block while not in a block definition");
         }
         lastBlockEvents.put(blockStack.pop(), event);
+        removeCurrentLocation();
         return event;
     }
 
@@ -71,6 +74,21 @@ public void addPhiDefinition(String blockId, Register register, String expressio
         phiDefinitions.computeIfAbsent(blockId, k -> new HashMap<>()).put(register, expressionId);
     }
 
+    public SourceLocation getCurrentLocation() {
+        if (currentLocation == null) {
+            throw new ParsingException("No source location for the instruction");
+        }
+        return currentLocation;
+    }
+
+    public void setCurrentLocation(SourceLocation loc) { currentLocation = loc; }
+
+    public void removeCurrentLocation() { currentLocation = null; }
+
+    public boolean hasCurrentLocation() {
+        return currentLocation != null;
+    }
+
     private void validateBeforeBuild() {
         if (!blockStack.isEmpty()) {
             throw new ParsingException("Unclosed blocks %s", String.join(",", blockStack));

diff --git a/...main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/builders/ProgramBuilder.java b/...main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/builders/ProgramBuilder.java
@@ -26,6 +26,7 @@ public class ProgramBuilder {
     protected final Map<String, Type> types = new HashMap<>();
     protected final Map<String, Expression> expressions = new HashMap<>();
     protected final Map<String, Expression> inputs = new HashMap<>();
+    protected final Map<String, String> debugInfos = new HashMap<>();
     protected final ThreadGrid grid;
     protected final Program program;
     protected ControlFlowBuilder controlFlowBuilder;
@@ -191,6 +192,9 @@ public Event addEvent(Event event) {
         if (!controlFlowBuilder.isInsideBlock()) {
             throw new ParsingException("Attempt to add an event outside a control flow block");
         }
+        if (controlFlowBuilder.hasCurrentLocation()) {
+            event.setMetadata(controlFlowBuilder.getCurrentLocation());
+        }
         if (event instanceof RegWriter regWriter) {
             Register register = regWriter.getResultRegister();
             addExpression(register.getName(), register);
@@ -228,6 +232,20 @@ public void endCurrentFunction() {
         currentFunction = null;
     }
 
+    public void addDebugInfo(String id, String info) {
+        if (debugInfos.containsKey(id)) {
+            throw new ParsingException("Attempt to add debug information with duplicate id");
+        }
+        debugInfos.put(id, info);
+    }
+
+    public String getDebugInfo(String id) {
+        if (!debugInfos.containsKey(id)) {
+            throw new ParsingException("No debug information with id '%s'", id);
+        }
+        return debugInfos.get(id);
+    }
+
     private void validateBeforeBuild() {
         if (nextOps != null) {
             throw new ParsingException("Missing expected op: %s",