silicon
silicon copied to clipboard
viperproject
Incompleteness from non-linear (permission) arithmetic
Created by bitbucket user fhahn on 2015-11-19 10:10 Last updated on 2019-08-28 21:03
Silicon seems to have problems unfolding predicates with variable permission parameter. For the following listing Silicon manages to verify foo_ok, wich passes constant permissions to the predicate valid.
The other two methods fail, because after unfolding Silicon complains There might be insufficient permission to access self.v.. Note that in those two methods, the permissions passed to the predicate are are a variable that's passed to the method.
#!scala
method foo_ok(self: Ref)
requires acc(valid__Cell(self, 1/2), 1/2)
requires (unfolding acc(valid__Cell(self, 1/2), 1/2) in self.v) == 1
{}
method foo_fail(self: Ref, rd: Perm)
requires acc(valid__Cell(self, rd), rd)
requires none < rd && rd < write
requires (unfolding acc(valid__Cell(self, rd), rd) in self.v) == 1
{}
method bar(self: Ref, rd: Perm)
requires acc(valid__Cell(self, rd), rd)
requires none < rd && rd < write
{
unfold acc(valid__Cell(self, rd), rd)
assert self.v == 1
}
field v: Int
predicate valid__Cell(self: Ref, rd: Perm) {
acc(self.v, rd)
}
Attachments:
@mschwerhoff commented on 2015-11-20 14:36
This is essentially an incompleteness of Z3's non-linear real arithmetic solver (apparently in combination with the theory of uninterpreted functions plus quantifiers), as demonstrated by the following SMT program, which I tested with Z3 4.4.0 and the most recent (at the time of writing) 4.4.2-nightly:
#!text
;;; Enabling auto_config or mbqi doesn't seem to make a difference
(set-option :auto_config false)
(set-option :smt.mbqi false)
;;; Any (not totally trivial) quantification will do.
;;; If it is removed, the check-sats succeed.
(declare-fun foo (Real) Real)
(assert (forall ((i Real)) (!
(= i (foo i))
:pattern ((foo i))
)))
(declare-const rd Real)
(assert (< 0 rd))
;;; Whether or not incremental mode (push-pop) is used doesn't seem to make
;;; a difference either
(push)
(assert (= rd 0))
(check-sat) ; UNSAT
(pop)
(push)
(assert (= (* rd rd) 0))
(check-sat) ; UNKNOWN
(pop)
(push)
(assert (<= rd 0))
(check-sat) ; UNSAT
(pop)
(push)
(assert (<= (* rd rd) 0 ))
(check-sat) ; UNKNOWN
(pop)
(push)
(assert (not (> (* rd rd) 0 )))
(check-sat) ; UNKNOWN
(pop)
I can post the problem on Stackoverflow, but I am sceptical that there'll be a fix any time soon.
@mschwerhoff on 2018-03-02 19:59:
- edited the title
- edited the description
@mschwerhoff commented on 2018-03-02 20:00
https://github.com/viperproject/silicon/issues/319 was marked as a duplicate of this issue.
@alexanderjsummers commented on 2019-08-28 10:25
Did you post on Stackoverflow, Malte? Now that I look at it again, it’s slightly surprising that the incompletenesses are so basic (especially since we only rely on non-linear real arithmetic (which is decidable, and I would have thought would be supported better in Z3). Maybe there’s some reason why this ends up with an integer solver anyway…
@mschwerhoff commented on 2019-08-28 21:03
@alexanderjsummers I don’t remember, but I can’t find a corresponding post/issue on Stackoverflow/Github, so probably … not.
This seems the same issue of #480 (and various others).
As for why the incompletenesses are so basic, @alexanderjsummers, this Z3 issue might shed some light. It's enough for the SMT query to contain any non-real-arithmetic feature, like labels, to make Z3 fall back from nlsat_solver to smt core (incomplete for nla).
