typetools / checker-framework

Pluggable type-checking for Java
http://checkerframework.org/
Other
988 stars 347 forks source link

Potential Exponential Behavior in Obligation Tracking in Must Call Inference #6566

Closed iamsanjaymalakar closed 2 weeks ago

iamsanjaymalakar commented 2 weeks ago

Description

During the investigation of what was initially suspected to be a non-termination bug in the url90b6689baa_adsonrocha_PD321_tgz-pJ8-MyFuzzyLiteClassJ8 project from the NJR dataset, it was discovered that the issue may actually be exponential growth in complexity rather than non-termination. This behavior occurs due to an unchecked accumulation of obligations to track across multiple control-flow paths when the bailout check MustCallConsistencyAnalyzer::shouldTrackInvocationResult is absent.

Steps to Reproduce

Fix

The MustCallConsistencyAnalyzer has a bail-out check before tracking obligations using the shouldTrackInvocationResult method. The original method was designed primarily for MustCall consistency checks and did not accommodate the unique requirements of resource leak inference.

The original method does not track the invocation result in these cases:

For example, consider the following code snippet:

@InheritableMustCall("a")
private class MCASuperClass {
  final @Owning Foo f;

  @MustCallAlias MCASuperClass(@MustCallAlias Foo foo) {
    this.f = foo;
  }

  public void a() {
    f.a();
  }
}

private class MCASuperCall extends MCASuperClass {
  MCASuperCall(Foo foo) {
    super(foo);
  }
}

In this scenario, if obligations for the super(foo) call are not tracked, then the must-call inference cannot infer that the parameter Foo foo and the constructor are resource aliases. This failure results in the inability to infer the @MustCallAlias annotation correctly for the MCASuperCall, leading to potential resource management issues.

@MustCallAlias MCASuperCall(@MustCallAlias Foo foo) {
  super(foo);
}

To rectify this, a new parameter isMustCallInference was added to the shouldTrackInvocationResult method. This parameter allows the method to adapt its behavior based on the context—skipping tracking where safe in general cases but enforcing it in resource leak scenarios to ensure accurate management of obligations.

CF Invocation Environment