From 2bc5e255c8dcd1ff492e6afb09db36a3ab8b1612 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 28 Sep 2022 12:22:02 -0400 Subject: [PATCH] crucible-llvm: Type-level pointer width, rather than architecture It's necessary to represent the pointer width at the type level in order to statically prevent the formation of ill-typed Crucible/What4 expressions. However, there is no similar motivation for representing architectures at the type level. The previous state of affairs was incoherent in the sense that we always provided an `ArchRepr` signaling the use of x86, without actually checking that this architecture was in use: https://github.com/GaloisInc/crucible/blob/041975a5ad4200633613ed30df144c3a9d0e9403/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Monad.hs#L113 We could have fixed this by checking the target triple (functionality recently added to llvm-pretty{,-bc-parser}) and adding constructors for more architectures to `ArchRepr`, but as discussed above there's no motivation to actually do this. --- crucible-llvm/crucible-llvm.cabal | 1 + .../src/Lang/Crucible/LLVM/Extension.hs | 2 + .../src/Lang/Crucible/LLVM/Extension/Arch.hs | 20 +++--- .../Lang/Crucible/LLVM/Extension/PtrSize.hs | 67 +++++++++++++++++++ crux-llvm/CHANGELOG.md | 14 +++- 5 files changed, 92 insertions(+), 12 deletions(-) create mode 100644 crucible-llvm/src/Lang/Crucible/LLVM/Extension/PtrSize.hs diff --git a/crucible-llvm/crucible-llvm.cabal b/crucible-llvm/crucible-llvm.cabal index 6e5da7eac..462c3f1cf 100644 --- a/crucible-llvm/crucible-llvm.cabal +++ b/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 diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Extension.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Extension.hs index 2efaf189e..251d4fee2 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Extension.hs +++ b/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. diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Extension/Arch.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Extension/Arch.hs index f16e89e96..882aec694 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Extension/Arch.hs +++ b/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 []) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Extension/PtrSize.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Extension/PtrSize.hs new file mode 100644 index 000000000..66d11eb22 --- /dev/null +++ b/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|]) + ]) diff --git a/crux-llvm/CHANGELOG.md b/crux-llvm/CHANGELOG.md index bdd0c0842..32492988a 100644 --- a/crux-llvm/CHANGELOG.md +++ b/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