Fix the semantics of strlen on symbolic strings.

Previously, `strlen` would recurse down a string until it
ran into a concrete zero.  This is fine, except that it would
assert that each load along the way would succeed, without taking
into account the previous zero tests that had to fail.  To correct
this we need to emulate a path condition such that to load
at position `n` each of the `n-1` previous locations must have
been non-zero, and the loads are only required to succeed under
that condition.  This allows one, for example, to assume that
some value in a string is 0 (but not specify which one).  Previously,
`strlen` would index off the end of the allocation of such a string
and fail.  Now it will succeed because the path condition required
to index out-of-bounds is inconsistent.

Fixes #468

crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs

@@ -215,6 +215,7 @@ import           Lang.Crucible.Simulator.SimError
 
 import           Lang.Crucible.LLVM.DataLayout
 import           Lang.Crucible.LLVM.Extension
+import           Lang.Crucible.LLVM.Extension.Safety
 import           Lang.Crucible.LLVM.Bytes
 import           Lang.Crucible.LLVM.MemType
 import           Lang.Crucible.LLVM.MemModel.Type
@@ -229,6 +230,7 @@ import           Lang.Crucible.LLVM.Types
 import           Lang.Crucible.Panic (panic)
 
 
+
 import           GHC.Stack
 
 ----------------------------------------------------------------------
@@ -971,22 +973,34 @@ isAllocatedAlignedPointer sym w alignment mutability ptr size mem =
 --
 --   The pointer to read from must be concrete and nonnull.  The contents
 --   of the string may be symbolic; HOWEVER, this function will not terminate
---   unless there it eventually reaches a concete null-terminator.
+--   until it eventually reaches a concete null-terminator or a load error.
 strLen :: forall sym wptr.
   (IsSymInterface sym, HasPtrWidth wptr, Partial.HasLLVMAnn sym) =>
   sym ->
   MemImpl sym      {- ^ memory to read from        -} ->
   LLVMPtr sym wptr {- ^ pointer to string value    -} ->
   IO (SymBV sym wptr)
-strLen sym mem = go 0
+strLen sym mem = go 0 (truePred sym)
   where
-  go !n p =
-    do v <- doLoad sym mem p (bitvectorType 1) (LLVMPointerRepr (knownNat @8)) noAlignment
-       test <- bvIsNonzero sym =<< projectLLVM_bv sym v
-       iteM bvIte sym
-            test
-            (go (n+1) =<< doPtrAddOffset sym mem p =<< bvLit sym PtrWidth 1)
-            (bvLit sym PtrWidth n)
+  go !n cond p =
+    loadRaw sym mem p (bitvectorType 1) noAlignment >>= \case
+      Partial.Err e ->
+        do ast <- impliesPred sym cond (falsePred sym)
+           let msg = show (ppMemoryLoadError e)
+           assert sym ast $ AssertFailureSimError "Error during memory load: strlen" msg
+           bvLit sym PtrWidth (maxUnsigned PtrWidth) -- bogus value, but have to return something...
+      Partial.NoErr loadok llvmval ->
+        do ast <- impliesPred sym cond loadok
+           assert sym ast $ AssertFailureSimError "Error during memory load: strlen" ""
+           v <- unpackMemValue sym (LLVMPointerRepr (knownNat @8)) llvmval
+           test <- bvIsNonzero sym =<< projectLLVM_bv sym v
+           iteM bvIte sym
+             test
+             (do cond' <- andPred sym cond test
+                 p'    <- doPtrAddOffset sym mem p =<< bvLit sym PtrWidth 1
+                 go (n+1) cond' p')
+             (bvLit sym PtrWidth n)
+
 
 -- | Load a null-terminated string from the memory.
 --

crux-llvm/test-data/golden/strlen_test.c

@@ -0,0 +1,23 @@
+#include <stdlib.h>
+#include <string.h>
+
+#include "crucible.h"
+
+#define MAX 10
+
+char* mkstr() {
+  char* x = malloc(MAX);
+  for( int i=0; i<MAX; i++ ) {
+    x[i] = crucible_int8_t( "x" );
+  }
+
+  assuming( x[MAX-1] == 0 );
+
+  return x;
+}
+
+int main() {
+  char *str = mkstr();
+  size_t sz = strlen(str);
+  check( sz < MAX );
+}

crux-llvm/test-data/golden/strlen_test.good

@@ -0,0 +1 @@
+[Crux] Overall status: Valid.