diff options
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 9 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerify.csproj | 1 | ||||
| -rw-r--r-- | Source/GPUVerify/LiveVariableAnalyser.cs | 124 |
3 files changed, 133 insertions, 1 deletions
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 070095ea..d41cead0 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -66,6 +66,7 @@ namespace GPUVerify public UniformityAnalyser uniformityAnalyser;
public MayBeTidAnalyser mayBeTidAnalyser;
public MayBePowerOfTwoAnalyser mayBePowerOfTwoAnalyser;
+ public LiveVariableAnalyser liveVariableAnalyser;
public GPUVerifier(string filename, Program program, IRaceInstrumenter raceInstrumenter) : this(filename, program, raceInstrumenter, false)
{
@@ -302,6 +303,11 @@ namespace GPUVerify internal void doit()
{
+ if (CommandLineOptions.ShowStages)
+ {
+ emitProgram(outputFilename + "_original");
+ }
+
preProcess();
DoLiveVariableAnalysis();
@@ -447,7 +453,8 @@ namespace GPUVerify private void DoLiveVariableAnalysis()
{
- // TODO
+ liveVariableAnalyser = new LiveVariableAnalyser(this);
+ liveVariableAnalyser.Analyse();
}
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index f6353895..d6958414 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -109,6 +109,7 @@ <Compile Include="AsymmetricExpressionFinder.cs" />
<Compile Include="EnsureDisabledThreadHasNoEffectInstrumenter.cs" />
<Compile Include="KernelDualiser.cs" />
+ <Compile Include="LiveVariableAnalyser.cs" />
<Compile Include="LoopInvariantGenerator.cs" />
<Compile Include="MayBePowerOfTwoAnalyser.cs" />
<Compile Include="MayBeTidAnalyser.cs" />
diff --git a/Source/GPUVerify/LiveVariableAnalyser.cs b/Source/GPUVerify/LiveVariableAnalyser.cs new file mode 100644 index 00000000..63542d80 --- /dev/null +++ b/Source/GPUVerify/LiveVariableAnalyser.cs @@ -0,0 +1,124 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics;
+using Microsoft.Boogie;
+
+namespace GPUVerify
+{
+ class LiveVariableAnalyser
+ {
+ private GPUVerifier verifier;
+
+ // Maps procedure -> loop -> set of variables live at the loop head
+ private Dictionary<string, Dictionary<string, HashSet<string>>> liveVariableInfo;
+
+ public LiveVariableAnalyser(GPUVerifier verifier)
+ {
+ this.verifier = verifier;
+ this.liveVariableInfo = new Dictionary<string, Dictionary<string, HashSet<string>>>();
+ }
+
+ internal void Analyse()
+ {
+ foreach (Declaration D in verifier.Program.TopLevelDeclarations)
+ {
+ if (D is Implementation)
+ {
+ Implementation impl = D as Implementation;
+
+ liveVariableInfo[impl.Name] = new Dictionary<string, HashSet<string>>();
+
+ LiveVariableAnalysis.ComputeLiveVariables(impl);
+
+ Analyse(impl.StructuredStmts, impl);
+
+ }
+ }
+ }
+
+ private void Analyse(StmtList stmtList, Implementation impl)
+ {
+ foreach (BigBlock bb in stmtList.BigBlocks)
+ {
+ Analyse(bb, impl);
+ }
+ }
+
+ private void Analyse(BigBlock bb, Implementation impl)
+ {
+ if (bb.ec is WhileCmd)
+ {
+ WhileCmd wc = bb.ec as WhileCmd;
+
+ Debug.Assert(wc.Invariants.Count >= 1);
+
+ string wcLabel = wc.Invariants[0].Attributes.Key;
+
+ Debug.Assert (wcLabel.Contains("loophead_"));
+
+ liveVariableInfo[impl.Name][wcLabel] = new HashSet<string>();
+
+ Block wcStartBlock = GetBlockForWhile(wc, impl);
+
+ Debug.Assert(wcStartBlock != null);
+
+// Debug.Assert(wcStartBlock.liveVarsBefore != null);
+
+ if (wcStartBlock.liveVarsBefore == null)
+ {
+ Console.WriteLine("live before is null for " + wcLabel);
+ }
+ else
+ {
+ Console.WriteLine("live before is non-null for " + wcLabel);
+ foreach (Variable v in impl.LocVars)
+ {
+ if (wcStartBlock.IsLive(v))
+ {
+ liveVariableInfo[impl.Name][wcLabel].Add(v.Name);
+ }
+ }
+ }
+
+ Analyse(wc.Body, impl);
+ }
+ else if (bb.ec is IfCmd)
+ {
+ Analyse((bb.ec as IfCmd).thn, impl);
+ if ((bb.ec as IfCmd).elseBlock != null)
+ {
+ Analyse((bb.ec as IfCmd).elseBlock, impl);
+ }
+ Debug.Assert((bb.ec as IfCmd).elseIf == null);
+ }
+
+ }
+
+ private Block GetBlockForWhile(WhileCmd wc, Implementation impl)
+ {
+ string whileLoopIdentifier =
+ wc.Invariants[0].Attributes.Key;
+
+ foreach (Block b in impl.Blocks)
+ {
+ if (b.Cmds.Length > 0 && b.Cmds[0] is AssertCmd)
+ {
+ AssertCmd ass = b.Cmds[0] as AssertCmd;
+ if (ass.Attributes != null)
+ {
+ if (ass.Attributes.Key.Equals(whileLoopIdentifier))
+ {
+ return b;
+ }
+ }
+ }
+ }
+
+ Debug.Assert(false);
+
+ return null;
+ }
+ }
+}
|