Support opaque pointers in llvm_fresh_expanded_val

[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

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_fresh_expanded_val command. This can be seen by running the following SAW script (using #1878):

// test.c
void f(int* x) {}

// test.saw
let f_spec = do {
    val <- llvm_fresh_expanded_val (llvm_type "ptr");
    llvm_execute_func [val];
};

m <- llvm_load_module "test.bc";
ov <- llvm_verify m "f" [] false f_spec z3;

$ ~/Software/clang+llvm-16.0.0/bin/clang -g -c -emit-llvm test.c
$ ./bin/saw test.saw



[12:02:45.670] Loading file "/home/ryanglscott/Documents/Hacking/Haskell/saw-script/test.saw"
[12:02:45.673] Stack trace:
"llvm_verify" (/home/ryanglscott/Documents/Hacking/Haskell/saw-script/test.saw:8:7-8:18)
llvm_fresh_expanded_var: PtrOpaque not supported

It's not clear to me what the right behavior should be for fresh opaque pointers. There is already a case for non-opaque pointers:

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

Lines 2211 to 2218 in 79f69bf

	Crucible.PtrType symTy ->
	case Crucible.asMemType symTy of
	Right memTy -> constructFreshPointer (symTypeAlias symTy) loc memTy
	Left err -> throwCrucibleSetup loc $ unlines
	[ "lhs not a valid pointer type: " ++ show symTy
	, "Details:"
	, err
	]

This case will construct a SAW allocation using the same machinery as the llvm_fresh_pointer command. This command relies on knowing what the pointer's pointee type is, however, and we don't have access to pointee types for opaque pointers.

One possibility is to just return a null pointer when making a fresh opaque pointer. This would work, but it would be noticeably different from how non-opaque pointers are treated, which could be confusing.

For now, I am going to make calling llvm_fresh_expanded_val on an opaque pointer an error. We can revisit this if someone expresses a desire for it.