crucible-llvm 0.9 → 0.10

raw patch · 49 files changed

+4620/−2396 lines, 49 filesdep +microlensdep +microlens-ghcdep +microlens-mtldep −lensdep ~basedep ~llvm-prettydep ~parameterized-utilsPVP ok

version bump matches the API change (PVP)

Dependencies added: microlens, microlens-ghc, microlens-mtl, microlens-th, oughta, time

Dependencies removed: lens

Dependency ranges changed: base, llvm-pretty, parameterized-utils

API changes (from Hackage documentation)

Files

• CHANGELOG.md +42/−2
• crucible-llvm.cabal +23/−8
• src/Lang/Crucible/LLVM.hs +5/−3
• src/Lang/Crucible/LLVM/Arch/X86.hs +3/−3
• src/Lang/Crucible/LLVM/ArraySizeProfile.hs +3/−5
• src/Lang/Crucible/LLVM/DataLayout.hs +12/−14
• src/Lang/Crucible/LLVM/Errors.hs +12/−10
• src/Lang/Crucible/LLVM/Errors/Poison.hs +71/−6
• src/Lang/Crucible/LLVM/Errors/UndefinedBehavior.hs +8/−5
• src/Lang/Crucible/LLVM/Eval.hs +2/−1
• src/Lang/Crucible/LLVM/Functions.hs +1/−1
• src/Lang/Crucible/LLVM/Globals.hs +2/−3
• src/Lang/Crucible/LLVM/Intrinsics.hs +86/−21
• src/Lang/Crucible/LLVM/Intrinsics/Cast.hs +351/−99
• src/Lang/Crucible/LLVM/Intrinsics/Common.hs +146/−84
• src/Lang/Crucible/LLVM/Intrinsics/Declare.hs +110/−0
• src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs +120/−1
• src/Lang/Crucible/LLVM/Intrinsics/Libc.hs +198/−1935
• src/Lang/Crucible/LLVM/Intrinsics/Libc/Math.hs +961/−0
• src/Lang/Crucible/LLVM/Intrinsics/Libc/Stdio.hs +306/−0
• src/Lang/Crucible/LLVM/Intrinsics/Libc/Stdlib.hs +487/−0
• src/Lang/Crucible/LLVM/Intrinsics/Libc/String.hs +443/−0
• src/Lang/Crucible/LLVM/Intrinsics/Libcxx.hs +88/−52
• src/Lang/Crucible/LLVM/MemModel.hs +6/−2
• src/Lang/Crucible/LLVM/MemModel/Common.hs +5/−4
• src/Lang/Crucible/LLVM/MemModel/Generic.hs +5/−4
• src/Lang/Crucible/LLVM/MemModel/MemLog.hs +2/−1
• src/Lang/Crucible/LLVM/MemModel/Partial.hs +7/−5
• src/Lang/Crucible/LLVM/MemModel/Pointer.hs +0/−16
• src/Lang/Crucible/LLVM/MemModel/Strings.hs +623/−3
• src/Lang/Crucible/LLVM/MemModel/Type.hs +1/−1
• src/Lang/Crucible/LLVM/MemModel/Value.hs +4/−2
• src/Lang/Crucible/LLVM/MemType.hs +1/−1
• src/Lang/Crucible/LLVM/QQ.hs +7/−41
• src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs +2/−1
• src/Lang/Crucible/LLVM/SimpleLoopFixpointCHC.hs +3/−1
• src/Lang/Crucible/LLVM/SimpleLoopInvariant.hs +6/−4
• src/Lang/Crucible/LLVM/Translation.hs +7/−6
• src/Lang/Crucible/LLVM/Translation/Aliases.hs +1/−1
• src/Lang/Crucible/LLVM/Translation/BlockInfo.hs +4/−0
• src/Lang/Crucible/LLVM/Translation/Constant.hs +5/−5
• src/Lang/Crucible/LLVM/Translation/Expr.hs +1/−1
• src/Lang/Crucible/LLVM/Translation/Instruction.hs +142/−12
• src/Lang/Crucible/LLVM/Translation/Monad.hs +5/−4
• src/Lang/Crucible/LLVM/TypeContext.hs +9/−7
• test/MemSetup.hs +20/−17
• test/TestBehavior.hs +266/−0
• test/TestMemory.hs +1/−1
• test/Tests.hs +7/−3

@@ -1,3 +1,43 @@+# 0.10 -- 2026-09-10++* Add support for GHC 9.12 (at 9.12.2) and bump from 9.10.1 to 9.10.3.+* **BREAKING:** Rename various bits associated with the "breakpoint"+  feature in accordance with renaming the feature to "cutpoint".+  In particular, `testBreakpointFunction` is now `testCutpointFunction`.+  Also, the family of LLVM symbols recognized now begins with `__cutpoint__`+  rather than `__breakpoint__`.+* Support LLVM 22.+* Remove `llvmOverride_declare :: Text.LLVM.AST.Declare` from `LLVMOverride`.++  * Add `Lang.Crucible.LLVM.Intrinsics.Declare` module.+  * Change functions in `Lang.Crucible.LLVM.Intrinsics` to work+    with `Lang.Crucible.LLVM.Intrinsics.Declare.Declare`s. To+    migrate, use `Lang.Crucible.LLVM.Intrinsics.Declare.fromLLVM`+    to translate `Text.LLVM.AST.Declare`s into+    `Lang.Crucible.LLVM.Intrinsics.Declare.Declare`s+  * `do_register_llvm_override` no longer does any mapping nor adaptation of+    types, use `Lang.Crucible.LLVM.Intrinsics.Cast.lowerLLVMOverride` for that.+  * Replace `build_llvm_override` with+    `Lang.Crucible.LLVM.Intrinsics.Cast.lowerLLVMOverride`.+  * Overhaul the API of `Lang.Crucible.LLVM.Intrinsics.Cast`.+  * Replace various fields of `LLVMOverride` with a `Declare`. To migrate:+    * Replace `llvmOverride_name` with `llvmOvSymbol`+    * Replace `llvmOverride_args` with `llvmOvArgs`+    * Replace `llvmOverride_ret` with `llvmOvRet`+* Support the `llvm.scmp.*` and `llvm.ucmp.*` three-way comparison intrinsics.+* Added `register_specific_llvm_overrides` to register overrides for a provided+  list of declarations and definitions rather than extracting them from a+  provided LLVM module.+* **BREAKING**: Changed `lookupMetadata` to take the new `llvm-pretty`-provided+  `UnnamedMdIdx` rather than the older simple `Int` value to refer to the index+  of the metadata to be looked up.+* **BREAKING**: `explainCex`, `concBadBehavior`, `concUB`, and `concPoison` now+  take a `FloatModeRepr` argument.+* Fix the semantics of the `fptoui` and `fptosi` instructions. These+  instructions now round towards zero (previously, they incorrectly rounded+  towards negative infinity), and they now report undefined behavior if the+  input does not fit in the return type.+ # 0.9 -- 2026-01-29  * The `LLVM_Debug` data constructor for `LLVMStmt`, as well as the related@@ -40,8 +80,8 @@   * `Lang.Crucible.LLVM.MemModel.ppLLVMIntrinsicTypes`   * `Lang.Crucible.LLVM.MemModel.ppLLVMMemIntrinsicType`   * `Lang.Crucible.LLVM.MemModel.Pointer.ppLLVMPointerIntrinsicType`-* Overrides for `strnlen`, `strcpy`, `strdup`, and `strndup` supported by new-  APIs in `Lang.Crucible.LLVM.MemModel.Strings`.+* Overrides for `memcmp`, `strcmp`, `strncmp`, `strnlen`, `strcpy`, `strdup`,+  and `strndup`, supported by new APIs in `Lang.Crucible.LLVM.MemModel.Strings`.  # 0.8.0 -- 2025-11-09 

@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name:          crucible-llvm-Version:       0.9+Version:       0.10 Author:        Galois Inc. Copyright:     (c) Galois, Inc 2014-2022 Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com@@ -48,7 +48,6 @@   ghc-options:     -Wall     -Werror=ambiguous-fields-    -Werror=compat-unqualified-imports     -Werror=deferred-type-errors     -Werror=deprecated-flags     -Werror=deprecations@@ -120,10 +119,14 @@       -Werror=deprecated-type-abstractions       -Werror=incomplete-record-selectors +  if impl(ghc < 9.12)+    ghc-options:+      -Werror=compat-unqualified-imports+ library   import: bldflags   build-depends:-    base >= 4.13 && < 4.21,+    base >= 4.13 && < 4.22,     attoparsec,     bv-sized >= 1.0.0,     bytestring,@@ -132,11 +135,14 @@     crucible-symio,     what4 >= 0.5,     extra,-    lens,+    microlens,+    microlens-ghc,+    microlens-mtl,+    microlens-th,     itanium-abi >= 0.1.1.1 && < 0.2,-    llvm-pretty >= 0.12.1 && < 0.15,+    llvm-pretty >= 0.15.0.0 && < 0.16,     mtl,-    parameterized-utils >= 2.1.5 && < 2.2,+    parameterized-utils >= 2.3 && < 2.4,     pretty,     prettyprinter >= 1.7.0,     text,@@ -166,6 +172,7 @@     Lang.Crucible.LLVM.Internal     Lang.Crucible.LLVM.Intrinsics     Lang.Crucible.LLVM.Intrinsics.Cast+    Lang.Crucible.LLVM.Intrinsics.Declare     Lang.Crucible.LLVM.Intrinsics.Libc     Lang.Crucible.LLVM.Intrinsics.LLVM     Lang.Crucible.LLVM.MalformedLLVMModule@@ -194,6 +201,10 @@     Lang.Crucible.LLVM.Extension.Arch     Lang.Crucible.LLVM.Extension.Syntax     Lang.Crucible.LLVM.Intrinsics.Common+    Lang.Crucible.LLVM.Intrinsics.Libc.Math+    Lang.Crucible.LLVM.Intrinsics.Libc.Stdio+    Lang.Crucible.LLVM.Intrinsics.Libc.Stdlib+    Lang.Crucible.LLVM.Intrinsics.Libc.String     Lang.Crucible.LLVM.Intrinsics.Libcxx     Lang.Crucible.LLVM.Intrinsics.Match     Lang.Crucible.LLVM.Intrinsics.Options@@ -221,6 +232,7 @@   main-is: Tests.hs   hs-source-dirs: test   other-modules: MemSetup+               , TestBehavior                , TestFunctions                , TestGlobals                , TestMemory@@ -228,17 +240,20 @@   build-depends:     base,     bv-sized,+    bytestring,     containers,     crucible,     crucible-llvm,     directory,     filepath,-    lens,     llvm-pretty,     llvm-pretty-bc-parser,-    lens,+    microlens,+    oughta >= 0.3 && < 0.4,     parameterized-utils,     process,+    text,+    time,     what4,     tasty,     tasty-quickcheck,

@@ -28,9 +28,11 @@   , llvmExtensionImpl   ) where -import           Control.Lens import           Control.Monad (when) import           Control.Monad.IO.Class+import           Data.Function ((&))+import           Lens.Micro ((^.))+import           Lens.Micro.Mtl (use) import qualified Text.LLVM.AST as L  import           Lang.Crucible.Analysis.Postdom@@ -100,13 +102,13 @@ --   'registerLazyModuleFn' for a description. registerLazyModule ::    (1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym) =>-   (LLVMTranslationWarning -> IO ()) {- ^ A callback for handling traslation warnings -} ->+   (LLVMTranslationWarning -> IO ()) {- ^ A callback for handling translation warnings -} ->    ModuleTranslation arch ->    OverrideSim p sym LLVM rtp l a () registerLazyModule handleWarning mtrans =    mapM_ (registerLazyModuleFn handleWarning mtrans) (map (L.decName.fst) (mtrans ^. modTransDefs)) --- | Lazily register the named function that is defnied in the given module+-- | Lazily register the named function that is defined in the given module --   translation. This will delay actually translating the function until it --   is called. This done by first installing a bootstrapping override that --   will peform the actual translation when first invoked, and then will backpatch

@@ -137,7 +137,7 @@  -- This is going to go away instance ShowFC ExtX86 where-  showFC _ _ = error "[ShowFC ExtX86] Not implmented."+  showFC _ _ = panic "ExtX86.showFC" ["Not implemented"]  instance TestEqualityFC ExtX86 where   testEqualityFC testSubterm =@@ -155,7 +155,7 @@  -- This is going away instance HashableFC ExtX86 where-  hashWithSaltFC _hash _s _x = error "[HashableFC ExtX86] Not implmented."+  hashWithSaltFC _hash _s _x = panic "ExtX86.hashWithSaltFC" ["Not implemented"]  instance FunctorFC ExtX86 where   fmapFC = fmapFCDefault@@ -167,7 +167,7 @@   traverseFC = $(U.structuralTraversal [t|ExtX86|] [])  instance PrettyApp ExtX86 where-  ppApp _pp _x = error "[PrettyApp ExtX86] XXX"+  ppApp _pp _x = panic "ExtX86.ppApp" ["Not implemented"]  instance TypeApp ExtX86 where   appType x =

@@ -31,12 +31,10 @@  , arraySizeProfile  ) where -import Control.Lens.TH--import Control.Lens--import Data.Type.Equality (testEquality)+import Data.Type.Equality (testEquality, (:~:)(Refl)) import Data.IORef+import Lens.Micro ((^.))+import Lens.Micro.TH (makeLenses) import Data.Text (Text) import qualified Data.Text as Text import qualified Data.Vector as Vector

@@ -38,16 +38,18 @@   , intWidthSize   ) where -import Control.Lens import Control.Monad.State.Strict import Data.Map (Map) import qualified Data.Map as Map import Data.Word (Word32)-import qualified Text.LLVM as L+import Lens.Micro (Lens', lens, (^.))+import Lens.Micro.Mtl ((.=), (%=), (?=)) import Numeric.Natural+import qualified Text.LLVM as L  import What4.Utils.Arithmetic import Lang.Crucible.LLVM.Bytes+import Lang.Crucible.Panic (panic)   ------------------------------------------------------------------------@@ -132,7 +134,7 @@  -- | Return maximum alignment constraint stored in tree. maxAlignmentInTree :: AlignInfo -> Alignment-maxAlignmentInTree (AT t) = foldrOf folded max noAlignment t+maxAlignmentInTree (AT t) = foldr max noAlignment (Map.elems t)  -- | Update alignment tree updateAlign :: Natural@@ -141,14 +143,10 @@             -> AlignInfo updateAlign w (AT t) ma = AT (Map.alter (const ma) w t) -type instance Index AlignInfo = Natural-type instance IxValue AlignInfo = Alignment--instance Ixed AlignInfo where-  ix k = at k . traverse--instance At AlignInfo where-  at k f m = updateAlign k m <$> indexed f k (findExact k m)+-- | Lens for accessing an alignment at a specific key in 'AlignInfo'.+atAlignInfo :: Natural -> Lens' AlignInfo (Maybe Alignment)+atAlignInfo k f m = updateAlign k m <$> f (findExact k m)+{-# INLINE atAlignInfo #-}  -- | Flags byte orientation of target machine. data EndianForm = BigEndian | LittleEndian@@ -226,7 +224,7 @@  -- | Insert alignment into spec. setAt :: Lens' DataLayout AlignInfo -> Natural -> Alignment -> State DataLayout ()-setAt f sz a = f . at sz ?= a+setAt f sz a = f . atAlignInfo sz ?= a  -- | The default data layout if no spec is defined. From the LLVM -- Language Reference: "When constructing the data layout for a given@@ -277,7 +275,7 @@           ]  fromSize :: Int -> Natural-fromSize i | i < 0 = error $ "Negative size given in data layout."+fromSize i | i < 0 = panic "fromSize" ["Negative size given in data layout."]            | otherwise = fromIntegral i  -- | Insert alignment into spec.@@ -285,7 +283,7 @@ setAtBits f spec st =   case fromBits (L.alignABI (L.storageAlignment st)) of     Left{} -> layoutWarnings %= (spec:)-    Right w -> f . at (fromSize (L.storageSize st)) .= Just w+    Right w -> f . atAlignInfo (fromSize (L.storageSize st)) .= Just w  -- | Insert alignment into spec. setBits :: Lens' DataLayout Alignment -> L.LayoutSpec -> L.NumBits -> State DataLayout ()

@@ -41,15 +41,14 @@  import           Prelude hiding (pred) -import           Control.Lens import           Data.Text (Text)- import           Data.Typeable (Typeable)+import           Lens.Micro (Lens', lens) import           GHC.Generics (Generic) import           Prettyprinter  import           What4.Interface-import           What4.Expr (GroundValue)+import           What4.Expr (ExprBuilder, Flags, FloatModeRepr, GroundValue)  import           Lang.Crucible.Simulator.RegValue (RegValue'(..)) import qualified Lang.Crucible.LLVM.Errors.MemoryError as ME@@ -67,13 +66,16 @@  deriving Typeable  concBadBehavior ::-  IsExprBuilder sym =>+  ( IsExprBuilder sym+  , sym ~ ExprBuilder t st (Flags fm)+  ) =>   sym ->+  FloatModeRepr fm ->   (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->   BadBehavior sym -> IO (BadBehavior sym)-concBadBehavior sym conc (BBUndefinedBehavior ub) =-  BBUndefinedBehavior <$> UB.concUB sym conc ub-concBadBehavior sym conc (BBMemoryError me) =+concBadBehavior sym fm conc (BBUndefinedBehavior ub) =+  BBUndefinedBehavior <$> UB.concUB sym fm conc ub+concBadBehavior sym _fm conc (BBMemoryError me) =   BBMemoryError <$> ME.concMemoryError sym conc me  -- -----------------------------------------------------------------------@@ -126,13 +128,13 @@ -- ----------------------------------------------------------------------- -- ** Lenses -classifier :: Simple Lens (LLVMSafetyAssertion sym) (BadBehavior sym)+classifier :: Lens' (LLVMSafetyAssertion sym) (BadBehavior sym) classifier = lens _classifier (\s v -> s { _classifier = v}) -predicate :: Simple Lens (LLVMSafetyAssertion sym) (Pred sym)+predicate :: Lens' (LLVMSafetyAssertion sym) (Pred sym) predicate = lens _predicate (\s v -> s { _predicate = v}) -extra :: Simple Lens (LLVMSafetyAssertion sym) (Maybe Text)+extra :: Lens' (LLVMSafetyAssertion sym) (Maybe Text) extra = lens _extra (\s v -> s { _extra = v})  explainBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann

@@ -49,14 +49,16 @@ import           Data.Parameterized.TraversableF (FunctorF(..), FoldableF(..), TraversableF(..)) import qualified Data.Parameterized.TH.GADT as U import           Data.Parameterized.ClassesC (TestEqualityC(..), OrdC(..))-import           Data.Parameterized.Classes (OrderingF(..), toOrdering)+import           Data.Parameterized.Classes (OrderingF(..), OrdF(..), toOrdering)  import           Lang.Crucible.LLVM.Errors.Standards import           Lang.Crucible.LLVM.MemModel.Pointer (LLVMPointerType, concBV, concPtr', ppPtr) import           Lang.Crucible.Simulator.RegValue (RegValue'(..)) import           Lang.Crucible.Types import qualified What4.Interface as W4I-import           What4.Expr (GroundValue)+import qualified What4.InterpretedFloatingPoint as W4IFP+import           What4.Expr (ExprBuilder, Flags, FloatModeRepr(..), GroundValue)+import qualified What4.Expr.GroundEval as W4GE  data Poison (e :: CrucibleType -> Type) where   -- | Arguments: @op1@, @op2@@@ -136,6 +138,18 @@   UiToFpNonNegative   :: (1 <= w)                       => e (BVType w)                       -> Poison e+  FpToUiNotRepresentable+                      :: (1 <= w)+                      => FloatInfoRepr fi+                      -> e (FloatType fi)+                      -> NatRepr w+                      -> Poison e+  FpToSiNotRepresentable+                      :: (1 <= w)+                      => FloatInfoRepr fi+                      -> e (FloatType fi)+                      -> NatRepr w+                      -> Poison e   TruncNoUnsignedWrap :: (1 <= w)                       => e (BVType w)                       -> Poison e@@ -172,6 +186,8 @@     GEPOutOfBounds _ _      -> LLVMRef LLVM8     ZExtNonNegative _       -> LLVMRef LLVM18     UiToFpNonNegative _     -> LLVMRef LLVM19+    FpToUiNotRepresentable _ _ _ -> LLVMRef LLVM8+    FpToSiNotRepresentable _ _ _ -> LLVMRef LLVM8     TruncNoUnsignedWrap _   -> LLVMRef LLVM20     TruncNoSignedWrap _     -> LLVMRef LLVM20     ICmpSameSign _ _        -> LLVMRef LLVM20@@ -201,6 +217,8 @@     GEPOutOfBounds _ _      -> "‘getelementptr’ Instruction (Semantics)"     ZExtNonNegative _       -> "‘zext’ Instruction (Semantics)"     UiToFpNonNegative _     -> "‘uitofp’ Instruction (Semantics)"+    FpToUiNotRepresentable _ _ _ -> "‘fptoui’ Instruction (Semantics)"+    FpToSiNotRepresentable _ _ _ -> "‘fptosi’ Instruction (Semantics)"     TruncNoUnsignedWrap _   -> "‘trunc’ Instruction (Semantics)"     TruncNoSignedWrap _     -> "‘trunc’ Instruction (Semantics)"     ICmpSameSign _ _        -> "‘icmp’ Instruction (Semantics)"@@ -263,6 +281,14 @@       "A negative integer was zero-extended even though the `nneg` flag was set"     UiToFpNonNegative _ ->       "A negative integer was converted to a floating-point value even though the `nneg` flag was set"+    FpToUiNotRepresentable _ _ _ -> cat $+      [ "A floating-point value was converted to an unsigned integer,"+      , "even though the value does not fit in the unsigned integer's type"+      ]+    FpToSiNotRepresentable _ _ _ -> cat $+      [ "A floating-point value was converted to a signed integer,"+      , "even though the value does not fit in the signed integer's type"+      ]     TruncNoUnsignedWrap _ ->       "Unsigned truncation caused wrapping even though the `nuw` flag was set"     TruncNoSignedWrap _ ->@@ -298,6 +324,16 @@       ]     ZExtNonNegative v -> args [v]     UiToFpNonNegative v -> args [v]+    FpToUiNotRepresentable fi (RV float) bvW ->+      [ "Floating-point type:" <+> pretty fi+      , "Floating-point value:" <+> W4I.printSymExpr float+      , "Unsigned integer size (in bits):" <+> viaShow bvW+      ]+    FpToSiNotRepresentable fi (RV float) bvW ->+      [ "Floating-point type:" <+> pretty fi+      , "Floating-point value:" <+> W4I.printSymExpr float+      , "Signed integer size (in bits):" <+> viaShow bvW+      ]     TruncNoUnsignedWrap v -> args [v]     TruncNoSignedWrap v -> args [v]     ICmpSameSign v1 v2 -> args [v1, v2]@@ -329,14 +365,35 @@ ppReg = pp details  -- | Concretize a poison error message.-concPoison :: forall sym.-  W4I.IsExprBuilder sym =>+concPoison :: forall sym t st fm.+  ( W4I.IsExprBuilder sym+  , sym ~ ExprBuilder t st (Flags fm)+  ) =>   sym ->+  FloatModeRepr fm ->   (forall tp. W4I.SymExpr sym tp -> IO (GroundValue tp)) ->   Poison (RegValue' sym) -> IO (Poison (RegValue' sym))-concPoison sym conc poison =+concPoison sym fm conc poison =   let bv :: forall w. (1 <= w) => RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))-      bv (RV x) = RV <$> concBV sym conc x in+      bv (RV x) = RV <$> concBV sym conc x++      fp ::+        forall fi.+        FloatInfoRepr fi ->+        RegValue' sym (FloatType fi) ->+        IO (RegValue' sym (FloatType fi))+      fp fi (RV x) = do+        v <- conc x+        rv <-+          case fm of+            FloatIEEERepr ->+              W4I.floatLit sym (floatInfoToPrecisionRepr fi) v+            FloatUninterpretedRepr -> do+              sv <- W4GE.groundToSym sym (floatInfoToBVTypeRepr fi) v+              W4IFP.iFloatFromBinary sym fi sv+            FloatRealRepr ->+              W4IFP.iFloatLitRational sym fi v+        pure $ RV rv in   case poison of     AddNoUnsignedWrap v1 v2 ->       AddNoUnsignedWrap <$> bv v1 <*> bv v2@@ -380,6 +437,10 @@       ZExtNonNegative <$> bv v     UiToFpNonNegative v ->       UiToFpNonNegative <$> bv v+    FpToUiNotRepresentable v1 v2 v3 ->+      FpToUiNotRepresentable v1 <$> fp v1 v2 <*> pure v3+    FpToSiNotRepresentable v1 v2 v3 ->+      FpToSiNotRepresentable v1 <$> fp v1 v2 <*> pure v3     TruncNoUnsignedWrap v ->       TruncNoUnsignedWrap <$> bv v     TruncNoSignedWrap v ->@@ -407,6 +468,8 @@            Nothing   -> Nothing    in $(U.structuralTypeEquality [t|Poison|]        [ ( U.DataArg 0 `U.TypeApp` U.AnyType, [| subterms' |])+       , ( U.ConType [t| FloatInfoRepr |] `U.TypeApp` U.AnyType, [| testEquality |])+       , ( U.ConType [t| NatRepr |] `U.TypeApp` U.AnyType, [| testEquality |])        ])  ordcPoison :: forall e f.@@ -422,6 +485,8 @@     in $(U.structuralTypeOrd [t|Poison|]        [ ( U.DataArg 0 `U.TypeApp` U.AnyType, [| subterms' |])+       , ( U.ConType [t| FloatInfoRepr |] `U.TypeApp` U.AnyType, [| compareF |])+       , ( U.ConType [t| NatRepr |] `U.TypeApp` U.AnyType, [| compareF |])        ])  instance TestEqualityC Poison where

@@ -71,7 +71,7 @@ import qualified Data.Parameterized.TraversableF as TF  import qualified What4.Interface as W4I-import           What4.Expr (GroundValue)+import           What4.Expr (ExprBuilder, Flags, FloatModeRepr, GroundValue)  import           Lang.Crucible.Types import           Lang.Crucible.Simulator.RegValue (RegValue'(..))@@ -560,12 +560,15 @@      ) subterms  -concUB :: forall sym.-  W4I.IsExprBuilder sym =>+concUB :: forall sym t st fm.+  ( W4I.IsExprBuilder sym+  , sym ~ ExprBuilder t st (Flags fm)+  ) =>   sym ->+  FloatModeRepr fm ->   (forall tp. W4I.SymExpr sym tp -> IO (GroundValue tp)) ->   UndefinedBehavior (RegValue' sym) -> IO (UndefinedBehavior (RegValue' sym))-concUB sym conc ub =+concUB sym fm conc ub =   let bv :: forall w. (1 <= w) => RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))       bv (RV x) = RV <$> concBV sym conc x in   case ub of@@ -614,4 +617,4 @@       AbsIntMin <$> bv v      PoisonValueCreated poison ->-      PoisonValueCreated <$> Poison.concPoison sym conc poison+      PoisonValueCreated <$> Poison.concPoison sym fm conc poison

@@ -7,10 +7,11 @@   , callStackFromMemVar   ) where -import           Control.Lens ((^.), view) import           Control.Monad (forM_) import qualified Data.List.NonEmpty as NE import           Data.Parameterized.TraversableF+import           Lens.Micro ((^.))+import           Lens.Micro.Extras (view)  import           What4.Interface 

@@ -55,12 +55,12 @@   , bindLLVMFunc   ) where -import           Control.Lens (use) import           Control.Monad (foldM) import           Control.Monad.IO.Class (liftIO) import qualified Data.Map as Map import qualified Data.Set as Set import           qualified Data.Text as Text+import           Lens.Micro.Mtl (use)  import qualified Text.LLVM.AST as L 

@@ -45,7 +45,6 @@ import           Control.Monad (foldM) import           Control.Monad.IO.Class (MonadIO(..)) import           Control.Monad.Except (MonadError(..))-import           Control.Lens hiding (op, (:>) ) import qualified Data.Foldable as Foldable import           Data.List (genericLength, isPrefixOf) import           Data.Map.Strict (Map)@@ -55,10 +54,10 @@ import           Control.Monad.State (StateT, runStateT, get, put) import           Data.Maybe (fromMaybe) import qualified Data.Parameterized.Context as Ctx+import           Data.Parameterized.NatRepr as NatRepr+import           Lens.Micro ((^.))  import qualified Text.LLVM.AST as L--import           Data.Parameterized.NatRepr as NatRepr  import           Lang.Crucible.LLVM.Bytes import           Lang.Crucible.LLVM.DataLayout

@@ -24,6 +24,7 @@ , LLVMOverride(..)  , register_llvm_overrides+, register_specific_llvm_overrides , register_llvm_overrides_ , llvmDeclToFunHandleRepr , declare_overrides@@ -33,9 +34,9 @@ , module Lang.Crucible.LLVM.Intrinsics.Match ) where -import           Control.Lens hiding (op, (:>), Empty) import           Control.Monad (forM) import           Data.Maybe (catMaybes)+import           Lens.Micro ((^.)) import qualified Text.LLVM.AST as L  import qualified ABI.Itanium as ABI@@ -53,6 +54,8 @@ import           Lang.Crucible.LLVM.TypeContext (TypeContext)  import           Lang.Crucible.LLVM.Intrinsics.Common+import qualified Lang.Crucible.LLVM.Intrinsics.Cast as Cast+import qualified Lang.Crucible.LLVM.Intrinsics.Declare as Decl import qualified Lang.Crucible.LLVM.Intrinsics.LLVM as LLVM import qualified Lang.Crucible.LLVM.Intrinsics.Libc as Libc import qualified Lang.Crucible.LLVM.Intrinsics.Libcxx as Libcxx@@ -65,9 +68,22 @@    MapF.insert (knownSymbol :: SymbolRepr "LLVM_pointer") IntrinsicMuxFn $    MapF.empty --- | Match two sets of 'OverrideTemplate's against the @declare@s and @define@s+-- | Match two sets of 'OverrideTemplate's against the @Declare@s and @Define@s -- in a 'L.Module', registering all the overrides that apply and returning them--- as a list.+-- as a list.  There are internal pre-determined overrides that will be applied,+-- as well as any additional overrides supplied by the user (internal overrides+-- will supercede user overrides).+--+-- The "define" overrides are applied to *both* the @Define@s and @Declare@s+-- elements found within a module.+--+-- The "declare" overrides are applied only to the @Declare@s found within a+-- module.  The intent is that these overrides should only apply to @Declare@s,+-- whereas the "define" overrides should apply to any matching symbol in the LLVM+-- @Module@.+--+-- If both lists specify an override that matches a declare, the declare override+-- takes precedence over the define override. register_llvm_overrides ::   ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch   , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>@@ -80,8 +96,38 @@ register_llvm_overrides llvmModule defineOvrs declareOvrs llvmctx =   do defOvs <- register_llvm_define_overrides llvmModule defineOvrs llvmctx      declOvs <- register_llvm_declare_overrides llvmModule declareOvrs llvmctx-     pure (defOvs,  declOvs)+     pure (defOvs, declOvs) ++-- | Match a set of 'OverrideTemplate's against a provided set of definitions and+-- declarations, registering all the overrides that apply and returning them as a+-- pair of lists: the registered definition overrides and the registered+-- declaration overrides.+--+-- This is an alternative entrypoint for registering overrides.  The+-- functionality here is largely the same as 'register_llvm_overrides' except the+-- list of declares and defines are provided manually by the caller instead of+-- being extracted from the LLVM @Module@.+register_specific_llvm_overrides ::+  IsSymInterface sym =>+  HasLLVMAnn sym =>+  HasPtrWidth wptr =>+  wptr ~ ArchWidth arch =>+  (?intrinsicsOpts :: IntrinsicsOptions) =>+  (?memOpts :: MemOptions) =>+  [L.Define] ->+  [L.Declare] ->+  [OverrideTemplate p sym LLVM arch] {- ^ Additional \"define\" overrides -} ->+  [OverrideTemplate p sym LLVM arch] {- ^ Additional \"declare\" overrides -} ->+  LLVMContext arch ->+  OverrideSim p sym LLVM rtp l a ( [SomeLLVMOverride p sym LLVM] -- ^ def overrides+                                 , [SomeLLVMOverride p sym LLVM] -- ^ decl overrides+                                 )+register_specific_llvm_overrides defs decls addlDefOvrs addlDeclOvrs llvmctx =+  (,)+  <$> register_overrides (declareFromDefine <$> defs) addlDefOvrs llvmctx+  <*> register_overrides decls addlDeclOvrs llvmctx+ -- | Filter the initial list of templates to only those that could -- possibly match the given declaration based on straightforward, -- relatively cheap string tests on the name of the declaration.@@ -91,10 +137,11 @@ -- and the structure of C++ demangled names to extract more information. filterTemplates ::   [OverrideTemplate p sym ext arch] ->-  L.Declare ->+  Decl.SomeDeclare ->   [OverrideTemplate p sym ext arch]-filterTemplates ts decl = filter (matches nm . overrideTemplateMatcher) ts- where L.Symbol nm = L.decName decl+filterTemplates ts (Decl.SomeDeclare decl) =+  filter (matches nm . overrideTemplateMatcher) ts+  where L.Symbol nm = Decl.decName decl  -- | Match a set of 'OverrideTemplate's against a single 'L.Declare', -- registering all the overrides that apply and returning them as a list.@@ -104,16 +151,17 @@   -- | Overrides to attempt to match against this declaration   [OverrideTemplate p sym ext arch] ->   -- | Declaration of the function that might get overridden-  L.Declare ->+  Decl.SomeDeclare ->   OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext]-match_llvm_overrides llvmctx acts decl =+match_llvm_overrides llvmctx acts someDecl =   llvmPtrWidth llvmctx $ \wptr -> withPtrWidth wptr $ do-    let acts' = filterTemplates acts decl-    let L.Symbol nm = L.decName decl+    let acts' = filterTemplates acts someDecl+    Decl.SomeDeclare decl <- pure someDecl+    let L.Symbol nm = Decl.decName decl     let declnm = either (const Nothing) Just $ ABI.demangleName nm     mbOvs <-       forM (map overrideTemplateAction acts') $ \(MakeOverride act) ->-        case act decl declnm llvmctx of+        case act someDecl declnm llvmctx of           Nothing -> pure Nothing           Just sov@(SomeLLVMOverride ov) -> do             register_llvm_override ov decl llvmctx@@ -128,30 +176,32 @@   -- | Overrides to attempt to match against these declarations   [OverrideTemplate p sym ext arch] ->   -- | Declarations of the functions that might get overridden-  [L.Declare] ->+  [Decl.SomeDeclare] ->   OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext] register_llvm_overrides_ llvmctx acts decls =   concat <$> forM decls (\decl -> match_llvm_overrides llvmctx acts decl)  -- | Match a set of 'OverrideTemplate's against all the @declare@s and @define@s -- in a 'L.Module', registering all the overrides that apply and returning them--- as a list.+-- as a list.  This should apply the override regardless of whether the override+-- applies to a @Define@ or a @Declare@. -- -- Registers a default set of overrides, in addition to the ones passed as an -- argument. register_llvm_define_overrides ::-  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>+  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch+  , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>   L.Module ->   -- | Additional (non-default) @define@ overrides   [OverrideTemplate p sym LLVM arch] ->   LLVMContext arch ->   OverrideSim p sym LLVM rtp l a [SomeLLVMOverride p sym LLVM] register_llvm_define_overrides llvmModule addlOvrs llvmctx =-  let ?lc = llvmctx^.llvmTypeCtx in-  register_llvm_overrides_ llvmctx (addlOvrs ++ define_overrides) $-     (allModuleDeclares llvmModule)+  let ?lc = llvmctx^.llvmTypeCtx+  in register_overrides (allModuleDeclares llvmModule) (addlOvrs ++ define_overrides)+     llvmctx --- | Match a set of 'OverrideTemplate's against all the @declare@s in a+-- | Match a set of 'OverrideTemplate's against all the @Declare@s in a -- 'L.Module', registering all the overrides that apply and returning them as -- a list. --@@ -167,9 +217,23 @@   OverrideSim p sym LLVM rtp l a [SomeLLVMOverride p sym LLVM] register_llvm_declare_overrides llvmModule addlOvrs llvmctx =   let ?lc = llvmctx^.llvmTypeCtx-  in register_llvm_overrides_ llvmctx (addlOvrs ++ declare_overrides) $-       L.modDeclares llvmModule+  in register_overrides (L.modDeclares llvmModule) (addlOvrs ++ declare_overrides)+     llvmctx +register_overrides ::+  ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch+  , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>+  [L.Declare] ->+  -- | Additional (non-default) @declare@ overrides+  [OverrideTemplate p sym LLVM arch] ->+  LLVMContext arch ->+  OverrideSim p sym LLVM rtp l a [SomeLLVMOverride p sym LLVM]+register_overrides llvmDecls ovrs llvmctx = do+  let ?lc = llvmctx^.llvmTypeCtx+  decls <- Decl.fromLLVMWithWarnings llvmDecls+  let ovs = map Cast.lowerOverrideTemplate ovrs+  register_llvm_overrides_ llvmctx ovs decls+ -- | Register overrides for declared-but-not-defined functions declare_overrides ::   ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch@@ -181,6 +245,7 @@   , map (\(SomeLLVMOverride ov) -> basic_llvm_override ov) LLVM.basic_llvm_overrides   , map (\(pfx, LLVM.Poly1LLVMOverride ov) -> polymorphic1_llvm_override pfx ov) LLVM.poly1_llvm_overrides   , map (\(pfx, LLVM.Poly1VecLLVMOverride ov) -> polymorphic1_vec_llvm_override pfx ov) LLVM.poly1_vec_llvm_overrides+  , map (\(pfx, LLVM.PolyCmpLLVMOverride ov) -> polymorphic_cmp_llvm_override pfx ov) LLVM.poly_cmp_llvm_overrides    -- C++ standard library functions   , [ Libcxx.register_cpp_override Libcxx.endlOverride ]

@@ -1,133 +1,385 @@ -- | -- Module           : Lang.Crucible.LLVM.Intrinsics.Cast--- Description      : Cast between bitvectors and pointers in signatures--- Copyright        : (c) Galois, Inc 2024+-- Description      : Casting to and from the Crucible-LLVM ABI+-- Copyright        : (c) Galois, Inc 2026 -- License          : BSD3 -- Maintainer       : Langston Barrett <langston@galois.com> -- Stability        : provisional ----- The built-in overrides in "Lang.Crucible.LLVM.Intrinsics.Libc" and--- "Lang.Crucible.LLVM.Intrinsics.LLVM" frequently take arguments of type--- 'Lang.Crucible.Types.BVType', but at runtime everything is represented as an--- 'Lang.Crucible.LLVM.MemModel.Pointer.LLVMPtr'. This module contains helpers--- for \"casting\" between pointers and bitvectors.+-- In Crucible-LLVM, LLVM pointers and integers are translated to terms+-- of type 'Lang.Crucible.LLVM.MemModel.Pointer.LLVMPointerType'. When+-- writing overrides, it can be convenient to take arguments or return+-- values of 'Lang.Crucible.Types.BVType'. This is done frequently in+-- the built-in overrides in "Lang.Crucible.LLVM.Intrinsics.Libc" and+-- "Lang.Crucible.LLVM.Intrinsics.LLVM". This module contains helpers for+-- \"lowering\" signatures using Crucible bitvectors to ones that use LLVM+-- pointers. ------------------------------------------------------------------------ -{-# LANGUAGE GADTs #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}  module Lang.Crucible.LLVM.Intrinsics.Cast-  ( ValCastError-  , printValCastError-  , ArgCast(applyArgCast)-  , ValCast(applyValCast)-  , castLLVMArgs-  , castLLVMRet+  ( -- * There+    CtxToLLVMType+  , ToLLVMType+  , ctxToLLVMType+  , toLLVMType+  , regValuesToLLVM+  , regValueToLLVM+    -- * Back again+  , regValuesFromLLVM+  , regValueFromLLVM+  , regEntriesFromLLVM+  , regMapFromLLVM+    -- * Lowering overrides+  , lowerLLVMOverride+  , lowerMakeOverride+  , lowerOverrideTemplate   ) where  import           Control.Monad.IO.Class (liftIO)-import           Control.Lens+import           Data.Coerce (coerce) import qualified Data.Text as Text+import           Data.Type.Equality ((:~:)(Refl), testEquality)  import qualified Data.Parameterized.Context as Ctx-import           Data.Parameterized.Some (Some(Some))-import           Data.Parameterized.TraversableFC (fmapFC)+import qualified Data.Parameterized.TraversableFC as TFC -import           What4.FunctionName (FunctionName (functionName))+import qualified What4.FunctionName as WFN -import           Lang.Crucible.Backend-import           Lang.Crucible.Simulator (SimErrorReason(AssertFailureSimError))-import           Lang.Crucible.Simulator.OverrideSim-import           Lang.Crucible.Simulator.RegMap-import           Lang.Crucible.Types+import qualified Lang.Crucible.Backend as CB+import           Lang.Crucible.Panic (panic)+import qualified Lang.Crucible.Simulator.OverrideSim as CSO+import qualified Lang.Crucible.Simulator.RegMap as CRM+import qualified Lang.Crucible.Simulator.RegValue as CRV+import qualified Lang.Crucible.Simulator.SimError as CSE+import qualified Lang.Crucible.Types as CT -import           Lang.Crucible.LLVM.MemModel.Partial (ptrToBv)-import           Lang.Crucible.LLVM.MemModel.Pointer+import qualified Lang.Crucible.LLVM.Intrinsics.Common as IC+import qualified Lang.Crucible.LLVM.Intrinsics.Declare as Decl+import           Lang.Crucible.LLVM.MemModel.Partial (HasLLVMAnn, ptrToBv)+import           Lang.Crucible.LLVM.MemModel.Pointer (LLVMPointerType)+import qualified Lang.Crucible.LLVM.MemModel.Pointer as Ptr -data ValCastError-  = -- | Mismatched number of arguments ('castLLVMArgs') or struct fields-    -- ('castLLVMRet').-    MismatchedShape-    -- | Can\'t cast between these types-  | ValCastError (Some TypeRepr) (Some TypeRepr)+---------------------------------------------------------------------+-- * There --- | Turn a 'ValCastError' into a human-readable message (lines).-printValCastError :: ValCastError -> [String]-printValCastError =+-- | Convert bitvectors to 'LLVMPointer's.+type CtxToLLVMType :: Ctx.Ctx CT.CrucibleType -> Ctx.Ctx CT.CrucibleType+type family CtxToLLVMType t where+  CtxToLLVMType Ctx.EmptyCtx = Ctx.EmptyCtx+  CtxToLLVMType (ctx Ctx.::> tp) = CtxToLLVMType ctx Ctx.::> ToLLVMType tp++-- | Convert bitvectors to 'LLVMPointer's.+type ToLLVMType :: CT.CrucibleType -> CT.CrucibleType+type family ToLLVMType t where+  ToLLVMType (CT.BVType w) = LLVMPointerType w++  -- recursive cases+  ToLLVMType (CT.VectorType tp) = CT.VectorType (ToLLVMType tp)+  ToLLVMType (CT.StructType ctx) = CT.StructType (CtxToLLVMType ctx)++  -- no-ops+  ToLLVMType CT.AnyType = CT.AnyType+  ToLLVMType CT.UnitType = CT.UnitType+  ToLLVMType CT.BoolType = CT.BoolType+  ToLLVMType CT.NatType = CT.NatType+  ToLLVMType CT.IntegerType = CT.IntegerType+  ToLLVMType CT.RealValType = CT.RealValType+  ToLLVMType (CT.FloatType flt) = CT.FloatType flt+  ToLLVMType (CT.IEEEFloatType ps) = CT.IEEEFloatType ps+  ToLLVMType CT.CharType = CT.CharType+  ToLLVMType (CT.StringType si) = CT.StringType si+  ToLLVMType (CT.ComplexRealType) = CT.ComplexRealType+  ToLLVMType (CT.IntrinsicType nm ctx) = CT.IntrinsicType nm ctx++  -- these shouldn't appear in override signaures, so don't worry about them+  ToLLVMType (CT.FunctionHandleType ctx ret) = CT.FunctionHandleType ctx ret+  ToLLVMType (CT.RecursiveType nm ctx) = CT.RecursiveType nm ctx+  ToLLVMType (CT.MaybeType tp) = CT.MaybeType tp+  ToLLVMType (CT.ReferenceType t) = CT.ReferenceType t+  ToLLVMType (CT.SequenceType tp) = CT.SequenceType tp+  ToLLVMType (CT.VariantType ctx) = CT.VariantType ctx+  ToLLVMType (CT.WordMapType n tp) = CT.WordMapType n tp+  ToLLVMType (CT.StringMapType tp) = CT.StringMapType tp+  ToLLVMType (CT.SymbolicArrayType idx t) = CT.SymbolicArrayType idx t+  ToLLVMType (CT.SymbolicStructType ctx) = CT.SymbolicStructType ctx++-- | Value-level analogue of 'CtxToLLVMType'+ctxToLLVMType ::+  Ctx.Assignment CT.TypeRepr ctx ->+  Ctx.Assignment CT.TypeRepr (CtxToLLVMType ctx)+ctxToLLVMType =   \case-    MismatchedShape -> ["argument shape mismatch"]-    ValCastError (Some ret) (Some ret') ->-      [ "Cannot cast types"-      , "*** Source type: " ++ show ret-      , "*** Target type: " ++ show ret'-      ]+    Ctx.Empty -> Ctx.empty+    ctx Ctx.:> t -> ctxToLLVMType ctx Ctx.:> toLLVMType t --- | A function to (infallibly) cast between 'Ctx.Assignment's of 'RegEntry's.-newtype ArgCast p sym ext args args' =-  ArgCast { applyArgCast :: (forall rtp l a.-    Ctx.Assignment (RegEntry sym) args ->-    OverrideSim p sym ext rtp l a (Ctx.Assignment (RegEntry sym) args')) }+-- | Value-level analogue of 'ToLLVMType'+toLLVMType ::+  CT.TypeRepr t ->+  CT.TypeRepr (ToLLVMType t)+toLLVMType =+  \case+    CT.BVRepr w -> Ptr.LLVMPointerRepr w --- | A function to (infallibly) cast a value of types @tp@ to @tp'@.-newtype ValCast p sym ext tp tp' =-  ValCast { applyValCast :: (forall rtp l a.-    RegValue sym tp ->-    OverrideSim p sym ext rtp l a (RegValue sym tp')) }+    -- recursive cases+    CT.VectorRepr tp -> CT.VectorRepr (toLLVMType tp)+    CT.StructRepr ctx -> CT.StructRepr (ctxToLLVMType ctx) --- | Attempt to construct a function to cast between 'Ctx.Assignment's of--- 'RegEntry's.-castLLVMArgs :: forall p sym ext bak args args'.-  IsSymBackend sym bak =>+    -- no-ops+    CT.AnyRepr -> CT.AnyRepr+    CT.UnitRepr -> CT.UnitRepr+    CT.BoolRepr -> CT.BoolRepr+    CT.NatRepr -> CT.NatRepr+    CT.IntegerRepr -> CT.IntegerRepr+    CT.RealValRepr -> CT.RealValRepr+    CT.FloatRepr flt -> CT.FloatRepr flt+    CT.IEEEFloatRepr ps -> CT.IEEEFloatRepr ps+    CT.CharRepr -> CT.CharRepr+    CT.StringRepr si -> CT.StringRepr si+    CT.ComplexRealRepr -> CT.ComplexRealRepr+    CT.IntrinsicRepr nm ctx -> CT.IntrinsicRepr nm ctx++    -- these shouldn't appear in override signaures, so don't worry about them+    t@CT.FunctionHandleRepr {} -> t+    t@CT.RecursiveRepr {} -> t+    t@CT.MaybeRepr {} -> t+    t@CT.SequenceRepr {} -> t+    t@CT.ReferenceRepr {} -> t+    t@CT.VariantRepr {} -> t+    t@CT.WordMapRepr {} -> t+    t@CT.StringMapRepr {} -> t+    t@CT.SymbolicArrayRepr {} -> t+    t@CT.SymbolicStructRepr {} -> t++-- | 'regValueToLLVM' over an 'Ctx.Assignment'+regValuesToLLVM ::+  CB.IsSymInterface sym =>+  sym ->+  Ctx.Assignment CT.TypeRepr tys ->+  Ctx.Assignment (CRV.RegValue' sym) tys ->+  IO (Ctx.Assignment  (CRV.RegValue' sym) (CtxToLLVMType tys))+regValuesToLLVM sym tys vals =+  case (tys, vals) of+    (Ctx.Empty, Ctx.Empty) -> pure Ctx.empty+    (restTys Ctx.:> ty, restVals Ctx.:> CRV.RV val) -> do+      rest <- regValuesToLLVM sym restTys restVals+      val' <- regValueToLLVM sym ty val+      pure (rest Ctx.:> CRV.RV val')++-- | Convert a 'CRV.RegValue' to its corresponding LLVM type (replacing+-- bitvectors with LLVM pointers).+regValueToLLVM ::+  CB.IsSymInterface sym =>+  sym ->+  CT.TypeRepr ty ->+  CRV.RegValue sym ty ->+  IO (CRV.RegValue sym (ToLLVMType ty))+regValueToLLVM sym ty val =+  case ty of+    CT.BVRepr {} -> Ptr.llvmPointer_bv sym val++    -- recursive cases+    CT.VectorRepr elemTy -> traverse (regValueToLLVM sym elemTy) val+    CT.StructRepr fieldTys -> regValuesToLLVM sym fieldTys val++    -- no-ops+    CT.AnyRepr -> pure val+    CT.UnitRepr -> pure val+    CT.BoolRepr -> pure val+    CT.NatRepr -> pure val+    CT.IntegerRepr -> pure val+    CT.RealValRepr -> pure val+    CT.FloatRepr {} -> pure val+    CT.IEEEFloatRepr {} -> pure val+    CT.CharRepr -> pure val+    CT.StringRepr {} -> pure val+    CT.ComplexRealRepr -> pure val+    CT.IntrinsicRepr {} -> pure val++    -- these shouldn't appear in override signaures, so don't worry about them+    CT.FunctionHandleRepr {} -> pure val+    CT.MaybeRepr {} -> pure val+    CT.SequenceRepr {} -> pure val+    CT.RecursiveRepr {} -> pure val+    CT.ReferenceRepr {} -> pure val+    CT.VariantRepr {} -> pure val+    CT.WordMapRepr {} -> pure val+    CT.StringMapRepr {} -> pure val+    CT.SymbolicArrayRepr {} -> pure val+    CT.SymbolicStructRepr {} -> pure val++---------------------------------------------------------------------+-- * Back again++-- | Map 'regValueFromLLVM' over an 'Ctx.Assignment'.+regValuesFromLLVM ::+  CB.IsSymBackend sym bak =>+  bak ->   -- | Only used in error messages-  FunctionName ->+  WFN.FunctionName ->+  Ctx.Assignment CT.TypeRepr tys ->+  Ctx.Assignment CT.TypeRepr (CtxToLLVMType tys) ->+  Ctx.Assignment (CRV.RegValue' sym) (CtxToLLVMType tys) ->+  IO (Ctx.Assignment (CRV.RegValue' sym) tys)+regValuesFromLLVM bak fNm wanteds tys vals =+  case (wanteds, tys) of+    (Ctx.Empty, Ctx.Empty) -> pure vals+    (restWanted Ctx.:> w, restTys Ctx.:> t) -> do+      case vals of+        rest Ctx.:> CRV.RV val -> do+          rest' <- regValuesFromLLVM bak fNm restWanted restTys rest+          val' <- regValueFromLLVM bak fNm w t val+          pure (rest' Ctx.:> CRV.RV val')++-- | Convert a 'CRV.RegValue' from its corresponding LLVM type (replacing LLVM+-- pointers with bitvectors where needed).+regValueFromLLVM ::+  forall sym bak ty.+  CB.IsSymBackend sym bak =>   bak ->-  CtxRepr args' ->-  CtxRepr args ->-  Either ValCastError (ArgCast p sym ext args args')-castLLVMArgs _fnm _ Ctx.Empty Ctx.Empty =-  Right (ArgCast (\_ -> return Ctx.Empty))-castLLVMArgs fnm bak (rest' Ctx.:> tp') (rest Ctx.:> tp) =-  do ValCast f  <- castLLVMRet fnm bak tp tp'-     ArgCast fs <- castLLVMArgs fnm bak rest' rest-     Right (ArgCast-              (\(xs Ctx.:> x) -> do-                    xs' <- fs xs-                    x'  <- f (regValue x)-                    pure (xs' Ctx.:> RegEntry tp' x')))-castLLVMArgs _ _ _ _ = Left MismatchedShape+  -- | Only used in error messages+  WFN.FunctionName ->+  CT.TypeRepr ty ->+  CT.TypeRepr (ToLLVMType ty) ->+  CRV.RegValue sym (ToLLVMType ty) ->+  IO (CRV.RegValue sym ty)+regValueFromLLVM bak fNm wanted ty val = do+  case (wanted, ty) of+    (CT.BVRepr w, Ptr.LLVMPointerRepr w')+      | Just Refl <- testEquality w w' -> do+        let err = +              CSE.AssertFailureSimError+               "Found a pointer where a bitvector was expected"+               ("In the arguments of "+                ++ Text.unpack (WFN.functionName fNm))+        ptrToBv bak err val+    (CT.BVRepr {}, _) ->+      panic+        "regValueFromLLVM"+        [ "Pointer and bitvector of different sizes related by ToLLVMType!"+        , "This is impossible by the definition of ToLLVMType."+        ] --- | Attempt to construct a function to cast values of type @ret@ to type--- @ret'@.-castLLVMRet ::-  IsSymBackend sym bak =>+    -- recursive cases++    (CT.VectorRepr wantedElemTy, CT.VectorRepr elemTy) ->+      traverse (regValueFromLLVM bak fNm wantedElemTy elemTy) val++    (CT.StructRepr wantedFieldTys, CT.StructRepr fieldTys) ->+      regValuesFromLLVM bak fNm wantedFieldTys fieldTys val++    -- no-ops++    (CT.AnyRepr, _) -> pure val+    (CT.UnitRepr, _) ->  pure val+    (CT.BoolRepr, _) ->  pure val+    (CT.NatRepr, _) -> pure val+    (CT.IntegerRepr, _) -> pure val+    (CT.RealValRepr, _) -> pure val+    (CT.CharRepr, _) -> pure val+    (CT.ComplexRealRepr, _) -> pure val+    (CT.FloatRepr {}, _) -> pure val+    (CT.IEEEFloatRepr {}, _) -> pure val+    (CT.StringRepr {}, _) -> pure val+    (CT.IntrinsicRepr {}, _) -> pure val++    -- these shouldn't appear in override signaures, so don't worry about them++    (CT.FunctionHandleRepr {}, _) -> pure val+    (CT.MaybeRepr {}, _) -> pure val+    (CT.SequenceRepr {}, _) -> pure val+    (CT.RecursiveRepr {}, _) -> pure val+    (CT.ReferenceRepr {}, _) -> pure val+    (CT.VariantRepr {}, _) -> pure val+    (CT.WordMapRepr {}, _) -> pure val+    (CT.StringMapRepr {}, _) -> pure val+    (CT.SymbolicArrayRepr {}, _) -> pure val+    (CT.SymbolicStructRepr {}, _) -> pure val++-- | Map 'regValueFromLLVM' over an 'Ctx.Assignment' of 'CRM.RegEntry's.+regEntriesFromLLVM ::+  CB.IsSymBackend sym bak =>+  bak ->   -- | Only used in error messages-  FunctionName ->+  WFN.FunctionName ->+  Ctx.Assignment CT.TypeRepr tys ->+  Ctx.Assignment CT.TypeRepr (CtxToLLVMType tys) ->+  Ctx.Assignment (CRM.RegEntry sym) (CtxToLLVMType tys) ->+  IO (Ctx.Assignment (CRM.RegEntry sym) tys)+regEntriesFromLLVM bak fNm wanteds tys vals = do+  let cast = regValuesFromLLVM bak fNm wanteds tys+  Ctx.zipWith (\ty (CRV.RV v) -> CRM.RegEntry ty v) wanteds+    <$> cast (TFC.fmapFC (\(CRM.RegEntry _ty v) -> CRM.RV v) vals)++-- | Map 'regValueFromLLVM' over a 'CRM.RegMap'.+regMapFromLLVM ::+  forall sym bak tys.+  CB.IsSymBackend sym bak =>   bak ->-  TypeRepr ret  ->-  TypeRepr ret' ->-  Either ValCastError (ValCast p sym ext ret ret')-castLLVMRet _fnm bak (BVRepr w) (LLVMPointerRepr w')-  | Just Refl <- testEquality w w'-  = Right (ValCast (liftIO . llvmPointer_bv (backendGetSym bak)))-castLLVMRet fnm bak (LLVMPointerRepr w) (BVRepr w')-  | Just Refl <- testEquality w w'-  = let err = -          AssertFailureSimError-           "Found a pointer where a bitvector was expected"-           ("In the arguments or return value of " ++ Text.unpack (functionName fnm)) in-    Right (ValCast (liftIO . ptrToBv bak err))-castLLVMRet fnm bak (VectorRepr tp) (VectorRepr tp')-  = do ValCast f <- castLLVMRet fnm bak tp tp'-       Right (ValCast (traverse f))-castLLVMRet fnm bak (StructRepr ctx) (StructRepr ctx')-  = do ArgCast tf <- castLLVMArgs fnm bak ctx' ctx-       Right (ValCast (\vals ->-          let vals' = Ctx.zipWith (\tp (RV v) -> RegEntry tp v) ctx vals in-          fmapFC (\x -> RV (regValue x)) <$> tf vals'))+  -- | Only used in error messages+  WFN.FunctionName ->+  Ctx.Assignment CT.TypeRepr tys ->+  Ctx.Assignment CT.TypeRepr (CtxToLLVMType tys) ->+  CRM.RegMap sym (CtxToLLVMType tys) ->+  IO (CRM.RegMap sym tys)+regMapFromLLVM bak fNm wanteds tys =+  coerce (regEntriesFromLLVM bak fNm wanteds tys) -castLLVMRet _fnm _bak ret ret'-  | Just Refl <- testEquality ret ret'-  = Right (ValCast return)-castLLVMRet _fnm _bak ret ret' = Left (ValCastError (Some ret) (Some ret'))+---------------------------------------------------------------------+-- * Lowering overrides++-- | Lower an override to use the Crucible-LLVM ABI.+lowerLLVMOverride ::+  forall p sym ext args ret.+  HasLLVMAnn sym =>+  IC.LLVMOverride p sym ext args ret ->+  IC.LLVMOverride p sym ext (CtxToLLVMType args) (ToLLVMType ret)+lowerLLVMOverride ov =+  IC.LLVMOverride+  { IC.llvmOvDecl =+      Decl.Declare+      { Decl.decName = IC.llvmOvSymbol ov +      , Decl.decArgs = argTys'+      , Decl.decRet = retTy'+      }+  , IC.llvmOvDefn =+    \mvar args ->+      CSO.ovrWithBackend $ \bak -> do+        let fNm = IC.llvmOvName ov+        args' <- liftIO (regEntriesFromLLVM bak fNm argTys argTys' args)+        ret <- IC.llvmOvDefn ov mvar args'+        liftIO (regValueToLLVM (CB.backendGetSym bak) retTy ret)+  }+  where+    argTys = IC.llvmOvArgs ov+    argTys' = ctxToLLVMType argTys+    retTy = IC.llvmOvRet ov+    retTy' = toLLVMType retTy++-- | Postcompose 'lowerLLVMOverride' with a 'IC.MakeOverride'+lowerMakeOverride ::+  HasLLVMAnn sym =>+  IC.MakeOverride p sym ext arch ->+  IC.MakeOverride p sym ext arch+lowerMakeOverride (IC.MakeOverride f) =+  IC.MakeOverride $ \decl nm ctx -> do+    IC.SomeLLVMOverride ov <- f decl nm ctx+    Just (IC.SomeLLVMOverride (lowerLLVMOverride ov))++-- | Call 'lowerLLVMOverride' on the override in a 'OverrideTemplate'+lowerOverrideTemplate ::+  HasLLVMAnn sym =>+  IC.OverrideTemplate p sym ext arch ->+  IC.OverrideTemplate p sym ext arch+lowerOverrideTemplate t =+  IC.OverrideTemplate+  { IC.overrideTemplateMatcher = IC.overrideTemplateMatcher t+  , IC.overrideTemplateAction = lowerMakeOverride (IC.overrideTemplateAction t)+  }

@@ -1,7 +1,7 @@ -- | -- Module           : Lang.Crucible.LLVM.Intrinsics.Common -- Description      : Types used in override definitions--- Copyright        : (c) Galois, Inc 2015-2019+-- Copyright        : (c) Galois, Inc 2015-2026 -- License          : BSD3 -- Maintainer       : Rob Dockins <rdockins@galois.com> -- Stability        : provisional@@ -19,7 +19,12 @@  module Lang.Crucible.LLVM.Intrinsics.Common   ( LLVMOverride(..)+  , llvmOvSymbol+  , llvmOvName+  , llvmOvArgs+  , llvmOvRet   , SomeLLVMOverride(..)+  , someLlvmOverrideDeclare   , MakeOverride(..)   , llvmSizeT   , llvmSSizeT@@ -29,8 +34,9 @@   , basic_llvm_override   , polymorphic1_llvm_override   , polymorphic1_vec_llvm_override+  , polymorphic_cmp_llvm_override -  , build_llvm_override+  , llvmOverrideToTypedOverride   , register_llvm_override   , register_1arg_polymorphic_override   , register_1arg_vec_polymorphic_override@@ -42,9 +48,11 @@  import           Control.Monad (when) import           Control.Monad.IO.Class (liftIO)-import           Control.Lens import qualified Data.List as List+import qualified Data.Maybe as Maybe import qualified Data.Text as Text+import           Lens.Micro ((^.), to)+import           Lens.Micro.Mtl (use) import           Numeric (readDec) import qualified System.Info as Info @@ -55,7 +63,6 @@ import           Lang.Crucible.Backend import           Lang.Crucible.CFG.Common (GlobalVar) import           Lang.Crucible.Simulator.ExecutionTree (FnState(UseOverride))-import           Lang.Crucible.Panic (panic) import           Lang.Crucible.Simulator.OverrideSim import           Lang.Crucible.Utils.MonadVerbosity (getLogFunction) import           Lang.Crucible.Simulator.RegMap@@ -68,10 +75,9 @@ import           Lang.Crucible.LLVM.Functions (registerFunPtr, bindLLVMFunc) import           Lang.Crucible.LLVM.MemModel import           Lang.Crucible.LLVM.MemModel.CallStack (CallStack)-import qualified Lang.Crucible.LLVM.Intrinsics.Cast as Cast+import qualified Lang.Crucible.LLVM.Intrinsics.Declare as Decl import qualified Lang.Crucible.LLVM.Intrinsics.Match as Match import           Lang.Crucible.LLVM.Translation.Monad-import           Lang.Crucible.LLVM.Translation.Types  -- | This type represents an implementation of an LLVM intrinsic function in -- Crucible.@@ -81,10 +87,8 @@ -- LLVM memory model, such as Macaw. data LLVMOverride p sym ext args ret =   LLVMOverride-  { llvmOverride_declare :: L.Declare    -- ^ An LLVM name and signature for this intrinsic-  , llvmOverride_args    :: CtxRepr args -- ^ A representation of the argument types-  , llvmOverride_ret     :: TypeRepr ret -- ^ A representation of the return type-  , llvmOverride_def ::+  { llvmOvDecl :: Decl.Declare args ret+  , llvmOvDefn ::       IsSymInterface sym =>       GlobalVar Mem ->       Ctx.Assignment (RegEntry sym) args ->@@ -94,9 +98,28 @@     -- (@OverrideSim@).   } +llvmOvSymbol :: LLVMOverride p sym ext args ret -> L.Symbol+llvmOvSymbol = Decl.decName . llvmOvDecl++llvmOvName :: LLVMOverride p sym ext args ret -> FunctionName+llvmOvName ov =+  let L.Symbol nm = llvmOvSymbol ov in+  functionNameFromText (Text.pack nm)++llvmOvArgs :: LLVMOverride p sym ext args ret -> CtxRepr args+llvmOvArgs = Decl.decArgs . llvmOvDecl++llvmOvRet :: LLVMOverride p sym ext args ret -> TypeRepr ret+llvmOvRet = Decl.decRet . llvmOvDecl+ data SomeLLVMOverride p sym ext =   forall args ret. SomeLLVMOverride (LLVMOverride p sym ext args ret) +-- | Map 'llvmOverride_decl' inside a 'SomeLLVMOverride'.+someLlvmOverrideDeclare :: SomeLLVMOverride p sym ext -> Decl.SomeDeclare+someLlvmOverrideDeclare (SomeLLVMOverride ov) =+  Decl.SomeDeclare (llvmOvDecl ov)+ -- | Convenient LLVM representation of the @size_t@ type. llvmSizeT :: HasPtrWidth wptr => L.Type llvmSizeT = L.PrimType $ L.Integer $ fromIntegral $ natValue $ PtrWidth@@ -110,7 +133,7 @@ newtype MakeOverride p sym ext arch =   MakeOverride     { runMakeOverride ::-        L.Declare ->+        Decl.SomeDeclare ->         -- Decoded version of the name in the declaration         Maybe ABI.DecodedName ->         LLVMContext arch ->@@ -138,39 +161,23 @@ ------------------------------------------------------------------------ -- ** register_llvm_override --- | Do some pipe-fitting to match a Crucible override function into the shape---   expected by the LLVM calling convention.  This basically just coerces---   between values of @BVType w@ and values of @LLVMPointerType w@.-build_llvm_override ::++llvmOverrideToTypedOverride ::+  IsSymInterface sym =>   HasLLVMAnn sym =>-  FunctionName ->-  CtxRepr args ->-  TypeRepr ret ->-  CtxRepr args' ->-  TypeRepr ret' ->-  (forall rtp' l' a'. IsSymInterface sym =>-   Ctx.Assignment (RegEntry sym) args ->-   OverrideSim p sym ext rtp' l' a' (RegValue sym ret)) ->-  OverrideSim p sym ext rtp l a (Override p sym ext args' ret')-build_llvm_override fnm args ret args' ret' llvmOverride =-  ovrWithBackend $ \bak ->-  do fargs <--       case Cast.castLLVMArgs fnm bak args args' of-         Left err ->-           panic "Intrinsics.build_llvm_override"-             (Cast.printValCastError err ++-               [ "in function: " ++ Text.unpack (functionName fnm) ])-         Right f -> pure f-     fret <--       case Cast.castLLVMRet fnm bak ret ret' of-         Left err ->-           panic "Intrinsics.build_llvm_override"-             (Cast.printValCastError err ++-               [ "in function: " ++ Text.unpack (functionName fnm) ])-         Right f -> pure f-     return $ mkOverride' fnm ret' $-            do RegMap xs <- getOverrideArgs-               Cast.applyValCast fret =<< llvmOverride =<< Cast.applyArgCast fargs xs+  GlobalVar Mem ->+  LLVMOverride p sym ext args ret ->+  TypedOverride p sym ext args ret+llvmOverrideToTypedOverride mvar ov =+  TypedOverride+  { typedOverrideArgs = llvmOvArgs ov+  , typedOverrideRet = llvmOvRet ov+  , typedOverrideHandler =+      \args -> do+        let argEntries =+              Ctx.zipWith (\t (RV v) -> RegEntry t v) (llvmOvArgs ov) args+        llvmOvDefn ov mvar argEntries+  }  polymorphic1_llvm_override :: forall p sym ext arch wptr.   (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>@@ -207,13 +214,36 @@ polymorphic1_vec_llvm_override prefix fn =   OverrideTemplate (Match.PrefixMatch prefix) (register_1arg_vec_polymorphic_override prefix fn) +-- | Create an 'OverrideTemplate' for an intrinsic in the @llvm.{s,u}cmp.*@+-- family. These can be instantiated at multiple types, including:+--+-- * @i2 \@llvm.scmp.i2.i32(i32, i32)@++-- * @i8 \@llvm.scmp.i8.i8(i8, i8)@+--+-- * etc.+--+-- Note that the argument and result types are allowed to be different, so the+-- @fn@ argument is parameterized by two separate 'NatRepr's.+polymorphic_cmp_llvm_override :: forall p sym ext arch wptr.+  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>+  String ->+  (forall argSz resSz.+    (1 <= argSz, 2 <= resSz) =>+    NatRepr argSz ->+    NatRepr resSz ->+    SomeLLVMOverride p sym ext) ->+  OverrideTemplate p sym ext arch+polymorphic_cmp_llvm_override prefix fn =+  OverrideTemplate (Match.PrefixMatch prefix) (register_cmp_polymorphic_override prefix fn)+ register_1arg_polymorphic_override :: forall p sym ext arch wptr.   (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>   String ->   (forall w. (1 <= w) => NatRepr w -> SomeLLVMOverride p sym ext) ->   MakeOverride p sym ext arch register_1arg_polymorphic_override prefix overrideFn =-  MakeOverride $ \(L.Declare{ L.decName = L.Symbol nm }) _ _ ->+  MakeOverride $ \(Decl.SomeDeclare (Decl.Declare{ Decl.decName = L.Symbol nm })) _ _ ->     case List.stripPrefix prefix nm of       Just ('.':'i': (readDec -> (sz,[]):_))         | Some w <- mkNatRepr sz@@ -240,7 +270,7 @@     SomeLLVMOverride p sym ext) ->   MakeOverride p sym ext arch register_1arg_vec_polymorphic_override prefix overrideFn =-  MakeOverride $ \(L.Declare{ L.decName = L.Symbol nm }) _ _ ->+  MakeOverride $ \(Decl.SomeDeclare (Decl.Declare{ Decl.decName = L.Symbol nm })) _ _ ->     case List.stripPrefix prefix nm of       Just ('.':'v':suffix1)         | (vecSzStr, 'i':intSzStr) <- break (== 'i') suffix1@@ -252,14 +282,43 @@         -> Just (overrideFn vecSzRepr intSzRepr)       _ -> Nothing +-- | Register an override for an intrinsic in the @llvm.{s,u}cmp.*@ family.+-- (See the Haddocks for 'polymorphic_cmp_llvm_override' for details on what+-- this means.) This function is responsible for parsing the suffixes in the+-- intrinsic's name, which encodes the sizes of the argument and result types.+-- As some examples:+--+-- * @.i2.i32@ (argument size @32@, result size @2@)+--+-- * @.i8.i64@ (argument size @64@, result size @8@)+register_cmp_polymorphic_override :: forall p sym ext arch wptr.+  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>+  String ->+  (forall argSz resSz.+    (1 <= argSz, 2 <= resSz) =>+    NatRepr argSz ->+    NatRepr resSz ->+    SomeLLVMOverride p sym ext) ->+  MakeOverride p sym ext arch+register_cmp_polymorphic_override prefix overrideFn =+  MakeOverride $ \(Decl.SomeDeclare (Decl.Declare{ Decl.decName = L.Symbol nm })) _ _ ->+    case List.stripPrefix prefix nm of+      Just ('.':'i': (readDec -> (resSz,rest):_))+        | '.':'i': (readDec -> (argSz,[]):_) <- rest+        , Some argW <- mkNatRepr argSz+        , Some resW <- mkNatRepr resSz+        , Just LeqProof <- testLeq (knownNat @1) argW+        , Just LeqProof <- testLeq (knownNat @2) resW+        -> Just (overrideFn argW resW)+      _ -> Nothing+ basic_llvm_override :: forall p args ret sym ext arch wptr.   (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>   LLVMOverride p sym ext args ret ->   OverrideTemplate p sym ext arch basic_llvm_override ovr = OverrideTemplate matcher regOvr   where-    ovrDecl = llvmOverride_declare ovr-    L.Symbol ovrNm = L.decName ovrDecl+    L.Symbol ovrNm = llvmOvSymbol ovr     isDarwin = Info.os == "darwin"      matcher :: Match.TemplateMatcher@@ -268,8 +327,8 @@      regOvr :: MakeOverride p sym ext arch     regOvr = do-      MakeOverride $ \requestedDecl _ _ -> do-        let L.Symbol requestedNm = L.decName requestedDecl+      MakeOverride $ \(Decl.SomeDeclare requestedDecl) _ _ -> do+        let L.Symbol requestedNm = Decl.decName requestedDecl         -- If we are on Darwin and the function name contains Darwin-specific         -- prefixes or suffixes, change the name of the override to the         -- name containing prefixes/suffixes. See Note [Darwin aliases] in@@ -277,8 +336,8 @@         -- do this.         let ovr' | isDarwin                  , ovrNm == Match.stripDarwinAliases requestedNm-                 = ovr { llvmOverride_declare =-                           ovrDecl { L.decName = L.Symbol requestedNm }}+                 = let decl = (llvmOvDecl ovr) { Decl.decName = L.Symbol requestedNm } in+                   ovr { llvmOvDecl = decl }                   | otherwise                  = ovr@@ -291,47 +350,53 @@ -- that we do not have to define quite so many overrides with different -- combinations of pointer types. isMatchingDeclaration ::-  L.Declare {- ^ Requested declaration -} ->-  L.Declare {- ^ Provided declaration for intrinsic -} ->+  Decl.Declare args' ret' {- ^ Requested declaration -} ->+  LLVMOverride p sym ext args ret ->   Bool-isMatchingDeclaration requested provided = and-  [ L.decName requested == L.decName provided-  , matchingArgList (L.decArgs requested) (L.decArgs provided)-  , L.decRetType requested `L.eqTypeModuloOpaquePtrs` L.decRetType provided-  -- TODO? do we need to pay attention to various attributes?+isMatchingDeclaration requested provided =+  let args = Decl.decArgs requested in+  let ret = Decl.decRet requested in+  and+  [ Decl.decName requested == llvmOvSymbol provided+  , matchingArgList args (llvmOvArgs provided)+  , Maybe.isJust (testEquality ret (llvmOvRet provided))   ] - where- matchingArgList [] [] = True- matchingArgList [] _  = L.decVarArgs requested- matchingArgList _  [] = L.decVarArgs provided- matchingArgList (x:xs) (y:ys) = x `L.eqTypeModuloOpaquePtrs` y && matchingArgList xs ys+  where+  matchingArgList ::+    Ctx.Assignment TypeRepr ctx1 ->+    Ctx.Assignment TypeRepr ctx2 ->+    Bool+  -- Ignore varargs as long as the rest of the arguments match (VectorRepr+  -- AnyRepr is how Crucible-LLVM represents varargs).+  matchingArgList (rest Ctx.:> VectorRepr AnyRepr) ys = matchingArgList rest ys+  matchingArgList xs (rest Ctx.:> VectorRepr AnyRepr) = matchingArgList xs rest+  matchingArgList xs ys = Maybe.isJust (testEquality xs ys) -register_llvm_override :: forall p args ret sym ext arch wptr rtp l a.+register_llvm_override ::+  forall p args ret args' ret' sym ext arch wptr rtp l a.   (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) =>   LLVMOverride p sym ext args ret ->-  L.Declare ->+  Decl.Declare args' ret' ->   LLVMContext arch ->   OverrideSim p sym ext rtp l a () register_llvm_override llvmOverride requestedDecl llvmctx = do-  let decl = llvmOverride_declare llvmOverride-  if not (isMatchingDeclaration requestedDecl decl) then-    do when (L.decName requestedDecl == L.decName decl) $+  let ?lc = llvmctx^.llvmTypeCtx+  if not (isMatchingDeclaration requestedDecl llvmOverride) then+    do when (Decl.decName requestedDecl == llvmOvSymbol llvmOverride) $          do logFn <- getLogFunction             liftIO $ logFn 3 $ unlines               [ "Mismatched declaration signatures"               , " *** requested: " ++ show requestedDecl-              , " *** found: "     ++ show decl-              , ""+              , " *** found args: " ++ show (llvmOvArgs llvmOverride)+              , " *** found ret: " ++ show (llvmOvRet llvmOverride)               ]   else do_register_llvm_override llvmctx llvmOverride  -- | Low-level function to register LLVM overrides. ----- Type-checks the LLVM override against the 'L.Declare' it contains, adapting--- its arguments and return values as necessary. Then creates and binds--- a function handle, and also binds the function to the global function--- allocation in the LLVM memory.+-- Creates and binds a function handle, and also binds the function to the+-- global function allocation in the LLVM memory. -- -- Useful when you don\'t have access to a full LLVM AST, e.g., when parsing -- Crucible CFGs written in crucible-syntax. For more usual cases, use@@ -342,20 +407,17 @@   LLVMOverride p sym ext args ret ->   OverrideSim p sym ext rtp l a () do_register_llvm_override llvmctx llvmOverride = do-  let decl = llvmOverride_declare llvmOverride-  let (L.Symbol str_nm) = L.decName decl+  let nm@(L.Symbol str_nm) = llvmOvSymbol llvmOverride   let fnm  = functionNameFromText (Text.pack str_nm)    let mvar = llvmMemVar llvmctx-  let overrideArgs = llvmOverride_args llvmOverride-  let overrideRet  = llvmOverride_ret llvmOverride-   let ?lc = llvmctx^.llvmTypeCtx -  llvmDeclToFunHandleRepr' decl $ \args ret -> do-    o <- build_llvm_override fnm overrideArgs overrideRet args ret-           (\asgn -> llvmOverride_def llvmOverride mvar asgn)-    bindLLVMFunc mvar (L.decName decl) args ret (UseOverride o)+  let typedOv = llvmOverrideToTypedOverride mvar llvmOverride+  let o = runTypedOverride fnm typedOv+  let args = typedOverrideArgs typedOv+  let ret = typedOverrideRet typedOv+  bindLLVMFunc mvar nm args ret (UseOverride o)  -- | Create an allocation for an override and register it. --@@ -374,7 +436,7 @@   [L.Symbol] ->   OverrideSim p sym LLVM rtp l a () alloc_and_register_override bak llvmctx llvmOverride aliases = do-  let L.Declare { L.decName = symb@(L.Symbol nm) } = llvmOverride_declare llvmOverride+  let symb@(L.Symbol nm) = llvmOvSymbol llvmOverride   let mvar = llvmMemVar llvmctx   mem <- readGlobal mvar   (_ptr, mem') <- liftIO (registerFunPtr bak mem nm symb aliases)

@@ -0,0 +1,110 @@+-- |+-- Module           : Lang.Crucible.LLVM.Intrinsics.Declare+-- Description      : Function declarations+-- Copyright        : (c) Galois, Inc 2026+-- License          : BSD3+-- Maintainer       : Langston Barrett <langston@galois.com>+-- Stability        : provisional+------------------------------------------------------------------------++{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE ImplicitParams #-}++module Lang.Crucible.LLVM.Intrinsics.Declare+  ( Declare(..)+  , SomeDeclare(SomeDeclare)+  , fromHandle+  , fromSomeHandle+  , fromLLVM+  , fromLLVMWithWarnings+  ) where++import qualified Control.Monad.Fail as Fail+import           Control.Monad.IO.Class (liftIO)+import qualified Data.Maybe as Maybe+import qualified Data.Text as Text+import           Data.Traversable (for)++import qualified Text.LLVM.AST as L++import qualified Data.Parameterized.Context as Ctx++import qualified What4.FunctionName as WFN++import qualified Lang.Crucible.FunctionHandle as CFH+import           Lang.Crucible.Simulator.OverrideSim (OverrideSim)+import qualified Lang.Crucible.Types as CT+import           Lang.Crucible.Utils.MonadVerbosity (getLogFunction)++import           Lang.Crucible.LLVM.MemModel.Pointer (HasPtrWidth)+import           Lang.Crucible.LLVM.Translation.Types (llvmDeclToFunHandleRepr')+import           Lang.Crucible.LLVM.TypeContext (TypeContext)++-- | The declaration of a function.+--+-- Used primarily for matching LLVM overrides to the declarations in LLVM+-- modules or S-expression programs.+data Declare args ret+  = Declare+    { decName :: L.Symbol+    , decArgs :: Ctx.Assignment CT.TypeRepr args+    , decRet :: CT.TypeRepr ret+    }+  deriving Show++data SomeDeclare = forall args ret. SomeDeclare (Declare args ret)++fromHandle :: CFH.FnHandle args ret -> Declare args ret+fromHandle hdl =+  Declare+  { decName = L.Symbol (Text.unpack (WFN.functionName (CFH.handleName hdl)))+  , decArgs = CFH.handleArgTypes hdl+  , decRet = CFH.handleReturnType hdl+  }++fromSomeHandle :: CFH.SomeHandle -> SomeDeclare+fromSomeHandle (CFH.SomeHandle hdl) = SomeDeclare (fromHandle hdl)++fromLLVM ::+  ( ?lc :: TypeContext+  , HasPtrWidth wptr+  , Fail.MonadFail m+  ) =>+  L.Declare ->+  m SomeDeclare+fromLLVM decl =+  llvmDeclToFunHandleRepr' decl $ \args ret ->+    pure $+      SomeDeclare $+        Declare+        { decName = L.decName decl+        , decArgs = args+        , decRet = ret+        }++-- | Internal, for 'Fail.MonadFail' instance+newtype EitherString a = EitherString (Either String a)+  deriving (Applicative, Functor, Monad)++instance Fail.MonadFail EitherString where+  fail = EitherString . Left++-- | Apply 'fromLLVM' in a loop, warning on failures+fromLLVMWithWarnings ::+  ( ?lc :: TypeContext+  , HasPtrWidth wptr+  ) =>+  [L.Declare] ->+  OverrideSim p sym ext rtp l a [SomeDeclare]+fromLLVMWithWarnings decls =+  fmap Maybe.catMaybes $+    for decls $ \decl -> do+      case fromLLVM decl of+        EitherString (Left err) -> do+          logFn <- getLogFunction+          let msg = unlines ["Unliftable LLVM declaration", show decl, show err]+          liftIO $ logFn 3 msg+          pure Nothing+        EitherString (Right d) ->+          pure (Just d)

@@ -29,7 +29,6 @@ module Lang.Crucible.LLVM.Intrinsics.LLVM where  import           GHC.TypeNats (KnownNat)-import           Control.Lens hiding (op, (:>), Empty) import           Control.Monad (foldM, unless) import           Control.Monad.IO.Class (MonadIO(..)) import           Data.Bits ((.&.))@@ -344,6 +343,35 @@     )   ] +-- | An LLVM override for the @llvm.{s,u}cmp.*@ family of intrinsics. These+-- overrides have a unique shape in that:+--+-- 1. Both their argument and result types are polymorphic integer types (which+--    are allowed to be different), and+--+-- 2. The result integer type must have a size of at least 2 bits.+newtype PolyCmpLLVMOverride p sym ext+  = PolyCmpLLVMOverride+      (forall argSz resSz+         . (1 <= argSz, 2 <= resSz)+        => NatRepr argSz+        -> NatRepr resSz+        -> SomeLLVMOverride p sym ext)++poly_cmp_llvm_overrides ::+  IsSymInterface sym =>+  [(String, PolyCmpLLVMOverride p sym ext)]+poly_cmp_llvm_overrides =+  [ ("llvm.scmp"+    , PolyCmpLLVMOverride $ \argSz resSz ->+        SomeLLVMOverride (llvmScmp argSz resSz)+    )+  , ("llvm.ucmp"+    , PolyCmpLLVMOverride $ \argSz resSz ->+        SomeLLVMOverride (llvmUcmp argSz resSz)+    )+  ]+ ------------------------------------------------------------------------ -- ** Declarations @@ -1739,6 +1767,54 @@      (VectorType (BVType intSz)) llvmUminVector = llvmVectorMap "umin" callVectorMapUmin +-- | Build an 'LLVMOverride' for an @llvm.{s,u}cmp.*@ intrinsic.+llvmCmp ::+  forall argSz resSz p sym ext.+  (1 <= argSz, 2 <= resSz) =>+  -- | The name of the operation (@scmp@ or @ucmp@).+  String ->+  -- | The semantics of the override.+  (forall r args ret.+    IsSymInterface sym =>+    RegEntry sym (BVType argSz) ->+    RegEntry sym (BVType argSz) ->+    OverrideSim p sym ext r args ret (SymBV sym resSz)) ->+  -- | The size of the argument type.+  NatRepr argSz ->+  -- | The size of the result type.+  NatRepr resSz ->+  LLVMOverride p sym ext+     (EmptyCtx ::> BVType argSz ::> BVType argSz)+     (BVType resSz)+llvmCmp cmpOpName cmpOp argSz resSz+  | (LeqProof :: LeqProof 1 resSz) <-+      leqTrans (LeqProof @1 @2) (LeqProof @2 @resSz)+  = let nm = L.Symbol ("llvm." ++ cmpOpName +++                       ".i" ++ show (natValue resSz) +++                       ".i" ++ show (natValue argSz)) in+      [llvmOvr| #resSz $nm( #argSz, #argSz ) |]+      (\_memOps args -> Ctx.uncurryAssignment cmpOp args)++llvmScmp ::+  forall argSz resSz p sym ext.+  (1 <= argSz, 2 <= resSz) =>+  NatRepr argSz ->+  NatRepr resSz ->+  LLVMOverride p sym ext+     (EmptyCtx ::> BVType argSz ::> BVType argSz)+     (BVType resSz)+llvmScmp argSz resSz = llvmCmp "scmp" (callScmp resSz) argSz resSz++llvmUcmp ::+  forall argSz resSz p sym ext.+  (1 <= argSz, 2 <= resSz) =>+  NatRepr argSz ->+  NatRepr resSz ->+  LLVMOverride p sym ext+     (EmptyCtx ::> BVType argSz ::> BVType argSz)+     (BVType resSz)+llvmUcmp argSz resSz = llvmCmp "ucmp" (callUcmp resSz) argSz resSz+ ------------------------------------------------------------------------ -- ** Implementations @@ -2459,3 +2535,46 @@ callVectorMapUmin vec1 vec2 = do   sym <- getSymInterface   callVectorMap (bvUmin sym) vec1 vec2++-- | The semantics of an @llvm.{s,u}cmp.*@ intrinsic.+callCmp ::+  forall argSz resSz p sym ext r args ret.+  (IsSymInterface sym, 1 <= argSz, 2 <= resSz) =>+  -- | The semantics of a bitvector less-than operation (either signed or+  -- unsigned).+  (sym -> SymBV sym argSz -> SymBV sym argSz -> IO (Pred sym)) ->+  -- | The size of the result type.+  NatRepr resSz ->+  RegEntry sym (BVType argSz) ->+  RegEntry sym (BVType argSz) ->+  OverrideSim p sym ext r args ret (SymBV sym resSz)+callCmp bvLtOp resSz (regValue -> x) (regValue -> y)+  | (LeqProof :: LeqProof 1 resSz) <-+      leqTrans (LeqProof @1 @2) (LeqProof @2 @resSz)+  = do sym <- getSymInterface+       liftIO $+         do xLtY <- bvLtOp sym x y+            xEqY <- bvEq sym x y+            zero <- bvZero sym resSz+            one <- bvOne sym resSz+            negOne <- bvNeg sym one+            -- If x < y, return -1. If x == y, return 0. If x > y, return 1.+            bvIte sym xLtY negOne =<< bvIte sym xEqY zero one++callScmp ::+  forall argSz resSz p sym ext r args ret.+  (IsSymInterface sym, 1 <= argSz, 2 <= resSz) =>+  NatRepr resSz ->+  RegEntry sym (BVType argSz) ->+  RegEntry sym (BVType argSz) ->+  OverrideSim p sym ext r args ret (SymBV sym resSz)+callScmp = callCmp bvSlt++callUcmp ::+  forall argSz resSz p sym ext r args ret.+  (IsSymInterface sym, 1 <= argSz, 2 <= resSz) =>+  NatRepr resSz ->+  RegEntry sym (BVType argSz) ->+  RegEntry sym (BVType argSz) ->+  OverrideSim p sym ext r args ret (SymBV sym resSz)+callUcmp = callCmp bvUlt

@@ -8,1938 +8,201 @@ ------------------------------------------------------------------------  {-# LANGUAGE DataKinds #-}-{-# LANGUAGE DoAndIfThenElse #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE ImplicitParams #-}-{-# LANGUAGE ImpredicativeTypes #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE QuasiQuotes #-}-{-# LANGUAGE Rank2Types #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE ViewPatterns #-}--module Lang.Crucible.LLVM.Intrinsics.Libc where--import           Control.Lens ((^.), _1, _2, _3)-import qualified Codec.Binary.UTF8.Generic as UTF8-import           Control.Monad (when)-import           Control.Monad.IO.Class (MonadIO(..))-import           Control.Monad.State (MonadState(..), StateT(..))-import           Control.Monad.Trans.Class (MonadTrans(..))-import qualified Data.ByteString as BS-import qualified Data.Vector as V-import           System.IO-import qualified GHC.Stack as GHC--import qualified Data.BitVector.Sized as BV-import           Data.Parameterized.Context ( pattern (:>), pattern Empty )-import qualified Data.Parameterized.Context as Ctx--import           What4.Interface-import           What4.ProgramLoc (plSourceLoc)-import qualified What4.SpecialFunctions as W4--import           Lang.Crucible.Backend-import           Lang.Crucible.CFG.Common-import           Lang.Crucible.Types-import           Lang.Crucible.Simulator.ExecutionTree-import           Lang.Crucible.Simulator.OverrideSim-import           Lang.Crucible.Simulator.RegMap-import           Lang.Crucible.Simulator.SimError--import           Lang.Crucible.LLVM.Bytes-import           Lang.Crucible.LLVM.DataLayout-import qualified Lang.Crucible.LLVM.Errors.Poison as Poison-import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as UB-import           Lang.Crucible.LLVM.MalformedLLVMModule-import           Lang.Crucible.LLVM.MemModel-import           Lang.Crucible.LLVM.MemModel.CallStack (CallStack)-import qualified Lang.Crucible.LLVM.MemModel.Type as G-import qualified Lang.Crucible.LLVM.MemModel.Generic as G-import           Lang.Crucible.LLVM.MemModel.Partial-import qualified Lang.Crucible.LLVM.MemModel.Pointer as Ptr-import           Lang.Crucible.LLVM.MemModel.Strings as CStr-import           Lang.Crucible.LLVM.Printf-import           Lang.Crucible.LLVM.QQ( llvmOvr )-import           Lang.Crucible.LLVM.TypeContext--import           Lang.Crucible.LLVM.Intrinsics.Common-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 =-  [ SomeLLVMOverride llvmAbortOverride-  , SomeLLVMOverride llvmAssertRtnOverride-  , SomeLLVMOverride llvmAssertFailOverride-  , SomeLLVMOverride llvmMemcpyOverride-  , SomeLLVMOverride llvmMemcpyChkOverride-  , SomeLLVMOverride llvmMemmoveOverride-  , SomeLLVMOverride llvmMemsetOverride-  , SomeLLVMOverride llvmMemsetChkOverride-  , SomeLLVMOverride llvmMallocOverride-  , SomeLLVMOverride llvmCallocOverride-  , SomeLLVMOverride llvmFreeOverride-  , SomeLLVMOverride llvmReallocOverride-  , SomeLLVMOverride llvmStrlenOverride-  , SomeLLVMOverride llvmStrnlenOverride-  , SomeLLVMOverride llvmStrcpyOverride-  , SomeLLVMOverride llvmStrdupOverride-  , SomeLLVMOverride llvmStrndupOverride-  , SomeLLVMOverride llvmPrintfOverride-  , SomeLLVMOverride llvmPrintfChkOverride-  , SomeLLVMOverride llvmPutsOverride-  , SomeLLVMOverride llvmPutCharOverride-  , SomeLLVMOverride llvmExitOverride-  , SomeLLVMOverride llvmGetenvOverride-  , SomeLLVMOverride llvmHtonlOverride-  , SomeLLVMOverride llvmHtonsOverride-  , SomeLLVMOverride llvmNtohlOverride-  , SomeLLVMOverride llvmNtohsOverride-  , SomeLLVMOverride llvmAbsOverride-  , SomeLLVMOverride llvmLAbsOverride_32-  , SomeLLVMOverride llvmLAbsOverride_64-  , SomeLLVMOverride llvmLLAbsOverride--  , SomeLLVMOverride llvmCeilOverride-  , SomeLLVMOverride llvmCeilfOverride-  , SomeLLVMOverride llvmFloorOverride-  , SomeLLVMOverride llvmFloorfOverride-  , SomeLLVMOverride llvmFmaOverride-  , SomeLLVMOverride llvmFmafOverride-  , SomeLLVMOverride llvmIsinfOverride-  , SomeLLVMOverride llvm__isinfOverride-  , SomeLLVMOverride llvm__isinffOverride-  , SomeLLVMOverride llvmIsnanOverride-  , SomeLLVMOverride llvm__isnanOverride-  , SomeLLVMOverride llvm__isnanfOverride-  , SomeLLVMOverride llvm__isnandOverride-  , SomeLLVMOverride llvmSqrtOverride-  , SomeLLVMOverride llvmSqrtfOverride-  , SomeLLVMOverride llvmSinOverride-  , SomeLLVMOverride llvmSinfOverride-  , SomeLLVMOverride llvmCosOverride-  , SomeLLVMOverride llvmCosfOverride-  , SomeLLVMOverride llvmTanOverride-  , SomeLLVMOverride llvmTanfOverride-  , SomeLLVMOverride llvmAsinOverride-  , SomeLLVMOverride llvmAsinfOverride-  , SomeLLVMOverride llvmAcosOverride-  , SomeLLVMOverride llvmAcosfOverride-  , SomeLLVMOverride llvmAtanOverride-  , SomeLLVMOverride llvmAtanfOverride-  , SomeLLVMOverride llvmSinhOverride-  , SomeLLVMOverride llvmSinhfOverride-  , SomeLLVMOverride llvmCoshOverride-  , SomeLLVMOverride llvmCoshfOverride-  , SomeLLVMOverride llvmTanhOverride-  , SomeLLVMOverride llvmTanhfOverride-  , SomeLLVMOverride llvmAsinhOverride-  , SomeLLVMOverride llvmAsinhfOverride-  , SomeLLVMOverride llvmAcoshOverride-  , SomeLLVMOverride llvmAcoshfOverride-  , SomeLLVMOverride llvmAtanhOverride-  , SomeLLVMOverride llvmAtanhfOverride-  , SomeLLVMOverride llvmHypotOverride-  , SomeLLVMOverride llvmHypotfOverride-  , SomeLLVMOverride llvmAtan2Override-  , SomeLLVMOverride llvmAtan2fOverride-  , SomeLLVMOverride llvmPowfOverride-  , SomeLLVMOverride llvmPowOverride-  , SomeLLVMOverride llvmExpOverride-  , SomeLLVMOverride llvmExpfOverride-  , SomeLLVMOverride llvmLogOverride-  , SomeLLVMOverride llvmLogfOverride-  , SomeLLVMOverride llvmExpm1Override-  , SomeLLVMOverride llvmExpm1fOverride-  , SomeLLVMOverride llvmLog1pOverride-  , SomeLLVMOverride llvmLog1pfOverride-  , SomeLLVMOverride llvmExp2Override-  , SomeLLVMOverride llvmExp2fOverride-  , SomeLLVMOverride llvmLog2Override-  , SomeLLVMOverride llvmLog2fOverride-  , SomeLLVMOverride llvmExp10Override-  , SomeLLVMOverride llvmExp10fOverride-  , SomeLLVMOverride llvm__exp10Override-  , SomeLLVMOverride llvm__exp10fOverride-  , SomeLLVMOverride llvmLog10Override-  , SomeLLVMOverride llvmLog10fOverride--  , SomeLLVMOverride cxa_atexitOverride-  , SomeLLVMOverride posixMemalignOverride-  ]----------------------------------------------------------------------------- ** Declarations---llvmMemcpyOverride-  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr-     , ?memOpts :: MemOptions )-  => LLVMOverride p sym ext-           (EmptyCtx ::> LLVMPointerType wptr-                     ::> LLVMPointerType wptr-                     ::> BVType wptr)-           (LLVMPointerType wptr)-llvmMemcpyOverride =-  [llvmOvr| i8* @memcpy( i8*, i8*, size_t ) |]-  (\memOps args ->-       do sym <- getSymInterface-          volatile <- liftIO $ RegEntry knownRepr <$> bvZero sym knownNat-          Ctx.uncurryAssignment (callMemcpy memOps)-                                (args :> volatile)-          return $ regValue $ args^._1 -- return first argument-    )---llvmMemcpyChkOverride-  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr-     , ?memOpts :: MemOptions )-  => LLVMOverride p sym ext-         (EmptyCtx ::> LLVMPointerType wptr-                   ::> LLVMPointerType wptr-                   ::> BVType wptr-                   ::> BVType wptr)-         (LLVMPointerType wptr)-llvmMemcpyChkOverride =-  [llvmOvr| i8* @__memcpy_chk ( i8*, i8*, size_t, size_t ) |]-  (\memOps args ->-      do let args' = Empty :> (args^._1) :> (args^._2) :> (args^._3)-         sym <- getSymInterface-         volatile <- liftIO $ RegEntry knownRepr <$> bvZero sym knownNat-         Ctx.uncurryAssignment (callMemcpy memOps)-                               (args' :> volatile)-         return $ regValue $ args^._1 -- return first argument-    )--llvmMemmoveOverride-  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr-     , ?memOpts :: MemOptions )-  => LLVMOverride p sym ext-         (EmptyCtx ::> (LLVMPointerType wptr)-                   ::> (LLVMPointerType wptr)-                   ::> BVType wptr)-         (LLVMPointerType wptr)-llvmMemmoveOverride =-  [llvmOvr| i8* @memmove( i8*, i8*, size_t ) |]-  (\memOps args ->-      do sym <- getSymInterface-         volatile <- liftIO (RegEntry knownRepr <$> bvZero sym knownNat)-         Ctx.uncurryAssignment (callMemmove memOps)-                               (args :> volatile)-         return $ regValue $ args^._1 -- return first argument-    )--llvmMemsetOverride :: forall p sym ext wptr.-     (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)-  => LLVMOverride p sym ext-         (EmptyCtx ::> LLVMPointerType wptr-                   ::> BVType 32-                   ::> BVType wptr)-         (LLVMPointerType wptr)-llvmMemsetOverride =-  [llvmOvr| i8* @memset( i8*, i32, size_t ) |]-  (\memOps args ->-      do sym <- getSymInterface-         LeqProof <- return (leqTrans @9 @16 @wptr LeqProof LeqProof)-         let dest = args^._1-         val <- liftIO (RegEntry knownRepr <$> bvTrunc sym (knownNat @8) (regValue (args^._2)))-         let len = args^._3-         volatile <- liftIO-            (RegEntry knownRepr <$> bvZero sym knownNat)-         callMemset memOps dest val len volatile-         return (regValue dest)-    )--llvmMemsetChkOverride-  :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)-  => LLVMOverride p sym ext-         (EmptyCtx ::> LLVMPointerType wptr-                 ::> BVType 32-                 ::> BVType wptr-                 ::> BVType wptr)-         (LLVMPointerType wptr)-llvmMemsetChkOverride =-  [llvmOvr| i8* @__memset_chk( i8*, i32, size_t, size_t ) |]-  (\memOps args ->-      do sym <- getSymInterface-         let dest = args^._1-         val <- liftIO-              (RegEntry knownRepr <$> bvTrunc sym knownNat (regValue (args^._2)))-         let len = args^._3-         volatile <- liftIO-            (RegEntry knownRepr <$> bvZero sym knownNat)-         callMemset memOps dest val len volatile-         return (regValue dest)-    )----------------------------------------------------------------------------- *** Allocation--llvmCallocOverride-  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr-     , ?lc :: TypeContext, ?memOpts :: MemOptions )-  => LLVMOverride p sym ext-         (EmptyCtx ::> BVType wptr ::> BVType wptr)-         (LLVMPointerType wptr)-llvmCallocOverride =-  let alignment = maxAlignment (llvmDataLayout ?lc) in-  [llvmOvr| i8* @calloc( size_t, size_t ) |]-  (\memOps args -> Ctx.uncurryAssignment (callCalloc memOps alignment) args)---llvmReallocOverride-  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr-     , ?lc :: TypeContext, ?memOpts :: MemOptions )-  => LLVMOverride p sym ext-         (EmptyCtx ::> LLVMPointerType wptr ::> BVType wptr)-         (LLVMPointerType wptr)-llvmReallocOverride =-  let alignment = maxAlignment (llvmDataLayout ?lc) in-  [llvmOvr| i8* @realloc( i8*, size_t ) |]-  (\memOps args -> Ctx.uncurryAssignment (callRealloc memOps alignment) args)--llvmMallocOverride-  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr-     , ?lc :: TypeContext, ?memOpts :: MemOptions )-  => LLVMOverride p sym ext-         (EmptyCtx ::> BVType wptr)-         (LLVMPointerType wptr)-llvmMallocOverride =-  let alignment = maxAlignment (llvmDataLayout ?lc) in-  [llvmOvr| i8* @malloc( size_t ) |]-  (\memOps args -> Ctx.uncurryAssignment (callMalloc memOps alignment) args)--posixMemalignOverride ::-  ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr-  , ?lc :: TypeContext, ?memOpts :: MemOptions ) =>-  LLVMOverride p sym ext-      (EmptyCtx ::> LLVMPointerType wptr-                ::> BVType wptr-                ::> BVType wptr)-      (BVType 32)-posixMemalignOverride =-  [llvmOvr| i32 @posix_memalign( i8**, size_t, size_t ) |]-  (\memOps args -> Ctx.uncurryAssignment (callPosixMemalign memOps) args)---llvmFreeOverride-  :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)-  => LLVMOverride p sym ext-         (EmptyCtx ::> LLVMPointerType wptr)-         UnitType-llvmFreeOverride =-  [llvmOvr| void @free( i8* ) |]-  (\memOps args -> Ctx.uncurryAssignment (callFree memOps) args)----------------------------------------------------------------------------- *** Strings and I/O--llvmPrintfOverride-  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym-     , ?memOpts :: MemOptions )-  => LLVMOverride p sym ext-         (EmptyCtx ::> LLVMPointerType wptr-                   ::> VectorType AnyType)-         (BVType 32)-llvmPrintfOverride =-  [llvmOvr| i32 @printf( i8*, ... ) |]-  (\memOps args -> Ctx.uncurryAssignment (callPrintf memOps) args)--llvmPrintfChkOverride-  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr-     , ?memOpts :: MemOptions )-  => LLVMOverride p sym ext-         (EmptyCtx ::> BVType 32-                   ::> LLVMPointerType wptr-                   ::> VectorType AnyType)-         (BVType 32)-llvmPrintfChkOverride =-  [llvmOvr| i32 @__printf_chk( i32, i8*, ... ) |]-  (\memOps args -> Ctx.uncurryAssignment (\_flg -> callPrintf memOps) args)---llvmPutCharOverride-  :: (IsSymInterface sym, HasPtrWidth wptr)-  => LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)-llvmPutCharOverride =-  [llvmOvr| i32 @putchar( i32 ) |]-  (\memOps args -> Ctx.uncurryAssignment (callPutChar memOps) args)---llvmPutsOverride-  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr-     , ?memOpts :: MemOptions )-  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) (BVType 32)-llvmPutsOverride =-  [llvmOvr| i32 @puts( i8* ) |]-  (\memOps args -> Ctx.uncurryAssignment (callPuts memOps) args)--llvmStrlenOverride-  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr-     , ?memOpts :: MemOptions )-  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) (BVType wptr)-llvmStrlenOverride =-  [llvmOvr| size_t @strlen( i8* ) |]-  (\memOps args -> Ctx.uncurryAssignment (callStrlen memOps) args)--llvmStrnlenOverride-  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr-     , ?memOpts :: MemOptions )-  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType wptr) (BVType wptr)-llvmStrnlenOverride =-  [llvmOvr| size_t @strnlen( i8*, size_t ) |]-  (\memOps args -> Ctx.uncurryAssignment (callStrnlen memOps) args)--llvmStrcpyOverride-  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr-     , ?memOpts :: MemOptions )-  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr) (LLVMPointerType wptr)-llvmStrcpyOverride =-  [llvmOvr| i8* @strcpy( i8*, i8* ) |]-  (\memOps args -> Ctx.uncurryAssignment (callStrcpy memOps) args)--llvmStrdupOverride-  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr-     , ?memOpts :: MemOptions )-  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) (LLVMPointerType wptr)-llvmStrdupOverride =-  [llvmOvr| i8* @strdup( i8* ) |]-  (\memOps args -> Ctx.uncurryAssignment (callStrdup memOps) args)--llvmStrndupOverride-  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr-     , ?memOpts :: MemOptions )-  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType wptr) (LLVMPointerType wptr)-llvmStrndupOverride =-  [llvmOvr| i8* @strndup( i8*, size_t ) |]-  (\memOps args -> Ctx.uncurryAssignment (callStrndup memOps) args)----------------------------------------------------------------------------- ** Implementations----------------------------------------------------------------------------- *** Allocation--callRealloc-  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym-     , ?memOpts :: MemOptions )-  => GlobalVar Mem-  -> Alignment-  -> RegEntry sym (LLVMPointerType wptr)-  -> RegEntry sym (BVType wptr)-  -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))-callRealloc mvar alignment (regValue -> ptr) (regValue -> sz) =-  ovrWithBackend $ \bak -> do-    let sym = backendGetSym bak-    szZero  <- liftIO (notPred sym =<< bvIsNonzero sym sz)-    ptrNull <- liftIO (ptrIsNull sym PtrWidth ptr)-    loc <- liftIO (plSourceLoc <$> getCurrentProgramLoc sym)-    let displayString = "<realloc> " ++ show loc--    symbolicBranches emptyRegMap-      -- If the pointer is null, behave like malloc-      [ ( ptrNull-        , modifyGlobal mvar $ \mem -> liftIO $ doMalloc bak G.HeapAlloc G.Mutable displayString mem sz alignment-        , Nothing-        )--      -- If the size is zero, behave like malloc (of zero bytes) then free-      , (szZero-        , modifyGlobal mvar $ \mem -> liftIO $-             do (newp, mem1) <- doMalloc bak G.HeapAlloc G.Mutable displayString mem sz alignment-                mem2 <- doFree bak mem1 ptr-                return (newp, mem2)-        , Nothing-        )--      -- Otherwise, allocate a new region, memcopy `sz` bytes and free the old pointer-      , (truePred sym-        , modifyGlobal mvar $ \mem -> liftIO $-             do (newp, mem1) <- doMalloc bak G.HeapAlloc G.Mutable displayString mem sz alignment-                mem2 <- uncheckedMemcpy sym mem1 newp ptr sz-                mem3 <- doFree bak mem2 ptr-                return (newp, mem3)-        , Nothing)-      ]---callPosixMemalign-  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr-     , ?lc :: TypeContext, ?memOpts :: MemOptions )-  => GlobalVar Mem-  -> RegEntry sym (LLVMPointerType wptr)-  -> RegEntry sym (BVType wptr)-  -> RegEntry sym (BVType wptr)-  -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))-callPosixMemalign mvar (regValue -> outPtr) (regValue -> align) (regValue -> sz) =-  ovrWithBackend $ \bak ->-    let sym = backendGetSym bak in-    case asBV align of-      Nothing -> fail $ unwords ["posix_memalign: alignment value must be concrete:", show (printSymExpr align)]-      Just concrete_align ->-        case toAlignment (toBytes (BV.asUnsigned concrete_align)) of-          Nothing -> fail $ unwords ["posix_memalign: invalid alignment value:", show concrete_align]-          Just a ->-            let dl = llvmDataLayout ?lc in-            modifyGlobal mvar $ \mem -> liftIO $-               do loc <- plSourceLoc <$> getCurrentProgramLoc sym-                  let displayString = "<posix_memaign> " ++ show loc-                  (p, mem') <- doMalloc bak G.HeapAlloc G.Mutable displayString mem sz a-                  mem'' <- storeRaw bak mem' outPtr (bitvectorType (dl^.ptrSize)) (dl^.ptrAlign) (ptrToPtrVal p)-                  z <- bvZero sym knownNat-                  return (z, mem'')--callMalloc-  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr-     , ?memOpts :: MemOptions )-  => GlobalVar Mem-  -> Alignment-  -> RegEntry sym (BVType wptr)-  -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))-callMalloc mvar alignment (regValue -> sz) =-  ovrWithBackend $ \bak ->-    modifyGlobal mvar $ \mem -> liftIO $-      do loc <- plSourceLoc <$> getCurrentProgramLoc (backendGetSym bak)-         let displayString = "<malloc> " ++ show loc-         doMalloc bak G.HeapAlloc G.Mutable displayString mem sz alignment--callCalloc-  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr-     , ?memOpts :: MemOptions )-  => GlobalVar Mem-  -> Alignment-  -> RegEntry sym (BVType wptr)-  -> RegEntry sym (BVType wptr)-  -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))-callCalloc mvar alignment-           (regValue -> sz)-           (regValue -> num) =-  ovrWithBackend $ \bak ->-    modifyGlobal mvar $ \mem -> liftIO $-      doCalloc bak mem sz num alignment--callFree-  :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)-  => GlobalVar Mem-  -> RegEntry sym (LLVMPointerType wptr)-  -> OverrideSim p sym ext r args ret ()-callFree mvar-           (regValue -> ptr) =-  ovrWithBackend $ \bak ->-    modifyGlobal mvar $ \mem -> liftIO $-      do mem' <- doFree bak mem ptr-         return ((), mem')----------------------------------------------------------------------------- *** Memory manipulation--callMemcpy-  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr-     , ?memOpts :: MemOptions )-  => GlobalVar Mem-  -> RegEntry sym (LLVMPointerType wptr)-  -> RegEntry sym (LLVMPointerType wptr)-  -> RegEntry sym (BVType w)-  -> RegEntry sym (BVType 1)-  -> OverrideSim p sym ext r args ret ()-callMemcpy mvar-           (regValue -> dest)-           (regValue -> src)-           (RegEntry (BVRepr w) len)-           _volatile =-  ovrWithBackend $ \bak ->-    modifyGlobal mvar $ \mem -> liftIO $-      do mem' <- doMemcpy bak w mem True dest src len-         return ((), mem')---- NB the only difference between memcpy and memove--- is that memmove does not assert that the memory--- ranges are disjoint.  The underlying operation--- works correctly in both cases.-callMemmove-  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr-     , ?memOpts :: MemOptions )-  => GlobalVar Mem-  -> RegEntry sym (LLVMPointerType wptr)-  -> RegEntry sym (LLVMPointerType wptr)-  -> RegEntry sym (BVType w)-  -> RegEntry sym (BVType 1)-  -> OverrideSim p sym ext r args ret ()-callMemmove mvar-           (regValue -> dest)-           (regValue -> src)-           (RegEntry (BVRepr w) len)-           _volatile =-  -- FIXME? add assertions about alignment-  ovrWithBackend $ \bak ->-    modifyGlobal mvar $ \mem -> liftIO $-      do mem' <- doMemcpy bak w mem False dest src len-         return ((), mem')--callMemset-  :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)-  => GlobalVar Mem-  -> RegEntry sym (LLVMPointerType wptr)-  -> RegEntry sym (BVType 8)-  -> RegEntry sym (BVType w)-  -> RegEntry sym (BVType 1)-  -> OverrideSim p sym ext r args ret ()-callMemset mvar-           (regValue -> dest)-           (regValue -> val)-           (RegEntry (BVRepr w) len)-           _volatile =-  ovrWithBackend $ \bak ->-    modifyGlobal mvar $ \mem -> liftIO $-      do mem' <- doMemset bak w mem dest val len-         return ((), mem')----------------------------------------------------------------------------- *** Strings and I/O--callPutChar-  :: IsSymInterface sym-  => GlobalVar Mem-  -> RegEntry sym (BVType 32)-  -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))-callPutChar _mvar- (regValue -> ch) = do-    h <- printHandle <$> getContext-    let chval = maybe '?' (toEnum . fromInteger) (BV.asUnsigned <$> asBV ch)-    liftIO $ hPutChar h chval-    return ch--callPuts-  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym-     , ?memOpts :: MemOptions )-  => GlobalVar Mem-  -> RegEntry sym (LLVMPointerType wptr)-  -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))-callPuts mvar-  (regValue -> strPtr) =-    ovrWithBackend $ \bak -> do-      mem <- readGlobal mvar-      str <- liftIO $ CStr.loadString bak mem strPtr Nothing-      h <- printHandle <$> getContext-      liftIO $ hPutStrLn h (UTF8.toString str)-      -- return non-negative value on success-      liftIO $ bvLit (backendGetSym bak) knownNat (BV.one knownNat)--callStrlen-  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym-     , ?memOpts :: MemOptions )-  => GlobalVar Mem-  -> RegEntry sym (LLVMPointerType wptr)-  -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr))-callStrlen mvar (regValue -> strPtr) =-  ovrWithBackend $ \bak -> do-    mem <- readGlobal mvar-    liftIO $ strLen bak mem strPtr--callStrnlen-  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym-     , ?memOpts :: MemOptions )-  => GlobalVar Mem-  -> RegEntry sym (LLVMPointerType wptr)-  -> RegEntry sym (BVType wptr)-  -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr))-callStrnlen mvar (regValue -> strPtr) (regValue -> bound) =-  ovrWithBackend $ \bak -> do-    mem <- readGlobal mvar-    liftIO $ CStr.strnlen bak mem strPtr bound--callStrcpy-  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym-     , ?memOpts :: MemOptions )-  => GlobalVar Mem-  -> RegEntry sym (LLVMPointerType wptr)-  -> RegEntry sym (LLVMPointerType wptr)-  -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))-callStrcpy mvar (regValue -> dst) (regValue -> src) =-  ovrWithBackend $ \bak ->-    modifyGlobal mvar $ \mem -> do-      mem' <- liftIO $ CStr.copyConcretelyNullTerminatedString bak mem dst src Nothing-      pure (dst, mem')--callStrdup-  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym-     , ?memOpts :: MemOptions )-  => GlobalVar Mem-  -> RegEntry sym (LLVMPointerType wptr)-  -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))-callStrdup mvar (regValue -> src) =-  ovrWithBackend $ \bak ->-    modifyGlobal mvar $ \mem -> liftIO $ do-      let sym = backendGetSym bak-      loc <- plSourceLoc <$> getCurrentProgramLoc sym-      let loc' = "<strdup> " ++ show loc-      CStr.dupConcretelyNullTerminatedString bak mem src Nothing loc' noAlignment--callStrndup-  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym-     , ?memOpts :: MemOptions )-  => GlobalVar Mem-  -> RegEntry sym (LLVMPointerType wptr)-  -> RegEntry sym (BVType wptr)-  -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))-callStrndup mvar (regValue -> src) (regValue -> bound) =-  ovrWithBackend $ \bak ->-    modifyGlobal mvar $ \mem -> liftIO $ do-      let sym = backendGetSym bak-      loc <- plSourceLoc <$> getCurrentProgramLoc sym-      let loc' = "<strndup> " ++ show loc-      case BV.asUnsigned <$> asBV bound of-        Nothing -> do-          let err = AssertFailureSimError "`strndup` called with symbolic max length" ""-          addFailedAssertion bak err-        Just b ->-          let bound' = Just (fromIntegral b) in-          CStr.dupConcretelyNullTerminatedString bak mem src bound' loc' noAlignment--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 mvar (Empty :> _pfn :> _pfile :> _pline :> ptxt ) =-  ovrWithBackend $ \bak -> do-    let sym = backendGetSym bak-    when failUponExit $-      do mem <- readGlobal mvar-         txt <- liftIO $ CStr.loadString bak mem (regValue ptxt) Nothing-         let err = AssertFailureSimError "Call to assert()" (UTF8.toString txt)-         liftIO $ addFailedAssertion bak err-    liftIO $-      do loc <- liftIO $ getCurrentProgramLoc sym-         abortExecBecause $ EarlyExit loc-  where-    failUponExit :: Bool-    failUponExit-      = abnormalExitBehavior ?intrinsicsOpts `elem` [AlwaysFail, OnlyAssertFail]--callExit :: ( IsSymInterface sym-            , ?intrinsicsOpts :: IntrinsicsOptions )-         => RegEntry sym (BVType 32)-         -> OverrideSim p sym ext r args ret (RegValue sym UnitType)-callExit ec =-  ovrWithBackend $ \bak -> liftIO $ do-    let sym = backendGetSym bak-    when (abnormalExitBehavior ?intrinsicsOpts == AlwaysFail) $-      do cond <- bvEq sym (regValue ec) =<< bvZero sym knownNat-         -- If the argument is non-zero, throw an assertion failure. Otherwise,-         -- simply stop the current thread of execution.-         assert bak cond "Call to exit() with non-zero argument"-    loc <- getCurrentProgramLoc sym-    abortExecBecause $ EarlyExit loc--callPrintf-  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym-     , ?memOpts :: MemOptions )-  => GlobalVar Mem-  -> RegEntry sym (LLVMPointerType wptr)-  -> RegEntry sym (VectorType AnyType)-  -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))-callPrintf mvar-  (regValue -> strPtr)-  (regValue -> valist) =-    ovrWithBackend $ \bak -> do-      mem <- readGlobal mvar-      formatStr <- liftIO $ CStr.loadString bak mem strPtr Nothing-      case parseDirectives formatStr of-        Left err -> overrideError $ AssertFailureSimError "Format string parsing failed" err-        Right ds -> do-          ((str, n), mem') <- liftIO $ runStateT (executeDirectives (printfOps bak valist) ds) mem-          writeGlobal mvar mem'-          h <- printHandle <$> getContext-          liftIO $ BS.hPutStr h str-          liftIO $ bvLit (backendGetSym bak) knownNat (BV.mkBV knownNat (toInteger n))--printfOps :: ( IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr-             , ?memOpts :: MemOptions )-          => bak-          -> V.Vector (AnyValue sym)-          -> PrintfOperations (StateT (MemImpl sym) IO)-printfOps bak valist =-  let sym = backendGetSym bak in-  PrintfOperations-  { printfUnsupported = \x -> lift $ addFailedAssertion bak-                                   $ Unsupported GHC.callStack x--  , printfGetInteger = \i sgn _len ->-     case valist V.!? (i-1) of-       Just (AnyValue (LLVMPointerRepr w) p@(LLVMPointer _blk bv)) ->-         do isBv <- liftIO (Ptr.ptrIsBv sym p)-            liftIO $ assert bak isBv $-              AssertFailureSimError-               "Passed a pointer to printf where a bitvector was expected"-               ""-            if sgn then-              return $ BV.asSigned w <$> asBV bv-            else-              return $ BV.asUnsigned <$> asBV bv-       Just (AnyValue tpr _) ->-         lift $ addFailedAssertion bak-              $ AssertFailureSimError-                "Type mismatch in printf"-                (unwords ["Expected integer, but got:", show tpr])-       Nothing ->-         lift $ addFailedAssertion bak-              $ AssertFailureSimError-               "Out-of-bounds argument access in printf"-               (unwords ["Index:", show i])--  , printfGetFloat = \i _len ->-     case valist V.!? (i-1) of-       Just (AnyValue (FloatRepr (_fi :: FloatInfoRepr fi)) x) ->-         do xr <- liftIO (iFloatToReal @_ @fi sym x)-            return (asRational xr)-       Just (AnyValue tpr _) ->-         lift $ addFailedAssertion bak-              $ AssertFailureSimError-                "Type mismatch in printf."-                (unwords ["Expected floating-point, but got:", show tpr])-       Nothing ->-         lift $ addFailedAssertion bak-              $ AssertFailureSimError-                "Out-of-bounds argument access in printf:"-                (unwords ["Index:", show i])--  , printfGetString  = \i numchars ->-     case valist V.!? (i-1) of-       Just (AnyValue PtrRepr ptr) ->-           do mem <- get-              liftIO $ CStr.loadString bak mem ptr numchars-       Just (AnyValue tpr _) ->-         lift $ addFailedAssertion bak-              $ AssertFailureSimError-                "Type mismatch in printf."-                (unwords ["Expected char*, but got:", show tpr])-       Nothing ->-         lift $ addFailedAssertion bak-              $ AssertFailureSimError-                "Out-of-bounds argument access in printf:"-                (unwords ["Index:", show i])--  , printfGetPointer = \i ->-     case valist V.!? (i-1) of-       Just (AnyValue PtrRepr ptr) ->-         return $ show (G.ppPtr ptr)-       Just (AnyValue tpr _) ->-         lift $ addFailedAssertion bak-              $ AssertFailureSimError-                "Type mismatch in printf."-                (unwords ["Expected void*, but got:", show tpr])-       Nothing ->-         lift $ addFailedAssertion bak-              $ AssertFailureSimError-                "Out-of-bounds argument access in printf:"-                (unwords ["Index:", show i])--  , printfSetInteger = \i len v ->-     case valist V.!? (i-1) of-       Just (AnyValue PtrRepr ptr) ->-         do mem <- get-            case len of-              Len_Byte  -> do-                 let w8 = knownNat :: NatRepr 8-                 let tp = G.bitvectorType 1-                 x <- liftIO (llvmPointer_bv sym =<< bvLit sym w8 (BV.mkBV w8 (toInteger v)))-                 mem' <- liftIO $ doStore bak mem ptr (LLVMPointerRepr w8) tp noAlignment x-                 put mem'-              Len_Short -> do-                 let w16 = knownNat :: NatRepr 16-                 let tp = G.bitvectorType 2-                 x <- liftIO (llvmPointer_bv sym =<< bvLit sym w16 (BV.mkBV w16 (toInteger v)))-                 mem' <- liftIO $ doStore bak mem ptr (LLVMPointerRepr w16) tp noAlignment x-                 put mem'-              Len_NoMod -> do-                 let w32  = knownNat :: NatRepr 32-                 let tp = G.bitvectorType 4-                 x <- liftIO (llvmPointer_bv sym =<< bvLit sym w32 (BV.mkBV w32 (toInteger v)))-                 mem' <- liftIO $ doStore bak mem ptr (LLVMPointerRepr w32) tp noAlignment x-                 put mem'-              Len_Long  -> do-                 let w64 = knownNat :: NatRepr 64-                 let tp = G.bitvectorType 8-                 x <- liftIO (llvmPointer_bv sym =<< bvLit sym w64 (BV.mkBV w64 (toInteger v)))-                 mem' <- liftIO $ doStore bak mem ptr (LLVMPointerRepr w64) tp noAlignment x-                 put mem'-              _ ->-                lift $ addFailedAssertion bak-                     $ Unsupported GHC.callStack-                     $ unwords ["Unsupported size modifier in %n conversion:", show len]--       Just (AnyValue tpr _) ->-         lift $ addFailedAssertion bak-              $ AssertFailureSimError-                "Type mismatch in printf."-                (unwords ["Expected void*, but got:", show tpr])--       Nothing ->-         lift $ addFailedAssertion bak-              $ AssertFailureSimError-                "Out-of-bounds argument access in printf:"-                (unwords ["Index:", show i])-  }----------------------------------------------------------------------------- *** Math--llvmCeilOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmCeilOverride =-  [llvmOvr| double @ceil( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment callCeil args)--llvmCeilfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmCeilfOverride =-  [llvmOvr| float @ceilf( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment callCeil args)---llvmFloorOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmFloorOverride =-  [llvmOvr| double @floor( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment callFloor args)--llvmFloorfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmFloorfOverride =-  [llvmOvr| float @floorf( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment callFloor args)--llvmFmafOverride ::-     forall sym p ext-   . IsSymInterface sym-  => LLVMOverride p sym ext-        (EmptyCtx ::> FloatType SingleFloat-                  ::> FloatType SingleFloat-                  ::> FloatType SingleFloat)-        (FloatType SingleFloat)-llvmFmafOverride =-  [llvmOvr| float @fmaf( float, float, float ) |]-  (\_memOps args -> Ctx.uncurryAssignment callFMA args)--llvmFmaOverride ::-     forall sym p ext-   . IsSymInterface sym-  => LLVMOverride p sym ext-        (EmptyCtx ::> FloatType DoubleFloat-                  ::> FloatType DoubleFloat-                  ::> FloatType DoubleFloat)-        (FloatType DoubleFloat)-llvmFmaOverride =-  [llvmOvr| double @fma( double, double, double ) |]-  (\_memOps args -> Ctx.uncurryAssignment callFMA args)----- math.h defines isinf() and isnan() as macros, so you might think it unusual--- to provide function overrides for them. However, if you write, say,--- (isnan)(x) instead of isnan(x), Clang will compile the former as a direct--- function call rather than as a macro application. Some experimentation--- reveals that the isnan function's argument is always a double, so we give its--- argument the type double here to match this unstated convention. We follow--- suit similarly with isinf.------ Clang does not yet provide direct function call versions of isfinite() or--- isnormal(), so we do not provide overrides for them.--llvmIsinfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (BVType 32)-llvmIsinfOverride =-  [llvmOvr| i32 @isinf( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callIsinf (knownNat @32)) args)---- __isinf and __isinff are like the isinf macro, except their arguments are--- known to be double or float, respectively. They are not mentioned in the--- POSIX source standard, only the binary standard. See--- http://refspecs.linux-foundation.org/LSB_4.0.0/LSB-Core-generic/LSB-Core-generic/baselib---isinf.html and--- http://refspecs.linux-foundation.org/LSB_4.0.0/LSB-Core-generic/LSB-Core-generic/baselib---isinff.html.-llvm__isinfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (BVType 32)-llvm__isinfOverride =-  [llvmOvr| i32 @__isinf( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callIsinf (knownNat @32)) args)--llvm__isinffOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (BVType 32)-llvm__isinffOverride =-  [llvmOvr| i32 @__isinff( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callIsinf (knownNat @32)) args)--llvmIsnanOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (BVType 32)-llvmIsnanOverride =-  [llvmOvr| i32 @isnan( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args)---- __isnan and __isnanf are like the isnan macro, except their arguments are--- known to be double or float, respectively. They are not mentioned in the--- POSIX source standard, only the binary standard. See--- http://refspecs.linux-foundation.org/LSB_4.0.0/LSB-Core-generic/LSB-Core-generic/baselib---isnan.html and--- http://refspecs.linux-foundation.org/LSB_4.0.0/LSB-Core-generic/LSB-Core-generic/baselib---isnanf.html.-llvm__isnanOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (BVType 32)-llvm__isnanOverride =-  [llvmOvr| i32 @__isnan( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args)--llvm__isnanfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (BVType 32)-llvm__isnanfOverride =-  [llvmOvr| i32 @__isnanf( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args)---- macOS compiles isnan() to __isnand() when the argument is a double.-llvm__isnandOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (BVType 32)-llvm__isnandOverride =-  [llvmOvr| i32 @__isnand( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args)--llvmSqrtOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmSqrtOverride =-  [llvmOvr| double @sqrt( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment callSqrt args)--llvmSqrtfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmSqrtfOverride =-  [llvmOvr| float @sqrtf( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment callSqrt args)--callSpecialFunction1 ::-  forall fi p sym ext r args ret.-  (IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>-  W4.SpecialFunction (EmptyCtx ::> W4.R) ->-  RegEntry sym (FloatType fi) ->-  OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))-callSpecialFunction1 fn (regValue -> x) = do-  sym <- getSymInterface-  liftIO $ iFloatSpecialFunction1 sym (knownRepr :: FloatInfoRepr fi) fn x--callSpecialFunction2 ::-  forall fi p sym ext r args ret.-  (IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>-  W4.SpecialFunction (EmptyCtx ::> W4.R ::> W4.R) ->-  RegEntry sym (FloatType fi) ->-  RegEntry sym (FloatType fi) ->-  OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))-callSpecialFunction2 fn (regValue -> x) (regValue -> y) = do-  sym <- getSymInterface-  liftIO $ iFloatSpecialFunction2 sym (knownRepr :: FloatInfoRepr fi) fn x y--callCeil ::-  forall fi p sym ext r args ret.-  IsSymInterface sym =>-  RegEntry sym (FloatType fi) ->-  OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))-callCeil (regValue -> x) = do-  sym <- getSymInterface-  liftIO $ iFloatRound @_ @fi sym RTP x--callFloor ::-  forall fi p sym ext r args ret.-  IsSymInterface sym =>-  RegEntry sym (FloatType fi) ->-  OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))-callFloor (regValue -> x) = do-  sym <- getSymInterface-  liftIO $ iFloatRound @_ @fi sym RTN x---- | An implementation of @libc@'s @fma@ function.-callFMA ::-     forall fi p sym ext r args ret-   . IsSymInterface sym-  => RegEntry sym (FloatType fi)-  -> RegEntry sym (FloatType fi)-  -> RegEntry sym (FloatType fi)-  -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))-callFMA (regValue -> x) (regValue -> y) (regValue -> z) = do-  sym <- getSymInterface-  liftIO $ iFloatFMA @_ @fi sym defaultRM x y z---- | An implementation of @libc@'s @isinf@ macro. This returns @1@ when the--- argument is positive infinity, @-1@ when the argument is negative infinity,--- and zero otherwise.-callIsinf ::-  forall fi w p sym ext r args ret.-  (IsSymInterface sym, 1 <= w) =>-  NatRepr w ->-  RegEntry sym (FloatType fi) ->-  OverrideSim p sym ext r args ret (RegValue sym (BVType w))-callIsinf w (regValue -> x) = do-  sym <- getSymInterface-  liftIO $ do-    isInf <- iFloatIsInf @_ @fi sym x-    isNeg <- iFloatIsNeg @_ @fi sym x-    isPos <- iFloatIsPos @_ @fi sym x-    isInfN <- andPred sym isInf isNeg-    isInfP <- andPred sym isInf isPos-    bv1 <- bvOne sym w-    bvNeg1 <- bvNeg sym bv1-    bv0 <- bvZero sym w-    res0 <- bvIte sym isInfP bv1 bv0-    bvIte sym isInfN bvNeg1 res0--callIsnan ::-  forall fi w p sym ext r args ret.-  (IsSymInterface sym, 1 <= w) =>-  NatRepr w ->-  RegEntry sym (FloatType fi) ->-  OverrideSim p sym ext r args ret (RegValue sym (BVType w))-callIsnan w (regValue -> x) = do-  sym <- getSymInterface-  liftIO $ do-    isnan  <- iFloatIsNaN @_ @fi sym x-    bv1 <- bvOne sym w-    bv0 <- bvZero sym w-    -- isnan() is allowed to return any nonzero value if the argument is NaN, and-    -- out of all the possible nonzero values, `1` is certainly one of them.-    bvIte sym isnan bv1 bv0--callSqrt ::-  forall fi p sym ext r args ret.-  IsSymInterface sym =>-  RegEntry sym (FloatType fi) ->-  OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))-callSqrt (regValue -> x) = do-  sym <- getSymInterface-  liftIO $ iFloatSqrt @_ @fi sym defaultRM x----------------------------------------------------------------------------- **** Circular trigonometry functions---- sin(f)--llvmSinOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmSinOverride =-  [llvmOvr| double @sin( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sin) args)--llvmSinfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmSinfOverride =-  [llvmOvr| float @sinf( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sin) args)---- cos(f)--llvmCosOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmCosOverride =-  [llvmOvr| double @cos( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cos) args)--llvmCosfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmCosfOverride =-  [llvmOvr| float @cosf( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cos) args)---- tan(f)--llvmTanOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmTanOverride =-  [llvmOvr| double @tan( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tan) args)--llvmTanfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmTanfOverride =-  [llvmOvr| float @tanf( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tan) args)---- asin(f)--llvmAsinOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmAsinOverride =-  [llvmOvr| double @asin( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsin) args)--llvmAsinfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmAsinfOverride =-  [llvmOvr| float @asinf( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsin) args)---- acos(f)--llvmAcosOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmAcosOverride =-  [llvmOvr| double @acos( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccos) args)--llvmAcosfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmAcosfOverride =-  [llvmOvr| float @acosf( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccos) args)---- atan(f)--llvmAtanOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmAtanOverride =-  [llvmOvr| double @atan( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctan) args)--llvmAtanfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmAtanfOverride =-  [llvmOvr| float @atanf( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctan) args)----------------------------------------------------------------------------- **** Hyperbolic trigonometry functions---- sinh(f)--llvmSinhOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmSinhOverride =-  [llvmOvr| double @sinh( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sinh) args)--llvmSinhfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmSinhfOverride =-  [llvmOvr| float @sinhf( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sinh) args)---- cosh(f)--llvmCoshOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmCoshOverride =-  [llvmOvr| double @cosh( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cosh) args)--llvmCoshfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmCoshfOverride =-  [llvmOvr| float @coshf( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cosh) args)---- tanh(f)--llvmTanhOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmTanhOverride =-  [llvmOvr| double @tanh( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tanh) args)--llvmTanhfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmTanhfOverride =-  [llvmOvr| float @tanhf( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tanh) args)---- asinh(f)--llvmAsinhOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmAsinhOverride =-  [llvmOvr| double @asinh( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsinh) args)--llvmAsinhfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmAsinhfOverride =-  [llvmOvr| float @asinhf( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsinh) args)---- acosh(f)--llvmAcoshOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmAcoshOverride =-  [llvmOvr| double @acosh( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccosh) args)--llvmAcoshfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmAcoshfOverride =-  [llvmOvr| float @acoshf( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccosh) args)---- atanh(f)--llvmAtanhOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmAtanhOverride =-  [llvmOvr| double @atanh( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctanh) args)--llvmAtanhfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmAtanhfOverride =-  [llvmOvr| float @atanhf( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctanh) args)----------------------------------------------------------------------------- **** Rectangular to polar coordinate conversion---- hypot(f)--llvmHypotOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmHypotOverride =-  [llvmOvr| double @hypot( double, double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Hypot) args)--llvmHypotfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmHypotfOverride =-  [llvmOvr| float @hypotf( float, float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Hypot) args)---- atan2(f)--llvmAtan2Override ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmAtan2Override =-  [llvmOvr| double @atan2( double, double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Arctan2) args)--llvmAtan2fOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmAtan2fOverride =-  [llvmOvr| float @atan2f( float, float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Arctan2) args)----------------------------------------------------------------------------- **** Exponential and logarithm functions---- pow(f)--llvmPowfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmPowfOverride =-  [llvmOvr| float @powf( float, float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Pow) args)--llvmPowOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmPowOverride =-  [llvmOvr| double @pow( double, double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Pow) args)---- exp(f)--llvmExpOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmExpOverride =-  [llvmOvr| double @exp( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp) args)--llvmExpfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmExpfOverride =-  [llvmOvr| float @expf( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp) args)---- log(f)--llvmLogOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmLogOverride =-  [llvmOvr| double @log( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log) args)--llvmLogfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmLogfOverride =-  [llvmOvr| float @logf( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log) args)---- expm1(f)--llvmExpm1Override ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmExpm1Override =-  [llvmOvr| double @expm1( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Expm1) args)--llvmExpm1fOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmExpm1fOverride =-  [llvmOvr| float @expm1f( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Expm1) args)---- log1p(f)--llvmLog1pOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmLog1pOverride =-  [llvmOvr| double @log1p( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log1p) args)--llvmLog1pfOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmLog1pfOverride =-  [llvmOvr| float @log1pf( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log1p) args)----------------------------------------------------------------------------- **** Base 2 exponential and logarithm---- exp2(f)--llvmExp2Override ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmExp2Override =-  [llvmOvr| double @exp2( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp2) args)--llvmExp2fOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmExp2fOverride =-  [llvmOvr| float @exp2f( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp2) args)---- log2(f)--llvmLog2Override ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmLog2Override =-  [llvmOvr| double @log2( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log2) args)--llvmLog2fOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmLog2fOverride =-  [llvmOvr| float @log2f( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log2) args)----------------------------------------------------------------------------- **** Base 10 exponential and logarithm---- exp10(f)--llvmExp10Override ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmExp10Override =-  [llvmOvr| double @exp10( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args)--llvmExp10fOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmExp10fOverride =-  [llvmOvr| float @exp10f( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args)---- macOS uses __exp10(f) instead of exp10(f).--llvm__exp10Override ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvm__exp10Override =-  [llvmOvr| double @__exp10( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args)--llvm__exp10fOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvm__exp10fOverride =-  [llvmOvr| float @__exp10f( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args)---- log10(f)--llvmLog10Override ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType DoubleFloat)-     (FloatType DoubleFloat)-llvmLog10Override =-  [llvmOvr| double @log10( double ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log10) args)--llvmLog10fOverride ::-  IsSymInterface sym =>-  LLVMOverride p sym ext-     (EmptyCtx ::> FloatType SingleFloat)-     (FloatType SingleFloat)-llvmLog10fOverride =-  [llvmOvr| float @log10f( float ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log10) args)----------------------------------------------------------------------------- *** 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 =-  [llvmOvr| void @__assert_rtn( i8*, i8*, i32, i8* ) |]-  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 =-  [llvmOvr| void @__assert_fail( i8*, i8*, i32, i8* ) |]-  callAssert---llvmAbortOverride-  :: ( IsSymInterface sym-     , ?intrinsicsOpts :: IntrinsicsOptions )-  => LLVMOverride p sym ext EmptyCtx UnitType-llvmAbortOverride =-  [llvmOvr| void @abort() |]-  (\_ _args ->-     ovrWithBackend $ \bak -> liftIO $ do -       let sym = backendGetSym bak-       when (abnormalExitBehavior ?intrinsicsOpts == AlwaysFail) $-           let err = AssertFailureSimError "Call to abort" "" in-           assert bak (falsePred sym) err-       loc <- getCurrentProgramLoc sym-       abortExecBecause $ EarlyExit loc-  )--llvmExitOverride-  :: forall sym p ext-   . ( IsSymInterface sym-     , ?intrinsicsOpts :: IntrinsicsOptions )-  => LLVMOverride p sym ext-         (EmptyCtx ::> BVType 32)-         UnitType-llvmExitOverride =-  [llvmOvr| void @exit( i32 ) |]-  (\_ args -> Ctx.uncurryAssignment callExit args)--llvmGetenvOverride-  :: (IsSymInterface sym, HasPtrWidth wptr)-  => LLVMOverride p sym ext-        (EmptyCtx ::> LLVMPointerType wptr)-        (LLVMPointerType wptr)-llvmGetenvOverride =-  [llvmOvr| i8* @getenv( i8* ) |]-  (\_ _args -> do-    sym <- getSymInterface-    liftIO $ mkNullPointer sym PtrWidth)--llvmHtonlOverride ::-  (IsSymInterface sym, ?lc :: TypeContext) =>-  LLVMOverride p sym ext-      (EmptyCtx ::> BVType 32)-      (BVType 32)-llvmHtonlOverride =-  [llvmOvr| i32 @htonl( i32 ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @4)) args)--llvmHtonsOverride ::-  (IsSymInterface sym, ?lc :: TypeContext) =>-  LLVMOverride p sym ext-      (EmptyCtx ::> BVType 16)-      (BVType 16)-llvmHtonsOverride =-  [llvmOvr| i16 @htons( i16 ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @2)) args)--llvmNtohlOverride ::-  (IsSymInterface sym, ?lc :: TypeContext) =>-  LLVMOverride p sym ext-      (EmptyCtx ::> BVType 32)-      (BVType 32)-llvmNtohlOverride =-  [llvmOvr| i32 @ntohl( i32 ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @4)) args)--llvmNtohsOverride ::-  (IsSymInterface sym, ?lc :: TypeContext) =>-  LLVMOverride p sym ext-      (EmptyCtx ::> BVType 16)-      (BVType 16)-llvmNtohsOverride =-  [llvmOvr| i16 @ntohs( i16 ) |]-  (\_memOps args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @2)) args)--llvmAbsOverride ::-  (IsSymInterface sym, HasLLVMAnn sym) =>-  LLVMOverride p sym ext-      (EmptyCtx ::> BVType 32)-      (BVType 32)-llvmAbsOverride =-  [llvmOvr| i32 @abs( i32 ) |]-  (\mvar args ->-     do callStack <- callStackFromMemVar' mvar-        Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @32)) args)---- @labs@ uses `long` as its argument and result type, so we need two overrides--- for @labs@. See Note [Overrides involving (unsigned) long] in--- Lang.Crucible.LLVM.Intrinsics.-llvmLAbsOverride_32 ::-  (IsSymInterface sym, HasLLVMAnn sym) =>-  LLVMOverride p sym ext-      (EmptyCtx ::> BVType 32)-      (BVType 32)-llvmLAbsOverride_32 =-  [llvmOvr| i32 @labs( i32 ) |]-  (\mvar args ->-     do callStack <- callStackFromMemVar' mvar-        Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @32)) args)--llvmLAbsOverride_64 ::-  (IsSymInterface sym, HasLLVMAnn sym) =>-  LLVMOverride p sym ext-      (EmptyCtx ::> BVType 64)-      (BVType 64)-llvmLAbsOverride_64 =-  [llvmOvr| i64 @labs( i64 ) |]-  (\mvar args ->-     do callStack <- callStackFromMemVar' mvar-        Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @64)) args)--llvmLLAbsOverride ::-  (IsSymInterface sym, HasLLVMAnn sym) =>-  LLVMOverride p sym ext-      (EmptyCtx ::> BVType 64)-      (BVType 64)-llvmLLAbsOverride =-  [llvmOvr| i64 @llabs( i64 ) |]-  (\mvar args ->-     do callStack <- callStackFromMemVar' mvar-        Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @64)) 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 widthRepr (regValue -> vec) = do-  sym <- getSymInterface-  liftIO $ bvSwap sym widthRepr vec---- | This determines under what circumstances @callAbs@ should check if its--- argument is equal to the smallest signed integer of a particular size--- (e.g., @INT_MIN@), and if it is equal to that value, what kind of error--- should be reported.-data CheckAbsIntMin-  = LibcAbsIntMinUB-    -- ^ For the @abs@, @labs@, and @llabs@ functions, always check if the-    --   argument is equal to @INT_MIN@. If so, report it as undefined-    --   behavior per the C standard.-  | LLVMAbsIntMinPoison Bool-    -- ^ For the @llvm.abs.*@ family of LLVM intrinsics, check if the argument-    --   is equal to @INT_MIN@ only when the 'Bool' argument is 'True'. If it-    --   is 'True' and the argument is equal to @INT_MIN@, return poison.---- | The workhorse for the @abs@, @labs@, and @llabs@ functions, as well as the--- @llvm.abs.*@ family of overloaded intrinsics.-callAbs ::-  forall w p sym ext r args ret.-  (1 <= w, IsSymInterface sym, HasLLVMAnn sym) =>-  CallStack ->-  CheckAbsIntMin ->-  NatRepr w ->-  RegEntry sym (BVType w) ->-  OverrideSim p sym ext r args ret (RegValue sym (BVType w))-callAbs callStack checkIntMin widthRepr (regValue -> src) = do-  sym <- getSymInterface-  ovrWithBackend $ \bak -> liftIO $ do-    bvIntMin    <- bvLit sym widthRepr (BV.minSigned widthRepr)-    isNotIntMin <- notPred sym =<< bvEq sym src bvIntMin--    when shouldCheckIntMin $ do-      isNotIntMinUB <- annotateUB sym callStack ub isNotIntMin-      let err = AssertFailureSimError "Undefined behavior encountered" $-                show $ UB.explain ub-      assert bak isNotIntMinUB err--    isSrcNegative <- bvIsNeg sym src-    srcNegated    <- bvNeg sym src-    bvIte sym isSrcNegative srcNegated src-    where-      shouldCheckIntMin :: Bool-      shouldCheckIntMin =-        case checkIntMin of-          LibcAbsIntMinUB                 -> True-          LLVMAbsIntMinPoison shouldCheck -> shouldCheck--      ub :: UB.UndefinedBehavior (RegValue' sym)-      ub = case checkIntMin of-             LibcAbsIntMinUB ->-               UB.AbsIntMin $ RV src-             LLVMAbsIntMinPoison{} ->-               UB.PoisonValueCreated $ Poison.LLVMAbsIntMin $ RV src--callLibcAbs ::-  (1 <= w, IsSymInterface sym, HasLLVMAnn sym) =>-  CallStack ->-  NatRepr w ->-  RegEntry sym (BVType w) ->-  OverrideSim p sym ext r args ret (RegValue sym (BVType w))-callLibcAbs callStack = callAbs callStack LibcAbsIntMinUB--callLLVMAbs ::-  (1 <= w, IsSymInterface sym, HasLLVMAnn sym) =>-  CallStack ->-  NatRepr w ->-  RegEntry sym (BVType w) ->-  RegEntry sym (BVType 1) ->-  OverrideSim p sym ext r args ret (RegValue sym (BVType w))-callLLVMAbs callStack widthRepr src (regValue -> isIntMinPoison) = do-  shouldCheckIntMin <- liftIO $-    -- Per https://releases.llvm.org/12.0.0/docs/LangRef.html#id451, the second-    -- argument must be a constant.-    case asBV isIntMinPoison of-      Just bv -> pure (bv /= BV.zero (knownNat @1))-      Nothing -> malformedLLVMModule-                   "Call to llvm.abs.* with non-constant second argument"-                   [printSymExpr isIntMinPoison]-  callAbs callStack (LLVMAbsIntMinPoison shouldCheckIntMin) widthRepr src---- | 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 widthRepr vec =-  case (llvmDataLayout ?lc)^.intLayout of-    BigEndian    -> pure (regValue vec)-    LittleEndian -> callBSwap widthRepr vec--------------------------------------------------------------------------------- atexit stuff--cxa_atexitOverride-  :: (IsSymInterface sym, HasPtrWidth wptr)-  => LLVMOverride p sym ext-        (EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr ::> LLVMPointerType wptr)-        (BVType 32)-cxa_atexitOverride =-  [llvmOvr| i32 @__cxa_atexit( void (i8*)*, i8*, i8* ) |]-  (\_ _args -> do-    sym <- getSymInterface-    liftIO $ bvZero sym knownNat)---------------------------------------------------------------------------------- | IEEE 754 declares 'RNE' to be the default rounding mode, and most @libc@--- implementations agree with this in practice. The only places where we do not--- use this as the default are operations that specifically require the behavior--- of a particular rounding mode, such as @ceil@ or @floor@.-defaultRM :: RoundingMode-defaultRM = RNE+{-# 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 =+  [ SomeLLVMOverride llvmAssertRtnOverride+  , SomeLLVMOverride llvmAssertFailOverride+  , SomeLLVMOverride llvmHtonlOverride+  , SomeLLVMOverride llvmHtonsOverride+  , SomeLLVMOverride llvmNtohlOverride+  , SomeLLVMOverride llvmNtohsOverride+  ]+  ++ mathOverrides+  ++ stdioOverrides+  ++ stdlibOverrides+  ++ 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 mvar (Empty :> _pfn :> _pfile :> _pline :> ptxt ) =+  ovrWithBackend $ \bak -> do+    let sym = backendGetSym bak+    when failUponExit $+      do mem <- readGlobal mvar+         txt <- liftIO $ CStr.loadString bak mem (regValue ptxt) Nothing+         let err = AssertFailureSimError "Call to assert()" (UTF8.toString txt)+         liftIO $ addFailedAssertion bak err+    liftIO $+      do loc <- liftIO $ getCurrentProgramLoc sym+         abortExecBecause $ EarlyExit loc+  where+    failUponExit :: Bool+    failUponExit+      = abnormalExitBehavior ?intrinsicsOpts `elem` [AlwaysFail, 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 =+  [llvmOvr| void @__assert_rtn( i8*, i8*, i32, i8* ) |]+  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 =+  [llvmOvr| void @__assert_fail( i8*, i8*, i32, i8* ) |]+  callAssert++++llvmHtonlOverride ::+  (IsSymInterface sym, ?lc :: TypeContext) =>+  LLVMOverride p sym ext+      (EmptyCtx ::> BVType 32)+      (BVType 32)+llvmHtonlOverride =+  [llvmOvr| i32 @htonl( i32 ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @4)) args)++llvmHtonsOverride ::+  (IsSymInterface sym, ?lc :: TypeContext) =>+  LLVMOverride p sym ext+      (EmptyCtx ::> BVType 16)+      (BVType 16)+llvmHtonsOverride =+  [llvmOvr| i16 @htons( i16 ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @2)) args)++llvmNtohlOverride ::+  (IsSymInterface sym, ?lc :: TypeContext) =>+  LLVMOverride p sym ext+      (EmptyCtx ::> BVType 32)+      (BVType 32)+llvmNtohlOverride =+  [llvmOvr| i32 @ntohl( i32 ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @4)) args)++llvmNtohsOverride ::+  (IsSymInterface sym, ?lc :: TypeContext) =>+  LLVMOverride p sym ext+      (EmptyCtx ::> BVType 16)+      (BVType 16)+llvmNtohsOverride =+  [llvmOvr| i16 @ntohs( i16 ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @2)) 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 widthRepr (regValue -> vec) = do+  sym <- getSymInterface+  liftIO $ bvSwap sym widthRepr 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 widthRepr vec =+  case (llvmDataLayout ?lc)^.intLayout of+    BigEndian    -> pure (regValue vec)+    LittleEndian -> callBSwap widthRepr vec+++----------------------------------------------------------------------------+

@@ -0,0 +1,961 @@+-- |+-- Module           : Lang.Crucible.LLVM.Intrinsics.Libc.Math+-- Description      : Override definitions for C @math.h@ functions+-- Copyright        : (c) Galois, Inc 2026+-- License          : BSD3+-- Maintainer       : Galois, Inc. <crux@galois.com>+-- Stability        : provisional+------------------------------------------------------------------------++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ViewPatterns #-}++module Lang.Crucible.LLVM.Intrinsics.Libc.Math+  ( -- * @math.h@ overrides+    mathOverrides+    -- * Override declarations+  , llvmCeilOverride+  , llvmCeilfOverride+  , llvmFloorOverride+  , llvmFloorfOverride+  , llvmFmaOverride+  , llvmFmafOverride+  , llvmIsinfOverride+  , llvm__isinfOverride+  , llvm__isinffOverride+  , llvmIsnanOverride+  , llvm__isnanOverride+  , llvm__isnanfOverride+  , llvm__isnandOverride+  , llvmSqrtOverride+  , llvmSqrtfOverride+  , llvmSinOverride+  , llvmSinfOverride+  , llvmCosOverride+  , llvmCosfOverride+  , llvmTanOverride+  , llvmTanfOverride+  , llvmAsinOverride+  , llvmAsinfOverride+  , llvmAcosOverride+  , llvmAcosfOverride+  , llvmAtanOverride+  , llvmAtanfOverride+  , llvmSinhOverride+  , llvmSinhfOverride+  , llvmCoshOverride+  , llvmCoshfOverride+  , llvmTanhOverride+  , llvmTanhfOverride+  , llvmAsinhOverride+  , llvmAsinhfOverride+  , llvmAcoshOverride+  , llvmAcoshfOverride+  , llvmAtanhOverride+  , llvmAtanhfOverride+  , llvmHypotOverride+  , llvmHypotfOverride+  , llvmAtan2Override+  , llvmAtan2fOverride+  , llvmPowfOverride+  , llvmPowOverride+  , llvmExpOverride+  , llvmExpfOverride+  , llvmLogOverride+  , llvmLogfOverride+  , llvmExpm1Override+  , llvmExpm1fOverride+  , llvmLog1pOverride+  , llvmLog1pfOverride+  , llvmExp2Override+  , llvmExp2fOverride+  , llvmLog2Override+  , llvmLog2fOverride+  , llvmExp10Override+  , llvmExp10fOverride+  , llvm__exp10Override+  , llvm__exp10fOverride+  , llvmLog10Override+  , llvmLog10fOverride+    -- * Implementation functions+  , callCeil+  , callFloor+  , callFMA+  , callIsinf+  , callIsnan+  , callSqrt+  , callSpecialFunction1+  , callSpecialFunction2+  , defaultRM+  ) where++import           Control.Monad.IO.Class (liftIO)++import qualified Data.Parameterized.Context as Ctx++import           What4.Interface+import qualified What4.SpecialFunctions as W4++import           Lang.Crucible.Backend+import           Lang.Crucible.Types+import           Lang.Crucible.Simulator.OverrideSim+import           Lang.Crucible.Simulator.RegMap++import           Lang.Crucible.LLVM.QQ( llvmOvr )++import           Lang.Crucible.LLVM.Intrinsics.Common++-- | All @math.h@ overrides+mathOverrides ::+  IsSymInterface sym =>+  [SomeLLVMOverride p sym ext]+mathOverrides =+  [ SomeLLVMOverride llvmCeilOverride+  , SomeLLVMOverride llvmCeilfOverride+  , SomeLLVMOverride llvmFloorOverride+  , SomeLLVMOverride llvmFloorfOverride+  , SomeLLVMOverride llvmFmaOverride+  , SomeLLVMOverride llvmFmafOverride+  , SomeLLVMOverride llvmIsinfOverride+  , SomeLLVMOverride llvm__isinfOverride+  , SomeLLVMOverride llvm__isinffOverride+  , SomeLLVMOverride llvmIsnanOverride+  , SomeLLVMOverride llvm__isnanOverride+  , SomeLLVMOverride llvm__isnanfOverride+  , SomeLLVMOverride llvm__isnandOverride+  , SomeLLVMOverride llvmSqrtOverride+  , SomeLLVMOverride llvmSqrtfOverride+  , SomeLLVMOverride llvmSinOverride+  , SomeLLVMOverride llvmSinfOverride+  , SomeLLVMOverride llvmCosOverride+  , SomeLLVMOverride llvmCosfOverride+  , SomeLLVMOverride llvmTanOverride+  , SomeLLVMOverride llvmTanfOverride+  , SomeLLVMOverride llvmAsinOverride+  , SomeLLVMOverride llvmAsinfOverride+  , SomeLLVMOverride llvmAcosOverride+  , SomeLLVMOverride llvmAcosfOverride+  , SomeLLVMOverride llvmAtanOverride+  , SomeLLVMOverride llvmAtanfOverride+  , SomeLLVMOverride llvmSinhOverride+  , SomeLLVMOverride llvmSinhfOverride+  , SomeLLVMOverride llvmCoshOverride+  , SomeLLVMOverride llvmCoshfOverride+  , SomeLLVMOverride llvmTanhOverride+  , SomeLLVMOverride llvmTanhfOverride+  , SomeLLVMOverride llvmAsinhOverride+  , SomeLLVMOverride llvmAsinhfOverride+  , SomeLLVMOverride llvmAcoshOverride+  , SomeLLVMOverride llvmAcoshfOverride+  , SomeLLVMOverride llvmAtanhOverride+  , SomeLLVMOverride llvmAtanhfOverride+  , SomeLLVMOverride llvmHypotOverride+  , SomeLLVMOverride llvmHypotfOverride+  , SomeLLVMOverride llvmAtan2Override+  , SomeLLVMOverride llvmAtan2fOverride+  , SomeLLVMOverride llvmPowfOverride+  , SomeLLVMOverride llvmPowOverride+  , SomeLLVMOverride llvmExpOverride+  , SomeLLVMOverride llvmExpfOverride+  , SomeLLVMOverride llvmLogOverride+  , SomeLLVMOverride llvmLogfOverride+  , SomeLLVMOverride llvmExpm1Override+  , SomeLLVMOverride llvmExpm1fOverride+  , SomeLLVMOverride llvmLog1pOverride+  , SomeLLVMOverride llvmLog1pfOverride+  , SomeLLVMOverride llvmExp2Override+  , SomeLLVMOverride llvmExp2fOverride+  , SomeLLVMOverride llvmLog2Override+  , SomeLLVMOverride llvmLog2fOverride+  , SomeLLVMOverride llvmExp10Override+  , SomeLLVMOverride llvmExp10fOverride+  , SomeLLVMOverride llvm__exp10Override+  , SomeLLVMOverride llvm__exp10fOverride+  , SomeLLVMOverride llvmLog10Override+  , SomeLLVMOverride llvmLog10fOverride+  ]++------------------------------------------------------------------------+-- ** Declarations++llvmCeilOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmCeilOverride =+  [llvmOvr| double @ceil( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment callCeil args)++llvmCeilfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmCeilfOverride =+  [llvmOvr| float @ceilf( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment callCeil args)+++llvmFloorOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmFloorOverride =+  [llvmOvr| double @floor( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment callFloor args)++llvmFloorfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmFloorfOverride =+  [llvmOvr| float @floorf( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment callFloor args)++llvmFmafOverride ::+     forall sym p ext+   . IsSymInterface sym+  => LLVMOverride p sym ext+        (EmptyCtx ::> FloatType SingleFloat+                  ::> FloatType SingleFloat+                  ::> FloatType SingleFloat)+        (FloatType SingleFloat)+llvmFmafOverride =+  [llvmOvr| float @fmaf( float, float, float ) |]+  (\_memOps args -> Ctx.uncurryAssignment callFMA args)++llvmFmaOverride ::+     forall sym p ext+   . IsSymInterface sym+  => LLVMOverride p sym ext+        (EmptyCtx ::> FloatType DoubleFloat+                  ::> FloatType DoubleFloat+                  ::> FloatType DoubleFloat)+        (FloatType DoubleFloat)+llvmFmaOverride =+  [llvmOvr| double @fma( double, double, double ) |]+  (\_memOps args -> Ctx.uncurryAssignment callFMA args)+++-- math.h defines isinf() and isnan() as macros, so you might think it unusual+-- to provide function overrides for them. However, if you write, say,+-- (isnan)(x) instead of isnan(x), Clang will compile the former as a direct+-- function call rather than as a macro application. Some experimentation+-- reveals that the isnan function's argument is always a double, so we give its+-- argument the type double here to match this unstated convention. We follow+-- suit similarly with isinf.+--+-- Clang does not yet provide direct function call versions of isfinite() or+-- isnormal(), so we do not provide overrides for them.++llvmIsinfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (BVType 32)+llvmIsinfOverride =+  [llvmOvr| i32 @isinf( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callIsinf (knownNat @32)) args)++-- __isinf and __isinff are like the isinf macro, except their arguments are+-- known to be double or float, respectively. They are not mentioned in the+-- POSIX source standard, only the binary standard. See+-- http://refspecs.linux-foundation.org/LSB_4.0.0/LSB-Core-generic/LSB-Core-generic/baselib---isinf.html and+-- http://refspecs.linux-foundation.org/LSB_4.0.0/LSB-Core-generic/LSB-Core-generic/baselib---isinff.html.+llvm__isinfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (BVType 32)+llvm__isinfOverride =+  [llvmOvr| i32 @__isinf( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callIsinf (knownNat @32)) args)++llvm__isinffOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (BVType 32)+llvm__isinffOverride =+  [llvmOvr| i32 @__isinff( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callIsinf (knownNat @32)) args)++llvmIsnanOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (BVType 32)+llvmIsnanOverride =+  [llvmOvr| i32 @isnan( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args)++-- __isnan and __isnanf are like the isnan macro, except their arguments are+-- known to be double or float, respectively. They are not mentioned in the+-- POSIX source standard, only the binary standard. See+-- http://refspecs.linux-foundation.org/LSB_4.0.0/LSB-Core-generic/LSB-Core-generic/baselib---isnan.html and+-- http://refspecs.linux-foundation.org/LSB_4.0.0/LSB-Core-generic/LSB-Core-generic/baselib---isnanf.html.+llvm__isnanOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (BVType 32)+llvm__isnanOverride =+  [llvmOvr| i32 @__isnan( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args)++llvm__isnanfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (BVType 32)+llvm__isnanfOverride =+  [llvmOvr| i32 @__isnanf( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args)++-- macOS compiles isnan() to __isnand() when the argument is a double.+llvm__isnandOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (BVType 32)+llvm__isnandOverride =+  [llvmOvr| i32 @__isnand( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args)++llvmSqrtOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmSqrtOverride =+  [llvmOvr| double @sqrt( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment callSqrt args)++llvmSqrtfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmSqrtfOverride =+  [llvmOvr| float @sqrtf( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment callSqrt args)++------------------------------------------------------------------------+-- **** Circular trigonometry functions++-- sin(f)++llvmSinOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmSinOverride =+  [llvmOvr| double @sin( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sin) args)++llvmSinfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmSinfOverride =+  [llvmOvr| float @sinf( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sin) args)++-- cos(f)++llvmCosOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmCosOverride =+  [llvmOvr| double @cos( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cos) args)++llvmCosfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmCosfOverride =+  [llvmOvr| float @cosf( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cos) args)++-- tan(f)++llvmTanOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmTanOverride =+  [llvmOvr| double @tan( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tan) args)++llvmTanfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmTanfOverride =+  [llvmOvr| float @tanf( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tan) args)++-- asin(f)++llvmAsinOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmAsinOverride =+  [llvmOvr| double @asin( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsin) args)++llvmAsinfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmAsinfOverride =+  [llvmOvr| float @asinf( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsin) args)++-- acos(f)++llvmAcosOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmAcosOverride =+  [llvmOvr| double @acos( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccos) args)++llvmAcosfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmAcosfOverride =+  [llvmOvr| float @acosf( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccos) args)++-- atan(f)++llvmAtanOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmAtanOverride =+  [llvmOvr| double @atan( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctan) args)++llvmAtanfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmAtanfOverride =+  [llvmOvr| float @atanf( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctan) args)++------------------------------------------------------------------------+-- **** Hyperbolic trigonometry functions++-- sinh(f)++llvmSinhOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmSinhOverride =+  [llvmOvr| double @sinh( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sinh) args)++llvmSinhfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmSinhfOverride =+  [llvmOvr| float @sinhf( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sinh) args)++-- cosh(f)++llvmCoshOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmCoshOverride =+  [llvmOvr| double @cosh( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cosh) args)++llvmCoshfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmCoshfOverride =+  [llvmOvr| float @coshf( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cosh) args)++-- tanh(f)++llvmTanhOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmTanhOverride =+  [llvmOvr| double @tanh( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tanh) args)++llvmTanhfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmTanhfOverride =+  [llvmOvr| float @tanhf( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tanh) args)++-- asinh(f)++llvmAsinhOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmAsinhOverride =+  [llvmOvr| double @asinh( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsinh) args)++llvmAsinhfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmAsinhfOverride =+  [llvmOvr| float @asinhf( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsinh) args)++-- acosh(f)++llvmAcoshOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmAcoshOverride =+  [llvmOvr| double @acosh( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccosh) args)++llvmAcoshfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmAcoshfOverride =+  [llvmOvr| float @acoshf( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccosh) args)++-- atanh(f)++llvmAtanhOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmAtanhOverride =+  [llvmOvr| double @atanh( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctanh) args)++llvmAtanhfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmAtanhfOverride =+  [llvmOvr| float @atanhf( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctanh) args)++------------------------------------------------------------------------+-- **** Rectangular to polar coordinate conversion++-- hypot(f)++llvmHypotOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmHypotOverride =+  [llvmOvr| double @hypot( double, double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Hypot) args)++llvmHypotfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmHypotfOverride =+  [llvmOvr| float @hypotf( float, float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Hypot) args)++-- atan2(f)++llvmAtan2Override ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmAtan2Override =+  [llvmOvr| double @atan2( double, double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Arctan2) args)++llvmAtan2fOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmAtan2fOverride =+  [llvmOvr| float @atan2f( float, float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Arctan2) args)++------------------------------------------------------------------------+-- **** Exponential and logarithm functions++-- pow(f)++llvmPowfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmPowfOverride =+  [llvmOvr| float @powf( float, float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Pow) args)++llvmPowOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmPowOverride =+  [llvmOvr| double @pow( double, double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Pow) args)++-- exp(f)++llvmExpOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmExpOverride =+  [llvmOvr| double @exp( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp) args)++llvmExpfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmExpfOverride =+  [llvmOvr| float @expf( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp) args)++-- log(f)++llvmLogOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmLogOverride =+  [llvmOvr| double @log( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log) args)++llvmLogfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmLogfOverride =+  [llvmOvr| float @logf( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log) args)++-- expm1(f)++llvmExpm1Override ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmExpm1Override =+  [llvmOvr| double @expm1( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Expm1) args)++llvmExpm1fOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmExpm1fOverride =+  [llvmOvr| float @expm1f( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Expm1) args)++-- log1p(f)++llvmLog1pOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmLog1pOverride =+  [llvmOvr| double @log1p( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log1p) args)++llvmLog1pfOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmLog1pfOverride =+  [llvmOvr| float @log1pf( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log1p) args)++------------------------------------------------------------------------+-- **** Base 2 exponential and logarithm++-- exp2(f)++llvmExp2Override ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmExp2Override =+  [llvmOvr| double @exp2( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp2) args)++llvmExp2fOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmExp2fOverride =+  [llvmOvr| float @exp2f( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp2) args)++-- log2(f)++llvmLog2Override ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmLog2Override =+  [llvmOvr| double @log2( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log2) args)++llvmLog2fOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmLog2fOverride =+  [llvmOvr| float @log2f( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log2) args)++------------------------------------------------------------------------+-- **** Base 10 exponential and logarithm++-- exp10(f)++llvmExp10Override ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmExp10Override =+  [llvmOvr| double @exp10( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args)++llvmExp10fOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmExp10fOverride =+  [llvmOvr| float @exp10f( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args)++-- macOS uses __exp10(f) instead of exp10(f).++llvm__exp10Override ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvm__exp10Override =+  [llvmOvr| double @__exp10( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args)++llvm__exp10fOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvm__exp10fOverride =+  [llvmOvr| float @__exp10f( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args)++-- log10(f)++llvmLog10Override ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmLog10Override =+  [llvmOvr| double @log10( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log10) args)++llvmLog10fOverride ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmLog10fOverride =+  [llvmOvr| float @log10f( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log10) args)++------------------------------------------------------------------------+-- ** Implementations++callSpecialFunction1 ::+  forall fi p sym ext r args ret.+  (IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>+  W4.SpecialFunction (EmptyCtx ::> W4.R) ->+  RegEntry sym (FloatType fi) ->+  OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))+callSpecialFunction1 fn (regValue -> x) = do+  sym <- getSymInterface+  liftIO $ iFloatSpecialFunction1 sym (knownRepr :: FloatInfoRepr fi) fn x++callSpecialFunction2 ::+  forall fi p sym ext r args ret.+  (IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>+  W4.SpecialFunction (EmptyCtx ::> W4.R ::> W4.R) ->+  RegEntry sym (FloatType fi) ->+  RegEntry sym (FloatType fi) ->+  OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))+callSpecialFunction2 fn (regValue -> x) (regValue -> y) = do+  sym <- getSymInterface+  liftIO $ iFloatSpecialFunction2 sym (knownRepr :: FloatInfoRepr fi) fn x y++callCeil ::+  forall fi p sym ext r args ret.+  IsSymInterface sym =>+  RegEntry sym (FloatType fi) ->+  OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))+callCeil (regValue -> x) = do+  sym <- getSymInterface+  liftIO $ iFloatRound @_ @fi sym RTP x++callFloor ::+  forall fi p sym ext r args ret.+  IsSymInterface sym =>+  RegEntry sym (FloatType fi) ->+  OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))+callFloor (regValue -> x) = do+  sym <- getSymInterface+  liftIO $ iFloatRound @_ @fi sym RTN x++-- | An implementation of @libc@'s @fma@ function.+callFMA ::+     forall fi p sym ext r args ret+   . IsSymInterface sym+  => RegEntry sym (FloatType fi)+  -> RegEntry sym (FloatType fi)+  -> RegEntry sym (FloatType fi)+  -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))+callFMA (regValue -> x) (regValue -> y) (regValue -> z) = do+  sym <- getSymInterface+  liftIO $ iFloatFMA @_ @fi sym defaultRM x y z++-- | An implementation of @libc@'s @isinf@ macro. This returns @1@ when the+-- argument is positive infinity, @-1@ when the argument is negative infinity,+-- and zero otherwise.+callIsinf ::+  forall fi w p sym ext r args ret.+  (IsSymInterface sym, 1 <= w) =>+  NatRepr w ->+  RegEntry sym (FloatType fi) ->+  OverrideSim p sym ext r args ret (RegValue sym (BVType w))+callIsinf w (regValue -> x) = do+  sym <- getSymInterface+  liftIO $ do+    isInf <- iFloatIsInf @_ @fi sym x+    isNeg <- iFloatIsNeg @_ @fi sym x+    isPos <- iFloatIsPos @_ @fi sym x+    isInfN <- andPred sym isInf isNeg+    isInfP <- andPred sym isInf isPos+    bv1 <- bvOne sym w+    bvNeg1 <- bvNeg sym bv1+    bv0 <- bvZero sym w+    res0 <- bvIte sym isInfP bv1 bv0+    bvIte sym isInfN bvNeg1 res0++callIsnan ::+  forall fi w p sym ext r args ret.+  (IsSymInterface sym, 1 <= w) =>+  NatRepr w ->+  RegEntry sym (FloatType fi) ->+  OverrideSim p sym ext r args ret (RegValue sym (BVType w))+callIsnan w (regValue -> x) = do+  sym <- getSymInterface+  liftIO $ do+    isnan  <- iFloatIsNaN @_ @fi sym x+    bv1 <- bvOne sym w+    bv0 <- bvZero sym w+    -- isnan() is allowed to return any nonzero value if the argument is NaN, and+    -- out of all the possible nonzero values, `1` is certainly one of them.+    bvIte sym isnan bv1 bv0++callSqrt ::+  forall fi p sym ext r args ret.+  IsSymInterface sym =>+  RegEntry sym (FloatType fi) ->+  OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))+callSqrt (regValue -> x) = do+  sym <- getSymInterface+  liftIO $ iFloatSqrt @_ @fi sym defaultRM x++-- | IEEE 754 declares 'RNE' to be the default rounding mode, and most @libc@+-- implementations agree with this in practice. The only places where we do not+-- use this as the default are operations that specifically require the behavior+-- of a particular rounding mode, such as @ceil@ or @floor@.+defaultRM :: RoundingMode+defaultRM = RNE

@@ -0,0 +1,306 @@+-- |+-- Module           : Lang.Crucible.LLVM.Intrinsics.Libc.Stdio+-- Description      : Override definitions for C @stdio.h@ functions+-- Copyright        : (c) Galois, Inc 2026+-- License          : BSD3+-- Maintainer       : Galois, Inc. <crux@galois.com>+-- Stability        : provisional+------------------------------------------------------------------------++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ViewPatterns #-}++module Lang.Crucible.LLVM.Intrinsics.Libc.Stdio+  ( -- * @stdio.h@ overrides+    stdioOverrides+    -- * Override declarations+  , llvmPrintfOverride+  , llvmPrintfChkOverride+  , llvmPutsOverride+  , llvmPutCharOverride+    -- * Implementation functions+  , callPrintf+  , callPutChar+  , callPuts+  , printfOps+  ) where++import           Control.Monad.IO.Class (liftIO)+import           Control.Monad.State (StateT(..), get, put)+import           Control.Monad.Trans.Class (MonadTrans(..))+import qualified Codec.Binary.UTF8.Generic as UTF8+import qualified Data.ByteString as BS+import qualified Data.Vector as V+import           System.IO+import qualified GHC.Stack as GHC++import qualified Data.BitVector.Sized as BV+import           Data.Parameterized.Context (pattern Empty)+import qualified Data.Parameterized.Context as Ctx++import           What4.Interface++import           Lang.Crucible.Backend+import           Lang.Crucible.CFG.Common+import           Lang.Crucible.Simulator (printHandle)+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 qualified Lang.Crucible.LLVM.MemModel.Generic as G+import qualified Lang.Crucible.LLVM.MemModel.Pointer as Ptr+import           Lang.Crucible.LLVM.MemModel.Strings as CStr+import qualified Lang.Crucible.LLVM.MemModel.Type as G+import           Lang.Crucible.LLVM.Printf+import           Lang.Crucible.LLVM.QQ( llvmOvr )++import           Lang.Crucible.LLVM.Intrinsics.Common++-- | All @stdio.h@ overrides+stdioOverrides ::+  ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+  , ?memOpts :: MemOptions ) =>+  [SomeLLVMOverride p sym ext]+stdioOverrides =+  [ SomeLLVMOverride llvmPrintfOverride+  , SomeLLVMOverride llvmPrintfChkOverride+  , SomeLLVMOverride llvmPutsOverride+  , SomeLLVMOverride llvmPutCharOverride+  ]++------------------------------------------------------------------------+-- ** Declarations++llvmPrintfOverride+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym+     , ?memOpts :: MemOptions )+  => LLVMOverride p sym ext+         (EmptyCtx ::> LLVMPointerType wptr+                   ::> VectorType AnyType)+         (BVType 32)+llvmPrintfOverride =+  [llvmOvr| i32 @printf( i8*, ... ) |]+  (\memOps args -> Ctx.uncurryAssignment (callPrintf memOps) args)++llvmPrintfChkOverride+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?memOpts :: MemOptions )+  => LLVMOverride p sym ext+         (EmptyCtx ::> BVType 32+                   ::> LLVMPointerType wptr+                   ::> VectorType AnyType)+         (BVType 32)+llvmPrintfChkOverride =+  [llvmOvr| i32 @__printf_chk( i32, i8*, ... ) |]+  (\memOps args -> Ctx.uncurryAssignment (\_flg -> callPrintf memOps) args)+++llvmPutCharOverride+  :: (IsSymInterface sym, HasPtrWidth wptr)+  => LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)+llvmPutCharOverride =+  [llvmOvr| i32 @putchar( i32 ) |]+  (\memOps args -> Ctx.uncurryAssignment (callPutChar memOps) args)+++llvmPutsOverride+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?memOpts :: MemOptions )+  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) (BVType 32)+llvmPutsOverride =+  [llvmOvr| i32 @puts( i8* ) |]+  (\memOps args -> Ctx.uncurryAssignment (callPuts memOps) args)++------------------------------------------------------------------------+-- ** Implementations++callPutChar+  :: IsSymInterface sym+  => GlobalVar Mem+  -> RegEntry sym (BVType 32)+  -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))+callPutChar _mvar+ (regValue -> ch) = do+    h <- printHandle <$> getContext+    let chval = maybe '?' (toEnum . fromInteger) (BV.asUnsigned <$> asBV ch)+    liftIO $ hPutChar h chval+    return ch++callPuts+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym+     , ?memOpts :: MemOptions )+  => GlobalVar Mem+  -> RegEntry sym (LLVMPointerType wptr)+  -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))+callPuts mvar+  (regValue -> strPtr) =+    ovrWithBackend $ \bak -> do+      mem <- readGlobal mvar+      str <- liftIO $ CStr.loadString bak mem strPtr Nothing+      h <- printHandle <$> getContext+      liftIO $ hPutStrLn h (UTF8.toString str)+      -- return non-negative value on success+      liftIO $ bvLit (backendGetSym bak) knownNat (BV.one knownNat)++callPrintf+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym+     , ?memOpts :: MemOptions )+  => GlobalVar Mem+  -> RegEntry sym (LLVMPointerType wptr)+  -> RegEntry sym (VectorType AnyType)+  -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))+callPrintf mvar+  (regValue -> strPtr)+  (regValue -> valist) =+    ovrWithBackend $ \bak -> do+      mem <- readGlobal mvar+      formatStr <- liftIO $ CStr.loadString bak mem strPtr Nothing+      case parseDirectives formatStr of+        Left err -> overrideError $ AssertFailureSimError "Format string parsing failed" err+        Right ds -> do+          ((str, n), mem') <- liftIO $ runStateT (executeDirectives (printfOps bak valist) ds) mem+          writeGlobal mvar mem'+          h <- printHandle <$> getContext+          liftIO $ BS.hPutStr h str+          liftIO $ bvLit (backendGetSym bak) knownNat (BV.mkBV knownNat (toInteger n))++printfOps :: ( IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr+             , ?memOpts :: MemOptions )+          => bak+          -> V.Vector (AnyValue sym)+          -> PrintfOperations (StateT (MemImpl sym) IO)+printfOps bak valist =+  let sym = backendGetSym bak in+  PrintfOperations+  { printfUnsupported = \x -> lift $ addFailedAssertion bak+                                   $ Unsupported GHC.callStack x++  , printfGetInteger = \i sgn _len ->+     case valist V.!? (i-1) of+       Just (AnyValue (LLVMPointerRepr w) p@(LLVMPointer _blk bv)) ->+         do isBv <- liftIO (Ptr.ptrIsBv sym p)+            liftIO $ assert bak isBv $+              AssertFailureSimError+               "Passed a pointer to printf where a bitvector was expected"+               ""+            if sgn then+              return $ BV.asSigned w <$> asBV bv+            else+              return $ BV.asUnsigned <$> asBV bv+       Just (AnyValue tpr _) ->+         lift $ addFailedAssertion bak+              $ AssertFailureSimError+                "Type mismatch in printf"+                (unwords ["Expected integer, but got:", show tpr])+       Nothing ->+         lift $ addFailedAssertion bak+              $ AssertFailureSimError+               "Out-of-bounds argument access in printf"+               (unwords ["Index:", show i])++  , printfGetFloat = \i _len ->+     case valist V.!? (i-1) of+       Just (AnyValue (FloatRepr (_fi :: FloatInfoRepr fi)) x) ->+         do xr <- liftIO (iFloatToReal @_ @fi sym x)+            return (asRational xr)+       Just (AnyValue tpr _) ->+         lift $ addFailedAssertion bak+              $ AssertFailureSimError+                "Type mismatch in printf."+                (unwords ["Expected floating-point, but got:", show tpr])+       Nothing ->+         lift $ addFailedAssertion bak+              $ AssertFailureSimError+                "Out-of-bounds argument access in printf:"+                (unwords ["Index:", show i])++  , printfGetString  = \i numchars ->+     case valist V.!? (i-1) of+       Just (AnyValue PtrRepr ptr) ->+           do mem <- get+              liftIO $ CStr.loadString bak mem ptr numchars+       Just (AnyValue tpr _) ->+         lift $ addFailedAssertion bak+              $ AssertFailureSimError+                "Type mismatch in printf."+                (unwords ["Expected char*, but got:", show tpr])+       Nothing ->+         lift $ addFailedAssertion bak+              $ AssertFailureSimError+                "Out-of-bounds argument access in printf:"+                (unwords ["Index:", show i])++  , printfGetPointer = \i ->+     case valist V.!? (i-1) of+       Just (AnyValue PtrRepr ptr) ->+         return $ show (G.ppPtr ptr)+       Just (AnyValue tpr _) ->+         lift $ addFailedAssertion bak+              $ AssertFailureSimError+                "Type mismatch in printf."+                (unwords ["Expected void*, but got:", show tpr])+       Nothing ->+         lift $ addFailedAssertion bak+              $ AssertFailureSimError+                "Out-of-bounds argument access in printf:"+                (unwords ["Index:", show i])++  , printfSetInteger = \i len v ->+     case valist V.!? (i-1) of+       Just (AnyValue PtrRepr ptr) ->+         do mem <- get+            case len of+              Len_Byte  -> do+                 let w8 = knownNat :: NatRepr 8+                 let tp = G.bitvectorType 1+                 x <- liftIO (llvmPointer_bv sym =<< bvLit sym w8 (BV.mkBV w8 (toInteger v)))+                 mem' <- liftIO $ doStore bak mem ptr (LLVMPointerRepr w8) tp noAlignment x+                 put mem'+              Len_Short -> do+                 let w16 = knownNat :: NatRepr 16+                 let tp = G.bitvectorType 2+                 x <- liftIO (llvmPointer_bv sym =<< bvLit sym w16 (BV.mkBV w16 (toInteger v)))+                 mem' <- liftIO $ doStore bak mem ptr (LLVMPointerRepr w16) tp noAlignment x+                 put mem'+              Len_NoMod -> do+                 let w32  = knownNat :: NatRepr 32+                 let tp = G.bitvectorType 4+                 x <- liftIO (llvmPointer_bv sym =<< bvLit sym w32 (BV.mkBV w32 (toInteger v)))+                 mem' <- liftIO $ doStore bak mem ptr (LLVMPointerRepr w32) tp noAlignment x+                 put mem'+              Len_Long  -> do+                 let w64 = knownNat :: NatRepr 64+                 let tp = G.bitvectorType 8+                 x <- liftIO (llvmPointer_bv sym =<< bvLit sym w64 (BV.mkBV w64 (toInteger v)))+                 mem' <- liftIO $ doStore bak mem ptr (LLVMPointerRepr w64) tp noAlignment x+                 put mem'+              _ ->+                lift $ addFailedAssertion bak+                     $ Unsupported GHC.callStack+                     $ unwords ["Unsupported size modifier in %n conversion:", show len]++       Just (AnyValue tpr _) ->+         lift $ addFailedAssertion bak+              $ AssertFailureSimError+                "Type mismatch in printf."+                (unwords ["Expected void*, but got:", show tpr])++       Nothing ->+         lift $ addFailedAssertion bak+              $ AssertFailureSimError+                "Out-of-bounds argument access in printf:"+                (unwords ["Index:", show i])+  }

@@ -0,0 +1,487 @@+-- |+-- Module           : Lang.Crucible.LLVM.Intrinsics.Libc.Stdlib+-- Description      : Override definitions for C @stdlib.h@ functions+-- Copyright        : (c) Galois, Inc 2026+-- License          : BSD3+-- Maintainer       : Galois, Inc. <crux@galois.com>+-- Stability        : provisional+------------------------------------------------------------------------++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ViewPatterns #-}++module Lang.Crucible.LLVM.Intrinsics.Libc.Stdlib+  ( -- * @stdlib.h@ overrides+    stdlibOverrides+    -- * Override declarations+  , llvmMallocOverride+  , llvmCallocOverride+  , llvmFreeOverride+  , llvmReallocOverride+  , posixMemalignOverride+  , llvmAbortOverride+  , llvmExitOverride+  , llvmGetenvOverride+  , llvmAbsOverride+  , llvmLAbsOverride_32+  , llvmLAbsOverride_64+  , llvmLLAbsOverride+  , cxa_atexitOverride+    -- * Implementation functions+  , callMalloc+  , callCalloc+  , callFree+  , callRealloc+  , callPosixMemalign+  , callExit+  , callLibcAbs+  , callLLVMAbs+  , callAbs+  , CheckAbsIntMin(..)+  ) where++import           Control.Monad (when)+import           Control.Monad.IO.Class (liftIO)+import           Lens.Micro ((^.))++import qualified Data.BitVector.Sized as BV+import qualified Data.Parameterized.Context as Ctx++import           What4.Interface+import           What4.ProgramLoc (plSourceLoc)++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.Bytes (toBytes)+import           Lang.Crucible.LLVM.DataLayout+import qualified Lang.Crucible.LLVM.Errors.Poison as Poison+import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as UB+import           Lang.Crucible.LLVM.MalformedLLVMModule+import           Lang.Crucible.LLVM.MemModel+import           Lang.Crucible.LLVM.MemModel.CallStack (CallStack)+import qualified Lang.Crucible.LLVM.MemModel.Generic as G+import           Lang.Crucible.LLVM.MemModel.Partial (annotateUB)+import           Lang.Crucible.LLVM.QQ( llvmOvr )+import           Lang.Crucible.LLVM.TypeContext++import           Lang.Crucible.LLVM.Intrinsics.Common+import           Lang.Crucible.LLVM.Intrinsics.Options++-- | All @stdlib.h@ overrides+stdlibOverrides ::+  ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+  , ?lc :: TypeContext, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>+  [SomeLLVMOverride p sym ext]+stdlibOverrides =+  [ SomeLLVMOverride llvmMallocOverride+  , SomeLLVMOverride llvmCallocOverride+  , SomeLLVMOverride llvmFreeOverride+  , SomeLLVMOverride llvmReallocOverride+  , SomeLLVMOverride posixMemalignOverride+  , SomeLLVMOverride llvmAbortOverride+  , SomeLLVMOverride llvmExitOverride+  , SomeLLVMOverride llvmGetenvOverride+  , SomeLLVMOverride llvmAbsOverride+  , SomeLLVMOverride llvmLAbsOverride_32+  , SomeLLVMOverride llvmLAbsOverride_64+  , SomeLLVMOverride llvmLLAbsOverride+  , SomeLLVMOverride cxa_atexitOverride+  ]++------------------------------------------------------------------------+-- ** Declarations++------------------------------------------------------------------------+-- *** Allocation++llvmCallocOverride+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?lc :: TypeContext, ?memOpts :: MemOptions )+  => LLVMOverride p sym ext+         (EmptyCtx ::> BVType wptr ::> BVType wptr)+         (LLVMPointerType wptr)+llvmCallocOverride =+  let alignment = maxAlignment (llvmDataLayout ?lc) in+  [llvmOvr| i8* @calloc( size_t, size_t ) |]+  (\memOps args -> Ctx.uncurryAssignment (callCalloc memOps alignment) args)+++llvmReallocOverride+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?lc :: TypeContext, ?memOpts :: MemOptions )+  => LLVMOverride p sym ext+         (EmptyCtx ::> LLVMPointerType wptr ::> BVType wptr)+         (LLVMPointerType wptr)+llvmReallocOverride =+  let alignment = maxAlignment (llvmDataLayout ?lc) in+  [llvmOvr| i8* @realloc( i8*, size_t ) |]+  (\memOps args -> Ctx.uncurryAssignment (callRealloc memOps alignment) args)++llvmMallocOverride+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?lc :: TypeContext, ?memOpts :: MemOptions )+  => LLVMOverride p sym ext+         (EmptyCtx ::> BVType wptr)+         (LLVMPointerType wptr)+llvmMallocOverride =+  let alignment = maxAlignment (llvmDataLayout ?lc) in+  [llvmOvr| i8* @malloc( size_t ) |]+  (\memOps args -> Ctx.uncurryAssignment (callMalloc memOps alignment) args)++posixMemalignOverride ::+  ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+  , ?lc :: TypeContext, ?memOpts :: MemOptions ) =>+  LLVMOverride p sym ext+      (EmptyCtx ::> LLVMPointerType wptr+                ::> BVType wptr+                ::> BVType wptr)+      (BVType 32)+posixMemalignOverride =+  [llvmOvr| i32 @posix_memalign( i8**, size_t, size_t ) |]+  (\memOps args -> Ctx.uncurryAssignment (callPosixMemalign memOps) args)+++llvmFreeOverride+  :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)+  => LLVMOverride p sym ext+         (EmptyCtx ::> LLVMPointerType wptr)+         UnitType+llvmFreeOverride =+  [llvmOvr| void @free( i8* ) |]+  (\memOps args -> Ctx.uncurryAssignment (callFree memOps) args)++------------------------------------------------------------------------+-- *** Process control++llvmAbortOverride+  :: ( IsSymInterface sym+     , ?intrinsicsOpts :: IntrinsicsOptions )+  => LLVMOverride p sym ext EmptyCtx UnitType+llvmAbortOverride =+  [llvmOvr| void @abort() |]+  (\_ _args ->+     ovrWithBackend $ \bak -> liftIO $ do+       let sym = backendGetSym bak+       when (abnormalExitBehavior ?intrinsicsOpts == AlwaysFail) $+           let err = AssertFailureSimError "Call to abort" "" in+           assert bak (falsePred sym) err+       loc <- getCurrentProgramLoc sym+       abortExecBecause $ EarlyExit loc+  )++llvmExitOverride+  :: forall sym p ext+   . ( IsSymInterface sym+     , ?intrinsicsOpts :: IntrinsicsOptions )+  => LLVMOverride p sym ext+         (EmptyCtx ::> BVType 32)+         UnitType+llvmExitOverride =+  [llvmOvr| void @exit( i32 ) |]+  (\_ args -> Ctx.uncurryAssignment callExit args)++llvmGetenvOverride+  :: (IsSymInterface sym, HasPtrWidth wptr)+  => LLVMOverride p sym ext+        (EmptyCtx ::> LLVMPointerType wptr)+        (LLVMPointerType wptr)+llvmGetenvOverride =+  [llvmOvr| i8* @getenv( i8* ) |]+  (\_ _args -> do+    sym <- getSymInterface+    liftIO $ mkNullPointer sym PtrWidth)++------------------------------------------------------------------------+-- *** Integer functions++llvmAbsOverride ::+  (IsSymInterface sym, HasLLVMAnn sym) =>+  LLVMOverride p sym ext+      (EmptyCtx ::> BVType 32)+      (BVType 32)+llvmAbsOverride =+  [llvmOvr| i32 @abs( i32 ) |]+  (\mvar args ->+     do callStack <- callStackFromMemVar' mvar+        Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @32)) args)++-- @labs@ uses `long` as its argument and result type, so we need two overrides+-- for @labs@. See Note [Overrides involving (unsigned) long] in+-- Lang.Crucible.LLVM.Intrinsics.+llvmLAbsOverride_32 ::+  (IsSymInterface sym, HasLLVMAnn sym) =>+  LLVMOverride p sym ext+      (EmptyCtx ::> BVType 32)+      (BVType 32)+llvmLAbsOverride_32 =+  [llvmOvr| i32 @labs( i32 ) |]+  (\mvar args ->+     do callStack <- callStackFromMemVar' mvar+        Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @32)) args)++llvmLAbsOverride_64 ::+  (IsSymInterface sym, HasLLVMAnn sym) =>+  LLVMOverride p sym ext+      (EmptyCtx ::> BVType 64)+      (BVType 64)+llvmLAbsOverride_64 =+  [llvmOvr| i64 @labs( i64 ) |]+  (\mvar args ->+     do callStack <- callStackFromMemVar' mvar+        Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @64)) args)++llvmLLAbsOverride ::+  (IsSymInterface sym, HasLLVMAnn sym) =>+  LLVMOverride p sym ext+      (EmptyCtx ::> BVType 64)+      (BVType 64)+llvmLLAbsOverride =+  [llvmOvr| i64 @llabs( i64 ) |]+  (\mvar args ->+     do callStack <- callStackFromMemVar' mvar+        Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @64)) args)++------------------------------------------------------------------------+-- *** atexit++cxa_atexitOverride+  :: (IsSymInterface sym, HasPtrWidth wptr)+  => LLVMOverride p sym ext+        (EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr ::> LLVMPointerType wptr)+        (BVType 32)+cxa_atexitOverride =+  [llvmOvr| i32 @__cxa_atexit( void (i8*)*, i8*, i8* ) |]+  (\_ _args -> do+    sym <- getSymInterface+    liftIO $ bvZero sym knownNat)++------------------------------------------------------------------------+-- ** Implementations++------------------------------------------------------------------------+-- *** Allocation++callRealloc+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym+     , ?memOpts :: MemOptions )+  => GlobalVar Mem+  -> Alignment+  -> RegEntry sym (LLVMPointerType wptr)+  -> RegEntry sym (BVType wptr)+  -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))+callRealloc mvar alignment (regValue -> ptr) (regValue -> sz) =+  ovrWithBackend $ \bak -> do+    let sym = backendGetSym bak+    szZero  <- liftIO (notPred sym =<< bvIsNonzero sym sz)+    ptrNull <- liftIO (ptrIsNull sym PtrWidth ptr)+    loc <- liftIO (plSourceLoc <$> getCurrentProgramLoc sym)+    let displayString = "<realloc> " ++ show loc++    symbolicBranches emptyRegMap+      -- If the pointer is null, behave like malloc+      [ ( ptrNull+        , modifyGlobal mvar $ \mem -> liftIO $ doMalloc bak G.HeapAlloc G.Mutable displayString mem sz alignment+        , Nothing+        )++      -- If the size is zero, behave like malloc (of zero bytes) then free+      , (szZero+        , modifyGlobal mvar $ \mem -> liftIO $+             do (newp, mem1) <- doMalloc bak G.HeapAlloc G.Mutable displayString mem sz alignment+                mem2 <- doFree bak mem1 ptr+                return (newp, mem2)+        , Nothing+        )++      -- Otherwise, allocate a new region, memcopy `sz` bytes and free the old pointer+      , (truePred sym+        , modifyGlobal mvar $ \mem -> liftIO $+             do (newp, mem1) <- doMalloc bak G.HeapAlloc G.Mutable displayString mem sz alignment+                mem2 <- uncheckedMemcpy sym mem1 newp ptr sz+                mem3 <- doFree bak mem2 ptr+                return (newp, mem3)+        , Nothing)+      ]+++callPosixMemalign+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?lc :: TypeContext, ?memOpts :: MemOptions )+  => GlobalVar Mem+  -> RegEntry sym (LLVMPointerType wptr)+  -> RegEntry sym (BVType wptr)+  -> RegEntry sym (BVType wptr)+  -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))+callPosixMemalign mvar (regValue -> outPtr) (regValue -> align) (regValue -> sz) =+  ovrWithBackend $ \bak ->+    let sym = backendGetSym bak in+    case asBV align of+      Nothing -> fail $ unwords ["posix_memalign: alignment value must be concrete:", show (printSymExpr align)]+      Just concrete_align ->+        case toAlignment (toBytes (BV.asUnsigned concrete_align)) of+          Nothing -> fail $ unwords ["posix_memalign: invalid alignment value:", show concrete_align]+          Just a ->+            let dl = llvmDataLayout ?lc in+            modifyGlobal mvar $ \mem -> liftIO $+               do loc <- plSourceLoc <$> getCurrentProgramLoc sym+                  let displayString = "<posix_memaign> " ++ show loc+                  (p, mem') <- doMalloc bak G.HeapAlloc G.Mutable displayString mem sz a+                  mem'' <- storeRaw bak mem' outPtr (bitvectorType (dl^.ptrSize)) (dl^.ptrAlign) (ptrToPtrVal p)+                  z <- bvZero sym knownNat+                  return (z, mem'')++callMalloc+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?memOpts :: MemOptions )+  => GlobalVar Mem+  -> Alignment+  -> RegEntry sym (BVType wptr)+  -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))+callMalloc mvar alignment (regValue -> sz) =+  ovrWithBackend $ \bak ->+    modifyGlobal mvar $ \mem -> liftIO $+      do loc <- plSourceLoc <$> getCurrentProgramLoc (backendGetSym bak)+         let displayString = "<malloc> " ++ show loc+         doMalloc bak G.HeapAlloc G.Mutable displayString mem sz alignment++callCalloc+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?memOpts :: MemOptions )+  => GlobalVar Mem+  -> Alignment+  -> RegEntry sym (BVType wptr)+  -> RegEntry sym (BVType wptr)+  -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))+callCalloc mvar alignment+           (regValue -> sz)+           (regValue -> num) =+  ovrWithBackend $ \bak ->+    modifyGlobal mvar $ \mem -> liftIO $+      doCalloc bak mem sz num alignment++callFree+  :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)+  => GlobalVar Mem+  -> RegEntry sym (LLVMPointerType wptr)+  -> OverrideSim p sym ext r args ret ()+callFree mvar+           (regValue -> ptr) =+  ovrWithBackend $ \bak ->+    modifyGlobal mvar $ \mem -> liftIO $+      do mem' <- doFree bak mem ptr+         return ((), mem')++------------------------------------------------------------------------+-- *** Process control++callExit :: ( IsSymInterface sym+            , ?intrinsicsOpts :: IntrinsicsOptions )+         => RegEntry sym (BVType 32)+         -> OverrideSim p sym ext r args ret (RegValue sym UnitType)+callExit ec =+  ovrWithBackend $ \bak -> liftIO $ do+    let sym = backendGetSym bak+    when (abnormalExitBehavior ?intrinsicsOpts == AlwaysFail) $+      do cond <- bvEq sym (regValue ec) =<< bvZero sym knownNat+         -- If the argument is non-zero, throw an assertion failure. Otherwise,+         -- simply stop the current thread of execution.+         assert bak cond "Call to exit() with non-zero argument"+    loc <- getCurrentProgramLoc sym+    abortExecBecause $ EarlyExit loc++------------------------------------------------------------------------+-- *** Integer functions++-- | This determines under what circumstances @callAbs@ should check if its+-- argument is equal to the smallest signed integer of a particular size+-- (e.g., @INT_MIN@), and if it is equal to that value, what kind of error+-- should be reported.+data CheckAbsIntMin+  = LibcAbsIntMinUB+    -- ^ For the @abs@, @labs@, and @llabs@ functions, always check if the+    --   argument is equal to @INT_MIN@. If so, report it as undefined+    --   behavior per the C standard.+  | LLVMAbsIntMinPoison Bool+    -- ^ For the @llvm.abs.*@ family of LLVM intrinsics, check if the argument+    --   is equal to @INT_MIN@ only when the 'Bool' argument is 'True'. If it+    --   is 'True' and the argument is equal to @INT_MIN@, return poison.++-- | The workhorse for the @abs@, @labs@, and @llabs@ functions, as well as the+-- @llvm.abs.*@ family of overloaded intrinsics.+callAbs ::+  forall w p sym ext r args ret.+  (1 <= w, IsSymInterface sym, HasLLVMAnn sym) =>+  CallStack ->+  CheckAbsIntMin ->+  NatRepr w ->+  RegEntry sym (BVType w) ->+  OverrideSim p sym ext r args ret (RegValue sym (BVType w))+callAbs callStack checkIntMin widthRepr (regValue -> src) = do+  sym <- getSymInterface+  ovrWithBackend $ \bak -> liftIO $ do+    bvIntMin    <- bvLit sym widthRepr (BV.minSigned widthRepr)+    isNotIntMin <- notPred sym =<< bvEq sym src bvIntMin++    when shouldCheckIntMin $ do+      isNotIntMinUB <- annotateUB sym callStack ub isNotIntMin+      let err = AssertFailureSimError "Undefined behavior encountered" $+                show $ UB.explain ub+      assert bak isNotIntMinUB err++    isSrcNegative <- bvIsNeg sym src+    srcNegated    <- bvNeg sym src+    bvIte sym isSrcNegative srcNegated src+    where+      shouldCheckIntMin :: Bool+      shouldCheckIntMin =+        case checkIntMin of+          LibcAbsIntMinUB                 -> True+          LLVMAbsIntMinPoison shouldCheck -> shouldCheck++      ub :: UB.UndefinedBehavior (RegValue' sym)+      ub = case checkIntMin of+             LibcAbsIntMinUB ->+               UB.AbsIntMin $ RV src+             LLVMAbsIntMinPoison{} ->+               UB.PoisonValueCreated $ Poison.LLVMAbsIntMin $ RV src++callLibcAbs ::+  (1 <= w, IsSymInterface sym, HasLLVMAnn sym) =>+  CallStack ->+  NatRepr w ->+  RegEntry sym (BVType w) ->+  OverrideSim p sym ext r args ret (RegValue sym (BVType w))+callLibcAbs callStack = callAbs callStack LibcAbsIntMinUB++callLLVMAbs ::+  (1 <= w, IsSymInterface sym, HasLLVMAnn sym) =>+  CallStack ->+  NatRepr w ->+  RegEntry sym (BVType w) ->+  RegEntry sym (BVType 1) ->+  OverrideSim p sym ext r args ret (RegValue sym (BVType w))+callLLVMAbs callStack widthRepr src (regValue -> isIntMinPoison) = do+  shouldCheckIntMin <- liftIO $+    -- Per https://releases.llvm.org/12.0.0/docs/LangRef.html#id451, the second+    -- argument must be a constant.+    case asBV isIntMinPoison of+      Just bv -> pure (bv /= BV.zero (knownNat @1))+      Nothing -> malformedLLVMModule+                   "Call to llvm.abs.* with non-constant second argument"+                   [printSymExpr isIntMinPoison]+  callAbs callStack (LLVMAbsIntMinPoison shouldCheckIntMin) widthRepr src

@@ -0,0 +1,443 @@+-- |+-- Module           : Lang.Crucible.LLVM.Intrinsics.Libc.String+-- Description      : Override definitions for C @string.h@ functions+-- Copyright        : (c) Galois, Inc 2026+-- License          : BSD3+-- Maintainer       : Galois, Inc. <crux@galois.com>+-- Stability        : provisional+------------------------------------------------------------------------++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ViewPatterns #-}++module Lang.Crucible.LLVM.Intrinsics.Libc.String+  ( -- * @string.h@ overrides+    stringOverrides+    -- * Override declarations+  , llvmMemcpyOverride+  , llvmMemcpyChkOverride+  , llvmMemmoveOverride+  , llvmMemsetOverride+  , llvmMemsetChkOverride+  , llvmMemcmpOverride+  , llvmStrlenOverride+  , llvmStrnlenOverride+  , llvmStrcpyOverride+  , llvmStrcmpOverride+  , llvmStrncmpOverride+  , llvmStrdupOverride+  , llvmStrndupOverride+    -- * Implementation functions+  , callMemcpy+  , callMemmove+  , callMemset+  , callMemcmp+  , callStrlen+  , callStrnlen+  , callStrcpy+  , callStrcmp+  , callStrncmp+  , callStrdup+  , callStrndup+  ) where++import           Control.Monad.IO.Class (liftIO)+import qualified Data.BitVector.Sized as BV+import           Lens.Micro ((^.), _1, _2, _3)++import           Data.Parameterized.Context ( pattern (:>), pattern Empty )+import qualified Data.Parameterized.Context as Ctx++import           What4.Interface+import           What4.ProgramLoc (plSourceLoc)++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.Intrinsics.Common++-- | All @string.h@ overrides+stringOverrides ::+  ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+  , ?memOpts :: MemOptions ) =>+  [SomeLLVMOverride p sym ext]+stringOverrides =+  [ SomeLLVMOverride llvmMemcpyOverride+  , SomeLLVMOverride llvmMemcpyChkOverride+  , SomeLLVMOverride llvmMemmoveOverride+  , SomeLLVMOverride llvmMemsetOverride+  , SomeLLVMOverride llvmMemsetChkOverride+  , SomeLLVMOverride llvmMemcmpOverride+  , SomeLLVMOverride llvmStrlenOverride+  , SomeLLVMOverride llvmStrnlenOverride+  , SomeLLVMOverride llvmStrcpyOverride+  , SomeLLVMOverride llvmStrcmpOverride+  , SomeLLVMOverride llvmStrncmpOverride+  , SomeLLVMOverride llvmStrdupOverride+  , SomeLLVMOverride llvmStrndupOverride+  ]++------------------------------------------------------------------------+-- ** Declarations++llvmMemcpyOverride+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?memOpts :: MemOptions )+  => LLVMOverride p sym ext+           (EmptyCtx ::> LLVMPointerType wptr+                     ::> LLVMPointerType wptr+                     ::> BVType wptr)+           (LLVMPointerType wptr)+llvmMemcpyOverride =+  [llvmOvr| i8* @memcpy( i8*, i8*, size_t ) |]+  (\memOps args ->+       do sym <- getSymInterface+          volatile <- liftIO $ RegEntry knownRepr <$> bvZero sym knownNat+          Ctx.uncurryAssignment (callMemcpy memOps)+                                (args :> volatile)+          return $ regValue $ args^._1 -- return first argument+    )+++llvmMemcpyChkOverride+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?memOpts :: MemOptions )+  => LLVMOverride p sym ext+         (EmptyCtx ::> LLVMPointerType wptr+                   ::> LLVMPointerType wptr+                   ::> BVType wptr+                   ::> BVType wptr)+         (LLVMPointerType wptr)+llvmMemcpyChkOverride =+  [llvmOvr| i8* @__memcpy_chk ( i8*, i8*, size_t, size_t ) |]+  (\memOps args ->+      do let args' = Empty :> (args^._1) :> (args^._2) :> (args^._3)+         sym <- getSymInterface+         volatile <- liftIO $ RegEntry knownRepr <$> bvZero sym knownNat+         Ctx.uncurryAssignment (callMemcpy memOps)+                               (args' :> volatile)+         return $ regValue $ args^._1 -- return first argument+    )++llvmMemmoveOverride+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?memOpts :: MemOptions )+  => LLVMOverride p sym ext+         (EmptyCtx ::> (LLVMPointerType wptr)+                   ::> (LLVMPointerType wptr)+                   ::> BVType wptr)+         (LLVMPointerType wptr)+llvmMemmoveOverride =+  [llvmOvr| i8* @memmove( i8*, i8*, size_t ) |]+  (\memOps args ->+      do sym <- getSymInterface+         volatile <- liftIO (RegEntry knownRepr <$> bvZero sym knownNat)+         Ctx.uncurryAssignment (callMemmove memOps)+                               (args :> volatile)+         return $ regValue $ args^._1 -- return first argument+    )++llvmMemsetOverride :: forall p sym ext wptr.+     (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)+  => LLVMOverride p sym ext+         (EmptyCtx ::> LLVMPointerType wptr+                   ::> BVType 32+                   ::> BVType wptr)+         (LLVMPointerType wptr)+llvmMemsetOverride =+  [llvmOvr| i8* @memset( i8*, i32, size_t ) |]+  (\memOps args ->+      do sym <- getSymInterface+         LeqProof <- return (leqTrans @9 @16 @wptr LeqProof LeqProof)+         let dest = args^._1+         val <- liftIO (RegEntry knownRepr <$> bvTrunc sym (knownNat @8) (regValue (args^._2)))+         let len = args^._3+         volatile <- liftIO+            (RegEntry knownRepr <$> bvZero sym knownNat)+         callMemset memOps dest val len volatile+         return (regValue dest)+    )++llvmMemsetChkOverride+  :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)+  => LLVMOverride p sym ext+         (EmptyCtx ::> LLVMPointerType wptr+                 ::> BVType 32+                 ::> BVType wptr+                 ::> BVType wptr)+         (LLVMPointerType wptr)+llvmMemsetChkOverride =+  [llvmOvr| i8* @__memset_chk( i8*, i32, size_t, size_t ) |]+  (\memOps args ->+      do sym <- getSymInterface+         let dest = args^._1+         val <- liftIO+              (RegEntry knownRepr <$> bvTrunc sym knownNat (regValue (args^._2)))+         let len = args^._3+         volatile <- liftIO+            (RegEntry knownRepr <$> bvZero sym knownNat)+         callMemset memOps dest val len volatile+         return (regValue dest)+    )++llvmStrlenOverride+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?memOpts :: MemOptions )+  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) (BVType wptr)+llvmStrlenOverride =+  [llvmOvr| size_t @strlen( i8* ) |]+  (\memOps args -> Ctx.uncurryAssignment (callStrlen memOps) args)++llvmStrnlenOverride+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?memOpts :: MemOptions )+  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType wptr) (BVType wptr)+llvmStrnlenOverride =+  [llvmOvr| size_t @strnlen( i8*, size_t ) |]+  (\memOps args -> Ctx.uncurryAssignment (callStrnlen memOps) args)++llvmStrcpyOverride+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?memOpts :: MemOptions )+  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr) (LLVMPointerType wptr)+llvmStrcpyOverride =+  [llvmOvr| i8* @strcpy( i8*, i8* ) |]+  (\memOps args -> Ctx.uncurryAssignment (callStrcpy memOps) args)++llvmStrdupOverride+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?memOpts :: MemOptions )+  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) (LLVMPointerType wptr)+llvmStrdupOverride =+  [llvmOvr| i8* @strdup( i8* ) |]+  (\memOps args -> Ctx.uncurryAssignment (callStrdup memOps) args)++llvmStrndupOverride+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?memOpts :: MemOptions )+  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType wptr) (LLVMPointerType wptr)+llvmStrndupOverride =+  [llvmOvr| i8* @strndup( i8*, size_t ) |]+  (\memOps args -> Ctx.uncurryAssignment (callStrndup memOps) args)++llvmMemcmpOverride+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?memOpts :: MemOptions )+  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr ::> BVType wptr) (BVType 32)+llvmMemcmpOverride =+  [llvmOvr| i32 @memcmp( i8*, i8*, size_t ) |]+  (\memOps args -> Ctx.uncurryAssignment (callMemcmp memOps) args)++llvmStrcmpOverride+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?memOpts :: MemOptions )+  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr) (BVType 32)+llvmStrcmpOverride =+  [llvmOvr| i32 @strcmp( i8*, i8* ) |]+  (\memOps args -> Ctx.uncurryAssignment (callStrcmp memOps) args)++llvmStrncmpOverride+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?memOpts :: MemOptions )+  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr ::> BVType wptr) (BVType 32)+llvmStrncmpOverride =+  [llvmOvr| i32 @strncmp( i8*, i8*, size_t ) |]+  (\memOps args -> Ctx.uncurryAssignment (callStrncmp memOps) args)++------------------------------------------------------------------------+-- ** Implementations++------------------------------------------------------------------------+-- *** Memory manipulation++callMemcpy+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?memOpts :: MemOptions )+  => GlobalVar Mem+  -> RegEntry sym (LLVMPointerType wptr)+  -> RegEntry sym (LLVMPointerType wptr)+  -> RegEntry sym (BVType w)+  -> RegEntry sym (BVType 1)+  -> OverrideSim p sym ext r args ret ()+callMemcpy mvar+           (regValue -> dest)+           (regValue -> src)+           (RegEntry (BVRepr w) len)+           _volatile =+  ovrWithBackend $ \bak ->+    modifyGlobal mvar $ \mem -> liftIO $+      do mem' <- doMemcpy bak w mem True dest src len+         return ((), mem')++-- NB the only difference between memcpy and memove+-- is that memmove does not assert that the memory+-- ranges are disjoint.  The underlying operation+-- works correctly in both cases.+callMemmove+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?memOpts :: MemOptions )+  => GlobalVar Mem+  -> RegEntry sym (LLVMPointerType wptr)+  -> RegEntry sym (LLVMPointerType wptr)+  -> RegEntry sym (BVType w)+  -> RegEntry sym (BVType 1)+  -> OverrideSim p sym ext r args ret ()+callMemmove mvar+           (regValue -> dest)+           (regValue -> src)+           (RegEntry (BVRepr w) len)+           _volatile =+  -- FIXME? add assertions about alignment+  ovrWithBackend $ \bak ->+    modifyGlobal mvar $ \mem -> liftIO $+      do mem' <- doMemcpy bak w mem False dest src len+         return ((), mem')++callMemset+  :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)+  => GlobalVar Mem+  -> RegEntry sym (LLVMPointerType wptr)+  -> RegEntry sym (BVType 8)+  -> RegEntry sym (BVType w)+  -> RegEntry sym (BVType 1)+  -> OverrideSim p sym ext r args ret ()+callMemset mvar+           (regValue -> dest)+           (regValue -> val)+           (RegEntry (BVRepr w) len)+           _volatile =+  ovrWithBackend $ \bak ->+    modifyGlobal mvar $ \mem -> liftIO $+      do mem' <- doMemset bak w mem dest val len+         return ((), mem')++------------------------------------------------------------------------+-- *** Strings++callStrlen+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym+     , ?memOpts :: MemOptions )+  => GlobalVar Mem+  -> RegEntry sym (LLVMPointerType wptr)+  -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr))+callStrlen mvar (regValue -> strPtr) =+  ovrWithBackend $ \bak -> do+    mem <- readGlobal mvar+    liftIO $ strLen bak mem strPtr++callStrnlen+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym+     , ?memOpts :: MemOptions )+  => GlobalVar Mem+  -> RegEntry sym (LLVMPointerType wptr)+  -> RegEntry sym (BVType wptr)+  -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr))+callStrnlen mvar (regValue -> strPtr) (regValue -> bound) =+  ovrWithBackend $ \bak -> do+    mem <- readGlobal mvar+    liftIO $ CStr.strnlen bak mem strPtr bound++callStrcpy+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym+     , ?memOpts :: MemOptions )+  => GlobalVar Mem+  -> RegEntry sym (LLVMPointerType wptr)+  -> RegEntry sym (LLVMPointerType wptr)+  -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))+callStrcpy mvar (regValue -> dst) (regValue -> src) =+  ovrWithBackend $ \bak ->+    modifyGlobal mvar $ \mem -> do+      mem' <- liftIO $ CStr.copyConcretelyNullTerminatedString bak mem dst src Nothing+      pure (dst, mem')++callStrdup+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym+     , ?memOpts :: MemOptions )+  => GlobalVar Mem+  -> RegEntry sym (LLVMPointerType wptr)+  -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))+callStrdup mvar (regValue -> src) =+  ovrWithBackend $ \bak ->+    modifyGlobal mvar $ \mem -> liftIO $ do+      let sym = backendGetSym bak+      loc <- plSourceLoc <$> getCurrentProgramLoc sym+      let loc' = "<strdup> " ++ show loc+      CStr.dupConcretelyNullTerminatedString bak mem src Nothing loc' noAlignment++callStrndup+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym+     , ?memOpts :: MemOptions )+  => GlobalVar Mem+  -> RegEntry sym (LLVMPointerType wptr)+  -> RegEntry sym (BVType wptr)+  -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))+callStrndup mvar (regValue -> src) (regValue -> bound) =+  ovrWithBackend $ \bak ->+    modifyGlobal mvar $ \mem -> liftIO $ do+      let sym = backendGetSym bak+      loc <- plSourceLoc <$> getCurrentProgramLoc sym+      let loc' = "<strndup> " ++ show loc+      case BV.asUnsigned <$> asBV bound of+        Nothing -> do+          let err = AssertFailureSimError "`strndup` called with symbolic max length" ""+          addFailedAssertion bak err+        Just b ->+          let bound' = Just (fromIntegral b) in+          CStr.dupConcretelyNullTerminatedString bak mem src bound' loc' noAlignment++callMemcmp+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym+     , ?memOpts :: MemOptions )+  => GlobalVar Mem+  -> RegEntry sym (LLVMPointerType wptr)+  -> RegEntry sym (LLVMPointerType wptr)+  -> RegEntry sym (BVType wptr)+  -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))+callMemcmp mvar (regValue -> ptr1) (regValue -> ptr2) (regValue -> len) =+  ovrWithBackend $ \bak -> do+    mem <- readGlobal mvar+    liftIO $ CStr.memcmp bak mem ptr1 ptr2 len++callStrcmp+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym+     , ?memOpts :: MemOptions )+  => GlobalVar Mem+  -> RegEntry sym (LLVMPointerType wptr)+  -> RegEntry sym (LLVMPointerType wptr)+  -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))+callStrcmp mvar (regValue -> ptr1) (regValue -> ptr2) =+  ovrWithBackend $ \bak -> do+    mem <- readGlobal mvar+    liftIO $ CStr.cmpConcretelyNullTerminatedString bak mem ptr1 ptr2 Nothing++callStrncmp+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym+     , ?memOpts :: MemOptions )+  => GlobalVar Mem+  -> RegEntry sym (LLVMPointerType wptr)+  -> RegEntry sym (LLVMPointerType wptr)+  -> RegEntry sym (BVType wptr)+  -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))+callStrncmp mvar (regValue -> ptr1) (regValue -> ptr2) (regValue -> len) =+  ovrWithBackend $ \bak -> do+    mem <- readGlobal mvar+    liftIO $ CStr.strncmp bak mem ptr1 ptr2 len

@@ -35,7 +35,6 @@   ) where  import qualified ABI.Itanium as ABI-import           Control.Lens ((^.)) import           Control.Monad.Reader import           Data.List (isInfixOf) import           Data.Type.Equality ((:~:)(Refl), testEquality)@@ -49,17 +48,17 @@  import           Lang.Crucible.Backend import           Lang.Crucible.CFG.Common (GlobalVar)-import           Lang.Crucible.Simulator.OverrideSim (getSymInterface)-import           Lang.Crucible.Simulator.RegMap (RegValue, regValue)+import           Lang.Crucible.Simulator.OverrideSim (OverrideSim, getSymInterface)+import           Lang.Crucible.Simulator.RegMap (RegEntry, RegValue, regValue) import           Lang.Crucible.Panic (panic)-import           Lang.Crucible.Types (TypeRepr(UnitRepr), CtxRepr)+import           Lang.Crucible.Types (TypeRepr(UnitRepr))  import           Lang.Crucible.LLVM.Extension import           Lang.Crucible.LLVM.Intrinsics.Common+import qualified Lang.Crucible.LLVM.Intrinsics.Declare as Decl import qualified Lang.Crucible.LLVM.Intrinsics.Match as Match import           Lang.Crucible.LLVM.MemModel-import           Lang.Crucible.LLVM.Translation.Monad-import           Lang.Crucible.LLVM.Translation.Types+import           Lang.Crucible.LLVM.Translation.Monad (LLVMContext)  ------------------------------------------------------------------------ -- ** General@@ -86,7 +85,11 @@ data SomeCPPOverride p sym arch =   SomeCPPOverride   { cppOverrideSubstrings :: [String]-  , cppOverrideAction :: L.Declare -> ABI.DecodedName -> LLVMContext arch -> Maybe (SomeLLVMOverride p sym LLVM)+  , cppOverrideAction ::+      Decl.SomeDeclare ->+      ABI.DecodedName ->+      LLVMContext arch ->+      Maybe (SomeLLVMOverride p sym LLVM)   }  ------------------------------------------------------------------------@@ -96,56 +99,68 @@ -- *** Utilities  matchSymbolName :: (L.Symbol -> ABI.DecodedName -> Bool)-                -> L.Declare+                -> Decl.SomeDeclare                 -> ABI.DecodedName                 -> Maybe a                 -> Maybe a-matchSymbolName match decl decodedName =-  if not (match (L.decName decl) decodedName)+matchSymbolName match (Decl.SomeDeclare decl) decodedName =+  if not (match (Decl.decName decl) decodedName)   then const Nothing   else id -panic_ :: (Show a, Show b)-       => String-       -> L.Declare-       -> a-       -> b-       -> c-panic_ from decl args ret =+panic_ :: String -> Decl.SomeDeclare -> c+panic_ from (Decl.SomeDeclare decl) =   panic from [ "Ill-typed override"              , "Name: " ++ nm-             , "Args: " ++ show args-             , "Ret:  " ++ show ret+             , "Args: " ++ show (Decl.decArgs decl)+             , "Ret:  " ++ show (Decl.decRet decl)              ]-  where L.Symbol nm = L.decName decl+  where L.Symbol nm = Decl.decName decl  -- | If the requested declaration's symbol matches the filter, look up its -- function handle in the symbol table and use that to construct an override mkOverride :: (IsSymInterface sym, HasPtrWidth (ArchWidth arch))            => [String] -- ^ Substrings for name filtering-           -> (forall args ret. L.Declare -> CtxRepr args -> TypeRepr ret -> Maybe (SomeLLVMOverride p sym LLVM))+           -> (Decl.SomeDeclare -> Maybe (SomeLLVMOverride p sym LLVM))            -> (L.Symbol -> ABI.DecodedName -> Bool)            -> SomeCPPOverride p sym arch mkOverride substrings ov filt =-  SomeCPPOverride substrings $ \requestedDecl decodedName llvmctx ->-    let ?lc = llvmctx^.llvmTypeCtx in-    matchSymbolName filt requestedDecl decodedName $-      llvmDeclToFunHandleRepr' requestedDecl $ \argTys retTy ->-        ov requestedDecl argTys retTy+  SomeCPPOverride substrings $ \requestedDecl decodedName _llvmCtx ->+    matchSymbolName filt requestedDecl decodedName (ov requestedDecl)  ------------------------------------------------------------------------ -- *** No-op override builders +someOv ::+  L.Symbol ->+  Ctx.Assignment TypeRepr args ->+  TypeRepr ret ->+  (IsSymInterface sym =>+    GlobalVar Mem ->+    Ctx.Assignment (RegEntry sym) args ->+    forall rtp args' ret'.+    OverrideSim p sym ext rtp args' ret' (RegValue sym ret)) ->+  SomeLLVMOverride p sym ext+someOv nm argTys retTy def =+  SomeLLVMOverride (LLVMOverride (Decl.Declare nm argTys retTy) def)+ -- | Make an override for a function which doesn't return anything. voidOverride :: (IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch)              => [String]              -> (L.Symbol -> ABI.DecodedName -> Bool)              -> SomeCPPOverride p sym arch voidOverride substrings =-  mkOverride substrings $ \decl argTys retTy -> Just $-      case retTy of-        UnitRepr -> SomeLLVMOverride $ LLVMOverride decl argTys retTy $ \_mem _args -> pure ()-        _ -> panic_ "voidOverride" decl argTys retTy+  mkOverride substrings $+    \sd@(Decl.SomeDeclare+          (Decl.Declare+          { Decl.decName = nm+          , Decl.decArgs = argTys+          , Decl.decRet = retTy+          })) ->+      Just $+        case retTy of+          UnitRepr -> someOv nm argTys retTy $ \_mem _args -> pure ()+          _ -> panic_ "voidOverride" sd  -- | Make an override for a function of (LLVM) type @a -> a@, for any @a@. --@@ -155,15 +170,22 @@                  -> (L.Symbol -> ABI.DecodedName -> Bool)                  -> SomeCPPOverride p sym arch identityOverride substrings =-  mkOverride substrings $ \decl argTys retTy -> Just $-    case argTys of-      (Ctx.Empty Ctx.:> argTy)-        | Just Refl <- testEquality argTy retTy ->-            SomeLLVMOverride $ LLVMOverride decl argTys retTy $ \_mem args ->-              -- Just return the input-              pure (Ctx.uncurryAssignment regValue args)+  mkOverride substrings $+    \sd@(Decl.SomeDeclare+          (Decl.Declare+          { Decl.decName = nm+          , Decl.decArgs = argTys+          , Decl.decRet = retTy+          })) ->+      Just $+        case argTys of+          (Ctx.Empty Ctx.:> argTy)+            | Just Refl <- testEquality argTy retTy ->+                someOv nm argTys retTy $ \_mem args ->+                  -- Just return the input+                  pure (Ctx.uncurryAssignment regValue args) -      _ -> panic_ "identityOverride" decl argTys retTy+          _ -> panic_ "identityOverride" sd  -- | Make an override for a function of (LLVM) type @a -> b -> a@, for any @a@. --@@ -173,14 +195,21 @@               -> (L.Symbol -> ABI.DecodedName -> Bool)               -> SomeCPPOverride p sym arch constOverride substrings =-  mkOverride substrings $ \decl argTys retTy -> Just $-    case argTys of-      (Ctx.Empty Ctx.:> fstTy Ctx.:> _)-        | Just Refl <- testEquality fstTy retTy ->-        SomeLLVMOverride $ LLVMOverride decl argTys retTy $ \_mem args ->-          pure (Ctx.uncurryAssignment (const . regValue) args)+  mkOverride substrings $+    \sd@(Decl.SomeDeclare+          (Decl.Declare+          { Decl.decName = nm+          , Decl.decArgs = argTys+          , Decl.decRet = retTy+          })) ->+      Just $+        case argTys of+          (Ctx.Empty Ctx.:> fstTy Ctx.:> _)+            | Just Refl <- testEquality fstTy retTy ->+            someOv nm argTys retTy $ \_mem args ->+              pure (Ctx.uncurryAssignment (const . regValue) args) -      _ -> panic_ "constOverride" decl argTys retTy+          _ -> panic_ "constOverride" sd  -- | Make an override that always returns the same value. fixedOverride :: (IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch)@@ -190,14 +219,21 @@               -> (L.Symbol -> ABI.DecodedName -> Bool)               -> SomeCPPOverride p sym arch fixedOverride ty regval substrings =-  mkOverride substrings $ \decl argTys retTy -> Just $-    case testEquality retTy ty of-      Just Refl ->-        SomeLLVMOverride $ LLVMOverride decl argTys retTy $ \mem _args -> do-          sym <- getSymInterface-          liftIO (regval mem sym)+  mkOverride substrings $+    \sd@(Decl.SomeDeclare+          (Decl.Declare+          { Decl.decName = nm+          , Decl.decArgs = argTys+          , Decl.decRet = retTy+          })) ->+      Just $+        case testEquality retTy ty of+          Just Refl ->+            someOv nm argTys retTy $ \mem _args -> do+              sym <- getSymInterface+              liftIO (regval mem sym) -      _ -> panic_ "fixedOverride" decl argTys retTy+          _ -> panic_ "fixedOverride" sd  -- | Return @true@. trueOverride :: (IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch)

@@ -197,7 +197,6 @@  import           Prelude hiding (seq) -import           Control.Lens hiding (Empty, (:>)) import           Control.Monad import           Control.Monad.IO.Class import           Control.Monad.Trans (lift)@@ -209,6 +208,8 @@ import           Data.Text (Text) import           Data.Word import qualified GHC.Stack as GHC+import           Lens.Micro ((^.), _2, to, folded)+import           Lens.Micro.Mtl (use, (%=)) import           Numeric.Natural (Natural) import qualified Prettyprinter as PP import           System.IO (Handle, hPutStrLn)@@ -480,7 +481,10 @@            Left lookupErr -> lift $              do p <- Partial.annotateME sym mop (BadFunctionPointer lookupErr) (falsePred sym)                 loc <- getCurrentProgramLoc sym-                let err = SimError loc (AssertFailureSimError "Failed to load function handle" (show (ME.ppFuncLookupError lookupErr)))+                let estr = "Failed to load function handle: "+                           <> fromMaybe "<unidentified>" gsym+                let err = SimError loc (AssertFailureSimError estr+                                        (show (ME.ppFuncLookupError lookupErr)))                 addProofObligation bak (LabeledPred p err)                 abortExecBecause (AssertionFailure err) 

@@ -49,13 +49,14 @@   ) where  import Control.Exception (assert)-import Control.Lens import Control.Monad (guard) import Data.Map (Map) import qualified Data.Map as Map import Data.Maybe import Data.Vector (Vector) import qualified Data.Vector as V+import Lens.Micro ((^.))+import Lens.Micro.Extras (view) import Numeric.Natural  import Lang.Crucible.Panic ( panic )@@ -454,9 +455,9 @@ loadBitvector lo lw so v = do   let le = lo + lw   let ltp = bitvectorType lw-  let stp = fromMaybe (error ("loadBitvector given bad view " ++ show v)) (viewType v)+  let stp = fromMaybe (panic "loadBitvector" ["given bad view", show v]) (viewType v)   let retValue eo v' = (sz', valueLoad lo' (bitvectorType sz') eo v')-        where etp = fromMaybe (error ("Bad view " ++ show v')) (viewType v')+        where etp = fromMaybe (panic "loadBitvector.retValue" ["bad view", show v']) (viewType v')               esz = storageTypeSize etp               lo' = max lo eo               sz' = min le (eo+esz) - lo'@@ -535,7 +536,7 @@       Struct lflds ->         let val f = (f, valueLoad (lo+fieldOffset f) (f^.fieldVal) so v)          in MkStruct (val <$> lflds)- where stp = fromMaybe (error ("Coerce value given bad view " ++ show v)) (viewType v)+ where stp = fromMaybe (panic "coerceValue" ["given bad view", show v]) (viewType v)        le = typeEnd lo ltp        se = so + storageTypeSize stp        nonZeroLoad = le - lo > 0

@@ -77,10 +77,10 @@ import           Prelude hiding (pred)  import qualified Control.Exception as X-import           Control.Lens import           Control.Monad import           Control.Monad.State.Strict import           Control.Monad.Trans.Maybe+import           Data.Function ((&)) import           Data.IORef import           Data.Maybe import qualified Data.List as List@@ -89,6 +89,7 @@ import qualified Data.IntMap as IntMap import           Data.Monoid import           Data.Text (Text)+import           Lens.Micro ((^.), (.~), (%~)) import           Numeric.Natural import           Prettyprinter import           Lang.Crucible.Panic (panic)@@ -1578,7 +1579,7 @@           BranchFrame (sizeMemAllocs (fst c)) wc c $ popf s           where c = (popMemAllocs a, w) -        popf EmptyMem{} = error "popStackFrameMem given unexpected memory"+        popf EmptyMem{} = panic "popStackFrameMem" ["given unexpected memory"]   -- | Free a heap-allocated block of memory.@@ -1625,7 +1626,7 @@ branchAbortMem :: Mem sym -> Mem sym branchAbortMem = memState %~ popf   where popf (BranchFrame _ _ c s) = s & memStateAddChanges c-        popf _ = error "branchAbortMem given unexpected memory"+        popf _ = panic "branchAbortMem" ["given unexpected memory"]  -- | Merge memory that was previously prepared via 'branchMem'. --@@ -1644,7 +1645,7 @@       X.assert (allocsEq && writesEq) $         let s' = s & memStateAddChanges (muxChanges c a b)         in x & memState .~ s'-    _ -> error "mergeMem given unexpected memories"+    _ -> panic "mergeMem" ["given unexpected memories"]  -------------------------------------------------------------------------------- -- Finding allocations

@@ -79,10 +79,10 @@   ) where  import           Control.Applicative ((<|>))-import           Control.Lens import           Control.Monad.State import           Control.Monad.Trans.Maybe import           Data.Foldable+import           Data.Function ((&)) import           Data.IntMap (IntMap) import qualified Data.IntMap as IntMap import qualified Data.List.Extra as List@@ -92,6 +92,7 @@ import           Data.Set (Set) import qualified Data.Set as Set import           Data.Text (Text)+import           Lens.Micro (Lens', lens, (^.), (.~)) import           Numeric.Natural import           Prettyprinter 

@@ -67,7 +67,6 @@  import           Prelude hiding (pred) -import           Control.Lens ((^.), view) import           Control.Monad.IO.Class (MonadIO(..)) import           Control.Monad.Except (ExceptT, MonadError(..), runExceptT) import           Control.Monad.State.Strict (StateT, get, put, runStateT)@@ -78,6 +77,8 @@ import qualified Data.Map as Map import           Data.Vector (Vector) import qualified Data.Vector as V+import           Lens.Micro ((^.))+import           Lens.Micro.Extras (view) import           Numeric.Natural  import qualified Data.BitVector.Sized as BV@@ -129,13 +130,14 @@   x <> NoExplanation = x   DisjOfFailures xs <> DisjOfFailures ys = DisjOfFailures (xs ++ ys) -explainCex :: forall t st fs sym.-  (IsSymInterface sym, sym ~ ExprBuilder t st fs) =>+explainCex :: forall t st fm sym.+  (IsSymInterface sym, sym ~ ExprBuilder t st (Flags fm)) =>   sym ->+  FloatModeRepr fm ->   LLVMAnnMap sym ->   Maybe (GroundEvalFn t) ->   IO (Pred sym -> IO (CexExplanation sym BaseBoolType))-explainCex sym bbMap evalFn =+explainCex sym fm bbMap evalFn =   do posCache <- newIdxCache      negCache <- newIdxCache      pure (evalPos posCache negCache)@@ -154,7 +156,7 @@           Nothing -> evalPos posCache negCache e'           Just (callStack, bb) ->             do bb' <- case evalFn of-                        Just f  -> concBadBehavior sym (groundEval f) bb+                        Just f  -> concBadBehavior sym fm (groundEval f) bb                         Nothing -> pure bb                pure (DisjOfFailures [ (callStack, bb') ]) 

@@ -104,7 +104,6 @@  import qualified What4.Expr.GroundEval as W4GE import           What4.Interface-import           What4.InterpretedFloatingPoint import           What4.Expr (GroundValue)  import           Lang.Crucible.Backend@@ -293,21 +292,6 @@   do b   <- natIte sym p b1 b2      off <- bvIte sym p off1 off2      return $ LLVMPointer b off--data FloatSize (fi :: FloatInfo) where-  SingleSize :: FloatSize SingleFloat-  DoubleSize :: FloatSize DoubleFloat--deriving instance Eq (FloatSize fi)--deriving instance Ord (FloatSize fi)--deriving instance Show (FloatSize fi)--instance TestEquality FloatSize where-  testEquality SingleSize SingleSize = Just Refl-  testEquality DoubleSize DoubleSize = Just Refl-  testEquality _ _ = Nothing  -- | Generate a concrete offset value from an @Addr@ value. constOffset :: (1 <= w, IsExprBuilder sym) => sym -> NatRepr w -> G.Addr -> IO (SymBV sym w)

@@ -7,6 +7,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE LambdaCase #-}+{-# LANGUAGE NegativeLiterals #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-}@@ -35,6 +36,15 @@   , dupConcreteString   , dupConcretelyNullTerminatedString   , dupProvablyNullTerminatedString+  -- * Memory comparison+  , memcmp+  , memcmpConcreteLen+  -- * String comparison+  , strncmp+  , strncmpConcreteLen+  , cmpConcreteString+  , cmpConcretelyNullTerminatedString+  , cmpProvablyNullTerminatedString   -- * Low-level string loading primitives   -- ** 'ByteChecker'   , ControlFlow(..)@@ -51,16 +61,36 @@   -- ** 'ByteLoader'   , ByteLoader(..)   , llvmByteLoader-  -- ** 'loadBytes'+  -- * 'loadBytes'   , loadBytes+  -- * Loading and checking two byte streams+  -- ** 'BytesLoader'+  , BytesLoader(..)+  , llvmBytesLoader+  , llvmStringsLoader+  -- ** 'BytesChecker'+  , BytesChecker(..)+  , withMaxBytes+  -- ** 'loadTwoBytes'+  , loadTwoBytes+  -- ** 'BytesChecker's for string comparison+  , fullyConcreteNullTerminatedStrings+  , concretelyNullTerminatedStrings+  , provablyNullTerminatedStrings+  , lengthBoundedStringComparison+  , lengthBoundedProvablyNullTerminatedStringComparison+  -- ** 'BytesChecker's for length-bounded comparison+  , simpleByteComparison+  , lengthBoundedByteComparison   ) where -import           Control.Lens ((^.), to) import           Data.Bifunctor (Bifunctor(bimap))+ import           Control.Monad.IO.Class (MonadIO, liftIO) import qualified Control.Monad.State.Strict as State import qualified Data.BitVector.Sized as BV import           Data.Functor ((<&>))+import           Lens.Micro ((^.), to) import qualified Data.Parameterized.NatRepr as DPN import           Data.Word (Word8) import qualified Data.Vector as Vec@@ -548,6 +578,221 @@   dupFromLoadedBytes bak mem (Vec.fromList bytes) displayString alignment  ---------------------------------------------------------------------+-- * String comparison++-- | Compare two concrete strings.+--+-- Uses 'fullyConcreteNullTerminatedStrings' checker. Both strings must be+-- fully concrete (no symbolic bytes).+--+-- Returns:+-- * 0 if the strings are equal+-- * A negative value if the first differing byte in s1 is less than in s2+-- * A positive value if the first differing byte in s1 is greater than in s2+cmpConcreteString ::+  forall sym bak wptr.+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Partial.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  ) =>+  bak ->+  Mem.MemImpl sym ->+  Mem.LLVMPtr sym wptr ->+  Mem.LLVMPtr sym wptr ->+  IO (WI.SymBV sym 32)+cmpConcreteString bak mem ptr1 ptr2 = do+  let sym = LCB.backendGetSym bak+  zero <- WI.bvZero sym (DPN.knownNat @32)+  loadTwoBytes bak mem zero ptr1 ptr2 (llvmStringsLoader mem) fullyConcreteNullTerminatedStrings++-- | Compare two strings with concrete null terminators.+--+-- Uses 'concretelyNullTerminatedStrings' checker. The strings must have+-- concrete null terminators, but may contain symbolic bytes before the terminator.+--+-- If a maximum length is provided, comparison stops at that length even if+-- no null terminator is encountered.+--+-- Returns:+-- * 0 if the strings are equal+-- * A negative value if the first differing byte in s1 is less than in s2+-- * A positive value if the first differing byte in s1 is greater than in s2+cmpConcretelyNullTerminatedString ::+  forall sym bak wptr.+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Partial.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  ) =>+  bak ->+  Mem.MemImpl sym ->+  Mem.LLVMPtr sym wptr ->+  Mem.LLVMPtr sym wptr ->+  -- | Maximum number of characters to compare+  Maybe Int ->+  IO (WI.SymBV sym 32)+cmpConcretelyNullTerminatedString bak mem ptr1 ptr2 maxLen = do+  let sym = LCB.backendGetSym bak+  zero <- WI.bvZero sym (DPN.knownNat @32)+  case maxLen of+    Nothing ->+      loadTwoBytes bak mem zero ptr1 ptr2 (llvmStringsLoader mem) concretelyNullTerminatedStrings+    Just 0 ->+      WI.bvZero sym (DPN.knownNat @32)+    Just n ->+      loadTwoBytes bak mem (zero, 0) ptr1 ptr2 (llvmStringsLoader mem) (lengthBoundedStringComparison (fromIntegral n))++-- | Compare two strings with provably null terminators.+--+-- Uses 'provablyNullTerminatedStrings' checker. Consults an SMT solver to+-- check if bytes are provably null terminators.+--+-- If a maximum length is provided, comparison stops at that length even if+-- no null terminator is encountered.+--+-- Returns:+-- * 0 if the strings are equal+-- * A negative value if the first differing byte in s1 is less than in s2+-- * A positive value if the first differing byte in s1 is greater than in s2+cmpProvablyNullTerminatedString ::+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Partial.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  , sym ~ WEB.ExprBuilder scope st fs+  , bak ~ LCBO.OnlineBackend solver scope st fs+  , WPO.OnlineSolver solver+  ) =>+  bak ->+  Mem.MemImpl sym ->+  Mem.LLVMPtr sym wptr ->+  Mem.LLVMPtr sym wptr ->+  -- | Maximum number of characters to compare+  Maybe Int ->+  IO (WI.SymBV sym 32)+cmpProvablyNullTerminatedString bak mem ptr1 ptr2 maxLen = do+  let sym = LCB.backendGetSym bak+  zero <- WI.bvZero sym (DPN.knownNat @32)+  case maxLen of+    Nothing ->+      loadTwoBytes bak mem zero ptr1 ptr2 (llvmStringsLoader mem) provablyNullTerminatedStrings+    Just 0 ->+      WI.bvZero sym (DPN.knownNat @32)+    Just n ->+      loadTwoBytes bak mem (zero, 0) ptr1 ptr2 (llvmStringsLoader mem) (lengthBoundedProvablyNullTerminatedStringComparison (fromIntegral n))++-- | @strncmp@ - compare two null-terminated strings up to n characters.+--+-- See 'strncmpConcreteLen' for the return value.+--+-- Asserts that the length is concrete (non-symbolic).+strncmp ::+  forall sym bak wptr.+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Partial.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  ) =>+  bak ->+  Mem.MemImpl sym ->+  Mem.LLVMPtr sym wptr ->+  Mem.LLVMPtr sym wptr ->+  WI.SymBV sym wptr ->+  IO (WI.SymBV sym 32)+strncmp bak mem ptr1 ptr2 len =+  case BV.asUnsigned <$> WI.asBV len of+    Just n -> strncmpConcreteLen bak mem ptr1 ptr2 (fromIntegral n)+    Nothing -> do+      let err = LCS.AssertFailureSimError "`strncmp` called with symbolic length" ""+      LCB.addFailedAssertion bak err++-- | Compare two null-terminated strings up to n characters with a concrete length.+--+-- Returns:+-- * 0 if the strings are equal (up to n characters or null terminator)+-- * A negative value if the first differing byte in s1 is less than in s2+-- * A positive value if the first differing byte in s1 is greater than in s2+--+-- Requires that both strings have concrete null terminators.+strncmpConcreteLen ::+  forall sym bak wptr.+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Partial.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  ) =>+  bak ->+  Mem.MemImpl sym ->+  Mem.LLVMPtr sym wptr ->+  Mem.LLVMPtr sym wptr ->+  Integer ->+  IO (WI.SymBV sym 32)+strncmpConcreteLen bak mem ptr1 ptr2 n =+  cmpConcretelyNullTerminatedString bak mem ptr1 ptr2 (Just (fromIntegral n))++---------------------------------------------------------------------+-- * Memory comparison++-- | @memcmp@.+--+-- See 'memcmpConcreteLen' for the return value.+--+-- Asserts that the length is concrete (non-symbolic).+memcmp ::+  forall sym bak wptr.+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Partial.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  ) =>+  bak ->+  Mem.MemImpl sym ->+  Mem.LLVMPtr sym wptr ->+  Mem.LLVMPtr sym wptr ->+  WI.SymBV sym wptr ->+  IO (WI.SymBV sym 32)+memcmp bak mem ptr1 ptr2 len =+  case BV.asUnsigned <$> WI.asBV len of+    Just n -> memcmpConcreteLen bak mem ptr1 ptr2 (fromIntegral n)+    Nothing -> do+      let err = LCS.AssertFailureSimError "`memcmp` called with symbolic length" ""+      LCB.addFailedAssertion bak err++-- | Compare two memory regions byte-by-byte with a concrete length.+--+-- Returns:+-- * 0 if the regions are equal+-- * A negative value if the first differing byte in s1 is less than in s2+-- * A positive value if the first differing byte in s1 is greater than in s2+memcmpConcreteLen ::+  forall sym bak wptr.+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Partial.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  ) =>+  bak ->+  Mem.MemImpl sym ->+  Mem.LLVMPtr sym wptr ->+  Mem.LLVMPtr sym wptr ->+  Integer ->+  IO (WI.SymBV sym 32)+memcmpConcreteLen bak mem ptr1 ptr2 n+  | n == 0 = do+      let sym = LCB.backendGetSym bak+      WI.bvZero sym (DPN.knownNat @32)+  | otherwise =+      loadTwoBytes bak mem ((), 0) ptr1 ptr2 (llvmBytesLoader mem) (lengthBoundedByteComparison n)++--------------------------------------------------------------------- -- * Low-level string loading primitives  ---------------------------------------------------------------------@@ -863,4 +1108,379 @@           liftIO (LCB.addAssumption bak assump)            ptr' <- liftIO (Mem.doPtrAddOffset bak mem ptr =<< WI.bvOne sym Mem.PtrWidth)-          go acc' ptr' loader checker +          go acc' ptr' loader checker++---------------------------------------------------------------------+-- * Loading and checking two byte streams++-- ** 'BytesLoader'++-- | Load a byte from each of two memory locations.+--+-- The loader can optionally add assumptions after loading bytes when iteration+-- continues. This is used for null-terminated string operations where we need+-- to assume loaded bytes are non-null.+--+-- Like 'ByteLoader', but for two bytes (usually from different strings) at+-- once.+data BytesLoader m sym bak wptr+  = BytesLoader+      { runBytesLoader :: bak -> Mem.LLVMPtr sym wptr -> Mem.LLVMPtr sym wptr -> m (Mem.LLVMPtr sym 8, Mem.LLVMPtr sym 8)+      -- | Called when the 'BytesChecker' returns 'Continue', allowing the+      -- loader to add assumptions about the loaded bytes (e.g., that they are+      -- non-null).+      , onContinue :: bak -> Mem.LLVMPtr sym 8 -> Mem.LLVMPtr sym 8 -> m ()+      }++-- | A 'BytesLoader' for LLVM memory based on 'Mem.doLoad'.+--+-- This version does not add any assumptions about loaded bytes.+-- Use this for length-bounded operations like @memcmp@ that need to handle+-- null bytes in the middle of the data.+llvmBytesLoader ::+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Mem.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  , MonadIO m+  ) =>+  Mem.MemImpl sym ->+  BytesLoader m sym bak wptr+llvmBytesLoader mem =+  BytesLoader+    { runBytesLoader = \bak ptr1 ptr2 -> do+        let i1 = Mem.bitvectorType 1+        let p8 = Mem.LLVMPointerRepr (DPN.knownNat @8)+        byte1 <- liftIO (Mem.doLoad bak mem ptr1 i1 p8 CLD.noAlignment)+        byte2 <- liftIO (Mem.doLoad bak mem ptr2 i1 p8 CLD.noAlignment)+        pure (byte1, byte2)+    , onContinue = \_ _ _ -> pure ()+    }++-- | A 'BytesLoader' for LLVM memory that adds non-null assumptions.+--+-- This version adds assumptions that loaded bytes are non-null when iteration+-- continues. Use this for null-terminated string operations like @strcmp@.+llvmStringsLoader ::+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Mem.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  , MonadIO m+  ) =>+  Mem.MemImpl sym ->+  BytesLoader m sym bak wptr+llvmStringsLoader mem =+  BytesLoader+    { runBytesLoader = \bak ptr1 ptr2 -> do+        let i1 = Mem.bitvectorType 1+        let p8 = Mem.LLVMPointerRepr (DPN.knownNat @8)+        byte1 <- liftIO (Mem.doLoad bak mem ptr1 i1 p8 CLD.noAlignment)+        byte2 <- liftIO (Mem.doLoad bak mem ptr2 i1 p8 CLD.noAlignment)+        pure (byte1, byte2)+    , onContinue = \bak byte1 byte2 -> liftIO $ do+        let sym = LCB.backendGetSym bak+        -- Add assumptions that both bytes were nonzero+        prevByte1WasNonNull <- WI.notPred sym =<< Mem.ptrIsNull sym (WI.knownNat @8) byte1+        prevByte2WasNonNull <- WI.notPred sym =<< Mem.ptrIsNull sym (WI.knownNat @8) byte2+        loc <- WI.getCurrentProgramLoc sym+        let assump1 = LCB.BranchCondition loc Nothing prevByte1WasNonNull+        let assump2 = LCB.BranchCondition loc Nothing prevByte2WasNonNull+        LCB.addAssumption bak assump1+        LCB.addAssumption bak assump2+    }++---------------------------------------------------------------------+-- ** 'BytesChecker'++-- | Compute a result from two symbolic bytes, and check if loading should+-- continue to the next pair of bytes.+--+-- Used to compare two byte streams simultaneously, e.g., for 'strcmp'.+--+-- Like 'ByteChecker', but for two bytes (usually from different strings) at+-- once.+newtype BytesChecker m sym bak a b+  = BytesChecker+      { runBytesChecker :: bak -> a -> Mem.LLVMPtr sym 8 -> Mem.LLVMPtr sym 8 -> m (ControlFlow a b) }++-- | 'BytesChecker' for adding a maximum byte length.+withMaxBytes ::+  MonadIO m =>+  GHC.HasCallStack =>+  LCB.IsSymBackend sym bak =>+  Functor m =>+  -- | Maximum number of bytes to compare+  Integer ->+  -- | What to do when the maximum is reached+  (bak -> a -> m b) ->+  BytesChecker m sym bak a b ->+  BytesChecker m sym bak (a, Integer) b+withMaxBytes limit done checker =+  BytesChecker $ \bak (acc, i) byte1Ptr byte2Ptr ->+    runBytesChecker checker bak acc byte1Ptr byte2Ptr >>=+      \case+        Break r -> pure (Break r)+        Continue r ->+          if i + 1 >= limit+          then Break <$> done bak r+          else pure (Continue (r, i + 1))++-- ** 'loadTwoBytes'++-- | Load sequences of bytes from two pointers simultaneously.+--+-- Used to implement 'strcmp'. Similar to 'loadBytes' but operates on two byte streams.+loadTwoBytes ::+  forall m a b sym bak wptr.+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Mem.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  , MonadIO m+  ) =>+  bak ->+  Mem.MemImpl sym ->+  -- | Initial accumulator+  a ->+  -- | First pointer to load from+  Mem.LLVMPtr sym wptr ->+  -- | Second pointer to load from+  Mem.LLVMPtr sym wptr ->+  -- | How to load a byte from each memory location+  BytesLoader m sym bak wptr ->+  -- | How to check if we should continue loading the next bytes+  BytesChecker m sym bak a b ->+  m b+loadTwoBytes bak mem = go+ where+  sym = LCB.backendGetSym bak+  go ::+    a ->+    Mem.LLVMPtr sym wptr ->+    Mem.LLVMPtr sym wptr ->+    BytesLoader m sym bak wptr ->+    BytesChecker m sym bak a b ->+    m b+  go acc ptr1 ptr2 loader checker = do+    (byte1, byte2) <- runBytesLoader loader bak ptr1 ptr2+    runBytesChecker checker bak acc byte1 byte2 >>=+      \case+        Break result -> pure result+        Continue acc' -> do+          -- Let the loader add any assumptions it needs (e.g., non-null for strcmp)+          onContinue loader bak byte1 byte2++          ptr1' <- liftIO (Mem.doPtrAddOffset bak mem ptr1 =<< WI.bvOne sym Mem.PtrWidth)+          ptr2' <- liftIO (Mem.doPtrAddOffset bak mem ptr2 =<< WI.bvOne sym Mem.PtrWidth)+          go acc' ptr1' ptr2' loader checker++---------------------------------------------------------------------+-- ** BytesCheckers for string comparison++-- Helper, not exported+-- Common logic for comparing two bytes after null-terminator checking.+-- Returns Nothing if bytes are equal (should continue), or Just result if different.+compareBytesForStrings ::+  MonadIO m =>+  LCB.IsSymBackend sym bak =>+  bak ->+  WI.SymBV sym 8 ->+  WI.SymBV sym 8 ->+  m (Maybe (WI.SymBV sym 32))+compareBytesForStrings bak byte1 byte2 = do+  let sym = LCB.backendGetSym bak+  let i32 = DPN.knownNat @32+  eq <- liftIO (WI.bvEq sym byte1 byte2)+  case WI.asConstantPred eq of+    Just False -> do+      lt <- liftIO (WI.bvUlt sym byte1 byte2)+      negOne <- liftIO (WI.bvLit sym i32 (BV.mkBV i32 -1))+      one <- liftIO (WI.bvOne sym i32)+      result <- liftIO (WI.bvIte sym lt negOne one)+      pure (Just result)+    _ -> pure Nothing++-- Helper, not exported+-- Common logic for handling null terminator cases in string comparison.+-- Returns Nothing if bytes are equal (should continue), or Just result if different or at null terminator.+handleNullTerminators ::+  MonadIO m =>+  LCB.IsSymBackend sym bak =>+  bak ->+  WI.SymBV sym 32 ->+  Bool ->+  Bool ->+  WI.SymBV sym 8 ->+  WI.SymBV sym 8 ->+  m (Maybe (WI.SymBV sym 32))+handleNullTerminators bak bothNullResult isNull1 isNull2 byte1 byte2 = do+  let sym = LCB.backendGetSym bak+  let i32 = DPN.knownNat @32+  case (isNull1, isNull2) of+    (True, True) -> pure (Just bothNullResult)+    (True, False) -> do+      negOne <- liftIO (WI.bvLit sym i32 (BV.mkBV i32 -1))+      pure (Just negOne)+    (False, True) -> do+      one <- liftIO (WI.bvOne sym i32)+      pure (Just one)+    (False, False) -> compareBytesForStrings bak byte1 byte2++-- | 'BytesChecker' for comparing concrete strings.+--+-- Stops when either string has a concrete null terminator.+fullyConcreteNullTerminatedStrings ::+  MonadIO m =>+  GHC.HasCallStack =>+  LCB.IsSymBackend sym bak =>+  BytesChecker m sym bak (WI.SymBV sym 32) (WI.SymBV sym 32)+fullyConcreteNullTerminatedStrings =+  BytesChecker $ \bak acc byte1Ptr byte2Ptr -> do+    byte1 <- liftIO (ptrToBv8 bak byte1Ptr)+    byte2 <- liftIO (ptrToBv8 bak byte2Ptr)+    let sym = LCB.backendGetSym bak+    let i32 = DPN.knownNat @32++    case (BV.asUnsigned <$> WI.asBV byte1, BV.asUnsigned <$> WI.asBV byte2) of+      (Just 0, Just 0) -> pure (Break acc)+      (Just 0, Just _) -> do+        negOne <- liftIO (WI.bvLit sym i32 (BV.mkBV i32 -1))+        pure (Break negOne)+      (Just _, Just 0) -> do+        one <- liftIO (WI.bvOne sym i32)+        pure (Break one)+      (Just c1, Just c2) | c1 == c2 -> pure (Continue acc)+      (Just c1, Just c2) -> do+        if c1 < c2+          then do+            negOne <- liftIO (WI.bvLit sym i32 (BV.mkBV i32 -1))+            pure (Break negOne)+          else do+            one <- liftIO (WI.bvOne sym i32)+            pure (Break one)+      _ -> do+        let msg = "Symbolic value encountered when comparing strings"+        liftIO (LCB.addFailedAssertion bak (LCS.Unsupported GHC.callStack msg))++-- | 'BytesChecker' for comparing strings with concrete null terminators.+--+-- Stops when either string has a concrete null terminator.+concretelyNullTerminatedStrings ::+  MonadIO m =>+  GHC.HasCallStack =>+  LCB.IsSymBackend sym bak =>+  BytesChecker m sym bak (WI.SymBV sym 32) (WI.SymBV sym 32)+concretelyNullTerminatedStrings =+  BytesChecker $ \bak acc byte1Ptr byte2Ptr -> do+    byte1 <- liftIO (ptrToBv8 bak byte1Ptr)+    byte2 <- liftIO (ptrToBv8 bak byte2Ptr)++    let isNull1 = (BV.asUnsigned <$> WI.asBV byte1) == Just 0+    let isNull2 = (BV.asUnsigned <$> WI.asBV byte2) == Just 0++    handleNullTerminators bak acc isNull1 isNull2 byte1 byte2 >>= \case+      Just result -> pure (Break result)+      Nothing -> pure (Continue acc)++-- | 'BytesChecker' for comparing strings with provably null terminators.+--+-- Stops when either string is provably null-terminated.+provablyNullTerminatedStrings ::+  MonadIO m =>+  GHC.HasCallStack =>+  LCB.IsSymBackend sym bak =>+  sym ~ WEB.ExprBuilder scope st fs =>+  bak ~ LCBO.OnlineBackend solver scope st fs =>+  WPO.OnlineSolver solver =>+  BytesChecker m sym bak (WI.SymBV sym 32) (WI.SymBV sym 32)+provablyNullTerminatedStrings =+  BytesChecker $ \bak acc byte1Ptr byte2Ptr -> liftIO $ do+    byte1 <- ptrToBv8 bak byte1Ptr+    byte2 <- ptrToBv8 bak byte2Ptr+    let sym = LCB.backendGetSym bak++    isNull1 <- isProvablyNullTerminator bak sym byte1+    isNull2 <- isProvablyNullTerminator bak sym byte2++    handleNullTerminators bak acc isNull1 isNull2 byte1 byte2 >>= \case+      Just result -> pure (Break result)+      Nothing -> pure (Continue acc)++-- | 'BytesChecker' for comparing strings with concrete null terminators+-- up to a maximum length.+--+-- Combines null-terminator checking (like strcmp) with length bounding+-- (like memcmp). Used for strncmp.+--+-- The accumulator is a pair of the comparison result so far and the current index.+lengthBoundedStringComparison ::+  MonadIO m =>+  GHC.HasCallStack =>+  LCB.IsSymBackend sym bak =>+  Integer ->+  BytesChecker m sym bak (WI.SymBV sym 32, Integer) (WI.SymBV sym 32)+lengthBoundedStringComparison maxLen =+  let onMaxBytes _bak zero = pure zero+  in withMaxBytes maxLen onMaxBytes concretelyNullTerminatedStrings++-- | 'BytesChecker' for comparing strings with provably null terminators+-- up to a maximum length.+--+-- Combines provably null-terminator checking with length bounding.+--+-- The accumulator is a pair of the comparison result so far and the current index.+lengthBoundedProvablyNullTerminatedStringComparison ::+  MonadIO m =>+  GHC.HasCallStack =>+  LCB.IsSymBackend sym bak =>+  sym ~ WEB.ExprBuilder scope st fs =>+  bak ~ LCBO.OnlineBackend solver scope st fs =>+  WPO.OnlineSolver solver =>+  Integer ->+  BytesChecker m sym bak (WI.SymBV sym 32, Integer) (WI.SymBV sym 32)+lengthBoundedProvablyNullTerminatedStringComparison maxLen =+  let onMaxBytes _bak zero = pure zero+  in withMaxBytes maxLen onMaxBytes provablyNullTerminatedStrings++---------------------------------------------------------------------+-- ** BytesCheckers for length-bounded comparison++-- | 'BytesChecker' for comparing two bytes without length bounds.+--+-- Stops when bytes differ, otherwise continues indefinitely.+simpleByteComparison ::+  MonadIO m =>+  GHC.HasCallStack =>+  LCB.IsSymBackend sym bak =>+  BytesChecker m sym bak () (WI.SymBV sym 32)+simpleByteComparison =+  BytesChecker $ \bak () byte1Ptr byte2Ptr -> do+    byte1 <- liftIO (ptrToBv8 bak byte1Ptr)+    byte2 <- liftIO (ptrToBv8 bak byte2Ptr)+    compareBytesForStrings bak byte1 byte2 >>= \case+      Just result -> pure (Break result)+      Nothing -> pure (Continue ())++-- | 'BytesChecker' for comparing memory regions with a concrete length bound.+--+-- The accumulator is a pair of unit and the current index. Stops when the index reaches the+-- maximum length, or when bytes differ.+--+-- Returns:+-- * 0 if all bytes up to the length are equal+-- * A negative value if the first differing byte in the first region is less+-- * A positive value if the first differing byte in the first region is greater+lengthBoundedByteComparison ::+  MonadIO m =>+  GHC.HasCallStack =>+  LCB.IsSymBackend sym bak =>+  -- | Maximum length+  Integer ->+  BytesChecker m sym bak ((), Integer) (WI.SymBV sym 32)+lengthBoundedByteComparison maxLen =+  let onMaxBytes bak () = liftIO (WI.bvZero (LCB.backendGetSym bak) (DPN.knownNat @32))+  in withMaxBytes maxLen onMaxBytes simpleByteComparison

@@ -35,12 +35,12 @@   , ppType   )  where -import Control.Lens import Control.Monad.State import Data.Typeable import Data.Vector (Vector) import qualified Data.Vector as V import Numeric.Natural+import Lens.Micro (Lens, lens, (^.)) import Prettyprinter  import Lang.Crucible.LLVM.Bytes

@@ -39,15 +39,17 @@   , testEqual   ) where -import           Control.Lens (view, over, _2, (^.)) import           Control.Monad (foldM, join) import           Data.ByteString (ByteString) import qualified Data.ByteString as BS import           Data.Map (Map) import           Data.Foldable (toList) import           Data.Functor.Identity (Identity(..))-import           Data.Maybe (fromMaybe, mapMaybe)+import           Lens.Micro ((^.), _2, over)+import           Lens.Micro.Extras (view)+ import           Data.List (intersperse)+import           Data.Maybe (fromMaybe, mapMaybe) import           Numeric.Natural import           Prettyprinter 

@@ -52,9 +52,9 @@   , ppIdent   ) where -import Control.Lens import Data.Vector (Vector) import qualified Data.Vector as V+import Lens.Micro ((^.)) import Numeric.Natural import qualified Text.LLVM as L import Prettyprinter

@@ -15,7 +15,6 @@  module Lang.Crucible.LLVM.QQ  ( llvmType- , llvmDecl  , llvmOvr  ) where @@ -34,6 +33,7 @@ import qualified Data.Parameterized.Context as Ctx import           Lang.Crucible.Types import qualified Lang.Crucible.LLVM.Intrinsics.Common as IC+import qualified Lang.Crucible.LLVM.Intrinsics.Declare as Decl import           Lang.Crucible.LLVM.Types  -- | This type closely mirrors the type syntax from llvm-pretty,@@ -85,6 +85,7 @@ parseFloatType :: AT.Parser L.FloatType parseFloatType = AT.choice   [ pure L.Half      <* AT.string "half"+  , pure L.BFloat    <* AT.string "bfloat"   , pure L.Float     <* AT.string "float"   , pure L.Double    <* AT.string "double"   , pure L.Fp128     <* AT.string "fp128"@@ -252,19 +253,8 @@     QQOpaque -> [| L.Opaque |]     QQFunTy ret args varargs -> [| L.FunTy $(liftQQType ret) $(listE (map liftQQType args)) $(lift varargs) |] -liftQQDecl :: QQDeclare -> Q Exp-liftQQDecl (QQDeclare ret nm args varargs) =-   [| L.Declare-      { L.decLinkage    = Nothing-      , L.decVisibility = Nothing-      , L.decRetType    = $(liftQQType ret)-      , L.decName       = $(f nm)-      , L.decArgs       = $(listE (map liftQQType args))-      , L.decVarArgs    = $(lift varargs)-      , L.decAttrs      = []-      , L.decComdat     = Nothing-      }-    |]+liftName :: Either String L.Symbol -> Q Exp+liftName nm = f nm   where   f (Left v)    = varE (mkName v)   f (Right sym) = lift sym@@ -301,6 +291,7 @@   liftFloatType ft = case ft of     L.Half      -> [| HalfFloatRepr |]     L.Float     -> [| SingleFloatRepr |]+    L.BFloat    -> fail "No support for Brain floats / bfloats yet"     L.Double    -> [| DoubleFloatRepr |]     L.Fp128     -> [| QuadFloatRepr |]     L.X86_fp80  -> [| X86_80FloatRepr |]@@ -316,8 +307,8 @@   liftQQDeclToOverride :: QQDeclare -> Q Exp-liftQQDeclToOverride qqd@(QQDeclare ret _nm args varargs) =-  [| IC.LLVMOverride $(liftQQDecl qqd) $(liftArgs args varargs) $(liftTypeRepr ret) |]+liftQQDeclToOverride (QQDeclare ret nm args varargs) =+  [| IC.LLVMOverride (Decl.Declare $(liftName nm) $(liftArgs args varargs) $(liftTypeRepr ret)) |]  -- | This quasiquoter parses values in LLVM type syntax, extended --   with metavariables, and builds values of @Text.LLVM.AST.Type@.@@ -339,31 +330,6 @@   , quotePat = error "llvmType cannot quasiquote a pattern"   , quoteType = error "llvmType cannot quasiquote a Haskell type"   , quoteDec = error "llvmType cannot quasiquote a declaration"-  }---- | This quasiquoter parses values in LLVM function declaration syntax,---   extended with metavariables, and builds values of @Text.LLVM.AST.Declare@.------   Type metavariables start with a @$@ and splice in the named---   program variable, which is expected to have type @Type@.------   Numeric metavariables start with @#@ and splice in an integer---   type whose width is given by the named program variable, which---   is expected to be a @NatRepr@.------   The name of the declaration may also be a @$@ metavariable, in which---   case the named variable is expeted to be a @Symbol@.-llvmDecl :: QuasiQuoter-llvmDecl =-  QuasiQuoter-  { quoteExp = \str ->-       do case AT.parseOnly parseDeclare (T.pack str) of-            Left msg -> error msg-            Right x  -> liftQQDecl x--  , quotePat = error "llvmDecl cannot quasiquote a pattern"-  , quoteType = error "llvmDecl cannot quasiquote a Haskell type"-  , quoteDec = error "llvmDecl cannot quasiquote a declaration"   }  -- | This quasiquoter parses values in LLVM function declaration syntax,

@@ -28,7 +28,6 @@   , simpleLoopFixpoint   ) where -import           Control.Lens import           Control.Monad (when) import           Control.Monad.IO.Class (MonadIO(..)) import           Control.Monad.Reader (ReaderT(..))@@ -36,6 +35,7 @@ import           Control.Monad.Trans.Maybe import           Data.Either import           Data.Foldable+import           Data.Function ((&)) import qualified Data.IntMap as IntMap import           Data.IORef import qualified Data.List as List@@ -43,6 +43,7 @@ import qualified Data.Map as Map import           Data.Map (Map) import qualified Data.Set as Set+import           Lens.Micro ((^.), (.~), (%~)) import qualified System.IO import           Numeric.Natural 

@@ -46,13 +46,14 @@   , simpleLoopFixpoint   ) where -import           Control.Lens import           Control.Monad import           Control.Monad.IO.Class import           Control.Monad.Reader import           Control.Monad.State import           Control.Monad.Trans.Maybe import           Data.Foldable+import           Data.Function ((&))+import           Data.Functor.Identity (runIdentity) import qualified Data.IntMap as IntMap import           Data.IORef import           Data.Kind@@ -64,6 +65,7 @@ import qualified Data.Set as Set import           Data.Set (Set) import           GHC.TypeLits (KnownNat)+import           Lens.Micro ((^.), (.~), (%~)) import           Numeric.Natural (Natural) import qualified System.IO