diff options
36 files changed, 1085 insertions, 654 deletions
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index c8300189..c6d8e7a4 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -168,18 +168,46 @@ namespace BytecodeTranslator { return 1;
}
- result = TranslateAssembly(assemblyNames, heap, options, exemptionList, whiteList);
+ var pgm = TranslateAssembly(assemblyNames, heap, options, exemptionList, whiteList);
+ var fileName = assemblyNames[0];
+ fileName = Path.GetFileNameWithoutExtension(fileName);
+ string outputFileName = fileName + ".bpl";
+ Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(outputFileName);
+ Prelude.Emit(writer);
+ pgm.Emit(writer);
+ writer.Close();
+ return 0; // success
} catch (Exception e) { // swallow everything and just return an error code
Console.WriteLine("The byte-code translator failed: {0}", e.Message);
// Console.WriteLine("Stack trace: {0}", e.StackTrace);
return -1;
}
- return result;
}
private static List<IModule> modules;
- public static int TranslateAssembly(List<string> assemblyNames, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {
+
+ public static int TranslateAssemblyAndWriteOutput(List<string> assemblyNames, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {
+ Contract.Requires(assemblyNames != null);
+ Contract.Requires(heapFactory != null);
+ try {
+ var pgm = TranslateAssembly(assemblyNames, heapFactory, options, exemptionList, whiteList);
+ var fileName = assemblyNames[0];
+ fileName = Path.GetFileNameWithoutExtension(fileName);
+ string outputFileName = fileName + ".bpl";
+ Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(outputFileName);
+ Prelude.Emit(writer);
+ pgm.Emit(writer);
+ writer.Close();
+ return 0; // success
+ } catch (Exception e) { // swallow everything and just return an error code
+ Console.WriteLine("The byte-code translator failed: {0}", e.Message);
+ // Console.WriteLine("Stack trace: {0}", e.StackTrace);
+ return -1;
+ }
+ }
+
+ public static Bpl.Program/*?*/ TranslateAssembly(List<string> assemblyNames, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {
Contract.Requires(assemblyNames != null);
Contract.Requires(heapFactory != null);
@@ -193,6 +221,8 @@ namespace BytecodeTranslator { var host = new CodeContractAwareHostEnvironment(libPaths != null ? libPaths : Enumerable<string>.Empty, true, true);
Host = host;
+ Bpl.CommandLineOptions.Install(new Bpl.CommandLineOptions());
+
#region Assemlies to translate (via cmd line)
modules = new List<IModule>();
var contractExtractors = new Dictionary<IUnit, IContractProvider>();
@@ -266,8 +296,7 @@ namespace BytecodeTranslator { #endregion
if (modules.Count == 0) {
- Console.WriteLine("No input assemblies to translate.");
- return -1;
+ throw new TranslationException("No input assemblies to translate.");
}
var primaryModule = modules[0];
@@ -378,14 +407,10 @@ namespace BytecodeTranslator { // }
//}
//sink.TranslatedProgram.TopLevelDeclarations = goodDecls;
-
- Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(outputFileName);
- Prelude.Emit(writer);
- sink.TranslatedProgram.Emit(writer);
- writer.Close();
- return 0; // success
+ return sink.TranslatedProgram;
}
+
private static void finalizeNavigationAnalysisAndBoogieCode(string phoneControlsConfigFile, Sink sink, string outputFileName) {
outputBoogieTrackedControlConfiguration(phoneControlsConfigFile);
checkTransitivelyCalledBackKeyNavigations(modules);
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index f68465d1..39c9986a 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -10,7 +10,7 @@ procedure {:inline 1} Alloc() returns (x: Ref); -implementation Alloc() returns (x: Ref)
+implementation {:inline 1} Alloc() returns (x: Ref)
{
assume $Alloc[x] == false && x != null;
$Alloc[x] := true;
@@ -38,7 +38,7 @@ procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref); -implementation System.Object.GetType(this: Ref) returns ($result: Ref)
+implementation {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)
{
$result := $TypeOf($DynamicType(this));
}
@@ -63,7 +63,7 @@ procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.Parameteriz -implementation System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)
+implementation {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)
{
assume $ThreadDelegate(this) == start$in;
}
@@ -74,7 +74,7 @@ procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, par -implementation System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)
+implementation {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)
{
call {:async} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in);
}
@@ -85,7 +85,7 @@ procedure {:inline 1} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$S -implementation Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref)
+implementation {:inline 1} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref)
{
$Exception := null;
call System.Threading.ParameterizedThreadStart.Invoke$System.Object(this, obj$in);
@@ -101,7 +101,7 @@ procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart -implementation System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref)
+implementation {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref)
{
assume $ThreadDelegate(this) == start$in;
}
@@ -112,7 +112,7 @@ procedure {:inline 1} System.Threading.Thread.Start(this: Ref); -implementation System.Threading.Thread.Start(this: Ref)
+implementation {:inline 1} System.Threading.Thread.Start(this: Ref)
{
call {:async} Wrapper_System.Threading.ThreadStart.Invoke($ThreadDelegate(this));
}
@@ -123,7 +123,7 @@ procedure {:inline 1} Wrapper_System.Threading.ThreadStart.Invoke(this: Ref); -implementation Wrapper_System.Threading.ThreadStart.Invoke(this: Ref)
+implementation {:inline 1} Wrapper_System.Threading.ThreadStart.Invoke(this: Ref)
{
$Exception := null;
call System.Threading.ThreadStart.Invoke(this);
@@ -159,7 +159,7 @@ procedure {:inline 1} DelegateAdd(a: Ref, b: Ref) returns (c: Ref); -implementation DelegateAdd(a: Ref, b: Ref) returns (c: Ref)
+implementation {:inline 1} DelegateAdd(a: Ref, b: Ref) returns (c: Ref)
{
var d: Delegate;
@@ -184,7 +184,7 @@ procedure {:inline 1} DelegateRemove(a: Ref, b: Ref) returns (c: Ref); -implementation DelegateRemove(a: Ref, b: Ref) returns (c: Ref)
+implementation {:inline 1} DelegateRemove(a: Ref, b: Ref) returns (c: Ref)
{
var d: Delegate;
@@ -213,7 +213,7 @@ procedure {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref); -implementation DelegateCreate(d: Delegate) returns (c: Ref)
+implementation {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref)
{
call c := Alloc();
assume $Delegate(c) == MultisetSingleton(d);
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index 9484ee38..22431543 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -8,7 +8,7 @@ procedure {:inline 1} Alloc() returns (x: Ref); -implementation Alloc() returns (x: Ref)
+implementation {:inline 1} Alloc() returns (x: Ref)
{
assume $Alloc[x] == false && x != null;
$Alloc[x] := true;
@@ -36,7 +36,7 @@ procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref); -implementation System.Object.GetType(this: Ref) returns ($result: Ref)
+implementation {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)
{
$result := $TypeOf($DynamicType(this));
}
@@ -61,7 +61,7 @@ procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.Parameteriz -implementation System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)
+implementation {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)
{
assume $ThreadDelegate(this) == start$in;
}
@@ -72,7 +72,7 @@ procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, par -implementation System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)
+implementation {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)
{
call {:async} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in);
}
@@ -83,7 +83,7 @@ procedure {:inline 1} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$S -implementation Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref)
+implementation {:inline 1} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref)
{
$Exception := null;
call System.Threading.ParameterizedThreadStart.Invoke$System.Object(this, obj$in);
@@ -99,7 +99,7 @@ procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart -implementation System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref)
+implementation {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref)
{
assume $ThreadDelegate(this) == start$in;
}
@@ -110,7 +110,7 @@ procedure {:inline 1} System.Threading.Thread.Start(this: Ref); -implementation System.Threading.Thread.Start(this: Ref)
+implementation {:inline 1} System.Threading.Thread.Start(this: Ref)
{
call {:async} Wrapper_System.Threading.ThreadStart.Invoke($ThreadDelegate(this));
}
@@ -121,7 +121,7 @@ procedure {:inline 1} Wrapper_System.Threading.ThreadStart.Invoke(this: Ref); -implementation Wrapper_System.Threading.ThreadStart.Invoke(this: Ref)
+implementation {:inline 1} Wrapper_System.Threading.ThreadStart.Invoke(this: Ref)
{
$Exception := null;
call System.Threading.ThreadStart.Invoke(this);
@@ -157,7 +157,7 @@ procedure {:inline 1} DelegateAdd(a: Ref, b: Ref) returns (c: Ref); -implementation DelegateAdd(a: Ref, b: Ref) returns (c: Ref)
+implementation {:inline 1} DelegateAdd(a: Ref, b: Ref) returns (c: Ref)
{
var d: Delegate;
@@ -182,7 +182,7 @@ procedure {:inline 1} DelegateRemove(a: Ref, b: Ref) returns (c: Ref); -implementation DelegateRemove(a: Ref, b: Ref) returns (c: Ref)
+implementation {:inline 1} DelegateRemove(a: Ref, b: Ref) returns (c: Ref)
{
var d: Delegate;
@@ -211,7 +211,7 @@ procedure {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref); -implementation DelegateCreate(d: Delegate) returns (c: Ref)
+implementation {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref)
{
call c := Alloc();
assume $Delegate(c) == MultisetSingleton(d);
diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs index a8b5fdb2..a48be6af 100644 --- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs +++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs @@ -61,7 +61,7 @@ namespace TranslationTest { #endregion
private string ExecuteTest(string assemblyName, HeapFactory heapFactory) {
- BCT.TranslateAssembly(new List<string>{assemblyName}, heapFactory, new Options(), null, false);
+ BCT.TranslateAssemblyAndWriteOutput(new List<string> { assemblyName }, heapFactory, new Options(), null, false);
var fileName = Path.ChangeExtension(assemblyName, "bpl");
var s = File.ReadAllText(fileName);
return s;
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 7b5576c1..4073c722 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -444,6 +444,9 @@ namespace Microsoft.Boogie { foreach (var x in outcome.assignment) {
Console.WriteLine(x.Key + " = " + x.Value);
}
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime);
+ }
errorCount = outcome.ErrorCount;
verified = outcome.Verified;
inconclusives = outcome.Inconclusives;
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 32b27ae6..0aaf3c46 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -308,7 +308,7 @@ namespace Microsoft.Boogie { Contract.Requires(rc != null);
// first resolve type constructors
foreach (Declaration d in TopLevelDeclarations) {
- if (d is TypeCtorDecl)
+ if (d is TypeCtorDecl && !QKeyValue.FindBoolAttribute(d.Attributes, "ignore"))
d.Resolve(rc);
}
@@ -316,7 +316,7 @@ namespace Microsoft.Boogie { List<TypeSynonymDecl/*!*/>/*!*/ synonymDecls = new List<TypeSynonymDecl/*!*/>();
foreach (Declaration d in TopLevelDeclarations) {
Contract.Assert(d != null);
- if (d is TypeSynonymDecl)
+ if (d is TypeSynonymDecl && !QKeyValue.FindBoolAttribute(d.Attributes, "ignore"))
synonymDecls.Add((TypeSynonymDecl)d);
}
@@ -1044,7 +1044,7 @@ namespace Microsoft.Boogie { }
public override void Register(ResolutionContext rc) {
//Contract.Requires(rc != null);
- // nothing to register
+ rc.AddAxiom(this);
}
public override void Resolve(ResolutionContext rc) {
//Contract.Requires(rc != null);
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index ae051b40..676ffd5a 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -2161,6 +2161,11 @@ namespace Microsoft.Boogie { {
assume.Attributes = Attributes;
}
+ if (QKeyValue.FindBoolAttribute(e.Attributes, "candidate"))
+ {
+ assume.Attributes = new QKeyValue(Token.NoToken, "candidate", new List<object>(), assume.Attributes);
+ assume.Attributes.Params.Add(this.callee);
+ }
#endregion
newBlockBody.Add(assume);
}
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index 0f29c9a0..cae8bd92 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -533,6 +533,13 @@ namespace Microsoft.Boogie { return l.asBigNum.ToIntSafe;
return defl;
}
+
+ public override Absy Clone() {
+ List<object> newParams = new List<object>();
+ foreach (object o in Params)
+ newParams.Add(o);
+ return new QKeyValue(tok, Key, newParams, (Next == null) ? null : (QKeyValue)Next.Clone());
+ }
}
public class Trigger : Absy {
@@ -546,7 +553,6 @@ namespace Microsoft.Boogie { Contract.Invariant(Pos || Tr.Length == 1);
}
-
public Trigger Next;
public Trigger(IToken tok, bool pos, ExprSeq tr)
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 7519fb4c..c7950c9a 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -585,9 +585,8 @@ Procedure<out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl> | { Spec<pre, mods, post> }
ImplBody<out locals, out stmtList>
(.
- // here we attach kv only to the Procedure, not its implementation
impl = new Implementation(x, x.val, typeParams,
- Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors);
+ Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
.)
)
(. proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); .)
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index adc7e2f0..c9f6445c 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -388,6 +388,27 @@ namespace Microsoft.Boogie { codeCopier.OldSubst = null;
}
+ private Cmd InlinedRequires(Implementation impl, CallCmd callCmd, Requires req) {
+ Requires/*!*/ reqCopy = (Requires/*!*/)cce.NonNull(req.Clone());
+ if (req.Free)
+ reqCopy.Condition = Expr.True;
+ else
+ reqCopy.Condition = codeCopier.CopyExpr(req.Condition);
+ AssertCmd/*!*/ a = new AssertRequiresCmd(callCmd, reqCopy);
+ a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;
+ return a;
+ }
+
+ private Cmd InlinedEnsures(Implementation impl, CallCmd callCmd, Ensures ens) {
+ if (impl.FindExprAttribute("inline") != null && !ens.Free) {
+ Ensures/*!*/ ensCopy = (Ensures/*!*/)cce.NonNull(ens.Clone());
+ ensCopy.Condition = codeCopier.CopyExpr(ens.Condition);
+ return new AssertEnsuresCmd(ensCopy);
+ }
+ else {
+ return new AssumeCmd(ens.tok, codeCopier.CopyExpr(ens.Condition));
+ }
+ }
// result[0] is the entry block
protected List<Block/*!*/>/*!*/ CreateInlinedBlocks(CallCmd callCmd, Implementation impl, string nextBlockLabel) {
@@ -418,17 +439,20 @@ namespace Microsoft.Boogie { inCmds.Add(cmd);
}
- // inject non-free requires
+ // inject requires
for (int i = 0; i < proc.Requires.Length; i++) {
Requires/*!*/ req = cce.NonNull(proc.Requires[i]);
+ inCmds.Add(InlinedRequires(impl, callCmd, req));
+ /*
if (!req.Free && !QKeyValue.FindBoolAttribute(req.Attributes, "candidate")) {
- Requires/*!*/ reqCopy = (Requires/*!*/)cce.NonNull(req.Clone());
+ Requires reqCopy = (Requires)cce.NonNull(req.Clone());
reqCopy.Condition = codeCopier.CopyExpr(req.Condition);
- AssertCmd/*!*/ a = new AssertRequiresCmd(callCmd, reqCopy);
+ AssertCmd a = new AssertRequiresCmd(callCmd, reqCopy);
Contract.Assert(a != null);
a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;
inCmds.Add(a);
}
+ */
}
VariableSeq locVars = cce.NonNull(impl.OriginalLocVars);
@@ -483,16 +507,19 @@ namespace Microsoft.Boogie { // create out block
CmdSeq outCmds = new CmdSeq();
- // inject non-free ensures
+ // inject ensures
for (int i = 0; i < proc.Ensures.Length; i++) {
Ensures/*!*/ ens = cce.NonNull(proc.Ensures[i]);
+ outCmds.Add(InlinedEnsures(impl, callCmd, ens));
+ /*
if (!ens.Free && !QKeyValue.FindBoolAttribute(ens.Attributes, "candidate")) {
- Ensures/*!*/ ensCopy = (Ensures/*!*/)cce.NonNull(ens.Clone());
+ Ensures ensCopy = (Ensures)cce.NonNull(ens.Clone());
ensCopy.Condition = codeCopier.CopyExpr(ens.Condition);
- AssertCmd/*!*/ a = new AssertEnsuresCmd(ensCopy);
+ AssertCmd a = new AssertEnsuresCmd(ensCopy);
Contract.Assert(a != null);
outCmds.Add(a);
}
+ */
}
// assign out params
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 34f43896..5bfbbfc2 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -503,7 +503,7 @@ private class BvBounds : Expr { }
ImplBody(out locals, out stmtList);
impl = new Implementation(x, x.val, typeParams,
- Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors);
+ Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
} else SynErr(91);
proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv);
diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs index 251ca1db..128df8c5 100644 --- a/Source/Core/ResolutionContext.cs +++ b/Source/Core/ResolutionContext.cs @@ -349,6 +349,26 @@ namespace Microsoft.Boogie { // not present in the relevant levels
return null;
}
+ Hashtable axioms = new Hashtable();
+
+ public void AddAxiom(Axiom axiom) {
+ string axiomName = QKeyValue.FindStringAttribute(axiom.Attributes, "name");
+ if (axiomName == null)
+ return;
+ var previous = (Axiom)axioms[axiomName];
+ if (previous == null) {
+ axioms.Add(axiomName, axiom);
+ }
+ else {
+ var r = (Axiom)SelectNonExtern(axiom, previous);
+ if (r == null) {
+ Error(axiom, "more than one declaration of axiom name: {0}", axiomName);
+ }
+ else {
+ axioms[axiomName] = r;
+ }
+ }
+ }
// ------------------------------ Functions/Procedures ------------------------------
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 745d50ef..4a1388d9 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -31,6 +31,7 @@ namespace Microsoft.Dafny public string DafnyPrintFile = null;
public bool Compile = true;
public bool ForceCompile = false;
+ public bool SpillTargetCode = false;
protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {
var args = ps.args; // convenient synonym
@@ -51,12 +52,21 @@ namespace Microsoft.Dafny case "compile": {
int compile = 0;
if (ps.GetNumericArgument(ref compile, 3)) {
+ // convert option to two booleans
Compile = compile == 1 || compile == 2;
ForceCompile = compile == 2;
}
return true;
}
+ case "spillTargetCode": {
+ int spill = 0;
+ if (ps.GetNumericArgument(ref spill, 2)) {
+ SpillTargetCode = spill != 0; // convert to a boolean
+ }
+ return true;
+ }
+
case "noCheating": {
int cheat = 0; // 0 is default, allows cheating
if (ps.GetNumericArgument(ref cheat, 2)) {
@@ -108,6 +118,10 @@ namespace Microsoft.Dafny program, compile Dafny program to C# program out.cs
2 - always attempt to compile Dafny program to C# program
out.cs, regardless of verification outcome
+ /spillTargetCode:<n>
+ 0 (default) - don't write the compiled Dafny program (but
+ still compile it, if /compile indicates to do so)
+ 1 - write the compiled Dafny program as a .cs file
/noCheating:<n>
0 (default) - allow assume statements and free invariants
1 - treat all assumptions as asserts, and drop free.
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index eed5cf59..80e24356 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -21,6 +21,7 @@ namespace Microsoft.Dafny using Microsoft.Boogie.AbstractInterpretation;
using System.Diagnostics;
using VC;
+ using System.CodeDom.Compiler;
using AI = Microsoft.AbstractInterpretationFramework;
public class DafnyDriver
@@ -173,12 +174,12 @@ namespace Microsoft.Dafny case PipelineOutcome.VerificationCompleted:
WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
if ((DafnyOptions.O.Compile && allOk && CommandLineOptions.Clo.ProcsToCheck == null) || DafnyOptions.O.ForceCompile)
- CompileDafnyProgram(dafnyProgram);
+ CompileDafnyProgram(dafnyProgram, fileNames[0]);
break;
case PipelineOutcome.Done:
WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
if (DafnyOptions.O.ForceCompile)
- CompileDafnyProgram(dafnyProgram);
+ CompileDafnyProgram(dafnyProgram, fileNames[0]);
break;
default:
// error has already been reported to user
@@ -190,17 +191,52 @@ namespace Microsoft.Dafny return exitValue;
}
- private static void CompileDafnyProgram(Dafny.Program dafnyProgram)
+ private static void CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyProgramName)
{
- string targetFilename = "out.cs";
- using (TextWriter target = new StreamWriter(new FileStream(targetFilename, System.IO.FileMode.Create))) {
- Dafny.Compiler compiler = new Dafny.Compiler(target);
- compiler.Compile(dafnyProgram);
- if (compiler.ErrorCount == 0) {
- Console.WriteLine("Compiled program written to {0}", targetFilename);
+ // Compile the Dafny program into a string that contains the C# program
+ StringWriter sw = new StringWriter();
+ Dafny.Compiler compiler = new Dafny.Compiler(sw);
+ compiler.Compile(dafnyProgram);
+ var csharpProgram = sw.ToString();
+ bool completeProgram = compiler.ErrorCount == 0;
+
+ // blurt out the code to a file
+ if (DafnyOptions.O.SpillTargetCode) {
+ string targetFilename = Path.ChangeExtension(dafnyProgramName, "cs");
+ using (TextWriter target = new StreamWriter(new FileStream(targetFilename, System.IO.FileMode.Create))) {
+ target.Write(csharpProgram);
+ if (completeProgram) {
+ Console.WriteLine("Compiled program written to {0}", targetFilename);
+ } else {
+ Console.WriteLine("File {0} contains the partially compiled program", targetFilename);
+ }
}
- else {
- Console.WriteLine("File {0} contains the partially compiled program", targetFilename);
+ }
+
+ // compile the program into an assembly
+ if (!completeProgram) {
+ // don't compile
+ } else if (!CodeDomProvider.IsDefinedLanguage("CSharp")) {
+ Console.WriteLine("Error: cannot compile, because there is no provider configured for input language CSharp");
+ } else {
+ var provider = CodeDomProvider.CreateProvider("CSharp");
+ var cp = new System.CodeDom.Compiler.CompilerParameters();
+ cp.GenerateExecutable = true;
+ // TODO: an improvement would be to generate a .dll if there is no Main method
+ cp.OutputAssembly = Path.ChangeExtension(dafnyProgramName, "exe");
+ cp.GenerateInMemory = false;
+ cp.ReferencedAssemblies.Add("System.Numerics.dll");
+ cp.CompilerOptions = "/debug";
+
+ var cr = provider.CompileAssemblyFromSource(cp, csharpProgram);
+ if (cr.Errors.Count == 0) {
+ Console.WriteLine("Compiled assembly into {0}", cr.PathToAssembly);
+ } else {
+ Console.WriteLine("Errors compiling program into {0}", cr.PathToAssembly);
+ foreach (var ce in cr.Errors) {
+ Console.WriteLine(ce.ToString());
+ Console.WriteLine();
+ }
}
}
}
diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs index bef0505e..99cc4b97 100644 --- a/Source/GPUVerify/CommandLineOptions.cs +++ b/Source/GPUVerify/CommandLineOptions.cs @@ -27,8 +27,6 @@ namespace GPUVerify public static bool Symmetry = false;
public static bool SetEncoding = false;
- public static bool RaceCheckingContract = false;
-
public static int Parse(string[] args)
{
for (int i = 0; i < args.Length; i++)
@@ -113,11 +111,6 @@ namespace GPUVerify Eager = true;
break;
- case "-raceCheckingContract":
- case "/raceCheckingContract":
- RaceCheckingContract = true;
- break;
-
case "-inference":
case "/inference":
Inference = true;
diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs index b17ca60f..84624e5d 100644 --- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs +++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs @@ -85,6 +85,8 @@ namespace GPUVerify Implementation LogReadOrWriteImplementation = new Implementation(v.tok, "_LOG_" + ReadOrWrite + "_" + v.Name, new TypeVariableSeq(), LogReadOrWriteProcedure.InParams, new VariableSeq(), locals, statements);
LogReadOrWriteImplementation.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });
+ LogReadOrWriteImplementation.Proc = LogReadOrWriteProcedure;
+
verifier.Program.TopLevelDeclarations.Add(LogReadOrWriteProcedure);
verifier.Program.TopLevelDeclarations.Add(LogReadOrWriteImplementation);
}
@@ -189,9 +191,12 @@ namespace GPUVerify bb.simpleCmds.Add(new AssignCmd(tok, lhss, rhss));
}
- public override void CheckForRaces(IToken tok, BigBlock bb, Variable v)
+ public override void CheckForRaces(IToken tok, BigBlock bb, Variable v, bool ReadWriteOnly)
{
- bb.simpleCmds.Add(new AssertCmd(tok, Expr.Not(GenerateRaceCondition(tok, v, "WRITE", "WRITE"))));
+ if (!ReadWriteOnly)
+ {
+ bb.simpleCmds.Add(new AssertCmd(tok, Expr.Not(GenerateRaceCondition(tok, v, "WRITE", "WRITE"))));
+ }
bb.simpleCmds.Add(new AssertCmd(tok, Expr.Not(GenerateRaceCondition(tok, v, "READ", "WRITE"))));
if (!CommandLineOptions.Symmetry)
{
@@ -229,9 +234,57 @@ namespace GPUVerify ));
}
+ if (FirstAccessType.Equals("WRITE") && SecondAccessType.Equals("WRITE") && !CommandLineOptions.FullAbstraction)
+ {
+ RaceCondition = Expr.And(RaceCondition, Expr.Neq(
+ MakeWrittenIndex(v, 1),
+ MakeWrittenIndex(v, 2)
+ ));
+ }
+
return RaceCondition;
}
+ private static Expr MakeWrittenIndex(Variable v, int OneOrTwo)
+ {
+ Expr result = new IdentifierExpr(v.tok, new VariableDualiser(OneOrTwo).VisitVariable(v.Clone() as Variable));
+
+ if (v.TypedIdent.Type is MapType)
+ {
+ MapType mt = v.TypedIdent.Type as MapType;
+ Debug.Assert(mt.Arguments.Length == 1);
+ Debug.Assert(GPUVerifier.IsIntOrBv32(mt.Arguments[0]));
+
+ result = Expr.Select(result,
+ new Expr[] { new IdentifierExpr(v.tok, new VariableDualiser(OneOrTwo).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, "WRITE"))) });
+
+ if (mt.Result is MapType)
+ {
+ MapType mt2 = mt.Result as MapType;
+ Debug.Assert(mt2.Arguments.Length == 1);
+ Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));
+
+ result = Expr.Select(result,
+ new Expr[] { new IdentifierExpr(v.tok, new VariableDualiser(OneOrTwo).VisitVariable(GPUVerifier.MakeOffsetYVariable(v, "WRITE"))) });
+
+ if (mt2.Result is MapType)
+ {
+ MapType mt3 = mt2.Arguments[0] as MapType;
+ Debug.Assert(mt3.Arguments.Length == 1);
+ Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));
+ Debug.Assert(!(mt3.Result is MapType));
+
+ result = Expr.Select(result,
+ new Expr[] { new IdentifierExpr(v.tok, new VariableDualiser(OneOrTwo).VisitVariable(GPUVerifier.MakeOffsetZVariable(v, "WRITE"))) });
+
+ }
+ }
+ }
+
+ return result;
+
+ }
+
internal static GlobalVariable MakeReadOrWriteHasOccurredVariable(Variable v, string ReadOrWrite)
{
return new GlobalVariable(v.tok, new TypedIdent(v.tok, "_" + ReadOrWrite + "_HAS_OCCURRED_" + v.Name, Microsoft.Boogie.Type.Bool));
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index c15327ca..5e33e78d 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -398,7 +398,7 @@ namespace GPUVerify if (impl.Name.Equals("_LOG_READ_" + v.Name) || impl.Name.Equals("_LOG_WRITE_" + v.Name))
{
BigBlock bb = new BigBlock(v.tok, "__CheckForRaces", new CmdSeq(), null, null);
- RaceInstrumenter.CheckForRaces(v.tok, bb, v);
+ RaceInstrumenter.CheckForRaces(v.tok, bb, v, impl.Name.Equals("_LOG_READ_" + v.Name));
StmtList newStatements = new StmtList(new List<BigBlock>(), v.tok);
foreach(BigBlock bb2 in impl.StructuredStmts.BigBlocks)
@@ -463,18 +463,11 @@ namespace GPUVerify }
AddCandidateRequires(Proc);
- if (CommandLineOptions.RaceCheckingContract)
- {
- RaceInstrumenter.AddRaceCheckingCandidateRequires(Proc);
- }
-
+ RaceInstrumenter.AddRaceCheckingCandidateRequires(Proc);
AddUserSuppliedCandidateRequires(Proc, UserSuppliedInvariants);
AddCandidateEnsures(Proc);
- if (CommandLineOptions.RaceCheckingContract)
- {
- RaceInstrumenter.AddRaceCheckingCandidateEnsures(Proc);
- }
+ RaceInstrumenter.AddRaceCheckingCandidateEnsures(Proc);
AddUserSuppliedCandidateEnsures(Proc, UserSuppliedInvariants);
}
@@ -987,35 +980,169 @@ namespace GPUVerify {
Debug.Assert(AssumeThreadIdsInRange != null);
- KernelProcedure.Requires.Add(new Requires(false, AssumeDistinctThreads));
- KernelProcedure.Requires.Add(new Requires(false, AssumeThreadIdsInRange));
+ foreach (Declaration D in Program.TopLevelDeclarations)
+ {
+ if (!(D is Procedure))
+ {
+ continue;
+ }
+ Procedure Proc = D as Procedure;
+ if (QKeyValue.FindIntAttribute(Proc.Attributes, "inline", -1) == 1)
+ {
+ continue;
+ }
+
+ Proc.Requires.Add(new Requires(false, AssumeDistinctThreads));
+ Proc.Requires.Add(new Requires(false, AssumeThreadIdsInRange));
+ }
}
else
{
Debug.Assert(AssumeThreadIdsInRange == null);
}
+ foreach (Declaration D in Program.TopLevelDeclarations)
+ {
+ if (!(D is Implementation))
+ {
+ continue;
+ }
+ Implementation Impl = D as Implementation;
+ if (QKeyValue.FindIntAttribute(Impl.Proc.Attributes, "inline", -1) == 1)
+ {
+ continue;
+ }
+ if (Impl.Proc == KernelProcedure)
+ {
+ continue;
+ }
+
+ EnsureDisabledThreadHasNoEffect(Impl);
+
+ }
}
- private void GeneratePreconditionsForDimension(ref Expr AssumeDistinctThreads, ref Expr AssumeThreadIdsInRange, IToken tok, String dimension)
+ private void EnsureDisabledThreadHasNoEffect(Implementation Impl)
{
- if (KernelHasId(dimension))
+ foreach (IdentifierExpr iex in Impl.Proc.Modifies)
{
- if (GetTypeOfId(dimension).Equals(Microsoft.Boogie.Type.GetBvType(32)))
+ // For some reason, this does not work well with maps
+ if (iex.Decl.TypedIdent.Type is MapType)
{
- KernelProcedure.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetTileSize(dimension)), ZeroBV(tok))));
- KernelProcedure.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetNumTiles(dimension)), ZeroBV(tok))));
- KernelProcedure.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GEQ", new IdentifierExpr(tok, GetTileId(dimension)), ZeroBV(tok))));
- KernelProcedure.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, GetTileId(dimension)), new IdentifierExpr(tok, GetNumTiles(dimension)))));
+ continue;
}
- else
+
+ Expr NoEffectExpr = Expr.Imp(
+ Expr.Not(new IdentifierExpr(iex.tok, new LocalVariable(iex.tok, new TypedIdent(iex.tok, "_P$" + GetThreadSuffix(iex.Name), Microsoft.Boogie.Type.Bool)))),
+ Expr.Eq(iex, new OldExpr(iex.tok, iex))
+ );
+
+ Impl.Proc.Ensures.Add(new Ensures(false,
+ NoEffectExpr
+ ));
+
+ AddInvariantToAllLoops(NoEffectExpr, Impl.StructuredStmts);
+
+ }
+
+ AddEnablednessInvariantToAllLoops(Impl.StructuredStmts);
+ }
+
+ private void AddEnablednessInvariantToAllLoops(StmtList stmtList)
+ {
+ foreach (BigBlock bb in stmtList.BigBlocks)
+ {
+ AddEnablednessInvariantToAllLoops(bb);
+ }
+ }
+
+ private void AddEnablednessInvariantToAllLoops(BigBlock bb)
+ {
+ if (bb.ec is WhileCmd)
+ {
+ WhileCmd wc = bb.ec as WhileCmd;
+ Debug.Assert(wc.Guard is NAryExpr);
+ Debug.Assert((wc.Guard as NAryExpr).Fun is BinaryOperator);
+ Debug.Assert((wc.Guard as NAryExpr).Args[0] is IdentifierExpr);
+ string LoopPredicate = ((wc.Guard as NAryExpr).Args[0] as IdentifierExpr).Name;
+ LoopPredicate = StripThreadIdentifier(LoopPredicate);
+
+ wc.Invariants.Add(
+ new AssertCmd(wc.tok,
+ Expr.Imp(
+ Expr.Not(new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, "_P$1", Microsoft.Boogie.Type.Bool)))),
+ Expr.Not(new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$1", Microsoft.Boogie.Type.Bool))))
+ )));
+
+ wc.Invariants.Add(
+ new AssertCmd(wc.tok,
+ Expr.Imp(
+ Expr.Not(new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, "_P$2", Microsoft.Boogie.Type.Bool)))),
+ Expr.Not(new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$2", Microsoft.Boogie.Type.Bool))))
+ )));
+
+ AddEnablednessInvariantToAllLoops(wc.Body);
+ }
+
+ }
+
+ private void AddInvariantToAllLoops(Expr Invariant, StmtList stmtList)
+ {
+ foreach (BigBlock bb in stmtList.BigBlocks)
+ {
+ AddInvariantToAllLoops(Invariant, bb);
+ }
+ }
+
+ private void AddInvariantToAllLoops(Expr Invariant, BigBlock bb)
+ {
+ if (bb.ec is WhileCmd)
+ {
+ WhileCmd wc = bb.ec as WhileCmd;
+ wc.Invariants.Add(new AssertCmd(wc.tok, Invariant));
+ AddInvariantToAllLoops(Invariant, wc.Body);
+ }
+ Debug.Assert(!(bb.ec is IfCmd));
+ }
+
+ private int GetThreadSuffix(string p)
+ {
+ return Int32.Parse(p.Substring(p.IndexOf("$") + 1, p.Length - (p.IndexOf("$") + 1)));
+ }
+
+ private void GeneratePreconditionsForDimension(ref Expr AssumeDistinctThreads, ref Expr AssumeThreadIdsInRange, IToken tok, String dimension)
+ {
+ if (KernelHasId(dimension))
+ {
+ foreach (Declaration D in Program.TopLevelDeclarations)
{
- KernelProcedure.Requires.Add(new Requires(false, Expr.Gt(new IdentifierExpr(tok, GetTileSize(dimension)), Zero(tok))));
- KernelProcedure.Requires.Add(new Requires(false, Expr.Gt(new IdentifierExpr(tok, GetNumTiles(dimension)), Zero(tok))));
- KernelProcedure.Requires.Add(new Requires(false, Expr.Ge(new IdentifierExpr(tok, GetTileId(dimension)), Zero(tok))));
- KernelProcedure.Requires.Add(new Requires(false, Expr.Lt(new IdentifierExpr(tok, GetTileId(dimension)), new IdentifierExpr(tok, GetNumTiles(dimension)))));
+ if (!(D is Procedure))
+ {
+ continue;
+ }
+ Procedure Proc = D as Procedure;
+ if (QKeyValue.FindIntAttribute(Proc.Attributes, "inline", -1) == 1)
+ {
+ continue;
+ }
+
+ if (GetTypeOfId(dimension).Equals(Microsoft.Boogie.Type.GetBvType(32)))
+ {
+ Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetTileSize(dimension)), ZeroBV(tok))));
+ Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetNumTiles(dimension)), ZeroBV(tok))));
+ Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GEQ", new IdentifierExpr(tok, GetTileId(dimension)), ZeroBV(tok))));
+ Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, GetTileId(dimension)), new IdentifierExpr(tok, GetNumTiles(dimension)))));
+ }
+ else
+ {
+ Proc.Requires.Add(new Requires(false, Expr.Gt(new IdentifierExpr(tok, GetTileSize(dimension)), Zero(tok))));
+ Proc.Requires.Add(new Requires(false, Expr.Gt(new IdentifierExpr(tok, GetNumTiles(dimension)), Zero(tok))));
+ Proc.Requires.Add(new Requires(false, Expr.Ge(new IdentifierExpr(tok, GetTileId(dimension)), Zero(tok))));
+ Proc.Requires.Add(new Requires(false, Expr.Lt(new IdentifierExpr(tok, GetTileId(dimension)), new IdentifierExpr(tok, GetNumTiles(dimension)))));
+ }
}
+
Expr AssumeThreadsDistinctInDimension =
Expr.Neq(
new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)),
@@ -1130,7 +1257,10 @@ namespace GPUVerify List<BigBlock> returnbigblocks = new List<BigBlock>();
returnbigblocks.Add(new BigBlock(tok, "__Disabled", new CmdSeq(), null, new ReturnCmd(tok)));
StmtList returnstatement = new StmtList(returnbigblocks, BarrierProcedure.tok);
- checkNonDivergence.ec = new IfCmd(tok, Expr.And(Expr.Not(P1), Expr.Not(P2)), returnstatement, null, null);
+ // We make this an "Or", not an "And", because "And" is implied by the assertion that the variables
+ // are equal, together with the "Or". The weaker "Or" ensures that many auxiliary assertions will not
+ // fail if divergence has not been proved.
+ checkNonDivergence.ec = new IfCmd(tok, Expr.Or(Expr.Not(P1), Expr.Not(P2)), returnstatement, null, null);
}
bigblocks.Add(RaceInstrumenter.MakeRaceCheckingStatements(tok));
@@ -1152,6 +1282,8 @@ namespace GPUVerify BarrierImplementation.AddAttribute("inline", new object[] { new LiteralExpr(tok, BigNum.FromInt(1)) });
BarrierProcedure.AddAttribute("inline", new object[] { new LiteralExpr(tok, BigNum.FromInt(1)) });
+ BarrierImplementation.Proc = BarrierProcedure;
+
Program.TopLevelDeclarations.Add(BarrierImplementation);
}
diff --git a/Source/GPUVerify/IRaceInstrumenter.cs b/Source/GPUVerify/IRaceInstrumenter.cs index 2540c9d7..9a1c0d8c 100644 --- a/Source/GPUVerify/IRaceInstrumenter.cs +++ b/Source/GPUVerify/IRaceInstrumenter.cs @@ -20,7 +20,7 @@ namespace GPUVerify BigBlock MakeRaceCheckingStatements(IToken tok);
- void CheckForRaces(IToken tok, BigBlock bb, Variable v);
+ void CheckForRaces(IToken tok, BigBlock bb, Variable v, bool ReadWriteOnly);
void AddRaceCheckingCandidateRequires(Procedure Proc);
diff --git a/Source/GPUVerify/NullRaceInstrumenter.cs b/Source/GPUVerify/NullRaceInstrumenter.cs index 3958a94e..a825a2eb 100644 --- a/Source/GPUVerify/NullRaceInstrumenter.cs +++ b/Source/GPUVerify/NullRaceInstrumenter.cs @@ -19,7 +19,7 @@ namespace GPUVerify }
- public void CheckForRaces(IToken tok, BigBlock bb, Variable v)
+ public void CheckForRaces(IToken tok, BigBlock bb, Variable v, bool ReadWriteOnly)
{
}
diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs index 237c155e..4f2f76be 100644 --- a/Source/GPUVerify/RaceInstrumenterBase.cs +++ b/Source/GPUVerify/RaceInstrumenterBase.cs @@ -244,6 +244,7 @@ namespace GPUVerify foreach (Cmd c in bb.simpleCmds)
{
+ result.simpleCmds.Add(c);
if (c is AssignCmd)
{
AssignCmd assign = c as AssignCmd;
@@ -313,7 +314,6 @@ namespace GPUVerify }
- result.simpleCmds.Add(c);
}
if (bb.ec is WhileCmd)
@@ -353,7 +353,7 @@ namespace GPUVerify {
foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
{
- CheckForRaces(tok, checkForRaces, v);
+ CheckForRaces(tok, checkForRaces, v, false);
}
}
@@ -372,7 +372,7 @@ namespace GPUVerify protected abstract void SetNoAccessOccurred(IToken tok, BigBlock bb, Variable v, string AccessType);
- public abstract void CheckForRaces(IToken tok, BigBlock bb, Variable v);
+ public abstract void CheckForRaces(IToken tok, BigBlock bb, Variable v, bool ReadWriteOnly);
protected void MakeLogAccessProcedureHeader(Variable v, string ReadOrWrite, out Variable XParameterVariable, out Variable YParameterVariable, out Variable ZParameterVariable, out Procedure LogReadOrWriteProcedure)
{
diff --git a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs index b3104609..e7e5854e 100644 --- a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs +++ b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs @@ -182,6 +182,8 @@ namespace GPUVerify Implementation LogReadOrWriteImplementation = new Implementation(v.tok, "_LOG_" + ReadOrWrite + "_" + v.Name, new TypeVariableSeq(), LogReadOrWriteProcedure.InParams, new VariableSeq(), new VariableSeq(), statements);
LogReadOrWriteImplementation.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });
+ LogReadOrWriteImplementation.Proc = LogReadOrWriteProcedure;
+
verifier.Program.TopLevelDeclarations.Add(LogReadOrWriteProcedure);
verifier.Program.TopLevelDeclarations.Add(LogReadOrWriteImplementation);
}
@@ -200,301 +202,168 @@ namespace GPUVerify }
bb.simpleCmds.Add(new HavocCmd(tok, VariablesToHavoc));
- if (v.TypedIdent.Type is MapType)
- {
- MapType mt = v.TypedIdent.Type as MapType;
- Debug.Assert(mt.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt.Arguments[0]));
-
- if (mt.Result is MapType)
- {
- MapType mt2 = mt.Result as MapType;
- Debug.Assert(mt2.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));
+ AddAssumeNoAccess(bb, v, AccessType);
- if (mt2.Result is MapType)
- {
- MapType mt3 = mt2.Arguments[0] as MapType;
- Debug.Assert(mt3.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));
- Debug.Assert(!(mt3.Result is MapType));
-
- Add3DAssumeNoAccess(tok, bb, v, AccessType, mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0]);
+ }
- }
- else
- {
- Add2DAssumeNoAccess(tok, bb, v, AccessType, mt.Arguments[0], mt2.Arguments[0]);
- }
- }
- else
- {
- Add1DAssumeNoAccess(tok, bb, v, AccessType, mt.Arguments[0]);
- }
+ public override void CheckForRaces(IToken tok, BigBlock bb, Variable v, bool ReadWriteOnly)
+ {
+ if (!ReadWriteOnly)
+ {
+ AddRaceCheck(bb, v, "WRITE", "WRITE");
}
- else
+ AddRaceCheck(bb, v, "READ", "WRITE");
+ if (!CommandLineOptions.Symmetry)
{
- Add0DAssumeNoAccess(tok, bb, v, AccessType);
+ AddRaceCheck(bb, v, "WRITE", "READ");
}
- }
- public override void CheckForRaces(IToken tok, BigBlock bb, Variable v)
- {
- if (v.TypedIdent.Type is MapType)
- {
- MapType mt = v.TypedIdent.Type as MapType;
- Debug.Assert(mt.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt.Arguments[0]));
- if (mt.Result is MapType)
- {
- MapType mt2 = mt.Result as MapType;
- Debug.Assert(mt2.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));
+ }
- if (mt2.Result is MapType)
- {
- MapType mt3 = mt2.Arguments[0] as MapType;
- Debug.Assert(mt3.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));
- Debug.Assert(!(mt3.Result is MapType));
- Add3DRaceCheck(tok, bb, v, "WRITE", "WRITE", mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0]);
- Add3DRaceCheck(tok, bb, v, "READ", "WRITE", mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0]);
- if (!CommandLineOptions.Symmetry)
- {
- Add3DRaceCheck(tok, bb, v, "WRITE", "READ", mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0]);
- }
+ private static Microsoft.Boogie.Type GetIndexType(Variable v, int index)
+ {
+ Debug.Assert(index == 1 || index == 2 || index == 3);
- }
- else
- {
-
- Add2DRaceCheck(tok, bb, v, "WRITE", "WRITE", mt.Arguments[0], mt2.Arguments[0]);
- Add2DRaceCheck(tok, bb, v, "READ", "WRITE", mt.Arguments[0], mt2.Arguments[0]);
- if (!CommandLineOptions.Symmetry)
- {
- Add2DRaceCheck(tok, bb, v, "WRITE", "READ", mt.Arguments[0], mt2.Arguments[0]);
- }
- }
- }
- else
- {
- Add1DRaceCheck(tok, bb, v, "WRITE", "WRITE", mt.Arguments[0]);
- Add1DRaceCheck(tok, bb, v, "READ", "WRITE", mt.Arguments[0]);
- if (!CommandLineOptions.Symmetry)
- {
- Add1DRaceCheck(tok, bb, v, "WRITE", "READ", mt.Arguments[0]);
- }
- }
- }
- else
+ Debug.Assert(v.TypedIdent.Type is MapType);
+ MapType mt = v.TypedIdent.Type as MapType;
+ Debug.Assert(mt.Arguments.Length == 1);
+ Debug.Assert(GPUVerifier.IsIntOrBv32(mt.Arguments[0]));
+
+ if (index == 1)
{
- Add0DRaceCheck(tok, bb, v, "WRITE", "WRITE");
- Add0DRaceCheck(tok, bb, v, "READ", "WRITE");
- if (!CommandLineOptions.Symmetry)
- {
- Add0DRaceCheck(tok, bb, v, "WRITE", "READ");
- }
+ return mt.Arguments[0];
}
- }
- private static void Add0DRaceCheck(IToken tok, BigBlock bb, Variable v, String Access1, String Access2)
- {
- bb.simpleCmds.Add(new AssertCmd(tok, Expr.Not(Expr.And(
- new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeAccessSetVariable(v, Access1))),
- new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeAccessSetVariable(v, Access2)))
- ))));
- }
+ Debug.Assert(mt.Result is MapType);
+ MapType mt2 = mt.Result as MapType;
+ Debug.Assert(mt2.Arguments.Length == 1);
+ Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));
- private static void Add1DRaceCheck(IToken tok, BigBlock bb, Variable v, String Access1, String Access2, Microsoft.Boogie.Type IndexType)
- {
- Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexType));
- bb.simpleCmds.Add(new AssertCmd(tok,
- new ForallExpr(tok, new VariableSeq(new Variable[] { DummyX }),
- Expr.Not(Expr.And(
- Expr.Select(new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeAccessSetVariable(v, Access1))), new Expr[] { new IdentifierExpr(tok, DummyX) }),
- Expr.Select(new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeAccessSetVariable(v, Access2))), new Expr[] { new IdentifierExpr(tok, DummyX) })
- ))
- )
- ));
- }
+ if (index == 2)
+ {
+ return mt2.Arguments[0];
+ }
- private static void Add2DRaceCheck(IToken tok, BigBlock bb, Variable v, String Access1, String Access2, Microsoft.Boogie.Type IndexTypeY, Microsoft.Boogie.Type IndexTypeX)
- {
- Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexTypeX));
- Variable DummyY = new LocalVariable(tok, new TypedIdent(tok, "__y", IndexTypeX));
- bb.simpleCmds.Add(new AssertCmd(tok,
- new ForallExpr(tok, new VariableSeq(new Variable[] { DummyY, DummyX }),
- Expr.Not(Expr.And(
- Expr.Select(
- Expr.Select(new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeAccessSetVariable(v, Access1))), new Expr[] { new IdentifierExpr(tok, DummyY) }),
- new Expr[] { new IdentifierExpr(tok, DummyX) }
- ),
- Expr.Select(
- Expr.Select(new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeAccessSetVariable(v, Access2))), new Expr[] { new IdentifierExpr(tok, DummyY) }),
- new Expr[] { new IdentifierExpr(tok, DummyX) }
- )
- ))
- )
- ));
- }
+ Debug.Assert(mt2.Result is MapType);
+ MapType mt3 = mt2.Arguments[0] as MapType;
+ Debug.Assert(mt3.Arguments.Length == 1);
+ Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));
+ Debug.Assert(!(mt3.Result is MapType));
- private static void Add3DRaceCheck(IToken tok, BigBlock bb, Variable v, String Access1, String Access2, Microsoft.Boogie.Type IndexTypeZ, Microsoft.Boogie.Type IndexTypeY, Microsoft.Boogie.Type IndexTypeX)
- {
- Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexTypeX));
- Variable DummyY = new LocalVariable(tok, new TypedIdent(tok, "__y", IndexTypeX));
- Variable DummyZ = new LocalVariable(tok, new TypedIdent(tok, "__z", IndexTypeX));
- bb.simpleCmds.Add(new AssertCmd(tok,
- new ForallExpr(tok, new VariableSeq(new Variable[] { DummyZ, DummyY, DummyX }),
- Expr.Not(Expr.And(
- Expr.Select(
- Expr.Select(
- Expr.Select(new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeAccessSetVariable(v, Access1))), new Expr[] { new IdentifierExpr(tok, DummyZ) }),
- new Expr[] { new IdentifierExpr(tok, DummyY) }
- ),
- new Expr[] { new IdentifierExpr(tok, DummyX) }
- ),
- Expr.Select(
- Expr.Select(
- Expr.Select(new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeAccessSetVariable(v, Access2))), new Expr[] { new IdentifierExpr(tok, DummyZ) }),
- new Expr[] { new IdentifierExpr(tok, DummyY) }
- ),
- new Expr[] { new IdentifierExpr(tok, DummyX) }
- )
- ))
- )
- ));
+ Debug.Assert(index == 3);
+ return mt3.Arguments[0];
}
-
- private static void Add0DAssumeNoAccess(IToken tok, BigBlock bb, Variable v, String AccessType)
+ private static void AddRaceCheck(BigBlock bb, Variable v, String Access1, String Access2)
{
- bb.simpleCmds.Add(new AssumeCmd(tok,
- NoAccess0DExpr(tok, v, AccessType, 1)
- ));
-
- if (!CommandLineOptions.Symmetry || !AccessType.Equals("READ"))
+ VariableSeq DummyVars1;
+ Expr SetExpr1 = AccessExpr(v, Access1, 1, out DummyVars1);
+
+ VariableSeq DummyVars2;
+ Expr SetExpr2 = AccessExpr(v, Access2, 2, out DummyVars2);
+
+ Debug.Assert(DummyVars1.Length == DummyVars2.Length);
+ for (int i = 0; i < DummyVars1.Length; i++)
{
- bb.simpleCmds.Add(new AssumeCmd(tok,
- NoAccess0DExpr(tok, v, AccessType, 2)
- ));
+ Debug.Assert(DummyVars1[i].Name.Equals(DummyVars2[i].Name));
}
- }
+ Expr AssertExpr = Expr.And(SetExpr1, SetExpr2);
- private static void Add1DAssumeNoAccess(IToken tok, BigBlock bb, Variable v, String AccessType, Microsoft.Boogie.Type IndexTypeX)
- {
- Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexTypeX));
- bb.simpleCmds.Add(new AssumeCmd(tok,
- NoAccess1DExpr(tok, v, AccessType, IndexTypeX, 1)
- ));
+ if (Access1.Equals("WRITE") && Access2.Equals("WRITE") && !CommandLineOptions.FullAbstraction)
+ {
+ VariableSeq DummyVarsAccess1;
+ VariableSeq DummyVarsAccess2;
+ Expr IndexExpr1 = QuantifiedIndexExpr(v, new VariableDualiser(1).VisitVariable(v.Clone() as Variable), out DummyVarsAccess1);
+ Expr IndexExpr2 = QuantifiedIndexExpr(v, new VariableDualiser(2).VisitVariable(v.Clone() as Variable), out DummyVarsAccess2);
+ Debug.Assert(DummyVarsAccess1.Length == DummyVarsAccess2.Length);
+ Debug.Assert(DummyVars1.Length == DummyVarsAccess1.Length);
+ for (int i = 0; i < DummyVars1.Length; i++)
+ {
+ Debug.Assert(DummyVarsAccess1[i].Name.Equals(DummyVarsAccess2[i].Name));
+ Debug.Assert(DummyVars1[i].Name.Equals(DummyVarsAccess1[i].Name));
+ }
+ AssertExpr = Expr.And(AssertExpr, Expr.Neq(IndexExpr1, IndexExpr2));
+ }
- if (!CommandLineOptions.Symmetry || !AccessType.Equals("READ"))
+ AssertExpr = Expr.Not(AssertExpr);
+ if (DummyVars1.Length > 0)
{
- bb.simpleCmds.Add(new AssumeCmd(tok,
- NoAccess1DExpr(tok, v, AccessType, IndexTypeX, 2)
- ));
+ AssertExpr = new ForallExpr(v.tok, DummyVars1, AssertExpr);
}
- }
+ bb.simpleCmds.Add(new AssertCmd(v.tok, AssertExpr));
+ }
- private static void Add2DAssumeNoAccess(IToken tok, BigBlock bb, Variable v, String AccessType, Microsoft.Boogie.Type IndexTypeY, Microsoft.Boogie.Type IndexTypeX)
+ private static void SetNameDeep(IdentifierExpr e, string name)
{
- Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexTypeX));
- Variable DummyY = new LocalVariable(tok, new TypedIdent(tok, "__y", IndexTypeX));
- bb.simpleCmds.Add(new AssumeCmd(tok,
- NoAccess2DExpr(tok, v, AccessType, IndexTypeY, IndexTypeX, 1)
- ));
-
- if (!CommandLineOptions.Symmetry || !AccessType.Equals("READ"))
- {
- bb.simpleCmds.Add(new AssumeCmd(tok,
- NoAccess2DExpr(tok, v, AccessType, IndexTypeY, IndexTypeX, 2)
- ));
- }
+ e.Name = e.Decl.Name = e.Decl.TypedIdent.Name = name;
}
+ private static LocalVariable MakeDummy(Variable v, int index)
+ {
+ return new LocalVariable(v.tok, new TypedIdent(v.tok, "__dummy", GetIndexType(v, index)));
+ }
- private static void Add3DAssumeNoAccess(IToken tok, BigBlock bb, Variable v, String AccessType, Microsoft.Boogie.Type IndexTypeZ, Microsoft.Boogie.Type IndexTypeY, Microsoft.Boogie.Type IndexTypeX)
+ private static void AddAssumeNoAccess(BigBlock bb, Variable v, String AccessType)
{
- bb.simpleCmds.Add(new AssumeCmd(tok,
- NoAccess3DExpr(tok, v, AccessType, IndexTypeZ, IndexTypeY, IndexTypeX, 1)
- ));
+ bb.simpleCmds.Add(new AssumeCmd(v.tok, NoAccessExpr(v, AccessType, 1)));
if (!CommandLineOptions.Symmetry || !AccessType.Equals("READ"))
{
- bb.simpleCmds.Add(new AssumeCmd(tok,
- NoAccess3DExpr(tok, v, AccessType, IndexTypeZ, IndexTypeY, IndexTypeX, 2)
- ));
+ bb.simpleCmds.Add(new AssumeCmd(v.tok, NoAccessExpr(v, AccessType, 2)));
}
}
- private static Expr NoAccess3DExpr(IToken tok, Variable v, String AccessType, Microsoft.Boogie.Type IndexTypeZ, Microsoft.Boogie.Type IndexTypeY, Microsoft.Boogie.Type IndexTypeX, int Thread)
+ private static Expr NoAccessExpr(Variable v, String AccessType, int Thread)
{
- Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexTypeX));
- Variable DummyY = new LocalVariable(tok, new TypedIdent(tok, "__y", IndexTypeY));
- Variable DummyZ = new LocalVariable(tok, new TypedIdent(tok, "__z", IndexTypeZ));
- return new ForallExpr(tok, new VariableSeq(new Variable[] { DummyZ, DummyY, DummyX }),
- Expr.Not(
- Expr.Select(
- Expr.Select(
- Expr.Select(new IdentifierExpr(tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, AccessType))), new Expr[] { new IdentifierExpr(tok, DummyZ) }),
- new Expr[] { new IdentifierExpr(tok, DummyY) }
- ),
- new Expr[] { new IdentifierExpr(tok, DummyX) }
- )
- )
- )
- ;
- }
+ VariableSeq DummyVars;
+ Expr result = AccessExpr(v, AccessType, Thread, out DummyVars);
- private static Expr NoAccess2DExpr(IToken tok, Variable v, String AccessType, Microsoft.Boogie.Type IndexTypeY, Microsoft.Boogie.Type IndexTypeX, int Thread)
- {
- Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexTypeX));
- Variable DummyY = new LocalVariable(tok, new TypedIdent(tok, "__y", IndexTypeY));
- return new ForallExpr(tok, new VariableSeq(new Variable[] { DummyY, DummyX }),
- Expr.Not(
- Expr.Select(
- Expr.Select(new IdentifierExpr(tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, AccessType))), new Expr[] { new IdentifierExpr(tok, DummyY) }),
- new Expr[] { new IdentifierExpr(tok, DummyX) }
- )
- )
- )
- ;
- }
+ result = Expr.Not(result);
+
+ if (DummyVars.Length > 0)
+ {
+ result = new ForallExpr(v.tok, DummyVars, result);
+ }
+ return result;
- private static Expr NoAccess1DExpr(IToken tok, Variable v, String AccessType, Microsoft.Boogie.Type IndexTypeX, int Thread)
- {
- Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexTypeX));
- return new ForallExpr(tok, new VariableSeq(new Variable[] { DummyX }),
- Expr.Not(
- Expr.Select(new IdentifierExpr(tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, AccessType))), new Expr[] { new IdentifierExpr(tok, DummyX) })
- )
- );
}
- private static Expr NoAccess0DExpr(IToken tok, Variable v, String AccessType, int Thread)
+ private static Expr AccessExpr(Variable v, String AccessType, int Thread, out VariableSeq DummyVars)
{
- return Expr.Not(new IdentifierExpr(tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, AccessType))));
+ return QuantifiedIndexExpr(v, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, AccessType)), out DummyVars);
}
-
- protected override void AddRequiresNoPendingAccess(Variable v)
+ private static Expr QuantifiedIndexExpr(Variable v, Variable AccessSetVariable, out VariableSeq DummyVars)
{
+ DummyVars = new VariableSeq();
+ Expr result = new IdentifierExpr(v.tok, AccessSetVariable);
+
if (v.TypedIdent.Type is MapType)
{
+ IdentifierExprSeq DummyIdentifierExprs = new IdentifierExprSeq();
MapType mt = v.TypedIdent.Type as MapType;
Debug.Assert(mt.Arguments.Length == 1);
Debug.Assert(GPUVerifier.IsIntOrBv32(mt.Arguments[0]));
+ DummyVars.Add(MakeDummy(v, 1));
+ DummyIdentifierExprs.Add(new IdentifierExpr(v.tok, DummyVars[0]));
+ result = Expr.Select(result, new Expr[] { DummyIdentifierExprs[0] });
+
if (mt.Result is MapType)
{
MapType mt2 = mt.Result as MapType;
Debug.Assert(mt2.Arguments.Length == 1);
Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));
+ DummyVars.Add(MakeDummy(v, 2));
+ DummyIdentifierExprs.Add(new IdentifierExpr(v.tok, DummyVars[1]));
+ result = Expr.Select(result, new Expr[] { DummyIdentifierExprs[1] });
+
if (mt2.Result is MapType)
{
MapType mt3 = mt2.Arguments[0] as MapType;
@@ -502,63 +371,42 @@ namespace GPUVerify Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));
Debug.Assert(!(mt3.Result is MapType));
- verifier.KernelProcedure.Requires.Add(new Requires(false,
- NoAccess3DExpr(v.tok, v, "WRITE", mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0], 1)));
- verifier.KernelProcedure.Requires.Add(new Requires(false,
- NoAccess3DExpr(v.tok, v, "WRITE", mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0], 2)));
- verifier.KernelProcedure.Requires.Add(new Requires(false,
- NoAccess3DExpr(v.tok, v, "READ", mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0], 1)));
- if (!CommandLineOptions.Symmetry)
- {
- verifier.KernelProcedure.Requires.Add(new Requires(false,
- NoAccess3DExpr(v.tok, v, "READ", mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0], 2)));
- }
-
+ DummyVars.Add(MakeDummy(v, 3));
+ DummyIdentifierExprs.Add(new IdentifierExpr(v.tok, DummyVars[2]));
+ result = Expr.Select(result, new Expr[] { DummyIdentifierExprs[2] });
+ SetNameDeep(DummyIdentifierExprs[0], "__z");
+ SetNameDeep(DummyIdentifierExprs[1], "__y");
+ SetNameDeep(DummyIdentifierExprs[2], "__x");
}
else
{
- verifier.KernelProcedure.Requires.Add(new Requires(false,
- NoAccess2DExpr(v.tok, v, "WRITE", mt.Arguments[0], mt2.Arguments[0], 1)));
- verifier.KernelProcedure.Requires.Add(new Requires(false,
- NoAccess2DExpr(v.tok, v, "WRITE", mt.Arguments[0], mt2.Arguments[0], 2)));
- verifier.KernelProcedure.Requires.Add(new Requires(false,
- NoAccess2DExpr(v.tok, v, "READ", mt.Arguments[0], mt2.Arguments[0], 1)));
- if(!CommandLineOptions.Symmetry)
- {
- verifier.KernelProcedure.Requires.Add(new Requires(false,
- NoAccess2DExpr(v.tok, v, "READ", mt.Arguments[0], mt2.Arguments[0], 2)));
- }
+ SetNameDeep(DummyIdentifierExprs[0], "__y");
+ SetNameDeep(DummyIdentifierExprs[1], "__x");
}
}
else
{
- verifier.KernelProcedure.Requires.Add(new Requires(false,
- NoAccess1DExpr(v.tok, v, "WRITE", mt.Arguments[0], 1)));
- verifier.KernelProcedure.Requires.Add(new Requires(false,
- NoAccess1DExpr(v.tok, v, "WRITE", mt.Arguments[0], 2)));
- verifier.KernelProcedure.Requires.Add(new Requires(false,
- NoAccess1DExpr(v.tok, v, "READ", mt.Arguments[0], 1)));
- if(!CommandLineOptions.Symmetry)
- {
- verifier.KernelProcedure.Requires.Add(new Requires(false,
- NoAccess1DExpr(v.tok, v, "READ", mt.Arguments[0], 2)));
- }
+ SetNameDeep(DummyIdentifierExprs[0], "__x");
}
}
- else
+ return result;
+ }
+
+ private static Expr NoAccess0DExpr(IToken tok, Variable v, String AccessType, int Thread)
+ {
+ return Expr.Not(new IdentifierExpr(tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, AccessType))));
+ }
+
+
+ protected override void AddRequiresNoPendingAccess(Variable v)
+ {
+ verifier.KernelProcedure.Requires.Add(new Requires(false, NoAccessExpr(v, "WRITE", 1)));
+ verifier.KernelProcedure.Requires.Add(new Requires(false, NoAccessExpr(v, "WRITE", 2)));
+ verifier.KernelProcedure.Requires.Add(new Requires(false, NoAccessExpr(v, "READ", 1)));
+ if(!CommandLineOptions.Symmetry)
{
- verifier.KernelProcedure.Requires.Add(new Requires(false,
- NoAccess0DExpr(v.tok, v, "WRITE", 1)));
- verifier.KernelProcedure.Requires.Add(new Requires(false,
- NoAccess0DExpr(v.tok, v, "WRITE", 2)));
- verifier.KernelProcedure.Requires.Add(new Requires(false,
- NoAccess0DExpr(v.tok, v, "READ", 1)));
- if(!CommandLineOptions.Symmetry)
- {
- verifier.KernelProcedure.Requires.Add(new Requires(false,
- NoAccess0DExpr(v.tok, v, "READ", 2)));
- }
+ verifier.KernelProcedure.Requires.Add(new Requires(false, NoAccessExpr(v, "READ", 2)));
}
}
@@ -569,44 +417,7 @@ namespace GPUVerify protected override Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwoString)
{
- int OneOrTwo = Int32.Parse(OneOrTwoString);
- Expr expr = null;
-
- if (v.TypedIdent.Type is MapType)
- {
- MapType mt = v.TypedIdent.Type as MapType;
- Debug.Assert(mt.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt.Arguments[0]));
-
- if (mt.Result is MapType)
- {
- MapType mt2 = mt.Result as MapType;
- Debug.Assert(mt2.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));
-
- if (mt2.Result is MapType)
- {
- MapType mt3 = mt2.Arguments[0] as MapType;
- Debug.Assert(mt3.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));
- Debug.Assert(!(mt3.Result is MapType));
- expr = NoAccess3DExpr(v.tok, v, ReadOrWrite, mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0], OneOrTwo);
- }
- else
- {
- expr = NoAccess2DExpr(v.tok, v, ReadOrWrite, mt.Arguments[0], mt2.Arguments[0], OneOrTwo);
- }
- }
- else
- {
- expr = NoAccess1DExpr(v.tok, v, ReadOrWrite, mt.Arguments[0], OneOrTwo);
- }
- }
- else
- {
- expr = NoAccess0DExpr(v.tok, v, ReadOrWrite, OneOrTwo);
- }
- return expr;
+ return NoAccessExpr(v, ReadOrWrite, Int32.Parse(OneOrTwoString));
}
@@ -623,131 +434,48 @@ namespace GPUVerify private Expr AccessOnlyAtThreadId(Variable v, string ReadOrWrite, int Thread)
{
- Expr expr = null;
+ VariableSeq Dummies;
+ Expr Access = AccessExpr(v, ReadOrWrite, Thread, out Dummies);
- if (v.TypedIdent.Type is MapType)
+ if (Dummies.Length == 0)
{
- MapType mt = v.TypedIdent.Type as MapType;
- Debug.Assert(mt.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt.Arguments[0]));
-
- if (mt.Result is MapType)
- {
- MapType mt2 = mt.Result as MapType;
- Debug.Assert(mt2.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));
-
- if (mt2.Result is MapType)
- {
- MapType mt3 = mt2.Arguments[0] as MapType;
- Debug.Assert(mt3.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));
- Debug.Assert(!(mt3.Result is MapType));
+ return null;
+ }
- if (verifier.KernelHasIdZ() && mt.Arguments[0].Equals(verifier.GetTypeOfIdZ()) &&
- mt2.Arguments[0].Equals(verifier.GetTypeOfIdY()) &&
- mt3.Arguments[0].Equals(verifier.GetTypeOfIdX()))
- {
- expr = No3DAccessExceptAtThreadId(v, ReadOrWrite, Thread);
- }
+ Expr ImplicationLhs;
- }
- else
- {
- if (verifier.KernelHasIdY() && mt.Arguments[0].Equals(verifier.GetTypeOfIdY()) &&
- mt2.Arguments[0].Equals(verifier.GetTypeOfIdX()))
- {
- expr = No2DAccessExceptAtThreadId(v, ReadOrWrite, Thread);
- }
- }
- }
- else
+ if (Dummies.Length == 1)
+ {
+ ImplicationLhs = Expr.Neq(new IdentifierExpr(v.tok, Dummies[0]), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread)));
+ }
+ else if (Dummies.Length == 2)
+ {
+ if (!verifier.KernelHasIdY())
{
- if (mt.Arguments[0].Equals(verifier.GetTypeOfIdX()))
- {
- expr = No1DAccessExceptAtThreadId(v, ReadOrWrite, Thread);
- }
+ return null;
}
+ ImplicationLhs = Expr.Or(
+ Expr.Neq(new IdentifierExpr(v.tok, Dummies[1]), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))),
+ Expr.Neq(new IdentifierExpr(v.tok, Dummies[0]), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Y", Thread)))
+ );
}
- return expr;
- }
-
- private Expr No1DAccessExceptAtThreadId(Variable v, string ReadOrWrite, int Thread)
- {
- Variable DummyX = new LocalVariable(v.tok, new TypedIdent(v.tok, "__x", verifier.GetTypeOfIdX()));
-
- return new ForallExpr(v.tok,
- new VariableSeq(new Variable[] { DummyX }),
- Expr.Imp(
- Expr.Neq(new IdentifierExpr(v.tok, DummyX), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))),
- Expr.Not(
- Expr.Select(
- new IdentifierExpr(v.tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, ReadOrWrite))),
- new IdentifierExpr(v.tok, DummyX)
- )
- )
- )
- );
- }
-
-
- private Expr No2DAccessExceptAtThreadId(Variable v, string ReadOrWrite, int Thread)
- {
- Variable DummyX = new LocalVariable(v.tok, new TypedIdent(v.tok, "__x", verifier.GetTypeOfIdX()));
- Variable DummyY = new LocalVariable(v.tok, new TypedIdent(v.tok, "__y", verifier.GetTypeOfIdY()));
-
- return new ForallExpr(v.tok,
- new VariableSeq(new Variable[] { DummyY, DummyX }),
- Expr.Imp(
- Expr.Or(
- Expr.Neq(new IdentifierExpr(v.tok, DummyX), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))),
- Expr.Neq(new IdentifierExpr(v.tok, DummyY), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Y", Thread)))
- ),
-
- Expr.Not(
- Expr.Select(
- Expr.Select(
- new IdentifierExpr(v.tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, ReadOrWrite))),
- new IdentifierExpr(v.tok, DummyY)
- ),
- new IdentifierExpr(v.tok, DummyX)
- )
- )
- )
- );
- }
-
- private Expr No3DAccessExceptAtThreadId(Variable v, string ReadOrWrite, int Thread)
- {
- Variable DummyX = new LocalVariable(v.tok, new TypedIdent(v.tok, "__x", verifier.GetTypeOfIdX()));
- Variable DummyY = new LocalVariable(v.tok, new TypedIdent(v.tok, "__y", verifier.GetTypeOfIdY()));
- Variable DummyZ = new LocalVariable(v.tok, new TypedIdent(v.tok, "__z", verifier.GetTypeOfIdY()));
-
- return new ForallExpr(v.tok,
- new VariableSeq(new Variable[] { DummyY, DummyX }),
- Expr.Imp(
+ else
+ {
+ Debug.Assert(Dummies.Length == 3);
+ if (!verifier.KernelHasIdZ())
+ {
+ return null;
+ }
+ ImplicationLhs = Expr.Or(
Expr.Or(
- Expr.Or(
- Expr.Neq(new IdentifierExpr(v.tok, DummyX), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))),
- Expr.Neq(new IdentifierExpr(v.tok, DummyY), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Y", Thread)))
- ),
- Expr.Neq(new IdentifierExpr(v.tok, DummyZ), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Z", Thread)))
+ Expr.Neq(new IdentifierExpr(v.tok, Dummies[2]), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))),
+ Expr.Neq(new IdentifierExpr(v.tok, Dummies[1]), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Y", Thread)))
),
+ Expr.Neq(new IdentifierExpr(v.tok, Dummies[0]), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Z", Thread)))
+ );
+ }
- Expr.Not(
- Expr.Select(
- Expr.Select(
- Expr.Select(
- new IdentifierExpr(v.tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, ReadOrWrite))),
- new IdentifierExpr(v.tok, DummyZ)
- ),
- new IdentifierExpr(v.tok, DummyY)
- ),
- new IdentifierExpr(v.tok, DummyX)
- )
- )
- )
- );
+ return new ForallExpr(v.tok, Dummies, Expr.Imp(ImplicationLhs, Expr.Not(Access)));
}
protected override void AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread)
diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index 3cb27e14..b0c8fabf 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -18,6 +18,7 @@ using VC; namespace Microsoft.Boogie.Houdini {
public class HoudiniSession {
+ public static double proverTime = 0;
private string descriptiveName;
private VCExpr conjecture;
private ProverInterface.ErrorHandler handler;
@@ -49,10 +50,13 @@ namespace Microsoft.Boogie.Houdini { public ProverInterface.Outcome Verify(Checker checker, VCExpr axiom, out List<Counterexample> errors) {
collector.examples.Clear();
VCExpr vc = checker.VCExprGen.Implies(axiom, conjecture);
+
+ DateTime now = DateTime.Now;
checker.BeginCheck(descriptiveName, vc, handler);
WaitHandle.WaitAny(new WaitHandle[] { checker.ProverDone });
-
ProverInterface.Outcome proverOutcome = checker.ReadOutcome();
+ proverTime += (DateTime.Now - now).TotalSeconds;
+
if (proverOutcome == ProverInterface.Outcome.Invalid) {
Contract.Assume(collector.examples != null);
if (collector.examples.Count == 0) {
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 06fd5502..27b8d05f 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -686,7 +686,7 @@ namespace Microsoft.Boogie.Houdini { this.NotifyStart(program, houdiniConstants.Keys.Count);
while (current.WorkList.Count > 0) {
- System.GC.Collect();
+ //System.GC.Collect();
this.NotifyIteration();
VCExpr axiom = BuildAxiom(current.Assignment);
@@ -722,7 +722,7 @@ namespace Microsoft.Boogie.Houdini { while (current.WorkList.Count > 0) {
bool exceptional = false;
- System.GC.Collect();
+ //System.GC.Collect();
this.NotifyIteration();
current.Implementation = current.WorkList.Peek();
@@ -763,7 +763,7 @@ namespace Microsoft.Boogie.Houdini { while (current.WorkList.Count > 0) {
bool exceptional = false;
- System.GC.Collect();
+ //System.GC.Collect();
this.NotifyIteration();
current.Implementation = current.WorkList.Peek();
@@ -960,7 +960,7 @@ namespace Microsoft.Boogie.Houdini { do {
if (pastFirstIter) {
- System.GC.Collect();
+ //System.GC.Collect();
this.NotifyIteration();
}
@@ -1027,7 +1027,7 @@ namespace Microsoft.Boogie.Houdini { outcome = ProverInterface.Outcome.Undetermined;
if (pastFirstIter) {
- System.GC.Collect();
+ //System.GC.Collect();
this.NotifyIteration();
}
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 0bcbad35..924d5a3b 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -27,6 +27,8 @@ namespace VC public static Dictionary<string, int> callTree = null;
public int numInlined = 0;
public readonly static string recordProcName = "boogie_si_record";
+ private bool useSummary;
+ private SummaryComputation summaryComputation;
[ContractInvariantMethod]
void ObjectInvariant()
@@ -47,6 +49,7 @@ namespace VC this.GenerateVCsForStratifiedInlining(program);
PersistCallTree = false;
+ useSummary = false;
}
public static RECORD_TYPES getRecordType(Bpl.Type type)
@@ -305,6 +308,236 @@ namespace VC return -1;
}
+ public class SummaryComputation
+ {
+ // The verification state
+ VerificationState vState;
+ // The call tree
+ FCallHandler calls;
+ // Fully-inlined guys we have already queried
+ HashSet<string> fullyInlinedCache;
+
+ // The summary: boolean guards that are true
+ HashSet<VCExprVar> trueSummaryConst;
+ HashSet<VCExprVar> trueSummaryConstUndeBound;
+
+ // Compute summaries under recursion bound or not?
+ bool ComputeUnderBound;
+
+ public SummaryComputation(VerificationState vState, bool ComputeUnderBound)
+ {
+ this.vState = vState;
+ this.calls = vState.calls;
+ this.fullyInlinedCache = new HashSet<string>();
+ this.trueSummaryConst = new HashSet<VCExprVar>();
+ this.trueSummaryConstUndeBound = new HashSet<VCExprVar>();
+ this.ComputeUnderBound = ComputeUnderBound;
+ }
+
+ public void boundChanged()
+ {
+ if (ComputeUnderBound)
+ {
+ var s = "";
+ trueSummaryConstUndeBound.Iter(v => s = s + v.ToString() + ",");
+ Console.WriteLine("Clearing summaries: {{0}}", s);
+
+ // start from scratch
+ trueSummaryConst.ExceptWith(trueSummaryConstUndeBound);
+ trueSummaryConstUndeBound = new HashSet<VCExprVar>();
+ }
+ }
+
+ public void compute(HashSet<int> goodCandidates, int bound)
+ {
+ // Find all nodes that have children only in goodCandidates
+ var overApproxNodes = FindNodes(calls.candidateParent, calls.currCandidates, goodCandidates);
+ overApproxNodes.IntersectWith(calls.summaryCandidates.Keys);
+
+ var roots = FindTopMostAncestors(calls.candidateParent, overApproxNodes);
+ var checker2 = vState.checker2;
+
+ checker2.Push();
+
+ // candidates to block
+ var block = new HashSet<int>();
+ var usesBound = new HashSet<int>();
+ if (ComputeUnderBound)
+ {
+ calls.currCandidates.Iter(id => { if (calls.getRecursionBound(id) > bound) block.Add(id); });
+ foreach (var id in block)
+ {
+ checker2.AddAxiom(calls.getFalseExpr(id));
+ var curr = id;
+ usesBound.Add(id);
+ while (curr != 0)
+ {
+ curr = calls.candidateParent[curr];
+ usesBound.Add(curr);
+ }
+ }
+
+ }
+
+ // Iterate over the roots
+ foreach (var id in roots)
+ {
+ // inline procedures in post order
+ var post = getPostOrder(calls.candidateParent, id);
+
+ vState.checker2.Push();
+ foreach (var cid in post)
+ {
+ if (goodCandidates.Contains(cid)) continue;
+
+ checker2.AddAxiom(calls.id2VC[cid]);
+ if (!overApproxNodes.Contains(cid)) continue;
+ checker2.AddAxiom(calls.id2ControlVar[cid]);
+
+ foreach (var tup in calls.summaryCandidates[cid])
+ {
+ if (trueSummaryConst.Contains(tup.Item1)) continue;
+
+ //Console.WriteLine("Going to try ({0} ==> {1}) on {2}", tup.Item1, tup.Item2, id);
+ //Console.WriteLine("Call expr: {0}", calls.id2Candidate[id]);
+
+ // It is OK to assume the summary while trying to prove it
+ var summary = getSummary(tup.Item1);
+
+ checker2.Push();
+ checker2.AddAxiom(summary);
+ checker2.AddAxiom(checker2.underlyingChecker.VCExprGen.Not(tup.Item2));
+ var outcome = checker2.CheckVC();
+ checker2.Pop();
+ if (outcome == Outcome.Correct)
+ {
+ Console.WriteLine("Found summary: {0}", tup.Item1);
+ trueSummaryConst.Add(tup.Item1);
+ if (usesBound.Contains(cid)) trueSummaryConstUndeBound.Add(tup.Item1);
+ }
+ }
+ }
+ checker2.Pop();
+ }
+ checker2.Pop();
+ }
+
+
+ public VCExpr getSummary()
+ {
+ return getSummary(new HashSet<VCExprVar>());
+ }
+
+ public VCExpr getSummary(params VCExprVar[] p)
+ {
+ var s = new HashSet<VCExprVar>();
+ p.Iter(v => s.Add(v));
+ return getSummary(s);
+ }
+
+ public VCExpr getSummary(HashSet<VCExprVar> extraToSet)
+ {
+ if (calls.allSummaryConst.Count == 0) return null;
+ // TODO: does it matter which checker we use here?
+ var Gen = vState.checker.underlyingChecker.VCExprGen;
+
+ var ret = VCExpressionGenerator.True;
+ foreach (var c in calls.allSummaryConst)
+ {
+ if (trueSummaryConst.Contains(c) || extraToSet.Contains(c))
+ {
+ ret = Gen.And(ret, c);
+ }
+ else
+ {
+ ret = Gen.And(ret, Gen.Not(c));
+ }
+ }
+ return ret;
+ }
+
+ // Return a subset of nodes such that all other nodes are their decendent
+ private HashSet<int> FindTopMostAncestors(Dictionary<int, int> parents, HashSet<int> nodes)
+ {
+ var ret = new HashSet<int>();
+ //var ancestorFound = new HashSet<int>();
+ foreach (var n in nodes)
+ {
+ var ancestor = n;
+ var curr = n;
+ while (curr != 0)
+ {
+ curr = parents[curr];
+ if (nodes.Contains(curr)) ancestor = curr;
+ }
+ ret.Add(ancestor);
+ }
+ return ret;
+ }
+
+ // Returns the set of candidates whose child leaves are all "good". Remove fully inlined ones.
+ HashSet<int> FindNodes(Dictionary<int, int> parents, HashSet<int> allLeaves,
+ HashSet<int> goodLeaves)
+ {
+ var ret = new HashSet<int>();
+ var leaves = new Dictionary<int, HashSet<int>>();
+ leaves.Add(0, new HashSet<int>());
+ parents.Keys.Iter(n => leaves.Add(n, new HashSet<int>()));
+ allLeaves.Iter(l => leaves[l].Add(l));
+
+ foreach (var l in allLeaves)
+ {
+ var curr = l;
+ leaves[curr].Add(l);
+ while (parents.ContainsKey(curr))
+ {
+ curr = parents[curr];
+ leaves[curr].Add(l);
+ }
+ }
+
+ foreach (var kvp in leaves)
+ {
+ if (kvp.Value.Count == 0)
+ {
+ var proc = calls.getProc(kvp.Key);
+ if (fullyInlinedCache.Contains(proc)) continue;
+ else
+ {
+ ret.Add(kvp.Key);
+ fullyInlinedCache.Add(proc);
+ }
+ }
+
+ if (kvp.Value.IsSubsetOf(goodLeaves))
+ {
+ ret.Add(kvp.Key);
+ }
+ }
+
+ return ret;
+ }
+
+
+ // returns children of root in post order
+ static List<int> getPostOrder(Dictionary<int, int> parents, int root)
+ {
+ var children = new Dictionary<int, HashSet<int>>();
+ foreach (var id in parents.Keys) children.Add(id, new HashSet<int>());
+ children.Add(0, new HashSet<int>());
+ foreach (var kvp in parents) children[kvp.Value].Add(kvp.Key);
+ return getPostOrder(children, root);
+ }
+ static List<int> getPostOrder(Dictionary<int, HashSet<int>> children, int root)
+ {
+ var ret = new List<int>();
+ foreach (var ch in children[root]) ret.AddRange(getPostOrder(children, ch));
+ ret.Add(root);
+ return ret;
+ }
+
+ }
+
public class BoundingVCMutator : MutatingVCExprVisitor<bool> {
StratifiedCheckerInterface checker;
string implName;
@@ -597,7 +830,6 @@ namespace VC public void addMain()
{
- if (coverageProcess == null) return;
newNodes.Add(0);
foreach (var n in calls.currCandidates)
{
@@ -1053,9 +1285,11 @@ namespace VC return checker.numQueries;
}
}
+ // For making summary queries on the side
+ public StratifiedCheckerInterface checker2;
public VerificationState(VCExpr vcMain, FCallHandler calls,
- ProverInterface.ErrorHandler reporter, Checker checker)
+ ProverInterface.ErrorHandler reporter, Checker checker, Checker checker2)
{
this.vcMain = vcMain;
this.calls = calls;
@@ -1063,13 +1297,18 @@ namespace VC if (checker.TheoremProver is ApiProverInterface)
{
this.checker = new ApiChecker(vcMain, reporter , checker);
+ if(checker2 != null)
+ this.checker2 = new ApiChecker(VCExpressionGenerator.False, new EmptyErrorHandler(), checker2);
}
else
{
this.checker = new NormalChecker(vcMain, reporter, checker);
+ if(checker2 != null)
+ this.checker2 = new NormalChecker(VCExpressionGenerator.False, new EmptyErrorHandler(), checker2);
}
vcSize = 0;
expansionCount = 0;
+
}
public void updateMainVC(VCExpr vcMain)
@@ -1121,7 +1360,7 @@ namespace VC vcMain = calls.Mutate(vcMain, true);
// Put all of the necessary state into one object
- var vState = new VerificationState(vcMain, calls, new EmptyErrorHandler(), checker);
+ var vState = new VerificationState(vcMain, calls, new EmptyErrorHandler(), checker, null);
vState.coverageManager = null;
// We'll restore the original state of the theorem prover at the end
@@ -1300,6 +1539,7 @@ namespace VC public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback)
{
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+ var computeUnderBound = true;
#region stratified inlining options
// This flag control the nature of queries made by Stratified VerifyImplementation
@@ -1326,13 +1566,30 @@ namespace VC incrementalSearch = false;
createVConDemand = false;
break;
+ case 6:
+ incrementalSearch = true;
+ createVConDemand = true;
+ useSummary = true;
+ break;
+ case 7:
+ incrementalSearch = true;
+ createVConDemand = true;
+ useSummary = true;
+ computeUnderBound = false;
+ break;
}
#endregion
// Get the checker
Checker checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime); Contract.Assert(checker != null);
-
+ Checker checker2 = null;
+ if (useSummary)
+ {
+
+ checker2 = new Checker(this, program, "checker2.txt", true, CommandLineOptions.Clo.ProverKillTime);
+ }
+
// Record current time
var startTime = DateTime.Now;
@@ -1370,16 +1627,23 @@ namespace VC calls.setCurrProcAsMain();
vc = calls.Mutate(vc, true);
reporter.SetCandidateHandler(calls);
+ calls.id2VC.Add(0, vc);
+
+ // Identify summary candidates: Match ensure clauses with the appropriate call site
+ if (useSummary) calls.matchSummaries();
+
// create a process for displaying coverage information
var coverageManager = new CoverageGraphManager(calls);
coverageManager.addMain();
// Put all of the necessary state into one object
- var vState = new VerificationState(vc, calls, reporter, checker);
+ var vState = new VerificationState(vc, calls, reporter, checker, checker2);
vState.vcSize += SizeComputingVisitor.ComputeSize(vc);
vState.coverageManager = coverageManager;
-
+
+ if (useSummary) summaryComputation = new SummaryComputation(vState, computeUnderBound);
+
// We'll restore the original state of the theorem prover at the end
// of this procedure
vState.checker.Push();
@@ -1441,6 +1705,9 @@ namespace VC int iters = 0;
+ // for blocking candidates (and focussing on a counterexample)
+ var block = new HashSet<int>();
+
// Process tasks while not done. We're done when:
// case 1: (correct) We didn't find a bug (either an over-approx query was valid
// or we reached the recursion bound) and the task is "step"
@@ -1487,10 +1754,24 @@ namespace VC break;
}
+ VCExpr summary = null;
+ if (useSummary) summary = summaryComputation.getSummary();
+
+ if (useSummary && summary != null)
+ {
+ vState.checker.Push();
+ vState.checker.AddAxiom(summary);
+ }
+
// Stratified Step
- ret = stratifiedStep(bound, vState);
+ ret = stratifiedStep(bound, vState, block);
iters++;
+ if (useSummary && summary != null)
+ {
+ vState.checker.Pop();
+ }
+
// Sorry, out of luck (time/memory)
if (ret == Outcome.Inconclusive || ret == Outcome.OutOfMemory || ret == Outcome.TimedOut)
{
@@ -1507,27 +1788,46 @@ namespace VC }
else if (ret == Outcome.Correct)
{
- // Correct
- done = 1;
- coverageManager.reportCorrect();
+ if (block.Count == 0)
+ {
+ // Correct
+ done = 1;
+ coverageManager.reportCorrect();
+ }
+ else
+ {
+ Contract.Assert(useSummary);
+ // reset blocked and continue loop
+ block.Clear();
+ }
}
else if (ret == Outcome.ReachedBound)
{
- // Increment bound
- var minRecReached = CommandLineOptions.Clo.RecursionBound + 1;
- foreach (var id in calls.currCandidates)
+ if (block.Count == 0)
{
- var rb = calls.getRecursionBound(id);
- if (rb <= bound) continue;
- if (rb < minRecReached) minRecReached = rb;
- }
- bound = minRecReached;
+ // Increment bound
+ var minRecReached = CommandLineOptions.Clo.RecursionBound + 1;
+ foreach (var id in calls.currCandidates)
+ {
+ var rb = calls.getRecursionBound(id);
+ if (rb <= bound) continue;
+ if (rb < minRecReached) minRecReached = rb;
+ }
+ bound = minRecReached;
+ if (useSummary) summaryComputation.boundChanged();
- if (bound > CommandLineOptions.Clo.RecursionBound)
+ if (bound > CommandLineOptions.Clo.RecursionBound)
+ {
+ // Correct under bound
+ done = 1;
+ coverageManager.reportCorrect(bound);
+ }
+ }
+ else
{
- // Correct under bound
- done = 1;
- coverageManager.reportCorrect(bound);
+ Contract.Assert(useSummary);
+ // reset blocked and continue loop
+ block.Clear();
}
}
else
@@ -1535,6 +1835,12 @@ namespace VC // Do inlining
Debug.Assert(ret == Outcome.Errors && !reporter.underapproximationMode);
Contract.Assert(reporter.candidatesToExpand.Count != 0);
+ if (useSummary)
+ {
+ // compute candidates to block
+ block = new HashSet<int>(calls.currCandidates);
+ block.ExceptWith(reporter.candidatesToExpand);
+ }
#region expand call tree
@@ -1593,7 +1899,7 @@ namespace VC callTree.Add(calls.getPersistentId(id), 0);
}
}
-
+ if (checker2 != null) checker2.Close();
return ret;
}
@@ -1932,7 +2238,7 @@ namespace VC }
// A step of the stratified inlining algorithm: both under-approx and over-approx queries
- private Outcome stratifiedStep(int bound, VerificationState vState)
+ private Outcome stratifiedStep(int bound, VerificationState vState, HashSet<int> block)
{
Outcome ret;
List<int> unsatCore;
@@ -1959,7 +2265,6 @@ namespace VC assumptions.Add(calls.getFalseExpr(id));
ids.Add(id);
}
-
ret = checker.CheckAssumptions(assumptions, out unsatCore);
if (!CommandLineOptions.Clo.UseUnsatCoreForInlining) break;
if (ret != Outcome.Correct) break;
@@ -2016,8 +2321,18 @@ namespace VC {
if (calls.getRecursionBound(id) <= bound)
{
- //checker.TheoremProver.PushVCExpression(calls.getTrueExpr(id));
- allFalse = false;
+ if (block.Contains(id))
+ {
+ Contract.Assert(useSummary);
+ //checker.AddAxiom(calls.getFalseExpr(id));
+ assumptions.Add(calls.getFalseExpr(id));
+ allTrue = false;
+ }
+ else
+ {
+ //checker.TheoremProver.PushVCExpression(calls.getTrueExpr(id));
+ allFalse = false;
+ }
}
else
{
@@ -2053,6 +2368,14 @@ namespace VC return ret;
}
+ if (useSummary)
+ {
+ // Find the set of candidates with valid over-approximations
+ var assumeTrueCandidates = new HashSet<int>(vState.calls.currCandidates);
+ assumeTrueCandidates.ExceptWith(block);
+ summaryComputation.compute(assumeTrueCandidates, bound);
+ }
+
// Nothing more can be done with current recursion bound.
return Outcome.ReachedBound;
}
@@ -2148,10 +2471,12 @@ namespace VC calls.currInlineCount = id;
calls.setCurrProc(procName);
expansion = calls.Mutate(expansion, true);
- if(vState.coverageManager != null) vState.coverageManager.addRecentEdges(id);
-
+ if (useSummary) calls.matchSummaries();
+ vState.coverageManager.addRecentEdges(id);
+
//expansion = checker.VCExprGen.Eq(calls.id2ControlVar[id], expansion);
expansion = checker.VCExprGen.Implies(calls.id2ControlVar[id], expansion);
+ calls.id2VC.Add(id, expansion);
exprToPush = checker.VCExprGen.And(exprToPush, expansion);
}
@@ -2227,6 +2552,7 @@ namespace VC calls.currCandidates.Remove(id);
// Record the new set of candidates and rename absy labels
+
calls.currInlineCount = id;
calls.setCurrProc(procName);
expansion = calls.Mutate(expansion, true);
@@ -2321,6 +2647,7 @@ namespace VC public Dictionary<BoogieCallExpr/*!*/, VCExpr>/*!*/ recordExpr2Var;
public Dictionary<int, VCExprNAry/*!*/>/*!*/ id2Candidate;
public Dictionary<int, VCExprVar/*!*/>/*!*/ id2ControlVar;
+ public Dictionary<int, VCExpr> id2VC;
public Dictionary<string/*!*/, int>/*!*/ label2Id;
// Stores the candidate from which this one originated
public Dictionary<int, int> candidateParent;
@@ -2340,6 +2667,12 @@ namespace VC // first argument (used for obtaining concrete values in error trace)
public Dictionary<int, VCExpr> argExprMap;
+ // map from candidate to summary candidates
+ public Dictionary<int, List<Tuple<VCExprVar, VCExpr>>> summaryCandidates;
+ private Dictionary<string, List<Tuple<VCExprVar, VCExpr>>> summaryTemp;
+ // set of all boolean guards of summaries
+ public HashSet<VCExprVar> allSummaryConst;
+
public HashSet<int> forcedCandidates;
////////////////////////////
@@ -2420,6 +2753,10 @@ namespace VC forcedCandidates = new HashSet<int>();
id2Vars = new Dictionary<int, Dictionary<VCExprVar, VCExpr>>();
+ summaryCandidates = new Dictionary<int, List<Tuple<VCExprVar, VCExpr>>>();
+ summaryTemp = new Dictionary<string, List<Tuple<VCExprVar, VCExpr>>>();
+ allSummaryConst = new HashSet<VCExprVar>();
+ id2VC = new Dictionary<int, VCExpr>();
}
public void Clear()
@@ -2432,6 +2769,14 @@ namespace VC return (id >= pcbStartingCandidateId);
}
+ // Return the set of all candidates
+ public HashSet<int> getAllCandidates()
+ {
+ var ret = new HashSet<int>(candidateParent.Keys);
+ ret.Add(0);
+ return ret;
+ }
+
// Given a candidate "id", let proc(id) be the
// procedure corresponding to id. This procedure returns
// the number of times proc(id) appears as an ancestor
@@ -2711,6 +3056,23 @@ namespace VC }
}
+ // summary candidate
+ if (lop.label.Substring(1).StartsWith("candidate_"))
+ {
+ var pname = lop.label.Substring("candidate_".Length + 1);
+
+ if (!summaryTemp.ContainsKey(pname))
+ summaryTemp.Add(pname, new List<Tuple<VCExprVar, VCExpr>>());
+
+ var expr = retnary[0] as VCExprNAry;
+ if (expr == null) return retnary[0];
+ if (expr.Op != VCExpressionGenerator.ImpliesOp) return retnary[0];
+ var tup = Tuple.Create(expr[0] as VCExprVar, expr[1]);
+ summaryTemp[pname].Add(tup);
+
+ return retnary[0];
+ }
+
// Else, rename label
string newLabel = RenameAbsyLabel(lop.label);
if (lop.pos)
@@ -2724,8 +3086,66 @@ namespace VC }
+ // Upgrades summaryTemp to summaryCandidates by matching ensure clauses with
+ // the appropriate candidate they came from
+ public void matchSummaries()
+ {
+ var id2Set = new Dictionary<string, List<Tuple<int, HashSet<VCExprVar>>>>();
+ foreach (var id in recentlyAddedCandidates)
+ {
+ var collect = new CollectVCVars();
+ var proc = getProc(id);
+ if (!id2Set.ContainsKey(proc)) id2Set.Add(proc, new List<Tuple<int, HashSet<VCExprVar>>>());
+ id2Set[proc].Add(Tuple.Create(id, collect.Collect(id2Candidate[id], true)));
+ }
+
+ foreach (var kvp in summaryTemp)
+ {
+ Contract.Assert (id2Set.ContainsKey(kvp.Key));
+ var ls = id2Set[kvp.Key];
+ foreach (var tup in kvp.Value)
+ {
+ var collect = new CollectVCVars();
+ var s1 = collect.Collect(tup.Item2, true);
+ var found = false;
+ foreach (var t in ls)
+ {
+ var s2 = t.Item2;
+ if (s1.IsSubsetOf(s2))
+ {
+ if (!summaryCandidates.ContainsKey(t.Item1))
+ summaryCandidates.Add(t.Item1, new List<Tuple<VCExprVar, VCExpr>>());
+ summaryCandidates[t.Item1].Add(tup);
+ allSummaryConst.Add(tup.Item1);
+ found = true;
+ break;
+ }
+ }
+ Contract.Assert(found);
+ }
+ }
+ summaryTemp.Clear();
+ }
+
} // end FCallHandler
+ // Collects the set of all VCExprVar in a given VCExpr
+ class CollectVCVars : CollectingVCExprVisitor<HashSet<VCExprVar>, bool>
+ {
+ public override HashSet<VCExprVar> Visit(VCExprVar node, bool arg)
+ {
+ var ret = new HashSet<VCExprVar>();
+ ret.Add(node);
+ return ret;
+ }
+
+ protected override HashSet<VCExprVar> CombineResults(List<HashSet<VCExprVar>> results, bool arg)
+ {
+ var ret = new HashSet<VCExprVar>();
+ results.ForEach(s => ret.UnionWith(s));
+ return ret;
+ }
+ }
public class FCallInliner : MutatingVCExprVisitor<bool>
{
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index f5469ebf..c3134c09 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -149,6 +149,12 @@ namespace VC { AssumeCmd ac = (AssumeCmd)cmd;
if(CommandLineOptions.Clo.StratifiedInlining > 0) {
+ var pname = QKeyValue.FindStringAttribute(ac.Attributes, "candidate");
+ if(pname != null)
+ {
+ return gen.ImpliesSimp(gen.LabelPos("candidate_" + pname.ToString(), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N);
+ }
+
// Label the assume if it is a procedure call
NAryExpr naryExpr = ac.Expr as NAryExpr;
if (naryExpr != null) {
diff --git a/Test/VSComp2010/Answer b/Test/VSComp2010/Answer index dc523fdf..9a083fa3 100644 --- a/Test/VSComp2010/Answer +++ b/Test/VSComp2010/Answer @@ -2,24 +2,19 @@ -------------------- Problem1-SumMax.dfy --------------------
Dafny program verifier finished with 4 verified, 0 errors
-Compiled program written to out.cs
-------------------- Problem2-Invert.dfy --------------------
Dafny program verifier finished with 7 verified, 0 errors
-Compiled program written to out.cs
-------------------- Problem3-FindZero.dfy --------------------
Dafny program verifier finished with 7 verified, 0 errors
-Compiled program written to out.cs
-------------------- Problem4-Queens.dfy --------------------
Dafny program verifier finished with 9 verified, 0 errors
-Compiled program written to out.cs
-------------------- Problem5-DoubleEndedQueue.dfy --------------------
Dafny program verifier finished with 21 verified, 0 errors
-Compiled program written to out.cs
diff --git a/Test/VSComp2010/runtest.bat b/Test/VSComp2010/runtest.bat index e16eda13..9535d677 100644 --- a/Test/VSComp2010/runtest.bat +++ b/Test/VSComp2010/runtest.bat @@ -11,7 +11,5 @@ for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy Problem5-DoubleEndedQueue.dfy) do (
echo.
echo -------------------- %%f --------------------
- %DAFNY_EXE% %* %%f
-
- IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs
+ %DAFNY_EXE% /compile:0 %* %%f
)
diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat index a733a1c0..611f9251 100644 --- a/Test/VSI-Benchmarks/runtest.bat +++ b/Test/VSI-Benchmarks/runtest.bat @@ -9,11 +9,5 @@ set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do (
echo.
echo -------------------- %%f --------------------
-
- REM The following line will just run the verifier
- IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 %* %%f
-
- REM Alternatively, the following lines also produce C# code and compile it
- IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f
- IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs
+ %DAFNY_EXE% /compile:0 %* %%f
)
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat index 15bd28a1..524765cf 100644 --- a/Test/dafny1/runtest.bat +++ b/Test/dafny1/runtest.bat @@ -26,11 +26,5 @@ for %%f in (Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy UltraFilter.dfy) do (
echo.
echo -------------------- %%f --------------------
-
- REM The following line will just run the verifier
- IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
-
- REM Alternatively, the following lines also produce C# code and compile it
- IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f
- IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs
+ %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
)
diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat index 50b4ca18..6c723ea5 100644 --- a/Test/dafny2/runtest.bat +++ b/Test/dafny2/runtest.bat @@ -16,11 +16,5 @@ for %%f in ( ) do (
echo.
echo -------------------- %%f --------------------
-
- REM The following line will just run the verifier
- IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
-
- REM Alternatively, the following lines also produce C# code and compile it
- IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f
- IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs
+ %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
)
diff --git a/Test/inline/Answer b/Test/inline/Answer index 2c29ab0b..d7e7edbe 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -32,7 +32,7 @@ procedure {:inline 1} incdec(x: int, y: int) returns (z: int); -implementation incdec(x: int, y: int) returns (z: int)
+implementation {:inline 1} incdec(x: int, y: int) returns (z: int)
{
anon0:
@@ -49,7 +49,7 @@ procedure {:inline 1} inc(x: int, i: int) returns (y: int); -implementation inc(x: int, i: int) returns (y: int)
+implementation {:inline 1} inc(x: int, i: int) returns (y: int)
{
anon0:
@@ -65,7 +65,7 @@ procedure {:inline 1} dec(x: int, i: int) returns (y: int); -implementation dec(x: int, i: int) returns (y: int)
+implementation {:inline 1} dec(x: int, i: int) returns (y: int)
{
anon0:
@@ -160,7 +160,7 @@ procedure {:inline 1} incdec(x: int, y: int) returns (z: int); ensures z == x + 1 - y;
-implementation incdec(x: int, y: int) returns (z: int)
+implementation {:inline 1} incdec(x: int, y: int) returns (z: int)
{
var inline$dec$0$x: int;
var inline$dec$0$i: int;
@@ -220,7 +220,7 @@ procedure {:inline 1} increase(i: int) returns (k: int); -implementation increase(i: int) returns (k: int)
+implementation {:inline 1} increase(i: int) returns (k: int)
{
var j: int;
@@ -298,7 +298,7 @@ procedure {:inline 3} recursive(x: int) returns (y: int); -implementation recursive(x: int) returns (y: int)
+implementation {:inline 3} recursive(x: int) returns (y: int)
{
var k: int;
@@ -421,7 +421,7 @@ after inlining procedure calls procedure {:inline 3} recursive(x: int) returns (y: int);
-implementation recursive(x: int) returns (y: int)
+implementation {:inline 3} recursive(x: int) returns (y: int)
{
var k: int;
var inline$recursive$0$k: int;
@@ -560,7 +560,7 @@ procedure {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, fo -implementation find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)
+implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)
{
var i: int;
var b: bool;
@@ -606,7 +606,7 @@ procedure {:inline 3} check(A: [int]int, i: int, c: int) returns (ret: bool); -implementation check(A: [int]int, i: int, c: int) returns (ret: bool)
+implementation {:inline 3} check(A: [int]int, i: int, c: int) returns (ret: bool)
{
anon0:
@@ -746,7 +746,7 @@ after inlining procedure calls procedure {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool);
-implementation find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)
+implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)
{
var i: int;
var b: bool;
@@ -866,7 +866,7 @@ procedure {:inline 2} foo(); -implementation foo()
+implementation {:inline 2} foo()
{
anon0:
@@ -882,7 +882,7 @@ procedure {:inline 2} foo1(); -implementation foo1()
+implementation {:inline 2} foo1()
{
anon0:
@@ -898,7 +898,7 @@ procedure {:inline 2} foo2(); -implementation foo2()
+implementation {:inline 2} foo2()
{
anon0:
@@ -914,7 +914,7 @@ procedure {:inline 2} foo3(); -implementation foo3()
+implementation {:inline 2} foo3()
{
anon0:
@@ -947,7 +947,7 @@ procedure {:inline 2} foo(); modifies x;
-implementation foo()
+implementation {:inline 2} foo()
{
var inline$foo$0$x: int;
var inline$foo$1$x: int;
@@ -992,7 +992,7 @@ procedure {:inline 2} foo1(); modifies x;
-implementation foo1()
+implementation {:inline 2} foo1()
{
var inline$foo2$0$x: int;
var inline$foo3$0$x: int;
@@ -1097,7 +1097,7 @@ procedure {:inline 2} foo2(); modifies x;
-implementation foo2()
+implementation {:inline 2} foo2()
{
var inline$foo3$0$x: int;
var inline$foo1$0$x: int;
@@ -1202,7 +1202,7 @@ procedure {:inline 2} foo3(); modifies x;
-implementation foo3()
+implementation {:inline 2} foo3()
{
var inline$foo1$0$x: int;
var inline$foo2$0$x: int;
@@ -1532,7 +1532,7 @@ procedure {:inline 1} foo(); -implementation foo()
+implementation {:inline 1} foo()
{
anon0:
@@ -1605,7 +1605,7 @@ procedure {:inline 1} foo(); modifies g;
-implementation foo()
+implementation {:inline 1} foo()
{
var inline$bar$0$g: int;
diff --git a/Test/vacid0/runtest.bat b/Test/vacid0/runtest.bat index 32c6a984..efe7b3d5 100644 --- a/Test/vacid0/runtest.bat +++ b/Test/vacid0/runtest.bat @@ -9,11 +9,5 @@ set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do (
echo.
echo -------------------- %%f --------------------
-
- REM The following line will just run the verifier
- IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 %* %%f
-
- REM Alternatively, the following lines also produce C# code and compile it
- IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f
- IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs
+ %DAFNY_EXE% /compile:0 %* %%f
)
diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat index 07b5859e..5145cb56 100644 --- a/Test/vstte2012/runtest.bat +++ b/Test/vstte2012/runtest.bat @@ -14,11 +14,5 @@ for %%f in ( ) do (
echo.
echo -------------------- %%f --------------------
-
- REM The following line will just run the verifier
- IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
-
- REM Alternatively, the following lines also produce C# code and compile it
- IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f
- IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs
+ %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
)
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs index 19a5e1df..31cc412e 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs @@ -167,7 +167,7 @@ namespace DafnyLanguage : base(program) {
this.dd = dd;
}
- protected override void Error(IToken tok, string msg, params object[] args) {
+ protected override void Error(Bpl.IToken tok, string msg, params object[] args) {
string s = string.Format(msg, args);
dd.RecordError(tok.line - 1, tok.col - 1, ErrorCategory.ResolveError, s);
ErrorCount++;
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj index 4ae02e17..cf33e5a0 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj +++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj @@ -57,21 +57,28 @@ <SpecificVersion>False</SpecificVersion>
<HintPath>..\..\..\..\Binaries\DafnyPipeline.dll</HintPath>
</Reference>
- <Reference Include="FSharp.Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
- <SpecificVersion>False</SpecificVersion>
- <HintPath>..\..\..\..\Binaries\FSharp.Core.dll</HintPath>
+ <Reference Include="Graph">
+ <HintPath>..\..\..\..\Binaries\Graph.dll</HintPath>
</Reference>
- <Reference Include="FSharp.PowerPack, Version=1.9.9.9, Culture=neutral, PublicKeyToken=a19089b1c74d0809, processorArchitecture=MSIL">
- <SpecificVersion>False</SpecificVersion>
- <HintPath>..\..\..\..\Binaries\FSharp.PowerPack.dll</HintPath>
+ <Reference Include="Houdini">
+ <HintPath>..\..\..\..\Binaries\Houdini.dll</HintPath>
</Reference>
<Reference Include="Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
<SpecificVersion>False</SpecificVersion>
<HintPath>..\..\..\..\Binaries\Microsoft.Contracts.dll</HintPath>
</Reference>
+ <Reference Include="Model">
+ <HintPath>..\..\..\..\Binaries\Model.dll</HintPath>
+ </Reference>
+ <Reference Include="ParserHelper">
+ <HintPath>..\..\..\..\Binaries\ParserHelper.dll</HintPath>
+ </Reference>
<Reference Include="Provers.Z3">
<HintPath>..\..\..\..\Binaries\Provers.Z3.dll</HintPath>
</Reference>
+ <Reference Include="VCExpr">
+ <HintPath>..\..\..\..\Binaries\VCExpr.dll</HintPath>
+ </Reference>
<Reference Include="VCGeneration, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
<SpecificVersion>False</SpecificVersion>
<HintPath>..\..\..\..\Binaries\VCGeneration.dll</HintPath>
diff --git a/_admin/Boogie/aste/summary.log b/_admin/Boogie/aste/summary.log index 80cb723d..563f39d3 100644 --- a/_admin/Boogie/aste/summary.log +++ b/_admin/Boogie/aste/summary.log @@ -1,15 +1,15 @@ -# Aste started: 2011-11-17 07:00:04
+# Aste started: 2011-11-21 07:00:05
# Host id: Boogiebox
# Configuration: boogie.cfg
# Task: aste.tasks.boogie.FullBuild
-# [2011-11-17 07:03:22] SpecSharp revision: 441525d3599d
-# [2011-11-17 07:03:22] SscBoogie revision: 441525d3599d
-# [2011-11-17 07:05:04] Boogie revision: d837d1c8382c
-[2011-11-17 07:06:14] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build
+# [2011-11-21 07:03:42] SpecSharp revision: fcf3177ec66b
+# [2011-11-21 07:03:42] SscBoogie revision: fcf3177ec66b
+# [2011-11-21 07:05:30] Boogie revision: 1af8119efee0
+[2011-11-21 07:06:49] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build
1>corflags : warning CF011: The specified file is strong name signed. Using /Force will invalidate the signature of this image and will require the assembly to be resigned.
warning CF011: The specified file is strong name signed. Using /Force will invalidate the signature of this image and will require the assembly to be resigned.
-[2011-11-17 07:07:38] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked
+[2011-11-21 07:08:17] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked
D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(823,16): warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()
D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(2802,16): warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode()
@@ -24,8 +24,7 @@ D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(266,7): warning CS0162: Unreachable code detected
D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1695,11): warning CS0162: Unreachable code detected
D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1855,11): warning CS0162: Unreachable code detected
- D:\Temp\aste\Boogie\Source\VCGeneration\Check.cs(161,16): warning CS0219: The variable 'expand' is assigned but its value is never used
- D:\Temp\aste\Boogie\Source\VCGeneration\StratifiedVC.cs(850,17): warning CC1032: Method 'VC.StratifiedVCGen+NormalChecker.CheckVC' overrides 'VC.StratifiedVCGen+StratifiedCheckerInterface.CheckVC', thus cannot add Requires.
+ D:\Temp\aste\Boogie\Source\VCGeneration\StratifiedVC.cs(852,17): warning CC1032: Method 'VC.StratifiedVCGen+NormalChecker.CheckVC' overrides 'VC.StratifiedVCGen+StratifiedCheckerInterface.CheckVC', thus cannot add Requires.
warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()
warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode()
warning CS0162: Unreachable code detected
@@ -39,15 +38,6 @@ warning CS0162: Unreachable code detected
warning CS0162: Unreachable code detected
warning CS0162: Unreachable code detected
- warning CS0219: The variable 'expand' is assigned but its value is never used
warning CC1032: Method 'VC.StratifiedVCGen+NormalChecker.CheckVC' overrides 'VC.StratifiedVCGen+StratifiedCheckerInterface.CheckVC', thus cannot add Requires.
-[2011-11-17 07:07:49] [Error] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Dafny.sln /Rebuild Checked
-
- D:\Temp\aste\Boogie\Source\Dafny\Translator.cs(5071,9): error CC1022: Bad use of method 'Contract.Invariant' in method body 'Microsoft.Dafny.Translator+ExpressionTranslator.#ctor(Microsoft.Dafny.Translator,Microsoft.Dafny.Translator+PredefinedDecls,Microsoft.Boogie.Expr,System.String,Microsoft.Dafny.Function,System.Int32,System.String)'
- D:\Temp\aste\Boogie\Source\Dafny\Translator.cs(5072,9): error CC1022: Bad use of method 'Contract.Invariant' in method body 'Microsoft.Dafny.Translator+ExpressionTranslator.#ctor(Microsoft.Dafny.Translator,Microsoft.Dafny.Translator+PredefinedDecls,Microsoft.Boogie.Expr,System.String,Microsoft.Dafny.Function,System.Int32,System.String)'
- D:\Temp\aste\Boogie\Source\Dafny\DafnyOptions.cs(36,7): warning CC1032: Method 'Microsoft.Dafny.DafnyOptions.ParseOption(System.String,Microsoft.Boogie.CommandLineOptionEngine+CommandLineParseState)' overrides 'Microsoft.Boogie.CommandLineOptionEngine.ParseOption(System.String,Microsoft.Boogie.CommandLineOptionEngine+CommandLineParseState)', thus cannot add Requires.
- C:\Program Files (x86)\Microsoft\Contracts\MsBuild\v4.0\Microsoft.CodeContracts.targets(240,5): error MSB3073: The command ""C:\Program Files (x86)\Microsoft\Contracts\Bin\ccrewrite" "@DafnyPipelineccrewrite.rsp"" exited with code 2.
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Dafny\bin\Checked\DafnyPipeline.dll' could not be found
- warning CC1032: Method 'Microsoft.Dafny.DafnyOptions.ParseOption(System.String,Microsoft.Boogie.CommandLineOptionEngine+CommandLineParseState)' overrides 'Microsoft.Boogie.CommandLineOptionEngine.ParseOption(System.String,Microsoft.Boogie.CommandLineOptionEngine+CommandLineParseState)', thus cannot add Requires.
- 1 error
- 2 failed
+[2011-11-21 08:04:18] 0 out of 32 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed
+# [2011-11-21 08:04:59] Released nightly of Boogie
|