Codegen failure: Unsupported intrinisic simd_insert

[adpaco]

The most recent version of RMC shows this panic while codegen'ing the rand crate (#111):

thread 'rustc' panicked at 'not implemented: unsupported intrinsic: simd_insert
        in function std::arch::x86_64::_mm_insert_epi32', compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs:463:18
stack backtrace:
   0: rust_begin_unwind
             at /home/ubuntu/rmc-rebase-3/library/std/src/panicking.rs:515:5
   1: core::panicking::panic_fmt
             at /home/ubuntu/rmc-rebase-3/library/core/src/panicking.rs:92:14
   2: rustc_codegen_llvm::gotoc::intrinsic::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_intrinsic
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs:463:18
   3: <rustc_codegen_llvm::gotoc::hooks::Intrinsic as rustc_codegen_llvm::gotoc::hooks::GotocHook>::handle
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_codegen_llvm/src/gotoc/hooks.rs:274:21
   4: rustc_codegen_llvm::gotoc::statement::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_funcall
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_codegen_llvm/src/gotoc/statement.rs:259:28
   5: rustc_codegen_llvm::gotoc::statement::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_terminator
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_codegen_llvm/src/gotoc/statement.rs:63:17
   6: rustc_codegen_llvm::gotoc::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_block
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_codegen_llvm/src/gotoc/mod.rs:63:28
   7: rustc_codegen_llvm::gotoc::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_function::{{closure}}
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_codegen_llvm/src/gotoc/mod.rs:143:71
   8: core::iter::traits::iterator::Iterator::for_each::call::{{closure}}
             at /home/ubuntu/rmc-rebase-3/library/core/src/iter/traits/iterator.rs:733:29
   9: core::iter::adapters::map::map_fold::{{closure}}
             at /home/ubuntu/rmc-rebase-3/library/core/src/iter/adapters/map.rs:82:21
  10: <core::iter::adapters::enumerate::Enumerate<I> as core::iter::traits::iterator::Iterator>::fold::enumerate::{{closure}}
             at /home/ubuntu/rmc-rebase-3/library/core/src/iter/adapters/enumerate.rs:104:27
  11: core::iter::traits::iterator::Iterator::fold
             at /home/ubuntu/rmc-rebase-3/library/core/src/iter/traits/iterator.rs:2173:21
  12: <core::iter::adapters::enumerate::Enumerate<I> as core::iter::traits::iterator::Iterator>::fold
             at /home/ubuntu/rmc-rebase-3/library/core/src/iter/adapters/enumerate.rs:110:9
  13: <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::fold
             at /home/ubuntu/rmc-rebase-3/library/core/src/iter/adapters/map.rs:122:9
  14: core::iter::traits::iterator::Iterator::for_each
             at /home/ubuntu/rmc-rebase-3/library/core/src/iter/traits/iterator.rs:736:9
  15: rustc_codegen_llvm::gotoc::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_function
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_codegen_llvm/src/gotoc/mod.rs:143:13
  16: <rustc_codegen_llvm::gotoc::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_codegen_llvm/src/gotoc/mod.rs:314:47
  17: rustc_interface::passes::start_codegen::{{closure}}
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_interface/src/passes.rs:1039:9
  18: rustc_data_structures::profiling::VerboseTimingGuard::run
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_data_structures/src/profiling.rs:573:9
  19: rustc_session::utils::<impl rustc_session::session::Session>::time
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_session/src/utils.rs:16:9
  20: rustc_interface::passes::start_codegen
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_interface/src/passes.rs:1038:19
  21: rustc_interface::queries::Queries::ongoing_codegen::{{closure}}::{{closure}}
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_interface/src/queries.rs:254:20
  22: rustc_interface::passes::QueryContext::enter::{{closure}}
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_interface/src/passes.rs:768:42
  23: rustc_middle::ty::context::tls::enter_context::{{closure}}
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_middle/src/ty/context.rs:1744:50
  24: rustc_middle::ty::context::tls::set_tlv
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_middle/src/ty/context.rs:1728:9
  25: rustc_middle::ty::context::tls::enter_context
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_middle/src/ty/context.rs:1744:9
  26: rustc_interface::passes::QueryContext::enter
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_interface/src/passes.rs:768:9
  27: rustc_interface::queries::Queries::ongoing_codegen::{{closure}}
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_interface/src/queries.rs:245:13
  28: rustc_interface::queries::Query<T>::compute
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_interface/src/queries.rs:38:28
  29: rustc_interface::queries::Queries::ongoing_codegen
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_interface/src/queries.rs:243:9
  30: rustc_driver::run_compiler::{{closure}}::{{closure}}
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_driver/src/lib.rs:407:13
  31: rustc_interface::queries::<impl rustc_interface::interface::Compiler>::enter
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_interface/src/queries.rs:394:19
  32: rustc_driver::run_compiler::{{closure}}
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_driver/src/lib.rs:312:22
  33: rustc_interface::interface::create_compiler_and_run::{{closure}}
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_interface/src/interface.rs:208:13
  34: rustc_span::with_source_map
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_span/src/lib.rs:873:5
  35: rustc_interface::interface::create_compiler_and_run
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_interface/src/interface.rs:202:5
  36: rustc_interface::interface::run_compiler::{{closure}}
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_interface/src/interface.rs:224:12
  37: rustc_interface::util::setup_callbacks_and_run_in_thread_pool_with_globals::{{closure}}::{{closure}}
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_interface/src/util.rs:158:13
  38: scoped_tls::ScopedKey<T>::set
             at /home/ubuntu/.cargo/registry/src/github.life-white.uk-1ecc6299db9ec823/scoped-tls-1.0.0/src/lib.rs:137:9
  39: rustc_span::with_session_globals
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_span/src/lib.rs:104:5
  40: rustc_interface::util::setup_callbacks_and_run_in_thread_pool_with_globals::{{closure}}
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_interface/src/util.rs:156:9
  41: rustc_interface::util::scoped_thread::{{closure}}
             at /home/ubuntu/rmc-rebase-3/compiler/rustc_interface/src/util.rs:131:24
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose 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.55.0-dev running on x86_64-unknown-linux-gnu

note: compiler flags: -Z trim-diagnostic-paths=no -Z codegen-backend=gotoc -C embed-bitcode=no -C debuginfo=2 -C incremental --crate-type lib

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

query stack during panic:
end of query stack
error: could not compile `rand_chacha`

[tedinski]

Some notes on my progress:

Targets seem to include:

• simd_insert, simd_extract (this issue)
  • Extract is basically just "array" indexing into the vector.
  • Insert, though, returns a new value with the specified vector index updated, it's not mutation. We'll have to copy the vector then mutate it in our translated "C", or something like that.
• simd_shuffle{2,4,8,16,32,64} (Codegen failure: Unsupported intrinisic simd_shuffle8 #309)
  • Shuffle semantics are two value-vectors input, plus an index-array. Produces a vector with values from the specified indexes into the original vectors, as if they had been concatenated.
  • CBMC's implementation is in shuffle_vector_exprt::lower() under src/ansi-c/c_expr.cpp. It's very straight-forward and we should be able to just do the same thing.

A pretty good reference for what else we could be missing for simd intrinsics is check_platform_intrinsic_type in compiler/rustc_typeck/src/check/intrinsic.rs. There's a fair bit missing still, but fewer if we're not targeting floating point yet.

RMC is translating these to vector types which CBMC seems to handle:

$ rmc --gen-c src/test/cbmc/SIMD/Operators/main.rs
...
$ cat src/test/cbmc/SIMD/Operators/main.c
...
long int __attribute__((vector_size (2*sizeof(long int)))) x;
...

In the symbol table (rmc --keep-temps) we get declarations like this:

Click to see vector variable declaration entry in the symbol table

    "main::1::var_1::x": {
      "baseName": "x",
      "isLvalue": true,
      "isStateVar": true,
      "isThreadLocal": true,
      "location": {...},
      "mode": "C",
      "module": "",
      "name": "main::1::var_1::x",
      "prettyName": "",
      "type": {
        "id": "vector",
        "namedSub": {
          "size": {
            "id": "constant",
            "namedSub": {
              "type": {
                "id": "signedbv",
                "namedSub": {
                  "width": {
                    "id": "64"
                  }
                }
              },
              "value": {
                "id": "2"
              }
            }
          }
        },
        "sub": [
          {
            "id": "signedbv",
            "namedSub": {
              "width": {
                "id": "64"
              }
            }
          }
        ]
      },
      "value": {
        "id": "nil"
      }
    },

and operations like add translate like this (abbreviated):

Click to see symbol table entry adding two vectors

        "sub": [
          {
            "id": "code",
            "namedSub": {
              "statement": {
                "id": "assign"
              }
            },
            "sub": [
              {
                "id": "symbol",
                "namedSub": {
                  "identifier": {
                    "id": "main::1::var_5::res_add"
                  },
                  "type": {the_vector_type}
                }
              },
              {
                "id": "+",
                "namedSub": {
                  "type": {the_vector_type}
                },
                "sub": [
                  {
                    "id": "symbol",
                    "namedSub": {
                      "identifier": {
                        "id": "main::1::var_6"
                      },
                      "type": {the_vector_type}
                    }
                  },

                  {
                    "id": "symbol",
                    "namedSub": {
                      "identifier": {
                        "id": "main::1::var_7"
                      },
                      "type": {the_vector_type}
                    }
                  }
                ]
              }
            ]
          },

So we're just "passing through" the semantics to CBMC for these.

Action plan:

1. Add simd_extract as just array indexing
2. Add simd_insert as copying to a new temporary that we mutate
3. Add simd_shuffle# using the same approach as CBMC: just construct a new vector by indexing into the old ones. (Rust might enforce constants for indexes, but I plan on sticking with CBMC's full generality of handling non-constants)