1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
|
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<string, RefutedAnnotation> refutedSharedAnnotations;
public static ConcurrentDictionary<string, RefutedAnnotation> 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<string, RefutedAnnotation>();
}
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<Variable, bool> 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;
}
}
}
|
