Merge pull request #1008 from GaloisInc/jvm-byte-char

Support byte/char/short in JVM verification commands.
GaloisInc · Jan 15, 2021 · 6789b1a · 6789b1a
2 parents b0cd28d + 8aa4f53
commit 6789b1a
Show file tree

Hide file tree

Showing 7 changed files with 158 additions and 13 deletions.
diff --git a/intTests/test_jvm_small_types/Makefile b/intTests/test_jvm_small_types/Makefile
@@ -0,0 +1,2 @@
+%.class: %.java
+	javac -g $<
diff --git a/intTests/test_jvm_small_types/Test.class b/intTests/test_jvm_small_types/Test.class
diff --git a/intTests/test_jvm_small_types/Test.java b/intTests/test_jvm_small_types/Test.java
@@ -0,0 +1,28 @@
+class Test
+{
+    public static boolean addBoolean(boolean x, boolean y) {
+        return x != y;
+    }
+    public static byte addByte(byte x, byte y) {
+        return (byte) (x + y);
+    }
+    public static char addChar(char x, char y) {
+        return (char) (x + y);
+    }
+    public static short addShort(short x, short y) {
+        return (short) (x + y);
+    }
+
+    public static void updBoolean(boolean []a, boolean x) {
+        a[0] = x;
+    }
+    public static void updByte(byte []a, byte x) {
+        a[0] = x;
+    }
+    public static void updChar(char []a, char x) {
+        a[0] = x;
+    }
+    public static void updShort(short []a, short x) {
+        a[0] = x;
+    }
+}
diff --git a/intTests/test_jvm_small_types/test.saw b/intTests/test_jvm_small_types/test.saw
@@ -0,0 +1,106 @@
+enable_experimental;
+c <- java_load_class "Test";
+
+jvm_verify c "addBoolean" [] false
+  do {
+    x <- jvm_fresh_var "x" java_bool;
+    y <- jvm_fresh_var "y" java_bool;
+    jvm_execute_func [jvm_term x, jvm_term y];
+    jvm_return (jvm_term {{ x ^ y }});
+  }
+  do {
+    check_goal;
+    z3;
+  };
+
+jvm_verify c "addByte" [] false
+  do {
+    x <- jvm_fresh_var "x" java_byte;
+    y <- jvm_fresh_var "y" java_byte;
+    jvm_execute_func [jvm_term x, jvm_term y];
+    jvm_return (jvm_term {{ x + y }});
+  }
+  do {
+    check_goal;
+    z3;
+  };
+
+jvm_verify c "addChar" [] false
+  do {
+    x <- jvm_fresh_var "x" java_char;
+    y <- jvm_fresh_var "y" java_char;
+    jvm_execute_func [jvm_term x, jvm_term y];
+    jvm_return (jvm_term {{ x + y }});
+  }
+  do {
+    check_goal;
+    z3;
+  };
+
+jvm_verify c "addShort" [] false
+  do {
+    x <- jvm_fresh_var "x" java_short;
+    y <- jvm_fresh_var "y" java_short;
+    jvm_execute_func [jvm_term x, jvm_term y];
+    jvm_return (jvm_term {{ x + y }});
+  }
+  do {
+    check_goal;
+    z3;
+  };
+
+jvm_verify c "updBoolean" [] false
+  do {
+    a <- jvm_fresh_var "x" (java_array 4 java_bool);
+    x <- jvm_fresh_var "x" java_bool;
+    aref <- jvm_alloc_array 4 java_bool;
+    jvm_array_is aref a;
+    jvm_execute_func [aref, jvm_term x];
+    jvm_array_is aref {{ update a 0x0 x }};
+  }
+  do {
+    check_goal;
+    z3;
+  };
+
+jvm_verify c "updByte" [] false
+  do {
+    a <- jvm_fresh_var "x" (java_array 4 java_byte);
+    x <- jvm_fresh_var "x" java_byte;
+    aref <- jvm_alloc_array 4 java_byte;
+    jvm_array_is aref a;
+    jvm_execute_func [aref, jvm_term x];
+    jvm_array_is aref {{ update a 0x0 x }};
+  }
+  do {
+    check_goal;
+    z3;
+  };
+
+jvm_verify c "updChar" [] false
+  do {
+    a <- jvm_fresh_var "x" (java_array 4 java_char);
+    x <- jvm_fresh_var "x" java_char;
+    aref <- jvm_alloc_array 4 java_char;
+    jvm_array_is aref a;
+    jvm_execute_func [aref, jvm_term x];
+    jvm_array_is aref {{ update a 0x0 x }};
+  }
+  do {
+    check_goal;
+    z3;
+  };
+
+jvm_verify c "updShort" [] false
+  do {
+    a <- jvm_fresh_var "x" (java_array 4 java_short);
+    x <- jvm_fresh_var "x" java_short;
+    aref <- jvm_alloc_array 4 java_short;
+    jvm_array_is aref a;
+    jvm_execute_func [aref, jvm_term x];
+    jvm_array_is aref {{ update a 0x0 x }};
+  }
+  do {
+    check_goal;
+    z3;
+  };
diff --git a/intTests/test_jvm_small_types/test.sh b/intTests/test_jvm_small_types/test.sh
@@ -0,0 +1 @@
+$SAW test.saw
diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs
@@ -590,15 +590,20 @@ valueToSC sym _ _ Cryptol.TVBit (IVal x) =
       -- TODO: assert that x is 0 or 1
      liftIO (CrucibleSAW.toSC sym b)
 
-valueToSC sym _ _ (Cryptol.TVSeq _n Cryptol.TVBit) (IVal x) =
+valueToSC sym _ _ (Cryptol.TVSeq 8 Cryptol.TVBit) (IVal x) =
+  liftIO (CrucibleSAW.toSC sym =<< W4.bvTrunc sym (W4.knownNat @8) x)
+
+valueToSC sym _ _ (Cryptol.TVSeq 16 Cryptol.TVBit) (IVal x) =
+  liftIO (CrucibleSAW.toSC sym =<< W4.bvTrunc sym (W4.knownNat @16) x)
+
+valueToSC sym _ _ (Cryptol.TVSeq 32 Cryptol.TVBit) (IVal x) =
   liftIO (CrucibleSAW.toSC sym x)
 
-valueToSC sym _ _ (Cryptol.TVSeq _n Cryptol.TVBit) (LVal x) =
+valueToSC sym _ _ (Cryptol.TVSeq 64 Cryptol.TVBit) (LVal x) =
   liftIO (CrucibleSAW.toSC sym x)
 
 valueToSC _sym loc failMsg _tval _val =
   failure loc failMsg
--- TODO: check sizes on bitvectors, support bool, char, and short types
 
 ------------------------------------------------------------------------
 
@@ -966,10 +971,10 @@ injectJVMVal sym jv =
 projectJVMVal :: Sym -> J.Type -> String -> Crucible.RegValue Sym CJ.JVMValueType -> IO JVMVal
 projectJVMVal sym ty msg' v =
   case ty of
-    J.BooleanType -> err -- FIXME
-    J.ByteType    -> err -- FIXME
-    J.CharType    -> err -- FIXME
-    J.ShortType   -> err -- FIXME
+    J.BooleanType -> IVal <$> proj v CJ.tagI
+    J.ByteType    -> IVal <$> proj v CJ.tagI
+    J.CharType    -> IVal <$> proj v CJ.tagI
+    J.ShortType   -> IVal <$> proj v CJ.tagI
     J.IntType     -> IVal <$> proj v CJ.tagI
     J.LongType    -> LVal <$> proj v CJ.tagL
     J.FloatType   -> err -- FIXME
@@ -991,9 +996,9 @@ decodeJVMVal :: J.Type -> Crucible.AnyValue Sym -> Maybe JVMVal
 decodeJVMVal ty v =
   case ty of
     J.BooleanType -> go v CJ.intRepr IVal
-    J.ByteType    -> Nothing -- FIXME
-    J.CharType    -> Nothing -- FIXME
-    J.ShortType   -> Nothing -- FIXME
+    J.ByteType    -> go v CJ.intRepr IVal
+    J.CharType    -> go v CJ.intRepr IVal
+    J.ShortType   -> go v CJ.intRepr IVal
     J.IntType     -> go @CJ.JVMIntType v CJ.intRepr IVal
     J.LongType    -> go @CJ.JVMLongType v CJ.longRepr LVal
     J.FloatType   -> Nothing -- FIXME

diff --git a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs
@@ -9,6 +9,7 @@ Stability   : provisional
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}
 
 module SAWScript.Crucible.JVM.ResolveSetupValue
@@ -218,8 +219,10 @@ resolveSAWTerm cc tp tm =
       fail "resolveSAWTerm: unimplemented type Rational (FIXME)"
     Cryptol.TVSeq sz Cryptol.TVBit ->
       case sz of
-        8  -> fail "resolveSAWTerm: unimplemented type char (FIXME)"
-        16 -> fail "resolveSAWTerm: unimplemented type short (FIXME)"
+        8  -> do x <- resolveBitvectorTerm sym (W4.knownNat @8) tm
+                 IVal <$> W4.bvSext sym W4.knownNat x
+        16 -> do x <- resolveBitvectorTerm sym (W4.knownNat @16) tm
+                 IVal <$> W4.bvSext sym W4.knownNat x
         32 -> IVal <$> resolveBitvectorTerm sym W4.knownNat tm
         64 -> LVal <$> resolveBitvectorTerm sym W4.knownNat tm
         _  -> fail ("Invalid bitvector width: " ++ show sz)
@@ -288,7 +291,7 @@ toJVMType tp =
     Cryptol.TVRational -> Nothing
     Cryptol.TVSeq n Cryptol.TVBit ->
       case n of
-        8  -> Just J.CharType
+        8  -> Just J.ByteType
         16 -> Just J.ShortType
         32 -> Just J.IntType
         64 -> Just J.LongType