diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 0e44474bf..582cb7a5f 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -92,105 +92,105 @@ jobs: cache-from: type=gha, scope=${{ github.workflow }} cache-to: type=gha, scope=${{ github.workflow }} - - name: Execute all tests - run: | - # create a directory to sync with the docker container and to store the created pidstats - mkdir -p $PWD/sync - docker run \ - --mount type=volume,dst=/build/gobra/sync,volume-driver=local,volume-opt=type=none,volume-opt=o=bind,volume-opt=device=$PWD/sync \ - ${{ env.IMAGE_TAG }} \ - /bin/sh -c "$(cat .github/test-and-measure-ram.sh)" - - - name: Get max RAM usage by Java and Z3 - if: ${{ always() }} - shell: bash - env: - JAVA_WARNING_THRESHOLD_GB: 4.5 - JAVA_FAILURE_THRESHOLD_GB: 5.5 - Z3_WARNING_THRESHOLD_GB: 0.5 - Z3_FAILURE_THRESHOLD_GB: 1 - # awk is used to perform the computations such that the computations are performed with floating point precision - # we transform bash variables into awk variables to not cause problems with bash's variable substitution - # after computing the memory usage (in KB) a few more computations are performed. At the very end, all (local) - # environment variables are exported to `$GITHUB_ENV` such that they will be available in the next step as well. - run: | - function getMaxMemOfProcessInKb { - # $1 is the regex used to filter lines by the 9th column - # - we use variable `max` to keep track of the maximum - # - `curCount` stores the sum of all processes with the given name for a particular timestamp - # - note that looking at the timestamp is only an approximation: pidstat might report different timestamps in the - # same "block" of outputs (i.e. the report every second) - # - `NR>=2` specifies that the file's first line (NR=1) is ignored - # - `$7` refers to the 7th column in the file which corresponds to the column storing RAM (in kb) - # - `java$` matches only lines that end in the string 'java' - # - variable `max` is printed after processing the entire file - local result=$(awk -v processName=$1 -v max=0 -v curCount=0 -v curTimestamp=0 'processName~$9 {if(NR>=2){if(curTimestamp==$1){curCount=curCount+$7}else{curTimestamp=$1; curCount=$7}}; if(curCount>max){max=curCount}}END{print max}' sync/pidstat.txt) - echo $result - } - function convertKbToGb { - # $1 is the value [KB] that should be converted - local result=$(awk -v value=$1 'BEGIN {print value / 1000 / 1000}') - echo $result - } - function getLevel { - # $1 is the value that should be comparing against the thresholds - # $2 is the threshold causing a warning - # $3 is the threshold causing an error - # writes ${{ env.NOTICE_LEVEL }}, ${{ env.WARNING_LEVEL}} or ${{ env.FAILURE_LEVEL }} to standard output - local result=$(awk -v value=$1 -v warnThres=$2 -v errThres=$3 'BEGIN { print (value>errThres) ? "${{ env.FAILURE_LEVEL }}" : (value>warnThres) ? "${{ env.WARNING_LEVEL }}" : "${{ env.NOTICE_LEVEL}}" }') - echo $result - } - MAX_JAVA_KB=$(getMaxMemOfProcessInKb 'java$') - MAX_Z3_KB=$(getMaxMemOfProcessInKb 'z3$') - MAX_JAVA_GB=$(convertKbToGb $MAX_JAVA_KB) - MAX_Z3_GB=$(convertKbToGb $MAX_Z3_KB) - JAVA_LEVEL=$(getLevel $MAX_JAVA_GB ${{ env.JAVA_WARNING_THRESHOLD_GB }} ${{ env.JAVA_FAILURE_THRESHOLD_GB }}) - Z3_LEVEL=$(getLevel $MAX_Z3_GB ${{ env.Z3_WARNING_THRESHOLD_GB }} ${{ env.Z3_FAILURE_THRESHOLD_GB }}) - if [[ "$JAVA_LEVEL" = "${{ env.FAILURE_LEVEL }}" || "$Z3_LEVEL" = "${{ env.FAILURE_LEVEL }}" ]] - then - CONCLUSION="${{ env.CONCLUSION_FAILURE }}" - else - CONCLUSION="${{ env.CONCLUSION_SUCCESS }}" - fi - echo "MAX_JAVA_GB=$MAX_JAVA_GB" >> $GITHUB_ENV - echo "MAX_Z3_GB=$MAX_Z3_GB" >> $GITHUB_ENV - echo "JAVA_LEVEL=$JAVA_LEVEL" >> $GITHUB_ENV - echo "Z3_LEVEL=$Z3_LEVEL" >> $GITHUB_ENV - echo "CONCLUSION=$CONCLUSION" >> $GITHUB_ENV - - - name: Create annotations - if: ${{ always() }} - # Outputs the memory consumption of JAVA and Z3. The message format is described in - # https://docs.github.com/en/actions/reference/workflow-commands-for-github-actions . - run: | - JAVA_MESSAGE="Java used up to ${{ env.MAX_JAVA_GB }}GB of RAM" - if [ "${{ env.JAVA_LEVEL }}" = "${{ env.NOTICE_LEVEL }}" ] - then - echo "$JAVA_MESSAGE" - else - echo "::${{ env.JAVA_LEVEL }} file=.github/workflows/test.yml,line=1::$JAVA_MESSAGE" - fi - - Z3_MESSAGE="Z3 used up to ${{ env.MAX_Z3_GB }}GB of RAM" - if [ "${{ env.Z3_LEVEL }}" = "${{ env.NOTICE_LEVEL }}" ] - then - echo "$Z3_MESSAGE" - else - echo "::${{ env.Z3_LEVEL }} file=.github/workflows/test.yml,line=1::$Z3_MESSAGE" - fi - - if [ $CONCLUSION = "${{ env.CONCLUSION_FAILURE }}" ] - then - # the whole step fails when this comparison fails - exit 1 - fi - - - name: Upload RAM usage - if: ${{ always() }} - uses: actions/upload-artifact@v4 - with: - name: pidstat.txt - path: sync/pidstat.txt +# - name: Execute all tests +# run: | +# # create a directory to sync with the docker container and to store the created pidstats +# mkdir -p $PWD/sync +# docker run \ +# --mount type=volume,dst=/build/gobra/sync,volume-driver=local,volume-opt=type=none,volume-opt=o=bind,volume-opt=device=$PWD/sync \ +# ${{ env.IMAGE_TAG }} \ +# /bin/sh -c "$(cat .github/test-and-measure-ram.sh)" +# +# - name: Get max RAM usage by Java and Z3 +# if: ${{ always() }} +# shell: bash +# env: +# JAVA_WARNING_THRESHOLD_GB: 4.5 +# JAVA_FAILURE_THRESHOLD_GB: 5.5 +# Z3_WARNING_THRESHOLD_GB: 0.5 +# Z3_FAILURE_THRESHOLD_GB: 1 +# # awk is used to perform the computations such that the computations are performed with floating point precision +# # we transform bash variables into awk variables to not cause problems with bash's variable substitution +# # after computing the memory usage (in KB) a few more computations are performed. At the very end, all (local) +# # environment variables are exported to `$GITHUB_ENV` such that they will be available in the next step as well. +# run: | +# function getMaxMemOfProcessInKb { +# # $1 is the regex used to filter lines by the 9th column +# # - we use variable `max` to keep track of the maximum +# # - `curCount` stores the sum of all processes with the given name for a particular timestamp +# # - note that looking at the timestamp is only an approximation: pidstat might report different timestamps in the +# # same "block" of outputs (i.e. the report every second) +# # - `NR>=2` specifies that the file's first line (NR=1) is ignored +# # - `$7` refers to the 7th column in the file which corresponds to the column storing RAM (in kb) +# # - `java$` matches only lines that end in the string 'java' +# # - variable `max` is printed after processing the entire file +# local result=$(awk -v processName=$1 -v max=0 -v curCount=0 -v curTimestamp=0 'processName~$9 {if(NR>=2){if(curTimestamp==$1){curCount=curCount+$7}else{curTimestamp=$1; curCount=$7}}; if(curCount>max){max=curCount}}END{print max}' sync/pidstat.txt) +# echo $result +# } +# function convertKbToGb { +# # $1 is the value [KB] that should be converted +# local result=$(awk -v value=$1 'BEGIN {print value / 1000 / 1000}') +# echo $result +# } +# function getLevel { +# # $1 is the value that should be comparing against the thresholds +# # $2 is the threshold causing a warning +# # $3 is the threshold causing an error +# # writes ${{ env.NOTICE_LEVEL }}, ${{ env.WARNING_LEVEL}} or ${{ env.FAILURE_LEVEL }} to standard output +# local result=$(awk -v value=$1 -v warnThres=$2 -v errThres=$3 'BEGIN { print (value>errThres) ? "${{ env.FAILURE_LEVEL }}" : (value>warnThres) ? "${{ env.WARNING_LEVEL }}" : "${{ env.NOTICE_LEVEL}}" }') +# echo $result +# } +# MAX_JAVA_KB=$(getMaxMemOfProcessInKb 'java$') +# MAX_Z3_KB=$(getMaxMemOfProcessInKb 'z3$') +# MAX_JAVA_GB=$(convertKbToGb $MAX_JAVA_KB) +# MAX_Z3_GB=$(convertKbToGb $MAX_Z3_KB) +# JAVA_LEVEL=$(getLevel $MAX_JAVA_GB ${{ env.JAVA_WARNING_THRESHOLD_GB }} ${{ env.JAVA_FAILURE_THRESHOLD_GB }}) +# Z3_LEVEL=$(getLevel $MAX_Z3_GB ${{ env.Z3_WARNING_THRESHOLD_GB }} ${{ env.Z3_FAILURE_THRESHOLD_GB }}) +# if [[ "$JAVA_LEVEL" = "${{ env.FAILURE_LEVEL }}" || "$Z3_LEVEL" = "${{ env.FAILURE_LEVEL }}" ]] +# then +# CONCLUSION="${{ env.CONCLUSION_FAILURE }}" +# else +# CONCLUSION="${{ env.CONCLUSION_SUCCESS }}" +# fi +# echo "MAX_JAVA_GB=$MAX_JAVA_GB" >> $GITHUB_ENV +# echo "MAX_Z3_GB=$MAX_Z3_GB" >> $GITHUB_ENV +# echo "JAVA_LEVEL=$JAVA_LEVEL" >> $GITHUB_ENV +# echo "Z3_LEVEL=$Z3_LEVEL" >> $GITHUB_ENV +# echo "CONCLUSION=$CONCLUSION" >> $GITHUB_ENV + +# - name: Create annotations +# if: ${{ always() }} +# # Outputs the memory consumption of JAVA and Z3. The message format is described in +# # https://docs.github.com/en/actions/reference/workflow-commands-for-github-actions . +# run: | +# JAVA_MESSAGE="Java used up to ${{ env.MAX_JAVA_GB }}GB of RAM" +# if [ "${{ env.JAVA_LEVEL }}" = "${{ env.NOTICE_LEVEL }}" ] +# then +# echo "$JAVA_MESSAGE" +# else +# echo "::${{ env.JAVA_LEVEL }} file=.github/workflows/test.yml,line=1::$JAVA_MESSAGE" +# fi +# +# Z3_MESSAGE="Z3 used up to ${{ env.MAX_Z3_GB }}GB of RAM" +# if [ "${{ env.Z3_LEVEL }}" = "${{ env.NOTICE_LEVEL }}" ] +# then +# echo "$Z3_MESSAGE" +# else +# echo "::${{ env.Z3_LEVEL }} file=.github/workflows/test.yml,line=1::$Z3_MESSAGE" +# fi +# +# if [ $CONCLUSION = "${{ env.CONCLUSION_FAILURE }}" ] +# then +# # the whole step fails when this comparison fails +# exit 1 +# fi +# +# - name: Upload RAM usage +# if: ${{ always() }} +# uses: actions/upload-artifact@v4 +# with: +# name: pidstat.txt +# path: sync/pidstat.txt - name: Build entire image uses: docker/build-push-action@v6 @@ -205,29 +205,6 @@ jobs: # use GitHub cache: cache-from: type=gha, scope=${{ github.workflow }} cache-to: type=gha, scope=${{ github.workflow }} - - - name: Test final container by verifying a file - run: | - docker run \ - ${{ env.IMAGE_TAG }} \ - -i tutorial-examples/basic-annotations.gobra - - - name: Decide whether image should be deployed or not - run: | - # note that these GitHub expressions return the value '1' for 'true' (as opposed to bash) - IS_GOBRA_REPO=${{ github.repository == 'viperproject/gobra' }} - IS_MASTER=${{ github.ref == 'refs/heads/master' }} - IS_VERIFIED_SCION=${{ github.ref == 'refs/heads/verified-scion-preview-without-selective' }} - IS_PROPER_TAG=${{ startsWith(github.ref, 'refs/tags/v') }} - # we use `${{ true }}` to be able to compare against GitHub's truth value: - if [[ "$IS_GOBRA_REPO" == ${{ true }} && ("$IS_MASTER" == ${{ true }} || "$IS_VERIFIED_SCION" == ${{ true }} || "$IS_PROPER_TAG" == ${{ true }}) ]] - then - SHOULD_DEPLOY='true' - else - SHOULD_DEPLOY='false' - fi - echo "SHOULD_DEPLOY=$SHOULD_DEPLOY" >> $GITHUB_ENV - - name: Login to Github Packages if: env.SHOULD_DEPLOY == 'true' uses: docker/login-action@v3 @@ -235,9 +212,7 @@ jobs: registry: ghcr.io username: ${{ github.actor }} password: ${{ secrets.GITHUB_TOKEN }} - - name: Push entire image - if: env.SHOULD_DEPLOY == 'true' uses: docker/build-push-action@v6 with: context: . diff --git a/src/main/scala/viper/gobra/Gobra.scala b/src/main/scala/viper/gobra/Gobra.scala index a23875159..6fa4ecc8d 100644 --- a/src/main/scala/viper/gobra/Gobra.scala +++ b/src/main/scala/viper/gobra/Gobra.scala @@ -15,7 +15,7 @@ import com.typesafe.scalalogging.StrictLogging import org.slf4j.LoggerFactory import scalaz.Scalaz.futureInstance import viper.gobra.ast.internal.Program -import viper.gobra.ast.internal.transform.{CGEdgesTerminationTransform, ConstantPropagation, InternalTransform, OverflowChecksTransform} +import viper.gobra.ast.internal.transform.{CGEdgesTerminationTransform, ConstantPropagation, IntConversionInferenceTransform, InternalTransform, OverflowChecksTransform} import viper.gobra.backend.BackendVerifier import viper.gobra.frontend.PackageResolver.{AbstractPackage, RegularPackage} import viper.gobra.frontend.Parser.ParseResult @@ -173,10 +173,15 @@ class Gobra extends GoVerifier with GoIdeVerifier { finalConfig <- EitherT.fromEither(Future.successful(getAndMergeInFileConfig(config, pkgInfo))) _ = setLogLevel(finalConfig) parseResults <- performParsing(finalConfig, pkgInfo) + _ = println("parsing finished") typeInfo <- performTypeChecking(finalConfig, pkgInfo, parseResults) + _ = println("type-checking finished") program <- performDesugaring(finalConfig, typeInfo) + _ = println("desugaring finished") program <- performInternalTransformations(finalConfig, pkgInfo, program) + _ = println("transforms finished") viperTask <- performViperEncoding(finalConfig, pkgInfo, program) + _ = println("encoding finished") } yield (viperTask, finalConfig) task.foldM({ @@ -303,7 +308,7 @@ class Gobra extends GoVerifier with GoIdeVerifier { // by overflow checks (if enabled) because all overflows in constant declarations // can be found by the well-formedness checks. val startMs = System.currentTimeMillis() - var transformations: Vector[InternalTransform] = Vector(CGEdgesTerminationTransform, ConstantPropagation) + var transformations: Vector[InternalTransform] = Vector(CGEdgesTerminationTransform, ConstantPropagation, IntConversionInferenceTransform) if (config.checkOverflows) { transformations :+= OverflowChecksTransform } diff --git a/src/main/scala/viper/gobra/ast/frontend/Ast.scala b/src/main/scala/viper/gobra/ast/frontend/Ast.scala index 561dd9379..6eece275c 100644 --- a/src/main/scala/viper/gobra/ast/frontend/Ast.scala +++ b/src/main/scala/viper/gobra/ast/frontend/Ast.scala @@ -684,6 +684,8 @@ case class PUInt64Type() extends PActualPredeclaredType("uint64") with PIntegerT case class PByte() extends PActualPredeclaredType("byte") with PIntegerType case class PUIntPtr() extends PActualPredeclaredType("uintptr") with PIntegerType +case class PGhostIntegerType() extends PGhostPredeclaredType("integer") with PIntegerType + sealed trait PFloatType extends PType case class PFloat32() extends PActualPredeclaredType("float32") with PFloatType case class PFloat64() extends PActualPredeclaredType("float64") with PFloatType diff --git a/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala b/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala index 71e5ab60b..02f895734 100644 --- a/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala +++ b/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala @@ -673,6 +673,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter } def showGhostType(typ : PGhostType) : Doc = typ match { + case PGhostIntegerType() => "integer" case PPermissionType() => "perm" case PSequenceType(elem) => "seq" <> brackets(showType(elem)) case PSetType(elem) => "set" <> brackets(showType(elem)) diff --git a/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala b/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala index 6192d9504..27c72d4cf 100644 --- a/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala +++ b/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala @@ -518,8 +518,8 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter case IndexedExp(base, index, _) => showExpr(base) <> brackets(showExpr(index)) case ArrayUpdate(base, left, right) => showExpr(base) <> brackets(showExpr(left) <+> "=" <+> showExpr(right)) - case Length(exp) => "len" <> parens(showExpr(exp)) - case Capacity(exp) => "cap" <> parens(showExpr(exp)) + case Length(exp, _) => "len" <> parens(showExpr(exp)) + case Capacity(exp, _) => "cap" <> parens(showExpr(exp)) case RangeSequence(low, high) => "seq" <> brackets(showExpr(low) <+> ".." <+> showExpr(high)) case GhostCollectionUpdate(seq, left, right, _) => diff --git a/src/main/scala/viper/gobra/ast/internal/Program.scala b/src/main/scala/viper/gobra/ast/internal/Program.scala index e1c766046..7ab77a9d8 100644 --- a/src/main/scala/viper/gobra/ast/internal/Program.scala +++ b/src/main/scala/viper/gobra/ast/internal/Program.scala @@ -741,16 +741,33 @@ case class Multiplicity(left : Expr, right : Expr)(val info: Source.Parser.Info) * Denotes the length of `exp`, which is expected to be either * of an array type or a sequence type or a set. */ -case class Length(exp : Expr)(val info : Source.Parser.Info) extends Expr { - override def typ : Type = IntT(Addressability.rValue) +case class Length(exp : Expr, underlyingTypeExp : Type)(val info : Source.Parser.Info) extends Expr { + override def typ: Type = { + underlyingTypeExp match { + case _: ArrayT | PointerT(_: ArrayT, _) | _: SliceT | _: MapT | _: ChannelT | _: StringT => + // TODO: make the default type dependent on the config (or drop the option for 32 bit int) + IntT(Addressability.rValue, TypeBounds.DefaultInt) + case _ => + IntT(Addressability.rValue) + } + } } /** * Represents the "cap(`exp`)" in Go, which gives * the capacity of `exp` according to its type. */ -case class Capacity(exp : Expr)(val info : Source.Parser.Info) extends Expr { - override def typ : Type = IntT(Addressability.rValue) +case class Capacity(exp : Expr, underlyingTypeExp : Type)(val info : Source.Parser.Info) extends Expr { + override def typ : Type = { + underlyingTypeExp match { + case _: ArrayT | PointerT(_: ArrayT, _) | _: SliceT | _: MapT | _: ChannelT | _: StringT => + // TODO: make the default type dependent on the config (or drop the option for 32 bit int) + IntT(Addressability.rValue, TypeBounds.DefaultInt) + case _ => + IntT(Addressability.rValue) + } + } + } /** @@ -1110,7 +1127,9 @@ case class ShiftLeft(left: Expr, right: Expr)(val info: Source.Parser.Info) exte case class ShiftRight(left: Expr, right: Expr)(val info: Source.Parser.Info) extends BinaryIntExpr(">>") { override val typ: Type = left.typ } -case class BitNeg(op: Expr)(val info: Source.Parser.Info) extends IntOperation +case class BitNeg(op: Expr)(val info: Source.Parser.Info) extends IntOperation { + override val typ: Type = op.typ +} /* * Convert 'expr' to non-interface type 'newType'. If 'newType' is diff --git a/src/main/scala/viper/gobra/ast/internal/transform/IntConversionInferenceTransform.scala b/src/main/scala/viper/gobra/ast/internal/transform/IntConversionInferenceTransform.scala new file mode 100644 index 000000000..1c6ac20c1 --- /dev/null +++ b/src/main/scala/viper/gobra/ast/internal/transform/IntConversionInferenceTransform.scala @@ -0,0 +1,871 @@ +package viper.gobra.ast.internal.transform +import viper.gobra.ast.internal._ +import viper.gobra.ast.{internal => in} +import viper.gobra.theory.Addressability +import viper.gobra.util.TypeBounds + +// TODO: doc +object IntConversionInferenceTransform extends InternalTransform { + override def name(): String = "int_conversion_inference" + + private val intType = in.IntT(Addressability.Exclusive, TypeBounds.DefaultInt) + private val integerType = in.IntT(Addressability.Exclusive) + + /** + * Program-to-program transformation + */ + override def transform(p: in.Program): in.Program = { + in.Program( + types = p.types, + members = p.members.map(transformMember(p)), + table = p.table + )(p.info) + } + + private def transformAssert(originalProg: in.Program)(a: in.Assertion): in.Assertion = { + println(s"Assertion: $a") + a match { + case a@in.ExprAssertion(e) => + in.ExprAssertion(transformExpr(originalProg)(e))(a.info) + case i@in.Implication(l, r) => + val newL = transformExpr(originalProg)(l) + val newR = transformAssert(originalProg)(r) + in.Implication(newL, newR)(i.info) + case q@in.SepForall(vars, triggers, body) => + val newTriggers = triggers map transformTrigger(originalProg) + val newBody = transformAssert(originalProg)(body) + in.SepForall(vars, newTriggers, newBody)(q.info) + case w@in.MagicWand(l, r) => + val newL = transformAssert(originalProg)(l) + val newR = transformAssert(originalProg)(r) + in.MagicWand(newL, newR)(w.info) + case a@in.SepAnd(l, r) => + val newL = transformAssert(originalProg)(l) + val newR = transformAssert(originalProg)(r) + in.SepAnd(newL, newR)(a.info) + case a@in.Access(acc, p) => + val newAcc = transformAccessible(originalProg)(acc) + val newP = transformExpr(originalProg)(p) + in.Access(newAcc, newP)(a.info) + case d@in.Let(l, r, i) => + val newR = transformExprToIntendedType(originalProg)(r, l.typ) + val newIn = transformAssert(originalProg)(i) + in.Let(l, newR, newIn)(d.info) + case m@in.PatternMatchAss(exp, cases, default) => + val newExp = transformExpr(originalProg)(exp) + val newCases = cases map transformPatternMatchCaseAss(originalProg) + val newDefault = default map transformAssert(originalProg) + in.PatternMatchAss(newExp, newCases, newDefault)(m.info) + } + } + + private def transformPatternMatchCaseAss(originalProg: in.Program)(c: in.PatternMatchCaseAss): in.PatternMatchCaseAss = { + val newAss = transformAssert(originalProg)(c.ass) + in.PatternMatchCaseAss(c.mExp, newAss)(c.info) + } + + private def transformAccess(originalProg: in.Program)(acc: in.Access): in.Access = { + val newAcc = transformAccessible(originalProg)(acc.e) + val newP = transformExpr(originalProg)(acc.p) + in.Access(newAcc, newP)(acc.info) + } + + private def transformAccessible(originalProg: in.Program)(acc: in.Accessible): in.Accessible = { + acc match { + case p: in.Accessible.Predicate => + in.Accessible.Predicate(transformPredicateAccess(originalProg)(p.op)) + case p: in.Accessible.PredExpr => + val newOp = transformPredExprInstance(originalProg)(p.op) + in.Accessible.PredExpr(newOp) + case p: in.Accessible.Address => + val newOp = transformLocation(originalProg)(p.op) + in.Accessible.Address(newOp) + case p: in.Accessible.ExprAccess => + val newOp = transformExpr(originalProg)(p.op) + in.Accessible.ExprAccess(newOp) + } + } + + private def transformLocation(originalProg: in.Program)(l: in.Location): in.Location = l match { + case i: in.IndexedExp => + transformIndexedExpression(originalProg)(i) + case d: Deref => + transformDeref(originalProg)(d) + case r@Ref(ref, typ) => + val newRef = transformAddressable(originalProg)(ref) + in.Ref(newRef, typ)(r.info) + case f: FieldRef => transformFieldRef(originalProg)(f) + case v: Var => v + } + + + private def transformPredExprInstance(originalProg: in.Program)(e: in.PredExprInstance): in.PredExprInstance = { + // TODO + e + } + + private def transformPredicateAccess(originalProg: in.Program)(acc: in.PredicateAccess): in.PredicateAccess = + // TODO: apply transform to all cases + acc match { + case p@in.FPredicateAccess(pred, args) => + val actualPred = originalProg.table.lookup(pred) + val argTypes = actualPred match { + case in.FPredicate(_, args, _) => args map (_.typ) + case in.BuiltInFPredicate(_, _, argsT) => argsT + } + val newArgs = args zip argTypes map { case (arg, typ) => + transformExprToIntendedType(originalProg)(arg, typ) + } + in.FPredicateAccess(pred, newArgs)(p.info) + case p@in.MPredicateAccess(recv, pred, args) => + // no need to cast the receiver to the intended receiver type, the type resolution would have failed if there + // was a type mismatch + val newRecv = transformExpr(originalProg)(recv) + val actualPred = originalProg.table.lookup(pred) + val argTypes = actualPred match { + case in.MPredicate(_, _, args, _) => args map (_.typ) + case in.BuiltInMPredicate(_, _, _, argsT) => argsT + } + val newArgs = args zip argTypes map { case (arg, typ) => + transformExprToIntendedType(originalProg)(arg, typ) + } + in.MPredicateAccess(newRecv, pred, newArgs)(p.info) + case in.MemoryPredicateAccess(arg) => ??? + + } + + private def transformExpr(originalProg: in.Program)(e: in.Expr): in.Expr = transformExprToIntendedType(originalProg)(e, e.typ) + private def transformExprToIntendedType(originalProg: in.Program)(e: in.Expr, intededType: in.Type): in.Expr = { + val newE: in.Expr = e match { + case c@in.Conditional(cond, thn, els, typ) => + val newCond = transformExpr(originalProg)(cond) + val newThn = transformExprToIntendedType(originalProg)(thn, typ) + val newEls = transformExprToIntendedType(originalProg)(els, typ) + in.Conditional(newCond, newThn, newEls, typ)(c.info) + case a@in.And(l, r) => + val newL = transformExpr(originalProg)(l) + val newR = transformExpr(originalProg)(r) + in.And(newL, newR)(a.info) + case o@in.Or(l, r) => + val newL = transformExpr(originalProg)(l) + val newR = transformExpr(originalProg)(r) + in.Or(newL, newR)(o.info) + case e@in.EqCmp(l, r) => + val (newL, newR) = mergeNumericalTypes(originalProg)(l.typ, r.typ) match { + case Some(typ) => + val ll = transformExprToIntendedType(originalProg)(l, typ) + val rr = transformExprToIntendedType(originalProg)(r, typ) + (ll, rr) + case None => + val ll = transformExpr(originalProg)(l) + val rr = transformExpr(originalProg)(r) + (ll, rr) + } + in.EqCmp(newL, newR)(e.info) + case e@in.GhostEqCmp(l, r) => + val (newL, newR) = mergeNumericalTypes(originalProg)(l.typ, r.typ) match { + case Some(typ) => + val ll = transformExprToIntendedType(originalProg)(l, typ) + val rr = transformExprToIntendedType(originalProg)(r, typ) + (ll, rr) + case None => + val ll = transformExpr(originalProg)(l) + val rr = transformExpr(originalProg)(r) + (ll, rr) + } + in.GhostEqCmp(newL, newR)(e.info) + case e@in.GhostUneqCmp(l, r) => + val (newL, newR) = mergeNumericalTypes(originalProg)(l.typ, r.typ) match { + case Some(typ) => + val ll = transformExprToIntendedType(originalProg)(l, typ) + val rr = transformExprToIntendedType(originalProg)(r, typ) + (ll, rr) + case None => + val ll = transformExpr(originalProg)(l) + val rr = transformExpr(originalProg)(r) + (ll, rr) + } + in.GhostUneqCmp(newL, newR)(e.info) + case u@in.UneqCmp(l, r) => + val (newL, newR) = mergeNumericalTypes(originalProg)(l.typ, r.typ) match { + case Some(typ) => + val ll = transformExprToIntendedType(originalProg)(l, typ) + val rr = transformExprToIntendedType(originalProg)(r, typ) + (ll, rr) + case None => + val ll = transformExpr(originalProg)(l) + val rr = transformExpr(originalProg)(r) + (ll, rr) + } + in.UneqCmp(newL, newR)(u.info) + case c@in.LessCmp(l, r) => + val (newL, newR) = mergeNumericalTypes(originalProg)(l.typ, r.typ) match { + case Some(typ) => + val ll = transformExprToIntendedType(originalProg)(l, typ) + val rr = transformExprToIntendedType(originalProg)(r, typ) + (ll, rr) + case None => + val ll = transformExpr(originalProg)(l) + val rr = transformExpr(originalProg)(r) + (ll, rr) + } + in.LessCmp(newL, newR)(c.info) + case c@in.GreaterCmp(l, r) => + val (newL, newR) = mergeNumericalTypes(originalProg)(l.typ, r.typ) match { + case Some(typ) => + val ll = transformExprToIntendedType(originalProg)(l, typ) + val rr = transformExprToIntendedType(originalProg)(r, typ) + (ll, rr) + case None => + val ll = transformExpr(originalProg)(l) + val rr = transformExpr(originalProg)(r) + (ll, rr) + } + in.GreaterCmp(newL, newR)(c.info) + case c@in.AtLeastCmp(l, r) => + val (newL, newR) = mergeNumericalTypes(originalProg)(l.typ, r.typ) match { + case Some(typ) => + val ll = transformExprToIntendedType(originalProg)(l, typ) + val rr = transformExprToIntendedType(originalProg)(r, typ) + (ll, rr) + case None => + val ll = transformExpr(originalProg)(l) + val rr = transformExpr(originalProg)(r) + (ll, rr) + } + in.AtLeastCmp(newL, newR)(c.info) + case c@in.AtMostCmp(l, r) => + val (newL, newR) = mergeNumericalTypes(originalProg)(l.typ, r.typ) match { + case Some(typ) => + val ll = transformExprToIntendedType(originalProg)(l, typ) + val rr = transformExprToIntendedType(originalProg)(r, typ) + (ll, rr) + case None => + val ll = transformExpr(originalProg)(l) + val rr = transformExpr(originalProg)(r) + (ll, rr) + } + in.AtMostCmp(newL, newR)(c.info) + case c@in.Add(l, r) => + val typ = c.typ + val newL = transformExprToIntendedType(originalProg)(l, typ) + val newR = transformExprToIntendedType(originalProg)(r, typ) + in.Add(newL, newR)(c.info) + case c@in.Sub(l, r) => + val typ = c.typ + val newL = transformExprToIntendedType(originalProg)(l, typ) + val newR = transformExprToIntendedType(originalProg)(r, typ) + in.Sub(newL, newR)(c.info) + case c@in.Mul(l, r) => + val typ = c.typ + val newL = transformExprToIntendedType(originalProg)(l, typ) + val newR = transformExprToIntendedType(originalProg)(r, typ) + in.Mul(newL, newR)(c.info) + case c@in.Div(l, r) => + val typ = c.typ + val newL = transformExprToIntendedType(originalProg)(l, typ) + val newR = transformExprToIntendedType(originalProg)(r, typ) + in.Div(newL, newR)(c.info) + case c@in.Mod(l, r) => + val typ = c.typ + val newL = transformExprToIntendedType(originalProg)(l, typ) + val newR = transformExprToIntendedType(originalProg)(r, typ) + in.Mod(newL, newR)(c.info) + case c@in.BitAnd(l, r) => + val typ = c.typ + val newL = transformExprToIntendedType(originalProg)(l, typ) + val newR = transformExprToIntendedType(originalProg)(r, typ) + in.BitAnd(newL, newR)(c.info) + case c@in.BitOr(l, r) => + val typ = c.typ + val newL = transformExprToIntendedType(originalProg)(l, typ) + val newR = transformExprToIntendedType(originalProg)(r, typ) + in.BitOr(newL, newR)(c.info) + case c@in.BitXor(l, r) => + val typ = c.typ + val newL = transformExprToIntendedType(originalProg)(l, typ) + val newR = transformExprToIntendedType(originalProg)(r, typ) + in.BitXor(newL, newR)(c.info) + case c@in.BitClear(l, r) => + val typ = c.typ + val newL = transformExprToIntendedType(originalProg)(l, typ) + val newR = transformExprToIntendedType(originalProg)(r, typ) + in.BitClear(newL, newR)(c.info) + case c@in.ShiftLeft(l, r) => + val typ = c.typ + val newL = transformExprToIntendedType(originalProg)(l, typ) + val newR = transformExpr(originalProg)(r) + in.ShiftLeft(newL, newR)(c.info) + case c@in.ShiftRight(l, r) => + val typ = c.typ + val newL = transformExprToIntendedType(originalProg)(l, typ) + val newR = transformExpr(originalProg)(r) + in.ShiftRight(newL, newR)(c.info) + case c@in.BitNeg(op) => + val newOp = transformExprToIntendedType(originalProg)(op, intededType) + in.BitNeg(newOp)(c.info) + case n@in.Negation(op) => + val newOp = transformExpr(originalProg)(op) + in.Negation(newOp)(n.info) + case c@in.PermGeCmp(l, r) => + val newL = transformExpr(originalProg)(l) // maybe cast this to Perm type instead + val newR = transformExpr(originalProg)(r) // maybe cast this to Perm type instead + in.PermGeCmp(newL, newR)(c.info) + case c@in.PermGtCmp(l, r) => + val newL = transformExpr(originalProg)(l) // maybe cast this to Perm type instead + val newR = transformExpr(originalProg)(r) // maybe cast this to Perm type instead + in.PermGtCmp(newL, newR)(c.info) + case c@in.PermLeCmp(l, r) => + val newL = transformExpr(originalProg)(l) // maybe cast this to Perm type instead + val newR = transformExpr(originalProg)(r) // maybe cast this to Perm type instead + in.PermLeCmp(newL, newR)(c.info) + case c@in.PermLtCmp(l, r) => + val newL = transformExpr(originalProg)(l) // maybe cast this to Perm type instead + val newR = transformExpr(originalProg)(r) // maybe cast this to Perm type instead + in.PermLtCmp(newL, newR)(c.info) + case f: in.FullPerm => f + case n: in.NoPerm => n + case w: in.WildcardPerm => w + /* + case p@in.FractionalPerm(l, r) => + val newL = transformExpr(originalProg)(l) // maybe cast this to Perm type instead + val newR = transformExpr(originalProg)(r) // maybe cast this to Perm type instead + in.FractionalPerm(newL, newR)(p.info) + + */ + case p@in.FractionalPerm(l, r) => + // skipping transformation for now, otherwise we run into issues with Viper's ambiguous syntax for fractional perms + in.FractionalPerm(l, r)(p.info) + case p@in.PermAdd(l, r) => + val newL = transformExpr(originalProg)(l) + val newR = transformExpr(originalProg)(r) + in.PermAdd(newL, newR)(p.info) + case p@in.PermSub(l, r) => + val newL = transformExpr(originalProg)(l) + val newR = transformExpr(originalProg)(r) + in.PermSub(newL, newR)(p.info) + case p@in.PermMul(l, r) => + val newL = transformExpr(originalProg)(l) + val newR = transformExpr(originalProg)(r) + in.PermMul(newL, newR)(p.info) + case p@in.PermDiv(l, r) => + val newL = transformExpr(originalProg)(l) + val newR = transformExpr(originalProg)(r) + in.PermDiv(newL, newR)(p.info) + case p@in.PermMinus(e) => + val newE = transformExpr(originalProg)(e) + in.PermMinus(newE)(p.info) + case c@in.Conversion(t, e) => + val newE = transformExpr(originalProg)(e) + in.Conversion(t, newE)(c.info) + case p@in.PureFunctionCall(func, args, typ, reveal) => + val f = originalProg.table.lookup(func) + val argTypes = f match { + case pf: PureFunction => pf.args map (_.typ) + case _ => + // unreachable case + ??? + } + val newArgs = args zip argTypes map { case (arg, typ) => + transformExprToIntendedType(originalProg)(arg, typ) + } + in.PureFunctionCall(func, newArgs, typ, reveal)(p.info) + case p@in.PureMethodCall(recv, func, args, typ, reveal) => + val m = originalProg.table.lookup(func) + val (recvT, argTypes) = m match { + case pf: PureMethod => (pf.receiver.typ ,pf.args map (_.typ)) + case bm: in.BuiltInMethod => (bm.receiverT, bm.argsT) + case f => + // unreachable case + println(s"missing this case: $f, ${f.getClass}") + ??? + } + val newRecv = transformExprToIntendedType(originalProg)(recv, recvT) + val newArgs = args zip argTypes map { case (arg, typ) => + transformExprToIntendedType(originalProg)(arg, typ) + } + in.PureMethodCall(newRecv, func, newArgs, typ, reveal)(p.info) + case l: in.Location => + transformLocation(originalProg)(l) + case l: in.Lit => l match { + case i: in.IntLit => i + case s: in.StructLit => + println(s"type of a lit: ${s.typ}") + val fieldsT = underlyingType(originalProg)(s.typ) match { + case st: in.StructT => + st.fields.map(_.typ) + case _ => + // error case + ??? + } + val newFields = fieldsT zip s.args map { case (t, arg) => transformExprToIntendedType(originalProg)(arg, t) } + // val structT = originalProg.table.lookup() + in.StructLit(s.typ, newFields)(s.info) + case o => + // TODO + o + } + case l: in.Length => l + case c: in.Capacity => c + //case s@in.Slice(base, low, high, max, baseUnderlyingType) => + case s@in.Slice(base, low, high, max, baseUnderlyingType) => + val idxType = baseUnderlyingType match { + case _: in.SequenceT => integerType + case _: in.SliceT => intType + case _: in.ArrayT => intType + case _: in.StringT => intType + case _ => intType + } + val newBase = transformExpr(originalProg)(base) + val newLow = transformExprToIntendedType(originalProg)(low, idxType) + val newHigh = transformExprToIntendedType(originalProg)(high, idxType) + val newMax = max map { m => transformExprToIntendedType(originalProg)(m, idxType) } + // in.Slice(newBase, low, high, max, baseUnderlyingType)(s.info) + val newS = in.Slice(newBase, newLow, newHigh, newMax, baseUnderlyingType)(s.info) + println(s"oldSlice: $s") + println(s"newSlice: $newS") + newS + + case d: in.DfltVal => d + case o: in.Old => + val newOp = transformExpr(originalProg)(o.operand) + in.Old(newOp)(o.info) + case o: in.LabeledOld => + val newOp = transformExpr(originalProg)(o.operand) + in.LabeledOld(o.label, newOp)(o.info) + case u: in.Unfolding => + val newAcc = transformAccess(originalProg)(u.acc) + val newExpr = transformExprToIntendedType(originalProg)(u.in, u.typ) + in.Unfolding(newAcc, newExpr)(u.info) + + case s@in.Contains(l, r) => + val newL = transformExpr(originalProg)(l) + val newR = transformExpr(originalProg)(r) + in.Contains(newL, newR)(s.info) + case u@in.Union(l, r, typ) => + val newL = transformExpr(originalProg)(l) + val newR = transformExpr(originalProg)(r) + in.Union(newL, newR, typ)(u.info) + case i@in.Intersection(l, r, typ) => + val newL = transformExpr(originalProg)(l) + val newR = transformExpr(originalProg)(r) + in.Intersection(newL, newR, typ)(i.info) + case m@in.SetMinus(l, r, typ) => + val newL = transformExpr(originalProg)(l) + val newR = transformExpr(originalProg)(r) + in.SetMinus(newL, newR, typ)(m.info) + case s@in.SequenceTake(left, right) => + val newL = transformExpr(originalProg)(left) + val newR = transformExpr(originalProg)(right) + in.SequenceTake(newL, newR)(s.info) + case s@in.SequenceDrop(left, right) => + val newL = transformExpr(originalProg)(left) + val newR = transformExpr(originalProg)(right) + in.SequenceDrop(newL, newR)(s.info) + case u@in.GhostCollectionUpdate(base, left, right, baseUnderlyingType) => + val newBase = transformExpr(originalProg)(base) + val newLeft = transformExpr(originalProg)(left) + val newRight = transformExpr(originalProg)(right) + in.GhostCollectionUpdate(newBase, newLeft, newRight, baseUnderlyingType)(u.info) + + + case k@in.MapKeys(exp, typ) => + val newExp = transformExpr(originalProg)(exp) + in.MapKeys(newExp, typ)(k.info) + + case p@in.PureLet(l, r, i) => + val newR = transformExprToIntendedType(originalProg)(r, l.typ) + val newI = transformExpr(originalProg)(i) + in.PureLet(l, newR, newI)(p.info) + + /* + case t@in.Tuple(args) => + val newArgs = args map transformExpr(originalProg) + in.Tuple(newArgs)(t.info) + + */ + + case t@in.ToInterface(exp, typ) => + val newExp = transformExpr(originalProg)(exp) + in.ToInterface(newExp, typ)(t.info) + case c@in.IsComparableInterface(exp) => + val newExp = transformExpr(originalProg)(exp) + in.IsComparableInterface(newExp)(c.info) + case c@in.IsComparableType(exp) => + val newExp = transformExpr(originalProg)(exp) + in.IsComparableType(newExp)(c.info) + case p@in.PredicateConstructor(proxy, proxyT, args) => + val argT = proxyT.args + /* + val newArgs = args zip argT map { case (arg, typ) => + transformExprToIntendedType(originalProg)(arg, typ) + } + */ + // TODO: for now, skip this. add necessary transformation later + p + case t@in.TypeOf(exp) => + val newExp = transformExpr(originalProg)(exp) + in.TypeOf(newExp)(t.info) + case t: in.TypeExpr => t + case a@in.TypeAssertion(exp, arg) => + val newExp = transformExpr(originalProg)(exp) + in.TypeAssertion(newExp, arg)(a.info) + case p@in.PureForall(vars, triggers, body) => + val newTriggers = triggers map transformTrigger(originalProg) + val newBody = transformExpr(originalProg)(body) + in.PureForall(vars, newTriggers, newBody)(p.info) + case s@in.OptionSome(exp) => + val newExpr = transformExpr(originalProg)(exp) + in.OptionSome(newExpr)(s.info) + case s@in.OptionNone(typ) => + in.OptionNone(typ)(s.info) + case s@in.OptionGet(exp) => + val newExpr = transformExpr(originalProg)(exp) + in.OptionGet(newExpr)(s.info) + case a@in.SequenceAppend(left, right, typ) => + val newLeft = transformExpr(originalProg)(left) + val newRight = transformExpr(originalProg)(right) + in.SequenceAppend(newLeft, newRight, typ)(a.info) + case a@in.AdtDiscriminator(base, clause) => + val newBase = transformExpr(originalProg)(base) + in.AdtDiscriminator(newBase, clause)(a.info) + case a@in.AdtDestructor(base, field) => + val newBase = transformExpr(originalProg)(base) + in.AdtDestructor(newBase, field)(a.info) + case m@in.PatternMatchExp(exp, typ, cases, default) => + val newExp = transformExpr(originalProg)(exp) + val newCases = cases map(transformPatternMatchCaseExp(originalProg)(_, typ)) + val newDefault = default map transformExpr(originalProg) + in.PatternMatchExp(newExp, typ, newCases, newDefault)(m.info) + + case i@in.ClosureImplements(closure, spec) => + val newClosure = transformExpr(originalProg)(closure) + val newSpec = transformClosureSpec(originalProg)(spec) + in.ClosureImplements(newClosure, newSpec)(i.info) + + case i => + println(s"Trying $i, class ${i.getClass}") + ??? + } + // TODO: check if I am trying to convert to an interface type + if (newE.typ.equalsWithoutMod(intededType)) + newE + else if (underlyingType(originalProg)(intededType).isInstanceOf[in.InterfaceT]) { + in.ToInterface(newE, intededType.withAddressability(newE.typ.addressability))(newE.info) + } else { + in.Conversion(intededType.withAddressability(newE.typ.addressability), newE)(newE.info) + } + } + + private def transformClosureSpec(originalProg: Program)(c: in.ClosureSpec): in.ClosureSpec = { + // TODO??? Does it need changes? + c + } + + private def transformPatternMatchCaseExp(originalProg: Program)(e: PatternMatchCaseExp, intendedType: in.Type): PatternMatchCaseExp = { + val newExp = transformExprToIntendedType(originalProg)(e.exp, intendedType) + in.PatternMatchCaseExp(e.mExp, newExp)(e.info) + } + + private def transformTrigger(originalProg: in.Program)(t: in.Trigger): in.Trigger = { + val newExprs = t.exprs map { + case e: in.Expr => transformExpr(originalProg)(e) + case o => + // TODO: adapt these + o + } + in.Trigger(newExprs)(t.info) + } + + private def transformBlock(originalProg: in.Program)(b: in.Block): in.Block = { + in.Block(b.decls, b.stmts map transformStmt(originalProg))(b.info) + } + + private def transformStmt(originalProg: in.Program)(s: in.Stmt): in.Stmt = s match { + case b: in.Block => transformBlock(originalProg)(b) + case s@in.Seqn(stmts) => in.Seqn(stmts map transformStmt(originalProg))(s.info) + case i: in.Initialization => i + case a@in.Assert(ass) => in.Assert(transformAssert(originalProg)(ass))(a.info) + case a@in.Assume(ass) => in.Assume(transformAssert(originalProg)(ass))(a.info) + case a@in.Inhale(ass) => in.Inhale(transformAssert(originalProg)(ass))(a.info) + case a@in.Exhale(ass) => in.Exhale(transformAssert(originalProg)(ass))(a.info) + case a@in.SingleAss(l, r) => + val newL = transformAssignee(originalProg)(l) + val newR = transformExprToIntendedType(originalProg)(r, l.op.typ) + in.SingleAss(newL, newR)(a.info) + case u@in.Fold(acc) => + val newAcc = transformAccess(originalProg)(acc) + in.Fold(newAcc)(u.info) + case u@in.Unfold(acc) => + val newAcc = transformAccess(originalProg)(acc) + in.Unfold(newAcc)(u.info) + case o@in.Outline(name, pres, posts, terminationMeasures, backendAnnotations, body, trusted) => + val newPres = pres map transformAssert(originalProg) + val newPosts = posts map transformAssert(originalProg) + val newMeasuers = terminationMeasures map transformTermMeasure(originalProg) + val newBody = transformStmt(originalProg)(body) + in.Outline(name, newPres, newPosts, newMeasuers, backendAnnotations, newBody, trusted)(o.info) + case a@in.ApplyWand(wand) => + val newWand = transformAssert(originalProg)(wand).asInstanceOf[in.MagicWand] + in.ApplyWand(newWand)(a.info) + case m@in.MakeSlice(target, typeParam, lenArg, capArg) => + // TODO: there's already some alternative means of preventing this error in the slice encoding. + // Chose a single solution + m + case n@in.New(target, expr) => + val newExpr = transformExpr(originalProg)(expr) + in.New(target, newExpr)(n.info) + case n@in.NewSliceLit(target, memberType, elems) => + val newElems = elems map { case (k, v) => + k -> transformExprToIntendedType(originalProg)(v, memberType) + } + in.NewSliceLit(target, memberType, newElems)(n.info) + case n@in.NewMapLit(target, keys, values, entries) => + val newEntries = entries map { case (k, v) => + val newK = transformExprToIntendedType(originalProg)(k, keys) + val newV = transformExprToIntendedType(originalProg)(v, values) + newK -> newV + } + in.NewMapLit(target, keys, values, newEntries)(n.info) + case i@in.If(cond, thn, els) => + val newCond = transformExpr(originalProg)(cond) + val newThn = transformStmt(originalProg)(thn) + val newEls = transformStmt(originalProg)(els) + in.If(newCond, newThn, newEls)(i.info) + case w@in.While(cond, invs, terminationMeasure, body) => + val newCond = transformExpr(originalProg)(cond) + val newInvs = invs map transformAssert(originalProg) + val newTerms = terminationMeasure map transformTermMeasure(originalProg) + val newBody = transformStmt(originalProg)(body) + in.While(newCond, newInvs, newTerms, newBody)(w.info) + case l: in.Label => l + case c: in.Continue => c + case b: in.Break => b + case r: in.Return => r + case d: in.Defer => + val newDef = transformStmt(originalProg)(d.stmt) + in.Defer(newDef.asInstanceOf[in.Deferrable])(d.info) + case p: in.PackageWand => + val newWand = transformAssert(originalProg)(p.wand).asInstanceOf[in.MagicWand] + val newBlock = p.block map transformStmt(originalProg) + in.PackageWand(newWand, newBlock)(p.info) + case c@FunctionCall(targets, func, args) => + val f = originalProg.table.lookup(func) + val argTypes = f match { + case f: in.Function => f.args map (_.typ) + case b: in.BuiltInFunction => b.argsT + case _ => + // unreachable case + ??? + } + val newArgs = args zip argTypes map { case (arg, typ) => + transformExprToIntendedType(originalProg)(arg, typ) + } + in.FunctionCall(targets, func, newArgs)(c.info) + case c@MethodCall(targets, recv, meth, args) => + val m = originalProg.table.lookup(meth) + val (recvT, argTypes) = m match { + case f: in.Method => (f.receiver.typ, f.args map (_.typ)) + case b: in.BuiltInMethod => (b.receiverT, b.argsT) + case _ => + // unreachable case + ??? + } + val newRecv = transformExprToIntendedType(originalProg)(recv, recvT) + val newArgs = args zip argTypes map { case (arg, typ) => + transformExprToIntendedType(originalProg)(arg, typ) + } + in.MethodCall(targets, newRecv, meth, newArgs)(c.info) + case e@in.EffectfulConversion(target, newType, expr) => + val newExpr = transformExpr(originalProg)(expr) + in.EffectfulConversion(target, newType, newExpr)(e.info) + case s@in.SafeTypeAssertion(resTarget, successTarget, expr, typ) => + val newExpr = transformExpr(originalProg)(expr) + in.SafeTypeAssertion(resTarget, successTarget, newExpr, typ)(s.info) + + case p@in.SpecImplementationProof(closure, spec, body, pres, posts) => + val newClosure = transformExpr(originalProg)(closure) + val newSpec = transformClosureSpec(originalProg)(spec) + val newBody = transformBlock(originalProg)(body) + val newPres = pres map transformAssert(originalProg) + val newPosts = posts map transformAssert(originalProg) + in.SpecImplementationProof(newClosure, newSpec, newBody, newPres, newPosts)(p.info) + case l@in.SafeMapLookup(resTarget, successTarget, mapLookup) => + val newMapLookup = transformIndexedExpression(originalProg)(mapLookup) + in.SafeMapLookup(resTarget, successTarget, newMapLookup)(l.info) + + case c@in.ClosureCall(targets, closure, args, spec) => + // TODO: improve, transformations missing + c + case GoFunctionCall(func, args) => ??? + case GoMethodCall(recv, meth, args) => ??? + case GoClosureCall(closure, args, spec) => ??? + } + + private def transformIndexedExpression(originalProg: in.Program)(e: in.IndexedExp): in.IndexedExp = e match { + case i@in.IndexedExp(base, index, baseUnderlyingType) => + val newBase = transformExpr(originalProg)(base) + val idxTyp = baseUnderlyingType match { + case _: in.SequenceT => integerType + case m: in.MapT => m.keys + case m: in.MathMapT => m.keys + case _ => intType + } + val newIdx = transformExprToIntendedType(originalProg)(index, idxTyp) + in.IndexedExp(newBase, newIdx, baseUnderlyingType)(i.info) + } + + private def transformAssignee(originalProg: in.Program)(a: in.Assignee): in.Assignee = a match { + case Assignee.Var(op) => Assignee.Var(op) + case Assignee.Pointer(op) => + val newOp = transformDeref(originalProg)(op) + Assignee.Pointer(newOp) + case Assignee.Field(op) => + val newOp = transformFieldRef(originalProg)(op) + Assignee.Field(newOp) + case Assignee.Index(op) => + val newOp = transformIndexedExpression(originalProg)(op) + Assignee.Index(newOp) + } + + private def transformAddressable(originalProg: in.Program)(a: in.Addressable): in.Addressable = a match { + case v@in.Addressable.Var(_) => v + case v@in.Addressable.GlobalVar(_) => v + case in.Addressable.Pointer(op) => + val newOp = transformDeref(originalProg)(op) + in.Addressable.Pointer(newOp) + case in.Addressable.Field(op) => + val newOp = transformFieldRef(originalProg)(op) + in.Addressable.Field(newOp) + case in.Addressable.Index(op) => + val newOp = transformIndexedExpression(originalProg)(op) + in.Addressable.Index(newOp) + } + + private def transformFieldRef(originalProg: in.Program)(f: in.FieldRef): in.FieldRef = { + val newExp = transformExpr(originalProg)(f.recv) + in.FieldRef(newExp, f.field)(f.info) + } + + private def transformDeref(originalProg: in.Program)(d: in.Deref): in.Deref = { + val newExpr = transformExpr(originalProg)(d.exp) + in.Deref(newExpr, d.underlyingTypeExpr)(d.info) + } + + private def transformMethodBody(originalProg: in.Program)(b: in.MethodBody): in.MethodBody = b match { + case b@in.MethodBody(decls, seqn, postprocessing) => + val newSeqn = in.MethodBodySeqn(seqn.stmts map transformStmt(originalProg))(seqn.info) + val newPostprocessing = postprocessing map transformStmt(originalProg) + in.MethodBody(decls, newSeqn, newPostprocessing)(b.info) + } + private def transformTermMeasure(originalProg: in.Program)(m: in.TerminationMeasure): in.TerminationMeasure = m match { + case m@in.ItfMethodWildcardMeasure(cond) => + in.ItfMethodWildcardMeasure(cond map transformExpr(originalProg))(m.info) + case m@in.NonItfMethodWildcardMeasure(cond) => + in.NonItfMethodWildcardMeasure(cond map transformExpr(originalProg))(m.info) + case m@in.ItfTupleTerminationMeasure(tuple, cond) => + val newTuple = tuple map { + case e: in.Expr => transformExpr(originalProg)(e) + case o => o + } + val newCond = cond map transformExpr(originalProg) + in.ItfTupleTerminationMeasure(newTuple, newCond)(m.info) + case m@in.NonItfTupleTerminationMeasure(tuple, cond) => + val newTuple = tuple map { + case e: in.Expr => transformExpr(originalProg)(e) + case o => o + } + val newCond = cond map transformExpr(originalProg) + in.NonItfTupleTerminationMeasure(newTuple, newCond)(m.info) + } + private def transformMember(originalProg: in.Program)(m: in.Member): in.Member = + m match { + case g@in.GlobalVarDecl(left, declStmts) => + val newDeclStmts = declStmts map transformStmt(originalProg) + in.GlobalVarDecl(left, newDeclStmts)(g.info) + + case g: in.GlobalConstDecl => g + case m@in.Method(receiver, name, args, results, pres, posts, terminationMeasures, backendAnnotations, body) => + val newPres = pres map transformAssert(originalProg) + val newPosts = posts map transformAssert(originalProg) + val newTermMeasures = terminationMeasures map transformTermMeasure(originalProg) + val newBody = body map transformMethodBody(originalProg) + in.Method(receiver, name, args, results, newPres, newPosts, newTermMeasures, backendAnnotations, newBody)(m.info) + case m@in.PureMethod(receiver, name, args, results, pres, posts, terminationMeasures, backendAnnotations, body, isOpaque) => + val newPres = pres map transformAssert(originalProg) + val newPosts = posts map transformAssert(originalProg) + val newTermMeasures = terminationMeasures map transformTermMeasure(originalProg) + val newBody = body map transformExpr(originalProg) + in.PureMethod(receiver, name, args, results, newPres, newPosts, newTermMeasures, backendAnnotations, newBody, isOpaque)(m.info) + case p@in.MethodSubtypeProof(subProxy, superT, superProxy, receiver, args, results, body) => + val newBody = body map(transformBlock(originalProg)(_)) + in.MethodSubtypeProof(subProxy, superT, superProxy, receiver, args, results, newBody)(p.info) + case p@in.PureMethodSubtypeProof(subProxy, superT, superProxy, receiver, args, results, body) => + val newBody = body map(transformExpr(originalProg)(_)) + in.PureMethodSubtypeProof(subProxy, superT, superProxy, receiver, args, results, newBody)(p.info) + case f@in.Function(name, args, results, pres, posts, terminationMeasures, backendAnnotations, body) => + val newPres = pres map transformAssert(originalProg) + val newPosts = posts map transformAssert(originalProg) + val newTermMeasures = terminationMeasures map transformTermMeasure(originalProg) + val newBody = body map transformMethodBody(originalProg) + in.Function(name, args, results, newPres, newPosts, newTermMeasures, backendAnnotations, newBody)(f.info) + case f@in.PureFunction(name, args, results, pres, posts, terminationMeasures, backendAnnotations, body, isOpaque) => + val newPres = pres map transformAssert(originalProg) + val newPosts = posts map transformAssert(originalProg) + val newTermMeasures = terminationMeasures map transformTermMeasure(originalProg) + val newBody = body map(transformExprToIntendedType(originalProg)(_, results(0).typ)) + in.PureFunction(name, args, results, newPres, newPosts, newTermMeasures, backendAnnotations, newBody, isOpaque)(f.info) + case t: in.BuiltInMember => t + case f@in.FPredicate(name, args, body) => + in.FPredicate(name, args, body.map(transformAssert(originalProg)))(f.info) + case m@in.MPredicate(receiver, name, args, body) => + in.MPredicate(receiver, name, args, body.map(transformAssert(originalProg)))(m.info) + case d@in.DomainDefinition(name, funcs, axioms) => + val newAxioms = axioms map { + case a@in.DomainAxiom(ax) => + val newAx = transformExpr(originalProg)(ax) + in.DomainAxiom(newAx)(a.info) + } + in.DomainDefinition(name, funcs, newAxioms)(d.info) + case a: in.AdtDefinition => a + } + + // TODO: maybe adapt to return an option[in.Type] + private def mergeNumericalTypes(originalProg: in.Program)(t1: in.Type, t2: in.Type): Option[in.Type] = { + val isNumerical1 = isNumericalType(originalProg)(t1) + val isNumerical2 = isNumericalType(originalProg)(t2) + if (!isNumerical1 || !isNumerical2) { + None + } else if (t1 == t2) { + Some(t1) + } else if (t1.equalsWithoutMod(t2)) { + println(s"AAA: weird case reached: t1: $t1, t2: $t2") + Some(t1.withAddressability(t2.addressability)) // TODO: what about this here? + } else if (isNumericalType(originalProg)(t1) && isNumericalType(originalProg)(t2)) { + (t1, t2) match { + case (in.IntT(_, TypeBounds.UnboundedInteger), _) => Some(t2) + case (_, in.IntT(_, TypeBounds.UnboundedInteger)) => Some(t1) + case (a, b) => + println(s"weird case: a: $a and b: $b") + None + case _ => + // cannot unify + ??? + } + } else { + None + } + } + + private def underlyingType(originalProg: in.Program)(t: in.Type): in.Type = t match { + case d: in.DefinedT => underlyingType(originalProg)(originalProg.table.lookup(d)) + case o => o + } + + private def isNumericalType(originalProg: in.Program)(t: in.Type): Boolean = { + underlyingType(originalProg)(t) match { + case _: in.IntT => true + case _ => false + } + } +} diff --git a/src/main/scala/viper/gobra/ast/internal/transform/OverflowChecksTransform.scala b/src/main/scala/viper/gobra/ast/internal/transform/OverflowChecksTransform.scala index 5c39831ca..4ebca3f39 100644 --- a/src/main/scala/viper/gobra/ast/internal/transform/OverflowChecksTransform.scala +++ b/src/main/scala/viper/gobra/ast/internal/transform/OverflowChecksTransform.scala @@ -13,6 +13,7 @@ import viper.gobra.reporting.Source.Parser.Single import viper.gobra.util.TypeBounds.BoundedIntegerKind import viper.gobra.util.Violation.violation +// TODO: drop this /** * Adds overflow checks to programs written in Gobra's internal language */ diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index f3b1e37e9..87dafb44f 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -158,10 +158,6 @@ case class Config( checkConsistency: Boolean = ConfigDefaults.DefaultCheckConsistency, shouldVerify: Boolean = true, shouldChop: Boolean = ConfigDefaults.DefaultShouldChop, - // The go language specification states that int and uint variables can have either 32bit or 64, as long - // as they have the same size. This flag allows users to pick the size of int's and uints's: 32 if true, - // 64 bit otherwise. - int32bit: Boolean = ConfigDefaults.DefaultInt32bit, // the following option is currently not controllable via CLI as it is meaningless without a constantly // running JVM. It is targeted in particular to Gobra Server and Gobra IDE cacheParserAndTypeChecker: Boolean = ConfigDefaults.DefaultCacheParserAndTypeChecker, @@ -232,7 +228,6 @@ case class Config( shouldViperEncode = shouldViperEncode, checkOverflows = checkOverflows || other.checkOverflows, shouldVerify = shouldVerify, - int32bit = int32bit || other.int32bit, checkConsistency = checkConsistency || other.checkConsistency, cacheParserAndTypeChecker = cacheParserAndTypeChecker || other.cacheParserAndTypeChecker, onlyFilesWithHeader = onlyFilesWithHeader || other.onlyFilesWithHeader, @@ -261,12 +256,7 @@ case class Config( ) } - lazy val typeBounds: TypeBounds = - if (int32bit) { - TypeBounds() - } else { - TypeBounds(Int = TypeBounds.IntWith64Bit, UInt = TypeBounds.UIntWith64Bit) - } + lazy val typeBounds: TypeBounds = TypeBounds() val backendOrDefault: ViperBackend = backend.getOrElse(ConfigDefaults.DefaultBackend) val hyperModeOrDefault: Hyper.Mode = hyperMode.getOrElse(ConfigDefaults.DefaultHyperMode) @@ -365,7 +355,6 @@ trait RawConfig { checkConsistency = baseConfig.checkConsistency, shouldVerify = baseConfig.shouldVerify, shouldChop = baseConfig.shouldChop, - int32bit = baseConfig.int32bit, cacheParserAndTypeChecker = baseConfig.cacheParserAndTypeChecker, onlyFilesWithHeader = baseConfig.onlyFilesWithHeader, assumeInjectivityOnInhale = baseConfig.assumeInjectivityOnInhale, diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala index 1508987b0..7491d9890 100644 --- a/src/main/scala/viper/gobra/frontend/Desugar.scala +++ b/src/main/scala/viper/gobra/frontend/Desugar.scala @@ -20,8 +20,9 @@ import viper.gobra.reporting.Source.{AutoImplProofAnnotation, ImportPreNotEstabl import viper.gobra.reporting.{DesugaredMessage, Source} import viper.gobra.theory.Addressability import viper.gobra.translator.Names +import viper.gobra.util.TypeBounds.UnboundedInteger import viper.gobra.util.Violation.violation -import viper.gobra.util.{BackendAnnotation, Computation, Constants, DesugarWriter, GobraExecutionContext, Violation} +import viper.gobra.util.{BackendAnnotation, Computation, Constants, DesugarWriter, GobraExecutionContext, TypeBounds, Violation} import java.nio.file.Paths import java.util.concurrent.atomic.AtomicLong @@ -1129,15 +1130,15 @@ object Desugar extends LazyLogging { addedInvariantsBefore = Vector( in.ExprAssertion(in.And( in.AtMostCmp(in.IntLit(0)(src), i0)(src), - in.AtMostCmp(i0, in.Length(c)(src))(src))(src))(src), + in.AtMostCmp(i0, in.Length(c, typ)(src))(src))(src))(src), in.Implication( - in.LessCmp(i0, in.Length(c)(src))(src), + in.LessCmp(i0, in.Length(c, typ)(src))(src), in.ExprAssertion(in.EqCmp(i0, i)(src))(src))(src) ) indexValueSrc = meta(range.exp, info).createAnnotatedInfo(Source.NoPermissionToRangeExpressionAnnotation()) addedInvariantsAfter = (if (hasValue) Vector( in.Implication( - in.LessCmp(i0, in.Length(c)(src))(src), + in.LessCmp(i0, in.Length(c, typ)(src))(src), in.ExprAssertion(in.GhostEqCmp(j, in.IndexedExp(c, i0, typ)(indexValueSrc))(indexValueSrc))(indexValueSrc))(indexValueSrc)) else Vector()) @@ -1158,7 +1159,7 @@ object Desugar extends LazyLogging { // c := x singleAss(in.Assignee.Var(c), exp)(rangeExpSrc), // length := len(c) to save for later since it can change - singleAss(in.Assignee.Var(length), in.Length(c)(src))(src), + singleAss(in.Assignee.Var(length), in.Length(c, typ)(src))(src), in.If( in.EqCmp(length, in.IntLit(0)(src))(src), in.Seqn(Vector( @@ -1268,20 +1269,20 @@ object Desugar extends LazyLogging { addedInvariantsBefore = Vector( in.ExprAssertion(in.And( in.AtMostCmp(in.IntLit(0)(src), i0)(src), - in.AtMostCmp(i0, in.Length(c)(src))(src))(src))(src) + in.AtMostCmp(i0, in.Length(c, typ)(src))(src))(src))(src) ) indexValueSrc = meta(range.exp, info).createAnnotatedInfo(Source.NoPermissionToRangeExpressionAnnotation()) addedInvariantsAfter = (if (hasValue) Vector( in.Implication( - in.LessCmp(i0, in.Length(c)(src))(src), + in.LessCmp(i0, in.Length(c, typ)(src))(src), in.ExprAssertion(in.EqCmp(i0, i.op)(src))(src))(src), in.Implication( - in.LessCmp(i0, in.Length(c)(src))(src), + in.LessCmp(i0, in.Length(c, typ)(src))(src), in.ExprAssertion(in.GhostEqCmp(j.op, in.IndexedExp(c, i0, typ)(indexValueSrc))(indexValueSrc))(indexValueSrc))(indexValueSrc)) else Vector( in.Implication( - in.LessCmp(i0, in.Length(c)(src))(src), + in.LessCmp(i0, in.Length(c, typ)(src))(src), in.ExprAssertion(in.EqCmp(i0, i.op)(src))(src))(src))) dBody = blockD(ctx, info)(body) @@ -1300,7 +1301,7 @@ object Desugar extends LazyLogging { // c := x singleAss(in.Assignee.Var(c), exp)(rangeExpSrc), // length := len(c) to save for later since it can change - singleAss(in.Assignee.Var(length), in.Length(c)(src))(src), + singleAss(in.Assignee.Var(length), in.Length(c, typ)(src))(src), in.If( in.EqCmp(length, in.IntLit(0)(src))(src), in.Seqn( @@ -1394,8 +1395,11 @@ object Desugar extends LazyLogging { c <- freshDeclaredExclusiveVar(exp.typ.withAddressability(Addressability.exclusiveVariable), n, info)(src) - (keyType, valType) = underlyingType(exp.typ) match { - case in.MapT(k, v, _) => (k.withAddressability(Addressability.exclusiveVariable), v.withAddressability(Addressability.exclusiveVariable)) + (keyType, valType, typ) = underlyingType(exp.typ) match { + case t@in.MapT(k, v, _) => + (k.withAddressability(Addressability.exclusiveVariable), + v.withAddressability(Addressability.exclusiveVariable), + t) case _ => violation("unexpected type of range expression") } @@ -1420,7 +1424,7 @@ object Desugar extends LazyLogging { (dInvPre, dInv) <- prelude(sequence(spec.invariants map assertionD(ctx, info))) addedInvariants = if (range.enumerated != PWildcard()) // emit invariants about visited set only if we actually use a with clause and specify an identifier for it Vector( - in.ExprAssertion(in.AtMostCmp(in.Length(visited.op)(src), in.Length(c)(src))(src))(src), + in.ExprAssertion(in.AtMostCmp(in.Length(visited.op, visitedT)(src), in.Length(c, typ)(src))(src))(src), in.ExprAssertion(in.Subset(visited.op, domain)(src))(src)) else Vector() @@ -1455,7 +1459,7 @@ object Desugar extends LazyLogging { enc = in.Seqn(Vector( singleAss(in.Assignee.Var(c), exp)(src), in.If( - in.EqCmp(in.Length(c)(src), in.IntLit(0)(src))(src), + in.EqCmp(in.Length(c, typ)(src), in.IntLit(0)(src))(src), in.Seqn( // assert (spec.invariants zip dInv).map[in.Stmt]((x: (PExpression, in.Assertion)) => in.Assert(x._2)(meta(x._1, info).createAnnotatedInfo(Source.LoopInvariantNotEstablishedAnnotation))))(src), @@ -1463,7 +1467,7 @@ object Desugar extends LazyLogging { dInvPre ++ dTerPre ++ Vector( initPerm, in.While( - in.LessCmp(in.Length(visited.op)(src), in.Length(c)(src))(src), + in.LessCmp(in.Length(visited.op, visitedT)(src), in.Length(c, typ)(src))(src), dInv ++ addedInvariants, dTer, in.Block(Vector(continueLoopLabelProxy, k) ++ (if (hasValue) Vector(v) else Vector()), Vector(exhalePerm, updateKeyVal, dBody, continueLoopLabel, inhalePerm, updateVisited) ++ dInvPre ++ dTerPre )(src))(src)) ++ (if (range.enumerated != PWildcard()) Vector(visitedEqDomain) else Vector()) ++ Vector(breakLoopLabel))(src) // emit assertions about visited set only if we actually use a with clause and specify an identifier for it @@ -1474,8 +1478,9 @@ object Desugar extends LazyLogging { def desugarMapAssRange(n: PAssForRange, range: PRange, ass: Vector[PAssignee], spec: PLoopSpec, body: PBlock)(src: Source.Parser.Info): Writer[in.Stmt] = unit(block(for { exp <- goE(range.exp) - keyType = underlyingType(exp.typ) match { - case in.MapT(k, _, _) => k.withAddressability(Addressability.exclusiveVariable) + (keyType, typ) = underlyingType(exp.typ) match { + case t@in.MapT(k, _, _) => + (k.withAddressability(Addressability.exclusiveVariable), t) case _ => violation("unexpected type of range expression") } @@ -1501,7 +1506,7 @@ object Desugar extends LazyLogging { (dTerPre, dTer) <- prelude(option(spec.terminationMeasure map terminationMeasureD(ctx, info, false))) (dInvPre, dInv) <- prelude(sequence(spec.invariants map assertionD(ctx, info))) addedInvariants = Vector( - in.ExprAssertion(in.AtMostCmp(in.Length(visited.op)(src), in.Length(c)(src))(src))(src), + in.ExprAssertion(in.AtMostCmp(in.Length(visited.op, visitedT)(src), in.Length(c, typ)(src))(src))(src), in.ExprAssertion(in.Subset(visited.op, domain)(src))(src)) dBody = blockD(ctx, info)(body) @@ -1537,7 +1542,7 @@ object Desugar extends LazyLogging { enc = in.Seqn(Vector( singleAss(in.Assignee.Var(c), exp)(src), in.If( - in.EqCmp(in.Length(c)(src), in.IntLit(0)(src))(src), + in.EqCmp(in.Length(c, typ)(src), in.IntLit(0)(src))(src), in.Seqn( // assert (spec.invariants zip dInv).map[in.Stmt]((x: (PExpression, in.Assertion)) => in.Assert(x._2)(meta(x._1, info).createAnnotatedInfo(Source.LoopInvariantNotEstablishedAnnotation))))(src), @@ -1545,7 +1550,7 @@ object Desugar extends LazyLogging { dInvPre ++ dTerPre ++ Vector( initPerm, in.While( - in.LessCmp(in.Length(visited.op)(src), in.Length(c)(src))(src), + in.LessCmp(in.Length(visited.op, visitedT)(src), in.Length(c, typ)(src))(src), dInv ++ addedInvariants, dTer, in.Block(Vector(continueLoopLabelProxy, tempk), Vector(exhalePerm, updateKeyVal, dBody, continueLoopLabel, inhalePerm, updateVisited) ++ dInvPre ++ dTerPre )(src))(src), visitedEqDomain, breakLoopLabel @@ -2754,25 +2759,37 @@ object Desugar extends LazyLogging { } case baseT @ (_: in.ArrayT | _: in.SliceT | in.PointerT(_: in.ArrayT, _)) => (dlow, dhigh) match { - case (None, None) => in.Slice(dbase, in.IntLit(0)(src), in.Length(dbase)(src), dcap, baseT)(src) - case (Some(lo), None) => in.Slice(dbase, lo, in.Length(dbase)(src), dcap, baseT)(src) + case (None, None) => in.Slice( + dbase, + in.Conversion(in.IntT(Addressability.Exclusive, TypeBounds.DefaultInt), in.IntLit(0)(src))(src), + in.Length(dbase, baseT)(src), + dcap, + baseT + )(src) + case (Some(lo), None) => in.Slice(dbase, lo, in.Length(dbase, baseT)(src), dcap, baseT)(src) case (None, Some(hi)) => in.Slice(dbase, in.IntLit(0)(src), hi, dcap, baseT)(src) case (Some(lo), Some(hi)) => in.Slice(dbase, lo, hi, dcap, baseT)(src) } case baseT: in.StringT => Violation.violation(dcap.isEmpty, s"expected dcap to be None when slicing strings, but got $dcap instead") (dlow, dhigh) match { - case (None, None) => in.Slice(dbase, in.IntLit(0)(src), in.Length(dbase)(src), None, baseT)(src) - case (Some(lo), None) => in.Slice(dbase, lo, in.Length(dbase)(src), None, baseT)(src) + case (None, None) => in.Slice(dbase, in.IntLit(0)(src), in.Length(dbase, baseT)(src), None, baseT)(src) + case (Some(lo), None) => in.Slice(dbase, lo, in.Length(dbase, baseT)(src), None, baseT)(src) case (None, Some(hi)) => in.Slice(dbase, in.IntLit(0)(src), hi, None, baseT)(src) case (Some(lo), Some(hi)) => in.Slice(dbase, lo, hi, None, baseT)(src) } case t => Violation.violation(s"desugaring of slice expressions of base type $t is currently not supported") } - case PLength(op) => go(op).map(in.Length(_)(src)) + case PLength(op) => + val typ = underlyingType(info.typ(op)) + val typD = typeD(typ, Addressability.Exclusive)(src) + go(op).map(in.Length(_, typD)(src)) - case PCapacity(op) => go(op).map(in.Capacity(_)(src)) + case PCapacity(op) => + val typ = underlyingType(info.typ(op)) + val typD = typeD(typ, Addressability.Exclusive)(src) + go(op).map(in.Capacity(_, typD)(src)) case g: PGhostExpression => ghostExprD(ctx, info)(g) @@ -3843,6 +3860,7 @@ object Desugar extends LazyLogging { case Type.BooleanT => in.BoolT(addrMod) case Type.StringT => in.StringT(addrMod) case Type.IntT(x) => in.IntT(addrMod, x) + case Type.GhostIntegerT => in.IntT(addrMod, UnboundedInteger) case Type.Float32T => in.Float32T(addrMod) case Type.Float64T => in.Float64T(addrMod) case Type.ArrayT(length, elem) => in.ArrayT(length, typeD(elem, Addressability.arrayElement(addrMod))(src), addrMod) diff --git a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala b/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala index f184db12c..8bc2abdc5 100644 --- a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala +++ b/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala @@ -232,6 +232,7 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole def visitTypeIdentifier(typ: PIdnUse): PUnqualifiedTypeName = { typ.name match { case "perm" => PPermissionType().at(typ) + case "integer" => PGhostIntegerType().at(typ) case "int" => PIntType().at(typ) case "int8" => PInt8Type().at(typ) case "int16" => PInt16Type().at(typ) diff --git a/src/main/scala/viper/gobra/frontend/info/Info.scala b/src/main/scala/viper/gobra/frontend/info/Info.scala index 5b738cf2d..4dfb0b50c 100644 --- a/src/main/scala/viper/gobra/frontend/info/Info.scala +++ b/src/main/scala/viper/gobra/frontend/info/Info.scala @@ -234,9 +234,7 @@ object Info extends LazyLogging { .sorted .mkString("") val isMainContextKey = if (isMainContext) "1" else "0" - val configKey = config.typeBounds.hashCode().toString ++ - (if (config.int32bit) "1" else "0") - + val configKey = config.typeBounds.hashCode().toString val key = pkgKey ++ dependentTypeInfoKey ++ isMainContextKey ++ diff --git a/src/main/scala/viper/gobra/frontend/info/base/BuiltInMemberTag.scala b/src/main/scala/viper/gobra/frontend/info/base/BuiltInMemberTag.scala index e80bb69da..143f1a58c 100644 --- a/src/main/scala/viper/gobra/frontend/info/base/BuiltInMemberTag.scala +++ b/src/main/scala/viper/gobra/frontend/info/base/BuiltInMemberTag.scala @@ -6,8 +6,8 @@ package viper.gobra.frontend.info.base -import viper.gobra.ast.frontend.{PBoolType, PByte, PFloat32, PFloat64, PInt16Type, PInt32Type, PInt64Type, PInt8Type, PIntType, PPermissionType, PRune, PStringType, PType, PUInt16Type, PUInt32Type, PUInt64Type, PUInt8Type, PUIntPtr, PUIntType} -import viper.gobra.frontend.info.base.Type.{BooleanT, Float32T, Float64T, IntT, PermissionT, StringT, Type} +import viper.gobra.ast.frontend.{PBoolType, PByte, PFloat32, PFloat64, PGhostIntegerType, PInt16Type, PInt32Type, PInt64Type, PInt8Type, PIntType, PPermissionType, PRune, PStringType, PType, PUInt16Type, PUInt32Type, PUInt64Type, PUInt8Type, PUIntPtr, PUIntType} +import viper.gobra.frontend.info.base.Type.{BooleanT, Float32T, Float64T, GhostIntegerT, IntT, PermissionT, StringT, Type} import viper.gobra.util.TypeBounds @@ -95,6 +95,13 @@ object BuiltInMemberTag { override def typ: Type = IntT(TypeBounds.DefaultInt) override def node: PType = PIntType() } + case object GhostIntegerType extends BuiltInTypeTag { + override def identifier: String = "integer" + override def name: String = "InteterType" + override def ghost: Boolean = true + override def typ: Type = GhostIntegerT + override def node: PType = PGhostIntegerType() + } case object Int8Type extends BuiltInTypeTag { override def identifier: String = "int8" override def name: String = "Int8Type" @@ -324,6 +331,7 @@ object BuiltInMemberTag { StringType, PermissionType, // signed integer types + GhostIntegerType, Rune, IntType, Int8Type, 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..802039c74 100644 --- a/src/main/scala/viper/gobra/frontend/info/base/Type.scala +++ b/src/main/scala/viper/gobra/frontend/info/base/Type.scala @@ -173,6 +173,8 @@ object Type { case class MathMapT(key : Type, elem : Type) extends PrettyType(s"mmap[$key]$elem") with GhostUnorderedCollectionType + case object GhostIntegerT extends PrettyType(s"integer") with GhostType + case object PermissionT extends PrettyType(s"perm") with GhostType @tailrec 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..e53c04426 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 @@ -125,6 +125,8 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl => // for ghost types case (BooleanT, AssertionT) => successProp + case (_: IntT, GhostIntegerT) => successProp + case (GhostIntegerT, _: IntT) => successProp case (SequenceT(l), SequenceT(r)) => assignableTo.result(l, r, mayInit) // implies that Sequences are covariant case (SetT(l), SetT(r)) => assignableTo.result(l, r, mayInit) case (MultisetT(l), MultisetT(r)) => assignableTo.result(l, r, mayInit) @@ -290,6 +292,7 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl => case typ: BoundedIntegerKind => typ.lower <= value && value <= typ.upper case _ => true } + case GhostIntegerT => true case _ => violation(s"Expected an integer type but instead received $typ.") } 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..c6b97b172 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, GhostIntegerT, GhostPointerT, IntT, PermissionT, Single, SliceT, StringT, Type} import viper.gobra.frontend.info.implementation.TypeInfoImpl trait Convertibility extends BaseProperty { this: TypeInfoImpl => @@ -28,12 +28,15 @@ trait Convertibility extends BaseProperty { this: TypeInfoImpl => case (Float32T, IntT(_)) => successProp case (Float64T, IntT(_)) => successProp case (IntT(_), IntT(_)) => successProp + case (IntT(_), GhostIntegerT) => successProp + case (GhostIntegerT, IntT(_)) => successProp case (SliceT(IntT(config.typeBounds.Byte)), StringT) => successProp case (StringT, SliceT(IntT(config.typeBounds.Byte))) => successProp case (IntT(_), PermissionT) => successProp case (left, right) => (underlyingType(left), underlyingType(right)) match { case (l, r) if identicalTypes(l, r) => successProp case (IntT(_), IntT(_)) => successProp + case (IntT(_), GhostIntegerT) => successProp case (ActualPointerT(l), ActualPointerT(r)) if identicalTypes(underlyingType(l), underlyingType(r)) && !(left.isInstanceOf[DeclaredT] && right.isInstanceOf[DeclaredT]) => successProp case (GhostPointerT(l), GhostPointerT(r)) if identicalTypes(underlyingType(l), underlyingType(r)) && diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/property/TypeIdentity.scala b/src/main/scala/viper/gobra/frontend/info/implementation/property/TypeIdentity.scala index ea7be1337..7749f5dbd 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/property/TypeIdentity.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/property/TypeIdentity.scala @@ -19,6 +19,7 @@ trait TypeIdentity extends BaseProperty { this: TypeInfoImpl => // Two integer types are equal if they have the same type or they are from types which are aliased case (IntT(x), IntT(y)) => x == y || Set(x,y).subsetOf(Set(TypeBounds.SignedInteger32, TypeBounds.Rune)) || Set(x,y).subsetOf(Set(TypeBounds.UnsignedInteger8, TypeBounds.Byte)) + case (GhostIntegerT, GhostIntegerT) => true case (BooleanT, BooleanT) => true case (AssertionT, AssertionT) => true case (StringT, StringT) => true 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..cda3410b9 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 @@ -7,7 +7,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, GhostIntegerT, GhostPointerT, GhostSliceT, IntT, InternalTupleT, MapT, MultisetT, PermissionT, SequenceT, SetT, Single, SliceT, Type} import viper.gobra.frontend.info.implementation.TypeInfoImpl trait TypeMerging extends BaseProperty { this: TypeInfoImpl => @@ -35,6 +35,8 @@ trait TypeMerging extends BaseProperty { this: TypeInfoImpl => case (AssertionT, BooleanT) => Some(AssertionT) case (IntT(_), PermissionT) => Some(PermissionT) case (PermissionT, IntT(_)) => Some(PermissionT) + case (IntT(_), GhostIntegerT) => Some(GhostIntegerT) + case (GhostIntegerT, IntT(_)) => Some(GhostIntegerT) case (SequenceT(l), SequenceT(r)) => typeMerge(l, r) map SequenceT case (SetT(l), SetT(r)) => typeMerge(l, r) map SetT case (MultisetT(l), MultisetT(r)) => typeMerge(l, r) map MultisetT 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..0ab178b27 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 @@ -355,6 +355,9 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => case (SequenceT(_), IntT(_)) => noMessages + case (SequenceT(_), GhostIntegerT) => + noMessages + case (_: SliceT | _: GhostSliceT, IntT(_)) => noMessages @@ -413,8 +416,9 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => error(base, s"array $base is not addressable", !addressable(base)) case (SequenceT(_), lowT, highT, capT) => { - lowT.fold(noMessages)(t => error(low, s"expected an integer but found $t", !t.isInstanceOf[IntT])) ++ - highT.fold(noMessages)(t => error(high, s"expected an integer but found $t", !t.isInstanceOf[IntT])) ++ + // println(s"PEW PEW PEW: $n") + lowT.fold(noMessages)(t => error(low, s"expected an integer but found $t", t != GhostIntegerT && !t.isInstanceOf[IntT])) ++ + highT.fold(noMessages)(t => error(high, s"expected an integer but found $t", t != GhostIntegerT && !t.isInstanceOf[IntT])) ++ error(cap, "sequence slice expressions do not allow specifying a capacity", capT.isDefined) } @@ -687,6 +691,9 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => val typCtx = getNonInterfaceTypeFromCtxt(exp) typCtx.map(underlyingType) match { case Some(intTypeCtx: IntT) => assignableWithinBounds.errors(intTypeCtx, exp)(exp) + case Some(GhostIntegerT) => assignableWithinBounds.errors(GhostIntegerT, exp)(exp) + case Some(Float32T) => noMessages + case Some(Float64T) => noMessages case Some(t) => error(exp, s"$exp is not assignable to type $t") case None => noMessages // no type inferred from context } @@ -743,6 +750,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => case (ArrayT(_, elem), IntT(_)) => elem case (PointerT(ArrayT(_, elem)), IntT(_)) => elem case (SequenceT(elem), IntT(_)) => elem + case (SequenceT(elem), GhostIntegerT) => elem case (SliceT(elem), IntT(_)) => elem case (GhostSliceT(elem), IntT(_)) => elem case (VariadicT(elem), IntT(_)) => elem @@ -761,7 +769,8 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => (underlyingType(baseType), low map exprType, high map exprType, cap map exprType) match { case (ArrayT(_, elem), None | Some(IntT(_)), None | Some(IntT(_)), None | Some(IntT(_))) if addressable(base) => SliceT(elem) case (ActualPointerT(ArrayT(_, elem)), None | Some(IntT(_)), None | Some(IntT(_)), None | Some(IntT(_))) => SliceT(elem) - case (SequenceT(_), None | Some(IntT(_)), None | Some(IntT(_)), None) => baseType + case (SequenceT(_), None | Some(IntT(_) | GhostIntegerT), None | Some(IntT(_) | GhostIntegerT), None) => baseType + // case (SequenceT(_), None | Some(GhostIntegerT), None | Some(IntT(_)), None) => baseType case (SliceT(_), None | Some(IntT(_)), None | Some(IntT(_)), None | Some(IntT(_))) => baseType case (GhostSliceT(_), None | Some(IntT(_)), None | Some(IntT(_)), None | Some(IntT(_))) => baseType case (StringT, None | Some(IntT(_)), None | Some(IntT(_)), None) => baseType @@ -984,6 +993,9 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => case PredT(fArgs) => fArgs.lift(index) case t => violation(s"predicate expression instance has base $base with unsupported type $t") } + case Some(ap.Conversion(t, e)) => + assert(expr == e) + Some(typeSymbType(t)) case _ => None } @@ -1135,7 +1147,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => underlyingType(exprType(expr.exp)) match { case _: ArrayT | _: SliceT | _: GhostSliceT | StringT | _: VariadicT | _: MapT => INT_TYPE case ActualPointerT(_: ArrayT) => INT_TYPE - case _: SequenceT | _: SetT | _: MultisetT | _: MathMapT | _: AdtT => UNTYPED_INT_CONST + case _: SequenceT | _: SetT | _: MultisetT | _: MathMapT | _: AdtT => GhostIntegerT case t => violation(s"unexpected argument ${expr.exp} of type $t passed to len") } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala index c6c7666b9..e6bf7fad5 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala @@ -183,7 +183,8 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl => }) case expr : PSequenceExp => expr match { - case PRangeSequence(low, high) => isExpr(low).out ++ isExpr(high).out ++ { + case PRangeSequence(low, high) => + isExpr(low).out ++ isExpr(high).out ++ { val lowT = exprType(low) val highT = exprType(high) error(low, s"expected an integer, but got $lowT", !lowT.isInstanceOf[IntT]) ++ diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostTypeTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostTypeTyping.scala index 0c107ceaf..d7569ffdc 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostTypeTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostTypeTyping.scala @@ -16,6 +16,7 @@ import viper.gobra.util.Violation trait GhostTypeTyping extends BaseTyping { this : TypeInfoImpl => private[typing] def wellDefGhostType(typ : PGhostType) : Messages = typ match { + case _: PGhostIntegerType => noMessages case _: PPermissionType => noMessages case PSequenceType(elem) => isType(elem).out case PSetType(elem) => isType(elem).out @@ -40,6 +41,7 @@ trait GhostTypeTyping extends BaseTyping { this : TypeInfoImpl => private[typing] def ghostTypeSymbType(typ : PGhostType) : Type = typ match { case PPermissionType() => PermissionT + case PGhostIntegerType() => GhostIntegerT case PSequenceType(elem) => SequenceT(typeSymbType(elem)) case PSetType(elem) => SetT(typeSymbType(elem)) case PMultisetType(elem) => MultisetT(typeSymbType(elem)) diff --git a/src/main/scala/viper/gobra/translator/context/DfltTranslatorConfig.scala b/src/main/scala/viper/gobra/translator/context/DfltTranslatorConfig.scala index 44d0322a1..8ed63b31d 100644 --- a/src/main/scala/viper/gobra/translator/context/DfltTranslatorConfig.scala +++ b/src/main/scala/viper/gobra/translator/context/DfltTranslatorConfig.scala @@ -66,10 +66,10 @@ class DfltTranslatorConfig( val typeEncoding: TypeEncoding = new FinalTypeEncoding( new SafeTypeEncodingCombiner(Vector( - new BoolEncoding, new IntEncoding, new PermissionEncoding, + new BoolEncoding, new StringEncoding, new IntEncoding, new PermissionEncoding, new PointerEncoding, new StructEncoding, arrayEncoding, new ClosureEncoding(config), new InterfaceEncoding, new SequenceEncoding, new SetEncoding, new OptionEncoding, new DomainEncoding, new AdtEncoding, - new SliceEncoding(arrayEncoding), new PredEncoding, new ChannelEncoding, new StringEncoding, + new SliceEncoding(arrayEncoding), new PredEncoding, new ChannelEncoding, new MapEncoding, new MathematicalMapEncoding, new FloatEncoding, new AssertionEncoding, new CallEncoding, new MemoryEncoding, new ControlEncoding, new TerminationEncoding, new BuiltInEncoding, new OutlineEncoding, new DeferEncoding, diff --git a/src/main/scala/viper/gobra/translator/encodings/FloatEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/FloatEncoding.scala index 76ee45196..cadba2250 100644 --- a/src/main/scala/viper/gobra/translator/encodings/FloatEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/FloatEncoding.scala @@ -74,10 +74,24 @@ class FloatEncoding extends LeafTypeEncoding { for { lE <- goE(l); rE <- goE(r) } yield withSrc(vpr.FuncApp(divFloat32, Seq(lE, rE)), div) case div @ in.Div(l :: ctx.Float64(), r :: ctx.Float64()) => for { lE <- goE(l); rE <- goE(r) } yield withSrc(vpr.FuncApp(divFloat64, Seq(lE, rE)), div) - case conv@in.Conversion(in.Float32T(_), expr :: ctx.Int()) => - for { e <- goE(expr) } yield withSrc(vpr.FuncApp(fromIntTo32, Seq(e)), conv) - case conv@in.Conversion(in.Float64T(_), expr :: ctx.Int()) => - for { e <- goE(expr) } yield withSrc(vpr.FuncApp(fromIntTo64, Seq(e)), conv) + case conv@in.Conversion(in.Float32T(_), expr :: ctx.Int(_)) => + for { + e <- goE(expr) + eKind = expr.typ match { + case in.IntT(_, kind) => kind + case _ => ??? + } + arg = IntEncodingGenerator.domainToIntFuncApp(eKind)(e)(e.pos, e.info, e.errT) + } yield withSrc(vpr.FuncApp(fromIntTo32, Seq(arg)), conv) + case conv@in.Conversion(in.Float64T(_), expr :: ctx.Int(_)) => + for { + e <- goE(expr) + eKind = expr.typ match { + case in.IntT(_, kind) => kind + case _ => ??? + } + arg = IntEncodingGenerator.domainToIntFuncApp(eKind)(e)(e.pos, e.info, e.errT) + } yield withSrc(vpr.FuncApp(fromIntTo64, Seq(arg)), conv) case conv@in.Conversion(in.IntT(_, _), expr :: ctx.Float32()) => for { e <- goE(expr) } yield withSrc(vpr.FuncApp(from32ToInt, Seq(e)), conv) case conv@in.Conversion(in.IntT(_, _), expr :: ctx.Float64()) => diff --git a/src/main/scala/viper/gobra/translator/encodings/IntEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/IntEncoding.scala index 2f7748897..4dfd32f08 100644 --- a/src/main/scala/viper/gobra/translator/encodings/IntEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/IntEncoding.scala @@ -12,39 +12,44 @@ import viper.gobra.reporting.BackTranslator.RichErrorMessage import viper.gobra.reporting.{ShiftPreconditionError, Source} import viper.gobra.theory.Addressability.{Exclusive, Shared} import viper.gobra.translator.Names -import viper.gobra.translator.encodings.combinators.LeafTypeEncoding import viper.gobra.translator.context.Context +import viper.gobra.translator.encodings.combinators.LeafTypeEncoding +import viper.gobra.translator.util.DomainGeneratorWithoutContext import viper.gobra.translator.util.ViperWriter.CodeWriter +import viper.gobra.util.TypeBounds +import viper.gobra.util.TypeBounds.{BoundedIntegerKind, IntegerKind} +import viper.silver.ast.{Domain, ErrorTrafo, Info, NoInfo, NoPosition, NoTrafos, Position} +import viper.silver.plugin.standard.termination import viper.silver.verifier.{errors => err} import viper.silver.{ast => vpr} -import viper.silver.plugin.standard.termination +import scala.collection.immutable.Seq + +// TODO: parameterize this with the config to define default int type class IntEncoding extends LeafTypeEncoding { import viper.gobra.translator.util.TypePatterns._ import viper.gobra.translator.util.ViperWriter.CodeLevel._ - private var isUsedBitAnd: Boolean = false - private var isUsedBitOr: Boolean = false - private var isUsedBitXor: Boolean = false - private var isUsedBitClear: Boolean = false private var isUsedLeftShift: Boolean = false private var isUsedRightShift: Boolean = false - private var isUsedBitNeg: Boolean = false - private var isUsedGoIntDiv: Boolean = false - private var isUsedGoIntMod: Boolean = false /** * Translates a type into a Viper type. */ override def typ(ctx: Context): in.Type ==> vpr.Type = { - case ctx.Int() / m => + case ctx.Int(kind) / m => m match { - case Exclusive => vpr.Int + case Exclusive => IntEncodingGenerator(Vector.empty, kind) case Shared => vpr.Ref } } + + // TODO: make pres conditional on whether the overflow flag is enabled or not + + + // TODO: explain our encoding is resilient to the type-checker imprecision /** * Encodes expressions as values that do not occupy some identifiable location in memory. * @@ -54,6 +59,7 @@ class IntEncoding extends LeafTypeEncoding { override def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = { def goE(x: in.Expr): CodeWriter[vpr.Exp] = ctx.expression(x) + /* def handleShift(shiftFunc: vpr.Function)(left: in.Expr, right: in.Expr): (vpr.Position, vpr.Info, vpr.ErrorTrafo) => CodeWriter[vpr.Exp] = { case (pos, info, errT) => for { @@ -67,93 +73,215 @@ class IntEncoding extends LeafTypeEncoding { } yield app } - default(super.expression(ctx)){ - case (e: in.DfltVal) :: ctx.Int() / Exclusive => unit(withSrc(vpr.IntLit(0), e)) - case lit: in.IntLit => unit(withSrc(vpr.IntLit(lit.v), lit)) + */ - case e@ in.Add(l, r) :: ctx.Int() => for {vl <- goE(l); vr <- goE(r)} yield withSrc(vpr.Add(vl, vr), e) - case e@ in.Sub(l, r) :: ctx.Int() => for {vl <- goE(l); vr <- goE(r)} yield withSrc(vpr.Sub(vl, vr), e) - case e@ in.Mul(l, r) :: ctx.Int() => for {vl <- goE(l); vr <- goE(r)} yield withSrc(vpr.Mul(vl, vr), e) - case e@ in.Mod(l, r) :: ctx.Int() => + default(super.expression(ctx)){ + case (e: in.DfltVal) :: ctx.Int(kind) / Exclusive => + unit(withSrc(IntEncodingGenerator.intToDomainFuncApp(kind)(vpr.IntLit(BigInt(0))()), e)) + case lit: in.IntLit => + unit(withSrc(IntEncodingGenerator.intToDomainFuncApp(lit.kind)(vpr.IntLit(lit.v)()), lit)) + case e@ in.Add(l :: ctx.Int(kindL), r :: ctx.Int(kindR)) :: ctx.Int(kind) => + for { + vl <- goE(l) + vr <- goE(r) + // TODO: explain the use of left and right + left = withSrc(IntEncodingGenerator.intToDomainFuncApp(kind)( + withSrc(IntEncodingGenerator.domainToIntFuncApp(kindL)(vl), l) + ), l) + right = withSrc(IntEncodingGenerator.intToDomainFuncApp(kind)( + withSrc(IntEncodingGenerator.domainToIntFuncApp(kindR)(vr), r) + ), r) + } yield withSrc(IntEncodingGenerator.addFuncApp(kind)(left, right), e) + case e@ in.Sub(l :: ctx.Int(kindL), r :: ctx.Int(kindR)) :: ctx.Int(kind) => + for { + vl <- goE(l) + vr <- goE(r) + // TODO: explain the use of left and right + left = withSrc(IntEncodingGenerator.intToDomainFuncApp(kind)( + withSrc(IntEncodingGenerator.domainToIntFuncApp(kindL)(vl), l) + ), l) + right = withSrc(IntEncodingGenerator.intToDomainFuncApp(kind)( + withSrc(IntEncodingGenerator.domainToIntFuncApp(kindR)(vr), r) + ), r) + } yield withSrc(IntEncodingGenerator.subFuncApp(kind)(left, right), e) + case e@ in.Mul(l :: ctx.Int(kindL) , r :: ctx.Int(kindR)) :: ctx.Int(kind) => + for { + vl <- goE(l) + vr <- goE(r) + // TODO: explain the use of left and right + left = withSrc(IntEncodingGenerator.intToDomainFuncApp(kind)( + withSrc(IntEncodingGenerator.domainToIntFuncApp(kindL)(vl), l) + ), l) + right = withSrc(IntEncodingGenerator.intToDomainFuncApp(kind)( + withSrc(IntEncodingGenerator.domainToIntFuncApp(kindR)(vr), r) + ), r) + } yield withSrc(IntEncodingGenerator.mulFuncApp(kind)(left, right), e) + case e@ in.Mod(l :: ctx.Int(kindL), r :: ctx.Int(kindR)) :: ctx.Int(kind) => // We currently implement our own modulo algorithm to mimic what Go does. The default modulo implementation in // Viper does not match Go's semantics. Check https://github.com/viperproject/gobra/issues/858 and // https://github.com/viperproject/silver/issues/297 - for {vl <- goE(l); vr <- goE(r)} yield withSrc(vpr.FuncApp(goIntMod, Seq(vl, vr)), e) - case e@ in.Div(l, r) :: ctx.Int() => + for { + vl <- goE(l) + vr <- goE(r) + // TODO: explain the use of left and right + left = withSrc(IntEncodingGenerator.intToDomainFuncApp(kind)( + withSrc(IntEncodingGenerator.domainToIntFuncApp(kindL)(vl), l) + ), l) + right = withSrc(IntEncodingGenerator.intToDomainFuncApp(kind)( + withSrc(IntEncodingGenerator.domainToIntFuncApp(kindR)(vr), r) + ), r) + } yield withSrc(IntEncodingGenerator.modFuncApp(kind)(left, right), e) + case e@ in.Div(l :: ctx.Int(kindL), r :: ctx.Int(kindR)) :: ctx.Int(kind) => // We currently implement our own division algorithm to mimic what Go does. The default division implementation in // Viper does not match Go's semantics. Check https://github.com/viperproject/gobra/issues/858 and // https://github.com/viperproject/silver/issues/297 - for {vl <- goE(l); vr <- goE(r)} yield withSrc(vpr.FuncApp(goIntDiv, Seq(vl, vr)), e) - case e@ in.BitAnd(l, r) :: ctx.Int() => for {vl <- goE(l); vr <- goE(r)} yield withSrc(vpr.FuncApp(bitwiseAnd, Seq(vl, vr)), e) - case e@ in.BitOr(l, r) :: ctx.Int() => for {vl <- goE(l); vr <- goE(r)} yield withSrc(vpr.FuncApp(bitwiseOr, Seq(vl, vr)), e) - case e@ in.BitXor(l, r) :: ctx.Int() => for {vl <- goE(l); vr <- goE(r)} yield withSrc(vpr.FuncApp(bitwiseXor, Seq(vl, vr)), e) - case e@ in.BitClear(l, r) :: ctx.Int() => for {vl <- goE(l); vr <- goE(r)} yield withSrc(vpr.FuncApp(bitClear, Seq(vl, vr)), e) - case e@ in.ShiftLeft(l, r) :: ctx.Int() => withSrc(handleShift(shiftLeft)(l, r), e) - case e@ in.ShiftRight(l, r) :: ctx.Int() => withSrc(handleShift(shiftRight)(l, r), e) - case e@ in.BitNeg(exp) :: ctx.Int() => for {ve <- goE(exp)} yield withSrc(vpr.FuncApp(bitwiseNegation, Seq(ve)), e) + for { + vl <- goE(l) + vr <- goE(r) + // TODO: explain the use of left and right + left = withSrc(IntEncodingGenerator.intToDomainFuncApp(kind)( + withSrc(IntEncodingGenerator.domainToIntFuncApp(kindL)(vl), l) + ), l) + right = withSrc(IntEncodingGenerator.intToDomainFuncApp(kind)( + withSrc(IntEncodingGenerator.domainToIntFuncApp(kindR)(vr), r) + ), r) + } yield withSrc(IntEncodingGenerator.divFuncApp(kind)(left, right), e) + case e@ in.BitAnd(l :: ctx.Int(kindL), r :: ctx.Int(kindR)) :: ctx.Int(kind) => + for { + vl <- goE(l) + vr <- goE(r) + // TODO: explain the use of left and right + left = withSrc(IntEncodingGenerator.intToDomainFuncApp(kind)( + withSrc(IntEncodingGenerator.domainToIntFuncApp(kindL)(vl), l) + ), l) + right = withSrc(IntEncodingGenerator.intToDomainFuncApp(kind)( + withSrc(IntEncodingGenerator.domainToIntFuncApp(kindR)(vr), r) + ), r) + } yield withSrc(IntEncodingGenerator.bitAndFuncApp(kind)(left, right), e) + case e@ in.BitOr(l :: ctx.Int(kindL), r :: ctx.Int(kindR)) :: ctx.Int(kind) => + for { + vl <- goE(l) + vr <- goE(r) + // TODO: explain the use of left and right + left = withSrc(IntEncodingGenerator.intToDomainFuncApp(kind)( + withSrc(IntEncodingGenerator.domainToIntFuncApp(kindL)(vl), l) + ), l) + right = withSrc(IntEncodingGenerator.intToDomainFuncApp(kind)( + withSrc(IntEncodingGenerator.domainToIntFuncApp(kindR)(vr), r) + ), r) + } yield withSrc(IntEncodingGenerator.bitOrFuncApp(kind)(left, right), e) + case e@ in.BitXor(l :: ctx.Int(kindL), r :: ctx.Int(kindR)) :: ctx.Int(kind) => + for { + vl <- goE(l) + vr <- goE(r) + // TODO: explain the use of left and right + left = withSrc(IntEncodingGenerator.intToDomainFuncApp(kind)( + withSrc(IntEncodingGenerator.domainToIntFuncApp(kindL)(vl), l) + ), l) + right = withSrc(IntEncodingGenerator.intToDomainFuncApp(kind)( + withSrc(IntEncodingGenerator.domainToIntFuncApp(kindR)(vr), r) + ), r) + } yield withSrc(IntEncodingGenerator.bitXorFuncApp(kind)(left, right), e) + case e@ in.BitClear(l :: ctx.Int(kindL), r :: ctx.Int(kindR)) :: ctx.Int(kind) => + for { + vl <- goE(l) + vr <- goE(r) + // TODO: explain the use of left and right + left = withSrc(IntEncodingGenerator.intToDomainFuncApp(kind)( + withSrc(IntEncodingGenerator.domainToIntFuncApp(kindL)(vl), l) + ), l) + right = withSrc(IntEncodingGenerator.intToDomainFuncApp(kind)( + withSrc(IntEncodingGenerator.domainToIntFuncApp(kindR)(vr), r) + ), r) + } yield withSrc(IntEncodingGenerator.bitClearFuncApp(kind)(left, right), e) + case e@ in.BitNeg(exp :: ctx.Int(kind)) => + for { expD <- goE(exp) } yield withSrc(IntEncodingGenerator.bitNegFuncApp(kind)(expD), e) + case e@ in.ShiftLeft(l :: ctx.Int(kind1), r :: ctx.Int(kind2)) => + for { + vl <- goE(l) + vr <- goE(r) + } yield withSrc(IntEncodingGenerator.bitShiftLeftFuncApp(kind1, kind2)(vl, vr), e) + // withSrc(handleShift(shiftLeft)(l, r), e) + // case e@ in.ShiftRight(l, r) :: ctx.Int(kind) => withSrc(handleShift(shiftRight)(l, r), e) + case e@ in.ShiftRight(l :: ctx.Int(kind1), r :: ctx.Int(kind2)) => + for { + vl <- goE(l) + vr <- goE(r) + } yield withSrc(IntEncodingGenerator.bitShiftRightFuncApp(kind1, kind2)(vl, vr), e) + case in.Conversion(t, expr) if isNumericType(t)(ctx) && isNumericType(expr.typ)(ctx) => + val dstType = ctx.underlyingType(t) + val dstKind = dstType match { + case in.IntT(_, kind) => kind + case _ => ??? + } + val srcType = ctx.underlyingType(expr.typ) + val srcKind = srcType match { + case in.IntT(_, kind) => kind + case _ => ??? + } + for { + e <- goE(expr) + intValue = withSrc(IntEncodingGenerator.domainToIntFuncApp(srcKind)(e), expr) + newDomainValue = withSrc(IntEncodingGenerator.intToDomainFuncApp(dstKind)(intValue), expr) + } yield newDomainValue + case n@in.LessCmp(l :: ctx.Int(kindL), r :: ctx.Int(kindR)) => + for { + vl <- ctx.expression(l) + vr <- ctx.expression(r) + numl = withSrc(IntEncodingGenerator.domainToIntFuncApp(kindL)(vl), l) + numr = withSrc(IntEncodingGenerator.domainToIntFuncApp(kindR)(vr), r) + } yield withSrc(vpr.LtCmp(numl, numr), n) + case n@in.AtMostCmp(l :: ctx.Int(kindL), r :: ctx.Int(kindR)) => + for { + vl <- ctx.expression(l) + vr <- ctx.expression(r) + numl = withSrc(IntEncodingGenerator.domainToIntFuncApp(kindL)(vl), l) + numr = withSrc(IntEncodingGenerator.domainToIntFuncApp(kindR)(vr), r) + } yield withSrc(vpr.LeCmp(numl, numr), n) + case n@in.GreaterCmp(l :: ctx.Int(kindL), r :: ctx.Int(kindR)) => + for { + vl <- ctx.expression(l) + vr <- ctx.expression(r) + numl = withSrc(IntEncodingGenerator.domainToIntFuncApp(kindL)(vl), l) + numr = withSrc(IntEncodingGenerator.domainToIntFuncApp(kindR)(vr), r) + } yield withSrc(vpr.GtCmp(numl, numr), n) + case n@in.AtLeastCmp(l :: ctx.Int(kindL), r :: ctx.Int(kindR)) => + for { + vl <- ctx.expression(l) + vr <- ctx.expression(r) + numl = withSrc(IntEncodingGenerator.domainToIntFuncApp(kindL)(vl), l) + numr = withSrc(IntEncodingGenerator.domainToIntFuncApp(kindR)(vr), r) + } yield withSrc(vpr.GeCmp(numl, numr), n) + case n@in.UneqCmp(l :: ctx.Int(kindL), r :: ctx.Int(kindR)) => + for { + vl <- ctx.expression(l) + vr <- ctx.expression(r) + numl = withSrc(IntEncodingGenerator.domainToIntFuncApp(kindL)(vl), l) + numr = withSrc(IntEncodingGenerator.domainToIntFuncApp(kindR)(vr), r) + } yield withSrc(vpr.NeCmp(numl, numr), n) + case n@in.GhostUneqCmp(l :: ctx.Int(kindL), r :: ctx.Int(kindR)) => + for { + vl <- ctx.expression(l) + vr <- ctx.expression(r) + numl = withSrc(IntEncodingGenerator.domainToIntFuncApp(kindL)(vl), l) + numr = withSrc(IntEncodingGenerator.domainToIntFuncApp(kindR)(vr), r) + } yield withSrc(vpr.NeCmp(numl, numr), n) } } + private def isNumericType(t: in.Type)(ctx: Context): Boolean = { + val ut = ctx.underlyingType(t) + ut.isInstanceOf[in.IntT] + } + override def finalize(addMemberFn: vpr.Member => Unit): Unit = { - if(isUsedBitAnd) { addMemberFn(bitwiseAnd) } - if(isUsedBitOr) { addMemberFn(bitwiseOr) } - if(isUsedBitXor) { addMemberFn(bitwiseXor) } - if(isUsedBitClear) { addMemberFn(bitClear) } + IntEncodingGenerator.finalize(addMemberFn) + // TODO: rework the following if(isUsedLeftShift) { addMemberFn(shiftLeft) } if(isUsedRightShift) { addMemberFn(shiftRight) } - if(isUsedBitNeg) { addMemberFn(bitwiseNegation) } - if(isUsedGoIntMod) { addMemberFn(goIntMod) } - if(isUsedGoIntDiv) { addMemberFn(goIntDiv) } } /* Bitwise Operations */ - private lazy val bitwiseAnd: vpr.Function = { - isUsedBitAnd = true - vpr.Function( - name = Names.bitwiseAnd, - formalArgs = Seq(vpr.LocalVarDecl("left", vpr.Int)(), vpr.LocalVarDecl("right", vpr.Int)()), - typ = vpr.Int, - pres = Seq(termination.DecreasesWildcard(None)()), - posts = Seq.empty, - body = None - )() - } - - private lazy val bitwiseOr: vpr.Function = { - isUsedBitOr = true - vpr.Function( - name = Names.bitwiseOr, - formalArgs = Seq(vpr.LocalVarDecl("left", vpr.Int)(), vpr.LocalVarDecl("right", vpr.Int)()), - typ = vpr.Int, - pres = Seq(termination.DecreasesWildcard(None)()), - posts = Seq.empty, - body = None - )() - } - - private lazy val bitwiseXor: vpr.Function = { - isUsedBitXor = true - vpr.Function( - name = Names.bitwiseXor, - formalArgs = Seq(vpr.LocalVarDecl("left", vpr.Int)(), vpr.LocalVarDecl("right", vpr.Int)()), - typ = vpr.Int, - pres = Seq(termination.DecreasesWildcard(None)()), - posts = Seq.empty, - body = None - )() - } - - private lazy val bitClear: vpr.Function = { - isUsedBitClear = true - vpr.Function( - name = Names.bitClear, - formalArgs = Seq(vpr.LocalVarDecl("left", vpr.Int)(), vpr.LocalVarDecl("right", vpr.Int)()), - typ = vpr.Int, - pres = Seq(termination.DecreasesWildcard(None)()), - posts = Seq.empty, - body = None - )() - } private lazy val shiftLeft: vpr.Function = { isUsedLeftShift = true @@ -184,85 +312,591 @@ class IntEncoding extends LeafTypeEncoding { body = None )() } +} - private lazy val bitwiseNegation: vpr.Function = { - isUsedBitNeg = true - vpr.Function( - name = Names.bitwiseNeg, - formalArgs = Seq(vpr.LocalVarDecl("exp", vpr.Int)()), +case object IntEncodingGenerator extends DomainGeneratorWithoutContext[IntegerKind] { + val intKind: TypeBounds.IntegerKind = TypeBounds.DefaultInt + val intType: vpr.Type = domainType(intKind) + + val integerKind: TypeBounds.IntegerKind = TypeBounds.UnboundedInteger + val integerType: vpr.Type = domainType(integerKind) + + // view operations + private var intToDomainFuncs: Map[IntegerKind, vpr.Function] = Map.empty + private var domainToIntFuncs: Map[IntegerKind, vpr.Function] = Map.empty + // arith operations + private var addFuncs: Map[IntegerKind, vpr.Function] = Map.empty + private var subFuncs: Map[IntegerKind, vpr.Function] = Map.empty + private var mulFuncs: Map[IntegerKind, vpr.Function] = Map.empty + private var divFuncs: Map[IntegerKind, vpr.Function] = Map.empty + private var modFuncs: Map[IntegerKind, vpr.Function] = Map.empty + // bitwise operations + private var bitAndFuncs: Map[IntegerKind, vpr.Function] = Map.empty + private var bitOrFuncs: Map[IntegerKind, vpr.Function] = Map.empty + private var bitXorFuncs: Map[IntegerKind, vpr.Function] = Map.empty + private var bitClearFuncs: Map[IntegerKind, vpr.Function] = Map.empty + private var bitNegFuncs: Map[IntegerKind, vpr.Function] = Map.empty + // shifts + private var bitShiftLeftFuncs: Map[(IntegerKind, IntegerKind), vpr.Function] = Map.empty + private var bitShiftRightFuncs: Map[(IntegerKind, IntegerKind), vpr.Function] = Map.empty + // + private var deferedIntToDomainFuncs: Set[IntegerKind] = Set.empty + + override def finalize(addMemberFn: vpr.Member => Unit): Unit = { + super.finalize(addMemberFn) + intToDomainFuncs.values.foreach(addMemberFn) + deferedIntToDomainFuncs.foreach { x => + if (!intToDomainFuncs.contains(x)) { + addMemberFn(intToDomainFunc(x)) + } + } + domainToIntFuncs.values.foreach(addMemberFn) + addFuncs.values.foreach(addMemberFn) + subFuncs.values.foreach(addMemberFn) + mulFuncs.values.foreach(addMemberFn) + divFuncs.values.foreach(addMemberFn) + modFuncs.values.foreach(addMemberFn) + bitAndFuncs.values.foreach(addMemberFn) + bitOrFuncs.values.foreach(addMemberFn) + bitXorFuncs.values.foreach(addMemberFn) + bitClearFuncs.values.foreach(addMemberFn) + bitNegFuncs.values.foreach(addMemberFn) + bitShiftLeftFuncs.values.foreach(addMemberFn) + bitShiftRightFuncs.values.foreach(addMemberFn) + + } + + override def genDomain(x: IntegerKind): Domain = { + val kindToDomainName = s"IntDomain${x.name}" + vpr.Domain(name = kindToDomainName, functions = Seq.empty, axioms = Seq.empty)() + } + + def domainType(x: IntegerKind): vpr.Type = { + this(Vector.empty, x) + } + + def intToDomainFuncApp(x: IntegerKind)(e: vpr.Exp) + (pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): vpr.Exp = { + val funcname = intToDomainFunc(x).name + vpr.FuncApp(funcname = funcname, args = Seq(e))(pos, info, typ = domainType(x), errT) + } + + private def intToDomainFunc(x: IntegerKind): vpr.Function = { + intToDomainFuncs.get(x) match { + case Some(f) => f + case _ => + val inputVarDecl = vpr.LocalVarDecl("x", vpr.Int)() + val resType = domainType(x) + val pre = x match { + case b: BoundedIntegerKind => + vpr.And( + vpr.LeCmp(vpr.IntLit(b.lower)(), inputVarDecl.localVar)(), + vpr.LeCmp(inputVarDecl.localVar, vpr.IntLit(b.upper)())() + )() + case _ => vpr.TrueLit()() + } + val post = vpr.EqCmp(domainToIntFuncApp(x)(vpr.Result(resType)())(), inputVarDecl.localVar)() + val res = vpr.Function( + name = s"intToDomain${x.name}", + formalArgs = Seq(inputVarDecl), + typ = resType, + pres = Seq(pre, termination.DecreasesWildcard(None)()), + posts = Seq(post), + body = None + )() + intToDomainFuncs += x -> res + res + } + } + + def domainToIntFuncApp(x: IntegerKind)(e: vpr.Exp) + (pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): vpr.Exp = { + val funcname = domainToIntFunc(x).name + vpr.FuncApp(funcname = funcname, args = Seq(e))(pos, info, typ = vpr.Int, errT) + } + + private def domainToIntFunc(x: IntegerKind): vpr.Function = { + val inputVarDecl = vpr.LocalVarDecl("x", domainType(x))() + val post1 = x match { + case b: BoundedIntegerKind => + vpr.And( + vpr.LeCmp(vpr.IntLit(b.lower)(), vpr.Result(vpr.Int)())(), + vpr.LeCmp(vpr.Result(vpr.Int)(), vpr.IntLit(b.upper)())() + )() + case _ => vpr.TrueLit()() + } + deferedIntToDomainFuncs += x + // explicit FuncApp construction here instead of call to intToDomainFuncApp to avoid creating a cycle between + // that function and domainToIntFuncApp + val intToDomainApp = + vpr.FuncApp(funcname = s"intToDomain${x.name}", args = Seq(vpr.Result(vpr.Int)()))(NoPosition, NoInfo, typ = vpr.Int, NoTrafos) + val post2 = vpr.EqCmp(intToDomainApp, inputVarDecl.localVar)() + val res = vpr.Function( + name = s"domainToInt${x.name}", + formalArgs = Seq(inputVarDecl), typ = vpr.Int, pres = Seq(termination.DecreasesWildcard(None)()), - posts = Seq.empty, + posts = Seq(post1, post2), body = None )() + domainToIntFuncs += x -> res + res + } + + def addFuncApp(x: IntegerKind)(e1: vpr.Exp, e2: vpr.Exp) + (pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): vpr.Exp = { + val funcname = addFunc(x).name + vpr.FuncApp(funcname = funcname, args = Seq(e1, e2))(pos, info, typ = domainType(x), errT) } + private def addFunc(x: IntegerKind): vpr.Function = { + addFuncs.get(x) match { + case Some(f) => f + case _ => + val domainT = domainType(x) + val inputVar1Decl = vpr.LocalVarDecl("x", domainT)() + val inputVar2Decl = vpr.LocalVarDecl("y", domainT)() + val pre = x match { + case b: BoundedIntegerKind => + val sumExpr = vpr.Add( + domainToIntFuncApp(x)(inputVar1Decl.localVar)(), + domainToIntFuncApp(x)(inputVar2Decl.localVar)(), + )() + vpr.And(vpr.LeCmp(vpr.IntLit(b.lower)(), sumExpr)(), vpr.LeCmp(sumExpr, vpr.IntLit(b.upper)())())() + case _ => vpr.TrueLit()() + } + val body = + intToDomainFuncApp(x)(vpr.Add( + domainToIntFuncApp(x)(inputVar1Decl.localVar)(), + domainToIntFuncApp(x)(inputVar2Decl.localVar)() + )())() + val res = vpr.Function( + name = s"add${x.name}", + formalArgs = Seq(inputVar1Decl, inputVar2Decl), + typ = domainT, + pres = Seq(pre, termination.DecreasesWildcard(None)()), + posts = Seq(), + body = Some(body) + )() + addFuncs += x -> res + res + } + } + + def subFuncApp(x: IntegerKind)(e1: vpr.Exp, e2: vpr.Exp) + (pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): vpr.Exp = { + val funcname = subFunc(x).name + vpr.FuncApp(funcname = funcname, args = Seq(e1, e2))(pos, info, typ = domainType(x), errT) + } + + private def subFunc(x: IntegerKind): vpr.Function = { + subFuncs.get(x) match { + case Some(f) => f + case _ => + val domainT = domainType(x) + val inputVar1Decl = vpr.LocalVarDecl("x", domainT)() + val inputVar2Decl = vpr.LocalVarDecl("y", domainT)() + val pre = x match { + case b: BoundedIntegerKind => + val sumExpr = vpr.Sub( + domainToIntFuncApp(x)(inputVar1Decl.localVar)(), + domainToIntFuncApp(x)(inputVar2Decl.localVar)(), + )() + vpr.And(vpr.LeCmp(vpr.IntLit(b.lower)(), sumExpr)(), vpr.LeCmp(sumExpr, vpr.IntLit(b.upper)())())() + case _ => vpr.TrueLit()() + } + val body = + intToDomainFuncApp(x)( + vpr.Sub( + domainToIntFuncApp(x)(inputVar1Decl.localVar)(), + domainToIntFuncApp(x)(inputVar2Decl.localVar)() + )() + )() + val res = vpr.Function( + name = s"sub${x.name}", + formalArgs = Seq(inputVar1Decl, inputVar2Decl), + typ = domainT, + pres = Seq(pre, termination.DecreasesWildcard(None)()), + posts = Seq(), + body = Some(body) + )() + subFuncs += x -> res + res + } + } + + def mulFuncApp(x: IntegerKind)(e1: vpr.Exp, e2: vpr.Exp) + (pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): vpr.Exp = { + val funcname = mulFunc(x).name + vpr.FuncApp(funcname = funcname, args = Seq(e1, e2))(pos, info, typ = domainType(x), errT) + } + + private def mulFunc(x: IntegerKind): vpr.Function = { + mulFuncs.get(x) match { + case Some(f) => f + case _ => + val domainT = domainType(x) + val inputVar1Decl = vpr.LocalVarDecl("x", domainT)() + val inputVar2Decl = vpr.LocalVarDecl("y", domainT)() + val pre = x match { + case b: BoundedIntegerKind => + val sumExpr = vpr.Mul( + domainToIntFuncApp(x)(inputVar1Decl.localVar)(), + domainToIntFuncApp(x)(inputVar2Decl.localVar)(), + )() + vpr.And(vpr.LeCmp(vpr.IntLit(b.lower)(), sumExpr)(), vpr.LeCmp(sumExpr, vpr.IntLit(b.upper)())())() + case _ => vpr.TrueLit()() + } + val body = intToDomainFuncApp(x)( + vpr.Mul( + domainToIntFuncApp(x)(inputVar1Decl.localVar)(), + domainToIntFuncApp(x)(inputVar2Decl.localVar)() + )() + )() + val res = vpr.Function( + name = s"mul${x.name}", + formalArgs = Seq(inputVar1Decl, inputVar2Decl), + typ = domainT, + pres = Seq(pre, termination.DecreasesWildcard(None)()), + posts = Seq(), + body = Some(body) + )() + mulFuncs += x -> res + res + } + } + + def divFuncApp(x: IntegerKind)(e1: vpr.Exp, e2: vpr.Exp)(pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): vpr.Exp = { + val funcname = divFunc(x).name + vpr.FuncApp(funcname = funcname, args = Seq(e1, e2))(pos, info, typ = domainType(x), errT) + } + + // TODO: update specs /** * Generates the following viper function that captures the semantics of the '/' operator in Go: - * function goIntDiv(l: Int, r: Int): Int - * requires r != 0 - * decreases _ - * { + * function goIntDiv(l: Int, r: Int): Int + * requires r != 0 + * decreases _ + * { * (0 <= l ? l \ r : -(-l \ r)) - * } + * } */ - private lazy val goIntDiv: vpr.Function = { - isUsedGoIntDiv = true - val lDecl = vpr.LocalVarDecl("l", vpr.Int)() - val rDecl = vpr.LocalVarDecl("r", vpr.Int)() - val l = lDecl.localVar - val r = rDecl.localVar - val zero = vpr.IntLit(0)() - val rNotZero = vpr.NeCmp(r, zero)() - vpr.Function( - name = Names.intDiv, - formalArgs = Seq(lDecl, rDecl), - typ = vpr.Int, - pres = Seq(rNotZero, termination.DecreasesWildcard(None)()), - posts = Seq.empty, - body = Some( - // 0 <= l ? l \ r : -((-l) \ r) - vpr.CondExp( - cond = vpr.LeCmp(zero, l)(), - thn = vpr.Div(l, r)(), - els = vpr.Minus(vpr.Div(vpr.Minus(l)(), r)())() + private def divFunc(x: IntegerKind): vpr.Function = { + divFuncs.get(x) match { + case Some(f) => f + case _ => + val domainT = domainType(x) + val inputVar1Decl = vpr.LocalVarDecl("x", domainT)() + val inputVar2Decl = vpr.LocalVarDecl("y", domainT)() + val zero = vpr.IntLit(0)() + val pre = vpr.NeCmp(domainToIntFuncApp(x)(inputVar2Decl.localVar)(), zero)() + val post = x match { + case b: BoundedIntegerKind => + val result = domainToIntFuncApp(x)(vpr.Result(domainT)())() + vpr.And(vpr.LeCmp(vpr.IntLit(b.lower)(), result)(), vpr.LeCmp(result, vpr.IntLit(b.upper)())())() + case _ => vpr.TrueLit()() + } + val body = { + val l = domainToIntFuncApp(x)(inputVar1Decl.localVar)() + val r = domainToIntFuncApp(x)(inputVar2Decl.localVar)() + // 0 <= l ? l \ r : -((-l) \ r) + intToDomainFuncApp(x)( + vpr.CondExp( + cond = vpr.LeCmp(zero, l)(), + thn = vpr.Div(l, r)(), + els = vpr.Minus(vpr.Div(vpr.Minus(l)(), r)())() + )() + )() + } + val res = vpr.Function( + name = s"div${x.name}", + formalArgs = Seq(inputVar1Decl, inputVar2Decl), + typ = domainT, + pres = Seq(pre, termination.DecreasesWildcard(None)()), + posts = Seq(post), + body = Some(body) )() - ) - )() + divFuncs += x -> res + res + } + } + + def modFuncApp(x: IntegerKind)(e1: vpr.Exp, e2: vpr.Exp)(pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): vpr.Exp = { + val funcname = modFunc(x).name + vpr.FuncApp(funcname = funcname, args = Seq(e1, e2))(pos, info, typ = domainType(x), errT) } + // TODO: update specs /** * Generates the following viper function that captures the semantics of the '%' operator in Go: - * function goIntMod(l: Int, r: Int): Int - * requires r != 0 - * decreases _ - * { + * function goIntMod(l: Int, r: Int): Int + * requires r != 0 + * decreases _ + * { * (0 <= l || l % r == 0 ? l % r : l % r - (0 <= r ? r : -r)) - * } + * } */ - private lazy val goIntMod: vpr.Function = { - isUsedGoIntMod = true - val lDecl = vpr.LocalVarDecl("l", vpr.Int)() - val rDecl = vpr.LocalVarDecl("r", vpr.Int)() - val l = lDecl.localVar - val r = rDecl.localVar - val zero = vpr.IntLit(0)() - val absR = vpr.CondExp(cond = vpr.LeCmp(zero, r)(), thn = r, els = vpr.Minus(r)())() - val rNotZero = vpr.NeCmp(r, zero)() - vpr.Function( - name = Names.intMod, - formalArgs = Seq(lDecl, rDecl), - typ = vpr.Int, - pres = Seq(rNotZero, termination.DecreasesWildcard(None)()), - posts = Seq.empty, - body = Some( - // (0 <= l || l % r == 0) ? l % r : (l % r - abs(r)) - vpr.CondExp( - cond = vpr.Or(left = vpr.LeCmp(zero, l)(), right = vpr.EqCmp(vpr.Mod(l, r)(), zero)())(), - thn = vpr.Mod(l, r)(), - els = vpr.Sub(vpr.Mod(l, r)(), absR)() + private def modFunc(x: IntegerKind): vpr.Function = { + modFuncs.get(x) match { + case Some(f) => f + case _ => + val domainT = domainType(x) + val inputVar1Decl = vpr.LocalVarDecl("x", domainT)() + val inputVar2Decl = vpr.LocalVarDecl("y", domainT)() + val zero = vpr.IntLit(0)() + val pre = vpr.NeCmp(domainToIntFuncApp(x)(inputVar2Decl.localVar)(), zero)() + val post = x match { + case b: BoundedIntegerKind => + val result = domainToIntFuncApp(x)(vpr.Result(domainT)())() + vpr.And(vpr.LeCmp(vpr.IntLit(b.lower)(), result)(), vpr.LeCmp(result, vpr.IntLit(b.upper)())())() + case _ => vpr.TrueLit()() + } + val body = { + val l = domainToIntFuncApp(x)(inputVar1Decl.localVar)() + val r = domainToIntFuncApp(x)(inputVar2Decl.localVar)() + val absR = vpr.CondExp(cond = vpr.LeCmp(zero, r)(), thn = r, els = vpr.Minus(r)())() + // (0 <= l || l % r == 0) ? l % r : (l % r - abs(r)) + intToDomainFuncApp(x)( + vpr.CondExp( + cond = vpr.Or(left = vpr.LeCmp(zero, l)(), right = vpr.EqCmp(vpr.Mod(l, r)(), zero)())(), + thn = vpr.Mod(l, r)(), + els = vpr.Sub(vpr.Mod(l, r)(), absR)() + )() + )() + } + val res = vpr.Function( + name = s"mod${x.name}", + formalArgs = Seq(inputVar1Decl, inputVar2Decl), + typ = domainT, + pres = Seq(pre, termination.DecreasesWildcard(None)()), + posts = Seq(post), + body = Some(body) )() - ) - )() + modFuncs += x -> res + res + } + } + + /***** Bitwise operations *****/ + def bitAndFuncApp(x: IntegerKind)(e1: vpr.Exp, e2: vpr.Exp) + (pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): vpr.Exp = { + val funcname = bitAndFunc(x).name + vpr.FuncApp(funcname = funcname, args = Seq(e1, e2))(pos, info, typ = domainType(x), errT) + } + + private def bitAndFunc(x: IntegerKind): vpr.Function = { + bitAndFuncs.get(x) match { + case Some(f) => f + case _ => + val domainT = domainType(x) + val inputVar1Decl = vpr.LocalVarDecl("x", domainT)() + val inputVar2Decl = vpr.LocalVarDecl("y", domainT)() + val post = x match { + case b: BoundedIntegerKind => + val resultVal = domainToIntFuncApp(x)(vpr.Result(domainT)())() + vpr.And(vpr.LeCmp(vpr.IntLit(b.lower)(), resultVal)(), vpr.LeCmp(resultVal, vpr.IntLit(b.upper)())())() + case _ => vpr.TrueLit()() + } + val res = vpr.Function( + name = s"bitAnd${x.name}", + formalArgs = Seq(inputVar1Decl, inputVar2Decl), + typ = domainT, + pres = Seq(termination.DecreasesWildcard(None)()), + posts = Seq(post), + body = None + )() + bitAndFuncs += x -> res + res + } + } + + def bitOrFuncApp(x: IntegerKind)(e1: vpr.Exp, e2: vpr.Exp) + (pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): vpr.Exp = { + val funcname = bitOrFunc(x).name + vpr.FuncApp(funcname = funcname, args = Seq(e1, e2))(pos, info, typ = domainType(x), errT) } + + private def bitOrFunc(x: IntegerKind): vpr.Function = { + bitOrFuncs.get(x) match { + case Some(f) => f + case _ => + val domainT = domainType(x) + val inputVar1Decl = vpr.LocalVarDecl("x", domainT)() + val inputVar2Decl = vpr.LocalVarDecl("y", domainT)() + val post = x match { + case b: BoundedIntegerKind => + val resultVal = domainToIntFuncApp(x)(vpr.Result(domainT)())() + vpr.And(vpr.LeCmp(vpr.IntLit(b.lower)(), resultVal)(), vpr.LeCmp(resultVal, vpr.IntLit(b.upper)())())() + case _ => vpr.TrueLit()() + } + val res = vpr.Function( + name = s"bitOr${x.name}", + formalArgs = Seq(inputVar1Decl, inputVar2Decl), + typ = domainT, + pres = Seq(termination.DecreasesWildcard(None)()), + posts = Seq(post), + body = None + )() + bitOrFuncs += x -> res + res + } + } + + def bitXorFuncApp(x: IntegerKind)(e1: vpr.Exp, e2: vpr.Exp) + (pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): vpr.Exp = { + val funcname = bitXorFunc(x).name + vpr.FuncApp(funcname = funcname, args = Seq(e1, e2))(pos, info, typ = domainType(x), errT) + } + + private def bitXorFunc(x: IntegerKind): vpr.Function = { + bitXorFuncs.get(x) match { + case Some(f) => f + case _ => + val domainT = domainType(x) + val inputVar1Decl = vpr.LocalVarDecl("x", domainT)() + val inputVar2Decl = vpr.LocalVarDecl("y", domainT)() + val post = x match { + case b: BoundedIntegerKind => + val resultVal = domainToIntFuncApp(x)(vpr.Result(domainT)())() + vpr.And(vpr.LeCmp(vpr.IntLit(b.lower)(), resultVal)(), vpr.LeCmp(resultVal, vpr.IntLit(b.upper)())())() + case _ => vpr.TrueLit()() + } + val res = vpr.Function( + name = s"bitXor${x.name}", + formalArgs = Seq(inputVar1Decl, inputVar2Decl), + typ = domainT, + pres = Seq(termination.DecreasesWildcard(None)()), + posts = Seq(post), + body = None + )() + bitXorFuncs += x -> res + res + } + } + + def bitClearFuncApp(x: IntegerKind)(e1: vpr.Exp, e2: vpr.Exp) + (pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): vpr.Exp = { + val funcname = bitClearFunc(x).name + vpr.FuncApp(funcname = funcname, args = Seq(e1, e2))(pos, info, typ = domainType(x), errT) + } + + private def bitClearFunc(x: IntegerKind): vpr.Function = { + bitClearFuncs.get(x) match { + case Some(f) => f + case _ => + val domainT = domainType(x) + val inputVar1Decl = vpr.LocalVarDecl("x", domainT)() + val inputVar2Decl = vpr.LocalVarDecl("y", domainT)() + val post = x match { + case b: BoundedIntegerKind => + val resultVal = domainToIntFuncApp(x)(vpr.Result(domainT)())() + vpr.And(vpr.LeCmp(vpr.IntLit(b.lower)(), resultVal)(), vpr.LeCmp(resultVal, vpr.IntLit(b.upper)())())() + case _ => vpr.TrueLit()() + } + val res = vpr.Function( + name = s"bitClear${x.name}", + formalArgs = Seq(inputVar1Decl, inputVar2Decl), + typ = domainT, + pres = Seq(termination.DecreasesWildcard(None)()), + posts = Seq(post), + body = None + )() + bitClearFuncs += x -> res + res + } + } + + def bitNegFuncApp(x: IntegerKind)(e: vpr.Exp) + (pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): vpr.Exp = { + val funcname = bitNegFunc(x).name + vpr.FuncApp(funcname = funcname, args = Seq(e))(pos, info, typ = domainType(x), errT) + } + + private def bitNegFunc(x: IntegerKind): vpr.Function = { + bitNegFuncs.get(x) match { + case Some(f) => f + case _ => + val domainT = domainType(x) + val inputVarDecl = vpr.LocalVarDecl("x", domainT)() + val post = x match { + case b: BoundedIntegerKind => + val resultVal = domainToIntFuncApp(x)(vpr.Result(domainT)())() + vpr.And(vpr.LeCmp(vpr.IntLit(b.lower)(), resultVal)(), vpr.LeCmp(resultVal, vpr.IntLit(b.upper)())())() + case _ => vpr.TrueLit()() + } + val res = vpr.Function( + name = s"bitNeg${x.name}", + formalArgs = Seq(inputVarDecl), + typ = domainT, + pres = Seq(termination.DecreasesWildcard(None)()), + posts = Seq(post), + body = None + )() + bitNegFuncs += x -> res + res + } + } + + def bitShiftLeftFuncApp(x: IntegerKind, y: IntegerKind)(e1: vpr.Exp, e2: vpr.Exp) + (pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): vpr.Exp = { + val funcname = bitShiftLeftFunc(x, y).name + vpr.FuncApp(funcname = funcname, args = Seq(e1, e2))(pos, info, typ = domainType(x), errT) + } + + private def bitShiftLeftFunc(x: IntegerKind, y: IntegerKind): vpr.Function = { + bitShiftLeftFuncs.get((x, y)) match { + case Some(f) => f + case _ => + val domainTX = domainType(x) + val domainTY = domainType(y) + val inputVar1Decl = vpr.LocalVarDecl("x", domainTX)() + val inputVar2Decl = vpr.LocalVarDecl("y", domainTY)() + val pre = vpr.GeCmp( + IntEncodingGenerator.domainToIntFuncApp(y)(inputVar2Decl.localVar)(), + vpr.IntLit(BigInt(0))() + )() + val res = vpr.Function( + name = s"bitShiftLeft${x.name}${y.name}", + formalArgs = Seq(inputVar1Decl, inputVar2Decl), + typ = domainTX, + pres = Seq(pre, termination.DecreasesWildcard(None)()), + posts = Seq(), + body = None + )() + bitShiftLeftFuncs += (x, y) -> res + res + } + } + + def bitShiftRightFuncApp(x: IntegerKind, y: IntegerKind)(e1: vpr.Exp, e2: vpr.Exp) + (pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): vpr.Exp = { + val funcname = bitShiftRightFunc(x, y).name + vpr.FuncApp(funcname = funcname, args = Seq(e1, e2))(pos, info, typ = domainType(x), errT) + } + + private def bitShiftRightFunc(x: IntegerKind, y: IntegerKind): vpr.Function = { + bitShiftRightFuncs.get((x, y)) match { + case Some(f) => f + case _ => + val domainTX = domainType(x) + val domainTY = domainType(y) + val inputVar1Decl = vpr.LocalVarDecl("x", domainTX)() + val inputVar2Decl = vpr.LocalVarDecl("y", domainTY)() + val pre = vpr.GeCmp( + IntEncodingGenerator.domainToIntFuncApp(y)(inputVar2Decl.localVar)(), + vpr.IntLit(BigInt(0))() + )() + val res = vpr.Function( + name = s"bitShiftRight${x.name}${y.name}", + formalArgs = Seq(inputVar1Decl, inputVar2Decl), + typ = domainTX, + pres = Seq(pre, termination.DecreasesWildcard(None)()), + posts = Seq(), + body = None + )() + bitShiftRightFuncs += (x, y) -> res + res + } + } + } \ No newline at end of file diff --git a/src/main/scala/viper/gobra/translator/encodings/PermissionEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/PermissionEncoding.scala index a0d436c86..37ef8d891 100644 --- a/src/main/scala/viper/gobra/translator/encodings/PermissionEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/PermissionEncoding.scala @@ -58,11 +58,33 @@ class PermissionEncoding extends LeafTypeEncoding { res = vpr.CurrentPerm(pap.loc)(pos, info, errT) } yield res case pm@ in.PermMinus(exp) => for { e <- goE(exp) } yield withSrc(vpr.PermMinus(e), pm) - case fp@ in.FractionalPerm(l, r) => for {vl <- goE(l); vr <- goE(r)} yield withSrc(vpr.FractionalPerm(vl, vr), fp) + case fp@ in.FractionalPerm(l, r) => + for { + vlDom <- goE(l) + vrDom <- goE(r) + intKindL = l.typ match { + case t: in.IntT => t.kind + case _ => ??? + } + vl = withSrc(IntEncodingGenerator.domainToIntFuncApp(intKindL)(vlDom), fp) + intKindR = r.typ match { + case t: in.IntT => t.kind + case _ => ??? + } + vr = withSrc(IntEncodingGenerator.domainToIntFuncApp(intKindR)(vrDom), fp) + } yield withSrc(vpr.FractionalPerm(vl, vr), fp) case pa@ in.PermAdd(l, r) => for {vl <- goE(l); vr <- goE(r)} yield withSrc(vpr.PermAdd(vl, vr), pa) case ps@ in.PermSub(l, r) => for {vl <- goE(l); vr <- goE(r)} yield withSrc(vpr.PermSub(vl, vr), ps) case pm@ in.PermMul(l, r) => for {vl <- goE(l); vr <- goE(r)} yield withSrc(vpr.PermMul(vl, vr), pm) - case pd@ in.PermDiv(l, r) => for {vl <- goE(l); vr <- goE(r)} yield withSrc(vpr.PermDiv(vl, vr), pd) + case pd@ in.PermDiv(l, r) => for { + vl <- goE(l) + vrDom <- goE(r) + vr = r.typ match { + case t: in.IntT => + withSrc(IntEncodingGenerator.domainToIntFuncApp(t.kind)(vrDom), pd) + case _ => vrDom + } + } yield withSrc(vpr.PermDiv(vl, vr), pd) // Perm comparisons case lt@in.PermLtCmp(l, r) => for { vl <- goE(l); vr <- goE(r) } yield withSrc(vpr.PermLtCmp(vl, vr), lt) diff --git a/src/main/scala/viper/gobra/translator/encodings/StringEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/StringEncoding.scala index f1a005852..46c3b5756 100644 --- a/src/main/scala/viper/gobra/translator/encodings/StringEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/StringEncoding.scala @@ -65,7 +65,7 @@ class StringEncoding extends LeafTypeEncoding { unit(withSrc(vpr.DomainFuncApp(func = makeFunc(""), Seq(), Map.empty), e)) // "" is the default string value case (lit: in.StringLit) :: _ / Exclusive => unit(withSrc(vpr.DomainFuncApp(func = makeFunc(lit.s), Seq(), Map.empty), lit)) - case len @ in.Length(exp :: ctx.String()) => + case len @ in.Length(exp :: ctx.String(), _) => for { e <- goE(exp) } yield withSrc(vpr.DomainFuncApp(func = lenFunc, Seq(e), Map.empty), len) case concat @ in.Add(l :: ctx.String(), r :: ctx.String()) => for { @@ -75,18 +75,32 @@ class StringEncoding extends LeafTypeEncoding { case slice @ in.Slice(base :: ctx.String(), low, high, _, _) => for { baseExp <- goE(base) - lowExp <- goE(low) + lowKind = ctx.underlyingType(low.typ) match { + case in.IntT(_, kind) => kind + case _ => ??? + } + lowExp <- goE(low) + lowInt = IntEncodingGenerator.domainToIntFuncApp(lowKind)(lowExp)(lowExp.pos, lowExp.info, lowExp.errT) highExp <- goE(high) - } yield withSrc(vpr.FuncApp(strSlice, Seq(baseExp, lowExp, highExp)), slice) + highKind = ctx.underlyingType(high.typ) match { + case in.IntT(_, kind) => kind + case _ => ??? + } + highInt = IntEncodingGenerator.domainToIntFuncApp(highKind)(highExp)(highExp.pos, highExp.info, highExp.errT) + } yield withSrc(vpr.FuncApp(strSlice, Seq(baseExp, lowInt, highInt)), slice) case conv@in.Conversion(in.StringT(_), expr :: ctx.Slice(in.IntT(_, TypeBounds.Byte))) => val (pos, info, errT) = conv.vprMeta for { e <- goE(expr) } yield byteSliceToStr(e)(ctx)(pos, info, errT) case e@in.IndexedExp(base, index, _: in.StringT) => + ??? + /* val (pos, info, errT) = e.vprMeta for { baseExp <- goE(base) indexExp <- goE(index) } yield stringIndex(baseExp, indexExp)(ctx)(pos, info, errT) + + */ } } @@ -116,21 +130,25 @@ class StringEncoding extends LeafTypeEncoding { val sliceT = in.SliceT(in.IntT(Addressability.sliceElement, TypeBounds.Byte), Addressability.outParameter) val slice = in.LocalVar(ctx.freshNames.next(), sliceT)(conv.info) val vprSlice = ctx.variable(slice) - val qtfVar = in.BoundVar("i", in.IntT(Addressability.boundVariable))(conv.info) + val qtfVar = in.BoundVar("i", in.IntT(Addressability.boundVariable, TypeBounds.DefaultInt))(conv.info) val post1 = in.SepForall( vars = Vector(qtfVar), triggers = Vector(in.Trigger(Vector(in.Ref(in.IndexedExp(slice, qtfVar, sliceT)(conv.info))(conv.info)))(conv.info)), body = in.Implication( - in.And(in.AtMostCmp(in.IntLit(BigInt(0))(conv.info), qtfVar)(conv.info), in.LessCmp(qtfVar, in.Length(slice)(conv.info))(conv.info))(conv.info), + in.And( + in.AtMostCmp(in.IntLit(BigInt(0))(conv.info), qtfVar)(conv.info), + in.LessCmp(qtfVar, in.Length(slice, sliceT)(conv.info))(conv.info) + )(conv.info), in.Access(in.Accessible.Address(in.IndexedExp(slice, qtfVar, sliceT)(conv.info)), in.FullPerm(conv.info))(conv.info) )(conv.info) )(conv.info) val post2 = in.ExprAssertion( in.EqCmp( - in.Length(slice)(conv.info), - in.Length(e)(conv.info), + in.Length(slice, sliceT)(conv.info), + in.Length(e, underlyingType(e.typ)(ctx))(conv.info), )(conv.info) )(conv.info) + /* val post3 = in.SepForall( vars = Vector(qtfVar), triggers = Vector( @@ -149,6 +167,7 @@ class StringEncoding extends LeafTypeEncoding { )(conv.info) )(conv.info) )(conv.info) + */ seqn( for { @@ -157,8 +176,8 @@ class StringEncoding extends LeafTypeEncoding { _ <- write(vpr.Inhale(vprPost1)(pos, info, errT)) vprPost2 <- goA(post2) _ <- write(vpr.Inhale(vprPost2)(pos, info, errT)) - vprPost3 <- goA(post3) - _ <- write(vpr.Inhale(vprPost3)(pos, info, errT)) + // vprPost3 <- goA(post3) + //_ <- write(vpr.Inhale(vprPost3)(pos, info, errT)) ass <- ctx.assignment(in.Assignee.Var(target), slice)(conv) } yield ass ) @@ -170,7 +189,7 @@ class StringEncoding extends LeafTypeEncoding { addMemberFn(genDomain()) if (strSliceIsUsed) { addMemberFn(strSlice) } byteSliceToStrFuncGenerator.finalize(addMemberFn) - stringIndexFuncGenerator.finalize(addMemberFn) + // stringIndexFuncGenerator.finalize(addMemberFn) } } private var isUsed: Boolean = false @@ -193,13 +212,13 @@ class StringEncoding extends LeafTypeEncoding { /** * Generates - * function strLen(id: Int): Int + * function strLen(id: Int): ??? */ private val lenFuncName: String = "strLen" private lazy val lenFunc: vpr.DomainFunc = vpr.DomainFunc( name = lenFuncName, formalArgs = Seq(vpr.LocalVarDecl("id", stringType)()), - typ = vpr.Int, + typ = IntEncodingGenerator.intType, )(domainName = domainName) /** @@ -238,12 +257,19 @@ class StringEncoding extends LeafTypeEncoding { pres = Seq( vpr.LeCmp(vpr.IntLit(0)(), argL.localVar)(), vpr.LeCmp(argL.localVar, argH.localVar)(), - vpr.LeCmp(argH.localVar, vpr.DomainFuncApp(lenFunc, Seq(argS.localVar), Map.empty)())(), + vpr.LeCmp( + argH.localVar, + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)( + vpr.DomainFuncApp(lenFunc, Seq(argS.localVar), Map.empty)() + )() + )(), synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate"), ), posts = Seq( vpr.EqCmp( - vpr.DomainFuncApp(lenFunc, Seq(vpr.Result(stringType)()), Map.empty)(), + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)( + vpr.DomainFuncApp(lenFunc, Seq(vpr.Result(stringType)()), Map.empty)() + )(), vpr.Sub(argH.localVar, argL.localVar)() )() ), @@ -263,7 +289,10 @@ class StringEncoding extends LeafTypeEncoding { vpr.AnonymousDomainAxiom { val encodedStr: vpr.Exp = vpr.DomainFuncApp(encodedStrings(str), Seq.empty, Map.empty)() val lenCall = vpr.DomainFuncApp(func = lenFunc, Seq(encodedStr), Map.empty)() - vpr.EqCmp(lenCall, vpr.IntLit(BigInt(str.length))())() + vpr.EqCmp( + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(lenCall)(), + vpr.IntLit(BigInt(str.length))() + )() }(domainName = domainName) } @@ -275,7 +304,9 @@ class StringEncoding extends LeafTypeEncoding { */ val lenAxiom = vpr.AnonymousDomainAxiom { val qtfVar = vpr.LocalVarDecl("str", stringType)() - val lenApp = vpr.DomainFuncApp(lenFunc, Seq(qtfVar.localVar), Map.empty)() + val lenApp = IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)( + vpr.DomainFuncApp(lenFunc, Seq(qtfVar.localVar), Map.empty)() + )() vpr.Forall( variables = Seq(qtfVar), triggers = Seq(vpr.Trigger(Seq(lenApp))()), @@ -293,11 +324,17 @@ class StringEncoding extends LeafTypeEncoding { val appAxiom: vpr.DomainAxiom = vpr.AnonymousDomainAxiom { val var1 = vpr.LocalVarDecl("l", stringType)() val var2 = vpr.LocalVarDecl("r", stringType)() - val lenConcat = vpr.DomainFuncApp(lenFunc, Seq(vpr.DomainFuncApp(concatFunc, Seq(var1.localVar, var2.localVar), Map.empty)()), Map.empty)() + val lenConcat = IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)( + vpr.DomainFuncApp(lenFunc, Seq(vpr.DomainFuncApp(concatFunc, Seq(var1.localVar, var2.localVar), Map.empty)()), Map.empty)() + )() val trigger = vpr.Trigger(Seq(lenConcat))() val exp = vpr.EqCmp(lenConcat, vpr.Add( - vpr.DomainFuncApp(lenFunc, Seq(var1.localVar), Map.empty)(), - vpr.DomainFuncApp(lenFunc, Seq(var2.localVar), Map.empty)() + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)( + vpr.DomainFuncApp(lenFunc, Seq(var1.localVar), Map.empty)() + )(), + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)( + vpr.DomainFuncApp(lenFunc, Seq(var2.localVar), Map.empty)() + )() )())() vpr.Forall(Seq(var1, var2), Seq(trigger), exp)() }(domainName = domainName) @@ -324,23 +361,25 @@ class StringEncoding extends LeafTypeEncoding { val info = Source.Parser.Internal val paramT = in.SliceT(in.IntT(Addressability.sliceElement, TypeBounds.Byte), Addressability.outParameter) val param = in.Parameter.In("s", paramT)(info) - val res = in.Parameter.Out("res", in.StringT(Addressability.outParameter))(info) - val qtfVar = in.BoundVar("i", in.IntT(Addressability.boundVariable))(info) + val resT = in.StringT(Addressability.outParameter) + val res = in.Parameter.Out("res", resT)(info) + val qtfVar = in.BoundVar("i", in.IntT(Addressability.boundVariable, TypeBounds.DefaultInt))(info) val trigger = in.Trigger(Vector(in.Ref(in.IndexedExp(param, qtfVar, paramT)(info))(info)))(info) val pre = in.SepForall( vars = Vector(qtfVar), triggers = Vector(trigger), body = in.Implication( - in.And(in.AtMostCmp(in.IntLit(BigInt(0))(info), qtfVar)(info), in.LessCmp(qtfVar, in.Length(param)(info))(info))(info), + in.And(in.AtMostCmp(in.IntLit(BigInt(0))(info), qtfVar)(info), in.LessCmp(qtfVar, in.Length(param, paramT)(info))(info))(info), in.Access(in.Accessible.Address(in.IndexedExp(param, qtfVar, paramT)(info)), in.WildcardPerm(info))(info) )(info) )(info) val post1 = in.ExprAssertion( in.EqCmp( - in.Length(param)(info), - in.Length(res)(info), + in.Length(param, paramT)(info), + in.Length(res, resT)(info), )(info) )(info) + /* val post2 = in.SepForall( vars = Vector(qtfVar), triggers = Vector( @@ -360,12 +399,14 @@ class StringEncoding extends LeafTypeEncoding { )(info) )(info) + */ + val func: in.PureFunction = in.PureFunction( name = in.FunctionProxy(byteSliceToStrFuncName)(info), args = Vector(param), results = Vector(res), pres = Vector(pre), - posts = Vector(post1, post2), + posts = Vector(post1 /*, post2 */), terminationMeasures = Vector(in.NonItfMethodWildcardMeasure(None)(info)), backendAnnotations = Vector.empty, body = None, @@ -385,6 +426,7 @@ class StringEncoding extends LeafTypeEncoding { * decreases _ * pure func stringIndexFunc(s string, i int) (res byte) */ + /* private val stringIndexFuncName: String = "stringIndexFunc" private val stringIndexFuncGenerator: FunctionGenerator[Unit] = new FunctionGenerator[Unit] { override def genFunction(@unused x: Unit)(ctx: Context): vpr.Function = { @@ -416,9 +458,11 @@ class StringEncoding extends LeafTypeEncoding { val translatedFunc = ctx.function(func) translatedFunc.res } + } + */ - private def stringIndex(str: vpr.Exp, idx: vpr.Exp)(ctx: Context)(pos: vpr.Position, info: vpr.Info, errT: vpr.ErrorTrafo): vpr.FuncApp = - stringIndexFuncGenerator(Vector(str, idx), ())(pos, info, errT)(ctx) + // private def stringIndex(str: vpr.Exp, idx: vpr.Exp)(ctx: Context)(pos: vpr.Position, info: vpr.Info, errT: vpr.ErrorTrafo): vpr.FuncApp = + // stringIndexFuncGenerator(Vector(str, idx), ())(pos, info, errT)(ctx) } diff --git a/src/main/scala/viper/gobra/translator/encodings/adts/AdtEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/adts/AdtEncoding.scala index 03ab482c8..933177ee7 100644 --- a/src/main/scala/viper/gobra/translator/encodings/adts/AdtEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/adts/AdtEncoding.scala @@ -341,7 +341,7 @@ class AdtEncoding extends LeafTypeEncoding { case p: in.PatternMatchExp => translatePatternMatchExp(p)(ctx) - case l@in.Length(expr :: ctx.Adt(a)) => + case l@in.Length(expr :: ctx.Adt(a), _) => for { e <- ctx.expression(expr) rankApp = withSrc(applyRankFunc(a.name, e), l) diff --git a/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala index e21e25f66..62fc910df 100644 --- a/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala @@ -8,18 +8,19 @@ package viper.gobra.translator.encodings.arrays import org.bitbucket.inkytonik.kiama.==> import viper.gobra.ast.{internal => in} -import viper.gobra.reporting.{LoadError, InsufficientPermissionError, Source} +import viper.gobra.reporting.{InsufficientPermissionError, LoadError, Source} import viper.gobra.theory.Addressability import viper.gobra.theory.Addressability.{Exclusive, Shared} import viper.gobra.translator.Names import viper.gobra.translator.encodings.arrays.ArrayEncoding.ComponentParameter import viper.gobra.translator.encodings.combinators.TypeEncoding import viper.gobra.translator.context.Context +import viper.gobra.translator.encodings.IntEncodingGenerator import viper.gobra.translator.library.embeddings.EmbeddingParameter import viper.gobra.translator.util.FunctionGenerator import viper.gobra.translator.util.ViperUtil.synthesized import viper.gobra.translator.util.ViperWriter.CodeWriter -import viper.gobra.util.Violation +import viper.gobra.util.{TypeBounds, Violation} import viper.silver.plugin.standard.termination import viper.silver.{ast => vpr} @@ -124,7 +125,7 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding { typLhs = underlyingType(lhs.typ)(ctx) typRhs = underlyingType(rhs.typ)(ctx) body = (idx: in.BoundVar) => ctx.equal(in.IndexedExp(x, idx, typLhs)(src.info), in.IndexedExp(y, idx, typRhs)(src.info))(src) - res <- boundedQuant(len, idx => xTrigger(idx) ++ yTrigger(idx), body)(src)(ctx) + res <- boundedQuant(len, IntEncodingGenerator.intKind, idx => xTrigger(idx) ++ yTrigger(idx), body)(src)(ctx) } yield res case (lhs :: ctx.*(ctx.Array(len, _)) / Exclusive, rhs :: ctx.*(ctx.Array(len2, _)), src) if len == len2 => @@ -178,8 +179,13 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding { case (loc@ in.IndexedExp(base :: ctx.Array(len, t), idx, _)) :: _ / Exclusive => for { vBase <- ctx.expression(base) + idxKind = ctx.underlyingType(idx.typ) match { + case in.IntT(_, k) => k + case _ => ??? + } vIdx <- ctx.expression(idx) - } yield ex.get(vBase, vIdx, cptParam(len, t)(ctx))(loc)(ctx) + newVIdx = IntEncodingGenerator.domainToIntFuncApp(idxKind)(vIdx)()// TODO: pos info + } yield ex.get(vBase, newVIdx, cptParam(len, t)(ctx))(loc)(ctx) case (upd: in.ArrayUpdate) :: ctx.Array(len, t) => for { @@ -199,28 +205,28 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding { vLit <- ctx.expression(in.SequenceLit(len, t, lit.elems)(lit.info)) } yield ex.fromSeq(vLit, cptParam(len, t)(ctx))(lit)(ctx) - case n@ in.Length(e :: ctx.Array(len, t) / m) => + case n@ in.Length(e :: ctx.Array(len, t) / m, _) => m match { case Exclusive => ctx.expression(e).map(ex.length(_, cptParam(len, t)(ctx))(n)(ctx)) case Shared => ctx.reference(e.asInstanceOf[in.Location]).map(sh.length(_, cptParam(len, t)(ctx))(n)(ctx)) } - case in.Length(exp :: ctx.*(t: in.ArrayT)) => + case in.Length(exp :: ctx.*(t: in.ArrayT), _) => val expInfo = exp.info val derefExp = in.Deref(exp, in.PointerT(t, t.addressability))(expInfo) - val newLenExpr = in.Length(derefExp)(expInfo) + val newLenExpr = in.Length(derefExp, underlyingType(derefExp.typ)(ctx))(expInfo) expression(ctx)(newLenExpr) - case n@in.Capacity(e :: ctx.Array(len, t) / m) => + case n@in.Capacity(e :: ctx.Array(len, t) / m, _) => m match { case Exclusive => ctx.expression(e).map(ex.length(_, cptParam(len, t)(ctx))(n)(ctx)) case Shared => ctx.reference(e.asInstanceOf[in.Location]).map(sh.length(_, cptParam(len, t)(ctx))(n)(ctx)) } - case in.Capacity(exp :: ctx.*(t: in.ArrayT)) => + case in.Capacity(exp :: ctx.*(t: in.ArrayT), _) => val expInfo = exp.info val derefExp = in.Deref(exp, in.PointerT(t, t.addressability))(expInfo) - val newLenExpr = in.Capacity(derefExp)(expInfo) + val newLenExpr = in.Capacity(derefExp, underlyingType(derefExp.typ)(ctx))(expInfo) expression(ctx)(newLenExpr) case n@ in.SequenceConversion(e :: ctx.Array(len, t) / Exclusive) => @@ -273,13 +279,25 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding { for { vBase <- ctx.reference(base.asInstanceOf[in.Location]) vIdx <- ctx.expression(idx) - } yield sh.get(vBase, vIdx, cptParam(len, t)(ctx))(loc)(ctx) + idxKind = ctx.underlyingType(idx.typ) match { + case in.IntT(_, k) => k + case _ => ??? + } + /* + vIdxNew = IntEncodingGenerator.domainToIntFuncApp(idxKind)(vIdx)() + */ + // _ = if (idxKind == IntEncodingGenerator.integerKind) { } else { println(s"Failed with $loc"); ???} + } yield sh.get(vBase, vIdx, idxKind, cptParam(len, t)(ctx))(loc)(ctx) case loc@in.IndexedExp(base :: ctx.*(in.ArrayT(len, t, _)), idx, ptrT) => val derefBase = in.Deref(base, ptrT)(base.info) for { vBase <- ctx.reference(derefBase.asInstanceOf[in.Location]) vIdx <- ctx.expression(idx) - } yield sh.get(vBase, vIdx, cptParam(len, t)(ctx))(loc)(ctx) + idxKind = ctx.underlyingType(idx.typ) match { + case in.IntT(_, k) => k + case _ => ??? + } + } yield sh.get(vBase, vIdx, idxKind, cptParam(len, t)(ctx))(loc)(ctx) } /** @@ -296,10 +314,12 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding { case (loc :: ctx.Array(len, t) / Shared, perm) => val (pos, info, errT) = loc.vprMeta val typ = underlyingType(loc.typ)(ctx) - val trigger = (idx: vpr.LocalVar) => - Seq(vpr.Trigger(Seq(sh.get(ctx.reference(loc).res, idx, cptParam(len, t)(ctx))(loc)(ctx)))(pos, info, errT)) + val trigger = (idx: vpr.LocalVar) => { + // val newIdx = IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.integerKind)(idx)() + Seq(vpr.Trigger(Seq(sh.get(ctx.reference(loc).res, idx, IntEncodingGenerator.intKind, cptParam(len, t)(ctx))(loc)(ctx)))(pos, info, errT)) + } val body = (idx: in.BoundVar) => ctx.footprint(in.IndexedExp(loc, idx, typ)(loc.info), perm) - boundedQuant(len, trigger, body)(loc)(ctx).map(forall => + boundedQuant(len, IntEncodingGenerator.intKind, trigger, body)(loc)(ctx).map(forall => // to eliminate nested quantified permissions, which are not supported by the silver ast. VU.bigAnd(viper.silver.ast.utility.QuantifiedPermissions.desugarSourceQuantifiedPermissionSyntax(forall))(pos, info, errT) ) @@ -315,7 +335,7 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding { super.isComparable(ctx)(exp).map{ _ => val (pos, info, errT) = exp.vprMeta // if this is executed, then type parameter must have dynamic comparability - val idx = in.BoundVar("idx", in.IntT(Exclusive))(exp.info) + val idx = in.BoundVar("idx", in.IntT(Exclusive, TypeBounds.DefaultInt))(exp.info) val vIdxDecl = ctx.variable(idx) val baseTyp = underlyingType(exp.typ)(ctx) for { @@ -324,7 +344,7 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding { res = vpr.Forall( variables = Seq(vIdxDecl), triggers = Seq(vpr.Trigger(Seq(rhs))(pos, info, errT)), - exp = vpr.Implies(boundaryCondition(vIdxDecl.localVar, len)(exp), rhs)(pos, info, errT) + exp = vpr.Implies(boundaryCondition(vIdxDecl.localVar, IntEncodingGenerator.intKind, len)(exp), rhs)(pos, info, errT) )(pos, info, errT) } yield res: vpr.Exp } @@ -379,18 +399,23 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding { // variable name does not matter because it is turned into a vpr.Result val resDummy = in.LocalVar("res", resType)(src.info) // variable name does not matter because it is the only variable occurring in the current scope - val idx = in.BoundVar("idx", in.IntT(Exclusive))(src.info) + val idx = in.BoundVar("idx", in.IntT(Exclusive, TypeBounds.DefaultInt))(src.info) val vIdx = ctx.variable(idx) val resAccess = in.IndexedExp(resDummy, idx, resType)(src.info) - val lenEq = pure(ctx.equal(in.Length(resDummy)(src.info), in.IntLit(resType.length)(src.info))(src))(ctx).res - .transform{ case x: vpr.LocalVar if x.name == resDummy.id => vpr.Result(vResType)() } + // val lenEq = pure(ctx.equal(in.Length(resDummy, resType)(src.info), in.IntLit(resType.length)(src.info))(src))(ctx).res + // .transform{ case x: vpr.LocalVar if x.name == resDummy.id => vpr.Result(vResType)() } + val lenEq = { + val l = ctx.expression(in.Length(resDummy, resType)(src.info)).res + .transform { case x: vpr.LocalVar if x.name == resDummy.id => vpr.Result(vResType)() } + vpr.EqCmp(l, IntEncodingGenerator.intToDomainFuncApp(IntEncodingGenerator.intKind)(vpr.IntLit(resType.length)())())() + } val idxEq = pure(ctx.equal(resAccess, in.DfltVal(resType.elems)(src.info))(src))(ctx).res .transform{ case x: vpr.LocalVar if x.name == resDummy.id => vpr.Result(vResType)() } - val trigger = ex.get(vpr.Result(vResType)(), vIdx.localVar, t)(src)(ctx) + val trigger = ex.get(vpr.Result(vResType)(), IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(vIdx.localVar)(), t)(src)(ctx) val arrayEq = vpr.Forall( Seq(vIdx), Seq(vpr.Trigger(Seq(trigger))()), - vpr.Implies(boundaryCondition(vIdx.localVar, t.len)(src), idxEq)() + vpr.Implies(boundaryCondition(vIdx.localVar, IntEncodingGenerator.intKind, t.len)(src), idxEq)() )() val terminationMeasure = synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate") @@ -407,23 +432,24 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding { } /** Returns: 0 <= 'base' && 'base' < 'length'. */ - private def boundaryCondition(base: vpr.Exp, length: BigInt)(src : in.Node) : vpr.Exp = { + private def boundaryCondition(base: vpr.Exp, baseKind: TypeBounds.IntegerKind, length: BigInt)(src : in.Node) : vpr.Exp = { val (pos, info, errT) = src.vprMeta + val baseInt = IntEncodingGenerator.domainToIntFuncApp(baseKind)(base)() vpr.And( - vpr.LeCmp(vpr.IntLit(0)(pos, info, errT), base)(pos, info, errT), - vpr.LtCmp(base, vpr.IntLit(length)(pos, info, errT))(pos, info, errT) + vpr.LeCmp(vpr.IntLit(0)(pos, info, errT), baseInt)(pos, info, errT), + vpr.LtCmp(baseInt, vpr.IntLit(length)(pos, info, errT))(pos, info, errT) )(pos, info, errT) } - /** Returns: Forall idx :: {'trigger'(idx)} 0 <= idx && idx < 'length' => ['body'(idx)] */ - private def boundedQuant(length: BigInt, trigger: vpr.LocalVar => Seq[vpr.Trigger], body: in.BoundVar => CodeWriter[vpr.Exp]) + /** Returns: Forall idx int :: {'trigger'(idx)} 0 <= idx && idx < 'length' => ['body'(idx)] */ + private def boundedQuant(length: BigInt, traversalVarKind: TypeBounds.IntegerKind, trigger: vpr.LocalVar => Seq[vpr.Trigger], body: in.BoundVar => CodeWriter[vpr.Exp]) (src: in.Node)(ctx: Context) : CodeWriter[vpr.Forall] = { val (pos, info, errT) = src.vprMeta - val idx = in.BoundVar(ctx.freshNames.next(), in.IntT(Exclusive))(src.info) + val idx = in.BoundVar(ctx.freshNames.next(), in.IntT(Exclusive, traversalVarKind))(src.info) val vIdx = ctx.variable(idx) for { @@ -431,7 +457,7 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding { forall = vpr.Forall( variables = Vector(vIdx), triggers = trigger(vIdx.localVar), - exp = vpr.Implies(boundaryCondition(vIdx.localVar, length)(src), vBody)(pos, info, errT) + exp = vpr.Implies(boundaryCondition(vIdx.localVar, traversalVarKind, length)(src), vBody)(pos, info, errT) )(pos, info, errT) } yield forall } @@ -450,7 +476,11 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding { vX = variable(ctx)(x) _ <- local(vX) _ <- bind(vX.localVar, vS) - trigger = (vIdx: vpr.LocalVar) => Seq(vpr.Trigger(Seq(ex.get(vX.localVar, vIdx, cptParam(len, t)(ctx))(e)(ctx)))(pos, info, errT)) + // TODO: here; adapt trigger + trigger = (vIdxDom: vpr.LocalVar) => { + val vIdx = IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(vIdxDom)() + Seq(vpr.Trigger(Seq(ex.get(vX.localVar, vIdx, cptParam(len, t)(ctx))(e)(ctx)))(pos, info, errT)) + } } yield (x, trigger) case (loc: in.Location) :: ctx.Array(len, t) / Shared => @@ -461,7 +491,11 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding { vX = variable(ctx)(x) _ <- local(vX) _ <- bind(vX.localVar, vS) - trigger = (vIdx: vpr.LocalVar) => Seq(vpr.Trigger(Seq(sh.get(vX.localVar, vIdx, cptParam(len, t)(ctx))(loc)(ctx)))(pos, info, errT)) + // TODO: here; adapt trigger + trigger = (vIdx: vpr.LocalVar) => { + // val vIdx = IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.integerKind)(vIdxDom)() + Seq(vpr.Trigger(Seq(sh.get(vX.localVar, vIdx, IntEncodingGenerator.intKind, cptParam(len, t)(ctx))(loc)(ctx)))(pos, info, errT)) + } } yield (x, trigger) case t => Violation.violation(s"Expected array, but got $t.") diff --git a/src/main/scala/viper/gobra/translator/encodings/arrays/ExclusiveArrayComponentImpl.scala b/src/main/scala/viper/gobra/translator/encodings/arrays/ExclusiveArrayComponentImpl.scala index 47daa219a..eb0ab768e 100644 --- a/src/main/scala/viper/gobra/translator/encodings/arrays/ExclusiveArrayComponentImpl.scala +++ b/src/main/scala/viper/gobra/translator/encodings/arrays/ExclusiveArrayComponentImpl.scala @@ -10,6 +10,7 @@ import viper.gobra.ast.{internal => in} import viper.silver.{ast => vpr} import ArrayEncoding.ComponentParameter import viper.gobra.translator.context.Context +import viper.gobra.translator.encodings.IntEncodingGenerator import viper.gobra.translator.library.embeddings.EmbeddingComponent class ExclusiveArrayComponentImpl extends ExclusiveArrayComponent { @@ -61,7 +62,9 @@ class ExclusiveArrayComponentImpl extends ExclusiveArrayComponent { /** Length of exclusive-array domain. */ override def length(arg: vpr.Exp, t: ComponentParameter)(src: in.Node)(ctx: Context): vpr.Exp = { val (pos, info, errT) = src.vprMeta - vpr.SeqLength(emb.unbox(arg, t)(pos, info, errT)(ctx))(pos, info, errT) // len(unbox(arg)) + IntEncodingGenerator.intToDomainFuncApp(IntEncodingGenerator.intKind)( + vpr.SeqLength(emb.unbox(arg, t)(pos, info, errT)(ctx))(pos, info, errT) // len(unbox(arg)) + )(pos, info, errT) } /** Returns an exclusive array from a sequence. */ diff --git a/src/main/scala/viper/gobra/translator/encodings/arrays/SharedArrayComponent.scala b/src/main/scala/viper/gobra/translator/encodings/arrays/SharedArrayComponent.scala index 1583d2545..50543d113 100644 --- a/src/main/scala/viper/gobra/translator/encodings/arrays/SharedArrayComponent.scala +++ b/src/main/scala/viper/gobra/translator/encodings/arrays/SharedArrayComponent.scala @@ -11,6 +11,7 @@ import viper.silver.{ast => vpr} import ArrayEncoding.ComponentParameter import viper.gobra.translator.library.Generator import viper.gobra.translator.context.Context +import viper.gobra.util.TypeBounds trait SharedArrayComponent extends Generator { @@ -18,7 +19,7 @@ trait SharedArrayComponent extends Generator { def typ(t: ComponentParameter)(ctx: Context): vpr.Type /** Getter of shared-array domain. */ - def get(base: vpr.Exp, idx: vpr.Exp, t: ComponentParameter)(src: in.Node)(ctx: Context): vpr.Exp + def get(base: vpr.Exp, idx: vpr.Exp, idxKind: TypeBounds.IntegerKind, t: ComponentParameter)(src: in.Node)(ctx: Context): vpr.Exp /** Nil of shared-struct domain */ def nil(t: ComponentParameter)(src: in.Node)(ctx: Context): vpr.Exp diff --git a/src/main/scala/viper/gobra/translator/encodings/arrays/SharedArrayComponentImpl.scala b/src/main/scala/viper/gobra/translator/encodings/arrays/SharedArrayComponentImpl.scala index 49adc4b88..4c61be191 100644 --- a/src/main/scala/viper/gobra/translator/encodings/arrays/SharedArrayComponentImpl.scala +++ b/src/main/scala/viper/gobra/translator/encodings/arrays/SharedArrayComponentImpl.scala @@ -14,9 +14,11 @@ import viper.gobra.theory.Addressability.{Exclusive, Shared} import viper.gobra.translator.context.Context import viper.gobra.translator.library.embeddings.EmbeddingComponent import viper.gobra.translator.Names +import viper.gobra.translator.encodings.IntEncodingGenerator import viper.gobra.translator.util.FunctionGenerator import viper.gobra.translator.util.ViperUtil.synthesized import viper.gobra.translator.util.ViperWriter.CodeLevel.pure +import viper.gobra.util.TypeBounds import viper.silver.plugin.standard.termination class SharedArrayComponentImpl extends SharedArrayComponent { @@ -38,7 +40,7 @@ class SharedArrayComponentImpl extends SharedArrayComponent { val src = in.DfltVal(t.arrayT(Shared))(Source.Parser.Internal) val idx = in.BoundVar("idx", in.IntT(Exclusive))(src.info) val vIdx = ctx.variable(idx) - val resAccess = ctx.array.loc(vpr.Result(vResType)(), vIdx.localVar)() + val resAccess = ctx.array.loc(vpr.Result(vResType)(), IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.integerKind)(vIdx.localVar)())() val idxEq = vpr.EqCmp(resAccess, pure(ctx.expression(in.DfltVal(t.elemT)(src.info)))(ctx).res)() val forall = vpr.Forall( Seq(vIdx), @@ -51,7 +53,13 @@ class SharedArrayComponentImpl extends SharedArrayComponent { formalArgs = Seq.empty, typ = vResType, pres = Seq(synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate")), - posts = Vector(vpr.EqCmp(ctx.array.len(vpr.Result(vResType)())(), vpr.IntLit(1)())(), forall), + posts = Vector( + vpr.EqCmp( + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.array.len(vpr.Result(vResType)())())(), + vpr.IntLit(1)() + )(), + forall + ), body = None )() } @@ -61,7 +69,7 @@ class SharedArrayComponentImpl extends SharedArrayComponent { private val emb: EmbeddingComponent[ComponentParameter] = new EmbeddingComponent.Impl[ComponentParameter]( p = (e: vpr.Exp, id: ComponentParameter) => (ctx: Context) => vpr.Or( // len(a) == n || a == arrayNil - vpr.EqCmp(ctx.array.len(e)(), vpr.IntLit(id.len)())(), + vpr.EqCmp(IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.array.len(e)())(), vpr.IntLit(id.len)())(), vpr.EqCmp(e, arrayNilFunc(Vector.empty, id)()(ctx))() )(), t = (id: ComponentParameter) => (ctx: Context) => ctx.array.typ(ctx.typ(id.elemT)) @@ -71,9 +79,10 @@ class SharedArrayComponentImpl extends SharedArrayComponent { override def typ(t: ComponentParameter)(ctx: Context): vpr.Type = emb.typ(t)(ctx) /** Getter of shared-array domain. */ - override def get(base: vpr.Exp, idx: vpr.Exp, t: ComponentParameter)(src: in.Node)(ctx: Context): vpr.Exp = { + override def get(base: vpr.Exp, idx: vpr.Exp, idxKind: TypeBounds.IntegerKind, t: ComponentParameter)(src: in.Node)(ctx: Context): vpr.Exp = { val (pos, info, errT) = src.vprMeta - ctx.array.loc(emb.unbox(base, t)(pos, info, errT)(ctx), idx)(pos, info, errT) // unbox(base)[idx] + val newIdx = IntEncodingGenerator.domainToIntFuncApp(idxKind)(idx)(idx.pos, idx.info, idx.errT) + ctx.array.loc(emb.unbox(base, t)(pos, info, errT)(ctx), newIdx)(pos, info, errT) // unbox(base)[idx] } /** Nil of shared-struct domain */ diff --git a/src/main/scala/viper/gobra/translator/encodings/closures/ClosureEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/closures/ClosureEncoding.scala index 0c467d9b0..d364f9961 100644 --- a/src/main/scala/viper/gobra/translator/encodings/closures/ClosureEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/closures/ClosureEncoding.scala @@ -16,6 +16,7 @@ import viper.gobra.theory.Addressability import viper.gobra.theory.Addressability.{Exclusive, Shared} import viper.gobra.translator.Names import viper.gobra.translator.context.Context +import viper.gobra.translator.encodings.IntEncodingGenerator import viper.gobra.translator.encodings.combinators.LeafTypeEncoding import viper.gobra.translator.util.{ViperUtil => vu} import viper.silver.plugin.standard.termination @@ -112,7 +113,7 @@ class ClosureEncoding(config: Config) extends LeafTypeEncoding { vpr.Method( Names.closureProofIterator, Seq.empty, - Seq(vpr.LocalVarDecl("res", vpr.Int)()), + Seq(vpr.LocalVarDecl("res", IntEncodingGenerator.integerType)()), Seq(termination.DecreasesTuple(Nil)()), Seq.empty, None )() } diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala index 377b54000..420e7b7de 100644 --- a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala @@ -230,7 +230,8 @@ trait TypeEncoding extends Generator { args = Seq.empty )(pos, info, typ, errT) unit(vprExpr) - case in.Conversion(t2, expr :: t) if typ(ctx).isDefinedAt(t) && typ(ctx).isDefinedAt(t2) => ctx.expression(expr) + case in.Conversion(t2, expr :: t) if typ(ctx).isDefinedAt(t) && typ(ctx).isDefinedAt(t2) && + !t.isInstanceOf[in.IntT] && !t2.isInstanceOf[in.IntT] => ctx.expression(expr) } /** diff --git a/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala index 398aa9414..db12ed4ec 100644 --- a/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala @@ -71,7 +71,7 @@ class MapEncoding extends LeafTypeEncoding { case (exp: in.NilLit) :: ctx.Map(_, _) / Exclusive => unit(withSrc(vpr.NullLit(), exp)) - case l@in.Length(exp :: ctx.Map(keys, values)) => + case l@in.Length(exp :: ctx.Map(keys, values), _) => val (pos, info, errT) = l.vprMeta // Encodes // [ len(m) ] -> [ m ] == null? 0 : | getCorrespondingMap([m]) | diff --git a/src/main/scala/viper/gobra/translator/encodings/maps/MathematicalMapEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/maps/MathematicalMapEncoding.scala index 7c8dbf6ff..a847e1190 100644 --- a/src/main/scala/viper/gobra/translator/encodings/maps/MathematicalMapEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/maps/MathematicalMapEncoding.scala @@ -103,7 +103,7 @@ class MathematicalMapEncoding extends LeafTypeEncoding { vRight <- goE(right) } yield vpr.MapUpdate(vBase, vLeft, vRight)(pos, info, errT) - case n@ in.Length(e :: ctx.MathematicalMap(_, _)) => + case n@ in.Length(e :: ctx.MathematicalMap(_, _), _) => val (pos, info, errT) = n.vprMeta goE(e).map(vpr.MapCardinality(_)(pos, info, errT)) diff --git a/src/main/scala/viper/gobra/translator/encodings/sequences/SequenceEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/sequences/SequenceEncoding.scala index cd81a08c0..04c43853c 100644 --- a/src/main/scala/viper/gobra/translator/encodings/sequences/SequenceEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/sequences/SequenceEncoding.scala @@ -13,6 +13,7 @@ import viper.gobra.theory.Addressability.{Exclusive, Shared} import viper.gobra.translator.Names import viper.gobra.translator.encodings.combinators.LeafTypeEncoding import viper.gobra.translator.context.Context +import viper.gobra.translator.encodings.IntEncodingGenerator import viper.gobra.translator.util.FunctionGenerator import viper.gobra.translator.util.ViperUtil.synthesized import viper.gobra.translator.util.ViperWriter.CodeWriter @@ -85,7 +86,11 @@ class SequenceEncoding extends LeafTypeEncoding { for { vE <- goE(e) vIdx <- goE(idx) - } yield vpr.SeqIndex(vE, vIdx)(pos, info, errT) + vIdxInt = idx.typ match { + case in.IntT(_, k) => IntEncodingGenerator.domainToIntFuncApp(k)(vIdx)(pos, info, errT) + case _ => vIdx + } + } yield vpr.SeqIndex(vE, vIdxInt)(pos, info, errT) case n@ in.GhostCollectionUpdate(base :: ctx.Seq(_), left, right, _) => val (pos, info, errT) = n.vprMeta @@ -115,9 +120,11 @@ class SequenceEncoding extends LeafTypeEncoding { } } - case n@ in.Length(e :: ctx.Seq(_)) => + case n@ in.Length(e :: ctx.Seq(_), _) => val (pos, info, errT) = n.vprMeta - goE(e).map(vpr.SeqLength(_)(pos, info, errT)) + goE(e) map { e => + IntEncodingGenerator.intToDomainFuncApp(IntEncodingGenerator.integerKind)(vpr.SeqLength(e)(pos, info, errT))(pos, info, errT) + } case in.SequenceConversion(e :: ctx.Seq(_)) => goE(e) @@ -162,14 +169,26 @@ class SequenceEncoding extends LeafTypeEncoding { for { leftT <- goE(n.left) rightT <- goE(n.right) - } yield vpr.SeqDrop(leftT, rightT)(pos, info, errT) + rightKind = ctx.underlyingType(n.right.typ) match { + case in.IntT(_, k) => k + case _ => ??? + } + // TODO: add more precise location info + rightTInt = IntEncodingGenerator.domainToIntFuncApp(rightKind)(rightT)(pos, info, errT) + } yield vpr.SeqDrop(leftT, rightTInt)(pos, info, errT) case n: in.SequenceTake => val (pos, info, errT) = n.vprMeta for { leftT <- goE(n.left) rightT <- goE(n.right) - } yield vpr.SeqTake(leftT, rightT)(pos, info, errT) + rightKind = ctx.underlyingType(n.right.typ) match { + case in.IntT(_, k) => k + case _ => ??? + } + // TODO: add more precise location info + rightTInt = IntEncodingGenerator.domainToIntFuncApp(rightKind)(rightT)(pos, info, errT) + } yield vpr.SeqTake(leftT, rightTInt)(pos, info, errT) } } diff --git a/src/main/scala/viper/gobra/translator/encodings/sets/SetEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/sets/SetEncoding.scala index 60075f11d..e13456c64 100644 --- a/src/main/scala/viper/gobra/translator/encodings/sets/SetEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/sets/SetEncoding.scala @@ -66,7 +66,7 @@ class SetEncoding extends LeafTypeEncoding { if (lit.exprs.isEmpty) unit(vpr.EmptyMultiset(ctx.typ(t))(pos, info, errT)) else sequence(lit.exprs map goE).map(args => vpr.ExplicitMultiset(args)(pos, info, errT)) - case n@ in.Length(exp :: ctx.AnySet(_)) => + case n@ in.Length(exp :: ctx.AnySet(_), _) => val (pos, info, errT) = n.vprMeta for { expT <- goE(exp) diff --git a/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala index f2fd03fdb..dade9b0d2 100644 --- a/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala @@ -16,10 +16,11 @@ import viper.gobra.translator.Names import viper.gobra.translator.encodings.arrays.SharedArrayEmbedding import viper.gobra.translator.encodings.combinators.LeafTypeEncoding import viper.gobra.translator.context.Context +import viper.gobra.translator.encodings.IntEncodingGenerator import viper.gobra.translator.util.FunctionGenerator import viper.gobra.translator.util.ViperUtil.synthesized import viper.gobra.translator.util.ViperWriter.CodeWriter -import viper.gobra.util.Violation +import viper.gobra.util.{TypeBounds, Violation} import viper.silver.verifier.{errors => err} import viper.silver.{ast => vpr} import viper.silver.plugin.standard.termination @@ -90,11 +91,11 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding { case (exp : in.NilLit) :: ctx.Slice(t) / Exclusive => unit(withSrc(nilSlice(t)(ctx), exp)) - case in.Length(exp :: ctx.Slice(_)) => for { + case in.Length(exp :: ctx.Slice(_), _) => for { expT <- goE(exp) } yield withSrc(ctx.slice.len(expT), exp) - case in.Capacity(exp :: ctx.Slice(_)) => for { + case in.Capacity(exp :: ctx.Slice(_), _) => for { expT <- goE(exp) } yield withSrc(ctx.slice.cap(expT), exp) @@ -116,10 +117,13 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding { val newSliceExpr = in.Slice(derefBase, low, high, max, t)(nInfo) expression(ctx)(newSliceExpr) - case exp @ in.Slice((base : in.Expr) :: ctx.Slice(_), low, high, max, _) => for { + case exp @ in.Slice((base : in.Expr) :: ctx.Slice(_), low :: in.IntT(_, kind1), high :: in.IntT(_, kind2), max, _) => for { baseT <- goE(base) - lowT <- goE(low) - highT <- goE(high) + lowTDom <- goE(low) + highTDom <- goE(high) + // low and high are IntDomains, we need to convert to ints + lowT = IntEncodingGenerator.domainToIntFuncApp(kind1)(lowTDom)() + highT = IntEncodingGenerator.domainToIntFuncApp(kind2)(highTDom)() maxOptT <- option(max map goE) } yield maxOptT match { case None => withSrc(sliceFromSlice(baseT, lowT, highT)(ctx), exp) @@ -155,8 +159,16 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding { _ <- local(vprSlice) capArg = optCapArg.getOrElse(lenArg) - vprLength <- ctx.expression(lenArg) - vprCapacity <- ctx.expression(capArg) + lenArgKind = lenArg.typ match { + case t: in.IntT => t.kind + case _ => ??? + } + capArgKind = capArg.typ match { + case t: in.IntT => t.kind + case _ => ??? + } + vprLength <- ctx.expression(lenArg).map(IntEncodingGenerator.domainToIntFuncApp(lenArgKind)(_)()) + vprCapacity <- ctx.expression(capArg).map(IntEncodingGenerator.domainToIntFuncApp(capArgKind)(_)()) // Perform additional runtime checks of conditions that must be true when make is invoked, otherwise the program panics (according to the go spec) // asserts 0 <= [len] && 0 <= [cap] && [len] <= [cap] @@ -176,15 +188,17 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding { footprintAssertion <- getCellPerms(ctx)(slice, in.FullPerm(slice.info), SliceBound.Cap) _ <- write(vpr.Inhale(footprintAssertion)(pos, info, errT)) - lenExpr = in.Length(slice)(makeStmt.info) - capExpr = in.Capacity(slice)(makeStmt.info) + capExpr = in.Capacity(slice, sliceT)(makeStmt.info) // inhale cap(a) == [cap] - eqCap <- ctx.equal(capExpr, capArg)(makeStmt) + vprCapExprInt <- ctx.expression(capExpr).map(IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(_)()) + eqCap = vpr.EqCmp(vprCapExprInt, vprCapacity)(pos, info, errT) _ <- write(vpr.Inhale(eqCap)(pos, info, errT)) // inhale len(a) == [len] - eqLen <- ctx.equal(lenExpr, lenArg)(makeStmt) + lenExpr = in.Length(slice, sliceT)(makeStmt.info) + vprLenExprInt <- ctx.expression(lenExpr).map(IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(_)()) + eqLen = vpr.EqCmp(vprLenExprInt, vprLength)(pos, info, errT) _ <- write(vpr.Inhale(eqLen)(pos, info, errT)) // inhale forall i: int :: {loc(a, i)} 0 <= i && i < [len] ==> [ a[i] == dfltVal(T) ] @@ -216,7 +230,12 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding { _ <- write(inhale) ass <- ctx.assignment( in.Assignee.Var(lit.target), - in.Slice(tmp, in.IntLit(0)(lit.info), in.IntLit(litA.length)(lit.info), None, underlyingTyp)(lit.info) + in.Slice(tmp, + in.IntLit(0, TypeBounds.DefaultInt)(lit.info), + in.IntLit(litA.length, TypeBounds.DefaultInt)(lit.info), + None, + underlyingTyp + )(lit.info) )(lit) } yield ass } @@ -233,10 +252,10 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding { case (loc :: ctx.Slice(_), perm :: ctx.Perm()) => val (pos, info, errT) = loc.vprMeta val bound = sliceBound match { - case SliceBound.Cap => in.Capacity(loc)(loc.info) - case SliceBound.Len => in.Length(loc)(loc.info) + case SliceBound.Cap => in.Capacity(loc, loc.typ)(loc.info) + case SliceBound.Len => in.Length(loc, loc.typ)(loc.info) } - val vprBound = ctx.expression(bound).res + val vprBound = IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.expression(bound).res)() val vprLoc = ctx.expression(loc).res val trigger = (idx: vpr.LocalVar) => Seq(vpr.Trigger(Seq(ctx.slice.loc(vprLoc, idx)(pos, info, errT)))(pos, info, errT)) @@ -264,7 +283,7 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding { val (pos, info, errT) = src.vprMeta - val idx = in.BoundVar(ctx.freshNames.next(), in.IntT(Exclusive))(src.info) + val idx = in.BoundVar(ctx.freshNames.next(), in.IntT(Exclusive, IntEncodingGenerator.intKind))(src.info) val vIdx = ctx.variable(idx) for { @@ -280,10 +299,11 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding { /** Returns: 0 <= 'base' && 'base' < 'bound'. */ private def boundaryCondition(base: vpr.Exp, bound: vpr.Exp)(src : in.Node) : vpr.Exp = { val (pos, info, errT) = src.vprMeta + val baseInt = IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(base)() vpr.And( - vpr.LeCmp(vpr.IntLit(0)(pos, info, errT), base)(pos, info, errT), - vpr.LtCmp(base, bound)(pos, info, errT) + vpr.LeCmp(vpr.IntLit(0)(pos, info, errT), baseInt)(pos, info, errT), + vpr.LtCmp(baseInt, bound)(pos, info, errT) )(pos, info, errT) } @@ -365,15 +385,26 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding { val pre1 = synthesized(vpr.LeCmp(vpr.IntLit(0)(), offsetDecl.localVar))("Slice offset might be negative") val pre2 = synthesized(vpr.LeCmp(vpr.IntLit(0)(), lenDecl.localVar))("Slice length might be negative") val pre3 = synthesized(vpr.LeCmp(lenDecl.localVar, capDecl.localVar))("Slice length might exceed capacity") - val pre4 = synthesized(vpr.LeCmp(vpr.Add(offsetDecl.localVar, capDecl.localVar)(), ctx.array.len(aDecl.localVar)()))("Slice capacity might exceed the capacity of the underlying array") + val pre4 = synthesized( + vpr.LeCmp( + vpr.Add(offsetDecl.localVar, capDecl.localVar)(), + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.array.len(aDecl.localVar)())() + ) + )("Slice capacity might exceed the capacity of the underlying array") val pre5 = synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate") // postconditions val result = vpr.Result(ctx.slice.typ(typ))() val post1 = vpr.EqCmp(ctx.slice.array(result)(), aDecl.localVar)() val post2 = vpr.EqCmp(ctx.slice.offset(result)(), offsetDecl.localVar)() - val post3 = vpr.EqCmp(ctx.slice.len(result)(), lenDecl.localVar)() - val post4 = vpr.EqCmp(ctx.slice.cap(result)(), capDecl.localVar)() + val post3 = vpr.EqCmp( + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.slice.len(result)())(), + lenDecl.localVar + )() + val post4 = vpr.EqCmp( + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.slice.cap(result)())(), + capDecl.localVar + )() vpr.Function( s"${Names.sliceConstruct}_${Names.serializeType(typ)}", @@ -417,13 +448,24 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding { val pre1 = synthesized(vpr.LeCmp(vpr.IntLit(0)(), iDecl.localVar))("The low bound of the slice might be negative") val pre2 = synthesized(vpr.LeCmp(iDecl.localVar, jDecl.localVar))("The low bound of the slice might exceed the high bound") val pre3 = synthesized(vpr.LeCmp(jDecl.localVar, kDecl.localVar))("The high bound of the slice might exceed the max bound") - val pre4 = synthesized(vpr.LeCmp(kDecl.localVar, ctx.array.len(aDecl.localVar)()))("The max bound of the slice might exceed the array capacity") + val pre4 = synthesized( + vpr.LeCmp( + kDecl.localVar, + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.array.len(aDecl.localVar)())() + ) + )("The max bound of the slice might exceed the array capacity") val pre5 = synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate") // postconditions val result = vpr.Result(ctx.slice.typ(typ))() val post1 = vpr.EqCmp(ctx.slice.offset(result)(), iDecl.localVar)() - val post2 = vpr.EqCmp(ctx.slice.len(result)(), vpr.Sub(jDecl.localVar, iDecl.localVar)())() - val post3 = vpr.EqCmp(ctx.slice.cap(result)(), vpr.Sub(kDecl.localVar, iDecl.localVar)())() + val post2 = vpr.EqCmp( + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.slice.len(result)())(), + vpr.Sub(jDecl.localVar, iDecl.localVar)() + )() + val post3 = vpr.EqCmp( + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.slice.cap(result)())(), + vpr.Sub(kDecl.localVar, iDecl.localVar)() + )() val post4 = vpr.EqCmp(ctx.slice.array(result)(), aDecl.localVar)() // function body @@ -477,13 +519,24 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding { val pre1 = synthesized(vpr.LeCmp(vpr.IntLit(0)(), iDecl.localVar))("The low bound of the slice might be negative") val pre2 = synthesized(vpr.LeCmp(iDecl.localVar, jDecl.localVar))("The low bound of the slice might exceed the high bound") val pre3 = synthesized(vpr.LeCmp(jDecl.localVar, kDecl.localVar))("The high bound of the slice might exceed the max bound") - val pre4 = synthesized(vpr.LeCmp(kDecl.localVar, ctx.slice.cap(sDecl.localVar)()))("The max bound of the slice might exceed the capacity") + val pre4 = synthesized( + vpr.LeCmp( + kDecl.localVar, + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.slice.cap(sDecl.localVar)())() + ) + )("The max bound of the slice might exceed the capacity") val pre5 = synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate") // postconditions val result = vpr.Result(ctx.slice.typ(typ))() val post1 = vpr.EqCmp(ctx.slice.offset(result)(), vpr.Add(ctx.slice.offset(sDecl.localVar)(), iDecl.localVar)())() - val post2 = vpr.EqCmp(ctx.slice.len(result)(), vpr.Sub(jDecl.localVar, iDecl.localVar)())() - val post3 = vpr.EqCmp(ctx.slice.cap(result)(), vpr.Sub(kDecl.localVar, iDecl.localVar)())() + val post2 = vpr.EqCmp( + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.slice.len(result)())(), + vpr.Sub(jDecl.localVar, iDecl.localVar)() + )() + val post3 = vpr.EqCmp( + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.slice.cap(result)())(), + vpr.Sub(kDecl.localVar, iDecl.localVar)() + )() val post4 = vpr.EqCmp(ctx.slice.array(result)(), ctx.slice.array(sDecl.localVar)())() // function body @@ -529,20 +582,35 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding { def genFunction(typ : vpr.Type)(ctx : Context): vpr.Function = { // declarations val aDecl = vpr.LocalVarDecl("a", ctx.array.typ(typ))() - val iDecl = vpr.LocalVarDecl("i", vpr.Int)() - val jDecl = vpr.LocalVarDecl("j", vpr.Int)() + val iDecl = vpr.LocalVarDecl("i", IntEncodingGenerator.intType)() + val jDecl = vpr.LocalVarDecl("j", IntEncodingGenerator.intType)() + + val iDeclInt = IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(iDecl.localVar)() + val jDeclInt = IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(jDecl.localVar)() // preconditions - val pre1 = synthesized(vpr.LeCmp(vpr.IntLit(0)(), iDecl.localVar))("The low bound of the slice might be negative") - val pre2 = synthesized(vpr.LeCmp(iDecl.localVar, jDecl.localVar))("The low bound of the slice might exceed the high bound") - val pre3 = synthesized(vpr.LeCmp(jDecl.localVar, ctx.array.len(aDecl.localVar)()))("The high bound of the slice might exceed the array capacity") + val pre1 = synthesized(vpr.LeCmp(vpr.IntLit(0)(), iDeclInt))("The low bound of the slice might be negative") + val pre2 = synthesized(vpr.LeCmp(iDeclInt, jDeclInt))("The low bound of the slice might exceed the high bound") + val pre3 = synthesized( + vpr.LeCmp(jDeclInt, + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.array.len(aDecl.localVar)())() + ))("The high bound of the slice might exceed the array capacity") val pre4 = synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate") // postconditions val result = vpr.Result(ctx.slice.typ(typ))() - val post1 = vpr.EqCmp(ctx.slice.offset(result)(), iDecl.localVar)() - val post2 = vpr.EqCmp(ctx.slice.len(result)(), vpr.Sub(jDecl.localVar, iDecl.localVar)())() - val post3 = vpr.EqCmp(ctx.slice.cap(result)(), vpr.Sub(ctx.array.len(aDecl.localVar)(), iDecl.localVar)())() + val post1 = vpr.EqCmp(ctx.slice.offset(result)(), iDeclInt)() + val post2 = vpr.EqCmp( + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.slice.len(result)())(), + vpr.Sub(jDeclInt, iDeclInt)() + )() + val post3 = vpr.EqCmp( + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.slice.cap(result)())(), + vpr.Sub( + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.array.len(aDecl.localVar)())(), + iDeclInt + )() + )() val post4 = vpr.EqCmp(ctx.slice.array(result)(), aDecl.localVar)() // function body @@ -593,13 +661,26 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding { // preconditions val pre1 = synthesized(vpr.LeCmp(vpr.IntLit(0)(), iDecl.localVar))("The low bound of the slice might be negative") val pre2 = synthesized(vpr.LeCmp(iDecl.localVar, jDecl.localVar))("The low bound of the slice might exceed the high bound") - val pre3 = synthesized(vpr.LeCmp(jDecl.localVar, ctx.slice.cap(sDecl.localVar)()))("The high bound of the slice might exceed the capacity") + val pre3 = synthesized( + vpr.LeCmp( + jDecl.localVar, + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.slice.cap(sDecl.localVar)())() + ))("The high bound of the slice might exceed the capacity") val pre4 = synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate") // postconditions val result = vpr.Result(ctx.slice.typ(typ))() val post1 = vpr.EqCmp(ctx.slice.offset(result)(), vpr.Add(ctx.slice.offset(sDecl.localVar)(), iDecl.localVar)())() - val post2 = vpr.EqCmp(ctx.slice.len(result)(), vpr.Sub(jDecl.localVar, iDecl.localVar)())() - val post3 = vpr.EqCmp(ctx.slice.cap(result)(), vpr.Sub(ctx.slice.cap(sDecl.localVar)(), iDecl.localVar)())() + val post2 = vpr.EqCmp( + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.slice.len(result)())(), + vpr.Sub(jDecl.localVar, iDecl.localVar)() + )() + val post3 = vpr.EqCmp( + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.slice.cap(result)())(), + vpr.Sub( + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.slice.cap(sDecl.localVar)())(), + iDecl.localVar + )() + )() val post4 = vpr.EqCmp(ctx.slice.array(result)(), ctx.slice.array(sDecl.localVar)())() // function body @@ -654,8 +735,14 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding { // postconditions val result = vpr.Result(sliceTypT)() val post1 = vpr.EqCmp(ctx.slice.offset(result)(), vpr.IntLit(0)())() - val post2 = vpr.EqCmp(ctx.slice.len(result)(), vpr.IntLit(0)())() - val post3 = vpr.EqCmp(ctx.slice.cap(result)(), vpr.IntLit(0)())() + val post2 = vpr.EqCmp( + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.slice.len(result)())(), + vpr.IntLit(0)() + )() + val post3 = vpr.EqCmp( + IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(ctx.slice.cap(result)())(), + vpr.IntLit(0)() + )() val post4 = vpr.EqCmp(ctx.slice.array(result)(), dfltArrayT)() // function body diff --git a/src/main/scala/viper/gobra/translator/encodings/typeless/BuiltInEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/typeless/BuiltInEncoding.scala index 1efa14940..166271ed7 100644 --- a/src/main/scala/viper/gobra/translator/encodings/typeless/BuiltInEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/typeless/BuiltInEncoding.scala @@ -17,7 +17,7 @@ import viper.gobra.translator.encodings.combinators.Encoding import viper.gobra.translator.context.Context import viper.gobra.translator.util.ViperWriter.MemberWriter import viper.gobra.translator.util.PrimitiveGenerator -import viper.gobra.util.Computation +import viper.gobra.util.{Computation, TypeBounds} import viper.gobra.util.Violation.violation import viper.silver.{ast => vpr} @@ -360,9 +360,9 @@ class BuiltInEncoding extends Encoding { val src = x.info var varCount = 0 - def freshBoundVar(): in.BoundVar = { + def freshBoundVar(kind: TypeBounds.IntegerKind): in.BoundVar = { varCount += 1 - in.BoundVar(s"i$varCount", in.IntT(Addressability.boundVariable))(src) + in.BoundVar(s"i$varCount", in.IntT(Addressability.boundVariable, kind))(src) } def inRange(exp: in.Expr, lower: in.Expr, upper: in.Expr): in.Expr = { @@ -372,15 +372,16 @@ class BuiltInEncoding extends Encoding { )(src) } - def quantify(trigger: in.BoundVar => Vector[in.Trigger], range: in.BoundVar => in.Expr, body: in.BoundVar => in.Assertion): in.Assertion = { - val i = freshBoundVar() + def quantify(qtfiedVarKind: TypeBounds.IntegerKind, trigger: in.BoundVar => Vector[in.Trigger], range: in.BoundVar => in.Expr, body: in.BoundVar => in.Assertion): in.Assertion = { + val i = freshBoundVar(qtfiedVarKind) in.SepForall(Vector(i), trigger(i), in.Implication(range(i), body(i))(src))(src) } def accessSlice(sliceExpr: in.Expr, perm: in.Expr): in.Assertion = quantify( + TypeBounds.DefaultInt, trigger = { i => Vector(in.Trigger(Vector(in.Ref(in.IndexedExp(sliceExpr, i, sliceExpr.typ)(src))(src)))(src)) }, - range = { i => inRange(i, in.IntLit(0)(src), in.Length(sliceExpr)(src)) }, + range = { i => inRange(i, in.IntLit(0)(src), in.Length(sliceExpr, ctx.underlyingType(sliceExpr.typ))(src)) }, body = { i => in.Access(in.Accessible.Address(in.IndexedExp(sliceExpr, i, sliceExpr.typ)(src)), perm)(src) } ) @@ -438,6 +439,7 @@ class BuiltInEncoding extends Encoding { * requires p > 0 * requires forall i int :: { &dst[i] } 0 <= i && i < len(dst) ==> acc(&dst[i]) * requires forall i int :: { &src[i] } 0 <= i && i < len(src) ==> acc(&src[i], p) + * requires integer(len(dst)) + integer(len(src)) <= MAX_INT * ensures len(res) == len(dst) + len(src) * ensures forall i int :: { &res[i] } 0 <= i && i < len(res) ==> acc(&res[i]) * ensures forall i int :: { &src[i] } 0 <= i && i < len(src) ==> acc(&src[i], p) @@ -465,20 +467,30 @@ class BuiltInEncoding extends Encoding { val preSlice = accessSlice(sliceParam, in.FullPerm(src)) val preVariadic = accessSlice(variadicParam, pParam) val pPre = in.ExprAssertion(in.LessCmp(in.NoPerm(src), pParam)(src))(src) - val pres: Vector[in.Assertion] = Vector(pPre, preSlice, preVariadic) + val pSumLengths = in.ExprAssertion( + in.AtMostCmp( + in.Add( + in.Conversion(in.IntT(Addressability.Exclusive), in.Length(sliceParam, sliceType)(src))(src), + in.Conversion(in.IntT(Addressability.Exclusive), in.Length(variadicParam, sliceType)(src))(src) + )(src), + in.IntLit(TypeBounds.DefaultInt.upper)(src) + )(src) + )(src) + val pres: Vector[in.Assertion] = Vector(pPre, preSlice, preVariadic, pSumLengths) // postconditions val postLen = in.ExprAssertion( in.EqCmp( - in.Length(resultParam)(src), - in.Add(in.Length(sliceParam)(src), in.Length(variadicParam)(src))(src) + in.Length(resultParam, sliceType)(src), + in.Add(in.Length(sliceParam, sliceType)(src), in.Length(variadicParam, sliceType)(src))(src) )(src) )(src) val postRes = accessSlice(resultParam, in.FullPerm(src)) val postVariadic = accessSlice(variadicParam, pParam) val postCmpSlice = quantify( + TypeBounds.DefaultInt, trigger = { i => Vector(in.Trigger(Vector(in.Ref(in.IndexedExp(resultParam, i, sliceType)(src))(src)))(src)) }, - range = { inRange(_, in.IntLit(0)(src), in.Length(sliceParam)(src)) }, + range = { inRange(_, in.IntLit(0)(src), in.Length(sliceParam, sliceType)(src)) }, body = { i => in.ExprAssertion( in.GhostEqCmp( @@ -489,13 +501,14 @@ class BuiltInEncoding extends Encoding { } ) val postCmpVariadic = quantify( + TypeBounds.DefaultInt, trigger = { i => Vector(in.Trigger(Vector(in.Ref(in.IndexedExp(resultParam, i, sliceType)(src))(src)))(src)) }, - range = { inRange(_, in.Length(sliceParam)(src), in.Length(resultParam)(src)) }, + range = { inRange(_, in.Length(sliceParam, sliceType)(src), in.Length(resultParam, sliceType)(src)) }, body = { i => in.ExprAssertion( in.GhostEqCmp( in.IndexedExp(resultParam, i, sliceType)(src), - in.IndexedExp(variadicParam, in.Sub(i, in.Length(sliceParam)(src))(src), sliceType)(src), + in.IndexedExp(variadicParam, in.Sub(i, in.Length(sliceParam, sliceType)(src))(src), sliceType)(src), )(src) )(src) } @@ -538,23 +551,25 @@ class BuiltInEncoding extends Encoding { val args = Vector(dstParam, srcParam, pParam) // results - val resParam = in.Parameter.Out("res", in.IntT(Addressability.outParameter))(src) + val resParam = in.Parameter.Out("res", in.IntT(Addressability.outParameter, TypeBounds.DefaultInt))(src) val results = Vector(resParam) // preconditions val pPre = in.ExprAssertion(in.LessCmp(in.NoPerm(src), pParam)(src))(src) val preDst = quantify( + TypeBounds.DefaultInt, trigger = { i => Vector(in.Trigger(Vector(in.Ref(in.IndexedExp(dstParam, i, dstUnderlyingType)(src))(src)))(src)) }, - range = { i => inRange(i, in.IntLit(0)(src), in.Length(dstParam)(src)) }, + range = { i => inRange(i, in.IntLit(0)(src), in.Length(dstParam, dstUnderlyingType)(src)) }, body = { i => in.Access(in.Accessible.Address(in.IndexedExp(dstParam, i, dstUnderlyingType)(src)), in.FullPerm(src))(src) } ) val preSrc = quantify( + TypeBounds.DefaultInt, trigger = { i => Vector(in.Trigger(Vector(in.Ref(in.IndexedExp(srcParam, i, srcUnderlyingType)(src))(src)))(src)) }, - range = { i => inRange(i, in.IntLit(0)(src), in.Length(srcParam)(src)) }, + range = { i => inRange(i, in.IntLit(0)(src), in.Length(srcParam, srcUnderlyingType)(src)) }, body = { i => in.Access(in.Accessible.Address(in.IndexedExp(srcParam, i, srcUnderlyingType)(src)), pParam)(src) } ) @@ -562,24 +577,25 @@ class BuiltInEncoding extends Encoding { // postconditions val postRes1 = in.Implication( - in.AtMostCmp(in.Length(dstParam)(src), in.Length(srcParam)(src))(src), - in.ExprAssertion(in.EqCmp(in.Length(dstParam)(src), resParam)(src))(src) + in.AtMostCmp(in.Length(dstParam, dstUnderlyingType)(src), in.Length(srcParam, srcUnderlyingType)(src))(src), + in.ExprAssertion(in.EqCmp(in.Length(dstParam, dstUnderlyingType)(src), resParam)(src))(src) )(src) val postRes2 = in.Implication( - in.LessCmp(in.Length(srcParam)(src), in.Length(dstParam)(src))(src), - in.ExprAssertion(in.EqCmp(in.Length(srcParam)(src), resParam)(src))(src) + in.LessCmp(in.Length(srcParam, srcUnderlyingType)(src), in.Length(dstParam, dstUnderlyingType)(src))(src), + in.ExprAssertion(in.EqCmp(in.Length(srcParam, srcUnderlyingType)(src), resParam)(src))(src) )(src) // the assertions in the pre-conditions can be reused here val postDst = preDst val postSrc = preSrc val postUpdate = quantify( + TypeBounds.DefaultInt, trigger = { i => Vector(in.Trigger(Vector(in.Ref(in.IndexedExp(dstParam, i, dstUnderlyingType)(src))(src)))(src)) }, range = { i => in.And( - inRange(i, in.IntLit(0)(src), in.Length(srcParam)(src)), - inRange(i, in.IntLit(0)(src), in.Length(dstParam)(src)), + inRange(i, in.IntLit(0)(src), in.Length(srcParam, srcUnderlyingType)(src)), + inRange(i, in.IntLit(0)(src), in.Length(dstParam, dstUnderlyingType)(src)), )(src) }, body = { i => @@ -592,8 +608,9 @@ class BuiltInEncoding extends Encoding { } ) val postSame = quantify( + TypeBounds.DefaultInt, trigger = { i => Vector(in.Trigger(Vector(in.Ref(in.IndexedExp(dstParam, i, dstUnderlyingType)(src))(src)))(src)) }, - range = { i => inRange(i, in.Length(srcParam)(src), in.Length(dstParam)(src)) }, + range = { i => inRange(i, in.Length(srcParam, srcUnderlyingType)(src), in.Length(dstParam, dstUnderlyingType)(src)) }, body = { i => in.ExprAssertion( in.GhostEqCmp( diff --git a/src/main/scala/viper/gobra/translator/encodings/typeless/MemoryEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/typeless/MemoryEncoding.scala index b5149518a..7f0f15742 100644 --- a/src/main/scala/viper/gobra/translator/encodings/typeless/MemoryEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/typeless/MemoryEncoding.scala @@ -18,13 +18,26 @@ class MemoryEncoding extends Encoding { override def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = { case r: in.Ref => ctx.reference(r.ref.op) case x@ in.EqCmp(l, r) => ctx.goEqual(l, r)(x) - case x@ in.UneqCmp(l, r) => ctx.goEqual(l, r)(x).map(v => withSrc(vpr.Not(v), x)) - case x@ in.GhostEqCmp(l, r) => ctx.equal(l, r)(x) - case x@ in.GhostUneqCmp(l, r) => ctx.equal(l, r)(x).map(v => withSrc(vpr.Not(v), x)) - case n@ in.LessCmp(l, r) => for {vl <- ctx.expression(l); vr <- ctx.expression(r)} yield withSrc(vpr.LtCmp(vl, vr), n) - case n@ in.AtMostCmp(l, r) => for {vl <- ctx.expression(l); vr <- ctx.expression(r)} yield withSrc(vpr.LeCmp(vl, vr), n) - case n@ in.GreaterCmp(l, r) => for {vl <- ctx.expression(l); vr <- ctx.expression(r)} yield withSrc(vpr.GtCmp(vl, vr), n) - case n@ in.AtLeastCmp(l, r) => for {vl <- ctx.expression(l); vr <- ctx.expression(r)} yield withSrc(vpr.GeCmp(vl, vr), n) + case x@ in.UneqCmp(l, r) if !ctx.underlyingType(l.typ).isInstanceOf[in.IntT] && + !ctx.underlyingType(r.typ).isInstanceOf[in.IntT] => + ctx.goEqual(l, r)(x).map(v => withSrc(vpr.Not(v), x)) + case x@ in.GhostEqCmp(l, r) => + ctx.equal(l, r)(x) + case x@ in.GhostUneqCmp(l, r) if !ctx.underlyingType(l.typ).isInstanceOf[in.IntT] && + !ctx.underlyingType(r.typ).isInstanceOf[in.IntT] => + ctx.equal(l, r)(x).map(v => withSrc(vpr.Not(v), x)) + case n@ in.LessCmp(l, r) if !ctx.underlyingType(l.typ).isInstanceOf[in.IntT] && + !ctx.underlyingType(r.typ).isInstanceOf[in.IntT] => + for {vl <- ctx.expression(l); vr <- ctx.expression(r)} yield withSrc(vpr.LtCmp(vl, vr), n) + case n@ in.AtMostCmp(l, r) if !ctx.underlyingType(l.typ).isInstanceOf[in.IntT] && + !ctx.underlyingType(r.typ).isInstanceOf[in.IntT] => + for {vl <- ctx.expression(l); vr <- ctx.expression(r)} yield withSrc(vpr.LeCmp(vl, vr), n) + case n@ in.GreaterCmp(l, r) if !ctx.underlyingType(l.typ).isInstanceOf[in.IntT] && + !ctx.underlyingType(r.typ).isInstanceOf[in.IntT] => + for {vl <- ctx.expression(l); vr <- ctx.expression(r)} yield withSrc(vpr.GtCmp(vl, vr), n) + case n@ in.AtLeastCmp(l, r) if !ctx.underlyingType(l.typ).isInstanceOf[in.IntT] && + !ctx.underlyingType(r.typ).isInstanceOf[in.IntT] => + for {vl <- ctx.expression(l); vr <- ctx.expression(r)} yield withSrc(vpr.GeCmp(vl, vr), n) } override def assertion(ctx: Context): in.Assertion ==> CodeWriter[vpr.Exp] = { diff --git a/src/main/scala/viper/gobra/translator/encodings/typeless/TerminationEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/typeless/TerminationEncoding.scala index 679706911..b3ec8a182 100644 --- a/src/main/scala/viper/gobra/translator/encodings/typeless/TerminationEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/typeless/TerminationEncoding.scala @@ -10,6 +10,7 @@ import org.bitbucket.inkytonik.kiama.==> import viper.gobra.ast.{internal => in} import viper.gobra.translator.encodings.combinators.Encoding import viper.gobra.translator.context.Context +import viper.gobra.translator.encodings.IntEncodingGenerator import viper.gobra.translator.util.ViperWriter.CodeWriter import viper.gobra.util.Violation.violation import viper.silver.ast.Member @@ -77,7 +78,17 @@ class TerminationEncoding extends Encoding { for { c <- option(t.cond map ctx.expression) v <- sequence(t.tuple.map { - case e: in.Expr => ctx.expression(e) + case e: in.Expr => + for { + newE <- ctx.expression(e) + } yield e.typ match { + // if we have a numeric decreases measure, we get its int value. this prevents us from having to + // create a new domain per int type. + case t: in.IntT => + IntEncodingGenerator.domainToIntFuncApp(t.kind)(newE)(newE.pos, newE.info, newE.errT) + case _ => newE + } + case p: in.Access => predicateInstance(p)(ctx) case _ => violation("invalid tuple measure argument") }) diff --git a/src/main/scala/viper/gobra/translator/library/arrays/ArraysImpl.scala b/src/main/scala/viper/gobra/translator/library/arrays/ArraysImpl.scala index 777a47556..d15a303c1 100644 --- a/src/main/scala/viper/gobra/translator/library/arrays/ArraysImpl.scala +++ b/src/main/scala/viper/gobra/translator/library/arrays/ArraysImpl.scala @@ -8,6 +8,7 @@ package viper.gobra.translator.library.arrays import viper.gobra.translator.Names import viper.silver.{ast => vpr} +import viper.gobra.translator.encodings.{IntEncoding, IntEncodingGenerator} /** * A specialized version of the array domain, where the element type is a parameter. @@ -24,6 +25,7 @@ class ArraysImpl extends Arrays { */ private lazy val (domain, locFunc, lenFunc) = genDomain + // TODO: change doc /** * Returns domain, loc function, and len function. * @@ -56,12 +58,13 @@ class ArraysImpl extends Arrays { val i = iDecl.localVar val locFunc = vpr.DomainFunc(s"${Names.sharedArrayDomain}loc", Seq(aDecl, iDecl), typeVar)(domainName = domainName) - val lenFunc = vpr.DomainFunc(s"${Names.sharedArrayDomain}len", Seq(aDecl), vpr.Int)(domainName = domainName) + val lenFunc = vpr.DomainFunc(s"${Names.sharedArrayDomain}len", Seq(aDecl), IntEncodingGenerator.intType)(domainName = domainName) val firstFunc = vpr.DomainFunc(s"${Names.sharedArrayDomain}first", Seq(rDecl), domainType)(domainName = domainName) val secondFunc = vpr.DomainFunc(s"${Names.sharedArrayDomain}second", Seq(rDecl), vpr.Int)(domainName = domainName) val locFuncApp = vpr.DomainFuncApp(locFunc, Seq(a, i), typeVarMap)() val lenFuncApp = vpr.DomainFuncApp(lenFunc, Seq(a), typeVarMap)() + val intValLenFuncApp = IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(lenFuncApp)() val injectivity = vpr.AnonymousDomainAxiom( vpr.Forall( @@ -70,7 +73,7 @@ class ArraysImpl extends Arrays { vpr.Implies( vpr.And( vpr.LeCmp(vpr.IntLit(0)(), i)(), - vpr.LtCmp(i, lenFuncApp)() + vpr.LtCmp(i, intValLenFuncApp)() )(), vpr.And( vpr.EqCmp(vpr.DomainFuncApp(firstFunc, Seq(locFuncApp), typeVarMap)(), a)(), @@ -84,7 +87,7 @@ class ArraysImpl extends Arrays { vpr.Forall( Seq(aDecl), Seq(vpr.Trigger(Seq(lenFuncApp))()), - vpr.GeCmp(lenFuncApp, vpr.IntLit(0)())() + vpr.GeCmp(intValLenFuncApp, vpr.IntLit(0)())() )() }(domainName = domainName) diff --git a/src/main/scala/viper/gobra/translator/library/slices/SlicesImpl.scala b/src/main/scala/viper/gobra/translator/library/slices/SlicesImpl.scala index aa1840cb6..f8c366fae 100644 --- a/src/main/scala/viper/gobra/translator/library/slices/SlicesImpl.scala +++ b/src/main/scala/viper/gobra/translator/library/slices/SlicesImpl.scala @@ -6,6 +6,7 @@ package viper.gobra.translator.library.slices +import viper.gobra.translator.encodings.IntEncodingGenerator import viper.gobra.translator.library.arrays.Arrays import viper.silver.plugin.standard.termination import viper.gobra.translator.util.ViperUtil.synthesized @@ -46,6 +47,7 @@ class SlicesImpl(val arrays : Arrays) extends Slices { vpr.Int )(domainName = domainName) + // TODO: doc /** * {{{ * function slen(s : Slice[T]) : Int @@ -54,7 +56,8 @@ class SlicesImpl(val arrays : Arrays) extends Slices { private lazy val slen_func : vpr.DomainFunc = vpr.DomainFunc( "slen", Seq(vpr.LocalVarDecl("s", domainType)()), - vpr.Int + //vpr.Int + IntEncodingGenerator.intType )(domainName = domainName) /** @@ -65,7 +68,8 @@ class SlicesImpl(val arrays : Arrays) extends Slices { private lazy val scap_func : vpr.DomainFunc = vpr.DomainFunc( "scap", Seq(vpr.LocalVarDecl("s", domainType)()), - vpr.Int + //vpr.Int + IntEncodingGenerator.intType )(domainName = domainName) /** @@ -90,7 +94,8 @@ class SlicesImpl(val arrays : Arrays) extends Slices { val sDecl = vpr.LocalVarDecl("s", domainType)() val exp = offset(sDecl.localVar)() - vpr.AnonymousDomainAxiom( + vpr.NamedDomainAxiom( + "slice_offset_nonneg", vpr.Forall( Seq(sDecl), Seq(vpr.Trigger(Seq(exp))()), @@ -108,9 +113,12 @@ class SlicesImpl(val arrays : Arrays) extends Slices { */ private lazy val slice_len_nonneg_axiom : vpr.DomainAxiom = { val sDecl = vpr.LocalVarDecl("s", domainType)() - val exp = len(sDecl.localVar)() + val exp = IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)( + len(sDecl.localVar)() + )() - vpr.AnonymousDomainAxiom( + vpr.NamedDomainAxiom( + "slice_len_nonneg", vpr.Forall( Seq(sDecl), Seq(vpr.Trigger(Seq(exp))()), @@ -128,10 +136,15 @@ class SlicesImpl(val arrays : Arrays) extends Slices { */ private lazy val slice_len_leq_cap_axiom : vpr.DomainAxiom = { val sDecl = vpr.LocalVarDecl("s", domainType)() - val left = len(sDecl.localVar)() - val right = cap(sDecl.localVar)() - - vpr.AnonymousDomainAxiom( + val left = IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)( + len(sDecl.localVar)() + )() + val right = IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)( + cap(sDecl.localVar)() + )() + + vpr.NamedDomainAxiom( + "slice_len_leq_cap", vpr.Forall( Seq(sDecl), Seq(vpr.Trigger(Seq(left))(), vpr.Trigger(Seq(right))()), @@ -151,10 +164,15 @@ class SlicesImpl(val arrays : Arrays) extends Slices { private lazy val slice_cap_leq_alen_axiom : vpr.DomainAxiom = { val sDecl = vpr.LocalVarDecl("s", domainType)() val soffset = offset(sDecl.localVar)() - val scap = cap(sDecl.localVar)() - val alen = arrays.len(array(sDecl.localVar)())() - - vpr.AnonymousDomainAxiom( + val scap = IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)( + cap(sDecl.localVar)() + )() + val alen = IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)( + arrays.len(array(sDecl.localVar)())() + )() + + vpr.NamedDomainAxiom( + "slice_cap_leq_alen", vpr.Forall( Seq(sDecl), Seq(vpr.Trigger(Seq(soffset, scap))(), vpr.Trigger(Seq(alen))()), @@ -197,12 +215,12 @@ class SlicesImpl(val arrays : Arrays) extends Slices { vpr.LeCmp(vpr.IntLit(0)(), off)(), vpr.And( vpr.LeCmp(vpr.IntLit(0)(), leh)(), vpr.And( vpr.LeCmp(leh, cay)(), - vpr.LeCmp(vpr.Add(off,cay)(), arrays.len(arr)())())())())() + vpr.LeCmp(vpr.Add(off,cay)(), IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(arrays.len(arr)())())())())())() val funcAppAxiom1 = array(smake)() val funcAppAxiom2 = offset(smake)() - val funcAppAxiom3 = len(smake)() - val funcAppAxiom4 = cap(smake)() + val funcAppAxiom3 = IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(len(smake)())() + val funcAppAxiom4 = IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(cap(smake)())() val rhsAxiom1 = vpr.EqCmp(funcAppAxiom1, arr)() val rhsAxiom2 = vpr.EqCmp(funcAppAxiom2, off)() val rhsAxiom3 = vpr.EqCmp(funcAppAxiom3, leh)() @@ -257,10 +275,15 @@ class SlicesImpl(val arrays : Arrays) extends Slices { val sarray = array(s)() val soff = offset(s)() - val slen = len(s)() - val scap = cap(s)() - - vpr.AnonymousDomainAxiom( + val slen = IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)( + len(s)() + )() + val scap = IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)( + cap(s)() + )() + + vpr.NamedDomainAxiom( + "slice_constructor_over_deconstructor", vpr.Forall( Seq(sDecl), Seq(vpr.Trigger(Seq(sarray))(), vpr.Trigger(Seq(soff))(), vpr.Trigger(Seq(slen))(), vpr.Trigger(Seq(scap))()), @@ -405,7 +428,7 @@ class SlicesImpl(val arrays : Arrays) extends Slices { override def loc(base : vpr.Exp, index : vpr.Exp)(pos : vpr.Position, info : vpr.Info, errT : vpr.ErrorTrafo) : vpr.Exp = { arrays.loc( array(base)(pos, info, errT), - add(offset(base)(pos, info, errT), index)(pos, info, errT) + add(offset(base)(pos, info, errT), IntEncodingGenerator.domainToIntFuncApp(IntEncodingGenerator.intKind)(index)())(pos, info, errT) )(pos, info, errT) } diff --git a/src/main/scala/viper/gobra/translator/util/DomainGenerator.scala b/src/main/scala/viper/gobra/translator/util/DomainGenerator.scala index f9530f39c..3730930e4 100644 --- a/src/main/scala/viper/gobra/translator/util/DomainGenerator.scala +++ b/src/main/scala/viper/gobra/translator/util/DomainGenerator.scala @@ -29,3 +29,22 @@ trait DomainGenerator[T] extends Generator { vpr.DomainType(domain, domain.typVars.zip(args).toMap) } } + +trait DomainGeneratorWithoutContext[T] extends Generator { + override def finalize(addMemberFn: vpr.Member => Unit): Unit = generatedMember foreach addMemberFn + + private var generatedMember: List[vpr.Domain] = List.empty + private var genMap: Map[T, vpr.Domain] = Map.empty + + def genDomain(x: T): vpr.Domain + + def apply(args: Vector[vpr.Type], x: T): vpr.DomainType = { + val domain = genMap.getOrElse(x, { + val newDomain = genDomain(x) + genMap += x -> newDomain + generatedMember ::= newDomain + newDomain + }) + vpr.DomainType(domain, domain.typVars.zip(args).toMap) + } +} \ No newline at end of file diff --git a/src/main/scala/viper/gobra/translator/util/TypePatterns.scala b/src/main/scala/viper/gobra/translator/util/TypePatterns.scala index dec73f083..fe74714d9 100644 --- a/src/main/scala/viper/gobra/translator/util/TypePatterns.scala +++ b/src/main/scala/viper/gobra/translator/util/TypePatterns.scala @@ -10,6 +10,7 @@ import viper.gobra.ast.{internal => in} import viper.gobra.theory.Addressability import viper.gobra.theory.Addressability.{Exclusive, Shared} import viper.gobra.translator.context.Context +import viper.gobra.util.TypeBounds.IntegerKind import scala.annotation.tailrec @@ -76,8 +77,11 @@ object TypePatterns { } object Int { - def unapply(arg: in.Type): Boolean = - underlyingType(arg)(ctx).isInstanceOf[in.IntT] + def unapply(arg: in.Type): Option[IntegerKind] = + underlyingType(arg)(ctx) match { + case in.IntT(_, kind) => Some(kind) + case _ => None + } } object Void { diff --git a/src/main/scala/viper/gobra/util/TypeBounds.scala b/src/main/scala/viper/gobra/util/TypeBounds.scala index bcbf82f81..30845c972 100644 --- a/src/main/scala/viper/gobra/util/TypeBounds.scala +++ b/src/main/scala/viper/gobra/util/TypeBounds.scala @@ -54,13 +54,12 @@ object TypeBounds { object SignedInteger16 extends BoundedIntegerKind("int16", 16) with Signed sealed abstract class AbstractSignedInteger32(override val name: String) extends BoundedIntegerKind(name, 32) with Signed - object DefaultInt extends AbstractSignedInteger32("int") // int definition when Gobra runs in 32-bit (i.e. default) mode object SignedInteger32 extends AbstractSignedInteger32("int32") object Rune extends AbstractSignedInteger32("rune") sealed abstract class AbstractSignedInteger64(override val name: String) extends BoundedIntegerKind(name, 64) with Signed object SignedInteger64 extends AbstractSignedInteger64("int64") - object IntWith64Bit extends AbstractSignedInteger64("int") // int definition when Gobra runs in 64-bit mode + // object IntWith64Bit extends AbstractSignedInteger64("int") // int definition when Gobra runs in 64-bit mode sealed abstract class AbstractUnsignedInteger8(override val name: String) extends BoundedIntegerKind(name, 8) with Unsigned object Byte extends AbstractUnsignedInteger8("byte") with Unsigned @@ -70,13 +69,15 @@ object TypeBounds { sealed abstract class AbstractUnsignedInteger32(override val name: String) extends BoundedIntegerKind(name, 32) with Unsigned object UnsignedInteger32 extends AbstractUnsignedInteger32("uint32") - object DefaultUInt extends AbstractUnsignedInteger32("uint") // uint definition when Gobra runs in 32-bit mode sealed abstract class AbstractUnsignedInteger64(override val name: String) extends BoundedIntegerKind(name, 64) with Unsigned object UnsignedInteger64 extends AbstractUnsignedInteger64("uint64") - object UIntWith64Bit extends AbstractUnsignedInteger64("uint") // uint definition when Gobra runs in 64-bit mode + // object UIntWith64Bit extends AbstractUnsignedInteger64("uint") // uint definition when Gobra runs in 64-bit mode object UIntPtr extends AbstractUnsignedInteger64("uintptr") + object DefaultInt extends AbstractSignedInteger64("int") + object DefaultUInt extends AbstractUnsignedInteger64("uint") // uint definition when Gobra runs in 32-bit mode + def merge(integerKind1: IntegerKind, integerKind2: IntegerKind): IntegerKind = (integerKind1, integerKind2) match { case (a, b) if a == b => a case (a, UnboundedInteger) => a