-- |
-- Module           : Lang.Crucible.LLVM.Intrinsics.Libc
-- Description      : Override definitions for C standard library functions
-- Copyright        : (c) Galois, Inc 2015-2019
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}

module Lang.Crucible.LLVM.Intrinsics.Libc
  ( module Lang.Crucible.LLVM.Intrinsics.Libc
  , module Lang.Crucible.LLVM.Intrinsics.Libc.Math
  , module Lang.Crucible.LLVM.Intrinsics.Libc.Stdio
  , module Lang.Crucible.LLVM.Intrinsics.Libc.Stdlib
  , module Lang.Crucible.LLVM.Intrinsics.Libc.String
  ) where

import qualified Codec.Binary.UTF8.Generic as UTF8
import           Control.Monad (when)
import           Control.Monad.IO.Class (liftIO)
import           Lens.Micro ((^.))

import           Data.Parameterized.Context ( pattern (:>), pattern Empty )
import qualified Data.Parameterized.Context as Ctx

import           What4.Interface

import           Lang.Crucible.Backend
import           Lang.Crucible.CFG.Common
import           Lang.Crucible.Types
import           Lang.Crucible.Simulator.OverrideSim
import           Lang.Crucible.Simulator.RegMap
import           Lang.Crucible.Simulator.SimError

import           Lang.Crucible.LLVM.DataLayout
import           Lang.Crucible.LLVM.MemModel
import           Lang.Crucible.LLVM.MemModel.Strings as CStr
import           Lang.Crucible.LLVM.QQ( llvmOvr )
import           Lang.Crucible.LLVM.TypeContext

import           Lang.Crucible.LLVM.Intrinsics.Common
import           Lang.Crucible.LLVM.Intrinsics.Libc.Math
import           Lang.Crucible.LLVM.Intrinsics.Libc.Stdio
import           Lang.Crucible.LLVM.Intrinsics.Libc.Stdlib
import           Lang.Crucible.LLVM.Intrinsics.Libc.String
import           Lang.Crucible.LLVM.Intrinsics.Options

-- | All libc overrides.
--
-- This list is useful to other Crucible frontends based on the LLVM memory
-- model (e.g., Macaw).
libc_overrides ::
  ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
  , ?lc :: TypeContext, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
  [SomeLLVMOverride p sym ext]
libc_overrides :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?lc::TypeContext, ?intrinsicsOpts::IntrinsicsOptions,
 ?memOpts::MemOptions) =>
[SomeLLVMOverride p sym ext]
libc_overrides =
  [ LLVMOverride
  p
  sym
  ext
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType 32)
   ::> LLVMPointerType wptr)
  UnitType
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType 32)
   ::> LLVMPointerType wptr)
  UnitType
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?intrinsicsOpts::IntrinsicsOptions, ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType 32)
   ::> LLVMPointerType wptr)
  UnitType
llvmAssertRtnOverride
  , LLVMOverride
  p
  sym
  ext
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType 32)
   ::> LLVMPointerType wptr)
  UnitType
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType 32)
   ::> LLVMPointerType wptr)
  UnitType
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?intrinsicsOpts::IntrinsicsOptions, ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType 32)
   ::> LLVMPointerType wptr)
  UnitType
llvmAssertFailOverride
  , LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
forall sym p ext.
(IsSymInterface sym, ?lc::TypeContext) =>
LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
llvmHtonlOverride
  , LLVMOverride p sym ext (EmptyCtx ::> BVType 16) (BVType 16)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride p sym ext (EmptyCtx ::> BVType 16) (BVType 16)
forall sym p ext.
(IsSymInterface sym, ?lc::TypeContext) =>
LLVMOverride p sym ext (EmptyCtx ::> BVType 16) (BVType 16)
llvmHtonsOverride
  , LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
forall sym p ext.
(IsSymInterface sym, ?lc::TypeContext) =>
LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
llvmNtohlOverride
  , LLVMOverride p sym ext (EmptyCtx ::> BVType 16) (BVType 16)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride p sym ext (EmptyCtx ::> BVType 16) (BVType 16)
forall sym p ext.
(IsSymInterface sym, ?lc::TypeContext) =>
LLVMOverride p sym ext (EmptyCtx ::> BVType 16) (BVType 16)
llvmNtohsOverride
  ]
  [SomeLLVMOverride p sym ext]
-> [SomeLLVMOverride p sym ext] -> [SomeLLVMOverride p sym ext]
forall a. [a] -> [a] -> [a]
++ [SomeLLVMOverride p sym ext]
forall sym p ext.
IsSymInterface sym =>
[SomeLLVMOverride p sym ext]
mathOverrides
  [SomeLLVMOverride p sym ext]
-> [SomeLLVMOverride p sym ext] -> [SomeLLVMOverride p sym ext]
forall a. [a] -> [a] -> [a]
++ [SomeLLVMOverride p sym ext]
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
[SomeLLVMOverride p sym ext]
stdioOverrides
  [SomeLLVMOverride p sym ext]
-> [SomeLLVMOverride p sym ext] -> [SomeLLVMOverride p sym ext]
forall a. [a] -> [a] -> [a]
++ [SomeLLVMOverride p sym ext]
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?lc::TypeContext, ?intrinsicsOpts::IntrinsicsOptions,
 ?memOpts::MemOptions) =>
[SomeLLVMOverride p sym ext]
stdlibOverrides
  [SomeLLVMOverride p sym ext]
-> [SomeLLVMOverride p sym ext] -> [SomeLLVMOverride p sym ext]
forall a. [a] -> [a] -> [a]
++ [SomeLLVMOverride p sym ext]
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
[SomeLLVMOverride p sym ext]
stringOverrides

------------------------------------------------------------------------
-- ** Implementations

callAssert
  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
     , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions )
  => GlobalVar Mem
  -> Ctx.Assignment (RegEntry sym)
        (EmptyCtx ::> LLVMPointerType wptr
                  ::> LLVMPointerType wptr
                  ::> BVType 32
                  ::> LLVMPointerType wptr)
  -> forall r args reg.
     OverrideSim p sym ext r args reg (RegValue sym UnitType)
callAssert :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?intrinsicsOpts::IntrinsicsOptions, ?memOpts::MemOptions) =>
GlobalVar Mem
-> Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType 32)
      ::> LLVMPointerType wptr)
-> forall r (args :: Ctx CrucibleType) (reg :: CrucibleType).
   OverrideSim p sym ext r args reg (RegValue sym UnitType)
callAssert GlobalVar Mem
mvar (Assignment (RegEntry sym) ctx
Empty :> RegEntry sym tp
_pfn :> RegEntry sym tp
_pfile :> RegEntry sym tp
_pline :> RegEntry sym tp
ptxt ) =
  (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext r args reg (RegValue sym UnitType))
-> OverrideSim p sym ext r args reg (RegValue sym UnitType)
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak -> OverrideSim p sym ext r args reg (RegValue sym UnitType))
 -> OverrideSim p sym ext r args reg (RegValue sym UnitType))
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym ext r args reg (RegValue sym UnitType))
-> OverrideSim p sym ext r args reg (RegValue sym UnitType)
forall a b. (a -> b) -> a -> b
$ \bak
bak -> do
    let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
    Bool
-> OverrideSim p sym ext r args reg ()
-> OverrideSim p sym ext r args reg ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when Bool
failUponExit (OverrideSim p sym ext r args reg ()
 -> OverrideSim p sym ext r args reg ())
-> OverrideSim p sym ext r args reg ()
-> OverrideSim p sym ext r args reg ()
forall a b. (a -> b) -> a -> b
$
      do MemImpl sym
mem <- GlobalVar Mem
-> OverrideSim p sym ext r args reg (RegValue sym Mem)
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
GlobalVar tp
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
readGlobal GlobalVar Mem
mvar
         [Word8]
txt <- IO [Word8] -> OverrideSim p sym ext r args reg [Word8]
forall a. IO a -> OverrideSim p sym ext r args reg a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO [Word8] -> OverrideSim p sym ext r args reg [Word8])
-> IO [Word8] -> OverrideSim p sym ext r args reg [Word8]
forall a b. (a -> b) -> a -> b
$ bak -> MemImpl sym -> LLVMPtr sym wptr -> Maybe Int -> IO [Word8]
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak -> MemImpl sym -> LLVMPtr sym wptr -> Maybe Int -> IO [Word8]
CStr.loadString bak
bak MemImpl sym
mem (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym tp
ptxt) Maybe Int
forall a. Maybe a
Nothing
         let err :: SimErrorReason
err = String -> String -> SimErrorReason
AssertFailureSimError String
"Call to assert()" ([Word8] -> String
forall b s. UTF8Bytes b s => b -> String
UTF8.toString [Word8]
txt)
         IO () -> OverrideSim p sym ext r args reg ()
forall a. IO a -> OverrideSim p sym ext r args reg a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> OverrideSim p sym ext r args reg ())
-> IO () -> OverrideSim p sym ext r args reg ()
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO ()
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak SimErrorReason
err
    IO () -> OverrideSim p sym ext r args reg ()
forall a. IO a -> OverrideSim p sym ext r args reg a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> OverrideSim p sym ext r args reg ())
-> IO () -> OverrideSim p sym ext r args reg ()
forall a b. (a -> b) -> a -> b
$
      do ProgramLoc
loc <- IO ProgramLoc -> IO ProgramLoc
forall a. IO a -> IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO ProgramLoc -> IO ProgramLoc) -> IO ProgramLoc -> IO ProgramLoc
forall a b. (a -> b) -> a -> b
$ sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
         AbortExecReason -> IO ()
forall a. AbortExecReason -> IO a
abortExecBecause (AbortExecReason -> IO ()) -> AbortExecReason -> IO ()
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> AbortExecReason
EarlyExit ProgramLoc
loc
  where
    failUponExit :: Bool
    failUponExit :: Bool
failUponExit
      = IntrinsicsOptions -> AbnormalExitBehavior
abnormalExitBehavior ?intrinsicsOpts::IntrinsicsOptions
IntrinsicsOptions
?intrinsicsOpts AbnormalExitBehavior -> [AbnormalExitBehavior] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` [AbnormalExitBehavior
AlwaysFail, AbnormalExitBehavior
OnlyAssertFail]


------------------------------------------------------------------------
-- *** Other

-- from OSX libc
llvmAssertRtnOverride
  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
     , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions )
  => LLVMOverride p sym ext
        (EmptyCtx ::> LLVMPointerType wptr
                  ::> LLVMPointerType wptr
                  ::> BVType 32
                  ::> LLVMPointerType wptr)
        UnitType
llvmAssertRtnOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?intrinsicsOpts::IntrinsicsOptions, ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType 32)
   ::> LLVMPointerType wptr)
  UnitType
llvmAssertRtnOverride =
  [llvmOvr| void @__assert_rtn( i8*, i8*, i32, i8* ) |]
  IsSymInterface sym =>
GlobalVar Mem
-> Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType 32)
      ::> LLVMPointerType wptr)
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim p sym ext rtp args' ret' (RegValue sym UnitType)
GlobalVar Mem
-> Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType 32)
      ::> LLVMPointerType wptr)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym UnitType)
GlobalVar Mem
-> Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType 32)
      ::> LLVMPointerType wptr)
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim p sym ext rtp args' ret' (RegValue sym UnitType)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?intrinsicsOpts::IntrinsicsOptions, ?memOpts::MemOptions) =>
GlobalVar Mem
-> Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType 32)
      ::> LLVMPointerType wptr)
-> forall r (args :: Ctx CrucibleType) (reg :: CrucibleType).
   OverrideSim p sym ext r args reg (RegValue sym UnitType)
callAssert

-- From glibc
llvmAssertFailOverride
  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
     , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions )
  => LLVMOverride p sym ext
        (EmptyCtx ::> LLVMPointerType wptr
                  ::> LLVMPointerType wptr
                  ::> BVType 32
                  ::> LLVMPointerType wptr)
        UnitType
llvmAssertFailOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?intrinsicsOpts::IntrinsicsOptions, ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType 32)
   ::> LLVMPointerType wptr)
  UnitType
llvmAssertFailOverride =
  [llvmOvr| void @__assert_fail( i8*, i8*, i32, i8* ) |]
  IsSymInterface sym =>
GlobalVar Mem
-> Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType 32)
      ::> LLVMPointerType wptr)
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim p sym ext rtp args' ret' (RegValue sym UnitType)
GlobalVar Mem
-> Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType 32)
      ::> LLVMPointerType wptr)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym UnitType)
GlobalVar Mem
-> Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType 32)
      ::> LLVMPointerType wptr)
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim p sym ext rtp args' ret' (RegValue sym UnitType)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?intrinsicsOpts::IntrinsicsOptions, ?memOpts::MemOptions) =>
GlobalVar Mem
-> Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType 32)
      ::> LLVMPointerType wptr)
-> forall r (args :: Ctx CrucibleType) (reg :: CrucibleType).
   OverrideSim p sym ext r args reg (RegValue sym UnitType)
callAssert



llvmHtonlOverride ::
  (IsSymInterface sym, ?lc :: TypeContext) =>
  LLVMOverride p sym ext
      (EmptyCtx ::> BVType 32)
      (BVType 32)
llvmHtonlOverride :: forall sym p ext.
(IsSymInterface sym, ?lc::TypeContext) =>
LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
llvmHtonlOverride =
  [llvmOvr| i32 @htonl( i32 ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
args -> CurryAssignment
  (EmptyCtx ::> BVType 32)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32)))
-> Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> BVType 32) f x
-> Assignment f (EmptyCtx ::> BVType 32) -> x
Ctx.uncurryAssignment (NatRepr 4
-> RegEntry sym (BVType (4 * 8))
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (BVType (4 * 8)))
forall (width :: Natural) sym p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(1 <= width, IsSymInterface sym, ?lc::TypeContext) =>
NatRepr width
-> RegEntry sym (BVType (width * 8))
-> OverrideSim
     p sym ext r args ret (RegValue sym (BVType (width * 8)))
callBSwapIfLittleEndian (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @4)) Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
args)

llvmHtonsOverride ::
  (IsSymInterface sym, ?lc :: TypeContext) =>
  LLVMOverride p sym ext
      (EmptyCtx ::> BVType 16)
      (BVType 16)
llvmHtonsOverride :: forall sym p ext.
(IsSymInterface sym, ?lc::TypeContext) =>
LLVMOverride p sym ext (EmptyCtx ::> BVType 16) (BVType 16)
llvmHtonsOverride =
  [llvmOvr| i16 @htons( i16 ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> BVType 16)
args -> CurryAssignment
  (EmptyCtx ::> BVType 16)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 16)))
-> Assignment (RegEntry sym) (EmptyCtx ::> BVType 16)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 16))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> BVType 16) f x
-> Assignment f (EmptyCtx ::> BVType 16) -> x
Ctx.uncurryAssignment (NatRepr 2
-> RegEntry sym (BVType (2 * 8))
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (BVType (2 * 8)))
forall (width :: Natural) sym p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(1 <= width, IsSymInterface sym, ?lc::TypeContext) =>
NatRepr width
-> RegEntry sym (BVType (width * 8))
-> OverrideSim
     p sym ext r args ret (RegValue sym (BVType (width * 8)))
callBSwapIfLittleEndian (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @2)) Assignment (RegEntry sym) (EmptyCtx ::> BVType 16)
args)

llvmNtohlOverride ::
  (IsSymInterface sym, ?lc :: TypeContext) =>
  LLVMOverride p sym ext
      (EmptyCtx ::> BVType 32)
      (BVType 32)
llvmNtohlOverride :: forall sym p ext.
(IsSymInterface sym, ?lc::TypeContext) =>
LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
llvmNtohlOverride =
  [llvmOvr| i32 @ntohl( i32 ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
args -> CurryAssignment
  (EmptyCtx ::> BVType 32)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32)))
-> Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> BVType 32) f x
-> Assignment f (EmptyCtx ::> BVType 32) -> x
Ctx.uncurryAssignment (NatRepr 4
-> RegEntry sym (BVType (4 * 8))
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (BVType (4 * 8)))
forall (width :: Natural) sym p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(1 <= width, IsSymInterface sym, ?lc::TypeContext) =>
NatRepr width
-> RegEntry sym (BVType (width * 8))
-> OverrideSim
     p sym ext r args ret (RegValue sym (BVType (width * 8)))
callBSwapIfLittleEndian (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @4)) Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
args)

llvmNtohsOverride ::
  (IsSymInterface sym, ?lc :: TypeContext) =>
  LLVMOverride p sym ext
      (EmptyCtx ::> BVType 16)
      (BVType 16)
llvmNtohsOverride :: forall sym p ext.
(IsSymInterface sym, ?lc::TypeContext) =>
LLVMOverride p sym ext (EmptyCtx ::> BVType 16) (BVType 16)
llvmNtohsOverride =
  [llvmOvr| i16 @ntohs( i16 ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> BVType 16)
args -> CurryAssignment
  (EmptyCtx ::> BVType 16)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 16)))
-> Assignment (RegEntry sym) (EmptyCtx ::> BVType 16)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 16))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> BVType 16) f x
-> Assignment f (EmptyCtx ::> BVType 16) -> x
Ctx.uncurryAssignment (NatRepr 2
-> RegEntry sym (BVType (2 * 8))
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (BVType (2 * 8)))
forall (width :: Natural) sym p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(1 <= width, IsSymInterface sym, ?lc::TypeContext) =>
NatRepr width
-> RegEntry sym (BVType (width * 8))
-> OverrideSim
     p sym ext r args ret (RegValue sym (BVType (width * 8)))
callBSwapIfLittleEndian (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @2)) Assignment (RegEntry sym) (EmptyCtx ::> BVType 16)
args)


callBSwap ::
  (1 <= width, IsSymInterface sym) =>
  NatRepr width ->
  RegEntry sym (BVType (width * 8)) ->
  OverrideSim p sym ext r args ret (RegValue sym (BVType (width * 8)))
callBSwap :: forall (width :: Natural) sym p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(1 <= width, IsSymInterface sym) =>
NatRepr width
-> RegEntry sym (BVType (width * 8))
-> OverrideSim
     p sym ext r args ret (RegValue sym (BVType (width * 8)))
callBSwap NatRepr width
widthRepr (RegEntry sym (BVType (width * 8))
-> RegValue sym (BVType (width * 8))
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (BVType (width * 8))
vec) = do
  sym
sym <- OverrideSim p sym ext r args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
  IO (SymExpr sym ('BaseBVType (width * 8)))
-> OverrideSim
     p sym ext r args ret (SymExpr sym ('BaseBVType (width * 8)))
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym ('BaseBVType (width * 8)))
 -> OverrideSim
      p sym ext r args ret (SymExpr sym ('BaseBVType (width * 8))))
-> IO (SymExpr sym ('BaseBVType (width * 8)))
-> OverrideSim
     p sym ext r args ret (SymExpr sym ('BaseBVType (width * 8)))
forall a b. (a -> b) -> a -> b
$ sym
-> NatRepr width
-> SymExpr sym ('BaseBVType (width * 8))
-> IO (SymExpr sym ('BaseBVType (width * 8)))
forall sym (n :: Natural).
(1 <= n, IsExprBuilder sym) =>
sym -> NatRepr n -> SymBV sym (n * 8) -> IO (SymBV sym (n * 8))
bvSwap sym
sym NatRepr width
widthRepr RegValue sym (BVType (width * 8))
SymExpr sym ('BaseBVType (width * 8))
vec


-- | If the data layout is little-endian, run 'callBSwap' on the input.
-- Otherwise, return the input unchanged. This is the workhorse for the
-- @hton{s,l}@ and @ntoh{s,l}@ overrides.
callBSwapIfLittleEndian ::
  (1 <= width, IsSymInterface sym, ?lc :: TypeContext) =>
  NatRepr width ->
  RegEntry sym (BVType (width * 8)) ->
  OverrideSim p sym ext r args ret (RegValue sym (BVType (width * 8)))
callBSwapIfLittleEndian :: forall (width :: Natural) sym p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(1 <= width, IsSymInterface sym, ?lc::TypeContext) =>
NatRepr width
-> RegEntry sym (BVType (width * 8))
-> OverrideSim
     p sym ext r args ret (RegValue sym (BVType (width * 8)))
callBSwapIfLittleEndian NatRepr width
widthRepr RegEntry sym (BVType (width * 8))
vec =
  case (TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc)DataLayout
-> Getting EndianForm DataLayout EndianForm -> EndianForm
forall s a. s -> Getting a s a -> a
^.Getting EndianForm DataLayout EndianForm
Lens' DataLayout EndianForm
intLayout of
    EndianForm
BigEndian    -> SymExpr sym ('BaseBVType (width * 8))
-> OverrideSim
     p sym ext r args ret (SymExpr sym ('BaseBVType (width * 8)))
forall a. a -> OverrideSim p sym ext r args ret a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (RegEntry sym (BVType (width * 8))
-> RegValue sym (BVType (width * 8))
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym (BVType (width * 8))
vec)
    EndianForm
LittleEndian -> NatRepr width
-> RegEntry sym (BVType (width * 8))
-> OverrideSim
     p sym ext r args ret (RegValue sym (BVType (width * 8)))
forall (width :: Natural) sym p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(1 <= width, IsSymInterface sym) =>
NatRepr width
-> RegEntry sym (BVType (width * 8))
-> OverrideSim
     p sym ext r args ret (RegValue sym (BVType (width * 8)))
callBSwap NatRepr width
widthRepr RegEntry sym (BVType (width * 8))
vec


----------------------------------------------------------------------------