search

smithy-lang / smithy-dafny

Apache License 2.0
9 stars 8 forks source link

Smithy-Dafny does not support services models containing no errors #439

Open justplaz opened 3 months ago

justplaz commented 3 months ago

This issue was found while working on https://github.com/smithy-lang/smithy-dafny/pull/395. A reproduction can be found in https://github.com/smithy-lang/smithy-dafny/pull/395/commits/d8bc3ee458e8a22be9d1784d519c488b27cc0127.

The gist is that when a projection (or a simple model, without projections) does not include an operation which has one or more errors, the transpiled code cannot be executed.

More specifically, the Dafny codegen does generate an OpaqueError, and the generated .NET code expects Error_Opaque, but the transpiled .NET code does not generate Error_Opaque. Also, the structure of the Error class is different than the one generated from a model with one or more errors. For example, in ImplementationFromDafny.cs, Error is a class, but in the transpiled code, Error is an abstract class which each modeled error implements.

robin-aws commented 3 months ago

I also found while working on #462 that a local service with no errors causes an unrelated issue with the Dafny-generated Java (https://github.com/smithy-lang/smithy-dafny/actions/runs/9701124683/job/26774083395):

Exception in thread "main" java.lang.ExceptionInInitializerError
    at simple.positional.internaldafny._ExternBase___default.SimplePositional(_ExternBase___default.java:23)

> Task :runTests FAILED
    at SimplePositionalImplTest_Compile.__default.TestDefaultConfig(__default.java:75)
    at _System.__default.__Test____Main__(__default.java:20)
    at _System.__default.__Main(__default.java:58)
SimplePositionalImplTest.TestDefaultConfig: 3 actionable tasks: 1 executed, 2 up-to-date
    at TestsFromDafny.lambda$main$0(TestsFromDafny.java:14)
    at dafny.Helpers.withHaltHandling(Helpers.java:[34](https://github.com/smithy-lang/smithy-dafny/actions/runs/9701124683/job/26774083395#step:13:35)5)
    at TestsFromDafny.main(TestsFromDafny.java:14)
Caused by: java.lang.NullPointerException
    at dafny.ArrayDafnySequence.empty(DafnySequence.java:506)
    at dafny.DafnySequence.empty(DafnySequence.java:68)
    at simple.positional.internaldafny.types.Error.<clinit>(Error.java:11)
    ... 7 more

I seem to recall this is known and hopefully has a Dafny-side issue already. It has to do with having a cycle in static initialization code, which having at least one case for the Error type seems to resolve.