Refactor SymExec.ModelBuiltins into toplevel module

Summary:public
Move ModelBuiltins out of SymExec.

Reviewed By: cristianoc

Differential Revision: D3102373

fb-gh-sync-id: 7fa8485
fbshipit-source-id: 7fa8485

infer/src/backend/modelBuiltins.mli

@@ -0,0 +1,43 @@
+(*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+(** Models for the builtin functions supported *)
+
+val __assert_fail : Procname.t
+val __delete : Procname.t
+val __delete_array : Procname.t
+val __exit : Procname.t
+val __get_array_size : Procname.t
+val __get_type_of : Procname.t
+val __infer_fail : Procname.t
+val __instanceof : Procname.t (** [__instanceof(val,typ)] implements java's [val instanceof typ] *)
+val __cast : Procname.t (** [__cast(val,typ)] implements java's [typ(val)] *)
+val __placement_delete : Procname.t
+val __placement_new : Procname.t
+val __new : Procname.t
+val __new_array : Procname.t
+val __objc_alloc : Procname.t
+val __objc_alloc_no_fail : Procname.t
+val __set_array_size : Procname.t
+val __unwrap_exception : Procname.t
+val __set_file_attribute : Procname.t
+val __set_mem_attribute : Procname.t
+val __set_locked_attribute : Procname.t
+val __set_unlocked_attribute : Procname.t
+val __infer_assume : Procname.t
+val __objc_retain : Procname.t
+val __objc_release : Procname.t
+val __objc_retain_cf : Procname.t
+val __objc_release_cf : Procname.t
+val __set_autorelease_attribute : Procname.t
+val __objc_release_autorelease_pool : Procname.t
+val __objc_cast : Procname.t
+val __objc_dictionary_literal : Procname.t
+val __cxx_typeid : Procname.t
+val malloc_no_fail : Procname.t

infer/src/backend/symExec.mli

@@ -10,51 +10,49 @@
 
 (** Symbolic Execution *)
 
-(** Lookup Java types by name. *)
+exception Cannot_convert_string_to_typ of string
+
 val lookup_java_typ_from_string : Tenv.t -> string -> Sil.typ
+(** Lookup Java types by name. May raise [Cannot_convert_string_to_typ]. *)
+
+val resolve_method : Tenv.t -> Typename.t -> Procname.t -> Procname.t
+(** OO method resolution: given a class name and a method name, climb the class hierarchy to find
+    the procname that the method name will actually resolve to at runtime. For example, if we have a
+    procname like Foo.toString() and Foo does not override toString(), we must resolve the call to
+    toString(). We will end up with Super.toString() where Super is some superclass of Foo. *)
+
+val prune_polarity : bool -> Sil.exp -> Prop.normal Prop.t -> Propset.t
+
+val exp_norm_check_arith :
+  Procname.t -> Prop.normal Prop.t -> Sil.exp -> Sil.exp * Prop.normal Prop.t
+(** Normalize an expression and check for arithmetic problems *)
+
+val execute_diverge :
+  Prop.normal Prop.t -> Paths.Path.t -> (Prop.normal Prop.t * Paths.Path.t) list
+
+val sym_exec_generated :
+  bool -> Tenv.t -> Cfg.Procdesc.t -> Sil.instr list ->
+  (Prop.normal Prop.t * Paths.Path.t) list -> (Prop.normal Prop.t * Paths.Path.t) list
+(** Execute generated instructions from a symbolic heap.
+    If errors occur and [mask_errors] is false, just treat as skip.*)
+
+val sym_exe_check_variadic_sentinel :
+  ?fails_on_nil:bool -> int -> int * int -> Builtin.args ->
+  (Prop.normal Prop.t * Paths.Path.t) list
+
+val check_untainted :
+  Sil.exp -> Procname.t -> Procname.t -> Prop.normal Prop.t -> Prop.normal Prop.t
+
+val call_unknown_or_scan :
+  Tenv.t -> bool -> Cfg.Procdesc.t -> Prop.normal Prop.t -> Paths.Path.t -> Ident.t list ->
+  Sil.typ option -> (Sil.exp * Sil.typ) list -> Procname.t -> Location.t ->
+  (Prop.normal Prop.t * Paths.Path.t) list
+
+val sym_exec_call :
+  Cfg.Procdesc.t -> Tenv.t -> Prop.normal Prop.t -> Paths.Path.t -> Ident.t list ->
+  (Sil.exp * Sil.typ) list -> Specs.summary -> Location.t ->
+  (Prop.normal Prop.t * Paths.Path.t) list
 
-(** symbolic execution on the level of sets of propositions *)
 val lifted_sym_exec : (exn -> unit) -> Tenv.t -> Cfg.Procdesc.t ->
   Paths.PathSet.t -> Cfg.Node.t -> Sil.instr list -> Paths.PathSet.t
-
-(** OO method resolution: given a class name and a method name, climb the class hierarchy to find
- * the procname that the method name will actually resolve to at runtime. For example, if we have
- * a procname like Foo.toString() and Foo does not override toString(), we must resolve the call to
- * toString(). We will end up with Super.toString() where Super is some superclass of Foo. *)
-val resolve_method : Tenv.t -> Typename.t -> Procname.t -> Procname.t
-(** {2 Functions for handling builtins } *)
-
-module ModelBuiltins : sig
-  val __assert_fail : Procname.t
-  val __delete : Procname.t
-  val __delete_array : Procname.t
-  val __exit : Procname.t
-  val __get_array_size : Procname.t
-  val __get_type_of : Procname.t
-  val __infer_fail : Procname.t
-  val __instanceof : Procname.t (** [__instanceof(val,typ)] implements java's [val instanceof typ] *)
-  val __cast : Procname.t (** [__cast(val,typ)] implements java's [typ(val)] *)
-  val __placement_delete : Procname.t
-  val __placement_new : Procname.t
-  val __new : Procname.t
-  val __new_array : Procname.t
-  val __objc_alloc : Procname.t
-  val __objc_alloc_no_fail : Procname.t
-  val __set_array_size : Procname.t
-  val __unwrap_exception : Procname.t
-  val __set_file_attribute : Procname.t
-  val __set_mem_attribute : Procname.t
-  val __set_locked_attribute : Procname.t
-  val __set_unlocked_attribute : Procname.t
-  val __infer_assume : Procname.t
-  val __objc_retain : Procname.t
-  val __objc_release : Procname.t
-  val __objc_retain_cf : Procname.t
-  val __objc_release_cf : Procname.t
-  val __set_autorelease_attribute : Procname.t
-  val __objc_release_autorelease_pool : Procname.t
-  val __objc_cast : Procname.t
-  val __objc_dictionary_literal : Procname.t
-  val __cxx_typeid : Procname.t
-  val malloc_no_fail : Procname.t
-end
+(** symbolic execution on the level of sets of propositions *)

infer/src/checkers/dataflow.ml

@@ -51,7 +51,7 @@ let node_throws node (proc_throws : Procname.t -> throws) : throws =
         Throws
     | Sil.Call (_, Sil.Const (Sil.Cfun callee_pn), _, _, _)
       when Builtin.is_registered callee_pn ->
-        if Procname.equal callee_pn SymExec.ModelBuiltins.__cast
+        if Procname.equal callee_pn ModelBuiltins.__cast
         then DontKnow
         else DoesNotThrow
     | Sil.Call (_, Sil.Const (Sil.Cfun callee_pn), _, _, _) ->

infer/src/checkers/repeatedCallsChecker.ml

@@ -67,8 +67,8 @@ struct
     let node_allocates node : Location.t option =
       let found = ref None in
       let proc_is_new pn =
-        Procname.equal pn SymExec.ModelBuiltins.__new ||
-        Procname.equal pn SymExec.ModelBuiltins.__new_array in
+        Procname.equal pn ModelBuiltins.__new ||
+        Procname.equal pn ModelBuiltins.__new_array in
       let do_instr instr =
         match instr with
         | Sil.Call (_, Sil.Const (Sil.Cfun pn), _, loc, _) when proc_is_new pn ->

infer/src/clang/ast_expressions.ml

@@ -621,6 +621,6 @@ let create_assume_not_null_call decl_info var_name var_type =
   let bin_op_expr_info = make_general_expr_info create_BOOL_type `RValue `Ordinary in
   let bin_op = make_binary_stmt decl_ref_exp_cast null_expr stmt_info bin_op_expr_info boi in
   let parameters = [bin_op] in
-  let procname = Procname.to_string SymExec.ModelBuiltins.__infer_assume in
+  let procname = Procname.to_string ModelBuiltins.__infer_assume in
   let qual_procname = Ast_utils.make_name_decl procname in
   create_call stmt_info var_decl_ptr qual_procname create_void_star_type parameters

infer/src/clang/cArithmetic_trans.ml

@@ -20,9 +20,9 @@ open CFrontend_utils
 (* See document: "Objective-C Automatic Reference Counting" describing the semantics *)
 let assignment_arc_mode e1 typ e2 loc rhs_owning_method is_e1_decl =
   let assign = Sil.Set (e1, typ, e2, loc) in
-  let retain_pname = SymExec.ModelBuiltins.__objc_retain in
-  let release_pname = SymExec.ModelBuiltins.__objc_release in
-  let autorelease_pname = SymExec.ModelBuiltins.__set_autorelease_attribute in
+  let retain_pname = ModelBuiltins.__objc_retain in
+  let release_pname = ModelBuiltins.__objc_release in
+  let autorelease_pname = ModelBuiltins.__set_autorelease_attribute in
   let mk_call procname e t =
     let bi_retain = Sil.Const (Sil.Cfun procname) in
     Sil.Call([], bi_retain, [(e, t)], loc, Sil.cf_default) in

infer/src/clang/cTrans.ml

@@ -79,7 +79,7 @@ struct
     if !Config.arc_mode &&
        not (CTrans_utils.is_owning_name method_name) &&
        ObjcInterface_decl.is_pointer_to_objc_class context.CContext.tenv typ then
-      let fname = SymExec.ModelBuiltins.__set_autorelease_attribute in
+      let fname = ModelBuiltins.__set_autorelease_attribute in
       let ret_id = Ident.create_fresh Ident.knormal in
       let stmt_call =
         Sil.Call ([ret_id], (Sil.Const (Sil.Cfun fname)), [(exp, typ)], sil_loc, Sil.cf_default) in
@@ -463,7 +463,7 @@ struct
       if name = CFrontend_config.malloc &&
          (!CFrontend_config.language = CFrontend_config.OBJC ||
           !CFrontend_config.language = CFrontend_config.OBJCPP) then
-        SymExec.ModelBuiltins.malloc_no_fail
+        ModelBuiltins.malloc_no_fail
       else Procname.from_string_c_fun name in
     let is_builtin = Builtin.is_registered non_mangled_func_name in
     if is_builtin then (* malloc, free, exit, scanf, ... *)
@@ -1937,7 +1937,7 @@ struct
     let typ =
       CTypes_decl.class_from_pointer_type
         trans_state.context.CContext.tenv info.Clang_ast_t.ei_type_ptr in
-    let dictionary_literal_pname = SymExec.ModelBuiltins.__objc_dictionary_literal in
+    let dictionary_literal_pname = ModelBuiltins.__objc_dictionary_literal in
     let dictionary_literal_s = Procname.get_method dictionary_literal_pname in
     let obj_c_message_expr_info =
       Ast_expressions.make_obj_c_message_expr_info_class dictionary_literal_s typ None in
@@ -1964,7 +1964,7 @@ struct
       then those objects are released and the autorelease flag is removed. *)
   and objcAutoreleasePool_trans trans_state stmt_info stmts =
     let sil_loc = CLocation.get_sil_location stmt_info trans_state.context in
-    let fname = SymExec.ModelBuiltins.__objc_release_autorelease_pool in
+    let fname = ModelBuiltins.__objc_release_autorelease_pool in
     let ret_id = Ident.create_fresh Ident.knormal in
     let autorelease_pool_vars = CVar_decl.compute_autorelease_pool_vars trans_state.context stmts in
     let stmt_call =
@@ -2065,8 +2065,8 @@ struct
     let sil_loc = CLocation.get_sil_location stmt_info context in
     let is_array = delete_expr_info.Clang_ast_t.xdei_is_array in
     let fname =
-      if is_array then SymExec.ModelBuiltins.__delete_array
-      else SymExec.ModelBuiltins.__delete in
+      if is_array then ModelBuiltins.__delete_array
+      else ModelBuiltins.__delete in
     let param = match stmt_list with [p] -> p | _ -> assert false in
     let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in
     let trans_state_param = { trans_state_pri with succ_nodes = [] } in
@@ -2121,7 +2121,7 @@ struct
     let sizeof_expr = match cast_type with
       | Sil.Tptr (typ, _) -> Sil.Sizeof (typ, subtypes)
       | _ -> assert false in
-    let builtin = Sil.Const (Sil.Cfun SymExec.ModelBuiltins.__cast) in
+    let builtin = Sil.Const (Sil.Cfun ModelBuiltins.__cast) in
     let stmt = match stmts with [stmt] -> stmt | _ -> assert false in
     let res_trans_stmt = exec_with_glvalue_as_reference instruction trans_state' stmt in
     let exp = match res_trans_stmt.exps with | [e] -> e | _ -> assert false in
@@ -2175,7 +2175,7 @@ struct
           let trans_state_param = { trans_state_pri with succ_nodes = [] } in
           instruction trans_state_param stmt
       | _ -> empty_res_trans in
-    let fun_name = SymExec.ModelBuiltins.__cxx_typeid in
+    let fun_name = ModelBuiltins.__cxx_typeid in
     let sil_fun = Sil.Const (Sil.Cfun fun_name) in
     let ret_id = Ident.create_fresh Ident.knormal in
     let type_info_objc = (Sil.Sizeof (typ, Sil.Subtype.exact), Sil.Tvoid) in

infer/src/clang/cTrans_models.ml

@@ -60,11 +60,11 @@ let is_autorelease_method funct =
 
 let get_builtinname method_name =
   if is_retain_method method_name then
-    Some SymExec.ModelBuiltins.__objc_retain
+    Some ModelBuiltins.__objc_retain
   else if is_autorelease_method method_name then
-    Some SymExec.ModelBuiltins.__set_autorelease_attribute
+    Some ModelBuiltins.__set_autorelease_attribute
   else if is_release_method method_name then
-    Some SymExec.ModelBuiltins.__objc_release
+    Some ModelBuiltins.__objc_release
   else None
 
 let is_modeled_builtin funct =
@@ -103,9 +103,9 @@ let builtin_predefined_model fun_stmt sil_fe =
       (match sil_fe with
        | Sil.Const (Sil.Cfun pn) when Specs.summary_exists pn -> sil_fe, false
        | Sil.Const (Sil.Cfun pn) when is_retain_predefined_model typ (Procname.to_string pn) ->
-           Sil.Const (Sil.Cfun SymExec.ModelBuiltins.__objc_retain_cf) , true
+           Sil.Const (Sil.Cfun ModelBuiltins.__objc_retain_cf) , true
        | Sil.Const (Sil.Cfun pn) when is_release_predefined_model typ (Procname.to_string pn) ->
-           Sil.Const (Sil.Cfun SymExec.ModelBuiltins.__objc_release_cf), true
+           Sil.Const (Sil.Cfun ModelBuiltins.__objc_release_cf), true
        | _ -> sil_fe, false)
   | _ -> sil_fe, false
 
@@ -165,14 +165,14 @@ let get_predefined_ms_nsautoreleasepool_release class_name method_name mk_procna
   let class_type = Ast_expressions.create_class_type (class_name, `OBJC) in
   get_predefined_ms_method condition class_name method_name Procname.Instance_objc_method
     mk_procname lang [(CFrontend_config.self, class_type)] Ast_expressions.create_void_type
-    [] (Some SymExec.ModelBuiltins.__objc_release_autorelease_pool)
+    [] (Some ModelBuiltins.__objc_release_autorelease_pool)
 
 let get_predefined_ms_is_kind_of_class class_name method_name mk_procname lang =
   let condition = method_name = CFrontend_config.is_kind_of_class in
   let class_type = Ast_expressions.create_class_type (class_name, `OBJC) in
   get_predefined_ms_method condition class_name method_name Procname.Instance_objc_method
     mk_procname lang [(CFrontend_config.self, class_type)] Ast_expressions.create_BOOL_type
-    [] (Some SymExec.ModelBuiltins.__instanceof)
+    [] (Some ModelBuiltins.__instanceof)
 
 let get_predefined_model_method_signature class_name method_name mk_procname lang =
   let next_predefined f = function

infer/src/clang/cTrans_utils.ml

@@ -309,9 +309,9 @@ let create_alloc_instrs context sil_loc function_type fname size_exp_opt =
 
 let alloc_trans trans_state loc stmt_info function_type is_cf_non_null_alloc =
   let fname = if is_cf_non_null_alloc then
-      SymExec.ModelBuiltins.__objc_alloc_no_fail
+      ModelBuiltins.__objc_alloc_no_fail
     else
-      SymExec.ModelBuiltins.__objc_alloc in
+      ModelBuiltins.__objc_alloc in
   let (function_type, ret_id, stmt_call, exp) =
     create_alloc_instrs trans_state.context loc function_type fname None in
   let res_trans_tmp = { empty_res_trans with ids =[ret_id]; instrs =[stmt_call]} in
@@ -321,7 +321,7 @@ let alloc_trans trans_state loc stmt_info function_type is_cf_non_null_alloc =
   { res_trans with exps =[(exp, function_type)]}
 
 let objc_new_trans trans_state loc stmt_info cls_name function_type =
-  let fname = SymExec.ModelBuiltins.__objc_alloc_no_fail in
+  let fname = ModelBuiltins.__objc_alloc_no_fail in
   let (alloc_ret_type, alloc_ret_id, alloc_stmt_call, _) =
     create_alloc_instrs trans_state.context loc function_type fname None in
   let init_ret_id = Ident.create_fresh Ident.knormal in
@@ -355,8 +355,8 @@ let new_or_alloc_trans trans_state loc stmt_info type_ptr class_name_opt selecto
 let cpp_new_trans trans_state sil_loc function_type size_exp_opt =
   let fname =
     match size_exp_opt with
-    | Some _ -> SymExec.ModelBuiltins.__new_array
-    | None -> SymExec.ModelBuiltins.__new in
+    | Some _ -> ModelBuiltins.__new_array
+    | None -> ModelBuiltins.__new in
   let (function_type, ret_id, stmt_call, exp) =
     create_alloc_instrs trans_state.context sil_loc function_type fname size_exp_opt  in
   { empty_res_trans with ids = [ret_id]; instrs = [stmt_call]; exps = [(exp, function_type)] }
@@ -366,7 +366,7 @@ let create_cast_instrs context exp cast_from_typ cast_to_typ sil_loc =
   let typ = CTypes.remove_pointer_to_typ cast_to_typ in
   let cast_typ_no_pointer = CTypes.expand_structured_type context.CContext.tenv typ in
   let sizeof_exp = Sil.Sizeof (cast_typ_no_pointer, Sil.Subtype.exact) in
-  let pname = SymExec.ModelBuiltins.__objc_cast in
+  let pname = ModelBuiltins.__objc_cast in
   let args = [(exp, cast_from_typ); (sizeof_exp, Sil.Tint Sil.IULong)] in
   let stmt_call = Sil.Call([ret_id], (Sil.Const (Sil.Cfun pname)), args, sil_loc, Sil.cf_default) in
   (ret_id, stmt_call, Sil.Var ret_id)
@@ -437,7 +437,7 @@ let cast_operation context cast_kind exps cast_typ sil_loc is_objc_bridged =
         ([],[], (exp, exp_typ))
 
 let trans_assertion_failure sil_loc context =
-  let assert_fail_builtin = Sil.Const (Sil.Cfun SymExec.ModelBuiltins.__infer_fail) in
+  let assert_fail_builtin = Sil.Const (Sil.Cfun ModelBuiltins.__infer_fail) in
   let args = [Sil.Const (Sil.Cstr Config.default_failure_name), Sil.Tvoid] in
   let call_instr = Sil.Call ([], assert_fail_builtin, args, sil_loc, Sil.cf_default) in
   let exit_node = Cfg.Procdesc.get_exit_node (CContext.get_procdesc context)

infer/src/eradicate/eradicateChecks.ml

@@ -139,7 +139,7 @@ let check_condition case_zero find_canonical_duplicate curr_pname
       | _ -> false in
     let do_instr = function
       | Sil.Call (_, Sil.Const (Sil.Cfun pn), [_; (Sil.Sizeof(t, _), _)], _, _) when
-          Procname.equal pn SymExec.ModelBuiltins.__instanceof && typ_is_throwable t ->
+          Procname.equal pn ModelBuiltins.__instanceof && typ_is_throwable t ->
           throwable_found := true
       | _ -> () in
     let do_node n =

infer/src/eradicate/typeCheck.ml

@@ -41,7 +41,7 @@ module ComplexExpressions = struct
 
 
   let procname_optional_isPresent = Models.is_optional_isPresent
-  let procname_instanceof = Procname.equal SymExec.ModelBuiltins.__instanceof
+  let procname_instanceof = Procname.equal ModelBuiltins.__instanceof
 
   let procname_is_false_on_null pn =
     match Specs.proc_resolve_attributes pn with
@@ -510,14 +510,14 @@ let typecheck_instr
       check_field_assign ();
       typestate2
   | Sil.Call ([id], Sil.Const (Sil.Cfun pn), [(_, typ)], loc, _)
-    when Procname.equal pn SymExec.ModelBuiltins.__new ||
-         Procname.equal pn SymExec.ModelBuiltins.__new_array ->
+    when Procname.equal pn ModelBuiltins.__new ||
+         Procname.equal pn ModelBuiltins.__new_array ->
       TypeState.add_id
         id
         (typ, TypeAnnotation.const Annotations.Nullable false TypeOrigin.New, [loc])
         typestate (* new never returns null *)
   | Sil.Call ([id], Sil.Const (Sil.Cfun pn), (e, typ):: _, loc, _)
-    when Procname.equal pn SymExec.ModelBuiltins.__cast ->
+    when Procname.equal pn ModelBuiltins.__cast ->
       typecheck_expr_for_errors typestate e loc;
       let e', typestate' =
         convert_complex_exp_to_pvar node false e typestate loc in
@@ -526,7 +526,7 @@ let typecheck_instr
         (typecheck_expr_simple typestate' e' typ TypeOrigin.ONone loc)
         typestate'
   | Sil.Call ([id], Sil.Const (Sil.Cfun pn), [(array_exp, t)], loc, _)
-    when Procname.equal pn SymExec.ModelBuiltins.__get_array_size ->
+    when Procname.equal pn ModelBuiltins.__get_array_size ->
       let (_, ta, _) = typecheck_expr
           find_canonical_duplicate
           calls_this

infer/src/harness/inhabit.ml

@@ -86,11 +86,11 @@ let rec inhabit_typ typ cfg env =
       | Sil.Tptr (Sil.Tarray (inner_typ, Sil.Const (Sil.Cint _)), Sil.Pk_pointer) ->
           let arr_size = Sil.Const (Sil.Cint (Sil.Int.one)) in
           let arr_typ = Sil.Tarray (inner_typ, arr_size) in
-          inhabit_alloc arr_typ typ SymExec.ModelBuiltins.__new_array env
+          inhabit_alloc arr_typ typ ModelBuiltins.__new_array env
       | Sil.Tptr (typ, Sil.Pk_pointer) as ptr_to_typ ->
           (* TODO (t4575417): this case does not work correctly for enums, but they are currently
            * broken in Infer anyway (see t4592290) *)
-          let (allocated_obj_exp, env) = inhabit_alloc typ typ SymExec.ModelBuiltins.__new env in
+          let (allocated_obj_exp, env) = inhabit_alloc typ typ ModelBuiltins.__new env in
           (* select methods that are constructors and won't force us into infinite recursion because
            * we are already inhabiting one of their argument types *)
           let get_all_suitable_constructors typ = match typ with

infer/src/java/jTrans.ml

@@ -395,10 +395,10 @@ let use_static_final_fields context =
   (not !no_static_final) && (JContext.get_meth_kind context) <> JContext.Init
 
 let builtin_new =
-  Sil.Const (Sil.Cfun SymExec.ModelBuiltins.__new)
+  Sil.Const (Sil.Cfun ModelBuiltins.__new)
 
 let builtin_get_array_size =
-  Sil.Const (Sil.Cfun SymExec.ModelBuiltins.__get_array_size)
+  Sil.Const (Sil.Cfun ModelBuiltins.__get_array_size)
 
 let create_sil_deref exp typ loc =
   let fresh_id = Ident.create_fresh Ident.knormal in
@@ -460,8 +460,8 @@ let rec expression context pc expr =
               JTransType.sizeof_of_object_type program tenv ot subtypes in
             let builtin =
               (match unop with
-               | JBir.InstanceOf _ -> Sil.Const (Sil.Cfun SymExec.ModelBuiltins.__instanceof)
-               | JBir.Cast _ -> Sil.Const (Sil.Cfun SymExec.ModelBuiltins.__cast)
+               | JBir.InstanceOf _ -> Sil.Const (Sil.Cfun ModelBuiltins.__instanceof)
+               | JBir.Cast _ -> Sil.Const (Sil.Cfun ModelBuiltins.__cast)
                | _ -> assert false) in
             let args = [(sil_ex, type_of_ex); (sizeof_expr, Sil.Tvoid)] in
             let ret_id = Ident.create_fresh Ident.knormal in
@@ -619,7 +619,7 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
     | (_, typ) as exp :: _
       when Procname.is_constructor callee_procname && JTransType.is_closeable program tenv typ ->
         let set_file_attr =
-          let set_builtin = Sil.Const (Sil.Cfun SymExec.ModelBuiltins.__set_file_attribute) in
+          let set_builtin = Sil.Const (Sil.Cfun ModelBuiltins.__set_file_attribute) in
           Sil.Call ([], set_builtin, [exp], loc, Sil.cf_default) in
         (* Exceptions thrown in the constructor should prevent adding the resource attribute *)
         call_instrs @ [set_file_attr]
@@ -628,7 +628,7 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
     | (_, typ) as exp :: []
       when Procname.java_is_close callee_procname && JTransType.is_closeable program tenv typ ->
         let set_mem_attr =
-          let set_builtin = Sil.Const (Sil.Cfun SymExec.ModelBuiltins.__set_mem_attribute) in
+          let set_builtin = Sil.Const (Sil.Cfun ModelBuiltins.__set_mem_attribute) in
           Sil.Call ([], set_builtin, [exp], loc, Sil.cf_default) in
         (* Exceptions thrown in the close method should not prevent the resource from being *)
         (* considered as closed *)
@@ -766,7 +766,7 @@ let is_this expr =
 
 
 let assume_not_null loc sil_expr =
-  let builtin_infer_assume = Sil.Const (Sil.Cfun SymExec.ModelBuiltins.__infer_assume) in
+  let builtin_infer_assume = Sil.Const (Sil.Cfun ModelBuiltins.__infer_assume) in
   let not_null_expr =
     Sil.BinOp (Sil.Ne, sil_expr, Sil.exp_null) in
   let assume_call_flag = { Sil.cf_default with Sil.cf_noreturn = true; } in
@@ -895,7 +895,7 @@ let rec instruction context pc instr : translation =
         JContext.add_goto_jump context pc JContext.Exit;
         Instr node
     | JBir.New (var, cn, constr_type_list, constr_arg_list) ->
-        let builtin_new = Sil.Const (Sil.Cfun SymExec.ModelBuiltins.__new) in
+        let builtin_new = Sil.Const (Sil.Cfun ModelBuiltins.__new) in
         let class_type = JTransType.get_class_type program tenv cn in
         let class_type_np = JTransType.get_class_type_no_pointer program tenv cn in
         let sizeof_exp = Sil.Sizeof (class_type_np, Sil.Subtype.exact) in
@@ -917,7 +917,7 @@ let rec instruction context pc instr : translation =
         Cg.add_edge cg caller_procname constr_procname;
         Instr node
     | JBir.NewArray (var, vt, expr_list) ->
-        let builtin_new_array = Sil.Const (Sil.Cfun SymExec.ModelBuiltins.__new_array) in
+        let builtin_new_array = Sil.Const (Sil.Cfun ModelBuiltins.__new_array) in
         let content_type = JTransType.value_type program tenv vt in
         let array_type = JTransType.create_array_type content_type (IList.length expr_list) in
         let array_name = JContext.set_pvar context var array_type in
@@ -1089,7 +1089,7 @@ let rec instruction context pc instr : translation =
         and ret_id = Ident.create_fresh Ident.knormal
         and sizeof_expr =
           JTransType.sizeof_of_object_type program tenv object_type Sil.Subtype.subtypes_instof in
-        let check_cast = Sil.Const (Sil.Cfun SymExec.ModelBuiltins.__instanceof) in
+        let check_cast = Sil.Const (Sil.Cfun ModelBuiltins.__instanceof) in
         let args = [(sil_expr, sil_type); (sizeof_expr, Sil.Tvoid)] in
         let call = Sil.Call([ret_id], check_cast, args, loc, Sil.cf_default) in
         let res_ex = Sil.Var ret_id in
@@ -1122,11 +1122,11 @@ let rec instruction context pc instr : translation =
         Prune (is_instance_node, throw_cast_exception_node)
     | JBir.MonitorEnter expr ->
         trans_monitor_enter_exit
-          context expr pc loc SymExec.ModelBuiltins.__set_locked_attribute "MonitorEnter"
+          context expr pc loc ModelBuiltins.__set_locked_attribute "MonitorEnter"
 
     | JBir.MonitorExit expr ->
         trans_monitor_enter_exit
-          context expr pc loc SymExec.ModelBuiltins.__set_unlocked_attribute "MonitorExit"
+          context expr pc loc ModelBuiltins.__set_unlocked_attribute "MonitorExit"
 
     | _ -> Skip
   with Frontend_error s ->

infer/src/java/jTransExn.ml

@@ -39,7 +39,7 @@ let translate_exceptions context exit_nodes get_body_nodes handler_table =
     let id_deactivate = Ident.create_fresh Ident.knormal in
     let instr_deactivate_exn = Sil.Set (Sil.Lvar ret_var, ret_type, Sil.Var id_deactivate, loc) in
     let instr_unwrap_ret_val =
-      let unwrap_builtin = Sil.Const (Sil.Cfun SymExec.ModelBuiltins.__unwrap_exception) in
+      let unwrap_builtin = Sil.Const (Sil.Cfun ModelBuiltins.__unwrap_exception) in
       Sil.Call([id_exn_val], unwrap_builtin, [(Sil.Var id_ret_val, ret_type)], loc, Sil.cf_default) in
     create_node loc Cfg.Node.exn_handler_kind [instr_get_ret_val; instr_deactivate_exn; instr_unwrap_ret_val] [id_ret_val; id_deactivate] in
   let create_entry_block handler_list =
@@ -61,7 +61,7 @@ let translate_exceptions context exit_nodes get_body_nodes handler_table =
           | _ -> assert false in
         let id_instanceof = Ident.create_fresh Ident.knormal in
         let instr_call_instanceof =
-          let instanceof_builtin = Sil.Const (Sil.Cfun SymExec.ModelBuiltins.__instanceof) in
+          let instanceof_builtin = Sil.Const (Sil.Cfun ModelBuiltins.__instanceof) in
           let args = [(Sil.Var id_exn_val, Sil.Tptr(exn_type, Sil.Pk_pointer)); (Sil.Sizeof (exn_type, Sil.Subtype.exact), Sil.Tvoid)] in
           Sil.Call ([id_instanceof], instanceof_builtin, args, loc, Sil.cf_default) in
         let if_kind = Sil.Ik_switch in