content: {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE ImplicitParams #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE TypeOperators #-}
  
  module TestMemory
    (
      memoryTests
    )
  where
  
  import           Control.Lens ( (^.), _1, _2 )
  import           Control.Monad ( foldM, forM_, void )
  import           Data.Foldable ( foldlM )
  import qualified Data.Vector as V
  
  import qualified Test.Tasty as T
  import           Test.Tasty.HUnit ( testCase, (@=?), assertFailure )
  
  import qualified Data.BitVector.Sized as BV
  import           Data.Parameterized.Context as Ctx
  import           Data.Parameterized.NatRepr ( knownNat )
  import           Data.Parameterized.Nonce ( withIONonceGenerator )
  import qualified What4.Expr as WE
  import qualified What4.Expr.Builder as WE
  import qualified What4.Config as What4
  import qualified What4.Interface as What4
  import           What4.ProblemFeatures ( noFeatures )
  import qualified What4.Protocol.Online as W4O
  import qualified What4.SatResult as W4Sat
  
  import qualified Lang.Crucible.Backend as CB
  import qualified Lang.Crucible.Backend.Online as CBO
  import qualified Lang.Crucible.Simulator as CS
  import qualified Lang.Crucible.Types as Crucible
  
  import           Lang.Crucible.LLVM.DataLayout ( noAlignment )
  import qualified Lang.Crucible.LLVM.DataLayout as LLVMD
  import           Lang.Crucible.LLVM.MemModel ( doLoad, doStore, projectLLVM_bv, ptrAdd )
  import qualified Lang.Crucible.LLVM.MemModel as LLVMMem
  import qualified Lang.Crucible.LLVM.MemModel.Generic as LLVMMemG
  
  
  memoryTests :: T.TestTree
  memoryTests = T.testGroup "Memory"
    [
      testArrayStride
    , testMemAllocs
    , testMemWritesIndexed
    , testMemArrayWithConstants
    , testMemArray
    , testPointerStore
    , testStructStore
    , testMemArrayCopy
    , testMemArraySet
    , testMemInvalidate
    ]
  
  withMem ::
    LLVMD.EndianForm ->
    (forall bak sym scope solver st fs wptr .
      ( sym ~ WE.ExprBuilder scope st fs
      , bak ~ CBO.OnlineBackend solver scope st fs
      , CB.IsSymBackend sym bak
      , LLVMMem.HasLLVMAnn sym
      , W4O.OnlineSolver solver
      , LLVMMem.HasPtrWidth wptr
      , ?memOpts :: LLVMMem.MemOptions ) =>
      bak -> LLVMMem.MemImpl sym -> IO a) ->
    IO a
  withMem endianess action = withIONonceGenerator $ \nonce_gen -> do
    sym <- WE.newExprBuilder WE.FloatIEEERepr WE.EmptyExprBuilderState nonce_gen
    CBO.withZ3OnlineBackend sym CBO.NoUnsatFeatures noFeatures $ \bak -> do
      let ?ptrWidth = knownNat @64
      let ?recordLLVMAnnotation = \_ _ _ -> pure ()
      let ?memOpts = LLVMMem.defaultMemOptions
      mem <- LLVMMem.emptyMem endianess
      action bak mem
  
  setCacheTerms :: CB.IsSymInterface sym => sym -> Bool ->IO ()
  setCacheTerms sym cache_terms_option = do
    cache_terms_setting <- What4.getOptionSetting WE.cacheTerms $ What4.getConfiguration sym
    void $ What4.setOpt cache_terms_setting cache_terms_option
  
  userSymbol' :: String -> What4.SolverSymbol
  userSymbol' s = case What4.userSymbol s of
    Left e -> error $ show e
    Right symbol -> symbol
  
  assume :: (CB.IsSymBackend sym bak) => bak -> What4.Pred sym -> IO ()
  assume bak p = do
    let sym = CB.backendGetSym bak
    loc <- What4.getCurrentProgramLoc sym
    CB.addAssumption bak (CB.GenericAssumption loc "assume" p)
  
  checkSat ::
    W4O.OnlineSolver solver =>
    CBO.OnlineBackend solver scope st fs ->
    WE.BoolExpr scope ->
    IO (W4Sat.SatResult () ())
  checkSat bak p =
    let err = fail "Online solving not enabled!" in
    CBO.withSolverProcess bak err $ \proc ->
       W4O.checkSatisfiable proc "" p
  
  
  testArrayStride :: T.TestTree
  testArrayStride = testCase "array stride" $ withMem LLVMD.BigEndian $ \bak mem0 -> do
    let sym = CB.backendGetSym bak
    sz <- What4.bvLit sym ?ptrWidth $ BV.mkBV ?ptrWidth (1024 * 1024)
    (base_ptr, mem1) <- LLVMMem.mallocRaw bak mem0 sz noAlignment
  
    let byte_type_repr = Crucible.baseToType $ What4.BaseBVRepr $ knownNat @8
    let byte_storage_type = LLVMMem.bitvectorType 1
    let ptr_byte_repr = LLVMMem.LLVMPointerRepr $ knownNat @8
  
    init_array_val <- LLVMMem.LLVMValArray byte_storage_type <$>
      V.generateM (1024 * 1024)
        (\i -> LLVMMem.packMemValue sym byte_storage_type byte_type_repr
          =<< What4.bvLit sym (knownNat @8) (BV.mkBV knownNat (fromIntegral (mod i (512 * 1024)))))
    mem2 <- LLVMMem.storeRaw
      bak
      mem1
      base_ptr
      (LLVMMem.arrayType (1024 * 1024) byte_storage_type)
      noAlignment
      init_array_val
  
    stride <- What4.bvLit sym ?ptrWidth $ BV.mkBV ?ptrWidth (512 * 1024)
  
    i <- What4.freshConstant sym (userSymbol' "i") $ What4.BaseBVRepr ?ptrWidth
    ptr_i <- ptrAdd sym ?ptrWidth base_ptr =<< What4.bvMul sym stride i
    ptr_i' <- ptrAdd sym ?ptrWidth ptr_i =<< What4.bvOne sym ?ptrWidth
  
    zero_bv <- What4.bvLit sym (knownNat @8) (BV.zero knownNat)
    mem3 <-
      doStore bak mem2 ptr_i byte_type_repr byte_storage_type noAlignment zero_bv
    one_bv <- What4.bvLit sym (knownNat @8) (BV.one knownNat)
    mem4 <-
      doStore bak mem3 ptr_i' byte_type_repr byte_storage_type noAlignment one_bv
  
    at_0_val <- projectLLVM_bv bak
      =<< doLoad bak mem4 base_ptr byte_storage_type ptr_byte_repr noAlignment
    (Just (BV.zero knownNat)) @=? What4.asBV at_0_val
  
    j <- What4.freshConstant sym (userSymbol' "j") $ What4.BaseBVRepr ?ptrWidth
    ptr_j <- ptrAdd sym ?ptrWidth base_ptr =<< What4.bvMul sym stride j
    ptr_j' <- ptrAdd sym ?ptrWidth ptr_j =<< What4.bvOne sym ?ptrWidth
  
    at_j_val <- projectLLVM_bv bak
      =<< doLoad bak mem4 ptr_j byte_storage_type ptr_byte_repr noAlignment
    (Just (BV.zero knownNat)) @=? What4.asBV at_j_val
  
    at_j'_val <- projectLLVM_bv bak
      =<< doLoad bak mem4 ptr_j' byte_storage_type ptr_byte_repr noAlignment
    (Just (BV.one knownNat)) @=? What4.asBV at_j'_val
  
  
  allocFreshArray ::
    ( CB.IsSymBackend sym bak, LLVMMem.HasLLVMAnn sym, LLVMMem.HasPtrWidth wptr
    , ?memOpts :: LLVMMem.MemOptions ) =>
    bak ->
    LLVMMem.MemImpl sym ->
    Integer ->
    IO (LLVMMem.LLVMPtr sym wptr, What4.SymArray sym (SingleCtx (What4.BaseBVType wptr)) (What4.BaseBVType 8), LLVMMem.MemImpl sym)
  allocFreshArray bak mem sz = do
    let sym = CB.backendGetSym bak
    sz_bv <- What4.bvLit sym ?ptrWidth $ BV.mkBV ?ptrWidth sz
    (base_ptr, mem1) <- LLVMMem.mallocRaw bak mem sz_bv noAlignment
    arr <- What4.freshConstant
      sym
      (userSymbol' "a")
      (What4.BaseArrayRepr (Ctx.singleton $ What4.BaseBVRepr ?ptrWidth) (What4.BaseBVRepr (knownNat @8)))
    mem2 <- LLVMMem.doArrayStore bak mem1 base_ptr noAlignment arr sz_bv
    return (base_ptr, arr, mem2)
  
  
  -- | This test case verifies that the symbolic aspects of the SMT-backed array
  -- memory model works (e.g., that constraints on symbolic indexes work as
  -- expected)
  testMemArray :: T.TestTree
  testMemArray = testCase "smt array memory model" $ withMem LLVMD.BigEndian $ \bak mem0 -> do
    let sym = CB.backendGetSym bak
    -- Make a fresh allocation (backed by a fresh SMT array) of size 1024*1024 bytes.
    -- The base pointer of the array is base_ptr
    sz <- What4.bvLit sym ?ptrWidth $ BV.mkBV ?ptrWidth (1024 * 1024)
    (base_ptr, mem1) <- LLVMMem.mallocRaw bak mem0 sz noAlignment
  
    arr <- What4.freshConstant
      sym
      (userSymbol' "a")
      (What4.BaseArrayRepr
        (Ctx.singleton $ What4.BaseBVRepr ?ptrWidth)
        (What4.BaseBVRepr (knownNat @8)))
    mem2 <- LLVMMem.doArrayStore bak mem1 base_ptr noAlignment arr sz
  
    let long_type_repr = Crucible.baseToType $ What4.BaseBVRepr $ knownNat @64
    let long_storage_type = LLVMMem.bitvectorType 8
    let ptr_long_repr = LLVMMem.LLVMPointerRepr $ knownNat @64
  
    -- Store a large known 8 byte value at a symbolic location in the array (at
    -- @i@ bytes from the beginning of the array).  The assumption constrains it
    -- such that the location is within the first 1024 bytes of the array.
    i <- What4.freshConstant sym (userSymbol' "i") $ What4.BaseBVRepr ?ptrWidth
    ptr_i <- ptrAdd sym ?ptrWidth base_ptr i
    assume bak =<< What4.bvUlt sym i =<< What4.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth 1024)
    some_val <- What4.bvLit sym (knownNat @64) (BV.mkBV knownNat 0x88888888f0f0f0f0)
    mem3 <-
      doStore bak mem2 ptr_i long_type_repr long_storage_type noAlignment some_val
  
    memset_ptr <- ptrAdd sym ?ptrWidth base_ptr =<< What4.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth 2048)
    memset_val <- What4.bvLit sym knownNat (BV.mkBV knownNat 0)
    memset_sz <- What4.bvLit sym (knownNat @64) (BV.mkBV knownNat 10)
    mem4 <- LLVMMem.doMemset bak (knownNat @64) mem3 memset_ptr memset_val memset_sz
  
    -- Read that same value back and make sure that they are the same
    at_i_val <- projectLLVM_bv bak
      =<< doLoad bak mem4 ptr_i long_storage_type ptr_long_repr noAlignment
    res_i <- checkSat bak =<< What4.bvNe sym some_val at_i_val
    True @=? W4Sat.isUnsat res_i
  
    -- Allocate another fresh arbitrary constant and add it to the base pointer.
    -- Assume that i = j, then verify that reading from j yields the same value as
    -- was written at i.
    j <- What4.freshConstant sym (userSymbol' "j") $ What4.BaseBVRepr ?ptrWidth
    ptr_j <- ptrAdd sym ?ptrWidth base_ptr j
    assume bak =<< What4.bvEq sym i j
    at_j_val <- projectLLVM_bv bak
      =<< doLoad bak mem4 ptr_j long_storage_type ptr_long_repr noAlignment
    res_j <- checkSat bak =<< What4.bvNe sym some_val at_j_val
    True @=? W4Sat.isUnsat res_j
  
  
  -- | Like testMemArray, but using some concrete indexes in a few places.  This
  -- test checks the implementation of saturated addition of two numbers.
  --
  -- This is simulating the use of an SMT array to represent a program stack, and
  -- ensures that:
  --
  -- * Concrete indexing works as expected
  -- * Goals that depend on the values of values stored in memory work
  testMemArrayWithConstants :: T.TestTree
  testMemArrayWithConstants = testCase "smt array memory model (with constant indexing)" $ do
    withMem LLVMD.LittleEndian $ \bak mem0 -> do
      let sym = CB.backendGetSym bak
      sz <- What4.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth (2 * 1024))
      (region_ptr, mem1) <- LLVMMem.mallocRaw bak mem0 sz noAlignment
      let mRepr = What4.BaseArrayRepr (Ctx.singleton (What4.BaseBVRepr ?ptrWidth)) (What4.BaseBVRepr (knownNat @8))
      backingArray <- What4.freshConstant sym (userSymbol' "backingArray") mRepr
      mem2 <- LLVMMem.doArrayStore bak mem1 region_ptr noAlignment backingArray sz
  
      let long_type_repr = Crucible.baseToType $ What4.BaseBVRepr $ knownNat @64
      let long_storage_type = LLVMMem.bitvectorType 8
      let ptr_long_repr = LLVMMem.LLVMPointerRepr $ knownNat @64
  
      -- Make our actual base pointer the middle of the stack, to simulate having
      -- some active frames above us
      base_off <- What4.freshConstant sym (userSymbol' "baseOffset") (What4.BaseBVRepr ?ptrWidth)
      assume bak =<< What4.bvUlt sym base_off =<< (What4.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth 10))
      base_ptr <- ptrAdd sym ?ptrWidth region_ptr base_off -- =<< What4.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth 1024)
  
      -- Assume we have two arguments to our virtual function:
      param_a <- What4.freshConstant sym (userSymbol' "paramA") (What4.BaseBVRepr (knownNat @64))
      param_b <- What4.freshConstant sym (userSymbol' "paramB") (What4.BaseBVRepr (knownNat @64))
  
      -- The fake stack frame will start at @sp@ be:
      --
      -- sp+8  : Stack slot for spilling a
      slot_a <- ptrAdd sym ?ptrWidth base_ptr =<< What4.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth 8)
      -- sp+16 : Stack slot for spilling b
      slot_b <- ptrAdd sym ?ptrWidth base_ptr =<< What4.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth 16)
      -- sp+24 : Stack slot for local variable c
      slot_c <- ptrAdd sym ?ptrWidth base_ptr =<< What4.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth 24)
  
      -- Store a and b onto the stack
      mem3 <- doStore bak mem2 slot_a long_type_repr long_storage_type noAlignment param_a
      mem4 <- doStore bak mem3 slot_b long_type_repr long_storage_type noAlignment param_b
  
      -- Read a and b off of the stack and compute c = a+b (storing the result on the stack in c's slot)
      valA0 <- projectLLVM_bv bak =<< doLoad bak mem4 slot_a long_storage_type ptr_long_repr noAlignment
      valB0 <- projectLLVM_bv bak =<< doLoad bak mem4 slot_b long_storage_type ptr_long_repr noAlignment
      mem5 <- doStore bak mem4 slot_c long_type_repr long_storage_type noAlignment =<< What4.bvAdd sym valA0 valB0
  
  
      valA1 <- projectLLVM_bv bak =<< doLoad bak mem5 slot_a long_storage_type ptr_long_repr noAlignment
      valB1 <- projectLLVM_bv bak =<< doLoad bak mem5 slot_b long_storage_type ptr_long_repr noAlignment
      valC1 <- projectLLVM_bv bak =<< doLoad bak mem5 slot_c long_storage_type ptr_long_repr noAlignment
  
      -- Add some assumptions to make our assertion actually hold (i.e., avoiding overflow)
      let n64 = knownNat @64
      -- assume sym =<< What4.bvUlt sym param_a =<< What4.bvLit sym n64 (BV.mkBV n64 100)
      -- assume sym =<< What4.bvUlt sym param_b =<< What4.bvLit sym n64 (BV.mkBV n64 100)
      cLessThanA <- What4.bvSlt sym valC1 valA1
      cLessThanB <- What4.bvSlt sym valC1 valB1
      ifOverflow <- What4.orPred sym cLessThanA cLessThanB
  
      i64Max <- What4.bvLit sym n64 (BV.mkBV n64 0x7fffffffffffffff)
      clamped_c <- What4.bvIte sym ifOverflow i64Max valC1
      mem6 <- doStore bak mem5 slot_c long_type_repr long_storage_type noAlignment clamped_c
  
      valC2 <- projectLLVM_bv bak =<< doLoad bak mem6 slot_c long_storage_type ptr_long_repr noAlignment
  
      aLessThanC <- What4.bvSle sym param_a valC2
      bLessThanC <- What4.bvSle sym param_b valC2
      assertion <- What4.andPred sym aLessThanC bLessThanC
      goal <- What4.notPred sym assertion
      res <- checkSat bak goal
      True @=? W4Sat.isUnsat res
  
  
  -- | This test case checks the memcpy aspect of the SMT-backed array memory model
  testMemArrayCopy :: T.TestTree
  testMemArrayCopy = testCase "smt array copy memory model" $ withMem LLVMD.LittleEndian $ \bak mem0 -> do
    let sym = CB.backendGetSym bak
  
    setCacheTerms sym True
  
    (dst_base_ptr, dst_arr, mem1) <- allocFreshArray bak mem0 (1024 * 1024)
    (src_base_ptr, src_arr, mem2) <- allocFreshArray bak mem1 1024
  
    i <- What4.freshConstant sym (userSymbol' "i") $ What4.BaseBVRepr ?ptrWidth
    dst_ptr <- ptrAdd sym ?ptrWidth dst_base_ptr i
    assume bak =<< What4.bvUlt sym i =<< What4.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth 1024)
    len <- What4.freshConstant sym (userSymbol' "l") $ What4.BaseBVRepr ?ptrWidth
    assume bak =<< What4.bvUlt sym len =<< What4.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth 1024)
    mem3 <- LLVMMem.doMemcpy bak ?ptrWidth mem2 False dst_ptr src_base_ptr len
  
    zero_bv <- What4.bvZero sym ?ptrWidth
    expected_arr <- What4.arrayCopy sym dst_arr i src_arr zero_bv len
    expected_val <- What4.arrayLookup sym expected_arr $ Ctx.singleton i
  
    actual_val <- projectLLVM_bv bak
      =<< doLoad bak mem3 dst_ptr (LLVMMem.bitvectorType 1) (LLVMMem.LLVMPointerRepr $ knownNat @8) noAlignment
  
    foo <- What4.bvEq sym expected_val actual_val
    (Just True) @=? What4.asConstantPred foo
  
  
  -- | This test case checks the memset aspect of the SMT-backed array memory model
  testMemArraySet :: T.TestTree
  testMemArraySet = testCase "smt array copy memory model" $ withMem LLVMD.LittleEndian $ \bak mem0 -> do
    let sym = CB.backendGetSym bak
    setCacheTerms sym True
  
    (base_ptr, arr, mem1) <- allocFreshArray bak mem0 (1024 * 1024)
  
    i <- What4.freshConstant sym (userSymbol' "i") $ What4.BaseBVRepr ?ptrWidth
    ptr_i <- ptrAdd sym ?ptrWidth base_ptr i
    assume bak =<< What4.bvUlt sym i =<< What4.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth 1024)
    val <- What4.freshConstant sym (userSymbol' "v") $ What4.BaseBVRepr $ knownNat @8
    len <- What4.freshConstant sym (userSymbol' "l") $ What4.BaseBVRepr ?ptrWidth
    assume bak =<< What4.bvUlt sym len =<< What4.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth 1024)
    mem3 <- LLVMMem.doMemset bak ?ptrWidth mem1 ptr_i val len
  
    expected_arr <- What4.arraySet sym arr i val len
    expected_val <- What4.arrayLookup sym expected_arr $ Ctx.singleton i
  
    actual_val <- projectLLVM_bv bak
      =<< doLoad bak mem3 ptr_i (LLVMMem.bitvectorType 1) (LLVMMem.LLVMPointerRepr $ knownNat @8) noAlignment
  
    foo <- What4.bvEq sym expected_val actual_val
    (Just True) @=? What4.asConstantPred foo
  
  
  testMemWritesIndexed :: T.TestTree
  testMemWritesIndexed = testCase "indexed memory writes" $ withMem LLVMD.BigEndian $ \bak mem0 -> do
    let sym = CB.backendGetSym bak
    let count = 100 * 1000
  
    sz <- What4.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth 8)
    (base_ptr1, mem1) <- LLVMMem.mallocRaw bak mem0 sz noAlignment
    (base_ptr2, mem2) <- LLVMMem.mallocRaw bak mem1 sz noAlignment
  
    let long_type_repr = Crucible.baseToType $ What4.BaseBVRepr $ knownNat @64
    let long_storage_type = LLVMMem.bitvectorType 8
    let ptr_long_repr = LLVMMem.LLVMPointerRepr $ knownNat @64
  
    zero_val <- What4.bvLit sym (knownNat @64) (BV.zero knownNat)
    mem3 <- doStore
      bak
      mem2
      base_ptr1
      long_type_repr
      long_storage_type
      noAlignment
      zero_val
  
    mem4 <- foldlM
      (\mem' i ->
        doStore bak mem' base_ptr2 long_type_repr long_storage_type noAlignment
          =<< What4.bvLit sym (knownNat @64) i)
      mem3
      (BV.enumFromToUnsigned (BV.zero (knownNat @64)) (BV.mkBV knownNat count))
  
    forM_ [0 .. count] $ \_ -> do
      val1 <- projectLLVM_bv bak
        =<< doLoad bak mem4 base_ptr1 long_storage_type ptr_long_repr noAlignment
      (Just (BV.zero knownNat)) @=? What4.asBV val1
  
    val2 <- projectLLVM_bv bak
      =<< doLoad bak mem4 base_ptr2 long_storage_type ptr_long_repr noAlignment
    (Just (BV.mkBV knownNat count)) @=? What4.asBV val2
  
  testMemAllocs :: T.TestTree
  testMemAllocs =
    testCase "memory model alloc/free" $
    withMem LLVMD.BigEndian $ \bak mem0 ->
    do let sym = CB.backendGetSym bak
       sz1 <- What4.bvLit sym ?ptrWidth $ BV.mkBV ?ptrWidth 128
       sz2 <- What4.bvLit sym ?ptrWidth $ BV.mkBV ?ptrWidth 72
       sz3 <- What4.bvLit sym ?ptrWidth $ BV.mkBV ?ptrWidth 32
       (ptr1, mem1) <- LLVMMem.mallocRaw bak mem0 sz1 noAlignment
       (ptr2, mem2) <- LLVMMem.mallocRaw bak mem1 sz2 noAlignment
       mem3 <- LLVMMem.doFree bak mem2 ptr2
       (ptr3, mem4) <- LLVMMem.mallocRaw bak mem3 sz3 noAlignment
       mem5 <- LLVMMem.doFree bak mem4 ptr1
       mem6 <- LLVMMem.doFree bak mem5 ptr3
  
       let isAllocated = LLVMMem.isAllocatedAlignedPointer sym ?ptrWidth noAlignment LLVMMem.Mutable
       assertions <-
         sequence
         [ isAllocated ptr1 (Just sz1) mem1
         , isAllocated ptr1 (Just sz1) mem2
         , isAllocated ptr1 (Just sz1) mem3
         , isAllocated ptr1 (Just sz1) mem4
         , isAllocated ptr1 (Just sz1) mem5 >>= What4.notPred sym
         , isAllocated ptr1 (Just sz1) mem6 >>= What4.notPred sym
  
         , isAllocated ptr2 (Just sz2) mem1 >>= What4.notPred sym
         , isAllocated ptr2 (Just sz2) mem2
         , isAllocated ptr2 (Just sz2) mem3 >>= What4.notPred sym
         , isAllocated ptr2 (Just sz2) mem4 >>= What4.notPred sym
         , isAllocated ptr2 (Just sz2) mem5 >>= What4.notPred sym
         , isAllocated ptr2 (Just sz2) mem6 >>= What4.notPred sym
  
         , isAllocated ptr3 (Just sz3) mem1 >>= What4.notPred sym
         , isAllocated ptr3 (Just sz3) mem2 >>= What4.notPred sym
         , isAllocated ptr3 (Just sz3) mem3 >>= What4.notPred sym
         , isAllocated ptr3 (Just sz3) mem4
         , isAllocated ptr3 (Just sz3) mem5
         , isAllocated ptr3 (Just sz3) mem6 >>= What4.notPred sym
         ]
       assertion <- foldM (What4.andPred sym) (What4.truePred sym) assertions
       res <- checkSat bak =<< What4.notPred sym assertion
       True @=? W4Sat.isUnsat res
  
  -- | This test case checks that 'doInvalidate' behaves as expected with and
  -- without 'laxLoadsAndStores' enabled.
  testMemInvalidate :: T.TestTree
  testMemInvalidate =
    testCase "memory invalidation" $ withMem LLVMD.BigEndian $ \bak mem0 ->
    do let sym = CB.backendGetSym bak
       sz <- What4.bvLit sym ?ptrWidth $ BV.mkBV ?ptrWidth 64
       let long_type_repr = Crucible.baseToType $ What4.BaseBVRepr $ knownNat @64
           long_storage_type = LLVMMem.bitvectorType 8
       zero_val <- What4.bvLit sym (knownNat @64) (BV.zero knownNat)
  
       let withInvalidatedReadVal memOpts k = do
             let ?memOpts = memOpts
             -- First, allocate some memory on the stack...
             (ptr, mem1) <- LLVMMem.doAlloca bak mem0 sz noAlignment "<alloca>"
             -- ...write some value to it (the exact value is unimportant)...
             mem2 <- LLVMMem.doStore bak mem1 ptr
                                     long_type_repr long_storage_type
                                     noAlignment zero_val
             -- ...invalidate the memory...
             mem3 <- LLVMMem.doInvalidate bak ?ptrWidth mem2 ptr "<invalidate>" sz
             -- ...and finally, read from the invalidated memory.
             partVal <- LLVMMemG.readMem sym ?ptrWidth Nothing ptr
                                         long_storage_type noAlignment
                                         (LLVMMem.memImplHeap mem3)
             k partVal
  
           testLaxInvalidatedRead :: String -> LLVMMem.IndeterminateLoadBehavior -> IO ()
           testLaxInvalidatedRead stability indeterminateLoadBehavior =
             withInvalidatedReadVal (?memOpts{ LLVMMem.laxLoadsAndStores = True
                                             , LLVMMem.indeterminateLoadBehavior = indeterminateLoadBehavior
                                             }) $ \partVal ->
             case partVal of
               LLVMMem.NoErr p _val -> do
                 res <- checkSat bak p
                 True @=? W4Sat.isSat res
               LLVMMem.Err p -> assertFailure $ unlines
                 [ "Reading from invalidated, " ++ stability ++ "-symbolic memory unexpectedly failed"
                 , "Predicate: " ++ show p
                 ]
  
       -- Test with laxLoadsAndStores disabled, where reading from invalidated
       -- memory should result in an error.
       withInvalidatedReadVal (?memOpts{LLVMMem.laxLoadsAndStores = False}) $ \partVal ->
         case partVal of
           LLVMMem.Err p -> do
             res <- checkSat bak p
             True @=? W4Sat.isUnsat res
           LLVMMem.NoErr p val -> assertFailure $ unlines
             [ "Reading from invalidated memory unexpectedly succeeded"
             , "Predicate: " ++ show p
             , "LLVM value read: " ++ show val
             ]
  
       -- Test with laxLoadsAndStores enabled, using both the
       -- StableSymbolic and UnstableSymbolic settings for
       -- indeterminateLoadBehavior. Here, reading from invalidated memory should succeed.
       testLaxInvalidatedRead "stable" LLVMMem.StableSymbolic
       testLaxInvalidatedRead "unstable" LLVMMem.UnstableSymbolic
  
  -- | Test storing and retrieving pointer in an SMT-backed array memory model
  testPointerStore :: T.TestTree
  testPointerStore = testCase "pointer store" $ withMem LLVMD.BigEndian $ \bak mem0 -> do
    let sym = CB.backendGetSym bak
    -- Allocate two blocks
    sz <- What4.bvLit sym ?ptrWidth $ BV.mkBV ?ptrWidth (1024 * 1024)
    (base_ptr1, _) <- LLVMMem.mallocRaw bak mem0 sz noAlignment
    (base_ptr2, block2_mem1) <- LLVMMem.mallocRaw bak mem0 sz noAlignment
  
    -- Store the first base pointer in the second block
    let pointer_storage_type = LLVMMem.bitvectorType 8
    let base_ptr1_val = LLVMMem.ptrToPtrVal base_ptr1
    block2_mem2 <- LLVMMem.storeRaw bak
                                    block2_mem1
                                    base_ptr2
                                    pointer_storage_type
                                    noAlignment
                                    base_ptr1_val
    -- Read the pointer back
    base_ptr1_back <- LLVMMem.loadRaw sym
                                      block2_mem2
                                      base_ptr2
                                      pointer_storage_type
                                      noAlignment
  
    -- Assert that the read pointer is equal to the original pointer
    base_ptr1_back_safe <- LLVMMem.assertSafe bak base_ptr1_back
    is_equal <- LLVMMem.testEqual sym base_ptr1_val base_ptr1_back_safe
    case is_equal of
      Nothing -> assertFailure "testEqual failed"
      Just p -> do
        goal <- What4.notPred sym p
        res <- checkSat bak goal
        True @=? W4Sat.isUnsat res
  
  -- | Test storing and retrieving a struct with and without 'laxLoadsAndStores'
  -- enabled.
  testStructStore :: T.TestTree
  testStructStore = testCase "struct store" $ withMem LLVMD.BigEndian $ \bak mem0 ->
    do let sym = CB.backendGetSym bak
       sz <- What4.bvLit sym ?ptrWidth $ BV.mkBV ?ptrWidth 64
       let struct_storage_type = LLVMMem.mkStructType $ V.fromList
                                   [ (LLVMMem.bitvectorType 2, 2)
                                   , (LLVMMem.bitvectorType 4, 0)
                                   ]
       let w16 = knownNat @16
       let w32 = knownNat @32
       let struct_type_repr = Crucible.StructRepr $
                                Ctx.Empty Ctx.:>
                                LLVMMem.LLVMPointerRepr w16 Ctx.:>
                                LLVMMem.LLVMPointerRepr w32
       let struct_bv1 = BV.mkBV w16 27
       let struct_bv2 = BV.mkBV w32 42
       struct_sym_bv1 <- What4.bvLit sym w16 struct_bv1
       struct_sym_bv2 <- What4.bvLit sym w32 struct_bv2
       struct_field1 <- LLVMMem.llvmPointer_bv sym struct_sym_bv1
       struct_field2 <- LLVMMem.llvmPointer_bv sym struct_sym_bv2
       let struct_val = Ctx.Empty Ctx.:>
                        CS.RV struct_field1 Ctx.:>
                        CS.RV struct_field2
  
       let testWithOpts memOpts = do
             let ?memOpts = memOpts
             -- First, allocate some memory on the stack...
             (ptr, mem1) <- LLVMMem.doAlloca bak mem0 sz noAlignment "<alloca>"
             -- ...write a struct to it...
             mem2 <- LLVMMem.doStore bak mem1 ptr
                       struct_type_repr struct_storage_type
                       noAlignment struct_val
             -- ...read back the struct...
             struct_val' <- LLVMMem.doLoad bak mem2 ptr
                              struct_storage_type struct_type_repr noAlignment
             -- ...and finally, check that the struct read from memory is the
             -- same as the original struct.
             let checkField ::
                   forall w sym bak.
                   CB.IsSymBackend sym bak =>
                   bak ->
                   BV.BV w ->
                   CS.RegValue' sym (LLVMMem.LLVMPointerType w) ->
                   IO ()
                 checkField bak' expectedBV actualPtrRV = do
                   actualSymBV <- projectLLVM_bv bak' $ CS.unRV actualPtrRV
                   Just expectedBV @=? What4.asBV actualSymBV
             checkField bak struct_bv1 (struct_val'^._1)
             checkField bak struct_bv2 (struct_val'^._2)
  
       testWithOpts (?memOpts{ LLVMMem.laxLoadsAndStores = False })
       testWithOpts (?memOpts{ LLVMMem.laxLoadsAndStores = True
                             , LLVMMem.indeterminateLoadBehavior = LLVMMem.StableSymbolic
                             })
       testWithOpts (?memOpts{ LLVMMem.laxLoadsAndStores = True
                             , LLVMMem.indeterminateLoadBehavior = LLVMMem.UnstableSymbolic
                             })
  