From ae51630d77bc84b7e260c8c77ef32563472722df Mon Sep 17 00:00:00 2001 From: Suryansh Sijwali Date: Mon, 13 Jul 2026 03:01:00 -0400 Subject: [PATCH] [pulse] model C variadic out-parameters to fix false MEMORY_LEAK_C --- infer/src/IR/Specialization.ml | 24 ++++-- infer/src/IR/Specialization.mli | 8 +- infer/src/pulse/PulseCallOperations.ml | 23 +++++- infer/src/pulse/PulseModelsC.ml | 55 ++++++++++++++ infer/src/pulse/PulseSpecialization.ml | 38 +++++++++- infer/tests/codetoanalyze/c/pulse/issues.exp | 5 ++ infer/tests/codetoanalyze/c/pulse/var_arg.c | 79 ++++++++++++++++++++ 7 files changed, 223 insertions(+), 9 deletions(-) diff --git a/infer/src/IR/Specialization.ml b/infer/src/IR/Specialization.ml index 500818d980f..ac498410074 100644 --- a/infer/src/IR/Specialization.ml +++ b/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 diff --git a/infer/src/IR/Specialization.mli b/infer/src/IR/Specialization.mli index 74c01e38b30..f61a160c118 100644 --- a/infer/src/IR/Specialization.mli +++ b/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 diff --git a/infer/src/pulse/PulseCallOperations.ml b/infer/src/pulse/PulseCallOperations.ml index 8c9e7019d87..393bc2f1fe4 100644 --- a/infer/src/pulse/PulseCallOperations.ml +++ b/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) diff --git a/infer/src/pulse/PulseModelsC.ml b/infer/src/pulse/PulseModelsC.ml index eebc2ee827e..c63e90034ce 100644 --- a/infer/src/pulse/PulseModelsC.ml +++ b/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 diff --git a/infer/src/pulse/PulseSpecialization.ml b/infer/src/pulse/PulseSpecialization.ml index b0c12014506..1e6b8b5a19d 100644 --- a/infer/src/pulse/PulseSpecialization.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index c6a755b04ce..41fefeb869d 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/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] diff --git a/infer/tests/codetoanalyze/c/pulse/var_arg.c b/infer/tests/codetoanalyze/c/pulse/var_arg.c index 5eae8d5f1ce..c8ccd8b8e2b 100644 --- a/infer/tests/codetoanalyze/c/pulse/var_arg.c +++ b/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); +}