diff options
| -rw-r--r-- | Chalice/src/Ast.scala | 32 | ||||
| -rw-r--r-- | Chalice/src/Chalice.scala | 182 | ||||
| -rw-r--r-- | Chalice/src/Parser.scala | 116 | ||||
| -rw-r--r-- | Chalice/src/Translator.scala | 51 | ||||
| -rw-r--r-- | Chalice/test.bat | 2 |
5 files changed, 209 insertions, 174 deletions
diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala index 53c2093d..4f63f57b 100644 --- a/Chalice/src/Ast.scala +++ b/Chalice/src/Ast.scala @@ -10,7 +10,9 @@ import scala.util.parsing.input.Positional trait ASTNode extends Positional
-// classes and types
+/**
+ * Classes and types
+ */
case class TopLevelDecl(id: String) extends ASTNode
@@ -115,7 +117,9 @@ sealed case class TokenType(C: Type, m: String) extends Type("token", Nil) { // override def FullName: String = "token<" + C.FullName + "." + m + ">"
}
-// members
+/**
+ * Members
+ */
sealed abstract class Member extends ASTNode {
val Hidden: Boolean = false // hidden means not mentionable in source
@@ -167,7 +171,9 @@ case class Precondition(e: Expression) extends Specification case class Postcondition(e: Expression) extends Specification
case class LockChange(ee: List[Expression]) extends Specification
-// statements
+/**
+ * Statements
+ */
sealed abstract class Statement extends ASTNode
case class Assert(e: Expression) extends Statement
@@ -197,6 +203,9 @@ case class Call(declaresLocal: List[Boolean], lhs: List[VariableExpr], obj: Expr var locals = List[Variable]()
var m: Method = null
}
+case class Spec(declaresLocal: List[Boolean], lhs: List[VariableExpr], pred: Expression) extends Statement {
+ var locals = List[Variable]()
+}
case class Install(obj: Expression, lowerBounds: List[Expression], upperBounds: List[Expression]) extends Statement
case class Share(obj: Expression, lowerBounds: List[Expression], upperBounds: List[Expression]) extends Statement
case class Unshare(obj: Expression) extends Statement
@@ -228,7 +237,9 @@ case class Receive(declaresLocal: List[Boolean], ch: Expression, outs: List[Vari case class Fold(pred: Access) extends Statement
case class Unfold(pred: Access) extends Statement
-// expressions
+/**
+ * Expressions
+ */
sealed abstract class RValue extends ASTNode {
var typ: Class = null
@@ -370,7 +381,10 @@ case class LockBelow(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) override val OpName = "<<"
}
-// quantifiers
+/**
+ * Expressions: quantifiers
+ */
+
trait Quant
object Forall extends Quant
object Exists extends Quant
@@ -384,7 +398,9 @@ sealed abstract class Quantification(q: Quant, is: List[String], e: Expression) case class SeqQuantification(q: Quant, is: List[String], seq: Expression, e: Expression) extends Quantification(q, is, e)
case class TypeQuantification(q: Quant, is: List[String], t: Type, e: Expression) extends Quantification(q, is, e)
-// sequences
+/**
+ * Expressions: sequences
+ */
case class EmptySeq(t: Type) extends Literal
case class ExplicitSeq(elems: List[Expression]) extends Expression
@@ -428,7 +444,9 @@ case class CallState(token: Expression, obj: Expression, id: String, args: List[ def target() = token;
}
-// visitors / operations
+/**
+ * AST operations
+ */
object AST {
/**
diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala index 0342964b..449db023 100644 --- a/Chalice/src/Chalice.scala +++ b/Chalice/src/Chalice.scala @@ -9,12 +9,12 @@ import java.io.InputStreamReader import java.io.File
import java.io.FileWriter
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"
- // parse command-line arguments
- var inputName: String = null
+ val inputs = new ListBuffer[String]()
var printProgram = false
var vsMode = false;
def ReportError(pos: Position, msg: String) = {
@@ -55,109 +55,127 @@ object Chalice { "-autoFold" -> {() => autoFold = true},
"-autoMagic"-> {() => autoMagic = true}
)
- val help = options.keys.foldLeft("syntax: chalice")((s, o) => s + " [" + o + "]") +
+ lazy val help = options.keys.foldLeft("syntax: chalice")((s, o) => s + " [" + o + "]") +
" [-boogie:path]" +
" [-defaults:int]" +
" [<boogie option>]*" +
- " <input file.chalice>";
+ " <file.chalice>";
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)
- 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("-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 }
+ else inputs += a
}
- // check the command-line arguments
- if (inputName == null && vsMode) {
- inputName = "<stdin>"
- } else if (inputName == null) { CommandLineError("missing input filename", help); return } else {
- val file = new File(inputName);
- if(! file.exists()){
+ // 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
}
+ file;
}
- // parse program
+
+ // parse programs
val parser = new Parser();
- parser.parseFile(inputName) match {
- case e: parser.NoSuccess =>
+ val parseResults = if (files.isEmpty) {
+ List(parser.parseStdin)
+ } 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 {
+ case e:parser.NoSuccess =>
+ parseErrors = true;
if (vsMode)
ReportError(e.next.pos, e.msg);
else
- Console.err.println("Error: " + e)
+ Console.err.println("Error: " + e);
+ Nil
case parser.Success(prog, _) =>
if (printProgram) PrintProgram.P(prog)
- if (doTypecheck) {
- // typecheck program
- Resolver.Resolve(prog) match {
- case Resolver.Errors(msgs) =>
- if (!vsMode) Console.err.println("The program did not typecheck.");
- msgs foreach { msg => ReportError(msg._1, msg._2) }
- case Resolver.Success() =>
- if (doTranslate) {
- // checking if Boogie.exe exists
- val boogieFile = new File(boogiePath);
- if(! boogieFile.exists() || ! boogieFile.isFile()) {
- CommandLineError("Boogie.exe not found at " + boogiePath, help); return
- }
- // 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(prog);
- // 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);
- // run Boogie.exe on out.bpl
- val boogie = Runtime.getRuntime.exec(boogiePath + " /errorTrace:0 " + boogieArgs + bplFilename);
- // terminate boogie if interrupted
- Runtime.getRuntime.addShutdownHook(new Thread(new Runnable() {
- def run {
- val kill = Runtime.getRuntime.exec("taskkill /T /F /IM Boogie.exe");
- kill.waitFor;
- // just to be sure
- boogie.destroy
- }
- }))
- // the process blocks until we exhaust input and error streams
- new Thread(new Runnable() {
- def run {
- val err = new BufferedReader(new InputStreamReader(boogie.getErrorStream));
- var line = err.readLine;
- while(line!=null) {Console.err.println(line); Console.err.flush}
- }
- }).start;
- val input = new BufferedReader(new InputStreamReader(boogie.getInputStream));
- var line = input.readLine();
- var previous_line = null: String;
- while(line!=null){
- Console.out.println(line);
- Console.out.flush;
- previous_line = line;
- line = input.readLine();
- }
- boogie.waitFor;
- input.close;
+ prog
+ }).flatten;
+ if (parseErrors) return;
- // generate code
- if(gen && (previous_line != null) && previous_line.endsWith(" 0 errors")) { // hack
- val converter = new ChaliceToCSharp();
- println("Code generated in out.cs.");
- writeFile("out.cs", converter.convertProgram(prog));
- }
+ // typecheck program
+ if (doTypecheck) {
+ Resolver.Resolve(program) match {
+ case Resolver.Errors(msgs) =>
+ if (!vsMode) Console.err.println("The program did not typecheck.");
+ msgs foreach { msg => ReportError(msg._1, msg._2) }
+ case Resolver.Success() =>
+ if (doTranslate) {
+ // checking if Boogie.exe exists
+ val boogieFile = new File(boogiePath);
+ if(! boogieFile.exists() || ! boogieFile.isFile()) {
+ CommandLineError("Boogie.exe not found at " + boogiePath, help); return
+ }
+ // 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);
+ // run Boogie.exe on out.bpl
+ val boogie = Runtime.getRuntime.exec(boogiePath + " /errorTrace:0 " + boogieArgs + bplFilename);
+ // terminate boogie if interrupted
+ Runtime.getRuntime.addShutdownHook(new Thread(new Runnable() {
+ def run {
+ val kill = Runtime.getRuntime.exec("taskkill /T /F /IM Boogie.exe");
+ kill.waitFor;
+ // just to be sure
+ boogie.destroy
}
+ }))
+ // the process blocks until we exhaust input and error streams
+ new Thread(new Runnable() {
+ def run {
+ val err = new BufferedReader(new InputStreamReader(boogie.getErrorStream));
+ var line = err.readLine;
+ while(line!=null) {Console.err.println(line); Console.err.flush}
+ }
+ }).start;
+ val input = new BufferedReader(new InputStreamReader(boogie.getInputStream));
+ var line = input.readLine();
+ var previous_line = null: String;
+ while(line!=null){
+ Console.out.println(line);
+ Console.out.flush;
+ previous_line = line;
+ line = input.readLine();
+ }
+ boogie.waitFor;
+ input.close;
+
+ // generate code
+ if(gen && (previous_line != null) && previous_line.endsWith(" 0 errors")) { // hack
+ val converter = new ChaliceToCSharp();
+ println("Code generated in out.cs.");
+ writeFile("out.cs", converter.convertProgram(program));
}
- }
+ }
+ }
}
}
diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala index 8999add9..b57a5ea4 100644 --- a/Chalice/src/Parser.scala +++ b/Chalice/src/Parser.scala @@ -10,17 +10,12 @@ import scala.collection.immutable.PagedSeq import scala.util.parsing.input.Position
import scala.util.parsing.input.Positional
import scala.util.parsing.input.NoPosition
+import java.io.File
class Parser extends StandardTokenParsers {
- def parseFile(path: String): this.ParseResult[List[TopLevelDecl]] = {
- val tokens = if (path == "<stdin>") {
- new lexical.Scanner(new PagedSeqReader(PagedSeq fromReader Console.in))
- } else {
- new lexical.Scanner(new PagedSeqReader(PagedSeq fromFile path));
- }
- phrase(programUnit)(tokens)
- }
+ def parseStdin = phrase(programUnit)(new lexical.Scanner(new PagedSeqReader(PagedSeq fromReader Console.in)))
+ def parseFile(file: File) = phrase(programUnit)(new lexical.Scanner(new PagedSeqReader(PagedSeq fromFile file)))
case class PositionedString(v: String) extends Positional
@@ -44,8 +39,12 @@ class Parser extends StandardTokenParsers { ";", ":", ":=", ",", "?", "|", "[", "]", "++", "::")
def programUnit = (classDecl | channelDecl)*
+ def Semi = ";" ?
+ var currentLocalVariables = Set[String]() // used in the method context
- // class and members
+ /**
+ * Top level declarations
+ */
def classDecl =
positioned(("external" ?) ~ ("class" ~> ident) ~ opt("module" ~> ident) ~ "{" ~ (memberDecl*) <~ "}" ^^ {
@@ -54,31 +53,22 @@ class Parser extends StandardTokenParsers { ext match { case None => case Some(t) => cl.IsExternal = true }
cl
})
- def memberDecl = positioned(fieldDecl | invariantDecl | methodDecl | conditionDecl |
- predicateDecl | functionDecl)
+ def channelDecl =
+ "channel" ~> ident ~ formalParameters(true) ~ ("where" ~> expression ?) <~ Semi ^^ {
+ case id ~ ins ~ None => Channel(id, ins, BoolLiteral(true))
+ case id ~ ins ~ Some(e) => Channel(id, ins, e)
+ }
+ /**
+ * Member declarations
+ */
+
+ def memberDecl = positioned(fieldDecl | invariantDecl | methodDecl | conditionDecl | predicateDecl | functionDecl)
def fieldDecl =
( "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id, t, false) }
| "ghost" ~> "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id, t, true) }
)
- def Ident =
- positioned(ident ^^ PositionedString)
- def idType =
- idTypeOpt ^^ {
- case (id, None) => (id, Type("int", Nil))
- case (id, Some(t)) => (id, t) }
- def idTypeOpt =
- ident ~ (":" ~> typeDecl ?) ^^ { case id ~ optT => (id, optT) }
- def typeDecl: Parser[Type] =
- positioned(("int" | "bool" | ident | "seq") ~ opt("<" ~> repsep(typeDecl, ",") <~ ">") ^^ { case t ~ parameters => Type(t, parameters.getOrElse(Nil)) }
- | ("token" ~ "<") ~> (typeDecl <~ ".") ~ ident <~ ">" ^^ { case c ~ m => TokenType(c, m) }
- )
- def Semi = ";" ?
-
- var currentLocalVariables = Set[String]()
-
def invariantDecl = positioned("invariant" ~> expression <~ Semi ^^ MonitorInvariant)
-
def methodDecl = {
currentLocalVariables = Set[String]()
"method" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~
@@ -88,51 +78,60 @@ class Parser extends StandardTokenParsers { case None => Method(id, ins, Nil, spec, body)
case Some(outs) => Method(id, ins, outs, spec, body) }}
}
- def channelDecl =
- "channel" ~> ident ~ formalParameters(true) ~ ("where" ~> expression ?) <~ Semi ^^ {
- case id ~ ins ~ None => Channel(id, ins, BoolLiteral(true))
- case id ~ ins ~ Some(e) => Channel(id, ins, e)
- }
- def predicateDecl: Parser[Predicate] =
+ def predicateDecl: Parser[Predicate] =
("predicate" ~> ident) ~ ("{" ~> expression <~ "}") ^^ { case id ~ definition => Predicate(id, definition) }
def functionDecl =
- ("function" ~> ident) ~ formalParameters(true) ~ (":" ~> typeDecl) ~ (methodSpec*) ~ opt("{" ~> expression <~ "}") ^^ { case id ~ ins ~ out ~ specs ~ body => Function(id, ins, out, specs, body) }
+ ("function" ~> ident) ~ formalParameters(true) ~ (":" ~> typeDecl) ~ (methodSpec*) ~ opt("{" ~> expression <~ "}") ^^ {
+ case id ~ ins ~ out ~ specs ~ body => Function(id, ins, out, specs, body)
+ }
+ def conditionDecl =
+ "condition" ~> ident ~ ("where" ~> expression ?) <~ Semi ^^ {
+ case id ~ optE => Condition(id, optE) }
+
def formalParameters(immutable: Boolean) =
"(" ~> (formalList(immutable) ?) <~ ")" ^^ {
case None => Nil
case Some(ids) => ids }
- def formalList(immutable: Boolean) = {
- repsep(formal(immutable), ",")
- }
+ def formalList(immutable: Boolean) = repsep(formal(immutable), ",")
def formal(immutable: Boolean): Parser[Variable] =
idType ^^ {case (id,t) =>
currentLocalVariables = currentLocalVariables + id;
- if (immutable)
- new ImmutableVariable(id,t)
- else
- new Variable(id,t)
+ if (immutable) new ImmutableVariable(id,t)
+ else new Variable(id,t)
}
+ def Ident = positioned(ident ^^ PositionedString)
+ def idType =
+ idTypeOpt ^^ {
+ case (id, None) => (id, Type("int", Nil))
+ case (id, Some(t)) => (id, t) }
+ def idTypeOpt =
+ ident ~ (":" ~> typeDecl ?) ^^ { case id ~ optT => (id, optT) }
+ def typeDecl: Parser[Type] =
+ positioned(("int" | "bool" | ident | "seq") ~ opt("<" ~> repsep(typeDecl, ",") <~ ">") ^^ { case t ~ parameters => Type(t, parameters.getOrElse(Nil)) }
+ | ("token" ~ "<") ~> (typeDecl <~ ".") ~ ident <~ ">" ^^ { case c ~ m => TokenType(c, m) }
+ )
+
+ /**
+ * Pre and post conditions
+ */
+
def methodSpec =
positioned( "requires" ~> expression <~ Semi ^^ Precondition
| "ensures" ~> expression <~ Semi ^^ Postcondition
| "lockchange" ~> expressionList <~ Semi ^^ LockChange
)
- def blockStatement: Parser[List[Statement]] = {
- "{" ~> blockStatementBody <~ "}"
- }
+
+ /**
+ * Statements
+ */
+
+ def blockStatement: Parser[List[Statement]] = "{" ~> blockStatementBody <~ "}"
def blockStatementBody: Parser[List[Statement]] = {
val prev = currentLocalVariables
(statement*) ^^ {
case x => currentLocalVariables = prev; x }
}
-
- def conditionDecl =
- "condition" ~> ident ~ ("where" ~> expression ?) <~ Semi ^^ {
- case id ~ optE => Condition(id, optE) }
-
- // statements
-
def statement: Parser[Statement] =
positioned( "assert" ~> expression <~ Semi ^^ Assert
| "assume" ~> expression <~ Semi ^^ Assume
@@ -316,9 +315,11 @@ class Parser extends StandardTokenParsers { case l ~ None => (l,Nil)
case l ~ Some(u) => (l,u) }
)
-
- // expressions
+ /**
+ * Expressions
+ */
+
def expressionList =
repsep(expression, ",")
def expression = positioned(iteExpr)
@@ -400,7 +401,6 @@ class Parser extends StandardTokenParsers { def exprBody =
"{" ~> expression <~ "}"
- // what is "FerSure"?
def selectExprFerSure: Parser[MemberAccess] =
positioned(atom ~ "." ~ ident ~ ("." ~> ident *) ^^ {
case e ~ _ ~ field ~ moreFields =>
@@ -486,28 +486,22 @@ class Parser extends StandardTokenParsers { | ("[" ~> expressionList <~ "]") ^^ { case es => ExplicitSeq(es) }
)
- // Scala type inference resists figuring out | (alternative) for these two
-
def quantifierSeq: Parser[Quantification] =
(quant ~ repsep(ident, ",")) into {case q ~ is => quantifierSeqBody(q, is)}
-
def quantifierSeqBody(q: Quant, is: List[String]) : Parser[Quantification] =
(("in" ~> expression <~ "::") ~ (exprWithLocals(is))) ^^
{ case seq ~ e =>
currentLocalVariables = currentLocalVariables -- is;
SeqQuantification(q, is, seq, e);
}
-
def quantifierType: Parser[Quantification] =
(quant ~ repsep(ident, ",")) into {case q ~ is => quantifierTypeBody(q, is)}
-
def quantifierTypeBody(q: Quant, is: List[String]) : Parser[Quantification] =
((":" ~> typeDecl <~ "::") ~ (exprWithLocals(is))) ^^
{ case t ~ e =>
currentLocalVariables = currentLocalVariables -- is;
TypeQuantification(q, is, t, e);
}
-
def quant: Parser[Quant] =
( "forall" ^^^ Forall | "exists" ^^^ Exists)
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index 45d875f0..d5ddfdcd 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -77,6 +77,8 @@ class Translator { translatePredicate(pred)
case inv: MonitorInvariant =>
Nil // already dealt with before
+ case _: Condition =>
+ throw new Exception("not yet implemented")
}
}
@@ -159,40 +161,41 @@ class Translator { def definitionAxiom(f: Function): List[Decl] = {
assert(f.definition.isDefined)
val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)});
- val frameFunctionName = "##" + f.FullName;
-
- /* axiom (forall h: HeapType, m: MaskType, this: ref, x_1: t_1, ..., x_n: t_n ::
- wf(h, m) && CurrentModule == module#C ==> #C.f(h, m, this, x_1, ..., x_n) == tr(body))
- */
val args = VarExpr("this") :: inArgs;
- var formals = BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar);
+ val formals = BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar);
val applyF = FunctionApp(functionName(f), List(etran.Heap, etran.Mask) ::: args);
- /** Limit application of the function by introducing a second limited function */
- val body = etran.Tr(if (f.isRecursive) {
- val limited = Map() ++ (f.SCC zip (f.SCC map {f =>
- val result = Function(f.id + "#limited", f.ins, f.out, f.spec, f.definition);
- result.Parent = f.Parent;
- result;
- }));
- def limit: Expression => Option[Expression] = _ match {
- case app @ FunctionApplication(obj, id, args) if (f.SCC contains app.f) =>
- val result = FunctionApplication(obj transform limit, id, args map (e => e transform limit));
- result.f = limited(app.f);
- Some(result)
- case _ => None
+ /** Limit application of the function by introducing a second (limited) function */
+ val body = etran.Tr(
+ if (f.isRecursive && ! f.isUnlimited) {
+ val limited = Map() ++ (f.SCC zip (f.SCC map {f =>
+ val result = Function(f.id + "#limited", f.ins, f.out, f.spec, f.definition);
+ result.Parent = f.Parent;
+ result;
+ }));
+ def limit: Expression => Option[Expression] = _ match {
+ case app @ FunctionApplication(obj, id, args) if (f.SCC contains app.f) =>
+ val result = FunctionApplication(obj transform limit, id, args map (e => e transform limit));
+ result.f = limited(app.f);
+ Some(result)
+ case _ => None
+ }
+ f.definition.get transform limit;
+ } else {
+ f.definition.get
}
- f.definition.get transform limit;
- } else
- f.definition.get);
+ );
+ /* axiom (forall h: HeapType, m: MaskType, this: ref, x_1: t_1, ..., x_n: t_n ::
+ wf(h, m) && CurrentModule == module#C ==> #C.f(h, m, this, x_1, ..., x_n) == tr(body))
+ */
Axiom(new Boogie.Forall(
formals, new Trigger(applyF),
(wf(VarExpr(HeapName), VarExpr(MaskName)) && (CurrentModule ==@ ModuleName(currentClass)))
==>
(applyF ==@ body))) ::
(if (f.isRecursive)
- // define the limited function
+ // define the limited function (even for unlimited function since its SCC might have limited functions)
Boogie.Function(functionName(f) + "#limited", formals, BVar("$myresult", f.out.typ)) ::
Axiom(new Boogie.Forall(
formals, new Trigger(applyF),
@@ -1553,6 +1556,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E case Frac(p) => (Tr(p), 0) : (Expr, Expr)
case Epsilon => (0, 1) : (Expr, Expr) // TODO: check for infinity bounds -- or perhaps just wait till epsilons are gone
case Epsilons(p) => (0, Tr(p)) : (Expr, Expr)
+ case Star => throw new Exception("not yet implemented")
};
(if (check) isDefined(s)(true) ::: isDefined(perm)(true) else Nil) :::
@@ -1731,6 +1735,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E case Frac(p) => (p, 0) : (Expr, Expr)
case Epsilon => (0, 1) : (Expr, Expr) // TODO: check for infinity bounds -- or perhaps just wait till epsilons are gone
case Epsilons(p) => (0, p) : (Expr, Expr)
+ case Star => throw new Exception("not yet implemented")
};
(if (check) isDefined(s)(true) ::: isDefined(perm)(true) else Nil) :::
diff --git a/Chalice/test.bat b/Chalice/test.bat index 9bc0f5ea..b45207b6 100644 --- a/Chalice/test.bat +++ b/Chalice/test.bat @@ -1,7 +1,7 @@ @echo off
echo start > Output
-set CHALICE=call scala -cp bin Chalice -nologo -boogie:"C:\\Users\\t-kuayes\\Documents\\Boogie-2010-07-13\\Boogie.exe"
+set CHALICE=call scala -cp bin chalice.Chalice -nologo -boogie:"C:\\Users\\t-kuayes\\Documents\\Boogie-2010-07-13\\Boogie.exe"
REM to do: AssociationList
|