diff --git a/saw-core/src/Verifier/SAW/Grammar.y b/saw-core/src/Verifier/SAW/Grammar.y index 9ecdf4fecf..a37fee8d01 100644 --- a/saw-core/src/Verifier/SAW/Grammar.y +++ b/saw-core/src/Verifier/SAW/Grammar.y @@ -80,6 +80,7 @@ import Verifier.SAW.Lexer 'injectCode' { PosPair _ (TKey "injectCode") } nat { PosPair _ (TNat _) } + bvlit { PosPair _ (TBitvector _) } '_' { PosPair _ (TIdent "_") } ident { PosPair _ (TIdent _) } identrec { PosPair _ (TRecursor _) } @@ -177,6 +178,7 @@ AppTerm : AtomTerm { $1 } AtomTerm :: { Term } AtomTerm : nat { NatLit (pos $1) (tokNat (val $1)) } + | bvlit { BVLit (pos $1) (tokBits (val $1)) } | string { StringLit (pos $1) (Text.pack (tokString (val $1))) } | Ident { Name $1 } | IdentRec { Recursor Nothing $1 } diff --git a/saw-core/src/Verifier/SAW/Lexer.x b/saw-core/src/Verifier/SAW/Lexer.x index 53bc175153..ffb2e9f77b 100644 --- a/saw-core/src/Verifier/SAW/Lexer.x +++ b/saw-core/src/Verifier/SAW/Lexer.x @@ -37,6 +37,8 @@ import Control.Monad.State.Strict import qualified Data.ByteString.Lazy as B import Data.ByteString.Lazy.UTF8 (toString) import Data.Word (Word8) +import Data.Bits +import Data.Char (digitToInt) import Numeric.Natural import Verifier.SAW.Position @@ -86,6 +88,8 @@ $white+; "-}" { \_ -> TCmntE } \" @string* \" { TString . read } @num { TNat . read } +"0x"@hex { TBitvector . readHexBV . drop 2 } +"0b"[0-1]+ { TBitvector . readBinBV . drop 2 } @key { TKey } @ident { TIdent } @ident "#rec" { TRecursor . dropRecSuffix } @@ -96,6 +100,7 @@ data Token = TIdent { tokIdent :: String } -- ^ Identifier | TRecursor { tokRecursor :: String } -- ^ Recursor | TNat { tokNat :: Natural } -- ^ Natural number literal + | TBitvector { tokBits :: [Bool] } -- ^ Bitvector literal | TString { tokString :: String } -- ^ String literal | TKey String -- ^ Keyword or predefined symbol | TEnd -- ^ End of file. @@ -108,12 +113,24 @@ data Token dropRecSuffix :: String -> String dropRecSuffix str = take (length str - 4) str +-- | Convert a hexadecimal string to a big endian list of bits +readHexBV :: String -> [Bool] +readHexBV = + concatMap (\c -> let i = digitToInt c in + [testBit i 3, testBit i 2, testBit i 1, testBit i 0]) + +-- | Convert a binary string to a big endian list of bits +readBinBV :: String -> [Bool] +readBinBV = map (\c -> c == '1') + ppToken :: Token -> String ppToken tkn = case tkn of TIdent s -> s TRecursor s -> s ++ "#rec" TNat n -> show n + TBitvector bits -> + "0b" ++ map (\b -> if b then '1' else '0') bits TString s -> show s TKey s -> s TEnd -> "END" diff --git a/saw-core/src/Verifier/SAW/Term/Pretty.hs b/saw-core/src/Verifier/SAW/Term/Pretty.hs index 981cfbe663..58cf0de96e 100644 --- a/saw-core/src/Verifier/SAW/Term/Pretty.hs +++ b/saw-core/src/Verifier/SAW/Term/Pretty.hs @@ -6,6 +6,7 @@ {-# LANGUAGE TupleSections #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE PatternGuards #-} {- | Module : Verifier.SAW.Term.Pretty @@ -40,6 +41,7 @@ module Verifier.SAW.Term.Pretty , ppName ) where +import Data.Char (intToDigit) import Data.Maybe (isJust) import Control.Monad.Reader import Control.Monad.State.Strict as State @@ -62,6 +64,7 @@ import qualified Data.IntMap.Strict as IntMap import Verifier.SAW.Name import Verifier.SAW.Term.Functor import Verifier.SAW.Utils (panic) +import Verifier.SAW.Recognizer -------------------------------------------------------------------------------- -- * Doc annotations @@ -469,11 +472,28 @@ ppFlatTermF prec tf = RecordProj e fld -> ppProj fld <$> ppTerm' PrecArg e Sort s h -> return ((if h then pretty ("i"::String) else mempty) <> viaShow s) NatLit i -> ppNat <$> (ppOpts <$> ask) <*> return (toInteger i) + ArrayValue (asBoolType -> Just _) args + | Just bits <- mapM asBool $ V.toList args -> + if length bits `mod` 4 == 0 then + return $ pretty ("0x" ++ ppBitsToHex bits) + else + return $ pretty ("0b" ++ map (\b -> if b then '1' else '0') bits) ArrayValue _ args -> ppArrayValue <$> mapM (ppTerm' PrecTerm) (V.toList args) StringLit s -> return $ viaShow s ExtCns cns -> annotate ExtCnsStyle <$> ppBestName (ecName cns) +-- | Pretty-print a big endian list of bit values as a hexadecimal number +ppBitsToHex :: [Bool] -> String +ppBitsToHex (b8:b4:b2:b1:bits') = + intToDigit (8 * toInt b8 + 4 * toInt b4 + 2 * toInt b2 + toInt b1) : + ppBitsToHex bits' + where toInt True = 1 + toInt False = 0 +ppBitsToHex [] = "" +ppBitsToHex bits = + panic "ppBitsToHex" ["length of bit list is not a multiple of 4", show bits] + -- | Pretty-print a name, using the best unambiguous alias from the -- naming environment. ppBestName :: NameInfo -> PPM SawDoc diff --git a/saw-core/src/Verifier/SAW/Typechecker.hs b/saw-core/src/Verifier/SAW/Typechecker.hs index cf5bc73700..c2ccb0903a 100644 --- a/saw-core/src/Verifier/SAW/Typechecker.hs +++ b/saw-core/src/Verifier/SAW/Typechecker.hs @@ -278,6 +278,11 @@ typeInferCompleteTerm (Un.VecLit _ ts) = type_of_tp <- typeInfer tp typeInferComplete (ArrayValue (TypedTerm tp type_of_tp) $ V.fromList typed_ts) +typeInferCompleteTerm (Un.BVLit _ []) = throwTCError EmptyVectorLit +typeInferCompleteTerm (Un.BVLit _ bits) = + do tp <- liftTCM scBoolType + bit_tms <- mapM (liftTCM scBool) bits + typeInferComplete $ ArrayValue tp $ V.fromList bit_tms typeInferCompleteTerm (Un.BadTerm _) = -- Should be unreachable, since BadTerms represent parse errors, that should diff --git a/saw-core/src/Verifier/SAW/UntypedAST.hs b/saw-core/src/Verifier/SAW/UntypedAST.hs index b09ee9a1ff..d889210fe2 100644 --- a/saw-core/src/Verifier/SAW/UntypedAST.hs +++ b/saw-core/src/Verifier/SAW/UntypedAST.hs @@ -84,6 +84,8 @@ data Term | StringLit Pos Text -- | Vector literal. | VecLit Pos [Term] + -- | Bitvector literal. + | BVLit Pos [Bool] | BadTerm Pos deriving (Show, TH.Lift) @@ -128,6 +130,7 @@ instance Positioned Term where NatLit p _ -> p StringLit p _ -> p VecLit p _ -> p + BVLit p _ -> p BadTerm p -> p instance Positioned TermVar where