Fix devirtualization (#557)

* Replaced exception with warning if no target for a dynamic call can be statically determined. Added assertion in the case that an execution dynamically reaches a dynamic call with an invalid function pointer. Added #annotations to program logging.
hernanponcedeleon · Nov 8, 2023 · ac85ae3 · ac85ae3
1 parent 44caf20
commit ac85ae3
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 6 deletions.
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LogThreadStatistics.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LogThreadStatistics.java
@@ -2,8 +2,8 @@
 
 import com.dat3m.dartagnan.program.Program;
 import com.dat3m.dartagnan.program.Thread;
-import com.dat3m.dartagnan.program.event.Tag;
 import com.dat3m.dartagnan.program.event.core.*;
+import com.dat3m.dartagnan.program.event.core.annotations.CodeAnnotation;
 import com.dat3m.dartagnan.program.memory.MemoryObject;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
@@ -30,6 +30,7 @@ public void run(Program program) {
         int loadCount = 0;
         int initCount = 0;
         int otherVisibleCount = 0;
+        int annotationCount = 0;
         for (Thread thread : threads) {
             for (Event e : thread.getEvents()) {
                 totalEventCount++;
@@ -41,6 +42,8 @@ public void run(Program program) {
                     loadCount++;
                 } else if (e instanceof GenericVisibleEvent) {
                     otherVisibleCount++;
+                } else if (e instanceof CodeAnnotation) {
+                    annotationCount++;
                 }
             }
         }
@@ -56,6 +59,7 @@ public void run(Program program) {
         output.append("\n======== Program statistics ========").append("\n");
         output.append("#Threads: ").append(numNonInitThreads).append("\n")
                 .append("#Events: ").append(totalEventCount).append("\n")
+                .append("\t#Annotations: ").append(annotationCount).append("\n")
                 .append("\t#Stores: ").append(storeCount).append("\n")
                 .append("\t#Loads: ").append(loadCount).append("\n")
                 .append("\t#Inits: ").append(initCount).append("\n")

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveDevirtualisation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveDevirtualisation.java
@@ -1,6 +1,5 @@
 package com.dat3m.dartagnan.program.processing;
 
-import com.dat3m.dartagnan.exception.MalformedProgramException;
 import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.expression.ExpressionFactory;
 import com.dat3m.dartagnan.expression.IValue;
@@ -144,8 +143,7 @@ private void devirtualise(Function function, Map<Function, IValue> func2AddressM
                 }
 
                 if (possibleTargets.isEmpty()) {
-                    final String error = String.format("Cannot resolve dynamic call \"%s\", no matching functions found.", call);
-                    throw new MalformedProgramException(error);
+                    logger.warn("Cannot resolve dynamic call \"{}\", no matching functions found.", call);
                 }
 
                 logger.trace("Devirtualizing call \"{}\" with possible targets: {}", call, possibleTargets);
@@ -162,8 +160,7 @@ private void devirtualise(Function function, Map<Function, IValue> func2AddressM
                     caseJumps.add(caseJump);
                 }
 
-                // FIXME: This should be an "assert(false)"
-                final Event noMatch = EventFactory.newAbortIf(expressions.makeTrue());
+                final Event noMatch = EventFactory.newAssert(expressions.makeFalse(), "Invalid function pointer");
                 final Label endLabel = EventFactory.newLabel(String.format("__Ldevirt_end#%s", devirtCounter));
 
                 final List<Event> callReplacement = new ArrayList<>();