From 1f605d3b964885f9d64770b05de8787c5ef9ad62 Mon Sep 17 00:00:00 2001
From: John Toman <jtoman@cs.washington.edu>
Date: Thu, 30 Aug 2018 15:40:28 -0700
Subject: [PATCH] Fix get/setShort for field and array reflection

---
 src/main/gov/nasa/jpf/vm/MJIEnv.java          |  6 ++++--
 .../jpf/vm/JPF_java_lang_reflect_Array.java   |  2 +-
 .../jpf/test/java/lang/reflect/FieldTest.java | 19 +++++++++++++++++++
 3 files changed, 24 insertions(+), 3 deletions(-)

diff --git a/src/main/gov/nasa/jpf/vm/MJIEnv.java b/src/main/gov/nasa/jpf/vm/MJIEnv.java
index 2bac12a..a37a941 100644
--- a/src/main/gov/nasa/jpf/vm/MJIEnv.java
+++ b/src/main/gov/nasa/jpf/vm/MJIEnv.java
@@ -562,11 +562,13 @@ public class MJIEnv {
   }
 
   public void setShortField (int objref, String fname, short val) {
-    setIntField(objref, fname, /*(int)*/ val);
+    ElementInfo ei = heap.getModifiable(objref);
+    ei.setShortField(fname, val);
   }
 
   public short getShortField (int objref, String fname) {
-    return (short) getIntField(objref, fname);
+    ElementInfo ei = heap.get(objref);
+    return ei.getShortField(fname);
   }
 
   /**
diff --git a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Array.java b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Array.java
index 8dfa035..325dcb7 100644
--- a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Array.java
+++ b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Array.java
@@ -111,7 +111,7 @@ public class JPF_java_lang_reflect_Array extends NativePeer {
   @MJI
   public int get__Ljava_lang_Object_2I__Ljava_lang_Object_2 (MJIEnv env, int clsRef,
                                                                     int aref, int index){
-    String at = env.getArrayType(aref);
+    String at = Types.getTypeName(env.getArrayType(aref));
     if (at.equals("int")){
       int vref = env.newObject("java.lang.Integer");
       env.setIntField(vref, "value", env.getIntArrayElement(aref,index));
diff --git a/src/tests/gov/nasa/jpf/test/java/lang/reflect/FieldTest.java b/src/tests/gov/nasa/jpf/test/java/lang/reflect/FieldTest.java
index ed29c71..48e863d 100644
--- a/src/tests/gov/nasa/jpf/test/java/lang/reflect/FieldTest.java
+++ b/src/tests/gov/nasa/jpf/test/java/lang/reflect/FieldTest.java
@@ -22,6 +22,7 @@ import gov.nasa.jpf.util.test.TestJPF;
 import java.lang.annotation.Inherited;
 import java.lang.annotation.Retention;
 import java.lang.annotation.RetentionPolicy;
+import java.lang.reflect.Array;
 import java.lang.reflect.Field;
 
 import org.junit.Test;
@@ -96,6 +97,10 @@ public class FieldTest extends TestJPF {
   public class Sub {
     public int f;
   }
+  
+  public static class ShortField {
+    short f;
+  }
 
   @Test
   public void getDeclaredAnnotationsTest () throws SecurityException, NoSuchFieldException{
@@ -106,4 +111,18 @@ public class FieldTest extends TestJPF {
       assertEquals(f2.getDeclaredAnnotations().length, 1);
     }
   }
+  
+  @Test
+  public void getSetShortFieldTest() throws NoSuchFieldException, SecurityException, IllegalArgumentException, IllegalAccessException {
+    if(verifyNoPropertyViolation()) {
+      ShortField sf = new ShortField();
+      Field f = sf.getClass().getField("f");
+      f.set(sf, (short)3);
+      assertEquals((short)f.get(sf), (short)3);
+      
+      short[] x = new short[] {1,2,3};
+      Array.setShort(x, 0, (short) 3);
+      assertEquals(Array.getShort(x, 0), (short)3);
+    }
+  }
 }
-- 
2.34.1