Skip to content

Avoid eager string conversions during analysis #1795

@sim642

Description

@sim642

But the other worrying point is that we're apparently printing something during solving itself. That's unusual, because usually it's just one solver stats printout after another. Perhaps there's some internal unnecessary string conversion taking place as well.

The analyses should not be using Pretty to convert things to strings during the analysis (unless warn_at is early at least). I may be wrong, but I can't currently think of a legitimate reason to do that.
It might help to do an sv-benchmarks run with -v to get the backtrace at that point. I think the backtrace should still contain the entire non-signal-handler stack, so it would expose where are we using Pretty during analysis.

Of course avoiding that isn't a particularly reliable fix, but it would make sense to avoid it anyway for performance reasons.

Originally posted by @sim642 in #1781

Metadata

Metadata

Assignees

Labels

cleanupRefactoring, clean-upperformanceAnalysis time, memory usage

Type

Projects

No projects

Relationships

None yet

Development

No branches or pull requests

Issue actions