Skip to content

Commit

Permalink
[pulse] suppress mutual recursion reports when heap progress has been…
Browse files Browse the repository at this point in the history
… made

Summary:
This usually indicates the recursion is intended as we are traversing an
inductive data structure. Could miss real bugs caused by cycles in the
heap in other calling contexts.

Reviewed By: skcho

Differential Revision:
D66667343

Privacy Context Container: L1208441

fbshipit-source-id: 64fd07d914168a5d6fa27734a249720e0057486a
  • Loading branch information
jvillard authored and facebook-github-bot committed Dec 3, 2024
1 parent c269e0f commit e995511
Show file tree
Hide file tree
Showing 7 changed files with 116 additions and 8 deletions.
28 changes: 28 additions & 0 deletions infer/src/pulse/PulseAbductiveDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2332,6 +2332,34 @@ let reachable_addresses_from ?edge_filter addresses astate pre_or_post =
|> CanonValue.downcast_set
let has_reachable_in_inner_pre_heap addresses astate =
(* We are looking for one "real" (i.e. in the program text somewhere) dereference from the stack
variables in the pre-condition. Since the first dereference is always to access the value of
the formal, it is enough to look for access paths with at least two dereferences. *)
let has_two_dereferences accesses =
let rec has_two_dereferences_aux has_deref (accesses : Access.t list) =
match accesses with
| [] ->
false
| Dereference :: accesses' ->
has_deref || has_two_dereferences_aux true accesses'
| _ :: accesses' ->
has_two_dereferences_aux has_deref accesses'
in
has_two_dereferences_aux false accesses
in
let addresses =
ListLabels.to_seq addresses |> Seq.map (CanonValue.canon' astate) |> CanonValue.Set.of_seq
in
GraphVisit.fold astate
~var_filter:(fun _ -> true)
`Pre ~init:false ~finish:Fn.id
~f:(fun _ found v accesses ->
if CanonValue.Set.mem v addresses && has_two_dereferences accesses then Stop true
else Continue found )
|> snd
module Stack = struct
include SafeStack
Expand Down
6 changes: 6 additions & 0 deletions infer/src/pulse/PulseAbductiveDomain.mli
Original file line number Diff line number Diff line change
Expand Up @@ -353,6 +353,12 @@ val reachable_addresses_from :
-> AbstractValue.Set.t
(** Compute the set of abstract addresses that are reachable from given abstract addresses. *)

val has_reachable_in_inner_pre_heap : AbstractValue.t list -> t -> bool
(** [true] if there is a value in the provided list that is reachable from the pre-condition after
some non-trivial steps in the pre heap, i.e. the value is gotten from at least one dereference
from the parameters of the current procedure. Used to detect likely-harmless recursive calls
since heap progress has been made. *)

val get_unreachable_attributes : t -> AbstractValue.t list
(** collect the addresses that have attributes but are unreachable in the current post-condition *)

Expand Down
26 changes: 23 additions & 3 deletions infer/src/pulse/PulseCallOperations.ml
Original file line number Diff line number Diff line change
Expand Up @@ -671,9 +671,29 @@ let on_recursive_call ({InterproceduralAnalysis.proc_desc} as analysis_data) cal
L.d_printfln "Suppressing recursive call report for non-user-visible function %a"
Procname.pp callee_pname
| _ ->
PulseReport.report analysis_data ~is_suppressed:false ~latent:false
(MutualRecursionCycle
{cycle= PulseMutualRecursion.mk call_loc callee_pname; location= call_loc} ) ) ;
if
AbductiveDomain.has_reachable_in_inner_pre_heap
(List.map actuals ~f:(fun ((actual, _), _) -> actual))
astate
then
L.d_printfln
"heap progress made before recursive call to %a; unlikely to be an infinite recursion, \
suppressing report"
Procname.pp callee_pname
else
PulseReport.report analysis_data ~is_suppressed:false ~latent:false
(MutualRecursionCycle
{cycle= PulseMutualRecursion.mk call_loc callee_pname; location= call_loc} ) ) ;
astate )
else if
AbductiveDomain.has_reachable_in_inner_pre_heap
(List.map actuals ~f:(fun ((actual, _), _) -> actual))
astate
then (
L.d_printfln
"heap progress made before recursive call to %a; unlikely to be an infinite recursion, not \
recording the cycle"
Procname.pp callee_pname ;
astate )
else AbductiveDomain.add_recursive_call call_loc callee_pname astate

Expand Down
19 changes: 15 additions & 4 deletions infer/src/pulse/PulseInterproc.ml
Original file line number Diff line number Diff line change
Expand Up @@ -964,7 +964,7 @@ let report_mutual_recursion_cycle


let record_recursive_calls ({InterproceduralAnalysis.proc_desc} as analysis_data) callee_proc_name
call_loc callee_summary call_state =
call_loc actuals callee_summary call_state =
if Procname.is_hack_xinit (Procdesc.get_proc_name proc_desc) then (
L.d_printfln "Not recording recursive calls for Hack xinit caller function %a" Procname.pp
(Procdesc.get_proc_name proc_desc) ;
Expand All @@ -975,6 +975,16 @@ let record_recursive_calls ({InterproceduralAnalysis.proc_desc} as analysis_data
L.d_printfln "Not recording recursive calls for Hack xinit callee function %a" Procname.pp
callee_proc_name ;
call_state )
else if
AbductiveDomain.has_reachable_in_inner_pre_heap
(List.map actuals ~f:(fun ((actual, _), _) -> actual))
call_state.astate
then (
L.d_printfln
"Not recording recursive calls for function %a since heap progress has been made to compute \
actuals"
Procname.pp callee_proc_name ;
call_state )
else
let callee_recursive_calls =
PulseMutualRecursion.Set.filter_map
Expand Down Expand Up @@ -1101,7 +1111,7 @@ let read_return_value {PathContext.timestamp} callee_proc_name call_loc
) )


let apply_post analysis_data path callee_proc_name call_location callee_summary call_state =
let apply_post analysis_data path callee_proc_name call_location actuals callee_summary call_state =
PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call post" ())) ;
let r =
call_state
Expand All @@ -1110,7 +1120,7 @@ let apply_post analysis_data path callee_proc_name call_location callee_summary
>>= apply_post_from_callee_post path callee_proc_name call_location callee_summary
>>| add_attributes `Post path callee_proc_name call_location
(AbductiveDomain.Summary.get_post callee_summary).attrs
>>| record_recursive_calls analysis_data callee_proc_name call_location callee_summary
>>| record_recursive_calls analysis_data callee_proc_name call_location actuals callee_summary
>>| record_skipped_calls callee_proc_name call_location callee_summary
>>| record_transitive_info analysis_data callee_proc_name call_location callee_summary
>>| read_return_value path callee_proc_name call_location callee_summary
Expand Down Expand Up @@ -1295,7 +1305,8 @@ let apply_summary analysis_data path ~callee_proc_name call_location ~callee_sum
let call_state = {call_state with astate; visited= AddressSet.empty} in
(* apply the postcondition *)
let* call_state, return_caller =
apply_post analysis_data path callee_proc_name call_location callee_summary call_state
apply_post analysis_data path callee_proc_name call_location actuals callee_summary
call_state
in
let astate =
if Topl.is_active () then
Expand Down
1 change: 0 additions & 1 deletion infer/tests/codetoanalyze/c/pulse/issues.exp
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,6 @@ codetoanalyze/c/pulse/latent.c, FN_crash_after_six_nodes_bad, 1, NULLPTR_DEREFER
codetoanalyze/c/pulse/latent.c, FN_crash_after_six_nodes_bad, 1, NULLPTR_DEREFERENCE_LATENT, no_bucket, ERROR, [*** SUPPRESSED ***,source of the null value part of the trace starts here,is assigned to the null pointer,null pointer dereference part of the trace starts here,parameter `q` of FN_crash_after_six_nodes_bad,invalid access occurs here]
codetoanalyze/c/pulse/latent.c, FN_crash_after_six_nodes_bad, 1, NULLPTR_DEREFERENCE_LATENT, no_bucket, ERROR, [*** SUPPRESSED ***,source of the null value part of the trace starts here,is assigned to the null pointer,null pointer dereference part of the trace starts here,parameter `q` of FN_crash_after_six_nodes_bad,invalid access occurs here]
codetoanalyze/c/pulse/latent.c, FN_crash_after_six_nodes_bad, 1, NULLPTR_DEREFERENCE_LATENT, no_bucket, ERROR, [*** SUPPRESSED ***,source of the null value part of the trace starts here,is assigned to the null pointer,null pointer dereference part of the trace starts here,parameter `q` of FN_crash_after_six_nodes_bad,invalid access occurs here]
codetoanalyze/c/pulse/list_api.c, list_elem_free, 5, MUTUAL_RECURSION_CYCLE, no_bucket, WARNING, [`list_elem_free` makes a recursive call to `list_elem_free`]
codetoanalyze/c/pulse/list_api.c, list_free, 1, NULLPTR_DEREFERENCE_LATENT, no_bucket, ERROR, [*** SUPPRESSED ***,source of the null value part of the trace starts here,is assigned to the null pointer,null pointer dereference part of the trace starts here,parameter `ptr` of list_free,invalid access occurs here]
codetoanalyze/c/pulse/list_checks.c, null_ptr_deref_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,when calling `go_to_next` here,parameter `head` of go_to_next,invalid access occurs here]
codetoanalyze/c/pulse/list_checks.c, null_ptr_deref2_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,when calling `go_to_end_of_list` here,parameter `head` of go_to_end_of_list,invalid access occurs here]
Expand Down
1 change: 1 addition & 0 deletions infer/tests/codetoanalyze/hack/pulse/issues.exp
Original file line number Diff line number Diff line change
Expand Up @@ -215,6 +215,7 @@ propagators.hack, Propagators::Flows$static.propToSinkBad, 3, TAINT_ERROR, no_bu
propagators.hack, Propagators::Flows$static.propWithSinkBad, 2, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `Propagators::Source$static.getTainted` with kind `Propagators`,when calling `Propagators::Prop$static.propWithSink` here,flows to this sink: value passed as argument `#0` to `Propagators::Sink$static.process` with kind `Propagators`], source: Propagators::Source$static.getTainted, sink: Propagators::Sink$static.process, tainted expression: Propagators::Prop$static.propWithSink()
propagators.hack, Propagators::Flows$static.propWithSinkToSinkBad, 2, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `Propagators::Source$static.getTainted` with kind `Propagators`,when calling `Propagators::Prop$static.propWithSink` here,flows to this sink: value passed as argument `#0` to `Propagators::Sink$static.process` with kind `Propagators`], source: Propagators::Source$static.getTainted, sink: Propagators::Sink$static.process, tainted expression: Propagators::Prop$static.propWithSink()
propagators.hack, Propagators::Flows$static.propWithSinkToSinkBad, 3, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `Propagators::Source$static.getTainted` with kind `Propagators`,flows to this sink: value passed as argument `#0` to `Propagators::Sink$static.process` with kind `Propagators`], source: Propagators::Source$static.getTainted, sink: Propagators::Sink$static.process, tainted expression: $t1
recursion.hack, Node.infinite_bad, 1, MUTUAL_RECURSION_CYCLE, no_bucket, WARNING, [`Node.infinite_bad` makes a recursive call to `Node.infinite_bad`]
return_type_matcher.hack, ReturnTypeMatcher::Flows$static.source1TaintFlowBad, 2, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `ReturnTypeMatcher::Source1$static.getTainted` with kind `ReturnTypeMatcher`,flows to this sink: value passed as argument `#0` to `ReturnTypeMatcher::Sink$static.process` with kind `ReturnTypeMatcher`], source: ReturnTypeMatcher::Source1$static.getTainted, sink: ReturnTypeMatcher::Sink$static.process, tainted expression: $source
return_type_matcher.hack, ReturnTypeMatcher::Flows$static.source2TaintFlowBad, 2, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `ReturnTypeMatcher::Source2$static.getTainted` with kind `ReturnTypeMatcher`,flows to this sink: value passed as argument `#0` to `ReturnTypeMatcher::Sink$static.process` with kind `ReturnTypeMatcher`], source: ReturnTypeMatcher::Source2$static.getTainted, sink: ReturnTypeMatcher::Sink$static.process, tainted expression: $source
sanitizers.hack, Sanitizers::Flows$static.taintedNotSanitizedBad, 2, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `Sanitizers::Source.getTainted` with kind `Sanitizers`,flows to this sink: value passed as argument `#0` to `Sanitizers::Sink$static.process` with kind `Sanitizers`], source: Sanitizers::Source.getTainted, sink: Sanitizers::Sink$static.process, tainted expression: $t
Expand Down
43 changes: 43 additions & 0 deletions infer/tests/codetoanalyze/hack/pulse/recursion.hack
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
// Copyright (c) Facebook, Inc. and its affiliates.
//
// This source code is licensed under the MIT license found in the
// LICENSE file in the root directory of this source tree.

class Node {
private Node $next;
private int $data;

public function __construct(int $data, Node $next) {
$this->data = $data;
$this->next = $next;
}

public function length_ok(): int {
if ($this->next == null) {
return 1;
}
return 1 + $this->next->length_ok();
}

// progress in callee
public function interproc_progress_ok(Node $list): void {
$this->interproc2_ok($list);
}

private function interproc2_ok(Node $list): void {
$this->interproc_progress_ok($list->next);
}

// progress before callee
public function other_interproc_progress_ok(Node $list): void {
$this->other_interproc2_ok($list->next);
}

private function other_interproc2_ok(Node $list): void {
$this->other_interproc_progress_ok($list);
}

public function infinite_bad(Node $something, Node $other): int {
return $this->infinite_bad($other, $something);
}
}

0 comments on commit e995511

Please sign in to comment.