diff options
| -rw-r--r-- | Chalice/src/Ast.scala | 24 | ||||
| -rw-r--r-- | Chalice/src/Parser.scala | 38 | ||||
| -rw-r--r-- | Chalice/src/PrettyPrinter.scala | 14 | ||||
| -rw-r--r-- | Chalice/src/Resolver.scala | 14 | ||||
| -rw-r--r-- | Chalice/src/Translator.scala | 41 |
5 files changed, 83 insertions, 48 deletions
diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala index 4f63f57b..570a527c 100644 --- a/Chalice/src/Ast.scala +++ b/Chalice/src/Ast.scala @@ -147,25 +147,23 @@ case class Function(id: String, ins: List[Variable], out: Type, spec: List[Speci var SCC: List[Function] = Nil;
}
case class Condition(id: String, where: Option[Expression]) extends NamedMember(id)
-class Variable(name: String, typ: Type) extends ASTNode {
+class Variable(name: String, typ: Type, isGhost: Boolean, isImmutable: Boolean) extends ASTNode {
val id = name
val t = typ
- val IsGhost: Boolean = false
- val IsImmutable: Boolean = false
+ val IsGhost = isGhost
+ val IsImmutable = isImmutable
val UniqueName = {
val n = Variable.VariableCount
Variable.VariableCount = Variable.VariableCount + 1
name + "#" + 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 }
-class ImmutableVariable(id: String, t: Type) extends Variable(id, t) {
- override val IsImmutable: Boolean = true
-}
-class SpecialVariable(name: String, typ: Type) extends Variable(name, typ) {
+class SpecialVariable(name: String, typ: Type) extends Variable(name, typ, false, false) {
override val UniqueName = name
}
-
sealed abstract class Specification extends ASTNode
case class Precondition(e: Expression) extends Specification
case class Postcondition(e: Expression) extends Specification
@@ -193,19 +191,13 @@ case class WhileStmt(guard: Expression, case class Assign(lhs: VariableExpr, rhs: RValue) extends Statement
case class FieldUpdate(lhs: MemberAccess, rhs: RValue) extends Statement
case class LocalVar(id: String, t: Type, const: Boolean, ghost: Boolean, rhs: Option[RValue]) extends Statement {
- val v =
- if (const)
- new ImmutableVariable(id, t){override val IsGhost = ghost}
- else
- new Variable(id, t){override val IsGhost = ghost}
+ val v = new Variable(id, t, ghost, const);
}
case class Call(declaresLocal: List[Boolean], lhs: List[VariableExpr], obj: Expression, id: String, args: List[Expression]) extends Statement {
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 SpecStmt(lhs: List[VariableExpr], locals:List[Variable], expr: Expression) extends Statement
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
diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala index b57a5ea4..d04746bc 100644 --- a/Chalice/src/Parser.scala +++ b/Chalice/src/Parser.scala @@ -65,8 +65,8 @@ class Parser extends StandardTokenParsers { 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) }
+ ( "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id.v, t, false) }
+ | "ghost" ~> "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id.v, t, true) }
)
def invariantDecl = positioned("invariant" ~> expression <~ Semi ^^ MonitorInvariant)
def methodDecl = {
@@ -95,18 +95,15 @@ class Parser extends StandardTokenParsers { 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)
+ currentLocalVariables = currentLocalVariables + id.v;
+ new Variable(id.v,t,false,immutable)
}
-
def Ident = positioned(ident ^^ PositionedString)
- def idType =
- idTypeOpt ^^ {
+ 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) }
+ 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) }
@@ -138,7 +135,8 @@ class Parser extends StandardTokenParsers { | blockStatement ^^ BlockStmt
| "var" ~> localVarStmt(false, false)
| "const" ~> localVarStmt(true, false)
- | "ghost" ~> ( "const" ~> localVarStmt(true, true) | "var" ~> localVarStmt(false, true))
+ | "ghost" ~> "const" ~> localVarStmt(true, true)
+ | "ghost" ~> "var" ~> localVarStmt(false, true)
| "call" ~> callStmt
| "if" ~> ifStmtThen
| "while" ~> "(" ~> expression ~ ")" ~ loopSpec ~ blockStatement ^^ {
@@ -225,10 +223,20 @@ class Parser extends StandardTokenParsers { Receive(declareImplicitLocals(lhs), e, lhs) }
)
def localVarStmt(const: Boolean, ghost: Boolean) =
- idTypeOpt ~ (":=" ~> Rhs ?) <~ Semi ^^ {
+ ( (rep1sep(idType, ",") into {decls:List[(PositionedString,Type)] => {
+ val locals = for ((id, t) <- decls; if (! currentLocalVariables.contains(id.v))) yield {
+ currentLocalVariables = currentLocalVariables + id.v
+ new Variable(id.v, t, ghost, const)
+ }
+ val lhs = for ((id, _) <- decls) yield {
+ val v = VariableExpr(id.v); v.pos = id.pos; v
+ }
+ "[" ~> expression <~ "]" <~ Semi ^^ {e => SpecStmt(lhs, locals, e)};
+ } })
+ | idTypeOpt ~ (":=" ~> Rhs ?) <~ Semi ^^ {
case (id,optT) ~ rhs =>
- currentLocalVariables = currentLocalVariables + id
- LocalVar(id,
+ currentLocalVariables = currentLocalVariables + id.v
+ LocalVar(id.v,
optT match {
case Some(t) => t
case None =>
@@ -240,8 +248,8 @@ class Parser extends StandardTokenParsers { case _ => Type("int", Nil)
}
},
- const, ghost, rhs)
- }
+ const, ghost, rhs) }
+ )
def ifStmtThen: Parser[IfStmt] =
"(" ~> expression ~ ")" ~ blockStatement ~ ("else" ~> ifStmtElse ?) ^^ {
case guard ~ _ ~ thenClause ~ elseClause => IfStmt(guard, BlockStmt(thenClause), elseClause) }
diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala index 3e8798f4..6f99db2c 100644 --- a/Chalice/src/PrettyPrinter.scala +++ b/Chalice/src/PrettyPrinter.scala @@ -95,6 +95,20 @@ object PrintProgram { print(id + ": " + t.FullName)
rhs match { case None => case Some(rhs) => print(" := "); Rhs(rhs) }
println(Semi)
+ case SpecStmt(lhs, locals, expr) =>
+ if (locals.size > 0) {
+ if (locals(0).IsGhost) print("ghost ");
+ if (locals(0).IsImmutable) print("const ") else print("var ")
+ } else
+ print("var ");
+ VarList(locals);
+ var first = (locals.size == 0);
+ for (l <- lhs)
+ if (! locals.exists(v => v.id == l.id)) {
+ if (first) first = false else print(", ");
+ print(l.id);
+ }
+ print(" ["); Expr(expr); print("]"); println(Semi);
case Call(_, outs, obj, id, args) =>
print("call ")
outs match {
diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala index 7365bfc8..c1740c61 100644 --- a/Chalice/src/Resolver.scala +++ b/Chalice/src/Resolver.scala @@ -6,6 +6,7 @@ package chalice;
import scala.util.parsing.input.Position
import scala.util.parsing.input.Positional
+import collection.mutable.ListBuffer
object Resolver {
sealed abstract class ResolverOutcome
@@ -268,7 +269,15 @@ object Resolver { for (v <- c.locals) { ctx = ctx.AddVariable(v) }
case r: Receive =>
ResolveStmt(r, ctx)
- for (v <- r.locals) { ctx = ctx.AddVariable(v) }
+ for (v <- r.locals) { ctx = ctx.AddVariable(v) }
+ case s: SpecStmt =>
+ for (v <- s.locals) { ResolveType(v.t, ctx); ctx = ctx.AddVariable(v) }
+ for (v <- s.lhs) {
+ ResolveExpr(v, ctx, true, true)(false)
+ if (v.v != null && !s.locals.contains(v.v) && v.v.IsImmutable)
+ context.Error(s.pos, "Immutable variable cannot be updated by a spec statement: " + v.id);
+ }
+ ResolveExpr(s.expr, ctx, true, true)(false)
case s =>
ResolveStmt(s, ctx)
}
@@ -308,7 +317,8 @@ object Resolver { ResolveExpr(rhs, context, false, false)(false)
if (! lhs.isPredicate && !canAssign(lhs.typ, rhs.typ)) context.Error(fu.pos, "type mismatch in assignment, lhs=" + lhs.typ.FullName + " rhs=" + rhs.typ.FullName)
if (! lhs.isPredicate && lhs.f != null && !lhs.f.isGhost) CheckNoGhost(rhs, context)
- case lv:LocalVar => throw new Exception("unexpected LocalVar; should have been handled in BlockStmt above")
+ case _:LocalVar => throw new Exception("unexpected LocalVar; should have been handled in BlockStmt above")
+ case _:SpecStmt => throw new Exception("should have been handled before")
case c @ Call(declaresLocal, lhs, obj, id, args) =>
ResolveExpr(obj, context, false, false)(false)
CheckNoGhost(obj, context)
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index d5ddfdcd..aae392fd 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -390,7 +390,7 @@ class Translator { translateWhile(w)
case Assign(lhs, rhs) =>
def assignOrAssumeEqual(r: Boogie.Expr): List[Boogie.Stmt] = {
- if (lhs.v.isInstanceOf[ImmutableVariable]) {
+ if (lhs.v.IsImmutable) {
// this must be a "ghost const"
val name = lhs.v.UniqueName
bassert(! VarExpr("assigned$" + name), lhs.pos, "Const variable can be assigned to only once.") ::
@@ -423,21 +423,18 @@ class Translator { isDefined(target) :::
bassert(CanWrite(target, lhs.f), s.pos, "Location might not be writable") ::
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, BoolClass) else null
- Comment("local " + (if (ghost) "ghost " else "") + (if (const) "const " else "var ") + id) ::
- BLocal(bv) ::
- { if (const)
- // havoc x; var assigned$x: bool; assigned$x := false;
- Havoc(new Boogie.VarExpr(bv)) ::
- BLocal(isAssignedVar) :: (new Boogie.VarExpr(isAssignedVar) := false)
- else
- List() } :::
- { rhs match {
+ case lv : LocalVar =>
+ translateLocalVarDecl(lv.v, false) :::
+ { lv.rhs match {
//update the local, provided a rhs was provided
- case None => List()
+ case None => Nil
case Some(rhs) => translateStatement(Assign(new VariableExpr(lv.v), rhs)) }}
+ case SpecStmt(lhs, locals, expr) =>
+ locals.flatMap(v => translateLocalVarDecl(v, true)) :::
+ Comment("spec statement") ::
+ lhs.map(l => Boogie.Havoc(l)) :::
+ isDefined(expr) :::
+ bassume(expr)
case c: Call =>
translateCall(c)
case Install(obj, lowerBounds, upperBounds) =>
@@ -756,6 +753,20 @@ class Translator { }
}
+ def translateLocalVarDecl(v: Variable, assignConst: Boolean) = {
+ val bv = Variable2BVarWhere(v)
+ Comment("local " + v) ::
+ BLocal(bv) ::
+ { if (v.IsImmutable) {
+ val isAssignedVar = new Boogie.BVar("assigned$" + bv.id, BoolClass)
+ // havoc x; var assigned$x: bool; assigned$x := false;
+ Havoc(new Boogie.VarExpr(bv)) ::
+ BLocal(isAssignedVar) ::
+ (new Boogie.VarExpr(isAssignedVar) := assignConst)
+ } else
+ Nil }
+ }
+
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", cl, true)
val (ttV,tt) = Boogie.NewTVar("T")
@@ -933,7 +944,7 @@ class Translator { (new VariableExpr(sv) := new VariableExpr(v))) :::
// havoc local-variable loop targets
(w.LoopTargets :\ List[Boogie.Stmt]()) ( (v,vars) => (v match {
- case v: ImmutableVariable => Boogie.Havoc(Boogie.VarExpr("assigned$" + v.id))
+ case v: Variable if v.IsImmutable => Boogie.Havoc(Boogie.VarExpr("assigned$" + v.id))
case _ => Boogie.Havoc(Boogie.VarExpr(v.UniqueName)) }) :: vars) :::
Boogie.If(null,
// 1. CHECK DEFINEDNESS OF INVARIANT
|