diff options
Diffstat (limited to 'Chalice/src/main/scala/Chalice.scala')
| -rw-r--r-- | Chalice/src/main/scala/Chalice.scala | 500 |
1 files changed, 0 insertions, 500 deletions
diff --git a/Chalice/src/main/scala/Chalice.scala b/Chalice/src/main/scala/Chalice.scala deleted file mode 100644 index 60f5f443..00000000 --- a/Chalice/src/main/scala/Chalice.scala +++ /dev/null @@ -1,500 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-package chalice;
-import java.io.BufferedReader
-import java.io.InputStreamReader
-import java.io.File
-import java.io.FileWriter
-import scala.util.parsing.input.Position
-import scala.util.parsing.input.NoPosition
-import collection.mutable.ListBuffer
-
-object Chalice {
- /**
- * Reporting options
- */
- private[chalice] var vsMode = false;
- private[chalice] var rise4funMode = false;
- private[chalice] var InputFilename = ""; // the name of the last input file mentioned on the command line, or "" if none
-
- /**
- * 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;
- private[chalice] var percentageSupport = 0;
- 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.
- * Can only be created parseCommandLine.
- */
- sealed abstract class CommandLineParameters {
- val boogiePath: String
- val files: List[File]
- val printProgram: Boolean
- val doTypecheck: Boolean
- val doTranslate: Boolean
- val boogieArgs: String
- val gen: Boolean
- val showFullStackTrace: Boolean
- val noBplFile: Boolean
- val bplFile: String
- def getHelp(): String
- }
-
- def parseCommandLine(args: Array[String]): Option[CommandLineParameters] = {
- // help texts and closures for boolean command line options
- // closures should be idempotent
- import scala.collection.immutable.ListMap
-
- var aBoogiePath = "C:\\boogie\\Binaries\\Boogie.exe"
- val inputs = new ListBuffer[String]()
- var aPrintProgram = false
- var aDoTypecheck = true
- var aDoTranslate = true
- var aNoBplFile = true
- var aBplFile = "out.bpl"
- var aBoogieArgs = " "
- var aGen = false;
- var aShowFullStackTrace = false
-
- val options = ListMap[String,(() => Unit, String)](
- "help" -> (
- {() => },
- "print this message"),
- "print" -> ({() => aNoBplFile = false},"output the Boogie program used for verification to 'out.bpl'"),
- "printIntermediate" -> ({() => aPrintProgram = true},"print intermediate versions of the Chalice program"),
- "noTranslate" -> (
- {() => aDoTranslate = false},
- "do not translate the program to Boogie (only parse and typecheck)"),
- "noTypecheck"-> (
- {() => aDoTypecheck = false},
- "do not typecheck the program (only parse). Implies /noTranslate."),
- "vs" -> (
- {() => vsMode = true},
- "Microsoft Visual Studio mode (special error reporting for Visual Studio; requires an existing, writable directory at C:\\tmp)"),
- "rise4fun" -> (
- {() => rise4funMode = true},
- "rise4fun mode (generates error messages in a format expected by the rise4fun harness"),
- "checkLeaks" -> (
- {() => checkLeaks = true},
- "(no description available)"),
- "noDeadlockChecks" -> (
- {() => skipDeadlockChecks = true},
- "skip all lock ordering checks"),
- "noTermination" -> (
- {() => skipTermination = true},
- "skip the termination checks for functions"),
- "defaults" -> (
- {() => defaults = 3},
- null),
- "gen" -> (
- {() => aGen = true},
- "generate C# code from the Chalice program"),
- "autoFold" -> (
- {() => autoFold = true},
- "automatically fold predicates whenever necessary"),
- "autoMagic" -> (
- {() => autoMagic = true},
- "automatically try to infer accessibility predicates and non-nullness checks in specifications"),
- "noFreeAssume" -> (
- {() => noFreeAssume = true},
- "(no description available)"),
- "showFullStackTrace" -> (
- {() => aShowFullStackTrace = true},
- "show the full stack trace if an exception is encountered"),
- "smoke" -> (
- {() => smoke = true},
- "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."),
- "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"+
- "level 2: unfold predicates and functions with receiver this in pre and postconditions\n"+
- "level 3 or above: level 2 + autoMagic"),
- "percentageSupport:<n>" -> ("determin how percentage permissions are translated to Boogie\n"+
- "0: use multiplication directly (default)\n"+
- "1: use a function and provide some (redundant) axioms")+
- "boogieOpt:<arg>, /bo:<arg>" -> "specify additional Boogie options"
- )
- lazy val help = {
- val maxLength = math.min((nonBooleanOptions.keys++options.keys).map(s => s.length+1).max,14)
- val printOptionHelp = (param: String, help: String) => "\n /" + param + (" "*(maxLength-param.length-1)) +
- ": " + help.split("\n").map(h => " "*(maxLength+2+2)+wordWrap(h, 80-2-2-math.max(maxLength,param.length+1)," "*(maxLength+2+2))).mkString("\n").substring(maxLength+2+2)
-
- "Chalice concurrent program verifier.\nUsage: chalice [option] <filename>+\n"+
- " where <option> is one of"+
- options.foldLeft("")((acc, v) => acc + (if (v._2._2 == null) "" else printOptionHelp(v._1, v._2._2)))+
- nonBooleanOptions.foldLeft("")((acc, v) => acc + printOptionHelp(v._1, v._2))
- }
-
- for (a <- args) {
- if (a == "/help" || a == "-help") {Console.out.println(help); return None}
- else if ((a.startsWith("-") || a.startsWith("/")) && (options contains a.substring(1))) options(a.substring(1))._1()
- else if (a.startsWith("/print:") || a.startsWith("-print:")) {aBplFile = a.substring(7); aNoBplFile = false}
- else if (a.startsWith("/boogie:") || a.startsWith("-boogie:")) aBoogiePath = a.substring(8)
- else if (a.startsWith("/defaults:") || 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("/percentageSupport:") || a.startsWith("-percentageSupport:")) {
- try {
- val in = Integer.parseInt(a.substring(19));
- if (in < 0 || in > 1) CommandLineError("/percentageSupport takes only values 0 or 1", 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:"))
- aBoogieArgs += ("\"/" + a.substring(4) + "\"" + " ")
- /* [MHS] Quote whole argument to not confuse Boogie with arguments that
- * contain spaces, e.g. if Chalice is invoked as
- * chalice -z3exe:"C:\Program Files\z3\z3.exe" program.chalice
- */
- else if (a.startsWith("-z3opt:") || a.startsWith("/z3opt:"))
- aBoogieArgs += ("\"/z3opt:" + a.substring(7) + "\"" + " ")
- else if (a.startsWith("-") || a.startsWith("/")) {
- CommandLineError("unknown command line parameter: "+a.substring(1), help)
- return None
- }
- else inputs += a
- }
-
- // for smoke testing, we want to see all failing assertions, so we use no
- // error limit (or a very high one), and turn the subsumption option off
- if (smoke) {
- aBoogieArgs += ("\"-errorLimit:10000\" ")
- }
-
- percentageSupport match {
- case 0 => TranslatorPrelude.addComponent(PercentageStandardPL)
- case 1 => TranslatorPrelude.addComponent(PercentageFunctionPL)
- }
-
- // check that input files exist
- var aFiles = for (input <- inputs.toList) yield {
- val file = new File(input);
- if(! file.exists) {
- CommandLineError("input file " + file.getName() + " could not be found", help);
- return None;
- }
- InputFilename = input
- file;
- }
-
- Some(new CommandLineParameters{
- val boogiePath = aBoogiePath
- val files = aFiles
- val printProgram = aPrintProgram
- val doTypecheck = aDoTypecheck
- val doTranslate = aDoTranslate
- val boogieArgs = aBoogieArgs
- val gen = aGen
- val showFullStackTrace = aShowFullStackTrace
- val noBplFile = aNoBplFile
- val bplFile = aBplFile
- def getHelp(): String = help
- })
- }
-
- def parsePrograms(params: CommandLineParameters): Option[List[TopLevelDecl]] = {
- val files = params.files;
- val printProgram = params.printProgram;
-
- // parse programs
- val parser = new Parser();
- val parseResults = if (files.isEmpty) {
- if (!vsMode) println("No input file provided. Use 'chalice /help' for a list of all available command line options. Reading from stdin...")
- 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.out.println("Error: " + e);
- Nil
- case parser.Success(prog, _) =>
- val pprog = if (smoke) SmokeTest.smokeProgram(prog) else prog
- if (printProgram) PrintProgram.P(pprog)
- pprog
- }).flatten;
- if (parseErrors)
- None
- else
- Some(program)
- }
-
- def typecheckProgram(params: CommandLineParameters, program: List[TopLevelDecl]): Boolean = {
- // typecheck program
- Resolver.Resolve(program) match {
- case Resolver.Errors(msgs) =>
- 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;
-
- // checking if Boogie.exe exists (on non-Linux machine)
- val boogieFile = new File(params.boogiePath);
- if(! boogieFile.exists() || ! boogieFile.isFile()
- && (System.getProperty("os.name") != "Linux")) {
- CommandLineError("Boogie.exe not found at " + params.boogiePath, params.getHelp());
- return;
- }
-
- val boogiePath = params.boogiePath
- val boogieArgs = params.boogieArgs
-
- // translate program to Boogie
- 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 };
- val bplFilename = if (vsMode) "c:\\tmp\\out.bpl" else (if (params.noBplFile) "stdin.bpl" else params.bplFile)
- if (!params.noBplFile) writeFile(bplFilename, bplText);
- // run Boogie.exe on out.bpl
- val boogie = Runtime.getRuntime.exec(boogiePath + " /errorTrace:0 " + boogieArgs + "stdin.bpl");
- val output = boogie.getOutputStream()
- output.write(bplText.getBytes)
- output.close
- // terminate boogie if interrupted
- Runtime.getRuntime.addShutdownHook(new Thread(new Runnable() {
- def run {
- 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;
- val boogieOutput: ListBuffer[String] = new ListBuffer()
- while (line!=null){
- if (!smoke) {
- if (previous_line != null) Console.out.println
- Console.out.print(line);
- Console.out.flush;
- }
- boogieOutput += line
- previous_line = line;
- line = input.readLine();
- }
- 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.print(output);
- Console.out.flush;
- }
-
- // generate code
- 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) {
- e.printStackTrace()
- Console.err.println()
- Console.err.println()
- }
- CommandLineError("Internal error: " + e.msg, params.getHelp())
- return
- }
- case e:NotSupportedException => {
- if (params.showFullStackTrace) {
- e.printStackTrace()
- Console.err.println()
- Console.err.println()
- }
- CommandLineError("Not supported: " + e.msg, params.getHelp())
- 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 = {
- val converter = new ChaliceToCSharp();
- println("Code generated in out.cs.");
- writeFile("out.cs", converter.convertProgram(program));
- }
-
- 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) = {
- Console.out.println("Error: " + msg)
- }
-
- def ReportError(pos: Position, msg: String) = {
- if (vsMode) {
- val (r,c) = (pos.line, pos.column)
- Console.out.println(r + "," + c + "," + r + "," + (c+5) + ":" + msg);
- } else {
- Console.out.println(pos + ": " + msg)
- }
- }
-
- def wordWrap(s: String, l: Int, indent: String): String = {
- var prefix = s.takeWhile(c => c == ' ').length
- if (prefix == 0) prefix = if (s.indexOf(": ") > 0) s.indexOf(": ")+2 else 0;
- val words = s.split(" ")
- var c = 0
- var result = ""
- var first = 0
- for (word <- words) {
- c += word.length + 1
- if (c-1 > l-first*prefix) { result += "\n"; c = word.length + 1; first = 1}
- result += word + " "
- }
- result.substring(0, result.length-1).replace("\n", "\n" + (" "*prefix) + indent).replace(" \n","\n")
- }
-}
-
-class InternalErrorException(val msg: String) extends Throwable
-class NotSupportedException(val msg: String) extends Throwable
-
|