Skip to content

Commit

Permalink
fix: Include arguments to Go external constructor (dafny-lang#5813)
Browse files Browse the repository at this point in the history
### Description
The Go backend was not passing arguments when invoking an `{:extern}`
constructor.

### How has this been tested?
Enabled Go in the existing `ExternCtors.dfy` test case, and refactored
it to not require support for classes with both Dafny- and
extern-implemented declarations (which is a separate feature).

<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>

Co-authored-by: Remy Willems <rwillems@amazon.com>
  • Loading branch information
robin-aws and keyboardDrummer authored Oct 9, 2024
1 parent cb5666e commit 37d3ff7
Show file tree
Hide file tree
Showing 6 changed files with 13 additions and 18 deletions.
3 changes: 3 additions & 0 deletions Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
Original file line number Diff line number Diff line change
Expand Up @@ -2236,8 +2236,11 @@ protected override void EmitNew(Type type, IToken tok, CallStmt initCall /*?*/,
if (cl is TraitDecl { IsObjectTrait: true }) {
wr.Write("_dafny.New_Object()");
} else {
var ctor = (Constructor)initCall?.Method; // correctness of cast follows from precondition of "EmitNew"
var sep = "";
wr.Write("{0}(", TypeName_Initializer(type, wr, tok));
EmitTypeDescriptorsActuals(TypeArgumentInstantiation.ListFromClass(cl, type.TypeArgs), tok, wr);
wr.Write(ConstructorArguments(initCall, wStmts, ctor, sep));
wr.Write(")");
}
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

import java.math.BigInteger;

public class Class extends _ExternBase_Class {
public class Class {
private final BigInteger n;

public Class(BigInteger n) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -17,12 +17,6 @@ func (obj *Class) Get() dafny.Int {
return obj.n
}

// have to implement this because the Go backend can't mix Dafny and Go code :-\

func (obj *Class) Print() {
fmt.Printf("My value is %d\n", obj.n)
}

type CompanionStruct_Class_ struct{}
var Companion_Class_ = CompanionStruct_Class_{}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,3 @@ def SayHi():

def Get(self):
return self.n

def Print(self):
_dafny.print(_dafny.string_of(_dafny.Seq("My value is ")))
_dafny.print(_dafny.string_of((self).Get()))
_dafny.print(_dafny.string_of(_dafny.Seq("\n")))
Original file line number Diff line number Diff line change
@@ -1,24 +1,23 @@
// RUN: %run --target cs "%s" --input %S/ExternCtors-externs/Library.cs > "%t"
// RUN: %run --target java "%s" --input %S/ExternCtors-externs/Class.java >> "%t"
// RUN: %run --target py "%s" --input %S/ExternCtors-externs/Library.py >> "%t"
// RUN: %run --target go "%s" --input %S/ExternCtors-externs/Library.go >> "%t"
// RUN: %diff "%s.expect" "%t"

// FIXME: Extern constructors are currently broken in Go and JavaScript,
// so they are omitted
// FIXME: Extern constructors are currently broken in JavaScript,
// so that is omitted

method Main() {
Library.Class.SayHi();
var obj := new Library.Class(42);
obj.Print();
print "My value is ", obj.Get(), "\n";
}

module {:extern "Library"} Library {
class {:extern} Class {
constructor {:extern} (n: int)
static method {:extern} SayHi()
function {:extern} Get() : int
method Print() {
print "My value is ", Get(), "\n";
}
}
}

Original file line number Diff line number Diff line change
Expand Up @@ -10,3 +10,7 @@ My value is 42
Dafny program verifier finished with 1 verified, 0 errors
Hello!
My value is 42

Dafny program verifier finished with 1 verified, 0 errors
Hello!
My value is 42

0 comments on commit 37d3ff7

Please sign in to comment.