Skip to content

Do cu specs #82

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

Closed
wants to merge 16 commits into from
Closed

Do cu specs #82

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
5e94b73
Corrected regression introduced when modified to write symbol table t…
tjj2017 Nov 1, 2018
6f6aa65
Modified Do_Compilation_Unit so that it first inserts declarations fr…
tjj2017 Nov 1, 2018
1001c3d
Separated out the processing of declarations and statements in prepar…
tjj2017 Nov 6, 2018
bd523a2
Merge remote-tracking branch 'diffblue/master' into do_cu_specs
tjj2017 Nov 6, 2018
3f5aa83
Added extra acceptable Nkinds to Process_Declaration to accept with N…
tjj2017 Nov 8, 2018
dc105aa
Put new subprograms into the correct place once I realised that all s…
tjj2017 Nov 20, 2018
8482297
Merge remote-tracking branch 'diffblue/master' into do_cu_specs
tjj2017 Nov 20, 2018
00fff9e
Existing subprogram Pragma was in the wrong place alphabetically
tjj2017 Nov 20, 2018
afd3376
Add subprograms to process withed package declarations.
tjj2017 Nov 20, 2018
8e1300b
Use Make_Nil instead of I_Code_Block to represent value of subprog de…
tjj2017 Nov 20, 2018
60c6f1e
All declarations now treated as Irep I_Code_Block.
tjj2017 Nov 22, 2018
255116c
Keep Process_Declarations as a procedure rather than a function as it…
tjj2017 Nov 22, 2018
7a7de4b
Avoid processing package declaration of System for the moment
tjj2017 Nov 22, 2018
0e187aa
Remove unused declaration
tjj2017 Nov 22, 2018
9eec7ee
Remove diagnostic print statements.
tjj2017 Nov 27, 2018
a7f0c4a
Remove the redundant "with Ada_Text_IO" clause as Ada_Text_IO contain…
tjj2017 Nov 27, 2018
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
212 changes: 107 additions & 105 deletions gnat2goto/driver/driver.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,9 +89,6 @@ package body Driver is
procedure Translate_Compilation_Unit (GNAT_Root : Node_Id)
is
pragma Assert (Nkind (GNAT_Root) = N_Compilation_Unit);
Add_Start : Boolean;
Program_Symbol : constant Symbol := Do_Compilation_Unit (GNAT_Root,
Add_Start);

Void_Type : constant Irep := New_Irep (I_Void_Type);

Expand All @@ -103,7 +100,17 @@ package body Driver is
Initial_Call : constant Irep := New_Irep (I_Code_Function_Call);
Initial_Call_Args : constant Irep := New_Irep (I_Argument_List);

Add_Start : Boolean;
Program_Symbol : constant Symbol := Do_Compilation_Unit (GNAT_Root,
Add_Start);

Sym_Tab_File : File_Type;
Base_Name : constant String :=
File_Name_Without_Suffix
(Get_Name_String (Unit_File_Name (Main_Unit)));
begin
Create (Sym_Tab_File, Out_File, Base_Name & ".json_symtab");

-- Gather local symbols and put them in the symtab
declare
Local_Symbols : Symbol_Table;
Expand All @@ -130,127 +137,122 @@ package body Driver is
end;

if not Add_Start then
Put_Line (Create (SymbolTable2Json (Global_Symbol_Table)).Write);
return;
end if;

Initialize_CProver_Internal_Variables (Start_Body);
declare
Program_Expr : constant Irep := New_Irep (I_Symbol_Expr);
Program_Type : constant Irep := Program_Symbol.SymType;
Program_Return_Type : constant Irep := Get_Return_Type (Program_Type);
Program_Args : constant Irep_List :=
Get_Parameter (Get_Parameters (Program_Type));
begin

-- Generate a simple _start function that calls the entry point
Put_Line (Sym_Tab_File,
Create (SymbolTable2Json (Global_Symbol_Table)).Write);
else
Initialize_CProver_Internal_Variables (Start_Body);
declare
C : List_Cursor := List_First (Program_Args);
Program_Expr : constant Irep := New_Irep (I_Symbol_Expr);
Program_Type : constant Irep := Program_Symbol.SymType;
Program_Return_Type : constant Irep :=
Get_Return_Type (Program_Type);
Program_Args : constant Irep_List :=
Get_Parameter (Get_Parameters (Program_Type));
begin
while List_Has_Element (Program_Args, C) loop
-- For each argument, declare and nondet-initialise a parameter
-- local and add it to the call argument list.
declare
Arg : constant Irep := List_Element (Program_Args, C);
Arg_Type : constant Irep := Get_Type (Arg);
Arg_Id : constant Symbol_Id :=
Intern ("input_" & Get_Identifier (Arg));
Arg_Symbol : Symbol;

Arg_Symbol_Expr : constant Irep := New_Irep (I_Symbol_Expr);
Arg_Decl : constant Irep := New_Irep (I_Code_Decl);
Arg_Nondet : constant Irep :=
New_Irep (I_Side_Effect_Expr_Nondet);
Arg_Assign : constant Irep := New_Irep (I_Code_Assign);

begin
Arg_Symbol.Name := Arg_Id;
Arg_Symbol.PrettyName := Arg_Id;
Arg_Symbol.BaseName := Arg_Id;
Arg_Symbol.Mode := Intern ("C");
Arg_Symbol.SymType := Arg_Type;
Arg_Symbol.IsStateVar := True;
Arg_Symbol.IsLValue := True;
Arg_Symbol.IsAuxiliary := True;
Global_Symbol_Table.Insert (Arg_Id, Arg_Symbol);

Set_Identifier (Arg_Symbol_Expr, Unintern (Arg_Id));
Set_Type (Arg_Symbol_Expr, Arg_Type);

Set_Symbol (Arg_Decl, Arg_Symbol_Expr);
Append_Op (Start_Body, Arg_Decl);

Set_Type (Arg_Nondet, Arg_Type);
Set_Lhs (Arg_Assign, Arg_Symbol_Expr);
Set_Rhs (Arg_Assign, Arg_Nondet);

Append_Op (Start_Body, Arg_Assign);

Append_Argument (Initial_Call_Args, Arg_Symbol_Expr);
end;
C := List_Next (Program_Args, C);
end loop;
end;
Set_Arguments (Initial_Call, Initial_Call_Args);

-- Catch the call's return value if it has one
if Kind (Program_Return_Type) /= I_Empty then
-- Generate a simple _start function that calls the entry point
declare
Return_Symbol : Symbol;

Return_Expr : constant Irep := New_Irep (I_Symbol_Expr);
Return_Decl : constant Irep := New_Irep (I_Code_Decl);
Return_Id : constant Symbol_Id := Intern ("return'");
C : List_Cursor := List_First (Program_Args);
begin
Return_Symbol.Name := Return_Id;
Return_Symbol.BaseName := Return_Id;
Return_Symbol.PrettyName := Return_Id;
Return_Symbol.Mode := Intern ("C");
Return_Symbol.SymType := Program_Return_Type;
Global_Symbol_Table.Insert (Return_Id, Return_Symbol);

Set_Identifier (Return_Expr, Unintern (Return_Id));
Set_Type (Return_Expr, Return_Symbol.SymType);
Set_Lhs (Initial_Call, Return_Expr);
Set_Symbol (Return_Decl, Return_Expr);
Append_Op (Start_Body, Return_Decl);
while List_Has_Element (Program_Args, C) loop
-- For each argument, declare and nondet-initialise a
-- parameter local and add it to the call argument list.
declare
Arg : constant Irep :=
List_Element (Program_Args, C);
Arg_Type : constant Irep := Get_Type (Arg);
Arg_Id : constant Symbol_Id :=
Intern ("input_" & Get_Identifier (Arg));
Arg_Symbol : Symbol;

Arg_Symbol_Expr : constant Irep :=
New_Irep (I_Symbol_Expr);
Arg_Decl : constant Irep :=
New_Irep (I_Code_Decl);
Arg_Nondet : constant Irep :=
New_Irep (I_Side_Effect_Expr_Nondet);
Arg_Assign : constant Irep :=
New_Irep (I_Code_Assign);

begin
Arg_Symbol.Name := Arg_Id;
Arg_Symbol.PrettyName := Arg_Id;
Arg_Symbol.BaseName := Arg_Id;
Arg_Symbol.Mode := Intern ("C");
Arg_Symbol.SymType := Arg_Type;
Arg_Symbol.IsStateVar := True;
Arg_Symbol.IsLValue := True;
Arg_Symbol.IsAuxiliary := True;
Global_Symbol_Table.Insert (Arg_Id, Arg_Symbol);

Set_Identifier (Arg_Symbol_Expr, Unintern (Arg_Id));
Set_Type (Arg_Symbol_Expr, Arg_Type);

Set_Symbol (Arg_Decl, Arg_Symbol_Expr);
Append_Op (Start_Body, Arg_Decl);

Set_Type (Arg_Nondet, Arg_Type);
Set_Lhs (Arg_Assign, Arg_Symbol_Expr);
Set_Rhs (Arg_Assign, Arg_Nondet);

Append_Op (Start_Body, Arg_Assign);

Append_Argument (Initial_Call_Args, Arg_Symbol_Expr);
end;
C := List_Next (Program_Args, C);
end loop;
end;
end if;
Set_Arguments (Initial_Call, Initial_Call_Args);

Set_Identifier (Program_Expr, Unintern (Program_Symbol.Name));
Set_Type (Program_Expr, Program_Symbol.SymType);
-- Catch the call's return value if it has one
if Kind (Program_Return_Type) /= I_Empty then
declare
Return_Symbol : Symbol;

Set_Function (Initial_Call, Program_Expr);
end;
Return_Expr : constant Irep := New_Irep (I_Symbol_Expr);
Return_Decl : constant Irep := New_Irep (I_Code_Decl);
Return_Id : constant Symbol_Id := Intern ("return'");
begin
Return_Symbol.Name := Return_Id;
Return_Symbol.BaseName := Return_Id;
Return_Symbol.PrettyName := Return_Id;
Return_Symbol.Mode := Intern ("C");
Return_Symbol.SymType := Program_Return_Type;
Global_Symbol_Table.Insert (Return_Id, Return_Symbol);

Set_Identifier (Return_Expr, Unintern (Return_Id));
Set_Type (Return_Expr, Return_Symbol.SymType);
Set_Lhs (Initial_Call, Return_Expr);
Set_Symbol (Return_Decl, Return_Expr);
Append_Op (Start_Body, Return_Decl);
end;
end if;

Append_Op (Start_Body, Initial_Call);
Set_Identifier (Program_Expr, Unintern (Program_Symbol.Name));
Set_Type (Program_Expr, Program_Symbol.SymType);

Start_Symbol.Name := Start_Name;
Start_Symbol.PrettyName := Start_Name;
Start_Symbol.BaseName := Start_Name;
Set_Function (Initial_Call, Program_Expr);
end;

Set_Return_Type (Start_Type, Void_Type);
Append_Op (Start_Body, Initial_Call);

Start_Symbol.SymType := Start_Type;
Start_Symbol.Value := Start_Body;
Start_Symbol.Mode := Intern ("C");
Start_Symbol.Name := Start_Name;
Start_Symbol.PrettyName := Start_Name;
Start_Symbol.BaseName := Start_Name;

Global_Symbol_Table.Insert (Start_Name, Start_Symbol);
Set_Return_Type (Start_Type, Void_Type);

declare
Sym_Tab_File : File_Type;
Base_Name : constant String :=
File_Name_Without_Suffix
(Get_Name_String (Unit_File_Name (Main_Unit)));
Start_Symbol.SymType := Start_Type;
Start_Symbol.Value := Start_Body;
Start_Symbol.Mode := Intern ("C");

begin
Create (Sym_Tab_File, Out_File, Base_Name & ".json_symtab");
Global_Symbol_Table.Insert (Start_Name, Start_Symbol);

Put_Line (Sym_Tab_File,
Create (SymbolTable2Json (Global_Symbol_Table)).Write);
end if;

Close (Sym_Tab_File);
end;
Close (Sym_Tab_File);
end Translate_Compilation_Unit;

function Is_Back_End_Switch (Switch : String) return Boolean is
Expand Down
Loading