ThreadEscape: Collect set of escaping threads flow-insensitively #1078

jerhard · 2023-06-07T09:05:38Z

This PR changes the ThreadEscape analysis to track which threads escaped a variable in a flow-insensitive invariant. A thread escapes a variable if it assigns it to an lvalue that may already be escaped.

The escape information in the local state now collects only the escapes that happened in the threads own past. That means, there is no joining of escaped variables from the flow-insensitive invariant into the local state.

When queried whether a variable is escaped, the analysis checks the flow-insensitive set of threads that escaped it. If the set is empty, it is not escaped. If the set is not empty, it is checked whether any of the other threads that escaped it may already be started. If so, the variable may be escaped. If none of the other threads escaped the variable, then it is checked whether the current thread may have escaped the variable. This is done by looking it up in the local state.

This approach in particular handles the case when variables escape via globals after some threads have already started (see #1074), while not treating such variables as escaped at all program points (which was one issue with #1075, as well as the issue with the implementation in threadenter mentioned here: #1075 (comment)).

Fixes #1074

…fy it.

…tive invariant.

…mode, support pthread_setspecific again. The base analysis relies on variables being considered escaped even in single-threaded mode, when determining which local variables to pass to a callee: Locals possibly reachable via globals need to be considered escaped.

If the current thread is non-unqiue and may escape the variable queried with (MayEscape v), then v may be escaped.

src/analyses/threadEscape.ml

… rel. Reuse implementation of enter in threadenter to determine what to add to rel.

… thread) to empty set. Previous solution that had a non-empty state was required only due to RelationAnalysis that did not pass reachable variables to the created thread in threadenter.

… args in rel." This reverts commit 7d70907.

jerhard · 2023-06-16T11:35:23Z

Some changes to the RelationAnalysis.threadenter were necessary. The reason is that the RelationAnalysis relied on variables that were reachable for the created thread via an argument to the pthread_create to be considered escaped right away, otherwise, it would crash. This becomes a problem now that the information that the parameter to the pthread_create escapes is only computed later during the evaluation of the constraint system (via a side-effect in threadspawn).
Therefore, I changed the RelationAnalysis.threadenter such that it maintains variables reachable from the passed argument in the relation rel of the created thread.

src/analyses/threadEscape.ml

src/analyses/apron/relationAnalysis.apron.ml

michael-schwarz

Apart from the comments, i think this is good to merge!

…following desctructive update. This ensures that new_rel is a disctinct object from ctx.local.rel to ensure that the latter is not modified by RD.remove_filter_with.

michael-schwarz · 2023-06-29T10:07:07Z

@sim642 Do you still want to review this or are we good to merge?

…eep_vars, keep_filter. The operations on a relational domain (wihtout _with suffix) should ensure that the returned object is not physically equal. This way, the explicit copy in relationAnalysis.make_callee_rel can be avoided.

michael-schwarz · 2023-07-04T13:44:52Z

@sim642 Since the remaining issue was addressed, is this now good to merge?

jerhard added 9 commits June 7, 2023 10:48

Add test case where escaped local has unsound value.

070f7ca

Remove race annotation, as this is secondary for this test case.

843e0dc

Move failing test with local escaping into escape test folder, simpli…

87a10f9

…fy it.

ThreadEscape: Extract function emitting events.

f2c2145

Add simple failiing test case due to unsound escape analysis.

df407b1

ThreadEscape: collect which threads escaped variables in flow-insensi…

9143b2a

…tive invariant.

Add test case, extend test case with interval checks.

7533309

Indent threadEscape.ml

fb90c45

jerhard mentioned this pull request Jun 7, 2023

ThreadEscape: Collect flow-insensitive set of variables reachable from globals #1075

Closed

michael-schwarz self-requested a review June 7, 2023 09:14

ThreadEscape: add escaped to local state in threadenter.

558ae51

sim642 added bug unsound labels Jun 8, 2023

jerhard added 2 commits June 14, 2023 10:43

Enable intervals for test case.

3fd471c

ThreadEscape: Check for uniquness of thread.

006d4ea

If the current thread is non-unqiue and may escape the variable queried with (MayEscape v), then v may be escaped.

github-advanced-security bot found potential problems Jun 14, 2023

View reviewed changes

src/analyses/threadEscape.ml Fixed Show fixed Hide fixed

jerhard added 6 commits June 14, 2023 12:34

RelationAnalysis.threadenter: include reachable thread create args in…

7d70907

… rel. Reuse implementation of enter in threadenter to determine what to add to rel.

ThreadEscape.threadenter: set local state (i.e., variables secaped in…

44d560e

… thread) to empty set. Previous solution that had a non-empty state was required only due to RelationAnalysis that did not pass reachable variables to the created thread in threadenter.

Remove debug output.

fb93563

Revert "RelationAnalysis.threadenter: include reachable thread create…

83e87e5

… args in rel." This reverts commit 7d70907.

Fix apron threadenter for unreached fixedpoint for 63/16.

6b6c00f

RelationAnalysis.threadenter: Deduplicate code with enter.

3d60727

michael-schwarz reviewed Jun 21, 2023

View reviewed changes

src/analyses/threadEscape.ml Outdated Show resolved Hide resolved

michael-schwarz reviewed Jun 21, 2023

View reviewed changes

src/analyses/apron/relationAnalysis.apron.ml Outdated Show resolved Hide resolved

michael-schwarz approved these changes Jun 21, 2023

View reviewed changes

sim642 self-requested a review June 22, 2023 10:21

jerhard added 2 commits June 26, 2023 13:57

Extract check for thread-uniqueness out.

a8c6722

Move copy of relation to ensure that ctx.local.rel is not changed by …

491dfbd

…following desctructive update. This ensures that new_rel is a disctinct object from ctx.local.rel to ensure that the latter is not modified by RD.remove_filter_with.

Move RD.copy up, so that copy is performed on possibly smaller rel.

44233f6

sim642 approved these changes Jul 4, 2023

View reviewed changes

michael-schwarz merged commit d65ed54 into master Jul 4, 2023

michael-schwarz deleted the escape_analysis_flow-insens branch July 4, 2023 16:23

sim642 added this to the v2.2.0 milestone Sep 11, 2023

sim642 mentioned this pull request Sep 13, 2023

[new release] goblint (2.2.0) ocaml/opam-repository#24420

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

ThreadEscape: Collect set of escaping threads flow-insensitively #1078

ThreadEscape: Collect set of escaping threads flow-insensitively #1078

jerhard commented Jun 7, 2023

jerhard commented Jun 16, 2023 •

edited

Loading

michael-schwarz left a comment

michael-schwarz commented Jun 29, 2023

michael-schwarz commented Jul 4, 2023

ThreadEscape: Collect set of escaping threads flow-insensitively #1078

ThreadEscape: Collect set of escaping threads flow-insensitively #1078

Conversation

jerhard commented Jun 7, 2023

jerhard commented Jun 16, 2023 • edited Loading

michael-schwarz left a comment

Choose a reason for hiding this comment

michael-schwarz commented Jun 29, 2023

michael-schwarz commented Jul 4, 2023

jerhard commented Jun 16, 2023 •

edited

Loading