search

goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
160 stars 72 forks source link

ApronPrecCompare runs >= 35h and consumes 40GB of RAM #1490

Open michael-schwarz opened 1 month ago

michael-schwarz commented 1 month ago

/home/goblint/michael-schwarz-dissertation/analyzer/apronPrecCompare /home/goblint/michael-schwarz-dissertation/bench/bench_result/wrk.box.prec /home/goblint/michael-schwarz-dissertation/bench/bench_result/wrk.oct.prec /home/goblint/michael-schwarz-dissertation/bench/bench_result/wrk.cluster12.prec

Does not terminate after more than 35h and gobbling up some 40GB of RAM, even though the individual analyses all terminated within 15min.

sim642 commented 1 month ago

How large are the dump files themselves? It could either be that the input files are already overly massive or that the comparison somehow allocates too much something.

michael-schwarz commented 1 month ago

They are ~800 MB each.

sim642 commented 1 month ago

That's quite significant, although I don't remember how large they were at the time (maybe I still have some laying around). There isn't much that can be done about it though I guess. We might've also gotten more precise which leads to more constraints in the output.

Is there any output over this comparison time or not? I wonder if there's slowdown due to just printing large states (e.g. in Pretty/Format) or it blows up before that point is reached.

michael-schwarz commented 1 month ago

Is there any output over this comparison time or not?

There's no output at this point.