Add verifier process supervisor and broaden analyzer/contracts/effects coverage - #124
Merged
Conversation
…s analyzer, contracts, and effects modules Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…n API mismatches - Enable AllowUnsafeBlocks in SharpProof.BuildTasks for LibraryImport marshalling - Rename duplicate local function AddReachableFinallyEntries overload - Use Conversion.Method instead of nonexistent Conversion.MethodSymbol - Use public CSharpExtensions.GetDeconstructionInfo instead of internal CSharpSemanticModel - Pin ToImmutableHashSet<INamedTypeSymbol> to avoid ISymbol inference mismatch Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…, IDE formatting - Move PushSequential/PushAll local functions out of PushChildren so outer while-loop callers can resolve them - Rename pattern-bound locals (property/field/simple) that collided across sibling blocks sharing the same enclosing scope - Cast IEventAssignmentOperation.EventReference to IEventReferenceOperation before accessing Instance/Event (property is typed as plain IOperation) - Fix DeconstructionInfo.Conversion?.MethodSymbol nullable access - Guard IConditionalOperation.WhenTrue/WhenFalse nullability in ConversionOwnershipClassifier - Narrow return types to satisfy CA1859 performance suggestions - Implement IDisposable on RunVerifier for its ManualResetEventSlim/ Process fields (CA1001/CA2213) - Use ToUpperInvariant per CA1308, await instead of Task.Result per CA1849 - Reformat RunVerifier property declarations for IDE0055 - Suppress CA1515 on public MSBuild Task types now that BuildTasks is an Exe project (task classes must stay public for MSBuild) Verified via standalone probe projects compiling SharpProof.Effects and SharpProof.BuildTasks with matching TreatWarningsAsErrors/AnalysisLevel settings, since the repo build is gated behind the Docker tooling container. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…of.Effects - Move a stray closing brace fix in ManagedAbstractFlow.cs pattern block - Replace list-pattern syntax in OperationCompletionEvaluator.cs that required System.Index (unavailable on this netstandard2.0 target) with equivalent Length/indexer checks - Suppress a CA1508 false positive where the analyzer misreads a multi-branch nullable assignment as always-null - Re-run dotnet format whitespace across the touched files to satisfy IDE0055 in the exact-SHA build gate Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Re-ran dotnet format whitespace after upstream edits reintroduced misaligned brace patterns in ConversionOwnershipClassifier.cs, and manually aligned the equivalent pattern in FrontendFuzzing.cs. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
- baseCall pattern variable collided with a later local of the same name (same class of bug fixed earlier in Effects) - IrSemanticTerms.CollectVariables doesn't exist; the method lives on the sibling IrTermAnalysis class in the same file - GetConstantPatternMatch/MatchTypePattern used the instance semanticModel field but were called from a static traversal method with no instance; made both static and threaded a Compilation parameter through instead (declarations without a matched type now report Unknown rather than passing a null argument) - IArrayLengthOperation isn't a real Roslyn operation kind; array .Length access is already covered by the adjacent IPropertyReferenceOperation case - A `var target = assignment.Left` inferred ExpressionSyntax, which can't hold SingleVariableDesignationSyntax or the SyntaxNode elements GetDeconstructionElements returns; declared explicitly as SyntaxNode - GetDeclaredSymbol(VariableDesignationSyntax) always returns null per RS1039; narrowed to SingleVariableDesignationSyntax first - Narrowed several return/parameter types for CA1859, suppressed a recurring CA1508 false positive on multi-branch nullable assignment patterns, and re-ran dotnet format for IDE0055 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…overy tests - The three CoalesceAssignmentSkipsSetterAfterNonreturning* tests only expected the target property's getter as a discovered candidate. RequiresCallSiteDiscovery legitimately also surfaces the ordinary invocation that produces the non-completing receiver/index/value (e.g. Fail()) as its own non-replayable candidate, consistent with the discovery API's documented behavior of surfacing every reachable call (see ImplicitBaseConstructorProducesOneReplayCandidate). Verified the actual candidate list locally (kind/name/canReplay/span) before updating the expected MethodKind sequences to include it. - UnreferencedLocalFunctionsAreNotAnalyzed expected 2 SP0027 diagnostics but the source only has one reachable Requires-violating call site (ThroughSibling's call to Positive(-2)); Dead() is correctly excluded as unreferenced, and Reachable() itself doesn't directly violate anything. Corrected the expected count to 1. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
- DefiniteOperationFacts.MayCompleteNormally: recognize a coalesce expression whose left side is statically null as only completing through its WhenNull branch; recognize an instance property/indexer access on a statically-null receiver as never completing; recognize an instance call dispatched on a statically-null receiver as never completing (InvocationMayCompleteNormally). - DefiniteOperationFacts.CompletesNormally: add the missing IFieldReferenceOperation and IObjectCreationOperation cases (both silently fell through to `_ => false`), matching the existing IMethodReferenceOperation pattern; treat an implicit/no-syntax constructor as trivially non-throwing. - RequiresCallSiteAnalyzer.AnalyzeConcreteCall/AnalyzeAbstractCallSite: bail out of concrete/abstract evaluation when the call's instance or any argument is proven to never complete normally, or when the instance is proven null for an instance-method dispatch, instead of only checking the parameters a Requires clause happens to reference. - RequiresCallSiteTreeAnalyzer.GetTuplePath: fixed an off-by-one ancestor lookup (checked candidate.Parent.Parent instead of candidate.Parent for a TupleExpressionSyntax), which made every tuple-component path resolve to null and fall back to whole-value tracking; also resolve component names from the converted tuple type so an unnamed literal converted to a named tuple type still matches on the correct field. - RequiresCallSiteTreeAnalyzer.BlockMayThrowBeforeAssignmentCommit: scan every block in the graph bounded by the assignment's syntax span, not just the single block containing the commit, since a ternary/coalesce RHS can be lowered across multiple CFG blocks. - RequiresCallSiteDiscovery.Get: list-pattern operations don't need a recorded flow-state entry to be replay-evaluated (their CanReplay already comes from the flow-independent HasReplayableAccessorEvaluation), so stop skipping them when the flow analysis has no per-operation state for them; also fold arrow-bodied Length/Count getters (ArrowExpressionClauseSyntax) the same way expression-bodied ones already are. Verified via the full SharpProof.Analyzer.Test, SharpProof.Effects.Test, and SharpProof.ContractForGenerator.Test suites locally (Docker), plus a full solution build with 0 warnings/errors. Diagnosed collaboratively with several parallel read-only investigation agents; all fixes were applied and verified directly against the actual production behavior rather than the agents' unverified guesses. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Classifying SharpProof.Fuzz as a production project (Directory.Build.props) means it now picks up BannedApiAnalyzers, but BoundaryEnforcementTests' hardcoded BannedApiProjects list was never updated to match. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…scanning tests BoundaryEnforcementTests' SourceFiles/ProjectFile/GeneratedProductionFilesAreExplicitlyApproved helpers assumed every project directory sits directly under the repo root, but SharpProof.Fuzz lives under Tools/SharpProof.Fuzz. Now that Fuzz is a production project (banned-API scope), these helpers threw DirectoryNotFoundException. Added a ProjectDirectory() resolver (mirroring the existing Tools\SharpProof.Fuzz special-case already used elsewhere in this file for the .sln project-list check) and routed all three helpers through it. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
… checkout Invoke-SharpProofReleaseContainer.ps1 dot-sources Resolve-SharpProofContainedPath.ps1 unconditionally at the top of the script, for every -Mode, but the release-tag fixture only ever copied Invoke-SharpProofReleaseContainer.ps1 and Get-SharpProofReleaseVersion.ps1 into the temp checkout. Every fixture invocation (including the should-succeed exact-annotated case) was throwing a file-not-found error at dot-source time, which Invoke-TagCase's try/catch silently turned into "rejected" — masking a real validation bug behind an apparent one. Verified locally: all release-tag fixtures now pass. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…eferences Root-caused ExceptionHandlersCanConsumeTrackedDelegates via a raw CFG dump: for `x = cond ? a : b;`, Roslyn lowers the condition-evaluation block with an IFlowCaptureOperation whose descendant ILocalReferenceOperation happens to share the exact same syntax span as the real assignment target `x`. IsAssignmentTarget is purely syntactic, so CanReachConsumption treated that flow-capture reference as the assignment commit, called BlockMayThrowBeforeAssignmentCommit on it, found no enclosing ISimpleAssignmentOperation (there isn't one - it's just a captured read), and returned false. That silently killed the tracked delegate with exceptionalStateSurvivesKill=false, which stops the BFS from enqueueing anything further - so the real commit block, the actual throwing condition, and the catch handler were never visited at all. Added HasEnclosingSimpleAssignment to distinguish a genuine commit reference (embedded in an ISimpleAssignmentOperation) from a same-span flow-capture artifact, and skip the latter instead of treating it as a kill. Verified: SharpProof.Analyzer.Test is now 389/389 (0 failures), a full solution build succeeds with 0 warnings/errors, and SharpProof.Effects.Test shows only the two pre-existing, unrelated failures that were already failing before this session. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Root-caused RefLikeValueCopiesPreserveExternalAliases (CopyReceiverThenMutate)
by tracing the effect summary join at each layer: BuildLocalRegions correctly
detects `target.Cell = ref Cell;` (in CopyTo, where target is a ref-like
parameter and Cell a ref field) as a ref-rebinding case needing local-region
tracking, but computed the *source* side via the generic ClassifyRegion
switch. That switch has no case for a non-static ref field used as a
ref-aliasing source, so `Cell` (i.e. `this.Cell`) fell through to the
same `IFieldReferenceOperation => Unknown` bucket used for ordinary field
*values* - even though IsCallMappedRefSource (used for the analogous
method-call case) already treats a ref field's instance recursively as
a valid mapped source.
That single Unknown then poisoned CopyTo's own effect summary (Write(Unknown)
instead of Write({Parameter(0), Receiver})), which in turn poisoned the
Join at CopyReceiverThenMutate's call site, overriding the otherwise-correct
Parameter(0) resolution from the later target.Set() call.
Added the missing case: a non-static ref field, read as an alias source,
recurses into its own instance's region instead of degrading to Unknown -
mirroring IsCallMappedRefSource's existing treatment of the same shape.
Verified: SharpProof.Effects.Test now only fails
ExceptionHandlersContributeEffectsOnlyWhenReachable (a separate, much
larger reachability-engine gap spanning ~65 assertions across dozens of
distinct C# constructs, explicitly deferred per user decision - not a
narrow fix like this one). SharpProof.Analyzer.Test remains 389/389, and
a full solution build succeeds with 0 warnings/errors.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
alexyorke
force-pushed
the
verifier-process-supervisor
branch
7 times, most recently
from
August 23, 2026 13:52
9f4d70c to
baad13c
Compare
alexyorke
force-pushed
the
verifier-process-supervisor
branch
from
August 23, 2026 14:20
baad13c to
78196c0
Compare
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.
Summary
SharpProof.BuildTasksverifier process supervisor (newProgram.cs,VerifierProcessSupervisor.cs) and extendRunVerifier.csmaster, ~12.3k insertions / 518 deletions across 101 filesTest plan
dotnet test) before merging🤖 Generated with Claude Code