1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
|
//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
import java.io.BufferedReader
import java.io.InputStreamReader
import java.io.File
import java.io.FileWriter
import scala.util.parsing.input.Position
object Chalice {
def main(args: Array[String]): Unit = {
var boogiePath = "C:\\boogie\\Binaries\\Boogie.exe"
// parse command-line arguments
var inputName: String = null
var printProgram = false
var vsMode = false;
def ReportError(pos: Position, msg: String) = {
if (vsMode) {
val r = pos.line - 1;
val c = pos.column - 1;
Console.out.println(r + "," + c + "," + r + "," + (c+5) + ":" + msg);
} 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;
// 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 (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("-") || 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", help); return } else {
val file = new File(inputName);
if(! file.exists()){
CommandLineError("input file " + file.getName() + " could not be found", help); return
}
}
// parse program
val parser = new Parser();
parser.parseFile(inputName) match {
case e: parser.NoSuccess =>
if (vsMode)
ReportError(e.next.pos, e.msg);
else
Console.err.println("Error: " + e)
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);
val input = new BufferedReader(new InputStreamReader(boogie.getInputStream()));
var line = input.readLine();
var previous_line = null: String;
while(line!=null){
println(line);
previous_line = line;
line = input.readLine();
}
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));
}
}
}
}
}
}
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.err.println("Error: " + msg)
Console.err.println(help);
}
}
|
