Merge pull request #1272 from arnaudgolfouse/document-creusot_contracts

Document more of `creusot_contracts`, and improve documentation layout
creusot-rs · Dec 2, 2024 · 7fbb07d · 7fbb07d
2 parents 29f350e + 4e0e61e
commit 7fbb07d
Show file tree

Hide file tree

Showing 93 changed files with 16,436 additions and 15,687 deletions.
diff --git a/README.md b/README.md
@@ -89,7 +89,7 @@ More examples are found in [creusot/tests/should_succeed](creusot/tests/should_s
 # Verifying with Creusot and Why3
 
 - To learn how to write code with creusot: [guide](https://creusot-rs.github.io/creusot/guide)
-- To see the API of `creusot_contracts` (creusot's "standart library"): [creusot_contracts API](https://creusot-rs.github.io/creusot/doc/creusot_contracts)
+- To see the API of `creusot_contracts` (creusot's "standard library"): [creusot_contracts API](https://creusot-rs.github.io/creusot/doc/creusot_contracts)
 
 # Hacking on Creusot
 

diff --git a/creusot-contracts-proc/src/doc.rs b/creusot-contracts-proc/src/doc.rs
@@ -1,26 +1,46 @@
 use proc_macro::TokenStream as TS1;
 use proc_macro2::TokenStream;
 use syn::{
-    GenericArgument, Generics, Ident, Lifetime, Path, PathArguments, QSelf, ReturnType, Type,
+    Attribute, GenericArgument, Generics, Ident, Lifetime, Path, PathArguments, QSelf, ReturnType,
+    Type,
 };
 
+/// The body of a logical function or a spec.
+#[derive(Debug)]
+pub(crate) enum LogicBody {
+    Some(TS1),
+    /// The function does not have a body. For example, if it is a trait function.
+    None,
+    /// The function has a body, but it is ignored because the function is `#[trusted]`
+    Trusted,
+}
+
 /// Generates a piece of documentation corresponding to the spec.
-pub(crate) fn document_spec(spec_name: &str, spec: TS1) -> TokenStream {
+pub(crate) fn document_spec(spec_name: &str, spec_body: LogicBody) -> TokenStream {
     let spec_color = match spec_name {
         "requires" => "Tomato",
         "ensures" => "DodgerBlue",
-        "terminates" | "pure" | "logic" | "logic(prophetic)" => "Violet",
+        "terminates" | "pure" | "logic" | "logic(prophetic)" | "law" => "Violet",
         _ => "LightGray",
     };
-    let spec_name =
-        format!("> <span style=\"color:{spec_color};\"><samp>{spec_name}</samp></span>");
-    if spec.is_empty() {
-        return quote::quote! {
-            #[cfg_attr(not(doctest), doc = "")]
-            #[cfg_attr(not(doctest), doc = #spec_name)]
-            #[cfg_attr(not(doctest), doc = "")]
-        };
-    }
+    let styled_spec_name = format!(
+        "<span style=\"color:{spec_color}; white-space:nowrap;\"><samp>{spec_name}</samp></span>"
+    );
+    let spec = match spec_body {
+        LogicBody::Some(s) if !s.is_empty() => s,
+        _ => {
+            let spec = if matches!(spec_body, LogicBody::Trusted) {
+                format!("{styled_spec_name} <span class=\"tooltip\" style=\"color:Red; white-space:nowrap;\" data-title=\"this function is trusted\"><sup>&#9888;</sup></span>")
+            } else {
+                styled_spec_name
+            };
+            return quote::quote! {
+                #[cfg_attr(not(doctest), doc = "")]
+                #[cfg_attr(not(doctest), doc = #spec)]
+                #[cfg_attr(not(doctest), doc = "")]
+            };
+        }
+    };
     let mut spec = {
         let mut span = None;
         for t in spec {
@@ -29,7 +49,7 @@ pub(crate) fn document_spec(spec_name: &str, spec: TS1) -> TokenStream {
                 Some(s) => span = s.join(t.span()),
             }
         }
-        let mut res = span.unwrap().source_text().unwrap();
+        let mut res = span.unwrap_or(proc_macro::Span::call_site()).source_text().unwrap();
         // hack to handle logic functions
         if res.starts_with("{\n") && res.ends_with("}") {
             let body = res[2..res.len() - 1].trim_end();
@@ -39,21 +59,56 @@ pub(crate) fn document_spec(spec_name: &str, spec: TS1) -> TokenStream {
                     std::cmp::min(leading_whitespace, line.len() - line.trim_start().len());
             }
             let mut trimmed_res = String::new();
-            for line in body.lines() {
+            for (i, line) in body.lines().enumerate() {
+                if i != 0 {
+                    trimmed_res.push('\n');
+                }
                 trimmed_res.push_str(&line[leading_whitespace..]);
-                trimmed_res.push('\n');
             }
             res = trimmed_res;
         }
         res
     };
-    spec = spec.replace('\n', "\n> > ");
-    spec = format!("> > ```\n> > {spec}\n> > ```");
-    quote::quote! {
-        #[cfg_attr(not(doctest), doc = "")]
-        #[cfg_attr(not(doctest), doc = #spec_name)]
-        #[cfg_attr(not(doctest), doc = #spec)]
+
+    if spec.len() > 80 - spec_name.len() || spec.contains('\n') {
+        spec = spec.replace('\n', "\n> ");
+        spec = format!("> ```\n> {spec}\n> ```");
+        quote::quote! {
+            #[cfg_attr(not(doctest), doc = "")]
+            #[cfg_attr(not(doctest), doc = #styled_spec_name)]
+            #[cfg_attr(not(doctest), doc = #spec)]
+        }
+    } else {
+        let spec = format!("```\n{spec}\n```");
+        quote::quote! {
+            #[cfg_attr(not(doctest), doc = "<div class=\"container\" style=\"display:flex; align-items:center; gap:5px; clip-path:inset(0.5em 0% 1.1em 0%);\"> <p>")]
+            #[cfg_attr(not(doctest), doc = #styled_spec_name)]
+            #[cfg_attr(not(doctest), doc = "   </p> <p>")]
+            #[cfg_attr(not(doctest), doc = "")]
+            #[cfg_attr(not(doctest), doc = #spec)]
+            #[cfg_attr(not(doctest), doc = "")]
+            #[cfg_attr(not(doctest), doc = "</p> </div>")]
+            #[cfg_attr(not(doctest), doc = "")]
+        }
+    }
+}
+
+pub(crate) fn is_trusted(attrs: &[Attribute]) -> bool {
+    for attr in attrs {
+        let path = attr.path();
+
+        if path.is_ident("trusted")
+            || (path.segments.len() == 3
+                && path
+                    .segments
+                    .iter()
+                    .zip(["creusot", "decl", "trusted"])
+                    .all(|(s1, s2)| s1.ident == s2))
+        {
+            return true;
+        }
     }
+    false
 }
 
 /// Create an item name from a type or a trait.

diff --git a/creusot-contracts-proc/src/lib.rs b/creusot-contracts-proc/src/lib.rs
@@ -206,7 +206,7 @@ fn sig_spec_item(tag: Ident, mut sig: Signature, p: Term) -> TokenStream {
 
 #[proc_macro_attribute]
 pub fn requires(attr: TS1, tokens: TS1) -> TS1 {
-    let documentation = document_spec("requires", attr.clone());
+    let documentation = document_spec("requires", doc::LogicBody::Some(attr.clone()));
 
     let mut item = parse_macro_input!(tokens as ContractSubject);
     let term = parse_macro_input!(attr as Term);
@@ -256,7 +256,7 @@ pub fn requires(attr: TS1, tokens: TS1) -> TS1 {
 
 #[proc_macro_attribute]
 pub fn ensures(attr: TS1, tokens: TS1) -> TS1 {
-    let documentation = document_spec("ensures", attr.clone());
+    let documentation = document_spec("ensures", doc::LogicBody::Some(attr.clone()));
 
     let mut item = parse_macro_input!(tokens as ContractSubject);
     let term = parse_macro_input!(attr as Term);
@@ -374,9 +374,22 @@ pub fn snapshot(assertion: TS1) -> TS1 {
     })
 }
 
+/// A structure to parse some attributes followed by something else.
+struct Attributes {
+    attrs: Vec<Attribute>,
+    rest: proc_macro2::TokenStream,
+}
+impl Parse for Attributes {
+    fn parse(input: parse::ParseStream) -> Result<Self> {
+        let attrs = Attribute::parse_outer(input).unwrap_or_else(|_| Vec::new());
+        let rest = input.parse()?;
+        Ok(Self { attrs, rest })
+    }
+}
+
 #[proc_macro_attribute]
 pub fn terminates(_: TS1, tokens: TS1) -> TS1 {
-    let documentation = document_spec("terminates", TS1::new());
+    let documentation = document_spec("terminates", doc::LogicBody::None);
     if let Ok(item) = syn::parse::<ImplItemFn>(tokens.clone()) {
         if let Some(def) = item.defaultness {
             return syn::Error::new(
@@ -388,14 +401,19 @@ pub fn terminates(_: TS1, tokens: TS1) -> TS1 {
         }
     };
 
-    let mut result = TS1::from(quote! { #[creusot::clause::terminates] #documentation });
-    result.extend(tokens);
-    result
+    let Attributes { attrs, rest } = syn::parse(tokens).unwrap();
+    quote! {
+        #[creusot::clause::terminates]
+        #(#attrs)*
+        #documentation
+        #rest
+    }
+    .into()
 }
 
 #[proc_macro_attribute]
 pub fn pure(_: TS1, tokens: TS1) -> TS1 {
-    let documentation = document_spec("pure", TS1::new());
+    let documentation = document_spec("pure", doc::LogicBody::None);
     if let Ok(item) = syn::parse::<ImplItemFn>(tokens.clone()) {
         if let Some(def) = item.defaultness {
             return syn::Error::new(
@@ -406,11 +424,15 @@ pub fn pure(_: TS1, tokens: TS1) -> TS1 {
             .into();
         }
     };
-    let mut result = TS1::from(
-        quote! { #[creusot::clause::no_panic] #[creusot::clause::terminates] #documentation },
-    );
-    result.extend(tokens);
-    result
+    let Attributes { attrs, rest } = syn::parse(tokens).unwrap();
+    quote! {
+        #[creusot::clause::no_panic]
+        #[creusot::clause::terminates]
+        #(#attrs)*
+        #documentation
+        #rest
+    }
+    .into()
 }
 
 #[proc_macro]
@@ -474,48 +496,84 @@ impl Parse for LogicInput {
     }
 }
 
+impl LogicInput {
+    fn logic_body(&self) -> doc::LogicBody {
+        match self {
+            LogicInput::Item(log_item) => {
+                if doc::is_trusted(&log_item.attrs) {
+                    doc::LogicBody::Trusted
+                } else {
+                    doc::LogicBody::Some(log_item.body.to_token_stream().into())
+                }
+            }
+            LogicInput::Sig(_) => doc::LogicBody::None,
+        }
+    }
+}
+
+enum LogicKind {
+    None,
+    Prophetic,
+    Law,
+}
+
+impl ToTokens for LogicKind {
+    fn to_tokens(&self, tokens: &mut TokenStream) {
+        match self {
+            Self::None | Self::Law => {}
+            Self::Prophetic => tokens.extend(quote!(#[creusot::decl::logic::prophetic])),
+        }
+    }
+}
+
 #[proc_macro_attribute]
-pub fn logic(prophetic: TS1, tokens: TS1) -> TS1 {
-    let prophetic = if prophetic.is_empty() {
-        None
+pub fn logic(kind: TS1, tokens: TS1) -> TS1 {
+    let kind = if kind.is_empty() {
+        LogicKind::None
     } else {
-        let t = parse_macro_input!(prophetic as Ident);
+        let t = parse_macro_input!(kind as Ident);
         if t == "prophetic" {
-            Some(quote!(#[creusot::decl::logic::prophetic]))
+            LogicKind::Prophetic
+        } else if t == "law" {
+            LogicKind::Law
         } else {
-            None
+            return syn::Error::new(
+                t.span(),
+                "unsupported modifier. The only supported modifier at the moment is `prophetic`",
+            )
+            .into_compile_error()
+            .into();
         }
     };
     let log = parse_macro_input!(tokens as LogicInput);
     let documentation = document_spec(
-        if prophetic.is_some() { "logic(prophetic)" } else { "logic" },
-        match &log {
-            LogicInput::Item(log_item) => log_item.body.to_token_stream().into(),
-            LogicInput::Sig(_) => TS1::new(),
+        match kind {
+            LogicKind::None => "logic",
+            LogicKind::Prophetic => "logic(prophetic)",
+            LogicKind::Law => "law",
         },
+        if matches!(kind, LogicKind::Law) { doc::LogicBody::None } else { log.logic_body() },
     );
     match log {
-        LogicInput::Item(log) => logic_item(log, prophetic, documentation),
-        LogicInput::Sig(sig) => logic_sig(sig, prophetic, documentation),
+        LogicInput::Item(log) => logic_item(log, kind, documentation),
+        LogicInput::Sig(sig) => logic_sig(sig, kind, documentation),
     }
 }
 
-fn logic_sig(
-    sig: TraitItemSignature,
-    prophetic: Option<TokenStream>,
-    documentation: TokenStream,
-) -> TS1 {
+fn logic_sig(mut sig: TraitItemSignature, kind: LogicKind, documentation: TokenStream) -> TS1 {
     let span = sig.span();
+    let attrs = std::mem::take(&mut sig.attrs);
 
     TS1::from(quote_spanned! {span =>
         #[creusot::decl::logic]
-        #prophetic
+        #kind
+        #(#attrs)*
         #documentation
         #sig
     })
 }
 
-fn logic_item(log: LogicItem, prophetic: Option<TokenStream>, documentation: TokenStream) -> TS1 {
+fn logic_item(log: LogicItem, kind: LogicKind, documentation: TokenStream) -> TS1 {
     let span = log.sig.span();
 
     let term = log.body;
@@ -527,9 +585,9 @@ fn logic_item(log: LogicItem, prophetic: Option<TokenStream>, documentation: Tok
 
     TS1::from(quote_spanned! {span =>
         #[creusot::decl::logic]
-        #prophetic
-        #documentation
+        #kind
         #(#attrs)*
+        #documentation
         #vis #def #sig {
             #req_body
         }
@@ -542,7 +600,7 @@ pub fn law(_: TS1, tokens: TS1) -> TS1 {
     TS1::from(quote! {
         #[creusot::decl::law]
         #[creusot::decl::no_trigger]
-        #[::creusot_contracts::logic]
+        #[::creusot_contracts::logic(law)]
         #tokens
     })
 }
@@ -583,10 +641,7 @@ pub fn predicate(prophetic: TS1, tokens: TS1) -> TS1 {
 
     let documentation = document_spec(
         if prophetic.is_some() { "logic(prophetic)" } else { "logic" },
-        match &pred {
-            LogicInput::Item(log_item) => log_item.body.to_token_stream().into(),
-            LogicInput::Sig(_) => TS1::new(),
-        },
+        pred.logic_body(),
     );
 
     match pred {
@@ -596,14 +651,16 @@ pub fn predicate(prophetic: TS1, tokens: TS1) -> TS1 {
 }
 
 fn predicate_sig(
-    sig: TraitItemSignature,
+    mut sig: TraitItemSignature,
     prophetic: Option<TokenStream>,
     documentation: TokenStream,
 ) -> TS1 {
     let span = sig.span();
+    let attrs = std::mem::take(&mut sig.attrs);
     TS1::from(quote_spanned! {span =>
         #[creusot::decl::predicate]
         #prophetic
+        #(#attrs)*
         #documentation
         #sig
     })
@@ -626,8 +683,8 @@ fn predicate_item(
     TS1::from(quote_spanned! {span =>
         #[creusot::decl::predicate]
         #prophetic
-        #documentation
         #(#attrs)*
+        #documentation
         #vis #def #sig {
             #req_body
         }