Merge pull request #826 from xldenis/tyinv-gen-param-min

Do not consider generic fields to have trivial invariants

Author: voidc

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_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/tests/should_fail/bug/692.mlcfg

@@ -417,9 +417,11 @@ end
 module Core_Ops_Range_Range_Type_Inv
   type idx
   use Core_Ops_Range_Range_Type as Core_Ops_Range_Range_Type
+  clone CreusotContracts_Invariant_Inv_Stub as Inv1 with
+    type t = idx
   clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
     type t = Core_Ops_Range_Range_Type.t_range idx
-  axiom inv_t_range : forall self : Core_Ops_Range_Range_Type.t_range idx . Inv0.inv self = true
+  axiom inv_t_range [@rewrite] : forall self : Core_Ops_Range_Range_Type.t_range idx . Inv0.inv self = (Inv1.inv (Core_Ops_Range_Range_Type.range_start self) /\ Inv1.inv (Core_Ops_Range_Range_Type.range_end self))
 end
 module CreusotContracts_Std1_Iter_Iterator_Completed_Stub
   type self
@@ -997,6 +999,12 @@ module CreusotContracts_Std1_Slice_Impl5_ResolveElswhere
     ensures { result = resolve_elswhere self old' fin }
 
 end
+module TyInv_Trivial
+  type t
+  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
+    type t = t
+  axiom inv_trivial : forall self : t . Inv0.inv self = true
+end
 module C100doors_F_Interface
   val f [#"../100doors.rs" 18 0 18 10] (_1 : ()) : ()
 end
@@ -1006,6 +1014,12 @@ module C100doors_F
   use prelude.Ghost
   use seq.Seq
   use prelude.Borrow
+  clone CreusotContracts_Invariant_Inv_Interface as Inv1 with
+    type t = usize
+  clone TyInv_Trivial as TyInv_Trivial0 with
+    type t = usize,
+    predicate Inv0.inv = Inv1.inv,
+    axiom .
   clone CreusotContracts_Std1_Slice_Impl5_ResolveElswhere as ResolveElswhere0 with
     type t = bool
   use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
@@ -1056,6 +1070,7 @@ module C100doors_F
   clone Core_Ops_Range_Range_Type_Inv as Core_Ops_Range_Range_Type_Inv0 with
     type idx = usize,
     predicate Inv0.inv = Inv0.inv,
+    predicate Inv1.inv = Inv1.inv,
     axiom .
   clone CreusotContracts_Std1_Iter_Impl0_IntoIterPost as IntoIterPost0 with
     type i = Core_Ops_Range_Range_Type.t_range usize

creusot/tests/should_fail/bug/695.mlcfg

@@ -7,7 +7,7 @@
 <path name=".."/><path name="100doors.mlcfg"/>
 <theory name="C100doors_F" proved="true">
  <goal name="f&#39;vc" expl="VC for f" proved="true">
- <proof prover="1"><result status="valid" time="0.220000" steps="45466"/></proof>
+ <proof prover="1"><result status="valid" time="0.220000" steps="49042"/></proof>
  </goal>
 </theory>
 </file>