Merge pull request #968 from creusot-rs/coma

Coma backend

.gitignore

@@ -13,10 +13,16 @@ _opam
 *.cmeta
 
 # Why3 Files
-/*.mlcfg
+/*.coma
 *.bak
 *~
 
 # macOS
 
 .DS_Store
+
+_opam/
+
+# failed tests
+
+why3tests/failed

.vscode/tasks.json

@@ -4,9 +4,9 @@
     "version": "2.0.0",
     "tasks": [
         {
-            "label": "Build MLCFG",
+            "label": "Build coma",
             "dependsOn": [
-                "Generate MLCFG",
+                "Generate coma",
                 "Reload Session"
             ],
             "dependsOrder": "sequence",
@@ -17,9 +17,9 @@
             }
         },
         {
-            "label": "Generate MLCFG",
+            "label": "Generate coma",
             "type": "shell",
-            "command": "./mlcfg ${file}",
+            "command": "./coma ${file}",
             "group": {
                 "kind": "build"
             },
@@ -28,7 +28,7 @@
             },
             "options": {
                 "env": {
-                    "OUTPUT_FILE": "${relativeFileDirname}/${fileBasenameNoExtension}.mlcfg"
+                    "OUTPUT_FILE": "${relativeFileDirname}/${fileBasenameNoExtension}.coma"
                 }
             }
         },

ARCHITECTURE.md

@@ -84,7 +84,7 @@ The binaries are structured following the pattern laid out by [flowistry](https:
 
 ## Program functions
 
-Each function is translated as a standalone Why module containing a single MLCFG function.
+Each function is translated as a standalone Why module containing a single coma function.
 We translate program functions from the *MIR* of a program, as we need to ensure that borrow checking succeeds and also use dataflow analysis on the MIR body.
 
 ### Encoding contracts
@@ -118,7 +118,7 @@ The section on compiling specifications will cover how this works
 
 ### Translating functions
 
-The translation of program functions occurs statement-by-statement from the MIR to MLCFG.
+The translation of program functions occurs statement-by-statement from the MIR to coma.
 Most MIR statements have an obvious translation, but there are a few key technicalities.
 
 #### Translating Places

CONTRIBUTING.md

@@ -20,11 +20,11 @@ The warnings and errors of each test are recorded in an accompanying `stderr` fi
 
 # 4. Verifying proofs
 
-Once you are satisfied with the MLCFG output, you can validate the proofs of Creusot by running `cargo test --test why3`. This will run each test in the UI suite, and if a Why3 session is found, execute the proofs within.
+Once you are satisfied with the coma output, you can validate the proofs of Creusot by running `cargo test --test why3`. This will run each test in the UI suite, and if a Why3 session is found, execute the proofs within.
 If you add a test that you believe should include a proof, you can add it using the `./ide` script provided in Creusot.
 Load your test case in the Why3 IDE, solve the proof and save the result, it will now be checked as part of CI.
 
-Because verifying the proofs can be tedious during development the `cargo test --test why3` command accepts two flags: `--diff-from=` which accepts a Git ref and only checks the MLCFG files that have changed since then, and `--replay=` which accepts one of three values: `none`, `obsolete`, `all` and guides which proofs should actually be run or only just typecheked.
+Because verifying the proofs can be tedious during development the `cargo test --test why3` command accepts two flags: `--diff-from=` which accepts a Git ref and only checks the coma files that have changed since then, and `--replay=` which accepts one of three values: `none`, `obsolete`, `all` and guides which proofs should actually be run or only just typecheked.
 
 Helpful cheatsheet:
 - `cargo test --test why3 -- --diff-from=master --replay=none`: only typecheck the test cases that have changed

HACKING.md

@@ -22,7 +22,7 @@ To avoid first installing the `cargo-creusot` binary before running `cargo
 
 ## Running the testsuite
 
-- Test the output of creusot (mlcfg files) against reference files:
+- Test the output of creusot (coma files) against reference files:
 ```
 cargo test --test ui
 ```

cargo-creusot/src/helpers.rs

@@ -23,29 +23,29 @@ pub(crate) fn make_cargo_metadata() -> Result<cargo_metadata::Metadata> {
 
 fn select_root_crate(m: &cargo_metadata::Metadata) -> Result<&Package> {
     if m.workspace_default_members.is_empty() {
-        return Err(anyhow!("can't create mlcfg file, no default workspace"));
+        return Err(anyhow!("can't create coma file, no default workspace"));
     }
 
     // cargo metadata doesn't specify one particular crate.
     // We consider that the first crate in the list of workspace_default_members will give the name of the file
     let crate_id = &m.workspace_default_members[0];
     let Some(package) = m.packages.iter().find(|p| &p.id == crate_id) else {
-        return Err(anyhow!("can't create mlcfg file, no default package"));
+        return Err(anyhow!("can't create coma file, no default package"));
     };
 
     Ok(package)
 }
 
-pub(crate) fn make_mlcfg_filename(m: &cargo_metadata::Metadata) -> Result<PathBuf> {
+pub(crate) fn make_coma_filename(m: &cargo_metadata::Metadata) -> Result<PathBuf> {
     let root_crate = select_root_crate(m)?;
 
     // to specify the crate kind in the file name: lib, bin
     if root_crate.targets.is_empty() || root_crate.targets[0].kind.is_empty() {
-        return Err(anyhow!("can't create mlcfg file, default package without target"));
+        return Err(anyhow!("can't create coma file, default package without target"));
     }
 
     let crate_type = &root_crate.targets[0].kind[0];
-    let filename = format!("{}-{}.mlcfg", root_crate.name, crate_type);
+    let filename = format!("{}-{}.coma", root_crate.name, crate_type);
 
     // put the file at the root of the target directory
     Ok(m.target_directory.join(filename).into())

cargo-creusot/src/main.rs

@@ -22,16 +22,16 @@ use Subcommand::*;
 
 fn main() -> Result<()> {
     let cargo_md = make_cargo_metadata()?;
-    let mlcfg_filename: PathBuf; //  mlcfg output file name container
+    let coma_filename: PathBuf; //  coma output file name container
 
     let mut cargs = CargoCreusotArgs::parse_from(std::env::args().skip(1));
 
-    // select mlcfg output file name
+    // select coma output file name
     if let Some(f) = &cargs.options.output_file {
-        mlcfg_filename = f.into();
+        coma_filename = f.into();
     } else {
-        mlcfg_filename = make_mlcfg_filename(&cargo_md)?;
-        cargs.options.output_file = Some(mlcfg_filename.to_string_lossy().into_owned());
+        coma_filename = make_coma_filename(&cargo_md)?;
+        cargs.options.output_file = Some(coma_filename.to_string_lossy().into_owned());
     }
 
     let subcommand = match cargs.subcommand {
@@ -71,7 +71,7 @@ fn main() -> Result<()> {
                 let mut b = Why3LauncherBuilder::new();
                 b.why3_path(config_args.why3_path);
                 b.config_file(config_args.why3_config);
-                b.output_file(mlcfg_filename);
+                b.output_file(coma_filename);
                 // temporary: for the moment we only launch why3 via cargo-creusot in Ide mode
                 b.mode(Why3Mode::Ide);
                 if let Some(subcmd) = &creusot_rustc_subcmd {

cargo-creusot/src/why3_launcher.rs

@@ -116,10 +116,10 @@ impl Why3LauncherBuilder {
     }
 
     pub fn build(self) -> Result<Why3Launcher> {
-        let Some(mlcfg_file) = self.output_file else {
-            return Err(anyhow!("can't launch why3, no mlcfg_file specify"));
+        let Some(coma_file) = self.output_file else {
+            return Err(anyhow!("can't launch why3, no coma_file specify"));
         };
 
-        Ok(Why3Launcher::new(self.mode, self.why3_path, self.config_file, self.args, mlcfg_file))
+        Ok(Why3Launcher::new(self.mode, self.why3_path, self.config_file, self.args, coma_file))
     }
 }

creusot-deps.opam

@@ -4,8 +4,8 @@ opam-version: "2.0"
 maintainer: "Armaël Guéneau <[email protected]>"
 authors: "the creusot authors"
 depends: [
-  "why3" {= "git-91b3"}
-  "why3-ide" {= "git-91b3" & !?in-creusot-ci}
+  "why3" {= "git-39f7"}
+  "why3-ide" {= "git-39f7" & !?in-creusot-ci}
 # optional dependencies of why3
   "ocamlgraph"
   "camlzip"
@@ -16,6 +16,6 @@ depends: [
 # When updating the hash and git-XXX below, don't forget to update them in the
 # depends: field above!
 pin-depends: [
-  [ "why3.git-91b3" "git+https://gitlab.inria.fr/why3/why3.git#91b314fb2" ]
-  [ "why3-ide.git-91b3" "git+https://gitlab.inria.fr/why3/why3.git#91b314fb2" ]
+  [ "why3.git-39f7" "git+https://gitlab.inria.fr/why3/why3.git#39f7bcf37" ]
+  [ "why3-ide.git-39f7" "git+https://gitlab.inria.fr/why3/why3.git#39f7bcf37" ]
 ]

creusot/src/backend.rs

@@ -37,6 +37,7 @@ pub(crate) mod term;
 pub(crate) mod traits;
 pub(crate) mod ty;
 pub(crate) mod ty_inv;
+mod wto;
 
 #[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
 pub(crate) enum TransId {
@@ -179,7 +180,10 @@ impl<'tcx> Why3Generator<'tcx> {
                         .insert(repr, TranslatedItem::Type { modl, accessors: Default::default() });
                 }
             }
-            ItemType::Field => self.translate_accessor(def_id),
+            ItemType::Field => unreachable!(),
+            ItemType::Variant => {
+                self.translate(self.ctx.parent(def_id));
+            }
             ItemType::Unsupported(dk) => self.crash_and_error(
                 self.tcx.def_span(def_id),
                 &format!("unsupported definition kind {:?} {:?}", def_id, dk),
@@ -387,7 +391,7 @@ impl<'tcx> Why3Generator<'tcx> {
                 let path = to_absolute(path);
                 let base = to_absolute(base);
                 // Why3 treats the spans as relative to the session, not the source file,
-                // and the session is in a subdirectory next to the mlcfg file, so we need
+                // and the session is in a subdirectory next to the coma file, so we need
                 // to add an extra ".."
                 let p = std::path::PathBuf::from("..");
                 let diff = pathdiff::diff_paths(&path, &base)?;

creusot/src/backend/clone_map.rs

@@ -56,10 +56,11 @@ pub enum PreludeModule {
     Ref,
     Seq,
     Type,
+    Intrinsic,
 }
 
 impl PreludeModule {
-    fn qname(&self) -> QName {
+    pub fn qname(&self) -> QName {
         match self {
             PreludeModule::Float32 => QName::from_string("prelude.Float32").unwrap(),
             PreludeModule::Float64 => QName::from_string("prelude.Float64").unwrap(),
@@ -84,6 +85,7 @@ impl PreludeModule {
             PreludeModule::Bool => QName::from_string("prelude.Bool").unwrap(),
             PreludeModule::Borrow => QName::from_string("prelude.Borrow").unwrap(),
             PreludeModule::Slice => QName::from_string("prelude.Slice").unwrap(),
+            PreludeModule::Intrinsic => QName::from_string("prelude.Intrinsic").unwrap(),
         }
     }
 }
@@ -112,7 +114,13 @@ pub(crate) trait Namer<'tcx> {
         ix: FieldIdx,
     ) -> QName;
 
-    fn normalize(&self, ctx: &TranslationCtx<'tcx>, ty: Ty<'tcx>) -> Ty<'tcx>;
+    fn eliminator(&mut self, def_id: DefId, subst: GenericArgsRef<'tcx>) -> QName;
+
+    fn normalize<T: TypeFoldable<TyCtxt<'tcx>> + Copy>(
+        &self,
+        ctx: &TranslationCtx<'tcx>,
+        ty: T,
+    ) -> T;
 
     fn import_prelude_module(&mut self, _: PreludeModule);
 
@@ -191,14 +199,43 @@ impl<'tcx> Namer<'tcx> for Dependencies<'tcx> {
         }
     }
 
+    fn eliminator(&mut self, def_id: DefId, subst: GenericArgsRef<'tcx>) -> QName {
+        let tcx = self.tcx;
+
+        match tcx.def_kind(def_id) {
+            DefKind::Variant => {
+                let clone = self.insert(DepNode::new(tcx, (tcx.parent(def_id), subst)));
+
+                let mut qname = clone.qname();
+                // TODO(xavier): Remove this hack
+                qname.name = DepNode::new(tcx, (def_id, subst)).base_ident(tcx).to_string().into();
+                qname
+            }
+            DefKind::Closure | DefKind::Struct | DefKind::Union => {
+                let mut node = DepNode::new(self.tcx, (def_id, subst));
+
+                if self.tcx.is_closure_like(def_id) {
+                    node = DepNode::Type(Ty::new_closure(self.tcx, def_id, subst));
+                }
+
+                self.insert(node).qname()
+            }
+            _ => unreachable!(),
+        }
+    }
+
     fn ty_inv(&mut self, ty: Ty<'tcx>) -> QName {
         let def_id =
             self.tcx.get_diagnostic_item(Symbol::intern("creusot_invariant_internal")).unwrap();
         let subst = self.tcx.mk_args(&[ty::GenericArg::from(ty)]);
         self.value(def_id, subst)
     }
 
-    fn normalize(&self, ctx: &TranslationCtx<'tcx>, ty: Ty<'tcx>) -> Ty<'tcx> {
+    fn normalize<T: TypeFoldable<TyCtxt<'tcx>> + Copy>(
+        &self,
+        ctx: &TranslationCtx<'tcx>,
+        ty: T,
+    ) -> T {
         self.tcx.try_normalize_erasing_regions(self.param_env(ctx), ty).unwrap_or(ty)
     }
 
@@ -239,7 +276,7 @@ pub struct Dependencies<'tcx> {
 }
 
 #[derive(Default, Clone)]
-struct NameSupply {
+pub(crate) struct NameSupply {
     name_counts: IndexMap<Symbol, usize>,
 }
 
@@ -301,6 +338,12 @@ impl<'tcx> CloneNames<'tcx> {
 
                 return kind;
             }
+            DepNode::Item(id, _) if util::item_type(self.tcx, id) == ItemType::Variant => {
+                let ty = self.tcx.parent(id);
+                let modl = module_name(self.tcx, ty);
+
+                Kind::Used(modl, key.base_ident(self.tcx))
+            }
             _ => {
                 if let DepNode::Item(id, _) = key
                     && let Some(why3_modl) = util::get_builtin(self.tcx, id)
@@ -320,9 +363,9 @@ impl<'tcx> CloneNames<'tcx> {
 }
 
 impl NameSupply {
-    fn freshen(&mut self, sym: Symbol) -> Symbol {
+    pub(crate) fn freshen(&mut self, sym: Symbol) -> Symbol {
         let count: usize = *self.name_counts.entry(sym).and_modify(|c| *c += 1).or_insert(0);
-        Symbol::intern(&format!("{sym}{count}"))
+        Symbol::intern(&format!("{sym}'{count}"))
     }
 }
 
@@ -381,7 +424,7 @@ impl<'tcx> DepGraph<'tcx> {
 
 // TODO: Get rid of the enum
 #[derive(Clone, Copy, Debug, PartialEq, Eq, TyEncodable, TyDecodable, Hash)]
-enum Kind {
+pub enum Kind {
     /// This symbol is locally defined
     Named(Symbol),
     /// This symbol must be acompanied by a `Use` statement in Why3