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: unexpected formula type "_0[any]" (found in CPAchecker benchmark) #307

Open
kfriedberger opened this issue Jun 4, 2023 · 1 comment
Open

Princess: unexpected formula type "_0[any]" (found in CPAchecker benchmark) #307

kfriedberger opened this issue Jun 4, 2023 · 1 comment
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 -predicateAnalysis -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeBitvectorAs=BITVECTOR -timelimit 60s -stats -spec ../sv-benchmarks/c/properties/unreach-call.prp -32 ../sv-benchmarks/c/loop-crafted/simple_array_index_value_4.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 / predicateAnalysis (OpenJDK 64-Bit Server VM 17.0.7) started (CPAchecker.run, INFO)

Parsing CFA from file(s) "../sv-benchmarks/c/loop-crafted/simple_array_index_value_4.i" (CPAchecker.parse, INFO)

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

Using predicate analysis with Princess 2022-11-03 and JFactory 1.21. (PredicateCPA:PredicateCPA.<init>, INFO)

Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. (PredicateCPA:PredicateCPARefiner.<init>, INFO)

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

Exception in thread "main" java.lang.IllegalArgumentException: Unknown formula type 'class ap.parser.ISortedVariable' for formula '_0[any]'.
	at org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.getFormulaType(PrincessEnvironment.java:516)
	at org.sosy_lab.java_smt.solvers.princess.PrincessFormulaCreator.getFormulaType(PrincessFormulaCreator.java:152)
	at org.sosy_lab.java_smt.solvers.princess.PrincessFormulaCreator.visit(PrincessFormulaCreator.java:370)
	at org.sosy_lab.java_smt.solvers.princess.PrincessFormulaCreator.visit(PrincessFormulaCreator.java:72)
	at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visit(FormulaCreator.java:278)
	at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.visit(AbstractFormulaManager.java:363)
	at org.sosy_lab.cpachecker.util.predicates.smt.FormulaManagerView.visit(FormulaManagerView.java:1847)
	at org.sosy_lab.cpachecker.util.predicates.smt.FormulaManagerView.myFreeVariableNodeTransformer(FormulaManagerView.java:1347)
	at org.sosy_lab.cpachecker.util.predicates.smt.FormulaManagerView.uninstantiate(FormulaManagerView.java:1211)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateAbstractionManager.lambda$getPredicatesForAtomsOf$2(PredicateAbstractionManager.java:1253)
	at com.google.common.collect.Iterators$6.transform(Iterators.java:828)
	at com.google.common.collect.TransformedIterator.next(TransformedIterator.java:52)
	at java.base/java.util.AbstractCollection.toArray(AbstractCollection.java:146)
	at com.google.common.collect.ImmutableSet.copyOf(ImmutableSet.java:240)
	at org.sosy_lab.common.collect.Collections3.transformedImmutableSetCopy(Collections3.java:129)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateAbstractionManager.getPredicatesForAtomsOf(PredicateAbstractionManager.java:1252)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateAbstractionRefinementStrategy.convertInterpolant(PredicateAbstractionRefinementStrategy.java:350)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateAbstractionRefinementStrategy.performRefinementForState(PredicateAbstractionRefinementStrategy.java:275)
	at org.sosy_lab.cpachecker.cpa.predicate.RefinementStrategy.evaluateInterpolantsOnPath(RefinementStrategy.java:195)
	at org.sosy_lab.cpachecker.cpa.predicate.RefinementStrategy.performRefinement(RefinementStrategy.java:98)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPARefiner.performRefinementForPath(PredicateCPARefiner.java:289)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateStaticRefiner.performRefinementForPath(PredicateStaticRefiner.java:183)
	at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinementForPath(AbstractARGBasedRefiner.java:158)
	at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinement(AbstractARGBasedRefiner.java:104)
	at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.refine(CEGARAlgorithm.java:310)
	at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.run(CEGARAlgorithm.java:256)
	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)
Caused by: java.lang.IllegalArgumentException: Unknown formula type 'class ap.types.Sort$$anon$1' for sort 'any'.
	at org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.getFormulaTypeFromSort(PrincessEnvironment.java:550)
	at org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.getFormulaType(PrincessEnvironment.java:512)
	... 28 more
@kfriedberger
Copy link
Member Author

Same here:
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 -predicateAnalysis -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeBitvectorAs=BITVECTOR -timelimit 60s -stats -spec ../sv-benchmarks/c/properties/unreach-call.prp -32 ../sv-benchmarks/c/loops/insertion_sort-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 / predicateAnalysis (OpenJDK 64-Bit Server VM 17.0.7) started (CPAchecker.run, INFO)

Parsing CFA from file(s) "../sv-benchmarks/c/loops/insertion_sort-1.c" (CPAchecker.parse, INFO)

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

Using predicate analysis with Princess 2022-11-03 and JFactory 1.21. (PredicateCPA:PredicateCPA.<init>, INFO)

Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. (PredicateCPA:PredicateCPARefiner.<init>, INFO)

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

Exception in thread "main" java.lang.IllegalArgumentException: Unknown formula type 'class ap.parser.ISortedVariable' for formula '_0[any]'.
	at org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.getFormulaType(PrincessEnvironment.java:516)
	at org.sosy_lab.java_smt.solvers.princess.PrincessFormulaCreator.getFormulaType(PrincessFormulaCreator.java:152)
	at org.sosy_lab.java_smt.solvers.princess.PrincessFormulaCreator.visit(PrincessFormulaCreator.java:370)
	at org.sosy_lab.java_smt.solvers.princess.PrincessFormulaCreator.visit(PrincessFormulaCreator.java:72)
	at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visit(FormulaCreator.java:278)
	at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.visit(AbstractFormulaManager.java:363)
	at org.sosy_lab.cpachecker.util.predicates.smt.FormulaManagerView.visit(FormulaManagerView.java:1847)
	at org.sosy_lab.cpachecker.util.predicates.smt.FormulaManagerView.myFreeVariableNodeTransformer(FormulaManagerView.java:1347)
	at org.sosy_lab.cpachecker.util.predicates.smt.FormulaManagerView.uninstantiate(FormulaManagerView.java:1211)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateAbstractionManager.lambda$getPredicatesForAtomsOf$2(PredicateAbstractionManager.java:1253)
	at com.google.common.collect.Iterators$6.transform(Iterators.java:828)
	at com.google.common.collect.TransformedIterator.next(TransformedIterator.java:52)
	at java.base/java.util.AbstractCollection.toArray(AbstractCollection.java:146)
	at com.google.common.collect.ImmutableSet.copyOf(ImmutableSet.java:240)
	at org.sosy_lab.common.collect.Collections3.transformedImmutableSetCopy(Collections3.java:129)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateAbstractionManager.getPredicatesForAtomsOf(PredicateAbstractionManager.java:1252)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateAbstractionRefinementStrategy.convertInterpolant(PredicateAbstractionRefinementStrategy.java:350)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateAbstractionRefinementStrategy.performRefinementForState(PredicateAbstractionRefinementStrategy.java:275)
	at org.sosy_lab.cpachecker.cpa.predicate.RefinementStrategy.evaluateInterpolantsOnPath(RefinementStrategy.java:195)
	at org.sosy_lab.cpachecker.cpa.predicate.RefinementStrategy.performRefinement(RefinementStrategy.java:98)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPARefiner.performRefinementForPath(PredicateCPARefiner.java:289)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateStaticRefiner.performRefinementForPath(PredicateStaticRefiner.java:183)
	at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinementForPath(AbstractARGBasedRefiner.java:158)
	at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinement(AbstractARGBasedRefiner.java:104)
	at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.refine(CEGARAlgorithm.java:310)
	at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.run(CEGARAlgorithm.java:256)
	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)
Caused by: java.lang.IllegalArgumentException: Unknown formula type 'class ap.types.Sort$$anon$1' for sort 'any'.
	at org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.getFormulaTypeFromSort(PrincessEnvironment.java:550)
	at org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.getFormulaType(PrincessEnvironment.java:512)
	... 28 more

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