Add support for memcpy_s (#686)

Signed-off-by: Hernan Ponce de Leon <[email protected]>
Co-authored-by: Hernan Ponce de Leon <[email protected]>

benchmarks/c/miscellaneous/memcpy_s.c

@@ -0,0 +1,62 @@
+#include <assert.h>
+#include <stddef.h>
+
+#ifdef __STDC_LIB_EXT1__
+    #define __STDC_WANT_LIB_EXT1__ 1
+    #include <string.h>
+#else
+    #define rsize_t size_t
+    #define errno_t int
+    extern errno_t memcpy_s( void *restrict dest, rsize_t destsz, const void *restrict src, rsize_t count );
+#endif
+
+int main()
+{
+    int a[4] = { 1, 2, 3, 4 };
+    int b[3] = { 5, 6, 7};
+
+    int ret;
+
+    // NULL dest
+    ret = memcpy_s(NULL, 3*sizeof(int), a, 3*sizeof(int));
+    assert(ret > 0);
+
+    // NULL src
+    ret = memcpy_s(b, 3*sizeof(int), NULL, 3*sizeof(int));
+    assert(ret > 0);
+    assert(b[0] == 0);
+    assert(b[1] == 0);
+    assert(b[2] == 0);
+    b[0] = 5;
+    b[1] = 6;
+    b[2] = 7;
+
+    // count > destsz
+    ret = memcpy_s(b, 2*sizeof(int), a, 4*sizeof(int));
+    assert(ret > 0);
+    assert(b[0] == 0);
+    assert(b[1] == 0);
+    // only [dest, dest+destsz) is zeroed
+    assert(b[2] == 7);
+    b[0] = 5;
+    b[1] = 6;
+
+    // Overlapping src and dest
+    ret = memcpy_s(b, 3*sizeof(int), b, 3*sizeof(int));
+    assert(ret > 0);
+    assert(b[0] == 0);
+    assert(b[1] == 0);
+    assert(b[2] == 0);
+    b[0] = 5;
+    b[1] = 6;
+    b[2] = 7;
+
+    // Success
+    ret = memcpy_s(b, 3*sizeof(int), a, 3*sizeof(int));
+    assert(ret == 0);
+    assert(b[0] == 1);
+    assert(b[1] == 2);
+    assert(b[2] == 3);
+
+	return 0;
+}

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java

@@ -15,8 +15,10 @@
 import com.dat3m.dartagnan.program.event.Event;
 import com.dat3m.dartagnan.program.event.EventFactory;
 import com.dat3m.dartagnan.program.event.Tag;
+import com.dat3m.dartagnan.program.event.core.CondJump;
 import com.dat3m.dartagnan.program.event.core.ExecutionStatus;
 import com.dat3m.dartagnan.program.event.core.Label;
+import com.dat3m.dartagnan.program.event.core.Local;
 import com.dat3m.dartagnan.program.event.functions.FunctionCall;
 import com.dat3m.dartagnan.program.event.functions.ValueFunctionCall;
 import com.dat3m.dartagnan.program.event.lang.svcomp.BeginAtomic;
@@ -209,6 +211,7 @@ public enum Info {
         LKMM_FENCE("__LKMM_FENCE", false, false, false, true, Intrinsics::handleLKMMIntrinsic),
         // --------------------------- Misc ---------------------------
         STD_MEMCPY("memcpy", true, true, true, false, Intrinsics::inlineMemCpy),
+        STD_MEMCPYS("memcpy_s", true, true, true, false, Intrinsics::inlineMemCpyS),
         STD_MEMSET(List.of("memset", "__memset_chk"), true, false, true, false, Intrinsics::inlineMemSet),
         STD_MEMCMP("memcmp", false, true, true, false, Intrinsics::inlineMemCmp),
         STD_MALLOC("malloc", false, false, true, true, Intrinsics::inlineMalloc),
@@ -1328,6 +1331,116 @@ private List<Event> inlineMemCpy(FunctionCall call) {
         return replacement;
     }
 
+    // https://en.cppreference.com/w/c/string/byte/memcpy
+    private List<Event> inlineMemCpyS(FunctionCall call) {
+        // Cast guaranteed to success by the return type of memcpy_s
+        final Register resultRegister = ((ValueFunctionCall)call).getResultRegister();
+        final Function caller = call.getFunction();
+        final Expression dest = call.getArguments().get(0);
+        final Expression destszExpr = call.getArguments().get(1);
+        final Expression src = call.getArguments().get(2);
+        final Expression countExpr = call.getArguments().get(3);
+
+        // TODO remove these two checks once we support dynamically-sized memcpy
+        if (!(countExpr instanceof IntLiteral countValue)) {
+            final String error = "Cannot handle memcpy_s with dynamic count argument: " + call;
+            throw new UnsupportedOperationException(error);
+        }
+        final int count = countValue.getValueAsInt();
+        if (!(destszExpr instanceof IntLiteral destszValue)) {
+            final String error = "Cannot handle memcpy_s with dynamic destsz argument: " + call;
+            throw new UnsupportedOperationException(error);
+        }
+        final int destsz = destszValue.getValueAsInt();
+
+        // Runtime checks
+        final Expression nullExpr = expressions.makeZero(types.getArchType());
+        final Expression destIsNull = expressions.makeEQ(dest, nullExpr);
+        final Expression srcIsNull = expressions.makeEQ(src, nullExpr);
+
+        // We assume RSIZE_MAX = 2^64-1
+        final Expression rsize_max = expressions.makeValue(BigInteger.ONE.shiftLeft(64).subtract(BigInteger.ONE), types.getArchType());
+        // These parameters have type rsize_t/size_t which we model as types.getArchType(), thus the cast
+        final Expression castDestszExpr = expressions.makeCast(destszExpr, types.getArchType());
+        final Expression castCountExpr = expressions.makeCast(countExpr, types.getArchType());
+
+        final Expression invalidDestsz = expressions.makeGT(castDestszExpr, rsize_max, false);
+        final Expression countGtMax = expressions.makeGT(castCountExpr, rsize_max, false);
+        final Expression countGtdestszExpr = expressions.makeGT(castCountExpr, castDestszExpr, false);
+        final Expression invalidCount = expressions.makeOr(countGtMax, countGtdestszExpr);
+        final Expression overlap = expressions.makeAnd(
+                expressions.makeGT(expressions.makeAdd(src, castCountExpr), dest, false),
+                expressions.makeGT(expressions.makeAdd(dest, castCountExpr), src, false));
+
+        final List<Event> replacement = new ArrayList<>();
+
+        Label check1 = EventFactory.newLabel("__memcpy_s_check_1");
+        Label check2 = EventFactory.newLabel("__memcpy_s_check_2");
+        Label success = EventFactory.newLabel("__memcpy_s_success");
+        Label end = EventFactory.newLabel("__memcpy_s_end");
+
+        Expression errorCodeFail = expressions.makeOne((IntegerType)resultRegister.getType());
+        Expression errorCodeSuccess = expressions.makeZero((IntegerType)resultRegister.getType());
+
+        // Condition 1: dest == NULL or destsz > RSIZE_MAX ----> return error > 0
+        final Expression cond1 = expressions.makeOr(destIsNull, invalidDestsz);
+        CondJump skipE1 = EventFactory.newJump(expressions.makeNot(cond1), check2);
+        CondJump skipRest1 = EventFactory.newGoto(end);
+        Local retError1 = EventFactory.newLocal(resultRegister, errorCodeFail);
+        replacement.addAll(List.of(
+            check1,
+            skipE1,
+            retError1,
+            skipRest1
+        ));
+
+        // Condition 2: dest != NULL && destsz <= RSIZE_MAX && (src == NULL || count > destsz || overlap(src, dest)) 
+        // ----> return error > 0 and zero out [dest, dest+destsz)
+        // The first two are guaranteed by not matching cond1
+        final Expression cond2 = expressions.makeOr(expressions.makeOr(srcIsNull, invalidCount), overlap);
+        CondJump skipE2 = EventFactory.newJump(expressions.makeNot(cond2), success);
+        CondJump skipRest2 = EventFactory.newGoto(end);
+        Local retError2 = EventFactory.newLocal(resultRegister, errorCodeFail);
+        replacement.addAll(List.of(
+            check2,
+            skipE2
+        ));
+        for (int i = 0; i < destsz; i++) {
+            final Expression offset = expressions.makeValue(i, types.getArchType());
+            final Expression destAddr = expressions.makeAdd(dest, offset);
+            final Expression zero = expressions.makeZero(types.getArchType());
+            replacement.add(
+                EventFactory.newStore(destAddr, zero)
+            );
+        }
+        replacement.addAll(List.of(
+            retError2,
+            skipRest2
+        ));
+
+        // Else ----> return error = 0 and do the actual copy
+        Local retSuccess = EventFactory.newLocal(resultRegister, errorCodeSuccess);
+        replacement.add(success);        
+        for (int i = 0; i < count; i++) {
+            final Expression offset = expressions.makeValue(i, types.getArchType());
+            final Expression srcAddr = expressions.makeAdd(src, offset);
+            final Expression destAddr = expressions.makeAdd(dest, offset);
+            // FIXME: We have no other choice but to load ptr-sized chunks for now
+            final Register reg = caller.getOrNewRegister("__memcpy_" + i, types.getArchType());
+
+            replacement.addAll(List.of(
+                    EventFactory.newLoad(reg, srcAddr),
+                    EventFactory.newStore(destAddr, reg)
+            ));
+        }
+        replacement.addAll(List.of(
+            retSuccess,
+            end
+        ));
+
+        return replacement;
+    }
+
     private List<Event> inlineMemCmp(FunctionCall call) {
         final Function caller = call.getFunction();
         final Expression src1 = call.getArguments().get(0);

dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java

@@ -85,7 +85,8 @@ public static Iterable<Object[]> data() throws IOException {
                 {"funcPtrInStaticMemory", IMM, PASS, 1},
                 {"verifierAssert", ARM8, FAIL, 1},
                 {"uninitRead", IMM, FAIL, 1},
-                {"multipleBackJumps", IMM, UNKNOWN, 1}
+                {"multipleBackJumps", IMM, UNKNOWN, 1},
+                {"memcpy_s", IMM, PASS, 1}
         });
     }