diff options
| -rw-r--r-- | Source/Core/Absy.cs | 19 | ||||
| -rw-r--r-- | Source/Core/Util.cs | 5 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 2 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 2 | ||||
| -rw-r--r-- | Source/GPUVerify/ElementEncodingRaceInstrumenter.cs | 69 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 46 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerify.csproj | 9 | ||||
| -rw-r--r-- | Source/GPUVerify/IRegion.cs | 1 | ||||
| -rw-r--r-- | Source/GPUVerify/KernelDualiser.cs | 23 | ||||
| -rw-r--r-- | Source/GPUVerify/MayBeFlattened2DTidOrGidAnalyser.cs | 322 | ||||
| -rw-r--r-- | Source/GPUVerify/MayBeGlobalSizeAnalyser.cs | 287 | ||||
| -rw-r--r-- | Source/GPUVerify/RaceInstrumenterBase.cs | 52 | ||||
| -rw-r--r-- | Source/GPUVerify/StructuredRegion.cs | 37 | ||||
| -rw-r--r-- | Source/GPUVerify/UnstructuredRegion.cs | 6 | ||||
| -rw-r--r-- | Source/GPUVerify/VariableDefinitionAnalysis.cs | 155 | ||||
| -rw-r--r-- | Source/VCGeneration/BlockPredicator.cs (renamed from Source/GPUVerify/BlockPredicator.cs) | 111 | ||||
| -rwxr-xr-x[-rw-r--r--] | Source/VCGeneration/GraphAlgorithms.cs (renamed from Source/GPUVerify/GraphAlgorithms.cs) | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/VCGeneration.csproj | 2 |
18 files changed, 327 insertions, 823 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index c4b5d7a9..9df982d9 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -911,6 +911,25 @@ namespace Microsoft.Boogie { }
return globals;
}
+
+ private int invariantGenerationCounter = 0;
+
+ public Constant MakeExistentialBoolean() {
+ Constant ExistentialBooleanConstant = new Constant(Token.NoToken, new TypedIdent(tok, "_b" + invariantGenerationCounter, Microsoft.Boogie.Type.Bool), false);
+ invariantGenerationCounter++;
+ ExistentialBooleanConstant.AddAttribute("existential", new object[] { Expr.True });
+ TopLevelDeclarations.Add(ExistentialBooleanConstant);
+ return ExistentialBooleanConstant;
+ }
+
+ public PredicateCmd CreateCandidateInvariant(Expr e, string tag = null) {
+ Constant ExistentialBooleanConstant = MakeExistentialBoolean();
+ IdentifierExpr ExistentialBoolean = new IdentifierExpr(Token.NoToken, ExistentialBooleanConstant);
+ PredicateCmd invariant = new AssertCmd(Token.NoToken, Expr.Imp(ExistentialBoolean, e));
+ if (tag != null)
+ invariant.Attributes = new QKeyValue(Token.NoToken, "tag", new List<object>(new object[] { tag }), null);
+ return invariant;
+ }
}
//---------------------------------------------------------------------
diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs index f45e2995..a8e12f63 100644 --- a/Source/Core/Util.cs +++ b/Source/Core/Util.cs @@ -61,6 +61,11 @@ namespace Microsoft.Boogie { {
foreach (var e in coll) fn(e);
}
+
+ public static IEnumerable<Tuple<TSource1, TSource2>> Zip<TSource1, TSource2>(this IEnumerable<TSource1> source1, IEnumerable<TSource2> source2)
+ {
+ return source1.Zip(source2, (e1, e2) => new Tuple<TSource1, TSource2>(e1, e2));
+ }
}
public class TokenTextWriter : IDisposable {
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index cbdf5c79..66756b0c 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -499,7 +499,7 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty> GenericInstantiation<gt> (. if (gt.Count != 2) {
SemErr("map type expects exactly two type arguments");
}
- ty = new MapType(gt[0], gt[1]);
+ else { ty = new MapType(gt[0], gt[1]); }
.)
| ReferenceType<out tok, out ty>
)
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index d6ae7e93..26b98833 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -786,7 +786,7 @@ bool IsAttribute() { if (gt.Count != 2) {
SemErr("map type expects exactly two type arguments");
}
- ty = new MapType(gt[0], gt[1]);
+ else { ty = new MapType(gt[0], gt[1]); }
break;
}
diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs index 3cd29367..cb880767 100644 --- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs +++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs @@ -205,16 +205,16 @@ namespace GPUVerify }
- protected override void AddAccessedOffsetIsThreadGlobalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite)
+ protected override void AddAccessedOffsetsAreConstantCandidateInvariant(IRegion region, Variable v, IEnumerable<Expr> offsets, string ReadOrWrite)
{
- Expr expr = AccessedOffsetIsThreadGlobalIdExpr(v, ReadOrWrite, 1);
- verifier.AddCandidateInvariant(region, expr, "accessed offset is global id");
+ Expr expr = AccessedOffsetsAreConstantExpr(v, offsets, ReadOrWrite, 1);
+ verifier.AddCandidateInvariant(region, expr, "accessed offsets are constant");
}
- protected override void AddAccessedOffsetIsThreadLocalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite)
- {
- Expr expr = AccessedOffsetIsThreadLocalIdExpr(v, ReadOrWrite, 1);
- verifier.AddCandidateInvariant(region, expr, "accessed offset is local id");
+ private Expr AccessedOffsetsAreConstantExpr(Variable v, IEnumerable<Expr> offsets, string ReadOrWrite, int Thread) {
+ return Expr.Imp(
+ new IdentifierExpr(Token.NoToken, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),
+ offsets.Select(ofs => (Expr)Expr.Eq(new IdentifierExpr(Token.NoToken, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite))), ofs)).Aggregate(Expr.Or));
}
private Expr AccessedOffsetIsThreadLocalIdExpr(Variable v, string ReadOrWrite, int Thread)
@@ -250,61 +250,6 @@ namespace GPUVerify return new VariableDualiser(Thread, null, null).VisitExpr(verifier.GlobalIdExpr(dimension).Clone() as Expr);
}
- private Expr GlobalSizeExpr(string dimension)
- {
- return GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL",
- new IdentifierExpr(Token.NoToken, verifier.GetNumGroups(dimension)),
- new IdentifierExpr(Token.NoToken, verifier.GetGroupSize(dimension)));
- }
-
- protected override void AddAccessedOffsetIsThreadFlattened2DLocalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite)
- {
- Expr expr = AccessedOffsetIsThreadFlattened2DLocalIdExpr(v, ReadOrWrite, 1);
- verifier.AddCandidateInvariant(region, expr, "accessed offset is flattened 2D local id");
- }
-
- private Expr AccessedOffsetIsThreadFlattened2DLocalIdExpr(Variable v, string ReadOrWrite, int Thread)
- {
- Expr expr = null;
- if (GPUVerifier.HasXDimension(v) && GPUVerifier.IndexTypeOfXDimension(v).Equals(verifier.GetTypeOfIdX()))
- {
- expr = Expr.Imp(
- AccessHasOccurred(v, ReadOrWrite, Thread),
- Expr.Eq(
- new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite))),
- GPUVerifier.MakeBitVectorBinaryBitVector("BV32_ADD", GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL",
- new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Y", Thread)), new IdentifierExpr(v.tok, verifier.GetGroupSize("X"))),
- new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread)))
- )
- );
- }
- return expr;
- }
-
- protected override void AddAccessedOffsetIsThreadFlattened2DGlobalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite)
- {
- Expr expr = AccessedOffsetIsThreadFlattened2DGlobalIdExpr(v, ReadOrWrite, 1);
- verifier.AddCandidateInvariant(region, expr, "accessed offset is flattened 2D global id");
- }
-
- private Expr AccessedOffsetIsThreadFlattened2DGlobalIdExpr(Variable v, string ReadOrWrite, int Thread)
- {
- Expr expr = null;
- if (GPUVerifier.HasXDimension(v) && GPUVerifier.IndexTypeOfXDimension(v).Equals(verifier.GetTypeOfIdX()))
- {
- expr = Expr.Imp(
- AccessHasOccurred(v, ReadOrWrite, Thread),
- Expr.Eq(
- new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite))),
- GPUVerifier.MakeBitVectorBinaryBitVector("BV32_ADD", GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL",
- GlobalIdExpr("Y", Thread), GlobalSizeExpr("X")),
- GlobalIdExpr("X", Thread))
- )
- );
- }
- return expr;
- }
-
protected override void AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite)
{
Expr expr = MakeCTimesLocalIdRangeExpression(v, constant, ReadOrWrite, 1);
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index a49461c7..40e27310 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -25,7 +25,6 @@ namespace GPUVerify private HashSet<string> ReservedNames = new HashSet<string>();
private int TempCounter = 0;
- private int invariantGenerationCounter = 0;
internal const string LOCAL_ID_X_STRING = "local_id_x";
internal const string LOCAL_ID_Y_STRING = "local_id_y";
@@ -64,13 +63,12 @@ namespace GPUVerify public UniformityAnalyser uniformityAnalyser;
public MayBeThreadConfigurationVariableAnalyser mayBeTidAnalyser;
public MayBeGidAnalyser mayBeGidAnalyser;
- public MayBeGlobalSizeAnalyser mayBeGlobalSizeAnalyser;
- public MayBeFlattened2DTidOrGidAnalyser mayBeFlattened2DTidOrGidAnalyser;
public MayBeLocalIdPlusConstantAnalyser mayBeTidPlusConstantAnalyser;
public MayBeGlobalIdPlusConstantAnalyser mayBeGidPlusConstantAnalyser;
public MayBePowerOfTwoAnalyser mayBePowerOfTwoAnalyser;
public LiveVariableAnalyser liveVariableAnalyser;
public ArrayControlFlowAnalyser arrayControlFlowAnalyser;
+ public Dictionary<Implementation, VariableDefinitionAnalysis> varDefAnalyses;
public GPUVerifier(string filename, Program program, ResolutionContext rc, IRaceInstrumenter raceInstrumenter) : this(filename, program, rc, raceInstrumenter, false)
{
@@ -371,6 +369,8 @@ namespace GPUVerify DoArrayControlFlowAnalysis();
+ DoVariableDefinitionAnalysis();
+
if (CommandLineOptions.ShowStages)
{
emitProgram(outputFilename + "_preprocessed");
@@ -490,12 +490,6 @@ namespace GPUVerify mayBeGidAnalyser = new MayBeGidAnalyser(this);
mayBeGidAnalyser.Analyse();
-
- mayBeGlobalSizeAnalyser = new MayBeGlobalSizeAnalyser(this);
- mayBeGlobalSizeAnalyser.Analyse();
-
- mayBeFlattened2DTidOrGidAnalyser = new MayBeFlattened2DTidOrGidAnalyser(this);
- mayBeFlattened2DTidOrGidAnalyser.Analyse();
}
private void DoMayBeIdPlusConstantAnalysis()
@@ -524,6 +518,12 @@ namespace GPUVerify liveVariableAnalyser.Analyse();
}
+ private void DoVariableDefinitionAnalysis()
+ {
+ varDefAnalyses = Program.TopLevelDeclarations
+ .OfType<Implementation>()
+ .ToDictionary(i => i, i => VariableDefinitionAnalysis.Analyse(this, i));
+ }
private void ProcessAccessInvariants()
{
@@ -814,18 +814,16 @@ namespace GPUVerify internal void AddCandidateRequires(Procedure Proc, Expr e)
{
- Constant ExistentialBooleanConstant = MakeExistentialBoolean(Proc.tok);
+ Constant ExistentialBooleanConstant = Program.MakeExistentialBoolean();
IdentifierExpr ExistentialBoolean = new IdentifierExpr(Proc.tok, ExistentialBooleanConstant);
Proc.Requires.Add(new Requires(false, Expr.Imp(ExistentialBoolean, e)));
- Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);
}
internal void AddCandidateEnsures(Procedure Proc, Expr e)
{
- Constant ExistentialBooleanConstant = MakeExistentialBoolean(Proc.tok);
+ Constant ExistentialBooleanConstant = Program.MakeExistentialBoolean();
IdentifierExpr ExistentialBoolean = new IdentifierExpr(Proc.tok, ExistentialBooleanConstant);
Proc.Ensures.Add(new Ensures(false, Expr.Imp(ExistentialBoolean, e)));
- Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);
}
private List<Expr> GetUserSuppliedInvariants(string ProcedureName)
@@ -1042,14 +1040,6 @@ namespace GPUVerify return _GROUP_SIZE_Z != null;
}
- internal Constant MakeExistentialBoolean(IToken tok)
- {
- Constant ExistentialBooleanConstant = new Constant(tok, new TypedIdent(tok, "_b" + invariantGenerationCounter, Microsoft.Boogie.Type.Bool), false);
- invariantGenerationCounter++;
- ExistentialBooleanConstant.AddAttribute("existential", new object[] { Expr.True });
- return ExistentialBooleanConstant;
- }
-
internal static string StripThreadIdentifier(string p)
{
if (p.Contains("$"))
@@ -2152,7 +2142,7 @@ namespace GPUVerify {
if (CommandLineOptions.Unstructured)
{
- BlockPredicator.Predicate(this, Program);
+ BlockPredicator.Predicate(Program, /*createCandidateInvariants=*/CommandLineOptions.Inference);
return;
}
@@ -2256,19 +2246,9 @@ namespace GPUVerify internal void AddCandidateInvariant(IRegion region, Expr e, string tag)
{
- region.AddInvariant(CreateCandidateInvariant(e, tag));
+ region.AddInvariant(Program.CreateCandidateInvariant(e, tag));
}
- internal PredicateCmd CreateCandidateInvariant(Expr e, string tag)
- {
- Constant ExistentialBooleanConstant = MakeExistentialBoolean(Token.NoToken);
- IdentifierExpr ExistentialBoolean = new IdentifierExpr(Token.NoToken, ExistentialBooleanConstant);
- PredicateCmd invariant = new AssertCmd(Token.NoToken, Expr.Imp(ExistentialBoolean, e));
- invariant.Attributes = new QKeyValue(Token.NoToken, "tag", new List<object>(new object[] { tag }), null);
- Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);
- return invariant;
- }
-
internal Implementation GetImplementation(string procedureName)
{
foreach (Declaration D in Program.TopLevelDeclarations)
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index 376d67b5..eba91cd2 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -108,15 +108,11 @@ <Compile Include="AccessRecord.cs" />
<Compile Include="ArrayControlFlowAnalyser.cs" />
<Compile Include="AsymmetricExpressionFinder.cs" />
- <Compile Include="BlockPredicator.cs" />
<Compile Include="UnstructuredRegion.cs" />
<Compile Include="IRegion.cs" />
- <Compile Include="GraphAlgorithms.cs" />
<Compile Include="InvariantGenerationRules\LoopVariableBoundsInvariantGenerator.cs" />
<Compile Include="InvariantGenerationRules\InvariantGenerationRule.cs" />
<Compile Include="InvariantGenerationRules\PowerOfTwoInvariantGenerator.cs" />
- <Compile Include="MayBeGlobalSizeAnalyser.cs" />
- <Compile Include="MayBeFlattened2DTidOrGidAnalyser.cs" />
<Compile Include="MayBeGidAnalyser.cs" />
<Compile Include="EnsureDisabledThreadHasNoEffectInstrumenter.cs" />
<Compile Include="KernelDualiser.cs" />
@@ -147,6 +143,7 @@ <Compile Include="UniformityAnalyser.cs" />
<Compile Include="VariableDualiser.cs" />
<Compile Include="VariablesOccurringInExpressionVisitor.cs" />
+ <Compile Include="VariableDefinitionAnalysis.cs" />
<Compile Include="StructuredRegion.cs" />
<Compile Include="WriteCollector.cs" />
</ItemGroup>
@@ -171,6 +168,10 @@ <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
<Name>ParserHelper</Name>
</ProjectReference>
+ <ProjectReference Include="..\VCGeneration\VCGeneration.csproj">
+ <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
+ <Name>VCGeneration</Name>
+ </ProjectReference>
</ItemGroup>
<Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
<!-- To modify your build process, add your task inside one of the targets below and uncomment it.
diff --git a/Source/GPUVerify/IRegion.cs b/Source/GPUVerify/IRegion.cs index 26adaa4e..c6655b06 100644 --- a/Source/GPUVerify/IRegion.cs +++ b/Source/GPUVerify/IRegion.cs @@ -7,6 +7,7 @@ using Microsoft.Boogie; namespace GPUVerify {
interface IRegion {
+ object Identifier();
IEnumerable<Cmd> Cmds();
IEnumerable<object> CmdsChildRegions();
IEnumerable<IRegion> SubRegions();
diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs index 614659b6..967b69ef 100644 --- a/Source/GPUVerify/KernelDualiser.cs +++ b/Source/GPUVerify/KernelDualiser.cs @@ -186,32 +186,27 @@ namespace GPUVerify else if (c is AssertCmd)
{
AssertCmd ass = c as AssertCmd;
- if (ContainsAsymmetricExpression(ass.Expr))
+ cs.Add(new AssertCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr), ass.Attributes));
+ if (!ContainsAsymmetricExpression(ass.Expr))
{
- cs.Add(new AssertCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr), ass.Attributes));
- }
- else
- {
- cs.Add(new AssertCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),
- new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)), ass.Attributes));
+ cs.Add(new AssertCmd(c.tok, new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr), ass.Attributes));
}
}
else if (c is AssumeCmd)
{
AssumeCmd ass = c as AssumeCmd;
- if (ContainsAsymmetricExpression(ass.Expr))
- {
- cs.Add(new AssumeCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));
- }
- else if (QKeyValue.FindBoolAttribute(ass.Attributes, "backedge"))
+ if (QKeyValue.FindBoolAttribute(ass.Attributes, "backedge"))
{
cs.Add(new AssumeCmd(c.tok, Expr.Or(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),
new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));
}
else
{
- cs.Add(new AssumeCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),
- new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));
+ cs.Add(new AssumeCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));
+ if (!ContainsAsymmetricExpression(ass.Expr))
+ {
+ cs.Add(new AssumeCmd(c.tok, new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));
+ }
}
}
else
diff --git a/Source/GPUVerify/MayBeFlattened2DTidOrGidAnalyser.cs b/Source/GPUVerify/MayBeFlattened2DTidOrGidAnalyser.cs deleted file mode 100644 index ea9b85fa..00000000 --- a/Source/GPUVerify/MayBeFlattened2DTidOrGidAnalyser.cs +++ /dev/null @@ -1,322 +0,0 @@ -using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Diagnostics;
-using Microsoft.Boogie;
-
-namespace GPUVerify
-{
- class MayBeFlattened2DTidOrGidAnalyser
- {
- private static string[] cases = { "local", "global" };
-
- private GPUVerifier verifier;
-
- private bool ProcedureChanged;
-
- private Dictionary<string, Dictionary<string, Dictionary<string, bool>>> mayBeInfo;
-
- public MayBeFlattened2DTidOrGidAnalyser(GPUVerifier verifier)
- {
- this.verifier = verifier;
-
- mayBeInfo = new Dictionary<string,Dictionary<string,Dictionary<string,bool>>>();
- foreach (string s in cases)
- {
- mayBeInfo[s] = new Dictionary<string, Dictionary<string, bool>>();
- }
-
- }
-
- internal void Analyse()
- {
- foreach (Declaration D in verifier.Program.TopLevelDeclarations)
- {
- if(D is Implementation)
- {
- Implementation Impl = D as Implementation;
-
- foreach (string s in cases)
- {
- mayBeInfo[s][Impl.Name] = new Dictionary<string, bool>();
- }
-
- foreach (Variable v in Impl.LocVars)
- {
- foreach (string s in cases)
- {
- SetMayBe(s, Impl.Name, v.Name);
- }
- }
-
- foreach (Variable v in Impl.InParams)
- {
- foreach (string s in cases)
- {
- SetMayBe(s, Impl.Name, v.Name);
- }
- }
-
- foreach (Variable v in Impl.OutParams)
- {
- foreach (string s in cases)
- {
- SetMayBe(s, Impl.Name, v.Name);
- }
- }
-
- ProcedureChanged = true;
- }
- }
-
- while (ProcedureChanged)
- {
- ProcedureChanged = false;
-
- foreach (Declaration D in verifier.Program.TopLevelDeclarations)
- {
- if (D is Implementation)
- {
- Implementation Impl = D as Implementation;
- Analyse(Impl);
- }
- }
- }
-
- if (CommandLineOptions.ShowMayBeThreadConfigurationVariableAnalysis)
- {
- dump();
- }
- }
-
- private void Analyse(Implementation Impl)
- {
- Analyse(Impl, verifier.RootRegion(Impl));
- }
-
- private void Analyse(Implementation impl, IRegion region)
- {
- foreach (Cmd c in region.Cmds())
- {
- if (c is AssignCmd)
- {
- foreach (string s in cases)
- {
- TransferAssign(impl, c as AssignCmd, s);
- }
- }
- else if (c is CallCmd)
- {
- foreach (string s in cases)
- {
- TransferCall(impl, c as CallCmd, s);
- }
- }
- else if (c is HavocCmd)
- {
- foreach (string s in cases)
- {
- TransferHavoc(impl, c as HavocCmd, s);
- }
- }
- }
- }
-
- private void TransferHavoc(Implementation impl, HavocCmd havoc, string component)
- {
- Debug.Assert(havoc.Vars.Length == 1);
- if (MayBe(component, impl.Name, havoc.Vars[0].Decl.Name))
- {
- SetNot(component, impl.Name, havoc.Vars[0].Decl.Name);
- }
- }
-
- private void TransferCall(Implementation impl, CallCmd callCmd, string component)
- {
- if (callCmd.callee != verifier.BarrierProcedure.Name)
- {
-
- Implementation CalleeImplementation = verifier.GetImplementation(callCmd.callee);
- for (int i = 0; i < CalleeImplementation.InParams.Length; i++)
- {
- if (MayBe(component, callCmd.callee, CalleeImplementation.InParams[i].Name)
- && !MayBe(component, impl.Name, callCmd.Ins[i]))
- {
- SetNot(component, callCmd.callee, CalleeImplementation.InParams[i].Name);
- }
- }
-
- for (int i = 0; i < CalleeImplementation.OutParams.Length; i++)
- {
- if (MayBe(component, impl.Name, callCmd.Outs[i].Name)
- && !MayBe(component, callCmd.callee, CalleeImplementation.OutParams[i].Name))
- {
- SetNot(component, impl.Name, callCmd.Outs[i].Name);
- }
- }
-
- }
- }
-
- private void TransferAssign(Implementation impl, AssignCmd assignCmd, string component)
- {
- for (int i = 0; i != assignCmd.Lhss.Count; ++i)
- {
- if (assignCmd.Lhss[i] is SimpleAssignLhs)
- {
- SimpleAssignLhs lhs = assignCmd.Lhss[i] as SimpleAssignLhs;
- Expr rhs = assignCmd.Rhss[i];
-
- if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)
- && !MayBe(component, impl.Name, rhs))
- {
- SetNot(component, impl.Name, lhs.AssignedVariable.Name);
- }
- }
- }
- }
-
- private void SetNot(string component, string proc, string v)
- {
- mayBeInfo[component][proc][v] = false;
- ProcedureChanged = true;
- }
-
- private void SetMayBe(string component, string proc, string v)
- {
- mayBeInfo[component][proc][v] = true;
- }
-
- internal bool MayBe(string component, string proc, string v)
- {
- if (!mayBeInfo[component].ContainsKey(proc))
- {
- return false;
- }
-
- if (!mayBeInfo[component][proc].ContainsKey(v))
- {
- return false;
- }
-
- return mayBeInfo[component][proc][v];
- }
-
- internal bool MayBe(string component, string proc, Expr e)
- {
- if (e is IdentifierExpr)
- {
- return MayBe(component, proc, (e as IdentifierExpr).Decl.Name);
- }
-
- if (e is NAryExpr && (e as NAryExpr).Fun.FunctionName.Equals("BV32_ADD"))
- {
- NAryExpr nary = e as NAryExpr;
-
- if (component.Equals("local"))
- {
- if (verifier.mayBeTidAnalyser.MayBe(GPUVerifier.LOCAL_ID_X_STRING, proc, nary.Args[1]))
- {
- return IsLocalIdYTimesGroupSizeX(proc, nary.Args[0]);
- }
-
- if (verifier.mayBeTidAnalyser.MayBe(GPUVerifier.LOCAL_ID_X_STRING, proc, nary.Args[0]))
- {
- return IsLocalIdYTimesGroupSizeX(proc, nary.Args[1]);
- }
- }
- else
- {
- Debug.Assert(component.Equals("global"));
- if (verifier.mayBeGidAnalyser.MayBe("x", proc, nary.Args[1]))
- {
- return IsGlobalIdYTimesGlobalSizeX(proc, nary.Args[0]);
- }
-
- if (verifier.mayBeGidAnalyser.MayBe("x", proc, nary.Args[0]))
- {
- return IsGlobalIdYTimesGlobalSizeX(proc, nary.Args[1]);
- }
- }
- }
-
- return false;
- }
-
- private bool IsLocalIdYTimesGroupSizeX(string proc, Expr expr)
- {
- if (expr is NAryExpr && (expr as NAryExpr).Fun.FunctionName.Equals("BV32_MUL"))
- {
- NAryExpr innerNary = expr as NAryExpr;
-
- if (IsLocalIdYAndGroupSizeX(proc, innerNary.Args[0], innerNary.Args[1]))
- {
- return true;
- }
-
- if (IsLocalIdYAndGroupSizeX(proc, innerNary.Args[1], innerNary.Args[0]))
- {
- return true;
- }
- }
- return false;
- }
-
- private bool IsLocalIdYAndGroupSizeX(string proc, Expr maybeLocalIdY, Expr maybeGroupSizeX)
- {
- return verifier.mayBeTidAnalyser.MayBe(GPUVerifier.LOCAL_ID_Y_STRING, proc, maybeLocalIdY) &&
- verifier.mayBeTidAnalyser.MayBe(GPUVerifier.GROUP_SIZE_X_STRING, proc, maybeGroupSizeX);
- }
-
-
- private bool IsGlobalIdYTimesGlobalSizeX(string proc, Expr expr)
- {
- if (expr is NAryExpr && (expr as NAryExpr).Fun.FunctionName.Equals("BV32_MUL"))
- {
- NAryExpr innerNary = expr as NAryExpr;
-
- if (IsGlobalIdYAndGlobalSizeX(proc, innerNary.Args[0], innerNary.Args[1]))
- {
- return true;
- }
-
- if (IsGlobalIdYAndGlobalSizeX(proc, innerNary.Args[1], innerNary.Args[0]))
- {
- return true;
- }
- }
- return false;
- }
-
- private bool IsGlobalIdYAndGlobalSizeX(string proc, Expr maybeGlobalIdY, Expr maybeGlobalSizeX)
- {
- return verifier.mayBeGidAnalyser.MayBe("y", proc, maybeGlobalIdY) &&
- verifier.mayBeGlobalSizeAnalyser.MayBe("x", proc, maybeGlobalSizeX);
- }
-
-
- private void dump()
- {
- foreach (string s in cases)
- {
- Console.WriteLine("*** flattened " + s + " id ***");
-
- foreach (string p in mayBeInfo[s].Keys)
- {
- Console.WriteLine(" Procedure " + p);
-
- foreach (string v in mayBeInfo[s][p].Keys)
- {
- if (mayBeInfo[s][p][v])
- {
- Console.WriteLine(" " + v + ": may be flattened " + s + " id");
- }
- }
- }
- }
-
- }
-
- }
-}
diff --git a/Source/GPUVerify/MayBeGlobalSizeAnalyser.cs b/Source/GPUVerify/MayBeGlobalSizeAnalyser.cs deleted file mode 100644 index 98e71179..00000000 --- a/Source/GPUVerify/MayBeGlobalSizeAnalyser.cs +++ /dev/null @@ -1,287 +0,0 @@ -using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Diagnostics;
-using Microsoft.Boogie;
-
-namespace GPUVerify
-{
- class MayBeGlobalSizeAnalyser
- {
- private static string[] dimensions = { "x", "y", "z" };
-
- private GPUVerifier verifier;
-
- private bool ProcedureChanged;
-
- private Dictionary<string, Dictionary<string, Dictionary<string, bool>>> mayBeInfo;
-
- public MayBeGlobalSizeAnalyser(GPUVerifier verifier)
- {
- this.verifier = verifier;
-
- mayBeInfo = new Dictionary<string,Dictionary<string,Dictionary<string,bool>>>();
- foreach (string s in dimensions)
- {
- mayBeInfo[s] = new Dictionary<string, Dictionary<string, bool>>();
- }
-
- }
-
- internal void Analyse()
- {
- foreach (Declaration D in verifier.Program.TopLevelDeclarations)
- {
- if(D is Implementation)
- {
- Implementation Impl = D as Implementation;
-
- foreach (string s in dimensions)
- {
- mayBeInfo[s][Impl.Name] = new Dictionary<string, bool>();
- }
-
- foreach (Variable v in Impl.LocVars)
- {
- foreach (string s in dimensions)
- {
- SetMayBe(s, Impl.Name, v.Name);
- }
- }
-
- foreach (Variable v in Impl.InParams)
- {
- foreach (string s in dimensions)
- {
- SetMayBe(s, Impl.Name, v.Name);
- }
- }
-
- foreach (Variable v in Impl.OutParams)
- {
- foreach (string s in dimensions)
- {
- SetMayBe(s, Impl.Name, v.Name);
- }
- }
-
- ProcedureChanged = true;
- }
- }
-
- while (ProcedureChanged)
- {
- ProcedureChanged = false;
-
- foreach (Declaration D in verifier.Program.TopLevelDeclarations)
- {
- if (D is Implementation)
- {
- Implementation Impl = D as Implementation;
- Analyse(Impl);
- }
- }
- }
-
- if (CommandLineOptions.ShowMayBeThreadConfigurationVariableAnalysis)
- {
- dump();
- }
- }
-
- private void Analyse(Implementation Impl)
- {
- Analyse(Impl, verifier.RootRegion(Impl));
- }
-
- private void Analyse(Implementation impl, IRegion region)
- {
- foreach (Cmd c in region.Cmds())
- {
- if (c is AssignCmd)
- {
- foreach (string s in dimensions)
- {
- TransferAssign(impl, c as AssignCmd, s);
- }
- }
- else if (c is CallCmd)
- {
- foreach (string s in dimensions)
- {
- TransferCall(impl, c as CallCmd, s);
- }
- }
- else if (c is HavocCmd)
- {
- foreach (string s in dimensions)
- {
- TransferHavoc(impl, c as HavocCmd, s);
- }
- }
- }
- }
-
- private void TransferHavoc(Implementation impl, HavocCmd havoc, string component)
- {
- Debug.Assert(havoc.Vars.Length == 1);
- if (MayBe(component, impl.Name, havoc.Vars[0].Decl.Name))
- {
- SetNot(component, impl.Name, havoc.Vars[0].Decl.Name);
- }
- }
-
- private void TransferCall(Implementation impl, CallCmd callCmd, string component)
- {
- if (callCmd.callee != verifier.BarrierProcedure.Name)
- {
-
- Implementation CalleeImplementation = verifier.GetImplementation(callCmd.callee);
- for (int i = 0; i < CalleeImplementation.InParams.Length; i++)
- {
- if (MayBe(component, callCmd.callee, CalleeImplementation.InParams[i].Name)
- && !MayBe(component, impl.Name, callCmd.Ins[i]))
- {
- SetNot(component, callCmd.callee, CalleeImplementation.InParams[i].Name);
- }
- }
-
- for (int i = 0; i < CalleeImplementation.OutParams.Length; i++)
- {
- if (MayBe(component, impl.Name, callCmd.Outs[i].Name)
- && !MayBe(component, callCmd.callee, CalleeImplementation.OutParams[i].Name))
- {
- SetNot(component, impl.Name, callCmd.Outs[i].Name);
- }
- }
-
- }
- }
-
- private void TransferAssign(Implementation impl, AssignCmd assignCmd, string component)
- {
- for (int i = 0; i != assignCmd.Lhss.Count; ++i)
- {
- if (assignCmd.Lhss[i] is SimpleAssignLhs)
- {
- SimpleAssignLhs lhs = assignCmd.Lhss[i] as SimpleAssignLhs;
- Expr rhs = assignCmd.Rhss[i];
-
- if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)
- && !MayBe(component, impl.Name, rhs))
- {
- SetNot(component, impl.Name, lhs.AssignedVariable.Name);
- }
- }
- }
- }
-
- private void SetNot(string component, string proc, string v)
- {
- mayBeInfo[component][proc][v] = false;
- ProcedureChanged = true;
- }
-
- private void SetMayBe(string component, string proc, string v)
- {
- mayBeInfo[component][proc][v] = true;
- }
-
- internal bool MayBe(string component, string proc, string v)
- {
- if (!mayBeInfo[component].ContainsKey(proc))
- {
- return false;
- }
-
- if (!mayBeInfo[component][proc].ContainsKey(v))
- {
- return false;
- }
-
- return mayBeInfo[component][proc][v];
- }
-
- internal bool MayBe(string component, string proc, Expr e)
- {
- if (e is IdentifierExpr)
- {
- return MayBe(component, proc, (e as IdentifierExpr).Decl.Name);
- }
-
- return IsNumGroupsTimesGroupSize(component, proc, e);
-
- }
-
- private bool IsNumGroupsTimesGroupSize(string component, string proc, Expr expr)
- {
- if (expr is NAryExpr && (expr as NAryExpr).Fun.FunctionName.Equals("BV32_MUL"))
- {
- NAryExpr innerNary = expr as NAryExpr;
-
- if (IsNumGroupsAndGroupSize(component, proc, innerNary.Args[0], innerNary.Args[1]))
- {
- return true;
- }
-
- if (IsNumGroupsAndGroupSize(component, proc, innerNary.Args[1], innerNary.Args[0]))
- {
- return true;
- }
- }
- return false;
- }
-
- private bool IsNumGroupsAndGroupSize(string component, string proc, Expr maybeNumGroups, Expr maybeGroupSize)
- {
- string numGroupsString = null;
- string groupSizeString = null;
- if (component.Equals("x"))
- {
- numGroupsString = GPUVerifier.NUM_GROUPS_X_STRING;
- groupSizeString = GPUVerifier.GROUP_SIZE_X_STRING;
- }
- else if (component.Equals("y"))
- {
- numGroupsString = GPUVerifier.NUM_GROUPS_Y_STRING;
- groupSizeString = GPUVerifier.GROUP_SIZE_Y_STRING;
- }
- else if (component.Equals("z"))
- {
- numGroupsString = GPUVerifier.NUM_GROUPS_Z_STRING;
- groupSizeString = GPUVerifier.GROUP_SIZE_Z_STRING;
- }
- else
- {
- Debug.Assert(false);
- }
-
- return verifier.mayBeTidAnalyser.MayBe(numGroupsString, proc, maybeNumGroups) &&
- verifier.mayBeTidAnalyser.MayBe(groupSizeString, proc, maybeGroupSize);
- }
-
- private void dump()
- {
- foreach (string s in dimensions)
- {
- Console.WriteLine("*** global_size_" + s + " ***");
-
- foreach (string p in mayBeInfo[s].Keys)
- {
- Console.WriteLine(" Procedure " + p);
-
- foreach (string v in mayBeInfo[s][p].Keys)
- {
- if (mayBeInfo[s][p][v])
- {
- Console.WriteLine(" " + v + ": may be global_size_" + s);
- }
- }
- }
- }
-
- }
-
- }
-}
diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs index 3b307e64..5155b192 100644 --- a/Source/GPUVerify/RaceInstrumenterBase.cs +++ b/Source/GPUVerify/RaceInstrumenterBase.cs @@ -452,45 +452,13 @@ namespace GPUVerify private void AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(Implementation impl, IRegion region, Variable v, string accessType)
{
+ var offsets = GetOffsetsAccessed(region, v, accessType)
+ .Select(ofs => verifier.varDefAnalyses[impl].SubstDualisedDefinitions(ofs, 1, impl.Name))
+ .ToList();
- foreach (Expr e in GetOffsetsAccessed(region, v, accessType))
+ if (!offsets.Contains(null))
{
- if (verifier.mayBeTidAnalyser.MayBe(GPUVerifier.LOCAL_ID_X_STRING, impl.Name, GPUVerifier.StripThreadIdentifiers(e)))
- {
- AddAccessedOffsetIsThreadLocalIdCandidateInvariant(region, v, accessType);
- // No point adding it multiple times
- break;
- }
- }
-
- foreach (Expr e in GetOffsetsAccessed(region, v, accessType))
- {
- if (verifier.mayBeGidAnalyser.MayBe("x", impl.Name, GPUVerifier.StripThreadIdentifiers(e)))
- {
- AddAccessedOffsetIsThreadGlobalIdCandidateInvariant(region, v, accessType);
- // No point adding it multiple times
- break;
- }
- }
-
- foreach (Expr e in GetOffsetsAccessed(region, v, accessType))
- {
- if (verifier.mayBeFlattened2DTidOrGidAnalyser.MayBe("local", impl.Name, GPUVerifier.StripThreadIdentifiers(e)))
- {
- AddAccessedOffsetIsThreadFlattened2DLocalIdCandidateInvariant(region, v, accessType);
- // No point adding it multiple times
- break;
- }
- }
-
- foreach (Expr e in GetOffsetsAccessed(region, v, accessType))
- {
- if (verifier.mayBeFlattened2DTidOrGidAnalyser.MayBe("global", impl.Name, GPUVerifier.StripThreadIdentifiers(e)))
- {
- AddAccessedOffsetIsThreadFlattened2DGlobalIdCandidateInvariant(region, v, accessType);
- // No point adding it multiple times
- break;
- }
+ AddAccessedOffsetsAreConstantCandidateInvariant(region, v, offsets, accessType);
}
KeyValuePair<IdentifierExpr, Expr> iLessThanC = GetILessThanC(region.Guard());
@@ -680,18 +648,12 @@ namespace GPUVerify AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "READ", 1);
}
- protected abstract void AddAccessedOffsetIsThreadLocalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite);
-
- protected abstract void AddAccessedOffsetIsThreadGlobalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite);
-
- protected abstract void AddAccessedOffsetIsThreadFlattened2DLocalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite);
-
- protected abstract void AddAccessedOffsetIsThreadFlattened2DGlobalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite);
-
protected abstract void AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite);
protected abstract void AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite);
+ protected abstract void AddAccessedOffsetsAreConstantCandidateInvariant(IRegion region, Variable v, IEnumerable<Expr> offsets, string ReadOrWrite);
+
protected abstract void AddAccessedOffsetIsThreadLocalIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread);
protected abstract void AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, int Thread);
diff --git a/Source/GPUVerify/StructuredRegion.cs b/Source/GPUVerify/StructuredRegion.cs index 815752dd..366682e0 100644 --- a/Source/GPUVerify/StructuredRegion.cs +++ b/Source/GPUVerify/StructuredRegion.cs @@ -7,19 +7,29 @@ using Microsoft.Boogie; namespace GPUVerify {
class StructuredRegion : IRegion {
+ Implementation impl;
WhileCmd cmd;
- StmtList stmts;
+
+ public StructuredRegion(Implementation impl) {
+ this.impl = impl;
+ }
public StructuredRegion(WhileCmd cmd) {
this.cmd = cmd;
}
- public StructuredRegion(StmtList stmts) {
- this.stmts = stmts;
+ public object Identifier() {
+ if (cmd != null)
+ return cmd;
+ else
+ return impl;
}
- public StructuredRegion(Implementation impl) {
- this.stmts = impl.StructuredStmts;
+ private StmtList StmtList() {
+ if (cmd != null)
+ return cmd.Body;
+ else
+ return impl.StructuredStmts;
}
private IEnumerable<Cmd> Cmds(StmtList stmts) {
@@ -84,24 +94,15 @@ class StructuredRegion : IRegion { }
public IEnumerable<Cmd> Cmds() {
- if (cmd != null)
- return Cmds(cmd.Body);
- else
- return Cmds(stmts);
+ return Cmds(StmtList());
}
public IEnumerable<object> CmdsChildRegions() {
- if (cmd != null)
- return CmdsChildRegions(cmd.Body);
- else
- return CmdsChildRegions(stmts);
+ return CmdsChildRegions(StmtList());
}
public IEnumerable<IRegion> SubRegions() {
- if (cmd != null)
- return SubRegions(cmd.Body);
- else
- return SubRegions(stmts);
+ return SubRegions(StmtList());
}
public Expr Guard() {
@@ -117,4 +118,4 @@ class StructuredRegion : IRegion { }
}
-}
\ No newline at end of file +}
diff --git a/Source/GPUVerify/UnstructuredRegion.cs b/Source/GPUVerify/UnstructuredRegion.cs index 607dc6d7..239f7ca0 100644 --- a/Source/GPUVerify/UnstructuredRegion.cs +++ b/Source/GPUVerify/UnstructuredRegion.cs @@ -37,6 +37,10 @@ class UnstructuredRegion : IRegion { guard = null;
}
+ public object Identifier() {
+ return header;
+ }
+
private HashSet<Block> SubBlocks() {
if (header != null) {
return loopNodes[header];
@@ -90,4 +94,4 @@ class UnstructuredRegion : IRegion { }
}
-}
\ No newline at end of file +}
diff --git a/Source/GPUVerify/VariableDefinitionAnalysis.cs b/Source/GPUVerify/VariableDefinitionAnalysis.cs new file mode 100644 index 00000000..f55e51e8 --- /dev/null +++ b/Source/GPUVerify/VariableDefinitionAnalysis.cs @@ -0,0 +1,155 @@ +using System;
+using Microsoft.Boogie;
+using System.Collections.Generic;
+using System.Linq;
+
+namespace GPUVerify {
+
+class VariableDefinitionAnalysis {
+ GPUVerifier verifier;
+ Implementation impl;
+
+ Dictionary<Variable, Expr> defMap = new Dictionary<Variable, Expr>();
+ Dictionary<string, Expr> namedDefMap = new Dictionary<string, Expr>();
+ bool changed;
+
+ VariableDefinitionAnalysis(GPUVerifier v, Implementation i) {
+ verifier = v;
+ impl = i;
+ }
+
+ private class IsConstantVisitor : StandardVisitor {
+ private VariableDefinitionAnalysis analysis;
+ public bool isConstant = true;
+
+ public IsConstantVisitor(VariableDefinitionAnalysis a) {
+ analysis = a;
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr expr) {
+ if (expr.Fun is MapSelect) {
+ isConstant = false;
+ return expr;
+ } else
+ return base.VisitNAryExpr(expr);
+ }
+
+ public override Expr VisitIdentifierExpr(IdentifierExpr expr) {
+ if (expr.Decl is Constant)
+ return expr;
+ if (!analysis.defMap.ContainsKey(expr.Decl) || analysis.defMap[expr.Decl] == null)
+ isConstant = false;
+ return expr;
+ }
+ };
+
+ bool IsConstant(Expr e) {
+ var v = new IsConstantVisitor(this);
+ v.Visit(e);
+ return v.isConstant;
+ }
+
+ void UpdateDefMap(Variable v, Expr def) {
+ if (!defMap.ContainsKey(v) || defMap[v] != def) {
+ changed = true;
+ defMap[v] = def;
+ }
+ }
+
+ void AddAssignment(AssignLhs lhs, Expr rhs) {
+ if (lhs is SimpleAssignLhs) {
+ var sLhs = (SimpleAssignLhs)lhs;
+ var theVar = sLhs.DeepAssignedVariable;
+ if ((defMap.ContainsKey(theVar) && defMap[theVar] != rhs) || !IsConstant(rhs)) {
+ UpdateDefMap(theVar, null);
+ } else {
+ UpdateDefMap(theVar, rhs);
+ }
+ }
+ }
+
+ void Analyse() {
+ do {
+ changed = false;
+ foreach (var c in verifier.RootRegion(impl).Cmds()) {
+ if (c is AssignCmd) {
+ var aCmd = (AssignCmd)c;
+ foreach (var a in aCmd.Lhss.Zip(aCmd.Rhss)) {
+ AddAssignment(a.Item1, a.Item2);
+ }
+ }
+ }
+ } while (changed);
+ }
+
+ private class BuildNamedDefVisitor : StandardVisitor {
+ private VariableDefinitionAnalysis analysis;
+
+ public BuildNamedDefVisitor(VariableDefinitionAnalysis a) {
+ analysis = a;
+ }
+
+ public override Expr VisitIdentifierExpr(IdentifierExpr expr) {
+ if (expr.Decl is Constant)
+ return expr;
+ return analysis.BuildNamedDefFor(expr.Decl);
+ }
+ }
+
+ Expr BuildNamedDefFor(Variable v) {
+ Expr def;
+ if (namedDefMap.TryGetValue(v.Name, out def))
+ return def;
+ def = (Expr)new BuildNamedDefVisitor(this).Visit(defMap[v].Clone());
+ namedDefMap[v.Name] = def;
+ return def;
+ }
+
+ void BuildNamedDefMap() {
+ foreach (var v in defMap.Keys)
+ if (defMap[v] != null)
+ BuildNamedDefFor(v);
+ }
+
+ private class SubstDualisedDefVisitor : StandardVisitor {
+ private VariableDefinitionAnalysis analysis;
+ private VariableDualiser dualiser;
+ public bool isSubstitutable = true;
+
+ public SubstDualisedDefVisitor(VariableDefinitionAnalysis a, int id, string procName) {
+ analysis = a;
+ dualiser = new VariableDualiser(id, analysis.verifier.uniformityAnalyser, procName);
+ }
+
+ public override Expr VisitIdentifierExpr(IdentifierExpr expr) {
+ if (expr.Decl is Constant)
+ return dualiser.VisitIdentifierExpr(expr);
+ var varName = GPUVerifier.StripThreadIdentifier(expr.Decl.Name);
+ Expr def;
+ if (!analysis.namedDefMap.TryGetValue(varName, out def)) {
+ isSubstitutable = false;
+ return null;
+ }
+ return (Expr)dualiser.Visit(def.Clone());
+ }
+ }
+
+ public Expr SubstDualisedDefinitions(Expr e, int id, string procName) {
+ var v = new SubstDualisedDefVisitor(this, id, procName);
+ Expr result = (Expr)v.Visit(e.Clone());
+ if (!v.isSubstitutable)
+ return null;
+ return result;
+ }
+
+ public static VariableDefinitionAnalysis Analyse(GPUVerifier verifier, Implementation impl) {
+ var a = new VariableDefinitionAnalysis(verifier, impl);
+ a.Analyse();
+ a.BuildNamedDefMap();
+ a.defMap = null;
+ return a;
+ }
+
+}
+
+}
diff --git a/Source/GPUVerify/BlockPredicator.cs b/Source/VCGeneration/BlockPredicator.cs index 5e61734d..f4e82182 100644 --- a/Source/GPUVerify/BlockPredicator.cs +++ b/Source/VCGeneration/BlockPredicator.cs @@ -1,19 +1,21 @@ using Graphing; -using Microsoft.Boogie; using System; using System.Collections.Generic; +using System.Diagnostics; using System.Diagnostics.Contracts; using System.Linq; -namespace GPUVerify { +namespace Microsoft.Boogie { -class BlockPredicator { +public class BlockPredicator { - GPUVerifier verifier; Program prog; Implementation impl; Graph<Block> blockGraph; + bool createCandidateInvariants = true; + bool useProcedurePredicates = true; + Expr returnBlockId; LocalVariable curVar, pVar; @@ -24,10 +26,39 @@ class BlockPredicator { Dictionary<Block, Expr> blockIds = new Dictionary<Block, Expr>(); HashSet<Block> doneBlocks = new HashSet<Block>(); - BlockPredicator(GPUVerifier v, Program p, Implementation i) { - verifier = v; + BlockPredicator(Program p, Implementation i, bool cci, bool upp) { prog = p; impl = i; + createCandidateInvariants = cci; + useProcedurePredicates = upp; + } + + void PredicateCmd(List<Block> blocks, Block block, Cmd cmd, out Block nextBlock) { + if (!useProcedurePredicates && cmd is CallCmd) { + var trueBlock = new Block(); + blocks.Add(trueBlock); + trueBlock.Label = block.Label + ".call.true"; + trueBlock.Cmds.Add(new AssumeCmd(Token.NoToken, p)); + trueBlock.Cmds.Add(cmd); + + var falseBlock = new Block(); + blocks.Add(falseBlock); + falseBlock.Label = block.Label + ".call.false"; + falseBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(p))); + + var contBlock = new Block(); + blocks.Add(contBlock); + contBlock.Label = block.Label + ".call.cont"; + + block.TransferCmd = + new GotoCmd(Token.NoToken, new BlockSeq(trueBlock, falseBlock)); + trueBlock.TransferCmd = falseBlock.TransferCmd = + new GotoCmd(Token.NoToken, new BlockSeq(contBlock)); + nextBlock = contBlock; + } else { + PredicateCmd(block.Cmds, cmd); + nextBlock = block; + } } void PredicateCmd(CmdSeq cmdSeq, Cmd cmd) { @@ -79,6 +110,7 @@ class BlockPredicator { new ExprSeq(p, havocTempExpr, v)))); } } else if (cmd is CallCmd) { + Debug.Assert(useProcedurePredicates); var cCmd = (CallCmd)cmd; cCmd.Ins.Insert(0, p); cmdSeq.Add(cCmd); @@ -145,16 +177,16 @@ class BlockPredicator { impl.LocVars.Add(pVar); p = Expr.Ident(pVar); + if (useProcedurePredicates) + fp = Expr.Ident(impl.InParams[0]); + var newBlocks = new List<Block>(); - fp = Expr.Ident(impl.InParams[0]); Block entryBlock = new Block(); entryBlock.Label = "entry"; entryBlock.Cmds = new CmdSeq(Cmd.SimpleAssign(Token.NoToken, cur, - new NAryExpr(Token.NoToken, - new IfThenElse(Token.NoToken), - new ExprSeq(fp, blockIds[sortedBlocks[0].Item1], - returnBlockId)))); + CreateIfFPThenElse(blockIds[sortedBlocks[0].Item1], + returnBlockId))); newBlocks.Add(entryBlock); var prevBlock = entryBlock; @@ -182,22 +214,23 @@ class BlockPredicator { prevBlock = tailBlock; } else { var runBlock = n.Item1; + var oldCmdSeq = runBlock.Cmds; + runBlock.Cmds = new CmdSeq(); newBlocks.Add(runBlock); + prevBlock.TransferCmd = new GotoCmd(Token.NoToken, + new BlockSeq(runBlock)); pExpr = Expr.Eq(cur, blockIds[runBlock]); - CmdSeq newCmdSeq = new CmdSeq(); - AddNonUniformInvariant(newCmdSeq, runBlock); - if (CommandLineOptions.Inference && blockGraph.Headers.Contains(runBlock)) { - AddUniformCandidateInvariant(newCmdSeq, runBlock); + if (createCandidateInvariants && blockGraph.Headers.Contains(runBlock)) { + AddUniformCandidateInvariant(runBlock.Cmds, runBlock); + AddNonUniformCandidateInvariant(runBlock.Cmds, runBlock); } - newCmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, p, pExpr)); - foreach (Cmd cmd in runBlock.Cmds) - PredicateCmd(newCmdSeq, cmd); - PredicateTransferCmd(newCmdSeq, runBlock.TransferCmd); - runBlock.Cmds = newCmdSeq; + runBlock.Cmds.Add(Cmd.SimpleAssign(Token.NoToken, p, pExpr)); + var transferCmd = runBlock.TransferCmd; + foreach (Cmd cmd in oldCmdSeq) + PredicateCmd(newBlocks, runBlock, cmd, out runBlock); + PredicateTransferCmd(runBlock.Cmds, transferCmd); - prevBlock.TransferCmd = new GotoCmd(Token.NoToken, - new BlockSeq(runBlock)); prevBlock = runBlock; doneBlocks.Add(runBlock); } @@ -207,15 +240,23 @@ class BlockPredicator { impl.Blocks = newBlocks; } - private void AddUniformCandidateInvariant(CmdSeq cs, Block header) { - cs.Add(verifier.CreateCandidateInvariant(Expr.Eq(cur, - new NAryExpr(Token.NoToken, + private Expr CreateIfFPThenElse(Expr then, Expr eElse) { + if (useProcedurePredicates) { + return new NAryExpr(Token.NoToken, new IfThenElse(Token.NoToken), - new ExprSeq(fp, blockIds[header], returnBlockId))), - "uniform loop")); + new ExprSeq(fp, then, eElse)); + } else { + return then; + } + } + + private void AddUniformCandidateInvariant(CmdSeq cs, Block header) { + cs.Add(prog.CreateCandidateInvariant(Expr.Eq(cur, + CreateIfFPThenElse(blockIds[header], returnBlockId)), + "uniform loop")); } - private void AddNonUniformInvariant(CmdSeq cs, Block header) { + private void AddNonUniformCandidateInvariant(CmdSeq cs, Block header) { var loopNodes = new HashSet<Block>(); foreach (var b in blockGraph.BackEdgeNodes(header)) loopNodes.UnionWith(blockGraph.NaturalLoops(header, b)); @@ -232,14 +273,16 @@ class BlockPredicator { } var curIsHeaderOrExit = exits.Aggregate((Expr)Expr.Eq(cur, blockIds[header]), (e, exit) => Expr.Or(e, Expr.Eq(cur, exit))); - cs.Add(new AssertCmd(Token.NoToken, new NAryExpr(Token.NoToken, - new IfThenElse(Token.NoToken), - new ExprSeq(fp, curIsHeaderOrExit, Expr.Eq(cur, returnBlockId))))); + cs.Add(prog.CreateCandidateInvariant( + CreateIfFPThenElse(curIsHeaderOrExit, Expr.Eq(cur, returnBlockId)), + "non-uniform loop")); } - public static void Predicate(GPUVerifier v, Program p) { + public static void Predicate(Program p, + bool createCandidateInvariants = true, + bool useProcedurePredicates = true) { foreach (var decl in p.TopLevelDeclarations.ToList()) { - if (decl is DeclWithFormals && !(decl is Function)) { + if (useProcedurePredicates && decl is DeclWithFormals && !(decl is Function)) { var dwf = (DeclWithFormals)decl; var fpVar = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "_P", @@ -251,7 +294,7 @@ class BlockPredicator { } var impl = decl as Implementation; if (impl != null) - new BlockPredicator(v, p, impl).PredicateImplementation(); + new BlockPredicator(p, impl, createCandidateInvariants, useProcedurePredicates).PredicateImplementation(); } } diff --git a/Source/GPUVerify/GraphAlgorithms.cs b/Source/VCGeneration/GraphAlgorithms.cs index 3442a64d..def77485 100644..100755 --- a/Source/GPUVerify/GraphAlgorithms.cs +++ b/Source/VCGeneration/GraphAlgorithms.cs @@ -4,7 +4,7 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; -namespace GPUVerify { +namespace Microsoft.Boogie { public static class GraphAlgorithms { diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj index 5b2541a9..39da0be6 100644 --- a/Source/VCGeneration/VCGeneration.csproj +++ b/Source/VCGeneration/VCGeneration.csproj @@ -144,6 +144,7 @@ <Reference Include="System.Xml" />
</ItemGroup>
<ItemGroup>
+ <Compile Include="BlockPredicator.cs" />
<Compile Include="Check.cs" />
<Compile Include="ConditionGeneration.cs" />
<Compile Include="Context.cs" />
@@ -151,6 +152,7 @@ <Compile Include="DoomedLoopUnrolling.cs" />
<Compile Include="DoomedStrategy.cs" />
<Compile Include="DoomErrorHandler.cs" />
+ <Compile Include="GraphAlgorithms.cs" />
<Compile Include="HasseDiagram.cs" />
<Compile Include="OrderingAxioms.cs" />
<Compile Include="StratifiedVC.cs" />
|