Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support opaque pointers in llvm_boilerplate/function skeletons #1877

Open
RyanGlScott opened this issue May 31, 2023 · 0 comments
Open

Support opaque pointers in llvm_boilerplate/function skeletons #1877

RyanGlScott opened this issue May 31, 2023 · 0 comments
Labels
crucible/llvm Related to crucible-llvm verification design-needed enhancement

Comments

@RyanGlScott
Copy link
Contributor

I have recently updated SAW to work with LLVM's opaque pointers, an LLVM language change that replaces pointers with explicit pointee types (e.g., i32*) with opaque pointers that lack pointee types. In an opaque pointer setting, all pointers have the type ptr, and LLVM determines how to interpret the underlying memory based on the types of instructions that the pointers are used in. For more information, see the following links:

While most parts of SAW now fully support opaque pointers, there is one part of SAW that cannot handle them at the moment: the llvm_boilerplate command. This is because llvm_boilerplate inspects the skeletons of LLVM function types to determine what boilerplate code to generate, and this code necessarily inspects pointee types. Look at this code to see what I mean:

parseType :: LLVM.Type -> IO TypeSkeleton
parseType (LLVM.PtrTo t) = pure $ TypeSkeleton t True [SizeGuess 1 True "default guess of size 1"]
parseType (LLVM.Array i t) = pure $ TypeSkeleton t True
[ SizeGuess (fromIntegral i) True $ "default guess of size " <> Text.pack (show i)
]
parseType t = pure $ TypeSkeleton t False []

This code records which types are pointers and records the pointee types. Later, these TypeSkeletons are used to generate SAWScript code, and different code is generated for pointers that makes use of the pointee types:

typeBoilerplate :: TypeSkeleton -> Text
typeBoilerplate t
| t ^. typeSkelIsPointer
, (s:_) <- t ^. typeSkelSizeGuesses
= mconcat
[ "(llvm_array "
, Text.pack . show $ s ^. sizeGuessElems
, " "
, llvmTypeBoilerplate $ t ^. typeSkelLLVMType
, ")"
]
| otherwise = llvmTypeBoilerplate $ t ^. typeSkelLLVMType

argPrecondition :: Int -> ArgSkeleton -> Text
argPrecondition i a
| a ^. argSkelType . typeSkelIsPointer
, (s:_) <- a ^. argSkelType . typeSkelSizeGuesses
, s ^. sizeGuessInitialized
= mconcat
[ " ", argName i a, " <- llvm_fresh_var \"", argName i a, "\" ", typeBoilerplate (a ^. argSkelType), ";\n"
, " ", argName i a, "_ptr <- llvm_alloc ", typeBoilerplate (a ^. argSkelType), ";\n"
, " llvm_points_to ", argName i a, "_ptr (llvm_term ", argName i a, ");\n\n"
]

It is not obvious how to adapt this code to work with opaque pointers, which lack pointee types entirely. SAW's llvm_alloc command requires a type to use, so where would we get this type from? Some half-baked ideas I have include:

  • Inspect the definitions of each LLVM function to see which instructions involve pointers, and use those instructions to infer the types of pointers' underlying memory. (This sounds quite complex in the general case.)
  • Add a variant of the function_skeleton command that allows users to specify what the types of pointers' underlying memory should be. (I'm unclear on what the design for this should look like.)

Because I am unclear on what the right approach should be, I have opted to make SAW error out whener it attempts to construct a skeleton for an opaque pointer type.

@RyanGlScott RyanGlScott added enhancement crucible/llvm Related to crucible-llvm verification design-needed labels May 31, 2023
RyanGlScott added a commit that referenced this issue May 31, 2023
This patch adds support for LLVM 15 and 16 by adding support for opaque
pointers, which are described in https://llvm.org/docs/OpaquePointers.html.  I
have also added a test case involving LLVM bitcode using opaque pointers to
kick the tires and ensure that the basics work as expected.

For the most part, this is a straightforward process, as most uses of pointer
types in SAW already do not care about pointee types. There are some
exceptions, however:

* The `typeOfSetupValue` function, as well as several places that use this
  function, scrutinize pointee types of pointers, which would appear to fly in
  the face of opaque pointers. I attempt to explain in #1876 which this is
  actually OK for now (although a bit awkward).
* The `llvm_boilerplate`/skeleton machinery does not support opaque pointers
  at all. See #1877.

This patch also bumps the following submodules to bring in support for opaque
pointers:

* `llvm-pretty`: GaloisInc/llvm-pretty#110
* `llvm-pretty-bc-parser`: GaloisInc/llvm-pretty-bc-parser#221
* `crucible`: GaloisInc/crucible#1085

This also bumps the `what4` submodule to bring in the changes from
GaloisInc/what4#234. This isn't necessary to support opaque pointers, but it
_is_ necessary to support a build plan involving `tasty-sugar-2.2.*`, which
`llvm-pretty-bc-parser`'s test suite now requires.
RyanGlScott added a commit that referenced this issue May 31, 2023
RyanGlScott added a commit that referenced this issue Jun 1, 2023
This patch adds support for LLVM 15 and 16 by adding support for opaque
pointers, which are described in https://llvm.org/docs/OpaquePointers.html.  I
have also added a test case involving LLVM bitcode using opaque pointers to
kick the tires and ensure that the basics work as expected.

For the most part, this is a straightforward process, as most uses of pointer
types in SAW already do not care about pointee types. There are some
exceptions, however:

* The `typeOfSetupValue` function, as well as several places that use this
  function, scrutinize pointee types of pointers, which would appear to fly in
  the face of opaque pointers. I attempt to explain in #1876 which this is
  actually OK for now (although a bit awkward).
* The `llvm_boilerplate`/skeleton machinery does not support opaque pointers
  at all. See #1877.
* The `llvm_fresh_expanded_val` command does not support opaque pointers at
  all. See #1879.

This patch also bumps the following submodules to bring in support for opaque
pointers:

* `llvm-pretty`: GaloisInc/llvm-pretty#110
* `llvm-pretty-bc-parser`: GaloisInc/llvm-pretty-bc-parser#221
* `crucible`: GaloisInc/crucible#1085

This also bumps the `what4` submodule to bring in the changes from
GaloisInc/what4#234. This isn't necessary to support opaque pointers, but it
_is_ necessary to support a build plan involving `tasty-sugar-2.2.*`, which
`llvm-pretty-bc-parser`'s test suite now requires.
RyanGlScott added a commit that referenced this issue Jun 1, 2023
yav pushed a commit that referenced this issue Jun 16, 2023
This patch adds support for LLVM 15 and 16 by adding support for opaque
pointers, which are described in https://llvm.org/docs/OpaquePointers.html.  I
have also added a test case involving LLVM bitcode using opaque pointers to
kick the tires and ensure that the basics work as expected.

For the most part, this is a straightforward process, as most uses of pointer
types in SAW already do not care about pointee types. There are some
exceptions, however:

* The `typeOfSetupValue` function, as well as several places that use this
  function, scrutinize pointee types of pointers, which would appear to fly in
  the face of opaque pointers. I attempt to explain in #1876 which this is
  actually OK for now (although a bit awkward).
* The `llvm_boilerplate`/skeleton machinery does not support opaque pointers
  at all. See #1877.
* The `llvm_fresh_expanded_val` command does not support opaque pointers at
  all. See #1879.

This patch also bumps the following submodules to bring in support for opaque
pointers:

* `llvm-pretty`: GaloisInc/llvm-pretty#110
* `llvm-pretty-bc-parser`: GaloisInc/llvm-pretty-bc-parser#221
* `crucible`: GaloisInc/crucible#1085

This also bumps the `what4` submodule to bring in the changes from
GaloisInc/what4#234. This isn't necessary to support opaque pointers, but it
_is_ necessary to support a build plan involving `tasty-sugar-2.2.*`, which
`llvm-pretty-bc-parser`'s test suite now requires.
yav pushed a commit that referenced this issue Jun 16, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
crucible/llvm Related to crucible-llvm verification design-needed enhancement
Projects
None yet
Development

No branches or pull requests

1 participant