Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat(TestModels): Resource #103

Merged
merged 47 commits into from
Feb 24, 2023
Merged

feat(TestModels): Resource #103

merged 47 commits into from
Feb 24, 2023

Conversation

texastony
Copy link
Contributor

@texastony texastony commented Jan 31, 2023 •
edited
Loading

Issue #, if available: CrypTool-4913

Description of changes:

  • fix(smithy-dotnet): Local Service Wrapper
  • feat(TestModels): Resource

Squash and Merge:

feat(TestModels): Resource

* fix(smithy-dotnet): Local Service Wrapper

TODO:

  • Add to GitHub Workflows
  • Author README

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

@texastony
test(resource): init testing of resource shim in C#
4a5d2c2 
Ran:
git checkout smithy-test-models -- resources.smithy
@texastony
fix(resources): polymorph's smithydotnet does not handle bigInit or b…
a74aaa9 
…igDecimal

We may have to address this later.
@texastony
feat: init Makefile for test
ee3e4b0 
Oi... this depends on all the simple types...
Is that intentional?
Or is that a mistake when we authored this Smithy?
@texastony
chore: ignore JetBrains
df4a884
@texastony
fix: resources.smithy
e1b2cc3 
Our Dafny code generator does not support:
- Bytes
- Shorts
- Floats
- BigInteger
- BigDecimal
- Timestamp
@texastony
fix: smithy-polymorph call's Model must be a directory
f144f7d 
Or smithy-polymorph will not output a Types.dfy.
@texastony
chore: ignore generate types files
93d66b6
@texastony
chore: ignore generated dafny in tests
915e470
@texastony
fix: Polymorph smithy-dafny MUST write to Model
717ccd2
@texastony
Merge branch 'main-1.x' into tony/test-resources
19ff9bf
@texastony
Merge branch 'main-1.x' into tony/test-resources
9c0aee2
@texastony
Merge branch 'main-1.x' into tony/test-resources
d7518c1
@texastony
fix: Service needs a concrete error
fa0c8d6
@texastony
feat: Simple implementaiton
f495b3d
@texastony
Merge branch 'main-1.x' into tony/test-resources
1af036c
@texastony
feat: Simple Resource Service
4fd0bfc
@texastony
refactor: remove un-needed post-conditions
e9060c4
@texastony
feat: compile impl to C#
6fa9de7
@texastony
wip: test the implementation
f073948 
Issue: transpile_test_net is failing:

```
$ make polymorph_dafny verify polymorph_net transpile_net
dafny \
	  -vcsCores:2 \
	  -compileTarget:cs \
	  -spillTargetCode:3 \
	  -compile:0 \
	  -optimizeErasableDatatypeWrapper:0 \
	  -useRuntimeLib \
	  -out runtimes/net/tests/TestsFromDafny \
	  -library /Volumes/workplace/ryan-new-world/polymorph/TestModels/resources/src/Index.dfy \
	  `find ./test -name '*.dfy'`
Unhandled exception. System.AggregateException: One or more errors occurred. (Object reference not set to an instance of an object.)
 ---> System.NullReferenceException: Object reference not set to an instance of an object.
   at Microsoft.Dafny.ErrorReporter.Error(MessageSource source, IToken tok, String msg) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Reporting.cs:line 45
   at Microsoft.Dafny.ErrorReporter.Error(MessageSource source, IToken tok, String msg, Object[] args) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Reporting.cs:line 67
   at Microsoft.Dafny.Resolver.ResolveMember(IToken tok, Type receiverType, String memberName, NonProxyType& tentativeReceiverType) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 12384
   at Microsoft.Dafny.Resolver.EnsureSupportsErrorHandling(IToken tok, Type tp, Boolean expectExtract, Boolean hasKeywordToken) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 11884
   at Microsoft.Dafny.Resolver.ResolveAssignOrReturnStmt(AssignOrReturnStmt s, ResolutionContext resolutionContext) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 11866
   at Microsoft.Dafny.Resolver.ResolveConcreteUpdateStmt(ConcreteUpdateStatement s, ResolutionContext resolutionContext) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 11476
   at Microsoft.Dafny.Resolver.ResolveStatement(Statement stmt, ResolutionContext resolutionContext) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 9581
   at Microsoft.Dafny.Resolver.ResolveStatementWithLabels(Statement stmt, ResolutionContext resolutionContext) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 12132
   at Microsoft.Dafny.Resolver.ResolveBlockStatement(BlockStmt blockStmt, ResolutionContext resolutionContext) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 12102
   at Microsoft.Dafny.Resolver.ResolveMethod(Method m) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 8809
   at Microsoft.Dafny.Resolver.ResolveClassMemberBodies(TopLevelDeclWithMembers cl) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 8001
   at Microsoft.Dafny.Resolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, Boolean isAnExport) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 2854
   at Microsoft.Dafny.Resolver.ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig, Boolean isAnExport) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 1043
   at Microsoft.Dafny.Resolver.ResolveProgram(Program prog) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 510
   at Microsoft.Dafny.Main.Resolve(Program program, ErrorReporter reporter) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/DafnyMain.cs:line 215
   at Microsoft.Dafny.Main.ParseCheck(IList`1 files, String programName, ErrorReporter reporter, Program& program) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/DafnyMain.cs:line 166
   at Microsoft.Dafny.DafnyDriver.ProcessFilesAsync(IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId) in /Volumes/workplace/dafny_src/dafny/Source/DafnyDriver/DafnyDriver.cs:line 345
   --- End of inner exception stack trace ---
   at System.Threading.Tasks.Task.ThrowIfExceptional(Boolean includeTaskCanceledExceptions)
   at System.Threading.Tasks.Task`1.GetResultCore(Boolean waitCompletionNotification)
   at System.Threading.Tasks.Task`1.get_Result()
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args) in /Volumes/workplace/dafny_src/dafny/Source/DafnyDriver/DafnyDriver.cs:line 123
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass10_0.<Main>b__0() in /Volumes/workplace/dafny_src/dafny/Source/DafnyDriver/DafnyDriver.cs:line 100
   at System.Threading.Thread.StartCallback()
/Users/tonyknap/workplace/dafny_src/dafny_path/dafny: line 34: 15045 Abort trap: 6           "$DOTNET" "$DAFNY" "$@"
make: *** [transpile_test_net] Error 134
```
@texastony
wip: transpile_net_test still fails w/ very simple test
4e7cf00
@texastony
Merge branch 'main-1.x' of github.com:awslabs/polymorph into tony/tes…
9cd0b43 
…t-resources
@texastony
wip: transpile_net_test still fails w/ very simple test
813dc9e
@texastony
wip: transpile_net_test still fails w/ very simple test
77b53ac
@texastony
wip: trans_net_test still fails w/o Independent Config
ba5b980
@texastony
debug: force check in Types
ca735c2
@texastony
Copy link
Contributor Author

texastony commented Feb 3, 2023 •
edited
Loading

For Dafny team: content deleted, for Dafny issue is #131

@texastony
fix(csproj): include Extern in test
30fe621
@texastony
wip: Test Wrapped Service
21db487 
`test_net` now fails with:
```
/Volumes/workplace/ryan-new-world/polymorph/TestModels/resources/runtimes/net/Generated/Wrapped/TypeConversion.cs(190,13): error CS0246: The type or namespace name 'WrappedNativeWrapper_SimpleResource' could not be found (are you missing a using directive or an assembly reference?) [/Volumes/workplace/ryan-new-world/polymorph/TestModels/resources/runtimes/net/SimpleResources.csproj]
```

Which I suspect is smithy-dotnet issue.
It may be that smithy-dotnet assumes all resources
are extendable.
@texastony
issue: broken wrapped C# code
306cbaf
@texastony
debug: try forcing non-NativeWrapper conversion
fa49b2b
@texastony
debug: try forcing NativeWrapper conversion
70beb46
@texastony
issue: WrappedCodegen's NativeWrapper assumes Exception name
09aafe2 
The C# Native Wrapper assumes an exception exsits
named SimpleResourcesException.
More generically,
it assumes an exception named <Namespace>Exception exsits.

Run:
`make polymorph_dafny polymorph_net verify transpile_net setup_net test_net`
to confirm.
@texastony
fix: issue in 09aafe2
bbe673d
@texastony
style: reformat C# for better comparison
dc44957
@texastony
style: run dotnet format
6fdb22b
texastony
texastony commented Feb 13, 2023
View reviewed changes
Copy link
Contributor Author

@texastony texastony left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Options is imported from Wrappers, which is opened.

TestModels/Resource/src/SimpleResource.dfy Outdated Show resolved Hide resolved
TestModels/Resource/test/Helpers.dfy Outdated Show resolved Hide resolved
@texastony texastony changed the title test(shims): resources feat(TestModels): Resource Feb 13, 2023
@texastony texastony marked this pull request as ready for review February 13, 2023 04:01
@texastony texastony requested a review from a team as a code owner February 13, 2023 04:01
@texastony texastony marked this pull request as draft February 13, 2023 17:49
seebees
seebees previously approved these changes Feb 13, 2023
View reviewed changes
Copy link
Contributor

@seebees seebees left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM!!!

@texastony texastony marked this pull request as ready for review February 23, 2023 21:27
seebees
seebees approved these changes Feb 24, 2023
View reviewed changes
Copy link
Contributor

@seebees seebees left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

@texastony texastony merged commit 0e2ebf9 into main-1.x Feb 24, 2023
@texastony texastony deleted the tony/test-resources branch February 24, 2023 00:30
robin-aws pushed a commit that referenced this pull request Apr 19, 2024
@seebees
chore: consolidate dafny version (#103)
66c493d 
Have a single place for dafny version for CI
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@seebees seebees seebees approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@texastony @seebees