Address model

experiments/golden-results/StratoX-summary.txt

@@ -8,7 +8,7 @@ Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Precondition
 Nkind: N_Pragma
 --
-Occurs: 232 times
+Occurs: 231 times
 Calling function: Process_Declaration
 Error message: Unknown declaration kind
 Nkind: N_Validate_Unchecked_Conversion
@@ -1745,7 +1745,7 @@ Error detected at REDACTED
 --
 Occurs: 3 times
 +===========================GNAT BUG DETECTED==============================+
-| GNU Ada (ada2goto) Assert_Failure tree_walk.adb:999                      |
+| GNU Ada (ada2goto) Assert_Failure tree_walk.adb:998                      |
 Error detected at REDACTED
 --
 Occurs: 2 times
@@ -1760,6 +1760,11 @@ Error detected at REDACTED
 --
 Occurs: 1 times
 +===========================GNAT BUG DETECTED==============================+
+| GNU Ada (ada2goto) Assert_Failure atree.adb:992                          |
+Error detected at REDACTED
+--
+Occurs: 1 times
++===========================GNAT BUG DETECTED==============================+
 | GNU Ada (ada2goto) Assert_Failure failed precondition from arrays.ads:71 |
 Error detected at REDACTED
 --
@@ -2160,7 +2165,7 @@ Error detected at REDACTED
 --
 Occurs: 1 times
 +===========================GNAT BUG DETECTED==============================+
-| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.adb:72|
+| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.adb:71|
 Error detected at REDACTED
 --
 Occurs: 1 times
@@ -2232,11 +2237,6 @@ Occurs: 2 times
 <========================>
 raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from arrays.ads:51
 
---
-Occurs: 2 times
-<========================>
-raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from ireps.ads:1648
-
 --
 Occurs: 2 times
 <========================>
@@ -2245,5 +2245,5 @@ raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from range_check.a
 --
 Occurs: 1 times
 <========================>
-raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from tree_walk.adb:72
+raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from tree_walk.adb:71
 

experiments/golden-results/Tokeneer-summary.txt

@@ -1035,7 +1035,7 @@ Error detected at REDACTED
 --
 Occurs: 2 times
 +===========================GNAT BUG DETECTED==============================+
-| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:106|
+| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:109|
 Error detected at REDACTED
 --
 Occurs: 1 times
@@ -1105,17 +1105,17 @@ Error detected at REDACTED
 --
 Occurs: 1 times
 +===========================GNAT BUG DETECTED==============================+
-| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:106|
+| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:109|
 Error detected at REDACTED
 --
 Occurs: 1 times
 +===========================GNAT BUG DETECTED==============================+
-| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:106|
+| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:109|
 Error detected at REDACTED
 --
 Occurs: 1 times
 +===========================GNAT BUG DETECTED==============================+
-| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:106|
+| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:109|
 Error detected at REDACTED
 --
 Occurs: 1 times

experiments/golden-results/muen-summary.txt

@@ -3185,7 +3185,7 @@ Error detected at REDACTED
 --
 Occurs: 1 times
 +===========================GNAT BUG DETECTED==============================+
-| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:106|
+| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:109|
 Error detected at REDACTED
 --
 Occurs: 1 times

gnat2goto/driver/asvat-address_model.adb

@@ -0,0 +1,170 @@
+with GOTO_Utils;        use GOTO_Utils;
+with Nlists;            use Nlists;
+with Tree_Walk;         use Tree_Walk;
+with Sem_Util;          use Sem_Util;
+with Einfo;             use Einfo;
+with Namet;             use Namet;
+with Follow;            use Follow;
+package body ASVAT.Address_Model is
+
+   -------------------------
+   -- Do_ASVAT_Address_Of --
+   -------------------------
+
+   function Do_ASVAT_Address_Of (N : Node_Id) return Irep is
+   begin
+      return Make_Op_Typecast
+        (Op0             => Do_Address_Of (N),
+         Source_Location => Get_Source_Location (N),
+         I_Type          => Make_Pointer_Type
+           (I_Subtype => Make_Unsignedbv_Type (8),
+            Width     => Pointer_Type_Width),
+         Range_Check     => False);
+   end Do_ASVAT_Address_Of;
+
+   ------------------------------------
+   --  Get_Intrinsic_Address_Function -
+   ------------------------------------
+
+   function Get_Intrinsic_Address_Function (E : Entity_Id) return
+     Address_To_Access_Functions
+   is
+      Fun_Name : constant String := Get_Name_String (Chars (E));
+   begin
+      return (if Fun_Name = "to_pointer" then
+                 To_Pointer_Function
+              elsif Fun_Name = "to_address" then
+                 To_Address_Function
+              else
+                 Not_An_Address_Function);
+   end Get_Intrinsic_Address_Function;
+
+   ---------------------
+   -- Make_To_Pointer --
+   ---------------------
+
+   procedure Make_To_Pointer (E : Entity_Id) is
+      Address_Parameter  : constant Node_Id :=
+        First (Parameter_Specifications (Declaration_Node (E)));
+   begin
+      pragma Assert ((Present (Address_Parameter) and
+                       not Present (Next (Address_Parameter)))
+                     and then not Out_Present (Address_Parameter)
+                     and then
+                     Nkind (Parameter_Type (Address_Parameter)) in N_Has_Etype
+                     and then
+                     Unique_Name
+                       (Etype (Parameter_Type (Address_Parameter))) =
+                       "system__address",
+                     "The function To_Pointer must have a single in mode " &
+                       "parameter of type System.Address");
+
+      declare
+         Source_Location : constant Irep := Get_Source_Location (E);
+         Function_Name      : constant String := Unique_Name (E);
+         Function_Id        : constant Symbol_Id := Intern (Function_Name);
+         Function_Type      : constant Node_Id := Etype (E);
+
+         Param_Name : constant String :=
+           Unique_Name (Defining_Identifier (Address_Parameter));
+
+         Param_Type  : constant Irep :=
+           Do_Type_Reference (Etype (Parameter_Type (Address_Parameter)));
+
+         Param_Irep : constant Irep :=
+           Make_Symbol_Expr
+             (Source_Location => Get_Source_Location (Address_Parameter),
+              I_Type          => Param_Type,
+              Range_Check     => False,
+              Identifier      => Param_Name);
+
+         Return_Type : constant Irep := Follow_Symbol_Type
+           (Do_Type_Reference (Function_Type), Global_Symbol_Table);
+
+         Return_Statement : constant Irep :=
+           Make_Code_Return
+             (Return_Value    => Make_Op_Typecast
+                (Op0             => Param_Irep,
+                 Source_Location => Source_Location,
+                 I_Type          => Return_Type),
+              Source_Location => Source_Location,
+              I_Type          => Return_Type,
+              Range_Check     => False);
+
+         Function_Body : constant Irep := Make_Code_Block (Source_Location);
+
+         Function_Symbol : Symbol := Global_Symbol_Table (Function_Id);
+      begin
+         Append_Op (Function_Body, Return_Statement);
+
+         Function_Symbol.Value := Function_Body;
+         Global_Symbol_Table.Replace (Function_Id, Function_Symbol);
+      end;
+   end Make_To_Pointer;
+
+   ---------------------
+   -- To_Address --
+   ---------------------
+
+   procedure Make_To_Address (E : Entity_Id) is
+      Pointer_Parameter  : constant Node_Id :=
+        First (Parameter_Specifications (Declaration_Node (E)));
+      Function_Type      : constant Node_Id := Etype (E);
+   begin
+      pragma Assert ((Present (Pointer_Parameter) and
+                       not Present (Next (Pointer_Parameter)))
+                     and then not Out_Present (Pointer_Parameter)
+                     and then
+                     Kind (Do_Type_Reference
+                       (Etype (Parameter_Type (Pointer_Parameter)))) =
+                       I_Pointer_Type
+                     and then Unique_Name (Function_Type) = "system__address",
+                     "The function To_Address must have a single in mode " &
+                       "parameter of an access type");
+
+      declare
+         Source_Location : constant Irep := Get_Source_Location (E);
+         Function_Name      : constant String := Unique_Name (E);
+         Function_Id        : constant Symbol_Id := Intern (Function_Name);
+
+         Param_Name : constant String :=
+           Unique_Name (Defining_Identifier (Pointer_Parameter));
+
+         Param_Type  : constant Irep :=
+           Do_Type_Reference (Etype (Parameter_Type (Pointer_Parameter)));
+
+         Param_Irep : constant Irep :=
+           Make_Symbol_Expr
+             (Source_Location => Get_Source_Location (Pointer_Parameter),
+              I_Type          => Param_Type,
+              Range_Check     => False,
+              Identifier      => Param_Name);
+
+         Return_Type : constant Irep := Make_Pointer_Type
+                   (I_Subtype => Make_Unsignedbv_Type (8),
+                    Width     => Pointer_Type_Width);
+
+         Return_Statement : constant Irep :=
+           Make_Code_Return
+             (Return_Value    => Make_Op_Typecast
+                (Op0             => Param_Irep,
+                 Source_Location => Source_Location,
+                 I_Type          => Return_Type,
+                 Range_Check     => False),
+              Source_Location => Source_Location,
+              I_Type          => Return_Type,
+              Range_Check     => False);
+
+         Function_Body : constant Irep := Make_Code_Block (Source_Location);
+
+         Function_Symbol : Symbol := Global_Symbol_Table (Function_Id);
+      begin
+         Append_Op (Function_Body, Return_Statement);
+
+         Function_Symbol.Value := Function_Body;
+         Global_Symbol_Table.Replace (Function_Id, Function_Symbol);
+      end;
+
+   end Make_To_Address;
+
+end ASVAT.Address_Model;

gnat2goto/driver/asvat-address_model.ads

@@ -0,0 +1,25 @@
+with Types;               use Types;
+with Atree;               use Atree;
+with Sinfo;               use Sinfo;
+with Snames;              use Snames;
+with Ireps;               use Ireps;
+package ASVAT.Address_Model is
+
+   type Address_To_Access_Functions is
+     (Not_An_Address_Function, To_Pointer_Function, To_Address_Function);
+
+   function Do_ASVAT_Address_Of (N : Node_Id) return Irep
+     with Pre => Nkind (N) = N_Attribute_Reference and then
+     Get_Attribute_Id (Attribute_Name (N)) = Attribute_Address;
+
+   function Get_Intrinsic_Address_Function (E : Entity_Id) return
+     Address_To_Access_Functions;
+
+   procedure Make_To_Pointer (E : Entity_Id);
+--       with Pre => Is_Intrinsic_Subprogram (E) and
+--       Get_Name_String (Chars (E)) = "to_pointer";
+
+   procedure Make_To_Address (E : Entity_Id);
+--       with Pre => Is_Intrinsic_Subprogram (E) and
+--       Get_Name_String (Chars (E)) = "to_address";
+end ASVAT.Address_Model;

gnat2goto/driver/asvat.ads

@@ -0,0 +1,28 @@
+with Ada.Containers.Hashed_Maps;
+with Ada.Containers;            use Ada.Containers;
+with GNATCOLL.Symbols;
+with Symbol_Table_Info;         use Symbol_Table_Info;
+with Uintp;                     use Uintp;
+package ASVAT is
+private
+   type Entity_Info is record
+      Specified_Rep_Size           : Uint;
+      Specified_Rep_Component_Size : Uint;
+   end record;
+
+   Empty_Entity_Info : constant Entity_Info :=
+     (Specified_Rep_Size           => Uint_0,
+      Specified_Rep_Component_Size => Uint_0);
+
+   use type GNATCOLL.Symbols.Symbol;  --  for "=" operator
+
+   package Entity_Info_Maps is new Hashed_Maps
+     (Key_Type        => Symbol_Id,  --  Should be Entity_Id
+      Element_Type    => Entity_Info,
+      Hash            => GNATCOLL.Symbols.Hash,
+      Equivalent_Keys => "=");
+
+   subtype Entity_Info_Table is Entity_Info_Maps.Map;
+
+   Extra_Entity_Info : Entity_Info_Table;
+end ASVAT;

gnat2goto/driver/goto_utils.ads

@@ -85,7 +85,7 @@ package GOTO_Utils is
                                          BaseName :              String;
                                          Symbol_Type :           Irep;
                                          A_Symbol_Table : in out Symbol_Table)
-     with Pre => Kind (Symbol_Type) in Class_Type;
+     with Pre => Kind (Symbol_Type) in Class_Type | I_Address_Of_Expr;
 
    function New_Function_Symbol_Entry (Name : String; Symbol_Type : Irep;
                                        Value : Irep;