`fix-846`: Viper encoding leads to insufficient permissions with interfaces

[henriman]

package tests

type HostAddr interface {
    pred Mem()

    ghost
    hyper
    requires Mem()
    decreases
    pure IsLow() bool
}

type HostNone int

pred (h HostNone) Mem() { true }

ghost
hyper
requires h.Mem()
decreases
pure func (h HostNone) IsLow() bool {
    return true
}

HostNone implements HostAddr

Trying to verify the above program using Gobra branch fix-846 and --hyperMode=on leads to the following verification error (line 6 is at ghost in the interface definition):

12:56:23.200 [pool-1-thread-1] ERROR viper.gobra.reporting.FileWriterReporter - Error at: <.\tests\test85-fix-846.gobra:6:5> Precondition of call might not hold.
Permission to Mem() might not suffice.
12:56:23.304 [pool-1-thread-1] ERROR viper.gobra.reporting.FileWriterReporter - Error at: <.\tests\test85-fix-846.gobra:6:5> Precondition of call might not hold.
Permission to Mem() might not suffice.

---

The reason can be found in the Viper encoding:

function IsLow_3eb53157_SY$ac11f519_3eb53157_(thisItf0: Tuple2[Ref, Types],
  thisItf1: Tuple2[Ref, Types]): Bool
  requires thisItf0 != (tuple2(null, nil_Types()): Tuple2[Ref, Types]) &&
    thisItf1 != (tuple2(null, nil_Types()): Tuple2[Ref, Types])
  requires acc(dynamic_pred_00(thisItf0), write) &&
    acc(dynamic_pred_01(thisItf1), write)
  ensures ((get1of2(thisItf0): Types) == HostNone_3eb53157_T_Types() ==>
    result ==
    DefinedHostNone_3eb53157_T$$$$_E_$$$_IsLow_3eb53157_MHostNone_IsLow_3eb53157_SY$ac11f519_3eb53157__proof((unbox_Poly((get0of2(thisItf0): Ref)): Int),
    (unbox_Poly((get0of2(thisItf1): Ref)): Int))) &&
    ((get1of2(thisItf1): Types) == HostNone_3eb53157_T_Types() ==>
    result ==
    DefinedHostNone_3eb53157_T$$$$_E_$$$_IsLow_3eb53157_MHostNone_IsLow_3eb53157_SY$ac11f519_3eb53157__proof((unbox_Poly((get0of2(thisItf0): Ref)): Int),
    (unbox_Poly((get0of2(thisItf1): Ref)): Int)))
  decreases ItfMethodMeasure(), ItfMethodMeasure()
{
  IsLow_3eb53157_SY$ac11f519_3eb53157_$itfcopy$fallback(thisItf0, thisItf1) &&
  IsLow_3eb53157_SY$ac11f519_3eb53157_$itfcopy$fallback(thisItf0, thisItf1)
}

Precondition of function DefinedHostNone_3eb53157_T$$$$_E_$$$_IsLow_3eb53157_MHostNone_IsLow_3eb53157_SY$ac11f519_3eb53157__proof might not hold. There might be insufficient permission to access dynamic_pred_01((tuple2((box_Poly((unbox_Poly((get0of2(thisItf1): Ref)): Int)): Ref), HostNone_3eb53157_T_Types()): Tuple2[Ref, Types]))

The problem: DefinedhostNone_... requires (get1of2(thisItf1): Types) == HostNone_3eb53157_T_Types() as well. Thus, a potential fix could be to replace

ensures ((get1of2(thisItf0): Types) == HostNone_3eb53157_T_Types() ==>

by

ensures ((get1of2(thisItf0): Types) == HostNone_3eb53157_T_Types() && (get1of2(thisItf1): Types) == HostNone_3eb53157_T_Types() ==>

(and analogously for the second call, where it is the other way around), which makes the file verify successfully.

---

This bug only occurs when the function is annotated with hyper, and when the interface has at least one type implementing it.

(@jcp19)

[henriman]

Likely related: test1 verifies successfully, test2 does not.

ghost
hyper
requires acc(ptr)
decreases
pure func IsLowPtr(ptr *int) bool {
    return low(*ptr)
}

requires acc(ptr)
requires IsLowPtr(ptr)
func test1(ptr *int)


requires acc(ptr) && IsLowPtr(ptr)
func test2(ptr *int)

15:52:34.832 [ForkJoinPool-3-worker-5] ERROR viper.gobra.reporting.FileWriterReporter - Error at: <.\tests\test87-fix-846-perms.gobra:16:22> Precondition of call IsLowPtr(ptr) might not hold.
Permission to ptr might not suffice.

Viper encoding:

method test1_3eb53157_F(ptr_V00: Ref, ptr_V01: Ref)
  requires acc(ptr_V00.Intint$$$$_E_$$$0, write) &&
    acc(ptr_V01.Intint$$$$_E_$$$1, write)
  requires IsLowPtr_3eb53157_F(ptr_V00, ptr_V01)

method test2_3eb53157_F(ptr_V00: Ref, ptr_V01: Ref)
  requires acc(ptr_V00.Intint$$$$_E_$$$0, write) &&
    IsLowPtr_3eb53157_F(ptr_V00, ptr_V01) &&
    (acc(ptr_V01.Intint$$$$_E_$$$1, write) &&
    IsLowPtr_3eb53157_F(ptr_V00, ptr_V01))

The first call to IsLowPtr_3eb53157_F(ptr_V00, ptr_V01) fails due to insufficient permissions to ptr_V01.Intint$$$$_E_$$$1.

[henriman]

Also likely related: Gobra complains about insufficient permissions on call to IsLowSlice in unfolding.

type T []byte

pred (t T) Mem() { acc(t) }

ghost
hyper
requires acc(b)
decreases
pure func IsLowSlice(b []byte) bool

ghost
requires acc(t.Mem(), _)
requires unfolding acc(t.Mem(), _) in IsLowSlice(t)
decreases
func (t T) Func()

11:44:41.233 [ForkJoinPool-3-worker-3] ERROR viper.gobra.reporting.FileWriterReporter - Error at: <.\bugs\bug955-3.gobra:15:39> Precondition of
call IsLowSlice(t) might not hold.
Permission to b might not suffice.

Viper encoding:

method Func_3d39276c_MT(t_V00: Slice[Ref], t_V01: Slice[Ref])
  requires acc(Mem_3d39276c_MT0(t_V00), wildcard) &&
    acc(Mem_3d39276c_MT1(t_V01), wildcard)
  requires (unfolding acc(Mem_3d39276c_MT0(t_V00), wildcard) in
      IsLowSlice_3d39276c_F(t_V00, t_V01)) &&
    (unfolding acc(Mem_3d39276c_MT1(t_V01), wildcard) in
      IsLowSlice_3d39276c_F(t_V00, t_V01))
  decreases

The first call to IsLowSlice_3d39276c_F fails due to insufficient permissions to (ShArrayloc((sarray(t_V01): ShArray[Ref]), sadd((soffset(t_V01): Int), fn$$01)): Ref).Intbyte$$$$_E_$$$1 (as we don't unfold Mem_3d39276c_MT1(t_V01) before).