Using pearlite! in a regular Rust function should probably error

[sarsko]

Not super important, but if one forgets to add #[logic]/#[predicate] and uses the pearlite! macro, Creusot will not complain. I think it would be better if it is checked by Creusot, rather than resulting in a not so helpful Why3 error.

Example:

extern crate creusot_contracts;
use creusot_contracts::*;
fn some_name() -> bool {
    pearlite!{ 0 === 0 }
}

Gives the following error in Why3: File "../ex.mlcfg", line 45, characters 99-109: unbound program function or variable symbol 'From0.from'

[xldenis]

I don't know of an easy way to prevent the pearlite! invocation itself, but I think this ties in with #35 #167 etc... I've been doing exploratory work on this front about how to enforce a proper separation even at the Rust level, however, it remains "challenging" :P

[xldenis]

I think this is pretty trivial to check in a lint :)

[xldenis]

use rustc_hir::def_id::DefId;
use rustc_lint::{LateContext, LateLintPass, LintContext};
use rustc_session::{declare_tool_lint, impl_lint_pass};
use rustc_span::{ExpnData, ExpnId, Span};

use crate::util;


declare_tool_lint! {
    /// Blah Blah
    pub creusot::PEARLITE,
    Forbid,
    "checks for valid usages of the pearlite macro"
}

pub struct PearliteInProgram {}
impl_lint_pass!(PearliteInProgram => [PEARLITE]);

fn root_macro_call(s: Span) -> Option<(DefId, ExpnId, Span)> {
    s.macro_backtrace()
        .filter_map(|exp_data| {
            if let ExpnData { parent, call_site, macro_def_id: Some(def_id), .. } = exp_data {
                Some((def_id, parent, call_site))
            } else {
                None
            }
        })
        .last()
}

impl<'tcx> LateLintPass<'tcx> for PearliteInProgram {
    fn check_expr(&mut self, cx: &LateContext<'tcx>, e: &'tcx rustc_hir::Expr<'tcx>) {
        eprintln!("Pearlite lint");
        if let Some((def_id, _, span)) = root_macro_call(e.span)
        && cx.tcx.item_name(def_id).as_str().contains("pearlite")
        && let Some(id) = cx.enclosing_body
        && let def_id = cx.tcx.hir().body_owner_def_id(id).to_def_id()
        && !util::is_logic(cx.tcx, def_id) && !util::is_predicate(cx.tcx, def_id) {
            cx.struct_span_lint(PEARLITE, span, "the `pearlite!` macro can only be used within `#[logic]` or `#[predicate]` functions", |lint| lint)
        }
    }
}

This lint implements the check. However, it acutally runs too late today in Creusot because we do some stuff before analysis which checks the 'purity' of calls. This check means that we will properly emit an error when you call functions with the wrong purity but you wont get a great error because it runs so late in the compilation chain.

[xldenis]

Today, we don't forbid the actual macro, but any call to a logical symbol will raise an error. I'm going to close this for now.