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
137
138
139
140
141
|
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Basetypes;
using Microsoft.Boogie;
namespace GPUVerify {
class StrideConstraint {
public static StrideConstraint Bottom(Expr e) {
int width = e.Type.BvBits;
return new ModStrideConstraint(new LiteralExpr(Token.NoToken, BigNum.FromInt(1), width),
new LiteralExpr(Token.NoToken, BigNum.FromInt(0), width));
}
public bool IsBottom() {
var msc = this as ModStrideConstraint;
if (msc == null)
return false;
var le = msc.mod as LiteralExpr;
if (le == null)
return false;
var bvc = le.Val as BvConst;
if (bvc == null)
return false;
return bvc.Value.InInt32 && bvc.Value.ToInt == 1;
}
private Expr ExprModPow2(GPUVerifier verifier, Expr expr, Expr powerOfTwoExpr) {
Expr Pow2Minus1 = verifier.MakeBVSub(powerOfTwoExpr,
new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 32));
return verifier.MakeBVAnd(Pow2Minus1, expr);
}
public Expr MaybeBuildPredicate(GPUVerifier verifier, Expr e) {
var msc = this as ModStrideConstraint;
if (msc != null && !msc.IsBottom()) {
Expr modEqExpr = Expr.Eq(ExprModPow2(verifier, e, msc.mod), ExprModPow2(verifier, msc.modEq, msc.mod));
return modEqExpr;
}
return null;
}
private static StrideConstraint BuildAddStrideConstraint(GPUVerifier verifier, Expr e, StrideConstraint lhsc, StrideConstraint rhsc) {
if (lhsc is EqStrideConstraint && rhsc is EqStrideConstraint) {
return new EqStrideConstraint(e);
}
if (lhsc is EqStrideConstraint && rhsc is ModStrideConstraint)
return BuildAddStrideConstraint(verifier, e, rhsc, lhsc);
if (lhsc is ModStrideConstraint && rhsc is EqStrideConstraint) {
var lhsmc = (ModStrideConstraint)lhsc;
var rhsec = (EqStrideConstraint)rhsc;
return new ModStrideConstraint(lhsmc.mod, verifier.MakeBVAdd(lhsmc.modEq, rhsec.eq));
}
if (lhsc is ModStrideConstraint && rhsc is ModStrideConstraint) {
var lhsmc = (ModStrideConstraint)lhsc;
var rhsmc = (ModStrideConstraint)rhsc;
if (lhsmc.mod == rhsmc.mod)
return new ModStrideConstraint(lhsmc.mod, verifier.MakeBVAdd(lhsmc.modEq, rhsmc.modEq));
}
return Bottom(e);
}
private static StrideConstraint BuildMulStrideConstraint(GPUVerifier verifier, Expr e, StrideConstraint lhsc, StrideConstraint rhsc) {
if (lhsc is EqStrideConstraint && rhsc is EqStrideConstraint) {
return new EqStrideConstraint(e);
}
if (lhsc is EqStrideConstraint && rhsc is ModStrideConstraint)
return BuildMulStrideConstraint(verifier, e, rhsc, lhsc);
if (lhsc is ModStrideConstraint && rhsc is EqStrideConstraint) {
var lhsmc = (ModStrideConstraint)lhsc;
var rhsec = (EqStrideConstraint)rhsc;
return new ModStrideConstraint(verifier.MakeBVMul(lhsmc.mod, rhsec.eq),
verifier.MakeBVMul(lhsmc.modEq, rhsec.eq));
}
return Bottom(e);
}
public static StrideConstraint FromExpr(GPUVerifier verifier, Implementation impl, Expr e) {
if (e is LiteralExpr)
return new EqStrideConstraint(e);
var ie = e as IdentifierExpr;
if (ie != null) {
if (ie.Decl is Constant)
return new EqStrideConstraint(e);
var rsa = verifier.reducedStrengthAnalyses[impl];
var sc = rsa.GetStrideConstraint(ie.Decl.Name);
if (sc == null)
return Bottom(e);
return sc;
}
Expr lhs, rhs;
if (GPUVerifier.IsBVAdd(e, out lhs, out rhs)) {
var lhsc = FromExpr(verifier, impl, lhs);
var rhsc = FromExpr(verifier, impl, rhs);
return BuildAddStrideConstraint(verifier, e, lhsc, rhsc);
}
if (GPUVerifier.IsBVMul(e, out lhs, out rhs)) {
var lhsc = FromExpr(verifier, impl, lhs);
var rhsc = FromExpr(verifier, impl, rhs);
return BuildMulStrideConstraint(verifier, e, lhsc, rhsc);
}
return Bottom(e);
}
}
class EqStrideConstraint : StrideConstraint {
public EqStrideConstraint(Expr eq) { this.eq = eq; }
public Expr eq;
}
class ModStrideConstraint : StrideConstraint {
public ModStrideConstraint(Expr mod, Expr modEq) { this.mod = mod; this.modEq = modEq; }
public Expr mod, modEq;
}
}
|
