`decreases` in interface introduces non-low branch condition (`--hyperMode=on`)

[henriman]

Trying to verify the following program with --hyperMode=on fails.

type Interface interface {
    decreases
    Func() int
}

type TypeAlias int

decreases
func (TypeAlias) Func() int

TypeAlias implements Interface

Assert might fail.
Assertion decreases
    Func() int might not hold.

The reason for this can be found in the Viper encoding, which contains a non-low branch condition; this branch is only generated when specifying decreases for Func. I don't see how this branch condition could be made low, it seems there is a problem with the encoding.

method Func_3eb53157_SY$417df6d7_3eb53157_(thisItf0: Tuple2[Ref, Types], thisItf1: Tuple2[Ref, Types])
  returns (P0_PO00: Int, P0_PO01: Int)
  requires thisItf0 != (tuple2(null, nil_Types()): Tuple2[Ref, Types]) &&
    thisItf1 != (tuple2(null, nil_Types()): Tuple2[Ref, Types])
  decreases ItfMethodMeasure(), ItfMethodMeasure()
{
  inhale P0_PO00 == 0
  inhale P0_PO01 == 0
  
  // decl 
  {
    // if((typeOf(thisItf) == TypeAlias_3eb53157_T)) {...} else {...}
    assert (typeOfInterface_Y$417df6d7_3eb53157_(thisItf0) ==
      TypeAlias_3eb53157_T_Types()) ==
      (typeOfInterface_Y$417df6d7_3eb53157_(thisItf1) ==
      TypeAlias_3eb53157_T_Types())
    if (typeOfInterface_Y$417df6d7_3eb53157_(thisItf0) ==
    TypeAlias_3eb53157_T_Types()) {
      
      // P0_PO0 = thisItf.(TypeAlias_3eb53157_T°)Func()
      P0_PO00, P0_PO01 := Func_3eb53157_MTypeAlias(assertArg2_Int(behavioral_subtype_Types(typeOfInterface_Y$417df6d7_3eb53157_(thisItf0),
        TypeAlias_3eb53157_T_Types()), (unbox_Poly((get0of2(thisItf0): Ref)): Int)),
        assertArg2_Int(behavioral_subtype_Types(typeOfInterface_Y$417df6d7_3eb53157_(thisItf1),
        TypeAlias_3eb53157_T_Types()), (unbox_Poly((get0of2(thisItf1): Ref)): Int)))
      
      // assume false
      inhale false
      inhale false
      
      // return
      goto returnLabel
    }
    
    // assume false
    inhale false
    inhale false
    label returnLabel
  }
}

Note that the extended encoding (--hyperMode=extended) does not have this problem.

(@jcp19: As the hyperGobra branch has been deleted, I'm not sure how to pin-point when this issue first occurred.)

[ArquintL]

The problem is that one has to prove that the same implementation is called in both executions (which would also arise with --hyperMode extended if the interface specifies lowEvent), i.e., that the receiver's dynamic type is low. I don't think our support for interfaces is expressive enough to state this as a precondition for the interface function and, thus, I believe adapting the interface encoding is the only option. Such a solution would have to add a precondition to the generated Viper method mentioned above asserting that the dynamic receiver type is low if the the hyperMode is (1) on or (2) extended and the interface function specifies lowEvent

[ArquintL]

@henriman to find the failing commit (although I'm a bit surprised to hear this ever worked), you can git bisect on the commits that you can still find in PR #802 as these commits are still in the git history despite the commit squashing while merging the PR.

[henriman]

Using git bisect (thank you!) I was able to identify f8041c9ae as the failing commit (0fb74181f does not seem to support SIF, in 327999355 this is still "working"). The reason why this used to "work" is that inhale false used to come before the branch (cf. 2b2c4f226 / #925):

method Func_fbe47909_SY$417df6d7_fbe47909_(thisItf0: Tuple2[Ref, Types], thisItf1: Tuple2[Ref, Types])
  returns (P0_PO00: Int, P0_PO01: Int)
  requires thisItf0 != (tuple2(null, nil_Types()): Tuple2[Ref, Types]) &&
    thisItf1 != (tuple2(null, nil_Types()): Tuple2[Ref, Types])
  decreases
{
  inhale P0_PO00 == 0
  inhale P0_PO01 == 0
  
  // decl 
  {

    // assume false
    inhale false
    inhale false
    
    // if((typeOf(thisItf) == TypeAlias_fbe47909_T)) {...} else {...}
    assert (typeOfInterface_Y$417df6d7_fbe47909_(thisItf0) ==
      TypeAlias_fbe47909_T_Types()) ==
      (typeOfInterface_Y$417df6d7_fbe47909_(thisItf1) ==
      TypeAlias_fbe47909_T_Types())
    if (typeOfInterface_Y$417df6d7_fbe47909_(thisItf0) ==
    TypeAlias_fbe47909_T_Types()) {
      
      // P0_PO0 = thisItf.(TypeAlias_fbe47909_T°)Func()
      P0_PO00, P0_PO01 := Func_fbe47909_MTypeAlias(assertArg2_Int(behavioral_subtype_Types(typeOfInterface_Y$417df6d7_fbe47909_(thisItf0),
        TypeAlias_fbe47909_T_Types()), (unbox_Poly((get0of2(thisItf0): Ref)): Int)),
        assertArg2_Int(behavioral_subtype_Types(typeOfInterface_Y$417df6d7_fbe47909_(thisItf1),
        TypeAlias_fbe47909_T_Types()), (unbox_Poly((get0of2(thisItf1): Ref)): Int)))
      
      // return
      goto returnLabel
    }
    label returnLabel
  }
}