Merge branch 'llvm-grammar0' of https://github.com/hernanponcedeleon/…

…Dat3M into llvm-grammar0
hernanponcedeleon · Aug 17, 2023 · 20d9f51 · 20d9f51
2 parents b322dcd + 4a321ff
commit 20d9f51
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 9 deletions.
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
@@ -159,6 +159,13 @@ public Expression visitFuncDef(FuncDefContext ctx) {
         // The grammar requires at least one block, thus an entry and an exit.
         for (final BasicBlockContext basicBlockContext : ctx.funcBody().basicBlock()) {
             block = getBlock(basicBlockContext.LabelIdent());
+            final List<Metadata> blockHeaderMetadata;
+            if (basicBlockContext.instruction().size() > 0) {
+                blockHeaderMetadata = parseMetadataAttachment(basicBlockContext.instruction(0).metadataAttachment());
+            } else {
+                blockHeaderMetadata = parseMetadataAttachment(basicBlockContext.terminator().metadataAttachment());
+            }
+            blockHeaderMetadata.forEach(block.label::setMetadata);
             for (final InstructionContext instructionContext : basicBlockContext.instruction()) {
                 parseBlockInstructionWithMetadata(instructionContext, instructionContext.metadataAttachment());
             }
@@ -175,12 +182,18 @@ public Expression visitFuncDef(FuncDefContext ctx) {
             for (final Event event : block.events) {
                 function.append(event);
             }
+
+            final Event terminator = block.events.get(block.events.size() - 1);
             for (final Map.Entry<BlockPair, List<Event>> phiNode : phiNodes.entrySet()) {
-                if (phiNode.getKey().from == block) {
+                final BlockPair blockPair = phiNode.getKey();
+                if (blockPair.from == block) {
                     for (Event event : phiNode.getValue()) {
+                        event.copyAllMetadataFrom(terminator);
                         function.append(event);
                     }
-                    function.append(newGoto(phiNode.getKey().to.label));
+                    final Event gotoTargetBlock = newGoto(blockPair.to.label);
+                    gotoTargetBlock.copyAllMetadataFrom(terminator);
+                    function.append(gotoTargetBlock);
                 }
             }
         }

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/IntrinsicsInsertion.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/IntrinsicsInsertion.java
@@ -48,6 +48,7 @@ public void run(Function function) {
                     case "__VERIFIER_spin_end" -> inlineSpinEnd(call);
                     case "__VERIFIER_atomic_begin" -> inlineAtomicBegin(call);
                     case "__VERIFIER_atomic_end" -> inlineAtomicEnd(call);
+                    case "__VERIFIER_assume" -> inlineAssume(call);
                     case "pthread_mutex_init" -> inlinePthreadMutexInit(call);
                     case "pthread_mutex_lock" -> inlinePthreadMutexLock(call);
                     case "pthread_mutex_unlock" -> inlinePthreadMutexUnlock(call);
@@ -90,6 +91,11 @@ private List<Event> inlineSpinEnd(DirectFunctionCall ignored) {
         return List.of(EventFactory.Svcomp.newSpinEnd());
     }
 
+    private List<Event> inlineAssume(DirectFunctionCall call) {
+        final Expression assumption = call.getArguments().get(0);
+        return List.of(EventFactory.newAssume(assumption));
+    }
+
     private List<Event> inlineAtomicBegin(DirectFunctionCall ignored) {
         return List.of(currentAtomicBegin = EventFactory.Svcomp.newBeginAtomic());
     }

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java
@@ -308,15 +308,15 @@ public Expression visit(Register reg) {
             if (e instanceof AbortIf abort) {
                 final Event jumpToEnd = EventFactory.newJump(abort.getCondition(), threadEnd);
                 jumpToEnd.addTags(abort.getTags());
+                jumpToEnd.copyAllMetadataFrom(abort);
                 abort.replaceBy(jumpToEnd);
             } else if (e instanceof Return ret) {
-                ret.insertAfter(EventFactory.newGoto(threadReturnLabel));
-                if (returnRegister != null) {
-                    ret.insertAfter(EventFactory.newLocal(returnRegister, ret.getValue().get()));
-                }
-                if (!ret.tryDelete()) {
-                    throw new MalformedProgramException("Unable to delete " + ret);
-                }
+                final List<Event> replacement = eventSequence(
+                        returnRegister != null ? EventFactory.newLocal(returnRegister, ret.getValue().get()) : null,
+                        EventFactory.newGoto(threadReturnLabel)
+                );
+                replacement.forEach(ev -> ev.copyAllMetadataFrom(ret));
+                ret.replaceBy(replacement);
             }
         }