Add Trees That Grow-style extension fields to SetupValue

[RyanGlScott]

Currently, SetupValue is defined like this:

saw-script/src/SAWScript/Crucible/Common/MethodSpec.hs

Lines 118 to 124 in 64f41ca

	-- | From the manual: \"The SetupValue type corresponds to values that can occur
	-- during symbolic execution, which includes both 'Term' values, pointers, and
	-- composite types consisting of either of these (both structures and arrays).\"
	data SetupValue ext where
	SetupVar :: AllocIndex -> SetupValue ext
	SetupTerm :: TypedTerm -> SetupValue ext
	SetupNull :: B (HasSetupNull ext) -> SetupValue ext

As this comment indicates, the design of SetupValue was inspired by the Trees That Grow paper, which allows defining an AST that can be extended with information specific to particular backends. Specifically, the ext type parameter is instantiated with one of LLVM, JVM, or MIR, and these determine whether fields with types such as B (HasSetupNull ext) are inhabited. If they are inhabited, these fields evaluate to (), indicating that that constructor is valid in that particular backend. If they are not inhabited, then these fields evaluate to Void, indicating that that constructor is never meant to be used in that particular backend.

Unfortunately, SetupValue only commits halfway to the Trees That Grow design. The definition for SetupStruct is:

saw-script/src/SAWScript/Crucible/Common/MethodSpec.hs

Lines 125 to 126 in 64f41ca

	-- | If the 'Bool' is 'True', it's a (LLVM) packed struct
	SetupStruct :: B (HasSetupStruct ext) -> Bool -> [SetupValue ext] -> SetupValue ext

This Bool field is terrible, as the notion of packed structs is only ever used by the LLVM backend. Despite this, other backends will still have to pass False when using SetupStruct, even though this Bool is immaterial in these backends. This goes against the entire philosophy of Trees That Grow, which offers a way to have information that is specific to each backend without requiring other backends to care about it.

I propose that we refactor the Trees That Grow machinery in SetupValue slightly to fix this infelicity. Instead of having type family HasSetupStruct ext :: Bool, type family HasSetupNull ext :: Bool, etc., we should instead have something like type family XSetupStruct ext :: Type. Just as before, we will provide instances of XSetupStruct et al. for LLVM, JVM, and MIR, and if a particular construct isn't used in a backend, we will declare XSetupStruct etc. to evaluate to Void. If a construct is used in a particular backend, however, then XSetupStruct etc. should evaluate to the type used in that specific backend rather than just (). To wit, this means that we would have:

type instance XSetupStruct LLVM = Bool -- True for packed structs, False for other structs
type instance XSetupStruct JVM = Void
...

Now that JVM backend doesn't need to care about packed structs at all.

This refactoring would be especially useful for the in-development MIR backend for SAW (see #1859), as various MIR constructs need additional information not required by other backends:

• MIR allows length-0 arrays, provided that the type of the array is known. SetupArray does not store this type, however.
• MIR structs need to know the type of the struct, since MIR has a nominal type system instead of LLVM's structural type system. Again, SetupStruct does not have a place to store this type.