search

sosy-lab / java-smt

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

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

Open kfriedberger opened 1 year ago

kfriedberger commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 10 months ago

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.

daniel-raffler commented 10 months ago

I've now opened a discussion on the CVC5 bugtracker: https://github.com/cvc5/cvc5/discussions/10265

daniel-raffler commented 7 months ago

CVC5 now has a new "TermManger" interface that should solve our problem: https://github.com/cvc5/cvc5/pull/10426 https://github.com/cvc5/cvc5/pull/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?