From 598749b6b356aabca7532f149c8b368cfa8d1b1f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Thu, 18 Apr 2024 20:18:38 +0200 Subject: [PATCH] Disable conditionalizePermissions (#319) * Update gobra.yml * Update gobra.yml * fix verification error * fixed precondition of XoverEvent * enable moreJoins impure (#321) * invariant strengthening * undo change to the state consolidator --------- Co-authored-by: mlimbeck Co-authored-by: Dspil --- .github/workflows/gobra.yml | 5 ++--- router/dataplane.go | 11 +++++++---- router/io-spec-abstract-transitions.gobra | 4 ++-- 3 files changed, 11 insertions(+), 9 deletions(-) diff --git a/.github/workflows/gobra.yml b/.github/workflows/gobra.yml index f16eae5a2..137fa6572 100644 --- a/.github/workflows/gobra.yml +++ b/.github/workflows/gobra.yml @@ -416,9 +416,8 @@ jobs: assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }} checkConsistency: ${{ env.checkConsistency }} parallelizeBranches: '1' - # The following flag has a significant influence on the number of branches verified. - # Without it, verification would take a lot longer. - conditionalizePermissions: '1' + conditionalizePermissions: '0' + moreJoins: 'impure' imageVersion: ${{ env.imageVersion }} mceMode: 'on' requireTriggers: ${{ env.requireTriggers }} diff --git a/router/dataplane.go b/router/dataplane.go index 01f71849e..4b22afc2c 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -2678,14 +2678,14 @@ func (p *scionPacketProcessor) doXover( /*@ ghost ub []byte, ghost dp io.DataPla var err error if p.hopField, err = p.path.GetCurrentHopField( /*@ ubPath @*/ ); err != nil { // @ ghost sl.CombineRange_Bytes(ub, startP, endP, writePerm) - // @ fold p.scionLayer.Mem(ub) + // @ fold acc(p.scionLayer.Mem(ub), 1-R55) // @ p.scionLayer.DowngradePerm(ub) // TODO parameter problem invalid path return processResult{}, err } if p.infoField, err = p.path.GetCurrentInfoField( /*@ ubPath @*/ ); err != nil { // @ ghost sl.CombineRange_Bytes(ub, startP, endP, writePerm) - // @ fold p.scionLayer.Mem(ub) + // @ fold acc(p.scionLayer.Mem(ub), 1-R55) // @ p.scionLayer.DowngradePerm(ub) // TODO parameter problem invalid path return processResult{}, err @@ -2696,6 +2696,8 @@ func (p *scionPacketProcessor) doXover( /*@ ghost ub []byte, ghost dp io.DataPla // @ TemporaryAssumeForIO(len(get(old(absPkt(dp, ub)).LeftSeg).History) == 0) // @ TemporaryAssumeForIO(slayers.ValidPktMetaHdr(ub) && p.scionLayer.EqAbsHeader(ub)) // @ TemporaryAssumeForIO(absPkt(dp, ub) == AbsDoXover(old(absPkt(dp, ub)))) + // @ TemporaryAssumeForIO(p.EqAbsHopField(absPkt(dp, ub))) + // @ TemporaryAssumeForIO(p.EqAbsInfoField(absPkt(dp, ub))) // @ fold acc(p.scionLayer.Mem(ub), 1-R55) return processResult{}, nil } @@ -3266,6 +3268,7 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, return r, serrors.WithCtx(err, "info", "after xover") /*@, false, absReturnErr(dp, r) @*/ } // @ assert AbsVerifyCurrentMACConstraint(nextPkt, dp) + // @ unfold acc(p.scionLayer.Mem(ub), R3) } // @ fold acc(p.scionLayer.Mem(ub), R3) // @ assert p.segmentChange ==> nextPkt.RightSeg != none[io.IO_seg2] @@ -3293,6 +3296,7 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, // @ p.d.getExternalMem() // @ if p.d.external != nil { unfold acc(accBatchConn(p.d.external), _) } if c, ok := p.d.external[egressID]; ok { + // @ TemporaryAssumeForIO(egressID != 0) if err := p.processEgress( /*@ ub, dp @*/ ); err != nil { // @ fold p.d.validResult(processResult{}, false) return processResult{}, err /*@, false, absReturnErr(dp, processResult{}) @*/ @@ -4125,8 +4129,7 @@ func decodeLayers(data []byte, base *slayers.SCION, // ghost clean-up: // @ ghost - // @ invariant 0 <= i0 && i0 <= len(opts) - // @ invariant -1 <= c && c <= i0 + // @ invariant -1 <= c && c < i0 // @ invariant len(processed) == len(opts) // @ invariant len(offsets) == len(opts) // @ invariant forall i int :: {&opts[i]} 0 <= i && i < len(opts) ==> acc(&opts[i], R10) diff --git a/router/io-spec-abstract-transitions.gobra b/router/io-spec-abstract-transitions.gobra index 2d36d4054..fb9d60482 100644 --- a/router/io-spec-abstract-transitions.gobra +++ b/router/io-spec-abstract-transitions.gobra @@ -212,7 +212,7 @@ requires len(get(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID).LeftSeg).Fu requires len(get(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID).LeftSeg).History) == 0 requires AbsVerifyCurrentMACConstraint(AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)), dp) requires AbsValidateEgressIDConstraintXover(AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)), dp) -requires AbsEgressInterfaceConstraint(AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)), egressID) +requires egressID != none[io.IO_ifs] ==> AbsEgressInterfaceConstraint(AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)), egressID) requires egressID == none[io.IO_ifs] ==> newPkt == AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)) requires egressID != none[io.IO_ifs] ==> newPkt == AbsProcessEgress(AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID))) preserves acc(ioLock.LockP(), _) && ioLock.LockInv() == SharedInv!< dp, ioSharedArg !>; @@ -227,8 +227,8 @@ func XoverEvent(oldPkt io.IO_pkt2, ingressID option[io.IO_ifs], newPkt io.IO_pkt reveal AbsVerifyCurrentMACConstraint(intermediatePkt1, dp) reveal AbsVerifyCurrentMACConstraint(intermediatePkt2, dp) reveal AbsValidateEgressIDConstraintXover(intermediatePkt2, dp) - reveal AbsEgressInterfaceConstraint(intermediatePkt2, egressID) if(egressID != none[io.IO_ifs]){ + reveal AbsEgressInterfaceConstraint(intermediatePkt2, egressID) reveal AbsProcessEgress(intermediatePkt2) } AtomicXover(oldPkt, ingressID, newPkt, egressID, ioLock, ioSharedArg, dp)