diff --git a/.github/workflows/gobra.yml b/.github/workflows/gobra.yml index 5d544611d1..163630cc2e 100644 --- a/.github/workflows/gobra.yml +++ b/.github/workflows/gobra.yml @@ -1,3 +1,18 @@ +# This file sets up a workflow that runs Gobra (github.com/viperproject/gobra) +# on selected packages of the SCION implementation. Gobra is a program verifier, +# i.e., it checks that the implementation of each function behaves as expected. +# The expected behaviour of each function is provided as a formal specification +# written in comments above the function signature. When Gobra is not able to +# prove that a function behaves according to its specification, it generates an +# (hopefully) informative error message, which identifies the parts of the code +# where the issues might lie. +# For more information on Gobra and its error messages, check the following: +# - The Gobra Book (WIP): viperproject.github.io/gobra-book/ +# - The tutorial: github.com/viperproject/gobra/blob/master/docs/tutorial.md +# The former covers more features of Gobra and contains more up-to-date +# information, but it is still under construction. + + name: Verify the specified codebase on: @@ -8,32 +23,53 @@ jobs: setup-and-test: runs-on: ubuntu-latest env: - statsFile: '/gobra/stats.json' + imageVersion: 'v25.09' + module: 'github.com/scionproto/scion/' + includePaths: '. ./gobra/stdlib-specs' + continueOnError: true steps: - name: Checkout the SCION repository uses: actions/checkout@v2 - - name: Set-up caching for the verification results - uses: actions/cache@v3 - env: - cache-name: gobra-cache + - name: Check that the package gobra/utils is well-formed + uses: viperproject/gobra-action@v25.09.1 with: - path: ${{ runner.workspace }}/.gobra/cache.json - key: ${{ env.cache-name }} - - name: Verify the specified files - uses: viperproject/gobra-action@v22.10.2 - with: - # Prefix used to resolve SCION packages - module: 'github.com/scionproto/scion/' + packages: 'gobra/utils' # Gobra only verifies files annotated with the header "// +gobra" headerOnly: '1' - # Traverse the entire repository, including nested packages, - # in search for annotated files to verify + timeout: 2m + imageVersion: ${{ env.imageVersion }} + module: ${{ env.module }} + includePaths: ${{ env.includePaths }} + continue-on-error: ${{ env.continueOnError }} + - name: Check that specifications of third-party libraries are well-formed + uses: viperproject/gobra-action@v25.09.1 + with: + projectLocation: 'scion/gobra/stdlib-specs' + headerOnly: '1' + # Check all package specifications in directory stdlib-specs recursive: '1' timeout: 10m - caching: '1' - statsFile: ${{ env.statsFile }} - - name: Upload the verification report - uses: actions/upload-artifact@v4 + imageVersion: ${{ env.imageVersion }} + module: ${{ env.module }} + includePaths: '. ../..' # relative to project location + continue-on-error: ${{ env.continueOnError }} + - name: Verify package `pkg/addr` + uses: viperproject/gobra-action@v25.09.1 + with: + packages: 'pkg/addr' + headerOnly: '1' + timeout: 2m + imageVersion: ${{ env.imageVersion }} + module: ${{ env.module }} + includePaths: ${{ env.includePaths }} + continue-on-error: ${{ env.continueOnError }} + - name: Verify package `pkg/slayers/path` + uses: viperproject/gobra-action@v25.09.1 with: - name: verification_stats.json - path: ${{ env.statsFile }} + packages: 'pkg/slayers/path' + headerOnly: '1' + timeout: 2m + imageVersion: ${{ env.imageVersion }} + module: ${{ env.module }} + includePaths: ${{ env.includePaths }} + continue-on-error: ${{ env.continueOnError }} diff --git a/gobra/README.md b/gobra/README.md new file mode 100644 index 0000000000..de4956e145 --- /dev/null +++ b/gobra/README.md @@ -0,0 +1,22 @@ +# Gobra specs + +This directory contains the formal specification of a small part of the +Go standard library (in [`./stdlib-specs`](./stdlib-specs)) required to +verify the annotated files in the SCION codebase. In addition, we provide +a verified Gobra package in [`./utils`](./utils) that contains useful +definitions that are used in the verified packages of SCION. + +## Contributing + +It is expected that we will need a formal specification for more parts +of the Go standard library as we progress in verifying more code in the +SCION repository. To do so, one may add the type declarations and +signatures of unspecified functions and methods (_without the bodies_), +together with their contracts (i.e., pre- and postconditions), to the +corresponding package specification in directory +[`./stdlib-specs`](./stdlib-specs). + +Given that the specification of the standard library is not verified by +Gobra itself, it is possible to introduce errors when writing the +specification for these methods. Thus, any extensions to the specification +require extreme care from the author of the extensions and from code reviewers. diff --git a/gobra/stdlib-specs/encoding/encoding_spec.gobra b/gobra/stdlib-specs/encoding/encoding_spec.gobra new file mode 100644 index 0000000000..1d752ccabf --- /dev/null +++ b/gobra/stdlib-specs/encoding/encoding_spec.gobra @@ -0,0 +1,26 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package encoding + +type TextUnmarshaler interface { + pred Mem() + + preserves Mem() && acc(text) + ensures err != nil ==> err.ErrorMem() + decreases + UnmarshalText(text []byte) (err error) +} \ No newline at end of file diff --git a/gobra/stdlib-specs/flag/flag_spec.gobra b/gobra/stdlib-specs/flag/flag_spec.gobra new file mode 100644 index 0000000000..be52f67db7 --- /dev/null +++ b/gobra/stdlib-specs/flag/flag_spec.gobra @@ -0,0 +1,28 @@ +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package flag + +type Value interface { + pred Mem() + + preserves Mem() + decreases + String() string + + preserves Mem() + ensures err != nil ==> err.ErrorMem() + decreases + Set(string) (err error) +} \ No newline at end of file diff --git a/gobra/stdlib-specs/fmt/fmt_spec.gobra b/gobra/stdlib-specs/fmt/fmt_spec.gobra new file mode 100644 index 0000000000..206f2d79e3 --- /dev/null +++ b/gobra/stdlib-specs/fmt/fmt_spec.gobra @@ -0,0 +1,32 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package fmt + +import "github.com/scionproto/scion/gobra/utils/" + +preserves forall i int :: { &v[i] } 0 <= i && i < len(v) ==> + acc(&v[i], utils.ReadPerm) +decreases +func Sprintf(format string, v ...interface{}) string + +type Stringer interface { + pred Mem() + + preserves Mem() + decreases + String() string +} \ No newline at end of file diff --git a/gobra/stdlib-specs/hash/hash_spec.gobra b/gobra/stdlib-specs/hash/hash_spec.gobra new file mode 100644 index 0000000000..ca6fd4e32c --- /dev/null +++ b/gobra/stdlib-specs/hash/hash_spec.gobra @@ -0,0 +1,55 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package hash + +import "github.com/scionproto/scion/gobra/utils/" + +type Hash interface { + pred Mem() + + // Implementations of Hash must also implement io.Writer. + preserves Mem() + preserves acc(p, utils.ReadPerm) + ensures 0 <= n && n <= len(p) + // The documentation of this interface states that the Write + // method in implementations of Hash may never fail. + // (https://pkg.go.dev/hash#Hash) + ensures err == nil && n == len(p) + ensures Size() == old(Size()) + len(p) + decreases + Write(p []byte) (n int, err error) + + preserves acc(Mem(), utils.ReadPerm) + requires acc(b) + ensures acc(res) && len(res) == len(b) + Size() + decreases + Sum(b []byte) (res []byte) + + preserves Mem() + decreases + Reset() + + requires Mem() + ensures 0 <= res + decreases + pure Size() (res int) + + requires Mem() + ensures 0 <= res + decreases + pure BlockSize() (res int) +} \ No newline at end of file diff --git a/gobra/stdlib-specs/net/ip.gobra b/gobra/stdlib-specs/net/ip.gobra new file mode 100644 index 0000000000..5f843ac3e9 --- /dev/null +++ b/gobra/stdlib-specs/net/ip.gobra @@ -0,0 +1,30 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package net + +// IP address lengths (bytes). +const ( + IPv4len = 4 + IPv6len = 16 +) + +type IP []byte + +pred (ip IP) Mem() { + (len(ip) == IPv4len || len(ip) == IPv6len) && + forall i int :: { &ip[i] } 0 <= i && i < len(ip) ==> acc(&ip[i]) +} diff --git a/gobra/stdlib-specs/net/iprawsock.gobra b/gobra/stdlib-specs/net/iprawsock.gobra new file mode 100644 index 0000000000..6353717a71 --- /dev/null +++ b/gobra/stdlib-specs/net/iprawsock.gobra @@ -0,0 +1,21 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package net + +ensures err != nil ==> err.ErrorMem() +decreases +func SplitHostPort(hostport string) (host string, port string, err error) \ No newline at end of file diff --git a/gobra/stdlib-specs/net/netip/netip_spec.gobra b/gobra/stdlib-specs/net/netip/netip_spec.gobra new file mode 100644 index 0000000000..7ddd423a0c --- /dev/null +++ b/gobra/stdlib-specs/net/netip/netip_spec.gobra @@ -0,0 +1,62 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package netip + +import "github.com/scionproto/scion/gobra/utils/" + +type Addr struct { + privateField utils.PrivateField +} + +type AddrPort struct { + privateField utils.PrivateField +} + +decreases +func (ip Addr) String() string + +ensures err != nil ==> err.ErrorMem() +decreases +func ParseAddr(s string) (addr Addr, err error) + +decreases +func AddrFrom4(addr [4]byte) Addr + +decreases +func AddrFrom16(addr [16]byte) Addr + +decreases +func (ip Addr) Unmap() Addr + +decreases +func (ip Addr) IsValid() (res bool) + +decreases +func (ip Addr) Is4() bool + +decreases +func (ip Addr) Is6() bool + +ensures acc(b) +decreases +func (ip Addr) AsSlice() (b []byte) + +decreases +func (p AddrPort) IsValid() (res bool) + +decreases +func (p AddrPort) Addr() Addr \ No newline at end of file diff --git a/gobra/stdlib-specs/strconv/atoi_spec.gobra b/gobra/stdlib-specs/strconv/atoi_spec.gobra new file mode 100644 index 0000000000..4644c9025e --- /dev/null +++ b/gobra/stdlib-specs/strconv/atoi_spec.gobra @@ -0,0 +1,25 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package strconv + +// ParseUint is like ParseInt but for unsigned numbers. +requires base == 0 || (2 <= base && base <= 36) +requires 0 < bitSize && bitSize <= 64 +ensures retErr == nil ==> (0 <= ret && ret < Exp(2, bitSize)) +ensures retErr != nil ==> retErr.ErrorMem() +decreases +func ParseUint(s string, base int, bitSize int) (ret uint64, retErr error) \ No newline at end of file diff --git a/gobra/stdlib-specs/strconv/exp.gobra b/gobra/stdlib-specs/strconv/exp.gobra new file mode 100644 index 0000000000..f549027200 --- /dev/null +++ b/gobra/stdlib-specs/strconv/exp.gobra @@ -0,0 +1,58 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +// This file contains a ghost function Exp (the exponentiation function) +// that is useful to specify ParseUInt and other similar functions. It also +// contains two additional lemmas that are useful in discharging proof obligations +// with Gobra. + +package strconv + +// TODO: move to a math library when there is one +// a to the power of b +ghost +requires 0 <= exp +decreases exp +pure func Exp(base int, exp int) (res int) { + return exp == 0 ? 1 : (base * Exp(base, exp - 1)) +} + +ghost +requires 10 <= exp +ensures Exp(2, exp) == 1024 * Exp(2, exp - 10) +decreases +func Exp2to10(exp int) { + assert Exp(2, exp) == 2 * Exp(2, exp - 1) + assert Exp(2, exp) == 4 * Exp(2, exp - 2) + assert Exp(2, exp) == 8 * Exp(2, exp - 3) + assert Exp(2, exp) == 16 * Exp(2, exp - 4) + assert Exp(2, exp) == 32 * Exp(2, exp - 5) + assert Exp(2, exp) == 64 * Exp(2, exp - 6) + assert Exp(2, exp) == 128 * Exp(2, exp - 7) + assert Exp(2, exp) == 256 * Exp(2, exp - 8) + assert Exp(2, exp) == 512 * Exp(2, exp - 9) +} + +ghost +ensures Exp(2, 32) == 4294967296 +decreases +func Exp2to32() { + assert Exp(2, 32) == 2 * Exp(2, 31) + assert Exp(2, 32) == 4 * Exp(2, 30) + Exp2to10(30) + Exp2to10(20) + Exp2to10(10) +} \ No newline at end of file diff --git a/gobra/stdlib-specs/strconv/itoa_spec.gobra b/gobra/stdlib-specs/strconv/itoa_spec.gobra new file mode 100644 index 0000000000..bade4fbce6 --- /dev/null +++ b/gobra/stdlib-specs/strconv/itoa_spec.gobra @@ -0,0 +1,24 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package strconv + +// FormatUint returns the string representation of i in the given base, +// for 2 <= base <= 36. The result uses the lower-case letters 'a' to 'z' +// for digit values >= 10. +requires 2 <= base && base <= 36 +decreases +func FormatUint(i uint64, base int) string \ No newline at end of file diff --git a/gobra/stdlib-specs/strings/builder_spec.gobra b/gobra/stdlib-specs/strings/builder_spec.gobra new file mode 100644 index 0000000000..24de00efbc --- /dev/null +++ b/gobra/stdlib-specs/strings/builder_spec.gobra @@ -0,0 +1,62 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +// This file contains a minimal specification of the type Builder. This +// specification is concerned only with memory safety, crash-freedom and termination. +// No functional properties are specified. + +package strings + +import "github.com/scionproto/scion/gobra/utils" + +// A Builder is used to efficiently build a string using Write methods. +// It minimizes memory copying. The zero value is ready to use. +// Do not copy a non-zero Builder. +type Builder struct { + privateFields utils.PrivateField +} + +pred (b *Builder) Mem() + +// String returns the accumulated string. +preserves b.Mem() +decreases +func (b *Builder) String() string + +requires 0 <= n +preserves b.Mem() +decreases +func (b *Builder) Grow(n int) + +preserves b.Mem() +// The documentation guarantees that calls to WriteString +// never return non-nil errors. +// (https://pkg.go.dev/strings#Builder.WriteString) +ensures n == len(s) && err == nil +decreases +func (b *Builder) WriteString(s string) (n int, err error) + +// This ghost method captures the natural-language sentence +// "The zero value is ready to use". Formally speaking, we may +// "give-up" the ownership of all the fields of b when b is +// freshly allocated, to obtain the ownership of resource b.Mem(), +// which allows us to call the operations specified above on b. +ghost +requires acc(b) +requires *b === Builder{} +ensures b.Mem() +decreases +func (b *Builder) ZeroBuilderIsReadyToUse() \ No newline at end of file diff --git a/gobra/stdlib-specs/strings/strings_spec.gobra b/gobra/stdlib-specs/strings/strings_spec.gobra new file mode 100644 index 0000000000..b38703b2ca --- /dev/null +++ b/gobra/stdlib-specs/strings/strings_spec.gobra @@ -0,0 +1,31 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package strings + +ensures -1 <= res && res < len(s) +decreases +func IndexByte(s string, c byte) (res int) + +decreases +func TrimSuffix(s, suffix string) string + +decreases +func HasSuffix(s, suffix string) (ret bool) + +ensures acc(res) +decreases +func Split(s, sep string) (res []string) \ No newline at end of file diff --git a/gobra/utils/defs.gobra b/gobra/utils/defs.gobra new file mode 100644 index 0000000000..9d4fbc249d --- /dev/null +++ b/gobra/utils/defs.gobra @@ -0,0 +1,46 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package utils + +// This type is used to mark the existence of private fields in +// the specification of types from specified (but not verified) imported +// libraries like the Go standard library. +type PrivateField int + +const ( + // Constants of the form RX stand for permission amounts smaller than 1, + // and thus, stand for "read" but not "write" permissions. If both exist, + // RX+1 is half of RX. + R0 perm = 1/(2 << iota) + R1 + R2 + R3 + R4 + R5 + R6 + R7 + R8 + R9 + R10 + // Small permission amount commonly used as a place-holder for read permissions. + ReadPerm +) + +// Short-hand for the ownership of an entire slice of bytes. +pred ByteSlice(s []byte) { + forall i int :: { &s[i] } 0 <= i && i < len(s) ==> acc(&s[i]) +} \ No newline at end of file diff --git a/pkg/addr/addr.go b/pkg/addr/addr.go index 55bc2170c9..c905b9ac4b 100644 --- a/pkg/addr/addr.go +++ b/pkg/addr/addr.go @@ -12,6 +12,8 @@ // See the License for the specific language governing permissions and // limitations under the License. +// +gobra + package addr import ( @@ -20,6 +22,7 @@ import ( "strconv" "strings" + // @ "github.com/scionproto/scion/gobra/utils" "github.com/scionproto/scion/pkg/private/serrors" ) @@ -31,7 +34,9 @@ type Addr struct { // ParseAddr parses s as an address in the format -,, // returning the result as an Addr. -func ParseAddr(s string) (Addr, error) { +// @ ensures err != nil ==> err.ErrorMem() +// @ decreases +func ParseAddr(s string) (a Addr, err error) { comma := strings.IndexByte(s, ',') if comma < 0 { return Addr{}, serrors.New("invalid address: expected comma", "value", s) @@ -49,6 +54,8 @@ func ParseAddr(s string) (Addr, error) { // MustParseAddr calls ParseAddr(s) and panics on error. // It is intended for use in tests with hard-coded strings. +// @ trusted +// @ requires false func MustParseAddr(s string) Addr { a, err := ParseAddr(s) if err != nil { @@ -57,17 +64,23 @@ func MustParseAddr(s string) Addr { return a } +// @ decreases func (a Addr) String() string { return fmt.Sprintf("%s,%s", a.IA, a.Host) } // Set implements flag.Value interface -func (a *Addr) Set(s string) error { +// @ preserves a.Mem() +// @ ensures err != nil ==> err.ErrorMem() +// @ decreases +func (a *Addr) Set(s string) (err error) { pA, err := ParseAddr(s) if err != nil { return err } + // @ unfold a.Mem() *a = pA + // @ fold a.Mem() return nil } @@ -75,6 +88,9 @@ func (a Addr) MarshalText() ([]byte, error) { return []byte(a.String()), nil } +// @ preserves a.Mem() +// @ preserves acc(b, utils.ReadPerm) +// @ decreases func (a *Addr) UnmarshalText(b []byte) error { return a.Set(string(b)) } diff --git a/pkg/addr/addr_spec.gobra b/pkg/addr/addr_spec.gobra new file mode 100644 index 0000000000..f2028e1e0f --- /dev/null +++ b/pkg/addr/addr_spec.gobra @@ -0,0 +1,21 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package addr + +pred (a *Addr) Mem() { + acc(a) +} \ No newline at end of file diff --git a/pkg/addr/fmt.go b/pkg/addr/fmt.go index e305877efd..7271d52e7f 100644 --- a/pkg/addr/fmt.go +++ b/pkg/addr/fmt.go @@ -12,6 +12,8 @@ // See the License for the specific language governing permissions and // limitations under the License. +// +gobra + package addr import ( @@ -24,6 +26,8 @@ import ( // ParseFormattedIA parses an IA that was formatted with the FormatIA function. // The same options must be provided to successfully parse. +// @ trusted +// @ requires false func ParseFormattedIA(ia string, opts ...FormatOption) (IA, error) { parts := strings.Split(ia, "-") if len(parts) != 2 { @@ -33,15 +37,17 @@ func ParseFormattedIA(ia string, opts ...FormatOption) (IA, error) { if err != nil { return 0, serrors.Wrap("parsing ISD part", err, "value", ia) } - as, err := ParseFormattedAS(parts[1], opts...) + a, err := ParseFormattedAS(parts[1], opts...) if err != nil { return 0, serrors.Wrap("parsing AS part", err, "value", ia) } - return MustIAFrom(isd, as), nil + return MustIAFrom(isd, a), nil } // ParseFormattedISD parses an ISD number that was formatted with the FormatISD // function. The same options must be provided to successfully parse. +// @ trusted +// @ requires false func ParseFormattedISD(isd string, opts ...FormatOption) (ISD, error) { o := applyFormatOptions(opts) if o.defaultPrefix { @@ -56,29 +62,35 @@ func ParseFormattedISD(isd string, opts ...FormatOption) (ISD, error) { // ParseFormattedAS parses an AS number that was formatted with the FormatAS // function. The same options must be provided to successfully parse. -func ParseFormattedAS(as string, opts ...FormatOption) (AS, error) { +// @ trusted +// @ requires false +func ParseFormattedAS(a string, opts ...FormatOption) (AS, error) { o := applyFormatOptions(opts) if o.defaultPrefix { - trimmed := strings.TrimPrefix(as, "AS") - if trimmed == as { - return 0, serrors.New("prefix is missing", "prefix", "AS", "value", as) + trimmed := strings.TrimPrefix(a, "AS") + if trimmed == a { + return 0, serrors.New("prefix is missing", "prefix", "AS", "value", a) } - as = trimmed + a = trimmed } - return parseAS(as, o.separator) + return parseAS(a, o.separator) } // FormatIA formats the ISD-AS. +// @ trusted +// @ requires false func FormatIA(ia IA, opts ...FormatOption) string { o := applyFormatOptions(opts) - as := fmtAS(ia.AS(), o.separator) + a := fmtAS(ia.AS(), o.separator) if o.defaultPrefix { - return fmt.Sprintf("ISD%d-AS%s", ia.ISD(), as) + return fmt.Sprintf("ISD%d-AS%s", ia.ISD(), a) } - return fmt.Sprintf("%d-%s", ia.ISD(), as) + return fmt.Sprintf("%d-%s", ia.ISD(), a) } // FormatISD formats the ISD number. +// @ trusted +// @ requires false func FormatISD(isd ISD, opts ...FormatOption) string { o := applyFormatOptions(opts) if o.defaultPrefix { @@ -88,44 +100,54 @@ func FormatISD(isd ISD, opts ...FormatOption) string { } // FormatAS formats the AS number. -func FormatAS(as AS, opts ...FormatOption) string { +// @ trusted +// @ requires false +func FormatAS(a AS, opts ...FormatOption) string { o := applyFormatOptions(opts) - s := fmtAS(as, o.separator) + s := fmtAS(a, o.separator) if o.defaultPrefix { return "AS" + s } return s } -func fmtAS(as AS, sep string) string { - if !as.inRange() { - return fmt.Sprintf("%d [Illegal AS: larger than %d]", as, MaxAS) +// @ decreases +func fmtAS(a AS, sep string) string { + if !a.inRange() { + return fmt.Sprintf("%d [Illegal AS: larger than %d]", a, MaxAS) } // Format BGP ASes as decimal - if as <= MaxBGPAS { - return strconv.FormatUint(uint64(as), 10) + if a <= MaxBGPAS { + return strconv.FormatUint(uint64(a), 10) } // Format all other ASes as 'sep'-separated hex. - const maxLen = len("ffff:ffff:ffff") - var b strings.Builder + var maxLen = len("ffff:ffff:ffff") + var b /*@@@*/ strings.Builder + // @ b.ZeroBuilderIsReadyToUse() b.Grow(maxLen) + // @ invariant b.Mem() + // @ decreases asParts - i for i := 0; i < asParts; i++ { if i > 0 { b.WriteString(sep) } shift := uint(asPartBits * (asParts - i - 1)) - b.WriteString(strconv.FormatUint(uint64(as>>shift)&asPartMask, asPartBase)) + b.WriteString(strconv.FormatUint(uint64(a>>shift)&asPartMask, asPartBase)) } return b.String() } -type FormatOption func(*formatOptions) +// The following is a type alias instead of a declared type. Currently, Gobra does +// not support this type declaration. +type FormatOption = func(*formatOptions) type formatOptions struct { defaultPrefix bool separator string } +// @ trusted +// @ requires false func applyFormatOptions(opts []FormatOption) formatOptions { o := formatOptions{ defaultPrefix: false, @@ -139,6 +161,8 @@ func applyFormatOptions(opts []FormatOption) formatOptions { // WithDefaultPrefix enables the default prefix which depends on the type. For // the AS number, the prefix is 'AS'. For the ISD number, the prefix is 'ISD'. +// @ trusted +// @ requires false func WithDefaultPrefix() FormatOption { return func(o *formatOptions) { o.defaultPrefix = true @@ -147,6 +171,8 @@ func WithDefaultPrefix() FormatOption { // WithSeparator sets the separator to use for formatting AS numbers. In case of // the empty string, the ':' is used. +// @ trusted +// @ requires false func WithSeparator(separator string) FormatOption { return func(o *formatOptions) { o.separator = separator @@ -154,6 +180,8 @@ func WithSeparator(separator string) FormatOption { } // WithFileSeparator returns an option that sets the separator to underscore. +// @ trusted +// @ requires false func WithFileSeparator() FormatOption { return WithSeparator("_") } diff --git a/pkg/addr/host.go b/pkg/addr/host.go index 6daa3a3f15..908cbba819 100644 --- a/pkg/addr/host.go +++ b/pkg/addr/host.go @@ -14,6 +14,8 @@ // See the License for the specific language governing permissions and // limitations under the License. +// +gobra + package addr import ( @@ -30,6 +32,8 @@ const ( HostTypeSVC ) +// @ requires t.IsValid() +// @ decreases func (t HostAddrType) String() string { switch t { case HostTypeNone: @@ -58,7 +62,9 @@ type Host struct { // returning the result as a Host address. // s can either be a SVC address, in the format supported by ParseSVC(s), // or an IP address in dotted decimal or IPv6 format. -func ParseHost(s string) (Host, error) { +// @ ensures err != nil ==> err.ErrorMem() +// @ decreases +func ParseHost(s string) (h Host, err error) { svc, err := ParseSVC(s) if err == nil { return HostSVC(svc), nil @@ -72,6 +78,8 @@ func ParseHost(s string) (Host, error) { // MustParseHost calls ParseHost(s) and panics on error. // It is intended for use in tests with hard-coded strings. +// @ trusted +// @ requires false func MustParseHost(s string) Host { host, err := ParseHost(s) if err != nil { @@ -81,22 +89,28 @@ func MustParseHost(s string) Host { } // HostIP returns a Host address representing ip, with type HostTypeIP. +// @ decreases func HostIP(ip netip.Addr) Host { return Host{t: HostTypeIP, ip: ip} } // HostSvc returns a Host address representing svc, with type HostTypeSVC. +// @ decreases func HostSVC(svc SVC) Host { return Host{t: HostTypeSVC, svc: svc} } // Type returns the type of the address represented by h. +// @ pure +// @ decreases func (h Host) Type() HostAddrType { return h.t } // IP returns the IP address represented by h. // Panics if h.Type() is not HostTypeIP. +// @ requires h.Type() == HostTypeIP +// @ decreases func (h Host) IP() netip.Addr { if h.t != HostTypeIP { panic("IP called on non-IP address: " + h.t.String()) @@ -106,6 +120,8 @@ func (h Host) IP() netip.Addr { // SVC returns the SVC address represented by h. // Panics if h.Type() is not HostTypeSVC. +// @ requires h.Type() == HostTypeSVC +// @ decreases func (h Host) SVC() SVC { if h.t != HostTypeSVC { panic("SVC called on non-SVC address: " + h.t.String()) @@ -113,6 +129,8 @@ func (h Host) SVC() SVC { return h.svc } +// @ requires h.Type().IsValid() +// @ decreases func (h Host) String() string { switch t := h.Type(); t { case HostTypeNone: @@ -127,11 +145,15 @@ func (h Host) String() string { } // Set implements flag.Value interface +// @ preserves h.Mem() +// @ decreases func (h *Host) Set(s string) error { pH, err := ParseHost(s) if err != nil { return err } + // @ unfold h.Mem() *h = pH + // @ fold h.Mem() return nil } diff --git a/pkg/addr/host_spec.gobra b/pkg/addr/host_spec.gobra new file mode 100644 index 0000000000..40ca3a0e4e --- /dev/null +++ b/pkg/addr/host_spec.gobra @@ -0,0 +1,27 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package addr + +pred (h *Host) Mem() { + acc(h) +} + +ghost +decreases +pure func (h HostAddrType) IsValid() bool { + return h == HostTypeNone || h == HostTypeIP || h == HostTypeSVC +} \ No newline at end of file diff --git a/pkg/addr/isdas.go b/pkg/addr/isdas.go index 42367fe28e..e5cc8e01d9 100644 --- a/pkg/addr/isdas.go +++ b/pkg/addr/isdas.go @@ -13,6 +13,8 @@ // See the License for the specific language governing permissions and // limitations under the License. +// +gobra + package addr import ( @@ -22,6 +24,7 @@ import ( "strconv" "strings" + // @ "github.com/scionproto/scion/gobra/utils" "github.com/scionproto/scion/pkg/private/serrors" ) @@ -46,7 +49,9 @@ type ISD uint16 // ParseISD parses an ISD from a decimal string. Note that ISD 0 is parsed // without any errors. -func ParseISD(s string) (ISD, error) { +// @ ensures err != nil ==> err.ErrorMem() +// @ decreases +func ParseISD(s string) (res ISD, err error) { isd, err := strconv.ParseUint(s, 10, ISDBits) if err != nil { return 0, serrors.Wrap("parsing ISD", err) @@ -56,6 +61,8 @@ func ParseISD(s string) (ISD, error) { // MustParseISD parses s and returns the corresponding addr.ISD object. It panics // if s is not valid ISD representation. +// @ trusted +// @ requires false func MustParseISD(s string) ISD { isd, err := ParseISD(s) if err != nil { @@ -64,6 +71,7 @@ func MustParseISD(s string) ISD { return isd } +// @ decreases func (isd ISD) String() string { return strconv.FormatUint(uint64(isd), 10) } @@ -76,76 +84,106 @@ type AS uint64 // ParseAS parses an AS from a decimal (in the case of the 32bit BGP AS number // space) or ipv6-style hex (in the case of SCION-only AS numbers) string. -func ParseAS(as string) (AS, error) { - return parseAS(as, ":") +// @ ensures err == nil ==> res.InRangeSpec() +// @ ensures err != nil ==> err.ErrorMem() +// @ decreases +func ParseAS(a string) (res AS, err error) { + return parseAS(a, ":") } // MustParseAS parses s and returns the corresponding addr.AS object. It panics // if s is not valid AS representation. +// @ trusted +// @ requires false func MustParseAS(s string) AS { - as, err := ParseAS(s) + a, err := ParseAS(s) if err != nil { panic(err) } - return as + return a } -func parseAS(as string, sep string) (AS, error) { - parts := strings.Split(as, sep) +// @ ensures err == nil ==> res.InRangeSpec() +// @ ensures err != nil ==> err.ErrorMem() +// @ decreases +func parseAS(a string, sep string) (res AS, err error) { + parts := strings.Split(a, sep) if len(parts) == 1 { // Must be a BGP AS, parse as 32-bit decimal number - return asParseBGP(as) + return asParseBGP(a) } if len(parts) != asParts { - return 0, serrors.New("wrong number of separators", "sep", sep, "value", as) + return 0, serrors.New("wrong number of separators", "sep", sep, "value", a) } var parsed AS + //@ invariant 0 <= i && i <= asParts + //@ invariant acc(parts) + //@ decreases asParts - i for i := 0; i < asParts; i++ { parsed <<= asPartBits v, err := strconv.ParseUint(parts[i], asPartBase, asPartBits) if err != nil { - return 0, serrors.Wrap("parsing AS part", err, "index", i, "value", as) + return 0, serrors.Wrap("parsing AS part", err, "index", i, "value", a) } parsed |= AS(v) } // This should not be reachable. However, we leave it here to protect // against future refactor mistakes. if !parsed.inRange() { - return 0, serrors.New("AS out of range", "max", MaxAS, "value", as) + return 0, serrors.New("AS out of range", "max", MaxAS, "value", a) } return parsed, nil } -func asParseBGP(s string) (AS, error) { - as, err := strconv.ParseUint(s, 10, BGPASBits) +// @ ensures err == nil ==> res.InRangeSpec() +// @ ensures err != nil ==> err.ErrorMem() +// @ decreases +func asParseBGP(s string) (res AS, err error) { + a, err := strconv.ParseUint(s, 10, BGPASBits) if err != nil { return 0, serrors.Wrap("parsing BGP AS", err) } - return AS(as), nil + // The following annotation is needed to prove res.InRangeSpec(). + // Gobra is not able to establish the upper limit of a without this + // annotation. + // @ strconv.Exp2to32() + return AS(a), nil } -func (as AS) String() string { - return fmtAS(as, ":") +// @ decreases +func (a AS) String() string { + return fmtAS(a, ":") } -func (as AS) inRange() bool { - return as <= MaxAS +// @ ensures res == a.InRangeSpec() +// @ decreases +func (a AS) inRange() (res bool) { + return a <= MaxAS } -func (as AS) MarshalText() ([]byte, error) { - if !as.inRange() { - return nil, serrors.New("AS out of range", "max", MaxAS, "value", as) +// @ ensures err == nil ==> acc(res) +// @ ensures err != nil ==> err.ErrorMem() +// @ decreases +func (a AS) MarshalText() (res []byte, err error) { + if !a.inRange() { + return nil, serrors.New("AS out of range", "max", MaxAS, "value", a) } - return []byte(as.String()), nil + return []byte(a.String()), nil } -func (as *AS) UnmarshalText(text []byte) error { +// @ preserves a.Mem() +// @ preserves acc(text, utils.ReadPerm) +// @ ensures err != nil ==> err.ErrorMem() +// @ decreases +func (a *AS) UnmarshalText(text []byte) (err error) { parsed, err := ParseAS(string(text)) if err != nil { return err } - *as = parsed + // @ unfold a.Mem() + *a = parsed + // @ fold a.Mem() return nil } @@ -162,8 +200,10 @@ type IA uint64 // MustIAFrom creates an IA from the ISD and AS number. It panics if any error // is encountered. Callers must ensure that the values passed to this function // are valid. -func MustIAFrom(isd ISD, as AS) IA { - ia, err := IAFrom(isd, as) +// @ requires a.InRangeSpec() +// @ decreases +func MustIAFrom(isd ISD, a AS) IA { + ia, err := IAFrom(isd, a) if err != nil { panic(fmt.Sprintf("parsing ISD-AS: %v", err)) } @@ -171,15 +211,20 @@ func MustIAFrom(isd ISD, as AS) IA { } // IAFrom creates an IA from the ISD and AS number. -func IAFrom(isd ISD, as AS) (IA, error) { - if !as.inRange() { - return 0, serrors.New("AS out of range", "max", MaxAS, "value", as) +// @ ensures a.InRangeSpec() == (err == nil) +// @ ensures err != nil ==> err.ErrorMem() +// @ decreases +func IAFrom(isd ISD, a AS) (ret IA, err error) { + if !a.inRange() { + return 0, serrors.New("AS out of range", "max", MaxAS, "value", a) } - return IA(isd)< err.ErrorMem() +// @ decreases +func ParseIA(ia string) (res IA, err error) { parts := strings.Split(ia, "-") if len(parts) != 2 { return 0, serrors.New("invalid ISD-AS", "value", ia) @@ -188,15 +233,17 @@ func ParseIA(ia string) (IA, error) { if err != nil { return 0, err } - as, err := ParseAS(parts[1]) + a, err := ParseAS(parts[1]) if err != nil { return 0, err } - return MustIAFrom(isd, as), nil + return MustIAFrom(isd, a), nil } // MustParseIA parses s and returns the corresponding addr.IA object. It // panics if s is not a valid ISD-AS representation. +// @ trusted +// @ requires false func MustParseIA(s string) IA { ia, err := ParseIA(s) if err != nil { @@ -205,24 +252,35 @@ func MustParseIA(s string) IA { return ia } +// @ decreases func (ia IA) ISD() ISD { return ISD(ia >> ASBits) } +// @ decreases func (ia IA) AS() AS { return AS(ia) & MaxAS } -func (ia IA) MarshalText() ([]byte, error) { +// @ ensures acc(s) +// @ ensures err == nil +// @ decreases +func (ia IA) MarshalText() (s []byte, err error) { return []byte(ia.String()), nil } -func (ia *IA) UnmarshalText(b []byte) error { +// @ preserves ia.Mem() +// @ preserves acc(b, utils.ReadPerm) +// @ ensures err != nil ==> err.ErrorMem() +// @ decreases +func (ia *IA) UnmarshalText(b []byte) (err error) { parsed, err := ParseIA(string(b)) if err != nil { return err } + // @ unfold ia.Mem() *ia = parsed + // @ fold ia.Mem() return nil } @@ -239,16 +297,22 @@ func (ia IA) IsWildcard() bool { return ia.ISD() == 0 || ia.AS() == 0 } +// @ decreases func (ia IA) String() string { return fmt.Sprintf("%d-%s", ia.ISD(), ia.AS()) } // Set implements flag.Value interface -func (ia *IA) Set(s string) error { +// @ preserves ia.Mem() +// @ ensures err != nil ==> err.ErrorMem() +// @ decreases +func (ia *IA) Set(s string) (err error) { pIA, err := ParseIA(s) if err != nil { return err } + // @ unfold ia.Mem() *ia = pIA + // @ fold ia.Mem() return nil } diff --git a/pkg/addr/isdas_spec.gobra b/pkg/addr/isdas_spec.gobra new file mode 100644 index 0000000000..db421cf7ef --- /dev/null +++ b/pkg/addr/isdas_spec.gobra @@ -0,0 +1,57 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package addr + +import ( + "fmt" + "encoding" + "flag" +) + +pred (ia *IA) Mem() { + acc(ia) +} + +pred (a *AS) Mem() { + acc(a) +} + +// Implementation proof would confuse the two predicates named Mem for IA and *IA +// Issue: https://github.com/viperproject/gobra/issues/449 +pred MemForStringer(ia IA) { + true +} + +IA implements fmt.Stringer { + pred Mem := MemForStringer +} + +(*IA) implements encoding.TextUnmarshaler + +(*AS) implements encoding.TextUnmarshaler + +(*IA) implements flag.Value + +// While this function may appear redundant (it's the same as inRange), +// this function is part of the public API and thus, may be used in the +// specification of public functions and methods. We should consider +// making inRange part of the public API of AS. +ghost +decreases +pure func (a AS) InRangeSpec() bool { + return a <= MaxAS +} \ No newline at end of file diff --git a/pkg/addr/svc.go b/pkg/addr/svc.go index d69ab926bc..9b9041ab05 100644 --- a/pkg/addr/svc.go +++ b/pkg/addr/svc.go @@ -12,6 +12,8 @@ // See the License for the specific language governing permissions and // limitations under the License. +// +gobra + package addr import ( @@ -46,7 +48,9 @@ type SVC uint16 // SVC addresses, use CS_A and DS_A; shorthand versions without // the _A suffix (e.g., CS) also return anycast SVC addresses. For multicast, // use CS_M, and DS_M. -func ParseSVC(str string) (SVC, error) { +// @ ensures err != nil ==> err.ErrorMem() +// @ decreases +func ParseSVC(str string) (res SVC, err error) { var m SVC switch { case strings.HasSuffix(str, "_A"): @@ -68,20 +72,24 @@ func ParseSVC(str string) (SVC, error) { } // IsMulticast returns the value of the multicast flag. +// @ decreases func (h SVC) IsMulticast() bool { return (h & SVCMcast) != 0 } // Base returns the SVC identifier with the multicast flag unset. +// @ decreases func (h SVC) Base() SVC { return h & ^SVCMcast } // Multicast returns the SVC identifier with the multicast flag set. +// @ decreases func (h SVC) Multicast() SVC { return h | SVCMcast } +// @ decreases func (h SVC) String() string { s := h.BaseString() if h.IsMulticast() { @@ -92,6 +100,7 @@ func (h SVC) String() string { // BaseString returns the upper case name of the service. For unrecognized services, it // returns "". +// @ decreases func (h SVC) BaseString() string { switch h.Base() { case SvcDS: diff --git a/pkg/private/serrors/errors_spec.gobra b/pkg/private/serrors/errors_spec.gobra index 44c715b0a2..a454f463f1 100644 --- a/pkg/private/serrors/errors_spec.gobra +++ b/pkg/private/serrors/errors_spec.gobra @@ -1,4 +1,4 @@ -// Copyright 2022 ETH Zurich +// Copyright 2025 ETH Zurich // // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. @@ -22,8 +22,24 @@ package serrors -// Allocates a new (non-nil) error. -// Calls to this method are assumed to always terminate. -ensures err != nil -decreases _ -func New(msg string, errCtx ...any) (err error) +import "github.com/scionproto/scion/gobra/utils" + +// New creates a new error with the given message and context. +preserves forall i int :: { &errCtx[i] } 0 <= i && i < len(errCtx) ==> + acc(&errCtx[i], utils.ReadPerm) +ensures res != nil && res.ErrorMem() +ensures res.IsDuplicableMem() +ensures isComparable(res) +decreases +func New(msg string, errCtx ...interface{}) (res error) + +// Wrap wraps the cause with the msg error and adds context to the resulting +// error. The returned error implements Is and Is(msg) and Is(cause) returns +// true. +requires cause.ErrorMem() +preserves forall i int :: { &errCtx[i] } 0 <= i && i < len(errCtx) ==> + acc(&errCtx[i], utils.ReadPerm) +ensures res != nil && res.ErrorMem() +ensures res.ErrorMem() --* cause.ErrorMem() +decreases +func Wrap(msg string, cause error, errCtx ...interface{}) (res error) \ No newline at end of file diff --git a/pkg/slayers/path/path.go b/pkg/slayers/path/path.go index 203d90bc5c..029593a930 100644 --- a/pkg/slayers/path/path.go +++ b/pkg/slayers/path/path.go @@ -12,11 +12,14 @@ // See the License for the specific language governing permissions and // limitations under the License. +// +gobra + package path import ( "fmt" + // @ "github.com/scionproto/scion/gobra/utils" "github.com/scionproto/scion/pkg/private/serrors" ) @@ -24,15 +27,20 @@ import ( const maxPathType = 256 var ( - registeredPaths [maxPathType]metadata - strictDecoding bool = true + registeredPaths/*@@@*/ [maxPathType]metadata + strictDecoding/*@@@*/ bool = true ) // Type indicates the type of the path contained in the SCION header. type Type uint8 +// @ requires 0 <= t && t < maxPathType +// @ preserves acc(PkgMem(), utils.ReadPerm) +// @ decreases func (t Type) String() string { + // @ unfold acc(PkgMem(), utils.ReadPerm) pm := registeredPaths[t] + // @ fold acc(PkgMem(), utils.ReadPerm) if !pm.inUse { return fmt.Sprintf("UNKNOWN (%d)", t) } @@ -41,17 +49,60 @@ func (t Type) String() string { // Path is the path contained in the SCION header. type Path interface { + + // Ownserhip of all necessary memory locations required to safely call + // DecodeFromBytes() on a Path instance. + //@ pred PreDecodeMem() + + // Ownserhip of all memory locations on an instance of Path initialized + // via a call to DecodeFromBytes. + //@ pred Mem() + + // Returns the slice of bytes from which the Path instance was decoded. + // @ ghost + // @ pure + // @ requires Mem() + // @ decreases + // @ DecodedFrom() []byte + // SerializeTo serializes the path into the provided buffer. - SerializeTo(b []byte) error + // @ preserves acc(Mem(), utils.ReadPerm) + // SerializeTo takes full ownership of the slice from which + // the instance was decoded, which allows for that slice to + // be mutated during the call to this method. This is perhaps + // surpising; one may expect that that slice is only read. + // However, the implementations of this method for type *Raw + // (declared in pkg/slayers/scion) does mutate the slice. + // @ preserves acc(utils.ByteSlice(DecodedFrom())) + // @ preserves utils.ByteSlice(b) + // @ ensures err != nil ==> err.ErrorMem() + SerializeTo(b []byte) (err error) + // DecodesFromBytes decodes the path from the provided buffer. - DecodeFromBytes(b []byte) error + // @ requires PreDecodeMem() + // @ preserves acc(utils.ByteSlice(b), utils.ReadPerm) + // @ ensures err == nil ==> Mem() && DecodedFrom() === b + // @ ensures err != nil ==> err.ErrorMem() && PreDecodeMem() + DecodeFromBytes(b []byte) (err error) + // Reverse reverses a path such that it can be used in the reversed direction. // // XXX(shitz): This method should possibly be moved to a higher-level path manipulation package. - Reverse() (Path, error) + // @ requires Mem() + // @ requires acc(utils.ByteSlice(DecodedFrom())) + // @ ensures acc(utils.ByteSlice(old(DecodedFrom()))) + // @ ensures err == nil ==> + // @ p != nil && p.Mem() && p.DecodedFrom() === old(DecodedFrom()) + // @ ensures err != nil ==> err.ErrorMem() + Reverse() (p Path, err error) + // Len returns the length of a path in bytes. - Len() int + // @ preserves acc(Mem(), utils.ReadPerm) + // @ ensures 0 <= res + Len() (res int) + // Type returns the type of a path. + // @ preserves acc(Mem(), utils.ReadPerm) Type() Type } @@ -72,13 +123,20 @@ type Metadata struct { // RegisterPath registers a new SCION path type globally. // The PathType passed in must be unique, or a runtime panic will occur. +// @ requires 0 <= pathMeta.Type && pathMeta.Type < maxPathType +// @ requires PkgMem() && !Registered(pathMeta.Type) +// @ requires pathMeta.New implements NewPathSpec +// @ ensures PkgMem() +// @ decreases func RegisterPath(pathMeta Metadata) { + // @ unfold PkgMem() pm := registeredPaths[pathMeta.Type] if pm.inUse { panic("path type already registered: " + pathMeta.Type.String()) } registeredPaths[pathMeta.Type].inUse = true registeredPaths[pathMeta.Type].Metadata = pathMeta + // @ fold PkgMem() } // StrictDecoding enables or disables strict path decoding. If enabled, unknown @@ -88,12 +146,21 @@ func RegisterPath(pathMeta Metadata) { // Strict parsing is enabled by default. // // Experimental: This function is experimental and might be subject to change. +// @ preserves PkgMem() +// @ decreases func StrictDecoding(strict bool) { + // @ unfold PkgMem() strictDecoding = strict + // @ fold PkgMem() } // NewPath returns a new path object of pathType. +// @ requires 0 <= pathType && pathType < maxPathType +// @ preserves acc(PkgMem(), utils.ReadPerm) +// @ decreases func NewPath(pathType Type) (Path, error) { + // @ unfold acc(PkgMem(), utils.ReadPerm) + // @ defer fold acc(PkgMem(), utils.ReadPerm) pm := registeredPaths[pathType] if !pm.inUse { if strictDecoding { @@ -101,12 +168,16 @@ func NewPath(pathType Type) (Path, error) { } return &rawPath{}, nil } - return pm.New(), nil + return pm.New() /*@ as NewPathSpec @*/, nil } // NewRawPath returns a new raw path that can hold any path type. -func NewRawPath() Path { - return &rawPath{} +// @ ensures res.PreDecodeMem() +// @ decreases +func NewRawPath() (res Path) { + p := &rawPath{} + // @ fold p.PreDecodeMem() + return p } type rawPath struct { @@ -114,24 +185,55 @@ type rawPath struct { pathType Type } -func (p *rawPath) SerializeTo(b []byte) error { - copy(b, p.raw) +// @ preserves acc(p.Mem(), utils.ReadPerm) +// @ preserves acc(utils.ByteSlice(p.DecodedFrom()), utils.ReadPerm) +// @ preserves utils.ByteSlice(b) +// @ ensures p.DecodedFrom() === old(p.DecodedFrom()) +// @ ensures err != nil ==> err.ErrorMem() +// @ decreases +func (p *rawPath) SerializeTo(b []byte) (err error) { + // @ ghost buf := p.DecodedFrom() + // @ unfold acc(p.Mem(), utils.ReadPerm) + // @ assert buf === p.raw + + // @ unfold utils.ByteSlice(b) + // @ unfold acc(utils.ByteSlice(p.raw), utils.ReadPerm) + copy(b, p.raw /*@, utils.ReadPerm @*/) + // @ fold acc(utils.ByteSlice(p.raw), utils.ReadPerm) + // @ fold utils.ByteSlice(b) + // @ fold acc(p.Mem(), utils.ReadPerm) return nil } -func (p *rawPath) DecodeFromBytes(b []byte) error { +// @ requires p.PreDecodeMem() +// @ ensures err == nil && p.Mem() && p.DecodedFrom() === b +// @ decreases +func (p *rawPath) DecodeFromBytes(b []byte) (err error) { + // @ unfold p.PreDecodeMem() p.raw = b + // @ fold p.Mem() return nil } -func (p *rawPath) Reverse() (Path, error) { +// @ ensures err != nil && err.ErrorMem() +// @ decreases +func (p *rawPath) Reverse() (res Path, err error) { return nil, serrors.New("not supported") } -func (p *rawPath) Len() int { +// @ preserves acc(p.Mem(), utils.ReadPerm) +// @ ensures 0 <= res +// @ decreases +func (p *rawPath) Len() (res int) { + // @ unfold acc(p.Mem(), utils.ReadPerm) + // @ defer fold acc(p.Mem(), utils.ReadPerm) return len(p.raw) } +// @ preserves acc(p.Mem(), utils.ReadPerm) +// @ decreases func (p *rawPath) Type() Type { + // @ unfold acc(p.Mem(), utils.ReadPerm) + // @ defer fold acc(p.Mem(), utils.ReadPerm) return p.pathType } diff --git a/pkg/slayers/path/path_spec.gobra b/pkg/slayers/path/path_spec.gobra new file mode 100644 index 0000000000..049e72d92f --- /dev/null +++ b/pkg/slayers/path/path_spec.gobra @@ -0,0 +1,56 @@ +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package path + +import "github.com/scionproto/scion/gobra/utils" + +// Resource PkgMem() stands for the ownership of the global state of this package. +pred PkgMem() { + acc(®isteredPaths) && + acc(&strictDecoding) && + // for every registered path, the allocator function in its metadata satisfies the contract of NewPathSpec. + (forall t Type :: { ®isteredPaths[t].inUse } (0 <= t && t < maxPathType && registeredPaths[t].inUse) ==> + registeredPaths[t].Metadata.New implements NewPathSpec) +} + +ghost +requires 0 <= t && t < maxPathType +requires PkgMem() +decreases +pure func Registered(t Type) (res bool) { + return unfolding PkgMem() in registeredPaths[t].inUse +} + +// Contract that allocator functions for Path implementations stored in +// registeredPaths must implement. +ensures p != nil && p.PreDecodeMem() +decreases +func NewPathSpec() (p Path) + +pred (p *rawPath) PreDecodeMem() { + acc(p) +} + +pred (p *rawPath) Mem() { + acc(p) +} + +ghost +requires p.Mem() +decreases +pure func (p *rawPath) DecodedFrom() []byte { + return unfolding p.Mem() in p.raw +} \ No newline at end of file