llvm: memcmp, strcmp, strncmp

crucible-llvm-cli/test-data/memcmp.cbl

@@ -0,0 +1,100 @@
+(declare @memcmp ((s1 (Ptr 64)) (s2 (Ptr 64)) (n (Bitvector 64))) (Bitvector 32))
+(declare @write-c-string ((dst Pointer) (src (String Unicode))) Unit)
+
+(defun @main () Unit
+  (start start:
+    ;; memcmp of equal strings
+    (let hello1 (alloca none (bv 64 6)))
+    (let hello2 (alloca none (bv 64 6)))
+    (funcall @write-c-string hello1 "Hello")
+    (funcall @write-c-string hello2 "Hello")
+    (let r1 (funcall @memcmp hello1 hello2 (bv 64 5)))
+    (assert! (equal? r1 (bv 32 0)) "memcmp('Hello', 'Hello', 5) == 0")
+
+    ;; memcmp with length 0 should always return 0
+    (let abc (alloca none (bv 64 4)))
+    (let xyz (alloca none (bv 64 4)))
+    (funcall @write-c-string abc "abc")
+    (funcall @write-c-string xyz "xyz")
+    (let r2 (funcall @memcmp abc xyz (bv 64 0)))
+    (assert! (equal? r2 (bv 32 0)) "memcmp with length 0 returns 0")
+
+    ;; memcmp with partial comparison - equal prefix
+    (let hello (alloca none (bv 64 7)))
+    (let help (alloca none (bv 64 7)))
+    (funcall @write-c-string hello "Hello!")
+    (funcall @write-c-string help "Help!!")
+    ;; Compare only first 3 bytes - should be equal
+    (let r3 (funcall @memcmp hello help (bv 64 3)))
+    (assert! (equal? r3 (bv 32 0)) "memcmp('Hello!', 'Help!!', 3) == 0")
+
+    ;; memcmp with single byte - equal
+    (let a1 (alloca none (bv 64 1)))
+    (let a2 (alloca none (bv 64 1)))
+    (let a (ptr 8 0 (bv 8 97))) ; 'a'
+    (store none i8 a1 a)
+    (store none i8 a2 a)
+    (let r4 (funcall @memcmp a1 a2 (bv 64 1)))
+    (assert! (equal? r4 (bv 32 0)) "memcmp('a', 'a', 1) == 0")
+
+    ;; memcmp with aliased strings (same pointer)
+    (let aliased (alloca none (bv 64 6)))
+    (funcall @write-c-string aliased "Hello")
+    (let r6 (funcall @memcmp aliased aliased (bv 64 5)))
+    (assert! (equal? r6 (bv 32 0)) "memcmp(ptr, ptr, n) == 0")
+
+    ;; memcmp('a', 'b') returns negative value
+    (let a4 (alloca none (bv 64 1)))
+    (let b2 (alloca none (bv 64 1)))
+    (let byte-a2 (ptr 8 0 (bv 8 97))) ; 'a'
+    (let byte-b2 (ptr 8 0 (bv 8 98))) ; 'b'
+    (store none i8 a4 byte-a2)
+    (store none i8 b2 byte-b2)
+    (let r7 (funcall @memcmp a4 b2 (bv 64 1)))
+    (assert! (<$ r7 (bv 32 0)) "memcmp('a', 'b', 1) < 0")
+
+    ;; memcmp('b', 'a') returns positive value
+    (let b3 (alloca none (bv 64 1)))
+    (let a5 (alloca none (bv 64 1)))
+    (let byte-b3 (ptr 8 0 (bv 8 98))) ; 'b'
+    (let byte-a3 (ptr 8 0 (bv 8 97))) ; 'a'
+    (store none i8 b3 byte-b3)
+    (store none i8 a5 byte-a3)
+    (let r8 (funcall @memcmp b3 a5 (bv 64 1)))
+    (assert! (<$ (bv 32 0) r8) "memcmp('b', 'a', 1) > 0")
+
+    ;; memcmp with null bytes in the middle - equal
+    ;; This tests that memcmp compares the full length, not stopping at null
+    (let buf1 (alloca none (bv 64 3)))
+    (let buf2 (alloca none (bv 64 3)))
+    ;; Store "a\0b" in buf1
+    (let byte-a (ptr 8 0 (bv 8 97)))   ; 'a'
+    (let byte-0 (ptr 8 0 (bv 8 0)))    ; '\0'
+    (let byte-b (ptr 8 0 (bv 8 98)))   ; 'b'
+    (store none i8 buf1 byte-a)
+    (let buf1-plus-1 (ptr-add-offset buf1 (bv 64 1)))
+    (store none i8 buf1-plus-1 byte-0)
+    (let buf1-plus-2 (ptr-add-offset buf1 (bv 64 2)))
+    (store none i8 buf1-plus-2 byte-b)
+    ;; Store "a\0b" in buf2
+    (store none i8 buf2 byte-a)
+    (let buf2-plus-1 (ptr-add-offset buf2 (bv 64 1)))
+    (store none i8 buf2-plus-1 byte-0)
+    (let buf2-plus-2 (ptr-add-offset buf2 (bv 64 2)))
+    (store none i8 buf2-plus-2 byte-b)
+    (let r9 (funcall @memcmp buf1 buf2 (bv 64 3)))
+    (assert! (equal? r9 (bv 32 0)) "memcmp('a\\0b', 'a\\0b', 3) == 0")
+
+    ;; memcmp with null bytes in the middle - different
+    ;; Compare "a\0b" with "a\0c" - should differ at the third byte
+    (let buf3 (alloca none (bv 64 3)))
+    (let byte-c (ptr 8 0 (bv 8 99)))   ; 'c'
+    (store none i8 buf3 byte-a)
+    (let buf3-plus-1 (ptr-add-offset buf3 (bv 64 1)))
+    (store none i8 buf3-plus-1 byte-0)
+    (let buf3-plus-2 (ptr-add-offset buf3 (bv 64 2)))
+    (store none i8 buf3-plus-2 byte-c)
+    (let r10 (funcall @memcmp buf1 buf3 (bv 64 3)))
+    (assert! (<$ r10 (bv 32 0)) "memcmp('a\\0b', 'a\\0c', 3) < 0")
+
+    (return ())))

crucible-llvm-cli/test-data/memcmp.out.good

@@ -0,0 +1,4 @@
+==== Begin Simulation ====
+
+==== Finish Simulation ====
+==== No proof obligations ====

crucible-llvm-cli/test-data/strcmp.cbl

@@ -0,0 +1,53 @@
+(declare @strcmp ((s1 (Ptr 64)) (s2 (Ptr 64))) (Bitvector 32))
+(declare @write-c-string ((dst Pointer) (src (String Unicode))) Unit)
+
+(defun @main () Unit
+  (start start:
+    (let hello1 (alloca none (bv 64 6)))
+    (let hello2 (alloca none (bv 64 6)))
+    (funcall @write-c-string hello1 "Hello")
+    (funcall @write-c-string hello2 "Hello")
+
+    (let abc (alloca none (bv 64 4)))
+    (funcall @write-c-string abc "abc")
+
+    (let xyz (alloca none (bv 64 4)))
+    (funcall @write-c-string xyz "xyz")
+
+    (let empty1 (alloca none (bv 64 1)))
+    (let empty2 (alloca none (bv 64 1)))
+    (funcall @write-c-string empty1 "")
+    (funcall @write-c-string empty2 "")
+
+    (let ab (alloca none (bv 64 3)))
+    (funcall @write-c-string ab "ab")
+
+    ;; strcmp of equal strings
+    (let r1 (funcall @strcmp hello1 hello2))
+    (assert! (equal? r1 (bv 32 0)) "strcmp('Hello', 'Hello') == 0")
+
+    ;; strcmp of different strings - first is less
+    (let r2 (funcall @strcmp abc xyz))
+    (assert! (<$ r2 (bv 32 0)) "strcmp('abc', 'xyz') < 0")
+
+    ;; strcmp of different strings - first is greater
+    (let r3 (funcall @strcmp xyz abc))
+    (assert! (<$ (bv 32 0) r3) "strcmp('xyz', 'abc') > 0")
+
+    ;; strcmp with aliased strings (same pointer)
+    (let r5 (funcall @strcmp hello1 hello1))
+    (assert! (equal? r5 (bv 32 0)) "strcmp(s, s) == 0")
+
+    ;; strcmp with empty strings
+    (let r6 (funcall @strcmp empty1 empty2))
+    (assert! (equal? r6 (bv 32 0)) "strcmp('', '') == 0")
+
+    ;; strcmp where first string is a prefix
+    (let r7 (funcall @strcmp ab abc))
+    (assert! (<$ r7 (bv 32 0)) "strcmp('ab', 'abc') < 0")
+
+    ;; strcmp where second string is a prefix
+    (let r8 (funcall @strcmp abc ab))
+    (assert! (<$ (bv 32 0) r8) "strcmp('abc', 'ab') > 0")
+
+    (return ())))

crucible-llvm-cli/test-data/strcmp.out.good

@@ -0,0 +1,4 @@
+==== Begin Simulation ====
+
+==== Finish Simulation ====
+==== No proof obligations ====

crucible-llvm/CHANGELOG.md

@@ -40,8 +40,10 @@
   * `Lang.Crucible.LLVM.MemModel.ppLLVMIntrinsicTypes`
   * `Lang.Crucible.LLVM.MemModel.ppLLVMMemIntrinsicType`
   * `Lang.Crucible.LLVM.MemModel.Pointer.ppLLVMPointerIntrinsicType`
-* Overrides for `strnlen`, `strcpy`, `strdup`, and `strndup` supported by new
+* Overrides for `strnlen`, `strcpy`, `strdup`, and `strndup`, supported by new
   APIs in `Lang.Crucible.LLVM.MemModel.Strings`.
+* Override for `memcmp`.
+* Override for `strcmp`.
 
 # 0.8.0 -- 2025-11-09
 

crucible-llvm/doc/dev.md

@@ -0,0 +1,28 @@
+# Crucible-LLVM developer documentation
+
+## Adding an override
+
+To add an override to Crucible-LLVM:
+
+- Carefully read the manpage (`man 3 FUN`). Pay special attention to mentions
+  of undefined behavior. If the manpage mentions the possibility undefined
+  behavior, the override must assert that it does not occur. For example,
+  the behavior of `strcpy` is undefined if the strings overlap, and the
+  corresponding override asserts that this does not occur.
+- Add the declaration and definition to `Intrinsics.Libc` or `Intrinsics.LLVM`.
+- Add the declaration to the appropriate list, e.g., `libc_overrides` if it
+  appears in libc or `basic_llvm_overrides` if it is an LLVM override (usually
+  starting with `@llvm.*`).
+- Add a test in `crucible-cli/test-data/simulate`. See `strdup.cbl` for an
+  example. If the override can exhibit undefined behavior, that should be
+  covered by the test.
+- Try running the test manually with: `cd crucible-cli && cabal run -- simulate
+  test-data/simulate/TEST.cbl`. Ensure that the output is what you expect.
+- Create the golden output file at `test-data/simulate/TEST.out` with `cd
+  crucible-cli && cabal run test:crucible-llvm-cli-tests --`. Double-check the
+  output.
+- If the override has any substantial limitations that make it less general than
+  actual C implementations (e.g., certain arguments must be concrete, it always
+  reports failure, etc.), note them in `doc/limitations.md`.
+- Note the addition of the override in `CHANGELOG.md`, e.g., "Add override for
+  `FUN`.".

crucible-llvm/doc/limitations.md

@@ -186,3 +186,8 @@ Crucible-LLVM is missing overrides for many of the functions from `string.h`,
 see issue [#1713] for an up-to-date list and status updates.
 
 [#1713]: https://github.com/GaloisInc/crucible/issues/1713
+
+Limitations of overrides
+========================
+
+- `memcmp` requires a concrete length.

crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs

@@ -99,6 +99,8 @@ libc_overrides =
   , SomeLLVMOverride llvmStrcpyOverride
   , SomeLLVMOverride llvmStrdupOverride
   , SomeLLVMOverride llvmStrndupOverride
+  , SomeLLVMOverride llvmMemcmpOverride
+  , SomeLLVMOverride llvmStrcmpOverride
   , SomeLLVMOverride llvmPrintfOverride
   , SomeLLVMOverride llvmPrintfChkOverride
   , SomeLLVMOverride llvmPutsOverride
@@ -428,6 +430,22 @@ llvmStrndupOverride =
   [llvmOvr| i8* @strndup( i8*, size_t ) |]
   (\memOps args -> Ctx.uncurryAssignment (callStrndup memOps) args)
 
+llvmMemcmpOverride
+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
+     , ?memOpts :: MemOptions )
+  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr ::> BVType wptr) (BVType 32)
+llvmMemcmpOverride =
+  [llvmOvr| i32 @memcmp( i8*, i8*, size_t ) |]
+  (\memOps args -> Ctx.uncurryAssignment (callMemcmp memOps) args)
+
+llvmStrcmpOverride
+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
+     , ?memOpts :: MemOptions )
+  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr) (BVType 32)
+llvmStrcmpOverride =
+  [llvmOvr| i32 @strcmp( i8*, i8* ) |]
+  (\memOps args -> Ctx.uncurryAssignment (callStrcmp memOps) args)
+
 ------------------------------------------------------------------------
 -- ** Implementations
 
@@ -710,6 +728,31 @@ callStrndup mvar (regValue -> src) (regValue -> bound) =
           let bound' = Just (fromIntegral b) in
           CStr.dupConcretelyNullTerminatedString bak mem src bound' loc' noAlignment
 
+callMemcmp
+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
+     , ?memOpts :: MemOptions )
+  => GlobalVar Mem
+  -> RegEntry sym (LLVMPointerType wptr)
+  -> RegEntry sym (LLVMPointerType wptr)
+  -> RegEntry sym (BVType wptr)
+  -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
+callMemcmp mvar (regValue -> ptr1) (regValue -> ptr2) (regValue -> len) =
+  ovrWithBackend $ \bak -> do
+    mem <- readGlobal mvar
+    liftIO $ CStr.memcmp bak mem ptr1 ptr2 len
+
+callStrcmp
+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
+     , ?memOpts :: MemOptions )
+  => GlobalVar Mem
+  -> RegEntry sym (LLVMPointerType wptr)
+  -> RegEntry sym (LLVMPointerType wptr)
+  -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
+callStrcmp mvar (regValue -> ptr1) (regValue -> ptr2) =
+  ovrWithBackend $ \bak -> do
+    mem <- readGlobal mvar
+    liftIO $ CStr.strcmp bak mem ptr1 ptr2
+
 callAssert
   :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
      , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions )