Move ownership of underlying slice of SerializableBuffer to outside of Mem()

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
 }

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,59 +130,37 @@ 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 {
  // @ fold s.Mem(ubufMem)
  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]
  bytes[2] = 0
  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]
  // @ assert forall i int :: { &bytes[2:][i] } 0 <= i && i < 2 ==> &bytes[2:][i] == &bytes[i + 2]
  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
 }