diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index 71d9bbed31a..189be194719 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/Source/DafnyCore/DafnyOptions.cs @@ -59,12 +59,12 @@ datatype with a single non-ghost constructor that has a single datatype Record = Record(x: int) is transformed into just 'int' in the target code.".TrimStart(), defaultValue: true); - RegisterLegacyUi(CommonOptionBag.Output, ParseString, "Compilation options", "out"); + RegisterLegacyUi(CommonOptionBag.Output, ParseFileInfo, "Compilation options", "out"); RegisterLegacyUi(CommonOptionBag.UnicodeCharacters, ParseBoolean, "Language feature selection", "unicodeChar", @" 0 (default) - The char type represents any UTF-16 code unit. 1 - The char type represents any Unicode scalar value.".TrimStart()); RegisterLegacyUi(CommonOptionBag.Plugin, ParseStringElement, "Plugins", defaultValue: new List()); - RegisterLegacyUi(CommonOptionBag.Prelude, ParseString, "Input configuration", "dprelude"); + RegisterLegacyUi(CommonOptionBag.Prelude, ParseFileInfo, "Input configuration", "dprelude"); RegisterLegacyUi(CommonOptionBag.Libraries, ParseStringElement, "Compilation options", defaultValue: new List()); RegisterLegacyUi(DeveloperOptionBag.ResolvedPrint, ParseString, "Overall reporting and printing", "rprint"); @@ -132,6 +132,12 @@ public static void RegisterLegacyBinding(Option option, Action bind(options, (T)o); } + public static void ParseFileInfo(Option option, Bpl.CommandLineParseState ps, DafnyOptions options) { + if (ps.ConfirmArgumentCount(1)) { + options.Set(option, new FileInfo(ps.args[ps.i])); + } + } + public static void ParseString(Option option, Bpl.CommandLineParseState ps, DafnyOptions options) { if (ps.ConfirmArgumentCount(1)) { options.Set(option, ps.args[ps.i]); diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index d359b31c82c..17368b5ecbd 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/Source/DafnyCore/Options/CommonOptionBag.cs @@ -1,6 +1,6 @@ using System.Collections.Generic; using System.CommandLine; -using System.Diagnostics.Tracing; +using System.IO; using System.Linq; namespace Microsoft.Dafny; @@ -45,7 +45,7 @@ datatype with a single non-ghost constructor that has a single This option is useful in a diamond dependency situation, to prevent code from the bottom dependency from being generated more than once.".TrimStart()); - public static readonly Option Output = new(new[] { "--output", "-o" }, + public static readonly Option Output = new(new[] { "--output", "-o" }, "Specify the filename and location for the generated target language files.") { ArgumentHelpName = "file" }; @@ -62,7 +62,7 @@ can also extend Microsoft.Dafny.Plugins.PluginConfiguration to ArgumentHelpName = "path-to-one-assembly[,argument]*" }; - public static readonly Option Prelude = new("--prelude", "Choose the Dafny prelude file.") { + public static readonly Option Prelude = new("--prelude", "Choose the Dafny prelude file.") { ArgumentHelpName = "file" }; @@ -111,7 +111,7 @@ Note that quantifier variable domains (<- ) are available in both syntax false - The char type represents any UTF-16 code unit. true - The char type represents any Unicode scalar value.".TrimStart()); - public static readonly Option SolverPath = new("--solver-path", + public static readonly Option SolverPath = new("--solver-path", "Can be used to specify a custom SMT solver to use for verifying Dafny proofs."); public static readonly Option VerifyIncludedFiles = new("--verify-included-files", "Verify code in included files."); @@ -137,8 +137,8 @@ public enum TestAssumptionsMode { static CommonOptionBag() { DafnyOptions.RegisterLegacyBinding(SolverPath, (options, value) => { - if (!string.IsNullOrEmpty(value)) { - options.ProverOptions.Add($"PROVER_PATH={value}"); + if (value != null) { + options.ProverOptions.Add($"PROVER_PATH={value?.FullName}"); } }); @@ -166,13 +166,13 @@ static CommonOptionBag() { DafnyOptions.RegisterLegacyBinding(Plugin, (options, value) => { options.AdditionalPluginArguments = value; }); DafnyOptions.RegisterLegacyBinding(Prelude, (options, value) => { - options.DafnyPrelude = value; + options.DafnyPrelude = value?.FullName; options.ExpandFilename(options.DafnyPrelude, x => options.DafnyPrelude = x, options.LogPrefix, options.FileTimestamp); }); DafnyOptions.RegisterLegacyBinding(Libraries, (options, value) => { options.LibraryFiles = value.ToHashSet(); }); - DafnyOptions.RegisterLegacyBinding(Output, (options, value) => { options.DafnyPrintCompiledFile = value; }); + DafnyOptions.RegisterLegacyBinding(Output, (options, value) => { options.DafnyPrintCompiledFile = value?.FullName; }); DafnyOptions.RegisterLegacyBinding(CompileVerbose, (o, v) => o.CompileVerbose = v); DafnyOptions.RegisterLegacyBinding(DisableNonLinearArithmetic, (o, v) => o.DisableNLarith = v); diff --git a/Source/DafnyCore/Options/DeveloperOptionBag.cs b/Source/DafnyCore/Options/DeveloperOptionBag.cs index 277d261aef9..d828c610df2 100644 --- a/Source/DafnyCore/Options/DeveloperOptionBag.cs +++ b/Source/DafnyCore/Options/DeveloperOptionBag.cs @@ -1,5 +1,5 @@ using System.CommandLine; -using Microsoft.Dafny.Plugins; +using System.IO; namespace Microsoft.Dafny; diff --git a/Source/DafnyCore/Options/ICommandSpec.cs b/Source/DafnyCore/Options/ICommandSpec.cs index 62f2fa0587c..fc4808172fe 100644 --- a/Source/DafnyCore/Options/ICommandSpec.cs +++ b/Source/DafnyCore/Options/ICommandSpec.cs @@ -11,18 +11,8 @@ public interface ICommandSpec { public static Argument FileArgument { get; } - private static ValidateSymbolResult ValidateFileArgument() { - return r => { - var value = r.Tokens[0].Value; - if (value.StartsWith("--")) { - r.ErrorMessage = $"{value} is not a valid argument"; - } - }; - } - static ICommandSpec() { FilesArgument = new Argument>("file", "input files"); - FilesArgument.AddValidator(ValidateFileArgument()); } public static Argument> FilesArgument { get; } diff --git a/Test/dafny4/- b/Test/dafny4/- new file mode 100644 index 00000000000..c339fdff1f5 --- /dev/null +++ b/Test/dafny4/- @@ -0,0 +1,180 @@ +// git-issue228.dfy + +/* +module _System { + /* CALL GRAPH for module _System: + * SCC at height 1: + * RotateRight + * SCC at height 1: + * RotateLeft + * SCC at height 0: + * nat + */ + type string(==,0) = seq + + type {:axiom} nat(==,0) = x: int + | 0 <= x + + trait {:compile false} object { } + /*-- non-null type + type {:axiom} object(==) = c: object? | c != null /*special witness*/ + */ + + class {:compile false} array { + var Length: int // immutable + } + /*-- non-null type + type {:axiom} array(==) = c: array? | c != null /*special witness*/ + */ + + class {:compile false} /*_#Func1*/ -T0 ~> +R { + function requires(x0: T0): bool + reads reads(x0) + + function reads(x0: T0): set + reads reads(x0) + } + + type {:compile false} /*_#PartialFunc1*/ -T0 --> +R = f: T0 ~> R + | forall x0: T0 :: f.reads(x0) == {} + /*special witness*/ + + type {:compile false} /*_#TotalFunc1*/ -T0 -> +R = f: T0 --> R + | forall x0: T0 :: f.requires(x0) + /*special witness*/ + + class {:compile false} /*_#Func0*/ () ~> +R { + function requires(): bool + reads reads() + + function reads(): set + reads reads() + } + + type {:compile false} /*_#PartialFunc0*/ () --> +R = f: () ~> R + | f.reads() == {} + /*special witness*/ + + type {:compile false} /*_#TotalFunc0*/ () -> +R = f: () --> R + | f.requires() + /*special witness*/ + + datatype {:compile false} /*_tuple#2*/ (+T0, +T1) = _#Make2(0: T0, 1: T1) + + type bool { } + + type int { } + + type real { + var Floor: int // immutable + } + + type ORDINAL { + var IsLimit: bool // immutable + var IsSucc: bool // immutable + var Offset: int // immutable + var IsNat: bool // immutable + } + + type _bv { + function method RotateLeft(w: nat): selftype + + function method RotateRight(w: nat): selftype + } + + type map { + var Keys: set // immutable + var Values: set // immutable + var Items: set<(T, U)> // immutable + } + + type imap { + var Keys: iset // immutable + var Values: iset // immutable + var Items: iset<(T, U)> // immutable + } + + datatype {:compile false} /*_tuple#0*/ () = _#Make0 +} +// bitvector types in use: bv0 bv19 +*/ + +/* CALL GRAPH for module _module: + * SCC at height 0: + * Sets + * SCC at height 0: + * Sequences + * SCC at height 1: + * SubsetTypes + * SCC at height 0: + * Subset_Byte + * SCC at height 0: + * Subset_NegIsOdd + * SCC at height 1: + * ConstrainedIntermediateExpressions + * SCC at height 0: + * Byte + * SCC at height 0: + * NegIsOdd + * SCC at height 1: + * Numerics + * SCC at height 0: + * nat + */ +newtype NegIsOdd = x: int + | x < 0 ==> x % 2 == 1 + witness 1 + +newtype Byte = x: int + | 0 <= x < 256 + +type Subset_NegIsOdd = x: int + | x < 0 ==> x % 2 == 1 + witness 1 + +type Subset_Byte = x: int + | 0 <= x < 256 + +lemma Sequences(s: seq, t: seq, u: seq) + ensures s + t + u == s + (t + u) + decreases s, t, u +{ +} + +lemma Sets(s: set, t: set, u: set) + ensures s + t + u == s + (t + u) + ensures s * t * u == s * (t * u) + decreases s, t, u +{ +} + +method Numerics() + returns (x: int, n: nat, r: real, o: ORDINAL, b: bv0, c: bv19) +{ + x := x + x + x + x; + n := n + n + n + n; + r := r + r + r + r; + o := o + o + o + o; + b := b + b + b + b; + c := c + c + c + c; +} + +method ConstrainedIntermediateExpressions(a: NegIsOdd, b: NegIsOdd, x: Byte, z: Byte) + requires 0 <= b && z == 0 + decreases a, b, x, z +{ + var c0: NegIsOdd := a + (b + b); + var c1: NegIsOdd := a + b + b; + var d0: Byte := x * (x * z); + var d1: Byte := x * x * z; +} + +method SubsetTypes(a: Subset_NegIsOdd, b: Subset_NegIsOdd, x: Subset_Byte, z: Subset_Byte) + requires 0 <= b && z == 0 + decreases a, b, x, z +{ + var c0: int := a + b + b; + var c1: int := a + b + b; + var d0: int := x * x * z; + var d1: int := x * x * z; +}