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

@@ -1,7 +1,7 @@
 use indexmap::{IndexMap, IndexSet};
 use rustc_hir::{def::DefKind, def_id::DefId};
 use rustc_middle::ty::{AliasTy, GenericParamDef, GenericParamDefKind, TyCtxt};
-use rustc_span::DUMMY_SP;
+use rustc_span::{RealFileName, Span, DUMMY_SP};
 use why3::declaration::{Decl, TyDecl};
 
 use crate::{
@@ -15,7 +15,9 @@ use std::{
     ops::{Deref, DerefMut},
 };
 
+use crate::{options::SpanMode, run_why3::SpanMap};
 pub(crate) use clone_map::*;
+use why3::Exp;
 
 use self::{
     dependency::{Dependency, HackedId},
@@ -56,6 +58,7 @@ pub struct Why3Generator<'tcx> {
     functions: IndexMap<TransId, TranslatedItem>,
     translated_items: IndexSet<TransId>,
     in_translation: Vec<IndexSet<TransId>>,
+    pub(crate) span_map: SpanMap,
 }
 
 impl<'tcx> Deref for Why3Generator<'tcx> {
@@ -81,6 +84,7 @@ impl<'tcx> Why3Generator<'tcx> {
             functions: Default::default(),
             translated_items: Default::default(),
             in_translation: Default::default(),
+            span_map: Default::default(),
         }
     }
 
@@ -270,8 +274,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<'a>(
+        &'a mut self,
+    ) -> impl Iterator<Item = (TransId, TranslatedItem)> + 'a {
+        self.functions.drain(..)
     }
 
     pub(crate) fn start_group(&mut self, ids: IndexSet<DefId>) {
@@ -345,6 +351,60 @@ impl<'tcx> Why3Generator<'tcx> {
             _ => false,
         }
     }
+
+    pub(crate) fn span_attr(&mut self, span: Span) -> Option<why3::declaration::Attribute> {
+        if span.is_dummy() {
+            return None;
+        }
+        if let Some(span) = self.span_map.encode_span(&self.ctx.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());
+
+        let rustc_span::FileName::Real(path) = &lo.file.name else { return None };
+
+        // If we ask for relative paths and the paths comes from the standard library, then we prefer returning
+        // None, since the relative path of the stdlib is not stable.
+        let path = match (&self.opts.span_mode, path) {
+            (SpanMode::Relative, RealFileName::Remapped { .. }) => return None,
+            _ => path.local_path_if_available(),
+        };
+
+        let mut buf;
+        let path = if path.is_relative() {
+            buf = std::env::current_dir().unwrap();
+            buf.push(path);
+            buf.as_path()
+        } else {
+            path
+        };
+
+        let filename = match self.opts.span_mode {
+            SpanMode::Absolute => path.to_string_lossy().into_owned(),
+            SpanMode::Relative => {
+                // Why3 treats the spans as relative to the session not the source file??
+                format!("{}", self.opts.relative_to_output(&path).to_string_lossy())
+            }
+            _ => return None,
+        };
+
+        Some(why3::declaration::Attribute::Span(
+            filename,
+            lo.line,
+            lo.col_display,
+            hi.line,
+            hi.col_display,
+        ))
+    }
+
+    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 {
+            exp
+        }
+    }
 }
 
 // Closures inherit the generic parameters of the original function they were defined in, but

creusot/src/backend/optimization.rs

@@ -77,7 +77,7 @@ impl<'a, 'tcx> LocalUsage<'a, 'tcx> {
 
     fn visit_statement(&mut self, b: &fmir::Statement<'tcx>) {
         match b {
-            fmir::Statement::Assignment(p, r) => {
+            fmir::Statement::Assignment(p, r, _) => {
                 self.write_place(p);
                 self.visit_rvalue(r)
             }
@@ -218,13 +218,13 @@ impl<'tcx> SimplePropagator<'tcx> {
         for mut s in std::mem::take(&mut b.stmts) {
             self.visit_statement(&mut s);
             match s {
-                fmir::Statement::Assignment(l, fmir::RValue::Expr(r))
+                fmir::Statement::Assignment(l, fmir::RValue::Expr(r), _)
                     // we do not propagate calls to avoid moving them after the resolve of their arguments
                     if self.should_propagate(l.local) && !self.usage[&l.local].used_in_pure_ctx && !r.is_call() => {
                       self.prop.insert(l.local, r);
                       self.dead.insert(l.local);
                     }
-                fmir::Statement::Assignment(ref l, fmir::RValue::Expr(ref r)) if self.should_erase(l.local)  && !r.is_call() && r.is_pure() => {
+                fmir::Statement::Assignment(ref l, fmir::RValue::Expr(ref r), _) if self.should_erase(l.local)  && !r.is_call() && r.is_pure() => {
                       self.dead.insert(l.local);
                 }
                 fmir::Statement::Resolve(_,_, ref p) => {
@@ -242,13 +242,13 @@ impl<'tcx> SimplePropagator<'tcx> {
             fmir::Terminator::Goto(_) => {}
             fmir::Terminator::Switch(e, _) => self.visit_expr(e),
             fmir::Terminator::Return => {}
-            fmir::Terminator::Abort => {}
+            fmir::Terminator::Abort(_) => {}
         }
     }
 
     fn visit_statement(&mut self, s: &mut fmir::Statement<'tcx>) {
         match s {
-            fmir::Statement::Assignment(_, r) => self.visit_rvalue(r),
+            fmir::Statement::Assignment(_, r, _) => self.visit_rvalue(r),
             fmir::Statement::Resolve(_, _, p) => {
               if let Some(l) = p.as_symbol() && self.dead.contains(&l) {