Skip to content

Handle representation clause address #233

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 11 commits into
base: master
Choose a base branch
from
Open

Handle representation clause address #233

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
b1567bc
Unify creating integer constants
petr-bauch Jun 6, 2019
1f7f49a
Implement representation clause address
petr-bauch Jun 6, 2019
2db62c7
Wrap selected symbol in a dereference expression
petr-bauch Jun 6, 2019
3f2cd54
Introduce cprover_memory
petr-bauch Jun 6, 2019
22d8f04
Testcase for representation clause address
petr-bauch Jun 6, 2019
a80baf8
Decorate addressed variables
petr-bauch Jun 7, 2019
1b3ba7f
Implement handling the address attribute
petr-bauch Jun 7, 2019
2e228e2
Implement checking string prefix
petr-bauch Jun 7, 2019
35808eb
Add default body for some subprograms
petr-bauch Jun 7, 2019
0c60e2b
Extend the test to check the address
petr-bauch Jun 7, 2019
743d8d9
Update golden results
petr-bauch Jun 7, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion experiments/golden-results/StratoX-summary.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ Calling function: Do_Type_Definition
Error message: Access type unsupported
Nkind: N_Access_To_Object_Definition
--
Occurs: 42 times
Occurs: 39 times
Calling function: Do_Expression
Error message: Unknown attribute
Nkind: N_Attribute_Reference
Expand Down
46 changes: 40 additions & 6 deletions gnat2goto/driver/driver.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -200,7 +200,7 @@ package body Driver is
(I_Type => Dead_Object_Type,
Identifier => "__CPROVER_dead_object",
Source_Location => No_Location);
Dead_Object_Val : constant Irep := Integer_Constant_To_Expr
Dead_Object_Val : constant Irep := Integer_Constant_To_BV_Expr
(Value => Uint_0,
Expr_Type => Dead_Object_Type,
Source_Location => No_Location);
Expand All @@ -223,7 +223,7 @@ package body Driver is
(I_Type => Deallocated_Type,
Identifier => "__CPROVER_deallocated",
Source_Location => No_Location);
Deallocated_Val : constant Irep := Integer_Constant_To_Expr
Deallocated_Val : constant Irep := Integer_Constant_To_BV_Expr
(Value => Uint_0,
Expr_Type => Deallocated_Type,
Source_Location => No_Location);
Expand All @@ -246,7 +246,7 @@ package body Driver is
(I_Type => Malloc_Object_Type,
Identifier => "__CPROVER_malloc_object",
Source_Location => No_Location);
Malloc_Object_Val : constant Irep := Integer_Constant_To_Expr
Malloc_Object_Val : constant Irep := Integer_Constant_To_BV_Expr
(Value => Uint_0,
Expr_Type => Malloc_Object_Type,
Source_Location => No_Location);
Expand All @@ -260,6 +260,29 @@ package body Driver is
Source_Location => No_Location));
end Initialize_CProver_Malloc_Object;

procedure Initialize_CProver_Memory;
procedure Initialize_CProver_Memory is
Memory_Type : constant Irep := Make_Pointer_Type
(I_Subtype => Make_Void_Type,
Width => Pointer_Type_Width);
Memory_Sym : constant Irep := Make_Symbol_Expr
(I_Type => Memory_Type,
Identifier => "__CPROVER_memory",
Source_Location => No_Location);
Memory_Val : constant Irep := Integer_Constant_To_BV_Expr
(Value => Uint_0,
Expr_Type => Memory_Type,
Source_Location => No_Location);
begin
Declare_Missing_Global (Memory_Sym);
Append_Op
(Start_Body,
Make_Code_Assign
(Lhs => Memory_Sym,
Rhs => Memory_Val,
Source_Location => No_Location));
end Initialize_CProver_Memory;

procedure Initialize_Enum_Values;
procedure Initialize_Enum_Values is

Expand Down Expand Up @@ -348,6 +371,7 @@ package body Driver is
Initialize_CProver_Dead_Object;
Initialize_CProver_Deallocated;
Initialize_CProver_Malloc_Object;
Initialize_CProver_Memory;
Initialize_Enum_Values;
Initialize_Boolean_Values;
end Initialize_CProver_Internal_Variables;
Expand Down Expand Up @@ -705,10 +729,20 @@ package body Driver is
begin
Modified_Symbol.SymType :=
Remove_Extra_Type_Information
(Follow_Irep (SymType, Follow_Symbol'Access));
(Follow_Irep (SymType, Follow_Symbol'Access));
for K in 1 .. Addressed_Variables.Last loop
Modified_Symbol.SymType := Wrap_Pointer
(Modified_Symbol.SymType,
Addressed_Variables.Table (K).all);
end loop;
Modified_Symbol.Value :=
Remove_Extra_Type_Information
(Follow_Irep (Value, Follow_Symbol'Access));
Remove_Extra_Type_Information
(Follow_Irep (Value, Follow_Symbol'Access));
for K in 1 .. Addressed_Variables.Last loop
Modified_Symbol.Value := Wrap_Pointer
(Modified_Symbol.Value,
Addressed_Variables.Table (K).all);
end loop;

New_Table.Insert
(Key => Symbol_Maps.Key (Sym_Iter),
Expand Down
56 changes: 46 additions & 10 deletions gnat2goto/driver/goto_utils.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,18 @@ package body GOTO_Utils is
return R;
end Make_Address_Of;

function Is_Prefix (Prefix : String; Base_String : String) return Boolean
is
begin
if Prefix'Length < Base_String'Length and then
Prefix = Base_String (Base_String'First .. Prefix'Length)
then
return True;
else
return False;
end if;
end Is_Prefix;

-------------------
-- Make_Int_Type --
-------------------
Expand Down Expand Up @@ -141,6 +153,7 @@ package body GOTO_Utils is

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Slightly confused with the commit message here. Should it read "Add default body for some subprograms and add that to those that have identity-like type"?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry about the confusion, no: the commit body only specifies which are the some subprogram for which we generate the default body (those that have identity-like type, etc.).

procedure New_Subprogram_Symbol_Entry (Subprog_Name : Symbol_Id;
Subprog_Type : Irep;
Subprog_Body : Irep;
A_Symbol_Table : in out Symbol_Table)
is
Subprog_Symbol : Symbol;
Expand All @@ -150,7 +163,7 @@ package body GOTO_Utils is
Subprog_Symbol.PrettyName := Subprog_Name;
Subprog_Symbol.SymType := Subprog_Type;
Subprog_Symbol.Mode := Intern ("C");
Subprog_Symbol.Value := Make_Nil (No_Location);
Subprog_Symbol.Value := Subprog_Body;

A_Symbol_Table.Insert (Subprog_Name, Subprog_Symbol);
end New_Subprogram_Symbol_Entry;
Expand Down Expand Up @@ -351,17 +364,29 @@ package body GOTO_Utils is
A_Symbol_Table => A_Symbol_Table);
end Build_Function;

function Build_Identity_Body (Parameters : Irep) return Irep
is
Parameter_List : constant Irep_List := Get_Parameter (Parameters);
First_Cursor : constant List_Cursor := List_First (Parameter_List);
Body_Block : constant Irep :=
Make_Code_Block (Source_Location => No_Location,
I_Type => Make_Nil_Type);
begin
pragma Assert (List_Has_Element (Parameter_List, First_Cursor));
Append_Op (Body_Block,
Make_Code_Return (Return_Value =>
Param_Symbol (List_Element (Parameter_List, First_Cursor)),
Source_Location => No_Location,
I_Type => Make_Nil_Type));
return Body_Block;
end Build_Identity_Body;

function Build_Index_Constant (Value : Int; Source_Loc : Source_Ptr)
return Irep
is
Value_Hex : constant String :=
Convert_Uint_To_Hex (Value => UI_From_Int (Value),
Bit_Width => Size_T_Width);
begin
return Make_Constant_Expr (Source_Location => Source_Loc,
I_Type => CProver_Size_T,
Range_Check => False,
Value => Value_Hex);
begin
return Integer_Constant_To_Expr (UI_From_Int (Value), CProver_Size_T,
Size_T_Width, Source_Loc);
end Build_Index_Constant;

function Build_Array_Size (First : Irep; Last : Irep) return Irep
Expand Down Expand Up @@ -503,14 +528,25 @@ package body GOTO_Utils is
return False;
end Has_GNAT2goto_Annotation;

function Integer_Constant_To_BV_Expr
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't quite understand, are there non-bitvector types to which this is applicable?

Also, seems like this could be its own PR

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The CPROVER_Size_T is not a bit-vector type.

(Value : Uint;
Expr_Type : Irep;
Source_Location : Source_Ptr)
return Irep is
begin
return Integer_Constant_To_Expr (Value, Expr_Type, Get_Width (Expr_Type),
Source_Location);
end Integer_Constant_To_BV_Expr;

function Integer_Constant_To_Expr
(Value : Uint;
Expr_Type : Irep;
Type_Width : Integer;
Source_Location : Source_Ptr)
return Irep is
Value_Hex : constant String := Convert_Uint_To_Hex
(Value => Value,
Bit_Width => Pos (Get_Width (Expr_Type)));
Bit_Width => Pos (Type_Width));
begin
return Make_Constant_Expr
(Source_Location => Source_Location,
Expand Down
38 changes: 33 additions & 5 deletions gnat2goto/driver/goto_utils.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ with Atree; use Atree;
with Sinfo; use Sinfo;
with Symbol_Table_Info; use Symbol_Table_Info;
with Uintp; use Uintp;
with GNAT.Table;

package GOTO_Utils is

Expand All @@ -14,11 +15,22 @@ package GOTO_Utils is
-- Utility routines for high-level GOTO AST construction

Pointer_Type_Width : constant Positive := 64;
Size_T_Width : constant Int := 64;
Size_T_Width : constant Integer := 64;
-- ??? this should be queried at runtime from GNAT

Synthetic_Variable_Counter : Positive := 1;

type String_Access is access String;

function Is_Prefix (Prefix : String; Base_String : String) return Boolean;

package Addressed_Variables is new
GNAT.Table (Table_Component_Type => String_Access,
Table_Index_Type => Natural,
Table_Low_Bound => 1,
Table_Initial => 1,
Table_Increment => 20);

function Fresh_Var_Name (Infix : String) return String;
function Fresh_Var_Symbol_Expr (Ty : Irep; Infix : String) return Irep;

Expand Down Expand Up @@ -51,8 +63,10 @@ package GOTO_Utils is

procedure New_Subprogram_Symbol_Entry (Subprog_Name : Symbol_Id;
Subprog_Type : Irep;
Subprog_Body : Irep;
A_Symbol_Table : in out Symbol_Table)
with Pre => Kind (Subprog_Type) = I_Code_Type;
with Pre => Kind (Subprog_Type) = I_Code_Type
and Kind (Subprog_Body) in I_Nil | I_Code_Block;
-- Insert the subprogram specification into the symbol table

procedure New_Type_Symbol_Entry (Type_Name : Symbol_Id; Type_Of_Type : Irep;
Expand Down Expand Up @@ -104,6 +118,10 @@ package GOTO_Utils is
and then Kind (Func_Params) = I_Parameter_List
and then Kind (FBody) in Class_Code);

function Build_Identity_Body (Parameters : Irep) return Irep
with Pre => Kind (Parameters) = I_Parameter_List,
Post => Kind (Build_Identity_Body'Result) = I_Code_Block;

function Build_Array_Size (Array_Comp : Irep) return Irep
with Pre => Kind (Array_Comp) in Class_Expr,
Post => Kind (Build_Array_Size'Result) = I_Op_Add;
Expand All @@ -129,7 +147,8 @@ package GOTO_Utils is
function Float_Mantissa_Size (Float_Type : Irep) return Integer;

function Build_Index_Constant (Value : Int;
Source_Loc : Source_Ptr) return Irep;
Source_Loc : Source_Ptr) return Irep
with Post => Kind (Build_Index_Constant'Result) = I_Constant_Expr;

function Name_Has_Prefix (N : Node_Id; Prefix : String) return Boolean;

Expand All @@ -140,13 +159,22 @@ package GOTO_Utils is
-- checks whether an entity has a certain GNAT2goto annotation.
-- This can be either an aspect, or a pragma.

function Integer_Constant_To_Expr
function Integer_Constant_To_BV_Expr
(Value : Uint;
Expr_Type : Irep;
Source_Location : Source_Ptr)
return Irep
with Pre => Kind (Expr_Type) in Class_Bitvector_Type,
Post => Kind (Integer_Constant_To_Expr'Result) = I_Constant_Expr;
Post => Kind (Integer_Constant_To_BV_Expr'Result) = I_Constant_Expr;

function Integer_Constant_To_Expr
(Value : Uint;
Expr_Type : Irep;
Type_Width : Integer;
Source_Location : Source_Ptr)
return Irep
with Pre => Kind (Expr_Type) in Class_Type,
Post => Kind (Integer_Constant_To_Expr'Result) = I_Constant_Expr;

function Make_Simple_Side_Effect_Expr_Function_Call
(Arguments : Irep_Array;
Expand Down
Loading