feat(core): UDP sockets in the simulation core
engine.ts ports the UDP part of Swift's "UDP sockets and Router RIP": a socket bound to a given port or to a free one drawn from 49152–65534 with Java's random numbers on Swift's seed; sending, also as a limited broadcast on every interface (or the bound one) with TTL 1; delivery into the queue of every socket on the destination port, which then answers to the last sender; receiving, with a timeout that advances the virtual clock; closing. Stopping forgets sockets and queues. RIP stays not ported; Swift's DHCP handling of a datagram has nothing to do until DHCP is in the snapshot. The oracle gets the steps bindUdp, sendUdp, receiveUdp and closeSocket on both sides and reports the sockets. Two new scenarios — a LAN, and two networks through a router with a UDP firewall rule and a broadcast that does not cross it — match the Swift engine trace for trace, the random ports included. Swift's four UDP engine tests are ported, with a test for stopping. 11 mutation probes were all caught (one only after the stop test was added). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This commit is contained in:
@@ -80,6 +80,9 @@
|
||||
"packet" : 7,
|
||||
"type" : "delivered"
|
||||
}
|
||||
],
|
||||
"sockets" : [
|
||||
|
||||
],
|
||||
"switchTables" : {
|
||||
"00000000-0000-0000-0000-000000000405" : {
|
||||
|
||||
@@ -151,6 +151,9 @@
|
||||
"type" : "delivered"
|
||||
},
|
||||
"02:00:00:00:02:22"
|
||||
],
|
||||
"sockets" : [
|
||||
|
||||
],
|
||||
"switchTables" : {
|
||||
|
||||
|
||||
@@ -204,6 +204,9 @@
|
||||
"packet" : 13,
|
||||
"type" : "delivered"
|
||||
}
|
||||
],
|
||||
"sockets" : [
|
||||
|
||||
],
|
||||
"switchTables" : {
|
||||
|
||||
|
||||
@@ -795,6 +795,9 @@
|
||||
"packet" : 3,
|
||||
"type" : "delivered"
|
||||
}
|
||||
],
|
||||
"sockets" : [
|
||||
|
||||
],
|
||||
"switchTables" : {
|
||||
"00000000-0000-0000-0000-000000000503" : {
|
||||
|
||||
@@ -99,6 +99,9 @@
|
||||
"packet" : 12,
|
||||
"type" : "delivered"
|
||||
}
|
||||
],
|
||||
"sockets" : [
|
||||
|
||||
],
|
||||
"switchTables" : {
|
||||
"00000000-0000-0000-0000-000000000104" : {
|
||||
|
||||
@@ -0,0 +1,209 @@
|
||||
{
|
||||
"seed": 21,
|
||||
"nodes": [
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-000000000101",
|
||||
"kind": "pc",
|
||||
"ports": [
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-000000000111",
|
||||
"label": "eth0"
|
||||
}
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-000000000102",
|
||||
"kind": "pc",
|
||||
"ports": [
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-000000000112",
|
||||
"label": "eth0"
|
||||
}
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-000000000103",
|
||||
"kind": "pc",
|
||||
"ports": [
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-000000000113",
|
||||
"label": "eth0"
|
||||
}
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-000000000104",
|
||||
"kind": "networkSwitch",
|
||||
"ports": [
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-000000000121",
|
||||
"label": "sw1"
|
||||
},
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-000000000122",
|
||||
"label": "sw2"
|
||||
},
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-000000000123",
|
||||
"label": "sw3"
|
||||
},
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-000000000124",
|
||||
"label": "sw4"
|
||||
}
|
||||
]
|
||||
}
|
||||
],
|
||||
"links": [
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-00000000F001",
|
||||
"sourceNode": "00000000-0000-0000-0000-000000000101",
|
||||
"sourcePort": "00000000-0000-0000-0000-000000000111",
|
||||
"targetNode": "00000000-0000-0000-0000-000000000104",
|
||||
"targetPort": "00000000-0000-0000-0000-000000000121"
|
||||
},
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-00000000F002",
|
||||
"sourceNode": "00000000-0000-0000-0000-000000000102",
|
||||
"sourcePort": "00000000-0000-0000-0000-000000000112",
|
||||
"targetNode": "00000000-0000-0000-0000-000000000104",
|
||||
"targetPort": "00000000-0000-0000-0000-000000000122"
|
||||
},
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-00000000F003",
|
||||
"sourceNode": "00000000-0000-0000-0000-000000000103",
|
||||
"sourcePort": "00000000-0000-0000-0000-000000000113",
|
||||
"targetNode": "00000000-0000-0000-0000-000000000104",
|
||||
"targetPort": "00000000-0000-0000-0000-000000000123"
|
||||
}
|
||||
],
|
||||
"devices": {
|
||||
"00000000-0000-0000-0000-000000000101": {
|
||||
"ip": "192.168.0.10",
|
||||
"mask": "255.255.255.0"
|
||||
},
|
||||
"00000000-0000-0000-0000-000000000102": {
|
||||
"ip": "192.168.0.20",
|
||||
"mask": "255.255.255.0"
|
||||
},
|
||||
"00000000-0000-0000-0000-000000000103": {
|
||||
"ip": "192.168.0.30",
|
||||
"mask": "255.255.255.0"
|
||||
}
|
||||
},
|
||||
"switches": {
|
||||
"00000000-0000-0000-0000-000000000104": {
|
||||
"ssid": "lab",
|
||||
"retention": 5000
|
||||
}
|
||||
},
|
||||
"steps": [
|
||||
{
|
||||
"op": "bindUdp",
|
||||
"node": "00000000-0000-0000-0000-000000000101",
|
||||
"port": 5000
|
||||
},
|
||||
{
|
||||
"op": "bindUdp",
|
||||
"node": "00000000-0000-0000-0000-000000000102"
|
||||
},
|
||||
{
|
||||
"op": "bindUdp",
|
||||
"node": "00000000-0000-0000-0000-000000000101",
|
||||
"port": 5000
|
||||
},
|
||||
{
|
||||
"op": "bindUdp",
|
||||
"node": "00000000-0000-0000-0000-000000000101",
|
||||
"localIp": "10.9.9.9"
|
||||
},
|
||||
{
|
||||
"op": "bindUdp",
|
||||
"node": "00000000-0000-0000-0000-000000000103",
|
||||
"port": 7000,
|
||||
"localIp": "192.168.0.30"
|
||||
},
|
||||
{
|
||||
"op": "sendUdp",
|
||||
"socket": "00000000-0000-0000-0000-000000000002",
|
||||
"target": "192.168.0.10",
|
||||
"port": 5000,
|
||||
"payload": "hallo"
|
||||
},
|
||||
{
|
||||
"op": "receiveUdp",
|
||||
"socket": "00000000-0000-0000-0000-000000000001"
|
||||
},
|
||||
{
|
||||
"op": "receiveUdp",
|
||||
"socket": "00000000-0000-0000-0000-000000000001",
|
||||
"timeout": 200
|
||||
},
|
||||
{
|
||||
"op": "sendUdp",
|
||||
"socket": "00000000-0000-0000-0000-000000000001",
|
||||
"payload": "antwort"
|
||||
},
|
||||
{
|
||||
"op": "receiveUdp",
|
||||
"socket": "00000000-0000-0000-0000-000000000002",
|
||||
"timeout": 200
|
||||
},
|
||||
{
|
||||
"op": "receiveUdp",
|
||||
"socket": "00000000-0000-0000-0000-000000000002"
|
||||
},
|
||||
{
|
||||
"op": "receiveUdp",
|
||||
"socket": "00000000-0000-0000-0000-000000000002",
|
||||
"timeout": 500
|
||||
},
|
||||
{
|
||||
"op": "sendUdp",
|
||||
"socket": "00000000-0000-0000-0000-000000000002",
|
||||
"target": "192.168.0.30",
|
||||
"port": 6000,
|
||||
"payload": "niemand"
|
||||
},
|
||||
{
|
||||
"op": "advance",
|
||||
"to": 2000
|
||||
},
|
||||
{
|
||||
"op": "sendUdp",
|
||||
"socket": "00000000-0000-0000-0000-000000000003",
|
||||
"target": "255.255.255.255",
|
||||
"port": 5000,
|
||||
"payload": "an alle"
|
||||
},
|
||||
{
|
||||
"op": "advance",
|
||||
"to": 3000
|
||||
},
|
||||
{
|
||||
"op": "receiveUdp",
|
||||
"socket": "00000000-0000-0000-0000-000000000001"
|
||||
},
|
||||
{
|
||||
"op": "sendUdp",
|
||||
"socket": "00000000-0000-0000-0000-000000000003",
|
||||
"payload": "ohne Ziel"
|
||||
},
|
||||
{
|
||||
"op": "closeSocket",
|
||||
"socket": "00000000-0000-0000-0000-000000000001"
|
||||
},
|
||||
{
|
||||
"op": "sendUdp",
|
||||
"socket": "00000000-0000-0000-0000-000000000001",
|
||||
"target": "192.168.0.20",
|
||||
"port": 5000,
|
||||
"payload": "geschlossen"
|
||||
},
|
||||
{
|
||||
"op": "bindUdp",
|
||||
"node": "00000000-0000-0000-0000-000000000101",
|
||||
"port": 5000
|
||||
}
|
||||
]
|
||||
}
|
||||
File diff suppressed because it is too large
Load Diff
@@ -0,0 +1,171 @@
|
||||
{
|
||||
"seed": 22,
|
||||
"nodes": [
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-000000000201",
|
||||
"kind": "pc",
|
||||
"ports": [
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-000000000211",
|
||||
"label": "eth0"
|
||||
}
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-000000000202",
|
||||
"kind": "router",
|
||||
"ports": [
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-000000000221",
|
||||
"label": "rt1"
|
||||
},
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-000000000222",
|
||||
"label": "rt2"
|
||||
}
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-000000000203",
|
||||
"kind": "pc",
|
||||
"ports": [
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-000000000213",
|
||||
"label": "eth0"
|
||||
}
|
||||
]
|
||||
}
|
||||
],
|
||||
"links": [
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-00000000F004",
|
||||
"sourceNode": "00000000-0000-0000-0000-000000000201",
|
||||
"sourcePort": "00000000-0000-0000-0000-000000000211",
|
||||
"targetNode": "00000000-0000-0000-0000-000000000202",
|
||||
"targetPort": "00000000-0000-0000-0000-000000000221"
|
||||
},
|
||||
{
|
||||
"id": "00000000-0000-0000-0000-00000000F005",
|
||||
"sourceNode": "00000000-0000-0000-0000-000000000202",
|
||||
"sourcePort": "00000000-0000-0000-0000-000000000222",
|
||||
"targetNode": "00000000-0000-0000-0000-000000000203",
|
||||
"targetPort": "00000000-0000-0000-0000-000000000213"
|
||||
}
|
||||
],
|
||||
"devices": {
|
||||
"00000000-0000-0000-0000-000000000201": {
|
||||
"ip": "10.0.0.2",
|
||||
"mask": "255.255.255.0",
|
||||
"gateway": "10.0.0.1"
|
||||
},
|
||||
"00000000-0000-0000-0000-000000000202": {
|
||||
"ip": "10.0.0.1",
|
||||
"mask": "255.255.255.0"
|
||||
},
|
||||
"00000000-0000-0000-0000-000000000203": {
|
||||
"ip": "20.0.0.2",
|
||||
"mask": "255.255.255.0",
|
||||
"gateway": "20.0.0.1"
|
||||
}
|
||||
},
|
||||
"interfaces": [
|
||||
{
|
||||
"node": "00000000-0000-0000-0000-000000000202",
|
||||
"port": "00000000-0000-0000-0000-000000000221",
|
||||
"ip": "10.0.0.1",
|
||||
"mask": "255.255.255.0"
|
||||
},
|
||||
{
|
||||
"node": "00000000-0000-0000-0000-000000000202",
|
||||
"port": "00000000-0000-0000-0000-000000000222",
|
||||
"ip": "20.0.0.1",
|
||||
"mask": "255.255.255.0"
|
||||
}
|
||||
],
|
||||
"steps": [
|
||||
{
|
||||
"op": "bindUdp",
|
||||
"node": "00000000-0000-0000-0000-000000000203",
|
||||
"port": 5000
|
||||
},
|
||||
{
|
||||
"op": "bindUdp",
|
||||
"node": "00000000-0000-0000-0000-000000000203",
|
||||
"port": 5001
|
||||
},
|
||||
{
|
||||
"op": "bindUdp",
|
||||
"node": "00000000-0000-0000-0000-000000000201"
|
||||
},
|
||||
{
|
||||
"op": "bindUdp",
|
||||
"node": "00000000-0000-0000-0000-000000000202",
|
||||
"port": 5000
|
||||
},
|
||||
{
|
||||
"op": "sendUdp",
|
||||
"socket": "00000000-0000-0000-0000-000000000003",
|
||||
"target": "20.0.0.2",
|
||||
"port": 5000,
|
||||
"payload": "durch den Router"
|
||||
},
|
||||
{
|
||||
"op": "receiveUdp",
|
||||
"socket": "00000000-0000-0000-0000-000000000001",
|
||||
"timeout": 500
|
||||
},
|
||||
{
|
||||
"op": "sendUdp",
|
||||
"socket": "00000000-0000-0000-0000-000000000003",
|
||||
"target": "20.0.0.2",
|
||||
"port": 5001,
|
||||
"payload": "verboten"
|
||||
},
|
||||
{
|
||||
"op": "receiveUdp",
|
||||
"socket": "00000000-0000-0000-0000-000000000002",
|
||||
"timeout": 500
|
||||
},
|
||||
{
|
||||
"op": "sendUdp",
|
||||
"socket": "00000000-0000-0000-0000-000000000003",
|
||||
"target": "255.255.255.255",
|
||||
"port": 5000,
|
||||
"payload": "Broadcast"
|
||||
},
|
||||
{
|
||||
"op": "receiveUdp",
|
||||
"socket": "00000000-0000-0000-0000-000000000004",
|
||||
"timeout": 500
|
||||
},
|
||||
{
|
||||
"op": "receiveUdp",
|
||||
"socket": "00000000-0000-0000-0000-000000000001",
|
||||
"timeout": 500
|
||||
},
|
||||
{
|
||||
"op": "sendUdp",
|
||||
"socket": "00000000-0000-0000-0000-000000000001",
|
||||
"payload": "zurueck"
|
||||
},
|
||||
{
|
||||
"op": "receiveUdp",
|
||||
"socket": "00000000-0000-0000-0000-000000000003",
|
||||
"timeout": 500
|
||||
}
|
||||
],
|
||||
"firewalls": {
|
||||
"00000000-0000-0000-0000-000000000202": {
|
||||
"active": true,
|
||||
"defaultPolicy": "accept",
|
||||
"filterUdp": true,
|
||||
"rules": [
|
||||
{
|
||||
"protocol": "udp",
|
||||
"port": 5001,
|
||||
"action": "drop"
|
||||
}
|
||||
]
|
||||
}
|
||||
}
|
||||
}
|
||||
File diff suppressed because it is too large
Load Diff
Reference in New Issue
Block a user