diff options
Diffstat (limited to 'Source/DafnyDriver')
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 796 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.csproj | 182 | ||||
| -rw-r--r-- | Source/DafnyDriver/app.config | 3 |
3 files changed, 981 insertions, 0 deletions
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs new file mode 100644 index 00000000..80f78d16 --- /dev/null +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -0,0 +1,796 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+//---------------------------------------------------------------------------------------------
+// DafnyDriver
+// - main program for taking a Dafny program and verifying it
+//---------------------------------------------------------------------------------------------
+
+namespace Microsoft.Dafny
+{
+ using System;
+ using System.IO;
+ using System.Collections;
+ using System.Collections.Generic;
+ using System.Diagnostics.Contracts;
+ using PureCollections;
+ using Microsoft.Boogie;
+ using Bpl = Microsoft.Boogie;
+ using Microsoft.Boogie.AbstractInterpretation;
+ using System.Diagnostics;
+ using VC;
+ using System.CodeDom.Compiler;
+
+ public class DafnyDriver
+ {
+ // ------------------------------------------------------------------------
+ // Main
+
+ public static int Main(string[] args)
+ {
+ Contract.Requires(cce.NonNullElements(args));
+
+ DafnyOptions.Install(new DafnyOptions());
+
+ //assert forall{int i in (0:args.Length); args[i] != null};
+ ExitValue exitValue = ExitValue.VERIFIED;
+ CommandLineOptions.Clo.RunningBoogieFromCommandLine = true;
+ if (!CommandLineOptions.Clo.Parse(args)) {
+ exitValue = ExitValue.PREPROCESSING_ERROR;
+ goto END;
+ }
+ if (CommandLineOptions.Clo.Files.Count == 0)
+ {
+ ErrorWriteLine("*** Error: No input files were specified.");
+ exitValue = ExitValue.PREPROCESSING_ERROR;
+ goto END;
+ }
+ if (CommandLineOptions.Clo.XmlSink != null) {
+ string errMsg = CommandLineOptions.Clo.XmlSink.Open();
+ if (errMsg != null) {
+ ErrorWriteLine("*** Error: " + errMsg);
+ exitValue = ExitValue.PREPROCESSING_ERROR;
+ goto END;
+ }
+ }
+ if (!CommandLineOptions.Clo.DontShowLogo)
+ {
+ Console.WriteLine(CommandLineOptions.Clo.Version);
+ }
+ if (CommandLineOptions.Clo.ShowEnv == CommandLineOptions.ShowEnvironment.Always)
+ {
+ Console.WriteLine("---Command arguments");
+ foreach (string arg in args)
+ {Contract.Assert(arg != null);
+ Console.WriteLine(arg);
+ }
+ Console.WriteLine("--------------------");
+ }
+
+ foreach (string file in CommandLineOptions.Clo.Files)
+ {Contract.Assert(file != null);
+ string extension = Path.GetExtension(file);
+ if (extension != null) { extension = extension.ToLower(); }
+ if (extension != ".dfy")
+ {
+ ErrorWriteLine("*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be Dafny programs (.dfy).", file,
+ extension == null ? "" : extension);
+ exitValue = ExitValue.PREPROCESSING_ERROR;
+ goto END;
+ }
+ }
+ exitValue = ProcessFiles(CommandLineOptions.Clo.Files);
+
+ END:
+ if (CommandLineOptions.Clo.XmlSink != null) {
+ CommandLineOptions.Clo.XmlSink.Close();
+ }
+ if (CommandLineOptions.Clo.Wait)
+ {
+ Console.WriteLine("Press Enter to exit.");
+ Console.ReadLine();
+ }
+ return (int)exitValue;
+ }
+
+ public static void ErrorWriteLine(string s) {Contract.Requires(s != null);
+ if (!s.Contains("Error: ") && !s.Contains("Error BP")) {
+ Console.WriteLine(s);
+ return;
+ }
+
+ // split the string up into its first line and the remaining lines
+ string remaining = null;
+ int i = s.IndexOf('\r');
+ if (0 <= i) {
+ remaining = s.Substring(i+1);
+ if (remaining.StartsWith("\n")) {
+ remaining = remaining.Substring(1);
+ }
+ s = s.Substring(0, i);
+ }
+
+ ConsoleColor col = Console.ForegroundColor;
+ Console.ForegroundColor = ConsoleColor.Red;
+ Console.WriteLine(s);
+ Console.ForegroundColor = col;
+
+ if (remaining != null) {
+ Console.WriteLine(remaining);
+ }
+ }
+
+ public static void ErrorWriteLine(string format, params object[] args) {
+ Contract.Requires(format != null);
+ string s = string.Format(format, args);
+ ErrorWriteLine(s);
+ }
+
+ public static void AdvisoryWriteLine(string format, params object[] args) {
+ Contract.Requires(format != null);
+ ConsoleColor col = Console.ForegroundColor;
+ Console.ForegroundColor = ConsoleColor.Yellow;
+ Console.WriteLine(format, args);
+ Console.ForegroundColor = col;
+ }
+
+ enum FileType { Unknown, Cil, Bpl, Dafny };
+
+ static ExitValue ProcessFiles (List<string/*!*/>/*!*/ fileNames)
+ {
+ Contract.Requires(cce.NonNullElements(fileNames));
+ ExitValue exitValue = ExitValue.VERIFIED;
+ using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count-1])) {
+ Dafny.Program dafnyProgram;
+ string programName = fileNames.Count == 1 ? fileNames[0] : "the program";
+ string err = Dafny.Main.ParseCheck(fileNames, programName, out dafnyProgram);
+ if (err != null) {
+ exitValue = ExitValue.DAFNY_ERROR;
+ ErrorWriteLine(err);
+ } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck) {
+ Dafny.Translator translator = new Dafny.Translator();
+ Bpl.Program boogieProgram = translator.Translate(dafnyProgram);
+ if (CommandLineOptions.Clo.PrintFile != null)
+ {
+ PrintBplFile(CommandLineOptions.Clo.PrintFile, boogieProgram, false);
+ }
+
+ string bplFilename;
+ if (CommandLineOptions.Clo.PrintFile != null) {
+ bplFilename = CommandLineOptions.Clo.PrintFile;
+ } else {
+ string baseName = cce.NonNull(Path.GetFileName(fileNames[fileNames.Count-1]));
+ baseName = cce.NonNull(Path.ChangeExtension(baseName, "bpl"));
+ bplFilename = Path.Combine(Path.GetTempPath(), baseName);
+ }
+
+ int errorCount, verified, inconclusives, timeOuts, outOfMemories;
+ PipelineOutcome oc = BoogiePipelineWithRerun(boogieProgram, bplFilename, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);
+ bool allOk = errorCount == 0 && inconclusives == 0 && timeOuts == 0 && outOfMemories == 0;
+ switch (oc) {
+ case PipelineOutcome.VerificationCompleted:
+ WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
+ if ((DafnyOptions.O.Compile && allOk && CommandLineOptions.Clo.ProcsToCheck == null) || DafnyOptions.O.ForceCompile)
+ CompileDafnyProgram(dafnyProgram, fileNames[0]);
+ break;
+ case PipelineOutcome.Done:
+ WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
+ if (DafnyOptions.O.ForceCompile)
+ CompileDafnyProgram(dafnyProgram, fileNames[0]);
+ break;
+ default:
+ // error has already been reported to user
+ break;
+ }
+ exitValue = allOk ? ExitValue.VERIFIED : ExitValue.NOT_VERIFIED;
+ }
+ }
+ return exitValue;
+ }
+
+ private static void CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyProgramName)
+ {
+ // Compile the Dafny program into a string that contains the C# program
+ StringWriter sw = new StringWriter();
+ Dafny.Compiler compiler = new Dafny.Compiler(sw);
+ compiler.Compile(dafnyProgram);
+ var csharpProgram = sw.ToString();
+ bool completeProgram = compiler.ErrorCount == 0;
+
+ // blurt out the code to a file
+ if (DafnyOptions.O.SpillTargetCode) {
+ string targetFilename = Path.ChangeExtension(dafnyProgramName, "cs");
+ using (TextWriter target = new StreamWriter(new FileStream(targetFilename, System.IO.FileMode.Create))) {
+ target.Write(csharpProgram);
+ if (completeProgram) {
+ Console.WriteLine("Compiled program written to {0}", targetFilename);
+ } else {
+ Console.WriteLine("File {0} contains the partially compiled program", targetFilename);
+ }
+ }
+ }
+
+ // compile the program into an assembly
+ if (!completeProgram) {
+ // don't compile
+ } else if (!CodeDomProvider.IsDefinedLanguage("CSharp")) {
+ Console.WriteLine("Error: cannot compile, because there is no provider configured for input language CSharp");
+ } else {
+ var provider = CodeDomProvider.CreateProvider("CSharp");
+ var cp = new System.CodeDom.Compiler.CompilerParameters();
+ cp.GenerateExecutable = true;
+ if (compiler.HasMain(dafnyProgram)) {
+ cp.OutputAssembly = Path.ChangeExtension(dafnyProgramName, "exe");
+ cp.CompilerOptions = "/debug";
+ } else {
+ cp.OutputAssembly = Path.ChangeExtension(dafnyProgramName, "dll");
+ cp.CompilerOptions = "/debug /target:library";
+ }
+ cp.GenerateInMemory = false;
+ cp.ReferencedAssemblies.Add("System.Numerics.dll");
+
+ var cr = provider.CompileAssemblyFromSource(cp, csharpProgram);
+ if (cr.Errors.Count == 0) {
+ Console.WriteLine("Compiled assembly into {0}", cr.PathToAssembly);
+ } else {
+ Console.WriteLine("Errors compiling program into {0}", cr.PathToAssembly);
+ foreach (var ce in cr.Errors) {
+ Console.WriteLine(ce.ToString());
+ Console.WriteLine();
+ }
+ }
+ }
+ }
+
+ static void PrintBplFile (string filename, Bpl.Program program, bool allowPrintDesugaring)
+ {
+ Contract.Requires(filename != null);
+ Contract.Requires(program != null);
+ bool oldPrintDesugaring = CommandLineOptions.Clo.PrintDesugarings;
+ if (!allowPrintDesugaring) {
+ CommandLineOptions.Clo.PrintDesugarings = false;
+ }
+ using (TokenTextWriter writer = filename == "-" ?
+ new TokenTextWriter("<console>", Console.Out, false) :
+ new TokenTextWriter(filename, false))
+ {
+ writer.WriteLine("// " + CommandLineOptions.Clo.Version);
+ writer.WriteLine("// " + CommandLineOptions.Clo.Environment);
+ writer.WriteLine();
+ program.Emit(writer);
+ }
+ CommandLineOptions.Clo.PrintDesugarings = oldPrintDesugaring;
+ }
+
+
+ static bool ProgramHasDebugInfo (Bpl.Program program)
+ {
+ Contract.Requires(program != null);
+ // We inspect the last declaration because the first comes from the prelude and therefore always has source context.
+ return program.TopLevelDeclarations.Count > 0 &&
+ cce.NonNull(program.TopLevelDeclarations[program.TopLevelDeclarations.Count - 1]).tok.IsValid;
+ }
+
+
+ /// <summary>
+ /// Inform the user about something and proceed with translation normally.
+ /// Print newline after the message.
+ /// </summary>
+ public static void Inform(string s) {
+ if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations) {
+ Console.WriteLine(s);
+ }
+ }
+
+ static void WriteTrailer(int verified, int errors, int inconclusives, int timeOuts, int outOfMemories){
+ Contract.Requires(0 <= errors && 0 <= inconclusives && 0 <= timeOuts && 0 <= outOfMemories);
+ Console.WriteLine();
+ Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.DescriptiveToolName, verified, errors, errors == 1 ? "" : "s");
+ if (inconclusives != 0) {
+ Console.Write(", {0} inconclusive{1}", inconclusives, inconclusives == 1 ? "" : "s");
+ }
+ if (timeOuts != 0) {
+ Console.Write(", {0} time out{1}", timeOuts, timeOuts == 1 ? "" : "s");
+ }
+ if (outOfMemories != 0) {
+ Console.Write(", {0} out of memory", outOfMemories);
+ }
+ Console.WriteLine();
+ Console.Out.Flush();
+ }
+
+
+
+ static void ReportBplError(IToken tok, string message, bool error)
+ {
+ Contract.Requires(message != null);
+ string s;
+ if (tok == null) {
+ s = message;
+ } else {
+ s = string.Format("{0}({1},{2}): {3}", tok.filename, tok.line, tok.col, message);
+ }
+ if (error) {
+ ErrorWriteLine(s);
+ } else {
+ Console.WriteLine(s);
+ }
+ if (tok is Dafny.NestedToken) {
+ var nt = (Dafny.NestedToken)tok;
+ ReportBplError(nt.Inner, "Related location: Related location", false);
+ }
+ }
+
+ /// <summary>
+ /// Parse the given files into one Boogie program. If an I/O or parse error occurs, an error will be printed
+ /// and null will be returned. On success, a non-null program is returned.
+ /// </summary>
+ static Bpl.Program ParseBoogieProgram(List<string/*!*/>/*!*/ fileNames, bool suppressTraceOutput)
+ {
+ Contract.Requires(cce.NonNullElements(fileNames));
+ //BoogiePL.Errors.count = 0;
+ Bpl.Program program = null;
+ bool okay = true;
+ foreach (string bplFileName in fileNames) {
+ if (!suppressTraceOutput) {
+ if (CommandLineOptions.Clo.XmlSink != null) {
+ CommandLineOptions.Clo.XmlSink.WriteFileFragment(bplFileName);
+ }
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine("Parsing " + bplFileName);
+ }
+ }
+
+ Bpl.Program programSnippet;
+ int errorCount;
+ try {
+ errorCount = Microsoft.Boogie.Parser.Parse(bplFileName, (List<string>)null, out programSnippet);
+ if (programSnippet == null || errorCount != 0) {
+ Console.WriteLine("{0} parse errors detected in {1}", errorCount, bplFileName);
+ okay = false;
+ continue;
+ }
+ } catch (IOException e) {
+ ErrorWriteLine("Error opening file \"{0}\": {1}", bplFileName, e.Message);
+ okay = false;
+ continue;
+ }
+ if (program == null) {
+ program = programSnippet;
+ } else if (programSnippet != null) {
+ program.TopLevelDeclarations.AddRange(programSnippet.TopLevelDeclarations);
+ }
+ }
+ if (!okay) {
+ return null;
+ } else if (program == null) {
+ return new Bpl.Program();
+ } else {
+ return program;
+ }
+ }
+
+ /// <summary>
+ /// Resolve, type check, infer invariants for, and verify the given Boogie program.
+ /// The intention is that this Boogie program has been produced by translation from something
+ /// else. Hence, any resolution errors and type checking errors are due to errors in
+ /// the translation.
+ /// The method prints errors for resolution and type checking errors, but still returns
+ /// their error code.
+ /// </summary>
+ static PipelineOutcome BoogiePipelineWithRerun (Bpl.Program/*!*/ program, string/*!*/ bplFileName,
+ out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories)
+ {
+ Contract.Requires(program != null);
+ Contract.Requires(bplFileName != null);
+ Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));
+
+ errorCount = verified = inconclusives = timeOuts = outOfMemories = 0;
+ PipelineOutcome oc = ResolveAndTypecheck(program, bplFileName);
+ switch (oc) {
+ case PipelineOutcome.Done:
+ return oc;
+
+ case PipelineOutcome.ResolutionError:
+ case PipelineOutcome.TypeCheckingError:
+ {
+ PrintBplFile(bplFileName, program, false);
+ Console.WriteLine();
+ Console.WriteLine("*** Encountered internal translation error - re-running Boogie to get better debug information");
+ Console.WriteLine();
+
+ List<string/*!*/>/*!*/ fileNames = new List<string/*!*/>();
+ fileNames.Add(bplFileName);
+ Bpl.Program reparsedProgram = ParseBoogieProgram(fileNames, true);
+ if (reparsedProgram != null) {
+ ResolveAndTypecheck(reparsedProgram, bplFileName);
+ }
+ }
+ return oc;
+
+ case PipelineOutcome.ResolvedAndTypeChecked:
+ EliminateDeadVariablesAndInline(program);
+ return InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);
+
+ default:
+ Contract.Assert(false);throw new cce.UnreachableException(); // unexpected outcome
+ }
+ }
+
+ static void EliminateDeadVariablesAndInline(Bpl.Program program) {
+ Contract.Requires(program != null);
+ // Eliminate dead variables
+ Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);
+
+ // Collect mod sets
+ if (CommandLineOptions.Clo.DoModSetAnalysis) {
+ Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);
+ }
+
+ // Coalesce blocks
+ if (CommandLineOptions.Clo.CoalesceBlocks) {
+ Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
+ }
+
+ // Inline
+ var TopLevelDeclarations = program.TopLevelDeclarations;
+
+ if (CommandLineOptions.Clo.ProcedureInlining != CommandLineOptions.Inlining.None) {
+ bool inline = false;
+ foreach (var d in TopLevelDeclarations) {
+ if (d.FindExprAttribute("inline") != null) {
+ inline = true;
+ }
+ }
+ if (inline && CommandLineOptions.Clo.StratifiedInlining == 0) {
+ foreach (var d in TopLevelDeclarations) {
+ var impl = d as Implementation;
+ if (impl != null) {
+ impl.OriginalBlocks = impl.Blocks;
+ impl.OriginalLocVars = impl.LocVars;
+ }
+ }
+ foreach (var d in TopLevelDeclarations) {
+ var impl = d as Implementation;
+ if (impl != null && !impl.SkipVerification) {
+ Inliner.ProcessImplementation(program, impl);
+ }
+ }
+ foreach (var d in TopLevelDeclarations) {
+ var impl = d as Implementation;
+ if (impl != null) {
+ impl.OriginalBlocks = null;
+ impl.OriginalLocVars = null;
+ }
+ }
+ }
+ }
+ }
+
+ enum PipelineOutcome { Done, ResolutionError, TypeCheckingError, ResolvedAndTypeChecked, FatalError, VerificationCompleted }
+ enum ExitValue { VERIFIED = 0, PREPROCESSING_ERROR, DAFNY_ERROR, NOT_VERIFIED }
+
+ /// <summary>
+ /// Resolves and type checks the given Boogie program. Any errors are reported to the
+ /// console. Returns:
+ /// - Done if no errors occurred, and command line specified no resolution or no type checking.
+ /// - ResolutionError if a resolution error occurred
+ /// - TypeCheckingError if a type checking error occurred
+ /// - ResolvedAndTypeChecked if both resolution and type checking succeeded
+ /// </summary>
+ static PipelineOutcome ResolveAndTypecheck (Bpl.Program program, string bplFileName)
+ {
+ Contract.Requires(program != null);
+ Contract.Requires(bplFileName != null);
+ // ---------- Resolve ------------------------------------------------------------
+
+ if (CommandLineOptions.Clo.NoResolve) { return PipelineOutcome.Done; }
+
+ int errorCount = program.Resolve();
+ if (errorCount != 0) {
+ Console.WriteLine("{0} name resolution errors detected in {1}", errorCount, bplFileName);
+ return PipelineOutcome.ResolutionError;
+ }
+
+ // ---------- Type check ------------------------------------------------------------
+
+ if (CommandLineOptions.Clo.NoTypecheck) { return PipelineOutcome.Done; }
+
+ errorCount = program.Typecheck();
+ if (errorCount != 0) {
+ Console.WriteLine("{0} type checking errors detected in {1}", errorCount, bplFileName);
+ return PipelineOutcome.TypeCheckingError;
+ }
+
+ if (CommandLineOptions.Clo.PrintFile != null && CommandLineOptions.Clo.PrintDesugarings)
+ {
+ // if PrintDesugaring option is engaged, print the file here, after resolution and type checking
+ PrintBplFile(CommandLineOptions.Clo.PrintFile, program, true);
+ }
+
+ return PipelineOutcome.ResolvedAndTypeChecked;
+ }
+
+ /// <summary>
+ /// Given a resolved and type checked Boogie program, infers invariants for the program
+ /// and then attempts to verify it. Returns:
+ /// - Done if command line specified no verification
+ /// - FatalError if a fatal error occurred, in which case an error has been printed to console
+ /// - VerificationCompleted if inference and verification completed, in which the out
+ /// parameters contain meaningful values
+ /// </summary>
+ static PipelineOutcome InferAndVerify (Bpl.Program program,
+ out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories)
+ {
+ Contract.Requires(program != null);
+ Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));
+
+ errorCount = verified = inconclusives = timeOuts = outOfMemories = 0;
+
+ // ---------- Infer invariants --------------------------------------------------------
+
+ // Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)
+ if (CommandLineOptions.Clo.UseAbstractInterpretation) {
+ if (CommandLineOptions.Clo.Ai.J_Intervals || CommandLineOptions.Clo.Ai.J_Trivial) {
+ Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);
+ } else {
+ // use /infer:j as the default
+ CommandLineOptions.Clo.Ai.J_Intervals = true;
+ Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);
+ }
+ }
+
+ if (CommandLineOptions.Clo.LoopUnrollCount != -1) {
+ program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);
+ }
+
+ if (CommandLineOptions.Clo.PrintInstrumented) {
+ program.Emit(new TokenTextWriter(Console.Out));
+ }
+
+ if (CommandLineOptions.Clo.ExpandLambdas) {
+ LambdaHelper.ExpandLambdas(program);
+ //PrintBplFile ("-", program, true);
+ }
+
+ // ---------- Verify ------------------------------------------------------------
+
+ if (!CommandLineOptions.Clo.Verify) { return PipelineOutcome.Done; }
+
+ #region Verify each implementation
+
+#if ROB_DEBUG
+ string now = DateTime.Now.ToString().Replace(' ','-').Replace('/','-').Replace(':','-');
+ System.IO.StreamWriter w = new System.IO.StreamWriter(@"\temp\batch_"+now+".bpl");
+ program.Emit(new TokenTextWriter(w));
+ w.Close();
+#endif
+
+ ConditionGeneration vcgen = null;
+ try
+ {
+ vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ }
+ catch (ProverException e)
+ {
+ ErrorWriteLine("Fatal Error: ProverException: {0}", e);
+ return PipelineOutcome.FatalError;
+ }
+
+ var decls = program.TopLevelDeclarations.ToArray();
+ foreach (var decl in decls )
+ {
+ Contract.Assert(decl != null);
+ Implementation impl = decl as Implementation;
+ if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification)
+ {
+ List<Counterexample>/*?*/ errors;
+
+ DateTime start = new DateTime(); // to please compiler's definite assignment rules
+ if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations || CommandLineOptions.Clo.XmlSink != null)
+ {
+ start = DateTime.Now;
+ if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations)
+ {
+ Console.WriteLine();
+ Console.WriteLine("Verifying {0} ...", impl.Name);
+ }
+ if (CommandLineOptions.Clo.XmlSink != null)
+ {
+ CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, start);
+ }
+ }
+
+ ConditionGeneration.Outcome outcome;
+ int prevAssertionCount = vcgen.CumulativeAssertionCount;
+ try
+ {
+ outcome = vcgen.VerifyImplementation(impl, out errors);
+ }
+ catch (VCGenException e)
+ {
+ ReportBplError(impl.tok, String.Format("Error BP5010: {0} Encountered in implementation {1}.", e.Message, impl.Name), true);
+ errors = null;
+ outcome = VCGen.Outcome.Inconclusive;
+ }
+ catch (UnexpectedProverOutputException upo)
+ {
+ AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message);
+ errors = null;
+ outcome = VCGen.Outcome.Inconclusive;
+ }
+
+ string timeIndication = "";
+ DateTime end = DateTime.Now;
+ TimeSpan elapsed = end - start;
+ if (CommandLineOptions.Clo.Trace) {
+ int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;
+ timeIndication = string.Format(" [{0:F3} s, {1} proof obligation{2}] ", elapsed.TotalSeconds, poCount, poCount == 1 ? "" : "s");
+ } else if (CommandLineOptions.Clo.TraceProofObligations) {
+ int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;
+ timeIndication = string.Format(" [{0} proof obligation{1}] ", poCount, poCount == 1 ? "" : "s");
+ }
+
+ switch (outcome)
+ {
+ default:
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected outcome
+ case VCGen.Outcome.Correct:
+ Inform(String.Format("{0}verified", timeIndication));
+ verified++;
+ break;
+ case VCGen.Outcome.TimedOut:
+ timeOuts++;
+ Inform(String.Format("{0}timed out", timeIndication));
+ break;
+ case VCGen.Outcome.OutOfMemory:
+ outOfMemories++;
+ Inform(String.Format("{0}out of memory", timeIndication));
+ break;
+ case VCGen.Outcome.Inconclusive:
+ inconclusives++;
+ Inform(String.Format("{0}inconclusive", timeIndication));
+ break;
+ case VCGen.Outcome.Errors:
+ Contract.Assert(errors != null); // guaranteed by postcondition of VerifyImplementation
+ // BP1xxx: Parsing errors
+ // BP2xxx: Name resolution errors
+ // BP3xxx: Typechecking errors
+ // BP4xxx: Abstract interpretation errors (Is there such a thing?)
+ // BP5xxx: Verification errors
+
+ errors.Sort(new CounterexampleComparer());
+ foreach (Counterexample error in errors)
+ {
+ if (error is CallCounterexample)
+ {
+ CallCounterexample err = (CallCounterexample)error;
+ ReportBplError(err.FailingCall.tok, (err.FailingCall.ErrorData as string) ?? "Error BP5002: A precondition for this call might not hold.", true);
+ ReportBplError(err.FailingRequires.tok, (err.FailingRequires.ErrorData as string) ?? "Related location: This is the precondition that might not hold.", false);
+ if (CommandLineOptions.Clo.XmlSink != null)
+ {
+ CommandLineOptions.Clo.XmlSink.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, error.Trace);
+ }
+ }
+ else if (error is ReturnCounterexample)
+ {
+ ReturnCounterexample err = (ReturnCounterexample)error;
+ ReportBplError(err.FailingReturn.tok, "Error BP5003: A postcondition might not hold on this return path.", true);
+ ReportBplError(err.FailingEnsures.tok, (err.FailingEnsures.ErrorData as string) ?? "Related location: This is the postcondition that might not hold.", false);
+ ReportAllBplErrors(err.FailingEnsures.Attributes);
+ if (CommandLineOptions.Clo.XmlSink != null)
+ {
+ CommandLineOptions.Clo.XmlSink.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, error.Trace);
+ }
+ }
+ else // error is AssertCounterexample
+ {
+ AssertCounterexample err = (AssertCounterexample)error;
+ if (err.FailingAssert is LoopInitAssertCmd)
+ {
+ ReportBplError(err.FailingAssert.tok, "Error BP5004: This loop invariant might not hold on entry.", true);
+ if (CommandLineOptions.Clo.XmlSink != null)
+ {
+ CommandLineOptions.Clo.XmlSink.WriteError("loop invariant entry violation", err.FailingAssert.tok, null, error.Trace);
+ }
+ }
+ else if (err.FailingAssert is LoopInvMaintainedAssertCmd)
+ {
+ // this assertion is a loop invariant which is not maintained
+ ReportBplError(err.FailingAssert.tok, "Error BP5005: This loop invariant might not be maintained by the loop.", true);
+ if (CommandLineOptions.Clo.XmlSink != null)
+ {
+ CommandLineOptions.Clo.XmlSink.WriteError("loop invariant maintenance violation", err.FailingAssert.tok, null, error.Trace);
+ }
+ }
+ else
+ {
+ string msg = err.FailingAssert.ErrorData as string;
+ if (msg == null)
+ {
+ msg = "Error BP5001: This assertion might not hold.";
+ }
+ ReportBplError(err.FailingAssert.tok, msg, true);
+ var attr = err.FailingAssert.Attributes;
+ ReportAllBplErrors(attr);
+ if (CommandLineOptions.Clo.XmlSink != null)
+ {
+ CommandLineOptions.Clo.XmlSink.WriteError("assertion violation", err.FailingAssert.tok, null, error.Trace);
+ }
+ }
+ }
+ if (CommandLineOptions.Clo.EnhancedErrorMessages == 1)
+ {
+ foreach (string info in error.relatedInformation)
+ {
+ Contract.Assert(info != null);
+ Console.WriteLine(" " + info);
+ }
+ }
+ if (CommandLineOptions.Clo.ErrorTrace > 0)
+ {
+ Console.WriteLine("Execution trace:");
+ foreach (Block b in error.Trace)
+ {
+ Contract.Assert(b != null);
+ if (b.tok == null)
+ {
+ Console.WriteLine(" <intermediate block>");
+ }
+ else
+ {
+ // for ErrorTrace == 1 restrict the output;
+ // do not print tokens with -17:-4 as their location because they have been
+ // introduced in the translation and do not give any useful feedback to the user
+ if (!(CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4))
+ {
+ Console.WriteLine(" {0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label);
+ }
+ }
+ }
+ }
+ if (CommandLineOptions.Clo.ModelViewFile != null)
+ {
+ error.PrintModel();
+ }
+ errorCount++;
+ }
+
+ Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));
+ break;
+ }
+
+ if (CommandLineOptions.Clo.XmlSink != null)
+ {
+ CommandLineOptions.Clo.XmlSink.WriteEndMethod(outcome.ToString().ToLowerInvariant(), end, elapsed);
+ }
+ if (outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace)
+ {
+ Console.Out.Flush();
+ }
+ }
+ }
+ vcgen.Close();
+ cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();
+
+ #endregion
+
+ return PipelineOutcome.VerificationCompleted;
+ }
+
+ private static void ReportAllBplErrors(QKeyValue attr) {
+ while (attr != null) {
+ if (attr.Key == "msg" && attr.Params.Count == 1) {
+ var str = attr.Params[0] as string;
+ if (str != null) {
+ ReportBplError(attr.tok, "Error: "+str, false);
+ }
+ }
+ attr = attr.Next;
+ }
+ }
+
+ }
+}
diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj new file mode 100644 index 00000000..6f32302d --- /dev/null +++ b/Source/DafnyDriver/DafnyDriver.csproj @@ -0,0 +1,182 @@ +<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+ <PropertyGroup>
+ <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+ <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+ <ProductVersion>9.0.30729</ProductVersion>
+ <SchemaVersion>2.0</SchemaVersion>
+ <ProjectGuid>{63400D1F-05B2-453E-9592-1EAB74B2C9CC}</ProjectGuid>
+ <OutputType>Exe</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>Dafny</RootNamespace>
+ <AssemblyName>Dafny</AssemblyName>
+ <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
+ <FileAlignment>512</FileAlignment>
+ <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
+ <SignAssembly>true</SignAssembly>
+ <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
+ <FileUpgradeFlags>
+ </FileUpgradeFlags>
+ <OldToolsVersion>3.5</OldToolsVersion>
+ <UpgradeBackupLocation />
+ <IsWebBootstrapper>false</IsWebBootstrapper>
+ <TargetFrameworkProfile />
+ <PublishUrl>publish\</PublishUrl>
+ <Install>true</Install>
+ <InstallFrom>Disk</InstallFrom>
+ <UpdateEnabled>false</UpdateEnabled>
+ <UpdateMode>Foreground</UpdateMode>
+ <UpdateInterval>7</UpdateInterval>
+ <UpdateIntervalUnits>Days</UpdateIntervalUnits>
+ <UpdatePeriodically>false</UpdatePeriodically>
+ <UpdateRequired>false</UpdateRequired>
+ <MapFileExtensions>true</MapFileExtensions>
+ <ApplicationRevision>0</ApplicationRevision>
+ <ApplicationVersion>1.0.0.%2a</ApplicationVersion>
+ <UseApplicationTrust>false</UseApplicationTrust>
+ <BootstrapperEnabled>true</BootstrapperEnabled>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+ <DebugSymbols>true</DebugSymbols>
+ <DebugType>full</DebugType>
+ <Optimize>false</Optimize>
+ <OutputPath>..\..\Binaries\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+ <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
+ <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly>
+ </CodeContractsCustomRewriterAssembly>
+ <CodeContractsCustomRewriterClass>
+ </CodeContractsCustomRewriterClass>
+ <CodeContractsLibPaths>
+ </CodeContractsLibPaths>
+ <CodeContractsExtraRewriteOptions>
+ </CodeContractsExtraRewriteOptions>
+ <CodeContractsExtraAnalysisOptions>
+ </CodeContractsExtraAnalysisOptions>
+ <CodeContractsBaseLineFile>
+ </CodeContractsBaseLineFile>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
+ <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
+ <DebugType>pdbonly</DebugType>
+ <Optimize>true</Optimize>
+ <OutputPath>bin\Release\</OutputPath>
+ <DefineConstants>TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
+ <DebugSymbols>true</DebugSymbols>
+ <OutputPath>..\..\Binaries\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <DebugType>full</DebugType>
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>
+ <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly />
+ <CodeContractsCustomRewriterClass />
+ <CodeContractsLibPaths />
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsExtraAnalysisOptions />
+ <CodeContractsBaseLineFile />
+ <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ </PropertyGroup>
+ <ItemGroup>
+ <Reference Include="AbsInt">
+ <HintPath>..\..\Binaries\AbsInt.dll</HintPath>
+ </Reference>
+ <Reference Include="Core">
+ <HintPath>..\..\Binaries\Core.dll</HintPath>
+ </Reference>
+ <Reference Include="ParserHelper, Version=2.2.30705.1126, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\Binaries\ParserHelper.dll</HintPath>
+ </Reference>
+ <Reference Include="System" />
+ <Reference Include="System.Data" />
+ <Reference Include="System.Xml" />
+ <Reference Include="VCGeneration">
+ <HintPath>..\..\Binaries\VCGeneration.dll</HintPath>
+ </Reference>
+ </ItemGroup>
+ <ItemGroup>
+ <Compile Include="DafnyDriver.cs" />
+ <Compile Include="..\version.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <ProjectReference Include="..\Dafny\DafnyPipeline.csproj">
+ <Project>{FE44674A-1633-4917-99F4-57635E6FA740}</Project>
+ <Name>DafnyPipeline</Name>
+ </ProjectReference>
+ </ItemGroup>
+ <ItemGroup>
+ <BootstrapperPackage Include="Microsoft.Net.Client.3.5">
+ <Visible>False</Visible>
+ <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>
+ <Install>false</Install>
+ </BootstrapperPackage>
+ <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">
+ <Visible>False</Visible>
+ <ProductName>.NET Framework 3.5 SP1</ProductName>
+ <Install>true</Install>
+ </BootstrapperPackage>
+ <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1">
+ <Visible>False</Visible>
+ <ProductName>Windows Installer 3.1</ProductName>
+ <Install>true</Install>
+ </BootstrapperPackage>
+ </ItemGroup>
+ <ItemGroup>
+ <None Include="app.config" />
+ </ItemGroup>
+ <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
+ <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
+ Other similar extension points exist, see Microsoft.Common.targets.
+ <Target Name="BeforeBuild">
+ </Target>
+ <Target Name="AfterBuild">
+ </Target>
+ -->
+</Project>
\ No newline at end of file diff --git a/Source/DafnyDriver/app.config b/Source/DafnyDriver/app.config new file mode 100644 index 00000000..cb2586be --- /dev/null +++ b/Source/DafnyDriver/app.config @@ -0,0 +1,3 @@ +<?xml version="1.0"?>
+<configuration>
+<startup><supportedRuntime version="v4.0" sku=".NETFramework,Version=v4.0"/></startup></configuration>
|