value might not fit into the target type (due to check_overflows)

[Pointerbender]

use prusti_contracts::*;

#[derive(Clone, Copy)]
pub struct A {
    count: isize,
}

impl A {
    #[pure]
    #[ensures(result <= isize::MAX as usize)]
    pub const fn len(&self) -> usize {
        if self.count < 0 {
            ((1_isize + self.count) + isize::MAX) as usize
        } else {
            self.count as usize
            //~^ ERROR value might not fit into the target type.
        }
    }
}

#[pure]
#[requires(slice.len() > 0)]
#[requires(slice[0].len() == 0)]
pub fn test(slice: &[A]) -> bool {
    true
}

fn main() {}

The above program yields the error [Prusti: verification error] value might not fit into the target type. for the Viper program of fn test (the Viper program for len verifies okay as expected). There seems to be a problem in the pure encoding of the struct fields for A in the precondition #[requires(slice[0].len() == 0)] of fn test. It looks like acc(isize(_1.f$count)) is not properly applied during the pure lookup of slice[0] in Viper function m_len__$TY$__Snap$struct$m_A$$int$(_1: Snap$struct$m_A): Int. Overflow checks should to be enabled to trigger this error.

Edit: the relevant generated Viper statements for the Viper program for fn test are:

domain MirrorDomain {

  function mirror_simple$m_len__$TY$__Snap$struct$m_A$$int$(_1: Snap$struct$m_A): Int
}

domain Snap$struct$m_A {

  function Snap$struct$m_A$0$field$f$count__$TY$__Snap$struct$m_A$$int$(self: Snap$struct$m_A): Int
}

function m_len__$TY$__Snap$struct$m_A$$int$(_1: Snap$struct$m_A): Int
  requires true
  requires true
  ensures result <= builtin$cast$isize$usize__$TY$__$int$$$int$(9223372036854775807)
  ensures 0 <= result
  ensures result <= 18446744073709551615
  ensures [result == mirror_simple$m_len__$TY$__Snap$struct$m_A$$int$(_1), true]
{
  (!(Snap$struct$m_A$0$field$f$count__$TY$__Snap$struct$m_A$$int$(_1) < 0) ? builtin$cast$isize$usize__$TY$__$int$$$int$(Snap$struct$m_A$0$field$f$count__$TY$__Snap$struct$m_A$$int$(_1)) : (!(1 + Snap$struct$m_A$0$field$f$count__$TY$__Snap$struct$m_A$$int$(_1) < -9223372036854775808 || 1 + Snap$struct$m_A$0$field$f$count__$TY$__Snap$struct$m_A$$int$(_1) > 9223372036854775807) ? (!(1 + Snap$struct$m_A$0$field$f$count__$TY$__Snap$struct$m_A$$int$(_1) + 9223372036854775807 < -9223372036854775808 || 1 + Snap$struct$m_A$0$field$f$count__$TY$__Snap$struct$m_A$$int$(_1) + 9223372036854775807 > 9223372036854775807) ? builtin$cast$isize$usize__$TY$__$int$$$int$(1 + Snap$struct$m_A$0$field$f$count__$TY$__Snap$struct$m_A$$int$(_1) + 9223372036854775807) : builtin$unreach_int__$TY$__$int$()) : builtin$unreach_int__$TY$__$int$()))
}

[fpoli]

Formatted (We should fix Silver to do this automatically):

function m_len__$TY$__Snap$struct$m_A$$int$(_1: Snap$struct$m_A): Int
  requires true
  requires true
  ensures result <= builtin$cast$isize$usize__$TY$__$int$$$int$(9223372036854775807)
  ensures 0 <= result
  ensures result <= 18446744073709551615
  ensures [result == mirror_simple$m_len__$TY$__Snap$struct$m_A$$int$(_1), true]
{
  (
    !(Snap$struct$m_A$0$field$f$count__$TY$__Snap$struct$m_A$$int$(_1) < 0)
    ? builtin$cast$isize$usize__$TY$__$int$$$int$(
      Snap$struct$m_A$0$field$f$count__$TY$__Snap$struct$m_A$$int$(_1)
    )
    : (
      !(
        (
          1 + Snap$struct$m_A$0$field$f$count__$TY$__Snap$struct$m_A$$int$(_1)
          < -9223372036854775808
        ) || (
          1 + Snap$struct$m_A$0$field$f$count__$TY$__Snap$struct$m_A$$int$(_1)
          > 9223372036854775807
        )
        ? (
          !(
            (
              1 + Snap$struct$m_A$0$field$f$count__$TY$__Snap$struct$m_A$$int$(_1)
              + 9223372036854775807
              < -9223372036854775808
            ) || (
              1 + Snap$struct$m_A$0$field$f$count__$TY$__Snap$struct$m_A$$int$(_1)
              + 9223372036854775807 > 9223372036854775807
            )
          )
          ? builtin$cast$isize$usize__$TY$__$int$$$int$(
            1 + Snap$struct$m_A$0$field$f$count__$TY$__Snap$struct$m_A$$int$(_1)
            + 9223372036854775807
          )
          : builtin$unreach_int__$TY$__$int$()
        )
        : builtin$unreach_int__$TY$__$int$()
    )
  )
}

What is happening here is that the pure encoding checks the value bounds in the postcondition, but does not require the input to be in its value bounds. It might be a leftover of the migration to snapshots. As discussed in https://github.com/viperproject/prusti-dev/issues/718, since the overflow checks are currently already checked in the impure encoding (with a Viper method), we should remove these checks from the pure encoding (the Viper function).

In other words, the postconditions

  ensures result <= builtin$cast$isize$usize__$TY$__$int$$$int$(9223372036854775807)
  ensures 0 <= result
  ensures result <= 18446744073709551615

should become something like

  ensures [result <= builtin$cast$isize$usize__$TY$__$int$$$int$(9223372036854775807), true]
  ensures [0 <= result, true]
  ensures [result <= 18446744073709551615, true]

such that they are not checked on the definition side but assumed on the call side.

(@zgrannan @JonasAlaif I think the encoding of invariants will face the same issue, when encoding pure functions.)

[Pointerbender]

In other words, the postconditions

  ensures result <= builtin$cast$isize$usize__$TY$__$int$$$int$(9223372036854775807)
  ensures 0 <= result
  ensures result <= 18446744073709551615

should become something like

  ensures [result <= builtin$cast$isize$usize__$TY$__$int$$$int$(9223372036854775807), true]
  ensures [0 <= result, true]
  ensures [result <= 18446744073709551615, true]

such that they are not checked on the definition side but assumed on the call side.

When making the suggested changes in the Viper program directly, there is another error stating Precondition of function builtin$cast$isize$usize__$TY$__$int$$$int$ might not hold. Assertion Snap$struct$m_A$0$field$f$count__$TY$__Snap$struct$m_A$$int$(_1) <= 9223372036854775807 might not hold. (lib.rs_test.vpr@83.121--83.121)

I believe the root cause for this lies in the Viper encoding of the domain for struct A:

domain Snap$struct$m_A {

  function Snap$struct$m_A$0$field$f$count__$TY$__Snap$struct$m_A$$int$(self: Snap$struct$m_A): Int
}

It appears to be missing information about the integer bounds for its field count: isize. I was able to make Viper verify the program by additionally adding the following axiom manually:

domain Snap$struct$m_A {

  function Snap$struct$m_A$0$field$f$count__$TY$__Snap$struct$m_A$$int$(self: Snap$struct$m_A): Int

  axiom struct$m_A$count$isize {
      (forall data: Snap$struct$m_A :: { Snap$struct$m_A$0$field$f$count__$TY$__Snap$struct$m_A$$int$(data) } Snap$struct$m_A$0$field$f$count__$TY$__Snap$struct$m_A$$int$(data) >= -9223372036854775808 && Snap$struct$m_A$0$field$f$count__$TY$__Snap$struct$m_A$$int$(data) <= 9223372036854775807 )
  }
}

Is this something that Prusti should generate automatically in the Viper program when check_overflows = true, or should this information be encoded differently somehow?

[vakaras]

Is this something that Prusti should generate automatically in the Viper program when check_overflows = true, or should this information be encoded differently somehow?

Yes, it should. After my refactorings are done, each type should have an automatically generated valid function that expresses the properties that hold for a valid instance of the type. For integers, the valid function would specify their bounds.

[JonasAlaif]

@vakaras This is still not fixed right? I ran into the same issue with:

use prusti_contracts::*;
fn main() {}

#[pure]
pub fn get(a: &usize) -> usize { *a }
fn foo(a: &usize) {
    let v = get(a);
}

Where the error is super counterintuitive since it is reported in foo and not get where the encoding is:

function m_get__$TY$__(_1: Int): Int
  ensures 0 <= result
  ensures result <= 18446744073709551615
  ensures [result == mirror_simple$m_get__$TY$__(_1), true]
{
  _1
}

The issue is, as you mention above, that we require any base type to adhere to non-overflow requirements, but any composite type doesn't have to.

[JonasAlaif]

Also, would it be easy to add support for get(&0)? Currently the &0 is [Prusti: unsupported feature] unsupported constant type Ref('_#6r, usize, Not)

[vakaras]

My refactorings are still in progress.

[vakaras]

Also, would it be easy to add support for get(&0)? Currently the &0 is [Prusti: unsupported feature] unsupported constant type Ref('_#6r, usize, Not)

In a pure context, you may be able to special case it by feeding in 0 instead of &0. In non-pure context, no idea.

[JonasAlaif]

The original example seems to now have been fixed, but the example I give still fails. I guess the refactorings should eventually fix it

[Pointerbender]

I've got two more examples related to this issue:

use prusti_contracts::*;

#[requires(test(1).a == 1)]
fn main() {}

#[derive(Clone, Copy)]
pub struct A {
    a: usize
}

#[pure]
#[requires(a <= isize::MAX as usize)]
#[ensures(result.a <= isize::MAX as usize)]
pub fn test(a: usize) -> A {
    A { a: a as isize as usize as isize as usize }
}

use prusti_contracts::*;

fn main() {
    bar(1, 1);
    bar(1, 2);
    baz(1, 1);
    baz(1, 2);
}

#[derive(Clone, Copy, PartialEq, Eq)]
pub struct A {
    a: usize
}

#[pure]
pub fn foo(a: usize) -> A {
    A { a }
}

#[pure]
#[requires(a == b ==> foo(a) == foo(b))]
pub fn bar(a: usize, b: usize) {}

#[pure]
#[requires(foo(a) == foo(b) ==> a == b)]
pub fn baz(a: usize, b: usize) {}

(I'm preparing a PR that addresses these 2 cases)