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

Princess: unhandled model value (found in CPAchecker benchmark) #305

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

Princess: unhandled model value (found in CPAchecker benchmark) #305

kfriedberger opened this issue Jun 4, 2023 · 0 comments
Labels
bug Princess

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 -kInduction -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeBitvectorAs=INTEGER -timelimit 60s -stats -spec ../sv-benchmarks/c/properties/unreach-call.prp -32 ../sv-benchmarks/c/loop-acceleration/array_2-1.i


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


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/loop-acceleration/array_2-1.i" (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 Princess 2022-11-03. (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 Princess 2022-11-03. (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)

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

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

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

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

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

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

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

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

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

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

Adjusting precision for CPA org.sosy_lab.cpachecker.cpa.invariants.InvariantsCPA@5917a039 (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)

Adjusting maximum formula depth to 3 (Parallel analysis 2:InvariantsCPA:InvariantsCPA$FormulaDepthAdjuster.adjustConditions, INFO)

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

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

Adjusting abstraction strategy to NEVER (Parallel analysis 2:InvariantsCPA:InvariantsCPA$AbstractionStrategyAdjuster.adjustConditions, INFO)

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

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

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

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

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

Adjusting maxLoopIterations to 2 (Parallel analysis 1:LoopBoundCPA:LoopBoundPrecisionAdjustment.nextState, 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)

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

Adjusting maxLoopIterations to 3 (Parallel analysis 1:LoopBoundCPA:LoopBoundPrecisionAdjustment.nextState, 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)

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

Adjusting maxLoopIterations to 4 (Parallel analysis 1:LoopBoundCPA:LoopBoundPrecisionAdjustment.nextState, 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)

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

Adjusting maxLoopIterations to 5 (Parallel analysis 1:LoopBoundCPA:LoopBoundPrecisionAdjustment.nextState, 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)

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

Adjusting maxLoopIterations to 6 (Parallel analysis 1:LoopBoundCPA:LoopBoundPrecisionAdjustment.nextState, 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)

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

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

Exception in thread "main" java.lang.IllegalArgumentException: unhandled model value store(store(store(store(store(store(store(store(store(const(12291), 8191, 12289), 8195, 12289), 12263, 8190), 12267, 8190), 12271, 8190), 12275, 8189), 12279, 8189), 12283, 8189), 12287, 8189) of type class ap.parser.IFunApp
	at org.sosy_lab.java_smt.solvers.princess.PrincessFormulaCreator.convertValue(PrincessFormulaCreator.java:147)
	at org.sosy_lab.java_smt.solvers.princess.PrincessFormulaCreator.convertValue(PrincessFormulaCreator.java:72)
	at org.sosy_lab.java_smt.solvers.princess.PrincessModel.getAssignments(PrincessModel.java:167)
	at org.sosy_lab.java_smt.solvers.princess.PrincessModel.asList(PrincessModel.java:74)
	at org.sosy_lab.java_smt.basicimpl.CachingModel.asList(CachingModel.java:38)
	at org.sosy_lab.java_smt.api.BasicProverEnvironment.getModelAssignments(BasicProverEnvironment.java:112)
	at org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper.getModelAssignments(BasicProverWithAssumptionsWrapper.java:89)
	at org.sosy_lab.cpachecker.util.predicates.smt.BasicProverEnvironmentView.getModelAssignments(BasicProverEnvironmentView.java:71)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.ProverEnvironmentWithFallback.getModelAssignments(ProverEnvironmentWithFallback.java:213)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.KInductionProver.check(KInductionProver.java:487)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.checkStepCase(AbstractBMCAlgorithm.java:563)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.run(AbstractBMCAlgorithm.java:496)
	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 added a commit that referenced this issue Jun 8, 2023
@kfriedberger
fix(#305): improve model generation for array theory.
99cf7ef 
I was not able to reconstruct the formula/model directly, but only within CPAchecker.
So we do not have a test for this case, except CPAchecker execution.
For details, see #305.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Princess
Milestone
No milestone
Development

No branches or pull requests
1 participant
@kfriedberger