Chalice:

* add sequence axiom updates from Dafny
* fix a bug in pretty printer for functions and predicates
* add a command line option for not checking termination; refactor options code to update syntax help string
* relax resolver to allow ghost state in assume statements (we don't know how to compile them in general anyways; assume false is still a special case and is compiled into assert false)

6 files changed, 68 insertions, 30 deletions

diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala
index 49f6b74e..8e95a725 100644
--- a/Chalice/src/Chalice.scala
+++ b/Chalice/src/Chalice.scala
@@ -36,33 +36,47 @@ object Chalice {
    var autoFold = false

    var autoMagic = false

    var skipDeadlockChecks = false

+   var skipTermination = false;

    var boogieArgs = " ";

    var gen = false;

 

+   // closures should be idempotent

+   val options = Map(

+     "-print" -> {() => printProgram = true},

+     "-noTranslate" -> {() => doTranslate = false},

+     "-noTypecheck"-> {() => doTypecheck = false},

+     "-vs" -> {() => vsMode = true},

+     "-checkLeaks" -> {() => checkLeaks = true},

+     "-noDeadlockChecks" -> {() => skipDeadlockChecks = true},

+     "-noTermination" -> {() => skipTermination = true}, 

+     "-defaults" -> {() => defaults = 3},

+     "-gen" -> {() => gen = true},

+     "-autoFold" -> {() => autoFold = true},

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

+   )

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

+   " [-boogie:path]" +

+   " [-defaults:int]" +

+   " [<boogie option>]*" +

+   " <input file.chalice>";

+

    for (a <- args) {

-     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

+     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 == "-defaults") defaults = 3

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

-     else if (a == "-gen") { gen = true; }

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

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

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

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

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

    }

+

    // check the command-line arguments

    if (inputName == null && vsMode) {

      inputName = "<stdin>"

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

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

      val file = new File(inputName);

      if(! file.exists()){

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

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

      }

    }

    // parse program

@@ -86,7 +100,7 @@ object Chalice {
                // checking if Boogie.exe exists

                val boogieFile = new File(boogiePath);

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

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

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

                }

                // translate program to Boogie

                val translator = new Translator();

@@ -96,6 +110,7 @@ object Chalice {
                TranslationOptions.autoFold = autoFold;

                TranslationOptions.autoMagic = autoMagic;

                TranslationOptions.skipDeadlockChecks = skipDeadlockChecks;

+               TranslationOptions.skipTermination = skipTermination;

                val bplProg = translator.translateProgram(prog);

                // write to out.bpl

                Boogie.vsMode = vsMode;

@@ -130,8 +145,8 @@ object Chalice {
    writer.close();

  }

 

- def CommandLineError(msg: String) = {

+ def CommandLineError(msg: String, help: String) = {

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

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

- }

+   Console.err.println(help);

+ }   

 }

diff --git a/Chalice/src/ChaliceToCSharp.scala b/Chalice/src/ChaliceToCSharp.scala
index f759831b..0c35bd5b 100644
--- a/Chalice/src/ChaliceToCSharp.scala
+++ b/Chalice/src/ChaliceToCSharp.scala
@@ -98,7 +98,10 @@ class ChaliceToCSharp {
   def convertStatement(statement: Statement): String = {

     statement match {

       case Assert(e) => indent + "// assert" + nl

-      case Assume(e) => indent + "assert " + convertExpression(e) + ";" // todo: what if e contains old, result, ...

+      case Assume(e) => indent + {e match {

+        case BoolLiteral(false) => "assert false;" + nl // abort since we made a wrong choice...

+        case _ => // TODO: what to do with assume expressions that contain old, result, ghost variables, etc.

+          "// assume" + nl}}

       case BlockStmt(ss) => indent + "{" + nl + (indentMore { rep(ss map convertStatement) }) + indent + "}" + nl

       case IfStmt(guard, thn, els) => indent + "if (" + convertExpression(guard) + ")" + nl + convertStatement(thn) + 

         (if(els.isDefined) (indent + "else" + nl + convertStatement(els.get)) else { "" }) + nl

diff --git a/Chalice/src/Prelude.scala b/Chalice/src/Prelude.scala
index 2fb58697..b4994889 100644
--- a/Chalice/src/Prelude.scala
+++ b/Chalice/src/Prelude.scala
@@ -101,10 +101,18 @@ function IsGoodInhaleState(ih: HeapType, h: HeapType,
   (forall o: ref :: { h[o, rdheld] }  h[o, rdheld] ==> ih[o, mu] == h[o, mu])

 }

 

+// ---------------------------------------------------------------

+// -- If then else -----------------------------------------------

+// ---------------------------------------------------------------

+

 function ite<T>(bool, T, T) returns (T);

 axiom (forall<T> con: bool, a: T, b: T :: {ite(con, a, b)} con ==> ite(con, a, b) == a);

 axiom (forall<T> con: bool, a: T, b: T :: {ite(con, a, b)} ! con ==> ite(con, a, b) == b);

 

+// ---------------------------------------------------------------

+// -- Axiomatization of sequences --------------------------------

+// ---------------------------------------------------------------

+

 type Seq T;

 

 function Seq#Length<T>(Seq T) returns (int);

@@ -182,7 +190,7 @@ axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) }
   0 <= n ==>

     (n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) &&

     (Seq#Length(s) < n ==> Seq#Length(Seq#Take(s,n)) == Seq#Length(s)));

-axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) }

+axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) } {:weight 25}

   0 <= j && j < n && j < Seq#Length(s) ==>

     Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j));

 

@@ -191,15 +199,24 @@ axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) }
   0 <= n ==>

     (n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) &&

     (Seq#Length(s) < n ==> Seq#Length(Seq#Drop(s,n)) == 0));

-axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) }

+axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) } {:weight 25}

   0 <= n && 0 <= j && j < Seq#Length(s)-n ==>

     Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, j+n));

 

+axiom (forall<T> s, t: Seq T ::

+  { Seq#Append(s, t) }

+  Seq#Take(Seq#Append(s, t), Seq#Length(s)) == s &&

+  Seq#Drop(Seq#Append(s, t), Seq#Length(s)) == t);

+

 function Seq#Range(min: int, max: int) returns (Seq int);

 

 axiom (forall min: int, max: int :: { Seq#Length(Seq#Range(min, max)) } (min < max ==> Seq#Length(Seq#Range(min, max)) == max-min) && (max <= min ==> Seq#Length(Seq#Range(min, max)) == 0));

 axiom (forall min: int, max: int, j: int :: { Seq#Index(Seq#Range(min, max), j) } 0<=j && j<max-min ==> Seq#Index(Seq#Range(min, max), j) == min + j);

 

+// ---------------------------------------------------------------

+// -- Permissions ------------------------------------------------

+// ---------------------------------------------------------------

+

 axiom (forall h: HeapType, m: MaskType, o: ref, q: ref :: {wf(h, m), h[o, mu], h[q, mu]} wf(h, m) && o!=q && (0 < h[o, held] || h[o, rdheld]) && (0 < h[q, held] || h[q, rdheld]) ==> h[o, mu] != h[q, mu]);

 

 function DecPerm<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);

diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index af068b23..82e7658c 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -41,19 +41,22 @@ object PrintProgram {
       print("  condition " + id)

       optE match {

         case None =>

-        case Some(e) => print(" where " + Expr(e))

+        case Some(e) => print(" where "); Expr(e)

       }

       println(Semi)

     case Predicate(id, definition) =>

-      println("  predicate " + id + "  { " + Expr(definition) + "}")

+      print("  predicate " + id + " { "); Expr(definition); println(" }")

     case Function(id, ins, out, specs, e) =>

-      print("  function " + id + "(" + VarList(ins) + ")" + ": " + out.id);

+      print("  function " + id + "("); VarList(ins); print("): " + out.FullName);

+      println

       specs foreach {

         case Precondition(e) => print("    requires "); Expr(e); println(Semi)

         case Postcondition(e) => print("    ensures "); Expr(e); println(Semi)

         case LockChange(ee) => print("    lockchange "); ExprList(ee); println(Semi)

       }

-      print("  { " + Expr(e) + "}");

+      print("  { ");

+      Expr(e);

+      println(" }");

   }

   def Stmt(s: Statement, indent: Int): Unit = s match {

     case Assert(e) =>

diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index 91bc1ede..c14b68c8 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -214,9 +214,8 @@ object Resolver {
      ResolveExpr(e, context, true, true)(false)

      if (!e.typ.IsBool) context.Error(e.pos, "assert statement requires a boolean expression (found " + e.typ.FullName + ")")

    case Assume(e) =>

-     ResolveExpr(e, context, false, false)(false)  // assume expressions remain at run-time, so OLD is not allowed

+     ResolveExpr(e, context, true, true)(false)  

      if (!e.typ.IsBool) context.Error(e.pos, "assume statement requires a boolean expression (found " + e.typ.FullName + ")")

-     CheckNoGhost(e, context)

    case BlockStmt(ss) =>

      var ctx = context

      for (s <- ss) s match {

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index e5a59385..ff840986 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -20,6 +20,7 @@ object TranslationOptions {
   var checkLeaks = false: Boolean;

   var autoMagic = false: Boolean;

   var skipDeadlockChecks = false: Boolean;

+  var skipTermination = false: Boolean;

 }

 

 class Translator {

@@ -124,7 +125,7 @@ class Translator {
 

   def translateFunction(f: Function): List[Decl] = {

     val myresult = BVar("result", f.out.typ);

-    etran.checkTermination = true;

+    etran.checkTermination = !skipTermination;

     val checkBody = isDefined(f.definition);

     etran.checkTermination = false;

     // Boogie function that represents the Chalice function

@@ -1110,7 +1111,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
   val Mask = globals(1);

   val Credits = globals(2);

   lazy val oldEtran = new ExpressionTranslator(preGlobals, preGlobals, currentClass)

-  var checkTermination = false; // check that heap required by callee is strictly smaller than heap required by caller

+  var checkTermination = false; 

 

   def this(globals: List[Boogie.Expr], cl: Class) = this(globals, globals map (g => Boogie.Old(g)), cl)

   def this(cl: Class) = this(for ((id,t) <- S_ExpressionTranslator.Globals) yield Boogie.VarExpr(id), cl)