Fix casting warnings in Projection::new

[avanhatt]

There is a commented-out assertion with a TODO in Projection::new: the assertion fails on some regression tests; but also on some standard library issues that would be useful to have an actual check for. Once we fix the regressions we should enable it.

        // TODO: these assertions fail on a few regressions. Figure out why.
        // I think it may have to do with boxed fat pointers.
        // assert!(
        //     Self::check_expr_typ(&goto_expr, &mir_typ_or_variant, ctx),
        //     "\n{:?}\n{:?}",
        //     &goto_expr,
        //     &mir_typ_or_variant
        // );

[avanhatt]

Example: boxed closures, like this:

   // Create a boxed once-callable closure
    let f: Box<dyn FnOnce()> = Box::new(|| {});
    f();

[celinval]

We need to investigate these. Currently, kani print warnings like the one above for these issues:

WARN kani_compiler::codegen_cprover_gotoc::codegen::place Unexpected type mismatch in projection:
Expr { value: Member { lhs: Expr { value: Symbol { identifier: "_ZN4core3num7flt2dec17digits_to_dec_str17h455a99ccc8826c4bE::1::var_4::parts" }, typ: StructTag("tag-_15158566036879639663"), location: None }, field: "data" }, typ: Pointer { typ: UnionTag("tag-_7532365074337032130") }, location: None }
Expr type
Pointer { typ: UnionTag("tag-_7532365074337032130") }
Type from MIR
FlexibleArray { typ: UnionTag("tag-_7532365074337032130") }

[tautschnig]

Not that I have a solution here as to why "Pointer" and "FlexibleArray" seem to be confused here, but I just wanted to note that CBMC now takes a #flexible_array_member annotation on flexible array members.

[celinval]

From what I gather so far, it looks like we are incorrectly using Struct { Pointer } when adding the symbol to the symbol table. Trying to pin down where this is happening.

[celinval]

Oh, I think I found it. :)

kani/src/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

Line 770 in e6fb988

Type::datatype_component("data", element_type.to_pointer()),

It looks like we are assuming in a lot of places in this file that a slice is encoded as:

struct<T> Slice{
   data: const* T,
   len: usize,
}

But in the following line we expect a FlexibleArray:

kani/src/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

Line 542 in e6fb988

ty::Slice(e) => self.codegen_ty(*e).flexible_array_of(),