Skip to content

Warn when ana.opt.hashcons is disabled but implicitly overridden, fail for Apron#1921

Open
Copilot wants to merge 10 commits intomasterfrom
copilot/warn-on-hashconsing-issues
Open

Warn when ana.opt.hashcons is disabled but implicitly overridden, fail for Apron#1921
Copilot wants to merge 10 commits intomasterfrom
copilot/warn-on-hashconsing-issues

Conversation

Copy link
Contributor

Copilot AI commented Jan 20, 2026

Plan: Warn when ana.opt.hashcons is off but hashconsing is forced on

  • Understand the issue: ana.opt.hashcons=false is overridden when exp.arg.enabled, witness.graphml.enabled, or Apron domain is on
  • Add warning logic in the general config compatibility check location
  • Remove tests (not needed per reviewer feedback)
  • Remove accidentally committed _codeql_detected_source_root file
  • Address reviewer feedback to make Apron check a fail instead of warn
  • Add usesApron flag to MCPRegistry for proper Apron detection
  • Swap order of checks (Apron fail before ARG warn)
  • Run code review and security checks

Changes made:

Added warnings/failures in check_arguments() in maingoblint.ml:

  • Failure when ana.opt.hashcons is disabled but Apron domains are activated (checked first - Apron requires hashconsing for compare operation and will crash without it)
  • Warning when ana.opt.hashcons is disabled but exp.arg.enabled is on (checked second - covers witness generation use case)
  • Checks placed alongside other config compatibility checks

Added usesApron flag to MCPRegistry:

  • Added optional ~usesApron parameter (default false) to MCPRegistry.register_analysis()
  • Added any_activated_uses_apron() function to check if any activated analysis uses Apron
  • Marked all Apron analyses (apronAnalysis, affineEqualityAnalysis, linearTwoVarEqualityAnalysis) with ~usesApron:true flag
  • This provides proper registry-based detection instead of string matching on analysis names

Kept variable refactoring in control.ml for consistency:

  • hashcons_enabled variable used throughout spec construction

Removed test files per @michael-schwarz's feedback that tests are not needed

Removed _codeql_detected_source_root file that was accidentally committed

The changes properly fail for the Apron case (which would crash) and warn for the ARG/witness case where hashconsing is implicitly enabled.

Original prompt

This section details on the original issue you should resolve

<issue_title>Warn when ana.opt.hashcons is off, but witness.graphml.enabled or exp.arg.enabled are on or an Apron domain is on</issue_title>
<issue_description>In theses cases, counterintuitively, --disable ana.opt.hashcons doesn't completely disable hashconsing, as observed by @sim642

let arg_enabled = get_bool "witness.graphml.enabled" || get_bool "exp.arg.enabled" in

(* 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 arg_enabled (module HashconsLifter)
</issue_description>

Comments on the Issue (you are @copilot in this section)

@sim642 As to the Apron domain use case (getting a totally-ordered `compare` for a type with just `equal` and `hash`), a thing to explore could also be wrapping hashconsing directly around that domain, instead of relying on some very outermost hashconsing to implement `compare` such that Goblint wouldn't crash outright.

💬 We'd love your input! Share your thoughts on Copilot coding agent in our 2 minute survey.

Copilot AI and others added 4 commits January 20, 2026 08:55
Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
Copilot AI changed the title [WIP] Add warning for conflicting configuration settings Warn when ana.opt.hashcons is disabled but implicitly overridden Jan 20, 2026
Copilot AI requested a review from michael-schwarz January 20, 2026 09:01
@michael-schwarz
Copy link
Member

@copilot this should be move to the general place where we check whether configs are compatible.

@michael-schwarz
Copy link
Member

@copilot tests for this issue are not needed.

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
Copy link
Contributor Author

Copilot AI commented Jan 20, 2026

@copilot this should be move to the general place where we check whether configs are compatible.

Done! Moved the warnings to check_arguments() in maingoblint.ml where other config compatibility checks are performed. See commit 88c9ac6.

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
Copy link
Contributor Author

Copilot AI commented Jan 20, 2026

@copilot tests for this issue are not needed.

Removed the test files. See commit daa36fb.

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
@michael-schwarz michael-schwarz marked this pull request as ready for review January 21, 2026 01:14
- Add usesApron flag to MCPRegistry.spec_modules
- Add optional ~usesApron parameter to register_analysis (default false)
- Add any_activated_uses_apron() function to check registry
- Mark Apron analyses with ~usesApron:true flag
- Change warning to fail when hashcons disabled with Apron

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
Copilot AI changed the title Warn when ana.opt.hashcons is disabled but implicitly overridden Warn when ana.opt.hashcons is disabled but implicitly overridden, fail for Apron Mar 6, 2026
Copilot AI requested a review from michael-schwarz March 6, 2026 09:03
Check Apron first (fail) before ARG (warn) since fail is more severe

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
@michael-schwarz michael-schwarz requested a review from sim642 March 6, 2026 09:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Warn when ana.opt.hashcons is off, but witness.graphml.enabled or exp.arg.enabled are on or an Apron domain is on

3 participants