Silicon generates invalid SMT code ("unknown constant") for QPs in functions

[viper-admin]

Created by bitbucket user gishors on 2018-04-04 07:13
Last updated on 2019-05-08 14:00

Important: This issue's cause roots in quantified permissions. If you get "unknown constant"/`"unknown function"` errors but don’t use quantified permissions, please file a new issue.

‌

Silicon is able to verify false in this example.

    field next : Ref

    method join()
    {
        assert false
    }

    domain Foobar {
        function foo(x: Set[Ref]): Bool
        function bar(y: Set[Int]): Bool
    }

    function getEdges(nodes : Set[Ref]): Set[Int]
        requires forall n : Ref :: { n.next } n in nodes ==> acc(n.next)

        ensures forall subnodes: Set[Ref] :: 
            { foo( subnodes ) } 
                subnodes subset nodes ==> bar(getEdges(subnodes))

When using Viper Online, Silicon and Carbon are not able to verify it, but Silicon-nightly and Carbon-nightly are, even though Silicon-nightly has the following original output:

  Interaction with Z3 (instance 02) failed: Unexpected output of Z3. Expected &<https://github.com/viperproject/silicon/issues/39>;success&<https://github.com/viperproject/silicon/issues/39>; but found: (error &<https://github.com/viperproject/silicon/issues/34>;line 509 column 44: unknown constant subnodes@4@00&<https://github.com/viperproject/silicon/issues/34>;)

[viper-admin]

@mschwerhoff commented on 2018-04-04 08:45

There are two orthogonal issues here:

1. Silicon generates invalid SMT code: that is clearly a Silicon bug
2. Viper Online ignores the problem and reports "verification successful": that is a known problem of Viper Online

[viper-admin]

@mschwerhoff on 2018-04-04 08:45:

• edited the title

[viper-admin]

@mschwerhoff commented on 2018-05-05 20:56

• Depends on Potential unsoundness when calling a function requiring QPs under a quantifier #327
• Another example is included in a comment in unknown constant appear in Z3 code #333
• Same symptom, but different root cause: Invalid SMT code ("unknown constant") due to merging chunks during function axiomatisation #379

[viper-admin]

@mschwerhoff commented on 2019-05-08 14:00

Silicon is able to verify false in this example.

#!Silver

    field next : Ref

    method join()
    {
        assert false
    }

    domain Foobar {
        function foo(x: Set[Ref]): Bool
        function bar(y: Set[Int]): Bool
    }

    function getEdges(nodes : Set[Ref]): Set[Int]
        requires forall n : Ref :: { n.next } n in nodes ==> acc(n.next)
        
        ensures forall subnodes: Set[Ref] :: 
            { foo( subnodes ) } 
                subnodes subset nodes ==> bar(getEdges(subnodes))

When using Viper Online, Silicon and Carbon are not able to verify it, but Silicon-nightly and Carbon-nightly are, even though Silicon-nightly has the following original output:

  Interaction with Z3 (instance 02) failed: Unexpected output of Z3. Expected 'success' but found: (error "line 509 column 44: unknown constant subnodes@4@00")

[viper-admin]

@mschwerhoff on 2019-05-08 14:00:

• changed priority from blocker to major
• edited the title
• edited the description

[pieter-bos]

We encountered this issue, I think it applies here (but please let me know if not)

Here is a reduced example from a case we encountered:

field f: Int

function h(xs: Seq[Ref]): Bool
  requires (forall i: Int :: 0 <= i && i < |xs| ==> acc(xs[i].f, write))

function g(xs: Seq[Ref]): Bool
  requires (forall i: Int :: 0 <= i && i < |xs| ==> acc(xs[i].f, write))
  ensures result ==> h(xs)
{
  h(xs)
}

Silicon 20.07 & nightly report:

Verification aborted exceptionally: java.util.concurrent.ExecutionException: viper.silicon.reporting.Z3InteractionFailed: Unexpected output of Z3. Expected 'success' but found: (error "line 1004 column 8: unknown constant result@3@00")
  Cause: viper.silicon.reporting.Z3InteractionFailed: Unexpected output of Z3. Expected 'success' but found: (error "line 1004 column 8: unknown constant result@3@00")
Silicon found 1 error in 3.19s:
  [0] Interaction with Z3 (instance 24) failed: Unexpected output of Z3. Expected 'success' but found: (error "line 1004 column 8: unknown constant result@3@00")

Additionally it seems that the viper IDE vscode plugin swallows the error, reporting "Successfully verified"