diff --git a/CHANGELOG.md b/CHANGELOG.md index 4cfcd37..b42ca02 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,4 +1,4 @@ -# Changelog for `pantomime` +# Changelog for `sym-fc` All notable changes to this project will be documented in this file. diff --git a/INSTALL.md b/INSTALL.md index e2e6d9b..c84a773 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -1,10 +1,10 @@ -# `Pantomime` Installation Guide +# `SymFC` Installation Guide -This document describes the external dependencies of `Pantomime`, how to add the `pantomime` package as a dependency to your project and how to enable the compiler plugin. +This document describes the external dependencies of `SymFC`, how to add the `sym-fc` package as a dependency to your project and how to enable the compiler plugin. ## SMT Solver -`Pantomime` assumes that the [`Z3`](https://github.com/z3prover/z3) SMT solver is installed and available from your `PATH`. To see if an installation is available on your machine, run the following command: +`SymFC` assumes that the [`Z3`](https://github.com/z3prover/z3) SMT solver is installed and available from your `PATH`. To see if an installation is available on your machine, run the following command: ```sh z3 --version @@ -14,7 +14,7 @@ In the future, we aim to make it configurable which solver is used. ## Stack or Cabal build -This guide explains how to use either [`Stack`](https://docs.haskellstack.org/en/stable/) or [`Cabal`](https://www.haskell.org/cabal/) to build `Pantomime`. If you don't already have either of these installed yet, we recommend managing them through [`GHCup`](https://www.haskell.org/ghcup/). Throughout the guide, we will also have collapsed fields like the ones below that help you with commands for your respective build tool of choise: +This guide explains how to use either [`Stack`](https://docs.haskellstack.org/en/stable/) or [`Cabal`](https://www.haskell.org/cabal/) to build `SymFC`. If you don't already have either of these installed yet, we recommend managing them through [`GHCup`](https://www.haskell.org/ghcup/). Throughout the guide, we will also have collapsed fields like the ones below that help you with commands for your respective build tool of choise:
Stack setup @@ -32,11 +32,11 @@ During this guide, feel free to build your project after any adjustment to the c ## Example Repository -If you are simply looking to try out `Pantomime`, or want to start a fresh project with `Pantomime`, you may also use the [example repository](https://github.com/PLSec-VU/pantomime-example) as a template. It can also serve as a reference to inspect in case you get stuck. If the guide was unclear in any way (or you have other suggestions), do [let us know](https://github.com/PLSec-VU/pantomime/issues/new) so we can improve it! +If you are simply looking to try out `SymFC`, or want to start a fresh project with `SymFC`, you may also use the [example repository](https://github.com/PLSec-VU/sym-fc-example) as a template. It can also serve as a reference to inspect in case you get stuck. If the guide was unclear in any way (or you have other suggestions), do [let us know](https://github.com/PLSec-VU/sym-fc/issues/new) so we can improve it! ## GHC Version -`Pantomime` is a `GHC` compiler plugin, which causes it to heavily rely on the API that `GHC` exposes to its users. At the time of writing, `Pantomime` is built using `GHC` version `9.12.2`. Altough untested, it is likely that `Pantomime` is incompatible with other versions of `GHC`. +`SymFC` is a `GHC` compiler plugin, which causes it to heavily rely on the API that `GHC` exposes to its users. At the time of writing, `SymFC` is built using `GHC` version `9.12.2`. Altough untested, it is likely that `SymFC` is incompatible with other versions of `GHC`.
Stack setup @@ -62,12 +62,12 @@ snapshot: ghc-9.12.2 TODO
-We aim to make `Pantomime` compatible with a wider range of `GHC` versions in +We aim to make `SymFC` compatible with a wider range of `GHC` versions in the future! ## Grisette -`Pantomime` uses a custom version of [`Grisette`](https://hackage-content.haskell.org/package/grisette-0.13.0.1), which can be found [here](https://github.com/RobinWebbers/grisette). In the future, we hope the [pull request](https://github.com/lsrcz/grisette/pull/309) for the extension will get merged and pushed to hackage. Sadly, this is one of the blocking factors for `Pantomime` to get pushed as a package on [`Hackage`](https://hackage.haskell.org/). +`SymFC` uses a custom version of [`Grisette`](https://hackage-content.haskell.org/package/grisette-0.13.0.1), which can be found [here](https://github.com/RobinWebbers/grisette). In the future, we hope the [pull request](https://github.com/lsrcz/grisette/pull/309) for the extension will get merged and pushed to hackage. Sadly, this is one of the blocking factors for `SymFC` to get pushed as a package on [`Hackage`](https://hackage.haskell.org/).
Stack setup @@ -89,30 +89,30 @@ You may add the `extra-deps` field if it does not already exist. TODO
-## Pantomime +## SymFC -We can now add a dependency to `Pantomime` in your project. Additionally, we will add a dependency to [`pantomime-base`](https://github.com/PLSec-VU/pantomime-base). It is not important to understand what this contains for the purpose of this setup, but feel free to check it out if you're interested. +We can now add a dependency to `SymFC` in your project. Additionally, we will add a dependency to [`sym-fc-base`](https://github.com/PLSec-VU/sym-fc-base). It is not important to understand what this contains for the purpose of this setup, but feel free to check it out if you're interested.
Stack setup -Add the `pantomime` and `pantomime-base` packages to the `extra-deps` field of your `stack.yaml` file. This lets stack know which version of these packages to build with, should they be used. For now, `Pantomime` is not available on [`Hackage`](https://hackage.haskell.org/) so we'll have to specify the git repository and which commit hash to use instead. We recommend getting the latest commit from the `main` branch of the respective repositories. +Add the `sym-fc` and `sym-fc-base` packages to the `extra-deps` field of your `stack.yaml` file. This lets stack know which version of these packages to build with, should they be used. For now, `SymFC` is not available on [`Hackage`](https://hackage.haskell.org/) so we'll have to specify the git repository and which commit hash to use instead. We recommend getting the latest commit from the `main` branch of the respective repositories. ```yaml extra-deps: -- git: https://github.com/PLSec-VU/pantomime.git - commit: -- git: https://github.com/PLSec-VU/pantomime-base.git - commit: +- git: https://github.com/PLSec-VU/sym-fc.git + commit: +- git: https://github.com/PLSec-VU/sym-fc-base.git + commit: ``` -Additionally, you will need to add these dependencies to a stanza (e.g. `library`, `executables`) of your choise. This exposes `Pantomime` modules to be available to import in your project. The following shows how to add the dependencies to your `library` build: +Additionally, you will need to add these dependencies to a stanza (e.g. `library`, `executables`) of your choise. This exposes `SymFC` modules to be available to import in your project. The following shows how to add the dependencies to your `library` build: ```yaml library: dependencies: - - pantomime - - pantomime-base + - sym-fc + - sym-fc-base ``` At this point, you can build the project using `stack build` to see if the `snapshot` you picked in one of the [previous steps](#ghc-version) works for the build. Though unusual, `Stack` may refuse to build if the set of packages was not consistent with themselves. You can try different snapshots until you find one that works. @@ -128,10 +128,10 @@ TODO ## Enable Plugin -To allow `Pantomime` to run on your code examples, its plugin needs to be enabled during compilation. You may either enable it per module or project wide. To enable `Pantomime` in a single module, add the following pragma at the top of the respective file. +To allow `SymFC` to run on your code examples, its plugin needs to be enabled during compilation. You may either enable it per module or project wide. To enable `SymFC` in a single module, add the following pragma at the top of the respective file. ```haskell -{-# OPTIONS_GHC "-fplugin Pantomime" #-} +{-# OPTIONS_GHC "-fplugin SymFC" #-} module Example.Module where ``` @@ -141,12 +141,12 @@ You can enable it project wide by passing this same option in your build files.
Stack setup -To illustrate, here we enable `Pantomime` when building your project's library. +To illustrate, here we enable `SymFC` when building your project's library. ```yaml library: ghc-options: - - -fplugin Pantomime + - -fplugin SymFC ```
@@ -158,27 +158,27 @@ TODO ## Try it! -At this point, the project should compile with the `Pantomime` plugin. You can +At this point, the project should compile with the `SymFC` plugin. You can try to build the following example module. ```haskell -{-# OPTIONS_GHC "-fplugin Pantomime" #-} -- or use system-wide setup +{-# OPTIONS_GHC "-fplugin SymFC" #-} -- or use system-wide setup module Example (example) where -import Pantomime (Theory (..)) -import qualified Pantomime.BuiltIn as Pantomime -import qualified Pantomime.Base as Base +import SymFC (Theory (..)) +import qualified SymFC.BuiltIn as SymFC +import qualified SymFC.Base as Base {-# ANN example (Theory Base.axioms) #-} -example :: Int -> Pantomime.Bool -example x = Pantomime.boolean $ x + x == 2 * x +example :: Int -> SymFC.Bool +example x = SymFC.boolean $ x + x == 2 * x ``` -If all went well, you should see a query to an SMT solver pop up in your terminal during compilation. `Pantomime` should tell you that the stub is indeed valid. +If all went well, you should see a query to an SMT solver pop up in your terminal during compilation. `SymFC` should tell you that the stub is indeed valid. -**NOTE**: As of writing, `Pantomime` only verifies a function if it is exported in the module. Make sure this is true in case you do not see any result. +**NOTE**: As of writing, `SymFC` only verifies a function if it is exported in the module. Make sure this is true in case you do not see any result. ## Documentation -This concludes the setup guide. Sadly, I cannot refer you to a `Hackage` page with documentation as it is not up yet. The [project page](https://github.com/PLSec-VU/pantomime) contains more information on `Pantomime`. You may also want to build the documentation through [`Haddock`](https://haskell-haddock.readthedocs.io/latest/). +This concludes the setup guide. Sadly, I cannot refer you to a `Hackage` page with documentation as it is not up yet. The [project page](https://github.com/PLSec-VU/sym-fc) contains more information on `SymFC`. You may also want to build the documentation through [`Haddock`](https://haskell-haddock.readthedocs.io/latest/). diff --git a/README.md b/README.md index 24a5971..1473550 100644 --- a/README.md +++ b/README.md @@ -1,26 +1,26 @@ -# Pantomime +# SymFC -`Pantomime` is a full-path symbolic execution engine for `GHC` Core—the internal language of `GHC`, which is based on System FC. `Pantomime` is a `GHC` Core plugin, which verifies validity of a boolean statement, given an annotation, as shown below. +`SymFC` is a full-path symbolic execution engine for `GHC` Core—the internal language of `GHC`, which is based on System FC. `SymFC` is a `GHC` Core plugin, which verifies validity of a boolean statement, given an annotation, as shown below. ```haskell -{-# OPTIONS_GHC "-fplugin Pantomime" #-} +{-# OPTIONS_GHC "-fplugin SymFC" #-} module Example.Module (example) where -import Pantomime (Theory (..)) +import SymFC (Theory (..)) {-# ANN example (Theory mempty) #-} -example :: Bool -> Bool -> Pantomime.Bool -example x y = Pantomime.boolean $ not x && not y == not (x || y) +example :: Bool -> Bool -> SymFC.Bool +example x y = SymFC.boolean $ not x && not y == not (x || y) ``` -In this case, `Pantomime` shows validity of the statement, quantified over all Boolean inputs. +In this case, `SymFC` shows validity of the statement, quantified over all Boolean inputs. **NOTE**: The value supplied to `Theory` is extremely important in most real-world scenarios. An explanation can be found in section [Embeddings](#embeddings). ## Getting Started -See the [installation guide](./INSTALL.md) on how to install `Pantomime` and its dependencies. +See the [installation guide](./INSTALL.md) on how to install `SymFC` and its dependencies. ## Documentation @@ -28,59 +28,59 @@ As of writing, this package is not hosted on `Hackage` and thus we do not host t ## Annotation -With this, `GHC` will run `Pantomime` on any expression that has an annotation with the `Theory` type, that returns an argument of type `Pantomime.Bool` when saturated: +With this, `GHC` will run `SymFC` on any expression that has an annotation with the `Theory` type, that returns an argument of type `SymFC.Bool` when saturated: ```haskell {-# ANN expr (Theory mempty) #-} -expr :: ... -> Pantomime.Bool +expr :: ... -> SymFC.Bool ``` -**PITFALL**: `Pantomime` will only run for expressions that are in the export list of the encapsulating module. Hopefully, we can remove this quirk in the future! +**PITFALL**: `SymFC` will only run for expressions that are in the export list of the encapsulating module. Hopefully, we can remove this quirk in the future! -`Pantomime` will run when `GHC` compiles the program. If the annotated formula is not valid, `Pantomime` will throw an error and display the arguments that were used to get `False` as a result. +`SymFC` will run when `GHC` compiles the program. If the annotated formula is not valid, `SymFC` will throw an error and display the arguments that were used to get `False` as a result. ## Built-In Types -`Pantomime` support the following SMT Theories: +`SymFC` support the following SMT Theories: - Theory of Bitvectors - Theory of Integers - Theory of Arrays -These data types and their functions are regarded as primitives and are exported from `Pantomime.BuiltIn`, along with the `Bool` primitive. +These data types and their functions are regarded as primitives and are exported from `SymFC.BuiltIn`, along with the `Bool` primitive. ## Embeddings -Pantomime directly supports computation on Algebraic Data Types. For example, we can check a function that uses `Maybe` and `Bool` as exported by `base`: +SymFC directly supports computation on Algebraic Data Types. For example, we can check a function that uses `Maybe` and `Bool` as exported by `base`: ```haskell -- NOTE: This will return a counterexample to validity when run. {-# ANN example (Theory mempty) #-} -example :: Maybe Bool -> Pantomime.Bool -example x = Pantomime.boolean $ x == Just False +example :: Maybe Bool -> SymFC.Bool +example x = SymFC.boolean $ x == Just False ``` -For types that are not algebraic, `Pantomime` exposes an interface to interpret them as SMT solver primitives. For example, the `Int64#` type and its operation `plusInt64#` have a natural embedding with the SMT primitive `BitVec 64` and its respective addition operation. In Pantomime, the user can directly encode this mapping within the annotation: +For types that are not algebraic, `SymFC` exposes an interface to interpret them as SMT solver primitives. For example, the `Int64#` type and its operation `plusInt64#` have a natural embedding with the SMT primitive `BitVec 64` and its respective addition operation. In SymFC, the user can directly encode this mapping within the annotation: ```haskell axioms :: PluginAxioms axioms = PluginAxioms - { typeAxioms = fromList [(''Int64#, ''Pantomime.BitVec 64)] - , termAxioms = [('plusInt64#, 'Pantomime.bvadd)] + { typeAxioms = fromList [(''Int64#, ''SymFC.BitVec 64)] + , termAxioms = [('plusInt64#, 'SymFC.bvadd)] } {-# ANN example (Theory axioms) #-} -example :: ... -> Pantomime.Bool +example :: ... -> SymFC.Bool ``` -For a reasonable mapping of `base`, check out [`pantomime-base`](https://github.com/PLSec-VU/pantomime-base). We also provide a mapping for `CLaSH` types and functions in [`pantomime-clash`](https://github.com/PLSec-VU/pantomime-clash). +For a reasonable mapping of `base`, check out [`sym-fc-base`](https://github.com/PLSec-VU/sym-fc-base). We also provide a mapping for `CLaSH` types and functions in [`sym-fc-clash`](https://github.com/PLSec-VU/sym-fc-clash). ```haskell -{-# ANN example (Theory Pantomime.Base.axioms) #-} -example :: ... -> Pantomime.Bool +{-# ANN example (Theory SymFC.Base.axioms) #-} +example :: ... -> SymFC.Bool ``` TODO: Writing mappings is a bit more involved, we should have some separate document where we go more in depth. There are whole lot of pitfalls... -TODO: Add explanation in the pantomime-clash and pantomime-base repositories. +TODO: Add explanation in the sym-fc-clash and sym-fc-base repositories. TODO: Extend explanation on PluginAxiom (at least that its a monoid and how it imports and what order). TODO: I would actually like to move most of the explanation here into the project documentation. I think it only makes sense once we have a haddock page for it however. diff --git a/package.yaml b/package.yaml index 3319cb5..1f8726a 100644 --- a/package.yaml +++ b/package.yaml @@ -1,6 +1,6 @@ -name: pantomime +name: sym-fc version: 0.1.0.0 -github: "PLSec-VU/pantomime" +github: "PLSec-VU/sym-fc" license: BSD-3-Clause author: "Robin Webbers" maintainer: "robin_webbers_1@hotmail.com" @@ -17,7 +17,7 @@ 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 @@ -92,7 +92,7 @@ library: - recursion-schemes tests: - pantomime-test: + sym-fc-test: main: Spec.hs source-dirs: test ghc-options: @@ -100,7 +100,7 @@ tests: - -rtsopts - -with-rtsopts=-N dependencies: - - pantomime + - sym-fc - hspec - hspec-expectations - HUnit diff --git a/src/Effectful/GHC/CoreE.hs b/src/Effectful/GHC/CoreE.hs index fe642a1..22f1a98 100644 --- a/src/Effectful/GHC/CoreE.hs +++ b/src/Effectful/GHC/CoreE.hs @@ -1,6 +1,5 @@ --- TODO: I guess this doesn't really need to be part of Pantomime? Maybe it --- should be split into a separate package? Otherwise, we can keep it here for --- now. +-- TODO: I guess this doesn't really need to be part of this package? Maybe it +-- should be split into a separate 'effectful-ghc' package? module Effectful.GHC.CoreE ( CoreE , liftCore diff --git a/src/Pantomime/Marker.hs b/src/Pantomime/Marker.hs deleted file mode 100644 index 4bc8486..0000000 --- a/src/Pantomime/Marker.hs +++ /dev/null @@ -1,18 +0,0 @@ -module Pantomime.Marker - ( pantomimeMarker - , pantomimeNothing - , pantomimeJust - ) where - -pantomimeMarker :: String -> Maybe String -pantomimeMarker name = error $ - "The marker function 'pantomimeMarker' for '" ++ name ++ "' was not replaced by the GHC compiler plugin pass." -{-# NOINLINE pantomimeMarker #-} - -pantomimeNothing :: Maybe String -pantomimeNothing = Nothing -{-# NOINLINE pantomimeNothing #-} - -pantomimeJust :: String -> Maybe String -pantomimeJust x = Just x -{-# NOINLINE pantomimeJust #-} diff --git a/src/Pantomime/TH.hs b/src/Pantomime/TH.hs deleted file mode 100644 index b50cb71..0000000 --- a/src/Pantomime/TH.hs +++ /dev/null @@ -1,13 +0,0 @@ -{-# LANGUAGE TemplateHaskellQuotes #-} - -module Pantomime.TH - ( pantomime - ) where - -import Language.Haskell.TH qualified as TH -import Pantomime.Marker - -pantomime :: TH.Name -> TH.Q TH.Exp -pantomime name = do - let nameStr = TH.nameBase name - pure $ TH.AppE (TH.VarE 'pantomimeMarker) (TH.LitE (TH.StringL nameStr)) diff --git a/src/Pantomime.hs b/src/SymFC.hs similarity index 69% rename from src/Pantomime.hs rename to src/SymFC.hs index 298a162..4c3b2e6 100644 --- a/src/Pantomime.hs +++ b/src/SymFC.hs @@ -1,23 +1,23 @@ {-# LANGUAGE DuplicateRecordFields #-} -module Pantomime +module SymFC ( plugin , Theory (..) , Embeddings (..) - , pantomime - , pantomimeMarker - , pantomimeNothing - , pantomimeJust + , symFC + , symFCMarker + , symFCNothing + , symFCJust ) where import GHC.Plugins hiding (empty, (<>)) -import Pantomime.Annotation -import Pantomime.Embed -import Pantomime.Passes -import Pantomime.TH (pantomime) -import Pantomime.Marker +import SymFC.Annotation +import SymFC.Embed +import SymFC.Passes +import SymFC.TH (symFC) +import SymFC.Marker plugin :: Plugin diff --git a/src/Pantomime/Annotation.hs b/src/SymFC/Annotation.hs similarity index 88% rename from src/Pantomime/Annotation.hs rename to src/SymFC/Annotation.hs index cfadf2f..427c56a 100644 --- a/src/Pantomime/Annotation.hs +++ b/src/SymFC/Annotation.hs @@ -1,12 +1,12 @@ {-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE OverloadedStrings #-} -module Pantomime.Annotation +module SymFC.Annotation ( Theory (..) ) where import Data.Data (Data) -import Pantomime.Embed (Embeddings) +import SymFC.Embed (Embeddings) import GHC.Utils.Outputable (Outputable (..), hang) -- TODO: Not sure I like the name. This checks whether an expression whose diff --git a/src/Pantomime/BuiltIn.hs b/src/SymFC/BuiltIn.hs similarity index 98% rename from src/Pantomime/BuiltIn.hs rename to src/SymFC/BuiltIn.hs index e577649..6de9889 100644 --- a/src/Pantomime/BuiltIn.hs +++ b/src/SymFC/BuiltIn.hs @@ -21,7 +21,7 @@ -- Many of the helper functions will look verbose and are written in a somewhat -- roundabout way. This is intentional, do not change them unless you know what -- you're doing! -module Pantomime.BuiltIn +module SymFC.BuiltIn -- | Embeddable constraint for user interpretations. ( Embeddable , Embedding (..) @@ -102,7 +102,7 @@ module Pantomime.BuiltIn , natVal -- TODO: Why is this an ambigous import without the fully qualified path this? -- The other SNat pattern synonym is a qualified import... - , SNat (Pantomime.BuiltIn.SNat) + , SNat (SymFC.BuiltIn.SNat) , (%+) , (%-) , cmpNat @@ -253,8 +253,8 @@ import Grisette , IntN ) import Grisette.Internal.SymPrim.Array qualified as Grisette -import Pantomime.Util (unsafeEq, foldrBy) -import Pantomime.Util qualified as Util (BitVec, (%+)) +import SymFC.Util (unsafeEq, foldrBy) +import SymFC.Util qualified as Util (BitVec, (%+)) import Prelude qualified as Base import Prelude ( Applicative (..) @@ -488,7 +488,7 @@ type PlatformWordSize = 64 -- document this once and have the instances reference this? -- -- Actually though, it would be good to have functions to switch between Haskell --- and Pantomime types, as one would perhaps also want to use these if they +-- and SymFC types, as one would perhaps also want to use these if they -- plan on actually using these primitives for some check. {-# OPAQUE toInt# #-} toInt# :: BitVec PlatformWordSize -> Int# @@ -574,10 +574,10 @@ fromWord64# w# = Base.fromIntegral $ W64# w# toInteger :: Integer -> Base.Integer toInteger = coerce --- | Convert a Haskell 'Integer' to a pantomime 'Integer'. +-- | Convert a Haskell 'Integer' to a symbolic 'Integer'. -- -- This function will be used to implement the 'Num' typeclass 'fromInteger' --- for pantomime 'Integer', and as such will allow one to write their literals. +-- for symbolic 'Integer', and as such will allow one to write their literals. -- -- As the conversion depends on the interpretation of haskell 'Integer', we can -- only ask a user to provide an instance for this. @@ -638,7 +638,7 @@ litAlts' cmp alts def !scrut = do foldrBy (def scrut) alts \(lit, rhs) acc -> do ite (cmp scrut lit) (rhs scrut) acc --- | 'KnownNat' constraint using Pantomime primitive 'Integer'. +-- | 'KnownNat' constraint using symbolic primitive 'Integer'. class KnownNat (n :: Nat) where natSing :: SNat n @@ -654,7 +654,7 @@ instance HasDict (KnownNat n) (SNat n) where natVal :: forall n. KnownNat n => Integer natVal = let UnsafeSNat i = natSing @n in i --- | Singleton natural number using Pantomime primitive 'Integer'. +-- | Singleton natural number using symbolic primitive 'Integer'. newtype SNat (n :: Nat) where UnsafeSNat :: Integer -> SNat n @@ -842,7 +842,7 @@ undefinedBehaviour = noinline undefinedBehaviour -- TODO: Another thing to look into is conversion between primitive types. Idk -- if there for example is a primitive operation to convert between an boolean -- and a single-bit bitvector. --- | Pantomime primitive Boolean. +-- | Symbolic primitive Boolean. newtype Bool where Bool :: Base.Bool -> Bool @@ -906,7 +906,7 @@ boolean = \case convert :: Bool -> Base.Bool convert value = ite value Base.True Base.False --- | Pantomime primitive integer. +-- | Symbolic primitive integer. newtype Integer where Integer :: Base.Integer -> Integer @@ -970,7 +970,7 @@ ile = coerce $ (Base.<=) @Base.Integer ilt :: Integer -> Integer -> Bool ilt = coerce $ (Base.<) @Base.Integer --- | Pantomime primitive bitvector. +-- | Symbolic primitive bitvector. data BitVec (n :: Nat) where BitVec :: (Base.KnownNat n, 1 <= n) => Util.BitVec n -> BitVec n @@ -1085,7 +1085,8 @@ bvs2i (BitVec x) = Integer $ Base.toInteger (bitCast @_ @(IntN n) x) bvsize' :: forall n. BitVec n -> Integer bvsize' BitVec {} = Integer $ Base.natVal @n Proxy --- TODO: I think we can actually just implement this one directly in Pantomime. +-- TODO: I think we can actually just implement this one directly in SymFC as +-- 'UnsafeSNat' is just a newtype around the symbolic 'Integer'. -- I guess it is perhaps prettier than exposing the current bvsize'. bvsize :: forall n. BitVec n -> SNat n bvsize bv = UnsafeSNat @n $ bvsize' bv diff --git a/src/Pantomime/Embed.hs b/src/SymFC/Embed.hs similarity index 99% rename from src/Pantomime/Embed.hs rename to src/SymFC/Embed.hs index 87ad5a2..15ec30c 100644 --- a/src/Pantomime/Embed.hs +++ b/src/SymFC/Embed.hs @@ -1,6 +1,6 @@ {-# LANGUAGE OverloadedStrings #-} -module Pantomime.Embed +module SymFC.Embed ( Embeddings (..) , EmbeddingsR (..) , TypeEmbeddingsR @@ -87,9 +87,9 @@ import Effectful.GHC.TH import Effectful.GHC.TyThing import Effectful.GHC.Unique (HasUnique) -import Pantomime.BuiltIn (Embeddable, Embedding (..)) -import Pantomime.Unification (subsumeExpr) -import Pantomime.Util (foldM') +import SymFC.BuiltIn (Embeddable, Embedding (..)) +import SymFC.Unification (subsumeExpr) +import SymFC.Util (foldM') -- TODO: The text below should be updated to reflect the current state of -- embeddings. We should at some point link the paper also. diff --git a/src/Pantomime/Literal.hs b/src/SymFC/Literal.hs similarity index 98% rename from src/Pantomime/Literal.hs rename to src/SymFC/Literal.hs index 44775aa..3297902 100644 --- a/src/Pantomime/Literal.hs +++ b/src/SymFC/Literal.hs @@ -3,7 +3,7 @@ {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ViewPatterns #-} -module Pantomime.Literal +module SymFC.Literal -- | The primary export of this module. -- -- This contains the 'Literal' itself as well as its type and typeclass @@ -44,7 +44,7 @@ import Grisette import Grisette.Internal.SymPrim.Prim.Term (SupportedNonFuncPrim) import Grisette.Internal.SymPrim.SymArray (SymArray) -import Pantomime.Util (KnownPos, SymBitVec, impossible) +import SymFC.Util (KnownPos, SymBitVec, impossible) class -- TODO: I'm not sure if I should have these here or somewhere else, as we can diff --git a/src/SymFC/Marker.hs b/src/SymFC/Marker.hs new file mode 100644 index 0000000..53cf8bb --- /dev/null +++ b/src/SymFC/Marker.hs @@ -0,0 +1,18 @@ +module SymFC.Marker + ( symFCMarker + , symFCNothing + , symFCJust + ) where + +symFCMarker :: String -> Maybe String +symFCMarker name = error $ + "The marker function 'symFCMarker' for '" ++ name ++ "' was not replaced by the GHC compiler plugin pass." +{-# NOINLINE symFCMarker #-} + +symFCNothing :: Maybe String +symFCNothing = Nothing +{-# NOINLINE symFCNothing #-} + +symFCJust :: String -> Maybe String +symFCJust x = Just x +{-# NOINLINE symFCJust #-} diff --git a/src/Pantomime/Orphan/GHC.hs b/src/SymFC/Orphan/GHC.hs similarity index 99% rename from src/Pantomime/Orphan/GHC.hs rename to src/SymFC/Orphan/GHC.hs index 5043096..b75e8b2 100644 --- a/src/Pantomime/Orphan/GHC.hs +++ b/src/SymFC/Orphan/GHC.hs @@ -8,7 +8,7 @@ -- -- Specifically, we wish to place GHC types inside of a Grisette Union, which -- requires the 'Mergeable' typeclass instance. -module Pantomime.Orphan.GHC +module SymFC.Orphan.GHC ( Generically (..) , Uniquely (..) ) where diff --git a/src/Pantomime/Orphan/Grisette.hs b/src/SymFC/Orphan/Grisette.hs similarity index 97% rename from src/Pantomime/Orphan/Grisette.hs rename to src/SymFC/Orphan/Grisette.hs index 7819e25..09de57f 100644 --- a/src/Pantomime/Orphan/Grisette.hs +++ b/src/SymFC/Orphan/Grisette.hs @@ -2,7 +2,7 @@ {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ViewPatterns #-} -module Pantomime.Orphan.Grisette +module SymFC.Orphan.Grisette ( pattern Single , pattern If ) where diff --git a/src/Pantomime/Passes.hs b/src/SymFC/Passes.hs similarity index 94% rename from src/Pantomime/Passes.hs rename to src/SymFC/Passes.hs index c98aaf5..2b7da07 100644 --- a/src/Pantomime/Passes.hs +++ b/src/SymFC/Passes.hs @@ -1,4 +1,4 @@ -module Pantomime.Passes +module SymFC.Passes ( printAndLintPass , checkValidityPass ) where @@ -18,16 +18,16 @@ import Data.Data (Data) import Data.Traversable (for) import Data.Maybe (catMaybes) import Data.ByteString.Char8 qualified as BS8 -import Pantomime.Marker +import SymFC.Marker import Control.Error import Language.Haskell.TH qualified as TH -import Pantomime.Solve -import Pantomime.Unification -import Pantomime.Embed (resolveEmbeddings) -import Pantomime.Annotation +import SymFC.Solve +import SymFC.Unification +import SymFC.Embed (resolveEmbeddings) +import SymFC.Annotation import Effectful import Effectful.Provider @@ -228,9 +228,9 @@ checkValidityAndEmbed checkValidityAndEmbed guts = do (_, anns) <- getFirstAnnotations @Theory deserializeWithData guts - markerPrimeId <- thNameToGhcName 'pantomimeMarker >>= lookupIdAll - nothingId <- thNameToGhcName 'pantomimeNothing >>= lookupIdAll - justId <- thNameToGhcName 'pantomimeJust >>= lookupIdAll + markerPrimeId <- thNameToGhcName 'symFCMarker >>= lookupIdAll + nothingId <- thNameToGhcName 'symFCNothing >>= lookupIdAll + justId <- thNameToGhcName 'symFCJust >>= lookupIdAll (binds, results) <- unzip <$> for (mg_binds guts) \case NonRec x e | Just (Theory embeddings) <- lookupUFM anns $ varName x -> do @@ -259,7 +259,7 @@ checkValidityAndEmbed guts = do pure guts { mg_binds = binds' } -- | Recursively traverses all bindings in the module and replaces occurrences of --- the 'pantomimeMarker' call with the pre-generated proof result expressions. +-- the 'symFCMarker' call with the pre-generated proof result expressions. replaceMarkerInBinds :: Id -> [(String, CoreExpr)] @@ -270,7 +270,7 @@ replaceMarkerInBinds markerPrimeId results = map goBind goBind (NonRec b e) = NonRec b (replaceMarker markerPrimeId results e) goBind (Rec bs) = Rec (map (\(b, e) -> (b, replaceMarker markerPrimeId results e)) bs) --- | Replaces any application of the 'pantomimeMarker' with its corresponding +-- | Replaces any application of the 'symFCMarker' with its corresponding -- compile-time Z3 proof result expression. replaceMarker :: Id @@ -322,7 +322,7 @@ exprToString (App (Var f) (Lit (LitString bs))) exprToString (Lit (LitString bs)) = Just (BS8.unpack bs) exprToString _ = Nothing --- | Scans the Core bindings for any call to 'pantomimeMarker' and returns the +-- | Scans the Core bindings for any call to 'symFCMarker' and returns the -- names of all assertions that are referenced by a splice but lack the corresponding -- 'Theory' annotation. findMissingAnnotations diff --git a/src/Pantomime/PrimOp.hs b/src/SymFC/PrimOp.hs similarity index 99% rename from src/Pantomime/PrimOp.hs rename to src/SymFC/PrimOp.hs index a2ac77a..bf3a420 100644 --- a/src/Pantomime/PrimOp.hs +++ b/src/SymFC/PrimOp.hs @@ -1,7 +1,7 @@ {-# LANGUAGE MagicHash #-} -- | Module defining the symbolic primitives and helper functions. -module Pantomime.PrimOp +module SymFC.PrimOp -- | Primitive operations and its functions. ( PrimOp (..) , arity @@ -12,7 +12,7 @@ import GHC.Plugins (Arity, Outputable (ppr)) import GHC.Generics (Generic) import Grisette (Mergeable, Default (..)) import Language.Haskell.TH qualified as TH -import Pantomime.BuiltIn qualified as Builtin +import SymFC.BuiltIn qualified as Builtin import Prelude hiding (lookup) import Unsafe.Coerce qualified as Builtin (unsafeEqualityProof) diff --git a/src/Pantomime/Solve.hs b/src/SymFC/Solve.hs similarity index 95% rename from src/Pantomime/Solve.hs rename to src/SymFC/Solve.hs index 699c6ec..ad42eed 100644 --- a/src/Pantomime/Solve.hs +++ b/src/SymFC/Solve.hs @@ -1,4 +1,4 @@ -module Pantomime.Solve +module SymFC.Solve ( checkValid ) where @@ -23,10 +23,10 @@ import Control.Monad.Except (runExceptT) import Data.Traversable (for) import Language.Haskell.TH qualified as TH -import Pantomime.BuiltIn qualified as Builtin -import Pantomime.Util (dbg) -import Pantomime.Embed (EmbeddingsR (..)) -import Pantomime.WHNF qualified as WHNF +import SymFC.BuiltIn qualified as Builtin +import SymFC.Util (dbg) +import SymFC.Embed (EmbeddingsR (..)) +import SymFC.WHNF qualified as WHNF import Effectful import Effectful.Context diff --git a/src/SymFC/TH.hs b/src/SymFC/TH.hs new file mode 100644 index 0000000..f885b3a --- /dev/null +++ b/src/SymFC/TH.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE TemplateHaskellQuotes #-} + +module SymFC.TH + ( symFC + ) where + +import Language.Haskell.TH qualified as TH +import SymFC.Marker + +symFC :: TH.Name -> TH.Q TH.Exp +symFC name = do + let nameStr = TH.nameBase name + pure $ TH.AppE (TH.VarE 'symFCMarker) (TH.LitE (TH.StringL nameStr)) diff --git a/src/Pantomime/Tsil.hs b/src/SymFC/Tsil.hs similarity index 98% rename from src/Pantomime/Tsil.hs rename to src/SymFC/Tsil.hs index 81e4caa..771db7b 100644 --- a/src/Pantomime/Tsil.hs +++ b/src/SymFC/Tsil.hs @@ -2,7 +2,7 @@ {-# LANGUAGE DerivingVia #-} {-# LANGUAGE ViewPatterns #-} -module Pantomime.Tsil +module SymFC.Tsil ( Tsil (Tsil, Lin, Snoc) ) where diff --git a/src/Pantomime/Unification.hs b/src/SymFC/Unification.hs similarity index 99% rename from src/Pantomime/Unification.hs rename to src/SymFC/Unification.hs index d0fcb33..16863ae 100644 --- a/src/Pantomime/Unification.hs +++ b/src/SymFC/Unification.hs @@ -1,9 +1,9 @@ {-# LANGUAGE OverloadedStrings #-} --- TODO: Rename to Pantomime.Unify, I think it's cleaner and it also mirrors the +-- TODO: Rename to SymFC.Unify, I think it's cleaner and it also mirrors the -- naming from GHC. -- TODO: Add module docs. -module Pantomime.Unification +module SymFC.Unification ( UnificationError (..) , OversaturatedError (..) , unifyApp @@ -38,7 +38,7 @@ import GHC.Plugins hiding ((<>)) import GHC.Tc.Utils.TcType (substTy, tcSplitSigmaTy) import Lens.Micro import Lens.Micro.Extras (view) -import Pantomime.Util +import SymFC.Util import Prelude hiding (break) -- | Error to indicate unification failure. diff --git a/src/Pantomime/Util.hs b/src/SymFC/Util.hs similarity index 99% rename from src/Pantomime/Util.hs rename to src/SymFC/Util.hs index 93d1e23..c03f81d 100644 --- a/src/Pantomime/Util.hs +++ b/src/SymFC/Util.hs @@ -3,7 +3,7 @@ {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE UndecidableInstances #-} -module Pantomime.Util +module SymFC.Util ( KnownPos , SymBitVec , BitVec diff --git a/src/Pantomime/WHNF.hs b/src/SymFC/WHNF.hs similarity index 99% rename from src/Pantomime/WHNF.hs rename to src/SymFC/WHNF.hs index aac7327..3855a9c 100644 --- a/src/Pantomime/WHNF.hs +++ b/src/SymFC/WHNF.hs @@ -2,7 +2,7 @@ {-# LANGUAGE MagicHash #-} {-# LANGUAGE OverloadedLists #-} -module Pantomime.WHNF +module SymFC.WHNF ( WHNF , Value (..) , Literal (..) @@ -145,8 +145,8 @@ import Grisette import Grisette qualified import Grisette.Internal.SymPrim.SymArray qualified as Grisette.Array import Language.Haskell.TH qualified as TH -import Pantomime.BuiltIn qualified as Builtin -import Pantomime.Literal +import SymFC.BuiltIn qualified as Builtin +import SymFC.Literal ( Literal (..) , LiteralType (..) , LiteralTypeable (..) @@ -155,12 +155,12 @@ import Pantomime.Literal , eqLiteralType , literalTypeOf ) -import Pantomime.PrimOp (PrimOp (..)) -import Pantomime.PrimOp qualified as PrimOp -import Pantomime.Orphan.GHC () -import Pantomime.Orphan.Grisette (pattern Single, pattern If) -import Pantomime.Tsil -import Pantomime.Util +import SymFC.PrimOp (PrimOp (..)) +import SymFC.PrimOp qualified as PrimOp +import SymFC.Orphan.GHC () +import SymFC.Orphan.Grisette (pattern Single, pattern If) +import SymFC.Tsil +import SymFC.Util ( SymBitVec , SomeBitVec (..) , KnownPos diff --git a/pantomime.cabal b/sym-fc.cabal similarity index 82% rename from pantomime.cabal rename to sym-fc.cabal index 3b54afb..c4b2d34 100644 --- a/pantomime.cabal +++ b/sym-fc.cabal @@ -4,11 +4,11 @@ cabal-version: 2.2 -- -- see: https://github.com/sol/hpack -name: pantomime +name: sym-fc version: 0.1.0.0 -description: Please see the README on GitHub at -homepage: https://github.com/PLSec-VU/pantomime#readme -bug-reports: https://github.com/PLSec-VU/pantomime/issues +description: Please see the README on GitHub at +homepage: https://github.com/PLSec-VU/sym-fc#readme +bug-reports: https://github.com/PLSec-VU/sym-fc/issues author: Robin Webbers maintainer: robin_webbers_1@hotmail.com copyright: 2026 Robin Webbers @@ -21,7 +21,7 @@ extra-source-files: source-repository head type: git - location: https://github.com/PLSec-VU/pantomime + location: https://github.com/PLSec-VU/sym-fc library exposed-modules: @@ -37,26 +37,26 @@ library Effectful.GHC.TyThing Effectful.GHC.Unique Effectful.Grisette.Solver - Pantomime - Pantomime.Annotation - Pantomime.BuiltIn - Pantomime.Embed - Pantomime.Literal - Pantomime.Marker - Pantomime.Orphan.GHC - Pantomime.Orphan.Grisette - Pantomime.Passes - Pantomime.PrimOp - Pantomime.Solve - Pantomime.TH - Pantomime.Tsil - Pantomime.Unification - Pantomime.Util - Pantomime.WHNF + SymFC + SymFC.Annotation + SymFC.BuiltIn + SymFC.Embed + SymFC.Literal + SymFC.Marker + SymFC.Orphan.GHC + SymFC.Orphan.Grisette + SymFC.Passes + SymFC.PrimOp + SymFC.Solve + SymFC.TH + SymFC.Tsil + SymFC.Unification + SymFC.Util + SymFC.WHNF other-modules: - Paths_pantomime + Paths_sym_fc autogen-modules: - Paths_pantomime + Paths_sym_fc hs-source-dirs: src default-extensions: @@ -114,13 +114,13 @@ library , unordered-containers default-language: Haskell2010 -test-suite pantomime-test +test-suite sym-fc-test type: exitcode-stdio-1.0 main-is: Spec.hs other-modules: - Paths_pantomime + Paths_sym_fc autogen-modules: - Paths_pantomime + Paths_sym_fc hs-source-dirs: test default-extensions: @@ -165,7 +165,7 @@ test-suite pantomime-test , hspec , hspec-expectations , mtl - , pantomime , silently + , sym-fc , template-haskell default-language: Haskell2010 diff --git a/test/Spec.hs b/test/Spec.hs index 0c6d890..ed990ca 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -1,4 +1,4 @@ -{-# OPTIONS_GHC -fplugin=Pantomime #-} +{-# OPTIONS_GHC -fplugin=SymFC #-} {-# LANGUAGE BlockArguments #-} module Main @@ -7,8 +7,8 @@ module Main import Test.Hspec -import Pantomime -import Pantomime.BuiltIn qualified as SymFC +import SymFC +import SymFC.BuiltIn qualified as SymFC -- ============================================================================= -- Test Case Definitions @@ -39,12 +39,12 @@ invalidAssertion = do main :: IO () main = hspec $ do - describe "Pantomime Symbolic Checker Unit Tests" $ do + describe "SymFC Symbolic Checker Unit Tests" $ do it "verifies validAssertion (should succeed with Nothing)" $ do - $(pantomime 'validAssertion) `shouldBe` Nothing + $(symFC 'validAssertion) `shouldBe` Nothing it "detects invalidAssertion (should fail with Just counterexample)" $ do - checkInvalid $(pantomime 'invalidAssertion) + checkInvalid $(symFC 'invalidAssertion) -- | Assert that a counterexample was found and print it. checkInvalid :: Maybe String -> Expectation