Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.sln

2 files changed, 178 insertions, 252 deletions

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index bd87186b..fcf556f0 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -20,7 +20,6 @@ namespace Microsoft.Boogie
   using Microsoft.Boogie.AbstractInterpretation;

   using System.Diagnostics;

   using VC;

-  using Cci = System.Compiler;

   using AI = Microsoft.AbstractInterpretationFramework;

 

 /* 

@@ -69,17 +68,6 @@ namespace Microsoft.Boogie
         Console.WriteLine("--------------------");

       }

 

-      SelectPlatform(CommandLineOptions.Clo);

-

-      // Make sure the Spec# runtime is initialized.

-      // This happens when the static constructor for the Runtime type is executed.

-      // Otherwise, if a reference happens to get chased to it, it is loaded twice

-      // and then the types in it do not get unique representations.

-      if (System.Type.GetType("Mono.Runtime") == null) {  // MONO

-        Cci.AssemblyNode a = Microsoft.SpecSharp.Runtime.RuntimeAssembly;

-        Contract.Assert( a != null);

-      }

-

       foreach (string file in CommandLineOptions.Clo.Files) 

       {Contract.Assert(file != null);

         string extension = Path.GetExtension(file);

@@ -146,78 +134,11 @@ namespace Microsoft.Boogie
       Console.ForegroundColor = col;

     }

 

-    public static void SelectPlatform(CommandLineOptions options)

-    {

-      Contract.Requires(options != null);

-      if (options.TargetPlatformLocation != null) {

-        // Make sure static constructor runs before we start setting locations, etc.

-        System.Compiler.SystemTypes.Clear();

-

-        switch (options.TargetPlatform){

-        case CommandLineOptions.PlatformType.v1: Microsoft.SpecSharp.TargetPlatform.SetToV1(options.TargetPlatformLocation); break;

-        case CommandLineOptions.PlatformType.v11: Microsoft.SpecSharp.TargetPlatform.SetToV1_1(options.TargetPlatformLocation); break;

-        case CommandLineOptions.PlatformType.v2: Microsoft.SpecSharp.TargetPlatform.SetToV2(options.TargetPlatformLocation); break;

-        case CommandLineOptions.PlatformType.cli1: Microsoft.SpecSharp.TargetPlatform.SetToPostV1_1(options.TargetPlatformLocation); break;

-        }

-        

-        if (options.StandardLibraryLocation != null && options.StandardLibraryLocation.Length > 0){

-          System.Compiler.SystemAssemblyLocation.Location = options.StandardLibraryLocation;

-        }

-        System.Compiler.SystemCompilerRuntimeAssemblyLocation.Location = options.TargetPlatformLocation + @"\System.Compiler.Runtime.dll";

-                

-        System.Compiler.SystemTypes.Initialize(true, true);

-      }

-    }

-  

-    static string GetErrorLine(Cci.ErrorNode node)

-    {    Contract.Requires( node.SourceContext.Document == null || node.SourceContext.Document.Name != null);

-    

-    

-    Contract.Requires(node != null);

-    Contract.Ensures(Contract.Result<string>() != null);

-

-      string message = node.GetMessage(System.Threading.Thread.CurrentThread.CurrentUICulture);

-      string kind;

-      if (message.Contains("(trace position)")) {

-        kind = "Related information";

-      } else {

-        kind = "Error";

-      }

-      if (node.SourceContext.Document != null) {

-        return string.Format("{0}({1},{2}): {3}: {4}", Path.GetFileName(cce.NonNull(node.SourceContext.Document.Name)), node.SourceContext.StartLine, node.SourceContext.StartColumn, kind, message);

-      } else {

-        return string.Format("{0}: {1}", kind, message);

-      }

-    }

-

     enum FileType { Unknown, Cil, Bpl, Dafny };

 

-    class ErrorReporter

-    {

-        public Cci.ErrorNodeList errors = new Cci.ErrorNodeList();

-      [ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(errors!=null);

-}

-

-        public int errorsReported;

-        

-        public void ReportErrors()

-        {

-            //sort the portion of the array that will be reported to make output more deterministic

-            errors.Sort(errorsReported,errors.Count-errorsReported);

-            for(;errorsReported < errors.Count; errorsReported++) {

-                Cci.ErrorNode error = errors[errorsReported];

-                if (error != null)

-                    ErrorWriteLine(GetErrorLine(error));

-            } 

-        }

-    }

-

     static void ProcessFiles (List<string/*!*/>/*!*/ fileNames)

     {

-  Contract.Requires(cce.NonNullElements(fileNames));

+      Contract.Requires(cce.NonNullElements(fileNames));

       using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count-1])) {

         Dafny.Program dafnyProgram;

         string programName = fileNames.Count == 1 ? fileNames[0] : "the program";

@@ -242,7 +163,7 @@ void ObjectInvariant()
           }

 

           int errorCount, verified, inconclusives, timeOuts, outOfMemories;

-          PipelineOutcome oc = BoogiePipelineWithRerun(boogieProgram, bplFilename, null/*new ErrorReporter()*/, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);

+          PipelineOutcome oc = BoogiePipelineWithRerun(boogieProgram, bplFilename, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);

           switch (oc) {

             case PipelineOutcome.VerificationCompleted:

               if (CommandLineOptions.Clo.Compile && errorCount == 0 && inconclusives == 0 && timeOuts == 0 && outOfMemories == 0) {

@@ -420,7 +341,6 @@ void ObjectInvariant()
     /// their error code.

     /// </summary>

     static PipelineOutcome BoogiePipelineWithRerun (Program/*!*/ program, string/*!*/ bplFileName,

-        ErrorReporter errorReporter,

         out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories)

     {Contract.Requires(program != null);

     Contract.Requires(cce.NonNullElements(bplFileName));

@@ -451,7 +371,7 @@ void ObjectInvariant()
           return oc;

 

         case PipelineOutcome.ResolvedAndTypeChecked:

-          return InferAndVerify(program, errorReporter, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);

+          return InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);

           

         default:

           Contract.Assert(false);throw new cce.UnreachableException();  // unexpected outcome

@@ -511,7 +431,6 @@ void ObjectInvariant()
     ///    parameters contain meaningful values

     /// </summary>

     static PipelineOutcome InferAndVerify (Program program,

-                                           ErrorReporter errorReporter,

                                            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));

@@ -569,169 +488,188 @@ void ObjectInvariant()
       foreach ( Declaration decl in program.TopLevelDeclarations )

       {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.XmlSink != null) {

-            start = DateTime.Now;

-            if (CommandLineOptions.Clo.Trace) {

-              Console.WriteLine();

-              Console.WriteLine("Verifying {0} ...", impl.Name);

-            }

-            if (CommandLineOptions.Clo.XmlSink != null) {

-              CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, start);

-            }

-          }

+        if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification)

+        {

+            List<Counterexample>/*?*/ errors;

 

-          ConditionGeneration.Outcome outcome;

-          try

-          {

-            outcome = vcgen.VerifyImplementation(impl, program, out errors);

-          }

-          catch (VCGenException e)

-          {

-            ReportBplError(impl, 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;

-          }

+            DateTime start = new DateTime();  // to please compiler's definite assignment rules

+            if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null)

+            {

+                start = DateTime.Now;

+                if (CommandLineOptions.Clo.Trace)

+                {

+                    Console.WriteLine();

+                    Console.WriteLine("Verifying {0} ...", impl.Name);

+                }

+                if (CommandLineOptions.Clo.XmlSink != null)

+                {

+                    CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, start);

+                }

+            }

 

-          string timeIndication = "";

-          DateTime end = DateTime.Now;

-          TimeSpan elapsed = end - start;

-          if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) {

-            if (CommandLineOptions.Clo.Trace) {

-              timeIndication = string.Format("  [{0} s]  ", elapsed.TotalSeconds);

+            ConditionGeneration.Outcome outcome;

+            try

+            {

+                outcome = vcgen.VerifyImplementation(impl, program, out errors);

+            }

+            catch (VCGenException e)

+            {

+                ReportBplError(impl, 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;

             }

-          }

-          

 

-          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

-              if (errorReporter != null)

-              {

-//                assert translatedProgram != null;

-//                ErrorReporting h = new ErrorReporting();

-//                h.errorReportingWithTrace(translatedProgram, errors, impl);

-                

-                errorReporter.ReportErrors();

-              }

-              else

-              {

-                // 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)

+            string timeIndication = "";

+            DateTime end = DateTime.Now;

+            TimeSpan elapsed = end - start;

+            if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null)

+            {

+                if (CommandLineOptions.Clo.Trace)

                 {

-                  if (error is CallCounterexample)

-                  {

-                    CallCounterexample err = (CallCounterexample) error;

-                    ReportBplError(err.FailingCall, "Error BP5002: A precondition for this call might not hold.", true);

-                    ReportBplError(err.FailingRequires, "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, "Error BP5003: A postcondition might not hold on this return path.", true);

-                    ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false);

-                    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, "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, "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, msg, true);

-                      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);

+                    timeIndication = string.Format("  [{0} s]  ", elapsed.TotalSeconds);

+                }

+            }

+

+            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, "Error BP5002: A precondition for this call might not hold.", true);

+                            ReportBplError(err.FailingRequires, "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, "Error BP5003: A postcondition might not hold on this return path.", true);

+                            ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false);

+                            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, "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, "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, msg, true);

+                                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++;

                     }

-                  }

-                  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();

-          }

+

+                    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();

diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj
index afd8f9b3..1ec5abb0 100644
--- a/Source/DafnyDriver/DafnyDriver.csproj
+++ b/Source/DafnyDriver/DafnyDriver.csproj
@@ -97,19 +97,7 @@
       <SpecificVersion>False</SpecificVersion>

       <HintPath>..\Core\bin\Debug\Core.dll</HintPath>

     </Reference>

-    <Reference Include="Microsoft.SpecSharp, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\Microsoft.SpecSharp.dll</HintPath>

-    </Reference>

     <Reference Include="System" />

-    <Reference Include="System.Compiler, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\System.Compiler.dll</HintPath>

-    </Reference>

-    <Reference Include="System.Compiler.Runtime, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\System.Compiler.Runtime.dll</HintPath>

-    </Reference>

     <Reference Include="System.Data" />

     <Reference Include="System.Xml" />

     <Reference Include="VCGeneration, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">