simplify error in diffusion1

[Stephen Siegel]

The current problem in diffusion1 happens in the simplify routine. I am running with the options shown below. If you run through the debugger you will see the expression being simplified is this:

(LET cvc_0 = (m0v14 WITH [1] := X1[0])
IN (cvc_0 WITH [2] := (cvc_0[2] WITH [0] := X1[1])))

The error message is a type error from CVC3:

+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|  version 1.0.r1240 (2009-12-20)        http://vsl.cis.udel.edu/tass  |
+----------------------------------------------------------------------+
               model : diffusion1_par (numProcs = 2)
          sourceFile : examples/diffusion/diffusion1_par.mmp
                mode : VERIFY
              prover : CVC3
            deadlock : IGNORE
           reduction : URGENT
            simplify : true
             verbose : false
         loop method : false
          repository : ./TASSREP

cvc3.TypecheckException: Type Checking error: Expected an ARRAY type in

  (m0v14 WITH [1] := X1[0])[2]

But received this:

  REAL

In the expression:

  ((m0v14 WITH [1] := X1[0])[2] WITH [0] := X1[1])
	at cvc3.ValidityChecker.jniSimplify(Native Method)
	at cvc3.ValidityChecker.simplify(ValidityChecker.java:1304)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.simplify(CVC3TheoremProver.java:723)
	at edu.udel.cis.vsl.minimp.symbolic.SymUniverse.writeExpr(SymUniverse.java:1426)
	at edu.udel.cis.vsl.minimp.symbolic.SymUniverse.writeExpr(SymUniverse.java:1439)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.convertArrayWrite(CVC3TheoremProver.java:1101)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.convertBack(CVC3TheoremProver.java:969)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.simplify(CVC3TheoremProver.java:734)
	at edu.udel.cis.vsl.minimp.symbolic.SymUniverse.writeExpr(SymUniverse.java:1426)
	at edu.udel.cis.vsl.minimp.symbolic.SymUniverse.writeExpr(SymUniverse.java:1439)
	at edu.udel.cis.vsl.minimp.symbolic.SymUniverse.writeExpr(SymUniverse.java:1445)
	at edu.udel.cis.vsl.minimp.dynamic.impl.value.ValueFactory.symExpression(ValueFactory.java:242)
	at edu.udel.cis.vsl.minimp.dynamic.impl.value.ValueFactory.symExpression(ValueFactory.java:261)
	at edu.udel.cis.vsl.minimp.dynamic.impl.value.ValueFactory.symExpression(ValueFactory.java:268)
	at edu.udel.cis.vsl.minimp.dynamic.impl.DynamicFactory.arrayReadSymbolic(DynamicFactory.java:184)
	at edu.udel.cis.vsl.minimp.dynamic.impl.DynamicFactory.arrayRead(DynamicFactory.java:174)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.dereference(Evaluator.java:426)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateSubscript(Evaluator.java:442)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateBinary(Evaluator.java:296)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluate(Evaluator.java:253)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateBinary(Evaluator.java:300)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluate(Evaluator.java:253)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateBinary(Evaluator.java:299)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluate(Evaluator.java:253)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateBinary(Evaluator.java:300)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluate(Evaluator.java:253)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateBinary(Evaluator.java:300)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluate(Evaluator.java:253)
	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.urgent.StateManager.nextStateSimple(StateManager.java:90)
	at edu.udel.cis.vsl.minimp.verify.urgent.StateManager.nextState(StateManager.java:77)
	at edu.udel.cis.vsl.minimp.verify.urgent.StateManager.nextState(StateManager.java:1)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.proceedToNewState(DfsSearcher.java:145)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:107)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:93)
	at edu.udel.cis.vsl.minimp.verify.Verification.verify(Verification.java:82)
	at edu.udel.cis.vsl.minimp.verify.Verification.verify(Verification.java:32)
	at edu.udel.cis.vsl.minimp.MiniMP.verify(MiniMP.java:415)
	at edu.udel.cis.vsl.minimp.MiniMP.main(MiniMP.java:483)

Here is a randomly-selected state, from which you see m0v14 is the value of v. Its type is real[m].

begin state 4
  save = false
  onStack = false;
  seen = false;
  pathCondition : (((((X6*-1)+2)+(((X0*-1)/2)*-1))==0)&&((0<X4)&&((0<=((X3*-1)+3))&&((0<=(X3+-1))&&((0<((X2*-1)+0.5))&&((0<X2)&&((0<=((X0*-1)+3))&&(0<=(X0+-2)))))))))
  begin model state
    begin shared variables
      nx = X0 (int);
      u0 = X1 (real[X0]);
      k = X2 (real);
      nsteps = X3 (int);
      dt = X4 (real);
      kappa = X5 (real);
      m = X6 (int);
      data = m0v7 (real[(X3+1)][X0]);
    end shared variables;
    begin process 0
      begin global variables
        nprocs = 2 (int);
        left = -1 (int);
        right = 1 (int);
        nxl = undefined (int);
        first = undefined (int);
        buf = m0v13 (real[2]);
        v = m0v14 (real[X6]);
        v_new = m0v15 (real[X6]);
      end global variables;
      begin stack frame 1
        function : init;
        location : 3;
        i = undefined (int);
        owner = undefined (int);
      end stack frame 1;
      begin stack frame 0
        function : main;
        location : 0;
        iter = undefined (int);
      end stack frame 0;
    end process 0;
    begin process 1
      begin global variables
        nprocs = undefined (int);
        left = undefined (int);
        right = undefined (int);
        nxl = undefined (int);
        first = undefined (int);
        buf = m0v21 (real[2]);
        v = m0v22 (real[X6]);
        v_new = m0v23 (real[X6]);
      end global variables;
      begin stack frame 0
        function : main;
        location : 0;
        iter = undefined (int);
      end stack frame 0;
    end process 1;
  end model state
end state 4.

[Stephen Siegel]

I have a smaller instance of the problem which I will check in. Run it through the debugger. You will see that simplify gets called with

m0v13<([0]), ((((X0*-1)+2)==0)?0:X1[1])>

which is type correct because m0v13 is a 1-dimensional array. However, a little later in the call stack after the convertArrayWrite and writeExpr, the list of indices becomes [0,0], i.e., it is now treating it as a 2-dimensional array. So there is some problem in the simplify routine.

[Stephen Siegel]

Yi fixed this in revision 1276.