diff options
Diffstat (limited to 'Source/GPUVerify/GPUVerifier.cs')
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 74 |
1 files changed, 43 insertions, 31 deletions
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index bada4cef..27ec052e 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -1550,37 +1550,50 @@ namespace GPUVerify if (c is AssignCmd)
{
AssignCmd assign = c as AssignCmd;
- Debug.Assert(assign.Lhss.Count == 1);
- Debug.Assert(assign.Rhss.Count == 1);
- AssignLhs lhs = assign.Lhss[0];
- Expr rhs = assign.Rhss[0];
- ReadCollector rc = new ReadCollector(NonLocalState);
- rc.Visit(rhs);
-
- bool foundAdversarial = false;
- foreach (AccessRecord ar in rc.accesses)
+
+ var lhss = new List<AssignLhs>();
+ var rhss = new List<Expr>();
+
+ for (int i = 0; i != assign.Lhss.Count; i++)
{
- if (ArrayModelledAdversarially(ar.v))
+ AssignLhs lhs = assign.Lhss[i];
+ Expr rhs = assign.Rhss[i];
+ ReadCollector rc = new ReadCollector(NonLocalState);
+ rc.Visit(rhs);
+
+ bool foundAdversarial = false;
+ foreach (AccessRecord ar in rc.accesses)
{
- foundAdversarial = true;
- break;
+ if (ArrayModelledAdversarially(ar.v))
+ {
+ foundAdversarial = true;
+ break;
+ }
}
- }
- if (foundAdversarial)
- {
- Debug.Assert(lhs is SimpleAssignLhs);
- result.Add(new HavocCmd(c.tok, new IdentifierExprSeq(new IdentifierExpr[] { (lhs as SimpleAssignLhs).AssignedVariable })));
- continue;
+ if (foundAdversarial)
+ {
+ Debug.Assert(lhs is SimpleAssignLhs);
+ result.Add(new HavocCmd(c.tok, new IdentifierExprSeq(new IdentifierExpr[] { (lhs as SimpleAssignLhs).AssignedVariable })));
+ continue;
+ }
+
+ WriteCollector wc = new WriteCollector(NonLocalState);
+ wc.Visit(lhs);
+ if (wc.GetAccess() != null && ArrayModelledAdversarially(wc.GetAccess().v))
+ {
+ continue; // Just remove the write
+ }
+
+ lhss.Add(lhs);
+ rhss.Add(rhs);
}
- WriteCollector wc = new WriteCollector(NonLocalState);
- wc.Visit(lhs);
- if (wc.GetAccess() != null && ArrayModelledAdversarially(wc.GetAccess().v))
+ if (lhss.Count != 0)
{
- continue; // Just remove the write
+ result.Add(new AssignCmd(assign.tok, lhss, rhss));
}
-
+ continue;
}
result.Add(c);
}
@@ -1892,19 +1905,18 @@ namespace GPUVerify {
AssignCmd assign = c as AssignCmd;
- Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);
-
- AssignLhs lhs = assign.Lhss.ElementAt(0);
- Expr rhs = assign.Rhss.ElementAt(0);
-
- if (!NonLocalAccessCollector.ContainsNonLocalAccess(rhs, NonLocalState) ||
- (!NonLocalAccessCollector.ContainsNonLocalAccess(lhs, NonLocalState) &&
- NonLocalAccessCollector.IsNonLocalAccess(rhs, NonLocalState)))
+ if (assign.Lhss.Zip(assign.Rhss, (lhs, rhs) =>
+ !NonLocalAccessCollector.ContainsNonLocalAccess(rhs, NonLocalState) ||
+ (!NonLocalAccessCollector.ContainsNonLocalAccess(lhs, NonLocalState) &&
+ NonLocalAccessCollector.IsNonLocalAccess(rhs, NonLocalState))).All(b => b))
{
result.simpleCmds.Add(c);
}
else
{
+ Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);
+ AssignLhs lhs = assign.Lhss.ElementAt(0);
+ Expr rhs = assign.Rhss.ElementAt(0);
rhs = PullOutNonLocalAccessesIntoTemps(result, rhs, impl);
List<AssignLhs> newLhss = new List<AssignLhs>();
newLhss.Add(lhs);
|