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 index 6119bcd54e..2aa75fc0d3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/IntrinsicsInsertion.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/IntrinsicsInsertion.java @@ -3,13 +3,22 @@ import com.dat3m.dartagnan.exception.MalformedProgramException; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; +import com.dat3m.dartagnan.expression.IConst; import com.dat3m.dartagnan.expression.IValue; +import com.dat3m.dartagnan.expression.op.IOpBin; import com.dat3m.dartagnan.program.Function; +import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.EventFactory; +import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.functions.DirectFunctionCall; +import com.dat3m.dartagnan.program.event.functions.DirectValueFunctionCall; import com.dat3m.dartagnan.program.event.lang.svcomp.BeginAtomic; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; + import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkNotNull; @@ -28,81 +37,168 @@ public static IntrinsicsInsertion newInstance() { public void run(Function function) { currentAtomicBegin = null; for (final DirectFunctionCall call : function.getEvents(DirectFunctionCall.class)) { - Event replacement = switch (call.getCallTarget().getName()) { - case "__VERIFIER_loop_begin" -> inlineLoopBegin(call); - case "__VERIFIER_loop_bound" -> inlineLoopBound(call); - case "__VERIFIER_spin_start" -> inlineSpinStart(call); - case "__VERIFIER_spin_end" -> inlineSpinEnd(call); - case "__VERIFIER_atomic_begin" -> inlineAtomicBegin(call); - case "__VERIFIER_atomic_end" -> inlineAtomicEnd(call); - case "pthread_mutex_init" -> inlinePthreadMutexInit(call); - case "pthread_mutex_lock" -> inlinePthreadMutexLock(call); - case "pthread_mutex_unlock" -> inlinePthreadMutexUnlock(call); - case "exit" -> inlineExit(call); - case "printf" -> null; - default -> call; - }; - - if (replacement == null) { + final List replacement; + if (isLKMMIntrinsic(call)) { + replacement = handleLKMMIntrinsic(call); + } else { + replacement = switch (call.getCallTarget().getName()) { + case "__VERIFIER_loop_begin" -> inlineLoopBegin(call); + case "__VERIFIER_loop_bound" -> inlineLoopBound(call); + case "__VERIFIER_spin_start" -> inlineSpinStart(call); + case "__VERIFIER_spin_end" -> inlineSpinEnd(call); + case "__VERIFIER_atomic_begin" -> inlineAtomicBegin(call); + case "__VERIFIER_atomic_end" -> inlineAtomicEnd(call); + case "pthread_mutex_init" -> inlinePthreadMutexInit(call); + case "pthread_mutex_lock" -> inlinePthreadMutexLock(call); + case "pthread_mutex_unlock" -> inlinePthreadMutexUnlock(call); + case "exit" -> inlineExit(call); + case "printf" -> List.of(); + default -> List.of(call); + }; + } + + if (replacement.isEmpty()) { call.tryDelete(); - } else if (call != replacement) { + } else if (replacement.get(0) != call) { call.replaceBy(replacement); - replacement.copyAllMetadataFrom(call); + replacement.forEach(e -> e.copyAllMetadataFrom(call)); } } } - private Event inlineExit(DirectFunctionCall ignored) { - return EventFactory.newAbortIf(ExpressionFactory.getInstance().makeTrue()); + private List inlineExit(DirectFunctionCall ignored) { + return List.of(EventFactory.newAbortIf(ExpressionFactory.getInstance().makeTrue())); } - private Event inlineLoopBegin(DirectFunctionCall ignored) { - return EventFactory.Svcomp.newLoopBegin(); + private List inlineLoopBegin(DirectFunctionCall ignored) { + return List.of(EventFactory.Svcomp.newLoopBegin()); } - private Event inlineLoopBound(DirectFunctionCall call) { + private List inlineLoopBound(DirectFunctionCall call) { final Expression boundExpression = call.getArguments().get(0); if (!(boundExpression instanceof IValue value)) { throw new MalformedProgramException("Non-constant bound for loop."); } - return EventFactory.Svcomp.newLoopBound(value.getValueAsInt()); + return List.of(EventFactory.Svcomp.newLoopBound(value.getValueAsInt())); } - private Event inlineSpinStart(DirectFunctionCall ignored) { - return EventFactory.Svcomp.newSpinStart(); + private List inlineSpinStart(DirectFunctionCall ignored) { + return List.of(EventFactory.Svcomp.newSpinStart()); } - private Event inlineSpinEnd(DirectFunctionCall ignored) { - return EventFactory.Svcomp.newSpinEnd(); + private List inlineSpinEnd(DirectFunctionCall ignored) { + return List.of(EventFactory.Svcomp.newSpinEnd()); } - private Event inlineAtomicBegin(DirectFunctionCall ignored) { - return currentAtomicBegin = EventFactory.Svcomp.newBeginAtomic(); + private List inlineAtomicBegin(DirectFunctionCall ignored) { + return List.of(currentAtomicBegin = EventFactory.Svcomp.newBeginAtomic()); } - private Event inlineAtomicEnd(DirectFunctionCall ignored) { - return EventFactory.Svcomp.newEndAtomic(checkNotNull(currentAtomicBegin)); + private List inlineAtomicEnd(DirectFunctionCall ignored) { + return List.of(EventFactory.Svcomp.newEndAtomic(checkNotNull(currentAtomicBegin))); } - private Event inlinePthreadMutexInit(DirectFunctionCall call) { + private List inlinePthreadMutexInit(DirectFunctionCall call) { checkArgument(call.getArguments().size() == 2); final Expression lockAddress = call.getArguments().get(0); final Expression lockValue = call.getArguments().get(1); final String lockName = lockAddress.toString(); - return EventFactory.Pthread.newInitLock(lockName, lockAddress, lockValue); + return List.of(EventFactory.Pthread.newInitLock(lockName, lockAddress, lockValue)); } - private Event inlinePthreadMutexLock(DirectFunctionCall call) { + private List inlinePthreadMutexLock(DirectFunctionCall call) { checkArgument(call.getArguments().size() == 1); final Expression lockAddress = call.getArguments().get(0); final String lockName = lockAddress.toString(); - return EventFactory.Pthread.newLock(lockName, lockAddress); + return List.of(EventFactory.Pthread.newLock(lockName, lockAddress)); } - private Event inlinePthreadMutexUnlock(DirectFunctionCall call) { + private List inlinePthreadMutexUnlock(DirectFunctionCall call) { checkArgument(call.getArguments().size() == 1); final Expression lockAddress = call.getArguments().get(0); final String lockName = lockAddress.toString(); - return EventFactory.Pthread.newUnlock(lockName, lockAddress); + return List.of(EventFactory.Pthread.newUnlock(lockName, lockAddress)); + } + + // -------------------------------------------------------------------------------------------------------- + // LKMM intrinsics + + private static final List LKMMPROCEDURES = Arrays.asList( + "__LKMM_LOAD", + "__LKMM_STORE", + "__LKMM_XCHG", + "__LKMM_CMPXCHG", + "__LKMM_ATOMIC_FETCH_OP", + "__LKMM_ATOMIC_OP", + "__LKMM_ATOMIC_OP_RETURN", + "__LKMM_FENCE", + "__LKMM_SPIN_LOCK", + "__LKMM_SPIN_UNLOCK"); + + private boolean isLKMMIntrinsic(DirectFunctionCall call) { + return LKMMPROCEDURES.contains(call.getCallTarget().getName()); + } + + private List handleLKMMIntrinsic(DirectFunctionCall call) { + final Register reg = (call instanceof DirectValueFunctionCall valueCall) ? valueCall.getResultRegister() : null; + final List args = call.getArguments(); + + final Expression p0 = args.get(0); + final Expression p1 = args.size() > 1 ? args.get(1) : null; + final Expression p2 = args.size() > 2 ? args.get(2) : null; + final Expression p3 = args.size() > 3 ? args.get(3) : null; + + String mo; + IOpBin op; + List result = new ArrayList<>(); + switch (call.getCallTarget().getName()) { + case "__LKMM_LOAD" -> { + mo = Tag.Linux.intToMo(((IConst) p1).getValueAsInt()); + result.add(EventFactory.Linux.newLKMMLoad(reg, p0, mo)); + } + case "__LKMM_STORE" -> { + mo = Tag.Linux.intToMo(((IConst) p2).getValueAsInt()); + result.add(EventFactory.Linux.newLKMMStore(p0, p1, mo.equals(Tag.Linux.MO_MB) ? Tag.Linux.MO_ONCE : mo)); + if (mo.equals(Tag.Linux.MO_MB)) { + result.add(EventFactory.Linux.newMemoryBarrier()); + } + } + case "__LKMM_XCHG" -> { + mo = Tag.Linux.intToMo(((IConst) p2).getValueAsInt()); + result.add(EventFactory.Linux.newRMWExchange(p0, reg, p1, mo)); + } + case "__LKMM_CMPXCHG" -> { + mo = Tag.Linux.intToMo(((IConst) p3).getValueAsInt()); + result.add(EventFactory.Linux.newRMWCompareExchange(p0, reg, p1, p2, mo)); + } + case "__LKMM_ATOMIC_FETCH_OP" -> { + mo = Tag.Linux.intToMo(((IConst) p2).getValueAsInt()); + op = IOpBin.intToOp(((IConst) p3).getValueAsInt()); + result.add(EventFactory.Linux.newRMWFetchOp(p0, reg, p1, op, mo)); + } + case "__LKMM_ATOMIC_OP_RETURN" -> { + mo = Tag.Linux.intToMo(((IConst) p2).getValueAsInt()); + op = IOpBin.intToOp(((IConst) p3).getValueAsInt()); + result.add(EventFactory.Linux.newRMWOpReturn(p0, reg, p1, op, mo)); + } + case "__LKMM_ATOMIC_OP" -> { + op = IOpBin.intToOp(((IConst) p2).getValueAsInt()); + result.add(EventFactory.Linux.newRMWOp( p0, p1, op)); + } + case "__LKMM_FENCE" -> { + String fence = Tag.Linux.intToMo(((IConst) p0).getValueAsInt()); + result.add(EventFactory.Linux.newLKMMFence(fence)); + } + case "__LKMM_SPIN_LOCK" -> { + result.add(EventFactory.Linux.newLock(p0)); + } + case "__LKMM_SPIN_UNLOCK" -> { + result.add(EventFactory.Linux.newUnlock(p0)); + } + default -> { + assert false; + } + } + return result; } } 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 index bbe7fbe787..73c3158c4c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java @@ -179,7 +179,10 @@ private void handlePthreadJoins(Thread thread, Map tid2ComAd for (DirectFunctionCall call : thread.getEvents(DirectFunctionCall.class)) { final String targetName = call.getCallTarget().getName(); - if (!(targetName.equals("pthread_join") || targetName.equals("__pthread_join"))) { + if (!(targetName.equals("pthread_join") + // The following two calls can be generated on macOS + || targetName.equals("__pthread_join") + || targetName.equals("\"\\01_pthread_join\""))) { continue; }