[IR] Adding the option of a function prototype to function types

Summary: This will be useful to translate more precisely the type of blocks, including annotations. See next diff.

Reviewed By: geralt-encore

Differential Revision: D64107251

fbshipit-source-id: 6cfa9d56d5e29229f1b3879cf8377b8d5ea28133

infer/src/IR/Tenv.ml

@@ -536,7 +536,7 @@ let rec is_trivially_copyable tenv {Typ.desc} =
       true
   | Tarray {elt} ->
       is_trivially_copyable tenv elt
-  | Tfun | TVar _ ->
+  | Tfun _ | TVar _ ->
       false
 
 

infer/src/IR/Typ.ml

@@ -128,11 +128,14 @@ type type_quals =
 (** types for sil (structured) expressions *)
 type t = {desc: desc; quals: type_quals}
 
+and function_prototype = {params_type: t list; return_type: t}
+[@@deriving compare, equal, yojson_of, sexp, hash, normalize]
+
 and desc =
   | Tint of ikind  (** integer type *)
   | Tfloat of fkind  (** float type *)
   | Tvoid  (** void type *)
-  | Tfun  (** function type *)
+  | Tfun of function_prototype option  (** function type *)
   | Tptr of t * ptr_kind  (** pointer type *)
   | Tstruct of name  (** structured value type name *)
   | TVar of string  (** type variable (ie. C++ template variables) *)
@@ -187,6 +190,12 @@ let rec pp_full pe f typ =
   F.fprintf f "%a%a" (pp_desc pe) typ.desc pp_quals typ
 
 
+and pp_function_prototype pe f prototype =
+  F.fprintf f "[%a] -> %a"
+    (Pp.comma_seq (pp_full pe))
+    prototype.params_type (pp_full pe) prototype.return_type
+
+
 and pp_desc pe f desc =
   match desc with
   | Tstruct tname ->
@@ -199,9 +208,13 @@ and pp_desc pe f desc =
       F.pp_print_string f (fkind_to_string fk)
   | Tvoid ->
       F.pp_print_string f "void"
-  | Tfun ->
-      F.pp_print_string f "_fn_"
-  | Tptr (({desc= Tarray _ | Tfun} as typ), pk) ->
+  | Tfun prototype_opt -> (
+    match prototype_opt with
+    | Some prototype ->
+        F.fprintf f "(_fn_ %a)" (pp_function_prototype pe) prototype
+    | None ->
+        F.pp_print_string f "_fn_" )
+  | Tptr (({desc= Tarray _ | Tfun _} as typ), pk) ->
       F.fprintf f "%a(%s)" (pp_full pe) typ (ptr_kind_string pk |> escape pe)
   | Tptr (typ, pk) ->
       F.fprintf f "%a%s" (pp_full pe) typ (ptr_kind_string pk |> escape pe)
@@ -278,7 +291,7 @@ and equal_desc_ignore_quals d1 d2 =
       equal_ikind ikind1 ikind2
   | Tfloat fkind1, Tfloat fkind2 ->
       equal_fkind fkind1 fkind2
-  | Tvoid, Tvoid | Tfun, Tfun ->
+  | Tvoid, Tvoid | Tfun _, Tfun _ ->
       true
   | Tptr (t1, ptr_kind1), Tptr (t2, ptr_kind2) ->
       equal_ptr_kind ptr_kind1 ptr_kind2 && equal_ignore_quals t1 t2
@@ -318,7 +331,7 @@ let rec strict_compatible_match formal actual =
       equal_ikind ikind1 ikind2
   | Tfloat fkind1, Tfloat fkind2 ->
       equal_fkind fkind1 fkind2
-  | Tvoid, Tvoid | Tfun, Tfun ->
+  | Tvoid, Tvoid | Tfun _, Tfun _ ->
       true
   | Tstruct name1, Tstruct name2 ->
       equal_name name1 name2 || (is_std_function formal && is_cpp_lambda actual)
@@ -822,7 +835,7 @@ let is_void typ = match typ.desc with Tvoid -> true | _ -> false
 
 let is_pointer_to_int typ = match typ.desc with Tptr ({desc= Tint _}, _) -> true | _ -> false
 
-let is_pointer_to_function typ = match typ.desc with Tptr ({desc= Tfun}, _) -> true | _ -> false
+let is_pointer_to_function typ = match typ.desc with Tptr ({desc= Tfun _}, _) -> true | _ -> false
 
 let is_int typ = match typ.desc with Tint _ -> true | _ -> false
 

infer/src/IR/Typ.mli

@@ -73,11 +73,14 @@ val is_volatile : type_quals -> bool
 (** types for sil (structured) expressions *)
 type t = {desc: desc; quals: type_quals}
 
+and function_prototype = {params_type: t list; return_type: t}
+[@@deriving compare, equal, yojson_of, sexp, hash, normalize]
+
 and desc =
   | Tint of ikind  (** integer type *)
   | Tfloat of fkind  (** float type *)
   | Tvoid  (** void type *)
-  | Tfun  (** function type *)
+  | Tfun of function_prototype option  (** function type *)
   | Tptr of t * ptr_kind  (** pointer type *)
   | Tstruct of name  (** structured value type name *)
   | TVar of string  (** type variable (ie. C++ template variables) *)

infer/src/biabduction/Abs.ml

@@ -471,7 +471,7 @@ let mk_rules_for_dll tenv (para : Predicates.hpara_dll) : rule list =
 let typ_get_recursive_flds tenv typ_exp =
   let filter typ ({Struct.typ= t} : Struct.field) =
     match t.desc with
-    | Tstruct _ | Tint _ | Tfloat _ | Tvoid | Tfun | TVar _ ->
+    | Tstruct _ | Tint _ | Tfloat _ | Tvoid | Tfun _ | TVar _ ->
         false
     | Tptr (({desc= Tstruct _} as typ'), _) ->
         Typ.equal typ' typ
@@ -491,7 +491,7 @@ let typ_get_recursive_flds tenv typ_exp =
             "@\ntyp_get_recursive_flds: unexpected %a unknown struct type: %a@\n" Exp.pp typ_exp
             Typ.Name.pp name ;
           [] )
-    | Tint _ | Tvoid | Tfun | Tptr _ | Tfloat _ | Tarray _ | TVar _ ->
+    | Tint _ | Tvoid | Tfun _ | Tptr _ | Tfloat _ | Tarray _ | TVar _ ->
         [] )
   | Exp.Var _ ->
       [] (* type of |-> not known yet *)

infer/src/biabduction/Absarray.ml

@@ -484,7 +484,7 @@ let keep_only_indices tenv (p : Prop.normal Prop.t) (path : StrexpMatch.path) (i
 (** If the type is array, check whether we should do abstraction *)
 let array_typ_can_abstract {Typ.desc} =
   match desc with
-  | Tarray {elt= {desc= Tptr ({desc= Tfun}, _)}} ->
+  | Tarray {elt= {desc= Tptr ({desc= Tfun _}, _)}} ->
       false (* don't abstract arrays of pointers *)
   | _ ->
       true

infer/src/biabduction/Prop.ml

@@ -458,7 +458,7 @@ let rec create_strexp_of_type ~path tenv struct_init_mode (typ : Typ.t) len inst
     else create_fresh_var ()
   in
   match (typ.desc, len) with
-  | (Tint _ | Tfloat _ | Tvoid | Tfun | Tptr _ | TVar _), None ->
+  | (Tint _ | Tfloat _ | Tvoid | Tfun _ | Tptr _ | TVar _), None ->
       Eexp (init_value (), inst)
   | Tstruct name, _ -> (
       if List.exists ~f:(fun (n, _) -> Typ.Name.equal n name) path then
@@ -488,7 +488,7 @@ let rec create_strexp_of_type ~path tenv struct_init_mode (typ : Typ.t) len inst
       Earray (len, [], inst)
   | Tarray _, Some len ->
       Earray (len, [], inst)
-  | (Tint _ | Tfloat _ | Tvoid | Tfun | Tptr _ | TVar _), Some _ ->
+  | (Tint _ | Tfloat _ | Tvoid | Tfun _ | Tptr _ | TVar _), Some _ ->
       assert false
 
 
@@ -546,7 +546,7 @@ let sigma_get_unsigned_exps sigma =
     to [x[2]]. The [typ] argument is used to ensure the soundness of this collapsing. *)
 let exp_collapse_consecutive_indices_prop (typ : Typ.t) exp =
   let typ_is_base (typ1 : Typ.t) =
-    match typ1.desc with Tint _ | Tfloat _ | Tstruct _ | Tvoid | Tfun -> true | _ -> false
+    match typ1.desc with Tint _ | Tfloat _ | Tstruct _ | Tvoid | Tfun _ -> true | _ -> false
   in
   let typ_is_one_step_from_base =
     match typ.desc with Tptr (t, _) | Tarray {elt= t} -> typ_is_base t | _ -> false

infer/src/biabduction/Rearrange.ml

@@ -158,10 +158,10 @@ let rec create_struct_values analysis_data pname tenv orig_prop footprint_part k
             (Predicates.Aeq (e, e') :: atoms', se, res_t)
         | Predicates.Off_fld _ :: _ ->
             assert false )
-    | Tint _, [] | Tfloat _, [] | Tvoid, [] | Tfun, [] | Tptr _, [] | TVar _, [] ->
+    | Tint _, [] | Tfloat _, [] | Tvoid, [] | Tfun _, [] | Tptr _, [] | TVar _, [] ->
         let id = new_id () in
         ([], Predicates.Eexp (Exp.Var id, inst), t)
-    | (Tint _ | Tfloat _ | Tvoid | Tfun | Tptr _ | TVar _), Off_index e :: off' ->
+    | (Tint _ | Tfloat _ | Tvoid | Tfun _ | Tptr _ | TVar _), Off_index e :: off' ->
         (* In this case, we lift t to the t array. *)
         let t', mk_typ_f =
           match t.Typ.desc with
@@ -179,7 +179,7 @@ let rec create_struct_values analysis_data pname tenv orig_prop footprint_part k
         let se = Predicates.Earray (len, [(e', se')], inst) in
         let res_t = mk_typ_f (Tarray {elt= res_t'; length= None; stride= None}) in
         (Predicates.Aeq (e, e') :: atoms', se, res_t)
-    | Tint _, _ | Tfloat _, _ | Tvoid, _ | Tfun, _ | Tptr _, _ | TVar _, _ ->
+    | Tint _, _ | Tfloat _, _ | Tvoid, _ | Tfun _, _ | Tptr _, _ | TVar _, _ ->
         fail t off __POS__
   in
   if Config.biabduction_trace_rearrange then (
@@ -265,7 +265,7 @@ let rec strexp_extend_values_ analysis_data pname tenv orig_prop footprint_part
         raise (Exceptions.Missing_fld (f, __POS__)) )
   | Off_fld _ :: _, _, _ ->
       raise (Exceptions.Bad_footprint __POS__)
-  | Off_index _ :: _, Predicates.Eexp _, (Tint _ | Tfloat _ | Tvoid | Tfun | Tptr _)
+  | Off_index _ :: _, Predicates.Eexp _, (Tint _ | Tfloat _ | Tvoid | Tfun _ | Tptr _)
   | Off_index _ :: _, Predicates.Estruct _, Tstruct _ ->
       (* L.d_strln ~color:Orange "turn into an array"; *)
       let len =
@@ -492,14 +492,14 @@ let mk_ptsto_exp_footprint analysis_data pname tenv orig_prop (lexp, typ) max_st
   in
   let create_ptsto footprint_part off0 =
     match (root, off0, typ.Typ.desc) with
-    | Exp.Lvar pvar, [], Typ.Tfun ->
+    | Exp.Lvar pvar, [], Typ.Tfun _ ->
         let fun_name = Procname.from_string_c_fun (Mangled.to_string (Pvar.get_name pvar)) in
         let fun_exp = Exp.Const (Const.Cfun fun_name) in
         ( []
         , Prop.mk_ptsto tenv root
             (Predicates.Eexp (fun_exp, inst))
             (Exp.Sizeof {typ; nbytes= None; dynamic_length= None; subtype; nullable= false}) )
-    | _, [], Typ.Tfun ->
+    | _, [], Typ.Tfun _ ->
         let atoms, se, typ =
           create_struct_values analysis_data pname tenv orig_prop footprint_part Ident.kfootprint
             max_stamp typ off0 inst

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -603,11 +603,11 @@ module Val = struct
       | Tint (IBool | IChar | ISChar | IUChar | IUShort) ->
           let v = itv_val ~non_int:is_java in
           if is_java then set_itv_updated_by_unknown v else set_itv_updated_by_addition v
-      | Tfloat _ | Tfun | TVar _ ->
+      | Tfloat _ | Tfun _ | TVar _ ->
           itv_val ~non_int:true |> set_itv_updated_by_unknown
       | Tint _ | Tvoid ->
           itv_val ~non_int:false |> set_itv_updated_by_addition
-      | Tptr ({desc= Tfun}, _) ->
+      | Tptr ({desc= Tfun _}, _) ->
           of_func_ptrs (FuncPtr.Set.of_path path)
       | Tptr ({desc= Tstruct name}, _)
         when PatternMatch.is_subtype tenv name StdTyp.Name.Objc.ns_enumerator ->

infer/src/clang/CType.ml

@@ -17,7 +17,7 @@ let objc_classname_of_desc desc =
   match (desc : Typ.desc) with
   | Tstruct name ->
       name
-  | Tfun ->
+  | Tfun _ ->
       Typ.Name.Objc.from_string CFrontend_config.objc_object
   | _ ->
       L.(debug Capture Verbose)

infer/src/clang/cTrans.ml

@@ -283,7 +283,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
     let call_instr =
       match function_sil with
       | Exp.Var _ ->
-          let closure_param = (function_sil, Typ.mk Typ.Tfun) in
+          let closure_param = (function_sil, Typ.mk (Typ.Tfun None)) in
           let builtin =
             if call_flags.CallFlags.cf_is_objc_block then BuiltinDecl.__call_objc_block
             else BuiltinDecl.__call_c_function_ptr
@@ -816,7 +816,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
                 IntLit.gt n (IntLit.of_int Config.clang_compound_literal_init_limit)
             | Tint _ | Tfloat _ | Tptr _ ->
                 false
-            | Tfun | Tvoid | Tarray _ | TVar _ ->
+            | Tfun _ | Tvoid | Tarray _ | TVar _ ->
                 true
           in
           if init_with_builtin then
@@ -857,7 +857,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
                 let zero_exp = Exp.zero_of_type_exn typ in
                 let instrs = [Sil.Store {e1= exp; typ; e2= zero_exp; loc= sil_loc}] in
                 mk_trans_result (exp, typ) {empty_control with instrs}
-            | Tfun | Tvoid | Tarray _ | TVar _ ->
+            | Tfun _ | Tvoid | Tarray _ | TVar _ ->
                 CFrontend_errors.unimplemented __POS__ stmt_info.Clang_ast_t.si_source_range
                   "fill_typ_with_zero on type %a" (Typ.pp Pp.text) typ
         in

infer/src/clang/cType_to_sil_type.ml

@@ -186,7 +186,7 @@ and type_desc_of_c_type ?attr_info translate_decl tenv c_type : Typ.desc =
   | ConstantArrayType (_, {arti_element_type; arti_stride}, n) ->
       build_array_type ?attr_info translate_decl tenv arti_element_type (Some n) arti_stride
   | FunctionProtoType _ | FunctionNoProtoType _ ->
-      Typ.Tfun
+      Typ.Tfun None
   | ParenType (_, qual_type) ->
       (qual_type_to_sil_type ?attr_info translate_decl tenv qual_type).Typ.desc
   | DecayedType (_, qual_type) ->

infer/src/cost/ConfigImpactAnalysis.ml

@@ -800,7 +800,7 @@ module Dom = struct
       | Tptr ({desc= Tstruct name}, _) ->
           let s = Typ.Name.name name in
           List.exists number_types ~f:(String.equal s)
-      | Tvoid | Tfun | TVar _ | Tarray _ | Tstruct _ | Tptr _ ->
+      | Tvoid | Tfun _ | TVar _ | Tarray _ | Tstruct _ | Tptr _ ->
           false
 
 

infer/src/integration/CaptureSILJson.ml

@@ -353,7 +353,7 @@ and parse_sil_type_name (json : Safe.t) : Typ.t =
     let tn = parse_typename (member "type_name" json) in
     Typ.mk (Typ.TVar (Typ.Name.name tn))
   else if String.equal type_kind "Tvoid" then StdTyp.void
-  else if String.equal type_kind "Tfun" then Typ.mk Tfun
+  else if String.equal type_kind "Tfun" then Typ.mk (Tfun None)
   else if String.equal type_kind "Tenum" then
     (* Sil.Tenum (parse_list (parse_pair (fun n -> Mangled.from_string (to_string n)) parse_constant) value) *)
     Logging.die InternalError "Enums are not supported yet"

infer/src/pulse/PulseAbductiveDomain.ml

@@ -1416,7 +1416,7 @@ let rec fold_pointer_targets tenv timestamp src typ location ?(fields_prefix = R
               fold_pointer_targets tenv timestamp
                 (`Malloc (field_addr, history))
                 field_typ location ~fields_prefix:fields astate ~f ~filter_name ~filter_struct ) )
-  | Tarray _ | Tvoid | Tfun | TVar _ ->
+  | Tarray _ | Tvoid | Tfun _ | TVar _ ->
       (* We ignore tricky types to mark uninitialized addresses. *)
       astate
 

infer/src/pulse/PulseNonDisjunctiveOperations.ml

@@ -184,7 +184,7 @@ let rec get_fixed_size integer_widths tenv name =
                 Some (match fkind with FFloat -> 32 | FDouble -> 64 | FLongDouble -> 128)
             | Tstruct name ->
                 get_fixed_size integer_widths tenv name
-            | Tvoid | Tfun | Tptr _ | TVar _ | Tarray _ ->
+            | Tvoid | Tfun _ | Tptr _ | TVar _ | Tarray _ ->
                 None
           in
           acc + size )

infer/src/textual/TextualSil.ml

@@ -240,7 +240,7 @@ module TypBridge = struct
         Float
     | Tvoid ->
         Void
-    | Tfun ->
+    | Tfun _ ->
         L.die InternalError "Textual conversion: Tfun type does not appear in Java"
     | Tptr (t, Pk_pointer) ->
         Ptr (of_sil t)

infer/src/unit/addressTakenTests.ml

@@ -14,7 +14,7 @@ let tests =
   let assert_empty = invariant "{ }" in
   let int_typ = Typ.mk (Tint IInt) in
   let int_ptr_typ = Typ.mk (Tptr (int_typ, Pk_pointer)) in
-  let fun_ptr_typ = Typ.mk (Tptr (Typ.mk Tfun, Pk_pointer)) in
+  let fun_ptr_typ = Typ.mk (Tptr (Typ.mk (Tfun None), Pk_pointer)) in
   let closure_exp captureds =
     let mk_captured_var str =
       ( Exp.Var (ident_of_str str)

infer/src/unit/livenessTests.ml

@@ -14,7 +14,7 @@ let tests =
   let open OUnit2 in
   let open AnalyzerTester.StructuredSil in
   let assert_empty = invariant "normal:{ }" in
-  let fun_ptr_typ = Typ.mk (Tptr (Typ.mk Tfun, Pk_pointer)) in
+  let fun_ptr_typ = Typ.mk (Tptr (Typ.mk (Tfun None), Pk_pointer)) in
   let closure_exp captured_pvars =
     let mk_captured_var str =
       ( Exp.Var (ident_of_str str)