Merge pull request #239 from xbauch/feature/representation-clause-component-size

chrisr-diffblue · web-flow · commit d459eee67763 · 2019-06-04T11:11:34.000+01:00
Representation clause component size
diff --git a/experiments/golden-results/SPARK-tetris-summary.txt b/experiments/golden-results/SPARK-tetris-summary.txt
@@ -4,11 +4,6 @@ Error message: Package declaration
 Nkind: N_Package_Declaration
 --
 Occurs: 1 times
-Calling function: Process_Declaration
-Error message: Representation clause unsupported: component_size
-Nkind: N_Attribute_Definition_Clause
---
-Occurs: 1 times
 Redacted compiler error message:
 "REDACTED" not declared in "REDACTED"
 Raw compiler error message:
diff --git a/experiments/golden-results/StratoX-summary.txt b/experiments/golden-results/StratoX-summary.txt
@@ -43,11 +43,6 @@ Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Check
 Nkind: N_Pragma
 --
-Occurs: 22 times
-Calling function: Process_Declaration
-Error message: Representation clause unsupported: component_size
-Nkind: N_Attribute_Definition_Clause
---
 Occurs: 21 times
 Calling function: Process_Declaration
 Error message: Package body declaration
diff --git a/experiments/golden-results/Tokeneer-summary.txt b/experiments/golden-results/Tokeneer-summary.txt
@@ -39,11 +39,6 @@ Error message: Abstract type declaration unsupported
 Nkind: N_Private_Type_Declaration
 --
 Occurs: 7 times
-Calling function: Process_Declaration
-Error message: Representation clause unsupported: component_size
-Nkind: N_Attribute_Definition_Clause
---
-Occurs: 7 times
 Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Ada 05
 Nkind: N_Pragma
diff --git a/experiments/golden-results/UKNI-Information-Barrier-summary.txt b/experiments/golden-results/UKNI-Information-Barrier-summary.txt
@@ -1,13 +1,3 @@
-Occurs: 42 times
-Calling function: Process_Declaration
-Error message: Representation clause unsupported: address
-Nkind: N_Attribute_Definition_Clause
---
-Occurs: 8 times
-Calling function: Process_Declaration
-Error message: Representation clause unsupported: component_size
-Nkind: N_Attribute_Definition_Clause
---
 Occurs: 7 times
 Calling function: Process_Declaration
 Error message: Subprogram body stub declaration
@@ -38,16 +28,6 @@ Calling function: Do_Base_Range_Constraint
 Error message: unsupported upper range kind
 Nkind: N_Attribute_Reference
 --
-Occurs: 1 times
-Calling function: Do_Operator_General
-Error message: Mod of unsupported type
-Nkind: N_Op_Not
---
-Occurs: 1 times
-Calling function: Process_Declaration
-Error message: Use package clause declaration
-Nkind: N_Use_Package_Clause
---
 Occurs: 5 times
 Redacted compiler error message:
 "REDACTED" not declared in "REDACTED"
diff --git a/experiments/golden-results/ksum-summary.txt b/experiments/golden-results/ksum-summary.txt
@@ -24,11 +24,6 @@ Error message: Access type unsupported
 Nkind: N_Access_To_Object_Definition
 --
 Occurs: 1 times
-Calling function: Process_Declaration
-Error message: Representation clause unsupported: component_size
-Nkind: N_Attribute_Definition_Clause
---
-Occurs: 1 times
 Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Ada 05
 Nkind: N_Pragma
diff --git a/experiments/golden-results/libkeccak-summary.txt b/experiments/golden-results/libkeccak-summary.txt
@@ -39,11 +39,6 @@ Error message: Abstract subprogram declaration
 Nkind: N_Abstract_Subprogram_Declaration
 --
 Occurs: 6 times
-Calling function: Process_Declaration
-Error message: Representation clause unsupported: component_size
-Nkind: N_Attribute_Definition_Clause
---
-Occurs: 6 times
 Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Ada 05
 Nkind: N_Pragma
diff --git a/experiments/golden-results/muen-summary.txt b/experiments/golden-results/muen-summary.txt
@@ -18,11 +18,6 @@ Calling function: Do_Private_Type_Declaration
 Error message: Abstract type declaration unsupported
 Nkind: N_Private_Type_Declaration
 --
-Occurs: 46 times
-Calling function: Process_Declaration
-Error message: Representation clause unsupported: component_size
-Nkind: N_Attribute_Definition_Clause
---
 Occurs: 28 times
 Calling function: Process_Declaration
 Error message: Abstract subprogram declaration
diff --git a/experiments/golden-results/vct-summary.txt b/experiments/golden-results/vct-summary.txt
@@ -58,11 +58,6 @@ Calling function: Do_Procedure_Call_Statement
 Error message: sym id not in symbol table
 Nkind: N_Procedure_Call_Statement
 --
-Occurs: 2 times
-Calling function: Process_Declaration
-Error message: Representation clause unsupported: component_size
-Nkind: N_Attribute_Definition_Clause
---
 Occurs: 1 times
 Calling function: Do_Function_Call
 Error message: func name not in symbol table
diff --git a/gnat2goto/driver/arrays.adb b/gnat2goto/driver/arrays.adb
@@ -981,11 +981,9 @@ package body Arrays is
       return List_Element (Struct_Component, Last_Cursor);
    end Get_Last_Index_Component;
 
-   function Get_Data_Component (Array_Struct : Irep;
-                                A_Symbol_Table : Symbol_Table) return Irep
+   function Get_Data_Component_From_Type (Array_Struct_Type : Irep)
+                                          return Irep
    is
-      Array_Struct_Type : constant Irep :=
-        Follow_Symbol_Type (Get_Type (Array_Struct), A_Symbol_Table);
       Struct_Component : constant Irep_List :=
         Get_Component (Get_Components (Array_Struct_Type));
       Last_Cursor :  constant List_Cursor :=
@@ -994,6 +992,16 @@ package body Arrays is
                      List_First (Struct_Component)));
    begin
       return List_Element (Struct_Component, Last_Cursor);
+   end Get_Data_Component_From_Type;
+
+   function Get_Data_Component (Array_Struct : Irep;
+                                A_Symbol_Table : Symbol_Table)
+                                return Irep
+   is
+      Array_Struct_Type : constant Irep :=
+        Follow_Symbol_Type (Get_Type (Array_Struct), A_Symbol_Table);
+   begin
+      return Get_Data_Component_From_Type (Array_Struct_Type);
    end Get_Data_Component;
 
    function Get_First_Index (Array_Struct : Irep) return Irep
diff --git a/gnat2goto/driver/arrays.ads b/gnat2goto/driver/arrays.ads
@@ -46,6 +46,12 @@ package Arrays is
    function Do_Indexed_Component (N : Node_Id) return Irep
      with Pre  => Nkind (N) = N_Indexed_Component;
 
+   function Get_Data_Component_From_Type (Array_Struct_Type : Irep)
+                                          return Irep
+     with Pre => Kind (Array_Struct_Type) in I_Struct_Type,
+     Post => Kind (Get_Type (Get_Data_Component_From_Type'Result))
+       in I_Pointer_Type;
+
    function Get_First_Index (Array_Struct : Irep) return Irep
      with Pre => (Kind (Array_Struct) in Class_Expr
                   and then Kind (Get_Type (Array_Struct)) in
diff --git a/gnat2goto/driver/tree_walk.adb b/gnat2goto/driver/tree_walk.adb
@@ -4589,24 +4589,48 @@ package body Tree_Walk is
       procedure Handle_Representation_Clause (N : Node_Id) is
          Attr_Id : constant String := Get_Name_String (Chars (N));
          Target_Name : constant Irep := Do_Identifier (Name (N));
-         Entity_Esize : constant Integer :=
-           Integer (UI_To_Int (Esize (Entity (N))));
+         Entity_Esize : constant Uint := Esize (Entity (N));
          Target_Type_Irep : constant Irep :=
            Follow_Symbol_Type (Get_Type (Target_Name), Global_Symbol_Table);
+         Expression_Value : constant Uint := Intval (Expression (N));
       begin
-         if Kind (Target_Type_Irep) in Class_Type then
-            if Attr_Id = "size" then
-
-               --  Just check that the front-end already applied this size
-               --  clause, i .e. that the size of type-irep we already had
-               --  equals the entity type this clause is applied to (and the
-               --  size specified in this clause).
-               pragma Assert (Entity_Esize = Get_Width (Target_Type_Irep)
-                              and Entity_Esize =
-                                Integer (UI_To_Int (Intval (Expression (N)))));
+         pragma Assert (Kind (Target_Type_Irep) in Class_Type);
+         if Attr_Id = "size" then
+
+            --  Just check that the front-end already applied this size
+            --  clause, i .e. that the size of type-irep we already had
+            --  equals the entity type this clause is applied to (and the
+            --  size specified in this clause).
+            pragma Assert (Entity_Esize =
+                             UI_From_Int (Int (Get_Width (Target_Type_Irep)))
+                           and Entity_Esize = Expression_Value);
+            return;
+         elsif Attr_Id = "component_size" then
+            if not Is_Array_Type (Entity (N)) then
+               Report_Unhandled_Node_Empty (N, "Process_Declaration",
+                              "Component size only supported for array types");
                return;
             end if;
+            declare
+               Array_Data : constant Irep :=
+                 Get_Data_Component_From_Type (Target_Type_Irep);
+               Target_Subtype : constant Irep :=
+                 Follow_Symbol_Type (Get_Subtype (Get_Type (Array_Data)),
+                                     Global_Symbol_Table);
+               Target_Subtype_Width : constant Uint :=
+                 UI_From_Int (Int (Get_Width (Target_Subtype)));
+            begin
+               if Component_Size (Entity (N)) /= Expression_Value or
+                 Target_Subtype_Width /= Expression_Value
+               then
+                  Report_Unhandled_Node_Empty (N, "Process_Declaration",
+                      "Having component sizes be different from the size of " &
+                      "their underlying type is currently not supported");
+               end if;
+            end;
+            return;
          end if;
+
          Report_Unhandled_Node_Empty (N, "Process_Declaration",
                               "Representation clause unsupported: " & Attr_Id);
       end Handle_Representation_Clause;
diff --git a/testsuite/gnat2goto/tests/representation_clause_component_size/test.adb b/testsuite/gnat2goto/tests/representation_clause_component_size/test.adb
@@ -0,0 +1,17 @@
+procedure Test is
+   Storage_Unit : constant := 8;
+
+   type Storage_Offset is range
+     -(2 ** (Integer'(Standard'Address_Size) - 1)) ..
+     +(2 ** (Integer'(Standard'Address_Size) - 1)) - Long_Long_Integer'(1);
+
+   type Storage_Element is mod 2 ** Storage_Unit;
+
+   type Storage_Array is
+     array (Storage_Offset range <>) of aliased Storage_Element;
+   for Storage_Array'Component_Size use Storage_Unit;
+
+   My_Storage_Array : constant Storage_Array (1..5) := (1,2,3,4,5);
+begin
+   pragma Assert (My_Storage_Array(2)=2);
+end Test;
diff --git a/testsuite/gnat2goto/tests/representation_clause_component_size/test.out b/testsuite/gnat2goto/tests/representation_clause_component_size/test.out
@@ -0,0 +1,5 @@
+[precondition_instance.1] memcpy src/dst overlap: SUCCESS
+[precondition_instance.2] memcpy source region readable: SUCCESS
+[precondition_instance.3] memcpy destination region writeable: SUCCESS
+[1] file test.adb line 16 assertion: SUCCESS
+VERIFICATION SUCCESSFUL
diff --git a/testsuite/gnat2goto/tests/representation_clause_component_size/test.py b/testsuite/gnat2goto/tests/representation_clause_component_size/test.py
@@ -0,0 +1,3 @@
+from test_support import *
+
+prove()
diff --git a/testsuite/gnat2goto/tests/representation_clause_component_size_change/test.adb b/testsuite/gnat2goto/tests/representation_clause_component_size_change/test.adb
@@ -0,0 +1,18 @@
+procedure Test is
+   Storage_Unit : constant := 8;
+   Storage_Unit_Size : constant := 16;
+
+   type Storage_Offset is range
+     -(2 ** (Integer'(Standard'Address_Size) - 1)) ..
+     +(2 ** (Integer'(Standard'Address_Size) - 1)) - Long_Long_Integer'(1);
+
+   type Storage_Element is mod 2 ** Storage_Unit;
+
+   type Storage_Array is
+     array (Storage_Offset range <>) of aliased Storage_Element;
+   for Storage_Array'Component_Size use Storage_Unit_Size;
+
+   My_Storage_Array : constant Storage_Array (1..5) := (1,2,3,4,5);
+begin
+   pragma Assert (My_Storage_Array(2)=2);
+end Test;
diff --git a/testsuite/gnat2goto/tests/representation_clause_component_size_change/test.opt b/testsuite/gnat2goto/tests/representation_clause_component_size_change/test.opt
@@ -0,0 +1 @@
+ALL XFAIL gnat2goto fails with changing component size unsupported
diff --git a/testsuite/gnat2goto/tests/representation_clause_component_size_change/test.py b/testsuite/gnat2goto/tests/representation_clause_component_size_change/test.py
@@ -0,0 +1,3 @@
+from test_support import *
+
+prove()
