Simplify IR Manipulation operations (#803)

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/builders/ControlFlowBuilder.java

@@ -41,7 +41,7 @@ public void build() {
                     Event event = EventFactory.newLocal(k, expressions.get(v));
                     SourceLocation loc = getPhiLocation(blockId, k);
                     if (loc != null) { event.setMetadata(loc); }
-                    lastBlockEvents.get(blockId).getPredecessor().insertAfter(event);
+                    lastBlockEvents.get(blockId).insertBefore(event);
                 }));
     }
 

dartagnan/src/main/java/com/dat3m/dartagnan/program/Function.java

@@ -6,10 +6,14 @@
 import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.expression.type.VoidType;
 import com.dat3m.dartagnan.program.event.Event;
+import com.dat3m.dartagnan.program.event.RegReader;
+import com.dat3m.dartagnan.program.event.RegWriter;
 import com.dat3m.dartagnan.program.event.core.CondJump;
 import com.dat3m.dartagnan.program.event.core.Label;
+import com.dat3m.dartagnan.program.event.lang.llvm.LlvmCmpXchg;
 import com.dat3m.dartagnan.program.processing.Intrinsics;
 import com.google.common.base.Preconditions;
+import com.google.common.collect.Iterables;
 
 import java.util.*;
 import java.util.stream.Collectors;
@@ -138,7 +142,8 @@ public Register getOrNewRegister(String name, Type type) {
         return found;
     }
 
-    public void append(Event event){
+    public void append(Event event) {
+        Preconditions.checkNotNull(event);
         if (entry == null) {
             entry = exit = event;
             event.setFunction(this);
@@ -149,12 +154,32 @@ public void append(Event event){
         }
     }
 
-    public void updateExit(Event event){
-        exit = event;
-        Event next;
-        while((next = exit.getSuccessor()) != null){
-            exit = next;
+    public void append(Iterable<? extends Event> events) {
+        if (Iterables.isEmpty(events)) {
+            return;
+        } else if (exit == null) {
+            append(Iterables.getFirst(events, null));
+            events = Iterables.skip(events, 1);
         }
+        exit.insertAfter(events);
+    }
+
+    public void updateExit(Event event) {
+        Preconditions.checkArgument(event.getFunction() == this);
+        Event cur = event;
+        while (cur.getSuccessor() != null) {
+            cur = cur.getSuccessor();
+        }
+        exit = cur;
+    }
+
+    public void updateEntry(Event event) {
+        Preconditions.checkArgument(event.getFunction() == this);
+        Event cur = event;
+        while (cur.getPredecessor() != null) {
+            cur = cur.getPredecessor();
+        }
+        entry = cur;
     }
 
     public void validate() {
@@ -179,6 +204,24 @@ public void validate() {
                     throw new MalformedProgramException(error);
                 }
             }
+
+            final Set<Register> registers = new HashSet<>(getRegisters());
+            if (ev instanceof RegReader reader) {
+                reader.getRegisterReads().stream()
+                        .filter(read -> !registers.contains(read.register())).findFirst().ifPresent(read -> {
+                            final String error = String.format("Event %s of function %s reads from external register %s of" +
+                                            "function %s .", reader, this, read.register(), read.register().getFunction()
+                            );
+                            throw new MalformedProgramException(error);
+                        });
+            }
+
+            if (ev instanceof RegWriter writer && !(writer instanceof LlvmCmpXchg) && !registers.contains(writer.getResultRegister())) {
+                final String error = String.format("Event %s of function %s writes to external register %s of function %s",
+                        writer, this, writer.getResultRegister(), writer.getResultRegister().getFunction()
+                );
+                throw new MalformedProgramException(error);
+            }
         }
     }
 

dartagnan/src/main/java/com/dat3m/dartagnan/program/IRHelper.java

@@ -1,18 +1,40 @@
 package com.dat3m.dartagnan.program;
 
+import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.expression.booleans.BoolLiteral;
+import com.dat3m.dartagnan.expression.processing.ExprTransformer;
 import com.dat3m.dartagnan.program.event.Event;
+import com.dat3m.dartagnan.program.event.EventUser;
+import com.dat3m.dartagnan.program.event.RegReader;
+import com.dat3m.dartagnan.program.event.RegWriter;
 import com.dat3m.dartagnan.program.event.core.CondJump;
 import com.dat3m.dartagnan.program.event.functions.AbortIf;
 import com.dat3m.dartagnan.program.event.functions.Return;
+import com.dat3m.dartagnan.program.event.lang.llvm.LlvmCmpXchg;
+import com.google.common.base.Preconditions;
+import com.google.common.base.Verify;
 
-import java.util.HashSet;
-import java.util.Set;
+import java.util.*;
+import java.util.function.Consumer;
 
 public class IRHelper {
 
     private IRHelper() {}
 
+    public static boolean isBackJump(CondJump jump) {
+        return jump.getLocalId() > jump.getLabel().getLocalId();
+    }
+
+    /*
+        Returns true if the syntactic successor of <e> (e.getSuccessor()) is not (generally) a semantic successor,
+        because <e> always jumps/branches/terminates etc.
+    */
+    public static boolean isAlwaysBranching(Event e) {
+        return e instanceof Return
+                || e instanceof AbortIf abort && abort.getCondition() instanceof BoolLiteral b && b.getValue()
+                || e instanceof CondJump jump && jump.isGoto();
+    }
+
     public static Set<Event> bulkDelete(Set<Event> toBeDeleted) {
         final Set<Event> nonDeleted = new HashSet<>();
         for (Event e : toBeDeleted) {
@@ -25,13 +47,91 @@ public static Set<Event> bulkDelete(Set<Event> toBeDeleted) {
         return nonDeleted;
     }
 
-    /*
-        Returns true if the syntactic successor of <e> (e.getSuccessor()) is not (generally) a semantic successor,
-        because <e> always jumps/branches/terminates etc.
-     */
-    public static boolean isAlwaysBranching(Event e) {
-        return e instanceof Return
-                || e instanceof AbortIf abort && abort.getCondition() instanceof BoolLiteral b && b.getValue()
-                || e instanceof CondJump jump && jump.isGoto();
+    public static Event replaceWithMetadata(Event event, Event replacement) {
+        event.replaceBy(replacement);
+        replacement.copyAllMetadataFrom(event);
+        return replacement;
+    }
+
+    public static List<Event> replaceWithMetadata(Event event, List<Event> replacement) {
+        event.replaceBy(replacement);
+        replacement.forEach(ev -> ev.copyAllMetadataFrom(event));
+        return replacement;
+    }
+
+    public static List<Event> getEventsFromTo(Event from, Event to, boolean endInclusive) {
+        Preconditions.checkArgument(from.getFunction() == to.getFunction());
+        final List<Event> events = new ArrayList<>();
+        Event cur = from;
+        do {
+            final boolean endReached = (cur == to);
+            if (!endReached || endInclusive) {
+                events.add(cur);
+            }
+            if (endReached) {
+                break;
+            }
+            cur = cur.getSuccessor();
+        } while (cur != null);
+        Verify.verify(cur != null, "Event '{}' is not before '{}'", from, to);
+
+        return events;
+    }
+
+    public static List<Event> copyEvents(Collection<? extends Event> events,
+                                         Consumer<Event> copyUpdater,
+                                         Map<Event, Event> copyContext) {
+        final List<Event> copies = new ArrayList<>();
+        for (Event e : events) {
+            final Event copy = e.getCopy();
+            copyUpdater.accept(copy);
+            copies.add(copy);
+            copyContext.put(e, copy);
+        }
+
+        copies.stream().filter(EventUser.class::isInstance).map(EventUser.class::cast)
+                .forEach(user -> user.updateReferences(copyContext));
+
+        return copies;
+    }
+
+    public static List<Event> copyPath(Event from, Event toExclusive,
+                                       Consumer<Event> copyUpdater,
+                                       Map<Event, Event> copyContext) {
+        return copyEvents(getEventsFromTo(from, toExclusive, false), copyUpdater, copyContext);
+    }
+
+    public static Consumer<Event> makeRegisterReplacer(Map<Register, Register> regReplacer) {
+        final ExprTransformer regSubstitutor =  new ExprTransformer() {
+            @Override
+            public Expression visitRegister(Register reg) {
+                return regReplacer.getOrDefault(reg, reg);
+            }
+        };
+        return event -> {
+            if (event instanceof RegReader reader) {
+                reader.transformExpressions(regSubstitutor);
+            }
+            if (event instanceof LlvmCmpXchg xchg) {
+                xchg.setStructRegister(0, (Register)xchg.getStructRegister(0).accept(regSubstitutor));
+                xchg.setStructRegister(1, (Register)xchg.getStructRegister(1).accept(regSubstitutor));
+            } else if (event instanceof RegWriter regWriter) {
+                regWriter.setResultRegister((Register) regWriter.getResultRegister().accept(regSubstitutor));
+            }
+        };
+    }
+
+    public static Map<Register, Register> copyOverRegisters(Iterable<Register> toCopy, Function target,
+                                                            java.util.function.Function<Register, String> registerRenaming,
+                                                            boolean guaranteeFreshRegisters) {
+        final Map<Register, Register> registerMap = new HashMap<>();
+        for (Register reg : toCopy) {
+            final String name = registerRenaming.apply(reg);
+            final Register copiedReg = guaranteeFreshRegisters ?
+                    target.newRegister(name, reg.getType())
+                    : target.getOrNewRegister(name, reg.getType());
+            registerMap.put(reg, copiedReg);
+        }
+        return registerMap;
     }
 }

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/AbstractEvent.java

@@ -160,21 +160,25 @@ public final List<Event> getPredecessors() {
     /*
         Detaches this event from the control-flow graph.
         This does not properly delete the event, and it may be reinserted elsewhere.
-        TODO: We need to special-case handle detaching the entry event of a function.
+        TODO: We should handle the edge-case where a function becomes empty after detaching.
      */
     @Override
     public void detach() {
-        Preconditions.checkState(function == null || this != function.getEntry(),
-                "Cannot detach the entry event %s of function %s", this, getFunction());
+        Preconditions.checkState(function == null || function.getEntry() != function.getExit(),
+                "Cannot detach the only event %s of function %s", this, getFunction());
         if (this.predecessor != null) {
             this.predecessor.successor = successor;
         }
         if (this.successor != null) {
             this.successor.predecessor = predecessor;
         }
+        if (function != null && this == function.getEntry()) {
+            function.updateEntry(this.successor);
+        }
         if (function != null && this == function.getExit()) {
             function.updateExit(this.predecessor);
         }
+
         this.function = null;
         this.predecessor = null;
         this.successor = null;
@@ -201,21 +205,31 @@ public boolean tryDelete() {
     @Override
     public void insertAfter(Event toBeInserted) {
         Preconditions.checkNotNull(toBeInserted);
-        insertBetween((AbstractEvent) toBeInserted, function, this, successor);
-        if (function.getExit() == this) {
-            function.updateExit(toBeInserted);
-        }
+        insertBetween((AbstractEvent) toBeInserted, function, this, this.successor);
     }
 
     @Override
-    public void insertAfter(List<Event> toBeInserted) {
+    public void insertAfter(Iterable<? extends Event> toBeInserted) {
         Event cur = this;
         for (Event next : toBeInserted) {
             cur.insertAfter(next);
             cur = next;
         }
     }
 
+    @Override
+    public void insertBefore(Event toBeInserted) {
+        Preconditions.checkNotNull(toBeInserted);
+        insertBetween((AbstractEvent) toBeInserted, function, this.predecessor, this);
+    }
+
+    @Override
+    public void insertBefore(Iterable<? extends Event> toBeInserted) {
+        for (Event next : toBeInserted) {
+            this.insertBefore(next);
+        }
+    }
+
     @Override
     public void replaceBy(Event replacement) {
         if (replacement == this) {
@@ -227,7 +241,7 @@ public void replaceBy(Event replacement) {
     }
 
     @Override
-    public void replaceBy(List<Event> replacement) {
+    public void replaceBy(Iterable<? extends Event> replacement) {
         Preconditions.checkState(currentUsers.isEmpty(), "Cannot replace event that is still in use.");
         this.insertAfter(replacement);
         this.forceDelete();
@@ -243,10 +257,16 @@ private static void insertBetween(AbstractEvent toBeInserted, Function func, Abs
 
         if (pred != null) {
             pred.successor = toBeInserted;
+        } else if (func != null) {
+            func.updateEntry(toBeInserted);
         }
+
         if (succ != null) {
             succ.predecessor = toBeInserted;
+        } else if (func != null) {
+            func.updateExit(toBeInserted);
         }
+
     }
 
     // ===============================================================================================

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Event.java

@@ -71,10 +71,13 @@ public interface Event extends Encoder, Comparable<Event> {
     void detach();
     void forceDelete(); // DANGEROUS: Deletes the event, including all events that reference it.
     boolean tryDelete(); // Deletes the event only if no other event references it.
+
     void insertAfter(Event toBeInserted);
-    void insertAfter(List<Event> toBeInserted);
+    void insertBefore(Event toBeInserted);
     void replaceBy(Event replacement);
-    void replaceBy(List<Event> replacement);
+    void insertAfter(Iterable<? extends Event> toBeInserted);
+    void insertBefore(Iterable<? extends Event> toBeInserted);
+    void replaceBy(Iterable<? extends Event> replacement);
 
     // ============================== Misc ==============================