Getting wrong type ID `0` for allocs used as fields of single-variant enum

[jberthold]

This surfaced in a test of mir-semantics. Originally posted by @jberthold in runtimeverification/mir-semantics#729 (comment)

For this simple test program

enum-two-refs-fail.rs

#[derive(PartialEq, Debug)]
enum Thing<'a> {
    Thing( &'a i16, &'a u16)
}

#[derive(PartialEq, Debug)]
struct Another<'a>(&'a i32, &'a u32);

fn main() {
    assert_eq!(Thing::Thing(&1, &2), Thing::Thing(&1, &2));
    assert_eq!(Another(&1, &2), Another(&1, &2));
    println!("All assertions passed");
}

the file enum-two-refs-fail.smir.json features ty(0) as the (data) type of four allocations, but also uses 0 as the ID for function lang_start_internal.

From inspecting the data: these allocs 10-13 are referenced from other allocs (1 references 10 and 11, 2 references 12 and 13), and 1 and 2 are of type Thing<'_> , so 10 and 12 should actually just be i16, 11 and 13 should be u16, but they aren't for some reason.

[dkcumming]

I believe problem is that constructing a GlobalAlloc::Memory sets the Ty to ty (0) in every case (inside the else). Perhaps this should also be ty? @jberthold I remember you were running into problems with the ty when you changed the Memory code. Do you think changing this to take ty is the wrong behaviour?

[jberthold]

After investigating the stable-mir-json code and the example:

• The problem comes from the inability of get_prov_ty to determine which variant of an enum to refer to with the field offset into the byte layout.
  

  stable-mir-json/src/printer.rs

  Lines 698 to 710 in b54152a

  	RigidTy::Adt(_adt_def, _args) if ty_kind.is_enum() => {
  	// we have to figure out which variant we are dealing with (requires the data)
  	match field_for_offset(layout, *offset) {
  	None =>
  	// FIXME we'd have to figure out which variant we are dealing with (requires the data)
  	{
  	None
  	}
  	Some(_idx) =>
  	// FIXME we'd have to figure out where that shared field is in the source ordering
  	{
  	None
  	}

  
  None is returned and the caller inserts a ty(0) into the allocation record.
• This is only relevant for allocated data that contains references to other allocated data (provenance map entries in an allocation)
• The problem should at least be logged (at a suitable new warn level?) to inform us about how much of a problem this is in p-token.