From b48d6c264b46a0ca709054141bb383a9d00c9063 Mon Sep 17 00:00:00 2001 From: Samuel Gruetter Date: Thu, 1 Aug 2019 20:56:52 -0700 Subject: [PATCH 1/5] first draft for exceptions --- Exceptions.md | 199 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 199 insertions(+) create mode 100644 Exceptions.md diff --git a/Exceptions.md b/Exceptions.md new file mode 100644 index 0000000..8f84171 --- /dev/null +++ b/Exceptions.md @@ -0,0 +1,199 @@ +# Exceptions + +## Preliminaries + +By `Result`, we mean the following datatype: + +``` +datatype Result = +| Success(value: T) +| Failure(error: string) +``` + +For simplicity, we use "C#" to refer to any target language into which Dafny compiles. + +## Motivations + +### More readable Dafny code + +At the moment, we're writing a lot of code of the following form: + +``` +var res1: Result := operation1(args1); +if res1.Failure? { + return Failure(res1.error); +} +var value1: T1 := res1.get; + +var res2: Result := operation2(args2); +if res2.Failure? { + return Failure(res2.error); +} +var value2: T2 := res2.get; + +... +``` + +It would be nicer to have more concise code, which could look like this: +``` +var value1: T1 :- operation1(args1); +var value2: T2 :- operation2(args2); +... +``` + +### Less glue code to interoperate with other languages + +Many Dafny libraries will live in a "sandwich" between two layers of C# code (or any other language Dafny compiles to): +* Code written in C# by clients who find it cool to use verified software, but don't want to write Dafny themselves +* Code written in Dafny, compiled to C# +* Primitives written in C# which cannot be written in Dafny (eg networking, file system access, etc) + +Both the layer above and the layer below the Dafny layer use exceptions, and at the moment, we have to wrap the primitives to turn exceptions into something Dafny understands, and then wrap the Dafny-generated C# code into exception-producing code, because clients don't want to deal with types such as `Result` or `Option`, they want exceptions. +It would be good to get rid of these two extra layers of wrappers. + +### Don't swallow exceptions if you can't handle them + +If an exception is thrown in the primitives layer, it should be possible to let it bubble up through the layers all the way up to the client code, because in many situations, only the client code knows how to deal with the exception appropriately. +For instance, if the exception is a network failure, and we're in an application which has an offline mode, we don't want the lower layers to swallow the exception and return some dummy value, or terminate the program, but the exception should be passed on to the client app, which could just say, "ok so let's switch to offline mode". + +### Printing stack traces + +While a client is debugging their app, it would be useful for them to get a stack trace in case of unhandled exceptions which goes all the way through the stack, and is not interrupted by the Dafny layer. + + +## Implementation + +The type `Result` is hardcoded into Dafny, the same way as `seq`, `map`, `int`, etc. + +Given a `MethodCall(args)` which returns `Result`, let's define + +``` +var v :- MethodCall(args); +... rest of the code using v as if it had type T ... +``` + +to be syntactic sugar for + +``` +var res_v: Result := MethodCall(args); +if res_v.Failure? { + return Failure(res_v.error); +} +var v := res_v.value; +... rest of the code using v as if it had type T ... +``` + +as far as verification and Boogie is concerned. + +We will not really implement it as syntactic sugar, though, because we want a separate AST node for this so that the compiler can regognize it easily. + +The compiler will then compile all methods which return `Result` into C# methods with signatures of the form + +``` +public T MethodCall(A1 a1, A2 a2, ...) throws Exception +``` + +(Note that C# method signatures do not have `throws` clauses, but we just add them here for clarity, even though that's not valid C# code). + +In particular, the same signature translation also applies for methods annotated with `{:extern}`, so for instance, given the C# method `System.IO.Stream.Read` with signature + +``` +public int Read (byte[] buffer, int offset, int count) +``` + +one could write a Dafny stub for it as + +``` +method {:extern} Read(buffer: array, offset: int32, count: int32) returns (nRead: Result) +``` + +which would enable us to call exception-throwing C# methods from Dafny without an extra unverified layer turning exceptions into `Result`. + +In the same way, methods implemented in Dafny which return `Result` would be compiled to exception-throwing methods and thus be directly usable by C# client programs. + +Moreover, + +``` +return Failure(someErrorMsg); +``` + +is compiled into a `throw` statement: + +``` +throw new Exception(dafnyStringToNativeString(someErrorMsg)); +``` + +Compilation of + +``` +return Success(someValue); +``` + +simply drops the wrapping: + +``` +return someValue; +``` + +And the new Dafny construct + +``` +var value1: T1 :- operation1(args1); +``` + +is simply compiled into + +``` +var value1 = operation1(args1); +``` + +and the handling of the failure case is done by C#'s exception mechanism. + + +## FAQ + +*Q:* Are we also adding special syntax/support for this inside expressions? +*A:* Not at the moment + +*Q:* What about target languages which do not have exceptions, such as Go? +*A:* Go uses a pattern of returning an additional return value to report success/failure, and the Dafny-to-Go compiler would use this pattern too. In general, the idea is to compile `Result` to the idiomatic way of dealing with failure in the target language, be it exceptions, extra return values, `Option`, `Maybe`, ... + +*Q:* Can this work for methods which have multiple return values? +*A:* It seems so. + + +## Discussion points, open questions + +### Should `Result` be first-class? + +Should it be possible to pass around values of type `Result`? That is, should it be allowed to assign a `Result` to a variable, or to pass a `Result` to a method? Say the user writes +``` +var res1: Result := operation1(args1); +anotherMethodCall(res1); +``` +If this happens, and the compiler compiled `operation1` into a `public T1 operation1(args) throws Exception`, then the code generated for the above snippet would have to catch the exception and materialize it into a `Result`. +In most cases, this is probably not the code which the user meant to write, so the questions are: Should this still be supported? Should it emit a warning? Should it emit an error? + + +### How to support returning through assignement instead of `return`? + +Should the following be supported? + +``` +method Test() returns (res: Result) { + res := someMethodCall(); + if changedMyMind() { + res := someOtherMethodCall(); + } +} +``` + +The most straightforward way of supporting this would be to surround `someMethodCall` and `someOtherMethodCall` with a `try/catch` block, materialize their result into a `Result`, and at the end of the method body, to return `res.get` or throw `res.error`. +This seems inefficient, can we do better? +Should it be supported at all, or would we only allow `return` in methods returning `Result`, but no assignment to the result variable? + + +## Status + +This has not been implemented yet, and not been fully thought trough yet, so it could be that we oversaw problems which would make this impossible. + From 05ea8c7504fc69b57e50a7e59fc2246f660bc4a4 Mon Sep 17 00:00:00 2001 From: Samuel Gruetter Date: Thu, 1 Aug 2019 21:14:02 -0700 Subject: [PATCH 2/5] update exceptions rfc --- Exceptions.md | 38 +++++++++++++++++++++++--------------- 1 file changed, 23 insertions(+), 15 deletions(-) diff --git a/Exceptions.md b/Exceptions.md index 8f84171..285b601 100644 --- a/Exceptions.md +++ b/Exceptions.md @@ -21,13 +21,13 @@ At the moment, we're writing a lot of code of the following form: ``` var res1: Result := operation1(args1); if res1.Failure? { - return Failure(res1.error); + return Failure(res1.error); } var value1: T1 := res1.get; var res2: Result := operation2(args2); if res2.Failure? { - return Failure(res2.error); + return Failure(res2.error); } var value2: T2 := res2.get; @@ -77,15 +77,15 @@ to be syntactic sugar for ``` var res_v: Result := MethodCall(args); if res_v.Failure? { - return Failure(res_v.error); + return Failure(res_v.error); } var v := res_v.value; ... rest of the code using v as if it had type T ... ``` -as far as verification and Boogie is concerned. +as far as verification and Boogie are concerned. -We will not really implement it as syntactic sugar, though, because we want a separate AST node for this so that the compiler can regognize it easily. +We will not really implement it as syntactic sugar, though, because we want a separate AST node for this so that the compiler can recognize it easily. The compiler will then compile all methods which return `Result` into C# methods with signatures of the form @@ -152,14 +152,17 @@ and the handling of the failure case is done by C#'s exception mechanism. ## FAQ -*Q:* Are we also adding special syntax/support for this inside expressions? -*A:* Not at the moment +**Q:** Are we also adding special syntax/support for this inside expressions? -*Q:* What about target languages which do not have exceptions, such as Go? -*A:* Go uses a pattern of returning an additional return value to report success/failure, and the Dafny-to-Go compiler would use this pattern too. In general, the idea is to compile `Result` to the idiomatic way of dealing with failure in the target language, be it exceptions, extra return values, `Option`, `Maybe`, ... +**A:** Not at the moment -*Q:* Can this work for methods which have multiple return values? -*A:* It seems so. +**Q:** What about target languages which do not have exceptions, such as Go? + +**A:** Go uses a pattern of returning an additional return value to report success/failure, and the Dafny-to-Go compiler would use this pattern too. In general, the idea is to compile `Result` to the idiomatic way of dealing with failure in the target language, be it exceptions, extra return values, `Option`, `Maybe`, ... + +**Q:** Can this work for methods which have multiple return values? + +**A:** It seems so. ## Discussion points, open questions @@ -181,10 +184,10 @@ Should the following be supported? ``` method Test() returns (res: Result) { - res := someMethodCall(); - if changedMyMind() { - res := someOtherMethodCall(); - } + res := someMethodCall(); + if changedMyMind() { + res := someOtherMethodCall(); + } } ``` @@ -193,6 +196,11 @@ This seems inefficient, can we do better? Should it be supported at all, or would we only allow `return` in methods returning `Result`, but no assignment to the result variable? +### What's the name for this? + +Googling `:-` will be very hard, so to make this new syntax less confusing, it would be good to agree on one canonical name for this feature, and use that same name everywhere (Dafny source code, documentation, blog posts, etc). + + ## Status This has not been implemented yet, and not been fully thought trough yet, so it could be that we oversaw problems which would make this impossible. From c9fb1db6fb92c220d82f9c2efcd2fd33f849143a Mon Sep 17 00:00:00 2001 From: Samuel Gruetter Date: Tue, 6 Aug 2019 10:24:46 -0700 Subject: [PATCH 3/5] What about exception-throwing methods returning void? --- Exceptions.md | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/Exceptions.md b/Exceptions.md index 285b601..7eb9aaf 100644 --- a/Exceptions.md +++ b/Exceptions.md @@ -196,6 +196,44 @@ This seems inefficient, can we do better? Should it be supported at all, or would we only allow `return` in methods returning `Result`, but no assignment to the result variable? +### What about exception-throwing methods returning void? + +The C# signature + +``` +void Test() throws Exception +``` + +would be represented as + +``` +method Test() returns (res: Result) +``` + +in Dafny, where + +``` +datatype Void = Void +``` + +is a single-constructor datatype to be added. Should `Void` also be a hardcoded type, or part of an always-included library? + +Moreover, how should such methods be called? + +``` +// (1) +var _ :- Test(); + +// (2) +:- Test(); + +// (3) +Test(); +``` + +Note that (3) currently is rejected by Dafny ("wrong number of method result arguments (got 0, expected 1)"), so (3) would not change the semantics of any existing valid Dafny code. + + ### What's the name for this? Googling `:-` will be very hard, so to make this new syntax less confusing, it would be good to agree on one canonical name for this feature, and use that same name everywhere (Dafny source code, documentation, blog posts, etc). From 9b22dd10a817b19c17671367e75e407dfd4d4fb4 Mon Sep 17 00:00:00 2001 From: Samuel Gruetter Date: Wed, 7 Aug 2019 17:24:47 -0700 Subject: [PATCH 4/5] update exceptions rfc --- Exceptions.md | 215 +++++++++++++++++++++++++++++++++++--------------- 1 file changed, 153 insertions(+), 62 deletions(-) diff --git a/Exceptions.md b/Exceptions.md index 7eb9aaf..9f7ccbc 100644 --- a/Exceptions.md +++ b/Exceptions.md @@ -2,16 +2,121 @@ ## Preliminaries +The examples in this document depend on the following small "library": + +``` +function method Unreachable(): R + requires false +{ + var o: Option := None; + assert o.Some?; + o.get +} + +datatype Option = None | Some(get: T) +``` + By `Result`, we mean the following datatype: ``` datatype Result = | Success(value: T) | Failure(error: string) +{ + predicate method IsFailure() { + this.Failure? + } + function method PropagateFailure(): Result requires IsFailure() { + Failure(this.error) + } + function method Extract(): T requires !IsFailure() { + this.value + } +} +``` + +Note that this is a datatype with instance methods, a feature which is not yet in Dafny at the moment, but will soon be added. + +Moreover, we will also use a type `NatOutcome`, which is a bit like `Result`, but uses traits and classes instead of a dataype, and hardcodes the type `T` to be `nat`: + +``` +trait NatOutcome { + predicate method IsFailure() + function method PropagateFailure(): NatOutcome requires IsFailure() + function method Extract(): nat requires !IsFailure() +} + +class NatSuccess extends NatOutcome { + const value: nat + constructor(value: nat) { + this.value := value; + } + predicate method IsFailure() { + false + } + function method PropagateFailure(): NatOutcome requires IsFailure() { + Unreachable() + } + function method Extract(): nat requires !IsFailure() { + value + } +} + +class NatFailure extends NatOutcome { + predicate method IsFailure() { + true + } + function method PropagateFailure(): NatOutcome requires IsFailure() { + this + } + function method Extract(): nat requires !IsFailure() { + Unreachable() + } +} +``` + +And finally, the example will also use a generic `Outcome` type, which is not supported by Dafny at the moment, because traits can't have type parameters, but we want to keep this example in mind in the design because type parameters might be added to traits at some point. + +``` +trait Outcome { + predicate method IsFailure() + function method PropagateFailure(): Outcome requires IsFailure() + function method Extract(): T requires !IsFailure() +} + +class Success extends Outcome { + const value: T + constructor(value: T) { + this.value := value; + } + predicate method IsFailure() { + false + } + method PropagateFailure() returns (o: Outcome) requires IsFailure() { + o := Unreachable>(); + } + method Extract() returns (t: T) requires !IsFailure() { + t := value; + } +} + +class Failure extends Outcome { + const error: string + predicate method IsFailure() { + true + } + method PropagateFailure() returns (o: Outcome) requires IsFailure() { + o := Failure(this.error); + } + method Extract() returns (t: T) requires !IsFailure() { + t := Unreachable(); + } +} ``` For simplicity, we use "C#" to refer to any target language into which Dafny compiles. + ## Motivations ### More readable Dafny code @@ -23,13 +128,13 @@ var res1: Result := operation1(args1); if res1.Failure? { return Failure(res1.error); } -var value1: T1 := res1.get; +var value1: T1 := res1.value; var res2: Result := operation2(args2); if res2.Failure? { return Failure(res2.error); } -var value2: T2 := res2.get; +var value2: T2 := res2.value; ... ``` @@ -61,33 +166,57 @@ For instance, if the exception is a network failure, and we're in an application While a client is debugging their app, it would be useful for them to get a stack trace in case of unhandled exceptions which goes all the way through the stack, and is not interrupted by the Dafny layer. -## Implementation - -The type `Result` is hardcoded into Dafny, the same way as `seq`, `map`, `int`, etc. +## Language-level changes -Given a `MethodCall(args)` which returns `Result`, let's define +The grammar of expressions is augmented with the following two forms: ``` -var v :- MethodCall(args); -... rest of the code using v as if it had type T ... +var x :- E; F +:- E; F ``` -to be syntactic sugar for +where `E` and `F` are expressions, and `x` is a variable name or a pattern. + +The grammar of statements is augmented with the following six forms: ``` -var res_v: Result := MethodCall(args); -if res_v.Failure? { - return Failure(res_v.error); -} -var v := res_v.value; -... rest of the code using v as if it had type T ... +var x :- M(...); +y :- M(...); +:- M(...); +var x :- E; +y :- E; +:- E; ``` -as far as verification and Boogie are concerned. +where `M` is a method name, `E` is an expression, `x` is a variable name or a pattern, and `y` is a (previously declared) variable. + +We say that a type `A` `SupportsNonVoidErrorHandling` if all of these are true: +* it has a member called `IsFailure` +* it has a member called `PropagateFailure` +* it has a member called `Extract` + +We say that a type `A` `SupportsVoidErrorHandling` if it has the following members: +* it has a member called `IsFailure` +* it has a member called `PropagateFailure` +* it has no member called `Extract` + +Note that we do not make any requirements on how many arguments and how many type parameters the above members have, nor on their return types, nor on whether they are functions, function methods, methods, or ghost methdos; as long as the code produced (as described below) makes type parameter inference and typechecking work, it's fine. -We will not really implement it as syntactic sugar, though, because we want a separate AST node for this so that the compiler can recognize it easily. +In the following, we will define how each of the above new grammar forms is desugared. +Let `EorM` be an expression or method call, let `TM` be its type, let `E` be an expression, let `TE` be the type of `E` and let `temp` denote a fresh variable name. -The compiler will then compile all methods which return `Result` into C# methods with signatures of the form +* Expression `var x :- E; F`: If `TE` `SupportsNonVoidErrorHandling` then desugar into `var temp := E; if temp.IsFailure() then temp.PropagateFailure() else var x := temp.Extract(); F` else emit error "`TE` does not support non-void error handling" +* Expression `:- E; F`: If `TE` `SupportsVoidErrorHandling` then desugar into `var temp := E; if temp.IsFailure() then temp.PropagateFailure() else F` else emit error "`TE` does not support void error handling" +* Statement `var x :- EorM;`: If `TM` `SupportsNonVoidErrorHandling` then desugar into `var temp := EorM; if temp.IsFailure() { return temp.PropagateFailure(); } var x := temp.Extract();` else emit error "`TM` does not support non-void error handling" +* Statement `y :- EorM;`: If `TM` `SupportsNonVoidErrorHandling` then desugar into `var temp := EorM; if temp.IsFailure() { return temp.PropagateFailure(); } y := temp.Extract();` else emit error "`TM` does not support non-void error handling" +* Statement `:- EorM;`: If `TM` `SupportsVoidErrorHandling` then desugar into `var temp := EorM; if temp.IsFailure() { return temp.PropagateFailure(); }` else emit error "`TM` does not support void error handling" + +Note that there are cases where the desugaring succeeds, yet the typechecker will fail on the produced desugared expression, and this is intended. + + +## Dafny-to-C# compiler changes + +The compiler will compile all methods which return a type which `SupportsErrorHandling` into C# methods with signatures of the form ``` public T MethodCall(A1 a1, A2 a2, ...) throws Exception @@ -152,17 +281,17 @@ and the handling of the failure case is done by C#'s exception mechanism. ## FAQ -**Q:** Are we also adding special syntax/support for this inside expressions? - -**A:** Not at the moment - **Q:** What about target languages which do not have exceptions, such as Go? **A:** Go uses a pattern of returning an additional return value to report success/failure, and the Dafny-to-Go compiler would use this pattern too. In general, the idea is to compile `Result` to the idiomatic way of dealing with failure in the target language, be it exceptions, extra return values, `Option`, `Maybe`, ... **Q:** Can this work for methods which have multiple return values? -**A:** It seems so. +**A:** Not really, but one can always just return a tuple. + +**Q:** Should `IsFailure`, `PropagateFailure`, `Extract` be functions or methods? + +**A:** `IsFailure` has to be a function, because it appears in the preconditions of the other two. We allow the user to choose whether `PropagateFailure` and `Extract` are functions, function methods, methods or ghost methods, but depending on what the user chooses, this exception handling feature might not be available in expressions or in statements. Note that requiring them to be function methods would prevent `PropagateFailure` from allocating a new object. ## Discussion points, open questions @@ -191,49 +320,11 @@ method Test() returns (res: Result) { } ``` -The most straightforward way of supporting this would be to surround `someMethodCall` and `someOtherMethodCall` with a `try/catch` block, materialize their result into a `Result`, and at the end of the method body, to return `res.get` or throw `res.error`. +The most straightforward way of supporting this would be to surround `someMethodCall` and `someOtherMethodCall` with a `try/catch` block, materialize their result into a `Result`, and at the end of the method body, to return `res.value` or throw `res.error`. This seems inefficient, can we do better? Should it be supported at all, or would we only allow `return` in methods returning `Result`, but no assignment to the result variable? -### What about exception-throwing methods returning void? - -The C# signature - -``` -void Test() throws Exception -``` - -would be represented as - -``` -method Test() returns (res: Result) -``` - -in Dafny, where - -``` -datatype Void = Void -``` - -is a single-constructor datatype to be added. Should `Void` also be a hardcoded type, or part of an always-included library? - -Moreover, how should such methods be called? - -``` -// (1) -var _ :- Test(); - -// (2) -:- Test(); - -// (3) -Test(); -``` - -Note that (3) currently is rejected by Dafny ("wrong number of method result arguments (got 0, expected 1)"), so (3) would not change the semantics of any existing valid Dafny code. - - ### What's the name for this? Googling `:-` will be very hard, so to make this new syntax less confusing, it would be good to agree on one canonical name for this feature, and use that same name everywhere (Dafny source code, documentation, blog posts, etc). From 250686552d3c2aeec8fc471229083a9f1e2c2047 Mon Sep 17 00:00:00 2001 From: Samuel Gruetter Date: Wed, 7 Aug 2019 18:37:52 -0700 Subject: [PATCH 5/5] add optional type annotations --- Exceptions.md | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/Exceptions.md b/Exceptions.md index 9f7ccbc..1d93b81 100644 --- a/Exceptions.md +++ b/Exceptions.md @@ -171,24 +171,25 @@ While a client is debugging their app, it would be useful for them to get a stac The grammar of expressions is augmented with the following two forms: ``` -var x :- E; F +var x: T :- E; F :- E; F ``` -where `E` and `F` are expressions, and `x` is a variable name or a pattern. +where `E` and `F` are expressions, `T` is a type, and `x` is a variable name or a pattern. The grammar of statements is augmented with the following six forms: ``` -var x :- M(...); +var x: T :- M(...); y :- M(...); :- M(...); -var x :- E; +var x: T :- E; y :- E; :- E; ``` -where `M` is a method name, `E` is an expression, `x` is a variable name or a pattern, and `y` is a (previously declared) variable. +where `M` is a method name, `E` is an expression, `T` is a type, `x` is a variable name or a pattern, and `y` is a (previously declared) variable. +The `: T` annotation is optional both for expressions and statements. We say that a type `A` `SupportsNonVoidErrorHandling` if all of these are true: * it has a member called `IsFailure` @@ -205,9 +206,9 @@ Note that we do not make any requirements on how many arguments and how many typ In the following, we will define how each of the above new grammar forms is desugared. Let `EorM` be an expression or method call, let `TM` be its type, let `E` be an expression, let `TE` be the type of `E` and let `temp` denote a fresh variable name. -* Expression `var x :- E; F`: If `TE` `SupportsNonVoidErrorHandling` then desugar into `var temp := E; if temp.IsFailure() then temp.PropagateFailure() else var x := temp.Extract(); F` else emit error "`TE` does not support non-void error handling" +* Expression `var x: T :- E; F`: If `TE` `SupportsNonVoidErrorHandling` then desugar into `var temp := E; if temp.IsFailure() then temp.PropagateFailure() else var x: T := temp.Extract(); F` else emit error "`TE` does not support non-void error handling" * Expression `:- E; F`: If `TE` `SupportsVoidErrorHandling` then desugar into `var temp := E; if temp.IsFailure() then temp.PropagateFailure() else F` else emit error "`TE` does not support void error handling" -* Statement `var x :- EorM;`: If `TM` `SupportsNonVoidErrorHandling` then desugar into `var temp := EorM; if temp.IsFailure() { return temp.PropagateFailure(); } var x := temp.Extract();` else emit error "`TM` does not support non-void error handling" +* Statement `var x: T :- EorM;`: If `TM` `SupportsNonVoidErrorHandling` then desugar into `var temp := EorM; if temp.IsFailure() { return temp.PropagateFailure(); } var x: T := temp.Extract();` else emit error "`TM` does not support non-void error handling" * Statement `y :- EorM;`: If `TM` `SupportsNonVoidErrorHandling` then desugar into `var temp := EorM; if temp.IsFailure() { return temp.PropagateFailure(); } y := temp.Extract();` else emit error "`TM` does not support non-void error handling" * Statement `:- EorM;`: If `TM` `SupportsVoidErrorHandling` then desugar into `var temp := EorM; if temp.IsFailure() { return temp.PropagateFailure(); }` else emit error "`TM` does not support void error handling"