diff options
| -rw-r--r-- | Chalice/refinements/Answer | 21 | ||||
| -rw-r--r-- | Chalice/refinements/LoopSqRoot.chalice | 28 | ||||
| -rw-r--r-- | Chalice/refinements/test.sh | 29 | ||||
| -rw-r--r-- | Chalice/src/Ast.scala | 33 | ||||
| -rw-r--r-- | Chalice/src/ChaliceToCSharp.scala | 6 | ||||
| -rw-r--r-- | Chalice/src/Parser.scala | 6 | ||||
| -rw-r--r-- | Chalice/src/PrettyPrinter.scala | 12 | ||||
| -rw-r--r-- | Chalice/src/Resolver.scala | 10 | ||||
| -rw-r--r-- | Chalice/src/Translator.scala | 7 |
9 files changed, 108 insertions, 44 deletions
diff --git a/Chalice/refinements/Answer b/Chalice/refinements/Answer new file mode 100644 index 00000000..52a7d06b --- /dev/null +++ b/Chalice/refinements/Answer @@ -0,0 +1,21 @@ +Processing LoopSqRoot.chalice +
+Boogie program verifier finished with 9 verified, 0 errors
+Processing RecSqRoot.chalice +
+Boogie program verifier finished with 11 verified, 0 errors
+Processing SpecStmt.chalice + 12.5: Assertion might not hold. The expression at 12.12 might not evaluate to true.
+ 25.5: Assertion might not hold. The expression at 25.12 might not evaluate to true.
+ 33.5: Assertion might not hold. The expression at 33.12 might not evaluate to true.
+
+Boogie program verifier finished with 4 verified, 3 errors
+Processing SumCubes.chalice +
+Boogie program verifier finished with 6 verified, 0 errors
+Processing TestTransform.chalice +
+Boogie program verifier finished with 10 verified, 0 errors
+Processing TestRefines.chalice +
+Boogie program verifier finished with 9 verified, 0 errors
diff --git a/Chalice/refinements/LoopSqRoot.chalice b/Chalice/refinements/LoopSqRoot.chalice index e14fe4d6..4ea9434d 100644 --- a/Chalice/refinements/LoopSqRoot.chalice +++ b/Chalice/refinements/LoopSqRoot.chalice @@ -27,25 +27,17 @@ class A1 refines A0 { } } } -/* - method compute2(n: int) returns (x: int) - requires n >= 0; - { - var l := 0; - var r := n + 1; - while (l + 1 != r) - invariant l >= 0 && r > l; - invariant l*l <= n && n < r*r; - { - var p [2*p <= l+r && l+r < 2*(p+1)]; - assert l < p && p < r; - if (p*p <= n) { - l := p; - } else { - r := p; + +class A2 refines A1 { + transforms sqroot(n) returns (x) + { + _ + while { + replaces k by { + var k [2*k <= l+r && l+r < 2*(k+1)] } + * } - // no need to reverify + _ } } -*/ diff --git a/Chalice/refinements/test.sh b/Chalice/refinements/test.sh new file mode 100644 index 00000000..9cc84d90 --- /dev/null +++ b/Chalice/refinements/test.sh @@ -0,0 +1,29 @@ +#!/usr/bin/bash + +TESTS=" + LoopSqRoot.chalice + RecSqRoot.chalice + SpecStmt.chalice + SumCubes.chalice + TestTransform.chalice + TestRefines.chalice +" +if [ -f Output ] +then + rm -f Output +fi + +for f in $TESTS +do + echo "Processing $f" | tee -a Output + scala -cp ../bin chalice.Chalice -nologo $f >> Output 2>&1 +done + +if diff Output Answer +then + echo Success +else + echo Failure +fi + + diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala index 8059284c..cbb2ac85 100644 --- a/Chalice/src/Ast.scala +++ b/Chalice/src/Ast.scala @@ -190,10 +190,25 @@ sealed abstract class Refinement(id: String) extends Callable(id) { case class MethodTransform(id: String, ins: List[Variable], outs: List[Variable], spec: List[Specification], trans: Transform) extends Refinement(id) {
var body = null:List[Statement];
def Spec = {assert(refines != null); refines.Spec ++ spec}
- def Body = {assert(body != null); body} // TODO: get rid of refinement blocks (that is make sure variables match)
+ def Body = {
+ assert(body != null);
+ // make sure the body appears as if it is from a normal method
+ def concretize(ss: List[Statement]): List[Statement] = ss flatMap {
+ case r @ RefinementBlock(con, abs) =>
+ con :::
+ (for ((a,c) <- (r.during._1 zip r.during._2)) yield LocalVar(a, Some(new VariableExpr(c))))
+ case BlockStmt(ss) => List(BlockStmt(concretize(ss)))
+ case IfStmt(guard, BlockStmt(thn), None) => List(IfStmt(guard, BlockStmt(concretize(thn)), None))
+ case IfStmt(guard, BlockStmt(thn), Some(els)) => List(IfStmt(guard, BlockStmt(concretize(thn)), Some(BlockStmt(concretize(List(els))))))
+ case WhileStmt(guard, oi, ni, lks, BlockStmt(ss)) => List(WhileStmt(guard, oi ++ ni, Nil, lks, BlockStmt(concretize(ss))))
+ case s => List(s)
+ }
+ concretize(body)
+ }
def Ins = {assert(refines != null); refines.Ins}
def Outs = {assert(refines != null); refines.Outs ++ outs.drop(refines.Outs.size)}
}
+
sealed abstract class Transform extends ASTNode
/** Pattern matching within a block (zero or more) over deterministic statements */
case class BlockPat() extends Transform {
@@ -226,7 +241,14 @@ case class SeqPat(pats: List[Transform]) extends Transform { }
case class RefinementBlock(con: List[Statement], abs: List[Statement]) extends Statement {
if (con.size > 0) pos = con.first.pos;
- var locals: List[Variable] = null;
+ // existing local variables before the block
+ var before: List[Variable] = null;
+ // shared declared local variables
+ lazy val during: (List[Variable], List[Variable]) = {
+ val a = for (v <- abs.flatMap(s => s.Declares)) yield v;
+ val c = for (v <- a) yield con.flatMap(s => s.Declares).find(_ == v).get
+ (a,c)
+ }
override def Declares = con flatMap {_.Declares}
}
@@ -257,8 +279,7 @@ case class Assign(lhs: VariableExpr, rhs: RValue) extends Statement { override def Targets = if (lhs.v != null) Set(lhs.v) else Set()
}
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 = new Variable(id, t, ghost, const);
+case class LocalVar(v: Variable, rhs: Option[RValue]) extends Statement {
override def Declares = List(v)
override def Targets = rhs match {case None => Set(); case Some(_) => Set(v)}
}
@@ -520,7 +541,7 @@ case class CallState(token: Expression, obj: Expression, id: String, args: List[ object AST {
/**
- * Flattens sequences of transforms and merges consecutive blocks
+ * Flattens sequences of transforms and merges consecutive block patterns
*/
def normalize(trans: Transform): Transform = trans match {
case IfPat(thn, Some(els)) => IfPat(normalize(thn), Some(normalize(els)))
@@ -548,7 +569,7 @@ object AST { /**
* Matches a proper block to a transform.
* Effects: some statements might be replaced by refinements blocks; Loops might have new invariants.
- * Requires: in transform, a sequence pattern should not contain a sequence pattern.
+ * Requires: transform is normalized
*/
def refine:(List[Statement], Transform) => TransformMatch = {
// order is important!
diff --git a/Chalice/src/ChaliceToCSharp.scala b/Chalice/src/ChaliceToCSharp.scala index 98258e97..21c9bd0c 100644 --- a/Chalice/src/ChaliceToCSharp.scala +++ b/Chalice/src/ChaliceToCSharp.scala @@ -106,9 +106,9 @@ class ChaliceToCSharp { 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
- case LocalVar(id, tp, const, ghost, rhs) =>
- indent + convertType(tp) + " " + id + " = " +
- (if(rhs.isDefined) convertExpression(rhs.get) else defaultValue(tp)) +
+ case LocalVar(v, rhs) =>
+ indent + convertType(v.t) + " " + v.id + " = " +
+ (if(rhs.isDefined) convertExpression(rhs.get) else defaultValue(v.t)) +
";" + nl
case FieldUpdate(MemberAccess(target, f), rhs) =>
indent + convertExpression(target) + "." + f + " = " + convertExpression(rhs) + ";" + nl
diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala index bffcfb00..b8390405 100644 --- a/Chalice/src/Parser.scala +++ b/Chalice/src/Parser.scala @@ -256,7 +256,7 @@ class Parser extends StandardTokenParsers { | idTypeOpt ~ (":=" ~> Rhs ?) <~ Semi ^^ {
case (id,optT) ~ rhs =>
currentLocalVariables = currentLocalVariables + id.v
- LocalVar(id.v,
+ val v = Variable(id.v,
optT match {
case Some(t) => t
case None =>
@@ -267,8 +267,8 @@ class Parser extends StandardTokenParsers { case Some(x:BinaryExpr) if x.ResultType != null => new Type(x.ResultType);
case _ => Type("int", Nil)
}
- },
- const, ghost, rhs) }
+ }, ghost, const)
+ LocalVar(v, rhs) }
)
def ifStmtThen: Parser[IfStmt] =
"(" ~> expression ~ ")" ~ blockStatement ~ ("else" ~> ifStmtElse ?) ^^ {
diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala index 6a408b45..30cfb66f 100644 --- a/Chalice/src/PrettyPrinter.scala +++ b/Chalice/src/PrettyPrinter.scala @@ -89,10 +89,14 @@ object PrintProgram { }
case w @ WhileStmt(guard, _, _, lkch, body) =>
print("while ("); Expr(guard); println(")")
- for (inv <- w.Invs) {
+ for (inv <- w.oldInvs) {
Spaces(indent+2)
print("invariant "); Expr(inv); println(Semi)
}
+ for (inv <- w.newInvs) {
+ Spaces(indent+2)
+ print("invariant "); Expr(inv); print(" // refined"); println(Semi)
+ }
for (l <- lkch) {
Spaces(indent+2)
print("lockchange "); Expr(l); println(Semi)
@@ -102,10 +106,8 @@ object PrintProgram { Expr(lhs); print(" := "); Rhs(rhs); println(Semi)
case FieldUpdate(lhs,rhs) =>
Expr(lhs); print(" := "); Rhs(rhs); println(Semi)
- case LocalVar(id,t,c,g,rhs) =>
- if (g) print("ghost ")
- if (c) print("const ") else print("var ")
- print(id + ": " + t.FullName)
+ case LocalVar(v,rhs) =>
+ print(v + ": " + v.t.FullName)
rhs match { case None => case Some(rhs) => print(" := "); Rhs(rhs) }
println(Semi)
case SpecStmt(lhs, locals, pre, post) =>
diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala index e50cc7ab..9a0b830d 100644 --- a/Chalice/src/Resolver.scala +++ b/Chalice/src/Resolver.scala @@ -291,14 +291,14 @@ object Resolver { case BlockStmt(ss) =>
var ctx = context
for (s <- ss) s match {
- case l @ LocalVar(id, t, c, g, rhs) =>
- ResolveType(l.v.t, ctx)
+ case l @ LocalVar(v, rhs) =>
+ ResolveType(v.t, ctx)
val oldCtx = ctx
- ctx = ctx.AddVariable(l.v)
+ ctx = ctx.AddVariable(v)
rhs match {
case None =>
case Some(rhs) =>
- val lhs = VariableExpr(id)
+ val lhs = VariableExpr(v.id)
lhs.pos = l.pos;
ResolveExpr(lhs, ctx, false, false)(false)
ResolveAssign(lhs, rhs, oldCtx)
@@ -1097,7 +1097,7 @@ object Resolver { s match {
case r @ RefinementBlock(c, a) =>
// abstract globals available at this point in the program
- r.locals = locals
+ r.before = locals
ResolveStmt(BlockStmt(c), ctx)
val vs = c flatMap {s => s.Declares};
for (v <- a flatMap {s => s.Declares}; if (! vs.contains(v)))
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index f4fd1108..1ae56ca2 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -347,7 +347,7 @@ class Translator { DefinePreInitialState :::
Inhale(Preconditions(mt.Spec), "precondition") :::
DefineInitialState :::
- translateStatements(mt.Body) :::
+ 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"),
@@ -1040,10 +1040,9 @@ class Translator { val conGlobals = etran.FreshGlobals("concrete")
val conTran = new ExpressionTranslator(conGlobals map {v => new VarExpr(v)}, etran.oldEtran.Globals, currentClass);
// shared locals before block (excluding immutable)
- val before = for (v <- r.locals; if (! v.isImmutable)) yield v;
+ val before = for (v <- r.before; if (! v.isImmutable)) yield v;
// shared locals in block
- val duringA = for (v <- r.abs.flatMap(s => s.Declares)) yield v;
- val duringC = for (v <- duringA) yield r.con.flatMap(s => s.Declares).find(_ == v).get
+ val (duringA, duringC) = r.during;
// save locals before (to restore for abstract block)
val beforeV = for (v <- before) yield new Variable(v.id, v.t)
// save locals after (to compare with abstract block)
|