diff options
| author |  allydonaldson <unknown> | 2013-07-16 10:50:41 +0100 |
|---|---|---|
| committer | allydonaldson <unknown> | 2013-07-16 10:50:41 +0100 |
| commit | 78f354c9dc7e64b915cd51b824fc7481c9f8b973 (patch) | |
| tree | c58cc589b2174729dd2d613f7438a44184820bc6 | |
| parent | ff6e4ffc5dfedf32e742f4a2df3a25d77de28abc (diff) | |
| parent | 1a55e51994e8c147ea27ead66cfc25c8cc8fb512 (diff) | |
Merge
| -rw-r--r-- | Source/BVD/App.config | 6 | ||||
| -rw-r--r-- | Source/BVD/BVD.csproj | 99 | ||||
| -rw-r--r-- | Source/BVD/Program.cs (renamed from Source/ModelViewer/Program.cs) | 0 | ||||
| -rw-r--r-- | Source/BVD/Properties/AssemblyInfo.cs | 36 | ||||
| -rw-r--r-- | Source/Boogie.sln | 26 | ||||
| -rw-r--r-- | Source/Core/Absy.cs | 9 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 3 | ||||
| -rw-r--r-- | Source/Core/LinearSets.cs | 63 | ||||
| -rw-r--r-- | Source/Core/OwickiGries.cs | 12 | ||||
| -rw-r--r-- | Source/Doomed/DoomCheck.cs | 23 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 18 | ||||
| -rw-r--r-- | Source/ModelViewer/Main.cs | 51 | ||||
| -rw-r--r-- | Source/ModelViewer/ModelViewer.csproj | 14 | ||||
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 75 | ||||
| -rw-r--r-- | Source/VCGeneration/Check.cs | 128 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 48 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 270 | ||||
| -rw-r--r-- | Test/linear/typecheck.bpl | 21 | ||||
| -rw-r--r-- | Test/og/Answer | 9 | ||||
| -rw-r--r-- | Test/og/async.bpl | 16 | ||||
| -rw-r--r-- | Test/og/runtest.bat | 2 | ||||
| -rw-r--r-- | Test/test2/Answer | 44 | ||||
| -rw-r--r-- | Test/test2/Timeouts0.bpl | 58 |
23 files changed, 761 insertions, 270 deletions
diff --git a/Source/BVD/App.config b/Source/BVD/App.config new file mode 100644 index 00000000..fad249e4 --- /dev/null +++ b/Source/BVD/App.config @@ -0,0 +1,6 @@ +<?xml version="1.0" encoding="utf-8" ?>
+<configuration>
+ <startup>
+ <supportedRuntime version="v4.0" sku=".NETFramework,Version=v4.5" />
+ </startup>
+</configuration>
\ No newline at end of file diff --git a/Source/BVD/BVD.csproj b/Source/BVD/BVD.csproj new file mode 100644 index 00000000..0b32dd22 --- /dev/null +++ b/Source/BVD/BVD.csproj @@ -0,0 +1,99 @@ +<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+ <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
+ <PropertyGroup>
+ <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+ <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+ <ProjectGuid>{8A05D14E-F2BF-4890-BBE0-D76B18A50797}</ProjectGuid>
+ <OutputType>WinExe</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>Microsoft.Boogie.ModelViewer</RootNamespace>
+ <AssemblyName>BVD</AssemblyName>
+ <TargetFrameworkVersion>v4.5</TargetFrameworkVersion>
+ <FileAlignment>512</FileAlignment>
+ <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>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <DebugSymbols>true</DebugSymbols>
+ <DebugType>full</DebugType>
+ <Optimize>false</Optimize>
+ <OutputPath>..\..\Binaries\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <DebugType>pdbonly</DebugType>
+ <Optimize>true</Optimize>
+ <OutputPath>bin\Release\</OutputPath>
+ <DefineConstants>TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <PropertyGroup>
+ <StartupObject />
+ </PropertyGroup>
+ <ItemGroup>
+ <Reference Include="System" />
+ <Reference Include="System.Core" />
+ <Reference Include="System.Data" />
+ <Reference Include="System.Deployment" />
+ <Reference Include="System.Drawing" />
+ <Reference Include="System.Numerics" />
+ <Reference Include="System.Windows.Forms" />
+ </ItemGroup>
+ <ItemGroup>
+ <Compile Include="Program.cs" />
+ <Compile Include="Properties\AssemblyInfo.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <None Include="App.config" />
+ </ItemGroup>
+ <ItemGroup>
+ <ProjectReference Include="..\ModelViewer\ModelViewer.csproj">
+ <Project>{a678c6eb-b329-46a9-bbfc-7585f01acd7c}</Project>
+ <Name>ModelViewer</Name>
+ </ProjectReference>
+ </ItemGroup>
+ <ItemGroup>
+ <BootstrapperPackage Include=".NETFramework,Version=v4.5">
+ <Visible>False</Visible>
+ <ProductName>Microsoft .NET Framework 4.5 %28x86 and x64%29</ProductName>
+ <Install>true</Install>
+ </BootstrapperPackage>
+ <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>false</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/ModelViewer/Program.cs b/Source/BVD/Program.cs index 669ea995..669ea995 100644 --- a/Source/ModelViewer/Program.cs +++ b/Source/BVD/Program.cs diff --git a/Source/BVD/Properties/AssemblyInfo.cs b/Source/BVD/Properties/AssemblyInfo.cs new file mode 100644 index 00000000..3512374e --- /dev/null +++ b/Source/BVD/Properties/AssemblyInfo.cs @@ -0,0 +1,36 @@ +using System.Reflection;
+using System.Runtime.CompilerServices;
+using System.Runtime.InteropServices;
+
+// General Information about an assembly is controlled through the following
+// set of attributes. Change these attribute values to modify the information
+// associated with an assembly.
+[assembly: AssemblyTitle("BVD")]
+[assembly: AssemblyDescription("")]
+[assembly: AssemblyConfiguration("")]
+[assembly: AssemblyCompany("")]
+[assembly: AssemblyProduct("BVD")]
+[assembly: AssemblyCopyright("Copyright © 2013")]
+[assembly: AssemblyTrademark("")]
+[assembly: AssemblyCulture("")]
+
+// Setting ComVisible to false makes the types in this assembly not visible
+// to COM components. If you need to access a type in this assembly from
+// COM, set the ComVisible attribute to true on that type.
+[assembly: ComVisible(false)]
+
+// The following GUID is for the ID of the typelib if this project is exposed to COM
+[assembly: Guid("00610a12-cf4c-4c29-af30-31a99d22b9d8")]
+
+// Version information for an assembly consists of the following four values:
+//
+// Major Version
+// Minor Version
+// Build Number
+// Revision
+//
+// You can specify all the values or you can default the Build and Revision Numbers
+// by using the '*' as shown below:
+// [assembly: AssemblyVersion("1.0.*")]
+[assembly: AssemblyVersion("1.0.0.0")]
+[assembly: AssemblyFileVersion("1.0.0.0")]
diff --git a/Source/Boogie.sln b/Source/Boogie.sln index b93bc31f..cadcaacb 100644 --- a/Source/Boogie.sln +++ b/Source/Boogie.sln @@ -35,6 +35,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Doomed", "Doomed\Doomed.csp EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ExecutionEngine", "ExecutionEngine\ExecutionEngine.csproj", "{EAA5EB79-D475-4601-A59B-825C191CD25F}"
EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BVD", "BVD\BVD.csproj", "{8A05D14E-F2BF-4890-BBE0-D76B18A50797}"
+EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
Checked|.NET = Checked|.NET
@@ -455,6 +457,30 @@ Global {EAA5EB79-D475-4601-A59B-825C191CD25F}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
{EAA5EB79-D475-4601-A59B-825C191CD25F}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
{EAA5EB79-D475-4601-A59B-825C191CD25F}.z3apidebug|x86.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Checked|.NET.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Checked|Any CPU.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Checked|Any CPU.Build.0 = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Checked|Mixed Platforms.Build.0 = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Checked|x86.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Release|.NET.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Release|Any CPU.Build.0 = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Release|x86.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.z3apidebug|.NET.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.z3apidebug|x86.ActiveCfg = Release|Any CPU
EndGlobalSection
GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 43523b55..5e69b179 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -1186,6 +1186,15 @@ namespace Microsoft.Boogie { }
}
+ public int TimeLimit
+ {
+ get
+ {
+ int tl = CommandLineOptions.Clo.ProverKillTime;
+ CheckIntAttribute("timeLimit", ref tl);
+ return tl;
+ }
+ }
public NamedDeclaration(IToken/*!*/ tok, string/*!*/ name)
: base(tok) {
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index fcb3157b..51034bf3 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -1496,6 +1496,9 @@ namespace Microsoft.Boogie { Assign a unique ID to an implementation to be used for verification
result caching (default: ""<impl. name>:0"").
+ {:timeLimit N}
+ Set the time limit for a given implementation.
+
---- On functions ----------------------------------------------------------
{:builtin ""spec""}
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs index 84ce264d..27312f38 100644 --- a/Source/Core/LinearSets.cs +++ b/Source/Core/LinearSets.cs @@ -156,24 +156,33 @@ namespace Microsoft.Boogie else if (cmd is CallCmd)
{
CallCmd callCmd = (CallCmd)cmd;
- for (int i = 0; i < callCmd.Proc.InParams.Count; i++)
+ while (callCmd != null)
{
- if (FindDomainName(callCmd.Proc.InParams[i]) == null) continue;
- IdentifierExpr ie = callCmd.Ins[i] as IdentifierExpr;
- if (start.Contains(ie.Decl))
- {
- start.Remove(ie.Decl);
- }
- else
+ for (int i = 0; i < callCmd.Proc.InParams.Count; i++)
{
- Error(ie, "unavailable source for a linear read");
+ if (FindDomainName(callCmd.Proc.InParams[i]) == null) continue;
+ IdentifierExpr ie = callCmd.Ins[i] as IdentifierExpr;
+ if (start.Contains(ie.Decl))
+ {
+ start.Remove(ie.Decl);
+ }
+ else
+ {
+ Error(ie, "unavailable source for a linear read");
+ }
}
+ callCmd = callCmd.InParallelWith;
}
+ callCmd = (CallCmd)cmd;
availableLocalLinearVars[callCmd] = new HashSet<Variable>(start);
- foreach (IdentifierExpr ie in callCmd.Outs)
+ while (callCmd != null)
{
- if (FindDomainName(ie.Decl) == null) continue;
- start.Add(ie.Decl);
+ foreach (IdentifierExpr ie in callCmd.Outs)
+ {
+ if (FindDomainName(ie.Decl) == null) continue;
+ start.Add(ie.Decl);
+ }
+ callCmd = callCmd.InParallelWith;
}
}
else if (cmd is HavocCmd)
@@ -356,19 +365,6 @@ namespace Microsoft.Boogie return base.VisitCallCmd(node);
}
- private void TransformCallCmd(CallCmd callCmd, Dictionary<string, Expr> domainNameToExpr)
- {
- foreach (var domainName in linearDomains.Keys)
- {
- callCmd.Ins.Add(domainNameToExpr[domainName]);
- }
- CallCmd parallelCallCmd = callCmd.InParallelWith;
- if (parallelCallCmd != null)
- {
- TransformCallCmd(parallelCallCmd, domainNameToExpr);
- }
- }
-
private void AddDisjointnessExpr(CmdSeq newCmds, Absy absy, Dictionary<string, Variable> domainNameToInputVar)
{
Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
@@ -427,6 +423,18 @@ namespace Microsoft.Boogie callCmd.Ins.Add(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.False)));
}
}
+ else if (callCmd.InParallelWith != null)
+ {
+ while (callCmd != null)
+ {
+ foreach (var domainName in linearDomains.Keys)
+ {
+ var domain = linearDomains[domainName];
+ callCmd.Ins.Add(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.False)));
+ }
+ callCmd = callCmd.InParallelWith;
+ }
+ }
else
{
Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
@@ -441,7 +449,10 @@ namespace Microsoft.Boogie IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), domainNameToExpr[domainName]));
}
- TransformCallCmd(callCmd, domainNameToExpr);
+ foreach (var domainName in linearDomains.Keys)
+ {
+ callCmd.Ins.Add(domainNameToExpr[domainName]);
+ }
}
}
else if (cmd is YieldCmd)
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index 14f5f328..e353700f 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -131,7 +131,7 @@ namespace Microsoft.Boogie public override Cmd VisitCallCmd(CallCmd node)
{
ProcedureInfo info = procNameToInfo[node.callee];
- if (!node.IsAsync && !info.isAtomic)
+ if (node.InParallelWith != null || node.IsAsync || !info.isAtomic)
{
procNameToInfo[currentImpl.Name].isAtomic = false;
moreProcessingRequired = true;
@@ -487,6 +487,10 @@ namespace Microsoft.Boogie CallCmd callCmd = cmd as CallCmd;
if (callCmd != null)
{
+ if (callCmd.InParallelWith != null || callCmd.IsAsync || !procNameToInfo[callCmd.callee].isAtomic)
+ {
+ AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);
+ }
if (callCmd.InParallelWith != null)
{
List<Expr> ins;
@@ -507,14 +511,12 @@ namespace Microsoft.Boogie dummyCallCmd.Proc = dummyAsyncTargetProc;
newCmds.Add(dummyCallCmd);
}
- else if (procNameToInfo[callCmd.callee].isAtomic)
+ else
{
newCmds.Add(callCmd);
}
- else
+ if (callCmd.InParallelWith != null || callCmd.IsAsync || !procNameToInfo[callCmd.callee].isAtomic)
{
- AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);
- newCmds.Add(callCmd);
HashSet<Variable> availableLocalLinearVars = new HashSet<Variable>(linearTypechecker.availableLocalLinearVars[callCmd]);
foreach (IdentifierExpr ie in callCmd.Outs)
{
diff --git a/Source/Doomed/DoomCheck.cs b/Source/Doomed/DoomCheck.cs index 7e2ec984..b317dc71 100644 --- a/Source/Doomed/DoomCheck.cs +++ b/Source/Doomed/DoomCheck.cs @@ -115,21 +115,26 @@ void ObjectInvariant() // Todo: Check if vc is trivial true or false
outcome = ProverInterface.Outcome.Undetermined;
- Contract.Assert( m_ErrorHandler !=null);
- m_Checker.BeginCheck(lv[0].Name, vc, m_ErrorHandler);
- m_Checker.ProverTask.Wait();
-
- try {
+ Contract.Assert(m_ErrorHandler != null);
+ try
+ {
+ m_Checker.BeginCheck(lv[0].Name, vc, m_ErrorHandler);
+ m_Checker.ProverTask.Wait();
outcome = m_Checker.ReadOutcome();
- m_Checker.GoBackToIdle();
- } catch (UnexpectedProverOutputException e)
+ }
+ catch (UnexpectedProverOutputException e)
{
- if (CommandLineOptions.Clo.TraceVerify) {
+ if (CommandLineOptions.Clo.TraceVerify)
+ {
Console.WriteLine("Prover is unable to check {0}! Reason:", lv[0].Name);
Console.WriteLine(e.ToString());
}
return false;
- }
+ }
+ finally
+ {
+ m_Checker.GoBackToIdle();
+ }
return true;
}
}
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 7910f9c9..b83a7d52 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -141,6 +141,7 @@ namespace Microsoft.Boogie }
tw.Write(errorInfo.Out.ToString());
+ tw.Write(errorInfo.Model.ToString());
tw.Flush();
}
@@ -235,6 +236,7 @@ namespace Microsoft.Boogie public ErrorKind Kind { get; set; }
public string ImplementationName { get; set; }
public TextWriter Out = new StringWriter();
+ public TextWriter Model = new StringWriter();
public string FullMsg
{
@@ -1016,7 +1018,7 @@ namespace Microsoft.Boogie #region Process the verification results and statistics
- ProcessOutcome(verificationResult.Outcome, verificationResult.Errors, TimeIndication(verificationResult), stats, output, er, verificationResult.ImplementationName, verificationResult.ImplementationToken, verificationResult.RequestId);
+ ProcessOutcome(verificationResult.Outcome, verificationResult.Errors, TimeIndication(verificationResult), stats, output, impl.TimeLimit, er, verificationResult.ImplementationName, verificationResult.ImplementationToken, verificationResult.RequestId);
ProcessErrors(verificationResult.Errors, verificationResult.Outcome, output, er, impl);
@@ -1139,7 +1141,7 @@ namespace Microsoft.Boogie foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)
{
- ProcessOutcome(x.outcome, x.errors, "", stats, Console.Out, er);
+ ProcessOutcome(x.outcome, x.errors, "", stats, Console.Out, CommandLineOptions.Clo.ProverKillTime, er);
ProcessErrors(x.errors, x.outcome, Console.Out, er);
}
//errorCount = outcome.ErrorCount;
@@ -1166,7 +1168,7 @@ namespace Microsoft.Boogie // Run Abstract Houdini
var abs = new Houdini.AbsHoudini(program, domain);
var absout = abs.ComputeSummaries();
- ProcessOutcome(absout.outcome, absout.errors, "", stats, Console.Out, er);
+ ProcessOutcome(absout.outcome, absout.errors, "", stats, Console.Out, CommandLineOptions.Clo.ProverKillTime, er);
ProcessErrors(absout.errors, absout.outcome, Console.Out, er);
//Houdini.PredicateAbs.Initialize(program);
@@ -1195,7 +1197,7 @@ namespace Microsoft.Boogie private static void ProcessOutcome(VC.VCGen.Outcome outcome, List<Counterexample> errors, string timeIndication,
- PipelineStatistics stats, TextWriter tw, ErrorReporterDelegate er = null, string implName = null, IToken implTok = null, string requestId = null)
+ PipelineStatistics stats, TextWriter tw, int timeLimit, ErrorReporterDelegate er = null, string implName = null, IToken implTok = null, string requestId = null)
{
Contract.Requires(stats != null);
@@ -1203,11 +1205,11 @@ namespace Microsoft.Boogie printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw);
- ReportOutcome(outcome, er, implName, implTok, requestId, tw);
+ ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit);
}
- private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw)
+ private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit)
{
ErrorInformation errorInfo = null;
@@ -1219,7 +1221,7 @@ namespace Microsoft.Boogie case VCGen.Outcome.TimedOut:
if (implName != null && implTok != null)
{
- errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification timed out after {0} seconds ({1})", CommandLineOptions.Clo.ProverKillTime, implName), requestId);
+ errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification timed out after {0} seconds ({1})", timeLimit, implName), requestId);
}
break;
case VCGen.Outcome.OutOfMemory:
@@ -1352,7 +1354,7 @@ namespace Microsoft.Boogie }
if (CommandLineOptions.Clo.ModelViewFile != null)
{
- error.PrintModel(errorInfo.Out);
+ error.PrintModel(errorInfo.Model);
}
printer.WriteErrorInformation(errorInfo, tw);
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs index 2e612aa1..1caed654 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -10,6 +10,7 @@ using System.Windows.Forms; using System.IO;
using Microsoft.Boogie;
+using System.Diagnostics.Contracts;
namespace Microsoft.Boogie.ModelViewer
{
@@ -92,6 +93,18 @@ namespace Microsoft.Boogie.ModelViewer }
}
+ public void ReadModel(string model, int setModelIdTo = 0)
+ {
+ Contract.Requires(model != null);
+
+ using (var rd = new StringReader(model))
+ {
+ allModels = Model.ParseModels(rd).ToArray();
+ }
+
+ AddAndLoadModel(setModelIdTo);
+ }
+
public void ReadModels(string modelFileName, int setModelIdTo)
{
this.lastModelFileName = modelFileName;
@@ -102,28 +115,34 @@ namespace Microsoft.Boogie.ModelViewer allModels = Model.ParseModels(rd).ToArray();
}
- modelId = setModelIdTo;
-
- if (modelId >= allModels.Length)
- modelId = 0;
-
- currentModel = allModels[modelId];
- AddModelMenu();
-
- foreach (var p in Providers()) {
- if (p.IsMyModel(currentModel)) {
- this.langProvider = p;
- break;
- }
- }
-
- LoadModel(modelId);
+ AddAndLoadModel(setModelIdTo);
} else {
currentModel = new Model();
}
this.SetWindowTitle(modelFileName);
+ }
+
+ private void AddAndLoadModel(int setModelIdTo)
+ {
+ modelId = setModelIdTo;
+
+ if (modelId >= allModels.Length)
+ modelId = 0;
+
+ currentModel = allModels[modelId];
+ AddModelMenu();
+
+ foreach (var p in Providers())
+ {
+ if (p.IsMyModel(currentModel))
+ {
+ this.langProvider = p;
+ break;
+ }
+ }
+ LoadModel(modelId);
}
private void LoadModel(int idx)
diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj index ae46767b..f708ddda 100644 --- a/Source/ModelViewer/ModelViewer.csproj +++ b/Source/ModelViewer/ModelViewer.csproj @@ -6,10 +6,10 @@ <ProductVersion>8.0.30703</ProductVersion>
<SchemaVersion>2.0</SchemaVersion>
<ProjectGuid>{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}</ProjectGuid>
- <OutputType>WinExe</OutputType>
+ <OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>Microsoft.Boogie.ModelViewer</RootNamespace>
- <AssemblyName>BVD</AssemblyName>
+ <AssemblyName>ModelViewer</AssemblyName>
<TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
<TargetFrameworkProfile>Client</TargetFrameworkProfile>
<FileAlignment>512</FileAlignment>
@@ -98,18 +98,17 @@ <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
</PropertyGroup>
+ <PropertyGroup>
+ <StartupObject />
+ </PropertyGroup>
<ItemGroup>
<Reference Include="System" />
<Reference Include="System.Core" />
- <Reference Include="System.Numerics" />
- <Reference Include="System.Xml.Linq" />
- <Reference Include="System.Data.DataSetExtensions" />
- <Reference Include="Microsoft.CSharp" />
<Reference Include="System.Data" />
+ <Reference Include="System.Numerics" />
<Reference Include="System.Deployment" />
<Reference Include="System.Drawing" />
<Reference Include="System.Windows.Forms" />
- <Reference Include="System.Xml" />
</ItemGroup>
<ItemGroup>
<Compile Include="BaseProvider.cs" />
@@ -124,7 +123,6 @@ </Compile>
<Compile Include="..\Model\Model.cs" />
<Compile Include="Namer.cs" />
- <Compile Include="Program.cs" />
<Compile Include="Properties\AssemblyInfo.cs" />
<Compile Include="SourceView.cs">
<SubType>Form</SubType>
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 2ff93c54..cac6d95b 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -1125,43 +1125,50 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Requires(cce.NonNullElements(typeArgs));
Contract.Assert(app.Func != null); // resolution must have happened
- if (app.Func.doingExpansion) {
- System.Console.WriteLine("*** detected expansion loop on {0}", app.Func);
- return null;
- }
+ lock (app.Func)
+ {
+ if (app.Func.doingExpansion)
+ {
+ System.Console.WriteLine("*** detected expansion loop on {0}", app.Func);
+ return null;
+ }
- var exp = app.Func.Body;
- if (exp == null)
- return null;
+ var exp = app.Func.Body;
+ if (exp == null)
+ return null;
- VCExpr/*!*/ translatedBody;
- VCExprSubstitution/*!*/ subst = new VCExprSubstitution();
- try {
- BaseTranslator.PushFormalsScope();
- BaseTranslator.PushBoundVariableScope();
- app.Func.doingExpansion = true;
-
- // first bind the formals to VCExpr variables, which are later
- // substituted with the actual parameters
- var inParams = app.Func.InParams;
- for (int i = 0; i < inParams.Length; ++i)
- subst[BaseTranslator.BindVariable(inParams[i])] = args[i];
-
- // recursively translate the body of the expansion
- translatedBody = BaseTranslator.Translate(exp);
- } finally {
- BaseTranslator.PopFormalsScope();
- BaseTranslator.PopBoundVariableScope();
- app.Func.doingExpansion = false;
- }
+ VCExpr/*!*/ translatedBody;
+ VCExprSubstitution/*!*/ subst = new VCExprSubstitution();
+ try
+ {
+ BaseTranslator.PushFormalsScope();
+ BaseTranslator.PushBoundVariableScope();
+ app.Func.doingExpansion = true;
+
+ // first bind the formals to VCExpr variables, which are later
+ // substituted with the actual parameters
+ var inParams = app.Func.InParams;
+ for (int i = 0; i < inParams.Length; ++i)
+ subst[BaseTranslator.BindVariable(inParams[i])] = args[i];
+
+ // recursively translate the body of the expansion
+ translatedBody = BaseTranslator.Translate(exp);
+ }
+ finally
+ {
+ BaseTranslator.PopFormalsScope();
+ BaseTranslator.PopBoundVariableScope();
+ app.Func.doingExpansion = false;
+ }
- // substitute the formals with the actual parameters in the body
- var tparms = app.Func.TypeParameters;
- Contract.Assert(typeArgs.Count == tparms.Length);
- for (int i = 0; i < typeArgs.Count; ++i)
- subst[tparms[i]] = typeArgs[i];
- SubstitutingVCExprVisitor/*!*/ substituter = new SubstitutingVCExprVisitor(Gen);
- return substituter.Mutate(translatedBody, subst);
+ // substitute the formals with the actual parameters in the body
+ var tparms = app.Func.TypeParameters;
+ Contract.Assert(typeArgs.Count == tparms.Length);
+ for (int i = 0; i < typeArgs.Count; ++i)
+ subst[tparms[i]] = typeArgs[i];
+ SubstitutingVCExprVisitor/*!*/ substituter = new SubstitutingVCExprVisitor(Gen);
+ return substituter.Mutate(translatedBody, subst);
+ }
}
}
}
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 88e760c7..3a8a1af9 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -53,7 +53,7 @@ namespace Microsoft.Boogie { private TimeSpan proverRunTime;
private volatile ProverInterface.ErrorHandler handler;
private volatile CheckerStatus status;
- public readonly Program Program;
+ public volatile Program Program;
public void GetReady()
{
@@ -178,11 +178,18 @@ namespace Microsoft.Boogie { public void Retarget(Program prog, ProverContext ctx, int timeout = 0)
{
+ lock (this)
+ {
+ hasOutput = default(bool);
+ outcome = default(ProverInterface.Outcome);
+ outputExn = default(UnexpectedProverOutputException);
+ handler = default(ProverInterface.ErrorHandler);
TheoremProver.FullReset();
ctx.Reset();
Setup(prog, ctx);
this.timeout = timeout;
SetTimeout();
+ }
}
public void SetTimeout()
@@ -197,36 +204,42 @@ namespace Microsoft.Boogie { }
}
- private static void Setup(Program prog, ProverContext ctx)
+ /// <summary>
+ /// Set up the context.
+ /// </summary>
+ private void Setup(Program prog, ProverContext ctx)
{
- // set up the context
- foreach (Declaration decl in prog.TopLevelDeclarations.ToList())
+ Program = prog;
+ lock (Program.TopLevelDeclarations)
{
- Contract.Assert(decl != null);
- var typeDecl = decl as TypeCtorDecl;
- var constDecl = decl as Constant;
- var funDecl = decl as Function;
- var axiomDecl = decl as Axiom;
- var glVarDecl = decl as GlobalVariable;
- if (typeDecl != null)
- {
- ctx.DeclareType(typeDecl, null);
- }
- else if (constDecl != null)
+ foreach (Declaration decl in Program.TopLevelDeclarations)
{
- ctx.DeclareConstant(constDecl, constDecl.Unique, null);
- }
- else if (funDecl != null)
- {
- ctx.DeclareFunction(funDecl, null);
- }
- else if (axiomDecl != null)
- {
- ctx.AddAxiom(axiomDecl, null);
- }
- else if (glVarDecl != null)
- {
- ctx.DeclareGlobalVariable(glVarDecl, null);
+ Contract.Assert(decl != null);
+ var typeDecl = decl as TypeCtorDecl;
+ var constDecl = decl as Constant;
+ var funDecl = decl as Function;
+ var axiomDecl = decl as Axiom;
+ var glVarDecl = decl as GlobalVariable;
+ if (typeDecl != null)
+ {
+ ctx.DeclareType(typeDecl, null);
+ }
+ else if (constDecl != null)
+ {
+ ctx.DeclareConstant(constDecl, constDecl.Unique, null);
+ }
+ else if (funDecl != null)
+ {
+ ctx.DeclareFunction(funDecl, null);
+ }
+ else if (axiomDecl != null)
+ {
+ ctx.AddAxiom(axiomDecl, null);
+ }
+ else if (glVarDecl != null)
+ {
+ ctx.DeclareGlobalVariable(glVarDecl, null);
+ }
}
}
}
@@ -282,32 +295,39 @@ namespace Microsoft.Boogie { }
private void WaitForOutput(object dummy) {
- try {
- outcome = thmProver.CheckOutcome(cce.NonNull(handler));
- } catch (UnexpectedProverOutputException e) {
- outputExn = e;
- }
-
- switch (outcome) {
- case ProverInterface.Outcome.Valid:
- thmProver.LogComment("Valid");
- break;
- case ProverInterface.Outcome.Invalid:
- thmProver.LogComment("Invalid");
- break;
- case ProverInterface.Outcome.TimeOut:
- thmProver.LogComment("Timed out");
- break;
- case ProverInterface.Outcome.OutOfMemory:
- thmProver.LogComment("Out of memory");
- break;
- case ProverInterface.Outcome.Undetermined:
- thmProver.LogComment("Undetermined");
- break;
- }
-
- hasOutput = true;
- proverRunTime = DateTime.UtcNow - proverStart;
+ lock (this)
+ {
+ try
+ {
+ outcome = thmProver.CheckOutcome(cce.NonNull(handler));
+ }
+ catch (UnexpectedProverOutputException e)
+ {
+ outputExn = e;
+ }
+
+ switch (outcome)
+ {
+ case ProverInterface.Outcome.Valid:
+ thmProver.LogComment("Valid");
+ break;
+ case ProverInterface.Outcome.Invalid:
+ thmProver.LogComment("Invalid");
+ break;
+ case ProverInterface.Outcome.TimeOut:
+ thmProver.LogComment("Timed out");
+ break;
+ case ProverInterface.Outcome.OutOfMemory:
+ thmProver.LogComment("Out of memory");
+ break;
+ case ProverInterface.Outcome.Undetermined:
+ thmProver.LogComment("Undetermined");
+ break;
+ }
+
+ hasOutput = true;
+ proverRunTime = DateTime.UtcNow - proverStart;
+ }
}
public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) {
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 5bc5eba3..8afbf027 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -972,44 +972,60 @@ namespace VC { #endregion
- protected Checker FindCheckerFor(int timeout)
+ protected Checker FindCheckerFor(int timeout, bool isBlocking = true)
{
Contract.Ensures(Contract.Result<Checker>() != null);
+ var maxRetries = 3;
lock (checkers)
{
retry:
// Look for existing checker.
for (int i = 0; i < checkers.Count; i++)
{
- var c = checkers.ElementAt(i);
- lock (c)
+ var c = checkers[i];
+ if (Monitor.TryEnter(c))
{
- if (c.WillingToHandle(timeout, program))
+ try
{
- c.GetReady();
- return c;
- }
- else if (c.IsIdle || c.IsClosed)
- {
- if (c.IsIdle)
+ if (c.WillingToHandle(timeout, program))
{
- c.Retarget(program, c.TheoremProver.Context, timeout);
+ c.GetReady();
return c;
}
- else
+ else if (c.IsIdle || c.IsClosed)
{
- checkers.RemoveAt(i);
+ if (c.IsIdle)
+ {
+ c.Retarget(program, c.TheoremProver.Context, timeout);
+ c.GetReady();
+ return c;
+ }
+ else
+ {
+ checkers.RemoveAt(i);
+ }
}
- continue;
+ }
+ finally
+ {
+ Monitor.Exit(c);
}
}
}
if (Cores <= checkers.Count)
{
- Monitor.Wait(checkers, 50);
- goto retry;
+ if (isBlocking || 0 < maxRetries)
+ {
+ Monitor.Wait(checkers, 50);
+ maxRetries--;
+ goto retry;
+ }
+ else
+ {
+ return null;
+ }
}
// Create a new checker.
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 3d64e790..80ffa072 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -252,18 +252,21 @@ namespace VC { return BooleanEval(e, ref val) && !val;
}
- bool CheckUnreachable(Block cur, CmdSeq seq) {
+ bool CheckUnreachable(Block cur, CmdSeq seq)
+ {
Contract.Requires(cur != null);
Contract.Requires(seq != null);
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- foreach (Cmd cmd in seq) {
+ foreach (Cmd cmd in seq)
+ {
AssertCmd assrt = cmd as AssertCmd;
if (assrt != null && QKeyValue.FindBoolAttribute(assrt.Attributes, "PossiblyUnreachable"))
return false;
}
DateTime start = DateTime.UtcNow;
- if (CommandLineOptions.Clo.Trace) {
+ if (CommandLineOptions.Clo.Trace)
+ {
System.Console.Write(" soundness smoke test #{0} ... ", id);
}
callback.OnProgress("smoke", id, id, 0.0);
@@ -278,7 +281,8 @@ namespace VC { Contract.Assert(backup != null);
impl.Blocks = GetCopiedBlocks();
copy.TransferCmd = new ReturnCmd(Token.NoToken);
- if (CommandLineOptions.Clo.TraceVerify) {
+ if (CommandLineOptions.Clo.TraceVerify)
+ {
System.Console.WriteLine();
System.Console.WriteLine(" --- smoke #{0}, before passify", id);
Emit();
@@ -290,39 +294,60 @@ namespace VC { Checker ch = parent.FindCheckerFor(CommandLineOptions.Clo.SmokeTimeout);
Contract.Assert(ch != null);
- var exprGen = ch.TheoremProver.Context.ExprGen;
- VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
+ ProverInterface.Outcome outcome = ProverInterface.Outcome.Undetermined;
+ try
+ {
+ lock (ch)
+ {
+ var exprGen = ch.TheoremProver.Context.ExprGen;
+ VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
- VCExpr vc = parent.GenerateVC(impl, controlFlowVariableExpr, out label2Absy, ch.TheoremProver.Context);
- Contract.Assert(vc != null);
+ VCExpr vc = parent.GenerateVC(impl, controlFlowVariableExpr, out label2Absy, ch.TheoremProver.Context);
+ Contract.Assert(vc != null);
- if (!CommandLineOptions.Clo.UseLabels) {
- VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO));
- VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));
- vc = exprGen.Implies(eqExpr, vc);
- }
+ if (!CommandLineOptions.Clo.UseLabels)
+ {
+ VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO));
+ VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));
+ vc = exprGen.Implies(eqExpr, vc);
+ }
- impl.Blocks = backup;
+ impl.Blocks = backup;
- if (CommandLineOptions.Clo.TraceVerify) {
- System.Console.WriteLine(" --- smoke #{0}, after passify", id);
- Emit();
+ if (CommandLineOptions.Clo.TraceVerify)
+ {
+ System.Console.WriteLine(" --- smoke #{0}, after passify", id);
+ Emit();
+ }
+
+ ch.BeginCheck(cce.NonNull(impl.Name + "_smoke" + id++), vc, new ErrorHandler(label2Absy, this.callback));
+ }
+
+ ch.ProverTask.Wait();
+
+ lock (ch)
+ {
+ outcome = ch.ReadOutcome();
+ }
}
- ch.BeginCheck(cce.NonNull(impl.Name + "_smoke" + id++), vc, new ErrorHandler(label2Absy, this.callback));
- ch.ProverTask.Wait();
- ProverInterface.Outcome outcome = ch.ReadOutcome();
- ch.GoBackToIdle();
+ finally
+ {
+ ch.GoBackToIdle();
+ }
+
parent.CurrentLocalVariables = null;
DateTime end = DateTime.UtcNow;
TimeSpan elapsed = end - start;
- if (CommandLineOptions.Clo.Trace) {
+ if (CommandLineOptions.Clo.Trace)
+ {
System.Console.WriteLine(" [{0} s] {1}", elapsed.TotalSeconds,
outcome == ProverInterface.Outcome.Valid ? "OOPS" :
"OK" + (outcome == ProverInterface.Outcome.Invalid ? "" : " (" + outcome + ")"));
}
- if (outcome == ProverInterface.Outcome.Valid) {
+ if (outcome == ProverInterface.Outcome.Valid)
+ {
// copy it again, so we get the version with calls, assignments and such
copy = CopyBlock(cur);
copy.Cmds = seq;
@@ -1183,20 +1208,25 @@ namespace VC { /// <summary>
/// As a side effect, updates "this.parent.CumulativeAssertionCount".
/// </summary>
- public void BeginCheck(VerifierCallback callback, ModelViewInfo mvInfo, int no, int timeout) {
+ public void BeginCheck(Checker checker, VerifierCallback callback, ModelViewInfo mvInfo, int no, int timeout)
+ {
+ Contract.Requires(checker != null);
Contract.Requires(callback != null);
+
splitNo = no;
impl.Blocks = blocks;
- checker = parent.FindCheckerFor(timeout);
+ this.checker = checker;
+
Hashtable/*<int, Absy!>*/ label2absy = new Hashtable/*<int, Absy!>*/();
ProverContext ctx = checker.TheoremProver.Context;
Boogie2VCExprTranslator bet = ctx.BoogieExprTranslator;
bet.SetCodeExprConverter(
new CodeExprConverter(
- delegate (CodeExpr codeExpr, Hashtable/*<Block, VCExprVar!>*/ blockVariables, List<VCExprLetBinding/*!*/> bindings) {
+ delegate(CodeExpr codeExpr, Hashtable/*<Block, VCExprVar!>*/ blockVariables, List<VCExprLetBinding/*!*/> bindings)
+ {
VCGen vcgen = new VCGen(new Program(), null, false, parent.checkers);
vcgen.variable2SequenceNumber = new Hashtable/*Variable -> int*/();
vcgen.incarnationOriginMap = new Dictionary<Incarnation, Absy>();
@@ -1210,15 +1240,18 @@ namespace VC { VCExpr startCorrect = VCGen.LetVC(codeExpr.Blocks[0], null, label2absy, blockVariables, bindings, ctx, out ac);
VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect);
- if (vcgen.CurrentLocalVariables.Length != 0) {
+ if (vcgen.CurrentLocalVariables.Length != 0)
+ {
Boogie2VCExprTranslator translator = checker.TheoremProver.Context.BoogieExprTranslator;
List<VCExprVar> boundVars = new List<VCExprVar>();
- foreach (Variable v in vcgen.CurrentLocalVariables) {
+ foreach (Variable v in vcgen.CurrentLocalVariables)
+ {
Contract.Assert(v != null);
VCExprVar ev = translator.LookupVariable(v);
Contract.Assert(ev != null);
boundVars.Add(ev);
- if (v.TypedIdent.Type.Equals(Bpl.Type.Bool)) {
+ if (v.TypedIdent.Type.Equals(Bpl.Type.Bool))
+ {
// add an antecedent (tickleBool ev) to help the prover find a possible trigger
vce = checker.VCExprGen.Implies(checker.VCExprGen.Function(VCExpressionGenerator.TickleBoolOp, ev), vce);
}
@@ -1227,7 +1260,7 @@ namespace VC { }
return vce;
}
- ));
+ ));
var exprGen = ctx.ExprGen;
VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
@@ -1235,19 +1268,24 @@ namespace VC { VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context);
Contract.Assert(vc != null);
- if (!CommandLineOptions.Clo.UseLabels) {
+ if (!CommandLineOptions.Clo.UseLabels)
+ {
VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO));
VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));
vc = exprGen.Implies(eqExpr, vc);
}
-
- if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {
+
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local)
+ {
reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, mvInfo, cce.NonNull(this.Checker.TheoremProver.Context), parent.program);
- } else {
+ }
+ else
+ {
reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, mvInfo, this.Checker.TheoremProver.Context, parent.program);
}
- if (CommandLineOptions.Clo.TraceVerify && no >= 0) {
+ if (CommandLineOptions.Clo.TraceVerify && no >= 0)
+ {
Console.WriteLine("-- after split #{0}", no);
Print();
}
@@ -1438,104 +1476,157 @@ namespace VC { remaining_cost = work.Peek().Cost;
}
- while (work.Any() || currently_running.Any()) {
+ while (work.Any() || currently_running.Any())
+ {
bool prover_failed = false;
- Split s;
+ Split s = null;
+ var isWaiting = !work.Any();
- if (work.Any() && currently_running.Count < Cores) {
- s = work.Pop();
+ if (!isWaiting)
+ {
+ s = work.Peek();
- if (first_round && max_splits > 1) {
+ if (first_round && max_splits > 1)
+ {
prover_failed = true;
remaining_cost -= s.Cost;
- } else {
- if (CommandLineOptions.Clo.Trace && no >= 0) {
- System.Console.WriteLine(" checking split {1}/{2}, {3:0.00}%, {0} ...",
+ }
+ else
+ {
+ var timeout = (keep_going && s.LastChance) ? CommandLineOptions.Clo.VcsFinalAssertTimeout :
+ keep_going ? CommandLineOptions.Clo.VcsKeepGoingTimeout :
+ impl.TimeLimit;
+
+ var checker = s.parent.FindCheckerFor(timeout, false);
+ if (checker == null)
+ {
+ isWaiting = true;
+ goto waiting;
+ }
+ else
+ {
+ s = work.Pop();
+ }
+
+ if (CommandLineOptions.Clo.Trace && no >= 0)
+ {
+ System.Console.WriteLine(" checking split {1}/{2}, {3:0.00}%, {0} ...",
s.Stats, no + 1, total, 100 * proven_cost / (proven_cost + remaining_cost));
}
callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));
Contract.Assert(s.parent == this);
- lock (program)
+ lock (checker)
{
- s.BeginCheck(callback, mvInfo, no,
- (keep_going && s.LastChance) ? CommandLineOptions.Clo.VcsFinalAssertTimeout :
- keep_going ? CommandLineOptions.Clo.VcsKeepGoingTimeout :
- CommandLineOptions.Clo.ProverKillTime);
+ s.BeginCheck(checker, callback, mvInfo, no, timeout);
}
no++;
currently_running.Add(s);
}
- } else {
+ }
+
+ waiting:
+ if (isWaiting)
+ {
// Wait for one split to terminate.
var tasks = currently_running.Select(splt => splt.ProverTask).ToArray();
- int index = Task.WaitAny(tasks);
- s = currently_running[index];
- currently_running.RemoveAt(index);
- if (do_splitting) {
- remaining_cost -= s.Cost;
- }
+ if (tasks.Any())
+ {
+ try
+ {
+ int index = Task.WaitAny(tasks);
+ s = currently_running[index];
+ currently_running.RemoveAt(index);
- s.ReadOutcome(ref outcome, out prover_failed);
+ if (do_splitting)
+ {
+ remaining_cost -= s.Cost;
+ }
- if (do_splitting) {
- if (prover_failed) {
- // even if the prover fails, we have learned something, i.e., it is
- // annoying to watch Boogie say Timeout, 0.00% a couple of times
- proven_cost += s.Cost / 100;
- } else {
- proven_cost += s.Cost;
- }
- }
- callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));
+ lock (s.Checker)
+ {
+ s.ReadOutcome(ref outcome, out prover_failed);
+ }
- if (prover_failed && !first_round && s.LastChance) {
- string msg = "some timeout";
- if (s.reporter != null && s.reporter.resourceExceededMessage != null) {
- msg = s.reporter.resourceExceededMessage;
- }
- callback.OnCounterexample(s.ToCounterexample(s.Checker.TheoremProver.Context), msg);
- outcome = Outcome.Errors;
- break;
- }
+ if (do_splitting)
+ {
+ if (prover_failed)
+ {
+ // even if the prover fails, we have learned something, i.e., it is
+ // annoying to watch Boogie say Timeout, 0.00% a couple of times
+ proven_cost += s.Cost / 100;
+ }
+ else
+ {
+ proven_cost += s.Cost;
+ }
+ }
+ callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));
- s.Checker.GoBackToIdle();
+ if (prover_failed && !first_round && s.LastChance)
+ {
+ string msg = "some timeout";
+ if (s.reporter != null && s.reporter.resourceExceededMessage != null)
+ {
+ msg = s.reporter.resourceExceededMessage;
+ }
+ callback.OnCounterexample(s.ToCounterexample(s.Checker.TheoremProver.Context), msg);
+ outcome = Outcome.Errors;
+ break;
+ }
+ }
+ finally
+ {
+ s.Checker.GoBackToIdle();
+ }
- Contract.Assert( prover_failed || outcome == Outcome.Correct || outcome == Outcome.Errors || outcome == Outcome.Inconclusive);
+ Contract.Assert(prover_failed || outcome == Outcome.Correct || outcome == Outcome.Errors || outcome == Outcome.Inconclusive);
+ }
}
- if (prover_failed) {
+ if (prover_failed)
+ {
int splits = first_round && max_splits > 1 ? max_splits : max_kg_splits;
- if (splits > 1) {
+ if (splits > 1)
+ {
List<Split> tmp = Split.DoSplit(s, max_vc_cost, splits);
Contract.Assert(tmp != null);
max_vc_cost = 1.0; // for future
first_round = false;
//tmp.Sort(new Comparison<Split!>(Split.Compare));
- foreach (Split a in tmp) {
+ foreach (Split a in tmp)
+ {
Contract.Assert(a != null);
work.Push(a);
total++;
remaining_cost += a.Cost;
}
- if (outcome != Outcome.Errors) {
+ if (outcome != Outcome.Errors)
+ {
outcome = Outcome.Correct;
}
- } else {
- Contract.Assert( outcome != Outcome.Correct);
- if (outcome == Outcome.TimedOut) {
+ }
+ else
+ {
+ Contract.Assert(outcome != Outcome.Correct);
+ if (outcome == Outcome.TimedOut)
+ {
string msg = "some timeout";
- if (s.reporter != null && s.reporter.resourceExceededMessage != null) {
+ if (s.reporter != null && s.reporter.resourceExceededMessage != null)
+ {
msg = s.reporter.resourceExceededMessage;
}
callback.OnTimeout(msg);
- } else if (outcome == Outcome.OutOfMemory) {
+ }
+ else if (outcome == Outcome.OutOfMemory)
+ {
string msg = "out of memory";
- if (s.reporter != null && s.reporter.resourceExceededMessage != null) {
+ if (s.reporter != null && s.reporter.resourceExceededMessage != null)
+ {
msg = s.reporter.resourceExceededMessage;
}
callback.OnOutOfMemory(msg);
@@ -1547,10 +1638,7 @@ namespace VC { }
if (outcome == Outcome.Correct && smoke_tester != null) {
- lock (program)
- {
- smoke_tester.Test();
- }
+ smoke_tester.Test();
}
callback.OnProgress("done", 0, 0, 1.0);
diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl index 7bdb339e..ebd3d07d 100644 --- a/Test/linear/typecheck.bpl +++ b/Test/linear/typecheck.bpl @@ -80,3 +80,24 @@ modifies g; {
g := r;
}
+
+procedure I({:linear ""} x:int) returns({:linear ""} x':int)
+{
+ x' := x;
+}
+
+procedure J()
+{
+}
+
+procedure P1({:linear ""} x:int) returns({:linear ""} x':int)
+{
+ call x' := I(x) | J();
+ call x' := I(x');
+}
+
+procedure P2({:linear ""} x:int) returns({:linear ""} x':int)
+{
+ call x' := I(x);
+ call x' := I(x') | J();
+}
diff --git a/Test/og/Answer b/Test/og/Answer index c29d38dc..d663de9a 100644 --- a/Test/og/Answer +++ b/Test/og/Answer @@ -98,3 +98,12 @@ Boogie program verifier finished with 2 verified, 0 errors -------------------- perm.bpl --------------------
Boogie program verifier finished with 2 verified, 0 errors
+
+-------------------- async.bpl --------------------
+async.bpl(13,1): Error BP5001: This assertion might not hold.
+Execution trace:
+ async.bpl(6,3): anon0
+ async.bpl(6,3): anon0$1
+ (0,0): inline$Proc_YieldChecker_P$1$L0
+
+Boogie program verifier finished with 1 verified, 1 error
diff --git a/Test/og/async.bpl b/Test/og/async.bpl new file mode 100644 index 00000000..15f89bae --- /dev/null +++ b/Test/og/async.bpl @@ -0,0 +1,16 @@ +var x: int;
+var y: int;
+
+procedure {:entrypoint} foo()
+{
+ assume x == y;
+ x := x + 1;
+ async call P();
+ y := y + 1;
+}
+
+procedure P()
+requires x != y;
+{
+ assert x != y;
+}
\ No newline at end of file diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat index dd07b4a4..5915a206 100644 --- a/Test/og/runtest.bat +++ b/Test/og/runtest.bat @@ -9,7 +9,7 @@ for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl parallel3.bpl) do ( %BGEXE% %* /nologo /noinfer /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f
)
-for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl parallel6.bpl parallel7.bpl akash.bpl t1.bpl new1.bpl perm.bpl) do (
+for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl parallel6.bpl parallel7.bpl akash.bpl t1.bpl new1.bpl perm.bpl async.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f
diff --git a/Test/test2/Answer b/Test/test2/Answer index 5f8642e1..e9390250 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -502,5 +502,45 @@ Execution trace: Timeouts0.bpl(10,5): anon4_LoopDone
Timeouts0.bpl(19,5): anon5_LoopHead
Timeouts0.bpl(23,11): anon5_LoopBody
-
-Boogie program verifier finished with 0 verified, 0 errors, 1 time out
+Timeouts0.bpl(41,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(37,7): anon0
+ Timeouts0.bpl(39,5): anon4_LoopHead
+ Timeouts0.bpl(43,20): anon4_LoopBody
+Timeouts0.bpl(48,5): Timed out on BP5003: A postcondition might not hold on this return path.
+Timeouts0.bpl(31,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Timeouts0.bpl(37,7): anon0
+ Timeouts0.bpl(39,5): anon4_LoopHead
+ Timeouts0.bpl(39,5): anon4_LoopDone
+ Timeouts0.bpl(48,5): anon5_LoopHead
+ Timeouts0.bpl(48,5): anon5_LoopDone
+Timeouts0.bpl(50,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(37,7): anon0
+ Timeouts0.bpl(39,5): anon4_LoopHead
+ Timeouts0.bpl(39,5): anon4_LoopDone
+ Timeouts0.bpl(48,5): anon5_LoopHead
+ Timeouts0.bpl(52,11): anon5_LoopBody
+Timeouts0.bpl(70,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(66,7): anon0
+ Timeouts0.bpl(68,5): anon4_LoopHead
+ Timeouts0.bpl(72,20): anon4_LoopBody
+Timeouts0.bpl(77,5): Timed out on BP5003: A postcondition might not hold on this return path.
+Timeouts0.bpl(60,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Timeouts0.bpl(66,7): anon0
+ Timeouts0.bpl(68,5): anon4_LoopHead
+ Timeouts0.bpl(68,5): anon4_LoopDone
+ Timeouts0.bpl(77,5): anon5_LoopHead
+ Timeouts0.bpl(77,5): anon5_LoopDone
+Timeouts0.bpl(79,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(66,7): anon0
+ Timeouts0.bpl(68,5): anon4_LoopHead
+ Timeouts0.bpl(68,5): anon4_LoopDone
+ Timeouts0.bpl(77,5): anon5_LoopHead
+ Timeouts0.bpl(81,11): anon5_LoopBody
+
+Boogie program verifier finished with 0 verified, 0 errors, 3 time outs
diff --git a/Test/test2/Timeouts0.bpl b/Test/test2/Timeouts0.bpl index c74e9320..c874a1c1 100644 --- a/Test/test2/Timeouts0.bpl +++ b/Test/test2/Timeouts0.bpl @@ -23,3 +23,61 @@ procedure TestTimeouts0(in: [int]int, len: int) returns (out: [int]int) i := i + 1;
}
}
+
+
+procedure TestTimeouts1(in: [int]int, len: int) returns (out: [int]int);
+ requires in[0] == 0 && (forall i: int :: 0 <= i ==> in[i + 1] == in[i] + 1);
+ requires 0 < len;
+ ensures (forall j: int :: 0 <= j && j < len ==> out[j] == j);
+
+implementation {:timeLimit 8} TestTimeouts1(in: [int]int, len: int) returns (out: [int]int)
+{
+ var i : int;
+
+ i := 0;
+ out[i] := 0;
+ while (i < len)
+ invariant 0 <= i && i <= len;
+ invariant out[0] == 0 && (forall j: int :: 0 <= j && j < i ==> out[j + 1] == out[j] + 1);
+ {
+ out[i + 1] := out[i] + 1;
+ i := i + 1;
+ }
+
+ i := 0;
+ while (i < len)
+ invariant 0 <= i && i <= len;
+ invariant (forall j: int :: 0 <= j && j < i ==> out[j] == in[j]);
+ {
+ i := i + 1;
+ }
+}
+
+
+procedure TestTimeouts2(in: [int]int, len: int) returns (out: [int]int);
+ requires in[0] == 0 && (forall i: int :: 0 <= i ==> in[i + 1] == in[i] + 1);
+ requires 0 < len;
+ ensures (forall j: int :: 0 <= j && j < len ==> out[j] == j);
+
+implementation {:timeLimit 2} TestTimeouts2(in: [int]int, len: int) returns (out: [int]int)
+{
+ var i : int;
+
+ i := 0;
+ out[i] := 0;
+ while (i < len)
+ invariant 0 <= i && i <= len;
+ invariant out[0] == 0 && (forall j: int :: 0 <= j && j < i ==> out[j + 1] == out[j] + 1);
+ {
+ out[i + 1] := out[i] + 1;
+ i := i + 1;
+ }
+
+ i := 0;
+ while (i < len)
+ invariant 0 <= i && i <= len;
+ invariant (forall j: int :: 0 <= j && j < i ==> out[j] == in[j]);
+ {
+ i := i + 1;
+ }
+}
|