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

CVC5: parallel prover instances cause issues (found in CPAchecker benchmark) #310

Open
kfriedberger opened this issue Jun 4, 2023 · 6 comments · Fixed by #336
Open

CVC5: parallel prover instances cause issues (found in CPAchecker benchmark) #310

kfriedberger opened this issue Jun 4, 2023 · 6 comments · Fixed by #336
Labels
bug CVC5

Comments

@kfriedberger
Copy link
Member

Our expectation in CVC5 being able to provide multiple provers that can be used interleaved (or even parallel) based on a common basis (shared types and formulas) was not fulfilled.
There are multiple errors when applying CVC5 that way.

Examples from CPAchecker when applying kInduction (two provers applied in parallel)
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=CVC5 -setprop cpa.predicate.encodeBitvectorAs=BITVECTOR -timelimit 60s -stats -spec ../sv-benchmarks/c/properties/unreach-call.prp -32 ../sv-benchmarks/c/loops/n.c24.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/loops/n.c24.i" (CPAchecker.parse, INFO)

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

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

Using predicate analysis with CVC5 1.0.5. (Parallel analysis 1:PredicateCPA:PredicateCPA.<init>, INFO)

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

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

Using predicate analysis with CVC5 1.0.5. (Parallel analysis 1:InductionStepCase:PredicateCPA:PredicateCPA.<init>, INFO)

Using unsound approximation of 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)

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

Exception in thread "main" java.lang.IllegalArgumentException: symbol name __ADDRESS_OF_main::i@ with sort (_ BitVec 32) already in use for different sort null
	at com.google.common.base.Preconditions.checkArgument(Preconditions.java:463)
	at org.sosy_lab.java_smt.solvers.cvc5.CVC5FormulaCreator.makeVariable(CVC5FormulaCreator.java:93)
	at org.sosy_lab.java_smt.solvers.cvc5.CVC5FormulaCreator.makeVariable(CVC5FormulaCreator.java:66)
	at org.sosy_lab.java_smt.solvers.cvc5.CVC5BitvectorFormulaManager.makeVariableImpl(CVC5BitvectorFormulaManager.java:102)
	at org.sosy_lab.java_smt.solvers.cvc5.CVC5BitvectorFormulaManager.makeVariableImpl(CVC5BitvectorFormulaManager.java:21)
	at org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager.makeVariable(AbstractBitvectorFormulaManager.java:287)
	at org.sosy_lab.cpachecker.util.predicates.smt.BitvectorFormulaManagerView.makeVariable(BitvectorFormulaManagerView.java:159)
	at org.sosy_lab.cpachecker.util.predicates.smt.FormulaManagerView.makeVariable(FormulaManagerView.java:448)
	at org.sosy_lab.cpachecker.util.predicates.smt.FormulaManagerView.makeVariableWithoutSSAIndex(FormulaManagerView.java:999)
	at org.sosy_lab.cpachecker.util.predicates.pathformula.pointeraliasing.PointerTargetSetManager.makeBaseAddressConstraints(PointerTargetSetManager.java:568)
	at org.sosy_lab.cpachecker.util.predicates.pathformula.pointeraliasing.PointerTargetSetBuilder$RealPointerTargetSetBuilder.addNextBaseAddressConstraints(PointerTargetSetBuilder.java:286)
	at org.sosy_lab.cpachecker.util.predicates.pathformula.pointeraliasing.CToFormulaConverterWithPointerAliasing.declareSharedBase(CToFormulaConverterWithPointerAliasing.java:433)
	at org.sosy_lab.cpachecker.util.predicates.pathformula.pointeraliasing.CToFormulaConverterWithPointerAliasing.makeDeclaration(CToFormulaConverterWithPointerAliasing.java:967)
	at org.sosy_lab.cpachecker.util.predicates.pathformula.ctoformula.CtoFormulaConverter.createFormulaForEdge(CtoFormulaConverter.java:1211)
	at org.sosy_lab.cpachecker.util.predicates.pathformula.ctoformula.CtoFormulaConverter.makeAnd(CtoFormulaConverter.java:1029)
	at org.sosy_lab.cpachecker.util.predicates.pathformula.PathFormulaManagerImpl.makeAnd(PathFormulaManagerImpl.java:246)
	at org.sosy_lab.cpachecker.util.predicates.pathformula.PathFormulaManagerImpl.makeAnd(PathFormulaManagerImpl.java:300)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateTransferRelation.convertEdgeToPathFormula(PredicateTransferRelation.java:203)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateTransferRelation.getAbstractSuccessorsForEdge(PredicateTransferRelation.java:113)
	at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.callTransferRelation(CompositeTransferRelation.java:297)
	at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessorForSimpleEdge(CompositeTransferRelation.java:264)
	at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessorForEdge(CompositeTransferRelation.java:196)
	at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessors(CompositeTransferRelation.java:88)
	at org.sosy_lab.cpachecker.cpa.arg.ARGTransferRelation.getAbstractSuccessors(ARGTransferRelation.java:45)
	at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.handleState(CPAAlgorithm.java:334)
	at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run0(CPAAlgorithm.java:289)
	at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run(CPAAlgorithm.java:260)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.BMCHelper.unroll(BMCHelper.java:193)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.run(AbstractBMCAlgorithm.java:426)
	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

Another log file
(the error message just tells us that '4' is not an integer; integer theory seems to be unknown/undefined):

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=CVC5 -setprop cpa.predicate.encodeBitvectorAs=INTEGER -timelimit 60s -stats -spec ../sv-benchmarks/c/properties/unreach-call.prp -32 ../sv-benchmarks/c/loops/terminator_03-1.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/loops/terminator_03-1.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 CVC5 1.0.5. (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 CVC5 1.0.5. (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)

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

Exception in thread "main" java.lang.NumberFormatException: Number is not an integer value: 4
	at org.sosy_lab.java_smt.solvers.cvc5.CVC5IntegerFormulaManager.makeNumberImpl(CVC5IntegerFormulaManager.java:78)
	at org.sosy_lab.java_smt.solvers.cvc5.CVC5NumeralFormulaManager.makeNumberImpl(CVC5NumeralFormulaManager.java:103)
	at org.sosy_lab.java_smt.solvers.cvc5.CVC5NumeralFormulaManager.makeNumberImpl(CVC5NumeralFormulaManager.java:30)
	at org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.makeNumber(AbstractNumeralFormulaManager.java:93)
	at org.sosy_lab.cpachecker.util.predicates.smt.ReplaceBitvectorWithNumeralAndFunctionTheory.makeBitvector(ReplaceBitvectorWithNumeralAndFunctionTheory.java:156)
	at org.sosy_lab.cpachecker.util.predicates.smt.BitvectorFormulaManagerView.makeBitvector(BitvectorFormulaManagerView.java:149)
	at org.sosy_lab.cpachecker.util.predicates.smt.BitvectorFormulaManagerView.makeBitvector(BitvectorFormulaManagerView.java:44)
	at org.sosy_lab.cpachecker.util.predicates.smt.FormulaManagerView.makeNumber(FormulaManagerView.java:479)
	at org.sosy_lab.cpachecker.util.predicates.pathformula.pointeraliasing.CToFormulaConverterWithPointerAliasing.getSizeExpression(CToFormulaConverterWithPointerAliasing.java:470)
	at org.sosy_lab.cpachecker.util.predicates.pathformula.pointeraliasing.CToFormulaConverterWithPointerAliasing.declareSharedBase(CToFormulaConverterWithPointerAliasing.java:424)
	at org.sosy_lab.cpachecker.util.predicates.pathformula.pointeraliasing.CToFormulaConverterWithPointerAliasing.makeDeclaration(CToFormulaConverterWithPointerAliasing.java:967)
	at org.sosy_lab.cpachecker.util.predicates.pathformula.ctoformula.CtoFormulaConverter.createFormulaForEdge(CtoFormulaConverter.java:1211)
	at org.sosy_lab.cpachecker.util.predicates.pathformula.ctoformula.CtoFormulaConverter.makeAnd(CtoFormulaConverter.java:1029)
	at org.sosy_lab.cpachecker.util.predicates.pathformula.PathFormulaManagerImpl.makeAnd(PathFormulaManagerImpl.java:246)
	at org.sosy_lab.cpachecker.util.predicates.pathformula.PathFormulaManagerImpl.makeAnd(PathFormulaManagerImpl.java:300)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateTransferRelation.convertEdgeToPathFormula(PredicateTransferRelation.java:203)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateTransferRelation.getAbstractSuccessorsForEdge(PredicateTransferRelation.java:113)
	at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.callTransferRelation(CompositeTransferRelation.java:297)
	at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessorForSimpleEdge(CompositeTransferRelation.java:264)
	at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessorForEdge(CompositeTransferRelation.java:196)
	at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessors(CompositeTransferRelation.java:88)
	at org.sosy_lab.cpachecker.cpa.arg.ARGTransferRelation.getAbstractSuccessors(ARGTransferRelation.java:45)
	at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.handleState(CPAAlgorithm.java:334)
	at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run0(CPAAlgorithm.java:289)
	at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run(CPAAlgorithm.java:260)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.BMCHelper.unroll(BMCHelper.java:193)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.run(AbstractBMCAlgorithm.java:426)
	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)

@baierd baierd mentioned this issue Sep 1, 2023
Merged
@baierd
Copy link
Collaborator

baierd commented Oct 11, 2023

This looks like a bug in CVC5. Because what fails is our preconditions Preconditions.checkArgument(sort.equals(exp.getSort()), ...) second argument exp.getSort(), as it equals null. So CVC5 can not find the Sort of the Term exp.
We need to create a program that emulates this behavior and send it to the developers.

@baierd baierd mentioned this issue Oct 25, 2023
Merged
@baierd baierd linked a pull request Oct 25, 2023 that will close this issue
310 cvc5 parallel prover instances cause issues found in cpachecker benchmark #336
Merged
@baierd baierd reopened this Oct 25, 2023
@baierd
Copy link
Collaborator

baierd commented Oct 25, 2023

While the bug is fixed for now, there are 2 problems with CVC5 that caused this problem.

  1. getSort() sometimes returns null.
  2. Sorts are not equal, while being equal. Example, Bitvectors with the equal size do not compare to equal with Javas equals method. (The pointers are distinct, and it checks the pointers).

We need to report these issues to the CVC5 devs.

daniel-raffler added a commit that referenced this issue Dec 8, 2023
@daniel-raffler
Added tests to narrow down bug #339. So far no luck, but we did stumb…
02d93be 
…le upon bug #310 for CVC5.
@daniel-raffler daniel-raffler mentioned this issue Dec 8, 2023
Closed
@daniel-raffler daniel-raffler mentioned this issue Dec 20, 2023
Open
daniel-raffler added a commit to daniel-raffler/cvc5 that referenced this issue Jan 2, 2024
@daniel-raffler
(Java) Added test cases for sosy-lab/java-smt#310
de8dc61
daniel-raffler added a commit to daniel-raffler/cvc5 that referenced this issue Jan 2, 2024
@daniel-raffler
(C++) Added test cases for sosy-lab/java-smt#310
34d7bbb
@daniel-raffler daniel-raffler reopened this Jan 2, 2024
@daniel-raffler
Copy link
Contributor

I've had a closer look at this bug since I've run into the same issue while working on the new SolverThreadLocalityTest class for bug #347.

The problem is that CVC5 doesn't separate between solver context and prover environment in the same way as JavaSMT does. Instead a single "Solver" class is used for almost everything: from declaring functions to building terms, pushing assertions and checking satisfiability. Internally there is a "NodeManager" that comes pretty close to the functionality of SolverContext in that it stores all the definitions, sorts and formulas that are available. However, this class is not exposed through the API. Instead whenever a new Solver instance is created the "current" NodeManager is used. Here "current" is defined by a thread_local variable. As a result all Solver instances created on the same thread share a single NodeManager, and terms can be moved freely between them. On the other hand moving Solver instances between threads becomes impossible, even if there is never any concurrent access.

I've added some test cases for this issue to my fork of CVC5 here. The last commit (here) tries to fix the issue by making the NodeManager global (instead of thread local). This of course comes with its own problems and means that solver instances can no longer be run in parallel. (In fact this patch will (re-)break the test case for #347 I added just a few days ago.) However, all test in SolverThreadLocalityTest pass with it.

I'll add a bug report for CVC5 in the next few days. Hopefully they can help us find a better solution.

baierd pushed a commit that referenced this issue Jan 3, 2024
@daniel-raffler @baierd
Added tests to narrow down bug #339. So far no luck, but we did stumb…
d961c65 
…le upon bug #310 for CVC5.
@daniel-raffler
Copy link
Contributor

I've now opened a discussion on the CVC5 bugtracker:
cvc5/cvc5#10265

@daniel-raffler
Copy link
Contributor

daniel-raffler commented Apr 3, 2024 •
edited

CVC5 now has a new "TermManger" interface that should solve our problem:
cvc5/cvc5#10426
cvc5/cvc5#10531

I'll start working on an update to the solver backend in the next few days.

EDIT:
I've updated our bindings, but the tests still fail. Maybe the internal rewrite isn't quite done after all?

daniel-raffler added a commit that referenced this issue Apr 4, 2024
@daniel-raffler
CVC5: Updated the JavaSMT backend for CVC5 to use the new TermManager…
7d7b00c 
…. See cvc5/cvc5#10426 for the interface. This will solve issue #310.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug CVC5
Milestone
No milestone
3 participants
@baierd @kfriedberger @daniel-raffler