Two-phase configuration: freeze point and analysis-phase getters

[Copilot]

Config reads during AfterConfig.run() (e.g. privatization module construction) see stale values because the autotuner runs afterward and modifies config. This introduces a two-phase configuration mechanism to separate config-building from analysis.

Changes

src/config/gobConfig.ml

• Added frozen : bool ref flag and is_frozen () / freeze () functions — freeze () permanently prevents further set_* calls
• Added analysis_read : bool ref flag — set to true once any get_*_analysis call is made; once set, any set_* call raises UsedForAnalysis
• Added exception UsedForAnalysis of string — raised by any set_* call if analysis_read is set, making configuration timing errors immediately visible
• Added analysis-phase getters: get_int_analysis, get_bool_analysis, get_string_analysis, get_list_analysis, get_string_list_analysis
• Added clear_analysis_reads () — resets the analysis_read flag; called automatically by with_immutable_conf on exit so that server-mode config changes between analysis runs continue to work

src/goblint.ml

• Call GobConfig.freeze () after all config modifications (AutoSoundConfig + AutoTune.chooseConfig) and before do_analyze

AutoSoundConfig.activateLongjmpAnalysesWhenRequired ();
if get_string "ana.specification" <> "" then AutoSoundConfig.enableAnalysesForSpecification ();
if get_bool "ana.autotune.enabled" then AutoTune.chooseConfig file;
GobConfig.freeze ();   (* <-- new: config locked from here *)
file |> do_analyze changeInfo;

How it catches bugs

Analysis code should use get_*_analysis instead of get_* for reads whose results feed into the analysis. Once any such call is made, all subsequent set_* calls raise UsedForAnalysis, pinpointing the timing error immediately rather than silently producing wrong results.

Server mode

freeze () is only called in the non-server path. Server mode continues using with_immutable_conf temporarily per analysis run, which now also calls clear_analysis_reads () on exit so that inter-run config changes via set_* are not blocked by reads from the previous run.

[michael-schwarz]

@copilot. This does not address the core issue, the problem is when values are used before the configuration has been built. So there should be two get functions, one for value to be used in the analysis, and one for getting values during building.

If a value is modified after a call to the get variant for analysis, an exception should be raised.

[Copilot]

@copilot. This does not address the core issue, the problem is when values are used before the configuration has been built. So there should be two get functions, one for value to be used in the analy...

Done in commit 2fd6827. The implementation adds:

• get_int_analysis, get_bool_analysis, get_string_analysis, get_list_analysis, get_string_list_analysis — analysis-phase getters that record which config paths they read into an analysis_reads set.
• exception UsedForAnalysis of string — raised by any set_* call if the target path was already read via a get_*_analysis function. This makes the timing error immediately visible.
• clear_analysis_reads () — clears the tracking set; called automatically by with_immutable_conf on exit (server mode), so config changes between analysis runs continue to work.

Example: if privatization code calls get_string_analysis "ana.base.privatization" during AfterConfig.run(), and then the autotuner calls set_string "ana.base.privatization" "...", the exception UsedForAnalysis "ana.base.privatization" is immediately raised, identifying the configuration timing error.

[michael-schwarz]

@copilot: The tracking need not be per attribute.

[Copilot]

@copilot: The tracking need not be per attribute.

Done in commit e620873. Replaced the per-attribute Hashtbl with a single bool ref analysis_read. Once any get_*_analysis call is made the flag is set, and any subsequent set_* raises UsedForAnalysis. clear_analysis_reads () resets the flag (called by with_immutable_conf on exit for server mode).