Chalice: introduce BoogieExpr to allow boogie expressions in the Chalice AST

4 files changed, 14 insertions, 5 deletions

diff --git a/Chalice/src/main/scala/Ast.scala b/Chalice/src/main/scala/Ast.scala
index 524bbf60..2c6684e4 100644
--- a/Chalice/src/main/scala/Ast.scala
+++ b/Chalice/src/main/scala/Ast.scala
@@ -208,9 +208,6 @@ case class Variable(id: String, t: Type, isGhost: Boolean, isImmutable: Boolean)
   def this(name: String, typ: Type) = this(name,typ,false,false);

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

 }

-case class BoogieExpr(expr: Boogie.Expr) extends ASTNode {

-  override def toString = "BoogieExpr("+expr+")"

-}

 object S_Variable { var VariableCount = 0 }

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

   override val UniqueName = name

@@ -411,6 +408,10 @@ case class VariableExpr(id: String) extends Expression {
   def this(vr: Variable) = { this(vr.id); v = vr; typ = vr.t.typ }

   def Resolve(vr: Variable) = { v = vr; typ = vr.t.typ }

 }

+// hack to allow boogie expressions in the Chalice AST during transformation

+case class BoogieExpr(expr: Boogie.Expr) extends Expression {

+  override def toString = "BoogieExpr("+expr+")"

+}

 case class Result() extends Expression

 sealed abstract class ThisExpr extends Expression

 case class ExplicitThisExpr() extends ThisExpr {

@@ -757,6 +758,7 @@ object AST {
       case _:ThisExpr => expr

       case _:Result => expr

       case _:VariableExpr => expr

+      case _:BoogieExpr => expr

       case ma@MemberAccess(e, id) =>

         val g = MemberAccess(func(e), id);

         g.f = ma.f;

@@ -855,6 +857,7 @@ object AST {
      case _:ThisExpr => ;

      case _:Result => ;

      case _:VariableExpr => ;

+     case _:BoogieExpr => ;

      case MemberAccess(e, _) =>

        visit(e, f);

 

diff --git a/Chalice/src/main/scala/PrettyPrinter.scala b/Chalice/src/main/scala/PrettyPrinter.scala
index ac9ebd2f..18557b99 100644
--- a/Chalice/src/main/scala/PrettyPrinter.scala
+++ b/Chalice/src/main/scala/PrettyPrinter.scala
@@ -258,6 +258,7 @@ object PrintProgram {
   }

   def Expr(e: Expression): Unit = Expr(e, 0, false)

   def Expr(e: Expression, contextBindingPower: Int, fragileContext: Boolean): Unit = e match {

+    case BoogieExpr(_) => throw new InternalErrorException("unexpected in pretty printer")

     case IntLiteral(n) => print(n)

     case BoolLiteral(b) => print(b)

     case NullLiteral() => print("null")

diff --git a/Chalice/src/main/scala/Resolver.scala b/Chalice/src/main/scala/Resolver.scala
index 3a317330..17bb668e 100644
--- a/Chalice/src/main/scala/Resolver.scala
+++ b/Chalice/src/main/scala/Resolver.scala
@@ -889,6 +889,8 @@ object Resolver {
      mx.typ = MuClass

    case mx:LockBottomLiteral =>

      mx.typ = MuClass

+   case _:BoogieExpr =>

+     throw new InternalErrorException("boogie expression unexpected here")

    case r:Result =>

      assert(context.currentMember!=null);

      r.typ = IntClass

@@ -1226,6 +1228,7 @@ object Resolver {
    case _:VariableExpr =>

    case _:ThisExpr =>

    case _:Result =>

+   case _:BoogieExpr =>

    case MemberAccess(e, id) =>

      CheckRunSpecification(e, context, false)

    case Frac(perm) => CheckRunSpecification(perm, context, false)

diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala
index 07bfa444..22a8820d 100644
--- a/Chalice/src/main/scala/Translator.scala
+++ b/Chalice/src/main/scala/Translator.scala
@@ -1490,6 +1490,7 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
       case LockBottomLiteral() => Nil

       case _:ThisExpr => Nil

       case _:Result => Nil

+      case _:BoogieExpr => Nil

       case _:VariableExpr => Nil

       case fs @ MemberAccess(e, f) =>       

         assert(!fs.isPredicate);

@@ -1652,6 +1653,7 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
       // since there currently are no operations defined on string, except == and !=, just translate

       // each string to a unique number

       s.hashCode()

+    case BoogieExpr(b) => b

     case MaxLockLiteral() => throw new InternalErrorException("waitlevel case should be handled in << and == and !=")

     case LockBottomLiteral() => bLockBottom

     case _:ThisExpr => VarExpr("this")

@@ -1997,7 +1999,7 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
     

     val occasion = "update SecMask ("+fp.receiver+"."+fp.predicate.FullName + ", version "+fp.version+")"

     // asserts are converted to assumes, so error messages do not matter

-    assert2assume(Exhale(SecMask, SecMask, List((definition, ErrorMessage(NoPosition, ""))), occasion, check=false, currentK, exactchecking=false /* it should not important what we pass here */, transferPermissionToSecMask=false, recurseOnPredicates=true))

+    assert2assume(Exhale(SecMask, SecMask, List((definition, ErrorMessage(NoPosition, ""))), occasion, false, currentK, false /* it should not important what we pass here */, false, true))

   }

   /** Most general form of exhale; implements all the specific versions above */

   def Exhale(m: Expr, sm: Expr, predicates: List[(Expression, ErrorMessage)], occasion: String, check: Boolean, currentK: Expr, exactchecking: Boolean, transferPermissionToSecMask: Boolean, recurseOnPredicates: Boolean): List[Boogie.Stmt] = {

@@ -2145,7 +2147,7 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
         bassume(AreGoodMasks(m, sm)) ::

         bassume(wf(Heap, m, sm))

       }

-    case cr@Credit(ch, n) if !onlyExactCheckingPermissions =>

+    case cr@Credit(ch, n) if !onlyExactCheckingPermissions && !recurseOnPredicates =>

       val trCh = Tr(ch)

       (if (check)

          isDefined(ch)(true) :::