Merge branch 'master' into simplify-segLen

viperproject · Jun 13, 2024 · 46d500b · 46d500b
2 parents 2d12d17 + b10cb4c
commit 46d500b
Show file tree

Hide file tree

Showing 4 changed files with 76 additions and 86 deletions.
diff --git a/pkg/experimental/epic/epic.go b/pkg/experimental/epic/epic.go
@@ -48,13 +48,11 @@ const (
 
 var zeroInitVector /*@@@*/ [16]byte
 
-/*@
 // ghost init
-func init() {
-	fold acc(sl.Bytes(zeroInitVector[:], 0, len(zeroInitVector[:])), _)
-	fold acc(postInitInvariant(), _)
-}
-@*/
+// @ func init() {
+// @ 	fold acc(sl.Bytes(zeroInitVector[:], 0, len(zeroInitVector[:])), _)
+// @ 	fold acc(postInitInvariant(), _)
+// @ }
 
 // CreateTimestamp returns the epic timestamp, which encodes the current time (now) relative to the
 // input timestamp. The input timestamp must not be in the future (compared to the current time),

diff --git a/pkg/slayers/scion.go b/pkg/slayers/scion.go
@@ -835,20 +835,18 @@ func packAddr(hostAddr net.Addr /*@ , ghost wildcard bool @*/) (addrtyp AddrType
 // @ ensures   0 <= res
 // @ decreases
 func (s *SCION) AddrHdrLen( /*@ ghost ubuf []byte, ghost insideSlayers bool @*/ ) (res int) {
-	/*@
-	ghost if !insideSlayers {
-		unfold acc(s.Mem(ubuf), R51)
-		defer fold acc(s.Mem(ubuf), R51)
-		unfold acc(s.HeaderMem(ubuf[CmnHdrLen:]), R51)
-		defer fold acc(s.HeaderMem(ubuf[CmnHdrLen:]), R51)
-		assert s.AddrHdrLenSpec(ubuf) == (
-			unfolding acc(s.Mem(ubuf), R52) in
-			unfolding acc(s.HeaderMem(ubuf[CmnHdrLen:]), R52) in
-			2*addr.IABytes + s.DstAddrType.Length() + s.SrcAddrType.Length())
-		assert s.AddrHdrLenSpec(ubuf) ==
-			2*addr.IABytes + s.DstAddrType.Length() + s.SrcAddrType.Length()
-	}
-	@*/
+	// @ ghost if !insideSlayers {
+	// @ 	unfold acc(s.Mem(ubuf), R51)
+	// @ 	defer fold acc(s.Mem(ubuf), R51)
+	// @ 	unfold acc(s.HeaderMem(ubuf[CmnHdrLen:]), R51)
+	// @ 	defer fold acc(s.HeaderMem(ubuf[CmnHdrLen:]), R51)
+	// @ 	assert s.AddrHdrLenSpec(ubuf) == (
+	// @ 		unfolding acc(s.Mem(ubuf), R52) in
+	// @ 		unfolding acc(s.HeaderMem(ubuf[CmnHdrLen:]), R52) in
+	// @ 		2*addr.IABytes + s.DstAddrType.Length() + s.SrcAddrType.Length())
+	// @ 	assert s.AddrHdrLenSpec(ubuf) ==
+	// @ 		2*addr.IABytes + s.DstAddrType.Length() + s.SrcAddrType.Length()
+	// @ }
 	return 2*addr.IABytes + s.DstAddrType.Length() + s.SrcAddrType.Length()
 }
 

diff --git a/private/underlay/conn/conn.go b/private/underlay/conn/conn.go
@@ -125,13 +125,11 @@ func New(listen, remote *net.UDPAddr, cfg *Config) (res Conn, e error) {
 	if listen == nil && remote == nil {
 		panic("either listen or remote must be set")
 	}
-	/*@
-	assert remote != nil ==> a == remote
-	assert remote == nil ==> a == listen
-	unfold acc(a.Mem(), R15)
-	unfold acc(sl.Bytes(a.IP, 0, len(a.IP)), R15)
-	assert forall i int :: { &a.IP[i] } 0 <= i && i < len(a.IP) ==> acc(&a.IP[i], R15)
-	@*/
+	// @ assert remote != nil ==> a == remote
+	// @ assert remote == nil ==> a == listen
+	// @ unfold acc(a.Mem(), R15)
+	// @ unfold acc(sl.Bytes(a.IP, 0, len(a.IP)), R15)
+	// @ assert forall i int :: { &a.IP[i] } 0 <= i && i < len(a.IP) ==> acc(&a.IP[i], R15)
 	if a.IP.To4( /*@ false @*/ ) != nil {
 		return newConnUDPIPv4(listen, remote, cfg)
 	}

diff --git a/router/dataplane.go b/router/dataplane.go
@@ -1487,39 +1487,37 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte,
 		// @ fold p.sInitD().validResult(processResult{}, false)
 		return processResult{}, err /*@, false, io.IO_val_Unit{} @*/
 	}
-	/*@
-	ghost var ub []byte
-	ghost var ubScionLayer []byte = p.rawPkt
-	ghost var ubHbhLayer []byte
-	ghost var ubE2eLayer []byte
-
-	ghost llStart := 0
-	ghost llEnd := 0
-	ghost mustCombineRanges := lastLayerIdx != -1 && !offsets[lastLayerIdx].isNil
-	ghost var o offsetPair
-	ghost if lastLayerIdx == -1 {
-		ub = p.rawPkt
-	} else {
-		if offsets[lastLayerIdx].isNil {
-			ub = nil
-			sl.NilAcc_Bytes()
-		} else {
-			o = offsets[lastLayerIdx]
-			ub = p.rawPkt[o.start:o.end]
-			llStart = o.start
-			llEnd = o.end
-			sl.SplitRange_Bytes(p.rawPkt, o.start, o.end, HalfPerm)
-		}
-	}
-	hasHbhLayer := processed[0]
-	oHbh := offsets[0]
-	ubHbhLayer = hasHbhLayer && !oHbh.isNil ? p.rawPkt[oHbh.start:oHbh.end] : ([]byte)(nil)
-	hasE2eLayer := processed[1]
-	oE2e := offsets[1]
-	ubE2eLayer = hasE2eLayer && !oE2e.isNil ? p.rawPkt[oE2e.start:oE2e.end] : ([]byte)(nil)
-	assert processed[0] ==> p.hbhLayer.Mem(ubHbhLayer)
-	assert processed[1] ==> p.e2eLayer.Mem(ubE2eLayer)
-	@*/
+	// @ ghost var ub []byte
+	// @ ghost var ubScionLayer []byte = p.rawPkt
+	// @ ghost var ubHbhLayer []byte
+	// @ ghost var ubE2eLayer []byte
+
+	// @ ghost llStart := 0
+	// @ ghost llEnd := 0
+	// @ ghost mustCombineRanges := lastLayerIdx != -1 && !offsets[lastLayerIdx].isNil
+	// @ ghost var o offsetPair
+	// @ ghost if lastLayerIdx == -1 {
+	// @ 	ub = p.rawPkt
+	// @ } else {
+	// @ 	if offsets[lastLayerIdx].isNil {
+	// @ 		ub = nil
+	// @ 		sl.NilAcc_Bytes()
+	// @ 	} else {
+	// @ 		o = offsets[lastLayerIdx]
+	// @ 		ub = p.rawPkt[o.start:o.end]
+	// @ 		llStart = o.start
+	// @ 		llEnd = o.end
+	// @ 		sl.SplitRange_Bytes(p.rawPkt, o.start, o.end, HalfPerm)
+	// @ 	}
+	// @ }
+	// @ hasHbhLayer := processed[0]
+	// @ oHbh := offsets[0]
+	// @ ubHbhLayer = hasHbhLayer && !oHbh.isNil ? p.rawPkt[oHbh.start:oHbh.end] : ([]byte)(nil)
+	// @ hasE2eLayer := processed[1]
+	// @ oE2e := offsets[1]
+	// @ ubE2eLayer = hasE2eLayer && !oE2e.isNil ? p.rawPkt[oE2e.start:oE2e.end] : ([]byte)(nil)
+	// @ assert processed[0] ==> p.hbhLayer.Mem(ubHbhLayer)
+	// @ assert processed[1] ==> p.e2eLayer.Mem(ubE2eLayer)
 	// @ assert acc(sl.Bytes(ub, 0, len(ub)), HalfPerm)
 	pld /*@ , start, end @*/ := p.lastLayer.LayerPayload( /*@ ub @*/ )
 	// @ sl.SplitRange_Bytes(ub, start, end, HalfPerm)
@@ -2921,19 +2919,18 @@ func (p *scionPacketProcessor) handleIngressRouterAlert( /*@ ghost ub []byte, gh
 	// @ assert slayers.ValidPktMetaHdr(ub)
 	// @ assert reveal p.LastHopLen(ub)
 	// @ assert p.scionLayer.EqAbsHeader(ub)
-	/*@
-	ghost var ubLL []byte
-	ghost if &p.scionLayer === p.lastLayer {
-		ubLL = ub
-	} else if llIsNil {
-		ubLL = nil
-		sl.NilAcc_Bytes()
-	} else {
-		ubLL = ub[startLL:endLL]
-		sl.SplitRange_Bytes(ub, startLL, endLL, R1)
-		ghost defer sl.CombineRange_Bytes(ub, startLL, endLL, R1)
-	}
-	@*/
+
+	// @ ghost var ubLL []byte
+	// @ ghost if &p.scionLayer === p.lastLayer {
+	// @ 	ubLL = ub
+	// @ } else if llIsNil {
+	// @ 	ubLL = nil
+	// @ 	sl.NilAcc_Bytes()
+	// @ } else {
+	// @ 	ubLL = ub[startLL:endLL]
+	// @ 	sl.SplitRange_Bytes(ub, startLL, endLL, R1)
+	// @ 	ghost defer sl.CombineRange_Bytes(ub, startLL, endLL, R1)
+	// @ }
 	return p.handleSCMPTraceRouteRequest(p.ingressID /*@, ubLL @*/)
 }
 
@@ -3027,19 +3024,18 @@ func (p *scionPacketProcessor) handleEgressRouterAlert( /*@ ghost ub []byte, gho
 	// @ TemporaryAssumeForIO(p.EqAbsInfoField(absPkt(ub)))
 	// @ sl.CombineRange_Bytes(ub, startP, endP, HalfPerm)
 	// @ TemporaryAssumeForIO(absPkt(ub) == old(absPkt(ub)))
-	/*@
-	ghost var ubLL []byte
-	ghost if &p.scionLayer === p.lastLayer {
-		ubLL = ub
-	} else if llIsNil {
-		ubLL = nil
-		sl.NilAcc_Bytes()
-	} else {
-		ubLL = ub[startLL:endLL]
-		sl.SplitRange_Bytes(ub, startLL, endLL, R1)
-		ghost defer sl.CombineRange_Bytes(ub, startLL, endLL, R1)
-	}
-	@*/
+
+	// @ ghost var ubLL []byte
+	// @ ghost if &p.scionLayer === p.lastLayer {
+	// @ 	ubLL = ub
+	// @ } else if llIsNil {
+	// @ 	ubLL = nil
+	// @ 	sl.NilAcc_Bytes()
+	// @ } else {
+	// @ 	ubLL = ub[startLL:endLL]
+	// @ 	sl.SplitRange_Bytes(ub, startLL, endLL, R1)
+	// @ 	ghost defer sl.CombineRange_Bytes(ub, startLL, endLL, R1)
+	// @ }
 	return p.handleSCMPTraceRouteRequest(egressID /*@, ubLL@*/)
 }