crucible_fresh_var produces wrong cryptol type for nested struct types

[brianhuffman]

The example is that I'm trying to verify a C function that uses the following struct types:

typedef struct {
    uint32_t fst;
    uint32_t snd;
} pair_t;

typedef struct {
    uint32_t head;
    pair_t tail;
} triple_t;

In LLVM, the type triple_t unfolds to the nested struct type { i32, { i32, i32 } }, which should correspond to the Cryptol nested tuple type ([32], ([32], [32])).

However, when I use crucible_fresh_var "x" (llvm_struct "struct.triple_t"), it gives me a term with cryptol type ([32], [32], [32]). Then crucible_points_to complains that the types are not memory compatible, because { i32, i32, i32 } does not match { i32, { i32, i32 } }.

The confusion might arise because the Cryptol types (a, (b, c)) and (a, b, c) have the same representation in saw-core, and we're probably reconstructing the cryptol type by type inference on the saw-core term. Instead, we should compute the cryptol type directly from the llvm type, so that we don't lose information.

[atomb]

Integration test test0048_alloc_post fails as a result of this. There are a variety of fixes we could consider, but I think that making nested struct types memory compatible with non-nested types may be the right things (as well as making one-element structs memory-compatible with the type of their one element).