diff options
Diffstat (limited to 'Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs')
| -rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs | 419 |
1 files changed, 0 insertions, 419 deletions
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs deleted file mode 100644 index 39829bb0..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs +++ /dev/null @@ -1,419 +0,0 @@ -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;
- }
- }
- }
- }
-}
|