silicon
silicon copied to clipboard
viperproject
Triggering problems due to internally introduced function symbols (e.g. join functions)
Created by bitbucket user ykass on 2014-08-21 08:41 Last updated on 2018-05-13 13:50
The verification of the attached file fails. Silicon can unfold the function definition in the first simple assertion, but if we make it more complicated it fails (second assertion)
Attachments:
Bitbucket user ykass commented on 2014-08-21 08:45
Could also be a problem with the ?: expression: I have seen it twice in this context
@mschwerhoff commented on 2014-08-21 09:56
In essence, the problem is due to triggers, which are too strict if the function application is inside a conditional that is evaluated locally. I'll look into it.
@mschwerhoff commented on 2014-08-31 10:41
Resolved with commit https://github.com/viperproject/silicon/commit/9823a155551005354ea217d79d4c296d76e45bf5. Locally evaluating if-then-else and unfolding expressions result in internally used functions that needed to be added to the list of triggers there were explicitly provided (or automatically computed) for a quantified expression.
@mschwerhoff commented on 2017-08-24 16:20
The problem has apparently been re-introduced in the meantime, but somehow went unnoticed.
I've extended regression test all/issues/silicon/0114.sil by a few small tests that illustrate different incarnations of the same underlying problem. test02 is probably the simplest: there, the program quantifier to assert roughly is forall j :: {fun1(j)} unfolding ... in fun1(j). Because the unfolding expression branches, a join function fun1_join will be introduced and axiomatised appropriately as part of the auxiliary quantifier corresponding to the program quantifier. However, the auxiliary quantifiers trigger will be that of the program quantifier, i.e. fun1(j), but the body of the program quantifier to assert will only mention fun1_join. An idea for a solution would be to add such internally introduced functions to the list of triggers of the auxiliary quantifiers.
A related, but slightly different issue is illustrated by test05: here, an explicitly provided trigger fun2(...) is replaced by the internally introduced join function fun2_join(...), but then the axiom doesn't trigger when fun2(...) is provided as a trigger later on.
@mschwerhoff commented on 2018-05-13 13:50
Related: https://github.com/viperproject/silicon/issues/331