fix: Don’t flag extern functions with {:axiom} as assumptions #4979
Conversation
| @@ -65,15 +65,14 @@ public class Function : MemberDecl, TypeParameter.ParentType, ICallable, ICanFor | |||
| yield return new Assumption(this, tok, AssumptionDescription.NoBody(IsGhost)); | |||
| } | |||
|
|
|||
| if (HasExternAttribute) { | |||
| if (HasExternAttribute && !HasAxiomAttribute) { | |||
There was a problem hiding this comment.
The way I understood the audit-report is that you don't run it as part of CI, but use it as part of a whole-program code review that you do at particular times in your development workflow, like before a release or when onboarding a new customer. What the auditor (a person) wants to know at those times is, what the overrides are that developers put in place to bypass verification, so any places where {:axiom} occurs !
@atomb did I understand that correctly?
There was a problem hiding this comment.
Yes, that's my intention for it as well. It's for when you want to say "this thing is fully verified, but what risks remain?". For that, we really want to keep all extern declarations in the list of things reported by the auditor.
I think this approach is a good one for silencing warnings during the normal development process. In the context of the auditor, I think having {:axiom} should convert an extern declaration from an implicit assumption to an explicit assumption. Explicit assumptions are those that have been acknowledged as assumptions through some extra annotation and are therefore considered intentional. The final goal for a verified project is, in my mind, for all remaining assumptions to be explicit, and to have documented reasons for why you think that each one is warranted.
There was a problem hiding this comment.
On thing that might not be obvious here: the state before this change is that function {:extern} {:axiom} ... would always produce two Assumptions: one for the presence of {:axiom} in general, and one for the fact that you're assuming that an extern actually behaves like a non-deterministic function. The first is considered an explicit assumption and the second an implicit one. The intent is that doo files only allow explicit assumptions, so the first was allowed but the second caused an error.
It was already true that adding {:axiom} to an extern method or function would replace the implicit assumptions for any post-conditions by an explicit one just saying "you have an axiom here" instead. The effect of this change is just to let the explicit {:axiom} assumption suppress the additional implicit one about the function-ness of your extern too. Hence just adding && !HasAxiomAttribute makes sense for both the auditor and building doo files.
There was a problem hiding this comment.
Makes sense. I had trouble seeing that the explicit assumption is still flagged.
There was a problem hiding this comment.
Ditto. I agree in that broader context.
Description
Fixes #4964, more directly and specifically than the general improvements @keyboardDrummer is making as per #4964 (comment) (which are also good improvements for the future). Pre/post-conditions on extern functions are already allowed in doo files with the
{:axiom}attribute, so this just allows that to suppress the additional implicit requirement that the extern implementation behaves like a deterministic function.How has this been tested?
Existing tests of the auditor and doo files (removes an arguably duplicative assumption on
function {:extern} {:axiom} ...declarations)By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.