From 066b132da25cea728cf8844f43223fd415ee7ccb Mon Sep 17 00:00:00 2001
From: Sam Blackshear <shb@fb.com>
Date: Wed, 17 Jun 2015 13:54:17 -0700
Subject: [PATCH] [Infer][Java] Handling assert keyword by adding a special
 case for the $assertionsDisabled field during translation

---
 infer/src/java/jTrans.ml      | 14 ++++++++++----
 infer/src/java/jTransType.ml  |  3 +++
 infer/src/java/jTransType.mli |  3 +++
 3 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml
index 5bb7f64b1..a28f5d958 100644
--- a/infer/src/java/jTrans.ml
+++ b/infer/src/java/jTrans.ml
@@ -577,10 +577,16 @@ let rec expression context pc expr =
         let field_type = (JTransType.get_class_type program tenv (JBasics.make_cn JConfig.string_cl)) in
         JTransStaticField.translate_instr_static_field context callee_procdesc fs field_type loc
       else
-        let sil_expr = Sil.Lfield (sil_expr, field_name, sil_type) in
-        let tmp_id = Ident.create_fresh Ident.knormal in
-        let lderef_instr = Sil.Letderef (tmp_id, sil_expr, sil_type, loc) in
-        (idl @ [tmp_id], instrs @ [lderef_instr], Sil.Var tmp_id)
+        if JTransType.is_autogenerated_assert_field field_name
+        then
+          (* assume that reading from C.$assertionsDisabled always yields "false". this allows *)
+          (* Infer to understand the assert keyword in the expected way *)
+          (idl, instrs, Sil.exp_zero)
+        else
+          let sil_expr = Sil.Lfield (sil_expr, field_name, sil_type) in
+          let tmp_id = Ident.create_fresh Ident.knormal in
+          let lderef_instr = Sil.Letderef (tmp_id, sil_expr, sil_type, loc) in
+          (idl @ [tmp_id], instrs @ [lderef_instr], Sil.Var tmp_id)
 
 let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_code is_static =
   let cfg = JContext.get_cfg context in
diff --git a/infer/src/java/jTransType.ml b/infer/src/java/jTransType.ml
index 728902d2b..246dfec8c 100644
--- a/infer/src/java/jTransType.ml
+++ b/infer/src/java/jTransType.ml
@@ -342,6 +342,9 @@ let get_class_type program tenv cn =
   let t = get_class_type_no_pointer program tenv cn in
   Sil.Tptr (t, Sil.Pk_pointer)
 
+(** return true if [field_name] is the autogenerated C.$assertionsDisabled field for class C *)
+let is_autogenerated_assert_field field_name =
+  string_equal (Ident.java_fieldname_get_field field_name) "$assertionsDisabled"
 
 (** translate an object type *)
 let rec object_type program tenv ot =
diff --git a/infer/src/java/jTransType.mli b/infer/src/java/jTransType.mli
index 05e8c60a0..1804d4cfa 100644
--- a/infer/src/java/jTransType.mli
+++ b/infer/src/java/jTransType.mli
@@ -19,6 +19,9 @@ val get_class_type_no_pointer: JClasspath.program -> Sil.tenv -> JBasics.class_n
 (** [get_class_type tenv cn] returns the sil type representation of the class  *)
 val get_class_type : JClasspath.program -> Sil.tenv -> JBasics.class_name -> Sil.typ
 
+(** return true if [field_name] is the autogenerated C.$assertionsDisabled field for class C *)
+val is_autogenerated_assert_field : Ident.fieldname -> bool
+
 (** transforms a Java object type to a Sil type *)
 val object_type : JClasspath.program -> Sil.tenv -> JBasics.object_type -> Sil.typ