Skip to content
This repository has been archived by the owner on May 4, 2024. It is now read-only.

[Prover] boogie_helpers.rs panics for generic axioms #700

Closed
junkil-park opened this issue Nov 28, 2022 · 1 comment · Fixed by #756
Closed

[Prover] boogie_helpers.rs panics for generic axioms #700

junkil-park opened this issue Nov 28, 2022 · 1 comment · Fixed by #756
Assignees

Comments

@junkil-park
Copy link
Collaborator

How to reproduce

Uncomment the axioms here: https://github.com/aptos-labs/aptos-core/pull/5712/files#diff-1ae5dcd6645422049524d26540de53b5f1e45aa68d0a74f727b265a22e4dee3fR13

Run Prover, and it will produce the following error:

RUST_BACKTRACE=1 move prove
[INFO] preparing module 0x1::debug
[INFO] preparing module 0x1::math128
[INFO] preparing module 0x1::math64
[INFO] preparing module 0x1::type_info
[INFO] preparing module 0x1::from_bcs
[INFO] preparing module 0x1::any
[INFO] preparing module 0x1::aptos_hash
[INFO] preparing module 0x1::bls12381
[INFO] preparing module 0x1::capability
[INFO] preparing module 0x1::comparator
[INFO] preparing module 0x1::copyable_any
[INFO] preparing module 0x1::ed25519
[INFO] preparing module 0x1::multi_ed25519
[INFO] preparing module 0x1::simple_map
[INFO] preparing module 0x1::pool_u64
[INFO] preparing module 0x1::ristretto255
[INFO] preparing module 0x1::secp256k1
[INFO] preparing module 0x1::table
[INFO] preparing module 0x1::table_with_length
[INFO] transforming bytecode
thread 'main' panicked at 'unexpected type', language/move-prover/boogie-backend/src/boogie_helpers.rs:194:35
stack backtrace:
   0: rust_begin_unwind
             at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/panicking.rs:584:5
   1: core::panicking::panic_fmt
             at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/core/src/panicking.rs:142:14
   2: move_prover_boogie_backend::boogie_helpers::boogie_type
   3: core::ops::function::impls::<impl core::ops::function::FnOnce<A> for &mut F>::call_once
   4: <core::iter::adapters::flatten::FlatMap<I,U,F> as core::iter::traits::iterator::Iterator>::next
   5: <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter
   6: <alloc::collections::btree::set::BTreeSet<T> as core::iter::traits::collect::FromIterator<T>>::from_iter
   7: move_prover_boogie_backend::add_prelude
   8: move_prover::generate_boogie
   9: move_prover::run_move_prover_with_model
  10: move_cli::base::prove::run_move_prover
  11: move_cli::base::prove::Prove::execute
  12: move_cli::run_cli
  13: move_cli::move_cli
  14: move::main
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

Expected result

Prover produces no error.

@junkil-park
Copy link
Collaborator Author

The panic happens at this line: https://github.com/move-language/move/blob/main/language/move-prover/boogie-backend/src/boogie_helpers.rs#L194

For some reason, Prover concretizes a type parameter T into Primitive(Range). This causes the panic.

junkil-park added a commit to junkil-park/move that referenced this issue Dec 7, 2022
Prover concretizes a type parameter `T` into `Primitive(Range)`  which eventually causes the panic.

So, this commit excludes the spec only primitive types during the mono analysis.

Resolves move-language#700
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.