Consider using a different type than MemType in typeOfSetupValue

[RyanGlScott]

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:

• The LLVM page on opaque pointers: https://llvm.org/docs/OpaquePointers.html
• The llvm-pretty PR to support opaque pointers: More complete support for opaque pointers (required for LLVM 15+) llvm-pretty#110
• The llvm-pretty-bc-parser PR to support opaque pointers: More complete support for opaque pointers (required for LLVM 15+) llvm-pretty-bc-parser#221
• The crucible PR to support opaque pointers: More complete support for opaque pointers (required for LLVM 15+) crucible#1085

For the most part, updating code to support opaque pointers means auditing every use of non-opaque pointers (e.g., llvm-pretty's PtrTo and crucible-llvm's PtrType) and making sure that the same code would work even if an opaque pointer were used instead. While that is generally possible in a SAW context, there is a place where this is not so straightforward: determining the types of SetupValues. To see what I mean, look at this case in the typeOfSetupValue function:

saw-script/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs

Lines 491 to 499 in 79f69bf

	SetupElem () v i -> do
	do memTy <- typeOfSetupValue cc env nameEnv v
	let msg = "typeOfSetupValue: llvm_elem requires pointer to struct or array, found " ++ show memTy
	case memTy of
	Crucible.PtrType symTy ->
	case let ?lc = lc in Crucible.asMemType symTy of
	Right memTy' ->
	case memTy' of
	Crucible.ArrayType n memTy''

This pattern-matches on a PtrType value and then proceeds by cases on the underlying pointee type. Usually, this is a red flag, as such code would fail to work in an opaque pointer setting. At the same time, it's not so obvious how to write this code if PtrType symTy were replaced with PtrOpaque. What would we use for the symTy in the code that follows?

In fact, there is something more interesting going on. I claim that this use of PtrType is ever-so-slightly different from most other uses of PtrType in that it is specifically referring to the type of a SAW allocation, not just any old pointer type. Unlike LLVM pointers in general, which might lack pointee types, SAW allocations are always declared with an explicit pointee type via the llvm_alloc* and llvm_fresh_pointer family of commands. (I am not proposing that we change llvm_alloc* and llvm_fresh_pointer to get rid of their pointee type arguments, as this is pretty deeply baked into SAW's design.)

As such, it is always fine to scrutinize a SAW allocation's pointee type. typeOfSetupValue isn't the only place where we scrutinize SAW allocations' pointee types, either. See also the following places in the code:

• saw-script/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs

  Lines 563 to 567 in 79f69bf

  	resolveSetupElemOffset cc env nameEnv v i = do
  	do memTy <- typeOfSetupValue cc env nameEnv v
  	let msg = "resolveSetupVal: llvm_elem requires pointer to struct or array, found " ++ show memTy
  	case memTy of
  	Crucible.PtrType symTy ->

• saw-script/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs

  Lines 394 to 395 in 79f69bf

  	do memTy <- typeOfSetupValue cc env nameEnv v
  	case do Crucible.PtrType symTy <- pure memTy

• saw-script/src/SAWScript/Crucible/LLVM/Builtins.hs

  Lines 2686 to 2688 in 79f69bf

  	ptrTy <- exceptToFail $ typeOfSetupValue cc env nameEnv ptr
  	case ptrTy of
  	Crucible.PtrType symTy ->

Note that all of these places are preceded by uses of typeOfSetupValue or a derived function.

This current status quo technically works, but it is a bit uncomfortable, as it relies on the llvm-pretty/crucible-llvm ASTs having special support for non-opaque pointers, a language feature which no longer exists in recent versions of LLVM. While it is unlikely that we will remove PtrTo/PtrType any time soon (if ever), it is worth thinking about how the code above could be made to work in a world where the ASTs only supported non-opaque pointers.

One way to do so would be to change the return type of typeOfSetupValue to use a slightly richer type than MemType. We could have it instead return SetupMemType, which might look roughly like:

data SetupMemType
  = AllocationType MemType -- For SAW allocations
  | LLVMValueType MemType  -- For all other values

This would allow us to express the fact that SAW allocations have explicit pointee types while keeping it separate from MemType. Of course, we'd have to refactor quite a bit of code to adapt to this change of data type, including conversions from SetupMemType to MemType and vice versa. For now, I am not going to perform this refactoring, as the current status quo works well enough, and it is unclear how much work the refactoring would take.

[eddywestbrook]

Interesting. Thanks for the very detailed and clear explanation!