diff --git a/src/main/resources/stubs/strconv/atoi.gobra b/src/main/resources/stubs/strconv/atoi.gobra index 454e456e0..c1876dab1 100644 --- a/src/main/resources/stubs/strconv/atoi.gobra +++ b/src/main/resources/stubs/strconv/atoi.gobra @@ -42,10 +42,11 @@ pure func (e *NumError) Unwrap() error { return e.Err } // a to the power of b ghost +requires base == 0 || (2 <= base && base <= 36) requires exp >= 0 ensures res == (exp == 0 ? 1 : (base * Exp(base, exp - 1))) decreases exp -pure func Exp(base int, exp int) (res int) { +pure func Exp(base uint64, exp int) (res uint64) { return exp == 0 ? 1 : (base * Exp(base, exp - 1)) } diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala index 1508987b0..c293ca32c 100644 --- a/src/main/scala/viper/gobra/frontend/Desugar.scala +++ b/src/main/scala/viper/gobra/frontend/Desugar.scala @@ -180,7 +180,7 @@ object Desugar extends LazyLogging { } } - private class Desugarer(pom: PositionManager, info: viper.gobra.frontend.info.TypeInfo, initSpecs: PackageInitSpecCollector) { + private class Desugarer(@unused pom: PositionManager, info: viper.gobra.frontend.info.TypeInfo, initSpecs: PackageInitSpecCollector) { type Meta = Source.Parser.Info diff --git a/src/main/scala/viper/gobra/frontend/info/base/Type.scala b/src/main/scala/viper/gobra/frontend/info/base/Type.scala index ee97ee787..5519680fb 100644 --- a/src/main/scala/viper/gobra/frontend/info/base/Type.scala +++ b/src/main/scala/viper/gobra/frontend/info/base/Type.scala @@ -41,8 +41,12 @@ object Type { case class IntT(kind: TypeBounds.IntegerKind) extends PrettyType(kind.name) - case object Float32T extends PrettyType("float32") - case object Float64T extends PrettyType("float64") + trait FloatT extends PrettyType + /** type for floating point numbers with unbounded precision */ + case object UnboundedFloatT extends PrettyType("unbounded float") with FloatT + trait TypedFloatT extends FloatT + case object Float32T extends PrettyType("float32") with TypedFloatT + case object Float64T extends PrettyType("float64") with TypedFloatT case class ArrayT(length: BigInt, elem: Type) extends PrettyType(s"[$length]$elem") { require(length >= 0, "The length of an array must be non-negative") diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala b/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala index 7d680dca7..46726f4b6 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala @@ -53,6 +53,7 @@ class TypeInfoImpl(final val tree: Info.GoTree, override final val dependentType with Assignability with Addressability with TypeIdentity + with Orderability with PointsTo with Executability with ConstantEvaluation diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/property/Assignability.scala b/src/main/scala/viper/gobra/frontend/info/implementation/property/Assignability.scala index 4bdc73c8c..0acecf1d5 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/property/Assignability.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/property/Assignability.scala @@ -110,6 +110,8 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl => case (UNTYPED_INT_CONST, r) if underlyingType(r).isInstanceOf[IntT] => successProp // not part of Go spec, but necessary for the definition of comparability case (l, UNTYPED_INT_CONST) if underlyingType(l).isInstanceOf[IntT] => successProp + case (UNTYPED_INT_CONST, r) if underlyingType(r).isInstanceOf[FloatT] => successProp + case (UnboundedFloatT, r) if underlyingType(r).isInstanceOf[FloatT] => successProp case (l, r) if identicalTypes(l, r) => successProp // the go language spec states that a value x of type V is assignable to a variable of type T // if V and T have identical underlying types and at least one of V or T is not a defined type diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/property/Convertibility.scala b/src/main/scala/viper/gobra/frontend/info/implementation/property/Convertibility.scala index 3a388b58c..abfc92359 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/property/Convertibility.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/property/Convertibility.scala @@ -6,7 +6,7 @@ package viper.gobra.frontend.info.implementation.property -import viper.gobra.frontend.info.base.Type.{ActualPointerT, DeclaredT, Float32T, Float64T, GhostPointerT, IntT, PermissionT, Single, SliceT, StringT, Type} +import viper.gobra.frontend.info.base.Type.{ActualPointerT, DeclaredT, Float32T, Float64T, FloatT, GhostPointerT, IntT, PermissionT, Single, SliceT, StringT, Type} import viper.gobra.frontend.info.implementation.TypeInfoImpl trait Convertibility extends BaseProperty { this: TypeInfoImpl => @@ -25,8 +25,7 @@ trait Convertibility extends BaseProperty { this: TypeInfoImpl => s"of this current package.") case (IntT(_), Float32T) => successProp case (IntT(_), Float64T) => successProp - case (Float32T, IntT(_)) => successProp - case (Float64T, IntT(_)) => successProp + case (_: FloatT, IntT(_)) => successProp case (IntT(_), IntT(_)) => successProp case (SliceT(IntT(config.typeBounds.Byte)), StringT) => successProp case (StringT, SliceT(IntT(config.typeBounds.Byte))) => successProp diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/property/Orderability.scala b/src/main/scala/viper/gobra/frontend/info/implementation/property/Orderability.scala new file mode 100644 index 000000000..ad3deb451 --- /dev/null +++ b/src/main/scala/viper/gobra/frontend/info/implementation/property/Orderability.scala @@ -0,0 +1,24 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. +// +// Copyright (c) 2011-2025 ETH Zurich. + +package viper.gobra.frontend.info.implementation.property + +import viper.gobra.frontend.info.base.Type._ +import viper.gobra.frontend.info.implementation.TypeInfoImpl + +trait Orderability extends BaseProperty { this: TypeInfoImpl => + + lazy val orderedType: Property[Type] = createBinaryProperty("ordered") { + case Single(st) => underlyingType(st) match { + case _: IntT => true + case PermissionT => true + case _: FloatT => true + case StringT => true + case _ => false + } + case _ => false + } +} diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/property/TypeMerging.scala b/src/main/scala/viper/gobra/frontend/info/implementation/property/TypeMerging.scala index 5edaae0ec..aa5d36d41 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/property/TypeMerging.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/property/TypeMerging.scala @@ -6,8 +6,7 @@ package viper.gobra.frontend.info.implementation.property -import viper.gobra.ast.internal.{Float32T, Float64T} -import viper.gobra.frontend.info.base.Type.{ActualPointerT, ArrayT, AssertionT, BooleanT, ChannelT, GhostPointerT, GhostSliceT, IntT, InternalTupleT, MapT, MultisetT, PermissionT, SequenceT, SetT, Single, SliceT, Type} +import viper.gobra.frontend.info.base.Type.{ActualPointerT, ArrayT, AssertionT, BooleanT, ChannelT, FloatT, GhostPointerT, GhostSliceT, IntT, InternalTupleT, MapT, MultisetT, PermissionT, SequenceT, SetT, Single, SliceT, Type, UnboundedFloatT} import viper.gobra.frontend.info.implementation.TypeInfoImpl trait TypeMerging extends BaseProperty { this: TypeInfoImpl => @@ -27,10 +26,10 @@ trait TypeMerging extends BaseProperty { this: TypeInfoImpl => case (a, UNTYPED_INT_CONST) if underlyingType(a).isInstanceOf[IntT] => Some(a) case (UNTYPED_INT_CONST, b) if underlyingType(b).isInstanceOf[IntT] => Some(b) - case (a, UNTYPED_INT_CONST) if underlyingType(a).isInstanceOf[Float64T] => Some(a) - case (UNTYPED_INT_CONST, b) if underlyingType(b).isInstanceOf[Float64T] => Some(b) - case (a, UNTYPED_INT_CONST) if underlyingType(a).isInstanceOf[Float32T] => Some(a) - case (UNTYPED_INT_CONST, b) if underlyingType(b).isInstanceOf[Float32T] => Some(b) + case (a, UNTYPED_INT_CONST) if underlyingType(a).isInstanceOf[FloatT] => Some(a) + case (UNTYPED_INT_CONST, b) if underlyingType(b).isInstanceOf[FloatT] => Some(b) + case (a, UnboundedFloatT) if underlyingType(a).isInstanceOf[FloatT] => Some(a) + case (UnboundedFloatT, b) if underlyingType(b).isInstanceOf[FloatT] => Some(b) case (BooleanT, AssertionT) => Some(AssertionT) case (AssertionT, BooleanT) => Some(AssertionT) case (IntT(_), PermissionT) => Some(PermissionT) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala index 91b45173c..7f83e1ce8 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala @@ -10,12 +10,14 @@ import org.bitbucket.inkytonik.kiama.util.Message import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, check, error, noMessages} import viper.gobra.ast.frontend.{AstPattern => ap, _} import viper.gobra.frontend.info.base.SymbolTable.{AdtDestructor, AdtDiscriminator, GlobalVariable, SingleConstant} -import viper.gobra.frontend.info.base.Type._ +import viper.gobra.frontend.info.base.Type.{StringT, _} import viper.gobra.frontend.info.base.{SymbolTable => st} import viper.gobra.frontend.info.implementation.TypeInfoImpl import viper.gobra.util.TypeBounds.{BoundedIntegerKind, UnboundedInteger} import viper.gobra.util.{Constants, TypeBounds, Violation} +import scala.annotation.nowarn + trait ExprTyping extends BaseTyping { this: TypeInfoImpl => import viper.gobra.util.Violation._ @@ -222,7 +224,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => case n: PIota => error(n, s"cannot use iota outside of constant declaration", enclosingPConstDecl(n).isEmpty) - case _: PFloatLit => ??? + case n: PFloatLit => error(n, s"floating point literals are not yet supported.") case n@PCompositeLit(t, lit) => val mayInit = isEnclosingMayInit(n) @@ -477,22 +479,30 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => case n: PBinaryExp[_,_] => val mayInit = isEnclosingMayInit(n) (n, exprOrTypeType(n.left), exprOrTypeType(n.right)) match { - case (_: PEquals | _: PUnequals, l, r) => comparableTypes.errors(l, r)(n) - case (_: PAnd | _: POr, l, r) => assignableTo.errors(l, AssertionT, mayInit)(n.left) ++ - assignableTo.errors(r, AssertionT, mayInit)(n.right) - case (_: PLess | _: PAtMost | _: PGreater | _: PAtLeast, l, r) => (l,r) match { - case (StringT, StringT) => noMessages - case (Float32T, Float32T) => noMessages - case (Float64T, Float64T) => noMessages - case _ if l == PermissionT || r == PermissionT => - assignableTo.errors(l, PermissionT, mayInit)(n.left) ++ - assignableTo.errors(r, PermissionT, mayInit)(n.right) - case _ => - assignableTo.errors(l, UNTYPED_INT_CONST, mayInit)(n.left) ++ - assignableTo.errors(r, UNTYPED_INT_CONST, mayInit)(n.right) - } + case (_: PEquals | _: PUnequals | _: PLess | _: PAtMost | _: PGreater | _: PAtLeast | _: PAnd | _: POr, l, r) => + // from the spec: "first operand must be assignable to the type of the second operand, or vice versa" + val fstAssignable = assignableTo.errors(l, r, mayInit)(n) + val sndAssignable = assignableTo.errors(r, l, mayInit)(n) + val assignable = if (fstAssignable.isEmpty || sndAssignable.isEmpty) noMessages + else error(n, s"neither operand is assignable to the type of the other operand") + @nowarn("msg=not.*?exhaustive") + val applicable = if (assignable.isEmpty) { + n match { + case _: PEquals | _: PUnequals => + // from the spec: "The equality operators == and != apply to operands of comparable types" + comparableTypes.errors(l, r)(n) + case _: PLess | _: PAtMost | _: PGreater | _: PAtLeast => + // from the spec: "The ordering operators <, <=, >, and >= apply to operands of ordered types" + orderedType.errors(l)(n.left) ++ orderedType.errors(r)(n.right) + case _: PAnd | _: POr => + // from the spec: "Logical operators apply to boolean values", which we extend from boolean to assertion values: + assignableTo.errors(l, AssertionT, mayInit)(n.left) ++ + assignableTo.errors(r, AssertionT, mayInit)(n.right) + } + } else noMessages + assignable ++ applicable case (_: PAdd, StringT, StringT) => noMessages - case (_: PAdd | _: PSub | _: PMul | _: PDiv, l, r) if Set(l, r).intersect(Set(Float32T, Float64T)).nonEmpty => + case (_: PAdd | _: PSub | _: PMul | _: PDiv, l, r) if Set(l, r).intersect(Set(UnboundedFloatT, Float32T, Float64T)).nonEmpty => mergeableTypes.errors(l, r)(n) case (_: PAdd | _: PSub | _: PMul | _: PMod | _: PDiv, l, r) if l == PermissionT || r == PermissionT || getTypeFromCtxt(n).contains(PermissionT) => @@ -680,7 +690,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => } private def numExprWithinTypeBounds(num: PNumExpression): Messages = - intExprWithinTypeBounds(num, intExprType(num)) + intExprWithinTypeBounds(num, numExprType(num)) private def intExprWithinTypeBounds(exp: PExpression, typ: Type): Messages = { if (typ == UNTYPED_INT_CONST) { @@ -711,6 +721,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => case _: PBoolLit => BooleanT case _: PNilLit => NilType case _: PStringLit => StringT + case _: PFloatLit => UnboundedFloatT case cl: PCompositeLit => expectedCompositeLitType(cl) @@ -797,7 +808,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => case _: PCapacity => INT_TYPE case exprNum: PNumExpression => - val typ = intExprType(exprNum) + val typ = numExprType(exprNum) if (typ == UNTYPED_INT_CONST) getNonInterfaceTypeFromCtxt(exprNum).getOrElse(typ) else typ case n: PUnfolding => exprType(n.op) @@ -1058,10 +1069,12 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => case _ => violation("blank identifier always has a parent") } - private def intExprType(expr: PNumExpression): Type = { + private def numExprType(expr: PNumExpression): Type = { val typ = expr match { case _: PIntLit => UNTYPED_INT_CONST + case _: PFloatLit => UnboundedFloatT + case e: PLength => typeOfPLength(e) case _: PCapacity => INT_TYPE diff --git a/src/test/resources/regressions/features/integers/int-assign-fail2.gobra b/src/test/resources/regressions/features/integers/int-assign-fail2.gobra new file mode 100644 index 000000000..915737992 --- /dev/null +++ b/src/test/resources/regressions/features/integers/int-assign-fail2.gobra @@ -0,0 +1,22 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package ints + +func test1() { + var j uint16 + for i := 0; i < 256; i++ { + //:: ExpectedOutput(type_error) + if i < j { // Go compiler reports "invalid operation: i < j (mismatched types int and uint16)" + j = 42 + } + } +} + +func test2() { + invariant 0 <= i && i <= 256 + //:: ExpectedOutput(type_error) + invariant forall j uint16 :: 0 <= j && j < i ==> true + decreases 256 - i + for i := 0; i < 256; i++ {} +} diff --git a/src/test/resources/regressions/issues/000783-1.gobra b/src/test/resources/regressions/issues/000783-1.gobra new file mode 100644 index 000000000..5067913f3 --- /dev/null +++ b/src/test/resources/regressions/issues/000783-1.gobra @@ -0,0 +1,13 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package issue783_1 + +//:: ExpectedOutput(type_error) +requires x > 0.0 +//:: ExpectedOutput(type_error) +ensures res > 0.0 +ensures false +func newton(x float32, y float32) (res float32) { + return x/2 + y / 2 / x +} diff --git a/src/test/resources/regressions/issues/000783-2.gobra b/src/test/resources/regressions/issues/000783-2.gobra new file mode 100644 index 000000000..8adf0da8b --- /dev/null +++ b/src/test/resources/regressions/issues/000783-2.gobra @@ -0,0 +1,10 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package issue783_2 + +func main() { + //:: ExpectedOutput(type_error) + assert 1e2 > 0 + assert false +} diff --git a/src/test/resources/regressions/issues/000783-3.gobra b/src/test/resources/regressions/issues/000783-3.gobra new file mode 100644 index 000000000..55998358e --- /dev/null +++ b/src/test/resources/regressions/issues/000783-3.gobra @@ -0,0 +1,10 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package issue783_3 + +ensures false +func floatfn3(f float64) float64 { + //:: ExpectedOutput(type_error) + return 0.0 +} diff --git a/src/test/resources/same_package/pkg_init/byte/byte.go b/src/test/resources/same_package/pkg_init/byte/byte.go index 7866c5411..fec46b17a 100644 --- a/src/test/resources/same_package/pkg_init/byte/byte.go +++ b/src/test/resources/same_package/pkg_init/byte/byte.go @@ -13,9 +13,9 @@ var byteCache /*@@@*/ [256]*Byte func init() { // @ invariant 0 <= i && i <= 256 && acc(&byteCache) - // @ invariant (forall j, k uint16 :: 0 <= j && j < k && k < i ==> + // @ invariant (forall j, k int :: 0 <= j && j < k && k < i ==> // @ byteCache[j] != byteCache[k]) - // @ invariant (forall j uint16 :: 0 <= j && j < i ==> + // @ invariant (forall j int :: 0 <= j && j < i ==> // @ acc(byteCache[j]) && byteCache[j].value == byte(j) - 128) // @ decreases 256 - i for i := 0; i < 256; i++ {