{-# 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.bvLit sym ?ptrWidth (BV.one ?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.bvLit sym ?ptrWidth (BV.one ?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.bvLit sym ?ptrWidth $ BV.zero ?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
                           })