From d4762961dd719a0f0783551aea5a17203cbe42eb Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 27 Jul 2014 08:16:27 +0100 Subject: Fix bug where Visitors could not visit Requires or Ensures because the StdDispatch method was missing on both Classes. --- Source/Core/Absy.cs | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'Source/Core') diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index d6ac8754..d961eb3e 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2434,6 +2434,10 @@ namespace Microsoft.Boogie { tc.Error(this, "preconditions must be of type bool"); } } + + public override Absy StdDispatch(StandardVisitor visitor) { + return visitor.VisitRequires(this); + } } public class Ensures : Absy, IPotentialErrorNode { @@ -2528,6 +2532,10 @@ namespace Microsoft.Boogie { tc.Error(this, "postconditions must be of type bool"); } } + + public override Absy StdDispatch(StandardVisitor visitor) { + return visitor.VisitEnsures(this); + } } public class Procedure : DeclWithFormals { -- cgit v1.2.3 From ca5d2c31be76c51bb00ad5253c1ded75c404642c Mon Sep 17 00:00:00 2001 From: akashlal Date: Mon, 28 Jul 2014 16:04:00 +0530 Subject: Helper procedures --- Source/Core/Util.cs | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'Source/Core') diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs index 75cb25aa..0a2e5a22 100644 --- a/Source/Core/Util.cs +++ b/Source/Core/Util.cs @@ -252,6 +252,11 @@ namespace Microsoft.Boogie { } } + public TokenTextWriter(string filename) + : this(filename, false) + { + } + public TokenTextWriter(string filename, bool pretty) : base() { Contract.Requires(filename != null); @@ -288,6 +293,11 @@ namespace Microsoft.Boogie { this.writer = writer; } + public TokenTextWriter(TextWriter writer) + : this(writer, false) + { + } + public TokenTextWriter(TextWriter writer, bool pretty) : base() { Contract.Requires(writer != null); -- cgit v1.2.3 From cbabeb3fdef4f1ad2aed7f32ba375ad4fdd6c298 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 28 Jul 2014 16:32:51 +0100 Subject: Fix bug in NAryExpr where Equals() override was not correctly implemented. The previous implementation which called object.Equals(this.Args, other.Args) would in turn call ``this.Args.Equals(others.Args)`` which for List<> is reference equality. Equals() is purposely overloaded on Expr classes in Boogie to provide structural equality so this has been fixed so a comparision of elements in the list is performed. --- Source/Core/AbsyExpr.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Source/Core') diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index bc603ea5..0a7bfa33 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -2110,7 +2110,7 @@ namespace Microsoft.Boogie { return false; NAryExpr other = (NAryExpr)obj; - return object.Equals(this.Fun, other.Fun) && object.Equals(this.Args, other.Args); + return object.Equals(this.Fun, other.Fun) && this.Args.SequenceEqual(other.Args); } [Pure] public override int GetHashCode() { -- cgit v1.2.3 From 0a050dea52296ba1bdd5be25d1528ecf29fbc7ed Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 28 Jul 2014 17:59:36 +0100 Subject: Fix bug in BinderExpr where Equals() was not corrected implemented. BinderExpr was doing: object.Equals(this.TypeParameters, other.TypeParameters) && object.Equals(this.Dummies, other.Dummies) Both of these are wrong because these are of type List<> and so - object.Equals(this.TypeParamters, other.TypeParameters) will call this.TypeParameters.Equals(other.TypeParamters) (assuming they aren't references to the same list) - object.Equals(this.Dummies, other.TypeParameters) will call this.TypeParameters.Equals(other.Dummies) (assuming they aren't references to the same list) so this is becomes a reference comparision on Lists<>. This is wrong because Equals() has been overloaded to implement structural equality. This affects the classes ForallExpr, LambdaExpr and ExistsExpr. --- Source/Core/AbsyQuant.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Source/Core') diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index c9e8f210..ce591cee 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -88,8 +88,8 @@ namespace Microsoft.Boogie { BinderExpr other = (BinderExpr)obj; // Note, we consider quantifiers equal modulo the Triggers. - return object.Equals(this.TypeParameters, other.TypeParameters) - && object.Equals(this.Dummies, other.Dummies) + return this.TypeParameters.SequenceEqual(other.TypeParameters) + && this.Dummies.SequenceEqual(other.Dummies) && object.Equals(this.Body, other.Body); } -- cgit v1.2.3 From a1f80cb9e477aba98aef11add502dbeef0670c35 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 29 Jul 2014 14:41:48 +0100 Subject: Fix bug in NAryExpr where is was possible for A.Equals(B) to return true but A.GetHashCode() == B.GetHashCode() return false. The case of the bug was that Args.GetHashCode() was being used which uses Object.GetHashCode() which uses references to compute GetHashCode(). This is wrong because we want hash codes to equal for structural equality. To fix this I've implemented a really simple hashing method. I have not tested how resilient this is to collisions. --- Source/Core/AbsyExpr.cs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'Source/Core') diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 0a7bfa33..8d372b0c 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -2115,7 +2115,11 @@ namespace Microsoft.Boogie { [Pure] public override int GetHashCode() { int h = this.Fun.GetHashCode(); - h ^= this.Args.GetHashCode(); + // DO NOT USE Args.GetHashCode() because that uses Object.GetHashCode() which uses references + // We want structural equality + foreach (var arg in Args) { + h = (97*h) + arg.GetHashCode(); + } return h; } public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { -- cgit v1.2.3 From 2e1ad5427a4ab826615855422f6228a1a557a8ab Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 29 Jul 2014 15:04:15 +0100 Subject: Fix bug in BinderExpr where is was possible for A.Equals(B) to return true but A.GetHashCode() == B.GetHashCode() return false. --- Source/Core/AbsyQuant.cs | 22 +++++++++++++++++++--- 1 file changed, 19 insertions(+), 3 deletions(-) (limited to 'Source/Core') diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index ce591cee..eefc7102 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -95,10 +95,26 @@ namespace Microsoft.Boogie { [Pure] public override int GetHashCode() { - int h = this.Dummies.GetHashCode(); + // DO NOT USE Dummies.GetHashCode() because we want structurally + // identical Expr to have the same hash code **not** identical references + // to have the same hash code. + int h = 0; + foreach (var dummyVar in this.Dummies) { + h = ( 53 * h ) + dummyVar.GetHashCode(); + } + // Note, we consider quantifiers equal modulo the Triggers. h ^= this.Body.GetHashCode(); - h = h * 5 + this.TypeParameters.GetHashCode(); + + // DO NOT USE TypeParameters.GetHashCode() because we want structural + // identical Expr to have the same hash code **not** identical references + // to have the same hash code. + int h2 = 0; + foreach (var typeParam in this.TypeParameters) { + h2 = ( 97 * h2 ) + typeParam.GetHashCode(); + } + + h = h * 5 + h2; h *= ((int)Kind + 1); return h; } @@ -796,4 +812,4 @@ namespace Microsoft.Boogie { } } -} \ No newline at end of file +} -- cgit v1.2.3 From e5e07af52dc1e27689c55ff3ff581e39b61e17b8 Mon Sep 17 00:00:00 2001 From: qadeer Date: Wed, 30 Jul 2014 07:55:48 -0700 Subject: removed /doNotUseParallelism --- Source/Core/CommandLineOptions.cs | 3 -- Source/ExecutionEngine/ExecutionEngine.cs | 90 ++++++++++++++----------------- 2 files changed, 40 insertions(+), 53 deletions(-) (limited to 'Source/Core') diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 65554a1e..d61c9941 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -496,8 +496,6 @@ namespace Microsoft.Boogie { public int TrustPhasesUpto = -1; public int TrustPhasesDownto = int.MaxValue; - public bool UseParallelism = true; - public enum VCVariety { Structured, Block, @@ -1431,7 +1429,6 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("verifySeparately", ref VerifySeparately) || ps.CheckBooleanFlag("trustAtomicityTypes", ref TrustAtomicityTypes) || ps.CheckBooleanFlag("trustNonInterference", ref TrustNonInterference) || - ps.CheckBooleanFlag("doNotUseParallelism", ref UseParallelism, false) || ps.CheckBooleanFlag("useBaseNameForFileName", ref UseBaseNameForFileName) ) { // one of the boolean flags matched diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index de69412e..dedb3981 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -900,67 +900,57 @@ namespace Microsoft.Boogie try { - if (CommandLineOptions.Clo.UseParallelism) + var cts = new CancellationTokenSource(); + RequestIdToCancellationTokenSource.AddOrUpdate(requestId, cts, (k, ov) => cts); + + var tasks = new Task[stablePrioritizedImpls.Length]; + // We use this semaphore to limit the number of tasks that are currently executing. + var semaphore = new SemaphoreSlim(CommandLineOptions.Clo.VcsCores); + + // Create a task per implementation. + for (int i = 0; i < stablePrioritizedImpls.Length; i++) { - var cts = new CancellationTokenSource(); - RequestIdToCancellationTokenSource.AddOrUpdate(requestId, cts, (k, ov) => cts); - - var tasks = new Task[stablePrioritizedImpls.Length]; - // We use this semaphore to limit the number of tasks that are currently executing. - var semaphore = new SemaphoreSlim(CommandLineOptions.Clo.VcsCores); - - // Create a task per implementation. - for (int i = 0; i < stablePrioritizedImpls.Length; i++) + var taskIndex = i; + var id = stablePrioritizedImpls[taskIndex].Id; + + CancellationTokenSource old; + if (ImplIdToCancellationTokenSource.TryGetValue(id, out old)) { - var taskIndex = i; - var id = stablePrioritizedImpls[taskIndex].Id; - - CancellationTokenSource old; - if (ImplIdToCancellationTokenSource.TryGetValue(id, out old)) + old.Cancel(); + } + ImplIdToCancellationTokenSource.AddOrUpdate(id, cts, (k, ov) => cts); + + var t = new Task((dummy) => { - old.Cancel(); - } - ImplIdToCancellationTokenSource.AddOrUpdate(id, cts, (k, ov) => cts); - - var t = new Task((dummy) => + try { - try + if (outcome == PipelineOutcome.FatalError) { - if (outcome == PipelineOutcome.FatalError) - { - return; - } - if (cts.Token.IsCancellationRequested) - { - cts.Token.ThrowIfCancellationRequested(); - } - VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, taskIndex, outputCollector, Checkers, programId); - ImplIdToCancellationTokenSource.TryRemove(id, out old); + return; } - finally + if (cts.Token.IsCancellationRequested) { - semaphore.Release(); + cts.Token.ThrowIfCancellationRequested(); } - }, cts.Token, TaskCreationOptions.LongRunning); - tasks[taskIndex] = t; - } - - // Execute the tasks. - for (int i = 0; i < stablePrioritizedImpls.Length && outcome != PipelineOutcome.FatalError; i++) - { - semaphore.Wait(cts.Token); - tasks[i].Start(TaskScheduler.Default); - } - - Task.WaitAll(tasks); + VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, taskIndex, outputCollector, Checkers, programId); + ImplIdToCancellationTokenSource.TryRemove(id, out old); + } + finally + { + semaphore.Release(); + } + }, cts.Token, TaskCreationOptions.LongRunning); + tasks[taskIndex] = t; } - else + + // Execute the tasks. + for (int i = 0; i < stablePrioritizedImpls.Length && outcome != PipelineOutcome.FatalError; i++) { - for (int i = 0; i < stablePrioritizedImpls.Length && outcome != PipelineOutcome.FatalError; i++) - { - VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, i, outputCollector, Checkers, programId); - } + semaphore.Wait(cts.Token); + tasks[i].Start(TaskScheduler.Default); } + + Task.WaitAll(tasks); } catch (AggregateException ae) { -- cgit v1.2.3