diff --git a/pkg/addr/fmt.go b/pkg/addr/fmt.go index ed9b2d9de..753ad39f3 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,7 @@ import ( // ParseFormattedIA parses an IA that was formatted with the FormatIA function. // The same options must be provided to successfully parse. +// @ trusted func ParseFormattedIA(ia string, opts ...FormatOption) (IA, error) { parts := strings.Split(ia, "-") if len(parts) != 2 { @@ -33,15 +36,16 @@ func ParseFormattedIA(ia string, opts ...FormatOption) (IA, error) { if err != nil { return 0, serrors.WrapStr("parsing ISD part", err, "value", ia) } - as, err := ParseFormattedAS(parts[1], opts...) + as_, err := ParseFormattedAS(parts[1], opts...) if err != nil { return 0, serrors.WrapStr("parsing AS part", err, "value", ia) } - return MustIAFrom(isd, as), nil + return MustIAFrom(isd, as_), nil } // ParseFormattedISD parses an ISD number that was formatted with the FormatISD // function. The same options must be provided to successfully parse. +// @ trusted func ParseFormattedISD(isd string, opts ...FormatOption) (ISD, error) { o := applyFormatOptions(opts) if o.defaultPrefix { @@ -56,29 +60,32 @@ 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 +func ParseFormattedAS(as_ 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(as_, "AS") + if trimmed == as_ { + return 0, serrors.New("prefix is missing", "prefix", "AS", "value", as_) } - as = trimmed + as_ = trimmed } - return parseAS(as, o.separator) + return parseAS(as_, o.separator) } // FormatIA formats the ISD-AS. +// @ trusted func FormatIA(ia IA, opts ...FormatOption) string { o := applyFormatOptions(opts) - as := fmtAS(ia.AS(), o.separator) + as_ := 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(), as_) } - return fmt.Sprintf("%d-%s", ia.ISD(), as) + return fmt.Sprintf("%d-%s", ia.ISD(), as_) } // FormatISD formats the ISD number. +// @ trusted func FormatISD(isd ISD, opts ...FormatOption) string { o := applyFormatOptions(opts) if o.defaultPrefix { @@ -88,44 +95,61 @@ func FormatISD(isd ISD, opts ...FormatOption) string { } // FormatAS formats the AS number. -func FormatAS(as AS, opts ...FormatOption) string { +// @ trusted +func FormatAS(as_ AS, opts ...FormatOption) string { o := applyFormatOptions(opts) - s := fmtAS(as, o.separator) + s := fmtAS(as_, 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) +// @ requires as_.inRange() +// @ decreases +func fmtAS(as_ AS, sep string) string { + if !as_.inRange() { + return fmt.Sprintf("%d [Illegal AS: larger than %d]", as_, MaxAS) } - // Format BGP ASes as decimal - if as <= MaxBGPAS { - return strconv.FormatUint(uint64(as), 10) + // Format BGP ASes as_ decimal + if as_ <= MaxBGPAS { + // (VerifiedSCION) the following property is guaranteed by the type system, + // but Gobra cannot infer it yet + // @ assume 0 <= as_ + return strconv.FormatUint(uint64(as_), 10) } - // Format all other ASes as 'sep'-separated hex. - const maxLen = len("ffff:ffff:ffff") - var b strings.Builder + // Format all other ASes as_ 'sep'-separated hex. + // (VerifiedSCION) revert this change when Gobra is fixed. + // const maxLen = len("ffff:ffff:ffff") + 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)) + // (VerifiedSCION) the following property is guaranteed by the type system, + // but Gobra cannot infer it yet + // @ assume 0 <= uint64(as_>>shift)&asPartMask + b.WriteString(strconv.FormatUint(uint64(as_>>shift)&asPartMask, asPartBase)) } return b.String() } -type FormatOption func(*formatOptions) +// (VerifiedSCION) revert this change when Gobra is fixed. +// type FormatOption func(*formatOptions) +type FormatOption = func(*formatOptions) type formatOptions struct { defaultPrefix bool separator string } +// @ trusted func applyFormatOptions(opts []FormatOption) formatOptions { o := formatOptions{ defaultPrefix: false, @@ -139,6 +163,7 @@ 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 func WithDefaultPrefix() FormatOption { return func(o *formatOptions) { o.defaultPrefix = true @@ -147,6 +172,7 @@ func WithDefaultPrefix() FormatOption { // WithSeparator sets the separator to use for formatting AS numbers. In case of // the empty string, the ':' is used. +// @ trusted func WithSeparator(separator string) FormatOption { return func(o *formatOptions) { o.separator = separator @@ -154,6 +180,7 @@ func WithSeparator(separator string) FormatOption { } // WithFileSeparator returns an option that sets the separator to underscore. +// @ trusted func WithFileSeparator() FormatOption { return WithSeparator("_") } diff --git a/pkg/addr/fmt_spec.gobra b/pkg/addr/fmt_spec.gobra deleted file mode 100644 index a180f94e3..000000000 --- a/pkg/addr/fmt_spec.gobra +++ /dev/null @@ -1,21 +0,0 @@ -// Copyright 2022 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 - -requires _as.inRange() -decreases -func fmtAS(_as AS, sep string) string diff --git a/verification/dependencies/strings/builder.gobra b/verification/dependencies/strings/builder.gobra new file mode 100644 index 000000000..7f49895c8 --- /dev/null +++ b/verification/dependencies/strings/builder.gobra @@ -0,0 +1,46 @@ +// Copyright 2009 The Go Authors. All rights reserved. +// Use of this source code is governed by a BSD-style +// license that can be found in https://golang.org/LICENSE + +// Signatures for the public declarations in file +// https://github.com/golang/go/blob/master/src/strings/strings.go + +// +gobra + +package strings + +// 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 { + addr *Builder // of receiver, to detect copies by value + buf []byte +} + +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() +ensures err == nil +decreases _ +func (b *Builder) WriteString(s string) (n int, err error) + +requires b.Mem() +decreases _ +func (b *Builder) String() string + +ghost +requires acc(b) +requires *b === Builder{} +ensures b.Mem() +decreases _ +func (b *Builder) ZeroBuilderIsReadyToUse() \ No newline at end of file