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"} 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/Differential/DifferentialExecutionTests.cs b/src/Sharpy.Compiler.Tests/Properties/Differential/DifferentialExecutionTests.cs index 348cd1b01..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 @@ -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..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 @@ -170,6 +175,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); @@ -689,7 +724,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/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..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,128 +21,117 @@ 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. Invariant violations are surfaced as failures while - /// unrelated compilation/parse errors (expected for random programs) are - /// swallowed. + /// 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); - try + // 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) { - 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; + functions++; + + 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 (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"); + 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"); } + + Interlocked.Increment(ref cfgsTested); } - 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. - } + 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 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/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/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/JudgeSourceTests.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/JudgeSourceTests.cs index 985d9fe84..adf32c0e1 100644 --- a/src/Sharpy.Compiler.Tests/Properties/Semantic/JudgeSourceTests.cs +++ b/src/Sharpy.Compiler.Tests/Properties/Semantic/JudgeSourceTests.cs @@ -38,12 +38,51 @@ 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" 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 @@ -51,7 +90,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] @@ -71,6 +110,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() @@ -98,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() 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/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/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/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); } 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}"); } } diff --git a/src/Sharpy.Compiler.Tests/Properties/Semantic/TypedGeneratorRosterTests.cs b/src/Sharpy.Compiler.Tests/Properties/Semantic/TypedGeneratorRosterTests.cs index 8cac5b05e..765bfa065 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)); } @@ -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 @@ -1429,7 +1601,7 @@ private static List Draw(Gen gen, int count) 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() 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!;