Crucible/LLVM: Return type checking is too lax

[langston-barrett]

I'm having buyer's remorse for the strict return type checking for CrucibleSetup blocks. With the strict check introduced there, I get messages like

Incompatible types for return value when verifying engine_table_select
Expected: %struct.engine_st*
but given value of type: void*

(see this minimal example: test.tar.gz). However, with the old check (checkRegisterCompatibility), differences between types like i30 and i32 weren't detected (see #438).

It seems to me like the best solution would be to stop using typeOfSetupValue, and instead develop a predicate

compatibleTypes :: SetupValue -> Crucible.MemType -> Maybe Err

But perhaps there's a better way I'm not aware of? Am I missing something important about the semantics of e.g. MemType vs StorageType?

[robdockins]

It's an unfortunate misnaming, but MemTypes correspond to things that can be stored in an LLVM virtual register, while StorageTypes correspond to things that can be stored in memory. Registers are not byte-oriented, and can contain arbitrary bit-widths, entire structs, etc. Memory is byte-oriented, and can only store things that are multiples of 8-bits... moreover StorageType ignores altogether the distinction between pointers and bitvectors and the distinction between arrays and vectors.

Fundamentally, what I think you're asking here is: "what is the right check for argument/return value compatibility?" I think it's clear that MemType equality is too strict. The old check was StorageType equality, which seems perhaps too lax...

Is what we want "MemType equality except that we consider all pointer types the same?" I'm not sure...

My only hesitation about developing a separate compatibleTypes predicate is that the more similar-but-not-quite-the-same checks we have, the more likely they get out of sync.

[langston-barrett]

@robdockins Thanks for clarifying that (I think you told me once and I forgot 😅)

This is an uncomfortable middle ground. I would think that we want MemType equality modulo special treatment of SetupNull, at least that would work for both the above examples.

[langston-barrett]

Rob and I had a conversation in which he convinced me that "MemType equality except that we consider all pointer types the same"* is probably what we want. We raised zero initialization of structs as an important example to keep in mind.

* "... possibly with a warning if the pointer types aren't on-the-nose the same, but probably no warning if one of them was the null pointer..."

[langston-barrett]

We changed it back to checkRegisterCompatibility in #463 to get ready for 0.3, but as noted above this check is too lax, and causes panics in our simulator if the user has ill-typed SAWscript code.