From 3331509eb975983bf99e811fc4f1172518e99070 Mon Sep 17 00:00:00 2001 From: mao2009 <39354512+mao2009@users.noreply.github.com> Date: Thu, 3 Sep 2026 12:01:02 +0900 Subject: [PATCH] =?UTF-8?q?docs:=20pure=20method=E5=91=BC=E3=81=B3?= =?UTF-8?q?=E5=87=BA=E3=81=97=E5=A5=91=E7=B4=84=E3=81=A8interprocedural?= =?UTF-8?q?=E8=A7=A3=E6=9E=90=E7=AF=84=E5=9B=B2=E3=82=92=E4=BB=95=E6=A7=98?= =?UTF-8?q?=E5=8C=96?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Issue #10 に対応し、[PureMethod] の契約を呼び出し先まで含めて一貫して 扱えるようにする。テスト数 128 -> 145。 追加: docs/CALL-CONTRACT.md 呼び出し契約を仕様化した。 [PureMethod] は「シンボルに宣言された契約」であり、実装から推論される 性質ではない。pure method から呼べるのは (1) 静的に解決されたシンボルが [PureMethod] を持つメソッド (2) 既知純粋型のメソッド のみで、それ以外は RT0002 とする。呼び出し先の本体は開かない。 未マークのメソッドは常に非純粋として扱う fail-closed 規則である。 解決規則を表で確定した。契約は「静的に解決されたシンボル」に対して 判定されるため、以下が帰結する (すべて実測で確認): - interface 呼び出しは interface メンバに解決されるため、 実装クラス側の [PureMethod] では契約を満たさない - base 型経由の virtual 呼び出しは base のシンボルに解決されるため、 override 側のみの [PureMethod] は効かない - overload は選択されたオーバーロード単位で判定される - 相互再帰は全参加者が [PureMethod] を持つ必要がある virtual dispatch が健全でないことを明記した。base の virtual に [PureMethod] を付けると base 型経由の呼び出しがすべて許可されるが、 override が純粋である保証はなく、PureSharp は検証しない。 virtual / interface メンバへの [PureMethod] 付与は、全 override で 契約を守る責任を著者が負う表明である。 interprocedural analysis の対象範囲を明示した。 v1.0 の対象は「呼び出し 1 段階のみ」。呼び出し先本体の読解、 未マークメソッドを介した推移的伝播、override の契約遵守検証、 whole-program 解析、delegate 実体の純粋性は対象外とした。 cross-method traversal を行わないことが線形コストの根拠である。 呼び出し契約の対象外を 2 件明記した (いずれも false negative)。 ユーザー定義 property getter は property 参照が I/O 型判定しか 行わないため対象外。コンストラクタは invocation として解析されない ため対象外。 external dependency の扱いを決定した。 外部アセンブリも同じ fail-closed 規則で扱い特別扱いしない。 既知純粋型リストに含まれれば許可、それ以外は RT0002。 却下した代替案とその理由も記載した (外部 IL からの純粋性推論は analyzer 内で決定不能かつ環境依存で再現性がない、既定で信頼するのは fail-open、他ライブラリの [Pure] 属性は意味論が弱く一貫性がない)。 既知純粋型リストは allowlist であり、取りこぼしは過剰報告になるが、 リストへの追加は検出範囲の縮小であり非破壊的変更として minor で 修正可能である。 performance を実測した。 methods=100 / 500 / 2000 に対し analyzer 時間は 186 / 349 / 844 ms、 1 メソッドあたり 1.86 / 0.70 / 0.42 ms。コストは解析対象 operation 数に 対して線形で、超線形な挙動はない。call graph を構築せず呼び出し先本体を 訪問しないことがその理由であり、1 段階契約の実利的な利点である。 同一ソースの baseline compile に対して概ね 0.8-1.1 倍。 測定方法も再現可能な形で記載した。 追加: CallContractTests.cs (17 tests) 上記の解決規則・external dependency・対象外ケースを実測で固定した。 performance guard も含む。厳密な閾値は環境差でフレークになるため 破滅的退行のみを検出する緩い上限 (2000 メソッドで 60 秒) とし、 絶対値は閾値ではなく傾向として文書に記録した。 本 PR は Analyzer の挙動を変更していない。 検出範囲の拡大を伴う項目は Open decisions として 5 件記載した (override の契約検証、属性の継承、property getter、コンストラクタ、 ローカル関数の契約継承)。 更新: docs/DIAGNOSTICS.md, docs/PURITY-SEMANTICS.md CALL-CONTRACT.md への相互参照を追加。 検証結果: - dotnet build: PASS (0 error) - dotnet test --no-build: PASS (145/145、baseline 56 から +89) - git diff --check: PASS Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01XB2mDSE67ZDQS9mk5KfAdZ --- docs/CALL-CONTRACT.md | 170 +++++++++++++ docs/DIAGNOSTICS.md | 2 + docs/PURITY-SEMANTICS.md | 2 +- .../CallContractTests.cs | 240 ++++++++++++++++++ 4 files changed, 413 insertions(+), 1 deletion(-) create mode 100644 docs/CALL-CONTRACT.md create mode 100644 src/PureSharp.Analyzers.Tests/CallContractTests.cs diff --git a/docs/CALL-CONTRACT.md b/docs/CALL-CONTRACT.md new file mode 100644 index 0000000..2e49449 --- /dev/null +++ b/docs/CALL-CONTRACT.md @@ -0,0 +1,170 @@ +# PureSharp `[PureMethod]` Call Contract + +**How `[PureMethod]` behaves across call boundaries, and how far v1.0 analyses.** + +This document specifies the call contract enforced by `RT0002`. For the purity model +itself see [`PURITY-SEMANTICS.md`](PURITY-SEMANTICS.md); for the diagnostic contract see +[`DIAGNOSTICS.md`](DIAGNOSTICS.md). + +Every behaviour below was **observed** by running the analyzer and is locked by +`CallContractTests`. + +## Design goal + +v1.0 deliberately does **not** attempt unrestricted whole-program analysis. The goal is a +contract that is **decidable, reproducible, and fast** inside a Roslyn analyzer: + +- decidable from the current compilation alone, +- independent of build order and of which assemblies happen to have source available, +- linear in the size of the analysed code. + +Whole-program purity inference would fail all three. + +## The contract + +> `[PureMethod]` is a **declared contract on a symbol**, not an inferred property of an +> implementation. + +From a `[PureMethod]` method you may call: + +1. a method whose **statically resolved symbol** carries `[PureMethod]`, or +2. a method on a **known-pure type**. + +Everything else is `RT0002`. PureSharp never opens the callee's body to decide whether it +happens to be pure — an unmarked method is treated as impure, always. + +This is a **fail-closed** rule: it can over-report, never under-report, for the calls it +covers. + +## Resolution rules + +The contract is checked against the symbol the compiler resolves the call to. This has +consequences worth stating explicitly, because they are easy to get wrong. + +| Call shape | Where `[PureMethod]` must be | Behaviour | +|---|---|---| +| Interface method | On the **interface declaration** | Attribute on the implementing class does **not** satisfy a call made through the interface — the call resolves to the interface member | +| `virtual` method called through the base type | On the **base declaration** | Attribute on the `override` alone does **not** satisfy it | +| `override` called through the derived type | On the resolved (derived) symbol | Normal resolution applies | +| Overloads | On the **specific overload** selected | Each overload is judged independently | +| Extension method | On the extension method itself | Resolves to the static method | +| Static method | On the method | Normal resolution applies | +| Recursion, mutual recursion | On **every** participant | One unmarked participant produces `RT0002` at that call site | +| Generic method | On the generic definition | Type arguments do not affect the decision | + +### Consequence: virtual dispatch is not sound + +Marking a base `virtual` method `[PureMethod]` permits every call made through the base +type, but an override may be impure. PureSharp does not verify that overrides honour the +base contract. + +```csharp +public class Base { [PureMethod] public virtual int M() => 1; } +public class Derived : Base { public override int M() { Console.WriteLine(); return 2; } } +``` + +A call to `Base.M()` from a pure method is accepted, and `Derived.M()` is not checked +against the base's contract. **Marking a virtual or interface member `[PureMethod]` is an +assertion the author is responsible for upholding in every override.** + +Verifying that overrides preserve the contract is a candidate for a future diagnostic +(see Open decisions). + +## Interprocedural scope + +**In scope for v1.0:** exactly one level — the call site, judged against the resolved +callee's declared attribute. + +**Not in scope for v1.0:** + +- Reading the callee's body to infer purity +- Propagating purity transitively through unmarked methods +- Verifying that overrides honour a base `[PureMethod]` contract +- Whole-program or cross-compilation analysis +- Purity of delegate targets (see `PURITY-SEMANTICS.md`) + +The analysis performs **no cross-method traversal**. Each call site is decided from the +resolved symbol's attributes and containing type name alone, which is what keeps the cost +linear. + +### Not covered by the call contract + +Two call-like constructs are not analysed as invocations at all: + +| Construct | Status | +|---|---| +| User-defined property getter | **Not checked.** Property references are inspected only for I/O types, so a getter running arbitrary code is invisible. | +| Constructor (`new T()`) | **Not checked.** Object creation is not an invocation operation here, so a constructor body doing anything at all is invisible. | + +Both are false negatives, locked by `FALSE_NEGATIVE_*` tests in `CallContractTests`. + +## External dependencies + +**Decision: external assemblies are handled by the same fail-closed rule, with no special +casing.** + +A method from an assembly PureSharp does not control cannot carry `[PureMethod]`, so: + +- if its containing type is on the **known-pure list**, the call is allowed; +- otherwise the call is `RT0002`. + +```csharp +[PureMethod] public object Run() => Math.Abs(-1); // allowed +[PureMethod] public object Run() => new StringBuilder().ToString(); // RT0002 +``` + +The alternatives were rejected: + +| Alternative | Why rejected | +|---|---| +| Read external metadata/IL to infer purity | Not decidable in an analyzer; depends on whether reference assemblies or full IL are available; not reproducible across build environments | +| Trust external methods by default | Fails open — silently permits arbitrary I/O | +| Honour a `[Pure]`-style attribute from other libraries | `System.Diagnostics.Contracts.PureAttribute` has weaker, inconsistently applied semantics; adopting it would import an unverified guarantee | + +The consequence is accepted: the known-pure list is an **allowlist**, and any pure BCL +type absent from it over-reports. Growing that list is a non-breaking change (it narrows +detection), so gaps can be fixed in minor releases. + +## Performance + +Measured on the analyzer as shipped, on synthetic compilations of `[PureMethod]` methods +each containing a pure call, an arithmetic call, and a local assignment. + +| Methods analysed | Analyzer time | Per method | +|---|---|---| +| 100 | 186 ms | 1.86 ms | +| 500 | 349 ms | 0.70 ms | +| 2 000 | 844 ms | 0.42 ms | + +Observations: + +- Cost grows **linearly** with the number of analysed operations. Per-method cost falls as + fixed startup cost is amortised; the 100-method figure is dominated by JIT warm-up. +- Analyzer time is of the same order as the baseline compilation of the same source + (roughly 0.8–1.1×), which is the expected range for an operation-walking analyzer. +- There is no super-linear behaviour, because no call graph is built and no callee body is + visited. This is the practical payoff of the one-level contract. + +**Method.** Build a `CSharpCompilation` from generated source, wrap it with +`WithAnalyzers`, and time `GetAnalyzerDiagnosticsAsync()`. `CallContractTests` +contains a reproducible guard at 2 000 methods; its bound is deliberately generous +(60 s) so it detects catastrophic regressions without becoming flaky on shared CI. + +Absolute numbers are machine-dependent and are recorded for **shape**, not as a +threshold to enforce. + +## Open decisions + +Each would be a breaking change under `DIAGNOSTICS.md` (widening detection → major +release) and needs a product decision. + +1. **Override contract verification** — report when an `override` of a `[PureMethod]` + member is not itself pure. Would close the virtual-dispatch soundness gap. +2. **Attribute inheritance** — should an `override` inherit the base's `[PureMethod]`, so + marking only the override is unnecessary and calls through the derived type behave + consistently? +3. **Property getters** — treat a user-defined getter as an invocation for contract + purposes. +4. **Constructors** — bring object creation under the call contract. +5. **Local functions** — let a local function inherit the enclosing method's contract, so + its invocation stops producing `RT0002` (see `PURITY-SEMANTICS.md`, gap 7). diff --git a/docs/DIAGNOSTICS.md b/docs/DIAGNOSTICS.md index 9c5fabd..6a035f0 100644 --- a/docs/DIAGNOSTICS.md +++ b/docs/DIAGNOSTICS.md @@ -20,6 +20,8 @@ with `[PureMethod]`**. The purity model these diagnostics approximate — and, importantly, the cases v1.0 does **not** detect — is specified in [`PURITY-SEMANTICS.md`](PURITY-SEMANTICS.md). +How `RT0002` treats calls across method, interface, and assembly boundaries is specified +in [`CALL-CONTRACT.md`](CALL-CONTRACT.md). | Field | Value | |---|---| diff --git a/docs/PURITY-SEMANTICS.md b/docs/PURITY-SEMANTICS.md index c30ed77..d7ef5f3 100644 --- a/docs/PURITY-SEMANTICS.md +++ b/docs/PURITY-SEMANTICS.md @@ -150,7 +150,7 @@ analysed in v1.0. An unmarked method is reported (`RT0002`) without inspecting its body, so PureSharp never concludes that an unmarked method *is* pure. The reach of the `[PureMethod]` contract -across call boundaries is specified separately — see Issue #10. +across call boundaries is specified in [`CALL-CONTRACT.md`](CALL-CONTRACT.md). ### 7. Local functions diff --git a/src/PureSharp.Analyzers.Tests/CallContractTests.cs b/src/PureSharp.Analyzers.Tests/CallContractTests.cs new file mode 100644 index 0000000..1b190f1 --- /dev/null +++ b/src/PureSharp.Analyzers.Tests/CallContractTests.cs @@ -0,0 +1,240 @@ +using System; +using System.Collections.Immutable; +using System.Diagnostics; +using System.Linq; +using System.Text; +using System.Threading.Tasks; +using Microsoft.CodeAnalysis; +using Microsoft.CodeAnalysis.CSharp; +using Microsoft.CodeAnalysis.Diagnostics; +using Xunit; + +namespace PureSharp.Analyzers.Tests; + +/// +/// [PureMethod] 呼び出し契約の仕様テスト。 +/// +/// docs/CALL-CONTRACT.md が定義する「契約は静的に解決されたシンボルに対して +/// 判定される」という原則と、interprocedural analysis の対象範囲を固定する。 +/// +public class CallContractTests +{ + private const string Attr = @" +namespace PureSharp.Core +{ + [System.AttributeUsage(System.AttributeTargets.Method, Inherited = false, AllowMultiple = false)] + public sealed class PureMethodAttribute : System.Attribute { } +} +"; + + private static string Source(string body, string members = "", string outer = "") => @" +using PureSharp.Core; +using System; +using System.Collections.Generic; +using System.Linq; +" + outer + @" +public class Probe +{ +" + members + @" + [PureMethod] + public object Run() + { +" + body + @" + } +} +" + Attr; + + private static async Task AssertIdsAsync(string source, params string[] expected) + { + var diagnostics = await AnalyzerProbe.RunAsync(new ReferentialTransparencyAnalyzer(), source); + var actual = diagnostics.Select(d => d.Id).OrderBy(x => x, StringComparer.Ordinal).ToArray(); + Assert.Equal(expected, actual); + } + + // ========================================================= + // 原則: 契約は「静的に解決されたシンボル」に対して判定される + // ========================================================= + + [Fact] + public async Task Interface_AttributeOnDeclaration_NoDiagnostic() + => await AssertIdsAsync(Source( + "return t.M();", + "private IThing t;", + "public interface IThing { [PureMethod] int M(); }")); + + [Fact] + public async Task Interface_AttributeOnImplementationOnly_ReportsRT0002() + // 呼び出しは interface メンバに解決されるため、実装側の [PureMethod] は + // 契約を満たさない。属性は宣言側に付ける必要がある。 + => await AssertIdsAsync(Source( + "return t.M();", + "private IThing t;", + "public interface IThing { int M(); } public class Impl : IThing { [PureMethod] public int M() => 1; }"), + "RT0002"); + + [Fact] + public async Task Virtual_AttributeOnBase_NoDiagnostic() + => await AssertIdsAsync(Source( + "return b.M();", + "private Base b;", + "public class Base { [PureMethod] public virtual int M() => 1; } public class Derived : Base { public override int M() => 2; }")); + + [Fact] + public async Task Virtual_AttributeOnOverrideOnly_ReportsRT0002() + // base 型経由の呼び出しは base のシンボルに解決されるため、override 側の + // [PureMethod] は効かない。 + => await AssertIdsAsync(Source( + "return b.M();", + "private Base b;", + "public class Base { public virtual int M() => 1; } public class Derived : Base { [PureMethod] public override int M() => 2; }"), + "RT0002"); + + [Fact] + public async Task Virtual_Unmarked_ReportsRT0002() + => await AssertIdsAsync(Source( + "return b.M();", + "private Base b;", + "public class Base { public virtual int M() => 1; }"), + "RT0002"); + + // ========================================================= + // Overload 解決 + // ========================================================= + + [Fact] + public async Task Overload_ResolvedToMarkedOverload_NoDiagnostic() + => await AssertIdsAsync(Source( + "return H(1);", + "[PureMethod] private int H(int x) => x; private int H(string s) => 0;")); + + [Fact] + public async Task Overload_ResolvedToUnmarkedOverload_ReportsRT0002() + => await AssertIdsAsync(Source( + "return H(\"a\");", + "[PureMethod] private int H(int x) => x; private int H(string s) => 0;"), + "RT0002"); + + // ========================================================= + // Extension method + // ========================================================= + + [Fact] + public async Task ExtensionMethod_Marked_NoDiagnostic() + => await AssertIdsAsync(Source( + "return this.Ext();", + "", + "public static class Ex { [PureMethod] public static int Ext(this Probe p) => 1; }")); + + [Fact] + public async Task ExtensionMethod_Unmarked_ReportsRT0002() + => await AssertIdsAsync(Source( + "return this.Ext();", + "", + "public static class Ex { public static int Ext(this Probe p) => 1; }"), + "RT0002"); + + // ========================================================= + // 再帰 / 相互再帰 + // ========================================================= + + [Fact] + public async Task MutualRecursion_BothMarked_NoDiagnostic() + => await AssertIdsAsync(Source( + "return A(1);", + "[PureMethod] private int A(int n) => n <= 0 ? 0 : B(n - 1); " + + "[PureMethod] private int B(int n) => n <= 0 ? 0 : A(n - 1);")); + + [Fact] + public async Task MutualRecursion_OneUnmarked_ReportsRT0002() + => await AssertIdsAsync(Source( + "return A(1);", + "[PureMethod] private int A(int n) => n <= 0 ? 0 : B(n - 1); " + + "private int B(int n) => n <= 0 ? 0 : A(n - 1);"), + "RT0002"); + + [Fact] + public async Task StaticMarkedMethod_NoDiagnostic() + => await AssertIdsAsync(Source("return S();", "[PureMethod] private static int S() => 1;")); + + // ========================================================= + // External dependency + // ========================================================= + + [Fact] + public async Task ExternalAssembly_UnmarkedType_ReportsRT0002() + // 外部アセンブリの型は [PureMethod] を付けられないため、既知純粋型 + // リストに含まれない限り常に RT0002 になる (fail-closed)。 + => await AssertIdsAsync( + Source("return new System.Text.StringBuilder().ToString();"), + "RT0002"); + + [Fact] + public async Task ExternalAssembly_KnownPureType_NoDiagnostic() + => await AssertIdsAsync(Source("return Math.Abs(-1);")); + + // ========================================================= + // 対象範囲外 (FALSE NEGATIVE) + // ========================================================= + + [Fact] + public async Task FALSE_NEGATIVE_UserPropertyGetter_NotDetected() + // プロパティ参照は I/O 型かどうかしか見ていないため、任意のコードを + // 実行しうるユーザー定義 getter は呼び出し契約の対象外。 + => await AssertIdsAsync(Source("return Q;", "private int Q => 1;")); + + [Fact] + public async Task FALSE_NEGATIVE_Constructor_NotDetected() + // オブジェクト生成は invocation として解析されないため、コンストラクタ本体は + // 呼び出し契約の対象外。 + => await AssertIdsAsync(Source( + "return new Other();", "", "public class Other { public Other() { } }")); + + // ========================================================= + // Performance guard + // ========================================================= + + [Fact] + public async Task Analyzer_ScalesLinearly_AndCompletesWithinGenerousBound() + { + // docs/CALL-CONTRACT.md の測定を再現可能にするための guard。 + // 厳密な閾値は環境差でフレークになるため、破滅的な性能退行のみを検出する + // 十分に緩い上限を用いる。 + var source = GenerateMethods(2000); + + var references = AppDomain.CurrentDomain.GetAssemblies() + .Where(a => !a.IsDynamic && !string.IsNullOrEmpty(a.Location)) + .Select(a => (MetadataReference)MetadataReference.CreateFromFile(a.Location)) + .ToImmutableArray(); + + var compilation = CSharpCompilation.Create( + "PerfGuard", + new[] { CSharpSyntaxTree.ParseText(source) }, + references, + new CSharpCompilationOptions(OutputKind.DynamicallyLinkedLibrary)); + + var withAnalyzers = compilation.WithAnalyzers( + ImmutableArray.Create(new ReferentialTransparencyAnalyzer())); + + var stopwatch = Stopwatch.StartNew(); + var diagnostics = await withAnalyzers.GetAnalyzerDiagnosticsAsync(); + stopwatch.Stop(); + + Assert.Empty(diagnostics); + Assert.True(stopwatch.Elapsed < TimeSpan.FromSeconds(60), + $"Analyzing 2000 pure methods took {stopwatch.Elapsed}, which indicates a severe regression."); + } + + private static string GenerateMethods(int count) + { + var sb = new StringBuilder(); + sb.AppendLine("using PureSharp.Core;"); + sb.AppendLine("using System;"); + sb.AppendLine("public class Big {"); + sb.AppendLine(" [PureMethod] private int Helper(int x) => x + 1;"); + for (var i = 0; i < count; i++) + sb.AppendLine($" [PureMethod] public int M{i}(int a) {{ var v = Helper(a); v = v + Math.Abs(a); return v + {i}; }}"); + sb.AppendLine("}"); + sb.AppendLine(Attr); + return sb.ToString(); + } +}