From 3817f0b3d2c636e2ef92286831362477025e352a Mon Sep 17 00:00:00 2001 From: Trevor Jennings Date: Thu, 28 May 2020 17:35:49 +0100 Subject: [PATCH 1/4] Add ASVAT address modelling features. --- gnat2goto/driver/asvat-address_model.adb | 170 +++++++++++++++++++++++ gnat2goto/driver/asvat-address_model.ads | 25 ++++ gnat2goto/driver/asvat.ads | 28 ++++ gnat2goto/driver/goto_utils.ads | 2 +- gnat2goto/driver/tree_walk.adb | 116 +++++++++++----- gnat2goto/driver/tree_walk.ads | 3 + 6 files changed, 311 insertions(+), 33 deletions(-) create mode 100644 gnat2goto/driver/asvat-address_model.adb create mode 100644 gnat2goto/driver/asvat-address_model.ads create mode 100644 gnat2goto/driver/asvat.ads diff --git a/gnat2goto/driver/asvat-address_model.adb b/gnat2goto/driver/asvat-address_model.adb new file mode 100644 index 000000000..fbc1c53ba --- /dev/null +++ b/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; diff --git a/gnat2goto/driver/asvat-address_model.ads b/gnat2goto/driver/asvat-address_model.ads new file mode 100644 index 000000000..58d5d01f6 --- /dev/null +++ b/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; diff --git a/gnat2goto/driver/asvat.ads b/gnat2goto/driver/asvat.ads new file mode 100644 index 000000000..c246614c8 --- /dev/null +++ b/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; diff --git a/gnat2goto/driver/goto_utils.ads b/gnat2goto/driver/goto_utils.ads index d8ced5eef..050de8677 100644 --- a/gnat2goto/driver/goto_utils.ads +++ b/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; diff --git a/gnat2goto/driver/tree_walk.adb b/gnat2goto/driver/tree_walk.adb index f8d692bb7..cca79233d 100644 --- a/gnat2goto/driver/tree_walk.adb +++ b/gnat2goto/driver/tree_walk.adb @@ -27,14 +27,12 @@ with Ada.Strings; with Ada.Strings.Fixed; with Ada.Characters.Handling; with Sinput; - +with ASVAT.Address_Model; use type + ASVAT.Address_Model.Address_To_Access_Functions; package body Tree_Walk is procedure Add_Entity_Substitution (E : Entity_Id; Subst : Irep); - function Do_Address_Of (N : Node_Id) return Irep - with Pre => Nkind (N) = N_Attribute_Reference; - function Do_Aggregate_Literal (N : Node_Id) return Irep with Pre => Nkind (N) = N_Aggregate; @@ -62,7 +60,8 @@ package body Tree_Walk is function Do_Constant (N : Node_Id) return Irep with Pre => Nkind (N) = N_Integer_Literal, - Post => Kind (Do_Constant'Result) = I_Constant_Expr; + Post => Kind (Do_Constant'Result) in + I_Constant_Expr | I_Op_Typecast; function Do_Character_Constant (N : Node_Id) return Irep with Pre => Nkind (N) = N_Character_Literal, @@ -1032,31 +1031,47 @@ package body Tree_Walk is Constant_Type : constant Irep := Do_Type_Reference (Etype (N)); Int_Val : constant Uint := Intval (N); Source_Loc : constant Irep := Get_Source_Location (N); - begin - if Etype (N) = Stand.Universal_Integer then - return Make_Constant_Expr + Is_Address : constant Boolean := + Unique_Name (Etype (N)) = "system__address"; + Is_Integer : constant Boolean := Etype (N) = Stand.Universal_Integer; + Is_BV : constant Boolean := + Kind (Constant_Type) in Class_Bitvector_Type; + + Const_Irep : constant Irep := + (if Is_Integer or Is_Address then + Make_Constant_Expr (Source_Location => Source_Loc, I_Type => Constant_Type, Range_Check => False, - Value => UI_Image (Int_Val, Decimal)); - end if; - - if not (Kind (Constant_Type) in Class_Bitvector_Type) - then + Value => UI_Image (Int_Val, Decimal)) + elsif Is_BV then + Make_Constant_Expr + (Source_Location => Source_Loc, + I_Type => Constant_Type, + Range_Check => False, + Value => + Convert_Uint_To_Hex (Int_Val, Pos (Get_Width (Constant_Type)))) + else + Make_Constant_Expr (Source_Location => Source_Loc, + I_Type => Constant_Type, + Range_Check => False, + Value => "0")); + begin + if not (Is_Integer or Is_BV or Is_Address) then Report_Unhandled_Node_Empty (N, "Do_Constant", "Unsupported constant type"); - return Make_Constant_Expr (Source_Location => Source_Loc, - I_Type => Constant_Type, - Range_Check => False, - Value => "0"); end if; - return Make_Constant_Expr - (Source_Location => Source_Loc, - I_Type => Constant_Type, - Range_Check => False, - Value => - Convert_Uint_To_Hex (Int_Val, Pos (Get_Width (Constant_Type)))); + return (if Is_Address then + Make_Op_Typecast + (Op0 => Const_Irep, + Source_Location => Get_Source_Location (N), + I_Type => Make_Pointer_Type + (I_Subtype => Make_Unsignedbv_Type (8), + Width => Pointer_Type_Width), + Range_Check => False) + else + Const_Irep); end Do_Constant; --------------------------- @@ -1366,9 +1381,8 @@ package body Tree_Walk is case Get_Attribute_Id (Attribute_Name (N)) is when Attribute_Access => return Do_Address_Of (N); when Attribute_Address => - -- The simplest way to model X'Address in ASVAT - -- is as an access to the object. - return Do_Address_Of (N); + -- Use the ASVAT.Address_Model to create the address. + return ASVAT.Address_Model.Do_ASVAT_Address_Of (N); when Attribute_Length => return Do_Array_Length (N); when Attribute_Range => return Report_Unhandled_Node_Irep (N, "Do_Expression", @@ -4934,9 +4948,35 @@ package body Tree_Walk is ------------------------------- procedure Do_Subprogram_Declaration (N : Node_Id) is + E : constant Node_Id := Defining_Unit_Name (Specification (N)); begin + pragma Assert (Ekind (E) in Subprogram_Kind); Register_Subprogram_Specification (Specification (N)); - -- Todo Aspect specifications + + if Is_Intrinsic_Subprogram (E) + and Nkind (Specification (N)) = N_Function_Specification + then + Check_For_Intrinsic_Address_Functions : + declare + Fun_Sort : constant + ASVAT.Address_Model.Address_To_Access_Functions := + ASVAT.Address_Model.Get_Intrinsic_Address_Function (E); + begin + if Fun_Sort = ASVAT.Address_Model.To_Pointer_Function then + -- Make a body for + -- function To_Pointer (System.Address) return access T. + ASVAT.Address_Model.Make_To_Pointer (E); + elsif Fun_Sort = ASVAT.Address_Model.To_Address_Function then + -- Make a body for + -- function To_Pointer (V : T) return Systen.Address. + ASVAT.Address_Model.Make_To_Address (E); + else + -- If the intrinsic funtion is not from an instatiation of + -- the System.Address_To_Access package nothing is done. + null; + end if; + end Check_For_Intrinsic_Address_Functions; + end if; end Do_Subprogram_Declaration; ---------------------------- @@ -5146,15 +5186,27 @@ package body Tree_Walk is procedure Do_Type_Declaration (New_Type_In : Irep; E : Entity_Id) is New_Type : constant Irep := New_Type_In; - New_Type_Name : constant Symbol_Id := Intern (Unique_Name (E)); + New_Type_Name : constant String := Unique_Name (E); + New_Type_Name_Id : constant Symbol_Id := Intern (New_Type_Name); New_Type_Symbol : constant Symbol := - Make_Type_Symbol (New_Type_Name, New_Type); + Make_Type_Symbol (New_Type_Name_Id, + (if New_Type_Name /= "system__address" then + -- For all type declarations except the + -- private type System.Address we use the + -- type declared in the source code. + New_Type + else + -- System.Address is modelled as a pointer + -- to a byte (an array of bytes). + Make_Pointer_Type + (I_Subtype => Make_Unsignedbv_Type (8), + Width => Pointer_Type_Width))); begin if Kind (New_Type) = I_Struct_Type then - Set_Tag (New_Type, Unintern (New_Type_Name)); + Set_Tag (New_Type, New_Type_Name); end if; - if not Symbol_Maps.Contains (Global_Symbol_Table, New_Type_Name) then - Symbol_Maps.Insert (Global_Symbol_Table, New_Type_Name, + if not Symbol_Maps.Contains (Global_Symbol_Table, New_Type_Name_Id) then + Symbol_Maps.Insert (Global_Symbol_Table, New_Type_Name_Id, New_Type_Symbol); end if; end Do_Type_Declaration; diff --git a/gnat2goto/driver/tree_walk.ads b/gnat2goto/driver/tree_walk.ads index e072ec1f3..2d0173bdd 100644 --- a/gnat2goto/driver/tree_walk.ads +++ b/gnat2goto/driver/tree_walk.ads @@ -102,6 +102,9 @@ package Tree_Walk is Post => Kind (Make_Malloc_Function_Call_Expr'Result) = I_Side_Effect_Expr_Function_Call; + function Do_Address_Of (N : Node_Id) return Irep + with Pre => Nkind (N) = N_Attribute_Reference; + function Do_Expression (N : Node_Id) return Irep with Pre => Nkind (N) in N_Subexpr, Post => Kind (Do_Expression'Result) in Class_Expr; From f2d2f68ec3bc88c84e2d0357488886a9947047cc Mon Sep 17 00:00:00 2001 From: Trevor Jennings Date: Thu, 28 May 2020 17:37:59 +0100 Subject: [PATCH 2/4] Add test cases for ASVAT address modelling. --- .../fixed_array_address_model.adb | 36 +++++++++++++++++++ .../tests/fixed_array_address_model/test.out | 13 +++++++ .../tests/fixed_array_address_model/test.py | 3 ++ .../record_address_model.adb | 33 +++++++++++++++++ .../tests/record_address_model/test.out | 14 ++++++++ .../tests/record_address_model/test.py | 3 ++ .../simple_address_model.adb | 32 +++++++++++++++++ .../tests/simple_address_model/test.out | 12 +++++++ .../tests/simple_address_model/test.py | 3 ++ .../tests/u_array_address_model/test.out | 18 ++++++++++ .../tests/u_array_address_model/test.py | 3 ++ .../u_array_address_model.adb | 36 +++++++++++++++++++ 12 files changed, 206 insertions(+) create mode 100644 testsuite/gnat2goto/tests/fixed_array_address_model/fixed_array_address_model.adb create mode 100644 testsuite/gnat2goto/tests/fixed_array_address_model/test.out create mode 100644 testsuite/gnat2goto/tests/fixed_array_address_model/test.py create mode 100644 testsuite/gnat2goto/tests/record_address_model/record_address_model.adb create mode 100644 testsuite/gnat2goto/tests/record_address_model/test.out create mode 100644 testsuite/gnat2goto/tests/record_address_model/test.py create mode 100644 testsuite/gnat2goto/tests/simple_address_model/simple_address_model.adb create mode 100644 testsuite/gnat2goto/tests/simple_address_model/test.out create mode 100644 testsuite/gnat2goto/tests/simple_address_model/test.py create mode 100644 testsuite/gnat2goto/tests/u_array_address_model/test.out create mode 100644 testsuite/gnat2goto/tests/u_array_address_model/test.py create mode 100644 testsuite/gnat2goto/tests/u_array_address_model/u_array_address_model.adb diff --git a/testsuite/gnat2goto/tests/fixed_array_address_model/fixed_array_address_model.adb b/testsuite/gnat2goto/tests/fixed_array_address_model/fixed_array_address_model.adb new file mode 100644 index 000000000..75ca068b2 --- /dev/null +++ b/testsuite/gnat2goto/tests/fixed_array_address_model/fixed_array_address_model.adb @@ -0,0 +1,36 @@ +with System; use type System.Address; +with System.Address_To_Access_Conversions; +procedure Fixed_Array_Address_Model is + + type My_Int is range 0 .. 100; + type My_Fixed_Array is array (1 .. 10) of My_Int; + + type Pointer is access all My_Fixed_Array; + + package Intrinsic_Address_To_Access_Conversions is new + System.Address_To_Access_Conversions (My_Fixed_Array); + use Intrinsic_Address_To_Access_Conversions; + + V : My_Fixed_Array; + PV : Pointer; +begin + for I in V'Range loop + V (I) := My_Int (I); + end loop; + + PV := Pointer (To_Pointer (V'Address)); + + for I in PV.all'Range loop + pragma Assert (PV.all (I) = My_Int (I)); + end loop; + + for I in PV.all'Range loop + PV.all (I) := My_Int (V'Last - I + 1); + end loop; + + for I in V'Range loop + pragma Assert (V (I) = My_Int (V'Last - I + 1)); + end loop; + + pragma Assert (V'Address = To_Address (Object_Pointer (PV))); +end Fixed_Array_Address_Model; diff --git a/testsuite/gnat2goto/tests/fixed_array_address_model/test.out b/testsuite/gnat2goto/tests/fixed_array_address_model/test.out new file mode 100644 index 000000000..b8bb9919c --- /dev/null +++ b/testsuite/gnat2goto/tests/fixed_array_address_model/test.out @@ -0,0 +1,13 @@ +Standard_Output from gnat2goto fixed_array_address_model: +----------At: Process_Pragma_Declaration---------- +----------Unknown pragma: compile_time_warning---------- +N_Pragma (Node_Id=3683) (source,analyzed) + Sloc = 19196 s-atacco.ads:42:4 [fixed_array_address_model.adb:10:4] + Pragma_Argument_Associations = List (List_Id=-99999824) + Pragma_Identifier = N_Identifier "compile_time_warning" (Node_Id=3695) + +[fixed_array_address_model.assertion.1] line 18 Ada Check assertion: SUCCESS +[fixed_array_address_model.assertion.2] line 24 assertion PV.all (I) = My_Int (I): SUCCESS +[fixed_array_address_model.assertion.3] line 32 assertion V (I) = My_Int (V'Last - I + 1): SUCCESS +[fixed_array_address_model.assertion.4] line 35 assertion V'Address = To_Address (Object_Pointer (PV)): SUCCESS +VERIFICATION SUCCESSFUL diff --git a/testsuite/gnat2goto/tests/fixed_array_address_model/test.py b/testsuite/gnat2goto/tests/fixed_array_address_model/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/fixed_array_address_model/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove() diff --git a/testsuite/gnat2goto/tests/record_address_model/record_address_model.adb b/testsuite/gnat2goto/tests/record_address_model/record_address_model.adb new file mode 100644 index 000000000..42040e495 --- /dev/null +++ b/testsuite/gnat2goto/tests/record_address_model/record_address_model.adb @@ -0,0 +1,33 @@ +with System; use type System.Address; +with System.Address_To_Access_Conversions; +procedure Record_Address_Model is + + type My_Int is range 0 .. 100; + type My_Record is record + A , B : My_Int; + end record; + + type Pointer is access all My_Record; + + package Intrinsic_Address_To_Access_Conversions is new + System.Address_To_Access_Conversions (My_Record); + use Intrinsic_Address_To_Access_Conversions; + + V : My_Record; + PV : Pointer; +begin + V.A := 3; + V.B := 5; + PV := Pointer (To_Pointer (V'Address)); + + pragma Assert (PV.all.A = 3); + pragma Assert (PV.all.B = 5); + + PV.all.A := 7; + PV.all.B := 11; + + pragma Assert (V.A = 7); + pragma Assert (V.B = 11); + + pragma Assert (V'Address = To_Address (Object_Pointer (PV))); +end Record_Address_Model; diff --git a/testsuite/gnat2goto/tests/record_address_model/test.out b/testsuite/gnat2goto/tests/record_address_model/test.out new file mode 100644 index 000000000..76575c797 --- /dev/null +++ b/testsuite/gnat2goto/tests/record_address_model/test.out @@ -0,0 +1,14 @@ +Standard_Output from gnat2goto record_address_model: +----------At: Process_Pragma_Declaration---------- +----------Unknown pragma: compile_time_warning---------- +N_Pragma (Node_Id=3577) (source,analyzed) + Sloc = 19196 s-atacco.ads:42:4 [record_address_model.adb:12:4] + Pragma_Argument_Associations = List (List_Id=-99999834) + Pragma_Identifier = N_Identifier "compile_time_warning" (Node_Id=3589) + +[record_address_model.assertion.1] line 23 assertion PV.all.A = 3: SUCCESS +[record_address_model.assertion.2] line 24 assertion PV.all.B = 5: SUCCESS +[record_address_model.assertion.3] line 29 assertion V.A = 7: SUCCESS +[record_address_model.assertion.4] line 30 assertion V.B = 11: SUCCESS +[record_address_model.assertion.5] line 32 assertion V'Address = To_Address (Object_Pointer (PV)): SUCCESS +VERIFICATION SUCCESSFUL diff --git a/testsuite/gnat2goto/tests/record_address_model/test.py b/testsuite/gnat2goto/tests/record_address_model/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/record_address_model/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove() diff --git a/testsuite/gnat2goto/tests/simple_address_model/simple_address_model.adb b/testsuite/gnat2goto/tests/simple_address_model/simple_address_model.adb new file mode 100644 index 000000000..18c07003a --- /dev/null +++ b/testsuite/gnat2goto/tests/simple_address_model/simple_address_model.adb @@ -0,0 +1,32 @@ +with System; use type System.Address; +with System.Address_To_Access_Conversions; +-- with System.Address_Image; +-- with Text_IO; use Text_IO; +procedure Simple_Address_Model is + + type My_Int is range 0 .. 100; + type Pointer is access all My_Int; + + package Intrinsic_Address_To_Access_Conversions is new + System.Address_To_Access_Conversions (My_Int); + use Intrinsic_Address_To_Access_Conversions; + + V : My_Int; + PV : Pointer; +begin + V := 3; + PV := Pointer (To_Pointer (V'Address)); + +-- Put_Line ("PV = " & My_Int'Image (PV.all)); + pragma Assert (PV.all = 3); + + PV.all := 5; + +-- Put_Line ("V = " & My_Int'Image (V)); + pragma Assert (V = 5); + +-- Put_Line ("V'Address = " & System.Address_Image (V'Address)); +-- Put_Line ("PV points to " & +-- System.Address_Image (To_Address (Object_Pointer (PV)))); + pragma Assert (V'Address = To_Address (Object_Pointer (PV))); +end Simple_Address_Model; diff --git a/testsuite/gnat2goto/tests/simple_address_model/test.out b/testsuite/gnat2goto/tests/simple_address_model/test.out new file mode 100644 index 000000000..e20fd66ff --- /dev/null +++ b/testsuite/gnat2goto/tests/simple_address_model/test.out @@ -0,0 +1,12 @@ +Standard_Output from gnat2goto simple_address_model: +----------At: Process_Pragma_Declaration---------- +----------Unknown pragma: compile_time_warning---------- +N_Pragma (Node_Id=3509) (source,analyzed) + Sloc = 19196 s-atacco.ads:42:4 [simple_address_model.adb:10:4] + Pragma_Argument_Associations = List (List_Id=-99999839) + Pragma_Identifier = N_Identifier "compile_time_warning" (Node_Id=3521) + +[simple_address_model.assertion.1] line 21 assertion PV.all = 3: SUCCESS +[simple_address_model.assertion.2] line 26 assertion V = 5: SUCCESS +[simple_address_model.assertion.3] line 31 assertion V'Address = To_Address (Object_Pointer (PV)): SUCCESS +VERIFICATION SUCCESSFUL diff --git a/testsuite/gnat2goto/tests/simple_address_model/test.py b/testsuite/gnat2goto/tests/simple_address_model/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/simple_address_model/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove() diff --git a/testsuite/gnat2goto/tests/u_array_address_model/test.out b/testsuite/gnat2goto/tests/u_array_address_model/test.out new file mode 100644 index 000000000..5eec940ca --- /dev/null +++ b/testsuite/gnat2goto/tests/u_array_address_model/test.out @@ -0,0 +1,18 @@ +Standard_Output from gnat2goto u_array_address_model: +----------At: Process_Pragma_Declaration---------- +----------Unknown pragma: compile_time_warning---------- +N_Pragma (Node_Id=3669) (source,analyzed) + Sloc = 19196 s-atacco.ads:42:4 [u_array_address_model.adb:10:4] + Pragma_Argument_Associations = List (List_Id=-99999824) + Pragma_Identifier = N_Identifier "compile_time_warning" (Node_Id=3681) + +Standard_Error from gnat2goto u_array_address_model: +u_array_address_model.adb:10:04: warning: in instantiation at s-atacco.ads:43 +u_array_address_model.adb:10:04: warning: Object is unconstrained array type +u_array_address_model.adb:10:04: warning: To_Pointer results may not have bounds + +[u_array_address_model.assertion.1] line 18 Ada Check assertion: SUCCESS +[u_array_address_model.assertion.2] line 24 assertion PV.all (I) = My_Int (I): SUCCESS +[u_array_address_model.assertion.3] line 32 assertion V (I) = My_Int (V'Last - I + 1): SUCCESS +[u_array_address_model.assertion.4] line 35 assertion V'Address = To_Address (Object_Pointer (PV)): SUCCESS +VERIFICATION SUCCESSFUL diff --git a/testsuite/gnat2goto/tests/u_array_address_model/test.py b/testsuite/gnat2goto/tests/u_array_address_model/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/u_array_address_model/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove() diff --git a/testsuite/gnat2goto/tests/u_array_address_model/u_array_address_model.adb b/testsuite/gnat2goto/tests/u_array_address_model/u_array_address_model.adb new file mode 100644 index 000000000..87b05bac9 --- /dev/null +++ b/testsuite/gnat2goto/tests/u_array_address_model/u_array_address_model.adb @@ -0,0 +1,36 @@ +with System; use type System.Address; +with System.Address_To_Access_Conversions; +procedure U_Array_Address_Model is + + type My_Int is range 0 .. 100; + type My_U_Array is array (Positive range <>) of My_Int; + + type Pointer is access all My_U_Array; + + package Intrinsic_Address_To_Access_Conversions is new + System.Address_To_Access_Conversions (My_U_Array); + use Intrinsic_Address_To_Access_Conversions; + + V : My_U_Array (1 ..10); + PV : Pointer; +begin + for I in V'Range loop + V (I) := My_Int (I); + end loop; + + PV := Pointer (To_Pointer (V'Address)); + + for I in V'Range loop + pragma Assert (PV.all (I) = My_Int (I)); + end loop; + + for I in V'Range loop + PV.all (I) := My_Int (V'Last - I + 1); + end loop; + + for I in V'Range loop + pragma Assert (V (I) = My_Int (V'Last - I + 1)); + end loop; + + pragma Assert (V'Address = To_Address (Object_Pointer (PV))); +end U_Array_Address_Model; From 4dabf5c4b254b829011cf1f43f436851f0206140 Mon Sep 17 00:00:00 2001 From: Trevor Jennings Date: Thu, 28 May 2020 17:39:45 +0100 Subject: [PATCH 3/4] Update golden results. --- experiments/golden-results/StratoX-summary.txt | 15 ++++++++++----- experiments/golden-results/Tokeneer-summary.txt | 8 ++++---- experiments/golden-results/muen-summary.txt | 2 +- 3 files changed, 15 insertions(+), 10 deletions(-) diff --git a/experiments/golden-results/StratoX-summary.txt b/experiments/golden-results/StratoX-summary.txt index 7686b8be8..c816008c0 100644 --- a/experiments/golden-results/StratoX-summary.txt +++ b/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 @@ -1760,7 +1760,12 @@ Error detected at REDACTED -- Occurs: 1 times +===========================GNAT BUG DETECTED==============================+ -| GNU Ada (ada2goto) Assert_Failure failed precondition from arrays.ads:71 | +| 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:51 | Error detected at REDACTED -- Occurs: 1 times @@ -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 @@ -2235,7 +2240,7 @@ 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 +raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from arrays.ads:57 -- Occurs: 2 times @@ -2245,5 +2250,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 diff --git a/experiments/golden-results/Tokeneer-summary.txt b/experiments/golden-results/Tokeneer-summary.txt index 18f085a2d..3612c4852 100644 --- a/experiments/golden-results/Tokeneer-summary.txt +++ b/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 diff --git a/experiments/golden-results/muen-summary.txt b/experiments/golden-results/muen-summary.txt index c9e5130cb..a9abf18b9 100644 --- a/experiments/golden-results/muen-summary.txt +++ b/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 From 60f7e8fdcb6832123c3b78d510b8ac2047edf2fe Mon Sep 17 00:00:00 2001 From: Trevor Jennings Date: Thu, 28 May 2020 18:40:07 +0100 Subject: [PATCH 4/4] Update small changes in StratoX-summary following rebase. --- experiments/golden-results/StratoX-summary.txt | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/experiments/golden-results/StratoX-summary.txt b/experiments/golden-results/StratoX-summary.txt index c816008c0..468c56848 100644 --- a/experiments/golden-results/StratoX-summary.txt +++ b/experiments/golden-results/StratoX-summary.txt @@ -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 @@ -1765,7 +1765,7 @@ Error detected at REDACTED -- Occurs: 1 times +===========================GNAT BUG DETECTED==============================+ -| GNU Ada (ada2goto) Assert_Failure failed precondition from arrays.ads:51 | +| GNU Ada (ada2goto) Assert_Failure failed precondition from arrays.ads:71 | Error detected at REDACTED -- Occurs: 1 times @@ -2237,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 arrays.ads:57 - -- Occurs: 2 times <========================>