[infer] Get widths of build-in integer types

Summary:
It gets built-in integer type widths of C from the clang plugin. For Java, it uses fixed widths.

The controller you requested could not be found.: facebook-clang-plugins

Reviewed By: jvillard

Differential Revision: D10397409

fbshipit-source-id: 73958742e

infer/src/IR/SourceFiles.ml

@@ -12,7 +12,7 @@ let store_statement =
   ResultsDatabase.register_statement
     {|
   INSERT OR REPLACE INTO source_files
-  VALUES (:source, :tenv, :proc_names, :freshly_captured) |}
+  VALUES (:source, :tenv, :integer_type_widths, :proc_names, :freshly_captured) |}
 
 
 let select_existing_statement =
@@ -34,7 +34,7 @@ let get_existing_data source_file =
           (tenv, proc_names) ) )
 
 
-let add source_file cfg tenv =
+let add source_file cfg tenv integer_type_widths =
   Cfg.inline_java_synthetic_methods cfg ;
   let tenv, proc_names =
     (* The same source file may get captured several times in a single capture event, for instance
@@ -73,11 +73,15 @@ let add source_file cfg tenv =
       Tenv.SQLite.serialize tenv |> Sqlite3.bind store_stmt 2
       (* :tenv *)
       |> SqliteUtils.check_result_code db ~log:"store bind type environment" ;
-      Typ.Procname.SQLiteList.serialize proc_names
+      Typ.IntegerWidths.SQLite.serialize integer_type_widths
       |> Sqlite3.bind store_stmt 3
+      (* :integer_type_widths *)
+      |> SqliteUtils.check_result_code db ~log:"store bind integer type widths" ;
+      Typ.Procname.SQLiteList.serialize proc_names
+      |> Sqlite3.bind store_stmt 4
       (* :proc_names *)
       |> SqliteUtils.check_result_code db ~log:"store bind proc names" ;
-      Sqlite3.bind store_stmt 4 (Sqlite3.Data.INT Int64.one)
+      Sqlite3.bind store_stmt 5 (Sqlite3.Data.INT Int64.one)
       (* :freshly_captured *)
       |> SqliteUtils.check_result_code db ~log:"store freshness" ;
       SqliteUtils.result_unit ~finalize:false ~log:"Cfg.store" db store_stmt )

infer/src/IR/SourceFiles.mli

@@ -7,7 +7,7 @@
 
 open! IStd
 
-val add : SourceFile.t -> Cfg.t -> Tenv.per_file -> unit
+val add : SourceFile.t -> Cfg.t -> Tenv.per_file -> Typ.IntegerWidths.t option -> unit
 (** Add or replace the row corresponding to the source file into the database. *)
 
 val get_all : filter:Filtering.source_files_filter -> unit -> SourceFile.t list

infer/src/IR/Typ.ml

@@ -13,6 +13,30 @@ module Hashtbl = Caml.Hashtbl
 module L = Logging
 module F = Format
 
+module IntegerWidths = struct
+  type t = {char_width: int; short_width: int; int_width: int; long_width: int; longlong_width: int}
+
+  let java = {char_width= 16; short_width= 16; int_width= 32; long_width= 64; longlong_width= 64}
+
+  module SQLite = SqliteUtils.MarshalledNullableData (struct
+    type nonrec t = t
+  end)
+
+  let load_statement =
+    ResultsDatabase.register_statement
+      "SELECT integer_type_widths FROM source_files WHERE source_file = :k"
+
+
+  let load source =
+    ResultsDatabase.with_registered_statement load_statement ~f:(fun db load_stmt ->
+        SourceFile.SQLite.serialize source
+        |> Sqlite3.bind load_stmt 1
+        |> SqliteUtils.check_result_code db ~log:"load bind source file" ;
+        SqliteUtils.result_single_column_option ~finalize:false ~log:"Typ.IntegerWidths.load" db
+          load_stmt
+        |> Option.bind ~f:SQLite.deserialize )
+end
+
 (** Kinds of integers *)
 type ikind =
   | IChar  (** [char] *)

infer/src/IR/Typ.mli

@@ -11,6 +11,18 @@
 open! IStd
 module F = Format
 
+module IntegerWidths : sig
+  type t = {char_width: int; short_width: int; int_width: int; long_width: int; longlong_width: int}
+
+  val java : t
+
+  val load : SourceFile.t -> t option
+
+  module SQLite : sig
+    val serialize : t option -> Sqlite3.Data.t
+  end
+end
+
 (** Kinds of integers *)
 type ikind =
   | IChar  (** [char] *)

infer/src/backend/callbacks.ml

@@ -13,6 +13,7 @@ module F = Format
 type proc_callback_args =
   { get_procs_in_file: Typ.Procname.t -> Typ.Procname.t list
   ; tenv: Tenv.t
+  ; integer_type_widths: Typ.IntegerWidths.t
   ; summary: Summary.t
   ; proc_desc: Procdesc.t
   ; exe_env: Exe_env.t }
@@ -66,6 +67,7 @@ let iterate_procedure_callbacks exe_env summary proc_desc =
     Option.value_map source_file ~default:[] ~f:SourceFiles.proc_names_of_source
   in
   let tenv = Exe_env.get_tenv exe_env proc_name in
+  let integer_type_widths = Exe_env.get_integer_type_widths exe_env proc_name in
   let is_specialized = Procdesc.is_specialized proc_desc in
   List.fold ~init:summary
     ~f:(fun summary {name; dynamic_dispatch; language; callback} ->
@@ -76,7 +78,9 @@ let iterate_procedure_callbacks exe_env summary proc_desc =
               log_begin_event logger ~name ~categories:["backend"]
                 ~arguments:[("proc", `String (Typ.Procname.to_string proc_name))]
                 () )) ;
-        let summary = callback {get_procs_in_file; tenv; summary; proc_desc; exe_env} in
+        let summary =
+          callback {get_procs_in_file; tenv; integer_type_widths; summary; proc_desc; exe_env}
+        in
         PerfEvent.(log (fun logger -> log_end_event logger ())) ;
         summary )
       else summary )

infer/src/backend/callbacks.mli

@@ -12,6 +12,7 @@ open! IStd
 type proc_callback_args =
   { get_procs_in_file: Typ.Procname.t -> Typ.Procname.t list
   ; tenv: Tenv.t
+  ; integer_type_widths: Typ.IntegerWidths.t
   ; summary: Summary.t
   ; proc_desc: Procdesc.t
   ; exe_env: Exe_env.t }

infer/src/backend/exe_env.ml

@@ -14,13 +14,16 @@ open! IStd
 module L = Logging
 
 (** per-file data: type environment and cfg *)
-type file_data = {source: SourceFile.t; mutable tenv: Tenv.t option}
+type file_data =
+  { source: SourceFile.t
+  ; mutable tenv: Tenv.t option
+  ; mutable integer_type_widths: Typ.IntegerWidths.t option }
 
 (** create a new file_data *)
 let new_file_data source =
   (* Do not fill in tenv and cfg as they can be quite large. This makes calls to fork() cheaper
      until we start filling out these fields. *)
-  {source; tenv= None (* Sil.load_tenv_from_file tenv_file *)}
+  {source; tenv= None (* Sil.load_tenv_from_file tenv_file *); integer_type_widths= None}
 
 
 let create_file_data table source =
@@ -63,6 +66,13 @@ let file_data_to_tenv file_data =
   file_data.tenv
 
 
+let file_data_to_integer_type_widths file_data =
+  if is_none file_data.integer_type_widths then
+    file_data.integer_type_widths
+    <- Option.first_some (Typ.IntegerWidths.load file_data.source) (Some Typ.IntegerWidths.java) ;
+  file_data.integer_type_widths
+
+
 let java_global_tenv =
   lazy
     ( match Tenv.load_global () with
@@ -72,27 +82,39 @@ let java_global_tenv =
         tenv )
 
 
-(** return the type environment associated to the procedure *)
-let get_tenv exe_env proc_name =
+let get_column_value ~value_on_java ~file_data_to_value ~column_name exe_env proc_name =
   match proc_name with
   | Typ.Procname.Java _ ->
-      Lazy.force java_global_tenv
+      Lazy.force value_on_java
   | _ -> (
     match get_file_data exe_env proc_name with
     | Some file_data -> (
-      match file_data_to_tenv file_data with
-      | Some tenv ->
-          tenv
+      match file_data_to_value file_data with
+      | Some v ->
+          v
       | None ->
           let loc = State.get_loc_exn () in
           L.(die InternalError)
-            "get_tenv: tenv not found for %a in file '%a' at %a" Typ.Procname.pp proc_name
-            SourceFile.pp loc.Location.file Location.pp loc )
+            "get_column_value: %s not found for %a in file '%a' at %a" column_name Typ.Procname.pp
+            proc_name SourceFile.pp loc.Location.file Location.pp loc )
     | None ->
         let loc = State.get_loc_exn () in
         L.(die InternalError)
-          "get_tenv: file_data not found for %a in file '%a' at %a" Typ.Procname.pp proc_name
-          SourceFile.pp loc.Location.file Location.pp loc )
+          "get_column_value: file_data not found for %a in file '%a' at %a" Typ.Procname.pp
+          proc_name SourceFile.pp loc.Location.file Location.pp loc )
+
+
+(** return the type environment associated to the procedure *)
+let get_tenv =
+  get_column_value ~value_on_java:java_global_tenv ~file_data_to_value:file_data_to_tenv
+    ~column_name:"tenv"
+
+
+(** return the integer type widths associated to the procedure *)
+let get_integer_type_widths =
+  get_column_value
+    ~value_on_java:(lazy Typ.IntegerWidths.java)
+    ~file_data_to_value:file_data_to_integer_type_widths ~column_name:"integer type widths"
 
 
 let mk () = {proc_map= Typ.Procname.Hash.create 17; file_map= SourceFile.Hash.create 1}

infer/src/backend/exe_env.mli

@@ -22,3 +22,6 @@ val mk : unit -> t
 
 val get_tenv : t -> Typ.Procname.t -> Tenv.t
 (** return the type environment associated with the procedure *)
+
+val get_integer_type_widths : t -> Typ.Procname.t -> Typ.IntegerWidths.t
+(** return the integer type widths associated with the procedure *)

infer/src/base/MergeResults.ml

@@ -35,7 +35,7 @@ let merge_source_files_table ~db_file =
   Sqlite3.exec db
     {|
     INSERT OR REPLACE INTO source_files
-    SELECT source_file, type_environment, procedure_names, 1
+    SELECT source_file, type_environment, integer_type_widths, procedure_names, 1
     FROM attached.source_files
 |}
   |> SqliteUtils.check_result_code db

infer/src/base/ResultsDatabase.ml

@@ -27,6 +27,7 @@ let source_files_schema =
   {|CREATE TABLE IF NOT EXISTS source_files
   ( source_file TEXT PRIMARY KEY
   , type_environment BLOB NOT NULL
+  , integer_type_widths BLOB
   , procedure_names BLOB NOT NULL
   , freshly_captured INT NOT NULL )|}
 

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -734,7 +734,7 @@ let get_local_decls proc_desc =
 
 
 let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Summary.t =
- fun {proc_desc; tenv; summary} ->
+ fun {proc_desc; tenv; summary; integer_type_widths= _} ->
   Preanal.do_preanalysis proc_desc tenv ;
   let symbol_table = Itv.SymbolTable.empty () in
   let pdata = ProcData.make proc_desc tenv symbol_table in

infer/src/clang/Capture.ml

@@ -75,7 +75,15 @@ let run_clang_frontend ast_source =
           | _ ->
               assert false
         in
-        {CFrontend_config.source_file; lang}
+        let integer_type_widths =
+          let widths = info.Clang_ast_t.tudi_integer_type_widths in
+          { Typ.IntegerWidths.char_width= widths.itw_char_type
+          ; short_width= widths.itw_short_type
+          ; int_width= widths.itw_int_type
+          ; long_width= widths.itw_long_type
+          ; longlong_width= widths.itw_longlong_type }
+        in
+        {CFrontend_config.source_file; lang; integer_type_widths}
     | _ ->
         assert false
   in

infer/src/clang/cFrontend.ml

@@ -47,6 +47,7 @@ let do_source_file (translation_unit_context : CFrontend_config.translation_unit
   CType_decl.add_predefined_types tenv ;
   init_global_state_capture () ;
   let source_file = translation_unit_context.CFrontend_config.source_file in
+  let integer_type_widths = translation_unit_context.CFrontend_config.integer_type_widths in
   L.(debug Capture Verbose)
     "@\n Start building call/cfg graph for '%a'....@\n" SourceFile.pp source_file ;
   let cfg = compute_icfg translation_unit_context tenv ast in
@@ -55,7 +56,7 @@ let do_source_file (translation_unit_context : CFrontend_config.translation_unit
   (* This part below is a boilerplate in every frontends. *)
   (* This could be moved in the cfg_infer module *)
   NullabilityPreanalysis.analysis cfg tenv ;
-  SourceFiles.add source_file cfg (FileLocal tenv) ;
+  SourceFiles.add source_file cfg (FileLocal tenv) (Some integer_type_widths) ;
   if Config.debug_mode then Tenv.store_debug_file_for_source source_file tenv ;
   if
     Config.debug_mode || Config.testing_mode || Config.frontend_tests

infer/src/clang/cFrontend_config.ml

@@ -36,7 +36,8 @@ let incorrect_assumption position source_range ?ast_node fmt =
   F.kasprintf (fun msg -> raise (IncorrectAssumption {msg; position; source_range; ast_node})) fmt
 
 
-type translation_unit_context = {lang: clang_lang; source_file: SourceFile.t}
+type translation_unit_context =
+  {lang: clang_lang; source_file: SourceFile.t; integer_type_widths: Typ.IntegerWidths.t}
 
 exception Invalid_declaration
 

infer/src/clang/cFrontend_config.mli

@@ -43,7 +43,8 @@ val incorrect_assumption :
 (** Used to mark places in the frontend that incorrectly assume something to be
     impossible. TODO(t21762295) get rid of all instances of this. *)
 
-type translation_unit_context = {lang: clang_lang; source_file: SourceFile.t}
+type translation_unit_context =
+  {lang: clang_lang; source_file: SourceFile.t; integer_type_widths: Typ.IntegerWidths.t}
 
 exception Invalid_declaration
 

infer/src/java/jMain.ml

@@ -20,7 +20,7 @@ let init_global_state source_file =
 
 
 let store_icfg source_file cfg =
-  SourceFiles.add source_file cfg Tenv.Global ;
+  SourceFiles.add source_file cfg Tenv.Global None ;
   if Config.debug_mode || Config.frontend_tests then Dotty.print_icfg_dotty source_file cfg ;
   ()