diff options
Diffstat (limited to 'Chalice/src')
| -rw-r--r-- | Chalice/src/Chalice.scala | 53 | ||||
| -rw-r--r-- | Chalice/src/ChaliceToCSharp.scala | 5 | ||||
| -rw-r--r-- | Chalice/src/Prelude.scala | 21 | ||||
| -rw-r--r-- | Chalice/src/PrettyPrinter.scala | 11 | ||||
| -rw-r--r-- | Chalice/src/Resolver.scala | 3 | ||||
| -rw-r--r-- | Chalice/src/Translator.scala | 5 |
6 files changed, 68 insertions, 30 deletions
diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala index 49f6b74e..8e95a725 100644 --- a/Chalice/src/Chalice.scala +++ b/Chalice/src/Chalice.scala @@ -36,33 +36,47 @@ object Chalice { var autoFold = false
var autoMagic = false
var skipDeadlockChecks = false
+ var skipTermination = false;
var boogieArgs = " ";
var gen = false;
+ // 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},
+ "-defaults" -> {() => defaults = 3},
+ "-gen" -> {() => gen = true},
+ "-autoFold" -> {() => autoFold = true},
+ "-autoMagic"-> {() => autoMagic = true}
+ )
+ val help = options.keys.foldLeft("syntax: chalice")((s, o) => s + " [" + o + "]") +
+ " [-boogie:path]" +
+ " [-defaults:int]" +
+ " [<boogie option>]*" +
+ " <input file.chalice>";
+
for (a <- args) {
- if (a == "-print") printProgram = true
- else if (a == "-noTranslate") doTranslate = false
- else if (a == "-noTypecheck") doTypecheck = false
- else if (a == "-vs") vsMode = true
- else if (a == "-checkLeaks") checkLeaks = true
- else if (a == "-noDeadlockChecks") skipDeadlockChecks = true
+ if (options contains a) options(a)()
+ else if (a == "-help") {Console.out.println(help); return}
else if (a.startsWith("-boogie:")) boogiePath = a.substring(8)
- else if (a == "-defaults") defaults = 3
- else if (a.startsWith("-defaults:")) { try { defaults = Integer.parseInt(a.substring(10)); if(3<=defaults) { autoMagic = true; } } catch { case _ => CommandLineError("-defaults takes integer argument"); } }
- else if (a == "-gen") { gen = true; }
- else if (a == "-autoFold") autoFold = true
- else if (a == "-autoMagic") autoMagic = true
- else if (a.startsWith("-") || a.startsWith("/")) boogieArgs += (a + " ") // arguments starting with "-" or "/" are sent to Boogie.exe
- else if (inputName != null) { CommandLineError("multiple input filenames: " + inputName + " and " + a); return }
+ else if (a.startsWith("-defaults:")) { try { defaults = Integer.parseInt(a.substring(10)); if(3<=defaults) { autoMagic = true; } } catch { case _ => CommandLineError("-defaults takes integer argument", help); } }
+ else if (a.startsWith("-") || a.startsWith("/")) boogieArgs += (a + " ") // other arguments starting with "-" or "/" are sent to Boogie.exe
+ else if (inputName != null) { CommandLineError("multiple input filenames: " + inputName + " and " + a, help); return }
else { inputName = a }
}
+
// check the command-line arguments
if (inputName == null && vsMode) {
inputName = "<stdin>"
- } else if (inputName == null) { CommandLineError("missing input filename"); return } else {
+ } else if (inputName == null) { CommandLineError("missing input filename", help); return } else {
val file = new File(inputName);
if(! file.exists()){
- CommandLineError("input file " + file.getName() + " could not be found"); return
+ CommandLineError("input file " + file.getName() + " could not be found", help); return
}
}
// parse program
@@ -86,7 +100,7 @@ object Chalice { // checking if Boogie.exe exists
val boogieFile = new File(boogiePath);
if(! boogieFile.exists() || ! boogieFile.isFile()) {
- CommandLineError("Boogie.exe not found at " + boogiePath); return
+ CommandLineError("Boogie.exe not found at " + boogiePath, help); return
}
// translate program to Boogie
val translator = new Translator();
@@ -96,6 +110,7 @@ object Chalice { TranslationOptions.autoFold = autoFold;
TranslationOptions.autoMagic = autoMagic;
TranslationOptions.skipDeadlockChecks = skipDeadlockChecks;
+ TranslationOptions.skipTermination = skipTermination;
val bplProg = translator.translateProgram(prog);
// write to out.bpl
Boogie.vsMode = vsMode;
@@ -130,8 +145,8 @@ object Chalice { writer.close();
}
- def CommandLineError(msg: String) = {
+ def CommandLineError(msg: String, help: String) = {
Console.err.println("Error: " + msg)
- Console.err.println("syntax: chalice [-print] [-noTypecheck] [-noTranslate] [-vs] [-boogie:path] [-defaults] [-autoFold] [-checkLeaks] [-noDeadlockChecks] inputFile")
- }
+ Console.err.println(help);
+ }
}
diff --git a/Chalice/src/ChaliceToCSharp.scala b/Chalice/src/ChaliceToCSharp.scala index f759831b..0c35bd5b 100644 --- a/Chalice/src/ChaliceToCSharp.scala +++ b/Chalice/src/ChaliceToCSharp.scala @@ -98,7 +98,10 @@ class ChaliceToCSharp { def convertStatement(statement: Statement): String = {
statement match {
case Assert(e) => indent + "// assert" + nl
- case Assume(e) => indent + "assert " + convertExpression(e) + ";" // todo: what if e contains old, result, ...
+ case Assume(e) => indent + {e match {
+ case BoolLiteral(false) => "assert false;" + nl // abort since we made a wrong choice...
+ case _ => // TODO: what to do with assume expressions that contain old, result, ghost variables, etc.
+ "// assume" + nl}}
case BlockStmt(ss) => indent + "{" + nl + (indentMore { rep(ss map convertStatement) }) + indent + "}" + nl
case IfStmt(guard, thn, els) => indent + "if (" + convertExpression(guard) + ")" + nl + convertStatement(thn) +
(if(els.isDefined) (indent + "else" + nl + convertStatement(els.get)) else { "" }) + nl
diff --git a/Chalice/src/Prelude.scala b/Chalice/src/Prelude.scala index 2fb58697..b4994889 100644 --- a/Chalice/src/Prelude.scala +++ b/Chalice/src/Prelude.scala @@ -101,10 +101,18 @@ function IsGoodInhaleState(ih: HeapType, h: HeapType, (forall o: ref :: { h[o, rdheld] } h[o, rdheld] ==> ih[o, mu] == h[o, mu])
}
+// ---------------------------------------------------------------
+// -- If then else -----------------------------------------------
+// ---------------------------------------------------------------
+
function ite<T>(bool, T, T) returns (T);
axiom (forall<T> con: bool, a: T, b: T :: {ite(con, a, b)} con ==> ite(con, a, b) == a);
axiom (forall<T> con: bool, a: T, b: T :: {ite(con, a, b)} ! con ==> ite(con, a, b) == b);
+// ---------------------------------------------------------------
+// -- Axiomatization of sequences --------------------------------
+// ---------------------------------------------------------------
+
type Seq T;
function Seq#Length<T>(Seq T) returns (int);
@@ -182,7 +190,7 @@ axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) } 0 <= n ==>
(n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) &&
(Seq#Length(s) < n ==> Seq#Length(Seq#Take(s,n)) == Seq#Length(s)));
-axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) }
+axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) } {:weight 25}
0 <= j && j < n && j < Seq#Length(s) ==>
Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j));
@@ -191,15 +199,24 @@ axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) } 0 <= n ==>
(n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) &&
(Seq#Length(s) < n ==> Seq#Length(Seq#Drop(s,n)) == 0));
-axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) }
+axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) } {:weight 25}
0 <= n && 0 <= j && j < Seq#Length(s)-n ==>
Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, j+n));
+axiom (forall<T> s, t: Seq T ::
+ { Seq#Append(s, t) }
+ Seq#Take(Seq#Append(s, t), Seq#Length(s)) == s &&
+ Seq#Drop(Seq#Append(s, t), Seq#Length(s)) == t);
+
function Seq#Range(min: int, max: int) returns (Seq int);
axiom (forall min: int, max: int :: { Seq#Length(Seq#Range(min, max)) } (min < max ==> Seq#Length(Seq#Range(min, max)) == max-min) && (max <= min ==> Seq#Length(Seq#Range(min, max)) == 0));
axiom (forall min: int, max: int, j: int :: { Seq#Index(Seq#Range(min, max), j) } 0<=j && j<max-min ==> Seq#Index(Seq#Range(min, max), j) == min + j);
+// ---------------------------------------------------------------
+// -- Permissions ------------------------------------------------
+// ---------------------------------------------------------------
+
axiom (forall h: HeapType, m: MaskType, o: ref, q: ref :: {wf(h, m), h[o, mu], h[q, mu]} wf(h, m) && o!=q && (0 < h[o, held] || h[o, rdheld]) && (0 < h[q, held] || h[q, rdheld]) ==> h[o, mu] != h[q, mu]);
function DecPerm<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala index af068b23..82e7658c 100644 --- a/Chalice/src/PrettyPrinter.scala +++ b/Chalice/src/PrettyPrinter.scala @@ -41,19 +41,22 @@ object PrintProgram { print(" condition " + id)
optE match {
case None =>
- case Some(e) => print(" where " + Expr(e))
+ case Some(e) => print(" where "); Expr(e)
}
println(Semi)
case Predicate(id, definition) =>
- println(" predicate " + id + " { " + Expr(definition) + "}")
+ print(" predicate " + id + " { "); Expr(definition); println(" }")
case Function(id, ins, out, specs, e) =>
- print(" function " + id + "(" + VarList(ins) + ")" + ": " + out.id);
+ print(" function " + id + "("); VarList(ins); print("): " + out.FullName);
+ println
specs foreach {
case Precondition(e) => print(" requires "); Expr(e); println(Semi)
case Postcondition(e) => print(" ensures "); Expr(e); println(Semi)
case LockChange(ee) => print(" lockchange "); ExprList(ee); println(Semi)
}
- print(" { " + Expr(e) + "}");
+ print(" { ");
+ Expr(e);
+ println(" }");
}
def Stmt(s: Statement, indent: Int): Unit = s match {
case Assert(e) =>
diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala index 91bc1ede..c14b68c8 100644 --- a/Chalice/src/Resolver.scala +++ b/Chalice/src/Resolver.scala @@ -214,9 +214,8 @@ object Resolver { ResolveExpr(e, context, true, true)(false)
if (!e.typ.IsBool) context.Error(e.pos, "assert statement requires a boolean expression (found " + e.typ.FullName + ")")
case Assume(e) =>
- ResolveExpr(e, context, false, false)(false) // assume expressions remain at run-time, so OLD is not allowed
+ ResolveExpr(e, context, true, true)(false)
if (!e.typ.IsBool) context.Error(e.pos, "assume statement requires a boolean expression (found " + e.typ.FullName + ")")
- CheckNoGhost(e, context)
case BlockStmt(ss) =>
var ctx = context
for (s <- ss) s match {
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index e5a59385..ff840986 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -20,6 +20,7 @@ object TranslationOptions { var checkLeaks = false: Boolean;
var autoMagic = false: Boolean;
var skipDeadlockChecks = false: Boolean;
+ var skipTermination = false: Boolean;
}
class Translator {
@@ -124,7 +125,7 @@ class Translator { def translateFunction(f: Function): List[Decl] = {
val myresult = BVar("result", f.out.typ);
- etran.checkTermination = true;
+ etran.checkTermination = !skipTermination;
val checkBody = isDefined(f.definition);
etran.checkTermination = false;
// Boogie function that represents the Chalice function
@@ -1110,7 +1111,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E val Mask = globals(1);
val Credits = globals(2);
lazy val oldEtran = new ExpressionTranslator(preGlobals, preGlobals, currentClass)
- var checkTermination = false; // check that heap required by callee is strictly smaller than heap required by caller
+ var checkTermination = false;
def this(globals: List[Boogie.Expr], cl: Class) = this(globals, globals map (g => Boogie.Old(g)), cl)
def this(cl: Class) = this(for ((id,t) <- S_ExpressionTranslator.Globals) yield Boogie.VarExpr(id), cl)
|