Feat/vsr operator - #8
Open
ricostynha1 wants to merge 5 commits into
Open
ricostynha1 wants to merge 5 commits into
ricostynha1 wants to merge 5 commits into
Conversation
CAS was emitted with neither a ShouldImplement nor an IsIncludedInTarget guard, so --operators X still scanned CAS and --line N produced CAS targets from other lines. CAS was also missing from IsValidOperator, so it could only ever leak, never be requested. Every restricted run to date scanned one more operator than asked for.
ProduceStmt.Rhss is null for a bare `return;` (as opposed to `return e;`). ScanCollectionUpdateTargets dereferenced it unguarded; the resulting NullReferenceException aborted the scan of the WHOLE file, so every method in it produced zero mutants -- indistinguishable from "this method has no targets". PreResolveTargetScanner.GetRhsNameList had the same null hazard.
MethodReturnReplacementMutator (MRR) already built an Expression for a type's default value -- 0 for int, [] for seq, the nullary constructor for a datatype:Ctor code, etc -- to use as a call-site/assignment-RHS replacement. Move it into the Mutator base as CreateDefaultExpression so other mutators can reuse the same construction instead of duplicating it. The switch was missing a "nat" case, so an MRR target for a nat-typed expression silently produced a null literal instead of 0. Fixed while moving it.
VSR replaces a method's whole body with a do-nothing stub. A stub that still verifies against the original contract is direct evidence the postcondition doesn't actually constrain the output: a body that throws its input away satisfies it. Because the stub is generated directly from the method's signature, VSR doesn't need to perturb an existing body the way every other operator here does -- it can produce a candidate mutant for a method regardless of that method's body shape. The stub plan arrives as the mutation argument: '+'-separated, one token per out-param -- d<typecode> (type default, via the shared CreateDefaultExpression), c<Ctor> (nullary datatype constructor, same helper), l<int> (a literal lifted from the ensures clause), v<name> (identity on an input) -- plus the whole-plan literal `empty` for a void method, whose stub is an empty body. Targets are emitted from PostResolveTargetScanner, where out-param types are resolved and TypeToStr is available. The identity family is skipped when it would regenerate the body verbatim (`ys := xs;`) -- that stub would be syntactically identical to the original method, the classic equivalent-mutant case: it trivially verifies because it IS the original program, not because anything was learned about the postcondition. The `empty` plan defers to SDL when SDL is also requested, since SDL already produces the same empty-body mutant by deleting the whole body -- otherwise the two operators would verify the same mutant twice under different labels. Measured over a corpus of 407 Dafny methods whose postconditions were suspected too weak to constrain their implementation, but where no existing operator had produced conclusive evidence either way: VSR produced at least one surviving (alive) mutant for 274 of them (67.3%), killed all its mutants for 92, and found no valid stub at all for the remaining 41 -- at 1.34 mutants and 3.6s per method.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Some bug fixes.
And one proposed new mutant operator (the new mutant operator simply replaces the complete body by a value of a given type using previous infrastructure for another mutant that already did something simmilar but for assigments).