Skip to content

Commit

Permalink
fix a few errors due to the new encoding of socket
Browse files Browse the repository at this point in the history
  • Loading branch information
@jcp19
jcp19 committed Jan 18, 2024
1 parent d813aab commit 2a65c9d
Show file tree
Hide file tree
Showing 7 changed files with 308 additions and 114 deletions.
26 changes: 13 additions & 13 deletions private/underlay/conn/conn.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ type Conn interface {
//@ ensures err != nil ==> err.ErrorMem()
ReadFrom(b []byte) (n int, addr *net.UDPAddr, err error)
//@ requires acc(Mem(), _)
//@ preserves forall i int :: { &m[i] } 0 <= i && i < len(m) ==> m[i].Mem(1)
//@ preserves forall i int :: { &m[i] } 0 <= i && i < len(m) ==> m[i].Mem()
//@ ensures err == nil ==> 0 <= n && n <= len(m)
//@ ensures err != nil ==> err.ErrorMem()
ReadBatch(m Messages) (n int, err error)
Expand All @@ -67,7 +67,7 @@ type Conn interface {
//@ ensures err != nil ==> err.ErrorMem()
WriteTo(b []byte, u *net.UDPAddr) (n int, err error)
//@ requires acc(Mem(), _)
//@ preserves forall i int :: { &m[i] } 0 <= i && i < len(m) ==> acc(m[i].Mem(1), R10)
//@ preserves forall i int :: { &m[i] } 0 <= i && i < len(m) ==> acc(m[i].Mem(), R10)
//@ ensures err == nil ==> 0 <= n && n <= len(m)
//@ ensures err != nil ==> err.ErrorMem()
WriteBatch(m Messages, k int) (n int, err error)
Expand Down Expand Up @@ -164,24 +164,24 @@ func newConnUDPIPv4(listen, remote *net.UDPAddr, cfg *Config) (res *connUDPIPv4,
// ReadBatch reads up to len(msgs) packets, and stores them in msgs.
// It returns the number of packets read, and an error if any.
// @ requires acc(c.Mem(), _)
// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem(1)
// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem()
// @ ensures errRet == nil ==> 0 <= nRet && nRet <= len(msgs)
// @ ensures errRet != nil ==> errRet.ErrorMem()
func (c *connUDPIPv4) ReadBatch(msgs Messages) (nRet int, errRet error) {
//@ unfold acc(c.Mem(), _)
// (VerifiedSCION) 1 is the length of the buffers of the messages in msgs
n, err := c.pconn.ReadBatch(msgs, syscall.MSG_WAITFORONE /*@, 1 @*/)
n, err := c.pconn.ReadBatch(msgs, syscall.MSG_WAITFORONE)
return n, err
}

// @ requires acc(c.Mem(), _)
// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(msgs[i].Mem(1), R10)
// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(msgs[i].Mem(), R10)
// @ ensures err == nil ==> 0 <= n && n <= len(msgs)
// @ ensures err != nil ==> err.ErrorMem()
func (c *connUDPIPv4) WriteBatch(msgs Messages, flags int) (n int, err error) {
//@ unfold acc(c.Mem(), _)
// (VerifiedSCION) 1 is the length of the buffers of the messages in msgs
return c.pconn.WriteBatch(msgs, flags /*@, 1 @*/)
return c.pconn.WriteBatch(msgs, flags)
}

// SetReadDeadline sets the read deadline associated with the endpoint.
Expand Down Expand Up @@ -238,24 +238,24 @@ func newConnUDPIPv6(listen, remote *net.UDPAddr, cfg *Config) (res *connUDPIPv6,
// ReadBatch reads up to len(msgs) packets, and stores them in msgs.
// It returns the number of packets read, and an error if any.
// @ requires acc(c.Mem(), _)
// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem(1)
// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem()
// @ ensures errRet == nil ==> 0 <= nRet && nRet <= len(msgs)
// @ ensures errRet != nil ==> errRet.ErrorMem()
func (c *connUDPIPv6) ReadBatch(msgs Messages) (nRet int, errRet error) {
//@ unfold acc(c.Mem(), _)
// (VerifiedSCION) 1 is the length of the buffers of the messages in msgs
n, err := c.pconn.ReadBatch(msgs, syscall.MSG_WAITFORONE /*@, 1 @*/)
n, err := c.pconn.ReadBatch(msgs, syscall.MSG_WAITFORONE)
return n, err
}

// @ requires acc(c.Mem(), _)
// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(msgs[i].Mem(1), R10)
// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(msgs[i].Mem(), R10)
// @ ensures err == nil ==> 0 <= n && n <= len(msgs)
// @ ensures err != nil ==> err.ErrorMem()
func (c *connUDPIPv6) WriteBatch(msgs Messages, flags int) (n int, err error) {
//@ unfold acc(c.Mem(), _)
// (VerifiedSCION) 1 is the length of the buffers of the messages in msgs
return c.pconn.WriteBatch(msgs, flags /*@, 1 @*/)
return c.pconn.WriteBatch(msgs, flags)
}

// SetReadDeadline sets the read deadline associated with the endpoint.
Expand Down Expand Up @@ -463,11 +463,11 @@ func (c *connUDPBase) Close() (err error) {
// messages.
// @ requires 0 < n
// @ ensures len(res) == n
// @ ensures forall i int :: { &res[i] } 0 <= i && i < n ==> res[i].Mem(1)
// @ ensures forall i int :: { &res[i] } 0 <= i && i < n ==> res[i].Mem()
// @ decreases
func NewReadMessages(n int) (res Messages) {
m := make(Messages, n)
//@ invariant forall j int :: { &m[j] } (0 <= j && j < i0) ==> m[j].Mem(1)
//@ invariant forall j int :: { &m[j] } (0 <= j && j < i0) ==> m[j].Mem()
//@ invariant forall j int :: { &m[j] } (i0 <= j && j < len(m)) ==> acc(&m[j]) && m[j].N == 0
//@ invariant forall j int :: { m[j].Addr } (i0 <= j && j < len(m)) ==> m[j].Addr == nil
//@ invariant forall j int :: { m[j].OOB } (i0 <= j && j < len(m)) ==> m[j].OOB == nil
Expand All @@ -477,7 +477,7 @@ func NewReadMessages(n int) (res Messages) {
m[i].Buffers = make([][]byte, 1)
//@ fold slices.AbsSlice_Bytes(m[i].Buffers[0], 0, len(m[i].Buffers[0]))
//@ fold slices.AbsSlice_Bytes(m[i].OOB, 0, len(m[i].OOB))
//@ fold m[i].Mem(1)
//@ fold m[i].Mem()
}
return m
}
56 changes: 28 additions & 28 deletions router/dataplane.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -115,12 +115,12 @@ type BatchConn interface {

// @ requires acc(Mem(), _)
// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
// @ (msgs[i].Mem(1) && msgs[i].HasActiveBuffers(1))
// @ (msgs[i].Mem() && msgs[i].HasActiveBuffers())
// @ ensures err == nil ==> 0 <= n && n <= len(msgs)
// @ ensures err == nil ==>
// @ forall i int :: { &msgs[i] } 0 <= i && i < n ==> (
// @ typeOf(msgs[i].GetAddr(1)) == type[*net.UDPAddr] &&
// @ !msgs[i].HasWildcardPermAddr(1))
// @ typeOf(msgs[i].GetAddr()) == type[*net.UDPAddr] &&
// @ !msgs[i].HasWildcardPermAddr())
// @ ensures err == nil ==>
// @ forall i int :: { &msgs[i] } 0 <= i && i < n ==> msgs[i].GetN() <= len(msgs[i].GetFstBuffer())
// @ ensures err != nil ==> err.ErrorMem()
Expand All @@ -133,7 +133,7 @@ type BatchConn interface {
WriteTo(b []byte, addr *net.UDPAddr) (n int, err error)
// @ requires acc(Mem(), _)
// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
// @ (acc(msgs[i].Mem(1), R50) && msgs[i].HasActiveBuffers(1))
// @ (acc(msgs[i].Mem(), R50) && msgs[i].HasActiveBuffers())
// @ ensures err == nil ==> 0 <= n && n <= len(msgs)
// @ ensures err != nil ==> err.ErrorMem()
WriteBatch(msgs underlayconn.Messages, flags int) (n int, err error)
Expand Down Expand Up @@ -707,25 +707,25 @@ func (d *DataPlane) Run(ctx context.Context) error {
msgs := conn.NewReadMessages(inputBatchCnt)
// @ socketspec.SplitPermMsgs(msgs)

// @ requires forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(&msgs[i], 1/2) && msgs[i].MemWithoutHalf(1)
// @ ensures forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem(1) && msgs[i].HasActiveBuffers(1)
// @ requires forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(&msgs[i], 1/2) && msgs[i].MemWithoutHalf()
// @ ensures forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem() && msgs[i].HasActiveBuffers()
// @ decreases
// @ outline (
// @ invariant len(msgs) != 0 ==> 0 <= i0 && i0 <= len(msgs)
// @ invariant forall i int :: { &msgs[i] } 0 < len(msgs) ==> i0 <= i && i < len(msgs) ==> acc(&msgs[i], 1/2)
// @ invariant forall i int :: { &msgs[i] } 0 < len(msgs) ==> i0 <= i && i < len(msgs) ==> msgs[i].MemWithoutHalf(1)
// @ invariant forall i int :: { &msgs[i] } 0 < len(msgs) ==> 0 <= i && i < i0 ==> msgs[i].Mem(1)
// @ invariant forall i int :: { &msgs[i] } 0 < len(msgs) ==> i0 <= i && i < len(msgs) ==> msgs[i].MemWithoutHalf()
// @ invariant forall i int :: { &msgs[i] } 0 < len(msgs) ==> 0 <= i && i < i0 ==> msgs[i].Mem()
// @ decreases len(msgs) - i0
for _, msg := range msgs /*@ with i0 @*/ {
tmp := make([]byte, bufSize)
// @ assert forall i int :: { &tmp[i] } 0 <= i && i < len(tmp) ==> acc(&tmp[i])
// @ fold sl.AbsSlice_Bytes(tmp, 0, len(tmp))
// @ assert msgs[i0] === msg
// @ unfold msgs[i0].MemWithoutHalf(1)
// @ unfold msgs[i0].MemWithoutHalf()
msg.Buffers[0] = tmp
// @ fold msgs[i0].Mem(1)
// @ assert forall i int :: { &msgs[i] } 0 <= i && i < i0 ==> msgs[i].Mem(1)
// @ assert forall i int :: { &msgs[i] } i0 < i && i < len(msgs) ==> acc(&msgs[i], 1/2) && msgs[i].MemWithoutHalf(1)
// @ fold msgs[i0].Mem()
// @ assert forall i int :: { &msgs[i] } 0 <= i && i < i0 ==> msgs[i].Mem()
// @ assert forall i int :: { &msgs[i] } i0 < i && i < len(msgs) ==> acc(&msgs[i], 1/2) && msgs[i].MemWithoutHalf()
}
// @ )
// @ ensures writeMsgInv(writeMsgs)
Expand All @@ -743,7 +743,7 @@ func (d *DataPlane) Run(ctx context.Context) error {

// non-wildcard permissions:
// @ invariant acc(&scmpErr)
// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem(1)
// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem()
// @ invariant writeMsgInv(writeMsgs)
// wildcard permissions:
// @ invariant acc(&d, _)
Expand All @@ -758,12 +758,12 @@ func (d *DataPlane) Run(ctx context.Context) error {
// @ invariant unfolding acc(accBatchConn(d.external), _) in (ingressID in domain(d.external))
// @ invariant d.svc != nil
// properties about messages:
// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].HasActiveBuffers(1)
// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].HasActiveBuffers()
// properties about packetProcessor:
// @ invariant processor.sInit() && processor.sInitD() === d
for d.running {
pkts, err := rd.ReadBatch(msgs)
// @ assert forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem(1)
// @ assert forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem()
// @ assert err == nil ==>
// @ forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> msgs[i].GetN() <= len(msgs[i].GetFstBuffer())
if err != nil {
Expand All @@ -775,14 +775,14 @@ func (d *DataPlane) Run(ctx context.Context) error {
continue
}
// @ assert pkts <= len(msgs)
// @ assert forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> !msgs[i].HasWildcardPermAddr(1)
// @ assert forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> !msgs[i].HasWildcardPermAddr()
// @ assert forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> msgs[i].GetN() <= len(msgs[i].GetFstBuffer())

// (VerifiedSCION) using regular for loop instead of range loop to avoid unnecessary
// complications with permissions
// non-wildcard permissions:
// @ invariant acc(&scmpErr)
// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem(1)
// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem()
// @ invariant writeMsgInv(writeMsgs)
// wildcard permissions:
// @ invariant acc(&d, _)
Expand All @@ -793,10 +793,10 @@ func (d *DataPlane) Run(ctx context.Context) error {
// other properties:
// @ invariant pkts <= len(msgs)
// @ invariant 0 <= i0 && i0 <= pkts
// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].HasActiveBuffers(1)
// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].HasActiveBuffers()
// @ invariant forall i int :: { &msgs[i] } i0 <= i && i < pkts ==>
// @ !msgs[i].HasWildcardPermAddr(1)
// @ invariant forall i int :: { &msgs[i] } i0 <= i && i < pkts ==> typeOf(msgs[i].GetAddr(1)) == type[*net.UDPAddr]
// @ !msgs[i].HasWildcardPermAddr()
// @ invariant forall i int :: { &msgs[i] } i0 <= i && i < pkts ==> typeOf(msgs[i].GetAddr()) == type[*net.UDPAddr]
// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> msgs[i].GetN() <= len(msgs[i].GetFstBuffer())
// @ invariant d.forwardingMetrics != nil
// @ invariant ingressID in domain(d.forwardingMetrics)
Expand Down Expand Up @@ -824,7 +824,7 @@ func (d *DataPlane) Run(ctx context.Context) error {
inputCounters.InputBytesTotal.Add(float64(p.N))

srcAddr := p.Addr.(*net.UDPAddr)
// @ unfold msgs[:pkts][i0].Mem(1)
// @ unfold msgs[:pkts][i0].Mem()
// @ assert p.Buffers === msgs[:pkts][i0].Buffers
// @ assert acc(&p.Buffers[0])
// @ assert p.N <= len(p.Buffers[0])
Expand Down Expand Up @@ -866,7 +866,7 @@ func (d *DataPlane) Run(ctx context.Context) error {
// @ assert sl.AbsSlice_Bytes(m.OOB, 0, len(m.OOB))
// @ assert (m.Addr != nil ==> acc(m.Addr.Mem(), _))
// @ assert 0 <= m.N
// @ fold msgs[:pkts][i0].Mem(1)
// @ fold msgs[:pkts][i0].Mem()
// @ unfold scmpErr.Mem()
log.Debug("Error processing packet", "err", err)
// @ assert acc(inputCounters.DroppedPacketsTotal.Mem(), _)
Expand All @@ -876,7 +876,7 @@ func (d *DataPlane) Run(ctx context.Context) error {
}
if result.OutConn == nil { // e.g. BFD case no message is forwarded
// @ assume false
// @ fold msgs[:pkts][i0].Mem(1)
// @ fold msgs[:pkts][i0].Mem()
continue
}

Expand All @@ -887,20 +887,20 @@ func (d *DataPlane) Run(ctx context.Context) error {
writeMsgs[0].Buffers[0] = result.OutPkt
// @ assert acc(sl.AbsSlice_Bytes(writeMsgs[0].Buffers[0], 0, len(writeMsgs[0].Buffers[0])), 1 - R15)
// @ writeMsgs[0].WildcardPerm = !addrAliasesPkt
// TODO: writeMsgs[0].Mem(1) should be an invariant
// TODO: writeMsgs[0].Mem() should be an invariant
// @ writeMsgs[0].IsActive = true
writeMsgs[0].Addr = nil
if result.OutAddr != nil { // don't assign directly to net.Addr, typed nil!
writeMsgs[0].Addr = result.OutAddr
}
// @ assert acc(sl.AbsSlice_Bytes(writeMsgs[0].Buffers[0], 0, len(writeMsgs[0].Buffers[0])), 1 - R15)
// @ assume !addrAliasesPkt
// @ fold acc(writeMsgs[0].Mem(1), R50)
// @ fold acc(writeMsgs[0].Mem(), R50)
// @ assert forall i int :: { &writeMsgs[i] } 0 <= i && i < len(writeMsgs) ==>
// @ acc(writeMsgs[i].Mem(1), R50)
// @ acc(writeMsgs[i].Mem(), R50)
_, err = result.OutConn.WriteBatch(writeMsgs, syscall.MSG_DONTWAIT)
/// -- Checked until here // TODO: drop comment
// @ unfold acc(writeMsgs[0].Mem(1), R50)
// @ unfold acc(writeMsgs[0].Mem(), R50)
// @ ghost if addrAliasesPkt {
// @ apply acc(result.OutAddr.Mem(), R15) --* acc(sl.AbsSlice_Bytes(tmpBuf, 0, len(tmpBuf)), R15)
// assert sl.AbsSlice_Bytes(tmpBuf, 0, len(tmpBuf))
Expand All @@ -915,7 +915,7 @@ func (d *DataPlane) Run(ctx context.Context) error {
// @ assume false

// @ fold writeMsgInv(writeMsgs)
// @ fold msgs[:pkts][i0].Mem(1)
// @ fold msgs[:pkts][i0].Mem()
// @ assume false
if err != nil {
// @ requires err != nil && err.ErrorMem()
Expand Down
Loading

0 comments on commit 2a65c9d

Please sign in to comment.