search

uuverifiers / princess

The Princess Theorem Prover
Other
22 stars 4 forks source link

Princess crashes in RShiftCastSplitter #13

Closed daniel-raffler closed 1 month ago

daniel-raffler commented 1 month ago

Hello, this is another issue I found while using CPAchecker with Princess. Unfortunately I haven't had much luck trying to pin the problem down. However, maybe the stack trace can be of help:

Exception in thread "main" ap.api.SimpleAPI$SimpleAPIForwardedException: Internal exception: java.lang.UnsupportedOperationException: Value too big to be converted to int
    at ap.api.SimpleAPI.ap$api$SimpleAPI$$evalProverResult(SimpleAPI.scala:2179)
    at ap.api.SimpleAPI.$anonfun$getOrUpdateLastStatus$1(SimpleAPI.scala:2115)
    at ap.api.SimpleAPI.$anonfun$getOrUpdateLastStatus$1$adapted(SimpleAPI.scala:2115)
    at scala.Option.foreach(Option.scala:437)
    at ap.api.SimpleAPI.getOrUpdateLastStatus(SimpleAPI.scala:2115)
    at ap.api.SimpleAPI.getStatusHelp(SimpleAPI.scala:2121)
    at ap.api.SimpleAPI.getStatusWithDeadline(SimpleAPI.scala:2095)
    at ap.api.SimpleAPI.checkSatHelp(SimpleAPI.scala:2018)
    at ap.api.SimpleAPI.checkSat(SimpleAPI.scala:1946)
    at org.sosy_lab.java_smt.solvers.princess.PrincessAbstractProver.isUnsat(PrincessAbstractProver.java:79)
    at org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper.isUnsat(BasicProverWithAssumptionsWrapper.java:65)
    at org.sosy_lab.cpachecker.util.predicates.smt.BasicProverEnvironmentView.isUnsat(BasicProverEnvironmentView.java:61)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.boundedModelCheck(AbstractBMCAlgorithm.java:712)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.boundedModelCheck(AbstractBMCAlgorithm.java:686)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.BMCAlgorithm.boundedModelCheck(BMCAlgorithm.java:158)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.run(AbstractBMCAlgorithm.java:454)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.BMCAlgorithm.run(BMCAlgorithm.java:130)
    at org.sosy_lab.cpachecker.core.CPAchecker.runAlgorithm(CPAchecker.java:489)
    at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:357)
    at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:171)
Caused by: java.lang.UnsupportedOperationException: Value too big to be converted to int
    at ap.basetypes.IdealInt.intValueSafe(IdealInt.scala:896)
    at ap.theories.bitvectors.RShiftCastSplitter$.$anonfun$shiftCastActions$9(ShiftCastSplitter.scala:403)
    at ap.theories.bitvectors.RShiftCastSplitter$.$anonfun$shiftCastActions$9$adapted(ShiftCastSplitter.scala:333)
    at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:575)
    at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:573)
    at scala.collection.AbstractIterable.foreach(Iterable.scala:933)
    at ap.theories.bitvectors.RShiftCastSplitter$.shiftCastActions(ShiftCastSplitter.scala:333)
    at ap.theories.bitvectors.ModPlugin$.modShiftCast(ModPlugin.scala:227)
    at ap.theories.bitvectors.ModPlugin$.handleGoal(ModPlugin.scala:175)
    at ap.proof.theoryPlugins.PluginSequence.handleGoal(Plugin.scala:324)
    at ap.proof.theoryPlugins.PluginTask.apply(Plugin.scala:493)
    at ap.proof.goal.Goal.step(Goal.scala:423)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:489)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:622)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:622)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver$IncProverImpl.checkValidityDir(ModelSearchProver.scala:1119)
    at ap.api.ProofThreadRunnable$$anonfun$1.$anonfun$applyOrElse$2(ProofThread.scala:157)
    at ap.util.Timeout$.catchTimeout(Timeout.scala:100)
    at ap.api.ProofThreadRunnable$$anonfun$1.applyOrElse(ProofThread.scala:158)
    at scala.runtime.AbstractPartialFunction.apply(AbstractPartialFunction.scala:35)
    at ap.api.ProofThreadRunnable.$anonfun$run$2(ProofThread.scala:213)
    at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
    at scala.util.DynamicVariable.withValue(DynamicVariable.scala:59)
    at ap.util.Timeout$.withChecker(Timeout.scala:56)
    at ap.api.ProofThreadRunnable.run(ProofThread.scala:203)
    at java.base/java.lang.Thread.run(Thread.java:1570)

The formula that Princess it's trying to solve looks something like this:

(declare-fun __+Infinity__ () Real)
(declare-fun __-Infinity__ () Real)
(declare-fun |__ADDRESS_OF_main::ew_u@| () (_ BitVec 32))
(declare-fun |__ADDRESS_OF_main::iw_u@| () (_ BitVec 32))
(declare-fun __NaN__ () Real)
(declare-fun __dummy_variable_dumping_formulas__ () Bool)
(declare-fun |main::ew_u$parts$lsw@3| () (_ BitVec 32))
(declare-fun |main::ew_u$parts$msw@3| () (_ BitVec 32))
(declare-fun |main::ew_u$value@3| () Real)
(declare-fun |main::i0@3| () (_ BitVec 32))
(declare-fun |main::i0@4| () (_ BitVec 32))
(declare-fun |main::iw_u$value@2| () Real)
(declare-fun |main::j0@3| () (_ BitVec 32))
(declare-fun |main::res@2| () Real)
(declare-fun |main::tmp1@1| () (_ BitVec 32))
(declare-fun |main::tmp1@2| () (_ BitVec 32))
(declare-fun |main::x@2| () Real)
(declare-fun __interpret_FloatingPoint<exp=11,mant=52>_as_Bitvector<64>__ (Real) (_ BitVec 64))
(define-fun abbrev_12 () Bool (and (and (and (and (= |main::x@2| (ite (= (Rat_int 0) (Rat_int 0)) __NaN__ (ite (<= 0 (+ (+ (Rat_int 0) (* (- 1) (Rat_int 0))) (- 1))) __-Infinity__ __+Infinity__))) (and (and (bvslt (_ bv0 32) |__ADDRESS_OF_main::ew_u@|) (= (bvurem |__ADDRESS_OF_main::ew_u@| (_ bv4 32)) (bvurem (_ bv0 32) (_ bv4 32)))) (bvslt (_ bv0 32) (bvadd |__ADDRESS_OF_main::ew_u@| (_ bv8 32))))) (and (and (= |main::ew_u$value@3| |main::x@2|) (= |main::ew_u$parts$lsw@3| ((_ extract 31 0) (__interpret_FloatingPoint<exp=11,mant=52>_as_Bitvector<64>__ |main::x@2|)))) (= |main::ew_u$parts$msw@3| ((_ extract 63 32) (__interpret_FloatingPoint<exp=11,mant=52>_as_Bitvector<64>__ |main::x@2|))))) (= |main::i0@3| |main::ew_u$parts$msw@3|)) (= |main::j0@3| (bvsub (bvand (bvashr |main::i0@3| (_ bv20 32)) (_ bv2047 32)) (_ bv1023 32)))))
(define-fun abbrev_47 () Bool (bvslt |main::j0@3| (_ bv20 32)))
(assert (= __dummy_variable_dumping_formulas__ (and (and (and (or (and (and (and abbrev_12 abbrev_47) (= |main::tmp1@2| (bvashr (_ bv1048575 32) |main::j0@3|))) (= |main::i0@4| (bvand |main::i0@3| (bvnot |main::tmp1@2|)))) (and (and abbrev_12 (not abbrev_47)) (and (= |main::i0@4| |main::i0@3|) (= |main::tmp1@2| |main::tmp1@1|)))) (and (and (bvslt (bvadd |__ADDRESS_OF_main::ew_u@| (_ bv8 32)) |__ADDRESS_OF_main::iw_u@|) (= (bvurem |__ADDRESS_OF_main::iw_u@| (_ bv4 32)) (bvurem (_ bv0 32) (_ bv4 32)))) (bvslt (_ bv0 32) (bvadd |__ADDRESS_OF_main::iw_u@| (_ bv8 32))))) (= |main::res@2| |main::iw_u$value@2|)) (= |main::res@2| |main::res@2|))))

I'll keep looking for a smaller example, but maybe you already have an idea what could be going wrong here?

pruemmer commented 1 month ago

I could not reproduce this problem, but I tried to get rid of the failing conversion. Does this error still occur with the latest version?

daniel-raffler commented 1 month ago

Thanks for your effort! Unfortunately it's not quite gone yet. With the new version I'm getting:

Exception in thread "main" ap.api.SimpleAPI$SimpleAPIForwardedException: Internal exception: java.lang.UnsupportedOperationException: Value too big to be converted to int
    at ap.api.SimpleAPI.ap$api$SimpleAPI$$evalProverResult(SimpleAPI.scala:2179)
    at ap.api.SimpleAPI.$anonfun$getOrUpdateLastStatus$1(SimpleAPI.scala:2115)
    at ap.api.SimpleAPI.$anonfun$getOrUpdateLastStatus$1$adapted(SimpleAPI.scala:2115)
    at scala.Option.foreach(Option.scala:437)
    at ap.api.SimpleAPI.getOrUpdateLastStatus(SimpleAPI.scala:2115)
    at ap.api.SimpleAPI.getStatusHelp(SimpleAPI.scala:2121)
    at ap.api.SimpleAPI.getStatusWithDeadline(SimpleAPI.scala:2095)
    at ap.api.SimpleAPI.checkSatHelp(SimpleAPI.scala:2018)
    at ap.api.SimpleAPI.checkSat(SimpleAPI.scala:1946)
    at org.sosy_lab.java_smt.solvers.princess.PrincessAbstractProver.isUnsat(PrincessAbstractProver.java:79)
    at org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper.isUnsat(BasicProverWithAssumptionsWrapper.java:65)
    at org.sosy_lab.cpachecker.util.predicates.smt.BasicProverEnvironmentView.isUnsat(BasicProverEnvironmentView.java:61)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.boundedModelCheck(AbstractBMCAlgorithm.java:711)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.boundedModelCheck(AbstractBMCAlgorithm.java:686)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.BMCAlgorithm.boundedModelCheck(BMCAlgorithm.java:158)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.run(AbstractBMCAlgorithm.java:454)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.BMCAlgorithm.run(BMCAlgorithm.java:130)
    at org.sosy_lab.cpachecker.core.CPAchecker.runAlgorithm(CPAchecker.java:489)
    at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:357)
    at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:171)
Caused by: java.lang.UnsupportedOperationException: Value too big to be converted to int
    at ap.basetypes.IdealInt.intValueSafe(IdealInt.scala:896)
    at ap.basetypes.IdealInt$.pow2(IdealInt.scala:156)
    at ap.theories.bitvectors.ModuloArithmetic$.pow2(ModuloArithmetic.scala:85)
    at ap.theories.bitvectors.RShiftCastSplitter$.rshiftToExtract(ShiftCastSplitter.scala:308)
    at ap.theories.bitvectors.RShiftCastSplitter$.$anonfun$shiftCastActions$9(ShiftCastSplitter.scala:428)
    at ap.theories.bitvectors.RShiftCastSplitter$.$anonfun$shiftCastActions$9$adapted(ShiftCastSplitter.scala:358)
    at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:563)
    at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:561)
    at scala.collection.AbstractIterable.foreach(Iterable.scala:926)
    at ap.theories.bitvectors.RShiftCastSplitter$.shiftCastActions(ShiftCastSplitter.scala:358)
    at ap.theories.bitvectors.ModPlugin$.modShiftCast(ModPlugin.scala:227)
    at ap.theories.bitvectors.ModPlugin$.handleGoal(ModPlugin.scala:175)
    at ap.proof.theoryPlugins.PluginSequence.handleGoal(Plugin.scala:324)
    at ap.proof.theoryPlugins.PluginTask.apply(Plugin.scala:493)
    at ap.proof.goal.Goal.step(Goal.scala:423)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:489)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:622)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:622)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:622)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:622)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver$IncProverImpl.checkValidityDir(ModelSearchProver.scala:1119)
    at ap.api.ProofThreadRunnable$$anonfun$1.$anonfun$applyOrElse$2(ProofThread.scala:157)
    at ap.util.Timeout$.catchTimeout(Timeout.scala:100)
    at ap.api.ProofThreadRunnable$$anonfun$1.applyOrElse(ProofThread.scala:158)
    at scala.runtime.AbstractPartialFunction.apply(AbstractPartialFunction.scala:35)
    at ap.api.ProofThreadRunnable.$anonfun$run$2(ProofThread.scala:213)
    at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
    at scala.util.DynamicVariable.withValue(DynamicVariable.scala:59)
    at ap.util.Timeout$.withChecker(Timeout.scala:56)
    at ap.api.ProofThreadRunnable.run(ProofThread.scala:203)
    at java.base/java.lang.Thread.run(Thread.java:1575)

I'll try to find a better example, but this one might be hard to debug.

daniel-raffler commented 1 month ago

I still haven't been able to find a smaller example. However, here is the Scala code that Princess generates for the query:

import ap.SimpleAPI
import ap.basetypes.IdealInt
import ap.parser._
import ap.theories.rationals.Rationals
import org.scalatest.funsuite.AnyFunSuite

class ModShifterBug extends AnyFunSuite {

  import ap.parser.IExpression.{Sort => _}
  import ap.theories.bitvectors.ModuloArithmetic._;

  val withAssertions = true;

  test("ModShifter bug") {
    SimpleAPI.withProver(enableAssert = withAssertions, tightFunctionScopes = true, genTotalityAxioms = false) { p =>
      import IExpression._
      import p._
      // addConstantRaw(__negativeInfinity__)
      val __negativeInfinity__ = createConstant("__negativeInfinity__", ap.theories.rationals.Rationals.dom)
      // addConstantRaw(__positiveInfinity__)
      val __positiveInfinity__ = createConstant("__positiveInfinity__", ap.theories.rationals.Rationals.dom)
      // addConstantRaw(__NaN__)
      val __NaN__ = createConstant("__NaN__", ap.theories.rationals.Rationals.dom)
      // addFunction(__string__)
      val __string__ = createFunction("__string__", List(Sort.Integer), ap.theories.ModuloArithmetic.ModSort(0, IdealInt("4294967295")))
      // addFunction(rationalMult)
      val rationalMult = createFunction("rationalMult", List(ap.theories.rationals.Rationals.dom, ap.theories.rationals.Rationals.dom), ap.theories.rationals.Rationals.dom)
      // addFunction(rationalDiv)
      val rationalDiv = createFunction("rationalDiv", List(ap.theories.rationals.Rationals.dom, ap.theories.rationals.Rationals.dom), ap.theories.rationals.Rationals.dom)
      // addFunction(__isSubnormal__)
      val __isSubnormal__ = createFunction("__isSubnormal__", List(ap.theories.rationals.Rationals.dom), Sort.Bool)
      // addFunction(integerMod)
      val integerMod = createFunction("integerMod", List(Sort.Integer, Sort.Integer), Sort.Integer)
      // addFunction(sqrt)
      val sqrt = createFunction("sqrt", List(ap.theories.rationals.Rationals.dom), ap.theories.rationals.Rationals.dom)
      // addFunction(integerMult)
      val integerMult = createFunction("integerMult", List(Sort.Integer, Sort.Integer), Sort.Integer)
      // addFunction(__isNormal__)
      val __isNormal__ = createFunction("__isNormal__", List(ap.theories.rationals.Rationals.dom), Sort.Bool)
      // addFunction(rationalMod)
      val rationalMod = createFunction("rationalMod", List(ap.theories.rationals.Rationals.dom, ap.theories.rationals.Rationals.dom), ap.theories.rationals.Rationals.dom)
      // addFunction(integerDiv)
      val integerDiv = createFunction("integerDiv", List(Sort.Integer, Sort.Integer), Sort.Integer)
      // addConstantRaw(main__xat2)
      val main__xat2 = createConstant("main__xat2", ap.theories.rationals.Rationals.dom)
      // addConstantRaw(floor_double__xat2)
      val floor_double__xat2 = createConstant("floor_double__xat2", ap.theories.rationals.Rationals.dom)
      // addConstantRaw(__ADDRESS_OF_floor_double__ew_uat)
      val __ADDRESS_OF_floor_double__ew_uat = createConstant("__ADDRESS_OF_floor_double__ew_uat", ap.theories.ModuloArithmetic.ModSort(0, IdealInt("4294967295")))
      // addConstantRaw(floor_double__ew_u_valueat3)
      val floor_double__ew_u_valueat3 = createConstant("floor_double__ew_u_valueat3", ap.theories.rationals.Rationals.dom)
      // addFunction(__interpret_FloatingPointDouble_as_BitvectorLong__)
      val __interpret_FloatingPointDouble_as_BitvectorLong__ = createFunction("__interpret_FloatingPointDouble_as_BitvectorLong__", List(ap.theories.rationals.Rationals.dom), ap.theories.ModuloArithmetic.ModSort(0, IdealInt("18446744073709551615")))
      // addConstantRaw(floor_double__ew_u_parts_lswat3)
      val floor_double__ew_u_parts_lswat3 = createConstant("floor_double__ew_u_parts_lswat3", ap.theories.ModuloArithmetic.ModSort(0, IdealInt("4294967295")))
      // addConstantRaw(floor_double__ew_u_parts_mswat3)
      val floor_double__ew_u_parts_mswat3 = createConstant("floor_double__ew_u_parts_mswat3", ap.theories.ModuloArithmetic.ModSort(0, IdealInt("4294967295")))
      // addConstantRaw(floor_double__i0at3)
      val floor_double__i0at3 = createConstant("floor_double__i0at3", ap.theories.ModuloArithmetic.ModSort(0, IdealInt("4294967295")))
      // addConstantRaw(floor_double__i1at3)
      val floor_double__i1at3 = createConstant("floor_double__i1at3", ap.theories.ModuloArithmetic.ModSort(0, IdealInt("4294967295")))
      // addConstantRaw(floor_double__j0at3)
      val floor_double__j0at3 = createConstant("floor_double__j0at3", ap.theories.ModuloArithmetic.ModSort(0, IdealInt("4294967295")))
      // addConstantRaw(floor_double__iat3)
      val floor_double__iat3 = createConstant("floor_double__iat3", ap.theories.ModuloArithmetic.ModSort(0, IdealInt("4294967295")))
      // addConstantRaw(floor_double____retval__at2)
      val floor_double____retval__at2 = createConstant("floor_double____retval__at2", ap.theories.rationals.Rationals.dom)
      // addConstantRaw(floor_double__iat2)
      val floor_double__iat2 = createConstant("floor_double__iat2", ap.theories.ModuloArithmetic.ModSort(0, IdealInt("4294967295")))
      // addConstantRaw(__ADDRESS_OF_floor_double__iw_uat)
      val __ADDRESS_OF_floor_double__iw_uat = createConstant("__ADDRESS_OF_floor_double__iw_uat", ap.theories.ModuloArithmetic.ModSort(0, IdealInt("4294967295")))
      // addConstantRaw(floor_double__iw_u_valueat2)
      val floor_double__iw_u_valueat2 = createConstant("floor_double__iw_u_valueat2", ap.theories.rationals.Rationals.dom)
      // addFunction(__interpret_BitvectorLong_as_FloatingPointDouble__)
      val __interpret_BitvectorLong_as_FloatingPointDouble__ = createFunction("__interpret_BitvectorLong_as_FloatingPointDouble__", List(ap.theories.ModuloArithmetic.ModSort(0, IdealInt("18446744073709551615"))), ap.theories.rationals.Rationals.dom)
      // addConstantRaw(floor_double__iw_u_valueat3)
      val floor_double__iw_u_valueat3 = createConstant("floor_double__iw_u_valueat3", ap.theories.rationals.Rationals.dom)
      // addConstantRaw(floor_double__iw_u_parts_mswat3)
      val floor_double__iw_u_parts_mswat3 = createConstant("floor_double__iw_u_parts_mswat3", ap.theories.ModuloArithmetic.ModSort(0, IdealInt("4294967295")))
      // addConstantRaw(floor_double__iw_u_valueat4)
      val floor_double__iw_u_valueat4 = createConstant("floor_double__iw_u_valueat4", ap.theories.rationals.Rationals.dom)
      // addConstantRaw(floor_double__iw_u_parts_lswat3)
      val floor_double__iw_u_parts_lswat3 = createConstant("floor_double__iw_u_parts_lswat3", ap.theories.ModuloArithmetic.ModSort(0, IdealInt("4294967295")))
      // addConstantRaw(floor_double__xat3)
      val floor_double__xat3 = createConstant("floor_double__xat3", ap.theories.rationals.Rationals.dom)
      // addConstantRaw(floor_double__iw_u_parts_lswat1)
      val floor_double__iw_u_parts_lswat1 = createConstant("floor_double__iw_u_parts_lswat1", ap.theories.ModuloArithmetic.ModSort(0, IdealInt("4294967295")))
      // addConstantRaw(floor_double__iw_u_parts_mswat1)
      val floor_double__iw_u_parts_mswat1 = createConstant("floor_double__iw_u_parts_mswat1", ap.theories.ModuloArithmetic.ModSort(0, IdealInt("4294967295")))
      // addConstantRaw(floor_double__iw_u_valueat1)
      val floor_double__iw_u_valueat1 = createConstant("floor_double__iw_u_valueat1", ap.theories.rationals.Rationals.dom)
      // addConstantRaw(main__resat3)
      val main__resat3 = createConstant("main__resat3", ap.theories.rationals.Rationals.dom)
      // addConstantRaw(isnan_double__xat2)
      val isnan_double__xat2 = createConstant("isnan_double__xat2", ap.theories.rationals.Rationals.dom)
      // addConstantRaw(isnan_double____retval__at2)
      val isnan_double____retval__at2 = createConstant("isnan_double____retval__at2", ap.theories.ModuloArithmetic.ModSort(0, IdealInt("4294967295")))
      // addConstantRaw(main____CPAchecker_TMP_0at3)
      val main____CPAchecker_TMP_0at3 = createConstant("main____CPAchecker_TMP_0at3", ap.theories.ModuloArithmetic.ModSort(0, IdealInt("4294967295")))
      // addConstantRaw(main____retval__at2)
      val main____retval__at2 = createConstant("main____retval__at2", ap.theories.ModuloArithmetic.ModSort(0, IdealInt("4294967295")))

      scope {
        setPartitionNumber(0)
        val abbrev_12 = abbrev((((((((main__xat2 === ITermITE((Rationals.frac(0, 1) === Rationals.frac(0, 1)), __NaN__, ITermITE(((Rationals.frac(0, 1) + (Rationals.frac(0, 1) * -1)) >= 1), __negativeInfinity__, __positiveInfinity__))) & (floor_double__xat2 === main__xat2)) & ((bv_slt(32, mod_cast(0, IdealInt("4294967295"), 0), __ADDRESS_OF_floor_double__ew_uat) & (bv_urem(32, __ADDRESS_OF_floor_double__ew_uat, mod_cast(0, IdealInt("4294967295"), 4)) === bv_urem(32, mod_cast(0, IdealInt("4294967295"), 0), mod_cast(0, IdealInt("4294967295"), 4)))) & bv_slt(32, mod_cast(0, IdealInt("4294967295"), 0), bv_add(32, __ADDRESS_OF_floor_double__ew_uat, mod_cast(0, IdealInt("4294967295"), 8))))) & (((floor_double__ew_u_valueat3 === floor_double__xat2) & (floor_double__ew_u_parts_lswat3 === bv_extract(31, 0, __interpret_FloatingPointDouble_as_BitvectorLong__(floor_double__xat2)))) & (floor_double__ew_u_parts_mswat3 === bv_extract(63, 32, __interpret_FloatingPointDouble_as_BitvectorLong__(floor_double__xat2))))) & (floor_double__i0at3 === floor_double__ew_u_parts_mswat3)) & (floor_double__i1at3 === floor_double__ew_u_parts_lswat3)) & (floor_double__j0at3 === bv_sub(32, bv_and(32, bv_ashr(32, floor_double__i0at3, mod_cast(0, IdealInt("4294967295"), 20)), mod_cast(0, IdealInt("4294967295"), 2047)), mod_cast(0, IdealInt("4294967295"), 1023)))), "abbrev_12")
        !!((((((((((((((((((abbrev_12 & bv_slt(32, floor_double__j0at3, mod_cast(0, IdealInt("4294967295"), 20))) & bv_slt(32, floor_double__j0at3, mod_cast(0, IdealInt("4294967295"), 0))) & !(((Rationals.frac(IdealInt("1000000000000000052504760255204420248704468581108159154915854115511802457988908195786371375080447864043704443832883878176942523235360430575644792184786706982848387200926575803737830233794788090059368953234970799945081119038967640880074652742780142494579258788820056842838115669472196386865459400540160"), 1) + floor_double__xat2) + (Rationals.frac(0, 1) * -1)) >= 1)) & (floor_double__iat3 === floor_double__iat2)) | (((((abbrev_12 & bv_slt(32, floor_double__j0at3, mod_cast(0, IdealInt("4294967295"), 20))) & !bv_slt(32, floor_double__j0at3, mod_cast(0, IdealInt("4294967295"), 0))) & (floor_double__iat3 === bv_ashr(32, mod_cast(0, IdealInt("4294967295"), 1048575), floor_double__j0at3))) & !((bv_and(32, floor_double__i0at3, floor_double__iat3) === mod_cast(0, IdealInt("4294967295"), 0)) & (floor_double__i1at3 === mod_cast(0, IdealInt("4294967295"), 0)))) & !(((Rationals.frac(IdealInt("1000000000000000052504760255204420248704468581108159154915854115511802457988908195786371375080447864043704443832883878176942523235360430575644792184786706982848387200926575803737830233794788090059368953234970799945081119038967640880074652742780142494579258788820056842838115669472196386865459400540160"), 1) + floor_double__xat2) + (Rationals.frac(0, 1) * -1)) >= 1))) | (((((abbrev_12 & !bv_slt(32, floor_double__j0at3, mod_cast(0, IdealInt("4294967295"), 20))) & !bv_slt(32, mod_cast(0, IdealInt("4294967295"), 51), floor_double__j0at3)) & (floor_double__iat3 === bv_lshr(32, mod_cast(0, IdealInt("4294967295"), IdealInt("4294967295")), bv_sub(32, floor_double__j0at3, mod_cast(0, IdealInt("4294967295"), 20))))) & !(bv_and(32, floor_double__i1at3, floor_double__iat3) === mod_cast(0, IdealInt("4294967295"), 0))) & !(((Rationals.frac(IdealInt("1000000000000000052504760255204420248704468581108159154915854115511802457988908195786371375080447864043704443832883878176942523235360430575644792184786706982848387200926575803737830233794788090059368953234970799945081119038967640880074652742780142494579258788820056842838115669472196386865459400540160"), 1) + floor_double__xat2) + (Rationals.frac(0, 1) * -1)) >= 1))) & ((bv_slt(32, bv_add(32, __ADDRESS_OF_floor_double__ew_uat, mod_cast(0, IdealInt("4294967295"), 8)), __ADDRESS_OF_floor_double__iw_uat) & (bv_urem(32, __ADDRESS_OF_floor_double__iw_uat, mod_cast(0, IdealInt("4294967295"), 4)) === bv_urem(32, mod_cast(0, IdealInt("4294967295"), 0), mod_cast(0, IdealInt("4294967295"), 4)))) & bv_slt(32, mod_cast(0, IdealInt("4294967295"), 0), bv_add(32, __ADDRESS_OF_floor_double__iw_uat, mod_cast(0, IdealInt("4294967295"), 8))))) & ((floor_double__iw_u_valueat3 === __interpret_BitvectorLong_as_FloatingPointDouble__(bv_concat(32, 32, bv_extract(31, 0, floor_double__i0at3), bv_extract(31, 0, __interpret_FloatingPointDouble_as_BitvectorLong__(floor_double__iw_u_valueat2))))) & (floor_double__iw_u_parts_mswat3 === floor_double__i0at3))) & ((floor_double__iw_u_valueat4 === __interpret_BitvectorLong_as_FloatingPointDouble__(bv_concat(32, 32, bv_extract(63, 32, __interpret_FloatingPointDouble_as_BitvectorLong__(floor_double__iw_u_valueat3)), bv_extract(31, 0, floor_double__i1at3)))) & (floor_double__iw_u_parts_lswat3 === floor_double__i1at3))) & (floor_double__xat3 === floor_double__iw_u_valueat4)) & (floor_double____retval__at2 === floor_double__xat3)) | (((((((abbrev_12 & bv_slt(32, floor_double__j0at3, mod_cast(0, IdealInt("4294967295"), 20))) & !bv_slt(32, floor_double__j0at3, mod_cast(0, IdealInt("4294967295"), 0))) & (floor_double__iat3 === bv_ashr(32, mod_cast(0, IdealInt("4294967295"), 1048575), floor_double__j0at3))) & ((bv_and(32, floor_double__i0at3, floor_double__iat3) === mod_cast(0, IdealInt("4294967295"), 0)) & (floor_double__i1at3 === mod_cast(0, IdealInt("4294967295"), 0)))) & (floor_double____retval__at2 === floor_double__xat2)) | ((((((abbrev_12 & !bv_slt(32, floor_double__j0at3, mod_cast(0, IdealInt("4294967295"), 20))) & bv_slt(32, mod_cast(0, IdealInt("4294967295"), 51), floor_double__j0at3)) & (floor_double__j0at3 === mod_cast(0, IdealInt("4294967295"), 1024))) & (floor_double____retval__at2 === (floor_double__xat2 + floor_double__xat2))) & (floor_double__iat3 === floor_double__iat2)) | ((((((abbrev_12 & !bv_slt(32, floor_double__j0at3, mod_cast(0, IdealInt("4294967295"), 20))) & bv_slt(32, mod_cast(0, IdealInt("4294967295"), 51), floor_double__j0at3)) & !(floor_double__j0at3 === mod_cast(0, IdealInt("4294967295"), 1024))) & (floor_double____retval__at2 === floor_double__xat2)) & (floor_double__iat3 === floor_double__iat2)) | (((((abbrev_12 & !bv_slt(32, floor_double__j0at3, mod_cast(0, IdealInt("4294967295"), 20))) & !bv_slt(32, mod_cast(0, IdealInt("4294967295"), 51), floor_double__j0at3)) & (floor_double__iat3 === bv_lshr(32, mod_cast(0, IdealInt("4294967295"), IdealInt("4294967295")), bv_sub(32, floor_double__j0at3, mod_cast(0, IdealInt("4294967295"), 20))))) & (bv_and(32, floor_double__i1at3, floor_double__iat3) === mod_cast(0, IdealInt("4294967295"), 0))) & (floor_double____retval__at2 === floor_double__xat2))))) & (((((floor_double__iw_u_parts_lswat3 === floor_double__iw_u_parts_lswat1) & (floor_double__iw_u_parts_mswat3 === floor_double__iw_u_parts_mswat1)) & (floor_double__iw_u_valueat4 === floor_double__iw_u_valueat1)) & (floor_double__xat3 === floor_double__xat2)) & ((bv_slt(32, bv_add(32, __ADDRESS_OF_floor_double__ew_uat, mod_cast(0, IdealInt("4294967295"), 8)), __ADDRESS_OF_floor_double__iw_uat) & (bv_urem(32, __ADDRESS_OF_floor_double__iw_uat, mod_cast(0, IdealInt("4294967295"), 1)) === bv_urem(32, mod_cast(0, IdealInt("4294967295"), 0), mod_cast(0, IdealInt("4294967295"), 1)))) & bv_slt(32, mod_cast(0, IdealInt("4294967295"), 0), bv_add(32, __ADDRESS_OF_floor_double__iw_uat, mod_cast(0, IdealInt("4294967295"), 8))))))) & (main__resat3 === floor_double____retval__at2)) & (isnan_double__xat2 === main__resat3)) & (isnan_double____retval__at2 === ITermITE(!(isnan_double__xat2 === isnan_double__xat2), mod_cast(0, IdealInt("4294967295"), 1), mod_cast(0, IdealInt("4294967295"), 0)))) & (main____CPAchecker_TMP_0at3 === isnan_double____retval__at2)) & (main____CPAchecker_TMP_0at3 === mod_cast(0, IdealInt("4294967295"), 0))))
        val __dummy_variable_dumping_formulas__ = createBooleanVariable("__dummy_variable_dumping_formulas__") // addBooleanVariable(__dummy_variable_dumping_formulas__)
        println("0: " + checkSat(true))
      } // pop scope
    } // withProver
  }
}

Running this will give me the same error message as in the last post.

pruemmer commented 1 month ago

Thanks, that failing test case was very useful! Hopefully the problem is fixed now.

daniel-raffler commented 1 month ago

It's working now. Thanks for all your help!