Skip to content

Refactor symtab inserts #240

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

Merged
xbauch merged 7 commits into from
Jun 3, 2019
Merged

Refactor symtab inserts #240

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
9b802b3
Extract symbol intro from do_enumeration_definition
petr-bauch Jun 3, 2019
732eec8
Extract constant entry from do_object_declaration
petr-bauch Jun 3, 2019
ea55211
Extract new type entry
petr-bauch Jun 3, 2019
bede848
Call function-symbol-entry wrapper
petr-bauch Jun 3, 2019
e5dfde8
Extract subprogram symbol entry
petr-bauch Jun 3, 2019
06173f9
Use wrapper for new param symbol
petr-bauch Jun 3, 2019
30ea446
Introduce declared object into symbol table
petr-bauch Jun 3, 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
80 changes: 80 additions & 0 deletions gnat2goto/driver/goto_utils.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -121,6 +121,86 @@ package body GOTO_Utils is
return Ret;
end Symbol_Expr;

procedure New_Object_Symbol_Entry (Object_Name : Symbol_Id;
Copy link
Contributor

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue May 21, 2019

Choose a reason for hiding this comment

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

What's "object" in this context? We don't usually use that terminology in CBMC. I believe that's what GNAT calls an LValue? If so, this should have IsLValue set to true.

Copy link
Contributor Author

@xbauch xbauch May 21, 2019 •
edited
Loading

Choose a reason for hiding this comment

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

The object from do_object_declaration. I this it takes place when we declare variables. I've added setting the lvalue flag.

Object_Type : Irep;
Object_Init_Value : Irep;
A_Symbol_Table : in out Symbol_Table)
is
Object_Symbol : Symbol;
begin
Object_Symbol.Name := Object_Name;
Object_Symbol.BaseName := Object_Name;
Object_Symbol.PrettyName := Object_Name;
Object_Symbol.SymType := Object_Type;
Object_Symbol.Mode := Intern ("C");
Object_Symbol.Value := Object_Init_Value;
Object_Symbol.IsLValue := True;

A_Symbol_Table.Insert (Object_Name, Object_Symbol);
end New_Object_Symbol_Entry;

procedure New_Subprogram_Symbol_Entry (Subprog_Name : Symbol_Id;
Subprog_Type : Irep;
A_Symbol_Table : in out Symbol_Table)
is
Subprog_Symbol : Symbol;
begin
Subprog_Symbol.Name := Subprog_Name;
Subprog_Symbol.BaseName := Subprog_Name;
Subprog_Symbol.PrettyName := Subprog_Name;
Subprog_Symbol.SymType := Subprog_Type;
Subprog_Symbol.Mode := Intern ("C");
Subprog_Symbol.Value := Make_Nil (No_Location);

A_Symbol_Table.Insert (Subprog_Name, Subprog_Symbol);
end New_Subprogram_Symbol_Entry;

procedure New_Type_Symbol_Entry (Type_Name : Symbol_Id; Type_Of_Type : Irep;
Copy link
Contributor

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue May 31, 2019

Choose a reason for hiding this comment

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

That kind of makes it sound like we have higher kinded types? I honestly don't really have a fantastic idea of what to name this either though.

A_Symbol_Table : in out Symbol_Table) is
Type_Symbol : Symbol;
begin
Type_Symbol.SymType := Type_Of_Type;
Type_Symbol.IsType := True;
Type_Symbol.Name := Type_Name;
Type_Symbol.PrettyName := Type_Name;
Type_Symbol.BaseName := Type_Name;
Type_Symbol.Mode := Intern ("C");

A_Symbol_Table.Insert (Type_Name, Type_Symbol);
end New_Type_Symbol_Entry;

procedure New_Valueless_Object_Symbol_Entry (Constant_Name : Symbol_Id;
A_Symbol_Table : in out Symbol_Table)
is
Object_Symbol : Symbol;
begin
Object_Symbol.Name := Constant_Name;
Object_Symbol.BaseName := Constant_Name;
Object_Symbol.PrettyName := Constant_Name;
Object_Symbol.SymType := Make_Nil (No_Location);
Object_Symbol.Mode := Intern ("C");
Object_Symbol.Value := Make_Nil (No_Location);

A_Symbol_Table.Insert (Constant_Name, Object_Symbol);
end New_Valueless_Object_Symbol_Entry;

procedure New_Enum_Member_Symbol_Entry (
Member_Name : Symbol_Id; Base_Name : Symbol_Id; Enum_Type : Irep;
Value_Expr : Irep; A_Symbol_Table : in out Symbol_Table) is
Member_Symbol : Symbol;
begin
Member_Symbol.Name := Member_Name;
Member_Symbol.PrettyName := Base_Name;
Member_Symbol.BaseName := Base_Name;
Member_Symbol.Mode := Intern ("C");
Member_Symbol.IsStaticLifetime := True;
Member_Symbol.IsStateVar := True;
Member_Symbol.SymType := Enum_Type;
Member_Symbol.Value := Value_Expr;

A_Symbol_Table.Insert (Member_Symbol.Name, Member_Symbol);
end New_Enum_Member_Symbol_Entry;

--------------------------------
-- New_Parameter_Symbol_Entry --
--------------------------------
Expand Down
25 changes: 25 additions & 0 deletions gnat2goto/driver/goto_utils.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,31 @@ package GOTO_Utils is
function Symbol_Expr (Sym : Symbol) return Irep
with Post => Kind (Symbol_Expr'Result) = I_Symbol_Expr;

procedure New_Object_Symbol_Entry (Object_Name : Symbol_Id;
Object_Type : Irep;
Object_Init_Value : Irep;
A_Symbol_Table : in out Symbol_Table)
with Pre => Kind (Object_Type) in Class_Type
and (Object_Init_Value = Ireps.Empty
or else Kind (Object_Init_Value) in Class_Expr);

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

procedure New_Type_Symbol_Entry (Type_Name : Symbol_Id; Type_Of_Type : Irep;
A_Symbol_Table : in out Symbol_Table)
with Pre => Kind (Type_Of_Type) in Class_Type;

procedure New_Valueless_Object_Symbol_Entry (Constant_Name : Symbol_Id;
A_Symbol_Table : in out Symbol_Table);

procedure New_Enum_Member_Symbol_Entry (
Member_Name : Symbol_Id; Base_Name : Symbol_Id; Enum_Type : Irep;
Value_Expr : Irep; A_Symbol_Table : in out Symbol_Table);

procedure New_Parameter_Symbol_Entry (Name_Id : Symbol_Id;
BaseName : String;
Symbol_Type : Irep;
Expand Down
111 changes: 41 additions & 70 deletions gnat2goto/driver/tree_walk.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1275,7 +1275,6 @@ package body Tree_Walk is
UI_Image (Enumeration_Rep (Member));
Val_Name : constant String := Unique_Name (Member);
Base_Name : constant String := Get_Name_String (Chars (Member));
Member_Symbol : Symbol;
Member_Symbol_Init : constant Irep := New_Irep (I_Constant_Expr);
Typecast_Expr : constant Irep := New_Irep (I_Op_Typecast);
Member_Size : constant Int := UI_To_Int (Esize (Etype (Member)));
Expand All @@ -1284,22 +1283,18 @@ package body Tree_Walk is
Set_Identifier (Element, Val_Name);
Set_Basename (Element, Base_Name);
Append_Member (Enum_Body, Element);
Member_Symbol.Name := Intern (Val_Name);
Member_Symbol.PrettyName := Intern (Base_Name);
Member_Symbol.BaseName := Intern (Base_Name);
Member_Symbol.Mode := Intern ("C");
Member_Symbol.IsStaticLifetime := True;
Member_Symbol.IsStateVar := True;
Member_Symbol.SymType := Enum_Type_Symbol;
Set_Type (Member_Symbol_Init,
Make_Int_Type (Integer (Member_Size)));
Set_Value (Member_Symbol_Init,
Convert_Uint_To_Hex (Enumeration_Rep (Member),
Member_Size));
Set_Op0 (Typecast_Expr, Member_Symbol_Init);
Set_Type (Typecast_Expr, Enum_Type_Symbol);
Member_Symbol.Value := Typecast_Expr;
Global_Symbol_Table.Insert (Member_Symbol.Name, Member_Symbol);
New_Enum_Member_Symbol_Entry (Member_Name => Intern (Val_Name),
Base_Name => Intern (Base_Name),
Enum_Type => Enum_Type_Symbol,
Value_Expr => Typecast_Expr,
A_Symbol_Table => Global_Symbol_Table);
end;
Next (Member);
exit when not Present (Member);
Expand Down Expand Up @@ -2633,25 +2628,6 @@ package body Tree_Walk is
-- declaration has the pragma Import applied.
Full_View_Entity : constant Entity_Id := Full_View (Entity);

procedure Register_Constant_In_Symbol_Table (N : Node_Id);
-- Adds a dummy entry to the symbol table to register that a
-- constant has already been processed.

procedure Register_Constant_In_Symbol_Table (N : Node_Id) is
Constant_Name : constant Symbol_Id :=
Intern (Unique_Name (Defining_Identifier (N)));
Constant_Symbol : Symbol;
begin
Constant_Symbol.Name := Constant_Name;
Constant_Symbol.BaseName := Constant_Name;
Constant_Symbol.PrettyName := Constant_Name;
Constant_Symbol.SymType := Make_Nil (Sloc (N));
Constant_Symbol.Mode := Intern ("C");
Constant_Symbol.Value := Make_Nil (Sloc (N));
Global_Symbol_Table.Insert (Constant_Name, Constant_Symbol);

end Register_Constant_In_Symbol_Table;

begin
if not Has_Init_Expression (N) and then
Present (Full_View_Entity)
Expand All @@ -2664,7 +2640,12 @@ package body Tree_Walk is
-- register it in the symbol table so that it is not
-- processed again when the completion is encountered in
-- the tree.
Register_Constant_In_Symbol_Table (N);
New_Valueless_Object_Symbol_Entry (Intern (Unique_Name
(Defining_Identifier (N))),
Global_Symbol_Table);
-- Adds a dummy entry to the symbol table to register that a
-- constant has already been processed.

Do_Object_Declaration_Full
(Declaration_Node (Full_View_Entity), Block);
else
Expand All @@ -2675,6 +2656,7 @@ package body Tree_Walk is
end;
end if;

pragma Assert (Global_Symbol_Table.Contains (Obj_Id));
end Do_Object_Declaration;

--------------------------------------------
Expand All @@ -2688,6 +2670,9 @@ package body Tree_Walk is
Decl : constant Irep := New_Irep (I_Code_Decl);
Init_Expr : Irep := Ireps.Empty;

Obj_Id : constant Symbol_Id := Intern (Unique_Name (Defined));
Obj_Type : constant Irep := Get_Type (Id);

function Has_Defaulted_Components (E : Entity_Id) return Boolean;
function Needs_Default_Initialisation (E : Entity_Id) return Boolean;
function Disc_Expr (N : Node_Id) return Node_Id;
Expand Down Expand Up @@ -2941,9 +2926,6 @@ package body Tree_Walk is
end Make_Default_Initialiser;

-- Begin processing for Do_Object_Declaration_Full_Declaration

Is_In_Symtab : constant Boolean :=
Global_Symbol_Table.Contains (Intern (Get_Identifier (Id)));
begin
Set_Source_Location (Decl, (Sloc (N)));
Set_Symbol (Decl, Id);
Expand All @@ -2964,14 +2946,22 @@ package body Tree_Walk is
end;
end if;

if not Global_Symbol_Table.Contains (Obj_Id)
then
New_Object_Symbol_Entry (Object_Name => Obj_Id,
Object_Type => Obj_Type,
Object_Init_Value => Init_Expr,
A_Symbol_Table => Global_Symbol_Table);
end if;

if Init_Expr /= Ireps.Empty then
Append_Op (Block, Make_Code_Assign (Lhs => Id,
Rhs => Typecast_If_Necessary (Init_Expr, Get_Type (Id),
Global_Symbol_Table),
Source_Location => Sloc (N)));
end if;

if not Is_In_Symtab then
if not Global_Symbol_Table.Contains (Intern (Get_Identifier (Id))) then
Register_Identifier_In_Symbol_Table
(Id, Init_Expr, Global_Symbol_Table);
end if;
Expand Down Expand Up @@ -4155,7 +4145,6 @@ package body Tree_Walk is
Unique_Name (Defining_Identifier (Param_Iter));

Param_Irep : constant Irep := New_Irep (I_Code_Parameter);
Param_Symbol : Symbol;
begin
if not (Nkind (Parameter_Type (Param_Iter)) in N_Has_Etype) then
Report_Unhandled_Node_Empty (N, "Do_Subprogram_Specification",
Expand All @@ -4174,15 +4163,10 @@ package body Tree_Walk is
Set_Base_Name (Param_Irep, Param_Name);
Append_Parameter (Param_List, Param_Irep);
-- Add the param to the symtab as well:
Param_Symbol.Name := Intern (Param_Name);
Param_Symbol.PrettyName := Param_Symbol.Name;
Param_Symbol.BaseName := Param_Symbol.Name;
Param_Symbol.SymType := Param_Type;
Param_Symbol.IsThreadLocal := True;
Param_Symbol.IsFileLocal := True;
Param_Symbol.IsLValue := True;
Param_Symbol.IsParameter := True;
Global_Symbol_Table.Insert (Param_Symbol.Name, Param_Symbol);
New_Parameter_Symbol_Entry (Name_Id => Intern (Param_Name),
BaseName => Param_Name,
Symbol_Type => Param_Type,
A_Symbol_Table => Global_Symbol_Table);
Next (Param_Iter);
end;
end loop;
Expand Down Expand Up @@ -4424,17 +4408,12 @@ package body Tree_Walk is
Number_Str : constant String :=
Number_Str_Raw (2 .. Number_Str_Raw'Last);
Fresh_Name : constant String := "__anonymous_type_" & Number_Str;
Type_Symbol : Symbol;
begin
Anonymous_Type_Counter := Anonymous_Type_Counter + 1;

Type_Symbol.SymType := Actual_Type;
Type_Symbol.IsType := True;
Type_Symbol.Name := Intern (Fresh_Name);
Type_Symbol.PrettyName := Intern (Fresh_Name);
Type_Symbol.BaseName := Intern (Fresh_Name);
Type_Symbol.Mode := Intern ("C");
Global_Symbol_Table.Insert (Intern (Fresh_Name), Type_Symbol);
New_Type_Symbol_Entry (Type_Name => Intern (Fresh_Name),
Type_Of_Type => Actual_Type,
A_Symbol_Table => Global_Symbol_Table);

Set_Identifier (Ret, Fresh_Name);

Expand Down Expand Up @@ -4510,6 +4489,7 @@ package body Tree_Walk is
-- Create the check function on demand:
declare
Fn_Symbol : Symbol;
Fn_Name : constant String := "__ada_runtime_check";
Assertion : constant Irep := New_Irep (I_Code_Assert);
Formal_Params : constant Irep := New_Irep (I_Parameter_List);
Formal_Param : constant Irep := New_Irep (I_Code_Parameter);
Expand All @@ -4527,15 +4507,14 @@ package body Tree_Walk is
Set_Return_Type (Fn_Type, Void_Type);
Set_Assertion (Assertion, Formal_Expr);

Fn_Symbol.Name := Intern ("__ada_runtime_check");
Fn_Symbol.PrettyName := Fn_Symbol.Name;
Fn_Symbol.BaseName := Fn_Symbol.Name;
Fn_Symbol.Value := Assertion;
Fn_Symbol.SymType := Fn_Type;
Global_Symbol_Table.Insert (Fn_Symbol.Name, Fn_Symbol);
Fn_Symbol :=
Copy link
Contributor

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue May 21, 2019

Choose a reason for hiding this comment

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

Can this be moved up to the declaration, and the symbol be made constant now?

Copy link
Contributor Author

@xbauch xbauch May 21, 2019

Choose a reason for hiding this comment

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

Well we are changing the assertion that will comprise the value of this symbol.

New_Function_Symbol_Entry (Name => Fn_Name,
Symbol_Type => Fn_Type,
Value => Assertion,
A_Symbol_Table => Global_Symbol_Table);

Check_Function_Symbol := New_Irep (I_Symbol_Expr);
Set_Identifier (Check_Function_Symbol, Unintern (Fn_Symbol.Name));
Set_Identifier (Check_Function_Symbol, Fn_Name);
Set_Type (Check_Function_Symbol, Fn_Symbol.SymType);
end;
end if;
Expand Down Expand Up @@ -5303,18 +5282,10 @@ package body Tree_Walk is
Do_Subprogram_Specification (N);
Subprog_Name : constant Symbol_Id :=
Intern (Unique_Name (Defining_Unit_Name (N)));

Subprog_Symbol : Symbol;

begin
Subprog_Symbol.Name := Subprog_Name;
Subprog_Symbol.BaseName := Subprog_Name;
Subprog_Symbol.PrettyName := Subprog_Name;
Subprog_Symbol.SymType := Subprog_Type;
Subprog_Symbol.Mode := Intern ("C");
Subprog_Symbol.Value := Make_Nil (Sloc (N));

Global_Symbol_Table.Insert (Subprog_Name, Subprog_Symbol);
New_Subprogram_Symbol_Entry (Subprog_Name => Subprog_Name,
Subprog_Type => Subprog_Type,
A_Symbol_Table => Global_Symbol_Table);
end Register_Subprogram_Specification;

-------------------------------
Expand Down