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
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
|
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Boogie;
using System.Diagnostics;
namespace GPUVerify
{
class CrossThreadInvariantProcessor : StandardVisitor
{
private GPUVerifier verifier;
private string procName;
public CrossThreadInvariantProcessor(GPUVerifier verifier, string procName)
{
this.verifier = verifier;
this.procName = procName;
}
public override Expr VisitNAryExpr(NAryExpr node)
{
if (node.Fun is FunctionCall)
{
FunctionCall call = node.Fun as FunctionCall;
if (call.Func.Name.Equals("__uniform_bv32") || call.Func.Name.Equals("__uniform_bool"))
{
return Expr.Eq(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr),
new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr));
}
if (call.Func.Name.Equals("__distinct_bv32") || call.Func.Name.Equals("__distinct_bool"))
{
return Expr.Neq(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr),
new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr));
}
if (call.Func.Name.Equals("__all"))
{
return Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr),
new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr));
}
if (call.Func.Name.Equals("__exclusive"))
{
return Expr.Not(Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr),
new VariableDualiser(2, verifier.uniformityAnalyser, procName)
.VisitExpr(node.Args[0].Clone() as Expr)));
}
}
return base.VisitNAryExpr(node);
}
internal EnsuresSeq ProcessCrossThreadInvariants(EnsuresSeq ensuresSeq)
{
EnsuresSeq result = new EnsuresSeq();
foreach (Ensures e in ensuresSeq)
{
result.Add(new Ensures(e.Free, VisitExpr(e.Condition.Clone() as Expr)));
}
return result;
}
internal RequiresSeq ProcessCrossThreadInvariants(RequiresSeq requiresSeq)
{
RequiresSeq result = new RequiresSeq();
foreach (Requires r in requiresSeq)
{
result.Add(new Requires(r.Free, VisitExpr(r.Condition.Clone() as Expr)));
}
return result;
}
internal void ProcessCrossThreadInvariants(StmtList stmtList)
{
foreach (BigBlock bb in stmtList.BigBlocks)
{
ProcessCrossThreadInvariants(bb);
}
}
internal void ProcessCrossThreadInvariants(List<Block> blocks)
{
foreach (Block b in blocks)
{
b.Cmds = ProcessCrossThreadInvariants(b.Cmds);
}
}
private void ProcessCrossThreadInvariants(BigBlock bb)
{
bb.simpleCmds = ProcessCrossThreadInvariants(bb.simpleCmds);
if (bb.ec is WhileCmd)
{
WhileCmd whileCmd = bb.ec as WhileCmd;
List<PredicateCmd> newInvariants = new List<PredicateCmd>();
foreach (PredicateCmd p in whileCmd.Invariants)
{
newInvariants.Add(new AssertCmd(p.tok, VisitExpr(p.Expr)));
}
whileCmd.Invariants = newInvariants;
ProcessCrossThreadInvariants(whileCmd.Body);
}
}
private CmdSeq ProcessCrossThreadInvariants(CmdSeq cmds)
{
CmdSeq newCommands = new CmdSeq();
foreach (Cmd c in cmds)
{
if (c is AssertCmd)
{
newCommands.Add(new AssertCmd(c.tok, VisitExpr((c as AssertCmd).Expr.Clone() as Expr)));
}
else if (c is AssumeCmd)
{
newCommands.Add(new AssumeCmd(c.tok, VisitExpr((c as AssumeCmd).Expr.Clone() as Expr)));
}
else
{
newCommands.Add(c);
}
}
return newCommands;
}
}
}
|
