Re: [Ada] Introduce hardbool Machine_Attribute for Ada

2022-05-13 Thread Alexandre Oliva via Gcc-patches
On May 12, 2022, Pierre-Marie de Rodat  wrote:

> Implement and document hardened booleans, from nonstandard boolean types
> with representation clauses to the extra validity checking performed on
> boolean types annotated with the "hardbool" Machine_Attribute pragma.

And here is a test for testsuite/gnat.dg.  Tested on x86_64-linux-gnu.
I'm checking this in.


Introduce tests for hardbool Machine_Attribute for Ada

Test for the validity checking performed on nonstandard booleans
annotated with the "hardbool" Machine_Attribute pragma.


for  gcc/testsuite/ChangeLog

* gnat.dg/hardbool.ads: New.
* gnat.dg/hardbool.adb: New.
---
 gcc/testsuite/gnat.dg/hardbool.adb |   46 
 gcc/testsuite/gnat.dg/hardbool.ads |   22 +
 2 files changed, 68 insertions(+)
 create mode 100644 gcc/testsuite/gnat.dg/hardbool.adb
 create mode 100644 gcc/testsuite/gnat.dg/hardbool.ads

diff --git a/gcc/testsuite/gnat.dg/hardbool.adb 
b/gcc/testsuite/gnat.dg/hardbool.adb
new file mode 100644
index 0..cc38af06a79b7
--- /dev/null
+++ b/gcc/testsuite/gnat.dg/hardbool.adb
@@ -0,0 +1,46 @@
+-- { dg-do compile }
+-- { dg-options "-O -gnatVT -fdump-tree-optimized" }
+
+--  Check that we perform the expected validity checks for
+--  hardbool-annotated types, even when checking of tests is disabled.
+
+package body Hardbool is
+   function T return Boolean is (Boolean (X) and then Boolean (Y));
+
+   procedure P1 is
+   begin
+  X := HBool1 (not Y);
+   end P1;
+
+   procedure P2 is
+   begin
+  X := HBool1 (if Y then HBool2'(False) else HBool2'(True));
+   end P2;
+
+   procedure P3 is
+   begin
+  X := (if Y then HBool1'(False) else HBool1'(True));
+   end P3;
+
+   procedure Q1 is
+   begin
+  Y := HBool2 (not X);
+   end Q1;
+
+   procedure Q2 is
+   begin
+  Y := HBool2 (if X then HBool1'(False) else HBool1'(True));
+   end Q2;
+
+   procedure Q3 is
+   begin
+  Y := (if X then HBool2'(False) else HBool2'(True));
+   end Q3;
+
+end Hardbool;
+
+-- One for each type's _rep_to_pos function.
+-- { dg-final { scan-tree-dump-times "gnat_rcheck_CE_Invalid_Data 
..hardbool.ads" 2 "optimized" } }
+
+-- One check for each variable used in T, one use in each P* and in each Q*.
+-- { dg-final { scan-tree-dump-times "gnat_rcheck_CE_Invalid_Data 
..hardbool.adb" 8 "optimized" } }
diff --git a/gcc/testsuite/gnat.dg/hardbool.ads 
b/gcc/testsuite/gnat.dg/hardbool.ads
new file mode 100644
index 0..7181220a6db5d
--- /dev/null
+++ b/gcc/testsuite/gnat.dg/hardbool.ads
@@ -0,0 +1,22 @@
+package Hardbool is
+   type HBool1 is new Boolean;
+   for HBool1'Size use 8;
+   for HBool1 use (16#5a#, 16#a5#);
+   pragma Machine_Attribute (HBool1, "hardbool");
+
+   type HBool2 is new Boolean;
+   for HBool2 use (16#0ff0#, 16#f00f#);
+   for HBool2'Size use 16;
+   pragma Machine_Attribute (HBool2, "hardbool");
+
+   X : HBool1 := False;
+   Y : HBool2 := True;
+
+   function T return Boolean;
+   procedure P1;
+   procedure P2;
+   procedure P3;
+   procedure Q1;
+   procedure Q2;
+   procedure Q3;
+end Hardbool;


-- 
Alexandre Oliva, happy hackerhttps://FSFLA.org/blogs/lxo/
   Free Software Activist   GNU Toolchain Engineer
Disinformation flourishes because many people care deeply about injustice
but very few check the facts.  Ask me about <https://stallmansupport.org>


[Ada] Introduce hardbool Machine_Attribute for Ada

2022-05-12 Thread Pierre-Marie de Rodat via Gcc-patches
Implement and document hardened booleans, from nonstandard boolean types
with representation clauses to the extra validity checking performed on
boolean types annotated with the "hardbool" Machine_Attribute pragma.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

* doc/gnat_rm/security_hardening_features.rst (Hardened
Booleans): New.
* exp_util.adb (Adjust_Condition): Perform validity checking on
hardbool-annotated types even with -gnatVT.
* gnat_rm.texi: Regenerate.
* gcc-interface/utils.cc (gnat_internal_attribute_table): Ignore
hardbool.diff --git a/gcc/ada/doc/gnat_rm/security_hardening_features.rst b/gcc/ada/doc/gnat_rm/security_hardening_features.rst
--- a/gcc/ada/doc/gnat_rm/security_hardening_features.rst
+++ b/gcc/ada/doc/gnat_rm/security_hardening_features.rst
@@ -160,3 +160,39 @@ files of the corresponding passes, through command line options
 
 They are separate options, however, because of the significantly
 different performance impact of the hardening transformations.
+
+
+.. Hardened Booleans:
+
+Hardened Booleans
+=
+
+Ada has built-in support for introducing boolean types with
+alternative representations, using representation clauses:
+
+.. code-block:: ada
+
+   type HBool is new Boolean;
+   for HBool use (16#5a#, 16#a5#);
+   for HBool'Size use 8;
+
+When validity checking is enabled, the compiler will check that
+variables of such types hold values corresponding to the selected
+representations.
+
+There are multiple strategies for where to introduce validity checking
+(see *-gnatV* options).  Their goal is to guard against various kinds
+of programming errors, and GNAT strives to omit checks when program
+logic rules out an invalid value, and optimizers may further remove
+checks found to be redundant.
+
+For additional hardening, the ``hardbool`` :samp:`Machine_Attribute`
+pragma can be used to annotate boolean types with representation
+clauses, so that expressions of such types used as conditions are
+checked even when compiling with *-gnatVT*.
+
+.. code-block:: ada
+
+   pragma Machine_Attribute (HBool, "hardbool");
+
+Note that *-gnatVn* will disable even ``hardbool`` testing.


diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -328,6 +328,72 @@ package body Exp_Util is
--
 
procedure Adjust_Condition (N : Node_Id) is
+
+  function Is_Hardbool_Type (T : Entity_Id) return Boolean;
+  --  Return True iff T is a type annotated with the
+  --  Machine_Attribute pragma "hardbool".
+
+  --
+  -- Is_Hardbool_Type --
+  --
+
+  function Is_Hardbool_Type (T : Entity_Id) return Boolean is
+
+ function Find_Hardbool_Pragma
+   (Id : Entity_Id) return Node_Id;
+ --  Return a Rep_Item associated with entity Id that
+ --  corresponds to the Hardbool Machine_Attribute pragma, if
+ --  any, or Empty otherwise.
+
+ function Pragma_Arg_To_String (Item : Node_Id) return String is
+(To_String (Strval (Expr_Value_S (Item;
+ --  Return the pragma argument Item as a String
+
+ function Hardbool_Pragma_P (Item : Node_Id) return Boolean is
+(Nkind (Item) = N_Pragma
+   and then
+ Pragma_Name (Item) = Name_Machine_Attribute
+   and then
+ Pragma_Arg_To_String
+   (Get_Pragma_Arg
+  (Next (First (Pragma_Argument_Associations (Item)
+   = "hardbool");
+ --  Return True iff representation Item is a "hardbool"
+ --  Machine_Attribute pragma.
+
+ --
+ -- Find_Hardbool_Pragma --
+ --
+
+ function Find_Hardbool_Pragma
+   (Id : Entity_Id) return Node_Id
+ is
+Item : Node_Id;
+
+ begin
+if not Has_Gigi_Rep_Item (Id) then
+   return Empty;
+end if;
+
+Item := First_Rep_Item (Id);
+while Present (Item) loop
+   if Hardbool_Pragma_P (Item) then
+  return Item;
+   end if;
+   Item := Next_Rep_Item (Item);
+end loop;
+
+return Empty;
+ end Find_Hardbool_Pragma;
+
+  --  Start of processing for Is_Hardbool_Type
+
+  begin
+ return Present (Find_Hardbool_Pragma (T));
+  end Is_Hardbool_Type;
+
+   --  Start of processing for Adjust_Condition
+
begin
   if No (N) then
  return;
@@ -347,7 +413,10 @@ package body Exp_Util is
 
  --  Apply validity checking if needed
 
- if Validity_Checks_On and Validity_Check_Tests then
+ if Validity_Checks_On
+   and then
+ (Validity_Check_Tests or else Is_Hardbool_Type (T))
+ then