Skip to content

Commit e25a0cb

Browse files
Petr BauchPetr Bauch
Petr Bauch
authored and
Petr Bauch
committed
Fix based on comments
1 parent fc32b97 commit e25a0cb

File tree

3 files changed

+138
-80
lines changed

3 files changed

+138
-80
lines changed

‎gnat2goto/driver/goto_utils.adb

Lines changed: 78 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@ with Namet; use Namet;
22
with Nlists; use Nlists;
33
with Aspects; use Aspects;
44

5+
with Ada.Text_IO; use Ada.Text_IO;
6+
57
package body GOTO_Utils is
68

79
---------------------
@@ -92,39 +94,97 @@ package body GOTO_Utils is
9294
return Ret;
9395
end Symbol_Expr;
9496

95-
--------------------------
96-
-- Create_Fun_Parameter --
97-
--------------------------
97+
--------------------------------
98+
-- New_Parameter_Symbol_Entry --
99+
--------------------------------
100+
101+
procedure New_Parameter_Symbol_Entry (Name_Id : Symbol_Id;
102+
BaseName : String;
103+
Symbol_Type : Irep;
104+
A_Symbol_Table : in out Symbol_Table)
105+
is
106+
New_Symbol : Symbol;
107+
begin
108+
New_Symbol.SymType := Symbol_Type;
109+
New_Symbol.Name := Name_Id;
110+
New_Symbol.PrettyName := Intern (BaseName);
111+
New_Symbol.BaseName := Intern (BaseName);
112+
New_Symbol.Mode := Intern ("C");
113+
114+
-- Setting it as a parameter
115+
New_Symbol.IsParameter := True;
116+
New_Symbol.IsLValue := True;
117+
New_Symbol.IsFileLocal := True;
118+
New_Symbol.IsThreadLocal := True;
119+
120+
if A_Symbol_Table.Contains (Key => Name_Id) then
121+
Put_Line (Standard_Error,
122+
"----------At: New_Parameter_Symbol_Entry----------");
123+
Put_Line (Standard_Error,
124+
"----------Trying to create known symbol.----------");
125+
Put_Line (Standard_Error, "----------" & BaseName & "----------");
126+
else
127+
A_Symbol_Table.Insert (Name_Id, New_Symbol);
128+
end if;
129+
end New_Parameter_Symbol_Entry;
130+
131+
-------------------------------
132+
-- New_Function_Symbol_Entry --
133+
-------------------------------
98134

135+
function New_Function_Symbol_Entry (Name : String; Symbol_Type : Irep;
136+
Value : Irep;
137+
A_Symbol_Table : in out Symbol_Table)
138+
return Symbol is
139+
New_Symbol : Symbol;
140+
begin
141+
New_Symbol.SymType := Symbol_Type;
142+
New_Symbol.Name := Intern (Name);
143+
New_Symbol.PrettyName := New_Symbol.Name;
144+
New_Symbol.BaseName := New_Symbol.Name;
145+
New_Symbol.Mode := Intern ("C");
146+
New_Symbol.Value := Value;
147+
148+
if A_Symbol_Table.Contains (Key => Intern (Name)) then
149+
Put_Line (Standard_Error,
150+
"----------At: New_Function_Symbol_Entry----------");
151+
Put_Line (Standard_Error,
152+
"----------Trying to create known symbol.----------");
153+
Put_Line (Standard_Error, "----------" & Name & "----------");
154+
else
155+
A_Symbol_Table.Insert (Intern (Name), New_Symbol);
156+
end if;
157+
return New_Symbol;
158+
end New_Function_Symbol_Entry;
159+
160+
--------------------------
161+
-- Create_Fun_Parameter --
162+
--------------------------
163+
164+
-- To be called when one needs to build a function inside gnat2goto
165+
-- Modifies symbol table and Param_List as a side effect
166+
-- Returns irep of type I_Code_Parameter
99167
function Create_Fun_Parameter (Fun_Name : String; Param_Name : String;
100168
Param_Type : Irep; Param_List : Irep;
101169
A_Symbol_Table : in out Symbol_Table;
102170
Source_Location : Source_Ptr := No_Location)
103171
return Irep is
104172
Func_Param_Id : constant Symbol_Id := Intern (Fun_Name & Param_Name);
105-
Value_Symbol : constant Symbol := (Name => Func_Param_Id,
106-
BaseName => Intern (Param_Name),
107-
PrettyName => Intern (Param_Name),
108-
Mode => Intern ("C"),
109-
SymType => Param_Type,
110-
IsParameter => True,
111-
IsLValue => True,
112-
IsFileLocal => True,
113-
IsThreadLocal => True,
114-
others => <>);
173+
-- Create an irep for the parameter
115174
Value_Arg : constant Irep :=
116175
Make_Code_Parameter (Source_Location => Source_Location,
117176
Default_Value => Ireps.Empty,
177+
I_Type => Param_Type,
118178
Base_Name => Param_Name,
119179
This => False,
120180
Identifier => Unintern (Func_Param_Id));
121181
begin
122-
A_Symbol_Table.Insert (Func_Param_Id, Value_Symbol);
123-
Set_Type (Value_Arg, Param_Type);
124-
Set_Identifier (Value_Arg, Unintern (Func_Param_Id));
125-
Set_Base_Name (Value_Arg, "value");
182+
-- Creates a symbol for the parameter
183+
New_Parameter_Symbol_Entry (Name_Id => Func_Param_Id,
184+
BaseName => Param_Name,
185+
Symbol_Type => Param_Type,
186+
A_Symbol_Table => A_Symbol_Table);
126187
Append_Parameter (Param_List, Value_Arg);
127-
128188
return Value_Arg;
129189
end Create_Fun_Parameter;
130190

‎gnat2goto/driver/goto_utils.ads

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,17 @@ package GOTO_Utils is
2727
Post => Kind (Param_Symbol'Result) = I_Symbol_Expr;
2828

2929
function Symbol_Expr (Sym : Symbol) return Irep
30-
with Post => Kind (Symbol_Expr'Result) = I_Symbol_Expr;
30+
with Post => Kind (Symbol_Expr'Result) = I_Symbol_Expr;
31+
32+
procedure New_Parameter_Symbol_Entry (Name_Id : Symbol_Id;
33+
BaseName : String;
34+
Symbol_Type : Irep;
35+
A_Symbol_Table : in out Symbol_Table);
36+
37+
function New_Function_Symbol_Entry (Name : String; Symbol_Type : Irep;
38+
Value : Irep;
39+
A_Symbol_Table : in out Symbol_Table)
40+
return Symbol;
3141

3242
function Create_Fun_Parameter (Fun_Name : String; Param_Name : String;
3343
Param_Type : Irep; Param_List : Irep;

‎gnat2goto/driver/tree_walk.adb

Lines changed: 49 additions & 61 deletions
Original file line numberDiff line numberDiff line change
@@ -30,9 +30,6 @@ package body Tree_Walk is
3030
procedure Append_Declare_And_Init
3131
(Symbol : Irep; Value : Irep; Block : Irep; Source_Loc : Source_Ptr);
3232

33-
function Add_To_Table (Name : String; Symbol_Type : Irep; Value : Irep)
34-
return Symbol;
35-
3633
procedure Declare_Itype (Ty : Entity_Id);
3734

3835
function Do_Address_Of (N : Node_Id) return Irep
@@ -129,7 +126,7 @@ package body Tree_Walk is
129126
Description : Irep) return Irep;
130127

131128
function Make_Range_Assert_Expr (N : Node_Id; Value : Irep;
132-
Value_Type : Irep) return Irep;
129+
Bounds_Type : Irep) return Irep;
133130

134131
function Do_Nondet_Function_Call (N : Node_Id) return Irep
135132
with Pre => Nkind (N) = N_Function_Call,
@@ -894,29 +891,8 @@ package body Tree_Walk is
894891
return Do_Bare_Range_Constraint (N, Underlying);
895892
end Do_Array_Range;
896893

897-
------------------
898-
-- Add_To_Table --
899-
------------------
900-
901-
function Add_To_Table (Name : String; Symbol_Type : Irep; Value : Irep)
902-
return Symbol is
903-
New_Symbol : Symbol;
904-
begin
905-
New_Symbol.SymType := Symbol_Type;
906-
New_Symbol.Name := Intern (Name);
907-
New_Symbol.PrettyName := New_Symbol.Name;
908-
New_Symbol.BaseName := New_Symbol.Name;
909-
New_Symbol.Mode := Intern ("C");
910-
New_Symbol.Value := Value;
911-
912-
if not (Global_Symbol_Table.Contains (Key => Intern (Name))) then
913-
Global_Symbol_Table.Insert (Intern (Name), New_Symbol);
914-
end if;
915-
return New_Symbol;
916-
end Add_To_Table;
917-
918894
function Make_Range_Assert_Expr (N : Node_Id; Value : Irep;
919-
Value_Type : Irep)
895+
Bounds_Type : Irep)
920896
return Irep
921897
is
922898
Call_Inst : constant Irep := New_Irep (I_Side_Effect_Expr_Function_Call);
@@ -930,45 +906,55 @@ package body Tree_Walk is
930906
-- Build_Assert_Function --
931907
---------------------------
932908

909+
-- Build a symbol for the following function
910+
-- Actual_Type range_check(Actual_Type value) {
911+
-- assert (value >= Bounds_Type.lower_bound
912+
-- && value <= Bounds_Type.upper_bound);
913+
-- return value;
914+
-- }
933915
function Build_Assert_Function return Symbol
934916
is
935-
Func_Type : constant Irep := New_Irep (I_Code_Type);
936-
Func_Args : constant Irep := New_Irep (I_Parameter_List);
937-
Func_Name : constant String :=
938-
Fresh_Var_Name ("range_check");
939-
Body_Block : constant Irep := New_Irep (I_Code_Block);
940-
Return_Inst : constant Irep := New_Irep (I_Code_Return);
941-
Description : constant Irep := New_Irep (I_String_Constant_Expr);
942-
Value_Param : Irep := New_Irep (I_Symbol_Expr);
917+
Func_Name : constant String := Fresh_Var_Name ("range_check");
918+
Body_Block : constant Irep := Make_Code_Block (Sloc (N));
919+
Description : constant Irep := Make_String_Constant_Expr (
920+
Source_Location => Sloc (N),
921+
I_Type => Ireps.Empty,
922+
Range_Check => False,
923+
Value => "Range Check");
924+
Func_Params : constant Irep := New_Irep (I_Parameter_List);
943925
Value_Arg : constant Irep :=
944926
Create_Fun_Parameter (Fun_Name => Func_Name,
945927
Param_Name => "value",
946928
Param_Type => Actual_Type,
947-
Param_List => Func_Args,
929+
Param_List => Func_Params,
948930
A_Symbol_Table => Global_Symbol_Table,
949931
Source_Location => Sloc (N));
932+
Func_Type : constant Irep := Make_Code_Type (
933+
-- Function parameters should only be created via
934+
-- Create_Fun_Parameter
935+
Parameters => Func_Params,
936+
Ellipsis => False,
937+
Return_Type => Actual_Type,
938+
Inlined => False,
939+
Knr => False);
940+
Value_Param : constant Irep := Param_Symbol (Value_Arg);
941+
--
942+
Return_Inst : constant Irep := Make_Code_Return (
943+
Return_Value => Value_Param,
944+
Source_Location => Sloc (N),
945+
I_Type => Ireps.Empty);
950946
begin
951-
-- Create type (value_type) -> element_type
952-
953-
Set_Parameters (Func_Type, Func_Args);
954-
Set_Return_Type (Func_Type, Actual_Type);
955-
Set_Ellipsis (Func_Type, False);
956-
957-
-- Create body (allocate and then call array_copy)
958-
Value_Param := Param_Symbol (Value_Arg);
959-
Set_Return_Value (Return_Inst, Value_Param);
960-
Set_Value (I => Description,
961-
Value => "Range Check");
962947
Append_Op (Body_Block,
963948
Make_Assert_Call (Expression (N),
964949
Make_Range_Expression
965-
(Value_Param, Value_Type),
950+
(Value_Param, Bounds_Type),
966951
Description));
967952
Append_Op (Body_Block, Return_Inst);
968953

969-
return Add_To_Table (Name => Func_Name,
970-
Symbol_Type => Func_Type,
971-
Value => Body_Block);
954+
return New_Function_Symbol_Entry (Name => Func_Name,
955+
Symbol_Type => Func_Type,
956+
Value => Body_Block,
957+
A_Symbol_Table => Global_Symbol_Table);
972958
end Build_Assert_Function;
973959

974960
begin
@@ -1011,7 +997,7 @@ package body Tree_Walk is
1011997
Value => Make_Range_Assert_Expr (
1012998
N => N,
1013999
Value => RHS,
1014-
Value_Type => Get_Type (LHS)));
1000+
Bounds_Type => Get_Type (LHS)));
10151001
-- Set_Op0 (Cast_RHS, RHS);
10161002
Set_Type (Cast_RHS, Get_Type (LHS));
10171003
Set_Rhs (I => R,
@@ -1717,21 +1703,23 @@ package body Tree_Walk is
17171703
----------------------
17181704

17191705
function Make_Assume_Expr (N : Node_Id; Assumption : Irep) return Irep is
1720-
SE_Call_Expr : constant Irep :=
1706+
Sym_Assume : constant Irep := Make_Symbol_Expr (
1707+
Source_Location => Sloc (N),
1708+
I_Type => New_Irep (I_Code_Type),
1709+
Range_Check => False,
1710+
Identifier => "__CPROVER_assume");
1711+
SEE_Fun_Call : constant Irep :=
17211712
New_Irep (I_Side_Effect_Expr_Function_Call);
1722-
Sym_Assume : constant Irep := New_Irep (I_Symbol_Expr);
17231713
Assume_Args : constant Irep := New_Irep (I_Argument_List);
17241714
begin
1725-
Set_Identifier (Sym_Assume, "__CPROVER_assume");
1726-
Set_Type (Sym_Assume, New_Irep (I_Code_Type));
17271715

17281716
Append_Argument (Assume_Args, Assumption);
17291717

1730-
Set_Source_Location (SE_Call_Expr, Sloc (N));
1731-
Set_Function (SE_Call_Expr, Sym_Assume);
1732-
Set_Arguments (SE_Call_Expr, Assume_Args);
1733-
Set_Type (SE_Call_Expr, Make_Void_Type);
1734-
return SE_Call_Expr;
1718+
Set_Source_Location (SEE_Fun_Call, Sloc (N));
1719+
Set_Function (SEE_Fun_Call, Sym_Assume);
1720+
Set_Arguments (SEE_Fun_Call, Assume_Args);
1721+
Set_Type (SEE_Fun_Call, Make_Void_Type);
1722+
return SEE_Fun_Call;
17351723
end Make_Assume_Expr;
17361724

17371725
----------------------
@@ -3809,7 +3797,7 @@ package body Tree_Walk is
38093797
Set_Op0 (I => Ret,
38103798
Value => Make_Range_Assert_Expr (N => N,
38113799
Value => To_Convert,
3812-
Value_Type => New_Type));
3800+
Bounds_Type => New_Type));
38133801
else
38143802
Set_Op0 (Ret, To_Convert);
38153803
end if;

0 commit comments

Comments
 (0)