Merge branch 'development' into ptx-constant

hernanponcedeleon · Oct 22, 2023 · c29e3bf · c29e3bf
2 parents f978c91 + 00045b2
commit c29e3bf
Show file tree

Hide file tree

Showing 3 changed files with 373 additions and 7 deletions.
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java
@@ -3,11 +3,7 @@
 import com.dat3m.dartagnan.exception.MalformedProgramException;
 import com.dat3m.dartagnan.expression.*;
 import com.dat3m.dartagnan.expression.op.IOpBin;
-import com.dat3m.dartagnan.expression.type.BooleanType;
-import com.dat3m.dartagnan.expression.type.FunctionType;
-import com.dat3m.dartagnan.expression.type.IntegerType;
-import com.dat3m.dartagnan.expression.type.Type;
-import com.dat3m.dartagnan.expression.type.TypeFactory;
+import com.dat3m.dartagnan.expression.type.*;
 import com.dat3m.dartagnan.program.Function;
 import com.dat3m.dartagnan.program.Program;
 import com.dat3m.dartagnan.program.Register;
@@ -122,7 +118,8 @@ public enum Info {
                 "llvm.ctlz", "llvm.ctpop"),
                 false, false, true, true, Intrinsics::handleLLVMIntrinsic),
         LLVM_ASSUME("llvm.assume", false, false, true, true, Intrinsics::inlineLLVMAssume),
-        LLVM_STACK(List.of("llvm.stacksave", "llvm.stackrestore"), false, false, true, true, Intrinsics::inlineAsZero),
+        LLVM_META(List.of("llvm.stacksave", "llvm.stackrestore", "llvm.lifetime"), false, false, true, true, Intrinsics::inlineAsZero),
+        LLVM_EXPECT("llvm.expect", false, false, true, true, Intrinsics::inlineLLVMExpect),
         LLVM_MEMCPY("llvm.memcpy", true, true, true, false, Intrinsics::inlineMemCpy),
         LLVM_MEMSET("llvm.memset", true, false, true, false, Intrinsics::inlineMemSet),
         // --------------------------- LKMM ---------------------------
@@ -192,7 +189,7 @@ public boolean isEarly() {
 
         private boolean matches(String funcName) {
             boolean isPrefix = switch(this) {
-                case LLVM, LLVM_ASSUME, LLVM_STACK, LLVM_MEMCPY, LLVM_MEMSET -> true;
+                case LLVM, LLVM_ASSUME, LLVM_META, LLVM_MEMCPY, LLVM_MEMSET, LLVM_EXPECT -> true;
                 default -> false;
             };
             BiPredicate<String, String> matchingFunction = isPrefix ? String::startsWith : String::equals;
@@ -394,6 +391,13 @@ private List<Event> handleLLVMIntrinsic(FunctionCall call) {
         }
     }
 
+    private List<Event> inlineLLVMExpect(FunctionCall call) {
+        assert call instanceof ValueFunctionCall;
+        final Register retReg = ((ValueFunctionCall) call).getResultRegister();
+        final Expression value = call.getArguments().get(0);
+        return List.of(EventFactory.newLocal(retReg, value));
+    }
+
     private List<Event> inlineLLVMAssume(FunctionCall call) {
         //see https://llvm.org/docs/LangRef.html#llvm-assume-intrinsic
         return List.of(EventFactory.newAssume(call.getArguments().get(0)));