diff options
| author |  Unknown <afd@afd-THINK.home> | 2012-10-01 22:03:47 +0100 |
|---|---|---|
| committer | Unknown <afd@afd-THINK.home> | 2012-10-01 22:03:47 +0100 |
| commit | 2232875cd561e0ffe412cdb5cb5acd05b1ef2a3a (patch) | |
| tree | 3fcfb062d4aa1598ca63851f9cde5116f6652549 | |
| parent | b31d36beb388e5ae402a8e24e21357a56eafe685 (diff) | |
Fixed GPUVerify solution.
Merged recent changes to BoogieDriver into GPUVerifyBoogieDriver.
| -rw-r--r-- | Source/GPUVerify.sln | 22 | ||||
| -rw-r--r-- | Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs | 1160 |
2 files changed, 520 insertions, 662 deletions
diff --git a/Source/GPUVerify.sln b/Source/GPUVerify.sln index 7853459f..75354021 100644 --- a/Source/GPUVerify.sln +++ b/Source/GPUVerify.sln @@ -27,8 +27,6 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Model", "Model\Model.csproj EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCExpr", "VCExpr\VCExpr.csproj", "{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}"
EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Isabelle", "Provers\Isabelle\Isabelle.csproj", "{435D5BD0-6F62-49F8-BB24-33E2257519AD}"
-EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "GPUVerifyBoogieDriver", "GPUVerifyBoogieDriver\GPUVerifyBoogieDriver.csproj", "{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}"
EndProject
Global
@@ -309,26 +307,6 @@ Global {56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.z3apidebug|Mixed Platforms.ActiveCfg = z3apidebug|Any CPU
{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.z3apidebug|Mixed Platforms.Build.0 = z3apidebug|Any CPU
{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
- {435D5BD0-6F62-49F8-BB24-33E2257519AD}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
- {435D5BD0-6F62-49F8-BB24-33E2257519AD}.Checked|Any CPU.Build.0 = Checked|Any CPU
- {435D5BD0-6F62-49F8-BB24-33E2257519AD}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
- {435D5BD0-6F62-49F8-BB24-33E2257519AD}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
- {435D5BD0-6F62-49F8-BB24-33E2257519AD}.Checked|x86.ActiveCfg = Checked|Any CPU
- {435D5BD0-6F62-49F8-BB24-33E2257519AD}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {435D5BD0-6F62-49F8-BB24-33E2257519AD}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {435D5BD0-6F62-49F8-BB24-33E2257519AD}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {435D5BD0-6F62-49F8-BB24-33E2257519AD}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
- {435D5BD0-6F62-49F8-BB24-33E2257519AD}.Debug|x86.ActiveCfg = Debug|Any CPU
- {435D5BD0-6F62-49F8-BB24-33E2257519AD}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {435D5BD0-6F62-49F8-BB24-33E2257519AD}.Release|Any CPU.Build.0 = Release|Any CPU
- {435D5BD0-6F62-49F8-BB24-33E2257519AD}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
- {435D5BD0-6F62-49F8-BB24-33E2257519AD}.Release|Mixed Platforms.Build.0 = Release|Any CPU
- {435D5BD0-6F62-49F8-BB24-33E2257519AD}.Release|x86.ActiveCfg = Release|Any CPU
- {435D5BD0-6F62-49F8-BB24-33E2257519AD}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
- {435D5BD0-6F62-49F8-BB24-33E2257519AD}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
- {435D5BD0-6F62-49F8-BB24-33E2257519AD}.z3apidebug|Mixed Platforms.ActiveCfg = z3apidebug|Any CPU
- {435D5BD0-6F62-49F8-BB24-33E2257519AD}.z3apidebug|Mixed Platforms.Build.0 = z3apidebug|Any CPU
- {435D5BD0-6F62-49F8-BB24-33E2257519AD}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.Checked|Any CPU.ActiveCfg = Release|x86
{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.Checked|Mixed Platforms.ActiveCfg = Release|x86
{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.Checked|Mixed Platforms.Build.0 = Release|x86
diff --git a/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs b/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs index 2e8adf6d..906e0202 100644 --- a/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs +++ b/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs @@ -38,39 +38,31 @@ namespace Microsoft.Boogie // ------------------------------------------------------------------------
// Main
- public static void Main(string[] args)
- {
+ public static void Main(string[] args) {
Contract.Requires(cce.NonNullElements(args));
CommandLineOptions.Install(new CommandLineOptions());
CommandLineOptions.Clo.RunningBoogieFromCommandLine = true;
- if (!CommandLineOptions.Clo.Parse(args))
- {
+ if (!CommandLineOptions.Clo.Parse(args)) {
goto END;
}
- if (CommandLineOptions.Clo.Files.Count == 0)
- {
+ if (CommandLineOptions.Clo.Files.Count == 0) {
ErrorWriteLine("*** Error: No input files were specified.");
goto END;
}
- if (CommandLineOptions.Clo.XmlSink != null)
- {
+ if (CommandLineOptions.Clo.XmlSink != null) {
string errMsg = CommandLineOptions.Clo.XmlSink.Open();
- if (errMsg != null)
- {
+ if (errMsg != null) {
ErrorWriteLine("*** Error: " + errMsg);
goto END;
}
}
- if (!CommandLineOptions.Clo.DontShowLogo)
- {
+ if (!CommandLineOptions.Clo.DontShowLogo) {
Console.WriteLine(CommandLineOptions.Clo.Version);
}
- if (CommandLineOptions.Clo.ShowEnv == CommandLineOptions.ShowEnvironment.Always)
- {
+ if (CommandLineOptions.Clo.ShowEnv == CommandLineOptions.ShowEnvironment.Always) {
Console.WriteLine("---Command arguments");
- foreach (string arg in args)
- {
+ foreach (string arg in args) {
Contract.Assert(arg != null);
Console.WriteLine(arg);
}
@@ -81,34 +73,27 @@ namespace Microsoft.Boogie Helpers.ExtraTraceInformation("Becoming sentient");
List<string> fileList = new List<string>();
- foreach (string file in CommandLineOptions.Clo.Files)
- {
+ foreach (string file in CommandLineOptions.Clo.Files) {
string extension = Path.GetExtension(file);
- if (extension != null)
- {
+ if (extension != null) {
extension = extension.ToLower();
}
- if (extension == ".txt")
- {
+ if (extension == ".txt") {
StreamReader stream = new StreamReader(file);
string s = stream.ReadToEnd();
fileList.AddRange(s.Split(new char[3] { ' ', '\n', '\r' }, StringSplitOptions.RemoveEmptyEntries));
}
- else
- {
+ else {
fileList.Add(file);
}
}
- foreach (string file in fileList)
- {
+ foreach (string file in fileList) {
Contract.Assert(file != null);
string extension = Path.GetExtension(file);
- if (extension != null)
- {
+ if (extension != null) {
extension = extension.ToLower();
}
- if (extension != ".bpl")
- {
+ if (extension != ".bpl") {
ErrorWriteLine("*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be BoogiePL programs (.bpl).", file,
extension == null ? "" : extension);
goto END;
@@ -117,19 +102,16 @@ namespace Microsoft.Boogie ProcessFiles(fileList);
END:
- if (CommandLineOptions.Clo.XmlSink != null)
- {
+ if (CommandLineOptions.Clo.XmlSink != null) {
CommandLineOptions.Clo.XmlSink.Close();
}
- if (CommandLineOptions.Clo.Wait)
- {
+ if (CommandLineOptions.Clo.Wait) {
Console.WriteLine("Press Enter to exit.");
Console.ReadLine();
}
}
- public static void ErrorWriteLine(string s)
- {
+ public static void ErrorWriteLine(string s) {
Contract.Requires(s != null);
ConsoleColor col = Console.ForegroundColor;
Console.ForegroundColor = ConsoleColor.DarkGray;
@@ -166,15 +148,13 @@ namespace Microsoft.Boogie Console.WriteLine(message);
}
- public static void ErrorWriteLine(string format, params object[] args)
- {
+ public static void ErrorWriteLine(string format, params object[] args) {
Contract.Requires(format != null);
string s = string.Format(format, args);
ErrorWriteLine(s);
}
- public static void AdvisoryWriteLine(string format, params object[] args)
- {
+ public static void AdvisoryWriteLine(string format, params object[] args) {
Contract.Requires(format != null);
ConsoleColor col = Console.ForegroundColor;
Console.ForegroundColor = ConsoleColor.Yellow;
@@ -182,8 +162,7 @@ namespace Microsoft.Boogie Console.ForegroundColor = col;
}
- enum FileType
- {
+ enum FileType {
Unknown,
Cil,
Bpl,
@@ -207,14 +186,12 @@ namespace Microsoft.Boogie static void ProcessFiles(List<string> fileNames)
{
Contract.Requires(cce.NonNullElements(fileNames));
- using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count - 1]))
- {
+ using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count - 1])) {
//BoogiePL.Errors.count = 0;
Program program = ParseBoogieProgram(fileNames, false);
if (program == null)
return;
- if (CommandLineOptions.Clo.PrintFile != null)
- {
+ if (CommandLineOptions.Clo.PrintFile != null) {
PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false);
}
@@ -224,19 +201,15 @@ namespace Microsoft.Boogie //BoogiePL.Errors.count = 0;
// Do bitvector analysis
- if (CommandLineOptions.Clo.DoBitVectorAnalysis)
- {
+ if (CommandLineOptions.Clo.DoBitVectorAnalysis) {
Microsoft.Boogie.BitVectorAnalysis.DoBitVectorAnalysis(program);
PrintBplFile(CommandLineOptions.Clo.BitVectorAnalysisOutputBplFile, program, false);
return;
}
- if (CommandLineOptions.Clo.PrintCFGPrefix != null)
- {
- foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())
- {
- using (StreamWriter sw = new StreamWriter(CommandLineOptions.Clo.PrintCFGPrefix + "." + impl.Name + ".dot"))
- {
+ if (CommandLineOptions.Clo.PrintCFGPrefix != null) {
+ foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>()) {
+ using (StreamWriter sw = new StreamWriter(CommandLineOptions.Clo.PrintCFGPrefix + "." + impl.Name + ".dot")) {
sw.Write(program.ProcessLoops(impl).ToDot());
}
}
@@ -246,8 +219,7 @@ namespace Microsoft.Boogie int errorCount, verified, inconclusives, timeOuts, outOfMemories;
oc = InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);
- switch (oc)
- {
+ switch (oc) {
case PipelineOutcome.Done:
case PipelineOutcome.VerificationCompleted:
WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
@@ -259,21 +231,17 @@ namespace Microsoft.Boogie }
- static void PrintBplFile(string filename, Program program, bool allowPrintDesugaring)
- {
+ static void PrintBplFile(string filename, Program program, bool allowPrintDesugaring) {
Contract.Requires(program != null);
Contract.Requires(filename != null);
bool oldPrintDesugaring = CommandLineOptions.Clo.PrintDesugarings;
- if (!allowPrintDesugaring)
- {
+ if (!allowPrintDesugaring) {
CommandLineOptions.Clo.PrintDesugarings = false;
}
using (TokenTextWriter writer = filename == "-" ?
new TokenTextWriter("<console>", Console.Out) :
- new TokenTextWriter(filename))
- {
- if (CommandLineOptions.Clo.ShowEnv != CommandLineOptions.ShowEnvironment.Never)
- {
+ new TokenTextWriter(filename)) {
+ if (CommandLineOptions.Clo.ShowEnv != CommandLineOptions.ShowEnvironment.Never) {
writer.WriteLine("// " + CommandLineOptions.Clo.Version);
writer.WriteLine("// " + CommandLineOptions.Clo.Environment);
}
@@ -284,106 +252,39 @@ namespace Microsoft.Boogie }
- static bool ProgramHasDebugInfo(Program program)
- {
+ static bool ProgramHasDebugInfo(Program program) {
Contract.Requires(program != null);
// We inspect the last declaration because the first comes from the prelude and therefore always has source context.
return program.TopLevelDeclarations.Count > 0 &&
((cce.NonNull(program.TopLevelDeclarations)[program.TopLevelDeclarations.Count - 1]).tok.IsValid);
}
- static QKeyValue GetAttributes(Absy a)
- {
- if (a is PredicateCmd)
- {
- return (a as PredicateCmd).Attributes;
- }
- else if (a is Requires)
- {
- return (a as Requires).Attributes;
- }
- else if (a is Ensures)
- {
- return (a as Ensures).Attributes;
- }
- else if (a is CallCmd)
- {
- return (a as CallCmd).Attributes;
- }
- //Debug.Assert(false);
- return null;
- }
/// <summary>
/// Inform the user about something and proceed with translation normally.
/// Print newline after the message.
/// </summary>
- public static void Inform(string s)
- {
- if (!CommandLineOptions.Clo.Trace)
- {
- return;
- }
- Console.WriteLine(s);
- }
-
- private static void AddPadding(ref string string1, ref string string2)
- {
- if (string1.Length < string2.Length)
- {
- for (int i = (string2.Length - string1.Length); i > 0; --i)
- {
- string1 += " ";
- }
- }
- else
- {
- for (int i = (string1.Length - string2.Length); i > 0; --i)
- {
- string2 += " ";
- }
- }
- }
-
- private static string TrimLeadingSpaces(string s1, int noOfSpaces)
- {
- if (String.IsNullOrWhiteSpace(s1))
- {
- return s1;
- }
-
- int index;
- for (index = 0; (index + 1) < s1.Length && Char.IsWhiteSpace(s1[index]); ++index);
- string returnString = s1.Substring(index);
- for (int i = noOfSpaces; i > 0; --i)
- {
- returnString = " " + returnString;
+ public static void Inform(string s) {
+ if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations) {
+ Console.WriteLine(s);
}
- return returnString;
}
- static void WriteTrailer(int verified, int errors, int inconclusives, int timeOuts, int outOfMemories)
- {
+ static void WriteTrailer(int verified, int errors, int inconclusives, int timeOuts, int outOfMemories) {
Contract.Requires(0 <= errors && 0 <= inconclusives && 0 <= timeOuts && 0 <= outOfMemories);
Console.WriteLine();
- if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
- {
- Console.Write("{0} finished with {1} credible, {2} doomed{3}", "GPUVerify", verified, errors, errors == 1 ? "" : "s");
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
+ Console.Write("{0} finished with {1} credible, {2} doomed{3}", CommandLineOptions.Clo.DescriptiveToolName, verified, errors, errors == 1 ? "" : "s");
+ } else {
+ Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.DescriptiveToolName, verified, errors, errors == 1 ? "" : "s");
}
- else
- {
- Console.Write("{0} finished with {1} verified, {2} error{3}", "GPUVerify", verified, errors, errors == 1 ? "" : "s");
- }
- if (inconclusives != 0)
- {
+ if (inconclusives != 0) {
Console.Write(", {0} inconclusive{1}", inconclusives, inconclusives == 1 ? "" : "s");
}
- if (timeOuts != 0)
- {
+ if (timeOuts != 0) {
Console.Write(", {0} time out{1}", timeOuts, timeOuts == 1 ? "" : "s");
}
- if (outOfMemories != 0)
- {
+ if (outOfMemories != 0) {
Console.Write(", {0} out of memory", outOfMemories);
}
Console.WriteLine();
@@ -434,72 +335,54 @@ namespace Microsoft.Boogie /// Parse the given files into one Boogie program. If an I/O or parse error occurs, an error will be printed
/// and null will be returned. On success, a non-null program is returned.
/// </summary>
- static Program ParseBoogieProgram(List<string> fileNames, bool suppressTraceOutput)
- {
+ static Program ParseBoogieProgram(List<string> fileNames, bool suppressTraceOutput) {
Contract.Requires(cce.NonNullElements(fileNames));
//BoogiePL.Errors.count = 0;
Program program = null;
bool okay = true;
- for (int fileId = 0; fileId < fileNames.Count; fileId++)
- {
+ for (int fileId = 0; fileId < fileNames.Count; fileId++) {
string bplFileName = fileNames[fileId];
- if (!suppressTraceOutput)
- {
- if (CommandLineOptions.Clo.XmlSink != null)
- {
+ if (!suppressTraceOutput) {
+ if (CommandLineOptions.Clo.XmlSink != null) {
CommandLineOptions.Clo.XmlSink.WriteFileFragment(bplFileName);
}
- if (CommandLineOptions.Clo.Trace)
- {
+ if (CommandLineOptions.Clo.Trace) {
Console.WriteLine("Parsing " + bplFileName);
}
}
Program programSnippet;
int errorCount;
- try
- {
+ try {
var defines = new List<string>() { "FILE_" + fileId };
errorCount = BoogiePL.Parser.Parse(bplFileName, defines, out programSnippet);
- if (programSnippet == null || errorCount != 0)
- {
+ if (programSnippet == null || errorCount != 0) {
Console.WriteLine("{0} parse errors detected in {1}", errorCount, bplFileName);
okay = false;
continue;
}
- }
- catch (IOException e)
- {
+ } catch (IOException e) {
ErrorWriteLine("Error opening file \"{0}\": {1}", bplFileName, e.Message);
okay = false;
continue;
}
- if (program == null)
- {
+ if (program == null) {
program = programSnippet;
- }
- else if (programSnippet != null)
- {
+ } else if (programSnippet != null) {
program.TopLevelDeclarations.AddRange(programSnippet.TopLevelDeclarations);
}
}
- if (!okay)
- {
+ if (!okay) {
return null;
- }
- else if (program == null)
- {
+ } else if (program == null) {
return new Program();
- }
- else
- {
+ } else {
return program;
}
}
- enum PipelineOutcome
- {
+ enum PipelineOutcome {
Done,
ResolutionError,
TypeCheckingError,
@@ -516,40 +399,34 @@ namespace Microsoft.Boogie /// - TypeCheckingError if a type checking error occurred
/// - ResolvedAndTypeChecked if both resolution and type checking succeeded
/// </summary>
- static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName)
- {
+ static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName) {
Contract.Requires(program != null);
Contract.Requires(bplFileName != null);
// ---------- Resolve ------------------------------------------------------------
- if (CommandLineOptions.Clo.NoResolve)
- {
+ if (CommandLineOptions.Clo.NoResolve) {
return PipelineOutcome.Done;
}
int errorCount = program.Resolve();
- if (errorCount != 0)
- {
+ if (errorCount != 0) {
Console.WriteLine("{0} name resolution errors detected in {1}", errorCount, bplFileName);
return PipelineOutcome.ResolutionError;
}
// ---------- Type check ------------------------------------------------------------
- if (CommandLineOptions.Clo.NoTypecheck)
- {
+ if (CommandLineOptions.Clo.NoTypecheck) {
return PipelineOutcome.Done;
}
errorCount = program.Typecheck();
- if (errorCount != 0)
- {
+ if (errorCount != 0) {
Console.WriteLine("{0} type checking errors detected in {1}", errorCount, bplFileName);
return PipelineOutcome.TypeCheckingError;
}
- if (CommandLineOptions.Clo.PrintFile != null && CommandLineOptions.Clo.PrintDesugarings)
- {
+ if (CommandLineOptions.Clo.PrintFile != null && CommandLineOptions.Clo.PrintDesugarings) {
// if PrintDesugaring option is engaged, print the file here, after resolution and type checking
PrintBplFile(CommandLineOptions.Clo.PrintFile, program, true);
}
@@ -557,21 +434,18 @@ namespace Microsoft.Boogie return PipelineOutcome.ResolvedAndTypeChecked;
}
- static void EliminateDeadVariablesAndInline(Program program)
- {
+ static void EliminateDeadVariablesAndInline(Program program) {
Contract.Requires(program != null);
// Eliminate dead variables
Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);
// Collect mod sets
- if (CommandLineOptions.Clo.DoModSetAnalysis)
- {
+ if (CommandLineOptions.Clo.DoModSetAnalysis) {
Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);
}
// Coalesce blocks
- if (CommandLineOptions.Clo.CoalesceBlocks)
- {
+ if (CommandLineOptions.Clo.CoalesceBlocks) {
if (CommandLineOptions.Clo.Trace)
Console.WriteLine("Coalescing blocks...");
Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
@@ -580,40 +454,30 @@ namespace Microsoft.Boogie // Inline
var TopLevelDeclarations = cce.NonNull(program.TopLevelDeclarations);
- if (CommandLineOptions.Clo.ProcedureInlining != CommandLineOptions.Inlining.None)
- {
+ if (CommandLineOptions.Clo.ProcedureInlining != CommandLineOptions.Inlining.None) {
bool inline = false;
- foreach (var d in TopLevelDeclarations)
- {
- if (d.FindExprAttribute("inline") != null)
- {
+ foreach (var d in TopLevelDeclarations) {
+ if (d.FindExprAttribute("inline") != null) {
inline = true;
}
}
- if (inline)
- {
- foreach (var d in TopLevelDeclarations)
- {
+ if (inline) {
+ foreach (var d in TopLevelDeclarations) {
var impl = d as Implementation;
- if (impl != null)
- {
+ if (impl != null) {
impl.OriginalBlocks = impl.Blocks;
impl.OriginalLocVars = impl.LocVars;
}
}
- foreach (var d in TopLevelDeclarations)
- {
+ foreach (var d in TopLevelDeclarations) {
var impl = d as Implementation;
- if (impl != null && !impl.SkipVerification)
- {
+ if (impl != null && !impl.SkipVerification) {
Inliner.ProcessImplementation(program, impl);
}
}
- foreach (var d in TopLevelDeclarations)
- {
+ foreach (var d in TopLevelDeclarations) {
var impl = d as Implementation;
- if (impl != null)
- {
+ if (impl != null) {
impl.OriginalBlocks = null;
impl.OriginalLocVars = null;
}
@@ -622,6 +486,449 @@ namespace Microsoft.Boogie }
}
+ static void ProcessOutcome(VC.VCGen.Outcome outcome, List<Counterexample> errors, string timeIndication,
+ ref int errorCount, ref int verified, ref int inconclusives, ref int timeOuts, ref int outOfMemories) {
+ switch (outcome) {
+ default:
+ Contract.Assert(false); // unexpected outcome
+ throw new cce.UnreachableException();
+ case VCGen.Outcome.ReachedBound:
+ Inform(String.Format("{0}verified", timeIndication));
+ Console.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound));
+ verified++;
+ break;
+ case VCGen.Outcome.Correct:
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
+ Inform(String.Format("{0}credible", timeIndication));
+ verified++;
+ }
+ else {
+ Inform(String.Format("{0}verified", timeIndication));
+ verified++;
+ }
+ break;
+ case VCGen.Outcome.TimedOut:
+ timeOuts++;
+ Inform(String.Format("{0}timed out", timeIndication));
+ break;
+ case VCGen.Outcome.OutOfMemory:
+ outOfMemories++;
+ Inform(String.Format("{0}out of memory", timeIndication));
+ break;
+ case VCGen.Outcome.Inconclusive:
+ inconclusives++;
+ Inform(String.Format("{0}inconclusive", timeIndication));
+ break;
+ case VCGen.Outcome.Errors:
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
+ Inform(String.Format("{0}doomed", timeIndication));
+ errorCount++;
+ } //else {
+ Contract.Assert(errors != null); // guaranteed by postcondition of VerifyImplementation
+ {
+ // BP1xxx: Parsing errors
+ // BP2xxx: Name resolution errors
+ // BP3xxx: Typechecking errors
+ // BP4xxx: Abstract interpretation errors (Is there such a thing?)
+ // BP5xxx: Verification errors
+
+ errors.Sort(new CounterexampleComparer());
+ foreach (Counterexample error in errors)
+ {
+ if (error is CallCounterexample)
+ {
+ CallCounterexample err = (CallCounterexample)error;
+ if (QKeyValue.FindBoolAttribute(err.FailingRequires.Attributes, "barrier_divergence"))
+ {
+ ReportBarrierDivergence(err.FailingCall);
+ }
+ else if (QKeyValue.FindBoolAttribute(err.FailingRequires.Attributes, "race"))
+ {
+ int byteOffset = -1, elemOffset = -1, elemWidth = -1;
+ string thread1 = null, thread2 = null, group1 = null, group2 = null, arrName = null;
+ //TODO: make this a command line argument.
+ bool detailedTrace = false;
+ string threadOneFailAccess = null, threadTwoFailAccess = null;
+
+ Variable offsetVar = ExtractOffsetVar(err.FailingRequires.Condition as NAryExpr);
+ /* Right now the offset incarnation that is extracted is the penultimate one if
+ * there is more than one incarnation, or the last one if there is only one incarnation.
+ * TODO: In future, we should know the exact incarnation to extract. This information is
+ * available when the CallCounterexample is created in VC.cs AssertCmdToCounterexample() (line 2405)
+ * The condition of the AssertRequiresCmd contains the incarnation information, so this should be passed
+ * on to the Requires of the created CallCounterexample. This can either be done by replacing the condition
+ * of the Requires with the condition from AssertRequiresCmd (containing incarnation information) or creating
+ * a separate field in the Requires to store this original condition.
+ */
+ Model.Func offsetFunc = ExtractIncarnationFromModel(error.Model, offsetVar.Name);
+ Debug.Assert(offsetFunc != null, "ProcessOutcome(): Could not extract incarnation.");
+ GetInfoFromVarAndFunc(offsetVar.Attributes, offsetFunc, out byteOffset, out elemOffset, out elemWidth, out arrName);
+
+ Debug.Assert(error.Model != null, "ProcessOutcome(): null model");
+ GetThreadsAndGroupsFromModel(err.Model, out thread1, out thread2, out group1, out group2, true);
+
+ if (QKeyValue.FindBoolAttribute(err.FailingRequires.Attributes, "write_read"))
+ {
+ err.FailingRequires.Attributes = GetSourceLocInfo(error, "WRITE");
+ threadOneFailAccess = "WRITE";
+ threadTwoFailAccess = "READ";
+ ReportRace(err.FailingCall, err.FailingRequires, thread1, thread2, group1, group2, arrName, byteOffset, RaceType.WR);
+ }
+ else if (QKeyValue.FindBoolAttribute(err.FailingRequires.Attributes, "read_write"))
+ {
+ err.FailingRequires.Attributes = GetSourceLocInfo(error, "READ");
+ threadOneFailAccess = "READ";
+ threadTwoFailAccess = "WRITE";
+ ReportRace(err.FailingCall, err.FailingRequires, thread1, thread2, group1, group2, arrName, byteOffset, RaceType.RW);
+
+ }
+ else if (QKeyValue.FindBoolAttribute(err.FailingRequires.Attributes, "write_write"))
+ {
+ err.FailingRequires.Attributes = GetSourceLocInfo(error, "WRITE");
+ threadOneFailAccess = "WRITE";
+ threadTwoFailAccess = "WRITE";
+ ReportRace(err.FailingCall, err.FailingRequires, thread1, thread2, group1, group2, arrName, byteOffset, RaceType.WW);
+ }
+
+ if (detailedTrace)
+ {
+ string fname = QKeyValue.FindStringAttribute(err.FailingCall.Attributes, "fname");
+ Debug.Assert(!String.IsNullOrEmpty(fname));
+ int colOneSize = fname.Length + 11;
+ string colTwoHeader = " T " + GetThreadOne(error.Model, false) + " G " + GetGroupOne(error.Model, false) + " ";
+ string colThreeHeader = " T " + GetThreadTwo(error.Model, false) + " G " + GetGroupTwo(error.Model, false) + " ";
+
+ int colTwoSize = colTwoHeader.Length + 2;
+ int colThreeSize = colTwoHeader.Length + 2;
+
+ PrintDetailedTraceHeader(colTwoHeader, colThreeHeader, colOneSize, colTwoSize, colThreeSize);
+ PrintDetailedTrace(err, colOneSize, colTwoSize, colThreeSize, elemOffset, elemWidth, threadOneFailAccess, threadTwoFailAccess);
+ }
+ }
+ else
+ {
+ ReportRequiresFailure(err.FailingCall, err.FailingRequires);
+ }
+ }
+ else if (error is ReturnCounterexample)
+ {
+ ReturnCounterexample err = (ReturnCounterexample)error;
+ ReportEnsuresFailure(err.FailingEnsures);
+ }
+ else
+ {
+ AssertCounterexample err = (AssertCounterexample)error;
+ if (err.FailingAssert is LoopInitAssertCmd)
+ {
+ ReportInvariantEntryFailure(err.FailingAssert);
+ }
+ else if (err.FailingAssert is LoopInvMaintainedAssertCmd)
+ {
+ ReportInvariantMaintedFailure(err.FailingAssert);
+ }
+ else
+ {
+ ReportFailingAssert(err.FailingAssert);
+ }
+ }
+ errorCount++;
+ }
+ //}
+ Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));
+ }
+ break;
+ }
+ }
+
+ private static void PrintDetailedTraceHeader(string colTwoHeader, string colThreeHeader, int locationColSize, int colTwoSize, int colThreeSize)
+ {
+ Console.Write("\nLocation");
+ PrintNChars(locationColSize - "Location".Length, ' ');
+ Console.WriteLine("|{0}|{1}", colTwoHeader + Chars(colTwoSize - colTwoHeader.Length, ' '), colThreeHeader + Chars(colThreeSize - colThreeHeader.Length, ' '));
+ PrintNChars(locationColSize, '-');
+ Console.Write("|");
+ PrintNChars(colTwoSize, '-');
+ Console.Write("|");
+ PrintNChars(colThreeSize, '-');
+ Console.WriteLine("");
+ }
+
+ private static void PrintNChars(int n, char c)
+ {
+ for (int i = 0; i < n; ++i)
+ {
+ Console.Write(c);
+ }
+ }
+
+ private static string Chars(int n, char c)
+ {
+ return new String(c, n);
+ }
+
+
+ /// <summary>
+ /// Given a resolved and type checked Boogie program, infers invariants for the program
+ /// and then attempts to verify it. Returns:
+ /// - Done if command line specified no verification
+ /// - FatalError if a fatal error occurred, in which case an error has been printed to console
+ /// - VerificationCompleted if inference and verification completed, in which the out
+ /// parameters contain meaningful values
+ /// </summary>
+ static PipelineOutcome InferAndVerify(Program program,
+ out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories) {
+ Contract.Requires(program != null);
+ Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));
+
+ errorCount = verified = inconclusives = timeOuts = outOfMemories = 0;
+
+ // ---------- Infer invariants --------------------------------------------------------
+
+ // Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)
+ if (CommandLineOptions.Clo.UseAbstractInterpretation) {
+ if (!CommandLineOptions.Clo.Ai.J_Intervals && !CommandLineOptions.Clo.Ai.J_Trivial) {
+ // use /infer:j as the default
+ CommandLineOptions.Clo.Ai.J_Intervals = true;
+ }
+ }
+ Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);
+
+ if (CommandLineOptions.Clo.LoopUnrollCount != -1) {
+ program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);
+ }
+
+ if (CommandLineOptions.Clo.DoPredication && CommandLineOptions.Clo.StratifiedInlining > 0) {
+ BlockPredicator.Predicate(program, false, false);
+ if (CommandLineOptions.Clo.PrintInstrumented) {
+ using (TokenTextWriter writer = new TokenTextWriter(Console.Out)) {
+ program.Emit(writer);
+ }
+ }
+ }
+
+ Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo = null;
+ if (CommandLineOptions.Clo.ExtractLoops)
+ {
+ extractLoopMappingInfo = program.ExtractLoops();
+ }
+
+ if (CommandLineOptions.Clo.PrintInstrumented) {
+ program.Emit(new TokenTextWriter(Console.Out));
+ }
+
+ if (CommandLineOptions.Clo.ExpandLambdas) {
+ LambdaHelper.ExpandLambdas(program);
+ //PrintBplFile ("-", program, true);
+ }
+
+ // ---------- Verify ------------------------------------------------------------
+
+ if (!CommandLineOptions.Clo.Verify) {
+ return PipelineOutcome.Done;
+ }
+
+ #region Run Houdini and verify
+ if (CommandLineOptions.Clo.ContractInfer) {
+ Houdini.Houdini houdini = new Houdini.Houdini(program);
+ Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();
+ if (CommandLineOptions.Clo.PrintAssignment) {
+ Console.WriteLine("Assignment computed by Houdini:");
+ foreach (var x in outcome.assignment) {
+ Console.WriteLine(x.Key + " = " + x.Value);
+ }
+ }
+ if (CommandLineOptions.Clo.Trace)
+ {
+ int numTrueAssigns = 0;
+ foreach (var x in outcome.assignment) {
+ if (x.Value)
+ numTrueAssigns++;
+ }
+ Console.WriteLine("Number of true assignments = " + numTrueAssigns);
+ Console.WriteLine("Number of false assignments = " + (outcome.assignment.Count - numTrueAssigns));
+ Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime);
+ Console.WriteLine("Unsat core prover time = " + Houdini.HoudiniSession.unsatCoreProverTime);
+ Console.WriteLine("Number of prover queries = " + Houdini.HoudiniSession.numProverQueries);
+ Console.WriteLine("Number of unsat core prover queries = " + Houdini.HoudiniSession.numUnsatCoreProverQueries);
+ Console.WriteLine("Number of unsat core prunings = " + Houdini.HoudiniSession.numUnsatCorePrunings);
+ }
+
+ foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values) {
+ ProcessOutcome(x.outcome, x.errors, "", ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories);
+ }
+ //errorCount = outcome.ErrorCount;
+ //verified = outcome.Verified;
+ //inconclusives = outcome.Inconclusives;
+ //timeOuts = outcome.TimeOuts;
+ //outOfMemories = 0;
+ return PipelineOutcome.Done;
+ }
+ #endregion
+
+ #region Verify each implementation
+
+ ConditionGeneration vcgen = null;
+ try {
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
+ vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ } else if(CommandLineOptions.Clo.StratifiedInlining > 0) {
+ vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ } else {
+ vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ }
+ } catch (ProverException e) {
+ ErrorWriteLine("Fatal Error: ProverException: {0}", e);
+ return PipelineOutcome.FatalError;
+ }
+
+ // operate on a stable copy, in case it gets updated while we're running
+ var decls = program.TopLevelDeclarations.ToArray();
+ foreach (Declaration decl in decls) {
+ Contract.Assert(decl != null);
+ int prevAssertionCount = vcgen.CumulativeAssertionCount;
+ Implementation impl = decl as Implementation;
+ if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification) {
+ List<Counterexample/*!*/>/*?*/ errors;
+
+ DateTime start = new DateTime(); // to please compiler's definite assignment rules
+ if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations || CommandLineOptions.Clo.XmlSink != null) {
+ start = DateTime.UtcNow;
+ if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations) {
+ Console.WriteLine();
+ Console.WriteLine("Verifying {0} ...", impl.Name);
+ }
+ if (CommandLineOptions.Clo.XmlSink != null) {
+ CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, start);
+ }
+ }
+
+ VCGen.Outcome outcome;
+ try {
+ if (CommandLineOptions.Clo.inferLeastForUnsat != null) {
+ var svcgen = vcgen as VC.StratifiedVCGen;
+ Contract.Assert(svcgen != null);
+ var ss = new HashSet<string>();
+ foreach (var tdecl in program.TopLevelDeclarations) {
+ var c = tdecl as Constant;
+ if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;
+ ss.Add(c.Name);
+ }
+ outcome = svcgen.FindLeastToVerify(impl, ref ss);
+ errors = new List<Counterexample>();
+ Console.Write("Result: ");
+ foreach (var s in ss) {
+ Console.Write("{0} ", s);
+ }
+ Console.WriteLine();
+ }
+ else {
+ outcome = vcgen.VerifyImplementation(impl, out errors);
+ if (CommandLineOptions.Clo.ExtractLoops && vcgen is VCGen && errors != null) {
+ for (int i = 0; i < errors.Count; i++) {
+ errors[i] = (vcgen as VCGen).extractLoopTrace(errors[i], impl.Name, program, extractLoopMappingInfo);
+ }
+ }
+ }
+ }
+ catch (VCGenException e) {
+ ReportBplError(impl, String.Format("Error BP5010: {0} Encountered in implementation {1}.", e.Message, impl.Name), true, true);
+ errors = null;
+ outcome = VCGen.Outcome.Inconclusive;
+ }
+ catch (UnexpectedProverOutputException upo) {
+ AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message);
+ errors = null;
+ outcome = VCGen.Outcome.Inconclusive;
+ }
+
+ string timeIndication = "";
+ DateTime end = DateTime.UtcNow;
+ TimeSpan elapsed = end - start;
+ if (CommandLineOptions.Clo.Trace) {
+ int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;
+ timeIndication = string.Format(" [{0:F3} s, {1} proof obligation{2}] ", elapsed.TotalSeconds, poCount, poCount == 1 ? "" : "s");
+ } else if (CommandLineOptions.Clo.TraceProofObligations) {
+ int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;
+ timeIndication = string.Format(" [{0} proof obligation{1}] ", poCount, poCount == 1 ? "" : "s");
+ }
+
+ ProcessOutcome(outcome, errors, timeIndication, ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories);
+
+ if (CommandLineOptions.Clo.XmlSink != null) {
+ CommandLineOptions.Clo.XmlSink.WriteEndMethod(outcome.ToString().ToLowerInvariant(), end, elapsed);
+ }
+ if (outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace) {
+ Console.Out.Flush();
+ }
+ }
+ }
+
+ vcgen.Close();
+ cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();
+
+
+ #endregion
+
+ return PipelineOutcome.VerificationCompleted;
+ }
+
+ private static void AddPadding(ref string string1, ref string string2)
+ {
+ if (string1.Length < string2.Length)
+ {
+ for (int i = (string2.Length - string1.Length); i > 0; --i)
+ {
+ string1 += " ";
+ }
+ }
+ else
+ {
+ for (int i = (string1.Length - string2.Length); i > 0; --i)
+ {
+ string2 += " ";
+ }
+ }
+ }
+
+ private static string TrimLeadingSpaces(string s1, int noOfSpaces)
+ {
+ if (String.IsNullOrWhiteSpace(s1))
+ {
+ return s1;
+ }
+
+ int index;
+ for (index = 0; (index + 1) < s1.Length && Char.IsWhiteSpace(s1[index]); ++index);
+ string returnString = s1.Substring(index);
+ for (int i = noOfSpaces; i > 0; --i)
+ {
+ returnString = " " + returnString;
+ }
+ return returnString;
+ }
+
+ static QKeyValue GetAttributes(Absy a)
+ {
+ if (a is PredicateCmd)
+ {
+ return (a as PredicateCmd).Attributes;
+ }
+ else if (a is Requires)
+ {
+ return (a as Requires).Attributes;
+ }
+ else if (a is Ensures)
+ {
+ return (a as Ensures).Attributes;
+ }
+ else if (a is CallCmd)
+ {
+ return (a as CallCmd).Attributes;
+ }
+ //Debug.Assert(false);
+ return null;
+ }
+
static Model.Func ExtractIncarnationFromModel(Model m, string varName)
{
Model.Func lastFunc = null;
@@ -964,191 +1271,6 @@ namespace Microsoft.Boogie */
}
- static void ProcessOutcome(VC.VCGen.Outcome outcome, List<Counterexample> errors, string timeIndication,
- ref int errorCount, ref int verified, ref int inconclusives, ref int timeOuts, ref int outOfMemories)
- {
- switch (outcome)
- {
- default:
- Contract.Assert(false); // unexpected outcome
- throw new cce.UnreachableException();
- case VCGen.Outcome.ReachedBound:
- Inform(String.Format("{0}verified", timeIndication));
- Console.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound));
- verified++;
- break;
- case VCGen.Outcome.Correct:
- if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
- {
- Inform(String.Format("{0}credible", timeIndication));
- verified++;
- }
- else
- {
- Inform(String.Format("{0}verified", timeIndication));
- verified++;
- }
- break;
- case VCGen.Outcome.TimedOut:
- timeOuts++;
- Inform(String.Format("{0}timed out", timeIndication));
- break;
- case VCGen.Outcome.OutOfMemory:
- outOfMemories++;
- Inform(String.Format("{0}out of memory", timeIndication));
- break;
- case VCGen.Outcome.Inconclusive:
- inconclusives++;
- Inform(String.Format("{0}inconclusive", timeIndication));
- break;
- case VCGen.Outcome.Errors:
- if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
- {
- Inform(String.Format("{0}doomed", timeIndication));
- errorCount++;
- } //else {
- Contract.Assert(errors != null); // guaranteed by postcondition of VerifyImplementation
- {
- // BP1xxx: Parsing errors
- // BP2xxx: Name resolution errors
- // BP3xxx: Typechecking errors
- // BP4xxx: Abstract interpretation errors (Is there such a thing?)
- // BP5xxx: Verification errors
-
- errors.Sort(new CounterexampleComparer());
- foreach (Counterexample error in errors)
- {
- if (error is CallCounterexample)
- {
- CallCounterexample err = (CallCounterexample)error;
- if (QKeyValue.FindBoolAttribute(err.FailingRequires.Attributes, "barrier_divergence"))
- {
- ReportBarrierDivergence(err.FailingCall);
- }
- else if (QKeyValue.FindBoolAttribute(err.FailingRequires.Attributes, "race"))
- {
- int byteOffset = -1, elemOffset = -1, elemWidth = -1;
- string thread1 = null, thread2 = null, group1 = null, group2 = null, arrName = null;
- //TODO: make this a command line argument.
- bool detailedTrace = false;
- string threadOneFailAccess = null, threadTwoFailAccess = null;
-
- Variable offsetVar = ExtractOffsetVar(err.FailingRequires.Condition as NAryExpr);
- /* Right now the offset incarnation that is extracted is the penultimate one if
- * there is more than one incarnation, or the last one if there is only one incarnation.
- * TODO: In future, we should know the exact incarnation to extract. This information is
- * available when the CallCounterexample is created in VC.cs AssertCmdToCounterexample() (line 2405)
- * The condition of the AssertRequiresCmd contains the incarnation information, so this should be passed
- * on to the Requires of the created CallCounterexample. This can either be done by replacing the condition
- * of the Requires with the condition from AssertRequiresCmd (containing incarnation information) or creating
- * a separate field in the Requires to store this original condition.
- */
- Model.Func offsetFunc = ExtractIncarnationFromModel(error.Model, offsetVar.Name);
- Debug.Assert(offsetFunc != null, "ProcessOutcome(): Could not extract incarnation.");
- GetInfoFromVarAndFunc(offsetVar.Attributes, offsetFunc, out byteOffset, out elemOffset, out elemWidth, out arrName);
-
- Debug.Assert(error.Model != null, "ProcessOutcome(): null model");
- GetThreadsAndGroupsFromModel(err.Model, out thread1, out thread2, out group1, out group2, true);
-
- if (QKeyValue.FindBoolAttribute(err.FailingRequires.Attributes, "write_read"))
- {
- err.FailingRequires.Attributes = GetSourceLocInfo(error, "WRITE");
- threadOneFailAccess = "WRITE";
- threadTwoFailAccess = "READ";
- ReportRace(err.FailingCall, err.FailingRequires, thread1, thread2, group1, group2, arrName, byteOffset, RaceType.WR);
- }
- else if (QKeyValue.FindBoolAttribute(err.FailingRequires.Attributes, "read_write"))
- {
- err.FailingRequires.Attributes = GetSourceLocInfo(error, "READ");
- threadOneFailAccess = "READ";
- threadTwoFailAccess = "WRITE";
- ReportRace(err.FailingCall, err.FailingRequires, thread1, thread2, group1, group2, arrName, byteOffset, RaceType.RW);
-
- }
- else if (QKeyValue.FindBoolAttribute(err.FailingRequires.Attributes, "write_write"))
- {
- err.FailingRequires.Attributes = GetSourceLocInfo(error, "WRITE");
- threadOneFailAccess = "WRITE";
- threadTwoFailAccess = "WRITE";
- ReportRace(err.FailingCall, err.FailingRequires, thread1, thread2, group1, group2, arrName, byteOffset, RaceType.WW);
- }
-
- if (detailedTrace)
- {
- string fname = QKeyValue.FindStringAttribute(err.FailingCall.Attributes, "fname");
- Debug.Assert(!String.IsNullOrEmpty(fname));
- int colOneSize = fname.Length + 11;
- string colTwoHeader = " T " + GetThreadOne(error.Model, false) + " G " + GetGroupOne(error.Model, false) + " ";
- string colThreeHeader = " T " + GetThreadTwo(error.Model, false) + " G " + GetGroupTwo(error.Model, false) + " ";
-
- int colTwoSize = colTwoHeader.Length + 2;
- int colThreeSize = colTwoHeader.Length + 2;
-
- PrintDetailedTraceHeader(colTwoHeader, colThreeHeader, colOneSize, colTwoSize, colThreeSize);
- PrintDetailedTrace(err, colOneSize, colTwoSize, colThreeSize, elemOffset, elemWidth, threadOneFailAccess, threadTwoFailAccess);
- }
- }
- else
- {
- ReportRequiresFailure(err.FailingCall, err.FailingRequires);
- }
- }
- else if (error is ReturnCounterexample)
- {
- ReturnCounterexample err = (ReturnCounterexample)error;
- ReportEnsuresFailure(err.FailingEnsures);
- }
- else
- {
- AssertCounterexample err = (AssertCounterexample)error;
- if (err.FailingAssert is LoopInitAssertCmd)
- {
- ReportInvariantEntryFailure(err.FailingAssert);
- }
- else if (err.FailingAssert is LoopInvMaintainedAssertCmd)
- {
- ReportInvariantMaintedFailure(err.FailingAssert);
- }
- else
- {
- ReportFailingAssert(err.FailingAssert);
- }
- }
- errorCount++;
- }
- //}
- Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));
- }
- break;
- }
- }
-
- private static void PrintDetailedTraceHeader(string colTwoHeader, string colThreeHeader, int locationColSize, int colTwoSize, int colThreeSize)
- {
- Console.Write("\nLocation");
- PrintNChars(locationColSize - "Location".Length, ' ');
- Console.WriteLine("|{0}|{1}", colTwoHeader + Chars(colTwoSize - colTwoHeader.Length, ' '), colThreeHeader + Chars(colThreeSize - colThreeHeader.Length, ' '));
- PrintNChars(locationColSize, '-');
- Console.Write("|");
- PrintNChars(colTwoSize, '-');
- Console.Write("|");
- PrintNChars(colThreeSize, '-');
- Console.WriteLine("");
- }
-
- private static void PrintNChars(int n, char c)
- {
- for (int i = 0; i < n; ++i)
- {
- Console.Write(c);
- }
- }
-
- private static string Chars(int n, char c)
- {
- return new String(c, n);
- }
-
private static void ReportFailingAssert(Absy node)
{
Console.WriteLine("");
@@ -1511,247 +1633,5 @@ namespace Microsoft.Boogie return null;
}
- /// <summary>
- /// Given a resolved and type checked Boogie program, infers invariants for the program
- /// and then attempts to verify it. Returns:
- /// - Done if command line specified no verification
- /// - FatalError if a fatal error occurred, in which case an error has been printed to console
- /// - VerificationCompleted if inference and verification completed, in which the out
- /// parameters contain meaningful values
- /// </summary>
- static PipelineOutcome InferAndVerify(Program program,
- out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories)
- {
- Contract.Requires(program != null);
- Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));
-
- errorCount = verified = inconclusives = timeOuts = outOfMemories = 0;
-
- // ---------- Infer invariants --------------------------------------------------------
-
- // Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)
- if (CommandLineOptions.Clo.UseAbstractInterpretation) {
- if (!CommandLineOptions.Clo.Ai.J_Intervals && !CommandLineOptions.Clo.Ai.J_Trivial) {
- // use /infer:j as the default
- CommandLineOptions.Clo.Ai.J_Intervals = true;
- }
- }
- Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);
-
- if (CommandLineOptions.Clo.LoopUnrollCount != -1)
- {
- program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);
- }
-
- if (CommandLineOptions.Clo.DoPredication && CommandLineOptions.Clo.StratifiedInlining > 0)
- {
- BlockPredicator.Predicate(program, false, false);
- if (CommandLineOptions.Clo.PrintInstrumented)
- {
- using (TokenTextWriter writer = new TokenTextWriter(Console.Out))
- {
- program.Emit(writer);
- }
- }
- }
-
- Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo = null;
- if (CommandLineOptions.Clo.ExtractLoops)
- {
- extractLoopMappingInfo = program.ExtractLoops();
- }
-
- if (CommandLineOptions.Clo.PrintInstrumented)
- {
- program.Emit(new TokenTextWriter(Console.Out));
- }
-
- if (CommandLineOptions.Clo.ExpandLambdas)
- {
- LambdaHelper.ExpandLambdas(program);
- //PrintBplFile ("-", program, true);
- }
-
- // ---------- Verify ------------------------------------------------------------
-
- if (!CommandLineOptions.Clo.Verify)
- {
- return PipelineOutcome.Done;
- }
-
- #region Run Houdini and verify
- if (CommandLineOptions.Clo.ContractInfer)
- {
- Houdini.Houdini houdini = new Houdini.Houdini(program);
- Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();
- if (CommandLineOptions.Clo.PrintAssignment)
- {
- Console.WriteLine("Assignment computed by Houdini:");
- foreach (var x in outcome.assignment)
- {
- Console.WriteLine(x.Key + " = " + x.Value);
- }
- }
- if (CommandLineOptions.Clo.Trace)
- {
- int numTrueAssigns = 0;
- foreach (var x in outcome.assignment)
- {
- if (x.Value)
- numTrueAssigns++;
- }
- Console.WriteLine("Number of true assignments = " + numTrueAssigns);
- Console.WriteLine("Number of false assignments = " + (outcome.assignment.Count - numTrueAssigns));
- Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime);
- Console.WriteLine("Unsat core prover time = " + Houdini.HoudiniSession.unsatCoreProverTime);
- Console.WriteLine("Number of prover queries = " + Houdini.HoudiniSession.numProverQueries);
- Console.WriteLine("Number of unsat core prover queries = " + Houdini.HoudiniSession.numUnsatCoreProverQueries);
- Console.WriteLine("Number of unsat core prunings = " + Houdini.HoudiniSession.numUnsatCorePrunings);
- }
-
- foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)
- {
- ProcessOutcome(x.outcome, x.errors, "", ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories);
- }
- //errorCount = outcome.ErrorCount;
- //verified = outcome.Verified;
- //inconclusives = outcome.Inconclusives;
- //timeOuts = outcome.TimeOuts;
- //outOfMemories = 0;
- return PipelineOutcome.Done;
- }
- #endregion
-
- #region Verify each implementation
-
- ConditionGeneration vcgen = null;
- try
- {
- if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
- {
- vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
- }
- else if (CommandLineOptions.Clo.StratifiedInlining > 0)
- {
- vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
- }
- else
- {
- vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
- }
- }
- catch (ProverException e)
- {
- ErrorWriteLine("Fatal Error: ProverException: {0}", e);
- return PipelineOutcome.FatalError;
- }
-
- // operate on a stable copy, in case it gets updated while we're running
- var decls = program.TopLevelDeclarations.ToArray();
- foreach (Declaration decl in decls)
- {
- Contract.Assert(decl != null);
- int prevAssertionCount = vcgen.CumulativeAssertionCount;
- Implementation impl = decl as Implementation;
- if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification)
- {
- List<Counterexample/*!*/>/*?*/ errors;
-
- DateTime start = new DateTime(); // to please compiler's definite assignment rules
- if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null)
- {
- start = DateTime.UtcNow;
- if (CommandLineOptions.Clo.Trace)
- {
- Console.WriteLine();
- Console.WriteLine("Verifying {0} ...", impl.Name);
- }
- if (CommandLineOptions.Clo.XmlSink != null)
- {
- CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, start);
- }
- }
-
- VCGen.Outcome outcome;
- try
- {
- if (CommandLineOptions.Clo.inferLeastForUnsat != null)
- {
- var svcgen = vcgen as VC.StratifiedVCGen;
- Contract.Assert(svcgen != null);
- var ss = new HashSet<string>();
- foreach (var tdecl in program.TopLevelDeclarations)
- {
- var c = tdecl as Constant;
- if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;
- ss.Add(c.Name);
- }
- outcome = svcgen.FindLeastToVerify(impl, ref ss);
- errors = new List<Counterexample>();
- Console.Write("Result: ");
- foreach (var s in ss)
- {
- Console.Write("{0} ", s);
- }
- Console.WriteLine();
- }
- else
- {
- outcome = vcgen.VerifyImplementation(impl, out errors);
- if (CommandLineOptions.Clo.ExtractLoops && vcgen is VCGen && errors != null)
- {
- for (int i = 0; i < errors.Count; i++)
- {
- errors[i] = (vcgen as VCGen).extractLoopTrace(errors[i], impl.Name, program, extractLoopMappingInfo);
- }
- }
- }
- }
- catch (VCGenException e)
- {
- ReportBplError(impl, String.Format("Error BP5010: {0} Encountered in implementation {1}.", e.Message, impl.Name), true, true);
- errors = null;
- outcome = VCGen.Outcome.Inconclusive;
- }
- catch (UnexpectedProverOutputException upo)
- {
- AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message);
- errors = null;
- outcome = VCGen.Outcome.Inconclusive;
- }
-
- string timeIndication = "";
- DateTime end = DateTime.UtcNow;
- TimeSpan elapsed = end - start;
- if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null)
- {
- if (CommandLineOptions.Clo.Trace)
- {
- int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;
- timeIndication = string.Format(" [{0} s, {1} proof obligation{2}] ", elapsed.ToString("%s\\.fff"), poCount, poCount == 1 ? "" : "s");
- }
- }
-
- ProcessOutcome(outcome, errors, timeIndication, ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories);
-
- if (CommandLineOptions.Clo.XmlSink != null)
- {
- CommandLineOptions.Clo.XmlSink.WriteEndMethod(outcome.ToString().ToLowerInvariant(), end, elapsed);
- }
- if (outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace)
- {
- Console.Out.Flush();
- }
- }
- }
-
- vcgen.Close();
- cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();
-
-
- #endregion
-
- return PipelineOutcome.VerificationCompleted;
- }
}
}
|