[gcc(refs/users/aoliva/heads/testme)] hardcfr: add optional checkpoints [ada docs]

[gcc(refs/users/aoliva/heads/testme)] hardcfr: add optional checkpoints [ada docs]

[Alexandre Oliva]

https://gcc.gnu.org/g:97a558c10f106e3e0a10e93a27b4993a66bbe734

commit 97a558c10f106e3e0a10e93a27b4993a66bbe734
Author: Alexandre Oliva <oliva@adacore.com>
Date:   Thu Oct 6 06:58:29 2022 -0300

    hardcfr: add optional checkpoints [ada docs]
    
    Previously, control flow redundancy only checked the visited bitmap
    against the control flow graph at return points and before mandatory
    tail calls, missing various other possibilities of exiting a
    subprogram, such as by raising or propagating exceptions, and calling
    noreturn functions.  The checks inserted before returns also prevented
    potential tail-call optimizations.
    
    This incremental change introduces options to control checking at each
    of these previously-missed checkpoints.  Unless disabled, a cleanup is
    introduced to check when an exceptions escapes a subprogram.  To avoid
    disrupting sibcall optimizations, when they are enabled, checks are
    introduced before calls whose results are immediately returned,
    whether or not they are ultimately optimized.  If enabled, checks are
    introduced before noreturn calls and exception raises, or only before
    nothrow noreturn calls.
    
    Add examples of code transformations to the GNAT RM.
    
    
    for  gcc/ada/ChangeLog
    
            * doc/gnat_rm/security_hardening_features.rst: Document
            optional hardcfr checkpoints.

Diff:
---
 .../doc/gnat_rm/security_hardening_features.rst    | 126 ++++++++++++++++++++-
 1 file changed, 121 insertions(+), 5 deletions(-)

diff --git a/gcc/ada/doc/gnat_rm/security_hardening_features.rst b/gcc/ada/doc/gnat_rm/security_hardening_features.rst
index f5fdc8e46b4..4dfda486795 100644
--- a/gcc/ada/doc/gnat_rm/security_hardening_features.rst
+++ b/gcc/ada/doc/gnat_rm/security_hardening_features.rst
@@ -263,11 +263,127 @@ For each block that is marked as visited, the mechanism checks that at
 least one of its predecessors, and at least one of its successors, are
 also marked as visited.
 
-Verification is performed just before returning.  Subprogram
-executions that complete by raising or propagating an exception bypass
-verification-and-return points.  A subprogram that can only complete
-by raising or propagating an exception may have instrumentation
-disabled altogether.
+Verification is performed just before a subprogram returns.  The
+following fragment:
+
+.. code-block:: ada
+
+   if X then
+     Y := F (Z);
+     return;
+   end if;
+
+
+gets turned into:
+
+.. code-block:: ada
+
+   type Visited_Bitmap is array (1..N) of Boolean with Pack;
+   Visited : aliased Visited_Bitmap := (others => False);
+   --  Bitmap of visited blocks.  N is the basic block count.
+   [...]
+   --  Basic block #I
+   Visited(I) := True;
+   if X then
+     --  Basic block #J
+     Visited(J) := True;
+     Y := F (Z);
+     CFR.Check (N, Visited'Access, CFG'Access);
+     --  CFR is a hypothetical package whose Check procedure calls
+     --  libgcc's __hardcfr_check, that traps if the Visited bitmap
+     --  does not hold a valid path in CFG, the run-time
+     --  representation of the control flow graph in the enclosing
+     --  subprogram.
+     return;
+   end if;
+   --  Basic block #K
+   Visited(K) := True;
+
+
+Verification would also be performed before must-tail calls, and
+before early-marked potential tail calls, but these do not occur in
+practice, as potential tail-calls are only detected in late
+optimization phases, too late for this transformation to act on it.
+
+In order to avoid adding verification after potential tail calls,
+which would prevent tail-call optimization, we recognize returning
+calls, i.e., calls whose result, if any, is returned by the calling
+subprogram to its caller immediately after the call returns.
+Verification is performed before such calls, whether or not they are
+ultimately optimized to tail calls.  This behavior is enabled by
+default whenever sibcall optimization is enabled (see
+:switch:`-foptimize-sibling-calls`); it may be disabled with
+:switch:`-fno-hardcfr-check-returning-calls`, or enabled with
+:switch:`-fhardcfr-check-returning-calls`, regardless of the
+optimization, but the lack of other optimizations may prevent calls
+from being recognized as returning calls:
+
+.. code-block:: ada
+
+     --  CFR.Check here, with -fhardcfr-check-returning-calls.
+     P (X);
+     --  CFR.Check here, with -fno-hardcfr-check-returning-calls.
+     return;
+
+or:
+
+.. code-block:: ada
+
+     --  CFR.Check here, with -fhardcfr-check-returning-calls.
+     R := F (X);
+     --  CFR.Check here, with -fno-hardcfr-check-returning-calls.
+     return R;
+
+
+Any subprogram from which an exception may escape, i.e., that may
+raise or propagate an exception that isn't handled internally, is
+conceptually enclosed by a cleanup handler that performs verification,
+unless this is disabled with :switch:`-fno-hardcfr-check-exceptions`.
+With this feature enabled, a subprogram body containing:
+
+.. code-block:: ada
+
+     --  ...
+       Y := F (X);  -- May raise exceptions.
+     --  ...
+       raise E;  -- Not handled internally.
+     --  ...
+
+
+gets modified as follows:
+
+.. code-block:: ada
+
+   begin
+     --  ...
+       Y := F (X);  -- May raise exceptions.
+     --  ...
+       raise E;  -- Not handled internally.
+     --  ...
+   exception
+     when others =>
+       CFR.Check (N, Visited'Access, CFG'Access);
+       raise;
+   end;
+
+
+Verification may also be performed before No_Return calls, whether
+only nothrow ones, with
+:switch:`-fhardcfr-check-noreturn-calls=nothrow`, or all of them, with
+:switch:`-fhardcfr-check-noreturn-calls=always`.  The default is
+:switch:`-fhardcfr-check-noreturn-calls=never` for this feature, that
+disables checking before No_Return calls.
+
+When a No_Return call returns control to its caller through an
+exception, verification may have already been performed before the
+call, if :switch:`-fhardcfr-check-noreturn-calls=always` is in effect.
+The compiler arranges for already-checked No_Return calls without a
+preexisting handler to bypass the implicitly-added cleanup handler and
+thus the redundant check, but a local exception or cleanup handler, if
+present, will modify the set of visited blocks, and checking will take
+place again when the caller reaches the next verification point,
+whether it is a return or reraise statement after the exception is
+otherwise handled, or even another No_Return call.
 
 The instrumentation for hardening with control flow redundancy can be
 observed in dump files generated by the command-line option

[gcc(refs/users/aoliva/heads/testme)] hardcfr: add optional checkpoints [ada docs]

[Alexandre Oliva]

https://gcc.gnu.org/g:c66ec1a0792b659633ac071693791a87842a0dae

commit c66ec1a0792b659633ac071693791a87842a0dae
Author: Alexandre Oliva <oliva@adacore.com>
Date:   Thu Jun 8 01:34:59 2023 -0300

    hardcfr: add optional checkpoints [ada docs]
    
    Previously, control flow redundancy only checked the visited bitmap
    against the control flow graph at return points and before mandatory
    tail calls, missing various other possibilities of exiting a
    subprogram, such as by raising or propagating exceptions, and calling
    noreturn functions.  The checks inserted before returns also prevented
    potential tail-call optimizations.
    
    This incremental change introduces options to control checking at each
    of these previously-missed checkpoints.  Unless disabled, a cleanup is
    introduced to check when an exceptions escapes a subprogram.  To avoid
    disrupting sibcall optimizations, when they are enabled, checks are
    introduced before calls whose results are immediately returned,
    whether or not they are ultimately optimized.  If enabled, checks are
    introduced before noreturn calls and exception raises, or only before
    nothrow noreturn calls.
    
    Add examples of code transformations to the GNAT RM.
    
    
    for  gcc/ada/ChangeLog
    
            * doc/gnat_rm/security_hardening_features.rst: Document
            optional hardcfr checkpoints.

Diff:

[gcc(refs/users/aoliva/heads/testme)] hardcfr: add optional checkpoints [ada docs]

[Alexandre Oliva]

https://gcc.gnu.org/g:440aa02e69cbda5ad34faddbde72ec5db6be1150

commit 440aa02e69cbda5ad34faddbde72ec5db6be1150
Author: Alexandre Oliva <oliva@adacore.com>
Date:   Wed Oct 19 20:36:17 2022 -0300

    hardcfr: add optional checkpoints [ada docs]
    
    Previously, control flow redundancy only checked the visited bitmap
    against the control flow graph at return points and before mandatory
    tail calls, missing various other possibilities of exiting a
    subprogram, such as by raising or propagating exceptions, and calling
    noreturn functions.  The checks inserted before returns also prevented
    potential tail-call optimizations.
    
    This incremental change introduces options to control checking at each
    of these previously-missed checkpoints.  Unless disabled, a cleanup is
    introduced to check when an exceptions escapes a subprogram.  To avoid
    disrupting sibcall optimizations, when they are enabled, checks are
    introduced before calls whose results are immediately returned,
    whether or not they are ultimately optimized.  If enabled, checks are
    introduced before noreturn calls and exception raises, or only before
    nothrow noreturn calls.
    
    Add examples of code transformations to the GNAT RM.
    
    
    for  gcc/ada/ChangeLog
    
            * doc/gnat_rm/security_hardening_features.rst: Document
            optional hardcfr checkpoints.

Diff:

[gcc(refs/users/aoliva/heads/testme)] hardcfr: add optional checkpoints [ada docs]

[Alexandre Oliva]

https://gcc.gnu.org/g:d2dab2c197309539d2e8891eb860015fceea556d

commit d2dab2c197309539d2e8891eb860015fceea556d
Author: Alexandre Oliva <oliva@adacore.com>
Date:   Thu Jun 8 01:34:59 2023 -0300

    hardcfr: add optional checkpoints [ada docs]
    
    Previously, control flow redundancy only checked the visited bitmap
    against the control flow graph at return points and before mandatory
    tail calls, missing various other possibilities of exiting a
    subprogram, such as by raising or propagating exceptions, and calling
    noreturn functions.  The checks inserted before returns also prevented
    potential tail-call optimizations.
    
    This incremental change introduces options to control checking at each
    of these previously-missed checkpoints.  Unless disabled, a cleanup is
    introduced to check when an exceptions escapes a subprogram.  To avoid
    disrupting sibcall optimizations, when they are enabled, checks are
    introduced before calls whose results are immediately returned,
    whether or not they are ultimately optimized.  If enabled, checks are
    introduced before noreturn calls and exception raises, or only before
    nothrow noreturn calls.
    
    Add examples of code transformations to the GNAT RM.
    
    
    for  gcc/ada/ChangeLog
    
            * doc/gnat_rm/security_hardening_features.rst: Document
            optional hardcfr checkpoints.

Diff:

[gcc(refs/users/aoliva/heads/testme)] hardcfr: add optional checkpoints [ada docs]

[Alexandre Oliva]

https://gcc.gnu.org/g:440aa02e69cbda5ad34faddbde72ec5db6be1150

commit 440aa02e69cbda5ad34faddbde72ec5db6be1150
Author: Alexandre Oliva <oliva@adacore.com>
Date:   Wed Oct 19 20:36:17 2022 -0300

    hardcfr: add optional checkpoints [ada docs]
    
    Previously, control flow redundancy only checked the visited bitmap
    against the control flow graph at return points and before mandatory
    tail calls, missing various other possibilities of exiting a
    subprogram, such as by raising or propagating exceptions, and calling
    noreturn functions.  The checks inserted before returns also prevented
    potential tail-call optimizations.
    
    This incremental change introduces options to control checking at each
    of these previously-missed checkpoints.  Unless disabled, a cleanup is
    introduced to check when an exceptions escapes a subprogram.  To avoid
    disrupting sibcall optimizations, when they are enabled, checks are
    introduced before calls whose results are immediately returned,
    whether or not they are ultimately optimized.  If enabled, checks are
    introduced before noreturn calls and exception raises, or only before
    nothrow noreturn calls.
    
    Add examples of code transformations to the GNAT RM.
    
    
    for  gcc/ada/ChangeLog
    
            * doc/gnat_rm/security_hardening_features.rst: Document
            optional hardcfr checkpoints.

Diff:

[gcc(refs/users/aoliva/heads/testme)] hardcfr: add optional checkpoints [ada docs]

[Alexandre Oliva]

https://gcc.gnu.org/g:5667c51ab286acf16b9e7bc67232514b614c0c68

commit 5667c51ab286acf16b9e7bc67232514b614c0c68
Author: Alexandre Oliva <oliva@adacore.com>
Date:   Wed Oct 19 20:36:17 2022 -0300

    hardcfr: add optional checkpoints [ada docs]
    
    Previously, control flow redundancy only checked the visited bitmap
    against the control flow graph at return points and before mandatory
    tail calls, missing various other possibilities of exiting a
    subprogram, such as by raising or propagating exceptions, and calling
    noreturn functions.  The checks inserted before returns also prevented
    potential tail-call optimizations.
    
    This incremental change introduces options to control checking at each
    of these previously-missed checkpoints.  Unless disabled, a cleanup is
    introduced to check when an exceptions escapes a subprogram.  To avoid
    disrupting sibcall optimizations, when they are enabled, checks are
    introduced before calls whose results are immediately returned,
    whether or not they are ultimately optimized.  If enabled, checks are
    introduced before noreturn calls and exception raises, or only before
    nothrow noreturn calls.
    
    Add examples of code transformations to the GNAT RM.
    
    
    for  gcc/ada/ChangeLog
    
            * doc/gnat_rm/security_hardening_features.rst: Document
            optional hardcfr checkpoints.

Diff:

[gcc(refs/users/aoliva/heads/testme)] hardcfr: add optional checkpoints [ada docs]

[Alexandre Oliva]

https://gcc.gnu.org/g:c5efc3d0255a49f7ba43060dce55ee716eaaf311

commit c5efc3d0255a49f7ba43060dce55ee716eaaf311
Author: Alexandre Oliva <oliva@adacore.com>
Date:   Wed Oct 19 20:36:17 2022 -0300

    hardcfr: add optional checkpoints [ada docs]
    
    Previously, control flow redundancy only checked the visited bitmap
    against the control flow graph at return points and before mandatory
    tail calls, missing various other possibilities of exiting a
    subprogram, such as by raising or propagating exceptions, and calling
    noreturn functions.  The checks inserted before returns also prevented
    potential tail-call optimizations.
    
    This incremental change introduces options to control checking at each
    of these previously-missed checkpoints.  Unless disabled, a cleanup is
    introduced to check when an exceptions escapes a subprogram.  To avoid
    disrupting sibcall optimizations, when they are enabled, checks are
    introduced before calls whose results are immediately returned,
    whether or not they are ultimately optimized.  If enabled, checks are
    introduced before noreturn calls and exception raises, or only before
    nothrow noreturn calls.
    
    Add examples of code transformations to the GNAT RM.
    
    
    for  gcc/ada/ChangeLog
    
            * doc/gnat_rm/security_hardening_features.rst: Document
            optional hardcfr checkpoints.

Diff:
---
 .../doc/gnat_rm/security_hardening_features.rst    | 126 ++++++++++++++++++++-
 1 file changed, 121 insertions(+), 5 deletions(-)

diff --git a/gcc/ada/doc/gnat_rm/security_hardening_features.rst b/gcc/ada/doc/gnat_rm/security_hardening_features.rst
index d7c02b94f36..08cfaaf0f79 100644
--- a/gcc/ada/doc/gnat_rm/security_hardening_features.rst
+++ b/gcc/ada/doc/gnat_rm/security_hardening_features.rst
@@ -383,11 +383,127 @@ For each block that is marked as visited, the mechanism checks that at
 least one of its predecessors, and at least one of its successors, are
 also marked as visited.
 
-Verification is performed just before returning.  Subprogram
-executions that complete by raising or propagating an exception bypass
-verification-and-return points.  A subprogram that can only complete
-by raising or propagating an exception may have instrumentation
-disabled altogether.
+Verification is performed just before a subprogram returns.  The
+following fragment:
+
+.. code-block:: ada
+
+   if X then
+     Y := F (Z);
+     return;
+   end if;
+
+
+gets turned into:
+
+.. code-block:: ada
+
+   type Visited_Bitmap is array (1..N) of Boolean with Pack;
+   Visited : aliased Visited_Bitmap := (others => False);
+   --  Bitmap of visited blocks.  N is the basic block count.
+   [...]
+   --  Basic block #I
+   Visited(I) := True;
+   if X then
+     --  Basic block #J
+     Visited(J) := True;
+     Y := F (Z);
+     CFR.Check (N, Visited'Access, CFG'Access);
+     --  CFR is a hypothetical package whose Check procedure calls
+     --  libgcc's __hardcfr_check, that traps if the Visited bitmap
+     --  does not hold a valid path in CFG, the run-time
+     --  representation of the control flow graph in the enclosing
+     --  subprogram.
+     return;
+   end if;
+   --  Basic block #K
+   Visited(K) := True;
+
+
+Verification would also be performed before must-tail calls, and
+before early-marked potential tail calls, but these do not occur in
+practice, as potential tail-calls are only detected in late
+optimization phases, too late for this transformation to act on it.
+
+In order to avoid adding verification after potential tail calls,
+which would prevent tail-call optimization, we recognize returning
+calls, i.e., calls whose result, if any, is returned by the calling
+subprogram to its caller immediately after the call returns.
+Verification is performed before such calls, whether or not they are
+ultimately optimized to tail calls.  This behavior is enabled by
+default whenever sibcall optimization is enabled (see
+:switch:`-foptimize-sibling-calls`); it may be disabled with
+:switch:`-fno-hardcfr-check-returning-calls`, or enabled with
+:switch:`-fhardcfr-check-returning-calls`, regardless of the
+optimization, but the lack of other optimizations may prevent calls
+from being recognized as returning calls:
+
+.. code-block:: ada
+
+     --  CFR.Check here, with -fhardcfr-check-returning-calls.
+     P (X);
+     --  CFR.Check here, with -fno-hardcfr-check-returning-calls.
+     return;
+
+or:
+
+.. code-block:: ada
+
+     --  CFR.Check here, with -fhardcfr-check-returning-calls.
+     R := F (X);
+     --  CFR.Check here, with -fno-hardcfr-check-returning-calls.
+     return R;
+
+
+Any subprogram from which an exception may escape, i.e., that may
+raise or propagate an exception that isn't handled internally, is
+conceptually enclosed by a cleanup handler that performs verification,
+unless this is disabled with :switch:`-fno-hardcfr-check-exceptions`.
+With this feature enabled, a subprogram body containing:
+
+.. code-block:: ada
+
+     --  ...
+       Y := F (X);  -- May raise exceptions.
+     --  ...
+       raise E;  -- Not handled internally.
+     --  ...
+
+
+gets modified as follows:
+
+.. code-block:: ada
+
+   begin
+     --  ...
+       Y := F (X);  -- May raise exceptions.
+     --  ...
+       raise E;  -- Not handled internally.
+     --  ...
+   exception
+     when others =>
+       CFR.Check (N, Visited'Access, CFG'Access);
+       raise;
+   end;
+
+
+Verification may also be performed before No_Return calls, whether
+only nothrow ones, with
+:switch:`-fhardcfr-check-noreturn-calls=nothrow`, or all of them, with
+:switch:`-fhardcfr-check-noreturn-calls=always`.  The default is
+:switch:`-fhardcfr-check-noreturn-calls=never` for this feature, that
+disables checking before No_Return calls.
+
+When a No_Return call returns control to its caller through an
+exception, verification may have already been performed before the
+call, if :switch:`-fhardcfr-check-noreturn-calls=always` is in effect.
+The compiler arranges for already-checked No_Return calls without a
+preexisting handler to bypass the implicitly-added cleanup handler and
+thus the redundant check, but a local exception or cleanup handler, if
+present, will modify the set of visited blocks, and checking will take
+place again when the caller reaches the next verification point,
+whether it is a return or reraise statement after the exception is
+otherwise handled, or even another No_Return call.
 
 The instrumentation for hardening with control flow redundancy can be
 observed in dump files generated by the command-line option

[gcc(refs/users/aoliva/heads/testme)] hardcfr: add optional checkpoints [ada docs]

[Alexandre Oliva]

https://gcc.gnu.org/g:1cdf09939f7dc22f469c71be701af3504f3849d7

commit 1cdf09939f7dc22f469c71be701af3504f3849d7
Author: Alexandre Oliva <oliva@adacore.com>
Date:   Wed Oct 19 20:36:17 2022 -0300

    hardcfr: add optional checkpoints [ada docs]
    
    Previously, control flow redundancy only checked the visited bitmap
    against the control flow graph at return points and before mandatory
    tail calls, missing various other possibilities of exiting a
    subprogram, such as by raising or propagating exceptions, and calling
    noreturn functions.  The checks inserted before returns also prevented
    potential tail-call optimizations.
    
    This incremental change introduces options to control checking at each
    of these previously-missed checkpoints.  Unless disabled, a cleanup is
    introduced to check when an exceptions escapes a subprogram.  To avoid
    disrupting sibcall optimizations, when they are enabled, checks are
    introduced before calls whose results are immediately returned,
    whether or not they are ultimately optimized.  If enabled, checks are
    introduced before noreturn calls and exception raises, or only before
    nothrow noreturn calls.
    
    Add examples of code transformations to the GNAT RM.
    
    
    for  gcc/ada/ChangeLog
    
            * doc/gnat_rm/security_hardening_features.rst: Document
            optional hardcfr checkpoints.

Diff:
---
 .../doc/gnat_rm/security_hardening_features.rst    | 126 ++++++++++++++++++++-
 1 file changed, 121 insertions(+), 5 deletions(-)

diff --git a/gcc/ada/doc/gnat_rm/security_hardening_features.rst b/gcc/ada/doc/gnat_rm/security_hardening_features.rst
index d7c02b94f36..08cfaaf0f79 100644
--- a/gcc/ada/doc/gnat_rm/security_hardening_features.rst
+++ b/gcc/ada/doc/gnat_rm/security_hardening_features.rst
@@ -383,11 +383,127 @@ For each block that is marked as visited, the mechanism checks that at
 least one of its predecessors, and at least one of its successors, are
 also marked as visited.
 
-Verification is performed just before returning.  Subprogram
-executions that complete by raising or propagating an exception bypass
-verification-and-return points.  A subprogram that can only complete
-by raising or propagating an exception may have instrumentation
-disabled altogether.
+Verification is performed just before a subprogram returns.  The
+following fragment:
+
+.. code-block:: ada
+
+   if X then
+     Y := F (Z);
+     return;
+   end if;
+
+
+gets turned into:
+
+.. code-block:: ada
+
+   type Visited_Bitmap is array (1..N) of Boolean with Pack;
+   Visited : aliased Visited_Bitmap := (others => False);
+   --  Bitmap of visited blocks.  N is the basic block count.
+   [...]
+   --  Basic block #I
+   Visited(I) := True;
+   if X then
+     --  Basic block #J
+     Visited(J) := True;
+     Y := F (Z);
+     CFR.Check (N, Visited'Access, CFG'Access);
+     --  CFR is a hypothetical package whose Check procedure calls
+     --  libgcc's __hardcfr_check, that traps if the Visited bitmap
+     --  does not hold a valid path in CFG, the run-time
+     --  representation of the control flow graph in the enclosing
+     --  subprogram.
+     return;
+   end if;
+   --  Basic block #K
+   Visited(K) := True;
+
+
+Verification would also be performed before must-tail calls, and
+before early-marked potential tail calls, but these do not occur in
+practice, as potential tail-calls are only detected in late
+optimization phases, too late for this transformation to act on it.
+
+In order to avoid adding verification after potential tail calls,
+which would prevent tail-call optimization, we recognize returning
+calls, i.e., calls whose result, if any, is returned by the calling
+subprogram to its caller immediately after the call returns.
+Verification is performed before such calls, whether or not they are
+ultimately optimized to tail calls.  This behavior is enabled by
+default whenever sibcall optimization is enabled (see
+:switch:`-foptimize-sibling-calls`); it may be disabled with
+:switch:`-fno-hardcfr-check-returning-calls`, or enabled with
+:switch:`-fhardcfr-check-returning-calls`, regardless of the
+optimization, but the lack of other optimizations may prevent calls
+from being recognized as returning calls:
+
+.. code-block:: ada
+
+     --  CFR.Check here, with -fhardcfr-check-returning-calls.
+     P (X);
+     --  CFR.Check here, with -fno-hardcfr-check-returning-calls.
+     return;
+
+or:
+
+.. code-block:: ada
+
+     --  CFR.Check here, with -fhardcfr-check-returning-calls.
+     R := F (X);
+     --  CFR.Check here, with -fno-hardcfr-check-returning-calls.
+     return R;
+
+
+Any subprogram from which an exception may escape, i.e., that may
+raise or propagate an exception that isn't handled internally, is
+conceptually enclosed by a cleanup handler that performs verification,
+unless this is disabled with :switch:`-fno-hardcfr-check-exceptions`.
+With this feature enabled, a subprogram body containing:
+
+.. code-block:: ada
+
+     --  ...
+       Y := F (X);  -- May raise exceptions.
+     --  ...
+       raise E;  -- Not handled internally.
+     --  ...
+
+
+gets modified as follows:
+
+.. code-block:: ada
+
+   begin
+     --  ...
+       Y := F (X);  -- May raise exceptions.
+     --  ...
+       raise E;  -- Not handled internally.
+     --  ...
+   exception
+     when others =>
+       CFR.Check (N, Visited'Access, CFG'Access);
+       raise;
+   end;
+
+
+Verification may also be performed before No_Return calls, whether
+only nothrow ones, with
+:switch:`-fhardcfr-check-noreturn-calls=nothrow`, or all of them, with
+:switch:`-fhardcfr-check-noreturn-calls=always`.  The default is
+:switch:`-fhardcfr-check-noreturn-calls=never` for this feature, that
+disables checking before No_Return calls.
+
+When a No_Return call returns control to its caller through an
+exception, verification may have already been performed before the
+call, if :switch:`-fhardcfr-check-noreturn-calls=always` is in effect.
+The compiler arranges for already-checked No_Return calls without a
+preexisting handler to bypass the implicitly-added cleanup handler and
+thus the redundant check, but a local exception or cleanup handler, if
+present, will modify the set of visited blocks, and checking will take
+place again when the caller reaches the next verification point,
+whether it is a return or reraise statement after the exception is
+otherwise handled, or even another No_Return call.
 
 The instrumentation for hardening with control flow redundancy can be
 observed in dump files generated by the command-line option