summaryrefslogtreecommitdiff
path: root/Chalice
diff options
context:
space:
mode:
Diffstat (limited to 'Chalice')
-rw-r--r--Chalice/src/Ast.scala6
-rw-r--r--Chalice/src/Boogie.scala22
-rw-r--r--Chalice/src/Chalice.scala136
-rw-r--r--Chalice/src/PrettyPrinter.scala5
-rw-r--r--Chalice/src/Translator.scala118
5 files changed, 154 insertions, 133 deletions
diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 464840c5..23d6356d 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -164,14 +164,14 @@ case class Function(id: String, ins: List[Variable], out: Type, spec: List[Speci
case class Condition(id: String, where: Option[Expression]) extends NamedMember(id)
case class Variable(id: String, t: Type, isGhost: Boolean, isImmutable: Boolean) extends ASTNode {
val UniqueName = {
- val n = Variable.VariableCount
- Variable.VariableCount = Variable.VariableCount + 1
+ val n = S_Variable.VariableCount
+ S_Variable.VariableCount = S_Variable.VariableCount + 1
id + "#" + n
}
def this(name: String, typ: Type) = this(name,typ,false,false);
override def toString = (if (isGhost) "ghost " else "") + (if (isImmutable) "const " else "var ") + id;
}
-object Variable { var VariableCount = 0 }
+object S_Variable { var VariableCount = 0 }
case class SpecialVariable(name: String, typ: Type) extends Variable(name, typ, false, false) {
override val UniqueName = name
}
diff --git a/Chalice/src/Boogie.scala b/Chalice/src/Boogie.scala
index 5e3206c1..4fa21be0 100644
--- a/Chalice/src/Boogie.scala
+++ b/Chalice/src/Boogie.scala
@@ -21,8 +21,10 @@ object Boogie {
case class NamedType(s: String) extends BType
case class IndexedType(id: String, t: BType) extends BType
+ case class Tag(s: String)
sealed abstract class Stmt {
def Locals = List[BVar]()
+ var tags: List[Tag] = Nil
}
case class Comment(comment: String) extends Stmt
case class Assert(e: Expr) extends Stmt {
@@ -113,15 +115,15 @@ object Boogie {
case class BVar(id: String, t: BType) {
def this(id: String, t: BType, uniquifyName: Boolean) =
this(if (uniquifyName) {
- val n = BVar.VariableCount
- BVar.VariableCount = BVar.VariableCount + 1
+ val n = S_BVar.VariableCount
+ S_BVar.VariableCount = S_BVar.VariableCount + 1
id + "#_" + n
} else {
id
}, t)
val where: Expr = null
}
- object BVar { var VariableCount = 0 }
+ object S_BVar { var VariableCount = 0 }
def NewBVar(id: String, t: BType, uniquifyName: Boolean) = {
val v = new Boogie.BVar(id, t, uniquifyName)
val e = new Boogie.VarExpr(v)
@@ -130,25 +132,23 @@ object Boogie {
case class TVar(id: String) {
def this(id: String, uniquifyName: Boolean) =
this(if (uniquifyName) {
- val n = TVar.VariableCount
- TVar.VariableCount = TVar.VariableCount + 1
+ val n = S_TVar.VariableCount
+ S_TVar.VariableCount = S_TVar.VariableCount + 1
id + "#_" + n
} else {
id
})
val where: Expr = null
}
- object TVar { var VariableCount = 0 }
+ object S_TVar { var VariableCount = 0 }
def NewTVar(id: String) = {
val v = new Boogie.TVar(id, true)
val e = new Boogie.NamedType(v.id)
(v,e)
}
- var vsMode = false; // global variable settable from outside the class (non-ideal design)
-
// def out(s: String) = Console.out.print(s)
- var indentLevel = 1
+ private var indentLevel = 1
def indent: String = {
def doIndent(i: Int): String = {
if(i==0) { "" } else { " " + doIndent(i-1) }
@@ -163,7 +163,7 @@ object Boogie {
indentLevel = prev
result
}
- def nl = System.getProperty("line.separator");
+ private val nl = System.getProperty("line.separator");
def Print[T](list: List[T], sep: String, p: T => String): String = list match {
case Nil => ""
@@ -207,7 +207,7 @@ object Boogie {
def PrintStmt(s: Stmt): String = s match {
case Comment(msg) => indent + "// " + msg + nl
case assert@Assert(e) =>
- val pos = if (vsMode) {
+ val pos = if (Chalice.vsMode) {
val r = assert.pos.line - 1;
val c = assert.pos.column - 1;
r + "," + c + "," + r + "," + (c+5) + ":"
diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala
index 0ced872e..43b3a330 100644
--- a/Chalice/src/Chalice.scala
+++ b/Chalice/src/Chalice.scala
@@ -12,12 +12,32 @@ import scala.util.parsing.input.Position
import collection.mutable.ListBuffer
object Chalice {
- def main(args: Array[String]): Unit = {
- var boogiePath = "C:\\boogie\\Binaries\\Boogie.exe"
- val inputs = new ListBuffer[String]()
- var printProgram = false
- var vsMode = false;
- def ReportError(pos: Position, msg: String) = {
+ /**
+ * Reporting options
+ */
+ private[chalice] var vsMode = false;
+
+ /**
+ * Translation options
+ */
+ // level 0 or below: no defaults
+ // level 1: unfold predicates with receiver this in pre and postconditions
+ // level 2: unfold predicates and functions with receiver this in pre and postconditions
+ // level 3 or above: level 2 + autoMagic\
+ private[chalice] var defaults = 0: Int;
+ private[chalice] var autoFold = false: Boolean;
+ private[chalice] var checkLeaks = false: Boolean;
+ private[chalice] var autoMagic = false: Boolean;
+ private[chalice] var skipDeadlockChecks = false: Boolean;
+ private[chalice] var skipTermination = false: Boolean;
+ private[chalice] var noFreeAssume = false: Boolean;
+
+ def main(args: Array[String]): Unit = {
+ var boogiePath = "C:\\boogie\\Binaries\\Boogie.exe"
+ val inputs = new ListBuffer[String]()
+ var printProgram = false
+
+ def ReportError(pos: Position, msg: String) = {
if (vsMode) {
val r = pos.line - 1;
val c = pos.column - 1;
@@ -25,43 +45,34 @@ object Chalice {
} else {
Console.err.println(pos + ": " + msg)
}
- }
- var doTypecheck = true
- var doTranslate = true
- var checkLeaks = false
- // level 0 or below: no defaults
- // level 1: unfold predicates with receiver this in pre and postconditions
- // level 2: unfold predicates and functions with receiver this in pre and postconditions
- // level 3 or above: level 2 + autoMagic
- var defaults = 0
- var autoFold = false
- var autoMagic = false
- var skipDeadlockChecks = false
- var skipTermination = false;
- var boogieArgs = " ";
- var gen = false;
+ }
+ var doTypecheck = true
+ var doTranslate = true
+ var boogieArgs = " ";
+ var gen = false;
- // closures should be idempotent
- val options = Map(
+ // closures should be idempotent
+ val options = Map(
"-print" -> {() => printProgram = true},
"-noTranslate" -> {() => doTranslate = false},
"-noTypecheck"-> {() => doTypecheck = false},
"-vs" -> {() => vsMode = true},
"-checkLeaks" -> {() => checkLeaks = true},
"-noDeadlockChecks" -> {() => skipDeadlockChecks = true},
- "-noTermination" -> {() => skipTermination = true},
+ "-noTermination" -> {() => skipTermination = true},
"-defaults" -> {() => defaults = 3},
"-gen" -> {() => gen = true},
"-autoFold" -> {() => autoFold = true},
- "-autoMagic"-> {() => autoMagic = true}
- )
- lazy val help = options.keys.foldLeft("syntax: chalice")((s, o) => s + " [" + o + "]") +
- " [-boogie:path]" +
- " [-defaults:int]" +
- " [<boogie option>]*" +
- " <file.chalice>*";
+ "-autoMagic"-> {() => autoMagic = true},
+ "-noFreeAssume" -> {() => noFreeAssume = true}
+ )
+ lazy val help = options.keys.foldLeft("syntax: chalice")((s, o) => s + " [" + o + "]") +
+ " [-boogie:path]" +
+ " [-defaults:int]" +
+ " <boogie option>*" +
+ " <file.chalice>*";
- for (a <- args) {
+ for (a <- args) {
if (options contains a) options(a)()
else if (a == "-help") {Console.out.println(help); return}
else if (a.startsWith("-boogie:")) boogiePath = a.substring(8)
@@ -73,29 +84,30 @@ object Chalice {
}
else if (a.startsWith("-") || a.startsWith("/")) boogieArgs += (a + " ") // other arguments starting with "-" or "/" are sent to Boogie.exe
else inputs += a
- }
+ }
- // check that input files exist
- var files = for (input <- inputs.toList) yield {
+ // check that input files exist
+ var files = for (input <- inputs.toList) yield {
val file = new File(input);
if(! file.exists) {
- CommandLineError("input file " + file.getName() + " could not be found", help); return
+ CommandLineError("input file " + file.getName() + " could not be found", help);
+ return
}
file;
- }
+ }
- // parse programs
- val parser = new Parser();
- val parseResults = if (files.isEmpty) {
+ // parse programs
+ val parser = new Parser();
+ val parseResults = if (files.isEmpty) {
List(parser.parseStdin)
- } else for (file <- files) yield {
+ } else for (file <- files) yield {
parser.parseFile(file)
- }
-
- // report errors and merge declarations
- assert(parseResults.size > 0)
- var parseErrors = false;
- val program:List[TopLevelDecl] = parseResults.map(result => result match {
+ }
+
+ // report errors and merge declarations
+ assert(parseResults.size > 0)
+ var parseErrors = false;
+ val program:List[TopLevelDecl] = parseResults.map(result => result match {
case e:parser.NoSuccess =>
parseErrors = true;
if (vsMode)
@@ -106,11 +118,11 @@ object Chalice {
case parser.Success(prog, _) =>
if (printProgram) PrintProgram.P(prog)
prog
- }).flatten;
- if (parseErrors) return;
+ }).flatten;
+ if (parseErrors) return;
- // typecheck program
- if (doTypecheck) {
+ // typecheck program
+ if (doTypecheck) {
Resolver.Resolve(program) match {
case Resolver.Errors(msgs) =>
if (!vsMode) Console.err.println("The program did not typecheck.");
@@ -128,16 +140,8 @@ object Chalice {
}
// translate program to Boogie
val translator = new Translator();
- // set the translation options
- TranslationOptions.checkLeaks = checkLeaks;
- TranslationOptions.defaults = defaults;
- TranslationOptions.autoFold = autoFold;
- TranslationOptions.autoMagic = autoMagic;
- TranslationOptions.skipDeadlockChecks = skipDeadlockChecks;
- TranslationOptions.skipTermination = skipTermination;
val bplProg = translator.translateProgram(program);
// write to out.bpl
- Boogie.vsMode = vsMode;
val bplText = TranslatorPrelude.P + (bplProg map Boogie.Print).foldLeft(""){ (a, b) => a + b };
val bplFilename = if (vsMode) "c:\\tmp\\out.bpl" else "out.bpl"
writeFile(bplFilename, bplText);
@@ -179,19 +183,19 @@ object Chalice {
writeFile("out.cs", converter.convertProgram(program));
}
}
- }
- }
- }
+ }
+ }
+ }
- def writeFile(filename: String, text: String) {
+ def writeFile(filename: String, text: String) {
val writer = new FileWriter(new File(filename));
writer.write(text);
writer.flush();
writer.close();
- }
+ }
- def CommandLineError(msg: String, help: String) = {
+ def CommandLineError(msg: String, help: String) = {
Console.err.println("Error: " + msg)
Console.err.println(help);
- }
+ }
}
diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index 5c955d01..2802e7b8 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -75,8 +75,9 @@ object PrintProgram {
case BlockStmt(ss) =>
PrintBlockStmt(ss, indent); println
case RefinementBlock(ss, old) =>
- println("// begin of refinement block")
- for (s <- old) {Spaces(indent); print("// "); Stmt(s, indent)}
+ println("/* begin of refinement block")
+ for (s <- old) {Spaces(indent); Stmt(s, indent)}
+ Spaces(indent); println("end of abstract code */")
for (s <- ss) {Spaces(indent); Stmt(s, indent)}
Spaces(indent); println("// end of refinement block")
case IfStmt(guard, BlockStmt(thn), els) =>
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index c1c36cb5..e6c3db7b 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -14,20 +14,8 @@ import Boogie.Proc, Boogie.NamedType, Boogie.NewBVar, Boogie.Havoc, Boogie.Stmt,
case class ErrorMessage(pos: Position, message: String)
-object TranslationOptions {
- // note: the initial values should match those Chalice.scala
-
- var defaults = 0: Int;
- var autoFold = false: Boolean;
- var checkLeaks = false: Boolean;
- var autoMagic = false: Boolean;
- var skipDeadlockChecks = false: Boolean;
- var skipTermination = false: Boolean;
-}
-
class Translator {
import TranslationHelper._;
- import TranslationOptions._;
var currentClass = null: Class;
var modules = Nil: List[String]
var etran = new ExpressionTranslator(null);
@@ -103,7 +91,7 @@ class Translator {
Havoc(etran.Heap) ::
// check that invariant is well-defined
etran.WhereOldIs(h1, m1, c1).Inhale(invs map { mi => mi.e}, "monitor invariant", true) :::
- (if (!checkLeaks || invs.length == 0) Nil else
+ (if (! Chalice.checkLeaks || invs.length == 0) Nil else
// check that there are no loops among .mu permissions in monitors
// !CanWrite[this,mu]
bassert(!etran.CanWrite(VarExpr("this"), "mu"), invs(0).pos, "Monitor invariant is not allowed to hold write permission to this.mu") ::
@@ -130,7 +118,7 @@ class Translator {
def translateFunction(f: Function): List[Decl] = {
val myresult = BVar("result", f.out.typ);
- etran = etran.CheckTermination(!skipTermination);
+ etran = etran.CheckTermination(! Chalice.skipTermination);
val checkBody = f.definition match {case Some(e) => isDefined(e); case None => Nil};
etran = etran.CheckTermination(false);
// Boogie function that represents the Chalice function
@@ -143,13 +131,13 @@ class Translator {
DefaultPrecondition(),
DefinePreInitialState :::
// check definedness of the precondition
- InhaleWithChecking(Preconditions(f.spec) map { p => (if(0<defaults) UnfoldPredicatesWithReceiverThis(p) else p)}, "precondition") :::
+ InhaleWithChecking(Preconditions(f.spec) map { p => (if(0 < Chalice.defaults) UnfoldPredicatesWithReceiverThis(p) else p)}, "precondition") :::
bassume(CurrentModule ==@ VarExpr(ModuleName(currentClass))) :: // verify the body assuming that you are in the module
// check definedness of function body
checkBody :::
(f.definition match {case Some(e) => BLocal(myresult) :: (Boogie.VarExpr("result") := etran.Tr(e)); case None => Nil}) :::
// check that postcondition holds
- ExhaleWithChecking(Postconditions(f.spec) map { post => ((if(0<defaults) UnfoldPredicatesWithReceiverThis(post) else post),
+ 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")) ::
// definition axiom
(if (f.definition.isDefined) definitionAxiom(f) else Nil) :::
@@ -322,11 +310,11 @@ class Translator {
bassume(CurrentModule ==@ Boogie.VarExpr(ModuleName(currentClass))) ::
bassume(CanAssumeFunctionDefs) ::
DefinePreInitialState :::
- Inhale(Preconditions(method.spec) map { p => (if(0<defaults) UnfoldPredicatesWithReceiverThis(p) else p)}, "precondition") :::
+ Inhale(Preconditions(method.spec) map { p => (if(0 < Chalice.defaults) UnfoldPredicatesWithReceiverThis(p) else p)}, "precondition") :::
DefineInitialState :::
translateStatements(method.body) :::
- Exhale(Postconditions(method.spec) map { p => ((if(0<defaults) UnfoldPredicatesWithReceiverThis(p) else p), ErrorMessage(method.pos, "The postcondition at " + p.pos + " might not hold."))}, "postcondition") :::
- (if(checkLeaks) isLeaking(method.pos, "Method " + method.FullName + " might leak references.") else Nil) :::
+ Exhale(Postconditions(method.spec) map { p => ((if(0 < Chalice.defaults) UnfoldPredicatesWithReceiverThis(p) else p), ErrorMessage(method.pos, "The postcondition at " + p.pos + " might not hold."))}, "postcondition") :::
+ (if(Chalice.checkLeaks) isLeaking(method.pos, "Method " + method.FullName + " might leak references.") else Nil) :::
bassert(LockFrame(LockChanges(method.spec), etran), method.pos, "Method might lock/unlock more than allowed.") :::
bassert(DebtCheck, method.pos, "Method body is not allowed to leave any debt."))
}
@@ -354,13 +342,18 @@ class Translator {
mt.Outs map {i => Variable2BVarWhere(i)},
GlobalNames,
DefaultPrecondition(),
- bassume(CurrentModule ==@ Boogie.VarExpr(ModuleName(currentClass))) ::
- bassume(CanAssumeFunctionDefs) ::
- DefinePreInitialState :::
- Inhale(Preconditions(mt.Spec), "precondition") :::
- DefineInitialState :::
- translateStatements(mt.Body) :::
- Exhale(Postconditions(mt.Spec) map { p => (p, ErrorMessage(p.pos, "The postcondition at " + p.pos + " might not hold."))}, "postcondition")
+ assert2assume {
+ bassume(CurrentModule ==@ Boogie.VarExpr(ModuleName(currentClass))) ::
+ bassume(CanAssumeFunctionDefs) ::
+ DefinePreInitialState :::
+ Inhale(Preconditions(mt.Spec), "precondition") :::
+ DefineInitialState :::
+ translateStatements(mt.Body) :::
+ Exhale(Postconditions(mt.refines.Spec) map {p => (p, ErrorMessage(p.pos, "The postcondition at " + p.pos + " might not hold."))}, "postcondition") :::
+ tag(
+ Exhale(Postconditions(mt.spec) map {p => (p, ErrorMessage(p.pos, "The postcondition at " + p.pos + " might not hold."))}, "refinement postcondition"),
+ keepTag)
+ }
)
}
@@ -826,7 +819,7 @@ class Translator {
val (lastAcquireVar, lastAcquire) = Boogie.NewBVar("lastAcquire", IntClass, true)
val (lastSeenHeldV, lastSeenHeld) = Boogie.NewBVar("lastSeenHeld", tint, true)
val (lastSeenMuV, lastSeenMu) = Boogie.NewBVar("lastSeenMu", tmu, true)
- (if (skipDeadlockChecks)
+ (if (Chalice.skipDeadlockChecks)
bassume(CanRead(o, "mu")) ::
bassume(etran.MaxLockIsBelowX(etran.Heap.select(o,"mu")))
else
@@ -1065,22 +1058,23 @@ class Translator {
// run concrete C on the fresh heap
{
etran = conTran;
- Comment("run concrete program") ::
+ Comment("run concrete program:") ::
translateStatements(r.con)
} :::
// run angelically A on the old heap
- Comment("run abstract program") ::
- {r.abs match {
+ Comment("run abstract program:") ::
+ { etran = absTran;
+ r.abs match {
case List(s: SpecStmt) =>
- etran = absTran;
- Comment("witness declared local variables") ::
- (for (v <- duringA) yield BLocal(Variable2BVarWhere(v))) :::
- (for ((v, w) <- duringA zip duringC) yield (new VariableExpr(v) := new VariableExpr(w))) :::
- bassert(s.post, r.pos, "Refinement fails to satisfy specification statement post-condition") ::
- (for ((v, w) <- beforeV zip before; if (! s.lhs.exists(ve => ve.v == w))) yield
- bassert(new VariableExpr(v) ==@ new VariableExpr(w), r.pos, "Refinement may change a variable not in frame of the specification statement: " + v.id))
+ tag(
+ Comment("witness declared local variables") ::
+ (for (v <- duringA) yield BLocal(Variable2BVarWhere(v))) :::
+ (for ((v, w) <- duringA zip duringC) yield (new VariableExpr(v) := new VariableExpr(w))) :::
+ bassert(s.post, r.pos, "Refinement fails to satisfy specification statement post-condition") ::
+ (for ((v, w) <- beforeV zip before; if (! s.lhs.exists(ve => ve.v == w))) yield
+ bassert(new VariableExpr(v) ==@ new VariableExpr(w), r.pos, "Refinement may change a variable not in frame of the specification statement: " + v.id)),
+ keepTag)
case _ =>
- etran = absTran;
Comment("save locals after") ::
(for (v <- afterV) yield BLocal(Variable2BVarWhere(v))) :::
(for ((v, w) <- afterV zip before) yield (new VariableExpr(v) := new VariableExpr(w))) :::
@@ -1088,13 +1082,15 @@ class Translator {
(for ((v, w) <- before zip beforeV) yield (new VariableExpr(v) := new VariableExpr(w))) :::
translateStatements(r.abs) :::
Comment("assert equality on shared locals") ::
- (for ((v, w) <- afterV zip before) yield
- bassert(new VariableExpr(v) ==@ new VariableExpr(w), r.pos, "Refinement may produce different value for pre-state local variable: " + v.id)) :::
- (for ((v, w) <- duringA zip duringC) yield
- bassert(new VariableExpr(v) ==@ new VariableExpr(w), r.pos, "Refinement may produce different value for a declared local variable: " + v.id))
+ tag(
+ (for ((v, w) <- afterV zip before) yield
+ bassert(new VariableExpr(v) ==@ new VariableExpr(w), r.pos, "Refinement may produce different value for pre-state local variable: " + v.id)) :::
+ (for ((v, w) <- duringA zip duringC) yield
+ bassert(new VariableExpr(v) ==@ new VariableExpr(w), r.pos, "Refinement may produce different value for a declared local variable: " + v.id)),
+ keepTag)
}} :::
Comment("end of refinement block")
- // TODO: global coupling: assert coupling invariants for locations with positive
+ // TODO: global coupling: assert coupling invariants for locations with positive, preserve permissions?
}
@@ -1168,7 +1164,7 @@ class Translator {
}
def isLeaking(pos: Position, msg: String): List[Boogie.Stmt] = {
- if(checkLeaks) {
+ if(Chalice.checkLeaks) {
var o = Boogie.VarExpr("$o");
var f = "$f";
val (ttV,tt) = Boogie.NewTVar("T")
@@ -1297,7 +1293,6 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
assert(preGlobals.size == 3)
import TranslationHelper._
- import TranslationOptions._
val Heap = globals(0);
val Mask = globals(1);
@@ -1810,7 +1805,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
bassert(nonNull(Tr(e.e)), error.pos, error.message + " The target of the acc predicate at " + acc.pos + " might be null.") else Nil) :::
BLocal(fractionV) :: (frac := Tr(fraction)) ::
// if the mask does not contain sufficient permissions, try folding acc(e, fraction)
- (if(e.isPredicate && autoFold && (perm == Full || canTakeFractionOf(DefinitionOf(e.predicate)))) {
+ (if(e.isPredicate && Chalice.autoFold && (perm == Full || canTakeFractionOf(DefinitionOf(e.predicate)))) {
val inhaleTran = new ExpressionTranslator(List(Heap, em, Credits), currentClass);
val sourceVar = new Variable("fraction", new Type(IntClass));
val bplVar = Variable2BVar(sourceVar);
@@ -1843,7 +1838,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
dfP else Nil) :::
BLocal(epsilonsV) :: (if(epsilons!=null) (eps := Tr(epsilons)) :: Nil else Nil) :::
// if the mask does not contain sufficient permissions, try folding rdacc(e, epsilons)
- (if(e.isPredicate && autoFold && canTakeEpsilonsOf(DefinitionOf(e.predicate)) && epsilons!=null) {
+ (if(e.isPredicate && Chalice.autoFold && canTakeEpsilonsOf(DefinitionOf(e.predicate)) && epsilons!=null) {
val inhaleTran = new ExpressionTranslator(List(Heap, em, Credits), currentClass);
val sourceVar = new Variable("epsilons", new Type(IntClass));
val bplVar = Variable2BVar(sourceVar);
@@ -2198,7 +2193,7 @@ object TranslationHelper {
def PredicateField(f: String) = FunctionApp("PredicateField", List(VarExpr(f)))
def cast(a: Expr, b: Expr) = FunctionApp("cast", List(a, b))
- // Sequences
+ // sequences
def createEmptySeq = FunctionApp("Seq#Empty", List())
def createSingletonSeq(e: Expr) = FunctionApp("Seq#Singleton", List(e))
@@ -2326,7 +2321,7 @@ object TranslationHelper {
val result = spec flatMap ( s => s match {
case Precondition(e) => List(e)
case _ => Nil });
- if(autoMagic) {
+ if(Chalice.autoMagic) {
automagic(result.foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b)}), Nil)._1 ::: result
} else {
result
@@ -2336,7 +2331,7 @@ object TranslationHelper {
val result = spec flatMap ( s => s match {
case Postcondition(e) => List(e)
case _ => Nil })
- if(autoMagic) {
+ if(Chalice.autoMagic) {
automagic(result.foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b)}), Nil)._1 ::: result
} else {
result
@@ -2422,7 +2417,7 @@ object TranslationHelper {
}
def DefinitionOf(predicate: Predicate): Expression = {
- if(autoMagic) {
+ if(Chalice.autoMagic) {
And(automagic(predicate.definition, Nil)._1.foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b)}), predicate.definition)
} else {
predicate.definition
@@ -2561,5 +2556,26 @@ object TranslationHelper {
case _ => None;
}
}
+
+ val keepTag = Boogie.Tag("keep")
+ // Assume the only composite statement is If
+ def tag(l: List[Stmt], t: Boogie.Tag):List[Stmt] =
+ for (s <- l) yield {
+ s.tags = t :: s.tags;
+ s match {
+ case Boogie.If(_, thn, els) => tag(thn, t); tag(els, t);
+ case _ =>
+ }
+ s
+ }
+ // Assume the only composite statement is If
+ def assert2assume(l: List[Stmt]):List[Stmt] =
+ if (Chalice.noFreeAssume) l else
+ l flatMap {
+ case Boogie.If(guard, thn, els) => Boogie.If(guard, assert2assume(thn), assert2assume(els))
+ case ba @ Boogie.Assert(e) =>
+ if (ba.tags contains keepTag) ba else Comment(" assert " + ba.pos + ": " + ba.message) :: Boogie.Assume(e)
+ case s => s
+ }
}
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-15 07:51:43 +0000