Properly extend path condition for llvm_conditional_points_to

This leverages the newly introduced `withConditionalPred` function (see the
parent commit) to make `llvm_conditional_points_to cond ptr val` properly
extend the path condition with `cond` before matching `val` against the value
that `ptr` points to.

Fixes #1945.

Author: RyanGlScott

intTests/test1945/Makefile

@@ -0,0 +1,11 @@
+CC = clang
+CFLAGS = -g -frecord-command-line -O0
+
+all: test.bc
+
+test.bc: test.c
+	$(CC) $(CFLAGS) -c -emit-llvm $< -o $@
+
+.PHONY: clean
+clean:
+	rm -f test.bc

intTests/test1945/test.bc

@@ -0,0 +1,3 @@
+#include <stdint.h>
+
+void test(uint8_t *x) {}

intTests/test1945/test.c

@@ -0,0 +1,17 @@
+// Test a use of `llvm_conditional_points_to` where the value that the pointer
+// points to will fail to match against the right-hand side value unless the
+// condition is properly incorporated into the path condition. This serves as
+// a regression test for https://github.com/GaloisInc/saw-script/issues/1945.
+
+let test_spec = do {
+  p <- llvm_alloc (llvm_int 8);
+  x <- llvm_fresh_var "x" (llvm_int 8);
+  llvm_points_to p (llvm_term x);
+
+  llvm_execute_func [p];
+
+  llvm_conditional_points_to {{ x == 1 }} p (llvm_term {{ 1 : [8] }});
+};
+
+m <- llvm_load_module "test.bc";
+llvm_verify m "test" [] false test_spec z3;

intTests/test1945/test.saw

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

intTests/test1945/test.sh

@@ -1410,14 +1410,28 @@ matchPointsToValue opts sc cc spec prepost md maybe_cond ptr val =
             let badLoadSummary = summarizeBadLoad cc memTy prepost ptr
             case res of
               Crucible.NoErr pred_ res_val -> do
-                pred_' <- case maybe_cond of
-                  Just cond -> do
-                    cond' <- instantiateExtResolveSAWPred sc cc (ttTerm cond)
-                    liftIO $ W4.impliesPred sym cond' pred_
-                  Nothing -> return pred_
+                -- If dealing with an `llvm_conditional_points_to` statement,
+                -- convert the condition to a `Pred`. If dealing with an
+                -- ordinary `llvm_points_to` statement, this condition will
+                -- simply be `True`.
+                cond' <- case maybe_cond of
+                  Just cond ->
+                    instantiateExtResolveSAWPred sc cc (ttTerm cond)
+                  Nothing ->
+                    pure $ W4.truePred sym
+                -- Next, construct an implication involving the condition and
+                -- assert it.
+                pred_' <- liftIO $ W4.impliesPred sym cond' pred_
                 addAssert pred_' md $ Crucible.SimError loc $
                   Crucible.AssertFailureSimError (show $ PP.vcat badLoadSummary) ""
-                pure Nothing <* matchArg opts sc cc spec prepost md res_val memTy val'
+
+                -- Finally, match the value that the pointer points to against
+                -- the right-hand side value in the points_to statement. Make
+                -- sure to execute this match with an extended path condition
+                -- that takes the condition above into account. See also
+                -- Note [oeConditionalPred] in SAWScript.Crucible.Common.Override.
+                withConditionalPred cond' $
+                  pure Nothing <* matchArg opts sc cc spec prepost md res_val memTy val'
               _ -> do
                 pure $ Just $ describeConcreteMemoryLoadFailure mem badLoadSummary ptr