diff options
| -rw-r--r-- | Source/AbsInt/AbsInt.csproj | 61 | ||||
| -rw-r--r-- | Source/Boogie.sln | 23 | ||||
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.csproj | 68 | ||||
| -rw-r--r-- | Source/Core/Absy.cs | 29 | ||||
| -rw-r--r-- | Source/Provers/Z3api/ContextLayer.cs | 249 | ||||
| -rw-r--r-- | Source/Provers/Z3api/VCExprVisitor.cs | 4 | ||||
| -rw-r--r-- | Source/Provers/Z3api/Z3api.csproj | 5 | ||||
| -rw-r--r-- | Source/VCGeneration/Check.cs | 9 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 2 |
9 files changed, 427 insertions, 23 deletions
diff --git a/Source/AbsInt/AbsInt.csproj b/Source/AbsInt/AbsInt.csproj index 93d304d7..9ccd0ffe 100644 --- a/Source/AbsInt/AbsInt.csproj +++ b/Source/AbsInt/AbsInt.csproj @@ -141,6 +141,67 @@ <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
</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>
+ </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>
+ </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>
+ </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>
+ </PropertyGroup>
<ItemGroup>
<Reference Include="System" />
<Reference Include="System.Core">
diff --git a/Source/Boogie.sln b/Source/Boogie.sln index 53130382..6599ecc2 100644 --- a/Source/Boogie.sln +++ b/Source/Boogie.sln @@ -85,7 +85,8 @@ Global {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|x86.ActiveCfg = z3apidebug|x86
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|x86.Build.0 = z3apidebug|x86
{435D5BD0-6F62-49F8-BB24-33E2257519AD}.Checked|.NET.ActiveCfg = Checked|Any CPU
{435D5BD0-6F62-49F8-BB24-33E2257519AD}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{435D5BD0-6F62-49F8-BB24-33E2257519AD}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -111,6 +112,7 @@ Global {435D5BD0-6F62-49F8-BB24-33E2257519AD}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
{435D5BD0-6F62-49F8-BB24-33E2257519AD}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
{435D5BD0-6F62-49F8-BB24-33E2257519AD}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {435D5BD0-6F62-49F8-BB24-33E2257519AD}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Checked|.NET.ActiveCfg = Checked|Any CPU
{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -135,7 +137,8 @@ Global {0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
- {0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.z3apidebug|x86.ActiveCfg = z3apidebug|x86
+ {0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.z3apidebug|x86.Build.0 = z3apidebug|x86
{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Checked|.NET.ActiveCfg = Checked|Any CPU
{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -161,6 +164,7 @@ Global {BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|.NET.ActiveCfg = Checked|Any CPU
{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -186,6 +190,7 @@ Global {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Checked|.NET.ActiveCfg = Checked|Any CPU
{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -211,6 +216,7 @@ Global {FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|.NET.ActiveCfg = Checked|Any CPU
{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -236,6 +242,7 @@ Global {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
{E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
{E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.Checked|.NET.ActiveCfg = Checked|Any CPU
{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -260,6 +267,7 @@ Global {56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
{B230A69C-C466-4065-B9C1-84D80E76D802}.Checked|.NET.ActiveCfg = Checked|Any CPU
{B230A69C-C466-4065-B9C1-84D80E76D802}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{B230A69C-C466-4065-B9C1-84D80E76D802}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -284,6 +292,7 @@ Global {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
{B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
{B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Checked|.NET.ActiveCfg = Checked|Any CPU
{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -293,6 +302,7 @@ Global {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|Any CPU.Build.0 = Debug|Any CPU
{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|x86.ActiveCfg = Debug|Any CPU
{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Release|.NET.ActiveCfg = Release|Any CPU
{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Release|Any CPU.ActiveCfg = Release|Any CPU
@@ -305,6 +315,7 @@ Global {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.z3apidebug|Mixed Platforms.ActiveCfg = z3apidebug|Any CPU
{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.z3apidebug|Mixed Platforms.Build.0 = z3apidebug|Any CPU
{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|.NET.ActiveCfg = Checked|Any CPU
{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -329,6 +340,7 @@ Global {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Checked|.NET.ActiveCfg = Checked|Any CPU
{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -353,6 +365,7 @@ Global {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Checked|.NET.ActiveCfg = Checked|Any CPU
{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -377,6 +390,7 @@ Global {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Checked|.NET.ActiveCfg = Checked|Any CPU
{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -401,6 +415,7 @@ Global {ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|.NET.ActiveCfg = Checked|x86
{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|Any CPU.ActiveCfg = Checked|x86
{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|Mixed Platforms.ActiveCfg = Checked|x86
@@ -449,6 +464,7 @@ Global {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.z3apidebug|x86.ActiveCfg = Release|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.z3apidebug|x86.Build.0 = Release|Any CPU
{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|.NET.ActiveCfg = Checked|Any CPU
{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -473,6 +489,7 @@ Global {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|x86.ActiveCfg = Release|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|x86.Build.0 = Release|Any CPU
{A598ED5A-93AD-4125-A555-3921A2F936FA}.Checked|.NET.ActiveCfg = Checked|Any CPU
{A598ED5A-93AD-4125-A555-3921A2F936FA}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{A598ED5A-93AD-4125-A555-3921A2F936FA}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -497,6 +514,7 @@ Global {A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
{A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
{A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|x86.ActiveCfg = Release|Any CPU
+ {A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|x86.Build.0 = Release|Any CPU
{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|.NET.ActiveCfg = Release|Any CPU
{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Any CPU.ActiveCfg = Release|Any CPU
{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Any CPU.Build.0 = Release|Any CPU
@@ -521,6 +539,7 @@ Global {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|x86.ActiveCfg = Release|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|x86.Build.0 = Release|Any CPU
EndGlobalSection
GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE
diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj index 52714dc9..de5fecd8 100644 --- a/Source/BoogieDriver/BoogieDriver.csproj +++ b/Source/BoogieDriver/BoogieDriver.csproj @@ -40,7 +40,7 @@ <DebugSymbols>true</DebugSymbols>
<DebugType>full</DebugType>
<Optimize>false</Optimize>
- <OutputPath>..\..\Binaries\</OutputPath>
+ <OutputPath>..\Provers\Z3api\bin\z3apidebug\</OutputPath>
<DefineConstants>TRACE;DEBUG</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
@@ -86,10 +86,10 @@ </PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'z3apidebug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\z3apidebug\</OutputPath>
+ <OutputPath>..\Provers\Z3api\bin\z3apidebug\</OutputPath>
<DefineConstants>DEBUG;TRACE</DefineConstants>
<DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
+ <PlatformTarget>x86</PlatformTarget>
<CodeAnalysisRuleAssemblies>
</CodeAnalysisRuleAssemblies>
<CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
@@ -138,6 +138,68 @@ <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
</PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|x86'">
+ <DebugSymbols>true</DebugSymbols>
+ <OutputPath>bin\x86\Debug\</OutputPath>
+ <DefineConstants>TRACE;DEBUG</DefineConstants>
+ <DebugType>full</DebugType>
+ <PlatformTarget>x86</PlatformTarget>
+ <CodeAnalysisLogFile>..\..\Binaries\Boogie.exe.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>false</CodeAnalysisIgnoreBuiltInRuleSets>
+ <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ </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\Boogie.exe.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>false</CodeAnalysisIgnoreBuiltInRuleSets>
+ <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ <CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules>
+ </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\Boogie.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>Migrated rules for BoogieDriver.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>
+ </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>..\..\Binaries\Boogie.exe.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;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>
+ <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ <CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules>
+ </PropertyGroup>
<ItemGroup>
<Reference Include="System" />
<Reference Include="System.Data" />
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 76eaf661..10077cc4 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -547,6 +547,8 @@ namespace Microsoft.Boogie { // header_last block that was created because of splitting header.
Dictionary<Block, Block> newBlocksCreated = new Dictionary<Block, Block>();
+ bool headRecursion = false; // testing an option to put recursive call before loop body
+
IEnumerable<Block> sortedHeaders = g.SortHeadersByDominance();
foreach (Block/*!*/ header in sortedHeaders)
{
@@ -567,7 +569,17 @@ namespace Microsoft.Boogie { continue;
Block newBlock = new Block();
newBlock.Label = block.Label;
- newBlock.Cmds = codeCopier.CopyCmdSeq(block.Cmds);
+ if (headRecursion && block == header)
+ {
+ CallCmd callCmd = (CallCmd)(loopHeaderToCallCmd2[header]).Clone();
+ addUniqueCallAttr(si_unique_loc, callCmd);
+ si_unique_loc++;
+ newBlock.Cmds.Add(callCmd); // add the recursive call at head of loop
+ var rest = codeCopier.CopyCmdSeq(block.Cmds);
+ newBlock.Cmds.AddRange(rest);
+ }
+ else
+ newBlock.Cmds = codeCopier.CopyCmdSeq(block.Cmds);
blockMap[block] = newBlock;
if (newBlocksCreated.ContainsKey(block))
{
@@ -578,14 +590,21 @@ namespace Microsoft.Boogie { }
}
- CallCmd callCmd = (CallCmd) (loopHeaderToCallCmd2[header]).Clone();
- addUniqueCallAttr(si_unique_loc, callCmd);
- si_unique_loc++;
+ CmdSeq cmdSeq;
+ if (headRecursion)
+ cmdSeq = new CmdSeq();
+ else
+ {
+ CallCmd callCmd = (CallCmd)(loopHeaderToCallCmd2[header]).Clone();
+ addUniqueCallAttr(si_unique_loc, callCmd);
+ si_unique_loc++;
+ cmdSeq = new CmdSeq(callCmd);
+ }
Block/*!*/ block1 = new Block(Token.NoToken, source.Label + "_dummy",
new CmdSeq(new AssumeCmd(Token.NoToken, Expr.False)), new ReturnCmd(Token.NoToken));
Block/*!*/ block2 = new Block(Token.NoToken, block1.Label,
- new CmdSeq(callCmd), new ReturnCmd(Token.NoToken));
+ cmdSeq, new ReturnCmd(Token.NoToken));
impl.Blocks.Add(block1);
dummyBlocks.Add(block1.Label);
diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs index f0aa3906..2eb01e24 100644 --- a/Source/Provers/Z3api/ContextLayer.cs +++ b/Source/Provers/Z3api/ContextLayer.cs @@ -20,6 +20,8 @@ namespace Microsoft.Boogie.Z3 { internal BacktrackDictionary<string, Term> constants = new BacktrackDictionary<string, Term>();
internal BacktrackDictionary<string, FuncDecl> functions = new BacktrackDictionary<string, FuncDecl>();
internal BacktrackDictionary<string, Term> labels = new BacktrackDictionary<string, Term>();
+ internal BacktrackDictionary<Term, VCExpr> constants_inv = null;
+ internal BacktrackDictionary<FuncDecl, Function> functions_inv = null;
public Config config;
public Context z3;
@@ -56,7 +58,13 @@ namespace Microsoft.Boogie.Z3 { z3 = new Context(config);
z3.SetPrintMode(PrintMode.Smtlib2Compliant);
if (logFilename != null)
- z3.OpenLog(logFilename);
+ {
+#if true
+ Z3Log.Open(logFilename);
+#else
+ z3.OpenLog(logFilename);
+#endif
+ }
foreach (string tag in debugTraces)
z3.EnableDebugTrace(tag);
@@ -65,6 +73,227 @@ namespace Microsoft.Boogie.Z3 { this.namer = new UniqueNamer();
}
+ public Z3apiProverContext(Context ctx, VCExpressionGenerator gen)
+ : base(gen, new VCGenerationOptions(new List<string>()))
+ {
+ z3 = ctx;
+
+ this.z3log = null;
+ this.tm = new Z3TypeCachedBuilder(this);
+ this.namer = new UniqueNamer();
+
+ // For external
+
+ constants_inv = new BacktrackDictionary<Term, VCExpr>();
+ functions_inv = new BacktrackDictionary<FuncDecl, Function>();
+ }
+
+ public Term VCExprToTerm(VCExpr expr, LineariserOptions linOptions) {
+ Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);
+ return (Term)expr.Accept(visitor, linOptions);
+ }
+
+
+ private class fromZ3
+ {
+ private VCExpressionGenerator gen;
+ private Dictionary<Term, VCExpr> memo;
+ private BacktrackDictionary<Term, VCExpr> constants_inv;
+ private BacktrackDictionary<FuncDecl, Function> functions_inv;
+ private List<VCExprLetBinding> lets;
+ private int let_ctr = 0;
+
+ private VCExpr create_let(Term t, VCExpr u)
+ {
+ var name = "$x" + let_ctr.ToString();
+ let_ctr++;
+ var sym = gen.Variable(name, u.Type);
+ memo.Remove(t);
+ memo.Add(t, sym);
+ lets.Add(gen.LetBinding(sym, u));
+ return sym;
+ }
+
+ public fromZ3(VCExpressionGenerator _gen,
+ BacktrackDictionary<Term, VCExpr> _constants_inv,
+ BacktrackDictionary<FuncDecl, Function> _functions_inv)
+ {
+ gen = _gen;
+ constants_inv = _constants_inv;
+ functions_inv = _functions_inv;
+ memo = new Dictionary<Term, VCExpr>();
+ lets = new List<VCExprLetBinding>();
+ }
+
+ public void clear()
+ {
+ memo.Clear();
+ lets.Clear();
+ }
+ public VCExpr get(Term arg)
+ {
+ if (memo.ContainsKey(arg))
+ return memo[arg];
+ VCExpr res = null;
+ switch (arg.GetKind())
+ {
+ case TermKind.Numeral:
+ var numstr = arg.GetNumeralString();
+ var bignum = Basetypes.BigNum.FromString(numstr);
+ res = gen.Integer(bignum);
+ break;
+ case TermKind.App:
+ var args = arg.GetAppArgs();
+ var vcargs = new VCExpr[args.Length];
+ for (int i = 0; i < args.Length; i++)
+ vcargs[i] = get(args[i]);
+
+ switch (arg.GetAppDecl().GetKind())
+ {
+ case DeclKind.Add:
+ if (vcargs.Length == 0)
+ res = gen.Integer(Basetypes.BigNum.FromInt(0));
+ else
+ {
+ res = vcargs[0];
+ for (int k = 1; k < vcargs.Length; k++)
+ res = gen.Add(res, vcargs[k]);
+ }
+ break;
+ case DeclKind.And:
+ res = VCExpressionGenerator.True;
+ for (int i = 0; i < vcargs.Length; i++)
+ res = gen.AndSimp(res, vcargs[i]);
+ break;
+ case DeclKind.Div:
+ Debug.Assert(vcargs.Length == 2);
+ res = gen.Function(VCExpressionGenerator.DivOp, vcargs[0], vcargs[1]);
+ break;
+ case DeclKind.Eq:
+ Debug.Assert(vcargs.Length == 2);
+ res = gen.Eq(vcargs[0], vcargs[1]);
+ break;
+ case DeclKind.False:
+ res = VCExpressionGenerator.False;
+ break;
+ case DeclKind.Ge:
+ Debug.Assert(vcargs.Length == 2);
+ res = gen.Function(VCExpressionGenerator.GeOp, vcargs[0], vcargs[1]);
+ break;
+ case DeclKind.Gt:
+ Debug.Assert(vcargs.Length == 2);
+ res = gen.Gt(vcargs[0], vcargs[1]);
+ break;
+ case DeclKind.IDiv:
+ Debug.Assert(vcargs.Length == 2);
+ res = gen.Function(VCExpressionGenerator.DivOp, vcargs[0], vcargs[1]);
+ break;
+ case DeclKind.Iff:
+ Debug.Assert(vcargs.Length == 2);
+ var l = create_let(args[0], vcargs[0]);
+ var r = create_let(args[1], vcargs[1]);
+ return gen.And(gen.Implies(l, r), gen.Implies(r, l));
+ case DeclKind.Implies:
+ Debug.Assert(vcargs.Length == 2);
+ res = gen.Implies(vcargs[0], vcargs[1]);
+ break;
+ case DeclKind.Ite:
+ Debug.Assert(vcargs.Length == 3);
+ res = gen.Function(VCExpressionGenerator.IfThenElseOp, vcargs[0], vcargs[1], vcargs[2]);
+ break;
+ case DeclKind.Le:
+ Debug.Assert(vcargs.Length == 2);
+ res = gen.Function(VCExpressionGenerator.LeOp, vcargs[0], vcargs[1]);
+ break;
+ case DeclKind.Lt:
+ Debug.Assert(vcargs.Length == 2);
+ res = gen.Function(VCExpressionGenerator.LtOp, vcargs[0], vcargs[1]);
+ break;
+ case DeclKind.Mod:
+ Debug.Assert(vcargs.Length == 2);
+ res = gen.Function(VCExpressionGenerator.ModOp, vcargs[0], vcargs[1]);
+ break;
+ case DeclKind.Mul:
+ Debug.Assert(vcargs.Length == 2);
+ res = gen.Function(VCExpressionGenerator.MulOp, vcargs[0], vcargs[1]);
+ break;
+ case DeclKind.Not:
+ Debug.Assert(vcargs.Length == 1);
+ res = gen.Not(vcargs[0]);
+ break;
+ case DeclKind.Or:
+ res = VCExpressionGenerator.False;
+ for (int i = 0; i < vcargs.Length; i++)
+ res = gen.OrSimp(res, vcargs[i]);
+ break;
+ case DeclKind.Select:
+ Debug.Assert(vcargs.Length == 2);
+ res = gen.Select(vcargs[0], vcargs[1]);
+ break;
+ case DeclKind.Store:
+ Debug.Assert(vcargs.Length == 3);
+ res = gen.Store(vcargs[0], vcargs[1], vcargs[2]);
+ break;
+ case DeclKind.Sub:
+ Debug.Assert(vcargs.Length == 2);
+ res = gen.Function(VCExpressionGenerator.SubOp, vcargs[0], vcargs[1]);
+ break;
+ case DeclKind.True:
+ res = VCExpressionGenerator.True;
+ break;
+ case DeclKind.Uminus:
+ Debug.Assert(vcargs.Length == 1);
+ var bigzero = Basetypes.BigNum.FromInt(0);
+ res = gen.Function(VCExpressionGenerator.SubOp, gen.Integer(bigzero), vcargs[0]);
+ break;
+ case DeclKind.Uninterpreted:
+ var name = arg.GetAppDecl().GetDeclName();
+ if (args.Length == 0)
+ { // a 0-ary constant is a VCExprVar
+ if (!constants_inv.TryGetValue(arg, out res))
+ throw new Exception("Z3 returned unknown constant: " + name);
+ }
+ else
+ {
+ Function f;
+ if (!functions_inv.TryGetValue(arg.GetAppDecl(), out f))
+ throw new Exception("Z3 returned unknown function: " + name);
+ List<VCExpr> vcargsList = new List<VCExpr>(vcargs);
+ res = gen.Function(f, vcargsList);
+ }
+ break;
+ default:
+ throw new Exception("Unknown Z3 operator");
+ }
+ break;
+ default:
+ Debug.Assert(false);
+ throw new Exception("Unknown Z3 AST kind");
+ }
+
+ memo.Add(arg, res);
+ return res;
+ }
+ public VCExpr add_lets(VCExpr e)
+ {
+ foreach (var let in lets)
+ {
+ e = gen.Let(e, let);
+ }
+ return e;
+ }
+ }
+
+ public VCExpr TermToVCExpr(Term t)
+ {
+ var fZ = new fromZ3(gen, constants_inv, functions_inv);
+ return fZ.add_lets(fZ.get(t));
+ }
+
+
+
+
+
public override void DeclareType(TypeCtorDecl t, string attributes) {
base.DeclareType(t, attributes);
log("(declare-sort {0})", t.Name);
@@ -97,6 +326,7 @@ namespace Microsoft.Boogie.Z3 { Sort rangeAst = tm.GetType(range);
FuncDecl constDeclAst = z3.MkFuncDecl(symbolAst, domainAst.ToArray(), rangeAst);
functions.Add(functionName, constDeclAst);
+ if(functions_inv != null)functions_inv.Add(constDeclAst, f);
log("(declare-funs (({0} {1} {2})))", functionName, domainStr, rangeAst);
}
@@ -122,7 +352,11 @@ namespace Microsoft.Boogie.Z3 { }
public void CloseLog() {
- z3.CloseLog();
+#if true
+ Z3Log.Close();
+#else
+ z3.CloseLog();
+#endif
if (z3log != null) {
z3log.Close();
}
@@ -134,6 +368,8 @@ namespace Microsoft.Boogie.Z3 { constants.CreateBacktrackPoint();
functions.CreateBacktrackPoint();
labels.CreateBacktrackPoint();
+ if(constants_inv != null)constants_inv.CreateBacktrackPoint();
+ if(functions_inv != null)functions_inv.CreateBacktrackPoint();
z3.Push();
log("(push)");
}
@@ -144,6 +380,8 @@ namespace Microsoft.Boogie.Z3 { functions.Backtrack();
constants.Backtrack();
symbols.Backtrack();
+ if (constants_inv != null) constants_inv.Backtrack();
+ if (functions_inv != null) functions_inv.Backtrack();
log("(pop)");
}
@@ -368,13 +606,18 @@ namespace Microsoft.Boogie.Z3 { return result;
}
- public Term GetConstant(string constantName, Type constantType) {
+ public Term GetConstant(string constantName, Type constantType, VCExpr node)
+ {
Term typeSafeTerm;
if (!constants.ContainsKey(constantName))
this.DeclareConstant(constantName, constantType);
if (!constants.TryGetValue(constantName, out typeSafeTerm))
throw new Exception("constant " + constantName + " is not defined");
+
+ if (constants_inv != null && !constants_inv.ContainsKey(typeSafeTerm))
+ constants_inv.Add(typeSafeTerm, node);
+
return typeSafeTerm;
}
diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs index 149a23f1..0605a854 100644 --- a/Source/Provers/Z3api/VCExprVisitor.cs +++ b/Source/Provers/Z3api/VCExprVisitor.cs @@ -188,7 +188,7 @@ namespace Microsoft.Boogie.Z3 else
{
string varName = namer.GetName(node, node.Name);
- return cm.GetConstant(varName, node.Type);
+ return cm.GetConstant(varName, node.Type,node);
}
}
@@ -252,7 +252,7 @@ namespace Microsoft.Boogie.Z3 private Term MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List<string> varNames, List<Type> boogieTypes, List<Pattern> patterns, List<Term> no_patterns, Term body) {
List<Term> bound = new List<Term>();
for (int i = 0; i < varNames.Count; i++) {
- Term t = cm.GetConstant(varNames[i], boogieTypes[i]);
+ Term t = cm.GetConstant(varNames[i], boogieTypes[i], null);
bound.Add(t);
}
diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj index 94184957..0923cb36 100644 --- a/Source/Provers/Z3api/Z3api.csproj +++ b/Source/Provers/Z3api/Z3api.csproj @@ -118,9 +118,8 @@ </Target>
-->
<ItemGroup>
- <Reference Include="Microsoft.Z3, Version=2.0.40827.2, Culture=neutral, PublicKeyToken=9c8d792caae602a2, processorArchitecture=x86">
- <SpecificVersion>False</SpecificVersion>
- <HintPath>..\..\..\Binaries\Microsoft.Z3.dll</HintPath>
+ <Reference Include="ManagedAPI">
+ <HintPath>..\..\..\..\..\iZ3\win\iZ3\Debug\ManagedAPI.dll</HintPath>
</Reference>
<Reference Include="System" />
<Reference Include="System.Core">
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 9b7b6e36..bb225071 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -100,8 +100,9 @@ namespace Microsoft.Boogie { /// <summary>
/// Constructor. Initialize a checker with the program and log file.
+ /// Optionally, use prover context provided by parameter "ctx".
/// </summary>
- public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout) {
+ public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, ProverContext ctx = null) {
Contract.Requires(vcgen != null);
Contract.Requires(prog != null);
this.timeout = timeout;
@@ -121,7 +122,6 @@ namespace Microsoft.Boogie { options.Parse(CommandLineOptions.Clo.ProverOptions);
ContextCacheKey key = new ContextCacheKey(prog);
- ProverContext ctx;
ProverInterface prover;
if (vcgen.CheckerCommonState == null) {
@@ -129,12 +129,13 @@ namespace Microsoft.Boogie { }
IDictionary<ContextCacheKey, ProverContext>/*!>!*/ cachedContexts = (IDictionary<ContextCacheKey, ProverContext/*!*/>)vcgen.CheckerCommonState;
- if (cachedContexts.TryGetValue(key, out ctx)) {
+ if (ctx == null && cachedContexts.TryGetValue(key, out ctx))
+ {
ctx = (ProverContext)cce.NonNull(ctx).Clone();
prover = (ProverInterface)
CommandLineOptions.Clo.TheProverFactory.SpawnProver(options, ctx);
} else {
- ctx = (ProverContext)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);
+ if (ctx == null) ctx = (ProverContext)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);
// set up the context
foreach (Declaration decl in prog.TopLevelDeclarations) {
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index d13811e0..db7f2dca 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -2454,7 +2454,7 @@ namespace VC {
GenerateVCForStratifiedInlining(program, info, checker);
}
- //Console.WriteLine("Inlining {0}", procName);
+ Console.WriteLine("Inlining {0}", procName);
VCExpr expansion = cce.NonNull(info.vcexpr);
// Instantiate the "forall" variables
|