diff --git a/.gitignore b/.gitignore index ce142e5..819bb25 100644 --- a/.gitignore +++ b/.gitignore @@ -2,3 +2,4 @@ dist-newstyle *~ .DS_Store +.zed/settings.json diff --git a/package.yaml b/package.yaml index ec9d9cf..3111b7c 100644 --- a/package.yaml +++ b/package.yaml @@ -1,14 +1,14 @@ -name: pantomime-base -version: 0.1.0.0 -github: "githubuser/pantomime-base" -license: BSD-3-Clause -author: "Author name here" -maintainer: "example@example.com" -copyright: "2026 Author name here" +name: pantomime-base +version: 0.1.0.0 +github: "githubuser/pantomime-base" +license: BSD-3-Clause +author: "Author name here" +maintainer: "example@example.com" +copyright: "2026 Author name here" extra-source-files: -- README.md -- CHANGELOG.md + - README.md + - CHANGELOG.md # Metadata used when publishing your package # synopsis: Short description of your package @@ -17,54 +17,79 @@ extra-source-files: # To avoid duplicated efforts in documentation and dealing with the # complications of embedding Haddock markup inside cabal files, it is # common to point users to the README.md file. -description: Please see the README on GitHub at +description: Please see the README on GitHub at default-extensions: -- AllowAmbiguousTypes -- BlockArguments -- ConstraintKinds -- DataKinds -- DeriveDataTypeable -- DeriveTraversable -- FlexibleContexts -- FlexibleInstances -- GADTs -- ImportQualifiedPost -- KindSignatures -- LambdaCase -- MultiParamTypeClasses -- MultiWayIf -- NamedFieldPuns -- RankNTypes -- RecordWildCards -- ScopedTypeVariables -- TemplateHaskell -- TupleSections -- TypeAbstractions -- TypeApplications -- TypeFamilies -- TypeOperators + - AllowAmbiguousTypes + - BlockArguments + - ConstraintKinds + - DataKinds + - DeriveDataTypeable + - DeriveTraversable + - FlexibleContexts + - FlexibleInstances + - GADTs + - ImportQualifiedPost + - KindSignatures + - LambdaCase + - MultiParamTypeClasses + - MultiWayIf + - NamedFieldPuns + - RankNTypes + - RecordWildCards + - ScopedTypeVariables + - TemplateHaskell + - TupleSections + - TypeAbstractions + - TypeApplications + - TypeFamilies + - TypeOperators dependencies: -- base >= 4.7 && < 5 -- composition -- constraints -- ghc-bignum -- ghc-prim -- pantomime + - base >= 4.7 && < 5 + - bytestring + - composition + - constraints + - ghc-bignum + - ghc-internal + - ghc-prim + - pantomime + - template-haskell ghc-options: -- -Wall -- -Wcompat -- -Widentities -- -Wincomplete-record-updates -- -Wincomplete-uni-patterns -- -Wmissing-export-lists -- -Wmissing-home-modules -- -Wpartial-fields -- -Wredundant-constraints -- -Wprepositive-qualified-module -- -fexpose-all-unfoldings + - -Wall + - -Wcompat + - -Widentities + - -Wincomplete-record-updates + - -Wincomplete-uni-patterns + - -Wmissing-export-lists + - -Wmissing-home-modules + - -Wpartial-fields + - -Wredundant-constraints + - -Wprepositive-qualified-module + - -fexpose-all-unfoldings library: source-dirs: src + +tests: + pantomime-base-test: + main: Main.hs + source-dirs: test + ghc-options: + - -threaded + - -rtsopts + - -with-rtsopts=-N + - -fplugin=Pantomime + default-extensions: + - MagicHash + - UnboxedTuples + dependencies: + - pantomime-base + - pantomime + - bytestring + - hspec + - hspec-expectations + - ghc-prim + - iproute + - containers diff --git a/pantomime-base.cabal b/pantomime-base.cabal index b24f77f..fcd8994 100644 --- a/pantomime-base.cabal +++ b/pantomime-base.cabal @@ -1,6 +1,6 @@ cabal-version: 2.2 --- This file has been generated from package.yaml by hpack version 0.39.1. +-- This file has been generated from package.yaml by hpack version 0.38.1. -- -- see: https://github.com/sol/hpack @@ -26,6 +26,8 @@ source-repository head library exposed-modules: Pantomime.Base + Pantomime.IO + Pantomime.Ptr other-modules: Paths_pantomime_base autogen-modules: @@ -60,9 +62,82 @@ library ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -Wprepositive-qualified-module -fexpose-all-unfoldings build-depends: base >=4.7 && <5 + , bytestring , composition , constraints , ghc-bignum + , ghc-internal , ghc-prim , pantomime + , template-haskell + default-language: Haskell2010 + +test-suite pantomime-base-test + type: exitcode-stdio-1.0 + main-is: Main.hs + other-modules: + BoolTest + ByteStringTest + Common + ContainersTest + Int + Int16 + Int32 + Int64 + Int8 + IntegerTest + IOTest + IProuteTest + PtrTest + Word + Word64 + Word8 + Paths_pantomime_base + autogen-modules: + Paths_pantomime_base + hs-source-dirs: + test + default-extensions: + AllowAmbiguousTypes + BlockArguments + ConstraintKinds + DataKinds + DeriveDataTypeable + DeriveTraversable + FlexibleContexts + FlexibleInstances + GADTs + ImportQualifiedPost + KindSignatures + LambdaCase + MultiParamTypeClasses + MultiWayIf + NamedFieldPuns + RankNTypes + RecordWildCards + ScopedTypeVariables + TemplateHaskell + TupleSections + TypeAbstractions + TypeApplications + TypeFamilies + TypeOperators + MagicHash + UnboxedTuples + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -Wprepositive-qualified-module -fexpose-all-unfoldings -threaded -rtsopts -with-rtsopts=-N -fplugin=Pantomime + build-depends: + base >=4.7 && <5 + , bytestring + , composition + , constraints + , containers + , ghc-bignum + , ghc-internal + , ghc-prim + , hspec + , hspec-expectations + , iproute + , pantomime + , pantomime-base + , template-haskell default-language: Haskell2010 diff --git a/src/Pantomime/Base.hs b/src/Pantomime/Base.hs index 60514d3..9745388 100644 --- a/src/Pantomime/Base.hs +++ b/src/Pantomime/Base.hs @@ -5,382 +5,389 @@ {-# LANGUAGE UnboxedTuples #-} module Pantomime.Base - ( axioms - ) where + ( axioms, + ) +where import Control.Exception.Base qualified as GHC (patError, throw) import Data.Constraint.Unsafe (unsafeSNat) import Data.List qualified as GHC (zip) +import Unsafe.Coerce (unsafeCoerce#) +import GHC.Stack (HasCallStack) import GHC.Base - ( TYPE - , Int# - , Int8# - , Int16# - , Int32# - , Int64# - , Word# - , Word8# - , Word16# - , Word32# - , Word64# - , Addr# - , RuntimeRep (..) - , Int (..) + ( Addr#, + Int (..), + Int#, + Int16#, + Int32#, + Int64#, + Int8#, + RuntimeRep (..), + TYPE, + Word#, + Word16#, + Word32#, + Word64#, + Word8#, ) import GHC.Base qualified as GHC +import GHC.Classes qualified as GHCClasses import GHC.Exts (IsList (..)) -import GHC.Num (Integer(..), Natural (..)) +import GHC.Magic (lazy) +import GHC.Num (Integer (..), Natural (..)) import GHC.Num qualified as GHC - ( integerFromBigNat# - , integerFromBigNatNeg# - , integerFromNatural - , integerFromWord# - , integerSub - , integerToInt# - , integerToNatural - , integerToWord# - , naturalAdd - , naturalSubThrow - , naturalFromBigNat# - , naturalFromWord# + ( integerFromBigNat#, + integerFromBigNatNeg#, + integerFromNatural, + integerFromWord#, + integerSub, + integerToInt#, + integerToNatural, + integerToWord#, + naturalAdd, + naturalFromBigNat#, + naturalFromWord#, + naturalSubThrow, ) -import GHC.Num.Primitives qualified as GHC (wordFromAbsInt#) import GHC.Num.BigNat qualified as GHC - ( bigNatFromWord# - , bigNatToWord# - , bigNatAddWord# - , bigNatAdd - , bigNatCompare - , bigNatFromWord2# - , bigNatSubWordUnsafe# - , bigNatSub - , bigNatSubUnsafe + ( bigNatAdd, + bigNatAddWord#, + bigNatCompare, + bigNatFromWord#, + bigNatFromWord2#, + bigNatSub, + bigNatSubUnsafe, + bigNatSubWordUnsafe#, + bigNatToWord#, ) +import GHC.Num.Primitives qualified as GHC (wordFromAbsInt#) import GHC.Prim qualified as GHC import GHC.Prim.Exception qualified as GHC import GHC.TypeLits (KnownNat, SNat, type (+)) import GHC.TypeNats qualified as GHC (withSomeSNat) import Pantomime (PluginAxioms (..)) import Pantomime.BuiltIn qualified as Pantomime -import Prelude hiding (undefined, map, zip, fromInteger, toInteger) import Unsafe.Coerce (unsafeCoerce) +import Prelude hiding (fromInteger, map, toInteger, undefined, zip) axioms :: PluginAxioms -axioms = PluginAxioms - { typeAxioms = fromList - [ (''Int#, ''BitVecPW) - , (''Int8#, ''BitVec8) - , (''Int16#, ''BitVec16) - , (''Int32#, ''BitVec32) - , (''Int64#, ''BitVec64) - , (''Word#, ''BitVecPW) - , (''Word8#, ''BitVec8) - , (''Word16#, ''BitVec16) - , (''Word32#, ''BitVec32) - , (''Word64#, ''BitVec64) - ] - , termAxioms = - -- Pantomime embed operations. - ------------------------------ - [ ('Pantomime.toInt#, 'fromBV) - , ('Pantomime.toInt8#, 'fromBV) - , ('Pantomime.toInt16#, 'fromBV) - , ('Pantomime.toInt32#, 'fromBV) - , ('Pantomime.toInt64#, 'fromBV) - , ('Pantomime.toWord#, 'fromBV) - , ('Pantomime.toWord8#, 'fromBV) - , ('Pantomime.toWord16#, 'fromBV) - , ('Pantomime.toWord32#, 'fromBV) - , ('Pantomime.toWord64#, 'fromBV) - , ('Pantomime.fromInt#, 'toBV) - , ('Pantomime.fromInt8#, 'toBV) - , ('Pantomime.fromInt16#, 'toBV) - , ('Pantomime.fromInt32#, 'toBV) - , ('Pantomime.fromInt64#, 'toBV) - , ('Pantomime.fromWord#, 'toBV) - , ('Pantomime.fromWord8#, 'toBV) - , ('Pantomime.fromWord16#, 'toBV) - , ('Pantomime.fromWord32#, 'toBV) - , ('Pantomime.fromWord64#, 'toBV) - - -- Integer to pantomime primitive conversions. - ---------------------------------------------- - , ('Pantomime.fromInteger, 'fromInteger) - , ('Pantomime.toInteger, 'toInteger) - - -- System FC primitive operations. - ---------------------------------- - , ('GHC.tagToEnum#, 'tagToEnum) - -- TODO: While these might be deprecated for use, they are in fact required - -- in this context... Not sure what to do if these are unexposed (but still - -- used internally) in the future. - , ('GHC.dataToTagSmall#, 'dataToTag) - , ('GHC.dataToTagLarge#, 'dataToTag) - , ('GHC.raise#, 'Pantomime.raise) - - -- Int# primitive operations. - ----------------------------- - , ('GHC.intToInt8#, 'intToInt8#) - , ('GHC.intToInt16#, 'intToInt16#) - , ('GHC.intToInt32#, 'intToInt32#) - , ('GHC.intToInt64#, 'intToInt64#) - , ('GHC.int2Word#, 'int2Word#) - -- , ('GHC.int2Float#, 'undefined) - -- , ('GHC.int2Double#, 'undefined) - , ('(GHC.+#), '(+#)) - , ('(GHC.-#), '(-#)) - , ('(GHC.*#), '(*#)) - , ('GHC.addIntC#, 'addIntC#) - , ('GHC.subIntC#, 'subIntC#) - -- , ('GHC.timesInt2#, 'timesInt2#) - -- , ('GHC.mulIntMayOflo#, 'mulIntMayOflo#) - -- , ('GHC.quotInt#, 'quotInt#) - -- , ('GHC.remInt#, 'remInt#) - -- , ('GHC.quotRemInt#, 'quotRemInt#) - , ('GHC.andI#, 'andI#) - , ('GHC.orI#, 'orI#) - , ('GHC.xorI#, 'xorI#) - , ('GHC.notI#, 'notI#) - , ('GHC.negateInt#, 'negateInt#) - -- , ('GHC.uncheckedIShiftL#, 'uncheckedIShiftL#) - -- , ('GHC.uncheckedIShiftRA#, 'uncheckedIShiftRA#) - -- , ('GHC.uncheckedIShiftRL#, 'uncheckedIShiftRL#) - , ('(GHC.==#), '(==#)) - , ('(GHC./=#), '(/=#)) - , ('(GHC.>=#), '(>=#)) - , ('(GHC.>#), '(>#)) - , ('(GHC.<=#), '(<=#)) - , ('(GHC.<#), '(<#)) - - -- Int8# primitive operations. - ------------------------------ - , ('GHC.int8ToInt#, 'int8ToInt#) - , ('GHC.int8ToWord8#, 'int8ToWord8#) - , ('GHC.plusInt8#, 'plusInt8#) - , ('GHC.subInt8#, 'subInt8#) - , ('GHC.timesInt8#, 'timesInt8#) - -- , ('GHC.quotInt8#, 'quotInt8#) - -- , ('GHC.remInt8#, 'remInt8#) - -- , ('GHC.quotRemInt8#, 'quotRemInt8#) - -- , ('GHC.uncheckedShiftLInt8#, 'uncheckedShiftLInt8#) - -- , ('GHC.uncheckedShiftRAInt8#, 'uncheckedShiftRAInt8#) - -- , ('GHC.uncheckedShiftRLInt8#, 'uncheckedShiftRLInt8#) - , ('GHC.negateInt8#, 'negateInt8#) - , ('GHC.eqInt8#, 'eqInt8#) - , ('GHC.neInt8#, 'neInt8#) - , ('GHC.geInt8#, 'geInt8#) - , ('GHC.gtInt8#, 'gtInt8#) - , ('GHC.leInt8#, 'leInt8#) - , ('GHC.ltInt8#, 'ltInt8#) - - -- Int16# primitive operations. - ------------------------------ - , ('GHC.int16ToInt#, 'int16ToInt#) - , ('GHC.int16ToWord16#, 'int16ToWord16#) - , ('GHC.plusInt16#, 'plusInt16#) - , ('GHC.subInt16#, 'subInt16#) - , ('GHC.timesInt16#, 'timesInt16#) - -- , ('GHC.quotInt16#, 'quotInt16#) - -- , ('GHC.remInt16#, 'remInt16#) - -- , ('GHC.quotRemInt16#, 'quotRemInt16#) - -- , ('GHC.uncheckedShiftLInt16#, 'uncheckedShiftLInt16#) - -- , ('GHC.uncheckedShiftRAInt16#, 'uncheckedShiftRAInt16#) - -- , ('GHC.uncheckedShiftRLInt16#, 'uncheckedShiftRLInt16#) - , ('GHC.negateInt16#, 'negateInt16#) - , ('GHC.eqInt16#, 'eqInt16#) - , ('GHC.neInt16#, 'neInt16#) - , ('GHC.geInt16#, 'geInt16#) - , ('GHC.gtInt16#, 'gtInt16#) - , ('GHC.leInt16#, 'leInt16#) - , ('GHC.ltInt16#, 'ltInt16#) - - -- Int32# primitive operations. - ------------------------------ - , ('GHC.int32ToInt#, 'int32ToInt#) - , ('GHC.int32ToWord32#, 'int32ToWord32#) - , ('GHC.plusInt32#, 'plusInt32#) - , ('GHC.subInt32#, 'subInt32#) - , ('GHC.timesInt32#, 'timesInt32#) - -- , ('GHC.quotInt32#, 'quotInt32#) - -- , ('GHC.remInt32#, 'remInt32#) - -- , ('GHC.quotRemInt32#, 'quotRemInt32#) - -- , ('GHC.uncheckedShiftLInt32#, 'uncheckedShiftLInt32#) - -- , ('GHC.uncheckedShiftRAInt32#, 'uncheckedShiftRAInt32#) - -- , ('GHC.uncheckedShiftRLInt32#, 'uncheckedShiftRLInt32#) - , ('GHC.negateInt32#, 'negateInt32#) - , ('GHC.eqInt32#, 'eqInt32#) - , ('GHC.neInt32#, 'neInt32#) - , ('GHC.geInt32#, 'geInt32#) - , ('GHC.gtInt32#, 'gtInt32#) - , ('GHC.leInt32#, 'leInt32#) - , ('GHC.ltInt32#, 'ltInt32#) - - -- Int64# primitive operations. - ------------------------------ - , ('GHC.int64ToInt#, 'int64ToInt#) - , ('GHC.int64ToWord64#, 'int64ToWord64#) - , ('GHC.plusInt64#, 'plusInt64#) - , ('GHC.subInt64#, 'subInt64#) - , ('GHC.timesInt64#, 'timesInt64#) - -- , ('GHC.quotInt64#, 'quotInt64#) - -- , ('GHC.remInt64#, 'remInt64#) - -- , ('GHC.uncheckedIShiftL64#, 'uncheckedIShiftL64#) - -- , ('GHC.uncheckedIShiftRA64#, 'uncheckedIShiftRA64#) - -- , ('GHC.uncheckedIShiftRL64#, 'uncheckedIShiftRL64#) - , ('GHC.negateInt64#, 'negateInt64#) - , ('GHC.eqInt64#, 'eqInt64#) - , ('GHC.neInt64#, 'neInt64#) - , ('GHC.geInt64#, 'geInt64#) - , ('GHC.gtInt64#, 'gtInt64#) - , ('GHC.leInt64#, 'leInt64#) - , ('GHC.ltInt64#, 'ltInt64#) - - -- Word# primitive operations. - ------------------------------ - , ('GHC.wordToWord8#, 'wordToWord8#) - , ('GHC.wordToWord16#, 'wordToWord16#) - , ('GHC.wordToWord32#, 'wordToWord32#) - , ('GHC.wordToWord64#, 'wordToWord64#) - , ('GHC.word2Int#, 'word2Int#) - -- , ('GHC.word2Float#, 'word2Float#) - -- , ('GHC.word2Double#, 'word2Double#) - , ('GHC.plusWord#, 'plusWord#) - , ('GHC.minusWord#, 'minusWord#) - , ('GHC.timesWord#, 'timesWord#) - , ('GHC.addWordC#, 'addWordC#) - , ('GHC.subWordC#, 'subWordC#) - -- , ('GHC.plusWord2#, 'plusWord2#) - -- , ('GHC.timesWord2#, 'timesWord2#) - -- , ('GHC.quotWord#, 'quotWord#) - -- , ('GHC.remWord#, 'remWord#) - -- , ('GHC.quotRemWord#, 'quotRemWord#) - -- , ('GHC.quotRemWord2#, 'quotRemWord2#) - , ('GHC.and#, 'and#) - , ('GHC.or#, 'or#) - , ('GHC.xor#, 'xor#) - , ('GHC.not#, 'not#) - , ('GHC.uncheckedShiftL#, 'uncheckedShiftL#) - , ('GHC.uncheckedShiftRL#, 'uncheckedShiftRL#) - , ('GHC.eqWord#, 'eqWord#) - , ('GHC.neWord#, 'neWord#) - , ('GHC.geWord#, 'geWord#) - , ('GHC.gtWord#, 'gtWord#) - , ('GHC.leWord#, 'leWord#) - , ('GHC.ltWord#, 'ltWord#) - - -- Word8# primitive operations. - ------------------------------ - , ('GHC.word8ToWord#, 'word8ToWord#) - , ('GHC.word8ToInt8#, 'word8ToInt8#) - , ('GHC.plusWord8#, 'plusWord8#) - , ('GHC.subWord8#, 'subWord8#) - , ('GHC.timesWord8#, 'timesWord8#) - -- , ('GHC.quotWord8#, 'quotWord8#) - -- , ('GHC.remWord8#, 'remWord8#) - -- , ('GHC.quotRemWord8#, 'quotRemWord8#) - , ('GHC.andWord8#, 'andWord8#) - , ('GHC.orWord8#, 'orWord8#) - , ('GHC.xorWord8#, 'xorWord8#) - , ('GHC.notWord8#, 'notWord8#) - -- , ('GHC.uncheckedShiftLWord8#, 'uncheckedShiftLWord8#) - -- , ('GHC.uncheckedShiftRLWord8#, 'uncheckedShiftRLWord8#) - , ('GHC.eqWord8#, 'eqWord8#) - , ('GHC.neWord8#, 'neWord8#) - , ('GHC.geWord8#, 'geWord8#) - , ('GHC.gtWord8#, 'gtWord8#) - , ('GHC.leWord8#, 'leWord8#) - , ('GHC.ltWord8#, 'ltWord8#) - - -- Word16# primitive operations. - ------------------------------ - , ('GHC.word16ToWord#, 'word16ToWord#) - , ('GHC.word16ToInt16#, 'word16ToInt16#) - , ('GHC.plusWord16#, 'plusWord16#) - , ('GHC.subWord16#, 'subWord16#) - , ('GHC.timesWord16#, 'timesWord16#) - -- , ('GHC.quotWord16#, 'quotWord16#) - -- , ('GHC.remWord16#, 'remWord16#) - -- , ('GHC.quotRemWord16#, 'quotRemWord16#) - , ('GHC.andWord16#, 'andWord16#) - , ('GHC.orWord16#, 'orWord16#) - , ('GHC.xorWord16#, 'xorWord16#) - , ('GHC.notWord16#, 'notWord16#) - -- , ('GHC.uncheckedShiftLWord16#, 'uncheckedShiftLWord16#) - -- , ('GHC.uncheckedShiftRLWord16#, 'uncheckedShiftRLWord16#) - , ('GHC.eqWord16#, 'eqWord16#) - , ('GHC.neWord16#, 'neWord16#) - , ('GHC.geWord16#, 'geWord16#) - , ('GHC.gtWord16#, 'gtWord16#) - , ('GHC.leWord16#, 'leWord16#) - , ('GHC.ltWord16#, 'ltWord16#) - - -- Word32# primitive operations. - ------------------------------ - , ('GHC.word32ToWord#, 'word32ToWord#) - , ('GHC.word32ToInt32#, 'word32ToInt32#) - , ('GHC.plusWord32#, 'plusWord32#) - , ('GHC.subWord32#, 'subWord32#) - , ('GHC.timesWord32#, 'timesWord32#) - -- , ('GHC.quotWord32#, 'quotWord32#) - -- , ('GHC.remWord32#, 'remWord32#) - -- , ('GHC.quotRemWord32#, 'quotRemWord32#) - , ('GHC.andWord32#, 'andWord32#) - , ('GHC.orWord32#, 'orWord32#) - , ('GHC.xorWord32#, 'xorWord32#) - , ('GHC.notWord32#, 'notWord32#) - -- , ('GHC.uncheckedShiftLWord32#, 'uncheckedShiftLWord32#) - -- , ('GHC.uncheckedShiftRLWord32#, 'uncheckedShiftRLWord32#) - , ('GHC.eqWord32#, 'eqWord32#) - , ('GHC.neWord32#, 'neWord32#) - , ('GHC.geWord32#, 'geWord32#) - , ('GHC.gtWord32#, 'gtWord32#) - , ('GHC.leWord32#, 'leWord32#) - , ('GHC.ltWord32#, 'ltWord32#) - - -- Word64# primitive operations. - ------------------------------ - , ('GHC.word64ToWord#, 'word64ToWord#) - , ('GHC.word64ToInt64#, 'word64ToInt64#) - , ('GHC.plusWord64#, 'plusWord64#) - , ('GHC.subWord64#, 'subWord64#) - , ('GHC.timesWord64#, 'timesWord64#) - -- , ('GHC.quotWord64#, 'quotWord64#) - -- , ('GHC.remWord64#, 'remWord64#) - , ('GHC.and64#, 'and64#) - , ('GHC.or64#, 'or64#) - , ('GHC.xor64#, 'xor64#) - , ('GHC.not64#, 'not64#) - -- , ('GHC.uncheckedShiftL64#, 'uncheckedShiftL64#) - -- , ('GHC.uncheckedShiftRL64#, 'uncheckedShiftRL64#) - , ('GHC.eqWord64#, 'eqWord64#) - , ('GHC.neWord64#, 'neWord64#) - , ('GHC.geWord64#, 'geWord64#) - , ('GHC.gtWord64#, 'gtWord64#) - , ('GHC.leWord64#, 'leWord64#) - , ('GHC.ltWord64#, 'ltWord64#) - - -- Haskell functions without unfoldings. - ---------------------------------------- - -- NOTE: Ideally we would not have these. It's just that GHC tosses - -- their unfolding and we cannot get 'base' to be compiled with the flag - -- 'expose-all-unfoldings' as 'base' is tied to the compiler... - , ('GHC.integerFromWord#, 'integerFromWord#) - , ('GHC.integerToWord#, 'integerToWord#) - , ('GHC.integerFromNatural, 'integerFromNatural) - , ('GHC.integerToNatural, 'integerToNatural) - , ('GHC.integerToInt#, 'integerToInt#) - , ('GHC.integerSub, 'integerSub) - , ('GHC.naturalAdd, 'naturalAdd) - , ('GHC.naturalSubThrow, 'naturalSubThrow) - , ('GHC.noinline, 'noinline) - , ('GHC.undefined, 'undefined) - , ('GHC.throw, 'throw) - , ('GHC.patError, 'patError') - , ('GHC.withSomeSNat, 'withSomeSNat) - , ('GHC.map, 'map) - , ('GHC.zip, 'zip) - ] - } +axioms = + PluginAxioms + { typeAxioms = + fromList + [ (''Int#, ''BitVecPW), + (''Int8#, ''BitVec8), + (''Int16#, ''BitVec16), + (''Int32#, ''BitVec32), + (''Int64#, ''BitVec64), + (''Word#, ''BitVecPW), + (''Word8#, ''BitVec8), + (''Word16#, ''BitVec16), + (''Word32#, ''BitVec32), + (''Word64#, ''BitVec64), + (''Addr#, ''BitVecPW) + ], + termAxioms = + -- Pantomime embed operations. + ------------------------------ + [ ('Pantomime.toInt#, 'fromBV), + ('Pantomime.toInt8#, 'fromBV), + ('Pantomime.toInt16#, 'fromBV), + ('Pantomime.toInt32#, 'fromBV), + ('Pantomime.toInt64#, 'fromBV), + ('Pantomime.toWord#, 'fromBV), + ('Pantomime.toWord8#, 'fromBV), + ('Pantomime.toWord16#, 'fromBV), + ('Pantomime.toWord32#, 'fromBV), + ('Pantomime.toWord64#, 'fromBV), + ('Pantomime.fromInt#, 'toBV), + ('Pantomime.fromInt8#, 'toBV), + ('Pantomime.fromInt16#, 'toBV), + ('Pantomime.fromInt32#, 'toBV), + ('Pantomime.fromInt64#, 'toBV), + ('Pantomime.fromWord#, 'toBV), + ('Pantomime.fromWord8#, 'toBV), + ('Pantomime.fromWord16#, 'toBV), + ('Pantomime.fromWord32#, 'toBV), + ('Pantomime.fromWord64#, 'toBV), + -- Integer to pantomime primitive conversions. + ---------------------------------------------- + ('Pantomime.fromInteger, 'fromInteger), + ('Pantomime.toInteger, 'toInteger), + -- System FC primitive operations. + ---------------------------------- + ('GHC.tagToEnum#, 'tagToEnum), + -- TODO: While these might be deprecated for use, they are in fact required + -- in this context... Not sure what to do if these are unexposed (but still + -- used internally) in the future. + ('GHC.dataToTagSmall#, 'dataToTag), + ('GHC.dataToTagLarge#, 'dataToTag), + ('GHC.raise#, 'Pantomime.raise), + -- Int# primitive operations. + ----------------------------- + ('GHC.intToInt8#, 'intToInt8#), + ('GHC.intToInt16#, 'intToInt16#), + ('GHC.intToInt32#, 'intToInt32#), + ('GHC.intToInt64#, 'intToInt64#), + ('GHC.int2Word#, 'int2Word#), + -- , ('GHC.int2Float#, 'undefined) + -- , ('GHC.int2Double#, 'undefined) + ('(GHC.+#), '(+#)), + ('(GHC.-#), '(-#)), + ('(GHC.*#), '(*#)), + ('GHC.addIntC#, 'addIntC#), + ('GHC.subIntC#, 'subIntC#), + -- , ('GHC.timesInt2#, 'timesInt2#) + -- , ('GHC.mulIntMayOflo#, 'mulIntMayOflo#) + ('GHC.quotInt#, 'quotInt#), + ('GHC.remInt#, 'remInt#), + ('GHC.uncheckedIShiftL#, 'uncheckedIShiftL#), + ('GHC.uncheckedIShiftRA#, 'uncheckedIShiftRA#), + ('GHC.uncheckedIShiftRL#, 'uncheckedIShiftRL#), + ('GHC.andI#, 'andI#), + ('GHC.orI#, 'orI#), + ('GHC.xorI#, 'xorI#), + ('GHC.notI#, 'notI#), + ('GHC.negateInt#, 'negateInt#), + ('(GHC.==#), '(==#)), + ('(GHC./=#), '(/=#)), + ('(GHC.>=#), '(>=#)), + ('(GHC.>#), '(>#)), + ('(GHC.<=#), '(<=#)), + ('(GHC.<#), '(<#)), + -- Int8# primitive operations. + ------------------------------ + ('GHC.int8ToInt#, 'int8ToInt#), + ('GHC.int8ToWord8#, 'int8ToWord8#), + ('GHC.plusInt8#, 'plusInt8#), + ('GHC.subInt8#, 'subInt8#), + ('GHC.timesInt8#, 'timesInt8#), + -- , ('GHC.quotInt8#, 'quotInt8#) + -- , ('GHC.remInt8#, 'remInt8#) + -- , ('GHC.quotRemInt8#, 'quotRemInt8#) + -- , ('GHC.uncheckedShiftLInt8#, 'uncheckedShiftLInt8#) + -- , ('GHC.uncheckedShiftRAInt8#, 'uncheckedShiftRAInt8#) + -- , ('GHC.uncheckedShiftRLInt8#, 'uncheckedShiftRLInt8#) + ('GHC.negateInt8#, 'negateInt8#), + ('GHC.eqInt8#, 'eqInt8#), + ('GHC.neInt8#, 'neInt8#), + ('GHC.geInt8#, 'geInt8#), + ('GHC.gtInt8#, 'gtInt8#), + ('GHC.leInt8#, 'leInt8#), + ('GHC.ltInt8#, 'ltInt8#), + -- Int16# primitive operations. + ------------------------------ + ('GHC.int16ToInt#, 'int16ToInt#), + ('GHC.int16ToWord16#, 'int16ToWord16#), + ('GHC.plusInt16#, 'plusInt16#), + ('GHC.subInt16#, 'subInt16#), + ('GHC.timesInt16#, 'timesInt16#), + -- , ('GHC.quotInt16#, 'quotInt16#) + -- , ('GHC.remInt16#, 'remInt16#) + -- , ('GHC.quotRemInt16#, 'quotRemInt16#) + -- , ('GHC.uncheckedShiftLInt16#, 'uncheckedShiftLInt16#) + -- , ('GHC.uncheckedShiftRAInt16#, 'uncheckedShiftRAInt16#) + -- , ('GHC.uncheckedShiftRLInt16#, 'uncheckedShiftRLInt16#) + ('GHC.negateInt16#, 'negateInt16#), + ('GHC.eqInt16#, 'eqInt16#), + ('GHC.neInt16#, 'neInt16#), + ('GHC.geInt16#, 'geInt16#), + ('GHC.gtInt16#, 'gtInt16#), + ('GHC.leInt16#, 'leInt16#), + ('GHC.ltInt16#, 'ltInt16#), + -- Int32# primitive operations. + ------------------------------ + ('GHC.int32ToInt#, 'int32ToInt#), + ('GHC.int32ToWord32#, 'int32ToWord32#), + ('GHC.plusInt32#, 'plusInt32#), + ('GHC.subInt32#, 'subInt32#), + ('GHC.timesInt32#, 'timesInt32#), + -- , ('GHC.quotInt32#, 'quotInt32#) + -- , ('GHC.remInt32#, 'remInt32#) + -- , ('GHC.quotRemInt32#, 'quotRemInt32#) + -- , ('GHC.uncheckedShiftLInt32#, 'uncheckedShiftLInt32#) + -- , ('GHC.uncheckedShiftRAInt32#, 'uncheckedShiftRAInt32#) + -- , ('GHC.uncheckedShiftRLInt32#, 'uncheckedShiftRLInt32#) + ('GHC.negateInt32#, 'negateInt32#), + ('GHC.eqInt32#, 'eqInt32#), + ('GHC.neInt32#, 'neInt32#), + ('GHC.geInt32#, 'geInt32#), + ('GHC.gtInt32#, 'gtInt32#), + ('GHC.leInt32#, 'leInt32#), + ('GHC.ltInt32#, 'ltInt32#), + -- Int64# primitive operations. + ------------------------------ + ('GHC.int64ToInt#, 'int64ToInt#), + ('GHC.int64ToWord64#, 'int64ToWord64#), + ('GHC.plusInt64#, 'plusInt64#), + ('GHC.subInt64#, 'subInt64#), + ('GHC.timesInt64#, 'timesInt64#), + -- , ('GHC.quotInt64#, 'quotInt64#) + -- , ('GHC.remInt64#, 'remInt64#) + -- , ('GHC.uncheckedIShiftL64#, 'uncheckedIShiftL64#) + -- , ('GHC.uncheckedIShiftRA64#, 'uncheckedIShiftRA64#) + -- , ('GHC.uncheckedIShiftRL64#, 'uncheckedIShiftRL64#) + ('GHC.negateInt64#, 'negateInt64#), + ('GHC.eqInt64#, 'eqInt64#), + ('GHC.neInt64#, 'neInt64#), + ('GHC.geInt64#, 'geInt64#), + ('GHC.gtInt64#, 'gtInt64#), + ('GHC.leInt64#, 'leInt64#), + ('GHC.ltInt64#, 'ltInt64#), + -- Word# primitive operations. + ------------------------------ + ('GHC.wordToWord8#, 'wordToWord8#), + ('GHC.wordToWord16#, 'wordToWord16#), + ('GHC.wordToWord32#, 'wordToWord32#), + ('GHC.wordToWord64#, 'wordToWord64#), + ('GHC.word2Int#, 'word2Int#), + -- , ('GHC.word2Float#, 'word2Float#) + -- , ('GHC.word2Double#, 'word2Double#) + ('GHC.plusWord#, 'plusWord#), + ('GHC.minusWord#, 'minusWord#), + ('GHC.timesWord#, 'timesWord#), + ('GHC.addWordC#, 'addWordC#), + ('GHC.subWordC#, 'subWordC#), + -- , ('GHC.plusWord2#, 'plusWord2#) + -- , ('GHC.timesWord2#, 'timesWord2#) + -- , ('GHC.quotWord#, 'quotWord#) + -- , ('GHC.remWord#, 'remWord#) + -- , ('GHC.quotRemWord#, 'quotRemWord#) + -- , ('GHC.quotRemWord2#, 'quotRemWord2#) + ('GHC.and#, 'and#), + ('GHC.or#, 'or#), + ('GHC.xor#, 'xor#), + ('GHC.not#, 'not#), + ('GHC.uncheckedShiftL#, 'uncheckedShiftL#), + ('GHC.uncheckedShiftRL#, 'uncheckedShiftRL#), + ('GHC.eqWord#, 'eqWord#), + ('GHC.neWord#, 'neWord#), + ('GHC.geWord#, 'geWord#), + ('GHC.gtWord#, 'gtWord#), + ('GHC.leWord#, 'leWord#), + ('GHC.ltWord#, 'ltWord#), + ('GHC.ltAddr#, 'ltAddr#), + ('GHC.leAddr#, 'leAddr#), + ('GHC.gtAddr#, 'gtAddr#), + ('GHC.geAddr#, 'geAddr#), + ('GHC.eqAddr#, 'eqAddr#), + ('GHC.neAddr#, 'neAddr#), + ('GHC.minusAddr#, 'minusAddr#), + -- Word8# primitive operations. + ------------------------------ + ('GHC.word8ToWord#, 'word8ToWord#), + ('GHC.word8ToInt8#, 'word8ToInt8#), + ('GHC.plusWord8#, 'plusWord8#), + ('GHC.subWord8#, 'subWord8#), + ('GHC.timesWord8#, 'timesWord8#), + -- , ('GHC.quotWord8#, 'quotWord8#) + -- , ('GHC.remWord8#, 'remWord8#) + -- , ('GHC.quotRemWord8#, 'quotRemWord8#) + ('GHC.andWord8#, 'andWord8#), + ('GHC.orWord8#, 'orWord8#), + ('GHC.xorWord8#, 'xorWord8#), + ('GHC.notWord8#, 'notWord8#), + ('GHC.uncheckedShiftLWord8#, 'uncheckedShiftLWord8#), + ('GHC.uncheckedShiftRLWord8#, 'uncheckedShiftRLWord8#), + ('GHC.eqWord8#, 'eqWord8#), + ('GHC.neWord8#, 'neWord8#), + ('GHC.geWord8#, 'geWord8#), + ('GHC.gtWord8#, 'gtWord8#), + ('GHC.leWord8#, 'leWord8#), + ('GHC.ltWord8#, 'ltWord8#), + -- Word16# primitive operations. + ------------------------------ + ('GHC.word16ToWord#, 'word16ToWord#), + ('GHC.word16ToInt16#, 'word16ToInt16#), + ('GHC.plusWord16#, 'plusWord16#), + ('GHC.subWord16#, 'subWord16#), + ('GHC.timesWord16#, 'timesWord16#), + -- , ('GHC.quotWord16#, 'quotWord16#) + -- , ('GHC.remWord16#, 'remWord16#) + -- , ('GHC.quotRemWord16#, 'quotRemWord16#) + ('GHC.andWord16#, 'andWord16#), + ('GHC.orWord16#, 'orWord16#), + ('GHC.xorWord16#, 'xorWord16#), + ('GHC.notWord16#, 'notWord16#), + -- , ('GHC.uncheckedShiftLWord16#, 'uncheckedShiftLWord16#) + -- , ('GHC.uncheckedShiftRLWord16#, 'uncheckedShiftRLWord16#) + ('GHC.eqWord16#, 'eqWord16#), + ('GHC.neWord16#, 'neWord16#), + ('GHC.geWord16#, 'geWord16#), + ('GHC.gtWord16#, 'gtWord16#), + ('GHC.leWord16#, 'leWord16#), + ('GHC.ltWord16#, 'ltWord16#), + -- Word32# primitive operations. + ------------------------------ + ('GHC.word32ToWord#, 'word32ToWord#), + ('GHC.word32ToInt32#, 'word32ToInt32#), + ('GHC.plusWord32#, 'plusWord32#), + ('GHC.subWord32#, 'subWord32#), + ('GHC.timesWord32#, 'timesWord32#), + -- , ('GHC.quotWord32#, 'quotWord32#) + -- , ('GHC.remWord32#, 'remWord32#) + -- , ('GHC.quotRemWord32#, 'quotRemWord32#) + ('GHC.andWord32#, 'andWord32#), + ('GHC.orWord32#, 'orWord32#), + ('GHC.xorWord32#, 'xorWord32#), + ('GHC.notWord32#, 'notWord32#), + ('GHC.uncheckedShiftLWord32#, 'uncheckedShiftLWord32#), + ('GHC.uncheckedShiftRLWord32#, 'uncheckedShiftRLWord32#), + ('GHC.eqWord32#, 'eqWord32#), + ('GHC.neWord32#, 'neWord32#), + ('GHC.geWord32#, 'geWord32#), + ('GHC.gtWord32#, 'gtWord32#), + ('GHC.leWord32#, 'leWord32#), + ('GHC.ltWord32#, 'ltWord32#), + -- Word64# primitive operations. + ------------------------------ + ('GHC.word64ToWord#, 'word64ToWord#), + ('GHC.word64ToInt64#, 'word64ToInt64#), + ('GHC.plusWord64#, 'plusWord64#), + ('GHC.subWord64#, 'subWord64#), + ('GHC.timesWord64#, 'timesWord64#), + -- , ('GHC.quotWord64#, 'quotWord64#) + -- , ('GHC.remWord64#, 'remWord64#) + ('GHC.and64#, 'and64#), + ('GHC.or64#, 'or64#), + ('GHC.xor64#, 'xor64#), + ('GHC.not64#, 'not64#), + ('GHC.uncheckedShiftL64#, 'uncheckedShiftL64#), + ('GHC.uncheckedShiftRL64#, 'uncheckedShiftRL64#), + ('GHC.eqWord64#, 'eqWord64#), + ('GHC.neWord64#, 'neWord64#), + ('GHC.geWord64#, 'geWord64#), + ('GHC.gtWord64#, 'gtWord64#), + ('GHC.leWord64#, 'leWord64#), + ('GHC.ltWord64#, 'ltWord64#), + -- Haskell functions without unfoldings. + ---------------------------------------- + -- NOTE: Ideally we would not have these. It's just that GHC tosses + -- their unfolding and we cannot get 'base' to be compiled with the flag + -- 'expose-all-unfoldings' as 'base' is tied to the compiler... + ('GHC.integerFromWord#, 'integerFromWord#), + ('GHC.integerToWord#, 'integerToWord#), + ('GHC.integerFromNatural, 'integerFromNatural), + ('GHC.integerToNatural, 'integerToNatural), + ('GHC.integerToInt#, 'integerToInt#), + ('GHC.integerSub, 'integerSub), + ('GHC.naturalAdd, 'naturalAdd), + ('GHC.naturalSubThrow, 'naturalSubThrow), + ('GHC.noinline, 'noinline), + ('lazy, 'lazyId), + -- compare*# check equality first so bveq can short-circuit, + -- avoiding symbolic branching on the less-than path that would + -- expose ptrEq inside containers' balancing code. + ('GHCClasses.compareInt#, 'compareIntImpl), + ('GHCClasses.compareWord#, 'compareWordImpl), + ('GHC.error, 'errorAxiom), + ('GHC.throw, 'throw), + ('GHC.patError, 'patError'), + ('GHC.withSomeSNat, 'withSomeSNat), + ('GHC.map, 'map), + ('GHC.zip, 'zip) + ] + } type BitVecPW = Pantomime.BitVec Pantomime.PlatformWordSize @@ -391,19 +398,18 @@ type BitVec16 = Pantomime.BitVec 16 type BitVec32 = Pantomime.BitVec 32 type BitVec64 = Pantomime.BitVec 64 - -fromBV - :: forall r n (a :: TYPE r) - . Pantomime.Embeddable (Pantomime.BitVec n) a - => Pantomime.BitVec n - -> a +fromBV :: + forall r n (a :: TYPE r). + (Pantomime.Embeddable (Pantomime.BitVec n) a) => + Pantomime.BitVec n -> + a fromBV = Pantomime.embed -toBV - :: forall r n (a :: TYPE r) - . Pantomime.Embeddable (Pantomime.BitVec n) a - => a - -> Pantomime.BitVec n +toBV :: + forall r n (a :: TYPE r). + (Pantomime.Embeddable (Pantomime.BitVec n) a) => + a -> + Pantomime.BitVec n toBV = Pantomime.project bool2I# :: Pantomime.Bool -> Int# @@ -438,11 +444,11 @@ intToInt32# x = Pantomime.toInt32# $ Pantomime.bvselect @0 $ Pantomime.fromInt# intToInt64# :: Int# -> Int64# intToInt64# x = Pantomime.toInt64# $ Pantomime.bvselect @0 $ Pantomime.fromInt# x -binaryInt# - :: (BitVecPW -> BitVecPW -> BitVecPW) - -> Int# - -> Int# - -> Int# +binaryInt# :: + (BitVecPW -> BitVecPW -> BitVecPW) -> + Int# -> + Int# -> + Int# binaryInt# f lhs rhs = do let lhs' = Pantomime.fromInt# lhs let rhs' = Pantomime.fromInt# rhs @@ -457,15 +463,23 @@ binaryInt# f lhs rhs = do (*#) :: Int# -> Int# -> Int# (*#) = binaryInt# (*) -binaryIntC# - :: (forall n. KnownNat n => Pantomime.BitVec n -> Pantomime.BitVec n -> Pantomime.BitVec n) - -> Int# - -> Int# - -> (# Int#, Int# #) +quotInt# :: Int# -> Int# -> Int# +quotInt# = binaryInt# Pantomime.bvsdiv + +remInt# :: Int# -> Int# -> Int# +remInt# = binaryInt# Pantomime.bvsrem + +binaryIntC# :: + (forall n. (KnownNat n) => Pantomime.BitVec n -> Pantomime.BitVec n -> Pantomime.BitVec n) -> + Int# -> + Int# -> + (# Int#, Int# #) + + binaryIntC# f lhs rhs = do - let project' x - = Pantomime.bvzext @_ @(Pantomime.PlatformWordSize + 1) - $ Pantomime.fromInt# x + let project' x = + Pantomime.bvzext @_ @(Pantomime.PlatformWordSize + 1) $ + Pantomime.fromInt# x let lhs' = project' lhs let rhs' = project' rhs @@ -481,6 +495,24 @@ addIntC# = binaryIntC# Pantomime.bvadd subIntC# :: Int# -> Int# -> (# Int#, Int# #) subIntC# = binaryIntC# \lhs rhs -> Pantomime.bvadd lhs (Pantomime.bvneg rhs) +uncheckedIShiftL# :: Int# -> Int# -> Int# +uncheckedIShiftL# val idx = do + let val' = Pantomime.fromInt# val + idx' = Pantomime.fromInt# idx + Pantomime.toInt# $ Pantomime.bvshl val' idx' + +uncheckedIShiftRA# :: Int# -> Int# -> Int# +uncheckedIShiftRA# val idx = do + let val' = Pantomime.fromInt# val + idx' = Pantomime.fromInt# idx + Pantomime.toInt# $ Pantomime.bvashr val' idx' + +uncheckedIShiftRL# :: Int# -> Int# -> Int# +uncheckedIShiftRL# val idx = do + let val' = Pantomime.fromInt# val + idx' = Pantomime.fromInt# idx + Pantomime.toInt# $ Pantomime.bvlshr val' idx' + andI# :: Int# -> Int# -> Int# andI# = binaryInt# Pantomime.bvand @@ -490,10 +522,10 @@ orI# = binaryInt# Pantomime.bvor xorI# :: Int# -> Int# -> Int# xorI# = binaryInt# Pantomime.bvxor -unaryInt# - :: (BitVecPW -> BitVecPW) - -> Int# - -> Int# +unaryInt# :: + (BitVecPW -> BitVecPW) -> + Int# -> + Int# unaryInt# f x = do let x' = Pantomime.fromInt# x Pantomime.toInt# $ f x' @@ -504,11 +536,11 @@ notI# = unaryInt# Pantomime.bvnot negateInt# :: Int# -> Int# negateInt# = unaryInt# Pantomime.bvneg -compareInt# - :: (BitVecPW -> BitVecPW -> Pantomime.Bool) - -> Int# - -> Int# - -> Int# +compareInt# :: + (BitVecPW -> BitVecPW -> Pantomime.Bool) -> + Int# -> + Int# -> + Int# compareInt# f lhs rhs = do let lhs' = Pantomime.fromInt# lhs let rhs' = Pantomime.fromInt# rhs @@ -538,11 +570,11 @@ int8ToInt# x = Pantomime.toInt# $ Pantomime.bvsext $ Pantomime.fromInt8# x int8ToWord8# :: Int8# -> Word8# int8ToWord8# x = Pantomime.toWord8# $ Pantomime.fromInt8# x -binaryInt8# - :: (BitVec8 -> BitVec8 -> BitVec8) - -> Int8# - -> Int8# - -> Int8# +binaryInt8# :: + (BitVec8 -> BitVec8 -> BitVec8) -> + Int8# -> + Int8# -> + Int8# binaryInt8# f lhs rhs = do let lhs' = Pantomime.fromInt8# lhs let rhs' = Pantomime.fromInt8# rhs @@ -557,10 +589,10 @@ subInt8# = binaryInt8# (-) timesInt8# :: Int8# -> Int8# -> Int8# timesInt8# = binaryInt8# (*) -unaryInt8# - :: (BitVec8 -> BitVec8) - -> Int8# - -> Int8# +unaryInt8# :: + (BitVec8 -> BitVec8) -> + Int8# -> + Int8# unaryInt8# f x = do let x' = Pantomime.fromInt8# x Pantomime.toInt8# $ f x' @@ -568,11 +600,11 @@ unaryInt8# f x = do negateInt8# :: Int8# -> Int8# negateInt8# = unaryInt8# negate -compareInt8# - :: (BitVec8 -> BitVec8 -> Pantomime.Bool) - -> Int8# - -> Int8# - -> Int# +compareInt8# :: + (BitVec8 -> BitVec8 -> Pantomime.Bool) -> + Int8# -> + Int8# -> + Int# compareInt8# f lhs rhs = do let lhs' = Pantomime.fromInt8# lhs let rhs' = Pantomime.fromInt8# rhs @@ -602,11 +634,11 @@ int16ToInt# x = Pantomime.toInt# $ Pantomime.bvsext $ Pantomime.fromInt16# x int16ToWord16# :: Int16# -> Word16# int16ToWord16# x = Pantomime.toWord16# $ Pantomime.fromInt16# x -binaryInt16# - :: (BitVec16 -> BitVec16 -> BitVec16) - -> Int16# - -> Int16# - -> Int16# +binaryInt16# :: + (BitVec16 -> BitVec16 -> BitVec16) -> + Int16# -> + Int16# -> + Int16# binaryInt16# f lhs rhs = do let lhs' = Pantomime.fromInt16# lhs let rhs' = Pantomime.fromInt16# rhs @@ -621,10 +653,10 @@ subInt16# = binaryInt16# (-) timesInt16# :: Int16# -> Int16# -> Int16# timesInt16# = binaryInt16# (*) -unaryInt16# - :: (BitVec16 -> BitVec16) - -> Int16# - -> Int16# +unaryInt16# :: + (BitVec16 -> BitVec16) -> + Int16# -> + Int16# unaryInt16# f x = do let x' = Pantomime.fromInt16# x Pantomime.toInt16# $ f x' @@ -632,11 +664,11 @@ unaryInt16# f x = do negateInt16# :: Int16# -> Int16# negateInt16# = unaryInt16# negate -compareInt16# - :: (BitVec16 -> BitVec16 -> Pantomime.Bool) - -> Int16# - -> Int16# - -> Int# +compareInt16# :: + (BitVec16 -> BitVec16 -> Pantomime.Bool) -> + Int16# -> + Int16# -> + Int# compareInt16# f lhs rhs = do let lhs' = Pantomime.fromInt16# lhs let rhs' = Pantomime.fromInt16# rhs @@ -666,11 +698,11 @@ int32ToInt# x = Pantomime.toInt# $ Pantomime.bvsext $ Pantomime.fromInt32# x int32ToWord32# :: Int32# -> Word32# int32ToWord32# x = Pantomime.toWord32# $ Pantomime.fromInt32# x -binaryInt32# - :: (BitVec32 -> BitVec32 -> BitVec32) - -> Int32# - -> Int32# - -> Int32# +binaryInt32# :: + (BitVec32 -> BitVec32 -> BitVec32) -> + Int32# -> + Int32# -> + Int32# binaryInt32# f lhs rhs = do let lhs' = Pantomime.fromInt32# lhs let rhs' = Pantomime.fromInt32# rhs @@ -685,10 +717,10 @@ subInt32# = binaryInt32# (-) timesInt32# :: Int32# -> Int32# -> Int32# timesInt32# = binaryInt32# (*) -unaryInt32# - :: (BitVec32 -> BitVec32) - -> Int32# - -> Int32# +unaryInt32# :: + (BitVec32 -> BitVec32) -> + Int32# -> + Int32# unaryInt32# f x = do let x' = Pantomime.fromInt32# x Pantomime.toInt32# $ f x' @@ -696,11 +728,11 @@ unaryInt32# f x = do negateInt32# :: Int32# -> Int32# negateInt32# = unaryInt32# negate -compareInt32# - :: (BitVec32 -> BitVec32 -> Pantomime.Bool) - -> Int32# - -> Int32# - -> Int# +compareInt32# :: + (BitVec32 -> BitVec32 -> Pantomime.Bool) -> + Int32# -> + Int32# -> + Int# compareInt32# f lhs rhs = do let lhs' = Pantomime.fromInt32# lhs let rhs' = Pantomime.fromInt32# rhs @@ -730,11 +762,11 @@ int64ToInt# x = Pantomime.toInt# $ Pantomime.bvsext $ Pantomime.fromInt64# x int64ToWord64# :: Int64# -> Word64# int64ToWord64# x = Pantomime.toWord64# $ Pantomime.fromInt64# x -binaryInt64# - :: (BitVec64 -> BitVec64 -> BitVec64) - -> Int64# - -> Int64# - -> Int64# +binaryInt64# :: + (BitVec64 -> BitVec64 -> BitVec64) -> + Int64# -> + Int64# -> + Int64# binaryInt64# f lhs rhs = do let lhs' = Pantomime.fromInt64# lhs let rhs' = Pantomime.fromInt64# rhs @@ -749,10 +781,10 @@ subInt64# = binaryInt64# (-) timesInt64# :: Int64# -> Int64# -> Int64# timesInt64# = binaryInt64# (*) -unaryInt64# - :: (BitVec64 -> BitVec64) - -> Int64# - -> Int64# +unaryInt64# :: + (BitVec64 -> BitVec64) -> + Int64# -> + Int64# unaryInt64# f x = do let x' = Pantomime.fromInt64# x Pantomime.toInt64# $ f x' @@ -760,11 +792,11 @@ unaryInt64# f x = do negateInt64# :: Int64# -> Int64# negateInt64# = unaryInt64# negate -compareInt64# - :: (BitVec64 -> BitVec64 -> Pantomime.Bool) - -> Int64# - -> Int64# - -> Int# +compareInt64# :: + (BitVec64 -> BitVec64 -> Pantomime.Bool) -> + Int64# -> + Int64# -> + Int# compareInt64# f lhs rhs = do let lhs' = Pantomime.fromInt64# lhs let rhs' = Pantomime.fromInt64# rhs @@ -803,11 +835,11 @@ wordToWord32# x = Pantomime.toWord32# $ Pantomime.bvselect @0 $ Pantomime.fromWo wordToWord64# :: Word# -> Word64# wordToWord64# x = Pantomime.toWord64# $ Pantomime.bvselect @0 $ Pantomime.fromWord# x -binaryWord# - :: (BitVecPW -> BitVecPW -> BitVecPW) - -> Word# - -> Word# - -> Word# +binaryWord# :: + (BitVecPW -> BitVecPW -> BitVecPW) -> + Word# -> + Word# -> + Word# binaryWord# f lhs rhs = do let lhs' = Pantomime.fromWord# lhs let rhs' = Pantomime.fromWord# rhs @@ -822,15 +854,15 @@ minusWord# = binaryWord# (-) timesWord# :: Word# -> Word# -> Word# timesWord# = binaryWord# (*) -binaryWordC# - :: (forall n. KnownNat n => Pantomime.BitVec n -> Pantomime.BitVec n -> Pantomime.BitVec n) - -> Word# - -> Word# - -> (# Word#, Int# #) +binaryWordC# :: + (forall n. (KnownNat n) => Pantomime.BitVec n -> Pantomime.BitVec n -> Pantomime.BitVec n) -> + Word# -> + Word# -> + (# Word#, Int# #) binaryWordC# f lhs rhs = do - let project' x - = Pantomime.bvzext @_ @(Pantomime.PlatformWordSize + 1) - $ Pantomime.fromWord# x + let project' x = + Pantomime.bvzext @_ @(Pantomime.PlatformWordSize + 1) $ + Pantomime.fromWord# x let lhs' = project' lhs let rhs' = project' rhs @@ -875,11 +907,11 @@ uncheckedShiftRL# val idx = do let idx' = Pantomime.fromInt# idx Pantomime.toWord# $ Pantomime.bvlshr val' idx' -compareWord# - :: (BitVecPW -> BitVecPW -> Pantomime.Bool) - -> Word# - -> Word# - -> Int# +compareWord# :: + (BitVecPW -> BitVecPW -> Pantomime.Bool) -> + Word# -> + Word# -> + Int# compareWord# f lhs rhs = do let lhs' = Pantomime.fromWord# lhs let rhs' = Pantomime.fromWord# rhs @@ -903,17 +935,52 @@ leWord# = compareWord# Pantomime.bvule ltWord# :: Word# -> Word# -> Int# ltWord# = compareWord# Pantomime.bvult +compareAddr# :: + (BitVecPW -> BitVecPW -> Pantomime.Bool) -> + Addr# -> + Addr# -> + Int# +compareAddr# f lhs rhs = do + let lhs' = Pantomime.fromWord# (unsafeCoerce# lhs :: Word#) + let rhs' = Pantomime.fromWord# (unsafeCoerce# rhs :: Word#) + bool2I# $ f lhs' rhs' + + +ltAddr# :: Addr# -> Addr# -> Int# +ltAddr# = compareAddr# Pantomime.bvult + +leAddr# :: Addr# -> Addr# -> Int# +leAddr# = compareAddr# Pantomime.bvule + +gtAddr# :: Addr# -> Addr# -> Int# +gtAddr# = compareAddr# $ flip Pantomime.bvult + +geAddr# :: Addr# -> Addr# -> Int# +geAddr# = compareAddr# $ flip Pantomime.bvule + +eqAddr# :: Addr# -> Addr# -> Int# +eqAddr# = compareAddr# Pantomime.bveq + +neAddr# :: Addr# -> Addr# -> Int# +neAddr# = compareAddr# Pantomime.bvneq + +minusAddr# :: Addr# -> Addr# -> Int# +minusAddr# lhs rhs = do + let lhs' = Pantomime.fromWord# (unsafeCoerce# lhs :: Word#) + let rhs' = Pantomime.fromWord# (unsafeCoerce# rhs :: Word#) + Pantomime.toInt# $ Pantomime.bvadd lhs' (Pantomime.bvneg rhs') + word8ToWord# :: Word8# -> Word# word8ToWord# x = Pantomime.toWord# $ Pantomime.bvzext $ Pantomime.fromWord8# x word8ToInt8# :: Word8# -> Int8# word8ToInt8# x = Pantomime.toInt8# $ Pantomime.fromWord8# x -binaryWord8# - :: (BitVec8 -> BitVec8 -> BitVec8) - -> Word8# - -> Word8# - -> Word8# +binaryWord8# :: + (BitVec8 -> BitVec8 -> BitVec8) -> + Word8# -> + Word8# -> + Word8# binaryWord8# f lhs rhs = do let lhs' = Pantomime.fromWord8# lhs let rhs' = Pantomime.fromWord8# rhs @@ -940,11 +1007,23 @@ xorWord8# = binaryWord8# Pantomime.bvxor notWord8# :: Word8# -> Word8# notWord8# x = Pantomime.toWord8# $ Pantomime.bvnot $ Pantomime.fromWord8# x -compareWord8# - :: (BitVec8 -> BitVec8 -> Pantomime.Bool) - -> Word8# - -> Word8# - -> Int# +uncheckedShiftLWord8# :: Word8# -> Int# -> Word8# +uncheckedShiftLWord8# val idx = do + let val' = Pantomime.fromWord8# val + let idx' = Pantomime.bvsresize @Pantomime.PlatformWordSize @8 $ Pantomime.fromInt# idx + Pantomime.toWord8# $ Pantomime.bvshl val' idx' + +uncheckedShiftRLWord8# :: Word8# -> Int# -> Word8# +uncheckedShiftRLWord8# val idx = do + let val' = Pantomime.fromWord8# val + let idx' = Pantomime.bvsresize @Pantomime.PlatformWordSize @8 $ Pantomime.fromInt# idx + Pantomime.toWord8# $ Pantomime.bvlshr val' idx' + +compareWord8# :: + (BitVec8 -> BitVec8 -> Pantomime.Bool) -> + Word8# -> + Word8# -> + Int# compareWord8# f lhs rhs = do let lhs' = Pantomime.fromWord8# lhs let rhs' = Pantomime.fromWord8# rhs @@ -974,11 +1053,11 @@ word16ToWord# x = Pantomime.toWord# $ Pantomime.bvzext $ Pantomime.fromWord16# x word16ToInt16# :: Word16# -> Int16# word16ToInt16# x = Pantomime.toInt16# $ Pantomime.fromWord16# x -binaryWord16# - :: (BitVec16 -> BitVec16 -> BitVec16) - -> Word16# - -> Word16# - -> Word16# +binaryWord16# :: + (BitVec16 -> BitVec16 -> BitVec16) -> + Word16# -> + Word16# -> + Word16# binaryWord16# f lhs rhs = do let lhs' = Pantomime.fromWord16# lhs let rhs' = Pantomime.fromWord16# rhs @@ -1005,11 +1084,11 @@ xorWord16# = binaryWord16# Pantomime.bvxor notWord16# :: Word16# -> Word16# notWord16# x = Pantomime.toWord16# $ Pantomime.bvnot $ Pantomime.fromWord16# x -compareWord16# - :: (BitVec16 -> BitVec16 -> Pantomime.Bool) - -> Word16# - -> Word16# - -> Int# +compareWord16# :: + (BitVec16 -> BitVec16 -> Pantomime.Bool) -> + Word16# -> + Word16# -> + Int# compareWord16# f lhs rhs = do let lhs' = Pantomime.fromWord16# lhs let rhs' = Pantomime.fromWord16# rhs @@ -1039,11 +1118,11 @@ word32ToWord# x = Pantomime.toWord# $ Pantomime.bvzext $ Pantomime.fromWord32# x word32ToInt32# :: Word32# -> Int32# word32ToInt32# x = Pantomime.toInt32# $ Pantomime.fromWord32# x -binaryWord32# - :: (BitVec32 -> BitVec32 -> BitVec32) - -> Word32# - -> Word32# - -> Word32# +binaryWord32# :: + (BitVec32 -> BitVec32 -> BitVec32) -> + Word32# -> + Word32# -> + Word32# binaryWord32# f lhs rhs = do let lhs' = Pantomime.fromWord32# lhs let rhs' = Pantomime.fromWord32# rhs @@ -1070,11 +1149,23 @@ xorWord32# = binaryWord32# Pantomime.bvxor notWord32# :: Word32# -> Word32# notWord32# x = Pantomime.toWord32# $ Pantomime.bvnot $ Pantomime.fromWord32# x -compareWord32# - :: (BitVec32 -> BitVec32 -> Pantomime.Bool) - -> Word32# - -> Word32# - -> Int# +uncheckedShiftLWord32# :: Word32# -> Int# -> Word32# +uncheckedShiftLWord32# val idx = do + let val' = Pantomime.fromWord32# val + let idx' = Pantomime.bvsresize @Pantomime.PlatformWordSize @32 $ Pantomime.fromInt# idx + Pantomime.toWord32# $ Pantomime.bvshl val' idx' + +uncheckedShiftRLWord32# :: Word32# -> Int# -> Word32# +uncheckedShiftRLWord32# val idx = do + let val' = Pantomime.fromWord32# val + let idx' = Pantomime.bvsresize @Pantomime.PlatformWordSize @32 $ Pantomime.fromInt# idx + Pantomime.toWord32# $ Pantomime.bvlshr val' idx' + +compareWord32# :: + (BitVec32 -> BitVec32 -> Pantomime.Bool) -> + Word32# -> + Word32# -> + Int# compareWord32# f lhs rhs = do let lhs' = Pantomime.fromWord32# lhs let rhs' = Pantomime.fromWord32# rhs @@ -1104,11 +1195,11 @@ word64ToWord# x = Pantomime.toWord# $ Pantomime.bvzext $ Pantomime.fromWord64# x word64ToInt64# :: Word64# -> Int64# word64ToInt64# x = Pantomime.toInt64# $ Pantomime.fromWord64# x -binaryWord64# - :: (BitVec64 -> BitVec64 -> BitVec64) - -> Word64# - -> Word64# - -> Word64# +binaryWord64# :: + (BitVec64 -> BitVec64 -> BitVec64) -> + Word64# -> + Word64# -> + Word64# binaryWord64# f lhs rhs = do let lhs' = Pantomime.fromWord64# lhs let rhs' = Pantomime.fromWord64# rhs @@ -1135,11 +1226,23 @@ xor64# = binaryWord64# Pantomime.bvxor not64# :: Word64# -> Word64# not64# x = Pantomime.toWord64# $ Pantomime.bvnot $ Pantomime.fromWord64# x -compareWord64# - :: (BitVec64 -> BitVec64 -> Pantomime.Bool) - -> Word64# - -> Word64# - -> Int# +uncheckedShiftL64# :: Word64# -> Int# -> Word64# +uncheckedShiftL64# val idx = do + let val' = Pantomime.fromWord64# val + let idx' = Pantomime.bvsresize @Pantomime.PlatformWordSize @64 $ Pantomime.fromInt# idx + Pantomime.toWord64# $ Pantomime.bvshl val' idx' + +uncheckedShiftRL64# :: Word64# -> Int# -> Word64# +uncheckedShiftRL64# val idx = do + let val' = Pantomime.fromWord64# val + let idx' = Pantomime.bvsresize @Pantomime.PlatformWordSize @64 $ Pantomime.fromInt# idx + Pantomime.toWord64# $ Pantomime.bvlshr val' idx' + +compareWord64# :: + (BitVec64 -> BitVec64 -> Pantomime.Bool) -> + Word64# -> + Word64# -> + Int# compareWord64# f lhs rhs = do let lhs' = Pantomime.fromWord64# lhs let rhs' = Pantomime.fromWord64# rhs @@ -1181,8 +1284,8 @@ toInteger x = do | x < minI -> undefined | maxI < x -> undefined | otherwise -> do - let x' = Pantomime.i2bv @Pantomime.PlatformWordSize x - IS $ Pantomime.toInt# x' + let x' = Pantomime.i2bv @Pantomime.PlatformWordSize x + IS $ Pantomime.toInt# x' -- TODO: The below definitions exists solely because the unfolding doesn't -- exist. There should be a way around this... @@ -1201,10 +1304,12 @@ integerToNatural = \case IN x -> GHC.naturalFromBigNat# x integerFromWord# :: Word# -> Integer -integerFromWord# w = if - | let i = GHC.word2Int# w - , GHC.isTrue# (i GHC.>=# 0#) -> IS i - | otherwise -> IP (GHC.bigNatFromWord# w) +integerFromWord# w = + if + | let i = GHC.word2Int# w, + GHC.isTrue# (i GHC.>=# 0#) -> + IS i + | otherwise -> IP (GHC.bigNatFromWord# w) integerToInt# :: Integer -> Int# integerToInt# = \case @@ -1219,48 +1324,48 @@ integerToWord# = \case IN bn -> GHC.int2Word# $ GHC.negateInt# $ GHC.word2Int# $ GHC.bigNatToWord# bn integerSub :: Integer -> Integer -> Integer -integerSub !x (IS 0#) = x -- Note [Bangs in Integer functions] -integerSub (IS x#) (IS y#) - = case GHC.subIntC# x# y# of +integerSub !x (IS 0#) = x -- Note [Bangs in Integer functions] +integerSub (IS x#) (IS y#) = + case GHC.subIntC# x# y# of (# z#, 0# #) -> IS z# - (# 0#, _ #) -> IN (GHC.bigNatFromWord2# 1## 0##) - (# z#, _ #) - | GHC.isTrue# (z# GHC.># 0#) - -> IN (GHC.bigNatFromWord# (GHC.int2Word# (GHC.negateInt# z#))) - | True - -> IP (GHC.bigNatFromWord# (GHC.int2Word# z#)) + (# 0#, _ #) -> IN (GHC.bigNatFromWord2# 1## 0##) + (# z#, _ #) + | GHC.isTrue# (z# GHC.># 0#) -> + IN (GHC.bigNatFromWord# (GHC.int2Word# (GHC.negateInt# z#))) + | True -> + IP (GHC.bigNatFromWord# (GHC.int2Word# z#)) integerSub (IS x#) (IP y) - | GHC.isTrue# (x# GHC.>=# 0#) - = GHC.integerFromBigNatNeg# (GHC.bigNatSubWordUnsafe# y (GHC.int2Word# x#)) - | otherwise - = IN (GHC.bigNatAddWord# y (GHC.int2Word# (GHC.negateInt# x#))) + | GHC.isTrue# (x# GHC.>=# 0#) = + GHC.integerFromBigNatNeg# (GHC.bigNatSubWordUnsafe# y (GHC.int2Word# x#)) + | otherwise = + IN (GHC.bigNatAddWord# y (GHC.int2Word# (GHC.negateInt# x#))) integerSub (IS x#) (IN y) - | GHC.isTrue# (x# GHC.>=# 0#) - = IP (GHC.bigNatAddWord# y (GHC.int2Word# x#)) - | otherwise - = GHC.integerFromBigNat# (GHC.bigNatSubWordUnsafe# y (GHC.int2Word# (GHC.negateInt# x#))) -integerSub (IP x) (IP y) - = case GHC.bigNatCompare x y of + | GHC.isTrue# (x# GHC.>=# 0#) = + IP (GHC.bigNatAddWord# y (GHC.int2Word# x#)) + | otherwise = + GHC.integerFromBigNat# (GHC.bigNatSubWordUnsafe# y (GHC.int2Word# (GHC.negateInt# x#))) +integerSub (IP x) (IP y) = + case GHC.bigNatCompare x y of LT -> GHC.integerFromBigNatNeg# (GHC.bigNatSubUnsafe y x) EQ -> IS 0# GT -> GHC.integerFromBigNat# (GHC.bigNatSubUnsafe x y) integerSub (IP x) (IN y) = IP (GHC.bigNatAdd x y) integerSub (IN x) (IP y) = IN (GHC.bigNatAdd x y) -integerSub (IN x) (IN y) - = case GHC.bigNatCompare x y of +integerSub (IN x) (IN y) = + case GHC.bigNatCompare x y of LT -> GHC.integerFromBigNat# (GHC.bigNatSubUnsafe y x) EQ -> IS 0# GT -> GHC.integerFromBigNatNeg# (GHC.bigNatSubUnsafe x y) integerSub (IP x) (IS y#) - | GHC.isTrue# (y# GHC.>=# 0#) - = GHC.integerFromBigNat# (GHC.bigNatSubWordUnsafe# x (GHC.int2Word# y#)) - | otherwise - = IP (GHC.bigNatAddWord# x (GHC.int2Word# (GHC.negateInt# y#))) + | GHC.isTrue# (y# GHC.>=# 0#) = + GHC.integerFromBigNat# (GHC.bigNatSubWordUnsafe# x (GHC.int2Word# y#)) + | otherwise = + IP (GHC.bigNatAddWord# x (GHC.int2Word# (GHC.negateInt# y#))) integerSub (IN x) (IS y#) - | GHC.isTrue# (y# GHC.>=# 0#) - = IN (GHC.bigNatAddWord# x (GHC.int2Word# y#)) - | otherwise - = GHC.integerFromBigNatNeg# (GHC.bigNatSubWordUnsafe# x (GHC.int2Word# (GHC.negateInt# y#))) + | GHC.isTrue# (y# GHC.>=# 0#) = + IN (GHC.bigNatAddWord# x (GHC.int2Word# y#)) + | otherwise = + GHC.integerFromBigNatNeg# (GHC.bigNatSubWordUnsafe# x (GHC.int2Word# (GHC.negateInt# y#))) naturalAdd :: Natural -> Natural -> Natural naturalAdd = \cases @@ -1269,21 +1374,37 @@ naturalAdd = \cases (NB x) (NB y) -> NB $ GHC.bigNatAdd x y (NS x) (NS y) -> case GHC.addWordC# x y of (# l, 0# #) -> NS l - (# l, c #) -> NB $ GHC.bigNatFromWord2# (GHC.int2Word# c) l + (# l, c #) -> NB $ GHC.bigNatFromWord2# (GHC.int2Word# c) l naturalSubThrow :: Natural -> Natural -> Natural naturalSubThrow (NS _) (NB _) = GHC.raiseUnderflow naturalSubThrow (NB x) (NS y) = GHC.naturalFromBigNat# $ GHC.bigNatSubWordUnsafe# x y naturalSubThrow (NS x) (NS y) = case GHC.subWordC# x y of (# l, 0# #) -> NS l - (# _, _ #) -> GHC.raiseUnderflow + (# _, _ #) -> GHC.raiseUnderflow naturalSubThrow (NB x) (NB y) = case GHC.bigNatSub x y of - (# (# #) | #) -> GHC.raiseUnderflow - (# | z #) -> GHC.naturalFromBigNat# z + (# (# #) | #) -> GHC.raiseUnderflow + (# | z #) -> GHC.naturalFromBigNat# z noinline :: a -> a noinline = id +lazyId :: a -> a +lazyId = id + +compareIntImpl :: Int# -> Int# -> Ordering +compareIntImpl x y = + if GHC.isTrue# (x ==# y) then EQ + else if GHC.isTrue# (x <# y) then LT + else GT + +compareWordImpl :: Word# -> Word# -> Ordering +compareWordImpl x y = + if GHC.isTrue# (eqWord# x y) then EQ + else if GHC.isTrue# (ltWord# x y) then LT + else GT + + -- FIXME: This is not actually the implementation for 'undefined'. undefined :: a undefined = GHC.raise# () @@ -1292,15 +1413,19 @@ undefined = GHC.raise# () throw :: forall rep (a :: TYPE rep) e. e -> a throw = GHC.raise# () +-- | Axiom for 'error' (HasCallStack => [Char] -> a). +errorAxiom :: forall rep (a :: TYPE rep). HasCallStack => [Char] -> a +errorAxiom _ = GHC.raise# () + -- FIXME: This is not actually the implementation for 'patError'. patError' :: forall q (a :: TYPE q). Addr# -> a patError' _ = GHC.raise# () -withSomeSNat - :: forall rep (r :: TYPE rep) - . Natural - -> (forall n. SNat n -> r) - -> r +withSomeSNat :: + forall rep (r :: TYPE rep). + Natural -> + (forall n. SNat n -> r) -> + r withSomeSNat n f = f $ unsafeSNat n map :: (a -> b) -> [a] -> [b] diff --git a/src/Pantomime/IO.hs b/src/Pantomime/IO.hs new file mode 100644 index 0000000..a27e444 --- /dev/null +++ b/src/Pantomime/IO.hs @@ -0,0 +1,163 @@ +{-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE UnboxedTuples #-} + +module Pantomime.IO + ( ioAxioms, + FakeWorld (..), + FakeIO (..), + FakeIORef (..), + FakeState (..), + nextWorld, + unsafePerformIOAxiom, + append, + updateAt, + ) +where + +import Data.Coerce (Coercible, coerce) +import Data.IORef (IORef, newIORef, readIORef, writeIORef) +import GHC.Base (Any, RealWorld, bindIO, returnIO) +import GHC.Exts (IsList (..)) +import GHC.Prim (State#) +import GHC.Internal.Base (RuntimeRep) +import GHC.Internal.Base qualified as GHC.Internal.Base +import GHC.Internal.IO qualified as GHC.Internal.IO +import GHC.Internal.IO.Unsafe qualified as GHC.Internal.IO.Unsafe +import GHC.IO qualified as GHC.IO +import GHC.IO.Unsafe qualified as GHC.IO.Unsafe +import Pantomime (PluginAxioms (..)) +import Pantomime.BuiltIn qualified as Pantomime +import System.IO.Unsafe (unsafePerformIO) +import Unsafe.Coerce (unsafeCoerce) + +ioAxioms :: PluginAxioms +ioAxioms = + PluginAxioms + { typeAxioms = + fromList + [ (''RealWorld, ''FakeWorld), + (''State#, ''FakeState), + (''IO, ''FakeIO), + (''IORef, ''FakeIORef) + ], + termAxioms = + [ ('unsafePerformIO, 'unsafePerformIOAxiom), + ('GHC.IO.unsafePerformIO, 'unsafePerformIOAxiom), + ('GHC.IO.Unsafe.unsafePerformIO, 'unsafePerformIOAxiom), + ('GHC.Internal.IO.unsafePerformIO, 'unsafePerformIOAxiom), + ('GHC.Internal.IO.Unsafe.unsafePerformIO, 'unsafePerformIOAxiom), + ('returnIO, 'returnIOAxiom), + ('GHC.Internal.Base.returnIO, 'returnIOAxiom), + ('bindIO, 'bindIOAxiom), + ('GHC.Internal.Base.bindIO, 'bindIOAxiom), + ('newIORef, 'newIORefAxiom), + ('readIORef, 'readIORefAxiom), + ('writeIORef, 'writeIORefAxiom) + ] + } + +data FakeIORef a = FakeIORef + { refID :: Pantomime.Integer + , value :: a + } + +data FakeWorld = FakeWorld + { time :: Pantomime.Integer + , refs :: [Any] + } + +newtype FakeIO a = FakeIO (FakeWorld -> (# FakeWorld, a #)) + +-- | Symbolic representation of 'State# s'. The phantom type argument +-- preserves the kind structure of 'State#'. The actual state is always +-- a 'FakeWorld' — the phantom just keeps the kinds consistent. +type role FakeState phantom +data FakeState (s :: RuntimeRep) = FakeState FakeWorld + +nextWorld :: FakeWorld -> FakeWorld +nextWorld wrld@(FakeWorld {..}) = wrld {time = time + 1} + +unsafePerformIOAxiom + :: forall io a + . Coercible FakeIO io + => io a + -> a +unsafePerformIOAxiom m = case coerce m of FakeIO f -> case f newWorld of (# _, a #) -> a + where + newWorld = FakeWorld + { time = 0 + , refs = [] + } + +returnIOAxiom + :: forall io a + . Coercible FakeIO io + => a -> io a +returnIOAxiom a = coerce (FakeIO $ \s -> (# nextWorld s, a #)) + +bindIOAxiom + :: forall io a b + . Coercible FakeIO io + => io a -> (a -> io b) -> io b +bindIOAxiom m k = coerce (bindFakeIO (coerce m :: FakeIO a) (\x -> coerce (k x) :: FakeIO b)) + where + bindFakeIO :: FakeIO a -> (a -> FakeIO b) -> FakeIO b + bindFakeIO (FakeIO f) g = FakeIO $ \s -> case f s of + (# s', a #) -> case g a of + FakeIO n -> n s' + +newIORefAxiom + :: forall a io ioref + . Coercible FakeIO io + => Coercible FakeIORef ioref + => a -> io (ioref a) +newIORefAxiom a = + let f :: FakeWorld -> (# FakeWorld, FakeIORef a #) + f s = let s' = s { time = time s + 1, refs = append (refs s) [unsafeCoerce a] } + ref = FakeIORef { refID = time s, value = a } + in (# s', ref #) + m :: io (FakeIORef a) + m = coerce (FakeIO f) + in coerce m + +readIORefAxiom + :: forall a io ioref + . Coercible FakeIO io + => Coercible FakeIORef ioref + => ioref a -> io a +readIORefAxiom ref = + let ref' :: FakeIORef a + ref' = coerce ref + f :: FakeWorld -> (# FakeWorld, a #) + f s = let FakeIORef { refID } = ref' + idx = fromIntegral (Pantomime.toInteger refID) + val = unsafeCoerce (refs s !! idx) + in (# nextWorld s, val #) + in coerce (FakeIO f) + +writeIORefAxiom + :: forall a io ioref + . Coercible FakeIO io + => Coercible FakeIORef ioref + => ioref a -> a -> io () +writeIORefAxiom ref a = + let ref' :: FakeIORef a + ref' = coerce ref + f :: FakeWorld -> (# FakeWorld, () #) + f s = let FakeIORef { refID } = ref' + idx = fromIntegral (Pantomime.toInteger refID) + s' = s { refs = updateAt idx (unsafeCoerce a) (refs s) } + in (# nextWorld s', () #) + in coerce (FakeIO f) + + + +append :: [a] -> [a] -> [a] +append [] ys = ys +append (x : xs) ys = x : append xs ys + +updateAt :: Int -> a -> [a] -> [a] +updateAt 0 y (_ : xs) = y : xs +updateAt n y (x : xs) = x : updateAt (n - 1) y xs +updateAt _ _ [] = [] diff --git a/src/Pantomime/Ptr.hs b/src/Pantomime/Ptr.hs new file mode 100644 index 0000000..842ab0b --- /dev/null +++ b/src/Pantomime/Ptr.hs @@ -0,0 +1,227 @@ +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE UnboxedTuples #-} + +module Pantomime.Ptr + ( ptrAxioms, + FakePtr (..), + FakeForeignPtr (..), + mallocByteStringAxiom, + withForeignPtrAxiom, + plusPtrAxiom, + peekByte, + pokeByte, + peekByteAxiom, + pokeByteAxiom, + mallocByteStringN, + withForeignPtrN, + plusPtrN, + castPtrN, + ) +where +import Data.ByteString.Internal (mallocByteString) +import Data.Coerce (Coercible, coerce) +import GHC.ForeignPtr (mallocPlainForeignPtrBytes) +import GHC.Word (Word8 (..), Word32 (..)) +import Foreign.ForeignPtr (ForeignPtr, mallocForeignPtrBytes, withForeignPtr) +import Foreign.Ptr (Ptr, castPtr, minusPtr, plusPtr) +import GHC.Base (Int (I#)) +import GHC.Exts (IsList (..)) +import Pantomime (PluginAxioms (..)) +import Pantomime.BuiltIn qualified as Pantomime +import Pantomime.IO + ( FakeIO (..), + FakeWorld (..), + nextWorld, + append, + updateAt, + ) +import Unsafe.Coerce (unsafeCoerce) + +-- | Word-sized bitvector, matching 'Int'/'Word' on the platform. +type PtrWord = Pantomime.BitVec Pantomime.PlatformWordSize + +-- | A fake pointer: (id, length, offset). The phantom @a@ carries the element +-- type, matching 'Ptr's phantom role. Fields are word-sized bitvectors to +-- match 'Int' arithmetic and avoid cross-theory SMT conversions. +data FakePtr a = FakePtr + { ptrOff :: PtrWord + , ptrId :: PtrWord + , ptrLen :: PtrWord + } + +-- | A fake foreign pointer: (id, length). No offset until 'withForeignPtr' +-- materializes a 'FakePtr'. +data FakeForeignPtr a = FakeForeignPtr + { fptrId :: PtrWord + , fptrLen :: PtrWord + } + +ptrAxioms :: PluginAxioms +ptrAxioms = + PluginAxioms + { typeAxioms = + fromList + [ (''Ptr, ''FakePtr), + (''ForeignPtr, ''FakeForeignPtr) + ], + termAxioms = + [ ('plusPtr, 'plusPtrAxiom), + ('plusPtrN, 'plusPtrAxiom), + ('minusPtr, 'minusPtrAxiom), + ('castPtr, 'castPtrAxiom), + ('castPtrN, 'castPtrAxiom), + ('mallocByteStringN, 'mallocByteStringAxiom), + ('mallocPlainForeignPtrBytes, 'mallocByteStringAxiom), + ('withForeignPtrN, 'withForeignPtrAxiom), + ('withForeignPtr, 'withForeignPtrAxiom), + ('peekByte, 'peekByteAxiom), + ('pokeByte, 'pokeByteAxiom) + ] + } + +-- | plusPtr :: Ptr a -> Int -> Ptr b +-- Bump the offset by n. Pure (no IO). +plusPtrAxiom + :: forall a b ptr + . Coercible FakePtr ptr + => ptr a + -> Int + -> ptr b +plusPtrAxiom p n = + let FakePtr {ptrId, ptrLen, ptrOff} = coerce p :: FakePtr a + n' = Pantomime.fromInt# (case n of I# i# -> i#) + result = FakePtr {ptrId, ptrLen, ptrOff = ptrOff + n'} :: FakePtr b + in coerce result + +-- | minusPtr :: Ptr a -> Ptr b -> Int +-- Offset difference. Pure. +minusPtrAxiom + :: forall a b ptr + . Coercible FakePtr ptr + => ptr a + -> ptr b + -> Int +minusPtrAxiom p1 p2 = + let FakePtr {ptrOff = o1} = coerce p1 :: FakePtr a + FakePtr {ptrOff = o2} = coerce p2 :: FakePtr b + diff = o1 - o2 + in I# (Pantomime.toInt# diff) + +-- | castPtr :: Ptr a -> Ptr b +-- Retype the phantom; no runtime change. +castPtrAxiom + :: forall a b ptr + . Coercible FakePtr ptr + => ptr a + -> ptr b +castPtrAxiom p = + let fake = coerce p :: FakePtr a + in coerce (unsafeCoerce fake :: FakePtr b) + +-- | mallocByteString :: Int -> IO (ForeignPtr a) +-- Allocate a fresh, zero-initialized byte array; return a fake foreign pointer. +mallocByteStringAxiom + :: forall a io fptr + . Coercible FakeIO io + => Coercible FakeForeignPtr fptr + => Int + -> io (fptr a) +mallocByteStringAxiom n = + let f :: FakeWorld -> (# FakeWorld, FakeForeignPtr a #) + f s = + let newId = time s + zeroByte = 0 :: Pantomime.BitVec 8 + arr = Pantomime.aconst @Pantomime.Integer @(Pantomime.BitVec 8) zeroByte + s' = s {time = newId + 1, refs = append (refs s) [unsafeCoerce arr]} + fptr = FakeForeignPtr + { fptrId = Pantomime.i2bv @Pantomime.PlatformWordSize newId + , fptrLen = Pantomime.fromInt# (case n of I# i# -> i#) + } + in (# s', fptr #) + m :: io (FakeForeignPtr a) + m = coerce (FakeIO f) + in coerce m + +-- | withForeignPtr :: ForeignPtr a -> (Ptr a -> IO b) -> IO b +-- Materialize a fake pointer at offset 0 with the full length, run the +-- callback in the same FakeIO so ref effects thread through. +withForeignPtrAxiom + :: forall a b io + . Coercible FakeIO io + => ForeignPtr a + -> (Ptr a -> io b) + -> io b +withForeignPtrAxiom fp k = + let f :: FakeWorld -> (# FakeWorld, b #) + f s = + let FakeForeignPtr {fptrId, fptrLen} = unsafeCoerce fp :: FakeForeignPtr a + fakePtr = FakePtr {ptrId = fptrId, ptrLen = fptrLen, ptrOff = 0} :: FakePtr a + realPtr = unsafeCoerce fakePtr :: Ptr a + FakeIO g = coerce (k realPtr) :: FakeIO b + in g s + in coerce (FakeIO f) + +{-# NOINLINE mallocByteStringN #-} +mallocByteStringN :: Int -> IO (ForeignPtr a) +mallocByteStringN = mallocByteString + +{-# NOINLINE withForeignPtrN #-} +withForeignPtrN :: ForeignPtr a -> (Ptr a -> IO b) -> IO b +withForeignPtrN = withForeignPtr + +{-# NOINLINE plusPtrN #-} +plusPtrN :: Ptr a -> Int -> Ptr b +plusPtrN = plusPtr + +{-# NOINLINE castPtrN #-} +castPtrN :: Ptr a -> Ptr b +castPtrN = castPtr + +{-# NOINLINE peekByte #-} +peekByte :: Ptr Word8 -> IO Word8 +peekByte = error "peekByte: axiom not resolved" + +{-# NOINLINE pokeByte #-} +pokeByte :: Ptr Word8 -> Word8 -> IO () +pokeByte = error "pokeByte: axiom not resolved" + +-- | peekByte :: Ptr Word8 -> IO Word8 +-- Read a single byte from the pointer's backing array at the pointer's offset. +peekByteAxiom + :: forall ptr io + . Coercible FakePtr ptr + => Coercible FakeIO io + => ptr Word8 + -> io Word8 +peekByteAxiom p = + let f :: FakeWorld -> (# FakeWorld, Word8 #) + f s = + let FakePtr {ptrId, ptrOff} = coerce p :: FakePtr Word8 + idx = fromIntegral (Pantomime.toInteger (Pantomime.bvu2i ptrId)) + arr = unsafeCoerce (refs s !! idx) :: Pantomime.Array Pantomime.Integer (Pantomime.BitVec 8) + val = Pantomime.aselect @Pantomime.Integer @(Pantomime.BitVec 8) arr (Pantomime.bvu2i ptrOff) + in (# nextWorld s, W8# (Pantomime.toWord8# val) #) + m :: io Word8 + m = coerce (FakeIO f) + in coerce m + +-- | pokeByte :: Ptr Word8 -> Word8 -> IO () +pokeByteAxiom + :: forall ptr io + . Coercible FakePtr ptr + => Coercible FakeIO io + => ptr Word8 + -> Word8 + -> io () +pokeByteAxiom p (W8# w#) = + let f :: FakeWorld -> (# FakeWorld, () #) + f s = + let FakePtr {ptrId, ptrOff} = coerce p :: FakePtr Word8 + idx = fromIntegral (Pantomime.toInteger (Pantomime.bvu2i ptrId)) + arr = unsafeCoerce (refs s !! idx) :: Pantomime.Array Pantomime.Integer (Pantomime.BitVec 8) + arr' = Pantomime.astore @Pantomime.Integer @(Pantomime.BitVec 8) arr (Pantomime.bvu2i ptrOff) (Pantomime.fromWord8# w#) + s' = s {refs = updateAt idx (unsafeCoerce arr') (refs s)} + in (# nextWorld s', () #) + m :: io () + m = coerce (FakeIO f) + in coerce m diff --git a/stack.yaml b/stack.yaml index a8122a8..b0147ae 100644 --- a/stack.yaml +++ b/stack.yaml @@ -1,69 +1,84 @@ snapshot: ghc-9.12.2 packages: -- . + - . extra-deps: -- github: PLSec-VU/pantomime - commit: 491638b742ce2d9fc92976ab0e2037ba259e5ae9 -- github: RobinWebbers/grisette - commit: ae4d837886efb2e7838f89271f343d6fa8130388 -- sbv-13.6 -- QuickCheck-2.18.0.0 -- async-2.2.6 -- atomic-primops-0.8.8 -- base16-bytestring-1.0.2.0 -- bytes-0.17.5 -- cereal-0.5.8.3 -- cereal-text-0.1.0.2 -- composition-1.0.2.2 -- constraints-0.14.4 -- cryptohash-sha512-0.11.103.0 -- effectful-core-2.6.1.0 -- generic-deriving-1.14.7 -- hashable-1.5.1.0 -- haskell-src-exts-1.23.1 -- haskell-src-meta-0.8.15 -- libBF-0.6.8 -- loch-th-0.2.2 -- microlens-0.5.0.0 -- parallel-3.2.2.0 -- prettyprinter-1.7.1 -- primitive-0.9.1.0 -- random-1.3.1 -- syb-0.7.4 -- th-abstraction-0.7.2.0 -- th-compat-0.1.7 -- th-expand-syns-0.4.12.0 -- th-lift-instances-0.1.20 -- tree-view-0.5.1 -- uniplate-1.6.13 -- unordered-containers-0.2.21 -- vector-0.13.2.0 -- binary-orphans-1.0.5 -- boring-0.2.2 -- happy-2.2 -- monad-control-1.0.3.1 -- scientific-0.3.8.1 -- splitmix-0.1.3.2 -- strict-mutable-base-1.1.0.0 -- tasty-1.5.4 -- th-lift-0.8.7 -- th-orphans-0.13.17 -- transformers-base-0.4.6.1 -- transformers-compat-0.8 -- unliftio-core-0.2.1.0 -- vector-stream-0.1.0.1 -- ansi-terminal-1.1.5 -- base-orphans-0.9.4 -- happy-lib-2.2 -- integer-logarithms-1.0.5 -- optparse-applicative-0.19.0.0 -- tagged-0.8.10 -- th-reify-many-0.1.10 -- ansi-terminal-types-1.1.3 -- colour-2.3.7 -- prettyprinter-ansi-terminal-1.1.3 -- safe-0.3.21 + - github: PLSec-VU/pantomime + commit: 47dd4aa58eb53e323ac7a8a0e1c9f22d3be17316 + - github: RobinWebbers/grisette + commit: ae4d837886efb2e7838f89271f343d6fa8130388 + - sbv-13.6 + - QuickCheck-2.18.0.0 + - async-2.2.6 + - atomic-primops-0.8.8 + - base16-bytestring-1.0.2.0 + - bytes-0.17.5 + - cereal-0.5.8.3 + - cereal-text-0.1.0.2 + - composition-1.0.2.2 + - constraints-0.14.4 + - cryptohash-sha512-0.11.103.0 + - effectful-core-2.6.1.0 + - generic-deriving-1.14.7 + - hashable-1.5.1.0 + - haskell-src-exts-1.23.1 + - haskell-src-meta-0.8.15 + - libBF-0.6.8 + - loch-th-0.2.2 + - microlens-0.5.0.0 + - parallel-3.2.2.0 + - prettyprinter-1.7.1 + - primitive-0.9.1.0 + - random-1.3.1 + - syb-0.7.4 + - th-abstraction-0.7.2.0 + - th-compat-0.1.7 + - th-expand-syns-0.4.12.0 + - th-lift-instances-0.1.20 + - tree-view-0.5.1 + - uniplate-1.6.13 + - unordered-containers-0.2.21 + - vector-0.13.2.0 + - binary-orphans-1.0.5 + - boring-0.2.2 + - happy-2.2 + - monad-control-1.0.3.1 + - scientific-0.3.8.1 + - splitmix-0.1.3.2 + - strict-mutable-base-1.1.0.0 + - tasty-1.5.4 + - th-lift-0.8.7 + - th-orphans-0.13.17 + - transformers-base-0.4.6.1 + - transformers-compat-0.8 + - unliftio-core-0.2.1.0 + - vector-stream-0.1.0.1 + - ansi-terminal-1.1.5 + - base-orphans-0.9.4 + - happy-lib-2.2 + - integer-logarithms-1.0.5 + - optparse-applicative-0.19.0.0 + - tagged-0.8.10 + - th-reify-many-0.1.10 + - ansi-terminal-types-1.1.3 + - colour-2.3.7 + - prettyprinter-ansi-terminal-1.1.3 + - safe-0.3.21 + - hspec-2.11.10 + - hspec-core-2.11.10 + - hspec-expectations-0.8.4 + - hspec-discover-2.11.10 + - HUnit-1.6.2.0 + - call-stack-0.4.0 + - clock-0.8.4 + - setenv-0.1.1.3 + - quickcheck-io-0.2.0 + - haskell-lexer-1.2.1 + - tf-random-0.5 + - iproute-1.7.13 + - appar-0.1.8 + - byteorder-1.0.4 + - network-3.2.7.0 allow-newer: true diff --git a/stack.yaml.lock b/stack.yaml.lock index 786f38e..714385a 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -5,27 +5,27 @@ packages: - completed: - commit: 491638b742ce2d9fc92976ab0e2037ba259e5ae9 - git: git@github.com:PLSec-VU/pantomime.git name: pantomime pantry-tree: - sha256: db092592a9914ed1ee72d5916ae4f063667170c0b30a5dc9fd36412582682947 - size: 2709 + sha256: f626edbf8c57b6c4d19246de72e57108b321971c2b107bfd12cf0b6b68dbc635 + size: 2948 + sha256: 2804ba3c40279cc2ba596c9832d37c14cd050a426f5e5a2c187566ae2f0910e2 + size: 89824 + url: https://github.com/PLSec-VU/pantomime/archive/47dd4aa58eb53e323ac7a8a0e1c9f22d3be17316.tar.gz version: 0.1.0.0 original: - commit: 491638b742ce2d9fc92976ab0e2037ba259e5ae9 - git: git@github.com:PLSec-VU/pantomime.git + url: https://github.com/PLSec-VU/pantomime/archive/47dd4aa58eb53e323ac7a8a0e1c9f22d3be17316.tar.gz - completed: - commit: ae4d837886efb2e7838f89271f343d6fa8130388 - git: git@github.com:RobinWebbers/grisette.git name: grisette pantry-tree: sha256: ac978bcc6a35ee65677dbe41373c2799759457dedee85c6888a2cb7b362a2068 size: 31883 + sha256: 46de15734b258feee28ccc47c60a36a12fd3e975077615e8c31291b9d8ca79ef + size: 555460 + url: https://github.com/RobinWebbers/grisette/archive/ae4d837886efb2e7838f89271f343d6fa8130388.tar.gz version: 0.13.0.1 original: - commit: ae4d837886efb2e7838f89271f343d6fa8130388 - git: git@github.com:RobinWebbers/grisette.git + url: https://github.com/RobinWebbers/grisette/archive/ae4d837886efb2e7838f89271f343d6fa8130388.tar.gz - completed: hackage: sbv-13.6@sha256:65099c81504a2e85a49cc94a4f8bacad12c423b9171cf2ef3b6686a6a71d99ec,27240 pantry-tree: @@ -425,4 +425,109 @@ packages: size: 564 original: hackage: safe-0.3.21 +- completed: + hackage: hspec-2.11.10@sha256:62f300fd84909669466a817a1a7eef68c96f5e40d6d85d23c4ee17d6478895b7,1766 + pantry-tree: + sha256: 963d4861c7d7b39f1f0a8af5dedcde93229cc3550a31998f291f05af8ea45fe5 + size: 584 + original: + hackage: hspec-2.11.10 +- completed: + hackage: hspec-core-2.11.10@sha256:da9f859a25e07f9e562e460037ba09f38c420c5fb6dc56b57027c7d6be0a4281,7498 + pantry-tree: + sha256: 2821221d332d3a9d0da91d4e2526a2d6af6b49aeea5419548be9045a1260dbb2 + size: 6935 + original: + hackage: hspec-core-2.11.10 +- completed: + hackage: hspec-expectations-0.8.4@sha256:4237f094a7931202ff57ac6475542b0b314b50a7024550e2b6eb87cfb0d4ff93,1702 + pantry-tree: + sha256: 87681840d430b84686f83f1ab8b5873b09c349775698665233443914acf9ba2b + size: 741 + original: + hackage: hspec-expectations-0.8.4 +- completed: + hackage: hspec-discover-2.11.10@sha256:66f66caff8e3a0b0b1575381e474157795452b86f676aae41d5eb87e18a858f0,2171 + pantry-tree: + sha256: 91a673f0f217913b93a6593d2c39cf57ffedfb395ca064a1003cccb52c1f3aa8 + size: 829 + original: + hackage: hspec-discover-2.11.10 +- completed: + hackage: HUnit-1.6.2.0@sha256:1a79174e8af616117ad39464cac9de205ca923da6582825e97c10786fda933a4,1588 + pantry-tree: + sha256: 4f20a5a33866171260d0ee1e256c27f53cc84d37a68d498c3e12347f4e3d05b4 + size: 878 + original: + hackage: HUnit-1.6.2.0 +- completed: + hackage: call-stack-0.4.0@sha256:ac44d2c00931dc20b01750da8c92ec443eb63a7231e8550188cb2ac2385f7feb,1200 + pantry-tree: + sha256: 04134fa69cdd824b4e4bb7f77e7173e0705f27deabdbbf99549c549400191e1e + size: 501 + original: + hackage: call-stack-0.4.0 +- completed: + hackage: clock-0.8.4@sha256:b938655b00cf204ce69abfff946021bed111d2609a9f7a9c22e28a1a202e9115,4631 + pantry-tree: + sha256: 0ca511f7ea409e65a9de5539f265bb906a3eec6a4ac1a201731a8a328120cc88 + size: 499 + original: + hackage: clock-0.8.4 +- completed: + hackage: setenv-0.1.1.3@sha256:c5916ac0d2a828473cd171261328a290afe0abd799db1ac8c310682fe778c45b,1053 + pantry-tree: + sha256: 9a071cf2552e6881cd3ac0ce81252d5b96ac7f42cae517d973ea167e3d503265 + size: 212 + original: + hackage: setenv-0.1.1.3 +- completed: + hackage: quickcheck-io-0.2.0@sha256:7bf0b68fb90873825eb2e5e958c1b76126dcf984debb998e81673e6d837e0b2d,1133 + pantry-tree: + sha256: afaa27fbf8b35aa7ce174abd9c59a84a12fd7f3d08300c3280b22c1d204f11ca + size: 223 + original: + hackage: quickcheck-io-0.2.0 +- completed: + hackage: haskell-lexer-1.2.1@sha256:393300e223f7b84c334d87780481bcede98392aa8bd82bc882d76b54b7d1c699,1279 + pantry-tree: + sha256: 8e533ad0dbb5b7cff21bc44767b88d5c152102979e7f465ca2402af21d6722c6 + size: 588 + original: + hackage: haskell-lexer-1.2.1 +- completed: + hackage: tf-random-0.5@sha256:14012837d0f0e18fdbbe3d56e67da8622ee5e20b180abce952dd50bd9f36b326,3983 + pantry-tree: + sha256: d6483580cfea846cbf23ff1d7a67849546d5096425b6d61318a34554043b4ffb + size: 941 + original: + hackage: tf-random-0.5 +- completed: + hackage: iproute-1.7.13@sha256:db38adf1850f0d0e07458e907748abdf45a6f9befed5d29c331d4525dec1b036,1936 + pantry-tree: + sha256: adaebd5c10dc0451ac1a90d04254d9dcea12ec6180c8473f341edbf1a4d9016e + size: 906 + original: + hackage: iproute-1.7.13 +- completed: + hackage: appar-0.1.8@sha256:a5d529bacbb74d566e4c5f9479af0637eac5957705f6db4d2670517489795de8,1070 + pantry-tree: + sha256: c8bae7bc8c04b6c3593b48f19f1d626face90832f268f6857aba934bccd4272d + size: 506 + original: + hackage: appar-0.1.8 +- completed: + hackage: byteorder-1.0.4@sha256:a952817dcbe20af0346fb55a28c13e95e2ddbf3e99f9b4fffdc063f150f13b20,636 + pantry-tree: + sha256: 1544dc41983f7fe963740d9a8ce2aec1daef17bcb0916fda253dbfa73a14c77a + size: 212 + original: + hackage: byteorder-1.0.4 +- completed: + hackage: network-3.2.7.0@sha256:e3a1ec8b8dd32f1d5a541679a67de60d6626487a95f20c6bc245268ae7142ab7,5305 + pantry-tree: + sha256: a6b96da036a806119e17bd90ab2ef499778cf727531e22f3274ae9970ea630cf + size: 4039 + original: + hackage: network-3.2.7.0 snapshots: [] diff --git a/test/BoolTest.hs b/test/BoolTest.hs new file mode 100644 index 0000000..b108dc6 --- /dev/null +++ b/test/BoolTest.hs @@ -0,0 +1,27 @@ +module BoolTest (spec) where + +import Common +import Pantomime.BuiltIn qualified as Pantomime + +{-# ANN deMorganValid (Theory mempty) #-} +deMorganValid :: Bool -> Bool -> Pantomime.Bool +deMorganValid a b = + let a' = Pantomime.boolean a + b' = Pantomime.boolean b + in Pantomime.iff + (Pantomime.not (a' Pantomime.&& b')) + (Pantomime.not a' Pantomime.|| Pantomime.not b') + +{-# ANN fallacyInvalid (Theory mempty) #-} +fallacyInvalid :: Bool -> Bool -> Pantomime.Bool +fallacyInvalid a b = + let a' = Pantomime.boolean a + b' = Pantomime.boolean b + in a' `Pantomime.implies` b' + +spec :: Spec +spec = describe "Bool operations (no axioms)" $ do + it "De Morgan's Law is valid" $ + $(pantomime 'deMorganValid) `shouldBe` Nothing + it "implication is not a tautology" $ + checkInvalid $(pantomime 'fallacyInvalid) diff --git a/test/ByteStringTest.hs b/test/ByteStringTest.hs new file mode 100644 index 0000000..f84dfcf --- /dev/null +++ b/test/ByteStringTest.hs @@ -0,0 +1,22 @@ +module ByteStringTest (spec) where + +import Common +import Data.ByteString qualified as BS +import Pantomime.BuiltIn qualified as Pantomime + +-- {-# ANN bsSingletonIndex (Theory (axioms <> byteStringAxioms)) #-} +bsSingletonIndex :: Word8 -> Pantomime.Bool +bsSingletonIndex w = Pantomime.boolean $ BS.index (BS.singleton w) 0 == w + +-- {-# ANN bsNotNull (Theory (axioms <> byteStringAxioms)) #-} +bsNotNull :: BS.ByteString -> Pantomime.Bool +bsNotNull bs = Pantomime.boolean $ BS.index bs 0 == 0 + +spec :: Spec +spec = describe "ByteString operations" $ do + it "index (singleton w) 0 == w" $ + -- $(pantomime 'bsSingletonIndex) `shouldBe` Nothing + todo + it "index isn't always 0 (counterexample)" $ + -- checkInvalid $(pantomime 'bsNotNull) + todo diff --git a/test/Common.hs b/test/Common.hs new file mode 100644 index 0000000..5ea02f8 --- /dev/null +++ b/test/Common.hs @@ -0,0 +1,41 @@ +{-# OPTIONS_GHC -Wno-orphans #-} + +module Common + ( checkInvalid + , todo + , axioms + , ioAxioms + , ptrAxioms + , module Test.Hspec + , module Pantomime + , module GHC.Exts + , module GHC.Int + , module GHC.Word + ) where + +import Test.Hspec +import Test.Hspec.Expectations (expectationFailure) + +import Pantomime.Base (axioms) +import Pantomime (Theory (..), pantomime) +import Pantomime.IO (ioAxioms) +import Pantomime.Ptr (ptrAxioms) +import Pantomime.BuiltIn qualified as Pantomime + +import GHC.Exts +import GHC.Int +import GHC.Word + +-- | Placeholder expectation for tests whose pantomime TH splice is not yet active. +todo :: Expectation +todo = pure () + +-- | Assert that a counterexample was found and print it. +checkInvalid :: Show a => Maybe a -> Expectation +checkInvalid = \case + Just ce -> do + putStrLn "" + putStrLn "Counterexample found:" + print ce + putStrLn "" + Nothing -> expectationFailure "Expected a counterexample but assertion was valid" diff --git a/test/ContainersTest.hs b/test/ContainersTest.hs new file mode 100644 index 0000000..61045b9 --- /dev/null +++ b/test/ContainersTest.hs @@ -0,0 +1,104 @@ +{-# OPTIONS_GHC -Wno-missing-export-lists #-} + +module ContainersTest (spec) where + +import Common +import Data.Map.Strict qualified as Map +import Data.Set qualified as Set +import Pantomime.BuiltIn qualified as Pantomime + +{-# ANN mapMemberEmpty (Theory axioms) #-} +mapMemberEmpty :: Int -> Pantomime.Bool +mapMemberEmpty k = Pantomime.boolean $ not (Map.member k (Map.empty :: Map.Map Int Int)) + +{-# ANN mapMemberSingleton (Theory axioms) #-} +mapMemberSingleton :: Int -> Int -> Pantomime.Bool +mapMemberSingleton k v = Pantomime.boolean $ Map.member k (Map.singleton k v) + +{-# ANN mapLookupSingleton (Theory axioms) #-} +mapLookupSingleton :: Int -> Int -> Pantomime.Bool +mapLookupSingleton k v = Pantomime.boolean $ Map.lookup k (Map.singleton k v) == Just v + +{-# ANN mapMemberInsert (Theory axioms) #-} +mapMemberInsert :: Int -> Int -> Pantomime.Bool +mapMemberInsert k v = Pantomime.boolean $ Map.member k (Map.insert k v Map.empty) + +{-# ANN mapLookupInsert (Theory axioms) #-} +mapLookupInsert :: Int -> Int -> Pantomime.Bool +mapLookupInsert k v = Pantomime.boolean $ Map.lookup k (Map.insert k v Map.empty) == Just v + +{-# ANN mapDeleteSelf (Theory axioms) #-} +mapDeleteSelf :: Int -> Pantomime.Bool +mapDeleteSelf k = Pantomime.boolean $ Map.null (Map.delete k (Map.singleton k (0 :: Int))) + +{-# ANN mapLookupDifferentKey (Theory axioms) #-} +mapLookupDifferentKey :: Int -> Int -> Int -> Pantomime.Bool +mapLookupDifferentKey k1 k2 v = Pantomime.boolean $ + (k1 /= k2) `implies` (Map.lookup k1 (Map.singleton k2 v) == Nothing) + where + implies False _ = True + implies True x = x + +{-# ANN setMemberEmpty (Theory axioms) #-} +setMemberEmpty :: Int -> Pantomime.Bool +setMemberEmpty k = Pantomime.boolean $ not (Set.member k Set.empty) + +{-# ANN setMemberSingleton (Theory axioms) #-} +setMemberSingleton :: Int -> Pantomime.Bool +setMemberSingleton k = Pantomime.boolean $ Set.member k (Set.singleton k) + +{-# ANN setMemberInsert (Theory axioms) #-} +setMemberInsert :: Int -> Pantomime.Bool +setMemberInsert k = Pantomime.boolean $ Set.member k (Set.insert k Set.empty) + +{-# ANN setDeleteSelf (Theory axioms) #-} +setDeleteSelf :: Int -> Pantomime.Bool +setDeleteSelf k = Pantomime.boolean $ not (Set.member k (Set.delete k (Set.singleton k))) + +-- Invalid properties + +-- Invalid: map.member k1 (singleton k2 v) without the k1 == k2 precondition +{-# ANN mapMemberWrongKey (Theory axioms) #-} +mapMemberWrongKey :: Int -> Int -> Int -> Pantomime.Bool +mapMemberWrongKey k1 k2 v = Pantomime.boolean $ + Map.member k1 (Map.singleton k2 v) + +{-# ANN mapMemberAfterDelete (Theory axioms) #-} +mapMemberAfterDelete :: Int -> Int -> Pantomime.Bool +mapMemberAfterDelete k v = Pantomime.boolean $ + Map.member k (Map.delete k (Map.singleton k v)) + +-- Invalid: after inserting k v1 the old value v2 should no longer be present +{-# ANN mapLookupAfterOverwrite (Theory axioms) #-} +mapLookupAfterOverwrite :: Int -> Int -> Int -> Pantomime.Bool +mapLookupAfterOverwrite k v1 v2 = Pantomime.boolean $ + Map.lookup k (Map.insert k v1 (Map.singleton k v2)) == Nothing + +{-# ANN setMemberAfterDelete (Theory axioms) #-} +setMemberAfterDelete :: Int -> Pantomime.Bool +setMemberAfterDelete k = Pantomime.boolean $ + Set.member k (Set.delete k (Set.singleton k)) + +spec :: Spec +spec = describe "containers (Data.Map.Strict + Data.Set)" $ do + describe "Data.Map.Strict" $ do + it "member k empty == False" $ $(pantomime 'mapMemberEmpty) `shouldBe` Nothing + it "member k (singleton k v) == True" $ $(pantomime 'mapMemberSingleton) `shouldBe` Nothing + it "lookup k (singleton k v) == Just v" $ $(pantomime 'mapLookupSingleton) `shouldBe` Nothing + it "member k (insert k v empty) == True" $ $(pantomime 'mapMemberInsert) `shouldBe` Nothing + it "lookup k (insert k v empty) == Just v" $ $(pantomime 'mapLookupInsert) `shouldBe` Nothing + it "null (delete k (singleton k v)) == True" $ $(pantomime 'mapDeleteSelf) `shouldBe` Nothing + it "k1 /= k2 implies lookup k1 (singleton k2 v) == Nothing" $ $(pantomime 'mapLookupDifferentKey) `shouldBe` Nothing + it "member k1 (singleton k2 v) without k1==k2 precondition is invalid" $ + checkInvalid $(pantomime 'mapMemberWrongKey) + it "member k (delete k (singleton k v)) is invalid" $ + checkInvalid $(pantomime 'mapMemberAfterDelete) + it "lookup k (insert k v1 (singleton k v2)) == Nothing is invalid (returns Just v1)" $ + checkInvalid $(pantomime 'mapLookupAfterOverwrite) + describe "Data.Set" $ do + it "member k empty == False" $ $(pantomime 'setMemberEmpty) `shouldBe` Nothing + it "member k (singleton k) == True" $ $(pantomime 'setMemberSingleton) `shouldBe` Nothing + it "member k (insert k empty) == True" $ $(pantomime 'setMemberInsert) `shouldBe` Nothing + it "not (member k (delete k (singleton k))) == True" $ $(pantomime 'setDeleteSelf) `shouldBe` Nothing + it "member k (delete k (singleton k)) is invalid" $ + checkInvalid $(pantomime 'setMemberAfterDelete) diff --git a/test/IOTest.hs b/test/IOTest.hs new file mode 100644 index 0000000..13534f1 --- /dev/null +++ b/test/IOTest.hs @@ -0,0 +1,22 @@ +module IOTest (spec) where + +import Common +import Pantomime.BuiltIn qualified as Pantomime +import System.IO.Unsafe (unsafePerformIO) +import GHC.Base +import Data.IORef + +ioRefPure :: a -> IO a +ioRefPure x = do + ref <- newIORef undefined + writeIORef ref x + readIORef ref + +{-# ANN testIO (Theory (axioms <> ioAxioms)) #-} +testIO :: Int -> Pantomime.Bool +testIO x = Pantomime.boolean (x == unsafePerformIO (ioRefPure x)) + +spec :: Spec +spec = describe "IO Explanation" $ do + it "dumps the expression" $ + $(pantomime 'testIO) `shouldBe` Nothing diff --git a/test/IProuteTest.hs b/test/IProuteTest.hs new file mode 100644 index 0000000..35bad67 --- /dev/null +++ b/test/IProuteTest.hs @@ -0,0 +1,107 @@ +{-# OPTIONS_GHC -Wno-missing-export-lists #-} + +module IProuteTest (spec) where + +import Common +import Data.Bits +import Data.IP (IPv4, IPv6, AddrRange, Addr (..), makeAddrRange, isMatchedTo, (>:>), + toIPv4w, toIPv6w, ipv4ToIPv6, ipv4RangeToIPv6) +import Data.Word (Word32, Word8) +import Pantomime.BuiltIn qualified as Pantomime + +-- | Internal helper from Data.IP.Addr, reproduced verbatim (not part of public API). +fixByteOrder :: Word32 -> Word32 +fixByteOrder s = d1 .|. d2 .|. d3 .|. d4 + where + d1 = shiftL s 24 + d2 = shiftL s 8 .&. 0x00ff0000 + d3 = shiftR s 8 .&. 0x0000ff00 + d4 = shiftR s 24 .&. 0x000000ff + +-- | Byte-swapping is its own inverse. +{-# ANN fixByteOrderInvolution (Theory axioms) #-} +fixByteOrderInvolution :: Word32 -> Pantomime.Bool +fixByteOrderInvolution w = Pantomime.boolean $ fixByteOrder (fixByteOrder w) == w + +-- | Any IPv4 address is contained in the subnet it generates. +{-# ANN addrInOwnRange (Theory axioms) #-} +addrInOwnRange :: Word32 -> Int -> Pantomime.Bool +addrInOwnRange w len = Pantomime.boolean $ + let a = toIPv4w w + in a `isMatchedTo` makeAddrRange a len + +-- | Subnet containment is reflexive. +{-# ANN subnetReflexive (Theory axioms) #-} +subnetReflexive :: Word32 -> Int -> Pantomime.Bool +subnetReflexive w len = Pantomime.boolean $ + let r = makeAddrRange (toIPv4w w) len + in r >:> r + +-- | Subnet containment is transitive (for valid IPv4 mask lengths 0-32). +{-# ANN subnetTransitive (Theory axioms) #-} +subnetTransitive :: Word32 -> Int -> Word32 -> Int -> Word32 -> Int -> Pantomime.Bool +subnetTransitive w1 l1 w2 l2 w3 l3 = Pantomime.boolean $ + let validLens = 0 <= l1 && l1 <= 32 && 0 <= l2 && l2 <= 32 && 0 <= l3 && l3 <= 32 + r1 = makeAddrRange (toIPv4w w1) l1 + r2 = makeAddrRange (toIPv4w w2) l2 + r3 = makeAddrRange (toIPv4w w3) l3 + in not validLens || not (r1 >:> r2 && r2 >:> r3) || r1 >:> r3 + +-- | Any IPv6 address is contained in the subnet it generates. +-- Using Word8 for len avoids the Int minBound overflow that causes shiftR +-- to receive a negative shift amount inside maskIPv6/shiftR128. +{-# ANN addrInOwnRangeIPv6 (Theory axioms) #-} +addrInOwnRangeIPv6 :: Word32 -> Word32 -> Word32 -> Word32 -> Word8 -> Pantomime.Bool +addrInOwnRangeIPv6 w1 w2 w3 w4 len8 = Pantomime.boolean $ + let a = toIPv6w (w1, w2, w3, w4) + len = fromIntegral len8 + in a `isMatchedTo` makeAddrRange a len + +-- | IPv6 subnet containment is reflexive for all mask lengths in [0, 255]. +-- Using Word8 avoids the Int minBound overflow that causes shiftR to receive +-- a negative shift amount inside maskIPv6/shiftR128. +{-# ANN subnetReflexiveIPv6 (Theory axioms) #-} +subnetReflexiveIPv6 :: Word32 -> Word32 -> Word32 -> Word32 -> Word8 -> Pantomime.Bool +subnetReflexiveIPv6 w1 w2 w3 w4 len8 = Pantomime.boolean $ + let len = fromIntegral len8 + r = makeAddrRange (toIPv6w (w1, w2, w3, w4)) len + in r >:> r + +-- | IPv4-mapped IPv6 containment: if an IPv4 address is in a range, +-- its IPv4-mapped IPv6 form is in the lifted IPv6 range. +-- Using Word8 for len avoids Int minBound overflow in maskIPv4/maskIPv6. +{-# ANN ipv4MappedContainment (Theory axioms) #-} +ipv4MappedContainment :: Word32 -> Word8 -> Pantomime.Bool +ipv4MappedContainment w len8 = Pantomime.boolean $ + let len = fromIntegral len8 + a = toIPv4w w + r = makeAddrRange a len + validLen = len <= 32 + in not validLen || ipv4ToIPv6 a `isMatchedTo` ipv4RangeToIPv6 r + +spec :: Spec +spec = describe "iproute address arithmetic" $ do + describe "IPv4" $ do + it "fixByteOrder is an involution" $ + $(pantomime 'fixByteOrderInvolution) `shouldBe` Nothing + it "makeAddrRange always contains its own address" $ + $(pantomime 'addrInOwnRange) `shouldBe` Nothing + it "subnet containment is reflexive" $ + $(pantomime 'subnetReflexive) `shouldBe` Nothing + it "subnet containment is transitive" $ + $(pantomime 'subnetTransitive) `shouldBe` Nothing + describe "IPv6" $ do + it "makeAddrRange always contains its own address" $ + $(pantomime 'addrInOwnRangeIPv6) `shouldBe` Nothing + it "subnet containment is reflexive" $ + $(pantomime 'subnetReflexiveIPv6) `shouldBe` Nothing + it "IPv4-mapped address is in its lifted IPv6 range" $ + $(pantomime 'ipv4MappedContainment) `shouldBe` Nothing + describe "counterexample display smoke test" $ do + it "w==0 && b==0 is falsifiable (counterexample should show Word32/Word8 values)" $ + $(pantomime 'badProp) `shouldNotBe` Nothing + +-- Deliberately false: used to smoke-test counterexample reporting. +{-# ANN badProp (Theory axioms) #-} +badProp :: Word32 -> Word8 -> Pantomime.Bool +badProp w b = Pantomime.boolean (w == 0 && b == 0) diff --git a/test/Int.hs b/test/Int.hs new file mode 100644 index 0000000..b81b0d5 --- /dev/null +++ b/test/Int.hs @@ -0,0 +1,37 @@ +module Int (spec) where + +import Common +import Pantomime.BuiltIn qualified as Pantomime + +{-# ANN intAddComm (Theory axioms) #-} +intAddComm :: Int -> Int -> Pantomime.Bool +intAddComm (I# x) (I# y) = Pantomime.eqInt# (x +# y) (y +# x) + +{-# ANN intAddIdent (Theory axioms) #-} +intAddIdent :: Int -> Pantomime.Bool +intAddIdent (I# x) = Pantomime.eqInt# (x +# 0#) x + +{-# ANN intSubSelf (Theory axioms) #-} +intSubSelf :: Int -> Pantomime.Bool +intSubSelf (I# x) = Pantomime.eqInt# (x -# x) 0# + +{-# ANN intMulComm (Theory axioms) #-} +intMulComm :: Int -> Int -> Pantomime.Bool +intMulComm (I# x) (I# y) = Pantomime.eqInt# (x *# y) (y *# x) + +{-# ANN intInvalid (Theory axioms) #-} +intInvalid :: Int -> Pantomime.Bool +intInvalid (I# x) = Pantomime.eqInt# (x <# x) 1# + +spec :: Spec +spec = describe "Int operations (via Int# axioms)" $ do + it "addition is commutative" $ + $(pantomime 'intAddComm) `shouldBe` Nothing + it "addition identity: x + 0 == x" $ + $(pantomime 'intAddIdent) `shouldBe` Nothing + it "self-subtraction: x - x == 0" $ + $(pantomime 'intSubSelf) `shouldBe` Nothing + it "multiplication is commutative" $ + $(pantomime 'intMulComm) `shouldBe` Nothing + it "x < x is always false (invalid property)" $ + checkInvalid $(pantomime 'intInvalid) diff --git a/test/Int16.hs b/test/Int16.hs new file mode 100644 index 0000000..b7c9b94 --- /dev/null +++ b/test/Int16.hs @@ -0,0 +1,19 @@ +module Int16 (spec) where + +import Common +import Pantomime.BuiltIn qualified as Pantomime + +{-# ANN int16AddComm (Theory axioms) #-} +int16AddComm :: Int16 -> Int16 -> Pantomime.Bool +int16AddComm (I16# x) (I16# y) = Pantomime.eqInt16# (x `plusInt16#` y) (y `plusInt16#` x) + +{-# ANN int16Invalid (Theory axioms) #-} +int16Invalid :: Int16 -> Pantomime.Bool +int16Invalid (I16# x) = Pantomime.eqInt# (x `ltInt16#` x) 1# + +spec :: Spec +spec = describe "Int16 operations" $ do + it "addition is commutative" $ + $(pantomime 'int16AddComm) `shouldBe` Nothing + it "x < x is always false (invalid property)" $ + checkInvalid $(pantomime 'int16Invalid) diff --git a/test/Int32.hs b/test/Int32.hs new file mode 100644 index 0000000..864f63f --- /dev/null +++ b/test/Int32.hs @@ -0,0 +1,19 @@ +module Int32 (spec) where + +import Common +import Pantomime.BuiltIn qualified as Pantomime + +{-# ANN int32AddComm (Theory axioms) #-} +int32AddComm :: Int32 -> Int32 -> Pantomime.Bool +int32AddComm (I32# x) (I32# y) = Pantomime.eqInt32# (x `plusInt32#` y) (y `plusInt32#` x) + +{-# ANN int32Invalid (Theory axioms) #-} +int32Invalid :: Int32 -> Pantomime.Bool +int32Invalid (I32# x) = Pantomime.eqInt# (x `ltInt32#` x) 1# + +spec :: Spec +spec = describe "Int32 operations" $ do + it "addition is commutative" $ + $(pantomime 'int32AddComm) `shouldBe` Nothing + it "x < x is always false (invalid property)" $ + checkInvalid $(pantomime 'int32Invalid) diff --git a/test/Int64.hs b/test/Int64.hs new file mode 100644 index 0000000..0556f06 --- /dev/null +++ b/test/Int64.hs @@ -0,0 +1,19 @@ +module Int64 (spec) where + +import Common +import Pantomime.BuiltIn qualified as Pantomime + +{-# ANN int64AddComm (Theory axioms) #-} +int64AddComm :: Int64 -> Int64 -> Pantomime.Bool +int64AddComm (I64# x) (I64# y) = Pantomime.eqInt64# (x `plusInt64#` y) (y `plusInt64#` x) + +{-# ANN int64Invalid (Theory axioms) #-} +int64Invalid :: Int64 -> Pantomime.Bool +int64Invalid (I64# x) = Pantomime.eqInt# (x `ltInt64#` x) 1# + +spec :: Spec +spec = describe "Int64 operations" $ do + it "addition is commutative" $ + $(pantomime 'int64AddComm) `shouldBe` Nothing + it "x < x is always false (invalid property)" $ + checkInvalid $(pantomime 'int64Invalid) diff --git a/test/Int8.hs b/test/Int8.hs new file mode 100644 index 0000000..c9ca4e3 --- /dev/null +++ b/test/Int8.hs @@ -0,0 +1,19 @@ +module Int8 (spec) where + +import Common +import Pantomime.BuiltIn qualified as Pantomime + +{-# ANN int8AddComm (Theory axioms) #-} +int8AddComm :: Int8 -> Int8 -> Pantomime.Bool +int8AddComm (I8# x) (I8# y) = Pantomime.eqInt8# (x `plusInt8#` y) (y `plusInt8#` x) + +{-# ANN int8Invalid (Theory axioms) #-} +int8Invalid :: Int8 -> Pantomime.Bool +int8Invalid (I8# x) = Pantomime.eqInt# (x `ltInt8#` x) 1# + +spec :: Spec +spec = describe "Int8 operations" $ do + it "addition is commutative" $ + $(pantomime 'int8AddComm) `shouldBe` Nothing + it "x < x is always false (invalid property)" $ + checkInvalid $(pantomime 'int8Invalid) diff --git a/test/IntegerTest.hs b/test/IntegerTest.hs new file mode 100644 index 0000000..744e77f --- /dev/null +++ b/test/IntegerTest.hs @@ -0,0 +1,19 @@ +module IntegerTest (spec) where + +import Common +import Pantomime.BuiltIn qualified as Pantomime + +{-# ANN integerAddComm (Theory axioms) #-} +integerAddComm :: Pantomime.Integer -> Pantomime.Integer -> Pantomime.Bool +integerAddComm x y = Pantomime.ieq (Pantomime.iadd x y) (Pantomime.iadd y x) + +{-# ANN integerSuccGt (Theory axioms) #-} +integerSuccGt :: Pantomime.Integer -> Pantomime.Bool +integerSuccGt x = Pantomime.ilt x (Pantomime.iadd x 1) + +spec :: Spec +spec = describe "Integer operations" $ do + it "addition is commutative" $ + $(pantomime 'integerAddComm) `shouldBe` Nothing + it "x < x + 1 (no overflow for unbounded integers)" $ + $(pantomime 'integerSuccGt) `shouldBe` Nothing diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 index 0000000..7d6ce8b --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,35 @@ +module Main (main) where + +import Test.Hspec + +import qualified Int +import qualified Int8 +import qualified Int16 +import qualified Int32 +import qualified Int64 +import qualified Word +import qualified Word8 +import qualified Word64 +import qualified IntegerTest +import qualified BoolTest +import qualified IOTest +import qualified PtrTest +import qualified IProuteTest +import qualified ContainersTest + +main :: IO () +main = hspec $ do + IOTest.spec + PtrTest.spec + IProuteTest.spec + ContainersTest.spec + BoolTest.spec + IntegerTest.spec + Int.spec + Int8.spec + Int16.spec + Int32.spec + Int64.spec + Word.spec + Word8.spec + Word64.spec diff --git a/test/PtrTest.hs b/test/PtrTest.hs new file mode 100644 index 0000000..edbc3f1 --- /dev/null +++ b/test/PtrTest.hs @@ -0,0 +1,187 @@ +module PtrTest (spec) where + +import Common +import Foreign.ForeignPtr (ForeignPtr) +import Pantomime.Ptr (mallocByteStringN, withForeignPtrN, plusPtrN) +import Foreign.Ptr (Ptr, castPtr, minusPtr) +import Pantomime.BuiltIn qualified as Pantomime +import Pantomime.Ptr (peekByte, pokeByte) +import System.IO.Unsafe (unsafePerformIO) +import Data.Word (Word8, Word16) + +-- | plusPtr then minusPtr should round-trip: (p `plusPtr` n) `minusPtr` p == n. +{-# ANN ptrRoundTrip (Theory (axioms <> ioAxioms <> ptrAxioms)) #-} +ptrRoundTrip :: Ptr Word8 -> Int -> Pantomime.Bool +ptrRoundTrip p n = Pantomime.boolean (minusPtr (plusPtrN p n) p == n) + +-- | castPtr preserves the pointer offset: minusPtr (castPtr p) p == 0. +{-# ANN castPtrPreservesOffset (Theory (axioms <> ioAxioms <> ptrAxioms)) #-} +castPtrPreservesOffset :: Ptr Word8 -> Pantomime.Bool +castPtrPreservesOffset p = Pantomime.boolean $ + minusPtr (castPtr p :: Ptr Word16) p == 0 + +-- | plusPtr is additive: minusPtr (plusPtr (plusPtr p m) n) p == m + n. +{-# ANN plusPtrAdditive (Theory (axioms <> ioAxioms <> ptrAxioms)) #-} +plusPtrAdditive :: Ptr Word8 -> Int -> Int -> Pantomime.Bool +plusPtrAdditive p m n = Pantomime.boolean (minusPtr (plusPtrN (plusPtrN p m) n) p == m + n) + +-- | mallocPlainForeignPtrBytes then withForeignPtr: the materialized pointer has +-- offset 0 relative to itself. +{-# ANN mallocOffsetZero (Theory (axioms <> ioAxioms <> ptrAxioms)) #-} +mallocOffsetZero :: Pantomime.Bool +mallocOffsetZero = Pantomime.boolean $ + unsafePerformIO $ do + fp <- mallocByteStringN 8 :: IO (ForeignPtr Word8) + withForeignPtrN fp $ \p -> return (minusPtr p p == 0) + +-- | malloc + withForeignPtr + plusPtr: minusPtr (plusPtr p n) p == n +{-# ANN mallocPlusPtrInside (Theory (axioms <> ioAxioms <> ptrAxioms)) #-} +mallocPlusPtrInside :: Int -> Pantomime.Bool +mallocPlusPtrInside n = Pantomime.boolean $ + unsafePerformIO $ do + fp <- mallocByteStringN 8 :: IO (ForeignPtr Word8) + withForeignPtrN fp $ \p -> return (minusPtr (plusPtrN p n) p == n) + +-- | poke then peek at the same offset returns the written byte. +{-# ANN pokePeekRoundTrip (Theory (axioms <> ioAxioms <> ptrAxioms)) #-} +pokePeekRoundTrip :: Word8 -> Pantomime.Bool +pokePeekRoundTrip v = Pantomime.boolean $ + unsafePerformIO $ do + fp <- mallocByteStringN 8 :: IO (ForeignPtr Word8) + withForeignPtrN fp $ \p -> do + pokeByte p v + r <- peekByte p + return (r == v) + +-- | peek at a freshly malloc'd buffer returns 0 (zero-initialization). +{-# ANN mallocPeekZero (Theory (axioms <> ioAxioms <> ptrAxioms)) #-} +mallocPeekZero :: Pantomime.Bool +mallocPeekZero = Pantomime.boolean $ + unsafePerformIO $ do + fp <- mallocByteStringN 8 :: IO (ForeignPtr Word8) + withForeignPtrN fp $ \p -> do + r <- peekByte p + return (r == 0) + +-- | poke at offset n, peek at the same offset: returns the written byte. +{-# ANN pokePeekAtOffset (Theory (axioms <> ioAxioms <> ptrAxioms)) #-} +pokePeekAtOffset :: Int -> Word8 -> Pantomime.Bool +pokePeekAtOffset n v = Pantomime.boolean $ + unsafePerformIO $ do + fp <- mallocByteStringN 16 :: IO (ForeignPtr Word8) + withForeignPtrN fp $ \p -> do + pokeByte (plusPtrN p n) v + r <- peekByte (plusPtrN p n) + return (r == v) + +-- | poke at offset 0, peek at offset 1: does NOT see the write (distinct cells). +{-# ANN pokePeekDistinctOffsets (Theory (axioms <> ioAxioms <> ptrAxioms)) #-} +pokePeekDistinctOffsets :: Word8 -> Pantomime.Bool +pokePeekDistinctOffsets v = Pantomime.boolean $ + unsafePerformIO $ do + fp <- mallocByteStringN 16 :: IO (ForeignPtr Word8) + withForeignPtrN fp $ \p -> do + pokeByte p v + r <- peekByte (plusPtrN p 1) + return (r == 0) + +-- | poke overwrites: poke v1, poke v2, peek returns v2. +{-# ANN pokeOverwrite (Theory (axioms <> ioAxioms <> ptrAxioms)) #-} +pokeOverwrite :: Word8 -> Word8 -> Pantomime.Bool +pokeOverwrite v1 v2 = Pantomime.boolean $ + unsafePerformIO $ do + fp <- mallocByteStringN 8 :: IO (ForeignPtr Word8) + withForeignPtrN fp $ \p -> do + pokeByte p v1 + pokeByte p v2 + r <- peekByte p + return (r == v2) + +-- | poke at symbolic offset m, peek at symbolic offset n: if m /= n, the +-- write is not observed. Generalizes 'pokePeekDistinctOffsets' from a fixed +-- literal offset to arbitrary symbolic offsets. +{-# ANN pokePeekDistinctSymbolicOffsets (Theory (axioms <> ioAxioms <> ptrAxioms)) #-} +pokePeekDistinctSymbolicOffsets :: Int -> Int -> Word8 -> Pantomime.Bool +pokePeekDistinctSymbolicOffsets m n v = Pantomime.boolean $ + unsafePerformIO $ do + fp <- mallocByteStringN 16 :: IO (ForeignPtr Word8) + withForeignPtrN fp $ \p -> do + pokeByte (plusPtrN p m) v + r <- peekByte (plusPtrN p n) + return ((m /= n) `implies` (r == 0)) + where + implies False _ = True + implies True x = x + +-- | poke at (p + m) + n, peek at p + (m + n): the same cell reached via two +-- different arithmetic paths is still the same cell. +{-# ANN pokePeekNestedArithmetic (Theory (axioms <> ioAxioms <> ptrAxioms)) #-} +pokePeekNestedArithmetic :: Int -> Int -> Word8 -> Pantomime.Bool +pokePeekNestedArithmetic m n v = Pantomime.boolean $ + unsafePerformIO $ do + fp <- mallocByteStringN 16 :: IO (ForeignPtr Word8) + withForeignPtrN fp $ \p -> do + pokeByte (plusPtrN (plusPtrN p m) n) v + r <- peekByte (plusPtrN p (m + n)) + return (r == v) + +-- | poke through p, peek through castPtr (castPtr p): a round-trip cast +-- through another element type still observes the write, since castPtr +-- retypes the phantom without changing the underlying address. +{-# ANN pokePeekThroughCast (Theory (axioms <> ioAxioms <> ptrAxioms)) #-} +pokePeekThroughCast :: Word8 -> Pantomime.Bool +pokePeekThroughCast v = Pantomime.boolean $ + unsafePerformIO $ do + fp <- mallocByteStringN 8 :: IO (ForeignPtr Word8) + withForeignPtrN fp $ \p -> do + pokeByte p v + let p' = castPtr (castPtr p :: Ptr Word16) :: Ptr Word8 + r <- peekByte p' + return (r == v) + +-- | poke into buffer A at offset k, peek from a distinct buffer B at the +-- same offset k: does NOT see the write. Unlike 'pokePeekDistinctOffsets' +-- and 'pokePeekDistinctSymbolicOffsets', this separates cells by allocation +-- id rather than by offset within one allocation. +{-# ANN pokePeekDistinctAllocations (Theory (axioms <> ioAxioms <> ptrAxioms)) #-} +pokePeekDistinctAllocations :: Int -> Word8 -> Pantomime.Bool +pokePeekDistinctAllocations k v = Pantomime.boolean $ + unsafePerformIO $ do + fpA <- mallocByteStringN 8 :: IO (ForeignPtr Word8) + fpB <- mallocByteStringN 8 :: IO (ForeignPtr Word8) + withForeignPtrN fpA $ \pa -> + withForeignPtrN fpB $ \pb -> do + pokeByte (plusPtrN pa k) v + r <- peekByte (plusPtrN pb k) + return (r == 0) + +spec :: Spec +spec = describe "Pointer axioms" $ do + it "plusPtr/minusPtr round-trip" $ + $(pantomime 'ptrRoundTrip) `shouldBe` Nothing + it "castPtr preserves offset" $ + $(pantomime 'castPtrPreservesOffset) `shouldBe` Nothing + it "plusPtr is additive" $ + $(pantomime 'plusPtrAdditive) `shouldBe` Nothing + it "mallocPlainForeignPtrBytes + withForeignPtr gives offset 0" $ + $(pantomime 'mallocOffsetZero) `shouldBe` Nothing + it "plusPtr inside withForeignPtr round-trips" $ + $(pantomime 'mallocPlusPtrInside) `shouldBe` Nothing + it "poke then peek at same offset round-trips" $ + $(pantomime 'pokePeekRoundTrip) `shouldBe` Nothing + it "peek at fresh malloc returns 0" $ + $(pantomime 'mallocPeekZero) `shouldBe` Nothing + it "poke/peek at symbolic offset round-trips" $ + $(pantomime 'pokePeekAtOffset) `shouldBe` Nothing + it "poke at 0 does not affect peek at 1" $ + $(pantomime 'pokePeekDistinctOffsets) `shouldBe` Nothing + it "poke overwrites previous value" $ + $(pantomime 'pokeOverwrite) `shouldBe` Nothing + it "poke/peek at distinct symbolic offsets does not alias" $ + $(pantomime 'pokePeekDistinctSymbolicOffsets) `shouldBe` Nothing + it "poke/peek through nested arithmetic reaches the same cell" $ + $(pantomime 'pokePeekNestedArithmetic) `shouldBe` Nothing + it "poke/peek through a round-trip castPtr sees the write" $ + $(pantomime 'pokePeekThroughCast) `shouldBe` Nothing + it "poke/peek across distinct allocations does not alias" $ + $(pantomime 'pokePeekDistinctAllocations) `shouldBe` Nothing diff --git a/test/Word.hs b/test/Word.hs new file mode 100644 index 0000000..c154729 --- /dev/null +++ b/test/Word.hs @@ -0,0 +1,31 @@ +module Word (spec) where + +import Common +import Pantomime.BuiltIn qualified as Pantomime + +{-# ANN wordAddComm (Theory axioms) #-} +wordAddComm :: Word -> Word -> Pantomime.Bool +wordAddComm (W# x) (W# y) = Pantomime.eqWord# (x `plusWord#` y) (y `plusWord#` x) + +{-# ANN wordAddIdent (Theory axioms) #-} +wordAddIdent :: Word -> Pantomime.Bool +wordAddIdent (W# x) = Pantomime.eqWord# (x `plusWord#` 0##) x + +{-# ANN wordAndComm (Theory axioms) #-} +wordAndComm :: Word -> Word -> Pantomime.Bool +wordAndComm (W# x) (W# y) = Pantomime.eqWord# (x `and#` y) (y `and#` x) + +{-# ANN wordInvalid (Theory axioms) #-} +wordInvalid :: Word -> Pantomime.Bool +wordInvalid (W# x) = Pantomime.eqInt# (x `ltWord#` x) 1# + +spec :: Spec +spec = describe "Word operations (via Word# axioms)" $ do + it "addition is commutative" $ + $(pantomime 'wordAddComm) `shouldBe` Nothing + it "addition identity: x + 0 == x" $ + $(pantomime 'wordAddIdent) `shouldBe` Nothing + it "AND is commutative" $ + $(pantomime 'wordAndComm) `shouldBe` Nothing + it "x < x is always false (invalid property)" $ + checkInvalid $(pantomime 'wordInvalid) diff --git a/test/Word64.hs b/test/Word64.hs new file mode 100644 index 0000000..29d9936 --- /dev/null +++ b/test/Word64.hs @@ -0,0 +1,19 @@ +module Word64 (spec) where + +import Common +import Pantomime.BuiltIn qualified as Pantomime + +{-# ANN word64AddComm (Theory axioms) #-} +word64AddComm :: Word64 -> Word64 -> Pantomime.Bool +word64AddComm (W64# x) (W64# y) = Pantomime.eqWord64# (x `plusWord64#` y) (y `plusWord64#` x) + +{-# ANN word64Invalid (Theory axioms) #-} +word64Invalid :: Word64 -> Pantomime.Bool +word64Invalid (W64# x) = Pantomime.eqInt# (x `ltWord64#` x) 1# + +spec :: Spec +spec = describe "Word64 operations" $ do + it "addition is commutative" $ + $(pantomime 'word64AddComm) `shouldBe` Nothing + it "x < x is always false (invalid property)" $ + checkInvalid $(pantomime 'word64Invalid) diff --git a/test/Word8.hs b/test/Word8.hs new file mode 100644 index 0000000..049e862 --- /dev/null +++ b/test/Word8.hs @@ -0,0 +1,19 @@ +module Word8 (spec) where + +import Common +import Pantomime.BuiltIn qualified as Pantomime + +{-# ANN word8AddComm (Theory axioms) #-} +word8AddComm :: Word8 -> Word8 -> Pantomime.Bool +word8AddComm (W8# x) (W8# y) = Pantomime.eqWord8# (x `plusWord8#` y) (y `plusWord8#` x) + +{-# ANN word8Invalid (Theory axioms) #-} +word8Invalid :: Word8 -> Pantomime.Bool +word8Invalid (W8# x) = Pantomime.eqInt# (x `ltWord8#` x) 1# + +spec :: Spec +spec = describe "Word8 operations" $ do + it "addition is commutative" $ + $(pantomime 'word8AddComm) `shouldBe` Nothing + it "x < x is always false (invalid property)" $ + checkInvalid $(pantomime 'word8Invalid)