Skip to content

Commit

Permalink
Fix Rust compilation errors for unused types and constant fields (daf…
Browse files Browse the repository at this point in the history 
…ny-lang#4450)

Fix Rust compilation errors for unused types and constant fields


Also fixes runtime crashes due to a buggy transmute for tuples.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT

license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

---
Stack created with [Sapling](https://sapling-scm.com). Best reviewed
with [ReviewStack](https://reviewstack.dev/dafny-lang/dafny/pull/4450).
* dafny-lang#4452
* __->__ dafny-lang#4450
  • Loading branch information
@shadaj @keyboardDrummer
shadaj authored and keyboardDrummer committed Sep 15, 2023
1 parent 3921ca2 commit dc9533d
Show file tree
Hide file tree
Showing 4 changed files with 6,036 additions and 5,918 deletions.
30 changes: 30 additions & 0 deletions Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -152,6 +152,10 @@ protected override IClassWriter CreateClass(string moduleName, string name, bool
if (currentBuilder is ClassContainer builder) {
List<DAST.Type> typeParams = new();
foreach (var tp in typeParameters) {
if (tp.Variance == TypeParameter.TPVariance.Contra) {
throw new NotImplementedException("Contravariance in type parameters");
}

typeParams.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence<Rune>.UnicodeFromString(IdProtect(tp.GetCompileName(Options)))));
}

Expand Down Expand Up @@ -183,6 +187,10 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT
if (currentBuilder is DatatypeContainer builder) {
List<DAST.Type> typeParams = new();
foreach (var tp in dt.TypeArgs) {
if (tp.Variance == TypeParameter.TPVariance.Contra) {
throw new NotImplementedException("Contravariance in type parameters");
}

typeParams.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence<Rune>.UnicodeFromString(IdProtect(tp.GetCompileName(Options)))));
}

Expand Down Expand Up @@ -295,6 +303,10 @@ protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree

List<DAST.Type> typeParams = new();
foreach (var tp in sst.TypeArgs) {
if (tp.Variance == TypeParameter.TPVariance.Contra) {
throw new NotImplementedException("Contravariance in type parameters");
}

typeParams.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence<Rune>.UnicodeFromString(tp.Name)));
}

Expand Down Expand Up @@ -325,6 +337,10 @@ public ConcreteSyntaxTree CreateMethod(Method m, List<TypeArgumentInstantiation>
List<DAST.Type> astTypeArgs = new();
if (m.IsStatic) {
foreach (var typeArg in typeArgs) {
if (typeArg.Formal.Variance == TypeParameter.TPVariance.Contra) {
throw new NotImplementedException("Contravariance in type parameters");
}

astTypeArgs.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence<Rune>.UnicodeFromString(compiler.IdProtect(typeArg.Formal.GetCompileName(compiler.Options)))));
}
}
Expand Down Expand Up @@ -372,6 +388,10 @@ public ConcreteSyntaxTree CreateFunction(string name, List<TypeArgumentInstantia
bool forBodyInheritance, bool lookasideBody) {
List<DAST.Type> astTypeArgs = new();
foreach (var typeArg in typeArgs) {
if (typeArg.Formal.Variance == TypeParameter.TPVariance.Contra) {
throw new NotImplementedException("Contravariance in type parameters");
}

astTypeArgs.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence<Rune>.UnicodeFromString(compiler.IdProtect(typeArg.Formal.GetCompileName(compiler.Options)))));
}

Expand Down Expand Up @@ -1310,6 +1330,16 @@ member.EnclosingClass is DatatypeDecl
member.IsStatic,
expectedType.AsArrowType.Arity
), null);
} else if (internalAccess && (member is ConstantField || member.EnclosingClass is TraitDecl)) {
return new ExprLvalue((DAST.Expression)DAST.Expression.create_Select(
objExpr,
Sequence<Rune>.UnicodeFromString("_" + member.GetCompileName(Options)),
false,
member.EnclosingClass is DatatypeDecl
), (DAST.AssignLhs)DAST.AssignLhs.create_Select(
objExpr,
Sequence<Rune>.UnicodeFromString("_" + member.GetCompileName(Options))
));
} else {
return new ExprLvalue((DAST.Expression)DAST.Expression.create_Select(
objExpr,
Expand Down
42 changes: 40 additions & 2 deletions Source/DafnyCore/Compilers/Rust/Dafny-compiler-rust.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,16 @@ module {:extern "DCOMP"} DCOMP {
fieldI := fieldI + 1;
}

s := "#[derive(Default)]\npub struct r#" + c.name + typeParams + " {\n" + fields + "\n}";
var typeParamI := 0;
while typeParamI < |c.typeParams| {
var tpeGen := GenType(c.typeParams[typeParamI], false, false);
fields := fields + "_phantom_type_param_" + natToString(typeParamI) + ": ::std::marker::PhantomData<" + tpeGen + ">,\n";
fieldInits := fieldInits + "_phantom_type_param_" + natToString(typeParamI) + ": ::std::marker::PhantomData,\n";

typeParamI := typeParamI + 1;
}

s := "pub struct r#" + c.name + typeParams + " {\n" + fields + "\n}";

var implBody, traitBodies := GenClassImplBody(c.body, false, Type.Path([], [], ResolvedType.Datatype(path)), {});
implBody := "pub fn new() -> Self {\n" + "r#" + c.name + " {\n" + fieldInits + "\n}\n}\n" + implBody;
Expand Down Expand Up @@ -118,6 +127,12 @@ module {:extern "DCOMP"} DCOMP {
}
}

var defaultImpl := "impl " + constrainedTypeParams + " ::std::default::Default for r#" + c.name + typeParams + " {\n";
defaultImpl := defaultImpl + "fn default() -> Self {\n";
defaultImpl := defaultImpl + "r#" + c.name + "::new()\n";
defaultImpl := defaultImpl + "}\n";
defaultImpl := defaultImpl + "}\n";

var printImpl := "impl " + constrainedTypeParams + " ::dafny_runtime::DafnyPrint for r#" + c.name + typeParams + " {\n" + "fn fmt_print(&self, __fmt_print_formatter: &mut ::std::fmt::Formatter, _in_seq: bool) -> std::fmt::Result {\n";
printImpl := printImpl + "write!(__fmt_print_formatter, \"r#" + c.name + "(" + (if |c.fields| > 0 then "" else ")") + "\")?;";
var i := 0;
Expand All @@ -136,7 +151,7 @@ module {:extern "DCOMP"} DCOMP {
ptrPartialEqImpl := ptrPartialEqImpl + "::std::ptr::eq(self, other)";
ptrPartialEqImpl := ptrPartialEqImpl + "\n}\n}\n";

s := s + "\n" + printImpl + "\n" + ptrPartialEqImpl;
s := s + "\n" + defaultImpl + "\n" + printImpl + "\n" + ptrPartialEqImpl;
}

static method GenTrait(t: Trait, containingPath: seq<Ident>) returns (s: string) {
Expand Down Expand Up @@ -284,6 +299,10 @@ module {:extern "DCOMP"} DCOMP {
k := k + 1;
}

if |c.typeParams| > 0 {
methodBody := methodBody + "r#" + c.name + "::_PhantomVariant(..) => panic!(),\n";
}

methodBody := methodBody + "}\n";

implBody := implBody + "pub fn r#" + formal.name + "(&self) -> &" + formalType + " {\n" + methodBody + "}\n";
Expand All @@ -294,6 +313,21 @@ module {:extern "DCOMP"} DCOMP {
i := i + 1;
}

if |c.typeParams| > 0 {
ctors := ctors + "_PhantomVariant(";
var typeI := 0;
while typeI < |c.typeParams| {
if typeI > 0 {
ctors := ctors + ", ";
}

var genTp := GenType(c.typeParams[typeI], false, false);
ctors := ctors + "::std::marker::PhantomData::<" + genTp + ">";
typeI := typeI + 1;
}
ctors := ctors + ")";
}

var enumBody := "#[derive(PartialEq)]\npub enum r#" + c.name + typeParams + " {\n" + ctors + "\n}" + "\n" + "impl " + constrainedTypeParams + " r#" + c.name + typeParams + " {\n" + implBody + "\n}";

var identEraseImpls := "impl " + constrainedTypeParams + " ::dafny_runtime::DafnyErasable for r#" + c.name + typeParams + " {\n" + "type Erased = Self;\nfn erase(&self) -> &Self::Erased { self }\nfn erase_owned(self) -> Self::Erased { self }}\n";
Expand Down Expand Up @@ -333,6 +367,10 @@ module {:extern "DCOMP"} DCOMP {
i := i + 1;
}

if |c.typeParams| > 0 {
printImpl := printImpl + "r#" + c.name + "::_PhantomVariant(..) => {panic!()\n}\n";
}

printImpl := printImpl + "}\n}\n}\n";

var defaultImpl := "";
Expand Down
Loading

0 comments on commit dc9533d

Please sign in to comment.