No way to set a configuration option to an empty value

[MartinSpiessl]

Taken from:

https://gitlab.com/sosy-lab/software/cpachecker/-/issues/578#note_412658216

Does an empty option (empty string, not an empty set) override an existing value correctly?

There seems to be a difference for: scripts/cpa.sh -valueAnalysis-concurrency -spec test/programs/benchmarks/properties/unreach-call.prp test/programs/benchmarks/pthread-atomic/dekker.i

when using the additional option: -setprop cpa.callstack.unsupportedFunctions=dummy # or "{}" or: -setprop cpa.callstack.unsupportedFunctions= # empty string

Is this a bug in our option handling?

The general problem is if an option that contains some kind of collection has a default value other than the empty list, how can we reset it to just contain the empty list?

[PhilippWendler]

If specifying an empty value currently does not work, then there is no other way. We should certainly make this possible, the question is how?

While resetting an option to the default value if an empty value is given is unintuitive, it has been the behavior of the configuration system for a long time, so people might (even without noticing it) rely on it. If we change the behavior now, this would mean that we suddenly silently produce different values.

[MartinSpiessl]

What about a special option that will clear the option names it gets in its value list:

options.setToEmptyList=cpa.callstack.unsupportedFunctions,cpa.predicate.foobar

That would probably already be possible to implement without touching the common lib. But of course it is not obvious and adds more complexity to the already complex config option handling. The advantage would be that we do not need to extend the syntax/introduce special character sequences etc.

[PhilippWendler]

What about a special option that will clear the option names it gets in its value list:

options.setToEmptyList=cpa.callstack.unsupportedFunctions,cpa.predicate.foobar

That would probably already be possible to implement without touching the common lib.

No, this really needs to be done in this lib, but of course, there is also no problem with that and it would be much better than doing it somewhere else anyway.

A reason why this needs to be done here is #include. If the main config file declares foo=bar and an included config file declares options.setToEmptyList=foo, how would you correctly find out that foo=bar if you look only at the map of options after the parsing is finished.

[MartinSpiessl]

A reason why this needs to be done here is #include. If the main config file declares foo=bar and an included config file declares options.setToEmptyList=foo, how would you correctly find out that foo=bar if you look only at the map of options after the parsing is finished.

I guess I did not think this trough. Yeah makes total sense, so it cannot be decided by the tool and has to be done in common lib.

No, this really needs to be done in this lib, but of course, there is also no problem with that and it would be much better than doing it somewhere else anyway.

So just to get this right, does that mean you would be in favor of adding such an option here in java-common-lib? Is there already a namespace where such things could be put, i.e., is there a better name than options.setToEmptyList?

[PhilippWendler]

No, I am not really in favor of adding such an option, I think it would be quite hard to discover and awkward to use.

For example, there are still complications with includes. In order to avoid the above problem, we would have to apply this option immediately after parsing an included file. However, this would mean that this option could not be overridden in including files, which would make it behave differently from all other options.

We would also have to think through what happens if this option is not specified in a config file but via some other way (in case of CPAchecker for example with -setprop). We certainly want a way to set options to the empty value in this case, too, however, this would make it even harder to understand (especially why it is not possible to overwrite the value of your proposed option in a config file with a different value for the same option on the command line).

And then for example in CPAchecker there are use cases where configuration instances are converted into strings, passed to some other component either in form of a config file or a list of command-line options, and then parsed again. I strongly suspect this would break here.

[PhilippWendler]

One thing that came to my mind while thinking about this:

We should probably not only provide a new way to set an option to the empty value, but also a new way to reset an option to the default value (i.e., what the current behavior of foo= is). If we do this, we can add a warning whenever the current ambiguous form foo= is used, and potentially at some point in the future even forbid this.