Array out of bound exception in AdderTest

[ywei]

Running AdderTest using JUnit and got an array out of bound exception as below:

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)

[Stephen Siegel]

The exception means that you are asking for an argument to a tree expression which does not exist. You need to call numArguments() first to see how many there are. Most of the expressions (add, and, multiply, etc.) can take any number of arguments, not just two.

[ywei]

I looked at the debugger and found that the expression that represents a single symbolic constant "X0" has the expression kind MULTIPLY, which leads to the exception. I don't quite understand the reason. Shouldn't the expression kind be SYMBOLIC_CONSTANT instead?

[Stephen Siegel]

It is equivalent. Multiply {x} = x = Add {x} = Multiply { Multiply {Multiply {x}}}.
"Multiply" means the product of all the numbers in the list. (1, if the list is empty.)
"Add" means the sum of all the numbers in the list. (0, if the list is empty.).
"And" means the conjunction of all the expressions in the list. (true if list is empty.)
"Or" means the disjunction (false if empty.)
And so on.

It comes that way because the expression is a monomial, which is a product of the form X1^{n1 * ... Xr}nr, and this monomial just happens to have one factor. But you don't have to know about that to process it.

[ywei]

I changed CVC3TheoremProver to fix the exception. Now I got another one as below:

java.lang.IllegalArgumentException: Real expression not instanceof RationalExpression: X1[0]

at edu.udel.cis.vsl.tass.symbolic.ideal.IdealUniverse.ideal(IdealUniverse.java:656)
at edu.udel.cis.vsl.tass.symbolic.ideal.IdealUniverse.arrayRead(IdealUniverse.java:364)
at edu.udel.cis.vsl.tass.symbolic.ideal.IdealUniverse.arrayRead(IdealUniverse.java:1)
at edu.udel.cis.vsl.tass.dynamic.impl.DynamicFactory.arrayRead(DynamicFactory.java:212)
at edu.udel.cis.vsl.tass.semantics.impl.Evaluator.dereference(Evaluator.java:503)
at edu.udel.cis.vsl.tass.semantics.impl.Evaluator.evaluateSubscript(Evaluator.java:519)
at edu.udel.cis.vsl.tass.semantics.impl.Evaluator.evaluateBinary(Evaluator.java:312)
at edu.udel.cis.vsl.tass.semantics.impl.Evaluator.evaluate(Evaluator.java:248)
at edu.udel.cis.vsl.tass.semantics.impl.Evaluator.evaluateBinary(Evaluator.java:323)
at edu.udel.cis.vsl.tass.semantics.impl.Evaluator.evaluate(Evaluator.java:248)
at edu.udel.cis.vsl.tass.semantics.impl.Executor.executeAssignment(Executor.java:251)
at edu.udel.cis.vsl.tass.semantics.impl.Executor.execute(Executor.java:101)
at edu.udel.cis.vsl.tass.verify.urgent.StateManager.nextStateSimple(StateManager.java:105)
at edu.udel.cis.vsl.tass.verify.urgent.StateManager.nextState(StateManager.java:92)
at edu.udel.cis.vsl.tass.verify.urgent.StateManager.nextState(StateManager.java:24)
at edu.udel.cis.vsl.tass.search.DfsSearcher.proceedToNewState(DfsSearcher.java:183)
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)