From 0fb0aefc6d746c55e9ceaaff5d9e2d3a6116bb28 Mon Sep 17 00:00:00 2001 From: antonsynd <2648730+antonsynd@users.noreply.github.com> Date: Tue, 20 Oct 2026 22:06:22 -0400 Subject: [PATCH 01/11] test(property): an admitted program whose validator-order re-analysis fails is a recorded failure, not a skipped comparison; the fact asserts compared == admitted (refs #2288) Verify finding F1 (live cell): ValidatorOrderingPropertyTests returned null from ValidateWith on a re-analysis throw (`catch { return null; }`) or failure (the multi-line `if (!analysis.Success || ...)` that evaded the line-based scan), and the caller returned/continued, so a re-analysis that failed on every sample left the fact green with "0/30 programs compared". ValidateWith now reports why (`out failure`), the caller records it on a failure queue asserted empty, a throw propagates and fails the sample, and the fact asserts total > 0 and compared == total. mutation M1 (ValidateWith always returns null): broken -> red (1 failed: "30 admitted program(s) did not re-analyse clean ... reference run: mutation M1"), restored -> green (18 passed, filter ValidatorOrdering|JudgeSourceTests|Roster.YInjected). Commit state: ValidatorOrdering + PropertyOracleConformance + TypedGeneratorRoster + ProcessGlobalStateConformance 43/0/0 (measured). Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_017D8V5muKcTsUwCKAHghw1h --- .../ValidatorOrderingPropertyTests.cs | 61 +++++++++++-------- 1 file changed, 36 insertions(+), 25 deletions(-) diff --git a/src/Sharpy.Compiler.Tests/Properties/Semantic/ValidatorOrderingPropertyTests.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/ValidatorOrderingPropertyTests.cs index da41ecce8..96f2d8e22 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Semantic/ValidatorOrderingPropertyTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Semantic/ValidatorOrderingPropertyTests.cs @@ -49,6 +49,10 @@ public void ValidationDiagnostics_AreRegistrationOrderIndependent() { int total = 0; int compared = 0; + // An admitted sample whose re-analysis does not analyse clean is a RECORDED failure, never a + // skipped comparison (#2288): before, ValidateWith returned null and the caller returned, so a + // re-analysis that failed on every sample left the fact green with "0/30 programs compared". + var failures = new System.Collections.Concurrent.ConcurrentQueue(); // The canonical (Order-sorted) validator NAME sequence, used to assert that // AddValidator restores execution order regardless of registration order. Validator @@ -78,9 +82,13 @@ public void ValidationDiagnostics_AreRegistrationOrderIndependent() // fresh, deterministic semantic state (validators mutate SemanticInfo, so the // state must not be shared between runs). Returns null if the program does not // analyze cleanly. - var reference = ValidateWith(source, ValidationPipelineFactory.CreateDefault().Validators.ToList()); + var reference = ValidateWith(source, ValidationPipelineFactory.CreateDefault().Validators.ToList(), + out var referenceFailure); if (reference is null) + { + failures.Enqueue($"reference run: {referenceFailure}\n{source}"); return; + } // The shuffle RNG is seeded from CsCheck, so the seed CsCheck prints reproduces the // exact registration orders this case tried. It used to be source.GetHashCode(), @@ -110,9 +118,12 @@ public void ValidationDiagnostics_AreRegistrationOrderIndependent() Environment.NewLine + "Actual: " + string.Join(" -> ", executionNames)); } - var actual = ValidateWith(source, pipeline); + var actual = ValidateWith(source, pipeline, out var actualFailure); if (actual is null) - continue; // Analysis is deterministic, but be defensive. + { + failures.Enqueue($"shuffled trial {trial}: {actualFailure}\n{source}"); + return; + } if (!reference.SequenceEqual(actual)) { @@ -132,9 +143,14 @@ public void ValidationDiagnostics_AreRegistrationOrderIndependent() }, print: s => $"shuffle seed {s.shuffleSeed}{Environment.NewLine}" + Sharpy.Compiler.Pretty.Unparser.Unparse(s.module), iter: 30); _output.WriteLine(sink.Summary); - Assert.True(sink.Unexplained.Count == 0, sink.Report()); - _output.WriteLine("Validator registration ordering: " + compared + "/" + total + " programs compared"); + Assert.True(sink.Unexplained.Count == 0, sink.Report()); + Assert.True(failures.IsEmpty, + $"{failures.Count} admitted program(s) did not re-analyse clean, so their validator order was never " + + $"compared; the first:\n{failures.FirstOrDefault()}"); + Assert.True(total > 0, "No program was admitted — the lane compared nothing"); + Assert.True(compared == total, + $"{compared}/{total} admitted programs compared — every admitted program must be compared"); } private static void FisherYatesShuffle(IList list, Random rng) @@ -147,12 +163,12 @@ private static void FisherYatesShuffle(IList list, Random rng) } private static List? ValidateWith( - string source, IReadOnlyList validators) + string source, IReadOnlyList validators, out string? failure) { var pipeline = ValidationPipelineFactory.CreateMinimal(); foreach (var v in validators) pipeline.AddValidator(v); - return ValidateWith(source, pipeline); + return ValidateWith(source, pipeline, out failure); } /// @@ -161,31 +177,26 @@ private static void FisherYatesShuffle(IList list, Random rng) /// SemanticInfo), then runs the given pipeline against it using a fresh /// with an unbounded error budget so every validator runs. /// Returns the sorted set of distinct resulting diagnostics (keyed by code, position, and - /// message), or null if the program does not analyze cleanly. The distinct set is + /// message), or null with saying why when the program does not + /// analyze cleanly — the caller records that as a failure, never a skip (a throw propagates and + /// fails the sample). The distinct set is /// used because validators legitimately deduplicate against already-reported diagnostics, /// so the count of identical duplicates is not significant. /// - private static List? ValidateWith(string source, ValidationPipeline pipeline) + private static List? ValidateWith(string source, ValidationPipeline pipeline, out string? failure) { var logger = NullLogger.Instance; - CompilationResult analysis; - try - { - analysis = new Sharpy.Compiler.Compiler().Analyze(source, "validator_order_test.spy"); - } - catch - { + var analysis = new Sharpy.Compiler.Compiler().Analyze(source, "validator_order_test.spy"); + var errors = analysis.Diagnostics.GetErrors().Select(d => d.Code ?? "(no code)").Distinct().ToList(); + failure = errors.Count > 0 ? $"re-analysis drew [{string.Join(", ", errors)}]" + : !analysis.Success ? "re-analysis failed without an error code" + : analysis.Module is null ? "re-analysis produced no module" + : analysis.SymbolTable is null ? "re-analysis produced no symbol table" + : analysis.SemanticInfo is null ? "re-analysis produced no semantic info" + : null; + if (failure is not null) return null; - } - - if (!analysis.Success - || analysis.Module is null - || analysis.SymbolTable is null - || analysis.SemanticInfo is null) - { - return null; - } var symbolTable = analysis.SymbolTable!; var semanticInfo = analysis.SemanticInfo!; From 84f4b9f97c3c25c24522dbc1cd319d78328c83d7 Mon Sep 17 00:00:00 2001 From: antonsynd <2648730+antonsynd@users.noreply.github.com> Date: Tue, 20 Oct 2026 22:09:00 -0400 Subject: [PATCH 02/11] =?UTF-8?q?test(property):=20a=20swallowed=20throw?= =?UTF-8?q?=20in=20a=20property=20lane=20is=20a=20failure=20=E2=80=94=20th?= =?UTF-8?q?e=20NeverThrows=20lanes=20judge=20every=20raw=20sample=20for=20?= =?UTF-8?q?a=20throw=20or=20SPY0909,=20the=20span/async/determinism/CFG=20?= =?UTF-8?q?lanes=20stop=20catching,=20and=20the=20differential=20sweep's?= =?UTF-8?q?=20generated=20arm=20records=20what=20it=20refuses=20and=20must?= =?UTF-8?q?=20reach=20its=20target=20(refs=20#2288)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Verify finding F2 (the oracle matrix did not drain to one kind): - ClassInheritance/FunctionSemantics/TypedAnalyze `*_NeverThrowsInternalError` caught only InternalCompilerErrorException, which Analyze never lets escape (the last-chance handler records SPY0909), and swallowed every other exception: they could not fail. They now judge each raw sample through the new ErrorInjector.JudgeNoInternalError (null unless the analysis throws or records SPY0909; a refusal is allowed, the sample is unfiltered) via JudgeSamples, asserting Tested > 0 and no failure. - DiagnosticSpan x3 and Async `AsyncFunction_Deterministic` lose `catch { /* swallow */ }`; Determinism's Compile/CompileFull lose their throw-to-sentinel catches and TypedCompilation_ProducesIdenticalCSharp fails when an ADMITTED program produces no C# instead of skipping the comparison; CfgWellFormedness (same universe, same shape) loses its catch-all, so a throw from compile, re-parse or the CFG builder fails the sample (a refused random program is still skipped — the untyped generator's programs are not well typed). - DifferentialExecutionTests' generated arm (a GapDiscovery sweep, trait and fixed-size arm kept): a candidate Sharpy refuses or throws on is recorded on a RejectionSink through the new SemanticFilter.AdmitWellTyped (WellTypedProgram's admission rule for one sample, without the forced GC — the class is not in a serial collection), an admitted candidate whose re-parse fails or throws is a recorded failure, only the subset filter discards, and AssertGeneratedArmSound requires no unexplained rejection, no failure and Programs == Target. A new fact GeneratedArm_DropsNothingSilently_AndReachesItsTarget guards the arm without the CPython oracle (the sweep's fact returns early when python3 is absent). - ClassInheritance's super-call counter is renamed superCallsTested (an applicability counter, for the scanner's lower-bound rule in the next commit). mutation M7 (production, src/Sharpy.Compiler/Compiler.cs: throw at the start of Analyze and of Compile): broken -> red (12 failed of 12: the 3 NeverThrows, DiagnosticSpan x3, Determinism x3, CfgWellFormedness, Async determinism, GeneratedArm), restored -> green. mutation M8 (production, ControlFlowValidator.VisitFunctionDef throws on `main` -> SPY0909, no exception escapes): broken -> red (3 failed of 3 NeverThrows: "100/100 typed programs crashed the compiler ... SPY0909"); control: the BASE NeverThrows lanes (git show HEAD versions) under the same mutation -> green (3 passed) — the old lanes were vacuous; restored -> green. Commit state: the touched classes + DifferentialExecution (sweep included) + PropertyOracleConformance + TypedGeneratorRoster + ProcessGlobalStateConformance 73/0/0 (measured). Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_017D8V5muKcTsUwCKAHghw1h --- .../DifferentialExecutionTests.cs | 99 ++++++++--- .../Generators/Typed/ErrorInjector.cs | 30 ++++ .../Generators/Typed/SemanticFilter.cs | 11 +- .../Properties/Semantic/AsyncPropertyTests.cs | 36 ++-- .../CfgWellFormednessPropertyTests.cs | 162 ++++++++--------- .../Semantic/ClassInheritancePropertyTests.cs | 37 ++-- .../Semantic/DeterminismPropertyTests.cs | 40 ++--- .../Semantic/DiagnosticSpanPropertyTests.cs | 166 ++++++++---------- .../FunctionSemanticsPropertyTests.cs | 32 ++-- .../Semantic/TypedAnalyzePropertyTests.cs | 33 ++-- 10 files changed, 333 insertions(+), 313 deletions(-) diff --git a/src/Sharpy.Compiler.Tests/Properties/Differential/DifferentialExecutionTests.cs b/src/Sharpy.Compiler.Tests/Properties/Differential/DifferentialExecutionTests.cs index 348cd1b01..e15862274 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Differential/DifferentialExecutionTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Differential/DifferentialExecutionTests.cs @@ -337,7 +337,7 @@ private Corpus BuildCorpus(int limit) if (limit <= FullPool) { var full = Fixtures(int.MaxValue); - return Compose(handpicked, full, Generated(FullPoolGeneratedTarget)); + return Compose(handpicked, full, Generated(FullPoolGeneratedTarget).Programs); } // DIFF_EXEC_LIMIT=: a subsample for fast local iteration. Split the remaining budget @@ -349,7 +349,7 @@ private Corpus BuildCorpus(int limit) var pool = Fixtures(fixtureTarget); // Any fixture budget the pool could not fill rolls over to the generated arm. generatedTarget += Math.Max(0, fixtureTarget - pool.Selected.Count); - return Compose(handpicked, pool, Generated(generatedTarget)); + return Compose(handpicked, pool, Generated(generatedTarget).Programs); } private static Corpus Compose(List handpicked, FixturePool pool, List generated) @@ -987,12 +987,22 @@ void Exclude(string shape, string? name = null) /// print(expr) statements over int / str / bool / list results with fuel 1 (shallow enough /// that int arithmetic cannot overflow Sharpy's 32-bit int and masquerade as a divergence). /// Each candidate must compile in Sharpy and pass the subset filter. + /// Nothing is dropped silently (#2288): a candidate Sharpy refuses or throws on is recorded on + /// a through (the generated + /// lane's one admission rule), an admitted candidate whose re-parse fails or throws is a recorded + /// failure, and only the subset filter — a property of the ORACLE, not of the compiler — discards a + /// sample. turns any of them into a red, and the arm must reach + /// its target. Before, every one of those samples was a bare return and the 12-program target + /// was never checked. /// - private static List Generated(int target) + private static GeneratedArm Generated(int target) { var results = new List(); + var sink = new RejectionSink("DifferentialExecution.Generated"); + var failures = new List(); + int outsideSubset = 0; if (target <= 0) - return results; + return new GeneratedArm(results, target, sink, failures, outsideSubset); var env = TypeEnv.WithCollections; var types = new[] { "int", "str", "bool", "list[int]", "list[str]" }; @@ -1020,39 +1030,84 @@ select BuildGeneratedMain(xv, yv, sv, flagv, if (results.Count >= target) return; - string source; - try - { source = Sharpy.Compiler.Pretty.Unparser.Unparse(module); } - catch { return; } + // Gate 1: Sharpy accepts it (analysis-clean) — or the sink records why not. + if (!SemanticFilter.AdmitWellTyped(module, sink)) + return; + + var source = Sharpy.Compiler.Pretty.Unparser.Unparse(module); if (!seenSources.Add(source)) return; - // Gate 1: Sharpy accepts it (analysis-clean). + // Gate 2: whole tree is in the shared executable subset (reparse then filter). The program + // was just analysed clean, so a re-parse error or throw is a failure, not a skip. + Module reparsed; try { - var analysis = new Sharpy.Compiler.Compiler().Analyze(source, "gen_diff.spy"); - if (!analysis.Success) + var parser = new Sharpy.Compiler.Parser.Parser( + new Sharpy.Compiler.Lexer.Lexer(source).TokenizeAll()); + reparsed = parser.ParseModule(); + var parseErrors = parser.Diagnostics.GetErrors(); + if (parseErrors.Count > 0) + { + failures.Add($"an admitted program re-parses with [{string.Join(", ", parseErrors.Select(d => d.Code))}]:\n{source}"); return; + } + } + catch (Exception e) + { + failures.Add($"re-parsing an admitted program threw {e.GetType().Name}:\n{source}\n{e}"); + return; } - catch { return; } - // Gate 2: whole tree is in the shared executable subset (reparse then filter). - try + if (!ExecSubsetFilter.IsInSharedSubset(reparsed)) { - var parser = new Sharpy.Compiler.Parser.Parser( - new Sharpy.Compiler.Lexer.Lexer(source).TokenizeAll()); - var reparsed = parser.ParseModule(); - if (parser.Diagnostics.HasErrors || !ExecSubsetFilter.IsInSharedSubset(reparsed)) - return; + outsideSubset++; + return; } - catch { return; } results.Add(new Program($"generated::g{idx++:D4}", source)); - // threads:1 keeps this collection loop single-threaded (results/seenSources are not + // threads:1 keeps this collection loop single-threaded (results/seenSources/failures are not // concurrent); seed pins determinism. }, seed: GeneratedSeed, iter: Math.Max(target * 12L, 96L), threads: 1); - return results; + var arm = new GeneratedArm(results, target, sink, failures, outsideSubset); + AssertGeneratedArmSound(arm); + return arm; + } + + /// The generated arm's programs and what it discarded on the way (#2288). + private sealed record GeneratedArm( + List Programs, int Target, RejectionSink Sink, List Failures, int OutsideSubset) + { + public string Summary => + $"{Sink.Summary}; re-parse failures {Failures.Count}; outside the shared subset {OutsideSubset}; " + + $"programs {Programs.Count}/{Target}"; + } + + /// The generated arm dropped nothing silently and reached its target: no unexplained + /// rejection on the sink, no re-parse failure, and programs. + private static void AssertGeneratedArmSound(GeneratedArm arm) + { + Assert.True(arm.Sink.Unexplained.Count == 0, arm.Sink.Report()); + Assert.True(arm.Failures.Count == 0, + $"{arm.Failures.Count} admitted generated program(s) failed to re-parse; the first:\n{arm.Failures.FirstOrDefault()}"); + Assert.True(arm.Programs.Count == arm.Target, + $"The generated arm reached {arm.Programs.Count}/{arm.Target} programs ({arm.Summary}) — a sweep " + + "whose fuzz arm falls short compares fewer programs than it claims"); + } + + /// + /// The generated arm at its full-pool size, without the CPython oracle (the sweep's fact returns + /// early when python3 is absent, so this is the arm's guard on every machine): every candidate + /// is admitted, pinned, or outside the shared subset, and the arm reaches + /// programs. + /// + [Fact] + public void GeneratedArm_DropsNothingSilently_AndReachesItsTarget() + { + var arm = Generated(FullPoolGeneratedTarget); + Output.WriteLine(arm.Summary); + Assert.Equal(FullPoolGeneratedTarget, arm.Programs.Count); } // ----------------------------------------------------------------------------------------- // diff --git a/src/Sharpy.Compiler.Tests/Properties/Generators/Typed/ErrorInjector.cs b/src/Sharpy.Compiler.Tests/Properties/Generators/Typed/ErrorInjector.cs index ac3557802..6963cdbac 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Generators/Typed/ErrorInjector.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Generators/Typed/ErrorInjector.cs @@ -170,6 +170,36 @@ public sealed record KnownRedRefusal(string Issue, string Observed); } } + /// + /// The no-crash verdict for a RAW sample — the one a *NeverThrows* lane reads (#2288): + /// null when analysing neither throws nor records an internal compiler + /// error (SPY0909, the code the compiler's last-chance handlers turn an escaped exception into), + /// otherwise why not. A refusal is NOT a failure here — the sample is unfiltered — but no throw is + /// ever acceptable: before, the lanes caught only InternalCompilerErrorException (which + /// Analyze never lets escape: it records SPY0909) and swallowed every other exception, so + /// they could not fail. + /// + public static string? JudgeNoInternalError(string source, string label) + { + try + { + var (_, all) = AnalyseSingleFile(source); + var internalErrors = all.Where(d => d.Code == InternalCompilerErrorCode).ToList(); + return internalErrors.Count == 0 + ? null + : $"Raw {label} drew an internal compiler error ({InternalCompilerErrorCode}): " + + $"{internalErrors[0].Message}\n{source}"; + } + catch (Exception e) + { + return $"Raw {label} threw {e.GetType().Name} — the compiler must never throw:\n{source}\n{e}"; + } + } + + /// DiagnosticCodes.Infrastructure.InternalCompilerError, spelled literally (a + /// renumbering must stay a live mutation). + private const string InternalCompilerErrorCode = "SPY0909"; + /// What saw: samples judged, /// non-null verdicts, the first of them. public sealed record SampleVerdicts(int Tested, int Failures, string? First); diff --git a/src/Sharpy.Compiler.Tests/Properties/Generators/Typed/SemanticFilter.cs b/src/Sharpy.Compiler.Tests/Properties/Generators/Typed/SemanticFilter.cs index 7d8e13e58..39a3b7df2 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Generators/Typed/SemanticFilter.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Generators/Typed/SemanticFilter.cs @@ -26,7 +26,7 @@ public static Gen WellTypedProgram(Gen source, RejectionSink sin { try { - return Admit(sink, () => Sharpy.Compiler.Pretty.Unparser.Unparse(module), module, AnalyseSingleFile); + return AdmitWellTyped(module, sink); } finally { @@ -35,6 +35,15 @@ public static Gen WellTypedProgram(Gen source, RejectionSink sin } }); + /// + /// The admission rule of for ONE sample, without the forced GC — for a + /// lane that collects its own programs in a loop (the differential sweep's generated arm, which runs + /// in a parallel class): true when the unparsed Analyzes clean, + /// otherwise the sample is recorded on exactly as the filter records it. + /// + public static bool AdmitWellTyped(Module module, RejectionSink sink) => + Admit(sink, () => Sharpy.Compiler.Pretty.Unparser.Unparse(module), module, AnalyseSingleFile); + /// Samples whose unparsed source Compiles clean (front end and C# emit). public static Gen CompilableProgram(Gen source, RejectionSink sink) => source.Where(module => diff --git a/src/Sharpy.Compiler.Tests/Properties/Semantic/AsyncPropertyTests.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/AsyncPropertyTests.cs index d71638906..cef6d9380 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Semantic/AsyncPropertyTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Semantic/AsyncPropertyTests.cs @@ -82,31 +82,25 @@ public void AsyncFunction_Deterministic() { var source = Sharpy.Compiler.Pretty.Unparser.Unparse(module); - try - { - var compiler1 = new Sharpy.Compiler.Compiler(); - var result1 = compiler1.Analyze(source, "async_test.spy"); - - var compiler2 = new Sharpy.Compiler.Compiler(); - var result2 = compiler2.Analyze(source, "async_test.spy"); + // A throw fails the sample: it used to be swallowed (#2288). + var compiler1 = new Sharpy.Compiler.Compiler(); + var result1 = compiler1.Analyze(source, "async_test.spy"); - if (result1.Success != result2.Success) - { - lock (errors) - errors.Add($"Success differs: {result1.Success} vs {result2.Success}"); - } + var compiler2 = new Sharpy.Compiler.Compiler(); + var result2 = compiler2.Analyze(source, "async_test.spy"); - var diags1 = result1.Diagnostics.GetAll().Select(d => d.Code).OrderBy(c => c).ToList(); - var diags2 = result2.Diagnostics.GetAll().Select(d => d.Code).OrderBy(c => c).ToList(); - if (!diags1.SequenceEqual(diags2)) - { - lock (errors) - errors.Add($"Diagnostics differ: [{string.Join(",", diags1)}] vs [{string.Join(",", diags2)}]"); - } + if (result1.Success != result2.Success) + { + lock (errors) + errors.Add($"Success differs: {result1.Success} vs {result2.Success}"); } - catch + + var diags1 = result1.Diagnostics.GetAll().Select(d => d.Code).OrderBy(c => c).ToList(); + var diags2 = result2.Diagnostics.GetAll().Select(d => d.Code).OrderBy(c => c).ToList(); + if (!diags1.SequenceEqual(diags2)) { - // Swallow + lock (errors) + errors.Add($"Diagnostics differ: [{string.Join(",", diags1)}] vs [{string.Join(",", diags2)}]"); } }, print: m => Sharpy.Compiler.Pretty.Unparser.Unparse(m), iter: 50); diff --git a/src/Sharpy.Compiler.Tests/Properties/Semantic/CfgWellFormednessPropertyTests.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/CfgWellFormednessPropertyTests.cs index 5be8166ad..05d50f94b 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Semantic/CfgWellFormednessPropertyTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Semantic/CfgWellFormednessPropertyTests.cs @@ -26,9 +26,10 @@ public CfgWellFormednessPropertyTests(ITestOutputHelper output) /// the entry block is labeled "entry"; entry and exit blocks are members /// of the Blocks collection; every successor edge points to a block in the /// graph; the exit block has no successors; and statement counts are - /// non-negative. Invariant violations are surfaced as failures while - /// unrelated compilation/parse errors (expected for random programs) are - /// swallowed. + /// non-negative. A program the compiler refuses is skipped (the untyped + /// generator's programs are not well typed); a THROW anywhere — compile, + /// re-parse or CFG build — fails the sample: it used to be swallowed with the + /// refusals, so a crashing CFG builder passed (#2288). /// [Fact] public void CfgFromCompiledPrograms_SatisfiesStructuralInvariants() @@ -45,100 +46,87 @@ public void CfgFromCompiledPrograms_SatisfiesStructuralInvariants() Interlocked.Increment(ref total); var source = Sharpy.Compiler.Pretty.Unparser.Unparse(module); - try - { - var compiler = new Sharpy.Compiler.Compiler(); - var result = compiler.Compile(source, "cfg_test.spy"); - if (!result.Success) - return; - - // Re-parse to obtain FunctionDef AST nodes to feed the CFG builder. - var lexer = new Sharpy.Compiler.Lexer.Lexer(source); - var tokens = lexer.TokenizeAll(); - var parser = new Sharpy.Compiler.Parser.Parser(tokens); - var parsed = parser.ParseModule(); - - foreach (var stmt in parsed.Body) - { - if (stmt is not FunctionDef funcDef) - continue; - - var builder = new ControlFlowGraphBuilder(); - var cfg = builder.Build(funcDef); - - // Entry block exists and is labeled "entry". - if (cfg.Entry.Label != "entry") - throw new CfgInvariantException( - $"Entry block label is '{cfg.Entry.Label}', expected 'entry'"); + var compiler = new Sharpy.Compiler.Compiler(); + var result = compiler.Compile(source, "cfg_test.spy"); + if (!result.Success) + return; - // Exit block is labeled "exit". - if (cfg.Exit.Label != "exit") - throw new CfgInvariantException( - $"Exit block label is '{cfg.Exit.Label}', expected 'exit'"); + // Re-parse to obtain FunctionDef AST nodes to feed the CFG builder. + var lexer = new Sharpy.Compiler.Lexer.Lexer(source); + var tokens = lexer.TokenizeAll(); + var parser = new Sharpy.Compiler.Parser.Parser(tokens); + var parsed = parser.ParseModule(); - // Entry and Exit are members of Blocks. - if (!cfg.Blocks.Contains(cfg.Entry)) - throw new CfgInvariantException("Entry block not in Blocks collection"); - if (!cfg.Blocks.Contains(cfg.Exit)) - throw new CfgInvariantException("Exit block not in Blocks collection"); + foreach (var stmt in parsed.Body) + { + if (stmt is not FunctionDef funcDef) + continue; + + var builder = new ControlFlowGraphBuilder(); + var cfg = builder.Build(funcDef); + + // Entry block exists and is labeled "entry". + if (cfg.Entry.Label != "entry") + throw new CfgInvariantException( + $"Entry block label is '{cfg.Entry.Label}', expected 'entry'"); + + // Exit block is labeled "exit". + if (cfg.Exit.Label != "exit") + throw new CfgInvariantException( + $"Exit block label is '{cfg.Exit.Label}', expected 'exit'"); + + // Entry and Exit are members of Blocks. + if (!cfg.Blocks.Contains(cfg.Entry)) + throw new CfgInvariantException("Entry block not in Blocks collection"); + if (!cfg.Blocks.Contains(cfg.Exit)) + throw new CfgInvariantException("Exit block not in Blocks collection"); + + // Block IDs are unique. + var ids = new HashSet(); + foreach (var block in cfg.Blocks) + { + if (!ids.Add(block.Id)) + throw new CfgInvariantException($"Duplicate block id {block.Id}"); + } - // Block IDs are unique. - var ids = new HashSet(); - foreach (var block in cfg.Blocks) + // Every successor edge points to a block in the graph, and + // edges are symmetric (successor lists imply predecessor lists). + var blockSet = new HashSet(cfg.Blocks); + foreach (var block in cfg.Blocks) + { + foreach (var succ in block.Successors) { - if (!ids.Add(block.Id)) - throw new CfgInvariantException($"Duplicate block id {block.Id}"); + if (!blockSet.Contains(succ)) + throw new CfgInvariantException( + $"Block {block} has successor {succ} not in Blocks"); + if (!succ.Predecessors.Contains(block)) + throw new CfgInvariantException( + $"Successor {succ} of {block} is missing matching predecessor edge"); } + } - // Every successor edge points to a block in the graph, and - // edges are symmetric (successor lists imply predecessor lists). - var blockSet = new HashSet(cfg.Blocks); - foreach (var block in cfg.Blocks) - { - foreach (var succ in block.Successors) - { - if (!blockSet.Contains(succ)) - throw new CfgInvariantException( - $"Block {block} has successor {succ} not in Blocks"); - if (!succ.Predecessors.Contains(block)) - throw new CfgInvariantException( - $"Successor {succ} of {block} is missing matching predecessor edge"); - } - } + // Exit has no successors. + if (cfg.Exit.Successors.Count != 0) + throw new CfgInvariantException( + $"Exit block has {cfg.Exit.Successors.Count} successors"); - // Exit has no successors. - if (cfg.Exit.Successors.Count != 0) + // Statement counts are non-negative (sanity). + foreach (var block in cfg.Blocks) + { + if (block.Statements.Count < 0) throw new CfgInvariantException( - $"Exit block has {cfg.Exit.Successors.Count} successors"); - - // Statement counts are non-negative (sanity). - foreach (var block in cfg.Blocks) - { - if (block.Statements.Count < 0) - throw new CfgInvariantException( - $"Block {block} has negative statement count"); - } - - // Unreachable-block detection must return a subset of Blocks. - foreach (var unreachable in cfg.FindUnreachableBlocks()) - { - if (!blockSet.Contains(unreachable)) - throw new CfgInvariantException( - "FindUnreachableBlocks returned a block not in Blocks"); - } + $"Block {block} has negative statement count"); + } - Interlocked.Increment(ref cfgsChecked); + // Unreachable-block detection must return a subset of Blocks. + foreach (var unreachable in cfg.FindUnreachableBlocks()) + { + if (!blockSet.Contains(unreachable)) + throw new CfgInvariantException( + "FindUnreachableBlocks returned a block not in Blocks"); } - } - catch (CfgInvariantException) - { - // Real invariant violation — propagate so the property fails. - throw; - } - catch (Exception) - { - // Compilation/parse/runtime failures are expected for random - // programs and are not what this property is testing. + + Interlocked.Increment(ref cfgsChecked); } }, print: m => Sharpy.Compiler.Pretty.Unparser.Unparse(m), iter: 50); diff --git a/src/Sharpy.Compiler.Tests/Properties/Semantic/ClassInheritancePropertyTests.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/ClassInheritancePropertyTests.cs index ba31d022a..f7da5fdc2 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Semantic/ClassInheritancePropertyTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Semantic/ClassInheritancePropertyTests.cs @@ -100,7 +100,7 @@ public void AbstractMethod_MustBeOverridden() public void SuperCall_ResolvesCorrectly() { var sink = new RejectionSink("ClassInheritance.SuperCall_ResolvesCorrectly"); - int withSuper = 0; + int superCallsTested = 0; SemanticFilter.WellTypedProgram(GenClasses.ModuleWithClasses(TypeEnv.Default, fuel: 2), sink) .Sample(module => @@ -109,40 +109,29 @@ public void SuperCall_ResolvesCorrectly() if (!source.Contains("super().__init__")) return; - Interlocked.Increment(ref withSuper); + Interlocked.Increment(ref superCallsTested); var result = new Sharpy.Compiler.Compiler().Analyze(source, "class_test.spy"); if (result.SemanticInfo == null) throw new Exception($"An admitted super() program has no semantic info:\n{source}"); }, print: m => Sharpy.Compiler.Pretty.Unparser.Unparse(m), iter: 50); _output.WriteLine(sink.Summary); - _output.WriteLine($"Super call resolution: {withSuper} admitted programs call super().__init__"); + _output.WriteLine($"Super call resolution: {superCallsTested} admitted programs call super().__init__"); Assert.True(sink.Unexplained.Count == 0, sink.Report()); - Assert.True(withSuper >= 1, "No sampled class program calls super().__init__ — the lane is vacuous"); + Assert.True(superCallsTested >= 1, "No sampled class program calls super().__init__ — the lane is vacuous"); } + /// Every RAW class program analyses without a throw or an internal compiler error + /// (); a refusal is allowed — the sample is + /// unfiltered. Before #2288 the lane swallowed every exception but one Analyze never throws. [Fact] public void ModuleWithClasses_NeverThrowsInternalError() { - GenClasses.ModuleWithClasses(TypeEnv.Default, fuel: 2) - .Sample(module => - { - var source = Sharpy.Compiler.Pretty.Unparser.Unparse(module); - - try - { - var compiler = new Sharpy.Compiler.Compiler(); - compiler.Analyze(source, "class_test.spy"); - } - catch (Sharpy.Compiler.Diagnostics.InternalCompilerErrorException ex) - { - throw new Exception( - $"InternalCompilerErrorException on class program:\n{source}\n{ex.Message}"); - } - catch - { - // Other exceptions are acceptable - } - }, print: m => Sharpy.Compiler.Pretty.Unparser.Unparse(m), iter: 50); + var verdicts = ErrorInjector.JudgeSamples(GenClasses.ModuleWithClasses(TypeEnv.Default, fuel: 2), + source => ErrorInjector.JudgeNoInternalError(source, "class program"), iter: 50); + _output.WriteLine($"Class programs: {verdicts.Tested - verdicts.Failures}/{verdicts.Tested} analysed without an internal error"); + Assert.True(verdicts.Tested > 0, "No class programs were sampled"); + Assert.True(verdicts.First is null, + $"{verdicts.Failures}/{verdicts.Tested} class programs crashed the compiler; the first:\n{verdicts.First}"); } } diff --git a/src/Sharpy.Compiler.Tests/Properties/Semantic/DeterminismPropertyTests.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/DeterminismPropertyTests.cs index f2d0362db..e3525b42f 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Semantic/DeterminismPropertyTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Semantic/DeterminismPropertyTests.cs @@ -92,8 +92,16 @@ public void TypedCompilation_ProducesIdenticalCSharp() var result1 = CompileFull(source); var result2 = CompileFull(source); - if (result1.csharp != null && result2.csharp != null && - result1.csharp != result2.csharp) + // The filter admitted the sample, so both runs must produce C# — a run without it (a + // throw or a refusal) is a failure, not a skipped comparison (#2288). + if (result1.csharp is null || result2.csharp is null) + { + throw new Exception( + $"An admitted program produced no C# (run 1 success {result1.success}, run 2 success " + + $"{result2.success}):\n{source}"); + } + + if (result1.csharp != result2.csharp) { throw new Exception( $"Generated C# differs between runs:\n{source}"); @@ -103,31 +111,19 @@ public void TypedCompilation_ProducesIdenticalCSharp() Assert.True(sink.Unexplained.Count == 0, sink.Report()); } + // A throw propagates and fails the sample: these used to return a sentinel, so two runs that + // both threw compared equal and an admitted program that threw was never compared (#2288). private static (bool success, int diagCount) Compile(string source) { - try - { - var compiler = new Sharpy.Compiler.Compiler(); - var result = compiler.Compile(source, "test.spy"); - return (result.Success, result.Diagnostics?.ErrorCount ?? 0); - } - catch - { - return (false, -1); - } + var compiler = new Sharpy.Compiler.Compiler(); + var result = compiler.Compile(source, "test.spy"); + return (result.Success, result.Diagnostics?.ErrorCount ?? 0); } private static (bool success, List diagnostics, string? csharp) CompileFull(string source) { - try - { - var compiler = new Sharpy.Compiler.Compiler(); - var result = compiler.Compile(source, "test.spy"); - return (result.Success, result.Diagnostics?.GetAll().ToList() ?? new(), result.GeneratedCSharpCode); - } - catch - { - return (false, new(), null); - } + var compiler = new Sharpy.Compiler.Compiler(); + var result = compiler.Compile(source, "test.spy"); + return (result.Success, result.Diagnostics?.GetAll().ToList() ?? new(), result.GeneratedCSharpCode); } } diff --git a/src/Sharpy.Compiler.Tests/Properties/Semantic/DiagnosticSpanPropertyTests.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/DiagnosticSpanPropertyTests.cs index 2ad65c897..215ce17e5 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Semantic/DiagnosticSpanPropertyTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Semantic/DiagnosticSpanPropertyTests.cs @@ -34,57 +34,51 @@ public void AllDiagnosticSpans_AreWithinSourceBounds() { var source = Sharpy.Compiler.Pretty.Unparser.Unparse(module); - try - { - var compiler = new Sharpy.Compiler.Compiler(); - var result = compiler.Analyze(source, "span_test.spy"); + // A throw fails the sample: it used to be swallowed, so a crash could hide a bad span (#2288). + var compiler = new Sharpy.Compiler.Compiler(); + var result = compiler.Analyze(source, "span_test.spy"); - var sourceLineCount = source.Split('\n').Length; + var sourceLineCount = source.Split('\n').Length; - foreach (var diag in result.Diagnostics.GetAll()) + foreach (var diag in result.Diagnostics.GetAll()) + { + if (diag.Span.HasValue) { - if (diag.Span.HasValue) + var span = diag.Span.Value; + if (span.Start < 0 || span.End > source.Length || span.Start > span.End) { - var span = diag.Span.Value; - if (span.Start < 0 || span.End > source.Length || span.Start > span.End) - { - lock (errors) - errors.Add( - $"Span out of bounds: {span} for source length {source.Length}, " + - $"diagnostic {diag.Code}: {diag.Message}\nSource:\n{source}"); - } + lock (errors) + errors.Add( + $"Span out of bounds: {span} for source length {source.Length}, " + + $"diagnostic {diag.Code}: {diag.Message}\nSource:\n{source}"); } + } - if (diag.Line.HasValue) + if (diag.Line.HasValue) + { + if (diag.Line.Value < 1) { - if (diag.Line.Value < 1) - { - lock (errors) - errors.Add( - $"Line {diag.Line.Value} is less than 1 (1-based), " + - $"diagnostic {diag.Code}: {diag.Message}\nSource:\n{source}"); - } - else if (diag.Line.Value > sourceLineCount) - { - lock (errors) - errors.Add( - $"Line {diag.Line.Value} exceeds source line count {sourceLineCount}, " + - $"diagnostic {diag.Code}: {diag.Message}\nSource:\n{source}"); - } + lock (errors) + errors.Add( + $"Line {diag.Line.Value} is less than 1 (1-based), " + + $"diagnostic {diag.Code}: {diag.Message}\nSource:\n{source}"); } - - if (diag.Column.HasValue && diag.Column.Value < 0) + else if (diag.Line.Value > sourceLineCount) { lock (errors) errors.Add( - $"Column {diag.Column.Value} is negative (0-based), " + + $"Line {diag.Line.Value} exceeds source line count {sourceLineCount}, " + $"diagnostic {diag.Code}: {diag.Message}\nSource:\n{source}"); } } - } - catch - { - // Swallow internal errors — focus on span validity, not crashes + + if (diag.Column.HasValue && diag.Column.Value < 0) + { + lock (errors) + errors.Add( + $"Column {diag.Column.Value} is negative (0-based), " + + $"diagnostic {diag.Code}: {diag.Message}\nSource:\n{source}"); + } } }, print: m => Sharpy.Compiler.Pretty.Unparser.Unparse(m), iter: 100); @@ -105,30 +99,24 @@ public void ErrorDiagnosticSpans_HaveNonNegativeLength() { var source = Sharpy.Compiler.Pretty.Unparser.Unparse(module); - try - { - var compiler = new Sharpy.Compiler.Compiler(); - var result = compiler.Analyze(source, "span_test.spy"); + // A throw fails the sample: it used to be swallowed, so a crash could hide a bad span (#2288). + var compiler = new Sharpy.Compiler.Compiler(); + var result = compiler.Analyze(source, "span_test.spy"); - foreach (var diag in result.Diagnostics.GetAll()) + foreach (var diag in result.Diagnostics.GetAll()) + { + if (diag.Severity == CompilerDiagnosticSeverity.Error && diag.Span.HasValue) { - if (diag.Severity == CompilerDiagnosticSeverity.Error && diag.Span.HasValue) + var span = diag.Span.Value; + if (span.Length < 0) { - var span = diag.Span.Value; - if (span.Length < 0) - { - lock (errors) - errors.Add( - $"Error diagnostic has negative-length span: {span}, " + - $"diagnostic {diag.Code}: {diag.Message}\nSource:\n{source}"); - } + lock (errors) + errors.Add( + $"Error diagnostic has negative-length span: {span}, " + + $"diagnostic {diag.Code}: {diag.Message}\nSource:\n{source}"); } } } - catch - { - // Swallow internal errors — focus on span validity, not crashes - } }, print: m => Sharpy.Compiler.Pretty.Unparser.Unparse(m), iter: 100); _output.WriteLine($"Error diagnostic span length: {errors.Count} violations found"); @@ -164,57 +152,51 @@ public void TypedPrograms_DiagnosticSpans_AreWithinSourceBounds() Interlocked.Increment(ref injected); var source = Sharpy.Compiler.Pretty.Unparser.Unparse(injection.Mutated); - try - { - var compiler = new Sharpy.Compiler.Compiler(); - var result = compiler.Analyze(source, "span_test.spy"); + // A throw fails the sample: it used to be swallowed, so a crash could hide a bad span (#2288). + var compiler = new Sharpy.Compiler.Compiler(); + var result = compiler.Analyze(source, "span_test.spy"); - var sourceLineCount = source.Split('\n').Length; + var sourceLineCount = source.Split('\n').Length; - foreach (var diag in result.Diagnostics.GetAll()) + foreach (var diag in result.Diagnostics.GetAll()) + { + if (diag.Span.HasValue) { - if (diag.Span.HasValue) + var span = diag.Span.Value; + if (span.Start < 0 || span.End > source.Length || span.Start > span.End) { - var span = diag.Span.Value; - if (span.Start < 0 || span.End > source.Length || span.Start > span.End) - { - lock (errors) - errors.Add( - $"Span out of bounds: {span} for source length {source.Length}, " + - $"diagnostic {diag.Code}: {diag.Message}\nSource:\n{source}"); - } + lock (errors) + errors.Add( + $"Span out of bounds: {span} for source length {source.Length}, " + + $"diagnostic {diag.Code}: {diag.Message}\nSource:\n{source}"); } + } - if (diag.Line.HasValue) + if (diag.Line.HasValue) + { + if (diag.Line.Value < 1) { - if (diag.Line.Value < 1) - { - lock (errors) - errors.Add( - $"Line {diag.Line.Value} is less than 1 (1-based), " + - $"diagnostic {diag.Code}: {diag.Message}\nSource:\n{source}"); - } - else if (diag.Line.Value > sourceLineCount) - { - lock (errors) - errors.Add( - $"Line {diag.Line.Value} exceeds source line count {sourceLineCount}, " + - $"diagnostic {diag.Code}: {diag.Message}\nSource:\n{source}"); - } + lock (errors) + errors.Add( + $"Line {diag.Line.Value} is less than 1 (1-based), " + + $"diagnostic {diag.Code}: {diag.Message}\nSource:\n{source}"); } - - if (diag.Column.HasValue && diag.Column.Value < 0) + else if (diag.Line.Value > sourceLineCount) { lock (errors) errors.Add( - $"Column {diag.Column.Value} is negative (0-based), " + + $"Line {diag.Line.Value} exceeds source line count {sourceLineCount}, " + $"diagnostic {diag.Code}: {diag.Message}\nSource:\n{source}"); } } - } - catch - { - // Swallow internal errors — focus on span validity, not crashes + + if (diag.Column.HasValue && diag.Column.Value < 0) + { + lock (errors) + errors.Add( + $"Column {diag.Column.Value} is negative (0-based), " + + $"diagnostic {diag.Code}: {diag.Message}\nSource:\n{source}"); + } } } }, print: m => Sharpy.Compiler.Pretty.Unparser.Unparse(m), iter: 30); diff --git a/src/Sharpy.Compiler.Tests/Properties/Semantic/FunctionSemanticsPropertyTests.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/FunctionSemanticsPropertyTests.cs index 935a15565..14de621dd 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Semantic/FunctionSemanticsPropertyTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Semantic/FunctionSemanticsPropertyTests.cs @@ -136,29 +136,19 @@ public void FunctionOverload_DispatchesCorrectly() Assert.True(sink.Unexplained.Count == 0, sink.Report()); } + /// Every RAW function program analyses without a throw or an internal compiler error + /// (); a refusal is allowed — the sample is + /// unfiltered. Before #2288 the lane swallowed every exception but one Analyze never throws. [Fact] public void ModuleWithFunctions_NeverThrowsInternalError() { - Gen.OneOfConst("int", "str", "bool").SelectMany(type => - GenFunctions.ModuleWithFunctions(TypeEnv.WithFunctions, type, fuel: 2)) - .Sample(module => - { - var source = Sharpy.Compiler.Pretty.Unparser.Unparse(module); - - try - { - var compiler = new Sharpy.Compiler.Compiler(); - compiler.Analyze(source, "func_test.spy"); - } - catch (Sharpy.Compiler.Diagnostics.InternalCompilerErrorException ex) - { - throw new Exception( - $"InternalCompilerErrorException on function program:\n{source}\n{ex.Message}"); - } - catch - { - // Other exceptions are acceptable - } - }, print: m => Sharpy.Compiler.Pretty.Unparser.Unparse(m), iter: 50); + var verdicts = ErrorInjector.JudgeSamples( + Gen.OneOfConst("int", "str", "bool").SelectMany(type => + GenFunctions.ModuleWithFunctions(TypeEnv.WithFunctions, type, fuel: 2)), + source => ErrorInjector.JudgeNoInternalError(source, "function program"), iter: 50); + _output.WriteLine($"Function programs: {verdicts.Tested - verdicts.Failures}/{verdicts.Tested} analysed without an internal error"); + Assert.True(verdicts.Tested > 0, "No function programs were sampled"); + Assert.True(verdicts.First is null, + $"{verdicts.Failures}/{verdicts.Tested} function programs crashed the compiler; the first:\n{verdicts.First}"); } } diff --git a/src/Sharpy.Compiler.Tests/Properties/Semantic/TypedAnalyzePropertyTests.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/TypedAnalyzePropertyTests.cs index 9ed295c4b..8c924e542 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Semantic/TypedAnalyzePropertyTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Semantic/TypedAnalyzePropertyTests.cs @@ -76,31 +76,18 @@ public void FilteredTypedProgram_AnalyzesClean() _output.WriteLine($"Filtered typed analysis: {count} programs all analyzed clean"); } + /// Every RAW typed program analyses without a throw or an internal compiler error + /// (); a refusal is allowed — the sample is + /// unfiltered. Before #2288 the lane swallowed every exception but one Analyze never throws. [Fact] public void TypedProgram_NeverThrowsInternalError() { - Gen.OneOfConst("int", "str", "bool").SelectMany(type => - { - var env = new TypeEnv(); - return GenTyped.TypedProgram(env, type, fuel: 3); - }).Sample(module => - { - var source = Sharpy.Compiler.Pretty.Unparser.Unparse(module); - - try - { - var compiler = new Sharpy.Compiler.Compiler(); - compiler.Analyze(source, "typed_test.spy"); - } - catch (Sharpy.Compiler.Diagnostics.InternalCompilerErrorException ex) - { - throw new Exception( - $"InternalCompilerErrorException on typed program:\n{source}\n{ex.Message}"); - } - catch - { - // Other exceptions are acceptable for generated code - } - }, print: m => Sharpy.Compiler.Pretty.Unparser.Unparse(m), iter: 100); + var verdicts = ErrorInjector.JudgeSamples( + Gen.OneOfConst("int", "str", "bool").SelectMany(type => GenTyped.TypedProgram(new TypeEnv(), type, fuel: 3)), + source => ErrorInjector.JudgeNoInternalError(source, "typed program"), iter: 100); + _output.WriteLine($"Typed programs: {verdicts.Tested - verdicts.Failures}/{verdicts.Tested} analysed without an internal error"); + Assert.True(verdicts.Tested > 0, "No typed programs were sampled"); + Assert.True(verdicts.First is null, + $"{verdicts.Failures}/{verdicts.Tested} typed programs crashed the compiler; the first:\n{verdicts.First}"); } } From 5c6a89f6cde73241f4db767f8bf72b2d3eb1b965 Mon Sep 17 00:00:00 2001 From: antonsynd <2648730+antonsynd@users.noreply.github.com> Date: Tue, 20 Oct 2026 22:10:57 -0400 Subject: [PATCH 03/11] =?UTF-8?q?test(property):=20the=20#2212=20explicit-?= =?UTF-8?q?instantiation=20pin=20is=20spelled=20`new=20KnownRedRefusal("#2?= =?UTF-8?q?212",=20=E2=80=A6)`=20so=20the=20issue-state=20gate=20reads=20i?= =?UTF-8?q?ts=20cite;=20the=20JudgeSource=20probe=20pin=20cites=20no=20iss?= =?UTF-8?q?ue=20(refs=20#2288,=20refs=20#2212)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Verify finding F5: ErrorInjector's ExplicitInstantiationConstraintPin was target-typed (`new("#2212", …)`), invisible to KNOWNRED_CELL_RE (`new\s+\w*KnownRed\w*\s*\(\s*"#?(\d+)"`), so #2212 closing without the pin draining would leave /push green. JudgeSourceTests' probe pin cited "#2288" (also target-typed, invisible), which would read as a stale cite once #2288 closes; it is "probe-pin" now — no `#`, never a cite. Gate rows (allowlist_issue_state.scan over the two files): at the base, 2 rows (the two #2143 pins); now 3 — `ErrorInjector.cs:722 [2212]` added; JudgeSourceTests none either way. mutation M-H6 (the pin's cite -> "#2250", a CLOSED issue): broken -> red (`python3 build_tools/allowlist_issue_state.py --paths ErrorInjector.cs` exit 1: "ErrorInjector.cs:722 ... → #2250 CLOSED"), restored -> green (exit 0). Commit state: JudgeSourceTests + ErrorCompleteness + PropertyOracleConformance 37/0/0 (measured); issue-state gate over ErrorInjector/JudgeSourceTests/KnownGeneratorPins exit 0. Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_017D8V5muKcTsUwCKAHghw1h --- .../Properties/Generators/Typed/ErrorInjector.cs | 2 +- .../Properties/Semantic/JudgeSourceTests.cs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Sharpy.Compiler.Tests/Properties/Generators/Typed/ErrorInjector.cs b/src/Sharpy.Compiler.Tests/Properties/Generators/Typed/ErrorInjector.cs index 6963cdbac..def0e5168 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Generators/Typed/ErrorInjector.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Generators/Typed/ErrorInjector.cs @@ -719,7 +719,7 @@ private static Expression ReplaceNestedCall(Expression expr, FunctionCall target return null; } - private static readonly KnownRedRefusal ExplicitInstantiationConstraintPin = new("#2212", + private static readonly KnownRedRefusal ExplicitInstantiationConstraintPin = new KnownRedRefusal("#2212", "analyses clean; run is SPY0908 CS0311 — a violated constraint at an explicit instantiation is refused by Roslyn, not Sharpy"); private const string PlainClassName = "Plain"; diff --git a/src/Sharpy.Compiler.Tests/Properties/Semantic/JudgeSourceTests.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/JudgeSourceTests.cs index 985d9fe84..7bddd51df 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Semantic/JudgeSourceTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Semantic/JudgeSourceTests.cs @@ -51,7 +51,7 @@ def main(): """; private static readonly ErrorInjector.KnownRedRefusal Pin = - new("#2288", "probe pin for the JudgeSource arms — never a real cell"); + new("probe-pin", "probe pin for the JudgeSource arms — never a real cell, so it cites no issue"); // (a) the warning arm accepts exactly one warning of the code with no error. [Fact] From 0a0af5b058c1392023a59165cac05dbb6fe2e81f Mon Sep 17 00:00:00 2001 From: antonsynd <2648730+antonsynd@users.noreply.github.com> Date: Tue, 20 Oct 2026 22:11:52 -0400 Subject: [PATCH 04/11] test(property): the JudgeSource warning arm requires exactly ONE warning diagnostic carrying the code and no error, not one distinct warning code (refs #2288) Verify finding F6 / plan Design Decision 6 ("exactly one diagnostic of the expected severity with the expected code, and no error"): JudgeDiagnostics compared DISTINCT warning codes, so two SPY0463 warnings (two broken facts) collapsed to one code and passed. The arm now counts warning diagnostics (`warningDiagnostics == 1`) beside the distinct-code check; the refusal message prints the count. Two JudgeSourceTests cells: two non-exhaustive matches -> refused ("warnings [SPY0463] (2 warning diagnostic(s))"); the warning beside an unrelated SPY0450 (a statement after `return`) -> refused (already refused before, now pinned). Measured first that the two warning lanes carry exactly one such diagnostic per sample under the stricter arm: MatchNonExhaustive 50/50 drew SPY0463, UnusedImportProgram 20/20 drew warning SPY0452 (PatternMatch/ImportResolution green). mutation M2 (`warningDiagnostics == 1` -> `>= 1`, i.e. one distinct code again): broken -> red (1 failed: WarningArm_TwoOfTheExpectedWarning_IsRefused), restored -> green. Commit state: JudgeSourceTests + PatternMatch + ImportResolution + PropertyOracleConformance 27/0/0 (measured). Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_017D8V5muKcTsUwCKAHghw1h --- .../Generators/Typed/ErrorInjector.cs | 19 ++++--- .../Properties/Semantic/JudgeSourceTests.cs | 51 +++++++++++++++++++ 2 files changed, 63 insertions(+), 7 deletions(-) diff --git a/src/Sharpy.Compiler.Tests/Properties/Generators/Typed/ErrorInjector.cs b/src/Sharpy.Compiler.Tests/Properties/Generators/Typed/ErrorInjector.cs index def0e5168..cf0dec61b 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Generators/Typed/ErrorInjector.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Generators/Typed/ErrorInjector.cs @@ -47,10 +47,11 @@ public sealed record KnownRedRefusal(string Issue, string Observed); /// /// Error: the distinct error codes are exactly [] /// (warnings are not read). Pinned: no error at all. - /// Warning: the distinct warning codes are exactly [] - /// AND there is no error — a warning lane whose program is also refused proves nothing about the - /// warning. Pinned: no error, and no warning of the code (no warning at all when the code is - /// null). + /// Warning: exactly ONE warning DIAGNOSTIC, carrying , AND no + /// error — a warning lane whose program is also refused proves nothing about the warning, and two + /// warnings of the code are two broken facts, not the one the injection made (P63 Design Decision + /// 6: "exactly one diagnostic of the expected severity"). Pinned: no error, and no warning of the + /// code (no warning at all when the code is null). /// /// Expected codes are literal strings at the call site, never DiagnosticCodes constants — /// a renumbering mutation must stay live. @@ -100,11 +101,13 @@ public sealed record KnownRedRefusal(string Issue, string Observed); var source = sourceForMessage; List errors; List warnings; + int warningDiagnostics; try { var (success, all) = analyse(); errors = DistinctCodes(all.Where(d => d.IsError)); warnings = DistinctCodes(all.Where(d => d.IsWarning)); + warningDiagnostics = all.Count(d => d.IsWarning); if (!success && errors.Count == 0) return $"Injected {label} failed analysis without an error code:\n{source}"; } @@ -116,7 +119,9 @@ public sealed record KnownRedRefusal(string Issue, string Observed); var isWarning = severity == CompilerDiagnosticSeverity.Warning; // The arm's own codes: errors on the error arm, warnings on the warning arm. var drew = Describe(isWarning ? warnings : errors); - var drewAll = isWarning ? $"errors [{Describe(errors)}], warnings [{drew}]" : $"[{drew}]"; + var drewAll = isWarning + ? $"errors [{Describe(errors)}], warnings [{drew}] ({warningDiagnostics} warning diagnostic(s))" + : $"[{drew}]"; if (pin is not null) { @@ -135,9 +140,9 @@ public sealed record KnownRedRefusal(string Issue, string Observed); ?? throw new InvalidOperationException($"Injection {label} has neither an expected code nor a KnownRed pin"); if (isWarning) { - return warnings is [var onlyWarning] && onlyWarning == expected && errors.Count == 0 + return warningDiagnostics == 1 && warnings is [var onlyWarning] && onlyWarning == expected && errors.Count == 0 ? null - : $"Injected {label} must draw exactly warning {expected} and no error, drew {drewAll}:\n{source}"; + : $"Injected {label} must draw exactly one warning, {expected}, and no error, drew {drewAll}:\n{source}"; } return errors is [var only] && only == expected diff --git a/src/Sharpy.Compiler.Tests/Properties/Semantic/JudgeSourceTests.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/JudgeSourceTests.cs index 7bddd51df..36a6a96a2 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Semantic/JudgeSourceTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Semantic/JudgeSourceTests.cs @@ -38,6 +38,36 @@ def main(): f(True) """; + // Two match statements on bool, each missing a case: two SPY0463 warnings, no error. + private const string TwoNonExhaustiveMatches = """ + def f(x: bool) -> None: + match x: + case True: + print("yes") + + def g(x: bool) -> None: + match x: + case False: + print("no") + + def main(): + f(True) + g(False) + """; + + // The warning beside an unrelated one (SPY0450, a statement after `return`): no error. + private const string NonExhaustiveMatchAndUnreachable = """ + def f(x: bool) -> None: + match x: + case True: + print("yes") + + def main(): + f(True) + return + print("never") + """; + private const string ErrorProgram = """ def main(): let n: int = "x" @@ -71,6 +101,27 @@ public void WarningArm_ExpectedWarningBesideAnError_IsRefused() Assert.Contains("errors [SPY0220], warnings [SPY0463]", failure); } + // (a) exactly ONE warning diagnostic (P63 Design Decision 6): two non-exhaustive matches are two + // SPY0463 warnings — one distinct code, but two broken facts, not the one the injection made. + [Fact] + public void WarningArm_TwoOfTheExpectedWarning_IsRefused() + { + var failure = ErrorInjector.JudgeSource( + TwoNonExhaustiveMatches, "SPY0463", CompilerDiagnosticSeverity.Warning, null, "match statement"); + Assert.NotNull(failure); + Assert.Contains("errors [nothing], warnings [SPY0463] (2 warning diagnostic(s))", failure); + } + + // (a) an unrelated warning beside the expected one is not a catch either. + [Fact] + public void WarningArm_ExpectedWarningBesideAnUnrelatedWarning_IsRefused() + { + var failure = ErrorInjector.JudgeSource( + NonExhaustiveMatchAndUnreachable, "SPY0463", CompilerDiagnosticSeverity.Warning, null, "match statement"); + Assert.NotNull(failure); + Assert.Contains("errors [nothing], warnings [SPY0450, SPY0463] (2 warning diagnostic(s))", failure); + } + // (b) the error arm never reads warnings: the warning program drew no error. [Fact] public void ErrorArm_WarningOnlyProgram_DrewNothing() From 31c783e0fbceddc53dd48580d9a451345362affb Mon Sep 17 00:00:00 2001 From: antonsynd <2648730+antonsynd@users.noreply.github.com> Date: Tue, 20 Oct 2026 22:12:45 -0400 Subject: [PATCH 05/11] =?UTF-8?q?test(roster):=20every=20roster=20lane=20i?= =?UTF-8?q?s=20tied=20to=20the=20property=20that=20sustains=20it=20?= =?UTF-8?q?=E2=80=94=20a=20YInjected=20row=20to=20a=20refusal=20lane=20nam?= =?UTF-8?q?ing=20its=20member=20and=20code,=20a=20Y=20row's=20member=20to?= =?UTF-8?q?=20an=20acceptance=20verdict,=20a=20Y=20label=20to=20the=20memb?= =?UTF-8?q?er=20its=20generator=20calls=20(refs=20#2288)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Verify finding F3: the roster's lane claims were a hand model checked only for member resolution and `^SPY\d{4}$`; a code, a deleted soundness fact or a label/lambda mismatch drifted green. PropertySourceIndex (new, Roslyn) indexes every method of Properties/** outside the roster and Generators/Typed/ (its X.Y references, string literals, same-file calls and their closure). Three facts: (a) YInjected_RowsAreBackedByTheirRefusalProperty — a generator-member row needs a property method naming the member AND the code literal in ONE body whose closure names CompilerDiagnosticSeverity. and reaches ErrorInjector.Judge/JudgeSource/ JudgeProject; an ErrorInjector row needs the injector's own body to draw exactly that code (its only code literal; a Warning severity named iff the row is a warning) and a property method referencing it whose closure reaches ErrorInjector.Judge. All 32 rows checked. (b) YGenerated_RowsAreBackedByAnAcceptanceProperty — every Y member is referenced by a property method whose closure reaches an acceptance verdict from the named set: SemanticFilter. {WellTypedProgram, CompilableProgram, WellTypedSource, CompilableProject, AdmitWellTyped}, ErrorInjector.JudgeClean, PropertyCorpus.AssertAllPassOrAllowed with allowedCodes null, VariancePropertyTests.AssertEverySampleIsDiagnosticFree, and Assert.Equal(x.Total, x.Passed). (c) YGenerated_LabelIsTheMemberItsGeneratorCalls — each `new Y("Label", () => …)` lambda calls (or passes as a method group) exactly one generator method, the label, following the roster's consumer-argument helpers; the syntax count equals ExpectedYGenerated (103). mutation M3 (roster: the await-outside-async row's "SPY0273" -> "SPY0274"): broken -> red (1 failed, (a): "no property method names the member and \"SPY0274\" in one body …"), restored -> green. mutation M4 (FStringPropertyTests.FString_WithFormatSpecs_CompilesClean deleted, on disk): broken -> red (1 failed, (b): "GenFStrings.FStringWithFormatSpecs: no property method samples it and reaches an acceptance verdict"), restored -> green. mutation M5 (the UnaryOperatorProgram row relabelled "GenOperators.BinaryOperatorProgram"): broken -> red (1 failed, (c): "line 768: label 'GenOperators.BinaryOperatorProgram', the generator calls [GenOperators.UnaryOperatorProgram]"), restored -> green. Commit state: TypedGeneratorRoster + PropertyOracleConformance + ProcessGlobalStateConformance 45/0/0 (measured). Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_017D8V5muKcTsUwCKAHghw1h --- .../Semantic/PropertySourceIndex.cs | 174 ++++++++++++++++++ .../Semantic/TypedGeneratorRosterTests.cs | 172 +++++++++++++++++ 2 files changed, 346 insertions(+) create mode 100644 src/Sharpy.Compiler.Tests/Properties/Semantic/PropertySourceIndex.cs diff --git a/src/Sharpy.Compiler.Tests/Properties/Semantic/PropertySourceIndex.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/PropertySourceIndex.cs new file mode 100644 index 000000000..f40d0f76c --- /dev/null +++ b/src/Sharpy.Compiler.Tests/Properties/Semantic/PropertySourceIndex.cs @@ -0,0 +1,174 @@ +using Microsoft.CodeAnalysis; +using Microsoft.CodeAnalysis.CSharp; +using Microsoft.CodeAnalysis.CSharp.Syntax; + +namespace Sharpy.Compiler.Tests.Properties.Semantic; + +/// +/// A Roslyn index of the property sources the typed-generator roster leans on (#2288, verify finding +/// F3): every method of every scanned file, with the Type.Member references, the string literals +/// and the same-file calls of its body. reads it to tie each +/// roster lane to the property that sustains it, so a roster row cannot drift green from the code. +/// +internal sealed class PropertySourceIndex +{ + /// One method: are the X.Y member accesses of its body + /// (calls and method groups alike), its string literals, + /// the simple names it invokes (candidates for a same-file helper). + public sealed record Method( + string File, + string Name, + SyntaxNode Body, + IReadOnlySet References, + IReadOnlySet Literals, + IReadOnlySet Calls) + { + public override string ToString() => $"{File}:{Name}"; + } + + private readonly Dictionary> _byFile; + + private PropertySourceIndex(Dictionary> byFile) + { + _byFile = byFile; + } + + public IEnumerable Methods => _byFile.Values.SelectMany(m => m); + + /// Indexes every *.cs under whose root-relative, + /// '/'-separated path accepts. + public static PropertySourceIndex Load(string root, Func include) + { + var byFile = new Dictionary>(StringComparer.Ordinal); + foreach (var path in Directory.EnumerateFiles(root, "*.cs", SearchOption.AllDirectories)) + { + var relative = Path.GetRelativePath(root, path).Replace(Path.DirectorySeparatorChar, '/'); + if (!include(relative)) + continue; + var tree = CSharpSyntaxTree.ParseText(File.ReadAllText(path)); + byFile[relative] = tree.GetRoot().DescendantNodes().OfType() + .Where(m => m.Body is not null || m.ExpressionBody is not null) + .Select(m => Describe(relative, m)) + .ToList(); + } + + return new PropertySourceIndex(byFile); + } + + private static Method Describe(string file, MethodDeclarationSyntax declaration) + { + SyntaxNode body = (SyntaxNode?)declaration.Body ?? declaration.ExpressionBody!; + var references = body.DescendantNodesAndSelf().OfType() + .Where(m => m.Expression is IdentifierNameSyntax) + .Select(m => $"{((IdentifierNameSyntax)m.Expression).Identifier.ValueText}.{m.Name.Identifier.ValueText}") + .ToHashSet(StringComparer.Ordinal); + var literals = body.DescendantNodesAndSelf().OfType() + .Where(l => l.IsKind(SyntaxKind.StringLiteralExpression)) + .Select(l => l.Token.ValueText) + .ToHashSet(StringComparer.Ordinal); + var calls = body.DescendantNodesAndSelf().OfType() + .Select(i => i.Expression switch + { + IdentifierNameSyntax id => id.Identifier.ValueText, + GenericNameSyntax g => g.Identifier.ValueText, + MemberAccessExpressionSyntax { Expression: ThisExpressionSyntax, Name: var n } => n.Identifier.ValueText, + _ => null, + }) + .OfType() + .ToHashSet(StringComparer.Ordinal); + return new Method(file, declaration.Identifier.ValueText, body, references, literals, calls); + } + + /// and every same-file method it calls, transitively — the code + /// that runs when the method runs, as far as one file can say. + public IReadOnlyList Closure(Method method) + { + var sameFile = _byFile[method.File]; + var seen = new HashSet { method }; + var queue = new Queue(seen); + while (queue.Count > 0) + { + var current = queue.Dequeue(); + foreach (var callee in sameFile.Where(m => current.Calls.Contains(m.Name))) + { + if (seen.Add(callee)) + queue.Enqueue(callee); + } + } + + return seen.ToList(); + } + + /// The invocations in 's closure, as X.Y (or the simple + /// name), each with its argument list. + public IEnumerable<(string Name, ArgumentListSyntax Arguments)> ClosureInvocations(Method method) => + Closure(method).SelectMany(m => m.Body.DescendantNodesAndSelf().OfType()) + .Select(i => (i.Expression switch + { + MemberAccessExpressionSyntax { Expression: IdentifierNameSyntax receiver, Name: var n } => + $"{receiver.Identifier.ValueText}.{n.Identifier.ValueText}", + MemberAccessExpressionSyntax { Name: var n } => n.Identifier.ValueText, + IdentifierNameSyntax id => id.Identifier.ValueText, + GenericNameSyntax g => g.Identifier.ValueText, + _ => "", + }, i.ArgumentList)); + + /// + /// Every new Y("Label", () => …) in : its label, line, and + /// the (Type.Method) its lambda calls or passes as a method + /// group — following calls to the roster's own helper methods (TypedStatements() → + /// GenTyped.TypedProgram). + /// + public static List<(string Label, int Line, IReadOnlySet Invoked)> YRows( + string rosterSource, IReadOnlySet generatorMethods) + { + var tree = CSharpSyntaxTree.ParseText(rosterSource); + var root = tree.GetRoot(); + var helpers = root.DescendantNodes().OfType() + .GroupBy(m => m.Identifier.ValueText) + .ToDictionary(g => g.Key, g => g.Select(m => (SyntaxNode?)m.Body ?? m.ExpressionBody!).ToList(), StringComparer.Ordinal); + + IReadOnlySet Invoked(SyntaxNode scope) + { + var found = new HashSet(StringComparer.Ordinal); + var visited = new HashSet(StringComparer.Ordinal); + var pending = new Stack(); + pending.Push(scope); + while (pending.Count > 0) + { + var current = pending.Pop(); + // A generator method called or passed as a method group (`SelectMany(GenX.Member)`). + foreach (var access in current.DescendantNodesAndSelf().OfType()) + { + if (access.Expression is IdentifierNameSyntax type + && generatorMethods.Contains($"{type.Identifier.ValueText}.{access.Name.Identifier.ValueText}")) + found.Add($"{type.Identifier.ValueText}.{access.Name.Identifier.ValueText}"); + } + + // A call to one of the roster's own helpers is followed into its body. + foreach (var invocation in current.DescendantNodesAndSelf().OfType()) + { + if (invocation.Expression is IdentifierNameSyntax helper + && helpers.TryGetValue(helper.Identifier.ValueText, out var bodies) + && visited.Add(helper.Identifier.ValueText)) + { + foreach (var body in bodies) + pending.Push(body); + } + } + } + + return found; + } + + return root.DescendantNodes().OfType() + .Where(c => c.Type is IdentifierNameSyntax { Identifier.ValueText: "Y" } + && c.ArgumentList is { Arguments.Count: >= 2 } args + && args.Arguments[0].Expression is LiteralExpressionSyntax { Token.Value: string }) + .Select(c => ( + (string)((LiteralExpressionSyntax)c.ArgumentList!.Arguments[0].Expression).Token.Value!, + tree.GetLineSpan(c.Span).StartLinePosition.Line + 1, + Invoked(c.ArgumentList.Arguments[1].Expression))) + .ToList(); + } +} diff --git a/src/Sharpy.Compiler.Tests/Properties/Semantic/TypedGeneratorRosterTests.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/TypedGeneratorRosterTests.cs index 8cac5b05e..34a6714b9 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Semantic/TypedGeneratorRosterTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Semantic/TypedGeneratorRosterTests.cs @@ -1416,6 +1416,178 @@ private static List Draw(Gen gen, int count) } } + // ---- Roster ↔ property links (#2288 verify F3) ------------------------------------------------ + // + // A roster lane is a claim about a property; these facts read the property sources (Roslyn) so the + // claim cannot drift green from the code that sustains it. The property universe is every *.cs under + // Properties/ except this roster and the generator namespace's own directory. + + private static string PropertiesRoot => Path.Combine(FixtureRoots.RepositoryRoot, "src", "Sharpy.Compiler.Tests", "Properties"); + + private const string RosterFile = "Semantic/TypedGeneratorRosterTests.cs"; + private const string GeneratorDirectory = "Generators/Typed/"; + private const string InjectorFile = "Generators/Typed/ErrorInjector.cs"; + + private static readonly Lazy PropertySources = new(() => PropertySourceIndex.Load(PropertiesRoot, + file => file != RosterFile && !file.StartsWith(GeneratorDirectory, StringComparison.Ordinal))); + + /// The refusal verdicts a YInjected lane's property must reach (the one seam). + private static readonly HashSet RefusalVerdicts = new(StringComparer.Ordinal) + { + "ErrorInjector.Judge", "ErrorInjector.JudgeSource", "ErrorInjector.JudgeProject", + }; + + /// + /// The ACCEPTANCE verdicts a Y-generated lane's property must reach — each judges every sample, never a + /// fraction: the generated-lane filter with its sink (SemanticFilter.*), the accepted-program + /// verdict (ErrorInjector.JudgeClean), PropertyCorpus.AssertAllPassOrAllowed with NO + /// allowed codes, the variance lanes' diagnostic-free core + /// (VariancePropertyTests.AssertEverySampleIsDiagnosticFree), and the decorator lanes' + /// Assert.Equal(set.Total, set.Passed) over every sample. + /// + private static readonly HashSet AcceptanceVerdicts = new(StringComparer.Ordinal) + { + "SemanticFilter.WellTypedProgram", "SemanticFilter.CompilableProgram", "SemanticFilter.WellTypedSource", + "SemanticFilter.CompilableProject", "SemanticFilter.AdmitWellTyped", "ErrorInjector.JudgeClean", + "PropertyCorpus.AssertAllPassOrAllowed", "AssertEverySampleIsDiagnosticFree", "Assert.Equal", + }; + + private static bool IsAcceptance(PropertySourceIndex.Method method, string name, + Microsoft.CodeAnalysis.CSharp.Syntax.ArgumentListSyntax arguments) + { + if (!AcceptanceVerdicts.Contains(name)) + return false; + var args = arguments.Arguments; + return name switch + { + // No allowed codes: the second argument (or `allowedCodes:`) is the null literal. + "PropertyCorpus.AssertAllPassOrAllowed" => args.Any(a => + (a.NameColon?.Name.Identifier.ValueText == "allowedCodes" || (a.NameColon is null && args.IndexOf(a) == 1)) + && Microsoft.CodeAnalysis.CSharpExtensions.IsKind(a.Expression, Microsoft.CodeAnalysis.CSharp.SyntaxKind.NullLiteralExpression)), + // Only the variance file's helper of that name. + "AssertEverySampleIsDiagnosticFree" => method.File == "Semantic/VariancePropertyTests.cs", + // Only Assert.Equal(x.Total, x.Passed): every sample passed. + "Assert.Equal" => args.Count == 2 + && args[0].Expression is Microsoft.CodeAnalysis.CSharp.Syntax.MemberAccessExpressionSyntax { Name.Identifier.ValueText: "Total" } + && args[1].Expression is Microsoft.CodeAnalysis.CSharp.Syntax.MemberAccessExpressionSyntax { Name.Identifier.ValueText: "Passed" }, + _ => true, + }; + } + + /// + /// Every row is the claim of a real refusal lane. For a generator member + /// (an invalid-program generator): some property method names the member AND the row's code literal in + /// ONE body, and its closure (the method plus the same-file helpers it calls) reaches the refusal seam + /// at the row's severity. For an ErrorInjector method: the method's own body draws exactly the + /// row's code (its only code literal, and CompilerDiagnosticSeverity.Warning named iff the row is + /// a warning), and some property method references it with a closure reaching + /// ErrorInjector.Judge. + /// + [Fact] + public void YInjected_RowsAreBackedByTheirRefusalProperty() + { + var index = PropertySources.Value; + var injector = PropertySourceIndex.Load(PropertiesRoot, file => file == InjectorFile); + var problems = new List(); + var checkedRows = 0; + + foreach (var row in Rows) + { + if (row.Injected is not YInjected yi) + continue; + checkedRows++; + var (type, member) = (yi.Member.Split('.')[0], yi.Member.Split('.')[1]); + var severity = $"CompilerDiagnosticSeverity.{yi.Severity}"; + + if (type == "ErrorInjector") + { + var bodies = injector.Methods.Where(m => m.Name == member).ToList(); + var codes = bodies.SelectMany(m => m.Literals).Where(l => DiagnosticCode.IsMatch(l)).Distinct().ToList(); + if (bodies.Count == 0) + problems.Add($"{yi.Member}: no such method in {InjectorFile}"); + else if (codes is not [var only] || only != yi.Code) + problems.Add($"{yi.Member}: the roster says {yi.Code}, the injector's body draws [{string.Join(", ", codes)}]"); + var warns = bodies.Any(m => m.References.Contains("CompilerDiagnosticSeverity.Warning")); + if (warns != (yi.Severity == CompilerDiagnosticSeverity.Warning)) + problems.Add($"{yi.Member}: the roster says {yi.Severity}, the injector {(warns ? "names" : "does not name")} a Warning severity"); + + if (!index.Methods.Any(m => m.References.Contains(yi.Member) + && index.ClosureInvocations(m).Any(i => i.Name == "ErrorInjector.Judge"))) + problems.Add($"{yi.Member}: no property method references it and reaches ErrorInjector.Judge"); + continue; + } + + var backing = index.Methods + .Where(m => m.References.Contains(yi.Member) && m.Literals.Contains(yi.Code)) + .Where(m => index.Closure(m).Any(c => c.References.Contains(severity))) + .Where(m => index.ClosureInvocations(m).Any(i => RefusalVerdicts.Contains(i.Name))) + .ToList(); + if (backing.Count == 0) + problems.Add($"{yi.Member} ({yi.Code}, {yi.Severity}): no property method names the member and \"{yi.Code}\" " + + $"in one body and reaches the refusal seam at {severity}"); + else + _output.WriteLine($" {yi.Member} {yi.Code} {yi.Severity} <- {string.Join(", ", backing)}"); + } + + Assert.Equal(ExpectedYInjected, checkedRows); + Assert.True(problems.Count == 0, + $"{problems.Count} YInjected row(s) are not backed by their property:\n " + string.Join("\n ", problems)); + } + + /// + /// Every row's member is sampled by a property that ACCEPTS every sample (Design + /// Decision 5: the roster's raw control proves presence, the property proves acceptance): some + /// property method references the member and its closure reaches one of + /// . + /// + [Fact] + public void YGenerated_RowsAreBackedByAnAcceptanceProperty() + { + var index = PropertySources.Value; + var problems = new List(); + var membersTested = Rows.Select(r => r.Generated).OfType().Select(y => y.Member).Distinct().OrderBy(m => m, StringComparer.Ordinal).ToList(); + + foreach (var member in membersTested) + { + var backing = index.Methods + .Where(m => m.References.Contains(member) + && index.ClosureInvocations(m).Any(i => IsAcceptance(m, i.Name, i.Arguments))) + .ToList(); + if (backing.Count == 0) + problems.Add($"{member}: no property method samples it and reaches an acceptance verdict"); + else + _output.WriteLine($" {member} <- {string.Join(", ", backing.Take(3))}{(backing.Count > 3 ? $" (+{backing.Count - 3})" : "")}"); + } + + Assert.True(membersTested.Count > 0, "no Y-generated member was checked — the link is vacuous"); + Assert.True(problems.Count == 0, + $"{problems.Count} Y-generated member(s) have no acceptance property:\n " + string.Join("\n ", problems)); + } + + /// + /// Every row's label is the generator member its lambda calls — read from this file's + /// syntax, following the roster's consumer-argument helpers — so the label + /// reflects on and the roster's links read cannot name one member while the control samples another. + /// + [Fact] + public void YGenerated_LabelIsTheMemberItsGeneratorCalls() + { + var generatorMethods = typeof(GenTyped).Assembly.GetTypes() + .Where(t => t.Namespace == GeneratorsNamespace && !t.IsNested && !t.Name.StartsWith("<", StringComparison.Ordinal)) + .SelectMany(t => t.GetMethods(BindingFlags.Public | BindingFlags.Static).Select(m => $"{t.Name}.{m.Name}")) + .ToHashSet(StringComparer.Ordinal); + var rows = PropertySourceIndex.YRows(File.ReadAllText(Path.Combine(PropertiesRoot, RosterFile)), generatorMethods); + + var problems = rows + .Where(r => r.Invoked.Count != 1 || !r.Invoked.Contains(r.Label)) + .Select(r => $"line {r.Line}: label '{r.Label}', the generator calls [{string.Join(", ", r.Invoked.OrderBy(i => i, StringComparer.Ordinal))}]") + .ToList(); + + Assert.Equal(ExpectedYGenerated, rows.Count); + Assert.True(problems.Count == 0, + $"{problems.Count} Y row(s) label a member their generator does not call:\n " + string.Join("\n ", problems)); + } + // ---- Totality (Task 4) ------------------------------------------------------------------- // Counted at landing and bumped in the same commit as the row that moves them. N = lanes citing the From 9691845cd83b6aedbedc51a51d7db95bf1e4116b Mon Sep 17 00:00:00 2001 From: antonsynd <2648730+antonsynd@users.noreply.github.com> Date: Tue, 20 Oct 2026 22:29:31 -0400 Subject: [PATCH 06/11] =?UTF-8?q?test(conformance):=20the=20property-oracl?= =?UTF-8?q?e=20scan=20reads=20the=20whitespace-normalized=20token=20stream?= =?UTF-8?q?,=20not=20lines,=20and=20bans=20the=20verify=20round's=20evasio?= =?UTF-8?q?ns=20=E2=80=94=20parenthesized/multiplied=20thresholds,=20lower?= =?UTF-8?q?=20bounds=20on=20any=20non-applicability=20counter,=20code=20li?= =?UTF-8?q?terals=20compared=20outside=20the=20seam,=20a=20HasErrors=20ver?= =?UTF-8?q?dict,=20and=20a=20catch=20that=20swallows=20what=20the=20pipeli?= =?UTF-8?q?ne=20threw=20(refs=20#2288)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Verify finding F1 (instrument): PropertyOracleConformanceTests matched six regexes per LINE, so `!analysis.Success` / `|| …` split over two lines evaded it (the live ValidatorOrdering cell, drained in bd313602f), and eleven measured spellings passed. Now: - Unit: the banned regexes run over the file's token stream with every trivia run (whitespace, newlines, comments) collapsed to one space (Roslyn), so a split spelling is one statement's text and a comment is never a hit; a hit reports the line of its first token and its enclosing statement. - threshold: also `> (total / 2)`, `passed * 2 > total`, `2 * passed > total`, `total / 2 < passed` (a multiplied counter compared with a literal, `x * 2) > 2`, and a relative tolerance `/ av) <= RelTol` are benign look-alikes). - lower-bound: inside any Assert, `x > 0`, `x >= 1`, `x != 0` (either side) and Assert.NotEmpty(x) on any counter except the applicability counters — names ending (case-insensitively) in tested, total, admitted, compared, injected, programs; for .Count/.Length the receiver's name. Renamed to fit: narrowed -> narrowedTested (ErrorCompleteness), RowsChecked -> RowsTested (roster); Differential's `results.Count > 0` becomes `results.Count == programs.Count` (every program classified; non-emptiness is the corpus assert above it). superCallsTested landed in c37894748. - any-failure: also `if (!r.Success) count++` with no throw/assert in the branch. - code-literal (new): a SPY code literal passed to Equal/Contains/Equals/StartsWith/… or compared with == / != against something that is not `.Code` (that is code-compare's spelling); the seam's own `JudgeSource(src, "SPY0273", …)` and `new InjectionResult(m, "SPY0220")` stay benign. - has-errors (new): `.HasErrors` asserted true, or counted by an if with no throw/assert. - swallow-catch (new): a catch whose try reaches the pipeline under test (Analyze, Compile, CompileAndExecute, CompileToCSharp, Unparse, ParseModule, TokenizeAll, Validate, Judge*; or new Compiler/Parser/Lexer/ControlFlowGraphBuilder/ProjectCompilationHelper) and whose body neither throws, asserts, calls a record verb (Add, AddRange, Enqueue, TryAdd, Reject, Exclude, Fail, Record) nor returns/assigns a message string or the caught exception. A catch around the CPython oracle's process management does not reach the pipeline and is not judged. The allowlist stays at 0 rows: c37894748/bd313602f drained every hit; no legitimate hit needed a rule beyond the documented ones above. Positive control: 38 hits = prefix 1, threshold 9, lower-bound 6, any-failure 3, two-bucket 1, catch-increment 2, code-compare 5, code-literal 5, has-errors 2, swallow-catch 4; every benign look-alike (now incl. the applicability floors, the seam's code literals, Assert.False(HasErrors), recording catches, a pipeline-free catch) draws none; the split any-failure and threshold are reported at their first token's line. mutation S8/M6 (ValidatorOrdering re-typed with `if (!analysis.Success` / `|| analysis.Module is null) return null;` split over two lines, on disk): broken -> red (1 failed: "ValidatorOrdering PropertyTests.cs has 1 [any-failure] hit(s) (lines 198)"), restored -> green (4 passed). Commit state = the round's final tree: edit loop Properties.Semantic|Census|Conformance|Roster| Infrastructure|Properties.CodeGen|DifferentialExecution 18011/0/0 (measured, DifferentialExecution sweep included). Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_017D8V5muKcTsUwCKAHghw1h --- .../DifferentialExecutionTests.cs | 2 +- .../ErrorCompletenessPropertyTests.cs | 8 +- .../PropertyOracleConformanceTests.cs | 423 ++++++++++++++++-- .../Semantic/TypedGeneratorRosterTests.cs | 6 +- 4 files changed, 382 insertions(+), 57 deletions(-) diff --git a/src/Sharpy.Compiler.Tests/Properties/Differential/DifferentialExecutionTests.cs b/src/Sharpy.Compiler.Tests/Properties/Differential/DifferentialExecutionTests.cs index e15862274..2607fab70 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Differential/DifferentialExecutionTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Differential/DifferentialExecutionTests.cs @@ -249,7 +249,7 @@ or Verdict.SharpyOkPythonError Output.WriteLine($" DIVERGENCE [{o.Verdict}] {o.Program.Key}: {o.Detail}"); // Enumeration sanity — a corpus that shrank to nothing is itself a regression. - Assert.True(results.Count > 0, "No programs were compared."); + Assert.True(results.Count == programs.Count, "Not every program was classified."); // Per-module vacuity guard. Admitting a module to CPythonAvailableModules only gets its // fixtures PAST THE FILTER; it does not make them comparable. If CPython cannot import the diff --git a/src/Sharpy.Compiler.Tests/Properties/Semantic/ErrorCompletenessPropertyTests.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/ErrorCompletenessPropertyTests.cs index 1cefdf40f..dca36f99d 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Semantic/ErrorCompletenessPropertyTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Semantic/ErrorCompletenessPropertyTests.cs @@ -159,18 +159,18 @@ public void UseInFailedNarrowingBranch_IsRejected() [Fact] public void NarrowedProgram_AnalysesClean() { - int narrowed = 0; + int narrowedTested = 0; var verdicts = ErrorInjector.JudgeSamples(ProgramWithNarrowing(fuel: 1), module => { if (HasNarrowedBlock(module)) - Interlocked.Increment(ref narrowed); + Interlocked.Increment(ref narrowedTested); return ErrorInjector.JudgeClean(Sharpy.Compiler.Pretty.Unparser.Unparse(module), "narrowed Optional program"); }, iter: 100, m => Sharpy.Compiler.Pretty.Unparser.Unparse(m)); _output.WriteLine($"narrowed Optional program: {verdicts.Tested - verdicts.Failures}/{verdicts.Tested} analysed clean; " - + $"{narrowed}/{verdicts.Tested} carry a NarrowedBlock"); + + $"{narrowedTested}/{verdicts.Tested} carry a NarrowedBlock"); Assert.True(verdicts.Tested > 0, "No narrowed Optional programs were generated"); - Assert.True(narrowed > 0, $"0/{verdicts.Tested} samples carry a NarrowedBlock — the soundness claim does not reach it"); + Assert.True(narrowedTested > 0, $"0/{verdicts.Tested} samples carry a NarrowedBlock — the soundness claim does not reach it"); Assert.True(verdicts.First is null, $"{verdicts.Failures}/{verdicts.Tested} narrowed Optional programs refused; the first:\n{verdicts.First}"); } diff --git a/src/Sharpy.Compiler.Tests/Properties/Semantic/PropertyOracleConformanceTests.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/PropertyOracleConformanceTests.cs index 1dbdfeb53..4f9e3628b 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Semantic/PropertyOracleConformanceTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Semantic/PropertyOracleConformanceTests.cs @@ -1,7 +1,9 @@ +using System.Text; using System.Text.RegularExpressions; using Microsoft.CodeAnalysis; using Microsoft.CodeAnalysis.CSharp; using Microsoft.CodeAnalysis.CSharp.Syntax; +using Microsoft.CodeAnalysis.Text; using Sharpy.TestInfrastructure.Integration; using Xunit; using Xunit.Abstractions; @@ -12,31 +14,49 @@ namespace Sharpy.Compiler.Tests.Properties.Semantic; /// Source-scan backstop for the typed-generator refusal oracles (#2288, P63 Design Decision 7): /// ErrorInjector.JudgeSource/Judge is the ONE refusal verdict, and the weak shapes /// that made the property lanes pass vacuously — prefix judging, thresholds, pass-counter lower -/// bounds, any-failure counting, two-bucket sums, a catch that counts as a pass, and a second -/// judging core comparing diagnostic codes outside the seam — must not be re-typed. +/// bounds, any-failure counting, two-bucket sums, a catch that counts as a pass or swallows a +/// throw, a HasErrors verdict, and a second judging core comparing diagnostic codes outside the +/// seam — must not be re-typed. /// /// Universe: every *.cs directly in Properties/Semantic, and every *.cs under /// src/Sharpy.Compiler.Tests/Properties/** whose text /// names the typed generator namespace, computed by the scan (no hand list), minus this scanner and the files inside /// that namespace's own directory (ErrorInjector and SemanticFilter ARE the seam). A /// universe under files fails loud — a broken path or marker would -/// otherwise scan nothing and pass. Comments are blanked (Roslyn trivia) before matching, so a -/// comment recording the old shape is not a hit; string literals are scanned (the codes live there). +/// otherwise scan nothing and pass. +/// +/// +/// Unit: the banned regexes run over the file's WHITESPACE-NORMALIZED token stream (Roslyn: every +/// run of trivia — spaces, newlines, comments — collapses to one space), so a spelling split over +/// lines (!r.Success / || …) is one statement's text, and a comment is never a hit. A hit +/// is reported at the line of its first token with its enclosing statement. String literals are +/// scanned (the codes live there). The syntax rules (lower bounds, catches, HasErrors, code +/// literals) read the tree itself. /// /// /// Deliberate exclusions (each a benign look-alike in the positive control): -/// tested > 0 — the applicability floor every lane keeps (an inapplicable injection is red); -/// => n / 2 — a lambda arrow is not a comparison; .Code != null / == null — a -/// null guard compares no code; a.Code != b.Code — two runs of the compiler compared with each -/// other (the determinism oracle), not a verdict against an expected code; {d.Code} — reading -/// a code to PRINT it; .ExitCode != 0 — not a diagnostic code; catch { return; } / -/// catch { throw …; } — a catch that counts nothing. +/// Assert.True(tested > 0) — a lower bound is banned only on a counter that is not an +/// applicability counter: the exempt names are (a counter, or the +/// receiver of its .Count/.Length, whose name ends in one of them counts samples that +/// REACHED the oracle, never samples that passed it); => n / 2 — a lambda arrow is not a +/// comparison; .Code != null / == null — a null guard compares no code; +/// a.Code != b.Code — two runs of the compiler compared with each other (the determinism +/// oracle), not a verdict against an expected code; {d.Code} — reading a code to PRINT it; +/// .ExitCode != 0 — not a diagnostic code; a code literal passed to the seam +/// (JudgeSource(src, "SPY0273", …), new InjectionResult(m, "SPY0220")); +/// Assert.False(x.HasErrors) — an acceptance check; if (errors.Count > 0) — a failure +/// check outside an assertion; a catch that RECORDS (a throw, an Assert, a call named +/// one of , or a return/assignment of a message string or of the caught +/// exception); a catch whose try never reaches the pipeline under test +/// (/ — e.g. killing the CPython oracle's +/// process). /// /// /// Not expressed: the plan's "new Compiler().Analyze( outside the seam" spelling — every /// soundness lane analyses its accepted program that way, so the call alone cannot be banned without /// banning the accepted-program lane; a second core is caught where it JUDGES, by -/// . +/// and . A filter of an UNTYPED generator's refusals +/// (if (!result.Success) return; over GenSharpy) is not a refusal verdict and is not banned. /// /// /// Allowlist: one literal row per (file, spelling) with the exact current count, each citing @@ -56,21 +76,29 @@ public class PropertyOracleConformanceTests private const string TwoBucket = "two-bucket"; private const string CatchIncrement = "catch-increment"; private const string CodeCompare = "code-compare"; + private const string CodeLiteral = "code-literal"; + private const string HasErrorsVerdict = "has-errors"; + private const string SwallowCatch = "swallow-catch"; private static readonly (string Id, Regex Pattern)[] BannedPatterns = { // Prefix judging: a code family is not a code. (Prefix, new Regex(@"StartsWith\(\s*""SPY", RegexOptions.Compiled)), - // Thresholds: `> total / 4`, `> tested / 2`, `>= analyzed / 2`, `> resolved / 2` … — a - // fraction of the samples may fail. The look-behind keeps `=>` (lambda) and `->` out. + // Thresholds: `> total / 4`, `> tested / 2`, `>= analyzed / 2`, `> (total / 2)`, `passed * 2 > total`, + // `total / 2 < passed` — a fraction of the samples may fail: a division by a sample count or a + // multiplied counter compared with a COUNTER (`x * 2) > 2` and a relative tolerance + // `/ av) <= RelTol` are not). The look-behind keeps `=>` (lambda), `->` and shifts out. (Threshold, new Regex( - @"(?=?\s*(?:(?:total|tested|analyzed|passed)\s*/|[A-Za-z_]\w*\s*/\s*\d)", + @"(?])>(?!>)=?\s*\(?\s*[A-Za-z_][\w\.]*\s*/\s*[\w\.]+" + + @"|\b[A-Za-z_][\w\.]*\s*\*\s*\d+\s*\)?\s*>(?!>)=?\s*\(?\s*[A-Za-z_]" + + @"|\b\d+\s*\*\s*[A-Za-z_][\w\.]*\s*\)?\s*>(?!>)=?\s*\(?\s*[A-Za-z_]" + + @"|[\w\.\)]\s*/\s*\d+\s*\)?\s*<(?![<])=?\s*\(?\s*[A-Za-z_]", RegexOptions.Compiled)), - // Lower bounds on a pass counter: one success anywhere satisfies it. `tested > 0` is - // deliberately NOT here — it is the applicability floor. + // Lower bounds on a pass counter outside an assertion (inside one, the syntax rule judges every + // counter): one success anywhere satisfies it. (LowerBound, new Regex(@"\b(?:passed|diagnosed|rejected|caught)\s*>\s*0\b", RegexOptions.Compiled)), // Any-failure counting: a refusal for an unrelated reason passes for the one under test. - (AnyFailure, new Regex(@"!\s*\w+\.Success\s*\|\|", RegexOptions.Compiled)), + (AnyFailure, new Regex(@"!\s*[A-Za-z_][\w\.]*\.Success\s*\|\|", RegexOptions.Compiled)), // Two-bucket sums: one accepted VALID program satisfies the refusal lane. (TwoBucket, new Regex(@"\b[A-Za-z_]\w*\s*\+\s*[A-Za-z_]\w*\s*>\s*0\b", RegexOptions.Compiled)), // A second judging core: a diagnostic code compared outside the seam. Excludes the null @@ -81,7 +109,45 @@ private static readonly (string Id, Regex Pattern)[] BannedPatterns = }; private static readonly string[] AllIds = - { Prefix, Threshold, LowerBound, AnyFailure, TwoBucket, CatchIncrement, CodeCompare }; + { + Prefix, Threshold, LowerBound, AnyFailure, TwoBucket, CatchIncrement, CodeCompare, CodeLiteral, + HasErrorsVerdict, SwallowCatch, + }; + + /// Counters a lower bound may floor: each counts samples that REACHED the oracle (or the + /// corpus a sweep compares), never samples that passed it — the applicability floor every lane + /// keeps. Matched case-insensitively as the counter's name or its suffix (verdicts.Tested, + /// superCallsTested, programs.Count). + private static readonly string[] ApplicabilityCounters = + { "tested", "total", "admitted", "compared", "injected", "programs" }; + + /// A diagnostic-code literal passed to one of these is a code compared outside the seam. + private static readonly HashSet CodeComparingCalls = new(StringComparer.Ordinal) + { + "Equal", "NotEqual", "Contains", "DoesNotContain", "Equals", "StartsWith", "EndsWith", "Single", + "SingleOrDefault", "First", "FirstOrDefault", "Any", "All", "Count", "Where", "IndexOf", "SequenceEqual", + "Remove", "Same", + }; + + /// A try that calls one of these (or constructs a ) reaches + /// the pipeline under test, so its catch must record what it caught. + private static readonly HashSet PipelineCalls = new(StringComparer.Ordinal) + { + "Analyze", "Compile", "CompileAndExecute", "CompileToCSharp", "Unparse", "ParseModule", "TokenizeAll", + "Validate", "Judge", "JudgeSource", "JudgeProject", + }; + + private static readonly HashSet PipelineTypes = new(StringComparer.Ordinal) + { + "Compiler", "Parser", "Lexer", "ControlFlowGraphBuilder", "ProjectCompilationHelper", + }; + + /// A call named one of these inside a catch records what was caught (a failure list, + /// a sink, a sweep's exclusion counter). + private static readonly HashSet RecordVerbs = new(StringComparer.Ordinal) + { + "Add", "AddRange", "Enqueue", "TryAdd", "Reject", "Exclude", "Fail", "Record", + }; /// /// Every current hit, by (file relative to Properties/, spelling) with its exact count. @@ -160,7 +226,10 @@ public void PropertyLanes_UseNoWeakRefusalOracle_BeyondTheAllowlist() /// /// Positive control: each banned spelling once → exactly that id; each benign look-alike → nothing. - /// A scanner whose patterns no longer match the real spellings fails here, not silently. + /// A scanner whose patterns no longer match the real spellings fails here, not silently. The second + /// half of Banned() is the verify round's evasions (#2288 F1): a spelling split over lines, + /// parenthesized and multiplied thresholds, lower bounds on any counter, code literals compared + /// outside the seam, a HasErrors verdict, and swallowing catches. /// [Fact] public void Scanner_FindsEachBannedSpelling_AndNoBenignLookAlike() @@ -189,9 +258,42 @@ void Banned() ok = d.Code is "SPY0463"; } + void Evasions() + { + if (!analysis.Success + || analysis.Module is null) + return; + Assert.True(diagnosed + > total / 4, ""); + Assert.True(passed > (total / 2), ""); + Assert.True(passed * 2 > total, ""); + Assert.True(total / 2 < passed, ""); + Assert.True(handled > 0, ""); + Assert.True(diagnosed >= 1, ""); + Assert.True(diagnosed != 0, ""); + Assert.NotEmpty(refusedSamples); + if (!result.Success) Interlocked.Increment(ref diagnosed); + Assert.Equal("SPY0273", diagnostics.First().Code); + ok = codes.Contains("SPY0273"); + Assert.Contains("SPY0273", diagnostics.Select(d => d.Code)); + ok = string.Equals(d.Code, "SPY0273"); + ok = codes[0] == "SPY0273"; + if (result.Diagnostics.HasErrors) diagnosed++; + Assert.True(result.Diagnostics.HasErrors, ""); + try { new Sharpy.Compiler.Compiler().Analyze(source, "a.spy"); } catch { } + try { Analyze(source); } catch { return null; } + try { var r = compiler.Compile(source, "a.spy"); } catch (Exception) { } + try { text = Unparser.Unparse(module); } catch { return (false, -1); } + } + void Benign() { Assert.True(tested > 0, "No injections were applicable"); + Assert.True(verdicts.Tested > 0, ""); + Assert.True(admitted > 0, ""); + Assert.True(superCallsTested >= 1, ""); + Assert.True(programs.Count > 0, ""); + Assert.True(compared == total, ""); // Assert.True(passed > tested / 2) — a comment recording the old shape /* if (!result.Success || other) { } */ var half = items.Select(n => n / 2); @@ -201,8 +303,24 @@ void Benign() ok = proc.ExitCode != 0; ok = result.Success && other; ok = count + 1 > 0; + if (errors.Count > 0) throw new Exception("errors"); + if (!result.Success) return; + verdict = ErrorInjector.JudgeSource(source, "SPY0273", CompilerDiagnosticSeverity.Error, null, "x"); + var injection = new ErrorInjector.InjectionResult(mutated, "SPY0220"); + Assert.False(parser.Diagnostics.HasErrors, ""); + if (parser.Diagnostics.HasErrors) { Exclude("parse-errors"); continue; } try { Run(); } catch { return; } try { Run(); } catch (Exception e) { throw new Exception("ICE", e); } + try { proc.Kill(); } catch { } + try { Analyze(source); } catch (Exception e) { failures.Add($"threw {e}"); } + try { Analyze(source); } catch (Exception e) { return $"threw {e.GetType().Name}"; } + try { Analyze(source); } catch (Exception e) { failure = $"threw {e.GetType().Name}"; } + try { Analyze(source); } catch (CfgInvariantException) { throw; } + try { ParseModule(source); } catch { Exclude("parse-errors"); continue; } + var walrus = "def main():\n ys = [y for x in [1, 2] if (y := x * 2) > 2]\n"; + ok = Math.Abs((av - bv) / av) <= RelTol; + if (parser.Diagnostics.HasErrors) { pinHits[pin]++; throw new Exception("unpinned"); } + if (!result.Success) { failures++; Assert.Fail("refused"); } } } """; @@ -215,22 +333,32 @@ void Benign() var expected = new Dictionary { [Prefix] = 1, - [Threshold] = 5, - [LowerBound] = 2, - [AnyFailure] = 1, + [Threshold] = 5 + 4, + [LowerBound] = 2 + 4, + [AnyFailure] = 1 + 2, [TwoBucket] = 1, [CatchIncrement] = 2, [CodeCompare] = 5, + [CodeLiteral] = 5, + [HasErrorsVerdict] = 2, + [SwallowCatch] = 4, }; Assert.Equal(AllIds.OrderBy(i => i), expected.Keys.OrderBy(i => i)); Assert.Equal( expected.OrderBy(kv => kv.Key).Select(kv => $"{kv.Key}={kv.Value}"), byId.OrderBy(kv => kv.Key).Select(kv => $"{kv.Key}={kv.Value}")); - // Every hit is in Banned(): the benign half produced none. + // Every hit is in Banned() or Evasions(): the benign half produced none. var benignStart = text.Split('\n').ToList().FindIndex(l => l.Contains("void Benign()")) + 1; Assert.All(hits, hit => Assert.True(hit.Line < benignStart, $"benign line {hit.Line} hit [{hit.Id}]: {hit.Text}")); - Assert.Equal(17, hits.Count); + Assert.Equal(38, hits.Count); + + // The split spellings are seen, each reported at the line of the match's first token. + var lines = text.Split('\n').ToList(); + var splitAnyFailure = lines.FindIndex(l => l.Contains("if (!analysis.Success")) + 1; + var splitThreshold = lines.FindIndex(l => l.TrimStart().StartsWith("> total / 4", StringComparison.Ordinal)) + 1; + Assert.Contains(hits, h => h.Id == AnyFailure && h.Line == splitAnyFailure); + Assert.Contains(hits, h => h.Id == Threshold && h.Line == splitThreshold); } /// @@ -260,44 +388,241 @@ private static HashSet Universe(string propertiesRoot) { var tree = CSharpSyntaxTree.ParseText(source); var root = tree.GetRoot(); + var found = new Dictionary<(string Id, int Position), SyntaxNode?>(); + + void Hit(string id, int position, SyntaxNode? node = null) => found.TryAdd((id, position), node); - // Blank every comment (keep newlines) so line numbers survive and comments never hit. - var chars = source.ToCharArray(); - foreach (var trivia in root.DescendantTrivia(descendIntoTrivia: true)) + // The regexes read the whitespace-normalized token stream: every trivia run (whitespace, + // newlines, comments) is one space, so a spelling split over lines is seen and a comment never is. + var (normalized, origin) = Normalize(root); + foreach (var (id, pattern) in BannedPatterns) { - if (!trivia.IsKind(SyntaxKind.SingleLineCommentTrivia) - && !trivia.IsKind(SyntaxKind.MultiLineCommentTrivia) - && !trivia.IsKind(SyntaxKind.SingleLineDocumentationCommentTrivia) - && !trivia.IsKind(SyntaxKind.MultiLineDocumentationCommentTrivia)) - continue; - for (int i = trivia.FullSpan.Start; i < trivia.FullSpan.End; i++) - { - if (chars[i] is not ('\n' or '\r')) - chars[i] = ' '; - } + foreach (Match match in pattern.Matches(normalized)) + Hit(id, origin[match.Index]); } - var lines = new string(chars).Split('\n'); - var hits = new List<(string Id, int Line, string Text)>(); - for (int i = 0; i < lines.Length; i++) + foreach (var invocation in root.DescendantNodes().OfType()) { - foreach (var (id, pattern) in BannedPatterns) + if (invocation.Expression is MemberAccessExpressionSyntax + { + Expression: IdentifierNameSyntax { Identifier.ValueText: "Assert" }, + Name.Identifier.ValueText: var assertion, + }) + { + // A lower bound inside an assertion, on any counter but an applicability counter. + foreach (var comparison in invocation.ArgumentList.DescendantNodes().OfType()) + { + if (LowerBoundOperand(comparison) is { } operand && !IsApplicabilityCounter(operand)) + Hit(LowerBound, operand.SpanStart, comparison); + } + + if (assertion == "NotEmpty" && invocation.ArgumentList.Arguments is [var only] + && !IsApplicabilityCounter(only.Expression)) + Hit(LowerBound, only.Expression.SpanStart, invocation); + + // "Some error was reported" asserted as the verdict. + if (assertion == "True") + { + foreach (var hasErrors in HasErrorsReads(invocation.ArgumentList)) + Hit(HasErrorsVerdict, hasErrors.SpanStart, invocation); + } + } + + // A diagnostic-code literal handed to a comparison outside the seam. + if (InvokedName(invocation) is { } name && CodeComparingCalls.Contains(name)) { - foreach (Match _ in pattern.Matches(lines[i])) - hits.Add((id, i + 1, lines[i].Trim())); + foreach (var argument in invocation.ArgumentList.Arguments) + { + if (IsCodeLiteral(argument.Expression)) + Hit(CodeLiteral, argument.Expression.SpanStart, invocation); + } } } - // A catch whose body counts: an exception passes for the outcome the counter records. + // `codes[0] == "SPY0273"` — a code literal compared with something that is not `.Code` (that is + // CodeCompare's spelling). + foreach (var equality in root.DescendantNodes().OfType() + .Where(b => b.IsKind(SyntaxKind.EqualsExpression) || b.IsKind(SyntaxKind.NotEqualsExpression))) + { + var (literal, other) = IsCodeLiteral(equality.Right) ? (equality.Right, equality.Left) + : IsCodeLiteral(equality.Left) ? (equality.Left, equality.Right) + : (null, null); + if (literal is not null && other is not MemberAccessExpressionSyntax { Name.Identifier.ValueText: "Code" } + && other is not ConditionalAccessExpressionSyntax) + Hit(CodeLiteral, literal.SpanStart, equality); + } + + // Counting by a verdict that admits any failure: `if (!r.Success) count++`, `if (d.HasErrors) count++`. + // A branch that also throws or asserts judges the failure itself; its counter only tallies. + foreach (var ifStatement in root.DescendantNodes().OfType()) + { + var branch = ifStatement.Statement.DescendantNodesAndSelf().ToList(); + if (!branch.Any(IsIncrement) || branch.Any(n => n is ThrowStatementSyntax or ThrowExpressionSyntax + || (n is InvocationExpressionSyntax inv && inv.Expression is MemberAccessExpressionSyntax + { + Expression: IdentifierNameSyntax { Identifier.ValueText: "Assert" }, + }))) + continue; + foreach (var not in ifStatement.Condition.DescendantNodesAndSelf().OfType() + .Where(p => p.IsKind(SyntaxKind.LogicalNotExpression) + && p.Operand is MemberAccessExpressionSyntax { Name.Identifier.ValueText: "Success" })) + Hit(AnyFailure, not.SpanStart, ifStatement); + foreach (var hasErrors in HasErrorsReads(ifStatement.Condition)) + Hit(HasErrorsVerdict, hasErrors.SpanStart, ifStatement); + } + foreach (var catchClause in root.DescendantNodes().OfType()) { - var increments = catchClause.Block.DescendantNodes().Count(IsIncrement); - var line = tree.GetLineSpan(catchClause.Span).StartLinePosition.Line; - for (int k = 0; k < increments; k++) - hits.Add((CatchIncrement, line + 1, lines[line].Trim())); + // A catch whose body counts: an exception passes for the outcome the counter records. + var increments = catchClause.Block.DescendantNodes().Where(IsIncrement).ToList(); + foreach (var increment in increments) + Hit(CatchIncrement, increment.SpanStart, catchClause); + + // A catch that swallows what the pipeline under test threw: no record, no rethrow, no assert. + if (increments.Count == 0 && catchClause.Parent is TryStatementSyntax tryStatement + && ReachesPipeline(tryStatement.Block) && !Records(catchClause)) + Hit(SwallowCatch, catchClause.SpanStart, catchClause); + } + + return found + .OrderBy(kv => kv.Key.Position) + .ThenBy(kv => kv.Key.Id, StringComparer.Ordinal) + .Select(kv => (kv.Key.Id, tree.GetLineSpan(new TextSpan(kv.Key.Position, 0)).StartLinePosition.Line + 1, + Describe(kv.Value ?? EnclosingStatement(root, kv.Key.Position)))) + .ToList(); + } + + /// The token stream with every trivia run collapsed to one space, and for each character + /// of it the source position it came from. + private static (string Text, int[] Origin) Normalize(SyntaxNode root) + { + var text = new StringBuilder(); + var origin = new List(); + var previousHadTrailing = false; + foreach (var token in root.DescendantTokens()) + { + if (text.Length > 0 && (previousHadTrailing || token.HasLeadingTrivia)) + { + text.Append(' '); + origin.Add(token.SpanStart); + } + + var tokenText = token.Text; + for (int k = 0; k < tokenText.Length; k++) + { + text.Append(tokenText[k]); + origin.Add(token.SpanStart + k); + } + + previousHadTrailing = token.HasTrailingTrivia; } - return hits; + return (text.ToString(), origin.ToArray()); + } + + private static SyntaxNode? EnclosingStatement(SyntaxNode root, int position) => + root.FindToken(position).Parent?.AncestorsAndSelf().FirstOrDefault(n => n is StatementSyntax or CatchClauseSyntax); + + private static string Describe(SyntaxNode? node) + { + if (node is null) + return ""; + var text = Regex.Replace(node.WithoutTrivia().ToString(), @"\s+", " "); + return text.Length <= 160 ? text : text[..160] + "…"; + } + + /// The counter side of x > 0, x >= 1, x != 0, 0 < x, + /// 1 <= x, 0 != x; null when the comparison is not a lower bound. + private static ExpressionSyntax? LowerBoundOperand(BinaryExpressionSyntax b) + { + static bool Is(ExpressionSyntax e, int value) => + e is LiteralExpressionSyntax { Token.Value: int v } && v == value; + + var operand = b.Kind() switch + { + SyntaxKind.GreaterThanExpression when Is(b.Right, 0) => b.Left, + SyntaxKind.GreaterThanOrEqualExpression when Is(b.Right, 1) => b.Left, + SyntaxKind.NotEqualsExpression when Is(b.Right, 0) => b.Left, + SyntaxKind.LessThanExpression when Is(b.Left, 0) => b.Right, + SyntaxKind.LessThanOrEqualExpression when Is(b.Left, 1) => b.Right, + SyntaxKind.NotEqualsExpression when Is(b.Left, 0) => b.Right, + _ => null, + }; + // A sum is TwoBucket's spelling; a lower bound floors one counter. + return operand is IdentifierNameSyntax or MemberAccessExpressionSyntax ? operand : null; + } + + /// The counter's name — the identifier, the member name, or for .Count/.Length + /// the receiver's — ends (case-insensitively) in one of . + private static bool IsApplicabilityCounter(ExpressionSyntax operand) + { + var name = operand switch + { + IdentifierNameSyntax id => id.Identifier.ValueText, + MemberAccessExpressionSyntax { Name.Identifier.ValueText: "Count" or "Length", Expression: var receiver } => + receiver switch + { + IdentifierNameSyntax rid => rid.Identifier.ValueText, + MemberAccessExpressionSyntax rma => rma.Name.Identifier.ValueText, + _ => "", + }, + MemberAccessExpressionSyntax ma => ma.Name.Identifier.ValueText, + _ => "", + }; + return ApplicabilityCounters.Any(c => name.EndsWith(c, StringComparison.OrdinalIgnoreCase)); + } + + private static IEnumerable HasErrorsReads(SyntaxNode scope) => + scope.DescendantNodesAndSelf().OfType() + .Where(m => m.Name.Identifier.ValueText == "HasErrors"); + + private static bool IsCodeLiteral(ExpressionSyntax expression) => + expression is LiteralExpressionSyntax { Token.Value: string s } && Regex.IsMatch(s, @"^SPY\d{4}$"); + + private static string? InvokedName(InvocationExpressionSyntax invocation) => invocation.Expression switch + { + MemberAccessExpressionSyntax ma => ma.Name.Identifier.ValueText, + IdentifierNameSyntax id => id.Identifier.ValueText, + GenericNameSyntax g => g.Identifier.ValueText, + MemberBindingExpressionSyntax mb => mb.Name.Identifier.ValueText, + _ => null, + }; + + private static bool ReachesPipeline(BlockSyntax tryBlock) => + tryBlock.DescendantNodes().Any(n => n switch + { + InvocationExpressionSyntax inv => InvokedName(inv) is { } name && PipelineCalls.Contains(name), + ObjectCreationExpressionSyntax creation => creation.Type switch + { + IdentifierNameSyntax id => PipelineTypes.Contains(id.Identifier.ValueText), + QualifiedNameSyntax q => PipelineTypes.Contains(q.Right.Identifier.ValueText), + _ => false, + }, + _ => false, + }); + + /// The catch body rethrows, asserts, calls a member, or returns or + /// assigns a message string or the caught exception. + private static bool Records(CatchClauseSyntax catchClause) + { + var exception = catchClause.Declaration?.Identifier.ValueText; + + bool Carries(ExpressionSyntax? e) => e is not null && ( + e is InterpolatedStringExpressionSyntax + || e is LiteralExpressionSyntax { Token.Value: string } + || (exception is { Length: > 0 } && e.DescendantNodesAndSelf().OfType() + .Any(id => id.Identifier.ValueText == exception))); + + return catchClause.Block.DescendantNodes().Any(n => n switch + { + ThrowStatementSyntax or ThrowExpressionSyntax => true, + InvocationExpressionSyntax inv => + (inv.Expression is MemberAccessExpressionSyntax { Expression: IdentifierNameSyntax { Identifier.ValueText: "Assert" } }) + || (InvokedName(inv) is { } name && RecordVerbs.Contains(name)), + ReturnStatementSyntax ret => Carries(ret.Expression), + AssignmentExpressionSyntax assignment => Carries(assignment.Right), + _ => false, + }); } private static bool IsIncrement(SyntaxNode node) => node switch diff --git a/src/Sharpy.Compiler.Tests/Properties/Semantic/TypedGeneratorRosterTests.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/TypedGeneratorRosterTests.cs index 34a6714b9..536689e2f 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Semantic/TypedGeneratorRosterTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Semantic/TypedGeneratorRosterTests.cs @@ -1209,7 +1209,7 @@ void CheckLane(RosterRow row, string laneName, Lane lane) // pin's code; any other parse error stays red. ParsePins_StillFire requires every pin to tolerate at // least one sample of the fixed-seed corpus, so a pin drains with its fix instead of going stale. - private sealed record RawControlResult(int RowsChecked, IReadOnlyList Failures, + private sealed record RawControlResult(int RowsTested, IReadOnlyList Failures, IReadOnlyDictionary PinHits, IReadOnlyList<(string Row, int Hits)> RowHits, string CorpusHash, TimeSpan Elapsed); private static readonly Lazy RawControl = new(RunRawControl); @@ -1260,7 +1260,7 @@ private static RawControlResult RunRawControl() private void PrintRawControl(RawControlResult result) { - _output.WriteLine($"RAW control: {result.RowsChecked} Y-generated rows x {RawSamples} samples, more where a row raises it (seed {RawSeed}) " + _output.WriteLine($"RAW control: {result.RowsTested} Y-generated rows x {RawSamples} samples, more where a row raises it (seed {RawSeed}) " + $"in {result.Elapsed.TotalSeconds:F1} s; corpus sha256 {result.CorpusHash} (equal across processes iff the generators are reproducible)"); foreach (var (pin, hits) in result.PinHits) _output.WriteLine($" parse pin {pin.Pin.Issue} ({pin.Code}): {hits} sample source(s) tolerated"); @@ -1278,7 +1278,7 @@ public void YGenerated_RawCorpusContainsTheConstruct() { var result = RawControl.Value; PrintRawControl(result); - Assert.True(result.RowsChecked > 0, "no Y-generated row was checked — the control is vacuous"); + Assert.True(result.RowsTested > 0, "no Y-generated row was checked — the control is vacuous"); Assert.True(result.Failures.Count == 0, $"{result.Failures.Count} Y-generated row(s) fail the raw control:\n " + string.Join("\n ", result.Failures)); } From f10b8381f524afd10c18b2833a08f6020c5bbf6f Mon Sep 17 00:00:00 2001 From: antonsynd <2648730+antonsynd@users.noreply.github.com> Date: Tue, 20 Oct 2026 22:58:58 -0400 Subject: [PATCH 07/11] =?UTF-8?q?test(property):=20the=20CFG=20well-formed?= =?UTF-8?q?ness=20lane=20reads=20typed=20function=20programs=20through=20t?= =?UTF-8?q?he=20sink=20and=20must=20check=20a=20CFG=20from=20every=20admit?= =?UTF-8?q?ted=20program=20=E2=80=94=20it=20checked=200=20CFGs=20from=2050?= =?UTF-8?q?=20programs=20and=20passed=20(refs=20#2288)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Hardening ledger row (cfgsChecked printed, never asserted). Measured first: with only an applicability floor added, the lane went red at once — "0 CFGs checked from 50 programs". The untyped GenSharpy.Module generator never produced a compiling program with a top-level function, and the lane skipped every refused program, so no CFG had ever been built by it. Now the lane samples GenFunctions.ModuleWithFunctions(TypeEnv.Default, "int", fuel: 2) through SemanticFilter.CompilableProgram with a RejectionSink (asserted no unexplained rejection; the #2169 Unparser cell is the one pin), throws when an admitted program has no FunctionDef, and asserts cfgsTested > 0. Measured: 152 CFGs from 50 programs, rejections 3/53 (pinned #2169 ×3, unexplained 0); restored run 147 CFGs, 5/55 all pinned. mutation M-skip (test: every FunctionDef skipped): broken -> red (1 failed: "ModuleWithFunctions drew a module without a function"), restored -> green. mutation M-prod (production, ControlFlowGraphBuilder.Connect drops `to.AddPredecessor(from)`): broken -> red (1 failed: "Successor BB2:body_start of BB0:entry is missing matching predecessor edge"); control: the PRIOR lane (HEAD version) under the same mutation -> green ("0 CFGs checked from 50 programs") — the old lane could not fail; restored (cp + touch, cmp-verified) -> green. Commit state: CfgWellFormedness + PropertyOracleConformance + ProcessGlobalStateConformance + TypedGeneratorRoster 46/0/0 (measured). Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_017D8V5muKcTsUwCKAHghw1h --- .../CfgWellFormednessPropertyTests.cs | 47 ++++++++++--------- 1 file changed, 24 insertions(+), 23 deletions(-) diff --git a/src/Sharpy.Compiler.Tests/Properties/Semantic/CfgWellFormednessPropertyTests.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/CfgWellFormednessPropertyTests.cs index 05d50f94b..8448045e9 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Semantic/CfgWellFormednessPropertyTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Semantic/CfgWellFormednessPropertyTests.cs @@ -1,7 +1,7 @@ using CsCheck; using Sharpy.Compiler.Analysis.ControlFlow; using Sharpy.Compiler.Parser.Ast; -using Sharpy.Compiler.Tests.Properties.Generators; +using Sharpy.Compiler.Tests.Properties.Generators.Typed; using Xunit; using Xunit.Abstractions; @@ -21,46 +21,41 @@ public CfgWellFormednessPropertyTests(ITestOutputHelper output) } /// - /// Builds control flow graphs from every function in randomly generated, - /// successfully-compiled programs and asserts structural invariants: - /// the entry block is labeled "entry"; entry and exit blocks are members - /// of the Blocks collection; every successor edge points to a block in the - /// graph; the exit block has no successors; and statement counts are - /// non-negative. A program the compiler refuses is skipped (the untyped - /// generator's programs are not well typed); a THROW anywhere — compile, - /// re-parse or CFG build — fails the sample: it used to be swallowed with the - /// refusals, so a crashing CFG builder passed (#2288). + /// Builds control flow graphs from every function in typed-generator programs that compile + /// clean and asserts structural invariants: the entry block is labeled "entry"; entry and exit + /// blocks are members of the Blocks collection; every successor edge points to a block in the + /// graph; the exit block has no successors; and statement counts are non-negative. The lane reads + /// through with a + /// : every raw sample compiles (or is a pinned known red), and a THROW + /// anywhere — compile, re-parse or CFG build — fails the sample. It used to sample the untyped + /// generator and skip what the compiler refused, which was every program with a function: the + /// lane checked 0 CFGs from 50 programs and passed (#2288). At least one CFG must be checked. /// [Fact] public void CfgFromCompiledPrograms_SatisfiesStructuralInvariants() { int total = 0; - int cfgsChecked = 0; + int cfgsTested = 0; + var sink = new RejectionSink("CfgWellFormedness.CfgFromCompiledPrograms_SatisfiesStructuralInvariants"); - Gen.Int[2, 3].SelectMany(fuel => - { - var ctx = GenContext.Default with { Fuel = fuel }; - return GenSharpy.Module(ctx); - }).Sample(module => + SemanticFilter.CompilableProgram(GenFunctions.ModuleWithFunctions(TypeEnv.Default, "int", fuel: 2), sink) + .Sample(module => { Interlocked.Increment(ref total); var source = Sharpy.Compiler.Pretty.Unparser.Unparse(module); - var compiler = new Sharpy.Compiler.Compiler(); - var result = compiler.Compile(source, "cfg_test.spy"); - if (!result.Success) - return; - // Re-parse to obtain FunctionDef AST nodes to feed the CFG builder. var lexer = new Sharpy.Compiler.Lexer.Lexer(source); var tokens = lexer.TokenizeAll(); var parser = new Sharpy.Compiler.Parser.Parser(tokens); var parsed = parser.ParseModule(); + int functions = 0; foreach (var stmt in parsed.Body) { if (stmt is not FunctionDef funcDef) continue; + functions++; var builder = new ControlFlowGraphBuilder(); var cfg = builder.Build(funcDef); @@ -126,11 +121,17 @@ public void CfgFromCompiledPrograms_SatisfiesStructuralInvariants() "FindUnreachableBlocks returned a block not in Blocks"); } - Interlocked.Increment(ref cfgsChecked); + Interlocked.Increment(ref cfgsTested); } + if (functions == 0) + throw new CfgInvariantException($"ModuleWithFunctions drew a module without a function:\n{source}"); }, print: m => Sharpy.Compiler.Pretty.Unparser.Unparse(m), iter: 50); - _output.WriteLine($"CFG well-formedness: {cfgsChecked} CFGs checked from {total} programs"); + _output.WriteLine(sink.Summary); + _output.WriteLine($"CFG well-formedness: {cfgsTested} CFGs checked from {total} programs"); + Assert.True(sink.Unexplained.Count == 0, sink.Report()); + // Applicability floor: a run that checks no CFG proves nothing (#2288). + Assert.True(cfgsTested > 0, $"no CFG was checked from {total} programs"); } private sealed class CfgInvariantException : Exception From 13c4ec04b0cc466e223a39de9c42a9cb78c18f64 Mon Sep 17 00:00:00 2001 From: antonsynd <2648730+antonsynd@users.noreply.github.com> Date: Wed, 21 Oct 2026 00:50:38 -0400 Subject: [PATCH 08/11] =?UTF-8?q?test(property):=20an=20admitted=20program?= =?UTF-8?q?'s=20failed=20run=20and=20a=20compiler=20throw=20are=20recorded?= =?UTF-8?q?=20failures=20=E2=80=94=20TypeSoundness's=20two=20execution=20l?= =?UTF-8?q?anes=20no=20longer=20filter=20run=20failures=20by=20four=20.NET?= =?UTF-8?q?=20exception=20names,=20and=20OverloadOrderIndependence=20no=20?= =?UTF-8?q?longer=20compares=20a=20caught=20throw=20as=20a=20signature=20(?= =?UTF-8?q?refs=20#2288)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit P63 verify round (sibling-cell prober K1, plan oracle-matrix kinds "filtered" / "no-throw"). TypedProgram_ExecutesWithoutRuntimeTypeErrors and TypedProgram_WithCollections_… recorded a failed run only when stderr named InvalidCast/NullReference/InvalidOperation/ArrayTypeMismatch; every other failure (a Sharpy runtime error, an ArgumentException, a Roslyn emit failure with empty stderr) was admitted silently — dd4ca1ec3 cured only FilteredTypedProgram. Both now record every failed run, as FilteredTypedProgram does. ResolutionSignature caught any compiler throw and returned "THREW:", so a throw identical in every declaration order compared equal and passed (the shape H2 cured in DeterminismPropertyTests); the throw now propagates and fails the sample. Measured: TypeSoundness 4/4, OverloadOrderIndependence 1/1 green @ this tree (no admitted sample fails to run; no throw). Mutations (worktree @ f10b8381f + this patch, restored by cp + touch): - MB: Builtins.PrintWithOptions throws ArgumentException → TypeSoundness red (3 failed: both execution lanes + FilteredTypedProgram; WithOptionals is analyse-only and stays green); at f10b8381f the same mutant left both execution lanes green (prober, measured). - MC: Compiler.Compile throws on every call → before this patch OverloadOrderIndependence 1/1 GREEN (vacuous, measured); after it RED (1 failed, "P63-verify mutant MC"). - Restored → 22/22 green (TypeSoundness | OverloadOrderIndependence | JudgeSourceTests). Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01ScHwfTQy7v2FAujH3NSLQg --- .../OverloadOrderIndependencePropertyTests.cs | 22 +++++-------- .../Semantic/TypeSoundnessPropertyTests.cs | 32 +++++++------------ 2 files changed, 20 insertions(+), 34 deletions(-) diff --git a/src/Sharpy.Compiler.Tests/Properties/Semantic/OverloadOrderIndependencePropertyTests.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/OverloadOrderIndependencePropertyTests.cs index 619973a8d..f861a2c66 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Semantic/OverloadOrderIndependencePropertyTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Semantic/OverloadOrderIndependencePropertyTests.cs @@ -116,23 +116,17 @@ public void OverloadResolution_IsDeclarationOrderIndependent() /// Positions and messages are excluded so that reordering the overload declarations (which /// shifts line numbers of any per-overload diagnostic) is not itself a difference; a change in /// which overload wins still shows up as a change in the code multiset (the str-typed consumer - /// errors or not). + /// errors or not). A throw is not a signature: it propagates and fails the sample, so a compiler + /// throw that is identical in every declaration order cannot compare equal and pass (#2288 verify). /// private static string ResolutionSignature(string source) { - try - { - var compiler = new Sharpy.Compiler.Compiler(); - var result = compiler.Compile(source, "test.spy"); - var codes = (result.Diagnostics?.GetAll() ?? Enumerable.Empty()) - .Select(d => d.Code) - .OrderBy(c => c, StringComparer.Ordinal); - return $"success={result.Success};codes=[{string.Join(",", codes)}]"; - } - catch (Exception ex) - { - return $"THREW:{ex.GetType().Name}"; - } + var compiler = new Sharpy.Compiler.Compiler(); + var result = compiler.Compile(source, "test.spy"); + var codes = (result.Diagnostics?.GetAll() ?? Enumerable.Empty()) + .Select(d => d.Code) + .OrderBy(c => c, StringComparer.Ordinal); + return $"success={result.Success};codes=[{string.Join(",", codes)}]"; } private static string BuildSource(Engine engine, List<(string Param, string Ret, string Lit)> overloads, string argLiteral) diff --git a/src/Sharpy.Compiler.Tests/Properties/Semantic/TypeSoundnessPropertyTests.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/TypeSoundnessPropertyTests.cs index 627ae69e6..b6a8cbdf9 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Semantic/TypeSoundnessPropertyTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Semantic/TypeSoundnessPropertyTests.cs @@ -33,23 +33,19 @@ public void TypedProgram_ExecutesWithoutRuntimeTypeErrors() var source = Sharpy.Compiler.Pretty.Unparser.Unparse(module); var result = CompileAndExecuteWithGC(source); + // The sink admitted the program, so ANY failed run is a finding — a runtime throw, a + // Roslyn emit failure (empty stderr) or a Sharpy runtime error — never a sample filtered + // by the exception's name (#2288 verify: four .NET names admitted every other failure). if (!result.Success) { - var stderr = result.StandardError ?? ""; - if (stderr.Contains("InvalidCastException") || - stderr.Contains("NullReferenceException") || - stderr.Contains("InvalidOperationException") || - stderr.Contains("ArrayTypeMismatchException")) - { - lock (errors) - errors.Add($"Runtime type error:\n{source}\nStderr: {stderr}"); - } + lock (errors) + errors.Add($"Compiled program failed to run: {string.Join("; ", result.CompilationErrors)} {result.Exception?.Message} {result.StandardError}\nSource:\n{source}"); } }, print: m => m == null ? "" : Sharpy.Compiler.Pretty.Unparser.Unparse(m), iter: 15); Output.WriteLine(sink.Summary); Assert.True(sink.Unexplained.Count == 0, sink.Report()); - Output.WriteLine($"Type soundness: {total} programs executed, {errors.Count} runtime type errors"); + Output.WriteLine($"Type soundness: {total} programs executed, {errors.Count} failed runs"); Assert.Empty(errors); } @@ -71,23 +67,19 @@ public void TypedProgram_WithCollections_ExecutesWithoutRuntimeTypeErrors() var source = Sharpy.Compiler.Pretty.Unparser.Unparse(module); var result = CompileAndExecuteWithGC(source); + // The sink admitted the program, so ANY failed run is a finding — a runtime throw, a + // Roslyn emit failure (empty stderr) or a Sharpy runtime error — never a sample filtered + // by the exception's name (#2288 verify: four .NET names admitted every other failure). if (!result.Success) { - var stderr = result.StandardError ?? ""; - if (stderr.Contains("InvalidCastException") || - stderr.Contains("NullReferenceException") || - stderr.Contains("InvalidOperationException") || - stderr.Contains("ArrayTypeMismatchException")) - { - lock (errors) - errors.Add($"Runtime type error:\n{source}\nStderr: {stderr}"); - } + lock (errors) + errors.Add($"Compiled program failed to run: {string.Join("; ", result.CompilationErrors)} {result.Exception?.Message} {result.StandardError}\nSource:\n{source}"); } }, print: m => m == null ? "" : Sharpy.Compiler.Pretty.Unparser.Unparse(m), iter: 15); Output.WriteLine(sink.Summary); Assert.True(sink.Unexplained.Count == 0, sink.Report()); - Output.WriteLine($"Type soundness (collections): {total} programs executed, {errors.Count} runtime type errors"); + Output.WriteLine($"Type soundness (collections): {total} programs executed, {errors.Count} failed runs"); Assert.Empty(errors); } From 7f22fcf9c8cc61c31b3895e58443c52eb781ceb5 Mon Sep 17 00:00:00 2001 From: antonsynd <2648730+antonsynd@users.noreply.github.com> Date: Wed, 21 Oct 2026 00:50:38 -0400 Subject: [PATCH 09/11] =?UTF-8?q?test(property):=20JudgeSource's=20error?= =?UTF-8?q?=20arm=20is=20pinned=20to=20exactly=20ONE=20code=20=E2=80=94=20?= =?UTF-8?q?the=20expected=20code=20beside=20a=20second=20error=20is=20refu?= =?UTF-8?q?sed=20(refs=20#2288)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit P63 verify round (class-cure auditor): weakening the error arm to `errors.Contains(expected)` left all 319 Properties.Semantic tests green — JudgeSourceTests had the warning arm's "beside an error / beside a second warning" cells but no error-arm twin. New cell: SPY0220 + SPY0200 (measured with the built sharpyc @ f10b8381f) judged for SPY0220 → refused, "drew [SPY0200, SPY0220]". Mutation (worktree @ f10b8381f + this patch): `errors is [var only] && only == expected` → `errors.Contains(expected)` → red (1 failed: ErrorArm_ExpectedCodeBesideASecondError_IsRefused); restored → green (JudgeSourceTests all passed, 22/22 with the sibling lanes). Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01ScHwfTQy7v2FAujH3NSLQg --- .../Properties/Semantic/JudgeSourceTests.cs | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/Sharpy.Compiler.Tests/Properties/Semantic/JudgeSourceTests.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/JudgeSourceTests.cs index 36a6a96a2..adf32c0e1 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Semantic/JudgeSourceTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Semantic/JudgeSourceTests.cs @@ -74,6 +74,15 @@ def main(): print(n) """; + // The error arm's code beside a second error (SPY0200, an undefined name): two broken facts — + // measured SPY0220 + SPY0200 with the built `sharpyc emit diagnostics` @ f10b8381f. + private const string ErrorProgramAndUndefinedName = """ + def main(): + let n: int = "x" + print(n) + print(undefined_name) + """; + private const string CleanProgram = """ def main(): let n: int = 1 @@ -149,6 +158,17 @@ public void ErrorArm_OtherCode_IsRefused() Assert.Contains("must draw exactly SPY0222, drew [SPY0220]", failure); } + // (c) exactly ONE code on the error arm: the expected code beside a second error is not a catch — + // the injection broke one fact and the program draws two. + [Fact] + public void ErrorArm_ExpectedCodeBesideASecondError_IsRefused() + { + var failure = ErrorInjector.JudgeSource( + ErrorProgramAndUndefinedName, "SPY0220", CompilerDiagnosticSeverity.Error, null, "type mismatch"); + Assert.NotNull(failure); + Assert.Contains("must draw exactly SPY0220, drew [SPY0200, SPY0220]", failure); + } + // (c) an error is not a warning: the warning arm does not read the error list as its own. [Fact] public void WarningArm_ErrorProgram_IsRefused() From e8933d3ff2077a9e3db53906a7cb5fc6626a3d9a Mon Sep 17 00:00:00 2001 From: antonsynd <2648730+antonsynd@users.noreply.github.com> Date: Wed, 21 Oct 2026 00:50:38 -0400 Subject: [PATCH 10/11] =?UTF-8?q?test(build-tools):=20query=5Fstates=20map?= =?UTF-8?q?s=20a=20pull-request=20url=20to=20PULL=5FREQUEST=20=E2=80=94=20?= =?UTF-8?q?the=20mapping=20c285511dc=20added=20was=20untested=20(refs=20#2?= =?UTF-8?q?288)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit P63 verify round (class-cure auditor): reverting `states[num] = "PULL_REQUEST" if "/pull/" in url else state` to `= state` left the pytest file 25/25 green — every test stubs query_states, so an OPEN pull request cited as a tracker would pass the gate unnoticed. New cells stub subprocess.run for `gh issue view`: a /pull/ url in states OPEN/MERGED/CLOSED → PULL_REQUEST; an /issues/ url keeps its state (positive control). Mutation: the mapping reverted → red (3 failed, the three PR-url cells; the issue-url control stays green); restored (cp + touch) → green (29 passed). Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01ScHwfTQy7v2FAujH3NSLQg --- .../tests/test_allowlist_issue_state.py | 26 +++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/build_tools/tests/test_allowlist_issue_state.py b/build_tools/tests/test_allowlist_issue_state.py index 27d8bd5c8..6d9f0573d 100644 --- a/build_tools/tests/test_allowlist_issue_state.py +++ b/build_tools/tests/test_allowlist_issue_state.py @@ -365,3 +365,29 @@ def test_knownred_cell_citing_a_non_open_issue_is_offence(tmp_path, state): with pytest.raises(SystemExit) as exc: mod.main() assert exc.value.code == 1 + + +@pytest.mark.parametrize("state", ["OPEN", "MERGED", "CLOSED"]) +def test_query_states_maps_a_pull_request_url_to_pull_request(state): + """`gh issue view` answers for a pull request too; query_states must name it PULL_REQUEST, so an + OPEN pull request cited as a tracker is red, not read as an open issue (#2288 verify).""" + def fake_run(args, **kwargs): + if args[:2] == ["gh", "--version"]: + return subprocess.CompletedProcess(args, 0, stdout="gh version 2\n", stderr="") + return subprocess.CompletedProcess( + args, 0, stdout=f"{state} https://github.com/antonsynd/sharpy/pull/1\n", stderr="") + + with patch.object(mod.subprocess, "run", fake_run): + assert mod.query_states([1]) == {1: "PULL_REQUEST"} + + +def test_query_states_keeps_an_issue_urls_state(): + """The positive control: an issue url keeps its own state.""" + def fake_run(args, **kwargs): + if args[:2] == ["gh", "--version"]: + return subprocess.CompletedProcess(args, 0, stdout="gh version 2\n", stderr="") + return subprocess.CompletedProcess( + args, 0, stdout="OPEN https://github.com/antonsynd/sharpy/issues/2287\n", stderr="") + + with patch.object(mod.subprocess, "run", fake_run): + assert mod.query_states([2287]) == {2287: "OPEN"} From 27bf064bb3b26bd1ea2933bd8c3263d837126072 Mon Sep 17 00:00:00 2001 From: antonsynd <2648730+antonsynd@users.noreply.github.com> Date: Wed, 21 Oct 2026 00:50:38 -0400 Subject: [PATCH 11/11] test(cleanup): drop AstDescendants.Descendants (no caller) and the closed #2288 from the roster's GeneratorTrackers (refs #2288) P63 verify round, Section B: every caller uses SelfAndDescendants; no roster row cites #2288 (the issue-state gate would redden on one), so the set only named a closed issue. Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01ScHwfTQy7v2FAujH3NSLQg --- src/Sharpy.Compiler.Tests/Infrastructure/AstDescendants.cs | 3 --- .../Properties/Semantic/TypedGeneratorRosterTests.cs | 2 +- 2 files changed, 1 insertion(+), 4 deletions(-) diff --git a/src/Sharpy.Compiler.Tests/Infrastructure/AstDescendants.cs b/src/Sharpy.Compiler.Tests/Infrastructure/AstDescendants.cs index f64f256a8..b73149743 100644 --- a/src/Sharpy.Compiler.Tests/Infrastructure/AstDescendants.cs +++ b/src/Sharpy.Compiler.Tests/Infrastructure/AstDescendants.cs @@ -28,7 +28,4 @@ public static IEnumerable SelfAndDescendants(Node root) stack.Push(children[i]); } } - - /// Every node below , excluding the root itself. - public static IEnumerable Descendants(Node root) => SelfAndDescendants(root).Skip(1); } diff --git a/src/Sharpy.Compiler.Tests/Properties/Semantic/TypedGeneratorRosterTests.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/TypedGeneratorRosterTests.cs index 536689e2f..765bfa065 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Semantic/TypedGeneratorRosterTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Semantic/TypedGeneratorRosterTests.cs @@ -1601,7 +1601,7 @@ public void YGenerated_LabelIsTheMemberItsGeneratorCalls() private const int ExpectedByDesign = 21; private const int ExpectedNoConstruct = 4; - private static readonly HashSet GeneratorTrackers = new(StringComparer.Ordinal) { "#2287", "#2288", "#2324" }; + private static readonly HashSet GeneratorTrackers = new(StringComparer.Ordinal) { "#2287", "#2324" }; [Fact] public void Totality_CountsMatchTheLiteralAnchors()