Chalice: Implemented -vs switch, for use when running Chalice from inside Visual Studio

3 files changed, 40 insertions, 17 deletions

diff --git a/Chalice/src/Boogie.scala b/Chalice/src/Boogie.scala
index 492e0669..b60ce521 100644
--- a/Chalice/src/Boogie.scala
+++ b/Chalice/src/Boogie.scala
@@ -133,7 +133,9 @@ object Boogie {
     (v,e)

   }

 

- // def out(s: String) = Console.out.print(s)

+  var vsMode = false;  // global variable settable from outside the class (non-ideal design)

+

+  // def out(s: String) = Console.out.print(s)

   var indentLevel = 1

   def indent: String = {

     def doIndent(i: int): String = {

@@ -194,7 +196,15 @@ object Boogie {
   }

   def PrintStmt(s: Stmt): String = s match {

     case Comment(msg) => indent +  "// " +  msg + nl

-    case assert@Assert(e) => indent +  "assert " + "{:msg \"  " + assert.pos + ": " + assert.message + "\"}" + " " + PrintExpr(e) + ";" + nl

+    case assert@Assert(e) =>

+      val pos = if (vsMode) {

+        val r = assert.pos.line - 1;

+        val c = assert.pos.column - 1;

+        r + "," + c + "," + r + "," + (c+5) + ":"

+      } else {

+        "  " + assert.pos + ": "

+      }

+      indent +  "assert " + "{:msg \"" + pos + assert.message + "\"}" + " " + PrintExpr(e) + ";" + nl

     case Assume(e) => indent + "assume " + PrintExpr(e) +  ";" + nl

     case If(guard, thn, els) =>

       indent + "if (" +

diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala
index 1bba1a99..1a6e3e48 100644
--- a/Chalice/src/Chalice.scala
+++ b/Chalice/src/Chalice.scala
@@ -7,6 +7,7 @@ import java.io.BufferedReader
 import java.io.InputStreamReader

 import java.io.File

 import java.io.FileWriter

+import scala.util.parsing.input.Position

 

 object Chalice {

   def main(args: Array[String]): unit = {

@@ -14,6 +15,16 @@ object Chalice {
     // parse command-line arguments

     var inputName: String = null

     var printProgram = false

+    var vsMode = false;

+    def ReportError(pos: Position, msg: String) = {

+      if (vsMode) {

+        val r = pos.line - 1;

+        val c = pos.column - 1;

+        Console.out.println(r + "," + c + "," + r + "," + (c+5) + ":" + msg);

+      } else {

+        Console.err.println(pos + ": " + msg)

+      }

+    }

     var doTypecheck = true

     var doTranslate = true

     var checkLeaks = false

@@ -32,6 +43,7 @@ object Chalice {
       if (a == "-print") printProgram = true

       else if (a == "-noTranslate") doTranslate = false

       else if (a == "-noTypecheck") doTypecheck = false

+      else if (a == "-vs") vsMode = true

       else if (a == "-checkLeaks") checkLeaks = true

       else if (a == "-noDeadlockChecks") skipDeadlockChecks = true

       else if (a.startsWith("-boogie:")) boogiePath = a.substring(8)

@@ -54,18 +66,19 @@ object Chalice {
     // parse program

     val parser = new Parser();

     parser.parseFile(inputName) match {

-      case e: parser.NoSuccess => Console.err.println("Error: " + e)

+      case e: parser.NoSuccess =>

+        if (vsMode)

+          ReportError(e.next.pos, e.msg);

+        else

+          Console.err.println("Error: " + e)

       case parser.Success(prog, _) =>

         if (printProgram) PrintProgram.P(prog)

         if (doTypecheck) {

           // typecheck program

           Resolver.Resolve(prog) match {

-            case Resolver.Error(pos, msg) => 

-              Console.err.println("The program did not typecheck.\n");

-              Console.err.println(msg)

             case Resolver.Errors(msgs) => 

-              Console.err.println("The program did not typecheck."); 

-              msgs foreach { msg => Console.err.println(msg) }

+              if (!vsMode) Console.err.println("The program did not typecheck.");

+              msgs foreach { msg => ReportError(msg._1, msg._2) }

             case Resolver.Success() =>

               if (doTranslate) {

                 // checking if Boogie.exe exists

@@ -73,7 +86,7 @@ object Chalice {
                 if(! boogieFile.exists() || ! boogieFile.isFile()) {

                   CommandLineError("Boogie.exe not found at " + boogiePath); return

                 }

-                // translate program to BoogiePL

+                // translate program to Boogie

                 val translator = new Translator();

                 // set the translation options

                 TranslationOptions.checkLeaks = checkLeaks;

@@ -83,6 +96,7 @@ object Chalice {
                 TranslationOptions.skipDeadlockChecks = skipDeadlockChecks;

                 val bplProg = translator.translateProgram(prog);

                 // write to out.bpl

+                Boogie.vsMode = vsMode;

                 val bplText = TranslatorPrelude.P + (bplProg map Boogie.Print).foldLeft(""){ (a, b) => a + b };

                 writeFile("out.bpl", bplText);

                 // run Boogie.exe on out.bpl

@@ -115,6 +129,6 @@ object Chalice {
 

   def CommandLineError(msg: String) = {

     Console.err.println("Error: " + msg)

-    Console.err.println("syntax: chalice [-print] [-noTypecheck] [-noTranslate] [-boogie:path] [-defaults] [-autoFold] [-checkLeaks] [-noDeadlockChecks] inputFile")

+    Console.err.println("syntax: chalice [-print] [-noTypecheck] [-noTranslate] [-vs] [-boogie:path] [-defaults] [-autoFold] [-checkLeaks] [-noDeadlockChecks] inputFile")

   }

 }

diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index 00daaa92..9e8e5b4a 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -9,8 +9,7 @@ import scala.util.parsing.input.Positional
 object Resolver {

   sealed abstract class ResolverOutcome

   case class Success extends ResolverOutcome

-  case class Error(pos: Position, s: String) extends ResolverOutcome

-  case class Errors(ss: List[String]) extends ResolverOutcome

+  case class Errors(ss: List[(Position,String)]) extends ResolverOutcome

 

   var seqClasses = Map[String, SeqClass]();

 

@@ -19,9 +18,9 @@ object Resolver {
     val CurrentClass = currentClass

     var currentMember = null: Member;

     def CurrentMember = currentMember: Member;  

-    var errors: List[String] = Nil

+    var errors: List[(Position,String)] = Nil

     def Error(pos: Position, msg: String) {

-      errors = errors + (pos + ": " + msg)

+      errors = errors + (pos, msg)

     }

     def AddVariable(v: Variable): ProgramContext = {

       new LProgramContext(v, this);

@@ -48,7 +47,7 @@ object Resolver {
     var decls = Map[String,TopLevelDecl]()

     for (decl <- BoolClass :: IntClass :: RootClass :: NullClass :: MuClass :: prog) {

       if (decls contains decl.id) {

-        return Error(decl.pos, "duplicate class/channel name: " + decl.id)

+        return Errors(List((decl.pos, "duplicate class/channel name: " + decl.id)))

       } else {

         decl match {

           case cl: Class =>

@@ -57,7 +56,7 @@ object Resolver {
               case m: NamedMember =>

                 m.Parent = cl

                 if (cl.mm contains m.Id) {

-                  return Error(m.pos, "duplicate member name " + m.Id + " in class " + cl.id)

+                  return Errors(List((m.pos, "duplicate member name " + m.Id + " in class " + cl.id)))

                 } else {

                   cl.mm = cl.mm + (m.Id -> m)

                 }

@@ -67,7 +66,7 @@ object Resolver {
         decls = decls + (decl.id -> decl)

       }

     }

-    var errors = List[String]()

+    var errors = List[(Position,String)]()

 

     // resolve types of members

     val contextNoCurrentClass = new ProgramContext(decls, null)