diff options
Diffstat (limited to 'Chalice')
146 files changed, 2843 insertions, 726 deletions
diff --git a/Chalice/chalice.bat b/Chalice/chalice.bat new file mode 100644 index 00000000..a81e4d5d --- /dev/null +++ b/Chalice/chalice.bat @@ -0,0 +1,5 @@ +@echo off
+
+call scala -cp "%~dp0\bin" chalice.Chalice -nologo %1 %2 %3 %4
+
+exit /B 0
diff --git a/Chalice/make.py b/Chalice/make.py index e3ba1ab9..c7fb52d9 100644 --- a/Chalice/make.py +++ b/Chalice/make.py @@ -14,6 +14,9 @@ lastbuild = None if os.path.exists(buildstamp):
lastbuild = os.path.getmtime(buildstamp)
+if not os.path.exists(bindir):
+ os.makedirs(bindir)
+
changedfiles = [file for file in srcfiles if not lastbuild or lastbuild <= os.path.getmtime(file)]
if not changedfiles:
diff --git a/Chalice/readme.txt b/Chalice/readme.txt new file mode 100644 index 00000000..124c3bc1 --- /dev/null +++ b/Chalice/readme.txt @@ -0,0 +1,7 @@ +
+Chalice - Verification of Concurrent Software
+=============================================
+
+Compiling Chalice: make.bat
+Running Chalice: chalice.bat <file.chalice> [-params]
+Running the tests for Chalice: see tests/readme.txt
diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala index 4b8b9189..8c59882f 100644 --- a/Chalice/src/Ast.scala +++ b/Chalice/src/Ast.scala @@ -27,6 +27,7 @@ sealed case class Class(classId: String, parameters: List[Class], module: String def IsChannel: Boolean = false
def IsState: Boolean = false
def IsNormalClass = true
+ def IsPermission = false
lazy val DeclaredFields = members flatMap {case x: Field => List(x); case _ => Nil}
lazy val MentionableFields = Fields filter {x => ! x.Hidden}
@@ -65,13 +66,23 @@ sealed case class Class(classId: String, parameters: List[Class], module: String lazy val Replaces: List[Field] = CouplingInvariants flatMap (_.fields)
}
-sealed case class Channel(channelId: String, parameters: List[Variable], where: Expression) extends TopLevelDecl(channelId)
+sealed case class Channel(channelId: String, parameters: List[Variable], private val rawWhere: Expression) extends TopLevelDecl(channelId) {
+ lazy val where: Expression = rawWhere.transform {
+ case Epsilon | MethodEpsilon => Some(ChannelEpsilon(None))
+ case _ => None
+ }
+}
sealed case class SeqClass(parameter: Class) extends Class("seq", List(parameter), "default", Nil) {
override def IsRef = false;
override def IsSeq = true;
override def IsNormalClass = false
}
+object PermClass extends Class("$Permission", Nil, "default", Nil) {
+ override def IsRef = false
+ override def IsPermission = true
+ override def IsNormalClass = false
+}
object IntClass extends Class("int", Nil, "default", Nil) {
override def IsRef = false
override def IsInt = true
@@ -114,6 +125,7 @@ object RootClass extends Class("$root", Nil, "default", List( )) // joinable and held are bool in Chalice, but translated into an int in Boogie
sealed case class Type(id: String, params: List[Type]) extends ASTNode { // denotes the use of a type
+ if (id equals "seq") TranslatorPrelude.addComponent(AxiomatizationOfSequencesPL) // include sequence axioms if necessary
var typ: Class = null
def this(id: String) = { this(id, Nil); }
def this(cl: Class) = { this(cl.id); typ = cl }
@@ -134,7 +146,13 @@ sealed case class TokenType(C: Type, m: String) extends Type("token", Nil) { // sealed abstract class Member extends ASTNode {
val Hidden: Boolean = false // hidden means not mentionable in source
}
-case class MonitorInvariant(e: Expression) extends Member
+case class MonitorInvariant(private val rawE: Expression) extends Member {
+ lazy val e: Expression = rawE.transform {
+ case Epsilon | MethodEpsilon => Some(MonitorEpsilon(None))
+ case _ => None
+ }
+}
+
sealed abstract class NamedMember(id: String) extends Member {
val Id = id
var Parent: Class = null
@@ -157,7 +175,12 @@ case class Method(id: String, ins: List[Variable], outs: List[Variable], spec: L override def Ins = ins
override def Outs = outs
}
-case class Predicate(id: String, definition: Expression) extends NamedMember(id)
+case class Predicate(id: String, private val rawDefinition: Expression) extends NamedMember(id) {
+ lazy val definition: Expression = rawDefinition.transform {
+ case Epsilon | MethodEpsilon => Some(PredicateEpsilon(None))
+ case _ => None
+ }
+}
case class Function(id: String, ins: List[Variable], out: Type, spec: List[Specification], definition: Option[Expression]) extends NamedMember(id) {
def apply(rec: Expression, args: List[Expression]): FunctionApplication = {
val result = FunctionApplication(rec, id, args);
@@ -175,6 +198,7 @@ case class Variable(id: String, t: Type, isGhost: Boolean, isImmutable: Boolean) S_Variable.VariableCount = S_Variable.VariableCount + 1
id + "#" + n
}
+ val Id = id;
def this(name: String, typ: Type) = this(name,typ,false,false);
override def toString = (if (isGhost) "ghost " else "") + (if (isImmutable) "const " else "var ") + id;
}
@@ -249,8 +273,6 @@ case class NonDetPat(is: List[String], code: List[Statement]) extends Transform def matches(s: Statement) = s match {
case _:Call => true
case _:SpecStmt => true
- case _:Assign => true // declarative expression on the right
- case _:LocalVar => true // declarative expression on the right
case _ => false
}
}
@@ -262,16 +284,11 @@ 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.head.pos
// local variables in context at the beginning of the block
-
var before: List[Variable] = null
// shared declared local variables (mapping between abstract and concrete)
- // should be called after resolution
lazy val during: (List[Variable], List[Variable]) = {
- val a = abs.flatMap(s => s.Declares);
- val c = for (v <- a) yield con.flatMap(s => s.Declares).find(_ == v) match {
- case Some(w) => w;
- case None => v;
- }
+ 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}
@@ -396,20 +413,65 @@ case class MemberAccess(e: Expression, id: String) extends Expression { }
case class IfThenElse(con: Expression, then: Expression, els: Expression) extends Expression
-sealed abstract class Permission extends Expression
-sealed abstract class Write extends Permission
+object PermissionType extends Enumeration {
+ type PermissionType = Value
+ val Fraction, Epsilons, Mixed = Value
+}
+import PermissionType._
+sealed abstract class Permission extends Expression {
+ typ = PermClass
+ def permissionType: PermissionType
+}
+sealed abstract class Write extends Permission {
+ override def permissionType = PermissionType.Fraction
+}
object Full extends Write // None
case class Frac(n: Expression) extends Write // Some(n)
-sealed abstract class Read extends Permission
-object Epsilon extends Read // None
-object Star extends Read // Some(None)
+sealed abstract class Read extends Permission {
+ override def permissionType = PermissionType.Epsilons
+}
+object Epsilon extends Write // None
+// we use Option for the argument of the next three classes as follows:
+// the argument is Some(_) if the exression originates from the user (e.g. if he used acc(x,rd(monitor))),
+// and None otherwise. If Some(_) is used, we have additional checks to ensure that we have read access
+// to _ and _ is not null.
+case class PredicateEpsilon(predicate: Option[Expression]) extends Write
+case class MonitorEpsilon(monitor: Option[Expression]) extends Write
+case class ChannelEpsilon(channel: Option[Expression]) extends Write
+object MethodEpsilon extends Write
+case class ForkEpsilon(token: Expression) extends Write
+object Star extends Write // Some(None)
case class Epsilons(n: Expression) extends Read // Some(Some(n))
+sealed abstract class ArithmeticPermission extends Permission
+case class PermTimes(val lhs: Permission, val rhs: Permission) extends ArithmeticPermission {
+ override def permissionType = {
+ if (lhs.permissionType == rhs.permissionType) lhs.permissionType
+ else Mixed
+ }
+}
+case class IntPermTimes(val lhs: Expression, val rhs: Permission) extends ArithmeticPermission {
+ override def permissionType = rhs.permissionType
+}
+case class PermPlus(val lhs: Permission, val rhs: Permission) extends ArithmeticPermission {
+ override def permissionType = {
+ if (lhs.permissionType == rhs.permissionType) lhs.permissionType
+ else Mixed
+ }
+}
+case class PermMinus(val lhs: Permission, val rhs: Permission) extends ArithmeticPermission {
+ override def permissionType = {
+ if (lhs.permissionType == rhs.permissionType) lhs.permissionType
+ else Mixed
+ }
+}
+
+
sealed abstract class PermissionExpr(perm: Permission) extends Expression
sealed abstract class WildCardPermission(perm: Permission) extends PermissionExpr(perm)
-case class Access(ma: MemberAccess, perm: Permission) extends PermissionExpr(perm)
-case class AccessAll(obj: Expression, perm: Permission) extends WildCardPermission(perm)
-case class AccessSeq(s: Expression, f: Option[MemberAccess], perm: Permission) extends WildCardPermission(perm)
+case class Access(ma: MemberAccess, var perm: Permission) extends PermissionExpr(perm)
+case class AccessAll(obj: Expression, var perm: Permission) extends WildCardPermission(perm)
+case class AccessSeq(s: Expression, f: Option[MemberAccess], var perm: Permission) extends WildCardPermission(perm)
case class Credit(e: Expression, n: Option[Expression]) extends Expression {
val N = n match { case None => IntLiteral(1) case Some(n) => n }
@@ -512,8 +574,15 @@ sealed abstract class Quantification(q: Quant, is: List[String], e: Expression) val E = e;
var variables = null: List[Variable]; // resolved by type checker
}
-case class SeqQuantification(q: Quant, is: List[String], seq: Expression, e: Expression) extends Quantification(q, is, e)
-case class TypeQuantification(q: Quant, is: List[String], t: Type, e: Expression) extends Quantification(q, is, e)
+case class SeqQuantification(q: Quant, is: List[String], seq: Expression, e: Expression) extends Quantification(q, is, e) {
+ TranslatorPrelude.addComponent(AxiomatizationOfSequencesPL) // include sequence axioms if necessary
+}
+// The minmax field stores the minimum and maximum of a range if the TypeQuantification originates from
+// a SeqQuantification (e.g. from "forall i in [0..2] :: ..". This is later needed in isDefined to
+// assert that min <= max
+case class TypeQuantification(q: Quant, is: List[String], t: Type, e: Expression, minmax: (Expression, Expression)) extends Quantification(q, is, e) {
+ def this(q: Quant, is: List[String], t: Type, e: Expression) = this(q, is, t, e, null)
+}
/**
* Expressions: sequences
@@ -623,7 +692,8 @@ object AST { case _ => Unmatched(wp)
}
// non det pat
- case (l @ List(s), ndp @ NonDetPat(_, code)) if ndp matches s => new Matched(RefinementBlock(code, l))
+ case (l @ List(_: Call), NonDetPat(_, code)) => new Matched(RefinementBlock(code, l))
+ case (l @ List(_: SpecStmt), NonDetPat(_, code)) => new Matched(RefinementBlock(code, l))
// insert pat
case (Nil, InsertPat(code)) => new Matched(RefinementBlock(code, Nil))
// block pattern (greedy matching)
@@ -678,9 +748,18 @@ object AST { g.predicate = ma.predicate;
g.isPredicate = ma.isPredicate;
g
- case Full | Epsilon | Star => expr
+ case ForkEpsilon(token) => ForkEpsilon(func(token))
+ case MonitorEpsilon(Some(monitor)) => MonitorEpsilon(Some(func(monitor)))
+ case ChannelEpsilon(Some(channel)) => ChannelEpsilon(Some(func(channel)))
+ case PredicateEpsilon(Some(predicate)) => PredicateEpsilon(Some(func(predicate)))
+ case ChannelEpsilon(None) | MonitorEpsilon(None) | PredicateEpsilon(None) => expr
+ case Full | Star | Epsilon | MethodEpsilon => expr
case Frac(perm) => Frac(func(perm))
case Epsilons(perm) => Epsilons(func(perm))
+ case PermTimes(lhs, rhs) => PermTimes(func(lhs).asInstanceOf[Permission], func(rhs).asInstanceOf[Permission])
+ case IntPermTimes(lhs, rhs) => IntPermTimes(func(lhs), func(rhs).asInstanceOf[Permission])
+ case PermPlus(lhs, rhs) => PermPlus(func(lhs).asInstanceOf[Permission], func(rhs).asInstanceOf[Permission])
+ case PermMinus(lhs, rhs) => PermMinus(func(lhs).asInstanceOf[Permission], func(rhs).asInstanceOf[Permission])
case Access(e, perm) => Access(func(e).asInstanceOf[MemberAccess], func(perm).asInstanceOf[Permission]);
case AccessAll(obj, perm) => AccessAll(func(obj), func(perm).asInstanceOf[Permission]);
case AccessSeq(s, None, perm) => AccessSeq(func(s), None, func(perm).asInstanceOf[Permission])
@@ -727,8 +806,12 @@ object AST { val result = SeqQuantification(q, is, func(seq), func(e));
result.variables = qe.variables;
result;
- case qe @ TypeQuantification(q, is, t, e) =>
- val result = TypeQuantification(q, is, t, func(e));
+ case qe @ TypeQuantification(q, is, t, e, (min, max)) =>
+ val result = TypeQuantification(q, is, t, func(e), (func(min),func(max)));
+ result.variables = qe.variables;
+ result;
+ case qe @ TypeQuantification(q, is, t, e, null) =>
+ val result = new TypeQuantification(q, is, t, func(e));
result.variables = qe.variables;
result;
case Eval(h, e) =>
@@ -762,7 +845,20 @@ object AST { case Frac(p) => visit(p, f);
case Epsilons(p) => visit(p, f);
- case Full | Epsilon | Star =>;
+ case Full | Epsilon | Star | MethodEpsilon =>;
+ case ChannelEpsilon(None) | PredicateEpsilon(None) | MonitorEpsilon(None) =>;
+ case ChannelEpsilon(Some(e)) => visit(e, f);
+ case PredicateEpsilon(Some(e)) => visit(e, f);
+ case MonitorEpsilon(Some(e)) => visit(e, f);
+ case ForkEpsilon(tk) => visit(tk, f);
+ case IntPermTimes(n, p) =>
+ visit(n, f); visit(p, f);
+ case PermTimes(e0, e1) =>
+ visit(e0, f); visit(e1, f);
+ case PermPlus(e0, e1) =>
+ visit(e0, f); visit(e1, f);
+ case PermMinus(e0, e1) =>
+ visit(e0, f); visit(e1, f);
case Access(e, perm) =>
visit(e, f); visit(perm, f);
case AccessAll(obj, perm) =>
@@ -789,8 +885,8 @@ object AST { visit(pred, f); visit(e, f);
case SeqQuantification(_, _, seq, e) => visit(seq, f); visit(e, f);
- case TypeQuantification(_, _, _, e) => visit(e, f);
-
+ case TypeQuantification(_, _, _, e, (min,max)) => visit(e, f); visit(min, f); visit(max, f);
+ case TypeQuantification(_, _, _, e, _) => visit(e, f);
case ExplicitSeq(es) =>
es foreach { e => visit(e, f) }
case Length(e) =>
diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala index fff66367..1b53a187 100644 --- a/Chalice/src/Chalice.scala +++ b/Chalice/src/Chalice.scala @@ -32,6 +32,11 @@ object Chalice { private[chalice] var skipDeadlockChecks = false: Boolean;
private[chalice] var skipTermination = false: Boolean;
private[chalice] var noFreeAssume = false: Boolean;
+ // percentageSupport 0: use multiplication directly
+ // percentageSupport 1: fix Permission$denominator as constant (possibly unsound for small values of the constant?)
+ // percentageSupport 2: use function and provide some (redundant) axioms
+ // percentageSupport 3: use an uninterpreted function and axiomatize the properties of multiplication
+ private[chalice] var percentageSupport = 2;
def main(args: Array[String]): Unit = {
var boogiePath = "C:\\boogie\\Binaries\\Boogie.exe"
@@ -41,6 +46,7 @@ object Chalice { var doTranslate = true
var boogieArgs = " ";
var gen = false;
+ var showFullStackTrace = false
// closures should be idempotent
val options = Map(
@@ -55,7 +61,8 @@ object Chalice { "-gen" -> {() => gen = true},
"-autoFold" -> {() => autoFold = true},
"-autoMagic"-> {() => autoMagic = true},
- "-noFreeAssume" -> {() => noFreeAssume = true}
+ "-noFreeAssume" -> {() => noFreeAssume = true},
+ "-showFullStackTrace" -> {() => showFullStackTrace = true}
)
lazy val help = options.keys.foldLeft("syntax: chalice")((s, o) => s + " [" + o + "]") +
" [-boogie:path]" +
@@ -73,9 +80,23 @@ object Chalice { if (3<=defaults) { autoMagic = true; }
} catch { case _ => CommandLineError("-defaults takes integer argument", help); }
}
+ else if (a.startsWith("-percentageSupport:")) {
+ try {
+ val in = Integer.parseInt(a.substring("-percentageSupport:".length));
+ if (in < 0 || in > 3) CommandLineError("-percentageSupport takes only values 0,1,2 or 3", help)
+ else percentageSupport = in
+ } catch { case _ => CommandLineError("-percentageSupport takes integer argument", help); }
+ }
else if (a.startsWith("-") || a.startsWith("/")) boogieArgs += (a + " ") // other arguments starting with "-" or "/" are sent to Boogie.exe
else inputs += a
}
+
+ percentageSupport match {
+ case 0 => TranslatorPrelude.addComponent(PercentageStandardPL)
+ case 1 => TranslatorPrelude.addComponent(PercentageStandardPL, PercentageFixedDenominatorPL)
+ case 2 => TranslatorPrelude.addComponent(PercentageFunctionPL)
+ case 3 => TranslatorPrelude.addComponent(PercentageUninterpretedFunctionPL)
+ }
// check that input files exist
var files = for (input <- inputs.toList) yield {
@@ -126,14 +147,34 @@ object Chalice { if (doTranslate) {
// checking if Boogie.exe exists
val boogieFile = new File(boogiePath);
- if (System.getProperty("os.name").toLowerCase.indexOf("win") >= 0) {
- if(! boogieFile.exists() || ! boogieFile.isFile()) {
- CommandLineError("Boogie.exe not found at " + boogiePath, help); return
- }
+ if(! boogieFile.exists() || ! boogieFile.isFile()) {
+ CommandLineError("Boogie.exe not found at " + boogiePath, help); return
}
// translate program to Boogie
val translator = new Translator();
- val bplProg = translator.translateProgram(program);
+ var bplProg: List[Boogie.Decl] = Nil
+ try {
+ bplProg = translator.translateProgram(program);
+ } catch {
+ case e:InternalErrorException => {
+ if (showFullStackTrace) {
+ e.printStackTrace()
+ Console.err.println()
+ Console.err.println()
+ }
+ CommandLineError("Internal error: " + e.msg, help)
+ return
+ }
+ case e:NotSupportedException => {
+ if (showFullStackTrace) {
+ e.printStackTrace()
+ Console.err.println()
+ Console.err.println()
+ }
+ CommandLineError("Not supported: " + e.msg, help)
+ return
+ }
+ }
// write to out.bpl
val bplText = TranslatorPrelude.P + (bplProg map Boogie.Print).foldLeft(""){ (a, b) => a + b };
val bplFilename = if (vsMode) "c:\\tmp\\out.bpl" else "out.bpl"
@@ -146,7 +187,7 @@ object Chalice { try {
val kill = Runtime.getRuntime.exec("taskkill /T /F /IM Boogie.exe");
kill.waitFor;
- } catch {case _ => }
+ } catch {case _ => }
// just to be sure
boogie.destroy
}
@@ -202,3 +243,6 @@ object Chalice { }
}
}
+
+class InternalErrorException(val msg: String) extends Throwable
+class NotSupportedException(val msg: String) extends Throwable
diff --git a/Chalice/src/ChaliceToCSharp.scala b/Chalice/src/ChaliceToCSharp.scala index 21c9bd0c..0ac84a4c 100644 --- a/Chalice/src/ChaliceToCSharp.scala +++ b/Chalice/src/ChaliceToCSharp.scala @@ -93,6 +93,7 @@ class ChaliceToCSharp { indent + "}" + nl
case MonitorInvariant(_) => indent + "// monitor invariant" + nl
case Predicate(_, _) => indent + "//predicate" + nl
+ case _ => throw new NotSupportedException("unsupportet construct")
}
}
@@ -156,6 +157,7 @@ class ChaliceToCSharp { case r@Receive(_, ch, outs) =>
declareLocals(r.locals) +
indent + convertExpression(ch) + ".Receive(" + repsep(outs map { out => "out " + convertExpression(out)}, ", ") + ")" + ";" + nl
+ case _ => throw new NotSupportedException("unsupportet construct")
}
}
@@ -201,7 +203,7 @@ class ChaliceToCSharp { case Range(min, max) => "Chalice.ImmutableList.Range(" + convertExpression(min) + ", " + convertExpression(max) + ")"
case Length(s) => convertExpression(s) + ".Length"
case IfThenElse(c, thn, els) => "(" + convertExpression(c) + " ? " + convertExpression(thn) + " : " + convertExpression(els) + ")"
- case _ => throw new Exception("Expression not supported yet!");
+ case _ => throw new NotSupportedException("Expression not supported yet!");
}
}
diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala index 44b8227a..f8824cee 100644 --- a/Chalice/src/Parser.scala +++ b/Chalice/src/Parser.scala @@ -5,6 +5,8 @@ //-----------------------------------------------------------------------------
package chalice;
import scala.util.parsing.combinator.syntactical.StandardTokenParsers
+import scala.util.parsing.combinator.lexical.StdLexical
+import scala.util.parsing.combinator._
import scala.util.parsing.input.PagedSeqReader
import scala.collection.immutable.PagedSeq
import scala.util.parsing.input.Position
@@ -18,7 +20,13 @@ class Parser extends StandardTokenParsers { def parseFile(file: File) = phrase(programUnit)(new lexical.Scanner(new PagedSeqReader(PagedSeq fromFile file)))
case class PositionedString(v: String) extends Positional
-
+
+ // handle comments already in lexer
+ override val lexical = new StdLexical {
+ def rp: RegexParsers = new RegexParsers {}
+ override val whitespace: Parser[Any] = rp.regex("""(\s|//.*|(?m)/\*(\*(?!/)|[^*])*\*/)*""".r).asInstanceOf[Parser[Any]]
+ }
+
lexical.reserved += ("class", "ghost", "var", "const", "method", "channel", "condition",
"assert", "assume", "new", "this", "reorder",
"between", "and", "above", "below", "share", "unshare", "acquire", "release", "downgrade",
@@ -45,6 +53,7 @@ class Parser extends StandardTokenParsers { def Semi = ";" ?
var currentLocalVariables = Set[String]() // used in the method context
var assumeAllLocals = false;
+ var insidePermission = false;
/**
* Top level declarations
@@ -273,8 +282,8 @@ class Parser extends StandardTokenParsers { case Some(NewRhs(tid, _, _, _)) => Type(tid, Nil)
case Some(BoolLiteral(b)) => Type("bool", Nil)
case Some(x:BinaryExpr) if x.ResultType != null => new Type(x.ResultType);
- case Some(x:Contains) => Type("bool", Nil)
- case Some(x:Quantification) => Type("bool", Nil)
+ case Some(x:Contains) => Type("bool", Nil)
+ case Some(x:Quantification) => Type("bool", Nil)
case _ => Type("int", Nil)
}
}, ghost, const)
@@ -485,14 +494,34 @@ class Parser extends StandardTokenParsers { r.pos = id.pos; r
}
| "rd" ~> "(" ~>
- ( (Ident ^^ (e => { val result = MemberAccess(ImplicitThisExpr(),e.v); result.pos = e.pos; result})) ~ rdPermArg <~ ")"
- | selectExprFerSureX ~ rdPermArg <~ ")"
- ) ^^ {
- case MemberAccess(obj, "*") ~ p => AccessAll(obj, p);
- case MemberAccess(obj, "[*].*") ~ p => AccessSeq(obj, None, p);
- case MemberAccess(MemberAccess(obj, "[*]"), f) ~ p => AccessSeq(obj, Some(MemberAccess(At(obj, IntLiteral(0)), f)), p);
- case e ~ p => Access(e, p)
+ ( // note: depending on the context where rd occurs, we parse it wrongly (e.g. acc(x,rd(n)) is parsed to
+ // Access(MemberAccess(ImplicitThisExpr(),x),Frac(Access(MemberAccess(ImplicitThisExpr(),n),Epsilon))) ).
+ // This might seem completely wrong (and it is), but we correct this later, see the comment before
+ // method ResolvePermissionExpr in the resolver.
+ (( (Ident ^^ (e => { val result = MemberAccess(ImplicitThisExpr(),e.v); result.pos = e.pos; result})) ~ rdPermArg <~ ")"
+ | selectExprFerSureX ~ rdPermArg <~ ")"
+ ) ^^ {
+ case MemberAccess(obj, "*") ~ p => AccessAll(obj, p);
+ case MemberAccess(obj, "[*].*") ~ p => AccessSeq(obj, None, p);
+ case MemberAccess(MemberAccess(obj, "[*]"), f) ~ p => AccessSeq(obj, Some(MemberAccess(At(obj, IntLiteral(0)), f)), p);
+ case e ~ p => Access(e, p)
+ })
+ | expression <~ ")" ^^ {
+ case e => val eps = Epsilons(e); eps.pos = e.pos; eps
}
+ | "*" ~> ")" ~ err("This syntax is not supported any longer. For the starred read permission, use rd*(o.f).") ^^^ Star
+ )
+ | "rd" ~> "*" ~> "(" ~>
+ (
+ (( (Ident ^^ (e => { val result = MemberAccess(ImplicitThisExpr(),e.v); result.pos = e.pos; result})) <~ ")"
+ | selectExprFerSureX <~ ")"
+ ) ^^ {
+ case MemberAccess(obj, "*") => AccessAll(obj, Star);
+ case MemberAccess(obj, "[*].*") => AccessSeq(obj, None, Star);
+ case MemberAccess(MemberAccess(obj, "[*]"), f) => AccessSeq(obj, Some(MemberAccess(At(obj, IntLiteral(0)), f)), Star);
+ case e => Access(e, Star)
+ })
+ )
| "acc" ~> "(" ~>
( (Ident ^^ (e => { val result = MemberAccess(ImplicitThisExpr(),e.v); result.pos = e.pos; result} )) ~ accPermArg <~ ")"
| selectExprFerSureX ~ accPermArg <~ ")"
@@ -506,6 +535,7 @@ class Parser extends StandardTokenParsers { case ch ~ n => Credit(ch, n) }
| "holds" ~> "(" ~> expression <~ ")" ^^ Holds
| "rd" ~> "holds" ~> "(" ~> expression <~ ")" ^^ RdHolds
+ | "rd" ^^ (_ => MethodEpsilon)
| "assigned" ~> "(" ~> ident <~ ")" ^^ Assigned
| "old" ~> "(" ~> expression <~ ")" ^^ Old
| ("unfolding" ~> suffixExpr <~ "in") ~ expression ^? {
@@ -538,7 +568,7 @@ class Parser extends StandardTokenParsers { ((":" ~> typeDecl <~ "::") ~ (exprWithLocals(is))) ^^
{ case t ~ e =>
currentLocalVariables = currentLocalVariables -- is;
- TypeQuantification(q, is, t, e);
+ new TypeQuantification(q, is, t, e);
}
def quant: Parser[Quant] =
( "forall" ^^^ Forall | "exists" ^^^ Exists)
@@ -557,12 +587,12 @@ class Parser extends StandardTokenParsers { case MemberAccess(obj,id) ~ args => CallState(e, obj, id, args) }
)}
- def rdPermArg : Parser[Read] =
- opt( "," ~> "*" ^^^ Star
- | "," ~> expression ^^ { case e => Epsilons(e) }) ^^ { case None => Epsilon; case Some(p) => p}
+ def rdPermArg : Parser[Permission] =
+ opt( "," ~> "*" ~ err("This syntax is not supported any longer. For the starred read permission, use rd*(o.f).") ^^^ Star
+ | "," ~> expression ^^ { case e => val eps = Epsilons(e); eps.pos = e.pos; eps }) ^^ { case None => Epsilon; case Some(p) => p}
def accPermArg : Parser[Write] =
- opt( "," ~> expression ^^ { case e => Frac(e) }) ^^ { case None => Full; case Some(p) => p}
+ opt( "," ~> expression ^^ { case e => val f: Frac = Frac(e); f.pos = e.pos; f }) ^^ { case None => Full; case Some(p) => p}
/**
* Transforms
diff --git a/Chalice/src/Prelude.scala b/Chalice/src/Prelude.scala index a9e00ace..f4a99796 100644 --- a/Chalice/src/Prelude.scala +++ b/Chalice/src/Prelude.scala @@ -4,10 +4,60 @@ //
//-----------------------------------------------------------------------------
package chalice;
+import scala.collection.mutable.Set;
+
+/*
+This object computes the Boogie prelude for the translator, which consists of different
+components (objects that are subtypes of PreludeComponent). It is possible to include
+such components only on demand, when they are actually needed. For instance, the sequence
+axiomatization is only included if sequences are used in the program at hand.
+*/
object TranslatorPrelude {
+
+ // adds component c to the prelude. has no effect if c is already present.
+ def addComponent(c: PreludeComponent*): Unit = {
+ components ++= c
+ }
+
+ // removes a component from the prelude. use with great care, as other parts of
+ // the system could depend on the component c being present in the prelude.
+ def removeComponent(c: PreludeComponent*): Unit = {
+ components --= c
+ }
+
+ // default components
+ private val components: Set[PreludeComponent] = Set(CopyrightPL, TypesPL, PermissionTypesAndConstantsPL, CreditsAndMuPL, PermissionFunctionsAndAxiomsPL, IfThenElsePL, ArithmeticPL)
+
+ // get the prelude (with all components currently included)
+ def P: String = {
+ val l = components.toList.sortWith((a,b) => a compare b)
+ l.foldLeft("")((s:String,a:PreludeComponent) => s + "\n" + (a text)) +
+"""
+
+// ---------------------------------------------------------------
+// -- End of prelude ---------------------------------------------
+// ---------------------------------------------------------------
+
+"""
+ }
- val P =
-"""// Copyright (c) 2008, Microsoft
+}
+
+sealed abstract class PreludeComponent {
+ // determines the order in which the components are output
+ def compare(that: PreludeComponent): Boolean = {
+ val order: List[PreludeComponent] = List(CopyrightPL, TypesPL, PermissionTypesAndConstantsPL, PercentageFixedDenominatorPL, PercentageFunctionPL, PercentageUninterpretedFunctionPL, CreditsAndMuPL, PermissionFunctionsAndAxiomsPL, IfThenElsePL, ArithmeticPL, AxiomatizationOfSequencesPL)
+ if (!order.contains(this)) false
+ else order.indexOf(this) < order.indexOf(that)
+ }
+ def text: String
+}
+
+object CopyrightPL extends PreludeComponent {
+ val text = "// Copyright (c) 2008, Microsoft"
+}
+object TypesPL extends PreludeComponent {
+ val text = """
type Field a;
type HeapType = <a>[ref,Field a]a;
type MaskType = <a>[ref,Field a][PermissionComponent]int;
@@ -15,41 +65,75 @@ type CreditsType = [ref]int; type ref;
const null: ref;
-var Heap: HeapType;
-
+var Heap: HeapType;"""
+}
+object PermissionTypesAndConstantsPL extends PreludeComponent {
+ val text = """
type PermissionComponent;
const unique perm$R: PermissionComponent;
const unique perm$N: PermissionComponent;
-const Permission$MinusInfinity: int;
-axiom Permission$MinusInfinity < -10000;
-const Permission$PlusInfinity: int;
-axiom 10000 < Permission$PlusInfinity;
var Mask: MaskType where IsGoodMask(Mask);
+const Permission$denominator: int;
+axiom Permission$denominator > 0;
+const Permission$FullFraction: int;
const Permission$Zero: [PermissionComponent]int;
axiom Permission$Zero[perm$R] == 0 && Permission$Zero[perm$N] == 0;
const Permission$Full: [PermissionComponent]int;
-axiom Permission$Full[perm$R] == 100 && Permission$Full[perm$N] == 0;
+axiom Permission$Full[perm$R] == Permission$FullFraction && Permission$Full[perm$N] == 0;
const ZeroMask: MaskType;
axiom (forall<T> o: ref, f: Field T, pc: PermissionComponent :: ZeroMask[o,f][pc] == 0);
axiom IsGoodMask(ZeroMask);
-function {:expand false} CanRead<T>(m: MaskType, obj: ref, f: Field T) returns (bool)
-{
- 0 < m[obj,f][perm$R] || 0 < m[obj,f][perm$N]
+const unique joinable: Field int;
+axiom NonPredicateField(joinable);
+const unique token#t: TypeName;
+const unique forkK: Field int;
+axiom NonPredicateField(forkK);
+const channelK: int;
+const monitorK: int;
+const predicateK: int;"""
}
-function {:expand false} CanWrite<T>(m: MaskType, obj: ref, f: Field T) returns (bool)
-{
- m[obj,f][perm$R] == 100 && m[obj,f][perm$N] == 0
+object PercentageStandardPL extends PreludeComponent {
+ val text = """
+axiom (0 < channelK && 1000*channelK < Permission$denominator);
+axiom (0 < monitorK && 1000*monitorK < Permission$denominator);
+axiom (0 < predicateK && 1000*predicateK < Permission$denominator);
+axiom Permission$FullFraction == 100*Permission$denominator;
+axiom predicateK == channelK && channelK == monitorK;"""
}
-function {:expand true} IsGoodMask(m: MaskType) returns (bool)
+object PercentageFixedDenominatorPL extends PreludeComponent {
+ val text = """
+axiom Permission$denominator == 100000000000;"""
+}
+object PercentageFunctionPL extends PreludeComponent {
+ val text = """
+function Fractions(n: int): int
{
- (forall<T> o: ref, f: Field T ::
- 0 <= m[o,f][perm$R] &&
- (NonPredicateField(f) ==>
- (m[o,f][perm$R]<=100 &&
- (0 < m[o,f][perm$N] ==> m[o,f][perm$R] < 100))) &&
- (m[o,f][perm$N] < 0 ==> 0 < m[o,f][perm$R]))
+ n * Permission$denominator
}
+axiom (forall x,y: int :: 0 <= x && x <= y ==> Fractions(x) <= Fractions(y));
+axiom Permission$FullFraction == Fractions(100);
+axiom 0 < channelK && 1000*channelK < Fractions(1);
+axiom 0 < monitorK && 1000*monitorK < Fractions(1);
+axiom 0 < predicateK && 1000*predicateK < Fractions(1);
+axiom predicateK == channelK && channelK == monitorK;"""
+}
+object PercentageUninterpretedFunctionPL extends PreludeComponent {
+ val text = """
+function Fractions(n: int): int;
+function Fractions'(n: int): int;
+axiom (forall x: int :: { Fractions(x) } Fractions(x) == Fractions'(x));
+axiom (forall x,y: int :: 0 <= x && x <= y ==> Fractions'(x) <= Fractions'(y));
+axiom (forall x,y: int :: { Fractions(x), Fractions(y) } Fractions(x) + Fractions(y) == Fractions'(x+y));
+
+axiom Permission$FullFraction == Fractions(100);
+axiom 0 < channelK && 1000*channelK < Fractions(1);
+axiom 0 < monitorK && 1000*monitorK < Fractions(1);
+axiom 0 < predicateK && 1000*predicateK < Fractions(1);
+axiom predicateK == channelK && channelK == monitorK;"""
+}
+object CreditsAndMuPL extends PreludeComponent {
+ val text = """
var Credits: CreditsType;
function IsGoodState<T>(T) returns (bool);
@@ -100,16 +184,118 @@ function IsGoodInhaleState(ih: HeapType, h: HeapType, (forall o: ref :: { ih[o, rdheld] } ih[o, rdheld] == h[o, rdheld]) &&
(forall o: ref :: { h[o, held] } (0<h[o, held]) ==> ih[o, mu] == h[o, mu]) &&
(forall o: ref :: { h[o, rdheld] } h[o, rdheld] ==> ih[o, mu] == h[o, mu])
+}"""
}
+object PermissionFunctionsAndAxiomsPL extends PreludeComponent {
+ val text = """
+// ---------------------------------------------------------------
+// -- Permissions ------------------------------------------------
+// ---------------------------------------------------------------
+
+function {:expand false} CanRead<T>(m: MaskType, obj: ref, f: Field T) returns (bool)
+{
+ 0 < m[obj,f][perm$R] || 0 < m[obj,f][perm$N]
+}
+function {:expand false} CanWrite<T>(m: MaskType, obj: ref, f: Field T) returns (bool)
+{
+ m[obj,f][perm$R] == Permission$FullFraction && m[obj,f][perm$N] == 0
+}
+function {:expand true} IsGoodMask(m: MaskType) returns (bool)
+{
+ (forall<T> o: ref, f: Field T ::
+ 0 <= m[o,f][perm$R] &&
+ (NonPredicateField(f) ==>
+ (m[o,f][perm$R]<=Permission$FullFraction &&
+ (0 < m[o,f][perm$N] ==> m[o,f][perm$R] < Permission$FullFraction))) &&
+ (m[o,f][perm$N] < 0 ==> 0 < m[o,f][perm$R]))
+}
+
+axiom (forall h: HeapType, m: MaskType, o: ref, q: ref :: {wf(h, m), h[o, mu], h[q, mu]} wf(h, m) && o!=q && (0 < h[o, held] || h[o, rdheld]) && (0 < h[q, held] || h[q, rdheld]) ==> h[o, mu] != h[q, mu]);
+
+function DecPerm<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
+
+axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {DecPerm(m, o, f, howMuch)[q, g][perm$R]}
+ DecPerm(m, o, f, howMuch)[q, g][perm$R] == ite(o==q && f ==g, m[q, g][perm$R] - howMuch, m[q, g][perm$R])
+);
+
+function DecEpsilons<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
+
+axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {DecPerm(m, o, f, howMuch)[q, g][perm$N]}
+ DecEpsilons(m, o, f, howMuch)[q, g][perm$N] == ite(o==q && f ==g, m[q, g][perm$N] - howMuch, m[q, g][perm$N])
+);
+
+function IncPerm<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
+
+axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {IncPerm(m, o, f, howMuch)[q, g][perm$R]}
+ IncPerm(m, o, f, howMuch)[q, g][perm$R] == ite(o==q && f ==g, m[q, g][perm$R] + howMuch, m[q, g][perm$R])
+);
+
+function IncEpsilons<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
+
+axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {IncPerm(m, o, f, howMuch)[q, g][perm$N]}
+ IncEpsilons(m, o, f, howMuch)[q, g][perm$N] == ite(o==q && f ==g, m[q, g][perm$N] + howMuch, m[q, g][perm$N])
+);
+
+function Havocing<T,U>(h: HeapType, o: ref, f: Field T, newValue: U) returns (HeapType);
+
+axiom (forall<T,U> h: HeapType, o: ref, f: Field T, newValue: U, q: ref, g: Field U :: {Havocing(h, o, f, newValue)[q, g]}
+ Havocing(h, o, f, newValue)[q, g] == ite(o==q && f ==g, newValue, h[q, g])
+);
+
+function Call$Heap(int) returns (HeapType);
+function Call$Mask(int) returns (MaskType);
+function Call$Credits(int) returns (CreditsType);
+function Call$Args(int) returns (ArgSeq);
+type ArgSeq = <T>[int]T;
+
+function EmptyMask(m: MaskType) returns (bool);
+axiom (forall m: MaskType :: {EmptyMask(m)} EmptyMask(m) <==> (forall<T> o: ref, f: Field T :: NonPredicateField(f) ==> m[o, f][perm$R]<=0 && m[o, f][perm$N]<=0));
+
+const ZeroCredits: CreditsType;
+axiom (forall o: ref :: ZeroCredits[o] == 0);
+function EmptyCredits(c: CreditsType) returns (bool);
+axiom (forall c: CreditsType :: {EmptyCredits(c)} EmptyCredits(c) <==> (forall o: ref :: o != null ==> c[o] == 0));
+
+function NonPredicateField<T>(f: Field T) returns (bool);
+function PredicateField<T>(f: Field T) returns (bool);
+axiom (forall<T> f: Field T :: NonPredicateField(f) ==> ! PredicateField(f));
+axiom (forall<T> f: Field T :: PredicateField(f) ==> ! NonPredicateField(f));
+
+function submask(m1: MaskType, m2: MaskType) returns (bool);
+axiom (forall m1: MaskType, m2: MaskType :: {submask(m1, m2)}
+ submask(m1, m2) <==> (forall<T> o: ref, f: Field T :: (m1[o, f][perm$R] < m2[o, f][perm$R]) || (m1[o, f][perm$R] == m2[o, f][perm$R] && m1[o, f][perm$N] <= m2[o, f][perm$N]))
+);"""
+}
+object IfThenElsePL extends PreludeComponent {
+ val text = """
// ---------------------------------------------------------------
// -- If then else -----------------------------------------------
// ---------------------------------------------------------------
function ite<T>(bool, T, T) returns (T);
axiom (forall<T> con: bool, a: T, b: T :: {ite(con, a, b)} con ==> ite(con, a, b) == a);
-axiom (forall<T> con: bool, a: T, b: T :: {ite(con, a, b)} ! con ==> ite(con, a, b) == b);
+axiom (forall<T> con: bool, a: T, b: T :: {ite(con, a, b)} ! con ==> ite(con, a, b) == b);"""
+}
+object ArithmeticPL extends PreludeComponent {
+ val text = """
+// ---------------------------------------------------------------
+// -- Arithmetic -------------------------------------------------
+// ---------------------------------------------------------------
+// the connection between % and /
+axiom (forall x:int, y:int :: {x % y} {x / y} x % y == x - x / y * y);
+
+// sign of denominator determines sign of remainder
+axiom (forall x:int, y:int :: {x % y} 0 < y ==> 0 <= x % y && x % y < y);
+axiom (forall x:int, y:int :: {x % y} y < 0 ==> y < x % y && x % y <= 0);
+
+// the following axiom has some unfortunate matching, but it does state a property about % that
+// is sometime useful
+axiom (forall a: int, b: int, d: int :: { a % d, b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b);"""
+}
+object AxiomatizationOfSequencesPL extends PreludeComponent {
+ val text = """
// ---------------------------------------------------------------
// -- Axiomatization of sequences --------------------------------
// ---------------------------------------------------------------
@@ -214,88 +400,7 @@ function Seq#Range(min: int, max: int) returns (Seq int); axiom (forall min: int, max: int :: { Seq#Length(Seq#Range(min, max)) } (min < max ==> Seq#Length(Seq#Range(min, max)) == max-min) && (max <= min ==> Seq#Length(Seq#Range(min, max)) == 0));
axiom (forall min: int, max: int, j: int :: { Seq#Index(Seq#Range(min, max), j) } 0<=j && j<max-min ==> Seq#Index(Seq#Range(min, max), j) == min + j);
-// ---------------------------------------------------------------
-// -- Permissions ------------------------------------------------
-// ---------------------------------------------------------------
-
-axiom (forall h: HeapType, m: MaskType, o: ref, q: ref :: {wf(h, m), h[o, mu], h[q, mu]} wf(h, m) && o!=q && (0 < h[o, held] || h[o, rdheld]) && (0 < h[q, held] || h[q, rdheld]) ==> h[o, mu] != h[q, mu]);
-
-function DecPerm<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
-
-axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {DecPerm(m, o, f, howMuch)[q, g][perm$R]}
- DecPerm(m, o, f, howMuch)[q, g][perm$R] == ite(o==q && f ==g, m[q, g][perm$R] - howMuch, m[q, g][perm$R])
-);
-
-function DecEpsilons<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
-
-axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {DecPerm(m, o, f, howMuch)[q, g][perm$N]}
- DecEpsilons(m, o, f, howMuch)[q, g][perm$N] == ite(o==q && f ==g, m[q, g][perm$N] - howMuch, m[q, g][perm$N])
-);
-
-function IncPerm<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
-
-axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {IncPerm(m, o, f, howMuch)[q, g][perm$R]}
- IncPerm(m, o, f, howMuch)[q, g][perm$R] == ite(o==q && f ==g, m[q, g][perm$R] + howMuch, m[q, g][perm$R])
-);
-
-function IncEpsilons<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
-
-axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {IncPerm(m, o, f, howMuch)[q, g][perm$N]}
- IncEpsilons(m, o, f, howMuch)[q, g][perm$N] == ite(o==q && f ==g, m[q, g][perm$N] + howMuch, m[q, g][perm$N])
-);
-
-function Havocing<T,U>(h: HeapType, o: ref, f: Field T, newValue: U) returns (HeapType);
-
-axiom (forall<T,U> h: HeapType, o: ref, f: Field T, newValue: U, q: ref, g: Field U :: {Havocing(h, o, f, newValue)[q, g]}
- Havocing(h, o, f, newValue)[q, g] == ite(o==q && f ==g, newValue, h[q, g])
-);
-
-const unique joinable: Field int;
-axiom NonPredicateField(joinable);
-const unique token#t: TypeName;
-
-function Call$Heap(int) returns (HeapType);
-function Call$Mask(int) returns (MaskType);
-function Call$Credits(int) returns (CreditsType);
-function Call$Args(int) returns (ArgSeq);
-type ArgSeq = <T>[int]T;
-
-function EmptyMask(m: MaskType) returns (bool);
-axiom (forall m: MaskType :: {EmptyMask(m)} EmptyMask(m) <==> (forall<T> o: ref, f: Field T :: NonPredicateField(f) ==> m[o, f][perm$R]<=0 && m[o, f][perm$N]<=0));
-
-const ZeroCredits: CreditsType;
-axiom (forall o: ref :: ZeroCredits[o] == 0);
-function EmptyCredits(c: CreditsType) returns (bool);
-axiom (forall c: CreditsType :: {EmptyCredits(c)} EmptyCredits(c) <==> (forall o: ref :: o != null ==> c[o] == 0));
-
-function NonPredicateField<T>(f: Field T) returns (bool);
-function PredicateField<T>(f: Field T) returns (bool);
-axiom (forall<T> f: Field T :: NonPredicateField(f) ==> ! PredicateField(f));
-axiom (forall<T> f: Field T :: PredicateField(f) ==> ! NonPredicateField(f));
-
-function submask(m1: MaskType, m2: MaskType) returns (bool);
-
-axiom (forall m1: MaskType, m2: MaskType :: {submask(m1, m2)}
- submask(m1, m2) <==> (forall<T> o: ref, f: Field T :: (m1[o, f][perm$R] < m2[o, f][perm$R]) || (m1[o, f][perm$R] == m2[o, f][perm$R] && m1[o, f][perm$N] <= m2[o, f][perm$N]))
-);
-
-// ---------------------------------------------------------------
-// -- Arithmetic -------------------------------------------------
-// ---------------------------------------------------------------
-
-// the connection between % and /
-axiom (forall x:int, y:int :: {x % y} {x / y} x % y == x - x / y * y);
-
-// sign of denominator determines sign of remainder
-axiom (forall x:int, y:int :: {x % y} 0 < y ==> 0 <= x % y && x % y < y);
-axiom (forall x:int, y:int :: {x % y} y < 0 ==> y < x % y && x % y <= 0);
-
-// the following axiom has some unfortunate matching, but it does state a property about % that
-// is sometime useful
-axiom (forall a: int, b: int, d: int :: { a % d, b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b);
-
-// ---------------------------------------------------------------
-// -- End of prelude ---------------------------------------------
-// ---------------------------------------------------------------
-"""
+axiom (forall<T> x, y: T ::
+ { Seq#Contains(Seq#Singleton(x),y) }
+ Seq#Contains(Seq#Singleton(x),y) <==> x==y);"""
}
diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala index 17e81923..bc7f2811 100644 --- a/Chalice/src/PrettyPrinter.scala +++ b/Chalice/src/PrettyPrinter.scala @@ -183,13 +183,19 @@ object PrintProgram { case Unfold(e) =>
print("unfold "); Expr(e); println(Semi)
case CallAsync(declaresLocal, token, obj, name, args) =>
- print("call async ");
+ print("fork ");
if (token != null) {
Expr(token); print(" := ");
}
Expr(obj); print("."); print(name); print("("); ExprList(args); print(")");
case JoinAsync(lhs, token) =>
- print("join async "); ExprList(lhs); print(" := "); Expr(token);
+ print("join ");
+ if (lhs != null && !lhs.isEmpty) {
+ ExprList(lhs);
+ print(" := ");
+ }
+ Expr(token);
+ println(Semi)
case Wait(obj, id) =>
print("wait ")
MemberSelect(obj, id, 0, false)
@@ -257,20 +263,26 @@ object PrintProgram { case _:Result => print("result")
case VariableExpr(id) => print(id)
case MemberAccess(e,f) => MemberSelect(e,f,contextBindingPower,fragileContext)
- case Full | Epsilon =>
- case Frac(e) => print(", "); Expr(e)
- case Star => print(", *")
- case Epsilons(e) => print(", "); Expr(e)
- case Access(e, p:Write) => print("acc("); Expr(e); Expr(p); print(")")
- case Access(e, p:Read) => print("rd("); Expr(e); Expr(p); print(")")
- case AccessAll(obj, p:Write) => print("acc("); Expr(obj); print(".*"); Expr(p); print(")")
- case AccessAll(obj, p:Read) => print("rd("); Expr(obj); print(".*"); Expr(p); print(")")
- case AccessSeq(s, f, p:Write) => print("acc("); Expr(s); print("[*].");
+ case Full => print("100");
+ case Epsilon => print("rd");
+ case MethodEpsilon => print("rd");
+ case Frac(e) => Expr(e);
+ case Star => print("rd(*)")
+ case ChannelEpsilon(None) | PredicateEpsilon(None) | MonitorEpsilon(None) => print("rd");
+ case ChannelEpsilon(Some(e)) => print("rd("); Expr(e); print(")");
+ case PredicateEpsilon(Some(e)) => print("rd("); Expr(e); print(")");
+ case MonitorEpsilon(Some(e)) => print("rd("); Expr(e); print(")");
+ case ForkEpsilon(tk) => print("rd("); Expr(tk); print(")");
+ case PermPlus(e0, e1) => BinExpr(e0, e1, "+", 0x50, false, false, contextBindingPower, fragileContext)
+ case PermMinus(e0, e1) => BinExpr(e0, e1, "-", 0x50, false, true, contextBindingPower, fragileContext)
+ case PermTimes(e0, e1) => BinExpr(e0, e1, "*", 0x60, false, false, contextBindingPower, fragileContext)
+ case IntPermTimes(n, p) => BinExpr(n, p, "*", 0x60, false, false, contextBindingPower, fragileContext)
+ case Epsilons(e) => print("rd("); Expr(e); print(")");
+ case Access(e, p) => print("acc("); Expr(e); print(", "); Expr(p); print(")")
+ case AccessAll(obj, p) => print("acc("); Expr(obj); print(", "); print(".*"); Expr(p); print(")")
+ case AccessSeq(s, f, p) => print("acc("); Expr(s); print(", "); print("[*].");
f match { case None => print("*"); case Some(x) => print(x)}
Expr(p); print(")")
- case AccessSeq(s, f, p:Read) => print("rd("); Expr(s); print("[*].");
- f match { case None => print("*"); case Some(x) => print(x)}
- Expr(p); print(")")
case Credit(e, n) =>
print("credit("); Expr(e)
n match { case None => case Some(n) => print(", "); Expr(n) }
@@ -338,7 +350,7 @@ object PrintProgram { {
case AcquireState(obj) => Expr(obj); print(".acquire");
case ReleaseState(obj) => Expr(obj); print(".release");
- case CallState(token, obj, id, args) => Expr(token); print(".joinable"); print(", "); Expr(obj); print("." + id + "("); ExprList(args); print(")");
+ case CallState(token, obj, id, args) => Expr(token); print(".fork"); print(" "); Expr(obj); print("." + id + "("); ExprList(args); print(")");
}); print(", "); Expr(e); print(")");
}
def MemberSelect(e: Expression, f: String, contextBindingPower: Int, fragileContext: Boolean) = e match {
@@ -351,6 +363,11 @@ object PrintProgram { ParenExpr(power, context, fragileContext,
{ Expr(bin.E0, power, fragileLeft); print(" " + op + " "); Expr(bin.E1, power, fragileRight) })
}
+ def BinExpr(left: Expression, right: Expression, op: String, power: Int, fragileLeft: Boolean, fragileRight: Boolean,
+ context: Int, fragileContext: Boolean) = {
+ ParenExpr(power, context, fragileContext,
+ { Expr(left, power, fragileLeft); print(" " + op + " "); Expr(right, power, fragileRight) })
+ }
def ParenExpr(power: Int, context: Int, fragileContext: Boolean, pe: =>Unit) {
val ap = power & 0xF0;
val cp = context & 0xF0;
diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala index bfd9ca99..efb19700 100644 --- a/Chalice/src/Resolver.scala +++ b/Chalice/src/Resolver.scala @@ -18,7 +18,7 @@ object Resolver { sealed class ProgramContext(val decls: Map[String,TopLevelDecl], val currentClass: Class,
val currentMember: Member, val errors: ListBuffer[(Position,String)]) {
final def AddVariable(v: Variable): ProgramContext = new LProgramContext(v, this);
- final def Error(pos: Position, msg: String) {errors.append((pos, msg))}
+ final def Error(pos: Position, msg: String) {errors += ((pos, msg))}
final def SetClass(cl: Class): ProgramContext = new MProgramContext(cl, null, this)
final def SetMember(m: Member): ProgramContext = {
var ctx:ProgramContext = new MProgramContext(currentClass, m, this)
@@ -150,15 +150,39 @@ object Resolver { case _: CouplingInvariant =>
case Field(_, t, _) =>
ResolveType(t, baseContext)
- case Method(_, ins, outs, _, _) =>
- for (v <- ins ++ outs) ResolveType(v.t, baseContext)
+ case Method(id, ins, outs, _, _) =>
+ val ids = scala.collection.mutable.Set.empty[String]
+ for (v <- ins ++ outs) {
+ ResolveType(v.t, baseContext)
+ if (ids contains v.Id) {
+ return Errors(List((m.pos, "duplicate parameter " + v.Id + " of method " + id + " in class " + cl.id)))
+ } else {
+ ids += v.Id
+ }
+ }
case _: Condition =>
case _: Predicate =>
case Function(id, ins, out, specs, _) =>
- for (v <- ins) ResolveType(v.t, baseContext)
+ val ids = scala.collection.mutable.Set.empty[String]
+ for (v <- ins) {
+ ResolveType(v.t, baseContext)
+ if (ids contains v.Id) {
+ return Errors(List((m.pos, "duplicate parameter " + v.Id + " of function " + id + " in class " + cl.id)))
+ } else {
+ ids += v.Id
+ }
+ }
ResolveType(out, baseContext)
case mt: MethodTransform =>
- for (v <- mt.ins ++ mt.outs) ResolveType(v.t, baseContext)
+ val ids = scala.collection.mutable.Set.empty[String]
+ for (v <- mt.ins ++ mt.outs) {
+ ResolveType(v.t, baseContext)
+ if (ids contains v.Id) {
+ return Errors(List((m.pos, "duplicate parameter " + v.Id + " of method transform " + mt.Id + " in class " + cl.id)))
+ } else {
+ ids += v.Id
+ }
+ }
}
}
@@ -189,7 +213,7 @@ object Resolver { case Precondition(e) => ResolveExpr(e, context, false, true)(false)
case Postcondition(e) => ResolveExpr(e, context, true, true)(false)
case lc@LockChange(ee) =>
- if(m.id == runMethod) context.Error(lc.pos, "lockchange not allowed on method run")
+ if (m.id == runMethod) context.Error(lc.pos, "lockchange not allowed on method run")
ee foreach (e => ResolveExpr(e, context, true, false)(false))
}
ResolveStmt(BlockStmt(body), context)
@@ -294,11 +318,14 @@ object Resolver { case Assume(e) =>
ResolveExpr(e, context, true, true)(false)
if (!e.typ.IsBool) context.Error(e.pos, "assume statement requires a boolean expression (found " + e.typ.FullName + ")")
- case RefinementBlock(ss, _) => throw new Exception("unexpected statement")
+ case RefinementBlock(ss, _) => throw new InternalErrorException("unexpected statement")
case BlockStmt(ss) =>
var ctx = context
for (s <- ss) s match {
case l @ LocalVar(v, rhs) =>
+ if (ctx.LookupVariable(v.id).isDefined) {
+ context.Error(l.pos, "local variable name "+v.id+" collides with parameter or other local variable")
+ }
ResolveType(v.t, ctx)
val oldCtx = ctx
ctx = ctx.AddVariable(v)
@@ -340,7 +367,7 @@ object Resolver { ResolveStmt(thn, context)
els match { case None => case Some(s) => ResolveStmt(s, context) }
case w@ WhileStmt(guard, invs, ref, lkch, body) =>
- if (ref.size > 0) throw new Exception("unexpected statement")
+ if (ref.size > 0) throw new InternalErrorException("unexpected statement")
ResolveExpr(guard, context, false, false)(false)
if (!guard.typ.IsBool) context.Error(guard.pos, "while statement requires a boolean guard (found " + guard.typ.FullName + ")")
CheckNoGhost(guard, context)
@@ -370,8 +397,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 _:LocalVar => throw new Exception("unexpected LocalVar; should have been handled in BlockStmt above")
- case _:SpecStmt => throw new Exception("should have been handled before")
+ case _:LocalVar => throw new InternalErrorException("unexpected LocalVar; should have been handled in BlockStmt above")
+ case _:SpecStmt => throw new InternalErrorException("should have been handled before")
case c @ Call(declaresLocal, lhs, obj, id, args) =>
ResolveExpr(obj, context, false, false)(false)
CheckNoGhost(obj, context)
@@ -630,6 +657,188 @@ object Resolver { context.Error(lhs.pos, "type mismatch in assignment, lhs=" + lhs.typ.FullName + " rhs=" + rhs.typ.FullName)
if (lhs.v != null && !lhs.v.isGhost) CheckNoGhost(rhs, context)
}
+
+ // ResolvePermissionExpr resolves all parts of a permission expression, and replaces arithmetic operations
+ // by the appropriate operation on permissions
+ // Note that the parsing of permissions can be highly inaccurate. Besides historic reasons, we also need type information
+ // to decide how rd(x) inside acc(o.f, ***) should be interpreted. If x is an integer expression, it stands for Epsilons(x),
+ // but x could also be a channel, monitor or predicate.
+ // For instance, acc(x,rd(n)) is parsed to
+ // Access(MemberAccess(ImplicitThisExpr(),x),Frac(Access(MemberAccess(ImplicitThisExpr(),n),Epsilon)))
+ // These error during parsing are corrected here during the resolve process. In particular, the following corrections are done:
+ // - Plus and Minus are replaced by the corresponding operation on permission (i.e. PermPlus and PermMinus)
+ // - Integer expressions x are replaced by Frac(x)
+ def ResolvePermissionExpr(e: Expression, context: ProgramContext, twoStateContext: Boolean,
+ specContext: Boolean, pos: Position)(implicit inPredicate: Boolean): Permission = e match {
+ case ve @ VariableExpr(id) =>
+ ResolvePermissionExpr(Frac(ve), context, twoStateContext, specContext, pos)(inPredicate);
+ case f @ Frac(perm) =>
+ ResolveExpr(perm, context, twoStateContext, false);
+ if(perm.typ != IntClass)
+ context.Error(pos, "fraction in permission must be of type integer")
+ f
+ case sel @ MemberAccess(e, id) =>
+ ResolvePermissionExpr(Frac(sel), context, twoStateContext, specContext, pos)(inPredicate);
+ case ep @ Epsilons(exp) =>
+ ResolveExpr(exp, context, twoStateContext, false)
+ var p: Permission = Epsilon
+ exp.typ match {
+ case BoolClass if exp.isInstanceOf[MemberAccess] && exp.asInstanceOf[MemberAccess].isPredicate =>
+ p = PredicateEpsilon(Some(exp.asInstanceOf[MemberAccess]))
+ p.pos = ep.pos
+ case IntClass =>
+ p = Epsilons(exp)
+ p.pos = ep.pos
+ case TokenClass(c, m) =>
+ p = ForkEpsilon(exp)
+ p.pos = ep.pos
+ case c:Channel =>
+ p = ChannelEpsilon(Some(exp))
+ p.pos = ep.pos
+ case c:Class if (c.IsNormalClass) =>
+ p = MonitorEpsilon(Some(exp))
+ p.pos = ep.pos
+ case _ =>
+ p = Star
+ context.Error(ep.pos, "type " + exp.typ.FullName + " is not supported inside a rd expression.");
+ }
+ exp.pos = ep.pos
+ p
+ case f @ Full => f
+ case f:PredicateEpsilon => f
+ case f:ForkEpsilon => f
+ case f:ChannelEpsilon => f
+ case f:MonitorEpsilon => f
+ case Epsilon => Epsilon
+ case MethodEpsilon => MethodEpsilon
+ case f @ Star => f
+ case p @ Plus(ee0, ee1) =>
+ if (ContainsStar(ee0) || ContainsStar(ee1))
+ context.Error(p.pos, "rd* is not allowed inside permission expressions.")
+ val e0 = ResolvePermissionExpr(ee0, context, twoStateContext, specContext, pos)(inPredicate);
+ val e1 = ResolvePermissionExpr(ee1, context, twoStateContext, specContext, pos)(inPredicate);
+ val pp = PermPlus(e0, e1)
+ pp.pos = p.pos;
+ pp
+ case p @ Minus(ee0, ee1) =>
+ if (ContainsStar(ee0) || ContainsStar(ee1))
+ context.Error(p.pos, "rd* is not allowed inside permission expressions.")
+ val e0 = ResolvePermissionExpr(ee0, context, twoStateContext, specContext, pos)(inPredicate);
+ val e1 = ResolvePermissionExpr(ee1, context, twoStateContext, specContext, pos)(inPredicate);
+ val pp = PermMinus(e0, e1)
+ pp.pos = p.pos;
+ pp
+ case a @ Access(sel @ MemberAccess(e, id),Epsilon) =>
+ var exp: Expression = sel
+ var typ: Class = null
+ if (e.getClass == classOf[ImplicitThisExpr]) { // id could be a local variable, if e == ImplicitThisExpr()
+ val ve = VariableExpr(id)
+ context.LookupVariable(id) match {
+ case Some(v) => ve.Resolve(v); typ = ve.typ; exp = ve;
+ case None =>
+ }
+ }
+ if (typ == null) {
+ ResolveExpr(e, context, twoStateContext, false)
+ e.typ.LookupMember(id) match {
+ case None =>
+ context.Error(sel.pos, "undeclared member " + id + " in class " + e.typ.FullName)
+ case Some(f: Field) => sel.f = f; typ = f.typ.typ
+ case Some(pred@Predicate(id, body)) =>
+ sel.predicate = pred;
+ sel.isPredicate = true;
+ typ = BoolClass
+ case _ => context.Error(sel.pos, "field-select expression does not denote a field: " + e.typ.FullName + "." + id);
+ }
+ sel.typ = typ
+ exp = sel
+ }
+ var p: Permission = Epsilon
+ typ match {
+ case BoolClass if sel.isPredicate =>
+ p = PredicateEpsilon(Some(sel))
+ p.pos = a.pos
+ case IntClass =>
+ p = Epsilons(exp)
+ p.pos = a.pos
+ case TokenClass(c, m) =>
+ p = ForkEpsilon(exp)
+ p.pos = a.pos
+ case c:Channel =>
+ p = ChannelEpsilon(Some(exp))
+ p.pos = a.pos
+ case c:Class if (c.IsNormalClass) =>
+ p = MonitorEpsilon(Some(exp))
+ p.pos = a.pos
+ case _ =>
+ context.Error(a.pos, "type " + typ.FullName + " of variable " + id + " is not supported inside a rd expression.")
+ p = Star
+ }
+ exp.pos = a.pos
+ p
+ // multiplication is a bit tricky: we want to support integer multiplication i0*i1 (which will
+ // correspond to a percentage i0*i1), but also the multiplication of an integer i0 with a permission
+ // amount p1 (and vice versa): i0*p1 or p0*i1.
+ // we first try to resolve both expressions as integer, and if not successful, try again as
+ // permission amount
+ case bin @ Times(e0, e1) =>
+ var p0, p1: Permission = null
+ var ee0 = e0
+ var ee1 = e1
+ var oldErrors = (new ListBuffer[(Position,String)]) ++= context.errors
+ ResolveExpr(bin.E0, context, twoStateContext, false)
+ if (context.errors.size > oldErrors.size) {
+ context.errors.clear; context.errors ++= oldErrors // reset errors
+ p0 = ResolvePermissionExpr(bin.E0, context, twoStateContext, specContext, pos)(inPredicate)
+ ee0 = p0
+ }
+
+ oldErrors = (new ListBuffer[(Position,String)]) ++= context.errors
+ ResolveExpr(bin.E1, context, twoStateContext, false)
+ if (context.errors.size > oldErrors.size) {
+ context.errors.clear; context.errors ++= oldErrors // reset errors
+ p1 = ResolvePermissionExpr(bin.E1, context, twoStateContext, specContext, pos)(inPredicate)
+ ee1 = p1
+ }
+
+ if (ee0.typ.IsInt && ee1.typ.IsInt) {
+ bin.typ = IntClass
+ val pp = Frac(bin)
+ pp.pos = bin.pos
+ pp
+ } else if (ee0.typ.IsInt && ee1.typ.IsPermission) {
+ val pp = IntPermTimes(ee0,p1)
+ pp.pos = bin.pos
+ pp
+ } else if (ee0.typ.IsPermission && ee1.typ.IsInt) {
+ val pp = IntPermTimes(ee1,p0)
+ pp.pos = bin.pos
+ pp
+ } else {
+ context.Error(pos, "multiplication of permission amounts not supported"); Star
+ }
+ case expr =>
+ ResolveExpr(expr, context, twoStateContext, specContext)(inPredicate);
+ if (expr.typ == IntClass) {
+ val pp = Frac(expr)
+ pp.pos = expr.pos;
+ pp
+ } else {
+ context.Error(pos, "expression of type " + expr.typ.FullName + " invalid in permission"); Star
+ }
+ }
+
+ // does e contain a Star (i.e., rd*)?
+ def ContainsStar(expr: Expression): Boolean = {
+ var x: Boolean = false
+ AST.visit(expr,
+ e => e match {
+ case Star => x = true
+ case _ =>
+ }
+ )
+ x
+ }
// ResolveExpr resolves all parts of an RValue, if possible, and (always) sets the RValue's typ field
def ResolveExpr(e: RValue, context: ProgramContext,
@@ -707,25 +916,26 @@ object Resolver { case _ => context.Error(sel.pos, "field-select expression does not denote a field: " + e.typ.FullName + "." + id);
}
sel.typ = typ
- case Frac(perm) => ResolveExpr(perm, context, twoStateContext, false);
- case Epsilons(perm) => ResolveExpr(perm, context, twoStateContext, false);
- case Full | Epsilon | Star => ;
+ case p: Permission => context.Error(p.pos, "permission not expected here.")
case expr @ Access(e, perm) =>
- if (!specContext) context.Error(expr.pos, (perm match {case _:Read => "rd"; case _:Write => "acc"}) + " expression is allowed only in positive predicate contexts")
+ if (!specContext) context.Error(expr.pos, permExpressionName(perm) + " expression is allowed only in positive predicate contexts")
ResolveExpr(e, context, twoStateContext, true)
- ResolveExpr(perm, context, twoStateContext, false);
+ val p = ResolvePermissionExpr(perm match { case Frac(f) => f; case o => o;}, context, twoStateContext, false, expr.pos);
+ expr.perm = p;
expr.typ = BoolClass
case expr @ AccessAll(obj, perm) =>
- if (!specContext) context.Error(expr.pos, (perm match {case _:Read => "rd"; case _:Write => "acc"}) + " expression is allowed only in positive predicate contexts")
+ if (!specContext) context.Error(expr.pos, permExpressionName(perm) + " expression is allowed only in positive predicate contexts")
ResolveExpr(obj, context, twoStateContext, false)
if(!obj.typ.IsRef) context.Error(expr.pos, "Target of .* must be object reference.")
- ResolveExpr(perm, context, twoStateContext, false);
+ val p = ResolvePermissionExpr(perm match { case Frac(f) => f; case o => o;}, context, twoStateContext, false, expr.pos);
+ expr.perm = p;
expr.typ = BoolClass
case expr @ AccessSeq(s, f, perm) =>
- if (!specContext) context.Error(expr.pos, (perm match {case _:Read => "rd"; case _:Write => "acc"}) + " expression is allowed only in positive predicate contexts")
+ if (!specContext) context.Error(expr.pos, permExpressionName(perm) + " expression is allowed only in positive predicate contexts")
ResolveExpr(s, context, twoStateContext, false)
if(!s.typ.IsSeq) context.Error(expr.pos, "Target of [*] must be sequence.")
- ResolveExpr(perm, context, twoStateContext, false);
+ val p = ResolvePermissionExpr(perm match { case Frac(f) => f; case o => o;}, context, twoStateContext, false, expr.pos);
+ expr.perm = p;
f match {
case Some(x) =>
ResolveExpr(x, context, twoStateContext, true);
@@ -1010,8 +1220,25 @@ object Resolver { case MemberAccess(e, id) =>
CheckRunSpecification(e, context, false)
case Frac(perm) => CheckRunSpecification(perm, context, false)
- case Epsilons(perm) => CheckRunSpecification(perm, context, false)
- case Full | Epsilon | Star =>
+ case Epsilons(perm) => CheckRunSpecification(perm, context, false)
+ case PermPlus(p0, p1) =>
+ CheckRunSpecification(p0, context, false)
+ CheckRunSpecification(p1, context, false)
+ case PermMinus(p0, p1) =>
+ CheckRunSpecification(p0, context, false)
+ CheckRunSpecification(p1, context, false)
+ case PermTimes(p0, p1) =>
+ CheckRunSpecification(p0, context, false)
+ CheckRunSpecification(p1, context, false)
+ case IntPermTimes(p0, p1) =>
+ CheckRunSpecification(p0, context, false)
+ CheckRunSpecification(p1, context, false)
+ case Full | Epsilon | Star | MethodEpsilon =>
+ case ChannelEpsilon(None) | PredicateEpsilon(None) | MonitorEpsilon(None) =>;
+ case ChannelEpsilon(Some(e)) => CheckRunSpecification(e, context, false);
+ case PredicateEpsilon(Some(e)) => CheckRunSpecification(e, context, false);
+ case MonitorEpsilon(Some(e)) => CheckRunSpecification(e, context, false);
+ case ForkEpsilon(tk) => CheckRunSpecification(tk, context, false);
case Access(e, perm) =>
CheckRunSpecification(e, context, false);
CheckRunSpecification(perm, context, false);
@@ -1081,7 +1308,7 @@ object Resolver { context.Error(e.pos, "Method refinement cannot add a pre-condition")
case Postcondition(e) =>
ResolveExpr(e, context.SetClass(mt.Parent).SetMember(mt), true, true)(false)
- case _ : LockChange => throw new Exception("not implemented")
+ case _ : LockChange => throw new NotSupportedException("not implemented")
}
if (mt.ins != mt.refines.Ins) context.Error(mt.pos, "Refinement must have same input arguments")
if (! mt.outs.startsWith(mt.refines.Outs)) context.Error(mt.pos, "Refinement must declare all abstract output variables")
@@ -1127,7 +1354,7 @@ object Resolver { }
}
}
- resolveBody(mt.body, context.SetClass(mt.Parent).SetMember(mt), mt.refines.Outs)
+ resolveBody(mt.body, context.SetClass(mt.Parent).SetMember(mt), Nil)
}
def ResolveCouplingInvariant(ci: CouplingInvariant, cl: Class, context: ProgramContext) {
@@ -1142,4 +1369,20 @@ object Resolver { // TODO: check coupling invariant may only give permissions to newly declared fields
// TODO: check concrete body cannot refer to replaced fields
}
+
+ // TODO: this method might need to be replaced at some point. it is not possible
+ // to decide what name is used on the source level just by the permission (e.g.,
+ // Epsilons can be rd(x,1) or acc(x,rd(1))
+ def permExpressionName(perm: Permission): String = {
+ perm match {
+ case _:Epsilons => "rd";
+ case Epsilon => "rd";
+ case MethodEpsilon => "rd"
+ case Star => "rd";
+ case Full => "acc";
+ case _:Frac => "acc";
+ case _:ArithmeticPermission => "acc";
+ case _:ChannelEpsilon | _:ForkEpsilon | _:MonitorEpsilon | _:PredicateEpsilon => "acc";
+ }
+ }
}
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index 3b6187cb..5e9943a0 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -66,7 +66,7 @@ class Translator { case inv: MonitorInvariant =>
Nil // already dealt with before
case _: Condition =>
- throw new Exception("not yet implemented")
+ throw new NotSupportedException("not yet implemented")
case mt: MethodTransform =>
translateMethodTransform(mt)
case ci: CouplingInvariant =>
@@ -80,20 +80,26 @@ class Translator { val (h1V, h1) = NewBVar("h1", theap, true); val (m1V, m1) = NewBVar("m1", tmask, true);
val (c1V, c1) = NewBVar("c1", tcredits, true);
val (lkV, lk) = NewBVar("lk", tref, true);
+
+ // pick new k
+ val (methodKV, methodK) = Boogie.NewBVar("methodK", tint, true)
+ val methodKStmts = BLocal(methodKV) :: bassume(0 < methodK && 1000*methodK < permissionOnePercent)
+
val oldTranslator = new ExpressionTranslator(List(h1, m1, c1), List(h0, m0, c0), currentClass);
Proc(currentClass.id + "$monitorinvariant$checkDefinedness",
List(NewBVarWhere("this", new Type(currentClass))),
Nil,
GlobalNames,
DefaultPrecondition(),
+ methodKStmts :::
BLocal(h0V) :: BLocal(m0V) :: BLocal(c0V) :: BLocal(h1V) :: BLocal(m1V) :: BLocal(c1V) :: BLocal(lkV) ::
bassume(wf(h0, m0)) :: bassume(wf(h1, m1)) ::
(oldTranslator.Mask := ZeroMask) :: (oldTranslator.Credits := ZeroCredits) ::
- oldTranslator.Inhale(invs map { mi => mi.e}, "monitor invariant", false) :::
+ oldTranslator.Inhale(invs map { mi => mi.e}, "monitor invariant", false, methodK) :::
(etran.Mask := ZeroMask) :: (etran.Credits := ZeroCredits) ::
Havoc(etran.Heap) ::
// check that invariant is well-defined
- etran.WhereOldIs(h1, m1, c1).Inhale(invs map { mi => mi.e}, "monitor invariant", true) :::
+ etran.WhereOldIs(h1, m1, c1).Inhale(invs map { mi => mi.e}, "monitor invariant", true, methodK) :::
(if (! Chalice.checkLeaks || invs.length == 0) Nil else
// check that there are no loops among .mu permissions in monitors
// !CanWrite[this,mu]
@@ -108,7 +114,7 @@ class Translator { "Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<<o.mu")
) :::
//check that invariant is reflexive
- etran.UseCurrentAsOld().Exhale(invs map {mi => (mi.e, ErrorMessage(mi.pos, "Monitor invariant might not be reflexive."))}, "invariant reflexive?", false) :::
+ etran.UseCurrentAsOld().Exhale(invs map {mi => (mi.e, ErrorMessage(mi.pos, "Monitor invariant might not be reflexive."))}, "invariant reflexive?", false, methodK, true) :::
bassert(DebtCheck(), pos, "Monitor invariant is not allowed to contain debt.")
)
}
@@ -123,6 +129,11 @@ class Translator { etran = etran.CheckTermination(! Chalice.skipTermination);
val checkBody = f.definition match {case Some(e) => isDefined(e); case None => Nil};
etran = etran.CheckTermination(false);
+
+ // pick new k
+ val (functionKV, functionK) = Boogie.NewBVar("functionK", tint, true)
+ val functionKStmts = BLocal(functionKV) :: bassume(0 < functionK && 1000*functionK < permissionOnePercent)
+
// Boogie function that represents the Chalice function
Boogie.Function(functionName(f), BVar("heap", theap) :: BVar("mask", tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar), BVar("$myresult", f.out.typ)) ::
// check definedness of the function's precondition and body
@@ -131,16 +142,17 @@ class Translator { Nil,
GlobalNames,
DefaultPrecondition(),
+ functionKStmts :::
DefinePreInitialState :::
// check definedness of the precondition
- InhaleWithChecking(Preconditions(f.spec) map { p => (if(0 < Chalice.defaults) UnfoldPredicatesWithReceiverThis(p) else p)}, "precondition") :::
+ InhaleWithChecking(Preconditions(f.spec) map { p => (if(0 < Chalice.defaults) UnfoldPredicatesWithReceiverThis(p) else p)}, "precondition", functionK) :::
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 < Chalice.defaults) UnfoldPredicatesWithReceiverThis(post) else post),
- ErrorMessage(f.pos, "Postcondition at " + post.pos + " might not hold."))}, "function postcondition")) ::
+ ErrorMessage(f.pos, "Postcondition at " + post.pos + " might not hold."))}, "function postcondition", functionK, true)) ::
// definition axiom
(f.definition match {
case Some(definition) => definitionAxiom(f, definition);
@@ -212,10 +224,10 @@ class Translator { // make sure version is of HeapType
val version = Boogie.FunctionApp("combine", List("nostate", Version(pre, etran)));
val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)});
- val frameFunctionName = "##" + f.FullName;
+ val frameFunctionName = "#" + functionName(f);
val args = VarExpr("this") :: inArgs;
- val applyF = FunctionApp(functionName(f), List(etran.Heap, etran.Mask) ::: args);
+ val applyF = FunctionApp(functionName(f) + (if (f.isRecursive) "#limited" else ""), List(etran.Heap, etran.Mask) ::: args);
val applyFrameFunction = FunctionApp(frameFunctionName, version :: args);
Boogie.Function(frameFunctionName, Boogie.BVar("state", theap) :: Boogie.BVar("this", tref) :: (f.ins map Variable2BVar), new BVar("$myresult", f.out.typ)) ::
Axiom(new Boogie.Forall(
@@ -272,6 +284,11 @@ class Translator { }
def translatePredicate(pred: Predicate): List[Decl] = {
+
+ // pick new k
+ val (predicateKV, predicateK) = Boogie.NewBVar("predicateK", tint, true)
+ val predicateKStmts = BLocal(predicateKV) :: bassume(0 < predicateK && 1000*predicateK < permissionOnePercent)
+
// const unique class.name: HeapType;
Const(pred.FullName, true, FieldType(theap)) ::
// axiom PredicateField(f);
@@ -282,26 +299,32 @@ class Translator { Nil,
GlobalNames,
DefaultPrecondition(),
+ predicateKStmts :::
DefinePreInitialState :::
- InhaleWithChecking(List(DefinitionOf(pred)), "predicate definition"))
+ InhaleWithChecking(List(DefinitionOf(pred)), "predicate definition", predicateK))
}
def translateMethod(method: Method): List[Decl] = {
+ // pick new k for this method, that represents the fraction for read permissions
+ val (methodKV, methodK) = Boogie.NewBVar("methodK", tint, true)
+ val methodKStmts = BLocal(methodKV) :: bassume(0 < methodK && 1000*methodK < permissionOnePercent)
+
// check definedness of the method contract
Proc(method.FullName + "$checkDefinedness",
NewBVarWhere("this", new Type(currentClass)) :: (method.ins map {i => Variable2BVarWhere(i)}),
method.outs map {i => Variable2BVarWhere(i)},
GlobalNames,
DefaultPrecondition(),
+ methodKStmts :::
DefinePreInitialState :::
bassume(CanAssumeFunctionDefs) ::
// check precondition
- InhaleWithChecking(Preconditions(method.spec), "precondition") :::
+ InhaleWithChecking(Preconditions(method.spec), "precondition", methodK) :::
DefineInitialState :::
(etran.Mask := ZeroMask) :: (etran.Credits := ZeroCredits) ::
Havoc(etran.Heap) ::
// check postcondition
- InhaleWithChecking(Postconditions(method.spec), "postcondition") :::
+ InhaleWithChecking(Postconditions(method.spec), "postcondition", methodK) :::
// check lockchange
(LockChanges(method.spec) flatMap { lc => isDefined(lc)})) ::
// check that method body satisfies the method contract
@@ -310,18 +333,20 @@ class Translator { method.outs map {i => Variable2BVarWhere(i)},
GlobalNames,
DefaultPrecondition(),
+ methodKStmts :::
bassume(CurrentModule ==@ Boogie.VarExpr(ModuleName(currentClass))) ::
bassume(CanAssumeFunctionDefs) ::
DefinePreInitialState :::
- Inhale(Preconditions(method.spec) map { p => (if(0 < Chalice.defaults) UnfoldPredicatesWithReceiverThis(p) else p)}, "precondition") :::
+ Inhale(Preconditions(method.spec) map { p => (if(0 < Chalice.defaults) UnfoldPredicatesWithReceiverThis(p) else p)}, "precondition", methodK) :::
DefineInitialState :::
- translateStatements(method.body) :::
- 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") :::
+ translateStatements(method.body, methodK) :::
+ 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", methodK, true) :::
(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."))
}
+ // TODO: This method has not yet been updated to the new permission model
def translateMethodTransform(mt: MethodTransform): List[Decl] = {
// extract coupling invariants
def Invariants(e: Expression): Expression = desugar(e) match {
@@ -330,7 +355,7 @@ class Translator { case Access(ma, Full) if ! ma.isPredicate =>
val cis = for (ci <- mt.Parent.CouplingInvariants; if (ci.fields.contains(ma.f))) yield FractionOf(ci.e, ci.fraction(ma.f));
cis.foldLeft(BoolLiteral(true):Expression)(And(_,_))
- case _: PermissionExpr => throw new Exception("not supported")
+ case _: PermissionExpr => throw new NotSupportedException("not supported")
case _ => BoolLiteral(true)
}
@@ -346,13 +371,13 @@ class Translator { DefinePreInitialState :::
bassume(CanAssumeFunctionDefs) ::
// check precondition
- InhaleWithChecking(Preconditions(mt.Spec) ::: preCI, "precondition") :::
+ InhaleWithChecking(Preconditions(mt.Spec) ::: preCI, "precondition", todoiparam) :::
DefineInitialState :::
(etran.Mask := ZeroMask) :: (etran.Credits := ZeroCredits) ::
Havoc(etran.Heap) ::
// check postcondition
- InhaleWithChecking(Postconditions(mt.refines.Spec), "postcondition") :::
- tag(InhaleWithChecking(postCI ::: Postconditions(mt.spec), "postcondition"), keepTag)
+ InhaleWithChecking(Postconditions(mt.refines.Spec), "postcondition", todoiparam) :::
+ tag(InhaleWithChecking(postCI ::: Postconditions(mt.spec), "postcondition", todoiparam), keepTag)
) ::
// check correctness of refinement
Proc(mt.FullName,
@@ -364,13 +389,13 @@ class Translator { bassume(CurrentModule ==@ Boogie.VarExpr(ModuleName(currentClass))) ::
bassume(CanAssumeFunctionDefs) ::
DefinePreInitialState :::
- Inhale(Preconditions(mt.Spec) ::: preCI, "precondition") :::
+ Inhale(Preconditions(mt.Spec) ::: preCI, "precondition", todoiparam) :::
DefineInitialState :::
- translateStatements(mt.body) :::
- Exhale(Postconditions(mt.refines.Spec) map {p => (p, ErrorMessage(p.pos, "The postcondition at " + p.pos + " might not hold."))}, "postcondition") :::
+ translateStatements(mt.body, todoiparam) :::
+ Exhale(Postconditions(mt.refines.Spec) map {p => (p, ErrorMessage(p.pos, "The postcondition at " + p.pos + " might not hold."))}, "postcondition", todoiparam, todobparam) :::
tag(Exhale(
(postCI map {p => (p, ErrorMessage(mt.pos, "The coupling invariant might not be preserved."))}) :::
- (Postconditions(mt.spec) map {p => (p, ErrorMessage(p.pos, "The postcondition at " + p.pos + " might not hold."))}), "postcondition"), keepTag)
+ (Postconditions(mt.spec) map {p => (p, ErrorMessage(p.pos, "The postcondition at " + p.pos + " might not hold."))}), "postcondition", todoiparam, todobparam), keepTag)
}
)
@@ -402,9 +427,9 @@ class Translator { /**********************************************************************
***************** STATEMENTS *****************
**********************************************************************/
- def translateStatements(statements: List[Statement]): List[Stmt] = statements flatMap translateStatement
+ def translateStatements(statements: List[Statement], methodK: Expr): List[Stmt] = statements flatMap (v => translateStatement(v, methodK))
- def translateStatement(s: Statement): List[Stmt] = {
+ def translateStatement(s: Statement, methodK: Expr): List[Stmt] = {
s match {
case Assert(e) =>
val newGlobals = etran.FreshGlobals("assert");
@@ -417,23 +442,23 @@ class Translator { BLocal(tmpHeap._1) :: (tmpHeap._2 := etran.Heap) ::
BLocal(tmpMask._1) :: (tmpMask._2 := etran.Mask) ::
BLocal(tmpCredits._1) :: (tmpCredits._2 := etran.Credits) ::
- tmpTranslator.Exhale(List((e, ErrorMessage(s.pos, "Assertion might not hold."))), "assert", true)
+ tmpTranslator.Exhale(List((e, ErrorMessage(s.pos, "Assertion might not hold."))), "assert", true, methodK, true)
case Assume(e) =>
Comment("assume") ::
isDefined(e) :::
bassume(e)
case BlockStmt(ss) =>
- translateStatements(ss)
+ translateStatements(ss, methodK)
case IfStmt(guard, then, els) =>
- val tt = translateStatement(then)
+ val tt = translateStatement(then, methodK)
val et = els match {
case None => Nil
- case Some(els) => translateStatement(els) }
+ case Some(els) => translateStatement(els, methodK) }
Comment("if") ::
isDefined(guard) :::
Boogie.If(guard, tt, et)
case w: WhileStmt =>
- translateWhile(w)
+ translateWhile(w, methodK)
case Assign(lhs, rhs) =>
def assignOrAssumeEqual(r: Boogie.Expr): List[Boogie.Stmt] = {
if (lhs.v.isImmutable) {
@@ -474,9 +499,9 @@ class Translator { { lv.rhs match {
//update the local, provided a rhs was provided
case None => Nil
- case Some(rhs) => translateStatement(Assign(new VariableExpr(lv.v), rhs)) }}
+ case Some(rhs) => translateStatement(Assign(new VariableExpr(lv.v), rhs), methodK) }}
case s: SpecStmt => translateSpecStmt(s)
- case c: Call => translateCall(c)
+ case c: Call => translateCall(c, methodK)
case Install(obj, lowerBounds, upperBounds) =>
Comment("install") ::
isDefined(obj) :::
@@ -494,7 +519,7 @@ class Translator { UpdateMu(obj, true, false, lowerBounds, upperBounds, ErrorMessage(s.pos, "Share might fail.")) :::
bassume(!isHeld(obj) && ! isRdHeld(obj)) :: // follows from o.mu==lockbottom
// exhale the monitor invariant (using the current state as the old state)
- ExhaleInvariants(obj, false, ErrorMessage(s.pos, "Monitor invariant might not hold."), etran.UseCurrentAsOld()) :::
+ ExhaleInvariants(obj, false, ErrorMessage(s.pos, "Monitor invariant might not hold."), etran.UseCurrentAsOld(), methodK) :::
// assume a seen state is the one right before the share
bassume(LastSeenHeap(etran.Heap.select(obj, "mu"), etran.Heap.select(obj, "held")) ==@ etran.Heap) ::
bassume(LastSeenMask(etran.Heap.select(obj, "mu"), etran.Heap.select(obj, "held")) ==@ preShareMask) ::
@@ -518,12 +543,12 @@ class Translator { Comment("acquire") ::
isDefined(obj) :::
bassert(nonNull(TrExpr(obj)), s.pos, "The target of the acquire statement might be null.") ::
- TrAcquire(s, obj)
+ TrAcquire(s, obj, methodK)
case Release(obj) =>
Comment("release") ::
isDefined(obj) :::
bassert(nonNull(TrExpr(obj)), s.pos, "The target of the release statement might be null.") ::
- TrRelease(s, obj)
+ TrRelease(s, obj, methodK)
case Lock(e, body, readonly) =>
val objV = new Variable("lock", new Type(e.typ))
val obj = new VariableExpr(objV)
@@ -534,25 +559,25 @@ class Translator { BLocal(Variable2BVar(objV)) :: (o := TrExpr(e)) ::
bassert(nonNull(o), s.pos, "The target of the " + sname + " statement might be null.") ::
{ if (readonly) {
- TrRdAcquire(s, obj) :::
- translateStatement(body) :::
- TrRdRelease(s, obj)
+ TrRdAcquire(s, obj, methodK) :::
+ translateStatement(body, methodK) :::
+ TrRdRelease(s, obj, methodK)
} else {
- TrAcquire(s, obj) :::
- translateStatement(body) :::
- TrRelease(s, obj)
+ TrAcquire(s, obj, methodK) :::
+ translateStatement(body, methodK) :::
+ TrRelease(s, obj, methodK)
}
}
case RdAcquire(obj) =>
Comment("rd acquire") ::
isDefined(obj) :::
bassert(nonNull(TrExpr(obj)), s.pos, "The target of the read-acquire statement might be null.") ::
- TrRdAcquire(s, obj)
+ TrRdAcquire(s, obj, methodK)
case rdrelease@RdRelease(obj) =>
Comment("rd release") ::
isDefined(obj) :::
bassert(nonNull(TrExpr(obj)), obj.pos, "The target of the read-release statement might be null.") ::
- TrRdRelease(s, obj)
+ TrRdRelease(s, obj, methodK)
case downgrade@Downgrade(obj) =>
val o = TrExpr(obj);
val prevHeapV = new Boogie.BVar("prevHeap", theap, true)
@@ -561,9 +586,9 @@ class Translator { bassert(nonNull(o), s.pos, "The target of the downgrade statement might be null.") ::
bassert(isHeld(o), s.pos, "The lock of the target of the downgrade statement might not be held by the current thread.") ::
bassert(! isRdHeld(o), s.pos, "The current thread might hold the read lock.") ::
- ExhaleInvariants(obj, false, ErrorMessage(downgrade.pos, "Monitor invariant might not hold.")) :::
+ ExhaleInvariants(obj, false, ErrorMessage(downgrade.pos, "Monitor invariant might not hold."), methodK) :::
BLocal(prevHeapV) ::
- InhaleInvariants(obj, true) :::
+ InhaleInvariants(obj, true, methodK) :::
bassume(etran.Heap ==@ new Boogie.VarExpr(prevHeapV)) ::
etran.Heap.store(o, "rdheld", true)
case Free(obj) =>
@@ -575,69 +600,35 @@ class Translator { (for (f <- obj.typ.Fields ++ RootClass.MentionableFields) yield
etran.SetNoPermission(o, f.FullName, etran.Mask))
// probably need to havoc all the fields! Do we check enough?
- case fold@Fold(acc@Access(pred@MemberAccess(e, f), fraction:Write)) =>
+ case fold@Fold(acc@Access(pred@MemberAccess(e, f), perm)) =>
val o = TrExpr(e);
- var definition = fraction match {
- case Frac(p) => FractionOf(SubstThis(DefinitionOf(pred.predicate), e), p);
- case Full => SubstThis(DefinitionOf(pred.predicate), e);
- }
+ var definition = scaleExpressionByPermission(SubstThis(DefinitionOf(pred.predicate), e), perm, fold.pos)
+
+ // pick new k
+ val (foldKV, foldK) = Boogie.NewBVar("foldK", tint, true)
Comment("fold") ::
+ BLocal(foldKV) :: bassume(0 < foldK && 1000*foldK < permissionFull) ::
isDefined(e) :::
+ isDefined(perm) :::
bassert(nonNull(o), s.pos, "The target of the fold statement might be null.") ::
- (fraction match {
- case Frac(p) => isDefined(p) :::
- bassert(0 <= etran.Tr(p), s.pos, "Fraction might be negative.") ::
- bassert(etran.Tr(p) <= 100, s.pos, "Fraction might be larger than 100.") :: Nil;
- case Full => Nil}) :::
// remove the definition from the current state, and replace by predicate itself
- Exhale(List((definition, ErrorMessage(s.pos, "Fold might fail because the definition of " + pred.predicate.FullName + " does not hold."))), "fold") :::
- Inhale(List(acc), "fold") :::
+ Exhale(List((definition, ErrorMessage(s.pos, "Fold might fail because the definition of " + pred.predicate.FullName + " does not hold."))), "fold", foldK, false) :::
+ Inhale(List(acc), "fold", foldK) :::
etran.Heap.store(o, pred.predicate.FullName, etran.Heap) :: // Is this necessary?
bassume(wf(etran.Heap, etran.Mask))
- case fld@Fold(acc@Access(pred@MemberAccess(e, f), nbEpsilons:Read)) =>
+ case unfld@Unfold(acc@Access(pred@MemberAccess(e, f), perm:Permission)) =>
val o = TrExpr(e);
- var (definition, checkEpsilons) = nbEpsilons match {
- case Epsilon => (EpsilonsOf(SubstThis(pred.predicate.definition, e), IntLiteral(1)), Nil)
- case Star => throw new Exception("Not supported yet!");
- case Epsilons(i) => (EpsilonsOf(SubstThis(DefinitionOf(pred.predicate), e), i), isDefined(i) ::: bassert(Boogie.IntLiteral(0) <= i, s.pos, "Number of epsilons might be negative.") :: Nil)
- }
- Comment("fold") ::
- isDefined(e) :::
- bassert(nonNull(o), s.pos, "The target of the fold statement might be null.") ::
- checkEpsilons :::
- Exhale(List((definition, ErrorMessage(fld.pos, "Fold might fail because the definition of " + pred.predicate.FullName + " does not hold."))), "fold") :::
- Inhale(List(acc), "fold") :::
- etran.Heap.store(e, pred.predicate.FullName, etran.Heap) ::
- bassume(wf(etran.Heap, etran.Mask))
- case unfld@Unfold(acc@Access(pred@MemberAccess(e, f), fraction:Write)) =>
- val o = TrExpr(e);
- var definition = fraction match {
- case Frac(p) => FractionOf(SubstThis(DefinitionOf(pred.predicate), e), p);
- case Full => SubstThis(DefinitionOf(pred.predicate), e);
- }
+ val definition = scaleExpressionByPermission(SubstThis(DefinitionOf(pred.predicate), e), perm, unfld.pos)
+
+ // pick new k
+ val (unfoldKV, unfoldK) = Boogie.NewBVar("unfoldK", tint, true)
Comment("unfold") ::
+ BLocal(unfoldKV) :: bassume(0 < unfoldK && unfoldK < permissionFull) ::
isDefined(e) :::
bassert(nonNull(o), s.pos, "The target of the fold statement might be null.") ::
- (fraction match {
- case Frac(p) => isDefined(p) :::
- bassert(Boogie.IntLiteral(0) <= p, s.pos, "Fraction might be negative.") ::
- bassert(p <= 100, s.pos, "Fraction might be larger than 100.") :: Nil
- case Full => Nil}) :::
- Exhale(List((acc, ErrorMessage(s.pos, "unfold might fail because the predicate " + pred.predicate.FullName + " does not hold."))), "unfold") :::
- etran.InhaleFrom(List(definition), "unfold", false, etran.Heap.select(o, pred.predicate.FullName))
- case unfld@Unfold(acc@Access(pred@MemberAccess(e, f), nbEpsilons:Read)) =>
- val o = TrExpr(e);
- var (definition, checkEpsilons) = nbEpsilons match {
- case Epsilon => (EpsilonsOf(SubstThis(DefinitionOf(pred.predicate), e), IntLiteral(1)), Nil)
- case Star => throw new Exception("Not supported yet!");
- case Epsilons(i) => (EpsilonsOf(SubstThis(DefinitionOf(pred.predicate), e), i), isDefined(i) ::: bassert(Boogie.IntLiteral(0) <= i, s.pos, "Number of epsilons might be negative.") :: Nil)
- }
- Comment("unfold") ::
- isDefined(e) :::
- bassert(nonNull(o), s.pos, "The target of the fold statement might be null.") ::
- checkEpsilons :::
- Exhale(List((acc, ErrorMessage(s.pos, "Unold might fail because the predicate " + pred.predicate.FullName + " does not hold."))), "unfold") :::
- etran.InhaleFrom(List(definition), "unfold", false, etran.Heap.select(o, pred.predicate.FullName))
+ isDefined(perm) :::
+ Exhale(List((acc, ErrorMessage(s.pos, "unfold might fail because the predicate " + pred.predicate.FullName + " does not hold."))), "unfold", unfoldK, false) :::
+ etran.InhaleFrom(List(definition), "unfold", false, etran.Heap.select(o, pred.predicate.FullName), unfoldK)
case c@CallAsync(declaresLocal, token, obj, id, args) =>
val formalThisV = new Variable("this", new Type(c.m.Parent))
val formalThis = new VariableExpr(formalThisV)
@@ -651,6 +642,11 @@ class Translator { val (preCallCreditsV, preCallCredits) = NewBVar("preCallCredits", tcredits, true)
val (argsSeqV, argsSeq) = NewBVar("argsSeq", tArgSeq, true)
val argsSeqLength = 1 + args.length;
+
+ // pick new k for this fork
+ val (asyncMethodCallKV, asyncMethodCallK) = Boogie.NewBVar("asyncMethodCallK", tint, true)
+ BLocal(asyncMethodCallKV) ::
+ bassume(0 < asyncMethodCallK) :: // upper bounds are later provided by the exhale
Comment("call " + id) ::
// declare the local variable, if needed
{ if (c.local == null)
@@ -678,25 +674,24 @@ class Translator { } :::
// exhale preconditions
Exhale(Preconditions(c.m.spec) map
- (p => SubstVars(p, formalThis, c.m.ins, formalIns)) zip (Preconditions(c.m.spec) map { p => ErrorMessage(c.pos, "The precondition at " + p.pos + " might not hold.")}), "precondition") :::
+ (p => SubstVars(p, formalThis, c.m.ins, formalIns)) zip (Preconditions(c.m.spec) map { p => ErrorMessage(c.pos, "The precondition at " + p.pos + " might not hold.")}), "precondition", asyncMethodCallK, false) :::
// create a new token
BLocal(tokenV) :: Havoc(tokenId) :: bassume(nonNull(tokenId)) ::
// the following assumes help in proving that the token is fresh
- // the first statement used to be an assume, but this caused an unsoundness in combination with the storing of a heap snapshot
- // in the location of a predicate. The assume constrained both the current heap and the snapshot, whereas the assignment
- // changes only the current heap (which is then different from a previously stored snapshot.
- etran.Heap.store(tokenId, "joinable", 0) ::
+ bassume(etran.Heap.select(tokenId, "joinable") ==@ 0) ::
bassume(new Boogie.MapSelect(etran.Mask, tokenId, "joinable", "perm$N")==@ 0) ::
bassume(new Boogie.MapSelect(etran.Mask, tokenId, "joinable", "perm$R")==@ 0) ::
- etran.IncPermission(tokenId, "joinable", 100) ::
+ etran.IncPermission(tokenId, "joinable", permissionFull) :::
// create a fresh value for the joinable field
BLocal(asyncStateV) :: Boogie.Havoc(asyncState) :: bassume(asyncState !=@ 0) ::
etran.Heap.store(tokenId, "joinable", asyncState) ::
+ // also store the k used for this fork, such that the same k can be used in the join
+ etran.Heap.store(tokenId, forkK, asyncMethodCallK) ::
// assume the pre call state for the token is the state before inhaling the precondition
bassume(CallHeap(asyncState) ==@ preCallHeap) ::
bassume(CallMask(asyncState) ==@ preCallMask) ::
bassume(CallCredits(asyncState) ==@ preCallCredits) ::
- bassume(CallArgs(asyncState) ==@ argsSeq) ::
+ bassume(CallArgs(asyncState) ==@ argsSeq) :::
// assign the returned token to the variable
{ if (token != null) List(token := tokenId) else List() }
case jn@JoinAsync(lhs, token) =>
@@ -713,7 +708,14 @@ class Translator { val (preCallCreditsV, preCallCredits) = NewBVar("preCallCredits", tcredits, true);
val preGlobals = List(preCallHeap, preCallMask, preCallCredits);
val postEtran = new ExpressionTranslator(List(etran.Heap, etran.Mask, etran.Credits), preGlobals, currentClass);
+ val (asyncJoinKV, asyncJoinK) = Boogie.NewBVar("asyncJoinK", tint, true)
+
Comment("join async") ::
+ // pick new k for this join
+ BLocal(asyncJoinKV) ::
+ bassume(0 < asyncJoinK) ::
+ // try to use the same k as for the fork
+ bassume(asyncJoinK ==@ etran.Heap.select(token, forkK)) ::
// check that token is well-defined
isDefined(token) :::
// check that we did not join yet
@@ -739,7 +741,7 @@ class Translator { etran.SetNoPermission(token, "joinable", etran.Mask) ::
// inhale postcondition of the call
postEtran.Inhale(Postconditions(jn.m.spec) map
- { p => SubstVars(p, formalThis, jn.m.ins ++ jn.m.outs, formalIns ++ formalOuts)}, "postcondition", false) :::
+ { p => SubstVars(p, formalThis, jn.m.ins ++ jn.m.outs, formalIns ++ formalOuts)}, "postcondition", false, asyncJoinK) :::
// assign formal outs to actual outs
(for ((v,e) <- lhs zip formalOuts) yield (v := e))
case s@Send(ch, args) =>
@@ -764,7 +766,7 @@ class Translator { Exhale(List(
(SubstVars(channel.where, formalThis, channel.parameters, formalParams),
ErrorMessage(s.pos, "The where clause at " + channel.where.pos + " might not hold."))),
- "channel where clause")
+ "channel where clause", methodK, false)
case r@Receive(_, ch, outs) =>
val channel = ch.typ.asInstanceOf[ChannelClass].ch
val formalThisV = new Variable("this", new Type(ch.typ))
@@ -786,7 +788,7 @@ class Translator { (formalThis := ch) ::
(for (v <- formalParams) yield Havoc(v)) :::
// inhale where clause
- Inhale(List(SubstVars(channel.where, formalThis, channel.parameters, formalParams)), "channel where clause") :::
+ Inhale(List(SubstVars(channel.where, formalThis, channel.parameters, formalParams)), "channel where clause", methodK) :::
// declare any new local variables among the actual outs
(for (v <- r.locals) yield BLocal(Variable2BVarWhere(v))) :::
// assign formal outs to actual outs
@@ -795,8 +797,8 @@ class Translator { new Boogie.MapUpdate(etran.Credits, TrExpr(ch), new Boogie.MapSelect(etran.Credits, TrExpr(ch)) - 1)
case r: RefinementBlock =>
translateRefinement(r)
- case _: Signal => throw new Exception("not implemented")
- case _: Wait => throw new Exception("not implemented")
+ case _: Signal => throw new NotSupportedException("not implemented")
+ case _: Wait => throw new NotSupportedException("not implemented")
}
}
@@ -832,13 +834,13 @@ class Translator { bassume(etran.Heap.select(nwe, "rdheld") ==@ false) ::
// give access to user-defined fields and special fields:
(for (f <- cl.Fields ++ RootClass.MentionableFields) yield
- etran.IncPermission(nwe, f.FullName, 100)) :::
+ etran.IncPermission(nwe, f.FullName, permissionFull)).flatten :::
// initialize fields according to the initialization
(initialization flatMap { init => isDefined(init.e) ::: etran.Heap.store(nwe, init.f.FullName, init.e) })
)
}
- def TrAcquire(s: Statement, nonNullObj: Expression) = {
+ def TrAcquire(s: Statement, nonNullObj: Expression, currentK: Expr) = {
val o = TrExpr(nonNullObj);
val (lastAcquireVar, lastAcquire) = Boogie.NewBVar("lastAcquire", IntClass, true)
val (lastSeenHeldV, lastSeenHeld) = Boogie.NewBVar("lastSeenHeld", tint, true)
@@ -860,13 +862,13 @@ class Translator { InhaleInvariants(nonNullObj, false, etran.WhereOldIs(
LastSeenHeap(lastSeenMu, lastSeenHeld),
LastSeenMask(lastSeenMu, lastSeenHeld),
- LastSeenCredits(lastSeenMu, lastSeenHeld))) :::
+ LastSeenCredits(lastSeenMu, lastSeenHeld)), currentK) :::
// remember values of Heap/Mask/Credits globals (for proving history constraint at release)
bassume(AcquireHeap(lastAcquire) ==@ etran.Heap) ::
bassume(AcquireMask(lastAcquire) ==@ etran.Mask) ::
bassume(AcquireCredits(lastAcquire) ==@ etran.Credits)
}
- def TrRelease(s: Statement, nonNullObj: Expression) = {
+ def TrRelease(s: Statement, nonNullObj: Expression, currentK: Expr) = {
val (heldV, held) = Boogie.NewBVar("held", tint, true)
val (prevLmV, prevLm) = Boogie.NewBVar("prevLM", tref, true)
val (preReleaseHeapV, preReleaseHeap) = NewBVar("preReleaseHeap", theap, true)
@@ -881,7 +883,7 @@ class Translator { ExhaleInvariants(nonNullObj, false, ErrorMessage(s.pos, "Monitor invariant might hot hold."), etran.WhereOldIs(
AcquireHeap(etran.Heap.select(o, "held")),
AcquireMask(etran.Heap.select(o, "held")),
- AcquireCredits(etran.Heap.select(o, "held")))) :::
+ AcquireCredits(etran.Heap.select(o, "held"))), currentK) :::
// havoc o.held where 0<=o.held
BLocal(heldV) :: Havoc(held) :: bassume(held <= 0) ::
etran.Heap.store(o, "held", held) ::
@@ -890,7 +892,7 @@ class Translator { bassume(LastSeenMask(etran.Heap.select(o, "mu"), held) ==@ preReleaseMask) ::
bassume(LastSeenCredits(etran.Heap.select(o, "mu"), held) ==@ preReleaseCredits)
}
- def TrRdAcquire(s: Statement, nonNullObj: Expression) = {
+ def TrRdAcquire(s: Statement, nonNullObj: Expression, currentK: Expr) = {
val (heldV, held) = Boogie.NewBVar("held", tint, true)
val o = TrExpr(nonNullObj)
bassert(CanRead(o, "mu"), s.pos, "The mu field of the target of the read-acquire statement might not be readable.") ::
@@ -900,18 +902,19 @@ class Translator { BLocal(heldV) :: Havoc(held) :: bassume(held <= 0) ::
etran.Heap.store(o, "held", held) ::
etran.Heap.store(o, "rdheld", true) ::
- InhaleInvariants(nonNullObj, true)
+ InhaleInvariants(nonNullObj, true, currentK)
}
- def TrRdRelease(s: Statement, nonNullObj: Expression) = {
+ def TrRdRelease(s: Statement, nonNullObj: Expression, currentK: Expr) = {
val (heldV, held) = Boogie.NewBVar("held", tint, true)
val o = TrExpr(nonNullObj);
bassert(isRdHeld(o), s.pos, "The current thread might not hold the read-lock of the object being released.") ::
- ExhaleInvariants(nonNullObj, true, ErrorMessage(s.pos, "Monitor invariant might not hold.")) :::
+ ExhaleInvariants(nonNullObj, true, ErrorMessage(s.pos, "Monitor invariant might not hold."), currentK) :::
BLocal(heldV) :: Havoc(held) :: bassume(held <= 0) ::
etran.Heap.store(o, "held", held) ::
etran.Heap.store(o, "rdheld", false)
}
+ // TODO: This method has not yet been updated to the new permission model
def translateSpecStmt(s: SpecStmt): List[Stmt] = {
val preGlobals = etran.FreshGlobals("pre")
@@ -922,14 +925,14 @@ class Translator { // remember values of globals
(for ((o,g) <- preGlobals zip etran.Globals) yield (new Boogie.VarExpr(o) := g)) :::
// exhale preconditions
- etran.Exhale(List((s.pre, ErrorMessage(s.pos, "The specification statement precondition at " + s.pos + " might not hold."))), "spec stmt precondition", true) :::
+ etran.Exhale(List((s.pre, ErrorMessage(s.pos, "The specification statement precondition at " + s.pos + " might not hold."))), "spec stmt precondition", true, todoiparam, todobparam) :::
// havoc locals
(s.lhs.map(l => Boogie.Havoc(l))) :::
// inhale postconditions (using the state before the call as the "old" state)
- etran.FromPreGlobals(preGlobals).Inhale(List(s.post), "spec stmt postcondition", true)
+ etran.FromPreGlobals(preGlobals).Inhale(List(s.post), "spec stmt postcondition", true, todoiparam)
}
- def translateCall(c: Call): List[Stmt] = {
+ def translateCall(c: Call, methodK: Expr): List[Stmt] = {
val obj = c.obj;
val lhs = c.lhs;
val id = c.id;
@@ -942,6 +945,11 @@ class Translator { val formalOuts = for (v <- formalOutsV) yield new VariableExpr(v)
val preGlobals = etran.FreshGlobals("call")
val postEtran = etran.FromPreGlobals(preGlobals)
+
+ // pick new k for this method call
+ val (methodCallKV, methodCallK) = Boogie.NewBVar("methodCallK", tint, true)
+ BLocal(methodCallKV) ::
+ bassume(0 < methodCallK) :: // upper bounds are later provided by the exhale
Comment("call " + id) ::
// introduce formal parameters and pre-state globals
(for (v <- formalThisV :: formalInsV ::: formalOutsV) yield BLocal(Variable2BVarWhere(v))) :::
@@ -957,21 +965,21 @@ class Translator { (for ((v,e) <- formalIns zip args) yield (v := e)) :::
// exhale preconditions
Exhale(Preconditions(c.m.Spec) map
- (p => SubstVars(p, formalThis, c.m.Ins, formalIns)) zip (Preconditions(c.m.Spec) map { p => ErrorMessage(c.pos, "The precondition at " + p.pos + " might not hold.")}), "precondition") :::
+ (p => SubstVars(p, formalThis, c.m.Ins, formalIns)) zip (Preconditions(c.m.Spec) map { p => ErrorMessage(c.pos, "The precondition at " + p.pos + " might not hold.")}), "precondition", methodCallK, false) :::
// havoc formal outs
(for (v <- formalOuts) yield Havoc(v)) :::
// havoc lockchanges
LockHavoc(for (e <- LockChanges(c.m.Spec) map (p => SubstVars(p, formalThis, c.m.Ins, formalIns))) yield etran.Tr(e), postEtran) :::
// inhale postconditions (using the state before the call as the "old" state)
postEtran.Inhale(Postconditions(c.m.Spec) map
- (p => SubstVars(p, formalThis, c.m.Ins ++ c.m.Outs, formalIns ++ formalOuts)) , "postcondition", false) :::
+ (p => SubstVars(p, formalThis, c.m.Ins ++ c.m.Outs, formalIns ++ formalOuts)) , "postcondition", false, methodCallK) :::
// declare any new local variables among the actual outs
(for (v <- c.locals) yield BLocal(Variable2BVarWhere(v))) :::
// assign formal outs to actual outs
(for ((v,e) <- lhs zip formalOuts) yield (v :=e))
}
- def translateWhile(w: WhileStmt): List[Stmt] = {
+ def translateWhile(w: WhileStmt, methodK: Expr): List[Stmt] = {
val guard = w.guard;
val lkch = w.lkch;
val body = w.body;
@@ -989,15 +997,20 @@ class Translator { val oldLocks = lkchOld map (e => loopEtran.oldEtran.Tr(e))
val iterStartLocks = lkchIterStart map (e => iterStartEtran.oldEtran.Tr(e))
val newLocks = lkch map (e => loopEtran.Tr(e));
+ val (whileKV, whileK) = Boogie.NewBVar("whileK", tint, true)
+
Comment("while") ::
+ // pick new k for this method call
+ BLocal(whileKV) ::
+ bassume(0 < whileK) :: // upper bounds are later provided by the exhale
// save globals
(for (v <- preLoopGlobals) yield BLocal(v)) :::
(loopEtran.oldEtran.Heap := loopEtran.Heap) ::
(loopEtran.oldEtran.Mask := loopEtran.Mask) :: // oldMask is not actually used below
(loopEtran.oldEtran.Credits := loopEtran.Credits) :: // is oldCredits?
// check invariant on entry to the loop
- Exhale(w.oldInvs map { inv => (inv, ErrorMessage(inv.pos, "The loop invariant might not hold on entry to the loop."))}, "loop invariant, initially") :::
- tag(Exhale(w.newInvs map { inv => (inv, ErrorMessage(inv.pos, "The loop invariant might not hold on entry to the loop."))}, "loop invariant, initially"), keepTag) :::
+ Exhale(w.oldInvs map { inv => (inv, ErrorMessage(inv.pos, "The loop invariant might not hold on entry to the loop."))}, "loop invariant, initially", whileK, false) :::
+ tag(Exhale(w.newInvs map { inv => (inv, ErrorMessage(inv.pos, "The loop invariant might not hold on entry to the loop."))}, "loop invariant, initially", whileK, false), keepTag) :::
List(bassert(DebtCheck, w.pos, "Loop invariant must consume all debt on entry to the loop.")) :::
// check lockchange on entry to the loop
Comment("check lockchange on entry to the loop") ::
@@ -1014,15 +1027,15 @@ class Translator { Comment("check loop invariant definedness") ::
//(w.LoopTargets.toList map { v: Variable => Boogie.Havoc(Boogie.VarExpr(v.id)) }) :::
Boogie.Havoc(etran.Heap) :: Boogie.Assign(etran.Mask, ZeroMask) :: Boogie.Assign(etran.Credits, ZeroCredits) ::
- InhaleWithChecking(w.oldInvs, "loop invariant definedness") :::
- tag(InhaleWithChecking(w.newInvs, "loop invariant definedness"), keepTag) :::
+ InhaleWithChecking(w.oldInvs, "loop invariant definedness", whileK) :::
+ tag(InhaleWithChecking(w.newInvs, "loop invariant definedness", whileK), keepTag) :::
bassume(false)
, Boogie.If(null,
// 2. CHECK LOOP BODY
// Renew state: set Mask to ZeroMask and Credits to ZeroCredits, and havoc Heap everywhere except
// at {old(local),local}.{held,rdheld}
Havoc(etran.Heap) :: (etran.Mask := ZeroMask) :: (etran.Credits := ZeroCredits) ::
- Inhale(w.Invs, "loop invariant, body") :::
+ Inhale(w.Invs, "loop invariant, body", whileK) :::
// assume lockchange at the beginning of the loop iteration
Comment("assume lockchange at the beginning of the loop iteration") ::
(bassume(LockFrame(lkch, etran))) ::
@@ -1036,10 +1049,10 @@ class Translator { (new VariableExpr(isv) := new VariableExpr(v))) :::
// evaluate the guard
isDefined(guard) ::: List(bassume(guard)) :::
- translateStatement(body) :::
+ translateStatement(body, whileK) :::
// check invariant
- Exhale(w.oldInvs map { inv => (inv, ErrorMessage(inv.pos, "The loop invariant at " + inv.pos + " might not be preserved by the loop."))}, "loop invariant, maintained") :::
- tag(Exhale(w.newInvs map { inv => (inv, ErrorMessage(inv.pos, "The loop invariant at " + inv.pos + " might not be preserved by the loop."))}, "loop invariant, maintained"), keepTag) :::
+ Exhale(w.oldInvs map { inv => (inv, ErrorMessage(inv.pos, "The loop invariant at " + inv.pos + " might not be preserved by the loop."))}, "loop invariant, maintained", whileK, true) :::
+ tag(Exhale(w.newInvs map { inv => (inv, ErrorMessage(inv.pos, "The loop invariant at " + inv.pos + " might not be preserved by the loop."))}, "loop invariant, maintained", whileK, true), keepTag) :::
isLeaking(w.pos, "The loop might leak refereces.") :::
// check lockchange after loop iteration
Comment("check lockchange after loop iteration") ::
@@ -1052,10 +1065,11 @@ class Translator { // assume lockchange after the loop
Comment("assume lockchange after the loop") ::
(bassume(LockFrame(lkch, etran))) ::
- Inhale(w.Invs, "loop invariant, after loop") :::
+ Inhale(w.Invs, "loop invariant, after loop", whileK) :::
bassume(!guard)))
}
+ // TODO: This method has not yet been updated to the new permission model
def translateRefinement(r: RefinementBlock): List[Stmt] = {
// abstract expression translator
val absTran = etran;
@@ -1082,7 +1096,7 @@ class Translator { {
etran = conTran;
Comment("run concrete program:") ::
- tag(translateStatements(r.con), keepTag)
+ tag(translateStatements(r.con, todoiparam), keepTag)
} :::
// run angelically A on the old heap
Comment("run abstract program:") ::
@@ -1097,7 +1111,7 @@ class Translator { (for ((v, w) <- duringA zip duringC) yield (new VariableExpr(v) := new VariableExpr(w))) :::
BLocal(m) ::
(me := absTran.Mask) ::
- absTran.Exhale(s.post, me, absTran.Heap, ErrorMessage(r.pos, "Refinement may fail to satisfy specification statement post-condition."), false) :::
+ absTran.Exhale(s.post, me, absTran.Heap, ErrorMessage(r.pos, "Refinement may fail to satisfy specification statement post-condition."), false, todoiparam, todobparam) :::
(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)
@@ -1107,7 +1121,7 @@ class Translator { (for ((v, w) <- afterV zip before) yield (new VariableExpr(v) := new VariableExpr(w))) :::
// restore locals before
(for ((v, w) <- before zip beforeV) yield (new VariableExpr(v) := new VariableExpr(w))) :::
- translateStatements(r.abs) :::
+ translateStatements(r.abs, todoiparam) :::
// assert equality on shared locals
tag(
(for ((v, w) <- afterV zip before) yield
@@ -1125,7 +1139,7 @@ class Translator { case And(a,b) => copy(a) ::: copy(b)
case Implies(a,b) => Boogie.If(absTran.Tr(a), copy(b), Nil)
case Access(ma, _) if ! ma.isPredicate => absTran.Heap.store(absTran.Tr(ma.e), new VarExpr(ma.f.FullName), conTran.Heap.select(absTran.Tr(ma.e), ma.f.FullName))
- case _: PermissionExpr => throw new Exception("not implemented")
+ case _: PermissionExpr => throw new NotSupportedException("not implemented")
case _ => Nil
}
@@ -1142,7 +1156,6 @@ class Translator { Comment("end of refinement block")
}
-
def UpdateMu(o: Expr, allowOnlyFromBottom: Boolean, justAssumeValue: Boolean,
lowerBounds: List[Expression], upperBounds: List[Expression], error: ErrorMessage): List[Stmt] = {
def BoundIsNullObject(b: Expression): Boogie.Expr = {
@@ -1254,8 +1267,7 @@ class Translator { Havoc(held) :: Havoc(rdheld) ::
bassume(rdheld ==> (0 < held)) ::
new MapUpdate(etran.Heap, o, VarExpr("held"), held) ::
- new MapUpdate(etran.Heap, o, VarExpr("rdheld"), rdheld) })
- .flatten
+ new MapUpdate(etran.Heap, o, VarExpr("rdheld"), rdheld) }).flatten
}
def NumberOfLocksHeldIsInvariant(oldLocks: List[Boogie.Expr], newLocks: List[Boogie.Expr],
etran: ExpressionTranslator) = {
@@ -1276,51 +1288,50 @@ class Translator { ((! new Boogie.MapSelect(etran.oldEtran.Heap, o, "rdheld")) ||
(! new Boogie.MapSelect(etran.Heap, o, "rdheld"))))) ::
Nil
- })
- .flatten
+ }).flatten
}
implicit def lift(s: Stmt): List[Stmt] = List(s)
def isDefined(e: Expression) = etran.isDefined(e)(true)
def TrExpr(e: Expression) = etran.Tr(e)
- def InhaleInvariants(obj: Expression, readonly: Boolean, tran: ExpressionTranslator) = {
+ def InhaleInvariants(obj: Expression, readonly: Boolean, tran: ExpressionTranslator, currentK: Expr) = {
val shV = new Variable("sh", new Type(obj.typ))
val sh = new VariableExpr(shV)
BLocal(Variable2BVar(shV)) :: Boogie.Assign(TrExpr(sh), TrExpr(obj)) ::
tran.Inhale(obj.typ.MonitorInvariants map
(inv => SubstThis(inv.e, sh)) map
- (inv => (if (readonly) SubstRd(inv) else inv)), "monitor invariant", false)
+ (inv => (if (readonly) SubstRd(inv) else inv)), "monitor invariant", false, currentK)
}
- def ExhaleInvariants(obj: Expression, readonly: Boolean, msg: ErrorMessage, tran: ExpressionTranslator) = {
+ def ExhaleInvariants(obj: Expression, readonly: Boolean, msg: ErrorMessage, tran: ExpressionTranslator, currentK: Expr) = {
val shV = new Variable("sh", new Type(obj.typ))
val sh = new VariableExpr(shV)
BLocal(Variable2BVar(shV)) :: Boogie.Assign(TrExpr(sh), TrExpr(obj)) ::
tran.Exhale(obj.typ.MonitorInvariants map
(inv => SubstThis(inv.e, sh)) map
- (inv => (if (readonly) SubstRd(inv) else inv, msg)), "monitor invariant", false)
+ (inv => (if (readonly) SubstRd(inv) else inv, msg)), "monitor invariant", false, currentK, false)
}
- def InhaleInvariants(obj: Expression, readonly: Boolean) = {
+ def InhaleInvariants(obj: Expression, readonly: Boolean, currentK: Expr) = {
val shV = new Variable("sh", new Type(obj.typ))
val sh = new VariableExpr(shV)
BLocal(Variable2BVar(shV)) :: Boogie.Assign(TrExpr(sh), TrExpr(obj)) ::
Inhale(obj.typ.MonitorInvariants map
(inv => SubstThis(inv.e, sh)) map
- (inv => (if (readonly) SubstRd(inv) else inv)), "monitor invariant")
+ (inv => (if (readonly) SubstRd(inv) else inv)), "monitor invariant", currentK)
}
- def ExhaleInvariants(obj: Expression, readonly: Boolean, msg: ErrorMessage) = {
+ def ExhaleInvariants(obj: Expression, readonly: Boolean, msg: ErrorMessage, currentK: Expr) = {
val shV = new Variable("sh", new Type(obj.typ))
val sh = new VariableExpr(shV)
BLocal(Variable2BVar(shV)) :: Boogie.Assign(TrExpr(sh), TrExpr(obj)) ::
Exhale(obj.typ.MonitorInvariants map
(inv => SubstThis(inv.e, sh)) map
- (inv => (if (readonly) SubstRd(inv) else inv, msg)), "monitor invariant")
+ (inv => (if (readonly) SubstRd(inv) else inv, msg)), "monitor invariant", currentK, false)
}
- def Inhale(predicates: List[Expression], occasion: String): List[Boogie.Stmt] = etran.Inhale(predicates, occasion, false)
- def Exhale(predicates: List[(Expression, ErrorMessage)], occasion: String): List[Boogie.Stmt] = etran.Exhale(predicates, occasion, false)
- def InhaleWithChecking(predicates: List[Expression], occasion: String): List[Boogie.Stmt] = etran.Inhale(predicates, occasion, true)
- def ExhaleWithChecking(predicates: List[(Expression, ErrorMessage)], occasion: String): List[Boogie.Stmt] = etran.Exhale(predicates, occasion, true)
+ def Inhale(predicates: List[Expression], occasion: String, currentK: Expr): List[Boogie.Stmt] = etran.Inhale(predicates, occasion, false, currentK)
+ def Exhale(predicates: List[(Expression, ErrorMessage)], occasion: String, currentK: Expr, exactchecking: Boolean): List[Boogie.Stmt] = etran.Exhale(predicates, occasion, false, currentK, exactchecking)
+ def InhaleWithChecking(predicates: List[Expression], occasion: String, currentK: Expr): List[Boogie.Stmt] = etran.Inhale(predicates, occasion, true, currentK)
+ def ExhaleWithChecking(predicates: List[(Expression, ErrorMessage)], occasion: String, currentK: Expr, exactchecking: Boolean): List[Boogie.Stmt] = etran.Exhale(predicates, occasion, true, currentK, exactchecking)
def CanRead(obj: Boogie.Expr, field: Boogie.Expr): Boogie.Expr = etran.CanRead(obj, field)
def CanWrite(obj: Boogie.Expr, field: Boogie.Expr): Boogie.Expr = etran.CanWrite(obj, field)
@@ -1406,12 +1417,21 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E isDefined(e) :::
prove(nonNull(Tr(e)), e.pos, "Receiver might be null.") ::
prove(CanRead(Tr(e), fs.f.FullName), fs.pos, "Location might not be readable.")
- case Full | Epsilon | Star => Nil
- case Frac(perm) => isDefined(perm) ::: bassert(Boogie.IntLiteral(0)<=Tr(perm), perm.pos, "Fraction might be negative.") :: Nil
- case Epsilons(p) => isDefined(p) ::: bassert(Boogie.IntLiteral(0)<=Tr(p), p.pos, "Number of epsilons might be negative.")
- case _:PermissionExpr => throw new Exception("permission expression unexpected here: " + e.pos)
+ case Full | Star | Epsilon | MethodEpsilon => Nil
+ case ForkEpsilon(token) => isDefined(token)
+ case MonitorEpsilon(Some(monitor)) => isDefined(monitor)
+ case ChannelEpsilon(Some(channel)) => isDefined(channel)
+ case PredicateEpsilon(_) => Nil
+ case ChannelEpsilon(None) | MonitorEpsilon(None) => Nil
+ case PermPlus(l,r) => isDefined(l) ::: isDefined(r)
+ case PermMinus(l,r) => isDefined(l) ::: isDefined(r)
+ case PermTimes(l,r) => isDefined(l) ::: isDefined(r)
+ case IntPermTimes(l,r) => isDefined(l) ::: isDefined(r)
+ case Frac(perm) => isDefined(perm)
+ case Epsilons(p) => isDefined(p)
+ case _:PermissionExpr => throw new InternalErrorException("permission expression unexpected here: " + e.pos + " (" + e + ")")
case c@Credit(e, n) =>
- isDefined(e);
+ isDefined(e) :::
isDefined(c.N)
case Holds(e) =>
isDefined(e)
@@ -1430,50 +1450,51 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E val (tmpMaskV, tmpMask) = Boogie.NewBVar("Mask", tmask, true);
val (tmpCreditsV, tmpCredits) = Boogie.NewBVar("Credits", tcredits, true);
val tmpTranslator = new ExpressionTranslator(List(tmpHeap,tmpMask,tmpCredits), currentClass);
+
+ // pick new k
+ val (funcappKV, funcappK) = Boogie.NewBVar("funcappK", tint, true)
+
// check definedness of receiver + arguments
(obj :: args flatMap { arg => isDefined(arg) }) :::
// check that receiver is not null
List(prove(nonNull(Tr(obj)), obj.pos, "Receiver might be null.")) :::
// check precondition of the function by exhaling the precondition in tmpHeap/tmpMask/tmpCredits
Comment("check precondition of call") ::
+ BLocal(funcappKV) :: bassume(0 < funcappK && 1000*funcappK < permissionFull) ::
bassume(assumption) ::
BLocal(tmpHeapV) :: (tmpHeap := Heap) ::
BLocal(tmpMaskV) :: (tmpMask := Mask) :::
BLocal(tmpCreditsV) :: (tmpCredits := Credits) :::
tmpTranslator.Exhale(Preconditions(func.f.spec) map { pre=> (SubstVars(pre, obj, func.f.ins, args), ErrorMessage(func.pos, "Precondition at " + pre.pos + " might not hold."))},
"function call",
- false) :::
+ false, funcappK, false) :::
// size of the heap of callee must be strictly smaller than size of the heap of the caller
(if(checkTermination) { List(prove(NonEmptyMask(tmpMask), func.pos, "The heap of the callee might not be strictly smaller than the heap of the caller.")) } else Nil)
- case unfolding@Unfolding(access, e) =>
- val (checks, predicate, definition, from) = access match {
- case acc@Access(pred@MemberAccess(obj, f), perm) =>
- val receiverOk = isDefined(obj) ::: prove(nonNull(Tr(obj)), obj.pos, "Receiver might be null.");
- val body = SubstThis(DefinitionOf(pred.predicate), obj);
- perm match {
- case Full => (receiverOk, acc, body, Heap.select(Tr(obj), pred.predicate.FullName))
- case Frac(fraction) => (receiverOk ::: isDefined(fraction) ::: prove(0 <= Tr(fraction), fraction.pos, "Fraction might be negative") :: prove(Tr(fraction) <= 100, fraction.pos, "Fraction might exceed 100."), acc, FractionOf(body, fraction), Heap.select(Tr(obj), pred.predicate.FullName))
- case Epsilon => (receiverOk, acc, EpsilonsOf(body, IntLiteral(1)), Heap.select(Tr(obj), pred.predicate.FullName))
- case Star => assert(false); (null, null, null, Heap.select(Tr(obj), pred.predicate.FullName))
- case Epsilons(epsilons) => (receiverOk ::: isDefined(epsilons) ::: prove(0 <= Tr(epsilons), epsilons.pos, "Number of epsilons might be negative"), acc, EpsilonsOf(body, epsilons), Heap.select(Tr(obj), pred.predicate.FullName))
- }
- }
+ case unfolding@Unfolding(acc@Access(pred@MemberAccess(obj, f), perm), e) =>
val newGlobals = FreshGlobals("checkPre");
val (tmpHeapV, tmpHeap) = Boogie.NewBVar("Heap", theap, true);
val (tmpMaskV, tmpMask) = Boogie.NewBVar("Mask", tmask, true);
val (tmpCreditsV, tmpCredits) = Boogie.NewBVar("Credits", tcredits, true);
val tmpTranslator = new ExpressionTranslator(List(tmpHeap, tmpMask, tmpCredits), currentClass);
+
+ val receiverOk = isDefined(obj) ::: prove(nonNull(Tr(obj)), obj.pos, "Receiver might be null.");
+ val definition = scaleExpressionByPermission(SubstThis(DefinitionOf(pred.predicate), obj), perm, unfolding.pos)
+
+ // pick new k
+ val (unfoldingKV, unfoldingK) = Boogie.NewBVar("unfoldingK", tint, true)
+
Comment("unfolding") ::
+ BLocal(unfoldingKV) :: bassume(0 < unfoldingK && 1000*unfoldingK < permissionFull) ::
// check definedness
- checks :::
+ receiverOk ::: isDefined(perm) :::
// copy state into temporary variables
BLocal(tmpHeapV) :: Boogie.Assign(tmpHeap, Heap) ::
BLocal(tmpMaskV) :: Boogie.Assign(tmpMask, Mask) ::
BLocal(tmpCreditsV) :: Boogie.Assign(tmpCredits, Credits) ::
// exhale the predicate
- tmpTranslator.Exhale(List((predicate, ErrorMessage(unfolding.pos, "Unfolding might fail."))), "unfolding", false) :::
+ tmpTranslator.Exhale(List((acc, ErrorMessage(unfolding.pos, "Unfolding might fail."))), "unfolding", false, unfoldingK, false) :::
// inhale the definition of the predicate
- tmpTranslator.InhaleFrom(List(definition), "unfolding", false, from) :::
+ tmpTranslator.InhaleFrom(List(definition), "unfolding", false, Heap.select(Tr(obj), pred.predicate.FullName), unfoldingK) :::
// check definedness of e in state where the predicate is unfolded
tmpTranslator.isDefined(e)
case Iff(e0,e1) =>
@@ -1506,7 +1527,8 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E case ExplicitSeq(es) =>
es flatMap { e => isDefined(e) }
case Range(min, max) =>
- isDefined(min) ::: isDefined(max)
+ isDefined(min) ::: isDefined(max) :::
+ prove(Tr(min) <= Tr(max), e.pos, "Range minimum might not be smaller or equal to range maximum.")
case Append(e0, e1) =>
isDefined(e0) ::: isDefined(e1)
case at@At(e0, e1) =>
@@ -1529,8 +1551,14 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E val (evalHeap, evalMask, evalCredits, checks, assumptions) = fromEvalState(h);
val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask, evalCredits), currentClass);
evalEtran.isDefined(e)
- case _ : SeqQuantification => throw new Exception("should be desugared")
- case tq @ TypeQuantification(_, _, _, e) =>
+ case _ : SeqQuantification => throw new InternalErrorException("should be desugared")
+ case tq @ TypeQuantification(_, _, _, e, (min, max)) =>
+ // replace variables since we need locals
+ val vars = tq.variables map {v => val result = new Variable(v.id, v.t); result.pos = v.pos; result;}
+ prove(Tr(min) <= Tr(max), e.pos, "Range minimum might not be smaller or equal to range maximum.") :::
+ (vars map {v => BLocal(Variable2BVarWhere(v))}) :::
+ isDefined(SubstVars(e, tq.variables, vars map {v => new VariableExpr(v);}))
+ case tq @ TypeQuantification(_, _, _, e, _) =>
// replace variables since we need locals
val vars = tq.variables map {v => val result = new Variable(v.id, v.t); result.pos = v.pos; result;}
(vars map {v => BLocal(Variable2BVarWhere(v))}) :::
@@ -1542,7 +1570,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E case IntLiteral(n) => n
case BoolLiteral(b) => b
case NullLiteral() => bnull
- case MaxLockLiteral() => throw new Exception("waitlevel case should be handled in << and == and !=")
+ case MaxLockLiteral() => throw new InternalErrorException("waitlevel case should be handled in << and == and !=")
case LockBottomLiteral() => bLockBottom
case _:ThisExpr => VarExpr("this")
case _:Result => VarExpr("result")
@@ -1554,9 +1582,9 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E r !=@ 0 // joinable is encoded as an integer
else
r
- case _:Permission => throw new Exception("permission unexpected here")
- case _:PermissionExpr => throw new Exception("permission expression unexpected here: " + e.pos)
- case _:Credit => throw new Exception("credit expression unexpected here")
+ case _:Permission => throw new InternalErrorException("permission unexpected here")
+ case _:PermissionExpr => throw new InternalErrorException("permission expression unexpected here: " + e.pos)
+ case _:Credit => throw new InternalErrorException("credit expression unexpected here")
case Holds(e) =>
(0 < Heap.select(Tr(e), "held")) &&
!Heap.select(Tr(e), "rdheld")
@@ -1643,16 +1671,16 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E Boogie.FunctionApp("Seq#Drop", List(Tr(e0), Tr(e1)))
case Take(e0, e1) =>
Boogie.FunctionApp("Seq#Take", List(Tr(e0), Tr(e1)))
- case Length(e) => SeqLength(e)
+ case Length(e) => SeqLength(Tr(e))
case Contains(e0, e1) => SeqContains(Tr(e1), Tr(e0))
case Eval(h, e) =>
val (evalHeap, evalMask, evalCredits, checks, assumptions) = fromEvalState(h);
val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask, evalCredits), currentClass);
evalEtran.Tr(e)
- case _:SeqQuantification => throw new Exception("should be desugared")
- case tq @ TypeQuantification(Forall, _, _, e) =>
+ case _:SeqQuantification => throw new InternalErrorException("should be desugared")
+ case tq @ TypeQuantification(Forall, _, _, e, _) =>
Boogie.Forall(Nil, tq.variables map { v => Variable2BVar(v)}, Nil, Tr(e))
- case tq @ TypeQuantification(Exists, _, _, e) =>
+ case tq @ TypeQuantification(Exists, _, _, e, _) =>
Boogie.Exists(Nil, tq.variables map { v => Variable2BVar(v)}, Nil, Tr(e))
}
@@ -1671,75 +1699,98 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E ***************** INHALE/EXHALE *****************
**********************************************************************/
- def Inhale(predicates: List[Expression], occasion: String, check: Boolean): List[Boogie.Stmt] = {
+ def Inhale(predicates: List[Expression], occasion: String, check: Boolean, currentK: Expr): List[Boogie.Stmt] = {
if (predicates.size == 0) return Nil;
val (ihV, ih) = Boogie.NewBVar("inhaleHeap", theap, true)
Comment("inhale (" + occasion + ")") ::
BLocal(ihV) :: Boogie.Havoc(ih) ::
bassume(IsGoodInhaleState(ih, Heap, Mask)) ::
- (for (p <- predicates) yield Inhale(p, ih, check)).flatten :::
+ (for (p <- predicates) yield Inhale(p, ih, check, currentK)).flatten :::
bassume(IsGoodMask(Mask)) ::
bassume(wf(Heap, Mask)) ::
Comment("end inhale")
}
- def InhaleFrom(predicates: List[Expression], occasion: String, check: Boolean, useHeap: Boogie.Expr): List[Boogie.Stmt] = {
+ def InhaleFrom(predicates: List[Expression], occasion: String, check: Boolean, useHeap: Boogie.Expr, currentK: Expr): List[Boogie.Stmt] = {
if (predicates.size == 0) return Nil;
val (ihV, ih) = Boogie.NewBVar("inhaleHeap", theap, true)
Comment("inhale (" + occasion + ")") ::
BLocal(ihV) :: Boogie.Assign(ih, useHeap) ::
bassume(IsGoodInhaleState(ih, Heap, Mask)) ::
- (for (p <- predicates) yield Inhale(p,ih, check)).flatten :::
+ (for (p <- predicates) yield Inhale(p,ih, check, currentK)).flatten :::
bassume(IsGoodMask(Mask)) ::
bassume(wf(Heap, Mask)) ::
Comment("end inhale")
}
+
+ def InhalePermission(perm: Permission, obj: Expr, memberName: String, currentK: Expr): List[Boogie.Stmt] = {
+
+ val (f, stmts) = extractKFromPermission(perm, currentK)
+ val n = extractEpsilonsFromPermission(perm);
+
+ stmts :::
+ (perm.permissionType match {
+ case PermissionType.Mixed =>
+ bassume(f > 0 || (f == 0 && n > 0)) ::
+ IncPermission(obj, memberName, f) :::
+ IncPermissionEpsilon(obj, memberName, n)
+ case PermissionType.Epsilons =>
+ bassume(n > 0) ::
+ IncPermissionEpsilon(obj, memberName, n)
+ case PermissionType.Fraction =>
+ bassume(f > 0) ::
+ IncPermission(obj, memberName, f)
+ })
+ }
- def Inhale(p: Expression, ih: Boogie.Expr, check: Boolean): List[Boogie.Stmt] = desugar(p) match {
- case pred@MemberAccess(e, p) if pred.isPredicate =>
+ def Inhale(p: Expression, ih: Boogie.Expr, check: Boolean, currentK: Expr): List[Boogie.Stmt] = desugar(p) match {
+ case pred@MemberAccess(e, p) if pred.isPredicate => + val chk = (if (check) { + isDefined(e)(true) ::: + bassert(nonNull(Tr(e)), e.pos, "Receiver might be null.") :: Nil + } else Nil)
val tmp = Access(pred, Full);
tmp.pos = pred.pos;
- Inhale(tmp, ih, check)
- case AccessAll(obj, perm) => throw new Exception("should be desugared")
- case AccessSeq(s, None, perm) => throw new Exception("should be desugared")
+ chk ::: Inhale(tmp, ih, check, currentK)
+ case AccessAll(obj, perm) => throw new InternalErrorException("should be desugared")
+ case AccessSeq(s, None, perm) => throw new InternalErrorException("should be desugared")
case acc@Access(e,perm) =>
val trE = Tr(e.e)
val module = currentClass.module;
val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;
// List(bassert(nonNull(trE), acc.pos, "The target of the acc predicate might be null."))
- (if(check) isDefined(e.e)(true) ::: isDefined(perm)(true) ::: (perm match {case Frac(p) if(! e.isPredicate) => bassert(Tr(p) <= 100, p.pos, "Fraction might exceed 100.") :: Nil; case _ => Nil})
+ (if(check) isDefined(e.e)(true) ::: isDefined(perm)(true)
else Nil) :::
bassume(nonNull(trE)) ::
new MapUpdate(Heap, trE, VarExpr(memberName), new Boogie.MapSelect(ih, trE, memberName)) ::
bassume(wf(Heap, Mask)) ::
(if(e.isPredicate && e.predicate.Parent.module.equals(currentClass.module)) List(bassume(new Boogie.MapSelect(ih, trE, memberName) ==@ Heap)) else Nil) :::
(if(e.isPredicate) Nil else List(bassume(TypeInformation(new Boogie.MapSelect(Heap, trE, memberName), e.f.typ.typ)))) :::
- (perm match {
- case Full => IncPermission(trE, memberName, 100)
- case Frac(perm) => IncPermission(trE, memberName, Tr(perm))
- case Epsilon => IncPermissionEpsilon(trE, memberName, 1)
- case Epsilons(p) => IncPermissionEpsilon(trE, memberName, Tr(p))
- case Star => IncPermissionEpsilon(trE, memberName, null)
- }) ::
+ InhalePermission(perm, trE, memberName, currentK) :::
bassume(IsGoodMask(Mask)) ::
bassume(IsGoodState(new Boogie.MapSelect(ih, trE, memberName))) ::
bassume(wf(Heap, Mask)) ::
bassume(wf(ih, Mask))
case acc @ AccessSeq(s, Some(member), perm) =>
- if (member.isPredicate) throw new Exception("not yet implemented");
+ if (member.isPredicate) throw new NotSupportedException("not yet implemented");
val e = Tr(s);
val memberName = member.f.FullName;
- val (r, n) = perm match {
- case Full => (100, 0) : (Expr, Expr)
- case Frac(p) => (Tr(p), 0) : (Expr, Expr)
- case Epsilon => (0, 1) : (Expr, Expr) // TODO: check for infinity bounds -- or perhaps just wait till epsilons are gone
- case Epsilons(p) => (0, Tr(p)) : (Expr, Expr)
- case Star => throw new Exception("not yet implemented")
- };
-
+ val (refV, ref) = Boogie.NewBVar("ref", tref, true);
+
+ val (r, stmts) = extractKFromPermission(perm, currentK)
+ val n = extractEpsilonsFromPermission(perm);
+
+ stmts :::
+ // assume that the permission is positive
+ bassume((SeqContains(e, ref) ==>
+ (perm.permissionType match {
+ case PermissionType.Fraction => r > 0
+ case PermissionType.Mixed => r > 0 || (r == 0 && n > 0)
+ case PermissionType.Epsilons => n > 0
+ })).forall(refV)) ::
(if (check) isDefined(s)(true) ::: isDefined(perm)(true) else Nil) :::
{
val (aV,a) = Boogie.NewTVar("alpha");
@@ -1751,9 +1802,9 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E bassume((SeqContains(e, ref) ==> TypeInformation(Heap(ref, memberName), member.f.typ.typ)).forall(refV))
} :::
bassume(wf(Heap, Mask)) ::
+ // update the map
{
val (aV,a) = Boogie.NewTVar("alpha");
- val (refV, ref) = Boogie.NewBVar("ref", tref, true);
val (fV, f) = Boogie.NewBVar("f", FieldType(a), true);
val (pcV,pc) = Boogie.NewBVar("p", tperm, true);
Mask := Lambda(List(aV), List(refV, fV),
@@ -1763,10 +1814,10 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E Mask(ref, f)("perm$R") + r,
Mask(ref, f)("perm$N") + n)),
Mask(ref, f)))
- } :::
- bassume(IsGoodMask(Mask)) ::
+ } :::
+ bassume(IsGoodMask(Mask)) ::
bassume(wf(Heap, Mask)) ::
- bassume(wf(ih, Mask))
+ bassume(wf(ih, Mask))
case cr@Credit(ch, n) =>
val trCh = Tr(ch)
(if (check)
@@ -1778,12 +1829,12 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E new Boogie.MapUpdate(Credits, trCh, new Boogie.MapSelect(Credits, trCh) + Tr(cr.N))
case Implies(e0,e1) =>
(if(check) isDefined(e0)(true) else Nil) :::
- Boogie.If(Tr(e0), Inhale(e1, ih, check), Nil)
+ Boogie.If(Tr(e0), Inhale(e1, ih, check, currentK), Nil)
case IfThenElse(con, then, els) =>
(if(check) isDefined(con)(true) else Nil) :::
- Boogie.If(Tr(con), Inhale(then, ih, check), Inhale(els, ih, check))
+ Boogie.If(Tr(con), Inhale(then, ih, check, currentK), Inhale(els, ih, check, currentK))
case And(e0,e1) =>
- Inhale(e0, ih, check) ::: Inhale(e1, ih, check)
+ Inhale(e0, ih, check, currentK) ::: Inhale(e1, ih, check, currentK)
case holds@Holds(e) =>
val trE = Tr(e);
(if(check)
@@ -1820,107 +1871,104 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E bassume(IsGoodMask(preEtran.Mask)) ::
bassume(wf(preEtran.Heap, preEtran.Mask)) ::
bassume(proofOrAssume) ::
- preEtran.Inhale(e, ih, check) :::
+ preEtran.Inhale(e, ih, check, currentK) :::
bassume(preEtran.Heap ==@ evalHeap) ::
bassume(submask(preEtran.Mask, evalMask))
case e => (if(check) isDefined(e)(true) else Nil) ::: bassume(Tr(e))
}
-
- def Exhale(predicates: List[(Expression, ErrorMessage)], occasion: String, check: Boolean): List[Boogie.Stmt] = {
+
+ def Exhale(predicates: List[(Expression, ErrorMessage)], occasion: String, check: Boolean, currentK: Expr, exactchecking: Boolean): List[Boogie.Stmt] = {
if (predicates.size == 0) return Nil;
val (emV, em) = NewBVar("exhaleMask", tmask, true)
Comment("begin exhale (" + occasion + ")") ::
BLocal(emV) :: (em := Mask) ::
- (for (p <- predicates) yield Exhale(p._1, em, null, p._2, check)).flatten :::
+ (for (p <- predicates) yield Exhale(p._1, em, null, p._2, check, currentK, exactchecking)).flatten :::
(Mask := em) ::
bassume(wf(Heap, Mask)) ::
Comment("end exhale")
}
-
- def Exhale(p: Expression, em: Boogie.Expr, eh: Boogie.Expr, error: ErrorMessage, check: Boolean): List[Boogie.Stmt] = desugar(p) match {
+
+ def ExhalePermission(perm: Permission, obj: Expr, memberName: String, currentK: Expr, pos: Position, error: ErrorMessage, em: Boogie.Expr, exactchecking: Boolean): List[Boogie.Stmt] = {
+ val ec = needExactChecking(perm, exactchecking);
+
+ val (f, stmts) = extractKFromPermission(perm, currentK)
+ val n = extractEpsilonsFromPermission(perm);
+
+ stmts :::
+ (perm.permissionType match {
+ case PermissionType.Mixed =>
+ bassert(f > 0 || (f == 0 && n > 0), error.pos, error.message + " The permission at " + perm.pos + " might not be positive.") ::
+ DecPermissionBoth(obj, memberName, f, n, em, error, pos, ec)
+ case PermissionType.Epsilons =>
+ bassert(n > 0, error.pos, error.message + " The permission at " + perm.pos + " might not be positive.") ::
+ DecPermissionEpsilon(obj, memberName, n, em, error, pos)
+ case PermissionType.Fraction =>
+ bassert(f > 0, error.pos, error.message + " The permission at " + perm.pos + " might not be positive.") ::
+ DecPermission(obj, memberName, f, em, error, pos, ec)
+ })
+ }
+
+ // does this permission require exact checking, or is it enough to check that we have any permission > 0?
+ def needExactChecking(perm: Permission, default: Boolean): Boolean = {
+ perm match {
+ case Full => true
+ case Frac(_) => true
+ case Epsilon => default
+ case PredicateEpsilon(_) | MonitorEpsilon(_) | ChannelEpsilon(_) | ForkEpsilon(_) => true
+ case MethodEpsilon => default
+ case Epsilons(p) => true
+ case Star => false
+ case IntPermTimes(lhs, rhs) => needExactChecking(rhs, default)
+ case PermTimes(lhs, rhs) => {
+ val l = needExactChecking(lhs, default);
+ val r = needExactChecking(rhs, default);
+ if (l == false || r == false) false else true // if one side doesn't need exact checking, the whole multiplication doesn't
+ }
+ case PermPlus(lhs, rhs) => {
+ val l = needExactChecking(lhs, default);
+ val r = needExactChecking(rhs, default);
+ if (l == true || r == true) true else false // if one side needs exact checking, use exact
+ }
+ case PermMinus(lhs, rhs) => {
+ val l = needExactChecking(lhs, default);
+ val r = needExactChecking(rhs, default);
+ if (l == true || r == true) true else false // if one side needs exact checking, use exact
+ }
+ }
+ }
+
+ def Exhale(p: Expression, em: Boogie.Expr, eh: Boogie.Expr, error: ErrorMessage, check: Boolean, currentK: Expr, exactchecking: Boolean): List[Boogie.Stmt] = desugar(p) match {
case pred@MemberAccess(e, p) if pred.isPredicate =>
val tmp = Access(pred, Full);
tmp.pos = pred.pos;
- Exhale(tmp, em , eh, error, check)
- case AccessAll(obj, perm) => throw new Exception("should be desugared")
- case AccessSeq(s, None, perm) => throw new Exception("should be desugared")
- case acc@Access(e,perm:Write) =>
+ Exhale(tmp, em , eh, error, check, currentK, exactchecking)
+ case AccessAll(obj, perm) => throw new InternalErrorException("should be desugared")
+ case AccessSeq(s, None, perm) => throw new InternalErrorException("should be desugared")
+ case acc@Access(e,perm) =>
val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;
+ val (starKV, starK) = NewBVar("starK", tint, true);
- // look up the fraction
- val (fraction, checkFraction) = perm match {
- case Full => (IntLiteral(100), Nil)
- case Frac(fr) => (fr, bassert(0<=Tr(fr), fr.pos, "Fraction might be negative.") :: (if(! e.isPredicate) bassert(Tr(fr)<=100, fr.pos, "Fraction might exceed 100.") :: Nil else Nil) ::: Nil)
- }
-
- val (fractionV, frac) = NewBVar("fraction", tint, true);
// check definedness
(if(check) isDefined(e.e)(true) :::
- checkFraction :::
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 && 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);
- BLocal(bplVar) :: (VarExpr(sourceVar.UniqueName) := frac) ::
- If(new MapSelect(em, Tr(e.e), memberName, "perm$R") < frac,
- Exhale(perm match {
- case Frac(p) => FractionOf(SubstThis(DefinitionOf(e.predicate), e.e), new VariableExpr(sourceVar));
- case Full => SubstThis(DefinitionOf(e.predicate), e.e)}, em, eh, ErrorMessage(error.pos, error.message + " Automatic fold might fail."), false) :::
- inhaleTran.Inhale(List(perm match {
- case Full => Access(e, Full);
- case Frac(p) => Access(e, Frac(new VariableExpr(sourceVar)))}), "automatic fold", false)
- , Nil) :: Nil}
- else Nil) :::
+ // TODO: include automagic again
// check that the necessary permissions are there and remove them from the mask
- DecPermission(Tr(e.e), memberName, frac, em, error, acc.pos) :::
- bassume(IsGoodMask(Mask)) ::
- bassume(wf(Heap, Mask)) ::
- bassume(wf(Heap, em))
- case rd@Access(e,perm:Read) =>
- val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;
- val (epsilonsV, eps) = NewBVar("epsilons", tint, true);
- val (dfP, epsilons) = perm match {
- case Epsilon => (List(), IntLiteral(1))
- case Star => (List(), null)
- case Epsilons(p) => (isDefined(p)(true) ::: List(bassert(0 <= Tr(p), error.pos, error.message + " The number of epsilons at " + rd.pos + " might be negative.")) , p)
- }
- // check definedness
- (if(check) isDefined(e.e)(true) :::
- bassert(nonNull(Tr(e.e)), error.pos, error.message + " The target of the rd predicate at " + rd.pos + " might be null.") ::
- 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 && 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);
- BLocal(bplVar) :: (VarExpr(sourceVar.UniqueName) := eps) ::
- If(new MapSelect(em, Tr(e.e), memberName, "perm$N") < eps,
- Exhale(EpsilonsOf(SubstThis(DefinitionOf(e.predicate), e.e), new VariableExpr(sourceVar)), em, eh, ErrorMessage(error.pos, error.message + " Automatic fold might fail."), false) :::
- inhaleTran.Inhale(List(Access(e, Epsilons(new VariableExpr(sourceVar)))), "automatic fold", false)
- , Nil) :: Nil}
- else Nil) :::
- // check that the necessary permissions are there and remove them from the mask
- DecPermissionEpsilon(Tr(e.e), memberName, if(epsilons != null) eps else null, em, error, rd.pos) :::
+ ExhalePermission(perm, Tr(e.e), memberName, currentK, acc.pos, error, em, exactchecking) :::
bassume(IsGoodMask(Mask)) ::
bassume(wf(Heap, Mask)) ::
bassume(wf(Heap, em))
case acc @ AccessSeq(s, Some(member), perm) =>
- if (member.isPredicate) throw new Exception("not yet implemented");
+ if (member.isPredicate) throw new NotSupportedException("not yet implemented");
val e = Tr(s);
val memberName = member.f.FullName;
- val (r, n) = perm match {
- case Full => (100, 0) : (Expr, Expr)
- case Frac(p) => (p, 0) : (Expr, Expr)
- case Epsilon => (0, 1) : (Expr, Expr) // TODO: check for infinity bounds -- or perhaps just wait till epsilons are gone
- case Epsilons(p) => (0, p) : (Expr, Expr)
- case Star => throw new Exception("not yet implemented")
- };
+
+ val (r, stmts) = extractKFromPermission(perm, currentK)
+ val n = extractEpsilonsFromPermission(perm);
+ val ec = needExactChecking(perm, exactchecking);
+ stmts :::
(if (check) isDefined(s)(true) ::: isDefined(perm)(true) else Nil) :::
{
val (aV,a) = Boogie.NewTVar("alpha");
@@ -1929,12 +1977,30 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E val (pcV,pc) = Boogie.NewBVar("p", tperm, true);
val mr = em(ref, memberName)("perm$R");
val mn = em(ref, memberName)("perm$N");
-
+
+ // assert that the permission is positive
+ bassert((SeqContains(e, ref) ==>
+ (perm.permissionType match {
+ case PermissionType.Fraction => r > 0
+ case PermissionType.Mixed => r > 0 || (r == 0 && n > 0)
+ case PermissionType.Epsilons => n > 0
+ })).forall(refV), error.pos, error.message + " The permission at " + acc.pos + " might not be positive.") ::
+ // make sure enough permission is available
bassert((SeqContains(e, ref) ==>
- (perm match {
- case _: Read => mr ==@ 0 ==> n <= mn
- case _: Write => r <= mr && (r ==@ mr ==> 0 <= mn)
- })).forall(refV), error.pos, error.message + " Insufficient permissions at " + acc.pos + " for " + member.f.FullName) ::
+ ((perm,perm.permissionType) match {
+ case _ if !ec => mr > 0
+ case (Star,_) => mr > 0
+ case (_,PermissionType.Fraction) => r <= mr && (r ==@ mr ==> 0 <= mn)
+ case (_,PermissionType.Mixed) => r <= mr && (r ==@ mr ==> n <= mn)
+ case (_,PermissionType.Epsilons) => mr ==@ 0 ==> n <= mn
+ })).forall(refV), error.pos, error.message + " Insufficient permission at " + acc.pos + " for " + member.f.FullName) ::
+ // additional assumption on k if we have a star permission or use inexact checking
+ ( perm match {
+ case _ if !ec => bassume((SeqContains(e, ref) ==> (r < mr)).forall(refV)) :: Nil
+ case Star => bassume((SeqContains(e, ref) ==> (r < mr)).forall(refV)) :: Nil
+ case _ => Nil
+ }) :::
+ // update the map
(em := Lambda(List(aV), List(refV, fV),
(SeqContains(e, ref) && f ==@ memberName).thenElse(
Lambda(List(), List(pcV), (pc ==@ "perm$R").thenElse(mr - r, mn - n)),
@@ -1955,12 +2021,12 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E new Boogie.MapUpdate(Credits, trCh, new Boogie.MapSelect(Credits, trCh) - Tr(cr.N))
case Implies(e0,e1) =>
(if(check) isDefined(e0)(true) else Nil) :::
- Boogie.If(Tr(e0), Exhale(e1, em, eh, error, check), Nil)
+ Boogie.If(Tr(e0), Exhale(e1, em, eh, error, check, currentK, exactchecking), Nil)
case IfThenElse(con, then, els) =>
(if(check) isDefined(con)(true) else Nil) :::
- Boogie.If(Tr(con), Exhale(then, em, eh, error, check), Exhale(els, em, eh, error, check))
+ Boogie.If(Tr(con), Exhale(then, em, eh, error, check, currentK, exactchecking), Exhale(els, em, eh, error, check, currentK, exactchecking))
case And(e0,e1) =>
- Exhale(e0, em, eh, error, check) ::: Exhale(e1, em, eh, error, check)
+ Exhale(e0, em, eh, error, check, currentK, exactchecking) ::: Exhale(e1, em, eh, error, check, currentK, exactchecking)
case holds@Holds(e) =>
(if(check) isDefined(e)(true) :::
bassert(nonNull(Tr(e)), error.pos, error.message + " The target of the holds predicate at " + holds.pos + " might be null.") :: Nil else Nil) :::
@@ -1980,9 +2046,63 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E bassume(IsGoodMask(preEtran.Mask)) ::
bassume(wf(preEtran.Heap, preEtran.Mask)) ::
bassert(proofOrAssume, p.pos, "Arguments for joinable might not match up.") ::
- preEtran.Exhale(List((e, error)), "eval", check)
+ preEtran.Exhale(List((e, error)), "eval", check, currentK, exactchecking)
case e => (if(check) isDefined(e)(true) else Nil) ::: List(bassert(Tr(e), error.pos, error.message + " The expression at " + e.pos + " might not evaluate to true."))
}
+
+ def extractKFromPermission(expr: Permission, currentK: Expr): (Expr, List[Boogie.Stmt]) = expr match {
+ case Full => (permissionFull, Nil)
+ case Epsilon => (currentK, Nil)
+ case Epsilons(_) => (0, Nil)
+ case PredicateEpsilon(_) => (predicateK, Nil)
+ case MonitorEpsilon(_) => (monitorK, Nil)
+ case ChannelEpsilon(_) => (channelK, Nil)
+ case MethodEpsilon => (currentK, Nil)
+ case ForkEpsilon(token) =>
+ val fk = etran.Heap.select(Tr(token), forkK)
+ (fk, bassume(0 < fk && fk < permissionFull) /* this is always true for forkK */)
+ case Star =>
+ val (starKV, starK) = NewBVar("starK", tint, true);
+ (starK, BLocal(starKV) :: bassume(starK > 0 /* an upper bound is provided later by DecPermission */) :: Nil)
+ case Frac(p) => (percentPermission(Tr(p)), Nil)
+ case IntPermTimes(lhs, rhs) => {
+ val (r, rs) = extractKFromPermission(rhs, currentK)
+ (lhs * r, rs)
+ }
+ case PermTimes(lhs, rhs) => {
+ val (l, ls) = extractKFromPermission(lhs, currentK)
+ val (r, rs) = extractKFromPermission(rhs, currentK)
+ val (resV, res) = Boogie.NewBVar("productK", tint, true)
+ (res, ls ::: rs ::: BLocal(resV) :: bassume(permissionFull * res ==@ l * r) :: Nil)
+ }
+ case PermPlus(lhs, rhs) => {
+ val (l, ls) = extractKFromPermission(lhs, currentK)
+ val (r, rs) = extractKFromPermission(rhs, currentK)
+ (l + r, Nil)
+ }
+ case PermMinus(lhs, rhs) => {
+ val (l, ls) = extractKFromPermission(lhs, currentK)
+ val (r, rs) = extractKFromPermission(rhs, currentK)
+ (l - r, Nil)
+ }
+ }
+
+ def extractEpsilonsFromPermission(expr: Permission): Expr = expr match {
+ case _:Write => 0
+ case Epsilons(n) => Tr(n)
+ case PermTimes(lhs, rhs) => 0 // multiplication cannot give epsilons
+ case IntPermTimes(lhs, rhs) => lhs * extractEpsilonsFromPermission(rhs)
+ case PermPlus(lhs, rhs) => {
+ val l = extractEpsilonsFromPermission(lhs)
+ val r = extractEpsilonsFromPermission(rhs)
+ l + r
+ }
+ case PermMinus(lhs, rhs) => {
+ val l = extractEpsilonsFromPermission(lhs)
+ val r = extractEpsilonsFromPermission(rhs)
+ l - r
+ }
+ }
def fromEvalState(h: EvalState): (Expr, Expr, Expr, List[Stmt], Expr) = {
h match {
@@ -2028,47 +2148,41 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E def SetNoPermission(obj: Boogie.Expr, field: String, mask: Boogie.Expr) =
Boogie.Assign(new Boogie.MapSelect(mask, obj, field), Boogie.VarExpr("Permission$Zero"))
def HasFullPermission(obj: Boogie.Expr, field: String, mask: Boogie.Expr) =
- (new Boogie.MapSelect(mask, obj, field, "perm$R") ==@ Boogie.IntLiteral(100)) &&
+ (new Boogie.MapSelect(mask, obj, field, "perm$R") ==@ permissionFull) &&
(new Boogie.MapSelect(mask, obj, field, "perm$N") ==@ Boogie.IntLiteral(0))
def SetFullPermission(obj: Boogie.Expr, field: String) =
Boogie.Assign(new Boogie.MapSelect(Mask, obj, field), Boogie.VarExpr("Permission$Full"))
- def IncPermission(obj: Boogie.Expr, field: String, howMuch: Boogie.Expr) =
- MapUpdate3(Mask, obj, field, "perm$R", new Boogie.MapSelect(Mask, obj, field, "perm$R") + howMuch)
- def IncPermissionEpsilon(obj: Boogie.Expr, field: String, epsilons: Boogie.Expr) =
- if (epsilons != null) {
- val g = (new Boogie.MapSelect(Mask, obj, field, "perm$N") !=@ Boogie.VarExpr("Permission$MinusInfinity")) &&
- (new Boogie.MapSelect(Mask, obj, field, "perm$N") !=@ Boogie.VarExpr("Permission$PlusInfinity"))
- Boogie.If(g,
- MapUpdate3(Mask, obj, field, "perm$N", new Boogie.MapSelect(Mask, obj, field, "perm$N") + epsilons) ::
- bassume(Boogie.FunctionApp("wf", List(Heap, Mask))) :: Nil
- , Nil)
- } else {
- val g = (new Boogie.MapSelect(Mask, obj, field, "perm$N") !=@ Boogie.VarExpr("Permission$MinusInfinity"))
- Boogie.If(g, MapUpdate3(Mask, obj, field, "perm$N", Boogie.VarExpr("Permission$PlusInfinity")), Nil)
- }
- def DecPermission(obj: Boogie.Expr, field: String, howMuch: Boogie.Expr, mask: Boogie.Expr, error: ErrorMessage, pos: Position) = {
+ def IncPermission(obj: Boogie.Expr, field: String, howMuch: Boogie.Expr): List[Boogie.Stmt] = {
+ MapUpdate3(Mask, obj, field, "perm$R", new Boogie.MapSelect(Mask, obj, field, "perm$R") + howMuch) :: Nil
+ }
+ def IncPermissionEpsilon(obj: Boogie.Expr, field: String, epsilons: Boogie.Expr): List[Boogie.Stmt] = {
+ MapUpdate3(Mask, obj, field, "perm$N", new Boogie.MapSelect(Mask, obj, field, "perm$N") + epsilons) ::
+ bassume(Boogie.FunctionApp("wf", List(Heap, Mask))) :: Nil
+ }
+ def DecPermission(obj: Boogie.Expr, field: String, howMuch: Boogie.Expr, mask: Boogie.Expr, error: ErrorMessage, pos: Position, exactchecking: Boolean): List[Boogie.Stmt] = {
val fP: Boogie.Expr = new Boogie.MapSelect(mask, obj, field, "perm$R")
val fC: Boogie.Expr = new Boogie.MapSelect(mask, obj, field, "perm$N")
- bassert(howMuch <= fP && (howMuch ==@ fP ==> 0 <= fC), error.pos, error.message + " Insufficient fraction at " + pos + " for " + field + ".") ::
+ (if (exactchecking) bassert(howMuch <= fP && (howMuch ==@ fP ==> 0 <= fC), error.pos, error.message + " Insufficient fraction at " + pos + " for " + field + ".") :: Nil
+ else bassert(fP > 0, error.pos, error.message + " Insufficient fraction at " + pos + " for " + field + ".") :: bassume(howMuch < fP)) :::
MapUpdate3(mask, obj, field, "perm$R", new Boogie.MapSelect(mask, obj, field, "perm$R") - howMuch)
}
- def DecPermissionEpsilon(obj: Boogie.Expr, field: String, epsilons: Boogie.Expr, mask: Boogie.Expr, error: ErrorMessage, pos: Position) =
- if (epsilons != null) {
- val g = (new Boogie.MapSelect(mask, obj, field, "perm$N") !=@ Boogie.VarExpr("Permission$MinusInfinity")) &&
- (new Boogie.MapSelect(mask, obj, field, "perm$N") !=@ Boogie.VarExpr("Permission$PlusInfinity"))
- val xyz = new Boogie.MapSelect(mask, obj, field, "perm$N")
- bassert((new Boogie.MapSelect(mask, obj, field, "perm$R") ==@ Boogie.IntLiteral(0)) ==> (epsilons <= xyz), error.pos, error.message + " Insufficient epsilons at " + pos + " for " + field + ".") ::
- Boogie.If(g,
- MapUpdate3(mask, obj, field, "perm$N", new Boogie.MapSelect(mask, obj, field, "perm$N") - epsilons) ::
- bassume(Boogie.FunctionApp("wf", List(Heap, Mask))) :: Nil
- , Nil)
- } else {
- val g = (new Boogie.MapSelect(mask, obj, field, "perm$N") !=@ Boogie.VarExpr("Permission$PlusInfinity"))
- bassert((new Boogie.MapSelect(mask, obj, field, "perm$R") ==@ Boogie.IntLiteral(0)) ==>
- (new Boogie.MapSelect(mask, obj, field, "perm$N") ==@ Boogie.VarExpr("Permission$PlusInfinity")), error.pos, error.message + " Insufficient epsilons at " + pos + " for " + field + ".") ::
- Boogie.If(g, MapUpdate3(mask, obj, field, "perm$N", Boogie.VarExpr("Permission$MinusInfinity")), Nil)
- }
+ def DecPermissionEpsilon(obj: Boogie.Expr, field: String, epsilons: Boogie.Expr, mask: Boogie.Expr, error: ErrorMessage, pos: Position): List[Boogie.Stmt] = {
+ val xyz = new Boogie.MapSelect(mask, obj, field, "perm$N")
+ bassert((new Boogie.MapSelect(mask, obj, field, "perm$R") ==@ Boogie.IntLiteral(0)) ==> (epsilons <= xyz), error.pos, error.message + " Insufficient epsilons at " + pos + " for " + field + ".") ::
+ MapUpdate3(mask, obj, field, "perm$N", new Boogie.MapSelect(mask, obj, field, "perm$N") - epsilons) ::
+ bassume(Boogie.FunctionApp("wf", List(Heap, Mask))) :: Nil
+ }
+ def DecPermissionBoth(obj: Boogie.Expr, field: String, howMuch: Boogie.Expr, epsilons: Boogie.Expr, mask: Boogie.Expr, error: ErrorMessage, pos: Position, exactchecking: Boolean): List[Boogie.Stmt] = {
+ val fP: Boogie.Expr = new Boogie.MapSelect(mask, obj, field, "perm$R")
+ val fC: Boogie.Expr = new Boogie.MapSelect(mask, obj, field, "perm$N")
+
+ (if (exactchecking) bassert(howMuch <= fP && (howMuch ==@ fP ==> epsilons <= fC), error.pos, error.message + " Insufficient permission at " + pos + " for " + field + ".") :: Nil
+ else bassert(fP > 0, error.pos, error.message + " Insufficient permission at " + pos + " for " + field + ".") :: bassume(howMuch < fP)) :::
+ MapUpdate3(mask, obj, field, "perm$N", fC - epsilons) ::
+ bassume(Boogie.FunctionApp("wf", List(Heap, Mask))) ::
+ MapUpdate3(mask, obj, field, "perm$R", fP - howMuch) :: Nil
+ }
def MapUpdate3(m: Boogie.Expr, arg0: Boogie.Expr, arg1: String, arg2: String, rhs: Boogie.Expr) = {
// m[a,b,c] := rhs
@@ -2085,20 +2199,20 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E def MaxLockIsBelowX(x: Boogie.Expr) = { // waitlevel << x
- val (oV, o) = Boogie.NewBVar("o", tref, false)
+ val (oV, o) = Boogie.NewBVar("o", tref, true)
new Boogie.Forall(oV,
(contributesToWaitLevel(o, Heap, Credits)) ==>
new Boogie.FunctionApp("MuBelow", new Boogie.MapSelect(Heap, o, "mu"), x))
}
def MaxLockIsAboveX(x: Boogie.Expr) = { // x << waitlevel
- val (oV, o) = Boogie.NewBVar("o", tref, false)
+ val (oV, o) = Boogie.NewBVar("o", tref, true)
new Boogie.Exists(oV,
(contributesToWaitLevel(o, Heap, Credits)) &&
new Boogie.FunctionApp("MuBelow", x, new Boogie.MapSelect(Heap, o, "mu")))
}
def IsHighestLock(x: Boogie.Expr) = {
// (forall r :: r.held ==> r.mu << x || r.mu == x)
- val (rV, r) = Boogie.NewBVar("r", tref, false)
+ val (rV, r) = Boogie.NewBVar("r", tref, true)
new Boogie.Forall(rV,
contributesToWaitLevel(r, Heap, Credits) ==>
(new Boogie.FunctionApp("MuBelow", new MapSelect(Heap, r, "mu"), x) ||
@@ -2111,7 +2225,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E // (forall r: ref ::
// old(Heap)[r,held] == Heap[r,held] &&
// (Heap[r,held] ==> old(Heap)[r,mu] == Heap[r,mu]))
- val (rV, r) = Boogie.NewBVar("r", tref, false)
+ val (rV, r) = Boogie.NewBVar("r", tref, true)
val b0 = new Boogie.Forall(rV,
((0 < new Boogie.MapSelect(oldEtran.Heap, r, "held")) ==@
(0 < new Boogie.MapSelect(Heap, r, "held"))) &&
@@ -2124,8 +2238,8 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E // p.held && (forall r :: r.held ==> r.mu << p.mu || r.mu == p.mu )
// ==>
// old(o.mu) == p.mu)
- val (oV, o) = Boogie.NewBVar("o", tref, false)
- val (pV, p) = Boogie.NewBVar("p", tref, false)
+ val (oV, o) = Boogie.NewBVar("o", tref, true)
+ val (pV, p) = Boogie.NewBVar("p", tref, true)
val b1 = Boogie.Forall(Nil, List(oV,pV), Nil,
((0 < new Boogie.MapSelect(oldEtran.Heap, o, "held")) &&
oldEtran.IsHighestLock(new Boogie.MapSelect(oldEtran.Heap, o, "mu")) &&
@@ -2139,16 +2253,11 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E // (exists o ::
// e1(o.held) &&
// (forall r :: e0(r.held) ==> e0(r.mu) << e1(o.mu)))
- val (oV, o) = Boogie.NewBVar("o", tref, false)
+ val (oV, o) = Boogie.NewBVar("o", tref, true)
new Boogie.Exists(oV,
(0 < new Boogie.MapSelect(e1.Heap, o, "held")) &&
e0.MaxLockIsBelowX(new Boogie.MapSelect(e1.Heap, o, "mu")))
}
-
- def fractionOk(expr: Expression) = {
- bassert(0 <= Tr(expr), expr.pos, "Fraction might be negative.") ::
- bassert(Tr(expr) <= 100, expr.pos, "Fraction might exceed 100.")
- }
}
// implicit (uses etran)
@@ -2194,6 +2303,9 @@ object TranslationHelper { // prelude definitions
+ def todoiparam: Expr = IntLiteral(-1); // This value is used as parameter at places where Chalice has not been updated to the new permission model.
+ def todobparam: Boolean = true; // This value is used as parameter at places where Chalice has not been updated to the new permission model.
+
def ModuleType = NamedType("ModuleName");
def ModuleName(cl: Class) = "module#" + cl.module.id;
def TypeName = NamedType("TypeName");
@@ -2219,6 +2331,18 @@ object TranslationHelper { def CreditsName = "Credits";
def GlobalNames = List(HeapName, MaskName, CreditsName);
def CanAssumeFunctionDefs = VarExpr("CanAssumeFunctionDefs");
+ def permissionFull = percentPermission(100);
+ def permissionOnePercent = percentPermission(1);
+ def percentPermission(e: Expr) = {
+ Chalice.percentageSupport match {
+ case 0 | 1 => e*VarExpr("Permission$denominator")
+ case 2 | 3 => FunctionApp("Fractions", List(e))
+ }
+ }
+ def forkK = "forkK";
+ def channelK = "channelK";
+ def monitorK = "monitorK";
+ def predicateK = "predicateK";
def CurrentModule = VarExpr("CurrentModule");
def IsGoodState(e: Expr) = FunctionApp("IsGoodState", List(e));
def dtype(e: Expr) = FunctionApp("dtype", List(e))
@@ -2266,50 +2390,35 @@ object TranslationHelper { override val where = TypeInformation(new Boogie.VarExpr(id), tp.typ) }
}
- // scale an expression by a fraction
- def FractionOf(expr: Expression, fraction: Expression) : Expression = {
+ // scale an expression (such as the definition of a predicate) by a permission
+ def scaleExpressionByPermission(expr: Expression, perm1: Permission, pos: Position): Expression = {
val result = expr match {
- case Access(e, Full) => Access(e, Frac(fraction))
- case AccessSeq(e, f, Full) => AccessSeq(e, f, Frac(fraction))
- case And(lhs, rhs) => And(FractionOf(lhs, fraction), FractionOf(rhs, fraction))
- case Implies(lhs, rhs) => Implies(lhs, FractionOf(rhs, fraction))
+ case Access(e, perm2) => Access(e, multiplyPermission(perm1, perm2, pos))
+ case AccessSeq(e, f, perm2) => AccessSeq(e, f, multiplyPermission(perm1, perm2, pos))
+ case And(lhs, rhs) => And(scaleExpressionByPermission(lhs, perm1, pos), scaleExpressionByPermission(rhs, perm1, pos))
+ case Implies(lhs, rhs) => Implies(lhs, scaleExpressionByPermission(rhs, perm1, pos))
case _ if ! expr.isInstanceOf[PermissionExpr] => expr
- case _ => throw new Exception(" " + expr.pos + ": Scaling non-full permissions is not supported yet." + expr);
+ case _ => throw new InternalErrorException("Unexpected expression, unable to scale.");
}
result.pos = expr.pos;
result
}
-
- def canTakeFractionOf(expr: Expression): Boolean = {
- expr match {
- case Access(e, Full) => true
- case AccessSeq(e, f, Full) => true
- case And(lhs, rhs) => canTakeFractionOf(lhs) && canTakeFractionOf(rhs)
- case Implies(lhs, rhs) => canTakeFractionOf(rhs)
- case _ if ! expr.isInstanceOf[PermissionExpr] => true
- case _ => false
- }
- }
-
- // scale an expression by a number of epsilons
- def EpsilonsOf(expr: Expression, nbEpsilons: Expression) : Expression = {
- val result = expr match {
- case Access(e, _:Write) => Access(e, Epsilons(nbEpsilons))
- case And(lhs, rhs) => And(FractionOf(lhs, nbEpsilons), FractionOf(rhs, nbEpsilons))
- case _ if ! expr.isInstanceOf[PermissionExpr] => expr
- case _ => throw new Exception(" " + expr.pos + ": Scaling non-full permissions is not supported yet." + expr);
+
+ // multiply two permissions
+ def multiplyPermission(perm1: Permission, perm2: Permission, pos: Position): Permission = {
+ val result = (perm1,perm2) match {
+ case (Full,p2) => p2
+ case (p1,Full) => p1
+ case (Epsilons(_),_) => throw new NotSupportedException(pos + ": Scaling epsilon permissions with non-full permissions is not possible.")
+ case (_,Epsilons(_)) => throw new NotSupportedException(pos + ": Scaling epsilon permissions with non-full permissions is not possible.")
+ case (p1,p2) => PermTimes(p1,p2)
}
- result.pos = expr.pos;
result
}
-
- def canTakeEpsilonsOf(expr: Expression): Boolean = {
- expr match {
- case Access(e, _:Write) => true
- case And(lhs, rhs) => canTakeEpsilonsOf(lhs) && canTakeEpsilonsOf(rhs)
- case _ if ! expr.isInstanceOf[PermissionExpr] => true
- case _ => false
- }
+
+ // TODO: this method is used by the method tranform extension, which has not yet been updated to the new permission model
+ def FractionOf(expr: Expression, fraction: Expression) : Expression = {
+ throw new NotSupportedException("Not supported")
}
def TypeInformation(e: Boogie.Expr, cl: Class): Boogie.Expr = {
@@ -2342,9 +2451,9 @@ object TranslationHelper { else Boogie.FunctionApp("combine", List(l, r))
case IfThenElse(con, then, els) =>
Boogie.Ite(etran.Tr(con), Version(then, etran), Version(els, etran))
- case _: PermissionExpr => throw new Exception("unexpected permission expression")
+ case _: PermissionExpr => throw new InternalErrorException("unexpected permission expression")
case e =>
- e visit {_ match { case _ : PermissionExpr => throw new Exception("unexpected permission expression"); case _ =>}}
+ e visit {_ match { case _ : PermissionExpr => throw new InternalErrorException("unexpected permission expression"); case _ =>}}
nostate
}
}
@@ -2370,9 +2479,9 @@ object TranslationHelper { Version(e0, etran1, etran2) && Version(e1, etran1, etran2)
case IfThenElse(con, then, els) =>
Version(then, etran1, etran2) && Version(els, etran1, etran2)
- case _: PermissionExpr => throw new Exception("unexpected permission expression")
+ case _: PermissionExpr => throw new InternalErrorException("unexpected permission expression")
case e =>
- e visit {_ match { case _ : PermissionExpr => throw new Exception("unexpected permission expression"); case _ =>}}
+ e visit {_ match { case _ : PermissionExpr => throw new InternalErrorException("unexpected permission expression"); case _ =>}}
Boogie.BoolLiteral(true)
}
}
@@ -2417,9 +2526,30 @@ object TranslationHelper { case Access(ma@MemberAccess(obj, f), perm) =>
val (assumptions, handled1) = automagic(obj, handled ::: List(ma));
perm match {
- case Full | Epsilon | Star => (assumptions, handled1);
+ case Full | Epsilon | Star | MethodEpsilon => (assumptions, handled1);
case Frac(fraction) => val result = automagic(fraction, handled1); (assumptions ::: result._1, result._2)
case Epsilons(epsilon) => val result = automagic(epsilon, handled1); (assumptions ::: result._1, result._2)
+ case ChannelEpsilon(None) | PredicateEpsilon(None) | MonitorEpsilon(None) => (assumptions, handled1)
+ case ChannelEpsilon(Some(e)) => val result = automagic(e, handled1); (assumptions ::: result._1, result._2)
+ case PredicateEpsilon(Some(e)) => val result = automagic(e, handled1); (assumptions ::: result._1, result._2)
+ case MonitorEpsilon(Some(e)) => val result = automagic(e, handled1); (assumptions ::: result._1, result._2)
+ case ForkEpsilon(e) => val result = automagic(e, handled1); (assumptions ::: result._1, result._2)
+ case IntPermTimes(e0, e1) =>
+ val (assumptions1, handled2) = automagic(e0, handled1);
+ val result = automagic(e1, handled2);
+ (assumptions ::: assumptions1 ::: result._1, result._2)
+ case PermTimes(e0, e1) =>
+ val (assumptions1, handled2) = automagic(e0, handled1);
+ val result = automagic(e1, handled2);
+ (assumptions ::: assumptions1 ::: result._1, result._2)
+ case PermPlus(e0, e1) =>
+ val (assumptions1, handled2) = automagic(e0, handled1);
+ val result = automagic(e1, handled2);
+ (assumptions ::: assumptions1 ::: result._1, result._2)
+ case PermMinus(e0, e1) =>
+ val (assumptions1, handled2) = automagic(e0, handled1);
+ val result = automagic(e1, handled2);
+ (assumptions ::: assumptions1 ::: result._1, result._2)
}
case AccessAll(obj, perm) =>
automagic(obj, handled)
@@ -2491,8 +2621,9 @@ object TranslationHelper { }
def SubstRd(e: Expression): Expression = e match {
- case Access(e, _:Write) =>
- val r = Access(e,Epsilon); r.pos = e.pos; r.typ = BoolClass; r
+ case Access(e, _:Permission) =>
+ //val r = Access(e,MonitorEpsilon(None)); r.pos = e.pos; r.typ = BoolClass; r
+ val r = Access(e,Epsilons(IntLiteral(1))); r.pos = e.pos; r.typ = BoolClass; r
case Implies(e0,e1) =>
val r = Implies(e0, SubstRd(e1)); r.pos = e.pos; r.typ = BoolClass; r
case And(e0,e1) =>
@@ -2506,13 +2637,8 @@ object TranslationHelper { case pred@MemberAccess(o, f) if pred.isPredicate && o.isInstanceOf[ThisExpr] =>
Some(SubstThis(DefinitionOf(pred.predicate), o))
case Access(pred@MemberAccess(o, f), p) if pred.isPredicate && o.isInstanceOf[ThisExpr] =>
- Some(p match {
- case Full => SubstThis(DefinitionOf(pred.predicate), o)
- case Frac(p) => FractionOf(SubstThis(DefinitionOf(pred.predicate), o), p)
- case Epsilon => EpsilonsOf(SubstThis(DefinitionOf(pred.predicate), o), IntLiteral(1))
- case Star => throw new Exception("not supported yet")
- case Epsilons(p) => EpsilonsOf(SubstThis(DefinitionOf(pred.predicate), o), p)
- })
+ val definition = scaleExpressionByPermission(SubstThis(DefinitionOf(pred.predicate), o), p, e.pos)
+ Some(definition)
case func@FunctionApplication(obj: ThisExpr, name, args) if 2<=Chalice.defaults && func.f.definition.isDefined =>
Some(SubstVars(func.f.definition.get, obj, func.f.ins, args))
case _ => None
@@ -2530,7 +2656,7 @@ object TranslationHelper { case e: VariableExpr =>
if (vs.contains(e.v)) Some(vs(e.v)) else None;
case q: Quantification =>
- q.variables foreach { (v) => if (vs.contains(v)) throw new Exception("cannot substitute a variable bound in the quantifier")}
+ q.variables foreach { (v) => if (vs.contains(v)) throw new InternalErrorException("cannot substitute a variable bound in the quantifier")}
None;
case _ => None;
}
@@ -2543,13 +2669,39 @@ object TranslationHelper { def SubstResult(expr: Expression, x: Expression): Expression = expr.transform {
case _: Result => Some(x)
case _ => None
- }
+ }
// De-sugar expression (idempotent)
// * unroll wildcard pattern (for objects) in permission expression
// * convert sequence quantification into type quantification
+ // * perform simple permission expression optimizations (e.g. Frac(1)+Frac(1) = Frac(1+1) or Frac(100) = Full)
+ // * simplify quantification over empty sequences
def desugar(expr: Expression): Expression = expr transform {
_ match {
+ case Frac(IntLiteral(100)) => Some(Full)
+ case PermTimes(Full, r) => Some(r)
+ case PermTimes(l, Full) => Some(l)
+ case PermPlus(lhs, rhs) =>
+ val ll = desugar(lhs)
+ val rr = desugar(rhs)
+ (ll, rr) match {
+ case (Frac(l), Frac(r)) => Some(Frac(Plus(l,r)))
+ case _ => Some(PermPlus(ll.asInstanceOf[Permission], rr.asInstanceOf[Permission]))
+ }
+ case PermMinus(lhs, rhs) =>
+ val ll = desugar(lhs)
+ val rr = desugar(rhs)
+ (ll, rr) match {
+ case (Frac(l), Frac(r)) => Some(Frac(Minus(l,r)))
+ case _ => Some(PermMinus(ll.asInstanceOf[Permission], rr.asInstanceOf[Permission]))
+ }
+ case PermTimes(lhs, rhs) =>
+ val ll = desugar(lhs)
+ val rr = desugar(rhs)
+ (ll, rr) match {
+ case (Frac(l), Frac(r)) => Some(Frac(Times(l,r)))
+ case _ => Some(PermTimes(ll.asInstanceOf[Permission], rr.asInstanceOf[Permission]))
+ }
case AccessAll(obj, perm) =>
Some(obj.typ.Fields.map({f =>
val ma = MemberAccess(desugar(obj), f.id);
@@ -2588,9 +2740,13 @@ object TranslationHelper { case Exists => And(assumption, de);
}
body.pos = expr.pos;
- val result = TypeQuantification(q, is, new Type(IntClass), body);
+ val result = TypeQuantification(q, is, new Type(IntClass), body, (dmin,dmax));
result.variables = dis;
Some(result);
+ case qe @ SeqQuantification(Forall, is, ExplicitSeq(List()), e) => Some(BoolLiteral(true))
+ case qe @ SeqQuantification(Exists, is, ExplicitSeq(List()), e) => Some(BoolLiteral(false))
+ case qe @ SeqQuantification(Forall, is, EmptySeq(_), e) => Some(BoolLiteral(true))
+ case qe @ SeqQuantification(Exists, is, EmptySeq(_), e) => Some(BoolLiteral(false))
case qe @ SeqQuantification(q, is, seq, e) =>
val dseq = desugar(seq);
val min = IntLiteral(0);
@@ -2610,7 +2766,7 @@ object TranslationHelper { case Exists => And(assumption, de);
}
body.pos = expr.pos;
- val result = TypeQuantification(q, is, new Type(IntClass), body);
+ val result = new TypeQuantification(q, is, new Type(IntClass), body);
result.variables = dis;
Some(result);
case _ => None;
@@ -2640,4 +2796,5 @@ object TranslationHelper { case s => s
}
}
+
}
diff --git a/Chalice/examples/AssociationList.chalice b/Chalice/tests/examples/AssociationList.chalice index cc3ecfb4..cc3ecfb4 100644 --- a/Chalice/examples/AssociationList.chalice +++ b/Chalice/tests/examples/AssociationList.chalice diff --git a/Chalice/tests/examples/AssociationList.output.txt b/Chalice/tests/examples/AssociationList.output.txt new file mode 100644 index 00000000..719af1af --- /dev/null +++ b/Chalice/tests/examples/AssociationList.output.txt @@ -0,0 +1,6 @@ +Verification of AssociationList.chalice
+
+ 19.3: The postcondition at 21.13 might not hold. Insufficient fraction at 21.13 for mu.
+ 64.9: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop.
+
+Boogie program verifier finished with 10 verified, 2 errors
diff --git a/Chalice/examples/CopyLessMessagePassing-with-ack.chalice b/Chalice/tests/examples/CopyLessMessagePassing-with-ack.chalice index 79e4d75e..2646f96a 100644 --- a/Chalice/examples/CopyLessMessagePassing-with-ack.chalice +++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack.chalice @@ -70,6 +70,7 @@ class Program { }
method Main(x: Node)
+ requires x != null;
requires x.list;
{
var e := new C;
diff --git a/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt b/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt new file mode 100644 index 00000000..46633611 --- /dev/null +++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt @@ -0,0 +1,4 @@ +Verification of CopyLessMessagePassing-with-ack.chalice
+
+
+Boogie program verifier finished with 11 verified, 0 errors
diff --git a/Chalice/examples/CopyLessMessagePassing-with-ack2.chalice b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.chalice index 41680258..7744d291 100644 --- a/Chalice/examples/CopyLessMessagePassing-with-ack2.chalice +++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.chalice @@ -75,6 +75,7 @@ class Program { }
method Main(x: Node)
+ requires x != null;
requires x.list;
{
var e := new C;
diff --git a/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt new file mode 100644 index 00000000..e8c42507 --- /dev/null +++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt @@ -0,0 +1,4 @@ +Verification of CopyLessMessagePassing-with-ack2.chalice
+
+
+Boogie program verifier finished with 12 verified, 0 errors
diff --git a/Chalice/examples/CopyLessMessagePassing.chalice b/Chalice/tests/examples/CopyLessMessagePassing.chalice index f5ca2372..4b8a9389 100644 --- a/Chalice/examples/CopyLessMessagePassing.chalice +++ b/Chalice/tests/examples/CopyLessMessagePassing.chalice @@ -59,6 +59,7 @@ class Program { }
method Main(x: Node)
+ requires x != null;
requires x.list;
{
var e := new C;
diff --git a/Chalice/tests/examples/CopyLessMessagePassing.output.txt b/Chalice/tests/examples/CopyLessMessagePassing.output.txt new file mode 100644 index 00000000..d6fd8be3 --- /dev/null +++ b/Chalice/tests/examples/CopyLessMessagePassing.output.txt @@ -0,0 +1,4 @@ +Verification of CopyLessMessagePassing.chalice
+
+
+Boogie program verifier finished with 11 verified, 0 errors
diff --git a/Chalice/examples/ForkJoin.chalice b/Chalice/tests/examples/ForkJoin.chalice index e79cded9..e79cded9 100644 --- a/Chalice/examples/ForkJoin.chalice +++ b/Chalice/tests/examples/ForkJoin.chalice diff --git a/Chalice/tests/examples/ForkJoin.output.txt b/Chalice/tests/examples/ForkJoin.output.txt new file mode 100644 index 00000000..06d44bec --- /dev/null +++ b/Chalice/tests/examples/ForkJoin.output.txt @@ -0,0 +1,4 @@ +Verification of ForkJoin.chalice
+
+
+Boogie program verifier finished with 18 verified, 0 errors
diff --git a/Chalice/examples/HandOverHand.chalice b/Chalice/tests/examples/HandOverHand.chalice index 307b653c..31818ca6 100644 --- a/Chalice/examples/HandOverHand.chalice +++ b/Chalice/tests/examples/HandOverHand.chalice @@ -18,7 +18,7 @@ class List { method Init()
requires acc(mu) && mu == lockbottom && acc(head) && acc(sum)
- ensures rd(mu,*) && waitlevel << this
+ ensures rd*(mu) && waitlevel << this
ensures acc(sum,80) && sum == 0
{
var t := new Node
@@ -46,11 +46,11 @@ class List { release this
while (p.next != null && p.next.val < x)
- invariant p != null && acc(p.next) && rd(p.val) && acc(p.mu,50)
+ invariant p != null && acc(p.next) && acc(p.val,rd(p)) && acc(p.mu,50)
invariant holds(p) && waitlevel == p.mu
invariant !old(holds(p)) && !old(rd holds(p))
invariant p.next != null ==> acc(p.next.mu,50) && p << p.next
- invariant p.next != null ==> rd(p.next.val) && p.val <= p.next.val
+ invariant p.next != null ==> acc(p.next.val,rd(p.next)) && p.val <= p.next.val
invariant acc(p.sum, 50)
invariant p.next == null ==> p.sum == x
invariant p.next != null ==> acc(p.next.sum, 50) && p.sum == p.next.val + p.next.sum + x
@@ -87,11 +87,11 @@ class List { release this
while (p.next != null && p.next.val < x)
- invariant p != null && acc(p.next) && rd(p.val) && acc(p.mu,50)
+ invariant p != null && acc(p.next) && acc(p.val,rd(p)) && acc(p.mu,50)
invariant holds(p) && waitlevel == p.mu && !assigned(c)
invariant !old(holds(p)) && !old(rd holds(p))
invariant p.next != null ==> acc(p.next.mu,50) && p << p.next
- invariant p.next != null ==> rd(p.next.val) && p.val <= p.next.val
+ invariant p.next != null ==> acc(p.next.val,rd(p.next)) && p.val <= p.next.val
invariant acc(p.sum, 50)
invariant p.next == null ==> p.sum == 0 - c
invariant p.next != null ==> acc(p.next.sum, 50) && p.sum == p.next.val + p.next.sum - c
diff --git a/Chalice/tests/examples/HandOverHand.output.txt b/Chalice/tests/examples/HandOverHand.output.txt new file mode 100644 index 00000000..a57fe677 --- /dev/null +++ b/Chalice/tests/examples/HandOverHand.output.txt @@ -0,0 +1,4 @@ +Verification of HandOverHand.chalice
+
+
+Boogie program verifier finished with 10 verified, 0 errors
diff --git a/Chalice/examples/ImplicitLocals.chalice b/Chalice/tests/examples/ImplicitLocals.chalice index 15ebe8e0..15ebe8e0 100644 --- a/Chalice/examples/ImplicitLocals.chalice +++ b/Chalice/tests/examples/ImplicitLocals.chalice diff --git a/Chalice/tests/examples/ImplicitLocals.output.txt b/Chalice/tests/examples/ImplicitLocals.output.txt new file mode 100644 index 00000000..c3f518ed --- /dev/null +++ b/Chalice/tests/examples/ImplicitLocals.output.txt @@ -0,0 +1,4 @@ +Verification of ImplicitLocals.chalice
+
+
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Chalice/examples/LoopLockChange.chalice b/Chalice/tests/examples/LoopLockChange.chalice index 5ccce089..5ccce089 100644 --- a/Chalice/examples/LoopLockChange.chalice +++ b/Chalice/tests/examples/LoopLockChange.chalice diff --git a/Chalice/tests/examples/LoopLockChange.output.txt b/Chalice/tests/examples/LoopLockChange.output.txt new file mode 100644 index 00000000..c6c69a24 --- /dev/null +++ b/Chalice/tests/examples/LoopLockChange.output.txt @@ -0,0 +1,7 @@ +Verification of LoopLockChange.chalice
+
+ 10.5: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop.
+ 35.5: The loop might lock/unlock more than the lockchange clause allows.
+ 65.5: The loop might lock/unlock more than the lockchange clause allows.
+
+Boogie program verifier finished with 14 verified, 3 errors
diff --git a/Chalice/examples/OwickiGries.chalice b/Chalice/tests/examples/OwickiGries.chalice index f466b58a..f466b58a 100644 --- a/Chalice/examples/OwickiGries.chalice +++ b/Chalice/tests/examples/OwickiGries.chalice diff --git a/Chalice/tests/examples/OwickiGries.output.txt b/Chalice/tests/examples/OwickiGries.output.txt new file mode 100644 index 00000000..ff585ab1 --- /dev/null +++ b/Chalice/tests/examples/OwickiGries.output.txt @@ -0,0 +1,4 @@ +Verification of OwickiGries.chalice
+
+
+Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Chalice/examples/PetersonsAlgorithm.chalice b/Chalice/tests/examples/PetersonsAlgorithm.chalice index 8760b04b..8760b04b 100644 --- a/Chalice/examples/PetersonsAlgorithm.chalice +++ b/Chalice/tests/examples/PetersonsAlgorithm.chalice diff --git a/Chalice/tests/examples/PetersonsAlgorithm.output.txt b/Chalice/tests/examples/PetersonsAlgorithm.output.txt new file mode 100644 index 00000000..bf470e3a --- /dev/null +++ b/Chalice/tests/examples/PetersonsAlgorithm.output.txt @@ -0,0 +1,4 @@ +Verification of PetersonsAlgorithm.chalice
+
+
+Boogie program verifier finished with 7 verified, 0 errors
diff --git a/Chalice/examples/ProdConsChannel.chalice b/Chalice/tests/examples/ProdConsChannel.chalice index 563d72b6..563d72b6 100644 --- a/Chalice/examples/ProdConsChannel.chalice +++ b/Chalice/tests/examples/ProdConsChannel.chalice diff --git a/Chalice/tests/examples/ProdConsChannel.output.txt b/Chalice/tests/examples/ProdConsChannel.output.txt new file mode 100644 index 00000000..1cfe7dfb --- /dev/null +++ b/Chalice/tests/examples/ProdConsChannel.output.txt @@ -0,0 +1,8 @@ +Verification of ProdConsChannel.chalice
+
+ 47.3: Method body is not allowed to leave any debt.
+ 61.3: Method body is not allowed to leave any debt.
+ 85.20: Location might not be readable.
+ 123.7: Assertion might not hold. The expression at 123.14 might not evaluate to true.
+
+Boogie program verifier finished with 19 verified, 4 errors
diff --git a/Chalice/examples/RockBand-automagic.chalice b/Chalice/tests/examples/RockBand-automagic.chalice index d231ae5a..d231ae5a 100644 --- a/Chalice/examples/RockBand-automagic.chalice +++ b/Chalice/tests/examples/RockBand-automagic.chalice diff --git a/Chalice/tests/examples/RockBand-automagic.output.txt b/Chalice/tests/examples/RockBand-automagic.output.txt new file mode 100644 index 00000000..d494e16a --- /dev/null +++ b/Chalice/tests/examples/RockBand-automagic.output.txt @@ -0,0 +1,11 @@ +Verification of RockBand-automagic.chalice
+
+ 19.27: Location might not be readable.
+ 27.3: The postcondition at 29.13 might not hold. Insufficient fraction at 29.13 for RockBand.Valid.
+ 41.10: Location might not be readable.
+ 50.5: Location might not be writable
+ 58.3: The postcondition at 60.13 might not hold. Insufficient fraction at 60.13 for Guitar.Valid.
+ 77.3: The postcondition at 79.13 might not hold. Insufficient fraction at 79.13 for Vocalist.Valid.
+ 96.3: The postcondition at 98.13 might not hold. Insufficient fraction at 98.13 for Organ.Valid.
+
+Boogie program verifier finished with 28 verified, 7 errors
diff --git a/Chalice/examples/RockBand.chalice b/Chalice/tests/examples/RockBand.chalice index 49b99a68..49b99a68 100644 --- a/Chalice/examples/RockBand.chalice +++ b/Chalice/tests/examples/RockBand.chalice diff --git a/Chalice/tests/examples/RockBand.output.txt b/Chalice/tests/examples/RockBand.output.txt new file mode 100644 index 00000000..3fb1b1c6 --- /dev/null +++ b/Chalice/tests/examples/RockBand.output.txt @@ -0,0 +1,10 @@ +Verification of RockBand.chalice
+
+ 27.3: The postcondition at 29.13 might not hold. Insufficient fraction at 29.13 for RockBand.Valid.
+ 41.10: Location might not be readable.
+ 50.5: Location might not be writable
+ 58.3: The postcondition at 60.13 might not hold. Insufficient fraction at 60.13 for Guitar.Valid.
+ 77.3: The postcondition at 79.13 might not hold. Insufficient fraction at 79.13 for Vocalist.Valid.
+ 96.3: The postcondition at 98.13 might not hold. Insufficient fraction at 98.13 for Organ.Valid.
+
+Boogie program verifier finished with 29 verified, 6 errors
diff --git a/Chalice/examples/Sieve.chalice b/Chalice/tests/examples/Sieve.chalice index a7ec9d10..d7223d04 100644 --- a/Chalice/examples/Sieve.chalice +++ b/Chalice/tests/examples/Sieve.chalice @@ -45,7 +45,7 @@ class Sieve { while (2 <= p)
invariant ch != null;
invariant 2 <= p ==> credit(ch, 1);
- invariant rd(ch.mu) && waitlevel << ch.mu;
+ invariant rd*(ch.mu) && waitlevel << ch.mu;
{
// print p--it's a prime!
var cp := new ChalicePrint; call cp.Int(p);
diff --git a/Chalice/tests/examples/Sieve.output.txt b/Chalice/tests/examples/Sieve.output.txt new file mode 100644 index 00000000..b8b74b59 --- /dev/null +++ b/Chalice/tests/examples/Sieve.output.txt @@ -0,0 +1,4 @@ +Verification of Sieve.chalice
+
+
+Boogie program verifier finished with 11 verified, 0 errors
diff --git a/Chalice/examples/cell-defaults.chalice b/Chalice/tests/examples/cell-defaults.chalice index 4781db97..4781db97 100644 --- a/Chalice/examples/cell-defaults.chalice +++ b/Chalice/tests/examples/cell-defaults.chalice diff --git a/Chalice/tests/examples/cell-defaults.output.txt b/Chalice/tests/examples/cell-defaults.output.txt new file mode 100644 index 00000000..ee7ae4e5 --- /dev/null +++ b/Chalice/tests/examples/cell-defaults.output.txt @@ -0,0 +1,17 @@ +Verification of cell-defaults.chalice
+
+ 6.3: The postcondition at 8.13 might not hold. Insufficient fraction at 8.13 for Cell.valid.
+ 17.5: Location might not be writable
+ 24.5: Location might not be writable
+ 31.5: The field x of the target of the free statement might not be writable.
+ 38.5: Location might not be readable.
+ 52.3: The postcondition at 55.13 might not hold. Insufficient fraction at 55.13 for Interval.valid.
+ 71.10: Location might not be readable.
+ 80.10: Location might not be readable.
+ 89.10: Location might not be readable.
+ 96.5: Location might not be readable.
+ 102.5: Location might not be readable.
+ 107.5: Location might not be readable.
+ 131.5: Assertion might not hold. Insufficient fraction at 131.12 for Cell.valid.
+
+Boogie program verifier finished with 19 verified, 13 errors
diff --git a/Chalice/examples/cell.chalice b/Chalice/tests/examples/cell.chalice index 1cf82950..1cf82950 100644 --- a/Chalice/examples/cell.chalice +++ b/Chalice/tests/examples/cell.chalice diff --git a/Chalice/tests/examples/cell.output.txt b/Chalice/tests/examples/cell.output.txt new file mode 100644 index 00000000..3ca21dd2 --- /dev/null +++ b/Chalice/tests/examples/cell.output.txt @@ -0,0 +1,5 @@ +Verification of cell.chalice
+
+ 142.5: Assertion might not hold. Insufficient fraction at 142.12 for Cell.valid.
+
+Boogie program verifier finished with 31 verified, 1 error
diff --git a/Chalice/examples/counter.chalice b/Chalice/tests/examples/counter.chalice index 828cf005..828cf005 100644 --- a/Chalice/examples/counter.chalice +++ b/Chalice/tests/examples/counter.chalice diff --git a/Chalice/tests/examples/counter.output.txt b/Chalice/tests/examples/counter.output.txt new file mode 100644 index 00000000..6fdd2d7c --- /dev/null +++ b/Chalice/tests/examples/counter.output.txt @@ -0,0 +1,10 @@ +Verification of counter.chalice
+
+ 69.5: Monitor invariant might hot hold. The expression at 4.27 might not evaluate to true.
+ 80.5: Assertion might not hold. The expression at 80.12 might not evaluate to true.
+ 119.5: The target of the release statement might not be locked by the current thread.
+ 128.7: The mu field of the target of the acquire statement might not be above waitlevel.
+ 136.7: The mu field of the target of the acquire statement might not be above waitlevel.
+ 145.5: The target of the release statement might not be locked by the current thread.
+
+Boogie program verifier finished with 24 verified, 6 errors
diff --git a/Chalice/examples/dining-philosophers.chalice b/Chalice/tests/examples/dining-philosophers.chalice index f4a7d1a6..f4a7d1a6 100644 --- a/Chalice/examples/dining-philosophers.chalice +++ b/Chalice/tests/examples/dining-philosophers.chalice diff --git a/Chalice/tests/examples/dining-philosophers.output.txt b/Chalice/tests/examples/dining-philosophers.output.txt new file mode 100644 index 00000000..2bf72597 --- /dev/null +++ b/Chalice/tests/examples/dining-philosophers.output.txt @@ -0,0 +1,4 @@ +Verification of dining-philosophers.chalice
+
+
+Boogie program verifier finished with 12 verified, 0 errors
diff --git a/Chalice/tests/examples/generate_reference.bat b/Chalice/tests/examples/generate_reference.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/examples/generate_reference.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/examples/generate_reference_all.bat b/Chalice/tests/examples/generate_reference_all.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/examples/generate_reference_all.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/examples/iterator.chalice b/Chalice/tests/examples/iterator.chalice index fd5d0352..fd5d0352 100644 --- a/Chalice/examples/iterator.chalice +++ b/Chalice/tests/examples/iterator.chalice diff --git a/Chalice/tests/examples/iterator.output.txt b/Chalice/tests/examples/iterator.output.txt new file mode 100644 index 00000000..a03f7c0c --- /dev/null +++ b/Chalice/tests/examples/iterator.output.txt @@ -0,0 +1,4 @@ +Verification of iterator.chalice
+
+
+Boogie program verifier finished with 22 verified, 0 errors
diff --git a/Chalice/examples/iterator2.chalice b/Chalice/tests/examples/iterator2.chalice index b0c8c6b9..4020ece3 100644 --- a/Chalice/examples/iterator2.chalice +++ b/Chalice/tests/examples/iterator2.chalice @@ -46,7 +46,7 @@ class Iterator module Collections { method init(l: List)
requires acc(list) && acc(index);
requires l!=null;
- requires rd(l.valid);
+ requires acc(l.valid,rd(l.valid));
ensures valid;
ensures getList()==l;
{
@@ -68,7 +68,7 @@ class Iterator module Collections { method dispose()
requires valid;
- ensures rd(old(getList()).valid);
+ ensures acc(old(getList()).valid,rd(old(getList()).valid));
{
unfold valid;
}
diff --git a/Chalice/tests/examples/iterator2.output.txt b/Chalice/tests/examples/iterator2.output.txt new file mode 100644 index 00000000..512a2e26 --- /dev/null +++ b/Chalice/tests/examples/iterator2.output.txt @@ -0,0 +1,4 @@ +Verification of iterator2.chalice
+
+
+Boogie program verifier finished with 21 verified, 0 errors
diff --git a/Chalice/examples/linkedlist.chalice b/Chalice/tests/examples/linkedlist.chalice index acde86ab..acde86ab 100644 --- a/Chalice/examples/linkedlist.chalice +++ b/Chalice/tests/examples/linkedlist.chalice diff --git a/Chalice/tests/examples/linkedlist.output.txt b/Chalice/tests/examples/linkedlist.output.txt new file mode 100644 index 00000000..b164664d --- /dev/null +++ b/Chalice/tests/examples/linkedlist.output.txt @@ -0,0 +1,5 @@ +Verification of linkedlist.chalice
+
+ 49.39: Precondition at 47.14 might not hold. The expression at 47.31 might not evaluate to true.
+
+Boogie program verifier finished with 9 verified, 1 error
diff --git a/Chalice/examples/producer-consumer.chalice b/Chalice/tests/examples/producer-consumer.chalice index 25253bfb..25253bfb 100644 --- a/Chalice/examples/producer-consumer.chalice +++ b/Chalice/tests/examples/producer-consumer.chalice diff --git a/Chalice/tests/examples/producer-consumer.output.txt b/Chalice/tests/examples/producer-consumer.output.txt new file mode 100644 index 00000000..ebf7c738 --- /dev/null +++ b/Chalice/tests/examples/producer-consumer.output.txt @@ -0,0 +1,4 @@ +Verification of producer-consumer.chalice
+
+
+Boogie program verifier finished with 36 verified, 0 errors
diff --git a/Chalice/examples/prog0.chalice b/Chalice/tests/examples/prog0.chalice index fb835a24..fb835a24 100644 --- a/Chalice/examples/prog0.chalice +++ b/Chalice/tests/examples/prog0.chalice diff --git a/Chalice/examples/Answer b/Chalice/tests/examples/prog0.output.txt index 087415ba..7949fa88 100644 --- a/Chalice/examples/Answer +++ b/Chalice/tests/examples/prog0.output.txt @@ -1,36 +1,5 @@ -start
------- Running regression test cell.chalice
- 142.5: Assertion might not hold. Insufficient fraction at 142.12 for Cell.valid.
+Verification of prog0.chalice
-Boogie program verifier finished with 31 verified, 1 error
------- Running regression test counter.chalice
- 69.5: Monitor invariant might hot hold. The expression at 4.27 might not evaluate to true.
- 80.5: Assertion might not hold. The expression at 80.12 might not evaluate to true.
- 119.5: The target of the release statement might not be locked by the current thread.
- 128.7: The mu field of the target of the acquire statement might not be above waitlevel.
- 136.7: The mu field of the target of the acquire statement might not be above waitlevel.
- 145.5: The target of the release statement might not be locked by the current thread.
-
-Boogie program verifier finished with 24 verified, 6 errors
------- Running regression test dining-philosophers.chalice
-
-Boogie program verifier finished with 12 verified, 0 errors
------- Running regression test ForkJoin.chalice
-
-Boogie program verifier finished with 18 verified, 0 errors
------- Running regression test HandOverHand.chalice
-
-Boogie program verifier finished with 10 verified, 0 errors
------- Running regression test iterator.chalice
-
-Boogie program verifier finished with 22 verified, 0 errors
------- Running regression test iterator2.chalice
-
-Boogie program verifier finished with 21 verified, 0 errors
------- Running regression test producer-consumer.chalice
-
-Boogie program verifier finished with 36 verified, 0 errors
------- Running regression test prog0.chalice
The program did not typecheck.
3.17: undeclared member a in class C
3.37: undeclared member a in class C
@@ -175,84 +144,3 @@ The program did not typecheck. 104.16: duplicate actual out-parameter: a
105.16: undeclared member b in class ImplicitC
105.16: undeclared member k in class int
------- Running regression test prog1.chalice
- 9.10: Location might not be readable.
- 25.5: Location might not be writable
- 33.14: Location might not be readable.
- 42.5: Monitor invariant might hot hold. The expression at 5.23 might not evaluate to true.
- 60.5: Location might not be writable
- 76.5: The target of the unshare statement might not be shared.
- 84.5: The target of the unshare statement might not be shared.
-
-Boogie program verifier finished with 16 verified, 7 errors
------- Running regression test prog2.chalice
- 24.5: Assertion might not hold. The expression at 24.12 might not evaluate to true.
- 31.13: Location might not be readable.
- 73.5: Const variable can be assigned to only once.
- 78.5: Assertion might not hold. The expression at 78.12 might not evaluate to true.
-
-Boogie program verifier finished with 24 verified, 4 errors
------- Running regression test prog3.chalice
- 76.3: The postcondition at 77.13 might not hold. The expression at 77.13 might not evaluate to true.
- 76.3: Method might lock/unlock more than allowed.
- 191.5: The precondition at 182.14 might not hold. Insufficient epsilons at 182.14 for ReadSharing.x.
- 202.3: The postcondition at 204.13 might not hold. Insufficient epsilons at 204.13 for ReadSharing.x.
-
-Boogie program verifier finished with 51 verified, 4 errors
------- Running regression test prog4.chalice
- 5.5: Assertion might not hold. The expression at 5.12 might not evaluate to true.
- 17.7: The target of the release statement might not be locked by the current thread.
- 17.7: Release might fail because the current thread might hold the read lock.
- 30.7: The target of the release statement might not be locked by the current thread.
- 30.7: Release might fail because the current thread might hold the read lock.
- 34.5: The target of the release statement might not be locked by the current thread.
- 34.5: Release might fail because the current thread might hold the read lock.
-
-Boogie program verifier finished with 6 verified, 7 errors
------- Running regression test ImplicitLocals.chalice
-
-Boogie program verifier finished with 8 verified, 0 errors
------- Running regression test RockBand.chalice
- 27.3: The postcondition at 29.13 might not hold. Insufficient fraction at 29.13 for RockBand.Valid.
- 41.10: Location might not be readable.
- 50.5: Location might not be writable
- 58.3: The postcondition at 60.13 might not hold. Insufficient fraction at 60.13 for Guitar.Valid.
- 77.3: The postcondition at 79.13 might not hold. Insufficient fraction at 79.13 for Vocalist.Valid.
- 96.3: The postcondition at 98.13 might not hold. Insufficient fraction at 98.13 for Organ.Valid.
-
-Boogie program verifier finished with 29 verified, 6 errors
------- Running regression test swap.chalice
-
-Boogie program verifier finished with 5 verified, 0 errors
------- Running regression test OwickiGries.chalice
-
-Boogie program verifier finished with 5 verified, 0 errors
------- Running regression test ProdConsChannel.chalice
- 47.3: Method body is not allowed to leave any debt.
- 61.3: Method body is not allowed to leave any debt.
- 85.20: Location might not be readable.
- 123.7: Assertion might not hold. The expression at 123.14 might not evaluate to true.
-
-Boogie program verifier finished with 19 verified, 4 errors
------- Running regression test LoopLockChange.chalice
- 10.5: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop.
- 35.5: The loop might lock/unlock more than the lockchange clause allows.
- 65.5: The loop might lock/unlock more than the lockchange clause allows.
-
-Boogie program verifier finished with 14 verified, 3 errors
------- Running regression test PetersonsAlgorithm.chalice
-
-Boogie program verifier finished with 7 verified, 0 errors
------- Running regression test quantifiers.chalice
- 57.29: The heap of the callee might not be strictly smaller than the heap of the caller.
-
-Boogie program verifier finished with 11 verified, 1 error
------- Running regression test cell-defaults.chalice
- 96.5: The heap of the callee might not be strictly smaller than the heap of the caller.
- 102.5: The heap of the callee might not be strictly smaller than the heap of the caller.
- 131.5: Assertion might not hold. Automatic fold might fail. Insufficient fraction at 42.5 for Cell.x.
-
-Boogie program verifier finished with 29 verified, 3 errors
------- Running regression test RockBand-automagic.chalice
-
-Boogie program verifier finished with 35 verified, 0 errors
diff --git a/Chalice/examples/prog1.chalice b/Chalice/tests/examples/prog1.chalice index 133de36d..133de36d 100644 --- a/Chalice/examples/prog1.chalice +++ b/Chalice/tests/examples/prog1.chalice diff --git a/Chalice/tests/examples/prog1.output.txt b/Chalice/tests/examples/prog1.output.txt new file mode 100644 index 00000000..eb552ac2 --- /dev/null +++ b/Chalice/tests/examples/prog1.output.txt @@ -0,0 +1,11 @@ +Verification of prog1.chalice
+
+ 9.10: Location might not be readable.
+ 25.5: Location might not be writable
+ 33.14: Location might not be readable.
+ 42.5: Monitor invariant might hot hold. The expression at 5.23 might not evaluate to true.
+ 60.5: Location might not be writable
+ 76.5: The target of the unshare statement might not be shared.
+ 84.5: The target of the unshare statement might not be shared.
+
+Boogie program verifier finished with 16 verified, 7 errors
diff --git a/Chalice/examples/prog2.chalice b/Chalice/tests/examples/prog2.chalice index 55fe8ff5..55fe8ff5 100644 --- a/Chalice/examples/prog2.chalice +++ b/Chalice/tests/examples/prog2.chalice diff --git a/Chalice/tests/examples/prog2.output.txt b/Chalice/tests/examples/prog2.output.txt new file mode 100644 index 00000000..1581039d --- /dev/null +++ b/Chalice/tests/examples/prog2.output.txt @@ -0,0 +1,8 @@ +Verification of prog2.chalice
+
+ 24.5: Assertion might not hold. The expression at 24.12 might not evaluate to true.
+ 31.13: Location might not be readable.
+ 73.5: Const variable can be assigned to only once.
+ 78.5: Assertion might not hold. The expression at 78.12 might not evaluate to true.
+
+Boogie program verifier finished with 24 verified, 4 errors
diff --git a/Chalice/examples/prog3.chalice b/Chalice/tests/examples/prog3.chalice index f3b8210b..de5dfad7 100644 --- a/Chalice/examples/prog3.chalice +++ b/Chalice/tests/examples/prog3.chalice @@ -179,13 +179,13 @@ class ReadSharing { var x: int
method Consume()
- requires rd(x)
+ requires rd(x,1)
{
// skip
}
method Divulge() // bad
- requires rd(x)
+ requires rd(x,1)
{
call Consume()
call Consume() // error: cannot share twice (1773)
@@ -209,8 +209,8 @@ class ReadSharing { } // error: does not live up to postcondition (2015)
method Shares() // good
- requires rd(x,*)
- ensures rd(x,*)
+ requires rd*(x)
+ ensures rd*(x)
{
call Consume()
call Consume()
@@ -218,27 +218,26 @@ class ReadSharing { }
method TeamPlayer(N: int) // good
- requires 0<=N && rd(x,N)
- ensures rd(x,0)
+ requires 0<N && rd(x,N)
{
var n := N
- while (0 < n)
- invariant 0<=n && rd(x,n)
+ while (1 < n)
+ invariant 0<n && rd(x,n)
{
n := n - 1
}
}
method Unselfish(N: int) // good
- requires rd(x,*)
- ensures rd(x,*)
+ requires rd*(x)
+ ensures rd*(x)
{
var n := N
if (N == 173) {
call Unselfish(200)
}
while (0 < n)
- invariant rd(x,*)
+ invariant rd*(x)
{
call Consume()
n := n - 1
diff --git a/Chalice/tests/examples/prog3.output.txt b/Chalice/tests/examples/prog3.output.txt new file mode 100644 index 00000000..7537f222 --- /dev/null +++ b/Chalice/tests/examples/prog3.output.txt @@ -0,0 +1,8 @@ +Verification of prog3.chalice
+
+ 76.3: The postcondition at 77.13 might not hold. The expression at 77.13 might not evaluate to true.
+ 76.3: Method might lock/unlock more than allowed.
+ 191.5: The precondition at 182.14 might not hold. Insufficient epsilons at 182.14 for ReadSharing.x.
+ 202.3: The postcondition at 204.13 might not hold. Insufficient epsilons at 204.13 for ReadSharing.x.
+
+Boogie program verifier finished with 51 verified, 4 errors
diff --git a/Chalice/examples/prog4.chalice b/Chalice/tests/examples/prog4.chalice index 3c655c71..3c655c71 100644 --- a/Chalice/examples/prog4.chalice +++ b/Chalice/tests/examples/prog4.chalice diff --git a/Chalice/tests/examples/prog4.output.txt b/Chalice/tests/examples/prog4.output.txt new file mode 100644 index 00000000..950c2277 --- /dev/null +++ b/Chalice/tests/examples/prog4.output.txt @@ -0,0 +1,11 @@ +Verification of prog4.chalice
+
+ 5.5: Assertion might not hold. The expression at 5.12 might not evaluate to true.
+ 17.7: The target of the release statement might not be locked by the current thread.
+ 17.7: Release might fail because the current thread might hold the read lock.
+ 30.7: The target of the release statement might not be locked by the current thread.
+ 30.7: Release might fail because the current thread might hold the read lock.
+ 34.5: The target of the release statement might not be locked by the current thread.
+ 34.5: Release might fail because the current thread might hold the read lock.
+
+Boogie program verifier finished with 6 verified, 7 errors
diff --git a/Chalice/examples/quantifiers.chalice b/Chalice/tests/examples/quantifiers.chalice index 7377ca3f..7377ca3f 100644 --- a/Chalice/examples/quantifiers.chalice +++ b/Chalice/tests/examples/quantifiers.chalice diff --git a/Chalice/tests/examples/quantifiers.output.txt b/Chalice/tests/examples/quantifiers.output.txt new file mode 100644 index 00000000..20b0af7b --- /dev/null +++ b/Chalice/tests/examples/quantifiers.output.txt @@ -0,0 +1,5 @@ +Verification of quantifiers.chalice
+
+ 57.29: The heap of the callee might not be strictly smaller than the heap of the caller.
+
+Boogie program verifier finished with 11 verified, 1 error
diff --git a/Chalice/tests/examples/reg_test.bat b/Chalice/tests/examples/reg_test.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/examples/reg_test.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/examples/reg_test_all.bat b/Chalice/tests/examples/reg_test_all.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/examples/reg_test_all.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/examples/swap.chalice b/Chalice/tests/examples/swap.chalice index 46a6a71a..46a6a71a 100644 --- a/Chalice/examples/swap.chalice +++ b/Chalice/tests/examples/swap.chalice diff --git a/Chalice/tests/examples/swap.output.txt b/Chalice/tests/examples/swap.output.txt new file mode 100644 index 00000000..29df3021 --- /dev/null +++ b/Chalice/tests/examples/swap.output.txt @@ -0,0 +1,4 @@ +Verification of swap.chalice
+
+
+Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Chalice/tests/examples/test.bat b/Chalice/tests/examples/test.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/examples/test.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/permission-model/basic.chalice b/Chalice/tests/permission-model/basic.chalice new file mode 100644 index 00000000..53443a49 --- /dev/null +++ b/Chalice/tests/permission-model/basic.chalice @@ -0,0 +1,232 @@ +class Cell {
+ var x: int;
+
+ // dispose a read permission to x
+ method dispose_rd()
+ requires rd(x);
+ ensures true;
+ {
+ }
+
+ // return read permission
+ method void()
+ requires rd(x);
+ ensures rd(x);
+ {
+ }
+
+ // multiple calls to method that destroys rd(x)
+ method a1()
+ requires rd(x);
+ ensures true;
+ {
+ call dispose_rd();
+ call dispose_rd();
+ }
+
+ // call to method that destroys rd(x) really removes permission
+ method a2()
+ requires rd(x);
+ ensures rd(x);
+ {
+ call dispose_rd();
+ // ERROR: should fail to verify postcondition
+ }
+
+ // forking and method calls of dispose_rd
+ method a3()
+ requires rd(x);
+ ensures true;
+ {
+ fork dispose_rd();
+ call dispose_rd();
+ fork dispose_rd();
+ call dispose_rd();
+ }
+
+ // forking and method calls of dispose_rd
+ method a4()
+ requires rd(x);
+ ensures rd(x);
+ {
+ fork dispose_rd();
+ // ERROR: should fail to verify postcondition
+ }
+
+ // forking and method calls of dispose_rd
+ method a5()
+ requires rd(x);
+ ensures rd(x,1);
+ {
+ fork dispose_rd();
+ // OK: giving away an epsilon permission however should work
+ }
+
+ // forking and method calls of dispose_rd
+ method a6()
+ requires rd(x);
+ ensures rd*(x);
+ {
+ fork dispose_rd();
+ // OK: giving away a 'undefined' read permission however should work
+ }
+
+ // multiple forks of dispose_rd
+ method a7()
+ requires rd(x);
+ ensures true;
+ {
+ fork dispose_rd();
+ fork dispose_rd();
+ fork dispose_rd();
+ fork dispose_rd();
+ fork dispose_rd();
+ fork dispose_rd();
+ }
+
+ // joining to regain permission
+ method a8(a: int)
+ requires rd(x);
+ ensures rd(x)
+ {
+ fork tk := void();
+ join tk;
+ }
+
+ // joining to regain permission
+ method a9(a: int)
+ requires rd(x);
+ ensures rd(x)
+ {
+ fork tk := dispose_rd();
+ join tk;
+ // ERROR: should fail to verify postcondition
+ }
+
+ // joining to regain permission
+ method a10(a: int)
+ requires rd(x);
+ ensures a == 3 ==> rd(x)
+ {
+ fork tk := void();
+ if (3 == a) {
+ join tk;
+ }
+ }
+
+ // finite loop of method calls, preserving rd(x)
+ method a11()
+ requires rd(x);
+ ensures rd(x);
+ {
+ var i: int;
+ i := 0;
+ while (i < 1000)
+ invariant rd(x);
+ {
+ call void();
+ i := i+1;
+ }
+ }
+
+ // forking dispose_rd in a loop (using rd(x,*) to denote unknown read permission)
+ method a12(a: int)
+ requires rd(x);
+ ensures rd*(x);
+ {
+ var i: int;
+ i := 0;
+ while (i < a)
+ invariant rd*(x);
+ {
+ fork dispose_rd();
+ i := i+1;
+ }
+ }
+
+ // forking dispose_rd in a loop (using rd(x,*) to denote unknown read permission)
+ method a13(a: int)
+ requires rd(x);
+ ensures rd(x);
+ {
+ var i: int;
+ i := 0;
+ while (i < a)
+ invariant rd*(x);
+ {
+ fork dispose_rd();
+ i := i+1;
+ }
+ // ERROR: should fail to verify postcondition
+ }
+
+ // calling dispose_rd in a loop (using rd(x,*) to denote unknown read permission)
+ method a14()
+ requires rd(x);
+ ensures true;
+ {
+ call dispose_rd();
+
+ var i: int;
+ i := 0;
+ while (i < 1000)
+ invariant rd*(x);
+ {
+ call dispose_rd();
+ i := i+1;
+ }
+ }
+
+ // return unknown permission
+ method a15()
+ requires rd(x);
+ ensures rd*(x);
+ {
+ call dispose_rd();
+ }
+
+ // rd in loop invariant
+ method a16()
+ requires rd(x);
+ ensures rd*(x);
+ {
+ call dispose_rd();
+
+ var i: int;
+ i := 0;
+ while (i < 1000)
+ invariant acc(x,rd);
+ {
+ call void();
+ i := i+1;
+ }
+ }
+
+ // rd in method contracts
+ method a17()
+ requires acc(x,rd);
+ {
+ call dispose_rd();
+ call a17();
+ }
+
+ // multiple rd in method contracts
+ method a18()
+ requires rd(x);
+ ensures rd(x)
+ {
+ call a18a()
+ call a18b()
+ }
+ method a18a()
+ requires acc(x,2*rd);
+ ensures acc(x,rd+rd);
+ {
+ }
+ method a18b()
+ requires acc(x,rd+rd);
+ ensures acc(x,rd*2);
+ {
+ }
+
+}
diff --git a/Chalice/tests/permission-model/basic.output.txt b/Chalice/tests/permission-model/basic.output.txt new file mode 100644 index 00000000..510ae7f5 --- /dev/null +++ b/Chalice/tests/permission-model/basic.output.txt @@ -0,0 +1,8 @@ +Verification of basic.chalice
+
+ 28.3: The postcondition at 30.13 might not hold. Insufficient fraction at 30.13 for Cell.x.
+ 48.3: The postcondition at 50.13 might not hold. Insufficient fraction at 50.13 for Cell.x.
+ 97.3: The postcondition at 99.13 might not hold. Insufficient fraction at 99.13 for Cell.x.
+ 148.3: The postcondition at 150.13 might not hold. Insufficient fraction at 150.13 for Cell.x.
+
+Boogie program verifier finished with 41 verified, 4 errors
diff --git a/Chalice/tests/permission-model/channels.chalice b/Chalice/tests/permission-model/channels.chalice new file mode 100644 index 00000000..6a4961cd --- /dev/null +++ b/Chalice/tests/permission-model/channels.chalice @@ -0,0 +1,45 @@ +class C {
+ var f: int;
+
+ method t1(ch: C1)
+ requires ch != null && rd(f);
+ ensures true;
+ {
+ send ch(this) // ERROR
+ }
+
+ method t2(ch: C1)
+ requires ch != null && acc(f);
+ ensures true;
+ {
+ send ch(this)
+ }
+
+ method t3(ch: C2)
+ requires ch != null && rd(f);
+ ensures rd(f);
+ {
+ send ch(this)
+ // ERROR: should fail to verify postcondition
+ }
+
+ method t4(ch: C1, a: C) returns (b: C)
+ requires ch != null && credit(ch, 1) && rd(ch.mu) && waitlevel << ch;
+ ensures rd*(b.f);
+ {
+ receive b := ch
+ }
+
+ method t5(ch: C1)
+ requires ch != null && acc(f,1);
+ ensures true;
+ {
+ send ch(this)
+ send ch(this)
+ send ch(this)
+ }
+
+}
+
+channel C1(x: C) where rd(x.f);
+channel C2(x: C) where rd*(x.f);
diff --git a/Chalice/tests/permission-model/channels.output.txt b/Chalice/tests/permission-model/channels.output.txt new file mode 100644 index 00000000..11543925 --- /dev/null +++ b/Chalice/tests/permission-model/channels.output.txt @@ -0,0 +1,6 @@ +Verification of channels.chalice
+
+ 8.5: The where clause at 44.24 might not hold. Insufficient fraction at 44.24 for C.f.
+ 18.3: The postcondition at 20.13 might not hold. Insufficient fraction at 20.13 for C.f.
+
+Boogie program verifier finished with 11 verified, 2 errors
diff --git a/Chalice/tests/permission-model/generate_reference.bat b/Chalice/tests/permission-model/generate_reference.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/permission-model/generate_reference.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/permission-model/generate_reference_all.bat b/Chalice/tests/permission-model/generate_reference_all.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/permission-model/generate_reference_all.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/permission-model/locks.chalice b/Chalice/tests/permission-model/locks.chalice new file mode 100644 index 00000000..5107fd38 --- /dev/null +++ b/Chalice/tests/permission-model/locks.chalice @@ -0,0 +1,146 @@ +class Cell {
+ var x: int;
+
+ // use starred read permission
+ invariant rd*(x);
+
+ method a1(c: Cell)
+ requires c != null && rd(c.mu) && waitlevel << c;
+ {
+ acquire c;
+ assert(rd*(c.x));
+
+ release c;
+ assert(rd*(c.x));
+ }
+
+ method a2(c: Cell)
+ requires c != null && rd(c.mu) && waitlevel << c;
+ {
+ acquire c;
+ assert(rd(c.x)); // ERROR: should fail
+
+ release c;
+ assert(rd(c.x)); // ERROR: should fail
+ }
+
+ method a3()
+ {
+ var c: Cell := new Cell;
+
+ share c;
+ assert(rd*(c.x));
+
+ acquire c;
+ unshare c;
+ assert(rd*(c.x));
+ }
+
+ method a4()
+ {
+ var c: Cell := new Cell;
+
+ share c;
+ assert(rd(c.x)); // ERROR: should fail
+ }
+
+ method a5()
+ {
+ var c: Cell := new Cell;
+
+ share c;
+ acquire c;
+ unshare c;
+ assert(rd(c.x)); // ERROR: should fail
+ }
+
+}
+
+
+class Cell2 {
+ var x: int;
+
+ // use normal fractional permission
+ invariant rd(x);
+
+ method a1(c: Cell2)
+ requires c != null && rd(c.mu) && waitlevel << c;
+ {
+ acquire c;
+ assert(rd*(c.x));
+
+ release c;
+ assert(rd*(c.x)); // ERROR: we gave away all permission
+ }
+
+ method a2(c: Cell2)
+ requires c != null && rd(c.mu) && waitlevel << c;
+ {
+ acquire c;
+ assert(rd(c.x)); // ERROR: should fail
+
+ release c;
+ assert(rd(c.x)); // ERROR: should fail
+ }
+
+ method a3()
+ {
+ var c: Cell2 := new Cell2;
+
+ share c;
+ assert(rd*(c.x));
+
+ call void(c);
+ assert(rd*(c.x));
+
+ call dispose(c);
+ assert(rd*(c.x));
+
+ acquire c;
+ unshare c;
+ assert(rd*(c.x));
+
+ assert(acc(c.x)); // ERROR: should fail
+ }
+
+ method a4(c: Cell2)
+ requires c != null && acc(c.mu) && holds(c);
+ requires rd(c.x);
+ lockchange c
+ {
+ release c; // ERROR: should fail, we don't have enough permission
+ }
+
+ method a5()
+ {
+ var c: Cell2 := new Cell2;
+
+ share c;
+ acquire c;
+ assert(acc(c.x));
+
+ unshare c;
+ assert(acc(c.x));
+ }
+
+ method a6(c: Cell2)
+ requires acc(c.x,rd(c)) && acc(c.mu) && c.mu == lockbottom
+ {
+ var n: int;
+
+ share c;
+ rd acquire c;
+ n := c.x
+ rd release c;
+
+ n := c.x // ERROR: no read access possible
+
+ acquire c;
+ unshare c;
+ }
+
+ method void(c: Cell2) requires rd(c.x); ensures rd(c.x); {}
+
+ method dispose(c: Cell2) requires rd(c.x); {}
+
+}
diff --git a/Chalice/tests/permission-model/locks.output.txt b/Chalice/tests/permission-model/locks.output.txt new file mode 100644 index 00000000..c1167c3b --- /dev/null +++ b/Chalice/tests/permission-model/locks.output.txt @@ -0,0 +1,14 @@ +Verification of locks.chalice
+
+ 21.5: Assertion might not hold. Insufficient fraction at 21.12 for Cell.x.
+ 24.5: Assertion might not hold. Insufficient fraction at 24.12 for Cell.x.
+ 44.5: Assertion might not hold. Insufficient fraction at 44.12 for Cell.x.
+ 54.5: Assertion might not hold. Insufficient fraction at 54.12 for Cell.x.
+ 73.5: Assertion might not hold. Insufficient fraction at 73.12 for Cell2.x.
+ 80.5: Assertion might not hold. Insufficient fraction at 80.12 for Cell2.x.
+ 83.5: Assertion might not hold. Insufficient fraction at 83.12 for Cell2.x.
+ 103.5: Assertion might not hold. Insufficient fraction at 103.12 for Cell2.x.
+ 111.5: Monitor invariant might hot hold. Insufficient fraction at 64.13 for Cell2.x.
+ 136.10: Location might not be readable.
+
+Boogie program verifier finished with 20 verified, 10 errors
diff --git a/Chalice/tests/permission-model/peculiar.chalice b/Chalice/tests/permission-model/peculiar.chalice new file mode 100644 index 00000000..31c4d259 --- /dev/null +++ b/Chalice/tests/permission-model/peculiar.chalice @@ -0,0 +1,55 @@ +class Cell {
+ var x: int;
+
+ invariant rd(x);
+
+ method t1()
+ requires acc(x);
+ ensures rd(x) && rd(x);
+ {
+ }
+
+ method t2()
+ requires acc(x,1);
+ ensures rd(x);
+ {
+ call void();
+ }
+
+ method t3()
+ requires rd(x);
+ {
+ call t3helper();
+ }
+
+ method t3helper()
+ requires rd(x) && rd(x);
+ ensures rd(x) && rd(x);
+ {}
+
+ method t4()
+ requires rd(x);
+ {
+ call dispose();
+ call void(); // call succeeds, even though the precondition is also rd(x), and the next assertion fails
+ assert(rd(x)); // ERROR: fails, as this check is done exactly (as it would in a postcondition)
+ }
+
+ method t5(n: int)
+ requires acc(x);
+ {
+ var i: int := 0;
+ call req99();
+ while (i < n)
+ invariant rd*(x);
+ {
+ call dispose();
+ i := i+1
+ }
+ }
+
+ method dispose() requires rd(x); {}
+ method void() requires rd(x); ensures rd(x); {}
+ method req99() requires acc(x,99); {}
+
+}
diff --git a/Chalice/tests/permission-model/peculiar.output.txt b/Chalice/tests/permission-model/peculiar.output.txt new file mode 100644 index 00000000..fd3c0a76 --- /dev/null +++ b/Chalice/tests/permission-model/peculiar.output.txt @@ -0,0 +1,5 @@ +Verification of peculiar.chalice
+
+ 35.5: Assertion might not hold. Insufficient fraction at 35.12 for Cell.x.
+
+Boogie program verifier finished with 18 verified, 1 error
diff --git a/Chalice/tests/permission-model/permarith_parser.chalice b/Chalice/tests/permission-model/permarith_parser.chalice new file mode 100644 index 00000000..5b011d79 --- /dev/null +++ b/Chalice/tests/permission-model/permarith_parser.chalice @@ -0,0 +1,37 @@ +class Cell {
+ var x: int;
+ var y: Cell;
+
+ method a1()
+ requires acc(x,y); // ERROR: amount is not integer
+ {
+ }
+
+ method a2()
+ requires acc(x,n); // ERROR: unknown variable
+ {
+ }
+
+ method a3()
+ requires acc(x,rd(rd(1))); // ERROR: invalid permission expression
+ {
+ }
+
+ method a4()
+ requires acc(x,rd*(y)); // ERROR: invalid permission expression
+ {
+ }
+
+ method a5()
+ requires acc(x,rd(this.mu)); // ERROR: invalid type inside rd
+ requires acc(x,rd(null)); // ERROR: invalid type inside rd
+ requires acc(x,rd(true)); // ERROR: invalid type inside rd
+ {
+ }
+
+ method a6()
+ requires acc(x,rd(x)*rd(x)); // ERROR: permission multiplication not allowed
+ {
+ }
+
+}
diff --git a/Chalice/tests/permission-model/permarith_parser.output.txt b/Chalice/tests/permission-model/permarith_parser.output.txt new file mode 100644 index 00000000..f124b714 --- /dev/null +++ b/Chalice/tests/permission-model/permarith_parser.output.txt @@ -0,0 +1,13 @@ +Verification of permarith_parser.chalice
+
+The program did not typecheck.
+6.14: fraction in permission must be of type integer
+11.20: undeclared member n in class Cell
+16.26: permission not expected here.
+16.26: type $Permission is not supported inside a rd expression.
+21.20: rd expression is allowed only in positive predicate contexts
+21.14: expression of type bool invalid in permission
+26.20: type $Mu of variable mu is not supported inside a rd expression.
+27.23: type null is not supported inside a rd expression.
+28.23: type bool is not supported inside a rd expression.
+33.14: multiplication of permission amounts not supported
diff --git a/Chalice/tests/permission-model/permission_arithmetic.chalice b/Chalice/tests/permission-model/permission_arithmetic.chalice new file mode 100644 index 00000000..94cf30a3 --- /dev/null +++ b/Chalice/tests/permission-model/permission_arithmetic.chalice @@ -0,0 +1,193 @@ +class Cell {
+ var x: int;
+ var i: int;
+ var y: Cell;
+
+ invariant rd(x);
+
+ predicate valid { rd(x) }
+
+ method a1(n: int) // test various arithmetic operations on permissions
+ requires acc(x,1+1) && acc(x,1) && acc(x,3) && acc(x,1-rd(5-7)+rd(3)) && rd(x) && rd(this.y);
+ ensures acc(x,100-97);
+ {
+ }
+
+ method a2(n: int)
+ requires acc(x,1-rd(1)-2);
+ {
+ assert false; // this should verify, as the precondition contains an invalid permission
+ }
+
+ method a3(n: int)
+ {
+ assert acc(x,1-rd(1)-2); // ERROR: invalid (negative) permission
+ }
+
+ method a4(n: int)
+ requires acc(x,rd(n));
+ {
+ }
+
+ method a5(n: int)
+ requires acc(x,rd(n)-rd(2));
+ {
+ }
+
+ method a6()
+ requires acc(x);
+ {
+ call a5(1); // ERROR: n=1 makes the permission in the precondition negative
+ }
+
+ method a7(c: Cell)
+ requires acc(c.x,100-rd(c));
+ requires c != null && acc(c.mu) && waitlevel << c;
+ ensures acc(c.x);
+ {
+ acquire(c);
+ unshare(c);
+ }
+
+ method a8()
+ requires acc(x,100-rd(valid)) && valid;
+ ensures acc(x);
+ {
+ unfold valid;
+ }
+
+ method a9()
+ requires acc(x,rd(valid));
+ ensures valid;
+ {
+ fold valid;
+ }
+
+ method a10()
+ requires valid;
+ ensures acc(x,rd(valid));
+ {
+ unfold valid;
+ }
+
+ method a11() // ERROR: postcondition does not hold (not enough permission)
+ requires valid;
+ ensures acc(x);
+ {
+ unfold valid;
+ }
+
+ method a12()
+ requires rd(this.i) && this.i > 0 && acc(x,rd(this.i));
+ ensures rd(this.i) && this.i > 0 && acc(x,rd(i));
+ {
+ }
+
+ method a13(i: int) // ERROR: postcondition does not hold
+ requires rd(this.i) && this.i > 0 && i > 0 && acc(x,rd(this.i));
+ ensures i > 0 && acc(x,rd(i));
+ {
+ }
+
+ method a14()
+ requires acc(y) && this.y == this; // test aliasing
+ requires acc(x,100-rd(y));
+ requires y != null && acc(this.mu) && waitlevel << this;
+ ensures acc(x);
+ lockchange this;
+ {
+ acquire this;
+ }
+
+ method a15()
+ requires acc(x,rd(this.i)); // ERROR: this.i is not readable
+ ensures acc(x,rd(this.i));
+ {
+ }
+
+ method a16()
+ requires acc(x,rd(this.y)); // ERROR: this.y is not readable
+ ensures acc(x,rd(this.y));
+ {
+ }
+
+ method a17(tk: token<Cell.void>)
+ requires acc(x,100-rd(tk)) && acc(tk.joinable) && tk.joinable;
+ requires eval(tk.fork this.void(),true);
+ ensures acc(x);
+ {
+ join tk;
+ }
+
+ method a18()
+ requires acc(x,rd+rd-rd+10*rd-rd*(5+5))
+ ensures rd(x)
+ {
+ call void();
+ }
+
+ method a19()
+ requires acc(x)
+ requires acc(this.mu) && lockbottom == this.mu
+ ensures acc(x)
+ lockchange this;
+ {
+ share this;
+ acquire this;
+ unshare this;
+ }
+
+ method a20()
+ requires rd(x)
+ requires acc(this.mu) && lockbottom == this.mu
+ lockchange this;
+ {
+ share this; // ERROR: not enough permission
+ }
+
+ method a21()
+ requires acc(x,rd*2)
+ ensures rd(x) && rd(x)
+ {
+ assert acc(x,rd+rd)
+ assert acc(x,(1+1)*rd)
+ }
+
+ method a22()
+ requires acc(x,1*2*5)
+ ensures acc(x,10)
+ {
+ }
+
+ method a23(c: Cell) // ERROR: permission in postcondition not positive
+ requires acc(x,rd-rd(c))
+ ensures acc(x,rd(c)-rd)
+ {
+ }
+
+ method a24()
+ requires rd*(x)
+ requires rd*(x)
+ {
+ }
+
+ method a25() // ERROR: postcondition does not hold, possibly not enough permission
+ requires rd*(x)
+ ensures acc(x,rd)
+ {
+ }
+
+ // interaction of monitors and predicates
+ method a26()
+ requires acc(x,rd(this))
+ requires acc(mu) && lockbottom == this.mu
+ ensures valid
+ lockchange this
+ {
+ share this
+ acquire this
+ fold valid
+ }
+
+ method void() requires rd(x); ensures rd(x); {}
+}
diff --git a/Chalice/tests/permission-model/permission_arithmetic.output.txt b/Chalice/tests/permission-model/permission_arithmetic.output.txt new file mode 100644 index 00000000..f735cf85 --- /dev/null +++ b/Chalice/tests/permission-model/permission_arithmetic.output.txt @@ -0,0 +1,13 @@ +Verification of permission_arithmetic.chalice
+
+ 24.5: Assertion might not hold. The permission at 24.18 might not be positive.
+ 40.5: The precondition at 33.14 might not hold. The permission at 33.20 might not be positive.
+ 73.3: The postcondition at 75.13 might not hold. Insufficient fraction at 75.13 for Cell.x.
+ 86.3: The postcondition at 88.13 might not hold. Insufficient epsilons at 88.22 for Cell.x.
+ 103.20: Location might not be readable.
+ 109.20: Location might not be readable.
+ 145.5: Monitor invariant might not hold. Insufficient fraction at 6.13 for Cell.x.
+ 162.3: The postcondition at 164.13 might not hold. The permission at 164.19 might not be positive.
+ 174.3: The postcondition at 176.13 might not hold. Insufficient fraction at 176.13 for Cell.x.
+
+Boogie program verifier finished with 47 verified, 9 errors
diff --git a/Chalice/tests/permission-model/predicate_error1.chalice b/Chalice/tests/permission-model/predicate_error1.chalice new file mode 100644 index 00000000..0726e349 --- /dev/null +++ b/Chalice/tests/permission-model/predicate_error1.chalice @@ -0,0 +1,20 @@ +class Cell {
+ var x: int;
+
+ // --- some predicates ---
+
+ predicate write1 { acc(x) } // full permission in a predicate
+ predicate write2 { acc(x,10) } // 10%
+ predicate read1 { rd(x) } // fractional read permission
+ predicate read2 { rd*(x) } // starred fractional read permission
+ predicate read3 { rd(x,1) } // counting permission (1 epsilon)
+
+ // --- invalid permission scaling ---
+
+ method error()
+ requires rd(read3);
+ {
+ unfold rd(read3); // ERROR: scaling epsilons is not possible
+ }
+
+}
diff --git a/Chalice/tests/permission-model/predicate_error1.output.txt b/Chalice/tests/permission-model/predicate_error1.output.txt new file mode 100644 index 00000000..d7964c29 --- /dev/null +++ b/Chalice/tests/permission-model/predicate_error1.output.txt @@ -0,0 +1,3 @@ +Verification of predicate_error1.chalice
+
+Error: Not supported: 17.5: Scaling epsilon permissions with non-full permissions is not possible.
diff --git a/Chalice/tests/permission-model/predicate_error2.chalice b/Chalice/tests/permission-model/predicate_error2.chalice new file mode 100644 index 00000000..cc8d7d28 --- /dev/null +++ b/Chalice/tests/permission-model/predicate_error2.chalice @@ -0,0 +1,20 @@ +class Cell {
+ var x: int;
+
+ // --- some predicates ---
+
+ predicate write1 { acc(x) } // full permission in a predicate
+ predicate write2 { acc(x,10) } // 10%
+ predicate read1 { rd(x) } // fractional read permission
+ predicate read2 { rd*(x) } // starred fractional read permission
+ predicate read3 { rd(x,1) } // counting permission (1 epsilon)
+
+ // --- invalid permission scaling ---
+
+ method error()
+ requires rd(read1,1);
+ {
+ unfold rd(read1,1); // ERROR: scaling epsilons is not possible
+ }
+
+}
diff --git a/Chalice/tests/permission-model/predicate_error2.output.txt b/Chalice/tests/permission-model/predicate_error2.output.txt new file mode 100644 index 00000000..cc580b7b --- /dev/null +++ b/Chalice/tests/permission-model/predicate_error2.output.txt @@ -0,0 +1,3 @@ +Verification of predicate_error2.chalice
+
+Error: Not supported: 17.5: Scaling epsilon permissions with non-full permissions is not possible.
diff --git a/Chalice/tests/permission-model/predicate_error3.chalice b/Chalice/tests/permission-model/predicate_error3.chalice new file mode 100644 index 00000000..eb1d8777 --- /dev/null +++ b/Chalice/tests/permission-model/predicate_error3.chalice @@ -0,0 +1,20 @@ +class Cell {
+ var x: int;
+
+ // --- some predicates ---
+
+ predicate write1 { acc(x) } // full permission in a predicate
+ predicate write2 { acc(x,10) } // 10%
+ predicate read1 { rd(x) } // fractional read permission
+ predicate read2 { rd*(x) } // starred fractional read permission
+ predicate read3 { rd(x,1) } // counting permission (1 epsilon)
+
+ // --- invalid permission scaling ---
+
+ method error()
+ requires rd(read3,1);
+ {
+ unfold rd(read3,1); // ERROR: scaling epsilons is not possible
+ }
+
+}
diff --git a/Chalice/tests/permission-model/predicate_error3.output.txt b/Chalice/tests/permission-model/predicate_error3.output.txt new file mode 100644 index 00000000..3e325f1b --- /dev/null +++ b/Chalice/tests/permission-model/predicate_error3.output.txt @@ -0,0 +1,3 @@ +Verification of predicate_error3.chalice
+
+Error: Not supported: 17.5: Scaling epsilon permissions with non-full permissions is not possible.
diff --git a/Chalice/tests/permission-model/predicate_error4.chalice b/Chalice/tests/permission-model/predicate_error4.chalice new file mode 100644 index 00000000..0726e349 --- /dev/null +++ b/Chalice/tests/permission-model/predicate_error4.chalice @@ -0,0 +1,20 @@ +class Cell {
+ var x: int;
+
+ // --- some predicates ---
+
+ predicate write1 { acc(x) } // full permission in a predicate
+ predicate write2 { acc(x,10) } // 10%
+ predicate read1 { rd(x) } // fractional read permission
+ predicate read2 { rd*(x) } // starred fractional read permission
+ predicate read3 { rd(x,1) } // counting permission (1 epsilon)
+
+ // --- invalid permission scaling ---
+
+ method error()
+ requires rd(read3);
+ {
+ unfold rd(read3); // ERROR: scaling epsilons is not possible
+ }
+
+}
diff --git a/Chalice/tests/permission-model/predicate_error4.output.txt b/Chalice/tests/permission-model/predicate_error4.output.txt new file mode 100644 index 00000000..8cd03821 --- /dev/null +++ b/Chalice/tests/permission-model/predicate_error4.output.txt @@ -0,0 +1,3 @@ +Verification of predicate_error4.chalice
+
+Error: Not supported: 17.5: Scaling epsilon permissions with non-full permissions is not possible.
diff --git a/Chalice/tests/permission-model/predicates.chalice b/Chalice/tests/permission-model/predicates.chalice new file mode 100644 index 00000000..1f752fda --- /dev/null +++ b/Chalice/tests/permission-model/predicates.chalice @@ -0,0 +1,103 @@ +class Cell {
+ var x: int;
+
+ // --- some predicates ---
+
+ predicate write1 { acc(x) } // full permission in a predicate
+ predicate write2 { acc(x,10) } // 10%
+ predicate read1 { rd(x) } // fractional read permission
+ predicate read2 { rd*(x) } // starred fractional read permission
+ predicate read3 { rd(x,1) } // counting permission (1 epsilon)
+
+ // --- basic tests ---
+
+ method b1()
+ requires write1 && write2 && read1 && read2 && read3;
+ ensures write1 && write2 && read1 && read2 && read3;
+ {
+ }
+
+ method b2()
+ requires write1;
+ ensures read1;
+ {
+ unfold write1;
+ fold read1;
+ }
+
+ method b3()
+ requires read1;
+ ensures read3;
+ {
+ unfold read1;
+ fold read3;
+ fold read2;
+ fold read3;
+ fold read2;
+ fold write1; // ERROR: should fail
+ }
+
+ method b4()
+ requires read2;
+ ensures read2;
+ {
+ unfold read2;
+ call dispose();
+ fold read2;
+ }
+
+ method b5()
+ requires read1;
+ ensures read1;
+ {
+ unfold read1;
+ call dispose();
+ fold read1; // ERROR: should fail
+ }
+
+ method b6()
+ requires acc(x);
+ ensures acc(x);
+ {
+ fold read1;
+ unfold read1;
+ }
+
+ method b7() // ERROR: precondition does not hold
+ requires acc(x);
+ ensures acc(x);
+ {
+ fold read2;
+ unfold read2;
+ }
+
+ method b8()
+ requires acc(x);
+ ensures acc(x);
+ {
+ fold read3;
+ unfold read3;
+ }
+
+ method b9()
+ requires acc(x);
+ ensures acc(x);
+ {
+ fold write1;
+ unfold write1;
+ }
+
+ method b10()
+ requires acc(x);
+ ensures acc(x);
+ {
+ fold write2;
+ unfold write2;
+ }
+
+ // --- helper functions ---
+
+ method void() requires rd(x); ensures rd(x); {}
+ method dispose() requires rd(x); {}
+
+}
diff --git a/Chalice/tests/permission-model/predicates.output.txt b/Chalice/tests/permission-model/predicates.output.txt new file mode 100644 index 00000000..be87e044 --- /dev/null +++ b/Chalice/tests/permission-model/predicates.output.txt @@ -0,0 +1,7 @@ +Verification of predicates.chalice
+
+ 37.5: Fold might fail because the definition of Cell.write1 does not hold. Insufficient fraction at 6.22 for Cell.x.
+ 55.5: Fold might fail because the definition of Cell.read1 does not hold. Insufficient fraction at 8.21 for Cell.x.
+ 66.3: The postcondition at 68.13 might not hold. Insufficient fraction at 68.13 for Cell.x.
+
+Boogie program verifier finished with 27 verified, 3 errors
diff --git a/Chalice/tests/permission-model/reg_test.bat b/Chalice/tests/permission-model/reg_test.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/permission-model/reg_test.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/permission-model/reg_test_all.bat b/Chalice/tests/permission-model/reg_test_all.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/permission-model/reg_test_all.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/permission-model/scaling.chalice b/Chalice/tests/permission-model/scaling.chalice new file mode 100644 index 00000000..29930346 --- /dev/null +++ b/Chalice/tests/permission-model/scaling.chalice @@ -0,0 +1,89 @@ +/*
+
+Note: At the moment, there is a performance problem if permissions are scaled.
+If a predicate (such as read1 below) contains a read permission, and one takes
+read access to that predicate (as in method s1; rd(read1)), then this
+effectively means that the fractions corresponding to the two read permissions
+are multiplied. This introduces non-linear arithmetic in Boogie, which can be
+very hard and unpredicable for the theorem prover. For this reason, this test is
+taking a very long time to complete.
+
+-- Stefan Heule, June 2011
+
+*/
+
+class Cell {
+ var x: int;
+
+ // --- some predicates ---
+
+ predicate write1 { acc(x) } // full permission in a predicate
+ predicate write2 { acc(x,10) } // 10%
+ predicate read1 { rd(x) } // abstract read permission
+ predicate read2 { rd*(x) } // starred read permission
+ predicate read3 { rd(x,1) } // counting permission (1 epsilon)
+
+ // --- permission scaling ---
+
+ method s1()
+ requires rd(read1);
+ {
+ unfold rd(read1);
+ assert(rd*(x));
+ assert(rd(x)); // ERROR: should fail
+ }
+
+ method s2() // INCOMPLETNESS: postcondition should hold, but fails at the moment
+ requires rd(read1);
+ ensures rd(read1);
+ {
+ unfold rd(read1);
+ fold rd(read1);
+ }
+
+ method s3()
+ requires acc(x);
+ ensures rd(read1);
+ {
+ fold rd(read1);
+ assert(rd*(x));
+ assert(acc(x)); // ERROR: should fail
+ }
+
+ method s4() // ERROR: postcondition does not hold
+ requires acc(x);
+ ensures read1;
+ {
+ fold rd(read1);
+ }
+
+ method s5()
+ requires rd(read2);
+ {
+ unfold rd(read2);
+ assert(rd*(x));
+ assert(rd(x)); // ERROR: should fail
+ }
+
+ method s6()
+ requires acc(x);
+ ensures rd(read2);
+ {
+ fold rd(read2);
+ assert(rd*(x));
+ assert(acc(x)); // ERROR: should fail
+ }
+
+ method s7() // ERROR: postcondition does not hold
+ requires acc(x);
+ ensures read2;
+ {
+ fold rd(read2);
+ }
+
+ // --- helper functions ---
+
+ method void() requires rd(x); ensures rd(x); {}
+ method dispose() requires rd(x); {}
+
+}
diff --git a/Chalice/tests/permission-model/scaling.output.txt b/Chalice/tests/permission-model/scaling.output.txt new file mode 100644 index 00000000..1ff1d596 --- /dev/null +++ b/Chalice/tests/permission-model/scaling.output.txt @@ -0,0 +1,11 @@ +Verification of scaling.chalice
+
+ 33.5: Assertion might not hold. Insufficient fraction at 33.12 for Cell.x.
+ 36.3: The postcondition at 38.13 might not hold. Insufficient fraction at 38.13 for Cell.read1.
+ 50.5: Assertion might not hold. Insufficient fraction at 50.12 for Cell.x.
+ 53.3: The postcondition at 55.13 might not hold. Insufficient fraction at 55.13 for Cell.read1.
+ 65.5: Assertion might not hold. Insufficient fraction at 65.12 for Cell.x.
+ 74.5: Assertion might not hold. Insufficient fraction at 74.12 for Cell.x.
+ 77.3: The postcondition at 79.13 might not hold. Insufficient fraction at 79.13 for Cell.read2.
+
+Boogie program verifier finished with 17 verified, 7 errors
diff --git a/Chalice/tests/permission-model/sequences.chalice b/Chalice/tests/permission-model/sequences.chalice new file mode 100644 index 00000000..0560945d --- /dev/null +++ b/Chalice/tests/permission-model/sequences.chalice @@ -0,0 +1,85 @@ +class Program {
+ var x: int;
+
+ method a(a: seq<A>)
+ requires |a| > 2;
+ requires rd(a[*].f);
+ requires forall i in [0..|a|-1] :: a[i] != null;
+ requires a[0].f == 1;
+ ensures rd(a[*].f);
+ {
+ assert rd(a[*].f);
+ call b(a);
+ }
+
+ method b(a: seq<A>)
+ requires |a| > 2;
+ requires rd(a[*].f);
+ requires forall i in [0..|a|-1] :: a[i] != null;
+ requires a[0].f == 1;
+ ensures rd(a[*].f);
+ {
+ assert rd(a[*].f);
+ }
+
+ method c(a: seq<A>)
+ requires |a| > 2;
+ requires rd(a[*].f);
+ requires forall i in [0..|a|-1] :: a[i] != null;
+ requires a[0].f == 1;
+ ensures rd(a[*].f);
+ {
+ call void(a[1]);
+ call void(a[0]);
+ }
+
+ method c1(a: seq<A>) // ERROR: should fail to verify postcondition
+ requires |a| > 2;
+ requires rd(a[*].f);
+ requires forall i in [0..|a|-1] :: a[i] != null;
+ requires a[0].f == 1;
+ ensures rd(a[*].f);
+ {
+ call dispose(a[1]);
+ }
+
+ method d(a: seq<A>)
+ requires |a| > 2;
+ requires rd(a[*].f);
+ requires forall i in [0..|a|-1] :: a[i] != null;
+ requires a[0].f == 1;
+ ensures rd*(a[*].f);
+ {
+ call dispose(a[1]); // we don't give away all the permission, thus verification succeeds
+
+ var x: int;
+ call x := some_number();
+ call dispose(a[x]); // slighly more interesting, but still clearly ok
+ }
+
+ method e(a: seq<A>) // ERROR: should fail to verify postcondition
+ requires |a| > 2;
+ requires acc(a[*].f,10);
+ requires forall i in [0..|a|-1] :: a[i] != null;
+ requires a[0].f == 1;
+ ensures rd*(a[*].f);
+ {
+ var x: int;
+ call x := some_number();
+ call dispose2(a[x]);
+ }
+
+ method some_number() returns (a: int)
+ ensures 0 <= a && a < 3;
+ {
+ a := 1;
+ }
+
+ method dispose(a: A) requires rd(a.f); {}
+ method dispose2(a: A) requires acc(a.f,10); {}
+ method void(a: A) requires rd(a.f); ensures rd(a.f); {}
+}
+
+class A {
+ var f: int;
+}
diff --git a/Chalice/tests/permission-model/sequences.output.txt b/Chalice/tests/permission-model/sequences.output.txt new file mode 100644 index 00000000..16dd9137 --- /dev/null +++ b/Chalice/tests/permission-model/sequences.output.txt @@ -0,0 +1,6 @@ +Verification of sequences.chalice
+
+ 36.3: The postcondition at 41.13 might not hold. Insufficient permission at 41.13 for A.f
+ 60.3: The postcondition at 65.13 might not hold. Insufficient permission at 65.13 for A.f
+
+Boogie program verifier finished with 20 verified, 2 errors
diff --git a/Chalice/tests/permission-model/test.bat b/Chalice/tests/permission-model/test.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/permission-model/test.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/readme.txt b/Chalice/tests/readme.txt new file mode 100644 index 00000000..0e09fb57 --- /dev/null +++ b/Chalice/tests/readme.txt @@ -0,0 +1,39 @@ +
+Chalice Test Suite
+==================
+
+Contents
+--------
+- examples: Various examples how Chalice can be used to verify concurrent
+ programs.
+- permission-model: Regression tests for the permission model of Chalice.
+- refinements: Regression tests for the refinement extension.
+- test-scripts: Some batch scripts that can be used to execute the tests in an
+ easy and automated way. More information below.
+
+
+Test Scripts
+------------
+In the directory test-scripts are various scripts to allow the execution of the
+tests in different ways. There are launchers in the test directories (e.g. in
+examples or permission-model) to access them.
+
+Commands (sorted by relevance):
+- test.bat <file> [-params]: Execute a test and output the result of the
+ verification. Note: <file> must not include the file extension.
+- reg_test.bat <file> [-params]: Execute a tests as a regression test, i.e., run
+ the test and compare the verification result with the reference output stored
+ in <file.output.txt>. Also shows the differences if any.
+- reg_test_all.bat: Execute all tests as regression tests in the current
+ directory.
+- generete_reference.bat <file> [-params]: Generate the reference output.
+- generate_reference_all.bat: Generate reference files for all tests in the
+ current directory.
+- getboogieoutput.bat: File used internally by generete_reference.bat.
+
+
+Note: There is also an alternative way to execute the tests in example, namely
+to use the script test.bat. The scripts in test-scripts allow more fine-grained
+testing, but they do not allow to use special parameters for certain tests
+(e.g. -autoMagic).
+For the refinement tests, there is a bash script test.sh, similar to test.bat.
diff --git a/Chalice/refinements/AngelicExec.chalice b/Chalice/tests/refinements/AngelicExec.chalice index 06ab9c83..06ab9c83 100644 --- a/Chalice/refinements/AngelicExec.chalice +++ b/Chalice/tests/refinements/AngelicExec.chalice diff --git a/Chalice/refinements/Answer b/Chalice/tests/refinements/Answer index 8bd8a24b..8bd8a24b 100644 --- a/Chalice/refinements/Answer +++ b/Chalice/tests/refinements/Answer diff --git a/Chalice/refinements/Calculator.chalice b/Chalice/tests/refinements/Calculator.chalice index 57c4c87d..57c4c87d 100644 --- a/Chalice/refinements/Calculator.chalice +++ b/Chalice/tests/refinements/Calculator.chalice diff --git a/Chalice/refinements/Celebrity.chalice b/Chalice/tests/refinements/Celebrity.chalice index b0d398e0..b0d398e0 100644 --- a/Chalice/refinements/Celebrity.chalice +++ b/Chalice/tests/refinements/Celebrity.chalice diff --git a/Chalice/refinements/Counter.chalice b/Chalice/tests/refinements/Counter.chalice index d1efae76..d1efae76 100644 --- a/Chalice/refinements/Counter.chalice +++ b/Chalice/tests/refinements/Counter.chalice diff --git a/Chalice/refinements/CounterReverse.chalice b/Chalice/tests/refinements/CounterReverse.chalice index 57d87803..57d87803 100644 --- a/Chalice/refinements/CounterReverse.chalice +++ b/Chalice/tests/refinements/CounterReverse.chalice diff --git a/Chalice/refinements/DSW.chalice b/Chalice/tests/refinements/DSW.chalice index 1737df85..1737df85 100644 --- a/Chalice/refinements/DSW.chalice +++ b/Chalice/tests/refinements/DSW.chalice diff --git a/Chalice/refinements/Duplicates.chalice b/Chalice/tests/refinements/Duplicates.chalice index 52cdc3c3..52cdc3c3 100644 --- a/Chalice/refinements/Duplicates.chalice +++ b/Chalice/tests/refinements/Duplicates.chalice diff --git a/Chalice/refinements/DuplicatesLight.chalice b/Chalice/tests/refinements/DuplicatesLight.chalice index 5fbe0735..5fbe0735 100644 --- a/Chalice/refinements/DuplicatesLight.chalice +++ b/Chalice/tests/refinements/DuplicatesLight.chalice diff --git a/Chalice/refinements/DuplicatesVideo.chalice b/Chalice/tests/refinements/DuplicatesVideo.chalice index 3886cb78..3886cb78 100644 --- a/Chalice/refinements/DuplicatesVideo.chalice +++ b/Chalice/tests/refinements/DuplicatesVideo.chalice diff --git a/Chalice/refinements/List.chalice b/Chalice/tests/refinements/List.chalice index b13f6ee3..b13f6ee3 100644 --- a/Chalice/refinements/List.chalice +++ b/Chalice/tests/refinements/List.chalice diff --git a/Chalice/refinements/LoopFiniteDiff.chalice b/Chalice/tests/refinements/LoopFiniteDiff.chalice index bd744c89..bd744c89 100644 --- a/Chalice/refinements/LoopFiniteDiff.chalice +++ b/Chalice/tests/refinements/LoopFiniteDiff.chalice diff --git a/Chalice/refinements/LoopSqRoot.chalice b/Chalice/tests/refinements/LoopSqRoot.chalice index 4ea9434d..4ea9434d 100644 --- a/Chalice/refinements/LoopSqRoot.chalice +++ b/Chalice/tests/refinements/LoopSqRoot.chalice diff --git a/Chalice/refinements/Pick.chalice b/Chalice/tests/refinements/Pick.chalice index 7df2f90d..7df2f90d 100644 --- a/Chalice/refinements/Pick.chalice +++ b/Chalice/tests/refinements/Pick.chalice diff --git a/Chalice/refinements/RecFiniteDiff.chalice b/Chalice/tests/refinements/RecFiniteDiff.chalice index 1a971aed..1a971aed 100644 --- a/Chalice/refinements/RecFiniteDiff.chalice +++ b/Chalice/tests/refinements/RecFiniteDiff.chalice diff --git a/Chalice/refinements/RecSqRoot.chalice b/Chalice/tests/refinements/RecSqRoot.chalice index a10c1b55..a10c1b55 100644 --- a/Chalice/refinements/RecSqRoot.chalice +++ b/Chalice/tests/refinements/RecSqRoot.chalice diff --git a/Chalice/refinements/SpecStmt.chalice b/Chalice/tests/refinements/SpecStmt.chalice index 15072d41..15072d41 100644 --- a/Chalice/refinements/SpecStmt.chalice +++ b/Chalice/tests/refinements/SpecStmt.chalice diff --git a/Chalice/refinements/SumCubes.chalice b/Chalice/tests/refinements/SumCubes.chalice index a24a0f37..a24a0f37 100644 --- a/Chalice/refinements/SumCubes.chalice +++ b/Chalice/tests/refinements/SumCubes.chalice diff --git a/Chalice/refinements/TestCoupling.chalice b/Chalice/tests/refinements/TestCoupling.chalice index a178c9b4..a178c9b4 100644 --- a/Chalice/refinements/TestCoupling.chalice +++ b/Chalice/tests/refinements/TestCoupling.chalice diff --git a/Chalice/refinements/TestRefines.chalice b/Chalice/tests/refinements/TestRefines.chalice index 3081eb90..3081eb90 100644 --- a/Chalice/refinements/TestRefines.chalice +++ b/Chalice/tests/refinements/TestRefines.chalice diff --git a/Chalice/refinements/TestTransform.chalice b/Chalice/tests/refinements/TestTransform.chalice index 2c18907f..2c18907f 100644 --- a/Chalice/refinements/TestTransform.chalice +++ b/Chalice/tests/refinements/TestTransform.chalice diff --git a/Chalice/refinements/original/CounterPredicate.chalice b/Chalice/tests/refinements/original/CounterPredicate.chalice index fd35c18c..fd35c18c 100644 --- a/Chalice/refinements/original/CounterPredicate.chalice +++ b/Chalice/tests/refinements/original/CounterPredicate.chalice diff --git a/Chalice/refinements/original/DSW0.chalice b/Chalice/tests/refinements/original/DSW0.chalice index d83c5438..d83c5438 100644 --- a/Chalice/refinements/original/DSW0.chalice +++ b/Chalice/tests/refinements/original/DSW0.chalice diff --git a/Chalice/refinements/original/DSW1.chalice b/Chalice/tests/refinements/original/DSW1.chalice index 612f21ac..612f21ac 100644 --- a/Chalice/refinements/original/DSW1.chalice +++ b/Chalice/tests/refinements/original/DSW1.chalice diff --git a/Chalice/refinements/original/DSW10.chalice b/Chalice/tests/refinements/original/DSW10.chalice index 3bf70eeb..3bf70eeb 100644 --- a/Chalice/refinements/original/DSW10.chalice +++ b/Chalice/tests/refinements/original/DSW10.chalice diff --git a/Chalice/refinements/original/DSW2.chalice b/Chalice/tests/refinements/original/DSW2.chalice index 7438c688..7438c688 100644 --- a/Chalice/refinements/original/DSW2.chalice +++ b/Chalice/tests/refinements/original/DSW2.chalice diff --git a/Chalice/refinements/original/DSW3.chalice b/Chalice/tests/refinements/original/DSW3.chalice index dbf161cd..dbf161cd 100644 --- a/Chalice/refinements/original/DSW3.chalice +++ b/Chalice/tests/refinements/original/DSW3.chalice diff --git a/Chalice/refinements/original/DSW4.chalice b/Chalice/tests/refinements/original/DSW4.chalice index f594595a..f594595a 100644 --- a/Chalice/refinements/original/DSW4.chalice +++ b/Chalice/tests/refinements/original/DSW4.chalice diff --git a/Chalice/refinements/original/List.chalice b/Chalice/tests/refinements/original/List.chalice index efcec2c8..efcec2c8 100644 --- a/Chalice/refinements/original/List.chalice +++ b/Chalice/tests/refinements/original/List.chalice diff --git a/Chalice/refinements/original/ListNode.chalice b/Chalice/tests/refinements/original/ListNode.chalice index ae72fe67..ae72fe67 100644 --- a/Chalice/refinements/original/ListNode.chalice +++ b/Chalice/tests/refinements/original/ListNode.chalice diff --git a/Chalice/refinements/original/ListPredicate.chalice b/Chalice/tests/refinements/original/ListPredicate.chalice index af334093..af334093 100644 --- a/Chalice/refinements/original/ListPredicate.chalice +++ b/Chalice/tests/refinements/original/ListPredicate.chalice diff --git a/Chalice/refinements/original/StringBuilder.chalice b/Chalice/tests/refinements/original/StringBuilder.chalice index d73f8373..d73f8373 100644 --- a/Chalice/refinements/original/StringBuilder.chalice +++ b/Chalice/tests/refinements/original/StringBuilder.chalice diff --git a/Chalice/refinements/test.sh b/Chalice/tests/refinements/test.sh index 8ebef27a..8ebef27a 100644 --- a/Chalice/refinements/test.sh +++ b/Chalice/tests/refinements/test.sh diff --git a/Chalice/tests/test-scripts/diff.bat b/Chalice/tests/test-scripts/diff.bat new file mode 100644 index 00000000..87fa935f --- /dev/null +++ b/Chalice/tests/test-scripts/diff.bat @@ -0,0 +1,21 @@ +@echo off
+
+set differ="C:\Program Files\TortoiseSVN\bin\TortoiseMerge.exe"
+if exist %differ% goto :diff
+if not exist %differ% goto :txtdiff
+
+:txtdiff
+echo ====================================
+echo Reference output: %1
+echo ------------------------------------
+type "%1"
+echo ====================================
+echo Currenct output: %2
+echo ------------------------------------
+type "%2"
+echo ====================================
+goto :eof
+
+:diff
+%differ% "%1" "%2"
+goto :eof
diff --git a/Chalice/tests/test-scripts/generate_reference.bat b/Chalice/tests/test-scripts/generate_reference.bat new file mode 100644 index 00000000..a2e9c443 --- /dev/null +++ b/Chalice/tests/test-scripts/generate_reference.bat @@ -0,0 +1,8 @@ +@echo off
+
+set getboogieoutput="%~dp0\getboogieoutput.bat"
+
+echo Generating reference for %1.chalice ...
+call %getboogieoutput% %1 %2 %3 %4 %5 %6 %7
+
+exit /b 0
diff --git a/Chalice/tests/test-scripts/generate_reference_all.bat b/Chalice/tests/test-scripts/generate_reference_all.bat new file mode 100644 index 00000000..83b04700 --- /dev/null +++ b/Chalice/tests/test-scripts/generate_reference_all.bat @@ -0,0 +1,10 @@ +@echo off
+
+set getboogieoutput="%~dp0\getboogieoutput.bat"
+
+for /F %%f in ('dir *.chalice /b') do (
+ echo Generating reference for %%~nf.chalice ...
+ call %getboogieoutput% %%~nf %1 %2 %3 %4 %5 %6 %7
+)
+
+exit /b 0
diff --git a/Chalice/tests/test-scripts/getboogieoutput.bat b/Chalice/tests/test-scripts/getboogieoutput.bat new file mode 100644 index 00000000..eb7d99a4 --- /dev/null +++ b/Chalice/tests/test-scripts/getboogieoutput.bat @@ -0,0 +1,13 @@ +@echo off
+
+set chalice="%~dp0\..\..\chalice.bat"
+
+set output="%1.output.txt"
+
+echo Verification of %1.chalice > %output%
+echo.>> %output%
+call %chalice% "%1.chalice" %2 %3 %4 %5 >> %output% 2>&1
+
+set o=%~dp1%out.bpl
+if exist "%o%" copy "%o%" "%1.bpl">nul
+if exist "%o%" del "%~dp1%out.bpl"
diff --git a/Chalice/tests/test-scripts/reg_test.bat b/Chalice/tests/test-scripts/reg_test.bat new file mode 100644 index 00000000..d31773da --- /dev/null +++ b/Chalice/tests/test-scripts/reg_test.bat @@ -0,0 +1,43 @@ +@echo off
+
+set chalice="%~dp0\..\..\chalice.bat"
+set diff="%~dp0\diff.bat"
+
+if not exist "%1.chalice" goto errorNotFound
+if not exist "%1.output.txt" goto errorNoRef
+
+set output=output.txt
+echo Verification of %1.chalice > %output%
+echo.>> %output%
+call %chalice% "%1.chalice" %2 %3 %4 %5 %6 %7 >> %output% 2>&1
+
+fc "%1.output.txt" output.txt > nul
+if not errorlevel 1 goto passTest
+goto failTest
+
+:passTest
+echo OK: %1.chalice
+goto end
+
+:failTest
+echo FAIL: %1.chalice
+call %diff% "%1.output.txt" output.txt
+goto errorEnd
+
+:errorEnd
+if exist out.bpl del out.bpl
+if exist output.txt del output.txt
+exit /b 1
+
+:end
+if exist out.bpl del out.bpl
+if exist output.txt del output.txt
+exit /b 0
+
+:errorNotFound
+echo ERROR: %1.chalice not found.
+goto errorEnd
+
+:errorNoRef
+echo ERROR: %1.output.txt (reference output) not found.
+goto errorEnd
diff --git a/Chalice/tests/test-scripts/reg_test_all.bat b/Chalice/tests/test-scripts/reg_test_all.bat new file mode 100644 index 00000000..6bbac775 --- /dev/null +++ b/Chalice/tests/test-scripts/reg_test_all.bat @@ -0,0 +1,9 @@ +@echo off
+
+set regtest="%~dp0\reg_test.bat"
+
+for /F %%f in ('dir *.chalice /b') do (
+ call %regtest% %%~nf %1 %2 %3 %4 %5 %6 %7 %8
+)
+
+exit /b 0
diff --git a/Chalice/tests/test-scripts/test.bat b/Chalice/tests/test-scripts/test.bat new file mode 100644 index 00000000..321fdcef --- /dev/null +++ b/Chalice/tests/test-scripts/test.bat @@ -0,0 +1,17 @@ +@echo off
+
+set chalice="%~dp0\..\..\chalice.bat"
+
+if not exist "%1.chalice" goto errorNotFound
+
+set output=output.txt
+echo Verification of %1.chalice > %output%
+echo.>> %output%
+call %chalice% "%1.chalice" %2 %3 %4 %5 %6 %7 >> %output% 2>&1
+type %output%
+
+exit /B 0
+
+:errorNotFound
+echo ERROR: %1.chalice not found.
+exit /B 1
|