WIP: Propagate Cryptol error strings

cryptol-saw-core/saw/Cryptol.sawcore

@@ -1406,17 +1406,14 @@ ecInfFromThen a pa x y =
 
 
 -- Run-time error
-ecError : (a : sort 0) -> (len : Num) -> seq len (Vec 8 Bool) -> a;
-ecError a len msg = error a "encountered call to the Cryptol 'error' function"; -- FIXME: don't throw away message
-{-
-primitive cryError : (a : sort 0) -> (n : Nat) -> Vec n (Vec 8 Bool) -> a;
-
 ecError : (a : sort 0) -> (len : Num) -> seq len (Vec 8 Bool) -> a;
 ecError a =
   finNumRec
     (\ (len:Num) -> seq len (Vec 8 Bool) -> a)
-    (\ (len:Nat) -> cryError a len);
--}
+    (\ (len:Nat) (msg:Vec len (Vec 8 Bool)) ->
+       error a (appendString "encountered call to the Cryptol 'error' function: "
+                             (bytesToString len msg))
+    );
 
 -- Random values
 ecRandom : (a : sort 0) -> Vec 32 Bool -> a;

cryptol-saw-core/src/Verifier/SAW/Cryptol.hs

@@ -1570,6 +1570,7 @@ asCryptolTypeValue v =
   case v of
     SC.VBoolType -> return (Right C.tBit)
     SC.VIntType -> return (Right C.tInteger)
+    SC.VStringType -> Nothing
     SC.VIntModType n -> return (Right (C.tIntMod (C.tNum n)))
     SC.VArrayType v1 v2 -> do
       Right t1 <- asCryptolTypeValue v1

saw-core/prelude/Prelude.sawcore

@@ -903,6 +903,7 @@ primitive expByNat : (a:sort 0) -> a -> (a -> a -> a) -> a -> Nat -> a;
 
 primitive equalString : String -> String -> Bool;
 
+primitive appendString : String -> String -> String;
 
 --------------------------------------------------------------------------------
 -- "Vec n a" is an array of n elements, each with type "a".
@@ -913,6 +914,9 @@ primitive gen : (n : Nat) -> (a : sort 0) -> (Nat -> a) -> Vec n a;
 
 primitive atWithDefault : (n : Nat) -> (a : sort 0) -> a -> Vec n a -> Nat -> a;
 
+-- Convert a Cryptol string (a sequence of 8-bit ASCII characters) to a SAWCore String.
+primitive bytesToString : (n : Nat) -> Vec n (Vec 8 Bool) -> String;
+
 at : (n : Nat) -> (a : sort 0) -> Vec n a -> Nat -> a;
 at n a v i = atWithDefault n a (error a "at: index out of bounds") v i;
 -- `at n a v i` has the precondition `ltNat i n`
@@ -1620,7 +1624,7 @@ genBVVec : (n : Nat) -> (len : Vec n Bool) -> (a : sort 0) ->
            BVVec n len a;
 genBVVec n len a f =
   genWithProof (bvToNat n len) a
-    (\(i:Nat) (pf:IsLtNat i (bvToNat n len)) -> 
+    (\(i:Nat) (pf:IsLtNat i (bvToNat n len)) ->
       f (bvNat n i) (IsLtNat_to_bvult n len i pf));
 
 -- Ex Falso Quodlibet: if True = False then anything is possible

saw-core/src/Verifier/SAW/Simulator/Prims.hs

@@ -30,9 +30,12 @@ import Control.Applicative
 import Control.Monad (liftM, unless)
 import Control.Monad.Fix (MonadFix(mfix))
 import Data.Bits
+import Data.Char (chr)
 import Data.Map (Map)
 import qualified Data.Map as Map
+import Data.Maybe (fromMaybe)
 import qualified Data.Text as Text
+import Data.Text (Text)
 import Data.Vector (Vector)
 import qualified Data.Vector as V
 import Numeric.Natural (Natural)
@@ -261,6 +264,10 @@ constMap bp = Map.fromList
   , ("Prelude.arrayLookup", arrayLookupOp bp)
   , ("Prelude.arrayUpdate", arrayUpdateOp bp)
   , ("Prelude.arrayEq", arrayEqOp bp)
+  -- Strings
+  , ("Prelude.String", TValue VStringType)
+  , ("Prelude.appendString", appendStringOp)
+  , ("Prelude.bytesToString", bytesToStringOp bp)
   ]
 
 -- | Call this function to indicate that a programming error has
@@ -303,6 +310,11 @@ intModFun msg f = strictFun g
   where g (VIntMod _ i) = f i
         g _ = panic $ "expected IntMod "++ msg
 
+stringFun :: VMonad l => String -> (Text -> MValue l) -> Value l
+stringFun msg f = strictFun g
+  where g (VString t) = f t
+        g _ = panic $ "expected String (" ++ msg ++ ")"
+
 toBool :: Show (Extra l) => Value l -> VBool l
 toBool (VBool b) = b
 toBool x = panic $ unwords ["Verifier.SAW.Simulator.toBool", show x]
@@ -1388,3 +1400,41 @@ arrayEqOp bp =
     x' <- toArray x
     y' <- toArray y
     VBool <$> bpArrayEq bp x' y'
+
+------------------------------------------------------------
+-- Strings
+
+-- appendString : String -> String -> String;
+appendStringOp :: VMonad l => Value l
+appendStringOp =
+  stringFun "appendStringOp" $ \x -> pure $
+  stringFun "appendStringOp" $ \y -> pure $
+  VString (x <> y)
+
+-- bytesToString : (n : Nat) -> Vec n (Vec 8 Bool) -> String;
+bytesToStringOp :: forall l. (VMonad l, Show (Extra l))
+                => BasePrims l -> Value l
+bytesToStringOp bp =
+  constFun $
+  vectorFun (bpUnpack bp) $ \v -> do
+    v' <- V.mapM byteToChar v
+    pure $ VString $ Text.pack $ V.toList v'
+  where
+    byteToChar :: Lazy (EvalM l) (Value l) -> EvalM l Char
+    byteToChar lv = do
+      v <- force lv
+      bits <- toBits (bpUnpack bp) v
+      pure $ chr $ bitsToInt $ V.map asBool bits
+
+    bitsToInt :: Vector Bool -> Int
+    bitsToInt = V.ifoldl' (\bits idx b ->
+                            -- Each character's bits are stored in big-endian
+                            -- order in the vector, so we must subtract the
+                            -- index of a bit from 7 (8 - 1) in order to set
+                            -- the bit at that index.
+                            if b then setBit bits (7 - idx) else bits)
+                          zeroBits
+
+    asBool :: VBool l -> Bool
+    asBool vb = fromMaybe (panic "bytesToStringOp: Nothing VBool")
+                          (bpAsBool bp vb)

saw-core/src/Verifier/SAW/Simulator/Value.hs

@@ -79,6 +79,7 @@ data TValue l
   = VVecType !Natural !(TValue l)
   | VBoolType
   | VIntType
+  | VStringType
   | VIntModType !Natural
   | VArrayType !(TValue l) !(TValue l)
   | VPiType LocalName !(TValue l) !(PiBody l)
@@ -214,6 +215,7 @@ instance Show (Extra l) => Show (TValue l) where
     case v of
       VBoolType      -> showString "Bool"
       VIntType       -> showString "Integer"
+      VStringType    -> showString "String"
       VIntModType n  -> showParen True (showString "IntMod " . shows n)
       VArrayType{}   -> showString "Array"
       VPiType _ t _    -> showParen True
@@ -343,6 +345,7 @@ asFirstOrderTypeTValue v =
     VSort{}     -> Nothing
     VRecursorType{} -> Nothing
     VTyTerm{}   -> Nothing
+    VStringType -> Nothing
 
 -- | A (partial) injective mapping from type values to strings. These
 -- are intended to be useful as suffixes for names of type instances
@@ -371,6 +374,7 @@ suffixTValue tv =
     VSort {} -> Nothing
     VRecursorType{} -> Nothing
     VTyTerm{} -> Nothing
+    VStringType -> Nothing
 
 
 neutralToTerm :: NeutralTerm -> Term