Merge pull request #49 from AeneasVerif/son_fixes

Minor fixes

Makefile

@@ -36,20 +36,27 @@ generate-rust-toolchain-%:
 .PHONY: build
 build: build-charon-rust build-charon-ml
 
+.PHONY: build-debug
+build-debug: build-charon-rust-debug build-charon-ml
+
 .PHONY: build-charon-rust
-build-charon-rust: generate-rust-toolchain build-bin-dir
+build-charon-rust: generate-rust-toolchain
 	cd charon && $(MAKE)
+	mkdir -p bin
+	cp -f charon/target/release/charon bin
+	cp -f charon/target/release/charon-driver bin
+
+.PHONY: build-charon-rust-debug
+build-charon-rust-debug: generate-rust-toolchain
+	cd charon && cargo build
+	mkdir -p bin
+	cp -f charon/target/debug/charon bin
+	cp -f charon/target/debug/charon-driver bin
 
 .PHONY: build-charon-ml
 build-charon-ml:
 	cd charon-ml && $(MAKE)
 
-.PHONY: build-bin-dir
-build-bin-dir:
-	mkdir -p bin
-	cp -f charon/target/release/charon bin
-	cp -f charon/target/release/charon-driver bin
-
 # Build the tests crate, and run the cargo tests
 .PHONY: build-tests
 build-tests:

charon/src/assumed.rs

@@ -41,6 +41,7 @@ pub static OPTION_SOME_VARIANT_ID: types::VariantId::Id = types::VariantId::ONE;
 //
 pub static PANIC_NAME: [&str; 3] = ["core", "panicking", "panic"];
 pub static BEGIN_PANIC_NAME: [&str; 3] = ["std", "panicking", "begin_panic"];
+pub static ASSERT_FAILED_NAME: [&str; 3] = ["core", "panicking", "assert_failed"];
 
 // Boxes
 pub static BOX_NEW_NAME: [&str; 4] = ["alloc", "boxed", "Box", "new"];

charon/src/gast_utils.rs

@@ -360,8 +360,8 @@ impl<T> GFunDecl<T> {
             format!(" -> {}", ret_ty.fmt_with_ctx(ctx))
         };
 
-        // Clauses
-        let trait_clauses = fmt_where_clauses_with_ctx(
+        // Predicates
+        let preds = fmt_where_clauses_with_ctx(
             ctx,
             tab,
             &self.signature.parent_params_info,
@@ -373,7 +373,7 @@ impl<T> GFunDecl<T> {
         match &self.body {
             Option::None => {
                 // Put everything together
-                format!("{tab}{unsafe_kw}fn {name}{params}({args}){ret_ty}{trait_clauses}")
+                format!("{tab}{unsafe_kw}fn {name}{params}({args}){ret_ty}{preds}")
             }
             Option::Some(body) => {
                 // Body
@@ -382,7 +382,7 @@ impl<T> GFunDecl<T> {
 
                 // Put everything together
                 format!(
-                    "{tab}{unsafe_kw}fn {name}{params}({args}){ret_ty}{trait_clauses}\n{tab}{{\n{body}\n{tab}}}",
+                    "{tab}{unsafe_kw}fn {name}{params}({args}){ret_ty}{preds}\n{tab}{{\n{body}\n{tab}}}",
                 )
             }
         }

charon/src/meta_utils.rs

@@ -45,19 +45,24 @@ impl Loc {
 /// meta-information of, say, a sequence).
 pub fn combine_meta(m0: &Meta, m1: &Meta) -> Meta {
     // Merge the spans
-    assert!(m0.span.file_id == m1.span.file_id);
-    let span = Span {
-        file_id: m0.span.file_id,
-        beg: Loc::min(&m0.span.beg, &m1.span.beg),
-        end: Loc::max(&m0.span.end, &m1.span.end),
-    };
-
-    // We don't attempt to merge the "generated from" spans: they might
-    // come from different files, and even if they come from the same files
-    // they might come from different macros, etc.
-    Meta {
-        span,
-        generated_from_span: None,
+    if m0.span.file_id == m1.span.file_id {
+        let span = Span {
+            file_id: m0.span.file_id,
+            beg: Loc::min(&m0.span.beg, &m1.span.beg),
+            end: Loc::max(&m0.span.end, &m1.span.end),
+        };
+
+        // We don't attempt to merge the "generated from" spans: they might
+        // come from different files, and even if they come from the same files
+        // they might come from different macros, etc.
+        Meta {
+            span,
+            generated_from_span: None,
+        }
+    } else {
+        // It happens that the spans don't come from the same file. In this
+        // situation, we just return the first span. TODO: improve this.
+        *m0
     }
 }
 

charon/src/regions_hierarchy.rs

@@ -78,6 +78,7 @@ fn compute_sccs_from_lifetime_constraints(
     let all_rids: Vec<Region<RegionVarId::Id>> = all_var_regions
         .chain(Some(Region::Static).into_iter())
         .collect();
+    trace!("all_rids: {:?}\nregion_sccs: {:?}", all_rids, region_sccs);
     let sccs = reorder_sccs(get_region_parents, &all_rids, &region_sccs);
 
     // Debugging
@@ -503,6 +504,10 @@ fn compute_regions_constraints_for_type_decl_group(
             (*id, {
                 let mut graph = LifetimeConstraints::new();
                 graph.add_node(Region::Static);
+                let d = types.get(*id).unwrap();
+                d.generics.regions.iter().for_each(|id| {
+                    let _ = graph.add_node(Region::Var(id.index));
+                });
                 graph
             })
         }));
@@ -624,6 +629,19 @@ pub fn compute_regions_hierarchy_for_type_decl_group(
     types: &mut TypeDecls,
     decl: &TypeDeclarationGroup,
 ) {
+    // TODO: for now we don't properly handle mutually recursive groups of definitions
+    // which use lifetimes.
+    {
+        let ids = decl.get_ids();
+        assert!(
+            ids.len() == 1
+                || ids.iter().all(|id| {
+                    let d = types.get(*id).unwrap();
+                    d.generics.regions.is_empty()
+                })
+        );
+    }
+
     // Compute the constraints for every definition in the declaration group
     let constraints = compute_regions_constraints_for_type_decl_group(constraints_map, types, decl);
 
@@ -816,13 +834,13 @@ pub fn compute(ctx: &mut TransCtx, ordered_decls: &DeclarationsGroups) {
     // constraints map while doing so. We compute by working on a whole type
     // declaration group at a time.
     let mut types_constraints = TypesConstraintsMap::new();
-    let type_defs = &mut ctx.type_defs;
     for dgroup in ordered_decls {
+        trace!("{}", dgroup.fmt_with_ctx(ctx));
         match dgroup {
             DeclarationGroup::Type(decl) => {
                 compute_regions_hierarchy_for_type_decl_group(
                     &mut types_constraints,
-                    type_defs,
+                    &mut ctx.type_defs,
                     decl,
                 );
             }

charon/src/reorder_decls.rs

@@ -39,6 +39,36 @@ pub enum DeclarationGroup {
     TraitImpl(GDeclarationGroup<TraitImplId::Id>),
 }
 
+impl<Id: Copy> GDeclarationGroup<Id> {
+    pub fn get_ids(&self) -> Vec<Id> {
+        use GDeclarationGroup::*;
+        match self {
+            NonRec(id) => vec![*id],
+            Rec(ids) => ids.clone(),
+        }
+    }
+}
+
+impl<Id: Copy> GDeclarationGroup<Id> {
+    pub fn fmt_with_ctx<C>(&self, ctx: &C) -> String
+    where
+        C: crate::formatter::Formatter<Id>,
+    {
+        use GDeclarationGroup::*;
+        match self {
+            NonRec(id) => format!("Non rec: {}", ctx.format_object(*id)),
+            Rec(ids) => {
+                let ids = ids
+                    .iter()
+                    .map(|id| ctx.format_object(*id))
+                    .collect::<Vec<String>>()
+                    .join(", ");
+                format!("Rec: {}", ids)
+            }
+        }
+    }
+}
+
 impl DeclarationGroup {
     fn make_type_group(is_rec: bool, gr: impl Iterator<Item = TypeDeclId::Id>) -> Self {
         let gr: Vec<_> = gr.collect();
@@ -109,6 +139,24 @@ impl DeclarationGroup {
         );
         DeclarationGroup::TraitImpl(GDeclarationGroup::NonRec(gr[0]))
     }
+
+    pub fn fmt_with_ctx<C>(&self, ctx: &C) -> String
+    where
+        C: crate::formatter::Formatter<TypeDeclId::Id>
+            + crate::formatter::Formatter<FunDeclId::Id>
+            + crate::formatter::Formatter<GlobalDeclId::Id>
+            + crate::formatter::Formatter<TraitDeclId::Id>
+            + crate::formatter::Formatter<TraitImplId::Id>,
+    {
+        use DeclarationGroup::*;
+        match self {
+            Type(g) => format!("Type decls group: {}", g.fmt_with_ctx(ctx)),
+            Fun(g) => format!("Fun decls group: {}", g.fmt_with_ctx(ctx)),
+            Global(g) => format!("Global decls group: {}", g.fmt_with_ctx(ctx)),
+            TraitDecl(g) => format!("Trait decls group: {}", g.fmt_with_ctx(ctx)),
+            TraitImpl(g) => format!("Trait impls group: {}", g.fmt_with_ctx(ctx)),
+        }
+    }
 }
 
 #[derive(

charon/src/translate_functions_to_ullbc.rs

@@ -746,6 +746,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         // Check if this function is a actually `panic`
         if name.equals_ref_name(&assumed::PANIC_NAME)
             || name.equals_ref_name(&assumed::BEGIN_PANIC_NAME)
+            || name.equals_ref_name(&assumed::ASSERT_FAILED_NAME)
         {
             return SubstFunIdOrPanic::Panic;
         }
@@ -1274,7 +1275,9 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 Ok(RawTerminator::Panic)
             }
             SubstFunIdOrPanic::Fun(fid) => {
-                let next_block = target.unwrap();
+                let next_block = target.unwrap_or_else(|| {
+                    panic!("Expected a next block after the call to {:?}.\n\nSubsts: {:?}\n\nArgs: {:?}:", rust_id, substs, args)
+                });
 
                 // Translate the target
                 let lval = self.translate_place(destination);
@@ -1482,6 +1485,9 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             }
         }
 
+        // Sanity check
+        self.check_generics();
+
         // Add the late bound parameters (bound in the signature, can only be lifetimes)
         let signature: hax::MirPolyFnSig = signature.sinto(&self.hax_state);