Merge branch 'master' into macaw-264

Author: mergify[bot]

saw-core-what4/src/Verifier/SAW/Simulator/What4.hs

@@ -961,6 +961,8 @@ applyUnintApp sym app0 v =
     VCtorApp i ps xv          -> foldM (applyUnintApp sym) app' =<< traverse force (ps++xv)
                                    where app' = suffixUnintApp ("_" ++ (Text.unpack (identBaseName (primName i)))) app0
     VNat n                    -> return (suffixUnintApp ("_" ++ show n) app0)
+    VBVToNat w v'             -> applyUnintApp sym app' v'
+                                   where app' = suffixUnintApp ("_" ++ show w) app0
     TValue (suffixTValue -> Just s)
                               -> return (suffixUnintApp s app0)
     VFun _ _ ->
@@ -1399,6 +1401,7 @@ data ArgTerm
     -- ^ length, element type, list, index
   | ArgTermPairLeft ArgTerm
   | ArgTermPairRight ArgTerm
+  | ArgTermBVToNat Natural ArgTerm
 
 -- | Reassemble a saw-core term from an 'ArgTerm' and a list of parts.
 -- The length of the list should be equal to the number of
@@ -1468,6 +1471,10 @@ reconstructArgTerm atrm sc ts =
           do (x1, ts1) <- parse at1 ts0
              x <- scPairRight sc x1
              return (x, ts1)
+        ArgTermBVToNat w at1 ->
+          do (x1, ts1) <- parse at1 ts0
+             x <- scBvToNat sc w x1
+             pure (x, ts1)
 
     parseList :: [ArgTerm] -> [Term] -> IO ([Term], [Term])
     parseList [] ts0 = return ([], ts0)
@@ -1519,6 +1526,15 @@ mkArgTerm sc ty val =
       do x <- termOfTValue sc tval
          pure (ArgTermConst x)
 
+    (_, VNat n) ->
+      do x <- scNat sc n
+         pure (ArgTermConst x)
+
+    (_, VBVToNat w v) ->
+      do let w' = fromIntegral w -- FIXME: make w :: Natural to avoid fromIntegral
+         x <- mkArgTerm sc (VVecType w' VBoolType) v
+         pure (ArgTermBVToNat w' x)
+
     _ -> fail $ "could not create uninterpreted function argument of type " ++ show ty
 
 termOfTValue :: SharedContext -> TValue (What4 sym) -> IO Term

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 }

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"

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

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

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