diff options
Diffstat (limited to 'Source/DafnyServer')
| -rw-r--r-- | Source/DafnyServer/App.config | 6 | ||||
| -rw-r--r-- | Source/DafnyServer/DafnyHelper.cs | 91 | ||||
| -rw-r--r-- | Source/DafnyServer/DafnyServer.csproj | 113 | ||||
| -rw-r--r-- | Source/DafnyServer/Properties/AssemblyInfo.cs | 36 | ||||
| -rw-r--r-- | Source/DafnyServer/Server.cs | 100 | ||||
| -rw-r--r-- | Source/DafnyServer/Utilities.cs | 61 | ||||
| -rw-r--r-- | Source/DafnyServer/VerificationTask.cs | 58 |
7 files changed, 465 insertions, 0 deletions
diff --git a/Source/DafnyServer/App.config b/Source/DafnyServer/App.config new file mode 100644 index 00000000..fad249e4 --- /dev/null +++ b/Source/DafnyServer/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/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs new file mode 100644 index 00000000..e54e2b48 --- /dev/null +++ b/Source/DafnyServer/DafnyHelper.cs @@ -0,0 +1,91 @@ +using System;
+using System.Collections.Generic;
+using System.IO;
+using System.Linq;
+using System.Text;
+using System.Threading.Tasks;
+using Microsoft.Boogie;
+using Bpl = Microsoft.Boogie;
+
+namespace Microsoft.Dafny {
+ // FIXME: This should not be duplicated here
+ class DafnyConsolePrinter : ConsolePrinter {
+ public override void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null) {
+ // Dafny has 0-indexed columns, but Boogie counts from 1
+ var realigned_tok = new Token(tok.line, tok.col - 1);
+ realigned_tok.kind = tok.kind;
+ realigned_tok.pos = tok.pos;
+ realigned_tok.val = tok.val;
+ realigned_tok.filename = tok.filename;
+ base.ReportBplError(realigned_tok, message, error, tw, category);
+
+ if (tok is Dafny.NestedToken) {
+ var nt = (Dafny.NestedToken)tok;
+ ReportBplError(nt.Inner, "Related location", false, tw);
+ }
+ }
+ }
+
+ class DafnyHelper {
+ private string fname;
+ private string source;
+ private string[] args;
+
+ private readonly Dafny.ErrorReporter reporter;
+ private Dafny.Program dafnyProgram;
+ private Bpl.Program boogieProgram;
+
+ public DafnyHelper(string[] args, string fname, string source) {
+ this.args = args;
+ this.fname = fname;
+ this.source = source;
+ this.reporter = new Dafny.ConsoleErrorReporter();
+ }
+
+ public bool Verify() {
+ ServerUtils.ApplyArgs(args, reporter);
+ return Parse() && Resolve() && Translate() && Boogie();
+ }
+
+ private bool Parse() {
+ Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null);
+ Dafny.BuiltIns builtIns = new Dafny.BuiltIns();
+ var success = (Dafny.Parser.Parse(source, fname, fname, module, builtIns, new Dafny.Errors(reporter)) == 0 &&
+ Dafny.Main.ParseIncludes(module, builtIns, new List<string>(), new Dafny.Errors(reporter)) == null);
+ if (success) {
+ dafnyProgram = new Dafny.Program(fname, module, builtIns, reporter);
+ }
+ return success;
+ }
+
+ private bool Resolve() {
+ var resolver = new Dafny.Resolver(dafnyProgram);
+ resolver.ResolveProgram(dafnyProgram);
+ return reporter.Count(ErrorLevel.Error) == 0;
+ }
+
+ private bool Translate() {
+ var translator = new Dafny.Translator(reporter) { InsertChecksums = true, UniqueIdPrefix = fname };
+ boogieProgram = translator.Translate(dafnyProgram); // FIXME how are translation errors reported?
+ return true;
+ }
+
+ private bool Boogie() {
+ if (boogieProgram.Resolve() == 0 && boogieProgram.Typecheck() == 0) { //FIXME ResolveAndTypecheck?
+ ExecutionEngine.EliminateDeadVariables(boogieProgram);
+ ExecutionEngine.CollectModSets(boogieProgram);
+ ExecutionEngine.CoalesceBlocks(boogieProgram);
+ ExecutionEngine.Inline(boogieProgram);
+
+ //NOTE: We could capture errors instead of printing them (pass a delegate instead of null)
+ switch (ExecutionEngine.InferAndVerify(boogieProgram, new PipelineStatistics(), "ServerProgram", null, DateTime.UtcNow.Ticks.ToString())) {
+ case PipelineOutcome.Done:
+ case PipelineOutcome.VerificationCompleted:
+ return true;
+ }
+ }
+
+ return false;
+ }
+ }
+}
diff --git a/Source/DafnyServer/DafnyServer.csproj b/Source/DafnyServer/DafnyServer.csproj new file mode 100644 index 00000000..af262fc3 --- /dev/null +++ b/Source/DafnyServer/DafnyServer.csproj @@ -0,0 +1,113 @@ +<?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>{AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}</ProjectGuid>
+ <OutputType>Exe</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>DafnyServer</RootNamespace>
+ <AssemblyName>DafnyServer</AssemblyName>
+ <TargetFrameworkVersion>v4.5</TargetFrameworkVersion>
+ <FileAlignment>512</FileAlignment>
+ <StartupObject>Microsoft.Dafny.Server</StartupObject>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+ <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>..\..\Binaries\</OutputPath>
+ <DefineConstants>TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
+ <DebugSymbols>true</DebugSymbols>
+ <OutputPath>..\..\Binaries\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <DebugType>full</DebugType>
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>
+ <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>
+ <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>
+ </PropertyGroup>
+ <ItemGroup>
+ <Reference Include="Core">
+ <HintPath>..\..\..\boogie\Binaries\Core.dll</HintPath>
+ </Reference>
+ <Reference Include="ExecutionEngine">
+ <HintPath>..\..\..\boogie\Binaries\ExecutionEngine.dll</HintPath>
+ </Reference>
+ <Reference Include="ParserHelper">
+ <HintPath>..\..\..\boogie\Binaries\ParserHelper.dll</HintPath>
+ </Reference>
+ <Reference Include="Provers.SMTLib">
+ <HintPath>..\..\..\boogie\Binaries\Provers.SMTLib.dll</HintPath>
+ </Reference>
+ <Reference Include="System" />
+ <Reference Include="System.Core" />
+ <Reference Include="System.Runtime.Serialization" />
+ <Reference Include="System.Xml.Linq" />
+ <Reference Include="Microsoft.CSharp" />
+ <Reference Include="System.Xml" />
+ </ItemGroup>
+ <ItemGroup>
+ <Compile Include="DafnyHelper.cs" />
+ <Compile Include="Utilities.cs" />
+ <Compile Include="VerificationTask.cs" />
+ <Compile Include="Properties\AssemblyInfo.cs" />
+ <Compile Include="Server.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <None Include="App.config" />
+ </ItemGroup>
+ <ItemGroup>
+ <ProjectReference Include="..\Dafny\DafnyPipeline.csproj">
+ <Project>{fe44674a-1633-4917-99f4-57635e6fa740}</Project>
+ <Name>DafnyPipeline</Name>
+ </ProjectReference>
+ </ItemGroup>
+ <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
+ <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
+ Other similar extension points exist, see Microsoft.Common.targets.
+ <Target Name="BeforeBuild">
+ </Target>
+ <Target Name="AfterBuild">
+ </Target>
+ -->
+</Project>
\ No newline at end of file diff --git a/Source/DafnyServer/Properties/AssemblyInfo.cs b/Source/DafnyServer/Properties/AssemblyInfo.cs new file mode 100644 index 00000000..5b996543 --- /dev/null +++ b/Source/DafnyServer/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("Dafny Server")]
+[assembly: AssemblyDescription("")]
+[assembly: AssemblyConfiguration("")]
+[assembly: AssemblyCompany("Microsoft Research")]
+[assembly: AssemblyProduct("Dafny Server")]
+[assembly: AssemblyCopyright("Copyright © 2015")]
+[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("44d9c1c1-773b-47c1-b876-2de17e70152e")]
+
+// 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/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs new file mode 100644 index 00000000..8c94ad5b --- /dev/null +++ b/Source/DafnyServer/Server.cs @@ -0,0 +1,100 @@ +using System;
+using System.IO;
+using System.Text;
+using System.Collections.Generic;
+using System.Runtime.Serialization;
+using System.Runtime.Serialization.Json;
+
+using Dafny = Microsoft.Dafny;
+using Bpl = Microsoft.Boogie;
+using Microsoft.Boogie;
+
+namespace Microsoft.Dafny {
+ class Server {
+ private bool running;
+
+ static void Main(string[] args) {
+ Server server = new Server();
+
+ var hasArg = args.Length > 0;
+ var arg = hasArg ? args[0] : null;
+
+ if (hasArg && args[0] == "selftest") {
+ VerificationTask.SelfTest();
+ } else if (hasArg && File.Exists(arg)) {
+ Console.WriteLine("# Reading from {0}", Path.GetFileName(arg));
+ Console.SetIn(new StreamReader(arg, Encoding.UTF8));
+ server.Loop();
+ } else {
+ server.Loop();
+ }
+ }
+
+ private void SetupConsole() {
+ // Setting InputEncoding to UTF8 causes z3 to choke.
+ Console.OutputEncoding = new UTF8Encoding(false, true);
+ }
+
+ public Server() {
+ this.running = true;
+ ExecutionEngine.printer = new DafnyConsolePrinter();
+ SetupConsole();
+ }
+
+ bool EndOfPayload(out string line) {
+ line = Console.ReadLine();
+ return line == null || line == Interaction.CLIENT_EOM_TAG;
+ }
+
+ string ReadPayload() {
+ StringBuilder buffer = new StringBuilder();
+ string line = null;
+ while (!EndOfPayload(out line)) {
+ buffer.Append(line);
+ }
+ return buffer.ToString();
+ }
+
+ void Loop() {
+ for (int cycle = 0; running; cycle++) {
+ var line = Console.ReadLine() ?? "quit";
+ if (line != String.Empty && !line.StartsWith("#")) {
+ var command = line.Split();
+ Respond(command);
+ }
+ }
+ }
+
+ void Respond(string[] command) {
+ try {
+ if (command.Length == 0) {
+ throw new ServerException("Empty command");
+ }
+
+ var verb = command[0];
+ if (verb == "verify") {
+ ServerUtils.checkArgs(command, 0);
+ var payload = ReadPayload();
+ VerificationTask.ReadTask(payload).Run();
+ } else if (verb == "quit") {
+ ServerUtils.checkArgs(command, 0);
+ Exit();
+ } else {
+ throw new ServerException("Unknown verb '{0}'", verb);
+ }
+
+ Interaction.EOM(Interaction.SUCCESS, "Verification completed successfully!");
+ } catch (ServerException ex) {
+ Interaction.EOM(Interaction.FAILURE, ex);
+ } catch (Exception ex) {
+ Interaction.EOM(Interaction.FAILURE, ex, "[FATAL]");
+ running = false;
+ }
+ }
+
+ void Exit() {
+ this.running = false;
+ }
+ }
+
+}
\ No newline at end of file diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs new file mode 100644 index 00000000..48bea01a --- /dev/null +++ b/Source/DafnyServer/Utilities.cs @@ -0,0 +1,61 @@ +using System;
+using System.IO;
+using System.Text;
+using System.Collections.Generic;
+using System.Runtime.Serialization;
+using System.Runtime.Serialization.Json;
+using Microsoft.Boogie;
+
+namespace Microsoft.Dafny {
+ class Interaction {
+ internal static string SUCCESS = "SUCCESS";
+ internal static string FAILURE = "FAILURE";
+ internal static string SERVER_EOM_TAG = "[[DAFNY-SERVER: EOM]]";
+ internal static string CLIENT_EOM_TAG = "[[DAFNY-CLIENT: EOM]]";
+
+ internal static void EOM(string header, string msg) {
+ var trailer = (msg == null) ? "" : "\n";
+ Console.Write("{0}{1}[{2}] {3}\n", msg ?? "", trailer, header, SERVER_EOM_TAG);
+ Console.Out.Flush();
+ }
+
+ internal static void EOM(string header, Exception ex, string subHeader = "") {
+ var aggregate = ex as AggregateException;
+ subHeader = String.IsNullOrEmpty(subHeader) ? "" : subHeader + " ";
+
+ if (aggregate == null) {
+ EOM(header, subHeader + ex.Message);
+ } else {
+ EOM(header, subHeader + aggregate.InnerExceptions.MapConcat(exn => exn.Message, ", "));
+ }
+ }
+ }
+
+ class ServerException : Exception {
+ internal ServerException(string message) : base(message) { }
+ internal ServerException(string message, params object[] args) : base(String.Format(message, args)) { }
+ }
+
+ class ServerUtils {
+ internal static void checkArgs(string[] command, int expectedLength) {
+ if (command.Length - 1 != expectedLength) {
+ throw new ServerException("Invalid argument count (got {0}, expected {1})", command.Length - 1, expectedLength);
+ }
+ }
+
+ internal static void ApplyArgs(string[] args, ErrorReporter reporter) {
+ Dafny.DafnyOptions.Install(new Dafny.DafnyOptions(reporter));
+ Dafny.DafnyOptions.O.ProverKillTime = 10; //This is just a default; it can be overriden
+
+ if (CommandLineOptions.Clo.Parse(args)) {
+ DafnyOptions.O.VerifySnapshots = 2; // Use caching
+ DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount / 2); // Don't use too many cores
+ DafnyOptions.O.PrintTooltips = true; // Dump tooptips (ErrorLevel.Info) to stdout
+ //DafnyOptions.O.UnicodeOutput = true; // Use pretty warning signs
+ DafnyOptions.O.TraceProofObligations = true; // Show which method is being verified, but don't show duration of verification
+ } else {
+ throw new ServerException("Invalid command line options");
+ }
+ }
+ }
+}
diff --git a/Source/DafnyServer/VerificationTask.cs b/Source/DafnyServer/VerificationTask.cs new file mode 100644 index 00000000..eb740e70 --- /dev/null +++ b/Source/DafnyServer/VerificationTask.cs @@ -0,0 +1,58 @@ +using System;
+using System.Collections.Generic;
+using System.IO;
+using System.Linq;
+using System.Runtime.Serialization;
+using System.Runtime.Serialization.Json;
+using System.Text;
+using System.Threading.Tasks;
+
+namespace Microsoft.Dafny {
+ [Serializable]
+ class VerificationTask {
+ [DataMember]
+ string[] args = null;
+
+ [DataMember]
+ string filename = null;
+
+ [DataMember]
+ string source = null;
+
+ [DataMember]
+ bool sourceIsFile = false;
+
+ string ProgramSource { get { return sourceIsFile ? File.ReadAllText(source) : source; } }
+
+ internal static VerificationTask ReadTask(string b64_repr) {
+ try {
+ var json = Encoding.UTF8.GetString(System.Convert.FromBase64String(b64_repr));
+ using (MemoryStream ms = new MemoryStream(Encoding.Unicode.GetBytes(json))) {
+ DataContractJsonSerializer serializer = new DataContractJsonSerializer(typeof(VerificationTask));
+ return (VerificationTask)serializer.ReadObject(ms);
+ }
+ } catch (Exception ex) {
+ throw new ServerException("Deserialization failed: {0}.", ex.Message);
+ }
+ }
+
+ internal static void SelfTest() {
+ var task = new VerificationTask() {
+ filename = "<none>",
+ sourceIsFile = false,
+ args = new string[] { },
+ source = "method selftest() { assert true; }"
+ };
+ try {
+ task.Run();
+ Interaction.EOM(Interaction.SUCCESS, null);
+ } catch (Exception ex) {
+ Interaction.EOM(Interaction.FAILURE, ex);
+ }
+ }
+
+ internal void Run() {
+ new DafnyHelper(args, filename, ProgramSource).Verify();
+ }
+ }
+}
|