search

sosy-lab / java-smt

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

CVC4: model evaluation crashes on constant value (found in CPAchecker benchmark) #309

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=CVC4 -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/prodbin-ll.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/prodbin-ll.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 CVC4 1.8-prerelease. (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" Illegal argument detected
const T& CVC4::Expr::getConst() const [with T = bool]

  `*this' is a bad argument; expected getKind() == ::CVC4::kind::CONST_BOOLEAN to hold
Improper kind for getConst<bool>()
    at edu.stanford.CVC4.CVC4JNI.Expr_getConstBoolean(Native Method)
    at edu.stanford.CVC4.Expr.getConstBoolean(Expr.java:355)
    at org.sosy_lab.java_smt.solvers.cvc4.CVC4FormulaCreator.convertValue(CVC4FormulaCreator.java:572)
    at org.sosy_lab.java_smt.solvers.cvc4.CVC4FormulaCreator.convertValue(CVC4FormulaCreator.java:65)
    at org.sosy_lab.java_smt.basicimpl.AbstractEvaluator.evaluateImpl(AbstractEvaluator.java:120)
    at org.sosy_lab.java_smt.basicimpl.AbstractEvaluator.evaluate(AbstractEvaluator.java:101)
    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)
kfriedberger commented 1 year ago

Same here:

scripts/cpa.sh -heap 13000M -noout -benchmark -stack 50M -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop counterexample.export.allowImpreciseCounterexamples=true -setprop cpa.predicate.encodeFloatAs=INTEGER -kInduction -setprop solver.solver=CVC4 -setprop cpa.predicate.encodeBitvectorAs=INTEGER -timelimit 60s -stats -spec ../sv-benchmarks/c/properties/unreach-call.prp -32 ../sv-benchmarks/c/nla-digbench-scaling/prodbin-ll_valuebound2.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 / kInduction (OpenJDK 64-Bit Server VM 17.0.7) started (CPAchecker.run, INFO)

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

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

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

Using predicate analysis with CVC4 1.8-prerelease. (Parallel analysis 1:PredicateCPA:PredicateCPA.<init>, INFO)

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

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

Using predicate analysis with CVC4 1.8-prerelease. (Parallel analysis 1:InductionStepCase:PredicateCPA:PredicateCPA.<init>, INFO)

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

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

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

Creating formula for program (Parallel analysis 1:AbstractBMCAlgorithm.run, INFO)

Starting satisfiability check... (Parallel analysis 1:AbstractBMCAlgorithm.boundedModelCheck, INFO)

Starting assertions check... (Parallel analysis 1:AbstractBMCAlgorithm.checkBoundingAssertions, INFO)

Running algorithm to create induction hypothesis (Parallel analysis 1:KInductionProver.check, INFO)

Adjusting interestingVariableLimit to 1 (Parallel analysis 2:InvariantsCPA:InvariantsCPA$InterestingVariableLimitAdjuster.adjustConditions, INFO)

Adjusting precision for CPA org.sosy_lab.cpachecker.cpa.invariants.InvariantsCPA@51819640 (Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis, INFO)

Updating reached set provided to other analyses (Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis, INFO)

Starting induction check... (Parallel analysis 1:KInductionProver.check, INFO)

Adjusting interestingVariableLimit to 2 (Parallel analysis 2:InvariantsCPA:InvariantsCPA$InterestingVariableLimitAdjuster.adjustConditions, INFO)

Adjusting precision for CPA org.sosy_lab.cpachecker.cpa.invariants.InvariantsCPA@51819640 (Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis, INFO)

Updating reached set provided to other analyses (Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis, INFO)

Adjusting maxLoopIterations to 2 (Parallel analysis 1:LoopBoundCPA:LoopBoundPrecisionAdjustment.nextState, INFO)

Creating formula for program (Parallel analysis 1:AbstractBMCAlgorithm.run, INFO)

Adjusting interestingVariableLimit to 3 (Parallel analysis 2:InvariantsCPA:InvariantsCPA$InterestingVariableLimitAdjuster.adjustConditions, INFO)

Adjusting precision for CPA org.sosy_lab.cpachecker.cpa.invariants.InvariantsCPA@51819640 (Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis, INFO)

Updating reached set provided to other analyses (Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis, INFO)

Starting satisfiability check... (Parallel analysis 1:AbstractBMCAlgorithm.boundedModelCheck, INFO)

Error found, creating error path (Parallel analysis 1:AbstractBMCAlgorithm.analyzeCounterexample0, INFO)

Analysis was terminated (Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis, INFO)

Exception in thread "main" Illegal argument detected
const T& CVC4::Expr::getConst() const [with T = bool]

  `*this' is a bad argument; expected getKind() == ::CVC4::kind::CONST_BOOLEAN to hold
Improper kind for getConst<bool>()
    at edu.stanford.CVC4.CVC4JNI.Expr_getConstBoolean(Native Method)
    at edu.stanford.CVC4.Expr.getConstBoolean(Expr.java:355)
    at org.sosy_lab.java_smt.solvers.cvc4.CVC4FormulaCreator.convertValue(CVC4FormulaCreator.java:572)
    at org.sosy_lab.java_smt.solvers.cvc4.CVC4FormulaCreator.convertValue(CVC4FormulaCreator.java:65)
    at org.sosy_lab.java_smt.basicimpl.AbstractEvaluator.evaluateImpl(AbstractEvaluator.java:120)
    at org.sosy_lab.java_smt.basicimpl.AbstractEvaluator.evaluate(AbstractEvaluator.java:101)
    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.algorithm.ParallelAlgorithm.runParallelAnalysis(ParallelAlgorithm.java:397)
    at org.sosy_lab.cpachecker.core.algorithm.ParallelAlgorithm.lambda$createParallelAnalysis$3(ParallelAlgorithm.java:342)
    at com.google.common.util.concurrent.TrustedListenableFutureTask$TrustedFutureInterruptibleTask.runInterruptibly(TrustedListenableFutureTask.java:131)
    at com.google.common.util.concurrent.InterruptibleTask.run(InterruptibleTask.java:75)
    at com.google.common.util.concurrent.TrustedListenableFutureTask.run(TrustedListenableFutureTask.java:82)
    at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1136)
    at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635)
    at java.base/java.lang.Thread.run(Thread.java:833)
kfriedberger commented 1 year ago

In those cases, CVC4 does not return a plain boolean, but a rest of a formula, including temporary variables like BOUND_VARIABLE_1218 (without quantifier). Thus, we can not convert it to a plain boolean constant. Solution is unclear.