Merge remote-tracking branch 'origin/master' into heapster-memblock-p…

…rover-improvements

CHANGES.md

@@ -24,6 +24,9 @@ A new `enable_lax_pointer_ordering` function exists, which relaxes the
 restrictions that Crucible imposes on comparisons between pointers from
 different allocation blocks.
 
+A SAW value of type `Bool` can now be brought into scope in Cryptol expressions
+as a value of type `Bit`.
+
 ## Changes
 
 * The linked-in version of ABC (based on the Haskell `abcBridge`

heapster-saw/src/Verifier/SAW/Heapster/Implication.hs

@@ -4101,7 +4101,6 @@ implIntroOrShapeMultiM x bp (sh1 : shs) i =
 implIntroOrShapeMultiM _ _ _ _ = error "implIntroOrShapeMultiM"
 
 
-
 ----------------------------------------------------------------------
 -- * Support for Proving Lifetimes Are Current
 ----------------------------------------------------------------------

intTests/test1404/test.saw

@@ -0,0 +1,2 @@
+let b = true;
+print {{ b }};

intTests/test1404/test.sh

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

src/SAWScript/Value.hs

@@ -574,6 +574,9 @@ extendEnv sc x mt md v rw =
          VString s ->
            do tt <- typedTermOfString sc (unpack s)
               pure $ CEnv.bindTypedTerm (ident, tt) ce
+         VBool b ->
+           do tt <- typedTermOfBool sc b
+              pure $ CEnv.bindTypedTerm (ident, tt) ce
          _ ->
            pure ce
      pure $
@@ -590,7 +593,7 @@ extendEnv sc x mt md v rw =
 
 typedTermOfString :: SharedContext -> String -> IO TypedTerm
 typedTermOfString sc str =
-  do let schema = Cryptol.Forall [] [] (Cryptol.tString (length str))
+  do let schema = Cryptol.tMono (Cryptol.tString (length str))
      bvNat <- scGlobalDef sc "Prelude.bvNat"
      bvNat8 <- scApply sc bvNat =<< scNat sc 8
      byteT <- scBitvector sc 8
@@ -599,6 +602,12 @@ typedTermOfString sc str =
      trm <- scVector sc byteT ts
      pure (TypedTerm (TypedTermSchema schema) trm)
 
+typedTermOfBool :: SharedContext -> Bool -> IO TypedTerm
+typedTermOfBool sc b =
+  do let schema = Cryptol.tMono Cryptol.tBit
+     trm <- scBool sc b
+     pure (TypedTerm (TypedTermSchema schema) trm)
+
 
 -- Other SAWScript Monads ------------------------------------------------------