From eca25793f0b9c95b06754781b3f227d500d3d730 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Sat, 8 Aug 2026 18:21:56 +0200 Subject: [PATCH 1/3] add more nil pres --- pkg/slayers/scmp_msg_spec.gobra | 1 + router/dataplane.go | 9 +++++++++ router/svc.go | 3 +++ 3 files changed, 13 insertions(+) diff --git a/pkg/slayers/scmp_msg_spec.gobra b/pkg/slayers/scmp_msg_spec.gobra index f4cd61b64..31b42cdaf 100644 --- a/pkg/slayers/scmp_msg_spec.gobra +++ b/pkg/slayers/scmp_msg_spec.gobra @@ -190,6 +190,7 @@ pred (s *SCMPDestinationUnreachable) NonInitMem() { } pred (s *SCMPDestinationUnreachable) Mem(ub []byte) { + s != nil && s.BaseLayer.Mem(ub, 4) } diff --git a/router/dataplane.go b/router/dataplane.go index 7803ba3c7..d7537b034 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -270,6 +270,7 @@ func (e scmpError) Error() string { } // SetIA sets the local IA for the dataplane. +// @ requires d != nil // @ requires acc(d.Mem(), OutMutexPerm) // @ requires !d.IsRunning() // @ requires d.LocalIA().IsZero() @@ -307,6 +308,7 @@ func (d *DataPlane) SetIA(ia addr.IA) (e error) { // SetKey sets the key used for MAC verification. The key provided here should // already be derived as in scrypto.HFMacFactory. +// @ requires d != nil // @ requires acc(d.Mem(), OutMutexPerm) // @ requires !d.IsRunning() // @ requires !d.KeyIsSet() @@ -371,6 +373,7 @@ func (d *DataPlane) SetKey(key []byte) (res error) { // send/receive traffic in the local AS. This can only be called once; future // calls will return an error. This can only be called on a not yet running // dataplane. +// @ requires d != nil // @ requires acc(d.Mem(), OutMutexPerm) // @ requires !d.IsRunning() // @ requires !d.InternalConnIsSet() @@ -416,6 +419,7 @@ func (d *DataPlane) AddInternalInterface(conn BatchConn, ip net.IP) error { // AddExternalInterface adds the inter AS connection for the given interface ID. // If a connection for the given ID is already set this method will return an // error. This can only be called on a not yet running dataplane. +// @ requires d != nil // @ requires conn != nil && conn.Mem() // @ preserves acc(d.Mem(), OutMutexPerm) // @ preserves !d.IsRunning() @@ -464,6 +468,7 @@ func (d *DataPlane) AddExternalInterface(ifID uint16, conn BatchConn) error { // AddNeighborIA adds the neighboring IA for a given interface ID. If an IA for // the given ID is already set, this method will return an error. This can only // be called on a yet running dataplane. +// @ requires d != nil // @ requires !remote.IsZero() // @ preserves acc(d.Mem(), OutMutexPerm) // @ preserves !d.IsRunning() @@ -630,6 +635,7 @@ func (d *DataPlane) addBFDController(ifID uint16, s *bfdSend, cfg control.BFD, // AddSvc adds the address for the given service. This can be called multiple // times for the same service, with the address added to the list of addresses // that provide the service. +// @ requires d != nil // @ requires a != nil && acc(a.Mem(), R10) // @ preserves acc(d.Mem(), OutMutexPerm) // @ preserves !d.IsRunning() @@ -691,6 +697,7 @@ func (d *DataPlane) AddSvc(svc addr.HostSVC, a *net.UDPAddr) error { // absence of race conditions. To specify that the router is not running, // we need to pass perms to d.Mem(), but if we do this, then we don't need // the lock invariant to perform the operations in this function. +// @ requires d != nil // @ requires a != nil && acc(a.Mem(), R10) // @ preserves acc(d.Mem(), OutMutexPerm/2) // @ preserves d.mtx.LockP() @@ -724,6 +731,7 @@ func (d *DataPlane) DelSvc(svc addr.HostSVC, a *net.UDPAddr) error { // AddNextHop sets the next hop address for the given interface ID. If the // interface ID already has an address associated this operation fails. This can // only be called on a not yet running dataplane. +// @ requires d != nil // @ requires a != nil && a.Mem() // @ preserves acc(d.Mem(), OutMutexPerm) // @ preserves !d.IsRunning() @@ -816,6 +824,7 @@ func (d *DataPlane) AddNextHopBFD(ifID uint16, src, dst *net.UDPAddr, cfg contro // @ requires d.mtx.LockInv() == MutexInvariant{d} // @ requires ctx != nil && ctx.Mem() // contracts for IO-spec +// @ requires d != nil // @ requires dp.Valid() // @ requires d.DpAgreesWithSpec(dp) // @ requires io.token(place) && dp.dp3s_iospec_ordered(state, place) diff --git a/router/svc.go b/router/svc.go index 0f4ea92be..77ef31f9d 100644 --- a/router/svc.go +++ b/router/svc.go @@ -40,6 +40,7 @@ func newServices() (s *services) { return tmp } +// @ requires s != nil // @ preserves acc(s.Mem(), R50) // @ requires acc(a.Mem(), R10) // @ decreases 0 if sync.IgnoreBlockingForTermination() @@ -68,6 +69,7 @@ func (s *services) AddSvc(svc addr.HostSVC, a *net.UDPAddr) { //@ fold acc(s.Mem(), R50) } +// @ requires s != nil // @ preserves acc(s.Mem(), R50) // @ preserves acc(a.Mem(), R10) // @ decreases 0 if sync.IgnoreBlockingForTermination() @@ -101,6 +103,7 @@ func (s *services) DelSvc(svc addr.HostSVC, a *net.UDPAddr) { //@ fold acc(s.Mem(), R50) } +// @ requires s != nil // @ requires acc(s.Mem(), _) // @ ensures !b ==> r == nil // @ ensures b ==> acc(r.Mem(), _) From a957cdc76b80f4283679dc3e0d57d73ef0503c28 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Sun, 9 Aug 2026 16:40:08 +0200 Subject: [PATCH 2/3] Apply suggestion from @jcp19 --- router/dataplane.go | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/router/dataplane.go b/router/dataplane.go index d7537b034..05594cc87 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -270,7 +270,7 @@ func (e scmpError) Error() string { } // SetIA sets the local IA for the dataplane. -// @ requires d != nil +// @ requires d != nil // @ requires acc(d.Mem(), OutMutexPerm) // @ requires !d.IsRunning() // @ requires d.LocalIA().IsZero() From f8ac95d2563042afcfb8f5d3180965ec42225213 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 4 Sep 2026 21:37:49 +0200 Subject: [PATCH 3/3] Apply batched suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: João Pereira --- router/dataplane.go | 14 +++++++------- router/svc.go | 4 ++-- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index 79f48a703..f912d8f1a 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -308,7 +308,7 @@ func (d *DataPlane) SetIA(ia addr.IA) (e error) { // SetKey sets the key used for MAC verification. The key provided here should // already be derived as in scrypto.HFMacFactory. -// @ requires d != nil +// @ requires d != nil // @ requires acc(d.Mem(), OutMutexPerm) // @ requires !d.IsRunning() // @ requires !d.KeyIsSet() @@ -373,7 +373,7 @@ func (d *DataPlane) SetKey(key []byte) (res error) { // send/receive traffic in the local AS. This can only be called once; future // calls will return an error. This can only be called on a not yet running // dataplane. -// @ requires d != nil +// @ requires d != nil // @ requires acc(d.Mem(), OutMutexPerm) // @ requires !d.IsRunning() // @ requires !d.InternalConnIsSet() @@ -419,7 +419,7 @@ func (d *DataPlane) AddInternalInterface(conn BatchConn, ip net.IP) error { // AddExternalInterface adds the inter AS connection for the given interface ID. // If a connection for the given ID is already set this method will return an // error. This can only be called on a not yet running dataplane. -// @ requires d != nil +// @ requires d != nil // @ requires conn != nil && conn.Mem() // @ preserves acc(d.Mem(), OutMutexPerm) // @ preserves !d.IsRunning() @@ -468,7 +468,7 @@ func (d *DataPlane) AddExternalInterface(ifID uint16, conn BatchConn) error { // AddNeighborIA adds the neighboring IA for a given interface ID. If an IA for // the given ID is already set, this method will return an error. This can only // be called on a yet running dataplane. -// @ requires d != nil +// @ requires d != nil // @ requires !remote.IsZero() // @ preserves acc(d.Mem(), OutMutexPerm) // @ preserves !d.IsRunning() @@ -635,7 +635,7 @@ func (d *DataPlane) addBFDController(ifID uint16, s *bfdSend, cfg control.BFD, // AddSvc adds the address for the given service. This can be called multiple // times for the same service, with the address added to the list of addresses // that provide the service. -// @ requires d != nil +// @ requires d != nil // @ requires a != nil && acc(a.Mem(), R10) // @ preserves acc(d.Mem(), OutMutexPerm) // @ preserves !d.IsRunning() @@ -697,7 +697,7 @@ func (d *DataPlane) AddSvc(svc addr.HostSVC, a *net.UDPAddr) error { // absence of race conditions. To specify that the router is not running, // we need to pass perms to d.Mem(), but if we do this, then we don't need // the lock invariant to perform the operations in this function. -// @ requires d != nil +// @ requires d != nil // @ requires a != nil && acc(a.Mem(), R10) // @ preserves acc(d.Mem(), OutMutexPerm/2) // @ preserves d.mtx.LockP() @@ -731,7 +731,7 @@ func (d *DataPlane) DelSvc(svc addr.HostSVC, a *net.UDPAddr) error { // AddNextHop sets the next hop address for the given interface ID. If the // interface ID already has an address associated this operation fails. This can // only be called on a not yet running dataplane. -// @ requires d != nil +// @ requires d != nil // @ requires a != nil && a.Mem() // @ preserves acc(d.Mem(), OutMutexPerm) // @ preserves !d.IsRunning() diff --git a/router/svc.go b/router/svc.go index 77ef31f9d..70c1455dd 100644 --- a/router/svc.go +++ b/router/svc.go @@ -40,7 +40,7 @@ func newServices() (s *services) { return tmp } -// @ requires s != nil +// @ requires s != nil // @ preserves acc(s.Mem(), R50) // @ requires acc(a.Mem(), R10) // @ decreases 0 if sync.IgnoreBlockingForTermination() @@ -69,7 +69,7 @@ func (s *services) AddSvc(svc addr.HostSVC, a *net.UDPAddr) { //@ fold acc(s.Mem(), R50) } -// @ requires s != nil +// @ requires s != nil // @ preserves acc(s.Mem(), R50) // @ preserves acc(a.Mem(), R10) // @ decreases 0 if sync.IgnoreBlockingForTermination()