diff options
Diffstat (limited to 'Source/DafnyExtension/DafnyDriver.cs')
| -rw-r--r-- | Source/DafnyExtension/DafnyDriver.cs | 419 |
1 files changed, 419 insertions, 0 deletions
diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs new file mode 100644 index 00000000..39829bb0 --- /dev/null +++ b/Source/DafnyExtension/DafnyDriver.cs @@ -0,0 +1,419 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.IO;
+using System.Diagnostics;
+using System.Diagnostics.Contracts;
+// Here come the Dafny/Boogie specific imports
+//using PureCollections;
+using Bpl = Microsoft.Boogie;
+using Dafny = Microsoft.Dafny;
+using Microsoft.Boogie.AbstractInterpretation;
+using VC;
+// using AI = Microsoft.AbstractInterpretationFramework;
+
+
+namespace DafnyLanguage
+{
+ class DafnyDriver
+ {
+ readonly string _programText;
+ readonly string _filename;
+ Dafny.Program _program;
+ List<DafnyError> _errors = new List<DafnyError>();
+ public List<DafnyError> Errors { get { return _errors; } }
+
+ public DafnyDriver(string programText, string filename) {
+ _programText = programText;
+ _filename = filename;
+ }
+
+ void RecordError(int line, int col, ErrorCategory cat, string msg) {
+ _errors.Add(new DafnyError(line, col, cat, msg));
+ }
+
+ static DafnyDriver() {
+ Initialize();
+ }
+
+ static void Initialize() {
+ if (Dafny.DafnyOptions.O == null) {
+ var options = new Dafny.DafnyOptions();
+ options.ProverKillTime = 10;
+ options.ErrorTrace = 0;
+ Dafny.DafnyOptions.Install(options);
+ options.ApplyDefaultOptions();
+ }
+ }
+
+ public Dafny.Program ProcessResolution() {
+ if (!ParseAndTypeCheck()) {
+ return null;
+ }
+ return _program;
+ }
+
+ bool ParseAndTypeCheck() {
+ Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null);
+ Dafny.BuiltIns builtIns = new Dafny.BuiltIns();
+ int errorCount = Dafny.Parser.Parse(_programText, _filename, module, builtIns, new VSErrors(this));
+ if (errorCount != 0)
+ return false;
+ Dafny.Program program = new Dafny.Program(_filename, module, builtIns);
+
+ Dafny.Resolver r = new VSResolver(program, this);
+ r.ResolveProgram(program);
+ if (r.ErrorCount != 0)
+ return false;
+
+ _program = program;
+ return true; // success
+ }
+
+ class VSErrors : Dafny.Errors
+ {
+ DafnyDriver dd;
+ public VSErrors(DafnyDriver dd) {
+ this.dd = dd;
+ }
+ public override void SynErr(string filename, int line, int col, string msg) {
+ dd.RecordError(line - 1, col - 1, ErrorCategory.ParseError, msg);
+ count++;
+ }
+ public override void SemErr(string filename, int line, int col, string msg) {
+ dd.RecordError(line - 1, col - 1, ErrorCategory.ResolveError, msg);
+ count++;
+ }
+ public override void Warning(string filename, int line, int col, string msg) {
+ dd.RecordError(line - 1, col - 1, ErrorCategory.ParseWarning, msg);
+ }
+ }
+
+ class VSResolver : Dafny.Resolver
+ {
+ DafnyDriver dd;
+ public VSResolver(Dafny.Program program, DafnyDriver dd)
+ : base(program) {
+ this.dd = dd;
+ }
+ public override void Error(Bpl.IToken tok, string msg, params object[] args) {
+ string s = string.Format(msg, args);
+ dd.RecordError(tok.line - 1, tok.col - 1, ErrorCategory.ResolveError, s);
+ ErrorCount++;
+ }
+ }
+
+ public static bool Verify(Dafny.Program dafnyProgram, ErrorReporterDelegate er) {
+ Dafny.Translator translator = new Dafny.Translator();
+ Bpl.Program boogieProgram = translator.Translate(dafnyProgram);
+
+ PipelineOutcome oc = BoogiePipeline(boogieProgram, er);
+ switch (oc) {
+ case PipelineOutcome.Done:
+ case PipelineOutcome.VerificationCompleted:
+ // TODO: This would be the place to proceed to compile the program, if desired
+ return true;
+ case PipelineOutcome.FatalError:
+ default:
+ return false;
+ }
+ }
+
+ enum PipelineOutcome { Done, ResolutionError, TypeCheckingError, ResolvedAndTypeChecked, FatalError, VerificationCompleted }
+
+ /// <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.
+ /// </summary>
+ static PipelineOutcome BoogiePipeline(Bpl.Program/*!*/ program, ErrorReporterDelegate er) {
+ Contract.Requires(program != null);
+
+ PipelineOutcome oc = BoogieResolveAndTypecheck(program);
+ if (oc == PipelineOutcome.ResolvedAndTypeChecked) {
+ EliminateDeadVariablesAndInline(program);
+ return BoogieInferAndVerify(program, er);
+ }
+ return oc;
+ }
+
+ static void EliminateDeadVariablesAndInline(Bpl.Program program) {
+ Contract.Requires(program != null);
+ // Eliminate dead variables
+ Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);
+
+ // Collect mod sets
+ if (Bpl.CommandLineOptions.Clo.DoModSetAnalysis) {
+ Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);
+ }
+
+ // Coalesce blocks
+ if (Bpl.CommandLineOptions.Clo.CoalesceBlocks) {
+ Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
+ }
+
+ // Inline
+ var TopLevelDeclarations = program.TopLevelDeclarations;
+
+ if (Bpl.CommandLineOptions.Clo.ProcedureInlining != Bpl.CommandLineOptions.Inlining.None) {
+ bool inline = false;
+ foreach (var d in TopLevelDeclarations) {
+ if (d.FindExprAttribute("inline") != null) {
+ inline = true;
+ }
+ }
+ if (inline && Bpl.CommandLineOptions.Clo.StratifiedInlining == 0) {
+ foreach (var d in TopLevelDeclarations) {
+ var impl = d as Bpl.Implementation;
+ if (impl != null) {
+ impl.OriginalBlocks = impl.Blocks;
+ impl.OriginalLocVars = impl.LocVars;
+ }
+ }
+ foreach (var d in TopLevelDeclarations) {
+ var impl = d as Bpl.Implementation;
+ if (impl != null && !impl.SkipVerification) {
+ Bpl.Inliner.ProcessImplementation(program, impl);
+ }
+ }
+ foreach (var d in TopLevelDeclarations) {
+ var impl = d as Bpl.Implementation;
+ if (impl != null) {
+ impl.OriginalBlocks = null;
+ impl.OriginalLocVars = null;
+ }
+ }
+ }
+ }
+ }
+
+ /// <summary>
+ /// Resolves and type checks the given Boogie program.
+ /// 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 BoogieResolveAndTypecheck(Bpl.Program program) {
+ Contract.Requires(program != null);
+ // ---------- Resolve ------------------------------------------------------------
+ int errorCount = program.Resolve();
+ if (errorCount != 0) {
+ return PipelineOutcome.ResolutionError;
+ }
+
+ // ---------- Type check ------------------------------------------------------------
+ errorCount = program.Typecheck();
+ if (errorCount != 0) {
+ return PipelineOutcome.TypeCheckingError;
+ }
+
+ 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
+ /// - VerificationCompleted if inference and verification completed, in which the out
+ /// parameters contain meaningful values
+ /// </summary>
+ static PipelineOutcome BoogieInferAndVerify(Bpl.Program program, ErrorReporterDelegate er) {
+ Contract.Requires(program != null);
+
+ // ---------- Infer invariants --------------------------------------------------------
+
+ // Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)
+ if (Bpl.CommandLineOptions.Clo.UseAbstractInterpretation) {
+ if (Bpl.CommandLineOptions.Clo.Ai.J_Intervals || Bpl.CommandLineOptions.Clo.Ai.J_Trivial) {
+ Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);
+ } else {
+ // use /infer:j as the default
+ Bpl.CommandLineOptions.Clo.Ai.J_Intervals = true;
+ Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);
+ }
+ }
+
+ if (Bpl.CommandLineOptions.Clo.LoopUnrollCount != -1) {
+ program.UnrollLoops(Bpl.CommandLineOptions.Clo.LoopUnrollCount);
+ }
+
+ if (Bpl.CommandLineOptions.Clo.ExpandLambdas) {
+ Bpl.LambdaHelper.ExpandLambdas(program);
+ //PrintBplFile ("-", program, true);
+ }
+
+ // ---------- Verify ------------------------------------------------------------
+
+ if (!Bpl.CommandLineOptions.Clo.Verify) { return PipelineOutcome.Done; }
+
+ #region Verify each implementation
+
+ ConditionGeneration vcgen = null;
+ try {
+ vcgen = new VCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend);
+ } catch (Bpl.ProverException) {
+ return PipelineOutcome.FatalError;
+ }
+
+ var decls = program.TopLevelDeclarations.ToArray();
+ foreach (var decl in decls) {
+ Contract.Assert(decl != null);
+ Bpl.Implementation impl = decl as Bpl.Implementation;
+ if (impl != null && Bpl.CommandLineOptions.Clo.UserWantsToCheckRoutine(impl.Name) && !impl.SkipVerification) {
+ List<Bpl.Counterexample>/*?*/ errors;
+
+ ConditionGeneration.Outcome outcome;
+ int prevAssertionCount = vcgen.CumulativeAssertionCount;
+ try {
+ outcome = vcgen.VerifyImplementation(impl, out errors);
+ } catch (VCGenException) {
+ errors = null;
+ outcome = VCGen.Outcome.Inconclusive;
+ } catch (Bpl.UnexpectedProverOutputException) {
+ errors = null;
+ outcome = VCGen.Outcome.Inconclusive;
+ }
+
+ switch (outcome) {
+ default:
+ Contract.Assert(false); throw new Exception(); // unexpected outcome
+ case VCGen.Outcome.Correct:
+ break;
+ case VCGen.Outcome.TimedOut:
+ er(new DafnyErrorInformation(impl.tok, "Verification timed out (" + impl.Name + ")"));
+ break;
+ case VCGen.Outcome.OutOfMemory:
+ er(new DafnyErrorInformation(impl.tok, "Verification out of memory (" + impl.Name + ")"));
+ break;
+ case VCGen.Outcome.Inconclusive:
+ er(new DafnyErrorInformation(impl.tok, "Verification inconclusive (" + impl.Name + ")"));
+ break;
+ case VCGen.Outcome.Errors:
+ Contract.Assert(errors != null); // guaranteed by postcondition of VerifyImplementation
+
+ errors.Sort(new Bpl.CounterexampleComparer());
+ foreach (var error in errors) {
+ DafnyErrorInformation errorInfo;
+
+ if (error is Bpl.CallCounterexample) {
+ var err = (Bpl.CallCounterexample)error;
+ errorInfo = new DafnyErrorInformation(err.FailingCall.tok, err.FailingCall.ErrorData as string ?? "A precondition for this call might not hold.");
+ errorInfo.AddAuxInfo(err.FailingRequires.tok, err.FailingRequires.ErrorData as string ?? "Related location: This is the precondition that might not hold.");
+
+ } else if (error is Bpl.ReturnCounterexample) {
+ var err = (Bpl.ReturnCounterexample)error;
+ errorInfo = new DafnyErrorInformation(err.FailingReturn.tok, "A postcondition might not hold on this return path.");
+ errorInfo.AddAuxInfo(err.FailingEnsures.tok, err.FailingEnsures.ErrorData as string ?? "Related location: This is the postcondition that might not hold.");
+ errorInfo.AddAuxInfo(err.FailingEnsures.Attributes);
+
+ } else { // error is AssertCounterexample
+ var err = (Bpl.AssertCounterexample)error;
+ if (err.FailingAssert is Bpl.LoopInitAssertCmd) {
+ errorInfo = new DafnyErrorInformation(err.FailingAssert.tok, "This loop invariant might not hold on entry.");
+ } else if (err.FailingAssert is Bpl.LoopInvMaintainedAssertCmd) {
+ // this assertion is a loop invariant which is not maintained
+ errorInfo = new DafnyErrorInformation(err.FailingAssert.tok, "This loop invariant might not be maintained by the loop.");
+ } else {
+ string msg = err.FailingAssert.ErrorData as string;
+ if (msg == null) {
+ msg = "This assertion might not hold.";
+ }
+ errorInfo = new DafnyErrorInformation(err.FailingAssert.tok, msg);
+ errorInfo.AddAuxInfo(err.FailingAssert.Attributes);
+ }
+ }
+ if (Bpl.CommandLineOptions.Clo.ErrorTrace > 0) {
+ foreach (Bpl.Block b in error.Trace) {
+ // 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 (!(Bpl.CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4) &&
+ b.tok.line != 0 && b.tok.col != 0) {
+ errorInfo.AddAuxInfo(b.tok, "Execution trace: " + b.Label);
+ }
+ }
+ }
+ // if (Bpl.CommandLineOptions.Clo.ModelViewFile != null) {
+ // error.PrintModel();
+ // }
+ er(errorInfo);
+ }
+ break;
+ }
+ }
+ }
+ vcgen.Close();
+ Bpl.CommandLineOptions.Clo.TheProverFactory.Close();
+
+ #endregion
+
+ return PipelineOutcome.VerificationCompleted;
+ }
+
+ public delegate void ErrorReporterDelegate(DafnyErrorInformation errInfo);
+
+ public class DafnyErrorInformation
+ {
+ public readonly Bpl.IToken Tok;
+ public readonly string Msg;
+ public readonly List<DafnyErrorAuxInfo> Aux = new List<DafnyErrorAuxInfo>();
+
+ public class DafnyErrorAuxInfo
+ {
+ public readonly Bpl.IToken Tok;
+ public readonly string Msg;
+ public DafnyErrorAuxInfo(Bpl.IToken tok, string msg) {
+ Tok = tok;
+ Msg = CleanUp(msg);
+ }
+ }
+
+ public DafnyErrorInformation(Bpl.IToken tok, string msg) {
+ Contract.Requires(tok != null);
+ Contract.Requires(1 <= tok.line && 1 <= tok.col);
+ Contract.Requires(msg != null);
+ Tok = tok;
+ Msg = CleanUp(msg);
+ AddNestingsAsAux(tok);
+ }
+ public void AddAuxInfo(Bpl.IToken tok, string msg) {
+ Contract.Requires(tok != null);
+ Contract.Requires(1 <= tok.line && 1 <= tok.col);
+ Contract.Requires(msg != null);
+ Aux.Add(new DafnyErrorAuxInfo(tok, msg));
+ AddNestingsAsAux(tok);
+ }
+ void AddNestingsAsAux(Bpl.IToken tok) {
+ while (tok is Dafny.NestedToken) {
+ var nt = (Dafny.NestedToken)tok;
+ tok = nt.Inner;
+ Aux.Add(new DafnyErrorAuxInfo(tok, "Related location"));
+ }
+ }
+ public void AddAuxInfo(Bpl.QKeyValue attr) {
+ while (attr != null) {
+ if (attr.Key == "msg" && attr.Params.Count == 1 && attr.tok.line != 0 && attr.tok.col != 0) {
+ var str = attr.Params[0] as string;
+ if (str != null) {
+ AddAuxInfo(attr.tok, str);
+ }
+ }
+ attr = attr.Next;
+ }
+ }
+
+ public static string CleanUp(string msg) {
+ if (msg.ToLower().StartsWith("error: ")) {
+ return msg.Substring(7);
+ } else {
+ return msg;
+ }
+ }
+ }
+ }
+}
|