[pulse] model C variadic out-parameters to fix false MEMORY_LEAK_C

infer/src/IR/Specialization.ml

@@ -59,13 +59,24 @@ module Pulse = struct
         F.fprintf fmt "}" )
   end
 
-  type t = {aliases: Aliases.t option; dynamic_types: DynamicTypes.t}
+  module VariadicActuals = struct
+    (* the caller's extra (variadic) actual arguments, in order, as heap paths, used to
+       specialize a C variadic callee so that its `va_arg` reads connect to them *)
+    type t = HeapPath.t list [@@deriving equal, compare, hash, sexp, yojson_of]
+
+    let pp fmt actuals =
+      if not (List.is_empty actuals) then
+        F.fprintf fmt "variadic_actuals: [%a] " (Pp.seq ~sep:"; " HeapPath.pp) actuals
+  end
+
+  type t =
+    {aliases: Aliases.t option; dynamic_types: DynamicTypes.t; variadic_actuals: VariadicActuals.t}
   [@@deriving equal, compare, hash, sexp, yojson_of]
 
-  let bottom = {aliases= None; dynamic_types= HeapPath.Map.empty}
+  let bottom = {aliases= None; dynamic_types= HeapPath.Map.empty; variadic_actuals= []}
 
-  let is_bottom {aliases; dynamic_types} =
-    Option.is_none aliases && HeapPath.Map.is_empty dynamic_types
+  let is_bottom {aliases; dynamic_types; variadic_actuals} =
+    Option.is_none aliases && HeapPath.Map.is_empty dynamic_types && List.is_empty variadic_actuals
 
 
   let pp_aliases fmt = function
@@ -75,8 +86,9 @@ module Pulse = struct
         F.fprintf fmt "alias: %a " Aliases.pp aliases
 
 
-  let pp fmt {aliases; dynamic_types} =
-    F.fprintf fmt "%a%a" pp_aliases aliases DynamicTypes.pp dynamic_types
+  let pp fmt {aliases; dynamic_types; variadic_actuals} =
+    F.fprintf fmt "%a%a%a" pp_aliases aliases DynamicTypes.pp dynamic_types VariadicActuals.pp
+      variadic_actuals
 
 
   module Set = PrettyPrintable.MakePPSet (struct

infer/src/IR/Specialization.mli

@@ -32,12 +32,18 @@ module Pulse : sig
     type t = Typ.name HeapPath.Map.t [@@deriving equal, compare]
   end
 
+  module VariadicActuals : sig
+    (** the extra variadic actual arguments, in order, as heap paths *)
+    type t = HeapPath.t list [@@deriving equal, compare]
+  end
+
   (** currently [aliases=None] means we did not detect any alias when applying the previous summary
       and this specialization will not introduce any alias assumption.
 
       [aliases=Some []] means something went wrong... We have detected some aliases when applying
       the last summary, but we were not able to phrase it in term of parameters equalities. *)
-  type t = {aliases: Aliases.t option; dynamic_types: DynamicTypes.t}
+  type t =
+    {aliases: Aliases.t option; dynamic_types: DynamicTypes.t; variadic_actuals: VariadicActuals.t}
   [@@deriving equal, compare, yojson_of]
 
   val bottom : t

infer/src/pulse/PulseCallOperations.ml

@@ -998,9 +998,30 @@ let call ?disjunct_limit ({InterproceduralAnalysis.analyze_dependency} as analys
       in
       let max_iteration = Config.pulse_specialization_iteration_limit in
       let already_given = Specialization.Pulse.Set.empty in
+      (* #1937: for a C variadic callee called with extra (variadic) actuals, request an
+         initial specialization carrying those actuals as heap paths so that the callee's
+         [va_arg] reads connect to them (see PulseSpecialization.seed_variadic_actuals). *)
+      let variadic_specialization =
+        let is_variadic =
+          Option.exists (IRAttributes.load callee_pname) ~f:(fun a ->
+              a.ProcAttributes.is_clang_variadic )
+        in
+        match formals_opt with
+        | Some formals when is_variadic && List.length actuals > List.length formals ->
+            let n_extra = List.length actuals - List.length formals in
+            let paths =
+              List.init n_extra ~f:(fun k ->
+                  Specialization.HeapPath.Pvar
+                    (Pvar.mk_global
+                       (Mangled.from_string (Printf.sprintf "__infer_va_actual_%d" k)) ) )
+            in
+            {Specialization.Pulse.bottom with variadic_actuals= paths}
+        | _ ->
+            Specialization.Pulse.bottom
+      in
       let res, summary_used, non_disj, contradiction, resolution_status =
         iter_call ~max_iteration ~nth_iteration:0 ~is_pulse_specialization_limit_reached
-          already_given summary.PulseSummary.main astate
+          ~specialization:variadic_specialization already_given summary.PulseSummary.main astate
       in
       let has_continue_program =
         has_continue_program res || not (NonDisjDomain.astate_is_bottom non_disj)

infer/src/pulse/PulseModelsC.ml

@@ -406,6 +406,57 @@ include struct
   let assertion_error _ : model = start_model @@ fun () -> report_assert_error
 
   let unreachable_path _ : model = start_model @@ fun () -> unreachable
+
+  (* Variadic (`va_list`) modeling for #1937. The `va_list` carries a monotonic cursor;
+     each pointer-typed `va_arg` reads the next element of a global array that is seeded
+     at specialised summary application with the caller's extra (variadic) actuals, so
+     that writes through variadic out-parameters are connected back to the caller. *)
+
+  (* Evaluate a global variable to an abstract value inside a DSL model. *)
+  let eval_read_global pvar : DSL.aval DSL.model_monad =
+    let open DSL.Syntax in
+    let* {PulseModelsImport.path; location} = get_data in
+    exec_operation (fun astate ->
+        let astate, ah = PulseOperations.eval_var path location pvar astate in
+        (ah, astate) )
+
+
+  let va_list_typ = Typ.CStruct (QualifiedCppName.of_qual_string "__infer_va_list")
+
+  let va_list_cursor = Fieldname.make va_list_typ "__infer_va_cursor"
+
+  (* The well-known global that specialization seeds with the caller's variadic actuals
+     (see PulseSpecialization.seed_variadic_actuals). va_arg reads successive elements. *)
+  let va_args_global = Pvar.mk_global (Mangled.from_string "__infer_va_args_global")
+
+  (* va_start: initialise the va_list cursor to 0. The backing array of variadic actuals
+     lives in the [va_args_global] global, seeded at specialised summary application. *)
+  let va_start_model va_list : model =
+    start_model
+    @@ fun () ->
+    let* zero = int 0 in
+    store_field ~ref:(to_aval va_list) va_list_cursor zero
+
+
+  (* va_arg: for a POINTER-typed read, return [va_args_global\[cursor\]] (the seeded caller
+     actual) and advance the cursor; this connects out-parameter writes to the caller. For a
+     non-pointer read (e.g. [va_arg(a, int)]), return a fresh unconstrained value so that
+     value-returning variadic functions (e.g. a summing [sum(int n, ...)]) are unaffected. *)
+  let va_arg_model va_list : model =
+    start_model
+    @@ fun () ->
+    let* {PulseModelsImport.ret= _, ret_typ} = get_data in
+    let va = to_aval va_list in
+    if Typ.is_pointer ret_typ then
+      let* cursor = load_access va (FieldAccess va_list_cursor) in
+      let* args = eval_read_global va_args_global in
+      let* elem = load_access args (ArrayAccess (StdTyp.void, fst cursor)) in
+      let* next = binop_int (Binop.PlusA None) cursor IntLit.one in
+      store_field ~ref:va va_list_cursor next @@> assign_ret elem
+    else assign_ret @= fresh ()
+
+
+  let va_end_model va_list : model = start_model @@ fun () -> check_valid va_list
 end
 
 (** Reference: https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
@@ -560,6 +611,10 @@ let matchers : matcher list =
   let taint_ret_from_arg arg = start_model @@ fun () -> data_dependency_to_ret [arg] in
   let map_context_tenv f (x, _) = f x in
   [ +BuiltinDecl.(match_builtin free) <>$ capt_arg $--> free
+  ; +BuiltinDecl.(match_builtin __builtin_va_start)
+    <>$ capt_arg_payload $+ any_arg $--> va_start_model
+  ; +BuiltinDecl.(match_builtin __builtin_va_arg) <>$ capt_arg_payload $--> va_arg_model
+  ; +BuiltinDecl.(match_builtin __builtin_va_end) <>$ capt_arg_payload $--> va_end_model
   ; +match_regexp_opt Config.pulse_model_free_pattern <>$ capt_arg $+...$--> free
   ; -"realloc" <>$ capt_arg $+ capt_exp $--> realloc ~null_case:true
   ; +match_regexp_opt Config.pulse_model_realloc_pattern

infer/src/pulse/PulseSpecialization.ml

@@ -39,7 +39,42 @@ let rec initialize_heap_path heap_path astate =
       Memory.eval_edge src_addr Dereference astate
 
 
-let apply {Specialization.Pulse.aliases; dynamic_types} location astate =
+(* Well-known global that bridges specialization (seeds the caller's variadic actuals)
+   and the C `va_start`/`va_arg` models (read them back). See #1937. *)
+let va_args_global_pvar = Pvar.mk_global (Mangled.from_string "__infer_va_args_global")
+
+(* Seed the global va-args array with the caller's extra (variadic) actuals so that,
+   during specialized re-analysis of a C variadic callee, each `va_arg` read connects
+   to the corresponding caller argument. *)
+let seed_variadic_actuals variadic_actuals location astate =
+  match variadic_actuals with
+  | [] ->
+      astate
+  | _ ->
+      let astate, global_addr =
+        let opt =
+          Stack.find_opt (Var.of_pvar va_args_global_pvar) astate
+          |> Option.map ~f:ValueOrigin.addr_hist
+        in
+        match opt with
+        | Some ah ->
+            (astate, ah)
+        | None ->
+            let ah = (AbstractValue.mk_fresh (), ValueHistory.epoch) in
+            (astate, ah)
+      in
+      List.foldi variadic_actuals ~init:astate ~f:(fun k astate heap_path ->
+          let astate, actual_ah = initialize_heap_path heap_path astate in
+          let index = (AbstractValue.mk_fresh (), ValueHistory.epoch) in
+          let astate =
+            PulseArithmetic.and_eq_int (fst index) (IntLit.of_int k) astate
+            |> PulseOperationResult.sat_ok |> Option.value ~default:astate
+          in
+          let access = Access.ArrayAccess (StdTyp.void, fst index) in
+          Memory.add_edge PathContext.initial global_addr access actual_ah location astate )
+
+
+let apply {Specialization.Pulse.aliases; dynamic_types; variadic_actuals} location astate =
   let astate =
     Option.value_map aliases ~default:astate ~f:(fun aliases ->
         List.fold aliases ~init:astate ~f:(fun astate alias ->
@@ -58,4 +93,5 @@ let apply {Specialization.Pulse.aliases; dynamic_types} location astate =
         PulseArithmetic.and_dynamic_type_is_unsafe addr typ location astate )
       dynamic_types astate
   in
+  let astate = seed_variadic_actuals variadic_actuals location astate in
   astate

infer/tests/codetoanalyze/c/pulse/issues.exp

@@ -276,3 +276,8 @@ codetoanalyze/c/pulse/var_arg.c, sum_one_then_npe_bad, 3, NULLPTR_DEREFERENCE, n
 codetoanalyze/c/pulse/var_arg.c, FP_sum_then_unreachable_npe_ok, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/var_arg.c, unknown_sum_one_then_npe_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/var_arg.c, unknown_sum_four_then_npe_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
+codetoanalyze/c/pulse/var_arg.c, FP_va_arg_out_param_no_leak_ok, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `v` declared here,read to uninitialized value occurs here]
+codetoanalyze/c/pulse/var_arg.c, FP_va_arg_two_out_params_no_leak_ok, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `v` declared here,read to uninitialized value occurs here]
+codetoanalyze/c/pulse/var_arg.c, FP_va_arg_two_out_params_no_leak_ok, 4, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `u` declared here,read to uninitialized value occurs here]
+codetoanalyze/c/pulse/var_arg.c, FP_va_arg_out_param_loop_no_leak_ok, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `v` declared here,read to uninitialized value occurs here]
+codetoanalyze/c/pulse/var_arg.c, FP_va_multi_malloc_out_params_ok, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `v` declared here,read to uninitialized value occurs here]

infer/tests/codetoanalyze/c/pulse/var_arg.c

@@ -63,3 +63,82 @@ void unknown_sum_four_then_npe_bad() {
   int* p = NULL;
   *p = four;
 }
+
+// #1937: memory allocated and stored through a variadic out-parameter used to be a
+// false MEMORY_LEAK_C, because [va_arg]'s result was disconnected from the caller's
+// argument. It is now connected via specialization, so the leak is no longer reported.
+// A separate PULSE_UNINITIALIZED_VALUE false positive on the out-parameter remains and
+// is marked with FP_ below.
+
+void va_set_ptr(int n, ...) {
+  va_list args;
+  va_start(args, n);
+  char** p = va_arg(args, char**);
+  *p = (char*)malloc(4);
+  va_end(args);
+}
+
+// no MEMORY_LEAK_C (fixed); FP_ marks the remaining UNINITIALIZED_VALUE on `v`
+void FP_va_arg_out_param_no_leak_ok() {
+  char* v;
+  va_set_ptr(1, &v);
+  free(v);
+}
+
+void va_set_two_ptrs(int n, ...) {
+  va_list args;
+  va_start(args, n);
+  char** p = va_arg(args, char**);
+  char** q = va_arg(args, char**);
+  *p = (char*)malloc(4);
+  *q = (char*)malloc(4);
+  va_end(args);
+}
+
+void FP_va_arg_two_out_params_no_leak_ok() {
+  char *v, *u;
+  va_set_two_ptrs(2, &v, &u);
+  free(v);
+  free(u);
+}
+
+void va_set_ptrs_loop(int n, ...) {
+  va_list args;
+  va_start(args, n);
+  for (int i = 0; i < n; i++) {
+    char** p = va_arg(args, char**);
+    *p = (char*)malloc(4);
+  }
+  va_end(args);
+}
+
+void FP_va_arg_out_param_loop_no_leak_ok() {
+  char* v;
+  va_set_ptrs_loop(1, &v);
+  free(v);
+}
+
+// Known limitation (#1937): a single [malloc] distributed across several
+// out-parameters (pointers into one block) is not modelled, so both a spurious
+// MEMORY_LEAK_C and UNINITIALIZED_VALUE are still reported.
+void* va_multi_malloc(int n, ...) {
+  va_list args;
+  va_start(args, n);
+  char* start = (char*)malloc(4 * n);
+  if (!start)
+    return 0;
+  char* res = start;
+  for (int i = 0; i < n; i++) {
+    char** p = va_arg(args, char**);
+    *p = res;
+    res += 4;
+  }
+  va_end(args);
+  return start;
+}
+
+void FP_va_multi_malloc_out_params_ok() {
+  char *v, *u;
+  va_multi_malloc(2, &v, &u);
+  free(v);
+}