Merge branch 'master' into update_toolchain_2023-06-25

Author: floriangru

creusot-contracts/src/logic/ops.rs

@@ -33,10 +33,9 @@ impl<T> IndexLogic<Int> for Ghost<Seq<T>> {
     type Item = T;
 
     #[logic]
-    #[trusted]
-    #[open(self)]
-    #[creusot::builtins = "seq.Seq.get"]
-    fn index_logic(self, _: Int) -> Self::Item {
-        absurd
+    #[open]
+    #[why3::attr = "inline:trivial"]
+    fn index_logic(self, ix: Int) -> Self::Item {
+        pearlite! { (*self)[ix] }
     }
 }

creusot-contracts/src/std/ops.rs

@@ -1,4 +1,7 @@
-use crate::{invariant::Invariant, *};
+use crate::{
+    invariant::{inv, Invariant},
+    *,
+};
 use ::std::marker::Tuple;
 pub use ::std::ops::*;
 
@@ -158,7 +161,9 @@ extern_spec! {
 
             trait FnMut<Args> where Self : FnMutExt<Args>, Args : Tuple {
                 #[requires((*self).precondition(arg))]
+                #[requires(inv(*self))]
                 #[ensures(self.postcondition_mut(arg, result))]
+                #[ensures(inv(^self))]
                 fn call_mut(&mut self, arg: Args) -> Self::Output;
             }
 

creusot/src/backend/ty.rs

@@ -372,7 +372,7 @@ fn build_ty_decl<'tcx>(
                 .fields
                 .iter()
                 .map(|f| {
-                    let ty = field_ty(ctx, names, param_env, f, substs);
+                    let ty = field_ty(ctx, names, param_env, did, f, substs);
                     Field { ty, ghost: false }
                 })
                 .collect();
@@ -410,14 +410,34 @@ fn field_ty<'tcx>(
     ctx: &mut Why3Generator<'tcx>,
     names: &mut CloneMap<'tcx>,
     param_env: ParamEnv<'tcx>,
+    adt_did: DefId,
     field: &FieldDef,
     substs: SubstsRef<'tcx>,
 ) -> MlT {
     let ty = field.ty(ctx.tcx, substs);
     let ty = ctx.try_normalize_erasing_regions(param_env, ty).unwrap_or(ty);
+
+    if !validate_field_ty(ctx, adt_did, ty) {
+        ctx.crash_and_error(ctx.def_span(field.did), "Illegal use of the Ghost type")
+    }
+
     translate_ty_inner(TyTranslation::Declaration, ctx, names, ctx.def_span(field.did), ty)
 }
 
+fn validate_field_ty<'tcx>(ctx: &mut Why3Generator<'tcx>, adt_did: DefId, ty: Ty<'tcx>) -> bool {
+    let tcx = ctx.tcx;
+    let bg = ctx.binding_group(adt_did);
+
+    !ty.walk().filter_map(ty::GenericArg::as_type).any(|ty| {
+        util::is_ghost_ty(tcx, ty)
+            && ty.walk().filter_map(ty::GenericArg::as_type).any(|ty| match ty.kind() {
+                TyKind::Adt(adt_def, _) => bg.contains(&adt_def.did()),
+                // TyKind::Param(_) => true,
+                _ => false,
+            })
+    })
+}
+
 pub(crate) fn translate_accessor(
     ctx: &mut Why3Generator<'_>,
     adt_did: DefId,
@@ -457,7 +477,8 @@ pub(crate) fn translate_accessor(
     let acc_name = format!("{}_{}", variant.name.as_str().to_ascii_lowercase(), field.name);
 
     let param_env = ctx.param_env(adt_did);
-    let target_ty = field_ty(ctx, &mut names, param_env, &variant.fields[ix.into()], substs);
+    let target_ty =
+        field_ty(ctx, &mut names, param_env, adt_did, &variant.fields[ix.into()], substs);
 
     let variant_arities: Vec<_> = adt_def
         .variants()

creusot/src/backend/ty_inv.rs

@@ -90,6 +90,7 @@ pub(crate) fn is_tyinv_trivial<'tcx>(
     tcx: TyCtxt<'tcx>,
     param_env: ParamEnv<'tcx>,
     ty: Ty<'tcx>,
+    default_trivial: bool,
 ) -> bool {
     if ty.is_closure() {
         return true;
@@ -99,7 +100,10 @@ pub(crate) fn is_tyinv_trivial<'tcx>(
     let mut visited_adts = IndexSet::new();
     let mut stack = vec![ty];
     while let Some(ty) = stack.pop() {
-        if resolve_user_inv(tcx, ty, param_env).is_some() {
+        if resolve_user_inv(tcx, ty, param_env).is_some()
+            // HACK we should never consider invariants of param types trivial 
+            || (!default_trivial && matches!(ty.kind(), TyKind::Param(_)))
+        {
             return false;
         }
 
@@ -187,7 +191,7 @@ fn build_inv_exp<'tcx>(
 ) -> Option<Exp> {
     let ty = ctx.tcx.normalize_erasing_regions(param_env, ty);
 
-    if mode == Mode::Field && is_tyinv_trivial(ctx.tcx, param_env, ty) {
+    if mode == Mode::Field && is_tyinv_trivial(ctx.tcx, param_env, ty, false) {
         return None;
     }
 

creusot/src/ctx.rs

@@ -210,7 +210,7 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
         let ty = self.try_normalize_erasing_regions(param_env, ty).ok()?;
 
         if util::is_open_ty_inv(self.tcx, def_id)
-            || ty_inv::is_tyinv_trivial(self.tcx, param_env, ty)
+            || ty_inv::is_tyinv_trivial(self.tcx, param_env, ty, true)
         {
             None
         } else {

creusot/src/translation/function.rs

@@ -285,7 +285,9 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> {
     fn resolve_locals(&mut self, mut locals: BitSet<Local>) {
         locals.subtract(&self.erased_locals.to_hybrid());
 
-        for local in locals.iter() {
+        // TODO determine resolution order based on outlives relation
+        let locals = locals.iter().collect::<Vec<_>>();
+        for local in locals.into_iter().rev() {
             self.emit_resolve(local.into());
         }
     }

creusot/src/util.rs

@@ -75,6 +75,15 @@ pub(crate) fn is_ghost_closure<'tcx>(tcx: TyCtxt<'tcx>, ty: Ty<'tcx>) -> Option<
     } else { None }
 }
 
+pub(crate) fn is_ghost_ty<'tcx>(tcx: TyCtxt<'tcx>, ty: Ty<'tcx>) -> bool {
+    let r: Option<bool> = try {
+        let adt = ty.ty_adt_def()?;
+        let builtin = get_builtin(tcx, adt.did())?;
+        builtin.as_str() == "prelude.Ghost.ghost_ty"
+    };
+    r.unwrap_or(false)
+}
+
 pub(crate) fn is_spec_logic(tcx: TyCtxt, def_id: DefId) -> bool {
     get_attr(tcx.get_attrs_unchecked(def_id), &["creusot", "decl", "spec_logic"]).is_some()
 }

creusot/tests/should_fail/bug/436.rs renamed to creusot/tests/should_fail/bug/436_0.rs

@@ -1,5 +1,5 @@
 error[creusot]: called Logic function in Ghost context "creusot_contracts::__stubs::fin"
-  --> 436.rs:10:5
+  --> 436_0.rs:10:5
    |
 10 |     pearlite! { *(^x).g }
    |     ^^^^^^^^^^^^^^^^^^^^^