Chalice: turn asserts into assumes for method refinements (use -noFreeAssume to disable)

5 files changed, 154 insertions, 133 deletions

diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 464840c5..23d6356d 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -164,14 +164,14 @@ case class Function(id: String, ins: List[Variable], out: Type, spec: List[Speci
 case class Condition(id: String, where: Option[Expression]) extends NamedMember(id)

 case class Variable(id: String, t: Type, isGhost: Boolean, isImmutable: Boolean) extends ASTNode {

   val UniqueName = {

-    val n = Variable.VariableCount

-    Variable.VariableCount = Variable.VariableCount + 1

+    val n = S_Variable.VariableCount

+    S_Variable.VariableCount = S_Variable.VariableCount + 1

     id + "#" + n

   }

   def this(name: String, typ: Type) = this(name,typ,false,false);

   override def toString = (if (isGhost) "ghost " else "") + (if (isImmutable) "const " else "var ") + id;

 }

-object Variable { var VariableCount = 0 }

+object S_Variable { var VariableCount = 0 }

 case class SpecialVariable(name: String, typ: Type) extends Variable(name, typ, false, false) {

   override val UniqueName = name

 }

diff --git a/Chalice/src/Boogie.scala b/Chalice/src/Boogie.scala
index 5e3206c1..4fa21be0 100644
--- a/Chalice/src/Boogie.scala
+++ b/Chalice/src/Boogie.scala
@@ -21,8 +21,10 @@ object Boogie {
  case class NamedType(s: String) extends BType

  case class IndexedType(id: String, t: BType) extends BType

 

+ case class Tag(s: String)

  sealed abstract class Stmt {

    def Locals = List[BVar]()

+   var tags: List[Tag] = Nil

  }

  case class Comment(comment: String) extends Stmt

  case class Assert(e: Expr) extends Stmt {

@@ -113,15 +115,15 @@ object Boogie {
  case class BVar(id: String, t: BType) {

    def this(id: String, t: BType, uniquifyName: Boolean) =

      this(if (uniquifyName) {

-            val n = BVar.VariableCount

-            BVar.VariableCount = BVar.VariableCount + 1

+            val n = S_BVar.VariableCount

+            S_BVar.VariableCount = S_BVar.VariableCount + 1

             id + "#_" + n

           } else {

             id

           }, t)

    val where: Expr = null

  }

- object BVar { var VariableCount = 0 }

+ object S_BVar { var VariableCount = 0 }

  def NewBVar(id: String, t: BType, uniquifyName: Boolean) = {

    val v = new Boogie.BVar(id, t, uniquifyName)

    val e = new Boogie.VarExpr(v)

@@ -130,25 +132,23 @@ object Boogie {
  case class TVar(id: String) {

    def this(id: String, uniquifyName: Boolean) =

      this(if (uniquifyName) {

-            val n = TVar.VariableCount

-            TVar.VariableCount = TVar.VariableCount + 1

+            val n = S_TVar.VariableCount

+            S_TVar.VariableCount = S_TVar.VariableCount + 1

             id + "#_" + n

           } else {

             id

           })

    val where: Expr = null

  }

- object TVar { var VariableCount = 0 }

+ object S_TVar { var VariableCount = 0 }

  def NewTVar(id: String) = {

    val v = new Boogie.TVar(id, true)

    val e = new Boogie.NamedType(v.id)

    (v,e)

  }

 

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

-

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

- var indentLevel = 1

+ private var indentLevel = 1

  def indent: String = {

    def doIndent(i: Int): String = {

      if(i==0) { "" } else { "  " + doIndent(i-1) }

@@ -163,7 +163,7 @@ object Boogie {
    indentLevel = prev

    result

  }

- def nl = System.getProperty("line.separator");

+ private val nl = System.getProperty("line.separator");

  

  def Print[T](list: List[T], sep: String, p: T => String): String = list match {

    case Nil => ""

@@ -207,7 +207,7 @@ object Boogie {
  def PrintStmt(s: Stmt): String = s match {

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

    case assert@Assert(e) =>

-     val pos = if (vsMode) {

+     val pos = if (Chalice.vsMode) {

        val r = assert.pos.line - 1;

        val c = assert.pos.column - 1;

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

diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala
index 0ced872e..43b3a330 100644
--- a/Chalice/src/Chalice.scala
+++ b/Chalice/src/Chalice.scala
@@ -12,12 +12,32 @@ 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"

-   val inputs = new ListBuffer[String]()

-   var printProgram = false

-   var vsMode = false;

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

+  /**

+   * Reporting options

+   */

+  private[chalice] var vsMode = false;

+

+  /**

+   * Translation options

+   */

+  // level 0 or below: no defaults

+  // level 1: unfold predicates with receiver this in pre and postconditions

+  // level 2: unfold predicates and functions with receiver this in pre and postconditions

+  // level 3 or above: level 2 + autoMagic\

+  private[chalice] var defaults = 0: Int;

+  private[chalice] var autoFold = false: Boolean;

+  private[chalice] var checkLeaks = false: Boolean;

+  private[chalice] var autoMagic = false: Boolean;

+  private[chalice] var skipDeadlockChecks = false: Boolean;

+  private[chalice] var skipTermination = false: Boolean;

+  private[chalice] var noFreeAssume = false: Boolean;

+

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

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

+    val inputs = new ListBuffer[String]()

+    var printProgram = false

+

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

      if (vsMode) {

        val r = pos.line - 1;

        val c = pos.column - 1;

@@ -25,43 +45,34 @@ object Chalice {
      } else {

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

      }

-   }

-   var doTypecheck = true

-   var doTranslate = true

-   var checkLeaks = false

-   // level 0 or below: no defaults

-   // level 1: unfold predicates with receiver this in pre and postconditions

-   // level 2: unfold predicates and functions with receiver this in pre and postconditions

-   // level 3 or above: level 2 + autoMagic

-   var defaults = 0

-   var autoFold = false

-   var autoMagic = false

-   var skipDeadlockChecks = false

-   var skipTermination = false;

-   var boogieArgs = " ";

-   var gen = false;

+    }

+    var doTypecheck = true

+    var doTranslate = true

+    var boogieArgs = " ";

+    var gen = false;

 

-   // closures should be idempotent

-   val options = Map(

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

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

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

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

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

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

-   )

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

-   " [-boogie:path]" +

-   " [-defaults:int]" +

-   " [<boogie option>]*" +

-   " <file.chalice>*";

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

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

+    )

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

+    " [-boogie:path]" +

+    " [-defaults:int]" +

+    " <boogie option>*" +

+    " <file.chalice>*";

 

-   for (a <- args) {

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

@@ -73,29 +84,30 @@ object Chalice {
      }

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

      else inputs += a

-   }

+    }

 

-   // check that input files exist

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

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

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

+       return

      }

      file;

-   }

+    }

 

-   // parse programs

-   val parser = new Parser();

-   val parseResults = if (files.isEmpty) {

+    // parse programs

+    val parser = new Parser();

+    val parseResults = if (files.isEmpty) {

      List(parser.parseStdin)

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

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

+    }

+

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

@@ -106,11 +118,11 @@ object Chalice {
      case parser.Success(prog, _) =>

        if (printProgram) PrintProgram.P(prog)

        prog

-   }).flatten;

-   if (parseErrors) return;

+    }).flatten;

+    if (parseErrors) return;

 

-   // typecheck program   

-   if (doTypecheck) {

+    // typecheck program

+    if (doTypecheck) {

      Resolver.Resolve(program) match {

        case Resolver.Errors(msgs) =>

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

@@ -128,16 +140,8 @@ object Chalice {
            }

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

@@ -179,19 +183,19 @@ object Chalice {
              writeFile("out.cs", converter.convertProgram(program));

            }

          }

-     }   

-   }

- }

+     }

+    }

+  }

 

- def writeFile(filename: String, text: String) {

+  def writeFile(filename: String, text: String) {

    val writer = new FileWriter(new File(filename));

    writer.write(text);

    writer.flush();

    writer.close();

- }

+  }

 

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

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

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

    Console.err.println(help);

- }   

+  }

 }

diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index 5c955d01..2802e7b8 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -75,8 +75,9 @@ object PrintProgram {
     case BlockStmt(ss) =>

       PrintBlockStmt(ss, indent); println

     case RefinementBlock(ss, old) =>

-      println("// begin of refinement block")

-      for (s <- old) {Spaces(indent); print("// "); Stmt(s, indent)}

+      println("/* begin of refinement block")

+      for (s <- old) {Spaces(indent); Stmt(s, indent)}

+      Spaces(indent); println("end of abstract code */")

       for (s <- ss) {Spaces(indent); Stmt(s, indent)}

       Spaces(indent); println("// end of refinement block")

     case IfStmt(guard, BlockStmt(thn), els) =>

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index c1c36cb5..e6c3db7b 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -14,20 +14,8 @@ import Boogie.Proc, Boogie.NamedType, Boogie.NewBVar, Boogie.Havoc, Boogie.Stmt,
 

 case class ErrorMessage(pos: Position, message: String)

 

-object TranslationOptions {

-  // note: the initial values should match those Chalice.scala

-

-  var defaults = 0: Int;

-  var autoFold = false: Boolean;

-  var checkLeaks = false: Boolean;

-  var autoMagic = false: Boolean;

-  var skipDeadlockChecks = false: Boolean;

-  var skipTermination = false: Boolean;

-}

-

 class Translator {

   import TranslationHelper._;

-  import TranslationOptions._;

   var currentClass = null: Class;

   var modules = Nil: List[String]

   var etran = new ExpressionTranslator(null);

@@ -103,7 +91,7 @@ class Translator {
         Havoc(etran.Heap) ::

         // check that invariant is well-defined

         etran.WhereOldIs(h1, m1, c1).Inhale(invs map { mi => mi.e}, "monitor invariant", true) :::

-        (if (!checkLeaks || invs.length == 0) Nil else

+        (if (! Chalice.checkLeaks || invs.length == 0) Nil else

           // check that there are no loops among .mu permissions in monitors

           // !CanWrite[this,mu]

           bassert(!etran.CanWrite(VarExpr("this"), "mu"), invs(0).pos, "Monitor invariant is not allowed to hold write permission to this.mu") ::

@@ -130,7 +118,7 @@ class Translator {
 

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

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

-    etran = etran.CheckTermination(!skipTermination);

+    etran = etran.CheckTermination(! Chalice.skipTermination);

     val checkBody = f.definition match {case Some(e) => isDefined(e); case None => Nil};

     etran = etran.CheckTermination(false);

     // Boogie function that represents the Chalice function

@@ -143,13 +131,13 @@ class Translator {
       DefaultPrecondition(),

       DefinePreInitialState :::

       // check definedness of the precondition

-      InhaleWithChecking(Preconditions(f.spec) map { p => (if(0<defaults) UnfoldPredicatesWithReceiverThis(p) else p)}, "precondition") :::

+      InhaleWithChecking(Preconditions(f.spec) map { p => (if(0 < Chalice.defaults) UnfoldPredicatesWithReceiverThis(p) else p)}, "precondition") :::

       bassume(CurrentModule ==@ VarExpr(ModuleName(currentClass))) :: // verify the body assuming that you are in the module

       // check definedness of function body

       checkBody :::

       (f.definition match {case Some(e) => BLocal(myresult) :: (Boogie.VarExpr("result") := etran.Tr(e)); case None => Nil}) :::

       // check that postcondition holds

-      ExhaleWithChecking(Postconditions(f.spec) map { post => ((if(0<defaults) UnfoldPredicatesWithReceiverThis(post) else post),

+      ExhaleWithChecking(Postconditions(f.spec) map { post => ((if(0 < Chalice.defaults) UnfoldPredicatesWithReceiverThis(post) else post),

               ErrorMessage(f.pos, "Postcondition at " + post.pos + " might not hold."))}, "function postcondition")) ::

     // definition axiom

     (if (f.definition.isDefined) definitionAxiom(f) else Nil) :::

@@ -322,11 +310,11 @@ class Translator {
         bassume(CurrentModule ==@ Boogie.VarExpr(ModuleName(currentClass))) ::

         bassume(CanAssumeFunctionDefs) ::

         DefinePreInitialState :::

-        Inhale(Preconditions(method.spec) map { p => (if(0<defaults) UnfoldPredicatesWithReceiverThis(p) else p)}, "precondition") :::

+        Inhale(Preconditions(method.spec) map { p => (if(0 < Chalice.defaults) UnfoldPredicatesWithReceiverThis(p) else p)}, "precondition") :::

         DefineInitialState :::

         translateStatements(method.body) :::

-        Exhale(Postconditions(method.spec) map { p => ((if(0<defaults) UnfoldPredicatesWithReceiverThis(p) else p), ErrorMessage(method.pos, "The postcondition at " + p.pos + " might not hold."))}, "postcondition") :::

-        (if(checkLeaks) isLeaking(method.pos, "Method " + method.FullName + " might leak references.") else Nil) :::

+        Exhale(Postconditions(method.spec) map { p => ((if(0 < Chalice.defaults) UnfoldPredicatesWithReceiverThis(p) else p), ErrorMessage(method.pos, "The postcondition at " + p.pos + " might not hold."))}, "postcondition") :::

+        (if(Chalice.checkLeaks) isLeaking(method.pos, "Method " + method.FullName + " might leak references.") else Nil) :::

         bassert(LockFrame(LockChanges(method.spec), etran), method.pos, "Method might lock/unlock more than allowed.") :::

         bassert(DebtCheck, method.pos, "Method body is not allowed to leave any debt."))

   }

@@ -354,13 +342,18 @@ class Translator {
       mt.Outs map {i => Variable2BVarWhere(i)},

       GlobalNames,

       DefaultPrecondition(),

-        bassume(CurrentModule ==@ Boogie.VarExpr(ModuleName(currentClass))) ::

-        bassume(CanAssumeFunctionDefs) ::

-        DefinePreInitialState :::

-        Inhale(Preconditions(mt.Spec), "precondition") :::

-        DefineInitialState :::

-        translateStatements(mt.Body) :::

-        Exhale(Postconditions(mt.Spec) map { p => (p, ErrorMessage(p.pos, "The postcondition at " + p.pos + " might not hold."))}, "postcondition")

+        assert2assume {

+          bassume(CurrentModule ==@ Boogie.VarExpr(ModuleName(currentClass))) ::

+          bassume(CanAssumeFunctionDefs) ::

+          DefinePreInitialState :::

+          Inhale(Preconditions(mt.Spec), "precondition") :::

+          DefineInitialState :::

+          translateStatements(mt.Body) :::

+          Exhale(Postconditions(mt.refines.Spec) map {p => (p, ErrorMessage(p.pos, "The postcondition at " + p.pos + " might not hold."))}, "postcondition") :::

+          tag(

+            Exhale(Postconditions(mt.spec) map {p => (p, ErrorMessage(p.pos, "The postcondition at " + p.pos + " might not hold."))}, "refinement postcondition"),

+            keepTag)

+        }

       )

   }

 

@@ -826,7 +819,7 @@ class Translator {
     val (lastAcquireVar, lastAcquire) = Boogie.NewBVar("lastAcquire", IntClass, true)

     val (lastSeenHeldV, lastSeenHeld) = Boogie.NewBVar("lastSeenHeld", tint, true)

     val (lastSeenMuV, lastSeenMu) = Boogie.NewBVar("lastSeenMu", tmu, true)

-    (if (skipDeadlockChecks)

+    (if (Chalice.skipDeadlockChecks)

        bassume(CanRead(o, "mu")) ::

        bassume(etran.MaxLockIsBelowX(etran.Heap.select(o,"mu")))

      else

@@ -1065,22 +1058,23 @@ class Translator {
     // run concrete C on the fresh heap

     {

       etran = conTran;

-      Comment("run concrete program") ::

+      Comment("run concrete program:") ::

       translateStatements(r.con)

     } :::

     // run angelically A on the old heap

-    Comment("run abstract program") ::

-    {r.abs match {

+    Comment("run abstract program:") ::

+    { etran = absTran;

+    r.abs match {

       case List(s: SpecStmt) =>

-        etran = absTran;

-        Comment("witness declared local variables") ::

-        (for (v <- duringA) yield BLocal(Variable2BVarWhere(v))) :::

-        (for ((v, w) <- duringA zip duringC) yield (new VariableExpr(v) := new VariableExpr(w))) :::

-        bassert(s.post, r.pos, "Refinement fails to satisfy specification statement post-condition") ::

-        (for ((v, w) <- beforeV zip before; if (! s.lhs.exists(ve => ve.v == w))) yield

-          bassert(new VariableExpr(v) ==@ new VariableExpr(w), r.pos, "Refinement may change a variable not in frame of the specification statement: " + v.id))        

+        tag(

+          Comment("witness declared local variables") ::

+          (for (v <- duringA) yield BLocal(Variable2BVarWhere(v))) :::

+          (for ((v, w) <- duringA zip duringC) yield (new VariableExpr(v) := new VariableExpr(w))) :::

+          bassert(s.post, r.pos, "Refinement fails to satisfy specification statement post-condition") ::

+          (for ((v, w) <- beforeV zip before; if (! s.lhs.exists(ve => ve.v == w))) yield

+             bassert(new VariableExpr(v) ==@ new VariableExpr(w), r.pos, "Refinement may change a variable not in frame of the specification statement: " + v.id)),

+          keepTag)

       case _ =>

-        etran = absTran;

         Comment("save locals after") ::

         (for (v <- afterV) yield BLocal(Variable2BVarWhere(v))) :::

         (for ((v, w) <- afterV zip before) yield (new VariableExpr(v) := new VariableExpr(w))) :::

@@ -1088,13 +1082,15 @@ class Translator {
         (for ((v, w) <- before zip beforeV) yield (new VariableExpr(v) := new VariableExpr(w))) :::

         translateStatements(r.abs) :::

         Comment("assert equality on shared locals") ::

-        (for ((v, w) <- afterV zip before) yield

-          bassert(new VariableExpr(v) ==@ new VariableExpr(w), r.pos, "Refinement may produce different value for pre-state local variable: " + v.id)) :::

-        (for ((v, w) <- duringA zip duringC) yield

-          bassert(new VariableExpr(v) ==@ new VariableExpr(w), r.pos, "Refinement may produce different value for a declared local variable: " + v.id))

+        tag(

+          (for ((v, w) <- afterV zip before) yield

+            bassert(new VariableExpr(v) ==@ new VariableExpr(w), r.pos, "Refinement may produce different value for pre-state local variable: " + v.id)) :::

+          (for ((v, w) <- duringA zip duringC) yield

+            bassert(new VariableExpr(v) ==@ new VariableExpr(w), r.pos, "Refinement may produce different value for a declared local variable: " + v.id)),

+          keepTag)

     }} :::

     Comment("end of refinement block")

-    // TODO: global coupling: assert coupling invariants for locations with positive

+    // TODO: global coupling: assert coupling invariants for locations with positive, preserve permissions?

   }

 

 

@@ -1168,7 +1164,7 @@ class Translator {
   }

 

   def isLeaking(pos: Position, msg: String): List[Boogie.Stmt] = {

-    if(checkLeaks) {

+    if(Chalice.checkLeaks) {

       var o = Boogie.VarExpr("$o");

       var f = "$f";

       val (ttV,tt) = Boogie.NewTVar("T")

@@ -1297,7 +1293,6 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
   assert(preGlobals.size == 3)

 

   import TranslationHelper._

-  import TranslationOptions._

 

   val Heap = globals(0);

   val Mask = globals(1);

@@ -1810,7 +1805,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
                  bassert(nonNull(Tr(e.e)), error.pos, error.message + " The target of the acc predicate at " + acc.pos + " might be null.") else Nil) :::

       BLocal(fractionV) :: (frac := Tr(fraction)) ::

       // if the mask does not contain sufficient permissions, try folding acc(e, fraction)

-      (if(e.isPredicate && autoFold && (perm == Full || canTakeFractionOf(DefinitionOf(e.predicate)))) {

+      (if(e.isPredicate && Chalice.autoFold && (perm == Full || canTakeFractionOf(DefinitionOf(e.predicate)))) {

          val inhaleTran = new ExpressionTranslator(List(Heap, em, Credits), currentClass);

          val sourceVar = new Variable("fraction", new Type(IntClass));

          val bplVar = Variable2BVar(sourceVar);

@@ -1843,7 +1838,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         dfP else Nil) :::

       BLocal(epsilonsV) :: (if(epsilons!=null) (eps := Tr(epsilons)) :: Nil else Nil) :::

       // if the mask does not contain sufficient permissions, try folding rdacc(e, epsilons)

-      (if(e.isPredicate && autoFold && canTakeEpsilonsOf(DefinitionOf(e.predicate)) && epsilons!=null) {

+      (if(e.isPredicate && Chalice.autoFold && canTakeEpsilonsOf(DefinitionOf(e.predicate)) && epsilons!=null) {

           val inhaleTran = new ExpressionTranslator(List(Heap, em, Credits), currentClass);

           val sourceVar = new Variable("epsilons", new Type(IntClass));

           val bplVar = Variable2BVar(sourceVar);

@@ -2198,7 +2193,7 @@ object TranslationHelper {
   def PredicateField(f: String) = FunctionApp("PredicateField", List(VarExpr(f)))

   def cast(a: Expr, b: Expr) = FunctionApp("cast", List(a, b))

 

-  // Sequences

+  // sequences

 

   def createEmptySeq = FunctionApp("Seq#Empty", List())

   def createSingletonSeq(e: Expr) = FunctionApp("Seq#Singleton", List(e)) 

@@ -2326,7 +2321,7 @@ object TranslationHelper {
     val result = spec flatMap ( s => s match {

       case Precondition(e) => List(e)

       case _ => Nil });

-    if(autoMagic) {

+    if(Chalice.autoMagic) {

       automagic(result.foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b)}), Nil)._1 ::: result

     } else {

       result

@@ -2336,7 +2331,7 @@ object TranslationHelper {
     val result = spec flatMap ( s => s match {

       case Postcondition(e) => List(e)

       case _ => Nil })

-    if(autoMagic) {

+    if(Chalice.autoMagic) {

       automagic(result.foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b)}), Nil)._1 ::: result

     } else {

       result

@@ -2422,7 +2417,7 @@ object TranslationHelper {
   }

 

   def DefinitionOf(predicate: Predicate): Expression = {

-    if(autoMagic) {

+    if(Chalice.autoMagic) {

       And(automagic(predicate.definition, Nil)._1.foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b)}), predicate.definition)

     } else {

       predicate.definition

@@ -2561,5 +2556,26 @@ object TranslationHelper {
       case _ => None;

     }

   }

+

+  val keepTag = Boogie.Tag("keep")

+  // Assume the only composite statement is If

+  def tag(l: List[Stmt], t: Boogie.Tag):List[Stmt] =

+    for (s <- l) yield {

+      s.tags = t :: s.tags;

+      s match {

+        case Boogie.If(_, thn, els) => tag(thn, t); tag(els, t);

+        case _ => 

+      }

+      s

+    }

+  // Assume the only composite statement is If

+  def assert2assume(l: List[Stmt]):List[Stmt] =

+    if (Chalice.noFreeAssume) l else

+      l flatMap {

+        case Boogie.If(guard, thn, els) => Boogie.If(guard, assert2assume(thn), assert2assume(els))

+        case ba @ Boogie.Assert(e) =>

+          if (ba.tags contains keepTag) ba else Comment(" assert " + ba.pos + ": " + ba.message) :: Boogie.Assume(e)

+        case s => s

+      }

 }

 }