search

sosy-lab / java-smt

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

Princess: match error in model evaluation (found in CPAchecker benchmark) #308

Open kfriedberger opened 1 year ago

kfriedberger commented 1 year ago

LOG:

scripts/cpa.sh -heap 13000M -noout -benchmark -stack 50M -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop counterexample.export.allowImpreciseCounterexamples=true -setprop cpa.predicate.encodeFloatAs=INTEGER -bmc -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeBitvectorAs=INTEGER -setprop cpa.loopbound.maxLoopIterations=10 -timelimit 60s -stats -spec ../sv-benchmarks/c/properties/unreach-call.prp -32 ../sv-benchmarks/c/nla-digbench-scaling/freire1_valuebound1.c

--------------------------------------------------------------------------------

Running CPAchecker with Java heap of size 13000M.
Running CPAchecker with Java stack of size 50M.
Language C detected and set for analysis (CPAMain.detectFrontendLanguageIfNecessary, INFO)

Using the following resource limits: CPU-time limit of 60s (ResourceLimitChecker.fromConfiguration, INFO)

CPAchecker 2.2.1-svn-43814M / bmc (OpenJDK 64-Bit Server VM 17.0.7) started (CPAchecker.run, INFO)

Parsing CFA from file(s) "../sv-benchmarks/c/nla-digbench-scaling/freire1_valuebound1.c" (CPAchecker.parse, INFO)

Using unsound approximation of ints with unbounded integers and floats with unbounded integers for encoding program semantics. (PredicateCPA:FormulaManagerView.<init>, WARNING)

Using predicate analysis with Princess 2022-11-03. (PredicateCPA:PredicateCPA.<init>, INFO)

Using unsound approximation of ints with unbounded integers and floats with unbounded integers for encoding program semantics. (AssumptionStorageCPA:FormulaManagerView.<init>, WARNING)

Starting analysis ... (CPAchecker.runAlgorithm, INFO)

Creating formula for program (AbstractBMCAlgorithm.run, INFO)

Starting satisfiability check... (AbstractBMCAlgorithm.boundedModelCheck, INFO)

Error found, creating error path (AbstractBMCAlgorithm.analyzeCounterexample0, INFO)

Exception in thread "main" scala.MatchError: _0 (of class ap.parser.ISortedVariable)
    at ap.api.PartialModel$Evaluator$.postVisit(PartialModel.scala:134)
    at ap.api.PartialModel$Evaluator$.postVisit(PartialModel.scala:114)
    at ap.parser.CollectingVisitor.visit(InputAbsyVisitor.scala:169)
    at ap.api.PartialModel$Evaluator$.apply(PartialModel.scala:116)
    at ap.api.PartialModel.evalExpression(PartialModel.scala:59)
    at org.sosy_lab.java_smt.solvers.princess.PrincessModel.evaluate(PrincessModel.java:251)
    at org.sosy_lab.java_smt.solvers.princess.PrincessModel.evalImpl(PrincessModel.java:237)
    at org.sosy_lab.java_smt.solvers.princess.PrincessModel.evalImpl(PrincessModel.java:42)
    at org.sosy_lab.java_smt.basicimpl.AbstractEvaluator.evaluateImpl(AbstractEvaluator.java:119)
    at org.sosy_lab.java_smt.basicimpl.AbstractEvaluator.evaluate(AbstractEvaluator.java:101)
    at org.sosy_lab.java_smt.basicimpl.CachingModel.evaluate(CachingModel.java:55)
    at org.sosy_lab.cpachecker.util.predicates.smt.ModelView.evaluateImpl(ModelView.java:48)
    at org.sosy_lab.cpachecker.util.predicates.smt.ModelView.evaluate(ModelView.java:72)
    at org.sosy_lab.cpachecker.util.predicates.pathformula.PathFormulaManagerImpl.lambda$getARGPathFromModel$0(PathFormulaManagerImpl.java:469)
    at org.sosy_lab.cpachecker.cpa.arg.ARGUtils.getPathFromBranchingInformation(ARGUtils.java:504)
    at org.sosy_lab.cpachecker.util.predicates.pathformula.PathFormulaManagerImpl.getARGPathFromModel(PathFormulaManagerImpl.java:446)
    at org.sosy_lab.cpachecker.util.predicates.pathformula.PathFormulaManager.getARGPathFromModel(PathFormulaManager.java:143)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.analyzeCounterexample0(AbstractBMCAlgorithm.java:878)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.BMCAlgorithm.analyzeCounterexample(BMCAlgorithm.java:168)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.boundedModelCheck(AbstractBMCAlgorithm.java:720)
    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:507)
    at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:369)
    at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:169)
daniel-raffler commented 1 month ago

I've seen this issue somewhat frequently and now reported it here