analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

Split octagon autotuner to separate octagonAnalysis and octagonVars autotuners

Open sim642 opened this issue 3 months ago • 1 comments

Turns out when the octagon autotuner says Enabled octagon domain for: ..., it implicitly means "disabling octagon analysis for all other variables, _even if explicitly enabled by the user". This massively shoot us in the foot for #1394 benchmarks, where explicitly enabling the apron analysis on top of the normal svcomp configuration, which intuitively should only make things more precise, only produced 1 relational invariant. Actually the autotuner more-or-less overrode that, disabling the autotuner gives us 1896 invariants!

We're really selling our novel relational analyses short by disabling them even when explicitly requested. If it's counterintuitive for us, it will definitely be counterintuitive for anyone else evaluating Goblint.

Much less confusing behavior would be to split the autotuner into two:

  1. octagonAnalysis, which is just in charge of enabling the octagon analysis, but not choosing a subset of the variables.
  2. octagonVars, which is in charge of choosing the variables, i.e. disabling octagon analysis for all other variables (because that's what it's really doing, not enabling for additional variables).

sim642 avatar May 08 '24 06:05 sim642