Skip to content

Commit 9a633c3

Browse files
author
aaronbojarski
committed
Merge branch 'master' into upstream
2 parents 05a645c + a6638e1 commit 9a633c3

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

58 files changed

+902
-879
lines changed

‎.github/workflows/gobra.yml‎

Lines changed: 22 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -25,8 +25,9 @@ env:
2525
useZ3API: '0'
2626
viperBackend: 'SILICON'
2727
disableNL: '0'
28-
unsafeWildcardOptimization: '1'
28+
unsafeWildcardOptimization: '0'
2929
overflow: '0'
30+
respectFunctionPrePermAmounts: '0'
3031

3132
jobs:
3233
verify-deps:
@@ -69,6 +70,7 @@ jobs:
6970
disableNL: ${{ env.disableNL }}
7071
viperBackend: ${{ env.viperBackend }}
7172
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
73+
respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
7274
- name: Verify package 'pkg/addr'
7375
uses: viperproject/gobra-action@main
7476
with:
@@ -89,6 +91,7 @@ jobs:
8991
disableNL: ${{ env.disableNL }}
9092
viperBackend: ${{ env.viperBackend }}
9193
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
94+
respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
9295
- name: Verify package 'pkg/experimental/epic'
9396
uses: viperproject/gobra-action@main
9497
with:
@@ -108,6 +111,7 @@ jobs:
108111
disableNL: ${{ env.disableNL }}
109112
viperBackend: ${{ env.viperBackend }}
110113
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
114+
respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
111115
- name: Verify package 'pkg/log'
112116
uses: viperproject/gobra-action@main
113117
with:
@@ -127,6 +131,7 @@ jobs:
127131
disableNL: ${{ env.disableNL }}
128132
viperBackend: ${{ env.viperBackend }}
129133
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
134+
respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
130135
- name: Verify package 'pkg/private/serrors'
131136
uses: viperproject/gobra-action@main
132137
with:
@@ -146,6 +151,7 @@ jobs:
146151
disableNL: ${{ env.disableNL }}
147152
viperBackend: ${{ env.viperBackend }}
148153
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
154+
respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
149155
- name: Verify package 'pkg/scrypto'
150156
uses: viperproject/gobra-action@main
151157
with:
@@ -165,6 +171,7 @@ jobs:
165171
disableNL: ${{ env.disableNL }}
166172
viperBackend: ${{ env.viperBackend }}
167173
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
174+
respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
168175
- name: Verify package 'pkg/slayers'
169176
uses: viperproject/gobra-action@main
170177
with:
@@ -184,6 +191,7 @@ jobs:
184191
disableNL: ${{ env.disableNL }}
185192
viperBackend: ${{ env.viperBackend }}
186193
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
194+
respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
187195
- name: Verify package 'pkg/slayers/path'
188196
uses: viperproject/gobra-action@main
189197
with:
@@ -203,6 +211,7 @@ jobs:
203211
disableNL: ${{ env.disableNL }}
204212
viperBackend: ${{ env.viperBackend }}
205213
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
214+
respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
206215
- name: Verify package 'pkg/slayers/path/empty'
207216
uses: viperproject/gobra-action@main
208217
with:
@@ -222,6 +231,7 @@ jobs:
222231
disableNL: ${{ env.disableNL }}
223232
viperBackend: ${{ env.viperBackend }}
224233
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
234+
respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
225235
- name: Verify package 'pkg/slayers/path/epic'
226236
uses: viperproject/gobra-action@main
227237
with:
@@ -242,6 +252,7 @@ jobs:
242252
disableNL: ${{ env.disableNL }}
243253
viperBackend: ${{ env.viperBackend }}
244254
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
255+
respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
245256
- name: Verify package 'pkg/slayers/path/onehop'
246257
uses: viperproject/gobra-action@main
247258
with:
@@ -261,6 +272,7 @@ jobs:
261272
disableNL: ${{ env.disableNL }}
262273
viperBackend: ${{ env.viperBackend }}
263274
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
275+
respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
264276
- name: Verify package 'pkg/slayers/path/scion'
265277
uses: viperproject/gobra-action@main
266278
with:
@@ -280,6 +292,7 @@ jobs:
280292
disableNL: ${{ env.disableNL }}
281293
viperBackend: ${{ env.viperBackend }}
282294
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
295+
respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
283296
- name: Verify package 'private/topology'
284297
uses: viperproject/gobra-action@main
285298
with:
@@ -299,6 +312,7 @@ jobs:
299312
disableNL: ${{ env.disableNL }}
300313
viperBackend: ${{ env.viperBackend }}
301314
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
315+
respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
302316
- name: Verify package 'private/topology/underlay'
303317
uses: viperproject/gobra-action@main
304318
with:
@@ -318,6 +332,7 @@ jobs:
318332
disableNL: ${{ env.disableNL }}
319333
viperBackend: ${{ env.viperBackend }}
320334
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
335+
respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
321336
- name: Verify package 'private/underlay/conn'
322337
uses: viperproject/gobra-action@main
323338
with:
@@ -337,6 +352,7 @@ jobs:
337352
disableNL: ${{ env.disableNL }}
338353
viperBackend: ${{ env.viperBackend }}
339354
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
355+
respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
340356
- name: Verify package 'private/underlay/sockctrl'
341357
uses: viperproject/gobra-action@main
342358
with:
@@ -356,6 +372,7 @@ jobs:
356372
disableNL: ${{ env.disableNL }}
357373
viperBackend: ${{ env.viperBackend }}
358374
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
375+
respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
359376
- name: Verify package 'router/bfd'
360377
uses: viperproject/gobra-action@main
361378
with:
@@ -375,6 +392,7 @@ jobs:
375392
disableNL: ${{ env.disableNL }}
376393
viperBackend: ${{ env.viperBackend }}
377394
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
395+
respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
378396
- name: Verify package 'router/control'
379397
uses: viperproject/gobra-action@main
380398
with:
@@ -394,6 +412,7 @@ jobs:
394412
disableNL: ${{ env.disableNL }}
395413
viperBackend: ${{ env.viperBackend }}
396414
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
415+
respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
397416
- name: Upload the verification report
398417
uses: actions/upload-artifact@v4
399418
with:
@@ -415,13 +434,7 @@ jobs:
415434
includePaths: ${{ env.includePaths }}
416435
assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
417436
checkConsistency: ${{ env.checkConsistency }}
418-
# Due to a bug introduced in https://github.com/viperproject/gobra/pull/776,
419-
# we must currently disable the chopper, otherwise we well-founded orders
420-
# for termination checking are not available at the chopped Viper parts.
421-
# We should reenable it whenever possible, as it reduces verification time in
422-
# ~8 min (20%).
423-
# chop: 10
424-
parallelizeBranches: '1'
437+
parallelizeBranches: '0'
425438
conditionalizePermissions: '1'
426439
moreJoins: 'impure'
427440
imageVersion: ${{ env.imageVersion }}
@@ -432,3 +445,4 @@ jobs:
432445
disableNL: '0'
433446
viperBackend: ${{ env.viperBackend }}
434447
unsafeWildcardOptimization: '0'
448+
respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}

‎pkg/addr/isdas.go‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -267,8 +267,8 @@ func (ia *IA) UnmarshalText(b []byte) error {
267267
return nil
268268
}
269269

270-
// @ pure
271270
// @ decreases
271+
// @ pure
272272
func (ia IA) IsZero() bool {
273273
return ia == 0
274274
}

‎pkg/experimental/epic/epic.go‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -205,7 +205,8 @@ func CoreFromPktCounter(counter uint32) (uint8, uint32) {
205205

206206
// @ requires len(key) == 16
207207
// @ preserves acc(sl.Bytes(key, 0, len(key)), R50)
208-
// @ ensures reserr == nil ==> res != nil && res.Mem() && res.BlockSize() == 16
208+
// @ ensures reserr == nil ==>
209+
// @ res != nil && res.Mem() && res.BlockSize() == 16
209210
// @ ensures reserr != nil ==> reserr.ErrorMem()
210211
// @ decreases
211212
func initEpicMac(key []byte) (res cipher.BlockMode, reserr error) {

‎pkg/experimental/epic/epic_spec.gobra‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,13 +19,14 @@ package epic
1919
import sl "github.com/scionproto/scion/verification/utils/slices"
2020

2121
pred postInitInvariant() {
22-
acc(&zeroInitVector, _) &&
22+
acc(&zeroInitVector) &&
2323
len(zeroInitVector[:]) == 16 &&
24-
acc(sl.Bytes(zeroInitVector[:], 0, len(zeroInitVector[:])), _)
24+
acc(sl.Bytes(zeroInitVector[:], 0, len(zeroInitVector[:])))
2525
}
2626

2727
// learn the invariant established by init
2828
ghost
29+
trusted // TODO: drop after init invs are added
2930
ensures acc(postInitInvariant(), _)
3031
decreases _
3132
func establishPostInitInvariant()

‎pkg/scrypto/scrypto_spec.gobra‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ import sl "github.com/scionproto/scion/verification/utils/slices"
2727
// calls to it will also succeed. This behaviour is abstracted using this
2828
// ghost function.
2929
ghost
30-
requires acc(sl.Bytes(key, 0, len(key)), _)
30+
requires sl.Bytes(key, 0, len(key))
3131
decreases _
3232
pure func ValidKeyForHash(key []byte) bool
3333

‎pkg/slayers/extn.go‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -158,7 +158,7 @@ func serializeTLVOptionPadding(data []byte, padLength int) {
158158
// serializeTLVOptions serializes options to buf and returns the length of the serialized options.
159159
// Passing in a nil-buffer will treat the serialization as a dryrun that can be used to calculate
160160
// the length needed for the buffer.
161-
// @ requires Uncallable()
161+
// @ requires false
162162
func serializeTLVOptions(buf []byte, options []*tlvOption, fixLengths bool) (res int) {
163163
dryrun := buf == nil
164164
// length start at 2 since the padding needs to be calculated taking the first 2 bytes of the
@@ -326,7 +326,7 @@ func (h *HopByHopExtn) LayerPayload( /*@ ghost ub []byte @*/ ) (res []byte /*@ ,
326326
}
327327

328328
// SerializeTo implementation according to gopacket.SerializableLayer.
329-
// @ requires Uncallable()
329+
// @ requires false
330330
func (h *HopByHopExtn) SerializeTo(b gopacket.SerializeBuffer,
331331
opts gopacket.SerializeOptions) error {
332332

@@ -561,7 +561,7 @@ func checkEndToEndExtnNextHdr(t L4ProtocolType) (err error) {
561561
}
562562

563563
// SerializeTo implementation according to gopacket.SerializableLayer
564-
// @ requires Uncallable()
564+
// @ requires false
565565
func (e *EndToEndExtn) SerializeTo(b gopacket.SerializeBuffer,
566566
opts gopacket.SerializeOptions) error {
567567

@@ -579,7 +579,7 @@ func (e *EndToEndExtn) SerializeTo(b gopacket.SerializeBuffer,
579579

580580
// FindOption returns the first option entry of the given type if any exists,
581581
// or ErrOptionNotFound otherwise.
582-
// @ requires Uncallable()
582+
// @ requires false
583583
func (e *EndToEndExtn) FindOption(typ OptionType) (*EndToEndOption, error) {
584584
for _, o := range e.Options {
585585
if o.OptType == typ {

‎pkg/slayers/extn_spec.gobra‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ pred (h *HopByHopExtn) Mem(ubuf []byte) {
5252

5353
// Gobra is not able to infer that HopByHopExtn is "inheriting"
5454
// the implementation of LayerContents from extnBase.
55-
requires Uncallable()
55+
requires false
5656
func (h *HopByHopExtn) LayerContents() (res []byte) {
5757
res = h.BaseLayer.LayerContents()
5858
return res
@@ -85,7 +85,7 @@ pred (h *HopByHopExtnSkipper) Mem(ubuf []byte) {
8585

8686
// Gobra is not able to infer that HopByHopExtnSkipper is "inheriting"
8787
// the implementation of LayerContents from extnBase.
88-
requires Uncallable()
88+
requires false
8989
func (h *HopByHopExtnSkipper) LayerContents() (res []byte) {
9090
res = h.BaseLayer.LayerContents()
9191
return res
@@ -140,7 +140,7 @@ pred (e *EndToEndExtn) Mem(ubuf []byte) {
140140

141141
// Gobra is not able to infer that EndToEndExtn is "inheriting"
142142
// the implementation of LayerContents from extnBase.
143-
requires Uncallable()
143+
requires false
144144
func (e *EndToEndExtn) LayerContents() (res []byte) {
145145
res = e.BaseLayer.LayerContents()
146146
return res
@@ -175,7 +175,7 @@ pred (e *EndToEndExtnSkipper) Mem(ubuf []byte) {
175175

176176
// Gobra is not able to infer that EndToEndExtnSkipper is "inheriting"
177177
// the implementation of LayerContents from extnBase.
178-
requires Uncallable()
178+
requires false
179179
func (e *EndToEndExtnSkipper) LayerContents() (res []byte) {
180180
res = e.BaseLayer.LayerContents()
181181
return res

‎pkg/slayers/path/empty/empty_spec.gobra‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -35,16 +35,14 @@ func (e Path) DowngradePerm(buf []byte) {
3535
}
3636

3737
ghost
38-
pure
3938
decreases
40-
func (p Path) IsValidResultOfDecoding(b []byte) bool {
39+
pure func (p Path) IsValidResultOfDecoding(b []byte) bool {
4140
return true
4241
}
4342

4443
ghost
45-
pure
4644
decreases
47-
func (p Path) LenSpec(ghost ub []byte) (l int) {
45+
pure func (p Path) LenSpec(ghost ub []byte) (l int) {
4846
return PathLen
4947
}
5048

‎pkg/slayers/path/epic/epic.go‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -225,7 +225,6 @@ func (p *Path) Len( /*@ ghost ubuf []byte @*/ ) (l int) {
225225

226226
// Type returns the EPIC path type identifier.
227227
// @ pure
228-
// @ requires acc(p.Mem(ubuf), _)
229228
// @ ensures t == PathType
230229
// @ decreases
231230
func (p *Path) Type( /*@ ghost ubuf []byte @*/ ) (t path.Type) {

0 commit comments

Comments
 (0)