From 959ad3dd23abf984b497eff43afefa39f73c7d56 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 5 Aug 2024 14:10:54 -0500 Subject: [PATCH 1/2] Fix: Support for double constant initialization in Dafny-to-Rust --- .../Backends/Rust/Dafny-compiler-rust.dfy | 5 ++--- Source/DafnyCore/GeneratedFromDafny/DCOMP.cs | 7 +++---- .../LitTests/LitTest/git-issues/git-issue-5642.dfy | 14 ++++++++++++++ .../LitTest/git-issues/git-issue-5642.dfy.expect | 2 ++ docs/dev/news/5642.fix | 1 + 5 files changed, 22 insertions(+), 7 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5642.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5642.dfy.expect create mode 100644 docs/dev/news/5642.fix diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy index 90f7a8dca0..a5b4ecf74b 100644 --- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy +++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy @@ -3361,9 +3361,8 @@ module {:extern "DCOMP"} DafnyToRustCompiler { rhs]); newEnv := newEnv.RemoveAssigned(isAssignedVar); } else { - error := Some("Unespected field to assign whose isAssignedVar is not in the environment: " + isAssignedVar); - generated := - R.AssignMember(R.RawExpr(error.value), fieldName, rhs); + // Already assigned, safe to override + generated := R.Assign(Some(R.SelectMember(modify_macro.Apply1(thisInConstructor), fieldName)), rhs); } case _ => if onExpr != R.Identifier("self") { diff --git a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs index b1c10c2461..4bc89968ae 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs @@ -2834,8 +2834,7 @@ public void GenAssignLhs(DAST._IAssignLhs lhs, RAST._IExpr rhs, DCOMP._ISelfInfo generated = (((RAST.__default.dafny__runtime).MSel((this).update__field__uninit__macro)).AsExpr()).Apply(Dafny.Sequence.FromElements((this).thisInConstructor, RAST.Expr.create_Identifier(_4_fieldName), RAST.Expr.create_Identifier(_8_isAssignedVar), rhs)); newEnv = (newEnv).RemoveAssigned(_8_isAssignedVar); } else { - (this).error = Std.Wrappers.Option>.create_Some(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("Unespected field to assign whose isAssignedVar is not in the environment: "), _8_isAssignedVar)); - generated = RAST.__default.AssignMember(RAST.Expr.create_RawExpr((this.error).dtor_value), _4_fieldName, rhs); + generated = RAST.Expr.create_Assign(Std.Wrappers.Option.create_Some(RAST.AssignLhs.create_SelectMember(((this).modify__macro).Apply1((this).thisInConstructor), _4_fieldName)), rhs); } goto after_match1; } @@ -5670,7 +5669,7 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv goto after__ASSIGN_SUCH_THAT_0; } } - throw new System.Exception("assign-such-that search produced no value (line 4736)"); + throw new System.Exception("assign-such-that search produced no value (line 4735)"); after__ASSIGN_SUCH_THAT_0: ; _63_allReadCloned = Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(_63_allReadCloned, Dafny.Sequence.UnicodeFromString("let ")), _64_next), Dafny.Sequence.UnicodeFromString(" = ")), _64_next), Dafny.Sequence.UnicodeFromString(".clone();\n")); _62_recIdents = Dafny.Set>.Difference(_62_recIdents, Dafny.Set>.FromElements(_64_next)); @@ -7026,7 +7025,7 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv goto after__ASSIGN_SUCH_THAT_1; } } - throw new System.Exception("assign-such-that search produced no value (line 5272)"); + throw new System.Exception("assign-such-that search produced no value (line 5271)"); after__ASSIGN_SUCH_THAT_1: ; if ((!object.Equals(selfIdent, DCOMP.SelfInfo.create_NoSelf())) && ((_310_next).Equals(Dafny.Sequence.UnicodeFromString("_this")))) { RAST._IExpr _311_selfCloned; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5642.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5642.dfy new file mode 100644 index 0000000000..55b40c2bba --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5642.dfy @@ -0,0 +1,14 @@ +// RUN: %testDafnyForEachCompiler "%s" + +class Cl { + const c: bool + constructor(c: bool) { + this.c := c; + this.c := c; + } +} + +method Main() { + var cl := new Cl(false); + print cl.c, "\n"; +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5642.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5642.dfy.expect new file mode 100644 index 0000000000..bacc454b89 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5642.dfy.expect @@ -0,0 +1,2 @@ + +false diff --git a/docs/dev/news/5642.fix b/docs/dev/news/5642.fix new file mode 100644 index 0000000000..b8dbeb1f2a --- /dev/null +++ b/docs/dev/news/5642.fix @@ -0,0 +1 @@ +Support for double constant initialization in Dafny-to-Rust \ No newline at end of file From a59357b69e8d33284852bc4491ed1d6b54029df3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Thu, 8 Aug 2024 07:48:06 -0500 Subject: [PATCH 2/2] Update git-issue-5642.dfy.expect --- .../LitTests/LitTest/git-issues/git-issue-5642.dfy.expect | 1 - 1 file changed, 1 deletion(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5642.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5642.dfy.expect index bacc454b89..c508d5366f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5642.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5642.dfy.expect @@ -1,2 +1 @@ - false