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
|
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Boogie;
using System.Diagnostics;
namespace GPUVerify
{
class EnsureDisabledThreadHasNoEffectInstrumenter
{
private GPUVerifier verifier;
private Implementation Impl;
public EnsureDisabledThreadHasNoEffectInstrumenter(GPUVerifier verifier, Implementation Impl)
{
this.verifier = verifier;
this.Impl = Impl;
}
internal void instrument()
{
if (verifier.uniformityAnalyser.IsUniform(Impl.Name))
{
return;
}
foreach (IdentifierExpr iex in Impl.Proc.Modifies)
{
// For some reason, this does not work well with maps
if (iex.Decl.TypedIdent.Type is MapType)
{
continue;
}
Expr NoEffectExpr = Expr.Imp(
Expr.Not(new IdentifierExpr(iex.tok, new LocalVariable(iex.tok, new TypedIdent(iex.tok, "_P$" +
GPUVerifier.GetThreadSuffix(iex.Name), Microsoft.Boogie.Type.Bool)))),
Expr.Eq(iex, new OldExpr(iex.tok, iex))
);
Impl.Proc.Ensures.Add(new Ensures(false,
NoEffectExpr
));
GPUVerifier.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 = GPUVerifier.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);
}
}
}
}
|
