From 9a93f7454e4ea07627909ec4f6fac85dacabbf62 Mon Sep 17 00:00:00 2001 From: elecball Date: Fri, 2 Oct 2026 10:50:18 +0000 Subject: [PATCH 1/2] [Link] add the verified coreutils link benchmark Implement GNU link with its specification, proof, parity tests, documentation, and fuzzer support. Validation: - make check TASK=link - cargo test Co-authored-by: OpenAI Codex --- bench/utils/link/Link.dfy | 74 +++++ bench/utils/link/LinkCli.dfy | 20 ++ bench/utils/link/LinkCore.dfy | 111 ++++++++ bench/utils/link/LinkProof.dfy | 17 ++ bench/utils/link/LinkSchema.dfy | 64 +++++ bench/utils/link/LinkSpec.dfy | 181 ++++++++++++ bench/utils/link/Makefile | 14 + bench/utils/link/Tests.py | 267 ++++++++++++++++++ bench/utils/link/benchmark.yaml | 8 + bench/utils/link/dfyconfig.toml | 6 + bench/utils/link/link.md | 99 +++++++ .../src/fuzz/input/generators/link.rs | 117 ++++++++ .../src/fuzz/input/generators/mod.rs | 1 + .../src/utils/capabilities.rs | 6 +- 14 files changed, 983 insertions(+), 2 deletions(-) create mode 100644 bench/utils/link/Link.dfy create mode 100644 bench/utils/link/LinkCli.dfy create mode 100644 bench/utils/link/LinkCore.dfy create mode 100644 bench/utils/link/LinkProof.dfy create mode 100644 bench/utils/link/LinkSchema.dfy create mode 100644 bench/utils/link/LinkSpec.dfy create mode 100644 bench/utils/link/Makefile create mode 100644 bench/utils/link/Tests.py create mode 100644 bench/utils/link/benchmark.yaml create mode 100644 bench/utils/link/dfyconfig.toml create mode 100644 bench/utils/link/link.md create mode 100644 tools/coreutils_fuzzer/src/fuzz/input/generators/link.rs diff --git a/bench/utils/link/Link.dfy b/bench/utils/link/Link.dfy new file mode 100644 index 00000000..e5a4db04 --- /dev/null +++ b/bench/utils/link/Link.dfy @@ -0,0 +1,74 @@ +include "../../core/BenchmarkItem.dfy" +include "../../core/Utf8.dfy" +include "LinkSpec.dfy" +include "LinkCore.dfy" +include "LinkProof.dfy" + +module Link { + import BenchIO + import BenchWorld + import BenchItem + import CliTypes + import Utf8 = Utf8Semantics + import S = LinkSchema + import Core = LinkCore + import Spec = LinkSpec + import Proof = LinkProof + import opened CliExtern + + class LinkBenchmarkItem extends BenchItem.BenchmarkItemTwostate { + constructor() {} + + method Name() returns (name: string) { + name := "link"; + } + + method Schema() returns (schema: CliTypes.CliSchema) { + schema := S.Schema(); + } + + method ParseConfig() returns (cfg: CliTypes.ParseConfig) { + cfg := S.ParserConfig(); + } + + method Decode(parsed: CliTypes.ParsedArgs) returns (raw: S.LinkCmdRaw) { + raw := S.Decode(parsed); + } + + method FormatParseError(err: CliTypes.ParseError) returns (msg: BenchWorld.Bytes) { + msg := Spec.ParseErrorText(err); + } + + method PlanParseFailure( + e: CliTypes.ParseError, + argv: seq + ) returns (plan: CliTypes.CliPlan) + decreases * + { + if 0 < e.tokenIndex && e.tokenIndex < |argv| { + var s := S.Schema(); + var cfg := S.ParserConfig(); + var result := Cli.Parse(argv[..e.tokenIndex], s, cfg); + match result { + case ParseSuccess(parsed) => + var raw := S.Decode(parsed); + if raw.mode == S.ModeHelp || raw.mode == S.ModeVersion { + plan := CliTypes.CliRun(raw); + return; + } + case ParseFailure(_) => + } + } + var msg := Spec.ParseErrorText(e); + plan := CliTypes.CliEarlyExit(1, [], msg); + } + + method RunCore(raw: S.LinkCmdRaw, io: BenchIO.IO) returns (exit: int) + modifies io.fsRegion, io.stdoutRegion, io.stderrRegion + ensures Spec.Spec(raw, io, exit) + { + exit := Core.RunCore(raw, io); + Proof.CoreSummaryImpliesSpec(raw, io, exit); + } + } +} diff --git a/bench/utils/link/LinkCli.dfy b/bench/utils/link/LinkCli.dfy new file mode 100644 index 00000000..620d2bcd --- /dev/null +++ b/bench/utils/link/LinkCli.dfy @@ -0,0 +1,20 @@ +include "Link.dfy" + +module LinkCli { + import BenchIO + import BenchItem + import Link + + method {:main} Main(args: seq) + modifies BenchIO.Process().Footprint() + decreases * + { + // Match the repository's .NET entry convention. + var effectiveArgs := if |args| > 0 && args[0] == "dotnet" then args[1..] else args; + var argv := ["link"] + effectiveArgs; + var io := BenchIO.Process(); + var item := new Link.LinkBenchmarkItem(); + var exit := BenchItem.RunMain(item, argv, io); + BenchIO.Exit(exit); + } +} diff --git a/bench/utils/link/LinkCore.dfy b/bench/utils/link/LinkCore.dfy new file mode 100644 index 00000000..0ad8903d --- /dev/null +++ b/bench/utils/link/LinkCore.dfy @@ -0,0 +1,111 @@ +include "../../core/IO.dfy" +include "LinkSchema.dfy" +include "LinkSpec.dfy" + +module LinkCore { + import BenchIO + import BenchWorld + import Schema = LinkSchema + import Spec = LinkSpec + import C = IOContract + import Utf8 = Utf8Semantics + + twostate predicate CoreSummary(raw: Schema.LinkCmdRaw, io: BenchIO.IO, exit: int) + reads io.Footprint() + { + if raw.mode == Schema.ModeHelp then + io.fs() == old(io.fs()) && + io.stdout() == old(io.stdout()) + Spec.HelpTextSpec() && + io.stderr() == old(io.stderr()) && + exit == 0 + else if raw.mode == Schema.ModeVersion then + io.fs() == old(io.fs()) && + io.stdout() == old(io.stdout()) + Spec.VersionTextSpec() && + io.stderr() == old(io.stderr()) && + exit == 0 + else if raw.mode != Schema.ModeRun then + match raw.mode + case ModeExtraOperand(operand) => + io.fs() == old(io.fs()) && + io.stdout() == old(io.stdout()) && + io.stderr() == old(io.stderr()) + + Spec.ExtraOperandText(C.QuoteArgumentResult(Utf8.Encode(operand))) && + exit == 1 + case _ => false + else if |raw.operands| == 0 then + io.fs() == old(io.fs()) && + io.stdout() == old(io.stdout()) && + io.stderr() == old(io.stderr()) + Spec.MissingOperandText() && + exit == 1 + else if |raw.operands| == 1 then + io.fs() == old(io.fs()) && + io.stdout() == old(io.stdout()) && + io.stderr() == old(io.stderr()) + + Spec.MissingOperandAfterText( + C.QuoteArgumentResult(Utf8.Encode(raw.operands[0])) + ) && + exit == 1 + else + exists ok: bool, err: int :: + Spec.LinkResult(io, raw.operands[0], raw.operands[1], ok, err) && + io.stdout() == old(io.stdout()) && + (if ok then + io.stderr() == old(io.stderr()) && exit == 0 + else + io.stderr() == old(io.stderr()) + + Spec.CannotCreateLinkText( + C.QuoteafPathResult(raw.operands[1]), + C.QuoteafPathResult(raw.operands[0]), + C.CLocaleErrnoTextResult(err) + ) && + exit == 1) + } + + method RunCore(raw: Schema.LinkCmdRaw, io: BenchIO.IO) returns (exit: int) + modifies io.fsRegion, io.stdoutRegion, io.stderrRegion + ensures CoreSummary(raw, io, exit) + { + if raw.mode == Schema.ModeHelp { + var _, _ := io.WriteStdout(Spec.HelpTextSpec(), BenchWorld.ThrowOnError); + exit := 0; + } else if raw.mode == Schema.ModeVersion { + var _, _ := io.WriteStdout(Spec.VersionTextSpec(), BenchWorld.ThrowOnError); + exit := 0; + } else if raw.mode.ModeExtraOperand? { + var quotedOperand := io.QuoteArgument(Utf8.Encode(raw.mode.operand)); + var _, _ := io.WriteStderr(Spec.ExtraOperandText(quotedOperand), BenchWorld.ThrowOnError); + exit := 1; + } else if |raw.operands| == 0 { + var _, _ := io.WriteStderr(Spec.MissingOperandText(), BenchWorld.ThrowOnError); + exit := 1; + } else if |raw.operands| == 1 { + var quotedSource := io.QuoteArgument(Utf8.Encode(raw.operands[0])); + var _, _ := io.WriteStderr( + Spec.MissingOperandAfterText(quotedSource), + BenchWorld.ThrowOnError + ); + exit := 1; + } else { + var source := raw.operands[0]; + var target := raw.operands[1]; + var ok, err := io.CreateHardLink(source, target); + assert Spec.LinkResult(io, source, target, ok, err); + + if ok { + exit := 0; + } else { + var reason := io.GetCLocaleErrnoText(err); + var quotedTarget := io.QuoteafPath(target); + var quotedSource := io.QuoteafPath(source); + var _, _ := io.WriteStderr( + Spec.CannotCreateLinkText(quotedTarget, quotedSource, reason), + BenchWorld.ThrowOnError + ); + exit := 1; + + assert C.GetCLocaleErrnoTextSpec(err, reason); + assert Spec.LinkResult(io, source, target, ok, err); + } + } + } +} diff --git a/bench/utils/link/LinkProof.dfy b/bench/utils/link/LinkProof.dfy new file mode 100644 index 00000000..b327704f --- /dev/null +++ b/bench/utils/link/LinkProof.dfy @@ -0,0 +1,17 @@ +include "LinkSpec.dfy" +include "LinkCore.dfy" + +module LinkProof { + import BenchIO + import Schema = LinkSchema + import Core = LinkCore + import Spec = LinkSpec + + twostate lemma CoreSummaryImpliesSpec( + raw: Schema.LinkCmdRaw, io: BenchIO.IO, exit: int) + requires Core.CoreSummary(raw, io, exit) + ensures Spec.Spec(raw, io, exit) + { + + } +} diff --git a/bench/utils/link/LinkSchema.dfy b/bench/utils/link/LinkSchema.dfy new file mode 100644 index 00000000..76b4bc93 --- /dev/null +++ b/bench/utils/link/LinkSchema.dfy @@ -0,0 +1,64 @@ +include "../../core/CliTypes.dfy" + +module LinkSchema { + import CliTypes + + datatype LinkMode = ModeRun | ModeHelp | ModeVersion | ModeExtraOperand(operand: string) + + datatype LinkCmdRaw = LinkCmdRaw( + mode: LinkMode, + operands: seq + ) + + method Schema() returns (schema: CliTypes.CliSchema) + { + schema := CliTypes.CliSchema([ + CliTypes.OptionDecl("link.help", [], ["help"], CliTypes.NoArg), + CliTypes.OptionDecl("link.version", [], ["version"], CliTypes.NoArg) + ], true); + } + + method ParserConfig() returns (cfg: CliTypes.ParseConfig) + { + cfg := CliTypes.ParseConfig(CliTypes.GNU_Permute, false, true, true); + } + + method Decode(parsed: CliTypes.ParsedArgs) returns (raw: LinkCmdRaw) + { + var seenHelp := false; + var seenVersion := false; + var helpTokenIndex := -1; + var versionTokenIndex := -1; + var i := 0; + while i < |parsed.options| + decreases |parsed.options| - i + { + var option := parsed.options[i]; + + if option.key == "link.help" { + seenHelp := true; + if helpTokenIndex == -1 || option.tokenIndex < helpTokenIndex { + helpTokenIndex := option.tokenIndex; + } + } + if option.key == "link.version" { + seenVersion := true; + if versionTokenIndex == -1 || option.tokenIndex < versionTokenIndex { + versionTokenIndex := option.tokenIndex; + } + } + + i := i + 1; + } + var mode := if seenHelp && (!seenVersion || helpTokenIndex <= versionTokenIndex) then + ModeHelp + else if seenVersion then + ModeVersion + else if |parsed.positionals| > 2 then + ModeExtraOperand(parsed.positionals[2]) + else + ModeRun; + + raw := LinkCmdRaw(mode, parsed.positionals); + } +} diff --git a/bench/utils/link/LinkSpec.dfy b/bench/utils/link/LinkSpec.dfy new file mode 100644 index 00000000..4ceec0e8 --- /dev/null +++ b/bench/utils/link/LinkSpec.dfy @@ -0,0 +1,181 @@ +include "LinkSchema.dfy" +include "../../core/IO.dfy" +include "../../core/Utf8.dfy" +include "../../core/CliModel.dfy" + +module LinkSpec { + import BenchIO + import BenchWorld + import CliTypes + import Schema = LinkSchema + import Utf8 = Utf8Semantics + import CliModel + import C = IOContract + + function HelpTextSpec(): BenchWorld.Bytes + { + "Usage: link FILE1 FILE2\n" + + " or: link OPTION\n" + + "Call the link function to create a link named FILE2 to an existing FILE1.\n" + + "\n" + + " --help\n" + + " display this help and exit\n" + + " --version\n" + + " output version information and exit\n" + + "\n" + + "Report bugs to: bug-coreutils@gnu.org\n" + + "GNU coreutils home page: \n" + + "General help using GNU software: \n" + + "Report any translation bugs to \n" + + "Full documentation \n" + + "or available locally via: info '(coreutils) link invocation'\n" + } + + function VersionTextSpec(): BenchWorld.Bytes + { + "link (GNU coreutils) 9.10.13-2cf49\n" + + "Copyright (C) 2026 Free Software Foundation, Inc.\n" + + "License GPLv3+: GNU GPL version 3 or later .\n" + + "This is free software: you are free to change and redistribute it.\n" + + "There is NO WARRANTY, to the extent permitted by law.\n" + + "\n" + + "Written by Michael Stone.\n" + } + + function LongOptionName(token: string): string + { + var eq := CliModel.FindChar(token, '='); + var name := if eq >= 0 then token[..eq] else token; + if |name| > 2 && CliModel.HasPrefix(name, "--") then + var abbreviation := name[2..]; + if CliModel.HasPrefix("help", abbreviation) then "--help" + else if CliModel.HasPrefix("version", abbreviation) then "--version" + else name + else name + } + + function ParseErrorText(err: CliTypes.ParseError): BenchWorld.Bytes + { + var text := if err.kind == CliTypes.UnknownOption then + if |err.rawToken| > 2 && err.rawToken[0] == '-' && err.rawToken[1] == '-' then + "link: unrecognized option '" + err.rawToken + "'\n" + + "Try 'link --help' for more information.\n" + else if |err.rawToken| > 1 && err.rawToken[0] == '-' then + "link: invalid option -- '" + [err.rawToken[1]] + "'\n" + + "Try 'link --help' for more information.\n" + else + "link: invalid option\nTry 'link --help' for more information.\n" + else if err.kind == CliTypes.UnexpectedValue then + "link: option '" + LongOptionName(err.rawToken) + + "' doesn't allow an argument\n" + + "Try 'link --help' for more information.\n" + else if err.kind == CliTypes.Ambiguous then + "link: option '" + err.rawToken + "' is ambiguous\n" + + "Try 'link --help' for more information.\n" + else + "link: " + + (if err.kind == CliTypes.MissingValue + then "missing option value" + else "parse error") + + " at token '" + err.rawToken + "'\n"; + Utf8.Encode(text) + } + + twostate predicate LinkResult( + io: BenchIO.IO, + source: BenchWorld.Path, + target: BenchWorld.Path, + ok: bool, + err: int + ) + reads io.fsRegion, io.nowRegion, io.trustedFilesystemRegion + { + C.CreateHardLinkSpec( + old(io.fs()), + old(io.now()), + old(io.trustedFilesystem()), + io.fs(), + source, + target, + ok, + err + ) + } + + function MissingOperandText(): BenchWorld.Bytes + { + "link: missing operand\n" + + "Try 'link --help' for more information.\n" + } + + function MissingOperandAfterText( + quotedSource: BenchWorld.Bytes + ): BenchWorld.Bytes + { + "link: missing operand after " + quotedSource + "\n" + + "Try 'link --help' for more information.\n" + } + + function ExtraOperandText(quotedOperand: BenchWorld.Bytes): BenchWorld.Bytes + { + "link: extra operand " + quotedOperand + "\n" + + "Try 'link --help' for more information.\n" + } + + function CannotCreateLinkText( + quotedTarget: BenchWorld.Bytes, + quotedSource: BenchWorld.Bytes, + reason: string + ): BenchWorld.Bytes + { + "link: cannot create link " + quotedTarget + " to " + quotedSource + ": " + + Utf8.Encode(reason) + "\n" + } + + twostate predicate Spec(raw: Schema.LinkCmdRaw, io: BenchIO.IO, exit: int) + reads io.Footprint() + { + if raw.mode == Schema.ModeHelp then + io.fs() == old(io.fs()) && + io.stdout() == old(io.stdout()) + HelpTextSpec() && + io.stderr() == old(io.stderr()) && + exit == 0 + else if raw.mode == Schema.ModeVersion then + io.fs() == old(io.fs()) && + io.stdout() == old(io.stdout()) + VersionTextSpec() && + io.stderr() == old(io.stderr()) && + exit == 0 + else if raw.mode != Schema.ModeRun then + match raw.mode + case ModeExtraOperand(operand) => + io.fs() == old(io.fs()) && + io.stdout() == old(io.stdout()) && + io.stderr() == old(io.stderr()) + + ExtraOperandText(C.QuoteArgumentResult(Utf8.Encode(operand))) && + exit == 1 + case _ => false + else if |raw.operands| == 0 then + io.fs() == old(io.fs()) && + io.stdout() == old(io.stdout()) && + io.stderr() == old(io.stderr()) + MissingOperandText() && + exit == 1 + else if |raw.operands| == 1 then + io.fs() == old(io.fs()) && + io.stdout() == old(io.stdout()) && + io.stderr() == old(io.stderr()) + + MissingOperandAfterText( + C.QuoteArgumentResult(Utf8.Encode(raw.operands[0])) + ) && + exit == 1 + else + exists ok: bool, err: int :: + LinkResult(io, raw.operands[0], raw.operands[1], ok, err) && + io.stdout() == old(io.stdout()) && + (if ok then + io.stderr() == old(io.stderr()) && exit == 0 + else + io.stderr() == old(io.stderr()) + + CannotCreateLinkText(C.QuoteafPathResult(raw.operands[1]), C.QuoteafPathResult(raw.operands[0]), C.CLocaleErrnoTextResult(err)) && + exit == 1) + } +} diff --git a/bench/utils/link/Makefile b/bench/utils/link/Makefile new file mode 100644 index 00000000..6bf21a50 --- /dev/null +++ b/bench/utils/link/Makefile @@ -0,0 +1,14 @@ +PROJECT_DIR := $(abspath $(dir $(lastword $(MAKEFILE_LIST)))) +REPO_ROOT := $(abspath $(PROJECT_DIR)/../../..) +LOCAL_TASK := $(notdir $(PROJECT_DIR)) + +.PHONY: build verify test + +build: + python3 -m benchmarks.make_tasks build --root "$(REPO_ROOT)" --task "$(LOCAL_TASK)" + +verify: + python3 -m benchmarks.verify --project "$(PROJECT_DIR)" --library "$(PROJECT_DIR)/../../core" + +test: + python3 -m benchmarks.make_tasks test --root "$(REPO_ROOT)" --task "$(LOCAL_TASK)" diff --git a/bench/utils/link/Tests.py b/bench/utils/link/Tests.py new file mode 100644 index 00000000..f005565e --- /dev/null +++ b/bench/utils/link/Tests.py @@ -0,0 +1,267 @@ +"""GNU parity cases for link.""" + +from pathlib import Path + +import pytest + +from tools.bench_test_support import ( + assert_result_matches_reference, + bench_dll_path, + build_bench_utility, + build_coreutils_utility, + coreutils_binary_path, + evaluation_target_root, + run_bench_utility, + run_coreutils_utility, + run_dafny_verify, +) + +ROOT = evaluation_target_root(Path(__file__).resolve().parents[3]) +UTILITY = "link" +PROJECT = ROOT / "bench" / "utils" / UTILITY + + +@pytest.fixture(scope="session") +def executables() -> tuple[Path, Path]: + """Build the two targets only for runtime cases; local Make targets use -n0.""" + build_bench_utility(ROOT, UTILITY) + build_coreutils_utility(ROOT, UTILITY) + return ( + coreutils_binary_path(ROOT, ROOT / "_build/coreutils/src" / UTILITY), + bench_dll_path(ROOT, ROOT / "_build/bench" / f"{UTILITY}_bench.dll"), + ) + + +def assert_parity( + executables: tuple[Path, Path], + args: list[str], + cwd: Path, + *, + input_data: bytes = b"", +) -> None: + """Compare a read-only scenario, including stderr on error exits.""" + reference, candidate = executables + expected = run_coreutils_utility(reference, UTILITY, args, cwd, input_data=input_data) + actual = run_bench_utility(candidate, args, cwd, input_data=input_data) + assert_result_matches_reference(expected, actual, ignore_stderr_when_exit_nonzero=False) + + +# Missing both operands reports a failure and usage guidance. +def test_missing_operands_match_coreutils(executables: tuple[Path, Path], tmp_path: Path) -> None: + # upstream: none - Adds missing-operand parity. + # upstream-reason: parity. + assert_parity(executables, [], tmp_path) + + +# Supplying only the source identifies that source in the missing-target diagnostic. +def test_missing_target_operand_matches_coreutils( + executables: tuple[Path, Path], tmp_path: Path +) -> None: + # upstream: none - Adds one-operand diagnostic parity. + # upstream-reason: parity. + assert_parity(executables, ["source"], tmp_path) + + +# Extra operands are rejected without creating the requested hard link. +def test_extra_operand_matches_coreutils(executables: tuple[Path, Path], tmp_path: Path) -> None: + # upstream: none - Adds extra-operand parity. + # upstream-reason: parity. + ref_dir = tmp_path / "reference" + bench_dir = tmp_path / "candidate" + for directory in (ref_dir, bench_dir): + directory.mkdir() + (directory / "source").write_bytes(b"payload\n") + + reference, candidate = executables + expected = run_coreutils_utility(reference, UTILITY, ["source", "target", "extra"], ref_dir) + actual = run_bench_utility(candidate, ["source", "target", "extra"], bench_dir) + assert_result_matches_reference(expected, actual, ignore_stderr_when_exit_nonzero=False) + for directory in (ref_dir, bench_dir): + assert not (directory / "target").exists() + assert (directory / "source").read_bytes() == b"payload\n" + + +# Extra-operand diagnostics quote special characters without creating a link. +@pytest.mark.parametrize("operand", ["a'b", 'a"b', "a\nb", "a\tb", "a\\b", "a b"]) +def test_quoted_extra_operand_matches_coreutils( + executables: tuple[Path, Path], tmp_path: Path, operand: str +) -> None: + # upstream: none - Adds GNU argument-quoting parity. + # upstream-reason: parity. + ref_dir = tmp_path / "reference" + bench_dir = tmp_path / "candidate" + for directory in (ref_dir, bench_dir): + directory.mkdir() + (directory / "source").write_bytes(b"payload") + + reference, candidate = executables + expected = run_coreutils_utility(reference, UTILITY, ["source", "target", operand], ref_dir) + actual = run_bench_utility(candidate, ["source", "target", operand], bench_dir) + assert_result_matches_reference(expected, actual, ignore_stderr_when_exit_nonzero=False) + for directory in (ref_dir, bench_dir): + assert not (directory / "target").exists() + + +# Successful execution creates a second name for the source inode. +def test_regular_file_hard_link_matches_coreutils( + executables: tuple[Path, Path], tmp_path: Path +) -> None: + # upstream: coreutils/tests/help/help-version.sh + ref_dir = tmp_path / "reference" + bench_dir = tmp_path / "candidate" + for directory in (ref_dir, bench_dir): + directory.mkdir() + (directory / "source").write_bytes(b"payload\n") + + reference, candidate = executables + expected = run_coreutils_utility(reference, UTILITY, ["source", "target"], ref_dir) + actual = run_bench_utility(candidate, ["source", "target"], bench_dir) + assert_result_matches_reference(expected, actual, ignore_stderr_when_exit_nonzero=False) + assert expected[2] == actual[2] == 0 + for directory in (ref_dir, bench_dir): + source_stat = (directory / "source").stat() + target_stat = (directory / "target").stat() + assert source_stat.st_ino == target_stat.st_ino + assert source_stat.st_nlink == target_stat.st_nlink == 2 + assert (directory / "target").read_bytes() == b"payload\n" + + +# A nonexistent source reports a creation error and leaves the target absent. +def test_missing_source_matches_coreutils(executables: tuple[Path, Path], tmp_path: Path) -> None: + # upstream: none - Adds missing-source parity. + # upstream-reason: parity. + ref_dir = tmp_path / "reference" + bench_dir = tmp_path / "candidate" + ref_dir.mkdir() + bench_dir.mkdir() + reference, candidate = executables + + expected = run_coreutils_utility(reference, UTILITY, ["missing", "target"], ref_dir) + actual = run_bench_utility(candidate, ["missing", "target"], bench_dir) + assert_result_matches_reference(expected, actual, ignore_stderr_when_exit_nonzero=False) + assert expected[2] == actual[2] == 1 + assert not (ref_dir / "target").exists() + assert not (bench_dir / "target").exists() + + +# An existing target reports a creation error and preserves both files. +def test_existing_target_matches_coreutils(executables: tuple[Path, Path], tmp_path: Path) -> None: + # upstream: none - Adds existing-target parity. + # upstream-reason: parity. + ref_dir = tmp_path / "reference" + bench_dir = tmp_path / "candidate" + for directory in (ref_dir, bench_dir): + directory.mkdir() + (directory / "source").write_bytes(b"source contents") + (directory / "target").write_bytes(b"target contents") + + reference, candidate = executables + expected = run_coreutils_utility(reference, UTILITY, ["source", "target"], ref_dir) + actual = run_bench_utility(candidate, ["source", "target"], bench_dir) + assert_result_matches_reference(expected, actual, ignore_stderr_when_exit_nonzero=False) + assert expected[2] == actual[2] == 1 + for directory in (ref_dir, bench_dir): + assert (directory / "source").read_bytes() == b"source contents" + assert (directory / "target").read_bytes() == b"target contents" + + +# Failed creation diagnostics quote special characters in both pathnames. +@pytest.mark.parametrize("source", ["a'b", 'a"b', "a\nb", "a\tb", "a\\b", "a b"]) +def test_quoted_missing_source_matches_coreutils( + executables: tuple[Path, Path], tmp_path: Path, source: str +) -> None: + # upstream: none - Adds GNU path-quoting parity. + # upstream-reason: parity. + assert_parity(executables, [source, "target name"], tmp_path) + + +# An empty source pathname reports the corresponding system error. +def test_empty_source_matches_coreutils(executables: tuple[Path, Path], tmp_path: Path) -> None: + # upstream: none - Adds empty-source parity. + # upstream-reason: parity. + assert_parity(executables, ["", "target"], tmp_path) + + +# A target in a nonexistent directory reports an error without changing the source. +def test_missing_target_parent_matches_coreutils( + executables: tuple[Path, Path], tmp_path: Path +) -> None: + # upstream: none - Adds missing-target-parent parity. + # upstream-reason: parity. + ref_dir = tmp_path / "reference" + bench_dir = tmp_path / "candidate" + for directory in (ref_dir, bench_dir): + directory.mkdir() + (directory / "source").write_bytes(b"payload") + + reference, candidate = executables + expected = run_coreutils_utility(reference, UTILITY, ["source", "missing/target"], ref_dir) + actual = run_bench_utility(candidate, ["source", "missing/target"], bench_dir) + assert_result_matches_reference(expected, actual, ignore_stderr_when_exit_nonzero=False) + assert expected[2] == actual[2] == 1 + for directory in (ref_dir, bench_dir): + assert (directory / "source").read_bytes() == b"payload" + assert not (directory / "missing").exists() + + +# Help exits successfully with the GNU help output. +def test_help_matches_coreutils(executables: tuple[Path, Path], tmp_path: Path) -> None: + # upstream: coreutils/tests/help/help-version.sh + assert_parity(executables, ["--help"], tmp_path) + + +# Version exits successfully with the GNU version output. +def test_version_matches_coreutils(executables: tuple[Path, Path], tmp_path: Path) -> None: + # upstream: coreutils/tests/help/help-version.sh + assert_parity(executables, ["--version"], tmp_path) + + +# An unknown long option produces GNU's option diagnostic. +def test_invalid_option_matches_coreutils(executables: tuple[Path, Path], tmp_path: Path) -> None: + # upstream: coreutils/tests/misc/usage_vs_getopt.sh + assert_parity(executables, ["--thisoptiondoesnotexist"], tmp_path) + + +# Help and version requests take precedence according to their argument order. +@pytest.mark.parametrize( + "args", + [ + ["--help", "--version"], + ["--version", "--help"], + ["--help", "--bad"], + ["--bad", "--help"], + ], +) +def test_option_precedence_matches_coreutils( + executables: tuple[Path, Path], tmp_path: Path, args: list[str] +) -> None: + # upstream: none - Adds mixed-option precedence parity. + # upstream-reason: parity. + assert_parity(executables, args, tmp_path) + + +# The option delimiter permits source and target names beginning with hyphens. +def test_option_like_paths_match_coreutils(executables: tuple[Path, Path], tmp_path: Path) -> None: + # upstream: none - Adds link-specific -- delimiter parity. + # upstream-reason: parity. + ref_dir = tmp_path / "reference" + bench_dir = tmp_path / "candidate" + for directory in (ref_dir, bench_dir): + directory.mkdir() + (directory / "--help").write_bytes(b"payload") + + reference, candidate = executables + expected = run_coreutils_utility(reference, UTILITY, ["--", "--help", "--version"], ref_dir) + actual = run_bench_utility(candidate, ["--", "--help", "--version"], bench_dir) + assert_result_matches_reference(expected, actual, ignore_stderr_when_exit_nonzero=False) + assert expected[2] == actual[2] == 0 + for directory in (ref_dir, bench_dir): + assert (directory / "--help").stat().st_ino == (directory / "--version").stat().st_ino + + +# Check each proof module as well as the entry contract required by make check. +@pytest.mark.dafny_verify +@pytest.mark.parametrize("filename", ["LinkCore.dfy", "LinkProof.dfy", "Link.dfy"]) +def test_verify_module(filename: str) -> None: + # upstream: none - Checks the Dafny proof surface, not GNU runtime behavior. + run_dafny_verify(PROJECT / filename) diff --git a/bench/utils/link/benchmark.yaml b/bench/utils/link/benchmark.yaml new file mode 100644 index 00000000..d1c806f8 --- /dev/null +++ b/bench/utils/link/benchmark.yaml @@ -0,0 +1,8 @@ +schema_version: benchmark.definition.v2 +task_id: "link" +kind: coreutils +source: + status: verified + name: GNU coreutils link + url: https://www.gnu.org/software/coreutils/ + license: GPL-3.0-or-later diff --git a/bench/utils/link/dfyconfig.toml b/bench/utils/link/dfyconfig.toml new file mode 100644 index 00000000..fda4af19 --- /dev/null +++ b/bench/utils/link/dfyconfig.toml @@ -0,0 +1,6 @@ +includes = ["LinkCli.dfy"] + +[options] +target = "cs" +no-verify = true +standard-libraries = false diff --git a/bench/utils/link/link.md b/bench/utils/link/link.md new file mode 100644 index 00000000..91f23ca8 --- /dev/null +++ b/bench/utils/link/link.md @@ -0,0 +1,99 @@ +# link NL Specification + +Source: +- `coreutils/doc/coreutils.texi` +- `@node link invocation` +- Source line range: 10491-10528 +- Implementation: `coreutils/src/link.c` at submodule commit + `2cf491412c199e2211880ec3f4ba387026638a33` +- License: GPL-3.0-or-later + +This file summarizes the upstream GNU `link` behavior relevant to the benchmark. + +## `link`: Make a hard link + +`link` creates one hard link by calling the system's `link` operation. It is a +smaller interface than `ln`: it accepts exactly one existing source name and +one new link name, without replacement, target-directory, or interactive +options. + +```text +link filename linkname +``` + +`filename` must name an existing filesystem object, and `linkname` must not +already exist. The directory containing `linkname` must exist. On success, the +two names refer to the same filesystem object, so changes made through either +name are visible through the other. + +If `filename` is a symbolic link, GNU documents whether the new hard link +refers to the symbolic link itself or to its target as unspecified. Use `ln -P` +or `ln -L` when that distinction must be selected explicitly. + +The command accepts `--help` and `--version`. To use an operand beginning with +`-`, place it after `--` or prefix it with a pathname component such as `./`. + +### Benchmark-Supported Behavior + +The benchmark handles exactly two pathnames, plus `--help`, `--version`, `--`, +GNU long-option abbreviations, and operand, option, and hard-link creation +errors. Zero operands, one operand, and more than two operands produce distinct +GNU-compatible diagnostics without changing the modeled filesystem. + +For ordinary execution, the first pathname is the existing source and the +second is the new target name. The filesystem effect is represented by the +shared `CreateHardLink` operation. Successful creation makes the target an +alias of the source and produces no output. Failures quote the target and +source in GNU's `cannot create link TARGET to SOURCE` diagnostic. + +No GNU `link` options are excluded due to missing `IO.dfy` support. A symbolic +link used as the source is not assigned behavior beyond the platform result, +because GNU documents whether `link` follows it as unspecified. + +### Scope and model + +- **Input and environment:** Finite arguments, GNU long-option handling, Linux + filesystem, current user permissions, and C-locale diagnostics; stdin is + unused. +- **Observation:** Output streams, exit status, and modeled filesystem. Help, + version, parsing, and operand-count errors leave the filesystem unchanged. + Successful creation adds `linkname` as an alias of `filename`. A failed + `CreateHardLinkSpec` uses the trusted filesystem observation and does not by + itself guarantee filesystem preservation; maintainer review is pending. +- **Trusted API:** Shared parser, `CreateHardLinkSpec`, errno text, + argument/path quoting, and stream append contracts in `bench/core` revision + `3699f93aa58aadf89ae69d822312371a98eeca2c`. +- **Proof:** `Link.RunCore` ensures `LinkSpec.Spec` through `LinkProof`. + `Decode` and `LinkCore.RunCore` terminate; whole-process termination is not + proved because the shared CLI entry uses `decreases *`. + +### Validation evidence + +The implementation was checked against GNU coreutils built from the pinned +submodule revision. Differential cases cover missing and extra operands, +argument and path quoting, successful hard-link identity, missing sources, +existing targets, missing target parents, option parsing and precedence, and +pathnames beginning with `-`. + +- `python3 -m benchmarks validate link`: `link: valid`. +- `make test TASK=link`: 28 runtime parity cases passed; 3 proof cases were + deselected by the runtime target. +- `python3 -m pytest -q -n0 --import-mode=importlib -m dafny_verify + bench/utils/link/Tests.py`: 3 proof cases passed; 28 runtime cases were + deselected. +- `python3 tools/coreutils_fuzzer/run.py fuzz link --seeds 1,7,19 + --iterations 1000`: each seed completed 1,000 matches with zero mismatches, + timeouts, incomplete iterations, or other errors. +- `make check TASK=link`: runtime tests, the 20-case automatic fuzz gate, + Dafny verification, proof tests, and definition checks passed. + +The first runtime test run exposed an older help-text layout copied from GNU +coreutils 9.4. The fixed text was updated to the pinned `9.10.13-2cf49` output, +after which all runtime cases passed. These automated results do not replace +the required human specification review. + +### Exit Status + +The supported command exits with status 0 after successful hard-link creation +or a help or version request. Operand, option, and link-creation errors exit +with status 1. diff --git a/tools/coreutils_fuzzer/src/fuzz/input/generators/link.rs b/tools/coreutils_fuzzer/src/fuzz/input/generators/link.rs new file mode 100644 index 00000000..63956e97 --- /dev/null +++ b/tools/coreutils_fuzzer/src/fuzz/input/generators/link.rs @@ -0,0 +1,117 @@ +use super::super::pattern::{ + Alternative, ArgvPattern, Atom, Element, OperandSource, OptionChoice, ValueContext, +}; +use super::super::PatternInputGenerator; +use super::super::{support, system_state}; +use crate::fuzz::{DirSpec, FileSpec, GeneratedCase, HardlinkSpec, UtilityProfile}; +use rand::rngs::StdRng; +use rand::Rng; +use std::path::PathBuf; + +const HELP_OR_VERSION: Atom = Atom::Option(OptionChoice::available(&["--help", "--version"])); +const SOURCE: Atom = Atom::Operand(OperandSource::Generated(link_source)); +const TARGET: Atom = Atom::Operand(OperandSource::Generated(link_target)); +const EXTRA: Atom = Atom::Operand(OperandSource::Target { + existing_percent: 50, +}); + +static ARGV_PATTERN: ArgvPattern = ArgvPattern::new(&[ + Alternative::weighted( + 6, + &[ + Element::repeated(0, 2, HELP_OR_VERSION), + Element::once(SOURCE), + Element::once(TARGET), + Element::up_to_budget(0, EXTRA), + ], + ), + Alternative::weighted( + 2, + &[ + Element::repeated(0, 2, HELP_OR_VERSION), + Element::optional(70, SOURCE), + ], + ), + Alternative::weighted( + 2, + &[ + Element::once(SOURCE), + Element::repeated(1, 2, HELP_OR_VERSION), + Element::optional(80, TARGET), + Element::up_to_budget(0, EXTRA), + ], + ), +]); + +pub(crate) static GENERATOR: PatternInputGenerator = + PatternInputGenerator::patterned(&ARGV_PATTERN, scenario_case).with_profile(UtilityProfile { + requires_path_operand: true, + prefers_existing_paths: true, + }); + +fn link_source(context: &ValueContext<'_>, rng: &mut StdRng) -> String { + let files = support::existing_file_operands(context.fixture()); + support::pick_file_or_missing(&files, rng) +} + +fn link_target(context: &ValueContext<'_>, rng: &mut StdRng) -> String { + let files = support::existing_file_operands(context.fixture()); + if !files.is_empty() && rng.random_bool(0.25) { + return support::pick_string(&files, rng); + } + + let name = format!("hard-link-{}", rng.random_range(0..10000)); + if rng.random_bool(0.15) { + format!("missing-parent/{name}") + } else { + name + } +} + +pub(super) fn scenario_case(iteration: usize) -> Option { + let mut fixture = system_state::basic_fixture(); + let args = match iteration { + 0 => vec!["a.txt", "a-hard"], + 1 => vec![], + 2 => vec!["a.txt"], + 3 => vec!["a.txt", "a-hard", "extra"], + 4 => vec!["missing.txt", "a-hard"], + 5 => vec!["a.txt", "target.txt"], + 6 => vec!["", "a-hard"], + 7 => vec!["a.txt", ""], + 8 => vec!["a.txt", "missing-parent/a-hard"], + 9 => vec!["dir", "dir-hard"], + 10 => vec!["--help", "--version"], + 11 => vec!["--version", "--help"], + 12 => vec!["--help", "--bad"], + 13 => vec!["--bad", "--help"], + 14 => vec!["--help=value"], + 15 => vec!["-x"], + 16 => vec!["--thisoptiondoesnotexist"], + 17 => { + fixture.files.push(FileSpec { + relative_path: PathBuf::from("--help"), + bytes: b"option-like source\n".to_vec(), + mode: 0o644, + }); + vec!["--", "--help", "--version"] + } + 18 => vec!["a'b", "target name"], + 19 => { + fixture.hardlinks.push(HardlinkSpec { + relative_path: PathBuf::from("alias"), + source_relative_path: PathBuf::from("a.txt"), + }); + vec!["alias", "alias-hard"] + } + 20 => { + fixture.directories.push(DirSpec { + relative_path: PathBuf::from("blocked"), + mode: 0o555, + }); + vec!["a.txt", "blocked/a-hard"] + } + _ => return None, + }; + Some(support::case(args, fixture, b"")) +} diff --git a/tools/coreutils_fuzzer/src/fuzz/input/generators/mod.rs b/tools/coreutils_fuzzer/src/fuzz/input/generators/mod.rs index f8776a0f..4382ce3f 100644 --- a/tools/coreutils_fuzzer/src/fuzz/input/generators/mod.rs +++ b/tools/coreutils_fuzzer/src/fuzz/input/generators/mod.rs @@ -14,6 +14,7 @@ pub(crate) mod factor; pub(crate) mod r#false; pub(crate) mod fold; pub(crate) mod head; +pub(crate) mod link; pub(crate) mod ln; pub(crate) mod logname; pub(crate) mod ls; diff --git a/tools/coreutils_fuzzer/src/utils/capabilities.rs b/tools/coreutils_fuzzer/src/utils/capabilities.rs index bf2340d5..2b290565 100644 --- a/tools/coreutils_fuzzer/src/utils/capabilities.rs +++ b/tools/coreutils_fuzzer/src/utils/capabilities.rs @@ -133,6 +133,7 @@ pub(crate) static UTILITY_CAPABILITIES: &[UtilityCapability] = &[ option_value_flags: &["-c", "--bytes", "-n", "--lines"], ..capability!("head", head) }, + capability!("link", link), capability!("ln", ln), capability!("logname", logname), UtilityCapability { @@ -387,8 +388,9 @@ mod tests { assert_eq!( patterned, BTreeSet::from([ - "cat", "chmod", "comm", "csplit", "cut", "du", "expand", "head", "ln", "ls", "mv", - "nl", "paste", "readlink", "stat", "tac", "tail", "touch", "uniq", "unlink", "wc", + "cat", "chmod", "comm", "csplit", "cut", "du", "expand", "head", "link", "ln", + "ls", "mv", "nl", "paste", "readlink", "stat", "tac", "tail", "touch", "uniq", + "unlink", "wc", ]) ); } From ed396e9e2c7d6de4ff0241818b73fbfdb1b95781 Mon Sep 17 00:00:00 2001 From: elecball Date: Sun, 4 Oct 2026 18:37:13 +0000 Subject: [PATCH 2/2] [Link] fix invalid option diagnostics Match GNU output for ambiguous and non-ASCII options. Add randomized malformed-option fuzzing and a regression test. Validation: make check TASK=link; 3,000 fuzz cases passed. Co-authored-by: OpenAI Codex --- bench/utils/link/LinkSpec.dfy | 34 ++++++++++++------ bench/utils/link/Tests.py | 9 +++++ .../src/fuzz/input/generators/link.rs | 36 ++++++++++++++++++- 3 files changed, 68 insertions(+), 11 deletions(-) diff --git a/bench/utils/link/LinkSpec.dfy b/bench/utils/link/LinkSpec.dfy index 4ceec0e8..5708ad2c 100644 --- a/bench/utils/link/LinkSpec.dfy +++ b/bench/utils/link/LinkSpec.dfy @@ -54,31 +54,45 @@ module LinkSpec { else name } + function UnknownShortTemplate(): BenchWorld.Bytes + { + ['l', 'i', 'n', 'k', ':', ' ', 'i', 'n', 'v', 'a', 'l', 'i', 'd', + ' ', 'o', 'p', 't', 'i', 'o', 'n', ' ', '-', '-', ' ', '\'', '\0', + '\'', '\n', 'T', 'r', 'y', ' ', '\'', 'l', 'i', 'n', 'k', ' ', '-', + '-', 'h', 'e', 'l', 'p', '\'', ' ', 'f', 'o', 'r', ' ', 'm', 'o', 'r', + 'e', ' ', 'i', 'n', 'f', 'o', 'r', 'm', 'a', 't', 'i', 'o', 'n', '.', + '\n'] + } + + function UnknownShortText(byte: BenchWorld.RawByte): BenchWorld.Bytes + { + UnknownShortTemplate()[25 := byte] + } + function ParseErrorText(err: CliTypes.ParseError): BenchWorld.Bytes { - var text := if err.kind == CliTypes.UnknownOption then + if err.kind == CliTypes.UnknownOption then if |err.rawToken| > 2 && err.rawToken[0] == '-' && err.rawToken[1] == '-' then - "link: unrecognized option '" + err.rawToken + "'\n" + + "link: unrecognized option '" + Utf8.Encode(err.rawToken) + "'\n" + "Try 'link --help' for more information.\n" else if |err.rawToken| > 1 && err.rawToken[0] == '-' then - "link: invalid option -- '" + [err.rawToken[1]] + "'\n" + - "Try 'link --help' for more information.\n" + UnknownShortText(Utf8.EncodeChar(err.rawToken[1])[0]) else "link: invalid option\nTry 'link --help' for more information.\n" else if err.kind == CliTypes.UnexpectedValue then - "link: option '" + LongOptionName(err.rawToken) + + "link: option '" + Utf8.Encode(LongOptionName(err.rawToken)) + "' doesn't allow an argument\n" + "Try 'link --help' for more information.\n" else if err.kind == CliTypes.Ambiguous then - "link: option '" + err.rawToken + "' is ambiguous\n" + + "link: option '" + Utf8.Encode(err.rawToken) + + "' is ambiguous; possibilities: '--help' '--version'\n" + "Try 'link --help' for more information.\n" else - "link: " + + "link: " + Utf8.Encode( (if err.kind == CliTypes.MissingValue then "missing option value" - else "parse error") + - " at token '" + err.rawToken + "'\n"; - Utf8.Encode(text) + else "parse error")) + + " at token '" + Utf8.Encode(err.rawToken) + "'\n" } twostate predicate LinkResult( diff --git a/bench/utils/link/Tests.py b/bench/utils/link/Tests.py index f005565e..36116fd7 100644 --- a/bench/utils/link/Tests.py +++ b/bench/utils/link/Tests.py @@ -222,6 +222,15 @@ def test_invalid_option_matches_coreutils(executables: tuple[Path, Path], tmp_pa assert_parity(executables, ["--thisoptiondoesnotexist"], tmp_path) +# A non-ASCII short option preserves GNU getopt's first-byte diagnostic. +def test_non_ascii_short_option_matches_coreutils( + executables: tuple[Path, Path], tmp_path: Path +) -> None: + # upstream: none - Adds byte-exact invalid-option diagnostic parity. + # upstream-reason: parity. + assert_parity(executables, ["-é"], tmp_path) + + # Help and version requests take precedence according to their argument order. @pytest.mark.parametrize( "args", diff --git a/tools/coreutils_fuzzer/src/fuzz/input/generators/link.rs b/tools/coreutils_fuzzer/src/fuzz/input/generators/link.rs index 63956e97..558f5029 100644 --- a/tools/coreutils_fuzzer/src/fuzz/input/generators/link.rs +++ b/tools/coreutils_fuzzer/src/fuzz/input/generators/link.rs @@ -1,5 +1,5 @@ use super::super::pattern::{ - Alternative, ArgvPattern, Atom, Element, OperandSource, OptionChoice, ValueContext, + Alternative, ArgvPattern, Atom, Element, OperandSource, OptionChoice, ValueContext, ValueSource, }; use super::super::PatternInputGenerator; use super::super::{support, system_state}; @@ -14,8 +14,10 @@ const TARGET: Atom = Atom::Operand(OperandSource::Generated(link_target)); const EXTRA: Atom = Atom::Operand(OperandSource::Target { existing_percent: 50, }); +const MALFORMED_OPTION: Atom = Atom::Value(ValueSource::Generated(malformed_option)); static ARGV_PATTERN: ArgvPattern = ArgvPattern::new(&[ + Alternative::weighted(2, &[Element::once(MALFORMED_OPTION)]), Alternative::weighted( 6, &[ @@ -68,6 +70,38 @@ fn link_target(context: &ValueContext<'_>, rng: &mut StdRng) -> String { } } +fn random_non_ascii_scalar(rng: &mut StdRng) -> char { + let codepoint = match rng.random_range(0..3) { + 0 => rng.random_range(0x80..=0x7ff), + 1 if rng.random_bool(0.5) => rng.random_range(0x800..=0xd7ff), + 1 => rng.random_range(0xe000..=0xffff), + _ => rng.random_range(0x10000..=0x10ffff), + }; + char::from_u32(codepoint).expect("generated Unicode scalar") +} + +fn malformed_option(_context: &ValueContext<'_>, rng: &mut StdRng) -> String { + let scalar = random_non_ascii_scalar(rng); + match rng.random_range(0..4) { + 0 => { + let suffix_len = rng.random_range(0..=4); + let suffix: String = (0..suffix_len) + .map(|_| rng.random_range(b'a'..=b'z') as char) + .collect(); + format!("--={suffix}") + } + 1 => format!("--={scalar}"), + 2 => format!("--{scalar}"), + _ => { + let suffix_len = rng.random_range(0..=3); + let suffix: String = (0..suffix_len) + .map(|_| rng.random_range(b'a'..=b'z') as char) + .collect(); + format!("-{scalar}{suffix}") + } + } +} + pub(super) fn scenario_case(iteration: usize) -> Option { let mut fixture = system_state::basic_fixture(); let args = match iteration {