search

AeneasVerif / charon

Interface with the rustc compiler for the purpose of program verification
Apache License 2.0
75 stars 15 forks source link

Add an attribute to mark definitions as `opaque` #206

Closed sonmarcho closed 1 week ago

sonmarcho commented 3 months ago

It is currently possible to pass an option to Charon to mark some modules as opaque, so that Charon will not look inside those definitions (it treats them similarly to external definitions). This option is a bit coarse grained: it would be good to be able to individually mark the functions with a charon::opaque attribute. In order not to confuse the Aeneas users, I suggest introducing a aeneas::opaque attribute which does the same, and generally speaking introducing both a charon::... and an aeneas::... version of every new attribute.

Nadrieril commented 3 months ago

Note: rustc will complain about such an attribute because it will try to find a macro with that name. Adding

#![feature(register_tool)]
#![register_tool(charon)]

at the top of each file that uses the attributes should solve the problem I hope. We can think of a cleaner solution afterwards. (See here for details about this feature).

sonmarcho commented 3 months ago

Ok, thanks for looking into this. My understanding is that there are clean ways of doing this, but I'm indeed not aware of the details. It might be worth looking at other verification projects which use attributes (e.g., Verus or Creusot).

Nadrieril commented 3 months ago

Creusot defines a proc-macro for their #[ensures]/#[invariant] etc attributes. That's one of the options available (and you started doing something like that with the attributes crate).

sonmarcho commented 3 months ago

What do you recommend doing? I initially thought that was the only way of doing, but I would prefer a way which doesn't require adding a dependency to Charon directly in the Rust code.

Nadrieril commented 3 months ago

register_tool is the simplest right now. I've heard discussions on the rustc side about what the best design for this feature would be, so I'd suggest using it for now and they'll likely figure out something more practical, e.g. a line to add in your Cargo.toml.

zhassan-aws commented 3 months ago

In case it helps, in Kani, we pass feature(register_tool) as part of the Rust flags:

https://github.com/model-checking/kani/blob/4a889397bba73fb76f0a21aad66171daad0b2b31/kani-driver/src/call_single_file.rs#L175-L178

Nadrieril commented 3 months ago

https://github.com/AeneasVerif/charon/pull/227 allows the attribute on definitions; it would be nice to also allow the attribute on modules.

Nadrieril commented 1 week ago

These attributes are supported on modules since one of the recent PRs that overhauled opaque handling.