[Benchmark] add link

bench/utils/link/Link.dfy

@@ -0,0 +1,74 @@
+include "../../core/BenchmarkItem.dfy"
+include "../../core/Utf8.dfy"
+include "LinkSpec.dfy"
+include "LinkCore.dfy"
+include "LinkProof.dfy"
+
+module Link {
+  import BenchIO
+  import BenchWorld
+  import BenchItem
+  import CliTypes
+  import Utf8 = Utf8Semantics
+  import S = LinkSchema
+  import Core = LinkCore
+  import Spec = LinkSpec
+  import Proof = LinkProof
+  import opened CliExtern
+
+  class LinkBenchmarkItem extends BenchItem.BenchmarkItemTwostate<S.LinkCmdRaw> {
+    constructor() {}
+
+    method Name() returns (name: string) {
+      name := "link";
+    }
+
+    method Schema() returns (schema: CliTypes.CliSchema) {
+      schema := S.Schema();
+    }
+
+    method ParseConfig() returns (cfg: CliTypes.ParseConfig) {
+      cfg := S.ParserConfig();
+    }
+
+    method Decode(parsed: CliTypes.ParsedArgs) returns (raw: S.LinkCmdRaw) {
+      raw := S.Decode(parsed);
+    }
+
+    method FormatParseError(err: CliTypes.ParseError) returns (msg: BenchWorld.Bytes) {
+      msg := Spec.ParseErrorText(err);
+    }
+
+    method PlanParseFailure(
+      e: CliTypes.ParseError,
+      argv: seq<string>
+    ) returns (plan: CliTypes.CliPlan<S.LinkCmdRaw>)
+      decreases *
+    {
+      if 0 < e.tokenIndex && e.tokenIndex < |argv| {
+        var s := S.Schema();
+        var cfg := S.ParserConfig();
+        var result := Cli.Parse(argv[..e.tokenIndex], s, cfg);
+        match result {
+          case ParseSuccess(parsed) =>
+            var raw := S.Decode(parsed);
+            if raw.mode == S.ModeHelp || raw.mode == S.ModeVersion {
+              plan := CliTypes.CliRun(raw);
+              return;
+            }
+          case ParseFailure(_) =>
+        }
+      }
+      var msg := Spec.ParseErrorText(e);
+      plan := CliTypes.CliEarlyExit(1, [], msg);
+    }
+
+    method RunCore(raw: S.LinkCmdRaw, io: BenchIO.IO) returns (exit: int)
+      modifies io.fsRegion, io.stdoutRegion, io.stderrRegion
+      ensures Spec.Spec(raw, io, exit)
+    {
+      exit := Core.RunCore(raw, io);
+      Proof.CoreSummaryImpliesSpec(raw, io, exit);
+    }
+  }
+}

bench/utils/link/LinkCli.dfy

@@ -0,0 +1,20 @@
+include "Link.dfy"
+
+module LinkCli {
+  import BenchIO
+  import BenchItem
+  import Link
+
+  method {:main} Main(args: seq<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 := ["link"] + effectiveArgs;
+    var io := BenchIO.Process();
+    var item := new Link.LinkBenchmarkItem();
+    var exit := BenchItem.RunMain(item, argv, io);
+    BenchIO.Exit(exit);
+  }
+}

bench/utils/link/LinkCore.dfy

@@ -0,0 +1,111 @@
+include "../../core/IO.dfy"
+include "LinkSchema.dfy"
+include "LinkSpec.dfy"
+
+module LinkCore {
+  import BenchIO
+  import BenchWorld
+  import Schema = LinkSchema
+  import Spec = LinkSpec
+  import C = IOContract
+  import Utf8 = Utf8Semantics
+
+  twostate predicate CoreSummary(raw: Schema.LinkCmdRaw, io: BenchIO.IO, exit: int)
+    reads io.Footprint()
+  {
+    if raw.mode == Schema.ModeHelp then
+      io.fs() == old(io.fs()) &&
+      io.stdout() == old(io.stdout()) + Spec.HelpTextSpec() &&
+      io.stderr() == old(io.stderr()) &&
+      exit == 0
+    else if raw.mode == Schema.ModeVersion then
+      io.fs() == old(io.fs()) &&
+      io.stdout() == old(io.stdout()) + Spec.VersionTextSpec() &&
+      io.stderr() == old(io.stderr()) &&
+      exit == 0
+    else if raw.mode != Schema.ModeRun then
+      match raw.mode
+      case ModeExtraOperand(operand) =>
+        io.fs() == old(io.fs()) &&
+        io.stdout() == old(io.stdout()) &&
+        io.stderr() == old(io.stderr()) +
+          Spec.ExtraOperandText(C.QuoteArgumentResult(Utf8.Encode(operand))) &&
+        exit == 1
+      case _ => false
+    else if |raw.operands| == 0 then
+      io.fs() == old(io.fs()) &&
+      io.stdout() == old(io.stdout()) &&
+      io.stderr() == old(io.stderr()) + Spec.MissingOperandText() &&
+      exit == 1
+    else if |raw.operands| == 1 then
+      io.fs() == old(io.fs()) &&
+      io.stdout() == old(io.stdout()) &&
+      io.stderr() == old(io.stderr()) +
+        Spec.MissingOperandAfterText(
+          C.QuoteArgumentResult(Utf8.Encode(raw.operands[0]))
+        ) &&
+      exit == 1
+    else
+      exists ok: bool, err: int ::
+        Spec.LinkResult(io, raw.operands[0], raw.operands[1], ok, err) &&
+        io.stdout() == old(io.stdout()) &&
+        (if ok then
+          io.stderr() == old(io.stderr()) && exit == 0
+        else
+          io.stderr() == old(io.stderr()) +
+            Spec.CannotCreateLinkText(
+              C.QuoteafPathResult(raw.operands[1]),
+              C.QuoteafPathResult(raw.operands[0]),
+              C.CLocaleErrnoTextResult(err)
+            ) &&
+          exit == 1)
+  }
+
+  method RunCore(raw: Schema.LinkCmdRaw, io: BenchIO.IO) returns (exit: int)
+    modifies io.fsRegion, io.stdoutRegion, io.stderrRegion
+    ensures CoreSummary(raw, io, exit)
+  {
+    if raw.mode == Schema.ModeHelp {
+      var _, _ := io.WriteStdout(Spec.HelpTextSpec(), BenchWorld.ThrowOnError);
+      exit := 0;
+    } else if raw.mode == Schema.ModeVersion {
+      var _, _ := io.WriteStdout(Spec.VersionTextSpec(), BenchWorld.ThrowOnError);
+      exit := 0;
+    } else if raw.mode.ModeExtraOperand? {
+      var quotedOperand := io.QuoteArgument(Utf8.Encode(raw.mode.operand));
+      var _, _ := io.WriteStderr(Spec.ExtraOperandText(quotedOperand), BenchWorld.ThrowOnError);
+      exit := 1;
+    } else if |raw.operands| == 0 {
+      var _, _ := io.WriteStderr(Spec.MissingOperandText(), BenchWorld.ThrowOnError);
+      exit := 1;
+    } else if |raw.operands| == 1 {
+      var quotedSource := io.QuoteArgument(Utf8.Encode(raw.operands[0]));
+      var _, _ := io.WriteStderr(
+        Spec.MissingOperandAfterText(quotedSource),
+        BenchWorld.ThrowOnError
+      );
+      exit := 1;
+    } else {
+      var source := raw.operands[0];
+      var target := raw.operands[1];
+      var ok, err := io.CreateHardLink(source, target);
+      assert Spec.LinkResult(io, source, target, ok, err);
+
+      if ok {
+        exit := 0;
+      } else {
+        var reason := io.GetCLocaleErrnoText(err);
+        var quotedTarget := io.QuoteafPath(target);
+        var quotedSource := io.QuoteafPath(source);
+        var _, _ := io.WriteStderr(
+          Spec.CannotCreateLinkText(quotedTarget, quotedSource, reason),
+          BenchWorld.ThrowOnError
+        );
+        exit := 1;
+
+        assert C.GetCLocaleErrnoTextSpec(err, reason);
+        assert Spec.LinkResult(io, source, target, ok, err);
+      }
+    }
+  }
+}

bench/utils/link/LinkProof.dfy

@@ -0,0 +1,17 @@
+include "LinkSpec.dfy"
+include "LinkCore.dfy"
+
+module LinkProof {
+  import BenchIO
+  import Schema = LinkSchema
+  import Core = LinkCore
+  import Spec = LinkSpec
+
+  twostate lemma CoreSummaryImpliesSpec(
+    raw: Schema.LinkCmdRaw, io: BenchIO.IO, exit: int)
+    requires Core.CoreSummary(raw, io, exit)
+    ensures Spec.Spec(raw, io, exit)
+  {
+
+  }
+}

bench/utils/link/LinkSchema.dfy

@@ -0,0 +1,64 @@
+include "../../core/CliTypes.dfy"
+
+module LinkSchema {
+  import CliTypes
+
+  datatype LinkMode = ModeRun | ModeHelp | ModeVersion | ModeExtraOperand(operand: string)
+
+  datatype LinkCmdRaw = LinkCmdRaw(
+    mode: LinkMode,
+    operands: seq<string>
+  )
+
+  method Schema() returns (schema: CliTypes.CliSchema)
+  {
+    schema := CliTypes.CliSchema([
+      CliTypes.OptionDecl("link.help", [], ["help"], CliTypes.NoArg),
+      CliTypes.OptionDecl("link.version", [], ["version"], CliTypes.NoArg)
+    ], true);
+  }
+
+  method ParserConfig() returns (cfg: CliTypes.ParseConfig)
+  {
+    cfg := CliTypes.ParseConfig(CliTypes.GNU_Permute, false, true, true);
+  }
+
+  method Decode(parsed: CliTypes.ParsedArgs) returns (raw: LinkCmdRaw)
+  {
+    var seenHelp := false;
+    var seenVersion := false;
+    var helpTokenIndex := -1;
+    var versionTokenIndex := -1;
+    var i := 0;
+    while i < |parsed.options|
+      decreases |parsed.options| - i
+    {
+      var option := parsed.options[i];
+
+      if option.key == "link.help" {
+        seenHelp := true;
+        if helpTokenIndex == -1 || option.tokenIndex < helpTokenIndex {
+          helpTokenIndex := option.tokenIndex;
+        }
+      }
+      if option.key == "link.version" {
+        seenVersion := true;
+        if versionTokenIndex == -1 || option.tokenIndex < versionTokenIndex {
+          versionTokenIndex := option.tokenIndex;
+        }
+      }
+
+      i := i + 1;
+    }
+    var mode := if seenHelp && (!seenVersion || helpTokenIndex <= versionTokenIndex) then
+        ModeHelp
+      else if seenVersion then
+        ModeVersion
+      else if |parsed.positionals| > 2 then
+        ModeExtraOperand(parsed.positionals[2])
+      else
+        ModeRun;
+
+    raw := LinkCmdRaw(mode, parsed.positionals);
+  }
+}