/*
 * $Id: CalcApplet.java,v 1.1 2004/06/09 13:37:07 martijno Exp $
 */

package applet;

import javacard.framework.*;

/**
 * Sample Java Card Calculator applet which operates on signed
 * shorts. Overflow is silent.
 *
 * Command APDU should have class byte 0xCC. The instructions are
 * the ASCII characters of the keypad keys: '0' - '9', '+', '-',
 * 'x', ':', '=', etc. This means that the terminal should send an
 * APDU for each key pressed.
 *
 * Response APDU consists of 5 data bytes. First byte indicates
 * whether the M register contains a non-zero value. The third
 * and fourth bytes encode the X register (the signed short value
 * to be displayed).
 *
 * The only non-transient field is m. This means that m is stored
 * in EEPROM and all other memory used is RAM.
 *
 * @author Martijn Oostdijk (martijno@cs.kun.nl)
 *
 * @version $Revision: 1.1 $
 */
public class CalcApplet extends Applet implements ISO7816 {

   static final byte CLA_CALC = (byte)0xCC;

   static final byte X = 0;
   static final byte Y = 1;

   /*@ non_null @*/ short[] xy;
   //@ invariant xy.length == 2;

   short m;

   /*@ non_null @*/ byte[] lastOp;
   //@ invariant lastOp.length == 1;

   /*@ non_null @*/ boolean[] lastKeyWasDigit;
   //@ invariant lastKeyWasDigit.length == 1;

   /*@ 
     @ ensures xy.length== 2;
     @ ensures lastOp.length== 1;
     @ ensures lastKeyWasDigit.length== 1;
     @ ensures m == 0;
     @*/
   public CalcApplet() throws SystemException {
      xy = JCSystem.makeTransientShortArray((short)2,JCSystem.CLEAR_ON_RESET);
      lastOp = JCSystem.makeTransientByteArray((short)1,JCSystem.CLEAR_ON_RESET);
      lastKeyWasDigit = JCSystem.makeTransientBooleanArray((short)1,JCSystem.CLEAR_ON_RESET);
      m = 0;
      register();
   }

   public static void install(byte[] buffer, short offset, byte length) throws SystemException {
      new CalcApplet();
   }

   /*@
     @ also
     @ assignable xy[X];
     @ assignable xy[Y];
     @ assignable lastOp[0];
     @ assignable lastKeyWasDigit[0];
     @ ensures (\forall byte i; 0 <= i && i < xy.length ==> xy[i] == 0);
     @ ensures lastOp[0] == (byte)'=';
     @ ensures !lastKeyWasDigit[0];
     @*/
   public boolean select() {
      xy[X] = 0;
      xy[Y] = 0;
      lastOp[0] = (byte)'=';
      lastKeyWasDigit[0] = false;
      return true;
   }

   /*@
     @ also
     @ requires apdu != null;
     @ requires apdu._APDU_state == 1;
     @ assignable xy[X];
     @ assignable xy[Y];
     @ assignable lastOp[0];
     @ assignable lastKeyWasDigit[0];
     @ assignable apdu._APDU_state;
     @ assignable m;
     @
     @ assignable \everything; // Needed because of a bug in ESCJava2?
     @
     @ signals (ISOException) true;
     @ signals (APDUException) true;
     @*/
   public void process(APDU apdu) throws ISOException, APDUException {
      byte[] buffer = apdu.getBuffer();
      byte cla = buffer[OFFSET_CLA];
      byte ins = buffer[OFFSET_INS];
      short lc = (short)(buffer[OFFSET_LC] & 0x00FF);
      short le = -1;

      /* Ignore the APDU that selects this applet... */
      if (selectingApplet()) {
         return;
      }

      if (cla != CLA_CALC) {
         ISOException.throwIt(SW_CLA_NOT_SUPPORTED);
      }

      switch (ins) {
         case '0': 
            digit((byte)0);
            break;
         case '1': 
            digit((byte)1);
            break;
         case '2': 
            digit((byte)2);
            break;
         case '3': 
            digit((byte)3);
            break;
         case '4': 
            digit((byte)4);
            break;
         case '5': 
            digit((byte)5);
            break;
         case '6': 
            digit((byte)6);
            break;
         case '7': 
            digit((byte)7);
            break;
         case '8': 
            digit((byte)8);
            break;
         case '9': 
            digit((byte)9);
            break;
         case '+':
         case '-':
         case 'x':
         case ':':
         case '=':
            operator(ins);
            break;
         case 'S':
         case 'R':
         case 'M':
            mem(ins);
            break;
         case 'C':
            select();
            break;
         default:
            ISOException.throwIt(SW_INS_NOT_SUPPORTED);
      }
      //@ assert apdu._APDU_state == 1;
      le = apdu.setOutgoing();
      //@ assert apdu._APDU_state == 3;
      if (le < 5) {
         ISOException.throwIt((short)(SW_WRONG_LENGTH | 5));
      }
      buffer[0] = (m == 0) ? (byte)0x00 : (byte)0x01;
      Util.setShort(buffer,(short)1,(short)0);
      Util.setShort(buffer,(short)3,xy[X]);
      apdu.setOutgoingLength((short)5);
      //@ assert apdu._APDU_state == 4;
      apdu.sendBytes((short)0,(short)5);
      //@ assert apdu._APDU_state == 4;
   }

   /*@ 
     @ assignable xy[X];
     @ assignable xy[Y];
     @ assignable lastKeyWasDigit[0];
     @ ensures lastKeyWasDigit[0];
     @*/
   void digit(byte d) {
      if (!lastKeyWasDigit[0]) {
         xy[Y] = xy[X];
         xy[X] = 0;
      }
      xy[X] = (short)((short)(xy[X] * 10) + (short)(d & 0x00FF));
      lastKeyWasDigit[0] = true;
   }

   /*@
     @ assignable lastOp[0];
     @ assignable lastKeyWasDigit[0];
     @ assignable xy[X];
     @ ensures !lastKeyWasDigit[0];
     @*/
   void operator(byte op) throws ISOException {
      switch (lastOp[0]) {
         case '+':
            xy[X] = (short)(xy[Y] + xy[X]);
            break;
         case '-':
            xy[X] = (short)(xy[Y] - xy[X]);
            break;
         case 'x':
            xy[X] = (short)(xy[Y] * xy[X]);
            break;
         case ':':
            if (xy[X] == 0) {
               ISOException.throwIt(SW_WRONG_DATA);
            }
            //@ assert xy[X] != 0;
            xy[X] = (short)(xy[Y] / xy[X]);
            break;
         default: break;
      }
      lastOp[0] = op;
      lastKeyWasDigit[0] = false;
   }

   /*@
     @ assignable lastKeyWasDigit[0];
     @ assignable xy[X];
     @ assignable xy[Y];
     @ assignable m;
     @ ensures !lastKeyWasDigit[0];
     @*/
   void mem(byte op) {
      switch(op) {
         case 'S': m = xy[X]; break;
         case 'R': xy[Y] = xy[X]; xy[X] = m; break;
         case 'M': m += xy[X]; break;
      }
      lastKeyWasDigit[0] = false;
   }
}