blob: f73bddb624d3ddd0ade32b16fb3898b3ac96be2d (
plain)
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
|
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics;
using Microsoft.Boogie;
using Microsoft.Basetypes;
namespace GPUVerify.InvariantGenerationRules
{
class LoopVariableBoundsInvariantGenerator : InvariantGenerationRule
{
public LoopVariableBoundsInvariantGenerator(GPUVerifier verifier)
: base(verifier)
{
}
public override void GenerateCandidates(Implementation Impl, IRegion region)
{
if (verifier.uniformityAnalyser.IsUniform(Impl.Name, region.Guard()))
{
VariablesOccurringInExpressionVisitor visitor = new VariablesOccurringInExpressionVisitor();
visitor.VisitExpr(region.Guard());
foreach (Variable v in visitor.GetVariables())
{
if (!verifier.ContainsNamedVariable(LoopInvariantGenerator.GetModifiedVariables(region), v.Name))
{
continue;
}
if (IsBVType (v.TypedIdent.Type))
{
int BVWidth = (v.TypedIdent.Type as BvType).Bits;
verifier.AddCandidateInvariant(region,
verifier.MakeBVSge(
new IdentifierExpr(v.tok, v),
new LiteralExpr(v.tok, BigNum.FromInt(0), BVWidth)), "loop guard variable non-negative");
}
}
}
}
private bool IsBVType(Microsoft.Boogie.Type type)
{
return type.Equals(Microsoft.Boogie.Type.GetBvType(32))
|| type.Equals(Microsoft.Boogie.Type.GetBvType(16))
|| type.Equals(Microsoft.Boogie.Type.GetBvType(8));
}
}
}
|
