Introduce rmc::proof function attribute #668

tedinski · 2021-11-24T02:21:16Z

Description of changes:

Introduce new rmc-annotations crate. This is necessary because to introduce proc macros, they need to be in a crate by themselves. Added as dependency of rmc crate. (And has to be injected in RMC's rustc flags.)
Added a #[rmc::proof] attribute. In the long run, this is meant to "work" (do the reasonable thing) whether under RMC or not. Under RMC (the only thing we use right now), it just expands to #[rmctool::proof].
The compiler now recognizes that attribute, and records the function and its mangled name in a new .rmc-metadata.json that will likely just grow to subsume everything we emit that isn't the symbol table (e.g. .type_map.json) later on.

Resolved issues:

Resolves... figure that out

Call-outs:

We should merge Add option to restrict vtable function pointers #536 before this, as I think there will be git merge conflicts and this is the smaller changer, easier to fix.
Right now functions marked with #[rmc::proof] must be pub or we silently don't notice it at all. I need to figure out a fix for this. Ideally it'd just work without issue, but I'd even settle for an error check for a missing pub if that's all we can figure out how to do, but even that's not obvious to me since we never call codegen_function as that's the problem in the first place!
"Actually using this emitted data" is a future PR, where we start implementing a production-quality cargo rmc. Notably, though, cargo typically produces a single .rmc-metadata.json (and friends) per-crate. So we'd really just be looking for the proof harnesses in our crate, not from our dependencies. (Or perhaps some similar heuristic. Only from local crates?)

Testing:

How is this change tested? TODO - draft PR
Is this a refactor change?

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

I'm so happy to see this going through! I know this is just a draft, but I left a few comments. Cheers

celinval · 2021-11-26T00:18:59Z

compiler/cbmc/src/goto_program/location.rs

    }

+    pub fn filename(&self) -> Option<String> {
+        match self {


Just a suggestion. This could be a one liner:

if let Location::Loc { file, .. } = self { Some(file.to_string) } else { None }

celinval · 2021-11-26T00:22:56Z

compiler/rustc_codegen_rmc/src/codegen/function.rs

+    ///
+    /// Currently, this is only proof harness annotations.
+    /// i.e. `#[rmc::proof]` (which rmc-annotations translates to `#[rmctool::proof]` for us to handle here)
+    fn codegen_rmctool_attributes(&mut self) {


I would suggest renaming to something like collect_rmc_attributes? This is not quite codegen.

I was also wondering if these functions should be inside metadata.rs instead.

Why do we need &mut?

celinval · 2021-11-26T00:24:08Z

compiler/rustc_codegen_rmc/src/codegen/function.rs

+    fn codegen_rmctool_attributes(&mut self) {
+        let instance = self.current_fn().instance();
+
+        for attr in self.tcx.get_attrs(instance.def_id()) {


Can you please add a debug statement?

celinval · 2021-11-26T00:47:15Z

compiler/rustc_codegen_rmc/src/codegen/function.rs

+        let instance = self.current_fn().instance();
+
+        for attr in self.tcx.get_attrs(instance.def_id()) {
+            if matches_rmctool_attr(attr, "proof") {


Can we add a sanity check somewhere that validates the rmctool attributes used in the function?

celinval · 2021-11-26T00:52:38Z

compiler/rustc_codegen_rmc/src/codegen/function.rs

+    }
+}
+
+fn matches_rmctool_attr(attr: &ast::Attribute, name: &str) -> bool {


I would return a set of rmctool attributes. We are planning to add multiple attributes, right? I don't think this method will scale well.

library/rmc-annotations/src/lib.rs

celinval · 2021-11-26T01:28:05Z

library/rmc-annotations/src/lib.rs

+    // but outside RMC, this code is likely never called.
+    let mut result = TokenStream::new();
+
+    result.extend("#[allow(dead_code)]".parse::<TokenStream>().unwrap());


I wouldn't add this. We don't want proof methods to inadvertently make it to the final library / binary. We can either extend with a #[cfg(proof)] or just document that users should do that.

I thought about additionally branching into having a debug/release version of the macro, with the release removing the function entirely. Would that work for you?

My goal here was to ensure #[proof] is enough all by itself and nothing further needs to be added, just like #[test]

But come to think of it, I think this won't work as-is anyway. If the goal is to let users add rmc as a dev-dependency, then this package (defining the #[proof] macro) wouldn't be in the dependency list anyway during a normal non-test compile. :( Might have to have a rethink about that problem...

Gotcha. I'm OK with the idea of users adding #[proof] by itself. I would just prefer for it to be a no-op if they are not using rmc. I.e., I would prefer if we remove the #[allow(dead_code)].

library/rmc-annotations/src/lib.rs

library/rmc/src/lib.rs

celinval · 2021-11-26T01:31:56Z

library/rmc-annotations/src/lib.rs

+pub fn proof(_attr: TokenStream, item: TokenStream) -> TokenStream {
+    let mut result = TokenStream::new();
+
+    result.extend("#[rmctool::proof]".parse::<TokenStream>().unwrap());


Can you please add the #[no_mangle] for now? You can link to #661 for us to remove it.

I thought the need for no_mangle was just the UI problem of predicting the mangled name. This feature is intended to solve that, since we get a map:

{ "pretty_name": "testing", "mangled_name": "_RNvCs1NZMV7qnTwy_1f7testing", "original_file": "/home/ubuntu/experiments/proof_anno/f.rs" }

Is there some other reason for no_mangle? Otherwise, I don't know why I'd add it here.

I was thinking about addressing that in a follow up PR so this PR doesn't get too big and we can merge it sooner rather than later. If you do add that to this PR, then it's OK to keep it without the no_mangle.

There are two reasons why we rely on the #[no_mangle] today. One is the friendly name and the second is that no_mangle makes the function public.

compiler/rustc_codegen_rmc/src/codegen/function.rs

tedinski · 2021-12-02T00:10:59Z

Merged and resolved conflicts with Alexa's changes. (Went easier than expected!)
I've renamed the crate to rmc_macros as that's more literal (and probably more correct, since eventually I think we might end up with a rmc::stub! { ... } macro...)
I've added no_mangle. The change we've made in Re-enable RMC to allow users to verify non-public main. #656 (I think) meant making a proof harness pub was no longer sufficient to codegen it, so I had to do something. I'm still not happy with this choice, since it comes with significant drawbacks (like name collisions).
I've broken the proof macro into three cases, instead of the old two, based on cfg(test):
1. !RMC, !Test (i.e. "normal build"): eliminate the proof harness. This will probably never happen since we expect #[rmc::proof] to (eventually) be brought in via a dev-dependency, but this ensures that's the case.
2. !RMC, Test: Leave it, but suppress dead code warnings. This makes it editable in IDEs and ensures it get compiled under normal testing conditions.
3. RMC: Now we know we can use the tool attribute. Also, as a hack temporarily, no_mangle so the function actually gets codegen'd.

Remaining things before mergable:

Revisit naming/comments around codegen_rmctool_attributes. Celina thought the name was weird and didn't notice the self.proof_harnesses.push mutation, which means the code isn't obvious enough yet. So I should fix that.
Add line numbers as requested by Zyad. Good idea. I had them originally but lost them in some debugging shuffling. (This code had a lot of iterations and failed experiments.)
I really want a better fix so I don't need no_mangle :(

celinval · 2021-12-02T06:28:01Z

Regarding # 3, I believe it should still work if you export RUSTFLAGS="--crate-type=lib". It should also work for cargo projects that are libraries.

Maybe we should add an option to rmc to allow switching them or just detect whether user target function is main or not.

tedinski · 2021-12-06T21:45:27Z

I think this is ready to merge.

Hopefully the code Celina tripped over is much clearer now.
I haven't added a requested debug line (not sure what'd be useful here...)

Checklist for me after merge:

Update RMC should use fully qualified name for harness selection and it should not rely on no_mangle attribute #661 to add more information on what the problem is and the path forward to eliminating no_mangle
Create feature request for #[rmc::unwind = 9] optional unwind annotations Add support for common proof options #600
Create feature request for annotation validation (e.g. right now, maybe just objecting to duplicate proof annotations? Or if the proof harness has any parameters? Support for parameters is something we could add later...) Introduce rmctool attribute validation #689
Create feature request to merge type_map and restrictions json files into rmc-metadata Merge type_map and restrictions into rmc-metadata.json #690
Create an issue to ensure cargo-rmc includes tests that exercise testing the output in rmc-metadata. Currently, we're not testing the changes in this PR. End-to-end tests needed for proof harness attributes #691

My next steps after this are to get started on a "real" Rust cargo-rmc application, which will subsume our current scripts and be the tool that actually consumes rmc-metadata from this PR.

celinval · 2021-12-07T22:49:30Z

I think this is ready to merge.

1. Hopefully the code Celina tripped over is much clearer now.

2. I haven't added a requested debug line (not sure what'd be useful here...)

Checklist for me after merge:

* [ ]  Update [RMC should use fully qualified name for harness selection and it should not rely on `no_mangle` attribute #661](https://github.com/model-checking/rmc/issues/661) to add more information on what the problem is and the path forward to eliminating `no_mangle`

* [ ]  Create feature request for `#[proof(unwind = 9)]` optional unwind annotations

* [ ]  Create feature request for annotation validation (e.g. right now, maybe just objecting to duplicate proof annotations? Or if the proof harness has any parameters? Support for parameters is something we could add later...)

* [ ]  Create feature request to merge `type_map` and `restrictions` json files into `rmc-metadata`

* [ ]  Create an issue to ensure `cargo-rmc` includes tests that exercise testing the output in `rmc-metadata`. Currently, we're not testing the changes in this PR.

My next steps after this are to get started on a "real" Rust cargo-rmc application, which will subsume our current scripts and be the tool that actually consumes rmc-metadata from this PR.

For the second bullet, we already have: #600

celinval

Just a few minor comments. Thanks

celinval · 2021-12-07T22:55:53Z

compiler/rustc_codegen_rmc/src/codegen/function.rs

+    }
+
+    /// Update `self` (the goto context) to add the current function as a listed proof harness
+    fn handle_rmctool_proof(&mut self) {


What is the plan for proof options like unwind? Are you thinking about adding arguments to this attribute or creating new attributes?

I'm thinking add arguments to this attribute, yes.

celinval · 2021-12-07T23:01:01Z

compiler/rustc_codegen_rmc/src/compiler_interface.rs

            None
        };

+        let metadata = RmcMetadata { proof_harnesses: c.proof_harnesses };


Why do we need this?

(I'm not sure what you mean by 'this'. The RmcMetadata type?) I'm planning on the rmc-metadata file becoming where we emit everything that isn't the symtab. So type_map, function restrictions, and more things like notable/important warnings (instead of just logging them).

Sorry, I mean the copy statement.

Still not sure what the "copy statement" is.

celinval · 2021-12-07T23:14:46Z

I also forgot... can you please a testcase?

tedinski · 2021-12-08T18:07:07Z

I also forgot... can you please a testcase?

I really want to but nothing reads this yet, so I was going to create an issue to not forget, and include that as part of cargo-rmc.

celinval · 2021-12-08T18:41:06Z

I also forgot... can you please a testcase?

I really want to but nothing reads this yet, so I was going to create an issue to not forget, and include that as part of cargo-rmc.

For now, it would at least ensure that things compile and that this code doesn't crash.

tedinski · 2021-12-08T18:42:59Z

For now, it would at least ensure that things compile and that this code doesn't crash.

Ah, this code is running by default, so all existing tests are exercising it. We're just not examining the output to see if it's correct (i.e. that proof harnesses show up and only the correct ones, etc)

tedinski · 2021-12-08T18:43:55Z

For now, it would at least ensure that things compile and that this code doesn't crash.

Oh wait, you mean add a test that has a harness to that actual branch gets run, even if nothing looks at it. I can do that.

tedinski · 2021-12-08T19:10:28Z

Ok, I've added a cargo-rmc test with a proof annotation, so now the code for the macro and the branch that actually adds a proof harness to the rmc-metadata is actually getting run in our tests. (With nothing checking on the output yet to ensure it's correct, but at least running and not crashing.)

* Introduce rmc::proof function attribute * add no_mangle as temporary measure to force function codegen

Introduce rmc::proof function attribute

1502f02

celinval suggested changes Nov 26, 2021

View reviewed changes

zhassan-aws reviewed Nov 29, 2021

View reviewed changes

compiler/rustc_codegen_rmc/src/codegen/function.rs Outdated Show resolved Hide resolved

tedinski added 4 commits November 29, 2021 22:36

merge from origin/main

ea2be69

rename crate to 'rmc_macros'

ee317ea

add no_mangle as temporary measure to force function codegen

e4de683

rmc::proof with 3 cases, not 2: normal build, test build, rmc build

37d6aa2

tedinski added 3 commits December 2, 2021 21:57

Merge remote-tracking branch 'origin/main' into proof-anno

1446d36

refactor the attribute 'parsing' code a bit

76081aa

Add original_line to proof harness metadata

00788d2

tedinski marked this pull request as ready for review December 6, 2021 21:45

tedinski requested a review from a team as a code owner December 6, 2021 21:45

celinval reviewed Dec 7, 2021

View reviewed changes

tedinski added 2 commits December 8, 2021 18:47

Merge remote-tracking branch 'origin/main' into proof-anno

9709a0b

introduce a 'exercise test' for proof annotations

2377945

celinval approved these changes Dec 10, 2021

View reviewed changes

tedinski merged commit 5b9071e into model-checking:main Dec 10, 2021

tedinski deleted the proof-anno branch December 10, 2021 17:01

celinval mentioned this pull request Dec 17, 2021

Add support for common proof options #600

Closed

2 tasks

jaisnan self-assigned this Jan 5, 2022

jaisnan removed their assignment Jan 5, 2022

tedinski added a commit to tedinski/rmc that referenced this pull request Apr 26, 2022

Introduce rmc::proof function attribute (model-checking#668)

d3606dc

* Introduce rmc::proof function attribute * add no_mangle as temporary measure to force function codegen

tedinski added a commit that referenced this pull request Apr 27, 2022

Introduce rmc::proof function attribute (#668)

f751146

* Introduce rmc::proof function attribute * add no_mangle as temporary measure to force function codegen

github-actions bot mentioned this pull request May 18, 2025

Automatic toolchain upgrade to nightly-2025-05-18 #4083

Merged

Introduce rmc::proof function attribute #668

Introduce rmc::proof function attribute #668

Uh oh!

Conversation

tedinski commented Nov 24, 2021

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

Uh oh!

celinval 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!

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!

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!

tedinski commented Dec 2, 2021

Uh oh!

celinval commented Dec 2, 2021

Uh oh!

tedinski commented Dec 6, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

celinval commented Dec 7, 2021

Uh oh!

celinval 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!

celinval commented Dec 7, 2021

Uh oh!

tedinski commented Dec 8, 2021

Uh oh!

celinval commented Dec 8, 2021

Uh oh!

tedinski commented Dec 8, 2021

Uh oh!

tedinski commented Dec 8, 2021

Uh oh!

tedinski commented Dec 8, 2021

Uh oh!

Reviewers

Assignees

Labels

Projects

tedinski commented Dec 6, 2021 •

edited

Loading