Skip to content

Fix exp.volatiles_are_top and exp.globs_are_top being ignored by relational (Apron) analysis#1988

Draft
Copilot wants to merge 2 commits intomasterfrom
copilot/fix-volatiles-and-globs-analysis
Draft

Fix exp.volatiles_are_top and exp.globs_are_top being ignored by relational (Apron) analysis#1988
Copilot wants to merge 2 commits intomasterfrom
copilot/fix-volatiles-and-globs-analysis

Conversation

Copy link
Copy Markdown
Contributor

Copilot AI commented Apr 12, 2026

exp.volatiles_are_top (volatile/extern vars → top) and exp.globs_are_top (all globals → top) were only enforced in the base analysis (base.ml, basePriv.ml). The relational (Apron-based) analysis silently ignored these options, potentially producing unsound results when reading from volatile or extern globals.

Changes

  • src/analyses/apron/relationAnalysis.apron.ml: Extended read_global to check both options after copying a global's value into a local temporary. If the global should be top, RD.forget_vars is called on the local, making it unconstrained in the relational domain. This applies to both single-threaded and multi-threaded (privatization) paths.
extern int ext;
volatile int vol;

int main(void) {
  ext = 5;
  int x = ext;        // x must be top — ext is extern
  __goblint_check(x == 5); // UNKNOWN! (was incorrectly provable before fix)

  vol = 3;
  int y = vol;        // y must be top — vol is volatile
  __goblint_check(y == 3); // UNKNOWN! (was incorrectly provable before fix)
}
  • tests/regression/36-apron/100-volatiles-are-top.c: Regression test verifying the Apron interval analysis correctly treats volatile/extern globals as top when exp.volatiles_are_top is enabled.

Note: GobConfig.get_bool is already memoized via BatCache, so the per-call overhead is a single hashtable lookup — consistent with how these options are checked elsewhere in the codebase.

… analysis

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/e5bf9b12-a6d7-4775-9602-3b87bd4442d0

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
Copilot AI changed the title [WIP] Fix analysis recognition for exp.volatiles_are_top and exp.globs_are_top Fix exp.volatiles_are_top and exp.globs_are_top being ignored by relational (Apron) analysis Apr 12, 2026
Copilot AI requested a review from michael-schwarz April 12, 2026 07: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.

exp.volatiles_are_top and exp.globs_are_top are only considered by base analysis

2 participants