Skip to content

Split octagon autotuner to separate octagonAnalysis and octagonVars autotuners #1449

Open
@sim642

Description

@sim642

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).

Metadata

Metadata

Assignees

No one assigned

    Labels

    cleanupRefactoring, clean-upprecisionrelationalRelational analyses (Apron, affeq, lin2var)sv-compSV-COMP (analyses, results), witnessesusability

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions