Common.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

-- | Functionality that is shared between multiple memory models.
module Data.Macaw.Symbolic.Memory.Common
  ( MemoryModelContents(..)
  , toCrucibleEndian
  , fromCrucibleEndian
  , GlobalMemoryHooks(..)
  , defaultGlobalMemoryHooks

  , mkGlobalPointerValidityPredCommon
  , mapRegionPointersCommon
  , populateMemChunkBytes
  , assumeMemArr
  , pleatM
  , ipleatM
  ) where

import           GHC.TypeLits

import qualified Control.Lens as L
import           Control.Monad.IO.Class ( MonadIO, liftIO )
import qualified Data.BitVector.Sized as BV
import qualified Data.ByteString as BS
import qualified Data.Foldable as F
import qualified Data.Foldable.WithIndex as FWI
import qualified Data.IntervalMap.Strict as IM

import qualified Data.Parameterized.Context as Ctx
import qualified Data.Macaw.CFG as MC
import qualified Lang.Crucible.Backend as CB
import qualified Lang.Crucible.LLVM.DataLayout as CLD
import qualified Lang.Crucible.LLVM.MemModel as CL
import qualified Lang.Crucible.Simulator as CS
import           Text.Printf ( printf )
import qualified What4.Expr.App as WEA
import qualified What4.Expr.BoolMap as BoolMap
import qualified What4.Expr.Builder as WEB
import qualified What4.Interface as WI

import qualified Data.Macaw.Symbolic as MS

-- | A configuration knob controlling how the initial contents of the memory
-- model are populated
--
-- The fundamental question is how to treat global data.  It is (generally) safe
-- to make read only data concrete, as it cannot change during normal execution
-- (ignoring cases where the program uses mprotect or similar calls to change
-- memory permissions at runtime).
--
-- If we are trying to prove properties about functions in isolation, though, we
-- have to assume that non-constant global data can have /any/ value, which
-- means that we have to represent each byte as symbolic.  This will change when
-- we start pursuing compositional verification and want to have more elaborate
-- memory setups.
--
-- Note that using concrete mutable data from the binary image is unsafe, but
-- may be useful in some cases.
data MemoryModelContents = SymbolicMutable
                         -- ^ All mutable global data is fully symbolic, but
                         -- read-only data is concrete (and taken from the
                         -- memory image of the binary)
                         | ConcreteMutable
                         -- ^ All of the global data is taken from the binary
  deriving Eq

-- | Convert a Macaw 'MC.Endianness' to a Crucible LLVM 'CLD.EndianForm'.
toCrucibleEndian :: MC.Endianness -> CLD.EndianForm
toCrucibleEndian MC.BigEndian    = CLD.BigEndian
toCrucibleEndian MC.LittleEndian = CLD.LittleEndian

-- | Convert a Crucible LLVM 'CLD.EndianForm' to a Macaw 'MC.Endianness'.
fromCrucibleEndian :: CLD.EndianForm -> MC.Endianness
fromCrucibleEndian CLD.BigEndian    = MC.BigEndian
fromCrucibleEndian CLD.LittleEndian = MC.LittleEndian

-- | Hooks to configure the initialization of global memory
data GlobalMemoryHooks w =
  GlobalMemoryHooks {
  populateRelocation
    :: forall sym bak
       . (CB.IsSymBackend sym bak)
    => bak
    -> MC.Memory w
    -- ^ The region of memory in which the relocation is defined
    -> MC.MemSegment w
    -- ^ The segment of memory in which the relocation is defined
    -> MC.MemAddr w
    -- ^ The address of the relocation
    -> MC.Relocation w
    -> IO [WI.SymExpr sym (WI.BaseBVType 8)]
    -- ^ The symbolic bytes to represent a relocation with
    --
    -- They could be entirely unconstrained bytes, or could be distinguished
    -- bytes used to implement linking of shared libraries (i.e., relocation
    -- resolution)
  }

-- | A default set of hooks that raises errors if they encounter constructs that
-- they do not handle (because there is no sensible default behavior).
defaultGlobalMemoryHooks :: GlobalMemoryHooks w
defaultGlobalMemoryHooks =
  GlobalMemoryHooks {
    populateRelocation = \_ _ _ _ r ->
      return (error ("SymbolicRef SegmentRanges are not supported yet: " ++ show r))
    }

-- | The shared implementation for the @mkGlobalPointerValidityPred@ function in
-- the default memory model ("Data.Macaw.Symbolic.Memory") and the lazy memory
-- model ("Data.Macaw.Symbolic.Memory.Lazy").
mkGlobalPointerValidityPredCommon ::
     forall sym w
   . ( CB.IsSymInterface sym
     , MC.MemWidth w
     )
  => IM.IntervalMap (MC.MemWord w) CL.Mutability
  -> MS.MkGlobalPointerValidityAssertion sym w
mkGlobalPointerValidityPredCommon tbl = \sym puse mcond ptr -> do
  let w = MC.memWidthNatRepr @w

  -- If this is a write, the pointer cannot be in an immutable range (so just
  -- return False for the predicate on that range).
  --
  -- Otherwise, the pointer is allowed to be between the lo/hi range
  let inMappedRange off (range, mut)
        | MS.pointerUseTag puse == MS.PointerWrite && mut == CL.Immutable = return (WI.falsePred sym)
        | otherwise =
          case range of
            IM.IntervalCO lo hi -> do
              lobv <- WI.bvLit sym w (BV.mkBV w (toInteger lo))
              hibv <- WI.bvLit sym w (BV.mkBV w (toInteger hi))
              lob <- WI.bvUle sym lobv off
              hib <- WI.bvUlt sym off hibv
              WI.andPred sym lob hib
            IM.ClosedInterval lo hi -> do
              lobv <- WI.bvLit sym w (BV.mkBV w (toInteger lo))
              hibv <- WI.bvLit sym w (BV.mkBV w (toInteger hi))
              lob <- WI.bvUle sym lobv off
              hib <- WI.bvUle sym off hibv
              WI.andPred sym lob hib
            IM.OpenInterval lo hi -> do
              lobv <- WI.bvLit sym w (BV.mkBV w (toInteger lo))
              hibv <- WI.bvLit sym w (BV.mkBV w (toInteger hi))
              lob <- WI.bvUlt sym lobv off
              hib <- WI.bvUlt sym off hibv
              WI.andPred sym lob hib
            IM.IntervalOC lo hi -> do
              lobv <- WI.bvLit sym w (BV.mkBV w (toInteger lo))
              hibv <- WI.bvLit sym w (BV.mkBV w (toInteger hi))
              lob <- WI.bvUlt sym lobv off
              hib <- WI.bvUle sym off hibv
              WI.andPred sym lob hib

  let mkPred off = do
        ps <- mapM (inMappedRange off) (IM.toList tbl)
        ps' <- WI.orOneOf sym (L.folded . id) ps
        -- Add the condition from a conditional write
        WI.itePred sym (maybe (WI.truePred sym) CS.regValue mcond) ps' (WI.truePred sym)


  let ptrVal = CS.regValue ptr
  let (ptrBase, ptrOff) = CL.llvmPointerView ptrVal
  case WI.asNat ptrBase of
    Just 0 -> do
      p <- mkPred ptrOff
      let msg = printf "%s outside of static memory range (known BlockID 0): %s" (show (MS.pointerUseTag puse)) (show (WI.printSymExpr ptrOff))
      let loc = MS.pointerUseLocation puse
      let assertion = CB.LabeledPred p (CS.SimError loc (CS.GenericSimError msg))
      return (Just assertion)
    Just _ -> return Nothing
    Nothing -> do
      -- In this case, we don't know for sure if the block id is 0, but it could
      -- be (it is symbolic).  The assertion has to be conditioned on the equality.
      p <- mkPred ptrOff
      zeroNat <- WI.natLit sym 0
      isZeroBase <- WI.natEq sym zeroNat ptrBase
      p' <- WI.itePred sym isZeroBase p (WI.truePred sym)
      let msg = printf "%s outside of static memory range (unknown BlockID): %s" (show (MS.pointerUseTag puse)) (show (WI.printSymExpr ptrOff))
      let loc = MS.pointerUseLocation puse
      let assertion = CB.LabeledPred p' (CS.SimError loc (CS.GenericSimError msg))
      return (Just assertion)

-- | The shared implementation for the @mapRegionPointers@ function in the
-- default memory model ("Data.Macaw.Symbolic.Memory") and the lazy memory model
-- ("Data.Macaw.Symbolic.Memory.Lazy").
mapRegionPointersCommon ::
     ( MC.MemWidth w
     , 16 <= w
     , CB.IsSymInterface sym
     , CL.HasLLVMAnn sym
     , ?memOpts :: CL.MemOptions
     )
  => CL.LLVMPtr sym w
  -> MS.GlobalMap sym CL.Mem w
mapRegionPointersCommon ptr = MS.GlobalMap $ \bak mem regionNum offsetVal ->
  let sym = CB.backendGetSym bak in
  case WI.asNat regionNum of
    Just 0 -> do
      let ?ptrWidth = WI.bvWidth offsetVal
      CL.doPtrAddOffset bak mem ptr offsetVal
    Just _ ->
      -- This is the case where the region number is concrete and non-zero,
      -- meaning that it is already an LLVM pointer
      --
      -- NOTE: This case is not possible because we only call this from
      -- 'tryGlobPtr', which handles this case separately
      return (CL.LLVMPointer regionNum offsetVal)
    Nothing -> do
      -- In this case, the region number is symbolic, so we need to be very
      -- careful to handle the possibility that it is zero (and thus must be
      -- conditionally mapped to one or all of our statically-allocated regions.
      --
      -- NOTE: We can avoid making a huge static mux over all regions: the
      -- low-level memory model code already handles building the mux tree as it
      -- walks backwards over all allocations that are live.
      --
      -- We just need to add one top-level mux:
      --
      -- > ite (blockid == 0) (translate base) (leave alone)
      let ?ptrWidth = WI.bvWidth offsetVal
      zeroNat <- WI.natLit sym 0
      isZeroRegion <- WI.natEq sym zeroNat regionNum
      -- The pointer mapped to global memory (if the region number is zero)
      globalPtr <- CL.doPtrAddOffset bak mem ptr offsetVal
      CL.muxLLVMPtr sym isZeroRegion globalPtr (CL.LLVMPointer regionNum offsetVal)

-- | Convert each byte in a 'MC.MemChunk' to the corresponding bytes. These
-- can possibly be symbolic bytes depending on the behavior of the
-- 'GlobalMemoryHooks'.
populateMemChunkBytes ::
     ( MonadIO m
     , CB.IsSymBackend sym bak
     , MC.MemWidth w
     )
  => bak
  -> GlobalMemoryHooks w
  -> MC.Memory w
  -> MC.MemSegment w
  -> MC.MemAddr w
  -> MC.MemChunk w
  -> m [WI.SymBV sym 8]
populateMemChunkBytes bak hooks mem seg addr memChunk =
  liftIO $
  case memChunk of
    MC.RelocationRegion reloc ->
      populateRelocation hooks bak mem seg addr reloc
    MC.BSSRegion sz ->
      replicate (fromIntegral sz) <$> WI.bvLit sym w8 (BV.zero w8)
    MC.ByteRegion bytes ->
      traverse (WI.bvLit sym w8 . BV.word8) $ BS.unpack bytes
  where
    sym = CB.backendGetSym bak
    w8 = WI.knownNat @8

-- | Populate the memory backing global memory by assuming that the elements
-- of the array are equal to the appropriate bytes.
assumeMemArr ::
     forall sym bak w t st fs m f
   . ( CB.IsSymBackend sym bak
     , sym ~ WEB.ExprBuilder t st fs
     , MC.MemWidth w
     , MonadIO m
     , FWI.FoldableWithIndex Int f
     )
  => bak
  -> WI.SymArray sym (Ctx.SingleCtx (WI.BaseBVType w)) (WI.BaseBVType 8)
  -> MC.MemWord w
  -> f (WI.SymBV sym 8)
  -> m ()
assumeMemArr bak symArray absAddr bytes = do
    -- We used to assert the equality of each byte separately.  This ended up
    -- being very slow for large binaries, as it synchronizes the pipe to the
    -- solver after each assertion. Instead, we now encode all of the initial
    -- values as equalities and generate a large conjunction that asserts them
    -- all at once.
    --
    -- The roundabout encoding below (using the low-level 'WEB.sbMakeExpr'
    -- API) is used because the natural encoding (using 'WI.andPred') attempts
    -- to apply an optimization called absorbtion (which attempts to discard
    -- redundant conjuncts). That optimization is quadratic in cost, which
    -- makes this encoding intractably expensive for large terms.  By using
    -- 'WEB.sbMakeExpr', we avoid that optimization (which will never fire for
    -- this term anyway, as there are no redundant conjuncts).
    initVals <- ipleatM [] bytes $ \idx bmvals byte -> do
      let absByteAddr = fromIntegral idx + absAddr
      index_bv <- liftIO $ WI.bvLit sym w (BV.mkBV w (toInteger absByteAddr))
      eq_pred <- liftIO $ WI.bvEq sym byte =<< WI.arrayLookup sym symArray (Ctx.singleton index_bv)
      return (eq_pred : bmvals)
    let desc = printf "Bytes@[addr=%s,nbytes=%s]" (show absAddr) (show (F.toList bytes))
    prog_loc <- liftIO $ WI.getCurrentProgramLoc sym
    byteEqualityAssertion <- liftIO $ WEB.sbMakeExpr sym (WEA.ConjPred (BoolMap.fromVars [(e, BoolMap.Positive) | e <- initVals]))
    liftIO $ CB.addAssumption bak (CB.GenericAssumption prog_loc desc byteEqualityAssertion)
  where
    sym = CB.backendGetSym bak
    w = MC.memWidthNatRepr @w

-- | The 'pleatM' function is 'foldM' with the arguments switched so
-- that the function is last.
pleatM :: (Monad m, F.Foldable t)
       => b
       -> t a
       -> (b -> a -> m b)
       -> m b
pleatM s l f = F.foldlM f s l

-- | The 'ipleatM' function is 'FWI.ifoldM' with the arguments switched so
-- that the function is last.
ipleatM :: (Monad m, FWI.FoldableWithIndex i t)
        => b
        -> t a
        -> (i -> b -> a -> m b)
        -> m b
ipleatM s l f = FWI.ifoldlM f s l