fix!: Disable automatically mapping a Dafny string to a Go string in externs

Source/DafnyCore/Compilers/GoLang/Compiler-go.cs

@@ -1402,9 +1402,7 @@ protected class ClassWriter : IClassWriter {
  Contract.Assume(type != null); // precondition; this ought to be declared as a Requires in the superclass
 
  var xType = DatatypeWrapperEraser.SimplifyType(type);
- if (xType is SpecialNativeType snt) {
- return snt.Name;
- } else if (xType is BoolType) {
+ if (xType is BoolType) {
  return "bool";
  } else if (xType is CharType) {
  return CharTypeName;
@@ -1675,21 +1673,6 @@ protected class ClassWriter : IClassWriter {
  return Capitalize(formal.CompileName);
  }
 
- protected override Type NativeForm(Type type) {
- if (type.IsStringType) {
- return NativeStringType;
- } else {
- return type;
- }
- }
-
- /// A type which is rendered to Go exactly as specified. Used to represent the native string type.
- private class SpecialNativeType : UserDefinedType {
- internal SpecialNativeType(string name) : base(Token.NoToken, name, null) { }
- }
-
- private readonly static SpecialNativeType NativeStringType = new SpecialNativeType("string");
-
  // ----- Declarations -------------------------------------------------------------
 
  protected void DeclareField(string name, bool isExtern, bool isStatic, bool isConst, Type type, IToken tok, string/*?*/ rhs, string className, ConcreteSyntaxTree wr, ConcreteSyntaxTree initWriter, ConcreteSyntaxTree concreteMethodWriter) {
@@ -3609,32 +3592,6 @@ private class SpecialNativeType : UserDefinedType {
  }
  }
 
- protected override ConcreteSyntaxTree EmitCoercionToNativeForm(Type from, IToken tok, ConcreteSyntaxTree wr) {
- // Don't expand! We want to distinguish string from seq<char> here
- from = from.Normalize();
- if (from is UserDefinedType udt && udt.Name == "string") {
- wr.Write('(');
- var w = wr.Fork();
- wr.Write(").String()");
- return w;
- } else {
- return wr;
- }
- }
-
- protected override ConcreteSyntaxTree EmitCoercionFromNativeForm(Type to, IToken tok, ConcreteSyntaxTree wr) {
- // Don't expand! We want to distinguish string from seq<char> here
- to = to.Normalize();
- if (to is UserDefinedType udt && udt.Name == "string") {
- wr.Write($"{HelperModulePrefix}SeqOfString(");
- var w = wr.Fork();
- wr.Write(")");
- return w;
- } else {
- return wr;
- }
- }
-
  protected override ConcreteSyntaxTree EmitCoercionToNativeInt(ConcreteSyntaxTree wr) {
  var w = wr.Fork();
  wr.Write(".(int)");

Source/DafnyCore/Compilers/SinglePassCompiler.cs

@@ -827,12 +827,6 @@ protected interface IClassWriter {
  return wr;
  }
 
- protected virtual ConcreteSyntaxTree EmitCoercionToNativeForm(Type/*?*/ from, IToken tok, ConcreteSyntaxTree wr) {
- return wr;
- }
- protected virtual ConcreteSyntaxTree EmitCoercionFromNativeForm(Type/*?*/ to, IToken tok, ConcreteSyntaxTree wr) {
- return wr;
- }
  protected virtual ConcreteSyntaxTree EmitCoercionToNativeInt(ConcreteSyntaxTree wr) {
  return wr;
  }
@@ -4457,9 +4451,6 @@ private class ArrayLvalueImpl : ILvalue {
  } else {
  type = instantiatedType;
  }
- if (s.Method.IsExtern(out _, out _)) {
- type = NativeForm(type);
- }
  outTypes.Add(type);
  outFormalTypes.Add(p.Type);
  outLhsTypes.Add(s.Lhs[i].Type);
@@ -4519,12 +4510,8 @@ private class ArrayLvalueImpl : ILvalue {
  var fromType = s.Args[i].Type;
  var toType = s.Method.Ins[i].Type;
  var instantiatedToType = toType.Subst(s.MethodSelect.TypeArgumentSubstitutionsWithParents());
- // Order of coercions is important here: EmitCoercionToNativeForm may coerce into a type we're unaware of, so it *has* to be last
  var w = EmitCoercionIfNecessary(fromType, toType, s.Tok, wr);
  w = EmitDowncastIfNecessary(fromType, instantiatedToType, s.Tok, w);
- if (s.Method.IsExtern(out _, out _)) {
- w = EmitCoercionToNativeForm(toType, s.Tok, w);
- }
  TrExpr(s.Args[i], w, false, wStmts);
  sep = ", ";
  }
@@ -4553,9 +4540,6 @@ private class ArrayLvalueImpl : ILvalue {
  // The type information here takes care both of implicit upcasts and
  // implicit downcasts from type parameters (see above).
  ConcreteSyntaxTree wRhs = EmitAssignment(lvalue, s.Lhs[j].Type, outTypes[l], wr, s.Tok);
- if (s.Method.IsExtern(out _, out _)) {
- wRhs = EmitCoercionFromNativeForm(p.Type, s.Tok, wRhs);
- }
  wRhs.Write(outTmps[l]);
  // Coercion from the out type to the LHS type is the responsibility
  // of the EmitAssignment above

Test/git-issues/github-issue-2989.dfy

@@ -0,0 +1,17 @@
+// RUN: %translate go --unicode-char:false "%s" > "%t"
+// RUN: %translate go --unicode-char:true "%s" >> "%t"
+// RUN: %diff "%s.expect" "%t" 
+
+method Main() {
+ var s := Foo();
+}
+
+// An extern method that returned a string used to cause
+// an internal contract violation and nonsensical errors like
+// "Error: Cannot convert from string to seq<char>"
+
+method {:extern "foo"} Foo() returns (s: string)
+
+method Bar() returns (s: string) {
+ return "hello";
+}

Test/git-issues/github-issue-2989.dfy.expect

@@ -0,0 +1,4 @@
+
+Dafny program verifier finished with 2 verified, 0 errors
+
+Dafny program verifier finished with 2 verified, 0 errors

Test/wishlist/GoModule.dfy

@@ -0,0 +1,58 @@
+// RUN: %exits-with 3 %dafny /compile:3 /unicodeChar:0 /spillTargetCode:2 "%s" /compileTarget:go 2> "%t"
+// note: putting /compileTarget:go after "%s" overrides user-provided option
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK: GoModuleConversions.go:10:3: imported and not used: "net/url"
+
+// This test used to work only because of a questionable Go-only feature
+// of mapping a Dafny string directly to a Go string when passed in or out of
+// an extern method. It barely worked in one direction and not in the other
+// (see https://github.com/dafny-lang/dafny/issues/2989),
+// and even when it did, equating these two types was not actually sound in all cases anyway.
+// This feature has been disabled since Dafny 4.0,
+// and unfortunately I found that rewriting the test to work without it was very
+// difficult for unrelated reasons.
+// In particular this version should work but produces unused imports
+// which the Go compiler complains about
+// (see https://github.com/dafny-lang/dafny/issues/2953).
+// Instead I've converted this into a negative test.
+
+// "url" is a built-in package, so it should be accessible to the
+// test suite without further requirements on the setup.
+module {:extern "url", "net/url"} URL {
+
+ class URL {
+ var {:extern "Host"} host: string
+ var {:extern "Path"} pathname: string
+ var {:extern "RawQuery"} search: string
+ }
+
+ trait {:extern "", "error"} Error { }
+}
+
+module {:extern "GoModuleConversions"} GoModuleConversions {
+ import opened URL
+ method {:extern "ParseURL"} Parse(address: string) returns (url: URL, error: Error?)
+}
+
+module Test {
+
+ import GoModuleConversions
+
+ method TryUrl(address: string) {
+ var u, e := GoModuleConversions.Parse(address);
+ if (e != null) {
+ print "Parse error: ", e, "\n";
+ } else {
+ print "The address ", address, "\n";
+ print "has the following parts:\n";
+ print "host: ", u.host, "\n";
+ print "pathname: ", u.pathname, "\n";
+ print "search: ", u.search, "\n";
+ }
+ }
+
+ method Main() {
+ TryUrl("http:https://localhost:8080/default.htm?year=1915&month=august&day=29");
+ TryUrl("http:https://localhost:8080/default.htm%");
+ }
+}

Test/wishlist/GoModuleConversions.go

@@ -0,0 +1,11 @@
+package GoModuleConversions
+
+import (
+ "dafny"
+ url "net/url"
+)
+
+func ParseURL(dafnyAddress dafny.Sequence) (*url.URL, error) {
+ var address = dafny.SequenceVerbatimString(dafnyAddress, false);
+ return url.Parse(address)
+}