summaryrefslogtreecommitdiff
path: root/Source/Predication
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Predication')
-rw-r--r--Source/Predication/Predication.csproj348
-rw-r--r--Source/Predication/SmartBlockPredicator.cs1274
-rw-r--r--Source/Predication/UniformityAnalyser.cs1082
3 files changed, 1352 insertions, 1352 deletions
diff --git a/Source/Predication/Predication.csproj b/Source/Predication/Predication.csproj
index 382a8aca..1319d7f7 100644
--- a/Source/Predication/Predication.csproj
+++ b/Source/Predication/Predication.csproj
@@ -1,174 +1,174 @@
-<?xml version="1.0" encoding="utf-8"?>
-<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
- <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
- <PropertyGroup>
- <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
- <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
- <ProjectGuid>{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}</ProjectGuid>
- <OutputType>Library</OutputType>
- <AppDesignerFolder>Properties</AppDesignerFolder>
- <RootNamespace>Predication</RootNamespace>
- <AssemblyName>Predication</AssemblyName>
- <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
- <FileAlignment>512</FileAlignment>
- <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>
- <ProductVersion>12.0.0</ProductVersion>
- <SchemaVersion>2.0</SchemaVersion>
- <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
- <DebugSymbols>true</DebugSymbols>
- <DebugType>full</DebugType>
- <Optimize>false</Optimize>
- <OutputPath>bin\Debug\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <ErrorReport>prompt</ErrorReport>
- <WarningLevel>4</WarningLevel>
- <CodeContractsEnableRuntimeChecking>False</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>True</CodeContractsEnumObligations>
- <CodeContractsRedundantAssumptions>True</CodeContractsRedundantAssumptions>
- <CodeContractsAssertsToContractsCheckBox>True</CodeContractsAssertsToContractsCheckBox>
- <CodeContractsRedundantTests>True</CodeContractsRedundantTests>
- <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings>
- <CodeContractsMissingPublicEnsuresAsWarnings>False</CodeContractsMissingPublicEnsuresAsWarnings>
- <CodeContractsInferRequires>True</CodeContractsInferRequires>
- <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
- <CodeContractsInferEnsuresAutoProperties>True</CodeContractsInferEnsuresAutoProperties>
- <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
- <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
- <CodeContractsSuggestAssumptionsForCallees>False</CodeContractsSuggestAssumptionsForCallees>
- <CodeContractsSuggestRequires>False</CodeContractsSuggestRequires>
- <CodeContractsNecessaryEnsures>True</CodeContractsNecessaryEnsures>
- <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
- <CodeContractsSuggestReadonly>True</CodeContractsSuggestReadonly>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly />
- <CodeContractsCustomRewriterClass />
- <CodeContractsLibPaths />
- <CodeContractsExtraRewriteOptions />
- <CodeContractsExtraAnalysisOptions />
- <CodeContractsSQLServerOption />
- <CodeContractsBaseLineFile />
- <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
- <CodeContractsSkipAnalysisIfCannotConnectToCache>False</CodeContractsSkipAnalysisIfCannotConnectToCache>
- <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings>
- <CodeContractsBeingOptimisticOnExternal>True</CodeContractsBeingOptimisticOnExternal>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly>
- <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
- <DebugType>pdbonly</DebugType>
- <Optimize>true</Optimize>
- <OutputPath>bin\Release\</OutputPath>
- <DefineConstants>TRACE</DefineConstants>
- <ErrorReport>prompt</ErrorReport>
- <WarningLevel>4</WarningLevel>
- <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
- <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
- <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
- <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
- <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
- <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
- <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
- <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings>
- <CodeContractsInferRequires>True</CodeContractsInferRequires>
- <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
- <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
- <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
- <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
- <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly />
- <CodeContractsCustomRewriterClass />
- <CodeContractsLibPaths />
- <CodeContractsExtraRewriteOptions />
- <CodeContractsExtraAnalysisOptions />
- <CodeContractsSQLServerOption />
- <CodeContractsBaseLineFile />
- <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
- <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly>
- <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
- </PropertyGroup>
- <PropertyGroup>
- <SignAssembly>true</SignAssembly>
- </PropertyGroup>
- <PropertyGroup>
- <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'QED|AnyCPU'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\QED\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
- </PropertyGroup>
- <ItemGroup>
- <Reference Include="System" />
- <Reference Include="System.Core" />
- <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="SmartBlockPredicator.cs" />
- <Compile Include="UniformityAnalyser.cs" />
- </ItemGroup>
- <ItemGroup>
- <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>
- <ItemGroup>
- <Folder Include="Properties\" />
- </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>
+<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+ <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
+ <PropertyGroup>
+ <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+ <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+ <ProjectGuid>{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}</ProjectGuid>
+ <OutputType>Library</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>Predication</RootNamespace>
+ <AssemblyName>BoogiePredication</AssemblyName>
+ <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
+ <FileAlignment>512</FileAlignment>
+ <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>
+ <ProductVersion>12.0.0</ProductVersion>
+ <SchemaVersion>2.0</SchemaVersion>
+ <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+ <DebugSymbols>true</DebugSymbols>
+ <DebugType>full</DebugType>
+ <Optimize>false</Optimize>
+ <OutputPath>bin\Debug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ <CodeContractsEnableRuntimeChecking>False</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>True</CodeContractsEnumObligations>
+ <CodeContractsRedundantAssumptions>True</CodeContractsRedundantAssumptions>
+ <CodeContractsAssertsToContractsCheckBox>True</CodeContractsAssertsToContractsCheckBox>
+ <CodeContractsRedundantTests>True</CodeContractsRedundantTests>
+ <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings>
+ <CodeContractsMissingPublicEnsuresAsWarnings>False</CodeContractsMissingPublicEnsuresAsWarnings>
+ <CodeContractsInferRequires>True</CodeContractsInferRequires>
+ <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
+ <CodeContractsInferEnsuresAutoProperties>True</CodeContractsInferEnsuresAutoProperties>
+ <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
+ <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
+ <CodeContractsSuggestAssumptionsForCallees>False</CodeContractsSuggestAssumptionsForCallees>
+ <CodeContractsSuggestRequires>False</CodeContractsSuggestRequires>
+ <CodeContractsNecessaryEnsures>True</CodeContractsNecessaryEnsures>
+ <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
+ <CodeContractsSuggestReadonly>True</CodeContractsSuggestReadonly>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly />
+ <CodeContractsCustomRewriterClass />
+ <CodeContractsLibPaths />
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsExtraAnalysisOptions />
+ <CodeContractsSQLServerOption />
+ <CodeContractsBaseLineFile />
+ <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
+ <CodeContractsSkipAnalysisIfCannotConnectToCache>False</CodeContractsSkipAnalysisIfCannotConnectToCache>
+ <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings>
+ <CodeContractsBeingOptimisticOnExternal>True</CodeContractsBeingOptimisticOnExternal>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
+ <DebugType>pdbonly</DebugType>
+ <Optimize>true</Optimize>
+ <OutputPath>bin\Release\</OutputPath>
+ <DefineConstants>TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings>
+ <CodeContractsInferRequires>True</CodeContractsInferRequires>
+ <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
+ <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
+ <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
+ <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
+ <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly />
+ <CodeContractsCustomRewriterClass />
+ <CodeContractsLibPaths />
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsExtraAnalysisOptions />
+ <CodeContractsSQLServerOption />
+ <CodeContractsBaseLineFile />
+ <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
+ <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ </PropertyGroup>
+ <PropertyGroup>
+ <SignAssembly>true</SignAssembly>
+ </PropertyGroup>
+ <PropertyGroup>
+ <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'QED|AnyCPU'">
+ <DebugSymbols>true</DebugSymbols>
+ <OutputPath>bin\QED\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <DebugType>full</DebugType>
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
+ </PropertyGroup>
+ <ItemGroup>
+ <Reference Include="System" />
+ <Reference Include="System.Core" />
+ <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="SmartBlockPredicator.cs" />
+ <Compile Include="UniformityAnalyser.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <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>
+ <ItemGroup>
+ <Folder Include="Properties\" />
+ </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/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs
index 739f0e2b..0f848152 100644
--- a/Source/Predication/SmartBlockPredicator.cs
+++ b/Source/Predication/SmartBlockPredicator.cs
@@ -1,637 +1,637 @@
-using Microsoft.Boogie.GraphUtil;
-using System;
-using System.Collections.Generic;
-using System.Diagnostics;
-using System.Diagnostics.Contracts;
-using System.Linq;
-
-namespace Microsoft.Boogie {
-
-public class SmartBlockPredicator {
-
- Program prog;
- Implementation impl;
- Graph<Block> blockGraph;
- List<Tuple<Block, bool>> sortedBlocks;
-
- Func<Procedure, bool> useProcedurePredicates;
-
- Dictionary<Block, Variable> predMap, defMap;
- Dictionary<Block, HashSet<Variable>> ownedMap;
- Dictionary<Block, Block> parentMap;
- Dictionary<Block, PartInfo> partInfo;
-
- IdentifierExpr fp;
- Dictionary<Microsoft.Boogie.Type, IdentifierExpr> havocVars =
- new Dictionary<Microsoft.Boogie.Type, IdentifierExpr>();
- HashSet<Block> doneBlocks = new HashSet<Block>();
- bool myUseProcedurePredicates;
- UniformityAnalyser uni;
-
- SmartBlockPredicator(Program p, Implementation i, Func<Procedure, bool> upp, UniformityAnalyser u) {
- prog = p;
- impl = i;
- useProcedurePredicates = upp;
- myUseProcedurePredicates = useProcedurePredicates(i.Proc);
- uni = u;
- }
-
- void PredicateCmd(Expr p, Expr pDom, List<Block> blocks, Block block, Cmd cmd, out Block nextBlock) {
- var cCmd = cmd as CallCmd;
- if (cCmd != null && !useProcedurePredicates(cCmd.Proc)) {
- if (p == null) {
- block.Cmds.Add(cmd);
- nextBlock = block;
- return;
- }
-
- 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 List<Block> { trueBlock, falseBlock });
- trueBlock.TransferCmd = falseBlock.TransferCmd =
- new GotoCmd(Token.NoToken, new List<Block> { contBlock });
- nextBlock = contBlock;
- } else {
- PredicateCmd(p, pDom, block.Cmds, cmd);
- nextBlock = block;
- }
- }
-
- void PredicateCmd(Expr p, Expr pDom, List<Cmd> cmdSeq, Cmd cmd) {
- if (cmd is CallCmd) {
- var cCmd = (CallCmd)cmd;
- Debug.Assert(useProcedurePredicates(cCmd.Proc));
- cCmd.Ins.Insert(0, p != null ? p : Expr.True);
- cmdSeq.Add(cCmd);
- } else if (p == null) {
- new EnabledReplacementVisitor(Expr.True, pDom).Visit(cmd);
- cmdSeq.Add(cmd);
- } else if (cmd is AssignCmd) {
- var aCmd = (AssignCmd)cmd;
- cmdSeq.Add(new AssignCmd(Token.NoToken, aCmd.Lhss,
- new List<Expr>(aCmd.Lhss.Zip(aCmd.Rhss, (lhs, rhs) =>
- new NAryExpr(Token.NoToken,
- new IfThenElse(Token.NoToken),
- new List<Expr> { p, rhs, lhs.AsExpr })))));
- } else if (cmd is AssertCmd) {
- var aCmd = (AssertCmd)cmd;
- Expr newExpr = new EnabledReplacementVisitor(p, pDom).VisitExpr(aCmd.Expr);
- aCmd.Expr = QKeyValue.FindBoolAttribute(aCmd.Attributes, "do_not_predicate") ? newExpr : Expr.Imp(p, newExpr);
- cmdSeq.Add(aCmd);
- } else if (cmd is AssumeCmd) {
- var aCmd = (AssumeCmd)cmd;
- Expr newExpr = new EnabledReplacementVisitor(p, pDom).VisitExpr(aCmd.Expr);
- aCmd.Expr = QKeyValue.FindBoolAttribute(aCmd.Attributes, "do_not_predicate") ? newExpr : Expr.Imp(p, newExpr);
- cmdSeq.Add(aCmd);
- } else if (cmd is HavocCmd) {
- var hCmd = (HavocCmd)cmd;
- foreach (IdentifierExpr v in hCmd.Vars) {
- Microsoft.Boogie.Type type = v.Decl.TypedIdent.Type;
- Contract.Assert(type != null);
-
- IdentifierExpr havocTempExpr;
- if (havocVars.ContainsKey(type)) {
- havocTempExpr = havocVars[type];
- } else {
- var havocVar = new LocalVariable(Token.NoToken,
- new TypedIdent(Token.NoToken,
- "_HAVOC_" + type.ToString(), type));
- impl.LocVars.Add(havocVar);
- havocVars[type] = havocTempExpr =
- new IdentifierExpr(Token.NoToken, havocVar);
- }
- cmdSeq.Add(new HavocCmd(Token.NoToken,
- new List<IdentifierExpr> { havocTempExpr }));
- cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,
- new NAryExpr(Token.NoToken,
- new IfThenElse(Token.NoToken),
- new List<Expr> { p, havocTempExpr, v })));
- }
- } else if (cmd is CommentCmd) {
- // skip
- } else if (cmd is StateCmd) {
- var sCmd = (StateCmd)cmd;
- var newCmdSeq = new List<Cmd>();
- foreach (Cmd c in sCmd.Cmds)
- PredicateCmd(p, pDom, newCmdSeq, c);
- sCmd.Cmds = newCmdSeq;
- cmdSeq.Add(sCmd);
- } else {
- Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
- }
- }
-
- // hasPredicatedRegion is true iff the block or its targets are predicated
- // (i.e. we enter, stay within or exit a predicated region).
- void PredicateTransferCmd(Expr p, Block src, List<Cmd> cmdSeq, TransferCmd cmd, out bool hasPredicatedRegion) {
- hasPredicatedRegion = predMap.ContainsKey(src);
-
- if (cmd is GotoCmd) {
- var gCmd = (GotoCmd)cmd;
-
- hasPredicatedRegion = hasPredicatedRegion ||
- gCmd.labelTargets.Cast<Block>().Any(b => predMap.ContainsKey(b));
-
- if (gCmd.labelTargets.Count == 1) {
- if (defMap.ContainsKey(gCmd.labelTargets[0])) {
- PredicateCmd(p, Expr.True, cmdSeq,
- Cmd.SimpleAssign(Token.NoToken,
- Expr.Ident(predMap[gCmd.labelTargets[0]]), Expr.True));
- }
- } else {
- Debug.Assert(gCmd.labelTargets.Count > 1);
- Debug.Assert(gCmd.labelTargets.Cast<Block>().All(t => uni.IsUniform(impl.Name, t) ||
- partInfo.ContainsKey(t)));
- foreach (Block target in gCmd.labelTargets) {
- if (!partInfo.ContainsKey(target))
- continue;
-
- // In this case we not only predicate with the current predicate p,
- // but also with the "part predicate"; this ensures that we do not
- // update a predicate twice when it occurs in both parts.
- var part = partInfo[target];
- if (defMap.ContainsKey(part.realDest)) {
- PredicateCmd(p == null ? part.pred : Expr.And(p, part.pred), Expr.True, cmdSeq,
- Cmd.SimpleAssign(Token.NoToken,
- Expr.Ident(predMap[part.realDest]), part.pred));
- }
- var predsExitingLoop = new Dictionary<Block, List<Expr>>();
- foreach (Block exit in LoopsExited(src, target)) {
- List<Expr> predList;
- if (!predsExitingLoop.ContainsKey(exit))
- predList = predsExitingLoop[exit] = new List<Expr>();
- else
- predList = predsExitingLoop[exit];
- predList.Add(part.pred);
- }
- foreach (var pred in predsExitingLoop) {
- PredicateCmd(p == null ? part.pred : Expr.And(p, part.pred), Expr.True, cmdSeq,
- Cmd.SimpleAssign(Token.NoToken,
- Expr.Ident(predMap[pred.Key]),
- Expr.Not(pred.Value.Aggregate(Expr.Or))));
- }
- }
- }
- } else if (cmd is ReturnCmd) {
- // Blocks which end in a return will never share a predicate with a block
- // which appears after it. Furthermore, such a block cannot be part of a
- // loop. So it is safe to do nothing here.
- } else {
- Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
- }
- }
-
- Variable FreshPredicate(ref int predCount) {
- var pVar = new LocalVariable(Token.NoToken,
- new TypedIdent(Token.NoToken,
- "p" + predCount++,
- Microsoft.Boogie.Type.Bool));
- impl.LocVars.Add(pVar);
- return pVar;
- }
-
- void AssignPredicates(Graph<Block> blockGraph,
- DomRelation<Block> dom,
- DomRelation<Block> pdom,
- IEnumerable<Block> headerDominance,
- IEnumerator<Tuple<Block, bool>> i,
- Variable headPredicate,
- ref int predCount) {
- var header = i.Current.Item1;
- var regionPreds = new List<Tuple<Block, Variable>>();
- var ownedPreds = new HashSet<Variable>();
- ownedMap[header] = ownedPreds;
-
- if (headPredicate != null) {
- predMap[header] = headPredicate;
- defMap[header] = headPredicate;
- regionPreds.Add(new Tuple<Block, Variable>(header, headPredicate));
- }
-
- while (i.MoveNext()) {
- var block = i.Current;
-
- if (block.Item2) {
- if (block.Item1 == header) {
- return;
- }
- }
-
- if (uni != null && uni.IsUniform(impl.Name, block.Item1)) {
- if (blockGraph.Headers.Contains(block.Item1)) {
- parentMap[block.Item1] = header;
- AssignPredicates(blockGraph, dom, pdom, headerDominance, i, headPredicate, ref predCount);
- }
- continue;
- }
-
- if (!block.Item2) {
- if (blockGraph.Headers.Contains(block.Item1)) {
- parentMap[block.Item1] = header;
- var loopPred = FreshPredicate(ref predCount);
- ownedPreds.Add(loopPred);
- AssignPredicates(blockGraph, dom, pdom, headerDominance, i, loopPred, ref predCount);
- } else {
- bool foundExisting = false;
- foreach (var regionPred in regionPreds) {
- if (dom.DominatedBy(block.Item1, regionPred.Item1) &&
- pdom.DominatedBy(regionPred.Item1, block.Item1)) {
- predMap[block.Item1] = regionPred.Item2;
- foundExisting = true;
- break;
- }
- }
- if (!foundExisting) {
- var condPred = FreshPredicate(ref predCount);
- predMap[block.Item1] = condPred;
- defMap[block.Item1] = condPred;
- var headerIterator = headerDominance.GetEnumerator();
- // Add the predicate to the loop header H that dominates the node (if one
- // exists) such that H does not dominate another header which also dominates
- // the node. Since predicates are owned by loop headers (or the program entry
- // node), this is the block 'closest' to block to which we are assigning a
- // that can be made to own the predicate.
- Block node = null;
- while (headerIterator.MoveNext()) {
- var current = headerIterator.Current;
- if (dom.DominatedBy(block.Item1, current)) {
- node = current;
- break;
- }
- }
- if (node != null) {
- ownedMap[node].Add(condPred);
- } else {
- // In this case the header is the program entry node.
- ownedPreds.Add(condPred);
- }
- regionPreds.Add(new Tuple<Block, Variable>(block.Item1, condPred));
- }
- }
- }
- }
- }
-
- void AssignPredicates() {
- DomRelation<Block> dom = blockGraph.DominatorMap;
-
- Graph<Block> dualGraph = blockGraph.Dual(new Block());
- DomRelation<Block> pdom = dualGraph.DominatorMap;
- IEnumerable<Block> headerDominance = blockGraph.SortHeadersByDominance();
-
- var iter = sortedBlocks.GetEnumerator();
- if (!iter.MoveNext()) {
- predMap = defMap = null;
- ownedMap = null;
- return;
- }
-
- int predCount = 0;
- predMap = new Dictionary<Block, Variable>();
- defMap = new Dictionary<Block, Variable>();
- ownedMap = new Dictionary<Block, HashSet<Variable>>();
- parentMap = new Dictionary<Block, Block>();
- AssignPredicates(blockGraph, dom, pdom, headerDominance, iter,
- myUseProcedurePredicates ? impl.InParams[0] : null,
- ref predCount);
- }
-
- IEnumerable<Block> LoopsExited(Block src, Block dest) {
- var i = sortedBlocks.GetEnumerator();
- while (i.MoveNext()) {
- var b = i.Current;
- if (b.Item1 == src) {
- return LoopsExitedForwardEdge(dest, i);
- } else if (b.Item1 == dest) {
- return LoopsExitedBackEdge(src, i);
- }
- }
- Debug.Assert(false);
- return null;
- }
-
- private IEnumerable<Block> LoopsExitedBackEdge(Block src, IEnumerator<Tuple<Block, bool>> i) {
- var headsSeen = new HashSet<Block>();
- while (i.MoveNext()) {
- var b = i.Current;
- if (!b.Item2 && blockGraph.Headers.Contains(b.Item1))
- headsSeen.Add(b.Item1);
- else if (b.Item2)
- headsSeen.Remove(b.Item1);
- if (b.Item1 == src)
- return headsSeen;
- }
- Debug.Assert(false);
- return null;
- }
-
- private IEnumerable<Block> LoopsExitedForwardEdge(Block dest, IEnumerator<Tuple<Block, bool>> i) {
- var headsSeen = new HashSet<Block>();
- while (i.MoveNext()) {
- var b = i.Current;
- if (b.Item1 == dest)
- yield break;
- else if (!b.Item2 && blockGraph.Headers.Contains(b.Item1))
- headsSeen.Add(b.Item1);
- else if (b.Item2 && !headsSeen.Contains(b.Item1))
- yield return b.Item1;
- }
- Debug.Assert(false);
- }
-
- class PartInfo {
- public PartInfo(Expr p, Block r) { pred = p; realDest = r; }
- public Expr pred;
- public Block realDest;
- }
-
- Dictionary<Block, PartInfo> BuildPartitionInfo() {
- var partInfo = new Dictionary<Block, PartInfo>();
- foreach (var block in blockGraph.Nodes) {
- if (uni.IsUniform(impl.Name, block))
- continue;
-
- var parts = block.Cmds.Cast<Cmd>().TakeWhile(
- c => c is AssumeCmd &&
- QKeyValue.FindBoolAttribute(((AssumeCmd)c).Attributes, "partition"));
-
- Expr pred = null;
- if (parts.Count() > 0) {
- pred = parts.Select(a => ((AssumeCmd)a).Expr).Aggregate(Expr.And);
- block.Cmds =
- new List<Cmd>(block.Cmds.Cast<Cmd>().Skip(parts.Count()).ToArray());
- } else {
- continue;
- }
-
- Block realDest = block;
- if (block.Cmds.Count == 0) {
- var gc = block.TransferCmd as GotoCmd;
- if (gc != null && gc.labelTargets.Count == 1)
- realDest = gc.labelTargets[0];
- }
- partInfo[block] = new PartInfo(pred, realDest);
- }
-
- return partInfo;
- }
-
- Block FindImmediateDominator(Block block) {
- Block predecessor = null;
- foreach(var pred in blockGraph.Predecessors(block)) {
- if (!blockGraph.DominatorMap.DominatedBy(pred, block)) {
- if (predecessor == null)
- predecessor = pred;
- else
- predecessor = blockGraph.DominatorMap.LeastCommonAncestor(pred, predecessor);
- }
- }
- return predecessor;
- }
-
- void PredicateImplementation() {
- blockGraph = prog.ProcessLoops(impl);
- sortedBlocks = blockGraph.LoopyTopSort();
-
- AssignPredicates();
- partInfo = BuildPartitionInfo();
-
- if (myUseProcedurePredicates)
- fp = Expr.Ident(impl.InParams[0]);
-
- var newBlocks = new List<Block>();
- Block prevBlock = null;
- foreach (var n in sortedBlocks) {
- if (predMap.ContainsKey(n.Item1)) {
- var p = predMap[n.Item1];
- var pExpr = Expr.Ident(p);
-
- if (n.Item2) {
- var dominator = FindImmediateDominator(n.Item1);
- if (dominator != null && predMap.ContainsKey(dominator)) {
- AssumeCmd aCmd = new AssumeCmd(Token.NoToken, Expr.True);
- aCmd.Attributes = new QKeyValue(Token.NoToken, "dominator_predicate", new List<object>() { predMap[dominator].ToString() }, aCmd.Attributes);
- aCmd.Attributes = new QKeyValue(Token.NoToken, "predicate", new List<object>() { predMap[n.Item1].ToString() }, aCmd.Attributes);
- n.Item1.Cmds.Insert(0, aCmd);
- }
-
- var backedgeBlock = new Block();
- newBlocks.Add(backedgeBlock);
-
- backedgeBlock.Label = n.Item1.Label + ".backedge";
- backedgeBlock.Cmds = new List<Cmd> { new AssumeCmd(Token.NoToken, pExpr,
- new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)) };
- backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken,
- new List<Block> { n.Item1 });
-
- var tailBlock = new Block();
- newBlocks.Add(tailBlock);
-
- tailBlock.Label = n.Item1.Label + ".tail";
- tailBlock.Cmds = new List<Cmd> { new AssumeCmd(Token.NoToken,
- Expr.Not(pExpr)) };
-
- if (uni != null && !uni.IsUniform(impl.Name, n.Item1)) {
- uni.AddNonUniform(impl.Name, backedgeBlock);
- uni.AddNonUniform(impl.Name, tailBlock);
- }
-
- if (prevBlock != null)
- prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
- new List<Block> { backedgeBlock, tailBlock });
- prevBlock = tailBlock;
- } else {
- PredicateBlock(pExpr, n.Item1, newBlocks, ref prevBlock);
- }
- } else {
- if (!n.Item2) {
- PredicateBlock(null, n.Item1, newBlocks, ref prevBlock);
- }
- }
- }
-
- if (prevBlock != null)
- prevBlock.TransferCmd = new ReturnCmd(Token.NoToken);
-
- impl.Blocks = newBlocks;
- }
-
- private void PredicateBlock(Expr pExpr, Block block, List<Block> newBlocks, ref Block prevBlock) {
- var firstBlock = block;
-
- var oldCmdSeq = block.Cmds;
- block.Cmds = new List<Cmd>();
- newBlocks.Add(block);
- if (prevBlock != null && !((prevBlock.TransferCmd is ReturnCmd) && uni != null && uni.IsUniform(impl.Name, block))) {
- prevBlock.TransferCmd = new GotoCmd(Token.NoToken, new List<Block> { block });
- }
-
- Block currentBlock = block;
- Expr pCurrentExpr = pExpr;
- while (parentMap.ContainsKey(currentBlock)) {
- Block parent = parentMap[currentBlock];
- Expr pParentExpr = null;
- if (predMap.ContainsKey(parent)) {
- var parentPred = predMap[parent];
- if (parentPred != null) {
- pParentExpr = Expr.Ident(parentPred);
- block.Cmds.Add(new AssertCmd(Token.NoToken,
- pCurrentExpr != null ? (Expr)Expr.Imp(pCurrentExpr, pParentExpr)
- : pParentExpr));
- }
- }
- currentBlock = parent;
- pCurrentExpr = pParentExpr;
- }
-
- Block dominator = FindImmediateDominator(block);
- Expr pDomExpr = Expr.True;
- if (dominator != null && predMap.ContainsKey(dominator))
- pDomExpr = new IdentifierExpr(Token.NoToken, predMap[dominator]);
- var transferCmd = block.TransferCmd;
- foreach (Cmd cmd in oldCmdSeq)
- PredicateCmd(pExpr, pDomExpr, newBlocks, block, cmd, out block);
-
- if (ownedMap.ContainsKey(firstBlock)) {
- var owned = ownedMap[firstBlock];
- foreach (var v in owned)
- block.Cmds.Add(Cmd.SimpleAssign(Token.NoToken, Expr.Ident(v), Expr.False));
- }
-
- bool hasPredicatedRegion;
- PredicateTransferCmd(pExpr, block, block.Cmds, transferCmd, out hasPredicatedRegion);
-
- if (hasPredicatedRegion)
- prevBlock = block;
- else
- prevBlock = null;
-
- doneBlocks.Add(block);
- }
-
- private Expr CreateIfFPThenElse(Expr then, Expr eElse) {
- if (myUseProcedurePredicates) {
- return new NAryExpr(Token.NoToken,
- new IfThenElse(Token.NoToken),
- new List<Expr> { fp, then, eElse });
- } else {
- return then;
- }
- }
-
- public static void Predicate(Program p,
- Func<Procedure, bool> useProcedurePredicates = null,
- UniformityAnalyser uni = null) {
- useProcedurePredicates = useProcedurePredicates ?? (proc => false);
- if (uni != null) {
- var oldUPP = useProcedurePredicates;
- useProcedurePredicates = proc => oldUPP(proc) && !uni.IsUniform(proc.Name);
- }
-
- foreach (var decl in p.TopLevelDeclarations.ToList()) {
- if (decl is Procedure || decl is Implementation) {
- var proc = decl as Procedure;
- Implementation impl = null;
- if (proc == null) {
- impl = (Implementation)decl;
- proc = impl.Proc;
- }
-
- bool upp = useProcedurePredicates(proc);
- if (upp) {
- var dwf = (DeclWithFormals)decl;
- var fpVar = new Formal(Token.NoToken,
- new TypedIdent(Token.NoToken, "_P",
- Microsoft.Boogie.Type.Bool),
- /*incoming=*/true);
- dwf.InParams = new List<Variable>(
- (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))
- .ToArray());
-
- if (impl == null) {
- var fpIdentifierExpr = new IdentifierExpr(Token.NoToken, fpVar);
- foreach (Requires r in proc.Requires) {
- new EnabledReplacementVisitor(fpIdentifierExpr, Expr.True).VisitExpr(r.Condition);
- if (!QKeyValue.FindBoolAttribute(r.Attributes, "do_not_predicate")) {
- r.Condition = Expr.Imp(fpIdentifierExpr, r.Condition);
- }
- }
- foreach (Ensures e in proc.Ensures) {
- new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar), Expr.True).VisitExpr(e.Condition);
- if (!QKeyValue.FindBoolAttribute(e.Attributes, "do_not_predicate")) {
- e.Condition = Expr.Imp(fpIdentifierExpr, e.Condition);
- }
- }
- }
- } else {
- if (impl == null) {
- foreach (Requires r in proc.Requires) {
- new EnabledReplacementVisitor(Expr.True, Expr.True).VisitExpr(r.Condition);
- }
- foreach (Ensures e in proc.Ensures) {
- new EnabledReplacementVisitor(Expr.True, Expr.True).VisitExpr(e.Condition);
- }
- }
- }
-
- if (impl != null) {
- try {
- new SmartBlockPredicator(p, impl, useProcedurePredicates, uni).PredicateImplementation();
- } catch (Program.IrreducibleLoopException) { }
- }
- }
- }
- }
-
- public static void Predicate(Program p, Implementation impl) {
- try {
- new SmartBlockPredicator(p, impl, proc => false, null).PredicateImplementation();
- }
- catch (Program.IrreducibleLoopException) { }
- }
-
-}
-
-class EnabledReplacementVisitor : StandardVisitor
-{
- private Expr pExpr;
- private Expr pDomExpr;
-
- internal EnabledReplacementVisitor(Expr pExpr, Expr pDomExpr)
- {
- this.pExpr = pExpr;
- this.pDomExpr = pDomExpr;
- }
-
- public override Expr VisitExpr(Expr node)
- {
- if (node is IdentifierExpr)
- {
- IdentifierExpr iExpr = node as IdentifierExpr;
- if (iExpr.Decl is Constant && QKeyValue.FindBoolAttribute(iExpr.Decl.Attributes, "__enabled"))
- {
- return pExpr;
- } else if (iExpr.Decl is Constant && QKeyValue.FindBoolAttribute(iExpr.Decl.Attributes, "__dominator_enabled"))
- {
- return pDomExpr;
- }
- }
- return base.VisitExpr(node);
- }
-}
-
-}
+using Microsoft.Boogie.GraphUtil;
+using System;
+using System.Collections.Generic;
+using System.Diagnostics;
+using System.Diagnostics.Contracts;
+using System.Linq;
+
+namespace Microsoft.Boogie {
+
+public class SmartBlockPredicator {
+
+ Program prog;
+ Implementation impl;
+ Graph<Block> blockGraph;
+ List<Tuple<Block, bool>> sortedBlocks;
+
+ Func<Procedure, bool> useProcedurePredicates;
+
+ Dictionary<Block, Variable> predMap, defMap;
+ Dictionary<Block, HashSet<Variable>> ownedMap;
+ Dictionary<Block, Block> parentMap;
+ Dictionary<Block, PartInfo> partInfo;
+
+ IdentifierExpr fp;
+ Dictionary<Microsoft.Boogie.Type, IdentifierExpr> havocVars =
+ new Dictionary<Microsoft.Boogie.Type, IdentifierExpr>();
+ HashSet<Block> doneBlocks = new HashSet<Block>();
+ bool myUseProcedurePredicates;
+ UniformityAnalyser uni;
+
+ SmartBlockPredicator(Program p, Implementation i, Func<Procedure, bool> upp, UniformityAnalyser u) {
+ prog = p;
+ impl = i;
+ useProcedurePredicates = upp;
+ myUseProcedurePredicates = useProcedurePredicates(i.Proc);
+ uni = u;
+ }
+
+ void PredicateCmd(Expr p, Expr pDom, List<Block> blocks, Block block, Cmd cmd, out Block nextBlock) {
+ var cCmd = cmd as CallCmd;
+ if (cCmd != null && !useProcedurePredicates(cCmd.Proc)) {
+ if (p == null) {
+ block.Cmds.Add(cmd);
+ nextBlock = block;
+ return;
+ }
+
+ 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 List<Block> { trueBlock, falseBlock });
+ trueBlock.TransferCmd = falseBlock.TransferCmd =
+ new GotoCmd(Token.NoToken, new List<Block> { contBlock });
+ nextBlock = contBlock;
+ } else {
+ PredicateCmd(p, pDom, block.Cmds, cmd);
+ nextBlock = block;
+ }
+ }
+
+ void PredicateCmd(Expr p, Expr pDom, List<Cmd> cmdSeq, Cmd cmd) {
+ if (cmd is CallCmd) {
+ var cCmd = (CallCmd)cmd;
+ Debug.Assert(useProcedurePredicates(cCmd.Proc));
+ cCmd.Ins.Insert(0, p != null ? p : Expr.True);
+ cmdSeq.Add(cCmd);
+ } else if (p == null) {
+ new EnabledReplacementVisitor(Expr.True, pDom).Visit(cmd);
+ cmdSeq.Add(cmd);
+ } else if (cmd is AssignCmd) {
+ var aCmd = (AssignCmd)cmd;
+ cmdSeq.Add(new AssignCmd(Token.NoToken, aCmd.Lhss,
+ new List<Expr>(aCmd.Lhss.Zip(aCmd.Rhss, (lhs, rhs) =>
+ new NAryExpr(Token.NoToken,
+ new IfThenElse(Token.NoToken),
+ new List<Expr> { p, rhs, lhs.AsExpr })))));
+ } else if (cmd is AssertCmd) {
+ var aCmd = (AssertCmd)cmd;
+ Expr newExpr = new EnabledReplacementVisitor(p, pDom).VisitExpr(aCmd.Expr);
+ aCmd.Expr = QKeyValue.FindBoolAttribute(aCmd.Attributes, "do_not_predicate") ? newExpr : Expr.Imp(p, newExpr);
+ cmdSeq.Add(aCmd);
+ } else if (cmd is AssumeCmd) {
+ var aCmd = (AssumeCmd)cmd;
+ Expr newExpr = new EnabledReplacementVisitor(p, pDom).VisitExpr(aCmd.Expr);
+ aCmd.Expr = QKeyValue.FindBoolAttribute(aCmd.Attributes, "do_not_predicate") ? newExpr : Expr.Imp(p, newExpr);
+ cmdSeq.Add(aCmd);
+ } else if (cmd is HavocCmd) {
+ var hCmd = (HavocCmd)cmd;
+ foreach (IdentifierExpr v in hCmd.Vars) {
+ Microsoft.Boogie.Type type = v.Decl.TypedIdent.Type;
+ Contract.Assert(type != null);
+
+ IdentifierExpr havocTempExpr;
+ if (havocVars.ContainsKey(type)) {
+ havocTempExpr = havocVars[type];
+ } else {
+ var havocVar = new LocalVariable(Token.NoToken,
+ new TypedIdent(Token.NoToken,
+ "_HAVOC_" + type.ToString(), type));
+ impl.LocVars.Add(havocVar);
+ havocVars[type] = havocTempExpr =
+ new IdentifierExpr(Token.NoToken, havocVar);
+ }
+ cmdSeq.Add(new HavocCmd(Token.NoToken,
+ new List<IdentifierExpr> { havocTempExpr }));
+ cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,
+ new NAryExpr(Token.NoToken,
+ new IfThenElse(Token.NoToken),
+ new List<Expr> { p, havocTempExpr, v })));
+ }
+ } else if (cmd is CommentCmd) {
+ // skip
+ } else if (cmd is StateCmd) {
+ var sCmd = (StateCmd)cmd;
+ var newCmdSeq = new List<Cmd>();
+ foreach (Cmd c in sCmd.Cmds)
+ PredicateCmd(p, pDom, newCmdSeq, c);
+ sCmd.Cmds = newCmdSeq;
+ cmdSeq.Add(sCmd);
+ } else {
+ Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
+ }
+ }
+
+ // hasPredicatedRegion is true iff the block or its targets are predicated
+ // (i.e. we enter, stay within or exit a predicated region).
+ void PredicateTransferCmd(Expr p, Block src, List<Cmd> cmdSeq, TransferCmd cmd, out bool hasPredicatedRegion) {
+ hasPredicatedRegion = predMap.ContainsKey(src);
+
+ if (cmd is GotoCmd) {
+ var gCmd = (GotoCmd)cmd;
+
+ hasPredicatedRegion = hasPredicatedRegion ||
+ gCmd.labelTargets.Cast<Block>().Any(b => predMap.ContainsKey(b));
+
+ if (gCmd.labelTargets.Count == 1) {
+ if (defMap.ContainsKey(gCmd.labelTargets[0])) {
+ PredicateCmd(p, Expr.True, cmdSeq,
+ Cmd.SimpleAssign(Token.NoToken,
+ Expr.Ident(predMap[gCmd.labelTargets[0]]), Expr.True));
+ }
+ } else {
+ Debug.Assert(gCmd.labelTargets.Count > 1);
+ Debug.Assert(gCmd.labelTargets.Cast<Block>().All(t => uni.IsUniform(impl.Name, t) ||
+ partInfo.ContainsKey(t)));
+ foreach (Block target in gCmd.labelTargets) {
+ if (!partInfo.ContainsKey(target))
+ continue;
+
+ // In this case we not only predicate with the current predicate p,
+ // but also with the "part predicate"; this ensures that we do not
+ // update a predicate twice when it occurs in both parts.
+ var part = partInfo[target];
+ if (defMap.ContainsKey(part.realDest)) {
+ PredicateCmd(p == null ? part.pred : Expr.And(p, part.pred), Expr.True, cmdSeq,
+ Cmd.SimpleAssign(Token.NoToken,
+ Expr.Ident(predMap[part.realDest]), part.pred));
+ }
+ var predsExitingLoop = new Dictionary<Block, List<Expr>>();
+ foreach (Block exit in LoopsExited(src, target)) {
+ List<Expr> predList;
+ if (!predsExitingLoop.ContainsKey(exit))
+ predList = predsExitingLoop[exit] = new List<Expr>();
+ else
+ predList = predsExitingLoop[exit];
+ predList.Add(part.pred);
+ }
+ foreach (var pred in predsExitingLoop) {
+ PredicateCmd(p == null ? part.pred : Expr.And(p, part.pred), Expr.True, cmdSeq,
+ Cmd.SimpleAssign(Token.NoToken,
+ Expr.Ident(predMap[pred.Key]),
+ Expr.Not(pred.Value.Aggregate(Expr.Or))));
+ }
+ }
+ }
+ } else if (cmd is ReturnCmd) {
+ // Blocks which end in a return will never share a predicate with a block
+ // which appears after it. Furthermore, such a block cannot be part of a
+ // loop. So it is safe to do nothing here.
+ } else {
+ Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
+ }
+ }
+
+ Variable FreshPredicate(ref int predCount) {
+ var pVar = new LocalVariable(Token.NoToken,
+ new TypedIdent(Token.NoToken,
+ "p" + predCount++,
+ Microsoft.Boogie.Type.Bool));
+ impl.LocVars.Add(pVar);
+ return pVar;
+ }
+
+ void AssignPredicates(Graph<Block> blockGraph,
+ DomRelation<Block> dom,
+ DomRelation<Block> pdom,
+ IEnumerable<Block> headerDominance,
+ IEnumerator<Tuple<Block, bool>> i,
+ Variable headPredicate,
+ ref int predCount) {
+ var header = i.Current.Item1;
+ var regionPreds = new List<Tuple<Block, Variable>>();
+ var ownedPreds = new HashSet<Variable>();
+ ownedMap[header] = ownedPreds;
+
+ if (headPredicate != null) {
+ predMap[header] = headPredicate;
+ defMap[header] = headPredicate;
+ regionPreds.Add(new Tuple<Block, Variable>(header, headPredicate));
+ }
+
+ while (i.MoveNext()) {
+ var block = i.Current;
+
+ if (block.Item2) {
+ if (block.Item1 == header) {
+ return;
+ }
+ }
+
+ if (uni != null && uni.IsUniform(impl.Name, block.Item1)) {
+ if (blockGraph.Headers.Contains(block.Item1)) {
+ parentMap[block.Item1] = header;
+ AssignPredicates(blockGraph, dom, pdom, headerDominance, i, headPredicate, ref predCount);
+ }
+ continue;
+ }
+
+ if (!block.Item2) {
+ if (blockGraph.Headers.Contains(block.Item1)) {
+ parentMap[block.Item1] = header;
+ var loopPred = FreshPredicate(ref predCount);
+ ownedPreds.Add(loopPred);
+ AssignPredicates(blockGraph, dom, pdom, headerDominance, i, loopPred, ref predCount);
+ } else {
+ bool foundExisting = false;
+ foreach (var regionPred in regionPreds) {
+ if (dom.DominatedBy(block.Item1, regionPred.Item1) &&
+ pdom.DominatedBy(regionPred.Item1, block.Item1)) {
+ predMap[block.Item1] = regionPred.Item2;
+ foundExisting = true;
+ break;
+ }
+ }
+ if (!foundExisting) {
+ var condPred = FreshPredicate(ref predCount);
+ predMap[block.Item1] = condPred;
+ defMap[block.Item1] = condPred;
+ var headerIterator = headerDominance.GetEnumerator();
+ // Add the predicate to the loop header H that dominates the node (if one
+ // exists) such that H does not dominate another header which also dominates
+ // the node. Since predicates are owned by loop headers (or the program entry
+ // node), this is the block 'closest' to block to which we are assigning a
+ // that can be made to own the predicate.
+ Block node = null;
+ while (headerIterator.MoveNext()) {
+ var current = headerIterator.Current;
+ if (dom.DominatedBy(block.Item1, current)) {
+ node = current;
+ break;
+ }
+ }
+ if (node != null) {
+ ownedMap[node].Add(condPred);
+ } else {
+ // In this case the header is the program entry node.
+ ownedPreds.Add(condPred);
+ }
+ regionPreds.Add(new Tuple<Block, Variable>(block.Item1, condPred));
+ }
+ }
+ }
+ }
+ }
+
+ void AssignPredicates() {
+ DomRelation<Block> dom = blockGraph.DominatorMap;
+
+ Graph<Block> dualGraph = blockGraph.Dual(new Block());
+ DomRelation<Block> pdom = dualGraph.DominatorMap;
+ IEnumerable<Block> headerDominance = blockGraph.SortHeadersByDominance();
+
+ var iter = sortedBlocks.GetEnumerator();
+ if (!iter.MoveNext()) {
+ predMap = defMap = null;
+ ownedMap = null;
+ return;
+ }
+
+ int predCount = 0;
+ predMap = new Dictionary<Block, Variable>();
+ defMap = new Dictionary<Block, Variable>();
+ ownedMap = new Dictionary<Block, HashSet<Variable>>();
+ parentMap = new Dictionary<Block, Block>();
+ AssignPredicates(blockGraph, dom, pdom, headerDominance, iter,
+ myUseProcedurePredicates ? impl.InParams[0] : null,
+ ref predCount);
+ }
+
+ IEnumerable<Block> LoopsExited(Block src, Block dest) {
+ var i = sortedBlocks.GetEnumerator();
+ while (i.MoveNext()) {
+ var b = i.Current;
+ if (b.Item1 == src) {
+ return LoopsExitedForwardEdge(dest, i);
+ } else if (b.Item1 == dest) {
+ return LoopsExitedBackEdge(src, i);
+ }
+ }
+ Debug.Assert(false);
+ return null;
+ }
+
+ private IEnumerable<Block> LoopsExitedBackEdge(Block src, IEnumerator<Tuple<Block, bool>> i) {
+ var headsSeen = new HashSet<Block>();
+ while (i.MoveNext()) {
+ var b = i.Current;
+ if (!b.Item2 && blockGraph.Headers.Contains(b.Item1))
+ headsSeen.Add(b.Item1);
+ else if (b.Item2)
+ headsSeen.Remove(b.Item1);
+ if (b.Item1 == src)
+ return headsSeen;
+ }
+ Debug.Assert(false);
+ return null;
+ }
+
+ private IEnumerable<Block> LoopsExitedForwardEdge(Block dest, IEnumerator<Tuple<Block, bool>> i) {
+ var headsSeen = new HashSet<Block>();
+ while (i.MoveNext()) {
+ var b = i.Current;
+ if (b.Item1 == dest)
+ yield break;
+ else if (!b.Item2 && blockGraph.Headers.Contains(b.Item1))
+ headsSeen.Add(b.Item1);
+ else if (b.Item2 && !headsSeen.Contains(b.Item1))
+ yield return b.Item1;
+ }
+ Debug.Assert(false);
+ }
+
+ class PartInfo {
+ public PartInfo(Expr p, Block r) { pred = p; realDest = r; }
+ public Expr pred;
+ public Block realDest;
+ }
+
+ Dictionary<Block, PartInfo> BuildPartitionInfo() {
+ var partInfo = new Dictionary<Block, PartInfo>();
+ foreach (var block in blockGraph.Nodes) {
+ if (uni.IsUniform(impl.Name, block))
+ continue;
+
+ var parts = block.Cmds.Cast<Cmd>().TakeWhile(
+ c => c is AssumeCmd &&
+ QKeyValue.FindBoolAttribute(((AssumeCmd)c).Attributes, "partition"));
+
+ Expr pred = null;
+ if (parts.Count() > 0) {
+ pred = parts.Select(a => ((AssumeCmd)a).Expr).Aggregate(Expr.And);
+ block.Cmds =
+ new List<Cmd>(block.Cmds.Cast<Cmd>().Skip(parts.Count()).ToArray());
+ } else {
+ continue;
+ }
+
+ Block realDest = block;
+ if (block.Cmds.Count == 0) {
+ var gc = block.TransferCmd as GotoCmd;
+ if (gc != null && gc.labelTargets.Count == 1)
+ realDest = gc.labelTargets[0];
+ }
+ partInfo[block] = new PartInfo(pred, realDest);
+ }
+
+ return partInfo;
+ }
+
+ Block FindImmediateDominator(Block block) {
+ Block predecessor = null;
+ foreach(var pred in blockGraph.Predecessors(block)) {
+ if (!blockGraph.DominatorMap.DominatedBy(pred, block)) {
+ if (predecessor == null)
+ predecessor = pred;
+ else
+ predecessor = blockGraph.DominatorMap.LeastCommonAncestor(pred, predecessor);
+ }
+ }
+ return predecessor;
+ }
+
+ void PredicateImplementation() {
+ blockGraph = prog.ProcessLoops(impl);
+ sortedBlocks = blockGraph.LoopyTopSort();
+
+ AssignPredicates();
+ partInfo = BuildPartitionInfo();
+
+ if (myUseProcedurePredicates)
+ fp = Expr.Ident(impl.InParams[0]);
+
+ var newBlocks = new List<Block>();
+ Block prevBlock = null;
+ foreach (var n in sortedBlocks) {
+ if (predMap.ContainsKey(n.Item1)) {
+ var p = predMap[n.Item1];
+ var pExpr = Expr.Ident(p);
+
+ if (n.Item2) {
+ var dominator = FindImmediateDominator(n.Item1);
+ if (dominator != null && predMap.ContainsKey(dominator)) {
+ AssumeCmd aCmd = new AssumeCmd(Token.NoToken, Expr.True);
+ aCmd.Attributes = new QKeyValue(Token.NoToken, "dominator_predicate", new List<object>() { predMap[dominator].ToString() }, aCmd.Attributes);
+ aCmd.Attributes = new QKeyValue(Token.NoToken, "predicate", new List<object>() { predMap[n.Item1].ToString() }, aCmd.Attributes);
+ n.Item1.Cmds.Insert(0, aCmd);
+ }
+
+ var backedgeBlock = new Block();
+ newBlocks.Add(backedgeBlock);
+
+ backedgeBlock.Label = n.Item1.Label + ".backedge";
+ backedgeBlock.Cmds = new List<Cmd> { new AssumeCmd(Token.NoToken, pExpr,
+ new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)) };
+ backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken,
+ new List<Block> { n.Item1 });
+
+ var tailBlock = new Block();
+ newBlocks.Add(tailBlock);
+
+ tailBlock.Label = n.Item1.Label + ".tail";
+ tailBlock.Cmds = new List<Cmd> { new AssumeCmd(Token.NoToken,
+ Expr.Not(pExpr)) };
+
+ if (uni != null && !uni.IsUniform(impl.Name, n.Item1)) {
+ uni.AddNonUniform(impl.Name, backedgeBlock);
+ uni.AddNonUniform(impl.Name, tailBlock);
+ }
+
+ if (prevBlock != null)
+ prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
+ new List<Block> { backedgeBlock, tailBlock });
+ prevBlock = tailBlock;
+ } else {
+ PredicateBlock(pExpr, n.Item1, newBlocks, ref prevBlock);
+ }
+ } else {
+ if (!n.Item2) {
+ PredicateBlock(null, n.Item1, newBlocks, ref prevBlock);
+ }
+ }
+ }
+
+ if (prevBlock != null)
+ prevBlock.TransferCmd = new ReturnCmd(Token.NoToken);
+
+ impl.Blocks = newBlocks;
+ }
+
+ private void PredicateBlock(Expr pExpr, Block block, List<Block> newBlocks, ref Block prevBlock) {
+ var firstBlock = block;
+
+ var oldCmdSeq = block.Cmds;
+ block.Cmds = new List<Cmd>();
+ newBlocks.Add(block);
+ if (prevBlock != null && !((prevBlock.TransferCmd is ReturnCmd) && uni != null && uni.IsUniform(impl.Name, block))) {
+ prevBlock.TransferCmd = new GotoCmd(Token.NoToken, new List<Block> { block });
+ }
+
+ Block currentBlock = block;
+ Expr pCurrentExpr = pExpr;
+ while (parentMap.ContainsKey(currentBlock)) {
+ Block parent = parentMap[currentBlock];
+ Expr pParentExpr = null;
+ if (predMap.ContainsKey(parent)) {
+ var parentPred = predMap[parent];
+ if (parentPred != null) {
+ pParentExpr = Expr.Ident(parentPred);
+ block.Cmds.Add(new AssertCmd(Token.NoToken,
+ pCurrentExpr != null ? (Expr)Expr.Imp(pCurrentExpr, pParentExpr)
+ : pParentExpr));
+ }
+ }
+ currentBlock = parent;
+ pCurrentExpr = pParentExpr;
+ }
+
+ Block dominator = FindImmediateDominator(block);
+ Expr pDomExpr = Expr.True;
+ if (dominator != null && predMap.ContainsKey(dominator))
+ pDomExpr = new IdentifierExpr(Token.NoToken, predMap[dominator]);
+ var transferCmd = block.TransferCmd;
+ foreach (Cmd cmd in oldCmdSeq)
+ PredicateCmd(pExpr, pDomExpr, newBlocks, block, cmd, out block);
+
+ if (ownedMap.ContainsKey(firstBlock)) {
+ var owned = ownedMap[firstBlock];
+ foreach (var v in owned)
+ block.Cmds.Add(Cmd.SimpleAssign(Token.NoToken, Expr.Ident(v), Expr.False));
+ }
+
+ bool hasPredicatedRegion;
+ PredicateTransferCmd(pExpr, block, block.Cmds, transferCmd, out hasPredicatedRegion);
+
+ if (hasPredicatedRegion)
+ prevBlock = block;
+ else
+ prevBlock = null;
+
+ doneBlocks.Add(block);
+ }
+
+ private Expr CreateIfFPThenElse(Expr then, Expr eElse) {
+ if (myUseProcedurePredicates) {
+ return new NAryExpr(Token.NoToken,
+ new IfThenElse(Token.NoToken),
+ new List<Expr> { fp, then, eElse });
+ } else {
+ return then;
+ }
+ }
+
+ public static void Predicate(Program p,
+ Func<Procedure, bool> useProcedurePredicates = null,
+ UniformityAnalyser uni = null) {
+ useProcedurePredicates = useProcedurePredicates ?? (proc => false);
+ if (uni != null) {
+ var oldUPP = useProcedurePredicates;
+ useProcedurePredicates = proc => oldUPP(proc) && !uni.IsUniform(proc.Name);
+ }
+
+ foreach (var decl in p.TopLevelDeclarations.ToList()) {
+ if (decl is Procedure || decl is Implementation) {
+ var proc = decl as Procedure;
+ Implementation impl = null;
+ if (proc == null) {
+ impl = (Implementation)decl;
+ proc = impl.Proc;
+ }
+
+ bool upp = useProcedurePredicates(proc);
+ if (upp) {
+ var dwf = (DeclWithFormals)decl;
+ var fpVar = new Formal(Token.NoToken,
+ new TypedIdent(Token.NoToken, "_P",
+ Microsoft.Boogie.Type.Bool),
+ /*incoming=*/true);
+ dwf.InParams = new List<Variable>(
+ (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))
+ .ToArray());
+
+ if (impl == null) {
+ var fpIdentifierExpr = new IdentifierExpr(Token.NoToken, fpVar);
+ foreach (Requires r in proc.Requires) {
+ new EnabledReplacementVisitor(fpIdentifierExpr, Expr.True).VisitExpr(r.Condition);
+ if (!QKeyValue.FindBoolAttribute(r.Attributes, "do_not_predicate")) {
+ r.Condition = Expr.Imp(fpIdentifierExpr, r.Condition);
+ }
+ }
+ foreach (Ensures e in proc.Ensures) {
+ new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar), Expr.True).VisitExpr(e.Condition);
+ if (!QKeyValue.FindBoolAttribute(e.Attributes, "do_not_predicate")) {
+ e.Condition = Expr.Imp(fpIdentifierExpr, e.Condition);
+ }
+ }
+ }
+ } else {
+ if (impl == null) {
+ foreach (Requires r in proc.Requires) {
+ new EnabledReplacementVisitor(Expr.True, Expr.True).VisitExpr(r.Condition);
+ }
+ foreach (Ensures e in proc.Ensures) {
+ new EnabledReplacementVisitor(Expr.True, Expr.True).VisitExpr(e.Condition);
+ }
+ }
+ }
+
+ if (impl != null) {
+ try {
+ new SmartBlockPredicator(p, impl, useProcedurePredicates, uni).PredicateImplementation();
+ } catch (Program.IrreducibleLoopException) { }
+ }
+ }
+ }
+ }
+
+ public static void Predicate(Program p, Implementation impl) {
+ try {
+ new SmartBlockPredicator(p, impl, proc => false, null).PredicateImplementation();
+ }
+ catch (Program.IrreducibleLoopException) { }
+ }
+
+}
+
+class EnabledReplacementVisitor : StandardVisitor
+{
+ private Expr pExpr;
+ private Expr pDomExpr;
+
+ internal EnabledReplacementVisitor(Expr pExpr, Expr pDomExpr)
+ {
+ this.pExpr = pExpr;
+ this.pDomExpr = pDomExpr;
+ }
+
+ public override Expr VisitExpr(Expr node)
+ {
+ if (node is IdentifierExpr)
+ {
+ IdentifierExpr iExpr = node as IdentifierExpr;
+ if (iExpr.Decl is Constant && QKeyValue.FindBoolAttribute(iExpr.Decl.Attributes, "__enabled"))
+ {
+ return pExpr;
+ } else if (iExpr.Decl is Constant && QKeyValue.FindBoolAttribute(iExpr.Decl.Attributes, "__dominator_enabled"))
+ {
+ return pDomExpr;
+ }
+ }
+ return base.VisitExpr(node);
+ }
+}
+
+}
diff --git a/Source/Predication/UniformityAnalyser.cs b/Source/Predication/UniformityAnalyser.cs
index ff298942..5ab2589f 100644
--- a/Source/Predication/UniformityAnalyser.cs
+++ b/Source/Predication/UniformityAnalyser.cs
@@ -1,541 +1,541 @@
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using Microsoft.Boogie;
-using System.Diagnostics;
-using Microsoft.Boogie.GraphUtil;
-
-namespace Microsoft.Boogie
-{
-
- public class UniformityAnalyser
- {
- private Program prog;
-
- private bool doAnalysis;
-
- private ISet<Implementation> entryPoints;
-
- private IEnumerable<Variable> nonUniformVars;
-
- private bool ProcedureChanged;
-
- private Dictionary<string, KeyValuePair<bool, Dictionary<string, bool>>> uniformityInfo;
-
- private Dictionary<string, HashSet<int>> nonUniformLoops;
-
- private Dictionary<string, HashSet<Block>> nonUniformBlocks;
-
- private Dictionary<string, HashSet<int>> loopsWithNonuniformReturn;
-
- private Dictionary<string, List<string>> inParameters;
-
- private Dictionary<string, List<string>> outParameters;
-
- /// <summary>
- /// Simplifies the CFG of the given implementation impl by merging each
- /// basic block with a single predecessor into that predecessor if the
- /// predecessor has a single successor. If a uniformity analyser is
- /// being used then blocks will only be merged if they are both uniform
- /// or both non-uniform
- /// </summary>
- public static void MergeBlocksIntoPredecessors(Program prog, Implementation impl, UniformityAnalyser uni)
- {
- var blockGraph = prog.ProcessLoops(impl);
- var predMap = new Dictionary<Block, Block>();
- foreach (var block in blockGraph.Nodes)
- {
- try
- {
- var pred = blockGraph.Predecessors(block).Single();
- if (blockGraph.Successors(pred).Single() == block &&
- (uni == null ||
- (uni.IsUniform(impl.Name, pred) && uni.IsUniform(impl.Name, block)) ||
- (!uni.IsUniform(impl.Name, pred) && !uni.IsUniform(impl.Name, block))))
- {
- Block predMapping;
- while (predMap.TryGetValue(pred, out predMapping))
- pred = predMapping;
- pred.Cmds.AddRange(block.Cmds);
- pred.TransferCmd = block.TransferCmd;
- impl.Blocks.Remove(block);
- predMap[block] = pred;
- }
- // If Single throws an exception above (i.e. not exactly one pred/succ), skip this block.
- }
- catch (InvalidOperationException) { }
- }
- }
-
- public UniformityAnalyser(Program prog, bool doAnalysis, ISet<Implementation> entryPoints, IEnumerable<Variable> nonUniformVars)
- {
- this.prog = prog;
- this.doAnalysis = doAnalysis;
- this.entryPoints = entryPoints;
- this.nonUniformVars = nonUniformVars;
- uniformityInfo = new Dictionary<string, KeyValuePair<bool, Dictionary<string, bool>>>();
- nonUniformLoops = new Dictionary<string, HashSet<int>>();
- nonUniformBlocks = new Dictionary<string, HashSet<Block>>();
- loopsWithNonuniformReturn = new Dictionary<string, HashSet<int>>();
- inParameters = new Dictionary<string, List<string>>();
- outParameters = new Dictionary<string, List<string>>();
- }
-
- public void Analyse()
- {
- var impls = prog.Implementations;
-
- foreach (var Impl in impls)
- {
- bool uniformProcedure = doAnalysis || entryPoints.Contains(Impl);
-
- uniformityInfo.Add(Impl.Name, new KeyValuePair<bool, Dictionary<string, bool>>
- (uniformProcedure, new Dictionary<string, bool> ()));
-
- nonUniformLoops.Add(Impl.Name, new HashSet<int>());
- loopsWithNonuniformReturn.Add(Impl.Name, new HashSet<int>());
-
- foreach (var v in nonUniformVars)
- SetNonUniform(Impl.Name, v.Name);
-
- foreach (Variable v in Impl.LocVars)
- {
- if (doAnalysis)
- {
- SetUniform(Impl.Name, v.Name);
- }
- else
- {
- SetNonUniform(Impl.Name, v.Name);
- }
- }
-
- inParameters[Impl.Name] = new List<string>();
-
- foreach (Variable v in Impl.InParams)
- {
- inParameters[Impl.Name].Add(v.Name);
- if (doAnalysis)
- {
- SetUniform(Impl.Name, v.Name);
- }
- else
- {
- SetNonUniform(Impl.Name, v.Name);
- }
- }
-
- outParameters[Impl.Name] = new List<string>();
- foreach (Variable v in Impl.OutParams)
- {
- outParameters[Impl.Name].Add(v.Name);
- if (doAnalysis)
- {
- SetUniform(Impl.Name, v.Name);
- }
- else
- {
- SetNonUniform(Impl.Name, v.Name);
- }
- }
-
- ProcedureChanged = true;
- }
-
- var procs = prog.Procedures;
-
- foreach (var Proc in procs) {
-
- if (uniformityInfo.ContainsKey(Proc.Name)) {
- continue;
- }
-
- bool uniformProcedure = doAnalysis;
-
- uniformityInfo.Add(Proc.Name, new KeyValuePair<bool, Dictionary<string, bool>>
- (uniformProcedure, new Dictionary<string, bool>()));
-
- inParameters[Proc.Name] = new List<string>();
-
- foreach (Variable v in Proc.InParams) {
- inParameters[Proc.Name].Add(v.Name);
- if (doAnalysis) {
- SetUniform(Proc.Name, v.Name);
- }
- else {
- SetNonUniform(Proc.Name, v.Name);
- }
- }
-
- outParameters[Proc.Name] = new List<string>();
- foreach (Variable v in Proc.OutParams) {
- outParameters[Proc.Name].Add(v.Name);
- // We do not have a body for the procedure,
- // so we must assume it produces non-uniform
- // results
- SetNonUniform(Proc.Name, v.Name);
- }
-
- ProcedureChanged = true;
- }
-
-
- if (doAnalysis)
- {
- while (ProcedureChanged)
- {
- ProcedureChanged = false;
-
- foreach (var Impl in impls)
- {
- Analyse(Impl, uniformityInfo[Impl.Name].Key);
- }
- }
- }
-
- foreach (var Proc in procs)
- {
- if (!IsUniform (Proc.Name))
- {
- List<string> newIns = new List<String>();
- newIns.Add("_P");
- foreach (string s in inParameters[Proc.Name])
- {
- newIns.Add(s);
- }
- inParameters[Proc.Name] = newIns;
- }
- }
- }
-
- private void Analyse(Implementation Impl, bool ControlFlowIsUniform)
- {
- if (!ControlFlowIsUniform)
- {
- nonUniformBlocks[Impl.Name] = new HashSet<Block>(Impl.Blocks);
-
- foreach (Variable v in Impl.LocVars) {
- if (IsUniform(Impl.Name, v.Name)) {
- SetNonUniform(Impl.Name, v.Name);
- }
- }
-
- foreach (Variable v in Impl.InParams) {
- if (IsUniform(Impl.Name, v.Name)) {
- SetNonUniform(Impl.Name, v.Name);
- }
- }
-
- foreach (Variable v in Impl.OutParams) {
- if (IsUniform(Impl.Name, v.Name)) {
- SetNonUniform(Impl.Name, v.Name);
- }
- }
-
- foreach (Block b in Impl.Blocks) {
- Analyse(Impl, b.Cmds, false);
- }
-
- return;
- }
-
- Graph<Block> blockGraph = prog.ProcessLoops(Impl);
- var ctrlDep = blockGraph.ControlDependence();
-
- // Compute transitive closure of control dependence info.
- ctrlDep.TransitiveClosure();
-
- var nonUniformBlockSet = new HashSet<Block>();
- nonUniformBlocks[Impl.Name] = nonUniformBlockSet;
-
- bool changed;
- do {
- changed = false;
- foreach (var block in Impl.Blocks) {
- bool uniform = !nonUniformBlockSet.Contains(block);
- bool newUniform = Analyse(Impl, block.Cmds, uniform);
- if (uniform && !newUniform) {
- changed = true;
- nonUniformBlockSet.Add(block);
- Block pred = blockGraph.Predecessors(block).Single();
- if (ctrlDep.ContainsKey(pred))
- nonUniformBlockSet.UnionWith(ctrlDep[pred]);
- }
- }
- } while (changed);
- }
-
- private Procedure GetProcedure(string procedureName)
- {
- foreach (var p in prog.Procedures)
- {
- if (p.Name == procedureName)
- {
- return p;
- }
- }
- Debug.Assert(false);
- return null;
- }
-
- private bool Analyse(Implementation impl, List<Cmd> cmdSeq, bool ControlFlowIsUniform)
- {
- foreach (Cmd c in cmdSeq)
- {
- if (c is AssignCmd)
- {
- AssignCmd assignCmd = c as AssignCmd;
- foreach (var a in assignCmd.Lhss.Zip(assignCmd.Rhss))
- {
-
- if (a.Item1 is SimpleAssignLhs)
- {
- SimpleAssignLhs lhs = a.Item1 as SimpleAssignLhs;
- Expr rhs = a.Item2;
- if (IsUniform(impl.Name, lhs.AssignedVariable.Name) &&
- (!ControlFlowIsUniform || !IsUniform(impl.Name, rhs)))
- {
- SetNonUniform(impl.Name, lhs.AssignedVariable.Name);
- }
-
- }
- }
- }
- else if (c is HavocCmd)
- {
- HavocCmd havocCmd = c as HavocCmd;
- foreach(IdentifierExpr ie in havocCmd.Vars)
- {
- if(IsUniform(impl.Name, ie.Decl.Name)) {
- SetNonUniform(impl.Name, ie.Decl.Name);
- }
- }
- }
- else if (c is CallCmd)
- {
- CallCmd callCmd = c as CallCmd;
- DeclWithFormals Callee = GetProcedure(callCmd.callee);
- Debug.Assert(Callee != null);
-
- if (!ControlFlowIsUniform)
- {
- if (IsUniform(callCmd.callee))
- {
- SetNonUniform(callCmd.callee);
- }
- }
- for (int i = 0; i < Callee.InParams.Count; i++)
- {
- if (IsUniform(callCmd.callee, Callee.InParams[i].Name)
- && !IsUniform(impl.Name, callCmd.Ins[i]))
- {
- SetNonUniform(callCmd.callee, Callee.InParams[i].Name);
- }
- }
-
- for (int i = 0; i < Callee.OutParams.Count; i++)
- {
- if (IsUniform(impl.Name, callCmd.Outs[i].Name)
- && !IsUniform(callCmd.callee, Callee.OutParams[i].Name))
- {
- SetNonUniform(impl.Name, callCmd.Outs[i].Name);
- }
- }
-
- }
- else if (c is AssumeCmd)
- {
- var ac = (AssumeCmd)c;
- if (ControlFlowIsUniform && QKeyValue.FindBoolAttribute(ac.Attributes, "partition") &&
- !IsUniform(impl.Name, ac.Expr))
- {
- ControlFlowIsUniform = false;
- }
- }
- }
-
- return ControlFlowIsUniform;
- }
-
- private int GetLoopId(WhileCmd wc)
- {
- AssertCmd inv = wc.Invariants[0] as AssertCmd;
- Debug.Assert(inv.Attributes.Key.Contains("loophead_"));
- return Convert.ToInt32(inv.Attributes.Key.Substring("loophead_".Length));
- }
-
- private void SetNonUniform(string procedureName)
- {
- uniformityInfo[procedureName] = new KeyValuePair<bool,Dictionary<string,bool>>
- (false, uniformityInfo[procedureName].Value);
- RecordProcedureChanged();
- }
-
- private void SetNonUniform(string procedureName, WhileCmd wc)
- {
- nonUniformLoops[procedureName].Add(GetLoopId(wc));
- RecordProcedureChanged();
- }
-
- public bool IsUniform(string procedureName)
- {
- if (!uniformityInfo.ContainsKey(procedureName))
- {
- return false;
- }
- return uniformityInfo[procedureName].Key;
- }
-
- public bool IsUniform(string procedureName, Block b)
- {
- if (!nonUniformBlocks.ContainsKey(procedureName))
- {
- return false;
- }
- return !nonUniformBlocks[procedureName].Contains(b);
- }
-
- class UniformExpressionAnalysisVisitor : ReadOnlyVisitor {
-
- private bool isUniform = true;
- private Dictionary<string, bool> uniformityInfo;
-
- public UniformExpressionAnalysisVisitor(Dictionary<string, bool> uniformityInfo) {
- this.uniformityInfo = uniformityInfo;
- }
-
- public override Variable VisitVariable(Variable v) {
- if (!uniformityInfo.ContainsKey(v.Name)) {
- isUniform = isUniform && (v is Constant);
- } else if (!uniformityInfo[v.Name]) {
- isUniform = false;
- }
-
- return v;
- }
-
- internal bool IsUniform() {
- return isUniform;
- }
- }
-
- public bool IsUniform(string procedureName, Expr expr)
- {
- if (!uniformityInfo.ContainsKey(procedureName))
- {
- return false;
- }
-
- UniformExpressionAnalysisVisitor visitor = new UniformExpressionAnalysisVisitor(uniformityInfo[procedureName].Value);
- visitor.VisitExpr(expr);
- return visitor.IsUniform();
- }
-
- public bool IsUniform(string procedureName, string v)
- {
- if (!uniformityInfo.ContainsKey(procedureName))
- {
- return false;
- }
-
- if (!uniformityInfo[procedureName].Value.ContainsKey(v))
- {
- return false;
- }
- return uniformityInfo[procedureName].Value[v];
- }
-
- private void SetUniform(string procedureName, string v)
- {
- uniformityInfo[procedureName].Value[v] = true;
- RecordProcedureChanged();
- }
-
- private void RecordProcedureChanged()
- {
- ProcedureChanged = true;
- }
-
- private void SetNonUniform(string procedureName, string v)
- {
- uniformityInfo[procedureName].Value[v] = false;
- RecordProcedureChanged();
- }
-
- public void dump()
- {
- foreach (string p in uniformityInfo.Keys)
- {
- Console.WriteLine("Procedure " + p + ": "
- + (uniformityInfo[p].Key ? "uniform" : "nonuniform"));
- foreach (string v in uniformityInfo[p].Value.Keys)
- {
- Console.WriteLine(" " + v + ": " +
- (uniformityInfo[p].Value[v] ? "uniform" : "nonuniform"));
- }
- Console.Write("Ins [");
- for (int i = 0; i < inParameters[p].Count; i++)
- {
- Console.Write((i == 0 ? "" : ", ") + inParameters[p][i]);
- }
- Console.WriteLine("]");
- Console.Write("Outs [");
- for (int i = 0; i < outParameters[p].Count; i++)
- {
- Console.Write((i == 0 ? "" : ", ") + outParameters[p][i]);
- }
- Console.WriteLine("]");
- if (nonUniformLoops.ContainsKey(p)) {
- Console.Write("Non-uniform loops:");
- foreach (int l in nonUniformLoops[p]) {
- Console.Write(" " + l);
- }
- Console.WriteLine();
- }
- if (nonUniformBlocks.ContainsKey(p)) {
- Console.Write("Non-uniform blocks:");
- foreach (Block b in nonUniformBlocks[p]) {
- Console.Write(" " + b.Label);
- }
- Console.WriteLine();
- }
- }
- }
-
-
- public string GetInParameter(string procName, int i)
- {
- return inParameters[procName][i];
- }
-
- public string GetOutParameter(string procName, int i)
- {
- return outParameters[procName][i];
- }
-
-
- public bool knowsOf(string p)
- {
- return uniformityInfo.ContainsKey(p);
- }
-
- public void AddNonUniform(string proc, string v)
- {
- if (uniformityInfo.ContainsKey(proc))
- {
- Debug.Assert(!uniformityInfo[proc].Value.ContainsKey(v));
- uniformityInfo[proc].Value[v] = false;
- }
- }
-
- public void AddNonUniform(string proc, Block b) {
- if (nonUniformBlocks.ContainsKey(proc)) {
- Debug.Assert(!nonUniformBlocks[proc].Contains(b));
- nonUniformBlocks[proc].Add(b);
- }
- }
-
- }
-
-}
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using System.Diagnostics;
+using Microsoft.Boogie.GraphUtil;
+
+namespace Microsoft.Boogie
+{
+
+ public class UniformityAnalyser
+ {
+ private Program prog;
+
+ private bool doAnalysis;
+
+ private ISet<Implementation> entryPoints;
+
+ private IEnumerable<Variable> nonUniformVars;
+
+ private bool ProcedureChanged;
+
+ private Dictionary<string, KeyValuePair<bool, Dictionary<string, bool>>> uniformityInfo;
+
+ private Dictionary<string, HashSet<int>> nonUniformLoops;
+
+ private Dictionary<string, HashSet<Block>> nonUniformBlocks;
+
+ private Dictionary<string, HashSet<int>> loopsWithNonuniformReturn;
+
+ private Dictionary<string, List<string>> inParameters;
+
+ private Dictionary<string, List<string>> outParameters;
+
+ /// <summary>
+ /// Simplifies the CFG of the given implementation impl by merging each
+ /// basic block with a single predecessor into that predecessor if the
+ /// predecessor has a single successor. If a uniformity analyser is
+ /// being used then blocks will only be merged if they are both uniform
+ /// or both non-uniform
+ /// </summary>
+ public static void MergeBlocksIntoPredecessors(Program prog, Implementation impl, UniformityAnalyser uni)
+ {
+ var blockGraph = prog.ProcessLoops(impl);
+ var predMap = new Dictionary<Block, Block>();
+ foreach (var block in blockGraph.Nodes)
+ {
+ try
+ {
+ var pred = blockGraph.Predecessors(block).Single();
+ if (blockGraph.Successors(pred).Single() == block &&
+ (uni == null ||
+ (uni.IsUniform(impl.Name, pred) && uni.IsUniform(impl.Name, block)) ||
+ (!uni.IsUniform(impl.Name, pred) && !uni.IsUniform(impl.Name, block))))
+ {
+ Block predMapping;
+ while (predMap.TryGetValue(pred, out predMapping))
+ pred = predMapping;
+ pred.Cmds.AddRange(block.Cmds);
+ pred.TransferCmd = block.TransferCmd;
+ impl.Blocks.Remove(block);
+ predMap[block] = pred;
+ }
+ // If Single throws an exception above (i.e. not exactly one pred/succ), skip this block.
+ }
+ catch (InvalidOperationException) { }
+ }
+ }
+
+ public UniformityAnalyser(Program prog, bool doAnalysis, ISet<Implementation> entryPoints, IEnumerable<Variable> nonUniformVars)
+ {
+ this.prog = prog;
+ this.doAnalysis = doAnalysis;
+ this.entryPoints = entryPoints;
+ this.nonUniformVars = nonUniformVars;
+ uniformityInfo = new Dictionary<string, KeyValuePair<bool, Dictionary<string, bool>>>();
+ nonUniformLoops = new Dictionary<string, HashSet<int>>();
+ nonUniformBlocks = new Dictionary<string, HashSet<Block>>();
+ loopsWithNonuniformReturn = new Dictionary<string, HashSet<int>>();
+ inParameters = new Dictionary<string, List<string>>();
+ outParameters = new Dictionary<string, List<string>>();
+ }
+
+ public void Analyse()
+ {
+ var impls = prog.Implementations;
+
+ foreach (var Impl in impls)
+ {
+ bool uniformProcedure = doAnalysis || entryPoints.Contains(Impl);
+
+ uniformityInfo.Add(Impl.Name, new KeyValuePair<bool, Dictionary<string, bool>>
+ (uniformProcedure, new Dictionary<string, bool> ()));
+
+ nonUniformLoops.Add(Impl.Name, new HashSet<int>());
+ loopsWithNonuniformReturn.Add(Impl.Name, new HashSet<int>());
+
+ foreach (var v in nonUniformVars)
+ SetNonUniform(Impl.Name, v.Name);
+
+ foreach (Variable v in Impl.LocVars)
+ {
+ if (doAnalysis)
+ {
+ SetUniform(Impl.Name, v.Name);
+ }
+ else
+ {
+ SetNonUniform(Impl.Name, v.Name);
+ }
+ }
+
+ inParameters[Impl.Name] = new List<string>();
+
+ foreach (Variable v in Impl.InParams)
+ {
+ inParameters[Impl.Name].Add(v.Name);
+ if (doAnalysis)
+ {
+ SetUniform(Impl.Name, v.Name);
+ }
+ else
+ {
+ SetNonUniform(Impl.Name, v.Name);
+ }
+ }
+
+ outParameters[Impl.Name] = new List<string>();
+ foreach (Variable v in Impl.OutParams)
+ {
+ outParameters[Impl.Name].Add(v.Name);
+ if (doAnalysis)
+ {
+ SetUniform(Impl.Name, v.Name);
+ }
+ else
+ {
+ SetNonUniform(Impl.Name, v.Name);
+ }
+ }
+
+ ProcedureChanged = true;
+ }
+
+ var procs = prog.Procedures;
+
+ foreach (var Proc in procs) {
+
+ if (uniformityInfo.ContainsKey(Proc.Name)) {
+ continue;
+ }
+
+ bool uniformProcedure = doAnalysis;
+
+ uniformityInfo.Add(Proc.Name, new KeyValuePair<bool, Dictionary<string, bool>>
+ (uniformProcedure, new Dictionary<string, bool>()));
+
+ inParameters[Proc.Name] = new List<string>();
+
+ foreach (Variable v in Proc.InParams) {
+ inParameters[Proc.Name].Add(v.Name);
+ if (doAnalysis) {
+ SetUniform(Proc.Name, v.Name);
+ }
+ else {
+ SetNonUniform(Proc.Name, v.Name);
+ }
+ }
+
+ outParameters[Proc.Name] = new List<string>();
+ foreach (Variable v in Proc.OutParams) {
+ outParameters[Proc.Name].Add(v.Name);
+ // We do not have a body for the procedure,
+ // so we must assume it produces non-uniform
+ // results
+ SetNonUniform(Proc.Name, v.Name);
+ }
+
+ ProcedureChanged = true;
+ }
+
+
+ if (doAnalysis)
+ {
+ while (ProcedureChanged)
+ {
+ ProcedureChanged = false;
+
+ foreach (var Impl in impls)
+ {
+ Analyse(Impl, uniformityInfo[Impl.Name].Key);
+ }
+ }
+ }
+
+ foreach (var Proc in procs)
+ {
+ if (!IsUniform (Proc.Name))
+ {
+ List<string> newIns = new List<String>();
+ newIns.Add("_P");
+ foreach (string s in inParameters[Proc.Name])
+ {
+ newIns.Add(s);
+ }
+ inParameters[Proc.Name] = newIns;
+ }
+ }
+ }
+
+ private void Analyse(Implementation Impl, bool ControlFlowIsUniform)
+ {
+ if (!ControlFlowIsUniform)
+ {
+ nonUniformBlocks[Impl.Name] = new HashSet<Block>(Impl.Blocks);
+
+ foreach (Variable v in Impl.LocVars) {
+ if (IsUniform(Impl.Name, v.Name)) {
+ SetNonUniform(Impl.Name, v.Name);
+ }
+ }
+
+ foreach (Variable v in Impl.InParams) {
+ if (IsUniform(Impl.Name, v.Name)) {
+ SetNonUniform(Impl.Name, v.Name);
+ }
+ }
+
+ foreach (Variable v in Impl.OutParams) {
+ if (IsUniform(Impl.Name, v.Name)) {
+ SetNonUniform(Impl.Name, v.Name);
+ }
+ }
+
+ foreach (Block b in Impl.Blocks) {
+ Analyse(Impl, b.Cmds, false);
+ }
+
+ return;
+ }
+
+ Graph<Block> blockGraph = prog.ProcessLoops(Impl);
+ var ctrlDep = blockGraph.ControlDependence();
+
+ // Compute transitive closure of control dependence info.
+ ctrlDep.TransitiveClosure();
+
+ var nonUniformBlockSet = new HashSet<Block>();
+ nonUniformBlocks[Impl.Name] = nonUniformBlockSet;
+
+ bool changed;
+ do {
+ changed = false;
+ foreach (var block in Impl.Blocks) {
+ bool uniform = !nonUniformBlockSet.Contains(block);
+ bool newUniform = Analyse(Impl, block.Cmds, uniform);
+ if (uniform && !newUniform) {
+ changed = true;
+ nonUniformBlockSet.Add(block);
+ Block pred = blockGraph.Predecessors(block).Single();
+ if (ctrlDep.ContainsKey(pred))
+ nonUniformBlockSet.UnionWith(ctrlDep[pred]);
+ }
+ }
+ } while (changed);
+ }
+
+ private Procedure GetProcedure(string procedureName)
+ {
+ foreach (var p in prog.Procedures)
+ {
+ if (p.Name == procedureName)
+ {
+ return p;
+ }
+ }
+ Debug.Assert(false);
+ return null;
+ }
+
+ private bool Analyse(Implementation impl, List<Cmd> cmdSeq, bool ControlFlowIsUniform)
+ {
+ foreach (Cmd c in cmdSeq)
+ {
+ if (c is AssignCmd)
+ {
+ AssignCmd assignCmd = c as AssignCmd;
+ foreach (var a in assignCmd.Lhss.Zip(assignCmd.Rhss))
+ {
+
+ if (a.Item1 is SimpleAssignLhs)
+ {
+ SimpleAssignLhs lhs = a.Item1 as SimpleAssignLhs;
+ Expr rhs = a.Item2;
+ if (IsUniform(impl.Name, lhs.AssignedVariable.Name) &&
+ (!ControlFlowIsUniform || !IsUniform(impl.Name, rhs)))
+ {
+ SetNonUniform(impl.Name, lhs.AssignedVariable.Name);
+ }
+
+ }
+ }
+ }
+ else if (c is HavocCmd)
+ {
+ HavocCmd havocCmd = c as HavocCmd;
+ foreach(IdentifierExpr ie in havocCmd.Vars)
+ {
+ if(IsUniform(impl.Name, ie.Decl.Name)) {
+ SetNonUniform(impl.Name, ie.Decl.Name);
+ }
+ }
+ }
+ else if (c is CallCmd)
+ {
+ CallCmd callCmd = c as CallCmd;
+ DeclWithFormals Callee = GetProcedure(callCmd.callee);
+ Debug.Assert(Callee != null);
+
+ if (!ControlFlowIsUniform)
+ {
+ if (IsUniform(callCmd.callee))
+ {
+ SetNonUniform(callCmd.callee);
+ }
+ }
+ for (int i = 0; i < Callee.InParams.Count; i++)
+ {
+ if (IsUniform(callCmd.callee, Callee.InParams[i].Name)
+ && !IsUniform(impl.Name, callCmd.Ins[i]))
+ {
+ SetNonUniform(callCmd.callee, Callee.InParams[i].Name);
+ }
+ }
+
+ for (int i = 0; i < Callee.OutParams.Count; i++)
+ {
+ if (IsUniform(impl.Name, callCmd.Outs[i].Name)
+ && !IsUniform(callCmd.callee, Callee.OutParams[i].Name))
+ {
+ SetNonUniform(impl.Name, callCmd.Outs[i].Name);
+ }
+ }
+
+ }
+ else if (c is AssumeCmd)
+ {
+ var ac = (AssumeCmd)c;
+ if (ControlFlowIsUniform && QKeyValue.FindBoolAttribute(ac.Attributes, "partition") &&
+ !IsUniform(impl.Name, ac.Expr))
+ {
+ ControlFlowIsUniform = false;
+ }
+ }
+ }
+
+ return ControlFlowIsUniform;
+ }
+
+ private int GetLoopId(WhileCmd wc)
+ {
+ AssertCmd inv = wc.Invariants[0] as AssertCmd;
+ Debug.Assert(inv.Attributes.Key.Contains("loophead_"));
+ return Convert.ToInt32(inv.Attributes.Key.Substring("loophead_".Length));
+ }
+
+ private void SetNonUniform(string procedureName)
+ {
+ uniformityInfo[procedureName] = new KeyValuePair<bool,Dictionary<string,bool>>
+ (false, uniformityInfo[procedureName].Value);
+ RecordProcedureChanged();
+ }
+
+ private void SetNonUniform(string procedureName, WhileCmd wc)
+ {
+ nonUniformLoops[procedureName].Add(GetLoopId(wc));
+ RecordProcedureChanged();
+ }
+
+ public bool IsUniform(string procedureName)
+ {
+ if (!uniformityInfo.ContainsKey(procedureName))
+ {
+ return false;
+ }
+ return uniformityInfo[procedureName].Key;
+ }
+
+ public bool IsUniform(string procedureName, Block b)
+ {
+ if (!nonUniformBlocks.ContainsKey(procedureName))
+ {
+ return false;
+ }
+ return !nonUniformBlocks[procedureName].Contains(b);
+ }
+
+ class UniformExpressionAnalysisVisitor : ReadOnlyVisitor {
+
+ private bool isUniform = true;
+ private Dictionary<string, bool> uniformityInfo;
+
+ public UniformExpressionAnalysisVisitor(Dictionary<string, bool> uniformityInfo) {
+ this.uniformityInfo = uniformityInfo;
+ }
+
+ public override Variable VisitVariable(Variable v) {
+ if (!uniformityInfo.ContainsKey(v.Name)) {
+ isUniform = isUniform && (v is Constant);
+ } else if (!uniformityInfo[v.Name]) {
+ isUniform = false;
+ }
+
+ return v;
+ }
+
+ internal bool IsUniform() {
+ return isUniform;
+ }
+ }
+
+ public bool IsUniform(string procedureName, Expr expr)
+ {
+ if (!uniformityInfo.ContainsKey(procedureName))
+ {
+ return false;
+ }
+
+ UniformExpressionAnalysisVisitor visitor = new UniformExpressionAnalysisVisitor(uniformityInfo[procedureName].Value);
+ visitor.VisitExpr(expr);
+ return visitor.IsUniform();
+ }
+
+ public bool IsUniform(string procedureName, string v)
+ {
+ if (!uniformityInfo.ContainsKey(procedureName))
+ {
+ return false;
+ }
+
+ if (!uniformityInfo[procedureName].Value.ContainsKey(v))
+ {
+ return false;
+ }
+ return uniformityInfo[procedureName].Value[v];
+ }
+
+ private void SetUniform(string procedureName, string v)
+ {
+ uniformityInfo[procedureName].Value[v] = true;
+ RecordProcedureChanged();
+ }
+
+ private void RecordProcedureChanged()
+ {
+ ProcedureChanged = true;
+ }
+
+ private void SetNonUniform(string procedureName, string v)
+ {
+ uniformityInfo[procedureName].Value[v] = false;
+ RecordProcedureChanged();
+ }
+
+ public void dump()
+ {
+ foreach (string p in uniformityInfo.Keys)
+ {
+ Console.WriteLine("Procedure " + p + ": "
+ + (uniformityInfo[p].Key ? "uniform" : "nonuniform"));
+ foreach (string v in uniformityInfo[p].Value.Keys)
+ {
+ Console.WriteLine(" " + v + ": " +
+ (uniformityInfo[p].Value[v] ? "uniform" : "nonuniform"));
+ }
+ Console.Write("Ins [");
+ for (int i = 0; i < inParameters[p].Count; i++)
+ {
+ Console.Write((i == 0 ? "" : ", ") + inParameters[p][i]);
+ }
+ Console.WriteLine("]");
+ Console.Write("Outs [");
+ for (int i = 0; i < outParameters[p].Count; i++)
+ {
+ Console.Write((i == 0 ? "" : ", ") + outParameters[p][i]);
+ }
+ Console.WriteLine("]");
+ if (nonUniformLoops.ContainsKey(p)) {
+ Console.Write("Non-uniform loops:");
+ foreach (int l in nonUniformLoops[p]) {
+ Console.Write(" " + l);
+ }
+ Console.WriteLine();
+ }
+ if (nonUniformBlocks.ContainsKey(p)) {
+ Console.Write("Non-uniform blocks:");
+ foreach (Block b in nonUniformBlocks[p]) {
+ Console.Write(" " + b.Label);
+ }
+ Console.WriteLine();
+ }
+ }
+ }
+
+
+ public string GetInParameter(string procName, int i)
+ {
+ return inParameters[procName][i];
+ }
+
+ public string GetOutParameter(string procName, int i)
+ {
+ return outParameters[procName][i];
+ }
+
+
+ public bool knowsOf(string p)
+ {
+ return uniformityInfo.ContainsKey(p);
+ }
+
+ public void AddNonUniform(string proc, string v)
+ {
+ if (uniformityInfo.ContainsKey(proc))
+ {
+ Debug.Assert(!uniformityInfo[proc].Value.ContainsKey(v));
+ uniformityInfo[proc].Value[v] = false;
+ }
+ }
+
+ public void AddNonUniform(string proc, Block b) {
+ if (nonUniformBlocks.ContainsKey(proc)) {
+ Debug.Assert(!nonUniformBlocks[proc].Contains(b));
+ nonUniformBlocks[proc].Add(b);
+ }
+ }
+
+ }
+
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 18:33:22 +0000