Python POC #282

lucasmcdonald3 · 2023-08-15T22:22:49Z

Python codegen for Smithy-Dafny.

This generates conversion code between Dafny-generated Python code and

Polymorph LocalServices
Polymorph wrapped LocalServices
AWS SDKs (boto3 wrapper)

The generated code works for all TestModels, the MPL, and MPL TestVectors.
MPL PR: aws/aws-cryptographic-material-providers-library#171

Sub-PRs

These smaller PRs focus on parts of this PR. These are not functional on their own. These are solely intended for reviewer readability.

Smithy/Dafny conversion. This contains ShapeVisitors that generate code to convert between Smithy and Dafny shapes and NameResolver helpers. https://github.com/lucasmcdonald3/smithy-dafny/pull/12/
TestModel project structure. This contains a file structure layout for TestModels and Python SharedMakefile targets. We would use a similar layout for all Polymorph projects. (This is pending author update -- I plan to change
namespacing soon.) https://github.com/lucasmcdonald3/smithy-dafny/pull/9
Customize code. This contains code that is called from the customize directive. This writes new files, and generally does not need to override any Smithy-Python generated code. https://github.com/lucasmcdonald3/smithy-dafny/pull/10.
Polymorph CLI integration. This allows Python codegen to be used as a target of Polymorph CLI. https://github.com/lucasmcdonald3/smithy-dafny/pull/13
Overwriting and extending Smithy-Python code. This contains code that overwrites Smithy-Python's behavior to make an HTTP request. It also overwrites its request serialization (Smithy to Dafny) and deserialization (Dafny to Smithy) logic. https://github.com/lucasmcdonald3/smithy-dafny/pull/11
- Related: Changes to forked Smithy-Python. This contains changes to Smithy-Python, mostly to make it more extensible for our use case. Changes between Smithy-Python mainline lucasmcdonald3/smithy-python#1

Pending work

"ExternV2"
- Replace PYTHONPATH hacks with Dafny ModuleName. These are identified with TODO-Python-PYTHONPATH.
- Change generated extern names back from _ to . (this will fix Java and Net AWS SDK GHA failures)
Use PyPi DafnyRuntime
Timestamp shapes (not used in MPL I believe; will be needed for DBESDK)

Build instructions

Set up project:

Check out fork with submodules
Build Dafny-nightly-latest from source; set as your default Dafny
Install Python 3.11

Build a TestModel:

make polymorph_dafny
make polymorph_python
make transpile_python
make test_python

GHA Failures

NET/Java/Verification AWS SDKs: I committed a name change to AWS SDKs to help Python out. I will remove this as part of Dafny ModuleName work ("ExternV2").
smithy-dafny-codegen-cli: This should solve itself once Smithy-Python is on Maven central, so I'm not planning to debug it (unless this becomes blocking).

Misc

This PR is WIP. Its primarily provides a testbed for me during development.
I won't merge this in until all CI passes to avoid blocking mainline Smithy-Dafny on in-dev work.
Smithy-Python is included as a submodule. It points to my fork of Smithy-Python. I am not sure how to proceed with having this fork of Smithy-Python. Ideally, we would include Smithy-Python's mainline as a submodule. I will clean up the changes on my fork, get those changes looked at by us, then open a PR against Smithy-Python.

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

robin-aws

Sticking my foot in the door as I really want to review this - feel free to pester me if I haven't started in a week :)

texastony

Praise: I have only viewed 15 files, but I like what I have read so far.

.github/workflows/smithy-dafny-conversion.yml

TestModels/Aggregate/runtimes/python/test/extern/test_dafny_wrapper.py

TestModels/Aggregate/smithy-build.json

texastony · 2023-09-26T22:17:34Z

TestModels/Constraints/runtimes/python/pyproject.toml

Note: I am skipping over the rest of the test Models for now.

texastony · 2023-09-26T22:27:04Z

TestModels/SharedMakefile.mk

+# Hacky workaround until Dafny supports per-language extern names.
+# Replaces `.`s with `_`s in strings like `{:extern ".*"}`.
+# This is flawed logic and should be removed, but is a reasonable band-aid for now.
+# TODO: Once Dafny supports per-language extern names, remove and replace with Pythonic extern names.
+# This is tracked in https://github.com/dafny-lang/dafny/issues/4322.
+# This may require new Smithy-Dafny logic to generate Pythonic extern names.
+_python_underscore_extern_names:
+	find src -regex ".*\.dfy" -type f -exec sed -i $(SED_PARAMETER) '/.*{:extern \".*\".*/s/\./_/g' {} \;
+	find Model -regex ".*\.dfy" -type f -exec sed -i $(SED_PARAMETER) '/.*{:extern \".*\.*"/s/\./_/g' {} \;
+	find test -regex ".*\.dfy" -type f -exec sed -i $(SED_PARAMETER) '/.*{:extern \".*\".*/s/\./_/g' {} \;
+
+_python_underscore_dependency_extern_names:
+	$(MAKE) -C $(STANDARD_LIBRARY_PATH) _python_underscore_extern_names
+	$(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% _python_underscore_extern_names;, $(LIBRARIES))


Praise/Note:
Nice way to "Make it Work".
This is very close to solution written by an ARG Intern from 2019.

codegen/smithy-dafny-codegen-cli/src/main/java/software/amazon/polymorph/CodegenCli.java

texastony · 2023-10-03T00:45:07Z

...odels/dafny-dependencies/StandardLibrary/runtimes/python/src/standard_library/extern/UTF8.py

+Note:
+Python's `.encode('utf-8')` does not handle surrogates.
+These methods are expected to handle surrogates (e.g. "\uD808\uDC00").
+To work around this, we encode Dafny strings into UTF-16-LE (little endian)
+and decode them before encoding into UTF-8 (`_strict_tostring`).
+To decode, we reverse the encode step. (`_reverse_strict_tostring`)


Question: Tell me about the performance characteristics of this implementation.
It appears that we parse every character three times.

For Encoding:

Encode to UTF-16-LE

Decode to ?

Encode to UTF-8

For Decode:

Decode from UTF-8

Is this correct?

We are parsing each character 3 times on decode as well (reverse of encode).

(Obviously I'm not happy about this, but I struggled to handle surrogate characters, and this seemed to be the most commonly suggested pattern to handle those...)

We do not need to block development on this.
But we should not ship a product with this deficiency.

I do not know how often we convert strings,
but I imagine it's often.

This might be a good time to at least discuss the eventual path to using --unicode-char:true in Dafny. A big part of supporting that mode is avoiding exactly this annoying edge case.

...odels/dafny-dependencies/StandardLibrary/runtimes/python/src/standard_library/extern/UTF8.py

…afny into lucmcdon/python-poc

texastony · 2023-10-06T17:50:41Z

Note: https://github.com/smithy-lang/smithy-dafny/blob/lucmcdon/python-poc/.github/workflows/test_models_dafny_verification.yml#L87

It looks like the Python GHA uses Dafny 4.3 but the Dafny Verification uses 4.1.

robin-aws · 2023-10-06T23:09:01Z

Smithy-Python is included as a submodule. It points to my fork of Smithy-Python. I am not sure how to proceed with having this fork of Smithy-Python. Ideally, we would include Smithy-Python's mainline as a submodule. I will clean up the changes on my fork, get those changes looked at by us, then open a PR against Smithy-Python.

What changes did you have to make to smithy-python? If we can get those contributed upstream or find a way to not need them, you could just depend on the software.amazon.smithy.python:smithy-python-codegen package from Maven Central (I'm not sure when they are planning on publishing it there but it's likely pretty soon).

lucasmcdonald3 · 2023-10-09T17:38:24Z

What changes did you have to make to smithy-python? If we can get those contributed upstream or find a way to not need them, you could just depend on the software.amazon.smithy.python:smithy-python-codegen package from Maven Central (I'm not sure when they are planning on publishing it there but it's likely pretty soon).

Changes are here.

* chore: add TestModel for SimpleEnumV2 in Python * chore: enable SimpleEnumV2 Python in CI

robin-aws requested changes Sep 18, 2023

View reviewed changes

texastony reviewed Sep 26, 2023

View reviewed changes

Lucas McDonald added 2 commits September 29, 2023 10:28

comment

a4bbd4d

wrap configs

22eb959

texastony reviewed Oct 2, 2023

View reviewed changes

codegen/smithy-dafny-codegen-cli/src/main/java/software/amazon/polymorph/CodegenCli.java Outdated Show resolved Hide resolved

Lucas McDonald added 4 commits October 2, 2023 15:16

utf8

884706f

fix stdlib

3fd241a

clarify

cb030b2

fix

3a13661

texastony reviewed Oct 3, 2023

View reviewed changes

Lucas McDonald and others added 13 commits October 3, 2023 11:20

catch more exceptions

23ae9f3

changes

795c148

refactor

5c5b04a

fix

ca6acb0

fix

d105232

clean externs

7bec002

fix

8e49dcb

update gitignore

a5d1a6d

fix

41e7e81

todos

34ea223

Merge branch 'main-1.x' into lucmcdon/python-poc

bc67cd4

fix

a361478

Merge branch 'lucmcdon/python-poc' of github.com:smithy-lang/smithy-d…

959bb0a

…afny into lucmcdon/python-poc

Lucas McDonald added 4 commits October 9, 2023 14:13

beta codegen for recursive structures via explicit conversion functions

99a2074

fixed circular dependency on dafny_to_smithy

847a792

non-service codegen

2c29c19

fix unions

471bea1

lucasmcdonald3 and others added 28 commits April 2, 2024 17:02

fix

1e82a3f

fix

4bc0584

fix

0445306

fix

0593eca

fix

02c26e3

fix

ff57913

add module

66836ce

settings

efc2281

rm gitmodules

d3fc5c8

rm

0552eeb

rm

ed4ce50

change

c438ce4

commit modules

de1e084

debug

9b0388f

debug

e55545f

wrap dep errors

f8c9b1f

wrap dep errors

9840d89

gen enum shapes

0767125

enum conversion

06f764b

fix

e2b9cea

fix

6a9596f

fix

d9e0b32

merge

8980c96

fix merge

b2e3c8a

update path

acd1957

fix

2ff0001

chore: add SimpleEnumV2 TestModel for Python (#346)

a2ad26a

* chore: add TestModel for SimpleEnumV2 in Python * chore: enable SimpleEnumV2 Python in CI

copyright

30ee7dd

lucasmcdonald3 closed this Jul 25, 2024

lucasmcdonald3 deleted the lucmcdon/python-poc branch August 27, 2024 20:23

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Python POC #282

Python POC #282

lucasmcdonald3 commented Aug 15, 2023 •

edited

Loading

robin-aws left a comment

texastony left a comment

texastony Sep 26, 2023

texastony Sep 26, 2023

texastony Oct 3, 2023

lucasmcdonald3 Oct 3, 2023 •

edited

Loading

texastony Oct 6, 2023

robin-aws Oct 6, 2023

texastony commented Oct 6, 2023

robin-aws commented Oct 6, 2023

lucasmcdonald3 commented Oct 9, 2023

Python POC #282

Python POC #282

Conversation

lucasmcdonald3 commented Aug 15, 2023 • edited Loading

Sub-PRs

Pending work

Build instructions

GHA Failures

Misc

robin-aws left a comment

Choose a reason for hiding this comment

texastony left a comment

Choose a reason for hiding this comment

texastony Sep 26, 2023

Choose a reason for hiding this comment

texastony Sep 26, 2023

Choose a reason for hiding this comment

texastony Oct 3, 2023

Choose a reason for hiding this comment

lucasmcdonald3 Oct 3, 2023 • edited Loading

Choose a reason for hiding this comment

texastony Oct 6, 2023

Choose a reason for hiding this comment

robin-aws Oct 6, 2023

Choose a reason for hiding this comment

texastony commented Oct 6, 2023

robin-aws commented Oct 6, 2023

lucasmcdonald3 commented Oct 9, 2023

lucasmcdonald3 commented Aug 15, 2023 •

edited

Loading

lucasmcdonald3 Oct 3, 2023 •

edited

Loading