Skip to content

Commit

Permalink
fix injectivity issue in run() and verification error in newPacketPro…
Browse files Browse the repository at this point in the history 
…cessor
  • Loading branch information
@mlimbeck
mlimbeck committed Aug 16, 2024
1 parent 6ccb661 commit 155909d
Showing 1 changed file with 47 additions and 30 deletions.
77 changes: 47 additions & 30 deletions router/dataplane.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -120,30 +120,36 @@ type BatchConn interface {

// @ requires acc(Mem(), _)
// @ requires forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
// @ msgs[i].Mem() &&
// @ acc(sl.Bytes(msgs[i].GetFstBuffer(), 0, len(msgs[i].GetFstBuffer())), writePerm)
// @ msgs[i].Mem()
// @ requires forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
// @ msgs[i].GetFstBuffer() in msgsUBufs
// @ requires forall ubuf []byte :: { ubuf } ubuf in msgsUBufs ==>
// @ sl.Bytes(ubuf, 0, len(ubuf))
// @ ensures forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
// @ (msgs[i].Mem() && msgs[i].HasActiveAddr() &&
// @ acc(sl.Bytes(msgs[i].GetFstBuffer(), 0, len(msgs[i].GetFstBuffer())), writePerm))
// @ (msgs[i].Mem() && msgs[i].HasActiveAddr())
// @ ensures err == nil ==> 0 <= n && n <= len(msgs)
// @ ensures err == nil ==>
// @ forall i int :: { &msgs[i] } 0 <= i && i < n ==> (
// @ 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 forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
// @ msgs[i].GetFstBuffer() in msgsUBufs
// @ ensures forall ubuf []byte :: { ubuf } ubuf in msgsUBufs ==>
// @ sl.Bytes(ubuf, 0, len(ubuf))
// @ ensures err != nil ==> err.ErrorMem()
// contracts for IO-spec
// @ requires Prophecy(prophecyM)
// @ requires io.token(place) && MultiReadBio(place, prophecyM)
// @ ensures err != nil ==> prophecyM == 0
// @ ensures err == nil ==> prophecyM == n
// @ ensures io.token(old(MultiReadBioNext(place, prophecyM)))
// @ ensures old(MultiReadBioCorrectIfs(place, prophecyM, path.ifsToIO_ifs(ingressID)))
// @ ensures err == nil ==>
// @ requires Prophecy(prophecyM)
// @ requires io.token(place) && MultiReadBio(place, prophecyM)
// @ ensures err != nil ==> prophecyM == 0
// @ ensures err == nil ==> prophecyM == n
// @ ensures io.token(old(MultiReadBioNext(place, prophecyM)))
// @ ensures old(MultiReadBioCorrectIfs(place, prophecyM, path.ifsToIO_ifs(ingressID)))
// @ ensures err == nil ==>
// @ forall i int :: { &msgs[i] } 0 <= i && i < n ==>
// @ MsgToAbsVal(&msgs[i], ingressID) == old(MultiReadBioIO_val(place, n)[i])
ReadBatch(msgs underlayconn.Messages /*@, ghost ingressID uint16, ghost prophecyM int, ghost place io.Place @*/) (n int, err error)
ReadBatch(msgs underlayconn.Messages /*@, ghost msgsUBufs set[[]byte], ghost ingressID uint16, ghost prophecyM int, ghost place io.Place @*/) (n int, err error)
// @ requires acc(addr.Mem(), _)
// @ requires acc(Mem(), _)
// @ preserves acc(sl.Bytes(b, 0, len(b)), R10)
Expand Down Expand Up @@ -820,23 +826,29 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
func /*@ rc @*/ (ingressID uint16, rd BatchConn, dPtr **DataPlane /*@, ghost ioLock gpointer[gsync.GhostMutex], ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/) {
d := *dPtr
msgs := conn.NewReadMessages(inputBatchCnt)
// @ ghost var msgsUBufs set[[]byte]
// @ requires forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
// @ msgs[i].Mem() && msgs[i].GetAddr() == nil &&
// @ acc(sl.Bytes(msgs[i].GetFstBuffer(), 0, len(msgs[i].GetFstBuffer())), writePerm)
// @ msgs[i].Mem() && msgs[i].GetAddr() == nil
// @ ensures forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
// @ msgs[i].Mem() &&
// @ msgs[i].HasActiveAddr() &&
// @ msgs[i].GetAddr() == nil &&
// @ acc(sl.Bytes(msgs[i].GetFstBuffer(), 0, len(msgs[i].GetFstBuffer())), writePerm)
// @ msgs[i].GetAddr() == nil
// @ ensures forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
// @ msgs[i].GetFstBuffer() in msgsUBufs
// @ ensures forall ubuf []byte :: { ubuf } ubuf in msgsUBufs ==>
// @ sl.Bytes(ubuf, 0, len(ubuf))
// @ decreases
// @ outline(
// @ msgsUBufs := set[[]byte]{}
// @ invariant 0 <= i0 && i0 <= len(msgs)
// @ invariant forall i int :: { &msgs[i] } i0 <= i && i < len(msgs) ==>
// @ msgs[i].Mem() && msgs[i].GetAddr() == nil &&
// @ acc(sl.Bytes(msgs[i].GetFstBuffer(), 0, len(msgs[i].GetFstBuffer())), writePerm)
// @ msgs[i].Mem() && msgs[i].GetAddr() == nil
// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < i0 ==>
// @ msgs[i].Mem() && msgs[i].GetAddr() == nil && msgs[i].HasActiveAddr() &&
// @ acc(sl.Bytes(msgs[i].GetFstBuffer(), 0, len(msgs[i].GetFstBuffer())), writePerm)
// @ msgs[i].Mem() && msgs[i].GetAddr() == nil && msgs[i].HasActiveAddr()
// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < i0 ==>
// @ msgs[i].GetFstBuffer() in msgsUBufs
// @ invariant forall ubuf []byte :: { ubuf } ubuf in msgsUBufs ==>
// @ sl.Bytes(ubuf, 0, len(ubuf))
// @ decreases len(msgs) - i0
for i0 := 0; i0 < len(msgs); i0 += 1 {
// (VerifiedSCION) changed a range loop in favor of a normal loop
Expand All @@ -854,6 +866,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
msg.Buffers[0] = tmp
// @ msgs[i0].IsActive = true
// @ fold msgs[i0].Mem()
// @ msgsUBufs = msgsUBufs union set[[]byte]{msgs[i0].GetFstBuffer()}
}
// @ )
// @ ensures writeMsgInv(writeMsgs)
Expand All @@ -873,8 +886,11 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta

// @ invariant acc(&scmpErr)
// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
// @ msgs[i].Mem() &&
// @ acc(sl.Bytes(msgs[i].GetFstBuffer(), 0, len(msgs[i].GetFstBuffer())), writePerm)
// @ msgs[i].Mem()
// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
// @ msgs[i].GetFstBuffer() in msgsUBufs
// @ invariant forall ubuf []byte :: { ubuf } ubuf in msgsUBufs ==>
// @ sl.Bytes(ubuf, 0, len(ubuf))
// @ invariant writeMsgInv(writeMsgs)
// @ invariant acc(dPtr, _) && *dPtr === d
// @ invariant acc(&d.running, _) // necessary for loop condition
Expand Down Expand Up @@ -906,7 +922,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
// @ ghost tN := MultiReadBioNext(t, numberOfReceivedPacketsProphecy)
// @ assert dp.dp3s_iospec_ordered(sN, tN)
// @ BeforeReadBatch:
pkts, err := rd.ReadBatch(msgs /*@, ingressID, numberOfReceivedPacketsProphecy, t @*/)
pkts, err := rd.ReadBatch(msgs /*@, msgsUBufs, ingressID, numberOfReceivedPacketsProphecy, t @*/)
// @ assert old[BeforeReadBatch](MultiReadBioIO_val(t, numberOfReceivedPacketsProphecy)) == ioValSeq
// @ assert err == nil ==>
// @ forall i int :: { &msgs[i] } 0 <= i && i < pkts ==>
Expand All @@ -923,8 +939,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
// @ ioLock.Unlock()
// End of multi recv event

// @ assert forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem() &&
// @ acc(sl.Bytes(msgs[i].GetFstBuffer(), 0, len(msgs[i].GetFstBuffer())), writePerm)
// @ 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 @@ -946,8 +961,11 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
// (VerifiedSCION) using regular for loop instead of range loop to avoid unnecessary
// complications with permissions
// @ invariant acc(&scmpErr)
// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem() &&
// @ acc(sl.Bytes(msgs[i].GetFstBuffer(), 0, len(msgs[i].GetFstBuffer())), writePerm)
// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem()
// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
// @ msgs[i].GetFstBuffer() in msgsUBufs
// @ invariant forall ubuf []byte :: { ubuf } ubuf in msgsUBufs ==>
// @ sl.Bytes(ubuf, 0, len(ubuf))
// @ invariant writeMsgInv(writeMsgs)
// @ invariant acc(dPtr, _) && *dPtr === d
// @ invariant acc(d.Mem(), _) && d.WellConfigured()
Expand Down Expand Up @@ -1395,7 +1413,7 @@ func newPacketProcessor(d *DataPlane, ingressID uint16) (res *scionPacketProcess
var verScionTmp gopacket.SerializeBuffer
// @ d.getNewPacketProcessorFootprint()
verScionTmp = gopacket.NewSerializeBuffer()
// @ assert acc(sl.Bytes(verScionTmp.UBuf(), 0, len(verScionTmp.UBuf())), writePerm)
// @ unfold acc(sl.Bytes(verScionTmp.UBuf(), 0, len(verScionTmp.UBuf())), writePerm)
p := &scionPacketProcessor{
d: d,
ingressID: ingressID,
Expand All @@ -1406,8 +1424,7 @@ func newPacketProcessor(d *DataPlane, ingressID uint16) (res *scionPacketProcess
epicInput: make([]byte, libepic.MACBufferSize),
},
}
// @ assert p.buffer.UBuf() === verScionTmp.UBuf()
// @ assert acc(sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())), writePerm)
// @ fold acc(sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())), writePerm)
// @ fold sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput))
// @ fold slayers.PathPoolMem(p.scionLayer.pathPool, p.scionLayer.pathPoolRaw)
p.scionLayer.RecyclePaths()
Expand Down

0 comments on commit 155909d

Please sign in to comment.