From c4042f18c1aaa86eec7cac2429f6e622cab40bcd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 26 Jan 2024 15:08:04 +0100 Subject: [PATCH 01/31] start --- router/dataplane.go | 1 - 1 file changed, 1 deletion(-) diff --git a/router/dataplane.go b/router/dataplane.go index 74e16f30f..f7d305669 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1552,7 +1552,6 @@ type macBuffersT struct { epicInput []byte } -// @ trusted // @ requires false func (p *scionPacketProcessor) packSCMP( typ slayers.SCMPType, From e308b68627097b29370df4877f845225967b50fb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 26 Jan 2024 15:34:28 +0100 Subject: [PATCH 02/31] make type-check --- router/dataplane.go | 55 +++++++++++++++++++++++++++++++++++---------- 1 file changed, 43 insertions(+), 12 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index f7d305669..e85ee31cd 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1552,18 +1552,37 @@ type macBuffersT struct { epicInput []byte } -// @ requires false +// @ requires acc(&p.d, _) && acc(MutexInvariant(p.d), _) +// @ requires acc(p.scionLayer.Mem(ub), R4) +// @ requires p.scionLayer.ValidPathMetaData(ub) +// @ requires sl.AbsSlice_Bytes(ub, 0, len(ub)) +// @ requires acc(&p.ingressID, R15) +// @ requires acc(&p.buffer, R50) && p.buffer.Mem() +// @ ensures acc(&p.d, _) +// @ ensures acc(p.scionLayer.Mem(ub), R4) +// @ ensures sl.AbsSlice_Bytes(ub, 0, len(ub)) +// @ ensures acc(&p.ingressID, R15) +// @ ensures p.d.validResult(respr, false) +// @ ensures acc(&p.buffer, R50) +// @ ensures respr === processResult{} ==> +// @ p.buffer.Mem() +// @ ensures respr !== processResult{} ==> +// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && +// @ sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ ensures reserr != nil ==> reserr.ErrorMem() +// @ decreases func (p *scionPacketProcessor) packSCMP( typ slayers.SCMPType, code slayers.SCMPCode, scmpP gopacket.SerializableLayer, cause error, -) (processResult, error) { - + // @ ghost ub []byte, +) (respr processResult, reserr error) { // check invoking packet was an SCMP error: - if p.lastLayer.NextLayerType() == slayers.LayerTypeSCMP { - var scmpLayer slayers.SCMP - err := scmpLayer.DecodeFromBytes(p.lastLayer.LayerPayload(), gopacket.NilDecodeFeedback) + if p.lastLayer.NextLayerType( /*@ nil @*/ ) == slayers.LayerTypeSCMP { + var scmpLayer /*@@@*/ slayers.SCMP + pld /*@ , start, end @*/ := p.lastLayer.LayerPayload( /*@ nil @*/ ) + err := scmpLayer.DecodeFromBytes(pld, gopacket.NilDecodeFeedback) if err != nil { return processResult{}, serrors.WrapStr("decoding SCMP layer", err) } @@ -1572,7 +1591,7 @@ func (p *scionPacketProcessor) packSCMP( } } - rawSCMP, err := p.prepareSCMP(typ, code, scmpP, cause /*@ , nil @*/) // (VerifiedSCION) replace nil by sth else + rawSCMP, err := p.prepareSCMP(typ, code, scmpP, cause /*@ , nil @*/) return processResult{OutPkt: rawSCMP}, err } @@ -1656,6 +1675,7 @@ func (p *scionPacketProcessor) validateHopExpiry() (respr processResult, reserr &slayers.SCMPParameterProblem{Pointer: p.currentHopPointer( /*@ nil @*/ )}, serrors.New("expired hop", "cons_dir", p.infoField.ConsDir, "if_id", p.ingressID, "curr_inf", p.path.PathMeta.CurrINF, "curr_hf", p.path.PathMeta.CurrHF), + /*@ nil , @*/ ) } @@ -1686,6 +1706,7 @@ func (p *scionPacketProcessor) validateIngressID() (respr processResult, reserr &slayers.SCMPParameterProblem{Pointer: p.currentHopPointer( /*@ nil @*/ )}, serrors.New("ingress interface invalid", "pkt_ingress", pktIngressID, "router_ingress", p.ingressID), + /*@ nil , @*/ ) } // @ fold p.d.validResult(respr, false) @@ -1751,6 +1772,7 @@ func (p *scionPacketProcessor) invalidSrcIA() (processResult, error) { slayers.SCMPCodeInvalidSourceAddress, &slayers.SCMPParameterProblem{Pointer: uint16(slayers.CmnHdrLen + addr.IABytes)}, invalidSrcIA, + /*@ nil , @*/ ) } @@ -1763,6 +1785,7 @@ func (p *scionPacketProcessor) invalidDstIA() (processResult, error) { slayers.SCMPCodeInvalidDestinationAddress, &slayers.SCMPParameterProblem{Pointer: uint16(slayers.CmnHdrLen)}, invalidDstIA, + /*@ nil , @*/ ) } @@ -1860,6 +1883,7 @@ func (p *scionPacketProcessor) validateEgressID() (respr processResult, reserr e errCode, &slayers.SCMPParameterProblem{Pointer: p.currentHopPointer( /*@ nil @*/ )}, cannotRoute, + /*@ nil , @*/ ) } @@ -1888,7 +1912,8 @@ func (p *scionPacketProcessor) validateEgressID() (respr processResult, reserr e slayers.SCMPCodeInvalidPath, // XXX(matzf) new code InvalidHop? &slayers.SCMPParameterProblem{Pointer: p.currentHopPointer( /*@ nil @*/ )}, serrors.WithCtx(cannotRoute, "ingress_id", p.ingressID, "ingress_type", ingress, - "egress_id", pktEgressID, "egress_type", egress)) + "egress_id", pktEgressID, "egress_type", egress), + /*@ nil , @*/) } } // Check that the interface pair is valid on a segment switch. @@ -1910,7 +1935,8 @@ func (p *scionPacketProcessor) validateEgressID() (respr processResult, reserr e slayers.SCMPCodeInvalidSegmentChange, &slayers.SCMPParameterProblem{Pointer: p.currentInfoPointer( /*@ nil @*/ )}, serrors.WithCtx(cannotRoute, "ingress_id", p.ingressID, "ingress_type", ingress, - "egress_id", pktEgressID, "egress_type", egress)) + "egress_id", pktEgressID, "egress_type", egress), + /*@ nil , @*/) } } @@ -2020,6 +2046,7 @@ func (p *scionPacketProcessor) verifyCurrentMAC() (respr processResult, reserr e "cons_dir", p.infoField.ConsDir, "if_id", p.ingressID, "curr_inf", p.path.PathMeta.CurrINF, "curr_hf", p.path.PathMeta.CurrHF, "seg_id", p.infoField.SegID), + /*@ nil , @*/ ) } // Add the full MAC to the SCION packet processor, @@ -2060,7 +2087,9 @@ func (p *scionPacketProcessor) resolveInbound( /*@ ghost ubScionL []byte @*/ ) ( r, err := p.packSCMP( slayers.SCMPTypeDestinationUnreachable, slayers.SCMPCodeNoRoute, - &slayers.SCMPDestinationUnreachable{}, err) + &slayers.SCMPDestinationUnreachable{}, + err, + /*@ nil , @*/) return nil, r, err /*@ , false @*/ default: // @ fold p.d.validResult(respr, addrAliases) @@ -2230,7 +2259,7 @@ func (p *scionPacketProcessor) validateEgressUp() (respr processResult, reserr e } } // @ TODO() - return p.packSCMP(typ, 0, scmpP, serrors.New("bfd session down")) + return p.packSCMP(typ, 0, scmpP, serrors.New("bfd session down") /*@, nil , @*/) } } // @ fold p.d.validResult(processResult{}, false) @@ -2453,7 +2482,7 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( Interface: uint64(interfaceID), } // @ TODO() - return p.packSCMP(slayers.SCMPTypeTracerouteReply, 0, &scmpP, nil) + return p.packSCMP(slayers.SCMPTypeTracerouteReply, 0, &scmpP, nil /*@ , nil @*/) } // @ preserves acc(p.scionLayer.Mem(ubScionL), R20) @@ -2477,6 +2506,7 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte @*/ ) ( &slayers.SCMPParameterProblem{Pointer: 0}, serrors.New("bad packet size", "header", p.scionLayer.PayloadLen, "actual", len(p.scionLayer.Payload)), + /*@ nil , @*/ ) } @@ -2642,6 +2672,7 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, errCode, &slayers.SCMPParameterProblem{Pointer: p.currentHopPointer( /*@ nil @*/ )}, cannotRoute, + /*@ nil , @*/ ) return tmp, err /*@, false @*/ } From 88c9632331d8f1eabf06655e19894e5570912e48 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 26 Jan 2024 15:58:29 +0100 Subject: [PATCH 03/31] backup --- router/dataplane.go | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/router/dataplane.go b/router/dataplane.go index e85ee31cd..a4de7fc6a 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1554,6 +1554,9 @@ type macBuffersT struct { // @ requires acc(&p.d, _) && acc(MutexInvariant(p.d), _) // @ requires acc(p.scionLayer.Mem(ub), R4) +// @ requires acc(&p.lastLayer, R55) && p.lastLayer != nil +// @ requires (p.scionLayer !== p.lastLayer ==> +// @ acc(p.lastLayer.Mem(nil), R15) // TODO: what is the buf here? we also need perms for the buffer // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires sl.AbsSlice_Bytes(ub, 0, len(ub)) // @ requires acc(&p.ingressID, R15) @@ -2482,7 +2485,7 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( Interface: uint64(interfaceID), } // @ TODO() - return p.packSCMP(slayers.SCMPTypeTracerouteReply, 0, &scmpP, nil /*@ , nil @*/) + return p.packSCMP(slayers.SCMPTypeTracerouteReply, 0, &scmpP, (error)(nil) /*@ , nil @*/) } // @ preserves acc(p.scionLayer.Mem(ubScionL), R20) From 43536ffcfbd26fe2f5ee7e288efbccd42c167c78 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 7 Feb 2024 17:08:17 +0100 Subject: [PATCH 04/31] fix syntax errors --- router/dataplane.go | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index a78a345a9..d808c1548 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1664,8 +1664,9 @@ type macBuffersT struct { // @ requires acc(&p.d, _) && acc(MutexInvariant(p.d), _) // @ requires acc(p.scionLayer.Mem(ub), R4) // @ requires acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ requires (p.scionLayer !== p.lastLayer ==> -// @ acc(p.lastLayer.Mem(nil), R15) // TODO: what is the buf here? we also need perms for the buffer +// TODO: what is the buf here? we also need perms for the buffer +// @ requires &p.scionLayer !== p.lastLayer ==> +// @ acc(p.lastLayer.Mem(nil), R15) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires sl.AbsSlice_Bytes(ub, 0, len(ub)) // @ requires acc(&p.ingressID, R15) From 7c324f1a800d855dec13ea40f60a26ecd62f8889 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 9 Feb 2024 18:41:26 +0100 Subject: [PATCH 05/31] establish necessary precondition of DecodeFromBytes --- router/dataplane.go | 1 + 1 file changed, 1 insertion(+) diff --git a/router/dataplane.go b/router/dataplane.go index d808c1548..0a958e8ba 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1695,6 +1695,7 @@ func (p *scionPacketProcessor) packSCMP( if p.lastLayer.NextLayerType( /*@ nil @*/ ) == slayers.LayerTypeSCMP { var scmpLayer /*@@@*/ slayers.SCMP pld /*@ , start, end @*/ := p.lastLayer.LayerPayload( /*@ nil @*/ ) + // @ gopacket.AssertInvariantNilDecodeFeedback() err := scmpLayer.DecodeFromBytes(pld, gopacket.NilDecodeFeedback) if err != nil { return processResult{}, serrors.WrapStr("decoding SCMP layer", err) From 467903eb16bec39ca93787ae88d3faa023a5d782 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Sun, 25 Feb 2024 20:14:24 +0100 Subject: [PATCH 06/31] remove TODOs --- router/dataplane.go | 17 +---------------- 1 file changed, 1 insertion(+), 16 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index 3fd931272..874151e09 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1898,8 +1898,7 @@ func (p *scionPacketProcessor) validateHopExpiry() (respr processResult, reserr // @ fold p.d.validResult(respr, false) return processResult{}, nil } - // @ TODO() - // TODO: adapt; note that packSCMP always returns an empty addr and conn and + // TODO: drop; note that packSCMP always returns an empty addr and conn and // when the err is nil, it returns the bytes of p.buffer. This should be a magic wand // that is consumed after sending the reply. For now, we are making this simplifying // assumption, but in the future, we should elaborate the proof for this to not be @@ -1939,7 +1938,6 @@ func (p *scionPacketProcessor) validateIngressID() (respr processResult, reserr errCode = slayers.SCMPCodeUnknownHopFieldEgress } if p.ingressID != 0 && p.ingressID != pktIngressID { - // @ TODO() return p.packSCMP( slayers.SCMPTypeParameterProblem, errCode, @@ -1981,21 +1979,17 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte @*/ ) // Note: SCMP error messages triggered by the sibling router may use paths that // don't start with the first hop. if p.path.IsFirstHop( /*@ ubPath @*/ ) && !srcIsLocal { - // @ TODO() // depends on packSCMP return p.invalidSrcIA() } if dstIsLocal { - // @ TODO() // depends on packSCMP return p.invalidDstIA() } } else { // Inbound if srcIsLocal { - // @ TODO() // depends on packSCMP return p.invalidSrcIA() } if p.path.IsLastHop( /*@ ubPath @*/ ) != dstIsLocal { - // @ TODO() // depends on packSCMP return p.invalidDstIA() } } @@ -2117,7 +2111,6 @@ func (p *scionPacketProcessor) validateEgressID() (respr processResult, reserr e if !p.infoField.ConsDir { errCode = slayers.SCMPCodeUnknownHopFieldIngress } - // @ TODO() return p.packSCMP( slayers.SCMPTypeParameterProblem, errCode, @@ -2146,7 +2139,6 @@ func (p *scionPacketProcessor) validateEgressID() (respr processResult, reserr e // @ fold p.d.validResult(respr, false) return processResult{}, nil default: // malicious - // @ TODO() return p.packSCMP( slayers.SCMPTypeParameterProblem, slayers.SCMPCodeInvalidPath, // XXX(matzf) new code InvalidHop? @@ -2169,7 +2161,6 @@ func (p *scionPacketProcessor) validateEgressID() (respr processResult, reserr e // @ fold p.d.validResult(respr, false) return processResult{}, nil default: - // @ TODO() return p.packSCMP( slayers.SCMPTypeParameterProblem, slayers.SCMPCodeInvalidSegmentChange, @@ -2275,7 +2266,6 @@ func (p *scionPacketProcessor) verifyCurrentMAC() (respr processResult, reserr e // @ sl.SplitRange_Bytes(fullMac, 0, path.MacLen, R20) // @ ghost defer sl.CombineRange_Bytes(fullMac, 0, path.MacLen, R20) if subtle.ConstantTimeCompare(p.hopField.Mac[:path.MacLen], fullMac[:path.MacLen]) == 0 { - // @ TODO() return p.packSCMP( slayers.SCMPTypeParameterProblem, slayers.SCMPCodeInvalidHopFieldMAC, @@ -2323,7 +2313,6 @@ func (p *scionPacketProcessor) resolveInbound( /*@ ghost ubScionL []byte @*/ ) ( // @ ghost if addrAliases { // @ apply acc(a.Mem(), R15) --* acc(sl.AbsSlice_Bytes(ubScionL, 0, len(ubScionL)), R15) // @ } - // @ TODO() r, err := p.packSCMP( slayers.SCMPTypeDestinationUnreachable, slayers.SCMPCodeNoRoute, @@ -2498,7 +2487,6 @@ func (p *scionPacketProcessor) validateEgressUp() (respr processResult, reserr e Egress: uint64(egressID), } } - // @ TODO() return p.packSCMP(typ, 0, scmpP, serrors.New("bfd session down") /*@, nil , @*/) } } @@ -2721,7 +2709,6 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( IA: p.d.localIA, Interface: uint64(interfaceID), } - // @ TODO() return p.packSCMP(slayers.SCMPTypeTracerouteReply, 0, &scmpP, (error)(nil) /*@ , nil @*/) } @@ -2739,7 +2726,6 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte @*/ ) ( // @ fold p.d.validResult(processResult{}, false) return processResult{}, nil } - // @ TODO() return p.packSCMP( slayers.SCMPTypeParameterProblem, slayers.SCMPCodeInvalidPacketSize, @@ -2905,7 +2891,6 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, if !p.infoField.ConsDir { errCode = slayers.SCMPCodeUnknownHopFieldIngress } - // @ TODO() // @ p.scionLayer.DowngradePerm(ub) tmp, err := p.packSCMP( slayers.SCMPTypeParameterProblem, From cfcd6efbc65f682cd5843be62ef3633536d92654 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 5 Mar 2024 00:02:24 +0100 Subject: [PATCH 07/31] backup --- router/dataplane.go | 62 ++++++++++++++++++++++++++++++--------------- 1 file changed, 42 insertions(+), 20 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index 874151e09..a11a7b08e 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1787,18 +1787,23 @@ type macBuffersT struct { epicInput []byte } -// @ requires acc(&p.d, _) && acc(MutexInvariant(p.d), _) +// @ requires acc(&p.d, _) && acc(p.d.Mem(), _) // @ requires acc(p.scionLayer.Mem(ub), R4) +// @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) +// @ requires ubLL == nil || ubLL === ub[startLL:endLL] // @ requires acc(&p.lastLayer, R55) && p.lastLayer != nil -// TODO: what is the buf here? we also need perms for the buffer // @ requires &p.scionLayer !== p.lastLayer ==> -// @ acc(p.lastLayer.Mem(nil), R15) +// @ acc(p.lastLayer.Mem(ubLL), R15) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires sl.AbsSlice_Bytes(ub, 0, len(ub)) // @ requires acc(&p.ingressID, R15) // @ requires acc(&p.buffer, R50) && p.buffer.Mem() +// @ requires cause.ErrorMem() // @ ensures acc(&p.d, _) // @ ensures acc(p.scionLayer.Mem(ub), R4) +// @ ensures acc(&p.lastLayer, R55) && p.lastLayer != nil +// @ ensures &p.scionLayer !== p.lastLayer ==> +// @ acc(p.lastLayer.Mem(ubLL), R15) // @ ensures sl.AbsSlice_Bytes(ub, 0, len(ub)) // @ ensures acc(&p.ingressID, R15) // @ ensures p.d.validResult(respr, false) @@ -1816,21 +1821,38 @@ func (p *scionPacketProcessor) packSCMP( scmpP gopacket.SerializableLayer, cause error, // @ ghost ub []byte, + // @ ghost ubLL []byte, + // @ ghost startLL int, + // @ ghost endLL int, ) (respr processResult, reserr error) { // check invoking packet was an SCMP error: - if p.lastLayer.NextLayerType( /*@ nil @*/ ) == slayers.LayerTypeSCMP { + if p.lastLayer.NextLayerType( /*@ ubLL @*/ ) == slayers.LayerTypeSCMP { var scmpLayer /*@@@*/ slayers.SCMP - pld /*@ , start, end @*/ := p.lastLayer.LayerPayload( /*@ nil @*/ ) + // @ fold scmpLayer.NonInitMem() + pld /*@ , start, end @*/ := p.lastLayer.LayerPayload( /*@ ubLL @*/ ) // @ gopacket.AssertInvariantNilDecodeFeedback() + /*@ + sl.SplitRange_Bytes(ub, startLL, endLL, writePerm) + ghost defer sl.CombineRange_Bytes(ub, startLL, endLL, writePerm) + if pld == nil { + fold sl.AbsSlice_Bytes(nil, 0, 0) + } else { + sl.SplitRange_Bytes(ubLL, start, endLL, writePerm) + ghost defer sl.CombineRange_Bytes(ubLL, start, endLL, writePerm) + } + @*/ err := scmpLayer.DecodeFromBytes(pld, gopacket.NilDecodeFeedback) if err != nil { + // @ fold p.d.validResult(respr, false) return processResult{}, serrors.WrapStr("decoding SCMP layer", err) } - if !scmpLayer.TypeCode.InfoMsg() { + if /*@ unfolding scmpLayer.Mem(pld) in @*/ !scmpLayer.TypeCode.InfoMsg() { + // @ fold p.d.validResult(respr, false) return processResult{}, serrors.WrapStr("SCMP error for SCMP error pkt -> DROP", cause) } } + // @ assume false rawSCMP, err := p.prepareSCMP(typ, code, scmpP, cause /*@ , nil @*/) return processResult{OutPkt: rawSCMP}, err } @@ -1914,7 +1936,7 @@ func (p *scionPacketProcessor) validateHopExpiry() (respr processResult, reserr &slayers.SCMPParameterProblem{Pointer: p.currentHopPointer( /*@ nil @*/ )}, serrors.New("expired hop", "cons_dir", p.infoField.ConsDir, "if_id", p.ingressID, "curr_inf", p.path.PathMeta.CurrINF, "curr_hf", p.path.PathMeta.CurrHF), - /*@ nil , @*/ + /*@ nil , nil, 0, 0, @*/ ) } @@ -1944,7 +1966,7 @@ func (p *scionPacketProcessor) validateIngressID() (respr processResult, reserr &slayers.SCMPParameterProblem{Pointer: p.currentHopPointer( /*@ nil @*/ )}, serrors.New("ingress interface invalid", "pkt_ingress", pktIngressID, "router_ingress", p.ingressID), - /*@ nil , @*/ + /*@ nil , nil, 0, 0, @*/ ) } // @ fold p.d.validResult(respr, false) @@ -1998,7 +2020,7 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte @*/ ) } // invalidSrcIA is a helper to return an SCMP error for an invalid SrcIA. -// @ trusted +// @ trusted // TODO: start here // @ requires false func (p *scionPacketProcessor) invalidSrcIA() (processResult, error) { return p.packSCMP( @@ -2011,7 +2033,7 @@ func (p *scionPacketProcessor) invalidSrcIA() (processResult, error) { } // invalidDstIA is a helper to return an SCMP error for an invalid DstIA. -// @ trusted +// @ trusted // TODO: start here // @ requires false func (p *scionPacketProcessor) invalidDstIA() (processResult, error) { return p.packSCMP( @@ -2019,7 +2041,7 @@ func (p *scionPacketProcessor) invalidDstIA() (processResult, error) { slayers.SCMPCodeInvalidDestinationAddress, &slayers.SCMPParameterProblem{Pointer: uint16(slayers.CmnHdrLen)}, invalidDstIA, - /*@ nil , @*/ + /*@ nil , nil, 0, 0, @*/ ) } @@ -2116,7 +2138,7 @@ func (p *scionPacketProcessor) validateEgressID() (respr processResult, reserr e errCode, &slayers.SCMPParameterProblem{Pointer: p.currentHopPointer( /*@ nil @*/ )}, cannotRoute, - /*@ nil , @*/ + /*@ nil, nil, 0, 0, @*/ ) } @@ -2145,7 +2167,7 @@ func (p *scionPacketProcessor) validateEgressID() (respr processResult, reserr e &slayers.SCMPParameterProblem{Pointer: p.currentHopPointer( /*@ nil @*/ )}, serrors.WithCtx(cannotRoute, "ingress_id", p.ingressID, "ingress_type", ingress, "egress_id", pktEgressID, "egress_type", egress), - /*@ nil , @*/) + /*@ nil, nil, 0, 0, @*/) } } // Check that the interface pair is valid on a segment switch. @@ -2167,7 +2189,7 @@ func (p *scionPacketProcessor) validateEgressID() (respr processResult, reserr e &slayers.SCMPParameterProblem{Pointer: p.currentInfoPointer( /*@ nil @*/ )}, serrors.WithCtx(cannotRoute, "ingress_id", p.ingressID, "ingress_type", ingress, "egress_id", pktEgressID, "egress_type", egress), - /*@ nil , @*/) + /*@ nil, nil, 0, 0, @*/) } } @@ -2276,7 +2298,7 @@ func (p *scionPacketProcessor) verifyCurrentMAC() (respr processResult, reserr e "cons_dir", p.infoField.ConsDir, "if_id", p.ingressID, "curr_inf", p.path.PathMeta.CurrINF, "curr_hf", p.path.PathMeta.CurrHF, "seg_id", p.infoField.SegID), - /*@ nil , @*/ + /*@ nil, nil, 0, 0, @*/ ) } // Add the full MAC to the SCION packet processor, @@ -2318,7 +2340,7 @@ func (p *scionPacketProcessor) resolveInbound( /*@ ghost ubScionL []byte @*/ ) ( slayers.SCMPCodeNoRoute, &slayers.SCMPDestinationUnreachable{}, err, - /*@ nil , @*/) + /*@ nil, nil, 0, 0, @*/) return nil, r, err /*@ , false @*/ default: // @ fold p.d.validResult(respr, addrAliases) @@ -2487,7 +2509,7 @@ func (p *scionPacketProcessor) validateEgressUp() (respr processResult, reserr e Egress: uint64(egressID), } } - return p.packSCMP(typ, 0, scmpP, serrors.New("bfd session down") /*@, nil , @*/) + return p.packSCMP(typ, 0, scmpP, serrors.New("bfd session down") /*@, nil , nil, 0, 0, @*/) } } // @ fold p.d.validResult(processResult{}, false) @@ -2709,7 +2731,7 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( IA: p.d.localIA, Interface: uint64(interfaceID), } - return p.packSCMP(slayers.SCMPTypeTracerouteReply, 0, &scmpP, (error)(nil) /*@ , nil @*/) + return p.packSCMP(slayers.SCMPTypeTracerouteReply, 0, &scmpP, (error)(nil) /*@ , nil, nil, 0, 0, @*/) } // @ preserves acc(p.scionLayer.Mem(ubScionL), R20) @@ -2732,7 +2754,7 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte @*/ ) ( &slayers.SCMPParameterProblem{Pointer: 0}, serrors.New("bad packet size", "header", p.scionLayer.PayloadLen, "actual", len(p.scionLayer.Payload)), - /*@ nil , @*/ + /*@ nil, nil, 0, 0, @*/ ) } @@ -2897,7 +2919,7 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, errCode, &slayers.SCMPParameterProblem{Pointer: p.currentHopPointer( /*@ nil @*/ )}, cannotRoute, - /*@ nil , @*/ + /*@ nil, nil, 0, 0, @*/ ) return tmp, err /*@, false @*/ } From ae8edf9a5f4902bb0c51067853d01618366a5a40 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 5 Mar 2024 12:29:44 +0100 Subject: [PATCH 08/31] move on with proof obligations --- router/dataplane.go | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index a11a7b08e..440dff586 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1794,6 +1794,8 @@ type macBuffersT struct { // @ requires acc(&p.lastLayer, R55) && p.lastLayer != nil // @ requires &p.scionLayer !== p.lastLayer ==> // @ acc(p.lastLayer.Mem(ubLL), R15) +// @ requires &p.scionLayer === p.lastLayer ==> +// @ ub === ubLL // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires sl.AbsSlice_Bytes(ub, 0, len(ub)) // @ requires acc(&p.ingressID, R15) @@ -1830,17 +1832,17 @@ func (p *scionPacketProcessor) packSCMP( var scmpLayer /*@@@*/ slayers.SCMP // @ fold scmpLayer.NonInitMem() pld /*@ , start, end @*/ := p.lastLayer.LayerPayload( /*@ ubLL @*/ ) - // @ gopacket.AssertInvariantNilDecodeFeedback() /*@ sl.SplitRange_Bytes(ub, startLL, endLL, writePerm) ghost defer sl.CombineRange_Bytes(ub, startLL, endLL, writePerm) if pld == nil { fold sl.AbsSlice_Bytes(nil, 0, 0) } else { - sl.SplitRange_Bytes(ubLL, start, endLL, writePerm) - ghost defer sl.CombineRange_Bytes(ubLL, start, endLL, writePerm) + sl.SplitRange_Bytes(ubLL, start, end, writePerm) + ghost defer sl.CombineRange_Bytes(ubLL, start, end, writePerm) } @*/ + // @ gopacket.AssertInvariantNilDecodeFeedback() err := scmpLayer.DecodeFromBytes(pld, gopacket.NilDecodeFeedback) if err != nil { // @ fold p.d.validResult(respr, false) @@ -3351,6 +3353,7 @@ func (b *bfdSend) Send(bfd *layers.BFD) error { // @ ensures acc(p.scionLayer.Mem(ub), R4) // @ ensures sl.AbsSlice_Bytes(ub, 0, len(ub)) // @ ensures acc(&p.ingressID, R15) +// TODO: ensures result and result --* p.Buffer.Mem() // @ decreases func (p *scionPacketProcessor) prepareSCMP( typ slayers.SCMPType, From 2da529ada78e59379e8f4e6dc80542d0dc845a30 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 5 Mar 2024 16:55:48 +0100 Subject: [PATCH 09/31] verify packSCMP; reinstate TODO()s for doing the proof step by step --- router/dataplane.go | 53 ++++++++++++++++++++++++++++++++++++++------- 1 file changed, 45 insertions(+), 8 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index 440dff586..802c87af6 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1827,35 +1827,54 @@ func (p *scionPacketProcessor) packSCMP( // @ ghost startLL int, // @ ghost endLL int, ) (respr processResult, reserr error) { + // @ ghost llIsScmp := false + // @ ghost scmpPldIsNil := false + // @ ghost maybeStartPld := 0 + // @ ghost maybeEndPld := 0 // check invoking packet was an SCMP error: if p.lastLayer.NextLayerType( /*@ ubLL @*/ ) == slayers.LayerTypeSCMP { + // @ llIsScmp = true var scmpLayer /*@@@*/ slayers.SCMP // @ fold scmpLayer.NonInitMem() pld /*@ , start, end @*/ := p.lastLayer.LayerPayload( /*@ ubLL @*/ ) /*@ sl.SplitRange_Bytes(ub, startLL, endLL, writePerm) - ghost defer sl.CombineRange_Bytes(ub, startLL, endLL, writePerm) + maybeStartPld = start + maybeEndPld = end if pld == nil { + scmpPldIsNil = true fold sl.AbsSlice_Bytes(nil, 0, 0) } else { sl.SplitRange_Bytes(ubLL, start, end, writePerm) - ghost defer sl.CombineRange_Bytes(ubLL, start, end, writePerm) } @*/ // @ gopacket.AssertInvariantNilDecodeFeedback() err := scmpLayer.DecodeFromBytes(pld, gopacket.NilDecodeFeedback) if err != nil { - // @ fold p.d.validResult(respr, false) + // @ ghost if !scmpPldIsNil { sl.CombineRange_Bytes(ubLL, start, end, writePerm) } + // @ sl.CombineRange_Bytes(ub, startLL, endLL, writePerm) + // @ fold p.d.validResult(processResult{}, false) return processResult{}, serrors.WrapStr("decoding SCMP layer", err) } if /*@ unfolding scmpLayer.Mem(pld) in @*/ !scmpLayer.TypeCode.InfoMsg() { - // @ fold p.d.validResult(respr, false) + // @ ghost if !scmpPldIsNil { sl.CombineRange_Bytes(ubLL, start, end, writePerm) } + // @ sl.CombineRange_Bytes(ub, startLL, endLL, writePerm) + // @ fold p.d.validResult(processResult{}, false) return processResult{}, serrors.WrapStr("SCMP error for SCMP error pkt -> DROP", cause) } } - // @ assume false - rawSCMP, err := p.prepareSCMP(typ, code, scmpP, cause /*@ , nil @*/) + /*@ + ghost if llIsScmp { + ghost if !scmpPldIsNil { + sl.CombineRange_Bytes(ubLL, maybeStartPld, maybeEndPld, writePerm) + } + sl.CombineRange_Bytes(ub, startLL, endLL, writePerm) + } + @*/ + rawSCMP, err := p.prepareSCMP(typ, code, scmpP, cause /*@ , ub @*/) + // @ ghost result := processResult{OutPkt: rawSCMP} + // @ fold p.d.validResult(result, false) return processResult{OutPkt: rawSCMP}, err } @@ -1922,6 +1941,7 @@ func (p *scionPacketProcessor) validateHopExpiry() (respr processResult, reserr // @ fold p.d.validResult(respr, false) return processResult{}, nil } + // @ TODO() // TODO: drop; note that packSCMP always returns an empty addr and conn and // when the err is nil, it returns the bytes of p.buffer. This should be a magic wand // that is consumed after sending the reply. For now, we are making this simplifying @@ -1962,6 +1982,7 @@ func (p *scionPacketProcessor) validateIngressID() (respr processResult, reserr errCode = slayers.SCMPCodeUnknownHopFieldEgress } if p.ingressID != 0 && p.ingressID != pktIngressID { + // @ TODO() return p.packSCMP( slayers.SCMPTypeParameterProblem, errCode, @@ -2135,6 +2156,7 @@ func (p *scionPacketProcessor) validateEgressID() (respr processResult, reserr e if !p.infoField.ConsDir { errCode = slayers.SCMPCodeUnknownHopFieldIngress } + // @ TODO() return p.packSCMP( slayers.SCMPTypeParameterProblem, errCode, @@ -2163,6 +2185,7 @@ func (p *scionPacketProcessor) validateEgressID() (respr processResult, reserr e // @ fold p.d.validResult(respr, false) return processResult{}, nil default: // malicious + // @ TODO() return p.packSCMP( slayers.SCMPTypeParameterProblem, slayers.SCMPCodeInvalidPath, // XXX(matzf) new code InvalidHop? @@ -2185,6 +2208,7 @@ func (p *scionPacketProcessor) validateEgressID() (respr processResult, reserr e // @ fold p.d.validResult(respr, false) return processResult{}, nil default: + // @ TODO() return p.packSCMP( slayers.SCMPTypeParameterProblem, slayers.SCMPCodeInvalidSegmentChange, @@ -2290,6 +2314,7 @@ func (p *scionPacketProcessor) verifyCurrentMAC() (respr processResult, reserr e // @ sl.SplitRange_Bytes(fullMac, 0, path.MacLen, R20) // @ ghost defer sl.CombineRange_Bytes(fullMac, 0, path.MacLen, R20) if subtle.ConstantTimeCompare(p.hopField.Mac[:path.MacLen], fullMac[:path.MacLen]) == 0 { + // @ TODO() return p.packSCMP( slayers.SCMPTypeParameterProblem, slayers.SCMPCodeInvalidHopFieldMAC, @@ -2337,6 +2362,7 @@ func (p *scionPacketProcessor) resolveInbound( /*@ ghost ubScionL []byte @*/ ) ( // @ ghost if addrAliases { // @ apply acc(a.Mem(), R15) --* acc(sl.AbsSlice_Bytes(ubScionL, 0, len(ubScionL)), R15) // @ } + // @ TODO() r, err := p.packSCMP( slayers.SCMPTypeDestinationUnreachable, slayers.SCMPCodeNoRoute, @@ -2511,6 +2537,7 @@ func (p *scionPacketProcessor) validateEgressUp() (respr processResult, reserr e Egress: uint64(egressID), } } + // @ TODO() return p.packSCMP(typ, 0, scmpP, serrors.New("bfd session down") /*@, nil , nil, 0, 0, @*/) } } @@ -2733,6 +2760,7 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( IA: p.d.localIA, Interface: uint64(interfaceID), } + // @ TODO() return p.packSCMP(slayers.SCMPTypeTracerouteReply, 0, &scmpP, (error)(nil) /*@ , nil, nil, 0, 0, @*/) } @@ -2750,6 +2778,7 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte @*/ ) ( // @ fold p.d.validResult(processResult{}, false) return processResult{}, nil } + // @ TODO() return p.packSCMP( slayers.SCMPTypeParameterProblem, slayers.SCMPCodeInvalidPacketSize, @@ -2916,6 +2945,7 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, errCode = slayers.SCMPCodeUnknownHopFieldIngress } // @ p.scionLayer.DowngradePerm(ub) + // @ TODO() tmp, err := p.packSCMP( slayers.SCMPTypeParameterProblem, errCode, @@ -3350,10 +3380,17 @@ func (b *bfdSend) Send(bfd *layers.BFD) error { // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires sl.AbsSlice_Bytes(ub, 0, len(ub)) // @ requires acc(&p.ingressID, R15) +// @ requires acc(&p.buffer, R55) && p.buffer.Mem() // @ ensures acc(p.scionLayer.Mem(ub), R4) // @ ensures sl.AbsSlice_Bytes(ub, 0, len(ub)) // @ ensures acc(&p.ingressID, R15) -// TODO: ensures result and result --* p.Buffer.Mem() +// @ ensures acc(&p.buffer, R55) +// @ ensures result != nil ==> +// @ sl.AbsSlice_Bytes(result, 0, len(result)) && +// @ p.buffer.MemWithoutUBuf(result) +// @ ensures result == nil ==> +// @ p.buffer.Mem() +// @ ensures reserr != nil && reserr.ErrorMem() // @ decreases func (p *scionPacketProcessor) prepareSCMP( typ slayers.SCMPType, @@ -3361,7 +3398,7 @@ func (p *scionPacketProcessor) prepareSCMP( scmpP gopacket.SerializableLayer, cause error, // @ ghost ub []byte, -) ([]byte, error) { +) (result []byte, reserr error) { // *copy* and reverse path -- the original path should not be modified as this writes directly // back to rawPkt (quote). From 0836f5f215f825d0817e1b5ee8a65e6e2e66275c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 5 Mar 2024 17:35:45 +0100 Subject: [PATCH 10/31] backup --- router/assumptions.gobra | 10 +++++ router/dataplane.go | 80 ++++++++++++++++++++++++++++++++++------ 2 files changed, 78 insertions(+), 12 deletions(-) diff --git a/router/assumptions.gobra b/router/assumptions.gobra index f8811b007..17716e7fc 100644 --- a/router/assumptions.gobra +++ b/router/assumptions.gobra @@ -75,6 +75,16 @@ ensures cannotRoute.ErrorMem() decreases _ func establishCannotRoute() +ghost +ensures invalidSrcIA.ErrorMem() +decreases _ +func establishInvalidSrcIA() + +ghost +ensures invalidDstIA.ErrorMem() +decreases _ +func establishInvalidDstIA() + /**** End of post-init invariants ****/ /**** scmpError ghost members ****/ diff --git a/router/dataplane.go b/router/dataplane.go index 802c87af6..3c494b5a6 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -2024,18 +2024,18 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte @*/ ) // Note: SCMP error messages triggered by the sibling router may use paths that // don't start with the first hop. if p.path.IsFirstHop( /*@ ubPath @*/ ) && !srcIsLocal { - return p.invalidSrcIA() + return p.invalidSrcIA( /*@ nil, nil, 0, 0 @*/ ) } if dstIsLocal { - return p.invalidDstIA() + return p.invalidDstIA( /*@ nil, nil, 0, 0 @*/ ) } } else { // Inbound if srcIsLocal { - return p.invalidSrcIA() + return p.invalidSrcIA( /*@ nil, nil, 0, 0 @*/ ) } if p.path.IsLastHop( /*@ ubPath @*/ ) != dstIsLocal { - return p.invalidDstIA() + return p.invalidDstIA( /*@ nil, nil, 0, 0 @*/ ) } } // @ fold p.d.validResult(processResult{}, false) @@ -2043,28 +2043,84 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte @*/ ) } // invalidSrcIA is a helper to return an SCMP error for an invalid SrcIA. -// @ trusted // TODO: start here -// @ requires false -func (p *scionPacketProcessor) invalidSrcIA() (processResult, error) { +// @ requires acc(&p.d, _) && acc(p.d.Mem(), _) +// @ requires acc(p.scionLayer.Mem(ub), R4) +// @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) +// @ requires ubLL == nil || ubLL === ub[startLL:endLL] +// @ requires acc(&p.lastLayer, R55) && p.lastLayer != nil +// @ requires &p.scionLayer !== p.lastLayer ==> +// @ acc(p.lastLayer.Mem(ubLL), R15) +// @ requires &p.scionLayer === p.lastLayer ==> +// @ ub === ubLL +// @ requires p.scionLayer.ValidPathMetaData(ub) +// @ requires sl.AbsSlice_Bytes(ub, 0, len(ub)) +// @ requires acc(&p.ingressID, R15) +// @ requires acc(&p.buffer, R50) && p.buffer.Mem() +// @ ensures acc(&p.d, _) +// @ ensures acc(p.scionLayer.Mem(ub), R4) +// @ ensures acc(&p.lastLayer, R55) && p.lastLayer != nil +// @ ensures &p.scionLayer !== p.lastLayer ==> +// @ acc(p.lastLayer.Mem(ubLL), R15) +// @ ensures sl.AbsSlice_Bytes(ub, 0, len(ub)) +// @ ensures acc(&p.ingressID, R15) +// @ ensures p.d.validResult(respr, false) +// @ ensures acc(&p.buffer, R50) +// @ ensures respr === processResult{} ==> +// @ p.buffer.Mem() +// @ ensures respr !== processResult{} ==> +// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && +// @ sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ ensures reserr != nil ==> reserr.ErrorMem() +// @ decreases +func (p *scionPacketProcessor) invalidSrcIA( /*@ ghost ub []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { + // @ establishInvalidSrcIA() return p.packSCMP( slayers.SCMPTypeParameterProblem, slayers.SCMPCodeInvalidSourceAddress, &slayers.SCMPParameterProblem{Pointer: uint16(slayers.CmnHdrLen + addr.IABytes)}, invalidSrcIA, - /*@ nil , @*/ + /*@ ub , ubLL, startLL, endLL, @*/ ) } // invalidDstIA is a helper to return an SCMP error for an invalid DstIA. -// @ trusted // TODO: start here -// @ requires false -func (p *scionPacketProcessor) invalidDstIA() (processResult, error) { +// @ requires acc(&p.d, _) && acc(p.d.Mem(), _) +// @ requires acc(p.scionLayer.Mem(ub), R4) +// @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) +// @ requires ubLL == nil || ubLL === ub[startLL:endLL] +// @ requires acc(&p.lastLayer, R55) && p.lastLayer != nil +// @ requires &p.scionLayer !== p.lastLayer ==> +// @ acc(p.lastLayer.Mem(ubLL), R15) +// @ requires &p.scionLayer === p.lastLayer ==> +// @ ub === ubLL +// @ requires p.scionLayer.ValidPathMetaData(ub) +// @ requires sl.AbsSlice_Bytes(ub, 0, len(ub)) +// @ requires acc(&p.ingressID, R15) +// @ requires acc(&p.buffer, R50) && p.buffer.Mem() +// @ ensures acc(&p.d, _) +// @ ensures acc(p.scionLayer.Mem(ub), R4) +// @ ensures acc(&p.lastLayer, R55) && p.lastLayer != nil +// @ ensures &p.scionLayer !== p.lastLayer ==> +// @ acc(p.lastLayer.Mem(ubLL), R15) +// @ ensures sl.AbsSlice_Bytes(ub, 0, len(ub)) +// @ ensures acc(&p.ingressID, R15) +// @ ensures p.d.validResult(respr, false) +// @ ensures acc(&p.buffer, R50) +// @ ensures respr === processResult{} ==> +// @ p.buffer.Mem() +// @ ensures respr !== processResult{} ==> +// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && +// @ sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ ensures reserr != nil ==> reserr.ErrorMem() +// @ decreases +func (p *scionPacketProcessor) invalidDstIA( /*@ ghost ub []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { + // @ establishInvalidDstIA() return p.packSCMP( slayers.SCMPTypeParameterProblem, slayers.SCMPCodeInvalidDestinationAddress, &slayers.SCMPParameterProblem{Pointer: uint16(slayers.CmnHdrLen)}, invalidDstIA, - /*@ nil , nil, 0, 0, @*/ + /*@ ub , ubLL, startLL, endLL, @*/ ) } From 28f71bde2bb1b4bb8eb468ad22979df2fb3dc51c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Thu, 7 Mar 2024 15:34:17 +0100 Subject: [PATCH 11/31] backup --- pkg/slayers/path/scion/base_spec.gobra | 4 +-- router/dataplane.go | 47 +++++++++++++++++++------- 2 files changed, 35 insertions(+), 16 deletions(-) diff --git a/pkg/slayers/path/scion/base_spec.gobra b/pkg/slayers/path/scion/base_spec.gobra index b12aec326..d06eba967 100644 --- a/pkg/slayers/path/scion/base_spec.gobra +++ b/pkg/slayers/path/scion/base_spec.gobra @@ -39,9 +39,7 @@ pred (b *Base) Mem() { acc(&b.PathMeta.SegLen[1]) && acc(&b.PathMeta.SegLen[2]) && 0 <= b.NumINF && b.NumINF <= MaxINFs && - // the program defines 64 as the maximum number of hops, - // but this does not seem to be enforced anywhere. - 0 <= b.NumHops && // b.NumHops <= MaxHops && + 0 <= b.NumHops && (0 < b.NumINF ==> 0 < b.NumHops) } diff --git a/router/dataplane.go b/router/dataplane.go index 3c494b5a6..b3bef7d23 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1787,7 +1787,7 @@ type macBuffersT struct { epicInput []byte } -// @ requires acc(&p.d, _) && acc(p.d.Mem(), _) +// @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) // @ requires acc(p.scionLayer.Mem(ub), R4) // @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) // @ requires ubLL == nil || ubLL === ub[startLL:endLL] @@ -1801,7 +1801,7 @@ type macBuffersT struct { // @ requires acc(&p.ingressID, R15) // @ requires acc(&p.buffer, R50) && p.buffer.Mem() // @ requires cause.ErrorMem() -// @ ensures acc(&p.d, _) +// @ ensures acc(&p.d, R20) // @ ensures acc(p.scionLayer.Mem(ub), R4) // @ ensures acc(&p.lastLayer, R55) && p.lastLayer != nil // @ ensures &p.scionLayer !== p.lastLayer ==> @@ -1925,6 +1925,7 @@ func (p *scionPacketProcessor) parsePath( /*@ ghost ub []byte @*/ ) (respr proce return processResult{}, nil } +// HERE // @ preserves acc(&p.infoField, R20) // @ preserves acc(&p.hopField, R20) // @ preserves acc(&p.d, R50) && acc(p.d.Mem(), _) @@ -2023,6 +2024,7 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte @*/ ) // Only check SrcIA if first hop, for transit this already checked by ingress router. // Note: SCMP error messages triggered by the sibling router may use paths that // don't start with the first hop. + // @ TODO() if p.path.IsFirstHop( /*@ ubPath @*/ ) && !srcIsLocal { return p.invalidSrcIA( /*@ nil, nil, 0, 0 @*/ ) } @@ -2043,7 +2045,7 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte @*/ ) } // invalidSrcIA is a helper to return an SCMP error for an invalid SrcIA. -// @ requires acc(&p.d, _) && acc(p.d.Mem(), _) +// @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) // @ requires acc(p.scionLayer.Mem(ub), R4) // @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) // @ requires ubLL == nil || ubLL === ub[startLL:endLL] @@ -2056,7 +2058,7 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte @*/ ) // @ requires sl.AbsSlice_Bytes(ub, 0, len(ub)) // @ requires acc(&p.ingressID, R15) // @ requires acc(&p.buffer, R50) && p.buffer.Mem() -// @ ensures acc(&p.d, _) +// @ ensures acc(&p.d, R20) // @ ensures acc(p.scionLayer.Mem(ub), R4) // @ ensures acc(&p.lastLayer, R55) && p.lastLayer != nil // @ ensures &p.scionLayer !== p.lastLayer ==> @@ -2084,7 +2086,7 @@ func (p *scionPacketProcessor) invalidSrcIA( /*@ ghost ub []byte, ghost ubLL []b } // invalidDstIA is a helper to return an SCMP error for an invalid DstIA. -// @ requires acc(&p.d, _) && acc(p.d.Mem(), _) +// @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) // @ requires acc(p.scionLayer.Mem(ub), R4) // @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) // @ requires ubLL == nil || ubLL === ub[startLL:endLL] @@ -2097,7 +2099,7 @@ func (p *scionPacketProcessor) invalidSrcIA( /*@ ghost ub []byte, ghost ubLL []b // @ requires sl.AbsSlice_Bytes(ub, 0, len(ub)) // @ requires acc(&p.ingressID, R15) // @ requires acc(&p.buffer, R50) && p.buffer.Mem() -// @ ensures acc(&p.d, _) +// @ ensures acc(&p.d, R20) // @ ensures acc(p.scionLayer.Mem(ub), R4) // @ ensures acc(&p.lastLayer, R55) && p.lastLayer != nil // @ ensures &p.scionLayer !== p.lastLayer ==> @@ -2563,15 +2565,34 @@ func (p *scionPacketProcessor) egressInterface() uint16 { } // @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) +// @ requires acc(p.scionLayer.Mem(ub), R4) +// @ requires p.scionLayer.ValidPathMetaData(ub) +// @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) +// @ requires ubLL == nil || ubLL === ub[startLL:endLL] +// @ requires acc(&p.lastLayer, R55) && p.lastLayer != nil +// @ requires &p.scionLayer !== p.lastLayer ==> +// @ acc(p.lastLayer.Mem(ubLL), R15) +// @ requires &p.scionLayer === p.lastLayer ==> +// @ ub === ubLL +// @ requires acc(&p.buffer, R50) && p.buffer.Mem() // @ preserves acc(&p.infoField, R20) // @ preserves acc(&p.hopField, R20) -// @ preserves acc(&p.ingressID, R20) +// @ preserves acc(&p.ingressID, R15) +// @ preserves sl.AbsSlice_Bytes(ub, 0, len(ub)) // @ ensures acc(&p.d, R20) // @ ensures p.d.validResult(respr, false) -// @ ensures respr.OutPkt != nil ==> -// @ reserr != nil && sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) // @ ensures reserr != nil ==> reserr.ErrorMem() -func (p *scionPacketProcessor) validateEgressUp() (respr processResult, reserr error) { +// @ ensures acc(p.scionLayer.Mem(ub), R4) +// @ ensures acc(&p.lastLayer, R55) && p.lastLayer != nil +// @ ensures &p.scionLayer !== p.lastLayer ==> +// @ acc(p.lastLayer.Mem(ubLL), R15) +// @ ensures acc(&p.buffer, R50) +// @ ensures respr === processResult{} ==> +// @ p.buffer.Mem() +// @ ensures respr !== processResult{} ==> +// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && +// @ sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +func (p *scionPacketProcessor) validateEgressUp( /*@ ghost ub []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int, @*/ ) (respr processResult, reserr error) { egressID := p.egressInterface() // @ p.d.getBfdSessionsMem() // @ ghost if p.d.bfdSessions != nil { unfold acc(accBfdSession(p.d.bfdSessions), _) } @@ -2593,8 +2614,7 @@ func (p *scionPacketProcessor) validateEgressUp() (respr processResult, reserr e Egress: uint64(egressID), } } - // @ TODO() - return p.packSCMP(typ, 0, scmpP, serrors.New("bfd session down") /*@, nil , nil, 0, 0, @*/) + return p.packSCMP(typ, 0, scmpP, serrors.New("bfd session down") /*@, ub , ubLL, startLL, endLL, @*/) } } // @ fold p.d.validResult(processResult{}, false) @@ -2971,7 +2991,8 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, // @ p.scionLayer.DowngradePerm(ub) return r, err /*@, false @*/ } - if r, err := p.validateEgressUp(); err != nil { + // @ ghost ubLL := llIsNil ? []byte(nil) : ub[startLL:endLL] + if r, err := p.validateEgressUp( /*@ ub, ubLL, startLL, endLL, @*/ ); err != nil { // @ p.scionLayer.DowngradePerm(ub) return r, err /*@, false @*/ } From f42467c84bbd0b98b9e8ca30d19fd735b3071f1e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Thu, 25 Apr 2024 15:20:37 +0200 Subject: [PATCH 12/31] fix parse and type errors --- pkg/slayers/path/scion/base_spec.gobra | 4 ++-- router/dataplane.go | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/pkg/slayers/path/scion/base_spec.gobra b/pkg/slayers/path/scion/base_spec.gobra index 2a32d2dd4..08482a112 100644 --- a/pkg/slayers/path/scion/base_spec.gobra +++ b/pkg/slayers/path/scion/base_spec.gobra @@ -40,8 +40,8 @@ pred (b *Base) Mem() { acc(&b.PathMeta.SegLen[0]) && acc(&b.PathMeta.SegLen[1]) && acc(&b.PathMeta.SegLen[2]) && - 0 <= b.NumINF && b.NumINF <= MaxINFs && - 0 <= b.NumHops && + 0 <= b.NumINF && b.NumINF <= MaxINFs && + 0 <= b.NumHops && b.NumHops <= MaxHops && (0 < b.NumINF ==> 0 < b.NumHops) } diff --git a/router/dataplane.go b/router/dataplane.go index 61eb1ec88..aa8e89213 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -2112,7 +2112,7 @@ func (p *scionPacketProcessor) validateIngressID( /*@ ghost oldPkt io.IO_pkt2, g &slayers.SCMPParameterProblem{Pointer: p.currentHopPointer( /*@ nil @*/ )}, serrors.New("ingress interface invalid", "pkt_ingress", pktIngressID, "router_ingress", p.ingressID), - /*@ nil , nil, 0, 0, dp @*/ + /*@ nil , nil, 0, 0, dp, @*/ ) } // @ reveal p.EqAbsHopField(oldPkt) @@ -2227,7 +2227,7 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte, ghos // @ sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) // @ ensures reserr != nil ==> reserr.ErrorMem() // @ decreases -func (p *scionPacketProcessor) invalidSrcIA( /*@ ghost ub, ghost ubLL []byte, ghost startLL, ghost endLL int, ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error) { +func (p *scionPacketProcessor) invalidSrcIA( /*@ ghost ub []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int, ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error) { // @ establishInvalidSrcIA() return p.packSCMP( slayers.SCMPTypeParameterProblem, @@ -2269,7 +2269,7 @@ func (p *scionPacketProcessor) invalidSrcIA( /*@ ghost ub, ghost ubLL []byte, gh // @ sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) // @ ensures reserr != nil ==> reserr.ErrorMem() // @ decreases -func (p *scionPacketProcessor) invalidDstIA( /*@ ghost ub, ghost ubLL []byte, ghost startLL, ghost endLL int, ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error) { +func (p *scionPacketProcessor) invalidDstIA( /*@ ghost ub []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int, ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error) { // @ establishInvalidDstIA() return p.packSCMP( slayers.SCMPTypeParameterProblem, @@ -2394,7 +2394,7 @@ func (p *scionPacketProcessor) validateEgressID( /*@ ghost oldPkt io.IO_pkt2, gh errCode, &slayers.SCMPParameterProblem{Pointer: p.currentHopPointer( /*@ nil @*/ )}, cannotRoute, - /*@ nil, nil, 0, 0, dp @*/ + /*@ nil, nil, 0, 0, dp, @*/ ) } From 9494a940df55da24715606163d7792a5543230da Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Thu, 25 Apr 2024 17:18:07 +0200 Subject: [PATCH 13/31] fix packscmp --- pkg/slayers/scion_spec.gobra | 4 ++-- router/dataplane.go | 41 ++++++++++++++++++------------------ 2 files changed, 22 insertions(+), 23 deletions(-) diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra index 01bd159e6..e8f695a0f 100644 --- a/pkg/slayers/scion_spec.gobra +++ b/pkg/slayers/scion_spec.gobra @@ -408,8 +408,8 @@ requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56) decreases pure func IsSupportedPkt(raw []byte) bool { return CmnHdrLen <= len(raw) && - let pathType := path.Type(GetPathType(raw)) in - let nextHdr := L4ProtocolType(GetNextHdr(raw)) in + let pathType := path.Type(GetPathType(raw)) in + let nextHdr := L4ProtocolType(GetNextHdr(raw)) in pathType == scion.PathType && nextHdr != L4SCMP } diff --git a/router/dataplane.go b/router/dataplane.go index aa8e89213..6b0738bd9 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1906,7 +1906,7 @@ type macBuffersT struct { // @ sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr != nil && respr.OutPkt != nil ==> -// @ absIO_val(dp, respr.OutPkt, respr.EgressID).isIO_val_Unsupported +// @ !slayers.IsSupportedPkt(respr.OutPkt) // @ decreases func (p *scionPacketProcessor) packSCMP( typ slayers.SCMPType, @@ -1929,17 +1929,15 @@ func (p *scionPacketProcessor) packSCMP( var scmpLayer /*@@@*/ slayers.SCMP // @ fold scmpLayer.NonInitMem() pld /*@ , start, end @*/ := p.lastLayer.LayerPayload( /*@ ubLL @*/ ) - /*@ - sl.SplitRange_Bytes(ub, startLL, endLL, writePerm) - maybeStartPld = start - maybeEndPld = end - if pld == nil { - scmpPldIsNil = true - fold sl.AbsSlice_Bytes(nil, 0, 0) - } else { - sl.SplitRange_Bytes(ubLL, start, end, writePerm) - } - @*/ + // @ sl.SplitRange_Bytes(ub, startLL, endLL, writePerm) + // @ maybeStartPld = start + // @ maybeEndPld = end + // @ if pld == nil { + // @ scmpPldIsNil = true + // @ fold sl.AbsSlice_Bytes(nil, 0, 0) + // @ } else { + // @ sl.SplitRange_Bytes(ubLL, start, end, writePerm) + // @ } // @ gopacket.AssertInvariantNilDecodeFeedback() err := scmpLayer.DecodeFromBytes(pld, gopacket.NilDecodeFeedback) if err != nil { @@ -1956,14 +1954,12 @@ func (p *scionPacketProcessor) packSCMP( } } - /*@ - ghost if llIsScmp { - ghost if !scmpPldIsNil { - sl.CombineRange_Bytes(ubLL, maybeStartPld, maybeEndPld, writePerm) - } - sl.CombineRange_Bytes(ub, startLL, endLL, writePerm) - } - @*/ + // @ ghost if llIsScmp { + // @ ghost if !scmpPldIsNil { + // @ sl.CombineRange_Bytes(ubLL, maybeStartPld, maybeEndPld, writePerm) + // @ } + // @ sl.CombineRange_Bytes(ub, startLL, endLL, writePerm) + // @ } rawSCMP, err := p.prepareSCMP(typ, code, scmpP, cause /*@ , ub @*/) // @ ghost result := processResult{OutPkt: rawSCMP} // @ fold p.d.validResult(result, false) @@ -3924,12 +3920,13 @@ func (b *bfdSend) Send(bfd *layers.BFD) error { return err } -// @ requires acc(&p.d, _) && acc(p.d.Mem(), _) +// @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires acc(p.scionLayer.Mem(ub), R4) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires sl.AbsSlice_Bytes(ub, 0, len(ub)) // @ requires acc(&p.ingressID, R15) // @ requires acc(&p.buffer, R55) && p.buffer.Mem() +// @ ensures acc(&p.d, R50) // @ ensures acc(p.scionLayer.Mem(ub), R4) // @ ensures sl.AbsSlice_Bytes(ub, 0, len(ub)) // @ ensures acc(&p.ingressID, R15) @@ -3940,6 +3937,8 @@ func (b *bfdSend) Send(bfd *layers.BFD) error { // @ ensures result == nil ==> // @ p.buffer.Mem() // @ ensures reserr != nil && reserr.ErrorMem() +// @ ensures reserr != nil && result != nil ==> +// @ !slayers.IsSupportedPkt(result) // @ decreases func (p *scionPacketProcessor) prepareSCMP( typ slayers.SCMPType, From 3eba8278ea8d358b43536fa09aeecf1718b8c6b3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 26 Apr 2024 15:50:41 +0200 Subject: [PATCH 14/31] backup --- pkg/slayers/path/scion/base.go | 17 ++------ pkg/slayers/path/scion/base_spec.gobra | 9 ++++ pkg/slayers/scion.go | 10 ++--- router/dataplane.go | 57 +++++++++++++------------- 4 files changed, 47 insertions(+), 46 deletions(-) diff --git a/pkg/slayers/path/scion/base.go b/pkg/slayers/path/scion/base.go index d74fe0c09..003a16d38 100644 --- a/pkg/slayers/path/scion/base.go +++ b/pkg/slayers/path/scion/base.go @@ -80,19 +80,10 @@ type Base struct { // @ requires s.NonInitMem() // @ preserves acc(sl.AbsSlice_Bytes(data, 0, len(data)), R50) -// @ ensures r != nil ==> (s.NonInitMem() && r.ErrorMem()) -// @ ensures r == nil ==> ( -// @ s.Mem() && -// @ let lenD := len(data) in -// @ MetaLen <= lenD && -// @ let b0 := sl.GetByte(data, 0, lenD, 0) in -// @ let b1 := sl.GetByte(data, 0, lenD, 1) in -// @ let b2 := sl.GetByte(data, 0, lenD, 2) in -// @ let b3 := sl.GetByte(data, 0, lenD, 3) in -// @ let line := binary.BigEndian.Uint32Spec(b0, b1, b2, b3) in -// @ let metaHdr := DecodedFrom(line) in -// @ metaHdr == s.GetMetaHdr() && -// @ s.InfsMatchHfs()) +// @ ensures r != nil ==> +// @ s.NonInitMem() && r.ErrorMem() +// @ ensures r == nil ==> +// @ s.Mem() && s.DecodeFromBytesSpec(data) && s.InfsMatchHfs() // @ ensures len(data) < MetaLen ==> r != nil // @ decreases func (s *Base) DecodeFromBytes(data []byte) (r error) { diff --git a/pkg/slayers/path/scion/base_spec.gobra b/pkg/slayers/path/scion/base_spec.gobra index 08482a112..0ea343894 100644 --- a/pkg/slayers/path/scion/base_spec.gobra +++ b/pkg/slayers/path/scion/base_spec.gobra @@ -361,6 +361,15 @@ pure func (m MetaHdr) DecodeFromBytesSpec(b []byte) bool { DecodedFrom(line) == m } +ghost +requires acc(s.Mem(), _) +requires acc(sl.AbsSlice_Bytes(b, 0, len(b)), _) +decreases +pure func (s *Base) DecodeFromBytesSpec(b []byte) bool { + return unfolding acc(s.Mem(), _) in + s.PathMeta.DecodeFromBytesSpec(b) +} + ghost decreases pure func (m MetaHdr) SegsInBounds() bool { diff --git a/pkg/slayers/scion.go b/pkg/slayers/scion.go index bb713a41d..cd8cd906c 100644 --- a/pkg/slayers/scion.go +++ b/pkg/slayers/scion.go @@ -418,11 +418,11 @@ func (s *SCION) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback) (res er // @ fold s.NonInitMem() return err } - /*@ ghost if typeOf(s.Path) == type[*onehop.Path] { - s.Path.(*onehop.Path).InferSizeUb(data[offset : offset+pathLen]) - assert s.Path.Len(data[offset : offset+pathLen]) <= len(data[offset : offset+pathLen]) - assert CmnHdrLen + s.AddrHdrLenSpecInternal() + s.Path.Len(data[offset : offset+pathLen]) <= len(data) - } @*/ + // @ ghost if typeOf(s.Path) == type[*onehop.Path] { + // @ s.Path.(*onehop.Path).InferSizeUb(data[offset : offset+pathLen]) + // @ assert s.Path.Len(data[offset : offset+pathLen]) <= len(data[offset : offset+pathLen]) + // @ assert CmnHdrLen + s.AddrHdrLenSpecInternal() + s.Path.Len(data[offset : offset+pathLen]) <= len(data) + // @ } s.Contents = data[:hdrBytes] s.Payload = data[hdrBytes:] diff --git a/router/dataplane.go b/router/dataplane.go index 6b0738bd9..58edae0bf 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1972,6 +1972,10 @@ func (p *scionPacketProcessor) packSCMP( // @ requires p.path === p.scionLayer.GetPath(ub) // @ requires acc(&p.hopField) && acc(&p.infoField) // @ requires acc(sl.AbsSlice_Bytes(ub, 0, len(ub)), R1) +// pres for IO-spec +// @ requires dp.Valid() +// @ requires slayers.ValidPktMetaHdr(ub) && p.scionLayer.EqAbsHeader(ub) +// @ requires len(absPkt(dp, ub).CurrSeg.Future) > 0 // @ ensures acc(sl.AbsSlice_Bytes(ub, 0, len(ub)), R1) // @ ensures acc(&p.d, R50) // @ ensures acc(p.scionLayer.Mem(ub), R6) @@ -1980,20 +1984,17 @@ func (p *scionPacketProcessor) packSCMP( // @ ensures acc(&p.hopField) && acc(&p.infoField) // @ ensures respr === processResult{} // @ ensures reserr == nil ==> ( -// @ let ubPath := p.scionLayer.UBPath(ub) in -// @ unfolding acc(p.scionLayer.Mem(ub), R10) in -// @ p.path.GetCurrHF(ubPath) < p.path.GetNumHops(ubPath)) +// @ let ubPath := p.scionLayer.UBPath(ub) in +// @ unfolding acc(p.scionLayer.Mem(ub), R10) in +// @ p.path.GetCurrHF(ubPath) < p.path.GetNumHops(ubPath)) // @ ensures acc(p.scionLayer.Mem(ub), R6) // @ ensures p.d.validResult(respr, false) // @ ensures reserr == nil ==> ( -// @ let ubPath := p.scionLayer.UBPath(ub) in -// @ unfolding acc(p.scionLayer.Mem(ub), R10) in +// @ let ubPath := p.scionLayer.UBPath(ub) in +// @ unfolding acc(p.scionLayer.Mem(ub), R10) in // @ p.path.GetCurrINF(ubPath) < p.path.GetNumINF(ubPath)) // @ ensures reserr != nil ==> reserr.ErrorMem() -// contracts for IO-spec -// @ requires dp.Valid() -// @ requires slayers.ValidPktMetaHdr(ub) && p.scionLayer.EqAbsHeader(ub) -// @ requires len(absPkt(dp, ub).CurrSeg.Future) > 0 +// posts for IO-spec // @ ensures dp.Valid() // @ ensures reserr == nil ==> slayers.ValidPktMetaHdr(ub) && p.scionLayer.EqAbsHeader(ub) // @ ensures reserr == nil ==> len(absPkt(dp, ub).CurrSeg.Future) > 0 @@ -4232,15 +4233,15 @@ func decodeLayers(data []byte, base *slayers.SCION, // @ invariant idx == -1 ==> (last === base && oldStart == 0 && oldEnd == len(oldData)) // @ invariant 0 <= idx ==> (processed[idx] && last === opts[idx]) // @ invariant forall i int :: {&opts[i]}{processed[i]} 0 <= i && i < len(opts) ==> - // @ (processed[i] ==> (0 <= offsets[i].start && offsets[i].start <= offsets[i].end && offsets[i].end <= len(data))) + // @ (processed[i] ==> (0 <= offsets[i].start && offsets[i].start <= offsets[i].end && offsets[i].end <= len(data))) // @ invariant forall i int :: {&opts[i]}{processed[i]} 0 <= i && i < len(opts) ==> - // @ ((processed[i] && !offsets[i].isNil) ==> opts[i].Mem(oldData[offsets[i].start:offsets[i].end])) + // @ ((processed[i] && !offsets[i].isNil) ==> opts[i].Mem(oldData[offsets[i].start:offsets[i].end])) // @ invariant forall i int :: {&opts[i]}{processed[i]} 0 <= i && i < len(opts) ==> - // @ ((processed[i] && offsets[i].isNil) ==> opts[i].Mem(nil)) + // @ ((processed[i] && offsets[i].isNil) ==> opts[i].Mem(nil)) // @ invariant forall i int :: {&opts[i]}{processed[i]} 0 < len(opts) && i0 <= i && i < len(opts) ==> - // @ !processed[i] + // @ !processed[i] // @ invariant forall i int :: {&opts[i]}{processed[i]} 0 <= i && i < len(opts) ==> - // @ (!processed[i] ==> opts[i].NonInitMem()) + // @ (!processed[i] ==> opts[i].NonInitMem()) // @ invariant gopacket.NilDecodeFeedback.Mem() // @ invariant 0 <= oldStart && oldStart <= oldEnd && oldEnd <= len(oldData) // @ decreases len(opts) - i0 @@ -4250,11 +4251,11 @@ func decodeLayers(data []byte, base *slayers.SCION, // @ ghost var pos offsetPair // @ ghost var ub []byte // @ ghost if idx == -1 { - // @ pos = offsetPair{0, len(oldData), false} - // @ ub = oldData + // @ pos = offsetPair{0, len(oldData), false} + // @ ub = oldData // @ } else { - // @ pos = offsets[idx] - // @ if pos.isNil { ub = nil } else { ub = oldData[pos.start:pos.end] } + // @ pos = offsets[idx] + // @ if pos.isNil { ub = nil } else { ub = oldData[pos.start:pos.end] } // @ } if layerClassTmp.Contains(last.NextLayerType( /*@ ub @*/ )) { data /*@ , start, end @*/ := last.LayerPayload( /*@ ub @*/ ) @@ -4264,7 +4265,7 @@ func decodeLayers(data []byte, base *slayers.SCION, // @ ghost if data == nil { // @ sl.NilAcc_Bytes() // @ } else { - // @ sl.SplitRange_Bytes(oldData, oldStart, oldEnd, R40) + // @ sl.SplitRange_Bytes(oldData, oldStart, oldEnd, R40) // @ } if err := opt.DecodeFromBytes(data, gopacket.NilDecodeFeedback); err != nil { // @ ghost if data != nil { sl.CombineRange_Bytes(oldData, oldStart, oldEnd, R40) } @@ -4279,22 +4280,22 @@ func decodeLayers(data []byte, base *slayers.SCION, // @ invariant forall i, j int :: {&opts[i], &opts[j]} 0 <= i && i < j && j < len(opts) ==> opts[i] !== opts[j] // @ invariant forall i int :: {&opts[i]} 0 <= i && i < len(opts) ==> opts[i] != nil // @ invariant forall i int :: {&opts[i]}{processed[i]} 0 <= i && i < len(opts) ==> - // @ (processed[i] ==> (0 <= offsets[i].start && offsets[i].start <= offsets[i].end && offsets[i].end <= len(oldData))) + // @ (processed[i] ==> (0 <= offsets[i].start && offsets[i].start <= offsets[i].end && offsets[i].end <= len(oldData))) // @ invariant forall i int :: {&opts[i]}{processed[i]} 0 <= i && i < len(opts) ==> - // @ ((processed[i] && !offsets[i].isNil) ==> opts[i].Mem(oldData[offsets[i].start:offsets[i].end])) + // @ ((processed[i] && !offsets[i].isNil) ==> opts[i].Mem(oldData[offsets[i].start:offsets[i].end])) // @ invariant forall i int :: {&opts[i]}{processed[i]} 0 <= i && i < len(opts) ==> - // @ ((processed[i] && offsets[i].isNil) ==> opts[i].Mem(nil)) + // @ ((processed[i] && offsets[i].isNil) ==> opts[i].Mem(nil)) // @ invariant forall i int :: {&opts[i]}{processed[i]} 0 <= i && i < len(opts) ==> - // @ (!processed[i] ==> opts[i].NonInitMem()) + // @ (!processed[i] ==> opts[i].NonInitMem()) // @ invariant forall i int :: {&opts[i]}{processed[i]} 0 < len(opts) && c < i && i < len(opts) ==> - // @ !processed[i] + // @ !processed[i] // @ decreases c // @ for c := i0-1; 0 <= c; c=c-1 { - // @ if processed[c] { - // @ off := offsets[c] - // @ if off.isNil { + // @ if processed[c] { + // @ off := offsets[c] + // @ if off.isNil { // @ opts[c].DowngradePerm(nil) - // @ } else { + // @ } else { // @ opts[c].DowngradePerm(oldData[off.start:off.end]) // @ } // @ } From cef60404af9c2a1a0675787baaae8b8c0f851c59 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 26 Apr 2024 17:33:56 +0200 Subject: [PATCH 15/31] backup --- pkg/slayers/path/scion/base_spec.gobra | 6 ++---- router/dataplane.go | 30 ++++++++++++++++++-------- 2 files changed, 23 insertions(+), 13 deletions(-) diff --git a/pkg/slayers/path/scion/base_spec.gobra b/pkg/slayers/path/scion/base_spec.gobra index 0ea343894..097c44c8d 100644 --- a/pkg/slayers/path/scion/base_spec.gobra +++ b/pkg/slayers/path/scion/base_spec.gobra @@ -73,8 +73,7 @@ pure func (b Base) ValidCurrIdxsSpec() bool { (forall i int :: { b.PathMeta.SegLen[i] } 0 <= i && i < b.NumINF ==> b.PathMeta.SegLen[i] != 0) && (forall i int :: { b.PathMeta.SegLen[i] } b.NumINF <= i && i < MaxINFs ==> - b.PathMeta.SegLen[i] == 0) && - b.PathMeta.CurrINF == b.InfForHfSpec(b.PathMeta.CurrHF) + b.PathMeta.SegLen[i] == 0) } ghost @@ -282,8 +281,7 @@ pure func (b AbsBase) ValidCurrIdxsSpec() bool { (forall i int :: { b.PathMeta.SegLen[i] } 0 <= i && i < b.NumINF ==> b.PathMeta.SegLen[i] != 0) && (forall i int :: { b.PathMeta.SegLen[i] } b.NumINF <= i && i < MaxINFs ==> - b.PathMeta.SegLen[i] == 0) && - b.PathMeta.CurrINF == b.InfForHfSpec(b.PathMeta.CurrHF) + b.PathMeta.SegLen[i] == 0) } ghost diff --git a/router/dataplane.go b/router/dataplane.go index 58edae0bf..5ab273fe0 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -2030,19 +2030,23 @@ func (p *scionPacketProcessor) parsePath( /*@ ghost ub []byte, ghost dp io.DataP } // HERE +// @ requires dp.Valid() // @ preserves acc(&p.infoField, R20) // @ preserves acc(&p.hopField, R20) +// @ preserves acc(&p.path, R20) +// @ preserves acc(&p.ingressID, R20) // @ preserves acc(&p.d, R50) && acc(p.d.Mem(), _) +// @ preserves acc(p.scionLayer.Mem(ubScionL), R3) +// @ preserves p.path == p.scionLayer.GetPath(ubScionL) // @ ensures p.d.validResult(respr, false) // @ ensures respr.OutPkt != nil ==> // @ reserr != nil && sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) // @ ensures reserr != nil ==> reserr.ErrorMem() -// contracts for IO-spec -// @ requires dp.Valid() +// posts for IO // @ ensures reserr != nil && respr.OutPkt != nil ==> // @ absIO_val(dp, respr.OutPkt, respr.EgressID).isIO_val_Unsupported // @ decreases -func (p *scionPacketProcessor) validateHopExpiry( /*@ ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error) { +func (p *scionPacketProcessor) validateHopExpiry( /*@ ghost dp io.DataPlaneSpec, ghost ubScionL []byte @*/ ) (respr processResult, reserr error) { expiration := util.SecsToTime(p.infoField.Timestamp). Add(path.ExpTimeToDuration(p.hopField.ExpTime)) expired := expiration.Before(time.Now()) @@ -2050,7 +2054,7 @@ func (p *scionPacketProcessor) validateHopExpiry( /*@ ghost dp io.DataPlaneSpec // @ fold p.d.validResult(respr, false) return processResult{}, nil } - // @ ToDoAfterScionFix("https://github.com/scionproto/scion/issues/4482") // depends on packSCMP + // ToDoAfterScionFix("https://github.com/scionproto/scion/issues/4482") // depends on packSCMP // (VerifiedSCION): adapt; note that packSCMP always returns an empty addr and conn and // when the err is nil, it returns the bytes of p.buffer. This should be a magic wand // that is consumed after sending the reply. For now, we are making this simplifying @@ -2064,9 +2068,17 @@ func (p *scionPacketProcessor) validateHopExpiry( /*@ ghost dp io.DataPlaneSpec return p.packSCMP( slayers.SCMPTypeParameterProblem, slayers.SCMPCodePathExpired, - &slayers.SCMPParameterProblem{Pointer: p.currentHopPointer( /*@ nil @*/ )}, - serrors.New("expired hop", "cons_dir", p.infoField.ConsDir, "if_id", p.ingressID, - "curr_inf", p.path.PathMeta.CurrINF, "curr_hf", p.path.PathMeta.CurrHF), + &slayers.SCMPParameterProblem{Pointer: p.currentHopPointer( /*@ ubScionL @*/ )}, + serrors.New( + "expired hop", + "cons_dir", + /*@ unfolding acc(p.scionLayer.Mem(ubScionL), R20) in @*/ p.infoField.ConsDir, + "if_id", + p.ingressID, + "curr_inf", + /*@ unfolding acc(p.scionLayer.Mem(ubScionL), R20) in @*/ p.path.PathMeta.CurrINF, + "curr_hf", + /*@ unfolding acc(p.scionLayer.Mem(ubScionL), R20) in @*/ p.path.PathMeta.CurrHF), /*@ nil , nil, 0, 0, dp, @*/ ) } @@ -3314,7 +3326,7 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, // @ p.scionLayer.DowngradePerm(ub) return r, err /*@, false, absReturnErr(dp, r) @*/ } - if r, err := p.validateHopExpiry( /*@ dp @*/ ); err != nil { + if r, err := p.validateHopExpiry( /*@ dp, ub @*/ ); err != nil { // @ p.scionLayer.DowngradePerm(ub) return r, err /*@, false, absReturnErr(dp, r) @*/ } @@ -3390,7 +3402,7 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, // @ assert absPkt(dp, ub) == AbsDoXover(nextPkt) // @ AbsValidateIngressIDXoverLemma(nextPkt, AbsDoXover(nextPkt), path.ifsToIO_ifs(p.ingressID)) // @ nextPkt = absPkt(dp, ub) - if r, err := p.validateHopExpiry( /*@ dp @*/ ); err != nil { + if r, err := p.validateHopExpiry( /*@ dp, ub @*/ ); err != nil { // @ p.scionLayer.DowngradePerm(ub) return r, serrors.WithCtx(err, "info", "after xover") /*@, false, absReturnErr(dp, r) @*/ } From e7dab5f55462588bfaaee845173d5ea133e8cd44 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 3 May 2024 20:51:22 +0200 Subject: [PATCH 16/31] kill branches for now --- pkg/slayers/path/scion/base_spec.gobra | 14 ++++++++++++++ router/dataplane.go | 7 +++++-- 2 files changed, 19 insertions(+), 2 deletions(-) diff --git a/pkg/slayers/path/scion/base_spec.gobra b/pkg/slayers/path/scion/base_spec.gobra index 097c44c8d..75620a731 100644 --- a/pkg/slayers/path/scion/base_spec.gobra +++ b/pkg/slayers/path/scion/base_spec.gobra @@ -76,6 +76,12 @@ pure func (b Base) ValidCurrIdxsSpec() bool { b.PathMeta.SegLen[i] == 0) } +ghost +decreases +pure func (b Base) CurrInfMatchesCurrHF() bool { + return b.PathMeta.CurrINF == b.InfForHfSpec(b.PathMeta.CurrHF) +} + ghost decreases pure func (b Base) InfsMatchHfsSpec() bool { @@ -284,6 +290,14 @@ pure func (b AbsBase) ValidCurrIdxsSpec() bool { b.PathMeta.SegLen[i] == 0) } +ghost +opaque +requires b.ValidCurrIdxsSpec() +decreases +pure func (b AbsBase) CurrInfMatchesCurrHF() bool { + return b.PathMeta.CurrINF == b.InfForHfSpec(b.PathMeta.CurrHF) +} + ghost decreases pure func (b AbsBase) ValidCurrInfSpec() bool { diff --git a/router/dataplane.go b/router/dataplane.go index 388260ab5..1d18e8d13 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -2054,7 +2054,7 @@ func (p *scionPacketProcessor) validateHopExpiry( /*@ ghost dp io.DataPlaneSpec, // @ fold p.d.validResult(respr, false) return processResult{}, nil } - // ToDoAfterScionFix("https://github.com/scionproto/scion/issues/4482") // depends on packSCMP + // @ ToDoAfterScionFix("https://github.com/scionproto/scion/issues/4482") // depends on packSCMP // (VerifiedSCION): adapt; note that packSCMP always returns an empty addr and conn and // when the err is nil, it returns the bytes of p.buffer. This should be a magic wand // that is consumed after sending the reply. For now, we are making this simplifying @@ -2172,19 +2172,22 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte, ghos // Only check SrcIA if first hop, for transit this already checked by ingress router. // Note: SCMP error messages triggered by the sibling router may use paths that // don't start with the first hop. - // @ TODO() if p.path.IsFirstHop( /*@ ubPath @*/ ) && !srcIsLocal { + // @ TODO() return p.invalidSrcIA( /*@ nil, nil, 0, 0, dp @*/ ) } if dstIsLocal { + // @ TODO() return p.invalidDstIA( /*@ nil, nil, 0, 0, dp @*/ ) } } else { // Inbound if srcIsLocal { + // @ TODO() return p.invalidSrcIA( /*@ nil, nil, 0, 0, dp @*/ ) } if p.path.IsLastHop( /*@ ubPath @*/ ) != dstIsLocal { + // @ TODO() return p.invalidDstIA( /*@ nil, nil, 0, 0, dp @*/ ) } // @ ghost if(p.path.IsLastHopSpec(ubPath)) { From ba85226a42e5be1bd834797f1160798cb00fc099 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Mon, 6 May 2024 13:50:09 +0200 Subject: [PATCH 17/31] backup --- router/dataplane.go | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/router/dataplane.go b/router/dataplane.go index 0e2dbdc9d..d92ea373e 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -3380,7 +3380,9 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, // @ p.d.getLocalIA() if /*@ unfolding acc(p.scionLayer.Mem(ub), R50) in (unfolding acc(p.scionLayer.HeaderMem(ub[slayers.CmnHdrLen:]), R55) in @*/ p.scionLayer.DstIA /*@ ) @*/ == p.d.localIA { // @ assert p.DstIsLocalIngressID(ub) - // @ assert unfolding acc(p.scionLayer.Mem(ub), R50) in (unfolding acc(p.scionLayer.HeaderMem(ub[slayers.CmnHdrLen:]), R55) in p.scionLayer.DstIA) == p.d.localIA + // @ assert unfolding acc(p.scionLayer.Mem(ub), R50) in + // @ (unfolding acc(p.scionLayer.HeaderMem(ub[slayers.CmnHdrLen:]), R55) in + // @ p.scionLayer.DstIA) == p.d.localIA // @ p.LocalDstLemma(ub, dp) // @ assert p.ingressID != 0 // @ assert len(nextPkt.CurrSeg.Future) == 1 From 2e6f4dbbec80faf60976e911fb5d27b07558aa85 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Mon, 6 May 2024 17:53:38 +0200 Subject: [PATCH 18/31] backup --- router/dataplane.go | 55 ++++++++++++++++++++++++++------------------ router/io-spec.gobra | 11 +++++++++ 2 files changed, 43 insertions(+), 23 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index d92ea373e..20f6d3e5b 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1890,7 +1890,7 @@ type macBuffersT struct { // @ ub === ubLL // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires sl.AbsSlice_Bytes(ub, 0, len(ub)) -// @ requires acc(&p.ingressID, R15) +// @ requires acc(&p.ingressID, R45) // @ requires acc(&p.buffer, R50) && p.buffer.Mem() // @ requires cause.ErrorMem() // @ requires dp.Valid() @@ -1900,7 +1900,7 @@ type macBuffersT struct { // @ ensures &p.scionLayer !== p.lastLayer ==> // @ acc(p.lastLayer.Mem(ubLL), R15) // @ ensures sl.AbsSlice_Bytes(ub, 0, len(ub)) -// @ ensures acc(&p.ingressID, R15) +// @ ensures acc(&p.ingressID, R45) // @ ensures p.d.validResult(respr, false) // @ ensures acc(&p.buffer, R50) // @ ensures respr === processResult{} ==> @@ -2874,12 +2874,13 @@ func (p *scionPacketProcessor) ingressInterface( /*@ ghost ubPath []byte @*/ ) u // @ requires acc(&p.infoField, R21) // @ requires acc(&p.hopField, R21) -// @ ensures acc(&p.infoField, R21) -// @ ensures acc(&p.hopField, R21) -// contracts for IO-spec +// pres for IO: // @ requires len(oldPkt.CurrSeg.Future) > 0 // @ requires p.EqAbsInfoField(oldPkt) // @ requires p.EqAbsHopField(oldPkt) +// @ ensures acc(&p.infoField, R21) +// @ ensures acc(&p.hopField, R21) +// posts for IO: // @ ensures p.EqAbsInfoField(oldPkt) // @ ensures p.EqAbsHopField(oldPkt) // @ ensures AbsEgressInterfaceConstraint(oldPkt, path.ifsToIO_ifs(egress)) @@ -2906,9 +2907,17 @@ func (p *scionPacketProcessor) egressInterface( /*@ ghost oldPkt io.IO_pkt2 @*/ // @ requires &p.scionLayer === p.lastLayer ==> // @ ub === ubLL // @ requires acc(&p.buffer, R50) && p.buffer.Mem() -// @ preserves acc(&p.infoField, R20) -// @ preserves acc(&p.hopField, R20) -// @ preserves acc(&p.ingressID, R21) +// @ requires acc(&p.infoField, R20) +// @ requires acc(&p.hopField, R20) +// @ requires acc(&p.ingressID, R21) +// pres for IO: +// @ requires dp.Valid() +// @ requires len(oldPkt.CurrSeg.Future) > 0 +// @ requires p.EqAbsInfoField(oldPkt) +// @ requires p.EqAbsHopField(oldPkt) +// @ ensures acc(&p.infoField, R20) +// @ ensures acc(&p.hopField, R20) +// @ ensures acc(&p.ingressID, R21) // @ preserves sl.AbsSlice_Bytes(ub, 0, len(ub)) // @ ensures acc(&p.d, R20) // @ ensures p.d.validResult(respr, false) @@ -2923,11 +2932,7 @@ func (p *scionPacketProcessor) egressInterface( /*@ ghost oldPkt io.IO_pkt2 @*/ // @ ensures respr !== processResult{} ==> // @ p.buffer.MemWithoutUBuf(respr.OutPkt) && // @ sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) -// contracts for IO-spec -// @ requires dp.Valid() -// @ requires len(oldPkt.CurrSeg.Future) > 0 -// @ requires p.EqAbsInfoField(oldPkt) -// @ requires p.EqAbsHopField(oldPkt) +// posts for IO: // @ ensures reserr != nil && respr.OutPkt != nil ==> // @ absIO_val(dp, respr.OutPkt, respr.EgressID).isIO_val_Unsupported // @ decreases 0 if sync.IgnoreBlockingForTermination() @@ -2953,7 +2958,11 @@ func (p *scionPacketProcessor) validateEgressUp( /*@ ghost ub []byte, ghost ubLL Egress: uint64(egressID), } } - return p.packSCMP(typ, 0, scmpP, serrors.New("bfd session down") /*@, ub , ubLL, startLL, endLL, dp, @*/) + tmpRes, tmpErr := p.packSCMP(typ, 0, scmpP, serrors.New("bfd session down") /*@, ub , ubLL, startLL, endLL, dp, @*/) + // @ ghost if tmpErr != nil && tmpRes.OutPkt != nil { + // @ AbsUnsupportedPktIsUnsupportedVal(dp, tmpRes.OutPkt, tmpRes.EgressID) + // @ } + return tmpRes, tmpErr } } // @ fold p.d.validResult(processResult{}, false) @@ -3071,9 +3080,9 @@ func (p *scionPacketProcessor) ingressRouterAlertFlag() (res *bool) { // @ requires acc(p.scionLayer.Mem(ub), R13) // @ requires p.path === p.scionLayer.GetPath(ub) // @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) -// @ requires sl.AbsSlice_Bytes(ub, 0, len(ub)) -// @ requires acc(&p.infoField, R20) -// @ requires acc(&p.hopField) +// @ requires sl.AbsSlice_Bytes(ub, 0, len(ub)) +// @ requires acc(&p.infoField, R20) +// @ requires acc(&p.hopField) // @ preserves acc(&p.lastLayer, R19) // @ preserves p.lastLayer != nil // @ preserves (&p.scionLayer !== p.lastLayer && llIsNil) ==> @@ -3081,9 +3090,9 @@ func (p *scionPacketProcessor) ingressRouterAlertFlag() (res *bool) { // @ preserves (&p.scionLayer !== p.lastLayer && !llIsNil) ==> // @ acc(p.lastLayer.Mem(ub[startLL:endLL]), R15) // @ preserves acc(&p.ingressID, R21) -// @ ensures acc(&p.infoField, R20) -// @ ensures acc(&p.hopField) -// @ ensures sl.AbsSlice_Bytes(ub, 0, len(ub)) +// @ ensures acc(&p.infoField, R20) +// @ ensures acc(&p.hopField) +// @ ensures sl.AbsSlice_Bytes(ub, 0, len(ub)) // @ ensures acc(&p.path, R20) // @ ensures acc(p.scionLayer.Mem(ub), R13) // @ ensures acc(&p.d, R20) @@ -3277,7 +3286,7 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost // @ requires p.scionLayer.Mem(ub) // @ requires p.path == p.scionLayer.GetPath(ub) // @ requires sl.AbsSlice_Bytes(ub, 0, len(ub)) -// @ requires acc(&p.ingressID, R20) +// @ requires acc(&p.ingressID, R20) // @ requires acc(&p.segmentChange) && !p.segmentChange // @ preserves acc(&p.srcAddr, R10) && acc(p.srcAddr.Mem(), _) // @ preserves acc(&p.lastLayer, R10) @@ -3943,12 +3952,12 @@ func (b *bfdSend) Send(bfd *layers.BFD) error { // @ requires acc(p.scionLayer.Mem(ub), R4) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires sl.AbsSlice_Bytes(ub, 0, len(ub)) -// @ requires acc(&p.ingressID, R15) +// @ requires acc(&p.ingressID, R50) // @ requires acc(&p.buffer, R55) && p.buffer.Mem() // @ ensures acc(&p.d, R50) // @ ensures acc(p.scionLayer.Mem(ub), R4) // @ ensures sl.AbsSlice_Bytes(ub, 0, len(ub)) -// @ ensures acc(&p.ingressID, R15) +// @ ensures acc(&p.ingressID, R50) // @ ensures acc(&p.buffer, R55) // @ ensures result != nil ==> // @ sl.AbsSlice_Bytes(result, 0, len(result)) && diff --git a/router/io-spec.gobra b/router/io-spec.gobra index 9b77fe93a..efd81f585 100644 --- a/router/io-spec.gobra +++ b/router/io-spec.gobra @@ -83,6 +83,17 @@ pure func absIO_val(dp io.DataPlaneSpec, raw []byte, ingressID uint16) (val io.I absIO_val_Unsupported(raw, ingressID) } +ghost +requires dp.Valid() +requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56) +requires !slayers.IsSupportedPkt(raw) +ensures acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56) +ensures absIO_val(dp, raw, ingressID).isIO_val_Unsupported +decreases +func AbsUnsupportedPktIsUnsupportedVal(dp io.DataPlaneSpec, raw []byte, ingressID uint16) { + reveal absIO_val(dp, raw, ingressID) +} + ghost requires dp.Valid() requires respr.OutPkt != nil ==> From efa659cfb72ffad1ad2491b9eabe4e019536abb4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Thu, 9 May 2024 15:54:48 +0200 Subject: [PATCH 19/31] remove files pushed by mistake --- .bazelbsp/BUILD | 0 .bazelbsp/WORKSPACE | 0 .bazelbsp/aspects/BUILD | 5 - .bazelbsp/aspects/core.bzl | 195 ------------------ .bazelbsp/aspects/extensions.bzl | 3 - .../aspects/rules/android/android_info.bzl | 83 -------- .bazelbsp/aspects/rules/cpp/cpp_info.bzl | 14 -- .bazelbsp/aspects/rules/java/java_info.bzl | 60 ------ .bazelbsp/aspects/rules/jvm/jvm_info.bzl | 166 --------------- .../aspects/rules/kt/kt_info.bzl.template | 45 ---- .../aspects/rules/python/python_info.bzl | 34 --- .bazelbsp/aspects/rules/rust/rust_info.bzl | 80 ------- .bazelbsp/aspects/rules/scala/scala_info.bzl | 49 ----- .bazelbsp/aspects/runtime_classpath_query.bzl | 24 --- .bazelbsp/aspects/utils/utils.bzl | 105 ---------- .bazelbsp/bazelbsp.log | 132 ------------ .bsp/bazelbsp.json | 19 -- .gitignore | 2 + 18 files changed, 2 insertions(+), 1014 deletions(-) delete mode 100644 .bazelbsp/BUILD delete mode 100644 .bazelbsp/WORKSPACE delete mode 100644 .bazelbsp/aspects/BUILD delete mode 100644 .bazelbsp/aspects/core.bzl delete mode 100644 .bazelbsp/aspects/extensions.bzl delete mode 100644 .bazelbsp/aspects/rules/android/android_info.bzl delete mode 100644 .bazelbsp/aspects/rules/cpp/cpp_info.bzl delete mode 100644 .bazelbsp/aspects/rules/java/java_info.bzl delete mode 100644 .bazelbsp/aspects/rules/jvm/jvm_info.bzl delete mode 100644 .bazelbsp/aspects/rules/kt/kt_info.bzl.template delete mode 100644 .bazelbsp/aspects/rules/python/python_info.bzl delete mode 100644 .bazelbsp/aspects/rules/rust/rust_info.bzl delete mode 100644 .bazelbsp/aspects/rules/scala/scala_info.bzl delete mode 100644 .bazelbsp/aspects/runtime_classpath_query.bzl delete mode 100644 .bazelbsp/aspects/utils/utils.bzl delete mode 100644 .bazelbsp/bazelbsp.log delete mode 100644 .bsp/bazelbsp.json diff --git a/.bazelbsp/BUILD b/.bazelbsp/BUILD deleted file mode 100644 index e69de29bb..000000000 diff --git a/.bazelbsp/WORKSPACE b/.bazelbsp/WORKSPACE deleted file mode 100644 index e69de29bb..000000000 diff --git a/.bazelbsp/aspects/BUILD b/.bazelbsp/aspects/BUILD deleted file mode 100644 index d6b6ba374..000000000 --- a/.bazelbsp/aspects/BUILD +++ /dev/null @@ -1,5 +0,0 @@ -filegroup( - name = "aspects", - srcs = glob(["**"]), - visibility = ["//visibility:public"], -) diff --git a/.bazelbsp/aspects/core.bzl b/.bazelbsp/aspects/core.bzl deleted file mode 100644 index 8305b4728..000000000 --- a/.bazelbsp/aspects/core.bzl +++ /dev/null @@ -1,195 +0,0 @@ -load("//aspects:utils/utils.bzl", "abs", "create_struct", "file_location", "get_aspect_ids", "update_sync_output_groups") -load("//aspects:extensions.bzl", "EXTENSIONS", "TOOLCHAINS") - -def create_all_extension_info(target, ctx, output_groups, dep_targets): - info = [create_extension_info(target = target, ctx = ctx, output_groups = output_groups, dep_targets = dep_targets) for create_extension_info in EXTENSIONS] - return [(file, data) for file, data in info if file != None] - -def _collect_target_from_attr(rule_attrs, attr_name, result): - """Collects the targets from the given attr into the result.""" - if not hasattr(rule_attrs, attr_name): - return - attr_value = getattr(rule_attrs, attr_name) - type_name = type(attr_value) - if type_name == "Target": - result.append(attr_value) - elif type_name == "list": - result.extend(attr_value) - -def is_valid_aspect_target(target): - return hasattr(target, "bsp_info") - -def collect_targets_from_attrs(rule_attrs, attrs): - result = [] - for attr_name in attrs: - _collect_target_from_attr(rule_attrs, attr_name, result) - return [target for target in result if is_valid_aspect_target(target)] - -COMPILE = 0 -RUNTIME = 1 - -COMPILE_DEPS = [ - "deps", - "jars", - "exports", - "associates", - "proc_macro_deps", -] - -PRIVATE_COMPILE_DEPS = [ - "_java_toolchain", - "_scala_toolchain", - "_scalac", - "_jvm", - "runtime_jdk", -] - -RUNTIME_DEPS = [ - "runtime_deps", -] - -ALL_DEPS = COMPILE_DEPS + PRIVATE_COMPILE_DEPS + RUNTIME_DEPS - -def make_dep(dep, dependency_type): - return struct( - id = str(dep.bsp_info.id), - dependency_type = dependency_type, - ) - -def make_deps(deps, dependency_type): - return [make_dep(dep, dependency_type) for dep in deps] - -def _is_proto_library_wrapper(target, ctx): - if not ctx.rule.kind.endswith("proto_library") or ctx.rule.kind == "proto_library": - return False - - deps = collect_targets_from_attrs(ctx.rule.attr, ["deps"]) - return len(deps) == 1 and deps[0].bsp_info and deps[0].bsp_info.kind == "proto_library" - -def _get_forwarded_deps(target, ctx): - if _is_proto_library_wrapper(target, ctx): - return collect_targets_from_attrs(ctx.rule.attr, ["deps"]) - return [] - -def _bsp_target_info_aspect_impl(target, ctx): - if target.label.name.endswith(".semanticdb"): - return [] - - rule_attrs = ctx.rule.attr - - direct_dep_targets = collect_targets_from_attrs(rule_attrs, COMPILE_DEPS) - private_direct_dep_targets = collect_targets_from_attrs(rule_attrs, PRIVATE_COMPILE_DEPS) - direct_deps = make_deps(direct_dep_targets, COMPILE) - - exported_deps_from_deps = [] - for dep in direct_dep_targets: - exported_deps_from_deps = exported_deps_from_deps + dep.bsp_info.export_deps - - compile_deps = direct_deps + exported_deps_from_deps - - runtime_dep_targets = collect_targets_from_attrs(rule_attrs, RUNTIME_DEPS) - runtime_deps = make_deps(runtime_dep_targets, RUNTIME) - - all_deps = depset(compile_deps + runtime_deps).to_list() - - # Propagate my own exports - export_deps = [] - direct_exports = [] - if JavaInfo in target: - direct_exports = collect_targets_from_attrs(rule_attrs, ["exports"]) - export_deps.extend(make_deps(direct_exports, COMPILE)) - for export in direct_exports: - export_deps.extend(export.bsp_info.export_deps) - export_deps = depset(export_deps).to_list() - - forwarded_deps = _get_forwarded_deps(target, ctx) + direct_exports - - dep_targets = direct_dep_targets + private_direct_dep_targets + runtime_dep_targets + direct_exports - output_groups = dict() - for dep in dep_targets: - for k, v in dep.bsp_info.output_groups.items(): - if dep in forwarded_deps: - output_groups[k] = output_groups[k] + [v] if k in output_groups else [v] - elif k.endswith("-direct-deps"): - pass - elif k.endswith("-outputs"): - directs = k[:-len("outputs")] + "direct-deps" - output_groups[directs] = output_groups[directs] + [v] if directs in output_groups else [v] - else: - output_groups[k] = output_groups[k] + [v] if k in output_groups else [v] - - for k, v in output_groups.items(): - output_groups[k] = depset(transitive = v) - - srcs_attr = getattr(ctx.rule.attr, "srcs", []) - sources = [] - - if type(srcs_attr) == "list": - sources = [ - file_location(f) - for t in srcs_attr - for f in t.files.to_list() - if f.is_source - ] - - resources_attr = getattr(ctx.rule.attr, "resources", []) - resources = [] - - if type(resources_attr) == "list": - resources = [ - file_location(f) - for t in resources_attr - for f in t.files.to_list() - ] - - aspect_ids = get_aspect_ids(ctx, target) - - result = dict( - id = str(target.label), - kind = ctx.rule.kind, - tags = rule_attrs.tags, - dependencies = list(all_deps), - sources = sources, - resources = resources, - env = getattr(rule_attrs, "env", {}), - env_inherit = getattr(rule_attrs, "env_inherit", []), - ) - - extension_info = create_all_extension_info(target, ctx, output_groups, dep_targets) - extension_exported_properties = dict() - for (_, data) in extension_info: - if data != None: - extension_exported_properties.update(data) - - info_files = [file for (file, _) in extension_info] - update_sync_output_groups(output_groups, "bsp-target-info", depset(info_files)) - - file_name = target.label.name - file_name = file_name + "-" + str(abs(hash(file_name))) - if aspect_ids: - file_name = file_name + "-" + str(abs(hash(".".join(aspect_ids)))) - file_name = "%s.general" % file_name - file_name = "%s.bsp-info.textproto" % file_name - info_file = ctx.actions.declare_file(file_name) - ctx.actions.write(info_file, create_struct(**result).to_proto()) - update_sync_output_groups(output_groups, "bsp-target-info", depset([info_file])) - - exported_properties = dict( - id = target.label, - kind = ctx.rule.kind, - export_deps = export_deps, - output_groups = output_groups, - **extension_exported_properties - ) - - return struct( - bsp_info = struct(**exported_properties), - output_groups = output_groups, - ) - -bsp_target_info_aspect = aspect( - implementation = _bsp_target_info_aspect_impl, - required_aspect_providers = [[JavaInfo]], - attr_aspects = ALL_DEPS, - toolchains = TOOLCHAINS, -) diff --git a/.bazelbsp/aspects/extensions.bzl b/.bazelbsp/aspects/extensions.bzl deleted file mode 100644 index 0c9d1ca73..000000000 --- a/.bazelbsp/aspects/extensions.bzl +++ /dev/null @@ -1,3 +0,0 @@ -# This file is supposed to be overwritten with extensions and toolchains relevant to the project. -EXTENSIONS = [] -TOOLCHAINS = [] diff --git a/.bazelbsp/aspects/rules/android/android_info.bzl b/.bazelbsp/aspects/rules/android/android_info.bzl deleted file mode 100644 index c8fcdaf42..000000000 --- a/.bazelbsp/aspects/rules/android/android_info.bzl +++ /dev/null @@ -1,83 +0,0 @@ -load("//aspects:utils/utils.bzl", "create_proto", "create_struct", "file_location") - -ANDROID_SDK_TOOLCHAIN_TYPE = "@bazel_tools//tools/android:sdk_toolchain_type" - -def extract_android_info(target, ctx, dep_targets, **kwargs): - if ANDROID_SDK_TOOLCHAIN_TYPE not in ctx.toolchains: - return None, None - android_sdk_toolchain = ctx.toolchains[ANDROID_SDK_TOOLCHAIN_TYPE] - - if android_sdk_toolchain == None: - return None, None - android_sdk_info = android_sdk_toolchain.android_sdk_info - android_jar = file_location(android_sdk_info.android_jar) - if android_jar == None: - return None, None - - manifest = None - if AndroidIdeInfo in target: - android_ide_info = target[AndroidIdeInfo] - manifest = file_location(android_ide_info.manifest) - - resources = [] - resource_folders_set = {} - if hasattr(ctx.rule.attr, "resource_files"): - for resource in ctx.rule.attr.resource_files: - for resource_file in resource.files.to_list(): - resource_file_location = file_location(resource_file) - resources.append(resource_file_location) - resource_source_dir_relative_path = android_common.resource_source_directory(resource_file) - if resource_source_dir_relative_path == None: - continue - resource_source_dir_location = struct( - relative_path = resource_source_dir_relative_path, - is_source = resource_file_location.is_source, - is_external = resource_file_location.is_external, - root_execution_path_fragment = resource_file_location.root_execution_path_fragment, - ) - - # Add to set - resource_folders_set[resource_source_dir_location] = None - - kotlin_target_id = None - if ctx.rule.kind == "android_library" and str(target.label).endswith("_base") and not ctx.rule.attr.srcs: - # This is a hack to detect the android_library target produced by kt_android_library. - # It creates an android_library target that ends with _base and a kt_jvm_library target that ends with _kt. - # Read more here: https://github.com/bazelbuild/rules_kotlin/blob/master/kotlin/internal/jvm/android.bzl - kotlin_target_id = str(target.label)[:-5] + "_kt" - - android_target_info_proto = create_struct( - android_jar = android_jar, - manifest = manifest, - resources = resources, - resource_folders = resource_folders_set.keys(), - kotlin_target_id = kotlin_target_id, - ) - - return create_proto(target, ctx, android_target_info_proto, "android_target_info"), None - -def extract_android_aar_import_info(target, ctx, dep_targets, **kwargs): - if ctx.rule.kind != "aar_import": - return None, None - - if AndroidManifestInfo not in target: - return None, None - manifest = file_location(target[AndroidManifestInfo].manifest) - - resource_folder = None - r_txt = None - if AndroidResourcesInfo in target: - direct_android_resources = target[AndroidResourcesInfo].direct_android_resources.to_list() - if direct_android_resources: - direct_android_resource = direct_android_resources[0] - resource_files = direct_android_resource.resources - if resource_files: - resource_folder = file_location(resource_files[0]) - r_txt = file_location(direct_android_resource.r_txt) - - android_aar_import_info_proto = create_struct( - manifest = manifest, - resource_folder = resource_folder, - r_txt = r_txt, - ) - return create_proto(target, ctx, android_aar_import_info_proto, "android_aar_import_info"), None diff --git a/.bazelbsp/aspects/rules/cpp/cpp_info.bzl b/.bazelbsp/aspects/rules/cpp/cpp_info.bzl deleted file mode 100644 index 6339c913b..000000000 --- a/.bazelbsp/aspects/rules/cpp/cpp_info.bzl +++ /dev/null @@ -1,14 +0,0 @@ -load("//aspects:utils/utils.bzl", "create_proto", "create_struct") - -def extract_cpp_info(target, ctx, **kwargs): - if CcInfo not in target: - return None, None - - result = create_struct( - copts = getattr(ctx.rule.attr, "copts", []), - defines = getattr(ctx.rule.attr, "defines", []), - link_opts = getattr(ctx.rule.attr, "linkopts", []), - link_shared = getattr(ctx.rule.attr, "linkshared", False), - ) - - return create_proto(target, ctx, result, "cpp_target_info"), None diff --git a/.bazelbsp/aspects/rules/java/java_info.bzl b/.bazelbsp/aspects/rules/java/java_info.bzl deleted file mode 100644 index a342ed600..000000000 --- a/.bazelbsp/aspects/rules/java/java_info.bzl +++ /dev/null @@ -1,60 +0,0 @@ -load("//aspects:utils/utils.bzl", "create_proto", "create_struct", "to_file_location") - -def extract_java_toolchain(target, ctx, dep_targets, **kwargs): - toolchain = None - - if hasattr(target, "java_toolchain"): - toolchain = target.java_toolchain - elif java_common.JavaToolchainInfo != platform_common.ToolchainInfo and \ - java_common.JavaToolchainInfo in target: - toolchain = target[java_common.JavaToolchainInfo] - - toolchain_info = None - if toolchain != None: - java_home = to_file_location(toolchain.java_runtime.java_home, "", False, True) if hasattr(toolchain, "java_runtime") else None - toolchain_info = create_struct( - source_version = toolchain.source_version, - target_version = toolchain.target_version, - java_home = java_home, - ) - else: - for dep in dep_targets: - if hasattr(dep.bsp_info, "java_toolchain_info"): - toolchain_info = dep.bsp_info.java_toolchain_info - break - - if toolchain_info != None: - info_file = create_proto(target, ctx, toolchain_info, "java_toolchain_info") - return info_file, dict(java_toolchain_info = toolchain_info) - else: - return None, None - -JAVA_RUNTIME_TOOLCHAIN_TYPE = "@bazel_tools//tools/jdk:runtime_toolchain_type" - -def extract_java_runtime(target, ctx, dep_targets, **kwargs): - runtime = None - - if java_common.JavaRuntimeInfo in target: # Bazel 5.4.0 way - runtime = target[java_common.JavaRuntimeInfo] - elif JAVA_RUNTIME_TOOLCHAIN_TYPE in ctx.toolchains: # Bazel 6.0.0 way - runtime = ctx.toolchains[JAVA_RUNTIME_TOOLCHAIN_TYPE].java_runtime - else: - runtime_jdk = getattr(ctx.rule.attr, "runtime_jdk", None) - if runtime_jdk and java_common.JavaRuntimeInfo in runtime_jdk: - runtime = runtime_jdk[java_common.JavaRuntimeInfo] - - runtime_info = None - if runtime != None: - java_home = to_file_location(runtime.java_home, "", False, True) if hasattr(runtime, "java_home") else None - runtime_info = create_struct(java_home = java_home) - else: - for dep in dep_targets: - if hasattr(dep.bsp_info, "java_runtime_info"): - runtime_info = dep.bsp_info.java_runtime_info - break - - if runtime_info != None: - info_file = create_proto(target, ctx, runtime_info, "java_runtime_info") - return info_file, dict(java_runtime_info = runtime_info) - else: - return None, None diff --git a/.bazelbsp/aspects/rules/jvm/jvm_info.bzl b/.bazelbsp/aspects/rules/jvm/jvm_info.bzl deleted file mode 100644 index 08d6bcee9..000000000 --- a/.bazelbsp/aspects/rules/jvm/jvm_info.bzl +++ /dev/null @@ -1,166 +0,0 @@ -load("//aspects:utils/utils.bzl", "create_proto", "create_struct", "file_location", "is_external", "map", "update_sync_output_groups") - -def map_with_resolve_files(f, xs): - results = [] - resolve_files = [] - - for x in xs: - if x != None: - res = f(x) - if res != None: - a, b = res - if a != None: - results.append(a) - if b != None: - resolve_files += b - - return results, resolve_files - -def get_interface_jars(output): - if hasattr(output, "compile_jar") and output.compile_jar: - return [output.compile_jar] - elif hasattr(output, "ijar") and output.ijar: - return [output.ijar] - else: - return [] - -def get_source_jars(output): - if hasattr(output, "source_jars"): - source_jars = output.source_jars - if type(source_jars) == "depset": - return source_jars.to_list() - else: - # assuming it returns sequence type here - return source_jars - if hasattr(output, "source_jar"): - return [output.source_jar] - return [] - -def to_generated_jvm_outputs(output): - if output == None or output.generated_class_jar == None: - return None - - class_jar = output.generated_class_jar - source_jar = output.generated_source_jar - - output = struct( - binary_jars = [file_location(class_jar)], - source_jars = [file_location(source_jar)], - ) - resolve_files = [class_jar, source_jar] - return output, resolve_files - -def get_generated_jars(provider): - if hasattr(provider, "java_outputs"): - return map_with_resolve_files(to_generated_jvm_outputs, provider.java_outputs) - - if hasattr(provider, "annotation_processing") and provider.annotation_processing and provider.annotation_processing.enabled: - class_jars = [provider.annotation_processing.class_jar] - source_jars = [provider.annotation_processing.source_jar] - - # Additional info from `rules_kotlin`'s `KtJvmInfo` - if hasattr(provider, "additional_generated_source_jars"): - source_jars = source_jars + [jar for jar in provider.additional_generated_source_jars] - if hasattr(provider, "all_output_jars"): - class_jars = class_jars + [jar for jar in provider.all_output_jars] - - output = struct( - binary_jars = [file_location(jar) for jar in class_jars], - source_jars = [file_location(jar) for jar in source_jars], - ) - resolve_files = class_jars + source_jars - return [output], resolve_files - - return [], [] - -def to_jvm_outputs(output): - if output == None or output.class_jar == None: - return None - - binary_jars = [output.class_jar] - interface_jars = get_interface_jars(output) - source_jars = get_source_jars(output) - output = struct( - binary_jars = map(file_location, binary_jars), - interface_jars = map(file_location, interface_jars), - source_jars = map(file_location, source_jars), - ) - resolve_files = binary_jars + interface_jars + source_jars - return output, resolve_files - -def extract_runtime_jars(target, provider): - compilation_info = getattr(provider, "compilation_info", None) - - if compilation_info: - return compilation_info.runtime_classpath - - return getattr(provider, "transitive_runtime_jars", target[JavaInfo].transitive_runtime_jars) - -def extract_compile_jars(provider): - compilation_info = getattr(provider, "compilation_info", None) - transitive_compile_time_jars = getattr(provider, "transitive_compile_time_jars", depset()) - - return compilation_info.compilation_classpath if compilation_info else transitive_compile_time_jars - -def get_jvm_provider(target): - if hasattr(target, "scala"): - return target.scala - if hasattr(target, "kt") and hasattr(target.kt, "outputs"): - return target.kt - if JavaInfo in target: - return target[JavaInfo] - return None - -def extract_jvm_info(target, ctx, output_groups, **kwargs): - provider = get_jvm_provider(target) - if not provider: - return None, None - - if hasattr(provider, "java_outputs") and provider.java_outputs: - java_outputs = provider.java_outputs - elif hasattr(provider, "outputs") and provider.outputs: - java_outputs = provider.outputs.jars - else: - return None, None - - # I don't know why, but it seems that the "java_outputs" variable can have a different type, depending on language - jdeps = get_jdeps(target) - - resolve_files = [] - - jars, resolve_files_jars = map_with_resolve_files(to_jvm_outputs, java_outputs) - resolve_files += resolve_files_jars - - generated_jars, resolve_files_generated_jars = get_generated_jars(provider) - resolve_files += resolve_files_generated_jars - - javac_opts = getattr(ctx.rule.attr, "javacopts", []) - jvm_flags = getattr(ctx.rule.attr, "jvm_flags", []) - args = getattr(ctx.rule.attr, "args", []) - main_class = getattr(ctx.rule.attr, "main_class", None) - - if (is_external(target)): - runtime_jars = extract_runtime_jars(target, provider).to_list() - compile_jars = extract_compile_jars(provider).to_list() - source_jars = getattr(provider, "transitive_source_jars", depset()).to_list() - resolve_files += runtime_jars - resolve_files += compile_jars - resolve_files += source_jars - update_sync_output_groups(output_groups, "external-deps-resolve", depset(resolve_files)) - - info = create_struct( - jars = jars, - generated_jars = generated_jars, - javac_opts = javac_opts, - jvm_flags = jvm_flags, - main_class = main_class, - args = args, - jdeps = [file_location(j) for j in jdeps], - ) - - return create_proto(target, ctx, info, "jvm_target_info"), None - -def get_jdeps(target): - if JavaInfo in target: - return [jo.jdeps for jo in target[JavaInfo].java_outputs if jo.jdeps != None] - return [] diff --git a/.bazelbsp/aspects/rules/kt/kt_info.bzl.template b/.bazelbsp/aspects/rules/kt/kt_info.bzl.template deleted file mode 100644 index 8ded158e3..000000000 --- a/.bazelbsp/aspects/rules/kt/kt_info.bzl.template +++ /dev/null @@ -1,45 +0,0 @@ -load("@${ruleName}//kotlin/internal:defs.bzl", "KtJvmInfo") -load("@${ruleName}//kotlin/internal:opts.bzl", "KotlincOptions", "kotlinc_options_to_flags") -load("//aspects:utils/utils.bzl", "convert_struct_to_dict", "create_proto", "create_struct", "map", "file_location") - -KOTLIN_TOOLCHAIN_TYPE = "@${ruleName}//kotlin/internal:kt_toolchain_type" - -def extract_kotlin_info(target, ctx, **kwargs): - if KtJvmInfo not in target: - return None, None - - # Only supports JVM platform now - provider = target[KtJvmInfo] - - language_version = getattr(provider, "language_version", None) - api_version = language_version - associates = getattr(ctx.rule.attr, "associates", []) - associates_labels = [str(associate.label) for associate in associates] - - kotlin_toolchain = ctx.toolchains[KOTLIN_TOOLCHAIN_TYPE] - toolchain_kotlinc_opts = kotlin_toolchain.kotlinc_options - kotlinc_opts_target = getattr(ctx.rule.attr, "kotlinc_opts", None) - kotlinc_opts = kotlinc_opts_target[KotlincOptions] if kotlinc_opts_target and KotlincOptions in kotlinc_opts_target else toolchain_kotlinc_opts - kotlinc_opts_dict = convert_struct_to_dict(kotlinc_opts) - - # Inject default JVM target version if necessary - - # if not specifically set, the default value of "jvm_target" in kotlinc_opts is an empty string. - if not kotlinc_opts_dict.get("jvm_target") and getattr(kotlin_toolchain, "jvm_target", ""): - kotlinc_opts_dict["jvm_target"] = getattr(kotlin_toolchain, "jvm_target") - - stdlibs_files = kotlin_toolchain.jvm_stdlibs.compile_jars.to_list() - stdlibs = map(file_location, stdlibs_files) - - kotlin_info = dict( - language_version = language_version, - api_version = api_version, - associates = associates_labels, - stdlibs = stdlibs, - kotlinc_opts = kotlinc_options_to_flags(create_struct(**kotlinc_opts_dict)) - ) - - kotlin_target_info = create_struct(**kotlin_info) - info_file = create_proto(target, ctx, kotlin_target_info, "kotlin_target_info") - - return info_file, None diff --git a/.bazelbsp/aspects/rules/python/python_info.bzl b/.bazelbsp/aspects/rules/python/python_info.bzl deleted file mode 100644 index c728e4070..000000000 --- a/.bazelbsp/aspects/rules/python/python_info.bzl +++ /dev/null @@ -1,34 +0,0 @@ -load("//aspects:utils/utils.bzl", "create_proto", "create_struct", "file_location", "to_file_location") - -def interpreter_from_absolute_path(path): - if path == None: - return None - - return to_file_location(path, "", False, True) - -def interpreter_from_file(file): - if file == None: - return None - - return file_location(file) - -def extract_python_info(target, ctx, **kwargs): - if PyInfo not in target: - return None, None - - if PyRuntimeInfo in target: - provider = target[PyRuntimeInfo] - else: - provider = None - - interpreter = interpreter_from_file(getattr(provider, "interpreter", None)) - interpreter_path = interpreter_from_absolute_path(getattr(provider, "interpreter_path", None)) - - final_interpreter = interpreter if interpreter != None else interpreter_path - - python_target_info = create_struct( - interpreter = final_interpreter, - version = getattr(provider, "python_version", None), - ) - - return create_proto(target, ctx, python_target_info, "python_target_info"), None diff --git a/.bazelbsp/aspects/rules/rust/rust_info.bzl b/.bazelbsp/aspects/rules/rust/rust_info.bzl deleted file mode 100644 index 4ae71c750..000000000 --- a/.bazelbsp/aspects/rules/rust/rust_info.bzl +++ /dev/null @@ -1,80 +0,0 @@ -load("@rules_rust//rust:rust_common.bzl", "BuildInfo", "CrateInfo") -load("//aspects:utils/utils.bzl", "create_proto", "create_struct", "filter", "flatmap") - -# This is supposed to be enum, but Starlark does not support enums. -# See bsp_target_info.proto:RustCrateLocation. -WORKSPACE_DIR = 0 -EXEC_ROOT = 1 - -RUST_TOOLCHAIN_TYPE = "@rules_rust//rust:toolchain_type" - -def collect_proc_macro_artifacts(target, kind, ext): - if not hasattr(target, "actions") or kind != "proc-macro": - return [] - - def is_proc_macro_output_with_ext(output): - return output.path.endswith(ext) - - return filter( - is_proc_macro_output_with_ext, - flatmap( - lambda _action: _action.outputs.to_list(), - target.actions, - ), - ) - -def extract_rust_crate_info(target, ctx, **kwargs): - if CrateInfo not in target: - return None, None - - if RUST_TOOLCHAIN_TYPE not in ctx.toolchains: - return None, None - - crate_info = target[CrateInfo] - build_info = None if not BuildInfo in target else target[BuildInfo] - toolchain = ctx.toolchains[RUST_TOOLCHAIN_TYPE] - - crate_root_path = crate_info.root.path - - def is_same_crate(dep): - if CrateInfo not in dep: - return False - - return dep[CrateInfo].root.path == crate_root_path - - crate_is_from_workspace = not crate_info.root.path.startswith("external/") - crate_is_generated = not crate_info.root.is_source - crate_is_in_exec_root = not crate_is_from_workspace or crate_is_generated - - deps = [ - dep[CrateInfo].root.path - for dep in (ctx.rule.attr.deps + ctx.rule.attr.proc_macro_deps) - if not is_same_crate(dep) and CrateInfo in dep - ] - - proc_macro_artifacts = collect_proc_macro_artifacts(target, crate_info.type, toolchain.dylib_ext) - proc_macro_artifacts_paths = [artifact.path for artifact in proc_macro_artifacts] - - # To obtain crate root file, find directory corresponding to - # `crate_location` and concatenate it with `crate_id` (relative crate root - # file path); this has be done in bazel-bsp - # (see rules_rust/tools/rust_analyzer/rust_project.rs:write_rust_project). - rust_crate_struct = create_struct( - # The `crate-id` field must be unique. The deduplication has to be done - # in bazel-bsp - # (see rules_rust/tools/rust_analyzer/aquery.rs:consolidate_crate_specs). - crate_id = crate_info.root.path, - location = EXEC_ROOT if crate_is_in_exec_root else WORKSPACE_DIR, - from_workspace = crate_is_from_workspace, - name = crate_info.name, - kind = crate_info.type, - edition = crate_info.edition, - out_dir = "" if build_info == None else build_info.out_dir.path, - crate_features = ctx.rule.attr.crate_features, - dependencies_crate_ids = deps, - crate_root = crate_info.root.path, - version = ctx.rule.attr.version, - proc_macro_artifacts = proc_macro_artifacts_paths, - ) - - return create_proto(target, ctx, rust_crate_struct, "rust_crate_info"), None diff --git a/.bazelbsp/aspects/rules/scala/scala_info.bzl b/.bazelbsp/aspects/rules/scala/scala_info.bzl deleted file mode 100644 index d9aa5f925..000000000 --- a/.bazelbsp/aspects/rules/scala/scala_info.bzl +++ /dev/null @@ -1,49 +0,0 @@ -load("//aspects:utils/utils.bzl", "create_proto", "file_location", "is_external", "map", "update_sync_output_groups") - -def find_scalac_classpath(runfiles): - result = [] - found_scala_compiler_jar = False - for file in runfiles: - name = file.basename - if file.extension == "jar" and ("scala3-compiler" in name or "scala-compiler" in name): - found_scala_compiler_jar = True - result.append(file) - elif file.extension == "jar" and ("scala3-library" in name or "scala3-reflect" in name or "scala-library" in name or "scala-reflect" in name): - result.append(file) - return result if found_scala_compiler_jar and len(result) >= 2 else [] - -def extract_scala_toolchain_info(target, ctx, output_groups, **kwargs): - runfiles = target.default_runfiles.files.to_list() - - classpath = find_scalac_classpath(runfiles) - - if not classpath: - return None, None - - resolve_files = classpath - compiler_classpath = map(file_location, classpath) - - if (is_external(target)): - update_sync_output_groups(output_groups, "external-deps-resolve", depset(resolve_files)) - - scala_toolchain_info = struct(compiler_classpath = compiler_classpath) - - return create_proto(target, ctx, scala_toolchain_info, "scala_toolchain_info"), None - -def extract_scala_info(target, ctx, output_groups, **kwargs): - kind = ctx.rule.kind - if not kind.startswith("scala_") and not kind.startswith("thrift_"): - return None, None - - SCALA_TOOLCHAIN = "@io_bazel_rules_scala//scala:toolchain_type" - - # check of _scala_toolchain is necessary, because SCALA_TOOLCHAIN will always be present - if hasattr(ctx.rule.attr, "_scala_toolchain"): - common_scalac_opts = ctx.toolchains[SCALA_TOOLCHAIN].scalacopts - else: - common_scalac_opts = [] - scalac_opts = common_scalac_opts + getattr(ctx.rule.attr, "scalacopts", []) - - scala_info = struct(scalac_opts = scalac_opts) - - return create_proto(target, ctx, scala_info, "scala_target_info"), None diff --git a/.bazelbsp/aspects/runtime_classpath_query.bzl b/.bazelbsp/aspects/runtime_classpath_query.bzl deleted file mode 100644 index ed0f64672..000000000 --- a/.bazelbsp/aspects/runtime_classpath_query.bzl +++ /dev/null @@ -1,24 +0,0 @@ -def format(target): - provider = providers(target).get("@@_builtins//:common/java/java_info.bzl%JavaInfo") - if provider == None: - provider = providers(target)["JavaInfo"] #bazel6 - - compilation_info = getattr(provider, "compilation_info", None) - - runtime_classpath = [] #bazel5 default to [] because depset() not available - if compilation_info: - runtime_classpath = compilation_info.runtime_classpath.to_list() - elif hasattr(provider, "transitive_runtime_jars"): - runtime_classpath = provider.transitive_runtime_jars.to_list() - - compile_classpath = [] #bazel5 default to [] because depset() not available - if (compilation_info and hasattr(compilation_info, "transitive_compile_time_jars")): - compile_classpath = compilation_info.transitive_compile_time_jars.to_list() - elif hasattr(provider, "transitive_compile_time_jars"): - compile_classpath = provider.transitive_compile_time_jars.to_list() - - return { - #bazel5 returning dict, because struct not available in queries - "runtime_classpath": [f.path for f in runtime_classpath], - "compile_classpath": [f.path for f in compile_classpath], - } diff --git a/.bazelbsp/aspects/utils/utils.bzl b/.bazelbsp/aspects/utils/utils.bzl deleted file mode 100644 index 109ce65c0..000000000 --- a/.bazelbsp/aspects/utils/utils.bzl +++ /dev/null @@ -1,105 +0,0 @@ -def abs(num): - if num < 0: - return -num - else: - return num - -def map(f, xs): - return [f(x) for x in xs] - -def filter(f, xs): - return [x for x in xs if f(x)] - -def flatten(xss): - return [x for xs in xss for x in xs] - -def flatmap(f, xs): - return flatten(map(f, xs)) - -def file_location(file): - if file == None: - return None - - return to_file_location( - file.path, - file.root.path if not file.is_source else "", - file.is_source, - file.owner.workspace_root.startswith("..") or file.owner.workspace_root.startswith("external"), - ) - -def _strip_root_exec_path_fragment(path, root_fragment): - if root_fragment and path.startswith(root_fragment + "/"): - return path[len(root_fragment + "/"):] - return path - -def _strip_external_workspace_prefix(path): - if path.startswith("../") or path.startswith("external/"): - return "/".join(path.split("/")[2:]) - return path - -def to_file_location(exec_path, root_exec_path_fragment, is_source, is_external): - # directory structure: - # exec_path = (../repo_name)? + (root_fragment)? + relative_path - relative_path = _strip_external_workspace_prefix(exec_path) - relative_path = _strip_root_exec_path_fragment(relative_path, root_exec_path_fragment) - - root_exec_path_fragment = exec_path[:-(len("/" + relative_path))] if relative_path != "" else exec_path - - return struct( - relative_path = relative_path, - is_source = is_source, - is_external = is_external, - root_execution_path_fragment = root_exec_path_fragment, - ) - -def create_struct(**kwargs): - d = {name: kwargs[name] for name in kwargs if kwargs[name] != None} - return struct(**d) - -def update_sync_output_groups(groups_dict, key, new_set): - update_set_in_dict(groups_dict, key + "-transitive-deps", new_set) - update_set_in_dict(groups_dict, key + "-outputs", new_set) - update_set_in_dict(groups_dict, key + "-direct-deps", new_set) - -def update_set_in_dict(input_dict, key, other_set): - input_dict[key] = depset(transitive = [input_dict.get(key, depset()), other_set]) - -def get_aspect_ids(ctx, target): - """Returns the all aspect ids, filtering out self.""" - aspect_ids = None - if hasattr(ctx, "aspect_ids"): - aspect_ids = ctx.aspect_ids - elif hasattr(target, "aspect_ids"): - aspect_ids = target.aspect_ids - else: - return None - return [aspect_id for aspect_id in aspect_ids if "bsp_target_info_aspect" not in aspect_id] - -def create_proto(target, ctx, data, name): - if data == None: - return None - - aspect_ids = get_aspect_ids(ctx, target) - file_name = target.label.name - file_name = file_name + "-" + str(abs(hash(file_name))) - if aspect_ids: - file_name = file_name + "-" + str(abs(hash(".".join(aspect_ids)))) - file_name = "%s.%s" % (file_name, name) - file_name = "%s.bsp-info.textproto" % file_name - info_file = ctx.actions.declare_file(file_name) - ctx.actions.write(info_file, data.to_proto()) - return info_file - -def is_external(target): - return not str(target.label).startswith("@@//") and not str(target.label).startswith("@//") and not str(target.label).startswith("//") - -def convert_struct_to_dict(s): - attrs = dir(s) - - # two deprecated methods of struct - if "to_json" in attrs: - attrs.remove("to_json") - if "to_proto" in attrs: - attrs.remove("to_proto") - - return {key: getattr(s, key) for key in attrs} diff --git a/.bazelbsp/bazelbsp.log b/.bazelbsp/bazelbsp.log deleted file mode 100644 index 74f9e7b25..000000000 --- a/.bazelbsp/bazelbsp.log +++ /dev/null @@ -1,132 +0,0 @@ -2024-05-07 12:12:57.136 [main] INFO org.jetbrains.bsp.bazel.workspacecontext.WorkspaceContextConstructor - Constructing workspace context for: ProjectView(targets=ProjectViewTargetsSection(values=[BuildTargetIdentifier [ - uri = "//..." -]], excludedValues=[]), bazelBinary=null, buildFlags=null, buildManualTargets=ProjectViewBuildManualTargetsSection(value=false), directories=null, deriveTargetsFromDirectories=ProjectViewDeriveTargetsFromDirectoriesSection(value=false), importDepth=null, enabledRules=ProjectViewEnabledRulesSection(values=[io_bazel_rules_scala, rules_java, rules_jvm])). -2024-05-07 12:12:57.143 [main] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelRunner - Invoking: /opt/homebrew/bin/bazel mod show_repo -2024-05-07 12:12:57.633 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - ERROR: The project you're trying to build requires Bazel 5.1.0 (specified in /Users/joao/code/VerifiedSCION/.bazelversion), but it wasn't found in /opt/homebrew/Cellar/bazel/7.1.1/libexec/bin. -2024-05-07 12:12:57.634 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:12:57.635 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - Bazel binaries for all official releases can be downloaded from here: -2024-05-07 12:12:57.635 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - https://github.com/bazelbuild/bazel/releases -2024-05-07 12:12:57.635 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:12:57.635 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - You can download the required version directly using this command: -2024-05-07 12:12:57.635 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - (cd "/opt/homebrew/Cellar/bazel/7.1.1/libexec/bin" && curl -fLO https://releases.bazel.build/5.1.0/release/bazel-5.1.0-darwin-arm64 && chmod +x bazel-5.1.0-darwin-arm64) -2024-05-07 12:12:57.643 [main] INFO org.jetbrains.bsp.bazel.workspacecontext.WorkspaceContextConstructor - Constructing workspace context for: ProjectView(targets=ProjectViewTargetsSection(values=[BuildTargetIdentifier [ - uri = "//..." -]], excludedValues=[]), bazelBinary=null, buildFlags=null, buildManualTargets=ProjectViewBuildManualTargetsSection(value=false), directories=null, deriveTargetsFromDirectories=ProjectViewDeriveTargetsFromDirectoriesSection(value=false), importDepth=null, enabledRules=ProjectViewEnabledRulesSection(values=[io_bazel_rules_scala, rules_java, rules_jvm])). -2024-05-07 12:12:57.644 [main] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelRunner - Invoking: /opt/homebrew/bin/bazel info -2024-05-07 12:12:57.664 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - ERROR: The project you're trying to build requires Bazel 5.1.0 (specified in /Users/joao/code/VerifiedSCION/.bazelversion), but it wasn't found in /opt/homebrew/Cellar/bazel/7.1.1/libexec/bin. -2024-05-07 12:12:57.665 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:12:57.665 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - Bazel binaries for all official releases can be downloaded from here: -2024-05-07 12:12:57.665 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - https://github.com/bazelbuild/bazel/releases -2024-05-07 12:12:57.666 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:12:57.666 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - You can download the required version directly using this command: -2024-05-07 12:12:57.666 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - (cd "/opt/homebrew/Cellar/bazel/7.1.1/libexec/bin" && curl -fLO https://releases.bazel.build/5.1.0/release/bazel-5.1.0-darwin-arm64 && chmod +x bazel-5.1.0-darwin-arm64) -2024-05-07 12:13:57.164 [main] INFO org.jetbrains.bsp.bazel.workspacecontext.WorkspaceContextConstructor - Constructing workspace context for: ProjectView(targets=ProjectViewTargetsSection(values=[BuildTargetIdentifier [ - uri = "//..." -]], excludedValues=[]), bazelBinary=null, buildFlags=null, buildManualTargets=ProjectViewBuildManualTargetsSection(value=false), directories=null, deriveTargetsFromDirectories=ProjectViewDeriveTargetsFromDirectoriesSection(value=false), importDepth=null, enabledRules=ProjectViewEnabledRulesSection(values=[io_bazel_rules_scala, rules_java, rules_jvm])). -2024-05-07 12:13:57.168 [main] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelRunner - Invoking: /opt/homebrew/bin/bazel mod show_repo -2024-05-07 12:13:57.189 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - ERROR: The project you're trying to build requires Bazel 5.1.0 (specified in /Users/joao/code/VerifiedSCION/.bazelversion), but it wasn't found in /opt/homebrew/Cellar/bazel/7.1.1/libexec/bin. -2024-05-07 12:13:57.190 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:13:57.190 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - Bazel binaries for all official releases can be downloaded from here: -2024-05-07 12:13:57.190 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - https://github.com/bazelbuild/bazel/releases -2024-05-07 12:13:57.190 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:13:57.191 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - You can download the required version directly using this command: -2024-05-07 12:13:57.191 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - (cd "/opt/homebrew/Cellar/bazel/7.1.1/libexec/bin" && curl -fLO https://releases.bazel.build/5.1.0/release/bazel-5.1.0-darwin-arm64 && chmod +x bazel-5.1.0-darwin-arm64) -2024-05-07 12:13:57.194 [main] INFO org.jetbrains.bsp.bazel.workspacecontext.WorkspaceContextConstructor - Constructing workspace context for: ProjectView(targets=ProjectViewTargetsSection(values=[BuildTargetIdentifier [ - uri = "//..." -]], excludedValues=[]), bazelBinary=null, buildFlags=null, buildManualTargets=ProjectViewBuildManualTargetsSection(value=false), directories=null, deriveTargetsFromDirectories=ProjectViewDeriveTargetsFromDirectoriesSection(value=false), importDepth=null, enabledRules=ProjectViewEnabledRulesSection(values=[io_bazel_rules_scala, rules_java, rules_jvm])). -2024-05-07 12:13:57.195 [main] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelRunner - Invoking: /opt/homebrew/bin/bazel info -2024-05-07 12:13:57.208 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - ERROR: The project you're trying to build requires Bazel 5.1.0 (specified in /Users/joao/code/VerifiedSCION/.bazelversion), but it wasn't found in /opt/homebrew/Cellar/bazel/7.1.1/libexec/bin. -2024-05-07 12:13:57.208 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:13:57.208 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - Bazel binaries for all official releases can be downloaded from here: -2024-05-07 12:13:57.208 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - https://github.com/bazelbuild/bazel/releases -2024-05-07 12:13:57.209 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:13:57.209 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - You can download the required version directly using this command: -2024-05-07 12:13:57.210 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - (cd "/opt/homebrew/Cellar/bazel/7.1.1/libexec/bin" && curl -fLO https://releases.bazel.build/5.1.0/release/bazel-5.1.0-darwin-arm64 && chmod +x bazel-5.1.0-darwin-arm64) -2024-05-07 12:14:57.190 [main] INFO org.jetbrains.bsp.bazel.workspacecontext.WorkspaceContextConstructor - Constructing workspace context for: ProjectView(targets=ProjectViewTargetsSection(values=[BuildTargetIdentifier [ - uri = "//..." -]], excludedValues=[]), bazelBinary=null, buildFlags=null, buildManualTargets=ProjectViewBuildManualTargetsSection(value=false), directories=null, deriveTargetsFromDirectories=ProjectViewDeriveTargetsFromDirectoriesSection(value=false), importDepth=null, enabledRules=ProjectViewEnabledRulesSection(values=[io_bazel_rules_scala, rules_java, rules_jvm])). -2024-05-07 12:14:57.193 [main] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelRunner - Invoking: /opt/homebrew/bin/bazel mod show_repo -2024-05-07 12:14:57.212 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - ERROR: The project you're trying to build requires Bazel 5.1.0 (specified in /Users/joao/code/VerifiedSCION/.bazelversion), but it wasn't found in /opt/homebrew/Cellar/bazel/7.1.1/libexec/bin. -2024-05-07 12:14:57.213 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:14:57.213 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - Bazel binaries for all official releases can be downloaded from here: -2024-05-07 12:14:57.213 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - https://github.com/bazelbuild/bazel/releases -2024-05-07 12:14:57.214 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:14:57.214 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - You can download the required version directly using this command: -2024-05-07 12:14:57.214 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - (cd "/opt/homebrew/Cellar/bazel/7.1.1/libexec/bin" && curl -fLO https://releases.bazel.build/5.1.0/release/bazel-5.1.0-darwin-arm64 && chmod +x bazel-5.1.0-darwin-arm64) -2024-05-07 12:14:57.218 [main] INFO org.jetbrains.bsp.bazel.workspacecontext.WorkspaceContextConstructor - Constructing workspace context for: ProjectView(targets=ProjectViewTargetsSection(values=[BuildTargetIdentifier [ - uri = "//..." -]], excludedValues=[]), bazelBinary=null, buildFlags=null, buildManualTargets=ProjectViewBuildManualTargetsSection(value=false), directories=null, deriveTargetsFromDirectories=ProjectViewDeriveTargetsFromDirectoriesSection(value=false), importDepth=null, enabledRules=ProjectViewEnabledRulesSection(values=[io_bazel_rules_scala, rules_java, rules_jvm])). -2024-05-07 12:14:57.218 [main] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelRunner - Invoking: /opt/homebrew/bin/bazel info -2024-05-07 12:14:57.231 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - ERROR: The project you're trying to build requires Bazel 5.1.0 (specified in /Users/joao/code/VerifiedSCION/.bazelversion), but it wasn't found in /opt/homebrew/Cellar/bazel/7.1.1/libexec/bin. -2024-05-07 12:14:57.231 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:14:57.231 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - Bazel binaries for all official releases can be downloaded from here: -2024-05-07 12:14:57.231 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - https://github.com/bazelbuild/bazel/releases -2024-05-07 12:14:57.232 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:14:57.232 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - You can download the required version directly using this command: -2024-05-07 12:14:57.233 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - (cd "/opt/homebrew/Cellar/bazel/7.1.1/libexec/bin" && curl -fLO https://releases.bazel.build/5.1.0/release/bazel-5.1.0-darwin-arm64 && chmod +x bazel-5.1.0-darwin-arm64) -2024-05-07 12:15:57.220 [main] INFO org.jetbrains.bsp.bazel.workspacecontext.WorkspaceContextConstructor - Constructing workspace context for: ProjectView(targets=ProjectViewTargetsSection(values=[BuildTargetIdentifier [ - uri = "//..." -]], excludedValues=[]), bazelBinary=null, buildFlags=null, buildManualTargets=ProjectViewBuildManualTargetsSection(value=false), directories=null, deriveTargetsFromDirectories=ProjectViewDeriveTargetsFromDirectoriesSection(value=false), importDepth=null, enabledRules=ProjectViewEnabledRulesSection(values=[io_bazel_rules_scala, rules_java, rules_jvm])). -2024-05-07 12:15:57.223 [main] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelRunner - Invoking: /opt/homebrew/bin/bazel mod show_repo -2024-05-07 12:15:57.244 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - ERROR: The project you're trying to build requires Bazel 5.1.0 (specified in /Users/joao/code/VerifiedSCION/.bazelversion), but it wasn't found in /opt/homebrew/Cellar/bazel/7.1.1/libexec/bin. -2024-05-07 12:15:57.245 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:15:57.245 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - Bazel binaries for all official releases can be downloaded from here: -2024-05-07 12:15:57.245 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - https://github.com/bazelbuild/bazel/releases -2024-05-07 12:15:57.246 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:15:57.246 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - You can download the required version directly using this command: -2024-05-07 12:15:57.246 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - (cd "/opt/homebrew/Cellar/bazel/7.1.1/libexec/bin" && curl -fLO https://releases.bazel.build/5.1.0/release/bazel-5.1.0-darwin-arm64 && chmod +x bazel-5.1.0-darwin-arm64) -2024-05-07 12:15:57.250 [main] INFO org.jetbrains.bsp.bazel.workspacecontext.WorkspaceContextConstructor - Constructing workspace context for: ProjectView(targets=ProjectViewTargetsSection(values=[BuildTargetIdentifier [ - uri = "//..." -]], excludedValues=[]), bazelBinary=null, buildFlags=null, buildManualTargets=ProjectViewBuildManualTargetsSection(value=false), directories=null, deriveTargetsFromDirectories=ProjectViewDeriveTargetsFromDirectoriesSection(value=false), importDepth=null, enabledRules=ProjectViewEnabledRulesSection(values=[io_bazel_rules_scala, rules_java, rules_jvm])). -2024-05-07 12:15:57.251 [main] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelRunner - Invoking: /opt/homebrew/bin/bazel info -2024-05-07 12:15:57.264 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - ERROR: The project you're trying to build requires Bazel 5.1.0 (specified in /Users/joao/code/VerifiedSCION/.bazelversion), but it wasn't found in /opt/homebrew/Cellar/bazel/7.1.1/libexec/bin. -2024-05-07 12:15:57.264 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:15:57.264 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - Bazel binaries for all official releases can be downloaded from here: -2024-05-07 12:15:57.264 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - https://github.com/bazelbuild/bazel/releases -2024-05-07 12:15:57.265 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:15:57.265 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - You can download the required version directly using this command: -2024-05-07 12:15:57.266 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - (cd "/opt/homebrew/Cellar/bazel/7.1.1/libexec/bin" && curl -fLO https://releases.bazel.build/5.1.0/release/bazel-5.1.0-darwin-arm64 && chmod +x bazel-5.1.0-darwin-arm64) -2024-05-07 12:16:57.235 [main] INFO org.jetbrains.bsp.bazel.workspacecontext.WorkspaceContextConstructor - Constructing workspace context for: ProjectView(targets=ProjectViewTargetsSection(values=[BuildTargetIdentifier [ - uri = "//..." -]], excludedValues=[]), bazelBinary=null, buildFlags=null, buildManualTargets=ProjectViewBuildManualTargetsSection(value=false), directories=null, deriveTargetsFromDirectories=ProjectViewDeriveTargetsFromDirectoriesSection(value=false), importDepth=null, enabledRules=ProjectViewEnabledRulesSection(values=[io_bazel_rules_scala, rules_java, rules_jvm])). -2024-05-07 12:16:57.238 [main] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelRunner - Invoking: /opt/homebrew/bin/bazel mod show_repo -2024-05-07 12:16:57.258 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - ERROR: The project you're trying to build requires Bazel 5.1.0 (specified in /Users/joao/code/VerifiedSCION/.bazelversion), but it wasn't found in /opt/homebrew/Cellar/bazel/7.1.1/libexec/bin. -2024-05-07 12:16:57.259 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:16:57.259 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - Bazel binaries for all official releases can be downloaded from here: -2024-05-07 12:16:57.259 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - https://github.com/bazelbuild/bazel/releases -2024-05-07 12:16:57.259 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:16:57.260 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - You can download the required version directly using this command: -2024-05-07 12:16:57.260 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - (cd "/opt/homebrew/Cellar/bazel/7.1.1/libexec/bin" && curl -fLO https://releases.bazel.build/5.1.0/release/bazel-5.1.0-darwin-arm64 && chmod +x bazel-5.1.0-darwin-arm64) -2024-05-07 12:16:57.264 [main] INFO org.jetbrains.bsp.bazel.workspacecontext.WorkspaceContextConstructor - Constructing workspace context for: ProjectView(targets=ProjectViewTargetsSection(values=[BuildTargetIdentifier [ - uri = "//..." -]], excludedValues=[]), bazelBinary=null, buildFlags=null, buildManualTargets=ProjectViewBuildManualTargetsSection(value=false), directories=null, deriveTargetsFromDirectories=ProjectViewDeriveTargetsFromDirectoriesSection(value=false), importDepth=null, enabledRules=ProjectViewEnabledRulesSection(values=[io_bazel_rules_scala, rules_java, rules_jvm])). -2024-05-07 12:16:57.264 [main] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelRunner - Invoking: /opt/homebrew/bin/bazel info -2024-05-07 12:16:57.277 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - ERROR: The project you're trying to build requires Bazel 5.1.0 (specified in /Users/joao/code/VerifiedSCION/.bazelversion), but it wasn't found in /opt/homebrew/Cellar/bazel/7.1.1/libexec/bin. -2024-05-07 12:16:57.278 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:16:57.278 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - Bazel binaries for all official releases can be downloaded from here: -2024-05-07 12:16:57.278 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - https://github.com/bazelbuild/bazel/releases -2024-05-07 12:16:57.278 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:16:57.279 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - You can download the required version directly using this command: -2024-05-07 12:16:57.279 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - (cd "/opt/homebrew/Cellar/bazel/7.1.1/libexec/bin" && curl -fLO https://releases.bazel.build/5.1.0/release/bazel-5.1.0-darwin-arm64 && chmod +x bazel-5.1.0-darwin-arm64) -2024-05-07 12:17:57.241 [main] INFO org.jetbrains.bsp.bazel.workspacecontext.WorkspaceContextConstructor - Constructing workspace context for: ProjectView(targets=ProjectViewTargetsSection(values=[BuildTargetIdentifier [ - uri = "//..." -]], excludedValues=[]), bazelBinary=null, buildFlags=null, buildManualTargets=ProjectViewBuildManualTargetsSection(value=false), directories=null, deriveTargetsFromDirectories=ProjectViewDeriveTargetsFromDirectoriesSection(value=false), importDepth=null, enabledRules=ProjectViewEnabledRulesSection(values=[io_bazel_rules_scala, rules_java, rules_jvm])). -2024-05-07 12:17:57.245 [main] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelRunner - Invoking: /opt/homebrew/bin/bazel mod show_repo -2024-05-07 12:17:57.266 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - ERROR: The project you're trying to build requires Bazel 5.1.0 (specified in /Users/joao/code/VerifiedSCION/.bazelversion), but it wasn't found in /opt/homebrew/Cellar/bazel/7.1.1/libexec/bin. -2024-05-07 12:17:57.267 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:17:57.267 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - Bazel binaries for all official releases can be downloaded from here: -2024-05-07 12:17:57.267 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - https://github.com/bazelbuild/bazel/releases -2024-05-07 12:17:57.268 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:17:57.268 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - You can download the required version directly using this command: -2024-05-07 12:17:57.268 [pool-3-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - (cd "/opt/homebrew/Cellar/bazel/7.1.1/libexec/bin" && curl -fLO https://releases.bazel.build/5.1.0/release/bazel-5.1.0-darwin-arm64 && chmod +x bazel-5.1.0-darwin-arm64) -2024-05-07 12:17:57.272 [main] INFO org.jetbrains.bsp.bazel.workspacecontext.WorkspaceContextConstructor - Constructing workspace context for: ProjectView(targets=ProjectViewTargetsSection(values=[BuildTargetIdentifier [ - uri = "//..." -]], excludedValues=[]), bazelBinary=null, buildFlags=null, buildManualTargets=ProjectViewBuildManualTargetsSection(value=false), directories=null, deriveTargetsFromDirectories=ProjectViewDeriveTargetsFromDirectoriesSection(value=false), importDepth=null, enabledRules=ProjectViewEnabledRulesSection(values=[io_bazel_rules_scala, rules_java, rules_jvm])). -2024-05-07 12:17:57.273 [main] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelRunner - Invoking: /opt/homebrew/bin/bazel info -2024-05-07 12:17:57.287 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - ERROR: The project you're trying to build requires Bazel 5.1.0 (specified in /Users/joao/code/VerifiedSCION/.bazelversion), but it wasn't found in /opt/homebrew/Cellar/bazel/7.1.1/libexec/bin. -2024-05-07 12:17:57.288 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:17:57.288 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - Bazel binaries for all official releases can be downloaded from here: -2024-05-07 12:17:57.288 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - https://github.com/bazelbuild/bazel/releases -2024-05-07 12:17:57.289 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - -2024-05-07 12:17:57.289 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - You can download the required version directly using this command: -2024-05-07 12:17:57.289 [pool-4-thread-1] INFO org.jetbrains.bsp.bazel.bazelrunner.BazelProcess - (cd "/opt/homebrew/Cellar/bazel/7.1.1/libexec/bin" && curl -fLO https://releases.bazel.build/5.1.0/release/bazel-5.1.0-darwin-arm64 && chmod +x bazel-5.1.0-darwin-arm64) diff --git a/.bsp/bazelbsp.json b/.bsp/bazelbsp.json deleted file mode 100644 index 7f32e82c2..000000000 --- a/.bsp/bazelbsp.json +++ /dev/null @@ -1,19 +0,0 @@ -{ - "name": "bazelbsp", - "argv": [ - "/Users/joao/.sdkman/candidates/java/11.0.19-ms/bin/java", - "-classpath", - "/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/jetbrains/bsp/bazel-bsp/3.1.0-20240313-89141af-NIGHTLY/bazel-bsp-3.1.0-20240313-89141af-NIGHTLY.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/ch/epfl/scala/bsp4j/2.2.0-M1/bsp4j-2.2.0-M1.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/core/jackson-annotations/2.16.2/jackson-annotations-2.16.2.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/core/jackson-databind/2.16.2/jackson-databind-2.16.2.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/module/jackson-module-kotlin/2.16.2/jackson-module-kotlin-2.16.2.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/google/code/gson/gson/2.10.1/gson-2.10.1.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/google/guava/guava/32.1.3-android/guava-32.1.3-android.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/google/protobuf/protobuf-java/3.25.3/protobuf-java-3.25.3.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/commons-cli/commons-cli/1.6.0/commons-cli-1.6.0.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/commons-io/commons-io/2.15.1/commons-io-2.15.1.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/grpc/grpc-protobuf/1.62.2/grpc-protobuf-1.62.2.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/grpc/grpc-stub/1.62.2/grpc-stub-1.62.2.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/apache/logging/log4j/log4j-api/2.23.1/log4j-api-2.23.1.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/apache/logging/log4j/log4j-core/2.23.1/log4j-core-2.23.1.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/apache/velocity/velocity-engine-core/2.3/velocity-engine-core-2.3.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/eclipse/lsp4j/org.eclipse.lsp4j.jsonrpc/0.20.1/org.eclipse.lsp4j.jsonrpc-0.20.1.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/jetbrains/kotlinx/kotlinx-coroutines-core/1.8.0/kotlinx-coroutines-core-1.8.0.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/eclipse/lsp4j/org.eclipse.lsp4j.generator/0.20.1/org.eclipse.lsp4j.generator-0.20.1.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/core/jackson-core/2.16.2/jackson-core-2.16.2.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/jetbrains/kotlin/kotlin-reflect/1.6.21/kotlin-reflect-1.6.21.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/google/guava/failureaccess/1.0.1/failureaccess-1.0.1.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/google/guava/listenablefuture/9999.0-empty-to-avoid-conflict-with-guava/listenablefuture-9999.0-empty-to-avoid-conflict-with-guava.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/google/code/findbugs/jsr305/3.0.2/jsr305-3.0.2.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/checkerframework/checker-qual/3.37.0/checker-qual-3.37.0.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/google/errorprone/error_prone_annotations/2.23.0/error_prone_annotations-2.23.0.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/google/j2objc/j2objc-annotations/2.8/j2objc-annotations-2.8.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/grpc/grpc-api/1.62.2/grpc-api-1.62.2.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/google/api/grpc/proto-google-common-protos/2.29.0/proto-google-common-protos-2.29.0.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/grpc/grpc-protobuf-lite/1.62.2/grpc-protobuf-lite-1.62.2.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/apache/commons/commons-lang3/3.11/commons-lang3-3.11.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/slf4j/slf4j-api/1.7.30/slf4j-api-1.7.30.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/jetbrains/kotlinx/kotlinx-coroutines-core-jvm/1.8.0/kotlinx-coroutines-core-jvm-1.8.0.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/eclipse/xtend/org.eclipse.xtend.lib/2.28.0/org.eclipse.xtend.lib-2.28.0.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/jetbrains/kotlin/kotlin-stdlib/1.9.21/kotlin-stdlib-1.9.21.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/jetbrains/annotations/23.0.0/annotations-23.0.0.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/eclipse/xtext/org.eclipse.xtext.xbase.lib/2.28.0/org.eclipse.xtext.xbase.lib-2.28.0.jar:/Users/joao/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/eclipse/xtend/org.eclipse.xtend.lib.macro/2.28.0/org.eclipse.xtend.lib.macro-2.28.0.jar", - "org.jetbrains.bsp.bazel.server.ServerInitializer", - "/Users/joao/code/VerifiedSCION", - "/Users/joao/code/VerifiedSCION/projectview.bazelproject", - "false" - ], - "version": "3.1.0-20240313-89141af-NIGHTLY", - "bspVersion": "2.1.0", - "languages": [ - "scala", - "java", - "kotlin" - ] -} \ No newline at end of file diff --git a/.gitignore b/.gitignore index 89f277b5d..098a44ecb 100644 --- a/.gitignore +++ b/.gitignore @@ -101,3 +101,5 @@ target *.internal .devcontainer .metals +.bazelbsp +.bazel From e070366b4dd475d656896a4419bc2861e09b35a7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Thu, 9 May 2024 15:55:53 +0200 Subject: [PATCH 20/31] del file --- projectview.bazelproject | 11 ----------- 1 file changed, 11 deletions(-) delete mode 100644 projectview.bazelproject diff --git a/projectview.bazelproject b/projectview.bazelproject deleted file mode 100644 index dc4756f49..000000000 --- a/projectview.bazelproject +++ /dev/null @@ -1,11 +0,0 @@ -targets: - //... - -build_manual_targets: false - -derive_targets_from_directories: false - -enabled_rules: - io_bazel_rules_scala - rules_java - rules_jvm From d5369c82dd0f426b77136eb8e30575f71044081e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Thu, 9 May 2024 20:16:13 +0200 Subject: [PATCH 21/31] fix verification error --- router/dataplane.go | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index f97d1069c..39237d7aa 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1717,7 +1717,7 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ acc(p.lastLayer.Mem(nil), R10) // @ preserves (p.lastLayer !== &p.scionLayer && !llIsNil) ==> // @ acc(p.lastLayer.Mem(ub[startLL:endLL]), R10) -// @ requires acc(&p.ingressID, R20) +// @ requires acc(&p.ingressID, R10) // @ preserves acc(&p.infoField) // @ preserves acc(&p.hopField) // @ preserves acc(&p.mac, R10) && p.mac != nil && p.mac.Mem() @@ -1725,7 +1725,7 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ preserves sl.AbsSlice_Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) // @ ensures acc(&p.segmentChange) -// @ ensures acc(&p.ingressID, R20) +// @ ensures acc(&p.ingressID, R10) // @ ensures acc(&p.d, R5) // @ ensures acc(&p.path) // @ ensures acc(&p.rawPkt, R1) @@ -3280,7 +3280,7 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte @*/ ) ( // @ requires p.scionLayer.Mem(ub) // @ requires p.path == p.scionLayer.GetPath(ub) // @ requires sl.AbsSlice_Bytes(ub, 0, len(ub)) -// @ requires acc(&p.ingressID, R20) +// @ requires acc(&p.ingressID, R15) // @ requires acc(&p.segmentChange) && !p.segmentChange // @ preserves acc(&p.srcAddr, R10) && acc(p.srcAddr.Mem(), _) // @ preserves acc(&p.lastLayer, R10) @@ -3296,7 +3296,7 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte @*/ ) ( // @ preserves sl.AbsSlice_Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) // @ ensures acc(&p.segmentChange) -// @ ensures acc(&p.ingressID, R20) +// @ ensures acc(&p.ingressID, R15) // @ ensures acc(&p.d, R5) // @ ensures acc(&p.path, R10) // @ ensures acc(&p.rawPkt, R1) From faa6e9bd49a54b196c4cf69fab7a16b5b9f130cb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Mon, 20 May 2024 11:51:57 +0200 Subject: [PATCH 22/31] change comment format --- router/dataplane.go | 124 ++++++++++++++++++++------------------------ 1 file changed, 56 insertions(+), 68 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index 4e896a972..ce4efc516 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -4003,15 +4003,13 @@ func (p *scionPacketProcessor) prepareSCMP( return nil, serrors.WithCtx(cannotRoute, "details", "unsupported path type", "path type", pathType) } - /*@ - scionBuf := epicPath.GetUnderlyingScionPathBuf(ubPath) - unfold acc(epicPath.Mem(ubPath), R4) - assert ubPath[epic.MetadataLen:] === scionBuf - epicPathUb = ubPath - ubPath = scionBuf - startP += epic.MetadataLen - assert ubPath === ub[startP:endP] - @*/ + // @ scionBuf := epicPath.GetUnderlyingScionPathBuf(ubPath) + // @ unfold acc(epicPath.Mem(ubPath), R4) + // @ assert ubPath[epic.MetadataLen:] === scionBuf + // @ epicPathUb = ubPath + // @ ubPath = scionBuf + // @ startP += epic.MetadataLen + // @ assert ubPath === ub[startP:endP] path = epicPath.ScionPath // @ pathFromEpic = true default: @@ -4019,46 +4017,40 @@ func (p *scionPacketProcessor) prepareSCMP( return nil, serrors.WithCtx(cannotRoute, "details", "unsupported path type", "path type", pathType) } - /*@ - assert pathType == scion.PathType || pathType == epic.PathType - assert typeOf(p.scionLayer.Path) == type[*scion.Raw] || typeOf(p.scionLayer.Path) == type[*epic.Path] - assert !pathFromEpic ==> typeOf(p.scionLayer.Path) == type[*scion.Raw] - assert pathFromEpic ==> typeOf(p.scionLayer.Path) == type[*epic.Path] - sl.SplitRange_Bytes(ub, startP, endP, writePerm) - @*/ + // @ assert pathType == scion.PathType || pathType == epic.PathType + // @ assert typeOf(p.scionLayer.Path) == type[*scion.Raw] || typeOf(p.scionLayer.Path) == type[*epic.Path] + // @ assert !pathFromEpic ==> typeOf(p.scionLayer.Path) == type[*scion.Raw] + // @ assert pathFromEpic ==> typeOf(p.scionLayer.Path) == type[*epic.Path] + // @ sl.SplitRange_Bytes(ub, startP, endP, writePerm) decPath, err := path.ToDecoded( /*@ ubPath @*/ ) if err != nil { - /*@ - sl.CombineRange_Bytes(ub, startP, endP, writePerm) - ghost if pathFromEpic { - epicPath := p.scionLayer.Path.(*epic.Path) - assert acc(path.Mem(ubPath), R4) - fold acc(epicPath.Mem(epicPathUb), R4) - } else { - rawPath := p.scionLayer.Path.(*scion.Raw) - assert acc(path.Mem(ubPath), R4) - assert acc(rawPath.Mem(ubPath), R4) - } - fold acc(p.scionLayer.Mem(ub), R4) - @*/ + // @ sl.CombineRange_Bytes(ub, startP, endP, writePerm) + // @ ghost if pathFromEpic { + // @ epicPath := p.scionLayer.Path.(*epic.Path) + // @ assert acc(path.Mem(ubPath), R4) + // @ fold acc(epicPath.Mem(epicPathUb), R4) + // @ } else { + // @ rawPath := p.scionLayer.Path.(*scion.Raw) + // @ assert acc(path.Mem(ubPath), R4) + // @ assert acc(rawPath.Mem(ubPath), R4) + // @ } + // @ fold acc(p.scionLayer.Mem(ub), R4) return nil, serrors.Wrap(cannotRoute, err, "details", "decoding raw path") } // @ ghost rawPath := path.RawBufferMem(ubPath) revPathTmp, err := decPath.Reverse( /*@ rawPath @*/ ) if err != nil { - /*@ - sl.CombineRange_Bytes(ub, startP, endP, writePerm) - ghost if pathFromEpic { - epicPath := p.scionLayer.Path.(*epic.Path) - assert acc(path.Mem(ubPath), R4) - fold acc(epicPath.Mem(epicPathUb), R4) - } else { - rawPath := p.scionLayer.Path.(*scion.Raw) - assert acc(path.Mem(ubPath), R4) - assert acc(rawPath.Mem(ubPath), R4) - } - fold acc(p.scionLayer.Mem(ub), R4) - @*/ + // @ sl.CombineRange_Bytes(ub, startP, endP, writePerm) + // @ ghost if pathFromEpic { + // @ epicPath := p.scionLayer.Path.(*epic.Path) + // @ assert acc(path.Mem(ubPath), R4) + // @ fold acc(epicPath.Mem(epicPathUb), R4) + // @ } else { + // @ rawPath := p.scionLayer.Path.(*scion.Raw) + // @ assert acc(path.Mem(ubPath), R4) + // @ assert acc(rawPath.Mem(ubPath), R4) + // @ } + // @ fold acc(p.scionLayer.Mem(ub), R4) return nil, serrors.Wrap(cannotRoute, err, "details", "reversing path for SCMP") } // @ assert revPathTmp.Mem(rawPath) @@ -4068,19 +4060,17 @@ func (p *scionPacketProcessor) prepareSCMP( // Revert potential path segment switches that were done during processing. if revPath.IsXover( /*@ rawPath @*/ ) { if err := revPath.IncPath( /*@ rawPath @*/ ); err != nil { - /*@ - sl.CombineRange_Bytes(ub, startP, endP, writePerm) - ghost if pathFromEpic { - epicPath := p.scionLayer.Path.(*epic.Path) - assert acc(path.Mem(ubPath), R4) - fold acc(epicPath.Mem(epicPathUb), R4) - } else { - rawPath := p.scionLayer.Path.(*scion.Raw) - assert acc(path.Mem(ubPath), R4) - assert acc(rawPath.Mem(ubPath), R4) - } - fold acc(p.scionLayer.Mem(ub), R4) - @*/ + // @ sl.CombineRange_Bytes(ub, startP, endP, writePerm) + // @ ghost if pathFromEpic { + // @ epicPath := p.scionLayer.Path.(*epic.Path) + // @ assert acc(path.Mem(ubPath), R4) + // @ fold acc(epicPath.Mem(epicPathUb), R4) + // @ } else { + // @ rawPath := p.scionLayer.Path.(*scion.Raw) + // @ assert acc(path.Mem(ubPath), R4) + // @ assert acc(rawPath.Mem(ubPath), R4) + // @ } + // @ fold acc(p.scionLayer.Mem(ub), R4) return nil, serrors.Wrap(cannotRoute, err, "details", "reverting cross over for SCMP") } } @@ -4107,19 +4097,17 @@ func (p *scionPacketProcessor) prepareSCMP( // @ fold revPath.Mem(rawPath) // @ ) if err := revPath.IncPath( /*@ rawPath @*/ ); err != nil { - /*@ - sl.CombineRange_Bytes(ub, startP, endP, writePerm) - ghost if pathFromEpic { - epicPath := p.scionLayer.Path.(*epic.Path) - assert acc(path.Mem(ubPath), R4) - fold acc(epicPath.Mem(epicPathUb), R4) - } else { - rawPath := p.scionLayer.Path.(*scion.Raw) - assert acc(path.Mem(ubPath), R4) - assert acc(rawPath.Mem(ubPath), R4) - } - fold acc(p.scionLayer.Mem(ub), R4) - @*/ + // @ sl.CombineRange_Bytes(ub, startP, endP, writePerm) + // @ ghost if pathFromEpic { + // @ epicPath := p.scionLayer.Path.(*epic.Path) + // @ assert acc(path.Mem(ubPath), R4) + // @ fold acc(epicPath.Mem(epicPathUb), R4) + // @ } else { + // @ rawPath := p.scionLayer.Path.(*scion.Raw) + // @ assert acc(path.Mem(ubPath), R4) + // @ assert acc(rawPath.Mem(ubPath), R4) + // @ } + // @ fold acc(p.scionLayer.Mem(ub), R4) return nil, serrors.Wrap(cannotRoute, err, "details", "incrementing path for SCMP") } } From e2d8843fb89ea98d5a301e24c5004f5ccc16c8ff Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Mon, 20 May 2024 23:52:21 +0200 Subject: [PATCH 23/31] backup --- pkg/slayers/path/epic/epic_spec.gobra | 12 ++++++++++++ pkg/slayers/path/scion/base_spec.gobra | 9 +++++++++ pkg/slayers/path/scion/decoded_spec.gobra | 1 - pkg/slayers/path/scion/raw_spec.gobra | 7 +++++++ pkg/slayers/scion_spec.gobra | 14 ++++++++++++++ router/dataplane.go | 6 +++--- 6 files changed, 45 insertions(+), 4 deletions(-) diff --git a/pkg/slayers/path/epic/epic_spec.gobra b/pkg/slayers/path/epic/epic_spec.gobra index 46666a552..2367523e0 100644 --- a/pkg/slayers/path/epic/epic_spec.gobra +++ b/pkg/slayers/path/epic/epic_spec.gobra @@ -18,6 +18,8 @@ package epic import ( "github.com/scionproto/scion/pkg/slayers/path" + "github.com/scionproto/scion/pkg/slayers/path/scion" + "github.com/scionproto/scion/verification/utils/slices" ) @@ -44,6 +46,15 @@ func (p *Path) DowngradePerm(buf []byte) { fold p.NonInitMem() } +ghost +requires acc(r.Mem(ub), _) +decreases +pure func (r *Path) GetBase(ub []byte) scion.Base { + return unfolding acc(r.Mem(ub), _) in + r.ScionPath.GetBase(ub[MetadataLen:]) +} + +// TODO: drop ghost requires acc(p.Mem(ub), _) decreases @@ -62,6 +73,7 @@ pure func (p *Path) ValidCurrHF(ghost ub []byte) bool { p.ScionPath.ValidCurrHF(ubPath) } +// TODO: drop this ghost requires acc(p.Mem(ub), _) decreases diff --git a/pkg/slayers/path/scion/base_spec.gobra b/pkg/slayers/path/scion/base_spec.gobra index 75620a731..3124b8900 100644 --- a/pkg/slayers/path/scion/base_spec.gobra +++ b/pkg/slayers/path/scion/base_spec.gobra @@ -57,6 +57,15 @@ pure func (b Base) ValidCurrHfSpec() bool { return 0 <= b.PathMeta.CurrHF && b.PathMeta.CurrHF < b.NumHops } +ghost +decreases +pure func (b Base) ValidCurrFieldsSpec() bool { + return 0 <= b.NumINF && b.NumINF <= MaxINFs && + 0 <= b.NumHops && b.NumHops <= MaxHops && + b.ValidCurrInfSpec() && + b.ValidCurrHfSpec() +} + ghost decreases pure func (b Base) ValidCurrIdxsSpec() bool { diff --git a/pkg/slayers/path/scion/decoded_spec.gobra b/pkg/slayers/path/scion/decoded_spec.gobra index fda3419f3..f9a907199 100644 --- a/pkg/slayers/path/scion/decoded_spec.gobra +++ b/pkg/slayers/path/scion/decoded_spec.gobra @@ -51,7 +51,6 @@ pred (d *Decoded) Mem(ubuf []byte) { * Unfortunately, Gobra does not fully support them yet, so we * introduced this method which acts as a wrapper. */ - // TODO: can this spec be simplified (by removing the access to d.Mem(...))? pure requires acc(d.Mem(ubuf), _) ensures unfolding acc(d.Mem(ubuf), _) in l == d.Base.Len() diff --git a/pkg/slayers/path/scion/raw_spec.gobra b/pkg/slayers/path/scion/raw_spec.gobra index 36018256a..1c0c80eb0 100644 --- a/pkg/slayers/path/scion/raw_spec.gobra +++ b/pkg/slayers/path/scion/raw_spec.gobra @@ -278,6 +278,13 @@ func (r *Raw) Widen(ubuf1, ubuf2 []byte) { /**** End of Lemmas ****/ /**** Start of helpful pure functions ****/ +ghost +requires acc(r.Mem(ub), _) +decreases +pure func (r *Raw) GetBase(ub []byte) Base { + return unfolding acc(r.Mem(ub), _) in r.Base.GetBase() +} + ghost requires acc(r.Mem(ub), _) decreases diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra index d4125611c..4ba06ba0f 100644 --- a/pkg/slayers/scion_spec.gobra +++ b/pkg/slayers/scion_spec.gobra @@ -181,6 +181,7 @@ pred (s *SCION) Mem(ubuf []byte) { (typeOf(s.Path) == type[*onehop.Path] ==> CmnHdrLen + s.AddrHdrLenSpecInternal() + s.Path.Len(ubuf[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen]) <= len(ubuf)) } +// TODO: drop ghost requires acc(s.Mem(ub), _) decreases @@ -193,6 +194,19 @@ pure func (s *SCION) ValidPathMetaData(ghost ub []byte) bool { s.Path.(*epic.Path).ValidCurrIdxs(ubPath)) } +ghost +opaque +requires acc(s.Mem(ub), _) +decreases +pure func (s *SCION) ValidCurrFieldsIfPresent(ghost ub []byte) bool { + return unfolding acc(s.Mem(ub), _) in + let ubPath := s.UBPath(ub) in + (typeOf(s.Path) == type[*scion.Raw] ==> + s.Path.(*scion.Raw).GetBase(ubPath).ValidCurrFieldsSpec()) && + (typeOf(s.Path) == type[*epic.Path] ==> + s.Path.(*epic.Path).GetBase(ubPath).ValidCurrFieldsSpec()) +} + // TODO: simplify the body of the predicate when let expressions // support predicates pred (s *SCION) HeaderMem(ubuf []byte) { diff --git a/router/dataplane.go b/router/dataplane.go index ce4efc516..9f480d6c8 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1975,7 +1975,7 @@ func (p *scionPacketProcessor) packSCMP( // @ requires len(absPkt(ub).CurrSeg.Future) > 0 // @ ensures acc(sl.AbsSlice_Bytes(ub, 0, len(ub)), R1) // @ ensures acc(&p.d, R50) -// @ ensures acc(p.scionLayer.Mem(ub), R6) +// @ ensures acc(p.scionLayer.Mem(ub), R5) // @ ensures acc(&p.path, R20) // @ ensures p.path === p.scionLayer.GetPath(ub) // @ ensures acc(&p.hopField) && acc(&p.infoField) @@ -1984,14 +1984,14 @@ func (p *scionPacketProcessor) packSCMP( // @ let ubPath := p.scionLayer.UBPath(ub) in // @ unfolding acc(p.scionLayer.Mem(ub), R10) in // @ p.path.GetCurrHF(ubPath) < p.path.GetNumHops(ubPath)) -// @ ensures acc(p.scionLayer.Mem(ub), R6) // @ ensures p.d.validResult(respr, false) // @ ensures reserr == nil ==> ( // @ let ubPath := p.scionLayer.UBPath(ub) in // @ unfolding acc(p.scionLayer.Mem(ub), R10) in // @ p.path.GetCurrINF(ubPath) < p.path.GetNumINF(ubPath)) // @ ensures reserr != nil ==> reserr.ErrorMem() -// @ ensures reserr == nil ==> slayers.ValidPktMetaHdr(ub) && p.scionLayer.EqAbsHeader(ub) +// @ ensures reserr == nil ==> +// @ slayers.ValidPktMetaHdr(ub) && p.scionLayer.EqAbsHeader(ub) // @ ensures reserr == nil ==> len(absPkt(ub).CurrSeg.Future) > 0 // @ ensures reserr == nil ==> p.EqAbsHopField(absPkt(ub)) // @ ensures reserr == nil ==> p.EqAbsInfoField(absPkt(ub)) From d7e952eb5d1f036393f8e0c78c7e9cfa9096d6ad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Mon, 17 Jun 2024 21:21:57 +0200 Subject: [PATCH 24/31] reset changes to scion_spec.gobra --- pkg/slayers/scion_spec.gobra | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra index 853a9b66b..9d5689d17 100644 --- a/pkg/slayers/scion_spec.gobra +++ b/pkg/slayers/scion_spec.gobra @@ -182,7 +182,6 @@ pred (s *SCION) Mem(ubuf []byte) { (typeOf(s.Path) == type[*onehop.Path] ==> CmnHdrLen + s.AddrHdrLenSpecInternal() + s.Path.LenSpec(ubuf[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen]) <= len(ubuf)) } -// TODO: drop ghost requires acc(s.Mem(ub), _) decreases @@ -195,19 +194,6 @@ pure func (s *SCION) ValidPathMetaData(ghost ub []byte) bool { s.Path.(*epic.Path).GetBase(ubPath).StronglyValid()) } -ghost -opaque -requires acc(s.Mem(ub), _) -decreases -pure func (s *SCION) ValidCurrFieldsIfPresent(ghost ub []byte) bool { - return unfolding acc(s.Mem(ub), _) in - let ubPath := s.UBPath(ub) in - (typeOf(s.Path) == type[*scion.Raw] ==> - s.Path.(*scion.Raw).GetBase(ubPath).ValidCurrFieldsSpec()) && - (typeOf(s.Path) == type[*epic.Path] ==> - s.Path.(*epic.Path).GetBase(ubPath).ValidCurrFieldsSpec()) -} - // TODO: simplify the body of the predicate when let expressions // support predicates pred (s *SCION) HeaderMem(ubuf []byte) { From 4a5a5f379ffa5d17897045a4b34debb6972e1eb1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 18 Jun 2024 17:41:28 +0200 Subject: [PATCH 25/31] continue making progress --- pkg/slayers/path/scion/raw_spec.gobra | 21 ++++++++++----------- pkg/slayers/scion_spec.gobra | 6 +++--- router/dataplane.go | 7 ++++--- 3 files changed, 17 insertions(+), 17 deletions(-) diff --git a/pkg/slayers/path/scion/raw_spec.gobra b/pkg/slayers/path/scion/raw_spec.gobra index 5fd0ba9a6..df7b48e19 100644 --- a/pkg/slayers/path/scion/raw_spec.gobra +++ b/pkg/slayers/path/scion/raw_spec.gobra @@ -382,15 +382,15 @@ requires validPktMetaHdr(raw) decreases pure func (s *Raw) absPkt(raw []byte) (res io.IO_pkt2) { return let _ := reveal validPktMetaHdr(raw) in - let metaHdr := RawBytesToMetaHdr(raw) in + let metaHdr := RawBytesToMetaHdr(raw) in let currInfIdx := int(metaHdr.CurrINF) in - let currHfIdx := int(metaHdr.CurrHF) in - let seg1Len := int(metaHdr.SegLen[0]) in - let seg2Len := int(metaHdr.SegLen[1]) in - let seg3Len := int(metaHdr.SegLen[2]) in + let currHfIdx := int(metaHdr.CurrHF) in + let seg1Len := int(metaHdr.SegLen[0]) in + let seg2Len := int(metaHdr.SegLen[1]) in + let seg3Len := int(metaHdr.SegLen[2]) in let segs := io.CombineSegLens(seg1Len, seg2Len, seg3Len) in - let segLen := segs.LengthOfCurrSeg(currHfIdx) in - let prevSegLen := segs.LengthOfPrevSeg(currHfIdx) in + let segLen := segs.LengthOfCurrSeg(currHfIdx) in + let prevSegLen := segs.LengthOfPrevSeg(currHfIdx) in let numINF := segs.NumInfoFields() in let offset := HopFieldOffset(numINF, prevSegLen, MetaLen) in io.IO_Packet2 { @@ -407,7 +407,7 @@ requires acc(sl.Bytes(raw, 0, len(raw)), R56) decreases pure func RawBytesToMetaHdr(raw []byte) MetaHdr { return unfolding acc(sl.Bytes(raw, 0, len(raw)), R56) in - let hdr := binary.BigEndian.Uint32(raw[:MetaLen]) in + let hdr := binary.BigEndian.Uint32(raw[:MetaLen]) in DecodedFrom(hdr) } @@ -436,9 +436,8 @@ pure func validPktMetaHdr(raw []byte) bool { let seg3 := int(metaHdr.SegLen[2]) in let segs := io.CombineSegLens(seg1, seg2, seg3) in let base := RawBytesToBase(raw) in - 0 < metaHdr.SegLen[0] && - base.StronglyValid() && - base.CurrInfMatchesCurrHF() && + 0 < metaHdr.SegLen[0] && + base.FullyValid() && PktLen(segs, MetaLen) <= len(raw) } diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra index 9d5689d17..11cea1c74 100644 --- a/pkg/slayers/scion_spec.gobra +++ b/pkg/slayers/scion_spec.gobra @@ -335,8 +335,8 @@ ghost requires 0 < p preserves acc(s.Mem(ub), p) ensures let start := s.PathStartIdx(ub) in - let end := s.PathEndIdx(ub) in - 0 <= start && start <= end && end <= len(ub) + let end := s.PathEndIdx(ub) in + 0 <= start && start <= end && end <= len(ub) decreases func LemmaPathIdxStartEnd(s *SCION, ub []byte, p perm) { unfold acc(s.Mem(ub), p) @@ -461,7 +461,7 @@ pure func ValidPktMetaHdr(raw []byte) bool { let length := GetLength(raw) in length <= len(raw) && unfolding acc(sl.Bytes(raw, 0, len(raw)), R56) in - let _ := Asserting(forall k int :: {&rawHdr[k]} 0 <= k && k < scion.MetaLen ==> &rawHdr[k] == &raw[start + k]) in + let _ := Asserting(forall k int :: {&rawHdr[k]} 0 <= k && k < scion.MetaLen ==> &rawHdr[k] == &raw[start + k]) in let hdr := binary.BigEndian.Uint32(rawHdr) in let metaHdr := scion.DecodedFrom(hdr) in let seg1 := int(metaHdr.SegLen[0]) in diff --git a/router/dataplane.go b/router/dataplane.go index acd869dd7..4ee8b846c 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1972,6 +1972,7 @@ func (p *scionPacketProcessor) packSCMP( return processResult{OutPkt: rawSCMP}, err } +// @ requires acc(sl.Bytes(ub, 0, len(ub)), R1) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires acc(p.scionLayer.Mem(ub), R5) // @ requires acc(&p.path, R20) @@ -1979,8 +1980,6 @@ func (p *scionPacketProcessor) packSCMP( // @ requires acc(&p.hopField) && acc(&p.infoField) // @ requires p.scionLayer.EqAbsHeader(ub) // @ requires p.scionLayer.ValidScionInitSpec(ub) -// @ requires len(absPkt(ub).CurrSeg.Future) > 0 -// @ requires acc(sl.Bytes(ub, 0, len(ub)), R1) // @ ensures acc(sl.Bytes(ub, 0, len(ub)), R1) // @ ensures acc(&p.d, R50) // @ ensures acc(p.scionLayer.Mem(ub), R5) @@ -1999,7 +1998,9 @@ func (p *scionPacketProcessor) packSCMP( // @ p.path.GetCurrINF(ubPath) < p.path.GetNumINF(ubPath)) // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> -// @ slayers.ValidPktMetaHdr(ub) && p.scionLayer.EqAbsHeader(ub) +// @ slayers.ValidPktMetaHdr(ub) && +// @ p.scionLayer.EqAbsHeader(ub) && +// @ p.scionLayer.ValidPathMetaData(ub) // @ ensures reserr == nil ==> len(absPkt(ub).CurrSeg.Future) > 0 // @ ensures reserr == nil ==> p.EqAbsHopField(absPkt(ub)) // @ ensures reserr == nil ==> p.EqAbsInfoField(absPkt(ub)) From dc25b29698fa37f4bb244e208bf19c7d81cc297a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 18 Jun 2024 18:05:46 +0200 Subject: [PATCH 26/31] backup --- router/dataplane.go | 2 ++ 1 file changed, 2 insertions(+) diff --git a/router/dataplane.go b/router/dataplane.go index 4ee8b846c..a94d2f656 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -2823,6 +2823,8 @@ func (p *scionPacketProcessor) processEgress( /*@ ghost ub []byte @*/ ) (reserr // @ ensures reserr == nil ==> p.EqAbsHopField(absPkt(ub)) // @ ensures reserr == nil ==> p.EqAbsInfoField(absPkt(ub)) // @ ensures reserr == nil ==> absPkt(ub) == AbsDoXover(old(absPkt(ub))) +// @ ensures reserr == nil ==> +// @ p.scionLayer.ValidPathMetaData(ub) == old(p.scionLayer.ValidPathMetaData(ub)) // @ decreases func (p *scionPacketProcessor) doXover( /*@ ghost ub []byte @*/ ) (respr processResult, reserr error) { p.segmentChange = true From c6194d19500fd19b45cd23b26c4038719892c8ce Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 18 Jun 2024 23:27:48 +0200 Subject: [PATCH 27/31] simplify spec --- pkg/slayers/scion_spec.gobra | 2 +- router/dataplane.go | 80 +++++++++++++++++++----------------- 2 files changed, 44 insertions(+), 38 deletions(-) diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra index 11cea1c74..56c1dbbba 100644 --- a/pkg/slayers/scion_spec.gobra +++ b/pkg/slayers/scion_spec.gobra @@ -335,7 +335,7 @@ ghost requires 0 < p preserves acc(s.Mem(ub), p) ensures let start := s.PathStartIdx(ub) in - let end := s.PathEndIdx(ub) in + let end := s.PathEndIdx(ub) in 0 <= start && start <= end && end <= len(ub) decreases func LemmaPathIdxStartEnd(s *SCION, ub []byte, p perm) { diff --git a/router/dataplane.go b/router/dataplane.go index a94d2f656..fe1fea807 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1883,36 +1883,32 @@ type macBuffersT struct { epicInput []byte } -// @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) -// @ requires acc(p.scionLayer.Mem(ub), R4) -// @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) -// @ requires ubLL == nil || ubLL === ub[startLL:endLL] -// @ requires acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ requires &p.scionLayer !== p.lastLayer ==> -// @ acc(p.lastLayer.Mem(ubLL), R15) -// @ requires &p.scionLayer === p.lastLayer ==> -// @ ub === ubLL -// @ 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 cause.ErrorMem() -// @ ensures acc(&p.d, R20) -// @ ensures acc(p.scionLayer.Mem(ub), R4) -// @ ensures acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ ensures &p.scionLayer !== p.lastLayer ==> -// @ acc(p.lastLayer.Mem(ubLL), R15) -// @ 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{} ==> +// @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) +// @ requires acc(p.scionLayer.Mem(ub), R4) +// @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) +// @ requires ubLL == nil || ubLL === ub[startLL:endLL] +// @ requires acc(&p.lastLayer, R55) && p.lastLayer != nil +// @ requires acc(p.lastLayer.Mem(ubLL), R15) +// @ 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 cause.ErrorMem() +// @ ensures acc(&p.d, R20) +// @ ensures acc(p.scionLayer.Mem(ub), R4) +// @ ensures acc(&p.lastLayer, R55) && p.lastLayer != nil +// @ ensures acc(p.lastLayer.Mem(ubLL), R15) +// @ 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() -// @ ensures respr !== processResult{} ==> +// @ ensures respr !== processResult{} ==> // @ p.buffer.MemWithoutUBuf(respr.OutPkt) && // @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) -// @ ensures reserr != nil ==> reserr.ErrorMem() -// @ ensures reserr != nil && respr.OutPkt != nil ==> +// @ ensures reserr != nil ==> reserr.ErrorMem() +// @ ensures reserr != nil && respr.OutPkt != nil ==> // @ !slayers.IsSupportedPkt(respr.OutPkt) // @ decreases func (p *scionPacketProcessor) packSCMP( @@ -2942,10 +2938,7 @@ func (p *scionPacketProcessor) egressInterface( /*@ ghost oldPkt io.IO_pkt2 @*/ // @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) // @ requires ubLL == nil || ubLL === ub[startLL:endLL] // @ requires acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ requires &p.scionLayer !== p.lastLayer ==> -// @ acc(p.lastLayer.Mem(ubLL), R15) -// @ requires &p.scionLayer === p.lastLayer ==> -// @ ub === ubLL +// @ requires acc(p.lastLayer.Mem(ubLL), R15) // @ requires acc(&p.buffer, R50) && p.buffer.Mem() // @ requires acc(&p.infoField, R20) // @ requires acc(&p.hopField, R20) @@ -2963,8 +2956,7 @@ func (p *scionPacketProcessor) egressInterface( /*@ ghost oldPkt io.IO_pkt2 @*/ // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures acc(p.scionLayer.Mem(ub), R4) // @ ensures acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ ensures &p.scionLayer !== p.lastLayer ==> -// @ acc(p.lastLayer.Mem(ubLL), R15) +// @ ensures acc(p.lastLayer.Mem(ubLL), R15) // @ ensures acc(&p.buffer, R50) // @ ensures respr === processResult{} ==> // @ p.buffer.Mem() @@ -2975,7 +2967,13 @@ func (p *scionPacketProcessor) egressInterface( /*@ ghost oldPkt io.IO_pkt2 @*/ // @ ensures reserr != nil && respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isIO_val_Unsupported // @ decreases 0 if sync.IgnoreBlockingForTermination() -func (p *scionPacketProcessor) validateEgressUp( /*@ ghost ub []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int, ghost oldPkt io.IO_pkt2 @*/ ) (respr processResult, reserr error) { +func (p *scionPacketProcessor) validateEgressUp( +// @ ghost ub []byte, +// @ ghost ubLL []byte, +// @ ghost startLL int, +// @ ghost endLL int, +// @ ghost oldPkt io.IO_pkt2, +) (respr processResult, reserr error) { egressID := p.egressInterface( /*@ oldPkt @ */ ) // @ p.d.getBfdSessionsMem() // @ ghost if p.d.bfdSessions != nil { unfold acc(accBfdSession(p.d.bfdSessions), _) } @@ -3374,7 +3372,15 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte @*/ ) ( // @ ensures (respr.OutPkt == nil) == (newAbsPkt == io.IO_val_Unit{}) // @ decreases 0 if sync.IgnoreBlockingForTermination() // @ #backend[stateConsolidationMode(6)] -func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, ghost startLL int, ghost endLL int, ghost ioLock gpointer[gsync.GhostMutex], ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error /*@, ghost addrAliasesPkt bool, ghost newAbsPkt io.IO_val @*/) { +func (p *scionPacketProcessor) process( +// @ ghost ub []byte, +// @ ghost llIsNil bool, +// @ ghost startLL int, +// @ ghost endLL int, +// @ ghost ioLock gpointer[gsync.GhostMutex], +// @ ghost ioSharedArg SharedArg, +// @ ghost dp io.DataPlaneSpec, +) (respr processResult, reserr error /*@, ghost addrAliasesPkt bool, ghost newAbsPkt io.IO_val @*/) { if r, err := p.parsePath( /*@ ub @*/ ); err != nil { // @ p.scionLayer.DowngradePerm(ub) return r, err /*@, false, absReturnErr(r) @*/ @@ -4230,9 +4236,9 @@ func (p *scionPacketProcessor) prepareSCMP( // @ ensures -1 <= idx && idx < len(opts) // @ ensures len(processed) == len(opts) // @ ensures len(offsets) == len(opts) -// @ ensures reterr == nil && 0 <= idx ==> processed[idx] +// @ ensures reterr == nil && 0 <= idx ==> processed[idx] // @ ensures reterr == nil && idx == -1 ==> retl === base -// @ ensures reterr == nil && 0 <= idx ==> retl === opts[idx] +// @ ensures reterr == nil && 0 <= idx ==> retl === opts[idx] // @ ensures reterr == nil ==> retl != nil // @ ensures reterr == nil ==> base.Mem(data) // @ ensures reterr == nil && typeOf(base.GetPath(data)) == *scion.Raw ==> From 4c2464dcb17ab9bd07e4d791290c8ea4cedc2923 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 18 Jun 2024 23:48:26 +0200 Subject: [PATCH 28/31] backup --- router/dataplane.go | 112 +++++++++++++++++++++++++------------------- 1 file changed, 63 insertions(+), 49 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index fe1fea807..6ce1d983d 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -2229,36 +2229,41 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte @*/ ) } // invalidSrcIA is a helper to return an SCMP error for an invalid SrcIA. -// @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) -// @ requires acc(p.scionLayer.Mem(ub), R4) -// @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) -// @ requires ubLL == nil || ubLL === ub[startLL:endLL] -// @ requires acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ requires &p.scionLayer !== p.lastLayer ==> +// @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) +// @ requires acc(p.scionLayer.Mem(ub), R4) +// @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) +// @ requires ubLL == nil || ubLL === ub[startLL:endLL] +// @ requires acc(&p.lastLayer, R55) && p.lastLayer != nil +// @ requires &p.scionLayer !== p.lastLayer ==> // @ acc(p.lastLayer.Mem(ubLL), R15) -// @ requires &p.scionLayer === p.lastLayer ==> +// @ requires &p.scionLayer === p.lastLayer ==> // @ ub === ubLL -// @ requires p.scionLayer.ValidPathMetaData(ub) -// @ requires sl.Bytes(ub, 0, len(ub)) -// @ requires acc(&p.ingressID, R15) -// @ requires acc(&p.buffer, R50) && p.buffer.Mem() -// @ ensures acc(&p.d, R20) -// @ ensures acc(p.scionLayer.Mem(ub), R4) -// @ ensures acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ ensures &p.scionLayer !== p.lastLayer ==> +// @ requires p.scionLayer.ValidPathMetaData(ub) +// @ requires sl.Bytes(ub, 0, len(ub)) +// @ requires acc(&p.ingressID, R15) +// @ requires acc(&p.buffer, R50) && p.buffer.Mem() +// @ ensures acc(&p.d, R20) +// @ ensures acc(p.scionLayer.Mem(ub), R4) +// @ ensures acc(&p.lastLayer, R55) && p.lastLayer != nil +// @ ensures &p.scionLayer !== p.lastLayer ==> // @ acc(p.lastLayer.Mem(ubLL), R15) -// @ ensures sl.Bytes(ub, 0, len(ub)) -// @ ensures acc(&p.ingressID, R15) -// @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) -// @ ensures respr === processResult{} ==> +// @ ensures sl.Bytes(ub, 0, len(ub)) +// @ ensures acc(&p.ingressID, R15) +// @ ensures p.d.validResult(respr, false) +// @ ensures acc(&p.buffer, R50) +// @ ensures respr === processResult{} ==> // @ p.buffer.Mem() -// @ ensures respr !== processResult{} ==> +// @ ensures respr !== processResult{} ==> // @ p.buffer.MemWithoutUBuf(respr.OutPkt) && // @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) -// @ ensures reserr != nil ==> reserr.ErrorMem() +// @ ensures reserr != nil ==> reserr.ErrorMem() // @ decreases -func (p *scionPacketProcessor) invalidSrcIA( /*@ ghost ub []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { +func (p *scionPacketProcessor) invalidSrcIA( +// @ ghost ub []byte, +// @ ghost ubLL []byte, +// @ ghost startLL int, +// @ ghost endLL int, +) (respr processResult, reserr error) { // @ establishInvalidSrcIA() return p.packSCMP( slayers.SCMPTypeParameterProblem, @@ -2270,36 +2275,41 @@ func (p *scionPacketProcessor) invalidSrcIA( /*@ ghost ub []byte, ghost ubLL []b } // invalidDstIA is a helper to return an SCMP error for an invalid DstIA. -// @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) -// @ requires acc(p.scionLayer.Mem(ub), R4) -// @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) -// @ requires ubLL == nil || ubLL === ub[startLL:endLL] -// @ requires acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ requires &p.scionLayer !== p.lastLayer ==> +// @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) +// @ requires acc(p.scionLayer.Mem(ub), R4) +// @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) +// @ requires ubLL == nil || ubLL === ub[startLL:endLL] +// @ requires acc(&p.lastLayer, R55) && p.lastLayer != nil +// @ requires &p.scionLayer !== p.lastLayer ==> // @ acc(p.lastLayer.Mem(ubLL), R15) -// @ requires &p.scionLayer === p.lastLayer ==> +// @ requires &p.scionLayer === p.lastLayer ==> // @ ub === ubLL -// @ requires p.scionLayer.ValidPathMetaData(ub) -// @ requires sl.Bytes(ub, 0, len(ub)) -// @ requires acc(&p.ingressID, R15) -// @ requires acc(&p.buffer, R50) && p.buffer.Mem() -// @ ensures acc(&p.d, R20) -// @ ensures acc(p.scionLayer.Mem(ub), R4) -// @ ensures acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ ensures &p.scionLayer !== p.lastLayer ==> +// @ requires p.scionLayer.ValidPathMetaData(ub) +// @ requires sl.Bytes(ub, 0, len(ub)) +// @ requires acc(&p.ingressID, R15) +// @ requires acc(&p.buffer, R50) && p.buffer.Mem() +// @ ensures acc(&p.d, R20) +// @ ensures acc(p.scionLayer.Mem(ub), R4) +// @ ensures acc(&p.lastLayer, R55) && p.lastLayer != nil +// @ ensures &p.scionLayer !== p.lastLayer ==> // @ acc(p.lastLayer.Mem(ubLL), R15) -// @ ensures sl.Bytes(ub, 0, len(ub)) -// @ ensures acc(&p.ingressID, R15) -// @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) -// @ ensures respr === processResult{} ==> +// @ ensures sl.Bytes(ub, 0, len(ub)) +// @ ensures acc(&p.ingressID, R15) +// @ ensures p.d.validResult(respr, false) +// @ ensures acc(&p.buffer, R50) +// @ ensures respr === processResult{} ==> // @ p.buffer.Mem() -// @ ensures respr !== processResult{} ==> +// @ ensures respr !== processResult{} ==> // @ p.buffer.MemWithoutUBuf(respr.OutPkt) && // @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) -// @ ensures reserr != nil ==> reserr.ErrorMem() +// @ ensures reserr != nil ==> reserr.ErrorMem() // @ decreases -func (p *scionPacketProcessor) invalidDstIA( /*@ ghost ub []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int, @*/ ) (respr processResult, reserr error) { +func (p *scionPacketProcessor) invalidDstIA( +// @ ghost ub []byte, +// @ ghost ubLL []byte, +// @ ghost startLL int, +// @ ghost endLL int, +) (respr processResult, reserr error) { // @ establishInvalidDstIA() return p.packSCMP( slayers.SCMPTypeParameterProblem, @@ -4258,9 +4268,13 @@ func (p *scionPacketProcessor) prepareSCMP( // @ decreases // (VerifiedSCION) originally, `base` was declared with type `gopacket.DecodingLayer`. This is unnecessarily complicated for a private function // that is only called once with a parameter of type `*SCION`, and leads to more annyoing post-conditions. -func decodeLayers(data []byte, base *slayers.SCION, - opts ...gopacket.DecodingLayer) (retl gopacket.DecodingLayer, reterr error /*@ , ghost processed seq[bool], ghost offsets seq[offsetPair], ghost idx int @*/) { - +func decodeLayers(data []byte, base *slayers.SCION, opts ...gopacket.DecodingLayer) ( + retl gopacket.DecodingLayer, + reterr error, + // @ ghost processed seq[bool], + // @ ghost offsets seq[offsetPair], + // @ ghost idx int, +) { // @ processed = seqs.NewSeqBool(len(opts)) // @ offsets = newOffsetPair(len(opts)) // @ idx = -1 From 2b178e8994a9145118ddc92e8c87d70039cda49c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 21 Jun 2024 12:14:00 +0200 Subject: [PATCH 29/31] non-termination again --- router/dataplane.go | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index 6ce1d983d..75e9ed15b 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -3327,8 +3327,6 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte @*/ ) ( // @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) // @ requires acc(&p.d, R5) && acc(p.d.Mem(), _) && p.d.WellConfigured() // @ requires p.d.getValSvc() != nil -// The ghost param ub here allows us to introduce a bound variable to p.rawPkt, -// which slightly simplifies the spec // @ requires acc(&p.rawPkt, R1) && ub === p.rawPkt // @ requires acc(&p.path, R10) // @ requires p.scionLayer.Mem(ub) @@ -3336,6 +3334,7 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte @*/ ) ( // @ requires sl.Bytes(ub, 0, len(ub)) // @ requires acc(&p.ingressID, R15) // @ requires acc(&p.segmentChange) && !p.segmentChange +// @ requires acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() // @ preserves acc(&p.srcAddr, R10) && acc(p.srcAddr.Mem(), _) // @ preserves acc(&p.lastLayer, R10) // @ preserves p.lastLayer != nil @@ -3362,8 +3361,11 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte @*/ ) ( // @ 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 reserr == nil ==> p.scionLayer.Mem(ub) -// @ ensures reserr != nil ==> p.scionLayer.NonInitMem() +// @ ensures acc(&p.buffer, R10) +// @ ensures reserr == nil ==> p.scionLayer.Mem(ub) && p.buffer.Mem() +// @ ensures reserr != nil ==> p.scionLayer.NonInitMem() && +// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && +// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) // @ ensures reserr != nil ==> reserr.ErrorMem() // contracts for IO-spec // @ requires p.d.DpAgreesWithSpec(dp) @@ -3510,7 +3512,11 @@ func (p *scionPacketProcessor) process( return r, err /*@, false, absReturnErr(r) @*/ } // @ assert nextPkt == absPkt(ub) - // @ ghost ubLL := llIsNil ? []byte(nil) : ub[startLL:endLL] + // @ ghost ubLL := llIsNil ? []byte(nil) : (p.lastLayer === &p.scionLayer ? ub : ub[startLL:endLL]) + // @ ghost if !llIsNil && p.lastLayer === &p.scionLayer { + // @ startLL = 0 + // @ endLL = len(ub) + // @ } if r, err := p.validateEgressUp( /*@ ub, ubLL, startLL, endLL, nextPkt, @*/ ); err != nil { // @ p.scionLayer.DowngradePerm(ub) return r, err /*@, false, absReturnErr(r) @*/ From 81ca9704caa3f3495b72d4522955224db37eb0a8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Mon, 24 Jun 2024 12:00:22 +0200 Subject: [PATCH 30/31] backup --- router/dataplane.go | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index 75e9ed15b..f8f7cdab0 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1888,7 +1888,8 @@ type macBuffersT struct { // @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) // @ requires ubLL == nil || ubLL === ub[startLL:endLL] // @ requires acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ requires acc(p.lastLayer.Mem(ubLL), R15) +// @ requires &p.scionLayer !== p.lastLayer ==> +// @ acc(p.lastLayer.Mem(ubLL), R15) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires sl.Bytes(ub, 0, len(ub)) // @ requires acc(&p.ingressID, R45) @@ -1896,8 +1897,9 @@ type macBuffersT struct { // @ requires cause.ErrorMem() // @ ensures acc(&p.d, R20) // @ ensures acc(p.scionLayer.Mem(ub), R4) -// @ ensures acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ ensures acc(p.lastLayer.Mem(ubLL), R15) +// @ ensures acc(&p.lastLayer, R55) +// @ ensures &p.scionLayer !== p.lastLayer ==> +// @ acc(p.lastLayer.Mem(ubLL), R15) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures acc(&p.ingressID, R45) // @ ensures p.d.validResult(respr, false) From 6570b454119fca32b53299507bff9db8172e2cc8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Mon, 24 Jun 2024 12:49:56 +0200 Subject: [PATCH 31/31] backup --- router/dataplane.go | 32 +++++++++++++++-------------- router/dataplane_spec.gobra | 40 +++++++++++++++++++++++++++++++++++++ 2 files changed, 57 insertions(+), 15 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index f8f7cdab0..3d9370488 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1426,6 +1426,7 @@ func (p *scionPacketProcessor) reset() (err error) { return nil } +// @ trusted // TODO: drop // @ requires p.sInit() // @ requires sl.Bytes(rawPkt, 0, len(rawPkt)) // @ requires acc(srcAddr.Mem(), _) @@ -1479,7 +1480,7 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // parse SCION header and skip extensions; var err error // @ ghost var processed seq[bool] - // @ ghost var offsets seq[offsetPair] + // ghost var offsets seq[offsetPair] // @ ghost var lastLayerIdx int p.lastLayer, err /*@ , processed, offsets, lastLayerIdx @*/ = decodeLayers(p.rawPkt, &p.scionLayer, &p.hbhLayer, &p.e2eLayer) if err != nil { @@ -4262,25 +4263,26 @@ func (p *scionPacketProcessor) prepareSCMP( // @ ensures reterr == nil && typeOf(base.GetPath(data)) == *scion.Raw ==> // @ base.EqAbsHeader(data) && base.ValidScionInitSpec(data) // @ ensures reterr == nil ==> base.EqPathType(data) -// @ ensures forall i int :: {&opts[i]}{processed[i]} 0 <= i && i < len(opts) ==> -// @ (processed[i] ==> (0 <= offsets[i].start && offsets[i].start <= offsets[i].end && offsets[i].end <= len(data))) -// @ ensures reterr == nil ==> forall i int :: {&opts[i]}{processed[i]} 0 <= i && i < len(opts) ==> -// @ ((processed[i] && !offsets[i].isNil) ==> opts[i].Mem(data[offsets[i].start:offsets[i].end])) -// @ ensures reterr == nil ==> forall i int :: {&opts[i]}{processed[i]} 0 <= i && i < len(opts) ==> -// @ ((processed[i] && offsets[i].isNil) ==> opts[i].Mem(nil)) -// @ ensures reterr == nil ==> forall i int :: {&opts[i]}{processed[i]} 0 <= i && i < len(opts) ==> -// @ (!processed[i] ==> opts[i].NonInitMem()) -// @ ensures reterr != nil ==> base.NonInitMem() -// @ ensures reterr != nil ==> (forall i int :: { &opts[i] } 0 <= i && i < len(opts) ==> opts[i].NonInitMem()) -// @ ensures reterr != nil ==> reterr.ErrorMem() +// @ ensures reterr == nil ==> +// @ forall i int :: { &opts[i] } 0 <= i && i < len(opts) && processed[i] ==> +// @ decRelations[i].IsValid(data) && +// @ opts[i].Mem(decRelations[i].LayerSlice(data)) +// @ ensures reterr == nil ==> +// @ forall i int :: { &opts[i] } 0 <= i && i < len(opts) && !processed[i] ==> +// @ opts[i].NonInitMem() +// @ ensures reterr != nil ==> +// @ base.NonInitMem() && reterr.ErrorMem() +// @ ensures reterr != nil ==> +// @ (forall i int :: { &opts[i] } 0 <= i && i < len(opts) ==> opts[i].NonInitMem()) // @ decreases -// (VerifiedSCION) originally, `base` was declared with type `gopacket.DecodingLayer`. This is unnecessarily complicated for a private function -// that is only called once with a parameter of type `*SCION`, and leads to more annyoing post-conditions. +// (VerifiedSCION) originally, `base` was declared with type `gopacket.DecodingLayer`. This is unnecessarily +// complicated for a private function that is only called once with a parameter of type `*SCION`, and leads +// to more annyoing post-conditions. func decodeLayers(data []byte, base *slayers.SCION, opts ...gopacket.DecodingLayer) ( retl gopacket.DecodingLayer, reterr error, // @ ghost processed seq[bool], - // @ ghost offsets seq[offsetPair], + // @ ghost decRelations seq[decodedLayerRelation], // @ ghost idx int, ) { // @ processed = seqs.NewSeqBool(len(opts)) diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra index 5361ad9c2..1288494f2 100644 --- a/router/dataplane_spec.gobra +++ b/router/dataplane_spec.gobra @@ -164,6 +164,7 @@ pred (err scmpError) ErrorMem() { scmpError implements error +// TODO: drop type offsetPair struct { start int end int @@ -718,3 +719,42 @@ pure func (d *DataPlane) DomainForwardingMetrics() set[uint16] { domain(d.forwardingMetrics) : set[uint16]{} } + +/**** Abstractions for `decodeLayers` and dealing with SCMP packets ****/ +type decodedLayerRelation adt { + decodedLayerIsNil {} + decodedLayerIsBaseLayer {} + decodedLayerIsSubsliceOfBase { + start int + end int + } +} + +ghost +decreases +pure func (l decodedLayerRelation) IsValid(base []byte) bool { + return (match l { + case decodedLayerIsNil{}: + true + case decodedLayerIsBaseLayer{}: + true + case decodedLayerIsSubsliceOfBase{?start, ?end}: + 0 <= start && + start <= end && + end <= len(base) + }) +} + +ghost +requires l.IsValid(base) +decreases +pure func (l decodedLayerRelation) LayerSlice(base []byte) []byte { + return (match l { + case decodedLayerIsNil{}: + nil + case decodedLayerIsBaseLayer{}: + base + case decodedLayerIsSubsliceOfBase{?start, ?end}: + base[start:end] + }) +} \ No newline at end of file