From 10afd021a117874bcc20d036b8cdbf699dfa2db3 Mon Sep 17 00:00:00 2001
From: Nikos Gorogiannis <nikosg@fb.com>
Date: Mon, 9 Mar 2020 09:03:00 -0700
Subject: [PATCH] [java] fix primitive types

Summary:
A java byte is not a short and a java character is not a C character. Fix those types by mapping them to what the spec ordains.

An extra advantage is that this establishes a bijection between java types and their project in the `sil` type system, so pretty printing in Java mode can actually be made to work.

Reviewed By: mityal

Differential Revision: D20330525

fbshipit-source-id: 00ac2294b
---
 infer/src/IR/Procname.ml                       | 2 +-
 infer/src/IR/Typ.ml                            | 6 ++++--
 infer/src/IR/Typ.mli                           | 2 ++
 infer/src/bufferoverrun/bufferOverrunDomain.ml | 2 +-
 infer/src/java/jAnnotation.ml                  | 2 +-
 infer/src/java/jTransType.ml                   | 5 +++--
 6 files changed, 12 insertions(+), 7 deletions(-)

diff --git a/infer/src/IR/Procname.ml b/infer/src/IR/Procname.ml
index d6818a6c9..2f5cec21b 100644
--- a/infer/src/IR/Procname.ml
+++ b/infer/src/IR/Procname.ml
@@ -136,7 +136,7 @@ module Java = struct
       | "boolean" ->
           Typ.boolean
       | "char" ->
-          Typ.char
+          Typ.java_char
       | "long" ->
           Typ.long
       | "float" ->
diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml
index 1410f35f9..4d520e17b 100644
--- a/infer/src/IR/Typ.ml
+++ b/infer/src/IR/Typ.ml
@@ -273,9 +273,11 @@ let void = mk Tvoid
 
 let void_star = mk (Tptr (void, Pk_pointer))
 
-let java_byte = mk (Tint IShort)
+let java_char = mk (Tint IUShort)
 
-let java_short = java_byte
+let java_byte = mk (Tint ISChar)
+
+let java_short = mk (Tint IShort)
 
 let boolean = mk (Tint IBool)
 
diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli
index abdaaea31..3a0eb4786 100644
--- a/infer/src/IR/Typ.mli
+++ b/infer/src/IR/Typ.mli
@@ -142,6 +142,8 @@ val mk_ptr : ?ptr_kind:ptr_kind -> t -> t
 val void : t
 (** void type *)
 
+val java_char : t
+
 val java_byte : t
 
 val java_short : t
diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index 58e895b09..0a6e6604a 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -673,7 +673,7 @@ module Val = struct
       else Taint.param_of_path path
     in
     match typ.Typ.desc with
-    | Tint (IBool | IChar | ISChar | IUChar) ->
+    | Tint (IBool | IChar | ISChar | IUChar | IUShort) ->
         let v = itv_val ~non_int:is_java ~taint in
         if Language.curr_language_is Java then set_itv_updated_by_unknown v
         else set_itv_updated_by_addition v
diff --git a/infer/src/java/jAnnotation.ml b/infer/src/java/jAnnotation.ml
index d670f924f..a2667b311 100644
--- a/infer/src/java/jAnnotation.ml
+++ b/infer/src/java/jAnnotation.ml
@@ -15,7 +15,7 @@ let translate_basic_type = function
   | `Byte ->
       Typ.java_byte
   | `Char ->
-      Typ.char
+      Typ.java_char
   | `Double ->
       Typ.double
   | `Float ->
diff --git a/infer/src/java/jTransType.ml b/infer/src/java/jTransType.ml
index ec886fdb0..1a4cb04c5 100644
--- a/infer/src/java/jTransType.ml
+++ b/infer/src/java/jTransType.ml
@@ -15,15 +15,16 @@ module L = Logging
 
 exception Type_tranlsation_error of string
 
+(** https://docs.oracle.com/javase/tutorial/java/nutsandbolts/datatypes.html *)
 let translate_basic_type = function
   | `Int ->
       Typ.int
   | `Bool ->
       Typ.boolean
   | `Byte ->
-      Typ.char
+      Typ.java_byte
   | `Char ->
-      Typ.char
+      Typ.java_char
   | `Double ->
       Typ.double
   | `Float ->