Merge branch 'development_rework' into merge

# Conflicts: # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/PthreadsProcedures.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/StdProcedures.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/SvcompProcedures.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/VisitorBoogie.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java
hernanponcedeleon · Jul 11, 2023 · d418c28 · d418c28
2 parents 1363c3f + 0dd7003
commit d418c28
Show file tree

Hide file tree

Showing 6 changed files with 9 additions and 76 deletions.
diff --git a/...src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/PthreadsProcedures.java b/...src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/PthreadsProcedures.java
@@ -6,44 +6,20 @@
 import com.dat3m.dartagnan.parsers.BoogieParser.ExprsContext;
 import com.dat3m.dartagnan.program.event.EventFactory;
 
-import java.util.Arrays;
-import java.util.List;
-
 public class PthreadsProcedures {
 
-    public static List<String> PTHREADPROCEDURES = Arrays.asList(
-            "pthread_create",
-            "pthread_cond_init",
-            "pthread_cond_wait",
-            "pthread_cond_signal",
-            "pthread_cond_broadcast",
-            "pthread_exit",
-            "pthread_getspecific",
-            "pthread_join",
-            "__pthread_join", // generated by Clang on MacOS
-            "pthread_key_create",
-            "pthread_mutex_init",
-            "pthread_mutex_destroy",
-            "pthread_mutex_lock",
-            "pthread_mutex_unlock",
-            "pthread_setspecific"
-    );
-
     public static boolean handlePthreadsFunctions(VisitorBoogie visitor, Call_cmdContext ctx) {
         final String funcName = visitor.getFunctionNameFromCallContext(ctx);
         switch (funcName) {
-            case "pthread_create":
-            case "__pthread_join":
-            case "pthread_join":
-                // These are handled by a dedicated pass
-                return false;
             case "pthread_cond_init":
             case "pthread_cond_wait":
             case "pthread_cond_signal":
             case "pthread_cond_broadcast":
             case "pthread_exit":
             case "pthread_mutex_destroy":
                 // TODO: These are skipped for now
+                VisitorBoogie.logger.warn(
+                        "Skipped call to {} because the function is not supported right now.", funcName);
                 return true;
             case "pthread_mutex_init":
                 mutexInit(visitor, ctx);
@@ -55,6 +31,7 @@ public static boolean handlePthreadsFunctions(VisitorBoogie visitor, Call_cmdCon
                 mutexUnlock(visitor, ctx);
                 return true;
             default:
+                // pthread_create and pthread_join are handled by a dedicated pass, so we skip them here.
                 return false;
         }
     }

diff --git a/...gnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/StdProcedures.java b/...gnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/StdProcedures.java
@@ -6,37 +6,8 @@
 import com.dat3m.dartagnan.program.Register;
 import com.dat3m.dartagnan.program.event.EventFactory;
 
-import java.util.Arrays;
-import java.util.List;
-
 public class StdProcedures {
 
-    public static List<String> STDPROCEDURES = Arrays.asList(
-            "abort",
-            "devirtbounce",
-            "external_alloc",
-            "$alloc",
-            "__assert_rtn", // generated on MacOS
-            "assert_.i32",
-            "__assert_fail",
-            "$malloc",
-            "calloc",
-            "malloc",
-            "fopen",
-            "free",
-            "memcpy",
-            "$memcpy",
-            "memset",
-            "$memset",
-            "nvram_read_byte",
-            "strcpy",
-            "strcmp",
-            "strncpy",
-            "llvm.stackrestore",
-            "llvm.stacksave",
-            "llvm.lifetime.start",
-            "llvm.lifetime.end");
-
     public static boolean handleStdFunction(VisitorBoogie visitor, Call_cmdContext ctx) {
         final String funcName = visitor.getFunctionNameFromCallContext(ctx);
         if (funcName.equals("$alloc") || funcName.equals("$malloc") || funcName.equals("calloc")

diff --git a/...n/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/SvcompProcedures.java b/...n/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/SvcompProcedures.java
@@ -7,22 +7,10 @@
 import com.dat3m.dartagnan.program.event.EventFactory;
 import com.dat3m.dartagnan.program.event.lang.svcomp.BeginAtomic;
 
-import java.util.Arrays;
-import java.util.List;
+import java.math.BigInteger;
 
 public class SvcompProcedures {
 
-    public static List<String> SVCOMPPROCEDURES = Arrays.asList(
-            "reach_error", // Only used in SVCOMP
-            "__VERIFIER_assert",
-            "__VERIFIER_assume",
-            "__VERIFIER_loop_bound",
-            "__VERIFIER_loop_begin",
-            "__VERIFIER_spin_start",
-            "__VERIFIER_spin_end",
-            "__VERIFIER_atomic_begin",
-            "__VERIFIER_atomic_end");
-
     public static boolean handleSvcompFunction(VisitorBoogie visitor, Call_cmdContext ctx) {
         final String funcName = visitor.getFunctionNameFromCallContext(ctx);
         switch (funcName) {

diff --git a/...gnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/VisitorBoogie.java b/...gnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/VisitorBoogie.java
@@ -51,7 +51,7 @@
 
 public class VisitorBoogie extends BoogieBaseVisitor<Object> {
 
-    private static final Logger logger = LogManager.getLogger(VisitorBoogie.class);
+    protected static final Logger logger = LogManager.getLogger(VisitorBoogie.class);
 
     protected final ProgramBuilder programBuilder = ProgramBuilder.forLanguage(Program.SourceLanguage.BOOGIE);
     protected final TypeFactory types = programBuilder.getTypeFactory();

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java
@@ -54,11 +54,11 @@ public void run(Program program) {
         }
     }
 
-    private void inlineAllCalls(Function thread) {
+    private void inlineAllCalls(Function function) {
         int scopeCounter = 0;
         Map<Event, List<DirectFunctionCall>> exitToCallMap = new HashMap<>();
         // Iteratively replace the first call.
-        Event event = thread.getEntry();
+        Event event = function.getEntry();
         while (event != null) {
             exitToCallMap.remove(event);
             // Work with successor because when calls get removed, the loop variable would be invalidated.
@@ -67,6 +67,7 @@ private void inlineAllCalls(Function thread) {
                 continue;
             }
             // Check whether recursion bound was reached.
+            // FIXME: The recursion check does not work
             exitToCallMap.computeIfAbsent(call.getSuccessor(), k -> new ArrayList<>()).add(call);
             long depth = exitToCallMap.values().stream().filter(c -> c.contains(call)).count();
             if (depth > bound) {
@@ -100,7 +101,7 @@ static void inlineBodyAfterCall(Event entry, Register result, List<Expression> a
         var registerMap = new HashMap<Register, Register>();
         assert arguments.size() == callTarget.getFunctionType().getParameterTypes().size();
         // All registers have to be replaced
-        for (Register register : callTarget.getRegisters()) {
+        for (Register register : List.copyOf(callTarget.getRegisters())) {
             String newName = scope + ":" + register.getName();
             registerMap.put(register, entry.getFunction().newRegister(newName, register.getType()));
         }
@@ -122,7 +123,6 @@ static void inlineBodyAfterCall(Event entry, Register result, List<Expression> a
             }
         }
 
-        //
         for (Event event : inlinedBody) {
             if (event instanceof EventUser user) {
                 user.updateReferences(replacementMap);

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
@@ -91,9 +91,6 @@ public void run(Program program) {
         if (program.getFormat().equals(Program.SourceLanguage.LITMUS)) {
             return;
         }
-        // TODO: test code
-        program.getThreads().clear(); // Clear old threads and create new ones
-        // TODO -----------
 
         final TypeFactory types = TypeFactory.getInstance();
         final ExpressionFactory expressions = ExpressionFactory.getInstance();