From 4e2998ecdeb756e4cd9805e03e91143b615e32ea Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 20 Jan 2026 08:48:39 +0000 Subject: [PATCH 1/8] Initial plan From 6f83ac05876f4b9585cf5be4e5a77e3dc46d7e61 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 20 Jan 2026 08:55:57 +0000 Subject: [PATCH 2/8] Add warning when hashconsing is force-enabled Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> --- src/framework/control.ml | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/src/framework/control.ml b/src/framework/control.ml index 9085d313eb..135c5ae3cb 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -13,6 +13,8 @@ open GobConfig open Constraints open SpecLifters +module M = Messages + module type S2S = Spec2Spec (* spec is lazy, so HConsed table in Hashcons lifters is preserved between analyses in server mode *) @@ -20,6 +22,17 @@ let spec_module: (module Spec) Lazy.t = lazy ( GobConfig.building_spec := true; let arg_enabled = get_bool "exp.arg.enabled" in let termination_enabled = List.mem "termination" (get_string_list "ana.activated") in (* check if loop termination analysis is enabled*) + let apron_enabled = List.mem "apron" (get_string_list "ana.activated") in + let hashcons_enabled = get_bool "ana.opt.hashcons" in + + (* Warn if hashconsing is disabled but will be force-enabled by other settings *) + if not hashcons_enabled then ( + if arg_enabled then + M.warn_noloc "Hashconsing (ana.opt.hashcons) is disabled, but is implicitly enabled because ARG is enabled (exp.arg.enabled)"; + if apron_enabled then + M.warn_noloc "Hashconsing (ana.opt.hashcons) is disabled, but may be required for Apron domain (ana.activated includes 'apron')" + ); + (* apply functor F on module X if opt is true *) let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in let module S1 = @@ -29,7 +42,7 @@ let spec_module: (module Spec) Lazy.t = lazy ( |> lift true (module WidenContextLifterSide) (* option checked in functor *) |> lift (get_int "ana.widen.delay.local" > 0) (module WideningDelay.DLifter) (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *) - |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter) + |> lift (hashcons_enabled || arg_enabled) (module HashconsContextLifter) |> lift (get_bool "ana.opt.hashcached") (module HashCachedContextLifter) |> lift arg_enabled (module HashconsLifter) |> lift arg_enabled (module ArgConstraints.PathSensitive3) @@ -37,8 +50,8 @@ let spec_module: (module Spec) Lazy.t = lazy ( |> lift (get_bool "ana.dead-code.branches") (module DeadBranchLifter) |> lift true (module DeadCodeLifter) |> lift (get_bool "dbg.slice.on") (module LevelSliceLifter) - |> lift (get_bool "ana.opt.equal" && not (get_bool "ana.opt.hashcons")) (module OptEqual) - |> lift (get_bool "ana.opt.hashcons") (module HashconsLifter) + |> lift (get_bool "ana.opt.equal" && not hashcons_enabled) (module OptEqual) + |> lift hashcons_enabled (module HashconsLifter) (* Widening tokens must be outside of hashcons, because widening token domain ignores token sets for identity, so hashcons doesn't allow adding tokens. Also must be outside of deadcode, because deadcode splits (like mutex lock event) don't pass on tokens. *) |> lift (get_bool "ana.widen.tokens") (module WideningTokenLifter.Lifter) From a1f285de5195c95832694532bf2e620c344c49d4 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 20 Jan 2026 08:57:13 +0000 Subject: [PATCH 3/8] Add test for hashcons warning Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> --- .../00-sanity/52-hashcons-warning.c | 4 ++++ .../00-sanity/52-hashcons-warning.t | 24 +++++++++++++++++++ 2 files changed, 28 insertions(+) create mode 100644 tests/regression/00-sanity/52-hashcons-warning.c create mode 100644 tests/regression/00-sanity/52-hashcons-warning.t diff --git a/tests/regression/00-sanity/52-hashcons-warning.c b/tests/regression/00-sanity/52-hashcons-warning.c new file mode 100644 index 0000000000..b66321a558 --- /dev/null +++ b/tests/regression/00-sanity/52-hashcons-warning.c @@ -0,0 +1,4 @@ +// Test to verify warning is issued when hashconsing is disabled but ARG or Apron is enabled +int main(void) { + return 0; +} diff --git a/tests/regression/00-sanity/52-hashcons-warning.t b/tests/regression/00-sanity/52-hashcons-warning.t new file mode 100644 index 0000000000..c25763fcb0 --- /dev/null +++ b/tests/regression/00-sanity/52-hashcons-warning.t @@ -0,0 +1,24 @@ +Test that warning is issued when hashconsing is disabled but ARG is enabled: + + $ goblint --disable ana.opt.hashcons --enable exp.arg.enabled 52-hashcons-warning.c 2>&1 | grep -i "hashcons" + [Warning] Hashconsing (ana.opt.hashcons) is disabled, but is implicitly enabled because ARG is enabled (exp.arg.enabled) + +Test that warning is issued when hashconsing is disabled but Apron is enabled: + + $ goblint --disable ana.opt.hashcons --set ana.activated[+] apron 52-hashcons-warning.c 2>&1 | grep -i "hashcons" + [Warning] Hashconsing (ana.opt.hashcons) is disabled, but may be required for Apron domain (ana.activated includes 'apron') + +Test that no warning is issued when hashconsing is enabled with ARG: + + $ goblint --enable ana.opt.hashcons --enable exp.arg.enabled 52-hashcons-warning.c 2>&1 | grep -i "hashcons" + [1] + +Test that no warning is issued when hashconsing is enabled with Apron: + + $ goblint --enable ana.opt.hashcons --set ana.activated[+] apron 52-hashcons-warning.c 2>&1 | grep -i "hashcons" + [1] + +Test that no warning is issued when hashconsing is disabled without ARG or Apron: + + $ goblint --disable ana.opt.hashcons 52-hashcons-warning.c 2>&1 | grep -i "hashcons" + [1] From cffdb824483c2364322fafbad68edeb97545338e Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 20 Jan 2026 08:58:06 +0000 Subject: [PATCH 4/8] Fix missing semicolon in warning logic Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> --- src/framework/control.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/framework/control.ml b/src/framework/control.ml index 135c5ae3cb..103a5f03c2 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -30,7 +30,7 @@ let spec_module: (module Spec) Lazy.t = lazy ( if arg_enabled then M.warn_noloc "Hashconsing (ana.opt.hashcons) is disabled, but is implicitly enabled because ARG is enabled (exp.arg.enabled)"; if apron_enabled then - M.warn_noloc "Hashconsing (ana.opt.hashcons) is disabled, but may be required for Apron domain (ana.activated includes 'apron')" + M.warn_noloc "Hashconsing (ana.opt.hashcons) is disabled, but may be required for Apron domain (ana.activated includes 'apron')"; ); (* apply functor F on module X if opt is true *) From 672701929310e307bb37ac895efd7946ac4a9faf Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 20 Jan 2026 08:59:22 +0000 Subject: [PATCH 5/8] Final: Complete implementation with warnings Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> --- _codeql_detected_source_root | 1 + 1 file changed, 1 insertion(+) create mode 120000 _codeql_detected_source_root diff --git a/_codeql_detected_source_root b/_codeql_detected_source_root new file mode 120000 index 0000000000..945c9b46d6 --- /dev/null +++ b/_codeql_detected_source_root @@ -0,0 +1 @@ +. \ No newline at end of file From 88c9ac6bb68baa7985d1b70dcfc804ddef2ba06f Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 20 Jan 2026 14:49:57 +0000 Subject: [PATCH 6/8] Move hashcons warning to check_arguments in maingoblint.ml Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> --- src/framework/control.ml | 12 ------------ src/maingoblint.ml | 6 ++++++ tests/regression/00-sanity/52-hashcons-warning.t | 4 ++-- 3 files changed, 8 insertions(+), 14 deletions(-) diff --git a/src/framework/control.ml b/src/framework/control.ml index 103a5f03c2..f2bfffde2d 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -13,8 +13,6 @@ open GobConfig open Constraints open SpecLifters -module M = Messages - module type S2S = Spec2Spec (* spec is lazy, so HConsed table in Hashcons lifters is preserved between analyses in server mode *) @@ -22,17 +20,7 @@ let spec_module: (module Spec) Lazy.t = lazy ( GobConfig.building_spec := true; let arg_enabled = get_bool "exp.arg.enabled" in let termination_enabled = List.mem "termination" (get_string_list "ana.activated") in (* check if loop termination analysis is enabled*) - let apron_enabled = List.mem "apron" (get_string_list "ana.activated") in let hashcons_enabled = get_bool "ana.opt.hashcons" in - - (* Warn if hashconsing is disabled but will be force-enabled by other settings *) - if not hashcons_enabled then ( - if arg_enabled then - M.warn_noloc "Hashconsing (ana.opt.hashcons) is disabled, but is implicitly enabled because ARG is enabled (exp.arg.enabled)"; - if apron_enabled then - M.warn_noloc "Hashconsing (ana.opt.hashcons) is disabled, but may be required for Apron domain (ana.activated includes 'apron')"; - ); - (* apply functor F on module X if opt is true *) let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in let module S1 = diff --git a/src/maingoblint.ml b/src/maingoblint.ml index ee59c91c01..8cea71f5d0 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -136,6 +136,12 @@ let check_arguments () = if get_bool "ana.autotune.enabled" && get_bool "incremental.load" then (set_bool "ana.autotune.enabled" false; warn "ana.autotune.enabled implicitly disabled by incremental.load"); if get_bool "exp.basic-blocks" && not (get_bool "justcil") && List.mem "assert" @@ get_string_list "trans.activated" then (set_bool "exp.basic-blocks" false; warn "The option exp.basic-blocks implicitly disabled by activating the \"assert\" transformation."); if (not @@ get_bool "witness.invariant.all-locals") && (not @@ get_bool "cil.addNestedScopeAttr") then (set_bool "cil.addNestedScopeAttr" true; warn "Disabling witness.invariant.all-locals implicitly enables cil.addNestedScopeAttr."); + if not (get_bool "ana.opt.hashcons") then ( + if get_bool "exp.arg.enabled" then + warn "Disabling ana.opt.hashcons has no effect because hashconsing is implicitly enabled by exp.arg.enabled"; + if List.mem "apron" (get_string_list "ana.activated") then + warn "Disabling ana.opt.hashcons has no effect because hashconsing is implicitly enabled by Apron (ana.activated includes 'apron')"; + ); if List.mem "remove_dead_code" @@ get_string_list "trans.activated" then ( (* 'assert' transform happens before 'remove_dead_code' transform *) ignore @@ List.fold_left diff --git a/tests/regression/00-sanity/52-hashcons-warning.t b/tests/regression/00-sanity/52-hashcons-warning.t index c25763fcb0..dae9822008 100644 --- a/tests/regression/00-sanity/52-hashcons-warning.t +++ b/tests/regression/00-sanity/52-hashcons-warning.t @@ -1,12 +1,12 @@ Test that warning is issued when hashconsing is disabled but ARG is enabled: $ goblint --disable ana.opt.hashcons --enable exp.arg.enabled 52-hashcons-warning.c 2>&1 | grep -i "hashcons" - [Warning] Hashconsing (ana.opt.hashcons) is disabled, but is implicitly enabled because ARG is enabled (exp.arg.enabled) + [Warning] Disabling ana.opt.hashcons has no effect because hashconsing is implicitly enabled by exp.arg.enabled Test that warning is issued when hashconsing is disabled but Apron is enabled: $ goblint --disable ana.opt.hashcons --set ana.activated[+] apron 52-hashcons-warning.c 2>&1 | grep -i "hashcons" - [Warning] Hashconsing (ana.opt.hashcons) is disabled, but may be required for Apron domain (ana.activated includes 'apron') + [Warning] Disabling ana.opt.hashcons has no effect because hashconsing is implicitly enabled by Apron (ana.activated includes 'apron') Test that no warning is issued when hashconsing is enabled with ARG: From daa36fba15189ee923778ef1de406f424a92a975 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 20 Jan 2026 14:53:32 +0000 Subject: [PATCH 7/8] Remove tests as they are not needed Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> --- .../00-sanity/52-hashcons-warning.c | 4 ---- .../00-sanity/52-hashcons-warning.t | 24 ------------------- 2 files changed, 28 deletions(-) delete mode 100644 tests/regression/00-sanity/52-hashcons-warning.c delete mode 100644 tests/regression/00-sanity/52-hashcons-warning.t diff --git a/tests/regression/00-sanity/52-hashcons-warning.c b/tests/regression/00-sanity/52-hashcons-warning.c deleted file mode 100644 index b66321a558..0000000000 --- a/tests/regression/00-sanity/52-hashcons-warning.c +++ /dev/null @@ -1,4 +0,0 @@ -// Test to verify warning is issued when hashconsing is disabled but ARG or Apron is enabled -int main(void) { - return 0; -} diff --git a/tests/regression/00-sanity/52-hashcons-warning.t b/tests/regression/00-sanity/52-hashcons-warning.t deleted file mode 100644 index dae9822008..0000000000 --- a/tests/regression/00-sanity/52-hashcons-warning.t +++ /dev/null @@ -1,24 +0,0 @@ -Test that warning is issued when hashconsing is disabled but ARG is enabled: - - $ goblint --disable ana.opt.hashcons --enable exp.arg.enabled 52-hashcons-warning.c 2>&1 | grep -i "hashcons" - [Warning] Disabling ana.opt.hashcons has no effect because hashconsing is implicitly enabled by exp.arg.enabled - -Test that warning is issued when hashconsing is disabled but Apron is enabled: - - $ goblint --disable ana.opt.hashcons --set ana.activated[+] apron 52-hashcons-warning.c 2>&1 | grep -i "hashcons" - [Warning] Disabling ana.opt.hashcons has no effect because hashconsing is implicitly enabled by Apron (ana.activated includes 'apron') - -Test that no warning is issued when hashconsing is enabled with ARG: - - $ goblint --enable ana.opt.hashcons --enable exp.arg.enabled 52-hashcons-warning.c 2>&1 | grep -i "hashcons" - [1] - -Test that no warning is issued when hashconsing is enabled with Apron: - - $ goblint --enable ana.opt.hashcons --set ana.activated[+] apron 52-hashcons-warning.c 2>&1 | grep -i "hashcons" - [1] - -Test that no warning is issued when hashconsing is disabled without ARG or Apron: - - $ goblint --disable ana.opt.hashcons 52-hashcons-warning.c 2>&1 | grep -i "hashcons" - [1] From 004be4c8dc1921d52675e054bac55e1be9a8cdb3 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 20 Jan 2026 14:58:52 +0000 Subject: [PATCH 8/8] Remove _codeql_detected_source_root file Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> --- _codeql_detected_source_root | 1 - 1 file changed, 1 deletion(-) delete mode 120000 _codeql_detected_source_root diff --git a/_codeql_detected_source_root b/_codeql_detected_source_root deleted file mode 120000 index 945c9b46d6..0000000000 --- a/_codeql_detected_source_root +++ /dev/null @@ -1 +0,0 @@ -. \ No newline at end of file