Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Non-recursive implementation of DependencyGraph to avoid stack overflow #590

Merged
merged 2 commits into from
Dec 12, 2023

Conversation

ThomasHaas
Copy link
Collaborator

No description provided.

@hernanponcedeleon
Copy link
Owner

@ThomasHaas do you remember any benchmark having this problem? I thought we had some in svcomp, but I cannot find any.

// Recursion in progress (we returned from a deeper recursion level)
v.lowlink = Math.min(v.lowlink, lastVisited.lowlink);
} else {
assert false;

Choose a reason for hiding this comment

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

I guess this point should never be reached. Maybe we should add an error msg to this sanity check.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I don't think an error message is reasonable for these kinds of invariants. But I will change the code to just have a else { assert (cond); ...} rather than else if (cond) { ...} else { assert false; }

Choose a reason for hiding this comment

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

Once you do this change, I can merge

@ThomasHaas
Copy link
Collaborator Author

@ThomasHaas do you remember any benchmark having this problem? I thought we had some in svcomp, but I cannot find any.

No, there are probably some examples in the Slack channel. Anyway, the problem must be gone because the recursion is definitely gone and I don't need a unit test to tell you that :P. Of course, it might be interesting to check if the programs now show other issues.

@hernanponcedeleon hernanponcedeleon merged commit c8111be into development Dec 12, 2023
1 check passed
@hernanponcedeleon hernanponcedeleon deleted the depGraph_no_recursion branch December 12, 2023 10:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants