RFC: crucible-llvm: Don't represent architecture at the type level

crucible-llvm/crucible-llvm.cabal

@@ -95,6 +95,7 @@ library
   other-modules:
     Lang.Crucible.LLVM.Errors.Standards
     Lang.Crucible.LLVM.Extension.Arch
+    Lang.Crucible.LLVM.Extension.PtrSize
     Lang.Crucible.LLVM.Extension.Syntax
     Lang.Crucible.LLVM.Intrinsics.Common
     Lang.Crucible.LLVM.Intrinsics.Libc

crucible-llvm/src/Lang/Crucible/LLVM/Extension.hs

@@ -17,6 +17,7 @@
 
 module Lang.Crucible.LLVM.Extension
   ( module Lang.Crucible.LLVM.Extension.Arch
+  , module Lang.Crucible.LLVM.Extension.PtrSize
   , module Lang.Crucible.LLVM.Extension.Syntax
   , LLVM
   ) where
@@ -28,6 +29,7 @@ import GHC.Generics ( Generic )
 import Lang.Crucible.CFG.Extension
 
 import Lang.Crucible.LLVM.Extension.Arch
+import Lang.Crucible.LLVM.Extension.PtrSize
 import Lang.Crucible.LLVM.Extension.Syntax
 
 -- | The Crucible extension type marker for LLVM.

crucible-llvm/src/Lang/Crucible/LLVM/Extension/Arch.hs

@@ -8,12 +8,11 @@
 ------------------------------------------------------------------------
 
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module Lang.Crucible.LLVM.Extension.Arch
   ( type LLVMArch
@@ -22,32 +21,35 @@ module Lang.Crucible.LLVM.Extension.Arch
   , ArchRepr(..)
   ) where
 
-import           GHC.Generics (Generic)
 import           Data.Parameterized (NatRepr)
 import           Data.Parameterized.Classes (OrdF(..))
 import qualified Data.Parameterized.TH.GADT as U
 import           Data.Type.Equality (TestEquality(..))
-import           Data.Typeable (Typeable)
 import           GHC.TypeLits (Nat)
 
+import           Lang.Crucible.LLVM.Extension.PtrSize
+
 -- | Data kind for representing LLVM architectures.
---   Currently only X86 variants are supported.
-data LLVMArch = X86 Nat
-  deriving (Generic, Typeable)
+type LLVMArch = PtrSize
+{-# DEPRECATED LLVMArch "Use Lang.Crucible.LLVM.Extension.PtrSize" #-}
 
 -- | LLVM Architecture tag for X86 variants
 --
 --   @X86 :: Nat -> LLVMArch@
-type X86 = 'X86
+type X86 = 'PtrSize
+{-# DEPRECATED X86 "Use Lang.Crucible.LLVM.Extension.PtrSize" #-}
 
 -- | Type family defining the native machine word size
 --   for a given architecture.
 type family ArchWidth (arch :: LLVMArch) :: Nat where
-  ArchWidth (X86 wptr) = wptr
+  ArchWidth ptrsz = PtrSizeBits ptrsz
+{-# DEPRECATED ArchWidth "Use Lang.Crucible.LLVM.Extension.PtrSize" #-}
 
 -- | Runtime representation of architectures.
 data ArchRepr (arch :: LLVMArch) where
   X86Repr :: NatRepr w -> ArchRepr (X86 w)
+{-# DEPRECATED ArchRepr "Use Lang.Crucible.LLVM.Extension.PtrSize" #-}
+{-# DEPRECATED X86Repr "Use Lang.Crucible.LLVM.Extension.PtrSize" #-}
 
 $(return [])
 

crucible-llvm/src/Lang/Crucible/LLVM/Extension/PtrSize.hs

@@ -0,0 +1,67 @@
+-- |
+-- Module           : Lang.Crucible.LLVM.PtrSize
+-- Description      : Type-level representation of LLVM pointer width
+-- Copyright        : (c) Galois, Inc 2022
+-- License          : BSD3
+-- Maintainer       : langston@galois.com
+-- Stability        : provisional
+--
+-- The Crucible type of LLVM pointers
+-- ('Lang.Crucible.LLVM.MemModel.Pointer.LLVMPointerType') explicitly represents
+-- the size of pointers at the type level, which can help prevent ill-typed
+-- expressions from being formed. This module provides a data kind ('PtrSize')
+-- and corresponding singleton ('PtrSizeRepr') for representing the size of
+-- pointers in a given LLVM module (which can be derived from the module's
+-- target triple and/or data layout).
+------------------------------------------------------------------------
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Lang.Crucible.LLVM.Extension.PtrSize
+  ( type PtrSize(PtrSize)
+  , PtrSizeRepr(..)
+  , PtrSizeBits
+  ) where
+
+import           Data.Kind (Type)
+
+import           Data.Parameterized (NatRepr)
+import           Data.Parameterized.Classes (OrdF(..))
+import qualified Data.Parameterized.TH.GADT as U
+import           Data.Type.Equality (TestEquality(..))
+import           GHC.TypeLits (Nat)
+
+-- | Data kind for representing pointer width. Size is measured in number of
+-- bits.
+--
+-- TODO(lb): Stop exporting the constructor when Arch.hs is removed.
+data PtrSize = PtrSize Nat
+
+-- | Get the width of pointers, measured in number of bits.
+type PtrSizeBits :: PtrSize -> Nat
+type family PtrSizeBits ptrsz where
+  PtrSizeBits ('PtrSize wptr) = wptr
+
+-- | Runtime representation of pointer width.
+type PtrSizeRepr :: PtrSize -> Type
+data PtrSizeRepr ptrsz where
+  PtrSizeRepr :: NatRepr wptr -> PtrSizeRepr ('PtrSize wptr)
+
+$(return [])
+
+instance TestEquality PtrSizeRepr where
+  testEquality =
+    $(U.structuralTypeEquality [t|PtrSizeRepr|]
+        [ (U.ConType [t|NatRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
+        ])
+
+instance OrdF PtrSizeRepr where
+  compareF =
+    $(U.structuralTypeOrd [t|PtrSizeRepr|]
+        [ (U.ConType [t|NatRepr|] `U.TypeApp` U.AnyType, [|compareF|])
+        ])

crux-llvm/CHANGELOG.md

@@ -10,12 +10,20 @@ subset of functions in a bitcode module are actually executed.
 
 * Added support for the `cvc5` SMT solver.
 
-* Added support for getting abducts during online goal solving. With 
-the `--get-abducts n` option, `crux-llvm` returns `n` abducts for 
+* Added support for getting abducts during online goal solving. With
+the `--get-abducts n` option, `crux-llvm` returns `n` abducts for
 each goal that the SMT solver found to be `sat`. An abduct is a formula
-that makes the goal `unsat` (would help the SMT solver prove the goal). 
+that makes the goal `unsat` (would help the SMT solver prove the goal).
 This feature only works with the `cvc5` SMT solver.
 
+## Library changes
+
+* Stop representing the "LLVM architecture" at the type level with the `LLVMArch`
+  and `ArchRepr` types. These were previously always set to x86 regardless of the
+  target triple. Instead, represent the pointer width directly with `PtrWidth`.
+  `LLVMArch` and related functionality will still work in this release, but
+  are deprecated and will be removed in the next release.
+
 # 0.6
 
 ## New features