crucible_field doesn't work with crucible_global

[brianhuffman]

Here's an example:

#include <stdint.h>

typedef struct {
	uint32_t first;
	uint32_t second;
} pair_t;

pair_t the_pair;

void set (uint32_t x, uint32_t y) {
	the_pair.first = x;
	the_pair.second = y;
}

bc <- llvm_load_module "global_struct.bc";

crucible_llvm_verify bc "set" [] false
  do {
    crucible_alloc_global "the_pair";
    x <- crucible_fresh_var "x" (llvm_int 32);
    y <- crucible_fresh_var "y" (llvm_int 32);
    crucible_execute_func [crucible_term x, crucible_term y];
    crucible_points_to (crucible_field (crucible_global "the_pair") "first") (crucible_term x);
    crucible_points_to (crucible_field (crucible_global "the_pair") "second") (crucible_term y);
  }
  z3;

Running this example in saw yields the following error message, even though the .bc file was compiled with debug symbols.

[21:11:06.651] Loading file "/Users/huffman/Documents/saw/global_struct.saw"
[21:11:06.656] Stack trace:
"crucible_llvm_verify" (/Users/huffman/Documents/saw/global_struct.saw:3:1-3:21):
"crucible_points_to" (/Users/huffman/Documents/saw/global_struct.saw:9:5-9:23):
Unable to resolve field name: "first"
No field names were found for this struct

[brianhuffman]

The problem is caused by the unimplemented SetupGlobal case in function resolveSetupValueInfo:

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

Lines 79 to 99 in 100cd24

	-- | Use the LLVM metadata to determine the struct field index
	-- corresponding to the given field name.
	resolveSetupValueInfo ::
	LLVMCrucibleContext wptr {- ^ crucible context -} ->
	Map AllocIndex LLVMAllocSpec {- ^ allocation types -} ->
	Map AllocIndex Crucible.Ident {- ^ allocation type names -} ->
	SetupValue (Crucible.LLVM arch) {- ^ pointer to struct -} ->
	L.Info {- ^ field index -}
	resolveSetupValueInfo cc env nameEnv v =
	case v of
	-- SetupGlobal g ->
	SetupVar i
	| Just alias <- Map.lookup i nameEnv
	, let mdMap = Crucible.llvmMetadataMap (ccTypeCtx cc)
	-> L.Pointer (guessAliasInfo mdMap alias)
	SetupField () a n ->
	fromMaybe L.Unknown $
	do L.Pointer (L.Structure xs) <- return (resolveSetupValueInfo cc env nameEnv a)
	listToMaybe [L.Pointer i | (n',_,i) <- xs, n == n' ]
	_ -> L.Unknown