Skip to content

Commit 779d38d

Browse files
robin-awsrobin-aws
authored
fix: Misc Rust bug fixes, mostly around @positional (#581)
1 parent 3e098eb commit 779d38d

File tree

3 files changed

+61
-67
lines changed

3 files changed

+61
-67
lines changed

‎codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/AbstractRustShimGenerator.java

Lines changed: 13 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -14,9 +14,11 @@
1414
import java.util.Set;
1515
import java.util.stream.Collectors;
1616
import java.util.stream.Stream;
17+
import software.amazon.polymorph.smithydafny.DafnyNameResolver;
1718
import software.amazon.polymorph.traits.DafnyUtf8BytesTrait;
1819
import software.amazon.polymorph.traits.PositionalTrait;
1920
import software.amazon.polymorph.traits.ReferenceTrait;
21+
import software.amazon.polymorph.utils.DafnyNameResolverHelpers;
2022
import software.amazon.polymorph.utils.IOUtils;
2123
import software.amazon.polymorph.utils.MapUtils;
2224
import software.amazon.polymorph.utils.ModelUtils;
@@ -505,14 +507,19 @@ protected TokenTree fromDafny(
505507
}
506508
}
507509
case INTEGER -> {
508-
if (isRustOption) {
510+
if (isDafnyOption) {
509511
yield TokenTree.of(
510512
"crate::standard_library_conversions::oint_from_dafny(%s.clone())".formatted(
511513
dafnyValue
512514
)
513515
);
514516
} else {
515-
yield TokenTree.of(dafnyValue, ".clone()");
517+
TokenTree result = TokenTree.of(dafnyValue, ".clone()");
518+
if (isRustOption) {
519+
result =
520+
TokenTree.of(TokenTree.of("Some("), result, TokenTree.of(")"));
521+
}
522+
yield result;
516523
}
517524
}
518525
case LONG -> {
@@ -908,23 +915,17 @@ protected RustFile enumConversionModule(final EnumShape enumShape) {
908915
protected HashMap<String, String> serviceVariables() {
909916
final HashMap<String, String> variables = new HashMap<>();
910917
variables.put("serviceName", service.getId().getName(service));
911-
variables.put("dafnyModuleName", getDafnyModuleName());
912918
variables.put("dafnyInternalModuleName", getDafnyInternalModuleName());
913919
variables.put("dafnyTypesModuleName", getDafnyTypesModuleName());
914920
variables.put("rustTypesModuleName", getRustTypesModuleName());
915921
return variables;
916922
}
917923

918-
protected String getDafnyModuleName() {
919-
return service
920-
.getId()
921-
.getNamespace()
922-
.replace(".", "::")
923-
.toLowerCase(Locale.ROOT);
924-
}
925-
926924
protected String getDafnyInternalModuleName() {
927-
return "%s::internaldafny".formatted(getDafnyModuleName());
925+
String dafnyExternName = DafnyNameResolver.dafnyExternNamespace(
926+
service.getId().getNamespace()
927+
);
928+
return dafnyExternName.replace(".", "::").toLowerCase(Locale.ROOT);
928929
}
929930

930931
protected String getDafnyTypesModuleName() {

‎codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/RustAwsSdkShimGenerator.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -511,8 +511,8 @@ pub fn to_dafny(
511511
}
512512

513513
@Override
514-
protected String getDafnyModuleName() {
515-
return "software::amazon::cryptography::services::%s".formatted(
514+
protected String getDafnyInternalModuleName() {
515+
return "software::amazon::cryptography::services::%s::internaldafny".formatted(
516516
getSdkId().toLowerCase()
517517
);
518518
}

‎codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/RustLibraryShimGenerator.java

Lines changed: 46 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -657,7 +657,7 @@ private RustFile operationOuterModule(final OperationShape operationShape) {
657657
StructureShape outputShape = operationIndex
658658
.getOutputShape(operationShape)
659659
.get();
660-
if (inputShape.hasTrait(PositionalTrait.class)) {
660+
if (outputShape.hasTrait(PositionalTrait.class)) {
661661
variables.put(
662662
"outputFromDafny",
663663
fromDafny(outputShape, "inner_result.value()", false, false)
@@ -1175,7 +1175,7 @@ protected Set<RustFile> operationConversionModules(
11751175
operationName(operationShape)
11761176
);
11771177

1178-
Optional<StructureShape> inputStructure = operationIndex.getOutputShape(
1178+
Optional<StructureShape> inputStructure = operationIndex.getInputShape(
11791179
operationShape
11801180
);
11811181
final boolean hasInputStructure =
@@ -1307,7 +1307,6 @@ private TokenTree operationStructureFromDafnyFunction(
13071307
structureId,
13081308
StructureShape.class
13091309
);
1310-
final boolean isPositional = structureShape.hasTrait(PositionalTrait.class);
13111310
final Map<String, String> variables = MapUtils.merge(
13121311
serviceVariables(),
13131312
operationVariables(operationShape),
@@ -1318,46 +1317,24 @@ private TokenTree operationStructureFromDafnyFunction(
13181317
fluentMemberSettersForStructure(structureShape).toString()
13191318
);
13201319

1321-
if (isPositional) {
1322-
return TokenTree.of(
1323-
evalTemplate(
1324-
"""
1325-
#[allow(dead_code)]
1326-
pub fn from_dafny(
1327-
dafny_value: ::std::rc::Rc<
1328-
crate::r#$dafnyTypesModuleName:L::$structureName:L,
1329-
>,
1330-
) -> crate::operation::$snakeCaseOperationName:L::$rustStructureName:L {
1331-
crate::operation::$snakeCaseOperationName:L::$rustStructureName:L::builder()
1332-
$fluentMemberSetters:L
1333-
.build()
1334-
.unwrap()
1335-
}
1336-
""",
1337-
variables
1338-
)
1339-
);
1340-
} else {
1341-
// unwrap() is safe as long as the builder is infallible
1342-
return TokenTree.of(
1343-
evalTemplate(
1344-
"""
1345-
#[allow(dead_code)]
1346-
pub fn from_dafny(
1347-
dafny_value: ::std::rc::Rc<
1348-
crate::r#$dafnyTypesModuleName:L::$structureName:L,
1349-
>,
1350-
) -> crate::operation::$snakeCaseOperationName:L::$rustStructureName:L {
1351-
crate::operation::$snakeCaseOperationName:L::$rustStructureName:L::builder()
1352-
$fluentMemberSetters:L
1353-
.build()
1354-
.unwrap()
1355-
}
1356-
""",
1357-
variables
1358-
)
1359-
);
1360-
}
1320+
return TokenTree.of(
1321+
evalTemplate(
1322+
"""
1323+
#[allow(dead_code)]
1324+
pub fn from_dafny(
1325+
dafny_value: ::std::rc::Rc<
1326+
crate::r#$dafnyTypesModuleName:L::$structureName:L,
1327+
>,
1328+
) -> crate::operation::$snakeCaseOperationName:L::$rustStructureName:L {
1329+
crate::operation::$snakeCaseOperationName:L::$rustStructureName:L::builder()
1330+
$fluentMemberSetters:L
1331+
.build()
1332+
.unwrap()
1333+
}
1334+
""",
1335+
variables
1336+
)
1337+
);
13611338
}
13621339

13631340
private RustFile wrappedModule() {
@@ -1434,7 +1411,7 @@ private String wrappedClientOperationImpl(
14341411
StructureShape outputShape = operationIndex
14351412
.getOutputShape(operationShape)
14361413
.get();
1437-
if (inputShape.hasTrait(PositionalTrait.class)) {
1414+
if (outputShape.hasTrait(PositionalTrait.class)) {
14381415
variables.put(
14391416
"outputToDafny",
14401417
toDafny(outputShape, "inner_result", false, false).toString()
@@ -1641,14 +1618,26 @@ protected TokenTree toDafny(
16411618
}
16421619
}
16431620
case BOOLEAN -> {
1644-
if (isRustOption) {
1645-
yield TokenTree.of(
1646-
"crate::standard_library_conversions::obool_to_dafny(&%s)".formatted(
1647-
rustValue
1648-
)
1649-
);
1621+
if (isDafnyOption) {
1622+
if (isRustOption) {
1623+
yield TokenTree.of(
1624+
"crate::standard_library_conversions::obool_to_dafny(&%s)".formatted(
1625+
rustValue
1626+
)
1627+
);
1628+
} else {
1629+
yield TokenTree.of(
1630+
"crate::standard_library_conversions::obool_to_dafny(Some(%s))".formatted(
1631+
rustValue
1632+
)
1633+
);
1634+
}
16501635
} else {
1651-
yield TokenTree.of("%s.clone()".formatted(rustValue));
1636+
if (isRustOption) {
1637+
yield TokenTree.of("%s.clone().unwrap()".formatted(rustValue));
1638+
} else {
1639+
yield TokenTree.of("%s.clone()".formatted(rustValue));
1640+
}
16521641
}
16531642
}
16541643
case INTEGER -> {
@@ -1667,7 +1656,11 @@ protected TokenTree toDafny(
16671656
);
16681657
}
16691658
} else {
1670-
yield TokenTree.of("%s.clone()".formatted(rustValue));
1659+
if (isRustOption) {
1660+
yield TokenTree.of("%s.clone().unwrap()".formatted(rustValue));
1661+
} else {
1662+
yield TokenTree.of("%s.clone()".formatted(rustValue));
1663+
}
16711664
}
16721665
}
16731666
case LONG -> {
@@ -1830,7 +1823,7 @@ protected TokenTree toDafny(
18301823
if (isRustOption) {
18311824
yield TokenTree.of(
18321825
"""
1833-
%s::conversions::%s::to_dafny(&%s.clone().unwrap())
1826+
%s::conversions::%s::to_dafny(%s.clone().unwrap())
18341827
""".formatted(prefix, structureShapeName, rustValue)
18351828
);
18361829
} else {

0 commit comments

Comments
 (0)