From 7095d76fe4f15da0548f7053509449bc0369c4a6 Mon Sep 17 00:00:00 2001 From: jkkms Date: Fri, 23 Oct 2026 16:51:21 +0000 Subject: [PATCH 1/8] [Benchmark] add mkfifo specification, implementation and proof Problem: TODOLIST lists mkfifo as open for contribution (issue #14). Approach: Scope follows GNU src/mkfifo.c and gnulib modechange.c. MODE is specified as abstract syntax with Render and Meaning; the Core parser is proved to invert Render, so "invalid mode" is exact and a valid MODE has one meaning. Each operand is one CreateSpecialNode call and, with -m, one non-following SetFileMode call (GNU lchmod). -Z/--context are left out. Boundaries: new files under bench/utils/mkfifo only; no shared IO change. Validation: make -C bench/utils/mkfifo verify -> 85 declarations, 946 conditions, 0 failed (DAFNY_VERIFICATION_OUTCOME=verified). A local differential smoke run of 36 cases against the pinned GNU build matched. Limitations: work in progress. Tests.py and the fuzzer generator are not written yet; make check and the fuzzing campaigns have not been run. Co-Authored-By: Claude Opus 5.5 --- bench/utils/mkfifo/CliSupport.dfy | 400 +++++++++++++++ bench/utils/mkfifo/Makefile | 14 + bench/utils/mkfifo/Mkfifo.dfy | 92 ++++ bench/utils/mkfifo/MkfifoCli.dfy | 20 + bench/utils/mkfifo/MkfifoCore.dfy | 173 +++++++ bench/utils/mkfifo/MkfifoModeCore.dfy | 153 ++++++ bench/utils/mkfifo/MkfifoModeProof.dfy | 433 +++++++++++++++++ bench/utils/mkfifo/MkfifoProof.dfy | 347 +++++++++++++ bench/utils/mkfifo/MkfifoSchema.dfy | 62 +++ bench/utils/mkfifo/MkfifoSpec.dfy | 643 +++++++++++++++++++++++++ bench/utils/mkfifo/Tests.py | 63 +++ bench/utils/mkfifo/benchmark.yaml | 9 + bench/utils/mkfifo/dfyconfig.toml | 6 + bench/utils/mkfifo/mkfifo.md | 133 +++++ 14 files changed, 2548 insertions(+) create mode 100644 bench/utils/mkfifo/CliSupport.dfy create mode 100644 bench/utils/mkfifo/Makefile create mode 100644 bench/utils/mkfifo/Mkfifo.dfy create mode 100644 bench/utils/mkfifo/MkfifoCli.dfy create mode 100644 bench/utils/mkfifo/MkfifoCore.dfy create mode 100644 bench/utils/mkfifo/MkfifoModeCore.dfy create mode 100644 bench/utils/mkfifo/MkfifoModeProof.dfy create mode 100644 bench/utils/mkfifo/MkfifoProof.dfy create mode 100644 bench/utils/mkfifo/MkfifoSchema.dfy create mode 100644 bench/utils/mkfifo/MkfifoSpec.dfy create mode 100644 bench/utils/mkfifo/Tests.py create mode 100644 bench/utils/mkfifo/benchmark.yaml create mode 100644 bench/utils/mkfifo/dfyconfig.toml create mode 100644 bench/utils/mkfifo/mkfifo.md diff --git a/bench/utils/mkfifo/CliSupport.dfy b/bench/utils/mkfifo/CliSupport.dfy new file mode 100644 index 0000000..7cba65e --- /dev/null +++ b/bench/utils/mkfifo/CliSupport.dfy @@ -0,0 +1,400 @@ +// Task-local CLI protocol scaffolding; not a library of utility algorithms. +include "../../core/IO.dfy" +include "../../core/CliTypes.dfy" +include "../../core/Utf8.dfy" + +module CliModel { + import opened CliTypes + + datatype OptionLookup = OptionMissing | OptionFound(decl: OptionDecl) + datatype LongOptionLookup = LongMissing | LongFound(decl: OptionDecl) | LongAmbiguous + datatype ShortParse = ShortParsed(options: seq, consumesNext: bool) | + ShortFailed(error: ParseError) + + function HasPrefix(text: string, prefix: string): bool + { + |prefix| <= |text| && text[..|prefix|] == prefix + } + + function FindCharFrom(text: string, target: char, i: nat): int + requires i <= |text| + ensures -1 <= FindCharFrom(text, target, i) < |text| + decreases |text| - i + { + if i == |text| then -1 + else if text[i] == target then i as int + else FindCharFrom(text, target, i + 1) + } + + function FindChar(text: string, target: char): int + { + FindCharFrom(text, target, 0) + } + + function {:fuel 20} ContainsChar(chars: seq, target: char): bool + decreases |chars| + { + |chars| > 0 && (chars[0] == target || ContainsChar(chars[1..], target)) + } + + function {:fuel 20} FindShortInDecls(options: seq, short: char): OptionLookup + decreases |options| + { + if |options| == 0 then OptionMissing + else if ContainsChar(options[0].shorts, short) then OptionFound(options[0]) + else FindShortInDecls(options[1..], short) + } + + function {:fuel 20} FindExactLongInNames( + decl: OptionDecl, + names: seq, + name: string + ): OptionLookup + decreases |names| + { + if |names| == 0 then OptionMissing + else if names[0] == name then OptionFound(decl) + else FindExactLongInNames(decl, names[1..], name) + } + + function {:fuel 20} FindExactLong(options: seq, name: string): OptionLookup + decreases |options| + { + if |options| == 0 then OptionMissing + else + match FindExactLongInNames(options[0], options[0].longs, name) + case OptionFound(decl) => OptionFound(decl) + case OptionMissing => FindExactLong(options[1..], name) + } + + function {:fuel 20} PrefixLongDecls( + options: seq, + name: string + ): seq + decreases |options| + { + if |options| == 0 then [] + else (PrefixLongNames(options[0], options[0].longs, name) + + PrefixLongDecls(options[1..], name)) + } + + function {:fuel 20} PrefixLongNames( + decl: OptionDecl, + names: seq, + name: string + ): seq + decreases |names| + { + if |names| == 0 then [] + else ((if HasPrefix(names[0], name) then [decl] else []) + + PrefixLongNames(decl, names[1..], name)) + } + + function FindLongOption( + options: seq, + name: string, + allowAbbrev: bool + ): LongOptionLookup + { + match FindExactLong(options, name) + case OptionFound(decl) => LongFound(decl) + case OptionMissing => + if !allowAbbrev then LongMissing + else + var matches := PrefixLongDecls(options, name); + if |matches| == 0 then LongMissing + else if |matches| == 1 then LongFound(matches[0]) + else LongAmbiguous + } + + function LooksLikeOption(token: string): bool + { + |token| > 1 && token[0] == '-' + } + + function ParseShortFrom( + argv: seq, + options: seq, + tokenIndex: nat, + token: string, + j: nat, + parsed: seq + ): ShortParse + requires tokenIndex < |argv| + requires 1 <= j <= |token| + ensures (ParseShortFrom(argv, options, tokenIndex, token, j, parsed).ShortParsed? && + ParseShortFrom(argv, options, tokenIndex, token, j, parsed).consumesNext) ==> + tokenIndex + 1 < |argv| + decreases |token| - j + { + if j == |token| then ShortParsed(parsed, false) + else + var c := token[j]; + match FindShortInDecls(options, c) + case OptionMissing => + ShortFailed(ParseError(UnknownOption, tokenIndex as int, token)) + case OptionFound(decl) => + if decl.arity == NoArg then + ParseShortFrom( + argv, options, tokenIndex, token, j + 1, + parsed + [OptOccurrence(decl.key, Short(c), None, tokenIndex as int, token)] + ) + else if decl.arity == ReqArg then + if j + 1 < |token| then + ShortParsed( + parsed + [OptOccurrence( + decl.key, Short(c), Some(token[j + 1..]), tokenIndex as int, token + )], + false + ) + else if tokenIndex + 1 < |argv| then + ShortParsed( + parsed + [OptOccurrence( + decl.key, Short(c), Some(argv[tokenIndex + 1]), tokenIndex as int, token + )], + true + ) + else + ShortFailed(ParseError(MissingValue, tokenIndex as int, token)) + else if j + 1 < |token| then + ShortParsed( + parsed + [OptOccurrence( + decl.key, Short(c), Some(token[j + 1..]), tokenIndex as int, token + )], + false + ) + else + ShortParsed( + parsed + [OptOccurrence(decl.key, Short(c), None, tokenIndex as int, token)], + false + ) + } + + function ParseFrom( + argv: seq, + schema: CliSchema, + cfg: ParseConfig, + prog: string, + i: nat, + options: seq, + positionals: seq, + sawDoubleDash: bool, + parsingOptions: bool + ): ParseResult + requires i <= |argv| + decreases |argv| - i + { + if i == |argv| then + ParseSuccess(ParsedArgs(prog, options, positionals, sawDoubleDash)) + else + var token := argv[i]; + if parsingOptions && schema.supportsDoubleDash && token == "--" then + ParseFrom(argv, schema, cfg, prog, i + 1, options, positionals, true, false) + else if parsingOptions && cfg.treatDashAsOperand && token == "-" then + ParseFrom( + argv, schema, cfg, prog, i + 1, options, positionals + [token], + sawDoubleDash, cfg.order != POSIX_StopAtFirst + ) + else if parsingOptions && |token| > 2 && token[0] == '-' && token[1] == '-' then + var longToken := token[2..]; + var eq := FindChar(longToken, '='); + var longName := if eq >= 0 then longToken[..eq] else longToken; + var inlineValue := if eq >= 0 then longToken[eq + 1..] else ""; + var hasInlineValue := eq >= 0; + match FindLongOption(schema.options, longName, cfg.allowLongAbbrev) + case LongAmbiguous => + ParseFailure(ParseError(Ambiguous, i as int, token)) + case LongMissing => + ParseFailure(ParseError(UnknownOption, i as int, token)) + case LongFound(decl) => + if decl.arity == NoArg then + if hasInlineValue then + ParseFailure(ParseError(UnexpectedValue, i as int, token)) + else + ParseFrom( + argv, schema, cfg, prog, i + 1, + options + [OptOccurrence(decl.key, Long(longName), None, i as int, token)], + positionals, sawDoubleDash, parsingOptions + ) + else if decl.arity == ReqArg then + if hasInlineValue then + ParseFrom( + argv, schema, cfg, prog, i + 1, + options + [OptOccurrence( + decl.key, Long(longName), Some(inlineValue), i as int, token + )], + positionals, sawDoubleDash, parsingOptions + ) + else if i + 1 < |argv| then + ParseFrom( + argv, schema, cfg, prog, i + 2, + options + [OptOccurrence( + decl.key, Long(longName), Some(argv[i + 1]), i as int, token + )], + positionals, sawDoubleDash, parsingOptions + ) + else + ParseFailure(ParseError(MissingValue, i as int, token)) + else if hasInlineValue then + ParseFrom( + argv, schema, cfg, prog, i + 1, + options + [OptOccurrence( + decl.key, Long(longName), Some(inlineValue), i as int, token + )], + positionals, sawDoubleDash, parsingOptions + ) + else if i + 1 < |argv| && !LooksLikeOption(argv[i + 1]) then + ParseFrom( + argv, schema, cfg, prog, i + 2, + options + [OptOccurrence( + decl.key, Long(longName), Some(argv[i + 1]), i as int, token + )], + positionals, sawDoubleDash, parsingOptions + ) + else + ParseFrom( + argv, schema, cfg, prog, i + 1, + options + [OptOccurrence(decl.key, Long(longName), None, i as int, token)], + positionals, sawDoubleDash, parsingOptions + ) + else if parsingOptions && |token| > 1 && token[0] == '-' then + if !cfg.allowBundling && |token| > 2 then + ParseFailure(ParseError(UnknownOption, i as int, token)) + else + match ParseShortFrom(argv, schema.options, i, token, 1, options) + case ShortFailed(error) => ParseFailure(error) + case ShortParsed(parsed, consumesNext) => + ParseFrom( + argv, schema, cfg, prog, if consumesNext then i + 2 else i + 1, + parsed, positionals, sawDoubleDash, parsingOptions + ) + else + ParseFrom( + argv, schema, cfg, prog, i + 1, options, positionals + [token], + sawDoubleDash, if cfg.order == POSIX_StopAtFirst then false else parsingOptions + ) + } + + function ParseValue( + argv: seq, + schema: CliSchema, + cfg: ParseConfig + ): ParseResult + { + var hasProg := |argv| > 0 && |argv[0]| > 0 && argv[0][0] != '-'; + ParseFrom( + argv, schema, cfg, + if hasProg then argv[0] else "", + if hasProg then 1 else 0, + [], [], false, true + ) + } +} + +module CliExtern { + import opened CliTypes + import CliModel + + class Cli { + static method Parse( + argv: seq, + schema: CliSchema, + cfg: ParseConfig + ) returns (res: ParseResult) + ensures res == CliModel.ParseValue(argv, schema, cfg) + { + res := CliModel.ParseValue(argv, schema, cfg); + } + + static method ParsePortable( + argv: seq, + schema: CliSchema, + cfg: ParseConfig + ) returns (res: ParseResult) + ensures res == CliModel.ParseValue(argv, schema, cfg) + { + res := CliModel.ParseValue(argv, schema, cfg); + } + } +} + +module BenchItem { + import opened BenchWorld + import BenchIO + import opened CliTypes + import opened CliExtern + import C = IOContract + import Utf8Semantics + + // CLI protocol code is fixed scaffolding. + export + provides BenchWorld, BenchIO, CliTypes + reveals BenchmarkItemTwostate + provides BenchmarkItemTwostate.Name, BenchmarkItemTwostate.Schema + provides BenchmarkItemTwostate.ParseConfig, BenchmarkItemTwostate.Decode + provides BenchmarkItemTwostate.FormatParseError, BenchmarkItemTwostate.PlanParsed + provides BenchmarkItemTwostate.PlanParseFailure, BenchmarkItemTwostate.PlanArgv + provides BenchmarkItemTwostate.RunCore, RunMain + + trait {:termination false} BenchmarkItemTwostate { + method Name() returns (name: string) + method Schema() returns (schema: CliSchema) + method ParseConfig() returns (cfg: ParseConfig) + method Decode(parsed: ParsedArgs) returns (raw: CmdRaw) + method FormatParseError(err: ParseError) returns (msg: Bytes) + method PlanParsed(parsed: ParsedArgs) returns (plan: CliPlan) + decreases * + { + var raw := Decode(parsed); + plan := CliRun(raw); + } + + method PlanArgv(argv: seq) returns (plan: CliPlan) + decreases * + { + var schema := Schema(); + var cfg := ParseConfig(); + var parseRes := Cli.Parse(argv, schema, cfg); + + match parseRes { + case ParseFailure(err) => + plan := PlanParseFailure(err, argv); + case ParseSuccess(parsed) => + plan := PlanParsed(parsed); + } + } + + method RunCore(raw: CmdRaw, io: BenchIO.IO) returns (exit: int) + modifies io.Footprint() + decreases * + + method PlanParseFailure(err: ParseError, argv: seq) returns (plan: CliPlan) + decreases * + { + var msg := FormatParseError(err); + plan := CliEarlyExit(1, [], msg); + } + } + + method RunMain(item: BenchmarkItemTwostate, argv: seq, io: BenchIO.IO) returns (exit: int) + modifies io.Footprint() + decreases * + { + var plan := item.PlanArgv(argv); + + match plan { + case CliRun(raw) => + exit := item.RunCore(raw, io); + case CliEarlyExit(code, stdout, stderr) => + var stdoutResult := io.WriteStdout(stdout); + var diagnostic := stderr; + if stdoutResult.Err? { + var name := item.Name(); + var reason := io.GetCLocaleErrnoText(C.ResultErrno(stdoutResult)); + diagnostic := diagnostic + Utf8Semantics.Encode(name + ": write error: " + reason + "\n"); + } + var stderrResult := io.WriteStderr(diagnostic); + exit := if stdoutResult.Err? || stderrResult.Err? then 1 else code; + } + } +} diff --git a/bench/utils/mkfifo/Makefile b/bench/utils/mkfifo/Makefile new file mode 100644 index 0000000..d26aad6 --- /dev/null +++ b/bench/utils/mkfifo/Makefile @@ -0,0 +1,14 @@ +PROJECT_DIR := $(abspath $(dir $(lastword $(MAKEFILE_LIST)))) +REPO_ROOT := $(abspath $(PROJECT_DIR)/../../..) +LOCAL_TASK := mkfifo + +.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/mkfifo/Mkfifo.dfy b/bench/utils/mkfifo/Mkfifo.dfy new file mode 100644 index 0000000..d70efb4 --- /dev/null +++ b/bench/utils/mkfifo/Mkfifo.dfy @@ -0,0 +1,92 @@ +include "MkfifoSpec.dfy" +include "CliSupport.dfy" +include "MkfifoCore.dfy" +include "MkfifoProof.dfy" + +module Mkfifo { + // CLI codecs are fixed protocol details, outside the candidate API. + export + provides BenchIO, BenchWorld, BenchItem, CliTypes, CliExtern, S, Core, Spec, Proof, MkfifoBenchmarkItem._ctor, MkfifoBenchmarkItem.Name, MkfifoBenchmarkItem.Schema, MkfifoBenchmarkItem.ParseConfig, MkfifoBenchmarkItem.Decode, MkfifoBenchmarkItem.FormatParseError, MkfifoBenchmarkItem.PlanParsed, MkfifoBenchmarkItem.PlanParseFailure, MkfifoBenchmarkItem.RunCore + reveals MkfifoBenchmarkItem + + import BenchIO + import BenchWorld + import BenchItem + import CliTypes + import opened CliExtern + import S = MkfifoSchema + import Core = MkfifoCore + import Spec = MkfifoSpec + import Proof = MkfifoProof + + class MkfifoBenchmarkItem extends BenchItem.BenchmarkItemTwostate { + constructor() {} + + method Name() returns (name: string) { + name := "mkfifo"; + } + + 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.MkfifoCmdRaw) { + raw := S.Decode(parsed); + } + + method FormatParseError(err: CliTypes.ParseError) returns (msg: BenchWorld.Bytes) { + msg := Spec.ParseErrorText(err); + } + + // GNU handles --help/--version as soon as getopt reaches them, then reports + // a missing operand; MODE is checked only after that. + method PlanParsed(parsed: CliTypes.ParsedArgs) + returns (plan: CliTypes.CliPlan) + { + var request := S.InformationRequest(parsed); + if request == CliTypes.RequestHelp { + plan := CliTypes.CliEarlyExit(0, Spec.HelpTextSpec(), []); + } else if request == CliTypes.RequestVersion { + plan := CliTypes.CliEarlyExit(0, Spec.VersionTextSpec(), []); + } else if |parsed.positionals| == 0 { + plan := CliTypes.CliEarlyExit(1, [], Spec.MissingOperandText()); + } else { + var raw := S.Decode(parsed); + plan := CliTypes.CliRun(raw); + } + } + + // An earlier --help/--version wins over a later parse error, as in getopt. + method PlanParseFailure(e: CliTypes.ParseError, argv: seq) + returns (plan: CliTypes.CliPlan) + { + if 0 < e.tokenIndex < |argv| { + var schema := S.Schema(); + var cfg := S.ParserConfig(); + var result := Cli.Parse(argv[..e.tokenIndex], schema, cfg); + match result { + case ParseSuccess(parsed) => + var request := S.InformationRequest(parsed); + if request != CliTypes.RequestNone { + plan := PlanParsed(parsed); + return; + } + case ParseFailure(_) => + } + } + var msg := FormatParseError(e); + plan := CliTypes.CliEarlyExit(1, [], msg); + } + + method RunCore(raw: S.MkfifoCmdRaw, io: BenchIO.IO) returns (exit: int) + modifies io.fsRegion, io.stderrRegion + ensures Spec.Spec(raw, io, exit) + { + exit := Core.RunCore(raw, io); + } + } +} diff --git a/bench/utils/mkfifo/MkfifoCli.dfy b/bench/utils/mkfifo/MkfifoCli.dfy new file mode 100644 index 0000000..2988a76 --- /dev/null +++ b/bench/utils/mkfifo/MkfifoCli.dfy @@ -0,0 +1,20 @@ +include "Mkfifo.dfy" + +module MkfifoCli { + import BenchIO + import BenchItem + import Mkfifo + + 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 := ["mkfifo"] + effectiveArgs; + var io := BenchIO.Process(); + var item := new Mkfifo.MkfifoBenchmarkItem(); + var exit := BenchItem.RunMain(item, argv, io); + BenchIO.Exit(exit); + } +} diff --git a/bench/utils/mkfifo/MkfifoCore.dfy b/bench/utils/mkfifo/MkfifoCore.dfy new file mode 100644 index 0000000..9cba331 --- /dev/null +++ b/bench/utils/mkfifo/MkfifoCore.dfy @@ -0,0 +1,173 @@ +include "../../core/Utf8.dfy" +include "MkfifoSpec.dfy" +include "MkfifoModeCore.dfy" +include "MkfifoProof.dfy" + +module MkfifoCore { + import BenchIO + import BW = BenchWorld + import C = IOContract + import Schema = MkfifoSchema + import Spec = MkfifoSpec + import P = MkfifoModeCore + import Proof = MkfifoProof + + method FormatOutcome(path: string, outcome: Spec.OperandOutcome, io: BenchIO.IO) + returns (piece: BW.Bytes) + ensures piece == Spec.OutcomeDiagnostic(path, outcome) + { + match outcome { + case Created => + piece := []; + case CreateFailed(err) => + var quoted := io.QuoteafPath(path); + var reason := io.GetCLocaleErrnoText(err); + piece := Spec.CreateFailureText(quoted, reason); + case PermissionFailed(err) => + var quoted := io.QuoteafPath(path); + var reason := io.GetCLocaleErrnoText(err); + piece := Spec.PermissionFailureText(quoted, reason); + } + } + + // All diagnostics are written to stderr once, after the operands. + method Flush(diagnostics: BW.Bytes, runExit: int, io: BenchIO.IO) returns (exit: int) + modifies io.stderrRegion + ensures Spec.StderrResult(old(io.stderr()), io.stderr(), io.trustedStreams(), + diagnostics, runExit, exit) + { + ghost var observations := io.trustedStreams(); + ghost var beforeErr := io.stderr(); + var errResult := io.WriteStderr(diagnostics); + ghost var errObservation := observations(BW.StreamWriteStderr(beforeErr, diagnostics)); + assert errObservation.StreamWriteResult? && errObservation.err == C.ResultErrno(errResult); + exit := if runExit == 0 && C.ResultErrno(errResult) == 0 then 0 else 1; + } + + // Decides the MODE plan before any operand, as GNU does. + method DecideMode(raw: Schema.MkfifoCmdRaw, io: BenchIO.IO) returns (plan: Spec.ModePlan) + ensures Proof.ComputedPlan(raw, C.GetUmaskResultFields(io.props()), plan) + { + plan := Spec.NoModeOption; + if raw.mode.Some? { + var umask := io.GetUmask(); + var parsed := P.ParseMode(raw.mode.value); + if parsed.None? { + plan := Spec.RejectInvalidMode; + } else { + var bits := Spec.Meaning(parsed.value, umask); + plan := if Spec.OnlyPermissionBits(bits) then Spec.ExplicitMode(bits) + else Spec.RejectSpecialBits; + } + } + } + + // One operand: create the FIFO and, with -m, set its permissions. + method ProcessOperand(path: string, plan: Spec.ModePlan, createMode: bv32, io: BenchIO.IO) + returns (outcome: Spec.OperandOutcome, piece: BW.Bytes) + requires plan.NoModeOption? || plan.ExplicitMode? + requires createMode == (if plan.ExplicitMode? then plan.bits else Spec.MKFIFO_BASE_MODE) + modifies io.fsRegion + ensures Spec.OperandStep(old(io.fs()), io.fs(), path, plan, io.now(), io.umask(), + io.trustedFilesystem(), io.trustedNativeFailures(), outcome) + ensures piece == Spec.OutcomeDiagnostic(path, outcome) + { + // Keep the native contracts folded: the lemmas only pass them along. + hide C.CreateSpecialNodeSpec(); + hide C.SetFileModeSpec(); + hide *; + var created := io.CreateSpecialNode(path, BW.FifoNode, createMode, 0, 0); + assert Proof.CreateFact(old(io.fs()), io.now(), io.trustedFilesystem(), io.umask(), io.fs(), path, + createMode, created.Ok?, C.ResultErrno(created)) by { + reveal Proof.CreateFact(); + } + if created.Err? || plan.NoModeOption? { + outcome := if created.Ok? then Spec.Created else Spec.CreateFailed(C.ResultErrno(created)); + Proof.StepCreateOnly(old(io.fs()), io.fs(), path, plan, io.now(), io.umask(), + io.trustedFilesystem(), io.trustedNativeFailures(), + created.Ok?, C.ResultErrno(created), outcome); + } else { + ghost var mid := io.fs(); + var changed := io.SetFileMode(path, false, plan.bits); + assert Proof.PermissionFact(mid, io.now(), io.trustedNativeFailures(), io.fs(), path, + plan.bits, changed.Ok?, C.ResultErrno(changed)) by { + reveal Proof.PermissionFact(); + } + outcome := if changed.Ok? then Spec.Created else Spec.PermissionFailed(C.ResultErrno(changed)); + Proof.StepCreateThenPermission(old(io.fs()), mid, io.fs(), path, plan, io.now(), io.umask(), + io.trustedFilesystem(), io.trustedNativeFailures(), + C.ResultErrno(created), changed.Ok?, C.ResultErrno(changed), + outcome); + } + piece := FormatOutcome(path, outcome, io); + } + + method RunOperands(paths: seq, plan: Spec.ModePlan, io: BenchIO.IO) + returns (diagnostics: BW.Bytes, runExit: int) + requires plan.NoModeOption? || plan.ExplicitMode? + modifies io.fsRegion + ensures Spec.PlanRun(paths, plan, old(io.fs()), io.fs(), io.now(), io.umask(), + io.trustedFilesystem(), io.trustedNativeFailures(), diagnostics, runExit) + { + // The relations are used only through the Proof lemmas. + hide *; + var createMode := if plan.ExplicitMode? then plan.bits else Spec.MKFIFO_BASE_MODE; + diagnostics := []; + runExit := 0; + ghost var states := [io.fs()]; + ghost var outcomes: seq := []; + ghost var cuts: seq := [0]; + Proof.EmptyLoop(paths, plan, io.fs(), io.now(), io.umask(), io.trustedFilesystem(), + io.trustedNativeFailures()); + var i := 0; + while i < |paths| + modifies io.fsRegion + invariant 0 <= i <= |paths| + invariant Proof.LoopState(paths, i, plan, old(io.fs()), io.fs(), io.now(), io.umask(), + io.trustedFilesystem(), io.trustedNativeFailures(), + states, outcomes, cuts, diagnostics, runExit) + decreases |paths| - i + { + ghost var before := io.fs(); + var outcome, piece := ProcessOperand(paths[i], plan, createMode, io); + Proof.ExtendLoop(paths, i, plan, old(io.fs()), before, io.fs(), io.now(), io.umask(), + io.trustedFilesystem(), io.trustedNativeFailures(), + states, outcomes, cuts, diagnostics, runExit, outcome, piece); + states := states + [io.fs()]; + cuts := cuts + [|diagnostics| + |piece|]; + outcomes := outcomes + [outcome]; + diagnostics := diagnostics + piece; + runExit := if outcome.Created? then runExit else 1; + i := i + 1; + } + Proof.FinishLoop(paths, plan, old(io.fs()), io.fs(), io.now(), io.umask(), + io.trustedFilesystem(), io.trustedNativeFailures(), + states, outcomes, cuts, diagnostics, runExit); + } + + method {:isolate_assertions} RunCore(raw: Schema.MkfifoCmdRaw, io: BenchIO.IO) returns (exit: int) + modifies io.fsRegion, io.stderrRegion + ensures Spec.Spec(raw, io, exit) + { + hide *; + ghost var modeUmask := C.GetUmaskResultFields(io.props()); + var plan := DecideMode(raw, io); + Proof.ComputedPlanIsSpecPlan(raw, modeUmask, plan); + var paths := Schema.Operands(raw); + var diagnostics: BW.Bytes; + var runExit: int; + if plan.RejectInvalidMode? || plan.RejectSpecialBits? { + diagnostics := if plan.RejectInvalidMode? then Spec.InvalidModeText() else Spec.SpecialBitsText(); + runExit := 1; + Proof.RejectRun(paths, plan, io.fs(), io.now(), io.umask(), + io.trustedFilesystem(), io.trustedNativeFailures(), diagnostics, runExit); + } else { + diagnostics, runExit := RunOperands(paths, plan, io); + } + Proof.AssembleRun(raw, plan, old(io.fs()), io.fs(), io.now(), io.umask(), modeUmask, + io.trustedFilesystem(), io.trustedNativeFailures(), diagnostics, runExit); + ghost var runExitValue := runExit; + exit := Flush(diagnostics, runExit, io); + Proof.Complete(raw, io, diagnostics, runExitValue, exit); + } +} diff --git a/bench/utils/mkfifo/MkfifoModeCore.dfy b/bench/utils/mkfifo/MkfifoModeCore.dfy new file mode 100644 index 0000000..e0cd4b7 --- /dev/null +++ b/bench/utils/mkfifo/MkfifoModeCore.dfy @@ -0,0 +1,153 @@ +include "MkfifoSpec.dfy" + +// Executable MODE parser. It reads the string from left to right, as GNU +// mode_compile does, and builds the abstract syntax defined in MkfifoSpec. +// MkfifoModeProof shows that it inverts MkfifoSpec.Render. +module MkfifoModeCore { + import S = MkfifoSpec + + datatype Option = None | Some(value: T) + + predicate IsWhoChar(c: char) { c == 'u' || c == 'g' || c == 'o' || c == 'a' } + predicate IsOpChar(c: char) { c == '+' || c == '-' || c == '=' } + predicate IsCopyChar(c: char) { c == 'u' || c == 'g' || c == 'o' } + predicate IsPermChar(c: char) { c == 'r' || c == 'w' || c == 'x' || c == 'X' || c == 's' || c == 't' } + predicate IsOctalChar(c: char) { '0' <= c <= '7' } + + function WhoOf(c: char): S.Who + requires IsWhoChar(c) + { + if c == 'u' then S.WhoU else if c == 'g' then S.WhoG else if c == 'o' then S.WhoO else S.WhoA + } + + function OpOf(c: char): S.OpSym + requires IsOpChar(c) + { + if c == '+' then S.OpAdd else if c == '-' then S.OpRemove else S.OpSet + } + + function SrcOf(c: char): S.CopySrc + requires IsCopyChar(c) + { + if c == 'u' then S.FromU else if c == 'g' then S.FromG else S.FromO + } + + function PermOf(c: char): S.Perm + requires IsPermChar(c) + { + if c == 'r' then S.PermR + else if c == 'w' then S.PermW + else if c == 'x' then S.PermX + else if c == 'X' then S.PermCondX + else if c == 's' then S.PermS + else S.PermT + } + + function DigitOf(c: char): S.OctDigit + requires IsOctalChar(c) + { + c as int - '0' as int + } + + // Each Take* function consumes the longest prefix of one character class. + + function TakeWho(s: string): (r: (seq, string)) + ensures |r.1| <= |s| + decreases |s| + { + if |s| > 0 && IsWhoChar(s[0]) then + var rest := TakeWho(s[1..]); + ([WhoOf(s[0])] + rest.0, rest.1) + else ([], s) + } + + function TakePerms(s: string): (r: (seq, string)) + ensures |r.1| <= |s| + decreases |s| + { + if |s| > 0 && IsPermChar(s[0]) then + var rest := TakePerms(s[1..]); + ([PermOf(s[0])] + rest.0, rest.1) + else ([], s) + } + + function TakeDigits(s: string): (r: (seq, string)) + ensures |r.1| <= |s| + ensures |s| > 0 && IsOctalChar(s[0]) ==> |r.0| > 0 + decreases |s| + { + if |s| > 0 && IsOctalChar(s[0]) then + var rest := TakeDigits(s[1..]); + ([DigitOf(s[0])] + rest.0, rest.1) + else ([], s) + } + + // The text right after an operator: one copy letter, a digit run, or permission letters. + function TakeRhs(s: string): (r: (S.Rhs, string)) + ensures |r.1| <= |s| + ensures r.0.Octal? ==> |r.0.digits| > 0 + { + if |s| > 0 && IsCopyChar(s[0]) then (S.Copy(SrcOf(s[0])), s[1..]) + else if |s| > 0 && IsOctalChar(s[0]) then + var d := TakeDigits(s); + (S.Octal(d.0), d.1) + else + var p := TakePerms(s); + (S.Perms(p.0), p.1) + } + + // One or more actions; s starts with an operator. + function TakeActions(s: string): (r: (seq, string)) + requires |s| > 0 && IsOpChar(s[0]) + ensures |r.0| > 0 && |r.1| < |s| + decreases |s| + { + var rhs := TakeRhs(s[1..]); + var a := S.Action(OpOf(s[0]), rhs.0); + if |rhs.1| > 0 && IsOpChar(rhs.1[0]) then + var more := TakeActions(rhs.1); + ([a] + more.0, more.1) + else ([a], rhs.1) + } + + // A clause and the unread rest, or None if the clause is malformed. + function TakeClause(s: string): (r: Option<(S.Clause, string)>) + ensures r.Some? ==> |r.value.1| < |s| && S.ClauseWellFormed(r.value.0) + { + var w := TakeWho(s); + if |w.1| == 0 || !IsOpChar(w.1[0]) then None + else + var acts := TakeActions(w.1); + var c := S.Clause(w.0, acts.0); + if S.ClauseWellFormed(c) then Some((c, acts.1)) else None + } + + // Clauses separated by ',' up to the end of s. + function ParseClauses(s: string): (r: Option>) + ensures r.Some? ==> |r.value| > 0 && forall c :: c in r.value ==> S.ClauseWellFormed(c) + decreases |s| + { + match TakeClause(s) + case None => None + case Some(cr) => + var (c, rest) := cr; + if |rest| == 0 then Some([c]) + else if rest[0] == ',' then + match ParseClauses(rest[1..]) + case None => None + case Some(cs) => Some([c] + cs) + else None + } + + function ParseMode(s: string): (r: Option) + ensures r.Some? ==> S.WellFormed(r.value) + { + if |s| > 0 && IsOctalChar(s[0]) then + var d := TakeDigits(s); + if |d.1| == 0 && S.OctalValue(d.0) <= S.ALLM then Some(S.Absolute(d.0)) else None + else + match ParseClauses(s) + case None => None + case Some(cs) => Some(S.Symbolic(cs)) + } +} diff --git a/bench/utils/mkfifo/MkfifoModeProof.dfy b/bench/utils/mkfifo/MkfifoModeProof.dfy new file mode 100644 index 0000000..8b29802 --- /dev/null +++ b/bench/utils/mkfifo/MkfifoModeProof.dfy @@ -0,0 +1,433 @@ +include "MkfifoSpec.dfy" +include "MkfifoModeCore.dfy" + +// The parser in MkfifoModeCore inverts MkfifoSpec.Render: +// - completeness: ParseMode(Render(e)) == Some(e) for every well-formed e; +// - soundness: ParseMode(s) == Some(e) implies Render(e) == s. +// Together they make "invalid mode" exact and give each valid MODE one meaning. +module MkfifoModeProof { + import S = MkfifoSpec + import P = MkfifoModeCore + + // --------------------------------------------------------------------------- + // Characters + // --------------------------------------------------------------------------- + + lemma WhoCharRoundTrip(w: S.Who) + ensures P.IsWhoChar(S.WhoChar(w)) && P.WhoOf(S.WhoChar(w)) == w + ensures !P.IsOpChar(S.WhoChar(w)) && !P.IsOctalChar(S.WhoChar(w)) + {} + + lemma OpCharRoundTrip(o: S.OpSym) + ensures P.IsOpChar(S.OpChar(o)) && P.OpOf(S.OpChar(o)) == o + ensures !P.IsWhoChar(S.OpChar(o)) && !P.IsPermChar(S.OpChar(o)) + ensures !P.IsCopyChar(S.OpChar(o)) && !P.IsOctalChar(S.OpChar(o)) + {} + + lemma PermCharRoundTrip(p: S.Perm) + ensures P.IsPermChar(S.PermChar(p)) && P.PermOf(S.PermChar(p)) == p + ensures !P.IsCopyChar(S.PermChar(p)) && !P.IsOctalChar(S.PermChar(p)) + {} + + lemma SrcCharRoundTrip(src: S.CopySrc) + ensures P.IsCopyChar(S.SrcChar(src)) && P.SrcOf(S.SrcChar(src)) == src + {} + + lemma DigitCharRoundTrip(d: S.OctDigit) + ensures P.IsOctalChar(S.DigitChar(d)) && P.DigitOf(S.DigitChar(d)) == d + ensures !P.IsCopyChar(S.DigitChar(d)) + {} + + lemma WhoOfRoundTrip(c: char) + requires P.IsWhoChar(c) + ensures S.WhoChar(P.WhoOf(c)) == c + {} + + lemma OpOfRoundTrip(c: char) + requires P.IsOpChar(c) + ensures S.OpChar(P.OpOf(c)) == c + {} + + lemma PermOfRoundTrip(c: char) + requires P.IsPermChar(c) + ensures S.PermChar(P.PermOf(c)) == c + {} + + lemma SrcOfRoundTrip(c: char) + requires P.IsCopyChar(c) + ensures S.SrcChar(P.SrcOf(c)) == c + {} + + lemma DigitOfRoundTrip(c: char) + requires P.IsOctalChar(c) + ensures S.DigitChar(P.DigitOf(c)) == c + {} + + // --------------------------------------------------------------------------- + // Completeness: reading a rendered prefix gives back the syntax + // --------------------------------------------------------------------------- + + lemma TakeWhoOfRender(ws: seq, rest: string) + requires |rest| == 0 || !P.IsWhoChar(rest[0]) + ensures P.TakeWho(S.RenderWho(ws) + rest) == (ws, rest) + decreases |ws| + { + if |ws| > 0 { + WhoCharRoundTrip(ws[0]); + var s := S.RenderWho(ws) + rest; + assert s == [S.WhoChar(ws[0])] + (S.RenderWho(ws[1..]) + rest); + assert s[1..] == S.RenderWho(ws[1..]) + rest; + TakeWhoOfRender(ws[1..], rest); + assert [ws[0]] + ws[1..] == ws; + } else { + assert S.RenderWho(ws) + rest == rest; + } + } + + lemma TakePermsOfRender(ps: seq, rest: string) + requires |rest| == 0 || !P.IsPermChar(rest[0]) + ensures P.TakePerms(S.RenderPerms(ps) + rest) == (ps, rest) + decreases |ps| + { + if |ps| > 0 { + PermCharRoundTrip(ps[0]); + var s := S.RenderPerms(ps) + rest; + assert s == [S.PermChar(ps[0])] + (S.RenderPerms(ps[1..]) + rest); + assert s[1..] == S.RenderPerms(ps[1..]) + rest; + TakePermsOfRender(ps[1..], rest); + assert [ps[0]] + ps[1..] == ps; + } else { + assert S.RenderPerms(ps) + rest == rest; + } + } + + lemma TakeDigitsOfRender(ds: seq, rest: string) + requires |rest| == 0 || !P.IsOctalChar(rest[0]) + ensures P.TakeDigits(S.RenderDigits(ds) + rest) == (ds, rest) + decreases |ds| + { + if |ds| > 0 { + DigitCharRoundTrip(ds[0]); + var s := S.RenderDigits(ds) + rest; + assert s == [S.DigitChar(ds[0])] + (S.RenderDigits(ds[1..]) + rest); + assert s[1..] == S.RenderDigits(ds[1..]) + rest; + TakeDigitsOfRender(ds[1..], rest); + assert [ds[0]] + ds[1..] == ds; + } else { + assert S.RenderDigits(ds) + rest == rest; + } + } + + // After a right-hand side comes an operator, ',' or the end. + predicate RhsFollower(rest: string) + { + |rest| == 0 || rest[0] == ',' || P.IsOpChar(rest[0]) + } + + lemma TakeRhsOfRender(rhs: S.Rhs, rest: string) + requires RhsFollower(rest) + requires rhs.Octal? ==> |rhs.digits| > 0 + ensures P.TakeRhs(S.RenderRhs(rhs) + rest) == (rhs, rest) + { + var s := S.RenderRhs(rhs) + rest; + match rhs + case Copy(src) => + SrcCharRoundTrip(src); + assert s[0] == S.SrcChar(src) && s[1..] == rest; + case Octal(ds) => + DigitCharRoundTrip(ds[0]); + assert s[0] == S.DigitChar(ds[0]); + TakeDigitsOfRender(ds, rest); + case Perms(ps) => + if |ps| > 0 { + PermCharRoundTrip(ps[0]); + assert s[0] == S.PermChar(ps[0]); + } else { + assert s == rest; + assert |s| == 0 || s[0] == ',' || P.IsOpChar(s[0]); + } + assert |s| == 0 || (!P.IsCopyChar(s[0]) && !P.IsOctalChar(s[0])); + assert P.TakeRhs(s) == (S.Perms(P.TakePerms(s).0), P.TakePerms(s).1); + TakePermsOfRender(ps, rest); + } + + predicate DigitsNonempty(as_: seq) + { + forall i :: 0 <= i < |as_| ==> as_[i].rhs.Octal? ==> |as_[i].rhs.digits| > 0 + } + + lemma TakeActionsOfRender(as_: seq, rest: string) + requires |as_| > 0 && DigitsNonempty(as_) + requires |rest| == 0 || rest[0] == ',' + ensures |S.RenderActions(as_) + rest| > 0 && P.IsOpChar((S.RenderActions(as_) + rest)[0]) + ensures P.TakeActions(S.RenderActions(as_) + rest) == (as_, rest) + decreases |as_| + { + var a := as_[0]; + var tail := as_[1..]; + OpCharRoundTrip(a.op); + var after := S.RenderActions(tail) + rest; + var s := S.RenderActions(as_) + rest; + assert s == [S.OpChar(a.op)] + (S.RenderRhs(a.rhs) + after); + assert s[0] == S.OpChar(a.op); + assert s[1..] == S.RenderRhs(a.rhs) + after; + if |tail| > 0 { + assert DigitsNonempty(tail) by { + forall i | 0 <= i < |tail| ensures tail[i].rhs.Octal? ==> |tail[i].rhs.digits| > 0 { + assert tail[i] == as_[i + 1]; + } + } + TakeActionsOfRender(tail, rest); + TakeRhsOfRender(a.rhs, after); + assert [a] + tail == as_; + } else { + assert after == rest; + TakeRhsOfRender(a.rhs, rest); + assert as_ == [a]; + } + } + + lemma ClauseDigitsNonempty(c: S.Clause) + requires S.ClauseWellFormed(c) + ensures DigitsNonempty(c.actions) + { + forall i | 0 <= i < |c.actions| && c.actions[i].rhs.Octal? + ensures |c.actions[i].rhs.digits| > 0 + { + assert S.ActionWellFormed(c.who, c.actions[i], i == |c.actions| - 1); + } + } + + lemma TakeClauseOfRender(c: S.Clause, rest: string) + requires S.ClauseWellFormed(c) + requires |rest| == 0 || rest[0] == ',' + ensures P.TakeClause(S.RenderClause(c) + rest) == P.Some((c, rest)) + { + ClauseDigitsNonempty(c); + var acts := S.RenderActions(c.actions) + rest; + TakeActionsOfRender(c.actions, rest); + OpCharRoundTrip(c.actions[0].op); + assert S.RenderClause(c) + rest == S.RenderWho(c.who) + acts; + TakeWhoOfRender(c.who, acts); + } + + lemma ParseClausesOfRender(cs: seq) + requires |cs| > 0 && forall c :: c in cs ==> S.ClauseWellFormed(c) + ensures P.ParseClauses(S.RenderClauses(cs)) == P.Some(cs) + decreases |cs| + { + assert cs[0] in cs; + if |cs| == 1 { + TakeClauseOfRender(cs[0], ""); + assert cs == [cs[0]]; + assert S.RenderClauses(cs) == S.RenderClause(cs[0]) + ""; + } else { + var rest := "," + S.RenderClauses(cs[1..]); + TakeClauseOfRender(cs[0], rest); + assert S.RenderClauses(cs) == S.RenderClause(cs[0]) + rest; + assert rest[1..] == S.RenderClauses(cs[1..]); + ParseClausesOfRender(cs[1..]); + assert [cs[0]] + cs[1..] == cs; + } + } + + lemma SymbolicStartsWithoutDigit(cs: seq) + requires |cs| > 0 && forall c :: c in cs ==> S.ClauseWellFormed(c) + ensures |S.RenderClauses(cs)| > 0 && !P.IsOctalChar(S.RenderClauses(cs)[0]) + { + var c := cs[0]; + assert S.ClauseWellFormed(c); + TakeClauseOfRender(c, if |cs| == 1 then "" else "," + S.RenderClauses(cs[1..])); + if |c.who| > 0 { + WhoCharRoundTrip(c.who[0]); + assert S.RenderClause(c)[0] == S.WhoChar(c.who[0]); + } else { + OpCharRoundTrip(c.actions[0].op); + assert S.RenderClause(c)[0] == S.OpChar(c.actions[0].op); + } + assert S.RenderClauses(cs)[0] == S.RenderClause(c)[0]; + } + + lemma ParseModeOfRender(e: S.ModeExpr) + requires S.WellFormed(e) + ensures P.ParseMode(S.Render(e)) == P.Some(e) + { + match e + case Absolute(ds) => + DigitCharRoundTrip(ds[0]); + TakeDigitsOfRender(ds, ""); + assert S.Render(e) == S.RenderDigits(ds) + ""; + case Symbolic(cs) => + SymbolicStartsWithoutDigit(cs); + ParseClausesOfRender(cs); + } + + // --------------------------------------------------------------------------- + // Soundness: what the parser returns renders back to its input + // --------------------------------------------------------------------------- + + lemma TakeWhoRenders(s: string) + ensures S.RenderWho(P.TakeWho(s).0) + P.TakeWho(s).1 == s + decreases |s| + { + if |s| > 0 && P.IsWhoChar(s[0]) { + WhoOfRoundTrip(s[0]); + TakeWhoRenders(s[1..]); + assert s == [s[0]] + s[1..]; + } + } + + lemma TakePermsRenders(s: string) + ensures S.RenderPerms(P.TakePerms(s).0) + P.TakePerms(s).1 == s + decreases |s| + { + if |s| > 0 && P.IsPermChar(s[0]) { + PermOfRoundTrip(s[0]); + TakePermsRenders(s[1..]); + assert s == [s[0]] + s[1..]; + } + } + + lemma TakeDigitsRenders(s: string) + ensures S.RenderDigits(P.TakeDigits(s).0) + P.TakeDigits(s).1 == s + decreases |s| + { + if |s| > 0 && P.IsOctalChar(s[0]) { + DigitOfRoundTrip(s[0]); + TakeDigitsRenders(s[1..]); + assert s == [s[0]] + s[1..]; + } + } + + lemma TakeRhsRenders(s: string) + ensures S.RenderRhs(P.TakeRhs(s).0) + P.TakeRhs(s).1 == s + { + if |s| > 0 && P.IsCopyChar(s[0]) { + SrcOfRoundTrip(s[0]); + assert s == [s[0]] + s[1..]; + } else if |s| > 0 && P.IsOctalChar(s[0]) { + TakeDigitsRenders(s); + } else { + TakePermsRenders(s); + } + } + + lemma RenderActionsCons(a: S.Action, more: seq) + ensures S.RenderActions([a] + more) == [S.OpChar(a.op)] + S.RenderRhs(a.rhs) + S.RenderActions(more) + { + assert ([a] + more)[0] == a && ([a] + more)[1..] == more; + } + + lemma {:isolate_assertions} TakeActionsRenders(s: string) + requires |s| > 0 && P.IsOpChar(s[0]) + ensures S.RenderActions(P.TakeActions(s).0) + P.TakeActions(s).1 == s + decreases |s| + { + var rhs := P.TakeRhs(s[1..]); + var a := S.Action(P.OpOf(s[0]), rhs.0); + TakeRhsRenders(s[1..]); + OpOfRoundTrip(s[0]); + assert S.RenderRhs(rhs.0) + rhs.1 == s[1..]; + assert s == [s[0]] + s[1..]; + if |rhs.1| > 0 && P.IsOpChar(rhs.1[0]) { + var more := P.TakeActions(rhs.1); + assert P.TakeActions(s) == ([a] + more.0, more.1); + TakeActionsRenders(rhs.1); + RenderActionsCons(a, more.0); + calc { + S.RenderActions([a] + more.0) + more.1; + [S.OpChar(a.op)] + S.RenderRhs(a.rhs) + S.RenderActions(more.0) + more.1; + [s[0]] + (S.RenderRhs(rhs.0) + (S.RenderActions(more.0) + more.1)); + [s[0]] + (S.RenderRhs(rhs.0) + rhs.1); + s; + } + } else { + assert P.TakeActions(s) == ([a], rhs.1); + RenderActionsCons(a, []); + assert S.RenderActions([]) == []; + calc { + S.RenderActions([a]) + rhs.1; + { assert [a] + [] == [a]; } + [S.OpChar(a.op)] + S.RenderRhs(a.rhs) + S.RenderActions([]) + rhs.1; + [s[0]] + (S.RenderRhs(rhs.0) + rhs.1); + s; + } + } + } + + lemma TakeClauseRenders(s: string) + ensures P.TakeClause(s).Some? ==> + S.RenderClause(P.TakeClause(s).value.0) + P.TakeClause(s).value.1 == s + { + var w := P.TakeWho(s); + TakeWhoRenders(s); + if |w.1| > 0 && P.IsOpChar(w.1[0]) { + TakeActionsRenders(w.1); + } + } + + lemma ParseClausesRenders(s: string) + ensures P.ParseClauses(s).Some? ==> S.RenderClauses(P.ParseClauses(s).value) == s + decreases |s| + { + TakeClauseRenders(s); + match P.TakeClause(s) + case None => + case Some(cr) => + var (c, rest) := cr; + if |rest| > 0 && rest[0] == ',' { + ParseClausesRenders(rest[1..]); + if P.ParseClauses(rest[1..]).Some? { + var cs := P.ParseClauses(rest[1..]).value; + assert P.ParseClauses(s).value == [c] + cs; + assert ([c] + cs)[1..] == cs; + assert rest == "," + rest[1..]; + } + } else if |rest| == 0 { + assert S.RenderClause(c) + rest == S.RenderClause(c); + } + } + + lemma ParseModeRenders(s: string) + ensures P.ParseMode(s).Some? ==> S.Render(P.ParseMode(s).value) == s + { + if |s| > 0 && P.IsOctalChar(s[0]) { + TakeDigitsRenders(s); + } else { + ParseClausesRenders(s); + } + } + + // --------------------------------------------------------------------------- + // What the rest of the proof uses + // --------------------------------------------------------------------------- + + lemma ParseNoneIsInvalid(s: string) + requires P.ParseMode(s) == P.None + ensures S.ModeInvalid(s) + { + forall e | S.WellFormed(e) + ensures S.Render(e) != s + { + ParseModeOfRender(e); + } + } + + lemma ParseSomeDenotes(s: string, umask: bv32) + requires P.ParseMode(s).Some? + ensures S.ModeDenotes(s, umask, S.Meaning(P.ParseMode(s).value, umask)) + { + ParseModeRenders(s); + } + + // A valid MODE has exactly one meaning. + lemma MeaningUnique(s: string, umask: bv32, m1: bv32, m2: bv32) + requires S.ModeDenotes(s, umask, m1) && S.ModeDenotes(s, umask, m2) + ensures m1 == m2 + { + var e1 :| S.WellFormed(e1) && S.Render(e1) == s && m1 == S.Meaning(e1, umask); + var e2 :| S.WellFormed(e2) && S.Render(e2) == s && m2 == S.Meaning(e2, umask); + ParseModeOfRender(e1); + ParseModeOfRender(e2); + } +} diff --git a/bench/utils/mkfifo/MkfifoProof.dfy b/bench/utils/mkfifo/MkfifoProof.dfy new file mode 100644 index 0000000..268c340 --- /dev/null +++ b/bench/utils/mkfifo/MkfifoProof.dfy @@ -0,0 +1,347 @@ +include "MkfifoSpec.dfy" +include "MkfifoModeCore.dfy" +include "MkfifoModeProof.dfy" + +module MkfifoProof { + import BenchIO + import BW = BenchWorld + import C = IOContract + import Spec = MkfifoSpec + import Schema = MkfifoSchema + import P = MkfifoModeCore + import MP = MkfifoModeProof + + // --------------------------------------------------------------------------- + // MODE decision + // --------------------------------------------------------------------------- + + // The decision RunCore computes from the parser result. + ghost predicate ComputedPlan(raw: Schema.MkfifoCmdRaw, umask: bv32, plan: Spec.ModePlan) + { + match raw.mode + case None => plan == Spec.NoModeOption + case Some(s) => + match P.ParseMode(s) + case None => plan == Spec.RejectInvalidMode + case Some(e) => + var bits := Spec.Meaning(e, umask); + plan == (if Spec.OnlyPermissionBits(bits) then Spec.ExplicitMode(bits) else Spec.RejectSpecialBits) + } + + lemma ComputedPlanIsSpecPlan(raw: Schema.MkfifoCmdRaw, umask: bv32, plan: Spec.ModePlan) + requires ComputedPlan(raw, umask, plan) + ensures Spec.ModePlanOf(raw, umask, plan) + { + match raw.mode + case None => + case Some(s) => + match P.ParseMode(s) + case None => + MP.ParseNoneIsInvalid(s); + case Some(e) => + MP.ParseSomeDenotes(s, umask); + var bits := Spec.Meaning(e, umask); + assert Spec.ModeDenotes(s, umask, bits); + } + + // --------------------------------------------------------------------------- + // One operand + // --------------------------------------------------------------------------- + + // Folded copies of the native contracts. Passing them to lemmas keeps each + // call-site check a single fact instead of every conjunct of the contract. + opaque ghost predicate CreateFact( + before: BW.FileSystem, now: int, fsObservations: C.ValidFilesystemObservations, umask: bv32, + after: BW.FileSystem, path: string, mode: bv32, ok: bool, err: int) + { + C.CreateSpecialNodeSpec(before, now, fsObservations, umask, after, path, BW.FifoNode, + mode, 0, 0, ok, err) + } + + opaque ghost predicate PermissionFact( + before: BW.FileSystem, now: int, failures: C.ValidNativeFailureObservations, + after: BW.FileSystem, path: string, mode: bv32, ok: bool, err: int) + { + C.SetFileModeSpec(before, now, failures, after, path, false, mode, ok, err) + } + + // Creation alone: it failed, or no -m was given. + lemma StepCreateOnly( + before: BW.FileSystem, after: BW.FileSystem, path: string, plan: Spec.ModePlan, + now: int, umask: bv32, + fsObservations: C.ValidFilesystemObservations, + failures: C.ValidNativeFailureObservations, + ok: bool, err: int, outcome: Spec.OperandOutcome) + requires plan.NoModeOption? || plan.ExplicitMode? + requires CreateFact(before, now, fsObservations, umask, after, path, + if plan.ExplicitMode? then plan.bits else Spec.MKFIFO_BASE_MODE, ok, err) + requires !ok || plan.NoModeOption? + requires outcome == (if ok then Spec.Created else Spec.CreateFailed(err)) + ensures Spec.OperandStep(before, after, path, plan, now, umask, fsObservations, failures, outcome) + { + reveal CreateFact(); + var created := after; + if !ok { + assert after == created && outcome == Spec.CreateFailed(err); + } else { + assert plan.NoModeOption? && after == created && outcome == Spec.Created; + } + } + + // Creation succeeded and -m was given: one non-following permission change. + lemma StepCreateThenPermission( + before: BW.FileSystem, created: BW.FileSystem, after: BW.FileSystem, path: string, + plan: Spec.ModePlan, now: int, umask: bv32, + fsObservations: C.ValidFilesystemObservations, + failures: C.ValidNativeFailureObservations, + err: int, permOk: bool, permErr: int, outcome: Spec.OperandOutcome) + requires plan.ExplicitMode? + requires CreateFact(before, now, fsObservations, umask, created, path, plan.bits, true, err) + requires PermissionFact(created, now, failures, after, path, plan.bits, permOk, permErr) + requires outcome == (if permOk then Spec.Created else Spec.PermissionFailed(permErr)) + ensures Spec.OperandStep(before, after, path, plan, now, umask, fsObservations, failures, outcome) + { + reveal CreateFact(); + reveal PermissionFact(); + assert outcome == (if permOk then Spec.Created else Spec.PermissionFailed(permErr)); + } + + // --------------------------------------------------------------------------- + // The operand loop + // --------------------------------------------------------------------------- + + lemma ExtendOperands( + paths: seq, plan: Spec.ModePlan, states: seq, + outcomes: seq, now: int, umask: bv32, + fsObservations: C.ValidFilesystemObservations, + failures: C.ValidNativeFailureObservations, + path: string, after: BW.FileSystem, outcome: Spec.OperandOutcome) + requires plan.NoModeOption? || plan.ExplicitMode? + requires Spec.OperandResults(paths, plan, states, outcomes, now, umask, fsObservations, failures) + requires Spec.OperandStep(states[|paths|], after, path, plan, now, umask, + fsObservations, failures, outcome) + ensures Spec.OperandResults(paths + [path], plan, states + [after], outcomes + [outcome], + now, umask, fsObservations, failures) + { + hide Spec.OperandStep(); + forall j | 0 <= j < |paths| + 1 + ensures Spec.OperandStep((states + [after])[j], (states + [after])[j + 1], (paths + [path])[j], + plan, now, umask, fsObservations, failures, (outcomes + [outcome])[j]) + { + if j < |paths| { + assert Spec.OperandStep(states[j], states[j + 1], paths[j], plan, now, umask, + fsObservations, failures, outcomes[j]); + } + } + } + + lemma {:isolate_assertions} ExtendDiagnostics( + paths: seq, outcomes: seq, diagnostics: BW.Bytes, cuts: seq, + path: string, outcome: Spec.OperandOutcome, piece: BW.Bytes) + requires Spec.OrderedDiagnostics(paths, outcomes, diagnostics, cuts) + requires piece == Spec.OutcomeDiagnostic(path, outcome) + ensures Spec.OrderedDiagnostics(paths + [path], outcomes + [outcome], diagnostics + piece, + cuts + [|diagnostics| + |piece|]) + { + hide Spec.OutcomeDiagnostic(); + var next := diagnostics + piece; + var nextCuts := cuts + [|next|]; + forall j {:trigger nextCuts[j]} | 0 <= j < |paths| + 1 + ensures nextCuts[j] <= nextCuts[j + 1] <= |next| + ensures next[nextCuts[j]..nextCuts[j + 1]] == + Spec.OutcomeDiagnostic((paths + [path])[j], (outcomes + [outcome])[j]) + { + if j < |paths| { + assert cuts[j] <= cuts[j + 1] <= |diagnostics|; + assert diagnostics[cuts[j]..cuts[j + 1]] == Spec.OutcomeDiagnostic(paths[j], outcomes[j]); + assert nextCuts[j] == cuts[j] && nextCuts[j + 1] == cuts[j + 1]; + assert next[..|diagnostics|] == diagnostics; + assert next[nextCuts[j]..nextCuts[j + 1]] == diagnostics[cuts[j]..cuts[j + 1]]; + } else { + assert nextCuts[j] == |diagnostics| && nextCuts[j + 1] == |next|; + assert next[nextCuts[j]..nextCuts[j + 1]] == piece; + } + } + } + + lemma AllCreatedSnoc(outcomes: seq, outcome: Spec.OperandOutcome) + ensures (forall j | 0 <= j < |outcomes + [outcome]| :: (outcomes + [outcome])[j].Created?) <==> + ((forall j | 0 <= j < |outcomes| :: outcomes[j].Created?) && outcome.Created?) + { + if forall j | 0 <= j < |outcomes + [outcome]| :: (outcomes + [outcome])[j].Created? { + assert (outcomes + [outcome])[|outcomes|] == outcome; + forall j | 0 <= j < |outcomes| + ensures outcomes[j].Created? + { + assert (outcomes + [outcome])[j] == outcomes[j]; + } + } + if (forall j | 0 <= j < |outcomes| :: outcomes[j].Created?) && outcome.Created? { + forall j | 0 <= j < |outcomes + [outcome]| + ensures (outcomes + [outcome])[j].Created? + { + if j < |outcomes| { + assert (outcomes + [outcome])[j] == outcomes[j]; + } + } + } + } + + lemma EmptyOperands( + plan: Spec.ModePlan, start: BW.FileSystem, now: int, umask: bv32, + fsObservations: C.ValidFilesystemObservations, + failures: C.ValidNativeFailureObservations) + requires plan.NoModeOption? || plan.ExplicitMode? + ensures Spec.OperandResults([], plan, [start], [], now, umask, fsObservations, failures) + ensures Spec.OrderedDiagnostics([], [], [], [0]) + {} + + // A rejected MODE leaves the filesystem alone and reports one line. + lemma RejectRun( + paths: seq, plan: Spec.ModePlan, fs: BW.FileSystem, now: int, umask: bv32, + fsObservations: C.ValidFilesystemObservations, + failures: C.ValidNativeFailureObservations, + diagnostics: BW.Bytes, runExit: int) + requires plan.RejectInvalidMode? || plan.RejectSpecialBits? + requires diagnostics == (if plan.RejectInvalidMode? then Spec.InvalidModeText() else Spec.SpecialBitsText()) + requires runExit == 1 + ensures Spec.PlanRun(paths, plan, fs, fs, now, umask, fsObservations, failures, diagnostics, runExit) + {} + + // The loop invariant of RunOperands after i operands. + ghost predicate LoopState( + paths: seq, i: nat, plan: Spec.ModePlan, start: BW.FileSystem, current: BW.FileSystem, + now: int, umask: bv32, + fsObservations: C.ValidFilesystemObservations, + failures: C.ValidNativeFailureObservations, + states: seq, outcomes: seq, cuts: seq, + diagnostics: BW.Bytes, runExit: int) + requires plan.NoModeOption? || plan.ExplicitMode? + { + i <= |paths| && + |states| == i + 1 && states[0] == start && states[i] == current && |outcomes| == i && + Spec.OperandResults(paths[..i], plan, states, outcomes, now, umask, fsObservations, failures) && + Spec.OrderedDiagnostics(paths[..i], outcomes, diagnostics, cuts) && + runExit == (if forall j | 0 <= j < i :: outcomes[j].Created? then 0 else 1) + } + + lemma EmptyLoop( + paths: seq, plan: Spec.ModePlan, start: BW.FileSystem, now: int, umask: bv32, + fsObservations: C.ValidFilesystemObservations, + failures: C.ValidNativeFailureObservations) + requires plan.NoModeOption? || plan.ExplicitMode? + ensures LoopState(paths, 0, plan, start, start, now, umask, fsObservations, failures, + [start], [], [0], [], 0) + { + EmptyOperands(plan, start, now, umask, fsObservations, failures); + assert paths[..0] == []; + } + + lemma ExtendLoop( + paths: seq, i: nat, plan: Spec.ModePlan, start: BW.FileSystem, + before: BW.FileSystem, after: BW.FileSystem, now: int, umask: bv32, + fsObservations: C.ValidFilesystemObservations, + failures: C.ValidNativeFailureObservations, + states: seq, outcomes: seq, cuts: seq, + diagnostics: BW.Bytes, runExit: int, outcome: Spec.OperandOutcome, piece: BW.Bytes) + requires plan.NoModeOption? || plan.ExplicitMode? + requires i < |paths| + requires LoopState(paths, i, plan, start, before, now, umask, fsObservations, failures, + states, outcomes, cuts, diagnostics, runExit) + requires Spec.OperandStep(before, after, paths[i], plan, now, umask, fsObservations, failures, outcome) + requires piece == Spec.OutcomeDiagnostic(paths[i], outcome) + ensures LoopState(paths, i + 1, plan, start, after, now, umask, fsObservations, failures, + states + [after], outcomes + [outcome], cuts + [|diagnostics| + |piece|], + diagnostics + piece, if outcome.Created? then runExit else 1) + { + hide Spec.OperandResults(); + hide Spec.OrderedDiagnostics(); + hide Spec.OperandStep(); + hide Spec.OutcomeDiagnostic(); + assert paths[..i + 1] == paths[..i] + [paths[i]]; + ExtendOperands(paths[..i], plan, states, outcomes, now, umask, fsObservations, failures, + paths[i], after, outcome); + ExtendDiagnostics(paths[..i], outcomes, diagnostics, cuts, paths[i], outcome, piece); + AllCreatedSnoc(outcomes, outcome); + } + + lemma FinishLoop( + paths: seq, plan: Spec.ModePlan, start: BW.FileSystem, current: BW.FileSystem, + now: int, umask: bv32, + fsObservations: C.ValidFilesystemObservations, + failures: C.ValidNativeFailureObservations, + states: seq, outcomes: seq, cuts: seq, + diagnostics: BW.Bytes, runExit: int) + requires plan.NoModeOption? || plan.ExplicitMode? + requires LoopState(paths, |paths|, plan, start, current, now, umask, fsObservations, failures, + states, outcomes, cuts, diagnostics, runExit) + ensures Spec.PlanRun(paths, plan, start, current, now, umask, fsObservations, failures, + diagnostics, runExit) + { + assert paths[..|paths|] == paths; + AssembleOperands(paths, plan, start, current, now, umask, fsObservations, failures, + diagnostics, runExit, states, outcomes, cuts); + } + + // --------------------------------------------------------------------------- + // Assembling the run + // --------------------------------------------------------------------------- + + lemma AssembleOperands( + paths: seq, plan: Spec.ModePlan, before: BW.FileSystem, after: BW.FileSystem, + now: int, umask: bv32, + fsObservations: C.ValidFilesystemObservations, + failures: C.ValidNativeFailureObservations, + diagnostics: BW.Bytes, runExit: int, + states: seq, outcomes: seq, cuts: seq) + requires plan.NoModeOption? || plan.ExplicitMode? + requires Spec.OperandResults(paths, plan, states, outcomes, now, umask, fsObservations, failures) + requires states[0] == before && states[|paths|] == after + requires Spec.OrderedDiagnostics(paths, outcomes, diagnostics, cuts) + requires runExit == (if forall i | 0 <= i < |paths| :: outcomes[i].Created? then 0 else 1) + ensures Spec.PlanRun(paths, plan, before, after, now, umask, fsObservations, failures, + diagnostics, runExit) + { + assert |states| == |paths| + 1; + hide Spec.OperandResults(); + hide Spec.OrderedDiagnostics(); + } + + lemma AssembleRun( + raw: Schema.MkfifoCmdRaw, plan: Spec.ModePlan, + before: BW.FileSystem, after: BW.FileSystem, now: int, createUmask: bv32, modeUmask: bv32, + fsObservations: C.ValidFilesystemObservations, + failures: C.ValidNativeFailureObservations, + diagnostics: BW.Bytes, runExit: int) + requires Spec.ModePlanOf(raw, modeUmask, plan) + requires Spec.PlanRun(Schema.Operands(raw), plan, before, after, now, createUmask, + fsObservations, failures, diagnostics, runExit) + ensures Spec.RunRelation(raw, before, after, now, createUmask, modeUmask, + fsObservations, failures, diagnostics, runExit) + { + hide Spec.ModePlanOf(); + hide Spec.PlanRun(); + } + + twostate lemma Complete( + raw: Schema.MkfifoCmdRaw, io: BenchIO.IO, diagnostics: BW.Bytes, runExit: int, exit: int) + requires Spec.RunRelation(raw, old(io.fs()), io.fs(), io.now(), io.umask(), + C.GetUmaskResultFields(io.props()), + io.trustedFilesystem(), io.trustedNativeFailures(), + diagnostics, runExit) + requires Spec.StderrResult(old(io.stderr()), io.stderr(), io.trustedStreams(), + diagnostics, runExit, exit) + ensures Spec.Spec(raw, io, exit) + { + hide Spec.RunRelation(); + hide Spec.StderrResult(); + assert exists chosenDiagnostics: BW.Bytes, chosenExit: int :: + chosenDiagnostics == diagnostics && chosenExit == runExit && + Spec.RunRelation(raw, old(io.fs()), io.fs(), io.now(), io.umask(), + C.GetUmaskResultFields(io.props()), + io.trustedFilesystem(), io.trustedNativeFailures(), + chosenDiagnostics, chosenExit) && + Spec.StderrResult(old(io.stderr()), io.stderr(), io.trustedStreams(), + chosenDiagnostics, chosenExit, exit); + } +} diff --git a/bench/utils/mkfifo/MkfifoSchema.dfy b/bench/utils/mkfifo/MkfifoSchema.dfy new file mode 100644 index 0000000..75aa282 --- /dev/null +++ b/bench/utils/mkfifo/MkfifoSchema.dfy @@ -0,0 +1,62 @@ +include "../../core/CliTypes.dfy" + +module MkfifoSchema { + import CliTypes + + // `mode` holds the value of the last -m/--mode occurrence (GNU keeps the last + // one), or None when no -m is given. -Z/--context are not declared: they are + // outside this contribution's accepted command domain (see mkfifo.md). + datatype MkfifoCmdRaw = MkfifoCmdRaw(mode: CliTypes.OptionalString, first: string, rest: seq) + + function Operands(raw: MkfifoCmdRaw): seq { + [raw.first] + raw.rest + } + + method Schema() returns (schema: CliTypes.CliSchema) { + schema := CliTypes.CliSchema([ + CliTypes.OptionDecl("mkfifo.mode", ['m'], ["mode"], CliTypes.ReqArg), + CliTypes.OptionDecl("mkfifo.help", [], ["help"], CliTypes.NoArg), + CliTypes.OptionDecl("mkfifo.version", [], ["version"], CliTypes.NoArg) + ], true); + } + + method ParserConfig() returns (cfg: CliTypes.ParseConfig) { + cfg := CliTypes.ParseConfig(CliTypes.GNU_Permute, true, true, true); + } + + method InformationRequest(parsed: CliTypes.ParsedArgs) + returns (request: CliTypes.PriorRequest) + { + request := CliTypes.RequestNone; + var firstIndex := -1; + var i := 0; + while i < |parsed.options| + decreases |parsed.options| - i + { + var option := parsed.options[i]; + if (option.key == "mkfifo.help" || option.key == "mkfifo.version") && + (firstIndex < 0 || option.tokenIndex < firstIndex) { + firstIndex := option.tokenIndex; + request := if option.key == "mkfifo.help" then CliTypes.RequestHelp + else CliTypes.RequestVersion; + } + i := i + 1; + } + } + + method Decode(parsed: CliTypes.ParsedArgs) returns (raw: MkfifoCmdRaw) { + var mode := CliTypes.None; + var i := 0; + while i < |parsed.options| + decreases |parsed.options| - i + { + if parsed.options[i].key == "mkfifo.mode" { + mode := parsed.options[i].value; + } + i := i + 1; + } + raw := MkfifoCmdRaw(mode, + if |parsed.positionals| == 0 then "" else parsed.positionals[0], + if |parsed.positionals| == 0 then [] else parsed.positionals[1..]); + } +} diff --git a/bench/utils/mkfifo/MkfifoSpec.dfy b/bench/utils/mkfifo/MkfifoSpec.dfy new file mode 100644 index 0000000..7472000 --- /dev/null +++ b/bench/utils/mkfifo/MkfifoSpec.dfy @@ -0,0 +1,643 @@ +include "MkfifoSchema.dfy" +include "../../core/IO.dfy" +include "../../core/Utf8.dfy" +include "CliSupport.dfy" + +// Observable behavior of GNU mkfifo (coreutils src/mkfifo.c at +// 2cf491412c199e2211880ec3f4ba387026638a33). MODE follows gnulib +// lib/modechange.c (mode_compile, mode_adjust) at +// 83730551b451b43577531986a5c4300e0166c42f, as mkfifo uses it: +// mode_adjust (0666, false, umask, changes). +// +// A MODE string is valid iff some well-formed expression renders to it; its +// result is that expression's Meaning. No parsing algorithm appears here. +module MkfifoSpec { + import BenchIO + import BenchWorld + import CliTypes + import Schema = MkfifoSchema + import Utf8 = Utf8Semantics + import CliModel + import C = IOContract + + // =========================================================================== + // MODE: abstract syntax, Render, Meaning + // =========================================================================== + + + // --------------------------------------------------------------------------- + // Abstract syntax + // --------------------------------------------------------------------------- + + datatype Who = WhoU | WhoG | WhoO | WhoA + datatype OpSym = OpAdd | OpRemove | OpSet + datatype Perm = PermR | PermW | PermX | PermCondX | PermS | PermT + datatype CopySrc = FromU | FromG | FromO + + type OctDigit = d: nat | d < 8 + + // The right-hand side of one operator. + datatype Rhs = + | Perms(perms: seq) // [rwxXst]*, possibly empty + | Copy(src: CopySrc) // u | g | o: copy that class's current bits + | Octal(digits: seq) // [0-7]+ after an operator + + datatype Action = Action(op: OpSym, rhs: Rhs) + + // [ugoa]* followed by one or more actions. + datatype Clause = Clause(who: seq, actions: seq) + + datatype ModeExpr = + | Absolute(digits: seq) // the whole string is an octal number + | Symbolic(clauses: seq) // clauses separated by ',' + + // --------------------------------------------------------------------------- + // Well-formedness + // --------------------------------------------------------------------------- + + const ALLM: nat := 4095 // 07777 + + function OctalValue(ds: seq): nat + decreases |ds| + { + if |ds| == 0 then 0 else OctalValue(ds[..|ds| - 1]) * 8 + ds[|ds| - 1] + } + + // An octal right-hand side needs an empty who list, a value of at most 07777, + // and must end its clause (GNU requires ',' or the end right after the digits). + predicate ActionWellFormed(who: seq, a: Action, isLast: bool) + { + match a.rhs + case Octal(ds) => |ds| > 0 && OctalValue(ds) <= ALLM && |who| == 0 && isLast + case _ => true + } + + predicate ClauseWellFormed(c: Clause) + { + |c.actions| > 0 && + forall i :: 0 <= i < |c.actions| ==> + ActionWellFormed(c.who, c.actions[i], i == |c.actions| - 1) + } + + predicate WellFormed(e: ModeExpr) + { + match e + case Absolute(ds) => |ds| > 0 && OctalValue(ds) <= ALLM + case Symbolic(cs) => |cs| > 0 && forall c :: c in cs ==> ClauseWellFormed(c) + } + + // --------------------------------------------------------------------------- + // Concrete syntax: Render + // --------------------------------------------------------------------------- + + function WhoChar(w: Who): char + { + match w + case WhoU => 'u' + case WhoG => 'g' + case WhoO => 'o' + case WhoA => 'a' + } + + function OpChar(o: OpSym): char + { + match o + case OpAdd => '+' + case OpRemove => '-' + case OpSet => '=' + } + + function PermChar(p: Perm): char + { + match p + case PermR => 'r' + case PermW => 'w' + case PermX => 'x' + case PermCondX => 'X' + case PermS => 's' + case PermT => 't' + } + + function SrcChar(s: CopySrc): char + { + match s + case FromU => 'u' + case FromG => 'g' + case FromO => 'o' + } + + function DigitChar(d: OctDigit): char + { + ('0' as int + d) as char + } + + function RenderWho(ws: seq): string + decreases |ws| + { + if |ws| == 0 then "" else [WhoChar(ws[0])] + RenderWho(ws[1..]) + } + + function RenderPerms(ps: seq): string + decreases |ps| + { + if |ps| == 0 then "" else [PermChar(ps[0])] + RenderPerms(ps[1..]) + } + + function RenderDigits(ds: seq): string + decreases |ds| + { + if |ds| == 0 then "" else [DigitChar(ds[0])] + RenderDigits(ds[1..]) + } + + function RenderRhs(r: Rhs): string + { + match r + case Perms(ps) => RenderPerms(ps) + case Copy(src) => [SrcChar(src)] + case Octal(ds) => RenderDigits(ds) + } + + function RenderActions(as_: seq): string + decreases |as_| + { + if |as_| == 0 then "" + else [OpChar(as_[0].op)] + RenderRhs(as_[0].rhs) + RenderActions(as_[1..]) + } + + function RenderClause(c: Clause): string + { + RenderWho(c.who) + RenderActions(c.actions) + } + + function RenderClauses(cs: seq): string + decreases |cs| + { + if |cs| == 0 then "" + else if |cs| == 1 then RenderClause(cs[0]) + else RenderClause(cs[0]) + "," + RenderClauses(cs[1..]) + } + + function Render(e: ModeExpr): string + { + match e + case Absolute(ds) => RenderDigits(ds) + case Symbolic(cs) => RenderClauses(cs) + } + + // --------------------------------------------------------------------------- + // Meaning + // --------------------------------------------------------------------------- + + const S_ISUID: bv32 := 0x800 + const S_ISGID: bv32 := 0x400 + const S_ISVTX: bv32 := 0x200 + const S_IRWXU: bv32 := 0x1C0 + const S_IRWXG: bv32 := 0x038 + const S_IRWXO: bv32 := 0x007 + const READ_BITS: bv32 := 0x124 // 0444 + const WRITE_BITS: bv32 := 0x092 // 0222 + const EXEC_BITS: bv32 := 0x049 // 0111 + const PERMISSION_BITS: bv32 := 0x1FF // 0777 + const MODE_BITS: bv32 := 0xFFF // 07777 + const MKFIFO_BASE_MODE: bv32 := 0x1B6 // 0666 = a=rw + + function WhoMask(w: Who): bv32 + { + match w + case WhoU => S_ISUID | S_IRWXU + case WhoG => S_ISGID | S_IRWXG + case WhoO => S_ISVTX | S_IRWXO + case WhoA => MODE_BITS + } + + // Bits selected by the who list; 0 means "no who given". + function WhoBits(ws: seq): bv32 + decreases |ws| + { + if |ws| == 0 then 0 else WhoMask(ws[0]) | WhoBits(ws[1..]) + } + + function PermBits(p: Perm): bv32 + { + match p + case PermR => READ_BITS + case PermW => WRITE_BITS + case PermX => EXEC_BITS + case PermCondX => 0 + case PermS => S_ISUID | S_ISGID + case PermT => S_ISVTX + } + + function PermsBits(ps: seq): bv32 + decreases |ps| + { + if |ps| == 0 then 0 else PermBits(ps[0]) | PermsBits(ps[1..]) + } + + function SrcBits(s: CopySrc): bv32 + { + match s + case FromU => S_IRWXU + case FromG => S_IRWXG + case FromO => S_IRWXO + } + + // Copy: take the source class's current bits and repeat each kind (r, w, x) + // in all three classes. + function CopyBits(s: CopySrc, cur: bv32): bv32 + { + var v := SrcBits(s) & cur; + v + | (if v & READ_BITS != 0 then READ_BITS else 0) + | (if v & WRITE_BITS != 0 then WRITE_BITS else 0) + | (if v & EXEC_BITS != 0 then EXEC_BITS else 0) + } + + // The bits an action proposes before the who/umask mask. 'X' adds execute bits + // only if some execute bit is already set (a FIFO is never a directory). + function RhsBits(r: Rhs, cur: bv32): bv32 + requires r.Octal? ==> OctalValue(r.digits) <= ALLM + { + match r + case Perms(ps) => + PermsBits(ps) | (if PermCondX in ps && cur & EXEC_BITS != 0 then EXEC_BITS else 0) + case Copy(src) => CopyBits(src, cur) + case Octal(ds) => OctalValue(ds) as bv32 + } + + // An octal right-hand side affects every mode bit, as if "a" were given. + function ActionScope(who: seq, a: Action): bv32 + { + if a.rhs.Octal? then MODE_BITS else WhoBits(who) + } + + // Without a who list the umask restricts the change; with one, the who bits do. + function ApplyAction(cur: bv32, umask: bv32, who: seq, a: Action): bv32 + requires a.rhs.Octal? ==> OctalValue(a.rhs.digits) <= ALLM + { + var scope := ActionScope(who, a); + var v := RhsBits(a.rhs, cur) & (if scope != 0 then scope else !umask); + match a.op + case OpSet => (cur & (if scope != 0 then !scope else 0)) | v + case OpAdd => cur | v + case OpRemove => cur & !v + } + + predicate ActionsBounded(as_: seq) + { + forall i :: 0 <= i < |as_| ==> + as_[i].rhs.Octal? ==> OctalValue(as_[i].rhs.digits) <= ALLM + } + + function ApplyActions(cur: bv32, umask: bv32, who: seq, as_: seq): bv32 + requires ActionsBounded(as_) + decreases |as_| + { + if |as_| == 0 then cur + else ApplyActions(ApplyAction(cur, umask, who, as_[0]), umask, who, as_[1..]) + } + + lemma ClauseActionsBounded(c: Clause) + requires ClauseWellFormed(c) + ensures ActionsBounded(c.actions) + { + forall i | 0 <= i < |c.actions| && c.actions[i].rhs.Octal? + ensures OctalValue(c.actions[i].rhs.digits) <= ALLM + { + assert ActionWellFormed(c.who, c.actions[i], i == |c.actions| - 1); + } + } + + function ApplyClauses(cur: bv32, umask: bv32, cs: seq): bv32 + requires forall c :: c in cs ==> ClauseWellFormed(c) + decreases |cs| + { + if |cs| == 0 then cur + else + ClauseActionsBounded(cs[0]); + ApplyClauses(ApplyActions(cur, umask, cs[0].who, cs[0].actions), umask, cs[1..]) + } + + // mkfifo starts from a=rw (0666). A numeric mode is used exactly; the umask + // only matters for symbolic actions without a who list. + function Meaning(e: ModeExpr, umask: bv32): bv32 + requires WellFormed(e) + { + match e + case Absolute(ds) => OctalValue(ds) as bv32 + case Symbolic(cs) => ApplyClauses(MKFIFO_BASE_MODE, umask, cs) + } + + // --------------------------------------------------------------------------- + // What the specification of mkfifo uses + // --------------------------------------------------------------------------- + + ghost predicate ModeDenotes(s: string, umask: bv32, mode: bv32) + { + exists e :: WellFormed(e) && Render(e) == s && mode == Meaning(e, umask) + } + + ghost predicate ModeInvalid(s: string) + { + forall e :: WellFormed(e) ==> Render(e) != s + } + + // GNU rejects a valid MODE whose result has set-ID or sticky bits: + // "mode must specify only file permission bits". + predicate OnlyPermissionBits(mode: bv32) + { + mode & !PERMISSION_BITS == 0 + } + + // =========================================================================== + // Commands + // =========================================================================== + + // --------------------------------------------------------------------------- + // Command-line parse errors (GNU getopt_long wording) + // --------------------------------------------------------------------------- + + // Long options that take no argument, by unique abbreviation. + function NoArgLongOptionName(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 TryHelpText(): BenchWorld.Bytes + { + "Try 'mkfifo --help' for more information.\n" + } + + function UnknownShortText(byte: BenchWorld.RawByte): BenchWorld.Bytes + { + "mkfifo: invalid option -- '" + [byte] + "'\n" + TryHelpText() + } + + function ParseErrorText(err: CliTypes.ParseError): BenchWorld.Bytes + { + var t := err.rawToken; + var isLong := |t| > 2 && t[0] == '-' && t[1] == '-'; + var isShort := |t| > 1 && t[0] == '-' && !isLong; + if err.kind == CliTypes.UnknownOption then + if isLong then + "mkfifo: unrecognized option '" + Utf8.Encode(t) + "'\n" + TryHelpText() + else if isShort then + UnknownShortText(Utf8.EncodeChar(t[1])[0]) + else + "mkfifo: invalid option\n" + TryHelpText() + else if err.kind == CliTypes.MissingValue then + if isLong then + "mkfifo: option '--mode' requires an argument\n" + TryHelpText() + else + "mkfifo: option requires an argument -- 'm'\n" + TryHelpText() + else if err.kind == CliTypes.UnexpectedValue then + "mkfifo: option '" + Utf8.Encode(NoArgLongOptionName(t)) + + "' doesn't allow an argument\n" + TryHelpText() + else + // The declared long options (mode, help, version) share no prefix, so an + // ambiguous abbreviation cannot occur. + "mkfifo: option '" + Utf8.Encode(t) + "' is ambiguous\n" + TryHelpText() + } + + // --------------------------------------------------------------------------- + // Fixed text + // --------------------------------------------------------------------------- + + // TODO: compare byte-for-byte with the pinned GNU binary (_build/coreutils/src/mkfifo --help). + function HelpTextSpec(): BenchWorld.Bytes + { + "Usage: mkfifo [OPTION]... NAME...\n" + + "Create named pipes (FIFOs) with the given NAMEs.\n" + + "\n" + + "Mandatory arguments to long options are mandatory for short options too.\n" + + " -m, --mode=MODE\n" + + " set file permission bits to MODE, not a=rw - umask\n" + + " -Z\n" + + " set the SELinux security context to default type\n" + + " --context[=CTX]\n" + + " like -Z, or if CTX is specified then set the\n" + + " SELinux or SMACK security context to CTX\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) mkfifo invocation'\n" + } + + // TODO: compare with the pinned GNU binary (_build/coreutils/src/mkfifo --version). + function VersionTextSpec(): BenchWorld.Bytes + { + "mkfifo (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 David MacKenzie.\n" + } + + function MissingOperandText(): BenchWorld.Bytes + { + "mkfifo: missing operand\nTry 'mkfifo --help' for more information.\n" + } + + function InvalidModeText(): BenchWorld.Bytes + { + "mkfifo: invalid mode\n" + } + + function SpecialBitsText(): BenchWorld.Bytes + { + "mkfifo: mode must specify only file permission bits\n" + } + + function CreateFailureText(quoted: BenchWorld.Bytes, reason: string): BenchWorld.Bytes + { + "mkfifo: cannot create fifo " + quoted + ": " + Utf8.Encode(reason) + "\n" + } + + function PermissionFailureText(quoted: BenchWorld.Bytes, reason: string): BenchWorld.Bytes + { + "mkfifo: cannot set permissions of " + quoted + ": " + Utf8.Encode(reason) + "\n" + } + + // GNU mkfifo quotes both diagnostics with quoteaf. + ghost function CreateFailure(path: string, err: int): BenchWorld.Bytes + { + CreateFailureText(C.QuoteafPathResult(path), C.CLocaleErrnoTextResult(err)) + } + + ghost function PermissionFailure(path: string, err: int): BenchWorld.Bytes + { + PermissionFailureText(C.QuoteafPathResult(path), C.CLocaleErrnoTextResult(err)) + } + + // --------------------------------------------------------------------------- + // MODE decision (made once, before any operand) + // --------------------------------------------------------------------------- + + datatype ModePlan = + | NoModeOption // no -m: create with 0666, no permission change + | ExplicitMode(bits: bv32) // valid MODE within 0777: create, then set bits + | RejectInvalidMode // "invalid mode" + | RejectSpecialBits // "mode must specify only file permission bits" + + ghost predicate ModePlanOf(raw: Schema.MkfifoCmdRaw, umask: bv32, plan: ModePlan) + { + match raw.mode + case None => plan == NoModeOption + case Some(s) => + (ModeInvalid(s) && plan == RejectInvalidMode) || + (exists bits :: ModeDenotes(s, umask, bits) && + plan == (if OnlyPermissionBits(bits) then ExplicitMode(bits) else RejectSpecialBits)) + } + + // --------------------------------------------------------------------------- + // One operand + // --------------------------------------------------------------------------- + + datatype OperandOutcome = + | Created + | CreateFailed(createErr: int) + | PermissionFailed(permErr: int) // the FIFO exists; its permission change failed + + // Without -m: exactly one creation with 0666. With -m: one creation with the + // MODE bits, then, only if it succeeded, one non-following permission change. + ghost predicate OperandStep( + before: BenchWorld.FileSystem, after: BenchWorld.FileSystem, path: string, plan: ModePlan, + now: int, umask: bv32, + fsObservations: C.ValidFilesystemObservations, + failures: C.ValidNativeFailureObservations, + outcome: OperandOutcome) + requires plan.NoModeOption? || plan.ExplicitMode? + { + var createMode := if plan.ExplicitMode? then plan.bits else MKFIFO_BASE_MODE; + exists created: BenchWorld.FileSystem, ok: bool, err: int :: + C.CreateSpecialNodeSpec(before, now, fsObservations, umask, created, + path, BenchWorld.FifoNode, createMode, 0, 0, ok, err) && + if !ok then + after == created && outcome == CreateFailed(err) + else if plan.NoModeOption? then + after == created && outcome == Created + else + exists permOk: bool, permErr: int :: + C.SetFileModeSpec(created, now, failures, after, path, false, plan.bits, permOk, permErr) && + outcome == (if permOk then Created else PermissionFailed(permErr)) + } + + ghost function OutcomeDiagnostic(path: string, outcome: OperandOutcome): BenchWorld.Bytes + { + match outcome + case Created => [] + case CreateFailed(err) => CreateFailure(path, err) + case PermissionFailed(err) => PermissionFailure(path, err) + } + + // --------------------------------------------------------------------------- + // All operands + // --------------------------------------------------------------------------- + + ghost predicate OperandResults( + paths: seq, plan: ModePlan, states: seq, outcomes: seq, + now: int, umask: bv32, + fsObservations: C.ValidFilesystemObservations, + failures: C.ValidNativeFailureObservations) + requires plan.NoModeOption? || plan.ExplicitMode? + { + |states| == |paths| + 1 && |outcomes| == |paths| && + (forall i | 0 <= i < |paths| :: + OperandStep(states[i], states[i + 1], paths[i], plan, now, umask, + fsObservations, failures, outcomes[i])) + } + + // Cuts partition stderr in operand order, including empty pieces. + ghost predicate OrderedDiagnostics( + paths: seq, outcomes: seq, diagnostics: BenchWorld.Bytes, cuts: seq) + { + |outcomes| == |paths| && |cuts| == |paths| + 1 && + cuts[0] == 0 && cuts[|paths|] == |diagnostics| && + (forall i {:trigger cuts[i]} | 0 <= i < |paths| :: + cuts[i] <= cuts[i + 1] <= |diagnostics| && + diagnostics[cuts[i]..cuts[i + 1]] == OutcomeDiagnostic(paths[i], outcomes[i])) + } + + // What a fixed MODE decision does to the filesystem and stderr. + ghost predicate PlanRun( + paths: seq, plan: ModePlan, + before: BenchWorld.FileSystem, after: BenchWorld.FileSystem, + now: int, umask: bv32, + fsObservations: C.ValidFilesystemObservations, + failures: C.ValidNativeFailureObservations, + diagnostics: BenchWorld.Bytes, runExit: int) + { + match plan + case RejectInvalidMode => + after == before && diagnostics == InvalidModeText() && runExit == 1 + case RejectSpecialBits => + after == before && diagnostics == SpecialBitsText() && runExit == 1 + case _ => + exists states: seq, outcomes: seq, cuts: seq :: + OperandResults(paths, plan, states, outcomes, now, umask, fsObservations, failures) && + states[0] == before && states[|paths|] == after && + OrderedDiagnostics(paths, outcomes, diagnostics, cuts) && + runExit == (if forall i | 0 <= i < |paths| :: outcomes[i].Created? then 0 else 1) + } + + // `createUmask` is the umask the native FIFO creation applies; `modeUmask` is + // the value GNU reads with umask() to evaluate a symbolic MODE. + ghost predicate RunRelation( + raw: Schema.MkfifoCmdRaw, + before: BenchWorld.FileSystem, after: BenchWorld.FileSystem, + now: int, createUmask: bv32, modeUmask: bv32, + fsObservations: C.ValidFilesystemObservations, + failures: C.ValidNativeFailureObservations, + diagnostics: BenchWorld.Bytes, runExit: int) + { + exists plan: ModePlan :: + ModePlanOf(raw, modeUmask, plan) && + PlanRun(Schema.Operands(raw), plan, before, after, now, createUmask, + fsObservations, failures, diagnostics, runExit) + } + + // --------------------------------------------------------------------------- + // Streams and the main specification + // --------------------------------------------------------------------------- + + // mkfifo writes nothing to stdout outside help/version. All diagnostics form + // one stderr write; a failed stderr write also makes the exit status 1. + ghost predicate StderrResult( + beforeErr: BenchWorld.Bytes, afterErr: BenchWorld.Bytes, + observations: (BenchWorld.TrustedStreamRequest) -> BenchWorld.TrustedStreamResult, + diagnostics: BenchWorld.Bytes, runExit: int, exit: int) + { + var errObservation := observations(BenchWorld.StreamWriteStderr(beforeErr, diagnostics)); + errObservation.StreamWriteResult? && + C.WriteStderrSpec(beforeErr, observations, afterErr, diagnostics, + errObservation.committed, errObservation.err) && + exit == (if runExit == 0 && errObservation.err == 0 then 0 else 1) + } + + twostate predicate Spec(raw: Schema.MkfifoCmdRaw, io: BenchIO.IO, exit: int) + reads io.fsRegion, io.stderrRegion, + io.nowRegion, io.umaskRegion, io.propsRegion, + io.trustedFilesystemRegion, io.trustedNativeFailuresRegion, io.trustedStreamsRegion + { + exists diagnostics: BenchWorld.Bytes, runExit: int :: + RunRelation(raw, old(io.fs()), io.fs(), io.now(), io.umask(), C.GetUmaskResultFields(io.props()), + io.trustedFilesystem(), io.trustedNativeFailures(), diagnostics, runExit) && + StderrResult(old(io.stderr()), io.stderr(), io.trustedStreams(), diagnostics, runExit, exit) + } +} diff --git a/bench/utils/mkfifo/Tests.py b/bench/utils/mkfifo/Tests.py new file mode 100644 index 0000000..a8c9724 --- /dev/null +++ b/bench/utils/mkfifo/Tests.py @@ -0,0 +1,63 @@ +"""GNU parity cases for mkfifo.""" + +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 = "mkfifo" +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) + + +# Replace this failure with one GNU scenario from the specified scope using +# executables and assert_parity. +def test_gnu_parity() -> None: + # TODO: add the upstream source path inside the completed test body. + pytest.fail("TODO: add a representative mkfifo GNU parity case") + + +# Check each proof module as well as the entry contract required by make check. +@pytest.mark.dafny_verify +@pytest.mark.parametrize( + "filename", ["MkfifoCore.dfy", "MkfifoProof.dfy", "Mkfifo.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/mkfifo/benchmark.yaml b/bench/utils/mkfifo/benchmark.yaml new file mode 100644 index 0000000..64da4ad --- /dev/null +++ b/bench/utils/mkfifo/benchmark.yaml @@ -0,0 +1,9 @@ +schema_version: benchmark.definition.v2 +task_id: "mkfifo" +kind: coreutils +source: + status: incomplete + name: TODO +capabilities: + gnu_reference: true + fuzzer: true diff --git a/bench/utils/mkfifo/dfyconfig.toml b/bench/utils/mkfifo/dfyconfig.toml new file mode 100644 index 0000000..28f621d --- /dev/null +++ b/bench/utils/mkfifo/dfyconfig.toml @@ -0,0 +1,6 @@ +includes = ["MkfifoCli.dfy"] + +[options] +target = "cs" +no-verify = true +standard-libraries = false diff --git a/bench/utils/mkfifo/mkfifo.md b/bench/utils/mkfifo/mkfifo.md new file mode 100644 index 0000000..2e56b29 --- /dev/null +++ b/bench/utils/mkfifo/mkfifo.md @@ -0,0 +1,133 @@ +# mkfifo + +## Scope + +This benchmark creates one FIFO per operand, in command-line order. It supports +`-m MODE` / `--mode=MODE` with octal and symbolic modes, unique long-option +abbreviations, options after operands, `--`, `--help`, `--version`, and GNU +parsing diagnostics. A failed operand does not roll back earlier FIFOs or +prevent later operands from being tried. + +- Reference: GNU coreutils `src/mkfifo.c` at + `2cf491412c199e2211880ec3f4ba387026638a33` and gnulib `lib/modechange.c` + (`mode_compile`, `mode_adjust`) at `83730551b451b43577531986a5c4300e0166c42f`; + upstream test `tests/misc/mknod.sh` (its `mkfifo -m 734` and + `mkfifo --mode='ug+rw,o+r'` cases); GPL-3.0-or-later, + . +- Model/API revision: repository revision + `37b35bac3d4cf84cdd8ea02eb3279e8aa49307df`; shared `bench/core/IO.dfy` and + `IOContract.dfy` are the trusted native boundary. +- AllowedInput: finite sequences of Linux paths representable as UTF-8 strings, + including empty operands, repeated paths, relative/absolute paths, trailing + separators, missing parents, existing names and dangling symlinks. Embedded + NUL is outside the native argv domain. `-m` may appear before or after + operands and more than once; the last one is used. Any MODE string is + accepted as input; whether it is valid is defined in [MODE](#mode). +- EnvironmentProfile: Linux, C locale, `TZ=UTC0`, and the filesystem, + credentials and umask supplied by the shared IO model. The mode, ownership, + timestamps and storage of a created FIFO are request-bound trusted + observations of `CreateSpecialNode`, not a simulation of the POSIX policy. +- Observation: exact stdout/stderr bytes and exit status, the resulting + namespace and FIFO inode metadata, and partial effects: a FIFO whose + permission change failed stays in place. Standard input is not consumed. + Standard output is written only by `--help` and `--version`. +- TrustedOperations: one `CreateSpecialNode(path, FIFO, mode, 0, 0)` call per + operand, where `mode` is `0666` without `-m` and the computed MODE result with + `-m` (the native call applies the process umask); after each successful + creation, and only when `-m` is given, one `SetFileMode(path, false, mode)` + call, which is GNU's `lchmod`; `GetUmask`; GNU path quoting; C-locale errno + text; and stream writes. MODE parsing and evaluation, operand iteration, + diagnostic order and the exit policy are implemented and proved. +- OptionsLeftOut: `-Z`, `--context[=CTX]` (see below). + +## Options left out due to IO.dfy + +| Option | Missing API support and source evidence | +| --- | --- | +| `-Z`, `--context[=CTX]` | `src/mkfifo.c` checks whether SMACK or SELinux is enabled and then calls `selabel_open`/`defaultcon`, `setfscreatecon` or `smack_set_label_for_self`. `IO.dfy` has no operation for the kernel's security-module state, file labels or the default creation context. On a kernel without SELinux/SMACK, GNU ignores `-Z` and `--context` and warns for `--context=CTX`, but that depends on kernel state the model cannot observe. This matches the `mkdir` decision. | + +These are model limits, not approximated behavior. Informational help keeps the +pinned GNU program's complete text. The generator restricts option pools to the +supported domain. + +## MODE + +MODE is evaluated once, before any operand is processed, starting from `a=rw` +(`0666`). + +- Octal: the whole string is octal digits with a value of at most `07777`. The + result is exactly that value; the umask does not apply, because GNU sets the + permissions again with `lchmod` after creation. +- Symbolic: one or more clauses separated by `,`. A clause is `[ugoa]*` followed + by one or more actions. An action is `+`, `-` or `=`, followed by `[rwxXst]*` + (possibly empty), by one of `u`, `g`, `o` (copy that class's current bits), or + by octal digits. Octal digits are allowed only when the clause has no `ugoa` + letters and the action is the last one in its clause; such an action affects + every mode bit. Actions apply from left to right. Without `ugoa` letters, the + umask limits the change. `X` adds execute bits only if an execute bit is + already set, because a FIFO is never a directory. +- Invalid MODE: if no expression of this grammar spells the string, mkfifo + writes `mkfifo: invalid mode`, exits 1 and creates nothing. +- Special bits: if the result has a set-user-ID, set-group-ID or sticky bit, + mkfifo writes `mkfifo: mode must specify only file permission bits`, exits 1 + and creates nothing. +- Both MODE errors are reported only after at least one operand is present; + `mkfifo -m bad` reports the missing operand instead. + +Examples with umask `022`: + +| MODE | Result | +| --- | --- | +| `0644`, `00000000644` | `0644` | +| `=rw,+x` | `0755` | +| `-w` | `0466` | +| `+644,u+x` | `0766` | +| `+X` / `u+x,+X` | `0666` / `0777` | +| `o+s`, `g+t` | `0666` (no effect) | +| `+s`, `u+s`, `+t`, `7777` | special-bits error | +| `10000`, `8`, empty, `u`, `+ur`, `u+644`, `+644u`, `u+r,`, `,u+r` | `invalid mode` | + +## Specification and proof + +- SpecificationEntry: `MkfifoSpec.Spec` relates each ordered operand to its + trusted creation effect and, when `-m` is given and creation succeeded, its + permission-change effect. Existential intermediate filesystems retain all + effects; byte partitions determine exact stderr. The MODE relation is stated + as abstract syntax, a `Render` function and a `Meaning` function, without a + parsing algorithm: a string is valid iff a well-formed expression renders to + it, and the result is that expression's meaning. +- Proof of MODE: Core's parser is proved to invert `Render` + (`Parse(Render(e)) == Some(e)` for every well-formed `e`, and a successful + parse renders back to its input). This makes the `invalid mode` decision exact + and shows that a valid string has one meaning. +- Frame: TODO after implementation; expected to modify only `fsRegion` and + `stderrRegion`, and to read `umaskRegion` and the trusted filesystem/stream + regions. +- TerminationPolicy: MODE parsing and the operand loop terminate for every + finite input. The shared CLI runner and parser keep their existing + nontermination/trusted boundary; CLI termination is not established. +- CLI boundary: help/version, parse errors and missing-operand requests use + early-exit plans; parsing remains the shared trusted boundary. `RunCore` + directly ensures `Spec(raw, io, exit)` for every decoded command with at + least one operand, including both MODE errors. +- Normal/error behavior: a successful operand writes nothing. A failed creation + writes `mkfifo: cannot create fifo : `; a failed permission + change writes `mkfifo: cannot set permissions of : ` and + leaves the FIFO in place. `` uses GNU quoting. Later operands are still + tried. Exit is 0 iff every operand succeeded and the stream writes succeeded, + and 1 otherwise. + +For example, with umask `022`, `mkfifo -m 600 pipe` creates a previously absent +FIFO `pipe` with mode `0600`, writes nothing and exits 0. + +The specification rejects success for an existing name, a creation request with +a different mode, a missing or extra permission change, a permission change +after a failed creation or one that follows a symlink, reordered or missing +diagnostics, rollback of earlier FIFOs, stopping before a later operand after an +error, and creating anything after an invalid MODE. + +## Contribution and review evidence + +TODO after the code is complete and verified: commands, versions, test +scenarios, seeds, case counts and verified files. Keep evaluator-only regression +inputs and reference answers outside this public description. From bbc1ad72fcae8d133b068828bce7c42bc3ba8685 Mon Sep 17 00:00:00 2001 From: jkkms Date: Fri, 23 Oct 2026 17:05:41 +0000 Subject: [PATCH 2/8] [Tests] add mkfifo GNU parity cases Problem: the mkfifo scaffold had no runtime cases, and the ambiguous empty long option ("--=", "--=x") did not list GNU's possibilities. Approach: port tests/misc/mknod.sh (octal and symbolic -m under umask 777) and add cases for default modes, MODE expressions under several umasks, invalid and special-bit MODEs, existing names, path errors, an unwritable directory, partial effects, quoting, option forms, information requests, parse errors and /dev/full streams. Fix the ambiguous-option text in Spec. Boundaries: bench/utils/mkfifo only (Tests.py and MkfifoSpec.dfy). Validation: make -C bench/utils/mkfifo test -> 145 passed, 6 deselected; dafny-benchmark verify MkfifoSpec.dfy (isolated, 30 s) -> 0 errors. Limitations: the fuzzer generator, make check and the fuzzing campaigns are still to come. A failed permission change after a successful creation cannot be triggered by these fixtures. Co-Authored-By: Claude Opus 5.5 --- bench/utils/mkfifo/MkfifoSpec.dfy | 8 +- bench/utils/mkfifo/Tests.py | 415 ++++++++++++++++++++++++++++-- 2 files changed, 404 insertions(+), 19 deletions(-) diff --git a/bench/utils/mkfifo/MkfifoSpec.dfy b/bench/utils/mkfifo/MkfifoSpec.dfy index 7472000..172d78a 100644 --- a/bench/utils/mkfifo/MkfifoSpec.dfy +++ b/bench/utils/mkfifo/MkfifoSpec.dfy @@ -401,9 +401,11 @@ module MkfifoSpec { "mkfifo: option '" + Utf8.Encode(NoArgLongOptionName(t)) + "' doesn't allow an argument\n" + TryHelpText() else - // The declared long options (mode, help, version) share no prefix, so an - // ambiguous abbreviation cannot occur. - "mkfifo: option '" + Utf8.Encode(t) + "' is ambiguous\n" + TryHelpText() + // The declared long options (mode, help, version) share no prefix, so only an + // empty name ("--=", "--=x") is ambiguous; GNU then lists every long option. + "mkfifo: option '" + Utf8.Encode(t) + + "' is ambiguous; possibilities: '--context' '--mode' '--help' '--version'\n" + + TryHelpText() } // --------------------------------------------------------------------------- diff --git a/bench/utils/mkfifo/Tests.py b/bench/utils/mkfifo/Tests.py index a8c9724..5ea866c 100644 --- a/bench/utils/mkfifo/Tests.py +++ b/bench/utils/mkfifo/Tests.py @@ -1,16 +1,24 @@ -"""GNU parity cases for mkfifo.""" +"""Benchmark oracle/scoring cases comparing bounded GNU and Dafny mkfifo fixtures.""" +import os +import stat +import subprocess +from collections.abc import Callable +from dataclasses import dataclass from pathlib import Path import pytest +from evaluation.submission.candidate_execution import run_candidate from tools.bench_test_support import ( + BENCH_COMMAND_TIMEOUT_SEC, assert_result_matches_reference, bench_dll_path, build_bench_utility, build_coreutils_utility, coreutils_binary_path, evaluation_target_root, + parity_env, run_bench_utility, run_coreutils_utility, run_dafny_verify, @@ -19,11 +27,26 @@ ROOT = evaluation_target_root(Path(__file__).resolve().parents[3]) UTILITY = "mkfifo" PROJECT = ROOT / "bench" / "utils" / UTILITY +INVALID_MODE = b"mkfifo: invalid mode\n" +SPECIAL_BITS = b"mkfifo: mode must specify only file permission bits\n" +MISSING_OPERAND = b"mkfifo: missing operand\nTry 'mkfifo --help' for more information.\n" + + +@dataclass(frozen=True) +class Entry: + kind: int + mode: int + uid: int + gid: int + links: int + identity: str + contents: bytes + target: str @pytest.fixture(scope="session") def executables() -> tuple[Path, Path]: - """Build the two targets only for runtime cases; local Make targets use -n0.""" + """Build each benchmark target once, independently of development tests.""" build_bench_utility(ROOT, UTILITY) build_coreutils_utility(ROOT, UTILITY) return ( @@ -32,32 +55,392 @@ def executables() -> tuple[Path, Path]: ) +def snapshot(cwd: Path) -> dict[str, Entry]: + """Observe this benchmark's small fixtures: kind, mode, owner, links and bytes.""" + identities: dict[tuple[int, int], str] = {} + entries: dict[str, Entry] = {} + for path in [cwd, *sorted(cwd.rglob("*"))]: + metadata = path.lstat() + relative = path.relative_to(cwd).as_posix() + identity = identities.setdefault((metadata.st_dev, metadata.st_ino), relative) + entries[relative] = Entry( + stat.S_IFMT(metadata.st_mode), + stat.S_IMODE(metadata.st_mode), + metadata.st_uid, + metadata.st_gid, + metadata.st_nlink, + identity, + path.read_bytes() if stat.S_ISREG(metadata.st_mode) else b"", + os.readlink(path) if stat.S_ISLNK(metadata.st_mode) else "", + ) + return entries + + +def restore_access(cwd: Path) -> None: + """Let pytest remove fixtures whose directories were made read-only.""" + for path in [cwd, *cwd.rglob("*")]: + if path.is_dir() and not path.is_symlink(): + path.chmod(0o700) + + def assert_parity( executables: tuple[Path, Path], args: list[str], - cwd: Path, - *, - input_data: bytes = b"", + workspace: Path, + setup: Callable[[Path], None] | None = None, + mask: int = 0o022, +) -> tuple[tuple[bytes, bytes, int], dict[str, Entry]]: + """Compare streams, status and complete fixture effects under one umask.""" + reference_dir = workspace / "reference" + candidate_dir = workspace / "candidate" + for cwd in (reference_dir, candidate_dir): + cwd.mkdir(mode=0o700) + cwd.chmod(0o700) + if setup is not None: + setup(cwd) + reference, candidate = executables + previous = os.umask(mask) + try: + expected = run_coreutils_utility(reference, UTILITY, args, reference_dir) + actual = run_bench_utility(candidate, args, candidate_dir) + finally: + os.umask(previous) + try: + assert_result_matches_reference(expected, actual, ignore_stderr_when_exit_nonzero=False) + expected_fs = snapshot(reference_dir) + assert snapshot(candidate_dir) == expected_fs + finally: + restore_access(reference_dir) + restore_access(candidate_dir) + return expected, expected_fs + + +# A plain operand creates one FIFO with the default mode. +def test_creates_fifo(executables: tuple[Path, Path], tmp_path: Path) -> None: + # upstream: coreutils/tests/misc/mknod.sh + # Port mkfifo_or_skip_'s plain "mkfifo fifo" creation. + result, entries = assert_parity(executables, ["fifo"], tmp_path) + assert result == (b"", b"", 0) + assert stat.S_ISFIFO(entries["fifo"].kind) + assert entries["fifo"].mode == 0o644 + + +# An octal MODE is applied exactly, even when the umask clears every bit. +def test_octal_mode_ignores_umask(executables: tuple[Path, Path], tmp_path: Path) -> None: + # upstream: coreutils/tests/misc/mknod.sh + # Port "umask 777; mkfifo -m 734 f2". + result, entries = assert_parity(executables, ["-m", "734", "f2"], tmp_path, mask=0o777) + assert result == (b"", b"", 0) + assert entries["f2"].mode == 0o734 + + +# A symbolic MODE with a who list starts from a=rw and ignores the umask. +def test_symbolic_mode_with_who(executables: tuple[Path, Path], tmp_path: Path) -> None: + # upstream: coreutils/tests/misc/mknod.sh + # Port "umask 777; mkfifo --mode='ug+rw,o+r' f5". + result, entries = assert_parity(executables, ["--mode=ug+rw,o+r", "f5"], tmp_path, mask=0o777) + assert result == (b"", b"", 0) + assert entries["f5"].mode == 0o666 + + +# Without -m, the native creation applies the process umask to a=rw. +@pytest.mark.parametrize("mask", [0o000, 0o022, 0o077, 0o137]) +def test_default_mode_umask(executables: tuple[Path, Path], tmp_path: Path, mask: int) -> None: + # upstream: none - Checks src/mkfifo.c's default MODE_RW_UGO creation. + result, entries = assert_parity(executables, ["p"], tmp_path, mask=mask) + assert result == (b"", b"", 0) + assert entries["p"].mode == 0o666 & ~mask + + +# Symbolic actions apply left to right; actions without who use the umask. +@pytest.mark.parametrize( + "mode", + [ + "u+x", + "=rw,+x", + "-w", + "a-rw", + "+644,u+x", + "+X", + "u+x,+X", + "u=g", + "g=u,o-r", + "go=", + "a=", + "=", + "+", + "uu+r", + "o+s", + "g+t", + "u=rwx,g=rx,o=", + "0", + "00000000644", + ], +) +@pytest.mark.parametrize("mask", [0o002, 0o022, 0o077]) +def test_mode_expression( + executables: tuple[Path, Path], tmp_path: Path, mode: str, mask: int ) -> None: - """Compare a read-only scenario, including stderr on error exits.""" + # upstream: none - Checks gnulib modechange.c mode_compile/mode_adjust from 0666. + result, entries = assert_parity(executables, ["-m", mode, "p"], tmp_path, mask=mask) + assert result == (b"", b"", 0) + assert stat.S_ISFIFO(entries["p"].kind) + + +# A MODE that no grammar expression spells is rejected before any creation. +@pytest.mark.parametrize( + "mode", + ["bad", "", "u", "+ur", "u+644", "+644u", "+644+r", "u+r,", ",u+r", "u+r,,g+w", "10000", "8"], +) +def test_invalid_mode(executables: tuple[Path, Path], tmp_path: Path, mode: str) -> None: + # upstream: none - Checks gnulib modechange.c mode_compile rejections. + result, entries = assert_parity(executables, ["-m", mode, "p", "q"], tmp_path) + assert result == (b"", INVALID_MODE, 1) + assert set(entries) == {"."} + + +# A MODE whose result has set-ID or sticky bits is rejected before any creation. +@pytest.mark.parametrize("mode", ["u+s", "+s", "+t", "4644", "7777", "g+s,o+t"]) +def test_special_bits(executables: tuple[Path, Path], tmp_path: Path, mode: str) -> None: + # upstream: none - Checks src/mkfifo.c's S_IRWXUGO check after mode_adjust. + result, entries = assert_parity(executables, ["-m", mode, "p"], tmp_path) + assert result == (b"", SPECIAL_BITS, 1) + assert set(entries) == {"."} + + +# MODE is checked only after an operand is known to exist. +@pytest.mark.parametrize("args", [[], ["-m", "600"], ["-m", "bad"]]) +def test_missing_operand(executables: tuple[Path, Path], tmp_path: Path, args: list[str]) -> None: + # upstream: none - Checks src/mkfifo.c's missing-operand branch before MODE. + result, entries = assert_parity(executables, args, tmp_path) + assert result == (b"", MISSING_OPERAND, 1) + assert set(entries) == {"."} + + +# Every kind of existing name is an error that leaves the entry unchanged. +@pytest.mark.parametrize("operand", ["file", "directory", "fifo", "link", "dangling"]) +@pytest.mark.parametrize("args", [[], ["-m", "600"]]) +def test_existing_name( + executables: tuple[Path, Path], tmp_path: Path, operand: str, args: list[str] +) -> None: + # upstream: none - Checks mkfifo(3)'s EEXIST without following a terminal symlink. + def setup(cwd: Path) -> None: + (cwd / "file").write_bytes(b"kept") + (cwd / "directory").mkdir() + os.mkfifo(cwd / "fifo", 0o600) + (cwd / "link").symlink_to("file") + (cwd / "dangling").symlink_to("absent") + + result, entries = assert_parity(executables, [*args, operand], tmp_path, setup) + assert result[2] == 1 + assert entries["file"].contents == b"kept" + assert entries["fifo"].mode == 0o600 + + +# Invalid paths report the exact syscall error without creating entries. +@pytest.mark.parametrize("operand", ["", ".", "file/child", "missing/child", "loop/child"]) +def test_path_error(executables: tuple[Path, Path], tmp_path: Path, operand: str) -> None: + # upstream: none - Checks Linux path failures exposed by the shared IO contracts. + def setup(cwd: Path) -> None: + (cwd / "file").write_bytes(b"retained") + (cwd / "loop").symlink_to("loop") + + result, entries = assert_parity(executables, [operand], tmp_path, setup) + assert result[2] == 1 + assert set(entries) == {".", "file", "loop"} + + +# A directory without write permission refuses the FIFO; later operands still run. +def test_unwritable_directory(executables: tuple[Path, Path], tmp_path: Path) -> None: + # upstream: none - Checks EACCES from mkfifo(3) and continued processing. + def setup(cwd: Path) -> None: + (cwd / "locked").mkdir() + (cwd / "locked").chmod(0o555) + + result, entries = assert_parity(executables, ["locked/p", "open"], tmp_path, setup) + assert result[2] == 1 + assert "locked/p" not in entries + assert stat.S_ISFIFO(entries["open"].kind) + + +# Earlier FIFOs survive a later failure, and the last operand is still tried. +@pytest.mark.parametrize("args", [[], ["-m", "600"], ["-m", "g+w"]]) +def test_partial_effects(executables: tuple[Path, Path], tmp_path: Path, args: list[str]) -> None: + # upstream: none - Checks src/mkfifo.c's ordered-operand loop. + result, entries = assert_parity( + executables, [*args, "first", "missing/child", "last"], tmp_path + ) + assert result[2] == 1 + assert set(entries) == {".", "first", "last"} + + +# A repeated operand is created once and then reported as existing. +def test_repeated_operand(executables: tuple[Path, Path], tmp_path: Path) -> None: + # upstream: none - Checks sequential effects between operands. + result, entries = assert_parity(executables, ["-m", "640", "p", "p"], tmp_path) + assert result[2] == 1 + assert entries["p"].mode == 0o640 + + +# Failure diagnostics quote names with GNU's quoteaf rules. +@pytest.mark.parametrize( + "operand", ["can't/p", "a b/p", "#hash/p", "~tilde/p", "tab\tname/p", "nl\nname/p", "é/p"] +) +def test_quoted_failure(executables: tuple[Path, Path], tmp_path: Path, operand: str) -> None: + # upstream: none - Checks quoteaf in "cannot create fifo" diagnostics. + result, entries = assert_parity(executables, [operand], tmp_path) + assert result[2] == 1 + assert set(entries) == {"."} + + +# -m may follow operands, repeat (last wins), attach its value or be abbreviated. +@pytest.mark.parametrize( + "args", + [ + ["x", "-m", "640", "y"], + ["-m", "600", "-m", "640", "z"], + ["-m600", "p"], + ["--mode", "600", "p"], + ["--mode=600", "p"], + ["--mo=700", "p"], + ["--m", "700", "p"], + ], +) +def test_mode_option_forms(executables: tuple[Path, Path], tmp_path: Path, args: list[str]) -> None: + # upstream: coreutils/tests/misc/invalid-opt.pl + # Port getopt_long permutation, abbreviation and attached-value conventions. + result, _ = assert_parity(executables, args, tmp_path) + assert result == (b"", b"", 0) + + +# A double dash makes option-looking names ordinary operands. +def test_double_dash(executables: tuple[Path, Path], tmp_path: Path) -> None: + # upstream: coreutils/tests/misc/invalid-opt.pl + result, entries = assert_parity(executables, ["--", "-j", "--help"], tmp_path) + assert result == (b"", b"", 0) + assert set(entries) == {".", "-j", "--help"} + + +# Informational requests use exact GNU bytes, including accepted abbreviations. +@pytest.mark.parametrize("args", [["--help"], ["--version"], ["--he"], ["--vers"]]) +def test_information(executables: tuple[Path, Path], tmp_path: Path, args: list[str]) -> None: + # upstream: coreutils/tests/help/help-version.sh + result, entries = assert_parity(executables, args, tmp_path) + assert result[2] == 0 + assert set(entries) == {"."} + + +# GNU acts on the first information request or earlier parse error. +@pytest.mark.parametrize( + "args", + [ + ["--help", "--bogus"], + ["--bogus", "--help"], + ["--version", "--help"], + ["--help", "--version"], + ["new", "--help", "--bogus"], + ["-m", "bad", "--help"], + ["--help", "-m"], + ], +) +def test_information_precedence( + executables: tuple[Path, Path], tmp_path: Path, args: list[str] +) -> None: + # upstream: coreutils/tests/help/help-version.sh + result, entries = assert_parity(executables, args, tmp_path) + assert set(entries) == {"."} + assert result[2] in (0, 1) + + +# Malformed options preserve GNU bytes and create nothing. +@pytest.mark.parametrize( + "args", + [ + ["--bogus", "p"], + ["-Q", "p"], + ["-Qm", "600", "p"], + ["-m"], + ["--mode"], + ["--mo"], + ["--help=value"], + ["--version=1"], + ["--he=x"], + ["-é", "p"], + ["--=", "p"], + ["--=x", "p"], + ], +) +def test_parse_error(executables: tuple[Path, Path], tmp_path: Path, args: list[str]) -> None: + # upstream: coreutils/tests/misc/invalid-opt.pl + result, entries = assert_parity(executables, args, tmp_path) + assert result[2] == 1 + assert set(entries) == {"."} + + +def run_with_full_stream( + executables: tuple[Path, Path], tmp_path: Path, args: list[str], stream: str +) -> tuple[tuple[bytes, bytes, int], tuple[bytes, bytes, int]]: + """Run both programs with one standard stream connected to /dev/full.""" 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) + results = [] + for name, runner in (("reference", "gnu"), ("candidate", "dafny")): + cwd = tmp_path / name + cwd.mkdir() + with Path("/dev/full").open("wb") as full: + streams = { + "stdout": full if stream == "stdout" else subprocess.PIPE, + "stderr": full if stream == "stderr" else subprocess.PIPE, + } + common = { + "cwd": cwd, + "check": False, + "env": parity_env(), + "timeout": BENCH_COMMAND_TIMEOUT_SEC, + **streams, + } + if runner == "gnu": + done = subprocess.run([UTILITY, *args], executable=str(reference), **common) + else: + done = run_candidate(candidate, args, **common) + results.append((done.stdout or b"", done.stderr or b"", done.returncode, snapshot(cwd))) + (gout, gerr, gcode, gfs), (dout, derr, dcode, dfs) = results + assert gfs == dfs + return (gout, gerr, gcode), (dout, derr, dcode) + + +# A full stdout does not matter: mkfifo writes nothing there on success. +def test_full_stdout_success(executables: tuple[Path, Path], tmp_path: Path) -> None: + # upstream: coreutils/tests/misc/write-errors.sh + # Apply its /dev/full scenario; close_stdout has nothing to flush. + expected, actual = run_with_full_stream(executables, tmp_path, ["p"], "stdout") assert_result_matches_reference(expected, actual, ignore_stderr_when_exit_nonzero=False) + assert expected[2] == 0 -# Replace this failure with one GNU scenario from the specified scope using -# executables and assert_parity. -def test_gnu_parity() -> None: - # TODO: add the upstream source path inside the completed test body. - pytest.fail("TODO: add a representative mkfifo GNU parity case") +# A full stderr keeps the creation effects and the failure status. +def test_full_stderr_failure(executables: tuple[Path, Path], tmp_path: Path) -> None: + # upstream: coreutils/tests/misc/write-errors.sh + # Apply its /dev/full scenario to the diagnostic stream. + expected, actual = run_with_full_stream( + executables, tmp_path, ["first", "missing/child"], "stderr" + ) + assert_result_matches_reference(expected, actual, ignore_stderr_when_exit_nonzero=False) + assert expected[2] == 1 -# Check each proof module as well as the entry contract required by make check. +# Check specification well-formedness, helpers and the entry obligation separately. @pytest.mark.dafny_verify @pytest.mark.parametrize( - "filename", ["MkfifoCore.dfy", "MkfifoProof.dfy", "Mkfifo.dfy"] + "filename", + [ + "MkfifoSpec.dfy", + "MkfifoModeCore.dfy", + "MkfifoModeProof.dfy", + "MkfifoCore.dfy", + "MkfifoProof.dfy", + "Mkfifo.dfy", + ], ) def test_verify_module(filename: str) -> None: - # upstream: none - Checks the Dafny proof surface, not GNU runtime behavior. + # upstream: none - Checks proof obligations rather than GNU runtime behavior. run_dafny_verify(PROJECT / filename) From 837da079dcb1ba38b1bbafd14515f7e23b388b80 Mon Sep 17 00:00:00 2001 From: jkkms Date: Sat, 24 Oct 2026 02:47:54 +0000 Subject: [PATCH 3/8] [Fuzzer] add mkfifo generator and FIFO snapshots Problem: the fuzzer had no mkfifo generator, and its filesystem snapshot rejected FIFO nodes as unsupported, so no mkfifo case could be compared. Approach: add generators/mkfifo.rs (MODE in four spellings from chmod's mode generator plus mkfifo edge cases, new/existing/nested operands, options after operands, malformed options and information requests, and 29 deterministic scenarios) and register it with -m/--mode as value flags. Record FIFOs in fs_snapshot.rs from metadata only, without opening them; character devices are still rejected. Add a regression test. Boundaries: shared fuzzer snapshot code gains one node kind; no change to comparison rules or other utilities' generators. Validation: cargo test --release -> 500 passed; cargo fmt --check clean. run.py fuzz mkfifo --seeds 1,7,19 --iterations 1000 -> each seed match=1000 mismatch=0 timeout=0 other_errors=0, option pairs 6/6. Limitations: the generator does not create pre-existing FIFOs in its fixtures; Tests.py covers that case. Co-Authored-By: Claude Opus 5.5 --- .../src/fuzz/comparison/fs_snapshot.rs | 14 ++ .../src/fuzz/input/generators/mkfifo.rs | 176 ++++++++++++++++++ .../src/fuzz/input/generators/mod.rs | 1 + tools/coreutils_fuzzer/src/tests/fuzzer.rs | 26 +++ .../src/utils/capabilities.rs | 9 +- 5 files changed, 224 insertions(+), 2 deletions(-) create mode 100644 tools/coreutils_fuzzer/src/fuzz/input/generators/mkfifo.rs diff --git a/tools/coreutils_fuzzer/src/fuzz/comparison/fs_snapshot.rs b/tools/coreutils_fuzzer/src/fuzz/comparison/fs_snapshot.rs index e3fd04f..856a44d 100644 --- a/tools/coreutils_fuzzer/src/fuzz/comparison/fs_snapshot.rs +++ b/tools/coreutils_fuzzer/src/fuzz/comparison/fs_snapshot.rs @@ -102,6 +102,17 @@ fn to_string_error(result: Result) -> Result { result.map_err(|error| error.to_string()) } +#[cfg(unix)] +fn is_fifo(file_type: &fs::FileType) -> bool { + use std::os::unix::fs::FileTypeExt; + file_type.is_fifo() +} + +#[cfg(not(unix))] +fn is_fifo(_file_type: &fs::FileType) -> bool { + false +} + #[cfg(test)] pub(crate) fn snapshot_fs(root: &Path) -> Result { to_string_error(snapshot_fs_checked(root)) @@ -647,6 +658,9 @@ fn snapshot_fs_with_observer_restore( None => read_snapshot_handle(&mut open_snapshot_file(current)?, current)?, }; ("file", String::new(), data) + } else if is_fifo(&file_type) { + // A FIFO has no contents to compare, and opening one could block. + ("fifo", String::new(), Vec::new()) } else { return Err(format!("unsupported filesystem node `{}`", current.display()).into()); }; diff --git a/tools/coreutils_fuzzer/src/fuzz/input/generators/mkfifo.rs b/tools/coreutils_fuzzer/src/fuzz/input/generators/mkfifo.rs new file mode 100644 index 0000000..3c3fb01 --- /dev/null +++ b/tools/coreutils_fuzzer/src/fuzz/input/generators/mkfifo.rs @@ -0,0 +1,176 @@ +use super::super::pattern::{ + Alternative, ArgvPattern, Atom, Element, OperandSource, OptionChoice, OptionValue, + OptionValueForm, ValueContext, ValueSource, +}; +use super::super::PatternInputGenerator; +use super::super::{support, system_state}; +use super::chmod::random_chmod_mode; +use crate::fuzz::{DirSpec, GeneratedCase, SymlinkSpec}; +use rand::rngs::StdRng; +use rand::Rng; +use std::path::PathBuf; + +const MODE: Atom = Atom::OptionValue(OptionValue::new( + &[ + OptionValueForm::separate("-m"), + OptionValueForm::attached("-m"), + OptionValueForm::separate("--mode"), + OptionValueForm::equals("--mode"), + ], + ValueSource::Generated(mode_value), +)); +const INFORMATION: Atom = Atom::Option(OptionChoice::available(&["--help", "--version"])); +const TARGET: Atom = Atom::Operand(OperandSource::Generated(fifo_operand)); +const MALFORMED: Atom = Atom::Value(ValueSource::Values(&[ + "--bogus", + "-Q", + "-Qm", + "--help=value", + "--version=1", + "--he=x", + "-é", + "--=", + "--=x", +])); + +static ARGV_PATTERN: ArgvPattern = ArgvPattern::new(&[ + Alternative::weighted( + 7, + &[ + Element::repeated(0, 2, MODE), + Element::up_to_budget(0, TARGET).captured(0).reusing(25), + ], + ), + // GNU getopt permutes options after operands. + Alternative::weighted( + 2, + &[ + Element::once(TARGET), + Element::once(MODE), + Element::up_to_budget(0, TARGET), + ], + ), + Alternative::weighted( + 2, + &[Element::once(MALFORMED), Element::optional(50, TARGET)], + ), + // Information requests win over a later MODE or malformed option. + Alternative::weighted( + 2, + &[ + Element::optional(40, MODE), + Element::optional(50, TARGET), + Element::repeated(1, 2, INFORMATION), + Element::optional(40, MODE), + Element::optional(30, MALFORMED), + ], + ), +]); + +pub(crate) static GENERATOR: PatternInputGenerator = + PatternInputGenerator::patterned(&ARGV_PATTERN, scenario_case); + +// MODE strings: chmod's generator plus cases specific to mkfifo's 0666 start, +// octal actions inside symbolic modes, and malformed clause lists. +fn mode_value(_context: &ValueContext<'_>, rng: &mut StdRng) -> String { + const MKFIFO_MODES: &[&str] = &[ + "+644,u+x", + "=644,+x", + "+0", + "u=g", + "g=u,o-r", + "a=", + "=", + "+", + "uu+r", + "+X", + "u+x,+X", + "o+s", + "g+t", + "u+s", + "+t", + "4644", + "00000000644", + "u+r,", + ",u+r", + "u+r,,g+w", + "+ur", + "u+644", + "+644u", + "+644+r", + "", + "8", + ]; + if rng.random_bool(0.4) { + MKFIFO_MODES[rng.random_range(0..MKFIFO_MODES.len())].to_string() + } else { + random_chmod_mode(rng) + } +} + +fn fifo_operand(context: &ValueContext<'_>, rng: &mut StdRng) -> String { + let existing = context.fixture().existing_operands(); + if !existing.is_empty() && rng.random_bool(0.3) { + return support::pick_string(&existing, rng); + } + let name = format!("new-fifo-{}", rng.random_range(0..10000)); + match rng.random_range(0..6) { + 0 => format!("absent-parent/{name}"), + 1 if !context.fixture().directories.is_empty() => { + let directory = &context.fixture().directories + [rng.random_range(0..context.fixture().directories.len())]; + directory.relative_path.join(name).display().to_string() + } + 2 => format!("{name}/"), + _ => name, + } +} + +pub(super) fn scenario_case(iteration: usize) -> Option { + let mut fixture = system_state::basic_fixture(); + let args = match iteration { + 0 => vec!["fifo"], + 1 => vec!["-m", "734", "f2"], + 2 => vec!["--mode=ug+rw,o+r", "f5"], + 3 => vec!["-m", "+644,u+x", "p"], + 4 => vec!["-m", "bad", "p", "q"], + 5 => vec!["-m", "u+s", "p"], + 6 => vec!["-m", "bad"], + 7 => vec![], + 8 => vec!["first", "absent/child", "last"], + 9 => vec!["-m", "600", "first", "absent/child", "last"], + 10 => vec!["-m", "640", "p", "p"], + 11 => vec!["x", "-m", "640", "y"], + 12 => vec!["-m", "600", "-m", "640", "z"], + 13 => vec!["-m600", "p"], + 14 => vec!["--mo=700", "p"], + 15 => vec!["--", "-j", "--help"], + 16 => vec!["--help", "--bogus"], + 17 => vec!["--bogus", "--help"], + 18 => vec!["-m", "bad", "--help"], + 19 => vec!["--=x"], + 20 => vec![""], + 21 => vec!["."], + 22 => vec!["a.txt/child"], + 23 => vec!["dir"], + 24 => vec!["a'b/p", "line\nbreak/p", "tab\tname/p", "한글/p"], + 25 => { + fixture.symlinks.push(SymlinkSpec { + relative_path: PathBuf::from("dangling"), + target: PathBuf::from("absent"), + }); + vec!["-m", "600", "dangling"] + } + 26 => { + fixture.directories.push(DirSpec { + relative_path: PathBuf::from("blocked"), + mode: 0o555, + }); + vec!["first", "blocked/new", "last"] + } + 27 => vec!["-m", "=", "p"], + 28 => vec!["-m", "00000000644", "p"], + _ => 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 8073165..7acd1c0 100644 --- a/tools/coreutils_fuzzer/src/fuzz/input/generators/mod.rs +++ b/tools/coreutils_fuzzer/src/fuzz/input/generators/mod.rs @@ -20,6 +20,7 @@ pub(crate) mod ln; pub(crate) mod logname; pub(crate) mod ls; pub(crate) mod mkdir; +pub(crate) mod mkfifo; pub(crate) mod mv; pub(crate) mod nl; pub(crate) mod paste; diff --git a/tools/coreutils_fuzzer/src/tests/fuzzer.rs b/tools/coreutils_fuzzer/src/tests/fuzzer.rs index bc29e74..f17d78d 100644 --- a/tools/coreutils_fuzzer/src/tests/fuzzer.rs +++ b/tools/coreutils_fuzzer/src/tests/fuzzer.rs @@ -1437,6 +1437,32 @@ fn snapshot_fs_rejects_character_device() { assert!(error.contains("/dev/null")); } +// A FIFO is recorded from metadata alone; reading it would block the observer. +#[test] +#[cfg(unix)] +fn snapshot_fs_records_fifo_without_opening_it() { + use std::ffi::CString; + use std::os::raw::c_char; + use std::os::unix::ffi::OsStrExt; + + unsafe extern "C" { + fn mkfifo(pathname: *const c_char, mode: u32) -> i32; + } + let temp = tempfile::tempdir().expect("tempdir"); + let fifo = temp.path().join("pipe"); + let raw = CString::new(fifo.as_os_str().as_bytes()).expect("fifo path"); + assert_eq!(unsafe { mkfifo(raw.as_ptr(), 0o600) }, 0); + + let snapshot = snapshot_fs(temp.path()).expect("FIFO snapshot"); + let node = snapshot + .iter() + .find(|(path, _)| path.ends_with("pipe")) + .map(|(_, node)| node) + .expect("FIFO node"); + + assert_eq!(node.kind, "fifo"); +} + // Repeated reads preserve the modeled tree after excluding observer-induced ctime advancement. #[test] #[cfg(unix)] diff --git a/tools/coreutils_fuzzer/src/utils/capabilities.rs b/tools/coreutils_fuzzer/src/utils/capabilities.rs index 584e7eb..32bde17 100644 --- a/tools/coreutils_fuzzer/src/utils/capabilities.rs +++ b/tools/coreutils_fuzzer/src/utils/capabilities.rs @@ -229,6 +229,11 @@ pub(crate) static UTILITY_CAPABILITIES: &[UtilityCapability] = &[ generated_options: Some(&["-v", "--verbose", "--help", "--version"]), ..capability!("mkdir", mkdir) }, + UtilityCapability { + generated_options: Some(&["-m", "--mode", "--help", "--version"]), + option_value_flags: &["-m", "--mode"], + ..capability!("mkfifo", mkfifo) + }, UtilityCapability { option_value_flags: &["-t", "--target-directory", "-S", "--suffix"], ..capability!("mv", mv) @@ -476,8 +481,8 @@ mod tests { patterned, BTreeSet::from([ "cat", "chmod", "comm", "cp", "csplit", "cut", "du", "expand", "head", "link", - "ln", "ls", "mkdir", "mv", "nl", "paste", "readlink", "rm", "rmdir", "stat", - "tail", "touch", "truncate", "tsort", "uniq", "unlink", "wc", + "ln", "ls", "mkdir", "mkfifo", "mv", "nl", "paste", "readlink", "rm", "rmdir", + "stat", "tail", "touch", "truncate", "tsort", "uniq", "unlink", "wc", ]) ); } From c7cae8c643d09cc1779a1a968fe15ae285b94a69 Mon Sep 17 00:00:00 2001 From: jkkms Date: Sat, 24 Oct 2026 03:20:23 +0000 Subject: [PATCH 4/8] [Docs] complete mkfifo definition and scope evidence Problem: benchmark.yaml was still the scaffold placeholder, so make check stopped at "source details are incomplete", and mkfifo.md left the frame and the evidence section as TODO. Approach: record GNU coreutils mkfifo, its URL and GPL-3.0-or-later license (checked in the src/mkfifo.c header) as verified source details; state the RunCore frame; summarize the measured tests, fuzzing, verification and final-gate results without evaluator inputs or reference answers. Boundaries: bench/utils/mkfifo/benchmark.yaml and mkfifo.md only. Validation: python3 -m benchmarks validate mkfifo -> mkfifo: valid; make check TASK=mkfifo (on da69888 plus this benchmark.yaml) -> mkfifo: checks passed. Limitations: the PR evidence will be rerun on the final commit. Co-Authored-By: Claude Opus 5.5 --- bench/utils/mkfifo/benchmark.yaml | 8 ++++--- bench/utils/mkfifo/mkfifo.md | 37 ++++++++++++++++++++++++++----- 2 files changed, 36 insertions(+), 9 deletions(-) diff --git a/bench/utils/mkfifo/benchmark.yaml b/bench/utils/mkfifo/benchmark.yaml index 64da4ad..8d6e2b4 100644 --- a/bench/utils/mkfifo/benchmark.yaml +++ b/bench/utils/mkfifo/benchmark.yaml @@ -1,9 +1,11 @@ schema_version: benchmark.definition.v2 -task_id: "mkfifo" +task_id: mkfifo kind: coreutils source: - status: incomplete - name: TODO + status: verified + name: GNU coreutils mkfifo + url: https://www.gnu.org/software/coreutils/ + license: GPL-3.0-or-later capabilities: gnu_reference: true fuzzer: true diff --git a/bench/utils/mkfifo/mkfifo.md b/bench/utils/mkfifo/mkfifo.md index 2e56b29..630ed94 100644 --- a/bench/utils/mkfifo/mkfifo.md +++ b/bench/utils/mkfifo/mkfifo.md @@ -100,9 +100,11 @@ Examples with umask `022`: (`Parse(Render(e)) == Some(e)` for every well-formed `e`, and a successful parse renders back to its input). This makes the `invalid mode` decision exact and shows that a valid string has one meaning. -- Frame: TODO after implementation; expected to modify only `fsRegion` and - `stderrRegion`, and to read `umaskRegion` and the trusted filesystem/stream - regions. +- Frame: `RunCore` modifies only `fsRegion` and `stderrRegion`. Its + specification also reads `nowRegion`, `umaskRegion` (the umask the native + creation applies), `propsRegion` (the umask value `GetUmask` returns, used to + evaluate MODE), `trustedFilesystemRegion`, `trustedNativeFailuresRegion` and + `trustedStreamsRegion`. Standard output is not written outside help/version. - TerminationPolicy: MODE parsing and the operand loop terminate for every finite input. The shared CLI runner and parser keep their existing nontermination/trusted boundary; CLI termination is not established. @@ -128,6 +130,29 @@ error, and creating anything after an invalid MODE. ## Contribution and review evidence -TODO after the code is complete and verified: commands, versions, test -scenarios, seeds, case counts and verified files. Keep evaluator-only regression -inputs and reference answers outside this public description. +Measured on commit `da69888` plus the completed `benchmark.yaml`, from base +revision `37b35bac3d4cf84cdd8ea02eb3279e8aa49307df`, in the contributor +container on Linux x86-64: Dafny 4.11.1+10dca3ba4a2909c11299176440401fc31413b53d, +.NET SDK 8.0.132, Python 3.12.3, pytest 9.1.1, Ruff 0.15.12, Rust/Cargo 1.94.0, +Z3 4.16.0. + +- Tests: `make -C bench/utils/mkfifo test` passes 145 runtime cases against the + pinned GNU build, comparing stdout, stderr, exit status and the resulting + filesystem, including the two `mkfifo` cases of `tests/misc/mknod.sh`. +- Fuzzing: `python3 tools/coreutils_fuzzer/run.py fuzz mkfifo --seeds 1,7,19 + --iterations 1000` completed 1000 matches per seed with no mismatch, timeout + or other error; option coverage was 4/4 singles and 6/6 pairs for each seed. + The fuzzer image is `dafnyutils-coreutils-fuzzer:latest` + (`sha256:c312109aeaec50957a8240aa7c52d6bf8b564f18d926afdcf6a672f552f2c6d5`). +- Verification: `make -C bench/utils/mkfifo verify` verified all 85 + declarations and 946 conditions with no failure, using the repository's + isolated assertions, 30-second condition limit and 100-second declaration + limit. Termination of MODE parsing and the operand loop is proved. +- Final gate: `python3 -m benchmarks validate mkfifo` reports `mkfifo: valid`, and + `make check TASK=mkfifo` reports `mkfifo: checks passed`. + +The fuzzer's filesystem snapshot previously rejected FIFO nodes; this +contribution records them from metadata only. A failed permission change after +a successful creation is specified and proved but cannot be produced by the +current fixtures. A maintainer still decides whether the specification is +accepted. From cb7df7ad9687f9e2cc6cf441d944c103b1934d87 Mon Sep 17 00:00:00 2001 From: jkkms Date: Sun, 25 Oct 2026 13:06:14 +0000 Subject: [PATCH 5/8] [Spec] state unchanged stdout and add the mkfifo NL specification Problem: the specification relied on the RunCore frame for standard output and did not state that a normal run leaves it unchanged; review on earlier PRs asked specifications to state what does not change. The scope document also lacked the natural-language description from the GNU manual. Approach: add `io.stdout() == old(io.stdout())` to MkfifoSpec.Spec and carry it through MkfifoProof.Complete and MkfifoCore.RunCore; summarize coreutils.texi "mkfifo invocation" (lines 10848-10886) at the top of mkfifo.md and reword the frame sentence. Boundaries: bench/utils/mkfifo only. Validation: dafny-benchmark verify (isolated, 30 s) on MkfifoSpec.dfy, the Complete lemma, MkfifoCore.RunCore and Mkfifo.RunCore -> 0 errors; python3 -m benchmarks validate mkfifo -> mkfifo: valid. A mutation check of 16 incorrect implementations (controls passing) failed verification in every case, including one that writes to standard output. Limitations: the full evidence is rerun on this commit. Co-Authored-By: Claude Opus 5.5 --- bench/utils/mkfifo/MkfifoCore.dfy | 1 + bench/utils/mkfifo/MkfifoProof.dfy | 1 + bench/utils/mkfifo/MkfifoSpec.dfy | 5 ++++- bench/utils/mkfifo/mkfifo.md | 31 +++++++++++++++++++++++++++++- 4 files changed, 36 insertions(+), 2 deletions(-) diff --git a/bench/utils/mkfifo/MkfifoCore.dfy b/bench/utils/mkfifo/MkfifoCore.dfy index 9cba331..1d35a20 100644 --- a/bench/utils/mkfifo/MkfifoCore.dfy +++ b/bench/utils/mkfifo/MkfifoCore.dfy @@ -168,6 +168,7 @@ module MkfifoCore { io.trustedFilesystem(), io.trustedNativeFailures(), diagnostics, runExit); ghost var runExitValue := runExit; exit := Flush(diagnostics, runExit, io); + assert io.stdout() == old(io.stdout()); Proof.Complete(raw, io, diagnostics, runExitValue, exit); } } diff --git a/bench/utils/mkfifo/MkfifoProof.dfy b/bench/utils/mkfifo/MkfifoProof.dfy index 268c340..4d56f64 100644 --- a/bench/utils/mkfifo/MkfifoProof.dfy +++ b/bench/utils/mkfifo/MkfifoProof.dfy @@ -331,6 +331,7 @@ module MkfifoProof { diagnostics, runExit) requires Spec.StderrResult(old(io.stderr()), io.stderr(), io.trustedStreams(), diagnostics, runExit, exit) + requires io.stdout() == old(io.stdout()) ensures Spec.Spec(raw, io, exit) { hide Spec.RunRelation(); diff --git a/bench/utils/mkfifo/MkfifoSpec.dfy b/bench/utils/mkfifo/MkfifoSpec.dfy index 172d78a..87454ae 100644 --- a/bench/utils/mkfifo/MkfifoSpec.dfy +++ b/bench/utils/mkfifo/MkfifoSpec.dfy @@ -632,11 +632,14 @@ module MkfifoSpec { exit == (if runExit == 0 && errObservation.err == 0 then 0 else 1) } + // Standard output is stated unchanged: mkfifo writes it only for --help and + // --version, which are early exits outside this relation. twostate predicate Spec(raw: Schema.MkfifoCmdRaw, io: BenchIO.IO, exit: int) - reads io.fsRegion, io.stderrRegion, + reads io.fsRegion, io.stdoutRegion, io.stderrRegion, io.nowRegion, io.umaskRegion, io.propsRegion, io.trustedFilesystemRegion, io.trustedNativeFailuresRegion, io.trustedStreamsRegion { + io.stdout() == old(io.stdout()) && exists diagnostics: BenchWorld.Bytes, runExit: int :: RunRelation(raw, old(io.fs()), io.fs(), io.now(), io.umask(), C.GetUmaskResultFields(io.props()), io.trustedFilesystem(), io.trustedNativeFailures(), diagnostics, runExit) && diff --git a/bench/utils/mkfifo/mkfifo.md b/bench/utils/mkfifo/mkfifo.md index 630ed94..535baa7 100644 --- a/bench/utils/mkfifo/mkfifo.md +++ b/bench/utils/mkfifo/mkfifo.md @@ -1,5 +1,33 @@ # mkfifo +## NL specification + +Source: +- `coreutils/doc/coreutils.texi`, `@node mkfifo invocation`, lines 10848-10886 +- Implementation: `coreutils/src/mkfifo.c` at submodule commit + `2cf491412c199e2211880ec3f4ba387026638a33` +- License: GPL-3.0-or-later + +`mkfifo` creates a FIFO, also called a named pipe, for each NAME. A FIFO is a +special file: one process opens it for writing and another for reading, and +data then flows between them as through an anonymous pipe. + +```text +mkfifo [OPTION]... NAME... +``` + +- `-m MODE`, `--mode=MODE`: set the permission bits of each created FIFO to + MODE. MODE is octal or symbolic as in `chmod`, starts from `a=rw`, and must + specify only file permission bits. +- `-Z`, `--context[=CTX]`: set an SELinux or SMACK security context. These + are outside this benchmark (see below). +- `--help`, `--version`: print information and exit. + +Without `-m`, a FIFO gets `a=rw` minus the process umask. The exit status is +0 when every FIFO was created and, with `-m`, received its permissions; it is +1 after any failed operand, an option error, a missing operand or a rejected +MODE. + ## Scope This benchmark creates one FIFO per operand, in command-line order. It supports @@ -104,7 +132,8 @@ Examples with umask `022`: specification also reads `nowRegion`, `umaskRegion` (the umask the native creation applies), `propsRegion` (the umask value `GetUmask` returns, used to evaluate MODE), `trustedFilesystemRegion`, `trustedNativeFailuresRegion` and - `trustedStreamsRegion`. Standard output is not written outside help/version. + `trustedStreamsRegion`. The specification states that standard output is + unchanged; mkfifo writes it only for help and version, which exit early. - TerminationPolicy: MODE parsing and the operand loop terminate for every finite input. The shared CLI runner and parser keep their existing nontermination/trusted boundary; CLI termination is not established. From a832a0ced933aa30be228526b0e8518f634acade Mon Sep 17 00:00:00 2001 From: jkkms Date: Sun, 25 Oct 2026 14:22:11 +0000 Subject: [PATCH 6/8] [Docs] keep mkfifo evidence independent of the tested revision Problem: the evidence section of mkfifo.md named commit da69888 and a verification count of 946 conditions. Adding the unchanged-stdout clause in 8f55d4a raised the count to 955, so the document no longer matched the commit it ships with, and any later revision would make it stale again. Approach: point to the pull request for the tested commit, artifact hashes, fuzzer image and full outputs; keep the base revision, tool versions, commands and the results that do not depend on the revision; state that every declaration verifies instead of giving counts. Boundaries: bench/utils/mkfifo/mkfifo.md only. Validation: python3 -m benchmarks validate mkfifo -> mkfifo: valid. Limitations: none; the PR evidence is rerun on this commit. Co-Authored-By: Claude Opus 5.5 --- bench/utils/mkfifo/mkfifo.md | 20 +++++++++----------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/bench/utils/mkfifo/mkfifo.md b/bench/utils/mkfifo/mkfifo.md index 535baa7..15f0b57 100644 --- a/bench/utils/mkfifo/mkfifo.md +++ b/bench/utils/mkfifo/mkfifo.md @@ -159,11 +159,11 @@ error, and creating anything after an invalid MODE. ## Contribution and review evidence -Measured on commit `da69888` plus the completed `benchmark.yaml`, from base -revision `37b35bac3d4cf84cdd8ea02eb3279e8aa49307df`, in the contributor -container on Linux x86-64: Dafny 4.11.1+10dca3ba4a2909c11299176440401fc31413b53d, -.NET SDK 8.0.132, Python 3.12.3, pytest 9.1.1, Ruff 0.15.12, Rust/Cargo 1.94.0, -Z3 4.16.0. +The pull request records the tested commit, the artifact hashes, the fuzzer +image and the full outputs. The results below were measured from base revision +`37b35bac3d4cf84cdd8ea02eb3279e8aa49307df` in the contributor container on +Linux x86-64: Dafny 4.11.1+10dca3ba4a2909c11299176440401fc31413b53d, .NET SDK +8.0.132, Python 3.12.3, pytest 9.1.1, Ruff 0.15.12, Rust/Cargo 1.94.0, Z3 4.16.0. - Tests: `make -C bench/utils/mkfifo test` passes 145 runtime cases against the pinned GNU build, comparing stdout, stderr, exit status and the resulting @@ -171,12 +171,10 @@ Z3 4.16.0. - Fuzzing: `python3 tools/coreutils_fuzzer/run.py fuzz mkfifo --seeds 1,7,19 --iterations 1000` completed 1000 matches per seed with no mismatch, timeout or other error; option coverage was 4/4 singles and 6/6 pairs for each seed. - The fuzzer image is `dafnyutils-coreutils-fuzzer:latest` - (`sha256:c312109aeaec50957a8240aa7c52d6bf8b564f18d926afdcf6a672f552f2c6d5`). -- Verification: `make -C bench/utils/mkfifo verify` verified all 85 - declarations and 946 conditions with no failure, using the repository's - isolated assertions, 30-second condition limit and 100-second declaration - limit. Termination of MODE parsing and the operand loop is proved. +- Verification: `make -C bench/utils/mkfifo verify` verified every declaration + with no failure, using the repository's isolated assertions, 30-second + condition limit and 100-second declaration limit. Termination of MODE parsing + and the operand loop is proved. - Final gate: `python3 -m benchmarks validate mkfifo` reports `mkfifo: valid`, and `make check TASK=mkfifo` reports `mkfifo: checks passed`. From 98c78a4b3df89ad09c61304191b11477e5c43ffc Mon Sep 17 00:00:00 2001 From: jkkms Date: Fri, 30 Oct 2026 03:47:12 +0000 Subject: [PATCH 7/8] [Core] compute mkfifo MODE with loops at run time Problem: Review of #42: the MODE parser and Meaning recursed once per character, so a long MODE overflowed the stack. A MODE of 50,000 characters (`0...0600` or `u...u+r`) crashed with "Stack overflow", and 20,000 characters took 12 s because every step copied the rest of the string. Approach: The recursive functions stay as the definitions the proofs use. ParseMode gets a `by method` body that walks indices of the string, and DecideMode calls ComputeMeaning instead of Spec.Meaning; each loop is proved to return the value of the function it replaces. Octal digits stop at the first value above 07777, as mode_compile does. Small helper methods hide the other spec definitions so that each step verifies within the time limit. mkfifo.md describes this and the new base revision. Boundaries: MkfifoModeCore.dfy, one call in MkfifoCore.dfy and mkfifo.md. The specification and the proofs are unchanged. Validation: make -C bench/utils/mkfifo verify -> 112 declarations, 1,542 conditions, 0 failed; make check TASK=mkfifo passes. A MODE of 100,000 characters now finishes in 0.3 s. Three incorrect variants of the new loops (trailing comma accepted, 07777 limit off by one, last clause skipped) each fail verification. Limitations: The recursive functions are still compiled, but no run-time path calls them. Co-Authored-By: Claude Opus 5.5 --- bench/utils/mkfifo/MkfifoCore.dfy | 2 +- bench/utils/mkfifo/MkfifoModeCore.dfy | 458 ++++++++++++++++++++++++++ bench/utils/mkfifo/mkfifo.md | 14 +- 3 files changed, 468 insertions(+), 6 deletions(-) diff --git a/bench/utils/mkfifo/MkfifoCore.dfy b/bench/utils/mkfifo/MkfifoCore.dfy index 1d35a20..c979355 100644 --- a/bench/utils/mkfifo/MkfifoCore.dfy +++ b/bench/utils/mkfifo/MkfifoCore.dfy @@ -55,7 +55,7 @@ module MkfifoCore { if parsed.None? { plan := Spec.RejectInvalidMode; } else { - var bits := Spec.Meaning(parsed.value, umask); + var bits := P.ComputeMeaning(parsed.value, umask); plan := if Spec.OnlyPermissionBits(bits) then Spec.ExplicitMode(bits) else Spec.RejectSpecialBits; } diff --git a/bench/utils/mkfifo/MkfifoModeCore.dfy b/bench/utils/mkfifo/MkfifoModeCore.dfy index e0cd4b7..f3dd3eb 100644 --- a/bench/utils/mkfifo/MkfifoModeCore.dfy +++ b/bench/utils/mkfifo/MkfifoModeCore.dfy @@ -3,6 +3,11 @@ include "MkfifoSpec.dfy" // Executable MODE parser. It reads the string from left to right, as GNU // mode_compile does, and builds the abstract syntax defined in MkfifoSpec. // MkfifoModeProof shows that it inverts MkfifoSpec.Render. +// +// The recursive functions define the parser for the proofs. At run time +// ParseMode and ComputeMeaning use the loops at the end of this module: they +// walk indices of the string, so a long MODE neither grows the call stack nor +// copies the string once per letter. module MkfifoModeCore { import S = MkfifoSpec @@ -149,5 +154,458 @@ module MkfifoModeCore { match ParseClauses(s) case None => None case Some(cs) => Some(S.Symbolic(cs)) + } by method { + assert s[0..] == s; + if |s| > 0 && IsOctalChar(s[0]) { + var ds, j := TakeDigitsAt(s, 0); + if j == |s| { + var _, within := OctalUpTo(ds); + r := if within then Some(S.Absolute(ds)) else None; + } else { + r := None; + } + } else { + var cs := ParseClausesFrom(s); + r := if cs.None? then None else Some(S.Symbolic(cs.value)); + } + } + + // --------------------------------------------------------------------------- + // Loops used at run time. Each one ends where the function of the same name + // would stop: Take*At(s, i) returns the value of Take*(s[i..]) and the index + // of the unread rest. + // --------------------------------------------------------------------------- + + method TakeWhoAt(s: string, i: nat) returns (xs: seq, j: nat) + requires i <= |s| + ensures i <= j <= |s| + ensures TakeWho(s[i..]).0 == xs && TakeWho(s[i..]).1 == s[j..] + { + xs, j := [], i; + assert [] + TakeWho(s[i..]).0 == TakeWho(s[i..]).0; + while j < |s| && IsWhoChar(s[j]) + invariant i <= j <= |s| + invariant TakeWho(s[i..]).0 == xs + TakeWho(s[j..]).0 + invariant TakeWho(s[i..]).1 == TakeWho(s[j..]).1 + { + ghost var rest := TakeWho(s[j + 1..]); + assert s[j..][1..] == s[j + 1..]; + assert TakeWho(s[j..]).0 == [WhoOf(s[j])] + rest.0 && TakeWho(s[j..]).1 == rest.1; + assert xs + ([WhoOf(s[j])] + rest.0) == (xs + [WhoOf(s[j])]) + rest.0; + xs, j := xs + [WhoOf(s[j])], j + 1; + } + assert xs + [] == xs; + } + + method TakePermsAt(s: string, i: nat) returns (xs: seq, j: nat) + requires i <= |s| + ensures i <= j <= |s| + ensures TakePerms(s[i..]).0 == xs && TakePerms(s[i..]).1 == s[j..] + { + xs, j := [], i; + assert [] + TakePerms(s[i..]).0 == TakePerms(s[i..]).0; + while j < |s| && IsPermChar(s[j]) + invariant i <= j <= |s| + invariant TakePerms(s[i..]).0 == xs + TakePerms(s[j..]).0 + invariant TakePerms(s[i..]).1 == TakePerms(s[j..]).1 + { + ghost var rest := TakePerms(s[j + 1..]); + assert s[j..][1..] == s[j + 1..]; + assert TakePerms(s[j..]).0 == [PermOf(s[j])] + rest.0 && TakePerms(s[j..]).1 == rest.1; + assert xs + ([PermOf(s[j])] + rest.0) == (xs + [PermOf(s[j])]) + rest.0; + xs, j := xs + [PermOf(s[j])], j + 1; + } + assert xs + [] == xs; + } + + method TakeDigitsAt(s: string, i: nat) returns (xs: seq, j: nat) + requires i <= |s| + ensures i <= j <= |s| + ensures TakeDigits(s[i..]).0 == xs && TakeDigits(s[i..]).1 == s[j..] + { + xs, j := [], i; + assert [] + TakeDigits(s[i..]).0 == TakeDigits(s[i..]).0; + while j < |s| && IsOctalChar(s[j]) + invariant i <= j <= |s| + invariant TakeDigits(s[i..]).0 == xs + TakeDigits(s[j..]).0 + invariant TakeDigits(s[i..]).1 == TakeDigits(s[j..]).1 + { + ghost var rest := TakeDigits(s[j + 1..]); + assert s[j..][1..] == s[j + 1..]; + assert TakeDigits(s[j..]).0 == [DigitOf(s[j])] + rest.0 && TakeDigits(s[j..]).1 == rest.1; + assert xs + ([DigitOf(s[j])] + rest.0) == (xs + [DigitOf(s[j])]) + rest.0; + xs, j := xs + [DigitOf(s[j])], j + 1; + } + assert xs + [] == xs; + } + + method TakeRhsAt(s: string, i: nat) returns (rhs: S.Rhs, j: nat) + requires i <= |s| + ensures i <= j <= |s| + ensures TakeRhs(s[i..]).0 == rhs && TakeRhs(s[i..]).1 == s[j..] + { + if i < |s| && IsCopyChar(s[i]) { + assert s[i..][1..] == s[i + 1..]; + rhs, j := S.Copy(SrcOf(s[i])), i + 1; + } else if i < |s| && IsOctalChar(s[i]) { + var ds; + ds, j := TakeDigitsAt(s, i); + rhs := S.Octal(ds); + } else { + var ps; + ps, j := TakePermsAt(s, i); + rhs := S.Perms(ps); + } + } + + method TakeActionsAt(s: string, i: nat) returns (acts: seq, j: nat) + requires i < |s| && IsOpChar(s[i]) + ensures i < j <= |s| + ensures TakeActions(s[i..]).0 == acts && TakeActions(s[i..]).1 == s[j..] + { + acts := []; + var k := i; + assert [] + TakeActions(s[i..]).0 == TakeActions(s[i..]).0; + while true + invariant i <= k < |s| && IsOpChar(s[k]) + invariant TakeActions(s[i..]).0 == acts + TakeActions(s[k..]).0 + invariant TakeActions(s[i..]).1 == TakeActions(s[k..]).1 + decreases |s| - k + { + assert s[k..][1..] == s[k + 1..]; + var rhs, m := TakeRhsAt(s, k + 1); + var a := S.Action(OpOf(s[k]), rhs); + if m < |s| && IsOpChar(s[m]) { + ghost var more := TakeActions(s[m..]); + assert TakeActions(s[k..]).0 == [a] + more.0 && TakeActions(s[k..]).1 == more.1; + assert acts + ([a] + more.0) == (acts + [a]) + more.0; + acts, k := acts + [a], m; + } else { + assert TakeActions(s[k..]).0 == [a] && TakeActions(s[k..]).1 == s[m..]; + acts, j := acts + [a], m; + return; + } + } + } + + method TakeClauseAt(s: string, i: nat) returns (r: Option<(S.Clause, nat)>) + requires i <= |s| + ensures r.None? <==> TakeClause(s[i..]).None? + ensures r.Some? ==> i < r.value.1 <= |s| + ensures r.Some? ==> TakeClause(s[i..]).value.0 == r.value.0 && TakeClause(s[i..]).value.1 == s[r.value.1..] + { + var who, k := TakeWhoAt(s, i); + if k == |s| || !IsOpChar(s[k]) { + return None; + } + var acts, m := TakeActionsAt(s, k); + var c := S.Clause(who, acts); + var ok := CheckClause(c); + r := if ok then Some((c, m)) else None; + } + + ghost function Prepend(acc: seq, r: Option>): Option> + { + match r + case None => None + case Some(cs) => Some(acc + cs) + } + + method ParseClausesFrom(s: string) returns (r: Option>) + ensures r == ParseClauses(s) + { + var acc: seq := []; + var k := 0; + assert s[0..] == s; + match ParseClauses(s) { + case None => + case Some(cs) => assert [] + cs == cs; + } + while true + invariant 0 <= k <= |s| + invariant ParseClauses(s) == Prepend(acc, ParseClauses(s[k..])) + decreases |s| - k + { + var taken := TakeClauseAt(s, k); + if taken.None? { + return None; + } + var c, m := taken.value.0, taken.value.1; + if m == |s| { + return Some(acc + [c]); + } else if s[m] == ',' { + assert s[m..][1..] == s[m + 1..]; + match ParseClauses(s[m + 1..]) { + case None => + case Some(cs) => assert acc + ([c] + cs) == (acc + [c]) + cs; + } + acc, k := acc + [c], m + 1; + } else { + return None; + } + } + } + + method CheckClause(c: S.Clause) returns (ok: bool) + ensures ok == S.ClauseWellFormed(c) + { + var n := |c.actions|; + ok := n > 0; + var t := 0; + while t < n + invariant 0 <= t <= n + invariant ok == (n > 0 && forall q :: 0 <= q < t ==> S.ActionWellFormed(c.who, c.actions[q], q == n - 1)) + { + var a := CheckAction(c.who, c.actions[t], t == n - 1); + ok := ok && a; + t := t + 1; + } + } + + method CheckAction(who: seq, a: S.Action, isLast: bool) returns (ok: bool) + ensures ok == S.ActionWellFormed(who, a, isLast) + { + match a.rhs + case Octal(ds) => + var _, within := OctalUpTo(ds); + ok := |ds| > 0 && within && |who| == 0 && isLast; + case _ => + ok := true; + } + + // The value of ds, read from the left. Like mode_compile, it stops as soon as + // the value passes 07777, so a long run of digits never builds a big number. + method OctalUpTo(ds: seq) returns (v: nat, within: bool) + ensures within == (S.OctalValue(ds) <= S.ALLM) + ensures within ==> v == S.OctalValue(ds) && v <= 4095 + { + v := 0; + var t := 0; + while t < |ds| + invariant 0 <= t <= |ds| + invariant v == S.OctalValue(ds[..t]) && v <= S.ALLM + { + assert ds[..t + 1][..t] == ds[..t]; + v := v * 8 + ds[t]; + if v > S.ALLM { + OctalPrefixAtMost(ds, t + 1); + return v, false; + } + t := t + 1; + } + assert ds[..t] == ds; + within := true; + } + + lemma OctalPrefixAtMost(ds: seq, t: nat) + requires t <= |ds| + ensures S.OctalValue(ds[..t]) <= S.OctalValue(ds) + decreases |ds| - t + { + if t < |ds| { + assert ds[..t + 1][..t] == ds[..t]; + OctalPrefixAtMost(ds, t + 1); + } else { + assert ds[..t] == ds; + } + } + + // --------------------------------------------------------------------------- + // MkfifoSpec.Meaning, computed with loops. The who and permission lists are + // folded from the right, as WhoBits and PermsBits are defined. + // --------------------------------------------------------------------------- + + method ComputeMeaning(e: S.ModeExpr, umask: bv32) returns (bits: bv32) + requires S.WellFormed(e) + ensures bits == S.Meaning(e, umask) + { + match e + case Absolute(ds) => + var v, _ := OctalUpTo(ds); + bits := v as bv32; + case Symbolic(cs) => + bits := S.MKFIFO_BASE_MODE; + var t := 0; + while t < |cs| + invariant 0 <= t <= |cs| + invariant S.ApplyClauses(S.MKFIFO_BASE_MODE, umask, cs) == S.ApplyClauses(bits, umask, cs[t..]) + { + assert cs[t..][1..] == cs[t + 1..]; + S.ClauseActionsBounded(cs[t]); + bits := ApplyClause(bits, umask, cs[t]); + t := t + 1; + } + assert cs[t..] == []; + } + + method ApplyClause(cur: bv32, umask: bv32, c: S.Clause) returns (r: bv32) + requires S.ActionsBounded(c.actions) + ensures r == S.ApplyActions(cur, umask, c.who, c.actions) + { + var who := WhoBitsOf(c.who); + r := cur; + var t := 0; + while t < |c.actions| + invariant 0 <= t <= |c.actions| + invariant S.ActionsBounded(c.actions[t..]) + invariant S.ApplyActions(cur, umask, c.who, c.actions) == S.ApplyActions(r, umask, c.who, c.actions[t..]) + { + assert c.actions[t..][1..] == c.actions[t + 1..]; + r := ApplyOne(r, umask, c.who, who, c.actions[t]); + t := t + 1; + } + assert c.actions[t..] == []; + } + + // The methods from ApplyOne to RhsOctal hide the other definitions of the + // spec module and prove one small step each: proved together, the steps do + // not finish within the solver's time limit (30 s per declaration). + method ApplyOne(cur: bv32, umask: bv32, who: seq, whoBits: bv32, a: S.Action) returns (r: bv32) + requires whoBits == S.WhoBits(who) + requires a.rhs.Octal? ==> S.OctalValue(a.rhs.digits) <= S.ALLM + ensures r == S.ApplyAction(cur, umask, who, a) + { + var scope := ScopeOf(who, whoBits, a); + var rhs := RhsBitsOf(a.rhs, cur); + r := ApplyWith(cur, umask, who, a, scope, rhs); + } + + method ScopeOf(who: seq, whoBits: bv32, a: S.Action) returns (scope: bv32) + requires whoBits == S.WhoBits(who) + ensures scope == S.ActionScope(who, a) + { + hide *; + reveal S.ActionScope; + scope := if a.rhs.Octal? then S.MODE_BITS else whoBits; + } + + // ApplyAction once the scope and the proposed bits are known, one operator + // at a time. + method ApplyWith(cur: bv32, umask: bv32, who: seq, a: S.Action, scope: bv32, rhs: bv32) + returns (r: bv32) + requires scope == S.ActionScope(who, a) + requires a.rhs.Octal? ==> S.OctalValue(a.rhs.digits) <= S.ALLM + requires rhs == S.RhsBits(a.rhs, cur) + ensures r == S.ApplyAction(cur, umask, who, a) + { + hide *; + match a.op + case OpSet => r := ApplySet(cur, umask, who, a, scope, rhs); + case OpAdd => r := ApplyAdd(cur, umask, who, a, scope, rhs); + case OpRemove => r := ApplyRemove(cur, umask, who, a, scope, rhs); + } + + method ApplySet(cur: bv32, umask: bv32, who: seq, a: S.Action, scope: bv32, rhs: bv32) + returns (r: bv32) + requires a.op.OpSet? && scope == S.ActionScope(who, a) + requires a.rhs.Octal? ==> S.OctalValue(a.rhs.digits) <= S.ALLM + requires rhs == S.RhsBits(a.rhs, cur) + ensures r == S.ApplyAction(cur, umask, who, a) + { + hide *; + reveal S.ApplyAction; + if scope != 0 { + r := (cur & !scope) | (rhs & scope); + } else { + r := rhs & !umask; + } + } + + method ApplyAdd(cur: bv32, umask: bv32, who: seq, a: S.Action, scope: bv32, rhs: bv32) + returns (r: bv32) + requires a.op.OpAdd? && scope == S.ActionScope(who, a) + requires a.rhs.Octal? ==> S.OctalValue(a.rhs.digits) <= S.ALLM + requires rhs == S.RhsBits(a.rhs, cur) + ensures r == S.ApplyAction(cur, umask, who, a) + { + hide *; + reveal S.ApplyAction; + r := cur | (rhs & (if scope != 0 then scope else !umask)); + } + + method ApplyRemove(cur: bv32, umask: bv32, who: seq, a: S.Action, scope: bv32, rhs: bv32) + returns (r: bv32) + requires a.op.OpRemove? && scope == S.ActionScope(who, a) + requires a.rhs.Octal? ==> S.OctalValue(a.rhs.digits) <= S.ALLM + requires rhs == S.RhsBits(a.rhs, cur) + ensures r == S.ApplyAction(cur, umask, who, a) + { + hide *; + reveal S.ApplyAction; + r := cur & !(rhs & (if scope != 0 then scope else !umask)); + } + + method RhsBitsOf(rhs: S.Rhs, cur: bv32) returns (r: bv32) + requires rhs.Octal? ==> S.OctalValue(rhs.digits) <= S.ALLM + ensures r == S.RhsBits(rhs, cur) + { + hide *; + match rhs + case Perms(ps) => r := RhsPerms(ps, cur); + case Copy(src) => r := RhsCopy(src, cur); + case Octal(ds) => r := RhsOctal(ds, cur); + } + + method RhsPerms(ps: seq, cur: bv32) returns (r: bv32) + ensures r == S.RhsBits(S.Perms(ps), cur) + { + hide *; + reveal S.RhsBits; + var bits := PermsBitsOf(ps); + var condX := CondXOf(ps, cur); + r := bits | (if condX then S.EXEC_BITS else 0); + } + + // Whether 'X' adds execute bits (see MkfifoSpec.RhsBits). + method CondXOf(ps: seq, cur: bv32) returns (b: bool) + ensures b == (S.PermCondX in ps && cur & S.EXEC_BITS != 0) + { + b := S.PermCondX in ps && cur & S.EXEC_BITS != 0; + } + + method RhsCopy(src: S.CopySrc, cur: bv32) returns (r: bv32) + ensures r == S.RhsBits(S.Copy(src), cur) + { + r := S.CopyBits(src, cur); + } + + method RhsOctal(ds: seq, cur: bv32) returns (r: bv32) + requires S.OctalValue(ds) <= S.ALLM + ensures r == S.RhsBits(S.Octal(ds), cur) + { + var v, _ := OctalUpTo(ds); + r := v as bv32; + } + + method WhoBitsOf(ws: seq) returns (r: bv32) + ensures r == S.WhoBits(ws) + { + r := 0; + var t := |ws|; + while t > 0 + invariant 0 <= t <= |ws| + invariant r == S.WhoBits(ws[t..]) + { + t := t - 1; + assert ws[t..][1..] == ws[t + 1..]; + r := S.WhoMask(ws[t]) | r; + } + assert ws[0..] == ws; + } + + method PermsBitsOf(ps: seq) returns (r: bv32) + ensures r == S.PermsBits(ps) + { + r := 0; + var t := |ps|; + while t > 0 + invariant 0 <= t <= |ps| + invariant r == S.PermsBits(ps[t..]) + { + t := t - 1; + assert ps[t..][1..] == ps[t + 1..]; + r := S.PermBits(ps[t]) | r; + } + assert ps[0..] == ps; } } diff --git a/bench/utils/mkfifo/mkfifo.md b/bench/utils/mkfifo/mkfifo.md index 15f0b57..836ccec 100644 --- a/bench/utils/mkfifo/mkfifo.md +++ b/bench/utils/mkfifo/mkfifo.md @@ -43,7 +43,7 @@ prevent later operands from being tried. `mkfifo --mode='ug+rw,o+r'` cases); GPL-3.0-or-later, . - Model/API revision: repository revision - `37b35bac3d4cf84cdd8ea02eb3279e8aa49307df`; shared `bench/core/IO.dfy` and + `3c704ee78884a4e764354431bb72b27771c02980`; shared `bench/core/IO.dfy` and `IOContract.dfy` are the trusted native boundary. - AllowedInput: finite sequences of Linux paths representable as UTF-8 strings, including empty operands, repeated paths, relative/absolute paths, trailing @@ -127,7 +127,10 @@ Examples with umask `022`: - Proof of MODE: Core's parser is proved to invert `Render` (`Parse(Render(e)) == Some(e)` for every well-formed `e`, and a successful parse renders back to its input). This makes the `invalid mode` decision exact - and shows that a valid string has one meaning. + and shows that a valid string has one meaning. At run time the parser and + `Meaning` are computed by loops over string indices (`ParseMode`'s + `by method` and `ComputeMeaning`), proved equal to the recursive definitions, + so the call depth does not grow with the length of MODE. - Frame: `RunCore` modifies only `fsRegion` and `stderrRegion`. Its specification also reads `nowRegion`, `umaskRegion` (the umask the native creation applies), `propsRegion` (the umask value `GetUmask` returns, used to @@ -161,13 +164,14 @@ error, and creating anything after an invalid MODE. The pull request records the tested commit, the artifact hashes, the fuzzer image and the full outputs. The results below were measured from base revision -`37b35bac3d4cf84cdd8ea02eb3279e8aa49307df` in the contributor container on +`3c704ee78884a4e764354431bb72b27771c02980` in the contributor container on Linux x86-64: Dafny 4.11.1+10dca3ba4a2909c11299176440401fc31413b53d, .NET SDK 8.0.132, Python 3.12.3, pytest 9.1.1, Ruff 0.15.12, Rust/Cargo 1.94.0, Z3 4.16.0. -- Tests: `make -C bench/utils/mkfifo test` passes 145 runtime cases against the +- Tests: `make -C bench/utils/mkfifo test` passes 153 runtime cases against the pinned GNU build, comparing stdout, stderr, exit status and the resulting - filesystem, including the two `mkfifo` cases of `tests/misc/mknod.sh`. + filesystem, including the two `mkfifo` cases of `tests/misc/mknod.sh` and + MODE strings of 100,000 characters. - Fuzzing: `python3 tools/coreutils_fuzzer/run.py fuzz mkfifo --seeds 1,7,19 --iterations 1000` completed 1000 matches per seed with no mismatch, timeout or other error; option coverage was 4/4 singles and 6/6 pairs for each seed. From 62c4c9ffef2464255c6234e76005615745ebbdde Mon Sep 17 00:00:00 2001 From: jkkms Date: Fri, 30 Oct 2026 03:47:12 +0000 Subject: [PATCH 8/8] [Tests] add long MODE parity cases Problem: Review of #42 asked for the long MODE cases as tests. Approach: Eight GNU parity cases with MODE strings of about 100,000 characters, below Linux's 128 KiB limit for one argument: the two cases from the review, long runs of permission letters, actions and clauses, a digit run after an operator, and two digit runs above 07777 that must be rejected. Boundaries: bench/utils/mkfifo/Tests.py only. Validation: make -C bench/utils/mkfifo test -> 153 passed. Limitations: none. Co-Authored-By: Claude Opus 5.5 --- bench/utils/mkfifo/Tests.py | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/bench/utils/mkfifo/Tests.py b/bench/utils/mkfifo/Tests.py index 5ea866c..03017e9 100644 --- a/bench/utils/mkfifo/Tests.py +++ b/bench/utils/mkfifo/Tests.py @@ -199,6 +199,42 @@ def test_invalid_mode(executables: tuple[Path, Path], tmp_path: Path, mode: str) assert set(entries) == {"."} +# Long MODE strings: one argument stays below Linux's 128 KiB limit. +LONG_MODE = 100_000 + + +@pytest.mark.parametrize( + "mode", + [ + pytest.param("0" * LONG_MODE + "600", id="leading-zeros"), + pytest.param("u" * LONG_MODE + "+r", id="who-letters"), + pytest.param("a+" + "r" * LONG_MODE, id="permission-letters"), + pytest.param("+r" * (LONG_MODE // 2), id="actions"), + pytest.param(",".join(["u+r"] * (LONG_MODE // 4)), id="clauses"), + pytest.param("+" + "0" * LONG_MODE + "644", id="octal-after-operator"), + ], +) +def test_long_mode(executables: tuple[Path, Path], tmp_path: Path, mode: str) -> None: + # upstream: none - Checks that a long MODE is parsed and applied without deep recursion. + result, entries = assert_parity(executables, ["-m", mode, "p"], tmp_path) + assert result == (b"", b"", 0) + assert stat.S_ISFIFO(entries["p"].kind) + + +@pytest.mark.parametrize( + "mode", + [ + pytest.param("7" * LONG_MODE, id="digits"), + pytest.param("0" * LONG_MODE + "10000", id="leading-zeros"), + ], +) +def test_long_invalid_mode(executables: tuple[Path, Path], tmp_path: Path, mode: str) -> None: + # upstream: none - Checks mode_compile's 07777 limit on a long digit run. + result, entries = assert_parity(executables, ["-m", mode, "p"], tmp_path) + assert result == (b"", INVALID_MODE, 1) + assert set(entries) == {"."} + + # A MODE whose result has set-ID or sticky bits is rejected before any creation. @pytest.mark.parametrize("mode", ["u+s", "+s", "+t", "4644", "7777", "g+s,o+t"]) def test_special_bits(executables: tuple[Path, Path], tmp_path: Path, mode: str) -> None: