Skip to content

Fix UKNI range issue, and add symbols earlier to the symbol table #238

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
merged 2 commits into from
May 28, 2019
Merged

Fix UKNI range issue, and add symbols earlier to the symbol table #238

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f9279d5
Fix UKNI range issue, and add symbols earlier to the symbol table
NlightNFotis May 17, 2019
0400863
Update golden results
NlightNFotis May 21, 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
5 changes: 0 additions & 5 deletions experiments/golden-results/SPARK-tetris-summary.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,6 @@ Calling function: Process_Declaration
Error message: Package declaration
Nkind: N_Package_Declaration
--
Occurs: 10 times
Calling function: Do_Base_Range_Constraint
Error message: range expression not bitvector type
Nkind: N_Range
--
Occurs: 9 times
Calling function: Process_Pragma_Declaration
Error message: Unsupported pragma: Volatile
Expand Down
27 changes: 11 additions & 16 deletions experiments/golden-results/StratoX-summary.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ Calling function: Process_Declaration
Error message: Unknown declaration kind
Nkind: N_Freeze_Generic_Entity
--
Occurs: 157 times
Occurs: 155 times
Calling function: Do_Function_Call
Error message: func name not in symbol table
Nkind: N_Function_Call
Expand Down Expand Up @@ -74,15 +74,15 @@ Error message: Unknown declaration kind
Nkind: N_Null_Statement
--
Occurs: 13 times
Calling function: Do_Constant
Error message: Constant Type not in symbol table
Nkind: N_Integer_Literal
--
Occurs: 13 times
Calling function: Process_Declaration
Error message: Generic instantiation declaration
Nkind: N_Function_Instantiation
--
Occurs: 12 times
Calling function: Do_Constant
Error message: Constant Type not in symbol table
Nkind: N_Integer_Literal
--
Occurs: 11 times
Calling function: Do_Expression
Error message: In
Expand All @@ -104,21 +104,11 @@ Error message: Unsupported pragma: Global
Nkind: N_Pragma
--
Occurs: 9 times
Calling function: Do_Procedure_Call_Statement
Error message: sym id not in symbol table
Nkind: N_Procedure_Call_Statement
--
Occurs: 9 times
Calling function: Process_Pragma_Declaration
Error message: Unsupported pragma: Elaborate Body
Nkind: N_Pragma
--
Occurs: 8 times
Calling function: Do_Base_Range_Constraint
Error message: range expression not bitvector type
Nkind: N_Range
--
Occurs: 8 times
Calling function: Process_Declaration
Error message: Generic instantiation declaration
Nkind: N_Package_Instantiation
Expand Down Expand Up @@ -204,6 +194,11 @@ Error message: Generic declaration
Nkind: N_Generic_Package_Declaration
--
Occurs: 3 times
Calling function: Do_Procedure_Call_Statement
Error message: sym id not in symbol table
Nkind: N_Procedure_Call_Statement
--
Occurs: 3 times
Calling function: Process_Statement
Error message: Unknown expression kind
Nkind: N_Object_Declaration
Expand Down
10 changes: 0 additions & 10 deletions experiments/golden-results/Tokeneer-summary.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,16 +84,6 @@ Error message: Abstract type declaration unsupported
Nkind: N_Private_Type_Declaration
--
Occurs: 8 times
Calling function: Do_Base_Range_Constraint
Error message: range expression not bitvector type
Nkind: N_Range
--
Occurs: 8 times
Calling function: Do_Base_Range_Constraint
Error message: unsupported upper range kind
Nkind: N_Identifier
--
Occurs: 8 times
Calling function: Process_Pragma_Declaration
Error message: Unknown pragma
Nkind: N_Pragma
Expand Down
5 changes: 0 additions & 5 deletions experiments/golden-results/UKNI-Information-Barrier-summary.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,11 +18,6 @@ Calling function: Do_Itype_Definition
Error message: Unknown Ekind
Nkind: N_Defining_Identifier
--
Occurs: 2 times
Calling function: Do_Base_Range_Constraint
Error message: range expression not bitvector type
Nkind: N_Range
--
Occurs: 1 times
Calling function: Process_Declaration
Error message: Use package clause declaration
Expand Down
30 changes: 10 additions & 20 deletions experiments/golden-results/muen-summary.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,16 +54,16 @@ Error message: Unsupported pragma: Abstract state
Nkind: N_Pragma
--
Occurs: 11 times
Calling function: Do_Constant
Error message: Constant Type not in symbol table
Nkind: N_Integer_Literal
--
Occurs: 11 times
Calling function: Process_Pragma_Declaration
Error message: Unsupported pragma: Initializes
Nkind: N_Pragma
--
Occurs: 10 times
Calling function: Do_Constant
Error message: Constant Type not in symbol table
Nkind: N_Integer_Literal
--
Occurs: 10 times
Calling function: Do_Type_Definition
Error message: Unknown expression kind
Nkind: N_Access_Function_Definition
Expand All @@ -73,11 +73,6 @@ Calling function: Process_Declaration
Error message: Package declaration
Nkind: N_Package_Declaration
--
Occurs: 9 times
Calling function: Do_Function_Call
Error message: func name not in symbol table
Nkind: N_Function_Call
--
Occurs: 8 times
Calling function: Do_Itype_Integer_Subtype
Error message: Non-literal bound unsupported
Expand All @@ -99,16 +94,16 @@ Error message: Unsupported pragma: Global
Nkind: N_Pragma
--
Occurs: 7 times
Calling function: Do_Function_Call
Error message: func name not in symbol table
Nkind: N_Function_Call
--
Occurs: 7 times
Calling function: Process_Declaration
Error message: Generic instantiation declaration
Nkind: N_Function_Instantiation
--
Occurs: 6 times
Calling function: Do_Base_Range_Constraint
Error message: range expression not bitvector type
Nkind: N_Range
--
Occurs: 6 times
Calling function: Process_Pragma_Declaration
Error message: Unsupported pragma: Precondition
Nkind: N_Pragma
Expand Down Expand Up @@ -149,11 +144,6 @@ Error message: Etype not a type
Nkind: N_Identifier
--
Occurs: 2 times
Calling function: Do_Procedure_Call_Statement
Error message: sym id not in symbol table
Nkind: N_Procedure_Call_Statement
--
Occurs: 2 times
Calling function: Do_Type_Definition
Error message: Unknown expression kind
Nkind: N_Access_Procedure_Definition
Expand Down
15 changes: 10 additions & 5 deletions experiments/golden-results/vct-summary.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,6 @@ Calling function: Process_Declaration
Error message: Exception declaration
Nkind: N_Exception_Declaration
--
Occurs: 32 times
Calling function: Do_Base_Range_Constraint
Error message: unsupported upper range kind
Nkind: N_Identifier
--
Occurs: 18 times
Calling function: Do_Operator_General
Error message: Concat unsupported
Expand Down Expand Up @@ -132,3 +127,13 @@ Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:29|
| Error detected at system.ads:156:5 |
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:29|
| Error detected at system.ads:156:5 |
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:29|
| Error detected at system.ads:156:5 |
17 changes: 17 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 @@ -473,4 +473,21 @@ package body GOTO_Utils is
(Get_Type (Function_Expr)),
Source_Location => Source_Location);
end Make_Simple_Side_Effect_Expr_Function_Call;

procedure Register_Identifier_In_Symbol_Table
(N : Irep; Val : Irep; Symtab : in out Symbol_Table) is
Identifier_Name : constant Symbol_Id :=
Intern (Get_Identifier (N));
Identifier_Symbol : Symbol;
begin
Identifier_Symbol.Name := Identifier_Name;
Identifier_Symbol.BaseName := Identifier_Name;
Identifier_Symbol.PrettyName := Identifier_Name;
Identifier_Symbol.SymType := Get_Type (N);
Identifier_Symbol.IsLValue := True;
Identifier_Symbol.IsStaticLifetime := True;
Identifier_Symbol.Mode := Intern ("C");
Identifier_Symbol.Value := Val;
Symtab.Insert (Identifier_Name, Identifier_Symbol);
end Register_Identifier_In_Symbol_Table;
end GOTO_Utils;
4 changes: 4 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 @@ -138,4 +138,8 @@ package GOTO_Utils is
Function_Expr : Irep;
Source_Location : Source_Ptr) return Irep;

procedure Register_Identifier_In_Symbol_Table
(N : Irep; Val : Irep; Symtab : in out Symbol_Table)
with Pre => Kind (N) = I_Symbol_Expr;

end GOTO_Utils;
54 changes: 49 additions & 5 deletions gnat2goto/driver/tree_walk.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -743,7 +743,9 @@ package body Tree_Walk is

Result_Type : constant Irep := New_Irep (I_Bounded_Signedbv_Type);
begin
if not (Kind (Resolved_Underlying) in Class_Bitvector_Type) then
if not (Kind (Resolved_Underlying) in Class_Bitvector_Type or
Kind (Resolved_Underlying) = I_C_Enum_Type)
then
return Report_Unhandled_Node_Type (Range_Expr,
"Do_Base_Range_Constraint",
"range expression not bitvector type");
Expand All @@ -754,6 +756,9 @@ package body Tree_Walk is
Store_Nat_Bound (Bound_Type_Nat (Intval (Lower_Bound)));
when N_Attribute_Reference => Lower_Bound_Value :=
Store_Symbol_Bound (Get_Array_Attr_Bound_Symbol (Lower_Bound));
when N_Identifier =>
Lower_Bound_Value :=
Store_Symbol_Bound (Bound_Type_Symbol (Lower_Bound));
when others =>
Report_Unhandled_Node_Empty (Lower_Bound,
"Do_Base_Range_Constraint",
Expand All @@ -765,13 +770,21 @@ package body Tree_Walk is
Store_Nat_Bound (Bound_Type_Nat (Intval (Upper_Bound)));
when N_Attribute_Reference => Upper_Bound_Value :=
Store_Symbol_Bound (Get_Array_Attr_Bound_Symbol (Upper_Bound));
when N_Identifier =>
Upper_Bound_Value :=
Store_Symbol_Bound (Bound_Type_Symbol (Upper_Bound));
when others =>
Report_Unhandled_Node_Empty (Upper_Bound,
"Do_Base_Range_Constraint",
"unsupported upper range kind");
end case;

Set_Width (Result_Type, Get_Width (Resolved_Underlying));
if Kind (Resolved_Underlying) = I_C_Enum_Type then
Copy link
Contributor

Choose a reason for hiding this comment

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

This seems sketchy. enumeration_typet does not have a width field, seems like you're basically invoking UB here?

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 enumeration_typet doesn't have a width field, but it has a subtype that has a width field.

Set_Width (Result_Type,
Get_Width (Get_Subtype (Resolved_Underlying)));
else
Set_Width (Result_Type, Get_Width (Resolved_Underlying));
end if;
Set_Lower_Bound (Result_Type, Lower_Bound_Value);
Set_Upper_Bound (Result_Type, Upper_Bound_Value);
return Result_Type;
Expand All @@ -792,23 +805,46 @@ package body Tree_Walk is

procedure Handle_Parameter (Formal : Entity_Id; Actual : Node_Id);

function Handle_Enum_Symbol_Members (Mem : Irep) return Irep;
Copy link
Contributor

Choose a reason for hiding this comment

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

What's Mem?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

This refers to the Member.

function Handle_Enum_Symbol_Members (Mem : Irep) return Irep is
Followed_Type_Symbol : constant Irep :=
Follow_Symbol_Type (Get_Type (Mem), Global_Symbol_Table);
begin
if Kind (Followed_Type_Symbol) = I_C_Enum_Type then
declare
Val : constant Irep := Global_Symbol_Table
(Intern
(Get_Identifier
(Mem)))
.Value;
Copy link
Contributor

Choose a reason for hiding this comment

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

So this function returns the initial value for the symbol? What if it's modified?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I will need to get back to you on that.

Copy link
Contributor

Choose a reason for hiding this comment

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

@xbauch The symbol is a variable, but they stand in for enum members. Since enum members aren't assignable this should be fine, but I'd prefer if exactly what's going on here would be spelled out in a comment or something.

begin
return
(if Kind (Val) = I_Op_Typecast
then Get_Op0 (Val) else Val);
end;
else
return Mem;
Copy link
Contributor

Choose a reason for hiding this comment

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

So the function is identity for non-C_Enum_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.

Yes. Do you think it's better to be documented? I thought it was obvious.

Copy link
Contributor

Choose a reason for hiding this comment

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

No. I was just trying to find out if it was intentional.

Copy link
Contributor

Choose a reason for hiding this comment

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

Maybe worth spelling out if it's not obvious.

end if;
end Handle_Enum_Symbol_Members;

----------------------
-- Handle_Parameter --
----------------------

procedure Handle_Parameter (Formal : Entity_Id; Actual : Node_Id) is
Is_Out : constant Boolean := Out_Present (Parent (Formal));
Actual_Irep : Irep;

Expression : constant Irep := Do_Expression (Actual);
begin
if Is_Out and then
not (Kind (Get_Type (Do_Expression (Actual))) in Class_Type)
not (Kind (Get_Type (Expression)) in Class_Type)
then
Report_Unhandled_Node_Empty (Actual, "Handle_Parameter",
"Kind of actual not in class type");
return;
end if;
Actual_Irep := Wrap_Argument (Do_Expression (Actual), Is_Out);
Actual_Irep := Wrap_Argument (
Handle_Enum_Symbol_Members (Expression), Is_Out);
Append_Argument (Args, Actual_Irep);
end Handle_Parameter;

Expand Down Expand Up @@ -2882,6 +2918,8 @@ package body Tree_Walk is

-- 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 @@ -2907,6 +2945,12 @@ package body Tree_Walk is
Rhs => Init_Expr,
Source_Location => Sloc (N)));
end if;

if not Is_In_Symtab then
Register_Identifier_In_Symbol_Table
(Id, Init_Expr, Global_Symbol_Table);
end if;

end Do_Object_Declaration_Full;

-------------------------
Expand Down
14 changes: 14 additions & 0 deletions testsuite/gnat2goto/tests/enum_symbols_range_constraint/range_constraint.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
procedure Range_Constraint is
type Indicator_Type is (
CALIBRATION_MODE,
MEASUREMENT_MODE,
CALIBRATION_PASS,
CALIBRATION_FAIL,
MEASUREMENT_NOT_PROVEN,
MEASUREMENT_PRESENT);

-- this particular test is testing a syntactic fix for ranges constraint by enum symbols.
subtype Result_Indicator_Type is Indicator_Type range CALIBRATION_PASS .. MEASUREMENT_NOT_PROVEN;
begin
null;
end Range_Constraint;
1 change: 1 addition & 0 deletions testsuite/gnat2goto/tests/enum_symbols_range_constraint/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
VERIFICATION SUCCESSFUL
3 changes: 3 additions & 0 deletions testsuite/gnat2goto/tests/enum_symbols_range_constraint/test.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
from test_support import *

prove()
16 changes: 16 additions & 0 deletions testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/range_constraint.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
procedure Range_Constraint is
type Indicator_Type is (
CALIBRATION_MODE,
MEASUREMENT_MODE,
CALIBRATION_PASS,
CALIBRATION_FAIL,
MEASUREMENT_NOT_PROVEN,
MEASUREMENT_PRESENT);

subtype Result_Indicator_Type is Indicator_Type range CALIBRATION_PASS .. MEASUREMENT_NOT_PROVEN;

-- this test is here because subtype assignment is broken and needs to be activated againt when fixed
Value : constant Result_Indicator_Type := CALIBRATION_FAIL;
begin
pragma assert (Value = CALIBRATION_FAIL);
end Range_Constraint;
1 change: 1 addition & 0 deletions testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.opt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ALL XFAIL symex is crashing at the assignment because of wrong code generation.
1 change: 1 addition & 0 deletions testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
VERIFICATION SUCCESSFUL
3 changes: 3 additions & 0 deletions testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
from test_support import *

prove()
Loading