diff options
| -rw-r--r-- | Source/GPUVerify/ArrayControlFlowAnalyser.cs | 14 | ||||
| -rw-r--r-- | Source/GPUVerify/BarrierInvariantDescriptor.cs | 37 | ||||
| -rw-r--r-- | Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs | 62 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 25 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerify.csproj | 345 | ||||
| -rw-r--r-- | Source/GPUVerify/KernelDualiser.cs | 159 | ||||
| -rw-r--r-- | Source/GPUVerify/UnaryBarrierInvariantDescriptor.cs | 49 | ||||
| -rw-r--r-- | Source/GPUVerify/VariableDualiser.cs | 14 |
8 files changed, 512 insertions, 193 deletions
diff --git a/Source/GPUVerify/ArrayControlFlowAnalyser.cs b/Source/GPUVerify/ArrayControlFlowAnalyser.cs index 649d76d7..8e52b9ef 100644 --- a/Source/GPUVerify/ArrayControlFlowAnalyser.cs +++ b/Source/GPUVerify/ArrayControlFlowAnalyser.cs @@ -172,10 +172,12 @@ namespace GPUVerify {
CallCmd callCmd = c as CallCmd;
- if (callCmd.callee != verifier.BarrierProcedure.Name &&
- callCmd.callee != verifier.BarrierInvariantProcedure.Name &&
- callCmd.callee != verifier.BarrierInvariantInstantiationProcedure.Name)
- {
+ if (QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "barrier_invariant") ||
+ QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "binary_barrier_invariant")) {
+ foreach (Expr param in callCmd.Ins) {
+ ExprMayAffectControlFlow(impl, param);
+ }
+ } else if(callCmd.callee != verifier.BarrierProcedure.Name) {
Implementation CalleeImplementation = verifier.GetImplementation(callCmd.callee);
for (int i = 0; i < CalleeImplementation.InParams.Length; i++)
@@ -220,6 +222,10 @@ namespace GPUVerify var assumeCmd = c as AssumeCmd;
ExprMayAffectControlFlow(impl, assumeCmd.Expr);
}
+ else if (c is AssertCmd) {
+ var assertCmd = c as AssertCmd;
+ ExprMayAffectControlFlow(impl, assertCmd.Expr);
+ }
}
}
diff --git a/Source/GPUVerify/BarrierInvariantDescriptor.cs b/Source/GPUVerify/BarrierInvariantDescriptor.cs new file mode 100644 index 00000000..a8320b18 --- /dev/null +++ b/Source/GPUVerify/BarrierInvariantDescriptor.cs @@ -0,0 +1,37 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics;
+using Microsoft.Boogie;
+
+namespace GPUVerify {
+ abstract class BarrierInvariantDescriptor {
+
+ protected Expr Predicate;
+ protected Expr BarrierInvariant;
+ protected KernelDualiser Dualiser;
+
+ public BarrierInvariantDescriptor(Expr Predicate, Expr BarrierInvariant, KernelDualiser Dualiser) {
+ this.Predicate = Predicate;
+ this.BarrierInvariant = BarrierInvariant;
+ this.Dualiser = Dualiser;
+ }
+
+ internal abstract AssertCmd GetAssertCmd(QKeyValue Attributes);
+
+ internal abstract List<AssumeCmd> GetInstantiationCmds();
+
+ protected Expr NonNegative(Expr e) {
+ return Dualiser.verifier.MakeBVSge(
+ e, GPUVerifier.ZeroBV());
+ }
+
+ protected Expr NotTooLarge(Expr e) {
+ return Dualiser.verifier.MakeBVSlt(e,
+ new IdentifierExpr(Token.NoToken,
+ Dualiser.verifier.GetGroupSize("X")));
+ }
+
+ }
+}
diff --git a/Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs b/Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs new file mode 100644 index 00000000..df84cae8 --- /dev/null +++ b/Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs @@ -0,0 +1,62 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+
+namespace GPUVerify {
+ class BinaryBarrierInvariantDescriptor : BarrierInvariantDescriptor {
+
+ private List<Tuple<Expr, Expr>> InstantiationExprPairs;
+
+ public BinaryBarrierInvariantDescriptor(Expr Predicate, Expr BarrierInvariant, KernelDualiser Dualiser) :
+ base(Predicate, BarrierInvariant, Dualiser) {
+ InstantiationExprPairs = new List<Tuple<Expr, Expr>>();
+ }
+
+ public void AddInstantiationExprPair(Expr first, Expr second) {
+ InstantiationExprPairs.Add(new Tuple<Expr, Expr>(first, second));
+ }
+
+ internal override AssertCmd GetAssertCmd(QKeyValue Attributes) {
+ var vd = new VariableDualiser(1, null, null);
+ return new AssertCmd(
+ Token.NoToken,
+ Expr.Imp(GPUVerifier.ThreadsInSameGroup(),
+ vd.VisitExpr(Expr.Imp(Predicate, BarrierInvariant))),
+ Dualiser.MakeThreadSpecificAttributes(Attributes, 1));
+ }
+
+ internal override List<AssumeCmd> GetInstantiationCmds() {
+ var result = new List<AssumeCmd>();
+ foreach (var Instantiation in InstantiationExprPairs) {
+ foreach (var Thread in new int[] { 1, 2 }) {
+
+ var vd = new VariableDualiser(Thread, null, null);
+
+ var ThreadInstantiationExpr = vd.VisitExpr(Instantiation.Item1);
+ var OtherThreadInstantiationExpr = vd.VisitExpr(Instantiation.Item2);
+
+ var ti = new ThreadPairInstantiator(Dualiser.verifier, ThreadInstantiationExpr, OtherThreadInstantiationExpr, Thread);
+
+ result.Add(new AssumeCmd(
+ Token.NoToken,
+ Expr.Imp(vd.VisitExpr(Predicate),
+ Expr.Imp(
+ Expr.And(
+ Expr.And(
+ Expr.And(NonNegative(ThreadInstantiationExpr),
+ NotTooLarge(ThreadInstantiationExpr)),
+ Expr.And(NonNegative(OtherThreadInstantiationExpr),
+ NotTooLarge(OtherThreadInstantiationExpr))
+ ),
+ Expr.Neq(ThreadInstantiationExpr, OtherThreadInstantiationExpr)),
+ ti.VisitExpr(BarrierInvariant)))));
+ }
+ }
+ return result;
+ }
+
+
+ }
+}
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 85821da2..94c460fe 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -19,8 +19,6 @@ namespace GPUVerify public Procedure KernelProcedure; public Implementation KernelImplementation; public Procedure BarrierProcedure;
- public Procedure BarrierInvariantProcedure;
- public Procedure BarrierInvariantInstantiationProcedure; public IKernelArrayInfo KernelArrayInfo = new KernelArrayInfoLists(); @@ -1766,7 +1764,13 @@ namespace GPUVerify if (c is CallCmd) { - CallCmd call = c as CallCmd; + CallCmd call = c as CallCmd;
+
+ if (QKeyValue.FindBoolAttribute(call.Proc.Attributes, "barrier_invariant") ||
+ QKeyValue.FindBoolAttribute(call.Proc.Attributes, "binary_barrier_invariant")) {
+ // Do not pull non-local accesses out of barrier invariants
+ continue;
+ } List<Expr> newIns = new List<Expr>(); @@ -1822,7 +1826,8 @@ namespace GPUVerify } else if (c is AssertCmd) { - // Do not pull non-local accesses out of assert commands + // Do not pull non-local accesses out of assert commands
+ continue; } else if (c is AssumeCmd) { @@ -1903,8 +1908,10 @@ namespace GPUVerify List<Declaration> NewTopLevelDeclarations = new List<Declaration>(); - foreach (Declaration d in Program.TopLevelDeclarations) - { + for(int i = 0; i < Program.TopLevelDeclarations.Count; i++) + {
+ Declaration d = Program.TopLevelDeclarations[i]; + if (d is Procedure) { @@ -2040,8 +2047,6 @@ namespace GPUVerify private int Check() { BarrierProcedure = FindOrCreateBarrierProcedure();
- BarrierInvariantProcedure = FindOrCreateBarrierInvariantProcedure();
- BarrierInvariantInstantiationProcedure = FindOrCreateBarrierInvariantInstantiationProcedure();
KernelProcedure = CheckExactlyOneKernelProcedure(); if (ErrorCount > 0) @@ -2267,6 +2272,10 @@ namespace GPUVerify return (expr.Decl is Constant) || (expr.Decl is Formal && ((Formal)expr.Decl).InComing); } + + internal static Expr GroupSharedIndexingExpr(int Thread) {
+ return Thread == 1 ? Expr.True : ThreadsInSameGroup();
+ }
} diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index e7122edf..2bcc5b15 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -1,178 +1,181 @@ -<?xml version="1.0" encoding="utf-8"?> -<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003"> - <PropertyGroup> - <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration> - <Platform Condition=" '$(Platform)' == '' ">x86</Platform> - <ProductVersion>8.0.30703</ProductVersion> - <SchemaVersion>2.0</SchemaVersion> - <ProjectGuid>{E5D16606-06D0-434F-A9D7-7D079BC80229}</ProjectGuid> - <OutputType>Exe</OutputType> - <AppDesignerFolder>Properties</AppDesignerFolder> - <RootNamespace>GPUVerify</RootNamespace> - <AssemblyName>GPUVerifyVCGen</AssemblyName> - <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> - <TargetFrameworkProfile>Client</TargetFrameworkProfile> - <FileAlignment>512</FileAlignment> - <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode> - </PropertyGroup> - <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|x86' "> - <PlatformTarget>x86</PlatformTarget> - <DebugSymbols>true</DebugSymbols> - <DebugType>full</DebugType> - <Optimize>false</Optimize> - <OutputPath>bin\Debug\</OutputPath> - <DefineConstants>DEBUG;TRACE</DefineConstants> - <ErrorReport>prompt</ErrorReport> - <WarningLevel>4</WarningLevel> - <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking> - <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface> - <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure> - <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires> - <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers> - <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis> - <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations> - <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations> - <CodeContractsArithmeticObligations>True</CodeContractsArithmeticObligations> - <CodeContractsEnumObligations>False</CodeContractsEnumObligations> - <CodeContractsPointerObligations>False</CodeContractsPointerObligations> - <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions> - <CodeContractsRunInBackground>True</CodeContractsRunInBackground> - <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies> - <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine> - <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs> - <CodeContractsCustomRewriterAssembly /> - <CodeContractsCustomRewriterClass /> - <CodeContractsLibPaths /> - <CodeContractsExtraRewriteOptions /> - <CodeContractsExtraAnalysisOptions /> - <CodeContractsBaseLineFile /> - <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults> - <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel> - <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly> - <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel> - <CodeContractsAnalysisPrecisionLevel>0</CodeContractsAnalysisPrecisionLevel> - </PropertyGroup> - <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' "> - <PlatformTarget>x86</PlatformTarget> - <DebugType>pdbonly</DebugType> - <Optimize>true</Optimize> - <OutputPath>bin\Release\</OutputPath> - <DefineConstants>TRACE</DefineConstants> - <ErrorReport>prompt</ErrorReport> - <WarningLevel>4</WarningLevel> - </PropertyGroup> - <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|AnyCPU'"> - <DebugSymbols>true</DebugSymbols> - <OutputPath>bin\Debug\</OutputPath> - <DefineConstants>DEBUG;TRACE</DefineConstants> - <DebugType>full</DebugType> - <PlatformTarget>AnyCPU</PlatformTarget> - <CodeAnalysisLogFile>bin\Debug\GPUVerify.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile> - <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression> - <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile> - <ErrorReport>prompt</ErrorReport> - <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet> - <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories> - <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets> - <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories> - <CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules> - <CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules> - </PropertyGroup> - <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|AnyCPU'"> - <OutputPath>bin\Release\</OutputPath> - <DefineConstants>TRACE</DefineConstants> - <Optimize>true</Optimize> - <DebugType>pdbonly</DebugType> - <PlatformTarget>AnyCPU</PlatformTarget> - <CodeAnalysisLogFile>bin\Release\GPUVerify.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile> - <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression> - <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile> - <ErrorReport>prompt</ErrorReport> - <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet> - <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories> - <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories> - </PropertyGroup> - <ItemGroup> - <Reference Include="System" /> - <Reference Include="System.Core" /> - <Reference Include="System.Windows.Forms" /> - <Reference Include="System.Xml.Linq" /> - <Reference Include="System.Data.DataSetExtensions" /> - <Reference Include="Microsoft.CSharp" /> - <Reference Include="System.Data" /> - <Reference Include="System.Xml" /> - </ItemGroup> - <ItemGroup> - <Compile Include="AccessCollector.cs" /> - <Compile Include="AccessRecord.cs" /> - <Compile Include="AdversarialAbstraction.cs" /> - <Compile Include="ArrayControlFlowAnalyser.cs" /> - <Compile Include="AsymmetricExpressionFinder.cs" /> - <Compile Include="StrideConstraint.cs" /> - <Compile Include="ReducedStrengthAnalysis.cs" /> - <Compile Include="UnstructuredRegion.cs" /> - <Compile Include="IRegion.cs" /> - <Compile Include="InvariantGenerationRules\LoopVariableBoundsInvariantGenerator.cs" /> - <Compile Include="InvariantGenerationRules\InvariantGenerationRule.cs" /> - <Compile Include="InvariantGenerationRules\PowerOfTwoInvariantGenerator.cs" /> - <Compile Include="EnsureDisabledThreadHasNoEffectInstrumenter.cs" /> - <Compile Include="KernelDualiser.cs" /> - <Compile Include="LiveVariableAnalyser.cs" /> - <Compile Include="LoopInvariantGenerator.cs" /> - <Compile Include="MayBePowerOfTwoAnalyser.cs" /> - <Compile Include="StructuredProgramVisitor.cs" /> - <Compile Include="EnabledToPredicateVisitor.cs" /> - <Compile Include="CommandLineOptions.cs" /> - <Compile Include="GPUVerifier.cs" /> - <Compile Include="IKernelArrayInfo.cs" /> - <Compile Include="IRaceInstrumenter.cs" /> - <Compile Include="Main.cs" /> - <Compile Include="NonLocalAccessCollector.cs" /> - <Compile Include="NonLocalAccessExtractor.cs" /> - <Compile Include="KernelArrayInfoLists.cs" /> - <Compile Include="NullRaceInstrumenter.cs" /> - <Compile Include="Predicator.cs" /> - <Compile Include="Properties\AssemblyInfo.cs" /> - <Compile Include="RaceInstrumenter.cs" /> - <Compile Include="ReadCollector.cs" /> - <Compile Include="VariableDualiser.cs" /> - <Compile Include="VariablesOccurringInExpressionVisitor.cs" /> - <Compile Include="VariableDefinitionAnalysis.cs" /> - <Compile Include="StructuredRegion.cs" /> - <Compile Include="WriteCollector.cs" /> - </ItemGroup> - <ItemGroup> - <ProjectReference Include="..\AIFramework\AIFramework.csproj"> - <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project> - <Name>AIFramework</Name> - </ProjectReference> - <ProjectReference Include="..\Basetypes\Basetypes.csproj"> - <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project> - <Name>Basetypes</Name> - </ProjectReference> - <ProjectReference Include="..\Core\Core.csproj"> - <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project> - <Name>Core</Name> - </ProjectReference> - <ProjectReference Include="..\Graph\Graph.csproj"> - <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project> - <Name>Graph</Name> - </ProjectReference> - <ProjectReference Include="..\ParserHelper\ParserHelper.csproj"> - <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" /> +<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+ <PropertyGroup>
+ <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+ <Platform Condition=" '$(Platform)' == '' ">x86</Platform>
+ <ProductVersion>8.0.30703</ProductVersion>
+ <SchemaVersion>2.0</SchemaVersion>
+ <ProjectGuid>{E5D16606-06D0-434F-A9D7-7D079BC80229}</ProjectGuid>
+ <OutputType>Exe</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>GPUVerify</RootNamespace>
+ <AssemblyName>GPUVerifyVCGen</AssemblyName>
+ <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
+ <TargetFrameworkProfile>Client</TargetFrameworkProfile>
+ <FileAlignment>512</FileAlignment>
+ <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|x86' ">
+ <PlatformTarget>x86</PlatformTarget>
+ <DebugSymbols>true</DebugSymbols>
+ <DebugType>full</DebugType>
+ <Optimize>false</Optimize>
+ <OutputPath>bin\Debug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>True</CodeContractsArithmeticObligations>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly />
+ <CodeContractsCustomRewriterClass />
+ <CodeContractsLibPaths />
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsExtraAnalysisOptions />
+ <CodeContractsBaseLineFile />
+ <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ <CodeContractsAnalysisPrecisionLevel>0</CodeContractsAnalysisPrecisionLevel>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">
+ <PlatformTarget>x86</PlatformTarget>
+ <DebugType>pdbonly</DebugType>
+ <Optimize>true</Optimize>
+ <OutputPath>bin\Release\</OutputPath>
+ <DefineConstants>TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|AnyCPU'">
+ <DebugSymbols>true</DebugSymbols>
+ <OutputPath>bin\Debug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <DebugType>full</DebugType>
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <CodeAnalysisLogFile>bin\Debug\GPUVerify.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>
+ <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ <CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules>
+ <CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|AnyCPU'">
+ <OutputPath>bin\Release\</OutputPath>
+ <DefineConstants>TRACE</DefineConstants>
+ <Optimize>true</Optimize>
+ <DebugType>pdbonly</DebugType>
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <CodeAnalysisLogFile>bin\Release\GPUVerify.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ </PropertyGroup>
+ <ItemGroup>
+ <Reference Include="System" />
+ <Reference Include="System.Core" />
+ <Reference Include="System.Windows.Forms" />
+ <Reference Include="System.Xml.Linq" />
+ <Reference Include="System.Data.DataSetExtensions" />
+ <Reference Include="Microsoft.CSharp" />
+ <Reference Include="System.Data" />
+ <Reference Include="System.Xml" />
+ </ItemGroup>
+ <ItemGroup>
+ <Compile Include="AccessCollector.cs" />
+ <Compile Include="AccessRecord.cs" />
+ <Compile Include="AdversarialAbstraction.cs" />
+ <Compile Include="ArrayControlFlowAnalyser.cs" />
+ <Compile Include="AsymmetricExpressionFinder.cs" />
+ <Compile Include="BarrierInvariantDescriptor.cs" />
+ <Compile Include="BinaryBarrierInvariantDescriptor.cs" />
+ <Compile Include="StrideConstraint.cs" />
+ <Compile Include="ReducedStrengthAnalysis.cs" />
+ <Compile Include="UnaryBarrierInvariantDescriptor.cs" />
+ <Compile Include="UnstructuredRegion.cs" />
+ <Compile Include="IRegion.cs" />
+ <Compile Include="InvariantGenerationRules\LoopVariableBoundsInvariantGenerator.cs" />
+ <Compile Include="InvariantGenerationRules\InvariantGenerationRule.cs" />
+ <Compile Include="InvariantGenerationRules\PowerOfTwoInvariantGenerator.cs" />
+ <Compile Include="EnsureDisabledThreadHasNoEffectInstrumenter.cs" />
+ <Compile Include="KernelDualiser.cs" />
+ <Compile Include="LiveVariableAnalyser.cs" />
+ <Compile Include="LoopInvariantGenerator.cs" />
+ <Compile Include="MayBePowerOfTwoAnalyser.cs" />
+ <Compile Include="StructuredProgramVisitor.cs" />
+ <Compile Include="EnabledToPredicateVisitor.cs" />
+ <Compile Include="CommandLineOptions.cs" />
+ <Compile Include="GPUVerifier.cs" />
+ <Compile Include="IKernelArrayInfo.cs" />
+ <Compile Include="IRaceInstrumenter.cs" />
+ <Compile Include="Main.cs" />
+ <Compile Include="NonLocalAccessCollector.cs" />
+ <Compile Include="NonLocalAccessExtractor.cs" />
+ <Compile Include="KernelArrayInfoLists.cs" />
+ <Compile Include="NullRaceInstrumenter.cs" />
+ <Compile Include="Predicator.cs" />
+ <Compile Include="Properties\AssemblyInfo.cs" />
+ <Compile Include="RaceInstrumenter.cs" />
+ <Compile Include="ReadCollector.cs" />
+ <Compile Include="VariableDualiser.cs" />
+ <Compile Include="VariablesOccurringInExpressionVisitor.cs" />
+ <Compile Include="VariableDefinitionAnalysis.cs" />
+ <Compile Include="StructuredRegion.cs" />
+ <Compile Include="WriteCollector.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <ProjectReference Include="..\AIFramework\AIFramework.csproj">
+ <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project>
+ <Name>AIFramework</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Basetypes\Basetypes.csproj">
+ <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
+ <Name>Basetypes</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Core\Core.csproj">
+ <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
+ <Name>Core</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Graph\Graph.csproj">
+ <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>
+ <Name>Graph</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
+ <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. Other similar extension points exist, see Microsoft.Common.targets. <Target Name="BeforeBuild"> </Target> <Target Name="AfterBuild"> </Target> - --> + -->
</Project>
\ No newline at end of file diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs index 201018bb..526e39a0 100644 --- a/Source/GPUVerify/KernelDualiser.cs +++ b/Source/GPUVerify/KernelDualiser.cs @@ -9,10 +9,13 @@ using Microsoft.Basetypes; namespace GPUVerify {
class KernelDualiser {
- private GPUVerifier verifier;
+ internal GPUVerifier verifier;
+
+ private List<BarrierInvariantDescriptor> BarrierInvariantDescriptors;
public KernelDualiser(GPUVerifier verifier) {
this.verifier = verifier;
+ BarrierInvariantDescriptors = new List<BarrierInvariantDescriptor>();
}
private string procName = null;
@@ -74,7 +77,7 @@ namespace GPUVerify { return result;
}
- private QKeyValue MakeThreadSpecificAttributes(QKeyValue attributes, int Thread) {
+ internal QKeyValue MakeThreadSpecificAttributes(QKeyValue attributes, int Thread) {
if (attributes == null) {
return null;
}
@@ -100,6 +103,41 @@ namespace GPUVerify { if (c is CallCmd) {
CallCmd Call = c as CallCmd;
+ if (QKeyValue.FindBoolAttribute(Call.Proc.Attributes, "barrier_invariant")) {
+ // There should be a predicate, an invariant expression, and at least one instantiation
+ Debug.Assert(Call.Ins.Count >= 3);
+ var BIDescriptor = new UnaryBarrierInvariantDescriptor(Call.Ins[0], + Expr.Neq(Call.Ins[1], + new LiteralExpr(Token.NoToken, BigNum.FromInt(0), 1)), this);
+ for (var i = 2; i < Call.Ins.Count; i++) {
+ BIDescriptor.AddInstantiationExpr(Call.Ins[i]);
+ }
+ BarrierInvariantDescriptors.Add(BIDescriptor);
+ return;
+ }
+
+ if (QKeyValue.FindBoolAttribute(Call.Proc.Attributes, "binary_barrier_invariant")) {
+ // There should be a predicate, an invariant expression, and at least one pair of
+ // instantiation expressions
+ Debug.Assert(Call.Ins.Count >= 4);
+ var BIDescriptor = new BinaryBarrierInvariantDescriptor(Call.Ins[0],
+ Expr.Neq(Call.Ins[1],
+ new LiteralExpr(Token.NoToken, BigNum.FromInt(0), 1)), this);
+ for (var i = 2; i < Call.Ins.Count; i += 2) {
+ BIDescriptor.AddInstantiationExprPair(Call.Ins[i], Call.Ins[i + 1]);
+ }
+ BarrierInvariantDescriptors.Add(BIDescriptor);
+ return;
+ }
+
+
+ if (Call.callee.Equals(verifier.BarrierProcedure.Name)) {
+ // Assert barrier invariants
+ foreach (var BIDescriptor in BarrierInvariantDescriptors) {
+ cs.Add(BIDescriptor.GetAssertCmd(Call.Attributes));
+ }
+ }
+
List<Expr> uniformNewIns = new List<Expr>();
List<Expr> nonUniformNewIns = new List<Expr>();
for (int i = 0; i < Call.Ins.Count; i++) {
@@ -148,6 +186,16 @@ namespace GPUVerify { NewCallCmd.Attributes = Call.Attributes;
cs.Add(NewCallCmd);
+
+ if (Call.callee.Equals(verifier.BarrierProcedure.Name)) {
+ foreach (var BIDescriptor in BarrierInvariantDescriptors) {
+ foreach (var Instantiation in BIDescriptor.GetInstantiationCmds()) {
+ cs.Add(Instantiation);
+ }
+ }
+ BarrierInvariantDescriptors.Clear();
+ }
+
}
else if (c is AssignCmd) {
AssignCmd assign = c as AssignCmd;
@@ -370,4 +418,111 @@ namespace GPUVerify { }
+ class ThreadInstantiator : Duplicator {
+
+ private GPUVerifier verifier;
+ private Expr InstantiationExpr;
+ private int Thread;
+
+ internal ThreadInstantiator(GPUVerifier verifier, Expr InstantiationExpr, int Thread) {
+ this.verifier = verifier;
+ this.InstantiationExpr = InstantiationExpr;
+ this.Thread = Thread;
+ }
+
+ public override Expr VisitIdentifierExpr(IdentifierExpr node) {
+ Debug.Assert(!(node.Decl is Formal));
+
+ if (GPUVerifier.IsThreadLocalIdConstant(node.Decl)) {
+ Debug.Assert(node.Decl.Name.Equals(GPUVerifier._X.Name));
+ return InstantiationExpr.Clone() as Expr;
+ }
+
+ Debug.Assert(node.Decl is Constant ||
+ verifier.KernelArrayInfo.getGroupSharedArrays().Contains(node.Decl) ||
+ verifier.KernelArrayInfo.getGlobalArrays().Contains(node.Decl));
+
+ return base.VisitIdentifierExpr(node);
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr node) {
+ if (node.Fun is MapSelect) {
+ Debug.Assert((node.Fun as MapSelect).Arity == 1);
+ Debug.Assert(node.Args[0] is IdentifierExpr);
+ var v = (node.Args[0] as IdentifierExpr).Decl;
+ if (QKeyValue.FindBoolAttribute(v.Attributes, "group_shared")) {
+ return new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new Expr[] { new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new Expr[] { node.Args[0], GPUVerifier.GroupSharedIndexingExpr(Thread) })), VisitExpr(node.Args[1]) }));
+ }
+ }
+ return base.VisitNAryExpr(node);
+ }
+
+
+ }
+
+
+
+ class ThreadPairInstantiator : Duplicator {
+
+ private GPUVerifier verifier;
+ private Tuple<Expr, Expr> InstantiationExprs;
+ private int Thread;
+
+ internal ThreadPairInstantiator(GPUVerifier verifier, Expr InstantiationExpr1, Expr InstantiationExpr2, int Thread) {
+ this.verifier = verifier;
+ this.InstantiationExprs = new Tuple<Expr, Expr>(InstantiationExpr1, InstantiationExpr2);
+ this.Thread = Thread;
+ }
+
+ public override Expr VisitIdentifierExpr(IdentifierExpr node) {
+ Debug.Assert(!(node.Decl is Formal));
+
+ if (GPUVerifier.IsThreadLocalIdConstant(node.Decl)) {
+ Debug.Assert(node.Decl.Name.Equals(GPUVerifier._X.Name));
+ return InstantiationExprs.Item1.Clone() as Expr;
+ }
+
+ Debug.Assert(node.Decl is Constant ||
+ verifier.KernelArrayInfo.getGroupSharedArrays().Contains(node.Decl) ||
+ verifier.KernelArrayInfo.getGlobalArrays().Contains(node.Decl));
+
+ return base.VisitIdentifierExpr(node);
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr node) {
+ if (node.Fun is MapSelect) {
+ Debug.Assert((node.Fun as MapSelect).Arity == 1);
+ Debug.Assert(node.Args[0] is IdentifierExpr);
+ var v = (node.Args[0] as IdentifierExpr).Decl;
+
+ if (QKeyValue.FindBoolAttribute(v.Attributes, "group_shared")) {
+ return new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new Expr[] { new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new Expr[] { node.Args[0], GPUVerifier.GroupSharedIndexingExpr(Thread) })), VisitExpr(node.Args[1]) }));
+ }
+ }
+
+ if (node.Fun is FunctionCall) {
+ FunctionCall call = node.Fun as FunctionCall;
+
+ // Alternate instantiation order for "other thread" functions.
+ // Note that we do not alternatve the "Thread" field, as we are not switching the
+ // thread for which instantiation is being performed
+ if (VariableDualiser.otherFunctionNames.Contains(call.Func.Name)) {
+ return new ThreadPairInstantiator(verifier, InstantiationExprs.Item2, InstantiationExprs.Item1, Thread)
+ .VisitExpr(node.Args[0]);
+ }
+
+ }
+
+ return base.VisitNAryExpr(node);
+ }
+
+
+ }
+
+
+
}
diff --git a/Source/GPUVerify/UnaryBarrierInvariantDescriptor.cs b/Source/GPUVerify/UnaryBarrierInvariantDescriptor.cs new file mode 100644 index 00000000..ef87750e --- /dev/null +++ b/Source/GPUVerify/UnaryBarrierInvariantDescriptor.cs @@ -0,0 +1,49 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+
+namespace GPUVerify {
+ class UnaryBarrierInvariantDescriptor : BarrierInvariantDescriptor {
+ private List<Expr> InstantiationExprs;
+
+ public UnaryBarrierInvariantDescriptor(Expr Predicate, Expr BarrierInvariant, KernelDualiser Dualiser) :
+ base(Predicate, BarrierInvariant, Dualiser) {
+ InstantiationExprs = new List<Expr>();
+ }
+
+ public void AddInstantiationExpr(Expr InstantiationExpr) {
+ InstantiationExprs.Add(InstantiationExpr);
+ }
+
+ internal override AssertCmd GetAssertCmd(QKeyValue Attributes) {
+ var vd = new VariableDualiser(1, null, null);
+ return new AssertCmd(
+ Token.NoToken,
+ vd.VisitExpr(Expr.Imp(Predicate, BarrierInvariant)),
+ Dualiser.MakeThreadSpecificAttributes(Attributes, 1));
+ }
+
+ internal override List<AssumeCmd> GetInstantiationCmds() {
+ var result = new List<AssumeCmd>();
+ foreach (var Instantiation in InstantiationExprs) {
+ foreach (var Thread in new int[] { 1, 2 }) {
+ var vd = new VariableDualiser(Thread, null, null);
+ var ThreadInstantiationExpr = vd.VisitExpr(Instantiation);
+ var ti = new ThreadInstantiator(Dualiser.verifier, ThreadInstantiationExpr, Thread);
+
+ result.Add(new AssumeCmd(
+ Token.NoToken,
+ Expr.Imp(vd.VisitExpr(Predicate),
+ Expr.Imp(Expr.And(
+ NonNegative(ThreadInstantiationExpr),
+ NotTooLarge(ThreadInstantiationExpr)),
+ ti.VisitExpr(BarrierInvariant)))));
+ }
+ }
+ return result;
+ }
+
+ }
+}
diff --git a/Source/GPUVerify/VariableDualiser.cs b/Source/GPUVerify/VariableDualiser.cs index ce5f78ee..d0b04598 100644 --- a/Source/GPUVerify/VariableDualiser.cs +++ b/Source/GPUVerify/VariableDualiser.cs @@ -10,7 +10,7 @@ namespace GPUVerify {
class VariableDualiser : Duplicator
{
- static HashSet<string> otherFunctionNames =
+ static internal HashSet<string> otherFunctionNames =
new HashSet<string>(new string[] { "__other_bool", "__other_bv32", "__other_arrayId" });
private int id;
@@ -91,15 +91,16 @@ namespace GPUVerify if (QKeyValue.FindBoolAttribute(v.Attributes, "group_shared")) {
return new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
new ExprSeq(new Expr[] { new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
- new ExprSeq(new Expr[] { node.Args[0], GroupSharedIndexingExpr() })), VisitExpr(node.Args[1]) }));
+ new ExprSeq(new Expr[] { node.Args[0], GPUVerifier.GroupSharedIndexingExpr(id) })),
+ VisitExpr(node.Args[1]) }));
}
}
- // Avoid dualisation of certain special builtin functions that are cross-thread
if (node.Fun is FunctionCall)
{
FunctionCall call = node.Fun as FunctionCall;
+ // Alternate dualisation for "other thread" functions
if (otherFunctionNames.Contains(call.Func.Name))
{
Debug.Assert(id == 1 || id == 2);
@@ -119,16 +120,13 @@ namespace GPUVerify var v = node.DeepAssignedVariable;
if(QKeyValue.FindBoolAttribute(v.Attributes, "group_shared")) {
return new MapAssignLhs(Token.NoToken, new MapAssignLhs(Token.NoToken, node.Map,
- new List<Expr>(new Expr[] { GroupSharedIndexingExpr() })), node.Indexes.Select(idx => this.VisitExpr(idx)).ToList());
+ new List<Expr>(new Expr[] { GPUVerifier.GroupSharedIndexingExpr(id) })),
+ node.Indexes.Select(idx => this.VisitExpr(idx)).ToList());
}
return base.VisitMapAssignLhs(node);
}
- private Expr GroupSharedIndexingExpr() {
- return id == 1 ? Expr.True : GPUVerifier.ThreadsInSameGroup();
- }
-
}
}
|