Set and Sequence axiomatisation incompletenesses

[viper-admin]

Created by @mschwerhoff on 2015-06-10 07:25
Last updated on 2019-05-16 13:37

#!text

method m03(S1: Seq[Ref], S2: Set[Ref], x: Ref)
  requires S1 == Seq(x) && S2 == Set(x)
  requires forall i: Int :: i in [0..|S1|) ==> S1[i] != null
  ensures  forall y: Ref :: y in S2 ==> y != null /* Fails */
{}

method m04(S1: Seq[Ref], S2: Set[Ref], x: Ref)
  requires S1 == Seq(x) && S2 == Set(x)
  requires forall y: Ref :: y in S1 ==> y != null
  ensures  forall y: Ref :: y in S2 ==> y != null /* Fails */
{}

method m03simplified(S1: Seq[Ref], x: Ref)
  requires S1 == Seq(x)
  requires forall i: Int :: i in [0..|S1|) ==> S1[i] != null
  ensures  x != null /* Fails */
{}

method m04simplified(S1: Seq[Ref], x: Ref)
  requires S1 == Seq(x)
  requires forall y: Ref :: y in S1 ==> y != null
  ensures  x != null /* Fails */
{}

method m04adapted(S1: Set[Ref], x: Ref)
  requires S1 == Set(x)
  requires forall y: Ref :: y in S1 ==> y != null
  ensures  x != null /* Fails */
{}

method m04adaptedWithProperty(S1: Set[Ref], x: Ref)
  requires S1 == Set(x)
  requires forall z: Ref :: {Set(z)} z in Set(z)
  requires forall y: Ref :: y in S1 ==> y != null
  ensures  x != null /* Passes */
{}

method m04adaptedWorse(S1: Set[Ref], x: Ref, a: Ref)
  requires S1 == Set(x,a)
  requires forall z: Ref :: {Set(z)} z in Set(z)
  requires forall y: Ref :: y in S1 ==> y != null
  ensures  x != null /* Fails in Silicon, but not in Carbon (?) - probably expected to fail */
{}

method m04adaptedWorseWithFurtherProperty(S1: Set[Ref], x: Ref)
  requires S1 == Set(x,x)
  requires forall z: Ref :: {Set(z)} z in Set(z)
  requires forall s1: Set[Ref], s2: Set[Ref], w:Ref :: {w in s1, (s1 union s2)} w in (s1 union s2) <==> (w in s1) || (w in s2)
  requires forall y: Ref :: y in S1 ==> y != null
  ensures  x != null /* Passes */
{}

[viper-admin]

@mschwerhoff on 2015-06-10 07:26:

• edited the description
• edited the title

[viper-admin]

@mschwerhoff commented on 2015-06-10 07:31

Corresponding tool issues:

• Carbon: issue 46
• Silicon: issue 150

[viper-admin]

@alexanderjsummers on 2015-06-10 09:46:

• edited the description
• edited the title

[viper-admin]

@alexanderjsummers on 2015-11-25 15:53:

• edited the description
• edited the title

[viper-admin]

@alexanderjsummers commented on 2015-11-25 16:11

The behaviour doesn't seem to be consistent between the two verifiers. We should check that the axiomatisations are in sync.

[viper-admin]

@aterga commented on 2017-01-08 23:10

This issue is (at least partially) related to triggering. The following code verifies:

function notNull(x: Ref): Bool
{
    x != null
}

method m04simplified(S1: Seq[Ref], x: Ref)
    requires S1 == Seq(x)
    requires forall y: Ref :: { notNull(y) } y in S1 ==> notNull(y)
    ensures notNull(x) 
{}

However, the more straightforward version does not verify:

method m04simplified(S1: Seq[Ref], x: Ref)
  requires S1 == Seq(x)
  requires forall y: Ref :: y in S1 ==> y != null
  ensures  x != null /* Fails */
{}

[viper-admin]

@alexanderjsummers commented on 2018-04-30 10:07

Some improvements were made in Carbon commit viperproject/carbon@3a7ce80

[viper-admin]

@mschwerhoff commented on 2018-05-01 12:43

@alexanderjsummers Should these recent changes be ported to Silicon?

[viper-admin]

@alexanderjsummers commented on 2018-05-02 10:21

I'm not sure how stable the solution is yet.

[viper-admin]

@alexanderjsummers commented on 2018-07-06 14:04

For reference, I reverted the changes, but am still optimistic that something better can be done..

[viper-admin]

@alexanderjsummers commented on 2018-07-09 15:45

Here's another good one:

#!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 in Silicon, not in Carbon
}

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 in both tools
}

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 commented on 2018-07-10 09:21

I edited the example above, as Carbon's behaviour changed (I think there was a related bug fixed)

[viper-admin]

@alexanderjsummers commented on 2019-05-16 13:33

See viperproject/silicon#380

[viper-admin]

@alexanderjsummers commented on 2019-05-16 13:37

See also viperproject/carbon#273