Laplace test errors

[Stephen Siegel]

Laplace tests have syntax exception.

[Stephen Siegel]

Here's the syntax error. The exit location for a branch location is not being set by the model builder.

void sendrecv(real[] sendbuf, int dest, int sendtag, real[] recvbuf, int source, int recvtag) {
  if (source != -1 && dest != -1){
    select
      when (true) {send(sendbuf, dest, sendtag); recv(recvbuf, source, recvtag);}
      when (true) {recv(recvbuf, source, recvtag); send(sendbuf, dest, sendtag);}
  }
  else {  /* either source or dest is invalid */
    if (source != -1) {
      recv(recvbuf, source, recvtag);
    }
    if (dest != -1) {
      send(sendbuf, dest, sendtag);
    }
  }
}

edu.udel.cis.vsl.minimp.model.IF.SyntaxException: Syntax error in laplaceImpl.mmp 89.4--89.18: "if (dest != -1)":
null[8]
Exit location for branch location has not been set
	at edu.udel.cis.vsl.minimp.model.impl.location.BranchLocation.complete(BranchLocation.java:28)
	at edu.udel.cis.vsl.minimp.model.impl.Function.complete(Function.java:341)
	at edu.udel.cis.vsl.minimp.model.impl.Process.complete(Process.java:122)
	at edu.udel.cis.vsl.minimp.model.impl.Model.complete(Model.java:171)
	at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processAST(ModelBuilder.java:275)
	at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.buildModel(ModelBuilder.java:162)
	at edu.udel.cis.vsl.minimp.test.LaplaceTest.setUpBeforeClass(LaplaceTest.java:56)
	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.RunBefores.evaluate(RunBefores.java:27)
	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]

Bug fixed. The example can now be parsed correctly. But I am getting an execution error as follows:
Exception in thread "main" edu.udel.cis.vsl.minimp.util.ExecutionException: Execution error encountered at laplaceImpl.mmp 29.8--29.12: "nxlg"
Cannot prove that extent 1 of array is nonnegative

at edu.udel.cis.vsl.minimp.semantics.impl.Executor.dimensions(Executor.java:774)
at edu.udel.cis.vsl.minimp.semantics.impl.Executor.arrayValueType(Executor.java:791)
at edu.udel.cis.vsl.minimp.semantics.impl.Executor.dynamicType(Executor.java:723)
at edu.udel.cis.vsl.minimp.semantics.impl.Executor.initializeVariable(Executor.java:548)
at edu.udel.cis.vsl.minimp.semantics.impl.Executor.initialize(Executor.java:604)
at edu.udel.cis.vsl.minimp.semantics.impl.Executor.initialize(Executor.java:615)
at edu.udel.cis.vsl.minimp.verify.std.StateManager.initialState(StateManager.java:49)
at edu.udel.cis.vsl.minimp.verify.Verification.verify(Verification.java:117)
at edu.udel.cis.vsl.minimp.MiniMP.verify(MiniMP.java:388)
at edu.udel.cis.vsl.minimp.MiniMP.main(MiniMP.java:505)

I think the reason is that the input variables nxlg and nylg are explicitly initialized, but input variables can not be written to.

[ywei]

I changed the input variables as follows:
input int nxlg {nxlg == 10};
input int nylg {nylg == 4};

And the program can verify that the extents of arrays are all non-negative. But I got another exception:
edu.udel.cis.vsl.minimp.util.ExecutionException: Execution error encountered at laplaceImpl.mmp 148.6--148.32: "grid[(new+1)%2][row][col] ="
Possible array out of bounds error:

array expression = grid[(new+1)%2][row]
index expression = col

index value = 4

array extent = X5

query = (4<X5)

path condition = ((X5==4)&&((X4==10)&&((0<X2)&&((0<X1)&&(0<X0)))))

at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.arrayElementReferenceValue(Evaluator.java:172)
at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.referenceValue(Evaluator.java:222)
at edu.udel.cis.vsl.minimp.semantics.impl.Executor.assignValue(Executor.java:236)
at edu.udel.cis.vsl.minimp.semantics.impl.Executor.executeAssignment(Executor.java:243)
at edu.udel.cis.vsl.minimp.semantics.impl.Executor.execute(Executor.java:99)
at edu.udel.cis.vsl.minimp.verify.std.StateManager.nextState(StateManager.java:74)
at edu.udel.cis.vsl.minimp.verify.std.StateManager.nextState(StateManager.java:1)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.proceedToNewState(DfsSearcher.java:141)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:102)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:88)
at edu.udel.cis.vsl.minimp.verify.Verification.verify(Verification.java:133)
at edu.udel.cis.vsl.minimp.MiniMP.verify(MiniMP.java:388)
at edu.udel.cis.vsl.minimp.MiniMP.main(MiniMP.java:505)

It looks like the while loop, from line 145 - 153 in laplaceImpl.mmp, had incorrect array upper bounds:
while (row < nylg) {

col = 0;
while (col < nxlg) {

grid[(new+1)%2][row][col] = 0.0;
grid[new][row][col] = 0.0;
col = col + 1;

}
row = row + 1;

}

I think the outer loop should have "row < nxlg" and inner loop should have "col < nxlg" since the definition of the array grid is "real[2][nxlg][nylg]" and the loop used grid[new][row][col] to get the element.