Skip to content

Conversation

@michael-schwarz
Copy link
Member

@jerhard and I realized that implementing the removal of directly recursive trash is quite easy. This PR adds this and a test where it makes a difference.

This is against a new branch on the same state as #1636, so the PR appears in this repo and not in the fork. Once #1636 is merged (hopefully soon), we can change the base for this.

michael-schwarz added a commit that referenced this pull request Apr 16, 2025
michael-schwarz added a commit that referenced this pull request Apr 16, 2025
@sim642 sim642 added the pr-dependency Depends or builds on another PR, which should be merged before label Apr 16, 2025
@michael-schwarz
Copy link
Member Author

I made a fork also of the experiments repo: https://github.com/tum-cit-pl/precision-recovery-mixed-flowsens-benchmarks/tree/cyclic

For now, there is no additional precision gain for large programs: plot4.pdf

@michael-schwarz michael-schwarz requested a review from jerhard April 17, 2025 08:16
@michael-schwarz
Copy link
Member Author

There is one program where we discover one additional call in a context to be dead:

Warning: siege.c has different dead counts for ours-bot-rec and ours-bot
Dead with ours-bot-rec: (756, 756, 808, 3198)
Dead with ours-bot: (755, 755, 808, 3198)

where the format is stillbot,botified,dead,total.

The experiments are run on https://github.com/goblint/analyzer/tree/pldi25_eval_stats_rectrash.

Copy link
Member

@sim642 sim642 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What does "directly recursive" mean? A function in a context depending on the same function in the same context, and only that?

@michael-schwarz
Copy link
Member Author

A function in a context depending on the same function in the same context, and only that?

Yes!

@sim642 sim642 removed the pr-dependency Depends or builds on another PR, which should be merged before label Apr 17, 2025
@michael-schwarz
Copy link
Member Author

Even after the fixes by @jerhard and me, there is only one program in the large subset where this makes a difference.

@michael-schwarz
Copy link
Member Author

It does not seem like it would make sense to pursue this for now.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants