diff --git a/README.md b/README.md index 8d72ded885..acdbc63f0e 100644 --- a/README.md +++ b/README.md @@ -1,10 +1,22 @@ -This repository contains the code for SAWCore, an intermediate -language for representing the semantics of software (and potentially -hardware). It provides support for constructing models in a -dependently-typed lambda-calculus, transforming those models using a -rewriting engine, concretely or symbolically interpreting those -models, and emitting them as input to various external theorem -provers. - -Currently, the library supports generating AIG, CNF, and SMT-Lib -output. +SAWCore is a purely functional dependently-typed intermediate language +for representing the semantics of software (and potentially hardware). +It includes primitive types and operations sufficient to represent +values from a multitude of languages, such as C, LLVM, Java, and +Cryptol. + +This repository contains multiple Haskell packages: + + * **`saw-core`** defines the term language, the surface syntax with + parser and type checker, a term rewriting engine, and various + operations for constructing, analyzing, and evaluating terms. + + * **`saw-core-aig`** provides a backend for generating And-Inverter + Graphs (AIGs) from SAWCore terms. + + * **`saw-core-sbv`** provides a backend for translating SAWCore + terms into symbolic values in the Haskell SBV library, which can + be sent to external SMT solvers. + + * **`saw-core-what4`** provides a backend for translating SAWCore + terms into symbolic values in the Haskell What4 library, which + can be send to external SMT solvers. diff --git a/saw-core-aig/.gitignore b/saw-core-aig/.gitignore new file mode 100644 index 0000000000..8ee1bf9489 --- /dev/null +++ b/saw-core-aig/.gitignore @@ -0,0 +1 @@ +.stack-work diff --git a/LICENSE b/saw-core-aig/LICENSE similarity index 100% rename from LICENSE rename to saw-core-aig/LICENSE diff --git a/saw-core-aig/README.md b/saw-core-aig/README.md new file mode 100644 index 0000000000..a70f295730 --- /dev/null +++ b/saw-core-aig/README.md @@ -0,0 +1,2 @@ +This repository contains a backend for the `saw-core` library that uses +the `aig` library for construction of And-Inverter Graphs (AIGs). diff --git a/Setup.hs b/saw-core-aig/Setup.hs similarity index 100% rename from Setup.hs rename to saw-core-aig/Setup.hs diff --git a/saw-core-aig/saw-core-aig.cabal b/saw-core-aig/saw-core-aig.cabal new file mode 100644 index 0000000000..921bc1a5ff --- /dev/null +++ b/saw-core-aig/saw-core-aig.cabal @@ -0,0 +1,29 @@ +Name: saw-core-aig +Version: 0.1 +License: BSD3 +License-file: LICENSE +Author: Galois, Inc. +Maintainer: huffman@galois.com +Copyright: (c) 2012-2016 Galois Inc. +Category: Formal Methods +Build-type: Simple +cabal-version: >= 1.8 +Synopsis: SAWCore backend for AIGs +Description: + A backend for symbolically evaluating terms in the SAWCore + intermediate language using the aig library to generate And-Inverter + Graphs (AIGs). + +library + build-depends: + aig, + base == 4.*, + containers, + saw-core, + vector + hs-source-dirs: src + exposed-modules: + Verifier.SAW.Simulator.BitBlast + GHC-options: -Wall -Werror + if impl(ghc == 8.0.1) + ghc-options: -Wno-redundant-constraints diff --git a/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs b/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs new file mode 100644 index 0000000000..776cc76dc0 --- /dev/null +++ b/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs @@ -0,0 +1,522 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE TypeFamilies #-} + +{- | +Module : Verifier.SAW.Simulator.BitBlast +Copyright : Galois, Inc. 2012-2015 +License : BSD3 +Maintainer : jhendrix@galois.com +Stability : experimental +Portability : non-portable (language extensions) +-} + +module Verifier.SAW.Simulator.BitBlast + ( BValue + , withBitBlastedPred + , withBitBlastedTerm + ) where + +#if !MIN_VERSION_base(4,8,0) +import Control.Applicative +import Data.Traversable +#endif +import Control.Monad ((<=<)) +import Data.IORef +import Data.Map (Map) +import qualified Data.Map as Map +import qualified Data.Vector as V +import Numeric.Natural (Natural) + +import Verifier.SAW.FiniteValue (FiniteType(..)) +import qualified Verifier.SAW.Simulator as Sim +import Verifier.SAW.Simulator.Value +import qualified Verifier.SAW.Simulator.Prims as Prims +import Verifier.SAW.SharedTerm +import Verifier.SAW.TypedAST +import qualified Verifier.SAW.Simulator.Concrete as Concrete +import qualified Verifier.SAW.Prim as Prim +import qualified Verifier.SAW.Recognizer as R + +import qualified Data.AIG as AIG + +type LitVector l = AIG.BV l + +------------------------------------------------------------ +-- Vector operations + +lvFromV :: V.Vector l -> LitVector l +lvFromV v = AIG.generate_msb0 (V.length v) ((V.!) v) + +vFromLV :: LitVector l -> V.Vector l +vFromLV lv = V.generate (AIG.length lv) (AIG.at lv) + +lvRotateL :: LitVector l -> Integer -> LitVector l +lvRotateL xs i + | AIG.length xs == 0 = xs + | otherwise = (AIG.++) (AIG.drop j xs) (AIG.take j xs) + where j = fromInteger (i `mod` toInteger (AIG.length xs)) + +lvRotateR :: LitVector l -> Integer -> LitVector l +lvRotateR xs i = lvRotateL xs (- i) + +lvShiftL :: l -> LitVector l -> Integer -> LitVector l +lvShiftL x xs i = (AIG.++) (AIG.drop j xs) (AIG.replicate j x) + where j = fromInteger (min i (toInteger (AIG.length xs))) + +lvShl :: l -> LitVector l -> Natural -> LitVector l +lvShl l v i = AIG.slice v j (n-j) AIG.++ AIG.replicate j l + where n = AIG.length v + j = fromIntegral i `min` n + +lvShiftR :: l -> LitVector l -> Integer -> LitVector l +lvShiftR x xs i = (AIG.++) (AIG.replicate j x) (AIG.take (AIG.length xs - j) xs) + where j = fromInteger (min i (toInteger (AIG.length xs))) + +lvShr :: l -> LitVector l -> Natural -> LitVector l +lvShr l v i = AIG.replicate j l AIG.++ AIG.slice v 0 (n-j) + where n = AIG.length v + j = fromIntegral i `min` n + +------------------------------------------------------------ +-- Values + +data BitBlast l + +type instance EvalM (BitBlast l) = IO +type instance VBool (BitBlast l) = l +type instance VWord (BitBlast l) = LitVector l +type instance VInt (BitBlast l) = Integer +type instance Extra (BitBlast l) = BExtra l + +type BValue l = Value (BitBlast l) +type BThunk l = Thunk (BitBlast l) + +data BExtra l + = BStream (Integer -> IO (BValue l)) (IORef (Map Integer (BValue l))) + +instance Show (BExtra l) where + show (BStream _ _) = "BStream" + +vBool :: l -> BValue l +vBool l = VBool l + +toBool :: BValue l -> l +toBool (VBool l) = l +toBool x = error $ unwords ["Verifier.SAW.Simulator.BitBlast.toBool", show x] + +vWord :: LitVector l -> BValue l +vWord lv = VWord lv + +toWord :: BValue l -> IO (LitVector l) +toWord (VWord lv) = return lv +toWord (VVector vv) = lvFromV <$> traverse (fmap toBool . force) vv +toWord x = fail $ unwords ["Verifier.SAW.Simulator.BitBlast.toWord", show x] + +flattenBValue :: BValue l -> IO (LitVector l) +flattenBValue (VBool l) = return (AIG.replicate 1 l) +flattenBValue (VWord lv) = return lv +flattenBValue (VExtra (BStream _ _)) = error "Verifier.SAW.Simulator.BitBlast.flattenBValue: BStream" +flattenBValue (VVector vv) = + AIG.concat <$> traverse (flattenBValue <=< force) (V.toList vv) +flattenBValue VUnit = return $ AIG.concat [] +flattenBValue (VPair x y) = do + vx <- flattenBValue =<< force x + vy <- flattenBValue =<< force y + return $ AIG.concat [vx, vy] +flattenBValue (VRecordValue elems) = do + AIG.concat <$> mapM (flattenBValue <=< force . snd) elems +flattenBValue _ = error $ unwords ["Verifier.SAW.Simulator.BitBlast.flattenBValue: unsupported value"] + +wordFun :: (LitVector l -> IO (BValue l)) -> BValue l +wordFun f = strictFun (\x -> toWord x >>= f) + +------------------------------------------------------------ + +-- | op :: (n :: Nat) -> bitvector n -> Nat -> bitvector n +bvShiftOp :: (LitVector l -> LitVector l -> IO (LitVector l)) + -> (LitVector l -> Natural -> LitVector l) + -> BValue l +bvShiftOp bvOp natOp = + constFun $ + wordFun $ \x -> return $ + strictFun $ \y -> + case y of + VNat n -> return (vWord (natOp x (fromInteger n))) + VToNat v -> fmap vWord (bvOp x =<< toWord v) + _ -> error $ unwords ["Verifier.SAW.Simulator.BitBlast.shiftOp", show y] + +lvSShr :: LitVector l -> Natural -> LitVector l +lvSShr v i = lvShr (AIG.msb v) v i + +------------------------------------------------------------ + +pure1 :: Applicative f => (a -> b) -> a -> f b +pure1 f x = pure (f x) + +pure2 :: Applicative f => (a -> b -> c) -> a -> b -> f c +pure2 f x y = pure (f x y) + +pure3 :: Applicative f => (a -> b -> c -> d) -> a -> b -> c -> f d +pure3 f x y z = pure (f x y z) + +prims :: AIG.IsAIG l g => g s -> Prims.BasePrims (BitBlast (l s)) +prims be = + Prims.BasePrims + { Prims.bpAsBool = AIG.asConstant be + -- Bitvectors + , Prims.bpUnpack = pure1 vFromLV + , Prims.bpPack = pure1 lvFromV + , Prims.bpBvAt = pure2 AIG.at + , Prims.bpBvLit = pure2 (AIG.bvFromInteger be) + , Prims.bpBvSize = AIG.length + , Prims.bpBvJoin = pure2 (AIG.++) + , Prims.bpBvSlice = pure3 (\i n v -> AIG.slice v i n) + -- Conditionals + , Prims.bpMuxBool = \b x y -> AIG.lazyMux be b (pure x) (pure y) + , Prims.bpMuxWord = \b x y -> AIG.iteM be b (pure x) (pure y) + , Prims.bpMuxInt = muxInt + , Prims.bpMuxExtra = muxBExtra be + -- Booleans + , Prims.bpTrue = AIG.trueLit be + , Prims.bpFalse = AIG.falseLit be + , Prims.bpNot = pure1 AIG.not + , Prims.bpAnd = AIG.and be + , Prims.bpOr = AIG.or be + , Prims.bpXor = AIG.xor be + , Prims.bpBoolEq = AIG.eq be + -- Bitvector logical + , Prims.bpBvNot = pure1 (fmap AIG.not) + , Prims.bpBvAnd = AIG.zipWithM (AIG.and be) + , Prims.bpBvOr = AIG.zipWithM (AIG.or be) + , Prims.bpBvXor = AIG.zipWithM (AIG.xor be) + -- Bitvector arithmetic + , Prims.bpBvNeg = AIG.neg be + , Prims.bpBvAdd = AIG.add be + , Prims.bpBvSub = AIG.sub be + , Prims.bpBvMul = AIG.mul be + , Prims.bpBvUDiv = AIG.uquot be + , Prims.bpBvURem = AIG.urem be + , Prims.bpBvSDiv = AIG.squot be + , Prims.bpBvSRem = AIG.srem be + , Prims.bpBvLg2 = bitblastLogBase2 be + -- Bitvector comparisons + , Prims.bpBvEq = AIG.bvEq be + , Prims.bpBvsle = AIG.sle be + , Prims.bpBvslt = AIG.slt be + , Prims.bpBvule = AIG.ule be + , Prims.bpBvult = AIG.ult be + , Prims.bpBvsge = flip (AIG.sle be) + , Prims.bpBvsgt = flip (AIG.slt be) + , Prims.bpBvuge = flip (AIG.ule be) + , Prims.bpBvugt = flip (AIG.ult be) + -- Bitvector shift/rotate + , Prims.bpBvRolInt = pure2 lvRotateL + , Prims.bpBvRorInt = pure2 lvRotateR + , Prims.bpBvShlInt = pure3 lvShiftL + , Prims.bpBvShrInt = pure3 lvShiftR + , Prims.bpBvRol = genShift be lvRotateL + , Prims.bpBvRor = genShift be lvRotateR + , Prims.bpBvShl = genShift be . lvShiftL + , Prims.bpBvShr = genShift be . lvShiftR + -- Bitvector misc + , Prims.bpBvPopcount = AIG.popCount be + , Prims.bpBvCountLeadingZeros = AIG.countLeadingZeros be + , Prims.bpBvCountTrailingZeros = AIG.countTrailingZeros be + , Prims.bpBvForall = unsupportedAIGPrimitive "bvForall" + + -- Integer operations + , Prims.bpIntAdd = pure2 (+) + , Prims.bpIntSub = pure2 (-) + , Prims.bpIntMul = pure2 (*) + , Prims.bpIntDiv = pure2 div + , Prims.bpIntMod = pure2 mod + , Prims.bpIntNeg = pure1 negate + , Prims.bpIntAbs = pure1 abs + , Prims.bpIntEq = pure2 (\x y -> AIG.constant be (x == y)) + , Prims.bpIntLe = pure2 (\x y -> AIG.constant be (x <= y)) + , Prims.bpIntLt = pure2 (\x y -> AIG.constant be (x < y)) + , Prims.bpIntMin = pure2 min + , Prims.bpIntMax = pure2 max + + -- Array operations + , Prims.bpArrayConstant = unsupportedAIGPrimitive "bpArrayConstant" + , Prims.bpArrayLookup = unsupportedAIGPrimitive "bpArrayLookup" + , Prims.bpArrayUpdate = unsupportedAIGPrimitive "bpArrayUpdate" + , Prims.bpArrayEq = unsupportedAIGPrimitive "bpArrayEq" + } + +unsupportedAIGPrimitive :: String -> a +unsupportedAIGPrimitive = Prim.unsupportedPrimitive "AIG" + +beConstMap :: AIG.IsAIG l g => g s -> Map Ident (BValue (l s)) +beConstMap be = + Map.union (Prims.constMap (prims be)) $ + Map.fromList + -- Shifts + [ ("Prelude.bvShl" , bvShiftOp (AIG.shl be) (lvShl (AIG.falseLit be))) + , ("Prelude.bvShr" , bvShiftOp (AIG.ushr be) (lvShr (AIG.falseLit be))) + , ("Prelude.bvSShr", bvShiftOp (AIG.sshr be) lvSShr) + -- Integers + , ("Prelude.intToNat", Prims.intToNatOp) + , ("Prelude.natToInt", Prims.natToIntOp) + , ("Prelude.intToBv" , intToBvOp be) + , ("Prelude.bvToInt" , bvToIntOp be) + , ("Prelude.sbvToInt", sbvToIntOp be) + -- Integers mod n + , ("Prelude.IntMod" , constFun VIntType) + , ("Prelude.toIntMod" , toIntModOp) + , ("Prelude.fromIntMod", constFun (VFun force)) + , ("Prelude.intModEq" , intModEqOp be) + , ("Prelude.intModAdd" , intModBinOp (+)) + , ("Prelude.intModSub" , intModBinOp (-)) + , ("Prelude.intModMul" , intModBinOp (*)) + , ("Prelude.intModNeg" , intModUnOp negate) + -- Streams + , ("Prelude.MkStream", mkStreamOp) + , ("Prelude.streamGet", streamGetOp be) + -- Misc + , ("Prelude.expByNat", Prims.expByNatOp (prims be)) + ] + +-- | Lifts a strict mux operation to a lazy mux +lazyMux :: AIG.IsAIG l g => g s -> (l s -> a -> a -> IO a) -> l s -> IO a -> IO a -> IO a +lazyMux be muxFn c tm fm + | (AIG.===) c (AIG.trueLit be) = tm + | (AIG.===) c (AIG.falseLit be) = fm + | otherwise = do + t <- tm + f <- fm + muxFn c t f + +muxBVal :: AIG.IsAIG l g => g s -> l s -> BValue (l s) -> BValue (l s) -> IO (BValue (l s)) +muxBVal be = Prims.muxValue (prims be) + +muxInt :: a -> Integer -> Integer -> IO Integer +muxInt _ x y = if x == y then return x else fail $ "muxBVal: VInt " ++ show (x, y) + +muxBExtra :: AIG.IsAIG l g => g s -> l s -> BExtra (l s) -> BExtra (l s) -> IO (BExtra (l s)) +muxBExtra be c x y = + do let f i = do xi <- lookupBStream (VExtra x) i + yi <- lookupBStream (VExtra y) i + muxBVal be c xi yi + r <- newIORef Map.empty + return (BStream f r) + +-- | Barrel-shifter algorithm. Takes a list of bits in big-endian order. +genShift :: + AIG.IsAIG l g => g s -> (LitVector (l s) -> Integer -> LitVector (l s)) -> + LitVector (l s) -> LitVector (l s) -> IO (LitVector (l s)) +genShift be op x y = Prims.shifter (AIG.ite be) (pure2 op) x (AIG.bvToList y) + +-- | rounded-up log base 2, where we complete the function by setting: +-- lg2 0 = 0 +bitblastLogBase2 :: AIG.IsAIG l g => g s -> LitVector (l s) -> IO (LitVector (l s)) +bitblastLogBase2 g x = do + z <- AIG.isZero g x + AIG.iteM g z (return x) (AIG.logBase2_up g x) + +----------------------------------------- +-- Integer/bitvector conversions + +-- primitive bvToInt :: (n::Nat) -> bitvector n -> Integer; +bvToIntOp :: AIG.IsAIG l g => g s -> BValue (l s) +bvToIntOp g = constFun $ wordFun $ \v -> + case AIG.asUnsigned g v of + Just i -> return $ VInt i + Nothing -> fail "Cannot convert symbolic bitvector to integer" + +-- primitive sbvToInt :: (n::Nat) -> bitvector n -> Integer; +sbvToIntOp :: AIG.IsAIG l g => g s -> BValue (l s) +sbvToIntOp g = constFun $ wordFun $ \v -> + case AIG.asSigned g v of + Just i -> return $ VInt i + Nothing -> fail "Cannot convert symbolic bitvector to integer" + +-- primitive intToBv :: (n::Nat) -> Integer -> bitvector n; +intToBvOp :: AIG.IsAIG l g => g s -> BValue (l s) +intToBvOp g = + Prims.natFun' "intToBv n" $ \n -> return $ + Prims.intFun "intToBv x" $ \x -> + VWord <$> + if n >= 0 then return (AIG.bvFromInteger g (fromIntegral n) x) + else AIG.neg g (AIG.bvFromInteger g (fromIntegral n) (negate x)) + +------------------------------------------------------------ + +toIntModOp :: BValue l +toIntModOp = + Prims.natFun $ \n -> return $ + Prims.intFun "toIntModOp" $ \x -> return $ + VInt (x `mod` toInteger n) + +intModEqOp :: AIG.IsAIG l g => g s -> BValue (l s) +intModEqOp be = + constFun $ + Prims.intFun "intModEqOp" $ \x -> return $ + Prims.intFun "intModEqOp" $ \y -> return $ + VBool (AIG.constant be (x == y)) + +intModBinOp :: (Integer -> Integer -> Integer) -> BValue l +intModBinOp f = + Prims.natFun $ \n -> return $ + Prims.intFun "intModBinOp x" $ \x -> return $ + Prims.intFun "intModBinOp y" $ \y -> return $ + VInt (f x y `mod` toInteger n) + +intModUnOp :: (Integer -> Integer) -> BValue l +intModUnOp f = + Prims.natFun $ \n -> return $ + Prims.intFun "intModUnOp" $ \x -> return $ + VInt (f x `mod` toInteger n) + +---------------------------------------- + +-- MkStream :: (a :: sort 0) -> (Nat -> a) -> Stream a; +mkStreamOp :: BValue l +mkStreamOp = + constFun $ + strictFun $ \f -> do + r <- newIORef Map.empty + return $ VExtra (BStream (\n -> apply f (ready (VNat n))) r) + +-- streamGet :: (a :: sort 0) -> Stream a -> Nat -> a; +streamGetOp :: AIG.IsAIG l g => g s -> BValue (l s) +streamGetOp be = + constFun $ + strictFun $ \xs -> return $ + strictFun $ \case + VNat n -> lookupBStream xs (toInteger n) + VToNat w -> + do bs <- toWord w + AIG.muxInteger (lazyMux be (muxBVal be)) ((2 ^ AIG.length bs) - 1) bs (lookupBStream xs) + v -> fail (unlines ["Verifier.SAW.Simulator.BitBlast.streamGetOp", "Expected Nat value", show v]) + + +lookupBStream :: BValue l -> Integer -> IO (BValue l) +lookupBStream (VExtra (BStream f r)) n = do + m <- readIORef r + case Map.lookup n m of + Just v -> return v + Nothing -> do v <- f n + writeIORef r (Map.insert n v m) + return v +lookupBStream _ _ = fail "Verifier.SAW.Simulator.BitBlast.lookupBStream: expected Stream" + +------------------------------------------------------------ +-- Generating variables for arguments + +newVars :: AIG.IsAIG l g => g s -> FiniteType -> IO (BValue (l s)) +newVars be FTBit = vBool <$> AIG.newInput be +newVars be (FTVec n tp) = VVector <$> V.replicateM (fromIntegral n) (newVars' be tp) +newVars be (FTTuple ts) = vTuple <$> traverse (newVars' be) ts +newVars be (FTRec tm) = vRecord <$> traverse (newVars' be) tm + +newVars' :: AIG.IsAIG l g => g s -> FiniteType -> IO (BThunk (l s)) +newVars' be shape = ready <$> newVars be shape + +------------------------------------------------------------ +-- Bit-blasting primitives. +-- +-- NB: It doesn't make sense to bit blast more than one term using the +-- same bit engine, so the primitives 'withBitBlasted*' create their +-- own bit engine internally, instead of receiving it from the caller, +-- and pass it to the caller-provided continuation. + +type PrimMap l g = forall s. g s -> Map Ident (BValue (l s)) + +bitBlastBasic :: AIG.IsAIG l g + => g s + -> ModuleMap + -> PrimMap l g + -> Map VarIndex (BValue (l s)) + -> Term + -> IO (BValue (l s)) +bitBlastBasic be m addlPrims ecMap t = do + cfg <- Sim.evalGlobal m (Map.union (beConstMap be) (addlPrims be)) + (bitBlastExtCns ecMap) + (const Nothing) + Sim.evalSharedTerm cfg t + +bitBlastExtCns :: + Map VarIndex (BValue (l s)) -> ExtCns (BValue (l s)) -> + IO (BValue (l s)) +bitBlastExtCns ecMap (EC idx name _v) = + case Map.lookup idx ecMap of + Just var -> return var + Nothing -> fail $ + "Verifier.SAW.Simulator.BitBlast: can't translate variable " ++ + show name ++ "(index: " ++ show idx ++ ")" + +asAIGType :: SharedContext -> Term -> IO [(String, Term)] +asAIGType sc t = do + t' <- scWhnf sc t + case t' of + (R.asPi -> Just (n, t1, t2)) -> ((n, t1) :) <$> asAIGType sc t2 + (R.asBoolType -> Just ()) -> return [] + (R.asVecType -> Just _) -> return [] + (R.asTupleType -> Just _) -> return [] + (R.asRecordType -> Just _) -> return [] + _ -> fail $ "Verifier.SAW.Simulator.BitBlast.adAIGType: invalid AIG type: " + ++ scPrettyTerm defaultPPOpts t' + +bitBlastTerm :: + AIG.IsAIG l g => + g s -> + SharedContext -> + PrimMap l g -> + Term -> + IO (BValue (l s), [(String, FiniteType)]) +bitBlastTerm be sc addlPrims t = do + ty <- scTypeOf sc t + args <- asAIGType sc ty + let ecs = getAllExts t + argShapes <- traverse (asFiniteType sc) (map snd args) + ecShapes <- traverse (asFiniteType sc) (map ecType ecs) + argVars <- traverse (newVars' be) argShapes + ecVars <- traverse (newVars be) ecShapes + let ecMap = Map.fromList $ zip (map ecVarIndex ecs) ecVars + modmap <- scGetModuleMap sc + bval <- bitBlastBasic be modmap addlPrims ecMap t + bval' <- applyAll bval argVars + let names = map fst args ++ map ecName ecs + shapes = argShapes ++ ecShapes + return (bval', zip names shapes) + +-- | Bitblast a predicate and apply a function to the result. Supports +-- @ExtCns@ subterms. +withBitBlastedPred :: AIG.IsAIG l g => AIG.Proxy l g -> + SharedContext -> + PrimMap l g -> + Term -> + (forall s. g s -> l s -> [(String, FiniteType)] -> IO a) -> IO a +withBitBlastedPred proxy sc addlPrims t c = AIG.withNewGraph proxy $ \be -> do + (bval, args) <- bitBlastTerm be sc addlPrims t + case bval of + VBool l -> c be l args + _ -> fail "Verifier.SAW.Simulator.BitBlast.bitBlast: non-boolean result type." + +-- | Bitblast a term and apply a function to the result. Does not +-- support @ExtCns@ subterms. +withBitBlastedTerm :: AIG.IsAIG l g => AIG.Proxy l g -> + SharedContext -> + PrimMap l g -> + Term -> + (forall s. g s -> LitVector (l s) -> IO a) -> IO a +withBitBlastedTerm proxy sc addlPrims t c = AIG.withNewGraph proxy $ \be -> do + (bval, _) <- bitBlastTerm be sc addlPrims t + v <- flattenBValue bval + c be v + +asFiniteType :: SharedContext -> Term -> IO FiniteType +asFiniteType sc t = + scGetModuleMap sc >>= \modmap -> + case asFiniteTypeValue (Concrete.evalSharedTerm modmap Map.empty t) of + Just ft -> return ft + Nothing -> + fail $ "asFiniteType: unsupported type " ++ scPrettyTerm defaultPPOpts t diff --git a/saw-core-sbv/.gitignore b/saw-core-sbv/.gitignore new file mode 100644 index 0000000000..8ee1bf9489 --- /dev/null +++ b/saw-core-sbv/.gitignore @@ -0,0 +1 @@ +.stack-work diff --git a/saw-core-sbv/LICENSE b/saw-core-sbv/LICENSE new file mode 100644 index 0000000000..9e2f031c53 --- /dev/null +++ b/saw-core-sbv/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2012-2016, Galois, Inc. + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the names of the authors nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/saw-core-sbv/README.md b/saw-core-sbv/README.md new file mode 100644 index 0000000000..4f024ce9c0 --- /dev/null +++ b/saw-core-sbv/README.md @@ -0,0 +1,2 @@ +This repository contains a backend for the `saw-core` library that uses +the `sbv` library for communication with SMT solvers. diff --git a/saw-core-sbv/Setup.hs b/saw-core-sbv/Setup.hs new file mode 100644 index 0000000000..9a994af677 --- /dev/null +++ b/saw-core-sbv/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/saw-core-sbv/saw-core-sbv.cabal b/saw-core-sbv/saw-core-sbv.cabal new file mode 100644 index 0000000000..ebb43f8c78 --- /dev/null +++ b/saw-core-sbv/saw-core-sbv.cabal @@ -0,0 +1,30 @@ +Name: saw-core-sbv +Version: 0.1 +License: BSD3 +License-file: LICENSE +Author: Galois, Inc. +Maintainer: huffman@galois.com +Copyright: (c) 2012-2016 Galois Inc. +Category: Formal Methods +Build-type: Simple +cabal-version: >= 1.8 +Synopsis: SAWCore backend for SBV +Description: + A backend for symbolically evaluating terms in the SAWCore + intermediate language using the SBV library to generate SMT-Lib. + +library + build-depends: + base == 4.*, + containers, + lens, + mtl, + saw-core, + sbv >= 8.0, + transformers, + vector + hs-source-dirs: src + exposed-modules: + Verifier.SAW.Simulator.SBV + Verifier.SAW.Simulator.SBV.SWord + GHC-options: -Wall -Werror -Wcompat diff --git a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs new file mode 100644 index 0000000000..4e0eb16522 --- /dev/null +++ b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs @@ -0,0 +1,855 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE EmptyDataDecls #-} + +{- | +Module : Verifier.SAW.Simulator.SBV +Copyright : Galois, Inc. 2012-2015 +License : BSD3 +Maintainer : huffman@galois.com +Stability : experimental +Portability : non-portable (language extensions) +-} +module Verifier.SAW.Simulator.SBV + ( sbvSolve + , sbvSolveBasic + , SValue + , Labeler(..) + , sbvCodeGen_definition + , sbvCodeGen + , toWord + , toBool + , module Verifier.SAW.Simulator.SBV.SWord + ) where + +import Data.SBV.Dynamic + +import Verifier.SAW.Simulator.SBV.SWord + +import Control.Lens ((<&>)) +import qualified Control.Arrow as A + +import Data.Bits +import Data.IORef +import Data.Map (Map) +import qualified Data.Map as Map +import qualified Data.Set as Set +import Data.Vector (Vector) +import qualified Data.Vector as V + +import Data.Traversable as T +#if !MIN_VERSION_base(4,8,0) +import Control.Applicative +#endif +import Control.Monad.IO.Class +import Control.Monad.State as ST +import Numeric.Natural (Natural) + +import qualified Verifier.SAW.Prim as Prim +import qualified Verifier.SAW.Recognizer as R +import qualified Verifier.SAW.Simulator as Sim +import qualified Verifier.SAW.Simulator.Prims as Prims +import Verifier.SAW.SharedTerm +import Verifier.SAW.Simulator.Value +import Verifier.SAW.TypedAST (FieldName, ModuleMap, identName) +import Verifier.SAW.FiniteValue (FirstOrderType(..), asFirstOrderType) + +data SBV + +type instance EvalM SBV = IO +type instance VBool SBV = SBool +type instance VWord SBV = SWord +type instance VInt SBV = SInteger +type instance Extra SBV = SbvExtra + +type SValue = Value SBV +--type SThunk = Thunk SBV + +data SbvExtra = + SStream (Integer -> IO SValue) (IORef (Map Integer SValue)) + +instance Show SbvExtra where + show (SStream _ _) = "" + +pure1 :: Applicative f => (a -> b) -> a -> f b +pure1 f x = pure (f x) + +pure2 :: Applicative f => (a -> b -> c) -> a -> b -> f c +pure2 f x y = pure (f x y) + +pure3 :: Applicative f => (a -> b -> c -> d) -> a -> b -> c -> f d +pure3 f x y z = pure (f x y z) + +prims :: Prims.BasePrims SBV +prims = + Prims.BasePrims + { Prims.bpAsBool = svAsBool + , Prims.bpUnpack = svUnpack + , Prims.bpPack = pure1 symFromBits + , Prims.bpBvAt = pure2 svAt + , Prims.bpBvLit = pure2 literalSWord + , Prims.bpBvSize = intSizeOf + , Prims.bpBvJoin = pure2 svJoin + , Prims.bpBvSlice = pure3 svSlice + -- Conditionals + , Prims.bpMuxBool = pure3 svIte + , Prims.bpMuxWord = pure3 svIte + , Prims.bpMuxInt = pure3 svIte + , Prims.bpMuxExtra = muxSbvExtra + -- Booleans + , Prims.bpTrue = svTrue + , Prims.bpFalse = svFalse + , Prims.bpNot = pure1 svNot + , Prims.bpAnd = pure2 svAnd + , Prims.bpOr = pure2 svOr + , Prims.bpXor = pure2 svXOr + , Prims.bpBoolEq = pure2 svEqual + -- Bitvector logical + , Prims.bpBvNot = pure1 svNot + , Prims.bpBvAnd = pure2 svAnd + , Prims.bpBvOr = pure2 svOr + , Prims.bpBvXor = pure2 svXOr + -- Bitvector arithmetic + , Prims.bpBvNeg = pure1 svUNeg + , Prims.bpBvAdd = pure2 svPlus + , Prims.bpBvSub = pure2 svMinus + , Prims.bpBvMul = pure2 svTimes + , Prims.bpBvUDiv = pure2 svQuot + , Prims.bpBvURem = pure2 svRem + , Prims.bpBvSDiv = \x y -> pure (svUnsign (svQuot (svSign x) (svSign y))) + , Prims.bpBvSRem = \x y -> pure (svUnsign (svRem (svSign x) (svSign y))) + , Prims.bpBvLg2 = pure1 sLg2 + -- Bitvector comparisons + , Prims.bpBvEq = pure2 svEqual + , Prims.bpBvsle = \x y -> pure (svLessEq (svSign x) (svSign y)) + , Prims.bpBvslt = \x y -> pure (svLessThan (svSign x) (svSign y)) + , Prims.bpBvule = pure2 svLessEq + , Prims.bpBvult = pure2 svLessThan + , Prims.bpBvsge = \x y -> pure (svGreaterEq (svSign x) (svSign y)) + , Prims.bpBvsgt = \x y -> pure (svGreaterThan (svSign x) (svSign y)) + , Prims.bpBvuge = pure2 svGreaterEq + , Prims.bpBvugt = pure2 svGreaterThan + -- Bitvector shift/rotate + , Prims.bpBvRolInt = pure2 svRol' + , Prims.bpBvRorInt = pure2 svRor' + , Prims.bpBvShlInt = pure3 svShl' + , Prims.bpBvShrInt = pure3 svShr' + , Prims.bpBvRol = pure2 svRotateLeft + , Prims.bpBvRor = pure2 svRotateRight + , Prims.bpBvShl = pure3 svShiftL + , Prims.bpBvShr = pure3 svShiftR + -- Bitvector misc + , Prims.bpBvPopcount = pure1 svPopcount + , Prims.bpBvCountLeadingZeros = pure1 svCountLeadingZeros + , Prims.bpBvCountTrailingZeros = pure1 svCountTrailingZeros + , Prims.bpBvForall = unsupportedSBVPrimitive "bvForall" + -- Integer operations + , Prims.bpIntAdd = pure2 svPlus + , Prims.bpIntSub = pure2 svMinus + , Prims.bpIntMul = pure2 svTimes + , Prims.bpIntDiv = pure2 svQuot + , Prims.bpIntMod = pure2 svRem + , Prims.bpIntNeg = pure1 svUNeg + , Prims.bpIntAbs = pure1 svAbs + , Prims.bpIntEq = pure2 svEqual + , Prims.bpIntLe = pure2 svLessEq + , Prims.bpIntLt = pure2 svLessThan + , Prims.bpIntMin = unsupportedSBVPrimitive "bpIntMin" + , Prims.bpIntMax = unsupportedSBVPrimitive "bpIntMax" + -- Array operations + , Prims.bpArrayConstant = unsupportedSBVPrimitive "bpArrayConstant" + , Prims.bpArrayLookup = unsupportedSBVPrimitive "bpArrayLookup" + , Prims.bpArrayUpdate = unsupportedSBVPrimitive "bpArrayUpdate" + , Prims.bpArrayEq = unsupportedSBVPrimitive "bpArrayEq" + } + +unsupportedSBVPrimitive :: String -> a +unsupportedSBVPrimitive = Prim.unsupportedPrimitive "SBV" + +constMap :: Map Ident SValue +constMap = + Map.union (Prims.constMap prims) $ + Map.fromList + [ + -- Shifts + ("Prelude.bvShl" , bvShLOp) + , ("Prelude.bvShr" , bvShROp) + , ("Prelude.bvSShr", bvSShROp) + -- Integers + , ("Prelude.intToNat", intToNatOp) + , ("Prelude.natToInt", natToIntOp) + , ("Prelude.intToBv" , intToBvOp) + , ("Prelude.bvToInt" , bvToIntOp) + , ("Prelude.sbvToInt", sbvToIntOp) + -- Integers mod n + , ("Prelude.IntMod" , constFun VIntType) + , ("Prelude.toIntMod" , constFun (VFun force)) + , ("Prelude.fromIntMod", fromIntModOp) + , ("Prelude.intModEq" , intModEqOp) + , ("Prelude.intModAdd" , intModBinOp svPlus) + , ("Prelude.intModSub" , intModBinOp svMinus) + , ("Prelude.intModMul" , intModBinOp svTimes) + , ("Prelude.intModNeg" , intModUnOp svUNeg) + -- Streams + , ("Prelude.MkStream", mkStreamOp) + , ("Prelude.streamGet", streamGetOp) + -- Misc + , ("Prelude.expByNat", Prims.expByNatOp prims) + ] + +------------------------------------------------------------ +-- Coercion functions +-- + +bitVector :: Int -> Integer -> SWord +bitVector w i = literalSWord w i + +symFromBits :: Vector SBool -> SWord +symFromBits v = V.foldl svJoin (bitVector 0 0) (V.map svToWord1 v) + +toMaybeBool :: SValue -> Maybe SBool +toMaybeBool (VBool b) = Just b +toMaybeBool _ = Nothing + +toBool :: SValue -> SBool +toBool (VBool b) = b +toBool sv = error $ unwords ["toBool failed:", show sv] + +toWord :: SValue -> IO SWord +toWord (VWord w) = return w +toWord (VVector vv) = symFromBits <$> traverse (fmap toBool . force) vv +toWord x = fail $ unwords ["Verifier.SAW.Simulator.SBV.toWord", show x] + +toMaybeWord :: SValue -> IO (Maybe SWord) +toMaybeWord (VWord w) = return (Just w) +toMaybeWord (VVector vv) = ((symFromBits <$>) . T.sequence) <$> traverse (fmap toMaybeBool . force) vv +toMaybeWord _ = return Nothing + +-- | Flatten an SValue to a sequence of components, each of which is +-- either a symbolic word or a symbolic boolean. If the SValue +-- contains any values built from data constructors, then return them +-- encoded as a String. +flattenSValue :: SValue -> IO ([SVal], String) +flattenSValue v = do + mw <- toMaybeWord v + case mw of + Just w -> return ([w], "") + Nothing -> + case v of + VUnit -> return ([], "") + VPair x y -> do (xs, sx) <- flattenSValue =<< force x + (ys, sy) <- flattenSValue =<< force y + return (xs ++ ys, sx ++ sy) + VRecordValue elems -> do (xss, sxs) <- + unzip <$> + mapM (flattenSValue <=< force . snd) elems + return (concat xss, concat sxs) + VVector (V.toList -> ts) -> do (xss, ss) <- unzip <$> traverse (force >=> flattenSValue) ts + return (concat xss, concat ss) + VBool sb -> return ([sb], "") + VWord sw -> return (if intSizeOf sw > 0 then [sw] else [], "") + VCtorApp i (V.toList->ts) -> do (xss, ss) <- unzip <$> traverse (force >=> flattenSValue) ts + return (concat xss, "_" ++ identName i ++ concat ss) + VNat n -> return ([], "_" ++ show n) + _ -> fail $ "Could not create sbv argument for " ++ show v + +vWord :: SWord -> SValue +vWord lv = VWord lv + +vBool :: SBool -> SValue +vBool l = VBool l + +vInteger :: SInteger -> SValue +vInteger x = VInt x + +------------------------------------------------------------ +-- Function constructors + +wordFun :: (SWord -> IO SValue) -> SValue +wordFun f = strictFun (\x -> toWord x >>= f) + +------------------------------------------------------------ +-- Indexing operations + +-- | Lifts a strict mux operation to a lazy mux +lazyMux :: (SBool -> a -> a -> IO a) -> (SBool -> IO a -> IO a -> IO a) +lazyMux muxFn c tm fm = + case svAsBool c of + Just True -> tm + Just False -> fm + Nothing -> do + t <- tm + f <- fm + muxFn c t f + +-- selectV merger maxValue valueFn index returns valueFn v when index has value v +-- if index is greater than maxValue, it returns valueFn maxValue. Use the ite op from merger. +selectV :: (Ord a, Num a, Bits a) => (SBool -> b -> b -> b) -> a -> (a -> b) -> SWord -> b +selectV merger maxValue valueFn vx = + case svAsInteger vx of + Just i -> valueFn (fromIntegral i) + Nothing -> impl (intSizeOf vx) 0 + where + impl _ x | x > maxValue || x < 0 = valueFn maxValue + impl 0 y = valueFn y + impl i y = merger (svTestBit vx j) (impl j (y `setBit` j)) (impl j y) where j = i - 1 + +-- Big-endian version of svTestBit +svAt :: SWord -> Int -> SBool +svAt x i = svTestBit x (intSizeOf x - 1 - i) + +svUnpack :: SWord -> IO (Vector SBool) +svUnpack x = return (V.generate (intSizeOf x) (svAt x)) + +asWordList :: [SValue] -> Maybe [SWord] +asWordList = go id + where + go f [] = Just (f []) + go f (VWord x : xs) = go (f . (x:)) xs + go _ _ = Nothing + +svSlice :: Int -> Int -> SWord -> SWord +svSlice i j x = svExtract (w - i - 1) (w - i - j) x + where w = intSizeOf x + +---------------------------------------- +-- Shift operations + +-- | op :: (n :: Nat) -> bitvector n -> Nat -> bitvector n +bvShiftOp :: (SWord -> SWord -> SWord) -> (SWord -> Int -> SWord) -> SValue +bvShiftOp bvOp natOp = + constFun $ + wordFun $ \x -> return $ + strictFun $ \y -> + case y of + VNat i -> return (vWord (natOp x j)) + where j = fromInteger (i `min` toInteger (intSizeOf x)) + VToNat v -> fmap (vWord . bvOp x) (toWord v) + _ -> error $ unwords ["Verifier.SAW.Simulator.SBV.bvShiftOp", show y] + +-- bvShl :: (w :: Nat) -> bitvector w -> Nat -> bitvector w; +bvShLOp :: SValue +bvShLOp = bvShiftOp svShiftLeft svShl + +-- bvShR :: (w :: Nat) -> bitvector w -> Nat -> bitvector w; +bvShROp :: SValue +bvShROp = bvShiftOp svShiftRight svShr + +-- bvSShR :: (w :: Nat) -> bitvector w -> Nat -> bitvector w; +bvSShROp :: SValue +bvSShROp = bvShiftOp bvOp natOp + where + bvOp w x = svUnsign (svShiftRight (svSign w) x) + natOp w i = svUnsign (svShr (svSign w) i) + +----------------------------------------- +-- Integer/bitvector conversions + +-- primitive intToNat : Integer -> Nat; +-- intToNat x == max 0 x +intToNatOp :: SValue +intToNatOp = + Prims.intFun "intToNat" $ \i -> + case svAsInteger i of + Just i' + | 0 <= i' -> pure (VNat i') + | otherwise -> pure (VNat 0) + Nothing -> + let z = svInteger KUnbounded 0 + i' = svIte (svLessThan i z) z i + in pure (VToNat (VInt i')) + +-- primitive natToInt :: Nat -> Integer; +natToIntOp :: SValue +natToIntOp = + Prims.natFun' "natToInt" $ \n -> return $ + VInt (literalSInteger (toInteger n)) + +-- primitive bvToInt :: (n::Nat) -> bitvector n -> Integer; +bvToIntOp :: SValue +bvToIntOp = constFun $ wordFun $ \v -> + case svAsInteger v of + Just i -> return $ VInt (literalSInteger i) + Nothing -> return $ VInt (svFromIntegral KUnbounded v) + +-- primitive sbvToInt :: (n::Nat) -> bitvector n -> Integer; +sbvToIntOp :: SValue +sbvToIntOp = constFun $ wordFun $ \v -> + case svAsInteger (svSign v) of + Just i -> return $ VInt (literalSInteger i) + Nothing -> return $ VInt (svFromIntegral KUnbounded (svSign v)) + +-- primitive intToBv :: (n::Nat) -> Integer -> bitvector n; +intToBvOp :: SValue +intToBvOp = + Prims.natFun' "intToBv n" $ \n -> return $ + Prims.intFun "intToBv x" $ \x -> + case svAsInteger x of + Just i -> return $ VWord $ literalSWord (fromIntegral n) i + Nothing -> return $ VWord $ svFromIntegral (KBounded False (fromIntegral n)) x + +------------------------------------------------------------ +-- Rotations and shifts + +svRol' :: SWord -> Integer -> SWord +svRol' x i = svRol x (fromInteger (i `mod` toInteger (intSizeOf x))) + +svRor' :: SWord -> Integer -> SWord +svRor' x i = svRor x (fromInteger (i `mod` toInteger (intSizeOf x))) + +svShl' :: SBool -> SWord -> Integer -> SWord +svShl' b x i = svIte b (svNot (svShl (svNot x) j)) (svShl x j) + where j = fromInteger (i `min` toInteger (intSizeOf x)) + +svShr' :: SBool -> SWord -> Integer -> SWord +svShr' b x i = svIte b (svNot (svShr (svNot x) j)) (svShr x j) + where j = fromInteger (i `min` toInteger (intSizeOf x)) + +svShiftL :: SBool -> SWord -> SWord -> SWord +svShiftL b x i = svIte b (svNot (svShiftLeft (svNot x) i)) (svShiftLeft x i) + +svShiftR :: SBool -> SWord -> SWord -> SWord +svShiftR b x i = svIte b (svNot (svShiftRight (svNot x) i)) (svShiftRight x i) + +------------------------------------------------------------ +-- Integers mod n + +fromIntModOp :: SValue +fromIntModOp = + Prims.natFun $ \n -> return $ + Prims.intFun "fromIntModOp" $ \x -> return $ + VInt (svRem x (literalSInteger (toInteger n))) + +intModEqOp :: SValue +intModEqOp = + Prims.natFun $ \n -> return $ + Prims.intFun "intModEqOp" $ \x -> return $ + Prims.intFun "intModEqOp" $ \y -> return $ + let modulus = literalSInteger (toInteger n) + in VBool (svEqual (svRem (svMinus x y) modulus) (literalSInteger 0)) + +intModBinOp :: (SInteger -> SInteger -> SInteger) -> SValue +intModBinOp f = + Prims.natFun $ \n -> return $ + Prims.intFun "intModBinOp x" $ \x -> return $ + Prims.intFun "intModBinOp y" $ \y -> return $ + VInt (normalizeIntMod n (f x y)) + +intModUnOp :: (SInteger -> SInteger) -> SValue +intModUnOp f = + Prims.natFun $ \n -> return $ + Prims.intFun "intModUnOp" $ \x -> return $ + VInt (normalizeIntMod n (f x)) + +normalizeIntMod :: Natural -> SInteger -> SInteger +normalizeIntMod n x = + case svAsInteger x of + Nothing -> x + Just i -> literalSInteger (i `mod` toInteger n) + +------------------------------------------------------------ +-- Stream operations + +-- MkStream :: (a :: sort 0) -> (Nat -> a) -> Stream a; +mkStreamOp :: SValue +mkStreamOp = + constFun $ + strictFun $ \f -> do + r <- newIORef Map.empty + return $ VExtra (SStream (\n -> apply f (ready (VNat n))) r) + +-- streamGet :: (a :: sort 0) -> Stream a -> Nat -> a; +streamGetOp :: SValue +streamGetOp = + constFun $ + strictFun $ \xs -> return $ + strictFun $ \case + VNat n -> lookupSStream xs (toInteger n) + VToNat w -> + do ilv <- toWord w + selectV (lazyMux muxBVal) ((2 ^ intSizeOf ilv) - 1) (lookupSStream xs) ilv + v -> Prims.panic "SBV.streamGetOp" ["Expected Nat value", show v] + + +lookupSStream :: SValue -> Integer -> IO SValue +lookupSStream (VExtra s) n = lookupSbvExtra s n +lookupSStream _ _ = fail "expected Stream" + +lookupSbvExtra :: SbvExtra -> Integer -> IO SValue +lookupSbvExtra (SStream f r) n = + do m <- readIORef r + case Map.lookup n m of + Just v -> return v + Nothing -> do v <- f n + writeIORef r (Map.insert n v m) + return v + +------------------------------------------------------------ +-- Misc operations + +svPopcount :: SWord -> SWord +svPopcount xs = if w == 0 then zero else foldr1 svPlus [ svIte b one zero | b <- bits ] + where + bits = svBlastLE xs + w = length bits + one = literalSWord w 1 + zero = literalSWord w 0 + +svCountLeadingZeros :: SWord -> SWord +svCountLeadingZeros xs = go 0 bits + where + bits = svBlastBE xs + w = length bits + go !i [] = literalSWord w i + go !i (b:bs) = svIte b (literalSWord w i) (go (i+1) bs) + +svCountTrailingZeros :: SWord -> SWord +svCountTrailingZeros xs = go 0 bits + where + bits = svBlastLE xs + w = length bits + go !i [] = literalSWord w i + go !i (b:bs) = svIte b (literalSWord w i) (go (i+1) bs) + +-- | Ceiling (log_2 x) +sLg2 :: SWord -> SWord +sLg2 x = go 0 + where + lit n = literalSWord (intSizeOf x) n + go i | i < intSizeOf x = svIte (svLessEq x (lit (2^i))) (lit (toInteger i)) (go (i + 1)) + | otherwise = lit (toInteger i) + +------------------------------------------------------------ +-- Ite ops + +muxBVal :: SBool -> SValue -> SValue -> IO SValue +muxBVal = Prims.muxValue prims + +muxSbvExtra :: SBool -> SbvExtra -> SbvExtra -> IO SbvExtra +muxSbvExtra c x y = + do let f i = do xi <- lookupSbvExtra x i + yi <- lookupSbvExtra y i + muxBVal c xi yi + r <- newIORef Map.empty + return (SStream f r) + +------------------------------------------------------------ +-- External interface + +-- | Abstract constants with names in the list 'unints' are kept as +-- uninterpreted constants; all others are unfolded. +sbvSolveBasic :: ModuleMap -> Map Ident SValue -> [String] -> Term -> IO SValue +sbvSolveBasic m addlPrims unints t = do + let unintSet = Set.fromList unints + let extcns (EC ix nm ty) = parseUninterpreted [] (nm ++ "#" ++ show ix) ty + let uninterpreted ec + | Set.member (ecName ec) unintSet = Just (extcns ec) + | otherwise = Nothing + cfg <- Sim.evalGlobal m (Map.union constMap addlPrims) extcns uninterpreted + Sim.evalSharedTerm cfg t + +parseUninterpreted :: [SVal] -> String -> SValue -> IO SValue +parseUninterpreted cws nm ty = + case ty of + (VPiType _ f) + -> return $ + strictFun $ \x -> do + (cws', suffix) <- flattenSValue x + t2 <- f (ready x) + parseUninterpreted (cws ++ cws') (nm ++ suffix) t2 + + VBoolType + -> return $ vBool $ mkUninterpreted KBool cws nm + + VIntType + -> return $ vInteger $ mkUninterpreted KUnbounded cws nm + + (VVecType (VNat n) VBoolType) + -> return $ vWord $ mkUninterpreted (KBounded False (fromIntegral n)) cws nm + + (VVecType (VNat n) ety) + -> do xs <- sequence $ + [ parseUninterpreted cws (nm ++ "@" ++ show i) ety + | i <- [0 .. n-1] ] + return (VVector (V.fromList (map ready xs))) + + VUnitType + -> return VUnit + + (VPairType ty1 ty2) + -> do x1 <- parseUninterpreted cws (nm ++ ".L") ty1 + x2 <- parseUninterpreted cws (nm ++ ".R") ty2 + return (VPair (ready x1) (ready x2)) + + (VRecordType elem_tps) + -> (VRecordValue <$> + mapM (\(f,tp) -> + (f,) <$> ready <$> + parseUninterpreted cws (nm ++ "." ++ f) tp) elem_tps) + + _ -> fail $ "could not create uninterpreted type for " ++ show ty + +mkUninterpreted :: Kind -> [SVal] -> String -> SVal +mkUninterpreted k args nm = svUninterpreted k nm' Nothing args + where nm' = "|" ++ nm ++ "|" -- enclose name to allow primes and other non-alphanum chars + +asPredType :: SValue -> IO [SValue] +asPredType v = + case v of + VBoolType -> return [] + VPiType v1 f -> + do v2 <- f (error "asPredType: unsupported dependent SAW-Core type") + vs <- asPredType v2 + return (v1 : vs) + _ -> fail $ "non-boolean result type: " ++ show v + +vAsFirstOrderType :: SValue -> Maybe FirstOrderType +vAsFirstOrderType v = + case v of + VBoolType + -> return FOTBit + VIntType + -> return FOTInt + VVecType (VNat n) v2 + -> FOTVec (fromInteger n) <$> vAsFirstOrderType v2 + VUnitType + -> return (FOTTuple []) + VPairType v1 v2 + -> do t1 <- vAsFirstOrderType v1 + t2 <- vAsFirstOrderType v2 + case t2 of + FOTTuple ts -> return (FOTTuple (t1 : ts)) + _ -> return (FOTTuple [t1, t2]) + + VRecordType tps + -> (FOTRec <$> Map.fromList <$> + mapM (\(f,tp) -> (f,) <$> vAsFirstOrderType tp) tps) + _ -> Nothing + +sbvSolve :: SharedContext + -> Map Ident SValue + -> [String] + -> Term + -> IO ([Maybe Labeler], Symbolic SBool) +sbvSolve sc addlPrims unints t = do + modmap <- scGetModuleMap sc + let eval = sbvSolveBasic modmap addlPrims unints + ty <- eval =<< scTypeOf sc t + let lamNames = map fst (fst (R.asLambdaList t)) + let varNames = [ "var" ++ show (i :: Integer) | i <- [0 ..] ] + let argNames = zipWith (++) varNames (map ("_" ++) lamNames ++ repeat "") + argTs <- asPredType ty + (labels, vars) <- + flip evalStateT 0 $ unzip <$> + sequence (zipWith newVarsForType argTs argNames) + bval <- eval t + let prd = do + bval' <- traverse (fmap ready) vars >>= (liftIO . applyAll bval) + case bval' of + VBool b -> return b + _ -> fail $ "sbvSolve: non-boolean result type. " ++ show bval' + return (labels, prd) + +data Labeler + = BoolLabel String + | IntegerLabel String + | WordLabel String + | VecLabel (Vector Labeler) + | TupleLabel (Vector Labeler) + | RecLabel (Map FieldName Labeler) + deriving (Show) + +nextId :: StateT Int IO String +nextId = ST.get >>= (\s-> modify (+1) >> return ("x" ++ show s)) + +--unzipMap :: Map k (a, b) -> (Map k a, Map k b) +--unzipMap m = (fmap fst m, fmap snd m) + +myfun ::(Map String (Labeler, Symbolic SValue)) -> (Map String Labeler, Map String (Symbolic SValue)) +myfun = fmap fst A.&&& fmap snd + +newVarsForType :: SValue -> String -> StateT Int IO (Maybe Labeler, Symbolic SValue) +newVarsForType v nm = + case vAsFirstOrderType v of + Just fot -> + do (l, sv) <- newVars fot + return (Just l, sv) + Nothing -> + do sv <- lift $ parseUninterpreted [] nm v + return (Nothing, return sv) + +newVars :: FirstOrderType -> StateT Int IO (Labeler, Symbolic SValue) +newVars FOTBit = nextId <&> \s-> (BoolLabel s, vBool <$> existsSBool s) +newVars FOTInt = nextId <&> \s-> (IntegerLabel s, vInteger <$> existsSInteger s) +newVars (FOTVec n FOTBit) = + if n == 0 + then nextId <&> \s-> (WordLabel s, return (vWord (literalSWord 0 0))) + else nextId <&> \s-> (WordLabel s, vWord <$> existsSWord s (fromIntegral n)) +newVars (FOTVec n tp) = do + (labels, vals) <- V.unzip <$> V.replicateM (fromIntegral n) (newVars tp) + return (VecLabel labels, VVector <$> traverse (fmap ready) vals) +newVars (FOTArray{}) = fail "FOTArray unimplemented for backend" +newVars (FOTTuple ts) = do + (labels, vals) <- V.unzip <$> traverse newVars (V.fromList ts) + return (TupleLabel labels, vTuple <$> traverse (fmap ready) (V.toList vals)) +newVars (FOTRec tm) = do + (labels, vals) <- myfun <$> (traverse newVars tm :: StateT Int IO (Map String (Labeler, Symbolic SValue))) + return (RecLabel labels, vRecord <$> traverse (fmap ready) (vals :: (Map String (Symbolic SValue)))) + +------------------------------------------------------------ +-- Code Generation + +newCodeGenVars :: (Natural -> Bool) -> FirstOrderType -> StateT Int IO (SBVCodeGen SValue) +newCodeGenVars _checkSz FOTBit = nextId <&> \s -> (vBool <$> svCgInput KBool s) +newCodeGenVars _checkSz FOTInt = nextId <&> \s -> (vInteger <$> svCgInput KUnbounded s) +newCodeGenVars checkSz (FOTVec n FOTBit) + | n == 0 = nextId <&> \_ -> return (vWord (literalSWord 0 0)) + | checkSz n = nextId <&> \s -> vWord <$> cgInputSWord s (fromIntegral n) + | otherwise = nextId <&> \s -> fail $ "Invalid codegen bit width for input variable \'" ++ s ++ "\': " ++ show n +newCodeGenVars checkSz (FOTVec n (FOTVec m FOTBit)) + | m == 0 = nextId <&> \_ -> return (VVector $ V.fromList $ replicate (fromIntegral n) (ready $ vWord (literalSWord 0 0))) + | checkSz m = do + let k = KBounded False (fromIntegral m) + vals <- nextId <&> \s -> svCgInputArr k (fromIntegral n) s + return (VVector . V.fromList . fmap (ready . vWord) <$> vals) + | otherwise = nextId <&> \s -> fail $ "Invalid codegen bit width for input variable array \'" ++ s ++ "\': " ++ show n +newCodeGenVars checkSz (FOTVec n tp) = do + vals <- V.replicateM (fromIntegral n) (newCodeGenVars checkSz tp) + return (VVector <$> traverse (fmap ready) vals) +newCodeGenVars _ (FOTArray{}) = fail "FOTArray unimplemented for backend" +newCodeGenVars checkSz (FOTTuple ts) = do + vals <- traverse (newCodeGenVars checkSz) ts + return (vTuple <$> traverse (fmap ready) vals) +newCodeGenVars checkSz (FOTRec tm) = do + vals <- traverse (newCodeGenVars checkSz) tm + return (vRecord <$> traverse (fmap ready) vals) + +cgInputSWord :: String -> Int -> SBVCodeGen SWord +cgInputSWord s n = svCgInput (KBounded False n) s + +argTypes :: SharedContext -> Term -> IO ([Term], Term) +argTypes sc t = do + t' <- scWhnf sc t + case t' of + (R.asPi -> Just (_, t1, t2)) -> do + (ts,res) <- argTypes sc t2 + return (t1:ts, res) + _ -> return ([], t') + +sbvCodeGen_definition + :: SharedContext + -> Map Ident SValue + -> [String] + -> Term + -> (Natural -> Bool) -- ^ Allowed word sizes + -> IO (SBVCodeGen (), [FirstOrderType], FirstOrderType) +sbvCodeGen_definition sc addlPrims unints t checkSz = do + ty <- scTypeOf sc t + (argTs,resTy) <- argTypes sc ty + shapes <- traverse (asFirstOrderType sc) argTs + resultShape <- asFirstOrderType sc resTy + modmap <- scGetModuleMap sc + bval <- sbvSolveBasic modmap addlPrims unints t + vars <- evalStateT (traverse (newCodeGenVars checkSz) shapes) 0 + let codegen = do + args <- traverse (fmap ready) vars + bval' <- liftIO (applyAll bval args) + sbvSetResult checkSz resultShape bval' + return (codegen, shapes, resultShape) + + +sbvSetResult :: (Natural -> Bool) + -> FirstOrderType + -> SValue + -> SBVCodeGen () +sbvSetResult _checkSz FOTBit (VBool b) = do + svCgReturn b +sbvSetResult checkSz (FOTVec n FOTBit) v + | n == 0 = return () + | checkSz n = do + w <- liftIO $ toWord v + svCgReturn w + | otherwise = + fail $ "Invalid word size in result: " ++ show n +sbvSetResult checkSz ft v = do + void $ sbvSetOutput checkSz ft v 0 + + +sbvSetOutput :: (Natural -> Bool) + -> FirstOrderType + -> SValue + -> Int + -> SBVCodeGen Int +sbvSetOutput _checkSz FOTBit (VBool b) i = do + svCgOutput ("out_"++show i) b + return $! i+1 +sbvSetOutput checkSz (FOTVec n FOTBit) v i + | n == 0 = return i + | checkSz n = do + w <- liftIO $ toWord v + svCgOutput ("out_"++show i) w + return $! i+1 + | otherwise = + fail $ "Invalid word size in output " ++ show i ++ ": " ++ show n + +sbvSetOutput checkSz (FOTVec n t) (VVector xv) i = do + xs <- liftIO $ traverse force $ V.toList xv + unless (toInteger n == toInteger (length xs)) $ + fail "sbvCodeGen: vector length mismatch when setting output values" + case asWordList xs of + Just ws -> do svCgOutputArr ("out_"++show i) ws + return $! i+1 + Nothing -> foldM (\i' x -> sbvSetOutput checkSz t x i') i xs +sbvSetOutput _checkSz (FOTTuple []) VUnit i = + return i +sbvSetOutput checkSz (FOTTuple [t]) v i = sbvSetOutput checkSz t v i +sbvSetOutput checkSz (FOTTuple (t:ts)) (VPair l r) i = do + l' <- liftIO $ force l + r' <- liftIO $ force r + sbvSetOutput checkSz t l' i >>= sbvSetOutput checkSz (FOTTuple ts) r' + +sbvSetOutput _checkSz (FOTRec fs) VUnit i | Map.null fs = do + return i + +sbvSetOutput _checkSz (FOTRec fs) (VRecordValue []) i | Map.null fs = return i + +sbvSetOutput checkSz (FOTRec fs) (VRecordValue ((fn,x):rest)) i = do + x' <- liftIO $ force x + case Map.lookup fn fs of + Just t -> do + let fs' = Map.delete fn fs + sbvSetOutput checkSz t x' i >>= + sbvSetOutput checkSz (FOTRec fs') (VRecordValue rest) + Nothing -> fail "sbvCodeGen: type mismatch when setting record output value" + +sbvSetOutput _checkSz _ft _v _i = do + fail "sbvCode gen: type mismatch when setting output values" + + +sbvCodeGen :: SharedContext + -> Map Ident SValue + -> [String] + -> Maybe FilePath + -> String + -> Term + -> IO () +sbvCodeGen sc addlPrims unints path fname t = do + -- The SBV C code generator expects only these word sizes + let checkSz n = n `elem` [8,16,32,64] + + (codegen,_,_) <- sbvCodeGen_definition sc addlPrims unints t checkSz + compileToC path fname codegen diff --git a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV/SWord.hs b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV/SWord.hs new file mode 100644 index 0000000000..ff76d32bcb --- /dev/null +++ b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV/SWord.hs @@ -0,0 +1,76 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE MultiParamTypeClasses #-} + +{- | +Module : Verifier.SAW.Simulator.SBV.SWord +Copyright : Galois, Inc. 2012-2015 +License : BSD3 +Maintainer : huffman@galois.com +Stability : experimental +Portability : non-portable (language extensions) +-} +module Verifier.SAW.Simulator.SBV.SWord + ( SBool, SWord, SInteger + , literalSWord, literalSInteger + , fromBitsLE + , forallSWord, existsSWord, forallSWord_, existsSWord_ + , forallSBool, existsSBool, forallSBool_, existsSBool_ + , forallSInteger, existsSInteger, forallSInteger_, existsSInteger_ + ) where + +import Control.Monad.Reader +import Data.List (foldl') + +import Data.SBV ( symbolicEnv ) +import Data.SBV.Dynamic + +type SBool = SVal +type SWord = SVal +type SInteger = SVal + +fromBitsLE :: [SBool] -> SWord +fromBitsLE bs = foldl' f (literalSWord 0 0) bs + where f w b = svJoin (svToWord1 b) w + +literalSWord :: Int -> Integer -> SWord +literalSWord w i = svInteger (KBounded False w) i + +literalSInteger :: Integer -> SWord +literalSInteger i = svInteger KUnbounded i + +forallSWord :: String -> Int -> Symbolic SWord +forallSWord nm w = symbolicEnv >>= liftIO . svMkSymVar (Just ALL) (KBounded False w) (Just nm) + +forallSWord_ :: Int -> Symbolic SWord +forallSWord_ w = symbolicEnv >>= liftIO . svMkSymVar (Just ALL) (KBounded False w) Nothing + +existsSWord :: String -> Int -> Symbolic SWord +existsSWord nm w = symbolicEnv >>= liftIO . svMkSymVar (Just EX) (KBounded False w) (Just nm) + +existsSWord_ :: Int -> Symbolic SWord +existsSWord_ w = symbolicEnv >>= liftIO . svMkSymVar (Just EX) (KBounded False w) Nothing + +forallSBool :: String -> Symbolic SBool +forallSBool nm = symbolicEnv >>= liftIO . svMkSymVar (Just ALL) KBool (Just nm) + +existsSBool :: String -> Symbolic SBool +existsSBool nm = symbolicEnv >>= liftIO . svMkSymVar (Just EX) KBool (Just nm) + +forallSBool_ :: Symbolic SBool +forallSBool_ = symbolicEnv >>= liftIO . svMkSymVar (Just ALL) KBool Nothing + +existsSBool_ :: Symbolic SBool +existsSBool_ = symbolicEnv >>= liftIO . svMkSymVar (Just EX) KBool Nothing + +forallSInteger :: String -> Symbolic SInteger +forallSInteger nm = symbolicEnv >>= liftIO . svMkSymVar (Just ALL) KUnbounded (Just nm) + +existsSInteger :: String -> Symbolic SInteger +existsSInteger nm = symbolicEnv >>= liftIO . svMkSymVar (Just EX) KUnbounded (Just nm) + +forallSInteger_ :: Symbolic SInteger +forallSInteger_ = symbolicEnv >>= liftIO . svMkSymVar (Just ALL) KUnbounded Nothing + +existsSInteger_ :: Symbolic SInteger +existsSInteger_ = symbolicEnv >>= liftIO . svMkSymVar (Just EX) KUnbounded Nothing diff --git a/saw-core-what4/.gitignore b/saw-core-what4/.gitignore new file mode 100644 index 0000000000..8f0f594227 --- /dev/null +++ b/saw-core-what4/.gitignore @@ -0,0 +1,3 @@ +.stack-work/ +dist/ +dist-newstyle/ diff --git a/saw-core-what4/Changelog.md b/saw-core-what4/Changelog.md new file mode 100644 index 0000000000..020ecadf40 --- /dev/null +++ b/saw-core-what4/Changelog.md @@ -0,0 +1,9 @@ +# Changelog for the `saw-core-what4` package + +## 0.2 -- *2019 Nov 06* + + * Bumped upper version bound for parameterized-utils + +## 0.1 -- *2018 Jun 06* + + * Initial version diff --git a/saw-core-what4/LICENSE b/saw-core-what4/LICENSE new file mode 100644 index 0000000000..9e2f031c53 --- /dev/null +++ b/saw-core-what4/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2012-2016, Galois, Inc. + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the names of the authors nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/saw-core-what4/README.md b/saw-core-what4/README.md new file mode 100644 index 0000000000..5f49d96494 --- /dev/null +++ b/saw-core-what4/README.md @@ -0,0 +1,2 @@ +This repository contains a backend for the `saw-core` library that uses +the `what4` library for communication with SMT solvers. diff --git a/saw-core-what4/Setup.hs b/saw-core-what4/Setup.hs new file mode 100644 index 0000000000..9a994af677 --- /dev/null +++ b/saw-core-what4/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/saw-core-what4/saw-core-what4.cabal b/saw-core-what4/saw-core-what4.cabal new file mode 100644 index 0000000000..6588181b0a --- /dev/null +++ b/saw-core-what4/saw-core-what4.cabal @@ -0,0 +1,39 @@ +Name: saw-core-what4 +Version: 0.2 +License: BSD3 +License-file: LICENSE +Author: Galois, Inc. +Maintainer: sweirich@galois.com +Copyright: (c) 2018 Galois Inc. +Category: Formal Methods +Build-type: Simple +cabal-version: >= 1.8 +Synopsis: SAWCore backend for What4 +Description: + A backend for symbolically evaluating terms in the SAWCore + intermediate language using the What4 library to generate SMT-Lib. + +library + build-depends: + ansi-wl-pprint, + base == 4.*, + bv-sized >= 1.0.0, + containers, + lens, + mtl, + saw-core, + what4, + crucible-saw, + panic, + transformers, + vector, + parameterized-utils >= 1.0.8 && < 2.2, + reflection + hs-source-dirs: src + exposed-modules: + Verifier.SAW.Simulator.What4 + Verifier.SAW.Simulator.What4.SWord + Verifier.SAW.Simulator.What4.FirstOrder + Verifier.SAW.Simulator.What4.PosNat + Verifier.SAW.Simulator.What4.Panic + GHC-options: -Wall -Werror diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs new file mode 100644 index 0000000000..eb25ff97c7 --- /dev/null +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs @@ -0,0 +1,1238 @@ +------------------------------------------------------------------------ +-- | +-- Module : Verifier.SAW.Simulator.What4 +-- Copyright : Galois, Inc. 2012-2015 +-- License : BSD3 +-- Maintainer : sweirich@galois.com +-- Stability : experimental +-- Portability : non-portable (language extensions) +-- +-- A symbolic simulator for saw-core terms using What4. +-- (This module is derived from Verifier.SAW.Simulator.SBV) +------------------------------------------------------------------------ + +{-# LANGUAGE CPP #-} +{-# LANGUAGE ConstraintKinds#-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE TypeApplications #-} + +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE AllowAmbiguousTypes #-} + +-- WithKnownNat +{-# OPTIONS_GHC -Wno-warnings-deprecations #-} + + +module Verifier.SAW.Simulator.What4 + ( w4Solve + , w4SolveAny + , w4SolveBasic + , SymFnCache + , TypedExpr(..) + , SValue + , Labeler(..) + , w4Eval + , w4EvalAny + , w4EvalBasic + ) where + + + +import qualified Control.Arrow as A + +import Data.Bits +import Data.IORef +import Data.Map (Map) +import qualified Data.Map as Map +import qualified Data.Set as Set +import Data.Vector (Vector) +import qualified Data.Vector as V + +import Data.Traversable as T +#if !MIN_VERSION_base(4,8,0) +import Control.Applicative +#endif +import Control.Monad.State as ST +import Numeric.Natural (Natural) + +import Data.Reflection (Given(..), give) + +-- saw-core +import qualified Verifier.SAW.Recognizer as R +import qualified Verifier.SAW.Simulator as Sim +import qualified Verifier.SAW.Simulator.Prims as Prims +import Verifier.SAW.SharedTerm +import Verifier.SAW.Simulator.Value +import Verifier.SAW.TypedAST (FieldName, ModuleMap, identName) +import Verifier.SAW.FiniteValue (FirstOrderType(..)) + +-- what4 +import What4.Interface(SymExpr,Pred,SymInteger, IsExpr, + IsExprBuilder,IsSymExprBuilder) +import qualified What4.Interface as W +import What4.BaseTypes + +-- parameterized-utils +import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.Map (MapF) +import qualified Data.Parameterized.Map as MapF +import Data.Parameterized.Context (Assignment) +import Data.Parameterized.Some + +-- crucible-saw +import qualified Lang.Crucible.Backend.SAWCore as CS + +-- saw-core-what4 +import Verifier.SAW.Simulator.What4.SWord +import Verifier.SAW.Simulator.What4.PosNat +import Verifier.SAW.Simulator.What4.FirstOrder +import Verifier.SAW.Simulator.What4.Panic + +--------------------------------------------------------------------- +-- empty datatype to index (open) type families +-- for this backend +data What4 (sym :: *) + +-- | A What4 symbolic array where the domain and co-domain types do not appear +-- in the type +data SArray sym where + SArray :: + W.IsExpr (W.SymExpr sym) => + W.SymArray sym (Ctx.EmptyCtx Ctx.::> itp) etp -> + SArray sym + +-- type abbreviations for uniform naming +type SBool sym = Pred sym +type SInt sym = SymInteger sym + +type instance EvalM (What4 sym) = IO +type instance VBool (What4 sym) = SBool sym +type instance VWord (What4 sym) = SWord sym +type instance VInt (What4 sym) = SInt sym +type instance VArray (What4 sym) = SArray sym +type instance Extra (What4 sym) = What4Extra sym + +type SValue sym = Value (What4 sym) + +-- Constraint +type Sym sym = (Given sym, IsSymExprBuilder sym) + +--------------------------------------------------------------------- + +data What4Extra sym = + SStream (Integer -> IO (SValue sym)) (IORef (Map Integer (SValue sym))) + +instance Show (What4Extra sym) where + show (SStream _ _) = "" + +--------------------------------------------------------------------- +-- +-- Basic primitive table for What4 data +-- + +prims :: forall sym. (Sym sym) => + Prims.BasePrims (What4 sym) +prims = + let sym :: sym = given in + Prims.BasePrims + { Prims.bpAsBool = W.asConstantPred + -- Bitvectors + , Prims.bpUnpack = bvUnpack sym + , Prims.bpPack = bvPack sym + , Prims.bpBvAt = bvAt sym + , Prims.bpBvLit = bvLit sym + , Prims.bpBvSize = intSizeOf + , Prims.bpBvJoin = bvJoin sym + , Prims.bpBvSlice = bvSlice sym + -- Conditionals + , Prims.bpMuxBool = W.itePred sym + , Prims.bpMuxWord = bvIte sym + , Prims.bpMuxInt = W.intIte sym + , Prims.bpMuxExtra = muxWhat4Extra + -- Booleans + , Prims.bpTrue = W.truePred sym + , Prims.bpFalse = W.falsePred sym + , Prims.bpNot = W.notPred sym + , Prims.bpAnd = W.andPred sym + , Prims.bpOr = W.orPred sym + , Prims.bpXor = W.xorPred sym + , Prims.bpBoolEq = W.isEq sym + -- Bitvector logical + , Prims.bpBvNot = bvNot sym + , Prims.bpBvAnd = bvAnd sym + , Prims.bpBvOr = bvOr sym + , Prims.bpBvXor = bvXor sym + -- Bitvector arithmetic + , Prims.bpBvNeg = bvNeg sym + , Prims.bpBvAdd = bvAdd sym + , Prims.bpBvSub = bvSub sym + , Prims.bpBvMul = bvMul sym + , Prims.bpBvUDiv = bvUDiv sym + , Prims.bpBvURem = bvURem sym + , Prims.bpBvSDiv = bvSDiv sym + , Prims.bpBvSRem = bvSRem sym + , Prims.bpBvLg2 = bvLg2 sym + -- Bitvector comparisons + , Prims.bpBvEq = bvEq sym + , Prims.bpBvsle = bvsle sym + , Prims.bpBvslt = bvslt sym + , Prims.bpBvule = bvule sym + , Prims.bpBvult = bvult sym + , Prims.bpBvsge = bvsge sym + , Prims.bpBvsgt = bvsgt sym + , Prims.bpBvuge = bvuge sym + , Prims.bpBvugt = bvugt sym + -- Bitvector shift/rotate + , Prims.bpBvRolInt = bvRolInt sym + , Prims.bpBvRorInt = bvRorInt sym + , Prims.bpBvShlInt = bvShlInt sym + , Prims.bpBvShrInt = bvShrInt sym + , Prims.bpBvRol = bvRol sym + , Prims.bpBvRor = bvRor sym + , Prims.bpBvShl = bvShl sym + , Prims.bpBvShr = bvShr sym + -- Bitvector misc + , Prims.bpBvPopcount = bvPopcount sym + , Prims.bpBvCountLeadingZeros = bvCountLeadingZeros sym + , Prims.bpBvCountTrailingZeros = bvCountTrailingZeros sym + , Prims.bpBvForall = bvForall sym + -- Integer operations + , Prims.bpIntAbs = W.intAbs sym + , Prims.bpIntAdd = W.intAdd sym + , Prims.bpIntSub = W.intSub sym + , Prims.bpIntMul = W.intMul sym + , Prims.bpIntDiv = W.intDiv sym + , Prims.bpIntMod = W.intMod sym + , Prims.bpIntNeg = W.intNeg sym + , Prims.bpIntEq = W.intEq sym + , Prims.bpIntLe = W.intLe sym + , Prims.bpIntLt = W.intLt sym + , Prims.bpIntMin = intMin sym + , Prims.bpIntMax = intMax sym + -- Array operations + , Prims.bpArrayConstant = arrayConstant sym + , Prims.bpArrayLookup = arrayLookup sym + , Prims.bpArrayUpdate = arrayUpdate sym + , Prims.bpArrayEq = arrayEq sym + } + + +constMap :: forall sym. (Sym sym) => Map Ident (SValue sym) +constMap = + Map.union (Prims.constMap prims) $ + Map.fromList + [ + -- Shifts + ("Prelude.bvShl" , bvShLOp) + , ("Prelude.bvShr" , bvShROp) + , ("Prelude.bvSShr", bvSShROp) + -- Integers + , ("Prelude.intToNat", intToNatOp) + , ("Prelude.natToInt", natToIntOp) + , ("Prelude.intToBv" , intToBvOp) + , ("Prelude.bvToInt" , bvToIntOp) + , ("Prelude.sbvToInt", sbvToIntOp) + -- Integers mod n + , ("Prelude.IntMod" , constFun VIntType) + , ("Prelude.toIntMod" , constFun (VFun force)) + , ("Prelude.fromIntMod", fromIntModOp sym) + , ("Prelude.intModEq" , intModEqOp sym) + , ("Prelude.intModAdd" , intModBinOp sym W.intAdd) + , ("Prelude.intModSub" , intModBinOp sym W.intSub) + , ("Prelude.intModMul" , intModBinOp sym W.intMul) + , ("Prelude.intModNeg" , intModUnOp sym W.intNeg) + -- Streams + , ("Prelude.MkStream", mkStreamOp) + , ("Prelude.streamGet", streamGetOp) + -- Misc + , ("Prelude.expByNat", Prims.expByNatOp prims) + ] + where sym = given :: sym + +----------------------------------------------------------------------- +-- Implementation of constMap primitives + +toBool :: SValue sym -> IO (SBool sym) +toBool (VBool b) = return b +toBool x = fail $ unwords ["Verifier.SAW.Simulator.What4.toBool", show x] + +toWord :: forall sym. (Sym sym) => + SValue sym -> IO (SWord sym) +toWord (VWord w) = return w +toWord (VVector vv) = do + -- vec :: Vector (SBool sym)) + vec1 <- T.traverse force vv + vec2 <- T.traverse toBool vec1 + bvPack (given :: sym) vec2 +toWord x = fail $ unwords ["Verifier.SAW.Simulator.What4.toWord", show x] + +wordFun :: (Sym sym) => + (SWord sym -> IO (SValue sym)) -> SValue sym +wordFun f = strictFun (\x -> f =<< toWord x) + +valueToSymExpr :: SValue sym -> Maybe (Some (W.SymExpr sym)) +valueToSymExpr = \case + VBool b -> Just $ Some b + VInt i -> Just $ Some i + VWord (DBV w) -> Just $ Some w + VArray (SArray a) -> Just $ Some a + _ -> Nothing + +symExprToValue :: + IsExpr (SymExpr sym) => + W.BaseTypeRepr tp -> + W.SymExpr sym tp -> + Maybe (SValue sym) +symExprToValue tp expr = case tp of + BaseBoolRepr -> Just $ VBool expr + BaseIntegerRepr -> Just $ VInt expr + (BaseBVRepr w) -> Just $ withKnownNat w $ VWord $ DBV expr + (BaseArrayRepr (Ctx.Empty Ctx.:> _) _) -> Just $ VArray $ SArray expr + _ -> Nothing + +-- +-- Integer bit/vector conversions +-- + +-- primitive intToNat : Integer -> Nat; +-- intToNat x == max 0 x +intToNatOp :: forall sym. Sym sym => SValue sym +intToNatOp = + Prims.intFun "intToNat" $ \i -> + case W.asInteger i of + Just i' + | 0 <= i' -> pure (VNat i') + | otherwise -> pure (VNat 0) + Nothing -> + do z <- W.intLit (given :: sym) 0 + pneg <- W.intLt (given :: sym) i z + i' <- W.intIte (given :: sym) pneg z i + pure (VToNat (VInt i')) + +-- primitive natToInt :: Nat -> Integer; +natToIntOp :: forall sym. (Sym sym) => SValue sym +natToIntOp = + Prims.natFun' "natToInt" $ \n -> + VInt <$> W.intLit (given :: sym) (toInteger n) + +-- interpret bitvector as unsigned integer +-- primitive bvToInt :: (n::Nat) -> bitvector n -> Integer; +bvToIntOp :: forall sym. (Sym sym) => SValue sym +bvToIntOp = constFun $ wordFun $ \(v :: SWord sym) -> do + VInt <$> bvToInteger (given :: sym) v + +-- interpret bitvector as signed integer +-- primitive sbvToInt :: (n::Nat) -> bitvector n -> Integer; +sbvToIntOp :: forall sym. (Sym sym) => SValue sym +sbvToIntOp = constFun $ wordFun $ \v -> do + VInt <$> sbvToInteger (given :: sym) v + +-- primitive intToBv :: (n::Nat) -> Integer -> bitvector n; +intToBvOp :: forall sym. (Sym sym) => SValue sym +intToBvOp = + Prims.natFun' "intToBv n" $ \n -> return $ + Prims.intFun "intToBv x" $ \(x :: SymInteger sym) -> + VWord <$> integerToBV (given :: sym) x n + + +-- +-- Shifts +-- + +-- | op :: (n :: Nat) -> bitvector n -> Nat -> bitvector n +bvShiftOp :: (Sym sym) => + (SWord sym -> SWord sym -> IO (SWord sym)) -> + (SWord sym -> Integer -> IO (SWord sym)) -> SValue sym +bvShiftOp bvOp natOp = + constFun $ -- additional argument? the size? + wordFun $ \x -> -- word to shift + return $ + strictFun $ \y -> -- amount to shift as a nat + case y of + VNat i -> VWord <$> natOp x j + where j = i `min` toInteger (intSizeOf x) + VToNat v -> VWord <$> (bvOp x =<< toWord v) + _ -> error $ unwords ["Verifier.SAW.Simulator.What4.bvShiftOp", show y] + +-- bvShl :: (w :: Nat) -> bitvector w -> Nat -> bitvector w; +bvShLOp :: forall sym. (Sym sym) => SValue sym +bvShLOp = bvShiftOp (bvShl given (W.falsePred @sym given)) + (bvShlInt given (W.falsePred @sym given)) + +-- bvShR :: (w :: Nat) -> bitvector w -> Nat -> bitvector w; +bvShROp :: forall sym. (Sym sym) => SValue sym +bvShROp = bvShiftOp (bvShr given (W.falsePred @sym given)) + (bvShrInt given (W.falsePred @sym given)) + + +-- bvShR :: (w :: Nat) -> bitvector w -> Nat -> bitvector w; +bvSShROp :: forall sym. (Sym sym) => SValue sym +bvSShROp = bvShiftOp (bvSShr given (W.falsePred @sym given)) + (bvSShrInt given (W.falsePred @sym given)) + + +-- +-- missing integer operations +-- + +intMin :: (IsExprBuilder sym) => sym -> SInt sym -> SInt sym -> IO (SInt sym) +intMin sym i1 i2 = do + p <- W.intLt sym i1 i2 + W.intIte sym p i1 i2 + +intMax :: (IsExprBuilder sym) => sym -> SInt sym -> SInt sym -> IO (SInt sym) +intMax sym i1 i2 = do + p <- W.intLt sym i1 i2 + W.intIte sym p i2 i1 + +------------------------------------------------------------ +-- Integers mod n + +fromIntModOp :: IsExprBuilder sym => sym -> SValue sym +fromIntModOp sym = + Prims.natFun $ \n -> return $ + Prims.intFun "fromIntModOp" $ \x -> + VInt <$> (W.intMod sym x =<< W.intLit sym (toInteger n)) + +intModEqOp :: IsExprBuilder sym => sym -> SValue sym +intModEqOp sym = + Prims.natFun $ \n -> return $ + Prims.intFun "intModEqOp" $ \x -> return $ + Prims.intFun "intModEqOp" $ \y -> + do modulus <- W.intLit sym (toInteger n) + d <- W.intSub sym x y + r <- W.intMod sym d modulus + z <- W.intLit sym 0 + VBool <$> W.intEq sym r z + +intModBinOp :: + IsExprBuilder sym => sym -> + (sym -> SInt sym -> SInt sym -> IO (SInt sym)) -> SValue sym +intModBinOp sym f = + Prims.natFun $ \n -> return $ + Prims.intFun "intModBinOp x" $ \x -> return $ + Prims.intFun "intModBinOp y" $ \y -> + VInt <$> (normalizeIntMod sym n =<< f sym x y) + +intModUnOp :: + IsExprBuilder sym => sym -> + (sym -> SInt sym -> IO (SInt sym)) -> SValue sym +intModUnOp sym f = + Prims.natFun $ \n -> return $ + Prims.intFun "intModUnOp" $ \x -> + VInt <$> (normalizeIntMod sym n =<< f sym x) + +normalizeIntMod :: IsExprBuilder sym => sym -> Natural -> SInt sym -> IO (SInt sym) +normalizeIntMod sym n x = + case W.asInteger x of + Nothing -> return x + Just i -> W.intLit sym (i `mod` toInteger n) + +------------------------------------------------------------ +-- Stream operations + +-- MkStream :: (a :: sort 0) -> (Nat -> a) -> Stream a; +mkStreamOp :: SValue sym +mkStreamOp = + constFun $ + strictFun $ \f -> do + r <- newIORef Map.empty + return $ VExtra (SStream (\n -> apply f (ready (VNat n))) r) + +-- streamGet :: (a :: sort 0) -> Stream a -> Nat -> a; +streamGetOp :: forall sym. (IsExpr (SymExpr sym), Sym sym) => SValue sym +streamGetOp = + constFun $ + strictFun $ \xs -> return $ + strictFun $ \case + VNat n -> lookupSStream xs (toInteger n) + VToNat w -> + do ilv <- toWord w + selectV (lazyMux @sym muxBVal) ((2 ^ intSizeOf ilv) - 1) (lookupSStream xs) ilv + v -> Prims.panic "streamGetOp" ["Expected Nat value", show v] + +lookupSStream :: SValue sym -> Integer -> IO (SValue sym) +lookupSStream (VExtra (SStream f r)) n = do + m <- readIORef r + case Map.lookup n m of + Just v -> return v + Nothing -> do v <- f n + writeIORef r (Map.insert n v m) + return v +lookupSStream _ _ = fail "expected Stream" + + +muxBVal :: forall sym. (Sym sym) => + SBool sym -> SValue sym -> SValue sym -> IO (SValue sym) +muxBVal = Prims.muxValue prims + +muxWhat4Extra :: + forall sym. (Sym sym) => + SBool sym -> What4Extra sym -> What4Extra sym -> IO (What4Extra sym) +muxWhat4Extra c x y = + do let f i = do xi <- lookupSStream (VExtra x) i + yi <- lookupSStream (VExtra y) i + muxBVal c xi yi + r <- newIORef Map.empty + return (SStream f r) + + +-- | Lifts a strict mux operation to a lazy mux +lazyMux :: (IsExpr (SymExpr sym)) => + (SBool sym -> a -> a -> IO a) -> (SBool sym -> IO a -> IO a -> IO a) +lazyMux muxFn c tm fm = + case W.asConstantPred c of + Just True -> tm + Just False -> fm + Nothing -> do + t <- tm + f <- fm + muxFn c t f + +-- selectV merger maxValue valueFn index returns valueFn v when index has value v +-- if index is greater than maxValue, it returns valueFn maxValue. Use the ite op from merger. +selectV :: forall sym a b. (Sym sym, Ord a, Num a, Bits a) => + (SBool sym -> IO b -> IO b -> IO b) -> a -> (a -> IO b) -> SWord sym -> IO b +selectV merger maxValue valueFn vx = + case bvAsUnsignedInteger vx of + Just i -> valueFn (fromIntegral i) + Nothing -> impl (intSizeOf vx) 0 + where + impl :: Int -> a -> IO b + impl _ x | x > maxValue || x < 0 = valueFn maxValue + impl 0 y = valueFn y + impl i y = do + p <- bvAt (given :: sym) vx j + merger p (impl j (y `setBit` j)) (impl j y) where j = i - 1 + +instance Show (SArray sym) where + show (SArray arr) = show $ W.printSymExpr arr + +arrayConstant :: + W.IsSymExprBuilder sym => + sym -> + SValue sym -> + SValue sym -> + IO (SArray sym) +arrayConstant sym ity elm + | Just (Some idx_repr) <- valueAsBaseType ity + , Just (Some elm_expr) <- valueToSymExpr elm = + SArray <$> W.constantArray sym (Ctx.Empty Ctx.:> idx_repr) elm_expr + | otherwise = + panic "Verifier.SAW.Simulator.What4.Panic.arrayConstant" ["argument type mismatch"] + +arrayLookup :: + W.IsSymExprBuilder sym => + sym -> + SArray sym -> + SValue sym -> + IO (SValue sym) +arrayLookup sym arr idx + | SArray arr_expr <- arr + , Just (Some idx_expr) <- valueToSymExpr idx + , W.BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) elm_repr <- W.exprType arr_expr + , Just Refl <- testEquality idx_repr (W.exprType idx_expr) = do + elm_expr <- W.arrayLookup sym arr_expr (Ctx.Empty Ctx.:> idx_expr) + maybe + (panic "Verifier.SAW.Simulator.What4.Panic.arrayLookup" ["argument type mismatch"]) + return + (symExprToValue elm_repr elm_expr) + | otherwise = + panic "Verifier.SAW.Simulator.What4.Panic.arrayLookup" ["argument type mismatch"] + +arrayUpdate :: + W.IsSymExprBuilder sym => + sym -> + SArray sym -> + SValue sym -> + SValue sym -> + IO (SArray sym) +arrayUpdate sym arr idx elm + | SArray arr_expr <- arr + , Just (Some idx_expr) <- valueToSymExpr idx + , Just (Some elm_expr) <- valueToSymExpr elm + , W.BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) elm_repr <- W.exprType arr_expr + , Just Refl <- testEquality idx_repr (W.exprType idx_expr) + , Just Refl <- testEquality elm_repr (W.exprType elm_expr) = + SArray <$> W.arrayUpdate sym arr_expr (Ctx.Empty Ctx.:> idx_expr) elm_expr + | otherwise = + panic "Verifier.SAW.Simulator.What4.Panic.arrayUpdate" ["argument type mismatch"] + +arrayEq :: + W.IsSymExprBuilder sym => + sym -> + SArray sym -> + SArray sym -> + IO (W.Pred sym) +arrayEq sym lhs_arr rhs_arr + | SArray lhs_arr_expr <- lhs_arr + , SArray rhs_arr_expr <- rhs_arr + , W.BaseArrayRepr (Ctx.Empty Ctx.:> lhs_idx_repr) lhs_elm_repr <- W.exprType lhs_arr_expr + , W.BaseArrayRepr (Ctx.Empty Ctx.:> rhs_idx_repr) rhs_elm_repr <- W.exprType rhs_arr_expr + , Just Refl <- testEquality lhs_idx_repr rhs_idx_repr + , Just Refl <- testEquality lhs_elm_repr rhs_elm_repr = + W.arrayEq sym lhs_arr_expr rhs_arr_expr + | otherwise = + panic "Verifier.SAW.Simulator.What4.Panic.arrayEq" ["argument type mismatch"] + +---------------------------------------------------------------------- +-- | A basic symbolic simulator/evaluator: interprets a saw-core Term as +-- a symbolic value + +w4SolveBasic :: + forall sym. (Given sym, IsSymExprBuilder sym) => + ModuleMap -> + Map Ident (SValue sym) {- ^ additional primitives -} -> + IORef (SymFnCache sym) {- ^ cache for uninterpreted function symbols -} -> + [String] {- ^ 'unints' Constants in this list are kept uninterpreted -} -> + Term {- ^ term to simulate -} -> + IO (SValue sym) +w4SolveBasic m addlPrims ref unints t = + do let unintSet = Set.fromList unints + let sym = given :: sym + let extcns (EC ix nm ty) = parseUninterpreted sym ref (mkUnintApp (nm ++ "_" ++ show ix)) ty + let uninterpreted ec + | Set.member (ecName ec) unintSet = Just (extcns ec) + | otherwise = Nothing + cfg <- Sim.evalGlobal m (constMap `Map.union` addlPrims) extcns uninterpreted + Sim.evalSharedTerm cfg t + + +---------------------------------------------------------------------- +-- Uninterpreted function cache + +data SymFnWrapper sym :: Ctx.Ctx BaseType -> * where + SymFnWrapper :: !(W.SymFn sym args ret) -> SymFnWrapper sym (args Ctx.::> ret) + +type SymFnCache sym = Map W.SolverSymbol (MapF (Assignment BaseTypeRepr) (SymFnWrapper sym)) + +lookupSymFn :: + W.SolverSymbol -> Assignment BaseTypeRepr args -> BaseTypeRepr ty -> + SymFnCache sym -> Maybe (W.SymFn sym args ty) +lookupSymFn s args ty cache = + do m <- Map.lookup s cache + SymFnWrapper fn <- MapF.lookup (Ctx.extend args ty) m + return fn + +insertSymFn :: + W.SolverSymbol -> Assignment BaseTypeRepr args -> BaseTypeRepr ty -> + W.SymFn sym args ty -> SymFnCache sym -> SymFnCache sym +insertSymFn s args ty fn = Map.alter upd s + where + upd Nothing = Just (MapF.singleton (Ctx.extend args ty) (SymFnWrapper fn)) + upd (Just m) = Just (MapF.insert (Ctx.extend args ty) (SymFnWrapper fn) m) + +mkSymFn :: + forall sym args ret. (IsSymExprBuilder sym) => + sym -> IORef (SymFnCache sym) -> + String -> Assignment BaseTypeRepr args -> BaseTypeRepr ret -> + IO (W.SymFn sym args ret) +mkSymFn sym ref nm args ret = + case W.userSymbol nm of + Left err -> fail $ show err ++ ": Cannot create uninterpreted constant " ++ nm + Right s -> + do cache <- readIORef ref + case lookupSymFn s args ret cache of + Just fn -> return fn + Nothing -> + do fn <- W.freshTotalUninterpFn sym s args ret + writeIORef ref (insertSymFn s args ret fn cache) + return fn + +---------------------------------------------------------------------- +-- Given a constant nm of (saw-core) type ty, construct an uninterpreted +-- constant with that type. +-- Importantly: The types of these uninterpreted values are *not* +-- limited to What4 BaseTypes or FirstOrderTypes. + +parseUninterpreted :: + forall sym. + (IsSymExprBuilder sym) => + sym -> IORef (SymFnCache sym) -> + UnintApp (SymExpr sym) -> + SValue sym -> IO (SValue sym) +parseUninterpreted sym ref app ty = + case ty of + VPiType _ f + -> return $ + strictFun $ \x -> do + app' <- applyUnintApp app x + t2 <- f (ready x) + parseUninterpreted sym ref app' t2 + + VBoolType + -> VBool <$> mkUninterpreted sym ref app BaseBoolRepr + + VIntType + -> VInt <$> mkUninterpreted sym ref app BaseIntegerRepr + + -- 0 width bitvector is a constant + VVecType (VNat 0) VBoolType + -> return $ VWord ZBV + + VVecType (VNat n) VBoolType + | Just (Some (PosNat w)) <- somePosNat n + -> (VWord . DBV) <$> mkUninterpreted sym ref app (BaseBVRepr w) + + VVecType (VNat n) ety + -> do xs <- sequence $ + [ parseUninterpreted sym ref (suffixUnintApp ("_a" ++ show i) app) ety + | i <- [0 .. n-1] ] + return (VVector (V.fromList (map ready xs))) + + VArrayType ity ety + | Just (Some idx_repr) <- valueAsBaseType ity + , Just (Some elm_repr) <- valueAsBaseType ety + -> (VArray . SArray) <$> + mkUninterpreted sym ref app (BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) elm_repr) + + VUnitType + -> return VUnit + + VPairType ty1 ty2 + -> do x1 <- parseUninterpreted sym ref (suffixUnintApp "_L" app) ty1 + x2 <- parseUninterpreted sym ref (suffixUnintApp "_R" app) ty2 + return (VPair (ready x1) (ready x2)) + + VRecordType elem_tps + -> (VRecordValue <$> + mapM (\(f,tp) -> + (f,) <$> ready <$> + parseUninterpreted sym ref (suffixUnintApp ("_" ++ f) app) tp) elem_tps) + + _ -> fail $ "could not create uninterpreted symbol of type " ++ show ty + + +mkUninterpreted :: + forall sym t. (IsSymExprBuilder sym) => + sym -> IORef (SymFnCache sym) -> + UnintApp (SymExpr sym) -> + BaseTypeRepr t -> + IO (SymExpr sym t) +mkUninterpreted sym ref (UnintApp nm args tys) ret = + do fn <- mkSymFn sym ref nm tys ret + W.applySymFn sym fn args + +-- | A value of type @UnintApp f@ represents an uninterpreted function +-- with the given 'String' name, applied to a list of argument values +-- paired with a representation of their types. The context of +-- argument types is existentially quantified. +data UnintApp f = + forall args. UnintApp String (Assignment f args) (Assignment BaseTypeRepr args) + +-- | Make an 'UnintApp' with the given name and no arguments. +mkUnintApp :: String -> UnintApp f +mkUnintApp nm = UnintApp nm Ctx.empty Ctx.empty + +-- | Add a suffix to the function name of an 'UnintApp'. +suffixUnintApp :: String -> UnintApp f -> UnintApp f +suffixUnintApp s (UnintApp nm args tys) = UnintApp (nm ++ s) args tys + +-- | Extend an 'UnintApp' with an additional argument. +extendUnintApp :: UnintApp f -> f ty -> BaseTypeRepr ty -> UnintApp f +extendUnintApp (UnintApp nm xs tys) x ty = + UnintApp nm (Ctx.extend xs x) (Ctx.extend tys ty) + +-- | Flatten an 'SValue' to a sequence of components, each of which is +-- a symbolic value of a base type (e.g. word or boolean), and add +-- them to the list of arguments of the given 'UnintApp'. If the +-- 'SValue' contains any values built from data constructors, then +-- encode them as suffixes on the function name of the 'UnintApp'. +applyUnintApp :: + forall sym. + UnintApp (SymExpr sym) -> + SValue sym -> + IO (UnintApp (SymExpr sym)) +applyUnintApp app0 v = + case v of + VUnit -> return app0 + VPair x y -> do app1 <- applyUnintApp app0 =<< force x + app2 <- applyUnintApp app1 =<< force y + return app2 + VRecordValue elems -> foldM applyUnintApp app0 =<< traverse (force . snd) elems + VVector xv -> foldM applyUnintApp app0 =<< traverse force xv + VBool sb -> return (extendUnintApp app0 sb BaseBoolRepr) + VInt si -> return (extendUnintApp app0 si BaseIntegerRepr) + VWord (DBV sw) -> return (extendUnintApp app0 sw (W.exprType sw)) + VArray (SArray sa) -> return (extendUnintApp app0 sa (W.exprType sa)) + VWord ZBV -> return app0 + VCtorApp i xv -> foldM applyUnintApp app' =<< traverse force xv + where app' = suffixUnintApp ("_" ++ identName i) app0 + VNat n -> return (suffixUnintApp ("_" ++ show n) app0) + _ -> fail $ "Could not create argument for " ++ show v + +------------------------------------------------------------ + +w4SolveAny :: + forall sym. (IsSymExprBuilder sym) => + sym -> SharedContext -> Map Ident (SValue sym) -> [String] -> Term -> + IO ([String], ([Maybe (Labeler sym)], SValue sym)) +w4SolveAny sym sc ps unints t = give sym $ do + modmap <- scGetModuleMap sc + ref <- newIORef Map.empty + let eval = w4SolveBasic modmap ps ref unints + ty <- eval =<< scTypeOf sc t + + -- get the names of the arguments to the function + let argNames = map fst (fst (R.asLambdaList t)) + let moreNames = [ "var" ++ show (i :: Integer) | i <- [0 ..] ] + + -- and their types + argTs <- argTypes ty + + -- construct symbolic expressions for the variables + vars' <- + flip evalStateT 0 $ + sequence (zipWith (newVarsForType ref) argTs (argNames ++ moreNames)) + + -- symbolically evaluate + bval <- eval t + + -- apply and existentially quantify + let (bvs, vars) = unzip vars' + let vars'' = fmap ready vars + bval' <- applyAll bval vars'' + + return (argNames, (bvs, bval')) + +w4Solve :: + forall sym. (IsSymExprBuilder sym) => + sym -> SharedContext -> Map Ident (SValue sym) -> [String] -> Term -> + IO ([String], ([Maybe (Labeler sym)], SBool sym)) +w4Solve sym sc ps unints t = + do (argNames, (bvs, bval)) <- w4SolveAny sym sc ps unints t + case bval of + VBool b -> return (argNames, (bvs, b)) + _ -> fail $ "w4Solve: non-boolean result type. " ++ show bval + + +-- +-- Pull out argument types until bottoming out at a non-Pi type +-- +argTypes :: IsSymExprBuilder sv => SValue sv -> IO [SValue sv] +argTypes v = + case v of + VPiType v1 f -> + do v2 <- f (error "argTypes: unsupported dependent SAW-Core type") + vs <- argTypes v2 + return (v1 : vs) + _ -> return [] + +-- +-- Convert a saw-core type expression to a FirstOrder type expression +-- +vAsFirstOrderType :: forall sv. IsSymExprBuilder sv => SValue sv -> Maybe FirstOrderType +vAsFirstOrderType v = + case v of + VBoolType + -> return FOTBit + VIntType + -> return FOTInt + VVecType (VNat n) v2 + -> FOTVec (fromInteger n) <$> vAsFirstOrderType v2 + VArrayType iv ev + -> FOTArray <$> vAsFirstOrderType iv <*> vAsFirstOrderType ev + VUnitType + -> return (FOTTuple []) + VPairType v1 v2 + -> do t1 <- vAsFirstOrderType v1 + t2 <- vAsFirstOrderType v2 + case t2 of + FOTTuple ts -> return (FOTTuple (t1 : ts)) + _ -> return (FOTTuple [t1, t2]) + VRecordType tps + -> (FOTRec <$> Map.fromList <$> + mapM (\(f,tp) -> (f,) <$> vAsFirstOrderType tp) tps) + _ -> Nothing + +valueAsBaseType :: IsSymExprBuilder sym => SValue sym -> Maybe (Some W.BaseTypeRepr) +valueAsBaseType v = fmap fotToBaseType $ vAsFirstOrderType v + +------------------------------------------------------------------------------ + +-- | Generate a new symbolic value (a variable) from a given first-order-type + + +data TypedExpr sym where + TypedExpr :: BaseTypeRepr ty -> SymExpr sym ty -> TypedExpr sym + + +-- | Generate a new variable from a given BaseType + +freshVar :: forall sym ty. (IsSymExprBuilder sym, Given sym) => + BaseTypeRepr ty -> String -> IO (TypedExpr sym) +freshVar ty str = + case W.userSymbol str of + Right solverSymbol -> do + c <- W.freshConstant (given :: sym) solverSymbol ty + return (TypedExpr ty c) + Left _ -> + fail $ "Cannot create solver symbol " ++ str + +nextId :: StateT Int IO String +nextId = ST.get >>= (\s-> modify (+1) >> return ("x" ++ show s)) + + +newVarsForType :: forall sym. (Given sym, IsSymExprBuilder sym) => + IORef (SymFnCache sym) -> + SValue sym -> String -> StateT Int IO (Maybe (Labeler sym), SValue sym) +newVarsForType ref v nm = + case vAsFirstOrderType v of + Just fot -> do + do (te,sv) <- newVarFOT fot + return (Just te, sv) + + Nothing -> + do sv <- lift $ parseUninterpreted sym ref (mkUnintApp nm) v + return (Nothing, sv) + where sym = given :: sym + +myfun ::(Map String (Labeler sym, SValue sym)) -> (Map String (Labeler sym), Map String (SValue sym)) +myfun = fmap fst A.&&& fmap snd + +data Labeler sym + = BaseLabel (TypedExpr sym) + | VecLabel (Vector (Labeler sym)) + | TupleLabel (Vector (Labeler sym)) + | RecLabel (Map FieldName (Labeler sym)) + + +newVarFOT :: forall sym. (IsSymExprBuilder sym, Given sym) => + FirstOrderType -> StateT Int IO (Labeler sym, SValue sym) + +newVarFOT (FOTTuple ts) = do + (labels,vals) <- V.unzip <$> traverse newVarFOT (V.fromList ts) + args <- traverse (return . ready) (V.toList vals) + return (TupleLabel labels, vTuple args) + +newVarFOT (FOTVec n tp) + | tp /= FOTBit + = do (labels,vals) <- V.unzip <$> V.replicateM (fromIntegral n) (newVarFOT tp) + args <- traverse @Vector @(StateT Int IO) (return . ready) vals + return (VecLabel labels, VVector args) + +newVarFOT (FOTRec tm) + = do (labels, vals) <- myfun <$> traverse newVarFOT tm + args <- traverse (return . ready) (vals :: (Map String (SValue sym))) + return (RecLabel labels, vRecord args) + +newVarFOT fot + | Some r <- fotToBaseType fot + = do nm <- nextId + te <- lift $ freshVar r nm + sv <- lift $ typedToSValue te + return (BaseLabel te, sv) + + + +typedToSValue :: (IsExpr (SymExpr sym)) => TypedExpr sym -> IO (SValue sym) +typedToSValue (TypedExpr ty expr) = + maybe (fail "Cannot handle") return $ symExprToValue ty expr + +---------------------------------------------------------------------- +-- Evaluation through crucible-saw backend + + +-- | Simplify a saw-core term by evaluating it through the saw backend +-- of what4. +w4EvalAny :: + forall n solver fs. + CS.SAWCoreBackend n solver fs -> SharedContext -> + Map Ident (SValue (CS.SAWCoreBackend n solver fs)) -> [String] -> Term -> + IO ([String], ([Maybe (Labeler (CS.SAWCoreBackend n solver fs))], SValue (CS.SAWCoreBackend n solver fs))) +w4EvalAny sym sc ps unints t = + do modmap <- scGetModuleMap sc + ref <- newIORef Map.empty + let eval = w4EvalBasic sym sc modmap ps ref unints + ty <- eval =<< scTypeOf sc t + + -- get the names of the arguments to the function + let lamNames = map fst (fst (R.asLambdaList t)) + let varNames = [ "var" ++ show (i :: Integer) | i <- [0 ..] ] + let argNames = zipWith (++) varNames (map ("_" ++) lamNames ++ repeat "") + + -- and their types + argTs <- argTypes ty + + -- construct symbolic expressions for the variables + vars' <- + give sym $ + flip evalStateT 0 $ + sequence (zipWith (newVarsForType ref) argTs argNames) + + -- symbolically evaluate + bval <- eval t + + -- apply and existentially quantify + let (bvs, vars) = unzip vars' + let vars'' = fmap ready vars + bval' <- applyAll bval vars'' + + return (argNames, (bvs, bval')) + +w4Eval :: + forall n solver fs. + CS.SAWCoreBackend n solver fs -> SharedContext -> + Map Ident (SValue (CS.SAWCoreBackend n solver fs)) -> [String] -> Term -> + IO ([String], ([Maybe (Labeler (CS.SAWCoreBackend n solver fs))], SBool (CS.SAWCoreBackend n solver fs))) +w4Eval sym sc ps uints t = + do (argNames, (bvs, bval)) <- w4EvalAny sym sc ps uints t + case bval of + VBool b -> return (argNames, (bvs, b)) + _ -> fail $ "w4Eval: non-boolean result type. " ++ show bval + +-- | Simplify a saw-core term by evaluating it through the saw backend +-- of what4. +w4EvalBasic :: + forall n solver fs. + CS.SAWCoreBackend n solver fs -> + SharedContext -> + ModuleMap -> + Map Ident (SValue (CS.SAWCoreBackend n solver fs)) {- ^ additional primitives -} -> + IORef (SymFnCache (CS.SAWCoreBackend n solver fs)) {- ^ cache for uninterpreted function symbols -} -> + [String] {- ^ 'unints' Constants in this list are kept uninterpreted -} -> + Term {- ^ term to simulate -} -> + IO (SValue (CS.SAWCoreBackend n solver fs)) +w4EvalBasic sym sc m addlPrims ref unints t = + do let unintSet = Set.fromList unints + let extcns tf (EC ix nm ty) = + do trm <- ArgTermConst <$> scTermF sc tf + parseUninterpretedSAW sym sc ref trm (mkUnintApp (nm ++ "_" ++ show ix)) ty + let uninterpreted tf ec + | Set.member (ecName ec) unintSet = Just (extcns tf ec) + | otherwise = Nothing + cfg <- Sim.evalGlobal' m (give sym constMap `Map.union` addlPrims) extcns uninterpreted + Sim.evalSharedTerm cfg t + +-- | Given a constant nm of (saw-core) type ty, construct an +-- uninterpreted constant with that type. The 'Term' argument should +-- be an open term, which should have the designated return type when +-- the local variables have the corresponding types from the +-- 'Assignment'. +parseUninterpretedSAW :: + forall n solver fs. + CS.SAWCoreBackend n solver fs -> SharedContext -> + IORef (SymFnCache (CS.SAWCoreBackend n solver fs)) -> + ArgTerm {- ^ representation of function applied to arguments -} -> + UnintApp (SymExpr (CS.SAWCoreBackend n solver fs)) -> + SValue (CS.SAWCoreBackend n solver fs) {- ^ return type -} -> + IO (SValue (CS.SAWCoreBackend n solver fs)) +parseUninterpretedSAW sym sc ref trm app ty = + case ty of + VPiType t1 f + -> return $ + strictFun $ \x -> do + app' <- applyUnintApp app x + arg <- mkArgTerm sc t1 x + let trm' = ArgTermApply trm arg + t2 <- f (ready x) + parseUninterpretedSAW sym sc ref trm' app' t2 + + VBoolType + -> VBool <$> mkUninterpretedSAW sym ref trm app BaseBoolRepr + + VIntType + -> VInt <$> mkUninterpretedSAW sym ref trm app BaseIntegerRepr + + -- 0 width bitvector is a constant + VVecType (VNat 0) VBoolType + -> return $ VWord ZBV + + VVecType (VNat n) VBoolType + | Just (Some (PosNat w)) <- somePosNat n + -> (VWord . DBV) <$> mkUninterpretedSAW sym ref trm app (BaseBVRepr w) + + VVecType (VNat n) ety + -> do ety' <- termOfSValue sc ety + let mkElem i = + do let trm' = ArgTermAt n ety' trm i + let app' = suffixUnintApp ("_a" ++ show i) app + parseUninterpretedSAW sym sc ref trm' app' ety + xs <- traverse mkElem [0 .. n-1] + return (VVector (V.fromList (map ready xs))) + + VArrayType ity ety + | Just (Some idx_repr) <- valueAsBaseType ity + , Just (Some elm_repr) <- valueAsBaseType ety + -> (VArray . SArray) <$> + mkUninterpretedSAW sym ref trm app (BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) elm_repr) + + VUnitType + -> return VUnit + + VPairType ty1 ty2 + -> do let trm1 = ArgTermPairLeft trm + let trm2 = ArgTermPairRight trm + x1 <- parseUninterpretedSAW sym sc ref trm1 (suffixUnintApp "_L" app) ty1 + x2 <- parseUninterpretedSAW sym sc ref trm2 (suffixUnintApp "_R" app) ty2 + return (VPair (ready x1) (ready x2)) + + _ -> fail $ "could not create uninterpreted symbol of type " ++ show ty + +mkUninterpretedSAW :: + forall n solver fs t. + CS.SAWCoreBackend n solver fs -> IORef (SymFnCache (CS.SAWCoreBackend n solver fs)) -> + ArgTerm -> + UnintApp (SymExpr (CS.SAWCoreBackend n solver fs)) -> + BaseTypeRepr t -> + IO (SymExpr (CS.SAWCoreBackend n solver fs) t) +mkUninterpretedSAW sym ref trm (UnintApp nm args tys) ret = + do fn <- mkSymFn sym ref nm tys ret + CS.sawRegisterSymFunInterp sym fn (reconstructArgTerm trm) + W.applySymFn sym fn args + +-- | An 'ArgTerm' is a description of how to reassemble a saw-core +-- term from a list of the atomic components it is composed of. +data ArgTerm + = ArgTermVar + | ArgTermBVZero -- ^ scBvNat 0 0 + | ArgTermVector Term [ArgTerm] -- ^ element type, elements + | ArgTermUnit + | ArgTermPair ArgTerm ArgTerm + | ArgTermRecord [(String, ArgTerm)] + | ArgTermConst Term + | ArgTermApply ArgTerm ArgTerm + | ArgTermAt Integer Term ArgTerm Integer + -- ^ length, element type, list, index + | ArgTermPairLeft ArgTerm + | ArgTermPairRight 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 +-- 'ArgTermVar' constructors in the 'ArgTerm'. +reconstructArgTerm :: ArgTerm -> SharedContext -> [Term] -> IO Term +reconstructArgTerm atrm sc ts = + do (t, unused) <- parse atrm ts + unless (null unused) $ fail "reconstructArgTerm: too many function arguments" + return t + where + parse :: ArgTerm -> [Term] -> IO (Term, [Term]) + parse at ts0 = + case at of + ArgTermVar -> + case ts0 of + x : ts1 -> return (x, ts1) + [] -> fail "reconstructArgTerm: too few function arguments" + ArgTermBVZero -> + do z <- scNat sc 0 + x <- scBvNat sc z z + return (x, ts0) + ArgTermVector ty ats -> + do (xs, ts1) <- parseList ats ts0 + x <- scVector sc ty xs + return (x, ts1) + ArgTermUnit -> + do x <- scUnitValue sc + return (x, ts0) + ArgTermPair at1 at2 -> + do (x1, ts1) <- parse at1 ts0 + (x2, ts2) <- parse at2 ts1 + x <- scPairValue sc x1 x2 + return (x, ts2) + ArgTermRecord flds -> + do let (tags, ats) = unzip flds + (xs, ts1) <- parseList ats ts0 + x <- scRecord sc (Map.fromList (zip tags xs)) + return (x, ts1) + ArgTermConst x -> + do return (x, ts0) + ArgTermApply at1 at2 -> + do (x1, ts1) <- parse at1 ts0 + (x2, ts2) <- parse at2 ts1 + x <- scApply sc x1 x2 + return (x, ts2) + ArgTermAt n ty at1 i -> + do n' <- scNat sc (fromInteger n) + (x1, ts1) <- parse at1 ts0 + i' <- scNat sc (fromInteger i) + x <- scAt sc n' ty x1 i' + return (x, ts1) + ArgTermPairLeft at1 -> + do (x1, ts1) <- parse at1 ts0 + x <- scPairLeft sc x1 + return (x, ts1) + ArgTermPairRight at1 -> + do (x1, ts1) <- parse at1 ts0 + x <- scPairRight sc x1 + return (x, ts1) + + parseList :: [ArgTerm] -> [Term] -> IO ([Term], [Term]) + parseList [] ts0 = return ([], ts0) + parseList (at : ats) ts0 = + do (x, ts1) <- parse at ts0 + (xs, ts2) <- parseList ats ts1 + return (x : xs, ts2) + +-- | Given a type and value encoded as 'SValue's, construct an +-- 'ArgTerm' that builds a term of that type from local variables with +-- base types. The number of 'ArgTermVar' constructors should match +-- the number of arguments appended by 'applyUnintApp'. +mkArgTerm :: SharedContext -> SValue sym -> SValue sym -> IO ArgTerm +mkArgTerm sc ty val = + case (ty, val) of + (VBoolType, VBool _) -> return ArgTermVar + (VIntType, VInt _) -> return ArgTermVar + (_, VWord ZBV) -> return ArgTermBVZero -- 0-width bitvector is a constant + (_, VWord (DBV _)) -> return ArgTermVar + (VUnitType, VUnit) -> return ArgTermUnit + + (VVecType _ ety, VVector vv) -> + do vs <- traverse force (V.toList vv) + xs <- traverse (mkArgTerm sc ety) vs + ety' <- termOfSValue sc ety + return (ArgTermVector ety' xs) + + (VPairType ty1 ty2, VPair v1 v2) -> + do x1 <- mkArgTerm sc ty1 =<< force v1 + x2 <- mkArgTerm sc ty2 =<< force v2 + return (ArgTermPair x1 x2) + + (VRecordType tys, VRecordValue flds) | map fst tys == map fst flds -> + do let tags = map fst tys + vs <- traverse (force . snd) flds + xs <- sequence [ mkArgTerm sc t v | (t, v) <- zip (map snd tys) vs ] + return (ArgTermRecord (zip tags xs)) + + (_, VCtorApp i vv) -> + do xs <- traverse (termOfSValue sc <=< force) (V.toList vv) + x <- scCtorApp sc i xs + return (ArgTermConst x) + + _ -> fail $ "could not create uninterpreted function argument of type " ++ show ty + +termOfSValue :: SharedContext -> SValue sym -> IO Term +termOfSValue sc val = + case val of + VUnit -> scUnitValue sc + VBoolType -> scBoolType sc + VIntType -> scIntegerType sc + VUnitType -> scUnitType sc + VVecType (VNat n) a -> + do n' <- scNat sc (fromInteger n) + a' <- termOfSValue sc a + scVecType sc n' a' + VPairType a b + -> do a' <- termOfSValue sc a + b' <- termOfSValue sc b + scPairType sc a' b' + VRecordType flds + -> do flds' <- traverse (traverse (termOfSValue sc)) flds + scRecordType sc flds' + VNat n + -> scNat sc (fromInteger n) + _ -> fail $ "termOfSValue: " ++ show val diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4/FirstOrder.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4/FirstOrder.hs new file mode 100644 index 0000000000..1d62689a70 --- /dev/null +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4/FirstOrder.hs @@ -0,0 +1,127 @@ +------------------------------------------------------------------------ +-- | +-- Module : Verifier.SAW.Simulator.What4.FirstOrder +-- Copyright : Galois, Inc. 2012-2015 +-- License : BSD3 +-- Maintainer : sweirich@galois.com +-- Stability : experimental +-- Portability : non-portable (language extensions) +-- +-- Connect What4's 'BaseType' with saw-core's 'FirstOrderType' +-- (both types and values of Base/FirstOrder type) +-- TODO NOTE: support for tuples, arrays and records is not complete +-- but is also unused in Verifier.SAW.Simulator.What4 +------------------------------------------------------------------------ +{-# LANGUAGE CPP #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE ViewPatterns #-} + +module Verifier.SAW.Simulator.What4.FirstOrder + ( + fotToBaseType, + typeReprToFOT, + groundToFOV + ) where + +import qualified Data.BitVector.Sized as BV +import Data.Parameterized.TraversableFC (FoldableFC(..)) +import Data.Parameterized.Some(Some(..)) +import Data.Parameterized.Context hiding (replicate) + +import Verifier.SAW.Simulator.What4.PosNat + +import Verifier.SAW.FiniteValue (FirstOrderType(..),FirstOrderValue(..)) + +import What4.BaseTypes +import What4.Expr.GroundEval + +--------------------------------------------------------------------- + +-- | Convert a type expression from SAW-core to What4 +fotToBaseType :: FirstOrderType -> Some BaseTypeRepr +fotToBaseType FOTBit + = Some BaseBoolRepr +fotToBaseType FOTInt + = Some BaseIntegerRepr +fotToBaseType (FOTVec nat FOTBit) + | Just (Some (PosNat nr)) <- somePosNat nat + = Some (BaseBVRepr nr) + | otherwise -- 0-width bit vector is 0 + = Some BaseIntegerRepr +fotToBaseType (FOTVec nat fot) + | Some assn <- listToAssn (replicate (fromIntegral nat) fot) + = Some (BaseStructRepr assn) +fotToBaseType (FOTArray fot1 fot2) + | Some ty1 <- fotToBaseType fot1 + , Some ty2 <- fotToBaseType fot2 + = Some $ BaseArrayRepr (Empty :> ty1) ty2 +fotToBaseType (FOTTuple fots) + | Some assn <- listToAssn fots + = Some (BaseStructRepr assn) +fotToBaseType (FOTRec _) + = error "TODO: convert to What4 records ?!" + +listToAssn :: [FirstOrderType] -> Some (Assignment BaseTypeRepr) +listToAssn [] = Some empty +listToAssn (fot:rest) = + case (fotToBaseType fot, listToAssn rest) of + (Some bt, Some assn) -> Some $ extend assn bt + +--------------------------------------------------------------------- +-- | Convert a type expression from What4 to SAW-core + +typeReprToFOT :: BaseTypeRepr ty -> Either String FirstOrderType +typeReprToFOT BaseBoolRepr = pure FOTBit +typeReprToFOT BaseNatRepr = pure FOTInt +typeReprToFOT BaseIntegerRepr = pure FOTInt +typeReprToFOT (BaseBVRepr w) = pure $ FOTVec (natValue w) FOTBit +typeReprToFOT BaseRealRepr = Left "No FO Real" +typeReprToFOT BaseComplexRepr = Left "No FO Complex" +typeReprToFOT (BaseStringRepr _) = Left "No FO String" +typeReprToFOT (BaseArrayRepr (Empty :> ty) b) + | Right fot1 <- typeReprToFOT ty + , Right fot2 <- typeReprToFOT b + = pure $ FOTArray fot1 fot2 +typeReprToFOT ty@(BaseArrayRepr _ctx _b) = Left $ "Unsupported FO Array: " ++ show ty +typeReprToFOT (BaseFloatRepr _) = Left "No FO Floating point" +typeReprToFOT (BaseStructRepr ctx) = FOTTuple <$> assnToList ctx + +assnToList :: Assignment BaseTypeRepr ctx -> Either String [FirstOrderType] +assnToList = foldrFC g (Right []) where + g :: BaseTypeRepr x -> Either String [FirstOrderType] -> Either String [FirstOrderType] + g ty l = (:) <$> typeReprToFOT ty <*> l + + +--------------------------------------------------------------------- +-- | Convert between What4 GroundValues and saw-core FirstOrderValues + +groundToFOV :: BaseTypeRepr ty -> GroundValue ty -> Either String FirstOrderValue +groundToFOV BaseBoolRepr b = pure $ FOVBit b +groundToFOV BaseNatRepr n = pure $ FOVInt (toInteger n) +groundToFOV BaseIntegerRepr i = pure $ FOVInt i +groundToFOV (BaseBVRepr w) bv = pure $ FOVWord (natValue w) (BV.asUnsigned bv) +groundToFOV BaseRealRepr _ = Left "Real is not FOV" +groundToFOV BaseComplexRepr _ = Left "Complex is not FOV" +groundToFOV (BaseStringRepr _) _ = Left "String is not FOV" +groundToFOV (BaseFloatRepr _) _ = Left "Floating point is not FOV" +groundToFOV (BaseArrayRepr (Empty :> ty) b) _ + | Right fot1 <- typeReprToFOT ty + , Right fot2 <- typeReprToFOT b + = pure $ FOVArray fot1 fot2 +groundToFOV (BaseArrayRepr _idx _b) _ = Left "Unsupported FOV Array" +groundToFOV (BaseStructRepr ctx) tup = FOVTuple <$> tupleToList ctx tup + + +tupleToList :: Assignment BaseTypeRepr ctx -> + Assignment GroundValueWrapper ctx -> Either String [FirstOrderValue] +tupleToList (viewAssign -> AssignEmpty) (viewAssign -> AssignEmpty) = Right [] +tupleToList (viewAssign -> AssignExtend rs r) (viewAssign -> AssignExtend gvs gv) = + (:) <$> groundToFOV r (unGVW gv) <*> tupleToList rs gvs +#if !MIN_VERSION_GLASGOW_HASKELL(8,10,0,0) +tupleToList _ _ = error "GADTs should rule this out." +#endif \ No newline at end of file diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4/Panic.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4/Panic.hs new file mode 100644 index 0000000000..635f1f500c --- /dev/null +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4/Panic.hs @@ -0,0 +1,22 @@ +{-# LANGUAGE Trustworthy #-} +{-# LANGUAGE TemplateHaskell #-} + +module Verifier.SAW.Simulator.What4.Panic + ( panic + ) where + +import Panic hiding (panic) +import qualified Panic + +data SAWCoreWhat4 = SAWCoreWhat4 + +panic :: HasCallStack => String -> [String] -> a +panic = Panic.panic SAWCoreWhat4 + +instance PanicComponent SAWCoreWhat4 where + panicComponentName _ = "SAWCoreWhat4" + panicComponentIssues _ = "https://github.com/GaloisInc/saw-core-what4/issues" + + {-# Noinline panicComponentRevision #-} + panicComponentRevision = $useGitRevision + diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4/PosNat.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4/PosNat.hs new file mode 100644 index 0000000000..a8f842f5dd --- /dev/null +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4/PosNat.hs @@ -0,0 +1,95 @@ +------------------------------------------------------------------------ +-- | +-- Module : Verifier.SAW.Simulator.What4.PosNat +-- Copyright : Galois, Inc. 2018 +-- License : BSD3 +-- Maintainer : sweirich@galois.com +-- Stability : experimental +-- Portability : non-portable (language extensions) +-- +-- A runtime representation of positive nats +------------------------------------------------------------------------ + +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DoAndIfThenElse #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeApplications #-} + +-- This module makes use of 'KnownNat' constraints in its interface as +-- opposed to arguments of type 'NatRepr' or 'PosNatRepr' +-- (cf. 'addPosNat'). As a result, we need two + +-- to allow implicitly provided nats +{-# LANGUAGE AllowAmbiguousTypes #-} + +-- to allow 'WithKnownNat' +{-# OPTIONS_GHC -Wno-warnings-deprecations #-} + +module Verifier.SAW.Simulator.What4.PosNat where +-- TODO: find the right place for this code + +import GHC.TypeNats +import Data.Parameterized.NatRepr +import Data.Parameterized.Some(Some(..)) + + +-- We include the KnownNat constraint here so that we can avoid using +-- withKnownNat outside this module. The downside is that we have two +-- different runtime representations of these positive nats --- the +-- one stored in the KnownNat, and the one stored in the NatRepr. + +-- | Runtime representation of a non-zero natural number +data PosNat (n :: Nat) where + PosNat :: (1 <= n, KnownNat n) => NatRepr n -> PosNat n + +-- | Check whether an integer is a positive nat +somePosNat :: Integral a => a -> Maybe (Some PosNat) +somePosNat n + | Just (Some nr) <- someNat n, + Just LeqProof <- testLeq (knownNat @1) nr + = withKnownNat nr $ Just (Some (PosNat nr)) + | otherwise + = Nothing + +-- The above definition should be added to +-- 'Data.Parameterized.NatRepr' so that the redundant check for +-- positivity can be removed. Annoyingly, we cannot do 'testLeq' +-- without already knowing that w >= 0) + + +-- | Add two numbers together and return a proof that their +-- result is positive. +addPosNat :: forall w1 w2. + (1 <= w1, 1 <= w2, KnownNat w1, KnownNat w2) => PosNat (w1 + w2) +addPosNat = + let w1 = knownNat @w1 + w2 = knownNat @w2 + sm = addNat w1 w2 in + case leqAddPos w1 w2 of + LeqProof -> withKnownNat sm $ PosNat sm + +-- I would hope that the 'leqAddPos' call can be compiled away... + + +--- Not needed but included for completeness + +-- | Compare for equality, returning witness if true +instance TestEquality PosNat where + testEquality (PosNat n1) (PosNat n2) = + case testEquality n1 n2 of + Just Refl -> Just Refl + Nothing -> Nothing diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4/SWord.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4/SWord.hs new file mode 100644 index 0000000000..b3d14d0569 --- /dev/null +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4/SWord.hs @@ -0,0 +1,664 @@ +------------------------------------------------------------------------ +-- | +-- Module : Verifier.SAW.Simulator.What4.SWord +-- Copyright : Galois, Inc. 2018 +-- License : BSD3 +-- Maintainer : sweirich@galois.com +-- Stability : experimental +-- Portability : non-portable (language extensions) +-- +-- A wrapper for What4 bitvectors so that the width is not tracked +-- statically. +-- This library is intended for use as a backend for saw-core. Therefore +-- it does not wrap all of the bitvector operations from the What4.Interface. +------------------------------------------------------------------------ + +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DoAndIfThenElse #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE PartialTypeSignatures #-} + +-- To allow implicitly provided nats +{-# LANGUAGE AllowAmbiguousTypes #-} + + +-- TODO: module exports? +module Verifier.SAW.Simulator.What4.SWord where + + +-- TODO: improve treatment of partiality. Currently, dynamic +-- failures (e.g. due to failing width checks) use 'fail' from +-- the IO monad. Perhaps this is what we want, as the saw-core +-- code should come in type checked. + +-- Question: Why do the functions in What4.Interface take +-- NatRepr's as arguments instead of implicit KnownNats ? +-- We then could use TypeApplications instead of constructing +-- reprs. +-- Overall, the operations below are a bit random about whether they +-- require an implicit or explicit type argument. + +import Data.Vector (Vector) +import qualified Data.Vector as V +import Numeric.Natural +import qualified Text.PrettyPrint.ANSI.Leijen as PP + +import GHC.TypeNats + +import qualified Data.BitVector.Sized as BV +import Data.Parameterized.NatRepr +import Data.Parameterized.Some(Some(..)) +import Verifier.SAW.Simulator.What4.PosNat + +import What4.Interface(SymBV,Pred,SymInteger,IsExpr,SymExpr,IsExprBuilder) +import qualified What4.Interface as W + + +------------------------------------------------------------- +-- +-- | A What4 symbolic bitvector where the size does not appear in the type +data SWord sym where + + DBV :: (IsExpr (SymExpr sym), KnownNat w, 1<=w) => SymBV sym w -> SWord sym + -- a bit-vector with positive length + + ZBV :: SWord sym + -- a zero-length bit vector. i.e. 0 + + +instance Show (SWord sym) where + show (DBV bv) = show $ W.printSymExpr bv + show ZBV = "0:[0]" + +------------------------------------------------------------- + +-- | Return the signed value if this is a constant bitvector +bvAsSignedInteger :: forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer +bvAsSignedInteger ZBV = Just 0 +bvAsSignedInteger (DBV (bv :: SymBV sym w)) = + BV.asSigned (W.bvWidth bv) <$> W.asBV bv + +-- | Return the unsigned value if this is a constant bitvector +bvAsUnsignedInteger :: forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer +bvAsUnsignedInteger ZBV = Just 0 +bvAsUnsignedInteger (DBV (bv :: SymBV sym w)) = + BV.asUnsigned <$> W.asBV bv + +-- | Convert an integer to an unsigned bitvector. +-- Result is undefined if integer is outside of range. +integerToBV :: forall sym width. (Integral width, IsExprBuilder sym) => + sym -> SymInteger sym -> width -> IO (SWord sym) +integerToBV sym i w + | Just (Some (PosNat wr)) <- somePosNat w + = DBV <$> W.integerToBV sym i wr + | 0 == toInteger w + = return ZBV + | otherwise + = fail "integerToBV: invalid arg" + +-- | Interpret the bit-vector as an unsigned integer +bvToInteger :: forall sym. (IsExprBuilder sym) => + sym -> SWord sym -> IO (SymInteger sym) +bvToInteger sym ZBV = W.intLit sym 0 +bvToInteger sym (DBV bv) = W.bvToInteger sym bv + +-- | Interpret the bit-vector as a signed integer +sbvToInteger :: forall sym. (IsExprBuilder sym) => + sym -> SWord sym -> IO (SymInteger sym) +sbvToInteger sym ZBV = W.intLit sym 0 +sbvToInteger sym (DBV bv) = W.sbvToInteger sym bv + + +-- | Get the width of a bitvector +intSizeOf :: forall sym. SWord sym -> Int +intSizeOf (DBV (_ :: SymBV sym w)) = + fromIntegral (natValue (knownNat @w)) +intSizeOf ZBV = 0 + +-- | Get the width of a bitvector +bvWidth :: SWord sym -> Int +bvWidth = intSizeOf + +-- | Create a bitvector with the given width and value +bvLit :: forall sym. IsExprBuilder sym => + sym -> Int -> Integer -> IO (SWord sym) +bvLit _ w _ + | w == 0 + = return ZBV +bvLit sym w dat + | Just (Some (PosNat rw)) <- somePosNat w + = DBV <$> W.bvLit sym rw (BV.mkBV rw dat) + | otherwise + = fail "bvLit: size of bitvector is < 0 or >= maxInt" + +-- | Returns true if the corresponding bit in the bitvector is set. +bvAt :: forall sym. IsExprBuilder sym => sym + -> SWord sym + -> Int -- ^ Index of bit (0 is the most significant bit) + -> IO (Pred sym) +bvAt sym (DBV (bv :: SymBV sym w)) i = do + let w = natValue (knownNat @w) + let idx = w - 1 - fromIntegral i + W.testBitBV sym idx bv +bvAt _ ZBV _ = fail "cannot index into empty bitvector" + -- TODO: or could return 0? + +-- | Concatenate two bitvectors. +bvJoin :: forall sym. IsExprBuilder sym => sym + -> SWord sym + -- ^ most significant bits + -> SWord sym + -- ^ least significant bits + -> IO (SWord sym) +bvJoin _ x ZBV = return x +bvJoin _ ZBV x = return x +bvJoin sym (DBV (bv1 :: SymBV sym w1)) (DBV (bv2 :: SymBV sym w2)) + | PosNat _ <- addPosNat @w1 @w2 + = DBV <$> W.bvConcat sym bv1 bv2 + +-- | Select a subsequence from a bitvector. +-- idx = w - (m + n) +-- This fails if idx + n is >= w +bvSlice :: forall sym. IsExprBuilder sym => sym + -> Int + -- ^ Starting index, from 0 as most significant bit + -> Int + -- ^ Number of bits to take (must be > 0) + -> SWord sym -> IO (SWord sym) +bvSlice sym m n (DBV (bv :: SymBV sym w)) + | Just (Some (PosNat nr)) <- somePosNat n, + Just (Some mr) <- someNat m, + let wr = knownNat @w, + Just LeqProof <- testLeq (addNat mr nr) wr, + let idx = subNat wr (addNat mr nr), + Just LeqProof <- testLeq (addNat idx nr) wr + = DBV <$> W.bvSelect sym idx nr bv + | otherwise + = fail $ + "invalid arguments to slice: " ++ show m ++ " " ++ show n + ++ " from vector of length " ++ show (knownNat @w) +bvSlice _ _ _ ZBV = return ZBV + +-- | Ceiling (log_2 x) +-- adapted from saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs +w_bvLg2 :: forall sym w. (IsExprBuilder sym, KnownNat w, 1 <= w) => + sym -> SymBV sym w -> IO (SymBV sym w) +w_bvLg2 sym x = go 0 + where + size :: Integer + size = intValue (knownNat @w) + lit :: Integer -> IO (SymBV sym w) + lit n = W.bvLit sym (knownNat @w) (BV.mkBV knownNat n) + go :: Integer -> IO (SymBV sym w) + go i | i < size = do + x' <- lit (2 ^ i) + b' <- W.bvUle sym x x' + th <- lit i + el <- go (i + 1) + W.bvIte sym b' th el + | otherwise = lit i + +-- | If-then-else applied to bitvectors. +bvIte :: forall sym. IsExprBuilder sym => + sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym) +bvIte _ _ ZBV ZBV + = return ZBV +bvIte sym p (DBV (bv1 :: SymBV sym w1)) (DBV (bv2 :: SymBV sym w2)) + | Just Refl <- testEquality (knownNat @w1) (knownNat @w2) + = DBV <$> W.bvIte sym p bv1 bv2 +bvIte _ _ _ _ + = fail "bit-vectors don't have same length" + + +---------------------------------------------------------------------- +-- Convert to/from Vectors +---------------------------------------------------------------------- + +-- | for debugging +showVec :: forall sym. (W.IsExpr (W.SymExpr sym)) => Vector (Pred sym) -> String +showVec vec = + show (PP.list (V.toList (V.map W.printSymExpr vec))) + +-- | explode a bitvector into a vector of booleans +bvUnpack :: forall sym. IsExprBuilder sym => + sym -> SWord sym -> IO (Vector (Pred sym)) +bvUnpack _ ZBV = return V.empty +bvUnpack sym (DBV (bv :: SymBV sym w)) = do + let w :: Natural + w = natValue (knownNat @w) + V.generateM (fromIntegral w) + (\i -> W.testBitBV sym (w - 1 - fromIntegral i) bv) + +-- | convert a vector of booleans to a bitvector +bvPack :: forall sym. (W.IsExpr (W.SymExpr sym), IsExprBuilder sym) => + sym -> Vector (Pred sym) -> IO (SWord sym) +bvPack sym vec = do + vec' <- V.mapM (\p -> do + v1 <- bvLit sym 1 1 + v2 <- bvLit sym 1 0 + bvIte sym p v1 v2) vec + V.foldM (\x y -> bvJoin sym x y) ZBV vec' + +---------------------------------------------------------------------- +-- Generic wrapper for unary operators +---------------------------------------------------------------------- + +-- | Type of unary operation on bitvectors +type SWordUn = + forall sym. IsExprBuilder sym => + sym -> SWord sym -> IO (SWord sym) + +-- | Convert a unary operation on length indexed bvs to a unary operation +-- on `SWord` +bvUn :: forall sym. IsExprBuilder sym => + (forall w. (KnownNat w, 1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w)) -> + sym -> SWord sym -> IO (SWord sym) +bvUn f sym (DBV (bv :: SymBV sym w)) = DBV <$> f sym bv +bvUn _ _ ZBV = return ZBV + +---------------------------------------------------------------------- +-- Generic wrapper for binary operators that take two words +-- of the same length +---------------------------------------------------------------------- + +-- | type of binary operation that returns a bitvector +type SWordBin = + forall sym. IsExprBuilder sym => + sym -> SWord sym -> SWord sym -> IO (SWord sym) +-- | type of binary operation that returns a boolean +type PredBin = + forall sym. IsExprBuilder sym => + sym -> SWord sym -> SWord sym -> IO (Pred sym) + + +-- | convert binary operations that return bitvectors +bvBin :: forall sym. IsExprBuilder sym => + (forall w. 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)) -> + sym -> SWord sym -> SWord sym -> IO (SWord sym) +bvBin f sym (DBV (bv1 :: SymBV sym w1)) (DBV (bv2 :: SymBV sym w2)) + | Just Refl <- testEquality (knownNat @w1) (knownNat @w2) + = DBV <$> f sym bv1 bv2 +bvBin _ _ ZBV ZBV + = return ZBV +bvBin _ _ _ _ + = fail "bit vectors must have same length" + + +-- | convert binary operations that return booleans (Pred) +bvBinPred :: forall sym. IsExprBuilder sym => + (forall w. 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)) -> + sym -> SWord sym -> SWord sym -> IO (Pred sym) +bvBinPred f sym (DBV (bv1:: SymBV sym w1)) (DBV (bv2 :: SymBV sym w2)) + | Just Refl <- testEquality (knownNat @w1) (knownNat @w2) + = f sym bv1 bv2 + | otherwise + = fail $ "bit vectors must have same length" ++ show (knownNat @w1) ++ " " ++ show (knownNat @w2) +bvBinPred _ _ ZBV ZBV + = fail "no zero-length bit vectors here" +bvBinPred _ _ _ _ + = fail $ "bit vectors must have same length" + + + + -- Bitvector logical + +-- | Bitwise complement +bvNot :: SWordUn +bvNot = bvUn W.bvNotBits + +-- | Bitwise logical and. +bvAnd :: SWordBin +bvAnd = bvBin W.bvAndBits + +-- | Bitwise logical or. +bvOr :: SWordBin +bvOr = bvBin W.bvOrBits + +-- | Bitwise logical exclusive or. +bvXor :: SWordBin +bvXor = bvBin W.bvXorBits + + -- Bitvector arithmetic + +-- | 2's complement negation. +bvNeg :: SWordUn +bvNeg = bvUn W.bvNeg + +-- | Add two bitvectors. +bvAdd :: SWordBin +bvAdd = bvBin W.bvAdd + +-- | Subtract one bitvector from another. +bvSub :: SWordBin +bvSub = bvBin W.bvSub + +-- | Multiply one bitvector by another. +bvMul :: SWordBin +bvMul = bvBin W.bvMul + + +bvPopcount :: SWordUn +bvPopcount = bvUn W.bvPopcount + +bvCountLeadingZeros :: SWordUn +bvCountLeadingZeros = bvUn W.bvCountLeadingZeros + +bvCountTrailingZeros :: SWordUn +bvCountTrailingZeros = bvUn W.bvCountTrailingZeros + +bvForall :: W.IsSymExprBuilder sym => + sym -> Natural -> (SWord sym -> IO (Pred sym)) -> IO (Pred sym) +bvForall sym n f = + case W.userSymbol "i" of + Left err -> fail $ show err + Right indexSymbol -> + case mkNatRepr n of + Some w + | Just LeqProof <- testLeq (knownNat @1) w -> + withKnownNat w $ do + i <- W.freshBoundVar sym indexSymbol $ W.BaseBVRepr w + body <- f . DBV $ W.varExpr sym i + W.forallPred sym i body + | otherwise -> f ZBV + +-- | Unsigned bitvector division. +-- +-- The result is undefined when @y@ is zero, +-- but is otherwise equal to @floor( x / y )@. +bvUDiv :: SWordBin +bvUDiv = bvBin W.bvUdiv + + +-- | Unsigned bitvector remainder. +-- +-- The result is undefined when @y@ is zero, +-- but is otherwise equal to @x - (bvUdiv x y) * y@. +bvURem :: SWordBin +bvURem = bvBin W.bvUrem + +-- | Signed bitvector division. The result is truncated to zero. +-- +-- The result of @bvSdiv x y@ is undefined when @y@ is zero, +-- but is equal to @floor(x/y)@ when @x@ and @y@ have the same sign, +-- and equal to @ceiling(x/y)@ when @x@ and @y@ have opposite signs. +-- +-- NOTE! However, that there is a corner case when dividing @MIN_INT@ by +-- @-1@, in which case an overflow condition occurs, and the result is instead +-- @MIN_INT@. +bvSDiv :: SWordBin +bvSDiv = bvBin W.bvSdiv + +-- | Signed bitvector remainder. +-- +-- The result of @bvSrem x y@ is undefined when @y@ is zero, but is +-- otherwise equal to @x - (bvSdiv x y) * y@. +bvSRem :: SWordBin +bvSRem = bvBin W.bvSrem + +bvLg2 :: SWordUn +bvLg2 = bvUn w_bvLg2 + + -- Bitvector comparisons + +-- | Return true if bitvectors are equal. +bvEq :: PredBin +bvEq = bvBinPred W.bvEq + +-- | Signed less-than-or-equal. +bvsle :: PredBin +bvsle = bvBinPred W.bvSle + +-- | Signed less-than. +bvslt :: PredBin +bvslt = bvBinPred W.bvSlt + +-- | Unsigned less-than-or-equal. +bvule :: PredBin +bvule = bvBinPred W.bvUle + +-- | Unsigned less-than. +bvult :: PredBin +bvult = bvBinPred W.bvUlt + +-- | Signed greater-than-or-equal. +bvsge :: PredBin +bvsge = bvBinPred W.bvSge + +-- | Signed greater-than. +bvsgt :: PredBin +bvsgt = bvBinPred W.bvSgt + +-- | Unsigned greater-than-or-equal. +bvuge :: PredBin +bvuge = bvBinPred W.bvUge + +-- | Unsigned greater-than. +bvugt :: PredBin +bvugt = bvBinPred W.bvUgt + +---------------------------------------- +-- Bitvector rotations +---------------------------------------- + +-- | Rotate left by a concrete integer value +bvRolInt :: forall sym. IsExprBuilder sym => sym -> + SWord sym -> Integer -> IO (SWord sym) +bvRolInt sym (DBV (bv :: SymBV sym w)) i = do + i' <- W.intLit sym i + DBV <$> bvRotateL' sym bv i' +bvRolInt _sym ZBV _i = return ZBV + +-- | Rotate right by a concrete integer value +bvRorInt :: forall sym. IsExprBuilder sym => sym -> + SWord sym -> Integer -> IO (SWord sym) +bvRorInt sym (DBV (bv :: SymBV sym w)) i = do + i' <- W.intLit sym i + DBV <$> bvRotateR' sym bv i' +bvRorInt _sym ZBV _i = return ZBV + +-- | Rotate left by a symbolic bitvector +-- +-- The two bitvectors do not need to be the same length +bvRol :: forall sym. IsExprBuilder sym => sym -> + SWord sym -> SWord sym -> IO (SWord sym) +bvRol sym (DBV (bv :: SymBV sym w1)) (DBV (i :: SymBV sym w2)) = do + i' <- W.bvToInteger sym i + DBV <$> bvRotateL' sym bv i' +bvRol _sym ZBV _i = return ZBV +bvRol _sym (DBV bv) ZBV = return $ DBV bv + +-- | Rotate right by a symbolic bitvector +-- +-- The two bitvectors do not need to be the same length +bvRor :: forall sym. IsExprBuilder sym => sym -> + SWord sym -> SWord sym -> IO (SWord sym) +bvRor sym (DBV (bv :: SymBV sym w1)) (DBV (i :: SymBV sym w2)) = do + i' <- W.bvToInteger sym i + DBV <$> bvRotateR' sym bv i' +bvRor _sym ZBV _i = return ZBV +bvRor _sym (DBV bv) ZBV = return $ DBV bv + +-- | Worker function for left rotations +-- +-- Defined from the concrete implementation +-- +-- bvRotateL (BV w x) i = Prim.bv w ((x `shiftL` j) .|. (x `shiftR` (w - j))) +-- where j = fromInteger (i `mod` toInteger w) +bvRotateL' :: forall sym w1. (KnownNat w1, IsExprBuilder sym, 1 <= w1) => sym -> + SymBV sym w1 -> SymInteger sym -> IO (SymBV sym w1) +bvRotateL' sym x i' = do + + w' <- W.intLit sym w + + j <- W.intMod sym i' w' + + jj <- W.integerToBV sym j (knownNat @w1) + + x1 <- bvShiftL sym pfalse x jj + + wmj <- W.intSub sym w' j + wmjj <- W.integerToBV sym wmj (knownNat @w1) + + x2 <- bvShiftR sym (W.bvLshr sym) pfalse x wmjj + W.bvOrBits sym x1 x2 + where + pfalse :: Pred sym + pfalse = W.falsePred sym + + w = intValue (knownNat @w1) + +-- | Worker function for right rotations +-- +-- Defined from the concrete implementation +bvRotateR' :: forall sym w1. (KnownNat w1, IsExprBuilder sym, 1 <= w1) => sym -> + SymBV sym w1 -> SymInteger sym -> IO (SymBV sym w1) +bvRotateR' sym x i = do + ii <- W.intNeg sym i + bvRotateL' sym x ii +---------------------------------------- +-- Bitvector shifts (prims) +---------------------------------------- + +-- | logical shift left, amount specified by concrete integer +bvShlInt :: forall sym. IsExprBuilder sym => sym -> + Pred sym -> SWord sym -> Integer -> IO (SWord sym) +bvShlInt sym p (DBV (bv :: SymBV sym w)) x + = DBV <$> bvShl' sym (knownNat @w) p bv x +bvShlInt _ _ ZBV _ + = return ZBV + +-- | logical (unsigned) shift right, specified by concrete integer +bvShrInt :: forall sym. IsExprBuilder sym => sym -> + Pred sym -> SWord sym -> Integer -> IO (SWord sym) +bvShrInt sym p (DBV (bv :: SymBV sym w)) x + = DBV <$> bvShr' sym (W.bvLshr sym) (knownNat @w) p bv x +bvShrInt _ _ ZBV _ + = return ZBV + +-- | arithmetic (signed) shift right +bvSShrInt :: forall sym. IsExprBuilder sym => sym -> + Pred sym -> SWord sym -> Integer -> IO (SWord sym) +bvSShrInt sym p (DBV (bv :: SymBV sym w)) x + = DBV <$> bvShr' sym (W.bvAshr sym) (knownNat @w) p bv x +bvSShrInt _ _ ZBV _ + = return ZBV + + +-- | logical shift left, amount specified by (symbolic) bitvector +bvShl :: forall sym. IsExprBuilder sym => sym + -> Pred sym + -> SWord sym + -- ^ shift this + -> SWord sym + -- ^ amount to shift by + -> IO (SWord sym) +bvShl sym p (DBV (bv1 :: SymBV sym w1)) (DBV (bv2 :: SymBV sym w2)) + | Just Refl <- testEquality (knownNat @w1) (knownNat @w2) + = DBV <$> bvShiftL sym p bv1 bv2 + -- amount to shift by is smaller + | Just LeqProof <- testLeq (addNat (knownNat @w2) (knownNat @1)) (knownNat @w1) + = do bv2' <- W.bvZext sym (knownNat @w1) bv2 + DBV <$> bvShiftL sym p bv1 bv2' + | otherwise + = fail $ "bvShl: bit vectors must have same length " + ++ show (knownNat @w1) ++ " " ++ show (knownNat @w2) +bvShl _ _ ZBV ZBV + = return ZBV +bvShl _ _ _ _ + = fail $ "bvShl: bitvectors do not have the same length" + + +-- | logical shift right +bvShr :: forall sym. IsExprBuilder sym => sym -> + Pred sym -> SWord sym -> SWord sym -> IO (SWord sym) +bvShr sym p (DBV (bv1 :: SymBV sym w1)) (DBV (bv2 :: SymBV sym w2)) + | Just Refl <- testEquality (knownNat @w1) (knownNat @w2) + = DBV <$> bvShiftR sym (W.bvLshr sym) p bv1 bv2 + | Just LeqProof <- testLeq (addNat (knownNat @w2) (knownNat @1)) (knownNat @w1) + = do bv2' <- W.bvZext sym (knownNat @w1) bv2 + DBV <$> bvShiftR sym (W.bvLshr sym) p bv1 bv2' + | otherwise + = fail $ "bvShr: bitvectors do not have the same length " + ++ show (knownNat @w1) ++ " " ++ show (knownNat @w2) +bvShr _ _ ZBV ZBV + = return ZBV +bvShr _ _ _ _ + = fail $ "bvShr: bitvectors do not have the same length" + + +-- | arithmetic shift right +bvSShr :: forall sym. IsExprBuilder sym => sym -> + Pred sym -> SWord sym -> SWord sym -> IO (SWord sym) +bvSShr sym p (DBV (bv1 :: SymBV sym w1)) (DBV (bv2 :: SymBV sym w2)) + | Just Refl <- testEquality (knownNat @w1) (knownNat @w2) + = DBV <$> bvShiftR sym (W.bvAshr sym) p bv1 bv2 + | Just LeqProof <- testLeq (addNat (knownNat @w2) (knownNat @1)) (knownNat @w1) + = do bv2' <- W.bvSext sym (knownNat @w1) bv2 + DBV <$> bvShiftR sym (W.bvAshr sym) p bv1 bv2' + | otherwise + = fail $ "bvSShr: bitvectors do not have the same length: " + ++ show (knownNat @w1) ++ " " ++ show (knownNat @w2) +bvSShr _ _ ZBV ZBV + = return ZBV +bvSShr _ _ _ _ + = fail $ "bvSShr: bitvectors do not have the same length: " + + +---------------------------------------- +-- Shift operations +---------------------------------------- + +-- If the predicate is true, invert the bitvector, shift then +-- invert again. (Following SBV definition). This means that +-- the predicate controls whether the newly added bit is a one +-- or a zero. + +bvShiftL :: forall sym w. (IsExprBuilder sym, 1 <= w) => sym -> + Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) +bvShiftL sym b x j = do + nx <- W.bvNotBits sym x + snx <- W.bvShl sym nx j + nsnx <- W.bvNotBits sym snx + W.bvIte sym b nsnx =<< W.bvShl sym x j + +bvShl' :: (IsExprBuilder sym, 1 <= w) => sym -> + NatRepr w -> Pred sym -> SymBV sym w -> Integer -> IO (SymBV sym w) +bvShl' sym rep b x i = do + -- what if i is too big for rep bits? + j <- W.bvLit sym rep (BV.mkBV rep i) + bvShiftL sym b x j + + +-- The shr argument should be W.bvAshr or W.bvLshr, depending +-- on whether to use arithmetic or logical shift right + +bvShiftR :: forall sym w. (IsExprBuilder sym, 1 <= w) => sym -> + (SymBV sym w -> SymBV sym w -> IO (SymBV sym w)) -> + Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) +bvShiftR sym shr b x j = do + nx <- W.bvNotBits sym x + snx <- shr nx j + nsnx <- W.bvNotBits sym snx + W.bvIte sym b nsnx =<< shr x j + +bvShr' :: (IsExprBuilder sym, 1 <= w) => sym -> + (SymBV sym w -> SymBV sym w -> IO (SymBV sym w)) -> + NatRepr w -> Pred sym -> SymBV sym w -> Integer -> IO (SymBV sym w) +bvShr' sym shr rep b x i = do + j <- W.bvLit sym rep (BV.mkBV rep i) + bvShiftR sym shr b x j diff --git a/.gitignore b/saw-core/.gitignore similarity index 100% rename from .gitignore rename to saw-core/.gitignore diff --git a/saw-core/LICENSE b/saw-core/LICENSE new file mode 100644 index 0000000000..9e2f031c53 --- /dev/null +++ b/saw-core/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2012-2016, Galois, Inc. + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the names of the authors nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/saw-core/README.md b/saw-core/README.md new file mode 100644 index 0000000000..8d72ded885 --- /dev/null +++ b/saw-core/README.md @@ -0,0 +1,10 @@ +This repository contains the code for SAWCore, an intermediate +language for representing the semantics of software (and potentially +hardware). It provides support for constructing models in a +dependently-typed lambda-calculus, transforming those models using a +rewriting engine, concretely or symbolically interpreting those +models, and emitting them as input to various external theorem +provers. + +Currently, the library supports generating AIG, CNF, and SMT-Lib +output. diff --git a/saw-core/Setup.hs b/saw-core/Setup.hs new file mode 100644 index 0000000000..9a994af677 --- /dev/null +++ b/saw-core/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/doc/Makefile b/saw-core/doc/Makefile similarity index 100% rename from doc/Makefile rename to saw-core/doc/Makefile diff --git a/doc/formal.tex b/saw-core/doc/formal.tex similarity index 100% rename from doc/formal.tex rename to saw-core/doc/formal.tex diff --git a/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore similarity index 100% rename from prelude/Prelude.sawcore rename to saw-core/prelude/Prelude.sawcore diff --git a/saw-core.cabal b/saw-core/saw-core.cabal similarity index 100% rename from saw-core.cabal rename to saw-core/saw-core.cabal diff --git a/src/Verifier/SAW.hs b/saw-core/src/Verifier/SAW.hs similarity index 100% rename from src/Verifier/SAW.hs rename to saw-core/src/Verifier/SAW.hs diff --git a/src/Verifier/SAW/Cache.hs b/saw-core/src/Verifier/SAW/Cache.hs similarity index 100% rename from src/Verifier/SAW/Cache.hs rename to saw-core/src/Verifier/SAW/Cache.hs diff --git a/src/Verifier/SAW/Change.hs b/saw-core/src/Verifier/SAW/Change.hs similarity index 100% rename from src/Verifier/SAW/Change.hs rename to saw-core/src/Verifier/SAW/Change.hs diff --git a/src/Verifier/SAW/Constant.hs b/saw-core/src/Verifier/SAW/Constant.hs similarity index 100% rename from src/Verifier/SAW/Constant.hs rename to saw-core/src/Verifier/SAW/Constant.hs diff --git a/src/Verifier/SAW/Conversion.hs b/saw-core/src/Verifier/SAW/Conversion.hs similarity index 100% rename from src/Verifier/SAW/Conversion.hs rename to saw-core/src/Verifier/SAW/Conversion.hs diff --git a/src/Verifier/SAW/ExternalFormat.hs b/saw-core/src/Verifier/SAW/ExternalFormat.hs similarity index 100% rename from src/Verifier/SAW/ExternalFormat.hs rename to saw-core/src/Verifier/SAW/ExternalFormat.hs diff --git a/src/Verifier/SAW/FiniteValue.hs b/saw-core/src/Verifier/SAW/FiniteValue.hs similarity index 100% rename from src/Verifier/SAW/FiniteValue.hs rename to saw-core/src/Verifier/SAW/FiniteValue.hs diff --git a/src/Verifier/SAW/Grammar.y b/saw-core/src/Verifier/SAW/Grammar.y similarity index 100% rename from src/Verifier/SAW/Grammar.y rename to saw-core/src/Verifier/SAW/Grammar.y diff --git a/src/Verifier/SAW/Lexer.x b/saw-core/src/Verifier/SAW/Lexer.x similarity index 100% rename from src/Verifier/SAW/Lexer.x rename to saw-core/src/Verifier/SAW/Lexer.x diff --git a/src/Verifier/SAW/Module.hs b/saw-core/src/Verifier/SAW/Module.hs similarity index 100% rename from src/Verifier/SAW/Module.hs rename to saw-core/src/Verifier/SAW/Module.hs diff --git a/src/Verifier/SAW/OpenTerm.hs b/saw-core/src/Verifier/SAW/OpenTerm.hs similarity index 100% rename from src/Verifier/SAW/OpenTerm.hs rename to saw-core/src/Verifier/SAW/OpenTerm.hs diff --git a/src/Verifier/SAW/ParserUtils.hs b/saw-core/src/Verifier/SAW/ParserUtils.hs similarity index 100% rename from src/Verifier/SAW/ParserUtils.hs rename to saw-core/src/Verifier/SAW/ParserUtils.hs diff --git a/src/Verifier/SAW/Position.hs b/saw-core/src/Verifier/SAW/Position.hs similarity index 100% rename from src/Verifier/SAW/Position.hs rename to saw-core/src/Verifier/SAW/Position.hs diff --git a/src/Verifier/SAW/Prelude.hs b/saw-core/src/Verifier/SAW/Prelude.hs similarity index 100% rename from src/Verifier/SAW/Prelude.hs rename to saw-core/src/Verifier/SAW/Prelude.hs diff --git a/src/Verifier/SAW/Prelude/Constants.hs b/saw-core/src/Verifier/SAW/Prelude/Constants.hs similarity index 100% rename from src/Verifier/SAW/Prelude/Constants.hs rename to saw-core/src/Verifier/SAW/Prelude/Constants.hs diff --git a/src/Verifier/SAW/Prim.hs b/saw-core/src/Verifier/SAW/Prim.hs similarity index 100% rename from src/Verifier/SAW/Prim.hs rename to saw-core/src/Verifier/SAW/Prim.hs diff --git a/src/Verifier/SAW/Recognizer.hs b/saw-core/src/Verifier/SAW/Recognizer.hs similarity index 100% rename from src/Verifier/SAW/Recognizer.hs rename to saw-core/src/Verifier/SAW/Recognizer.hs diff --git a/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs similarity index 100% rename from src/Verifier/SAW/Rewriter.hs rename to saw-core/src/Verifier/SAW/Rewriter.hs diff --git a/src/Verifier/SAW/SCTypeCheck.hs b/saw-core/src/Verifier/SAW/SCTypeCheck.hs similarity index 100% rename from src/Verifier/SAW/SCTypeCheck.hs rename to saw-core/src/Verifier/SAW/SCTypeCheck.hs diff --git a/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs similarity index 100% rename from src/Verifier/SAW/SharedTerm.hs rename to saw-core/src/Verifier/SAW/SharedTerm.hs diff --git a/src/Verifier/SAW/Simulator.hs b/saw-core/src/Verifier/SAW/Simulator.hs similarity index 100% rename from src/Verifier/SAW/Simulator.hs rename to saw-core/src/Verifier/SAW/Simulator.hs diff --git a/src/Verifier/SAW/Simulator/Concrete.hs b/saw-core/src/Verifier/SAW/Simulator/Concrete.hs similarity index 100% rename from src/Verifier/SAW/Simulator/Concrete.hs rename to saw-core/src/Verifier/SAW/Simulator/Concrete.hs diff --git a/src/Verifier/SAW/Simulator/MonadLazy.hs b/saw-core/src/Verifier/SAW/Simulator/MonadLazy.hs similarity index 100% rename from src/Verifier/SAW/Simulator/MonadLazy.hs rename to saw-core/src/Verifier/SAW/Simulator/MonadLazy.hs diff --git a/src/Verifier/SAW/Simulator/Prims.hs b/saw-core/src/Verifier/SAW/Simulator/Prims.hs similarity index 100% rename from src/Verifier/SAW/Simulator/Prims.hs rename to saw-core/src/Verifier/SAW/Simulator/Prims.hs diff --git a/src/Verifier/SAW/Simulator/RME.hs b/saw-core/src/Verifier/SAW/Simulator/RME.hs similarity index 100% rename from src/Verifier/SAW/Simulator/RME.hs rename to saw-core/src/Verifier/SAW/Simulator/RME.hs diff --git a/src/Verifier/SAW/Simulator/RME/Base.hs b/saw-core/src/Verifier/SAW/Simulator/RME/Base.hs similarity index 100% rename from src/Verifier/SAW/Simulator/RME/Base.hs rename to saw-core/src/Verifier/SAW/Simulator/RME/Base.hs diff --git a/src/Verifier/SAW/Simulator/RME/Vector.hs b/saw-core/src/Verifier/SAW/Simulator/RME/Vector.hs similarity index 100% rename from src/Verifier/SAW/Simulator/RME/Vector.hs rename to saw-core/src/Verifier/SAW/Simulator/RME/Vector.hs diff --git a/src/Verifier/SAW/Simulator/Value.hs b/saw-core/src/Verifier/SAW/Simulator/Value.hs similarity index 100% rename from src/Verifier/SAW/Simulator/Value.hs rename to saw-core/src/Verifier/SAW/Simulator/Value.hs diff --git a/src/Verifier/SAW/Term/CtxTerm.hs b/saw-core/src/Verifier/SAW/Term/CtxTerm.hs similarity index 100% rename from src/Verifier/SAW/Term/CtxTerm.hs rename to saw-core/src/Verifier/SAW/Term/CtxTerm.hs diff --git a/src/Verifier/SAW/Term/Functor.hs b/saw-core/src/Verifier/SAW/Term/Functor.hs similarity index 100% rename from src/Verifier/SAW/Term/Functor.hs rename to saw-core/src/Verifier/SAW/Term/Functor.hs diff --git a/src/Verifier/SAW/Term/Pretty.hs b/saw-core/src/Verifier/SAW/Term/Pretty.hs similarity index 100% rename from src/Verifier/SAW/Term/Pretty.hs rename to saw-core/src/Verifier/SAW/Term/Pretty.hs diff --git a/src/Verifier/SAW/TermNet.hs b/saw-core/src/Verifier/SAW/TermNet.hs similarity index 100% rename from src/Verifier/SAW/TermNet.hs rename to saw-core/src/Verifier/SAW/TermNet.hs diff --git a/src/Verifier/SAW/Testing/Random.hs b/saw-core/src/Verifier/SAW/Testing/Random.hs similarity index 100% rename from src/Verifier/SAW/Testing/Random.hs rename to saw-core/src/Verifier/SAW/Testing/Random.hs diff --git a/src/Verifier/SAW/Typechecker.hs b/saw-core/src/Verifier/SAW/Typechecker.hs similarity index 100% rename from src/Verifier/SAW/Typechecker.hs rename to saw-core/src/Verifier/SAW/Typechecker.hs diff --git a/src/Verifier/SAW/TypedAST.hs b/saw-core/src/Verifier/SAW/TypedAST.hs similarity index 100% rename from src/Verifier/SAW/TypedAST.hs rename to saw-core/src/Verifier/SAW/TypedAST.hs diff --git a/src/Verifier/SAW/UnionFind.hs b/saw-core/src/Verifier/SAW/UnionFind.hs similarity index 100% rename from src/Verifier/SAW/UnionFind.hs rename to saw-core/src/Verifier/SAW/UnionFind.hs diff --git a/src/Verifier/SAW/Unique.hs b/saw-core/src/Verifier/SAW/Unique.hs similarity index 100% rename from src/Verifier/SAW/Unique.hs rename to saw-core/src/Verifier/SAW/Unique.hs diff --git a/src/Verifier/SAW/UntypedAST.hs b/saw-core/src/Verifier/SAW/UntypedAST.hs similarity index 100% rename from src/Verifier/SAW/UntypedAST.hs rename to saw-core/src/Verifier/SAW/UntypedAST.hs diff --git a/src/Verifier/SAW/Utils.hs b/saw-core/src/Verifier/SAW/Utils.hs similarity index 100% rename from src/Verifier/SAW/Utils.hs rename to saw-core/src/Verifier/SAW/Utils.hs diff --git a/tests/src/Tests.hs b/saw-core/tests/src/Tests.hs similarity index 100% rename from tests/src/Tests.hs rename to saw-core/tests/src/Tests.hs diff --git a/tests/src/Tests/CacheTests.hs b/saw-core/tests/src/Tests/CacheTests.hs similarity index 100% rename from tests/src/Tests/CacheTests.hs rename to saw-core/tests/src/Tests/CacheTests.hs diff --git a/tests/src/Tests/Parser.hs b/saw-core/tests/src/Tests/Parser.hs similarity index 100% rename from tests/src/Tests/Parser.hs rename to saw-core/tests/src/Tests/Parser.hs diff --git a/tests/src/Tests/Rewriter.hs b/saw-core/tests/src/Tests/Rewriter.hs similarity index 100% rename from tests/src/Tests/Rewriter.hs rename to saw-core/tests/src/Tests/Rewriter.hs diff --git a/tests/src/Tests/SharedTerm.hs b/saw-core/tests/src/Tests/SharedTerm.hs similarity index 100% rename from tests/src/Tests/SharedTerm.hs rename to saw-core/tests/src/Tests/SharedTerm.hs diff --git a/tools/extcore-info.hs b/saw-core/tools/extcore-info.hs similarity index 100% rename from tools/extcore-info.hs rename to saw-core/tools/extcore-info.hs