@@ -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 tail calls, if any
+front-ends marked them as mandatory or desirable, but none do.
+Regular calls are optimized into tail calls 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
@@ -19,7 +19,7 @@
@copying
@quotation
-GNAT Reference Manual , Oct 27, 2022
+GNAT Reference Manual , Nov 14, 2022
AdaCore
@@ -29037,11 +29037,122 @@ 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:
+
+@example
+if X then
+ Y := F (Z);
+ return;
+end if;
+@end example
+
+gets turned into:
+
+@example
+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;
+@end example
+
+Verification would also be performed before tail calls, if any
+front-ends marked them as mandatory or desirable, but none do.
+Regular calls are optimized into tail calls 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
+@code{-foptimize-sibling-calls}); it may be disabled with
+@code{-fno-hardcfr-check-returning-calls}, or enabled with
+@code{-fhardcfr-check-returning-calls}, regardless of the
+optimization, but the lack of other optimizations may prevent calls
+from being recognized as returning calls:
+
+@example
+-- CFR.Check here, with -fhardcfr-check-returning-calls.
+P (X);
+-- CFR.Check here, with -fno-hardcfr-check-returning-calls.
+return;
+@end example
+
+or:
+
+@example
+-- CFR.Check here, with -fhardcfr-check-returning-calls.
+R := F (X);
+-- CFR.Check here, with -fno-hardcfr-check-returning-calls.
+return R;
+@end example
+
+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 @code{-fno-hardcfr-check-exceptions}.
+With this feature enabled, a subprogram body containing:
+
+@example
+-- ...
+ Y := F (X); -- May raise exceptions.
+-- ...
+ raise E; -- Not handled internally.
+-- ...
+@end example
+
+gets modified as follows:
+
+@example
+begin
+ -- ...
+ Y := F (X); -- May raise exceptions.
+ -- ...
+ raise E; -- Not handled internally.
+ -- ...
+exception
+ when others =>
+ CFR.Check (N, Visited'Access, CFG'Access);
+ raise;
+end;
+@end example
+
+Verification may also be performed before No_Return calls, whether
+only nothrow ones, with
+@code{-fhardcfr-check-noreturn-calls=nothrow}, or all of them, with
+@code{-fhardcfr-check-noreturn-calls=always}. The default is
+@code{-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 @code{-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
@@ -19,7 +19,7 @@
@copying
@quotation
-GNAT User's Guide for Native Platforms , Oct 27, 2022
+GNAT User's Guide for Native Platforms , Nov 14, 2022
AdaCore
@@ -17993,7 +17993,6 @@ instr.ads
-
@c -- Example: A |withing| unit has a |with| clause, it |withs| a |withed| unit
@node GNAT and Program Execution,Platform-Specific Information,GNAT Utility Programs,Top
@@ -29382,8 +29381,8 @@ to permit their use in free software.
@printindex ge
-@anchor{cf}@w{ }
@anchor{gnat_ugn/gnat_utility_programs switches-related-to-project-files}@w{ }
+@anchor{cf}@w{ }
@c %**end of body
@bye