Documentation: Limitations by adpaco-aws · Pull Request #714 · model-checking/kani

adpaco-aws · 2021-12-22T22:55:31Z

Description of changes:

No changes to RMC. Adds a new section "Limitations" to documentation in order to summarize the current status in regards to Rust feature support using a table.

Preview here

Call-outs:

Open as draft so I can get some feedback.

Testing:

How is this change tested? Running remote server for documentation.
Is this a refactor change? No.

Checklist

Each commit message has a non-empty body, explaining why the change was made
Methods or procedures are documented
Regression or unit tests are included, or existing tests cover the modified code
My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

celinval

Thanks for doing this. I just have a few minor comments.

Can you please add that we currently do not support stack unwinding?

rmc-docs/src/limitations.md

celinval · 2021-12-29T20:39:06Z

rmc-docs/src/limitations.md

We should add that we support to generic functions and macros at this point. They get monomorphized / expanded during the compilation. BTW, I don't think we are running the rustc pass to inline functions.

Not sure why you want to add it here. I think the table already includes this information and I'm not sure what it has to do with the standard library.

Removed "unless they are inlined" from this block.

Sorry if I wasn't clear. I was talking about the "unless they are inlined". The correct would be "unless they are generic, intrinsics, inlined or macros." :)

celinval · 2021-12-29T20:39:48Z

rmc-docs/src/limitations.md

Did we run these experiments before or after enabling the code slicing?

If you refer to --drop-unused-functions, I tried both when doing these experiments. It reduced the generated code considerably, but still kept many other functions around which made this approach unfeasible.

did your experiments include tests with println?

Yes, in fact they just included println.

rmc-docs/src/limitations.md

adpaco-aws · 2021-12-30T21:56:17Z

Thanks @celinval ! Updated the PR with some of your suggestions, let me know if you have other comments 😄

adpaco-aws · 2022-01-03T15:30:29Z

Forgot to mention stack unwinding - Added a new section on panic strategies just now.

rmc-docs/src/limitations.md

tedinski · 2022-01-03T16:10:31Z

rmc-docs/src/limitations.md

+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


~~not using~~ that do not use

(I think your phrasing is technically fine, it is just potentially ambiguous what 'not using' refers to (the code, not the verification) until you read after it in the sentence.)

(Hopefully not too nitpicky here, but it's public facing documentation, so I'm looking for these things)

No worries, feedback regarding these subtleties is welcome too! It's changed now.

tedinski · 2022-01-03T16:13:31Z

rmc-docs/src/limitations.md

+
+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`).


wait, I thought I added shuffle.

Sorry, I thought this was not supported by CBMC but after reviewing related issues I see that you implemented shuffle operations in RMC. So I removed shuffling from here.

tedinski · 2022-01-03T16:16:54Z

rmc-docs/src/limitations.md

+issue](https://github.com/model-checking/rmc/issues/581), but we have some ideas
+for future work in this direction.
+
+### Advanced features


I worry this section might be too vague. It might be a good idea to back-reference what we say in the table? (E.g. there's a lot of links from the table to here that seem to be about projections, and I think our goal is to have to solid by 1.0.)

I think over-technical would be better than vague. If this section answered for us "what would it take for us to remove this section from this doc because we know we support it now" I think that's be better than being vague.

I was not sure how to make this more technical, so I highlighted some outstanding issues here.

Please let me know how it looks and if it does not look good to you we can work together on this section.

celinval

It looks good to me. Please make sure you address Ted's feedback before pushing. :)

zhassan-aws

First batch of comments.

zhassan-aws · 2022-01-03T18:19:17Z

rmc-docs/src/limitations.md

+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 |


Would "Remarks" or "Notes" be more suitable than "Observations"?

Replaced with "Notes".

zhassan-aws · 2022-01-03T18:22:54Z

rmc-docs/src/limitations.md

+
+### Code generation for unsupported features
+
+RMC aims to be a industrial verification tool. Most industrial crates may


Suggested change

RMC aims to be a industrial verification tool. Most industrial crates may

RMC aims to be an industrial verification tool. Most industrial crates may

Not sure I like the word "industrial", but can't think of an alternative.

Done, let me know if you think of another word (I don't like it that much neither).

One possibility (I don't feel strongly about it either): RMC is intended to be used on real-world Rust code. Most real-world crates ...

zhassan-aws · 2022-01-03T18:24:07Z

rmc-docs/src/limitations.md

+
+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.


Suggested change

verified. In general, this should not prevent users from verifying their code.

verified. In general, this should not prevent users from using RMC to verify their code.

zhassan-aws · 2022-01-03T18:27:22Z

rmc-docs/src/limitations.md

+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)`


Technically, it generates assert(false) followed by assume(false). I think this piece of detail is worth mentioning since it may cause some asserts to become unreachable, and hence vacuously pass.

Alright, added both and included a short sentence to explain what they do. Let me know how it looks to you.

zhassan-aws · 2022-01-03T18:28:10Z

rmc-docs/src/limitations.md

+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


Suggested change

statement when compiling any unsupported feature. This will cause proofs to fail

statement when compiling any unsupported feature. This will cause verification to fail

zhassan-aws · 2022-01-03T18:30:12Z

rmc-docs/src/limitations.md

+verification, so users can still verify components of their code not using
+unsupported features.
+
+### Assembly


I think the official term is "Inline Assembly".

There are two options in Rust for adding assembly code: Inline and global. Note that below we link an issue for each of them, so I thought "Assembly" was a good name for this section.

zhassan-aws · 2022-01-03T18:31:32Z

rmc-docs/src/limitations.md

+
+### Concurrency
+
+Concurrent features are out of scope for RMC. In general, the verification of


Should we add "currently"?

Suggested change

Concurrent features are out of scope for RMC. In general, the verification of

Concurrent features are currently out of scope for RMC. In general, the verification of

zhassan-aws · 2022-01-03T18:34:02Z

rmc-docs/src/limitations.md

+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.


Does RMC pick some order for execution of the concurrent code? If so, we should point out that this may lead to RMC missing bugs that may occur with a different execution order.

AFAIK it assumes all code to be sequential. I think there are some CBMC options for concurrent code verification but we do not make use of them at the moment.

zhassan-aws · 2022-01-03T18:39:10Z

rmc-docs/src/limitations.md

+### 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


but the generated code will not contain them

This sentence a bit vague. Can we clarify it? Does RMC generate these functions with an empty body?

Added a sentence to mention these are treated in a similar way to unsupported features. Let me know what you think!

rmc-docs/src/limitations.md

zhassan-aws · 2022-01-04T18:48:42Z

rmc-docs/src/limitations.md

+### 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


Suggested change

generated code will not contain them unless they generic, intrinsics, inlined or

generated code will not contain them unless they are generic, intrinsics, inlined or

zhassan-aws · 2022-01-04T18:53:07Z

rmc-docs/src/limitations.md

+#### Atomics
+
+All atomic intrinsics are compiled as an atomic block where the operation is
+performed. But as noted in [Notes - Concurrency](#concurrency), CBMC


Should we replace the two occurrences of CBMC in this section by RMC?

* Initial version of support table * Define support values for table * Add intrinsics table and other content * Observations on stdlib * Address Celina's comments * More comments * Add section on panic strategies * Address more comments * Minor comments

adpaco-aws force-pushed the support-table branch from 1b78dc5 to 81c945f Compare December 23, 2021 19:08

celinval suggested changes Dec 29, 2021

View reviewed changes

adpaco-aws added 5 commits December 30, 2021 21:08

Initial version of support table

a5b9487

Define support values for table

009f2e1

Add intrinsics table and other content

65f3cff

Observations on stdlib

932b093

Address Celina's comments

cbe1e52

adpaco-aws force-pushed the support-table branch from 81c945f to cbe1e52 Compare December 30, 2021 21:37

More comments

efe48b0

adpaco-aws marked this pull request as ready for review December 30, 2021 21:55

adpaco-aws requested a review from a team as a code owner December 30, 2021 21:55

Add section on panic strategies

88e1880

tedinski reviewed Jan 3, 2022

View reviewed changes

celinval approved these changes Jan 3, 2022

View reviewed changes

zhassan-aws reviewed Jan 3, 2022

View reviewed changes

Address more comments

58a831c

tedinski approved these changes Jan 4, 2022

View reviewed changes

zhassan-aws approved these changes Jan 4, 2022

View reviewed changes

adpaco-aws and others added 2 commits January 4, 2022 19:58

Minor comments

e478025

Merge branch 'main' into support-table

a88af2a

adpaco-aws merged commit 1f3e3b2 into model-checking:main Jan 4, 2022

adpaco-aws mentioned this pull request Jan 5, 2022

Intrinsics Audit #727

Closed


		### Code generation for unsupported features

		RMC aims to be a industrial verification tool. Most industrial crates may

	RMC aims to be a industrial verification tool. Most industrial crates may
	RMC aims to be an industrial verification tool. Most industrial crates may

	verified. In general, this should not prevent users from verifying their code.
	verified. In general, this should not prevent users from using RMC to verify their code.

	statement when compiling any unsupported feature. This will cause proofs to fail
	statement when compiling any unsupported feature. This will cause verification to fail


		### Concurrency

		Concurrent features are out of scope for RMC. In general, the verification of

	Concurrent features are out of scope for RMC. In general, the verification of
	Concurrent features are currently out of scope for RMC. In general, the verification of

	generated code will not contain them unless they generic, intrinsics, inlined or
	generated code will not contain them unless they are generic, intrinsics, inlined or

Conversation

adpaco-aws commented Dec 22, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description of changes:

Call-outs:

Testing:

Checklist

Uh oh!

celinval left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

adpaco-aws commented Dec 30, 2021

Uh oh!

adpaco-aws commented Jan 3, 2022

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

celinval left a comment

Choose a reason for hiding this comment

Uh oh!

zhassan-aws left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

zhassan-aws Jan 3, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

adpaco-aws commented Dec 22, 2021 •

edited

Loading

zhassan-aws Jan 3, 2022 •

edited

Loading

zhassan-aws Jan 3, 2022 •

edited

Loading