search

sosy-lab / java-smt

JavaSMT - Unified Java API for SMT solvers.
Apache License 2.0
182 stars 46 forks source link

NoSuchElementException in Princess #232

Closed kfriedberger closed 3 years ago

kfriedberger commented 3 years ago

The newly updated version of Princess in JavaSMT 3.9.0 still has some issues. For example, there is a NoSuchElementException in CPAchecker r37570.

Command line:

scripts/cpa.sh -setprop cpa.predicate.encodeFloatAs=INTEGER -predicateAnalysis -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeBitvectorAs=INTEGER -spec test/programs/benchmarks/properties/unreach-call.prp -32 test/programs/benchmarks/ntdrivers/parport.i.cil-1.c

Stacktrace:

Exception in thread "main" ap.SimpleAPI$SimpleAPIForwardedException: Internal exception: java.util.NoSuchElementException: key not found: sc_66_0_4
    at ap.SimpleAPI.evalProverResult(SimpleAPI.scala:2299)
    at ap.SimpleAPI.getStatusHelp(SimpleAPI.scala:2235)
    at ap.SimpleAPI.getStatusWithDeadline(SimpleAPI.scala:2216)
    at ap.SimpleAPI.checkSatHelp(SimpleAPI.scala:2140)
    at ap.SimpleAPI.checkSat(SimpleAPI.scala:2080)
    at org.sosy_lab.java_smt.solvers.princess.PrincessAbstractProver.isUnsat(PrincessAbstractProver.java:68)
    at org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat.iterateOverAllModels(AbstractProverWithAllSat.java:72)
    at org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat.allSat(AbstractProverWithAllSat.java:54)
    at org.sosy_lab.java_smt.solvers.princess.PrincessAbstractProver.allSat(PrincessAbstractProver.java:212)
    at org.sosy_lab.java_smt.basicimpl.reusableStack.ReusableStackAbstractProver.allSat(ReusableStackAbstractProver.java:112)
    at org.sosy_lab.java_smt.basicimpl.reusableStack.ReusableStackTheoremProver.allSat(ReusableStackTheoremProver.java:13)
    at org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper.allSat(BasicProverWithAssumptionsWrapper.java:113)
    at org.sosy_lab.cpachecker.util.predicates.smt.BasicProverEnvironmentView.allSat(BasicProverEnvironmentView.java:105)
    at org.sosy_lab.cpachecker.cpa.predicate.PredicateAbstractionManager.computeBooleanAbstraction(PredicateAbstractionManager.java:1001)
    at org.sosy_lab.cpachecker.cpa.predicate.PredicateAbstractionManager.computeAbstraction(PredicateAbstractionManager.java:774)
    at org.sosy_lab.cpachecker.cpa.predicate.PredicateAbstractionManager.buildAbstraction(PredicateAbstractionManager.java:391)
    at org.sosy_lab.cpachecker.cpa.predicate.PredicatePrecisionAdjustment.computeAbstraction(PredicatePrecisionAdjustment.java:190)
    at org.sosy_lab.cpachecker.cpa.predicate.PredicatePrecisionAdjustment.prec(PredicatePrecisionAdjustment.java:97)
    at org.sosy_lab.cpachecker.cpa.composite.CompositePrecisionAdjustment.prec(CompositePrecisionAdjustment.java:67)
    at org.sosy_lab.cpachecker.cpa.arg.ARGPrecisionAdjustment.prec(ARGPrecisionAdjustment.java:80)
    at org.sosy_lab.cpachecker.cpa.arg.ARGPrecisionAdjustment.prec(ARGPrecisionAdjustment.java:54)
    at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.handleState(CPAAlgorithm.java:340)
    at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run0(CPAAlgorithm.java:273)
    at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run(CPAAlgorithm.java:245)
    at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.run(CEGARAlgorithm.java:231)
    at org.sosy_lab.cpachecker.core.CPAchecker.runAlgorithm(CPAchecker.java:531)
    at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:398)
    at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:168)
Caused by: java.util.NoSuchElementException: key not found: sc_66_0_4
    at scala.collection.MapOps.default(Map.scala:241)
    at scala.collection.MapOps.default$(Map.scala:240)
    at scala.collection.AbstractMap.default(Map.scala:372)
    at scala.collection.mutable.HashMap.apply(HashMap.scala:425)
    at ap.util.FastImmutableMap.apply(FastImmutableMap.scala:75)
    at ap.terfor.TermOrder.compareTerms(TermOrder.scala:393)
    at ap.terfor.TermOrder.compare(TermOrder.scala:378)
    at ap.terfor.linearcombination.LinearCombination1.$minus(LinearCombination.scala:1569)
    at ap.terfor.RichLinearCombinationSeq.$anonfun$$minus$minus$minus$3(TerForConvenience.scala:307)
    at scala.collection.Iterator$$anon$9.next(Iterator.scala:575)
    at scala.collection.immutable.List.prependedAll(List.scala:153)
    at scala.collection.IterableOnceOps.toList(IterableOnce.scala:1251)
    at scala.collection.IterableOnceOps.toList$(IterableOnce.scala:1251)
    at scala.collection.AbstractIterator.toList(Iterator.scala:1279)
    at ap.terfor.RichLinearCombinationSeq.$minus$minus$minus(TerForConvenience.scala:307)
    at ap.terfor.RichLinearCombinationSeq.$eq$eq$eq(TerForConvenience.scala:323)
    at ap.theories.ExtArray$Reducer.$anonfun$reduceSelects$1(ExtArray.scala:972)
    at ap.terfor.conjunctions.ReducerPlugin$.rewritePreds(ReducerPlugin.scala:101)
    at ap.theories.ExtArray$Reducer.reduceSelects(ExtArray.scala:951)
    at ap.theories.ExtArray$Reducer.$anonfun$reduce$1(ExtArray.scala:905)
    at ap.terfor.conjunctions.ReducerPlugin$UnchangedResult$.orElse(ReducerPlugin.scala:54)
    at ap.theories.ExtArray$Reducer.reduce(ExtArray.scala:905)
    at ap.terfor.conjunctions.SeqReducerPlugin.reduce(ReducerPlugin.scala:383)
    at ap.terfor.conjunctions.ReduceWithConjunction.ap$terfor$conjunctions$ReduceWithConjunction$$reduceWithPlugin(ReduceWithConjunction.scala:633)
    at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reReduceConj(ReduceWithConjunction.scala:343)
    at ap.terfor.conjunctions.ReduceWithConjunction$.$anonfun$reReduceConj$1(ReduceWithConjunction.scala:352)
    at scala.collection.SeqView$Map.apply(SeqView.scala:59)
    at scala.collection.IndexedSeqView$IndexedSeqViewIterator.next(IndexedSeqView.scala:59)
    at scala.collection.IterableOnceOps.copyToArray(IterableOnce.scala:874)
    at scala.collection.IterableOnceOps.copyToArray$(IterableOnce.scala:869)
    at scala.collection.AbstractIterator.copyToArray(Iterator.scala:1279)
    at scala.collection.IterableOnceOps.copyToArray(IterableOnce.scala:835)
    at scala.collection.IterableOnceOps.copyToArray$(IterableOnce.scala:835)
    at scala.collection.AbstractIterator.copyToArray(Iterator.scala:1279)
    at scala.collection.immutable.Vector$.from(Vector.scala:54)
    at scala.collection.immutable.Vector$.from(Vector.scala:34)
    at scala.collection.SeqFactory$Delegate.from(Factory.scala:306)
    at scala.collection.immutable.IndexedSeq$.from(Seq.scala:115)
    at scala.collection.immutable.IndexedSeq$.from(Seq.scala:112)
    at scala.collection.IndexedSeqOps.map(IndexedSeq.scala:86)
    at scala.collection.IndexedSeqOps.map$(IndexedSeq.scala:86)
    at ap.terfor.conjunctions.NegatedConjunctions.map(NegatedConjunctions.scala:84)
    at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reReduceConj(ReduceWithConjunction.scala:347)
    at ap.terfor.conjunctions.ReduceWithConjunction.tentativeReduce(ReduceWithConjunction.scala:453)
    at ap.proof.goal.FormulaTask.updateTask(FormulaTask.scala:95)
    at ap.proof.goal.BetaFormulaTask.updateTask(BetaFormulaTask.scala:407)
    at ap.proof.goal.TaskManager.updateTask$1(TaskManager.scala:200)
    at ap.proof.goal.TaskManager.$anonfun$updateTasks$2(TaskManager.scala:213)
    at ap.basetypes.Node.flatItMapRec(LeftistHeap.scala:519)
    at ap.basetypes.Node.flatItMapRec(LeftistHeap.scala:520)
    at ap.basetypes.LeftistHeap.flatItMap(LeftistHeap.scala:241)
    at ap.proof.goal.TaskManager.updateTasks(TaskManager.scala:213)
    at ap.proof.goal.UpdateTasksTask$.apply(UpdateTasksTask.scala:78)
    at ap.proof.goal.Goal.step(Goal.scala:408)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:482)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:544)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:491)
[... 'findModel' repeats about 50 times ...]
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:491)
    at ap.proof.ModelSearchProver$IncProverImpl.checkValidityDir(ModelSearchProver.scala:1092)
    at ap.SimpleAPI$$anon$4$$anonfun$1.$anonfun$applyOrElse$2(SimpleAPI.scala:4542)
    at ap.util.Timeout$.catchTimeout(Timeout.scala:100)
    at ap.SimpleAPI$$anon$4$$anonfun$1.applyOrElse(SimpleAPI.scala:4543)
    at scala.runtime.AbstractPartialFunction.apply(AbstractPartialFunction.scala:35)
    at ap.SimpleAPI$$anon$4.$anonfun$run$2(SimpleAPI.scala:4598)
    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.SimpleAPI$$anon$4.run(SimpleAPI.scala:4588)
    at java.base/java.lang.Thread.run(Thread.java:829)

There are about 50 other sv-benchmark tasks resulting in the same exception. We should be able to generate a SMTLIB query out of the given command and provide a direct bug report for the Princess developers.

kfriedberger commented 3 years ago

Another similar exception:

Command line:

scripts/cpa.sh -setprop cpa.predicate.encodeFloatAs=INTEGER -predicateAnalysis -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeBitvectorAs=BITVECTOR -spec test/programs/benchmarks/properties/unreach-call.prp -32 test/programs/benchmarks/ldv-regression/test07.c

Stacktrace:

Exception in thread "main" org.sosy_lab.common.Classes$UnexpectedCheckedException: Unexpected checked exception SimpleAPIForwardedException during refinement: Internal exception: java.util.NoSuchElementException: key not found: sc_40_0_0
    at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.callWithTimelimit(InterpolationManager.java:292)
    at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.buildCounterexampleTraceWithoutInterpolation(InterpolationManager.java:370)
    at org.sosy_lab.cpachecker.cpa.predicate.PredicateStaticRefiner.performStaticRefinementForPath(PredicateStaticRefiner.java:214)
    at org.sosy_lab.cpachecker.cpa.predicate.PredicateStaticRefiner.performRefinementForPath(PredicateStaticRefiner.java:179)
    at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinementForPath(AbstractARGBasedRefiner.java:157)
    at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinement(AbstractARGBasedRefiner.java:102)
    at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.refine(CEGARAlgorithm.java:296)
    at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.run(CEGARAlgorithm.java:242)
    at org.sosy_lab.cpachecker.core.CPAchecker.runAlgorithm(CPAchecker.java:531)
    at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:398)
    at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:168)
Caused by: ap.SimpleAPI$SimpleAPIForwardedException: Internal exception: java.util.NoSuchElementException: key not found: sc_40_0_0
    at ap.SimpleAPI.evalProverResult(SimpleAPI.scala:2299)
    at ap.SimpleAPI.getStatusHelp(SimpleAPI.scala:2235)
    at ap.SimpleAPI.getStatusWithDeadline(SimpleAPI.scala:2216)
    at ap.SimpleAPI.checkSatHelp(SimpleAPI.scala:2140)
    at ap.SimpleAPI.checkSat(SimpleAPI.scala:2080)
    at org.sosy_lab.java_smt.solvers.princess.PrincessAbstractProver.isUnsat(PrincessAbstractProver.java:68)
    at org.sosy_lab.java_smt.basicimpl.reusableStack.ReusableStackAbstractProver.isUnsat(ReusableStackAbstractProver.java:45)
    at org.sosy_lab.java_smt.basicimpl.reusableStack.ReusableStackTheoremProver.isUnsat(ReusableStackTheoremProver.java:13)
    at org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper.isUnsat(BasicProverWithAssumptionsWrapper.java:59)
    at org.sosy_lab.cpachecker.util.predicates.smt.BasicProverEnvironmentView.isUnsat(BasicProverEnvironmentView.java:56)
    at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.solveCounterexample(InterpolationManager.java:454)
    at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.buildCounterexampleTraceWithoutInterpolation0(InterpolationManager.java:383)
    at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.lambda$buildCounterexampleTraceWithoutInterpolation$1(InterpolationManager.java:371)
    at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.callWithTimelimit(InterpolationManager.java:289)
    ... 10 more
Caused by: java.util.NoSuchElementException: key not found: sc_40_0_0
    at scala.collection.MapOps.default(Map.scala:241)
    at scala.collection.MapOps.default$(Map.scala:240)
    at scala.collection.AbstractMap.default(Map.scala:372)
    at scala.collection.mutable.HashMap.apply(HashMap.scala:425)
    at ap.util.FastImmutableMap.apply(FastImmutableMap.scala:75)
    at ap.terfor.TermOrder.compareTerms(TermOrder.scala:393)
    at ap.terfor.TermOrder.compare(TermOrder.scala:378)
    at ap.terfor.linearcombination.LinearCombination1.$minus(LinearCombination.scala:1569)
    at ap.terfor.RichLinearCombinationSeq.$anonfun$$minus$minus$minus$3(TerForConvenience.scala:307)
    at scala.collection.Iterator$$anon$9.next(Iterator.scala:575)
    at scala.collection.immutable.List.prependedAll(List.scala:153)
    at scala.collection.IterableOnceOps.toList(IterableOnce.scala:1251)
    at scala.collection.IterableOnceOps.toList$(IterableOnce.scala:1251)
    at scala.collection.AbstractIterator.toList(Iterator.scala:1279)
    at ap.terfor.RichLinearCombinationSeq.$minus$minus$minus(TerForConvenience.scala:307)
    at ap.terfor.RichLinearCombinationSeq.$eq$eq$eq(TerForConvenience.scala:323)
    at ap.theories.ExtArray$Reducer.$anonfun$reduceSelects$1(ExtArray.scala:972)
    at ap.terfor.conjunctions.ReducerPlugin$.rewritePreds(ReducerPlugin.scala:117)
    at ap.theories.ExtArray$Reducer.reduceSelects(ExtArray.scala:951)
    at ap.theories.ExtArray$Reducer.$anonfun$reduce$1(ExtArray.scala:905)
    at ap.terfor.conjunctions.ReducerPlugin$UnchangedResult$.orElse(ReducerPlugin.scala:54)
    at ap.theories.ExtArray$Reducer.reduce(ExtArray.scala:905)
    at ap.terfor.conjunctions.SeqReducerPlugin.reduce(ReducerPlugin.scala:383)
    at ap.terfor.conjunctions.ReduceWithConjunction.ap$terfor$conjunctions$ReduceWithConjunction$$reduceWithPlugin(ReduceWithConjunction.scala:633)
    at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:105)
    at ap.terfor.conjunctions.ReduceWithConjunction.apply(ReduceWithConjunction.scala:432)
    at ap.terfor.conjunctions.ReduceWithConjunction.apply(ReduceWithConjunction.scala:425)
    at ap.terfor.conjunctions.ReduceWithConjunction.tentativeReduce(ReduceWithConjunction.scala:459)
    at ap.proof.goal.FormulaTask.updateTask(FormulaTask.scala:95)
    at ap.proof.goal.BetaFormulaTask.updateTask(BetaFormulaTask.scala:407)
    at ap.proof.goal.TaskManager.updateTask$1(TaskManager.scala:200)
    at ap.proof.goal.TaskManager.$anonfun$updateTasks$2(TaskManager.scala:213)
    at ap.basetypes.Node.flatItMapRec(LeftistHeap.scala:519)
    at ap.basetypes.Node.flatItMapRec(LeftistHeap.scala:520)
    at ap.basetypes.LeftistHeap.flatItMap(LeftistHeap.scala:241)
    at ap.proof.goal.TaskManager.updateTasks(TaskManager.scala:213)
    at ap.proof.goal.UpdateTasksTask$.apply(UpdateTasksTask.scala:78)
    at ap.proof.goal.Goal.step(Goal.scala:408)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:482)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:544)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:491)
[... 'findModel' repeats about 20 times ...]
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:491)
    at ap.proof.ModelSearchProver$IncProverImpl.checkValidityDir(ModelSearchProver.scala:1092)
    at ap.SimpleAPI$$anon$4$$anonfun$1.$anonfun$applyOrElse$2(SimpleAPI.scala:4542)
    at ap.util.Timeout$.catchTimeout(Timeout.scala:100)
    at ap.SimpleAPI$$anon$4$$anonfun$1.applyOrElse(SimpleAPI.scala:4543)
    at scala.runtime.AbstractPartialFunction.apply(AbstractPartialFunction.scala:35)
    at ap.SimpleAPI$$anon$4.$anonfun$run$2(SimpleAPI.scala:4598)
    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.SimpleAPI$$anon$4.run(SimpleAPI.scala:4588)
    at java.base/java.lang.Thread.run(Thread.java:829)
kfriedberger commented 3 years ago

The SMTLIB query for the second given command line does not directly crash Princess, but returns an invalid result SAT. I have not checked manually, but at least MathSAT5 and Z3 return UNSAT on the following query:

(declare-fun __ART__11 () Bool)
(declare-fun __ART__4 () Bool)
(declare-fun a@2 () (_ BitVec 32))
(declare-fun b@2 () (_ BitVec 32))
(declare-fun p1@2 () (_ BitVec 32))
(declare-fun p2@2 () (_ BitVec 32))
(declare-fun p1@3 () (_ BitVec 32))
(declare-fun p2@3 () (_ BitVec 32))
(declare-fun p1@4 () (_ BitVec 32))
(declare-fun |f::v@2| () (_ BitVec 32))
(declare-fun |f::__retval__@2| () (_ BitVec 32))
(declare-fun |main::__retval__@2| () (_ BitVec 32))
(declare-fun __ADDRESS_OF_a@ () (_ BitVec 32))
(declare-fun __ADDRESS_OF_b@ () (_ BitVec 32))
(declare-fun *int@1 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun *int@2 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun *int@3 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun *int@4 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun *int@5 () (Array (_ BitVec 32) (_ BitVec 32)))
(define-fun abbrev_9 () Bool (and (and (and (and (and (and (and (and (and (and (= a@2 (_ bv0 32)) (and (and (bvslt (_ bv0 32) __ADDRESS_OF_a@) (= (bvurem __ADDRESS_OF_a@ (_ bv4 32)) (bvurem (_ bv0 32) (_ bv4 32)))) (bvslt (_ bv0 32) (bvadd __ADDRESS_OF_a@ (_ bv4 32))))) (and (= b@2 (_ bv0 32)) (and (and (bvslt (bvadd __ADDRESS_OF_a@ (_ bv4 32)) __ADDRESS_OF_b@) (= (bvurem __ADDRESS_OF_b@ (_ bv4 32)) (bvurem (_ bv0 32) (_ bv4 32)))) (bvslt (_ bv0 32) (bvadd __ADDRESS_OF_b@ (_ bv4 32)))))) (= p1@2 (_ bv0 32))) (= p2@2 (_ bv0 32))) (and (= p1@3 __ADDRESS_OF_a@) (= (select *int@1 __ADDRESS_OF_a@) a@2))) (and (= p2@3 __ADDRESS_OF_b@) (= (select *int@1 __ADDRESS_OF_b@) b@2))) (= *int@2 (store *int@1 __ADDRESS_OF_b@ (_ bv1 32)))) (= *int@3 (store *int@2 __ADDRESS_OF_a@ (_ bv5 32)))) (= *int@4 (store *int@3 __ADDRESS_OF_a@ (bvsub (select *int@3 __ADDRESS_OF_a@) (_ bv1 32))))) (= |f::v@2| (bvsub (bvadd (select *int@4 p1@3) (select *int@4 p2@3)) (select *int@4 __ADDRESS_OF_a@)))))
(assert (or (and (and (and (or (and (and (and abbrev_9 (= |f::v@2| (_ bv1 32))) (= p1@4 p2@3)) (= |f::__retval__@2| |f::v@2|)) (and (and (and abbrev_9 (not (= |f::v@2| (_ bv1 32)))) (= |f::__retval__@2| (_ bv0 32))) (= p1@4 p1@3))) (= *int@5 (store *int@4 __ADDRESS_OF_a@ |f::__retval__@2|))) (not (= (select *int@5 __ADDRESS_OF_a@) (_ bv0 32)))) (not (= p1@4 p2@3))) (and (and (or (and (and (and abbrev_9 (= |f::v@2| (_ bv1 32))) (= p1@4 p2@3)) (= |f::__retval__@2| |f::v@2|)) (and (and (and abbrev_9 (not (= |f::v@2| (_ bv1 32)))) (= |f::__retval__@2| (_ bv0 32))) (= p1@4 p1@3))) (= *int@5 (store *int@4 __ADDRESS_OF_a@ |f::__retval__@2|))) (= (select *int@5 __ADDRESS_OF_a@) (_ bv0 32)))))

Princess 2021-05-10 returns a model here:

{
  *int@4 -> const(0), 
  f::__retval__@2 -> mod_cast(0, 4294967295, 0), 
  *int@5 -> store(const(0), mod_cast(0, 4294967295, 4294967295), mod_cast(0, 4294967295, 0)), 
  f::v@2 -> mod_cast(0, 4294967295, 0), 
  __ADDRESS_OF_a@ -> mod_cast(0, 4294967295, 4294967295), 
  p1@3 -> mod_cast(0, 4294967295, 4294967295), 
  p2@3 -> mod_cast(0, 4294967295, 4294967295), 
  p1@4 -> mod_cast(0, 4294967295, 4294967295), 
  store(const(0), mod_cast(0, 4294967295, 4294967295), mod_cast(0, 4294967295, 0)) -> store(const(0), mod_cast(0, 4294967295, 4294967295), mod_cast(0, 4294967295, 0)), 
  abbrev_5 -> true
}
kfriedberger commented 3 years ago

Update for the last issue from above: It seems as if Princess did not yet provide abbreviations in the parser result, which causes an unknown/new boolean symbol in the parsed query for JavaSMT. Thus, the query was trivially satisfiable. We requested two changes in the API of Princess, and got both fixed:

The new version of princess is available as 2021-06-28.

I will now continue to debug the NoSuchElementException from the sat-check.

kfriedberger commented 3 years ago

With Princess 2021-06-28, I can trigger an exception via the following Java code (given as JUnit test). The exception is thrown non-deterministically in about 50% of all cases. The non-determinism could be caused by the non-deterministic ordering of constants/symbols from the parser result.

private final String PRINCESS_CRASH_QUERY =
      "(declare-fun a@2 () (_ BitVec 32))\n"
          + "(declare-fun b@2 () (_ BitVec 32))\n"
          + "(declare-fun p1@2 () (_ BitVec 32))\n"
          + "(declare-fun p2@2 () (_ BitVec 32))\n"
          + "(declare-fun p1@3 () (_ BitVec 32))\n"
          + "(declare-fun p2@3 () (_ BitVec 32))\n"
          + "(declare-fun p1@4 () (_ BitVec 32))\n"
          + "(declare-fun |f::v@2| () (_ BitVec 32))\n"
          + "(declare-fun |f::__retval__@2| () (_ BitVec 32))\n"
          + "(declare-fun __ADDRESS_OF_a@ () (_ BitVec 32))\n"
          + "(declare-fun __ADDRESS_OF_b@ () (_ BitVec 32))\n"
          + "(declare-fun *int@1 () (Array (_ BitVec 32) (_ BitVec 32)))\n"
          + "(declare-fun *int@2 () (Array (_ BitVec 32) (_ BitVec 32)))\n"
          + "(declare-fun *int@3 () (Array (_ BitVec 32) (_ BitVec 32)))\n"
          + "(declare-fun *int@4 () (Array (_ BitVec 32) (_ BitVec 32)))\n"
          + "(declare-fun *int@5 () (Array (_ BitVec 32) (_ BitVec 32)))\n"
          + "(define-fun abbrev_9 () Bool (and (and (and (and (and (and (and (and (and (and (="
          + " a@2 (_ bv0 32)) (and (and (bvslt (_ bv0 32) __ADDRESS_OF_a@) (= (bvurem"
          + " __ADDRESS_OF_a@ (_ bv4 32)) (bvurem (_ bv0 32) (_ bv4 32)))) (bvslt (_ bv0 32)"
          + " (bvadd __ADDRESS_OF_a@ (_ bv4 32))))) (and (= b@2 (_ bv0 32)) (and (and (bvslt"
          + " (bvadd __ADDRESS_OF_a@ (_ bv4 32)) __ADDRESS_OF_b@) (= (bvurem __ADDRESS_OF_b@ (_"
          + " bv4 32)) (bvurem (_ bv0 32) (_ bv4 32)))) (bvslt (_ bv0 32) (bvadd __ADDRESS_OF_b@"
          + " (_ bv4 32)))))) (= p1@2 (_ bv0 32))) (= p2@2 (_ bv0 32))) (and (= p1@3"
          + " __ADDRESS_OF_a@) (= (select *int@1 __ADDRESS_OF_a@) a@2))) (and (= p2@3"
          + " __ADDRESS_OF_b@) (= (select *int@1 __ADDRESS_OF_b@) b@2))) (= *int@2 (store *int@1"
          + " __ADDRESS_OF_b@ (_ bv1 32)))) (= *int@3 (store *int@2 __ADDRESS_OF_a@ (_ bv5 32))))"
          + " (= *int@4 (store *int@3 __ADDRESS_OF_a@ (bvsub (select *int@3 __ADDRESS_OF_a@) (_"
          + " bv1 32))))) (= |f::v@2| (bvsub (bvadd (select *int@4 p1@3) (select *int@4 p2@3))"
          + " (select *int@4 __ADDRESS_OF_a@)))))\n"
          + "(assert (or (and (and (and (or (and (and (and abbrev_9 (= |f::v@2| (_ bv1 32))) (="
          + " p1@4 p2@3)) (= |f::__retval__@2| |f::v@2|)) (and (and (and abbrev_9 (not (="
          + " |f::v@2| (_ bv1 32)))) (= |f::__retval__@2| (_ bv0 32))) (= p1@4 p1@3))) (= *int@5"
          + " (store *int@4 __ADDRESS_OF_a@ |f::__retval__@2|))) (not (= (select *int@5"
          + " __ADDRESS_OF_a@) (_ bv0 32)))) (not (= p1@4 p2@3))) (and (and (or (and (and (and"
          + " abbrev_9 (= |f::v@2| (_ bv1 32))) (= p1@4 p2@3)) (= |f::__retval__@2| |f::v@2|))"
          + " (and (and (and abbrev_9 (not (= |f::v@2| (_ bv1 32)))) (= |f::__retval__@2| (_ bv0"
          + " 32))) (= p1@4 p1@3))) (= *int@5 (store *int@4 __ADDRESS_OF_a@ |f::__retval__@2|)))"
          + " (= (select *int@5 __ADDRESS_OF_a@) (_ bv0 32)))))";

  @Test
  public void crashPrincessDirectly() {
    Debug.enableAllAssertions(true);

    // create formula in one API
    final SimpleAPI api = SimpleAPI.spawn();
    Tuple4<
            Seq<IFormula>,
            Map<IFunction, SMTFunctionType>,
            Map<ConstantTerm, SMTType>,
            Map<Predicate, SMTFunctionType>>
        parserResult =
            api.extractSMTLIBAssertionsSymbols(new StringReader(PRINCESS_CRASH_QUERY), true);
    IFormula assertion = asJava(parserResult._1()).get(0);

    // add symbols to a second API
    final SimpleAPI api2 = SimpleAPI.spawn();
    for (Entry<ConstantTerm, SMTType> entry : asJava(parserResult._3()).entrySet()) { // non-deterministic ordering?
      api2.addConstantRaw(entry.getKey());
    }

    // and solver the original query in the second API
    api2.push();
    api2.addAssertion(assertion);
    Value satResult = api2.checkSat(true); // <-- crash happens here
    assert_().that(satResult).isEqualTo(SimpleAPI.ProverStatus$.MODULE$.Unsat());
  }

The corresponding stacktrace:

Click here for details 
ap.SimpleAPI$SimpleAPIForwardedException: Internal exception: java.util.NoSuchElementException: key not found: sc_33_0_0
    at ap.SimpleAPI.evalProverResult(SimpleAPI.scala:2312)
    at ap.SimpleAPI.getStatusHelp(SimpleAPI.scala:2248)
    at ap.SimpleAPI.getStatusWithDeadline(SimpleAPI.scala:2229)
    at ap.SimpleAPI.checkSatHelp(SimpleAPI.scala:2153)
    at ap.SimpleAPI.checkSat(SimpleAPI.scala:2093)
    at [... my JUnit test ...]
Caused by: java.util.NoSuchElementException: key not found: sc_33_0_0
    at scala.collection.MapOps.default(Map.scala:241)
    at scala.collection.MapOps.default$(Map.scala:240)
    at scala.collection.AbstractMap.default(Map.scala:372)
    at scala.collection.mutable.HashMap.apply(HashMap.scala:425)
    at ap.util.FastImmutableMap.apply(FastImmutableMap.scala:75)
    at ap.terfor.TermOrder.compareTerms(TermOrder.scala:393)
    at ap.terfor.TermOrder.compare(TermOrder.scala:378)
    at ap.terfor.linearcombination.LinearCombination1.$minus(LinearCombination.scala:1587)
    at ap.terfor.RichLinearCombinationSeq.$anonfun$$minus$minus$minus$3(TerForConvenience.scala:307)
    at scala.collection.Iterator$$anon$9.next(Iterator.scala:575)
    at scala.collection.immutable.List.prependedAll(List.scala:153)
    at scala.collection.IterableOnceOps.toList(IterableOnce.scala:1251)
    at scala.collection.IterableOnceOps.toList$(IterableOnce.scala:1251)
    at scala.collection.AbstractIterator.toList(Iterator.scala:1279)
    at ap.terfor.RichLinearCombinationSeq.$minus$minus$minus(TerForConvenience.scala:307)
    at ap.terfor.RichLinearCombinationSeq.$eq$eq$eq(TerForConvenience.scala:323)
    at ap.theories.ExtArray$Reducer.$anonfun$reduceSelects$1(ExtArray.scala:972)
    at ap.terfor.conjunctions.ReducerPlugin$.rewritePreds(ReducerPlugin.scala:117)
    at ap.theories.ExtArray$Reducer.reduceSelects(ExtArray.scala:951)
    at ap.theories.ExtArray$Reducer.$anonfun$reduce$1(ExtArray.scala:905)
    at ap.terfor.conjunctions.ReducerPlugin$UnchangedResult$.orElse(ReducerPlugin.scala:54)
    at ap.theories.ExtArray$Reducer.reduce(ExtArray.scala:905)
    at ap.terfor.conjunctions.SeqReducerPlugin.reduce(ReducerPlugin.scala:383)
    at ap.terfor.conjunctions.ReduceWithConjunction.ap$terfor$conjunctions$ReduceWithConjunction$$reduceWithPlugin(ReduceWithConjunction.scala:707)
    at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:105)
    at ap.terfor.conjunctions.ReduceWithConjunction.apply(ReduceWithConjunction.scala:506)
    at ap.terfor.conjunctions.ReduceWithConjunction.apply(ReduceWithConjunction.scala:499)
    at ap.terfor.conjunctions.ReduceWithConjunction.tentativeReduce(ReduceWithConjunction.scala:533)
    at ap.proof.goal.FormulaTask.updateTask(FormulaTask.scala:95)
    at ap.proof.goal.BetaFormulaTask.updateTask(BetaFormulaTask.scala:407)
    at ap.proof.goal.TaskManager.updateTask$1(TaskManager.scala:200)
    at ap.proof.goal.TaskManager.$anonfun$updateTasks$2(TaskManager.scala:213)
    at ap.basetypes.Node.flatItMapRec(LeftistHeap.scala:519)
    at ap.basetypes.Node.flatItMapRec(LeftistHeap.scala:521)
    at ap.basetypes.Node.flatItMapRec(LeftistHeap.scala:520)
    at ap.basetypes.LeftistHeap.flatItMap(LeftistHeap.scala:241)
    at ap.proof.goal.TaskManager.updateTasks(TaskManager.scala:213)
    at ap.proof.goal.UpdateTasksTask$.apply(UpdateTasksTask.scala:78)
    at ap.proof.goal.Goal.step(Goal.scala:408)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:482)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:544)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:491)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:602)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:491)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:491)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:544)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:491)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:544)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:491)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:544)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:491)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:544)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:491)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:544)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:491)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:544)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:491)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:544)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:491)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:544)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:491)
    at ap.proof.ModelSearchProver$IncProverImpl.checkValidityDir(ModelSearchProver.scala:1092)
    at ap.SimpleAPI$$anon$4$$anonfun$1.$anonfun$applyOrElse$2(SimpleAPI.scala:4608)
    at ap.util.Timeout$.catchTimeout(Timeout.scala:100)
    at ap.SimpleAPI$$anon$4$$anonfun$1.applyOrElse(SimpleAPI.scala:4609)
    at scala.runtime.AbstractPartialFunction.apply(AbstractPartialFunction.scala:35)
    at ap.SimpleAPI$$anon$4.$anonfun$run$2(SimpleAPI.scala:4664)
    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.SimpleAPI$$anon$4.run(SimpleAPI.scala:4654)
    at java.base/java.lang.Thread.run(Thread.java:829)
kfriedberger commented 3 years ago

Current status: most bugs already fixed in Princess, new release of Princess requested.

kfriedberger commented 3 years ago

Current status: several bugs are fixed, Princess still fails with NoSuchElementException on one quite large SMT query from a JUnit test. The failing test is listed as first entry in this list of Junit tests.

baierd commented 3 years ago

The exception does not happen in the initial isUnsat() call but in a second one that checks if the model assignments, interpreted as formulas, are satisfiable. And here lies the problem, the model has several additional variables which are not added to the solver (SimpleAPI of Princess) automatically. As they are all named abbrev_x or abbrev_x_def with x being a number, i guess those are abbreviations? At the very least they are auxiliary variables not needed.

The exception itself signals that a variable is used in a formula that is unknown. (I don't know why it is not throwing the exact variable in this case, but if you check the conjunction with the original formula it throws the name of the failed variable)

I've tested removing only the abbrev variables from the model/checked model formulas and the tests works after that. Further, i've send a mail to Philipp Rümmer and asked him about these variables. I'll update here once i got a reply.

The abbrev variables are only Boolean by the way. So i guess removing all of them from the model would be the go to way?

kfriedberger commented 3 years ago

The problem with exporting abbreviations should be fixed with e537e7f416c1daf18852631ec410d21d9029b966.