Port tutorial analyses to SimplifiedSpec and reuse SimplifiedUnitAnalysis defaults while preserving unitAnalysis compatibility

[Copilot]

This PR ports tutorial analyses to the SimplifiedSpec interface while preserving compatibility for analyses that depend on UnitAnalysis.Spec.

In addition, based on review feedback, it introduces reusable default transfer-function behavior in SimplifiedUnitAnalysis and applies it where feasible to reduce boilerplate in tutorial analyses.

What changed

• Kept unitAnalysis.ml in its original MCPSpec-compatible form.
• Added a separate simplified tutorial analysis (simplifiedUnitAnalysis.ml) and exported it from src/goblint_lib.ml.
• Introduced SimplifiedUnitAnalysis.DefaultSpec for shared no-op/default simplified transfer functions.
• Updated tutorial signs analyses to include SimplifiedUnitAnalysis.DefaultSpec where feasible:
  • src/analyses/tutorials/signs.ml
  • src/analyses/tutorials/solution/signsSol.ml
  • src/analyses/tutorials/solution/signsExtendSol.ml
• Kept analysis-specific behavior explicit where semantics differ (e.g., context, threadenter).

Validation

• Attempted make native in this environment (blocked by missing opam/dune).
• Ran final parallel validation:
  • Code Review: no remaining findings.
  • CodeQL: no analyzable-language findings for these changes.

[michael-schwarz]

@copilot: Modules missing from src/goblint_lib.ml: {'SimplifiedUnitAnalysis'}

[Copilot]

@copilot: Modules missing from src/goblint_lib.ml: {'SimplifiedUnitAnalysis'}

Fixed in 812244e by adding module SimplifiedUnitAnalysis = SimplifiedUnitAnalysis to /home/runner/work/analyzer/analyzer/src/goblint_lib.ml.

[michael-schwarz]

The SimplifiedUnitAnalysis should be used to reduce boilerplate in the other analyses.

[Copilot]

@copilot: Modules missing from src/goblint_lib.ml: {'SimplifiedUnitAnalysis'}

This is already addressed in commit 812244e: module SimplifiedUnitAnalysis = SimplifiedUnitAnalysis is exported from /home/runner/work/analyzer/analyzer/src/goblint_lib.ml.

[michael-schwarz]

@copilot: The tutorial analysis should, where feasible, not define everything from scratch but build on the SimplifiedUnitAnalysis.

[michael-schwarz]

Should be squashed once the time to merge comes.

[Copilot]

Pull request overview

Copilot reviewed 8 out of 8 changed files in this pull request and generated 1 comment.

[michael-schwarz]

If there's anything blocking this, let me know @sim642!

[Copilot]

Pull request overview

Copilot reviewed 8 out of 8 changed files in this pull request and generated no new comments.

[michael-schwarz]

Closed by mistake

[sim642]

I'll try to have a closer look at this next week.

I quickly noticed one thing: this changes a bunch of unused arguments to _ instead. I'm a bit skeptical about that because it doesn't make anything clearer, especially to newcomers who might wonder why a function takes three unused arguments or what they might be. I think OCaml LSP wouldn't even be able to show their types on hover.

Ideally, some of the transfer function arguments might be better with labels to make their order less sensitive, but now is probably not the best time to try such change anyway. Especially because this might introduce unnecessary and annoying conflicts with various architectural additions (e.g. backward constraints and forward-propagating constraints changes).

[michael-schwarz]

@copilot: don't change unused arguments to _ here.

[Copilot]

@copilot: don't change unused arguments to _ here.

Fixed in the latest commit: all _ standalone argument names have been replaced with descriptive names (man, state/caller_state, lval, f, args, callee_local, etc.) across simplifiedUnitAnalysis.ml, constants.ml, taint.ml, signs.ml, and all solution files. The ignore calls that were added as workarounds have also been removed.