From 17405efd598d2a8a2dac304ee9a7f7d9bd30a558 Mon Sep 17 00:00:00 2001 From: "Richard L. Ford" Date: Wed, 27 Jan 2016 14:09:16 -0800 Subject: Implement 'extern' declaration modifier. The 'extern' declaration modifier provides a more convenient way of interfacing Dafny code with C# source files and .Net DLLs. We support an 'extern' keyword on a module, class, function method, or method (cannot extern ghost). We check the CompileNames of all modules to make sure there are no duplicate names. Every Dafny-generated C# class is marked partial, so it can potentially be extended. The extern keyword could be accompanied by an optional string naming the corresponding C# method/class to connect to. If not given the name of the method/class is used. An 'extern' keyword implies an {:axiom} attribute for functions and methods, so their ensures clauses are assumed to be true without proof. In addition to the .dfy files, the user may supply C# files (.cs) and dynamic linked libraries (.dll) on command line. These will be passed onto the C# compiler, the .cs files as sources, and the .dll files as references. As part of this change the grammar was refactored some. New productions are - TopDecls - a list of top-level declarations. - TopDecl - a single top-level declaration - DeclModifiers - a list of declaration modifiers which are either 'abstract', 'ghost', 'static', 'protected', or 'extern'. They can be in any order and we diagnose duplicates. In addition, since they are not all allowed in all contexts, we check and give diagnostics if an DeclModifier appears where it is not allowed. --- Test/dafny0/Extern.dfy | 27 +++++++++++++++++++++++++++ Test/dafny0/Extern.dfy.expect | 4 ++++ Test/dafny0/Extern2.cs | 14 ++++++++++++++ Test/dafny0/ExternHelloLibrary.cs | 15 +++++++++++++++ Test/dafny0/ExternHelloLibrary.dll | Bin 0 -> 3072 bytes Test/dafny0/ExternNegative.dfy | 26 ++++++++++++++++++++++++++ Test/dafny0/ExternNegative.dfy.expect | 3 +++ Test/dafny0/ExternNegative2.dfy | 26 ++++++++++++++++++++++++++ 8 files changed, 115 insertions(+) create mode 100644 Test/dafny0/Extern.dfy create mode 100644 Test/dafny0/Extern.dfy.expect create mode 100644 Test/dafny0/Extern2.cs create mode 100644 Test/dafny0/ExternHelloLibrary.cs create mode 100644 Test/dafny0/ExternHelloLibrary.dll create mode 100644 Test/dafny0/ExternNegative.dfy create mode 100644 Test/dafny0/ExternNegative.dfy.expect create mode 100644 Test/dafny0/ExternNegative2.dfy (limited to 'Test') diff --git a/Test/dafny0/Extern.dfy b/Test/dafny0/Extern.dfy new file mode 100644 index 00000000..cbdffe34 --- /dev/null +++ b/Test/dafny0/Extern.dfy @@ -0,0 +1,27 @@ +// RUN: %dafny /compile:1 /print:"%t.print" /dprint:"%t.dprint" "%s" "%S\Extern2.cs" "%S\ExternHelloLibrary.dll" > "%t" +// RUN: %diff "%s.expect" "%t" +extern "Modx" module Mod1 +{ + extern "classx" class Class1 + { + extern "Fun1x" static function method Fun1() : int + ensures Fun1() > 0 + extern "Method1x" static method Method1() returns (x: int) + ensures x > 0 + static function method Fun2() : int + ensures Fun2() > 0 + { + Fun1() + } + static method Method2() returns (x: int) + ensures x > 0 + { + x := Method1(); + } + } + method Main() + { + var m2 := Class1.Method2(); + print ("Fun2() = ", Class1.Fun2(), "Method2() = ", m2, "\n"); + } +} diff --git a/Test/dafny0/Extern.dfy.expect b/Test/dafny0/Extern.dfy.expect new file mode 100644 index 00000000..fec087d9 --- /dev/null +++ b/Test/dafny0/Extern.dfy.expect @@ -0,0 +1,4 @@ + +Dafny program verifier finished with 7 verified, 0 errors +Compiled program written to D:\de\dafny\Test\dafny0\Extern.cs +Compiled assembly into Extern.exe diff --git a/Test/dafny0/Extern2.cs b/Test/dafny0/Extern2.cs new file mode 100644 index 00000000..2fcaf18b --- /dev/null +++ b/Test/dafny0/Extern2.cs @@ -0,0 +1,14 @@ +using System.Numerics; +namespace @Modx { + + public partial class @classx { + public static BigInteger @Fun1x() { + return BigInteger.One; + } + public static void @Method1x(out BigInteger @x) + { + ExternHelloLibrary.ExternHelloLibrary.SayHello(); + @x = BigInteger.One; + } + } +} diff --git a/Test/dafny0/ExternHelloLibrary.cs b/Test/dafny0/ExternHelloLibrary.cs new file mode 100644 index 00000000..81163997 --- /dev/null +++ b/Test/dafny0/ExternHelloLibrary.cs @@ -0,0 +1,15 @@ +// Note that ExternHelloLibrary.dll was produced from this file using +// csc /t:library ExternHelloLibrary.cs + +using System; + +namespace ExternHelloLibrary +{ + public static class ExternHelloLibrary + { + public static void SayHello() + { + Console.WriteLine("Hello from ExternHelloLibrary."); + } + } +} diff --git a/Test/dafny0/ExternHelloLibrary.dll b/Test/dafny0/ExternHelloLibrary.dll new file mode 100644 index 00000000..914e4248 Binary files /dev/null and b/Test/dafny0/ExternHelloLibrary.dll differ diff --git a/Test/dafny0/ExternNegative.dfy b/Test/dafny0/ExternNegative.dfy new file mode 100644 index 00000000..4ae73232 --- /dev/null +++ b/Test/dafny0/ExternNegative.dfy @@ -0,0 +1,26 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +extern "Modx" module Mod1 +{ + extern "classx" class Class1 + { + extern "Fun1x" static function method Fun1() : int + ensures Fun1() > 0 + extern "Method1x" static method Method1() returns (x: int) + ensures x > 0 + static abstract function method Fun2() : int + ensures Fun2() > 0 + { + Fun1() + } + static static method Method2() returns (x: int) + ensures x > 0 + { + x := Method1(); + } + } +} +// Will give error about duplicate CompileName for module. +extern "Modx" module Mod2 +{ +} diff --git a/Test/dafny0/ExternNegative.dfy.expect b/Test/dafny0/ExternNegative.dfy.expect new file mode 100644 index 00000000..5d95ced7 --- /dev/null +++ b/Test/dafny0/ExternNegative.dfy.expect @@ -0,0 +1,3 @@ +ExternNegative.dfy(11,11): Error: Function methods cannot be declared 'abstract'. +ExternNegative.dfy(16,11): Error: Duplicate declaration modifier: static +2 parse errors detected in ExternNegative.dfy diff --git a/Test/dafny0/ExternNegative2.dfy b/Test/dafny0/ExternNegative2.dfy new file mode 100644 index 00000000..3d09913b --- /dev/null +++ b/Test/dafny0/ExternNegative2.dfy @@ -0,0 +1,26 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +extern "Modx" module Mod1 +{ + extern "classx" class Class1 + { + extern "Fun1x" static function method Fun1() : int + ensures Fun1() > 0 + extern "Method1x" static method Method1() returns (x: int) + ensures x > 0 + static function method Fun2() : int + ensures Fun2() > 0 + { + Fun1() + } + static method Method2() returns (x: int) + ensures x > 0 + { + x := Method1(); + } + } +} +// Will give error about duplicate CompileName for module. +extern "Modx" module Mod2 +{ +} -- cgit v1.2.3