Macros

Prusti makes use of procedural macros as the interface for user-provided specifications.

Specification syntax

Prusti specification syntax is a superset of Rust boolean expressions. The parsing of Prusti-specific syntax is achieved with a custom preparser. Parsing of Rust syntax is delegated to the syn crate.

The preparser accepts the following EBNF grammar:

assertion ::= prusti_expr ;
pledge ::= pledge_lhs, ",", prusti_expr ;
pledge_lhs ::= [ ? actual rust expression ?, "=>" ], prusti_expr ;
 
prusti_expr ::= conjunction, [ "==>", prusti_expr ] ;
conjunction ::= entailment, { "&&", entailment } ;
entailment ::= primary | ? actual rust expression ?, [ "|=", [ "|", ? args as parsed by syn2 ?, "|" ], "[", [ ( requires | ensures ), { ",", ( requires | ensures ) } ], "]" ] ;
primary ::= "(", prusti_expr, ")"
          | "forall", "(", "|", ? one or more args as parsed by syn2 ?, "|", prusti_expr, [ ",", "triggers", "=", ? array as parsed by syn2 ? ] ")"
          ;
requires ::= "requires", "(", prusti_expr, ")" ;
ensures ::= "ensures", "(", prusti_expr, ")" ;

Specification serialization

Because procedural macros are executed in a separate, sandboxed process, it is not straight-forward to pass data from procedural macros to the rest of the Prusti pipeline. Any collected data (e.g. parsed assertions) is therefore serialized and inserted into the processed HIR as attributes on dummy functions, where it can be picked up by a HIR visitor.