Chalice: accept many input files at once; read from stdin if no input file specified

5 files changed, 209 insertions, 174 deletions

diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 53c2093d..4f63f57b 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -10,7 +10,9 @@ import scala.util.parsing.input.Positional
 

 trait ASTNode extends Positional

 

-// classes and types

+/**

+ * Classes and types

+ */

 

 case class TopLevelDecl(id: String) extends ASTNode

 

@@ -115,7 +117,9 @@ sealed case class TokenType(C: Type, m: String) extends Type("token", Nil) {  //
   override def FullName: String = "token<" + C.FullName + "." + m + ">"

 }

 

-// members

+/**

+ * Members 

+ */

 

 sealed abstract class Member extends ASTNode {

   val Hidden: Boolean = false  // hidden means not mentionable in source

@@ -167,7 +171,9 @@ case class Precondition(e: Expression) extends Specification
 case class Postcondition(e: Expression) extends Specification

 case class LockChange(ee: List[Expression]) extends Specification

 

-// statements

+/**

+ * Statements

+ */

 

 sealed abstract class Statement extends ASTNode

 case class Assert(e: Expression) extends Statement

@@ -197,6 +203,9 @@ case class Call(declaresLocal: List[Boolean], lhs: List[VariableExpr], obj: Expr
   var locals = List[Variable]()

   var m: Method = null

 }

+case class Spec(declaresLocal: List[Boolean], lhs: List[VariableExpr], pred: Expression) extends Statement {

+  var locals = List[Variable]()

+}

 case class Install(obj: Expression, lowerBounds: List[Expression], upperBounds: List[Expression]) extends Statement

 case class Share(obj: Expression, lowerBounds: List[Expression], upperBounds: List[Expression]) extends Statement

 case class Unshare(obj: Expression) extends Statement

@@ -228,7 +237,9 @@ case class Receive(declaresLocal: List[Boolean], ch: Expression, outs: List[Vari
 case class Fold(pred: Access) extends Statement

 case class Unfold(pred: Access) extends Statement

 

-// expressions

+/**

+ * Expressions

+ */

 

 sealed abstract class RValue extends ASTNode {

   var typ: Class = null

@@ -370,7 +381,10 @@ case class LockBelow(e0: Expression, e1: Expression) extends CompareExpr(e0,e1)
   override val OpName = "<<"

 }

 

-// quantifiers

+/**

+ * Expressions: quantifiers

+ */

+

 trait Quant

 object Forall extends Quant

 object Exists extends Quant

@@ -384,7 +398,9 @@ sealed abstract class Quantification(q: Quant, is: List[String], e: Expression)
 case class SeqQuantification(q: Quant, is: List[String], seq: Expression, e: Expression) extends Quantification(q, is, e)

 case class TypeQuantification(q: Quant, is: List[String], t: Type, e: Expression) extends Quantification(q, is, e)

 

-// sequences

+/**

+ * Expressions: sequences

+ */

 

 case class EmptySeq(t: Type) extends Literal

 case class ExplicitSeq(elems: List[Expression]) extends Expression

@@ -428,7 +444,9 @@ case class CallState(token: Expression, obj: Expression, id: String, args: List[
   def target() = token;

 }

 

-// visitors / operations

+/**

+ * AST operations

+ */

 

 object AST {

   /**

diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala
index 0342964b..449db023 100644
--- a/Chalice/src/Chalice.scala
+++ b/Chalice/src/Chalice.scala
@@ -9,12 +9,12 @@ import java.io.InputStreamReader
 import java.io.File

 import java.io.FileWriter

 import scala.util.parsing.input.Position

+import collection.mutable.ListBuffer

 

 object Chalice {

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

    var boogiePath = "C:\\boogie\\Binaries\\Boogie.exe"

-   // parse command-line arguments

-   var inputName: String = null

+   val inputs = new ListBuffer[String]()

    var printProgram = false

    var vsMode = false;

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

@@ -55,109 +55,127 @@ object Chalice {
      "-autoFold" -> {() => autoFold = true},

      "-autoMagic"-> {() => autoMagic = true}

    )

-   val help = options.keys.foldLeft("syntax: chalice")((s, o) => s + " [" + o + "]") +

+   lazy val help = options.keys.foldLeft("syntax: chalice")((s, o) => s + " [" + o + "]") +

    " [-boogie:path]" +

    " [-defaults:int]" +

    " [<boogie option>]*" +

-   " <input file.chalice>";

+   " <file.chalice>";

 

    for (a <- args) {

      if (options contains a) options(a)()

      else if (a == "-help") {Console.out.println(help); return}

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

-     else if (a.startsWith("-defaults:")) { try { defaults = Integer.parseInt(a.substring(10)); if(3<=defaults) { autoMagic = true; } } catch { case _ => CommandLineError("-defaults takes integer argument", help); } }

+     else if (a.startsWith("-defaults:")) {

+       try {

+         defaults = Integer.parseInt(a.substring(10));

+         if (3<=defaults) { autoMagic = true; }

+       } catch { case _ => CommandLineError("-defaults takes integer argument", help); }

+     }

      else if (a.startsWith("-") || a.startsWith("/")) boogieArgs += (a + " ") // other arguments starting with "-" or "/" are sent to Boogie.exe

-     else if (inputName != null) { CommandLineError("multiple input filenames: " + inputName + " and " + a, help); return }

-     else { inputName = a }

+     else inputs += a

    }

 

-   // check the command-line arguments

-   if (inputName == null && vsMode) {

-     inputName = "<stdin>"

-   } else if (inputName == null) { CommandLineError("missing input filename", help); return } else {

-     val file = new File(inputName);

-     if(! file.exists()){

+   // check that input files exist

+   var files = for (input <- inputs.toList) yield {

+     val file = new File(input);

+     if(! file.exists) {

        CommandLineError("input file " + file.getName() + " could not be found", help); return

      }

+     file;

    }

-   // parse program

+

+   // parse programs

    val parser = new Parser();

-   parser.parseFile(inputName) match {

-     case e: parser.NoSuccess =>

+   val parseResults = if (files.isEmpty) {

+     List(parser.parseStdin)

+   } else for (file <- files) yield {

+     parser.parseFile(file)

+   }

+   

+   // report errors and merge declarations

+   assert(parseResults.size > 0)

+   var parseErrors = false;

+   val program:List[TopLevelDecl] = parseResults.map(result => result match {

+     case e:parser.NoSuccess =>

+       parseErrors = true;

        if (vsMode)

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

        else

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

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

+       Nil

      case parser.Success(prog, _) =>

        if (printProgram) PrintProgram.P(prog)

-       if (doTypecheck) {

-         // typecheck program

-         Resolver.Resolve(prog) match {

-           case Resolver.Errors(msgs) => 

-             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

-               val boogieFile = new File(boogiePath);

-               if(! boogieFile.exists() || ! boogieFile.isFile()) {

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

-               }

-               // translate program to Boogie

-               val translator = new Translator();

-               // set the translation options

-               TranslationOptions.checkLeaks = checkLeaks;

-               TranslationOptions.defaults = defaults;

-               TranslationOptions.autoFold = autoFold;

-               TranslationOptions.autoMagic = autoMagic;

-               TranslationOptions.skipDeadlockChecks = skipDeadlockChecks;

-               TranslationOptions.skipTermination = skipTermination;

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

-               val bplFilename = if (vsMode) "c:\\tmp\\out.bpl" else "out.bpl"

-               writeFile(bplFilename, bplText);

-               // run Boogie.exe on out.bpl

-               val boogie = Runtime.getRuntime.exec(boogiePath + " /errorTrace:0 " + boogieArgs + bplFilename);

-               // terminate boogie if interrupted

-               Runtime.getRuntime.addShutdownHook(new Thread(new Runnable() {

-                 def run {

-                   val kill = Runtime.getRuntime.exec("taskkill /T /F /IM Boogie.exe");

-                   kill.waitFor;

-                   // just to be sure

-                   boogie.destroy

-                 }

-               }))

-               // the process blocks until we exhaust input and error streams

-               new Thread(new Runnable() {

-                 def run {

-                   val err = new BufferedReader(new InputStreamReader(boogie.getErrorStream));

-                   var line = err.readLine;

-                   while(line!=null) {Console.err.println(line); Console.err.flush}

-                 }

-               }).start;

-               val input = new BufferedReader(new InputStreamReader(boogie.getInputStream));

-               var line = input.readLine();

-               var previous_line = null: String;

-               while(line!=null){

-                 Console.out.println(line);

-                 Console.out.flush;

-                 previous_line = line;

-                 line = input.readLine();

-               }

-               boogie.waitFor;

-               input.close;

+       prog

+   }).flatten;

+   if (parseErrors) return;

 

-               // generate code

-               if(gen && (previous_line != null) && previous_line.endsWith(" 0 errors")) { // hack

-                 val converter = new ChaliceToCSharp(); 

-                 println("Code generated in out.cs.");

-                 writeFile("out.cs", converter.convertProgram(prog));

-               }

+   // typecheck program   

+   if (doTypecheck) {

+     Resolver.Resolve(program) match {

+       case Resolver.Errors(msgs) =>

+         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

+           val boogieFile = new File(boogiePath);

+           if(! boogieFile.exists() || ! boogieFile.isFile()) {

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

+           }

+           // translate program to Boogie

+           val translator = new Translator();

+           // set the translation options

+           TranslationOptions.checkLeaks = checkLeaks;

+           TranslationOptions.defaults = defaults;

+           TranslationOptions.autoFold = autoFold;

+           TranslationOptions.autoMagic = autoMagic;

+           TranslationOptions.skipDeadlockChecks = skipDeadlockChecks;

+           TranslationOptions.skipTermination = skipTermination;

+           val bplProg = translator.translateProgram(program);

+           // write to out.bpl

+           Boogie.vsMode = vsMode;

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

+           val bplFilename = if (vsMode) "c:\\tmp\\out.bpl" else "out.bpl"

+           writeFile(bplFilename, bplText);

+           // run Boogie.exe on out.bpl

+           val boogie = Runtime.getRuntime.exec(boogiePath + " /errorTrace:0 " + boogieArgs + bplFilename);

+           // terminate boogie if interrupted

+           Runtime.getRuntime.addShutdownHook(new Thread(new Runnable() {

+             def run {

+               val kill = Runtime.getRuntime.exec("taskkill /T /F /IM Boogie.exe");

+               kill.waitFor;

+               // just to be sure

+               boogie.destroy

              }

+           }))

+           // the process blocks until we exhaust input and error streams

+           new Thread(new Runnable() {

+             def run {

+               val err = new BufferedReader(new InputStreamReader(boogie.getErrorStream));

+               var line = err.readLine;

+               while(line!=null) {Console.err.println(line); Console.err.flush}

+             }

+           }).start;

+           val input = new BufferedReader(new InputStreamReader(boogie.getInputStream));

+           var line = input.readLine();

+           var previous_line = null: String;

+           while(line!=null){

+             Console.out.println(line);

+             Console.out.flush;

+             previous_line = line;

+             line = input.readLine();

+           }

+           boogie.waitFor;

+           input.close;

+

+           // generate code

+           if(gen && (previous_line != null) && previous_line.endsWith(" 0 errors")) { // hack

+             val converter = new ChaliceToCSharp();

+             println("Code generated in out.cs.");

+             writeFile("out.cs", converter.convertProgram(program));

            }

-       }

+         }

+     }   

    }

  }

 

diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index 8999add9..b57a5ea4 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -10,17 +10,12 @@ import scala.collection.immutable.PagedSeq
 import scala.util.parsing.input.Position

 import scala.util.parsing.input.Positional

 import scala.util.parsing.input.NoPosition

+import java.io.File

 

 class Parser extends StandardTokenParsers {

 

-  def parseFile(path: String): this.ParseResult[List[TopLevelDecl]] = {

-    val tokens = if (path == "<stdin>") {

-        new lexical.Scanner(new PagedSeqReader(PagedSeq fromReader Console.in))

-      } else {

-        new lexical.Scanner(new PagedSeqReader(PagedSeq fromFile path));

-      }

-    phrase(programUnit)(tokens)

-  }

+  def parseStdin = phrase(programUnit)(new lexical.Scanner(new PagedSeqReader(PagedSeq fromReader Console.in)))

+  def parseFile(file: File) = phrase(programUnit)(new lexical.Scanner(new PagedSeqReader(PagedSeq fromFile file)))

  

   case class PositionedString(v: String) extends Positional

 

@@ -44,8 +39,12 @@ class Parser extends StandardTokenParsers {
                          ";", ":", ":=", ",", "?", "|", "[", "]", "++", "::")

 

   def programUnit = (classDecl | channelDecl)*

+  def Semi = ";" ?

+  var currentLocalVariables = Set[String]() // used in the method context

 

-  // class and members

+  /**

+   * Top level declarations

+   */

 

   def classDecl =

         positioned(("external" ?) ~ ("class" ~> ident) ~ opt("module" ~> ident) ~ "{" ~ (memberDecl*) <~ "}" ^^ {

@@ -54,31 +53,22 @@ class Parser extends StandardTokenParsers {
             ext match { case None => case Some(t) => cl.IsExternal = true }

             cl

         })

-  def memberDecl = positioned(fieldDecl | invariantDecl | methodDecl | conditionDecl |

-                   predicateDecl | functionDecl)

+  def channelDecl =

+    "channel" ~> ident ~ formalParameters(true) ~ ("where" ~> expression ?) <~ Semi ^^ {

+      case id ~ ins ~ None => Channel(id, ins, BoolLiteral(true))

+      case id ~ ins ~ Some(e) => Channel(id, ins, e)

+    }

 

+  /**

+   * Member declarations

+   */

+

+  def memberDecl = positioned(fieldDecl | invariantDecl | methodDecl | conditionDecl | predicateDecl | functionDecl)

   def fieldDecl =

         ( "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id, t, false) }

         | "ghost" ~> "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id, t, true) }

         )

-  def Ident = 

-    positioned(ident ^^ PositionedString)

-  def idType =

-    idTypeOpt ^^ {

-      case (id, None) => (id, Type("int", Nil))

-      case (id, Some(t)) => (id, t) }

-  def idTypeOpt =

-    ident ~ (":" ~> typeDecl ?) ^^ { case id ~ optT => (id, optT) }

-  def typeDecl: Parser[Type] =

-      positioned(("int" | "bool" | ident | "seq") ~ opt("<" ~> repsep(typeDecl, ",") <~ ">") ^^ { case t ~ parameters => Type(t, parameters.getOrElse(Nil)) }

-      | ("token" ~ "<") ~> (typeDecl <~ ".") ~ ident <~ ">" ^^ { case c ~ m => TokenType(c, m) }

-      )

-  def Semi = ";" ?

-

-  var currentLocalVariables = Set[String]()

-

   def invariantDecl = positioned("invariant" ~> expression <~ Semi ^^ MonitorInvariant)

-

   def methodDecl = {

     currentLocalVariables = Set[String]()

     "method" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~

@@ -88,51 +78,60 @@ class Parser extends StandardTokenParsers {
           case None => Method(id, ins, Nil, spec, body)

           case Some(outs) => Method(id, ins, outs, spec, body) }}

   }

-  def channelDecl =

-    "channel" ~> ident ~ formalParameters(true) ~ ("where" ~> expression ?) <~ Semi ^^ {

-      case id ~ ins ~ None => Channel(id, ins, BoolLiteral(true))

-      case id ~ ins ~ Some(e) => Channel(id, ins, e)

-    }

-  def predicateDecl: Parser[Predicate] = 

+  def predicateDecl: Parser[Predicate] =

     ("predicate" ~> ident) ~ ("{" ~> expression <~ "}") ^^ { case id ~ definition => Predicate(id, definition) }

   def functionDecl = 

-    ("function" ~> ident) ~ formalParameters(true) ~ (":" ~> typeDecl) ~ (methodSpec*) ~ opt("{" ~> expression <~ "}") ^^ { case id ~ ins ~ out ~ specs ~ body => Function(id, ins, out, specs, body) }

+    ("function" ~> ident) ~ formalParameters(true) ~ (":" ~> typeDecl) ~ (methodSpec*) ~ opt("{" ~> expression <~ "}") ^^ {

+      case id ~ ins ~ out ~ specs ~ body => Function(id, ins, out, specs, body)

+    }

+  def conditionDecl =

+    "condition" ~> ident ~ ("where" ~> expression ?) <~ Semi ^^ {

+      case id ~ optE => Condition(id, optE) }

+  

   def formalParameters(immutable: Boolean) =

     "(" ~> (formalList(immutable) ?) <~ ")" ^^ {

       case None => Nil

       case Some(ids) => ids }

-  def formalList(immutable: Boolean) = {

-    repsep(formal(immutable), ",")

-  }

+  def formalList(immutable: Boolean) = repsep(formal(immutable), ",")  

   def formal(immutable: Boolean): Parser[Variable] =

     idType ^^ {case (id,t) =>

       currentLocalVariables = currentLocalVariables + id;

-      if (immutable)

-        new ImmutableVariable(id,t)

-      else

-        new Variable(id,t) 

+      if (immutable) new ImmutableVariable(id,t)

+      else new Variable(id,t) 

     }

 

+  def Ident = positioned(ident ^^ PositionedString)

+  def idType =

+    idTypeOpt ^^ {

+      case (id, None) => (id, Type("int", Nil))

+      case (id, Some(t)) => (id, t) }

+  def idTypeOpt =

+    ident ~ (":" ~> typeDecl ?) ^^ { case id ~ optT => (id, optT) }

+  def typeDecl: Parser[Type] =

+      positioned(("int" | "bool" | ident | "seq") ~ opt("<" ~> repsep(typeDecl, ",") <~ ">") ^^ { case t ~ parameters => Type(t, parameters.getOrElse(Nil)) }

+      | ("token" ~ "<") ~> (typeDecl <~ ".") ~ ident <~ ">" ^^ { case c ~ m => TokenType(c, m) }

+      )

+

+  /**

+   * Pre and post conditions

+   */

+  

   def methodSpec =

     positioned( "requires" ~> expression <~ Semi ^^ Precondition

     | "ensures" ~> expression <~ Semi ^^ Postcondition

     | "lockchange" ~> expressionList <~ Semi ^^ LockChange

     )

-  def blockStatement: Parser[List[Statement]] = {

-    "{" ~> blockStatementBody <~ "}"

-  }

+

+  /**

+   * Statements

+   */

+

+  def blockStatement: Parser[List[Statement]] = "{" ~> blockStatementBody <~ "}"

   def blockStatementBody: Parser[List[Statement]] = {

     val prev = currentLocalVariables

     (statement*) ^^ {

       case x => currentLocalVariables = prev; x }

   }

-

-  def conditionDecl =

-    "condition" ~> ident ~ ("where" ~> expression ?) <~ Semi ^^ {

-      case id ~ optE => Condition(id, optE) }

-

-  // statements

-

   def statement: Parser[Statement] =

     positioned( "assert" ~> expression <~ Semi ^^ Assert

     | "assume" ~> expression <~ Semi ^^ Assume

@@ -316,9 +315,11 @@ class Parser extends StandardTokenParsers {
         case l ~ None => (l,Nil)

         case l ~ Some(u) => (l,u) }

     )

-  

-  // expressions

 

+  /**

+   * Expressions

+   */

+  

   def expressionList =

     repsep(expression, ",")

   def expression = positioned(iteExpr)

@@ -400,7 +401,6 @@ class Parser extends StandardTokenParsers {
   def exprBody =

     "{" ~> expression <~ "}"

 

-  // what is "FerSure"?

   def selectExprFerSure: Parser[MemberAccess] =

     positioned(atom ~ "." ~ ident ~ ("." ~> ident *) ^^ {

       case e ~ _ ~ field ~ moreFields =>

@@ -486,28 +486,22 @@ class Parser extends StandardTokenParsers {
     | ("[" ~> expressionList <~ "]") ^^ { case es => ExplicitSeq(es) }

     )

 

-  // Scala type inference resists figuring out | (alternative) for these two

-

   def quantifierSeq: Parser[Quantification] =

     (quant ~ repsep(ident, ",")) into {case q ~ is => quantifierSeqBody(q, is)}

-

   def quantifierSeqBody(q: Quant, is: List[String]) : Parser[Quantification] =

     (("in" ~> expression <~ "::") ~ (exprWithLocals(is))) ^^

       { case seq ~ e =>

         currentLocalVariables = currentLocalVariables -- is;

         SeqQuantification(q, is, seq, e);

       }

-  

   def quantifierType: Parser[Quantification] =

     (quant ~ repsep(ident, ",")) into {case q ~ is => quantifierTypeBody(q, is)}

-

   def quantifierTypeBody(q: Quant, is: List[String]) : Parser[Quantification] =

     ((":" ~> typeDecl <~ "::") ~ (exprWithLocals(is))) ^^

       { case t ~ e =>

         currentLocalVariables = currentLocalVariables -- is;

         TypeQuantification(q, is, t, e);

       }

-

   def quant: Parser[Quant] =

     ( "forall" ^^^ Forall | "exists" ^^^ Exists)

 

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 45d875f0..d5ddfdcd 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -77,6 +77,8 @@ class Translator {
         translatePredicate(pred)

       case inv: MonitorInvariant =>

         Nil // already dealt with before

+      case _: Condition =>

+        throw new Exception("not yet implemented")

     }

   }

 

@@ -159,40 +161,41 @@ class Translator {
   def definitionAxiom(f: Function): List[Decl] = {

     assert(f.definition.isDefined)

     val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)});

-    val frameFunctionName = "##" + f.FullName;

-

-    /* axiom (forall h: HeapType, m: MaskType, this: ref, x_1: t_1, ..., x_n: t_n ::

-         wf(h, m) && CurrentModule == module#C ==> #C.f(h, m, this, x_1, ..., x_n) == tr(body))

-    */

     val args = VarExpr("this") :: inArgs;

-    var formals = BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar);

+    val formals = BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar);

     val applyF = FunctionApp(functionName(f), List(etran.Heap, etran.Mask) ::: args);

 

-    /** Limit application of the function by introducing a second limited function */

-    val body = etran.Tr(if (f.isRecursive) {

-      val limited = Map() ++ (f.SCC zip (f.SCC map {f =>

-        val result = Function(f.id + "#limited", f.ins, f.out, f.spec, f.definition);

-        result.Parent = f.Parent;

-        result;

-      }));

-      def limit: Expression => Option[Expression] = _ match {

-        case app @ FunctionApplication(obj, id, args) if (f.SCC contains app.f) =>

-          val result = FunctionApplication(obj transform limit, id, args map (e => e transform limit));          

-          result.f = limited(app.f);          

-          Some(result)

-        case _ => None

+    /** Limit application of the function by introducing a second (limited) function */

+    val body = etran.Tr(

+      if (f.isRecursive && ! f.isUnlimited) {

+        val limited = Map() ++ (f.SCC zip (f.SCC map {f =>

+          val result = Function(f.id + "#limited", f.ins, f.out, f.spec, f.definition);

+          result.Parent = f.Parent;

+          result;

+        }));

+        def limit: Expression => Option[Expression] = _ match {

+          case app @ FunctionApplication(obj, id, args) if (f.SCC contains app.f) =>

+            val result = FunctionApplication(obj transform limit, id, args map (e => e transform limit));

+            result.f = limited(app.f);

+            Some(result)

+          case _ => None

+        }

+        f.definition.get transform limit;

+      } else {

+        f.definition.get

       }

-      f.definition.get transform limit;

-    } else

-      f.definition.get);

+    );

 

+    /* axiom (forall h: HeapType, m: MaskType, this: ref, x_1: t_1, ..., x_n: t_n ::

+         wf(h, m) && CurrentModule == module#C ==> #C.f(h, m, this, x_1, ..., x_n) == tr(body))

+    */    

     Axiom(new Boogie.Forall(

       formals, new Trigger(applyF),

         (wf(VarExpr(HeapName), VarExpr(MaskName)) && (CurrentModule ==@ ModuleName(currentClass)))

         ==>

         (applyF ==@ body))) ::

     (if (f.isRecursive)

-      // define the limited function

+      // define the limited function (even for unlimited function since its SCC might have limited functions)

       Boogie.Function(functionName(f) + "#limited", formals, BVar("$myresult", f.out.typ)) ::

       Axiom(new Boogie.Forall(

         formals, new Trigger(applyF),

@@ -1553,6 +1556,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         case Frac(p) => (Tr(p), 0) : (Expr, Expr)

         case Epsilon => (0, 1) : (Expr, Expr)        // TODO: check for infinity bounds -- or perhaps just wait till epsilons are gone

         case Epsilons(p) => (0, Tr(p)) : (Expr, Expr)

+        case Star => throw new Exception("not yet implemented")

       };

 

       (if (check) isDefined(s)(true) ::: isDefined(perm)(true) else Nil) :::

@@ -1731,6 +1735,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         case Frac(p) => (p, 0) : (Expr, Expr)

         case Epsilon => (0, 1) : (Expr, Expr)        // TODO: check for infinity bounds -- or perhaps just wait till epsilons are gone

         case Epsilons(p) => (0, p) : (Expr, Expr)

+        case Star => throw new Exception("not yet implemented")

       };

 

       (if (check) isDefined(s)(true) ::: isDefined(perm)(true) else Nil) :::

diff --git a/Chalice/test.bat b/Chalice/test.bat
index 9bc0f5ea..b45207b6 100644
--- a/Chalice/test.bat
+++ b/Chalice/test.bat
@@ -1,7 +1,7 @@
 @echo off

 echo start > Output

 

-set CHALICE=call scala -cp bin Chalice -nologo -boogie:"C:\\Users\\t-kuayes\\Documents\\Boogie-2010-07-13\\Boogie.exe" 

+set CHALICE=call scala -cp bin chalice.Chalice -nologo -boogie:"C:\\Users\\t-kuayes\\Documents\\Boogie-2010-07-13\\Boogie.exe" 

 

 

 REM to do: AssociationList