summaryrefslogtreecommitdiff
path: root/Source/AbsInt
diff options
context:
space:
mode:
Diffstat (limited to 'Source/AbsInt')
-rw-r--r--Source/AbsInt/AbsInt.csproj590
-rw-r--r--Source/AbsInt/IntervalDomain.cs2428
-rw-r--r--Source/AbsInt/NativeLattice.cs670
-rw-r--r--Source/AbsInt/Traverse.cs338
-rw-r--r--Source/AbsInt/TrivialDomain.cs158
-rw-r--r--Source/AbsInt/cce.cs124
6 files changed, 2158 insertions, 2150 deletions
diff --git a/Source/AbsInt/AbsInt.csproj b/Source/AbsInt/AbsInt.csproj
index 69a2667c..359eb146 100644
--- a/Source/AbsInt/AbsInt.csproj
+++ b/Source/AbsInt/AbsInt.csproj
@@ -1,296 +1,296 @@
-<?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)' == '' ">AnyCPU</Platform>
- <ProductVersion>9.0.21022</ProductVersion>
- <SchemaVersion>2.0</SchemaVersion>
- <ProjectGuid>{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}</ProjectGuid>
- <OutputType>Library</OutputType>
- <AppDesignerFolder>Properties</AppDesignerFolder>
- <RootNamespace>AbsInt</RootNamespace>
- <AssemblyName>AbsInt</AssemblyName>
- <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
- <FileAlignment>512</FileAlignment>
- <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
- <SignAssembly>true</SignAssembly>
- <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
- <FileUpgradeFlags>
- </FileUpgradeFlags>
- <OldToolsVersion>3.5</OldToolsVersion>
- <UpgradeBackupLocation />
- <PublishUrl>publish\</PublishUrl>
- <Install>true</Install>
- <InstallFrom>Disk</InstallFrom>
- <UpdateEnabled>false</UpdateEnabled>
- <UpdateMode>Foreground</UpdateMode>
- <UpdateInterval>7</UpdateInterval>
- <UpdateIntervalUnits>Days</UpdateIntervalUnits>
- <UpdatePeriodically>false</UpdatePeriodically>
- <UpdateRequired>false</UpdateRequired>
- <MapFileExtensions>true</MapFileExtensions>
- <ApplicationRevision>0</ApplicationRevision>
- <ApplicationVersion>1.0.0.%2a</ApplicationVersion>
- <IsWebBootstrapper>false</IsWebBootstrapper>
- <UseApplicationTrust>false</UseApplicationTrust>
- <BootstrapperEnabled>true</BootstrapperEnabled>
- <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile>
- </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>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
- <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
- <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis>
- <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly>
- </CodeContractsCustomRewriterAssembly>
- <CodeContractsCustomRewriterClass>
- </CodeContractsCustomRewriterClass>
- <CodeContractsLibPaths>
- </CodeContractsLibPaths>
- <CodeContractsExtraRewriteOptions>
- </CodeContractsExtraRewriteOptions>
- <CodeContractsExtraAnalysisOptions>
- </CodeContractsExtraAnalysisOptions>
- <CodeContractsBaseLineFile>
- </CodeContractsBaseLineFile>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- </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>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'z3apidebug|AnyCPU' ">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\z3apidebug\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <CodeAnalysisRuleAssemblies>
- </CodeAnalysisRuleAssemblies>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>Migrated rules for AbsInt.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
- <WarningLevel>4</WarningLevel>
- <Optimize>false</Optimize>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\Checked\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <CodeAnalysisLogFile>bin\Debug\AbsInt.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
- <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
- <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
- <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
- <CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>
- <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
- <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
- <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
- <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
- <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
- <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
- <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
- <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly />
- <CodeContractsCustomRewriterClass />
- <CodeContractsLibPaths />
- <CodeContractsExtraRewriteOptions />
- <CodeContractsExtraAnalysisOptions />
- <CodeContractsBaseLineFile />
- <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
- <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
- <WarningLevel>4</WarningLevel>
- <Optimize>false</Optimize>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|x86'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\x86\Debug\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>x86</PlatformTarget>
- <CodeAnalysisLogFile>bin\Debug\AbsInt.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
- <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
- <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
- <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
- <WarningLevel>4</WarningLevel>
- <Optimize>false</Optimize>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x86'">
- <OutputPath>bin\x86\Release\</OutputPath>
- <DefineConstants>TRACE</DefineConstants>
- <Optimize>true</Optimize>
- <DebugType>pdbonly</DebugType>
- <PlatformTarget>x86</PlatformTarget>
- <CodeAnalysisLogFile>bin\Release\AbsInt.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
- <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
- <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
- <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
- <WarningLevel>4</WarningLevel>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'z3apidebug|x86'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\x86\z3apidebug\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>x86</PlatformTarget>
- <CodeAnalysisLogFile>bin\z3apidebug\AbsInt.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>Migrated rules for AbsInt.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
- <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>
- <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
- <WarningLevel>4</WarningLevel>
- <Optimize>false</Optimize>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|x86'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\x86\Checked\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>x86</PlatformTarget>
- <CodeAnalysisLogFile>bin\Debug\AbsInt.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>AllRules.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>
- <WarningLevel>4</WarningLevel>
- <Optimize>false</Optimize>
- </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>AllRules.ruleset</CodeAnalysisRuleSet>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'QED|x86'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\QED\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- </PropertyGroup>
- <ItemGroup>
- <Reference Include="System" />
- <Reference Include="System.Core">
- <RequiredTargetFramework>3.5</RequiredTargetFramework>
- </Reference>
- <Reference Include="System.Data" />
- <Reference Include="System.Numerics" />
- <Reference Include="System.Xml" />
- </ItemGroup>
- <ItemGroup>
- <Compile Include="IntervalDomain.cs" />
- <Compile Include="TrivialDomain.cs" />
- <Compile Include="NativeLattice.cs" />
- <Compile Include="Traverse.cs" />
- <Compile Include="..\version.cs" />
- </ItemGroup>
- <ItemGroup>
- <ProjectReference Include="..\Basetypes\Basetypes.csproj">
- <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
- <Name>Basetypes</Name>
- </ProjectReference>
- <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">
- <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>
- <Name>CodeContractsExtender</Name>
- </ProjectReference>
- <ProjectReference Include="..\Core\Core.csproj">
- <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
- <Name>Core</Name>
- </ProjectReference>
- <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
- <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
- <Name>ParserHelper</Name>
- </ProjectReference>
- </ItemGroup>
- <ItemGroup>
- <Folder Include="Properties\" />
- </ItemGroup>
- <ItemGroup>
- <BootstrapperPackage Include="Microsoft.Net.Client.3.5">
- <Visible>False</Visible>
- <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>
- <Install>false</Install>
- </BootstrapperPackage>
- <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">
- <Visible>False</Visible>
- <ProductName>.NET Framework 3.5 SP1</ProductName>
- <Install>true</Install>
- </BootstrapperPackage>
- <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1">
- <Visible>False</Visible>
- <ProductName>Windows Installer 3.1</ProductName>
- <Install>true</Install>
- </BootstrapperPackage>
- </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>
- -->
+<?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)' == '' ">AnyCPU</Platform>
+ <ProductVersion>9.0.21022</ProductVersion>
+ <SchemaVersion>2.0</SchemaVersion>
+ <ProjectGuid>{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}</ProjectGuid>
+ <OutputType>Library</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>AbsInt</RootNamespace>
+ <AssemblyName>BoogieAbsInt</AssemblyName>
+ <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
+ <FileAlignment>512</FileAlignment>
+ <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
+ <SignAssembly>true</SignAssembly>
+ <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
+ <FileUpgradeFlags>
+ </FileUpgradeFlags>
+ <OldToolsVersion>3.5</OldToolsVersion>
+ <UpgradeBackupLocation />
+ <PublishUrl>publish\</PublishUrl>
+ <Install>true</Install>
+ <InstallFrom>Disk</InstallFrom>
+ <UpdateEnabled>false</UpdateEnabled>
+ <UpdateMode>Foreground</UpdateMode>
+ <UpdateInterval>7</UpdateInterval>
+ <UpdateIntervalUnits>Days</UpdateIntervalUnits>
+ <UpdatePeriodically>false</UpdatePeriodically>
+ <UpdateRequired>false</UpdateRequired>
+ <MapFileExtensions>true</MapFileExtensions>
+ <ApplicationRevision>0</ApplicationRevision>
+ <ApplicationVersion>1.0.0.%2a</ApplicationVersion>
+ <IsWebBootstrapper>false</IsWebBootstrapper>
+ <UseApplicationTrust>false</UseApplicationTrust>
+ <BootstrapperEnabled>true</BootstrapperEnabled>
+ <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>
+ </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>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+ <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
+ <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly>
+ </CodeContractsCustomRewriterAssembly>
+ <CodeContractsCustomRewriterClass>
+ </CodeContractsCustomRewriterClass>
+ <CodeContractsLibPaths>
+ </CodeContractsLibPaths>
+ <CodeContractsExtraRewriteOptions>
+ </CodeContractsExtraRewriteOptions>
+ <CodeContractsExtraAnalysisOptions>
+ </CodeContractsExtraAnalysisOptions>
+ <CodeContractsBaseLineFile>
+ </CodeContractsBaseLineFile>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
+ <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+ </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>
+ <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'z3apidebug|AnyCPU' ">
+ <DebugSymbols>true</DebugSymbols>
+ <OutputPath>bin\z3apidebug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <DebugType>full</DebugType>
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <CodeAnalysisRuleAssemblies>
+ </CodeAnalysisRuleAssemblies>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>Migrated rules for AbsInt.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
+ <DebugSymbols>true</DebugSymbols>
+ <OutputPath>bin\Checked\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <DebugType>full</DebugType>
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <CodeAnalysisLogFile>bin\Debug\AbsInt.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
+ <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>
+ <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly />
+ <CodeContractsCustomRewriterClass />
+ <CodeContractsLibPaths />
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsExtraAnalysisOptions />
+ <CodeContractsBaseLineFile />
+ <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|x86'">
+ <DebugSymbols>true</DebugSymbols>
+ <OutputPath>bin\x86\Debug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <DebugType>full</DebugType>
+ <PlatformTarget>x86</PlatformTarget>
+ <CodeAnalysisLogFile>bin\Debug\AbsInt.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
+ <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x86'">
+ <OutputPath>bin\x86\Release\</OutputPath>
+ <DefineConstants>TRACE</DefineConstants>
+ <Optimize>true</Optimize>
+ <DebugType>pdbonly</DebugType>
+ <PlatformTarget>x86</PlatformTarget>
+ <CodeAnalysisLogFile>bin\Release\AbsInt.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
+ <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'z3apidebug|x86'">
+ <DebugSymbols>true</DebugSymbols>
+ <OutputPath>bin\x86\z3apidebug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <DebugType>full</DebugType>
+ <PlatformTarget>x86</PlatformTarget>
+ <CodeAnalysisLogFile>bin\z3apidebug\AbsInt.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>Migrated rules for AbsInt.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>
+ <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|x86'">
+ <DebugSymbols>true</DebugSymbols>
+ <OutputPath>bin\x86\Checked\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <DebugType>full</DebugType>
+ <PlatformTarget>x86</PlatformTarget>
+ <CodeAnalysisLogFile>bin\Debug\AbsInt.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>AllRules.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>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
+ </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>AllRules.ruleset</CodeAnalysisRuleSet>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'QED|x86'">
+ <DebugSymbols>true</DebugSymbols>
+ <OutputPath>bin\QED\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <DebugType>full</DebugType>
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+ </PropertyGroup>
+ <ItemGroup>
+ <Reference Include="System" />
+ <Reference Include="System.Core">
+ <RequiredTargetFramework>3.5</RequiredTargetFramework>
+ </Reference>
+ <Reference Include="System.Data" />
+ <Reference Include="System.Numerics" />
+ <Reference Include="System.Xml" />
+ </ItemGroup>
+ <ItemGroup>
+ <Compile Include="IntervalDomain.cs" />
+ <Compile Include="TrivialDomain.cs" />
+ <Compile Include="NativeLattice.cs" />
+ <Compile Include="Traverse.cs" />
+ <Compile Include="..\version.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <ProjectReference Include="..\Basetypes\Basetypes.csproj">
+ <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
+ <Name>Basetypes</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">
+ <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>
+ <Name>CodeContractsExtender</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Core\Core.csproj">
+ <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
+ <Name>Core</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
+ <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
+ <Name>ParserHelper</Name>
+ </ProjectReference>
+ </ItemGroup>
+ <ItemGroup>
+ <Folder Include="Properties\" />
+ </ItemGroup>
+ <ItemGroup>
+ <BootstrapperPackage Include="Microsoft.Net.Client.3.5">
+ <Visible>False</Visible>
+ <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>
+ <Install>false</Install>
+ </BootstrapperPackage>
+ <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">
+ <Visible>False</Visible>
+ <ProductName>.NET Framework 3.5 SP1</ProductName>
+ <Install>true</Install>
+ </BootstrapperPackage>
+ <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1">
+ <Visible>False</Visible>
+ <ProductName>Windows Installer 3.1</ProductName>
+ <Install>true</Install>
+ </BootstrapperPackage>
+ </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/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index d5a5efc9..0dd78cbb 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -1,1210 +1,1218 @@
-using System;
-using System.Numerics;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-using Microsoft.Basetypes;
-
-namespace Microsoft.Boogie.AbstractInterpretation
-{
- class NativeIntervallDomain : NativeLattice
- {
- abstract class E_Common : NativeLattice.Element { }
- class E_Bottom : E_Common
- {
- public override Expr ToExpr() {
- return Expr.False;
- }
- }
- class E : E_Common
- {
- public readonly Node N;
- public E() { }
- public E(Node n) {
- N = n;
- }
-
- public override Expr ToExpr() {
- Expr expr = Expr.True;
- for (var n = N; n != null; n = n.Next) {
- expr = BplAnd(expr, n.ToExpr());
- }
- return expr;
- }
- }
- public class Node
- {
- public readonly Variable V; // variable has type bool or int
- // For an integer variable (Lo,Hi) indicates Lo <= V < Hi, where Lo==null means no lower bound and Hi==null means no upper bound.
- // For a real variable (Lo,Hi) indicates Lo <= V <= Hi, where Lo==null means no lower bound and Hi==null means no upper bound.
- // For a boolean variable, (Lo,Hi) is one of: (null,null) for {false,true}, (null,1) for {false}, and (1,null) for {true}.
- public readonly BigInteger? Lo;
- public readonly BigInteger? Hi;
- public Node Next; // always sorted according to StrictlyBefore; readonly after full initialization
- [Pure]
- public static bool StrictlyBefore(Variable a, Variable b) {
- Contract.Assert(a.UniqueId != b.UniqueId || a == b);
- return a.UniqueId < b.UniqueId;
- }
-
- Node(Variable v, BigInteger? lo, BigInteger? hi, Node next) {
- Contract.Requires(lo != null || hi != null); // don't accept empty constraints
- Contract.Requires(next == null || StrictlyBefore(v, next.V));
- V = v;
- Lo = lo;
- Hi = hi;
- Next = next;
- }
-
- /// <summary>
- /// This constructor leaves Next as null, allowing the caller to fill in Next to finish off the construction.
- /// </summary>
- public Node(Variable v, BigInteger? lo, BigInteger? hi) {
- Contract.Requires(lo != null || hi != null); // don't accept empty constraints
- V = v;
- Lo = lo;
- Hi = hi;
- }
-
- /// <summary>
- /// Returns a Node that has the constraints head.{V,Lo,Hi} plus
- /// all the constraints entailed by Nodes reachable from tail.
- /// Requires that "head" sorts no later than anything in "tail".
- /// Create either returns "head" itself or returns a new Node.
- /// </summary>
- public static Node Create(Node head, Node tail) {
- Contract.Requires(head != null);
- Contract.Requires(tail == null || !StrictlyBefore(tail.V, head.V));
- Contract.Requires(head != tail);
-
- if (head.Next == tail) {
- return head;
- } else if (tail != null && head.V == tail.V) {
- // incorporate both constraints into one Node
- return new Node(head.V, Max(head.Lo, tail.Lo, true), Min(head.Lo, tail.Lo, true), tail.Next);
- } else {
- return new Node(head.V, head.Lo, head.Hi, tail);
- }
- }
-
- public static void GetBounds(Node n, Variable v, out BigInteger? lo, out BigInteger? hi) {
- for (; n != null; n = n.Next) {
- if (n.V == v) {
- lo = n.Lo;
- hi = n.Hi;
- return;
- } else if (StrictlyBefore(v, n.V)) {
- break;
- }
- }
- lo = null;
- hi = null;
- }
-
- /// <summary>
- /// Return the minimum of "a" and "b". If treatNullAsUnit==true, then "null" is
- /// interpreted as positive infinity (the unit element of min); otherwise, it is
- /// treated as negative infinity (the zero element of min).
- /// </summary>
- public static BigInteger? Min(BigInteger? a, BigInteger? b, bool treatNullAsUnit) {
- if (a == null) {
- return treatNullAsUnit ? b : a;
- } else if (b == null) {
- return treatNullAsUnit ? a : b;
- } else {
- return BigInteger.Min((BigInteger)a, (BigInteger)b);
- }
- }
-
- /// <summary>
- /// Return the maximum of "a" and "b". If treatNullAsUnit==true, then "null" is
- /// interpreted as negative infinity (the unit element of max); otherwise, it is
- /// treated as positive infinity (the zero element of max).
- /// </summary>
- public static BigInteger? Max(BigInteger? a, BigInteger? b, bool treatNullAsUnit) {
- if (a == null) {
- return treatNullAsUnit ? b : a;
- } else if (b == null) {
- return treatNullAsUnit ? a : b;
- } else {
- return BigInteger.Max((BigInteger)a, (BigInteger)b);
- }
- }
-
- public static IEnumerable<Tuple<Node, Node>> Merge(Node a, Node b) {
- while (true) {
- if (a == null && b == null) {
- yield break;
- } else if (a == null || b == null) {
- yield return new Tuple<Node, Node>(a, b);
- if (a != null) { a = a.Next; } else { b = b.Next; }
- } else if (a.V == b.V) {
- yield return new Tuple<Node, Node>(a, b);
- a = a.Next; b = b.Next;
- } else if (StrictlyBefore(a.V, b.V)) {
- yield return new Tuple<Node, Node>(a, null);
- a = a.Next;
- } else {
- yield return new Tuple<Node, Node>(null, b);
- b = b.Next;
- }
- }
- }
-
- public Expr ToExpr() {
- if (!V.IsMutable && CommandLineOptions.Clo.InstrumentInfer != CommandLineOptions.InstrumentationPlaces.Everywhere) {
- // omit invariants about readonly variables
- return Expr.True;
- } else if (V.TypedIdent.Type.IsBool) {
- if (Lo == null && Hi == null) {
- return Expr.True;
- } else {
- Contract.Assert((Lo == null && (BigInteger)Hi == 1) || (Hi == null && (BigInteger)Lo == 1));
- var ide = new IdentifierExpr(Token.NoToken, V);
- return Hi == null ? ide : Expr.Not(ide);
- }
- } else if (V.TypedIdent.Type.IsInt) {
- Expr e = Expr.True;
- if (Lo != null && Hi != null && Lo + 1 == Hi) {
- // produce an equality
- var ide = new IdentifierExpr(Token.NoToken, V);
- e = Expr.And(e, BplEq(ide, NumberToExpr((BigInteger)Lo, V.TypedIdent.Type)));
- } else {
- // produce a (possibly empty) conjunction of inequalities
- if (Lo != null) {
- var ide = new IdentifierExpr(Token.NoToken, V);
- e = Expr.And(e, BplLe(NumberToExpr((BigInteger)Lo, V.TypedIdent.Type), ide));
- }
- if (Hi != null) {
- var ide = new IdentifierExpr(Token.NoToken, V);
- e = Expr.And(e, BplLt(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type)));
- }
- }
- return e;
- } else if (V.TypedIdent.Type.IsReal){
- Expr e = Expr.True;
- if (Lo != null && Hi != null && Lo == Hi) {
- // produce an equality
- var ide = new IdentifierExpr(Token.NoToken, V);
- e = Expr.And(e, BplEq(ide, NumberToExpr((BigInteger)Lo, V.TypedIdent.Type)));
- } else {
- // produce a (possibly empty) conjunction of inequalities
- if (Lo != null) {
- var ide = new IdentifierExpr(Token.NoToken, V);
- e = Expr.And(e, BplLe(NumberToExpr((BigInteger)Lo, V.TypedIdent.Type), ide));
- }
- if (Hi != null) {
- var ide = new IdentifierExpr(Token.NoToken, V);
- e = Expr.And(e, BplLe(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type)));
- }
- }
- return e;
- } else {
- Contract.Assert(V.TypedIdent.Type.IsFloat);
- Expr e = Expr.True;
- if (Lo != null && Hi != null && Lo == Hi)
- {
- // produce an equality
- var ide = new IdentifierExpr(Token.NoToken, V);
- e = Expr.And(e, BplEq(ide, NumberToExpr((BigInteger)Lo, V.TypedIdent.Type)));
- }
- else
- {
- // produce a (possibly empty) conjunction of inequalities
- if (Lo != null)
- {
- var ide = new IdentifierExpr(Token.NoToken, V);
- e = Expr.And(e, BplLe(NumberToExpr((BigInteger)Lo, V.TypedIdent.Type), ide));
- }
- if (Hi != null)
- {
- var ide = new IdentifierExpr(Token.NoToken, V);
- e = Expr.And(e, BplLe(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type)));
- }
- }
- return e;
- }
- }
- }
-
- static Expr NumberToExpr(BigInteger n, Type ty) {
- if (n == null) {
- return null;
- } else if (ty.IsReal) {
- return Expr.Literal(Basetypes.BigDec.FromBigInt(n));
- } else if (ty.IsFloat) {
- return Expr.Literal(Basetypes.BigFloat.FromBigInt(n, ty.FloatExponent, ty.FloatMantissa));
- } else {
- Contract.Assume(ty.IsInt);
- return Expr.Literal(Basetypes.BigNum.FromBigInt(n));
- }
- }
-
- List<BigInteger> upThresholds; // invariant: thresholds are sorted
- List<BigInteger> downThresholds; // invariant: thresholds are sorted
-
- /// <summary>
- /// Requires "thresholds" to be sorted.
- /// </summary>
- public NativeIntervallDomain() {
- upThresholds = new List<BigInteger>();
- downThresholds = new List<BigInteger>();
- }
-
- public override void Specialize(Implementation impl) {
- if (impl == null) {
- // remove thresholds
- upThresholds = new List<BigInteger>();
- downThresholds = new List<BigInteger>();
- } else {
- var tf = new ThresholdFinder(impl);
- tf.Find(out downThresholds, out upThresholds);
-#if DEBUG_PRINT
- Console.Write("DEBUG: for implementation '{0}', setting downs to [", impl.Name);
- foreach (var i in downThresholds) {
- Console.Write(" {0}", i);
- }
- Console.Write(" ] and ups to [");
- foreach (var i in upThresholds) {
- Console.Write(" {0}", i);
- }
- Console.WriteLine(" ]");
-#endif
- }
- base.Specialize(impl);
- }
-
- private E_Common top = new E();
- private E_Common bottom = new E_Bottom();
-
- public override Element Top { get { return top; } }
- public override Element Bottom { get { return bottom; } }
-
- public override bool IsTop(Element element) {
- var e = element as E;
- return e != null && e.N == null;
- }
- public override bool IsBottom(Element element) {
- return element is E_Bottom;
- }
-
- public override bool Below(Element a, Element b) {
- if (a is E_Bottom) {
- return true;
- } else if (b is E_Bottom) {
- return false;
- } else {
- var aa = (E)a;
- var bb = (E)b;
- // check if every constraint in 'bb' is implied by constraints in 'aa'
- foreach (var t in Node.Merge(aa.N, bb.N)) {
- var x = t.Item1;
- var y = t.Item2;
- if (x == null) {
- // bb constrains a variable that aa does not
- return false;
- } else if (y == null) {
- // aa constrains a variable that bb does not; that's fine
- } else if (y.Lo != null && (x.Lo == null || x.Lo < y.Lo)) {
- // bb has a Lo constraint, and either aa has no Lo constraint or it has a weaker Lo constraint
- return false;
- } else if (y.Hi != null && (x.Hi == null || y.Hi < x.Hi)) {
- // bb has a Hi o constraint, and either aa has no Hi constraint or it has a weaker Hi constraint
- return false;
- }
- }
- return true;
- }
- }
-
- public override Element Meet(Element a, Element b) {
- if (a is E_Bottom) {
- return a;
- } else if (b is E_Bottom) {
- return b;
- } else {
- var aa = (E)a;
- var bb = (E)b;
- Node head = null;
- Node prev = null;
- foreach (var t in Node.Merge(aa.N, bb.N)) {
- var x = t.Item1;
- var y = t.Item2;
- Node n;
- if (x == null) {
- n = new Node(y.V, y.Lo, y.Hi);
- } else if (y == null) {
- n = new Node(x.V, x.Lo, x.Hi);
- } else {
- var lo = Node.Max(x.Lo, y.Lo, true);
- var hi = Node.Min(x.Hi, y.Hi, true);
- // if hi<=lo (or hi<lo for reals), then we're overconstrained
- if (lo != null && hi != null && (x.V.TypedIdent.Type.IsReal ? hi < lo : hi <= lo)) {
- return bottom;
- }
- n = new Node(x.V, lo, hi);
- }
- if (head == null) {
- head = n;
- } else {
- prev.Next = n;
- }
- prev = n;
- }
- return new E(head);
- }
- }
-
- public override Element Join(Element a, Element b) {
- if (a is E_Bottom) {
- return b;
- } else if (b is E_Bottom) {
- return a;
- } else {
- var aa = (E)a;
- var bb = (E)b;
- // for each variable, take the weaker of the constraints
- Node head = null;
- Node prev = null;
- foreach (var t in Node.Merge(aa.N, bb.N)) {
- if (t.Item1 != null && t.Item2 != null) {
- var lo = Node.Min(t.Item1.Lo, t.Item2.Lo, false);
- var hi = Node.Max(t.Item1.Hi, t.Item2.Hi, false);
- if (lo != null || hi != null) {
- var n = new Node(t.Item1.V, lo, hi);
- if (head == null) {
- head = n;
- } else {
- prev.Next = n;
- }
- prev = n;
- }
- }
- }
- return new E(head);
- }
- }
-
- public override Element Widen(Element a, Element b) {
- if (a is E_Bottom) {
- return b; // since this is done just once, we maintain the ascending chains property
- } else if (b is E_Bottom) {
- return a;
- } else {
- var aa = (E)a;
- var bb = (E)b;
- // return a subset of the constraints of aa, namely those that are implied by bb
- Node head = null;
- Node prev = null;
- foreach (var t in Node.Merge(aa.N, bb.N)) {
- var x = t.Item1;
- var y = t.Item2;
- if (x != null && y != null) {
- BigInteger? lo, hi;
- lo = hi = null;
- if (x.Lo != null && y.Lo != null) {
- if (x.Lo <= y.Lo) {
- // okay, we keep the lower bound
- lo = x.Lo;
- } else {
- // set "lo" to the threshold that is below (or equal) y.Lo
- lo = RoundDown((BigInteger)y.Lo);
- }
- }
- if (x.Hi != null && y.Hi != null) {
- if (y.Hi <= x.Hi) {
- // okay, we keep the upper bound
- hi = x.Hi;
- } else {
- // set "hi" to the threshold that is above (or equal) y.Hi
- hi = RoundUp((BigInteger)y.Hi);
- }
- }
- if (lo != null || hi != null) {
- var n = new Node(x.V, lo, hi);
- if (head == null) {
- head = n;
- } else {
- prev.Next = n;
- }
- prev = n;
- }
- }
- }
- return new E(head);
- }
- }
-
- /// <summary>
- /// For a proof of correctness of this method, see Test/dafny2/Intervals.dfy.
- /// A difference is that the this method returns:
- /// let d = Dafny_RoundDown(k);
- /// return d == -1 ? null : downThresholds[d];
- /// </summary>
- BigInteger? RoundDown(BigInteger k)
- {
- if (downThresholds.Count == 0 || k < downThresholds[0]) {
- return null;
- }
- var i = 0;
- var j = downThresholds.Count - 1;
- while (i < j)
- {
- var mid = i + (j - i + 1) / 2;
- if (downThresholds[mid] <= k) {
- i = mid;
- } else {
- j = mid - 1;
- }
- }
- return downThresholds[i];
- }
-
- /// <summary>
- /// For a proof of correctness of this method, see Test/dafny2/Intervals.dfy.
- /// A difference is that the this method returns:
- /// let d = Dafny_RoundUp(k);
- /// return d == thresholds.Count ? null : upThresholds[d];
- /// </summary>
- BigInteger? RoundUp(BigInteger k)
- {
- if (upThresholds.Count == 0 || upThresholds[upThresholds.Count - 1] < k) {
- return null;
- }
- var i = 0;
- var j = upThresholds.Count - 1;
- while (i < j)
- {
- var mid = i + (j - i) / 2;
- if (upThresholds[mid] < k) {
- i = mid + 1;
- } else {
- j = mid;
- }
- }
- return upThresholds[i];
- }
-
- public override Element Constrain(Element element, Expr expr) {
- if (element is E_Bottom) {
- return element;
- } else {
- var e = (E)element;
- var c = Constraint(expr, e.N);
- return c == null ? element : Meet(element, c);
- }
- }
-
- /// <summary>
- /// Returns an Element that corresponds to the constraints implied by "expr" in the
- /// state "state".
- /// Return "null" to indicate no constraints.
- /// </summary>
- E_Common Constraint(Expr expr, Node state) {
- Variable v;
- if (IsVariable(expr, out v)) {
- var n = new Node(v, BigInteger.One, null);
- return new E(n);
- } else if (expr is LiteralExpr) {
- var e = (LiteralExpr)expr;
- return (bool)e.Val ? null : new E_Bottom();
- } else if (expr is NAryExpr) {
- var e = (NAryExpr)expr;
- if (e.Fun is UnaryOperator) {
- if (((UnaryOperator)e.Fun).Op == UnaryOperator.Opcode.Not) {
- if (IsVariable(e.Args[0], out v)) {
- var n = new Node(v, null, BigInteger.One);
- return new E(n);
- }
- }
- } else if (e.Fun is BinaryOperator) {
- var op = ((BinaryOperator)e.Fun).Op;
- var arg0 = e.Args[0];
- var arg1 = e.Args[1];
- switch (op) {
- case BinaryOperator.Opcode.Eq:
- case BinaryOperator.Opcode.Iff: {
- E_Common c = null;
- if (IsVariable(arg0, out v)) {
- BigInteger? lo, hi;
- if (PartiallyEvaluate(arg1, state, out lo, out hi)) {
- var n = new Node(v, lo, hi);
- c = new E(n);
- }
- }
- if (IsVariable(arg1, out v)) {
- BigInteger? lo, hi;
- if (PartiallyEvaluate(arg1, state, out lo, out hi)) {
- var n = new Node(v, lo, hi);
- c = c == null ? new E(n) : (E_Common)Meet(c, new E(n));
- }
- }
- return c;
- }
- case BinaryOperator.Opcode.Neq: {
- E_Common c = null;
- if (IsVariable(arg0, out v)) {
- c = ConstrainNeq(state, v, arg1);
- }
- if (IsVariable(arg1, out v)) {
- var cc = ConstrainNeq(state, v, arg0);
- if (cc != null) {
- c = c == null ? cc : (E_Common)Meet(c, cc);
- }
- }
- return c;
- }
- case BinaryOperator.Opcode.Le: {
- E_Common c = null;
- if (IsVariable(arg1, out v)) {
- BigInteger? lo, hi;
- PartiallyEvaluate(arg0, state, out lo, out hi);
- if (lo != null) {
- var n = new Node(v, lo, null);
- c = new E(n);
- }
- }
- if (IsVariable(arg0, out v)) {
- BigInteger? lo, hi;
- PartiallyEvaluate(arg1, state, out lo, out hi);
- if (hi != null) {
- var n = new Node(v, null, hi);
- c = c == null ? new E(n) : (E_Common)Meet(c, new E(n));
- }
- }
- return c;
- }
- case BinaryOperator.Opcode.Lt: {
- E_Common c = null;
- if (IsVariable(arg1, out v)) {
- BigInteger? lo, hi;
- PartiallyEvaluate(arg0, state, out lo, out hi);
- if (lo != null) {
- var n = new Node(v, v.TypedIdent.Type.IsReal ? lo : lo + 1, null);
- c = new E(n);
- }
- }
- if (IsVariable(arg0, out v)) {
- BigInteger? lo, hi;
- PartiallyEvaluate(arg1, state, out lo, out hi);
- if (hi != null) {
- var n = new Node(v, null, v.TypedIdent.Type.IsReal ? hi : hi - 1);
- c = c == null ? new E(n) : (E_Common)Meet(c, new E(n));
- }
- }
- return c;
- }
- case BinaryOperator.Opcode.Ge: {
- var tmp = arg0; arg0 = arg1; arg1 = tmp;
- goto case BinaryOperator.Opcode.Le;
- }
- case BinaryOperator.Opcode.Gt: {
- var tmp = arg0; arg0 = arg1; arg1 = tmp;
- goto case BinaryOperator.Opcode.Lt;
- }
- default:
- break;
- }
- }
- }
- return null; // approximation
- }
-
- private E ConstrainNeq(Node state, Variable v, Expr arg) {
- BigInteger? lo, hi;
- if (PartiallyEvaluate(arg, state, out lo, out hi)) {
- if (!v.TypedIdent.Type.IsReal && lo != null && hi != null && lo + 1 == hi) {
- var exclude = lo;
- // If the partially evaluated arg (whose value is "exclude") is an end-point of
- // the interval known for "v", then produce a constraint that excludes that bound.
- Node.GetBounds(state, v, out lo, out hi);
- if (lo != null && lo == exclude) {
- var n = new Node(v, lo + 1, null);
- return new E(n);
- } else if (hi != null && exclude + 1 == hi) {
- var n = new Node(v, null, exclude);
- return new E(n);
- }
- }
- }
- return null;
- }
-
- bool IsVariable(Expr expr, out Variable v) {
- var e = expr as IdentifierExpr;
- if (e == null) {
- v = null;
- return false;
- } else {
- v = e.Decl;
- return true;
- }
- }
-
- public override Element Update(Element element, AssignCmd cmd) {
- if (element is E_Bottom) {
- return element;
- }
- var e = (E)element;
- var nn = e.N;
- Contract.Assert(cmd.Lhss.Count == cmd.Rhss.Count);
- for (int i = 0; i < cmd.Lhss.Count; i++) {
- var lhs = cmd.Lhss[i];
- var rhs = cmd.Rhss[i];
- BigInteger? lo;
- BigInteger? hi;
- PartiallyEvaluate(rhs, e.N, out lo, out hi);
- nn = UpdateOne(nn, lhs.DeepAssignedVariable, lo, hi);
- }
- return new E(nn);
- }
-
- bool PartiallyEvaluate(Expr rhs, Node node, out BigInteger? lo, out BigInteger? hi) {
- var pe = new PEVisitor(node);
- pe.VisitExpr(rhs);
- lo = pe.Lo;
- hi = pe.Hi;
- return lo != null || hi != null;
- }
-
- class PEVisitor : ReadOnlyVisitor
- {
- public BigInteger? Lo;
- public BigInteger? Hi;
-
- readonly BigInteger one = BigInteger.One;
-
- Node N;
- public PEVisitor(Node n) {
- N = n;
- }
-
- // Override visitors for all expressions that can return a boolean, integer, or real result
-
- public override Expr VisitExpr(Expr node) {
- Lo = Hi = null;
- return base.VisitExpr(node);
- }
- public override Expr VisitLiteralExpr(LiteralExpr node) {
- if (node.Val is BigNum) {
- var n = ((BigNum)node.Val).ToBigInteger;
- Lo = n;
- Hi = n + 1;
- } else if (node.Val is BigDec) {
- BigInteger floor, ceiling;
- ((BigDec)node.Val).FloorCeiling(out floor, out ceiling);
- Lo = floor;
- Hi = ceiling;
- } else if (node.Val is BigFloat) {
- BigNum floor, ceiling;
- ((BigFloat)node.Val).FloorCeiling(out floor, out ceiling);
- Lo = floor.ToBigInteger;
- Hi = ceiling.ToBigInteger;
- } else if (node.Val is bool) {
- if ((bool)node.Val) {
- // true
- Lo = one;
- Hi = null;
- } else {
- // false
- Lo = null;
- Hi = one;
- }
- }
- return node;
- }
- public override Expr VisitIdentifierExpr(IdentifierExpr node) {
- if (node.Type.IsBool || node.Type.IsInt || node.Type.IsReal) {
- Node.GetBounds(N, node.Decl, out Lo, out Hi);
- }
- return node;
- }
- public override Expr VisitNAryExpr(NAryExpr node) {
- if (node.Fun is UnaryOperator) {
- var op = (UnaryOperator)node.Fun;
- Contract.Assert(node.Args.Count == 1);
- if (op.Op == UnaryOperator.Opcode.Neg) {
- BigInteger? lo, hi;
- VisitExpr(node.Args[0]);
- lo = Lo; hi = Hi;
- if (hi != null) {
- Lo = node.Type.IsReal ? -hi : 1 - hi;
- }
- if (lo != null) {
- Hi = node.Type.IsReal ? -lo : 1 - lo;
- }
- }
- else if (op.Op == UnaryOperator.Opcode.Not) {
- VisitExpr(node.Args[0]);
- Contract.Assert((Lo == null && Hi == null) ||
- (Lo == null && (BigInteger)Hi == 1) ||
- (Hi == null && (BigInteger)Lo == 1));
- var tmp = Lo;
- Lo = Hi;
- Hi = tmp;
- }
- } else if (node.Fun is BinaryOperator) {
- var op = (BinaryOperator)node.Fun;
- Contract.Assert(node.Args.Count == 2);
- BigInteger? lo0, hi0, lo1, hi1;
- VisitExpr(node.Args[0]);
- lo0 = Lo; hi0 = Hi;
- VisitExpr(node.Args[1]);
- lo1 = Lo; hi1 = Hi;
- Lo = Hi = null;
- var isReal = node.Args[0].Type.IsReal;
- switch (op.Op) {
- case BinaryOperator.Opcode.And:
- if (hi0 != null || hi1 != null) {
- // one operand is definitely false, thus so is the result
- Lo = null; Hi = one;
- } else if (lo0 != null && lo1 != null) {
- // both operands are definitely true, thus so is the result
- Lo = one; Hi = null;
- }
- break;
- case BinaryOperator.Opcode.Or:
- if (lo0 != null || lo1 != null) {
- // one operand is definitely true, thus so is the result
- Lo = one; Hi = null;
- } else if (hi0 != null && hi1 != null) {
- // both operands are definitely false, thus so is the result
- Lo = null; Hi = one;
- }
- break;
- case BinaryOperator.Opcode.Imp:
- if (hi0 != null || lo1 != null) {
- // either arg0 false or arg1 is true, so the result is true
- Lo = one; Hi = null;
- } else if (lo0 != null && hi1 != null) {
- // arg0 is true and arg1 is false, so the result is false
- Lo = null; Hi = one;
- }
- break;
- case BinaryOperator.Opcode.Iff:
- if (lo0 != null && lo1 != null) {
- Lo = one; Hi = null;
- } else if (hi0 != null && hi1 != null) {
- Lo = one; Hi = null;
- } else if (lo0 != null && hi1 != null) {
- Lo = null; Hi = one;
- } else if (hi0 != null && lo1 != null) {
- Lo = null; Hi = one;
- }
- if (op.Op == BinaryOperator.Opcode.Neq) {
- var tmp = Lo; Lo = Hi; Hi = tmp;
- }
- break;
- case BinaryOperator.Opcode.Eq:
- case BinaryOperator.Opcode.Neq:
- if (node.Args[0].Type.IsBool) {
- goto case BinaryOperator.Opcode.Iff;
- }
- // For Eq:
- // If the (lo0,hi0) and (lo1,hi1) ranges do not overlap, the answer is false.
- // If both ranges are the same unit range, then the answer is true.
- if (hi0 != null && lo1 != null && (isReal ? hi0 < lo1 : hi0 <= lo1)) {
- // no overlap
- Lo = null; Hi = one;
- } else if (lo0 != null && hi1 != null && (isReal ? hi1 < lo0 : hi1 <= lo0)) {
- Lo = null; Hi = one;
- // no overlaop
- } else if (lo0 != null && hi0 != null && lo1 != null && hi1 != null &&
- lo0 == lo1 && hi0 == hi1 && // ranges are the same
- (isReal ? lo0 == hi0 : lo0 + 1 == hi0)) { // unit range
- // both ranges are the same unit range
- Lo = one; Hi = null;
- }
- if (op.Op == BinaryOperator.Opcode.Neq) {
- var tmp = Lo; Lo = Hi; Hi = tmp;
- }
- break;
- case BinaryOperator.Opcode.Le:
- if (isReal) {
- // If hi0 <= lo1, then the answer is true.
- // If hi1 < lo0, then the answer is false.
- if (hi0 != null && lo1 != null && hi0 <= lo1) {
- Lo = one; Hi = null;
- } else if (hi1 != null && lo0 != null && hi1 < lo0) {
- Lo = null; Hi = one;
- }
- } else {
- // If hi0 - 1 <= lo1, then the answer is true.
- // If hi1 <= lo0, then the answer is false.
- if (hi0 != null && lo1 != null && hi0 - 1 <= lo1) {
- Lo = one; Hi = null;
- } else if (lo0 != null && hi1 != null && hi1 <= lo0) {
- Lo = null; Hi = one;
- }
- }
- break;
- case BinaryOperator.Opcode.Lt:
- if (isReal) {
- // If hi0 < lo1, then the answer is true.
- // If hi1 <= lo0, then the answer is false.
- if (hi0 != null && lo1 != null && hi0 < lo1) {
- Lo = one; Hi = null;
- } else if (hi1 != null && lo0 != null && hi1 <= lo0) {
- Lo = null; Hi = one;
- }
- } else {
- // If hi0 <= lo1, then the answer is true.
- // If hi1 - 1 <= lo0, then the answer is false.
- if (hi0 != null && lo1 != null && hi0 <= lo1) {
- Lo = one; Hi = null;
- } else if (lo0 != null && hi1 != null && hi1 - 1 <= lo0) {
- Lo = null; Hi = one;
- }
- }
- break;
- case BinaryOperator.Opcode.Gt:
- // swap the operands and then continue as Lt
- {
- var tmp = lo0; lo0 = lo1; lo1 = tmp;
- tmp = hi0; hi0 = hi1; hi1 = tmp;
- }
- goto case BinaryOperator.Opcode.Lt;
- case BinaryOperator.Opcode.Ge:
- // swap the operands and then continue as Le
- {
- var tmp = lo0; lo0 = lo1; lo1 = tmp;
- tmp = hi0; hi0 = hi1; hi1 = tmp;
- }
- goto case BinaryOperator.Opcode.Le;
- case BinaryOperator.Opcode.Add:
- if (lo0 != null && lo1 != null) {
- Lo = lo0 + lo1;
- }
- if (hi0 != null && hi1 != null) {
- Hi = isReal ? hi0 + hi1 : hi0 + hi1 - 1;
- }
- break;
- case BinaryOperator.Opcode.Sub:
- if (lo0 != null && hi1 != null) {
- Lo = isReal ? lo0 - hi1 : lo0 - hi1 + 1;
- }
- if (hi0 != null && lo1 != null) {
- Hi = hi0 - lo1;
- }
- break;
- case BinaryOperator.Opcode.Mul:
- // this uses an incomplete approximation that could be tightened up
- if (lo0 != null && lo1 != null) {
- if (0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
- Lo = lo0 * lo1;
- Hi = hi0 == null || hi1 == null ? null : isReal ? hi0 * hi1 : (hi0 - 1) * (hi1 - 1) + 1;
- } else if ((BigInteger)lo0 < 0 && (BigInteger)lo1 < 0) {
- Lo = null; // approximation
- Hi = isReal ? lo0 * lo1 : lo0 * lo1 + 1;
- }
- }
- break;
- case BinaryOperator.Opcode.Div:
- // this uses an incomplete approximation that could be tightened up
- if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
- Lo = BigInteger.Zero;
- Hi = hi0;
- }
- break;
- case BinaryOperator.Opcode.Mod:
- // this uses an incomplete approximation that could be tightened up
- if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
- Lo = BigInteger.Zero;
- Hi = hi1;
- }
- break;
- case BinaryOperator.Opcode.RealDiv:
- // this uses an incomplete approximation that could be tightened up
- if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
- Lo = BigInteger.Zero;
- Hi = 1 <= (BigInteger)lo1 ? hi0 : null;
- }
- break;
- case BinaryOperator.Opcode.Pow:
- // this uses an incomplete approximation that could be tightened up
- if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
- Lo = 1 <= (BigInteger)lo1 ? BigInteger.One : BigInteger.Zero;
- Hi = hi1;
- }
- break;
- default:
- break;
- }
- } else if (node.Fun is IfThenElse) {
- var op = (IfThenElse)node.Fun;
- Contract.Assert(node.Args.Count == 3);
- BigInteger? guardLo, guardHi, lo0, hi0, lo1, hi1;
- VisitExpr(node.Args[0]);
- guardLo = Lo; guardHi = Hi;
- VisitExpr(node.Args[1]);
- lo0 = Lo; hi0 = Hi;
- VisitExpr(node.Args[2]);
- lo1 = Lo; hi1 = Hi;
- Contract.Assert(guardLo == null || guardHi == null); // this is a consequence of the guard being boolean
- if (guardLo != null) {
- // guard is always true
- Lo = lo0; Hi = hi0;
- } else if (guardHi != null) {
- // guard is always false
- Lo = lo1; Hi = hi1;
- } else {
- // we don't know which branch will be taken, so join the information from the two branches
- Lo = Node.Min(lo0, lo1, false);
- Hi = Node.Max(hi0, hi1, false);
- }
- } else if (node.Fun is FunctionCall) {
- var call = (FunctionCall)node.Fun;
- // See if this is an identity function, which we do by checking: that the function has
- // exactly one argument and the function has been marked by the user with the attribute {:identity}
- bool claimsToBeIdentity = false;
- if (call.ArgumentCount == 1 && call.Func.CheckBooleanAttribute("identity", ref claimsToBeIdentity) && claimsToBeIdentity && node.Args[0].Type.Equals(node.Type)) {
- VisitExpr(node.Args[0]);
- }
- }
- return node;
- }
- public override BinderExpr VisitBinderExpr(BinderExpr node) {
- // don't recurse on subexpression
- return node;
- }
- public override Expr VisitOldExpr(OldExpr node) {
- // don't recurse on subexpression
- return node;
- }
- public override Expr VisitCodeExpr(CodeExpr node) {
- // don't recurse on subexpression
- return node;
- }
- public override Expr VisitBvConcatExpr(BvConcatExpr node) {
- // don't recurse on subexpression
- return node;
- }
- public override Expr VisitBvExtractExpr(BvExtractExpr node) {
- // don't recurse on subexpression
- return node;
- }
- }
-
- public override Element Eliminate(Element element, Variable v) {
- if (element is E_Bottom) {
- return element;
- }
- var e = (E)element;
- var nn = UpdateOne(e.N, v, null, null);
- if (nn == e.N) {
- return element;
- } else {
- return new E(nn);
- }
- }
-
- Node UpdateOne(Node nn, Variable v, BigInteger? lo, BigInteger? hi) {
- var orig = nn;
- Node head = null;
- Node prev = null;
- var foundV = false;
- for (; nn != null && !Node.StrictlyBefore(v, nn.V); nn = nn.Next) {
- if (nn.V == v) {
- foundV = true;
- nn = nn.Next;
- break; // we found the place where the new node goes
- } else {
- var n = new Node(nn.V, nn.Lo, nn.Hi); // copy this Node
- if (head == null) {
- head = n;
- } else {
- prev.Next = n;
- }
- prev = n;
- }
- }
- Node rest;
- if (lo == null && hi == null) {
- // eliminate all information about "v"
- if (!foundV) {
- return orig;
- }
- rest = nn;
- } else {
- rest = new Node(v, lo, hi);
- rest.Next = nn;
- }
- if (head == null) {
- head = rest;
- } else {
- prev.Next = rest;
- }
- return head;
- }
-
- /// <summary>
- /// Return a resolved/type-checked expression that represents the conjunction of a and b.
- /// Requires a and b to be resolved and type checked already.
- /// </summary>
- public static Expr BplAnd(Expr a, Expr b) {
- if (a == Expr.True) {
- return b;
- } else if (b == Expr.True) {
- return a;
- } else {
- var nary = Expr.Binary(BinaryOperator.Opcode.And, a, b);
- nary.Type = Type.Bool;
- nary.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
- return nary;
- }
- }
-
- /// <summary>
- /// Return a resolved/type-checked expression that represents a EQUALS b.
- /// Requires a and b to be resolved and type checked already.
- /// </summary>
- public static Expr BplEq(Expr a, Expr b) {
- var e = Expr.Eq(a, b);
- e.Type = Type.Bool;
- return e;
- }
-
- /// <summary>
- /// Return a resolved/type-checked expression that represents a LESS-EQUAL b.
- /// Requires a and b to be resolved and type checked already.
- /// </summary>
- public static Expr BplLe(Expr a, Expr b) {
- var e = Expr.Le(a, b);
- e.Type = Type.Bool;
- return e;
- }
- /// <summary>
- /// Return a resolved/type-checked expression that represents a LESS b.
- /// Requires a and b to be resolved and type checked already.
- /// </summary>
- public static Expr BplLt(Expr a, Expr b) {
- var e = Expr.Lt(a, b);
- e.Type = Type.Bool;
- return e;
- }
- }
-
- public class ThresholdFinder : ReadOnlyVisitor
- {
- readonly Implementation Impl;
- public ThresholdFinder(Implementation impl) {
- Contract.Requires(impl != null);
- Impl = impl;
- }
- HashSet<BigInteger> downs = new HashSet<BigInteger>();
- HashSet<BigInteger> ups = new HashSet<BigInteger>();
- public void Find(out List<BigInteger> downThresholds, out List<BigInteger> upThresholds) {
- // always include -1, 0, 1 as down-thresholds
- downs.Clear();
- downs.Add(-1);
- downs.Add(0);
- downs.Add(1);
- // always include 0 and 1 as up-thresholds
- ups.Clear();
- ups.Add(0);
- ups.Add(1);
-
- foreach (Requires p in Impl.Proc.Requires) {
- Visit(p.Condition);
- }
- foreach (Ensures p in Impl.Proc.Ensures) {
- Visit(p.Condition);
- }
- foreach (var b in Impl.Blocks) {
- foreach (Cmd c in b.Cmds) {
- Visit(c);
- }
- }
-
- // convert the HashSets to sorted Lists and return
- downThresholds = new List<BigInteger>();
- foreach (var i in downs) {
- downThresholds.Add(i);
- }
- downThresholds.Sort();
- upThresholds = new List<BigInteger>();
- foreach (var i in ups) {
- upThresholds.Add(i);
- }
- upThresholds.Sort();
- }
-
- public override Expr VisitNAryExpr(NAryExpr node) {
- if (node.Fun is BinaryOperator) {
- var op = (BinaryOperator)node.Fun;
- Contract.Assert(node.Args.Count == 2);
- var arg0 = node.Args[0];
- var arg1 = node.Args[1];
- var offset = arg0.Type.IsReal ? 0 : 1;
- BigInteger? k;
- switch (op.Op) {
- case BinaryOperator.Opcode.Eq:
- case BinaryOperator.Opcode.Neq:
- k = AsIntLiteral(arg0);
- if (k != null) {
- var i = (BigInteger)k;
- downs.Add(i - 1);
- downs.Add(i);
- ups.Add(i + 1);
- ups.Add(i + 2);
- }
- k = AsIntLiteral(arg1);
- if (k != null) {
- var i = (BigInteger)k;
- downs.Add(i - 1);
- downs.Add(i);
- ups.Add(i + 1);
- ups.Add(i + 2);
- }
- break;
- case BinaryOperator.Opcode.Le:
- k = AsIntLiteral(arg0);
- if (k != null) {
- var i = (BigInteger)k;
- downs.Add(i - 1);
- downs.Add(i);
- }
- k = AsIntLiteral(arg1);
- if (k != null) {
- var i = (BigInteger)k;
- ups.Add(i + offset);
- ups.Add(i + 1 + offset);
- }
- break;
- case BinaryOperator.Opcode.Lt:
- k = AsIntLiteral(arg0);
- if (k != null) {
- var i = (BigInteger)k;
- downs.Add(i );
- downs.Add(i + 1);
- }
- k = AsIntLiteral(arg1);
- if (k != null) {
- var i = (BigInteger)k;
- ups.Add(i - 1 + offset);
- ups.Add(i + offset);
- }
- break;
- case BinaryOperator.Opcode.Ge:
- { var tmp = arg0; arg0 = arg1; arg1 = tmp; }
- goto case BinaryOperator.Opcode.Le;
- case BinaryOperator.Opcode.Gt:
- { var tmp = arg0; arg0 = arg1; arg1 = tmp; }
- goto case BinaryOperator.Opcode.Lt;
- default:
- break;
- }
- }
- return base.VisitNAryExpr(node);
- }
-
- BigInteger? AsIntLiteral(Expr e) {
- var lit = e as LiteralExpr;
- if (lit != null && lit.isBigNum) {
- BigNum bn = lit.asBigNum;
- return bn.ToBigInteger;
- }
- return null;
- }
- }
-
-}
+using System;
+using System.Numerics;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using Microsoft.Basetypes;
+
+namespace Microsoft.Boogie.AbstractInterpretation
+{
+ class NativeIntervallDomain : NativeLattice
+ {
+ abstract class E_Common : NativeLattice.Element { }
+ class E_Bottom : E_Common
+ {
+ public override Expr ToExpr() {
+ return Expr.False;
+ }
+ }
+ class E : E_Common
+ {
+ public readonly Node N;
+ public E() { }
+ public E(Node n) {
+ N = n;
+ }
+
+ public override Expr ToExpr() {
+ Expr expr = Expr.True;
+ for (var n = N; n != null; n = n.Next) {
+ expr = BplAnd(expr, n.ToExpr());
+ }
+ return expr;
+ }
+ }
+ public class Node
+ {
+ public readonly Variable V; // variable has type bool or int
+ // For an integer variable (Lo,Hi) indicates Lo <= V < Hi, where Lo==null means no lower bound and Hi==null means no upper bound.
+ // For a real variable (Lo,Hi) indicates Lo <= V <= Hi, where Lo==null means no lower bound and Hi==null means no upper bound.
+ // For a boolean variable, (Lo,Hi) is one of: (null,null) for {false,true}, (null,1) for {false}, and (1,null) for {true}.
+ public readonly BigInteger? Lo;
+ public readonly BigInteger? Hi;
+ public Node Next; // always sorted according to StrictlyBefore; readonly after full initialization
+ [Pure]
+ public static bool StrictlyBefore(Variable a, Variable b) {
+ Contract.Assert(a.UniqueId != b.UniqueId || a == b);
+ return a.UniqueId < b.UniqueId;
+ }
+
+ Node(Variable v, BigInteger? lo, BigInteger? hi, Node next) {
+ Contract.Requires(lo != null || hi != null); // don't accept empty constraints
+ Contract.Requires(next == null || StrictlyBefore(v, next.V));
+ V = v;
+ Lo = lo;
+ Hi = hi;
+ Next = next;
+ }
+
+ /// <summary>
+ /// This constructor leaves Next as null, allowing the caller to fill in Next to finish off the construction.
+ /// </summary>
+ public Node(Variable v, BigInteger? lo, BigInteger? hi) {
+ Contract.Requires(lo != null || hi != null); // don't accept empty constraints
+ V = v;
+ Lo = lo;
+ Hi = hi;
+ }
+
+ /// <summary>
+ /// Returns a Node that has the constraints head.{V,Lo,Hi} plus
+ /// all the constraints entailed by Nodes reachable from tail.
+ /// Requires that "head" sorts no later than anything in "tail".
+ /// Create either returns "head" itself or returns a new Node.
+ /// </summary>
+ public static Node Create(Node head, Node tail) {
+ Contract.Requires(head != null);
+ Contract.Requires(tail == null || !StrictlyBefore(tail.V, head.V));
+ Contract.Requires(head != tail);
+
+ if (head.Next == tail) {
+ return head;
+ } else if (tail != null && head.V == tail.V) {
+ // incorporate both constraints into one Node
+ return new Node(head.V, Max(head.Lo, tail.Lo, true), Min(head.Lo, tail.Lo, true), tail.Next);
+ } else {
+ return new Node(head.V, head.Lo, head.Hi, tail);
+ }
+ }
+
+ public static void GetBounds(Node n, Variable v, out BigInteger? lo, out BigInteger? hi) {
+ for (; n != null; n = n.Next) {
+ if (n.V == v) {
+ lo = n.Lo;
+ hi = n.Hi;
+ return;
+ } else if (StrictlyBefore(v, n.V)) {
+ break;
+ }
+ }
+ lo = null;
+ hi = null;
+ }
+
+ /// <summary>
+ /// Return the minimum of "a" and "b". If treatNullAsUnit==true, then "null" is
+ /// interpreted as positive infinity (the unit element of min); otherwise, it is
+ /// treated as negative infinity (the zero element of min).
+ /// </summary>
+ public static BigInteger? Min(BigInteger? a, BigInteger? b, bool treatNullAsUnit) {
+ if (a == null) {
+ return treatNullAsUnit ? b : a;
+ } else if (b == null) {
+ return treatNullAsUnit ? a : b;
+ } else {
+ return BigInteger.Min((BigInteger)a, (BigInteger)b);
+ }
+ }
+
+ /// <summary>
+ /// Return the maximum of "a" and "b". If treatNullAsUnit==true, then "null" is
+ /// interpreted as negative infinity (the unit element of max); otherwise, it is
+ /// treated as positive infinity (the zero element of max).
+ /// </summary>
+ public static BigInteger? Max(BigInteger? a, BigInteger? b, bool treatNullAsUnit) {
+ if (a == null) {
+ return treatNullAsUnit ? b : a;
+ } else if (b == null) {
+ return treatNullAsUnit ? a : b;
+ } else {
+ return BigInteger.Max((BigInteger)a, (BigInteger)b);
+ }
+ }
+
+ public static IEnumerable<Tuple<Node, Node>> Merge(Node a, Node b) {
+ while (true) {
+ if (a == null && b == null) {
+ yield break;
+ } else if (a == null || b == null) {
+ yield return new Tuple<Node, Node>(a, b);
+ if (a != null) { a = a.Next; } else { b = b.Next; }
+ } else if (a.V == b.V) {
+ yield return new Tuple<Node, Node>(a, b);
+ a = a.Next; b = b.Next;
+ } else if (StrictlyBefore(a.V, b.V)) {
+ yield return new Tuple<Node, Node>(a, null);
+ a = a.Next;
+ } else {
+ yield return new Tuple<Node, Node>(null, b);
+ b = b.Next;
+ }
+ }
+ }
+
+ public Expr ToExpr() {
+ if (!V.IsMutable && CommandLineOptions.Clo.InstrumentInfer != CommandLineOptions.InstrumentationPlaces.Everywhere) {
+ // omit invariants about readonly variables
+ return Expr.True;
+ } else if (V.TypedIdent.Type.IsBool) {
+ if (Lo == null && Hi == null) {
+ return Expr.True;
+ } else {
+ Contract.Assert((Lo == null && (BigInteger)Hi == 1) || (Hi == null && (BigInteger)Lo == 1));
+ var ide = new IdentifierExpr(Token.NoToken, V);
+ return Hi == null ? ide : Expr.Not(ide);
+ }
+ } else if (V.TypedIdent.Type.IsInt) {
+ Expr e = Expr.True;
+ if (Lo != null && Hi != null && Lo + 1 == Hi) {
+ // produce an equality
+ var ide = new IdentifierExpr(Token.NoToken, V);
+ e = Expr.And(e, BplEq(ide, NumberToExpr((BigInteger)Lo, V.TypedIdent.Type)));
+ } else {
+ // produce a (possibly empty) conjunction of inequalities
+ if (Lo != null) {
+ var ide = new IdentifierExpr(Token.NoToken, V);
+ e = Expr.And(e, BplLe(NumberToExpr((BigInteger)Lo, V.TypedIdent.Type), ide));
+ }
+ if (Hi != null) {
+ var ide = new IdentifierExpr(Token.NoToken, V);
+ e = Expr.And(e, BplLt(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type)));
+ }
+ }
+ return e;
+ } else if (V.TypedIdent.Type.IsReal){
+ Expr e = Expr.True;
+ if (Lo != null && Hi != null && Lo == Hi) {
+ // produce an equality
+ var ide = new IdentifierExpr(Token.NoToken, V);
+ e = Expr.And(e, BplEq(ide, NumberToExpr((BigInteger)Lo, V.TypedIdent.Type)));
+ } else {
+ // produce a (possibly empty) conjunction of inequalities
+ if (Lo != null) {
+ var ide = new IdentifierExpr(Token.NoToken, V);
+ e = Expr.And(e, BplLe(NumberToExpr((BigInteger)Lo, V.TypedIdent.Type), ide));
+ }
+ if (Hi != null) {
+ var ide = new IdentifierExpr(Token.NoToken, V);
+ e = Expr.And(e, BplLe(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type)));
+ }
+ }
+ return e;
+ } else {
+ Contract.Assert(V.TypedIdent.Type.IsFloat);
+ Expr e = Expr.True;
+ if (Lo != null && Hi != null && Lo == Hi)
+ {
+ // produce an equality
+ var ide = new IdentifierExpr(Token.NoToken, V);
+ e = Expr.And(e, BplEq(ide, NumberToExpr((BigInteger)Lo, V.TypedIdent.Type)));
+ }
+ else
+ {
+ // produce a (possibly empty) conjunction of inequalities
+ if (Lo != null)
+ {
+ var ide = new IdentifierExpr(Token.NoToken, V);
+ e = Expr.And(e, BplLe(NumberToExpr((BigInteger)Lo, V.TypedIdent.Type), ide));
+ }
+ if (Hi != null)
+ {
+ var ide = new IdentifierExpr(Token.NoToken, V);
+ e = Expr.And(e, BplLe(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type)));
+ }
+ }
+ return e;
+ }
+ }
+ }
+
+ static Expr NumberToExpr(BigInteger n, Type ty) {
+ if (n == null) {
+ return null;
+ } else if (ty.IsReal) {
+ return Expr.Literal(Basetypes.BigDec.FromBigInt(n));
+ } else if (ty.IsFloat) {
+ return Expr.Literal(Basetypes.BigFloat.FromBigInt(n, ty.FloatExponent, ty.FloatMantissa));
+ } else {
+ Contract.Assume(ty.IsInt);
+ return Expr.Literal(Basetypes.BigNum.FromBigInt(n));
+ }
+ }
+
+ List<BigInteger> upThresholds; // invariant: thresholds are sorted
+ List<BigInteger> downThresholds; // invariant: thresholds are sorted
+
+ /// <summary>
+ /// Requires "thresholds" to be sorted.
+ /// </summary>
+ public NativeIntervallDomain() {
+ upThresholds = new List<BigInteger>();
+ downThresholds = new List<BigInteger>();
+ }
+
+ public override void Specialize(Implementation impl) {
+ if (impl == null) {
+ // remove thresholds
+ upThresholds = new List<BigInteger>();
+ downThresholds = new List<BigInteger>();
+ } else {
+ var tf = new ThresholdFinder(impl);
+ tf.Find(out downThresholds, out upThresholds);
+#if DEBUG_PRINT
+ Console.Write("DEBUG: for implementation '{0}', setting downs to [", impl.Name);
+ foreach (var i in downThresholds) {
+ Console.Write(" {0}", i);
+ }
+ Console.Write(" ] and ups to [");
+ foreach (var i in upThresholds) {
+ Console.Write(" {0}", i);
+ }
+ Console.WriteLine(" ]");
+#endif
+ }
+ base.Specialize(impl);
+ }
+
+ private E_Common top = new E();
+ private E_Common bottom = new E_Bottom();
+
+ public override Element Top { get { return top; } }
+ public override Element Bottom { get { return bottom; } }
+
+ public override bool IsTop(Element element) {
+ var e = element as E;
+ return e != null && e.N == null;
+ }
+ public override bool IsBottom(Element element) {
+ return element is E_Bottom;
+ }
+
+ public override bool Below(Element a, Element b) {
+ if (a is E_Bottom) {
+ return true;
+ } else if (b is E_Bottom) {
+ return false;
+ } else {
+ var aa = (E)a;
+ var bb = (E)b;
+ // check if every constraint in 'bb' is implied by constraints in 'aa'
+ foreach (var t in Node.Merge(aa.N, bb.N)) {
+ var x = t.Item1;
+ var y = t.Item2;
+ if (x == null) {
+ // bb constrains a variable that aa does not
+ return false;
+ } else if (y == null) {
+ // aa constrains a variable that bb does not; that's fine
+ } else if (y.Lo != null && (x.Lo == null || x.Lo < y.Lo)) {
+ // bb has a Lo constraint, and either aa has no Lo constraint or it has a weaker Lo constraint
+ return false;
+ } else if (y.Hi != null && (x.Hi == null || y.Hi < x.Hi)) {
+ // bb has a Hi o constraint, and either aa has no Hi constraint or it has a weaker Hi constraint
+ return false;
+ }
+ }
+ return true;
+ }
+ }
+
+ public override Element Meet(Element a, Element b) {
+ if (a is E_Bottom) {
+ return a;
+ } else if (b is E_Bottom) {
+ return b;
+ } else {
+ var aa = (E)a;
+ var bb = (E)b;
+ Node head = null;
+ Node prev = null;
+ foreach (var t in Node.Merge(aa.N, bb.N)) {
+ var x = t.Item1;
+ var y = t.Item2;
+ Node n;
+ if (x == null) {
+ n = new Node(y.V, y.Lo, y.Hi);
+ } else if (y == null) {
+ n = new Node(x.V, x.Lo, x.Hi);
+ } else {
+ var lo = Node.Max(x.Lo, y.Lo, true);
+ var hi = Node.Min(x.Hi, y.Hi, true);
+ // if hi<=lo (or hi<lo for reals), then we're overconstrained
+ if (lo != null && hi != null && (x.V.TypedIdent.Type.IsReal ? hi < lo : hi <= lo)) {
+ return bottom;
+ }
+ n = new Node(x.V, lo, hi);
+ }
+ if (head == null) {
+ head = n;
+ } else {
+ prev.Next = n;
+ }
+ prev = n;
+ }
+ return new E(head);
+ }
+ }
+
+ public override Element Join(Element a, Element b) {
+ if (a is E_Bottom) {
+ return b;
+ } else if (b is E_Bottom) {
+ return a;
+ } else {
+ var aa = (E)a;
+ var bb = (E)b;
+ // for each variable, take the weaker of the constraints
+ Node head = null;
+ Node prev = null;
+ foreach (var t in Node.Merge(aa.N, bb.N)) {
+ if (t.Item1 != null && t.Item2 != null) {
+ var lo = Node.Min(t.Item1.Lo, t.Item2.Lo, false);
+ var hi = Node.Max(t.Item1.Hi, t.Item2.Hi, false);
+ if (lo != null || hi != null) {
+ var n = new Node(t.Item1.V, lo, hi);
+ if (head == null) {
+ head = n;
+ } else {
+ prev.Next = n;
+ }
+ prev = n;
+ }
+ }
+ }
+ return new E(head);
+ }
+ }
+
+ public override Element Widen(Element a, Element b) {
+ if (a is E_Bottom) {
+ return b; // since this is done just once, we maintain the ascending chains property
+ } else if (b is E_Bottom) {
+ return a;
+ } else {
+ var aa = (E)a;
+ var bb = (E)b;
+ // return a subset of the constraints of aa, namely those that are implied by bb
+ Node head = null;
+ Node prev = null;
+ foreach (var t in Node.Merge(aa.N, bb.N)) {
+ var x = t.Item1;
+ var y = t.Item2;
+ if (x != null && y != null) {
+ BigInteger? lo, hi;
+ lo = hi = null;
+ if (x.Lo != null && y.Lo != null) {
+ if (x.Lo <= y.Lo) {
+ // okay, we keep the lower bound
+ lo = x.Lo;
+ } else {
+ // set "lo" to the threshold that is below (or equal) y.Lo
+ lo = RoundDown((BigInteger)y.Lo);
+ }
+ }
+ if (x.Hi != null && y.Hi != null) {
+ if (y.Hi <= x.Hi) {
+ // okay, we keep the upper bound
+ hi = x.Hi;
+ } else {
+ // set "hi" to the threshold that is above (or equal) y.Hi
+ hi = RoundUp((BigInteger)y.Hi);
+ }
+ }
+ if (lo != null || hi != null) {
+ var n = new Node(x.V, lo, hi);
+ if (head == null) {
+ head = n;
+ } else {
+ prev.Next = n;
+ }
+ prev = n;
+ }
+ }
+ }
+ return new E(head);
+ }
+ }
+
+ /// <summary>
+ /// For a proof of correctness of this method, see Test/dafny2/Intervals.dfy.
+ /// A difference is that the this method returns:
+ /// let d = Dafny_RoundDown(k);
+ /// return d == -1 ? null : downThresholds[d];
+ /// </summary>
+ BigInteger? RoundDown(BigInteger k)
+ {
+ if (downThresholds.Count == 0 || k < downThresholds[0]) {
+ return null;
+ }
+ var i = 0;
+ var j = downThresholds.Count - 1;
+ while (i < j)
+ {
+ var mid = i + (j - i + 1) / 2;
+ if (downThresholds[mid] <= k) {
+ i = mid;
+ } else {
+ j = mid - 1;
+ }
+ }
+ return downThresholds[i];
+ }
+
+ /// <summary>
+ /// For a proof of correctness of this method, see Test/dafny2/Intervals.dfy.
+ /// A difference is that the this method returns:
+ /// let d = Dafny_RoundUp(k);
+ /// return d == thresholds.Count ? null : upThresholds[d];
+ /// </summary>
+ BigInteger? RoundUp(BigInteger k)
+ {
+ if (upThresholds.Count == 0 || upThresholds[upThresholds.Count - 1] < k) {
+ return null;
+ }
+ var i = 0;
+ var j = upThresholds.Count - 1;
+ while (i < j)
+ {
+ var mid = i + (j - i) / 2;
+ if (upThresholds[mid] < k) {
+ i = mid + 1;
+ } else {
+ j = mid;
+ }
+ }
+ return upThresholds[i];
+ }
+
+ public override Element Constrain(Element element, Expr expr) {
+ if (element is E_Bottom) {
+ return element;
+ } else {
+ var e = (E)element;
+ var c = Constraint(expr, e.N);
+ return c == null ? element : Meet(element, c);
+ }
+ }
+
+ /// <summary>
+ /// Returns an Element that corresponds to the constraints implied by "expr" in the
+ /// state "state".
+ /// Return "null" to indicate no constraints.
+ /// </summary>
+ E_Common Constraint(Expr expr, Node state) {
+ Variable v;
+ if (IsVariable(expr, out v)) {
+ var n = new Node(v, BigInteger.One, null);
+ return new E(n);
+ } else if (expr is LiteralExpr) {
+ var e = (LiteralExpr)expr;
+ return (bool)e.Val ? null : new E_Bottom();
+ } else if (expr is NAryExpr) {
+ var e = (NAryExpr)expr;
+ if (e.Fun is UnaryOperator) {
+ if (((UnaryOperator)e.Fun).Op == UnaryOperator.Opcode.Not) {
+ if (IsVariable(e.Args[0], out v)) {
+ var n = new Node(v, null, BigInteger.One);
+ return new E(n);
+ }
+ }
+ } else if (e.Fun is BinaryOperator) {
+ var op = ((BinaryOperator)e.Fun).Op;
+ var arg0 = e.Args[0];
+ var arg1 = e.Args[1];
+ switch (op) {
+ case BinaryOperator.Opcode.Eq:
+ case BinaryOperator.Opcode.Iff: {
+ E_Common c = null;
+ if (IsVariable(arg0, out v)) {
+ BigInteger? lo, hi;
+ if (PartiallyEvaluate(arg1, state, out lo, out hi)) {
+ var n = new Node(v, lo, hi);
+ c = new E(n);
+ }
+ }
+ if (IsVariable(arg1, out v)) {
+ BigInteger? lo, hi;
+ if (PartiallyEvaluate(arg1, state, out lo, out hi)) {
+ var n = new Node(v, lo, hi);
+ c = c == null ? new E(n) : (E_Common)Meet(c, new E(n));
+ }
+ }
+ return c;
+ }
+ case BinaryOperator.Opcode.Neq: {
+ E_Common c = null;
+ if (IsVariable(arg0, out v)) {
+ c = ConstrainNeq(state, v, arg1);
+ }
+ if (IsVariable(arg1, out v)) {
+ var cc = ConstrainNeq(state, v, arg0);
+ if (cc != null) {
+ c = c == null ? cc : (E_Common)Meet(c, cc);
+ }
+ }
+ return c;
+ }
+ case BinaryOperator.Opcode.Le: {
+ E_Common c = null;
+ if (IsVariable(arg1, out v)) {
+ BigInteger? lo, hi;
+ PartiallyEvaluate(arg0, state, out lo, out hi);
+ if (lo != null) {
+ var n = new Node(v, lo, null);
+ c = new E(n);
+ }
+ }
+ if (IsVariable(arg0, out v)) {
+ BigInteger? lo, hi;
+ PartiallyEvaluate(arg1, state, out lo, out hi);
+ if (hi != null) {
+ var n = new Node(v, null, hi);
+ c = c == null ? new E(n) : (E_Common)Meet(c, new E(n));
+ }
+ }
+ return c;
+ }
+ case BinaryOperator.Opcode.Lt: {
+ E_Common c = null;
+ if (IsVariable(arg1, out v)) {
+ BigInteger? lo, hi;
+ PartiallyEvaluate(arg0, state, out lo, out hi);
+ if (lo != null) {
+ var n = new Node(v, v.TypedIdent.Type.IsReal ? lo : lo + 1, null);
+ c = new E(n);
+ }
+ }
+ if (IsVariable(arg0, out v)) {
+ BigInteger? lo, hi;
+ PartiallyEvaluate(arg1, state, out lo, out hi);
+ if (hi != null) {
+ var n = new Node(v, null, v.TypedIdent.Type.IsReal ? hi : hi - 1);
+ c = c == null ? new E(n) : (E_Common)Meet(c, new E(n));
+ }
+ }
+ return c;
+ }
+ case BinaryOperator.Opcode.Ge: {
+ var tmp = arg0; arg0 = arg1; arg1 = tmp;
+ goto case BinaryOperator.Opcode.Le;
+ }
+ case BinaryOperator.Opcode.Gt: {
+ var tmp = arg0; arg0 = arg1; arg1 = tmp;
+ goto case BinaryOperator.Opcode.Lt;
+ }
+ default:
+ break;
+ }
+ }
+ }
+ return null; // approximation
+ }
+
+ private E ConstrainNeq(Node state, Variable v, Expr arg) {
+ BigInteger? lo, hi;
+ if (PartiallyEvaluate(arg, state, out lo, out hi)) {
+ if (!v.TypedIdent.Type.IsReal && lo != null && hi != null && lo + 1 == hi) {
+ var exclude = lo;
+ // If the partially evaluated arg (whose value is "exclude") is an end-point of
+ // the interval known for "v", then produce a constraint that excludes that bound.
+ Node.GetBounds(state, v, out lo, out hi);
+ if (lo != null && lo == exclude) {
+ var n = new Node(v, lo + 1, null);
+ return new E(n);
+ } else if (hi != null && exclude + 1 == hi) {
+ var n = new Node(v, null, exclude);
+ return new E(n);
+ }
+ }
+ }
+ return null;
+ }
+
+ bool IsVariable(Expr expr, out Variable v) {
+ var e = expr as IdentifierExpr;
+ if (e == null) {
+ v = null;
+ return false;
+ } else {
+ v = e.Decl;
+ return true;
+ }
+ }
+
+ public override Element Update(Element element, AssignCmd cmd) {
+ if (element is E_Bottom) {
+ return element;
+ }
+ var e = (E)element;
+ var nn = e.N;
+ Contract.Assert(cmd.Lhss.Count == cmd.Rhss.Count);
+ for (int i = 0; i < cmd.Lhss.Count; i++) {
+ var lhs = cmd.Lhss[i];
+ var rhs = cmd.Rhss[i];
+ BigInteger? lo;
+ BigInteger? hi;
+ PartiallyEvaluate(rhs, e.N, out lo, out hi);
+ nn = UpdateOne(nn, lhs.DeepAssignedVariable, lo, hi);
+ }
+ return new E(nn);
+ }
+
+ bool PartiallyEvaluate(Expr rhs, Node node, out BigInteger? lo, out BigInteger? hi) {
+ var pe = new PEVisitor(node);
+ pe.VisitExpr(rhs);
+ lo = pe.Lo;
+ hi = pe.Hi;
+ return lo != null || hi != null;
+ }
+
+ class PEVisitor : ReadOnlyVisitor
+ {
+ public BigInteger? Lo;
+ public BigInteger? Hi;
+
+ readonly BigInteger one = BigInteger.One;
+
+ Node N;
+ public PEVisitor(Node n) {
+ N = n;
+ }
+
+ // Override visitors for all expressions that can return a boolean, integer, or real result
+
+ public override Expr VisitExpr(Expr node) {
+ Lo = Hi = null;
+ return base.VisitExpr(node);
+ }
+ public override Expr VisitLiteralExpr(LiteralExpr node) {
+ if (node.Val is BigNum) {
+ var n = ((BigNum)node.Val).ToBigInteger;
+ Lo = n;
+ Hi = n + 1;
+ } else if (node.Val is BigDec) {
+ BigInteger floor, ceiling;
+ ((BigDec)node.Val).FloorCeiling(out floor, out ceiling);
+ Lo = floor;
+ Hi = ceiling;
+ } else if (node.Val is BigFloat) {
+ BigNum floor, ceiling;
+ ((BigFloat)node.Val).FloorCeiling(out floor, out ceiling);
+ Lo = floor.ToBigInteger;
+ Hi = ceiling.ToBigInteger;
+ } else if (node.Val is bool) {
+ if ((bool)node.Val) {
+ // true
+ Lo = one;
+ Hi = null;
+ } else {
+ // false
+ Lo = null;
+ Hi = one;
+ }
+ }
+ return node;
+ }
+ public override Expr VisitIdentifierExpr(IdentifierExpr node) {
+ if (node.Type.IsBool || node.Type.IsInt || node.Type.IsReal) {
+ Node.GetBounds(N, node.Decl, out Lo, out Hi);
+ }
+ return node;
+ }
+ public override Expr VisitNAryExpr(NAryExpr node) {
+ if (node.Fun is UnaryOperator) {
+ var op = (UnaryOperator)node.Fun;
+ Contract.Assert(node.Args.Count == 1);
+ if (op.Op == UnaryOperator.Opcode.Neg) {
+ BigInteger? lo, hi;
+ VisitExpr(node.Args[0]);
+ lo = Lo; hi = Hi;
+ if (hi != null) {
+ Lo = node.Type.IsReal ? -hi : 1 - hi;
+ } else {
+ Lo = null;
+ }
+ if (lo != null) {
+ Hi = node.Type.IsReal ? -lo : 1 - lo;
+ } else {
+ Hi = null;
+ }
+ }
+ else if (op.Op == UnaryOperator.Opcode.Not) {
+ VisitExpr(node.Args[0]);
+ Contract.Assert((Lo == null && Hi == null) ||
+ (Lo == null && (BigInteger)Hi == 1) ||
+ (Hi == null && (BigInteger)Lo == 1));
+ var tmp = Lo;
+ Lo = Hi;
+ Hi = tmp;
+ }
+ } else if (node.Fun is BinaryOperator) {
+ var op = (BinaryOperator)node.Fun;
+ Contract.Assert(node.Args.Count == 2);
+ BigInteger? lo0, hi0, lo1, hi1;
+ VisitExpr(node.Args[0]);
+ lo0 = Lo; hi0 = Hi;
+ VisitExpr(node.Args[1]);
+ lo1 = Lo; hi1 = Hi;
+ Lo = Hi = null;
+ var isReal = node.Args[0].Type.IsReal;
+ switch (op.Op) {
+ case BinaryOperator.Opcode.And:
+ if (hi0 != null || hi1 != null) {
+ // one operand is definitely false, thus so is the result
+ Lo = null; Hi = one;
+ } else if (lo0 != null && lo1 != null) {
+ // both operands are definitely true, thus so is the result
+ Lo = one; Hi = null;
+ }
+ break;
+ case BinaryOperator.Opcode.Or:
+ if (lo0 != null || lo1 != null) {
+ // one operand is definitely true, thus so is the result
+ Lo = one; Hi = null;
+ } else if (hi0 != null && hi1 != null) {
+ // both operands are definitely false, thus so is the result
+ Lo = null; Hi = one;
+ }
+ break;
+ case BinaryOperator.Opcode.Imp:
+ if (hi0 != null || lo1 != null) {
+ // either arg0 false or arg1 is true, so the result is true
+ Lo = one; Hi = null;
+ } else if (lo0 != null && hi1 != null) {
+ // arg0 is true and arg1 is false, so the result is false
+ Lo = null; Hi = one;
+ }
+ break;
+ case BinaryOperator.Opcode.Iff:
+ if (lo0 != null && lo1 != null) {
+ Lo = one; Hi = null;
+ } else if (hi0 != null && hi1 != null) {
+ Lo = one; Hi = null;
+ } else if (lo0 != null && hi1 != null) {
+ Lo = null; Hi = one;
+ } else if (hi0 != null && lo1 != null) {
+ Lo = null; Hi = one;
+ }
+ if (op.Op == BinaryOperator.Opcode.Neq) {
+ var tmp = Lo; Lo = Hi; Hi = tmp;
+ }
+ break;
+ case BinaryOperator.Opcode.Eq:
+ case BinaryOperator.Opcode.Neq:
+ if (node.Args[0].Type.IsBool) {
+ goto case BinaryOperator.Opcode.Iff;
+ }
+ // For Eq:
+ // If the (lo0,hi0) and (lo1,hi1) ranges do not overlap, the answer is false.
+ // If both ranges are the same unit range, then the answer is true.
+ if (hi0 != null && lo1 != null && (isReal ? hi0 < lo1 : hi0 <= lo1)) {
+ // no overlap
+ Lo = null; Hi = one;
+ } else if (lo0 != null && hi1 != null && (isReal ? hi1 < lo0 : hi1 <= lo0)) {
+ Lo = null; Hi = one;
+ // no overlaop
+ } else if (lo0 != null && hi0 != null && lo1 != null && hi1 != null &&
+ lo0 == lo1 && hi0 == hi1 && // ranges are the same
+ (isReal ? lo0 == hi0 : lo0 + 1 == hi0)) { // unit range
+ // both ranges are the same unit range
+ Lo = one; Hi = null;
+ }
+ if (op.Op == BinaryOperator.Opcode.Neq) {
+ var tmp = Lo; Lo = Hi; Hi = tmp;
+ }
+ break;
+ case BinaryOperator.Opcode.Le:
+ if (isReal) {
+ // If hi0 <= lo1, then the answer is true.
+ // If hi1 < lo0, then the answer is false.
+ if (hi0 != null && lo1 != null && hi0 <= lo1) {
+ Lo = one; Hi = null;
+ } else if (hi1 != null && lo0 != null && hi1 < lo0) {
+ Lo = null; Hi = one;
+ }
+ } else {
+ // If hi0 - 1 <= lo1, then the answer is true.
+ // If hi1 <= lo0, then the answer is false.
+ if (hi0 != null && lo1 != null && hi0 - 1 <= lo1) {
+ Lo = one; Hi = null;
+ } else if (lo0 != null && hi1 != null && hi1 <= lo0) {
+ Lo = null; Hi = one;
+ }
+ }
+ break;
+ case BinaryOperator.Opcode.Lt:
+ if (isReal) {
+ // If hi0 < lo1, then the answer is true.
+ // If hi1 <= lo0, then the answer is false.
+ if (hi0 != null && lo1 != null && hi0 < lo1) {
+ Lo = one; Hi = null;
+ } else if (hi1 != null && lo0 != null && hi1 <= lo0) {
+ Lo = null; Hi = one;
+ }
+ } else {
+ // If hi0 <= lo1, then the answer is true.
+ // If hi1 - 1 <= lo0, then the answer is false.
+ if (hi0 != null && lo1 != null && hi0 <= lo1) {
+ Lo = one; Hi = null;
+ } else if (lo0 != null && hi1 != null && hi1 - 1 <= lo0) {
+ Lo = null; Hi = one;
+ }
+ }
+ break;
+ case BinaryOperator.Opcode.Gt:
+ // swap the operands and then continue as Lt
+ {
+ var tmp = lo0; lo0 = lo1; lo1 = tmp;
+ tmp = hi0; hi0 = hi1; hi1 = tmp;
+ }
+ goto case BinaryOperator.Opcode.Lt;
+ case BinaryOperator.Opcode.Ge:
+ // swap the operands and then continue as Le
+ {
+ var tmp = lo0; lo0 = lo1; lo1 = tmp;
+ tmp = hi0; hi0 = hi1; hi1 = tmp;
+ }
+ goto case BinaryOperator.Opcode.Le;
+ case BinaryOperator.Opcode.Add:
+ if (lo0 != null && lo1 != null) {
+ Lo = lo0 + lo1;
+ }
+ if (hi0 != null && hi1 != null) {
+ Hi = isReal ? hi0 + hi1 : hi0 + hi1 - 1;
+ }
+ break;
+ case BinaryOperator.Opcode.Sub:
+ if (lo0 != null && hi1 != null) {
+ Lo = isReal ? lo0 - hi1 : lo0 - hi1 + 1;
+ }
+ if (hi0 != null && lo1 != null) {
+ Hi = hi0 - lo1;
+ }
+ break;
+ case BinaryOperator.Opcode.Mul:
+ // this uses an incomplete approximation that could be tightened up
+ if (lo0 != null && lo1 != null) {
+ if (0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
+ Lo = lo0 * lo1;
+ Hi = hi0 == null || hi1 == null ? null : isReal ? hi0 * hi1 : (hi0 - 1) * (hi1 - 1) + 1;
+ } else if ((BigInteger)lo0 < 0 && (BigInteger)lo1 < 0) {
+ Lo = null; // approximation
+ Hi = isReal ? lo0 * lo1 : lo0 * lo1 + 1;
+ }
+ }
+ break;
+ case BinaryOperator.Opcode.Div:
+ // this uses an incomplete approximation that could be tightened up
+ if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
+ Lo = BigInteger.Zero;
+ Hi = hi0;
+ }
+ break;
+ case BinaryOperator.Opcode.Mod:
+ // this uses an incomplete approximation that could be tightened up
+ if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
+ Lo = BigInteger.Zero;
+ Hi = hi1;
+ if (lo0 < lo1 && hi0 != null && hi0 < lo1) {
+ Lo = lo0;
+ Hi = hi0;
+ }
+ }
+ break;
+ case BinaryOperator.Opcode.RealDiv:
+ // this uses an incomplete approximation that could be tightened up
+ if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
+ Lo = BigInteger.Zero;
+ Hi = 1 <= (BigInteger)lo1 ? hi0 : null;
+ }
+ break;
+ case BinaryOperator.Opcode.Pow:
+ // this uses an incomplete approximation that could be tightened up
+ if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
+ Lo = 1 <= (BigInteger)lo1 ? BigInteger.One : BigInteger.Zero;
+ Hi = hi1;
+ }
+ break;
+ default:
+ break;
+ }
+ } else if (node.Fun is IfThenElse) {
+ var op = (IfThenElse)node.Fun;
+ Contract.Assert(node.Args.Count == 3);
+ BigInteger? guardLo, guardHi, lo0, hi0, lo1, hi1;
+ VisitExpr(node.Args[0]);
+ guardLo = Lo; guardHi = Hi;
+ VisitExpr(node.Args[1]);
+ lo0 = Lo; hi0 = Hi;
+ VisitExpr(node.Args[2]);
+ lo1 = Lo; hi1 = Hi;
+ Contract.Assert(guardLo == null || guardHi == null); // this is a consequence of the guard being boolean
+ if (guardLo != null) {
+ // guard is always true
+ Lo = lo0; Hi = hi0;
+ } else if (guardHi != null) {
+ // guard is always false
+ Lo = lo1; Hi = hi1;
+ } else {
+ // we don't know which branch will be taken, so join the information from the two branches
+ Lo = Node.Min(lo0, lo1, false);
+ Hi = Node.Max(hi0, hi1, false);
+ }
+ } else if (node.Fun is FunctionCall) {
+ var call = (FunctionCall)node.Fun;
+ // See if this is an identity function, which we do by checking: that the function has
+ // exactly one argument and the function has been marked by the user with the attribute {:identity}
+ bool claimsToBeIdentity = false;
+ if (call.ArgumentCount == 1 && call.Func.CheckBooleanAttribute("identity", ref claimsToBeIdentity) && claimsToBeIdentity && node.Args[0].Type.Equals(node.Type)) {
+ VisitExpr(node.Args[0]);
+ }
+ }
+ return node;
+ }
+ public override BinderExpr VisitBinderExpr(BinderExpr node) {
+ // don't recurse on subexpression
+ return node;
+ }
+ public override Expr VisitOldExpr(OldExpr node) {
+ // don't recurse on subexpression
+ return node;
+ }
+ public override Expr VisitCodeExpr(CodeExpr node) {
+ // don't recurse on subexpression
+ return node;
+ }
+ public override Expr VisitBvConcatExpr(BvConcatExpr node) {
+ // don't recurse on subexpression
+ return node;
+ }
+ public override Expr VisitBvExtractExpr(BvExtractExpr node) {
+ // don't recurse on subexpression
+ return node;
+ }
+ }
+
+ public override Element Eliminate(Element element, Variable v) {
+ if (element is E_Bottom) {
+ return element;
+ }
+ var e = (E)element;
+ var nn = UpdateOne(e.N, v, null, null);
+ if (nn == e.N) {
+ return element;
+ } else {
+ return new E(nn);
+ }
+ }
+
+ Node UpdateOne(Node nn, Variable v, BigInteger? lo, BigInteger? hi) {
+ var orig = nn;
+ Node head = null;
+ Node prev = null;
+ var foundV = false;
+ for (; nn != null && !Node.StrictlyBefore(v, nn.V); nn = nn.Next) {
+ if (nn.V == v) {
+ foundV = true;
+ nn = nn.Next;
+ break; // we found the place where the new node goes
+ } else {
+ var n = new Node(nn.V, nn.Lo, nn.Hi); // copy this Node
+ if (head == null) {
+ head = n;
+ } else {
+ prev.Next = n;
+ }
+ prev = n;
+ }
+ }
+ Node rest;
+ if (lo == null && hi == null) {
+ // eliminate all information about "v"
+ if (!foundV) {
+ return orig;
+ }
+ rest = nn;
+ } else {
+ rest = new Node(v, lo, hi);
+ rest.Next = nn;
+ }
+ if (head == null) {
+ head = rest;
+ } else {
+ prev.Next = rest;
+ }
+ return head;
+ }
+
+ /// <summary>
+ /// Return a resolved/type-checked expression that represents the conjunction of a and b.
+ /// Requires a and b to be resolved and type checked already.
+ /// </summary>
+ public static Expr BplAnd(Expr a, Expr b) {
+ if (a == Expr.True) {
+ return b;
+ } else if (b == Expr.True) {
+ return a;
+ } else {
+ var nary = Expr.Binary(BinaryOperator.Opcode.And, a, b);
+ nary.Type = Type.Bool;
+ nary.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+ return nary;
+ }
+ }
+
+ /// <summary>
+ /// Return a resolved/type-checked expression that represents a EQUALS b.
+ /// Requires a and b to be resolved and type checked already.
+ /// </summary>
+ public static Expr BplEq(Expr a, Expr b) {
+ var e = Expr.Eq(a, b);
+ e.Type = Type.Bool;
+ return e;
+ }
+
+ /// <summary>
+ /// Return a resolved/type-checked expression that represents a LESS-EQUAL b.
+ /// Requires a and b to be resolved and type checked already.
+ /// </summary>
+ public static Expr BplLe(Expr a, Expr b) {
+ var e = Expr.Le(a, b);
+ e.Type = Type.Bool;
+ return e;
+ }
+ /// <summary>
+ /// Return a resolved/type-checked expression that represents a LESS b.
+ /// Requires a and b to be resolved and type checked already.
+ /// </summary>
+ public static Expr BplLt(Expr a, Expr b) {
+ var e = Expr.Lt(a, b);
+ e.Type = Type.Bool;
+ return e;
+ }
+ }
+
+ public class ThresholdFinder : ReadOnlyVisitor
+ {
+ readonly Implementation Impl;
+ public ThresholdFinder(Implementation impl) {
+ Contract.Requires(impl != null);
+ Impl = impl;
+ }
+ HashSet<BigInteger> downs = new HashSet<BigInteger>();
+ HashSet<BigInteger> ups = new HashSet<BigInteger>();
+ public void Find(out List<BigInteger> downThresholds, out List<BigInteger> upThresholds) {
+ // always include -1, 0, 1 as down-thresholds
+ downs.Clear();
+ downs.Add(-1);
+ downs.Add(0);
+ downs.Add(1);
+ // always include 0 and 1 as up-thresholds
+ ups.Clear();
+ ups.Add(0);
+ ups.Add(1);
+
+ foreach (Requires p in Impl.Proc.Requires) {
+ Visit(p.Condition);
+ }
+ foreach (Ensures p in Impl.Proc.Ensures) {
+ Visit(p.Condition);
+ }
+ foreach (var b in Impl.Blocks) {
+ foreach (Cmd c in b.Cmds) {
+ Visit(c);
+ }
+ }
+
+ // convert the HashSets to sorted Lists and return
+ downThresholds = new List<BigInteger>();
+ foreach (var i in downs) {
+ downThresholds.Add(i);
+ }
+ downThresholds.Sort();
+ upThresholds = new List<BigInteger>();
+ foreach (var i in ups) {
+ upThresholds.Add(i);
+ }
+ upThresholds.Sort();
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr node) {
+ if (node.Fun is BinaryOperator) {
+ var op = (BinaryOperator)node.Fun;
+ Contract.Assert(node.Args.Count == 2);
+ var arg0 = node.Args[0];
+ var arg1 = node.Args[1];
+ var offset = arg0.Type.IsReal ? 0 : 1;
+ BigInteger? k;
+ switch (op.Op) {
+ case BinaryOperator.Opcode.Eq:
+ case BinaryOperator.Opcode.Neq:
+ k = AsIntLiteral(arg0);
+ if (k != null) {
+ var i = (BigInteger)k;
+ downs.Add(i - 1);
+ downs.Add(i);
+ ups.Add(i + 1);
+ ups.Add(i + 2);
+ }
+ k = AsIntLiteral(arg1);
+ if (k != null) {
+ var i = (BigInteger)k;
+ downs.Add(i - 1);
+ downs.Add(i);
+ ups.Add(i + 1);
+ ups.Add(i + 2);
+ }
+ break;
+ case BinaryOperator.Opcode.Le:
+ k = AsIntLiteral(arg0);
+ if (k != null) {
+ var i = (BigInteger)k;
+ downs.Add(i - 1);
+ downs.Add(i);
+ }
+ k = AsIntLiteral(arg1);
+ if (k != null) {
+ var i = (BigInteger)k;
+ ups.Add(i + offset);
+ ups.Add(i + 1 + offset);
+ }
+ break;
+ case BinaryOperator.Opcode.Lt:
+ k = AsIntLiteral(arg0);
+ if (k != null) {
+ var i = (BigInteger)k;
+ downs.Add(i );
+ downs.Add(i + 1);
+ }
+ k = AsIntLiteral(arg1);
+ if (k != null) {
+ var i = (BigInteger)k;
+ ups.Add(i - 1 + offset);
+ ups.Add(i + offset);
+ }
+ break;
+ case BinaryOperator.Opcode.Ge:
+ { var tmp = arg0; arg0 = arg1; arg1 = tmp; }
+ goto case BinaryOperator.Opcode.Le;
+ case BinaryOperator.Opcode.Gt:
+ { var tmp = arg0; arg0 = arg1; arg1 = tmp; }
+ goto case BinaryOperator.Opcode.Lt;
+ default:
+ break;
+ }
+ }
+ return base.VisitNAryExpr(node);
+ }
+
+ BigInteger? AsIntLiteral(Expr e) {
+ var lit = e as LiteralExpr;
+ if (lit != null && lit.isBigNum) {
+ BigNum bn = lit.asBigNum;
+ return bn.ToBigInteger;
+ }
+ return null;
+ }
+ }
+
+}
diff --git a/Source/AbsInt/NativeLattice.cs b/Source/AbsInt/NativeLattice.cs
index 30014643..d1ae215a 100644
--- a/Source/AbsInt/NativeLattice.cs
+++ b/Source/AbsInt/NativeLattice.cs
@@ -1,335 +1,335 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Diagnostics.Contracts;
-using Microsoft.Boogie;
-
-namespace Microsoft.Boogie.AbstractInterpretation
-{
- /// <summary>
- /// Specifies the operations (e.g., join) on a mathematical lattice that depend
- /// only on the elements of the lattice.
- /// </summary>
- public abstract class NativeLattice
- {
- /// <summary>
- /// An element of the lattice. This class should be derived from in any
- /// implementation of MathematicalLattice.
- /// </summary>
- public abstract class Element
- {
- public abstract Expr ToExpr();
- }
-
- public abstract Element Top { get; }
- public abstract Element Bottom { get; }
-
- public abstract bool IsTop(Element element);
- public abstract bool IsBottom(Element element);
-
- /// <summary>
- /// Is 'a' better (or equal) information than 'b'? That is, is 'a' below 'b' in the lattice?
- /// </summary>
- public abstract bool Below(Element a, Element b);
-
- public abstract Element Meet(Element a, Element b);
- public abstract Element Join(Element a, Element b);
- public abstract Element Widen(Element a, Element b);
-
- public abstract Element Constrain(Element element, Expr expr);
- public abstract Element Update(Element element, AssignCmd cmd); // requiers 'cmd' to be a simple (possibly parallel) assignment command
- public abstract Element Eliminate(Element element, Variable v);
-
- /// <summary>
- /// Specialize the lattice to implementation "impl", if non-null.
- /// If "impl" is null, remove specialization.
- /// </summary>
- public virtual void Specialize(Implementation impl) {
- }
-
- public virtual void Validate() {
- Contract.Assert(IsTop(Top));
- Contract.Assert(IsBottom(Bottom));
- Contract.Assert(!IsBottom(Top));
- Contract.Assert(!IsTop(Bottom));
-
- Contract.Assert(Below(Top, Top));
- Contract.Assert(Below(Bottom, Top));
- Contract.Assert(Below(Bottom, Bottom));
-
- Contract.Assert(IsTop(Join(Top, Top)));
- Contract.Assert(IsBottom(Join(Bottom, Bottom)));
- }
- }
-
- public class NativeAbstractInterpretation
- {
- public static void RunAbstractInterpretation(Program program) {
- Contract.Requires(program != null);
-
- if (!CommandLineOptions.Clo.UseAbstractInterpretation) {
- return;
- }
- Helpers.ExtraTraceInformation("Starting abstract interpretation");
-
- DateTime start = new DateTime(); // to please compiler's definite assignment rules
- if (CommandLineOptions.Clo.Trace) {
- Console.WriteLine();
- Console.WriteLine("Running abstract interpretation...");
- start = DateTime.UtcNow;
- }
-
- WidenPoints.Compute(program);
-
- NativeLattice lattice = null;
- if (CommandLineOptions.Clo.Ai.J_Trivial) {
- lattice = new TrivialDomain();
- } else if (CommandLineOptions.Clo.Ai.J_Intervals) {
- lattice = new NativeIntervallDomain();
- }
-
- if (lattice != null) {
- Dictionary<Procedure, Implementation[]> procedureImplementations = ComputeProcImplMap(program);
- ComputeProgramInvariants(program, procedureImplementations, lattice);
- if (CommandLineOptions.Clo.Ai.DebugStatistics) {
- Console.Error.WriteLine(lattice);
- }
- }
-
- if (CommandLineOptions.Clo.Trace) {
- DateTime end = DateTime.UtcNow;
- TimeSpan elapsed = end - start;
- Console.WriteLine(" [{0} s]", elapsed.TotalSeconds);
- Console.Out.Flush();
- }
- }
-
- private static Dictionary<Procedure, Implementation[]> ComputeProcImplMap(Program program) {
- Contract.Requires(program != null);
- // Since implementations call procedures (impl. signatures)
- // rather than directly calling other implementations, we first
- // need to compute which implementations implement which
- // procedures and remember which implementations call which
- // procedures.
-
- return program
- .Implementations
- .GroupBy(i => i.Proc).Select(g => g.ToArray()).ToDictionary(a => a[0].Proc);
- }
-
- /// <summary>
- /// Compute and apply the invariants for the program using the underlying abstract domain.
- /// </summary>
- public static void ComputeProgramInvariants(Program program, Dictionary<Procedure, Implementation[]> procedureImplementations, NativeLattice lattice) {
- Contract.Requires(program != null);
- Contract.Requires(procedureImplementations != null);
- Contract.Requires(lattice != null);
-
- // Gather all the axioms to create the initial lattice element
- // Differently stated, it is the \alpha from axioms (i.e. first order formulae) to the underlyng abstract domain
- var initialElement = lattice.Top;
- Contract.Assert(initialElement != null);
- foreach (var ax in program.Axioms) {
- initialElement = lattice.Constrain(initialElement, ax.Expr);
- }
-
- // analyze each procedure
- foreach (var proc in program.Procedures) {
- if (procedureImplementations.ContainsKey(proc)) {
- // analyze each implementation of the procedure
- foreach (var impl in procedureImplementations[proc]) {
- // add the precondition to the axioms
- Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());
- var start = initialElement;
- foreach (Requires pre in proc.Requires) {
- Expr e = Substituter.Apply(formalProcImplSubst, pre.Condition);
- start = lattice.Constrain(start, e);
- }
-
- lattice.Specialize(impl);
- Analyze(impl, lattice, start);
- lattice.Specialize(null);
- }
- }
- }
- }
-
- public static void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.Element start) {
- // We need to keep track of some information for each(some) block(s). To do that efficiently,
- // we number the implementation's blocks sequentially, and then we can use arrays to store
- // the additional information.
- var pre = new NativeLattice.Element[impl.Blocks.Count]; // set to null if we never compute a join/widen at this block
- var post = CommandLineOptions.Clo.InstrumentInfer == CommandLineOptions.InstrumentationPlaces.Everywhere ? new NativeLattice.Element[impl.Blocks.Count] : null;
- var iterations = new int[impl.Blocks.Count];
- var bottom = lattice.Bottom;
- int n = 0;
- foreach (var block in impl.Blocks) {
- block.aiId = n;
- // Note: The forward analysis below will store lattice elements in pre[n] if pre[n] is non-null.
- // Thus, the assignment "pre[n] = bottom;" below must be done under the following condition:
- // n == 0 || block.widenBlock
- // One possible strategy would be to do it only under that condition. Alternatively,
- // one could do the assignment under the following condition:
- // n == 0 || block.widenBlock || block.Predecessors.Length != 1
- // (which would require first setting the Predecessors field). In any case, if
- // CommandLineOptions.Clo.InstrumentInfer == CommandLineOptions.InstrumentationPlaces.Everywhere
- // then all pre[n] should be set.
- pre[n] = bottom;
- n++;
- }
- Contract.Assert(n == impl.Blocks.Count);
-
- var workItems = new Queue<Tuple<Block, NativeLattice.Element>>();
- workItems.Enqueue(new Tuple<Block, NativeLattice.Element>(impl.Blocks[0], start));
- //ComputeBlockInvariantsNative(impl, );
- // compute a fixpoint here
- while (workItems.Count > 0) {
- var workItem = workItems.Dequeue();
- var b = workItem.Item1;
- var id = b.aiId;
- var e = workItem.Item2;
- if (pre[id] == null) {
- // no pre information stored here, so just go ahead through the block
- } else if (lattice.Below(e, pre[id])) {
- // no change
- continue;
- } else if (b.widenBlock && CommandLineOptions.Clo.StepsBeforeWidening <= iterations[id]) {
- e = lattice.Widen(pre[id], e);
- pre[id] = e;
- iterations[id]++;
- } else {
- e = lattice.Join(pre[id], e);
- pre[id] = e;
- iterations[id]++;
- }
-
- // propagate'e' through b.Cmds
- foreach (Cmd cmd in b.Cmds) {
- e = Step(lattice, cmd, e);
- }
-
- if (post != null && pre[id] != null) {
- post[id] = e;
- }
-
- var g = b.TransferCmd as GotoCmd;
- if (g != null) { // if g==null, it's a pity we didn't pay attention to that earlier, because then we could have skipped analyzing the code in this block
- foreach (Block succ in g.labelTargets) {
- workItems.Enqueue(new Tuple<Block, NativeLattice.Element>(succ, e));
- }
- }
- }
-
- Instrument(impl, pre, post);
- }
-
- static void Instrument(Implementation impl, NativeLattice.Element[] pre, NativeLattice.Element[] post) {
- Contract.Requires(impl != null);
- Contract.Requires(pre != null);
-
- foreach (var b in impl.Blocks) {
- var element = pre[b.aiId];
- if (element != null && (b.widenBlock || CommandLineOptions.Clo.InstrumentInfer == CommandLineOptions.InstrumentationPlaces.Everywhere)) {
- List<Cmd> newCommands = new List<Cmd>();
- Expr inv = element.ToExpr();
- PredicateCmd cmd;
- var kv = new QKeyValue(Token.NoToken, "inferred", new List<object>(), null);
- if (CommandLineOptions.Clo.InstrumentWithAsserts) {
- cmd = new AssertCmd(Token.NoToken, inv, kv);
- } else {
- cmd = new AssumeCmd(Token.NoToken, inv, kv);
- }
- newCommands.Add(cmd);
- newCommands.AddRange(b.Cmds);
- if (post != null && post[b.aiId] != null) {
- inv = post[b.aiId].ToExpr();
- kv = new QKeyValue(Token.NoToken, "inferred", new List<object>(), null);
- if (CommandLineOptions.Clo.InstrumentWithAsserts) {
- cmd = new AssertCmd(Token.NoToken, inv, kv);
- } else {
- cmd = new AssumeCmd(Token.NoToken, inv, kv);
- }
- newCommands.Add(cmd);
- }
- b.Cmds = newCommands; // destructively replace the commands of the block
- }
- }
- }
-
- /// <summary>
- /// The abstract transition relation.
- /// 'cmd' is allowed to be a StateCmd.
- /// </summary>
- static NativeLattice.Element Step(NativeLattice lattice, Cmd cmd, NativeLattice.Element elmt) {
- Contract.Requires(lattice != null);
- Contract.Requires(cmd != null);
- Contract.Requires(elmt != null);
- Contract.Ensures(Contract.Result<NativeLattice.Element>() != null);
-
- if (cmd is AssignCmd) { // parallel assignment
- var c = (AssignCmd)cmd;
- elmt = lattice.Update(elmt, c.AsSimpleAssignCmd);
- } else if (cmd is HavocCmd) {
- var c = (HavocCmd)cmd;
- foreach (IdentifierExpr id in c.Vars) {
- Contract.Assert(id != null);
- elmt = lattice.Eliminate(elmt, id.Decl);
- }
- } else if (cmd is PredicateCmd) {
- var c = (PredicateCmd)cmd;
- var conjuncts = new List<Expr>();
- foreach (var ee in Conjuncts(c.Expr)) {
- Contract.Assert(ee != null);
- elmt = lattice.Constrain(elmt, ee);
- }
- } else if (cmd is StateCmd) {
- var c = (StateCmd)cmd;
- // Iterate the abstract transition on all the commands in the desugaring of the call
- foreach (Cmd callDesug in c.Cmds) {
- Contract.Assert(callDesug != null);
- elmt = Step(lattice, callDesug, elmt);
- }
- // Project out the local variables of the StateCmd
- foreach (Variable local in c.Locals) {
- Contract.Assert(local != null);
- elmt = lattice.Eliminate(elmt, local);
- }
- } else if (cmd is SugaredCmd) {
- var c = (SugaredCmd)cmd;
- elmt = Step(lattice, c.Desugaring, elmt);
- } else if (cmd is CommentCmd) {
- // skip
- } else {
- Contract.Assert(false); // unknown command
- }
- return elmt;
- }
-
- /// <summary>
- /// Yields the conjuncts of 'expr'.
- /// </summary>
- public static IEnumerable<Expr> Conjuncts(Expr expr) {
- Contract.Requires(expr != null);
-
- var e = expr as NAryExpr;
- if (e != null && e.Fun.FunctionName == "&&") { // if it is a conjunction
- foreach (Expr ee in e.Args) {
- Contract.Assert(ee != null);
- foreach (var c in Conjuncts(ee)) {
- yield return c;
- }
- }
- } else {
- yield return expr;
- }
- }
-
- }
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics.Contracts;
+using Microsoft.Boogie;
+
+namespace Microsoft.Boogie.AbstractInterpretation
+{
+ /// <summary>
+ /// Specifies the operations (e.g., join) on a mathematical lattice that depend
+ /// only on the elements of the lattice.
+ /// </summary>
+ public abstract class NativeLattice
+ {
+ /// <summary>
+ /// An element of the lattice. This class should be derived from in any
+ /// implementation of MathematicalLattice.
+ /// </summary>
+ public abstract class Element
+ {
+ public abstract Expr ToExpr();
+ }
+
+ public abstract Element Top { get; }
+ public abstract Element Bottom { get; }
+
+ public abstract bool IsTop(Element element);
+ public abstract bool IsBottom(Element element);
+
+ /// <summary>
+ /// Is 'a' better (or equal) information than 'b'? That is, is 'a' below 'b' in the lattice?
+ /// </summary>
+ public abstract bool Below(Element a, Element b);
+
+ public abstract Element Meet(Element a, Element b);
+ public abstract Element Join(Element a, Element b);
+ public abstract Element Widen(Element a, Element b);
+
+ public abstract Element Constrain(Element element, Expr expr);
+ public abstract Element Update(Element element, AssignCmd cmd); // requiers 'cmd' to be a simple (possibly parallel) assignment command
+ public abstract Element Eliminate(Element element, Variable v);
+
+ /// <summary>
+ /// Specialize the lattice to implementation "impl", if non-null.
+ /// If "impl" is null, remove specialization.
+ /// </summary>
+ public virtual void Specialize(Implementation impl) {
+ }
+
+ public virtual void Validate() {
+ Contract.Assert(IsTop(Top));
+ Contract.Assert(IsBottom(Bottom));
+ Contract.Assert(!IsBottom(Top));
+ Contract.Assert(!IsTop(Bottom));
+
+ Contract.Assert(Below(Top, Top));
+ Contract.Assert(Below(Bottom, Top));
+ Contract.Assert(Below(Bottom, Bottom));
+
+ Contract.Assert(IsTop(Join(Top, Top)));
+ Contract.Assert(IsBottom(Join(Bottom, Bottom)));
+ }
+ }
+
+ public class NativeAbstractInterpretation
+ {
+ public static void RunAbstractInterpretation(Program program) {
+ Contract.Requires(program != null);
+
+ if (!CommandLineOptions.Clo.UseAbstractInterpretation) {
+ return;
+ }
+ Helpers.ExtraTraceInformation("Starting abstract interpretation");
+
+ DateTime start = new DateTime(); // to please compiler's definite assignment rules
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine();
+ Console.WriteLine("Running abstract interpretation...");
+ start = DateTime.UtcNow;
+ }
+
+ WidenPoints.Compute(program);
+
+ NativeLattice lattice = null;
+ if (CommandLineOptions.Clo.Ai.J_Trivial) {
+ lattice = new TrivialDomain();
+ } else if (CommandLineOptions.Clo.Ai.J_Intervals) {
+ lattice = new NativeIntervallDomain();
+ }
+
+ if (lattice != null) {
+ Dictionary<Procedure, Implementation[]> procedureImplementations = ComputeProcImplMap(program);
+ ComputeProgramInvariants(program, procedureImplementations, lattice);
+ if (CommandLineOptions.Clo.Ai.DebugStatistics) {
+ Console.Error.WriteLine(lattice);
+ }
+ }
+
+ if (CommandLineOptions.Clo.Trace) {
+ DateTime end = DateTime.UtcNow;
+ TimeSpan elapsed = end - start;
+ Console.WriteLine(" [{0} s]", elapsed.TotalSeconds);
+ Console.Out.Flush();
+ }
+ }
+
+ private static Dictionary<Procedure, Implementation[]> ComputeProcImplMap(Program program) {
+ Contract.Requires(program != null);
+ // Since implementations call procedures (impl. signatures)
+ // rather than directly calling other implementations, we first
+ // need to compute which implementations implement which
+ // procedures and remember which implementations call which
+ // procedures.
+
+ return program
+ .Implementations
+ .GroupBy(i => i.Proc).Select(g => g.ToArray()).ToDictionary(a => a[0].Proc);
+ }
+
+ /// <summary>
+ /// Compute and apply the invariants for the program using the underlying abstract domain.
+ /// </summary>
+ public static void ComputeProgramInvariants(Program program, Dictionary<Procedure, Implementation[]> procedureImplementations, NativeLattice lattice) {
+ Contract.Requires(program != null);
+ Contract.Requires(procedureImplementations != null);
+ Contract.Requires(lattice != null);
+
+ // Gather all the axioms to create the initial lattice element
+ // Differently stated, it is the \alpha from axioms (i.e. first order formulae) to the underlyng abstract domain
+ var initialElement = lattice.Top;
+ Contract.Assert(initialElement != null);
+ foreach (var ax in program.Axioms) {
+ initialElement = lattice.Constrain(initialElement, ax.Expr);
+ }
+
+ // analyze each procedure
+ foreach (var proc in program.Procedures) {
+ if (procedureImplementations.ContainsKey(proc)) {
+ // analyze each implementation of the procedure
+ foreach (var impl in procedureImplementations[proc]) {
+ // add the precondition to the axioms
+ Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());
+ var start = initialElement;
+ foreach (Requires pre in proc.Requires) {
+ Expr e = Substituter.Apply(formalProcImplSubst, pre.Condition);
+ start = lattice.Constrain(start, e);
+ }
+
+ lattice.Specialize(impl);
+ Analyze(impl, lattice, start);
+ lattice.Specialize(null);
+ }
+ }
+ }
+ }
+
+ public static void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.Element start) {
+ // We need to keep track of some information for each(some) block(s). To do that efficiently,
+ // we number the implementation's blocks sequentially, and then we can use arrays to store
+ // the additional information.
+ var pre = new NativeLattice.Element[impl.Blocks.Count]; // set to null if we never compute a join/widen at this block
+ var post = CommandLineOptions.Clo.InstrumentInfer == CommandLineOptions.InstrumentationPlaces.Everywhere ? new NativeLattice.Element[impl.Blocks.Count] : null;
+ var iterations = new int[impl.Blocks.Count];
+ var bottom = lattice.Bottom;
+ int n = 0;
+ foreach (var block in impl.Blocks) {
+ block.aiId = n;
+ // Note: The forward analysis below will store lattice elements in pre[n] if pre[n] is non-null.
+ // Thus, the assignment "pre[n] = bottom;" below must be done under the following condition:
+ // n == 0 || block.widenBlock
+ // One possible strategy would be to do it only under that condition. Alternatively,
+ // one could do the assignment under the following condition:
+ // n == 0 || block.widenBlock || block.Predecessors.Length != 1
+ // (which would require first setting the Predecessors field). In any case, if
+ // CommandLineOptions.Clo.InstrumentInfer == CommandLineOptions.InstrumentationPlaces.Everywhere
+ // then all pre[n] should be set.
+ pre[n] = bottom;
+ n++;
+ }
+ Contract.Assert(n == impl.Blocks.Count);
+
+ var workItems = new Queue<Tuple<Block, NativeLattice.Element>>();
+ workItems.Enqueue(new Tuple<Block, NativeLattice.Element>(impl.Blocks[0], start));
+ //ComputeBlockInvariantsNative(impl, );
+ // compute a fixpoint here
+ while (workItems.Count > 0) {
+ var workItem = workItems.Dequeue();
+ var b = workItem.Item1;
+ var id = b.aiId;
+ var e = workItem.Item2;
+ if (pre[id] == null) {
+ // no pre information stored here, so just go ahead through the block
+ } else if (lattice.Below(e, pre[id])) {
+ // no change
+ continue;
+ } else if (b.widenBlock && CommandLineOptions.Clo.StepsBeforeWidening <= iterations[id]) {
+ e = lattice.Widen(pre[id], e);
+ pre[id] = e;
+ iterations[id]++;
+ } else {
+ e = lattice.Join(pre[id], e);
+ pre[id] = e;
+ iterations[id]++;
+ }
+
+ // propagate'e' through b.Cmds
+ foreach (Cmd cmd in b.Cmds) {
+ e = Step(lattice, cmd, e);
+ }
+
+ if (post != null && pre[id] != null) {
+ post[id] = e;
+ }
+
+ var g = b.TransferCmd as GotoCmd;
+ if (g != null) { // if g==null, it's a pity we didn't pay attention to that earlier, because then we could have skipped analyzing the code in this block
+ foreach (Block succ in g.labelTargets) {
+ workItems.Enqueue(new Tuple<Block, NativeLattice.Element>(succ, e));
+ }
+ }
+ }
+
+ Instrument(impl, pre, post);
+ }
+
+ static void Instrument(Implementation impl, NativeLattice.Element[] pre, NativeLattice.Element[] post) {
+ Contract.Requires(impl != null);
+ Contract.Requires(pre != null);
+
+ foreach (var b in impl.Blocks) {
+ var element = pre[b.aiId];
+ if (element != null && (b.widenBlock || CommandLineOptions.Clo.InstrumentInfer == CommandLineOptions.InstrumentationPlaces.Everywhere)) {
+ List<Cmd> newCommands = new List<Cmd>();
+ Expr inv = element.ToExpr();
+ PredicateCmd cmd;
+ var kv = new QKeyValue(Token.NoToken, "inferred", new List<object>(), null);
+ if (CommandLineOptions.Clo.InstrumentWithAsserts) {
+ cmd = new AssertCmd(Token.NoToken, inv, kv);
+ } else {
+ cmd = new AssumeCmd(Token.NoToken, inv, kv);
+ }
+ newCommands.Add(cmd);
+ newCommands.AddRange(b.Cmds);
+ if (post != null && post[b.aiId] != null) {
+ inv = post[b.aiId].ToExpr();
+ kv = new QKeyValue(Token.NoToken, "inferred", new List<object>(), null);
+ if (CommandLineOptions.Clo.InstrumentWithAsserts) {
+ cmd = new AssertCmd(Token.NoToken, inv, kv);
+ } else {
+ cmd = new AssumeCmd(Token.NoToken, inv, kv);
+ }
+ newCommands.Add(cmd);
+ }
+ b.Cmds = newCommands; // destructively replace the commands of the block
+ }
+ }
+ }
+
+ /// <summary>
+ /// The abstract transition relation.
+ /// 'cmd' is allowed to be a StateCmd.
+ /// </summary>
+ static NativeLattice.Element Step(NativeLattice lattice, Cmd cmd, NativeLattice.Element elmt) {
+ Contract.Requires(lattice != null);
+ Contract.Requires(cmd != null);
+ Contract.Requires(elmt != null);
+ Contract.Ensures(Contract.Result<NativeLattice.Element>() != null);
+
+ if (cmd is AssignCmd) { // parallel assignment
+ var c = (AssignCmd)cmd;
+ elmt = lattice.Update(elmt, c.AsSimpleAssignCmd);
+ } else if (cmd is HavocCmd) {
+ var c = (HavocCmd)cmd;
+ foreach (IdentifierExpr id in c.Vars) {
+ Contract.Assert(id != null);
+ elmt = lattice.Eliminate(elmt, id.Decl);
+ }
+ } else if (cmd is PredicateCmd) {
+ var c = (PredicateCmd)cmd;
+ var conjuncts = new List<Expr>();
+ foreach (var ee in Conjuncts(c.Expr)) {
+ Contract.Assert(ee != null);
+ elmt = lattice.Constrain(elmt, ee);
+ }
+ } else if (cmd is StateCmd) {
+ var c = (StateCmd)cmd;
+ // Iterate the abstract transition on all the commands in the desugaring of the call
+ foreach (Cmd callDesug in c.Cmds) {
+ Contract.Assert(callDesug != null);
+ elmt = Step(lattice, callDesug, elmt);
+ }
+ // Project out the local variables of the StateCmd
+ foreach (Variable local in c.Locals) {
+ Contract.Assert(local != null);
+ elmt = lattice.Eliminate(elmt, local);
+ }
+ } else if (cmd is SugaredCmd) {
+ var c = (SugaredCmd)cmd;
+ elmt = Step(lattice, c.Desugaring, elmt);
+ } else if (cmd is CommentCmd) {
+ // skip
+ } else {
+ Contract.Assert(false); // unknown command
+ }
+ return elmt;
+ }
+
+ /// <summary>
+ /// Yields the conjuncts of 'expr'.
+ /// </summary>
+ public static IEnumerable<Expr> Conjuncts(Expr expr) {
+ Contract.Requires(expr != null);
+
+ var e = expr as NAryExpr;
+ if (e != null && e.Fun.FunctionName == "&&") { // if it is a conjunction
+ foreach (Expr ee in e.Args) {
+ Contract.Assert(ee != null);
+ foreach (var c in Conjuncts(ee)) {
+ yield return c;
+ }
+ }
+ } else {
+ yield return expr;
+ }
+ }
+
+ }
+}
diff --git a/Source/AbsInt/Traverse.cs b/Source/AbsInt/Traverse.cs
index 184a4071..92377e56 100644
--- a/Source/AbsInt/Traverse.cs
+++ b/Source/AbsInt/Traverse.cs
@@ -1,169 +1,169 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-namespace Microsoft.Boogie {
- using System;
- using System.Collections.Generic;
- using System.Diagnostics.Contracts;
-
-
- /// <summary>
- /// This class provides the functionality of traversing a program to determine which
- /// blocks are blocks where the widening operator may need to be applied. Assumes
- /// all 'currentlyTraversed' bits to be initially false, and leaves them that way in
- /// the end. Assumes the 'widenBlock' bits are initially false, and sets them
- /// appropriately.
- /// </summary>
- public class WidenPoints {
- /// <summary>
- /// Compute the widen points of a program
- /// </summary>
- public static void Compute(Program program) {
- Contract.Requires(program != null);
- cce.BeginExpose(program);
-
- foreach (var impl in program.Implementations) {
- if (impl.Blocks != null && impl.Blocks.Count > 0) {
- Contract.Assume(cce.IsConsistent(impl));
- cce.BeginExpose(impl);
- Block start = impl.Blocks[0];
- Contract.Assume(start != null);
- Contract.Assume(cce.IsConsistent(start));
- Visit(start);
-
- // We reset the state...
- foreach (Block b in impl.Blocks) {
- cce.BeginExpose(b);
- b.TraversingStatus = Block.VisitState.ToVisit;
- cce.EndExpose();
- }
- cce.EndExpose();
- }
- }
- cce.EndExpose();
- }
-
- static void Visit(Block b) {
- Contract.Requires(b != null);
- Contract.Assume(cce.IsExposable(b));
- if (b.TraversingStatus == Block.VisitState.BeingVisited) {
- cce.BeginExpose(b);
- // we got here through a back-edge
- b.widenBlock = true;
- cce.EndExpose();
- } else if (b.TraversingStatus == Block.VisitState.AlreadyVisited) {
- // do nothing... we already saw this node
- } else if (b.TransferCmd is GotoCmd) {
- Contract.Assert(b.TraversingStatus == Block.VisitState.ToVisit);
-
- GotoCmd g = (GotoCmd)b.TransferCmd;
- cce.BeginExpose(b);
-
- cce.BeginExpose(g); //PM: required for the subsequent expose (g.labelTargets)
- b.TraversingStatus = Block.VisitState.BeingVisited;
-
- // labelTargets is made non-null by Resolve, which we assume
- // has already called in a prior pass.
- Contract.Assume(g.labelTargets != null);
- cce.BeginExpose(g.labelTargets);
- foreach (Block succ in g.labelTargets)
- // invariant b.currentlyTraversed;
- //PM: The following loop invariant will work once properties are axiomatized
- //&& (g.labelNames != null && g.labelTargets != null ==> g.labelNames.Length == g.labelTargets.Length);
- {
- Contract.Assert(succ != null);
- Visit(succ);
- }
- cce.EndExpose();
-
- Contract.Assert(b.TraversingStatus == Block.VisitState.BeingVisited);
- // System.Diagnostics.Debug.Assert(b.currentlyTraversed);
-
- b.TraversingStatus = Block.VisitState.AlreadyVisited;
-
- //PM: The folowing assumption is needed because we cannot prove that a simple field update
- //PM: leaves the value of a property unchanged.
- Contract.Assume(g.labelNames == null || g.labelNames.Count == g.labelTargets.Count);
- cce.EndExpose();
- } else {
- Contract.Assert(b.TransferCmd == null || b.TransferCmd is ReturnCmd); // It must be a returnCmd;
- }
- }
-
- static private Block rootBlock = null; // The root point we have to consider
-
- /// <summary>
- /// Compute the blocks in the body loop.
- /// <param name ="block"> Tt is the head of the loop. It must be a widen block </param>
- /// <return> The blocks that are in the loop from block </return>
- /// </summary>
- public static List<Block> ComputeLoopBodyFrom(Block block) {
- Contract.Requires(block.widenBlock);
- Contract.Requires(block != null);
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
-
- Contract.Assert(rootBlock == null);
- rootBlock = block;
-
- List<Block/*!*/> blocksInLoop = new List<Block/*!*/>(); // We use a list just because .net does not define a set
- List<Block/*!*/> visitingPath = new List<Block/*!*/>(); // The order is important, as we want paths
-
- blocksInLoop.Add(block);
-
- DoDFSVisit(block, visitingPath, blocksInLoop);
-
- visitingPath.Add(block);
-
-
- rootBlock = null; // We reset the invariant
-
- return blocksInLoop;
- }
-
- /// <summary>
- /// Perform the Depth-first search of the so to find the loop
- /// <param name = "block"> The block to visit </param>
- /// <param name = "path"> The path we are visiting so far </param>
- /// </summary>
- private static void DoDFSVisit(Block block, List<Block> path, List<Block> blocksInPath) {
- Contract.Requires(block != null);
- Contract.Requires(cce.NonNullElements(path));
- Contract.Requires(cce.NonNullElements(path));
- #region case 1. We visit the root => We are done, "path" is a path inside the loop
- if (block == rootBlock && path.Count > 1) {
- blocksInPath.AddRange(path); // Add all the blocks in this path
- }
-
- #endregion
- #region case 2. We visit a node that ends with a return => "path" is not inside the loop
- if (block.TransferCmd is ReturnCmd) {
- return;
- }
- #endregion
- #region case 3. We visit a node with successors => continue the exploration of its successors
- {
- Contract.Assert(block.TransferCmd is GotoCmd);
- GotoCmd successors = (GotoCmd)block.TransferCmd;
- Contract.Assert(successors != null);
-
- if (successors.labelTargets != null)
- foreach (Block nextBlock in successors.labelTargets) {
- Contract.Assert(nextBlock != null);
- if (path.Contains(nextBlock)) // If the current path has already seen the block, just skip it
- continue;
- // Otherwise we perform the DFS visit
- path.Add(nextBlock);
- DoDFSVisit(nextBlock, path, blocksInPath);
-
- Contract.Assert(nextBlock == path[path.Count - 1]);
- path.RemoveAt(path.Count - 1);
- }
-
- }
-
- #endregion
- }
- }
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.Boogie {
+ using System;
+ using System.Collections.Generic;
+ using System.Diagnostics.Contracts;
+
+
+ /// <summary>
+ /// This class provides the functionality of traversing a program to determine which
+ /// blocks are blocks where the widening operator may need to be applied. Assumes
+ /// all 'currentlyTraversed' bits to be initially false, and leaves them that way in
+ /// the end. Assumes the 'widenBlock' bits are initially false, and sets them
+ /// appropriately.
+ /// </summary>
+ public class WidenPoints {
+ /// <summary>
+ /// Compute the widen points of a program
+ /// </summary>
+ public static void Compute(Program program) {
+ Contract.Requires(program != null);
+ cce.BeginExpose(program);
+
+ foreach (var impl in program.Implementations) {
+ if (impl.Blocks != null && impl.Blocks.Count > 0) {
+ Contract.Assume(cce.IsConsistent(impl));
+ cce.BeginExpose(impl);
+ Block start = impl.Blocks[0];
+ Contract.Assume(start != null);
+ Contract.Assume(cce.IsConsistent(start));
+ Visit(start);
+
+ // We reset the state...
+ foreach (Block b in impl.Blocks) {
+ cce.BeginExpose(b);
+ b.TraversingStatus = Block.VisitState.ToVisit;
+ cce.EndExpose();
+ }
+ cce.EndExpose();
+ }
+ }
+ cce.EndExpose();
+ }
+
+ static void Visit(Block b) {
+ Contract.Requires(b != null);
+ Contract.Assume(cce.IsExposable(b));
+ if (b.TraversingStatus == Block.VisitState.BeingVisited) {
+ cce.BeginExpose(b);
+ // we got here through a back-edge
+ b.widenBlock = true;
+ cce.EndExpose();
+ } else if (b.TraversingStatus == Block.VisitState.AlreadyVisited) {
+ // do nothing... we already saw this node
+ } else if (b.TransferCmd is GotoCmd) {
+ Contract.Assert(b.TraversingStatus == Block.VisitState.ToVisit);
+
+ GotoCmd g = (GotoCmd)b.TransferCmd;
+ cce.BeginExpose(b);
+
+ cce.BeginExpose(g); //PM: required for the subsequent expose (g.labelTargets)
+ b.TraversingStatus = Block.VisitState.BeingVisited;
+
+ // labelTargets is made non-null by Resolve, which we assume
+ // has already called in a prior pass.
+ Contract.Assume(g.labelTargets != null);
+ cce.BeginExpose(g.labelTargets);
+ foreach (Block succ in g.labelTargets)
+ // invariant b.currentlyTraversed;
+ //PM: The following loop invariant will work once properties are axiomatized
+ //&& (g.labelNames != null && g.labelTargets != null ==> g.labelNames.Length == g.labelTargets.Length);
+ {
+ Contract.Assert(succ != null);
+ Visit(succ);
+ }
+ cce.EndExpose();
+
+ Contract.Assert(b.TraversingStatus == Block.VisitState.BeingVisited);
+ // System.Diagnostics.Debug.Assert(b.currentlyTraversed);
+
+ b.TraversingStatus = Block.VisitState.AlreadyVisited;
+
+ //PM: The folowing assumption is needed because we cannot prove that a simple field update
+ //PM: leaves the value of a property unchanged.
+ Contract.Assume(g.labelNames == null || g.labelNames.Count == g.labelTargets.Count);
+ cce.EndExpose();
+ } else {
+ Contract.Assert(b.TransferCmd == null || b.TransferCmd is ReturnCmd); // It must be a returnCmd;
+ }
+ }
+
+ static private Block rootBlock = null; // The root point we have to consider
+
+ /// <summary>
+ /// Compute the blocks in the body loop.
+ /// <param name ="block"> Tt is the head of the loop. It must be a widen block </param>
+ /// <return> The blocks that are in the loop from block </return>
+ /// </summary>
+ public static List<Block> ComputeLoopBodyFrom(Block block) {
+ Contract.Requires(block.widenBlock);
+ Contract.Requires(block != null);
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
+
+ Contract.Assert(rootBlock == null);
+ rootBlock = block;
+
+ List<Block/*!*/> blocksInLoop = new List<Block/*!*/>(); // We use a list just because .net does not define a set
+ List<Block/*!*/> visitingPath = new List<Block/*!*/>(); // The order is important, as we want paths
+
+ blocksInLoop.Add(block);
+
+ DoDFSVisit(block, visitingPath, blocksInLoop);
+
+ visitingPath.Add(block);
+
+
+ rootBlock = null; // We reset the invariant
+
+ return blocksInLoop;
+ }
+
+ /// <summary>
+ /// Perform the Depth-first search of the so to find the loop
+ /// <param name = "block"> The block to visit </param>
+ /// <param name = "path"> The path we are visiting so far </param>
+ /// </summary>
+ private static void DoDFSVisit(Block block, List<Block> path, List<Block> blocksInPath) {
+ Contract.Requires(block != null);
+ Contract.Requires(cce.NonNullElements(path));
+ Contract.Requires(cce.NonNullElements(path));
+ #region case 1. We visit the root => We are done, "path" is a path inside the loop
+ if (block == rootBlock && path.Count > 1) {
+ blocksInPath.AddRange(path); // Add all the blocks in this path
+ }
+
+ #endregion
+ #region case 2. We visit a node that ends with a return => "path" is not inside the loop
+ if (block.TransferCmd is ReturnCmd) {
+ return;
+ }
+ #endregion
+ #region case 3. We visit a node with successors => continue the exploration of its successors
+ {
+ Contract.Assert(block.TransferCmd is GotoCmd);
+ GotoCmd successors = (GotoCmd)block.TransferCmd;
+ Contract.Assert(successors != null);
+
+ if (successors.labelTargets != null)
+ foreach (Block nextBlock in successors.labelTargets) {
+ Contract.Assert(nextBlock != null);
+ if (path.Contains(nextBlock)) // If the current path has already seen the block, just skip it
+ continue;
+ // Otherwise we perform the DFS visit
+ path.Add(nextBlock);
+ DoDFSVisit(nextBlock, path, blocksInPath);
+
+ Contract.Assert(nextBlock == path[path.Count - 1]);
+ path.RemoveAt(path.Count - 1);
+ }
+
+ }
+
+ #endregion
+ }
+ }
+}
diff --git a/Source/AbsInt/TrivialDomain.cs b/Source/AbsInt/TrivialDomain.cs
index f9298e11..123bcefe 100644
--- a/Source/AbsInt/TrivialDomain.cs
+++ b/Source/AbsInt/TrivialDomain.cs
@@ -1,79 +1,79 @@
-using System;
-using System.Numerics;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-
-namespace Microsoft.Boogie.AbstractInterpretation
-{
- class TrivialDomain : NativeLattice
- {
- class E : NativeLattice.Element
- {
- public readonly bool IsTop;
- public E(bool isTop) {
- IsTop = isTop;
- }
-
- public override Expr ToExpr() {
- return Expr.Literal(IsTop);
- }
- }
-
- private E top = new E(true);
- private E bottom = new E(false);
-
- public override Element Top { get { return top; } }
- public override Element Bottom { get { return bottom; } }
-
- public override bool IsTop(Element element) {
- var e = (E)element;
- return e.IsTop;
- }
- public override bool IsBottom(Element element) {
- var e = (E)element;
- return !e.IsTop;
- }
-
- public override bool Below(Element a, Element b) {
- return IsBottom(a) || IsTop(b);
- }
-
- public override Element Meet(Element a, Element b) {
- if (IsBottom(b)) {
- return b;
- } else {
- return a;
- }
- }
-
- public override Element Join(Element a, Element b) {
- if (IsTop(b)) {
- return b;
- } else {
- return a;
- }
- }
-
- public override Element Widen(Element a, Element b) {
- return Join(a, b); // it's a finite domain, after all
- }
-
- public override Element Constrain(Element element, Expr expr) {
- var e = (E)element;
- var lit = expr as LiteralExpr;
- if (lit != null && lit.isBool && !(bool)lit.Val) {
- return bottom;
- } else {
- return e;
- }
- }
-
- public override Element Update(Element element, AssignCmd cmd) {
- return element;
- }
-
- public override Element Eliminate(Element element, Variable v) {
- return element;
- }
- }
-}
+using System;
+using System.Numerics;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Boogie.AbstractInterpretation
+{
+ class TrivialDomain : NativeLattice
+ {
+ class E : NativeLattice.Element
+ {
+ public readonly bool IsTop;
+ public E(bool isTop) {
+ IsTop = isTop;
+ }
+
+ public override Expr ToExpr() {
+ return Expr.Literal(IsTop);
+ }
+ }
+
+ private E top = new E(true);
+ private E bottom = new E(false);
+
+ public override Element Top { get { return top; } }
+ public override Element Bottom { get { return bottom; } }
+
+ public override bool IsTop(Element element) {
+ var e = (E)element;
+ return e.IsTop;
+ }
+ public override bool IsBottom(Element element) {
+ var e = (E)element;
+ return !e.IsTop;
+ }
+
+ public override bool Below(Element a, Element b) {
+ return IsBottom(a) || IsTop(b);
+ }
+
+ public override Element Meet(Element a, Element b) {
+ if (IsBottom(b)) {
+ return b;
+ } else {
+ return a;
+ }
+ }
+
+ public override Element Join(Element a, Element b) {
+ if (IsTop(b)) {
+ return b;
+ } else {
+ return a;
+ }
+ }
+
+ public override Element Widen(Element a, Element b) {
+ return Join(a, b); // it's a finite domain, after all
+ }
+
+ public override Element Constrain(Element element, Expr expr) {
+ var e = (E)element;
+ var lit = expr as LiteralExpr;
+ if (lit != null && lit.isBool && !(bool)lit.Val) {
+ return bottom;
+ } else {
+ return e;
+ }
+ }
+
+ public override Element Update(Element element, AssignCmd cmd) {
+ return element;
+ }
+
+ public override Element Eliminate(Element element, Variable v) {
+ return element;
+ }
+ }
+}
diff --git a/Source/AbsInt/cce.cs b/Source/AbsInt/cce.cs
index 693d608c..627add75 100644
--- a/Source/AbsInt/cce.cs
+++ b/Source/AbsInt/cce.cs
@@ -1,62 +1,62 @@
-
-using System;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-using System.Text;
-using Microsoft.Boogie;
-
- /// <summary>
- /// A class containing static methods to extend the functionality of Code Contracts
- /// </summary>
-
-public static class cce {
- [Pure]
- public static T NonNull<T>(T t) {
- Contract.Assert(t != null);
- return t;
- }
- [Pure]
- public static bool NonNullElements<T>(IEnumerable<T> collection) {
- return collection != null && Contract.ForAll(collection, c => c != null);
- }
- [Pure]
- public static bool NonNullElements(VariableSeq collection) {
- return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null);
- }
-
- public class UnreachableException : Exception {
- public UnreachableException() {
- }
- }
-
- [Pure]
- public static void BeginExpose(object o) {
- }
- [Pure]
- public static void EndExpose() {
- }
-
- public static bool IsPeerConsistent(this object o) {
- return true;
- }
-
- public static bool IsConsistent(this object o) {
- return true;
- }
-
- public static bool IsExposable(this object o) {
- return true;
- }
- public static class Owner {
- [Pure]
- public static bool Same(object o, object p) {
- return true;
- }
- }
-}
-public class PeerAttribute : System.Attribute {
-}
-public class RepAttribute : System.Attribute {
-}
-public class CapturedAttribute : System.Attribute {
-}
+
+using System;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Text;
+using Microsoft.Boogie;
+
+ /// <summary>
+ /// A class containing static methods to extend the functionality of Code Contracts
+ /// </summary>
+
+public static class cce {
+ [Pure]
+ public static T NonNull<T>(T t) {
+ Contract.Assert(t != null);
+ return t;
+ }
+ [Pure]
+ public static bool NonNullElements<T>(IEnumerable<T> collection) {
+ return collection != null && Contract.ForAll(collection, c => c != null);
+ }
+ [Pure]
+ public static bool NonNullElements(VariableSeq collection) {
+ return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null);
+ }
+
+ public class UnreachableException : Exception {
+ public UnreachableException() {
+ }
+ }
+
+ [Pure]
+ public static void BeginExpose(object o) {
+ }
+ [Pure]
+ public static void EndExpose() {
+ }
+
+ public static bool IsPeerConsistent(this object o) {
+ return true;
+ }
+
+ public static bool IsConsistent(this object o) {
+ return true;
+ }
+
+ public static bool IsExposable(this object o) {
+ return true;
+ }
+ public static class Owner {
+ [Pure]
+ public static bool Same(object o, object p) {
+ return true;
+ }
+ }
+}
+public class PeerAttribute : System.Attribute {
+}
+public class RepAttribute : System.Attribute {
+}
+public class CapturedAttribute : System.Attribute {
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-22 07:26:20 +0000