Change the algorithm in validate_terminates

creusot/src/translation/traits.rs

@@ -304,6 +304,29 @@ impl<'tcx> TraitResolved<'tcx> {
         }
     }
 
+    /// Given a trait and some type parameters, try to find a concrete `impl` block for
+    /// this trait.
+    pub(crate) fn impl_id_of_trait(
+        tcx: TyCtxt<'tcx>,
+        param_env: ParamEnv<'tcx>,
+        trait_def_id: DefId,
+        substs: GenericArgsRef<'tcx>,
+    ) -> Option<DefId> {
+        let trait_ref = TraitRef::from_method(tcx, trait_def_id, substs);
+        let trait_ref = tcx.normalize_erasing_regions(param_env, trait_ref);
+
+        let Ok(source) = tcx.codegen_select_candidate((param_env, trait_ref)) else {
+            return None;
+        };
+        trace!("resolve_assoc_item_opt {source:?}",);
+        match source {
+            ImplSource::UserDefined(impl_data) => Some(impl_data.impl_def_id),
+            ImplSource::Param(_) => None,
+            // TODO: should we return something here, like we do in the above method?
+            ImplSource::Builtin(_, _) => None,
+        }
+    }
+
     pub fn to_opt(
         self,
         did: DefId,

creusot/tests/should_fail/cycle.stderr

@@ -1,19 +1,19 @@
-error: Mutually recursive functions: when calling `g`...
-  --> cycle.rs:12:1
+error: Mutually recursive functions: when calling `f`...
+  --> cycle.rs:6:1
    |
-12 | pub fn g(x: bool) {
-   | ^^^^^^^^^^^^^^^^^
+6  | pub fn f() {
+   | ^^^^^^^^^^
    |
-note: then `g` calls `f`...
-  --> cycle.rs:14:9
-   |
-14 |         f();
-   |         ^^^
-note: finally `f` calls `g`.
+note: then `f` calls `g`...
   --> cycle.rs:7:5
    |
 7  |     g(true);
    |     ^^^^^^^
+note: finally `g` calls `f`.
+  --> cycle.rs:14:9
+   |
+14 |         f();
+   |         ^^^
 
 error: aborting due to 1 previous error
 

creusot/tests/should_fail/ghost/non_terminating.stderr

@@ -27,22 +27,22 @@ note: looping occurs here
    |         ^^^^^^^
    = note: this error originates in the macro `ghost` (in Nightly builds, run with -Z macro-backtrace for more info)
 
-error: Mutually recursive functions: when calling `f`...
-  --> non_terminating.rs:13:1
+error: Mutually recursive functions: when calling `recursive`...
+  --> non_terminating.rs:5:1
    |
-13 | fn f() {
-   | ^^^^^^
+5  | pub fn recursive() {
+   | ^^^^^^^^^^^^^^^^^^
    |
-note: then `f` calls `recursive`...
-  --> non_terminating.rs:14:5
-   |
-14 |     recursive();
-   |     ^^^^^^^^^^^
-note: finally `recursive` calls `f`.
+note: then `recursive` calls `f`...
   --> non_terminating.rs:7:9
    |
 7  |         f();
    |         ^^^
+note: finally `f` calls `recursive`.
+  --> non_terminating.rs:14:5
+   |
+14 |     recursive();
+   |     ^^^^^^^^^^^
 
 error: aborting due to 2 previous errors; 1 warning emitted
 

creusot/tests/should_fail/terminates/complicated_traits_recursion.stderr

@@ -1,18 +1,10 @@
-error: Mutually recursive functions: when calling `bar`...
-  --> complicated_traits_recursion.rs:18:1
+error: Mutually recursive functions: when calling `<i32 as Foo>::foo`...
+  --> complicated_traits_recursion.rs:12:5
    |
-18 | / fn bar<I>(_: I)
-19 | | where
-20 | |     I: Iterator,
-21 | |     I::Item: Foo,
-   | |_________________^
+12 |     fn foo() {
+   |     ^^^^^^^^
    |
-note: then `bar` calls `<i32 as Foo>::foo`...
-  --> complicated_traits_recursion.rs:23:5
-   |
-23 |     I::Item::foo()
-   |     ^^^^^^^^^^^^^^
-note: finally `<i32 as Foo>::foo` calls `bar`.
+note: then `<i32 as Foo>::foo` might call `<i32 as Foo>::foo` via the call to `bar`.
   --> complicated_traits_recursion.rs:13:9
    |
 13 |         bar::<std::iter::Once<i32>>(std::iter::once(1i32));

creusot/tests/should_fail/terminates/mutual_recursion.stderr

@@ -1,24 +1,24 @@
-error: Mutually recursive functions: when calling `f3`...
-  --> mutual_recursion.rs:18:1
+error: Mutually recursive functions: when calling `m::f1`...
+  --> mutual_recursion.rs:7:5
    |
-18 | fn f3() {
-   | ^^^^^^^
+7  |     pub fn f1() {
+   |     ^^^^^^^^^^^
    |
-note: then `f3` calls `m::f1`...
-  --> mutual_recursion.rs:19:5
-   |
-19 |     m::f1();
-   |     ^^^^^^^
 note: then `m::f1` calls `f2`...
   --> mutual_recursion.rs:8:9
    |
 8  |         super::f2();
    |         ^^^^^^^^^^^
-note: finally `f2` calls `f3`.
+note: then `f2` calls `f3`...
   --> mutual_recursion.rs:14:5
    |
 14 |     f3();
    |     ^^^^
+note: finally `f3` calls `m::f1`.
+  --> mutual_recursion.rs:19:5
+   |
+19 |     m::f1();
+   |     ^^^^^^^
 
 error: aborting due to 1 previous error
 

creusot/tests/should_fail/terminates/mutual_recursion_trait.stderr

@@ -4,7 +4,7 @@ error: Mutually recursive functions: when calling `bar`...
 18 | fn bar() {
    | ^^^^^^^^
    |
-note: then `bar` calls `<i32 as Foo>::foo`...
+note: then `bar` might call `<i32 as Foo>::foo` via the call to `Foo::foo`...
   --> mutual_recursion_trait.rs:19:5
    |
 19 |     <i32 as Foo>::foo();

creusot/tests/should_fail/terminates/recursion_through_contract.stderr

@@ -1,36 +1,36 @@
-error: Mutually recursive functions: when calling `f2`...
-  --> recursion_through_contract.rs:23:1
+error: Mutually recursive functions: when calling `with_requires`...
+  --> recursion_through_contract.rs:20:1
    |
-23 | fn f2() -> Int {
-   | ^^^^^^^^^^^^^^
+20 | fn with_requires(x: Int) {}
+   | ^^^^^^^^^^^^^^^^^^^^^^^^
    |
-note: then `f2` calls `with_requires`...
-  --> recursion_through_contract.rs:24:5
-   |
-24 |     with_requires(5);
-   |     ^^^^^^^^^^^^^^^^
-note: finally `with_requires` calls `f2`.
+note: then `with_requires` calls `f2`...
   --> recursion_through_contract.rs:19:17
    |
 19 | #[requires(x == f2())]
    |                 ^^^^
-
-error: Mutually recursive functions: when calling `f1`...
-  --> recursion_through_contract.rs:13:1
+note: finally `f2` calls `with_requires`.
+  --> recursion_through_contract.rs:24:5
    |
-13 | fn f1() -> Int {
-   | ^^^^^^^^^^^^^^
+24 |     with_requires(5);
+   |     ^^^^^^^^^^^^^^^^
+
+error: Mutually recursive functions: when calling `with_proof_assert`...
+  --> recursion_through_contract.rs:6:1
    |
-note: then `f1` calls `with_proof_assert`...
-  --> recursion_through_contract.rs:14:5
+6  | fn with_proof_assert(x: Int) {
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
-14 |     with_proof_assert(5);
-   |     ^^^^^^^^^^^^^^^^^^^^
-note: finally `with_proof_assert` calls `f1`.
+note: then `with_proof_assert` calls `f1`...
   --> recursion_through_contract.rs:8:14
    |
 8  |         x == f1()
    |              ^^^^
+note: finally `f1` calls `with_proof_assert`.
+  --> recursion_through_contract.rs:14:5
+   |
+14 |     with_proof_assert(5);
+   |     ^^^^^^^^^^^^^^^^^^^^
 
 error: aborting due to 2 previous errors