Chalice: adding support for sequence local variables; removed ClassType from Boogie since it was maskng bad job done by Translator; fixing warnings in case we ever decide to switch to newer Scala compiler

6 files changed, 39 insertions, 40 deletions

diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 065c03ff..48990ce9 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -12,6 +12,7 @@ trait ASTNode extends Positional
 

 case class TopLevelDecl(id: String) extends ASTNode

 

+// this is in fact root of type hierarchy (confusingly, called "class")

 sealed case class Class(classId: String, parameters: List[Class], module: String, members: List[Member]) extends TopLevelDecl(classId) {

   var mm = Map[String,Member]()

   def LookupMember(id: String): Option[Member] = {

diff --git a/Chalice/src/Boogie.scala b/Chalice/src/Boogie.scala
index 9d290aa5..7578a92c 100644
--- a/Chalice/src/Boogie.scala
+++ b/Chalice/src/Boogie.scala
@@ -18,7 +18,6 @@ object Boogie {
 

  sealed abstract class BType

  case class NamedType(s: String) extends BType

- case class ClassType(cl: Class) extends BType

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

 

  sealed abstract class Stmt {

@@ -68,9 +67,9 @@ object Boogie {
    def select(e: Expr, f: Expr) = new MapSelect(this, e, PrintExpr(f))

    def store(e: Expr, f: Expr, rhs: Expr) = MapUpdate(this, e, PrintExpr(f), rhs)

  }

- case class IntLiteral(n: int) extends Expr

+ case class IntLiteral(n: Int) extends Expr

  case class BoolLiteral(b: Boolean) extends Expr

- case class Null extends Expr

+ case class Null() extends Expr

  case class VarExpr(id: String) extends Expr {

    def this(v: BVar) = this(v.id)

  }

@@ -138,7 +137,7 @@ object Boogie {
  // def out(s: String) = Console.out.print(s)

  var indentLevel = 1

  def indent: String = {

-   def doIndent(i: int): String = {

+   def doIndent(i: Int): String = {

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

    }

    doIndent(indentLevel);

@@ -161,10 +160,6 @@ object Boogie {
  def PrintType(t: BType): String = t match {

    case nt@ NamedType(s) =>

      s

-   case ClassType(cl) =>

-     if (cl.IsRef) "ref"

-     else if (cl.IsSeq) "Seq " + cl.parameters(0).id

-     else cl.id

    case IndexedType(id,t) =>

      id + " (" + PrintType(t) + ")"

  }

diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index 123ead89..cc82cacf 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -409,7 +409,8 @@ class Parser extends StandardTokenParsers {
     | "acquire" ^^^ "acquire"

     | "release" ^^^ "release"

     | "fork" ^^^ "fork"

-    | "*" ^^^ "*")

+    | "*" ^^^ "*"

+    )

 

   def atom : Parser[Expression] =

     positioned(

diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index 84d4df31..ef775b2a 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -55,7 +55,7 @@ object PrintProgram {
       }

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

   }

-  def Stmt(s: Statement, indent: int): unit = s match {

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

     case Assert(e) =>

       print("assert "); Expr(e); println(Semi)

     case Assume(e) =>

@@ -168,7 +168,7 @@ object PrintProgram {
       print(" between "); ExprList(lower); print(" and "); ExprList(upper)

     }

   }

-  def PrintBlockStmt(ss: List[Statement], indent: int) = {

+  def PrintBlockStmt(ss: List[Statement], indent: Int) = {

     println("{")

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

     Spaces(indent);  print("}")

@@ -177,7 +177,7 @@ object PrintProgram {
     case Nil =>

     case v :: rest =>

       print(v.id + ": " + v.t.id)

-      rest foreach { v => print(", " + v.id + ": " + v.t.id) }

+      rest foreach { v  => print(", " + v.id + ": " + v.t.id) }

   }

   def ExprList(ee: List[Expression]) = ee match {

     case Nil =>

@@ -195,7 +195,7 @@ object PrintProgram {
     case e: Expression => Expr(e)

   }

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

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

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

     case IntLiteral(n) => print(n)

     case BoolLiteral(b) => print(b)

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

@@ -293,17 +293,17 @@ object PrintProgram {
           case CallState(token, obj, id, args) => Expr(token); print(".joinable"); print(", "); Expr(obj); print("." + id + "("); ExprList(args); print(")"); 

         }); print(", "); Expr(e); print(")"); 

   }

-  def MemberSelect(e: Expression, f: String, contextBindingPower: int, fragileContext: Boolean) = e match {

+  def MemberSelect(e: Expression, f: String, contextBindingPower: Int, fragileContext: Boolean) = e match {

     case e:ImplicitThisExpr => print(f)

     case _ =>

       ParenExpr(0x90, contextBindingPower, fragileContext, { Expr(e,0x90,false); print("." + f) })

   }

-  def BinExpr(bin: BinaryExpr, op: String, power: int, fragileLeft: Boolean, fragileRight: Boolean,

-              context: int, fragileContext: Boolean) = {

+  def BinExpr(bin: BinaryExpr, op: String, power: Int, fragileLeft: Boolean, fragileRight: Boolean,

+              context: Int, fragileContext: Boolean) = {

     ParenExpr(power, context, fragileContext,

           { Expr(bin.E0, power, fragileLeft); print(" " + op + " "); Expr(bin.E1, power, fragileRight) })

   }

-  def ParenExpr(power: int, context: int, fragileContext: Boolean, pe: =>Unit) {

+  def ParenExpr(power: Int, context: Int, fragileContext: Boolean, pe: =>Unit) {

     val ap = power & 0xF0;

     val cp = context & 0xF0;

     val parensNeeded = ap < cp || (ap == cp && (power != context || fragileContext));

@@ -311,7 +311,7 @@ object PrintProgram {
     pe

     if (parensNeeded) { print(")") }

   }

-  def Spaces(N: int) = {

+  def Spaces(N: Int) = {

     val abunchaSpaces = "          "

     var n = N

     while (abunchaSpaces.length <= n) {

diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index 73b248e3..d2f4d0f2 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -18,9 +18,9 @@ object Resolver {
    val CurrentClass = currentClass

    var currentMember = null: Member;

    def CurrentMember = currentMember: Member;  

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

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

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

-     errors = errors + (pos, msg)

+     errors = errors ::: List((pos, msg))

    }

    def AddVariable(v: Variable): ProgramContext = {

      new LProgramContext(v, this);

@@ -497,7 +497,7 @@ object Resolver {
    for (((declareLocal, actual), formal) <- declaresLocal zip actuals zip formals) {

      if (declareLocal) {

        val local = new Variable(actual.id, new Type(formal.t.typ))

-       locals = locals + local

+       locals = locals ::: List(local)

        ResolveType(local.t, ctx)

        actual.Resolve(local)

        vars = vars + actual.v

@@ -795,7 +795,7 @@ object Resolver {
        q.Is foreach { i =>

          val variable = new Variable(i, new Type(elementType));

          bodyContext = bodyContext.AddVariable(variable);

-         bvariables = bvariables + variable;

+         bvariables = bvariables ::: List(variable);

        }

        ResolveExpr(q.E, bodyContext, twoStateContext, true);

        if(! q.E.typ.IsBool) context.Error(q.E.pos, "Body of quantification must be a boolean. (found: " +  q.E.typ.FullName + ").");

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index c4934a43..43cf1b35 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -117,17 +117,17 @@ class Translator {
   }

 

   def translateField(f: Field): List[Decl] = {

-    Const(f.FullName, true, FieldType(f.typ)) ::

+    Const(f.FullName, true, FieldType(f.typ.typ)) ::

     Axiom(NonPredicateField(f.FullName))

   }

 

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

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

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

     etran.checkTermination = true;

     val checkBody = isDefined(f.definition);

     etran.checkTermination = false;

     // Boogie function that represents the Chalice function

-    Boogie.Function(functionName(f), BVar("heap", theap) :: Boogie.BVar("mask", tmask) :: Boogie.BVar("this", tref) :: (f.ins map Variable2BVar), new Boogie.BVar("$myresult", Boogie.ClassType(f.out.typ))) ::

+    Boogie.Function(functionName(f), BVar("heap", theap) :: Boogie.BVar("mask", tmask) :: Boogie.BVar("this", tref) :: (f.ins map Variable2BVar), new Boogie.BVar("$myresult", f.out.typ)) ::

     // check definedness of the function's precondition and body

     Proc(f.FullName + "$checkDefinedness", 

       NewBVarWhere("this", new Type(currentClass)) :: (f.ins map {i => Variable2BVarWhere(i)}),

@@ -183,7 +183,7 @@ class Translator {
     val args = VarExpr("this") :: inArgs;

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

     val applyFrameFunction = FunctionApp(frameFunctionName, version :: args);

-    Boogie.Function("##" + f.FullName, Boogie.BVar("state", theap) :: Boogie.BVar("this", tref) :: (f.ins map Variable2BVar), new BVar("$myresult", f.out)) ::

+    Boogie.Function("##" + f.FullName, Boogie.BVar("state", theap) :: Boogie.BVar("this", tref) :: (f.ins map Variable2BVar), new BVar("$myresult", f.out.typ)) ::

     Axiom(new Boogie.Forall(

       BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar),

       List(applyF),

@@ -200,7 +200,7 @@ class Translator {
     */

     val version = Version(Preconditions(f.spec).foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b) }), etran);

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

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

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

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

     val applyF = FunctionApp(functionName(f), List(VarExpr(HeapName), VarExpr(MaskName)) ::: args)

     //postcondition axioms

@@ -361,7 +361,7 @@ class Translator {
         statements ::: etran.Heap.store(target, lhs.f, toStore) :: bassume(wf(VarExpr(HeapName), VarExpr(MaskName)))

       case lv @ LocalVar(id, t, const, ghost, rhs) =>

         val bv = Variable2BVarWhere(lv.v)

-        val isAssignedVar = if (const) new Boogie.BVar("assigned$" + bv.id, Boogie.ClassType(BoolClass)) else null

+        val isAssignedVar = if (const) new Boogie.BVar("assigned$" + bv.id, BoolClass) else null

         Comment("local " + (if (ghost) "ghost " else "") + (if (const) "const " else "var ") + id) ::

         BLocal(bv) :: 

         { if (const)

@@ -683,7 +683,7 @@ class Translator {
   }

 

   def translateAllocation(cl: Class, initialization: List[Init], lowerBounds: List[Expression], upperBounds: List[Expression], pos: Position): (Boogie.BVar, List[Boogie.Stmt]) = {

-    val (nw, nwe) = NewBVar("nw", Boogie.ClassType(cl), true)

+    val (nw, nwe) = NewBVar("nw", cl, true)

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

     val f = new Boogie.BVar("f", FieldType(tt))

     (nw,

@@ -708,7 +708,7 @@ class Translator {
 

   def TrAcquire(s: Statement, nonNullObj: Expression) = {

     val o = TrExpr(nonNullObj);

-    val (lastAcquireVar, lastAcquire) = Boogie.NewBVar("lastAcquire", Boogie.ClassType(IntClass), true)

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

@@ -1010,8 +1010,8 @@ class Translator {
                   ((exceptions :\ b) ((e,ll) => ll || (lk ==@ e))))

   }

   def LockHavoc(locks: List[Boogie.Expr], etran: ExpressionTranslator) = {

-    val (heldV, held) = NewBVar("isHeld", Boogie.ClassType(IntClass), true)

-    val (rdheldV, rdheld) = NewBVar("isRdHeld", Boogie.ClassType(BoolClass), true)

+    val (heldV, held) = NewBVar("isHeld", IntClass, true)

+    val (rdheldV, rdheld) = NewBVar("isRdHeld", BoolClass, true)

     BLocal(heldV) :: BLocal(rdheldV) ::

     List.flatten (for (o <- locks) yield {  // todo: somewhere we should worry about Df(l)

       Havoc(held) :: Havoc(rdheld) ::

@@ -2001,8 +2001,7 @@ object TranslationHelper {
   implicit def bool2Bool(b: Boolean): Boogie.BoolLiteral = Boogie.BoolLiteral(b)

   implicit def int2Int(n: Int): Boogie.IntLiteral = Boogie.IntLiteral(n)

   implicit def lift(s: Boogie.Stmt): List[Boogie.Stmt] = List(s)

-  implicit def type2BType(tp: Type): BType = {

-    val cl = tp.typ;

+  implicit def type2BType(cl: Class): BType = {

     if(cl.IsRef) {

       tref

     } else if(cl.IsBool) {

@@ -2012,9 +2011,9 @@ object TranslationHelper {
     } else if(cl.IsInt) {

       tint

     } else if(cl.IsSeq) {

-      tseq(type2BType(new Type(cl.asInstanceOf[SeqClass].parameter)))

+      tseq(type2BType(cl.asInstanceOf[SeqClass].parameter))

     } else {

-      assert(false); null

+      assert(false, "unexpectected type: " + cl.FullName); null

     }

   }

   implicit def decl2DeclList(decl: Decl): List[Decl] = List(decl)

@@ -2026,10 +2025,10 @@ object TranslationHelper {
     }

   }

 

-  def Variable2BVar(v: Variable) = new Boogie.BVar(v.UniqueName, Boogie.ClassType(v.t.typ))

+  def Variable2BVar(v: Variable) = new Boogie.BVar(v.UniqueName, v.t.typ)

   def Variable2BVarWhere(v: Variable) = NewBVarWhere(v.UniqueName, v.t)

   def NewBVarWhere(id: String, tp: Type) = {

-    new Boogie.BVar(id, Boogie.ClassType(tp.typ)){

+    new Boogie.BVar(id, tp.typ){

       override val where = TypeInformation(new Boogie.VarExpr(id), tp) }

   }

 

@@ -2105,6 +2104,7 @@ object TranslationHelper {
       case e => Boogie.VarExpr("nostate")

     }

   }

+  /* Unused code that would fail for a nontrivial class  

   def FieldTp(f: Field): String = {

     f match {

       case SpecialField("mu", _) => "Mu"

@@ -2123,6 +2123,7 @@ object TranslationHelper {
       case _ => if(tp.IsSeq) "seq" else "ref"

     }

   }

+ */

   def Preconditions(spec: List[Specification]): List[Expression] = {

     val result = spec flatMap ( s => s match {

       case Precondition(e) => List(e)

@@ -2293,8 +2294,9 @@ object TranslationHelper {
             case Some(e) => e;

             case None => e;

           }

-        case e: VariableExpr => 

-          for ((v,x) <- sub if v == e.v) { return x }

+        case e: VariableExpr =>

+          // TODO: this will update the value of x many times

+          for ((v,x) <- sub if v == e.v) { x.pos = v.pos; return x }

           e

         case q : Quantification =>

           // would be better if this is a part of manipulate method