I am trying to do a simple UDP networking example in Dafny by calling System.Net.Sockets.UdpClient in C# externally. I've defined :extern classes and methods in Dafny that I've implemented in a C# file that calls UdpClient to send packets. However, I am facing the following issue, in that the Dafny compiler complains that it cannot find UdpClient, among other things, in the System.Net namespace.
Here is the code that I am using, which is based on an old version of Ironfleet.
Io.dfy
include "NativeTypes.dfy"
module{:extern "NativeIO"} NativeIO {
import opened NativeTypes
class OkState
{
constructor{:axiom} () requires false
function{:axiom} ok():bool reads this
}
class HostEnvironment
{
ghost var ok:OkState
constructor{:axiom} () requires false
predicate Valid()
reads this
{
true
}
}
datatype EndPoint = EndPoint(addr:seq<byte>, port:uint16)
class{:extern "IPEndPoint"} IPEndPoint
{
ghost var env:HostEnvironment
function{:extern} Address():seq<byte> reads this
function{:extern} Port():uint16 reads this
constructor{:extern} () requires false
method{:extern} GetAddress() returns(addr:array<byte>)
ensures fresh(addr)
ensures addr[..] == Address()
ensures addr.Length == 4 // Encoding current IPv4 assumption
method{:axiom} GetPort() returns (port: uint16)
ensures port == Port()
static method{:axiom} Construct(ipAddress:array<byte>, port:uint16, ghost env:HostEnvironment) returns(ok:bool, ep:IPEndPoint)
requires env.Valid()
modifies env.ok
ensures env.ok.ok() == ok
ensures ok ==> fresh(ep) && ep.env == env && ep.Address() == ipAddress[..] && ep.Port() == port
static method{:extern} DnsResolve(name:seq<uint16>) returns (resolved_name:seq<uint16>)
}
function MaxPacketSize() : int { 0xFFFF_FFFF_FFFF_FFFF }
class{:extern "UdpClient"} UdpClient
{
ghost var env:HostEnvironment
function{:axiom} LocalEndPoint():EndPoint reads this
function{:axiom} IsOpen():bool reads this
constructor{:axiom} () requires false
static method{:axiom} Construct(localEP:IPEndPoint, ghost env:HostEnvironment) returns(ok:bool, udp:UdpClient?)
method{:axiom} Close() returns(ok:bool)
method{:axiom} Receive(timeLimit:int32) returns(ok:bool, timedOut:bool, remote:IPEndPoint, buffer:array<byte>)
method{:axiom} Send(remote:IPEndPoint, buffer:array<byte>) returns(ok:bool)
}
}
IoNative.cs
using System;
using System.Net.Sockets;
using System.Numerics;
using System.Diagnostics;
using System.Threading;
using System.Collections.Concurrent;
using System.Collections.Generic;
using UClient = System.Net.Sockets.UdpClient;
using IEndPoint = System.Net.IPEndPoint;
namespace NativeIO {
public partial class HostConstants
{
public static uint NumCommandLineArgs()
{
return (uint)System.Environment.GetCommandLineArgs().Length;
}
public static ushort[] GetCommandLineArg(ulong i)
{
return Array.ConvertAll(System.Environment.GetCommandLineArgs()[i].ToCharArray(), c => (ushort)c);
}
}
public partial class IPEndPoint
{
internal IEndPoint endpoint;
internal IPEndPoint(IEndPoint endpoint) { this.endpoint = endpoint; }
public byte[] GetAddress()
{
// no exceptions thrown:
return (byte[])(endpoint.Address.GetAddressBytes().Clone());
}
public ushort GetPort()
{
// no exceptions thrown:
return (ushort)endpoint.Port;
}
public static void Construct(byte[] ipAddress, ushort port, out bool ok, out IPEndPoint? endpoint)
{
try
{
ipAddress = (byte[])(ipAddress.Clone());
endpoint = new IPEndPoint(new IEndPoint(new System.Net.IPAddress(ipAddress), port));
ok = true;
}
catch (Exception e)
{
System.Console.Error.WriteLine(e);
endpoint = null;
ok = false;
}
}
// DnsResolve is a Dafny function, which must be deterministic, so remember lookup results
private static System.Collections.Generic.Dictionary<string, string> dns =
new System.Collections.Generic.Dictionary<string, string>();
public static Dafny.ISequence<ushort> DnsResolve(Dafny.ISequence<ushort> name)
{
var str_name = new String(Array.ConvertAll(name.Elements, c => (char)c));
try
{
if (dns.ContainsKey(str_name))
{
return Dafny.Sequence<ushort>.FromArray(Array.ConvertAll(dns[str_name].ToCharArray(), c => (ushort)c));
}
foreach (var addr in System.Net.Dns.GetHostEntry(str_name).AddressList)
{
if (addr.AddressFamily == AddressFamily.InterNetwork)
{
dns.Add(str_name, addr.ToString());
return Dafny.Sequence<ushort>.FromArray(Array.ConvertAll(addr.ToString().ToCharArray(), c => (ushort)c));
}
}
}
catch (Exception e)
{
System.Console.Error.WriteLine("Error: DNS lookup failed for " + str_name);
System.Console.Error.WriteLine(e);
dns.Add(str_name, str_name);
return name;
}
System.Console.Error.WriteLine("Error: could not find IPv4 address for " + str_name);
dns.Add(str_name, str_name);
return name;
}
}
public struct Packet {
public IEndPoint ep;
public byte[] buffer;
}
public partial class UdpClient
{
internal UClient client;
internal Thread sender;
internal Thread receiver;
internal ConcurrentQueue<Packet> send_queue;
internal ConcurrentQueue<Packet> receive_queue;
internal UdpClient(UClient client) {
this.client = client;
this.send_queue = new ConcurrentQueue<Packet>();
this.receive_queue = new ConcurrentQueue<Packet>();
this.sender = new Thread(SendLoop);
this.sender.Start();
this.receiver = new Thread(ReceiveLoop);
this.receiver.Start();
}
private static bool ShouldIgnoreException(Exception e)
{
if (e is SocketException se) {
if (se.ErrorCode == 10054 /* WSAECONNRESET */) {
return true;
}
}
return false;
}
public static void Construct(IPEndPoint localEP, out bool ok, out UdpClient? udp)
{
try
{
udp = new UdpClient(new UClient(localEP.endpoint));
udp.client.Client.ReceiveBufferSize = 8192 * 100;
ok = true;
}
catch (Exception e)
{
System.Console.Error.WriteLine(e);
udp = null;
ok = false;
}
}
public void Close(out bool ok)
{
try
{
client.Close();
ok = true;
}
catch (Exception e)
{
if (ShouldIgnoreException(e)) {
ok = true;
}
else {
System.Console.Error.WriteLine(e);
ok = false;
}
}
}
public void Receive(int timeLimit, out bool ok, out bool timedOut, out IPEndPoint? remote, out byte[]? buffer)
{
buffer = null;
remote = null;
try
{
Packet packet;
bool dequeued = this.receive_queue.TryDequeue(out packet);
if (!dequeued) {
if (timeLimit == 0) {
ok = true;
timedOut = true;
return;
} else {
System.Console.Out.WriteLine("Going to sleep unexpectedly!");
Thread.Sleep(timeLimit); // REVIEW: This is very conservative, but shouldn't matter, since we don't use this path
Receive(0, out ok, out timedOut, out remote, out buffer);
}
} else {
// System.Console.Out.WriteLine("Dequeued a packet from: " + packet.ep.Address + " port " + packet.ep.Port);
timedOut = false;
remote = new IPEndPoint(packet.ep);
buffer = new byte[packet.buffer.Length];
Array.Copy(packet.buffer, buffer, packet.buffer.Length);
ok = true;
}
}
catch (Exception e)
{
if (ShouldIgnoreException(e)) {
ok = true;
timedOut = true;
}
else {
System.Console.Error.WriteLine(e);
timedOut = false;
ok = false;
}
}
}
public void ReceiveLoop() {
while (true) {
try {
Packet packet = new Packet();
packet.buffer = client.Receive(ref packet.ep);
this.receive_queue.Enqueue(packet);
//System.Console.Out.WriteLine("Enqueued a packet from: " + packet.ep.Address);
} catch (Exception e) {
if (!ShouldIgnoreException(e)) {
System.Console.Error.WriteLine(e);
}
}
}
}
public void SendLoop() {
while (true) {
try {
Packet packet;
bool dequeued = this.send_queue.TryDequeue(out packet);
if (dequeued) {
int nSent = client.Send(packet.buffer, packet.buffer.Length, packet.ep);
if (nSent != packet.buffer.Length) {
//throw new Exception("only sent " + nSent + " of " + packet.buffer.Length + " bytes");
System.Console.Error.Write("only sent " + nSent + " of " + packet.buffer.Length + " bytes");
}
}
} catch (Exception e) {
if (!ShouldIgnoreException(e)) {
System.Console.Error.WriteLine(e);
}
}
}
}
public bool Send(IPEndPoint remote, byte[] buffer)
{
Packet p = new Packet();
p.ep = remote.endpoint;
p.buffer = new byte[buffer.Length];
Array.Copy(buffer, p.buffer, buffer.Length);
this.send_queue.Enqueue(p);
return true; // ok
}
}
}
IoTest.dfy (main function)
include "Io.dfy"
module Main {
import opened NativeIO
import opened NativeTypes
method {:main} Main(ghost env: HostEnvironment)
requires env.ok.ok()
modifies env.ok
{
var ipAddress := new byte[4];
ipAddress[0] := 0x7F;
ipAddress[1] := 0x00;
ipAddress[2] := 0x00;
ipAddress[3] := 0x01;
var ok, localEndpoint := IPEndPoint.Construct(ipAddress, 5000, env);
var client: UdpClient?;
ok, client := UdpClient.Construct(localEndpoint, env);
var port := localEndpoint.GetPort();
print port, "\n";
}
}
And here is the output I get when I try to compile IoTest.cs and IoNative.cs together using the Dafny compiler.
$ dafny IoTest.dfy IoNative.cs
Dafny program verifier finished with 2 verified, 0 errors
Wrote textual form of target program to IoTest.cs
Errors compiling program into IoTest
(8,28): error CS0234: The type or namespace name 'Sockets' does not exist in the namespace 'System.Net' (are you missing an assembly reference?)
(9,30): error CS0234: The type or namespace name 'IPEndPoint' does not exist in the namespace 'System.Net' (are you missing an assembly reference?)
(2,18): error CS0234: The type or namespace name 'Sockets' does not exist in the namespace 'System.Net' (are you missing an assembly reference?)
(120,16): error CS0246: The type or namespace name 'SocketException' could not be found (are you missing a using directive or an assembly reference?)
(49,68): error CS0234: The type or namespace name 'IPAddress' does not exist in the namespace 'System.Net' (are you missing an assembly reference?)
(73,34): error CS0234: The type or namespace name 'Dns' does not exist in the namespace 'System.Net' (are you missing an assembly reference?)
(75,43): error CS0103: The name 'AddressFamily' does not exist in the current context
I know that these do indeed exist in the System.Net namespace in my .NET installation, because when I compile and run the C# file alone with dotnet, it works. What might be causing this discrepancy between the Dafny compiler and the dotnet compiler?