Statement assignment assert failing

[nchong-at-aws]

There are two cases where the assert in gotoc statement assignment is failing [0]

1. When the types are wrapped (e.g. in a Cell) array types when one has an explicit length (e.g., [T;N]) and the other is inferred ([T;_]). E.g.: StructTag("tag-std::cell::RefCell<[bool; 16]>") and StructTag("tag-std::cell::RefCell<[bool; _]>")

2. When the types are closures. E.g., Pointer { typ: StructTag("tag-[closure@file.rs:536:13: 546:14]") } and Pointer { typ: StructTag("tag-[closure@file.rs:503:13: 509:14]") }

The root cause is the naming of these symbol associated with these types.

[0] https://github.com/model-checking/rmc/blob/main-151-2021-04-16/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/stmt.rs#L153

[avanhatt]

Is this resolved by #496 ?

[adpaco-aws]

Just tried to enable the type-checking assertion and it fails the standard library test:

Starting RMC codegen for the Rust standard library...

     Created library `std_lib_test` package
Starting cargo build with RMC
   Compiling compiler_builtins v0.1.55
   Compiling core v0.0.0 (/home/ubuntu/rmc-dash/build/x86_64-unknown-linux-gnu/stage1/lib/rustlib/src/rust/library/core)
   Compiling libc v0.2.108
   Compiling cc v1.0.69
   Compiling memchr v2.4.1
   Compiling std v0.0.0 (/home/ubuntu/rmc-dash/build/x86_64-unknown-linux-gnu/stage1/lib/rustlib/src/rust/library/std)
   Compiling unwind v0.0.0 (/home/ubuntu/rmc-dash/build/x86_64-unknown-linux-gnu/stage1/lib/rustlib/src/rust/library/unwind)
   Compiling rustc-std-workspace-core v1.99.0 (/home/ubuntu/rmc-dash/build/x86_64-unknown-linux-gnu/stage1/lib/rustlib/src/rust/library/rustc-std-workspace-core)
   Compiling alloc v0.0.0 (/home/ubuntu/rmc-dash/build/x86_64-unknown-linux-gnu/stage1/lib/rustlib/src/rust/library/alloc)
   Compiling cfg-if v0.1.10
   Compiling adler v0.2.3
   Compiling rustc-demangle v0.1.21
thread 'rustc' panicked at 'assertion failed: `(left == right)`
  left: `Pointer { typ: StructTag("tag-_5015814172080081019") }`,
 right: `Pointer { typ: StructTag("tag-_12664537782996255021") }`', compiler/cbmc/src/goto_program/stmt.rs:157:9
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

error: internal compiler error: unexpected panic

note: the compiler unexpectedly panicked. this is a bug.

note: we would appreciate a bug report: https://github.com/rust-lang/rust/issues/new?labels=C-bug%2C+I-ICE%2C+T-compiler&template=ice.md

note: rustc 1.59.0-dev running on x86_64-unknown-linux-gnu

note: compiler flags: -Z force-unstable-if-unmarked -Z codegen-backend=gotoc -Z trim-diagnostic-paths=no -Z human_readable_cgu_names -C embed-bitcode=no -C debuginfo=2 -C overflow-checks=on --crate-type lib

note: some of the compiler flags provided by cargo are hidden

query stack during panic:
end of query stack

[RMC] current codegen item: codegen_function: <rustc_std_workspace_core::iter::Peekable<I> as rustc_std_workspace_core::iter::Iterator>::next
_ZN108_$LT$core..iter..adapters..peekable..Peekable$LT$I$GT$$u20$as$u20$core..iter..traits..iterator..Iterator$GT$4next17heda63757b9a33924E
[RMC] current codegen location: Loc { file: "/home/ubuntu/rmc-dash/library/core/src/iter/adapters/peekable.rs", function: None, line: 36, col: Some(5) }

RMC unexpectedly panicked during code generation.

If you are seeing this message, please file an issue here instead of on the Rust compiler: https://github.com/model-checking/rmc/issues/new?labels=bug&template=bug_report.md
error: could not compile `rustc-demangle`
warning: build failed, waiting for other jobs to finish...
thread 'rustc' panicked at 'assertion failed: `(left == right)`
  left: `StructTag("tag-_16610526870762658295")`,
 right: `StructTag("tag-_13428073055387301367")`', compiler/cbmc/src/goto_program/stmt.rs:157:9
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

error: internal compiler error: unexpected panic

note: the compiler unexpectedly panicked. this is a bug.

note: we would appreciate a bug report: https://github.com/rust-lang/rust/issues/new?labels=C-bug%2C+I-ICE%2C+T-compiler&template=ice.md

note: rustc 1.59.0-dev running on x86_64-unknown-linux-gnu

note: compiler flags: -Z force-unstable-if-unmarked -Z codegen-backend=gotoc -Z trim-diagnostic-paths=no -Z human_readable_cgu_names -C embed-bitcode=no -C debuginfo=2 -C overflow-checks=on --crate-type lib

note: some of the compiler flags provided by cargo are hidden

query stack during panic:
end of query stack

[RMC] current codegen item: codegen_function: iter::adapters::flatten::FlatMap::<I, U, F>::new
_ZN4core4iter8adapters7flatten24FlatMap$LT$I$C$U$C$F$GT$3new17h5457415d685bef8eE
[RMC] current codegen location: Loc { file: "/home/ubuntu/rmc-dash/library/core/src/iter/adapters/flatten.rs", function: None, line: 17, col: Some(5) }

RMC unexpectedly panicked during code generation.

If you are seeing this message, please file an issue here instead of on the Rust compiler: https://github.com/model-checking/rmc/issues/new?labels=bug&template=bug_report.md
error: build failed
Command exited with non-zero status 101
        Command being timed: "cargo +nightly build -Z build-std --lib --target x86_64-unknown-linux-gnu"
        User time (seconds): 54.99
        System time (seconds): 6.19
        Percent of CPU this job got: 140%
        Elapsed (wall clock) time (h:mm:ss or m:ss): 0:43.41
        Average shared text size (kbytes): 0
        Average unshared data size (kbytes): 0
        Average stack size (kbytes): 0
        Average total size (kbytes): 0
        Maximum resident set size (kbytes): 933320
        Average resident set size (kbytes): 0
        Major (requiring I/O) page faults: 61
        Minor (reclaiming a frame) page faults: 542492
        Voluntary context switches: 3191
        Involuntary context switches: 198
        Swaps: 0
        File system inputs: 0
        File system outputs: 308352
        Socket messages sent: 0
        Socket messages received: 0
        Signals delivered: 0
        Page size (bytes): 4096
        Exit status: 101

real    0m43.840s
user    0m55.197s
sys     0m6.363s

[danielsn]

Looks like this is related to the projection issue Celina is looking into