Merge branch 'master' into debt-24-demo-materials

goblint · Sep 13, 2024 · 60be1db · 60be1db
2 parents 3759d3f + 96beec2
commit 60be1db
Show file tree

Hide file tree

Showing 3 changed files with 21 additions and 5 deletions.
diff --git a/src/main/java/abstractdebugging/AbstractDebuggingServer.java b/src/main/java/abstractdebugging/AbstractDebuggingServer.java
@@ -370,9 +370,11 @@ public CompletableFuture<StepInTargetsResponse> stepInTargets(StepInTargetsArgum
                 for (int i = 0; i < cfgEdges.size(); i++) {
                     var edge = cfgEdges.get(i);
                     var node = resultsService.lookupNode(edge.nodeId());
+                    var lval = edge.lval();
+                    lval = lval == null ? "" : " " + domainValueToString(resultsService.evaluateExpression(edge.nodeId(), edge.lval()));
                     forwardTargets.add(target(
                             STEP_OVER_OFFSET + i,
-                            "Step: " + edge.statementDisplayString(),
+                            "Step: " + edge.statementDisplayString() + lval,
                             node.location()
                     ));
                 }
@@ -817,8 +819,8 @@ private void stepAllThreadsIntoMatchingEdge(int primaryThreadId, EdgeInfo primar
         onThreadsStopped("step", primaryThreadId);
     }
 
-    private EdgeInfo findTargetEdge(EdgeInfo primaryTargetEdge, List<? extends EdgeInfo> candidateEdges, String threadName) throws IllegalStepException {
-        // This is will throw if there are multiple distinct target edges with the same target CFG node.
+    private EdgeInfo findTargetEdge(EdgeInfo primaryTargetEdge, List<? extends EdgeInfo> candidateEdges, String threadName) {
+        // This is will make ambiguous threads unavailable if there are multiple distinct target edges with the same target CFG node.
         // TODO: Somehow ensure this can never happen.
         //  Options:
         //  * Throw error (current approach) (problem: might make it impossible to step at all in some cases. it is difficult to provide meaningful error messages for all cases)
@@ -836,7 +838,7 @@ private EdgeInfo findTargetEdge(EdgeInfo primaryTargetEdge, List<? extends EdgeI
                 .filter(e -> e.cfgNodeId().equals(primaryTargetEdge.cfgNodeId()))
                 .toList();
         if (targetEdgesByCFGNode.size() > 1) {
-            throw new IllegalStepException("Path is ambiguous for " + threadName + ".");
+            log.warn("Disabling synchronous stepping in the debugging thread \"" + threadName + "\", as the path there is ambiguous.");
         }
         return targetEdgesByCFGNode.size() == 1 ? targetEdgesByCFGNode.get(0) : null;
     }

diff --git a/src/main/java/abstractdebugging/CFGEdgeInfo.java b/src/main/java/abstractdebugging/CFGEdgeInfo.java
@@ -7,15 +7,28 @@
 public class CFGEdgeInfo extends EdgeInfo {
 
     private final String statementDisplayString;
+    private final String lval;
 
     public CFGEdgeInfo(String nodeId, String cfgNodeId, String contextId, String pathId,
                        String statementDisplayString) {
         super(nodeId, cfgNodeId, contextId, pathId);
+        this.lval = null;
+        this.statementDisplayString = statementDisplayString;
+    }
+
+    public CFGEdgeInfo(String nodeId, String cfgNodeId, String contextId, String pathId,
+                       String statementDisplayString, String lval) {
+        super(nodeId, cfgNodeId, contextId, pathId);
+        this.lval = lval;
         this.statementDisplayString = statementDisplayString;
     }
 
     public final String statementDisplayString() {
         return statementDisplayString;
     }
 
+    public final String lval() {
+        return lval;
+    }
+
 }
diff --git a/src/main/java/api/messages/GoblintARGLookupResult.java b/src/main/java/api/messages/GoblintARGLookupResult.java
@@ -63,8 +63,9 @@ private static void mapEdges(List<Edge> edges, List<CFGEdgeInfo> cfgEdges, List<
         for (var edge : edges) {
             if (edge.edge.cfg != null || edge.edge.inlined != null) {
                 var properties = edge.edge.cfg != null ? edge.edge.cfg : edge.edge.inlined;
+                var lval = properties.get("lval");
                 CFGEdgeInfo edgeInfo = new CFGEdgeInfo(edge.node, edge.cfg_node, edge.context, edge.path,
-                        properties.get("string").getAsString());
+                        properties.get("string").getAsString(), lval == null || lval.isJsonNull() ? null : lval.getAsString());
                 cfgEdges.add(edgeInfo);
             } else if (edge.edge.ret != null) {
                 var properties = edge.edge.ret;