diff --git a/bench/utils/mkfifo/CliSupport.dfy b/bench/utils/mkfifo/CliSupport.dfy new file mode 100644 index 00000000..7cba65e7 --- /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 00000000..d26aad6e --- /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 00000000..d70efb40 --- /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 00000000..2988a767 --- /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 00000000..c9793552 --- /dev/null +++ b/bench/utils/mkfifo/MkfifoCore.dfy @@ -0,0 +1,174 @@ +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 := P.ComputeMeaning(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); + assert io.stdout() == old(io.stdout()); + 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 00000000..f3dd3ebf --- /dev/null +++ b/bench/utils/mkfifo/MkfifoModeCore.dfy @@ -0,0 +1,611 @@ +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 + + 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)) + } 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/MkfifoModeProof.dfy b/bench/utils/mkfifo/MkfifoModeProof.dfy new file mode 100644 index 00000000..8b298028 --- /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 00000000..4d56f64a --- /dev/null +++ b/bench/utils/mkfifo/MkfifoProof.dfy @@ -0,0 +1,348 @@ +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) + requires io.stdout() == old(io.stdout()) + 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 00000000..75aa2828 --- /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 00000000..87454ae8 --- /dev/null +++ b/bench/utils/mkfifo/MkfifoSpec.dfy @@ -0,0 +1,648 @@ +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 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() + } + + // --------------------------------------------------------------------------- + // 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) + } + + // 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.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) && + 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 00000000..03017e9d --- /dev/null +++ b/bench/utils/mkfifo/Tests.py @@ -0,0 +1,482 @@ +"""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, +) + +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 each benchmark target once, independently of development tests.""" + 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 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], + 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: + # 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) == {"."} + + +# 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: + # 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 + 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 + + +# 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 specification well-formedness, helpers and the entry obligation separately. +@pytest.mark.dafny_verify +@pytest.mark.parametrize( + "filename", + [ + "MkfifoSpec.dfy", + "MkfifoModeCore.dfy", + "MkfifoModeProof.dfy", + "MkfifoCore.dfy", + "MkfifoProof.dfy", + "Mkfifo.dfy", + ], +) +def test_verify_module(filename: str) -> None: + # upstream: none - Checks proof obligations rather than 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 00000000..8d6e2b44 --- /dev/null +++ b/bench/utils/mkfifo/benchmark.yaml @@ -0,0 +1,11 @@ +schema_version: benchmark.definition.v2 +task_id: mkfifo +kind: coreutils +source: + 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/dfyconfig.toml b/bench/utils/mkfifo/dfyconfig.toml new file mode 100644 index 00000000..28f621dc --- /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 00000000..836ccecc --- /dev/null +++ b/bench/utils/mkfifo/mkfifo.md @@ -0,0 +1,189 @@ +# 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 +`-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 + `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 + 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. 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 + evaluate MODE), `trustedFilesystemRegion`, `trustedNativeFailuresRegion` and + `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. +- 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 + +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 +`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 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` 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. +- 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`. + +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. diff --git a/tools/coreutils_fuzzer/src/fuzz/comparison/fs_snapshot.rs b/tools/coreutils_fuzzer/src/fuzz/comparison/fs_snapshot.rs index e3fd04f8..856a44dd 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 00000000..3c3fb015 --- /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 80731659..7acd1c00 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 bc29e746..f17d78d9 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 584e7ebd..32bde170 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", ]) ); }