content: {-# Language GADTs, KindSignatures, DataKinds, ImplicitParams #-}
  {-# Language PatternSynonyms, TypeFamilies, TypeSynonymInstances #-}
  {-# Language TypeApplications #-}
  {-# Language TypeOperators #-}
  {-# Language OverloadedStrings #-}
  {-# Language ExistentialQuantification #-}
  {-# Language Rank2Types #-}
  {-# Language FlexibleContexts #-}
  {-# Language ScopedTypeVariables #-}
  {-# Language ConstraintKinds #-}
  {-# Language PartialTypeSignatures #-}
  {-# Language CPP #-}
  #if __GLASGOW_HASKELL__ >= 806
  {-# Language NoStarIsType #-}
  #endif
  module SAWCentral.X86Spec
    ( Specification(..)
    , SpecType, Pre, Post
    , FunSpec(..)
    , verifyMode
    , overrideMode
    , State(..)
    , Loc(..)
    , V(..)
    , Prop(..)
    , Alloc(..)
    , Area(..)
    , Mode(..)
    , Unit(..)
    , (*.)
    , inMem
    , (===)
    , Opts(..)
    , optsSym
    , KnownType
    , intLit
    , litByte
    , litWord
    , litDWord
    , litQWord
    , litV128
    , litV256
    , area
    , LLVMPointerType
    , Overrides
    , debugPPReg
  
    , Sym
    , freshRegister
  
    -- * Cryptol
    , CryArg(..)
    , cryPre
    , cryCur
    , cryTerm
    , cryConst
    , mkGlobalMap
    ) where
  
  import GHC.TypeLits(KnownNat)
  import GHC.Natural(Natural)
  import Data.Kind(Type)
  import Control.Applicative ( (<|>) )
  import Control.Lens (view, (^.), over)
  import qualified Data.BitVector.Sized as BV
  import Data.List(sortBy)
  import Data.Maybe(catMaybes)
  import Data.Text (Text)
  import qualified Data.Text as Text
  import Data.Map (Map)
  import Data.Proxy(Proxy(..))
  import qualified Data.Map as Map
  import Data.IORef(newIORef,atomicModifyIORef')
  import Data.String
  import Control.Monad (MonadPlus(..), foldM, join, zipWithM)
  import Control.Monad.IO.Class (MonadIO(..))
  
  import Data.Parameterized.NatRepr
  import Data.Parameterized.Classes
  import qualified Data.Parameterized.Context as Ctx
  import qualified Data.Parameterized.Map as MapF
  import Data.Parameterized.Pair
  
  import Data.Foldable(foldlM, toList)
  
  import What4.Interface
            (bvLit,isEq, Pred, notPred, orPred, natEq, freshNat
            , bvUle, truePred, natLit, asNat, andPred, userSymbol, freshConstant )
  import What4.ProgramLoc
  
  import Lang.Crucible.FunctionHandle
  import SAWCentral.Crucible.LLVM.CrucibleLLVM
    ( EndianForm(LittleEndian)
    , MemImpl, doLoad, doPtrAddOffset, emptyMem
    , AllocType(HeapAlloc, GlobalAlloc), Mutability(..), Mem
    , pattern LLVMPointerRepr, doMalloc, storeConstRaw, packMemValue
    , LLVMPointerType, LLVMVal(LLVMValInt)
    , ptrEq, LLVMPtr, ppPtr, llvmPointerView, projectLLVM_bv, llvmPointer_bv
    , muxLLVMPtr
    , bitvectorType
    , Bytes, bytesToInteger, toBytes
    , StorageType
    , noAlignment
    , pattern LLVMPointer
    )
  import qualified Lang.Crucible.LLVM.MemModel as Crucible
  
  import Lang.Crucible.Simulator.SimError(SimErrorReason(AssertFailureSimError))
  import Lang.Crucible.Backend
            ( addAssumption, getProofObligations, goalsToList
            , assert, CrucibleAssumption(..)
            , ProofGoal(..), labeledPredMsg
            , HasSymInterface(backendGetSym)
            , SomeBackend(..), IsSymBackend
            )
  import Lang.Crucible.Simulator.ExecutionTree
  import Lang.Crucible.Simulator.OverrideSim
  import Lang.Crucible.CFG.Common
  import Lang.Crucible.Simulator.RegMap
  
  --import Lang.Crucible.Backend.SAWCore
  --  (bindSAWTerm,sawBackendSharedContext,toSC,SAWCoreBackend)
  import Lang.Crucible.Types
    (TypeRepr(..),BaseTypeRepr(..),BaseToType,CrucibleType)
  
  import SAWCore.SharedTerm
    (Term,scApplyAll,scVector,scBitvector,scAt,scNat)
  import Data.Macaw.Memory(RegionIndex)
  import Data.Macaw.Symbolic
    ( GlobalMap(..), ToCrucibleType, LookupFunctionHandle(..)
    , MacawCrucibleRegTypes, MacawSimulatorState
    )
  import Data.Macaw.Symbolic.Backend ( crucArchRegTypes )
  import Data.Macaw.X86.X86Reg
  import Data.Macaw.X86.Symbolic
       (x86_64MacawSymbolicFns,lookupX86Reg,updateX86Reg)
  import Data.Macaw.X86.ArchTypes(X86_64)
  import qualified Data.Macaw.Types as M
  
  import CryptolSAWCore.CryptolEnv(CryptolEnv(..), lookupIn, getAllIfaceDecls)
  import SAWCoreWhat4.ReturnTrip
  
  import Cryptol.ModuleSystem.Name(Name)
  import Cryptol.ModuleSystem.Interface(ifTySyns)
  import Cryptol.TypeCheck.AST(TySyn(tsDef))
  import Cryptol.TypeCheck.TypePat(aNat)
  import Cryptol.Utils.PP(pp)
  import Cryptol.Utils.Patterns(matchMaybe)
  
  import SAWCentral.Crucible.Common (Sym, sawCoreState)
  
  
  data Specification = Specification
    { specAllocs  :: ![Alloc]
    , specPres    :: ![(String, Prop Pre)]
    , specPosts   :: ![(String, Prop Post)]
  
    , specGlobsRO :: ![ (String, Integer, Unit, [ Integer ]) ]
      -- ^ Read only globals.
  
    , specCalls   :: ![ (String, Integer, Int -> Specification) ]
      -- ^ Specifications for the functions we call.
      -- The integer is the absolute address of the function.
      -- The "Int" counts how many times we called this function so far.
    }
  
  data Unit = Bytes | Words | DWords | QWords | V128s | V256s deriving Show
  
  {- | A specifiction for a function.
  The outer, "Pre", computiation sets up the initial state of the
  computation (i.e., the pre-condition for the function).
  As a result, we return the inital register assignemtn,
  and the post-condition for the function). -}
  data FunSpec =
      NewStyle (CryptolEnv -> IO Specification)
               (State -> IO ())
                -- Debug: Run this to print some stuff at interesting times.
  
  -- | Is this a pre- or post-condition specificiation.
  data {- kind -} SpecType = Pre | Post
  
  -- | We are specifying a pre-condition.
  type Pre  = 'Pre
  
  -- | We are specifying a post-condition.
  type Post = 'Post
  
  
  
  data Opts = Opts
    { optsBackend :: SomeBackend Sym
    , optsMvar :: GlobalVar Mem
    , optsCry :: CryptolEnv
    }
  
  optsWithBackend :: Opts -> (forall bak. IsSymBackend Sym bak => bak -> a) -> a
  optsWithBackend opts k = case optsBackend opts of SomeBackend bak -> k bak
  
  optsSym :: Opts -> Sym
  optsSym opts = optsWithBackend opts backendGetSym
  
  (*.) :: Integer -> Unit -> Bytes
  n *. u = toBytes (fromInteger n * bs)
    where bs = unitByteSize u natValue :: Natural
  
  unitBitSize :: Unit -> (forall w. (1 <= w) => NatRepr w -> a) -> a
  unitBitSize u k = unitByteSize u $ \bits ->
    case leqMulPos (knownNat @8) bits of
      LeqProof -> k (natMultiply (knownNat @8) bits)
  
  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)
  
  
  
  data Mode = RO    -- ^ Starts initialized; cannot write to it
            | RW    -- ^ Starts initialized; can write to it
            | WO    -- ^ Starts uninitialized; can write to it
            deriving (Eq,Show)
  
  data Area = Area
    { areaName :: String
    , areaMode :: Mode
    , areaSize :: (Integer,Unit)
  
    , areaHasPointers :: Bool
      -- ^ Could this area contain pointers
  
    , areaPtr  :: Bytes
      {- ^ The canonical pointer to this area is this many bytes from
      -- the start of the actual object.
      -- When we initialize such an area, we allocate it, then advnace
      -- the pointer by this much, and return *that* as the value of
      -- initialization.
  
      -- When we match such an area, we get the value as it,
      -- but then we have to check that there are this many bytes *before*
      -- the value we got.
      -}
    }
  
  area :: String -> Mode -> Integer -> Unit -> Area
  area n m u s = Area { areaName = n
                    , areaMode = m
                    , areaSize = (u,s)
                    , areaHasPointers = False
                    , areaPtr = 0 *. Bytes
                    }
  
  data Loc :: CrucibleType -> Type where
  
    InMem :: (1 <= w) =>
             NatRepr w                {- Read this much (in bytes) -} ->
             Loc (LLVMPointerType 64) {- Read from this pointer -} ->
             Integer                  {- Starting at this offset in bytes -} ->
             Loc (LLVMPointerType (8*w))
  
    InReg :: X86Reg tp -> Loc (ToCrucibleType tp)
  
  instance Show (Loc t) where
    show x =
      case x of
        InReg r -> show r
        InMem w l o ->
          "[" ++ show l ++ off ++ " |" ++ show (8 * natValue w) ++ "]"
          where off | o < 0     = " - " ++ show (negate o)
                    | o == 0    = ""
                    | otherwise = " + " ++ show o
  
  inMem ::
    (1 <= w, KnownNat w) =>
    Loc (LLVMPointerType 64) ->
    Integer ->
    Unit ->
    Loc (LLVMPointerType (8 * w))
  inMem l n u = InMem knownNat l (bytesToInteger (n *. u))
  
  instance TestEquality Loc where
    testEquality x y = case compareF x y of
                         EQF -> Just Refl
                         _   -> Nothing
  
  -- | Allocation order.  Also used when resolving equalities,
  -- the smallest number is the representative.
  instance OrdF Loc where
    compareF x y =
      case (x,y) of
        (InReg a, InReg b) -> case compareF a b of
                                EQF -> EQF
                                LTF -> LTF
                                GTF -> GTF
  
        (InReg {}, InMem {}) -> LTF
        (InMem {}, InReg {}) -> GTF
        (InMem s a i, InMem t b j) ->
          case compareF a b of
            EQF -> case compare i j of
                     LT -> LTF
                     GT -> GTF
                     EQ -> case compareF s t of
                             LTF -> LTF -- XXX: shouldn't allow?
                             GTF -> GTF -- XXX: shouldn't allow?
                             EQF -> EQF
            LTF -> LTF
            GTF -> GTF
  
  
  
  data Alloc = Loc (LLVMPointerType 64) := Area
  
  allocArea :: Alloc -> Area
  allocArea (_ := a) = a
  
  cmpAlloc :: Alloc -> Alloc -> Ordering
  cmpAlloc (l1 := _) (l2 := _) = case compareF l1 l2 of
                                   LTF -> LT
                                   EQF -> EQ
                                   GTF -> GT
  
  data V :: SpecType -> CrucibleType -> Type where
  
    CryFun ::
      (1 <= w) => NatRepr w -> Text -> [CryArg p] -> V p (LLVMPointerType w)
    -- An opaque Cryptol term; WARNING: type is unchecked
    -- XXX there does not appear to be anything that creates these
  
    IntLit :: (1 <= w) => NatRepr w -> Integer -> V p (LLVMPointerType w)
    -- A literal value
  
    -- The whole location thing needs to be fixed...
  
    Loc    :: Loc t -> V p t
    -- Read the value at the location in the *current* state:
    -- pre or post depending on `p`
  
    PreLoc :: Loc t -> V Post t
    -- Read the location from the pre-condition state.
  
    PreAddPtr ::
      Loc (LLVMPointerType 64) -> Integer -> Unit -> V Post (LLVMPointerType 64)
    -- Add a constant to a pointer from a location in the pre-condition.
  
  
  instance Show (V p t) where
    show val =
      case val of
        CryFun w f xs -> pars (Text.unpack f ++ " " ++ unwords (map show xs) ++ sh w)
        IntLit w x -> pars (show x ++ sh w)
        Loc l     -> show l
        PreLoc l  -> pars ("pre " ++ show l)
        PreAddPtr l i u ->
            pars ("pre &" ++ show l ++ " + " ++ show i ++ " " ++ show u)
  
      where
      pars x = "(" ++ x ++ ")"
      sh w = " : [" ++ show (natValue w) ++ "]"
  
  
  litByte :: Integer -> V p (LLVMPointerType 8)
  litByte = intLit
  
  litWord :: Integer -> V p (LLVMPointerType 16)
  litWord = intLit
  
  litDWord :: Integer -> V p (LLVMPointerType 32)
  litDWord = intLit
  
  litQWord :: Integer -> V p (LLVMPointerType 64)
  litQWord = intLit
  
  litV128 :: Integer -> V p (LLVMPointerType 128)
  litV128 = intLit
  
  litV256 :: Integer -> V p (LLVMPointerType 256)
  litV256 = intLit
  
  intLit :: (1 <= w, KnownNat w) => Integer -> V p (LLVMPointerType w)
  intLit = IntLit knownNat
  
  
  
  data CryArg :: SpecType -> Type where
    CryNat    :: Integer -> CryArg p
    Cry       :: V p (LLVMPointerType w) -> CryArg p
    CryArrCur :: V p (LLVMPointerType 64) -> Integer -> Unit -> CryArg p
    CryArrPre :: V Post (LLVMPointerType 64) -> Integer -> Unit -> CryArg Post
  
  
  instance Show (CryArg p) where
    show x =
      case x of
        Cry v -> show v
        CryNat n -> show n
        CryArrCur p n u -> "[" ++ show p ++ "|" ++ show n ++ " " ++ show u ++ "]"
        CryArrPre p n u ->
          "[pre " ++ show p ++ "|" ++ show n ++ " " ++ show u ++ "]"
  
  cryPre :: Loc (LLVMPointerType w) -> CryArg Post
  cryPre l = Cry (PreLoc l)
  
  cryCur :: Loc (LLVMPointerType w) -> CryArg p
  cryCur l = Cry (Loc l)
  
  
  data Prop :: SpecType -> Type where
    Same    :: TypeRepr t -> V p t -> V p t -> Prop p
    CryProp :: Text -> [ CryArg p ] -> Prop p
    CryPostMem ::
      V Post (LLVMPointerType 64) {- starting here -} ->
      Integer                     {- this many elemnts -} ->
      Unit                        {- of this size -} ->
      Text                        {- are defined by this Cry. func. -} ->
      [CryArg Post]               {- applied to these argumnets -} ->
      Prop Post
  
  type KnownType = KnownRepr TypeRepr
  
  (===) :: KnownType t => V p t -> V p t -> Prop p
  x === y = Same knownRepr x y
  
  locRepr :: Loc t -> TypeRepr t
  locRepr l =
    case l of
      InMem w _ _ -> ptrTy w
      InReg r ->
        case M.typeRepr r of
          M.BVTypeRepr w -> LLVMPointerRepr w
          M.BoolTypeRepr -> BoolRepr
          M.TupleTypeRepr {} -> error $ "[locRepr] Unexpected tuple register"
          M.FloatTypeRepr {} -> error $ "[locRepr] Unexpected float register"
          M.VecTypeRepr {} -> error $ "[locRepr] Unexpected vector register"
  
  --------------------------------------------------------------------------------
  
  data State = State
    { stateMem  :: MemImpl Sym
    , stateRegs :: Ctx.Assignment (RegValue' Sym) (MacawCrucibleRegTypes X86_64)
    }
  
  freshState :: Sym -> IO State
  freshState sym =
    do regs <- Ctx.traverseWithIndex (freshRegister sym) knownRepr
       mem  <- emptyMem LittleEndian
       return State { stateMem = mem, stateRegs = regs }
  
  freshRegister :: Sym -> Ctx.Index ctx tp -> TypeRepr tp -> IO (RegValue' Sym tp)
  freshRegister sym idx repr = RV <$> freshVal sym repr True ("reg" ++ show idx)
  
  freshVal ::
    Sym -> TypeRepr t -> Bool {- ptrOK ?-}-> String -> IO (RegValue Sym t)
  freshVal sym t ptrOk nm =
    case t of
      BoolRepr -> do
        sn <- symName nm
        freshConstant sym sn BaseBoolRepr
      LLVMPointerRepr w
        | ptrOk, Just Refl <- testEquality w (knownNat @64) -> do
            sn_base <- symName (nm ++ "_base")
            sn_off <- symName (nm ++ "_off")
            base <- freshNat sym sn_base
            off <- freshConstant sym sn_off (BaseBVRepr w)
            return (LLVMPointer base off)
        | otherwise -> do
            sn <- symName nm
            base <- natLit sym 0
            off <- freshConstant sym sn (BaseBVRepr w)
            return (LLVMPointer base off)
      it -> fail ("[freshVal] Unexpected type repr: " ++ show it)
  
    where
    symName s =
      case userSymbol ("macaw_" ++ s) of
        Left err -> error ("Invalid symbol name " ++ show s ++ ": " ++ show err)
        Right a -> return a
  
  getLoc :: (?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Loc t -> Opts -> State -> IO (RegValue Sym t)
  getLoc l =
    case l of
  
      InReg r ->
        \_ s -> case lookupX86Reg r (stateRegs s) of
                  Just (RV v) -> return v
                  _           -> fail ("[getLoc] Invalid register: " ++ show r)
  
      InMem w lm n ->
        \opts s -> optsWithBackend opts $ \bak ->
           do obj <- getLoc lm opts s
              let mem = stateMem s
              let ?ptrWidth = knownNat
              loc <- adjustPtr bak mem obj n
              doLoad bak mem loc (llvmBytes w) (locRepr l) noAlignment
  
  ptrTy :: (1 <= w) => NatRepr w -> TypeRepr (LLVMPointerType (8 * w))
  ptrTy wb
    | LeqProof <- leqMulPos (knownNat @8) wb =
          LLVMPointerRepr (natMultiply (knownNat @8) wb)
  
  llvmBytes :: NatRepr w -> StorageType
  llvmBytes w = bitvectorType (toBytes (natValue w))
  
  setLoc :: (?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Loc t -> Opts -> RegValue Sym t -> State -> IO State
  setLoc l =
  
    case l of
      InReg r ->
        \_ v s ->
          case updateX86Reg r (const (RV v)) (stateRegs s) of
            Just rs -> return s { stateRegs = rs }
            Nothing -> fail ("[setLoc] Invalid register: " ++ show r)
  
      InMem w lm n ->
        \opts v s ->
          optsWithBackend opts $ \bak ->
            do let sym = backendGetSym bak
               obj <- getLoc lm opts s
               let mem = stateMem s
               let ?ptrWidth = knownNat
               loc <- adjustPtr bak mem obj n
  
               let lty = llvmBytes w
                   ty  = locRepr l
               val <- packMemValue sym lty ty v
               let alignment = noAlignment -- default to byte-aligned (FIXME, see #338)
               mem1 <- storeConstRaw bak mem loc lty alignment val
  
               return s { stateMem = mem1 }
  
  
  class Eval p where
    type S p
    eval ::
      (?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
      V p t -> Opts -> S p -> IO (RegValue Sym t)
    curState :: f p -> S p -> State
    setCurState :: f p -> State -> S p -> S p
  
  evIntLit :: (1 <= w) => Sym -> NatRepr w -> Integer -> IO (LLVMPtr Sym w)
  evIntLit sym w n = llvmPointer_bv sym =<< bvLit sym w (BV.mkBV w n)
  
  instance Eval Pre where
    type S Pre = State
    eval val =
      case val of
        CryFun w f xs  -> \opts s -> evalCryFun opts s w f xs
        IntLit w n     -> \opts _ -> evIntLit (optsSym opts) w n
        Loc l          -> \opts s -> getLoc l opts s
    curState _ s = s
    setCurState _ s _ = s
  
  instance Eval Post where
    type S Post = (State,State)
    eval val =
      case val of
        CryFun w f xs   -> \opts s         -> evalCryFun opts s w f xs
        IntLit w n      -> \opts _         -> evIntLit (optsSym opts) w n
        Loc l           -> \opts (_,post)  -> getLoc l opts post
        PreLoc l        -> \opts (pre,_)   -> getLoc l opts pre
        PreAddPtr l i u -> \opts (pre,_) ->
          do ptr <- getLoc l opts pre
             optsWithBackend opts $ \bak ->
               adjustPtr bak (stateMem pre) ptr (bytesToInteger (i *. u))
  
    curState _ (_,s) = s
    setCurState _ s (s1,_) = (s1,s)
  
  evalCry ::
    forall p.
    (Eval p, ?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Opts -> CryArg p -> S p -> IO Term
  evalCry opts cry s =
    optsWithBackend opts $ \bak ->
        do let sym = backendGetSym bak
           st <- sawCoreState sym
           let sc = saw_ctx st
           case cry of
             CryNat n -> scNat sc (fromInteger n)
  
             Cry v -> toSC sym st =<< projectLLVM_bv bak =<< eval v opts s
  
             CryArrCur ptr n u ->
               unitByteSize u $ \byteW ->
               do vs <- readArr opts ptr n byteW s (curState (Proxy @p) s)
                  terms <- mapM (\x -> toSC sym st =<< projectLLVM_bv bak x) vs
                  ty <- scBitvector sc (fromIntegral (8 * natValue byteW))
                  scVector sc ty terms
  
             CryArrPre ptr n u ->
               unitByteSize u $ \byteW ->
               do vs <- readArr opts ptr n byteW s (fst s)
                  terms <- mapM (\x -> toSC sym st =<< projectLLVM_bv bak x) vs
                  ty <- scBitvector sc (fromIntegral (8 * natValue byteW))
                  scVector sc ty terms
  
  evalCryFunGen ::
    (Eval p, ?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Opts ->
    S p ->
    BaseTypeRepr t ->
    Text ->
    [CryArg p] ->
    IO (RegValue Sym (BaseToType t))
  evalCryFunGen opts s ty f xs =
    do let sym = optsSym opts
       st <- sawCoreState sym
       ts <- mapM (\x -> evalCry opts x s) xs
       bindSAWTerm sym st ty =<< cryTerm opts f ts
  
  
  -- | Cryptol function that returns a list of bit-vectors.
  evalCryFunArr ::
    (1 <= w, Eval p, ?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Opts ->
    S p ->
    Integer ->
    NatRepr w ->
    Text ->
    [CryArg p] ->
    IO [ LLVMPtr Sym w ]
  evalCryFunArr opts s n w f xs =
    do term <- cryTerm opts f =<< mapM (\x -> evalCry opts x s) xs
       let sym = optsSym opts
       st  <- sawCoreState sym
       let sc = saw_ctx st
       len <- scNat sc (fromInteger n)
       ty  <- scBitvector sc (natValue w)
       let atIx i = do ind    <- scNat sc (fromInteger i)
                       term_i <- scAt sc len ty term ind
                       bv <- bindSAWTerm sym st (BaseBVRepr w) term_i
                       llvmPointer_bv sym bv
       mapM atIx [ 0 .. n - 1 ]
  
  
  -- | Cryptol function that returns a bitvector of the given len
  evalCryFun ::
    (1 <= w, Eval p, ?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Opts ->
    S p ->
    NatRepr w ->
    Text ->
    [CryArg p] ->
    IO (LLVMPtr Sym w)
  evalCryFun opts s w f xs =
    llvmPointer_bv (optsSym opts) =<< evalCryFunGen opts s (BaseBVRepr w) f xs
  
  evalProp ::
    (Eval p, ?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Opts -> Prop p -> S p -> IO (Pred Sym)
  evalProp opts p s =
    case p of
      Same t x y ->
        do v1 <- eval x opts s
           v2 <- eval y opts s
           evalSame sym t v1 v2
  
      CryProp f xs -> evalCryFunGen opts s BaseBoolRepr f xs
  
      CryPostMem ptr n u f xs ->
        -- unitBitSize  u $ \wBits ->
        unitByteSize u $ \wBytes ->
        do LeqProof <- return (leqMulPos (Proxy @8) wBytes)
           let wBits = natMultiply (knownNat @8) wBytes
           need   <- evalCryFunArr opts s n wBits f xs -- expected values
           have   <- readArr opts ptr n wBytes s (snd s)
           checks <- zipWithM (ptrEq sym wBits) need have
           foldM (andPred sym) (truePred sym) checks
    where
    sym = optsSym opts
  
  
  readArr :: forall w p.
    (1 <= w, Eval p, ?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Opts ->
    V p (LLVMPointerType 64) ->
    Integer ->
    NatRepr w ->
    S p ->
    State ->
    IO [ LLVMPtr Sym (8 * w) ]
  readArr opts ptr n wBytes s sMem =
    optsWithBackend opts $ \bak ->
        do ptrV <- eval ptr opts s
           LeqProof <- return (leqMulPos (Proxy @8) (Proxy @w))
           let mem    = stateMem sMem
               wBits  = natMultiply (knownNat @8) wBytes
               cruT   = LLVMPointerRepr wBits
               llT    = llvmBytes wBytes
               getAt i =
                 do let ?ptrWidth = knownNat
                    loc <- adjustPtr bak mem ptrV (i * toInteger (natValue wBytes))
                    doLoad bak mem loc llT cruT noAlignment
  
           mapM getAt [ 0 .. n - 1 ]
  
  
  evalSame ::
    Sym -> TypeRepr t -> RegValue Sym t -> RegValue Sym t -> IO (Pred Sym)
  evalSame sym t v1 v2 =
    case t of
      BoolRepr          -> isEq sym v1 v2
      LLVMPointerRepr w -> ptrEq sym w v1 v2
      it -> fail ("[evalProp] Unexpected value repr: " ++ show it)
  
  
  
  -- | Add an assertion to the post-condition.
  doAssert ::
    (Eval p, ?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Opts -> S p -> (String, Prop p) -> IO ()
  doAssert opts s (msg,p) =
    do pr <- evalProp opts p s
       optsWithBackend opts $ \bak ->
         assert bak pr (AssertFailureSimError msg "")
  
  
  --------------------------------------------------------------------------------
  
  data Rep t = Rep (TypeRepr t) Int
  
  instance Eq (Rep t) where
    Rep _ x == Rep _ y = x == y
  
  instance TestEquality Rep where
    testEquality x y = case compareF x y of
                         EQF -> Just Refl
                         _   -> Nothing
  
  instance OrdF Rep where
    compareF (Rep s x) (Rep t y) =
      case compareF s t of
        LTF -> LTF
        GTF -> GTF
        EQF -> case compare x y of
                  LT -> LTF
                  GT -> GTF
                  EQ -> EQF
  
  data RepMap p = RepMap
    { repFor :: MapF.MapF Loc Rep
       -- ^ Keeps track of the representative for a value
  
    , repBy  :: MapF.MapF Rep (Equiv p)
      -- ^ Inverse of the above: keeps track of which locs have this rep.
  
    , nextRep :: !Int
    }
  
  
  emptyRepMap :: RepMap p
  emptyRepMap = RepMap { repFor = MapF.empty
                       , repBy = MapF.empty
                       , nextRep = 0
                       }
  
  data Equiv p t = Equiv [ Loc t ] [ V p t ] deriving Show
  
  jnEquiv :: Equiv p t -> Equiv p t -> Equiv p t
  jnEquiv (Equiv xs ys) (Equiv as bs) = Equiv (xs ++ as) (ys ++ bs)
  
  -- | Add a fresh representative for something that had no rep before.
  newRep :: TypeRepr t -> Equiv p t -> RepMap p -> (Rep t, RepMap p)
  newRep t xs mp =
    let n = nextRep mp
        r = Rep t n
    in (r, mp { nextRep = n + 1
              , repBy   = MapF.insert r xs (repBy mp)
              })
  
  getRep :: TypeRepr t -> RepMap p -> Loc t -> (Rep t, RepMap p)
  getRep t mp x =
    case MapF.lookup x (repFor mp) of
      Nothing -> let (r,mp1) = newRep t (Equiv [x] []) mp
                 in (r, mp1 { repFor = MapF.insert x r (repFor mp1) })
      Just y  -> (y, mp)
  
  
  addEqLocVal :: TypeRepr t -> Loc t -> V p t -> RepMap p -> RepMap p
  addEqLocVal t loc lit mp =
    let (x1,mp1) = getRep t mp loc
        (x2,mp2) = newRep t (Equiv [] [lit]) mp1
    in joinReps x1 x2 mp2
  
  addEqLocLoc :: TypeRepr t -> Loc t -> Loc t -> RepMap p -> RepMap p
  addEqLocLoc t x y mp =
    let (x1,mp1) = getRep t mp  x
        (y1,mp2) = getRep t mp1 y
    in joinReps x1 y1 mp2
  
  joinReps :: Rep t -> Rep t -> RepMap p -> RepMap p
  joinReps x y mp
    | x == y = mp
    | otherwise =
      -- x is the new rep
      case MapF.lookup y (repBy mp) of
        Nothing -> error "[joinReps] Empty equivalance class"
        Just new@(Equiv ls _) ->
          let setRep z = MapF.insert z x
          in mp { repBy = MapF.insertWith jnEquiv x new
                        $ MapF.delete y (repBy mp)
                , repFor = foldr setRep (repFor mp) ls
                }
  
  getEq :: (String,Prop p) -> RepMap p -> RepMap p
  getEq (_,p) mp =
    case p of
      Same t (Loc x) (Loc y) -> addEqLocLoc t x y mp
      Same t (Loc x) v       -> addEqLocVal t x v mp
      Same t v       (Loc x) -> addEqLocVal t x v mp
      _                      -> mp
  
  makeEquiv ::
    forall p.
    (Eval p, ?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Opts -> S p -> Pair Rep (Equiv p) -> IO (S p)
  makeEquiv opts s (Pair (Rep t _) (Equiv xs ys)) =
   optsWithBackend opts $ \bak ->
    do -- Note that (at least currently) the `ys` do not
       -- depend on the current state: they are all either `Lit`
       -- or SAW terms, or `PreLoc`.  This is why we can evaluate
       -- them now, without worrying about dependencies.  I think. (Yav)
  
       -- XXX: With the introduction of `CryFun` one could depend on the
       -- current state.  For now, we are simply careful not to,
       -- in particular, `CryFun` is used only in pre-conditions and all
       -- its arguments are `LocPre` (i.e., the values before execution).
  
       -- Note 2: Sometimes it is useful for CryFun to depend on the current
       -- state.  For example, consider a function which computes two things
       -- f : x -> (a,b)
       -- Now we may have specs like this:
       --    a = spec1 x
       --    b = spec2 x a
       -- Of course, we could replcae `b` by:
       --    b = spec2 x (spec1 x)
       -- but that's ugly and duplicates stuff.
  
       vs <- mapM (\v -> eval v opts s) ys
  
       let sym = backendGetSym bak
       let pName = Proxy :: Proxy p
       let cur = curState pName s
  
       (v,rest) <- case vs of
                     v : us -> return (v,us)
                     [] -> case xs of
                             [] -> error "[makeEquiv] Empty equivalence class"
                             l : _ -> do v <- getLoc l opts cur
                                         return (v,[])
  
       s1 <- foldM (\s' y -> setLoc y opts v s') cur xs
  
       let same a =
             do p <- evalSame sym t v a
                let loc = mkProgramLoc "<makeEquiv>" InternalPos
                addAssumption bak
                  $ GenericAssumption loc "equivalance class assumption" p
  
       mapM_ same rest
  
       return (setCurState pName s1 s)
  
  
  makeEquivs ::
    (Eval p, ?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Opts -> RepMap p -> S p -> IO (S p)
  makeEquivs opts mp s = foldM (makeEquiv opts) s (MapF.toList (repBy mp))
  
  
  
  addAsmp ::
    (Eval p, ?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Opts -> S p -> (String,Prop p) -> IO ()
  addAsmp opts s (msg,p) =
    case p of
      Same _ (Loc _) _ -> return ()
      Same _ _ (Loc _) -> return ()
      CryPostMem {}    -> return ()
  
      _ -> optsWithBackend opts $ \bak ->
             do p' <- evalProp opts p s
                let loc = mkProgramLoc "<addAssmp>" InternalPos -- FIXME
                addAssumption bak (GenericAssumption loc msg p')
  
  setCryPost ::
    forall p.
    (Eval p, ?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Opts -> S p -> (String,Prop p) -> IO (S p)
  setCryPost opts s (_nm,p) =
    optsWithBackend opts $ \bak ->
    case p of
      (CryPostMem ptr n u f xs) ->
        unitBitSize  u $ \bitW ->
        unitByteSize u $ \byteW ->
        do vs   <- evalCryFunArr opts s n bitW f xs
           ptrV <- eval ptr opts s
           let llT  = llvmBytes byteW
               cruT = LLVMPointerRepr bitW
               sym  = backendGetSym bak
  
           let doSet mem (i,v) =
                 do let ?ptrWidth = knownNat
                    loc <- adjustPtr bak mem ptrV (bytesToInteger (i *. u))
                    val <- packMemValue sym llT cruT v
                    let alignment = noAlignment -- default to byte-aligned (FIXME, see #338)
                    storeConstRaw bak mem loc llT alignment val
  
           let cur   = Proxy @p
               curSt = curState cur s :: State
           mem1 <- foldM doSet (stateMem curSt) (zip [ 0 .. ] vs)
           return (setCurState cur curSt { stateMem = mem1 } s)
  
      _ -> return s
  
  
  addAssumptions ::
    forall p.
    (Eval p, ?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Opts -> S p -> [(String, Prop p)] -> IO State
  addAssumptions opts s0 ps =
    do let mp = foldr getEq emptyRepMap ps
       s1 <- makeEquivs opts mp s0
       s2 <- foldM (setCryPost opts) s1 ps
       mapM_ (addAsmp opts s2) ps
       return (curState (Proxy :: Proxy p) s2)
  
  
  --------------------------------------------------------------------------------
  
  -- | Allocate a memory region.
  allocate ::
    (?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Opts -> Area -> State -> IO (LLVMPtr Sym 64, State)
  allocate opts ar s =
    case areaMode ar of
      RO -> do (base,p,m1) <- alloc Immutable
               m2     <- fillFresh opts withPtrs base uni names m1
               return (p, s { stateMem = m2 })
  
      RW -> do (base,p,m1) <- alloc Mutable
               m2 <- fillFresh opts withPtrs base uni names m1
               return (p, s { stateMem = m2 })
  
      WO -> do (_,p,m1) <- alloc Mutable
               return (p, s { stateMem = m1 })
    where
    withPtrs = areaHasPointers ar
  
    alloc mut =
      optsWithBackend opts $ \bak ->
        do let sym = backendGetSym bak
           let ?ptrWidth = knownNat @64
           let szInt = bytesToInteger (uncurry (*.) (areaSize ar))
           sz <- bvLit sym knownNat (BV.mkBV knownNat szInt)
           let alignment = noAlignment -- default to byte-aligned (FIXME, see #338)
           (base,mem) <- doMalloc bak HeapAlloc mut (areaName ar) (stateMem s) sz alignment
           ptr <- adjustPtr bak mem base (bytesToInteger (areaPtr ar))
           return (base,ptr,mem)
  
    (num,uni) = areaSize ar
  
    names :: [String]
    names = [ areaName ar ++ "_" ++ show uni ++ "_" ++ show i
            | i <- take (fromInteger num) [ 0 :: Int .. ] ]
  
  fillFresh ::
    (?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Opts ->
    Bool ->
    LLVMPtr Sym 64 ->
    Unit ->
    [String] ->
    MemImpl Sym ->
    IO (MemImpl Sym)
  fillFresh opts ptrOk p u todo mem =
    unitByteSize u $ \w ->
    optsWithBackend opts $ \bak ->
    case todo of
      [] -> return mem
      nm : more ->
        do let sym = backendGetSym bak
           let ?ptrWidth = knownNat
           let ty        = ptrTy w
           let elS       = toInteger (natValue w)
           let lty       = bitvectorType (toBytes elS)
           val <- packMemValue sym lty ty =<< freshVal sym ty ptrOk nm
           -- Here we use the write that ignore mutability.
           -- This is because we are writinging initialization code.
           let alignment = noAlignment -- default to byte-aligned (FIXME, see #338)
           mem1 <- storeConstRaw bak mem p lty alignment val
           p1   <- adjustPtr bak mem1 p elS
           fillFresh opts ptrOk p1 u more mem1
  
  
  -- | Make an allocation.  Used when verifying.
  doAlloc ::
    (?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Opts -> State -> Alloc -> IO State
  doAlloc opts s (l := a) =
    do (p,s1) <- allocate opts a s
       setLoc l opts p s1
  
  -- | Fill-in a memory area with fresh values.
  -- This has no effect if the area is RO.
  clobberArea ::
    (?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Opts -> MemImpl Sym -> LLVMPtr Sym 64 -> Area -> IO (MemImpl Sym)
  clobberArea opts mem p ar =
    case areaMode ar of
      RO -> return mem
      _  -> optsWithBackend opts $ \bak ->
        do base <- adjustPtr bak mem p (negate (bytesToInteger (areaPtr ar)))
           let (num,uni) = areaSize ar
               xs = take (fromInteger num)
                    [ areaName ar ++ "_" ++ show uni ++ "_at_" ++ show i
                                                        | i <- [ 0 :: Int .. ]]
           fillFresh opts (areaHasPointers ar) base uni xs mem
  
  
  -- | Lookup the value for an allocation in the existing state.
  -- Used when overriding.
  -- Returns the start and end of the allocation.
  checkAlloc ::
    (?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Opts -> State -> Alloc -> IO (LLVMPtr Sym 64, LLVMPtr Sym 64)
  checkAlloc opts s (l := a) =
    optsWithBackend opts $ \bak ->
      do let mem = stateMem s
         p1 <- getLoc l opts s
         p2 <- adjustPtr bak mem p1 (negate (bytesToInteger (areaPtr a)))
  
         -- Make sure that we have a pointer and it is big enough.
         let siI = bytesToInteger $ uncurry (*.) (areaSize a)
         p3 <- adjustPtr bak mem p2 siI
         return (p2,p3)
  
  -- | Implements a layer to map 'LLVMPtr's to their underlying allocations, as
  -- tracked by the 'RegionIndex' map
  --
  -- NOTE: If the initial obvious mapping (where the concrete nat is in the map)
  -- fails, there are two possibilities:
  --
  -- 1. The region ID is concrete but not in the map.  We should just pass it
  --    through without modifying it, since it is a valid LLVM pointer
  -- 2. The region ID is symbolic.  In this case, we need to generate a mux that
  --    dispatches to the entries in the map when they match, or otherwise passes
  --    the pointer through untouched.
  --
  -- If the region ID is concretely zero, it should be the case that the
  -- 'RegionIndex' map would translate it into a real 'LLVMPtr' since the only map
  -- entry (established in 'setupGlobals') is for 0.
  mkGlobalMap ::
    (?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Map.Map RegionIndex (LLVMPtr Sym 64) ->
    GlobalMap Sym Crucible.Mem 64
  mkGlobalMap rmap = GlobalMap $ \bak mem region off ->
    let
      sym = backendGetSym bak
  
      mapConcreteRegion = maybe mzero id (addOffset <$> thisRegion)
      thisRegion = join (findRegion <$> asNat region)
      findRegion r = Map.lookup (fromIntegral r) rmap
      addOffset p = doPtrAddOffset bak mem p off
        where ?ptrWidth = knownNat
      passThroughConcreteRegion =
        case asNat region of
          Nothing -> mzero
          Just _ -> return (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 (LLVMPointer region off) (Map.toList rmap)
      muxSymbolicRegion others (regionNum, basePtr) = do
        thisRegionNat <- natLit sym (fromIntegral regionNum)
        isEqRegion <- natEq sym thisRegionNat region
        adjustedPtr <- addOffset basePtr
        muxLLVMPtr sym isEqRegion adjustedPtr others
  
    in mapConcreteRegion <|> passThroughConcreteRegion <|> mapSymbolicRegion
  
  -- | Setup globals in a single read-only region (index 0).
  setupGlobals ::
    (?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Opts ->
    [(String,Integer,Unit,[Integer])] ->
    [(String,Integer,Int -> Specification)] ->
    State ->
    IO ((GlobalMap Sym Crucible.Mem 64, Overrides), State)
  setupGlobals opts gs fs s
    | null regions && null fs = return ((mkGlobalMap Map.empty, Map.empty), s)
  
    | not (null overlaps) =
        fail $ unlines $ "Overlapping regions in global spec:"
                       : [ "*** " ++ x ++ " and " ++ y
                            | (x,y) <- overlaps ]
  
    | otherwise =
      optsWithBackend opts $ \bak ->
      do let endGlob = case last regions of
                         (_,start,n) -> start + bytesToInteger n
             size    = maximum (endGlob : fundAddrs)
  
         let ?ptrWidth = knownNat @64
         sz <- bvLit sym knownNat (BV.mkBV knownNat size)
         let alignment = noAlignment -- default to byte-aligned (FIXME, see #338)
         (p,mem) <- doMalloc bak GlobalAlloc Immutable "Globals" (stateMem s) sz alignment
  
         base <- case asNat (fst (llvmPointerView p)) of
           Just base -> pure base
           Nothing   -> error "[setupGlobals] Expected concrete block number from doMalloc"
  
         mem1 <- foldM (writeGlob p) mem gs
         let gMap = mkGlobalMap (Map.singleton 0 p)
  
             {- NOTE:  Some functions are called multiple times with different
                       sizes. This means that we need different specs for them,
                       at least until we support polymorphic specs.  As a quick
                       work-around we count the number of times a function is
                       entered and provide this as an input to the spec.
                       In simple cases this allows the spec to change itslef. -}
             mkHandler (name,a, sp) =
                do entryCounter <- newIORef 0
                   let fname = fromString name
                   return $
                      ( (base,a)
                      , \_ -> LookupFunctionHandle $ \st _ _ ->
                           do let sty = crucArchRegTypes x86_64MacawSymbolicFns
                              let rty = StructRepr sty
                              let o = mkOverride' fname rty $ do
                                        -- NB, grab the backend from the override monad;
                                        -- this may be different than the one available now
                                        -- while setting up the globals
                                        bak' <- _ctxBackend <$> getContext
  
                                        ent <- liftIO $ atomicModifyIORef' entryCounter $
                                                               \e -> (e + 1, e)
                                        -- liftIO $ putStrLn ("ENTER " ++ _f)
                                        RegMap args <- getOverrideArgs
                                        mem' <- readGlobal (optsMvar opts)
                                        let st0 = State { stateRegs = regValue (Ctx.last args), stateMem = mem' }
                                        -- liftIO $ debugPPReg RCX st0
                                        st1 <- liftIO $ overrideMode (sp ent) opts{ optsBackend = bak' } st0
                                        -- liftIO $ debugPPReg RCX st1
                                        writeGlobal (optsMvar opts) (stateMem st1)
                                        -- liftIO $ putStrLn ("EXIT " ++ _f)
                                        return (stateRegs st1)
                              let halloc = simHandleAllocator (st ^. stateContext)
                              h <- mkHandle halloc fname
                              let addBinding = over (stateContext . functionBindings)
                                                 (FnBindings . insertHandleMap h (UseOverride o) . fnBindings)
                              return (h, addBinding st)
                        )
  
         fMap <- Map.fromList <$> mapM mkHandler fs
  
         return ((gMap,fMap), s { stateMem = mem1 })
    where
    sym = optsSym opts
  
    fundAddrs = [ a | (_,a,_) <- fs ]
  
    regions = sortBy cmpStart
            $ [ (nm,start, fromIntegral (length els) *. u)
                | (nm,start,u,els) <- gs ]
    cmpStart (_,s1,_) (_,s2,_) = compare s1 s2
  
    overlaps = catMaybes (zipWith check regions (drop 1 regions))
  
    -- check for overlap, assuming first one starts at smaller address.
    check (r1,s1,n1) (r2,s2,_)
      | s1 + bytesToInteger n1 <= s2 = Nothing
      | otherwise                    = Just (r1,r2)
  
    writeGlob base mem (_,start,u,els) =
      optsWithBackend opts $ \bak ->
        do p <- adjustPtr bak mem base start
           snd <$> foldM (writeU u) (p,mem) els
  
    writeU u (p,mem) v =
      unitBitSize u $ \w ->
      optsWithBackend opts $ \bak ->
        do let sz = 1 *. u
               szI = bytesToInteger sz
               lty = bitvectorType sz
           z    <- natLit sym 0
           val  <- LLVMValInt z <$> bvLit sym w (BV.mkBV w v)
           let ?ptrWidth = knownNat
           let alignment = noAlignment -- default to byte-aligned (FIXME, see #338)
           mem1 <- storeConstRaw bak mem p lty alignment val
           p1   <- adjustPtr bak mem1 p szI
           return (p1,mem1)
  
  debugPPReg ::
    (ToCrucibleType mt ~ LLVMPointerType w) =>
    X86Reg mt -> State -> IO ()
  debugPPReg r s =
    do RV v <- case lookupX86Reg r (stateRegs s) of
         Just rv -> pure rv
         Nothing -> error $ "[debugPPReg] Could not find register: " ++ show r
       putStrLn (show r ++ " = " ++ show (ppPtr v))
  
  _debugDumpGoals :: Opts -> IO ()
  _debugDumpGoals opts =
    optsWithBackend opts $ \bak ->
      do obls <- maybe [] goalsToList <$> getProofObligations bak
         mapM_ sh (toList obls)
    where
    sh (ProofGoal _hyps g) = print (view labeledPredMsg g)
  
  
  type Overrides = Map (Natural,Integer) (Sym -> LookupFunctionHandle (MacawSimulatorState Sym) Sym X86_64)
  
  -- | Use a specification to verify a function.
  -- Returns the initial state for the function, and a post-condition.
  verifyMode ::
    (?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Specification ->
    Opts ->
    IO ( (GlobalMap Sym Crucible.Mem 64, Overrides)
       , State
       , State -> IO ()
       )
  verifyMode spec opts =
    do let sym = optsSym opts
       s0 <- freshState sym
       (globs,s1) <- setupGlobals opts (specGlobsRO spec) (specCalls spec) s0
       s2 <- foldM (doAlloc opts) s1 $ sortBy cmpAlloc $ specAllocs spec
       s3 <- addAssumptions opts s2 (specPres spec)
       let post sF = mapM_ (doAssert opts (s3,sF)) (specPosts spec)
       return (globs, s3, post)
  
  -- | Ensure that writable areas do not overlap with any other areas.
  checkOverlaps ::
    (?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
     Opts -> [((LLVMPtr Sym 64, LLVMPtr Sym 64), Area)] -> IO ()
  checkOverlaps opts = check
    where
    check (p : ps) = mapM_ (nonOverLap p) ps >> check ps
    check []       = return ()
  
    nonOverLap ((p1,p2),ar1) ((q1,q2),ar2)
      -- Read-only area may overlap
      | areaMode ar1 == RO && areaMode ar2 == RO = return ()
  
      | otherwise =
      optsWithBackend opts $ \bak ->
        do let sym = backendGetSym bak
           let (a1,x1) = llvmPointerView p1
               (_, x2) = llvmPointerView p2
               (b1,y1) = llvmPointerView q1
               (_,y2)  = llvmPointerView q2
           opt1 <- notPred sym =<< natEq sym a1 b1
           opt2 <- bvUle sym x2 y1
           opt3 <- bvUle sym y2 x1
           ok <- orPred sym opt1 =<< orPred sym opt2 opt3
           let msg = unlines
                 [ "Potentially aliased pointers:"
                 , "*** " ++ show (ppPtr p1)
                 , "*** " ++ show (ppPtr q1)
                 ]
           assert bak ok $ AssertFailureSimError msg ""
  
  -- | Use a specification to replace the execution of a function.
  overrideMode ::
    (?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
    Specification -> Opts -> State -> IO State
  overrideMode spec opts s =
    do let sym = optsSym opts
       let orderedAllocs = sortBy cmpAlloc (specAllocs spec)
       as <- mapM (checkAlloc opts s) orderedAllocs    -- check sizes
       checkOverlaps opts (zip as (map allocArea orderedAllocs)) -- check distinct
       mapM_ (doAssert opts s) (specPres spec)         -- assert pre-condition
  
       newRegs <- stateRegs <$> freshState sym
  
       mem1 <- foldM (\s' (p,a) -> clobberArea opts s' p a) (stateMem s)
             $ reverse $ zip (map fst as) [ a | _ := a <- orderedAllocs ]
  
       let sNew1 = State { stateMem = mem1, stateRegs = newRegs  }
       sf <- addAssumptions opts (s,sNew1) (specPosts spec)
  
       -- XXX: When Macaw calls us, the IP is already at the adress of the
       -- called function.  Unfortunately, the return address is not on top
       -- of the stack, as it shold be, so we don't know the correct value.
       -- It looks like things work, if keep the orignal value instead.
  
       ip0 <- case lookupX86Reg X86_IP (stateRegs s) of
         Just ip0 -> pure ip0
         Nothing  -> noIPError
       finalRegs <- case updateX86Reg X86_IP (const ip0) (stateRegs sf) of
         Just finalRegs -> pure finalRegs
         Nothing        -> noIPError
       return sf { stateRegs = finalRegs }
    where
      noIPError :: a
      noIPError = error "[overrideMode] Could not find instruction pointer"
  
  
  
  --------------------------------------------------------------------------------
  -- Cryptol
  
  
  -- | Lookup a cryptol term, and apply it to the given arguments,
  -- returning the result.
  cryTerm :: Opts -> Text -> [Term] -> IO Term
  cryTerm opts x xs =
    case lookupCry x (eTermEnv (optsCry opts)) of
      Left err -> fail $ Text.unpack err
      Right t ->
       do let sym = optsSym opts
          sc <- saw_ctx <$> sawCoreState sym
          scApplyAll sc t xs
  
  -- | Lookup a Crytpol type synonym, which should resolve to a constant.
  cryConst :: CryptolEnv -> Text -> Either Text Integer
  cryConst env x =
    do let mp = ifTySyns (getAllIfaceDecls (eModuleEnv env))
       t <- lookupCry x mp
       case matchMaybe (aNat (tsDef t)) of
         Just n  -> return n
         Nothing -> Left (x <> " is not a fixed constant type synonym.")
  
  -- | Lookup a name in a map indexed by Cryptol names.
  lookupCry :: Text -> Map Name a -> Either Text a
  lookupCry x mp =
    case x `lookupIn` mp of
      Left [] -> Left $ Text.unlines $ ("Missing Cryptol name: " <> x)
                                     : [ "*** " <> ppName y | y <- Map.keys mp ]
      Left ys -> Left $ Text.unlines ( "Ambiguous Cryptol name:"
                                     : [ "*** " <> ppName y | y <- ys ]
                                     )
      Right a -> Right a
  
    where ppName = Text.pack . show . pp
  
  
  
  
  --------------------------------------------------------------------------------
  
  
  adjustPtr ::
    (?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym, IsSymBackend Sym bak) =>
    bak ->
    MemImpl Sym ->
    LLVMPtr Sym 64 ->
    Integer ->
    IO (LLVMPtr Sym 64)
  adjustPtr bak mem ptr amt
    | amt == 0  = return ptr
    | otherwise =
      do let ?ptrWidth = knownNat
         let sym = backendGetSym bak
         doPtrAddOffset bak mem ptr =<< bvLit sym knownNat (BV.mkBV knownNat amt)
  