From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/Houdini/ConcurrentHoudini.cs | 208 ++++++++++++++++++------------------ 1 file changed, 104 insertions(+), 104 deletions(-) (limited to 'Source/Houdini/ConcurrentHoudini.cs') diff --git a/Source/Houdini/ConcurrentHoudini.cs b/Source/Houdini/ConcurrentHoudini.cs index bfc7cbc1..e13fa802 100644 --- a/Source/Houdini/ConcurrentHoudini.cs +++ b/Source/Houdini/ConcurrentHoudini.cs @@ -1,104 +1,104 @@ -using System; -using System.IO; -using System.Collections.Generic; -using System.Collections.Concurrent; -using System.Diagnostics; -using System.Diagnostics.Contracts; -using System.Text.RegularExpressions; -using System.Linq; -using VC; - -namespace Microsoft.Boogie.Houdini -{ - public class ConcurrentHoudini : Houdini - { - - protected int taskID; - - private static ConcurrentDictionary refutedSharedAnnotations; - - public static ConcurrentDictionary RefutedSharedAnnotations { get { return refutedSharedAnnotations; } } - - public ConcurrentHoudini(int taskId, Program program, HoudiniSession.HoudiniStatistics stats, string cexTraceFile = "houdiniCexTrace.txt") { - Contract.Assert(taskId >= 0); - this.program = program; - this.cexTraceFile = cexTraceFile; - this.taskID = taskId; - Initialize(program, stats); - } - - static ConcurrentHoudini() - { - refutedSharedAnnotations = new ConcurrentDictionary(); - } - - protected override bool ExchangeRefutedAnnotations() - { - int count = 0; - - if (CommandLineOptions.Clo.DebugConcurrentHoudini) - Console.WriteLine("# number of shared refuted annotations: " + refutedSharedAnnotations.Count); - - foreach (string key in refutedSharedAnnotations.Keys) { - KeyValuePair kv = currentHoudiniState.Assignment.FirstOrDefault(entry => entry.Key.Name.Equals(key) && entry.Value); - - if (kv.Key != null) { - RefutedAnnotation ra = null; - Implementation refutationSite = null; - - foreach (var r in program.Implementations) { - if (r.Name.Equals(refutedSharedAnnotations[key].RefutationSite.Name)) { - refutationSite = r; - break; - } - } - Debug.Assert(refutationSite != null); - - if (refutedSharedAnnotations[key].Kind == RefutedAnnotationKind.REQUIRES) { - Procedure proc = null; - foreach (var p in program.Procedures) { - if (p.Name.Equals(refutedSharedAnnotations[key].CalleeProc.Name)) { - proc = p; - break; - } - } - Debug.Assert(proc != null); - ra = RefutedAnnotation.BuildRefutedRequires(kv.Key, proc, refutationSite); - } else if (refutedSharedAnnotations[key].Kind == RefutedAnnotationKind.ENSURES) - ra = RefutedAnnotation.BuildRefutedEnsures(kv.Key, refutationSite); - else if (refutedSharedAnnotations[key].Kind == RefutedAnnotationKind.ASSERT) - ra = RefutedAnnotation.BuildRefutedAssert(kv.Key, refutationSite); - Debug.Assert(ra != null); - - if (CommandLineOptions.Clo.DebugConcurrentHoudini) - Console.WriteLine("(+) " + ra.Constant + "," + ra.Kind + "," + ra.CalleeProc + "," + ra.RefutationSite); - - AddRelatedToWorkList(ra); - UpdateAssignment(ra); - count++; - } - } - - return count > 0 ? true : false; - } - - protected override void ShareRefutedAnnotation(RefutedAnnotation refutedAnnotation) { - refutedSharedAnnotations.TryAdd(refutedAnnotation.Constant.Name, refutedAnnotation); - } - - protected override void ApplyRefutedSharedAnnotations() { - if (refutedSharedAnnotations.Count > 0) { - foreach (var v in currentHoudiniState.Assignment.Keys.ToList()) { - if (refutedSharedAnnotations.ContainsKey(v.Name)) { - currentHoudiniState.Assignment[v] = false; - } - } - } - } - - protected override int GetTaskID() { - return taskID; - } - - } -} +using System; +using System.IO; +using System.Collections.Generic; +using System.Collections.Concurrent; +using System.Diagnostics; +using System.Diagnostics.Contracts; +using System.Text.RegularExpressions; +using System.Linq; +using VC; + +namespace Microsoft.Boogie.Houdini +{ + public class ConcurrentHoudini : Houdini + { + + protected int taskID; + + private static ConcurrentDictionary refutedSharedAnnotations; + + public static ConcurrentDictionary RefutedSharedAnnotations { get { return refutedSharedAnnotations; } } + + public ConcurrentHoudini(int taskId, Program program, HoudiniSession.HoudiniStatistics stats, string cexTraceFile = "houdiniCexTrace.txt") { + Contract.Assert(taskId >= 0); + this.program = program; + this.cexTraceFile = cexTraceFile; + this.taskID = taskId; + Initialize(program, stats); + } + + static ConcurrentHoudini() + { + refutedSharedAnnotations = new ConcurrentDictionary(); + } + + protected override bool ExchangeRefutedAnnotations() + { + int count = 0; + + if (CommandLineOptions.Clo.DebugConcurrentHoudini) + Console.WriteLine("# number of shared refuted annotations: " + refutedSharedAnnotations.Count); + + foreach (string key in refutedSharedAnnotations.Keys) { + KeyValuePair kv = currentHoudiniState.Assignment.FirstOrDefault(entry => entry.Key.Name.Equals(key) && entry.Value); + + if (kv.Key != null) { + RefutedAnnotation ra = null; + Implementation refutationSite = null; + + foreach (var r in program.Implementations) { + if (r.Name.Equals(refutedSharedAnnotations[key].RefutationSite.Name)) { + refutationSite = r; + break; + } + } + Debug.Assert(refutationSite != null); + + if (refutedSharedAnnotations[key].Kind == RefutedAnnotationKind.REQUIRES) { + Procedure proc = null; + foreach (var p in program.Procedures) { + if (p.Name.Equals(refutedSharedAnnotations[key].CalleeProc.Name)) { + proc = p; + break; + } + } + Debug.Assert(proc != null); + ra = RefutedAnnotation.BuildRefutedRequires(kv.Key, proc, refutationSite); + } else if (refutedSharedAnnotations[key].Kind == RefutedAnnotationKind.ENSURES) + ra = RefutedAnnotation.BuildRefutedEnsures(kv.Key, refutationSite); + else if (refutedSharedAnnotations[key].Kind == RefutedAnnotationKind.ASSERT) + ra = RefutedAnnotation.BuildRefutedAssert(kv.Key, refutationSite); + Debug.Assert(ra != null); + + if (CommandLineOptions.Clo.DebugConcurrentHoudini) + Console.WriteLine("(+) " + ra.Constant + "," + ra.Kind + "," + ra.CalleeProc + "," + ra.RefutationSite); + + AddRelatedToWorkList(ra); + UpdateAssignment(ra); + count++; + } + } + + return count > 0 ? true : false; + } + + protected override void ShareRefutedAnnotation(RefutedAnnotation refutedAnnotation) { + refutedSharedAnnotations.TryAdd(refutedAnnotation.Constant.Name, refutedAnnotation); + } + + protected override void ApplyRefutedSharedAnnotations() { + if (refutedSharedAnnotations.Count > 0) { + foreach (var v in currentHoudiniState.Assignment.Keys.ToList()) { + if (refutedSharedAnnotations.ContainsKey(v.Name)) { + currentHoudiniState.Assignment[v] = false; + } + } + } + } + + protected override int GetTaskID() { + return taskID; + } + + } +} -- cgit v1.2.3