From f9063fc3f9230afc8789931407c9965bdca20349 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 12 Apr 2026 07:11:09 +0000 Subject: [PATCH 1/5] Initial plan From ac9eccb91c50bb0e53ac72ef14bdb3b2d6320f3c Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 12 Apr 2026 07:33:29 +0000 Subject: [PATCH 2/5] Add freeze mechanism to GobConfig and call it before analysis Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/e7f71803-86c8-4b4a-a4cc-78b9bce5ae4b Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> --- src/config/gobConfig.ml | 17 +++++++++++++++++ src/goblint.ml | 1 + 2 files changed, 18 insertions(+) diff --git a/src/config/gobConfig.ml b/src/config/gobConfig.ml index 92012108c3..97821e38b6 100644 --- a/src/config/gobConfig.ml +++ b/src/config/gobConfig.ml @@ -91,6 +91,13 @@ sig (** Run the given computation with modification to configuration disabled. *) val with_immutable_conf : (unit -> 'a) -> 'a + + (** Check whether the configuration has been frozen (i.e., analysis phase has started). *) + val is_frozen : unit -> bool + + (** Freeze the configuration, permanently preventing further modifications. + Should be called after all configuration setup (including autotuner) is complete and before analysis starts. *) + val freeze : unit -> unit end (** The implementation of the [gobConfig] module. *) @@ -245,6 +252,16 @@ struct let is_immutable () = !immutable + (** (Global) flag indicating that the configuration has been frozen for the analysis phase. *) + let frozen = ref false + + let is_frozen () = !frozen + + (** Freeze the configuration, permanently preventing further modifications. *) + let freeze () = + frozen := true; + set_immutable true + let with_immutable_conf f = (* allow nesting *) if is_immutable () then f () diff --git a/src/goblint.ml b/src/goblint.ml index c74bf7f17c..747661f5f9 100644 --- a/src/goblint.ml +++ b/src/goblint.ml @@ -66,6 +66,7 @@ let main () = AutoSoundConfig.activateLongjmpAnalysesWhenRequired (); if get_string "ana.specification" <> "" then AutoSoundConfig.enableAnalysesForSpecification (); if get_bool "ana.autotune.enabled" then AutoTune.chooseConfig file; + GobConfig.freeze (); file |> do_analyze changeInfo; do_gobview file; do_stats (); From c9e3fdcbe106cc6e433ca18faef99f59ddfecd83 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 12 Apr 2026 15:22:13 +0000 Subject: [PATCH 3/5] Add get_*_analysis functions and UsedForAnalysis exception for timing-error detection Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/1ccb990f-d34c-4830-a4fe-3127d58dabd4 Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> --- src/config/gobConfig.ml | 50 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 49 insertions(+), 1 deletion(-) diff --git a/src/config/gobConfig.ml b/src/config/gobConfig.ml index 97821e38b6..dd9ed33a44 100644 --- a/src/config/gobConfig.ml +++ b/src/config/gobConfig.ml @@ -98,6 +98,21 @@ sig (** Freeze the configuration, permanently preventing further modifications. Should be called after all configuration setup (including autotuner) is complete and before analysis starts. *) val freeze : unit -> unit + + (** Raised when [set_*] is called on a config key that was already read via [get_*_analysis]. *) + exception UsedForAnalysis of string + + (** Functions to query conf variables for use during analysis. + Records the accessed path so that any subsequent [set_*] call for that path raises [UsedForAnalysis]. *) + val get_int_analysis : string -> int + val get_bool_analysis : string -> bool + val get_string_analysis : string -> string + val get_list_analysis : string -> Yojson.Safe.t list + val get_string_list_analysis : string -> string list + + (** Clear the set of paths that have been read via [get_*_analysis]. + Should be called between analysis runs in server mode so that new [set_*] calls succeed. *) + val clear_analysis_reads : unit -> unit end (** The implementation of the [gobConfig] module. *) @@ -262,12 +277,29 @@ struct frozen := true; set_immutable true + (** Set of config paths (trimmed strings) that have been read via [get_*_analysis]. + If any of these paths are subsequently modified via [set_*], [UsedForAnalysis] is raised. *) + let analysis_reads : (string, unit) Hashtbl.t = Hashtbl.create 17 + + exception UsedForAnalysis of string + + let () = Printexc.register_printer @@ + function + | UsedForAnalysis st -> + Some (Printf.sprintf "GobConfig: config key '%s' was already read for analysis but is being modified; this is a configuration timing error" st) + | _ -> None + + let clear_analysis_reads () = Hashtbl.clear analysis_reads + let with_immutable_conf f = (* allow nesting *) if is_immutable () then f () else ( set_immutable true; - Fun.protect ~finally:(fun () -> set_immutable false) f + Fun.protect ~finally:(fun () -> + set_immutable false; + clear_analysis_reads () + ) f ) (** The main function to write new values into the conf. Use [set_value] to properly invalidate cache and check immutability. @@ -363,6 +395,19 @@ struct let get_list = wrap_get memo_list.get let get_string_list = List.map Yojson.Safe.Util.to_string % get_list + (** Getter wrapper for analysis-phase reads. + Records the accessed path so that any subsequent [set_*] to that path raises [UsedForAnalysis]. *) + let wrap_get_analysis f x = + let x' = String.trim x in + Hashtbl.replace analysis_reads x' (); + f x + + let get_int_analysis = wrap_get_analysis get_int + let get_bool_analysis = wrap_get_analysis get_bool + let get_string_analysis = wrap_get_analysis get_string + let get_list_analysis = wrap_get_analysis get_list + let get_string_list_analysis = List.map Yojson.Safe.Util.to_string % get_list_analysis + (** Helper functions for writing values. *) (** Sets a value, preventing changes when the configuration is immutable and invalidating the cache. @@ -375,10 +420,13 @@ struct (** Helper function for writing values. Handles the tracing. @raise Failure if path couldn't be parsed. @raise Immutable + @raise UsedForAnalysis if the path was already read via [get_*_analysis] @raise TypeError @raise Invalid_argument @raise Json_encoding.Cannot_destruct *) let set_path_string st v = + let st' = String.trim st in + if Hashtbl.mem analysis_reads st' then raise (UsedForAnalysis st'); if Goblint_tracing.tracing then Goblint_tracing.trace "conf" "Setting '%s' to %a." st GobYojson.pretty v; set_value v json_conf (parse_path st) From 2fd6827470fa14bb931bc541516aac9987799aa8 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 12 Apr 2026 15:23:18 +0000 Subject: [PATCH 4/5] Use consistent hashtable init_size with comment for analysis_reads Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/1ccb990f-d34c-4830-a4fe-3127d58dabd4 Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> --- src/config/gobConfig.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/config/gobConfig.ml b/src/config/gobConfig.ml index dd9ed33a44..0dd3a85556 100644 --- a/src/config/gobConfig.ml +++ b/src/config/gobConfig.ml @@ -279,7 +279,7 @@ struct (** Set of config paths (trimmed strings) that have been read via [get_*_analysis]. If any of these paths are subsequently modified via [set_*], [UsedForAnalysis] is raised. *) - let analysis_reads : (string, unit) Hashtbl.t = Hashtbl.create 17 + let analysis_reads : (string, unit) Hashtbl.t = Hashtbl.create 5 (* uses hashtable; fine since our options are bounded *) exception UsedForAnalysis of string From e620873069c3efde494889243c308b64d7a65cab Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 12 Apr 2026 15:28:19 +0000 Subject: [PATCH 5/5] Simplify analysis-read tracking to a single bool ref instead of per-attribute hashtable Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/1445f474-579c-45c1-ae37-d8bd066195d7 Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> --- src/config/gobConfig.ml | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/src/config/gobConfig.ml b/src/config/gobConfig.ml index 0dd3a85556..9de3db2ccc 100644 --- a/src/config/gobConfig.ml +++ b/src/config/gobConfig.ml @@ -99,18 +99,18 @@ sig Should be called after all configuration setup (including autotuner) is complete and before analysis starts. *) val freeze : unit -> unit - (** Raised when [set_*] is called on a config key that was already read via [get_*_analysis]. *) + (** Raised when [set_*] is called after any [get_*_analysis] read has occurred. *) exception UsedForAnalysis of string (** Functions to query conf variables for use during analysis. - Records the accessed path so that any subsequent [set_*] call for that path raises [UsedForAnalysis]. *) + Once called, any subsequent [set_*] call raises [UsedForAnalysis]. *) val get_int_analysis : string -> int val get_bool_analysis : string -> bool val get_string_analysis : string -> string val get_list_analysis : string -> Yojson.Safe.t list val get_string_list_analysis : string -> string list - (** Clear the set of paths that have been read via [get_*_analysis]. + (** Clear the analysis-read flag. Should be called between analysis runs in server mode so that new [set_*] calls succeed. *) val clear_analysis_reads : unit -> unit end @@ -277,19 +277,19 @@ struct frozen := true; set_immutable true - (** Set of config paths (trimmed strings) that have been read via [get_*_analysis]. - If any of these paths are subsequently modified via [set_*], [UsedForAnalysis] is raised. *) - let analysis_reads : (string, unit) Hashtbl.t = Hashtbl.create 5 (* uses hashtable; fine since our options are bounded *) + (** Flag indicating that some config value has been read for analysis. + Once set, any [set_*] call raises [UsedForAnalysis]. *) + let analysis_read = ref false exception UsedForAnalysis of string let () = Printexc.register_printer @@ function | UsedForAnalysis st -> - Some (Printf.sprintf "GobConfig: config key '%s' was already read for analysis but is being modified; this is a configuration timing error" st) + Some (Printf.sprintf "GobConfig: config key '%s' is being modified after analysis-phase reads have occurred; this is a configuration timing error" st) | _ -> None - let clear_analysis_reads () = Hashtbl.clear analysis_reads + let clear_analysis_reads () = analysis_read := false let with_immutable_conf f = (* allow nesting *) @@ -396,10 +396,9 @@ struct let get_string_list = List.map Yojson.Safe.Util.to_string % get_list (** Getter wrapper for analysis-phase reads. - Records the accessed path so that any subsequent [set_*] to that path raises [UsedForAnalysis]. *) + Sets the analysis-read flag so that any subsequent [set_*] raises [UsedForAnalysis]. *) let wrap_get_analysis f x = - let x' = String.trim x in - Hashtbl.replace analysis_reads x' (); + analysis_read := true; f x let get_int_analysis = wrap_get_analysis get_int @@ -420,13 +419,12 @@ struct (** Helper function for writing values. Handles the tracing. @raise Failure if path couldn't be parsed. @raise Immutable - @raise UsedForAnalysis if the path was already read via [get_*_analysis] + @raise UsedForAnalysis if any [get_*_analysis] call has occurred @raise TypeError @raise Invalid_argument @raise Json_encoding.Cannot_destruct *) let set_path_string st v = - let st' = String.trim st in - if Hashtbl.mem analysis_reads st' then raise (UsedForAnalysis st'); + if !analysis_read then raise (UsedForAnalysis st); if Goblint_tracing.tracing then Goblint_tracing.trace "conf" "Setting '%s' to %a." st GobYojson.pretty v; set_value v json_conf (parse_path st)