From a5b9487b863053f2c422b5898b5602bd383bf7f9 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 17 Dec 2021 22:11:32 +0000 Subject: [PATCH 1/9] Initial version of support table --- rmc-docs/src/SUMMARY.md | 2 + rmc-docs/src/limitations.md | 120 ++++++++++++++++++++++++++++++++++++ 2 files changed, 122 insertions(+) create mode 100644 rmc-docs/src/limitations.md diff --git a/rmc-docs/src/SUMMARY.md b/rmc-docs/src/SUMMARY.md index d168cb4b0468..7c16b30125fe 100644 --- a/rmc-docs/src/SUMMARY.md +++ b/rmc-docs/src/SUMMARY.md @@ -18,3 +18,5 @@ - [RMC developer documentation](./dev-documentation.md) - [Testing](./rmc-testing.md) - [Book runner](./bookrunner.md) + +- [Limitations](./limitations.md) diff --git a/rmc-docs/src/limitations.md b/rmc-docs/src/limitations.md new file mode 100644 index 000000000000..1e1397f05c8a --- /dev/null +++ b/rmc-docs/src/limitations.md @@ -0,0 +1,120 @@ +# Limitations + +## Rust feature support + +*Define Yes, No and Partial* + +Reference | Feature | Support | Observations | +--- | --- | --- | --- | +3.1 | Macros By Example | Yes | | +3.2 | Procedural Macros | Yes | | +4 | Crates and source files | Yes | | +5 | Conditional compilation | Yes | | +6.1 | Modules | Yes | | +6.2 | Extern crates | Yes | | +6.3 | Use declarations | Yes | | +6.4 | Functions | Yes | | +6.5 | Type aliases | Yes | | +6.6 | Structs | Yes | | +6.7 | Enumerations | Yes | | +6.8 | Unions | Yes | | +6.9 | Constant items | Yes | | +6.10 | Static items | Yes | | +6.11 | Traits | Yes | | +6.12 | Implementations | Yes | | +6.13 | External blocks | Yes | | +6.14 | Generic parameters | Yes | | +6.15 | Associated Items | Yes | | +7 | Attributes | Yes | | +8.1 | Statements | Yes | | +8.2.1 | Literal expressions | Yes | | +8.2.2 | Path expressions | Yes | | +8.2.3 | Block expressions | Yes | | +8.2.4 | Operator expressions | Yes | | +8.2.5 | Grouped expressions | Yes | | +8.2.6 | Array and index expressions | Yes | | +8.2.7 | Tuple and index expressions | Yes | | +8.2.8 | Struct expressions | Yes | | +8.2.9 | Call expressions | Yes | | +8.2.10 | Method call expressions | Yes | | +8.2.11 | Field access expressions | Yes | | +8.2.12 | Closure expressions | Yes | | +8.2.13 | Loop expressions | Yes | | +8.2.14 | Range expressions | Yes | | +8.2.15 | If and if let expressions | Yes | | +8.2.16 | Match expressions | Yes | | +8.2.17 | Return expressions | Yes | | +8.2.18 | Await expressions | No | [Concurrency](#concurrency) | +9 | Patterns | Partial | [Patterns](#patterns) | +10.1.1 | Boolean type | Yes | | +10.1.2 | Numeric types | Yes | | +10.1.3 | Textual types | Yes | | +10.1.4 | Never type | Yes | | +10.1.5 | Tuple types | Yes | | +10.1.6 | Array types | Yes | | +10.1.7 | Slice types | Yes | | +10.1.8 | Struct types | Yes | | +10.1.9 | Enumerated types | Yes | | +10.1.10 | Union types | Yes | | +10.1.11 | Function item types | Yes | | +10.1.12 | Closure types | Partial | | +10.1.13 | Pointer types | Partial | | +10.1.14 | Function pointer types | Partial | | +10.1.15 | Trait object types | Partial | | +10.1.16 | Impl trait type | Partial | | +10.1.17 | Type parameters | Partial | | +10.1.18 | Inferred type | Partial | | +10.2 | Dynamically Sized Types | Partial | | +10.3 | Type layout | Yes | | +10.4 | Interior mutability | Yes | | +10.5 | Subtyping and Variance | Yes | | +10.6 | Trait and lifetime bounds | Yes | | +10.7 | Type coercions | Partial | | +10.8 | Destructors | Partial | | +10.9 | Lifetime elision | Yes | | +11 | Special types and traits | Partial | | +| | `Box` | Yes | | +| | `Rc` | Yes | | +| | `Arc` | Yes | | +| | `Pin` | Yes | | +| | `UnsafeCell` | Partial | | +| | `PhantomData` | Partial | *Review this* | +| | Operator Traits | Partial | | +| | `Deref` and `DerefMut` | Yes | | +| | `Drop` | Partial | | +| | `Copy` | Yes | | +| | `Clone` | Yes | | +14 | Linkage | Yes | | +15.1 | Unsafe functions | Yes | | +15.2 | Unsafe blocks | Yes | | +15.3 | Behavior considered undefined | Partial | | +| | Data races | No | [Concurrency](#concurrency) | +| | Dereferencing dangling raw pointers | Yes | | +| | Dereferencing unaligned raw pointers | No | | +| | Breaking pointer aliasing rules | No | | +| | Mutating immutable data | No | | +| | Invoking undefined behavior via compiler intrinsics | Partial | [Intrinsics](#intrinsics) | +| | Executing code compiled with platform features that the current platform does not support | No | | +| | Producing an invalid value, even in private fields and locals | No | | + +## Observations on partially or unsupported features + +### Assembly + +To be written. + +### Concurrency + +Concurrent features are out of scope for RMC. In general, the verification of +concurrent programs continues to be an open research problem. In particular, +support for concurrent verification in CBMC is limited and RMC emits warnings +whenever it finds concurrent constructs in programs. + +### Patterns + +The code for handling patterns has not been tested in a thorough manner. We +expect to fully support this feature in the near future. + +### Intrinsics + +TBD \ No newline at end of file From 009f2e188a8c658040da660f4cb88b725d274228 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 20 Dec 2021 18:35:23 +0000 Subject: [PATCH 2/9] Define support values for table --- rmc-docs/src/limitations.md | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/rmc-docs/src/limitations.md b/rmc-docs/src/limitations.md index 1e1397f05c8a..ef4d5f0ca3c0 100644 --- a/rmc-docs/src/limitations.md +++ b/rmc-docs/src/limitations.md @@ -2,6 +2,14 @@ ## Rust feature support +The table below tries to summarize the current support in RMC for +the Rust language features according to the [Rust Reference](https://doc.rust-lang.org/stable/reference/). +We use three values to indicate the level of support: + * *Yes*: The feature is fully supported. There may + * *Partial*: The feature is at least partially supported. This means we are aware of some issue + with the feature. + * *No*: + *Define Yes, No and Partial* Reference | Feature | Support | Observations | @@ -90,7 +98,7 @@ Reference | Feature | Support | Observations | 15.3 | Behavior considered undefined | Partial | | | | Data races | No | [Concurrency](#concurrency) | | | Dereferencing dangling raw pointers | Yes | | -| | Dereferencing unaligned raw pointers | No | | +| | Dereferencing unaligned raw pointers | No | | | | Breaking pointer aliasing rules | No | | | | Mutating immutable data | No | | | | Invoking undefined behavior via compiler intrinsics | Partial | [Intrinsics](#intrinsics) | From 65f3cff26cf79520a9b21550154ba3417bdf43e2 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 21 Dec 2021 22:00:05 +0000 Subject: [PATCH 3/9] Add intrinsics table and other content --- rmc-docs/src/limitations.md | 312 +++++++++++++++++++++++++++++++++--- 1 file changed, 286 insertions(+), 26 deletions(-) diff --git a/rmc-docs/src/limitations.md b/rmc-docs/src/limitations.md index ef4d5f0ca3c0..c2d198145212 100644 --- a/rmc-docs/src/limitations.md +++ b/rmc-docs/src/limitations.md @@ -4,13 +4,14 @@ The table below tries to summarize the current support in RMC for the Rust language features according to the [Rust Reference](https://doc.rust-lang.org/stable/reference/). -We use three values to indicate the level of support: - * *Yes*: The feature is fully supported. There may - * *Partial*: The feature is at least partially supported. This means we are aware of some issue - with the feature. - * *No*: +We use the following values to indicate the level of support: + * **Yes**: The feature is fully supported. We are not aware of any issue with it. + * **Partial**: The feature is at least partially supported. We are aware of some issue with + with it. + * **No**: The feature is not supported. Some support may be available but analyses should not be trusted. -*Define Yes, No and Partial* +As with all software, bugs may be found anywhere regardless of the level of support. In such cases, we +would greatly appreciate that you [filed a bug report](https://github.com/model-checking/rmc/issues/new?assignees=&labels=bug&template=bug_report.md). Reference | Feature | Support | Observations | --- | --- | --- | --- | @@ -52,8 +53,8 @@ Reference | Feature | Support | Observations | 8.2.15 | If and if let expressions | Yes | | 8.2.16 | Match expressions | Yes | | 8.2.17 | Return expressions | Yes | | -8.2.18 | Await expressions | No | [Concurrency](#concurrency) | -9 | Patterns | Partial | [Patterns](#patterns) | +8.2.18 | Await expressions | No | See [Observations - Concurrency](#concurrency) | +9 | Patterns | Partial | Needs more testing | 10.1.1 | Boolean type | Yes | | 10.1.2 | Numeric types | Yes | | 10.1.3 | Textual types | Yes | | @@ -65,19 +66,19 @@ Reference | Feature | Support | Observations | 10.1.9 | Enumerated types | Yes | | 10.1.10 | Union types | Yes | | 10.1.11 | Function item types | Yes | | -10.1.12 | Closure types | Partial | | -10.1.13 | Pointer types | Partial | | -10.1.14 | Function pointer types | Partial | | -10.1.15 | Trait object types | Partial | | -10.1.16 | Impl trait type | Partial | | -10.1.17 | Type parameters | Partial | | -10.1.18 | Inferred type | Partial | | -10.2 | Dynamically Sized Types | Partial | | +10.1.12 | Closure types | Partial | See [Observations - Advanced features](#advanced-features) | +10.1.13 | Pointer types | Partial | See [Observations - Advanced features](#advanced-features) | +10.1.14 | Function pointer types | Partial | See [Observations - Advanced features](#advanced-features) | +10.1.15 | Trait object types | Partial | See [Observations - Advanced features](#advanced-features) | +10.1.16 | Impl trait type | Partial | See [Observations - Advanced features](#advanced-features) | +10.1.17 | Type parameters | Partial | See [Observations - Advanced features](#advanced-features) | +10.1.18 | Inferred type | Partial | See [Observations - Advanced features](#advanced-features) | +10.2 | Dynamically Sized Types | Partial | See [Observations - Advanced features](#advanced-features) | 10.3 | Type layout | Yes | | 10.4 | Interior mutability | Yes | | 10.5 | Subtyping and Variance | Yes | | 10.6 | Trait and lifetime bounds | Yes | | -10.7 | Type coercions | Partial | | +10.7 | Type coercions | Partial | See [Observations - Advanced features](#advanced-features) | 10.8 | Destructors | Partial | | 10.9 | Lifetime elision | Yes | | 11 | Special types and traits | Partial | | @@ -96,33 +97,292 @@ Reference | Feature | Support | Observations | 15.1 | Unsafe functions | Yes | | 15.2 | Unsafe blocks | Yes | | 15.3 | Behavior considered undefined | Partial | | -| | Data races | No | [Concurrency](#concurrency) | +| | Data races | No | See [Observations - Concurrency](#concurrency) | | | Dereferencing dangling raw pointers | Yes | | | | Dereferencing unaligned raw pointers | No | | | | Breaking pointer aliasing rules | No | | | | Mutating immutable data | No | | -| | Invoking undefined behavior via compiler intrinsics | Partial | [Intrinsics](#intrinsics) | +| | Invoking undefined behavior via compiler intrinsics | Partial | See [Observations - Intrinsics](#intrinsics) | | | Executing code compiled with platform features that the current platform does not support | No | | | | Producing an invalid value, even in private fields and locals | No | | ## Observations on partially or unsupported features +### Code generation for unsupported features + +RMC aims to be a industrial verification tool. Most industrial crates may +include unsupported features in parts of their code that do not need to be +verified. In general, this should not prevent users from verifying their code. + +Because of that, the general rule is that RMC generates an `assert(false)` +statement when compiling any unsupported feature. This will cause proofs to fail +if the statement is reachable during the verification stage. However, the +analysis will not affected if the statement is not reachable from the code under +verification, so users can still verify components of their code not using +unsupported features. + ### Assembly -To be written. +CBMC support for assembly code is quite limited. It may be extended in the +future but at present there are no plans to do so. + +Check out the tracking issues for [inline assembly (`asm!` +macro)](https://github.com/model-checking/rmc/issues/2) and [global assembly +(`asm_global!` macro)](https://github.com/model-checking/rmc/issues/316) to know +more about the current status. ### Concurrency Concurrent features are out of scope for RMC. In general, the verification of concurrent programs continues to be an open research problem. In particular, -support for concurrent verification in CBMC is limited and RMC emits warnings -whenever it finds concurrent constructs in programs. +support for concurrent verification in CBMC is limited and RMC emits a warning +whenever it encounters concurrent code. + +### Advanced features + +Advanced features (traits, types, etc.) from Rust have proven to particularly +difficult to model. Even though the code handling these features has been +reviewed in multiple occasions, we often find new corner cases that are not +covered by RMC. We are especially interested in bug reports concerning these +features, so please [file a bug +report](https://github.com/model-checking/rmc/issues/new?assignees=&labels=bug&template=bug_report.md) +if you are aware of one. -### Patterns +### Destructors -The code for handling patterns has not been tested in a thorough manner. We -expect to fully support this feature in the near future. +At present, we are aware of some issues with destructors, in particular those +related to [advanced features](#advanced-features). ### Intrinsics -TBD \ No newline at end of file +The table below tries to summarize the current support in RMC for Rust +intrinsics. + +In general, code generation for unsupported intrinsics follows the rule +described in [Code generation for unsupported +features](#code-generation-for-unsupported-features). + +Name | Support | Observations | +--- | --- | --- | +abort | Yes | | +add_with_overflow | Yes | | +arith_offset | Yes | | +assert_inhabited | Yes | | +assert_uninit_valid | Partial | Generates `SKIP` statement | +assert_zero_valid | Partial | Generates `SKIP` statement | +assume | Yes | | +atomic_and | Partial | See [Atomics](#atomics) | +atomic_and_acq | Partial | See [Atomics](#atomics) | +atomic_and_acqrel | Partial | See [Atomics](#atomics) | +atomic_and_rel | Partial | See [Atomics](#atomics) | +atomic_and_relaxed | Partial | See [Atomics](#atomics) | +atomic_cxchg | Partial | See [Atomics](#atomics) | +atomic_cxchg_acq | Partial | See [Atomics](#atomics) | +atomic_cxchg_acq_failrelaxed | Partial | See [Atomics](#atomics) | +atomic_cxchg_acqrel | Partial | See [Atomics](#atomics) | +atomic_cxchg_acqrel_failrelaxed | Partial | See [Atomics](#atomics) | +atomic_cxchg_failacq | Partial | See [Atomics](#atomics) | +atomic_cxchg_failrelaxed | Partial | See [Atomics](#atomics) | +atomic_cxchg_rel | Partial | See [Atomics](#atomics) | +atomic_cxchg_relaxed | Partial | See [Atomics](#atomics) | +atomic_cxchgweak | Partial | See [Atomics](#atomics) | +atomic_cxchgweak_acq | Partial | See [Atomics](#atomics) | +atomic_cxchgweak_acq_failrelaxed | Partial | See [Atomics](#atomics) | +atomic_cxchgweak_acqrel | Partial | See [Atomics](#atomics) | +atomic_cxchgweak_acqrel_failrelaxed | Partial | See [Atomics](#atomics) | +atomic_cxchgweak_failacq | Partial | See [Atomics](#atomics) | +atomic_cxchgweak_failrelaxed | Partial | See [Atomics](#atomics) | +atomic_cxchgweak_rel | Partial | See [Atomics](#atomics) | +atomic_cxchgweak_relaxed | Partial | See [Atomics](#atomics) | +atomic_fence | Partial | See [Atomics](#atomics) | +atomic_fence_acq | Partial | See [Atomics](#atomics) | +atomic_fence_acqrel | Partial | See [Atomics](#atomics) | +atomic_fence_rel | Partial | See [Atomics](#atomics) | +atomic_load | Partial | See [Atomics](#atomics) | +atomic_load_acq | Partial | See [Atomics](#atomics) | +atomic_load_relaxed | Partial | See [Atomics](#atomics) | +atomic_load_unordered | Partial | See [Atomics](#atomics) | +atomic_max | Partial | See [Atomics](#atomics) | +atomic_max_acq | Partial | See [Atomics](#atomics) | +atomic_max_acqrel | Partial | See [Atomics](#atomics) | +atomic_max_rel | Partial | See [Atomics](#atomics) | +atomic_max_relaxed | Partial | See [Atomics](#atomics) | +atomic_min | Partial | See [Atomics](#atomics) | +atomic_min_acq | Partial | See [Atomics](#atomics) | +atomic_min_acqrel | Partial | See [Atomics](#atomics) | +atomic_min_rel | Partial | See [Atomics](#atomics) | +atomic_min_relaxed | Partial | See [Atomics](#atomics) | +atomic_nand | Partial | See [Atomics](#atomics) | +atomic_nand_acq | Partial | See [Atomics](#atomics) | +atomic_nand_acqrel | Partial | See [Atomics](#atomics) | +atomic_nand_rel | Partial | See [Atomics](#atomics) | +atomic_nand_relaxed | Partial | See [Atomics](#atomics) | +atomic_or | Partial | See [Atomics](#atomics) | +atomic_or_acq | Partial | See [Atomics](#atomics) | +atomic_or_acqrel | Partial | See [Atomics](#atomics) | +atomic_or_rel | Partial | See [Atomics](#atomics) | +atomic_or_relaxed | Partial | See [Atomics](#atomics) | +atomic_singlethreadfence | Partial | See [Atomics](#atomics) | +atomic_singlethreadfence_acq | Partial | See [Atomics](#atomics) | +atomic_singlethreadfence_acqrel | Partial | See [Atomics](#atomics) | +atomic_singlethreadfence_rel | Partial | See [Atomics](#atomics) | +atomic_store | Partial | See [Atomics](#atomics) | +atomic_store_rel | Partial | See [Atomics](#atomics) | +atomic_store_relaxed | Partial | See [Atomics](#atomics) | +atomic_store_unordered | Partial | See [Atomics](#atomics) | +atomic_umax | Partial | See [Atomics](#atomics) | +atomic_umax_acq | Partial | See [Atomics](#atomics) | +atomic_umax_acqrel | Partial | See [Atomics](#atomics) | +atomic_umax_rel | Partial | See [Atomics](#atomics) | +atomic_umax_relaxed | Partial | See [Atomics](#atomics) | +atomic_umin | Partial | See [Atomics](#atomics) | +atomic_umin_acq | Partial | See [Atomics](#atomics) | +atomic_umin_acqrel | Partial | See [Atomics](#atomics) | +atomic_umin_rel | Partial | See [Atomics](#atomics) | +atomic_umin_relaxed | Partial | See [Atomics](#atomics) | +atomic_xadd | Partial | See [Atomics](#atomics) | +atomic_xadd_acq | Partial | See [Atomics](#atomics) | +atomic_xadd_acqrel | Partial | See [Atomics](#atomics) | +atomic_xadd_rel | Partial | See [Atomics](#atomics) | +atomic_xadd_relaxed | Partial | See [Atomics](#atomics) | +atomic_xchg | Partial | See [Atomics](#atomics) | +atomic_xchg_acq | Partial | See [Atomics](#atomics) | +atomic_xchg_acqrel | Partial | See [Atomics](#atomics) | +atomic_xchg_rel | Partial | See [Atomics](#atomics) | +atomic_xchg_relaxed | Partial | See [Atomics](#atomics) | +atomic_xor | Partial | See [Atomics](#atomics) | +atomic_xor_acq | Partial | See [Atomics](#atomics) | +atomic_xor_acqrel | Partial | See [Atomics](#atomics) | +atomic_xor_rel | Partial | See [Atomics](#atomics) | +atomic_xor_relaxed | Partial | See [Atomics](#atomics) | +atomic_xsub | Partial | See [Atomics](#atomics) | +atomic_xsub_acq | Partial | See [Atomics](#atomics) | +atomic_xsub_acqrel | Partial | See [Atomics](#atomics) | +atomic_xsub_rel | Partial | See [Atomics](#atomics) | +atomic_xsub_relaxed | Partial | See [Atomics](#atomics) | +bitreverse | No | | +breakpoint | Yes | | +bswap | Yes | | +caller_location | No | | +ceilf32 | Yes | | +ceilf64 | Yes | | +copy_nonoverlapping | Yes | | +copysignf32 | Yes | | +copysignf64 | Yes | | +cosf32 | Yes | | +cosf64 | Yes | | +ctlz | Yes | | +ctlz_nonzero | Yes | | +ctpop | Yes | | +cttz | Yes | | +cttz_nonzero | Yes | | +discriminant_value | Yes | | +drop_in_place | No | | +exact_div | Yes | | +exp2f32 | Yes | | +exp2f64 | Yes | | +expf32 | Yes | | +expf64 | Yes | | +fabsf32 | Yes | | +fabsf64 | Yes | | +fadd_fast | No | | +fdiv_fast | No | | +float_to_int_unchecked | No | | +floorf32 | Yes | | +floorf64 | Yes | | +fmaf32 | Yes | | +fmaf64 | Yes | | +fmul_fast | No | | +forget | Partial | Generates `SKIP` statement | +frem_fast | No | | +fsub_fast | No | | +likely | Yes | | +log2f32 | Yes | | +log2f64 | Yes | | +log10f32 | Yes | | +log10f64 | Yes | | +logf32 | Yes | | +logf64 | Yes | | +maxnumf32 | Yes | | +maxnumf64 | Yes | | +min_align_of | Yes | | +min_align_of_val | Yes | | +minnumf32 | Yes | | +minnumf64 | Yes | | +move_val_init | No | | +mul_with_overflow | Yes | | +nearbyintf32 | Yes | | +nearbyintf64 | Yes | | +needs_drop | Yes | | +nontemporal_store | No | | +offset | Partial | Missing undefined behavior checks | +powf32 | Yes | | +powf64 | Yes | | +powif32 | Yes | | +powif64 | Yes | | +pref_align_of | Yes | | +prefetch_read_data | No | | +prefetch_read_instruction | No | | +prefetch_write_data | No | | +prefetch_write_instruction | No | | +ptr_guaranteed_eq | Partial | | +ptr_guaranteed_ne | Partial | | +ptr_offset_from | Partial | Missing undefined behavior checks | +raw_eq | Partial | Missing undefined behavior checks | +rintf32 | Yes | | +rintf64 | Yes | | +rotate_left | Yes | | +rotate_right | Yes | | +roundf32 | Yes | | +roundf64 | Yes | | +rustc_peek | No | | +saturating_add | Yes | | +saturating_sub | Yes | | +sinf32 | Yes | | +sinf64 | Yes | | +size_of | Yes | | +size_of_val | Yes | | +sqrtf32 | Yes | | +sqrtf64 | Yes | | +sub_with_overflow | Yes | | +transmute | Yes | | +truncf32 | Yes | | +truncf64 | Yes | | +try | No | | +type_id | Yes | | +type_name | Yes | | +unaligned_volatile_load | Partial | See [Observations - Concurrency](#concurrency) | +unaligned_volatile_store | No | See [Observations - Concurrency](#concurrency) | +unchecked_add | Yes | | +unchecked_div | Yes | | +unchecked_mul | Yes | | +unchecked_rem | Yes | | +unchecked_shl | Yes | | +unchecked_shr | Yes | | +unchecked_sub | Yes | | +unlikely | Yes | | +unreachable | Yes | | +variant_count | No | | +volatile_copy_memory | Partial | See [Observations - Concurrency](#concurrency) | +volatile_copy_nonoverlapping_memory | Partial | See [Observations - Concurrency](#concurrency) | +volatile_load | Partial | See [Observations - Concurrency](#concurrency) | +volatile_set_memory | No | See [Observations - Concurrency](#concurrency) | +volatile_store | No | See [Observations - Concurrency](#concurrency) | +wrapping_add | Yes | | +wrapping_mul | Yes | | +wrapping_sub | Yes | | +write_bytes | Yes | | + +#### Atomics + +All atomic intrinsics are compiled as an atomic block where the operation is +performed. But as noted in [Observations - Concurrency](#concurrency), CBMC +support for concurrent verification is limited and not used by default. +Verification on code containing atomic intrinsics should not be trusted given +that CBMC assumes the code to be sequential. + +#### SIMD instructions + +While RMC is capable of generating code for SIMD instructions. Unfortunately, +CBMC does not provide support for some operations like vector comparison (e.g., +`simd_eq`) or shuffling (e.g., `simd_shuffle8`). From 932b09378d8649ef798c688c174b548cc5b26b49 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 23 Dec 2021 17:11:36 +0000 Subject: [PATCH 4/9] Observations on stdlib --- rmc-docs/src/limitations.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/rmc-docs/src/limitations.md b/rmc-docs/src/limitations.md index c2d198145212..787f20df005b 100644 --- a/rmc-docs/src/limitations.md +++ b/rmc-docs/src/limitations.md @@ -138,6 +138,19 @@ concurrent programs continues to be an open research problem. In particular, support for concurrent verification in CBMC is limited and RMC emits a warning whenever it encounters concurrent code. +### Not inlined standard library functions + +At present, RMC is able to link in functions from the standard library but the +generated code will not contain them unless they are inlined. This results in +verification failures if the code under verification, for example, includes a +`println!` statement. + +We have done some experiments to embed the standard library into the generated +code, but this causes verification times to increase significantly. As of now, +we have not been able to find a simple solution for [this +issue](https://github.com/model-checking/rmc/issues/581), but we have some ideas +for future work in this direction. + ### Advanced features Advanced features (traits, types, etc.) from Rust have proven to particularly From cbe1e527b53f2df5c8661c416fa421538fedd223 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 30 Dec 2021 21:36:48 +0000 Subject: [PATCH 5/9] Address Celina's comments --- rmc-docs/src/limitations.md | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/rmc-docs/src/limitations.md b/rmc-docs/src/limitations.md index 787f20df005b..9282dd7fc537 100644 --- a/rmc-docs/src/limitations.md +++ b/rmc-docs/src/limitations.md @@ -123,8 +123,8 @@ unsupported features. ### Assembly -CBMC support for assembly code is quite limited. It may be extended in the -future but at present there are no plans to do so. +RMC does not support assembly code for now. We may add it in the future but at +present there are no plans to do so. Check out the tracking issues for [inline assembly (`asm!` macro)](https://github.com/model-checking/rmc/issues/2) and [global assembly @@ -134,11 +134,12 @@ more about the current status. ### Concurrency Concurrent features are out of scope for RMC. In general, the verification of -concurrent programs continues to be an open research problem. In particular, -support for concurrent verification in CBMC is limited and RMC emits a warning -whenever it encounters concurrent code. +concurrent programs continues to be an open research problem where most tools +that analyze concurrent code lack support for other features. Because of this, +RMC emits a warning whenever it encounters concurrent code and compiles as if it +was sequential code. -### Not inlined standard library functions +### Standard library functions At present, RMC is able to link in functions from the standard library but the generated code will not contain them unless they are inlined. This results in From efe48b092bbd5476f6110d2d639a741aff96983c Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 30 Dec 2021 21:41:14 +0000 Subject: [PATCH 6/9] More comments --- rmc-docs/src/limitations.md | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/rmc-docs/src/limitations.md b/rmc-docs/src/limitations.md index 9282dd7fc537..1f7b271bcf1f 100644 --- a/rmc-docs/src/limitations.md +++ b/rmc-docs/src/limitations.md @@ -142,9 +142,8 @@ was sequential code. ### Standard library functions At present, RMC is able to link in functions from the standard library but the -generated code will not contain them unless they are inlined. This results in -verification failures if the code under verification, for example, includes a -`println!` statement. +generated code will not contain them. This results in verification failures if +the code under verification, for example, includes a `println!` statement. We have done some experiments to embed the standard library into the generated code, but this causes verification times to increase significantly. As of now, @@ -154,11 +153,10 @@ for future work in this direction. ### Advanced features -Advanced features (traits, types, etc.) from Rust have proven to particularly -difficult to model. Even though the code handling these features has been -reviewed in multiple occasions, we often find new corner cases that are not -covered by RMC. We are especially interested in bug reports concerning these -features, so please [file a bug +The semantics around some advanced features (traits, types, etc.) from Rust are +not formally defined which makes it harder to ensure that we can properly model +all their use cases. We are particularly interested in bug reports concerning +these features, so please [file a bug report](https://github.com/model-checking/rmc/issues/new?assignees=&labels=bug&template=bug_report.md) if you are aware of one. From 88e1880e37fe7295233313762e28e51bbd378ac2 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 3 Jan 2022 15:28:24 +0000 Subject: [PATCH 7/9] Add section on panic strategies --- rmc-docs/src/limitations.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/rmc-docs/src/limitations.md b/rmc-docs/src/limitations.md index 1f7b271bcf1f..854931861c28 100644 --- a/rmc-docs/src/limitations.md +++ b/rmc-docs/src/limitations.md @@ -160,6 +160,19 @@ these features, so please [file a bug report](https://github.com/model-checking/rmc/issues/new?assignees=&labels=bug&template=bug_report.md) if you are aware of one. +### Panic strategies + +Rust has two different strategies when a panic occurs: + 1. Stack unwinding (default): Walks back the stack cleaning up the data from + each function it encounters. + 2. Abortion: Immediately ends the program without cleaning up. + +Currently, RMC does not support stack unwinding. This has some implications +regarding memory safety since programs sometimes rely on the unwinding logic to +ensure there is no resource leak or persistent data inconsistency. Check out +[this issue](https://github.com/model-checking/rmc/issues/692) for updates on +stack unwinding support. + ### Destructors At present, we are aware of some issues with destructors, in particular those From 58a831c10df4daa50fbf19685dd4c0c769f400a1 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 4 Jan 2022 17:24:10 +0000 Subject: [PATCH 8/9] Address more comments --- rmc-docs/src/limitations.md | 101 +++++++++++++++++++++--------------- 1 file changed, 60 insertions(+), 41 deletions(-) diff --git a/rmc-docs/src/limitations.md b/rmc-docs/src/limitations.md index 854931861c28..076a8c42b052 100644 --- a/rmc-docs/src/limitations.md +++ b/rmc-docs/src/limitations.md @@ -13,7 +13,7 @@ We use the following values to indicate the level of support: As with all software, bugs may be found anywhere regardless of the level of support. In such cases, we would greatly appreciate that you [filed a bug report](https://github.com/model-checking/rmc/issues/new?assignees=&labels=bug&template=bug_report.md). -Reference | Feature | Support | Observations | +Reference | Feature | Support | Notes | --- | --- | --- | --- | 3.1 | Macros By Example | Yes | | 3.2 | Procedural Macros | Yes | | @@ -53,7 +53,7 @@ Reference | Feature | Support | Observations | 8.2.15 | If and if let expressions | Yes | | 8.2.16 | Match expressions | Yes | | 8.2.17 | Return expressions | Yes | | -8.2.18 | Await expressions | No | See [Observations - Concurrency](#concurrency) | +8.2.18 | Await expressions | No | See [Notes - Concurrency](#concurrency) | 9 | Patterns | Partial | Needs more testing | 10.1.1 | Boolean type | Yes | | 10.1.2 | Numeric types | Yes | | @@ -66,19 +66,19 @@ Reference | Feature | Support | Observations | 10.1.9 | Enumerated types | Yes | | 10.1.10 | Union types | Yes | | 10.1.11 | Function item types | Yes | | -10.1.12 | Closure types | Partial | See [Observations - Advanced features](#advanced-features) | -10.1.13 | Pointer types | Partial | See [Observations - Advanced features](#advanced-features) | -10.1.14 | Function pointer types | Partial | See [Observations - Advanced features](#advanced-features) | -10.1.15 | Trait object types | Partial | See [Observations - Advanced features](#advanced-features) | -10.1.16 | Impl trait type | Partial | See [Observations - Advanced features](#advanced-features) | -10.1.17 | Type parameters | Partial | See [Observations - Advanced features](#advanced-features) | -10.1.18 | Inferred type | Partial | See [Observations - Advanced features](#advanced-features) | -10.2 | Dynamically Sized Types | Partial | See [Observations - Advanced features](#advanced-features) | +10.1.12 | Closure types | Partial | See [Notes - Advanced features](#advanced-features) | +10.1.13 | Pointer types | Partial | See [Notes - Advanced features](#advanced-features) | +10.1.14 | Function pointer types | Partial | See [Notes - Advanced features](#advanced-features) | +10.1.15 | Trait object types | Partial | See [Notes - Advanced features](#advanced-features) | +10.1.16 | Impl trait type | Partial | See [Notes - Advanced features](#advanced-features) | +10.1.17 | Type parameters | Partial | See [Notes - Advanced features](#advanced-features) | +10.1.18 | Inferred type | Partial | See [Notes - Advanced features](#advanced-features) | +10.2 | Dynamically Sized Types | Partial | See [Notes - Advanced features](#advanced-features) | 10.3 | Type layout | Yes | | 10.4 | Interior mutability | Yes | | 10.5 | Subtyping and Variance | Yes | | 10.6 | Trait and lifetime bounds | Yes | | -10.7 | Type coercions | Partial | See [Observations - Advanced features](#advanced-features) | +10.7 | Type coercions | Partial | See [Notes - Advanced features](#advanced-features) | 10.8 | Destructors | Partial | | 10.9 | Lifetime elision | Yes | | 11 | Special types and traits | Partial | | @@ -97,29 +97,31 @@ Reference | Feature | Support | Observations | 15.1 | Unsafe functions | Yes | | 15.2 | Unsafe blocks | Yes | | 15.3 | Behavior considered undefined | Partial | | -| | Data races | No | See [Observations - Concurrency](#concurrency) | +| | Data races | No | See [Notes - Concurrency](#concurrency) | | | Dereferencing dangling raw pointers | Yes | | | | Dereferencing unaligned raw pointers | No | | | | Breaking pointer aliasing rules | No | | | | Mutating immutable data | No | | -| | Invoking undefined behavior via compiler intrinsics | Partial | See [Observations - Intrinsics](#intrinsics) | +| | Invoking undefined behavior via compiler intrinsics | Partial | See [Notes - Intrinsics](#intrinsics) | | | Executing code compiled with platform features that the current platform does not support | No | | | | Producing an invalid value, even in private fields and locals | No | | -## Observations on partially or unsupported features +## Notes on partially or unsupported features ### Code generation for unsupported features -RMC aims to be a industrial verification tool. Most industrial crates may +RMC aims to be an industrial verification tool. Most industrial crates may include unsupported features in parts of their code that do not need to be -verified. In general, this should not prevent users from verifying their code. +verified. In general, this should not prevent users using RMC to verify their code. Because of that, the general rule is that RMC generates an `assert(false)` -statement when compiling any unsupported feature. This will cause proofs to fail -if the statement is reachable during the verification stage. However, the -analysis will not affected if the statement is not reachable from the code under -verification, so users can still verify components of their code not using -unsupported features. +statement followed by an `assume(false)` statement when compiling any +unsupported feature. `assert(false)` will cause verification to fail if the +statement is reachable during the verification stage, while `assume(false)` will +block any further exploration of the path. However, the analysis will not be +affected if the statement is not reachable from the code under verification, so +users can still verify components of their code that do not use unsupported +features. ### Assembly @@ -133,17 +135,20 @@ more about the current status. ### Concurrency -Concurrent features are out of scope for RMC. In general, the verification of -concurrent programs continues to be an open research problem where most tools -that analyze concurrent code lack support for other features. Because of this, -RMC emits a warning whenever it encounters concurrent code and compiles as if it -was sequential code. +Concurrent features are currently out of scope for RMC. In general, the +verification of concurrent programs continues to be an open research problem +where most tools that analyze concurrent code lack support for other features. +Because of this, RMC emits a warning whenever it encounters concurrent code and +compiles as if it was sequential code. ### Standard library functions At present, RMC is able to link in functions from the standard library but the -generated code will not contain them. This results in verification failures if -the code under verification, for example, includes a `println!` statement. +generated code will not contain them unless they generic, intrinsics, inlined or +macros. Missing functions are treated in a similar way to unsupported features +(i.e., replacing the function body with an `assert(false)` statement). This +results in verification failures if the code under verification, for example, +includes a reachable `println!` statement. We have done some experiments to embed the standard library into the generated code, but this causes verification times to increase significantly. As of now, @@ -155,7 +160,21 @@ for future work in this direction. The semantics around some advanced features (traits, types, etc.) from Rust are not formally defined which makes it harder to ensure that we can properly model -all their use cases. We are particularly interested in bug reports concerning +all their use cases. + +In particular, there are some outstanding issues to note here: + * Unimplemented `PointerCast::ClosureFnPointer` in + [#274](https://github.com/model-checking/rmc/issues/274) and `Variant` case + in projections type in + [#448](https://github.com/model-checking/rmc/issues/448). + * Unexpected fat pointer results in + [#82](https://github.com/model-checking/rmc/issues/82), + [#277](https://github.com/model-checking/rmc/issues/277), + [#327](https://github.com/model-checking/rmc/issues/327), + [#378](https://github.com/model-checking/rmc/issues/378) and + [#676](https://github.com/model-checking/rmc/issues/676). + +We are particularly interested in bug reports concerning these features, so please [file a bug report](https://github.com/model-checking/rmc/issues/new?assignees=&labels=bug&template=bug_report.md) if you are aware of one. @@ -187,7 +206,7 @@ In general, code generation for unsupported intrinsics follows the rule described in [Code generation for unsupported features](#code-generation-for-unsupported-features). -Name | Support | Observations | +Name | Support | Notes | --- | --- | --- | abort | Yes | | add_with_overflow | Yes | | @@ -376,8 +395,8 @@ truncf64 | Yes | | try | No | | type_id | Yes | | type_name | Yes | | -unaligned_volatile_load | Partial | See [Observations - Concurrency](#concurrency) | -unaligned_volatile_store | No | See [Observations - Concurrency](#concurrency) | +unaligned_volatile_load | Partial | See [Notes - Concurrency](#concurrency) | +unaligned_volatile_store | No | See [Notes - Concurrency](#concurrency) | unchecked_add | Yes | | unchecked_div | Yes | | unchecked_mul | Yes | | @@ -388,11 +407,11 @@ unchecked_sub | Yes | | unlikely | Yes | | unreachable | Yes | | variant_count | No | | -volatile_copy_memory | Partial | See [Observations - Concurrency](#concurrency) | -volatile_copy_nonoverlapping_memory | Partial | See [Observations - Concurrency](#concurrency) | -volatile_load | Partial | See [Observations - Concurrency](#concurrency) | -volatile_set_memory | No | See [Observations - Concurrency](#concurrency) | -volatile_store | No | See [Observations - Concurrency](#concurrency) | +volatile_copy_memory | Partial | See [Notes - Concurrency](#concurrency) | +volatile_copy_nonoverlapping_memory | Partial | See [Notes - Concurrency](#concurrency) | +volatile_load | Partial | See [Notes - Concurrency](#concurrency) | +volatile_set_memory | No | See [Notes - Concurrency](#concurrency) | +volatile_store | No | See [Notes - Concurrency](#concurrency) | wrapping_add | Yes | | wrapping_mul | Yes | | wrapping_sub | Yes | | @@ -401,13 +420,13 @@ write_bytes | Yes | | #### Atomics All atomic intrinsics are compiled as an atomic block where the operation is -performed. But as noted in [Observations - Concurrency](#concurrency), CBMC +performed. But as noted in [Notes - Concurrency](#concurrency), CBMC support for concurrent verification is limited and not used by default. Verification on code containing atomic intrinsics should not be trusted given that CBMC assumes the code to be sequential. #### SIMD instructions -While RMC is capable of generating code for SIMD instructions. Unfortunately, -CBMC does not provide support for some operations like vector comparison (e.g., -`simd_eq`) or shuffling (e.g., `simd_shuffle8`). +While RMC is capable of generating code for SIMD instructions, unfortunately, it +does not provide support for the verification of some operations like vector +comparison (e.g., `simd_eq`). From e478025f8dd94dad998eb0d51b2a95635d03bc64 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 4 Jan 2022 19:58:26 +0000 Subject: [PATCH 9/9] Minor comments --- rmc-docs/src/limitations.md | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/rmc-docs/src/limitations.md b/rmc-docs/src/limitations.md index 076a8c42b052..09838b38448e 100644 --- a/rmc-docs/src/limitations.md +++ b/rmc-docs/src/limitations.md @@ -144,11 +144,11 @@ compiles as if it was sequential code. ### Standard library functions At present, RMC is able to link in functions from the standard library but the -generated code will not contain them unless they generic, intrinsics, inlined or -macros. Missing functions are treated in a similar way to unsupported features -(i.e., replacing the function body with an `assert(false)` statement). This -results in verification failures if the code under verification, for example, -includes a reachable `println!` statement. +generated code will not contain them unless they are generic, intrinsics, +inlined or macros. Missing functions are treated in a similar way to unsupported +features (i.e., replacing the function body with an `assert(false)` statement). +This results in verification failures if the code under verification, for +example, includes a reachable `println!` statement. We have done some experiments to embed the standard library into the generated code, but this causes verification times to increase significantly. As of now, @@ -420,10 +420,10 @@ write_bytes | Yes | | #### Atomics All atomic intrinsics are compiled as an atomic block where the operation is -performed. But as noted in [Notes - Concurrency](#concurrency), CBMC -support for concurrent verification is limited and not used by default. -Verification on code containing atomic intrinsics should not be trusted given -that CBMC assumes the code to be sequential. +performed. But as noted in [Notes - Concurrency](#concurrency), RMC support for +concurrent verification is limited and not used by default. Verification on code +containing atomic intrinsics should not be trusted given that RMC assumes the +code to be sequential. #### SIMD instructions