Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Open
kfriedberger opened this issue Jun 4, 2023 · 2 comments
Open

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

kfriedberger opened this issue Jun 4, 2023 · 2 comments
Labels
bug CVC4

Comments

@kfriedberger
Copy link
Member

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
Copy link
Member Author

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
Copy link
Member Author

kfriedberger commented Jun 8, 2023 •
edited

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug CVC4
Milestone
No milestone
Development

No branches or pull requests
1 participant
@kfriedberger