null pointer exception from CVC3 prover

[Stephen Siegel]

Run AdderTest now (TASSv1.0 r1532) and you will get a null pointer exception inside CVC3, which is caused by something in the valid method in CVC3TheoremProver setting the assumption to null, even though the context passed to this method was not null.

java.lang.NullPointerException
	at cvc3.ValidityChecker.assertFormula(ValidityChecker.java:1289)
	at edu.udel.cis.vsl.tass.prove.cvc.CVC3TheoremProver.addAssumption(CVC3TheoremProver.java:1014)
	at edu.udel.cis.vsl.tass.prove.cvc.CVC3TheoremProver.valid(CVC3TheoremProver.java:567)
	at edu.udel.cis.vsl.tass.prove.ideal.IdealCVC3HybridProver.valid(IdealCVC3HybridProver.java:49)
	at edu.udel.cis.vsl.tass.dynamic.impl.DynamicFactory.valid(DynamicFactory.java:870)
	at edu.udel.cis.vsl.tass.dynamic.impl.DynamicFactory.isValid(DynamicFactory.java:823)
	at edu.udel.cis.vsl.tass.verify.urgent.Enabler.newPathCondition(Enabler.java:346)
	at edu.udel.cis.vsl.tass.verify.urgent.Enabler.enabledTransitions(Enabler.java:107)
	at edu.udel.cis.vsl.tass.verify.urgent.Enabler.enabledTransitions(Enabler.java:1)
	at edu.udel.cis.vsl.tass.search.DfsSearcher.proceedToNewState(DfsSearcher.java:195)
	at edu.udel.cis.vsl.tass.search.DfsSearcher.search(DfsSearcher.java:141)
	at edu.udel.cis.vsl.tass.search.DfsSearcher.search(DfsSearcher.java:122)
	at edu.udel.cis.vsl.tass.verify.Comparison.compare(Comparison.java:84)
	at adder.AdderTest.testCompare(AdderTest.java:55)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:44)
	at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:15)
	at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:41)
	at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:20)
	at org.junit.internal.runners.statements.RunBefores.evaluate(RunBefores.java:28)
	at org.junit.internal.runners.statements.RunAfters.evaluate(RunAfters.java:31)
	at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:73)
	at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:46)
	at org.junit.runners.ParentRunner.runChildren(ParentRunner.java:180)
	at org.junit.runners.ParentRunner.access$000(ParentRunner.java:41)
	at org.junit.runners.ParentRunner$1.evaluate(ParentRunner.java:173)
	at org.junit.internal.runners.statements.RunBefores.evaluate(RunBefores.java:28)
	at org.junit.internal.runners.statements.RunAfters.evaluate(RunAfters.java:31)
	at org.junit.runners.ParentRunner.run(ParentRunner.java:220)
	at org.eclipse.jdt.internal.junit4.runner.JUnit4TestReference.run(JUnit4TestReference.java:46)
	at org.eclipse.jdt.internal.junit.runner.TestExecution.run(TestExecution.java:38)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:467)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:683)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.run(RemoteTestRunner.java:390)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.main(RemoteTestRunner.java:197)

[ywei]

How did you run the adder example? I still got the unresolved compilation problem exception and couldn't reproduce the null pointer exception.

[Stephen Siegel]

I am just running through Eclipse by clicking on AdderTest.java and selecting "Run As JUnit Test."
I have my usual commandline args:
-ea -d64 -Djava.library.path=/tools/cvc3-20090309/java/lib

[ywei]

That's exactly what I did and I got the the following trace:

java.lang.Error: Unresolved compilation problem:

The method newProver(SymbolicUniverseIF) of type UrgentVerificationFactory must override a superclass method

at edu.udel.cis.vsl.tass.verify.urgent.UrgentVerificationFactory.newProver(UrgentVerificationFactory.java:96)
at edu.udel.cis.vsl.tass.verify.IF.DualFactories.<init>(DualFactories.java:38)
at edu.udel.cis.vsl.tass.verify.Comparison.compare(Comparison.java:67)
at adder.AdderTest.testCompare(AdderTest.java:55)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
at java.lang.reflect.Method.invoke(Method.java:597)
at org.junit.internal.runners.TestMethodRunner.executeMethodBody(TestMethodRunner.java:99)
at org.junit.internal.runners.TestMethodRunner.runUnprotected(TestMethodRunner.java:81)
at org.junit.internal.runners.BeforeAndAfterRunner.runProtected(BeforeAndAfterRunner.java:34)
at org.junit.internal.runners.TestMethodRunner.runMethod(TestMethodRunner.java:75)
at org.junit.internal.runners.TestMethodRunner.run(TestMethodRunner.java:45)
at org.junit.internal.runners.TestClassMethodsRunner.invokeTestMethod(TestClassMethodsRunner.java:66)
at org.junit.internal.runners.TestClassMethodsRunner.run(TestClassMethodsRunner.java:35)
at org.junit.internal.runners.TestClassRunner$1.runUnprotected(TestClassRunner.java:42)
at org.junit.internal.runners.BeforeAndAfterRunner.runProtected(BeforeAndAfterRunner.java:34)
at org.junit.internal.runners.TestClassRunner.run(TestClassRunner.java:52)
at org.eclipse.jdt.internal.junit4.runner.JUnit4TestReference.run(JUnit4TestReference.java:45)
at org.eclipse.jdt.internal.junit.runner.TestExecution.run(TestExecution.java:38)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:460)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:673)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.run(RemoteTestRunner.java:386)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.main(RemoteTestRunner.java:196)

[ywei]

The problem is that the symbolic expression being parsed is an instance of a BooleanIdealExpression and CVC3TheoremProver class has no knowledge about it. I added the check in the parseSymExpr() method to throw a runtime exception. But as far as I know, an ideal expression has no corresponding interface in the IF package, so I will have to use condition like "if(expr instanceof IdealExpression)" to determine whether a symbolic expression is an ideal expression. My concern is does this violate the principle of the IF/impl contract in which CVC3TheoremProver class is only supposed to use the interfaces in the IF package.

[Stephen Siegel]

You're right that the prover doesn't need to know anything about IdealExpressions, etc., it should just recognize it as an instance of SymbolicExpressionIF. But it needs to call the method tree() on the symbolic expression to get the instance of TreeExpressionIF:

	/** Places a symbolic expression in the universe's internal
	 * canonical form into standard tree form. */
	TreeExpressionIF tree(SymbolicExpressionIF expression);

and then do its thing.

[ywei]

So I need to call the tree() method in SymbolicUniverseIF before I parse a symbolic expression to get the standard tree form? I added "expr = this.universe.tree(expr);" in CVC3TheoremProver where expr is the symbolic expression but I got a class cast exception as below: (svn update needed)
java.lang.ClassCastException: edu.udel.cis.vsl.tass.symbolic.cnf.OrExpression cannot be cast to edu.udel.cis.vsl.tass.symbolic.ideal.IdealExpression

at edu.udel.cis.vsl.tass.symbolic.ideal.IdealUniverse.tree(IdealUniverse.java:1020)
at edu.udel.cis.vsl.tass.prove.cvc.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:124)
at edu.udel.cis.vsl.tass.prove.cvc.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:183)
at edu.udel.cis.vsl.tass.prove.cvc.CVC3TheoremProver.valid(CVC3TheoremProver.java:570)
at edu.udel.cis.vsl.tass.prove.ideal.IdealCVC3HybridProver.valid(IdealCVC3HybridProver.java:49)
at edu.udel.cis.vsl.tass.dynamic.impl.DynamicFactory.valid(DynamicFactory.java:865)
at edu.udel.cis.vsl.tass.dynamic.impl.DynamicFactory.isValid(DynamicFactory.java:818)
at edu.udel.cis.vsl.tass.verify.urgent.Enabler.newPathCondition(Enabler.java:346)
at edu.udel.cis.vsl.tass.verify.urgent.Enabler.enabledTransitions(Enabler.java:107)
at edu.udel.cis.vsl.tass.verify.urgent.Enabler.enabledTransitions(Enabler.java:34)
at edu.udel.cis.vsl.tass.search.DfsSearcher.proceedToNewState(DfsSearcher.java:195)
at edu.udel.cis.vsl.tass.search.DfsSearcher.search(DfsSearcher.java:141)
at edu.udel.cis.vsl.tass.search.DfsSearcher.search(DfsSearcher.java:122)
at edu.udel.cis.vsl.tass.verify.Comparison.compare(Comparison.java:84)
at adder.AdderTest.testCompare(AdderTest.java:55)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
at java.lang.reflect.Method.invoke(Method.java:597)
at org.junit.internal.runners.TestMethodRunner.executeMethodBody(TestMethodRunner.java:99)
at org.junit.internal.runners.TestMethodRunner.runUnprotected(TestMethodRunner.java:81)
at org.junit.internal.runners.BeforeAndAfterRunner.runProtected(BeforeAndAfterRunner.java:34)
at org.junit.internal.runners.TestMethodRunner.runMethod(TestMethodRunner.java:75)
at org.junit.internal.runners.TestMethodRunner.run(TestMethodRunner.java:45)
at org.junit.internal.runners.TestClassMethodsRunner.invokeTestMethod(TestClassMethodsRunner.java:66)
at org.junit.internal.runners.TestClassMethodsRunner.run(TestClassMethodsRunner.java:35)
at org.junit.internal.runners.TestClassRunner$1.runUnprotected(TestClassRunner.java:42)
at org.junit.internal.runners.BeforeAndAfterRunner.runProtected(BeforeAndAfterRunner.java:34)
at org.junit.internal.runners.TestClassRunner.run(TestClassRunner.java:52)
at org.eclipse.jdt.internal.junit4.runner.JUnit4TestReference.run(JUnit4TestReference.java:45)
at org.eclipse.jdt.internal.junit.runner.TestExecution.run(TestExecution.java:38)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:460)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:673)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.run(RemoteTestRunner.java:386)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.main(RemoteTestRunner.java:196)

[Stephen Siegel]

The methods you want to use to get arguments and operators are only defined on TreeExpressionIF, not on SymbolicExpressionIF, so if you want to use those methods you certainly need to convert to a tree first.

It isn't clear to me why you would use the same variable expr for both the original symbolic expression and the tree, since the first is an instance of SymbolicExpressionIF and the second is an instance of TreeExpressionIF (which is a subtype of SymbolicExpressionIF) and you are definitely going to want a variable of type TreeExpressionIF if you are going to do anything with it. What is the type of your variable expr?

I will look into the cause of the exception.

[Stephen Siegel]

The problem is you are invoking tree() on an expression which is already a TreeExpresionIF because you are calling your method parseSymExpr recursively. The symbolic universe is correctly complaining about this. The method tree(...) take a canonical expression and returns a tree expression. It does not take a tree expression.

You only need to convert to tree once. All of the arguments from a tree expression are tree expressions.

[ywei]

I see what you mean. I will change the way the parseSymExpr() method work to deal with this situation.

[ywei]

Now I got an array out of bound exception (svn update needed):

java.lang.ArrayIndexOutOfBoundsException: 1

at edu.udel.cis.vsl.tass.symbolic.monic.MonicMonomial.argument(MonicMonomial.java:168)
at edu.udel.cis.vsl.tass.prove.cvc.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:162)
at edu.udel.cis.vsl.tass.prove.cvc.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:162)
at edu.udel.cis.vsl.tass.prove.cvc.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:149)
at edu.udel.cis.vsl.tass.prove.cvc.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:157)
at edu.udel.cis.vsl.tass.prove.cvc.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:162)
at edu.udel.cis.vsl.tass.prove.cvc.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:182)
at edu.udel.cis.vsl.tass.prove.cvc.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:192)
at edu.udel.cis.vsl.tass.prove.cvc.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:177)
at edu.udel.cis.vsl.tass.prove.cvc.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:173)
at edu.udel.cis.vsl.tass.prove.cvc.CVC3TheoremProver.valid(CVC3TheoremProver.java:550)
at edu.udel.cis.vsl.tass.prove.ideal.IdealCVC3HybridProver.valid(IdealCVC3HybridProver.java:49)
at edu.udel.cis.vsl.tass.dynamic.impl.DynamicFactory.valid(DynamicFactory.java:865)
at edu.udel.cis.vsl.tass.dynamic.impl.DynamicFactory.isValid(DynamicFactory.java:818)
at edu.udel.cis.vsl.tass.verify.urgent.Enabler.newPathCondition(Enabler.java:346)
at edu.udel.cis.vsl.tass.verify.urgent.Enabler.enabledTransitions(Enabler.java:107)
at edu.udel.cis.vsl.tass.verify.urgent.Enabler.enabledTransitions(Enabler.java:34)
at edu.udel.cis.vsl.tass.search.DfsSearcher.proceedToNewState(DfsSearcher.java:195)
at edu.udel.cis.vsl.tass.search.DfsSearcher.search(DfsSearcher.java:141)
at edu.udel.cis.vsl.tass.search.DfsSearcher.search(DfsSearcher.java:122)
at edu.udel.cis.vsl.tass.verify.Comparison.compare(Comparison.java:84)
at adder.AdderTest.testCompare(AdderTest.java:55)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
at java.lang.reflect.Method.invoke(Method.java:597)
at org.junit.internal.runners.TestMethodRunner.executeMethodBody(TestMethodRunner.java:99)
at org.junit.internal.runners.TestMethodRunner.runUnprotected(TestMethodRunner.java:81)
at org.junit.internal.runners.BeforeAndAfterRunner.runProtected(BeforeAndAfterRunner.java:34)
at org.junit.internal.runners.TestMethodRunner.runMethod(TestMethodRunner.java:75)
at org.junit.internal.runners.TestMethodRunner.run(TestMethodRunner.java:45)
at org.junit.internal.runners.TestClassMethodsRunner.invokeTestMethod(TestClassMethodsRunner.java:66)
at org.junit.internal.runners.TestClassMethodsRunner.run(TestClassMethodsRunner.java:35)
at org.junit.internal.runners.TestClassRunner$1.runUnprotected(TestClassRunner.java:42)
at org.junit.internal.runners.BeforeAndAfterRunner.runProtected(BeforeAndAfterRunner.java:34)
at org.junit.internal.runners.TestClassRunner.run(TestClassRunner.java:52)
at org.eclipse.jdt.internal.junit4.runner.JUnit4TestReference.run(JUnit4TestReference.java:45)
at org.eclipse.jdt.internal.junit.runner.TestExecution.run(TestExecution.java:38)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:460)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:673)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.run(RemoteTestRunner.java:386)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.main(RemoteTestRunner.java:196)

I don't quite understand why the expression kind of a single symbolic constant is still MULTIPLY.

[Stephen Siegel]

OK, close this ticket as resolved and open new one with the array bound exception.