Map generic formal inputs in generated globals

[truemagic-coder]

Fixes #62.

The original approach mapped generic formal in objects during later flow analysis. That works within one compilation unit, but not when the generated contract is consumed from another unit.

This version moves the required mapping into generated-global construction, while the generic actual expression is still available. It preserves the generated proper/refined distinction through phase 2 and propagates the proper dependency to callers outside the instance.

In particular:

• generic formal in objects are mapped to the inputs of their actual expressions during global generation;
• initialized constants are projected to the package inputs that initialize them before the generated contract is serialized;
• phase 2 preserves the proper/refined pair produced by phase 1;
• callers outside the instance use the generated proper dependency while the instantiated body retains the refined view;
• ordinary explicit contracts keep their existing behavior;
• the three upstream 84__flow_generic_in_* regressions are enabled by removing their XFAIL markers;
• the generated-global behavior is documented.

Verification

The exact submitted commit was independently verified with FalseGreen against a frozen verification contract.

• clean source-bound gnat2why build passed;
• all 3 verification criteria passed;
• all 6/6 semantic checks passed;
• all three maintainer regression cases were covered;
• the expected proper/refined generic dependencies were verified;
• cross-unit Clock_Time propagation and rejection of the invalid Global => null case were verified;
• 0 errors or tool failures;
• the exact SARIF warning allowlist was retained and unknown warnings were rejected;
• verified commit: cd927c837d90c3943681601e2d2f60f5d4f99093.

The verification used a public FSF 16 source-equivalent build because current master requires a matching internal frontend. It is scoped to the criteria above and does not claim correctness outside those checks.

Assisted-by: Codex

[CLAassistant]

All committers have signed the CLA.

[andrestt]

This approach does not work in a multi-unit context. In general all implicit global dependencies should have already been computed in the global generation phase and returned by GG_Get_Globals above. See the new tests 84__flow_generic_in_cross_unit_basic and 84__flow_generic_in_cross_unit_gg for concrete examples where this approach fails.

[andrestt]

We’ve now captured this reproducer as 84__flow_generic_in_repro_gg. So this test is no longer needed.

[andrestt]

For any tests added to this issue please use the prefix 84__flow_. 84 is the number of the corresponding issue in the main repository and __flow adds suitable default handling for flow-related tests (more details can be found in testsuite/gnatprove/run-tests).

[andrestt]

This file is not needed. It is better to use the default test configuration for flow as explained in a previous comment.

Also, a no_crash test does not capture the output baseline. It is preferable to either use prove_all or do_flow that also capture the output. This is also granted by the default behavior of the testing framework.

[andrestt]

Hello @truemagic-coder

Thank you for taking the time to contribute!

The bug in this issue is subtle and requires handling in several phases of GNATprove to properly support cross-unit patterns. As also mentioned in the review comments, the patch that you provided is effective only in the analysis phase and hence can only handle cases when the generic instance and its caller are in the same compilation unit.

We have added some more complex multi-unit tests to the repository to demonstrate the issue:

• 84__flow_generic_in_cross_unit_basic a wrong explicit global contract is currently accepted.
• 84__flow_generic_in_cross_unit_gg has essentially the same code pattern, but demonstrates a wrong automatic generation of the global contract.

To properly support this pattern the global generation phase should be improved because that phase has access to the full AST of any compilation unit. The later analysis phase must rely on the results of the global generation for all the dependencies when no explicit contract is present.

[truemagic-coder]

Hi @andrestt

Thanks — I reworked this based on your feedback.

The late flow-analysis approach is gone. The fix now happens as part of generated-global construction, with phase 2 preserving and propagating the proper/refined distinction across compilation units.

I also updated the branch to current master, dropped my duplicate fixture, and switched to the upstream 84__flow_generic_in_* tests and default flow-test setup.

The three upstream regressions now pass locally with the new implementation.