Optimize event extraction

Signed-off-by: Tianrui Zheng <[email protected]>
hernanponcedeleon · Nov 27, 2024 · 5a7238d · 5a7238d
1 parent d76b53a
commit 5a7238d
Show file tree

Hide file tree

Showing 15 changed files with 109 additions and 147 deletions.
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelNext.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelNext.java
@@ -41,8 +41,8 @@ public class ExecutionModelNext {
         atomicBlocksMap = new HashMap<>();
     }
 
-    public void addThreadEvents(Thread thread, List<EventModel> events) {
-        threadList.add(new ThreadModel(thread, events));
+    public void addThread(ThreadModel tModel) {
+        threadList.add(tModel);
     }
 
     public void addEvent(Event e, EventModel eModel) {
@@ -93,7 +93,7 @@ public List<EventModel> getEventList() {
     }
 
     public List<EventModel> getVisibleEventList() {
-        return eventList.stream().filter(e -> e.hasTag(Tag.VISIBLE)).toList();
+        return eventList.stream().filter(e -> e.isVisible()).toList();
     }
 
     public List<EventModel> getEventsByFilter(Filter filter) {

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ThreadModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ThreadModel.java
@@ -6,32 +6,41 @@
 
 import java.util.Collections;
 import java.util.List;
+import java.util.ArrayList;
 
 
 public class ThreadModel {
     private final Thread thread;
     private final List<EventModel> eventList;
 
-    public ThreadModel(Thread thread, List<EventModel> eventList) {
+    public ThreadModel(Thread thread) {
         this.thread = thread;
-        this.eventList = eventList;
+        this.eventList = new ArrayList<>();
+    }
+
+    public void addEvent(EventModel event) {
+        eventList.add(event);
     }
 
     public int getId() {
         return thread.getId();
     }
 
+    public String getName() {
+        return thread.getName();
+    }
+
     public List<EventModel> getEventList() {
         return Collections.unmodifiableList(eventList);
     }
 
     public List<EventModel> getVisibleEventList() {
-        return eventList.stream().filter(e -> e.hasTag(Tag.VISIBLE)).toList();
+        return eventList.stream().filter(e -> e.isVisible()).toList();
     }
 
     public List<EventModel> getEventModelsToShow() {
         return eventList.stream()
-                        .filter(e -> e.hasTag(Tag.VISIBLE) || e.isLocal() || e.isAssert())
+                        .filter(e -> e.isVisible() || e.isLocal() || e.isAssert())
                         .toList();
     }
 }
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/AssertModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/AssertModel.java
@@ -3,13 +3,14 @@
 import com.dat3m.dartagnan.program.Register.Read;
 import com.dat3m.dartagnan.program.event.RegReader;
 import com.dat3m.dartagnan.program.event.core.Assert;
+import com.dat3m.dartagnan.verification.model.ThreadModel;
 
 import java.util.Set;
 
 
 public class AssertModel extends DefaultEventModel implements RegReaderModel {
-    public AssertModel(Assert event) {
-        super(event);
+    public AssertModel(Assert event, ThreadModel thread, int id) {
+        super(event, thread, id);
     }
 
     @Override

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/CondJumpModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/CondJumpModel.java
@@ -5,14 +5,15 @@
 import com.dat3m.dartagnan.program.event.RegReader;
 import com.dat3m.dartagnan.program.event.core.CondJump;
 import com.dat3m.dartagnan.program.event.core.IfAsJump;
+import com.dat3m.dartagnan.verification.model.ThreadModel;
 
 import java.util.Set;
 import java.util.List;
 
 
 public class CondJumpModel extends DefaultEventModel implements RegReaderModel {
-    public CondJumpModel(CondJump event) {
-        super(event);
+    public CondJumpModel(CondJump event, ThreadModel thread, int id) {
+        super(event, thread, id);
     }
 
     public List<Event> getDependentEvents() {

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/DefaultEventModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/DefaultEventModel.java
@@ -1,22 +1,25 @@
 package com.dat3m.dartagnan.verification.model.event;
 
-import com.dat3m.dartagnan.program.Thread;
 import com.dat3m.dartagnan.program.event.core.*;
 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.verification.model.ThreadModel;
 
 import static com.dat3m.dartagnan.program.event.Tag.*;
 
 
 public class DefaultEventModel implements EventModel {
     protected final Event event;
+    protected final ThreadModel thread;
     protected int id = -1;
-    protected int localId = -1;
-    protected boolean executed;
 
-    public DefaultEventModel(Event event) {
+    public DefaultEventModel(Event event, ThreadModel thread, int id) {
         this.event = event;
+        this.thread = thread;
+        this.id = id;
+
+        thread.addEvent(this);
     }
 
     @Override
@@ -25,40 +28,15 @@ public Event getEvent() {
     }
 
     @Override
-    public Thread getThread() {
-        return event.getThread();
+    public ThreadModel getThread() {
+        return thread;
     }
 
     @Override
     public int getId() {
         return id;
     }
 
-    @Override
-    public void setId(int id) {
-        this.id = id;
-    }
-
-    @Override
-    public int getLocalId() {
-        return localId;
-    }
-
-    @Override
-    public void setLocalId(int localId) {
-        this.localId = localId;
-    }
-
-    @Override
-    public boolean wasExecuted() {
-        return executed;
-    }
-
-    @Override
-    public void setWasExecuted(boolean executed) {
-        this.executed = executed;
-    }
-
     @Override
     public boolean isMemoryEvent() { return event.hasTag(MEMORY); }
 
@@ -80,6 +58,9 @@ public void setWasExecuted(boolean executed) {
     @Override
     public boolean isRMW() { return event.hasTag(RMW); }
 
+    @Override
+    public boolean isVisible() { return event.hasTag(VISIBLE); }
+
     @Override
     public boolean isJump() { return event instanceof CondJump; }
 
@@ -95,11 +76,6 @@ public void setWasExecuted(boolean executed) {
     @Override
     public boolean isRegWriter() { return event instanceof RegWriter; }
 
-    @Override
-    public boolean hasTag(String tag) {
-    	return event.hasTag(tag);
-    }
-
     @Override
     public int hashCode() {
         return id;
@@ -113,7 +89,7 @@ public boolean equals(Object obj) {
 
     @Override
     public String toString() {
-        return String.format("T%d:%d", event.getThread().getId(), localId);
+        return String.format("T%d/E%d", thread.getId(), id);
     }
 
     @Override

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/EventModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/EventModel.java
@@ -1,22 +1,15 @@
 package com.dat3m.dartagnan.verification.model.event;
 
-import com.dat3m.dartagnan.program.Thread;
 import com.dat3m.dartagnan.program.event.Event;
+import com.dat3m.dartagnan.verification.model.ThreadModel;
 
 
 public interface EventModel extends Comparable<EventModel> {
     Event getEvent();
 
-    Thread getThread();
+    ThreadModel getThread();
 
     int getId();
-    void setId(int id);
-
-    int getLocalId();
-    void setLocalId(int localId);
-
-    boolean wasExecuted();
-    void setWasExecuted(boolean executed);
 
     boolean isMemoryEvent();
     boolean isInit();
@@ -25,10 +18,10 @@ public interface EventModel extends Comparable<EventModel> {
     boolean isFence();
     boolean isExclusive();
     boolean isRMW();
+    boolean isVisible();
     boolean isJump();
     boolean isAssert();
     boolean isLocal();
     boolean isRegReader();
     boolean isRegWriter();
-    boolean hasTag(String tag);
 }