Add add option for running why3 though cargo creusot CLI

cargo-creusot/src/options.rs

@@ -35,6 +35,9 @@ pub struct CreusotArgs {
     /// Use `result` as the trigger of definition and specification axioms of logic/ghost/predicate functions
     #[clap(long, default_value_t = false, action = clap::ArgAction::Set)]
     pub simple_triggers: bool,
+    /// Run why3 with the following configuration (Should start with "prove" or "ide")
+    #[clap(long)]
+    why3: Option<String>,
 }
 
 /// Parse a single key-value pair

creusot-rustc/src/options.rs

@@ -38,6 +38,9 @@ pub struct CreusotArgs {
     /// uses `result` as the trigger of definition and specification axioms of logic/ghost/predicate functions
     #[clap(long, default_value_t = false, action = clap::ArgAction::Set)]
     pub simple_triggers: bool,
+    /// Run why3 with the following configuration (Should start with "prove" or "ide")
+    #[clap(long)]
+    why3: Option<String>,
 }
 
 /// Parse a single key-value pair
@@ -97,6 +100,7 @@ impl CreusotArgs {
             span_mode: span_mode,
             match_str: self.focus_on,
             simple_triggers: self.simple_triggers,
+            why3_cmd: self.why3,
         }
     }
 }

creusot/Cargo.toml

@@ -15,6 +15,9 @@ toml = "0.5.8"
 why3 = { path = "../why3", features = ["serialize"] }
 clap = { version = "4.2", features = ["derive", "env"] }
 creusot-metadata = { path = "../creusot-metadata" }
+include_dir = "0.7.3"
+tempdir = "0.3.7"
+serde_json = { version = "1.0" }
 lazy_static = "1.4.0"
 
 [dev-dependencies]

creusot/src/backend.rs

@@ -247,8 +247,10 @@ impl<'tcx> Why3Generator<'tcx> {
         self.functions.get(&tid)
     }
 
-    pub(crate) fn modules(self) -> impl Iterator<Item = (TransId, TranslatedItem)> + 'tcx {
-        self.functions.into_iter()
+    pub(crate) fn modules(
+        self,
+    ) -> (impl Iterator<Item = (TransId, TranslatedItem)> + 'tcx, TranslationCtx<'tcx>) {
+        (self.functions.into_iter(), self.ctx)
     }
 
     pub(crate) fn start_group(&mut self, ids: IndexSet<DefId>) {

creusot/src/backend/optimization.rs

@@ -100,7 +100,7 @@ impl<'a, 'tcx> LocalUsage<'a, 'tcx> {
     fn visit_rvalue(&mut self, r: &fmir::RValue<'tcx>) {
         match r {
             fmir::RValue::Ghost(t) => self.visit_term(t),
-            fmir::RValue::Borrow(p) => {
+            fmir::RValue::Borrow(p, _) => {
                 self.read_place(p);
                 self.read_place(p)
             }
@@ -242,7 +242,7 @@ impl<'tcx> SimplePropagator<'tcx> {
             fmir::Terminator::Goto(_) => {}
             fmir::Terminator::Switch(e, _) => self.visit_expr(e),
             fmir::Terminator::Return => {}
-            fmir::Terminator::Abort => {}
+            fmir::Terminator::Abort(_) => {}
         }
     }
 
@@ -265,7 +265,7 @@ impl<'tcx> SimplePropagator<'tcx> {
     fn visit_rvalue(&mut self, r: &mut fmir::RValue<'tcx>) {
         match r {
             fmir::RValue::Ghost(t) => self.visit_term(t),
-            fmir::RValue::Borrow(p) => {
+            fmir::RValue::Borrow(p, _) => {
                 assert!(self.prop.get(&p.local).is_none(), "Trying to propagate borrowed variable")
             }
             fmir::RValue::Expr(e) => self.visit_expr(e),

creusot/src/backend/place.rs

@@ -6,7 +6,7 @@ use rustc_middle::{
     mir::{self, tcx::PlaceTy, ProjectionElem},
     ty::{self, Ty, TyCtxt, TyKind},
 };
-use rustc_span::Symbol;
+use rustc_span::{Span, Symbol};
 use why3::{
     exp::{
         Exp::{self, *},
@@ -38,6 +38,7 @@ pub(crate) fn create_assign_inner<'tcx>(
     locals: &LocalDecls<'tcx>,
     lhs: &fmir::Place<'tcx>,
     rhs: Exp,
+    span: Span,
 ) -> mlcfg::Statement {
     let inner = create_assign_rec(
         ctx,
@@ -50,7 +51,7 @@ pub(crate) fn create_assign_inner<'tcx>(
         rhs,
     );
 
-    Assign { lhs: Ident::build(lhs.local.as_str()), rhs: inner }
+    Assign { lhs: Ident::build(lhs.local.as_str()), rhs: inner, attr: ctx.span_attr(span) }
 }
 
 fn create_assign_rec<'tcx>(

creusot/src/backend/program.rs

@@ -248,7 +248,7 @@ fn lower_promoted<'tcx>(
         let exps: Vec<_> =
             bbd.stmts.into_iter().map(|s| s.to_why(ctx, names, &fmir.locals)).flatten().collect();
         exp = exps.into_iter().rfold(exp, |acc, asgn| match asgn {
-            why3::mlcfg::Statement::Assign { lhs, rhs } => {
+            why3::mlcfg::Statement::Assign { lhs, rhs, attr: _ } => {
                 Exp::Let { pattern: Pattern::VarP(lhs), arg: Box::new(rhs), body: Box::new(acc) }
             }
             why3::mlcfg::Statement::Assume(_) => acc,
@@ -547,7 +547,7 @@ impl<'tcx> Terminator<'tcx> {
                 }
             },
             Terminator::Return => {}
-            Terminator::Abort => {}
+            Terminator::Abort(_) => {}
         }
     }
 
@@ -556,6 +556,7 @@ impl<'tcx> Terminator<'tcx> {
         ctx: &mut Why3Generator<'tcx>,
         names: &mut CloneMap<'tcx>,
         locals: &LocalDecls<'tcx>,
+        statements: &mut Vec<mlcfg::Statement>,
     ) -> why3::mlcfg::Terminator {
         use why3::mlcfg::Terminator::*;
         match self {
@@ -565,7 +566,11 @@ impl<'tcx> Terminator<'tcx> {
                 branches.to_why(ctx, names, discr)
             }
             Terminator::Return => Return,
-            Terminator::Abort => Absurd,
+            Terminator::Abort(span) => {
+                let exp = ctx.attach_span(span, Exp::mk_false());
+                statements.push(mlcfg::Statement::Assert(exp));
+                Absurd
+            }
         }
     }
 }
@@ -635,10 +640,10 @@ impl<'tcx> Block<'tcx> {
         names: &mut CloneMap<'tcx>,
         locals: &LocalDecls<'tcx>,
     ) -> why3::mlcfg::Block {
-        mlcfg::Block {
-            statements: self.stmts.into_iter().flat_map(|s| s.to_why(ctx, names, locals)).collect(),
-            terminator: self.terminator.to_why(ctx, names, locals),
-        }
+        let mut statements =
+            self.stmts.into_iter().flat_map(|s| s.to_why(ctx, names, locals)).collect();
+        let terminator = self.terminator.to_why(ctx, names, locals, &mut statements);
+        mlcfg::Block { statements, terminator }
     }
 }
 
@@ -661,32 +666,42 @@ impl<'tcx> Statement<'tcx> {
         locals: &LocalDecls<'tcx>,
     ) -> Vec<mlcfg::Statement> {
         match self {
-            Statement::Assignment(lhs, RValue::Borrow(rhs)) => {
+            Statement::Assignment(lhs, RValue::Borrow(rhs, span)) => {
                 let borrow = Exp::Call(
                     Box::new(Exp::impure_qvar(QName::from_string("Borrow.borrow_mut").unwrap())),
                     vec![rhs.as_rplace(ctx, names, locals)],
                 );
                 let reassign = Exp::Final(Box::new(lhs.as_rplace(ctx, names, locals)));
 
                 vec![
-                    place::create_assign_inner(ctx, names, locals, &lhs, borrow),
-                    place::create_assign_inner(ctx, names, locals, &rhs, reassign),
+                    place::create_assign_inner(ctx, names, locals, &lhs, borrow, span),
+                    place::create_assign_inner(ctx, names, locals, &rhs, reassign, span),
                 ]
             }
             Statement::Assignment(lhs, RValue::Ghost(rhs)) => {
+                let span = rhs.span;
                 let ghost = lower_pure(ctx, names, rhs);
 
-                vec![place::create_assign_inner(ctx, names, locals, &lhs, ghost)]
+                vec![place::create_assign_inner(ctx, names, locals, &lhs, ghost, span)]
             }
             Statement::Assignment(lhs, RValue::Expr(rhs)) => {
                 let mut invalid = Vec::new();
                 rhs.invalidated_places(&mut invalid);
+                let span = rhs.span;
                 let rhs = rhs.to_why(ctx, names, locals);
-                let mut exps = vec![place::create_assign_inner(ctx, names, locals, &lhs, rhs)];
+                let mut exps =
+                    vec![place::create_assign_inner(ctx, names, locals, &lhs, rhs, span)];
                 for pl in invalid {
                     let ty = pl.ty(ctx.tcx, locals);
                     let ty = translate_ty(ctx, names, DUMMY_SP, ty);
-                    exps.push(place::create_assign_inner(ctx, names, locals, &pl, Exp::Any(ty)));
+                    exps.push(place::create_assign_inner(
+                        ctx,
+                        names,
+                        locals,
+                        &pl,
+                        Exp::Any(ty),
+                        DUMMY_SP,
+                    ));
                 }
                 exps
             }

creusot/src/ctx.rs

@@ -8,6 +8,7 @@ use crate::{
     error::{CrErr, CreusotResult, Error},
     metadata::{BinaryMetadata, Metadata},
     options::{Options, SpanMode},
+    run_why3::SpanMap,
     translation::{
         self,
         external::{extract_extern_specs_from_item, ExternSpec},
@@ -97,6 +98,7 @@ pub struct TranslationCtx<'tcx> {
     sig: HashMap<DefId, PreSignature<'tcx>>,
     bodies: HashMap<LocalDefId, BodyWithBorrowckFacts<'tcx>>,
     opacity: HashMap<DefId, Opacity>,
+    pub(crate) span_map: SpanMap,
 }
 
 #[derive(Copy, Clone)]
@@ -139,6 +141,7 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
             sig: Default::default(),
             bodies: Default::default(),
             opacity: Default::default(),
+            span_map: Default::default(),
         }
     }
 
@@ -386,7 +389,10 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
         }
     }
 
-    pub(crate) fn span_attr(&self, span: Span) -> Option<why3::declaration::Attribute> {
+    pub(crate) fn span_attr(&mut self, span: Span) -> Option<why3::declaration::Attribute> {
+        if let Some(span) = self.span_map.encode_span(&self.opts, span) {
+            return Some(span);
+        };
         let lo = self.sess.source_map().lookup_char_pos(span.lo());
         let hi = self.sess.source_map().lookup_char_pos(span.hi());
 
@@ -426,7 +432,7 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
         ))
     }
 
-    pub(crate) fn attach_span(&self, span: Span, exp: Exp) -> Exp {
+    pub(crate) fn attach_span(&mut self, span: Span, exp: Exp) -> Exp {
         if let Some(attr) = self.span_attr(span) {
             Exp::Attr(attr, Box::new(exp))
         } else {

creusot/src/lib.rs

@@ -5,6 +5,7 @@
 #[macro_use]
 extern crate log;
 extern crate rustc_ast;
+extern crate rustc_ast_pretty;
 extern crate rustc_borrowck;
 extern crate rustc_data_structures;
 extern crate rustc_driver;
@@ -48,5 +49,6 @@ use translation::*;
 mod error;
 pub(crate) mod lints;
 pub(crate) mod metadata;
+mod run_why3;
 mod translated_item;
 mod validate;

creusot/src/options.rs

@@ -21,6 +21,7 @@ pub struct Options {
     pub span_mode: SpanMode,
     pub match_str: Option<String>,
     pub simple_triggers: bool,
+    pub why3_cmd: Option<String>,
 }
 
 #[derive(Debug, Clone)]