diff --git a/.gitmodules b/.gitmodules index 7b798103f..743a61f25 100644 --- a/.gitmodules +++ b/.gitmodules @@ -52,3 +52,15 @@ [submodule "deps/mir-json"] path = deps/mir-json url = https://github.com/GaloisInc/mir-json.git +[submodule "deps/asl-translator"] + path = deps/asl-translator + url = https://github.com/GaloisInc/asl-translator +[submodule "deps/arm-asl-parser"] + path = deps/arm-asl-parser + url = https://github.com/GaloisInc/arm-asl-parser +[submodule "deps/dismantle"] + path = deps/dismantle + url = https://github.com/travitch/dismantle +[submodule "deps/semmc"] + path = deps/semmc + url = https://github.com/GaloisInc/semmc diff --git a/cabal.project b/cabal.project index 220f25b1c..c3d514563 100644 --- a/cabal.project +++ b/cabal.project @@ -35,13 +35,24 @@ packages: deps/flexdis86/binary-symbols deps/lmdb/lmdb deps/lmdb/lmdb-simple + deps/asl-translator + deps/arm-asl-parser + deps/dismantle/dismantle-tablegen + deps/dismantle/dismantle-arm-xml + deps/semmc/semmc + deps/semmc/semmc-synthesis + deps/semmc/semmc-aarch32 deps/macaw/base deps/macaw/macaw-dump deps/macaw/macaw-loader + deps/macaw/macaw-loader-aarch32 deps/macaw/macaw-loader-x86 deps/macaw/symbolic deps/macaw/x86 deps/macaw/x86_symbolic + deps/macaw/macaw-semmc + deps/macaw/macaw-aarch32 + deps/macaw/macaw-aarch32-symbolic deps/elf-edit deps/dwarf deps/argo/argo diff --git a/deps/arm-asl-parser b/deps/arm-asl-parser new file mode 160000 index 000000000..4473ebc22 --- /dev/null +++ b/deps/arm-asl-parser @@ -0,0 +1 @@ +Subproject commit 4473ebc229c2ee44ed6cf51e3eedebebce5a4bb7 diff --git a/deps/asl-translator b/deps/asl-translator new file mode 160000 index 000000000..9940a0483 --- /dev/null +++ b/deps/asl-translator @@ -0,0 +1 @@ +Subproject commit 9940a0483f7042c021984281ad5ca5e3b781215e diff --git a/deps/dismantle b/deps/dismantle new file mode 160000 index 000000000..e4ebe05fb --- /dev/null +++ b/deps/dismantle @@ -0,0 +1 @@ +Subproject commit e4ebe05fbce079973e9619198c9eb14dec74fe5f diff --git a/deps/macaw b/deps/macaw index 81570f6d2..898c3d1da 160000 --- a/deps/macaw +++ b/deps/macaw @@ -1 +1 @@ -Subproject commit 81570f6d20c168f76ace608c82770513d4f71aeb +Subproject commit 898c3d1dabe21580c6fb860b464f22ebef4b71b3 diff --git a/deps/semmc b/deps/semmc new file mode 160000 index 000000000..519d70e2a --- /dev/null +++ b/deps/semmc @@ -0,0 +1 @@ +Subproject commit 519d70e2a588a9c69f2d5caa3af31c61a0c5f100 diff --git a/saw-script.cabal b/saw-script.cabal index 2275d502a..8f3b17139 100644 --- a/saw-script.cabal +++ b/saw-script.cabal @@ -79,6 +79,7 @@ library -- packages in git submodules -- (hobbits is for now actually a source-repository-package) , aig + , asl-translator , crucible >= 0.4 , crucible-jvm , crucible-llvm >= 0.2 @@ -95,6 +96,8 @@ library , lmdb-simple , macaw-base , macaw-x86 + , macaw-aarch32 + , macaw-aarch32-symbolic , macaw-symbolic , macaw-x86-symbolic , parameterized-utils @@ -154,6 +157,8 @@ library SAWScript.HeapsterBuiltins + SAWScript.Crucible.CrucibleSAW.SAWCore + SAWScript.Crucible.Common SAWScript.Crucible.Common.MethodSpec SAWScript.Crucible.Common.Override @@ -173,6 +178,7 @@ library SAWScript.Crucible.LLVM.Skeleton SAWScript.Crucible.LLVM.Skeleton.Builtins SAWScript.Crucible.LLVM.X86 + SAWScript.Crucible.LLVM.AArch32 SAWScript.Crucible.JVM.Builtins SAWScript.Crucible.JVM.BuiltinsJVM diff --git a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs new file mode 100644 index 000000000..de409b013 --- /dev/null +++ b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs @@ -0,0 +1,1366 @@ +----------------------------------------------------------------------- +-- | +-- Module : Lang.Crucible.Backend.SAWCore +-- Description : Crucible interface for generating SAWCore +-- Copyright : (c) Galois, Inc 2014-2016 +-- License : BSD3 +-- Maintainer : Rob Dockins +-- Stability : provisional +-- +-- This module provides a Crucible backend that produces SAWCore terms. +------------------------------------------------------------------------ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ViewPatterns #-} + +--module Lang.Crucible.Backend.SAWCore where +module SAWScript.Crucible.CrucibleSAW.SAWCore where + +import Control.Exception ( bracket ) +import Control.Lens +import Control.Monad +import qualified Data.BitVector.Sized as BV +import Data.IORef +import Data.List (elemIndex) +import Data.Foldable (toList) +import Data.IntMap (IntMap) +import qualified Data.IntMap as IntMap +import Data.List.NonEmpty (NonEmpty(..)) +import Data.Map ( Map ) +import qualified Data.Map as Map +import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.Nonce +import Data.Parameterized.Some +import Data.Parameterized.TraversableFC +import Data.Ratio +import Data.Sequence (Seq) +import qualified Data.Sequence as Seq +import Data.Word(Word64) +import qualified Data.Text as Text + +import Numeric.Natural + +import GHC.Stack + +import What4.BaseTypes +import What4.Config +import What4.Interface +import qualified What4.Expr.ArrayUpdateMap as AUM +import qualified What4.Expr.Builder as B +import qualified What4.Expr.BoolMap as BM +import qualified What4.Expr.WeightedSum as WSum +import What4.ProgramLoc +import What4.Protocol.Online +import What4.Protocol.SMTWriter as SMT +import What4.SatResult +import qualified What4.SemiRing as B +import qualified What4.Solver.Yices as Yices +import What4.Symbol + +import Lang.Crucible.Panic(panic) +import Lang.Crucible.Backend +import Lang.Crucible.Backend.Online hiding (withSolverProcess) +import qualified Lang.Crucible.Backend.AssumptionStack as AS +import Lang.Crucible.Simulator.SimError + +import qualified Verifier.SAW.SharedTerm as SC +import qualified Verifier.SAW.TypedAST as SC + +data SAWCruciblePersonality sym = SAWCruciblePersonality + +-- | The SAWCoreBackend is a crucible backend that represents symbolic values +-- as SAWCore terms. +data SAWCoreState solver fs n + = SAWCoreState + { saw_ctx :: SC.SharedContext -- ^ the main SAWCore datastructure for building shared terms + , saw_inputs :: IORef (Seq (SC.ExtCns SC.Term )) + -- ^ a record of all the symbolic input variables created so far, + -- in the order they were created + + , saw_symMap :: !(Map Word64 (SC.SharedContext -> [SC.Term] -> IO SC.Term)) + -- ^ What to do with uninterpreted functions. + -- The key is the "indexValue" of the "symFunId" for the function + + , saw_elt_cache :: B.IdxCache n SAWExpr + -- ^ cache mapping a What4 variable nonce to its corresponding SAWCore term. + + , saw_elt_cache_r :: IORef (IntMap (Some (B.SymExpr (SAWCoreBackend n solver fs)))) + -- ^ reverse cache mapping a SAWCore TermIndex to its corresponding What4 variable. + -- 'saw_elt_cache' and 'saw_elt_cache_r' implement a bidirectional map between + -- SAWCore terms and What4 variables. + + , saw_online_state_maybe :: Maybe (OnlineBackend solver n (SAWCoreState' solver fs) fs) + } + +-- | Wrapper around SAWCoreState that accounts for how the IORef needs +-- to be stuffed into the What4 ExprBuilder. XXX: gross. It looks +-- like the intended model is that the elements of SAWCoreState that +-- need to be mutable should become IORefs instead. +newtype SAWCoreState' solver fs n = SAWCoreState' (IORef (SAWCoreState solver fs n)) + +-- | Accessor to extract the ref +userStateRef :: SAWCoreBackend n solver fs -> IORef (SAWCoreState solver fs n) +userStateRef sym = + let SAWCoreState' ref = sym ^. B.userState in + ref + +data SAWExpr (bt :: BaseType) where + SAWExpr :: !SC.Term -> SAWExpr bt + + -- This is a term that represents an integer, but has an + -- implicit integer-to-real conversion. + IntToRealSAWExpr :: !(SAWExpr BaseIntegerType) -> SAWExpr BaseRealType + -- This is a SAWCore term that represents a natural number, but has an + -- implicit nat-to-integer conversion. + --NatToIntSAWExpr :: !(SAWExpr BaseNatType) -> SAWExpr BaseIntegerType + +type SAWCoreBackend n solver fs = B.ExprBuilder n (SAWCoreState' solver fs) fs + + +-- | Run the given IO action with the given SAW backend. +-- While while running the action, the SAW backend is +-- set up with a fresh naming context. This means that all +-- symbolic inputs, symMap entries, element cache entires, +-- assertions and proof obligations start empty while +-- running the action. After the action completes, the +-- state of these fields is restored. +inFreshNamingContext :: SAWCoreBackend n solver fs -> IO a -> IO a +inFreshNamingContext sym f = + do old <- readIORef (userStateRef sym) + bracket (mkNew (sym ^. B.exprCounter) old) (restore old) action + + where + action new = + do writeIORef (userStateRef sym) new + f + + restore old _new = + do writeIORef (userStateRef sym) old + + mkNew _gen old = + do ch <- B.newIdxCache + ch_r <- newIORef IntMap.empty + iref <- newIORef mempty + let new = SAWCoreState + { saw_ctx = saw_ctx old + , saw_inputs = iref + , saw_symMap = mempty + , saw_elt_cache = ch + , saw_elt_cache_r = ch_r + , saw_online_state_maybe = saw_online_state_maybe old + } + return new + +getInputs :: SAWCoreBackend n solver fs -> IO (Seq (SC.ExtCns SC.Term)) +getInputs sym = + do st <- readIORef (userStateRef sym) + readIORef (saw_inputs st) + +baseSCType :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + BaseTypeRepr tp -> + IO SC.Term +baseSCType sym sc bt = + case bt of + BaseBoolRepr -> SC.scBoolType sc + BaseBVRepr w -> SC.scBitvector sc $ fromIntegral (natValue w) + BaseIntegerRepr -> SC.scIntegerType sc + BaseArrayRepr indexTypes range + | Ctx.Empty Ctx.:> idx_type <- indexTypes -> + do sc_idx_type <- baseSCType sym sc idx_type + sc_elm_type <- baseSCType sym sc range + SC.scArrayType sc sc_idx_type sc_elm_type + | otherwise -> + unsupported sym "SAW backend does not support multidimensional Arrays: baseSCType" + BaseFloatRepr _ -> + unsupported sym "SAW backend does not support IEEE-754 floating point values: baseSCType" + BaseStringRepr _ -> + unsupported sym "SAW backend does not support string values: baseSCType" + BaseComplexRepr -> + unsupported sym "SAW backend does not support complex values: baseSCType" + BaseRealRepr -> + unsupported sym "SAW backend does not support real values: baseSCType" + BaseStructRepr ts -> + SC.scTupleType sc =<< baseSCTypes ts + where + baseSCTypes :: Ctx.Assignment BaseTypeRepr args -> IO [SC.Term] + baseSCTypes Ctx.Empty = return [] + baseSCTypes (xs Ctx.:> x) = + do ts <- baseSCTypes xs + t <- baseSCType sym sc x + return (ts ++ [t]) + +-- | Create a new symbolic variable. +sawCreateVar :: SAWCoreBackend n solver fs + -> Text.Text -- ^ the name of the variable + -> SC.Term + -> IO SC.Term +sawCreateVar sym nm tp = do + st <- readIORef (userStateRef sym) + let sc = saw_ctx st + ec <- SC.scFreshEC sc nm tp + t <- SC.scFlatTermF sc (SC.ExtCns ec) + modifyIORef (saw_inputs st) (\xs -> xs Seq.|> ec) + return t + +bindSAWTerm :: SAWCoreBackend n solver fs + -> BaseTypeRepr bt + -> SC.Term + -> IO (B.Expr n bt) +bindSAWTerm sym bt t = do + st <- readIORef $ userStateRef sym + ch_r <- readIORef $ saw_elt_cache_r st + let midx = + case t of + SC.STApp { SC.stAppIndex = idx } -> Just idx + SC.Unshared _ -> Nothing + case midx >>= flip IntMap.lookup ch_r of + Just (Some var) -> do + Just Refl <- return $ testEquality bt (B.exprType var) + return var + Nothing -> do + sbVar@(B.BoundVarExpr bv) <- freshConstant sym emptySymbol bt + B.insertIdxValue (saw_elt_cache st) (B.bvarId bv) (SAWExpr t) + case midx of + Just i -> modifyIORef' (saw_elt_cache_r st) $ IntMap.insert i (Some sbVar) + Nothing -> pure () + return sbVar + +newSAWCoreBackend :: + B.FloatModeRepr fm -> + SC.SharedContext -> + NonceGenerator IO s -> + IO (SAWCoreBackend s Yices.Connection (B.Flags fm)) +newSAWCoreBackend fm sc gen = do + inpr <- newIORef Seq.empty + ch <- B.newIdxCache + ch_r <- newIORef IntMap.empty + let feats = Yices.yicesDefaultFeatures + + -- dholland 20250409 this initialization is now circular: + -- the SAWCoreState requires an OnlineBackend + -- the OnlineBackend requires sym + -- sym (the ExprBuilder) requires a SAWCoreState + -- + -- We can't fix this by mucking with the ExprBuilder or + -- OnlineBackend construction as those are controlled by Crucible + -- and What4 interfaces (resp.) so we have to create an initial + -- SAWCoreState with a dummy OnlineBackend. Then we can update the + -- state. However, in order to do this we need to make the state + -- field Maybe, which will be a headache wherever it's used. + let st0 = SAWCoreState + { saw_ctx = sc + , saw_inputs = inpr + , saw_symMap = Map.empty + , saw_elt_cache = ch + , saw_elt_cache_r = ch_r + , saw_online_state_maybe = Nothing + } + st0' <- SAWCoreState' <$> newIORef st0 + sym <- B.newExprBuilder fm st0' gen + ob_st0 <- newOnlineBackend sym feats + let st = st0 { saw_online_state_maybe = Just ob_st0 } + + -- though on the plus side this goop is now handled inside newOnlineBackend +{- + let options = backendOptions ++ onlineBackendOptions ob_st0 ++ Yices.yicesOptions + extendConfig options (getConfiguration sym) + + enableOpt <- getOptionSetting enableOnlineBackend (getConfiguration sym) + let st = st0{ saw_online_state = ob_st0{ onlineEnabled = getOpt enableOpt } } +-} + + writeIORef (userStateRef sym) st + return sym + +-- | Extract the saw_online_state from the SAWCoreState. This is a +-- pretend field accessor created for compat with code from before +-- the online state needed a Maybe in it. (The Nothing case of said +-- Maybe only exists during initialization; see newSAWCoreBackend. +saw_online_state :: SAWCoreState solver fs n -> OnlineBackend solver n (SAWCoreState' solver fs) fs +saw_online_state st = case saw_online_state_maybe st of + Nothing -> panic "CrucibleSAW.SAWCore" ["saw_online_state: hit Nothing after initialization"] + Just ob_st -> ob_st + +-- | Register an interpretation for a symbolic function. This is not +-- used during simulation, but rather, when we translate Crucible +-- values back into SAW. The interpretation function takes a list of +-- arguments in regular (left-to-right) order. +sawRegisterSymFunInterp :: + SAWCoreBackend n solver fs -> + B.ExprSymFn n args ret -> + (SC.SharedContext -> [SC.Term] -> IO SC.Term) -> + IO () +sawRegisterSymFunInterp sym f i = + modifyIORef (userStateRef sym) $ \s -> + s { saw_symMap = Map.insert (indexValue (B.symFnId f)) i (saw_symMap s) } + + +sawBackendSharedContext :: SAWCoreBackend n solver fs -> IO SC.SharedContext +sawBackendSharedContext sym = + saw_ctx <$> readIORef (userStateRef sym) + + +toSC :: OnlineSolver solver => + SAWCoreBackend n solver fs -> B.Expr n tp -> IO SC.Term +toSC sym elt = + do st <- readIORef $ userStateRef sym + evaluateExpr sym (saw_ctx st) (saw_elt_cache st) elt + + +-- | Return a shared term with type nat from a SAWExpr. +{- +scAsIntExpr :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + SAWExpr BaseRealType -> + IO SC.Term +scAsIntExpr _ sc (IntToRealSAWExpr (NatToIntSAWExpr (SAWExpr t))) = SC.scNatToInt sc t +scAsIntExpr _ _ (IntToRealSAWExpr (SAWExpr t)) = return t +scAsIntExpr sym _ SAWExpr{} = unsupported sym + "SAWbackend does not support real values." +-} + +-- | Create a Real SAWELT value from a Rational. +-- +-- This fails on non-integer expressions. +scRealLit :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + Rational -> + IO (SAWExpr BaseRealType) +scRealLit sym sc r + | denominator r /= 1 = + unsupported sym "SAW backend does not support real values" + | otherwise = + IntToRealSAWExpr <$> scIntLit sc (numerator r) + +-- | Create a SAWCore term with type 'Integer' from a Haskell Integer. +scIntLit :: SC.SharedContext -> Integer -> IO (SAWExpr BaseIntegerType) +scIntLit sc i + | i >= 0 = + SAWExpr <$> (SC.scNatToInt sc =<< SC.scNat sc (fromInteger i)) + | otherwise = + SAWExpr <$> (SC.scIntNeg sc =<< SC.scNatToInt sc =<< SC.scNat sc (fromInteger (negate i))) + +-- | Create a SAWCore term with type 'Nat' from a Haskell Nat. +--scNatLit :: SC.SharedContext -> Natural -> IO (SAWExpr BaseNatType) +--scNatLit sc n = SAWExpr <$> SC.scNat sc n + +scBvLit :: SC.SharedContext -> NatRepr w -> BV.BV w -> IO (SAWExpr (BaseBVType w)) +scBvLit sc w bv = SAWExpr <$> SC.scBvConst sc (natValue w) (BV.asUnsigned bv) + + +scRealCmpop :: + OnlineSolver solver => + (SC.SharedContext -> SAWExpr BaseIntegerType -> SAWExpr BaseIntegerType -> IO (SAWExpr BaseBoolType)) -> + SAWCoreBackend n solver fs -> + SC.SharedContext -> + SAWExpr BaseRealType -> + SAWExpr BaseRealType -> + IO (SAWExpr BaseBoolType) +scRealCmpop intOp _ sc (IntToRealSAWExpr x) (IntToRealSAWExpr y) = + intOp sc x y +scRealCmpop _ sym _ _ _ = + unsupported sym "SAW backend does not support real values" + +scRealBinop :: + OnlineSolver solver => + (SC.SharedContext -> SAWExpr BaseIntegerType -> SAWExpr BaseIntegerType -> IO (SAWExpr BaseIntegerType)) -> + SAWCoreBackend n solver fs -> + SC.SharedContext -> + SAWExpr BaseRealType -> + SAWExpr BaseRealType -> + IO (SAWExpr BaseRealType) +scRealBinop intOp _ sc (IntToRealSAWExpr x) (IntToRealSAWExpr y) = + IntToRealSAWExpr <$> intOp sc x y +scRealBinop _ sym _ _ _ = + unsupported sym "SAW backend does not support real values" + + +{- +scIntBinop :: + (SC.SharedContext -> SAWExpr BaseNatType -> SAWExpr BaseNatType -> IO (SAWExpr BaseNatType)) + {- ^ operation on naturals -} -> + (SC.SharedContext -> SC.Term -> SC.Term -> IO SC.Term) {- ^ operation on integers -} -> + SC.SharedContext -> + SAWExpr BaseIntegerType -> + SAWExpr BaseIntegerType -> + IO (SAWExpr BaseIntegerType) +scIntBinop natOp _intOp sc (NatToIntSAWExpr x) (NatToIntSAWExpr y) = + NatToIntSAWExpr <$> natOp sc x y +scIntBinop _natOp intOp sc (NatToIntSAWExpr (SAWExpr x)) (SAWExpr y) = + SAWExpr <$> join (intOp sc <$> SC.scNatToInt sc x <*> pure y) +scIntBinop _natOp intOp sc (SAWExpr x) (NatToIntSAWExpr (SAWExpr y)) = + SAWExpr <$> join (intOp sc <$> pure x <*> SC.scNatToInt sc y) +scIntBinop _natOp intOp sc (SAWExpr x) (SAWExpr y) = + SAWExpr <$> intOp sc x y +-} + +{- +scIntCmpop :: + (SC.SharedContext -> SAWExpr BaseNatType -> SAWExpr BaseNatType -> IO (SAWExpr BaseBoolType)) + {- ^ operation on naturals -} -> + (SC.SharedContext -> SC.Term -> SC.Term -> IO SC.Term) {- ^ operation on integers -} -> + SC.SharedContext -> + SAWExpr BaseIntegerType -> + SAWExpr BaseIntegerType -> + IO (SAWExpr BaseBoolType) +scIntCmpop natOp _intOp sc (NatToIntSAWExpr x) (NatToIntSAWExpr y) = + natOp sc x y +scIntCmpop _natOp intOp sc (NatToIntSAWExpr (SAWExpr x)) (SAWExpr y) = + SAWExpr <$> join (intOp sc <$> SC.scNatToInt sc x <*> pure y) +scIntCmpop _natOp intOp sc (SAWExpr x) (NatToIntSAWExpr (SAWExpr y)) = + SAWExpr <$> join (intOp sc <$> pure x <*> SC.scNatToInt sc y) +scIntCmpop _natOp intOp sc (SAWExpr x) (SAWExpr y) = + SAWExpr <$> intOp sc x y +-} + +scAddReal :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + SAWExpr BaseRealType -> + SAWExpr BaseRealType -> + IO (SAWExpr BaseRealType) +scAddReal = scRealBinop scAddInt + +scAddInt :: SC.SharedContext + -> SAWExpr BaseIntegerType + -> SAWExpr BaseIntegerType + -> IO (SAWExpr BaseIntegerType) +scAddInt = scIntBinop scAddNat SC.scIntAdd + +{- +scAddNat :: SC.SharedContext + -> SAWExpr BaseNatType + -> SAWExpr BaseNatType + -> IO (SAWExpr BaseNatType) +scAddNat sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> SC.scAddNat sc x y +-} + + +scMulReal :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + SAWExpr BaseRealType -> + SAWExpr BaseRealType -> + IO (SAWExpr BaseRealType) +scMulReal = scRealBinop scMulInt + +scMulInt :: SC.SharedContext + -> SAWExpr BaseIntegerType + -> SAWExpr BaseIntegerType + -> IO (SAWExpr BaseIntegerType) +scMulInt = scIntBinop scMulNat SC.scIntMul + +{- +scMulNat :: SC.SharedContext + -> SAWExpr BaseNatType + -> SAWExpr BaseNatType + -> IO (SAWExpr BaseNatType) +scMulNat sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> SC.scMulNat sc x y +-} + +scIteReal :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + SC.Term -> + SAWExpr BaseRealType -> + SAWExpr BaseRealType -> + IO (SAWExpr BaseRealType) +scIteReal sym sc p = scRealBinop (\sc' -> scIteInt sc' p) sym sc + +scIteInt :: SC.SharedContext + -> SC.Term + -> SAWExpr BaseIntegerType + -> SAWExpr BaseIntegerType + -> IO (SAWExpr BaseIntegerType) +scIteInt sc p = scIntBinop + (\sc' -> scIteNat sc' p) + (\sc' x y -> SC.scIntegerType sc >>= \tp -> SC.scIte sc' tp p x y) + sc + +{- +scIteNat :: SC.SharedContext + -> SC.Term + -> SAWExpr BaseNatType + -> SAWExpr BaseNatType + -> IO (SAWExpr BaseNatType) +scIteNat sc p (SAWExpr x) (SAWExpr y) = + SAWExpr <$> (SC.scNatType sc >>= \tp -> SC.scIte sc tp p x y) +-} + +scIte :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + BaseTypeRepr tp -> + SAWExpr BaseBoolType -> + SAWExpr tp -> + SAWExpr tp -> + IO (SAWExpr tp) +scIte sym sc tp (SAWExpr p) x y = + case tp of + BaseRealRepr -> scIteReal sym sc p x y + BaseIntegerRepr -> scIteInt sc p x y + _ -> + do tp' <- baseSCType sym sc tp + x' <- termOfSAWExpr sym sc x + y' <- termOfSAWExpr sym sc y + SAWExpr <$> SC.scIte sc tp' p x' y' + + +scRealEq :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + SAWExpr BaseRealType -> + SAWExpr BaseRealType -> + IO (SAWExpr BaseBoolType) +scRealEq = scRealCmpop scIntEq + +scIntEq :: SC.SharedContext + -> SAWExpr BaseIntegerType + -> SAWExpr BaseIntegerType + -> IO (SAWExpr BaseBoolType) +scIntEq = scIntCmpop scNatEq SC.scIntEq + +{- +scNatEq :: SC.SharedContext + -> SAWExpr BaseNatType + -> SAWExpr BaseNatType + -> IO (SAWExpr BaseBoolType) +scNatEq sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> SC.scEqualNat sc x y +-} + +scBoolEq :: + SC.SharedContext -> + SAWExpr BaseBoolType -> + SAWExpr BaseBoolType -> + IO (SAWExpr BaseBoolType) +scBoolEq sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> SC.scBoolEq sc x y + +scEq :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + BaseTypeRepr tp -> + SAWExpr tp -> + SAWExpr tp -> + IO (SAWExpr BaseBoolType) +scEq sym sc tp x y = + case tp of + BaseBoolRepr -> scBoolEq sc x y + BaseRealRepr -> scRealEq sym sc x y + BaseIntegerRepr -> scIntEq sc x y + BaseBVRepr w -> + do let SAWExpr x' = x + let SAWExpr y' = y + w' <- SC.scNat sc $ fromIntegral (natValue w) + SAWExpr <$> SC.scBvEq sc w' x' y' + _ -> unsupported sym ("SAW backend: equality comparison on unsupported type:" <> Text.pack (show tp)) + + +scAllEq :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + Ctx.Assignment BaseTypeRepr ctx -> + Ctx.Assignment SAWExpr ctx -> + Ctx.Assignment SAWExpr ctx -> + IO (SAWExpr BaseBoolType) +scAllEq _sym sc Ctx.Empty _ _ = SAWExpr <$> SC.scBool sc True +scAllEq sym sc (ctx Ctx.:> tp) (xs Ctx.:> x) (ys Ctx.:> y) + | Ctx.null ctx = scEq sym sc tp x y + | otherwise = + do SAWExpr p <- scAllEq sym sc ctx xs ys + SAWExpr q <- scEq sym sc tp x y + SAWExpr <$> SC.scAnd sc p q + +scRealLe, scRealLt :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + SAWExpr BaseRealType -> + SAWExpr BaseRealType -> + IO (SAWExpr BaseBoolType) +scRealLe = scRealCmpop scIntLe +scRealLt = scRealCmpop scIntLt + +scIntLe, scIntLt :: + SC.SharedContext -> + SAWExpr BaseIntegerType -> + SAWExpr BaseIntegerType -> + IO (SAWExpr BaseBoolType) +scIntLe = scIntCmpop scNatLe SC.scIntLe +scIntLt = scIntCmpop scNatLt SC.scIntLt + +{- +scNatLe, scNatLt :: + SC.SharedContext -> + SAWExpr BaseNatType -> + SAWExpr BaseNatType -> + IO (SAWExpr BaseBoolType) +scNatLe sc (SAWExpr x) (SAWExpr y) = + do lt <- SC.scLtNat sc x y + eq <- SC.scEqualNat sc x y + SAWExpr <$> SC.scOr sc lt eq +scNatLt sc (SAWExpr x) (SAWExpr y) = + SAWExpr <$> SC.scLtNat sc x y +-} + +scBvAdd :: + SC.SharedContext -> + NatRepr w -> + SAWExpr (BaseBVType w) -> + SAWExpr (BaseBVType w) -> + IO (SAWExpr (BaseBVType w)) +scBvAdd sc w (SAWExpr x) (SAWExpr y) = + do n <- SC.scNat sc (natValue w) + SAWExpr <$> SC.scBvAdd sc n x y + +scBvNot :: + SC.SharedContext -> + NatRepr w -> + SAWExpr (BaseBVType w) -> + IO (SAWExpr (BaseBVType w)) +scBvNot sc w (SAWExpr x) = + do n <- SC.scNat sc (natValue w) + SAWExpr <$> SC.scBvNot sc n x + +scBvMul :: + SC.SharedContext -> + NatRepr w -> + SAWExpr (BaseBVType w) -> + SAWExpr (BaseBVType w) -> + IO (SAWExpr (BaseBVType w)) +scBvMul sc w (SAWExpr x) (SAWExpr y) = + do n <- SC.scNat sc (natValue w) + SAWExpr <$> SC.scBvMul sc n x y + +scBvAnd :: + SC.SharedContext -> + NatRepr w -> + SAWExpr (BaseBVType w) -> + SAWExpr (BaseBVType w) -> + IO (SAWExpr (BaseBVType w)) +scBvAnd sc w (SAWExpr x) (SAWExpr y) = + do n <- SC.scNat sc (natValue w) + SAWExpr <$> SC.scBvAnd sc n x y + +scBvXor :: + SC.SharedContext -> + NatRepr w -> + SAWExpr (BaseBVType w) -> + SAWExpr (BaseBVType w) -> + IO (SAWExpr (BaseBVType w)) +scBvXor sc w (SAWExpr x) (SAWExpr y) = + do n <- SC.scNat sc (natValue w) + SAWExpr <$> SC.scBvXor sc n x y + +termOfSAWExpr :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + SAWExpr tp -> IO SC.Term +termOfSAWExpr sym sc expr = + case expr of + SAWExpr t -> return t + --NatToIntSAWExpr (SAWExpr t) -> SC.scNatToInt sc t + IntToRealSAWExpr _ + -> unsupported sym "SAW backend does not support real values" + +applyExprSymFn :: + forall n solver fs args ret. + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + B.ExprSymFn n args ret -> + Ctx.Assignment SAWExpr args -> + IO (SAWExpr ret) +applyExprSymFn sym sc fn args = + do st <- readIORef (userStateRef sym) + mk <- + case Map.lookup (indexValue (B.symFnId fn)) (saw_symMap st) of + Nothing -> panic "SAWCore.applyExprSymFn" + [ "Unknown symbolic function." + , "*** Name: " ++ show fn + ] + Just mk -> return mk + ts <- evaluateAsgn args + SAWExpr <$> mk sc (reverse ts) + where + evaluateAsgn :: Ctx.Assignment SAWExpr args' -> IO [SC.Term] + evaluateAsgn Ctx.Empty = return [] + evaluateAsgn (xs Ctx.:> x) = + do vs <- evaluateAsgn xs + v <- termOfSAWExpr sym sc x + return (v : vs) + + +considerSatisfiability :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + Maybe ProgramLoc -> + B.BoolExpr n -> + IO BranchResult +considerSatisfiability sym mbPloc p = + withSolverProcess' + (\sym' -> saw_online_state <$> readIORef (userStateRef sym')) sym + (pure IndeterminateBranchResult) + $ \proc -> + do pnot <- notPred sym p + let locDesc = case mbPloc of + Just ploc -> show (plSourceLoc ploc) + Nothing -> "(unknown location)" + let rsn = "branch sat: " ++ locDesc + p_res <- checkSatisfiable proc rsn p + pnot_res <- checkSatisfiable proc rsn pnot + case (p_res, pnot_res) of + (Unsat{}, Unsat{}) -> return UnsatisfiableContext + (_ , Unsat{}) -> return (NoBranch True) + (Unsat{}, _ ) -> return (NoBranch False) + _ -> return IndeterminateBranchResult + +{- | Declare that we don't support something or other. +This aborts the current path of execution, and adds a proof +obligation to ensure that we won't get there. +These proof obligations are all tagged with "Unsupported", so that +users of the library can choose if they will try to discharge them, +fail in some other way, or just ignore them. -} +unsupported :: OnlineSolver solver => SAWCoreBackend n solver fs -> Text.Text -> IO a +unsupported sym x = addFailedAssertion sym (Unsupported callstack $ Text.unpack x) + +evaluateExpr :: forall n solver tp fs. + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + B.IdxCache n SAWExpr -> + B.Expr n tp -> + IO SC.Term +evaluateExpr sym sc cache = f [] + where + -- Evaluate the element, and expect the result to have the same type. + f :: [Maybe SolverSymbol] -> B.Expr n tp' -> IO SC.Term + f env elt = termOfSAWExpr sym sc =<< eval env elt + + eval :: [Maybe SolverSymbol] -> B.Expr n tp' -> IO (SAWExpr tp') + eval env elt = B.idxCacheEval cache elt (go env elt) + + realFail :: IO a + realFail = unsupported sym "SAW backend does not support real values" + + cplxFail :: IO a + cplxFail = unsupported sym "SAW backend does not support complex values" + + floatFail :: IO a + floatFail = unsupported sym "SAW backend does not support floating-point values" + + stringFail :: IO a + stringFail = unsupported sym "SAW backend does not support string values" + + unimplemented :: Text.Text -> IO a + unimplemented x = unsupported sym $ "SAW backend: not implemented: " <> x + + go :: [Maybe SolverSymbol] -> B.Expr n tp' -> IO (SAWExpr tp') + + go _ (B.BoolExpr b _) = SAWExpr <$> SC.scBool sc b + + go _ (B.SemiRingLiteral sr x _) = + case sr of + --B.SemiRingNatRepr -> scNatLit sc x + B.SemiRingBVRepr _ w -> scBvLit sc w x + B.SemiRingIntegerRepr -> scIntLit sc x + B.SemiRingRealRepr -> scRealLit sym sc x + + go _ (B.StringExpr{}) = + unsupported sym "SAW backend does not support string values" + + go env (B.BoundVarExpr bv) = + case B.bvarKind bv of + B.UninterpVarKind -> do + tp <- baseSCType sym sc (B.bvarType bv) + SAWExpr <$> sawCreateVar sym nm tp + where nm = solverSymbolAsText $ B.bvarName bv + B.LatchVarKind -> + unsupported sym "SAW backend does not support latch variables" + B.QuantifierVarKind -> do + case elemIndex (Just $ B.bvarName bv) env of + Nothing -> unsupported sym $ "unbound quantifier variable " <> nm + Just idx -> SAWExpr <$> SC.scLocalVar sc idx + where nm = solverSymbolAsText $ B.bvarName bv + + go env (B.NonceAppExpr p) = + case B.nonceExprApp p of + B.Annotation _tpr _n x -> + eval env x + + B.Forall bvar body -> + case B.bvarType bvar of + BaseBVRepr wrepr -> do + w <- SC.scNat sc $ natValue wrepr + ty <- SC.scVecType sc w =<< SC.scBoolType sc + SAWExpr <$> + (SC.scBvForall sc w + =<< SC.scLambda sc nm ty =<< f (Just (B.bvarName bvar):env) body) + where nm = solverSymbolAsText $ B.bvarName bvar + _ -> unsupported sym "SAW backend only supports universal quantifiers over bitvectors" + B.Exists{} -> + unsupported sym "SAW backend does not support existential quantifiers" + B.ArrayFromFn{} -> unimplemented "ArrayFromFn" + B.MapOverArrays{} -> unimplemented "MapOverArrays" + B.ArrayTrueOnEntries{} -> unimplemented "ArrayTrueOnEntries" + B.FnApp fn asgn -> + do args <- traverseFC (eval env) asgn + applyExprSymFn sym sc fn args + + go env a0@(B.AppExpr a) = + let nyi = unsupported sym $ + "Expression form not yet implemented in SAWCore backend:\n" + <> Text.pack (show a0) + in + case B.appExprApp a of + B.BaseIte bt _ c xe ye -> join (scIte sym sc bt <$> eval env c <*> eval env xe <*> eval env ye) + B.BaseEq bt xe ye -> join (scEq sym sc bt <$> eval env xe <*> eval env ye) + + B.SemiRingLe sr xe ye -> + case sr of + B.OrderedSemiRingRealRepr -> join (scRealLe sym sc <$> eval env xe <*> eval env ye) + B.OrderedSemiRingIntegerRepr -> join (scIntLe sc <$> eval env xe <*> eval env ye) + --B.OrderedSemiRingNatRepr -> join (scNatLe sc <$> eval env xe <*> eval env ye) + + B.NotPred x -> + goNeg env x + + B.ConjPred xs -> + case BM.viewConjMap xs of + BM.ConjTrue -> SAWExpr <$> SC.scBool sc True + BM.ConjFalse -> SAWExpr <$> SC.scBool sc False + BM.Conjuncts (t:|ts) -> + let pol (x,BM.Positive) = f env x + pol (x,BM.Negative) = termOfSAWExpr sym sc =<< goNeg env x + in SAWExpr <$> join (foldM (SC.scAnd sc) <$> pol t <*> mapM pol ts) + + B.SemiRingProd pd -> + case WSum.prodRepr pd of + B.SemiRingRealRepr -> + do pd' <- WSum.prodEvalM (scMulReal sym sc) (eval env) pd + maybe (scRealLit sym sc 1) return pd' + B.SemiRingIntegerRepr -> + do pd' <- WSum.prodEvalM (scMulInt sc) (eval env) pd + maybe (scIntLit sc 1) return pd' +{- + B.SemiRingNatRepr -> + do pd' <- WSum.prodEvalM (scMulNat sc) (eval env) pd + maybe (scNatLit sc 1) return pd' +-} + B.SemiRingBVRepr B.BVArithRepr w -> + do n <- SC.scNat sc (natValue w) + pd' <- WSum.prodEvalM (SC.scBvMul sc n) (f env) pd + maybe (scBvLit sc w (BV.one w)) (return . SAWExpr) pd' + B.SemiRingBVRepr B.BVBitsRepr w -> + do n <- SC.scNat sc (natValue w) + pd' <- WSum.prodEvalM (SC.scBvAnd sc n) (f env) pd + maybe (scBvLit sc w (BV.maxUnsigned w)) (return . SAWExpr) pd' + + B.SemiRingSum ss -> + case WSum.sumRepr ss of + B.SemiRingRealRepr -> WSum.evalM add smul (scRealLit sym sc) ss + where add x y = scAddReal sym sc x y + smul 1 e = eval env e + smul sm e = join $ scMulReal sym sc <$> scRealLit sym sc sm <*> eval env e + B.SemiRingIntegerRepr -> WSum.evalM add smul (scIntLit sc) ss + where add x y = scAddInt sc x y + smul 1 e = eval env e + smul sm e = join $ scMulInt sc <$> scIntLit sc sm <*> eval env e +{- + B.SemiRingNatRepr -> WSum.evalM add smul (scNatLit sc) ss + where add x y = scAddNat sc x y + smul 1 e = eval env e + smul sm e = join $ scMulNat sc <$> scNatLit sc sm <*> eval env e +-} + B.SemiRingBVRepr B.BVArithRepr w -> WSum.evalM add smul (scBvLit sc w) ss + where add x y = scBvAdd sc w x y + smul (BV.BV 1) e = eval env e + smul sm e = join (scBvMul sc w <$> scBvLit sc w sm <*> eval env e) + B.SemiRingBVRepr B.BVBitsRepr w + | ss^.WSum.sumOffset == one -> scBvNot sc w =<< bitwise_eval (ss & WSum.sumOffset .~ BV.zero w) + | otherwise -> bitwise_eval ss + + where one = BV.maxUnsigned w + bitwise_eval = WSum.evalM add smul (scBvLit sc w) + add x y = scBvXor sc w x y + smul sm e + | sm == one = eval env e + | otherwise = join (scBvAnd sc w <$> scBvLit sc w sm <*> eval env e) + + B.RealIsInteger{} -> unsupported sym "SAW backend does not support real values" + + B.BVOrBits w bs -> + do n <- SC.scNat sc (natValue w) + bs' <- traverse (f env) (B.bvOrToList bs) + case bs' of + [] -> scBvLit sc w (BV.zero w) + x:xs -> SAWExpr <$> foldM (SC.scBvOr sc n) x xs + + B.BVFill w p -> + do bit <- SC.scBoolType sc + n <- SC.scNat sc (natValue w) + x <- f env p + SAWExpr <$> SC.scGlobalApply sc (SC.mkIdent SC.preludeName "replicate") [n, bit, x] + + B.BVTestBit i bv -> fmap SAWExpr $ do + w <- SC.scNat sc (natValue (bvWidth bv)) + bit <- SC.scBoolType sc + -- NB, SAWCore's `scAt` is big endian + let j = natValue (bvWidth bv) - i - 1 + join (SC.scAt sc w bit <$> f env bv <*> SC.scNat sc j) + + B.BVSlt x y -> fmap SAWExpr $ do + w <- SC.scNat sc (natValue (bvWidth x)) + join (SC.scBvSLt sc w <$> f env x <*> f env y) + B.BVUlt x y -> fmap SAWExpr $ do + w <- SC.scNat sc (natValue (bvWidth x)) + join (SC.scBvULt sc w <$> f env x <*> f env y) + + B.BVUnaryTerm{} -> unsupported sym "SAW backend does not support the unary bitvector representation" + + B.BVUdiv _ x y -> fmap SAWExpr $ do + n <- SC.scNat sc (natValue (bvWidth x)) + join (SC.scBvUDiv sc n <$> f env x <*> f env y) + B.BVUrem _ x y -> fmap SAWExpr $ do + n <- SC.scNat sc (natValue (bvWidth x)) + join (SC.scBvURem sc n <$> f env x <*> f env y) + B.BVSdiv _ x y -> fmap SAWExpr $ do + -- NB: bvSDiv applies 'Succ' to its width argument, so we + -- need to subtract 1 to make the types match. + n <- SC.scNat sc (natValue (bvWidth x) - 1) + join (SC.scBvSDiv sc n <$> f env x <*> f env y) + B.BVSrem _ x y -> fmap SAWExpr $ do + -- NB: bvSDiv applies 'Succ' to its width argument, so we + -- need to subtract 1 to make the types match. + n <- SC.scNat sc (natValue (bvWidth x) - 1) + join (SC.scBvSRem sc n <$> f env x <*> f env y) + B.BVShl _ x y -> fmap SAWExpr $ do + let w = natValue (bvWidth x) + n <- SC.scNat sc w + join (SC.scBvShl sc n <$> f env x <*> (SC.scBvToNat sc w =<< f env y)) + B.BVLshr _ x y -> fmap SAWExpr $ do + let w = natValue (bvWidth x) + n <- SC.scNat sc w + join (SC.scBvShr sc n <$> f env x <*> (SC.scBvToNat sc w =<< f env y)) + B.BVAshr _ x y -> fmap SAWExpr $ do + let w = natValue (bvWidth x) + -- NB: bvSShr applies a `Succ` to its width argument, so we subtract + -- 1 here to make things match up. + n <- SC.scNat sc (w - 1) + join (SC.scBvSShr sc n <$> f env x <*> (SC.scBvToNat sc w =<< f env y)) + B.BVRol w x y -> fmap SAWExpr $ do + n <- SC.scNat sc (natValue w) + bit <- SC.scBoolType sc + x' <- f env x + y' <- SC.scBvToNat sc (natValue w) =<< f env y + SC.scGlobalApply sc (SC.mkIdent SC.preludeName "rotateL") [n,bit,x',y'] + B.BVRor w x y -> fmap SAWExpr $ do + n <- SC.scNat sc (natValue w) + bit <- SC.scBoolType sc + x' <- f env x + y' <- SC.scBvToNat sc (natValue w) =<< f env y + SC.scGlobalApply sc (SC.mkIdent SC.preludeName "rotateR") [n,bit,x',y'] + B.BVConcat _ x y -> fmap SAWExpr $ do + n <- SC.scNat sc (natValue (bvWidth x)) + m <- SC.scNat sc (natValue (bvWidth y)) + t <- SC.scBoolType sc + join (SC.scAppend sc t n m <$> f env x <*> f env y) + B.BVSelect start num x -> fmap SAWExpr $ do + i <- SC.scNat sc (natValue (bvWidth x) - natValue num - natValue start) + n <- SC.scNat sc (natValue num) + o <- SC.scNat sc (natValue start) + t <- SC.scBoolType sc + x' <- f env x + SC.scSlice sc t i n o x' + B.BVZext w' x -> fmap SAWExpr $ do + let w = bvWidth x + n <- SC.scNat sc (natValue w) + m <- SC.scNat sc (natValue w' - natValue w) + x' <- f env x + SC.scBvUExt sc m n x' + B.BVSext w' x -> fmap SAWExpr $ do + let w = bvWidth x + -- NB: width - 1 to make SAWCore types work out + n <- SC.scNat sc (natValue w - 1) + m <- SC.scNat sc (natValue w' - natValue w) + x' <- f env x + SC.scBvSExt sc m n x' + B.BVPopcount w x -> + do n <- SC.scNat sc (natValue w) + x' <- f env x + SAWExpr <$> SC.scBvPopcount sc n x' + B.BVCountLeadingZeros w x -> + do n <- SC.scNat sc (natValue w) + x' <- f env x + SAWExpr <$> SC.scBvCountLeadingZeros sc n x' + B.BVCountTrailingZeros w x -> + do n <- SC.scNat sc (natValue w) + x' <- f env x + SAWExpr <$> SC.scBvCountTrailingZeros sc n x' + + -- Note: SAWCore supports only unidimensional arrays. As a result, What4 multidimensional + -- arrays cannot be translated to SAWCore. + B.ArrayMap indexTypes range updates arr + | Ctx.Empty Ctx.:> idx_type <- indexTypes -> + do sc_idx_type <- baseSCType sym sc idx_type + sc_elm_type <- baseSCType sym sc range + sc_arr <- f env arr + SAWExpr <$> foldM + (\sc_acc_arr (Ctx.Empty Ctx.:> idx_lit, elm) -> + do sc_idx <- f env =<< indexLit sym idx_lit + sc_elm <- f env elm + SC.scArrayUpdate sc sc_idx_type sc_elm_type sc_acc_arr sc_idx sc_elm) + sc_arr + (AUM.toList updates) + | otherwise -> unimplemented "multidimensional ArrayMap" + + B.ConstantArray indexTypes range v + | Ctx.Empty Ctx.:> idx_type <- indexTypes -> + do sc_idx_type <- baseSCType sym sc idx_type + sc_elm_type <- baseSCType sym sc range + sc_elm <- f env v + SAWExpr <$> SC.scArrayConstant sc sc_idx_type sc_elm_type sc_elm + | otherwise -> unimplemented "multidimensional ConstantArray" + + B.SelectArray range arr indexTerms + | Ctx.Empty Ctx.:> idx <- indexTerms + , idx_type <- exprType idx -> + do sc_idx_type <- baseSCType sym sc idx_type + sc_elm_type <- baseSCType sym sc range + sc_arr <- f env arr + sc_idx <- f env idx + SAWExpr <$> SC.scArrayLookup sc sc_idx_type sc_elm_type sc_arr sc_idx + | otherwise -> unimplemented "multidimensional SelectArray" + + B.UpdateArray range indexTypes arr indexTerms v + | Ctx.Empty Ctx.:> idx_type <- indexTypes + , Ctx.Empty Ctx.:> idx <- indexTerms -> + do sc_idx_type <- baseSCType sym sc idx_type + sc_elm_type <- baseSCType sym sc range + sc_arr <- f env arr + sc_idx <- f env idx + sc_elm <- f env v + SAWExpr <$> SC.scArrayUpdate sc sc_idx_type sc_elm_type sc_arr sc_idx sc_elm + | otherwise -> unimplemented "multidimensional UpdateArray" + + B.CopyArray w a_repr dest_arr dest_idx src_arr src_idx len -> + do sc_w <- SC.scNat sc (natValue w) + sc_a <- baseSCType sym sc a_repr + sc_dest_arr <- f env dest_arr + sc_dest_idx <- f env dest_idx + sc_src_arr <- f env src_arr + sc_src_idx <- f env src_idx + sc_len <- f env len + SAWExpr <$> SC.scArrayCopy sc sc_w sc_a sc_dest_arr sc_dest_idx sc_src_arr sc_src_idx sc_len + + B.SetArray w a_repr arr idx val len -> + do sc_w <- SC.scNat sc (natValue w) + sc_a <- baseSCType sym sc a_repr + sc_arr <- f env arr + sc_idx <- f env idx + sc_val <- f env val + sc_len <- f env len + SAWExpr <$> SC.scArraySet sc sc_w sc_a sc_arr sc_idx sc_val sc_len + +{- + B.NatToInteger x -> NatToIntSAWExpr <$> eval env x + B.IntegerToNat x -> + eval env x >>= \case + NatToIntSAWExpr z -> return z + SAWExpr z -> SAWExpr <$> (SC.scIntToNat sc z) + + B.NatDiv x y -> + do x' <- f env x + y' <- f env y + SAWExpr <$> SC.scDivNat sc x' y' + + B.NatMod x y -> + do x' <- f env x + y' <- f env y + SAWExpr <$> SC.scModNat sc x' y' +-} + + B.IntDiv x y -> + do x' <- f env x + y' <- f env y + SAWExpr <$> SC.scIntDiv sc x' y' + B.IntMod x y -> + do x' <- f env x + y' <- f env y + SAWExpr <$> SC.scIntMod sc x' y' + B.IntAbs x -> + eval env x >>= \case + --NatToIntSAWExpr z -> return (NatToIntSAWExpr z) + SAWExpr z -> SAWExpr <$> (SC.scIntAbs sc z) + + B.IntDivisible x 0 -> + do x' <- f env x + SAWExpr <$> (SC.scIntEq sc x' =<< SC.scIntegerConst sc 0) + B.IntDivisible x k -> + do x' <- f env x + k' <- SC.scIntegerConst sc (toInteger k) + z <- SC.scIntMod sc x' k' + SAWExpr <$> (SC.scIntEq sc z =<< SC.scIntegerConst sc 0) + +{- + B.BVToNat x -> + let n = natValue (bvWidth x) in + SAWExpr <$> (SC.scBvToNat sc n =<< f env x) +-} + + B.IntegerToBV x w -> + do n <- SC.scNat sc (natValue w) + SAWExpr <$> (SC.scIntToBv sc n =<< f env x) + + B.BVToInteger x -> + do n <- SC.scNat sc (natValue (bvWidth x)) + SAWExpr <$> (SC.scBvToInt sc n =<< f env x) + + B.SBVToInteger x -> + do n <- SC.scNat sc (natValue (bvWidth x)) + SAWExpr <$> (SC.scSbvToInt sc n =<< f env x) + + -- Proper support for real and complex numbers will require additional + -- work on the SAWCore side + B.IntegerToReal x -> IntToRealSAWExpr . SAWExpr <$> f env x + B.RealToInteger x -> + eval env x >>= \case + IntToRealSAWExpr x' -> return x' + _ -> realFail + + ------------------------------------------------------------------------ + -- Floating point operations + + --B.FloatPZero{} -> floatFail + --B.FloatNZero{} -> floatFail + --B.FloatNaN{} -> floatFail + --B.FloatPInf{} -> floatFail + --B.FloatNInf{} -> floatFail + B.FloatNeg{} -> floatFail + B.FloatAbs{} -> floatFail + B.FloatSqrt{} -> floatFail + B.FloatAdd{} -> floatFail + B.FloatSub{} -> floatFail + B.FloatMul{} -> floatFail + B.FloatDiv{} -> floatFail + B.FloatRem{} -> floatFail + --B.FloatMin{} -> floatFail + --B.FloatMax{} -> floatFail + B.FloatFMA{} -> floatFail + B.FloatFpEq{} -> floatFail + --B.FloatFpNe{} -> floatFail + B.FloatLe{} -> floatFail + B.FloatLt{} -> floatFail + B.FloatIsNaN{} -> floatFail + B.FloatIsInf{} -> floatFail + B.FloatIsZero{} -> floatFail + B.FloatIsPos{} -> floatFail + B.FloatIsNeg{} -> floatFail + B.FloatIsSubnorm{} -> floatFail + B.FloatIsNorm{} -> floatFail + B.FloatCast{} -> floatFail + B.FloatRound{} -> floatFail + B.FloatFromBinary{} -> floatFail + B.BVToFloat{} -> floatFail + B.SBVToFloat{} -> floatFail + B.RealToFloat{} -> floatFail + B.FloatToBV{} -> floatFail + B.FloatToSBV{} -> floatFail + B.FloatToReal{} -> floatFail + B.FloatToBinary{} -> floatFail + + B.RoundReal{} -> realFail + B.RoundEvenReal{} -> realFail + B.FloorReal{} -> realFail + B.CeilReal{} -> realFail + B.RealDiv{} -> realFail + B.RealSqrt{} -> realFail + --B.Pi{} -> realFail + --B.RealSin{} -> realFail + --B.RealCos{} -> realFail + --B.RealSinh{} -> realFail + --B.RealCosh{} -> realFail + --B.RealExp{} -> realFail + --B.RealLog{} -> realFail + --B.RealATan2{} -> realFail + B.RealSpecialFunction{} -> realFail + + B.Cplx{} -> cplxFail + B.RealPart{} -> cplxFail + B.ImagPart{} -> cplxFail + + B.StringLength{} -> stringFail + B.StringAppend{} -> stringFail + B.StringContains{} -> stringFail + B.StringIsPrefixOf{} -> stringFail + B.StringIsSuffixOf{} -> stringFail + B.StringIndexOf{} -> stringFail + B.StringSubstring{} -> stringFail + + B.StructCtor{} -> nyi -- FIXME + B.StructField{} -> nyi -- FIXME + + -- returns the logical negation of the result of 'go' + -- negations are pushed inside conjunctions and less-than-or-equal + goNeg :: [Maybe SolverSymbol] -> B.Expr n BaseBoolType -> IO (SAWExpr BaseBoolType) + goNeg env expr = + case expr of + -- negation of (x /\ y) becomes (~x \/ ~y) + B.AppExpr (B.appExprApp -> B.ConjPred xs) -> + case BM.viewConjMap xs of + BM.ConjTrue -> SAWExpr <$> SC.scBool sc False + BM.ConjFalse -> SAWExpr <$> SC.scBool sc True + BM.Conjuncts (t:|ts) -> + let pol (x, BM.Positive) = termOfSAWExpr sym sc =<< goNegAtom env x + pol (x, BM.Negative) = f env x + in SAWExpr <$> join (foldM (SC.scOr sc) <$> pol t <*> mapM pol ts) + _ -> goNegAtom env expr + + -- returns the logical negation of the result of 'go' + -- negations are pushed inside less-than-or-equal + goNegAtom :: [Maybe SolverSymbol] -> B.Expr n BaseBoolType -> IO (SAWExpr BaseBoolType) + goNegAtom env expr = + case expr of + -- negation of (x <= y) becomes (y < x) + B.AppExpr (B.appExprApp -> B.SemiRingLe sr xe ye) -> + case sr of + B.OrderedSemiRingRealRepr -> join (scRealLt sym sc <$> eval env ye <*> eval env xe) + B.OrderedSemiRingIntegerRepr -> join (scIntLt sc <$> eval env ye <*> eval env xe) + --B.OrderedSemiRingNatRepr -> join (scNatLt sc <$> eval env ye <*> eval env xe) + _ -> SAWExpr <$> (SC.scNot sc =<< f env expr) + +withSolverProcess :: + OnlineSolver solver => + SAWCoreBackend scope solver fs -> + IO a -> + (SolverProcess scope solver -> IO a) -> + IO a +withSolverProcess = withSolverProcess' (\sym' -> saw_online_state <$> readIORef (userStateRef sym')) + +withSolverConn :: + OnlineSolver solver => + SAWCoreBackend scope solver fs -> + (WriterConn scope solver -> IO ()) -> + IO () +withSolverConn sym k = withSolverProcess sym (pure ()) (k . solverConn) + + +getAssumptionStack :: + SAWCoreBackend s solver fs -> + IO (AssumptionStack (Assumption (B.BoolExpr s)) SimError) +getAssumptionStack sym = + (assumptionStack . saw_online_state) <$> readIORef (userStateRef sym) + + +-- TODO! we should find a better way to share implementations with `OnlineBackend` +-- +-- XXX: while the first argument here needs to be the ExprBuilder, the second can +-- be something else (AIUI) and if we peel some bits of the state out and put +-- them in the second argument instead we can probably avoid the circular +-- initialization in newSAWCoreBackend. +instance OnlineSolver solver => IsSymBackend (SAWCoreBackend n solver fs) (SAWCoreBackend n solver fs) where + + addDurableProofObligation sym a = + AS.addProofObligation a =<< getAssumptionStack sym + + addAssumption sym a = + let cond = asConstantPred (a^.labeledPred) + in case cond of + Just False -> abortExecBecause (AssumedFalse (a^.labeledPredMsg)) + _ -> -- Send assertion to the solver, unless it is trivial. + -- NB, don't add the assumption to the assumption stack unless + -- the solver assumptions succeeded + do withSolverConn sym $ \conn -> + case cond of + Just True -> return () + _ -> SMT.assume conn (a^.labeledPred) + + -- Record assumption, even if trivial. + -- This allows us to keep track of the full path we are on. + stk <- getAssumptionStack sym + AS.appendAssumptions (Seq.singleton a) stk + + addAssumptions sym a = + -- NB, don't add the assumption to the assumption stack unless + -- the solver assumptions succeeded + do withSolverConn sym $ \conn -> + -- Tell the solver of assertions + mapM_ (SMT.assume conn . view labeledPred) (toList a) + -- Add assertions to list + stk <- getAssumptionStack sym + AS.appendAssumptions a stk + + getPathCondition sym = + do stk <- getAssumptionStack sym + ps <- AS.collectAssumptions stk + andAllOf sym (folded.labeledPred) ps + + collectAssumptions sym = + AS.collectAssumptions =<< getAssumptionStack sym + + pushAssumptionFrame sym = + do -- NB, don't push a frame in the assumption stack unless + -- pushing to the solver succeeded + withSolverProcess sym (pure ()) push + AS.pushFrame =<< getAssumptionStack sym + + popAssumptionFrame sym ident = + -- NB, pop the frame whether or not the solver pop succeeds + do frm <- AS.popFrame ident =<< getAssumptionStack sym + withSolverProcess sym (pure ()) pop + return frm + + popUntilAssumptionFrame sym ident = + -- NB, pop the frames whether or not the solver pop succeeds + do n <- AS.popFramesUntil ident =<< getAssumptionStack sym + withSolverProcess sym (pure ()) $ \proc -> + forM_ [0..(n-1)] $ \_ -> pop proc + + popAssumptionFrameAndObligations sym ident = do + -- NB, pop the frames whether or not the solver pop succeeds + do frmAndGls <- AS.popFrameAndGoals ident =<< getAssumptionStack sym + withSolverProcess sym (pure ()) pop + return frmAndGls + + getProofObligations sym = + do stk <- getAssumptionStack sym + AS.getProofObligations stk + + clearProofObligations sym = + do stk <- getAssumptionStack sym + AS.clearProofObligations stk + + saveAssumptionState sym = + do stk <- getAssumptionStack sym + AS.saveAssumptionStack stk + + restoreAssumptionState sym gc = + do st <- saw_online_state <$> readIORef (userStateRef sym) + restoreSolverState gc st + + -- restore the previous assumption stack + stk <- getAssumptionStack sym + AS.restoreAssumptionStack gc stk diff --git a/src/SAWScript/Crucible/LLVM/AArch32.hs b/src/SAWScript/Crucible/LLVM/AArch32.hs new file mode 100644 index 000000000..5e541cf11 --- /dev/null +++ b/src/SAWScript/Crucible/LLVM/AArch32.hs @@ -0,0 +1,1033 @@ +{- | +Module : SAWScript.Crucible.LLVM.AArch32 +Description : Implements a SAWScript primitive for verifying aarch32 functions + against LLVM specifications. +Maintainer : sbreese +Stability : provisional +-} + +{-# Language OverloadedStrings #-} +{-# Language FlexibleContexts #-} +{-# Language ScopedTypeVariables #-} +{-# Language TypeOperators #-} +{-# Language PatternSynonyms #-} +{-# Language LambdaCase #-} +{-# Language MultiWayIf #-} +{-# Language TupleSections #-} +{-# Language ImplicitParams #-} +{-# Language TypeApplications #-} +{-# Language GADTs #-} +{-# Language RankNTypes #-} +{-# Language DataKinds #-} +{-# Language ConstraintKinds #-} +{-# Language GeneralizedNewtypeDeriving #-} +{-# Language TemplateHaskell #-} + +module SAWScript.Crucible.LLVM.AArch32 + ( llvm_verify_aarch32 + ) where + +import Control.Lens.TH (makeLenses) + +import GHC.Natural (Natural) + +import System.IO (stdout) +import Control.Exception (Exception(..), throw) +import Control.Lens (view, use, toListOf, folded, (&), (^.), (.~), (%~), (.=)) +import Control.Applicative ((<|>)) +import Control.Monad.State +import Control.Monad.Catch (MonadThrow) + +import qualified Data.BitVector.Sized as BV +import Data.Foldable (foldlM) +import qualified Data.List.NonEmpty as NE +import qualified Data.Vector as Vector +import qualified Data.Text as Text +import Data.Text.Encoding (decodeUtf8, encodeUtf8) +import Data.ByteString (ByteString) +import qualified Data.ByteString as BS +import qualified Data.ByteString.Char8 as BSC +import qualified Data.Set as Set +import qualified Data.Map as Map +import Data.Map (Map) +import Data.Maybe + +import qualified Text.LLVM.AST as LLVM + +import Data.Parameterized.Some +import Data.Parameterized.NatRepr +import Data.Parameterized.Context hiding (view) +import Data.Parameterized.Nonce + +import Verifier.SAW.FiniteValue +import Verifier.SAW.SharedTerm +import Verifier.SAW.TypedTerm +import Verifier.SAW.Recognizer (asBool) + +import SAWScript.Proof +import SAWScript.Prover.SolverStats +import SAWScript.TopLevel +import SAWScript.Value +import SAWScript.Options + +import qualified SAWScript.Crucible.Common.MethodSpec as MS +import qualified SAWScript.Crucible.Common.Override as O +import qualified SAWScript.Crucible.Common.Setup.Type as Setup + +import SAWScript.Crucible.LLVM.Builtins +import SAWScript.Crucible.LLVM.MethodSpecIR (LLVMCrucibleContext(..)) +import SAWScript.Crucible.LLVM.ResolveSetupValue +import qualified SAWScript.Crucible.LLVM.Override as LO + +import qualified What4.Expr as W4 +import qualified What4.FunctionName as W4 +import qualified What4.Interface as W4 +import qualified What4.LabeledPred as W4 +import qualified What4.ProgramLoc as W4 +import qualified What4.Solver.Yices as Yices + +import qualified Lang.Crucible.Analysis.Postdom as C +import qualified Lang.Crucible.Backend as C +import qualified SAWScript.Crucible.CrucibleSAW.SAWCore as C +import qualified Lang.Crucible.CFG.Core as C +import qualified Lang.Crucible.FunctionHandle as C +import qualified Lang.Crucible.Simulator.EvalStmt as C +import qualified Lang.Crucible.Simulator.ExecutionTree as C +import qualified Lang.Crucible.Simulator.GlobalState as C +import qualified Lang.Crucible.Simulator.Operations as C +import qualified Lang.Crucible.Simulator.OverrideSim as C +import qualified Lang.Crucible.Simulator.RegMap as C +import qualified Lang.Crucible.Simulator.SimError as C +import qualified Lang.Crucible.Simulator.PathSatisfiability as C + +import qualified Lang.Crucible.LLVM.DataLayout as C.LLVM +import qualified Lang.Crucible.LLVM.Extension as C.LLVM +import qualified Lang.Crucible.LLVM.Intrinsics as C.LLVM +import qualified Lang.Crucible.LLVM.MemModel as C.LLVM +import qualified Lang.Crucible.LLVM.MemType as C.LLVM +import qualified Lang.Crucible.LLVM.Translation as C.LLVM +import qualified Lang.Crucible.LLVM.TypeContext as C.LLVM + +import qualified Data.Macaw.Types as Macaw +import qualified Data.Macaw.Discovery as Macaw +import qualified Data.Macaw.Memory as Macaw +import qualified Data.Macaw.Memory.LoadCommon as Macaw +import qualified Data.Macaw.Memory.ElfLoader as Macaw +import qualified Data.Macaw.CFG as Macaw +import qualified Data.Macaw.Symbolic as Macaw +import qualified Data.Macaw.Symbolic.Backend as Macaw +import qualified Data.Macaw.AArch32.Symbolic as Macaw +import qualified Data.Macaw.AArch32.Symbolic as Macaw.AArch32 +import qualified Data.Macaw.ARM as Macaw +import qualified Data.Macaw.ARM.ARMReg as Macaw + +import qualified Data.ElfEdit as Elf + +import qualified Language.ASL.Globals as ASL + +------------------------------------------------------------------------------- +-- ** Utility type synonyms and functions + +type Sym = C.SAWCoreBackend GlobalNonceGenerator Yices.Connection (W4.Flags W4.FloatReal) +type LLVMArch = C.LLVM.X86 32 +--type LLVM = C.LLVM.LLVM LLVMArch +type LLVM = C.LLVM.LLVM +type LLVMOverrideMatcher rorw a = O.OverrideMatcher LLVM rorw a +type Regs = Assignment (C.RegValue' Sym) (Macaw.MacawCrucibleRegTypes Macaw.ARM) +type Register = Macaw.ARMReg (Macaw.BVType 32) +type Mem = C.LLVM.MemImpl Sym +type Ptr = C.LLVM.LLVMPtr Sym 32 +type AArch32Constraints = + ( C.LLVM.HasPtrWidth (C.LLVM.ArchWidth LLVMArch) + , C.LLVM.HasLLVMAnn Sym + , ?lc :: C.LLVM.TypeContext + ) + +newtype AArch32Error = AArch32Error String deriving Show +instance Exception AArch32Error + +throwAArch32 :: MonadThrow m => String -> m a +throwAArch32 = throw . AArch32Error + +data RelevantElf = RelevantElf + { memory :: Macaw.Memory 32 + , funSymMap :: Macaw.AddrSymMap 32 + , symMap :: Macaw.AddrSymMap 32 + } + +data Unit = Bytes | Words | DWords | QWords | V128s | V256s deriving Show + +unitByteSize :: Unit -> (forall w. (1 <= w) => NatRepr w -> a) -> a +unitByteSize u k = + case u of + Bytes -> k (knownNat @1) + Words -> k (knownNat @2) + DWords -> k (knownNat @4) + QWords -> k (knownNat @8) + V128s -> k (knownNat @16) + V256s -> k (knownNat @32) + +getElf :: FilePath -> IO (Elf.ElfHeaderInfo 32) +getElf path = + do bs <- BS.readFile path + case Elf.decodeElfHeaderInfo bs of + Right (Elf.SomeElf hdr) + | Elf.ELFCLASS32 <- Elf.headerClass (Elf.header hdr) -> pure hdr + | otherwise -> throwAArch32 "64-bit ELF format" + Left _ -> throwAArch32 "Invalid ELF header" + + +getRelevant :: Elf.ElfHeaderInfo 32 -> IO RelevantElf +getRelevant elf = + case (Macaw.memoryForElf opts elf, Macaw.memoryForElfAllSymbols opts elf) of + (Left err, _) -> throwAArch32 err + (_, Left err) -> throwAArch32 err + (Right (mem, faddrs, _warnings, _errs), Right (_, addrs, _, _)) -> + do let toEntry msym = (Macaw.memSymbolStart msym, Macaw.memSymbolName msym) + return RelevantElf { memory = mem + , funSymMap = Map.fromList (map toEntry faddrs) + , symMap = Map.fromList (map toEntry addrs) + } + + where + opts = Macaw.LoadOptions + { Macaw.loadOffset = Just 0 + } + +posFn :: Macaw.MemSegmentOff 32 -> W4.Position +posFn = W4.OtherPos . Text.pack . show + +findSymbols :: Macaw.AddrSymMap 32 -> ByteString -> [Macaw.MemSegmentOff 32] +findSymbols addrs nm = Map.findWithDefault [] nm invertedMap + where + invertedMap = Map.fromListWith (++) [ (y,[x]) | (x,y) <- Map.toList addrs ] + +loadGlobal :: + RelevantElf -> + (ByteString, Integer, Unit) -> + IO [(String, Integer, Unit, [Integer])] +loadGlobal elf (nm,n,u) = + case findSymbols (symMap elf) nm of + [] -> do print $ symMap elf + err "Global not found" + _ -> mapM loadLoc (findSymbols (symMap elf) nm) + where + mem = memory elf + sname = BSC.unpack nm + + readOne a = case u of + Bytes -> check (Macaw.readWord8 mem a) + Words -> check (Macaw.readWord16le mem a) + DWords -> check (Macaw.readWord32le mem a) + QWords -> check (Macaw.readWord64le mem a) + _ -> err ("unsuported global size: " ++ show u) + + nextAddr = Macaw.incAddr $ fromIntegral (unitByteSize u natValue :: Natural) + + addrsFor o = Prelude.take (fromIntegral n) (iterate nextAddr o) + + check :: (Show b, Integral a) => Either b a -> IO Integer + check res = case res of + Left e -> err (show e) + Right a -> return (fromIntegral a) + + + loadLoc off = do let start = Macaw.segoffAddr off + a = Macaw.memWordToUnsigned (Macaw.addrOffset start) + is <- mapM readOne (addrsFor start) + return (sname, a, u, is) + + err :: [Char] -> IO a + err xs = fail $ unlines + [ "Failed to load global." + , "*** Global: " ++ show nm + , "*** Error: " ++ xs + ] + +freshVal :: + Sym -> C.TypeRepr t -> Bool {- ptrOK ?-}-> String -> IO (C.RegValue Sym t) +freshVal sym t ptrOk nm = + case t of + C.BoolRepr -> do + sn <- symName nm + W4.freshConstant sym sn C.BaseBoolRepr + C.StructRepr tps -> + traverseWithIndex (\idx repr -> C.RV <$> freshVal sym repr True (nm ++ "_field_" ++ show idx)) tps + C.LLVM.LLVMPointerRepr w + | ptrOk, Just Refl <- testEquality w (knownNat @64) -> do + sn_base <- symName (nm ++ "_base") + sn_off <- symName (nm ++ "_off") + base <- W4.freshNat sym sn_base + off <- W4.freshConstant sym sn_off (C.BaseBVRepr w) + return (C.LLVM.LLVMPointer base off) + | otherwise -> do + sn <- symName nm + base <- W4.natLit sym 0 + off <- W4.freshConstant sym sn (C.BaseBVRepr w) + return (C.LLVM.LLVMPointer base off) + it -> fail ("[freshVal] Unexpected type repr: " ++ show it) + + where + symName s = + case W4.userSymbol ("macaw_" ++ s) of + Left err -> error ("Invalid symbol name " ++ show s ++ ": " ++ show err) + Right a -> return a + +freshRegister :: Sym -> Index ctx tp -> C.TypeRepr tp -> IO (C.RegValue' Sym tp) +freshRegister sym idx repr = C.RV <$> freshVal sym repr True ("reg" ++ show idx) + +mkGlobalMap :: + C.LLVM.HasLLVMAnn Sym => + Map.Map Macaw.RegionIndex Ptr -> + Macaw.GlobalMap Sym C.LLVM.Mem 32 +mkGlobalMap rmap sym mem region off = + mapConcreteRegion <|> passThroughConcreteRegion <|> mapSymbolicRegion + where + mapConcreteRegion = maybe mzero id (addOffset <$> thisRegion) + thisRegion = join (findRegion <$> W4.asNat region) + findRegion r = Map.lookup (fromIntegral r) rmap + addOffset p = C.LLVM.doPtrAddOffset sym mem p off + where ?ptrWidth = knownNat + passThroughConcreteRegion = + case W4.asNat region of + Nothing -> mzero + Just _ -> return (C.LLVM.LLVMPointer region off) + -- If the symbolic nat is (symbolically) equal to any of the entries in the + -- rmap, we need to do the translation; otherwise, we pass it through + mapSymbolicRegion = foldlM muxSymbolicRegion (C.LLVM.LLVMPointer region off) (Map.toList rmap) + muxSymbolicRegion others (regionNum, basePtr) = do + thisRegionNat <- W4.natLit sym (fromIntegral regionNum) + isEqRegion <- W4.natEq sym thisRegionNat region + adjustedPtr <- addOffset basePtr + C.LLVM.muxLLVMPtr sym isEqRegion adjustedPtr others + +data Goal = Goal + { gAssumes :: [Term] + , gShows :: Term + , gLoc :: W4.ProgramLoc + , gMessage :: C.SimErrorReason + } + +gGoal :: SharedContext -> Goal -> IO Prop +gGoal sc g0 = predicateToProp sc Universal [] =<< go (gAssumes g) + where + g = g0 { gAssumes = mapMaybe skip (gAssumes g0) } + + _shG = do putStrLn "Assuming:" + mapM_ _shT (gAssumes g) + putStrLn "Shows:" + _shT (gShows g) + + + _shT t = putStrLn (" " ++ showTerm t) + + skip a = case asBool a of + Just True -> Nothing + _ -> Just a + + go xs = case xs of + [] -> return (gShows g) + a : as -> scImplies sc a =<< go as + +getGoals :: Sym -> IO [Goal] +getGoals sym = + do obls <- C.proofGoalsToList <$> C.getProofObligations sym + mapM toGoal obls + where + toGoal (C.ProofGoal asmps g) = + do as <- mapM (C.toSC sym) (toListOf (folded . C.labeledPred) asmps) + p <- C.toSC sym (g ^. C.labeledPred) + let C.SimError loc msg = g^.C.labeledPredMsg + return Goal { gAssumes = as + , gShows = p + , gLoc = loc + , gMessage = msg + } + +newtype AArch32Sim a = AArch32Sim { unAArch32Sim :: StateT AArch32State IO a } + deriving (Functor, Applicative, Monad, MonadIO, MonadState AArch32State, MonadThrow) + +data AArch32State = AArch32State + { _aarch32Sym :: Sym + , _aarch32Options :: Options + , _aarch32SharedContext :: SharedContext + , _aarch32CrucibleContext :: LLVMCrucibleContext LLVMArch + , _aarch32ElfSymtab :: Elf.Symtab 32 + , _aarch32RelevantElf :: RelevantElf + , _aarch32MethodSpec :: MS.CrucibleMethodSpecIR LLVM + , _aarch32Mem :: Mem + , _aarch32Regs :: Regs + , _aarch32GlobalBase :: Ptr + } +makeLenses ''AArch32State + +runAArch32Sim :: AArch32State -> AArch32Sim a -> IO (a, AArch32State) +runAArch32Sim st m = runStateT (unAArch32Sim m) st + +setReg :: + (MonadIO m, MonadThrow m) => + Register -> + C.RegValue Sym (C.LLVM.LLVMPointerType 32) -> + Regs -> + m Regs +setReg reg val regs = pure $ Macaw.AArch32.updateReg reg (C.RV . const val) regs + +getReg :: + (MonadIO m, MonadThrow m) => + Register -> + Regs -> + m (C.RegValue Sym (C.LLVM.LLVMPointerType 32)) +getReg reg regs = case Macaw.AArch32.lookupReg reg regs of C.RV val -> pure val + +------------------------------------------------------------------------------- +-- ** Entrypoint + +llvm_verify_aarch32 :: + Some LLVMModule {- ^ Module to associate with method spec -} -> + FilePath {- ^ Path to ELF file -} -> + String {- ^ Function's symbol in ELF file -} -> + [(String, Integer)] {- ^ Global variable symbol names and sizes (in bytes) -} -> + Bool {- ^ Whether to enable path satisfiability checking -} -> + LLVMCrucibleSetupM () {- ^ Specification to verify against -} -> + ProofScript SatResult {- ^ Tactic used to use when discharging goals -} -> + TopLevel (SomeLLVM MS.CrucibleMethodSpecIR) +llvm_verify_aarch32 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat setup tactic + | Just Refl <- testEquality (C.LLVM.X86Repr $ knownNat @32) . C.LLVM.llvmArch $ modTrans llvmModule ^. C.LLVM.transContext = do + let ?ptrWidth = knownNat @32 + let ?recordLLVMAnnotation = \_ _ -> return () + sc <- getSharedContext + opts <- getOptions + basic_ss <- getBasicSS + sym <- liftIO $ C.newSAWCoreBackend W4.FloatRealRepr sc globalNonceGenerator + halloc <- getHandleAlloc + let mvar = C.LLVM.llvmMemVar . view C.LLVM.transContext $ modTrans llvmModule + sfs <- liftIO $ Macaw.newSymFuns sym + + (C.SomeCFG cfg, elf, relf, addr, cfgs) <- liftIO $ buildCFG opts halloc path nm + liftIO . print $ cfg + addrInt <- if Macaw.segmentBase (Macaw.segoffSegment addr) == 0 + then pure . toInteger $ Macaw.segmentOffset (Macaw.segoffSegment addr) + Macaw.segoffOffset addr + else fail $ mconcat ["Address of \"", nm, "\" is not an absolute address"] + let maxAddr = addrInt + toInteger (Macaw.segmentSize $ Macaw.segoffSegment addr) + + let + cc :: LLVMCrucibleContext x + cc = LLVMCrucibleContext + { _ccLLVMModule = llvmModule + , _ccBackend = sym + , _ccBasicSS = basic_ss + + -- It's unpleasant that we need to do this to use resolveSetupVal. + , _ccLLVMSimContext = error "Attempted to access ccLLVMSimContext" + , _ccLLVMGlobals = error "Attempted to access ccLLVMGlobals" + } + + liftIO . printOutLn opts Info $ mconcat + [ "Simulating function \"" + , nm + , "\" (at address " + , show addr + , ")" + ] + + liftIO $ printOutLn opts Info "Examining specification to determine preconditions" + methodSpec <- buildMethodSpec llvmModule nm (show addr) checkSat setup + let ?lc = modTrans llvmModule ^. C.LLVM.transContext . C.LLVM.llvmTypeCtx + + liftIO $ printOutLn opts Info "foo" + + emptyState <- liftIO $ initialState sym opts sc cc elf relf methodSpec globsyms maxAddr + liftIO $ printOutLn opts Info "bar" + (env, preState) <- liftIO . runAArch32Sim emptyState $ setupMemory globsyms + liftIO $ printOutLn opts Info "baz" + + let + funcLookup = Macaw.LookupFunctionHandle $ \st _mem regs -> do + C.LLVM.LLVMPointer _base off <- getReg Macaw.ip_reg regs + case BV.asUnsigned <$> W4.asBV off of + Nothing -> fail $ mconcat + [ "Attempted to call a function with non-concrete address " + , show $ W4.ppExpr off + ] + Just funcAddr -> do + case Macaw.resolveRegionOff (memory relf) 0 $ fromIntegral funcAddr of + Nothing -> fail $ mconcat + [ "Failed to resolve function address " + , show $ W4.ppExpr off + ] + Just funcAddrOff -> do + case Map.lookup funcAddrOff cfgs of + Just (C.SomeCFG funcCFG) -> + pure + ( C.cfgHandle funcCFG + , st & C.stateContext . C.functionBindings + %~ C.insertHandleMap (C.cfgHandle funcCFG) (C.UseCFG funcCFG $ C.postdomInfo funcCFG) + ) + Nothing -> fail $ mconcat + [ "Unable to find CFG for function at address " + , show $ W4.ppExpr off + ] + noExtraValidityPred _ _ _ _ = return Nothing + ctx :: C.SimContext (Macaw.MacawSimulatorState Sym) Sym (Macaw.MacawExt Macaw.ARM) + ctx = C.SimContext + { C._ctxSymInterface = sym + , C.ctxSolverProof = id + , C.ctxIntrinsicTypes = C.LLVM.llvmIntrinsicTypes + , C.simHandleAllocator = halloc + , C.printHandle = stdout + , C.extensionImpl = + Macaw.macawExtensions (Macaw.aarch32MacawEvalFn sfs) mvar + (mkGlobalMap . Map.singleton 0 $ preState ^. aarch32GlobalBase) + funcLookup noExtraValidityPred + , C._functionBindings = C.insertHandleMap (C.cfgHandle cfg) (C.UseCFG cfg $ C.postdomInfo cfg) C.emptyHandleMap + , C._cruciblePersonality = Macaw.MacawSimulatorState + , C._profilingMetrics = Map.empty + } + globals = C.insertGlobal mvar (preState ^. aarch32Mem) C.emptyGlobals + macawStructRepr = C.StructRepr $ Macaw.crucArchRegTypes Macaw.aarch32MacawSymbolicFns + initial = C.InitialState ctx globals C.defaultAbortHandler macawStructRepr + $ C.runOverrideSim macawStructRepr + $ Macaw.crucGenArchConstraints Macaw.aarch32MacawSymbolicFns + $ do + r <- C.callCFG cfg . C.RegMap . singleton . C.RegEntry macawStructRepr $ preState ^. aarch32Regs + globals' <- C.readGlobals + mem' <- C.readGlobal mvar + let finalState = preState + { _aarch32Mem = mem' + , _aarch32Regs = C.regValue r + , _aarch32CrucibleContext = cc & ccLLVMGlobals .~ globals' + } + liftIO $ printOutLn opts Info + "Examining specification to determine postconditions" + liftIO . void . runAArch32Sim finalState $ assertPost globals' env (preState ^. aarch32Mem) (preState ^. aarch32Regs) + pure $ C.regValue r + + liftIO $ printOutLn opts Info "Simulating function" + + psatf <- + if checkSat then + do f <- liftIO (C.pathSatisfiabilityFeature sym (C.considerSatisfiability sym)) + pure [C.genericToExecutionFeature f] + else + pure [] + + let execFeatures = psatf + + liftIO $ C.executeCrucible execFeatures initial >>= \case + C.FinishedResult{} -> pure () + C.AbortedResult{} -> printOutLn opts Warn "Warning: function never returns" + C.TimeoutResult{} -> fail "Execution timed out" + + stats <- checkGoals sym opts sc tactic + + returnProof $ SomeLLVM (methodSpec & MS.csSolverStats .~ stats) + | otherwise = fail "LLVM module must be AArch32" + +-------------------------------------------------------------------------------- +-- ** Computing the CFG + +-- | Load the given ELF file and use Macaw to construct a Crucible CFG. +buildCFG :: + Options -> + C.HandleAllocator -> + String {- ^ Path to ELF file -} -> + String {- ^ Function's symbol in ELF file -} -> + IO ( C.SomeCFG + (Macaw.MacawExt Macaw.ARM) + (EmptyCtx ::> Macaw.ArchRegStruct Macaw.ARM) + (Macaw.ArchRegStruct Macaw.ARM) + , Elf.ElfHeaderInfo 32 + , RelevantElf + , Macaw.MemSegmentOff 32 + , Map + (Macaw.MemSegmentOff 32) + (C.SomeCFG + (Macaw.MacawExt Macaw.ARM) + (EmptyCtx ::> Macaw.ArchRegStruct Macaw.ARM) + (Macaw.ArchRegStruct Macaw.ARM)) + ) +buildCFG opts halloc path nm = do + printOutLn opts Info $ mconcat ["Finding symbol for \"", nm, "\""] + elf <- getElf path + relf <- getRelevant elf + (addr :: Macaw.MemSegmentOff 32) <- + case findSymbols (symMap relf) . encodeUtf8 $ Text.pack nm of + (addr:_) -> pure addr + _ -> fail $ mconcat ["Could not find symbol \"", nm, "\""] + printOutLn opts Info $ mconcat ["Found symbol at address ", show addr, ", building CFG"] + let + initialDiscoveryState = + Macaw.emptyDiscoveryState (memory relf) (funSymMap relf) Macaw.arm_linux_info + -- "inline" any function addresses that we happen to jump to + & Macaw.trustedFunctionEntryPoints .~ Map.empty + finalState = Macaw.cfgFromAddrsAndState initialDiscoveryState [addr] [] + finfos = finalState ^. Macaw.funInfo + cfgs <- forM finfos $ \(Some finfo) -> + Macaw.mkFunCFG Macaw.aarch32MacawSymbolicFns halloc + (W4.functionNameFromText . decodeUtf8 $ Macaw.discoveredFunName finfo) + posFn finfo + + case Map.lookup addr cfgs of + Nothing -> throwAArch32 $ "Unable to discover CFG from address " <> show addr + Just scfg -> pure (scfg, elf, relf, addr, cfgs) + +-------------------------------------------------------------------------------- +-- ** Computing the specification + +-- | Construct the method spec like we normally would in llvm_verify. +-- Unlike in llvm_verify, we can't reuse the simulator state (due to the +-- different memory layout / RegMap). +buildMethodSpec :: + LLVMModule LLVMArch -> + String {- ^ Name of method -} -> + String {- ^ Source location for method spec (here, we use the address) -} -> + Bool {- ^ check sat -} -> + LLVMCrucibleSetupM () -> + TopLevel (MS.CrucibleMethodSpecIR LLVM) +buildMethodSpec lm nm loc checkSat setup = + setupLLVMCrucibleContext checkSat lm $ \cc -> do + let methodId = LLVMMethodId nm Nothing + let programLoc = + W4.mkProgramLoc (W4.functionNameFromText $ Text.pack nm) + . W4.OtherPos $ Text.pack loc + let lc = modTrans lm ^. C.LLVM.transContext . C.LLVM.llvmTypeCtx + opts <- getOptions + (args, ret) <- case llvmSignature opts lm nm of + Left err -> fail $ mconcat ["Could not find declaration for \"", nm, "\": ", err] + Right x -> pure x + (mtargs, mtret) <- case (,) <$> mapM (llvmTypeToMemType lc) args <*> mapM (llvmTypeToMemType lc) ret of + Left err -> fail err + Right x -> pure x + let initialMethodSpec = MS.makeCrucibleMethodSpecIR @LLVM + methodId mtargs mtret programLoc lm + view Setup.csMethodSpec <$> execStateT (runLLVMCrucibleSetupM setup) + (Setup.makeCrucibleSetupState cc initialMethodSpec) + +llvmTypeToMemType :: + C.LLVM.TypeContext -> + LLVM.Type -> + Either String C.LLVM.MemType +llvmTypeToMemType lc t = let ?lc = lc in C.LLVM.liftMemType t + +-- | Find a function declaration in the LLVM AST and return its signature. +llvmSignature :: + Options -> + LLVMModule LLVMArch -> + String -> + Either String ([LLVM.Type], Maybe LLVM.Type) +llvmSignature opts llvmModule nm = + case findDecl (modAST llvmModule) nm of + Left err -> case findDefMaybeStatic (modAST llvmModule) nm of + Left _ -> Left $ displayVerifExceptionOpts opts err + Right defs -> pure + ( LLVM.typedType <$> LLVM.defArgs (NE.head defs) + , case LLVM.defRetType $ NE.head defs of + LLVM.PrimType LLVM.Void -> Nothing + x -> Just x + ) + Right decl -> pure + ( LLVM.decArgs decl + , case LLVM.decRetType decl of + LLVM.PrimType LLVM.Void -> Nothing + x -> Just x + ) + +-------------------------------------------------------------------------------- +-- ** Building the initial state + +initialState :: + AArch32Constraints => + Sym -> + Options -> + SharedContext -> + LLVMCrucibleContext LLVMArch -> + Elf.ElfHeaderInfo 32 -> + RelevantElf -> + MS.CrucibleMethodSpecIR LLVM -> + [(String, Integer)] {- ^ Global variable symbol names and sizes (in bytes) -} -> + Integer {- ^ Minimum size of the global allocation (here, the end of the .text segment -} -> + IO AArch32State +initialState sym opts sc cc elf relf ms globs maxAddr = do + emptyMem <- C.LLVM.emptyMem C.LLVM.LittleEndian + emptyRegs <- traverseWithIndex (freshRegister sym) C.knownRepr + symTab <- case Elf.decodeHeaderSymtab elf of + Nothing -> throwAArch32 "Elf file has no symbol table" + Just (Left _err) -> throwAArch32 "Failed to decode symbol table" + Just (Right st) -> pure st + let + align = C.LLVM.exponentToAlignment 4 + allocGlobalEnd :: MS.AllocGlobal LLVM -> Integer + allocGlobalEnd (LLVMAllocGlobal _ (LLVM.Symbol nm)) = globalEnd nm + globalEnd :: String -> Integer + globalEnd nm = maybe 0 (\entry -> fromIntegral $ Elf.steValue entry + Elf.steSize entry) $ + (Vector.!? 0) + . Vector.filter (\e -> Elf.steName e == encodeUtf8 (Text.pack nm)) + $ Elf.symtabEntries symTab + sz <- W4.bvLit sym knownNat . BV.mkBV knownNat . maximum $ mconcat + [ [maxAddr, globalEnd "_end"] + , globalEnd . fst <$> globs + , allocGlobalEnd <$> ms ^. MS.csGlobalAllocs + ] + (base, mem) <- C.LLVM.doMalloc sym C.LLVM.GlobalAlloc C.LLVM.Immutable + "globals" emptyMem sz align + pure $ AArch32State + { _aarch32Sym = sym + , _aarch32Options = opts + , _aarch32SharedContext = sc + , _aarch32CrucibleContext = cc + , _aarch32ElfSymtab = symTab + , _aarch32RelevantElf = relf + , _aarch32MethodSpec = ms + , _aarch32Mem = mem + , _aarch32Regs = emptyRegs + , _aarch32GlobalBase = base + } + +-------------------------------------------------------------------------------- +-- ** Precondition + +-- | Given the method spec, build the initial memory, register map, and global map. +setupMemory :: + AArch32Constraints => + [(String, Integer)] {- ^ Global variable symbol names and sizes (in bytes) -} -> + AArch32Sim (Map MS.AllocIndex Ptr) +setupMemory globsyms = do + setupGlobals globsyms + + liftIO $ putStrLn "1" + + -- Allocate a reasonable amount of stack (4 KiB + 1 qword for IP) + allocateStack 4096 + + liftIO $ putStrLn "2" + + ms <- use aarch32MethodSpec + + let + tyenv = ms ^. MS.csPreState . MS.csAllocs + nameEnv = MS.csTypeNames ms + + env <- foldlM assumeAllocation Map.empty . Map.assocs $ tyenv + + liftIO $ putStrLn "3" + + mapM_ (assumePointsTo env tyenv nameEnv) $ ms ^. MS.csPreState . MS.csPointsTos + + liftIO $ putStrLn "4" + + setArgs env tyenv nameEnv . fmap snd . Map.elems $ ms ^. MS.csArgBindings + + liftIO $ putStrLn "5" + + pure env + +-- | Given an alist of symbol names and sizes (in bytes), allocate space and copy +-- the corresponding globals from the Macaw memory to the Crucible LLVM memory model. +setupGlobals :: + AArch32Constraints => + [(String, Integer)] {- ^ Global variable symbol names and sizes (in bytes) -} -> + AArch32Sim () +setupGlobals globsyms = do + sym <- use aarch32Sym + mem <- use aarch32Mem + relf <- use aarch32RelevantElf + base <- use aarch32GlobalBase + let + readInitialGlobal :: (String, Integer) -> IO [(String, Integer, [Integer])] + readInitialGlobal (nm, sz) = do + res <- loadGlobal relf (encodeUtf8 $ Text.pack nm, sz, Bytes) + pure $ (\(name, addr, _unit, bytes) -> (name, addr, bytes)) <$> res + convertByte :: Integer -> IO (C.LLVM.LLVMVal Sym) + convertByte byte = + C.LLVM.LLVMValInt <$> W4.natLit sym 0 <*> W4.bvLit sym (knownNat @8) (BV.mkBV knownNat byte) + writeGlobal :: Mem -> (String, Integer, [Integer]) -> IO Mem + writeGlobal m (_nm, addr, bytes) = do + ptr <- C.LLVM.doPtrAddOffset sym m base =<< W4.bvLit sym knownNat (BV.mkBV knownNat addr) + v <- Vector.fromList <$> mapM convertByte bytes + let st = C.LLVM.arrayType (fromIntegral $ length bytes) $ C.LLVM.bitvectorType 1 + C.LLVM.storeConstRaw sym m ptr st C.LLVM.noAlignment + $ C.LLVM.LLVMValArray (C.LLVM.bitvectorType 1) v + globs <- liftIO $ mconcat <$> mapM readInitialGlobal globsyms + mem' <- liftIO $ foldlM writeGlobal mem globs + aarch32Mem .= mem' + +-- | Allocate memory for the stack, and pushes a fresh pointer as the return +-- address. +allocateStack :: + AArch32Constraints => + Integer {- ^ Stack size in bytes -} -> + AArch32Sim () +allocateStack szInt = do + sym <- use aarch32Sym + mem <- use aarch32Mem + regs <- use aarch32Regs + let align = C.LLVM.exponentToAlignment 4 + sz <- liftIO $ W4.bvLit sym knownNat $ BV.mkBV knownNat $ szInt + 8 + (base, mem') <- liftIO $ C.LLVM.doMalloc sym C.LLVM.HeapAlloc C.LLVM.Mutable + "stack_alloc" mem sz align + sn <- case W4.userSymbol "stack" of + Left err -> throwAArch32 $ "Invalid symbol for stack: " <> show err + Right sn -> pure sn + aarch32Mem .= mem' + finalRegs <- setReg (Macaw.ARMGlobalBV (ASL.knownGlobalRef @"_R13")) base regs + aarch32Regs .= finalRegs + +-- | Process an llvm_alloc statement, allocating the requested memory and +-- associating a pointer to that memory with the appropriate index. +assumeAllocation :: + AArch32Constraints => + Map MS.AllocIndex Ptr -> + (MS.AllocIndex, LLVMAllocSpec) {- ^ llvm_alloc statement -} -> + AArch32Sim (Map MS.AllocIndex Ptr) +assumeAllocation env (i, LLVMAllocSpec mut _memTy align sz loc False) = do + cc <- use aarch32CrucibleContext + sym <- use aarch32Sym + mem <- use aarch32Mem + sz' <- liftIO $ resolveSAWSymBV cc knownNat sz + (ptr, mem') <- liftIO $ C.LLVM.doMalloc sym C.LLVM.HeapAlloc mut + (show $ W4.plSourceLoc loc) mem sz' align + aarch32Mem .= mem' + pure $ Map.insert i ptr env +assumeAllocation env _ = pure env + -- no allocation is done for llvm_fresh_pointer + -- TODO: support llvm_fresh_pointer in x86 verification + +-- | Process an llvm_points_to statement, writing some SetupValue to a pointer. +assumePointsTo :: + AArch32Constraints => + Map MS.AllocIndex Ptr {- ^ Associates each AllocIndex with the corresponding allocation -} -> + Map MS.AllocIndex LLVMAllocSpec {- ^ Associates each AllocIndex with its specification -} -> + Map MS.AllocIndex C.LLVM.Ident {- ^ Associates each AllocIndex with its name -} -> + LLVMPointsTo LLVMArch {- ^ llvm_points_to statement from the precondition -} -> + AArch32Sim () +assumePointsTo env tyenv nameEnv (LLVMPointsTo _ cond tptr tptval) = do + when (isJust cond) $ throwAArch32 "unsupported x86_64 command: llvm_conditional_points_to" + tval <- checkConcreteSizePointsToValue tptval + sym <- use aarch32Sym + cc <- use aarch32CrucibleContext + mem <- use aarch32Mem + ptr <- resolvePtrSetupValue env tyenv tptr + val <- liftIO $ resolveSetupVal cc mem env tyenv Map.empty tval + storTy <- liftIO $ C.LLVM.toStorableType =<< typeOfSetupValue cc tyenv nameEnv tval + mem' <- liftIO $ C.LLVM.storeConstRaw sym mem ptr storTy C.LLVM.noAlignment val + aarch32Mem .= mem' + +resolvePtrSetupValue :: + AArch32Constraints => + Map MS.AllocIndex Ptr -> + Map MS.AllocIndex LLVMAllocSpec -> + MS.SetupValue LLVM -> + AArch32Sim Ptr +resolvePtrSetupValue env tyenv tptr = do + sym <- use aarch32Sym + cc <- use aarch32CrucibleContext + mem <- use aarch32Mem + symTab <- use aarch32ElfSymtab + base <- use aarch32GlobalBase + case tptr of + MS.SetupGlobal () nm -> case + (Vector.!? 0) + . Vector.filter (\e -> Elf.steName e == encodeUtf8 (Text.pack nm)) + $ Elf.symtabEntries symTab of + Nothing -> throwAArch32 $ mconcat ["Global symbol \"", nm, "\" not found"] + Just entry -> do + let addr = fromIntegral $ Elf.steValue entry + liftIO $ C.LLVM.doPtrAddOffset sym mem base =<< W4.bvLit sym knownNat (BV.mkBV knownNat addr) + _ -> liftIO $ C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @32) + =<< resolveSetupVal cc mem env tyenv Map.empty tptr + +checkConcreteSizePointsToValue :: LLVMPointsToValue LLVMArch -> AArch32Sim (MS.SetupValue LLVM) +checkConcreteSizePointsToValue = \case + ConcreteSizeValue val -> return val + SymbolicSizeValue{} -> throwAArch32 "unsupported x86_64 command: llvm_points_to_array_prefix" + +-- | Write each SetupValue passed to llvm_execute_func to the appropriate +-- x86_64 register from the calling convention. +setArgs :: + AArch32Constraints => + Map MS.AllocIndex Ptr {- ^ Associates each AllocIndex with the corresponding allocation -} -> + Map MS.AllocIndex LLVMAllocSpec {- ^ Associates each AllocIndex with its specification -} -> + Map MS.AllocIndex C.LLVM.Ident {- ^ Associates each AllocIndex with its name -} -> + [MS.SetupValue LLVM] {- ^ Arguments passed to llvm_execute_func -} -> + AArch32Sim () +setArgs env tyenv nameEnv args + | length args > length argRegs = throwAArch32 "More arguments than would fit into general-purpose registers" + | otherwise = do + sym <- use aarch32Sym + cc <- use aarch32CrucibleContext + mem <- use aarch32Mem + let + setRegSetupValue rs (reg, sval) = typeOfSetupValue cc tyenv nameEnv sval >>= \ty -> + case ty of + C.LLVM.PtrType _ -> do + val <- C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @32) + =<< resolveSetupVal cc mem env tyenv nameEnv sval + setReg reg val rs + C.LLVM.IntType 32 -> do + val <- C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @32) + =<< resolveSetupVal cc mem env tyenv nameEnv sval + setReg reg val rs + C.LLVM.IntType _ -> do + C.LLVM.LLVMValInt base off <- resolveSetupVal cc mem env tyenv nameEnv sval + case testLeq (incNat $ W4.bvWidth off) (knownNat @32) of + Nothing -> fail "Argument bitvector does not fit in a single general-purpose register" + Just LeqProof -> do + off' <- W4.bvZext sym (knownNat @32) off + val <- C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @32) + $ C.LLVM.LLVMValInt base off' + setReg reg val rs + _ -> fail "Argument does not fit into a single general-purpose register" + regs <- use aarch32Regs + newRegs <- liftIO . foldlM setRegSetupValue regs $ zip argRegs args + aarch32Regs .= newRegs + where + argRegs = + [ Macaw.ARMGlobalBV (ASL.knownGlobalRef @"_R0") + , Macaw.ARMGlobalBV (ASL.knownGlobalRef @"_R1") + , Macaw.ARMGlobalBV (ASL.knownGlobalRef @"_R2") + , Macaw.ARMGlobalBV (ASL.knownGlobalRef @"_R3") + ] + +-------------------------------------------------------------------------------- +-- ** Postcondition + +-- | Assert the postcondition for the spec, given the final memory and register map. +assertPost :: + AArch32Constraints => + C.SymGlobalState Sym -> + Map MS.AllocIndex Ptr -> + Mem {- ^ The state of memory before simulation -} -> + Regs {- ^ The state of the registers before simulation -} -> + AArch32Sim () +assertPost globals env premem preregs = do + sym <- use aarch32Sym + opts <- use aarch32Options + sc <- use aarch32SharedContext + cc <- use aarch32CrucibleContext + ms <- use aarch32MethodSpec + postregs <- use aarch32Regs + let + tyenv = ms ^. MS.csPreState . MS.csAllocs + nameEnv = MS.csTypeNames ms + + expectedIP <- getReg (Macaw.ARMGlobalBV (ASL.knownGlobalRef @"_R14")) preregs + actualIP <- getReg Macaw.ip_reg postregs + correctRetAddr <- liftIO $ C.LLVM.ptrEq sym C.LLVM.PtrWidth actualIP expectedIP + liftIO . C.addAssertion sym . C.LabeledPred correctRetAddr . C.SimError W4.initializationLoc + $ C.AssertFailureSimError "Instruction pointer not set to return address" "" + + prersp <- getReg (Macaw.ARMGlobalBV (ASL.knownGlobalRef @"_R13")) preregs + postrsp <- getReg (Macaw.ARMGlobalBV (ASL.knownGlobalRef @"_R13")) postregs + correctStack <- liftIO $ C.LLVM.ptrEq sym C.LLVM.PtrWidth prersp postrsp + liftIO $ C.addAssertion sym . C.LabeledPred correctStack . C.SimError W4.initializationLoc + $ C.AssertFailureSimError "Stack not preserved" "" + + returnMatches <- case (ms ^. MS.csRetValue, ms ^. MS.csRet) of + (Just expectedRet, Just retTy) -> do + postRAX <- C.LLVM.ptrToPtrVal <$> getReg (Macaw.ARMGlobalBV (ASL.knownGlobalRef @"_R0")) postregs + case (postRAX, C.LLVM.memTypeBitwidth retTy) of + (C.LLVM.LLVMValInt base off, Just retTyBits) -> do + let + truncateRAX :: forall r. NatRepr r -> AArch32Sim (C.LLVM.LLVMVal Sym) + truncateRAX rsz = + case (testLeq (knownNat @1) rsz, testLeq rsz (W4.bvWidth off)) of + (Just LeqProof, Just LeqProof) -> + case testStrictLeq rsz (W4.bvWidth off) of + Left LeqProof -> do + offTrunc <- liftIO $ W4.bvTrunc sym rsz off + pure $ C.LLVM.LLVMValInt base offTrunc + _ -> pure $ C.LLVM.LLVMValInt base off + _ -> throwAArch32 "Width of return type is zero bits" + postRAXTrunc <- viewSome truncateRAX (mkNatRepr retTyBits) + pure [LO.matchArg opts sc cc ms MS.PostState postRAXTrunc retTy expectedRet] + _ -> throwAArch32 $ "Invalid return type: " <> show (C.LLVM.ppMemType retTy) + _ -> pure [] + + pointsToMatches <- forM (ms ^. MS.csPostState . MS.csPointsTos) + $ assertPointsTo env tyenv nameEnv + + let setupConditionMatches = fmap + (LO.learnSetupCondition opts sc cc ms MS.PostState) + $ ms ^. MS.csPostState . MS.csConditions + + let + initialECs = Map.fromList + [ (ecVarIndex ec, ec) + | tt <- ms ^. MS.csPreState . MS.csFreshVars + , let ec = tecExt tt + ] + initialFree = Set.fromList . fmap (ecVarIndex . tecExt) $ ms ^. MS.csPostState . MS.csFreshVars + + initialTerms <- liftIO $ traverse (scExtCns sc) initialECs + + result <- liftIO + . O.runOverrideMatcher sym globals env initialTerms initialFree (ms ^. MS.csLoc) + . sequence_ $ mconcat + [ returnMatches + , pointsToMatches + , setupConditionMatches + ] + st <- case result of + Left err -> throwAArch32 $ show err + Right (_, st) -> pure st + liftIO . forM_ (view LO.osAsserts st) $ \(W4.LabeledPred p r) -> + C.addAssertion sym $ C.LabeledPred p r + +-- | Assert that a points-to postcondition holds. +assertPointsTo :: + AArch32Constraints => + Map MS.AllocIndex Ptr {- ^ Associates each AllocIndex with the corresponding allocation -} -> + Map MS.AllocIndex LLVMAllocSpec {- ^ Associates each AllocIndex with its specification -} -> + Map MS.AllocIndex C.LLVM.Ident {- ^ Associates each AllocIndex with its name -} -> + LLVMPointsTo LLVMArch {- ^ llvm_points_to statement from the precondition -} -> + AArch32Sim (LLVMOverrideMatcher md ()) +assertPointsTo env tyenv nameEnv (LLVMPointsTo _ cond tptr tptexpected) = do + when (isJust cond) $ throwAArch32 "unsupported x86_64 command: llvm_conditional_points_to" + texpected <- checkConcreteSizePointsToValue tptexpected + sym <- use aarch32Sym + opts <- use aarch32Options + sc <- use aarch32SharedContext + cc <- use aarch32CrucibleContext + ms <- use aarch32MethodSpec + mem <- use aarch32Mem + ptr <- resolvePtrSetupValue env tyenv tptr + memTy <- liftIO $ typeOfSetupValue cc tyenv nameEnv texpected + storTy <- liftIO $ C.LLVM.toStorableType memTy + + actual <- liftIO $ C.LLVM.assertSafe sym =<< C.LLVM.loadRaw sym mem ptr storTy C.LLVM.noAlignment + pure $ LO.matchArg opts sc cc ms MS.PostState actual memTy texpected + +-- | Gather and run the solver on goals from the simulator. +checkGoals :: + Sym -> + Options -> + SharedContext -> + ProofScript SatResult -> + TopLevel SolverStats +checkGoals sym opts sc tactic = do + gs <- liftIO $ getGoals sym + liftIO . printOutLn opts Info $ mconcat + [ "Simulation finished, running solver on " + , show $ length gs + , " goals" + ] + stats <- forM (zip [0..] gs) $ \(n, g) -> do + term <- liftIO $ gGoal sc g + let proofgoal = ProofGoal n "vc" (show $ gMessage g) term + r <- evalStateT tactic $ startProof proofgoal + case r of + Unsat stats -> return stats + SatMulti stats vals -> do + printOutLnTop Info $ unwords ["Subgoal failed:", show $ gMessage g] + printOutLnTop Info (show stats) + printOutLnTop OnlyCounterExamples "----------Counterexample----------" + ppOpts <- sawPPOpts . rwPPOpts <$> getTopLevelRW + case vals of + [] -> printOutLnTop OnlyCounterExamples "<>" + _ -> let showAssignment (name, val) = + mconcat [ " ", name, ": ", show $ ppFirstOrderValue ppOpts val ] + in mapM_ (printOutLnTop OnlyCounterExamples . showAssignment) vals + printOutLnTop OnlyCounterExamples "----------------------------------" + throwTopLevel "Proof failed." + liftIO $ printOutLn opts Info "All goals succeeded" + return (mconcat stats) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 1e71ba018..b84ba4a3b 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -106,6 +106,7 @@ import SAWScript.Crucible.LLVM.Builtins import SAWScript.Crucible.JVM.Builtins import SAWScript.Crucible.MIR.Builtins import SAWScript.Crucible.LLVM.X86 +import SAWScript.Crucible.LLVM.AArch32 import SAWScript.Crucible.LLVM.Boilerplate import SAWScript.Crucible.LLVM.Skeleton.Builtins import SAWScript.Crucible.LLVM.FFI @@ -3820,6 +3821,21 @@ primitives = Map.fromList ,"This is used for path-sat checks, and sat checks when applying overrides." ] + , prim "llvm_verify_aarch32" + "LLVMModule -> String -> String -> [(String, Int)] -> Bool -> LLVMSetup () -> ProofScript SatResult -> TopLevel LLVMSpec" + (pureVal llvm_verify_aarch32) + Experimental + [ "Verify an AArch32 function from an ELF file for use as an override in an" + , "LLVM verification. The first argument specifies the LLVM module" + , "containing the _caller_. The second and third specify the ELF file" + , "name and symbol name of the function to be verifier. The fourth" + , "specifies the names and sizes (in bytes) of global variables to" + , "initialize, and the fifth whether to perform path satisfiability" + , "checking. The last argument is the LLVM specification of the calling" + , "context against which to verify the function. Returns a method spec" + , "that can be used as an override when verifying other LLVM functions." + ] + , prim "llvm_array_value" "[SetupValue] -> SetupValue" (pureVal CIR.anySetupArray)