From b9c77840475d6201776fc5aa2376349ad76fdc27 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 16 Jun 2021 16:55:12 -0400 Subject: [PATCH] Propagate Cryptol error strings This patch adds two new SAWCore primitives: * `appendString : String -> String -> String`, which appends the underlying `Text` values in a `String`, and * `bytesToString : (n : Nat) -> Vec n (Vec 8 Bool) -> String`, which converts a Cryptol string (a sequence of 8-bit ASCII characters) to a SAWCore `String`. Moreover, this reimplements `ecError` in terms of `appendString`/`bytesToString` such that invoking the Cryptol `error` function from SAW will preserve the string passed to `error`. Previously, if you invoked the following in SAW: ``` sawscript> prove abc {{ error "Descriptive error message" : Bit }} ``` You would get: ``` Run-time error: encountered call to the Cryptol 'error' function ``` Now, you get: ``` Run-time error: encountered call to the Cryptol 'error' function: Descriptive error message ``` Fixes #1326. --- cryptol-saw-core/saw/Cryptol.sawcore | 11 ++--- cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 1 + saw-core/prelude/Prelude.sawcore | 6 ++- saw-core/src/Verifier/SAW/Simulator/Prims.hs | 50 ++++++++++++++++++++ saw-core/src/Verifier/SAW/Simulator/Value.hs | 4 ++ 5 files changed, 64 insertions(+), 8 deletions(-) diff --git a/cryptol-saw-core/saw/Cryptol.sawcore b/cryptol-saw-core/saw/Cryptol.sawcore index 6d081c5158..40f6f3b293 100644 --- a/cryptol-saw-core/saw/Cryptol.sawcore +++ b/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; diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index fbab2aeae8..3b165d1191 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/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 diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore index 82ddf83936..27e3717284 100644 --- a/saw-core/prelude/Prelude.sawcore +++ b/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 diff --git a/saw-core/src/Verifier/SAW/Simulator/Prims.hs b/saw-core/src/Verifier/SAW/Simulator/Prims.hs index b6c6441dc0..2a20191c22 100644 --- a/saw-core/src/Verifier/SAW/Simulator/Prims.hs +++ b/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) diff --git a/saw-core/src/Verifier/SAW/Simulator/Value.hs b/saw-core/src/Verifier/SAW/Simulator/Value.hs index afba5ea5fb..268fe158d7 100644 --- a/saw-core/src/Verifier/SAW/Simulator/Value.hs +++ b/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