[PATCH] c++: Implement P1494 and P3641 Partial program correctness [PR119060].

Jason Merrill jason@redhat.com
Thu Oct 9 16:04:10 GMT 2025


On 10/8/25 7:47 PM, Iain Sandoe wrote:
> 
> 
>> On 8 Oct 2025, at 16:57, Jason Merrill <jason@redhat.com> wrote:
>>
>> On 10/8/25 4:11 PM, Iain Sandoe wrote:
>>>> On 8 Oct 2025, at 16:04, Jason Merrill <jason@redhat.com> wrote:
>>>>
>>>> On 10/8/25 3:08 PM, Iain Sandoe wrote:
>>>>>>> Otherwise, I’m looking for guidance on what’s needed to land this.
>>>>>> IIRC the paper talks about a call to an unknown function having the desired semantics.  I’ll go with that, making it not throwing, const but looping and leaf.  We can make it stronger if necessary, weakening it after people rely on semantics is less useful IMO.  On RTL we have nothing at all, I’ve heard ,volatile‘ asm is only about missing outputs, not side effects in general.  So I’d expand to nothing on RTL, watching what breaks.
>>>>> with a follow up to a query
>>>>>> I suggest to remove the assert or replace it with one that checks that if ECF_LOOPING_CONST_OR_PURE is set the function is either ECF_CONST or ECF_PURE.
>>>>> Done and re-tested on x86_64-darwin24 and powerpc64le-linux, OK for trunk now?
>>>>> thanks
>>>>> Iain
>>>>> --- 8< ---
>>>>> P1494 provides a mechanism that serves to demarc epochs within the code
>>>>> preventing UB-based optimisations from 'time traveling' across such
>>>>> boundaries.  The additional paper, P3641, alters the name of the function
>>>>> to 'observable_checkpoint' which is the name used here.
>>>>> This implementation  maintains the observable function call through to
>>>>> expand, where it produces no code.
>>>>> PR c++/119060
>>>>> gcc/ChangeLog:
>>>>> * builtins.cc (expand_builtin): Handle BUILT_IN_OBSERVABLE_CHKPT.
>>>>> * builtins.def (BUILT_IN_OBSERVABLE_CHKPT): New.
>>>>> * tree.cc (build_common_builtin_nodes): Build observable
>>>>> checkpoint builtin.
>>>>> gcc/cp/ChangeLog:
>>>>> * cp-gimplify.cc (cp_fold): Handle std::observable_checkpoint
>>>>> specially, lowering it to the builtin.
>>>>> * cxxapi-data.csv: Add observable_checkpoint to <utility>.
>>>>> * std-name-hint.gperf: Add observable_checkpoint to <utility>.
>>>>> * std-name-hint.h: Regenerate.
>>>>> gcc/testsuite/ChangeLog:
>>>>> * g++.dg/cpp26/observable-checkpoint.C: New test.
>>>>> Signed-off-by: Iain Sandoe <iain@sandoe.co.uk>
>>>>> ---
>>>>>   gcc/builtins.cc                               |   4 +
>>>>>   gcc/builtins.def                              |   1 +
>>>>>   gcc/cp/cp-gimplify.cc                         |  16 ++
>>>>>   gcc/cp/cxxapi-data.csv                        |   1 +
>>>>>   gcc/cp/std-name-hint.gperf                    |   1 +
>>>>>   gcc/cp/std-name-hint.h                        | 142 +++++++++---------
>>>>>   .../g++.dg/cpp26/observable-checkpoint.C      |  25 +++
>>>>>   gcc/tree.cc                                   |   9 +-
>>>>>   8 files changed, 128 insertions(+), 71 deletions(-)
>>>>>   create mode 100644 gcc/testsuite/g++.dg/cpp26/observable-checkpoint.C
>>>>> diff --git a/gcc/builtins.cc b/gcc/builtins.cc
>>>>> index 78b561529f5..fb294ce58cd 100644
>>>>> --- a/gcc/builtins.cc
>>>>> +++ b/gcc/builtins.cc
>>>>> @@ -8427,6 +8427,10 @@ expand_builtin (tree exp, rtx target, rtx subtarget, machine_mode mode,
>>>>>         expand_builtin_unreachable ();
>>>>>         return const0_rtx;
>>>>>   +    case BUILT_IN_OBSERVABLE_CHKPT:
>>>>> +      /* Generate no code.  */
>>>>> +      return const0_rtx;
>>>>> +
>>>>>       CASE_FLT_FN (BUILT_IN_SIGNBIT):
>>>>>       case BUILT_IN_SIGNBITD32:
>>>>>       case BUILT_IN_SIGNBITD64:
>>>>> diff --git a/gcc/builtins.def b/gcc/builtins.def
>>>>> index 3dc2333c6f2..7cd5353bcb1 100644
>>>>> --- a/gcc/builtins.def
>>>>> +++ b/gcc/builtins.def
>>>>> @@ -1142,6 +1142,7 @@ DEF_C2Y_BUILTIN        (BUILT_IN_ULABS, "ulabs", BT_FN_ULONG_LONG, ATTR_CONST_NO
>>>>>   DEF_C2Y_BUILTIN        (BUILT_IN_ULLABS, "ullabs", BT_FN_ULONGLONG_LONGLONG, ATTR_CONST_NOTHROW_LEAF_LIST)
>>>>>   DEF_GCC_BUILTIN        (BUILT_IN_UNREACHABLE_TRAP, "unreachable trap", BT_FN_VOID, ATTR_CONST_NORETURN_NOTHROW_LEAF_COLD_LIST)
>>>>>   DEF_GCC_BUILTIN        (BUILT_IN_UNREACHABLE, "unreachable", BT_FN_VOID, ATTR_CONST_NORETURN_NOTHROW_LEAF_COLD_LIST)
>>>>> +DEF_GCC_BUILTIN        (BUILT_IN_OBSERVABLE_CHKPT, "observable_checkpoint", BT_FN_VOID, ATTR_NOTHROW_LEAF_LIST)
>>>>>   DEF_GCC_BUILTIN        (BUILT_IN_UNWIND_INIT, "unwind_init", BT_FN_VOID, ATTR_NULL)
>>>>>   DEF_GCC_BUILTIN        (BUILT_IN_UPDATE_SETJMP_BUF, "update_setjmp_buf", BT_FN_VOID_PTR, ATTR_NULL)
>>>>>   DEF_GCC_BUILTIN        (BUILT_IN_VA_COPY, "va_copy", BT_FN_VOID_VALIST_REF_VALIST_ARG, ATTR_NOTHROW_LEAF_LIST)
>>>>> diff --git a/gcc/cp/cp-gimplify.cc b/gcc/cp/cp-gimplify.cc
>>>>> index 1662336e165..483d964bd62 100644
>>>>> --- a/gcc/cp/cp-gimplify.cc
>>>>> +++ b/gcc/cp/cp-gimplify.cc
>>>>> @@ -3452,6 +3452,22 @@ cp_fold (tree x, fold_flags_t flags)
>>>>>        break;
>>>>>      }
>>>>>   + /* We need to convert std::observable_checkpoint () into its equivalent
>>>>> +    builtin for correctness, but must not rely on middle-end inlining
>>>>> +    to do this; special-case it here.  */
>>>>
>>>> Why is this necessary?  If it isn't inlined, it's still a call, and we talked about an unknown call having the desired semantics.
>>> As I understand the intention of the paper, the function is not supposed to generate any code - if, for some reason, it was not inlined then it would generate a call.
>>
>> Indeed it's probably better QoI to avoid generating code,
> 
> in this instance I view it as somewhat stronger than QoI - since it’s stated in the paper as part of the general solution.
> 
>> As a practical matter, a compiler can implement std::observable efficiently as an intrinsic that counts as a possible termination, which the optimizer thus cannot remove. After optimization (including any link-time optimization), the code generator can then produce zero machine instructions for it.
>> 
> (I am not sure how one would turn that objective into normative text, but it seemed we should honour it).
> 
>> but marking the library function as always_inline should accomplish the same result?
> 
> Yes, it seems to - even with -O0 -fno-inline (the function was already so marked).
> 
> Removed that hunk and bootstrapped and tested on x86_64-darwin24 (in fact, this is much the same as the implementation we have in the contracts development branch).
> 
> OK for trunk now?

LGTM if Richi has no more comments this week.

Jason



More information about the Libstdc++ mailing list