diff --git a/pkg/slayers/scion.go b/pkg/slayers/scion.go index fdf5a4232..e3de3e8f3 100644 --- a/pkg/slayers/scion.go +++ b/pkg/slayers/scion.go @@ -218,9 +218,11 @@ func (s *SCION) NetworkFlow() (res gopacket.Flow) { // @ requires b != nil && b.Mem() // @ requires acc(s.Mem(ubuf), R0) // @ requires sl.Bytes(ubuf, 0, len(ubuf)) +// @ requires sl.Bytes(b.UBuf(), 0, len(b.UBuf())) // @ ensures b.Mem() // @ ensures acc(s.Mem(ubuf), R0) // @ ensures sl.Bytes(ubuf, 0, len(ubuf)) +// @ ensures sl.Bytes(b.UBuf(), 0, len(b.UBuf())) // TODO: hide internal spec details // @ ensures e == nil && s.HasOneHopPath(ubuf) ==> // @ len(b.UBuf()) == old(len(b.UBuf())) + unfolding acc(s.Mem(ubuf), R55) in @@ -257,7 +259,6 @@ func (s *SCION) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeO } // @ ghost uSerBufN := b.UBuf() // @ assert buf === uSerBufN[:scnLen] - // @ b.ExchangePred() // @ unfold acc(sl.Bytes(uSerBufN, 0, len(uSerBufN)), writePerm) // Serialize common header. @@ -287,7 +288,6 @@ func (s *SCION) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeO // @ sl.Unslice_Bytes(uSerBufN, 0, CmnHdrLen, R54) // @ sl.CombineRange_Bytes(uSerBufN, CmnHdrLen, scnLen, writePerm) // @ sl.CombineRange_Bytes(ubuf, CmnHdrLen, len(ubuf), R10) - // @ b.RestoreMem(uSerBufN) return err } offset := CmnHdrLen + s.AddrHdrLen( /*@ nil, true @*/ ) @@ -320,7 +320,6 @@ func (s *SCION) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeO // @ sl.CombineRange_Bytes(uSerBufN, offset, scnLen, HalfPerm) // @ sl.CombineRange_Bytes(ubuf, startP, endP, HalfPerm) // @ reveal IsSupportedPkt(uSerBufN) - // @ b.RestoreMem(uSerBufN) // @ reveal IsSupportedRawPkt(b.View()) return tmp } diff --git a/pkg/slayers/scmp.go b/pkg/slayers/scmp.go index ab15de197..6892c007d 100644 --- a/pkg/slayers/scmp.go +++ b/pkg/slayers/scmp.go @@ -111,6 +111,7 @@ func (s *SCMP) NextLayerType( /*@ ghost ub []byte @*/ ) gopacket.LayerType { // @ requires b != nil // @ requires s.Mem(ubufMem) // @ preserves b.Mem() +// @ preserves sl.Bytes(b.UBuf(), 0, len(b.UBuf())) // @ ensures err == nil ==> s.Mem(ubufMem) // @ ensures err != nil ==> err.ErrorMem() // @ decreases @@ -121,15 +122,6 @@ func (s *SCMP) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOp return err } // @ unfold s.Mem(ubufMem) - - // @ requires len(underlyingBufRes) >= 4 - // @ requires bytes === underlyingBufRes[:4] - // @ requires b != nil - // @ preserves acc(&s.TypeCode) - // @ preserves b.Mem() && b.UBuf() === underlyingBufRes - // @ decreases - // @ outline ( - // @ b.ExchangePred() // @ sl.SplitByIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm) // @ unfold sl.Bytes(underlyingBufRes, 0, 2) // @ assert forall i int :: { &bytes[i] } 0 <= i && i < 2 ==> &bytes[i] == &underlyingBufRes[i] @@ -138,8 +130,6 @@ func (s *SCMP) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOp // @ unfold sl.Bytes(bytes, 0, 2) // @ fold sl.Bytes(underlyingBufRes, 0, 2) // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm) - // @ b.RestoreMem(underlyingBufRes) - // @ ) if opts.ComputeChecksums { if s.scn == nil { @@ -147,13 +137,6 @@ func (s *SCMP) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOp return serrors.New("can not calculate checksum without SCION header") } // zero out checksum bytes - // @ requires len(underlyingBufRes) >= 4 - // @ requires bytes === underlyingBufRes[:4] - // @ requires b != nil - // @ preserves b.Mem() && b.UBuf() === underlyingBufRes - // @ decreases - // @ outline ( - // @ b.ExchangePred() // @ sl.SplitByIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 4, writePerm) // @ unfold sl.Bytes(underlyingBufRes, 0, 4) // @ assert forall i int :: { &bytes[i] } 0 <= i && i < 4 ==> &bytes[i] == &underlyingBufRes[i] @@ -161,27 +144,16 @@ func (s *SCMP) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOp bytes[3] = 0 // @ fold sl.Bytes(underlyingBufRes, 0, 4) // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 4, writePerm) - // @ b.RestoreMem(underlyingBufRes) - // @ ) verScionTmp := b.Bytes() // @ unfold s.scn.ChecksumMem() s.Checksum, err = s.scn.computeChecksum(verScionTmp, uint8(L4SCMP)) // @ fold s.scn.ChecksumMem() - // @ b.RestoreMem(verScionTmp) if err != nil { // @ fold s.Mem(ubufMem) return err } } - // @ requires len(underlyingBufRes) >= 4 - // @ requires bytes === underlyingBufRes[:4] - // @ requires b != nil - // @ preserves acc(&s.Checksum) - // @ preserves b.Mem() && b.UBuf() === underlyingBufRes - // @ decreases - // @ outline ( - // @ b.ExchangePred() // @ sl.SplitByIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 4, writePerm) // @ unfold sl.Bytes(underlyingBufRes, 0, 4) // @ assert forall i int :: { &bytes[i] } 0 <= i && i < 4 ==> &bytes[i] == &underlyingBufRes[i] @@ -189,8 +161,6 @@ func (s *SCMP) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOp binary.BigEndian.PutUint16(bytes[2:], s.Checksum) // @ fold sl.Bytes(underlyingBufRes, 0, 4) // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 4, writePerm) - // @ b.RestoreMem(underlyingBufRes) - // @ ) // @ fold s.Mem(ubufMem) return nil } diff --git a/pkg/slayers/scmp_msg.go b/pkg/slayers/scmp_msg.go index 80748dddd..6df7fdee6 100644 --- a/pkg/slayers/scmp_msg.go +++ b/pkg/slayers/scmp_msg.go @@ -110,6 +110,7 @@ func (i *SCMPExternalInterfaceDown) DecodeFromBytes(data []byte, // @ requires b != nil // @ requires i.Mem(ubufMem) // @ preserves b.Mem() +// @ preserves sl.Bytes(b.UBuf(), 0, len(b.UBuf())) // @ ensures err == nil ==> i.Mem(ubufMem) // @ ensures err != nil ==> err.ErrorMem() // @ decreases @@ -123,7 +124,6 @@ func (i *SCMPExternalInterfaceDown) SerializeTo(b gopacket.SerializeBuffer, opts offset := 0 // @ unfold i.Mem(ubufMem) // @ defer fold i.Mem(ubufMem) - // @ b.ExchangePred() // @ assert buf === underlyingBufRes[:addr.IABytes+scmpRawInterfaceLen] // @ sl.SplitRange_Bytes(underlyingBufRes, 0, len(buf), writePerm) // @ assert sl.Bytes(buf, 0, len(buf)) @@ -138,7 +138,6 @@ func (i *SCMPExternalInterfaceDown) SerializeTo(b gopacket.SerializeBuffer, opts // @ fold sl.Bytes(newSlice, 0, len(newSlice)) // @ sl.CombineRange_Bytes(buf, offset, offset+scmpRawInterfaceLen, writePerm) // @ sl.CombineRange_Bytes(underlyingBufRes, 0, len(buf), writePerm) - // @ b.RestoreMem(underlyingBufRes) return nil } @@ -256,6 +255,7 @@ func (i *SCMPInternalConnectivityDown) DecodeFromBytes(data []byte, // @ requires b != nil // @ requires i.Mem(ubufMem) // @ preserves b.Mem() +// @ preserves sl.Bytes(b.UBuf(), 0, len(b.UBuf())) // @ ensures err == nil ==> i.Mem(ubufMem) // @ ensures err != nil ==> err.ErrorMem() // @ decreases @@ -269,7 +269,6 @@ func (i *SCMPInternalConnectivityDown) SerializeTo(b gopacket.SerializeBuffer, o offset := 0 // @ unfold i.Mem(ubufMem) // @ defer fold i.Mem(ubufMem) - // @ b.ExchangePred() // @ sl.SplitRange_Bytes(underlyingBufRes, 0, len(buf), writePerm) // @ assert sl.Bytes(buf, 0, len(buf)) // @ sl.SplitRange_Bytes(buf, offset, len(buf), writePerm) @@ -292,7 +291,6 @@ func (i *SCMPInternalConnectivityDown) SerializeTo(b gopacket.SerializeBuffer, o // @ fold sl.Bytes(newSlice, 0, len(newSlice)) // @ sl.CombineRange_Bytes(buf, offset, offset+scmpRawInterfaceLen, writePerm) // @ sl.CombineRange_Bytes(underlyingBufRes, 0, len(buf), writePerm) - // @ b.RestoreMem(underlyingBufRes) return nil } @@ -419,6 +417,7 @@ func (i *SCMPEcho) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback) (res // @ requires b != nil // @ requires i.Mem(ubufMem) // @ preserves b.Mem() +// @ preserves sl.Bytes(b.UBuf(), 0, len(b.UBuf())) // @ ensures err == nil ==> i.Mem(ubufMem) // @ ensures err != nil ==> err.ErrorMem() // @ decreases @@ -431,32 +430,12 @@ func (i *SCMPEcho) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.Seriali offset := 0 // @ unfold i.Mem(ubufMem) // @ defer fold i.Mem(ubufMem) - // @ requires offset == 0 - // @ requires len(underlyingBufRes) >= 4 - // @ requires buf === underlyingBufRes[:4] - // @ requires b != nil - // @ preserves acc(&i.Identifier) - // @ preserves b.Mem() && b.UBuf() === underlyingBufRes - // @ decreases - // @ outline ( - // @ b.ExchangePred() // @ sl.SplitByIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm) // @ unfold sl.Bytes(underlyingBufRes, 0, 2) binary.BigEndian.PutUint16(buf[:2], i.Identifier) // @ fold sl.Bytes(underlyingBufRes, 0, 2) // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm) - // @ b.RestoreMem(underlyingBufRes) - // @ ) offset += 2 - // @ requires offset == 2 - // @ requires len(underlyingBufRes) >= 4 - // @ requires buf === underlyingBufRes[:4] - // @ requires b != nil - // @ preserves acc(&i.SeqNumber) - // @ preserves b.Mem() && b.UBuf() === underlyingBufRes - // @ decreases - // @ outline ( - // @ b.ExchangePred() // @ sl.SplitByIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm) // @ sl.SplitByIndex_Bytes(underlyingBufRes, 2, len(underlyingBufRes), 4, writePerm) // @ unfold sl.Bytes(underlyingBufRes, 2, 4) @@ -465,8 +444,6 @@ func (i *SCMPEcho) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.Seriali // @ fold sl.Bytes(underlyingBufRes, 2, 4) // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 2, len(underlyingBufRes), 4, writePerm) // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm) - // @ b.RestoreMem(underlyingBufRes) - // @ ) return nil } @@ -567,6 +544,7 @@ func (i *SCMPParameterProblem) DecodeFromBytes(data []byte, df gopacket.DecodeFe // @ requires b != nil // @ requires i.Mem(ubufMem) // @ preserves b.Mem() +// @ preserves sl.Bytes(b.UBuf(), 0, len(b.UBuf())) // @ ensures err == nil ==> i.Mem(ubufMem) // @ ensures err != nil ==> err.ErrorMem() // @ decreases @@ -579,28 +557,11 @@ func (i *SCMPParameterProblem) SerializeTo(b gopacket.SerializeBuffer, opts gopa } // @ unfold i.Mem(ubufMem) // @ defer fold i.Mem(ubufMem) - // @ requires len(underlyingBufRes) >= 4 - // @ requires buf === underlyingBufRes[:4] - // @ requires b != nil - // @ preserves b.Mem() && b.UBuf() === underlyingBufRes - // @ decreases - // @ outline ( - // @ b.ExchangePred() // @ sl.SplitByIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm) // @ unfold sl.Bytes(underlyingBufRes, 0, 2) binary.BigEndian.PutUint16(buf[0:2], uint16(0)) //Reserved // @ fold sl.Bytes(underlyingBufRes, 0, 2) // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm) - // @ b.RestoreMem(underlyingBufRes) - // @ ) - // @ requires len(underlyingBufRes) >= 4 - // @ requires buf === underlyingBufRes[:4] - // @ requires b != nil - // @ preserves acc(&i.Pointer) - // @ preserves b.Mem() && b.UBuf() === underlyingBufRes - // @ decreases - // @ outline ( - // @ b.ExchangePred() // @ sl.SplitByIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm) // @ sl.SplitByIndex_Bytes(underlyingBufRes, 2, len(underlyingBufRes), 4, writePerm) // @ unfold sl.Bytes(underlyingBufRes, 2, 4) @@ -609,8 +570,6 @@ func (i *SCMPParameterProblem) SerializeTo(b gopacket.SerializeBuffer, opts gopa // @ fold sl.Bytes(underlyingBufRes, 2, 4) // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 2, len(underlyingBufRes), 4, writePerm) // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm) - // @ b.RestoreMem(underlyingBufRes) - // @ ) return nil } @@ -763,6 +722,7 @@ func (i *SCMPTraceroute) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback // @ requires b != nil // @ requires i.Mem(ubufMem) // @ preserves b.Mem() +// @ preserves sl.Bytes(b.UBuf(), 0, len(b.UBuf())) // @ ensures err == nil ==> i.Mem(ubufMem) // @ ensures err != nil ==> err.ErrorMem() // @ decreases @@ -776,32 +736,12 @@ func (i *SCMPTraceroute) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.S offset := 0 // @ unfold i.Mem(ubufMem) // @ defer fold i.Mem(ubufMem) - // @ requires offset == 0 - // @ requires len(underlyingBufRes) >= 2 + 2 + addr.IABytes + scmpRawInterfaceLen - // @ requires buf === underlyingBufRes[:2+2+addr.IABytes+scmpRawInterfaceLen] - // @ requires b != nil - // @ preserves acc(&i.Identifier) - // @ preserves b.Mem() && b.UBuf() === underlyingBufRes - // @ decreases - // @ outline ( - // @ b.ExchangePred() // @ sl.SplitByIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm) // @ unfold sl.Bytes(underlyingBufRes, 0, 2) binary.BigEndian.PutUint16(buf[:2], i.Identifier) // @ fold sl.Bytes(underlyingBufRes, 0, 2) // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm) - // @ b.RestoreMem(underlyingBufRes) - // @ ) offset += 2 - // @ requires offset == 2 - // @ requires len(underlyingBufRes) >= 2 + 2 + addr.IABytes + scmpRawInterfaceLen - // @ requires buf === underlyingBufRes[:2 + 2 + addr.IABytes + scmpRawInterfaceLen] - // @ requires b != nil - // @ preserves acc(&i.Sequence) - // @ preserves b.Mem() && b.UBuf() === underlyingBufRes - // @ decreases - // @ outline ( - // @ b.ExchangePred() // @ sl.SplitByIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm) // @ sl.SplitByIndex_Bytes(underlyingBufRes, 2, len(underlyingBufRes), 2+2, writePerm) // @ unfold sl.Bytes(underlyingBufRes, 2, 2+2) @@ -810,18 +750,7 @@ func (i *SCMPTraceroute) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.S // @ fold sl.Bytes(underlyingBufRes, 2, 2+2) // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 2, len(underlyingBufRes), 2+2, writePerm) // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm) - // @ b.RestoreMem(underlyingBufRes) - // @ ) offset += 2 - // @ requires offset == 2 + 2 - // @ requires len(underlyingBufRes) >= 2 + 2 + addr.IABytes + scmpRawInterfaceLen - // @ requires buf === underlyingBufRes[:2 + 2 + addr.IABytes + scmpRawInterfaceLen] - // @ requires b != nil - // @ preserves acc(&i.IA) - // @ preserves b.Mem() && b.UBuf() === underlyingBufRes - // @ decreases - // @ outline ( - // @ b.ExchangePred() // @ sl.SplitByIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2+2, writePerm) // @ sl.SplitByIndex_Bytes(underlyingBufRes, 2+2, len(underlyingBufRes), 2+2+addr.IABytes, writePerm) // @ unfold sl.Bytes(underlyingBufRes, 2+2, 2+2+addr.IABytes) @@ -830,18 +759,7 @@ func (i *SCMPTraceroute) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.S // @ fold sl.Bytes(underlyingBufRes, 2+2, 2+2+addr.IABytes) // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 2+2, len(underlyingBufRes), 2+2+addr.IABytes, writePerm) // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2+2, writePerm) - // @ b.RestoreMem(underlyingBufRes) - // @ ) offset += addr.IABytes - // @ requires offset == 2 + 2 + addr.IABytes - // @ requires len(underlyingBufRes) >= 2 + 2 + addr.IABytes + scmpRawInterfaceLen - // @ requires buf === underlyingBufRes[:2 + 2 + addr.IABytes + scmpRawInterfaceLen] - // @ requires b != nil - // @ preserves acc(&i.Interface) - // @ preserves b.Mem() && b.UBuf() === underlyingBufRes - // @ decreases - // @ outline ( - // @ b.ExchangePred() // @ sl.SplitByIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2+2+addr.IABytes, writePerm) // @ sl.SplitByIndex_Bytes(underlyingBufRes, 2+2+addr.IABytes, len(underlyingBufRes), 2+2+addr.IABytes+scmpRawInterfaceLen, writePerm) // @ unfold sl.Bytes(underlyingBufRes, 2+2+addr.IABytes, 2+2+addr.IABytes+scmpRawInterfaceLen) @@ -850,8 +768,6 @@ func (i *SCMPTraceroute) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.S // @ fold sl.Bytes(underlyingBufRes, 2+2+addr.IABytes, 2+2+addr.IABytes+scmpRawInterfaceLen) // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 2+2+addr.IABytes, len(underlyingBufRes), 2+2+addr.IABytes+scmpRawInterfaceLen, writePerm) // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2+2+addr.IABytes, writePerm) - // @ b.RestoreMem(underlyingBufRes) - // @ ) return nil } @@ -935,6 +851,7 @@ func (i *SCMPDestinationUnreachable) DecodeFromBytes(data []byte, // @ requires b != nil // @ requires i.Mem(ubufMem) // @ preserves b.Mem() +// @ preserves sl.Bytes(b.UBuf(), 0, len(b.UBuf())) // @ ensures err == nil ==> i.Mem(ubufMem) // @ ensures err != nil ==> err.ErrorMem() // @ decreases @@ -946,13 +863,11 @@ func (i *SCMPDestinationUnreachable) SerializeTo(b gopacket.SerializeBuffer, opt return err } // @ assert buf === underlyingBufRes[:4] - // @ b.ExchangePred() // @ sl.SplitByIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 4, writePerm) // @ unfold sl.Bytes(underlyingBufRes, 0, 4) copy(buf, make([]byte, 4) /*@, writePerm@*/) // @ fold sl.Bytes(underlyingBufRes, 0, 4) // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 4, writePerm) - // @ b.RestoreMem(underlyingBufRes) return nil } @@ -1054,6 +969,7 @@ func (i *SCMPPacketTooBig) DecodeFromBytes(data []byte, df gopacket.DecodeFeedba // @ requires b != nil // @ requires i.Mem(ubufMem) // @ preserves b.Mem() +// @ preserves sl.Bytes(b.UBuf(), 0, len(b.UBuf())) // @ ensures err == nil ==> i.Mem(ubufMem) // @ ensures err != nil ==> err.ErrorMem() // @ decreases @@ -1066,28 +982,11 @@ func (i *SCMPPacketTooBig) SerializeTo(b gopacket.SerializeBuffer, opts gopacket } // @ unfold i.Mem(ubufMem) // @ defer fold i.Mem(ubufMem) - // @ requires len(underlyingBufRes) >= 4 - // @ requires buf === underlyingBufRes[:4] - // @ requires b != nil - // @ preserves b.Mem() && b.UBuf() === underlyingBufRes - // @ decreases - // @ outline ( - // @ b.ExchangePred() // @ sl.SplitByIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm) // @ unfold sl.Bytes(underlyingBufRes, 0, 2) binary.BigEndian.PutUint16(buf[0:2], uint16(0)) //Reserved // @ fold sl.Bytes(underlyingBufRes, 0, 2) // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm) - // @ b.RestoreMem(underlyingBufRes) - // @ ) - // @ requires len(underlyingBufRes) >= 4 - // @ requires buf === underlyingBufRes[:4] - // @ requires b != nil - // @ preserves acc(&i.MTU) - // @ preserves b.Mem() && b.UBuf() === underlyingBufRes - // @ decreases - // @ outline ( - // @ b.ExchangePred() // @ sl.SplitByIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm) // @ sl.SplitByIndex_Bytes(underlyingBufRes, 2, len(underlyingBufRes), 4, writePerm) // @ unfold sl.Bytes(underlyingBufRes, 2, 4) @@ -1096,8 +995,6 @@ func (i *SCMPPacketTooBig) SerializeTo(b gopacket.SerializeBuffer, opts gopacket // @ fold sl.Bytes(underlyingBufRes, 2, 4) // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 2, len(underlyingBufRes), 4, writePerm) // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm) - // @ b.RestoreMem(underlyingBufRes) - // @ ) return nil } diff --git a/router/dataplane.go b/router/dataplane.go index 48781475b..8cb63d1d9 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -121,6 +121,8 @@ type BatchConn interface { // @ requires acc(Mem(), _) // @ requires forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> // @ msgs[i].Mem() + // @ requires forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> + // @ sl.Bytes(msgs[j].GetFstBuffer(), 0, len(msgs[j].GetFstBuffer())) // @ ensures forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> // @ (msgs[i].Mem() && msgs[i].HasActiveAddr()) // @ ensures err == nil ==> 0 <= n && n <= len(msgs) @@ -130,15 +132,17 @@ type BatchConn interface { // @ !msgs[i].HasWildcardPermAddr()) // @ ensures err == nil ==> // @ forall i int :: { &msgs[i] } 0 <= i && i < n ==> msgs[i].GetN() <= len(msgs[i].GetFstBuffer()) + // @ ensures forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> + // @ sl.Bytes(msgs[j].GetFstBuffer(), 0, len(msgs[j].GetFstBuffer())) // @ 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) @@ -153,10 +157,12 @@ type BatchConn interface { // performance reasons. // @ requires len(msgs) == 1 // @ requires acc(msgs[0].Mem(), R50) && msgs[0].HasActiveAddr() + // @ requires acc(sl.Bytes(msgs[0].GetFstBuffer(), 0, len(msgs[0].GetFstBuffer())), R50) // preconditions for IO-spec: // @ requires MsgToAbsVal(&msgs[0], egressID) == ioAbsPkts // @ requires io.token(place) && io.CBioIO_bio3s_send(place, ioAbsPkts) // @ ensures acc(msgs[0].Mem(), R50) && msgs[0].HasActiveAddr() + // @ ensures acc(sl.Bytes(msgs[0].GetFstBuffer(), 0, len(msgs[0].GetFstBuffer())), R50) // @ ensures err == nil ==> 0 <= n && n <= len(msgs) // @ ensures err != nil ==> err.ErrorMem() // postconditions for IO-spec: @@ -822,6 +828,8 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ msgs[i].Mem() && // @ msgs[i].HasActiveAddr() && // @ msgs[i].GetAddr() == nil + // @ ensures forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> + // @ sl.Bytes(msgs[j].GetFstBuffer(), 0, len(msgs[j].GetFstBuffer())) // @ decreases // @ outline( // @ invariant 0 <= i0 && i0 <= len(msgs) @@ -829,6 +837,10 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ 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() + // @ invariant forall j, k int :: { &msgs[j], &msgs[k] } 0 <= j && j < k && k < i0 ==> + // @ msgs[j].GetFstBuffer() !== msgs[k].GetFstBuffer() + // @ invariant forall j int :: { &msgs[j] } 0 <= j && j < i0 ==> + // @ sl.Bytes(msgs[j].GetFstBuffer(), 0, len(msgs[j].GetFstBuffer())) // @ decreases len(msgs) - i0 for i0 := 0; i0 < len(msgs); i0 += 1 { // (VerifiedSCION) changed a range loop in favor of a normal loop @@ -836,6 +848,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ unfold msgs[i0].Mem() msg := msgs[i0] // @ ensures sl.Bytes(tmp, 0, len(tmp)) + // @ ensures len(tmp) > 0 // @ decreases // @ outline( tmp := make([]byte, bufSize) @@ -846,6 +859,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() + // @ msgs[i0].EnsureBufferInjectivityAgainstList(msgs[:i0]) } // @ ) // @ ensures writeMsgInv(writeMsgs) @@ -866,6 +880,8 @@ 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() + // @ invariant forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> + // @ sl.Bytes(msgs[j].GetFstBuffer(), 0, len(msgs[j].GetFstBuffer())) // @ invariant writeMsgInv(writeMsgs) // @ invariant acc(dPtr, _) && *dPtr === d // @ invariant acc(&d.running, _) // necessary for loop condition @@ -876,8 +892,9 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ invariant ingressID in d.getDomForwardingMetrics() // @ invariant acc(rd.Mem(), _) // @ invariant processor.sInit() && processor.sInitD() === d + // @ invariant let ubuf := processor.sInitBufferUBuf() in + // @ acc(sl.Bytes(ubuf, 0, len(ubuf)), writePerm) // @ invariant processor.getIngressID() == ingressID - // @ invariant processor.sInitBuffWithFullPerm() // @ invariant acc(ioLock.LockP(), _) // @ invariant ioLock.LockInv() == SharedInv!< dp, ioSharedArg !> // @ invariant d.DpAgreesWithSpec(dp) && dp.Valid() @@ -936,6 +953,8 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // complications with permissions // @ invariant acc(&scmpErr) // @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem() + // @ invariant forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> + // @ sl.Bytes(msgs[j].GetFstBuffer(), 0, len(msgs[j].GetFstBuffer())) // @ invariant writeMsgInv(writeMsgs) // @ invariant acc(dPtr, _) && *dPtr === d // @ invariant acc(d.Mem(), _) && d.WellConfigured() @@ -953,8 +972,9 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ invariant forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> // @ msgs[i].GetN() <= len(msgs[i].GetFstBuffer()) // @ invariant processor.sInit() && processor.sInitD() === d + // @ invariant let ubuf := processor.sInitBufferUBuf() in + // @ acc(sl.Bytes(ubuf, 0, len(ubuf)), writePerm) // @ invariant processor.getIngressID() == ingressID - // @ invariant processor.sInitBuffWithFullPerm() // contracts for IO-spec // @ invariant pkts <= len(ioValSeq) // @ invariant d.DpAgreesWithSpec(dp) && dp.Valid() @@ -1086,7 +1106,6 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ assert result.OutPkt != nil ==> newAbsPkt == // @ absIO_val(writeMsgs[0].Buffers[0], result.EgressID) // @ fold acc(writeMsgs[0].Mem(), R50) - // @ ghost ioLock.Lock() // @ unfold SharedInv!< dp, ioSharedArg !>() // @ ghost t, s := *ioSharedArg.Place, *ioSharedArg.State @@ -1110,12 +1129,6 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ sl.CombineRange_Bytes(p.Buffers[0], 0, p.N, writePerm) // @ msgs[:pkts][i0].IsActive = false // @ fold msgs[:pkts][i0].Mem() - // @ ghost if !processor.sInitBuffWithFullPerm(){ - // @ processor.sInitBuffer().RestoreMem(writeMsgs[0].Buffers[0]) - // @ unfold acc(processor.sInit(), _) - // @ processor.buffWithFullPerm = true - // @ fold acc(processor.sInit(), _) - // @ } // @ fold writeMsgInv(writeMsgs) if err != nil { // @ requires err != nil && err.ErrorMem() @@ -1381,12 +1394,14 @@ type processResult struct { // @ requires acc(d.Mem(), _) && d.getMacFactory() != nil // @ ensures res.sInit() && res.sInitD() == d && res.getIngressID() == ingressID -// @ ensures res.sInitBuffWithFullPerm() +// @ ensures let ubuf := res.sInitBufferUBuf() in +// @ acc(sl.Bytes(ubuf, 0, len(ubuf)), writePerm) // @ decreases func newPacketProcessor(d *DataPlane, ingressID uint16) (res *scionPacketProcessor) { var verScionTmp gopacket.SerializeBuffer // @ d.getNewPacketProcessorFootprint() verScionTmp = gopacket.NewSerializeBuffer() + // @ sl.PermsImplyIneqWithWildcard(verScionTmp.UBuf(), *d.key) p := &scionPacketProcessor{ d: d, ingressID: ingressID, @@ -1397,7 +1412,6 @@ func newPacketProcessor(d *DataPlane, ingressID uint16) (res *scionPacketProcess epicInput: make([]byte, libepic.MACBufferSize), }, } - // @ p.buffWithFullPerm = true // @ fold sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ fold slayers.PathPoolMem(p.scionLayer.pathPool, p.scionLayer.pathPoolRaw) p.scionLayer.RecyclePaths() @@ -1410,7 +1424,8 @@ func newPacketProcessor(d *DataPlane, ingressID uint16) (res *scionPacketProcess } // @ preserves p.sInit() -// @ preserves p.sInitBuffWithFullPerm() +// @ preserves let ubuf := p.sInitBufferUBuf() in +// @ acc(sl.Bytes(ubuf, 0, len(ubuf)), writePerm) // @ ensures p.sInitD() == old(p.sInitD()) // @ ensures p.getIngressID() == old(p.getIngressID()) // @ ensures p.sInitRawPkt() == nil @@ -1434,7 +1449,6 @@ func (p *scionPacketProcessor) reset() (err error) { } p.mac.Reset() p.cachedMac = nil - // @ p.buffWithFullPerm = true return nil } @@ -1447,7 +1461,8 @@ func (p *scionPacketProcessor) reset() (err error) { // @ d.getValSvc() != nil && // @ d.getValForwardingMetrics() != nil && // @ d.DpAgreesWithSpec(dp) -// @ requires p.sInitBuffWithFullPerm() +// @ requires let ubuf := p.sInitBufferUBuf() in +// @ acc(sl.Bytes(ubuf, 0, len(ubuf)), writePerm) // @ ensures p.sInit() // @ ensures acc(p.sInitD().Mem(), _) // @ ensures p.sInitD() == old(p.sInitD()) @@ -1458,10 +1473,11 @@ func (p *scionPacketProcessor) reset() (err error) { // @ respr.OutAddr != nil && // @ (acc(respr.OutAddr.Mem(), R15) --* acc(sl.Bytes(rawPkt, 0, len(rawPkt)), R15))) // @ ensures !addrAliasesPkt ==> acc(sl.Bytes(rawPkt, 0, len(rawPkt)), R15) -// @ ensures respr.OutPkt !== rawPkt && respr.OutPkt != nil ==> -// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ ensures let ubuf := p.sInitBufferUBuf() in +// @ acc(sl.Bytes(ubuf, 0, len(ubuf)), writePerm) +// @ ensures respr.OutPkt != nil ==> +// @ (respr.OutPkt === rawPkt || respr.OutPkt === p.sInitBufferUBuf()) // @ ensures reserr != nil ==> reserr.ErrorMem() -// @ ensures !p.sInitBuffWithFullPerm() ==> p.sInitBuffer().MemWithoutUBuf(respr.OutPkt) // contracts for IO-spec // @ requires dp.Valid() // @ requires acc(ioLock.LockP(), _) @@ -1732,8 +1748,8 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ requires sl.Bytes(ub, 0, len(ub)) // @ requires acc(&p.segmentChange) && !p.segmentChange // @ requires acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.ingressID, R10) -// @ requires acc(&p.buffWithFullPerm) && p.buffWithFullPerm // @ preserves acc(&p.srcAddr, R10) && acc(p.srcAddr.Mem(), _) // @ preserves acc(&p.lastLayer, R10) // @ preserves p.lastLayer != nil @@ -1749,7 +1765,6 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ preserves acc(&p.macBuffers.scionInput, R10) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) -// @ ensures acc(&p.buffWithFullPerm) // @ ensures acc(&p.segmentChange) // @ ensures acc(&p.ingressID, R10) // @ ensures acc(&p.d, R5) @@ -1761,16 +1776,12 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ respr.OutAddr != nil && // @ (acc(respr.OutAddr.Mem(), R15) --* acc(sl.Bytes(ub, 0, len(ub)), R15))) // @ ensures !addrAliasesPkt ==> acc(sl.Bytes(ub, 0, len(ub)), R15) -// @ ensures respr.OutPkt !== ub && respr.OutPkt != nil ==> -// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) -// @ ensures acc(&p.buffer, R10) +// @ ensures acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() // @ ensures reserr == nil ==> p.scionLayer.Mem(ub) -// @ ensures reserr == nil ==> p.buffer.Mem() && p.buffWithFullPerm // @ ensures reserr != nil ==> p.scionLayer.NonInitMem() -// @ ensures reserr != nil && respr === processResult{} ==> -// @ p.buffer.Mem() && p.buffWithFullPerm -// @ ensures reserr != nil && respr !== processResult{} ==> -// @ !p.buffWithFullPerm && p.buffer.MemWithoutUBuf(respr.OutPkt) +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +// @ ensures respr.OutPkt != nil ==> +// @ (respr.OutPkt === ub || respr.OutPkt === p.buffer.UBuf()) // @ ensures reserr != nil ==> reserr.ErrorMem() // contracts for IO-spec // @ requires p.d.DpAgreesWithSpec(dp) @@ -1859,9 +1870,6 @@ func (p *scionPacketProcessor) processEPIC() (processResult, error) { // scionPacketProcessor processes packets. It contains pre-allocated per-packet // mutable state and context information which should be reused. type scionPacketProcessor struct { - // (VerifiedSCION) buffWithFullPerm holds if we currently hold full permissions - // to the underlying slice from `buffer`. - // @ ghost buffWithFullPerm bool // d is a reference to the dataplane instance that initiated this processor. d *DataPlane // ingressID is the interface ID this packet came in, determined from the @@ -1917,29 +1925,24 @@ type macBuffersT struct { // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires sl.Bytes(ub, 0, len(ub)) // @ requires acc(&p.ingressID, R45) -// @ requires acc(&p.buffer, R50) && p.buffer.Mem() +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires cause != nil ==> cause.ErrorMem() -// @ requires acc(&p.buffWithFullPerm) -// @ requires p.buffWithFullPerm // @ preserves ubLL == nil || ubLL === ub[startLL:endLL] // @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil // @ preserves &p.scionLayer !== p.lastLayer ==> // @ acc(p.lastLayer.Mem(ubLL), R15) // @ preserves &p.scionLayer === p.lastLayer ==> // @ ub === ubLL -// @ ensures acc(&p.buffWithFullPerm) // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) // @ ensures acc(p.scionLayer.Mem(ub), R4) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures acc(&p.ingressID, R45) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) -// @ ensures respr === processResult{} ==> -// @ p.buffer.Mem() && p.buffWithFullPerm +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && -// @ !p.buffWithFullPerm && -// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil && reserr.ErrorMem() // @ ensures respr.OutPkt != nil ==> // @ !slayers.IsSupportedPkt(respr.OutPkt) @@ -2102,9 +2105,8 @@ func (p *scionPacketProcessor) parsePath( /*@ ghost ub []byte @*/ ) (respr proce // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires p.path == p.scionLayer.GetPath(ubScionL) -// @ requires acc(&p.buffer, R50) && p.buffer.Mem() -// @ requires acc(&p.buffWithFullPerm) -// @ requires p.buffWithFullPerm +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // pres for IO: // @ requires slayers.ValidPktMetaHdr(ubScionL) && p.scionLayer.EqAbsHeader(ubScionL) // @ requires absPkt(ubScionL).PathNotFullyTraversed() @@ -2117,19 +2119,15 @@ func (p *scionPacketProcessor) parsePath( /*@ ghost ub []byte @*/ ) (respr proce // @ preserves acc(&p.infoField, R20) // @ preserves acc(&p.hopField, R20) // @ preserves acc(&p.ingressID, R20) -// @ ensures acc(&p.buffWithFullPerm) // @ ensures acc(&p.path, R20) // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) // @ ensures sl.Bytes(ubScionL, 0, len(ubScionL)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) -// @ ensures respr === processResult{} ==> -// @ p.buffer.Mem() && p.buffWithFullPerm +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && -// @ !p.buffWithFullPerm && -// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -2160,11 +2158,6 @@ func (p *scionPacketProcessor) validateHopExpiry( /*@ ghost ubScionL []byte, gho // @ defer fold acc(p.path.Mem(ubPath), R14) // @ unfold acc(p.path.Base.Mem(), R15) // @ defer fold acc(p.path.Base.Mem(), R15) - // (VerifiedSCION) Gobra is unable to verify permissions for `p.path.PathMeta.CurrINF` - // and `p.path.PathMeta.CurrHF` directly at the function call. - // To work around this limitation, these fields are first stored in temporary variables. - tmpCurrINF := p.path.PathMeta.CurrINF - tmpCurrHF := p.path.PathMeta.CurrHF tmpRes, tmpErr := p.packSCMP( slayers.SCMPTypeParameterProblem, @@ -2177,9 +2170,9 @@ func (p *scionPacketProcessor) validateHopExpiry( /*@ ghost ubScionL []byte, gho "if_id", p.ingressID, "curr_inf", - tmpCurrINF, + p.path.PathMeta.CurrINF, "curr_hf", - tmpCurrHF), + p.path.PathMeta.CurrHF), /*@ ubScionL, ubLL, startLL, endLL, @*/ ) // @ ghost if tmpErr != nil && tmpRes.OutPkt != nil { @@ -2194,9 +2187,8 @@ func (p *scionPacketProcessor) validateHopExpiry( /*@ ghost ubScionL []byte, gho // @ requires acc(p.scionLayer.Mem(ubScionL), R3) // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires p.path == p.scionLayer.GetPath(ubScionL) -// @ requires acc(&p.buffer, R50) && p.buffer.Mem() -// @ requires acc(&p.buffWithFullPerm) -// @ requires p.buffWithFullPerm +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.ingressID, R21) // @ requires acc(&p.hopField, R20) // @ requires acc(&p.infoField, R20) @@ -2209,7 +2201,6 @@ func (p *scionPacketProcessor) validateHopExpiry( /*@ ghost ubScionL []byte, gho // @ ubScionL === ubLL // @ ensures acc(&p.d, R50) // @ ensures acc(&p.path, R20) -// @ ensures acc(&p.buffWithFullPerm) // @ ensures acc(&p.infoField, R20) // @ ensures acc(&p.hopField, R20) // @ ensures acc(&p.ingressID, R21) @@ -2220,13 +2211,10 @@ func (p *scionPacketProcessor) validateHopExpiry( /*@ ghost ubScionL []byte, gho // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) // @ ensures sl.Bytes(ubScionL, 0, len(ubScionL)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) -// @ ensures respr === processResult{} ==> -// @ p.buffer.Mem() && p.buffWithFullPerm +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && -// @ !p.buffWithFullPerm && -// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -2278,9 +2266,8 @@ func (p *scionPacketProcessor) validateIngressID( /*@ ghost ubScionL []byte, gho // @ requires acc(p.scionLayer.Mem(ubScionL), R2) // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires p.path == p.scionLayer.GetPath(ubScionL) -// @ requires acc(&p.buffer, R50) && p.buffer.Mem() -// @ requires acc(&p.buffWithFullPerm) -// @ requires p.buffWithFullPerm +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ preserves acc(&p.ingressID, R21) // @ preserves ubLL == nil || ubLL === ubScionL[startLL:endLL] @@ -2290,18 +2277,14 @@ func (p *scionPacketProcessor) validateIngressID( /*@ ghost ubScionL []byte, gho // @ preserves &p.scionLayer === p.lastLayer ==> // @ ubScionL === ubLL // @ ensures acc(p.scionLayer.Mem(ubScionL), R2) -// @ ensures acc(&p.buffWithFullPerm) // @ ensures acc(&p.path, R20) // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) // @ ensures sl.Bytes(ubScionL, 0, len(ubScionL)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) -// @ ensures respr === processResult{} ==> -// @ p.buffer.Mem() && p.buffWithFullPerm +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && -// @ !p.buffWithFullPerm && -// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -2381,9 +2364,8 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte, ghos // @ requires acc(p.scionLayer.Mem(ub), R3) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires p.path == p.scionLayer.GetPath(ub) -// @ requires acc(&p.buffer, R50) && p.buffer.Mem() -// @ requires acc(&p.buffWithFullPerm) -// @ requires p.buffWithFullPerm +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ preserves acc(&p.ingressID, R40) // @ preserves ubLL == nil || ubLL === ub[startLL:endLL] @@ -2394,17 +2376,13 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte, ghos // @ ub === ubLL // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) // @ ensures acc(&p.path, R20) -// @ ensures acc(&p.buffWithFullPerm) // @ ensures acc(p.scionLayer.Mem(ub), R3) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) -// @ ensures respr === processResult{} ==> -// @ p.buffer.Mem() && p.buffWithFullPerm +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && -// @ !p.buffWithFullPerm && -// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil && reserr.ErrorMem() // @ ensures respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isIO_val_Unsupported @@ -2436,9 +2414,8 @@ func (p *scionPacketProcessor) invalidSrcIA( // @ requires acc(p.scionLayer.Mem(ub), R3) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires p.path == p.scionLayer.GetPath(ub) -// @ requires acc(&p.buffer, R50) && p.buffer.Mem() -// @ requires acc(&p.buffWithFullPerm) -// @ requires p.buffWithFullPerm +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ preserves acc(&p.ingressID, R40) // @ preserves ubLL == nil || ubLL === ub[startLL:endLL] @@ -2449,17 +2426,13 @@ func (p *scionPacketProcessor) invalidSrcIA( // @ ub === ubLL // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) // @ ensures acc(&p.path, R20) -// @ ensures acc(&p.buffWithFullPerm) // @ ensures acc(p.scionLayer.Mem(ub), R3) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) -// @ ensures respr === processResult{} ==> -// @ p.buffer.Mem() && p.buffWithFullPerm +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && -// @ !p.buffWithFullPerm && -// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil && reserr.ErrorMem() // @ ensures respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isIO_val_Unsupported @@ -2556,9 +2529,8 @@ func (p *scionPacketProcessor) validateTransitUnderlaySrc( /*@ ghost ub []byte @ // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires p.path == p.scionLayer.GetPath(ubScionL) -// @ requires acc(&p.buffer, R50) && p.buffer.Mem() -// @ requires acc(&p.buffWithFullPerm) -// @ requires p.buffWithFullPerm +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.segmentChange, R20) // @ requires acc(&p.ingressID, R21) // @ requires acc(&p.infoField, R20) @@ -2573,19 +2545,15 @@ func (p *scionPacketProcessor) validateTransitUnderlaySrc( /*@ ghost ub []byte @ // @ ensures acc(&p.hopField, R20) // @ ensures acc(&p.ingressID, R21) // @ ensures acc(&p.segmentChange, R20) -// @ ensures acc(&p.buffWithFullPerm) // @ ensures acc(&p.path, R20) // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) // @ ensures sl.Bytes(ubScionL, 0, len(ubScionL)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) -// @ ensures respr === processResult{} ==> -// @ p.buffer.Mem() && p.buffWithFullPerm +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && -// @ !p.buffWithFullPerm && -// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -2805,10 +2773,10 @@ func (p *scionPacketProcessor) updateNonConsDirIngressSegID( /*@ ghost ub []byte } // @ requires acc(p.scionLayer.Mem(ubScionL), R20) -// @ requires acc(&p.path, R20) +// @ requires acc(&p.path, R50) // @ requires p.path == p.scionLayer.GetPath(ubScionL) // @ ensures acc(p.scionLayer.Mem(ubScionL), R20) -// @ ensures acc(&p.path, R20) +// @ ensures acc(&p.path, R50) // @ decreases func (p *scionPacketProcessor) currentInfoPointer( /*@ ghost ubScionL []byte @*/ ) uint16 { // @ ghost ubPath := p.scionLayer.UBPath(ubScionL) @@ -2825,10 +2793,10 @@ func (p *scionPacketProcessor) currentInfoPointer( /*@ ghost ubScionL []byte @*/ // (VerifiedSCION) This could probably be made pure, but it is likely not beneficial, nor needed // to expose the body of this function at the moment. // @ requires acc(p.scionLayer.Mem(ubScionL), R20) -// @ requires acc(&p.path, R20) +// @ requires acc(&p.path, R50) // @ requires p.path == p.scionLayer.GetPath(ubScionL) // @ ensures acc(p.scionLayer.Mem(ubScionL), R20) -// @ ensures acc(&p.path, R20) +// @ ensures acc(&p.path, R50) // @ decreases func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ ) uint16 { // @ ghost ubPath := p.scionLayer.UBPath(ubScionL) @@ -2848,9 +2816,8 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ // @ requires acc(p.scionLayer.Mem(ubScionL), R3) // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires p.path == p.scionLayer.GetPath(ubScionL) -// @ requires acc(&p.buffer, R50) && p.buffer.Mem() -// @ requires acc(&p.buffWithFullPerm) -// @ requires p.buffWithFullPerm +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ preserves acc(&p.ingressID, R21) // @ requires acc(&p.infoField, R20) @@ -2869,17 +2836,13 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ // @ ensures acc(&p.infoField, R20) // @ ensures acc(&p.hopField, R20) // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) -// @ ensures acc(&p.buffWithFullPerm) // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) // @ ensures sl.Bytes(ubScionL, 0, len(ubScionL)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) -// @ ensures respr === processResult{} ==> -// @ p.buffer.Mem() && p.buffWithFullPerm +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && -// @ !p.buffWithFullPerm && -// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -2917,11 +2880,6 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, // @ defer fold acc(p.path.Mem(ubPath), R14) // @ unfold acc(p.path.Base.Mem(), R15) // @ defer fold acc(p.path.Base.Mem(), R15) - // (VerifiedSCION) Gobra is unable to verify permissions for `p.path.PathMeta.CurrINF` - // and `p.path.PathMeta.CurrHF` directly at the function call. - // To work around this limitation, these fields are first stored in temporary variables. - tmpCurrINF := p.path.PathMeta.CurrINF - tmpCurrHF := p.path.PathMeta.CurrHF tmpRes, tmpErr := p.packSCMP( slayers.SCMPTypeParameterProblem, @@ -2931,8 +2889,8 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, "%x", fullMac[:path.MacLen]), "actual", fmt.Sprintf("%x", p.hopField.Mac[:path.MacLen]), "cons_dir", p.infoField.ConsDir, - "if_id", p.ingressID, "curr_inf", tmpCurrINF, - "curr_hf", tmpCurrHF, "seg_id", p.infoField.SegID), + "if_id", p.ingressID, "curr_inf", p.path.PathMeta.CurrINF, + "curr_hf", p.path.PathMeta.CurrHF, "seg_id", p.infoField.SegID), /*@ ubScionL, ubLL, startLL, endLL, @*/ ) // @ ghost if tmpErr != nil && tmpRes.OutPkt != nil { @@ -2960,9 +2918,8 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, // @ requires acc(p.scionLayer.Mem(ubScionL), R3) // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires p.path == p.scionLayer.GetPath(ubScionL) -// @ requires acc(&p.buffer, R50) && p.buffer.Mem() -// @ requires acc(&p.buffWithFullPerm) -// @ requires p.buffWithFullPerm +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R15) && acc(p.d.Mem(), _) // pres for IO: // @ requires slayers.ValidPktMetaHdr(ubScionL) && p.scionLayer.EqAbsHeader(ubScionL) @@ -2984,16 +2941,12 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, // @ ensures addrAliasesUb ==> (acc(resaddr.Mem(), R15) --* acc(sl.Bytes(ubScionL, 0, len(ubScionL)), R15)) // @ ensures reserr != nil ==> !addrAliasesUb // @ ensures acc(&p.path, R20) -// @ ensures acc(&p.buffWithFullPerm) // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) // @ ensures acc(sl.Bytes(ubScionL, 0, len(ubScionL)), 1-R15) -// @ ensures acc(&p.buffer, R50) -// @ ensures respr === processResult{} ==> -// @ p.buffer.Mem() && p.buffWithFullPerm +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && -// @ !p.buffWithFullPerm && -// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -3301,10 +3254,9 @@ func (p *scionPacketProcessor) egressInterface( /*@ ghost oldPkt io.IO_pkt2 @*/ // @ requires acc(p.scionLayer.Mem(ub), R2) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires p.path == p.scionLayer.GetPath(ub) -// @ requires acc(&p.buffer, R50) && p.buffer.Mem() -// @ requires acc(&p.buffWithFullPerm) +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) -// @ requires p.buffWithFullPerm // @ requires acc(&p.infoField, R20) // @ requires acc(&p.hopField, R20) // @ requires acc(&p.ingressID, R21) @@ -3324,17 +3276,13 @@ func (p *scionPacketProcessor) egressInterface( /*@ ghost oldPkt io.IO_pkt2 @*/ // @ ensures acc(&p.ingressID, R21) // @ ensures acc(&p.path, R20) // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) -// @ ensures acc(&p.buffWithFullPerm) // @ ensures acc(p.scionLayer.Mem(ub), R2) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) -// @ ensures respr === processResult{} ==> -// @ p.buffer.Mem() && p.buffWithFullPerm +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && -// @ !p.buffWithFullPerm && -// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -3390,9 +3338,8 @@ func (p *scionPacketProcessor) validateEgressUp( // @ requires acc(p.scionLayer.Mem(ub), R3) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires p.path == p.scionLayer.GetPath(ub) -// @ requires acc(&p.buffer, R50) && p.buffer.Mem() -// @ requires acc(&p.buffWithFullPerm) -// @ requires p.buffWithFullPerm +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires acc(&p.ingressID, R21) // @ requires acc(&p.infoField, R20) @@ -3412,17 +3359,13 @@ func (p *scionPacketProcessor) validateEgressUp( // @ ensures acc(&p.infoField, R20) // @ ensures acc(&p.hopField) // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) -// @ ensures acc(&p.buffWithFullPerm) // @ ensures acc(p.scionLayer.Mem(ub), R3) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) -// @ ensures respr === processResult{} ==> -// @ p.buffer.Mem() && p.buffWithFullPerm +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && -// @ !p.buffWithFullPerm && -// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -3510,9 +3453,8 @@ func (p *scionPacketProcessor) ingressRouterAlertFlag() (res *bool) { // @ requires acc(p.scionLayer.Mem(ub), R3) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires p.path == p.scionLayer.GetPath(ub) -// @ requires acc(&p.buffer, R50) && p.buffer.Mem() -// @ requires acc(&p.buffWithFullPerm) -// @ requires p.buffWithFullPerm +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires acc(&p.ingressID, R21) // @ requires acc(&p.infoField, R20) @@ -3532,17 +3474,13 @@ func (p *scionPacketProcessor) ingressRouterAlertFlag() (res *bool) { // @ ensures acc(&p.infoField, R20) // @ ensures acc(&p.hopField) // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) -// @ ensures acc(&p.buffWithFullPerm) // @ ensures acc(p.scionLayer.Mem(ub), R3) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) -// @ ensures respr === processResult{} ==> -// @ p.buffer.Mem() && p.buffWithFullPerm +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && -// @ !p.buffWithFullPerm && -// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -3631,9 +3569,8 @@ func (p *scionPacketProcessor) egressRouterAlertFlag() (res *bool) { // @ requires acc(p.scionLayer.Mem(ubScionL), R3) // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires p.path == p.scionLayer.GetPath(ubScionL) -// @ requires acc(&p.buffer, R50) && p.buffer.Mem() -// @ requires acc(&p.buffWithFullPerm) -// @ requires p.buffWithFullPerm +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires acc(&p.infoField, R20) // @ requires acc(&p.hopField, R20) @@ -3656,17 +3593,13 @@ func (p *scionPacketProcessor) egressRouterAlertFlag() (res *bool) { // @ ensures acc(&p.infoField, R20) // @ ensures acc(&p.hopField, R20) // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) -// @ ensures acc(&p.buffWithFullPerm) // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) // @ ensures sl.Bytes(ubScionL, 0, len(ubScionL)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) -// @ ensures respr === processResult{} ==> -// @ p.buffer.Mem() && p.buffWithFullPerm +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && -// @ !p.buffWithFullPerm && -// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -3762,9 +3695,8 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( // @ requires acc(p.scionLayer.Mem(ubScionL), R3) // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires p.path == p.scionLayer.GetPath(ubScionL) -// @ requires acc(&p.buffer, R50) && p.buffer.Mem() -// @ requires acc(&p.buffWithFullPerm) -// @ requires p.buffWithFullPerm +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ preserves acc(&p.ingressID, R20) // @ preserves ubLL == nil || ubLL === ubScionL[startLL:endLL] @@ -3775,17 +3707,13 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( // @ ubScionL === ubLL // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) // @ ensures acc(&p.path, R20) -// @ ensures acc(&p.buffWithFullPerm) // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) // @ ensures sl.Bytes(ubScionL, 0, len(ubScionL)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) -// @ ensures respr === processResult{} ==> -// @ p.buffer.Mem() && p.buffWithFullPerm +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && -// @ !p.buffWithFullPerm && -// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr == nil ==> // @ int(p.scionLayer.GetPayloadLen(ubScionL)) == len(p.scionLayer.GetPayload(ubScionL)) // @ ensures reserr != nil ==> reserr.ErrorMem() @@ -3834,7 +3762,7 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost // @ requires acc(&p.ingressID, R15) // @ requires acc(&p.segmentChange) && !p.segmentChange // @ requires acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() -// @ requires acc(&p.buffWithFullPerm) && p.buffWithFullPerm +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ preserves acc(&p.srcAddr, R10) && acc(p.srcAddr.Mem(), _) // @ preserves acc(&p.lastLayer, R10) // @ preserves p.lastLayer != nil @@ -3849,7 +3777,6 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost // @ preserves acc(&p.macBuffers.scionInput, R10) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) -// @ ensures acc(&p.buffWithFullPerm) // @ ensures acc(&p.segmentChange) // @ ensures acc(&p.ingressID, R15) // @ ensures acc(&p.d, R5) @@ -3861,16 +3788,12 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost // @ respr.OutAddr != nil && // @ (acc(respr.OutAddr.Mem(), R15) --* acc(sl.Bytes(ub, 0, len(ub)), R15))) // @ ensures !addrAliasesPkt ==> acc(sl.Bytes(ub, 0, len(ub)), R15) -// @ ensures respr.OutPkt !== ub && respr.OutPkt != nil ==> -// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) -// @ ensures acc(&p.buffer, R10) +// @ ensures acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() // @ ensures reserr == nil ==> p.scionLayer.Mem(ub) -// @ ensures reserr == nil ==> p.buffer.Mem() && p.buffWithFullPerm // @ ensures reserr != nil ==> p.scionLayer.NonInitMem() -// @ ensures reserr != nil && respr === processResult{} ==> -// @ p.buffer.Mem() && p.buffWithFullPerm -// @ ensures reserr != nil && respr !== processResult{} ==> -// @ !p.buffWithFullPerm && p.buffer.MemWithoutUBuf(respr.OutPkt) +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +// @ ensures respr.OutPkt != nil ==> +// @ (respr.OutPkt === ub || respr.OutPkt === p.buffer.UBuf()) // @ ensures reserr != nil ==> reserr.ErrorMem() // contracts for IO-spec // @ requires p.d.DpAgreesWithSpec(dp) @@ -4098,6 +4021,7 @@ func (p *scionPacketProcessor) process( // @ preserves acc(&p.macBuffers.scionInput, R10) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() +// @ preserves sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures acc(&p.rawPkt, R15) // @ ensures p.scionLayer.Mem(p.rawPkt) // @ ensures acc(&p.ingressID, R15) @@ -4109,8 +4033,7 @@ func (p *scionPacketProcessor) process( // @ let rawPkt := p.rawPkt in // @ (acc(respr.OutAddr.Mem(), R15) --* acc(sl.Bytes(rawPkt, 0, len(rawPkt)), R15))) // @ ensures !addrAliasesPkt ==> acc(sl.Bytes(p.rawPkt, 0, len(p.rawPkt)), R15) -// @ ensures respr.OutPkt !== p.rawPkt && respr.OutPkt != nil ==> -// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ ensures respr.OutPkt != nil ==> respr.OutPkt === p.rawPkt // @ ensures reserr != nil ==> reserr.ErrorMem() // contracts for IO-spec // @ requires p.scionLayer.EqPathType(p.rawPkt) @@ -4372,6 +4295,7 @@ func addEndhostPort(dst *net.IPAddr) (res *net.UDPAddr) { // @ requires s.HasOneHopPath(rawPkt) // @ requires sl.Bytes(rawPkt, 0, len(rawPkt)) // @ preserves buffer != nil && buffer.Mem() +// @ preserves sl.Bytes(buffer.UBuf(), 0, len(buffer.UBuf())) // pres for IO: // @ requires s.EqPathType(rawPkt) // @ requires !slayers.IsSupportedPkt(rawPkt) @@ -4409,7 +4333,6 @@ func updateSCIONLayer(rawPkt []byte, s *slayers.SCION, buffer gopacket.Serialize copy(rawPkt[:len(rawContents)], rawContents /*@ , R20 @*/) // @ fold sl.Bytes(rawPkt, 0, len(rawPkt)) // @ fold acc(sl.Bytes(rawContents, 0, len(rawContents)), R20) - // @ buffer.RestoreMem(rawContents) // @ assert !(reveal slayers.IsSupportedPkt(rawPkt)) return nil } @@ -4513,22 +4436,17 @@ func (b *bfdSend) Send(bfd *layers.BFD) error { // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires sl.Bytes(ub, 0, len(ub)) // @ requires acc(&p.ingressID, R50) -// @ requires acc(&p.buffer, R55) && p.buffer.Mem() -// @ requires acc(&p.buffWithFullPerm) -// @ requires p.buffWithFullPerm +// @ requires acc(&p.buffer, R55) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires cause != nil ==> cause.ErrorMem() -// @ ensures acc(&p.buffWithFullPerm) // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) // @ ensures acc(p.scionLayer.Mem(ub), R4) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures acc(&p.ingressID, R50) -// @ ensures acc(&p.buffer, R55) -// @ ensures result == nil ==> -// @ p.buffer.Mem() && p.buffWithFullPerm +// @ ensures acc(&p.buffer, R55) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures result != nil ==> -// @ p.buffer.MemWithoutUBuf(result) && -// @ !p.buffWithFullPerm && -// @ sl.Bytes(result, 0, len(result)) +// @ result === p.buffer.UBuf() // @ ensures reserr != nil && reserr.ErrorMem() // @ ensures result != nil ==> // @ !slayers.IsSupportedPkt(result) @@ -4707,7 +4625,6 @@ func (p *scionPacketProcessor) prepareSCMP( if err := p.buffer.Clear(); err != nil { return nil, err } - sopts := gopacket.SerializeOptions{ ComputeChecksums: true, FixLengths: true, @@ -4736,7 +4653,6 @@ func (p *scionPacketProcessor) prepareSCMP( if err != nil { return nil, serrors.Wrap(cannotRoute, err, "details", "serializing SCMP message") } - // @ p.buffWithFullPerm = false return p.buffer.Bytes(), scmpError{TypeCode: typeCode, Cause: cause} } diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra index f6ca68c9a..fd0d667ec 100644 --- a/router/dataplane_spec.gobra +++ b/router/dataplane_spec.gobra @@ -67,9 +67,10 @@ pred (d *DataPlane) Mem() { (d.internalNextHops != nil ==> accAddr(d.internalNextHops)) && (d.svc != nil ==> d.svc.Mem()) && (d.macFactory != nil ==> ( - acc(d.key) && - acc(sl.Bytes(*d.key, 0, len(*d.key)), _) && - scrypto.ValidKeyForHash(*d.key) && + acc(d.key) && + acc(sl.Bytes(*d.key, 0, len(*d.key)), _) && + len(*d.key) > 0 && + scrypto.ValidKeyForHash(*d.key) && d.macFactory implements MacFactorySpec{d.key})) && (d.bfdSessions != nil ==> accBfdSession(d.bfdSessions)) && (d.Metrics != nil ==> acc(d.Metrics.Mem(), _)) && @@ -129,7 +130,6 @@ func liftForwardingMetricsNonInjectiveMem(v forwardingMetrics, id uint16) { pred (p *scionPacketProcessor) initMem() { acc(&p.d) && acc(&p.ingressID) && - acc(&p.buffWithFullPerm) && acc(&p.buffer) && acc(&p.mac) && acc(p.scionLayer.NonInitMem()) && @@ -421,6 +421,7 @@ requires acc(d.Mem(), _) && d.getMacFactory() != nil ensures acc(&d.macFactory, _) && acc(&d.key, _) && acc(d.key, _) ensures acc(sl.Bytes(*d.key, 0, len(*d.key)), _) ensures scrypto.ValidKeyForHash(*d.key) +ensures len(*d.key) > 0 ensures d.macFactory implements MacFactorySpec{d.key} decreases func (d *DataPlane) getNewPacketProcessorFootprint() { @@ -567,8 +568,7 @@ pred (s* scionPacketProcessor) sInit() { acc(&s.d) && acc(&s.ingressID) && acc(&s.buffer) && s.buffer != nil && - acc(&s.buffWithFullPerm) && - (s.buffWithFullPerm ==> s.buffer.Mem()) && + s.buffer.Mem() && acc(&s.mac) && s.mac != nil && s.mac.Mem() && s.scionLayer.NonInitMem() && // The following is not necessary @@ -635,16 +635,8 @@ pure func (s* scionPacketProcessor) sInitSegmentChange() (res bool) { ghost requires acc(s.sInit(), _) decreases -pure func (s* scionPacketProcessor) sInitBuffWithFullPerm() (res bool) { - return unfolding acc(s.sInit(), _) in s.buffWithFullPerm -} - -ghost -requires acc(s.sInit(), _) -ensures res != nil -decreases -pure func (s* scionPacketProcessor) sInitBuffer() (res gopacket.SerializeBuffer) { - return unfolding acc(s.sInit(), _) in s.buffer +pure func (s* scionPacketProcessor) sInitBufferUBuf() (res []byte) { + return unfolding acc(s.sInit(), _) in s.buffer.UBuf() } /** end spec for newPacketProcessor **/ diff --git a/router/dataplane_spec_test.gobra b/router/dataplane_spec_test.gobra index 433b3bd86..1f33af4a7 100644 --- a/router/dataplane_spec_test.gobra +++ b/router/dataplane_spec_test.gobra @@ -82,7 +82,8 @@ func canModifyRunning(d *DataPlane) { requires macFactory != nil && acc(key) && - acc(sl.Bytes(*key, 0, len(*key)), _) && + len(*key) > 0 && + acc(sl.Bytes(*key, 0, len(*key)), _) && scrypto.ValidKeyForHash(*key) && macFactory implements MacFactorySpec{key} requires metrics != nil && metrics.Mem() diff --git a/router/io-spec.gobra b/router/io-spec.gobra index 8fb6b9023..d1afe6f3c 100644 --- a/router/io-spec.gobra +++ b/router/io-spec.gobra @@ -199,6 +199,7 @@ func (d *DataPlane) getDomExternalLemma() { ghost requires acc(msg.Mem(), R50) +requires acc(sl.Bytes(msg.GetFstBuffer(), 0, len(msg.GetFstBuffer())), R50) decreases pure func MsgToAbsVal(msg *ipv4.Message, ingressID uint16) (res io.IO_val) { return unfolding acc(msg.Mem(), R50) in diff --git a/verification/dependencies/github.com/google/gopacket/base.gobra b/verification/dependencies/github.com/google/gopacket/base.gobra index 9c0ae5c81..084b6800a 100644 --- a/verification/dependencies/github.com/google/gopacket/base.gobra +++ b/verification/dependencies/github.com/google/gopacket/base.gobra @@ -66,7 +66,9 @@ func (p Payload) Payload(ghost ub []byte) (res []byte, ghost start int, ghost en requires b != nil && b.Mem() requires p.Mem(ubuf) +requires slices.Bytes(b.UBuf(), 0, len(b.UBuf())) ensures err == nil ==> (p.Mem(ubuf) && b.Mem()) +ensures err == nil ==> slices.Bytes(b.UBuf(), 0, len(b.UBuf())) ensures err != nil ==> err.ErrorMem() decreases func (p Payload) SerializeTo(b SerializeBuffer, opts SerializeOptions, ghost ubuf []byte) (err error) diff --git a/verification/dependencies/github.com/google/gopacket/layers/bfd.gobra b/verification/dependencies/github.com/google/gopacket/layers/bfd.gobra index 743d748e4..14214df43 100644 --- a/verification/dependencies/github.com/google/gopacket/layers/bfd.gobra +++ b/verification/dependencies/github.com/google/gopacket/layers/bfd.gobra @@ -191,8 +191,11 @@ ensures err != nil ==> err.ErrorMem() && d.NonInitMem() decreases func (d *BFD) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback) (err error) -requires d.Mem(ub) && b.Mem() +requires d.Mem(ub) +requires b != nil && b.Mem() +requires sl.Bytes(b.UBuf(), 0, len(b.UBuf())) ensures err == nil ==> d.Mem(ub) && b.Mem() +ensures err == nil ==> sl.Bytes(b.UBuf(), 0, len(b.UBuf())) ensures err != nil ==> err.ErrorMem() decreases func (d *BFD) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOptions, ghost ub []byte) (err error) diff --git a/verification/dependencies/github.com/google/gopacket/writer.gobra b/verification/dependencies/github.com/google/gopacket/writer.gobra index 413e26b8b..9c8f84252 100644 --- a/verification/dependencies/github.com/google/gopacket/writer.gobra +++ b/verification/dependencies/github.com/google/gopacket/writer.gobra @@ -17,9 +17,11 @@ type SerializableLayer interface { requires !opts.FixLengths requires b != nil && b.Mem() + requires sl.Bytes(b.UBuf(), 0, len(b.UBuf())) requires Mem(ubuf) preserves sl.Bytes(ubuf, 0, len(ubuf)) ensures err == nil ==> (Mem(ubuf) && b.Mem()) + ensures err == nil ==> sl.Bytes(b.UBuf(), 0, len(b.UBuf())) ensures err != nil ==> err.ErrorMem() decreases SerializeTo(b SerializeBuffer, opts SerializeOptions, ghost ubuf []byte) (err error) @@ -36,8 +38,6 @@ type SerializeOptions struct { type SerializeBuffer interface { pred Mem() - // morally, corresponds to sl.Bytes(ub, 0, len(ub)) --* (Mem() && UBuf() === ub) - pred MemWithoutUBuf(ub []byte) ghost pure @@ -48,39 +48,23 @@ type SerializeBuffer interface { ghost pure requires acc(Mem(), _) + requires acc(sl.Bytes(UBuf(), 0, len(UBuf())), _) + ensures res == seqs.ToSeqByte(UBuf()) decreases View() (ghost res seq[byte]) - ghost - requires Mem() - ensures res === old(UBuf()) - ensures sl.Bytes(res, 0, len(res)) - ensures MemWithoutUBuf(res) - ensures old(View()) == seqs.ToSeqByte(res) - decreases - ExchangePred() (res []byte) - - ghost - requires MemWithoutUBuf(ub) - requires sl.Bytes(ub, 0, len(ub)) - ensures Mem() && UBuf() === ub - ensures View() == old(seqs.ToSeqByte(ub)) - decreases - RestoreMem(ghost ub []byte) - - requires Mem() - ensures res === old(UBuf()) - ensures sl.Bytes(res, 0, len(res)) - ensures MemWithoutUBuf(res) - ensures old(View()) == seqs.ToSeqByte(res) + preserves acc(Mem(), R50) + ensures res === UBuf() decreases Bytes() (res []byte) preserves Mem() requires num >= 0 + preserves sl.Bytes(UBuf(), 0, len(UBuf())) ensures err == nil ==> len(UBuf()) == len(old(UBuf())) + num ensures err == nil ==> len(res) == num - ensures err == nil ==> res === (UBuf())[:num] + ensures err == nil ==> res === UBuf()[:num] + ensures err == nil ==> old(View()) == View()[num:] ensures err != nil ==> UBuf() === old(UBuf()) ensures err != nil ==> err.ErrorMem() decreases @@ -88,31 +72,33 @@ type SerializeBuffer interface { preserves Mem() requires num >= 0 + preserves sl.Bytes(UBuf(), 0, len(UBuf())) ensures err == nil ==> len(UBuf()) == len(old(UBuf())) + num ensures err == nil ==> len(res) == num - ensures err == nil ==> res === (UBuf())[len(UBuf()) - num:] + ensures err == nil ==> res === UBuf()[len(UBuf()) - num:] ensures err != nil ==> UBuf() === old(UBuf()) ensures err != nil ==> err.ErrorMem() decreases AppendBytes(num int) (res []byte, err error) preserves Mem() + preserves sl.Bytes(UBuf(), 0, len(UBuf())) ensures err != nil ==> err.ErrorMem() ensures err == nil ==> len(UBuf()) == 0 decreases Clear() (err error) - preserves Mem() - ensures forall i int :: {&res[i]} 0 <= i && i < len(res) ==> acc(&res[i]) + requires false decreases Layers() (res []LayerType) - preserves Mem() + requires false decreases PushLayer(LayerType) } ensures res != nil && res.Mem() +ensures sl.Bytes(res.UBuf(), 0, len(res.UBuf())) decreases func NewSerializeBuffer() (res SerializeBuffer) diff --git a/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra b/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra index b985da7b2..1684e668a 100644 --- a/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra +++ b/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra @@ -14,8 +14,8 @@ package socket import ( "net" - - sl "github.com/scionproto/scion/verification/utils/slices" + . "verification/utils/definitions" + sl "verification/utils/slices" ) @@ -52,7 +52,6 @@ pred (m *Message) Mem() { acc(m) && len(m.Buffers) == 1 && acc(&m.Buffers[0]) && - sl.Bytes(m.Buffers[0], 0, len(m.Buffers[0])) && sl.Bytes(m.OOB, 0, len(m.OOB)) && // typeOf(m.Addr) == type[*net.UDPAddr] && ((m.Addr != nil && m.IsActive && !m.WildcardPerm) ==> m.Addr.Mem()) && @@ -110,3 +109,49 @@ decreases pure func (m *Message) GetN() (res int) { return unfolding acc(m.Mem(), _) in m.N } + +// This function establishes the injectivity of the underlying buffers across +// a list of messages. Specifically, it ensures that for any given message `m` +// and any message in the list `msgs` up to index `k`, their buffers are not +// pointing to the same memory location. +// +// The challenge arises when initializing buffers for each message in `msgs`, +// as Gobra cannot automatically infer that these buffers are located in distinct +// memory regions. Consequently, the property +// `forall i int :: 0 <= i && i <= k ==> msgs[i].GetFstBuffer() !== m.GetFstBuffer()` +// does not hold automatically. To address this, the function uses a proof by +// recursion, ensuring that the buffer of a new message `m` is distinct from the +// buffers of all messages in the list. +ghost +requires 0 <= k && k < len(msgs) +preserves acc(m.Mem(), R55) +preserves len(m.GetFstBuffer()) > 0 +preserves sl.Bytes(m.GetFstBuffer(), 0, len(m.GetFstBuffer())) +preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(msgs[i].Mem(), R55) +preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> + acc(sl.Bytes(msgs[i].GetFstBuffer(), 0, len(msgs[i].GetFstBuffer())), R55) +ensures forall i int :: { &msgs[i] } 0 <= i && i <= k ==> + msgs[i].GetFstBuffer() !== m.GetFstBuffer() +decreases k +func (m *Message) ensureBufferInjectivityAgainstList(msgs []Message, k int) { + if k != 0 { + m.ensureBufferInjectivityAgainstList(msgs, k-1) + } + sl.PermsImplyIneq(m.GetFstBuffer(), msgs[k].GetFstBuffer(), R55) +} + +ghost +preserves acc(m.Mem(), R55) +preserves len(m.GetFstBuffer()) > 0 +preserves sl.Bytes(m.GetFstBuffer(), 0, len(m.GetFstBuffer())) +preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(msgs[i].Mem(), R55) +preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> + acc(sl.Bytes(msgs[i].GetFstBuffer(), 0, len(msgs[i].GetFstBuffer())), R55) +ensures forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> + msgs[i].GetFstBuffer() !== m.GetFstBuffer() +decreases +func (m *Message) EnsureBufferInjectivityAgainstList(msgs []Message) { + if len(msgs) != 0 { + m.ensureBufferInjectivityAgainstList(msgs, len(msgs)-1) + } +} \ No newline at end of file diff --git a/verification/utils/slices/slices.gobra b/verification/utils/slices/slices.gobra index d44e840b0..8c7c4ac15 100644 --- a/verification/utils/slices/slices.gobra +++ b/verification/utils/slices/slices.gobra @@ -141,6 +141,45 @@ func NilAcc_Bytes() { fold Bytes(nil, 0, 0) } +ghost +requires len(s1) > 0 || len(s2) > 0 +preserves Bytes(s1, 0, len(s1)) +preserves acc(Bytes(s2, 0, len(s2)), _) +ensures s1 !== s2 +decreases +func PermsImplyIneqWithWildcard(s1 []byte, s2 []byte) { + unfold Bytes(s1, 0, len(s1)) + unfold acc(Bytes(s2, 0, len(s2)), _) + if len(s1) > 0 && len(s2) > 0 { + // This assertion checks that the memory addresses of the first elements + // in s1 and s2 are different. By doing so, we instantiate the triggers in + // the quantifier bodies to prove the required inequality for non-empty slices. + assert &s1[0] != &s2[0] + } + fold Bytes(s1, 0, len(s1)) + fold acc(Bytes(s2, 0, len(s2)), _) +} + +ghost +requires 0 < p +requires len(s1) > 0 || len(s2) > 0 +preserves Bytes(s1, 0, len(s1)) +preserves acc(Bytes(s2, 0, len(s2)), p) +ensures s1 !== s2 +decreases +func PermsImplyIneq(s1 []byte, s2 []byte, p perm) { + unfold Bytes(s1, 0, len(s1)) + unfold acc(Bytes(s2, 0, len(s2)), p) + if len(s1) > 0 && len(s2) > 0 { + // This assertion checks that the memory addresses of the first elements + // in s1 and s2 are different. By doing so, we instantiate the triggers in + // the quantifier bodies to prove the required inequality for non-empty slices. + assert &s1[0] != &s2[0] + } + fold Bytes(s1, 0, len(s1)) + fold acc(Bytes(s2, 0, len(s2)), p) +} + /** Auxiliar definitions Any **/ ghost requires size >= 0