* [wwwdocs] Add Ada's GCC 14 changelog entry @ 2024-02-25 20:48 Fernando Oleo Blanco 2024-02-26 9:17 ` Marc Poulhiès 0 siblings, 1 reply; 4+ messages in thread From: Fernando Oleo Blanco @ 2024-02-25 20:48 UTC (permalink / raw) To: gcc-patches; +Cc: Arnaud Charlet [-- Attachment #1: Type: text/plain, Size: 345 bytes --] Dear all, just like last year, I would like to commit the changes that took place over at GNAT for GCC v14. The patch is attached to the email. Hopefully it is good enough to just be added to master. If you see something wrong or if you would like to add anything to it, feel free :) Feedback is always welcomed. Best regards, Fer [-- Attachment #2: 0001-Add-Ada-changes-for-v14.patch --] [-- Type: text/x-patch, Size: 2967 bytes --] From 0ae94649be7f638bb4f98ba3e2ba2e1bf9770c09 Mon Sep 17 00:00:00 2001 From: Fernando Oleo Blanco <irvise@irvise.xyz> Date: Sun, 25 Feb 2024 21:43:43 +0100 Subject: [PATCH 1/1] Add Ada changes for v14 --- htdocs/gcc-14/changes.html | 44 +++++++++++++++++++++++++++++++++++++- 1 file changed, 43 insertions(+), 1 deletion(-) diff --git a/htdocs/gcc-14/changes.html b/htdocs/gcc-14/changes.html index 85ccc54d..e6c96c9f 100644 --- a/htdocs/gcc-14/changes.html +++ b/htdocs/gcc-14/changes.html @@ -171,7 +171,49 @@ a work-in-progress.</p> <!-- .................................................................. --> <h2 id="languages">New Languages and Language specific improvements</h2> -<!-- <h3 id="ada">Ada</h3> --> +<h3 id="ada">Ada</h3> + +<ul> + <li>Several new aspects and contracts have been implemented: + <ul> + <li><code>Exceptional_Cases</code> may be specified for procedures and + functions with side effects; it can be used to list exceptions that might + be propagated by the subprogram with side effects in the context of its + precondition, and associate them with a specific postcondition. For more + information, refer to SPARK 2014 Reference Manual, section 6.1.9.</li> + <li><code>User_Aspect</code> takes an argument that is the name of an + aspect defined by a User_Aspect_Definition configuration pragma.</li> + <li><code>Local_Restrictions</code> is used to specify that a particular + subprogram does not violate one or more local restrictions, nor can it + call a subprogram that is not subject to the same requirements.</li> + <li><code>Side_Effects</code> is equivalent to <code>pragma + Side_Effecs</code>.</li> + <li><code>Always_Terminates</code> is a boolean equivalent to <code>pragma + Always_Terminates</code></li> + <li><code>Ghost_Predicate</code></li> + </ul> + </li> + <li>The new attributes and contracts have been applied to the relevant parts + of the Ada library and more code has been proven to be correct.</li> + <li>Initial support for the + <a href="https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/"><code>CHERI</code></a> + architecture.</li> + <li>Support for the <code>LoongArch</code> architecture.</li> + <li>Hardening improvements: + <ul> + <li>Use of the new <code>-fharden*</code> options. Most + notably <code>-fharden-compares</code>, + <code>-fharden-conditional-branches</code> and + <code>-fharden-control-flow-redundancy</code>.</li> + <li>Custom bools with higher Hamming distance.</li> + <li>The <code>strub</code> attribute has been added for functions and + variables in order to automatically zero-out their stack upon use or + return.</li> + </ul> + </li> + <li>Further clean up and improvements to the GNAT code.</li> + <li>Support for vxWorks 7 Cert RTP has been removed.</li> +</ul> <!-- <h3 id="c-family">C family</h3> --> -- 2.43.2 ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: [wwwdocs] Add Ada's GCC 14 changelog entry 2024-02-25 20:48 [wwwdocs] Add Ada's GCC 14 changelog entry Fernando Oleo Blanco @ 2024-02-26 9:17 ` Marc Poulhiès 2024-02-26 19:36 ` Fernando Oleo Blanco 0 siblings, 1 reply; 4+ messages in thread From: Marc Poulhiès @ 2024-02-26 9:17 UTC (permalink / raw) To: Fernando Oleo Blanco; +Cc: Arnaud Charlet, gcc-patches Fernando Oleo Blanco <irvise_ml@irvise.xyz> writes: > Dear all, > > just like last year, I would like to commit the changes that took place > over at GNAT for GCC v14. The patch is attached to the email. Hopefully > it is good enough to just be added to master. If you see something wrong > or if you would like to add anything to it, feel free :) Feedback is > always welcomed. Fernando, Thank you for this work! I have a few comments, see below. diff --git a/htdocs/gcc-14/changes.html b/htdocs/gcc-14/changes.html index 85ccc54d..e6c96c9f 100644 --- a/htdocs/gcc-14/changes.html +++ b/htdocs/gcc-14/changes.html @@ -171,7 +171,49 @@ a work-in-progress.</p> <!-- .................................................................. --> <h2 id="languages">New Languages and Language specific improvements</h2> -<!-- <h3 id="ada">Ada</h3> --> +<h3 id="ada">Ada</h3> + +<ul> + <li>Several new aspects and contracts have been implemented: Maybe worth noting that these are implementation defined aspects. + <ul> + <li><code>Exceptional_Cases</code> may be specified for procedures and + functions with side effects; it can be used to list exceptions that might + be propagated by the subprogram with side effects in the context of its + precondition, and associate them with a specific postcondition. For more + information, refer to SPARK 2014 Reference Manual, section 6.1.9.</li> + <li><code>User_Aspect</code> takes an argument that is the name of an + aspect defined by a User_Aspect_Definition configuration pragma.</li> + <li><code>Local_Restrictions</code> is used to specify that a particular + subprogram does not violate one or more local restrictions, nor can it + call a subprogram that is not subject to the same requirements.</li> + <li><code>Side_Effects</code> is equivalent to <code>pragma + Side_Effecs</code>.</li> + <li><code>Always_Terminates</code> is a boolean equivalent to <code>pragma + Always_Terminates</code></li> + <li><code>Ghost_Predicate</code></li> It looks like Ghost_Predicate is missing some text here. It may be a good thing to link to the actual documentation for these options. Thanks to some documention changes, we can now link to an option directly. For example: https://gcc.gnu.org/onlinedocs/gnat_rm/Implementation-Defined-Pragmas.html You would need to point to the correct version (this one points to current devel version). + </ul> + </li> + <li>The new attributes and contracts have been applied to the relevant parts + of the Ada library and more code has been proven to be correct.</li> + <li>Initial support for the + <a href="https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/"><code>CHERI</code></a> + architecture.</li> + <li>Support for the <code>LoongArch</code> architecture.</li> + <li>Hardening improvements: + <ul> + <li>Use of the new <code>-fharden*</code> options. Most + notably <code>-fharden-compares</code>, + <code>-fharden-conditional-branches</code> and + <code>-fharden-control-flow-redundancy</code>.</li> + <li>Custom bools with higher Hamming distance.</li> + <li>The <code>strub</code> attribute has been added for functions and Same as above for doc links: https://gcc.gnu.org/onlinedocs/gcc/Instrumentation-Options.html#index-fharden-compares + variables in order to automatically zero-out their stack upon use or + return.</li> + </ul> + </li> + <li>Further clean up and improvements to the GNAT code.</li> + <li>Support for vxWorks 7 Cert RTP has been removed.</li> +</ul> <!-- <h3 id="c-family">C family</h3> --> ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: [wwwdocs] Add Ada's GCC 14 changelog entry 2024-02-26 9:17 ` Marc Poulhiès @ 2024-02-26 19:36 ` Fernando Oleo Blanco 2024-03-10 17:30 ` Fernando Oleo Blanco 0 siblings, 1 reply; 4+ messages in thread From: Fernando Oleo Blanco @ 2024-02-26 19:36 UTC (permalink / raw) To: Marc Poulhiès; +Cc: Arnaud Charlet, gcc-patches [-- Attachment #1: Type: text/plain, Size: 2679 bytes --] Hi Mark, On 2/26/24 10:17, Marc Poulhiès wrote: > > Fernando, > > Thank you for this work! I have a few comments, see below. > > diff --git a/htdocs/gcc-14/changes.html b/htdocs/gcc-14/changes.html > index 85ccc54d..e6c96c9f 100644 > --- a/htdocs/gcc-14/changes.html > +++ b/htdocs/gcc-14/changes.html > @@ -171,7 +171,49 @@ a work-in-progress.</p> > <!-- .................................................................. --> > <h2 id="languages">New Languages and Language specific improvements</h2> > > -<!-- <h3 id="ada">Ada</h3> --> > +<h3 id="ada">Ada</h3> > + > +<ul> > + <li>Several new aspects and contracts have been implemented: > > Maybe worth noting that these are implementation defined aspects. Noted > > + <ul> > + <li><code>Exceptional_Cases</code> may be specified for procedures and [...] > + Side_Effecs</code>.</li> > + <li><code>Always_Terminates</code> is a boolean equivalent to <code>pragma > + Always_Terminates</code></li> > + <li><code>Ghost_Predicate</code></li> > > It looks like Ghost_Predicate is missing some text here. > > It may be a good thing to link to the actual documentation for these > options. Thanks to some documention changes, we can now link to > an option directly. For example: > > https://gcc.gnu.org/onlinedocs/gnat_rm/Implementation-Defined-Pragmas.html Added > > You would need to point to the correct version (this one points to > current devel version). > Done > + </ul> > + </li> > + <li>The new attributes and contracts have been applied to the relevant parts [...] > + <code>-fharden-control-flow-redundancy</code>.</li> > + <li>Custom bools with higher Hamming distance.</li> > + <li>The <code>strub</code> attribute has been added for functions and > > Same as above for doc links: > > https://gcc.gnu.org/onlinedocs/gcc/Instrumentation-Options.html#index-fharden-compares Done > > + variables in order to automatically zero-out their stack upon use or > + return.</li> > + </ul> > + </li> > + <li>Further clean up and improvements to the GNAT code.</li> > + <li>Support for vxWorks 7 Cert RTP has been removed.</li> > +</ul> > > <!-- <h3 id="c-family">C family</h3> --> I have applied your recommendations. The documentation links are still not up... Nonetheless, I created the URL in such a way that they should work once the final documentation is given a release number (which I guessed to be 14.1.0). If you think this can be improved just say so. Nonetheless, feel free to modify my patch if you see it fit. Best regards, Fer [-- Attachment #2: 0002-Add-more-information-to-the-Ada-changes.patch --] [-- Type: text/x-patch, Size: 5095 bytes --] From 0ae94649be7f638bb4f98ba3e2ba2e1bf9770c09 Mon Sep 17 00:00:00 2001 From: Fernando Oleo Blanco <irvise@irvise.xyz> Date: Sun, 25 Feb 2024 21:43:43 +0100 Subject: [PATCH 1/2] Add Ada changes for v14 --- htdocs/gcc-14/changes.html | 44 +++++++++++++++++++++++++++++++++++++- 1 file changed, 43 insertions(+), 1 deletion(-) diff --git a/htdocs/gcc-14/changes.html b/htdocs/gcc-14/changes.html index 85ccc54d..e6c96c9f 100644 --- a/htdocs/gcc-14/changes.html +++ b/htdocs/gcc-14/changes.html @@ -171,7 +171,49 @@ a work-in-progress.</p> <!-- .................................................................. --> <h2 id="languages">New Languages and Language specific improvements</h2> -<!-- <h3 id="ada">Ada</h3> --> +<h3 id="ada">Ada</h3> + +<ul> + <li>Several new aspects and contracts have been implemented: + <ul> + <li><code>Exceptional_Cases</code> may be specified for procedures and + functions with side effects; it can be used to list exceptions that might + be propagated by the subprogram with side effects in the context of its + precondition, and associate them with a specific postcondition. For more + information, refer to SPARK 2014 Reference Manual, section 6.1.9.</li> + <li><code>User_Aspect</code> takes an argument that is the name of an + aspect defined by a User_Aspect_Definition configuration pragma.</li> + <li><code>Local_Restrictions</code> is used to specify that a particular + subprogram does not violate one or more local restrictions, nor can it + call a subprogram that is not subject to the same requirements.</li> + <li><code>Side_Effects</code> is equivalent to <code>pragma + Side_Effecs</code>.</li> + <li><code>Always_Terminates</code> is a boolean equivalent to <code>pragma + Always_Terminates</code></li> + <li><code>Ghost_Predicate</code></li> + </ul> + </li> + <li>The new attributes and contracts have been applied to the relevant parts + of the Ada library and more code has been proven to be correct.</li> + <li>Initial support for the + <a href="https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/"><code>CHERI</code></a> + architecture.</li> + <li>Support for the <code>LoongArch</code> architecture.</li> + <li>Hardening improvements: + <ul> + <li>Use of the new <code>-fharden*</code> options. Most + notably <code>-fharden-compares</code>, + <code>-fharden-conditional-branches</code> and + <code>-fharden-control-flow-redundancy</code>.</li> + <li>Custom bools with higher Hamming distance.</li> + <li>The <code>strub</code> attribute has been added for functions and + variables in order to automatically zero-out their stack upon use or + return.</li> + </ul> + </li> + <li>Further clean up and improvements to the GNAT code.</li> + <li>Support for vxWorks 7 Cert RTP has been removed.</li> +</ul> <!-- <h3 id="c-family">C family</h3> --> -- 2.43.2 From ddacac13df6df1527b2368818fe6e9f0cc34028e Mon Sep 17 00:00:00 2001 From: Fernando Oleo Blanco <irvise@irvise.xyz> Date: Mon, 26 Feb 2024 20:26:55 +0100 Subject: [PATCH 2/2] Add more information to the Ada changes --- htdocs/gcc-14/changes.html | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/htdocs/gcc-14/changes.html b/htdocs/gcc-14/changes.html index e6c96c9f..260d04f5 100644 --- a/htdocs/gcc-14/changes.html +++ b/htdocs/gcc-14/changes.html @@ -174,7 +174,8 @@ a work-in-progress.</p> <h3 id="ada">Ada</h3> <ul> - <li>Several new aspects and contracts have been implemented: + <li>Several new implementation defined aspects and contracts have been + added: <ul> <li><code>Exceptional_Cases</code> may be specified for procedures and functions with side effects; it can be used to list exceptions that might @@ -190,8 +191,12 @@ a work-in-progress.</p> Side_Effecs</code>.</li> <li><code>Always_Terminates</code> is a boolean equivalent to <code>pragma Always_Terminates</code></li> - <li><code>Ghost_Predicate</code></li> + <li><code>Ghost_Predicate</code> introduces a subtype predicate that can + reference <code>Ghost</code> entities.</li> </ul> + For more information and usage guidelines, see + the <a href="https://gcc.gnu.org/onlinedocs/gcc-14.1.0/gnat_rm/Implementation-Defined-Pragmas.html">GNAT + Reference Manual</a>. </li> <li>The new attributes and contracts have been applied to the relevant parts of the Ada library and more code has been proven to be correct.</li> @@ -210,6 +215,9 @@ a work-in-progress.</p> variables in order to automatically zero-out their stack upon use or return.</li> </ul> + For more information reltated to hardening options, refer to + the <a href="https://gcc.gnu.org/onlinedocs/gcc-14.1.0/Instrumentation-Options.html#index-fharden-compares">GCC + Instrumentation Options</a>. </li> <li>Further clean up and improvements to the GNAT code.</li> <li>Support for vxWorks 7 Cert RTP has been removed.</li> -- 2.43.2 ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: [wwwdocs] Add Ada's GCC 14 changelog entry 2024-02-26 19:36 ` Fernando Oleo Blanco @ 2024-03-10 17:30 ` Fernando Oleo Blanco 0 siblings, 0 replies; 4+ messages in thread From: Fernando Oleo Blanco @ 2024-03-10 17:30 UTC (permalink / raw) To: Marc Poulhiès; +Cc: Arnaud Charlet, gcc-patches, Alexandre Oliva [-- Attachment #1: Type: text/plain, Size: 2621 bytes --] Hi all, I have a new revision of the patch. Alexandre pointed out a few issues with the hardening options and I agreed with the comments. I took a look at when the boolean hardening and stack scrubbing options became available within Ada. Hardbools were already available in GCC 13.1, stack scrubbing was already present in GCC 12.1. Which means that adding this changes to the changelog would be incorrect. The additional compiler hardening options/flags within GCC are not unique to Ada and they are already documented in the general compiler section and they are available for the C family of languages as well as Ada. Therefore, it made sense not to explicitly have them in the Ada section. Nonetheless, there have been some (smaller) hardening improvements to Ada, so I just wrote a generic note and pointers to the documentation. I know this is not the pretties thing to do, but I did something similar in the GCC 12 changelog so... On 2/26/24 20:36, Fernando Oleo Blanco wrote: > Hi Mark, > > On 2/26/24 10:17, Marc Poulhiès wrote: >> >> Fernando, >> >> Thank you for this work! I have a few comments, see below. >> >> diff --git a/htdocs/gcc-14/changes.html b/htdocs/gcc-14/changes.html >> index 85ccc54d..e6c96c9f 100644 >> --- a/htdocs/gcc-14/changes.html >> +++ b/htdocs/gcc-14/changes.html >> @@ -171,7 +171,49 @@ a work-in-progress.</p> >> <!-- .................................................................. --> >> <h2 id="languages">New Languages and Language specific improvements</h2> >> >> -<!-- <h3 id="ada">Ada</h3> --> >> +<h3 id="ada">Ada</h3> [... omitted for brevity ...] > > I have applied your recommendations. The documentation links are still > not up... Nonetheless, I created the URL in such a way that they should > work once the final documentation is given a release number (which I > guessed to be 14.1.0). If you think this can be improved just say so. > Nonetheless, feel free to modify my patch if you see it fit. In this newly revised patch I have not modified the URLs to point to the future GCC 14 documentation. I saw that the links in the changelog all had the unversioned "master" links, so I just followed the same convention. > > Best regards, > Fer I squashed the different commits I had submitted and created a completely new patch. Hopefully this is acceptable and leads to a cleaner, less noisy commit history/patch. It is attached to the email. I think the patch should be in an acceptable state to be committed, but feel free to give back any feedback! Best regards, Fer [-- Attachment #2: 0001-Add-Ada-changes-for-v14.patch --] [-- Type: text/x-patch, Size: 3146 bytes --] From 9ad2e979e921938c466de3a7868346e8b2426e49 Mon Sep 17 00:00:00 2001 From: Fernando Oleo Blanco <irvise@irvise.xyz> Date: Sun, 10 Mar 2024 17:47:46 +0100 Subject: [PATCH] Add Ada changes for v14 --- htdocs/gcc-14/changes.html | 43 +++++++++++++++++++++++++++++++++++++- 1 file changed, 42 insertions(+), 1 deletion(-) diff --git a/htdocs/gcc-14/changes.html b/htdocs/gcc-14/changes.html index 85ccc54d..0886241a 100644 --- a/htdocs/gcc-14/changes.html +++ b/htdocs/gcc-14/changes.html @@ -171,7 +171,48 @@ a work-in-progress.</p> <!-- .................................................................. --> <h2 id="languages">New Languages and Language specific improvements</h2> -<!-- <h3 id="ada">Ada</h3> --> +<h3 id="ada">Ada</h3> + +<ul> + <li>Several new implementation defined aspects and contracts have been + added: + <ul> + <li><code>Exceptional_Cases</code> may be specified for procedures and + functions with side effects; it can be used to list exceptions that might + be propagated by the subprogram with side effects in the context of its + precondition, and associate them with a specific postcondition. For more + information, refer to SPARK 2014 Reference Manual, section 6.1.9.</li> + <li><code>User_Aspect</code> takes an argument that is the name of an + aspect defined by a User_Aspect_Definition configuration pragma.</li> + <li><code>Local_Restrictions</code> is used to specify that a particular + subprogram does not violate one or more local restrictions, nor can it + call a subprogram that is not subject to the same requirements.</li> + <li><code>Side_Effects</code> is equivalent to <code>pragma + Side_Effecs</code>.</li> + <li><code>Always_Terminates</code> is a boolean equivalent to <code>pragma + Always_Terminates</code></li> + <li><code>Ghost_Predicate</code> introduces a subtype predicate that can + reference <code>Ghost</code> entities.</li> + </ul> + For more information and usage guidelines, see + the <a href="https://gcc.gnu.org/onlinedocs/gnat_rm/Implementation-Defined-Pragmas.html">GNAT + Reference Manual</a>. + </li> + <li>The new attributes and contracts have been applied to the relevant parts + of the Ada library and more code has been proven to be correct.</li> + <li>Initial support for the + <a href="https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/"><code>CHERI</code></a> + architecture.</li> + <li>Support for the <code>LoongArch</code> architecture.</li> + <li>Support for vxWorks 7 Cert RTP has been removed.</li> + <li>Additional hardening improvements. For more information reltated to hardening options, refer to + the <a href="https://gcc.gnu.org/onlinedocs/gcc/Instrumentation-Options.html#index-fharden-compares">GCC + Instrumentation Options</a> and + the <a href="https://gcc.gnu.org/onlinedocs/gnat_rm/Security-Hardening-Features.html">GNAT + Reference Manual, Security and Hardening Features</a>. + </li> + <li>Further clean up and improvements to the GNAT code.</li> +</ul> <!-- <h3 id="c-family">C family</h3> --> -- 2.44.0 ^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2024-03-10 17:30 UTC | newest] Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2024-02-25 20:48 [wwwdocs] Add Ada's GCC 14 changelog entry Fernando Oleo Blanco 2024-02-26 9:17 ` Marc Poulhiès 2024-02-26 19:36 ` Fernando Oleo Blanco 2024-03-10 17:30 ` Fernando Oleo Blanco
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).