Merge pull request #2149 from GaloisInc/T2148-match-LLVMValString

Match against `LLVMValString` in overrides (#2148)

CHANGES.md

@@ -7,6 +7,9 @@
 
 * Due to the regressions seen in issues #1946 and #1944, the experimental compositional hardware verification work has been reverted.
 
+* Fix a bug in which an LLVM override would fail to apply when matching an
+  argument against a string constant.
+
 # Version 1.2 -- 2024-08-30
 
 ## New Features

intTests/test2148/Makefile

@@ -0,0 +1,18 @@
+# The current checked-in test.bc was generated by:
+#    Ubuntu clang version 14.0.0-1ubuntu1.1
+#    Target: x86_64-pc-linux-gnu
+#    Thread model: posix
+#    InstalledDir: /usr/bin
+# but neither the target nor the clang/llvm version is expected to be
+# significant.
+CC = clang
+CFLAGS = -g -O0
+
+all: test.bc
+
+test.bc: test.c
+	$(CC) $(CFLAGS) -c -emit-llvm $< -o $@
+
+.PHONY: clean
+clean:
+	rm -f test.bc

intTests/test2148/test.c

@@ -0,0 +1,11 @@
+#include "stdint.h"
+#include "stdbool.h"
+
+void foo(uint8_t xs[4]);
+
+void bar() {
+    uint8_t xs[4] = {0,1,2,3};
+    for (int i = 0; i < 10; ++i) {
+        foo(xs);
+    }
+}

intTests/test2148/test.saw

@@ -0,0 +1,47 @@
+// A regression test that ensures that LLVM overrides will match successfully
+// when an argument is a string constant (#2148).
+
+let alloc_init ty v = do {
+    p <- llvm_alloc ty;
+    llvm_points_to p v;
+    return p;
+};
+
+let ptr_to_fresh n ty = do {
+    x <- llvm_fresh_var n ty;
+    p <- alloc_init ty (llvm_term x);
+    return (x, p);
+};
+
+let foo_spec1 = do {
+    (x, p_x) <- ptr_to_fresh "xs" (llvm_array 4 (llvm_int 8));
+
+    llvm_execute_func [p_x];
+
+    llvm_points_to p_x (llvm_term x);
+};
+
+// A slight variation of foo_spec1 that uses `llvm_fresh_expanded_val` instead
+// of `llvm_fresh_var`. This triggers a different code path in the LLVM override
+// matching logic.
+let foo_spec2 = do {
+    let ty = llvm_array 4 (llvm_int 8);
+    x <- llvm_fresh_expanded_val ty;
+    p_x <- alloc_init ty x;
+
+    llvm_execute_func [p_x];
+
+    llvm_points_to p_x x;
+};
+
+let bar_spec = do {
+    llvm_execute_func [];
+};
+
+m <- llvm_load_module "test.bc";
+
+foo_ov1 <- llvm_unsafe_assume_spec m "foo" foo_spec1;
+llvm_verify m "bar" [foo_ov1] true bar_spec z3;
+
+foo_ov2 <- llvm_unsafe_assume_spec m "foo" foo_spec2;
+llvm_verify m "bar" [foo_ov2] true bar_spec z3;

intTests/test2148/test.sh

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw

src/SAWScript/Crucible/LLVM/Override.hs

@@ -68,6 +68,7 @@ import           Control.Exception as X
 import           Control.Monad (filterM, foldM, forM, forM_, zipWithM)
 import           Control.Monad.Except (runExcept)
 import           Control.Monad.IO.Class (MonadIO(..))
+import qualified Data.ByteString as BS
 import           Data.Either (partitionEithers)
 import           Data.Foldable (for_, traverse_, toList)
 import           Data.List
@@ -1165,6 +1166,13 @@ matchArg opts sc cc cs prepost md actual expectedTy expected =
           [ matchArg opts sc cc cs prepost md x y z
           | (x, z) <- zip (V.toList xs) zs ]
 
+    -- LLVM string literals are syntactic shorthand for [<N> x i8] arrays,
+    -- so we defer to the LLVMValArray case above.
+    (Crucible.LLVMValString xs, Crucible.ArrayType _len (Crucible.IntType 8), SetupArray () zs)
+      | BS.length xs >= length zs ->
+        do explodedActual <- liftIO $ Crucible.explodeStringValue sym xs
+           matchArg opts sc cc cs prepost md explodedActual expectedTy expected
+
     -- match the fields of struct point-wise
     (Crucible.LLVMValStruct xs, Crucible.StructType fields, SetupStruct _ zs) ->
       sequence_
@@ -1306,6 +1314,13 @@ valueToSC sym md failMsg (Cryptol.TVSeq n cryty) (Crucible.LLVMValArray ty vals)
        t <- liftIO (typeToSC sc ty)
        liftIO (scVectorReduced sc t terms)
 
+-- LLVM string literals are syntactic shorthand for [<N> x i8] arrays, so we
+-- defer to the LLVMValArray case above.
+valueToSC sym md failMsg tval@(Cryptol.TVSeq n (Cryptol.TVSeq 8 Cryptol.TVBit)) (Crucible.LLVMValString str)
+  | toInteger (BS.length str) == n
+  = do explodedVal <- liftIO $ Crucible.explodeStringValue sym str
+       valueToSC sym md failMsg tval explodedVal
+
 valueToSC _ _ _ _ Crucible.LLVMValFloat{} =
   fail  "valueToSC: Real not supported"