diff options
| author |  Unknown <afd@afd-THINK> | 2012-09-21 09:00:04 +0100 |
|---|---|---|
| committer | Unknown <afd@afd-THINK> | 2012-09-21 09:00:04 +0100 |
| commit | e6f74f9c507607556e408153e66ac143b93c371a (patch) | |
| tree | ced06bd9fcecbe3a500c2a60348fcfead0ece020 | |
| parent | 15e8142718b25cc3d3d56286de8955c3296848fb (diff) | |
| parent | 5784ba07c74bf6d5af0743d306a77dcf0f4236d5 (diff) | |
Merge
109 files changed, 1617 insertions, 317 deletions
diff --git a/Chalice/build.sbt b/Chalice/build.sbt index 3fa72ec5..ea32574f 100644 --- a/Chalice/build.sbt +++ b/Chalice/build.sbt @@ -3,7 +3,7 @@ name := "Chalice" version := "1.0" -scalaVersion := "2.8.1" +scalaVersion := "2.9.2" scalacOptions += "-deprecation" diff --git a/Chalice/chalice.bat b/Chalice/chalice.bat index 6400ca7b..66dc095c 100644 --- a/Chalice/chalice.bat +++ b/Chalice/chalice.bat @@ -12,11 +12,11 @@ if not %ERRORLEVEL%==0 ( )
-set SCALA_DIR=scala-2.8.1
+set SCALA_DIR=scala-2.9.2
REM Set classpath elements
set __CP.SCALA_LIB="%ROOT_DIR%project\boot\%SCALA_DIR%\lib\scala-library.jar"
-set __CP.CHALICE="%ROOT_DIR%target\%SCALA_DIR%.final\classes"
+set __CP.CHALICE="%ROOT_DIR%target\%SCALA_DIR%\classes"
REM Assemble classpath and check if all classpath elements exist
set CP=
diff --git a/Chalice/scripts/create_release/create_release.bat b/Chalice/scripts/create_release/create_release.bat index a0d67fd9..5aadd36e 100644 --- a/Chalice/scripts/create_release/create_release.bat +++ b/Chalice/scripts/create_release/create_release.bat @@ -6,7 +6,7 @@ set BASE_DIR=%~dp0\..\.. set RELEASE_DIR_SRC=%~dp0\files
set RELEASE_DIR_DST=%~dp0\release
-set CHALICE_JAR_SRC=%BASE_DIR%\target\scala-2.8.1.final\chalice_2.8.1-1.0.jar
+set CHALICE_JAR_SRC=%BASE_DIR%\target\scala-2.9.2\chalice_2.9.2-1.0.jar
set CHALICE_JAR_DST=%RELEASE_DIR_DST%\chalice.jar
pushd %BASE_DIR%
diff --git a/Chalice/src/main/scala/Ast.scala b/Chalice/src/main/scala/Ast.scala index 1cfd173e..ff41e9db 100644 --- a/Chalice/src/main/scala/Ast.scala +++ b/Chalice/src/main/scala/Ast.scala @@ -209,8 +209,13 @@ case class Function(id: String, ins: List[Variable], out: Type, spec: List[Speci result
}
var isUnlimited = false
+ var isStatic = false
var isRecursive = false
var SCC: List[Function] = Nil
+ // the 'height' of this function is determined by a topological sort of the
+ // condensation of the call graph; mutually recursive functions get the same
+ // height.
+ var height: Int = -1
}
case class Condition(id: String, where: Option[Expression]) extends NamedMember(id)
case class Variable(id: String, t: Type, isGhost: Boolean, isImmutable: Boolean) extends ASTNode {
diff --git a/Chalice/src/main/scala/Chalice.scala b/Chalice/src/main/scala/Chalice.scala index 077e5c46..2514d6b1 100644 --- a/Chalice/src/main/scala/Chalice.scala +++ b/Chalice/src/main/scala/Chalice.scala @@ -41,6 +41,7 @@ object Chalice { private[chalice] var percentageSupport = 2;
private[chalice] var smoke = false;
private[chalice] var smokeAll = false;
+ private[chalice] var timingVerbosity = 1;
/**
* Holds all command line arguments not stored in fields of Chalice.
@@ -126,12 +127,20 @@ object Chalice { "smoke testing; try to find unreachable code, preconditions/invariants/predicates that are equivalent to false and assumptions that introduce contradictions, by trying to prove 'false' at various positions."),
"smokeAll" -> (
{() => smokeAll = true; smoke = true},
- "aggressive smoke testing; try to prove false after every statement.")
+ "aggressive smoke testing; try to prove false after every statement."),
+ "time" -> (
+ {() => timingVerbosity = 2},
+ "sets /time:2")
)
// help text for options with arguments
val nonBooleanOptions = ListMap(
"boogie:<file>" -> "use the executable of Boogie at <file>",
"print:<file>" -> "print the Boogie program used for verification into file <file>",
+ "time:<n>" -> ("output timing information\n"+
+ "0: no information is included\n"+
+ "1: the overall verification time is output (default)\n"+
+ "2: detailed timings for each phase of the verification are output\n"+
+ "3: (used for testing only) output the overall verification time on stderr"),
"defaults:<level>" -> ("defaults to reduce specification overhead\n"+
"level 0 or below: no defaults\n"+
"level 1: unfold predicates with receiver this in pre and postconditions\n"+
@@ -169,10 +178,17 @@ object Chalice { else if (a.startsWith("/percentageSupport:") || a.startsWith("-percentageSupport:")) {
try {
val in = Integer.parseInt(a.substring(19));
- if (in < 0 || in > 3) CommandLineError("/percentageSupport takes only values 0,1,2 or 3", help)
+ 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("/time:") || a.startsWith("-time:")) {
+ try {
+ val in = Integer.parseInt(a.substring(6));
+ if (in < 0 || in > 3) CommandLineError("/time takes only values 0, 1, 2 or 3", help)
+ else timingVerbosity = in
+ } catch { case _ => CommandLineError("/time takes integer argument", help); }
+ }
else if (a.startsWith("-boogieOpt:") || a.startsWith("/boogieOpt:"))
aBoogieArgs += ("\"/" + a.substring(11) + "\"" + " ")
else if (a.startsWith("-bo:") || a.startsWith("/bo:"))
@@ -251,7 +267,7 @@ object Chalice { if (vsMode)
ReportError(e.next.pos, e.msg);
else
- Console.err.println("Error: " + e);
+ Console.out.println("Error: " + e);
Nil
case parser.Success(prog, _) =>
val pprog = if (smoke) SmokeTest.smokeProgram(prog) else prog
@@ -268,36 +284,64 @@ object Chalice { // typecheck program
Resolver.Resolve(program) match {
case Resolver.Errors(msgs) =>
- if (!vsMode) Console.err.println("The program did not typecheck.");
+ if (!vsMode) Console.out.println("The program did not typecheck.");
msgs foreach { msg => ReportError(msg._1, msg._2) };
false;
case Resolver.Success() =>
true
}
}
-
+
+ object VerificationSteps extends Enumeration {
+ type VerificationSteps = Value
+ val Init = Value("Init")
+ val Parse = Value("Parse")
+ val TypeCheck = Value("TypeCheck")
+ val PrintProgram = Value("PrintProgram")
+ val Translate = Value("Translate")
+ val Boogie = Value("Boogie")
+ val GenerateCode = Value("GenerateCode")
+ }
+
def main(args: Array[String]): Unit = {
+ var timings = scala.collection.immutable.ListMap[VerificationSteps.Value, Long]()
+ for (step <- VerificationSteps.values) timings += (step -> 0)
+ var startTime = System.nanoTime
+ var tmpTime = startTime
+
//Parse command line arguments
val params = parseCommandLine(args) match {
case Some(p) => p
case None => return //invalid arguments, help has been displayed
}
-
+
+ timings += (VerificationSteps.Init -> (System.nanoTime - tmpTime))
+ tmpTime = System.nanoTime
+
try {
val program = parsePrograms(params) match {
case Some(p) => p
case None => return //illegal program, errors have already been displayed
}
+
+ timings += (VerificationSteps.Parse -> (System.nanoTime - tmpTime))
+ tmpTime = System.nanoTime
if(!params.doTypecheck || !typecheckProgram(params, program))
return ;
-
+
+ timings += (VerificationSteps.TypeCheck -> (System.nanoTime - tmpTime))
+ tmpTime = System.nanoTime
+
if (params.printProgram) {
Console.out.println("Program after type checking: ");
PrintProgram.P(program)
}
+
+ timings += (VerificationSteps.PrintProgram -> (System.nanoTime - tmpTime))
+ tmpTime = System.nanoTime
if(!params.doTranslate)
return;
@@ -317,6 +361,9 @@ object Chalice { val translator = new Translator();
var bplProg: List[Boogie.Decl] = Nil
bplProg = translator.translateProgram(program);
+
+ timings += (VerificationSteps.Translate -> (System.nanoTime - tmpTime))
+ tmpTime = System.nanoTime
// write to out.bpl
val bplText = TranslatorPrelude.P + (bplProg map Boogie.Print).foldLeft(""){ (a, b) => a + b };
@@ -347,7 +394,8 @@ object Chalice { val boogieOutput: ListBuffer[String] = new ListBuffer()
while (line!=null){
if (!smoke) {
- Console.out.println(line);
+ if (previous_line != null) Console.out.println
+ Console.out.print(line);
Console.out.flush;
}
boogieOutput += line
@@ -356,11 +404,14 @@ object Chalice { }
boogie.waitFor;
input.close;
+
+ timings += (VerificationSteps.Boogie -> (System.nanoTime - tmpTime))
+ tmpTime = System.nanoTime
// smoke test output
if (smoke) {
val output = SmokeTest.processBoogieOutput(boogieOutput.toList)
- Console.out.println(output);
+ Console.out.print(output);
Console.out.flush;
}
@@ -368,6 +419,9 @@ object Chalice { if(params.gen && (previous_line != null) && previous_line.endsWith(" 0 errors")) { // hack
generateCSharpCode(params, program)
}
+
+ timings += (VerificationSteps.GenerateCode -> (System.nanoTime - tmpTime))
+ tmpTime = System.nanoTime
} catch {
case e:InternalErrorException => {
if (params.showFullStackTrace) {
@@ -388,6 +442,23 @@ object Chalice { return
}
}
+
+ val time = System.nanoTime - startTime
+ if (timingVerbosity == 1) {
+ Console.out.println(" in " + ("%1.3f" format (time / 1000000000.0)) + " seconds")
+ } else if (timingVerbosity == 2) {
+ Console.out.println; Console.out.println
+ Console.out.println("Timings Information")
+ val max = (timings.keySet.toList.map(a => a.toString.length).sortWith( (a, b) => a > b )).head
+ for ((step, time) <- timings) {
+ Console.out.println(" " + step + ": " + (" "*(max - step.toString.length)) + ("%1.3f" format (time / 1000000000.0)) + " seconds")
+ }
+ } else {
+ Console.out.println
+ }
+ if (timingVerbosity == 3) {
+ Console.err.println(("%1.3f" format (time / 1000000000.0)))
+ }
}
def generateCSharpCode(params: CommandLineParameters, program: List[TopLevelDecl]): Unit = {
@@ -404,7 +475,7 @@ object Chalice { }
def CommandLineError(msg: String, help: String) = {
- Console.err.println("Error: " + msg)
+ Console.out.println("Error: " + msg)
}
def ReportError(pos: Position, msg: String) = {
@@ -412,7 +483,7 @@ object Chalice { val (r,c) = (pos.line, pos.column)
Console.out.println(r + "," + c + "," + r + "," + (c+5) + ":" + msg);
} else {
- Console.err.println(pos + ": " + msg)
+ Console.out.println(pos + ": " + msg)
}
}
diff --git a/Chalice/src/main/scala/Parser.scala b/Chalice/src/main/scala/Parser.scala index d75cf9c8..9a4cd272 100644 --- a/Chalice/src/main/scala/Parser.scala +++ b/Chalice/src/main/scala/Parser.scala @@ -32,7 +32,7 @@ class Parser extends StandardTokenParsers { "between", "and", "above", "below", "share", "unshare", "acquire", "release", "downgrade",
"lock", "fork", "join", "rd", "acc", "credit", "holds", "old", "assigned",
"call", "if", "else", "while", "invariant", "lockchange",
- "returns", "requires", "ensures", "where",
+ "returns", "requires", "ensures", "where", "static",
"int", "bool", "false", "true", "null", "string", "waitlevel", "lockbottom",
"module", "external",
"predicate", "function", "free", "send", "receive",
@@ -105,10 +105,11 @@ class Parser extends StandardTokenParsers { }
def functionDecl = {
currentLocalVariables = Set[String]();
- ("unlimited" ?) ~ ("function" ~> ident) ~ formalParameters(true) ~ (":" ~> typeDecl) ~ (methodSpec*) ~ opt("{" ~> expression <~ "}") ^^ {
- case u ~ id ~ ins ~ out ~ specs ~ body => {
+ ("unlimited" ?) ~ ("static" ?) ~ ("function" ~> ident) ~ formalParameters(true) ~ (":" ~> typeDecl) ~ (methodSpec*) ~ opt("{" ~> expression <~ "}") ^^ {
+ case u ~ s ~ id ~ ins ~ out ~ specs ~ body => {
val f = Function(id, ins, out, specs, body);
if (u.isDefined) f.isUnlimited = true;
+ if (s.isDefined) f.isStatic = true;
f
}
}
diff --git a/Chalice/src/main/scala/Prelude.scala b/Chalice/src/main/scala/Prelude.scala index f54cee2c..410a96ef 100644 --- a/Chalice/src/main/scala/Prelude.scala +++ b/Chalice/src/main/scala/Prelude.scala @@ -61,6 +61,7 @@ object TypesPL extends PreludeComponent { type Field a;
type HeapType = <a>[ref,Field a]a;
type MaskType = <a>[ref,Field a][PermissionComponent]int;
+type PMaskType = <a>[ref,Field a]bool;
type CreditsType = [ref]int;
type ref;
const null: ref;
@@ -83,6 +84,8 @@ const Permission$Full: [PermissionComponent]int; 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);
+const ZeroPMask: PMaskType;
+axiom (forall<T> o: ref, f: Field T :: ZeroPMask[o,f] == false);
axiom IsGoodMask(ZeroMask);
const unique joinable: Field int;
axiom NonPredicateField(joinable);
@@ -147,6 +150,7 @@ const CurrentModule: ModuleName; type TypeName;
function dtype(ref) returns (TypeName);
const CanAssumeFunctionDefs: bool;
+const FunctionContextHeight: int;
type Mu;
const unique mu: Field Mu;
@@ -186,6 +190,10 @@ function IsGoodInhaleState(ih: HeapType, h: HeapType, (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])
}
+function IsGoodExhalePredicateState(eh: HeapType, h: HeapType, pm: PMaskType) returns (bool)
+{
+ (forall<T> o: ref, f: Field T :: { eh[o, f] } pm[o, f] ==> eh[o, f] == h[o, f])
+}
function IsGoodExhaleState(eh: HeapType, h: HeapType,
m: MaskType, sm: MaskType) returns (bool)
{
@@ -196,7 +204,8 @@ function IsGoodExhaleState(eh: HeapType, h: HeapType, (forall o: ref :: { h[o, rdheld] } h[o, rdheld] ==> eh[o, mu] == h[o, mu]) &&
(forall o: ref :: { h[o, forkK] } { eh[o, forkK] } h[o, forkK] == eh[o, forkK]) &&
(forall o: ref :: { h[o, held] } { eh[o, held] } h[o, held] == eh[o, held]) &&
- (forall o: ref, f: Field int :: { eh[o, f], PredicateField(f) } PredicateField(f) ==> h[o, f] <= eh[o, f])
+ (forall o: ref, f: Field int :: { eh[o, f], PredicateField(f) } PredicateField(f) ==> h[o, f] <= eh[o, f]) &&
+ (forall pmask: Field PMaskType, o: ref :: eh[o, pmask] == h[o, pmask])
}"""
}
object PermissionFunctionsAndAxiomsPL extends PreludeComponent {
@@ -207,8 +216,7 @@ object PermissionFunctionsAndAxiomsPL extends PreludeComponent { function {:expand false} CanRead<T>(m: MaskType, sm: MaskType, obj: ref, f: Field T) returns (bool)
{
- 0 < m[obj,f][perm$R] || 0 < m[obj,f][perm$N] ||
- 0 < sm[obj,f][perm$R] || 0 < sm[obj,f][perm$N]
+ 0 < m[obj,f][perm$R] || 0 < m[obj,f][perm$N]
}
function {:expand false} CanReadForSure<T>(m: MaskType, obj: ref, f: Field T) returns (bool)
{
@@ -280,6 +288,16 @@ 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 for recording enclosure of one predicate instance in another
+function #predicateInside#(x:ref, p: Field (int), v:int, y:ref, q:Field (int), w : int) returns (bool);
+
+// transitivity for #predicateInside#
+axiom (forall x:ref, p: Field (int), v:int, y:ref, q:Field (int), w : int, z:ref, r:Field(int),u:int :: {#predicateInside#(x,p,v,y,q,w), #predicateInside#(y,q,w,z,r,u)} #predicateInside#(x,p,v,y,q,w) && #predicateInside#(y,q,w,z,r,u) ==> #predicateInside#(x,p,v,z,r,u));
+
+// knowledge that two identical instances of the same predicate cannot be inside each other
+axiom (forall x:ref, p: Field (int), v:int, y:ref, w:int :: {#predicateInside#(x,p,v,y,p,w)} #predicateInside#(x,p,v,y,p,w) ==> x!=y);
+
+
function submask(m1: MaskType, m2: MaskType) returns (bool);
axiom (forall m1: MaskType, m2: MaskType :: {submask(m1, m2)}
diff --git a/Chalice/src/main/scala/Resolver.scala b/Chalice/src/main/scala/Resolver.scala index dda5d989..95ae5f9e 100644 --- a/Chalice/src/main/scala/Resolver.scala +++ b/Chalice/src/main/scala/Resolver.scala @@ -19,9 +19,13 @@ object Resolver { 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 += ((pos, msg))}
- final def SetClass(cl: Class): ProgramContext = new MProgramContext(cl, null, this)
+ final def SetClass(cl: Class): ProgramContext = new MProgramContext(cl, null, false, this)
final def SetMember(m: Member): ProgramContext = {
- var ctx:ProgramContext = new MProgramContext(currentClass, m, this)
+ val static = m match {
+ case f: Function => f.isStatic
+ case _ => false
+ }
+ var ctx:ProgramContext = new MProgramContext(currentClass, m, static, this)
m match {
case m: Method =>
assert(currentClass == m.Parent)
@@ -36,20 +40,30 @@ object Resolver { }
ctx
}
+ final def AsNonStatic(): ProgramContext = new NSProgramContext(this)
def LookupVariable(id: String): Option[Variable] = None
def IsVariablePresent(vr: Variable): Boolean = false
-
+ def IsStatic: Boolean = false
+
private class LProgramContext(v: Variable, parent: ProgramContext) extends ProgramContext(parent.decls, parent.currentClass, parent.currentMember, errors) {
assert (v!=null)
override def LookupVariable(id: String): Option[Variable] =
if (id == v.id) Some(v) else parent.LookupVariable(id)
override def IsVariablePresent(vr: Variable): Boolean =
if (vr == v) true else parent.IsVariablePresent(vr)
+ override def IsStatic = parent.IsStatic
+ }
+ private class MProgramContext(cl: Class, m: Member, static: Boolean, parent: ProgramContext) extends ProgramContext(parent.decls, cl, m, errors) {
+ override def LookupVariable(id: String) = parent.LookupVariable(id)
+ override def IsVariablePresent(vr: Variable) = parent.IsVariablePresent(vr)
+ override def IsStatic: Boolean =
+ if (static) true else parent.IsStatic
}
- private class MProgramContext(cl: Class, m: Member, parent: ProgramContext) extends ProgramContext(parent.decls, cl, m, errors) {
+ private class NSProgramContext(parent: ProgramContext) extends ProgramContext(parent.decls, parent.currentClass, parent.currentMember, errors) {
override def LookupVariable(id: String) = parent.LookupVariable(id)
override def IsVariablePresent(vr: Variable) = parent.IsVariablePresent(vr)
+ override def IsStatic = false
}
}
@@ -244,6 +258,15 @@ object Resolver { }
b
}
+ def hasAccessibilityPredicate(e: Expression) = {
+ var b = false
+ e transform {
+ case _: PermissionExpr => b = true; None
+ case ma: MemberAccess => if (ma.isPredicate) b = true; None
+ case _ => None
+ }
+ b
+ }
spec foreach {
case p@Precondition(e) =>
ResolveExpr(e, context, false, true)(false)
@@ -251,6 +274,7 @@ object Resolver { case p@Postcondition(e) =>
ResolveExpr(e, context, false, true)(false)
if (hasCredit(e)) context.Error(p.pos, "the specification of functions cannot contain credit expressions")
+ if (hasAccessibilityPredicate(e)) context.Error(p.pos, "the postcondition of functions cannot contain accessibility predicates (permissions are returned automatically)")
case lc : LockChange => context.Error(lc.pos, "lockchange not allowed on function")
}
@@ -275,10 +299,13 @@ object Resolver { }
}
- // fill in SCC for recursive functions
- val (_, h) = calls.computeSCC;
+ // fill in SCC and height for recursive functions
+ val (callGraphCondensation, h) = calls.computeSCC;
+ val callGraphTopoSort = callGraphCondensation.computeTopologicalSort.reverse
h.keys foreach {f:Function =>
f.SCC = h(f);
+ f.height = callGraphTopoSort.indexOf(h(f))
+ assert(f.height >= 0)
assert(f.SCC contains f);
if (h(f).size > 1)
f.isRecursive = true;
@@ -939,7 +966,11 @@ object Resolver { context.LookupVariable(id) match {
case None => context.Error(ve.pos, "undefined local variable " + id); ve.typ = IntClass
case Some(v) => ve.Resolve(v) }
- case v:ThisExpr => v.typ = context.currentClass
+ case v:ThisExpr =>
+ v.typ = context.currentClass
+ if (context.IsStatic) {
+ context.Error(v.pos, "Accessing non-static member not allowed in static context.")
+ }
case sel @ MemberAccess(e, id) =>
ResolveExpr(e, context, twoStateContext, false)
var typ: Class = IntClass
@@ -1018,7 +1049,8 @@ object Resolver { if (!e.typ.IsBool) context.Error(expr.pos, "not-expression requires boolean operand")
expr.typ = BoolClass
case appl@FunctionApplication(obj, id, args) =>
- ResolveExpr(obj, context, twoStateContext, false);
+ // HACK: allow non-static access for receiver
+ ResolveExpr(obj, context.AsNonStatic(), twoStateContext, false);
args foreach { arg => ResolveExpr(arg, context, twoStateContext, false)};
// lookup function
appl.typ = IntClass
diff --git a/Chalice/src/main/scala/SmokeTest.scala b/Chalice/src/main/scala/SmokeTest.scala index f317f24c..bd733ee6 100644 --- a/Chalice/src/main/scala/SmokeTest.scala +++ b/Chalice/src/main/scala/SmokeTest.scala @@ -76,7 +76,7 @@ object SmokeTest { case None => ""
case Some((verified,errors)) =>
realErrors = errors-smokeErrors.size
- "Boogie program verifier finished with " + realErrors + " errors and " + smokeTestWarnings + " smoke test warnings."
+ "Boogie program verifier finished with " + realErrors + " errors and " + smokeTestWarnings + " smoke test warnings"
})
verificationResult +
diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala index 94d44d9e..f09c37e7 100644 --- a/Chalice/src/main/scala/Translator.scala +++ b/Chalice/src/main/scala/Translator.scala @@ -168,15 +168,29 @@ class Translator { 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("this", tref) :: (f.ins map Variable2BVar), BVar("$myresult", f.out.typ)) ::
+ {
+ val bIns = if (f.isStatic) {
+ BVar("heap", theap) :: (f.ins map Variable2BVar)
+ } else {
+ BVar("heap", theap) :: BVar("this", tref) :: (f.ins map Variable2BVar)
+ }
+ Boogie.Function(functionName(f), bIns, BVar("$myresult", f.out.typ))
+ } ::
// check definedness of the function's precondition and body
- Proc(f.FullName + "$checkDefinedness",
- NewBVarWhere("this", new Type(currentClass)) :: (f.ins map {i => Variable2BVarWhere(i)}),
+ Proc(f.FullName + "$checkDefinedness",
+ {
+ val insVar = f.ins map {i => Variable2BVarWhere(i)}
+ if (!f.isStatic) {
+ NewBVarWhere("this", new Type(currentClass)) :: insVar
+ } else {
+ insVar
+ }
+ },
Nil,
GlobalNames,
- DefaultPrecondition(),
+ DefaultPrecondition(f.isStatic),
functionKStmts :::
- //bassume(CanAssumeFunctionDefs) ::
+ bassume(FunctionContextHeight ==@ f.height) ::
DefinePreInitialState :::
// check definedness of the precondition
InhaleWithChecking(Preconditions(f.spec) map { p => (if(0 < Chalice.defaults) UnfoldPredicatesWithReceiverThis(p) else p)}, "precondition", functionK) :::
@@ -189,6 +203,19 @@ class Translator { // check definedness of function body
checkBody :::
(f.definition match {case Some(e) => BLocal(myresult) :: (Boogie.VarExpr("result") := etran.Tr(e)); case None => Nil}) :::
+ // assume canCall for all recursive calls
+ {
+ var b: Expr = true
+ f.definition match {
+ case Some(e) => e transform {
+ case app @ FunctionApplication(obj, id, args) if id == f.Id =>
+ b = b && FunctionApp(functionName(f) + "#canCall", (obj :: args) map etran.Tr); None
+ case _ => None
+ }
+ case _ =>
+ }
+ bassume(b) :: 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", functionK, true)) ::
@@ -206,21 +233,35 @@ class Translator { def definitionAxiom(f: Function, definition: Expression): List[Decl] = {
val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)})
val thisArg = VarExpr("this")
- val args = thisArg :: inArgs;
+ val args = if (f.isStatic) inArgs else thisArg :: inArgs;
+
+ /////
- val formalsNoMask = BVar(HeapName, theap) :: BVar("this", tref) :: (f.ins map Variable2BVar)
+ val formalsNoHeapNoMask = if (f.isStatic) {
+ (f.ins map Variable2BVar)
+ } else {
+ BVar("this", tref) :: (f.ins map Variable2BVar)
+ }
+
+ val formalsNoMask = BVar(HeapName, theap) :: formalsNoHeapNoMask
val formals = BVar(MaskName, tmask) :: BVar(SecMaskName, tmask) :: formalsNoMask
val applyF = FunctionApp(functionName(f), List(etran.Heap) ::: args);
val limitedApplyF = FunctionApp(functionName(f) + "#limited", List(etran.Heap) ::: args)
+ /////
+ val limitedFTrigger = FunctionApp(functionName(f) + "#limited#trigger", args)
+
val pre = Preconditions(f.spec).foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b) });
val wellformed = wf(VarExpr(HeapName), VarExpr(MaskName), VarExpr(SecMaskName))
val triggers = f.dependentPredicates map (p => new Trigger(List(limitedApplyF, wellformed, FunctionApp("#" + p.FullName+"#trigger", thisArg :: Nil))))
+ /////
+ val newTriggers = new Trigger(List(limitedFTrigger, wellformed) ::: (f.dependentPredicates map (p => FunctionApp("#" + p.FullName+"#trigger", thisArg :: Nil))))
/** Limit application of the function by introducing a second (limited) function */
val body = etran.Tr(
- if (f.isRecursive && ! f.isUnlimited) {
+ if (true) { // used to be: if (f.isRecursive && ! f.isUnlimited) ... but now we treat all functions uniformly
val limited = Map() ++ (f.SCC zip (f.SCC map {f =>
val result = Function(f.id + "#limited", f.ins, f.out, f.spec, None);
+ result.isStatic = f.isStatic
result.Parent = f.Parent;
result;
}));
@@ -237,21 +278,28 @@ class Translator { }
);
+ Boogie.Function(functionName(f) + "#canCall", formalsNoHeapNoMask, BVar("$myresult", tbool)) ::
/* axiom (forall h: HeapType, m, sm: MaskType, this: ref, x_1: t_1, ..., x_n: t_n ::
wf(h, m, sm) && CurrentModule == module#C ==> #C.f(h, m, this, x_1, ..., x_n) == tr(body))
*/
Axiom(new Boogie.Forall(Nil,
- formals, List(new Trigger(List(applyF,wellformed))),
+ formals, newTriggers :: List(new Trigger(List(applyF,wellformed))) ,
(wellformed && (CurrentModule ==@ ModuleName(currentClass)) && etran.TrAll(pre))
==>
(applyF ==@ body))) ::
- (if (f.isRecursive)
+ (if (true)
+ // used to be: (if (f.isRecursive) ... but now we treat all functions uniformly
// define the limited function (even for unlimited function since its SCC might have limited functions)
Boogie.Function(functionName(f) + "#limited", formalsNoMask, BVar("$myresult", f.out.typ)) ::
Axiom(new Boogie.Forall(Nil, formals,
- new Trigger(List(applyF,wellformed)) :: triggers,
+ new Trigger(List(applyF,wellformed)) :: Nil,
+ // new Trigger(List(applyF,wellformed)) :: triggers, // commented, as secondary patterns seem not to be working
(wellformed ==> (applyF ==@ limitedApplyF)))) ::
- Nil
+ Boogie.Function(functionName(f) + "#limited#trigger", formalsNoHeapNoMask, BVar("$myresult", tbool)) ::
+ Axiom(new Boogie.Forall(Nil, formals,
+ List(new Trigger(List(limitedApplyF,wellformed))),
+ (wellformed ==> limitedFTrigger))) ::
+ Nil ///// above
else
Nil)
}
@@ -271,18 +319,29 @@ class Translator { val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)});
val frameFunctionName = "#" + functionName(f);
- val args = VarExpr("this") :: inArgs;
+ val args = if (!f.isStatic) VarExpr("this") :: inArgs else inArgs;
val applyF = FunctionApp(functionName(f) + (if (f.isRecursive) "#limited" else ""), List(etran.Heap) ::: args);
val applyFrameFunction = FunctionApp(frameFunctionName, partialHeap :: args)
val wellformed = wf(VarExpr(HeapName), VarExpr(MaskName), VarExpr(SecMaskName))
- Boogie.Function(frameFunctionName, Boogie.BVar("state", tpartialheap) :: Boogie.BVar("this", tref) :: (f.ins map Variable2BVar), new BVar("$myresult", f.out.typ)) ::
- Axiom(new Boogie.Forall(
- BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar(SecMaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar),
- new Trigger(List(applyF, wellformed)),
- (wellformed && CanAssumeFunctionDefs)
- ==>
- (applyF ==@ applyFrameFunction))
+ if (!f.isStatic) (
+ Boogie.Function(frameFunctionName, Boogie.BVar("state", tpartialheap) :: Boogie.BVar("this", tref) :: (f.ins map Variable2BVar), new BVar("$myresult", f.out.typ)) ::
+ Axiom(new Boogie.Forall(
+ BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar(SecMaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar),
+ new Trigger(List(applyF, wellformed)),
+ (wellformed)
+ ==>
+ (applyF ==@ applyFrameFunction))
+ )
+ ) else (
+ Boogie.Function(frameFunctionName, Boogie.BVar("state", tpartialheap) :: (f.ins map Variable2BVar), new BVar("$myresult", f.out.typ)) ::
+ Axiom(new Boogie.Forall(
+ BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar(SecMaskName, tmask) :: (f.ins map Variable2BVar),
+ new Trigger(List(applyF, wellformed)),
+ (wellformed)
+ ==>
+ (applyF ==@ applyFrameFunction))
+ )
)
} else {
// Encoding with universal quantification over two heaps
@@ -290,7 +349,8 @@ class Translator { wf(h1,m1,sm1) && wf(h2,m2,sm1) && functionDependenciesEqual(h1, h2, #C.f) ==>
#C.f(h1, m1, sm1, this, x_1, ..., x_n) == #C.f(h2, m2, sm2, this, x_1, ..., x_n)
*/
- var args = VarExpr("this") :: (f.ins map {i => Boogie.VarExpr(i.UniqueName)});
+ var args = if (!f.isStatic) VarExpr("this") :: (f.ins map {i => Boogie.VarExpr(i.UniqueName)})
+ else (f.ins map {i => Boogie.VarExpr(i.UniqueName)})
// create two heaps
val (globals1V, globals1) = etran.FreshGlobals("a"); val etran1 = new ExpressionTranslator(globals1, currentClass);
@@ -301,25 +361,36 @@ class Translator { val apply2 = FunctionApp(functionName(f), etran2.Heap :: args)
val wellformed1 = wf(etran1.Heap, etran1.Mask, etran1.SecMask)
val wellformed2 = wf(etran2.Heap, etran2.Mask, etran2.SecMask)
-
- Axiom(new Boogie.Forall(
- heap1 :: heap2 :: mask1 :: mask2 :: secmask1 :: secmask2 :: BVar("this", tref) :: (f.ins map Variable2BVar),
- new Trigger(List(apply1, apply2, wellformed1, wellformed2)),
- (wellformed1 && wellformed2 && functionDependenciesEqual(pre, etran1, etran2) && CanAssumeFunctionDefs)
- ==>
- (apply1 ==@ apply2)
- ))
+
+ if (!f.isStatic) (
+ Axiom(new Boogie.Forall(
+ heap1 :: heap2 :: mask1 :: mask2 :: secmask1 :: secmask2 :: BVar("this", tref) :: (f.ins map Variable2BVar),
+ new Trigger(List(apply1, apply2, wellformed1, wellformed2)),
+ (wellformed1 && wellformed2 && functionDependenciesEqual(pre, etran1, etran2))
+ ==>
+ (apply1 ==@ apply2)
+ ))
+ ) else (
+ Axiom(new Boogie.Forall(
+ heap1 :: heap2 :: mask1 :: mask2 :: secmask1 :: secmask2 :: (f.ins map Variable2BVar),
+ new Trigger(List(apply1, apply2, wellformed1, wellformed2)),
+ (wellformed1 && wellformed2 && functionDependenciesEqual(pre, etran1, etran2))
+ ==>
+ (apply1 ==@ apply2)
+ ))
+ )
}
}
def postconditionAxiom(f: Function): List[Decl] = {
/* axiom (forall h: HeapType, m, sm: MaskType, this: ref, x_1: t_1, ..., x_n: t_n ::
- wf(h, m, sm) && CanAssumeFunctionDefs ==> Q[#C.f(h, m, this, x_1, ..., x_n)/result]
+ wf(h, m, sm) && (CanAssumeFunctionDefs || f.height < FunctionContextHeight) ==> Q[#C.f(h, m, this, x_1, ..., x_n)/result]
*/
val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)});
val myresult = Boogie.BVar("result", f.out.typ);
val args = VarExpr("this") :: inArgs;
val applyF = FunctionApp(functionName(f), List(VarExpr(HeapName)) ::: args)
+ val canCall = FunctionApp(functionName(f) + "#canCall", args)
val wellformed = wf(VarExpr(HeapName), VarExpr(MaskName), VarExpr(SecMaskName))
//postcondition axioms
@@ -327,7 +398,7 @@ class Translator { Axiom(new Boogie.Forall(
BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar(SecMaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar),
new Trigger(List(applyF, wellformed)),
- (wellformed && CanAssumeFunctionDefs)
+ (wellformed && (CanAssumeFunctionDefs || f.height < FunctionContextHeight || canCall))
==>
etran.Tr(SubstResult(post, f.apply(ExplicitThisExpr(), f.ins map { arg => new VariableExpr(arg) })))
))
@@ -342,6 +413,7 @@ class Translator { // const unique class.name: HeapType;
Const(pred.FullName, true, FieldType(tint)) ::
+ Const(pred.FullName+"#m", true, FieldType(tpmask)) ::
// axiom PredicateField(f);
Axiom(PredicateField(pred.FullName)) ::
// trigger function to unfold function definitions
@@ -476,10 +548,13 @@ class Translator { new Boogie.Forall(chV, (ch ==@ bnull) || (0 <= new MapSelect(etran.Credits, ch)))
}
- def DefaultPrecondition() = {
- "requires this!=null;" ::
- "free requires wf(Heap, Mask, SecMask);" ::
- Nil
+ def DefaultPrecondition(isStatic: Boolean = false) = {
+ if (!isStatic) {
+ "requires this!=null;" ::
+ "free requires wf(Heap, Mask, SecMask);" :: Nil
+ } else {
+ "free requires wf(Heap, Mask, SecMask);" :: Nil
+ }
}
def DefinePreInitialState = {
@@ -487,11 +562,14 @@ class Translator { (etran.Mask := ZeroMask) :: (etran.SecMask := ZeroMask) :: (etran.Credits := ZeroCredits)
}
def DefineInitialState = {
+ val (refV, ref) = Boogie.NewBVar("ref", tref, true)
+ val (pmaskV, pmask) = Boogie.NewBVar("pmask", FieldType(tpmask), true)
Comment("define initial state") ::
bassume(etran.Heap ==@ Boogie.Old(etran.Heap)) ::
bassume(etran.Mask ==@ Boogie.Old(etran.Mask)) ::
bassume(etran.SecMask ==@ Boogie.Old(etran.SecMask)) ::
- bassume(etran.Credits ==@ Boogie.Old(etran.Credits))
+ bassume(etran.Credits ==@ Boogie.Old(etran.Credits)) ::
+ bassume((etran.Heap.select(ref, pmask.id) ==@ ZeroPMask).forall(refV).forall(pmaskV))
}
/**********************************************************************
@@ -696,11 +774,12 @@ class Translator { isDefined(perm) :::
bassert(nonNull(o), s.pos, "The target of the fold statement might be null.") ::
// remove the definition from the current state, and replace by predicate itself
- etran.ExhaleAndTransferToSecMask(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) :::
BLocal(receiverV) :: (receiver := o) ::
BLocal(versionV) :: (version := etran.Heap.select(o, pred.predicate.FullName)) ::
BLocal(flagV) :: (flag := true) ::
+ etran.ExhaleAndTransferToSecMask(o, pred.predicate, List((definition, ErrorMessage(s.pos, "Fold might fail because the definition of " + pred.predicate.FullName + " does not hold."))), "fold", foldK, false, receiver, pred.predicate.FullName, version) :::
+ Inhale(List(acc), "fold", foldK) :::
+ etran.keepFoldedLocations(definition, o, pred.predicate, etran.Mask, etran.Heap, etran.fpi.getFoldedPredicates(pred.predicate)) :::
bassume(wf(etran.Heap, etran.Mask, etran.SecMask))
// record folded predicate
@@ -713,14 +792,19 @@ class Translator { // pick new k
val (unfoldKV, unfoldK) = Boogie.NewBVar("unfoldK", tint, true)
+ // record version of unfolded instance
+ val (receiverV, receiver) = Boogie.NewBVar("predRec", tref, true)
+ val (versionV, version) = Boogie.NewBVar("predVer", tint, true)
Comment("unfold") ::
functionTrigger(o, pred.predicate) ::
+ BLocal(receiverV) :: (receiver := o) ::
+ BLocal(versionV) :: (version := etran.Heap.select(o, pred.predicate.FullName)) ::
BLocal(unfoldKV) :: bassume(0 < unfoldK && unfoldK < percentPermission(1) && 1000*unfoldK < methodK) ::
isDefined(e) :::
bassert(nonNull(o), s.pos, "The target of the fold statement might be null.") ::
isDefined(perm) :::
ExhaleDuringUnfold(List((acc, ErrorMessage(s.pos, "unfold might fail because the predicate " + pred.predicate.FullName + " does not hold."))), "unfold", unfoldK, false) :::
- etran.Inhale(List(definition), "unfold", false, unfoldK)
+ etran.Inhale(List(definition), "unfold", false, unfoldK, receiver, pred.predicate.FullName, version)
case c@CallAsync(declaresLocal, token, obj, id, args) =>
val formalThisV = new Variable("this", new Type(c.m.Parent))
val formalThis = new VariableExpr(formalThisV)
@@ -1475,11 +1559,21 @@ class FoldedPredicatesInfo { foldedPredicates filter (fp => fp.predicate.FullName == predicate.FullName)
}
+ /** return a list of all folded predicates */
+ def getFoldedPredicates(): List[FoldedPredicate] = {
+ foldedPredicates
+ }
+
/** get an upper bound on the recursion depth when updating the secondary mask */
def getRecursionBound(predicate: Predicate): Int = {
foldedPredicates length
}
+ /** get an upper bound on the recursion depth when updating the secondary mask */
+ def getRecursionBound(): Int = {
+ foldedPredicates length
+ }
+
}
object FoldedPredicatesInfo {
def apply() = new FoldedPredicatesInfo()
@@ -1605,17 +1699,23 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F // pick new k
val (funcappKV, funcappK) = Boogie.NewBVar("funcappK", tint, true)
- // check definedness of receiver + arguments
- (obj :: args flatMap { arg => isDefined(arg) }) :::
+ // check definedness of receiver
+ (if (!func.f.isStatic) {
+ isDefined(obj)
+ } else Nil) :::
+ // check definedness of arguments
+ (args flatMap { arg => isDefined(arg) }) :::
// check that receiver is not null
- List(prove(nonNull(Tr(obj)), obj.pos, "Receiver might be null.")) :::
+ (if (!func.f.isStatic) {
+ List(prove(nonNull(Tr(obj)), obj.pos, "Receiver might be null."))
+ } else Nil) :::
// 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 < percentPermission(1)) ::
bassume(assumption) ::
BLocals(tmpGlobalsV) :::
copyState(tmpGlobals, this) :::
- 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."))},
+ tmpTranslator.Exhale(Preconditions(func.f.spec) map { pre=> (if (func.f.isStatic) SubstVars(pre, func.f.ins, args) else SubstVars(pre, obj, func.f.ins, args), ErrorMessage(func.pos, "Precondition at " + pre.pos + " might not hold."))},
"function call",
false, funcappK, false) :::
// size of the heap of callee must be strictly smaller than size of the heap of the caller
@@ -1631,10 +1731,15 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F // pick new k
val (unfoldingKV, unfoldingK) = Boogie.NewBVar("unfoldingK", tint, true)
-
+ // record version of unfolded instance
+ val (receiverV, receiver) = Boogie.NewBVar("predRec", tref, true)
+ val (versionV, version) = Boogie.NewBVar("predVer", tint, true)
+
val res = Comment("unfolding") ::
BLocal(unfoldingKV) :: bassume(0 < unfoldingK && 1000*unfoldingK < percentPermission(1)) ::
BLocal(flagV) :: (flag := true) ::
+ BLocal(receiverV) :: (receiver := o) ::
+ BLocal(versionV) :: (version := etran.Heap.select(o, pred.predicate.FullName)) :::
// check definedness
receiverOk ::: isDefined(perm) :::
// copy state into temporary variables
@@ -1643,16 +1748,16 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F // exhale the predicate
tmpTranslator.ExhaleDuringUnfold(List((acc, ErrorMessage(unfolding.pos, "Unfolding might fail."))), "unfolding", false, unfoldingK, false) :::
// inhale the definition of the predicate
- tmpTranslator.Inhale(List(definition), "unfolding", false, unfoldingK) :::
- // remove secondary permissions (if any), and add them again
- (if (isOldEtran) Nil else
- UpdateSecMaskDuringUnfold(pred.predicate, Tr(obj), Heap.select(Tr(obj), pred.predicate.FullName), perm, unfoldingK) :::
- TransferPermissionToSecMask(pred.predicate, obj, perm, unfolding.pos)) :::
+ tmpTranslator.Inhale(List(definition), "unfolding", false, unfoldingK, receiver, pred.predicate.FullName, version) :::
+ // update the predicate mask to indicate the predicates that are folded under 'pred'
+ (if (isOldEtran) Nil
+ else etran.keepFoldedLocations(definition, o, pred.predicate, etran.Mask, etran.Heap, etran.fpi.getFoldedPredicates(pred.predicate))) :::
// check definedness of e in state where the predicate is unfolded
- tmpTranslator.isDefined(e)
+ tmpTranslator.isDefined(e) :::
+ bassume(wf(etran.Heap, etran.Mask, etran.SecMask)) :: Nil
// record folded predicate
- val version = Heap.select(o, pred.predicate.FullName)
+ //val version = Heap.select(o, pred.predicate.FullName)
if (!isOldEtran) fpi.addFoldedPredicate(FoldedPredicate(pred.predicate, o, version, fpi.currentConditions, flag))
res
@@ -1729,140 +1834,359 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F * the expression and an expression translator as argument). The default
* behaviour is to translate only pure assertions (and throw and error otherwise).
*/
- def Tr(e: Expression): Boogie.Expr = Tr(e, (ee,et) => et.Tr(ee))
- def Tr(e: Expression, trrec: (Expression, ExpressionTranslator) => Expr): Boogie.Expr = {
- def trrecursive(e: Expression): Expr = trrec(e, this)
+ def Tr(e: Expression): Boogie.Expr = (Tr(e,false))._1
+ def Tr(e: Expression, listNeeded: Boolean) : (Boogie.Expr, List[Boogie.Stmt]) = (Tr(e, (ee,et) => et.Tr(ee,listNeeded), listNeeded))
+ def Tr(e: Expression, trrec: (Expression, ExpressionTranslator) => (Boogie.Expr, List[Boogie.Stmt]), listNeeded: Boolean = false): (Boogie.Expr, List[Boogie.Stmt]) = {
+ def trrecursive(e: Expression): (Boogie.Expr, List[Boogie.Stmt]) = trrec(e, this)
desugar(e) match {
- case IntLiteral(n) => n
- case BoolLiteral(b) => b
- case NullLiteral() => bnull
+ case IntLiteral(n) => (n,Nil)
+ case BoolLiteral(b) => (b,Nil)
+ case NullLiteral() => (bnull,Nil)
case StringLiteral(s) =>
// since there currently are no operations defined on string, except == and !=, just translate
// each string to a unique number
- s.hashCode()
- case BoogieExpr(b) => b
+ (s.hashCode(),Nil)
+ case BoogieExpr(b) => (b,Nil)
case MaxLockLiteral() => throw new InternalErrorException("waitlevel case should be handled in << and == and !=")
- case LockBottomLiteral() => bLockBottom
- case _:ThisExpr => VarExpr("this")
- case _:Result => VarExpr("result")
- case ve : VariableExpr => VarExpr(ve.v.UniqueName)
+ case LockBottomLiteral() => (bLockBottom,Nil)
+ case _:ThisExpr => (VarExpr("this"),Nil)
+ case _:Result => (VarExpr("result"),Nil)
+ case ve : VariableExpr => (VarExpr(ve.v.UniqueName),Nil)
case fs @ MemberAccess(e,_) =>
assert(! fs.isPredicate);
- var r = Heap.select(trrecursive(e), fs.f.FullName);
+ var (ee,ll) = trrecursive(e)
+ var r = Heap.select(ee, fs.f.FullName);
if (fs.f.isInstanceOf[SpecialField] && fs.f.id == "joinable")
- r !=@ 0 // joinable is encoded as an integer
+ (r !=@ 0,ll) // joinable is encoded as an integer
else
- r
+ (r,ll)
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) =>
- var ee = trrecursive(e)
- (0 < Heap.select(ee, "held")) &&
- !Heap.select(ee, "rdheld")
+ var (ee,ll) = trrecursive(e)
+ ((0 < Heap.select(ee, "held")) &&
+ !Heap.select(ee, "rdheld"),ll)
case RdHolds(e) =>
- Heap.select(trrecursive(e), "rdheld")
+ var (ee,ll) = trrecursive(e)
+ (Heap.select(ee, "rdheld"),ll)
case a: Assigned =>
- VarExpr("assigned$" + a.v.UniqueName)
+ (VarExpr("assigned$" + a.v.UniqueName),Nil)
case Old(e) =>
trrec(e, oldEtran)
case IfThenElse(con, then, els) =>
- Boogie.Ite(trrecursive(con), trrecursive(then), trrecursive(els)) // of type: VarExpr(TrClass(then.typ))
+ var (conE,conL) = trrecursive(con)
+ var (thenE,thenL) = trrecursive(then)
+ var (elsE,elsL) = trrecursive(els)
+ (Boogie.Ite(conE, thenE, elsE), (if (listNeeded) (conL ::: thenL ::: elsL) else Nil)) // of type: VarExpr(TrClass(then.typ))
case Not(e) =>
- ! trrecursive(e)
- case func@FunctionApplication(obj, id, args) =>
- FunctionApp(functionName(func.f), Heap :: (obj :: args map { arg => trrecursive(arg)}))
- case uf@Unfolding(_, e) =>
- trrecursive(e)
+ var (ee,ll) = trrecursive(e)
+ ((! ee),ll)
+ case func@FunctionApplication(obj, id, args) => {
+ var fullArgs = if (!func.f.isStatic) (obj :: args) else (args)
+ var trArgs = fullArgs map {arg => trrecursive(arg)} // yields a list of (Expr, List[Boogie.Stmt]) pairs
+ var trArgsE = trArgs.foldRight(List[Boogie.Expr]())((el, ll) => el._1 :: ll) // collect list of exprs
+ var trArgsL = if (listNeeded) (trArgs.foldRight(List[Boogie.Stmt]())((x,y) => ((x._2) ::: y))) else Nil // concatenate lists of statements
+ (FunctionApp(functionName(func.f), Heap :: trArgsE),trArgsL)
+ }
+ case uf@Unfolding(acc@Access(pred@MemberAccess(obj, f), perm), ufexpr) =>
+ // record extra information resulting from "peeking inside" the predicate, generating appropriate statements (this is used in Exhale of an expression)
+ val (ee,ll) = trrecursive(ufexpr)
+ val (receiverV, receiver) = Boogie.NewBVar("predRec", tref, true)
+ val (versionV, version) = Boogie.NewBVar("predVer", tint, true)
+ val (flagV, flag) = Boogie.NewBVar("predFlag", tbool, true)
+ val o = TrExpr(obj);
+
+ val stmts = if (listNeeded) (BLocal(receiverV) :: (receiver := o) ::
+ BLocal(flagV) :: (flag := true) ::
+ functionTrigger(o, pred.predicate) ::
+ BLocal(versionV) :: (version := Heap.select(o, pred.predicate.FullName)) :::
+ // UpdateSecMaskDuringUnfold(pred.predicate, o, Heap.select(o, pred.predicate.FullName), perm, currentK) :::
+ TransferPermissionToSecMask(pred.predicate, BoogieExpr(receiver), perm, uf.pos, receiver, pred.predicate.FullName, version)) else Nil
+
+ (ee, ll ::: stmts)
case Iff(e0,e1) =>
- trrecursive(e0) <==> trrecursive(e1)
+ var (ee0,l0) = trrecursive(e0)
+ var (ee1,l1) = trrecursive(e1)
+ ((ee0 <==> ee1), if (listNeeded) (l0 ::: l1) else Nil)
case Implies(e0,e1) =>
- trrecursive(e0) ==> trrecursive(e1)
+ var (ee0,l0) = trrecursive(e0)
+ var (ee1,l1) = trrecursive(e1)
+ ((ee0 ==> ee1), if (listNeeded) (l0 ::: l1) else Nil)
case And(e0,e1) =>
- trrecursive(e0) && trrecursive(e1)
+ var (ee0,l0) = trrecursive(e0)
+ var (ee1,l1) = trrecursive(e1)
+ ((ee0 && ee1), if (listNeeded) (l0 ::: l1) else Nil)
case Or(e0,e1) =>
- trrecursive(e0) || trrecursive(e1)
+ var (ee0,l0) = trrecursive(e0)
+ var (ee1,l1) = trrecursive(e1)
+ ((ee0 || ee1), if (listNeeded) (l0 ::: l1) else Nil)
case Eq(e0,e1) =>
(ShaveOffOld(e0), ShaveOffOld(e1)) match {
case ((MaxLockLiteral(),o0), (MaxLockLiteral(),o1)) =>
if (o0 == o1)
- true
+ (true, Nil) // in this case, l0 and l1 would be Nil, (and Tr((MaxLockLiteral(),_)) is not defined)
else
- MaxLockPreserved
- case ((MaxLockLiteral(),o), _) => ChooseEtran(o).IsHighestLock(trrecursive(e1))
- case (_, (MaxLockLiteral(),o)) => ChooseEtran(o).IsHighestLock(trrecursive(e0))
- case _ => if(e0.typ.IsSeq) FunctionApp("Seq#Equal", List(trrecursive(e0), trrecursive(e1))) else (trrecursive(e0) ==@ trrecursive(e1))
+ (MaxLockPreserved, Nil) // in this case, l0 and l1 would be Nil, (and Tr((MaxLockLiteral(),_)) is not defined)
+ case ((MaxLockLiteral(),o), _) =>
+ var (ee1,l1) = trrecursive(e1)
+ (ChooseEtran(o).IsHighestLock(ee1), l1) // in this case, l0 would be Nil, (and Tr((MaxLockLiteral(),_)) is not defined)
+ case (_, (MaxLockLiteral(),o)) =>
+ var (ee0,l0) = trrecursive(e0)
+ (ChooseEtran(o).IsHighestLock(ee0), l0) // in this case, l1 would be Nil, (and Tr((MaxLockLiteral(),_)) is not defined)
+ case _ =>
+ var (ee0,l0) = trrecursive(e0)
+ var (ee1,l1) = trrecursive(e1)
+ ((if(e0.typ.IsSeq) FunctionApp("Seq#Equal", List(ee0, ee1)) else (ee0 ==@ ee1)), if (listNeeded) (l0 ::: l1) else Nil)
}
case Neq(e0,e1) =>
trrecursive(Not(Eq(e0,e1)))
case Less(e0,e1) =>
- trrecursive(e0) < trrecursive(e1)
+ var (ee0,l0) = trrecursive(e0)
+ var (ee1,l1) = trrecursive(e1)
+ (ee0 < ee1, if (listNeeded) (l0 ::: l1) else Nil)
case AtMost(e0,e1) =>
- trrecursive(e0) <= trrecursive(e1)
+ var (ee0,l0) = trrecursive(e0)
+ var (ee1,l1) = trrecursive(e1)
+ (ee0 <= ee1, if (listNeeded) (l0 ::: l1) else Nil)
case AtLeast(e0,e1) =>
- trrecursive(e0) >= trrecursive(e1)
+ var (ee0,l0) = trrecursive(e0)
+ var (ee1,l1) = trrecursive(e1)
+ (ee0 >= ee1, if (listNeeded) (l0 ::: l1) else Nil)
case Greater(e0,e1) =>
- trrecursive(e0) > trrecursive(e1)
+ var (ee0,l0) = trrecursive(e0)
+ var (ee1,l1) = trrecursive(e1)
+ (ee0 > ee1, if (listNeeded) (l0 ::: l1) else Nil)
case LockBelow(e0,e1) => {
- def MuValue(b: Expression): Boogie.Expr =
- if (b.typ.IsRef) new Boogie.MapSelect(Heap, trrecursive(b), "mu") else trrecursive(b)
+ def MuValue(b: Expression): (Boogie.Expr, List[Boogie.Stmt]) = (
+ trrecursive(b) match {
+ case (eb, lb) =>
+ ((if (b.typ.IsRef) new Boogie.MapSelect(Heap, eb, "mu") else eb),lb)
+ }
+ )
(ShaveOffOld(e0), ShaveOffOld(e1)) match {
case ((MaxLockLiteral(),o0), (MaxLockLiteral(),o1)) =>
if (o0 == o1)
- false
+ (false,Nil) // in this case, l0 and l1 are guaranteed to be Nil
else
- TemporalMaxLockComparison(ChooseEtran(o0), ChooseEtran(o1))
- case ((MaxLockLiteral(),o), _) => ChooseEtran(o).MaxLockIsBelowX(MuValue(e1))
- case (_, (MaxLockLiteral(),o)) => ChooseEtran(o).MaxLockIsAboveX(MuValue(e0))
- case _ => new FunctionApp("MuBelow", MuValue(e0), MuValue(e1)) }
+ (TemporalMaxLockComparison(ChooseEtran(o0), ChooseEtran(o1)),Nil) // in this case, l0 and l1 are guaranteed to be Nil
+ case ((MaxLockLiteral(),o), _) =>
+ var (ee1, l1) = MuValue(e1)
+ (ChooseEtran(o).MaxLockIsBelowX(ee1),l1)
+ case (_, (MaxLockLiteral(),o)) =>
+ var (ee0, l0) = MuValue(e0)
+ (ChooseEtran(o).MaxLockIsAboveX(ee0),l0)
+ case _ =>
+ var (ee0, l0) = MuValue(e0)
+ var (ee1, l1) = MuValue(e1)
+ ((new FunctionApp("MuBelow", ee0, ee1)), if (listNeeded) (l0 ::: l1) else Nil) }
}
case Plus(e0,e1) =>
- trrecursive(e0) + trrecursive(e1)
+ var (ee0,l0) = trrecursive(e0)
+ var (ee1,l1) = trrecursive(e1)
+ (ee0 + ee1, if (listNeeded) (l0 ::: l1) else Nil)
case Minus(e0,e1) =>
- trrecursive(e0) - trrecursive(e1)
+ var (ee0,l0) = trrecursive(e0)
+ var (ee1,l1) = trrecursive(e1)
+ (ee0 - ee1, if (listNeeded) (l0 ::: l1) else Nil)
case Times(e0,e1) =>
- trrecursive(e0) * trrecursive(e1)
+ var (ee0,l0) = trrecursive(e0)
+ var (ee1,l1) = trrecursive(e1)
+ (ee0 * ee1, if (listNeeded) (l0 ::: l1) else Nil)
case Div(e0,e1) =>
- trrecursive(e0) / trrecursive(e1)
+ var (ee0,l0) = trrecursive(e0)
+ var (ee1,l1) = trrecursive(e1)
+ (ee0 / ee1, if (listNeeded) (l0 ::: l1) else Nil)
case Mod(e0,e1) =>
- trrecursive(e0) % trrecursive(e1)
+ var (ee0,l0) = trrecursive(e0)
+ var (ee1,l1) = trrecursive(e1)
+ (ee0 % ee1, if (listNeeded) (l0 ::: l1) else Nil)
case EmptySeq(t) =>
- createEmptySeq
+ (createEmptySeq, Nil)
case ExplicitSeq(es) =>
es match {
- case Nil => createEmptySeq
- case h :: Nil => createSingletonSeq(trrecursive(h))
- case h :: t => createAppendSeq(createSingletonSeq(trrecursive(h)), trrecursive(ExplicitSeq(t)))
+ case Nil => (createEmptySeq, Nil)
+ case h :: Nil =>
+ var (eh,lh) = trrecursive(h)
+ (createSingletonSeq(eh),lh)
+ case h :: t =>
+ var (eh,lh) = trrecursive(h)
+ var (et,lt) = trrecursive(ExplicitSeq(t))
+ ((createAppendSeq(createSingletonSeq(eh), et)), if (listNeeded) (lh ::: lt) else Nil)
}
case Range(min, max) =>
- createRange(trrecursive(min), trrecursive(max))
+ var (emin,lmin) = trrecursive(min)
+ var (emax,lmax) = trrecursive(max)
+ ((createRange(emin, emax)), if (listNeeded) (lmin ::: lmax) else Nil)
case Append(e0, e1) =>
- createAppendSeq(trrecursive(e0), trrecursive(e1))
- case at@At(e0, e1) =>SeqIndex(trrecursive(e0), trrecursive(e1))
+ var (ee0,l0) = trrecursive(e0)
+ var (ee1,l1) = trrecursive(e1)
+ ((createAppendSeq(ee0, ee1)), if (listNeeded) (l0 ::: l1) else Nil)
+ case at@At(e0, e1) =>
+ var (ee0,l0) = trrecursive(e0)
+ var (ee1,l1) = trrecursive(e1)
+ ((SeqIndex(ee0, ee1)), if (listNeeded) (l0 ::: l1) else Nil)
case Drop(e0, e1) =>
+ var (ee0,l0) = trrecursive(e0)
+ var (ee1,l1) = trrecursive(e1)
e1 match {
case IntLiteral(0) =>
- trrecursive(e0)
+ (ee0, if (listNeeded) (l0 ::: l1) else Nil)
case _ =>
- Boogie.FunctionApp("Seq#Drop", List(trrecursive(e0), trrecursive(e1)))
+ ((Boogie.FunctionApp("Seq#Drop", List(ee0, ee1))), if (listNeeded) (l0 ::: l1) else Nil)
}
case Take(e0, e1) =>
- Boogie.FunctionApp("Seq#Take", List(trrecursive(e0), trrecursive(e1)))
- case Length(e) => SeqLength(trrecursive(e))
- case Contains(e0, e1) => SeqContains(trrecursive(e1), trrecursive(e0))
+ var (ee0,l0) = trrecursive(e0)
+ var (ee1,l1) = trrecursive(e1)
+ ((Boogie.FunctionApp("Seq#Take", List(ee0, ee1))), if (listNeeded) (l0 ::: l1) else Nil)
+ case Length(e) =>
+ var (ee,l) = trrecursive(e)
+ (SeqLength(ee), l)
+ case Contains(e0, e1) =>
+ var (ee0,l0) = trrecursive(e0)
+ var (ee1,l1) = trrecursive(e1)
+ (SeqContains(ee1, ee0), if (listNeeded) (l0 ::: l1) else Nil) // Note: swapping of arguments
case Eval(h, e) =>
val (evalHeap, evalMask, evalSecMask, evalCredits, checks, assumptions) = fromEvalState(h);
val evalEtran = new ExpressionTranslator(Globals(evalHeap, evalMask, evalSecMask, evalCredits), oldEtran.globals, currentClass);
trrec(e, evalEtran)
case _:SeqQuantification => throw new InternalErrorException("should be desugared")
case tq @ TypeQuantification(Forall, _, _, e, _) =>
- Boogie.Forall(Nil, tq.variables map { v => Variable2BVar(v)}, Nil, trrecursive(e))
+ val(ee,l) = trrecursive(e)
+ val groupedTriggerSets = generateTriggers(tq.variables,e)
+ val oneQuantifier : (((List[Trigger],List[Variable])) => Boogie.Expr) = ((trigsAndExtraVars) => (Boogie.Forall(Nil, (tq.variables ::: trigsAndExtraVars._2) map { v => Variable2BVar(v)}, trigsAndExtraVars._1, ee)))
+ var firstTriggerSet : (List[Trigger],List[Variable]) = (Nil,Nil);
+ var restTriggerSet : List[(List[Trigger],List[Variable])] = Nil;
+
+ groupedTriggerSets match {
+ case Nil =>
+ firstTriggerSet = (Nil,Nil); // we will generate no triggers for this quantifier
+ restTriggerSet = Nil
+ case ts :: rest =>
+ firstTriggerSet = ts;
+ restTriggerSet = rest
+ }
+ (restTriggerSet.foldRight(oneQuantifier(firstTriggerSet))((trigset,expr) => (oneQuantifier(trigset) && expr)),l)
case tq @ TypeQuantification(Exists, _, _, e, _) =>
- Boogie.Exists(Nil, tq.variables map { v => Variable2BVar(v)}, Nil, trrecursive(e))
+ var (ee,l) = trrecursive(e)
+ ((Boogie.Exists(Nil, tq.variables map { v => Variable2BVar(v)}, Nil, ee)),l)
}
}
+ // This is used for searching for triggers for quantifiers around the expression "toSearch". The list "vs" gives the variables which need triggering
+ // Returns a list of function applications (the framing function) paired with two sets of variables.
+ // The first set of variables shows which of the "vs" occur (useful for deciding how to select applications for trigger sets later)
+ // The second set of variables indicated the extra boolean variables which were introduced to "hide" problematic logical/comparison operators which may not occur in triggers.
+ // e.g., if vs = [x] and toSearch = f(x, y ==> z) then a singleton list will be returned, containing (f(x,b),{x},{b}).
+ def getFunctionAppsContaining(vs:List[Variable], toSearch : Expression): (List[(Boogie.FunctionApp,Set[Variable],Set[Variable])]) = {
+ var functions: List[(Boogie.FunctionApp,Set[Variable],Set[Variable])] = List() // accumulate candidate functions to return
+ var nestedBoundVars : List[Variable] = List(); // count all variables bound in nested quantifiers, to avoid considering function applications mentioning these
+
+ // get all nested bound vars
+ toSearch visit {
+ _ match {
+ case qe : Quantification =>
+ nestedBoundVars :::= qe.variables
+ case _ =>
+ }
+ }
+
+ // get all function applications
+ toSearch visit {
+ _ match {
+ case fapp@FunctionApplication(obj, id, args) =>
+ var extraVars : Set[Variable] = Set() // collect extra variables generated for this term
+ var containsNestedBoundVars = false // flag to rule out this term
+ // closure to generate fresh boolean variable
+ val freshBoolVar : (() => Option[Expression]) = {() =>
+ val newV = new Variable("b", new Type(BoolClass))
+ extraVars += newV;
+ Some(new VariableExpr(newV))
+ }
+ // replaces problematic logical/comparison expressions with fresh boolean variables
+ val boolExprEliminator : (Expression => Option[Expression]) = ((expr:Expression) =>
+ expr match {
+ case exp@Not(e) => freshBoolVar()
+ case exp@Iff(e0,e1) => freshBoolVar()
+ case exp@Implies(e0,e1) => freshBoolVar()
+ case exp@And(e0,e1) => freshBoolVar()
+ case exp@Or(e0,e1) => freshBoolVar()
+ case Eq(e0,e1) => freshBoolVar()
+ case Neq(e0,e1) => freshBoolVar()
+ case Less(e0,e1) => freshBoolVar()
+ case AtMost(e0,e1) => freshBoolVar()
+ case AtLeast(e0,e1) => freshBoolVar()
+ case Greater(e0,e1) => freshBoolVar()
+ case _ => None
+ });
+ var containedVars : Set[Variable] = Set()
+ val processedArgs = args map (_.transform(boolExprEliminator)) // eliminate all boolean expressions forbidden from triggers, and replace with "extraVars"
+ // collect all the sought (vs) variables in the function application
+ processedArgs map {e => e visit {_ match {
+ case ve@VariableExpr(s) =>
+ val v : Variable = ve.v
+ if (nestedBoundVars.contains(v)) (containsNestedBoundVars = true);
+ if (vs.contains(v)) (containedVars += v)
+ case _ =>}
+ }
+ }
+ if (!containsNestedBoundVars && !containedVars.isEmpty) {
+ val fullArgs = if (!fapp.f.isStatic) (obj :: processedArgs) else (processedArgs)
+ val noOldETran = this.UseCurrentAsOld();
+ val trArgs = fullArgs map {arg => noOldETran.Tr(arg)} // translate args
+ val precs = Preconditions(fapp.f.spec) map (p => SubstVars(p, obj, fapp.f.ins, processedArgs))
+ val pre = precs.foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b) });
+ val partialHeap = functionDependencies(pre, etran);
+ val frameFunctionName = "#" + functionName(fapp.f);
+ functions ::= (FunctionApp(frameFunctionName, partialHeap :: trArgs),containedVars,extraVars)
+ }
+ case _ =>}
+ }
+ functions
+ }
+
+
+
+
+ // Precondition : if vars is non-empty then every (f,vs) pair in functs satisfies the property that vars and vs are not disjoint.
+ // Finds trigger sets by selecting entries from "functs" until all of "vars" occur, and accumulating the extra variables needed for each function term.
+ // Returns a list of the trigger sets found, paired with the extra boolean variables they use
+def buildTriggersCovering(vars : Set[Variable], functs : List[(Boogie.FunctionApp,Set[Variable],Set[Variable])], currentTrigger : List[Expr], extraVars : Set[Variable]) : List[(Trigger,Set[Variable])] = {
+ if (vars.isEmpty) (List((Boogie.Trigger(currentTrigger),extraVars))) // we have found a suitable trigger set
+ else (functs match {
+ case Nil => Nil // this branch didn't result in a solution
+ case ((f,vs,extra) :: rest) => {
+ val needed : Set[Variable] = vars.diff(vs) // variables still not triggered
+ // try adding the next element of functs, or not..
+ buildTriggersCovering(needed, (rest.filter(func => !func._2.intersect(needed).isEmpty)), f :: currentTrigger, extraVars|extra) ::: buildTriggersCovering(vars, rest, currentTrigger, extraVars)
+ }
+ }
+ )
+ }
+
+
+ // Generates trigger sets to cover the variables "vs", by searching the expression "toSearch".
+ // Returns a list of pairs of lists of trigger sets couple with the extra variables they require to be quantified over (each list of triggers must contain trigger sets which employ exactly the same extra variables).
+ def generateTriggers(vs: List[Variable], toSearch : Expression) : List[(List[Trigger],List[Variable])] = {
+ val functionApps : (List[(Boogie.FunctionApp,Set[Variable],Set[Variable])]) = getFunctionAppsContaining(vs, toSearch) // find suitable function applications
+ if (functionApps.isEmpty) List() else {
+ var triggerSetsToUse : List[(Trigger,Set[Variable])] = buildTriggersCovering(Set() ++ vs, functionApps, Nil, Set())
+ var groupedTriggerSets : List[(List[Trigger],List[Variable])] = List() // group trigger sets by those which use the same sets of extra boolean variables
+
+ while (!triggerSetsToUse.isEmpty) {
+ triggerSetsToUse.partition((ts : (Trigger,Set[Variable])) => triggerSetsToUse.head._2.equals(ts._2)) match {
+ case (sameVars,rest) =>
+ triggerSetsToUse = rest;
+ groupedTriggerSets ::= ((sameVars map (_._1)), sameVars.head._2.toList)
+ }
+ }
+ groupedTriggerSets
+ }
+ }
+
+
/** translate everything, including permissions and credit expressions */
+ // Since this is only used in axiom generation (so far), the ability to generate "side-effects" from the evaluation of unfolding expressions (as in the list of boogie statements returned from Tr) is not implemented here (in axioms the side-effects are not wanted anyway)
def TrAll(e: Expression): Expr = {
def TrAllHelper(e: Expression, etran: ExpressionTranslator): Expr = e match {
case pred@MemberAccess(e, p) if pred.isPredicate =>
@@ -1876,7 +2200,7 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F val memberName = member.f.FullName;
val (refV, ref) = Boogie.NewBVar("ref", tref, true);
(SeqContains(Tr(s), ref) ==> CanRead(ref, memberName)).forall(refV)
- case _ => etran.Tr(e, TrAllHelper)
+ case _ => (etran.Tr(e, (ee : Expression, et : ExpressionTranslator) => (TrAllHelper(ee,et),Nil)))._1 //wrap TrAllHelper to give it the return type needed for Tr.
}
TrAllHelper(e, this)
}
@@ -1896,14 +2220,14 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F ***************** INHALE/EXHALE *****************
**********************************************************************/
- def Inhale(predicates: List[Expression], occasion: String, check: Boolean, currentK: Expr): List[Boogie.Stmt] = {
+ def Inhale(predicates: List[Expression], occasion: String, check: Boolean, currentK: Expr, unfoldReceiver: VarExpr = null, unfoldPredicateName: String = null, unfoldVersion: VarExpr = null): 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, SecMask)) ::
- (for (p <- predicates) yield Inhale(p, Heap, check, currentK)).flatten :::
+ (for (p <- predicates) yield Inhale(p, Heap, check, currentK, unfoldReceiver, unfoldPredicateName, unfoldVersion)).flatten :::
bassume(AreGoodMasks(Mask, SecMask)) ::
bassume(wf(Heap, Mask, SecMask)) ::
Comment("end inhale")
@@ -1929,13 +2253,13 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F })
}
- def Inhale(p: Expression, ih: Boogie.Expr, check: Boolean, currentK: Expr): List[Boogie.Stmt] =
- InhaleImplementation(p, ih, check, currentK, false)
+ def Inhale(p: Expression, ih: Boogie.Expr, check: Boolean, currentK: Expr, unfoldReceiver: VarExpr, unfoldPredicateName : String, unfoldVersion: VarExpr): List[Boogie.Stmt] =
+ InhaleImplementation(p, ih, check, currentK, false, unfoldReceiver, unfoldPredicateName, unfoldVersion)
- def InhaleToSecMask(p: Expression): List[Boogie.Stmt] =
- InhaleImplementation(p, Heap /* it should not matter what we pass here */, false /* check */, -1 /* it should not matter what we pass here */, true)
+ def InhaleToSecMask(p: Expression, unfoldingReceiver: VarExpr = null, unfoldingPredicateName: String = null, unfoldingVersion: VarExpr = null): List[Boogie.Stmt] =
+ InhaleImplementation(p, Heap /* it should not matter what we pass here */, false /* check */, -1 /* it should not matter what we pass here */, true, unfoldingReceiver, unfoldingPredicateName, unfoldingVersion)
- def InhaleImplementation(p: Expression, ih: Boogie.Expr, check: Boolean, currentK: Expr, transferToSecMask: Boolean): List[Boogie.Stmt] = desugar(p) match {
+ def InhaleImplementation(p: Expression, ih: Boogie.Expr, check: Boolean, currentK: Expr, transferToSecMask: Boolean, unfoldReceiver: VarExpr = null, unfoldPredicateName: String = null, unfoldVersion: VarExpr = null): List[Boogie.Stmt] = desugar(p) match {
case pred@MemberAccess(e, p) if pred.isPredicate =>
val chk = (if (check) {
isDefined(e)(true) :::
@@ -1943,7 +2267,7 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F } else Nil)
val tmp = Access(pred, Full);
tmp.pos = pred.pos;
- chk ::: InhaleImplementation(tmp, ih, check, currentK, transferToSecMask)
+ chk ::: InhaleImplementation(tmp, ih, check, currentK, transferToSecMask, unfoldReceiver, unfoldPredicateName, unfoldVersion)
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) =>
@@ -1958,6 +2282,8 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F bassume(wf(Heap, Mask, SecMask)) ::
(if(e.isPredicate) Nil else List(bassume(TypeInformation(new Boogie.MapSelect(Heap, trE, memberName), e.f.typ.typ)))) :::
InhalePermission(perm, trE, memberName, currentK, (if (transferToSecMask) SecMask else Mask)) :::
+ // record "inside" relationship for predicate instances
+ (if(e.isPredicate && unfoldReceiver != null) bassume(FunctionApp("#predicateInside#", unfoldReceiver :: VarExpr(unfoldPredicateName) :: unfoldVersion :: trE :: VarExpr(memberName) :: Heap.select(trE, memberName) :: Nil)) :: Nil else Nil) :::
bassume(AreGoodMasks(Mask, SecMask)) ::
bassume(wf(Heap, Mask, SecMask)) ::
bassume(wf(ih, Mask, SecMask))
@@ -2017,12 +2343,12 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F 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), InhaleImplementation(e1, ih, check, currentK, transferToSecMask), Nil)
+ Boogie.If(Tr(e0), InhaleImplementation(e1, ih, check, currentK, transferToSecMask, unfoldReceiver, unfoldPredicateName, unfoldVersion), Nil)
case IfThenElse(con, then, els) =>
(if(check) isDefined(con)(true) else Nil) :::
- Boogie.If(Tr(con), InhaleImplementation(then, ih, check, currentK, transferToSecMask), InhaleImplementation(els, ih, check, currentK, transferToSecMask))
+ Boogie.If(Tr(con), InhaleImplementation(then, ih, check, currentK, transferToSecMask, unfoldReceiver, unfoldPredicateName, unfoldVersion), InhaleImplementation(els, ih, check, currentK, transferToSecMask, unfoldReceiver, unfoldPredicateName, unfoldVersion))
case And(e0,e1) =>
- InhaleImplementation(e0, ih, check, currentK, transferToSecMask) ::: InhaleImplementation(e1, ih, check, currentK, transferToSecMask)
+ InhaleImplementation(e0, ih, check, currentK, transferToSecMask) ::: InhaleImplementation(e1, ih, check, currentK, transferToSecMask, unfoldReceiver, unfoldPredicateName, unfoldVersion)
case holds@Holds(e) =>
val trE = Tr(e);
(if(check)
@@ -2060,7 +2386,7 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F bassume(AreGoodMasks(preEtran.Mask, preEtran.SecMask)) ::
bassume(wf(preEtran.Heap, preEtran.Mask, preEtran.SecMask)) ::
bassume(proofOrAssume) ::
- preEtran.InhaleImplementation(e, ih, check, currentK, transferToSecMask) :::
+ preEtran.InhaleImplementation(e, ih, check, currentK, transferToSecMask, unfoldReceiver, unfoldPredicateName, unfoldVersion) :::
bassume(preEtran.Heap ==@ evalHeap) ::
bassume(submask(preEtran.Mask, evalMask))
case uf@Unfolding(acc@Access(pred@MemberAccess(obj, f), perm), ufexpr) =>
@@ -2080,7 +2406,7 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F if (isOldEtran) Nil else
// remove secondary permissions (if any), and add them again
UpdateSecMaskDuringUnfold(pred.predicate, o, Heap.select(o, pred.predicate.FullName), perm, currentK) :::
- TransferPermissionToSecMask(pred.predicate, BoogieExpr(receiver), perm, uf.pos)
+ TransferPermissionToSecMask(pred.predicate, BoogieExpr(receiver), perm, uf.pos, receiver, pred.predicate.FullName, version)
) :::
bassume(Tr(uf))
@@ -2096,10 +2422,10 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F /** Transfer the permissions mentioned in the body of the predicate to the
* secondary mask.
*/
- def TransferPermissionToSecMask(pred: Predicate, obj: Expression, perm: Permission, pos: Position): List[Stmt] = {
+ def TransferPermissionToSecMask(pred: Predicate, obj: Expression, perm: Permission, pos: Position, unfoldingReceiver: VarExpr = null, unfoldingPredicateName: String = null, unfoldingVersion: VarExpr = null): List[Stmt] = {
var definition = scaleExpressionByPermission(SubstThis(DefinitionOf(pred), obj), perm, pos)
// go through definition and handle all permisions correctly
- InhaleToSecMask(definition)
+ InhaleToSecMask(definition, unfoldingReceiver, unfoldingPredicateName, unfoldingVersion)
}
// Exhale is done in two passes: In the first run, everything except permissions
@@ -2125,8 +2451,8 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F Exhale(m, sm, predicates, occasion, check, currentK, exactchecking, false, -1, false, null, false)
}
/** Exhale that transfers permission to the secondary mask */
- def ExhaleAndTransferToSecMask(predicates: List[(Expression, ErrorMessage)], occasion: String, currentK: Expr, exactchecking: Boolean): List[Boogie.Stmt] = {
- Exhale(Mask, SecMask, predicates, occasion, false, currentK, exactchecking, true /* transfer to SecMask */, -1, false, null, false)
+ def ExhaleAndTransferToSecMask(receiver: Expr, pred: Predicate, predicates: List[(Expression, ErrorMessage)], occasion: String, currentK: Expr, exactchecking: Boolean, foldReceiver: VarExpr = null, foldPredicateName: String = null, foldVersion: VarExpr = null): List[Boogie.Stmt] = {
+ Exhale(receiver, pred, Mask, SecMask, predicates, occasion, false, currentK, exactchecking, true /* transfer to SecMask */, -1, false, null, false, foldReceiver, foldPredicateName, foldVersion)
}
/** Remove permission from the secondary mask, and assume all assertions that
* would get generated. Recursion is bouded by the parameter depth.
@@ -2138,36 +2464,9 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F def UpdateSecMaskDuringUnfold(predicate: Predicate, receiver: Expr, version: Expr, perm: Permission, currentK: Expr): List[Stmt] = {
UpdateSecMask(predicate, receiver, version, perm, currentK, 1, Map())
}
+ // no longer relevant (as of Sept 2012), since we don't take this approach with secondary mask any more
def UpdateSecMask(predicate: Predicate, receiver: Expr, version: Expr, perm: Permission, currentK: Expr, depth: Int, previousReceivers: Map[String,List[Expr]]): List[Stmt] = {
- assert (depth >= 0)
- if (depth <= 0) return Nil
-
- val definition = scaleExpressionByPermission(SubstThis(DefinitionOf(predicate), BoogieExpr(receiver)), perm, NoPosition)
- val occasion = "update SecMask"
-
- // condition: if any folded predicate matches (both receiver and version), update the secondary map
- val disj = (for (fp <- etran.fpi.getFoldedPredicates(predicate)) yield {
- val conditions = (fp.conditions map (c => if (c._2) c._1 else !c._1)).foldLeft(true: Expr){ (a: Expr, b: Expr) => a && b }
- val b = fp.version ==@ version && fp.receiver ==@ receiver && conditions && fp.flag
- (b, fp.flag)
- })
- val b = (disj map (a => a._1)).foldLeft(false: Expr){ (a: Expr, b: Expr) => a || b }
-
- // add receiver to list of previous receivers
- val newPreviousReceivers = previousReceivers + (predicate.FullName -> (receiver :: previousReceivers.getOrElse(predicate.FullName, Nil)))
-
- // assumption that the current receiver is different from all previous ones
- (for (r <- previousReceivers.getOrElse(predicate.FullName, Nil)) yield {
- bassume(receiver !=@ r)
- }) :::
- // actually update the secondary mask
- Boogie.If(b,
- // remove correct predicate from the auxiliary information by setting
- // its flag to false
- (disj.foldLeft(Nil: List[Stmt]){ (a: List[Stmt], b: (Expr, Expr)) => Boogie.If(b._1,/*(b._2 := false) :: */Nil,a) :: Nil }) :::
- // asserts are converted to assumes, so error messages do not matter
- assert2assume(Exhale(SecMask, SecMask, List((definition, ErrorMessage(NoPosition, ""))), occasion, false, currentK, false /* it should not important what we pass here */, false, depth-1, true, newPreviousReceivers, false)),
- Nil) :: Nil
+ Nil
}
/** Most general form of exhale; implements all the specific versions above */
// Note: If isUpdatingSecMask, then m is actually a secondary mask, and at the
@@ -2190,27 +2489,33 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F // previousReceivers is not needed, and thus null.
// Assumption 4+5: duringUnfold can only be true if transferPermissionToSecMask
// and isUpdatingSecMask are not.
- def Exhale(m: Expr, sm: Expr, predicates: List[(Expression, ErrorMessage)], occasion: String, check: Boolean, currentK: Expr, exactchecking: Boolean, transferPermissionToSecMask: Boolean, recurseOnPredicatesDepth: Int, isUpdatingSecMask: Boolean, previousReceivers: Map[String,List[Expr]], duringUnfold: Boolean): List[Boogie.Stmt] = {
+ // Assumption 6: foldReceiver, foldPredicateName, foldVersion are all either non-null (in which case this exhale is the body of the corresponding predicate instance being folded) or all non-null.
+ def Exhale(m: Expr, sm: Expr, predicates: List[(Expression, ErrorMessage)], occasion: String, check: Boolean, currentK: Expr, exactchecking: Boolean, transferPermissionToSecMask: Boolean, recurseOnPredicatesDepth: Int, isUpdatingSecMask: Boolean, previousReceivers: Map[String,List[Expr]], duringUnfold: Boolean, foldReceiver: VarExpr = null, foldPredicateName: String = null, foldVersion: VarExpr = null): List[Boogie.Stmt] =
+ Exhale(null, null, m, sm, predicates, occasion, check, currentK, exactchecking, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers, duringUnfold, foldReceiver, foldPredicateName, foldVersion)
+ def Exhale(receiver: Expr, pred: Predicate, m: Expr, sm: Expr, predicates: List[(Expression, ErrorMessage)], occasion: String, check: Boolean, currentK: Expr, exactchecking: Boolean, transferPermissionToSecMask: Boolean, recurseOnPredicatesDepth: Int, isUpdatingSecMask: Boolean, previousReceivers: Map[String,List[Expr]], duringUnfold: Boolean, foldReceiver: VarExpr, foldPredicateName: String, foldVersion: VarExpr): List[Boogie.Stmt] = {
assert ((isUpdatingSecMask && recurseOnPredicatesDepth >= 0) || (!isUpdatingSecMask && recurseOnPredicatesDepth == -1)) // check assumption 2
assert (isUpdatingSecMask || (previousReceivers == null))
assert (!(isUpdatingSecMask && duringUnfold))
assert (!(transferPermissionToSecMask && duringUnfold))
+ assert ((foldReceiver == null) == (foldPredicateName == null))
+ assert ((foldPredicateName == null) == (foldVersion == null))
if (predicates.size == 0) return Nil;
val (ehV, eh) = Boogie.NewBVar("exhaleHeap", theap, true)
var (emV, em: Expr) = Boogie.NewBVar("exhaleMask", tmask, true)
Comment("begin exhale (" + occasion + ")") ::
- (if (!isUpdatingSecMask && !duringUnfold)
+ (if (!isUpdatingSecMask && !duringUnfold && !transferPermissionToSecMask)
BLocal(emV) :: (em := m) ::
BLocal(ehV) :: Boogie.Havoc(eh) :: Nil
else {
em = m
Nil
}) :::
- (for (p <- predicates) yield ExhaleHelper(p._1, em, sm, eh, p._2, check, currentK, exactchecking, false, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers, duringUnfold)).flatten :::
- (for (p <- predicates) yield ExhaleHelper(p._1, em, sm, eh, p._2, check, currentK, exactchecking, true, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers, duringUnfold)).flatten :::
- (if (!isUpdatingSecMask && !duringUnfold)
+ (for (p <- predicates) yield ExhaleHelper(p._1, em, sm, eh, p._2, check, currentK, exactchecking, false, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers, duringUnfold, foldReceiver, foldPredicateName, foldVersion )).flatten :::
+ (for (p <- predicates) yield ExhaleHelper(p._1, em, sm, eh, p._2, check, currentK, exactchecking, true, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers, duringUnfold, foldReceiver, foldPredicateName, foldVersion )).flatten :::
+ (if (!isUpdatingSecMask && !duringUnfold && !transferPermissionToSecMask)
(m := em) ::
bassume(IsGoodExhaleState(eh, Heap, m, sm)) ::
+ restoreFoldedLocations(m, Heap, eh) :::
(Heap := eh) :: Nil
else Nil) :::
(if (isUpdatingSecMask) Nil else bassume(AreGoodMasks(m, sm)) :: Nil) :::
@@ -2218,6 +2523,60 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F Comment("end exhale")
}
+ /** copy all the values of locations that are folded under any predicate (that we care about) one or more levels down from 'heap' to 'exhaleHeap' */
+ def restoreFoldedLocations(mask: Expr, heap: Boogie.Expr, exhaleHeap: Boogie.Expr): List[Boogie.Stmt] = {
+ val foldedPredicates = etran.fpi.getFoldedPredicates()
+ (for (fp <- foldedPredicates) yield {
+ val stmts = bassume(IsGoodExhalePredicateState(exhaleHeap, heap, heap.select(fp.receiver, fp.predicate.FullName+"#m")))
+ Boogie.If(CanRead(fp.receiver, fp.predicate.FullName, mask, ZeroMask) && heap.select(fp.receiver, fp.predicate.FullName) ==@ fp.version, stmts, Nil) :: Nil
+ }) flatten
+ }
+
+ /** the actual recursive method for restoreFoldedLocationsHelperPred */
+ def keepFoldedLocations(expr: Expression, foldReceiver: Expr, foldPred: Predicate, mask: Expr, heap: Boogie.Expr, otherPredicates: List[FoldedPredicate]): List[Boogie.Stmt] = {
+ val f = (expr: Expression) => keepFoldedLocations(expr, foldReceiver, foldPred, mask, heap, otherPredicates)
+ expr match {
+ case pred@MemberAccess(e, p) if pred.isPredicate =>
+ val tmp = Access(pred, Full);
+ tmp.pos = pred.pos;
+ f(tmp)
+ case AccessAll(obj, perm) =>
+ throw new InternalErrorException("not implemented yet")
+ case AccessSeq(s, None, perm) =>
+ throw new InternalErrorException("not implemented yet")
+ case acc@Access(e,perm) =>
+ val memberName = if (e.isPredicate) e.predicate.FullName else e.f.FullName;
+ val trE = Tr(e.e)
+ (if (e.isPredicate) {
+ val (ttV,tt) = Boogie.NewTVar("T")
+ val (refV, ref) = Boogie.NewBVar("ref", tref, true)
+ val (fV, f) = Boogie.NewBVar("f", FieldType(tt), true)
+ val (pmV, pm: Expr) = Boogie.NewBVar("newPredicateMask", tpmask, true)
+ val assumption = (heap.select(foldReceiver, foldPred.FullName+"#m").select(ref, f.id) || heap.select(trE, memberName+"#m").select(ref, f.id)) ==> pm.select(ref, f.id)
+ BLocal(pmV) :: Havoc(pm) ::
+ bassume(new Boogie.Forall(ttV, fV, assumption).forall(refV)) ::
+ (heap.select(foldReceiver, foldPred.FullName+"#m") := pm) :: Nil
+ } else Nil) :::
+ (heap.select(foldReceiver, foldPred.FullName+"#m").select(trE, memberName) := true) :: Nil
+ case acc @ AccessSeq(s, Some(member), perm) =>
+ throw new InternalErrorException("not implemented yet")
+ case cr@Credit(ch, n) =>
+ Nil
+ case Implies(e0,e1) =>
+ Boogie.If(Tr(e0), f(e1), Nil)
+ case IfThenElse(con, then, els) =>
+ Boogie.If(Tr(con), f(then), f(els))
+ case And(e0,e1) =>
+ f(e0) ::: f(e1)
+ case holds@Holds(e) =>
+ Nil
+ case Eval(h, e) =>
+ Nil
+ case e =>
+ Nil
+ }
+ }
+
// see comment in front of method exhale about parameter isUpdatingSecMask
def ExhalePermission(perm: Permission, obj: Expr, memberName: String, currentK: Expr, pos: Position, error: ErrorMessage, em: Boogie.Expr, exactchecking: Boolean, isUpdatingSecMask: Boolean): List[Boogie.Stmt] = {
val (f, stmts) = extractKFromPermission(perm, currentK)
@@ -2273,11 +2632,13 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F }
}
- def ExhaleHelper(p: Expression, m: Boogie.Expr, sm: Boogie.Expr, eh: Boogie.Expr, error: ErrorMessage, check: Boolean, currentK: Expr, exactchecking: Boolean, onlyExactCheckingPermissions: Boolean, transferPermissionToSecMask: Boolean, recurseOnPredicatesDepth: Int, isUpdatingSecMask: Boolean, previousReceivers: Map[String,List[Expr]], duringUnfold: Boolean): List[Boogie.Stmt] = desugar(p) match {
+ def ExhaleHelper(p: Expression, m: Boogie.Expr, sm: Boogie.Expr, eh: Boogie.Expr, error: ErrorMessage, check: Boolean, currentK: Expr, exactchecking: Boolean, onlyExactCheckingPermissions: Boolean, transferPermissionToSecMask: Boolean, recurseOnPredicatesDepth: Int, isUpdatingSecMask: Boolean, previousReceivers: Map[String,List[Expr]], duringUnfold: Boolean, foldReceiver: VarExpr = null, foldPredicateName: String = null, foldVersion: VarExpr = null): List[Boogie.Stmt] = {
+ val LocalExhaleHelper = (expr: Expression) => ExhaleHelper(expr, m, sm, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers, duringUnfold, foldReceiver, foldPredicateName, foldVersion)
+ desugar(p) match {
case pred@MemberAccess(e, p) if pred.isPredicate =>
val tmp = Access(pred, Full);
tmp.pos = pred.pos;
- ExhaleHelper(tmp, m, sm, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers, duringUnfold)
+ LocalExhaleHelper(tmp)
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) =>
@@ -2290,29 +2651,15 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F // check definedness
(if(check) isDefined(e.e)(true) :::
bassert(nonNull(Tr(e.e)), error.pos, error.message + " The target of the acc predicate at " + acc.pos + " might be null.") else Nil) :::
+ (if(e.isPredicate && foldReceiver != null) bassume(FunctionApp("#predicateInside#", foldReceiver :: VarExpr(foldPredicateName) :: foldVersion :: trE :: VarExpr(memberName) :: Heap.select(trE, memberName) :: Nil)) :: Nil else Nil) :::
// if the mask does not contain sufficient permissions, try folding acc(e, fraction)
// TODO: include automagic again
// check that the necessary permissions are there and remove them from the mask
ExhalePermission(perm, trE, memberName, currentK, acc.pos, error, m, ec, isUpdatingSecMask) :::
- // transfer permission to secondary mask if necessary
- (if (transferPermissionToSecMask) InhalePermission(perm, trE, memberName, currentK, sm)
- else Nil) :::
- // give up secondary permission to locations of the body of the predicate (also recursively)
- (if (e.isPredicate && !transferPermissionToSecMask)
- (if (isUpdatingSecMask)
- UpdateSecMask(e.predicate, trE, Heap.select(trE, memberName), perm, currentK, recurseOnPredicatesDepth, previousReceivers)
- else
- (if (duringUnfold)
- UpdateSecMaskDuringUnfold(e.predicate, trE, Heap.select(trE, memberName), perm, currentK)
- else
- UpdateSecMask(e.predicate, trE, Heap.select(trE, memberName), perm, currentK)
- )
- )
- else Nil) :::
// update version number (if necessary)
(if (e.isPredicate && !isUpdatingSecMask)
Boogie.If(!CanRead(trE, memberName, m, sm), // if we cannot access the predicate anymore, then its version will be havoced
- (if (!duringUnfold) bassume(Heap.select(trE, memberName) < eh.select(trE, memberName)) :: Nil // assume that the predicate's version grows monotonically
+ (if (!duringUnfold) (if (!transferPermissionToSecMask) bassume(Heap.select(trE, memberName) < eh.select(trE, memberName)) :: Nil else Nil) // assume that the predicate's version grows monotonically
else { // duringUnfold -> the heap is not havoced, thus we need to locally havoc the version
val (oldVersV, oldVers) = Boogie.NewBVar("oldVers", tint, true)
val (newVersV, newVers) = Boogie.NewBVar("newVers", tint, true)
@@ -2322,7 +2669,6 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F }),
Nil) :: Nil
else Nil) :::
- (if (isUpdatingSecMask) Nil else bassume(AreGoodMasks(m, sm)) :: Nil) :::
bassume(wf(Heap, m, sm)) :::
(if (m != Mask || sm != SecMask) bassume(wf(Heap, Mask, SecMask)) :: Nil else Nil)
}
@@ -2375,7 +2721,6 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F Lambda(List(), List(pcV), (pc ==@ "perm$R").thenElse(mr - r, mn - n)),
m(ref, f))))
} :::
- (if (isUpdatingSecMask) Nil else bassume(AreGoodMasks(m, sm)) :: Nil) :::
bassume(wf(Heap, m, sm)) :::
(if (m != Mask || sm != SecMask) bassume(wf(Heap, Mask, SecMask)) :: Nil else Nil)
}
@@ -2393,12 +2738,12 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F else Nil)
case Implies(e0,e1) =>
(if(check && !onlyExactCheckingPermissions) isDefined(e0)(true) else Nil) :::
- Boogie.If(Tr(e0), ExhaleHelper(e1, m, sm, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers, duringUnfold), Nil)
+ Boogie.If(Tr(e0), LocalExhaleHelper(e1), Nil)
case IfThenElse(con, then, els) =>
(if(check) isDefined(con)(true) else Nil) :::
- Boogie.If(Tr(con), ExhaleHelper(then, m, sm, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers, duringUnfold), ExhaleHelper(els, m, sm, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers, duringUnfold))
+ Boogie.If(Tr(con), LocalExhaleHelper(then), LocalExhaleHelper(els))
case And(e0,e1) =>
- ExhaleHelper(e0, m, sm, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers, duringUnfold) ::: ExhaleHelper(e1, m, sm, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers, duringUnfold)
+ LocalExhaleHelper(e0) ::: LocalExhaleHelper(e1)
case holds@Holds(e) if !onlyExactCheckingPermissions =>
(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) :::
@@ -2417,9 +2762,11 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F bassume(wf(preEtran.Heap, preEtran.Mask, preEtran.SecMask)) ::
bassert(proofOrAssume, p.pos, "Arguments for joinable might not match up.") ::
preEtran.Exhale(List((e, error)), "eval", check, currentK, exactchecking)
- case e if !onlyExactCheckingPermissions => (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."))
+ case e if !onlyExactCheckingPermissions =>
+ val (ee,ll) = Tr(e, true) // keep list ll of statements here, in case we are missing effects from unfolding expressions (if we do not call isDefined(e) below, we won't add secondary permissions/"inside" instances)
+ (if(check) isDefined(e)(true) else ll) ::: List(bassert(ee, error.pos, error.message + " The expression at " + e.pos + " might not evaluate to true."))
case _ => Nil
- }
+ }}
def extractKFromPermission(expr: Permission, currentK: Expr): (Expr, List[Boogie.Stmt]) = expr match {
case Full => (permissionFull, Nil)
@@ -2735,9 +3082,11 @@ object TranslationHelper { def tseq(arg: BType) = IndexedType("Seq", arg)
def theap = NamedType("HeapType");
def tmask = NamedType("MaskType");
+ def tpmask = NamedType("PMaskType");
def tcredits = NamedType("CreditsType");
def tperm = NamedType("PermissionComponent");
def ZeroMask = VarExpr("ZeroMask");
+ def ZeroPMask = VarExpr("ZeroPMask");
def ZeroCredits = VarExpr("ZeroCredits");
def HeapName = "Heap";
def MaskName = "Mask";
@@ -2745,6 +3094,7 @@ object TranslationHelper { def CreditsName = "Credits";
def GlobalNames = List(HeapName, MaskName, SecMaskName, CreditsName);
def CanAssumeFunctionDefs = VarExpr("CanAssumeFunctionDefs");
+ def FunctionContextHeight = VarExpr("FunctionContextHeight");
def permissionFull = percentPermission(100);
def permissionOnePercent = percentPermission(1);
def percentPermission(e: Expr) = {
@@ -2785,6 +3135,7 @@ object TranslationHelper { def AreGoodMasks(m: Expr, sm: Expr) = IsGoodMask(m) // && IsGoodMask(sm) /** The second mask does currently not necessarily contain positive permissions, which means that we cannot assume IsGoodMask(sm). This might change in the future if we see a need for it */
def IsGoodInhaleState(ih: Expr, h: Expr, m: Expr, sm: Expr) = FunctionApp("IsGoodInhaleState", List(ih,h,m,sm))
def IsGoodExhaleState(eh: Expr, h: Expr, m: Expr, sm: Expr) = FunctionApp("IsGoodExhaleState", List(eh,h,m,sm))
+ def IsGoodExhalePredicateState(eh: Expr, h: Expr, pm: Expr) = FunctionApp("IsGoodExhalePredicateState", List(eh,h,pm))
def contributesToWaitLevel(e: Expr, h: Expr, c: Expr) =
(0 < h.select(e, "held")) || h.select(e, "rdheld") || (new Boogie.MapSelect(c, e) < 0)
def NonEmptyMask(m: Expr) = ! FunctionApp("EmptyMask", List(m))
@@ -2898,7 +3249,7 @@ object TranslationHelper { heapFragment(Boogie.Ite(etran.Tr(con), functionDependencies(then, etran), functionDependencies(els, etran)))
case Unfolding(_, _) =>
emptyPartialHeap // the predicate of the unfolding expression needs to have been mentioned already (framing check), so we can safely ignore it now
- case p: PermissionExpr => println(p); throw new InternalErrorException("unexpected permission expression")
+ case p: PermissionExpr => throw new InternalErrorException("unexpected permission expression")
case e =>
e visitOpt {_ match {
case Unfolding(_, _) => false
diff --git a/Chalice/tests/examples/AVLTree.iterative.output.txt b/Chalice/tests/examples/AVLTree.iterative.output.txt index 152260e3..9b8797ef 100644 --- a/Chalice/tests/examples/AVLTree.iterative.output.txt +++ b/Chalice/tests/examples/AVLTree.iterative.output.txt @@ -1,4 +1,4 @@ Verification of AVLTree.iterative.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/AVLTree.nokeys.output.txt b/Chalice/tests/examples/AVLTree.nokeys.output.txt index c9dc557a..49850add 100644 --- a/Chalice/tests/examples/AVLTree.nokeys.output.txt +++ b/Chalice/tests/examples/AVLTree.nokeys.output.txt @@ -1,4 +1,4 @@ Verification of AVLTree.nokeys.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/AssociationList.output.txt b/Chalice/tests/examples/AssociationList.output.txt index 2955a814..e7ae56f6 100644 --- a/Chalice/tests/examples/AssociationList.output.txt +++ b/Chalice/tests/examples/AssociationList.output.txt @@ -7,4 +7,4 @@ Verification of AssociationList.chalice using parameters="" 73.9: The loop might lock/unlock more than the lockchange clause allows. 107.7: Monitor invariant might hot hold. Insufficient fraction at 120.13 for Node.key. -Boogie program verifier finished with 6 errors and 0 smoke test warnings.
+Boogie program verifier finished with 6 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/BackgroundComputation.output.txt b/Chalice/tests/examples/BackgroundComputation.output.txt index dc1bafc1..ad3f590e 100644 --- a/Chalice/tests/examples/BackgroundComputation.output.txt +++ b/Chalice/tests/examples/BackgroundComputation.output.txt @@ -1,4 +1,4 @@ Verification of BackgroundComputation.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt b/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt index b47290ea..91c56769 100644 --- a/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt +++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt @@ -5,4 +5,4 @@ Verification of CopyLessMessagePassing-with-ack.chalice using parameters="" 69.22: Assumption introduces a contradiction. 72.21: Assumption introduces a contradiction. -Boogie program verifier finished with 0 errors and 3 smoke test warnings.
+Boogie program verifier finished with 0 errors and 3 smoke test warnings
diff --git a/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt index 42a63bf1..2d6d752d 100644 --- a/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt +++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt @@ -4,4 +4,4 @@ Verification of CopyLessMessagePassing-with-ack2.chalice using parameters="" 50.23: Assumption introduces a contradiction. 65.27: Assumption introduces a contradiction. -Boogie program verifier finished with 0 errors and 2 smoke test warnings.
+Boogie program verifier finished with 0 errors and 2 smoke test warnings
diff --git a/Chalice/tests/examples/CopyLessMessagePassing.output.txt b/Chalice/tests/examples/CopyLessMessagePassing.output.txt index 26784a86..2caf540b 100644 --- a/Chalice/tests/examples/CopyLessMessagePassing.output.txt +++ b/Chalice/tests/examples/CopyLessMessagePassing.output.txt @@ -1,4 +1,4 @@ Verification of CopyLessMessagePassing.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/FictionallyDisjointCells.output.txt b/Chalice/tests/examples/FictionallyDisjointCells.output.txt index 9bc4fb68..0b8b0c4f 100644 --- a/Chalice/tests/examples/FictionallyDisjointCells.output.txt +++ b/Chalice/tests/examples/FictionallyDisjointCells.output.txt @@ -1,4 +1,4 @@ Verification of FictionallyDisjointCells.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/ForkJoin.output.txt b/Chalice/tests/examples/ForkJoin.output.txt index b1371da7..5ddd0f65 100644 --- a/Chalice/tests/examples/ForkJoin.output.txt +++ b/Chalice/tests/examples/ForkJoin.output.txt @@ -1,4 +1,4 @@ Verification of ForkJoin.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/HandOverHand.output.txt b/Chalice/tests/examples/HandOverHand.output.txt index 5d32ad2e..13ff996a 100644 --- a/Chalice/tests/examples/HandOverHand.output.txt +++ b/Chalice/tests/examples/HandOverHand.output.txt @@ -1,4 +1,4 @@ Verification of HandOverHand.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/OwickiGries.output.txt b/Chalice/tests/examples/OwickiGries.output.txt index 3a9a215b..8235b0f4 100644 --- a/Chalice/tests/examples/OwickiGries.output.txt +++ b/Chalice/tests/examples/OwickiGries.output.txt @@ -1,4 +1,4 @@ Verification of OwickiGries.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/PetersonsAlgorithm.output.txt b/Chalice/tests/examples/PetersonsAlgorithm.output.txt index eddb4927..1be5bf8c 100644 --- a/Chalice/tests/examples/PetersonsAlgorithm.output.txt +++ b/Chalice/tests/examples/PetersonsAlgorithm.output.txt @@ -5,4 +5,4 @@ Verification of PetersonsAlgorithm.chalice using parameters="" 34.5: The statements after the while-loop are unreachable. 59.5: The statements after the while-loop are unreachable. -Boogie program verifier finished with 0 errors and 3 smoke test warnings.
+Boogie program verifier finished with 0 errors and 3 smoke test warnings
diff --git a/Chalice/tests/examples/ProdConsChannel.output.txt b/Chalice/tests/examples/ProdConsChannel.output.txt index 4d91605c..20a587da 100644 --- a/Chalice/tests/examples/ProdConsChannel.output.txt +++ b/Chalice/tests/examples/ProdConsChannel.output.txt @@ -1,4 +1,4 @@ Verification of ProdConsChannel.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/RockBand.output.txt b/Chalice/tests/examples/RockBand.output.txt index 94f92a6e..f505fdb3 100644 --- a/Chalice/tests/examples/RockBand.output.txt +++ b/Chalice/tests/examples/RockBand.output.txt @@ -1,4 +1,4 @@ Verification of RockBand.chalice using parameters="-checkLeaks -defaults -autoFold"
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/Sieve.output.txt b/Chalice/tests/examples/Sieve.output.txt index 3e5117d3..0e37cd00 100644 --- a/Chalice/tests/examples/Sieve.output.txt +++ b/Chalice/tests/examples/Sieve.output.txt @@ -1,4 +1,4 @@ Verification of Sieve.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/Solver.output.txt b/Chalice/tests/examples/Solver.output.txt index 1ec04d27..7b6882c5 100644 --- a/Chalice/tests/examples/Solver.output.txt +++ b/Chalice/tests/examples/Solver.output.txt @@ -1,4 +1,4 @@ Verification of Solver.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/TreeOfWorker.output.txt b/Chalice/tests/examples/TreeOfWorker.output.txt index 13932da9..fe0c3376 100644 --- a/Chalice/tests/examples/TreeOfWorker.output.txt +++ b/Chalice/tests/examples/TreeOfWorker.output.txt @@ -1,4 +1,4 @@ Verification of TreeOfWorker.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/UnboundedThreads.output.txt b/Chalice/tests/examples/UnboundedThreads.output.txt index ccb4e93c..f8a05ed9 100644 --- a/Chalice/tests/examples/UnboundedThreads.output.txt +++ b/Chalice/tests/examples/UnboundedThreads.output.txt @@ -2,4 +2,4 @@ Verification of UnboundedThreads.chalice using parameters="" 40.17: The loop invariant at 40.17 might not be preserved by the loop. Insufficient epsilons at 40.27 for C.f. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/cell.output.txt b/Chalice/tests/examples/cell.output.txt index b5ba1586..b1567d01 100644 --- a/Chalice/tests/examples/cell.output.txt +++ b/Chalice/tests/examples/cell.output.txt @@ -5,4 +5,4 @@ Verification of cell.chalice using parameters="" The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. 135.3: The end of method main2 is unreachable. -Boogie program verifier finished with 1 errors and 1 smoke test warnings.
+Boogie program verifier finished with 1 errors and 1 smoke test warnings
diff --git a/Chalice/tests/examples/dining-philosophers.output.txt b/Chalice/tests/examples/dining-philosophers.output.txt index bd1bd4a0..ffba722f 100644 --- a/Chalice/tests/examples/dining-philosophers.output.txt +++ b/Chalice/tests/examples/dining-philosophers.output.txt @@ -3,4 +3,4 @@ Verification of dining-philosophers.chalice using parameters="" 24.5: The statements after the while-loop are unreachable. -Boogie program verifier finished with 0 errors and 1 smoke test warnings.
+Boogie program verifier finished with 0 errors and 1 smoke test warnings
diff --git a/Chalice/tests/examples/iterator.output.txt b/Chalice/tests/examples/iterator.output.txt index a33f44db..36a72bac 100644 --- a/Chalice/tests/examples/iterator.output.txt +++ b/Chalice/tests/examples/iterator.output.txt @@ -1,4 +1,4 @@ Verification of iterator.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/iterator2.output.txt b/Chalice/tests/examples/iterator2.output.txt index 02a7f02d..a28c5785 100644 --- a/Chalice/tests/examples/iterator2.output.txt +++ b/Chalice/tests/examples/iterator2.output.txt @@ -1,4 +1,4 @@ Verification of iterator2.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/linkedlist.chalice b/Chalice/tests/examples/linkedlist.chalice index acde86ab..a9859aaa 100644 --- a/Chalice/tests/examples/linkedlist.chalice +++ b/Chalice/tests/examples/linkedlist.chalice @@ -6,7 +6,7 @@ class Node { method init(v: int)
requires acc(next) && acc(value);
- ensures valid && size() == 1;
+ ensures valid && size() == 1 && (forall y:int :: contains(y) <==> y==v);
{
next := null;
value := v;
@@ -17,6 +17,7 @@ class Node { requires valid;
ensures valid;
ensures size() == old(size())+1;
+ ensures (forall y:int :: contains(y)==(old(contains(y)) || x==y));
{
unfold this.valid;
if(next==null) {
@@ -24,11 +25,32 @@ class Node { n := new Node;
call n.init(x);
next := n;
+ // unfold next.valid; fold next.valid; // makes it work
} else {
+
call next.add(x);
}
fold this.valid;
}
+
+ method addother(i:int)
+ requires valid
+ ensures valid && (forall x:int :: contains(x)==(old(contains(x)) || x==i))
+ {
+ unfold valid
+ if(next!=null)
+ {
+ call next.addother(i)
+ }
+ else
+ {
+ next:=new Node
+ next.value:=i
+ next.next:=null
+ fold next.valid
+ }
+ fold valid
+ }
method addFirst(x: int) returns (rt: Node)
requires valid;
@@ -46,14 +68,22 @@ class Node { function at(i: int): int
requires valid && 0<=i && i<size();
{
- unfolding valid in i==0 ? value : next.at(i-1) // no warning anymore... fishy!
+ unfolding valid in i==0 ? value : next.at(i-1)
}
function size(): int
requires valid;
+ ensures result > 0
{
unfolding this.valid in (next!=null ? 1+ next.size() : 1)
}
+
+ function contains(i:int):bool
+ requires valid
+ {
+ unfolding valid in i==value || (next!=null && next.contains(i))
+ }
+
predicate valid {
acc(next) && acc(value) && (next!=null ==> next.valid)
diff --git a/Chalice/tests/examples/linkedlist.output.txt b/Chalice/tests/examples/linkedlist.output.txt index ce5b5844..ffb5327d 100644 --- a/Chalice/tests/examples/linkedlist.output.txt +++ b/Chalice/tests/examples/linkedlist.output.txt @@ -1,5 +1,4 @@ Verification of linkedlist.chalice using parameters=""
- 49.39: Precondition at 47.14 might not hold. The expression at 47.31 might not evaluate to true. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/list-reverse.output.txt b/Chalice/tests/examples/list-reverse.output.txt index d8e19122..6179841d 100644 --- a/Chalice/tests/examples/list-reverse.output.txt +++ b/Chalice/tests/examples/list-reverse.output.txt @@ -1,4 +1,4 @@ Verification of list-reverse.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/lseg.chalice b/Chalice/tests/examples/lseg.chalice new file mode 100644 index 00000000..c7b6421a --- /dev/null +++ b/Chalice/tests/examples/lseg.chalice @@ -0,0 +1,86 @@ +class Node {
+ var next : Node;
+ var val : int;
+ /* ghost */ var length : int;
+
+ predicate lseg {
+ acc(length) && length > 0 && acc(next) && acc(val) && (length > 1 ==> next != null && next.lseg && next.lseg_length() + 1 == this.length)
+ }
+
+ function lseg_length() : int
+ requires lseg
+ {
+ unfolding lseg in length
+ }
+
+ function elems() : seq<int>
+ requires lseg
+ {
+ unfolding lseg in (length == 1 ? [val] : [val] ++ next.elems())
+ }
+
+ function end() : Node
+ requires lseg
+ {
+ unfolding lseg in (length == 1 ? next : next.end())
+ }
+
+ /* ghost */ method addAtEndRec(n:Node)
+ requires lseg && acc(n.*)
+ ensures lseg
+ ensures elems() == old(elems()) ++ [old(n.val)]
+ ensures end() == old(n.next)
+ ensures lseg_length() == old(lseg_length()) + 1
+ {
+ unfold this.lseg;
+ if (length == 1) {
+ this.next := n
+ n.length := 1
+ fold n.lseg
+ } else {
+ call this.next.addAtEndRec(n)
+ }
+ this.length := this.length + 1
+ fold this.lseg
+ }
+
+ method addAtEnd(v: int)
+ requires lseg
+ requires this.end() == null
+ ensures lseg
+ ensures elems() == old(elems()) ++ [v]
+ {
+ var cur: Node := this
+ unfold lseg
+ while (cur.next != null)
+ invariant acc(cur.*)
+ invariant this != cur ==> this.lseg && this.end() == cur
+ invariant cur.length > 0 && (cur.length > 1 ==> cur.next != null && cur.next.lseg) && (cur.length == 1 ? cur.next : cur.next.end()) == null
+ invariant ((this == cur ? [] : this.elems())
+ ++ [cur.val]
+ ++ (cur.next == null ? [] : cur.next.elems())) == old(this.elems())
+ {
+ /* ghost */ var temp: Node := cur
+ cur := cur.next
+ if (this == temp) {
+ this.length := 1
+ fold lseg
+ } else {
+ call addAtEndRec(temp)
+ }
+ unfold cur.lseg
+ }
+
+ var n: Node := new Node
+ n.val := v
+ n.next := null
+ cur.next := n
+ if(cur == this) {
+ this.length := 1
+ fold lseg
+ } else {
+ call addAtEndRec(cur)
+ }
+ call addAtEndRec(n)
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/examples/lseg.output.txt b/Chalice/tests/examples/lseg.output.txt new file mode 100644 index 00000000..ed31a673 --- /dev/null +++ b/Chalice/tests/examples/lseg.output.txt @@ -0,0 +1,4 @@ +Verification of lseg.chalice using parameters=""
+
+ +Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/producer-consumer.output.txt b/Chalice/tests/examples/producer-consumer.output.txt index 55f4bf3c..f3c3a28a 100644 --- a/Chalice/tests/examples/producer-consumer.output.txt +++ b/Chalice/tests/examples/producer-consumer.output.txt @@ -4,4 +4,4 @@ Verification of producer-consumer.chalice using parameters="" 42.5: The statements after the while-loop are unreachable. 81.5: The statements after the while-loop are unreachable. -Boogie program verifier finished with 0 errors and 2 smoke test warnings.
+Boogie program verifier finished with 0 errors and 2 smoke test warnings
diff --git a/Chalice/tests/examples/swap.output.txt b/Chalice/tests/examples/swap.output.txt index 8cd3bb7c..c0e86b2a 100644 --- a/Chalice/tests/examples/swap.output.txt +++ b/Chalice/tests/examples/swap.output.txt @@ -1,4 +1,4 @@ Verification of swap.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/general-tests/ImplicitLocals.output.txt b/Chalice/tests/general-tests/ImplicitLocals.output.txt index db26bba6..8e59a2b0 100644 --- a/Chalice/tests/general-tests/ImplicitLocals.output.txt +++ b/Chalice/tests/general-tests/ImplicitLocals.output.txt @@ -1,4 +1,4 @@ Verification of ImplicitLocals.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/general-tests/LoopLockChange.output.txt b/Chalice/tests/general-tests/LoopLockChange.output.txt index 19e84f93..ccd9a36a 100644 --- a/Chalice/tests/general-tests/LoopLockChange.output.txt +++ b/Chalice/tests/general-tests/LoopLockChange.output.txt @@ -9,4 +9,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 10.5: The statements after the while-loop are unreachable. 75.5: Assumption introduces a contradiction. -Boogie program verifier finished with 3 errors and 3 smoke test warnings.
+Boogie program verifier finished with 3 errors and 3 smoke test warnings
diff --git a/Chalice/tests/general-tests/RockBand-automagic.output.txt b/Chalice/tests/general-tests/RockBand-automagic.output.txt index 2e62b457..652213d9 100644 --- a/Chalice/tests/general-tests/RockBand-automagic.output.txt +++ b/Chalice/tests/general-tests/RockBand-automagic.output.txt @@ -1,4 +1,4 @@ Verification of RockBand-automagic.chalice using parameters="-checkLeaks -defaults -autoFold -autoMagic"
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/general-tests/SmokeTestTest.output.txt b/Chalice/tests/general-tests/SmokeTestTest.output.txt index 3d1cd786..1ad5f926 100644 --- a/Chalice/tests/general-tests/SmokeTestTest.output.txt +++ b/Chalice/tests/general-tests/SmokeTestTest.output.txt @@ -20,4 +20,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 116.3: Predicate Cell.valid is equivalent to false. 121.1: Where clause of channel C is equivalent to false. -Boogie program verifier finished with 1 errors and 16 smoke test warnings.
+Boogie program verifier finished with 1 errors and 16 smoke test warnings
diff --git a/Chalice/tests/general-tests/cell-defaults.output.txt b/Chalice/tests/general-tests/cell-defaults.output.txt index 138a5717..fd748230 100644 --- a/Chalice/tests/general-tests/cell-defaults.output.txt +++ b/Chalice/tests/general-tests/cell-defaults.output.txt @@ -7,4 +7,4 @@ Verification of cell-defaults.chalice using parameters="-defaults -autoFold -aut The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. 125.3: The end of method main2 is unreachable. -Boogie program verifier finished with 3 errors and 1 smoke test warnings.
+Boogie program verifier finished with 3 errors and 1 smoke test warnings
diff --git a/Chalice/tests/general-tests/counter.output.txt b/Chalice/tests/general-tests/counter.output.txt index 3c7f78b0..53bcd98d 100644 --- a/Chalice/tests/general-tests/counter.output.txt +++ b/Chalice/tests/general-tests/counter.output.txt @@ -14,4 +14,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 137.7: The begging of the lock-block is unreachable. 142.3: The end of method nestedBad3 is unreachable. -Boogie program verifier finished with 6 errors and 5 smoke test warnings.
+Boogie program verifier finished with 6 errors and 5 smoke test warnings
diff --git a/Chalice/tests/general-tests/nestedPredicates.chalice b/Chalice/tests/general-tests/nestedPredicates.chalice new file mode 100644 index 00000000..8afbff5c --- /dev/null +++ b/Chalice/tests/general-tests/nestedPredicates.chalice @@ -0,0 +1,114 @@ +/* Recursive implementation and specification of a linked list. */
+
+class Node {
+ var next: Node;
+ var value: int;
+
+ predicate valid {
+ rd*(next) && rd*(value) && (next!=null ==> next.valid)
+ }
+
+ method testNestingUnfold()
+ requires acc(this.valid)
+ {
+ unfold this.valid;
+ assert this != this.next;
+ if(this.next != null) {
+ unfold this.next.valid;
+ assert this.next != this.next.next;
+ assert this != this.next.next;
+ }
+ }
+
+ method testNestingFold() // this test shows that we build in the assumption that predicate instances with infinite expansions cannot be exist (in reachable code)
+ requires rd*(this.next) && rd*(this.value) && rd*(this.next.next) && rd*(this.next.value) && this.next != null && this.next.next != null && this.next.next.valid
+
+ {
+ fold this.next.valid;
+ assert this.next != this.next.next; // definition of valid "proves" that this.next and this.next.next cannot be aliases
+ fold this.valid;
+ assert this != this.next;
+ assert this != this.next.next;
+ }
+
+ method testNestingUnfolding()
+ requires acc(this.valid)
+ {
+ assert this != (unfolding this.valid in this.next);
+ if((unfolding this.valid in this.next) != null) {
+ assert (unfolding this.valid in this.next) != (unfolding this.valid in (unfolding this.next.valid in this.next.next));
+ assert this != (unfolding this.valid in (unfolding this.next.valid in this.next.next));
+ }
+ }
+
+ predicate p {
+ rd*(next) && rd*(value) && (next!=null ==> next.q)
+ }
+
+ predicate q {
+ rd*(next) && rd*(value) && (next!=null ==> next.p)
+ }
+
+ method testNestingUnfoldTwo()
+ requires acc(this.p)
+ {
+ unfold this.p;
+ assert this != this.next; // should fail
+ if(this.next != null) {
+ unfold this.next.q;
+ assert this.next != this.next.next; // should fail
+ assert this != this.next.next; // should succeed
+ }
+ }
+
+ method testNestingFoldTwo() // this test shows that we build in the assumption that predicate instances with infinite expansions cannot be exist (in reachable code)
+ requires rd*(this.next) && rd*(this.value) && rd*(this.next.next) && rd*(this.next.value) && this.next != null && this.next.next != null && this.next.next.p
+
+ {
+ fold this.next.q;
+ assert this != this.next; // should fail
+ assert this.next != this.next.next; // should fail
+ assert this != this.next.next; // should fail
+ }
+
+ method testNestingFoldThree() // this test shows that we build in the assumption that predicate instances with infinite expansions cannot be exist (in reachable code)
+ requires rd*(this.next) && rd*(this.value) && rd*(this.next.next) && rd*(this.next.value) && this.next != null && this.next.next != null && this.next.next.p
+
+ {
+ fold this.next.q;
+ fold this.p;
+ assert this != this.next; // should succeed, since this == this.next ==> this == this.next.next
+ assert this.next != this.next.next; // should fail - we haven't seen a cycle which would follow from this fact
+ assert this != this.next.next; // should succeed
+ }
+
+ method testNestingUnfoldingTwo()
+ requires acc(this.p)
+ {
+ assert this != (unfolding this.p in this.next); // should fail
+ if((unfolding this.p in this.next) != null) {
+ assert (unfolding this.p in this.next) != (unfolding this.p in (unfolding this.next.q in this.next.next)); // should fail
+ assert this != (unfolding this.p in (unfolding this.next.q in this.next.next)); // should succeed
+ }
+ }
+
+ method testNestingUnfoldingPrecondition(x: Node)
+ requires acc(this.valid) && (unfolding this.valid in this.next == x);
+ {
+ assert this != x;
+ }
+
+ function getNext() : Node
+ requires this.valid;
+ {
+ unfolding this.valid in this.next
+ }
+
+ method testNestingUnfoldingPostcondition(x: Node)
+ requires acc(this.valid);
+ ensures acc(this.valid) && (unfolding this.valid in true) && this != this.getNext()
+ {
+ // nothing
+ }
+
+}
\ No newline at end of file diff --git a/Chalice/tests/general-tests/nestedPredicates.output.txt b/Chalice/tests/general-tests/nestedPredicates.output.txt new file mode 100644 index 00000000..635ae780 --- /dev/null +++ b/Chalice/tests/general-tests/nestedPredicates.output.txt @@ -0,0 +1,12 @@ +Verification of nestedPredicates.chalice using parameters=""
+
+ 56.7: Assertion might not hold. The expression at 56.14 might not evaluate to true. + 59.9: Assertion might not hold. The expression at 59.16 might not evaluate to true. + 69.7: Assertion might not hold. The expression at 69.14 might not evaluate to true. + 70.7: Assertion might not hold. The expression at 70.14 might not evaluate to true. + 71.7: Assertion might not hold. The expression at 71.14 might not evaluate to true. + 81.7: Assertion might not hold. The expression at 81.14 might not evaluate to true. + 88.7: Assertion might not hold. The expression at 88.14 might not evaluate to true. + 90.9: Assertion might not hold. The expression at 90.16 might not evaluate to true. + +Boogie program verifier finished with 8 errors and 0 smoke test warnings
diff --git a/Chalice/tests/general-tests/prog1.output.txt b/Chalice/tests/general-tests/prog1.output.txt index 630ecdfa..c6c5fe0e 100644 --- a/Chalice/tests/general-tests/prog1.output.txt +++ b/Chalice/tests/general-tests/prog1.output.txt @@ -16,4 +16,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 73.3: The end of method main5 is unreachable. 78.3: The end of method main6 is unreachable. -Boogie program verifier finished with 7 errors and 6 smoke test warnings.
+Boogie program verifier finished with 7 errors and 6 smoke test warnings
diff --git a/Chalice/tests/general-tests/prog2.output.txt b/Chalice/tests/general-tests/prog2.output.txt index 68cd4870..da8dcf22 100644 --- a/Chalice/tests/general-tests/prog2.output.txt +++ b/Chalice/tests/general-tests/prog2.output.txt @@ -9,4 +9,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 20.3: The end of method Caller1 is unreachable. 69.3: The end of method M2 is unreachable. -Boogie program verifier finished with 4 errors and 2 smoke test warnings.
+Boogie program verifier finished with 4 errors and 2 smoke test warnings
diff --git a/Chalice/tests/general-tests/prog3.output.txt b/Chalice/tests/general-tests/prog3.output.txt index 18d05658..286b9248 100644 --- a/Chalice/tests/general-tests/prog3.output.txt +++ b/Chalice/tests/general-tests/prog3.output.txt @@ -8,4 +8,4 @@ Verification of prog3.chalice using parameters="" The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. 191.5: The statements after the method call statement are unreachable. -Boogie program verifier finished with 4 errors and 1 smoke test warnings.
+Boogie program verifier finished with 4 errors and 1 smoke test warnings
diff --git a/Chalice/tests/general-tests/prog4.output.txt b/Chalice/tests/general-tests/prog4.output.txt index 9415df7c..4ab057dd 100644 --- a/Chalice/tests/general-tests/prog4.output.txt +++ b/Chalice/tests/general-tests/prog4.output.txt @@ -11,4 +11,4 @@ Verification of prog4.chalice using parameters="" The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. 2.3: The end of method M is unreachable. -Boogie program verifier finished with 7 errors and 1 smoke test warnings.
+Boogie program verifier finished with 7 errors and 1 smoke test warnings
diff --git a/Chalice/tests/general-tests/quantifiers.output.txt b/Chalice/tests/general-tests/quantifiers.output.txt index 2f325c42..f05847b6 100644 --- a/Chalice/tests/general-tests/quantifiers.output.txt +++ b/Chalice/tests/general-tests/quantifiers.output.txt @@ -2,4 +2,4 @@ Verification of quantifiers.chalice using parameters="" 57.29: The heap of the callee might not be strictly smaller than the heap of the caller. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/general-tests/triggers.chalice b/Chalice/tests/general-tests/triggers.chalice new file mode 100644 index 00000000..08a6a7dd --- /dev/null +++ b/Chalice/tests/general-tests/triggers.chalice @@ -0,0 +1,81 @@ +// this test is for the automatic trigger generation
+
+class Triggers
+{
+ var next : Triggers // to allow recursive definitions
+
+ predicate valid { acc(next) && next != null && next.valid } // intentionally doesn't terminate - allows function definitions to be unknown
+
+ function f(x,y,z : int):bool
+ requires valid
+ {
+ unfolding valid in next.f(x,y,z) // unknown definition
+ }
+
+ function h(x,y,z : int):bool
+ requires valid
+ {
+ unfolding valid in next.h(x,y,z) // unknown definition
+ }
+
+ function g(x : int) : bool
+ requires valid
+ {
+ unfolding valid in next.g(x) // unknown definition
+ }
+
+ function i(x:int, y:bool) : bool
+ requires valid
+ {
+ unfolding valid in next.i(x,y) // unknown definition
+ }
+
+
+ method triggers_one()
+ requires valid
+ requires (forall a : int :: !(g(a) ==> false))
+ ensures valid
+ ensures (forall b : int :: g(b))
+ { }
+
+ method triggers_two()
+ requires valid
+ requires (forall a,b,c : int :: ( g(a) && f(a,b,c)))
+ ensures valid
+ ensures (forall x,y,z : int :: f(x,y,z))
+ ensures (forall w : int :: (g(w))) // fails because there isn't a good enough trigger for finding g(w)
+ { }
+
+ method triggers_three()
+ requires valid
+ requires (forall a : int :: ( g(a) && (forall b,c : int :: f(a,b,c))))
+ ensures valid
+ ensures (forall x,y,z : int :: f(x,y,z)) // fails because of the trigger chosen for a (g(a)).
+ ensures (forall w : int :: (g(w)))
+ { }
+
+ method triggers_four()
+ requires valid
+ requires (forall a,b,c,d,e:int :: f(a,b,c) && h(b,c,d) && f(c,d,e))
+ ensures valid
+ ensures (forall x,y,z : int :: f(x,y,z)) // fails - not enough triggers
+ ensures (forall x,y,z : int :: f(x,y,z) && f(z,y,x)) // succeeds - {f(a,b,c),f(c,d,e)} is one of the trigger sets which should be found
+ { }
+
+ method triggers_five(c : bool, d : bool)
+ requires c ==> d
+ requires valid
+ requires (forall x : int :: i(x, (c ==> d))) // check that logical operators are suitably avoided in triggers
+ ensures valid
+ ensures i(4,true)
+ { }
+
+ method triggers_six(c : int, d : int)
+ requires c > d
+ requires valid
+ requires (forall x : int :: i(x, (c > d))) // check that logical operators are suitably avoided in triggers
+ ensures valid
+ ensures i(4,true)
+ { }
+
+}
\ No newline at end of file diff --git a/Chalice/tests/general-tests/triggers.output.txt b/Chalice/tests/general-tests/triggers.output.txt new file mode 100644 index 00000000..3fae3c21 --- /dev/null +++ b/Chalice/tests/general-tests/triggers.output.txt @@ -0,0 +1,7 @@ +Verification of triggers.chalice using parameters=""
+
+ 41.3: The postcondition at 46.14 might not hold. The expression at 46.14 might not evaluate to true. + 49.3: The postcondition at 53.14 might not hold. The expression at 53.14 might not evaluate to true. + 57.3: The postcondition at 61.14 might not hold. The expression at 61.14 might not evaluate to true. + +Boogie program verifier finished with 3 errors and 0 smoke test warnings
diff --git a/Chalice/tests/permission-model/basic.output.txt b/Chalice/tests/permission-model/basic.output.txt index 02e7acb7..b2bf49bd 100644 --- a/Chalice/tests/permission-model/basic.output.txt +++ b/Chalice/tests/permission-model/basic.output.txt @@ -5,4 +5,4 @@ Verification of basic.chalice using parameters="" 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 4 errors and 0 smoke test warnings.
+Boogie program verifier finished with 4 errors and 0 smoke test warnings
diff --git a/Chalice/tests/permission-model/channels.output.txt b/Chalice/tests/permission-model/channels.output.txt index 159e0ee6..b2f76ab6 100644 --- a/Chalice/tests/permission-model/channels.output.txt +++ b/Chalice/tests/permission-model/channels.output.txt @@ -3,4 +3,4 @@ Verification of channels.chalice using parameters="" 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 2 errors and 0 smoke test warnings.
+Boogie program verifier finished with 2 errors and 0 smoke test warnings
diff --git a/Chalice/tests/permission-model/locks.output.txt b/Chalice/tests/permission-model/locks.output.txt index b6ea8f80..6b3a7abe 100644 --- a/Chalice/tests/permission-model/locks.output.txt +++ b/Chalice/tests/permission-model/locks.output.txt @@ -17,4 +17,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 86.3: The end of method a3 is unreachable. 138.5: The statements after the acquire statement are unreachable. -Boogie program verifier finished with 10 errors and 4 smoke test warnings.
+Boogie program verifier finished with 10 errors and 4 smoke test warnings
diff --git a/Chalice/tests/permission-model/peculiar.output.txt b/Chalice/tests/permission-model/peculiar.output.txt index e2e6ec90..07104e77 100644 --- a/Chalice/tests/permission-model/peculiar.output.txt +++ b/Chalice/tests/permission-model/peculiar.output.txt @@ -5,4 +5,4 @@ Verification of peculiar.chalice using parameters="" The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. 30.3: The end of method t4 is unreachable. -Boogie program verifier finished with 1 errors and 1 smoke test warnings.
+Boogie program verifier finished with 1 errors and 1 smoke test warnings
diff --git a/Chalice/tests/permission-model/permission_arithmetic.output.txt b/Chalice/tests/permission-model/permission_arithmetic.output.txt index f5c02b3d..b9d20e08 100644 --- a/Chalice/tests/permission-model/permission_arithmetic.output.txt +++ b/Chalice/tests/permission-model/permission_arithmetic.output.txt @@ -19,4 +19,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 200.3: The end of method a28 is unreachable. 215.3: The end of method a28b is unreachable. -Boogie program verifier finished with 11 errors and 5 smoke test warnings.
+Boogie program verifier finished with 11 errors and 5 smoke test warnings
diff --git a/Chalice/tests/permission-model/predicates.output.txt b/Chalice/tests/permission-model/predicates.output.txt index 5c0d0455..2f4acf7b 100644 --- a/Chalice/tests/permission-model/predicates.output.txt +++ b/Chalice/tests/permission-model/predicates.output.txt @@ -8,4 +8,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 28.3: The end of method b3 is unreachable. 49.3: The end of method b5 is unreachable. -Boogie program verifier finished with 3 errors and 2 smoke test warnings.
+Boogie program verifier finished with 3 errors and 2 smoke test warnings
diff --git a/Chalice/tests/permission-model/scaling.output.txt b/Chalice/tests/permission-model/scaling.output.txt index d57ab458..f2ebfdff 100644 --- a/Chalice/tests/permission-model/scaling.output.txt +++ b/Chalice/tests/permission-model/scaling.output.txt @@ -1,4 +1,4 @@ Verification of scaling.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/permission-model/sequences.output.txt b/Chalice/tests/permission-model/sequences.output.txt index f557b8c7..7c295c9d 100644 --- a/Chalice/tests/permission-model/sequences.output.txt +++ b/Chalice/tests/permission-model/sequences.output.txt @@ -3,4 +3,4 @@ Verification of sequences.chalice using parameters="" 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 2 errors and 0 smoke test warnings.
+Boogie program verifier finished with 2 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/FoldUnfoldExperiments.output.txt b/Chalice/tests/predicates/FoldUnfoldExperiments.output.txt index 7239cf05..ba48d6f4 100644 --- a/Chalice/tests/predicates/FoldUnfoldExperiments.output.txt +++ b/Chalice/tests/predicates/FoldUnfoldExperiments.output.txt @@ -1,4 +1,4 @@ Verification of FoldUnfoldExperiments.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/LinkedList-various.chalice b/Chalice/tests/predicates/LinkedList-various.chalice new file mode 100644 index 00000000..a888b647 --- /dev/null +++ b/Chalice/tests/predicates/LinkedList-various.chalice @@ -0,0 +1,176 @@ +class Node
+{
+ var v:int;
+ var n:Node;
+
+ predicate inv
+ { acc(v) && acc(n) && (n!=null ==> n.inv) }
+
+ function len():int
+ requires inv;
+ ensures result>0;
+ {
+ unfolding inv in (n==null) ? 1 : 1+n.len()
+ }
+
+ function get(i:int):int
+ requires inv && 0<=i && i<len();
+ {
+ unfolding inv in (i==0) ? v : n.get(i-1)
+ }
+
+ method addLast(x:int)
+ requires inv;
+ ensures inv;
+ ensures len()==old(len())+1 && get(old(len()))==x;
+ ensures (forall i:int :: 0<=i && i<old(len()) ==> get(i)==old(get(i)));
+ {
+ unfold inv;
+ if(n==null)
+ {
+ n:=new Node;
+ n.v:=x; n.n:=null;
+ fold n.inv;
+ }
+ else
+ {
+ call n.addLast(x);
+ }
+ fold inv;
+ }
+
+ method append(p:List)
+ requires inv && p!=null && p.inv;
+ ensures inv;
+ ensures len()==old(len()+p.len());
+ ensures (forall i in [0..old(len())] :: get(i)==old(get(i)));
+ ensures (forall i in [old(len())..len()] :: get(i)==old(p.get(i-len())));
+ {
+ unfold inv;
+ if(n==null)
+ {
+ unfold p.inv;
+ n:=p.c;
+ }
+ else
+ {
+ call n.append(p);
+ }
+ fold inv;
+ }
+
+ method remove(i:int)
+ requires inv && i>=0 && i<len()-1;
+ ensures inv;
+ ensures len()==old(len())-1;
+ ensures (forall j in [0..i+1] :: get(j)==old(get(j)));
+ ensures (forall j in [i+1..len()] :: get(j)==old(get(j+1)));
+ {
+ unfold inv;
+ if(i==0)
+ {
+ unfold n.inv;
+ n:=n.n;
+ }
+ else
+ {
+ call n.remove(i-1);
+ }
+ fold inv;
+ }
+}
+
+class List
+{
+ var c:Node;
+
+ predicate inv { acc(c) && (c!=null ==> c.inv) }
+
+ function len():int
+ requires inv;
+ ensures result>=0;
+ {
+ unfolding inv in (c==null) ? 0 : c.len()
+ }
+
+ function get(i:int):int
+ requires inv && 0<=i && i<len();
+ {
+ unfolding inv in c.get(i)
+ }
+
+ method addFirst(x:int)
+ requires inv;
+ ensures inv;
+ ensures len()==old(len())+1 && get(0)==x;
+ ensures (forall i:int :: 1<=i && i<len() ==> get(i)==old(get(i-1)));
+ {
+ var p:Node;
+
+ unfold inv;
+ p:=new Node; p.v:=x; p.n:=c; c:=p;
+ fold c.inv;
+ assert c.len()==old(len())+1
+ fold inv;
+ }
+
+ method addLast(x:int)
+ requires inv;
+ ensures inv;
+ ensures len()==old(len())+1 && get(old(len()))==x;
+ ensures (forall i:int :: 0<=i && i<old(len()) ==> get(i)==old(get(i)));
+ {
+ unfold inv;
+ if(c==null)
+ {
+ c:=new Node;
+ c.v:=x; c.n:=null;
+ fold c.inv;
+ }
+ else
+ {
+ call c.addLast(x);
+ }
+ fold inv;
+ }
+
+ method append(p:List)
+ requires inv && p!=null && p.inv;
+ ensures inv;
+ ensures len()==old(len()+p.len());
+ ensures (forall i in [0..old(len())] :: get(i)==old(get(i)));
+ ensures (forall i in [old(len())..len()] :: get(i)==old(p.get(i-len())));
+ {
+ unfold inv;
+ if(c==null)
+ {
+ unfold p.inv;
+ c:=p.c;
+ }
+ else
+ {
+ call c.append(p);
+ }
+ fold inv;
+ }
+
+ method remove(i:int)
+ requires inv && i>=0 && i<len();
+ ensures inv;
+ ensures len()==old(len())-1;
+ ensures (forall j in [0..i] :: get(j)==old(get(j)));
+ ensures (forall j in [i..len()] :: get(j)==old(get(j+1)));
+ {
+ unfold inv;
+ if(i==0)
+ {
+ unfold c.inv;
+ c:=c.n;
+ }
+ else
+ {
+ call c.remove(i-1);
+ }
+ fold inv;
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/predicates/aux-info.output.txt b/Chalice/tests/predicates/aux-info.output.txt index ae84772b..3d873f60 100644 --- a/Chalice/tests/predicates/aux-info.output.txt +++ b/Chalice/tests/predicates/aux-info.output.txt @@ -1,4 +1,4 @@ Verification of aux-info.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/framing-fields.chalice b/Chalice/tests/predicates/framing-fields.chalice index ce168f26..6cfd4607 100644 --- a/Chalice/tests/predicates/framing-fields.chalice +++ b/Chalice/tests/predicates/framing-fields.chalice @@ -11,9 +11,6 @@ class C {
method M (x:List, y:List)
requires x!=null && y!=null && x!=y && x.valid && y.valid;
- requires unfolding x.valid in x.next!=y;
- requires unfolding y.valid in y.next!=x;
- // the two requirements above are needed, otherwise Chalice cannot prove that the two lists are disjoint
{
var i: int := unfolding x.valid in x.value;
var j: int := unfolding y.valid in y.value;
diff --git a/Chalice/tests/predicates/framing-fields.output.txt b/Chalice/tests/predicates/framing-fields.output.txt index 3a7ea2ba..f1b426c6 100644 --- a/Chalice/tests/predicates/framing-fields.output.txt +++ b/Chalice/tests/predicates/framing-fields.output.txt @@ -1,5 +1,5 @@ Verification of framing-fields.chalice using parameters=""
- 22.5: Assertion might not hold. The expression at 22.12 might not evaluate to true. + 19.5: Assertion might not hold. The expression at 19.12 might not evaluate to true. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/framing-functions.output.txt b/Chalice/tests/predicates/framing-functions.output.txt index 01bdd7bb..2a3426c9 100644 --- a/Chalice/tests/predicates/framing-functions.output.txt +++ b/Chalice/tests/predicates/framing-functions.output.txt @@ -2,4 +2,4 @@ Verification of framing-functions.chalice using parameters="" 23.5: Assertion might not hold. The expression at 23.12 might not evaluate to true. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/list-reverse-extra-unfold-fold.chalice b/Chalice/tests/predicates/list-reverse-extra-unfold-fold.chalice new file mode 100644 index 00000000..8467ce4c --- /dev/null +++ b/Chalice/tests/predicates/list-reverse-extra-unfold-fold.chalice @@ -0,0 +1,51 @@ +class Node {
+ var next : Node;
+ var val : int;
+
+ predicate list {
+ acc(next) && acc(val) && (next!=null ==> next.list)
+ }
+
+ function vals() : seq<int>
+ requires list
+ {
+ unfolding list in (next == null ? [val] : [val] ++ next.vals())
+ }
+
+ function reverse_vals() : seq<int>
+ requires list
+ {
+ unfolding list in (next == null ? [val] : next.reverse_vals() ++ [val])
+ }
+
+ method reverse_in_place() returns (r:Node)
+ requires list;
+ ensures r != null && r.list;
+ ensures r.vals() == old(this.reverse_vals());
+ {
+ var l : Node := this;
+ r := null;
+
+ while (l != null)
+ invariant l!=null ==> l.list;
+ invariant r!=null ==> r.list;
+ invariant old(this.reverse_vals()) == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
+ {
+ var y: Node;
+ if (r != null) {
+ unfold r.list; fold r.list;
+ }
+ unfold l.list;
+ if (l.next != null) {
+ unfold l.next.list; fold l.next.list;
+ }
+
+
+ y := l.next;
+ l.next := r;
+ r := l;
+ fold r.list;
+ l := y;
+ }
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/predicates/list-reverse-extra-unfold-fold.output.txt b/Chalice/tests/predicates/list-reverse-extra-unfold-fold.output.txt new file mode 100644 index 00000000..6d2967f5 --- /dev/null +++ b/Chalice/tests/predicates/list-reverse-extra-unfold-fold.output.txt @@ -0,0 +1,4 @@ +Verification of list-reverse-extra-unfold-fold.chalice using parameters=""
+
+ +Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/mutual-dependence.output.txt b/Chalice/tests/predicates/mutual-dependence.output.txt index a35556a9..263084ac 100644 --- a/Chalice/tests/predicates/mutual-dependence.output.txt +++ b/Chalice/tests/predicates/mutual-dependence.output.txt @@ -2,4 +2,4 @@ Verification of mutual-dependence.chalice using parameters="" 16.5: Assertion might not hold. The expression at 16.12 might not evaluate to true. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/setset.output.txt b/Chalice/tests/predicates/setset.output.txt index c20911f0..b2e963ee 100644 --- a/Chalice/tests/predicates/setset.output.txt +++ b/Chalice/tests/predicates/setset.output.txt @@ -5,4 +5,4 @@ Verification of setset.chalice using parameters="" The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. 27.3: The end of method main is unreachable. -Boogie program verifier finished with 1 errors and 1 smoke test warnings.
+Boogie program verifier finished with 1 errors and 1 smoke test warnings
diff --git a/Chalice/tests/predicates/test.chalice b/Chalice/tests/predicates/test.chalice index 6c416671..9477caa6 100644 --- a/Chalice/tests/predicates/test.chalice +++ b/Chalice/tests/predicates/test.chalice @@ -30,9 +30,6 @@ class List fork t:=skip();
// mask: value=0,p=100, secmask: -
assert unfolding P in value==old(value);
- // ERROR: Chalice currently cannot verify this example, as there is neither
- // primary nor secondary permission available to value directly before the
- // assertion
}
}
diff --git a/Chalice/tests/predicates/test.output.txt b/Chalice/tests/predicates/test.output.txt index e05e1b4e..8b97e503 100644 --- a/Chalice/tests/predicates/test.output.txt +++ b/Chalice/tests/predicates/test.output.txt @@ -1,5 +1,4 @@ Verification of test.chalice using parameters=""
- 32.5: Assertion might not hold. The expression at 32.12 might not evaluate to true. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test1.output.txt b/Chalice/tests/predicates/test1.output.txt index 73be63ec..56888ecb 100644 --- a/Chalice/tests/predicates/test1.output.txt +++ b/Chalice/tests/predicates/test1.output.txt @@ -1,4 +1,4 @@ Verification of test1.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test10.output.txt b/Chalice/tests/predicates/test10.output.txt index d38b56a0..c043cbed 100644 --- a/Chalice/tests/predicates/test10.output.txt +++ b/Chalice/tests/predicates/test10.output.txt @@ -1,4 +1,4 @@ Verification of test10.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test2.output.txt b/Chalice/tests/predicates/test2.output.txt index d0bed944..780c15ef 100644 --- a/Chalice/tests/predicates/test2.output.txt +++ b/Chalice/tests/predicates/test2.output.txt @@ -1,4 +1,4 @@ Verification of test2.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test3.output.txt b/Chalice/tests/predicates/test3.output.txt index 7e4e49d6..2753e3f5 100644 --- a/Chalice/tests/predicates/test3.output.txt +++ b/Chalice/tests/predicates/test3.output.txt @@ -1,4 +1,4 @@ Verification of test3.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test4.output.txt b/Chalice/tests/predicates/test4.output.txt index 5268bec7..08a565c8 100644 --- a/Chalice/tests/predicates/test4.output.txt +++ b/Chalice/tests/predicates/test4.output.txt @@ -2,4 +2,4 @@ Verification of test4.chalice using parameters="" 54.2: Assertion might not hold. The expression at 54.9 might not evaluate to true. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test7.output.txt b/Chalice/tests/predicates/test7.output.txt index 46ac796c..e66a1d75 100644 --- a/Chalice/tests/predicates/test7.output.txt +++ b/Chalice/tests/predicates/test7.output.txt @@ -13,4 +13,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 62.3: The end of method uf0 is unreachable. 86.3: The end of method uf3 is unreachable. -Boogie program verifier finished with 7 errors and 3 smoke test warnings.
+Boogie program verifier finished with 7 errors and 3 smoke test warnings
diff --git a/Chalice/tests/predicates/test8.output.txt b/Chalice/tests/predicates/test8.output.txt index 881b2ef0..567d2894 100644 --- a/Chalice/tests/predicates/test8.output.txt +++ b/Chalice/tests/predicates/test8.output.txt @@ -1,4 +1,4 @@ Verification of test8.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/unfolding.chalice b/Chalice/tests/predicates/unfolding.chalice index f01b237d..6b276a04 100644 --- a/Chalice/tests/predicates/unfolding.chalice +++ b/Chalice/tests/predicates/unfolding.chalice @@ -14,6 +14,7 @@ class Cell { method test2()
requires p
+ ensures p
{
var tmp: int := unfolding p in value;
var tmp2: int := unfolding p in value;
diff --git a/Chalice/tests/predicates/unfolding.output.txt b/Chalice/tests/predicates/unfolding.output.txt index 4a1ebbde..7ff49106 100644 --- a/Chalice/tests/predicates/unfolding.output.txt +++ b/Chalice/tests/predicates/unfolding.output.txt @@ -2,4 +2,4 @@ Verification of unfolding.chalice using parameters="" 12.5: Assertion might not hold. The expression at 12.12 might not evaluate to true. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/internal-bug-1.output.txt b/Chalice/tests/regressions/internal-bug-1.output.txt index ea14d3e3..7685b77a 100644 --- a/Chalice/tests/regressions/internal-bug-1.output.txt +++ b/Chalice/tests/regressions/internal-bug-1.output.txt @@ -1,4 +1,4 @@ Verification of internal-bug-1.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/internal-bug-2.output.txt b/Chalice/tests/regressions/internal-bug-2.output.txt index 3b763659..8724af64 100644 --- a/Chalice/tests/regressions/internal-bug-2.output.txt +++ b/Chalice/tests/regressions/internal-bug-2.output.txt @@ -5,4 +5,4 @@ Verification of internal-bug-2.chalice using parameters="" The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. 6.5: The end of method koko is unreachable. -Boogie program verifier finished with 1 errors and 1 smoke test warnings.
+Boogie program verifier finished with 1 errors and 1 smoke test warnings
diff --git a/Chalice/tests/regressions/internal-bug-4.chalice b/Chalice/tests/regressions/internal-bug-4.chalice new file mode 100644 index 00000000..af850d49 --- /dev/null +++ b/Chalice/tests/regressions/internal-bug-4.chalice @@ -0,0 +1,17 @@ +class C
+{
+ var f: int;
+ predicate valid { acc(f) }
+
+ function foo1(): int
+ ensures valid;
+ { 1 }
+
+ function foo2(): int
+ ensures acc(f);
+ { 1 }
+
+ function foo3(): int
+ ensures rd(f);
+ { 1 }
+}
diff --git a/Chalice/tests/regressions/internal-bug-4.output.txt b/Chalice/tests/regressions/internal-bug-4.output.txt new file mode 100644 index 00000000..a985df28 --- /dev/null +++ b/Chalice/tests/regressions/internal-bug-4.output.txt @@ -0,0 +1,6 @@ +Verification of internal-bug-4.chalice using parameters=""
+
+The program did not typecheck.
+7.3: the postcondition of functions cannot contain accessibility predicates (permissions are returned automatically)
+11.3: the postcondition of functions cannot contain accessibility predicates (permissions are returned automatically)
+15.3: the postcondition of functions cannot contain accessibility predicates (permissions are returned automatically)
diff --git a/Chalice/tests/regressions/workitem-10189.chalice b/Chalice/tests/regressions/workitem-10189.chalice new file mode 100644 index 00000000..b37b83f2 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10189.chalice @@ -0,0 +1,23 @@ +class Node { + var v: int + var next: Node + + predicate V { + acc(v) + && acc(next) + && (next != null ==> next.V) + } + + unlimited function length(): int + requires rd(V) + { 1 + unfolding rd(V) in next == null ? 0 : next.length() } + + unlimited function at(i: int): int + requires rd(V) + requires i >= 0 + requires i < length() // XXXX + { + unfolding rd(V) in i == 0 ? v : next.at(i - 1) + // Precondition at XXX might not hold + } +}
\ No newline at end of file diff --git a/Chalice/tests/regressions/workitem-10189.output.txt b/Chalice/tests/regressions/workitem-10189.output.txt new file mode 100644 index 00000000..96f05468 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10189.output.txt @@ -0,0 +1,4 @@ +Verification of workitem-10189.chalice using parameters=""
+
+ +Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10192.output.txt b/Chalice/tests/regressions/workitem-10192.output.txt index 1f5fbeec..f2a5b539 100644 --- a/Chalice/tests/regressions/workitem-10192.output.txt +++ b/Chalice/tests/regressions/workitem-10192.output.txt @@ -1,4 +1,4 @@ Verification of workitem-10192.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10194.output.txt b/Chalice/tests/regressions/workitem-10194.output.txt index 580a8068..23114b0a 100644 --- a/Chalice/tests/regressions/workitem-10194.output.txt +++ b/Chalice/tests/regressions/workitem-10194.output.txt @@ -3,4 +3,4 @@ Verification of workitem-10194.chalice using parameters="" 20.35: Location might not be readable. 35.3: Assertion might not hold. The expression at 35.10 might not evaluate to true. -Boogie program verifier finished with 2 errors and 0 smoke test warnings.
+Boogie program verifier finished with 2 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10195.output.txt b/Chalice/tests/regressions/workitem-10195.output.txt index 0636df17..6e8b3556 100644 --- a/Chalice/tests/regressions/workitem-10195.output.txt +++ b/Chalice/tests/regressions/workitem-10195.output.txt @@ -9,4 +9,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 19.9: Precondition of method succeeds2 is equivalent to false. 27.9: Precondition of method fails2 is equivalent to false. -Boogie program verifier finished with 2 errors and 4 smoke test warnings.
+Boogie program verifier finished with 2 errors and 4 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10196.output.txt b/Chalice/tests/regressions/workitem-10196.output.txt index 013880cc..26199999 100644 --- a/Chalice/tests/regressions/workitem-10196.output.txt +++ b/Chalice/tests/regressions/workitem-10196.output.txt @@ -1,4 +1,4 @@ Verification of workitem-10196.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10197.output.txt b/Chalice/tests/regressions/workitem-10197.output.txt index 9cc1319a..c83bbfe0 100644 --- a/Chalice/tests/regressions/workitem-10197.output.txt +++ b/Chalice/tests/regressions/workitem-10197.output.txt @@ -1,4 +1,4 @@ Verification of workitem-10197.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10198.output.txt b/Chalice/tests/regressions/workitem-10198.output.txt index 8e421059..c3b59307 100644 --- a/Chalice/tests/regressions/workitem-10198.output.txt +++ b/Chalice/tests/regressions/workitem-10198.output.txt @@ -2,4 +2,4 @@ Verification of workitem-10198.chalice using parameters="" 12.2: Method might lock/unlock more than allowed. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10199.output.txt b/Chalice/tests/regressions/workitem-10199.output.txt index 4fb873e7..660fd6ae 100644 --- a/Chalice/tests/regressions/workitem-10199.output.txt +++ b/Chalice/tests/regressions/workitem-10199.output.txt @@ -1,4 +1,4 @@ Verification of workitem-10199.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10200.output.txt b/Chalice/tests/regressions/workitem-10200.output.txt index cac4bb62..90d5b467 100644 --- a/Chalice/tests/regressions/workitem-10200.output.txt +++ b/Chalice/tests/regressions/workitem-10200.output.txt @@ -2,4 +2,4 @@ Verification of workitem-10200.chalice using parameters="" 7.15: The heap of the callee might not be strictly smaller than the heap of the caller. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10208.chalice b/Chalice/tests/regressions/workitem-10208.chalice new file mode 100644 index 00000000..ae1a7d89 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10208.chalice @@ -0,0 +1,41 @@ +class Test {
+ var f1: int;
+ var f2: int;
+
+ predicate valid {
+ acc(f1) && acc(f2) && f1 == f2
+ }
+
+ method test()
+ requires valid
+ {
+ unfold valid
+ f1 := 2
+ f2 := 2
+ fold valid
+
+ /* --- not strictly necessary */
+ unfold valid
+ assert f1 == 2
+ fold valid
+ /* --- */
+
+ call test2()
+
+ unfold valid
+ assert f1 == 2 // BUG: this should not verify (1)
+ assert false // BUG: this should not verify (2)
+ }
+
+ method test2()
+ requires valid
+ ensures valid
+ ensures unfolding valid in f1 == 1 // line (1) above verifies also without this postcondition
+ {
+ unfold valid
+ f1 := 1
+ f2 := 1
+ fold valid
+ }
+
+}
diff --git a/Chalice/tests/regressions/workitem-10208.output.txt b/Chalice/tests/regressions/workitem-10208.output.txt new file mode 100644 index 00000000..0666393a --- /dev/null +++ b/Chalice/tests/regressions/workitem-10208.output.txt @@ -0,0 +1,8 @@ +Verification of workitem-10208.chalice using parameters=""
+
+ 26.5: Assertion might not hold. The expression at 26.12 might not evaluate to true. + +The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. + 9.3: The end of method test is unreachable. + +Boogie program verifier finished with 1 errors and 1 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10221.chalice b/Chalice/tests/regressions/workitem-10221.chalice new file mode 100644 index 00000000..2a8ae723 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10221.chalice @@ -0,0 +1,158 @@ +// In this example, additional unfold/fold pairs make the verification of the last three methods fail.
+
+class Node {
+ var next : Node;
+ var val : int;
+
+ predicate list {
+ acc(next) && acc(val) && (next!=null ==> next.list)
+ }
+
+ function vals() : seq<int>
+ requires list
+ {
+ unfolding list in (next == null ? [val] : [val] ++ next.vals())
+ }
+
+ function reverse_vals() : seq<int>
+ requires list
+ {
+ unfolding list in (next == null ? [val] : next.reverse_vals() ++ [val])
+ }
+
+ method reverse_in_place() returns (r:Node)
+ requires list;
+ ensures true;
+ {
+ var l : Node := this;
+ r := null;
+
+ var rev : seq<int> := this.reverse_vals();
+
+ while (l != null)
+ invariant l!=null ==> l.list;
+ invariant r!=null ==> r.list;
+ invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
+ {
+ var y: Node;
+// if (r != null) {
+// unfold r.list; fold r.list;
+// }
+ unfold l.list;
+// if (l.next != null) {
+// unfold l.next.list; fold l.next.list;
+// }
+
+ y := l.next;
+ l.next := r;
+ r := l;
+ fold r.list;
+ l := y;
+ }
+ assert r.vals() == rev; // should be the post-condition
+ }
+
+
+ method reverse_in_place_01() returns (r:Node)
+ requires list;
+ ensures true;
+ {
+ var l : Node := this;
+ r := null;
+
+ var rev : seq<int> := this.reverse_vals();
+
+ while (l != null)
+ invariant l!=null ==> l.list;
+ invariant r!=null ==> r.list;
+ invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
+ {
+ var y: Node;
+// if (r != null) {
+// unfold r.list; fold r.list;
+// }
+ unfold l.list;
+ if (l.next != null) {
+ unfold l.next.list; fold l.next.list;
+ }
+
+ y := l.next;
+ l.next := r;
+ r := l;
+ fold r.list;
+ l := y;
+ }
+ assert r.vals() == rev; // should be the post-condition
+ }
+
+
+
+ method reverse_in_place_10() returns (r:Node)
+ requires list;
+ ensures true;
+ {
+ var l : Node := this;
+ r := null;
+
+ var rev : seq<int> := this.reverse_vals();
+
+ while (l != null)
+ invariant l!=null ==> l.list;
+ invariant r!=null ==> r.list;
+ invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
+ {
+ var y: Node;
+ if (r != null) {
+ unfold r.list; fold r.list;
+ }
+ unfold l.list;
+// if (l.next != null) {
+// unfold l.next.list; fold l.next.list;
+// }
+
+ y := l.next;
+ l.next := r;
+ r := l;
+ fold r.list;
+ l := y;
+ }
+ assert r.vals() == rev; // should be the post-condition
+ }
+
+
+
+
+ method reverse_in_place_11() returns (r:Node)
+ requires list;
+ ensures true;
+ {
+ var l : Node := this;
+ r := null;
+
+ var rev : seq<int> := this.reverse_vals();
+
+ while (l != null)
+ invariant l!=null ==> l.list;
+ invariant r!=null ==> r.list;
+ invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
+ {
+ var y: Node;
+ if (r != null) {
+ unfold r.list; fold r.list;
+ }
+ unfold l.list;
+ if (l.next != null) {
+ unfold l.next.list; fold l.next.list;
+ }
+
+ y := l.next;
+ l.next := r;
+ r := l;
+ fold r.list;
+ l := y;
+ }
+ assert r.vals() == rev; // should be the post-condition
+ }
+
+
+}
\ No newline at end of file diff --git a/Chalice/tests/regressions/workitem-10221.output.txt b/Chalice/tests/regressions/workitem-10221.output.txt new file mode 100644 index 00000000..e209c3c1 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10221.output.txt @@ -0,0 +1,4 @@ +Verification of workitem-10221.chalice using parameters=""
+
+ +Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10223.output.txt b/Chalice/tests/regressions/workitem-10223.output.txt index f4bfd78d..b65fbc0c 100644 --- a/Chalice/tests/regressions/workitem-10223.output.txt +++ b/Chalice/tests/regressions/workitem-10223.output.txt @@ -1,4 +1,4 @@ Verification of workitem-10223.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-8234.output.txt b/Chalice/tests/regressions/workitem-8234.output.txt index 8d13e17a..14175fd2 100644 --- a/Chalice/tests/regressions/workitem-8234.output.txt +++ b/Chalice/tests/regressions/workitem-8234.output.txt @@ -1,4 +1,4 @@ Verification of workitem-8234.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-8236.output.txt b/Chalice/tests/regressions/workitem-8236.output.txt index 30b42ab1..6f1994d3 100644 --- a/Chalice/tests/regressions/workitem-8236.output.txt +++ b/Chalice/tests/regressions/workitem-8236.output.txt @@ -2,4 +2,4 @@ Verification of workitem-8236.chalice using parameters="" 3.2: Method might lock/unlock more than allowed. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-9978.output.txt b/Chalice/tests/regressions/workitem-9978.output.txt index 0e557a3b..e6086625 100644 --- a/Chalice/tests/regressions/workitem-9978.output.txt +++ b/Chalice/tests/regressions/workitem-9978.output.txt @@ -3,4 +3,4 @@ Verification of workitem-9978.chalice using parameters="" 4.5: The statements after the while-loop are unreachable. -Boogie program verifier finished with 0 errors and 1 smoke test warnings.
+Boogie program verifier finished with 0 errors and 1 smoke test warnings
diff --git a/Chalice/tests/test-scripts/getboogieoutput.bat b/Chalice/tests/test-scripts/getboogieoutput.bat index f7b729fe..76af1fcf 100644 --- a/Chalice/tests/test-scripts/getboogieoutput.bat +++ b/Chalice/tests/test-scripts/getboogieoutput.bat @@ -25,7 +25,7 @@ if "!key!"=="!str!" ( echo Verification of %1.chalice using parameters="%chaliceparameters%" > %output%
echo.>> %output%
-call %chalice% "%1.chalice" -smoke %chaliceparameters% %2 %3 %4 %5 %6 %7 >> %output% 2>&1
+call %chalice% "%1.chalice" -smoke -time:0 %chaliceparameters% %2 %3 %4 %5 %6 %7 >> %output% 2>&1
set o=%~dp1%out.bpl
if exist "%o%" copy "%o%" "%1.bpl">nul
diff --git a/Chalice/tests/test-scripts/reg_test.bat b/Chalice/tests/test-scripts/reg_test.bat index c6ab8424..54549afc 100644 --- a/Chalice/tests/test-scripts/reg_test.bat +++ b/Chalice/tests/test-scripts/reg_test.bat @@ -35,18 +35,20 @@ if "!key!"=="!str!" ( set output=output.txt
echo Verification of %1.chalice using parameters="%chaliceparameters%" > %output%
echo.>> %output%
-call %chalice% "%1.chalice" -smoke %chaliceparameters% %2 %3 %4 %5 %6 %7 >> %output% 2>&1
+call %chalice% "%1.chalice" -smoke -time:3 %chaliceparameters% %2 %3 %4 %5 %6 %7 1>> %output% 2> time.log
+set /p extime= < time.log
+del time.log
fc "%1.output.txt" output.txt > nul
if not errorlevel 1 goto passTest
goto failTest
:passTest
-echo OK: %1.chalice
+echo OK: %1.chalice (%extime% seconds)
goto end
:failTest
-echo FAIL: %1.chalice
+echo FAIL: %1.chalice (%extime% seconds)
if %nodiff%==0 (
call %diff% "%1.output.txt" output.txt
)
diff --git a/Chalice/tests/test-scripts/test.bat b/Chalice/tests/test-scripts/test.bat index 30e135bd..8572dc6b 100644 --- a/Chalice/tests/test-scripts/test.bat +++ b/Chalice/tests/test-scripts/test.bat @@ -27,7 +27,7 @@ if "!key!"=="!str!" ( set output=output.txt
echo Verification of %1.chalice using parameters="%chaliceparameters%" > %output%
echo.>> %output%
-call %chalice% "%1.chalice" -smoke %chaliceparameters% %2 %3 %4 %5 %6 %7 >> %output% 2>&1
+call %chalice% "%1.chalice" -smoke -time:0 %chaliceparameters% %2 %3 %4 %5 %6 %7 >> %output% 2>&1
type %output%
exit /B 0
diff --git a/Source/Core/Makefile b/Source/Core/Makefile index 192a16db..4d3f433a 100644 --- a/Source/Core/Makefile +++ b/Source/Core/Makefile @@ -10,10 +10,11 @@ FRAME_DIR = ..\..\..\boogiepartners\CocoR\Modified # "all" depends on 2 files, really (Parser.cs and Scanner.cs), but they
# are both generated in one go and I don't know a better way to tell
# nmake that. --KRML
-all: Parser.ssc
+all: Parser.cs
-Parser.ssc: $(FRAME_DIR)\Scanner.frame $(FRAME_DIR)\Parser.frame BoogiePL.atg
+Parser.cs: $(FRAME_DIR)\Scanner.frame $(FRAME_DIR)\Parser.frame BoogiePL.atg
$(COCO) BoogiePL.atg -namespace Microsoft.Boogie -frames $(FRAME_DIR)
clean:
- rm -f Scanner.cs Parser.cs
+ if exist Scanner.cs del Scanner.cs
+ if exist Parser.cs del Parser.cs
|