Heap-dependent triggers don't trigger reliably across state-changes

[viper-admin]

Created by @alexanderjsummers on 2018-09-14 09:56
Last updated on 2018-11-22 09:51

For example, all of the following assert statements fail:

#!scala

field data: Seq[Int]

function f(x:Int) : Bool

method test(i:Int)
{
    var s : Seq[Int]
    assume forall x : Int :: {x in s} f(x)
    s := s ++ Seq(1)
    assert i in s ==> f(i) // FAILS
}

method test_two(i:Int)
{
    var r : Ref
    inhale acc(r.data)
    assume forall x : Int :: {x in r.data} f(x)
    r.data := r.data ++ Seq(1)
    assert i in r.data ==> f(i) // FAILS
}

method test_three(i:Int)
{ 
    var r : Ref
    inhale acc(r.data)
    assume forall x : Int :: {r.data[x] in r.data} f(x)
    r.data := r.data ++ Seq(1)
    assert i in r.data ==> f(i) // FAILS in Carbon, not in Silicon
}

[viper-admin]

@alexanderjsummers on 2018-09-14 09:56:

• edited the title

[viper-admin]

@mschwerhoff commented on 2018-10-12 13:46

Potentially related: #257

[viper-admin]

@alexanderjsummers commented on 2018-10-12 18:03

I think the above example is totally bogus. I'm not 100% sure where it came from, to be honest; I suspect we have similar methods elsewhere in the test suite...

For example, in test, i in s should arguably (if the sequence axioms allow it) lead to knowing i in s' OR i in Seq(1) where s' is the original value of s (which is used in the trigger of the quantifier). After branching on this disjunction, the latter case should fail. However, it seems that, depending on precisely which sequence axioms are used, and various other details of the example, the assertion either verifies or doesn't. I found this behaviour sufficiently confusing that I reduced a variant of the example down to an smt query that I posted for help on stackoverflow, but haven't had a response yet.

[viper-admin]

@mschwerhoff commented on 2018-10-12 18:03

test and test_two still fail in Silicon, despite Tobias' recent changes.

I've looked at the Z3 code generated for test in more detail, it looks basically as follows (background axioms omitted):

(declare-const s1 $Seq<Int>) ; ///// Initial value of variable s

;  ///// Assume statement
(assert (forall ((x Int)) (!
  (f $Snap.unit x)
  :pattern (($Seq.contains s1 x))
  )))

; ///// s := s ++ Seq(1)
(assert (= ($Seq.length ($Seq.singleton 1)) 1))
(declare-const s2 $Seq<Int>)
(assert ($Seq.equal s2 ($Seq.append s1 ($Seq.singleton 1))))

; ///// The final assert statement
(push)
  (assert (not (implies ($Seq.contains s2 1) (f $Snap.unit 1))))
(check-sat) ; //// UNKNOWN, assert might not hold
(pop)

Seems that the non-quantified s1 in the trigger prevents the desired quantifier instantiation.

[viper-admin]

@alexanderjsummers commented on 2018-10-12 18:04

Here is a rewritten form of the test case, reflecting what I think should happen:

#!scala

field data: Seq[Int]

function f(x:Int) : Bool

method test_one(i:Int)
{
    var s : Seq[Int]
    assume forall x : Int :: {x in s} f(x)
    s := s ++ Seq(1)
    //:: ExpectedOutput(assert.failed:assertion.false)
    assert i in s ==> f(i) // not the same s as in trigger above!
}

method test_one_stronger(i:Int)
{
    var s : Seq[Int]
    assume forall x : Int :: {x in s} f(x)
    s := s ++ Seq(1)
    assert i in s && i != 1 ==> f(i) 
}

method test_two(i:Int)
{
    var r : Ref
    var b : Bool
    inhale acc(r.data)
    assume forall x : Int :: {x in r.data} f(x)
    r.data := r.data ++ Seq(1)
    if(b) {
      //:: ExpectedOutput(assert.failed:assertion.false)
      assert i in r.data ==> f(i) // not the same r.data as in trigger above!
    } else {
      assert i in r.data && i != 1 ==> f(i) // not the same r.data!
    }
}

method test_two_switched(i:Int)
{
    var r : Ref
    var b : Bool
    inhale acc(r.data)
    assume forall x : Int :: {x in r.data} f(x)
    r.data := r.data ++ Seq(1)
    if(b) {
      assert i in r.data && i != 1 ==> f(i)
    } else {
      // Somewhat surprisingly, this doesn't fail. It seems Z3 keeps the quantifier instantation?
      assert i in r.data ==> f(i) 
    }
}

method test_three(i:Int)
{ 
    var r : Ref
    inhale acc(r.data)
    assume forall x : Int :: {r.data[x] in r.data} f(x)
    r.data := r.data ++ Seq(1)
    //:: ExpectedOutput(assert.failed:assertion.false)
    assert i in r.data ==> f(i)     // rather surprisingly, this didn't fail

}

[viper-admin]

@fabiopakk commented on 2018-11-22 09:51

Merge from fabiopakk_issue_silver_252_deprecated_features, fixing issue 252 in Silver.

→ <<cset f2e57dc>>

[viper-admin]

@fabiopakk on 2018-11-22 09:51:

• changed state from new to resolved