[Benchmark] add mkfifo

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)"

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<S.MkfifoCmdRaw> {
+    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<S.MkfifoCmdRaw>)
+    {
+      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<string>)
+      returns (plan: CliTypes.CliPlan<S.MkfifoCmdRaw>)
+    {
+      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);
+    }
+  }
+}

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<string>)
+    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);
+  }
+}

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<string>, 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<Spec.OperandOutcome> := [];
+    ghost var cuts: seq<nat> := [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);
+  }
+}