From f9279d5390a33a2f371ae1ececee1dcc6984dcf4 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 17 May 2019 17:03:54 +0100 Subject: [PATCH 1/2] Fix UKNI range issue, and add symbols earlier to the symbol table --- gnat2goto/driver/goto_utils.adb | 17 ++++++ gnat2goto/driver/goto_utils.ads | 4 ++ gnat2goto/driver/tree_walk.adb | 54 +++++++++++++++++-- .../range_constraint.adb | 14 +++++ .../enum_symbols_range_constraint/test.out | 1 + .../enum_symbols_range_constraint/test.py | 3 ++ .../range_constraint.adb | 16 ++++++ .../test.opt | 1 + .../test.out | 1 + .../test.py | 3 ++ .../tests/range_second/range_second.adb | 20 +++++++ .../tests/range_second/range_third.adb | 14 +++++ .../gnat2goto/tests/range_second/test.opt | 2 + .../gnat2goto/tests/range_second/test.py | 3 ++ 14 files changed, 148 insertions(+), 5 deletions(-) create mode 100644 testsuite/gnat2goto/tests/enum_symbols_range_constraint/range_constraint.adb create mode 100644 testsuite/gnat2goto/tests/enum_symbols_range_constraint/test.out create mode 100644 testsuite/gnat2goto/tests/enum_symbols_range_constraint/test.py create mode 100644 testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/range_constraint.adb create mode 100644 testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.opt create mode 100644 testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.out create mode 100644 testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.py create mode 100644 testsuite/gnat2goto/tests/range_second/range_second.adb create mode 100644 testsuite/gnat2goto/tests/range_second/range_third.adb create mode 100644 testsuite/gnat2goto/tests/range_second/test.opt create mode 100644 testsuite/gnat2goto/tests/range_second/test.py diff --git a/gnat2goto/driver/goto_utils.adb b/gnat2goto/driver/goto_utils.adb index 941ee78d5..bb5230ab4 100644 --- a/gnat2goto/driver/goto_utils.adb +++ b/gnat2goto/driver/goto_utils.adb @@ -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; diff --git a/gnat2goto/driver/goto_utils.ads b/gnat2goto/driver/goto_utils.ads index 048aaecb7..ca29fe597 100644 --- a/gnat2goto/driver/goto_utils.ads +++ b/gnat2goto/driver/goto_utils.ads @@ -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; diff --git a/gnat2goto/driver/tree_walk.adb b/gnat2goto/driver/tree_walk.adb index 0f6ff8852..faebe263a 100644 --- a/gnat2goto/driver/tree_walk.adb +++ b/gnat2goto/driver/tree_walk.adb @@ -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"); @@ -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", @@ -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 + 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; @@ -792,6 +805,28 @@ package body Tree_Walk is procedure Handle_Parameter (Formal : Entity_Id; Actual : Node_Id); + function Handle_Enum_Symbol_Members (Mem : Irep) return Irep; + 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; + begin + return + (if Kind (Val) = I_Op_Typecast + then Get_Op0 (Val) else Val); + end; + else + return Mem; + end if; + end Handle_Enum_Symbol_Members; + ---------------------- -- Handle_Parameter -- ---------------------- @@ -799,16 +834,17 @@ package body Tree_Walk is 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; @@ -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); @@ -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; ------------------------- diff --git a/testsuite/gnat2goto/tests/enum_symbols_range_constraint/range_constraint.adb b/testsuite/gnat2goto/tests/enum_symbols_range_constraint/range_constraint.adb new file mode 100644 index 000000000..304aa5528 --- /dev/null +++ b/testsuite/gnat2goto/tests/enum_symbols_range_constraint/range_constraint.adb @@ -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; diff --git a/testsuite/gnat2goto/tests/enum_symbols_range_constraint/test.out b/testsuite/gnat2goto/tests/enum_symbols_range_constraint/test.out new file mode 100644 index 000000000..c0794a357 --- /dev/null +++ b/testsuite/gnat2goto/tests/enum_symbols_range_constraint/test.out @@ -0,0 +1 @@ +VERIFICATION SUCCESSFUL diff --git a/testsuite/gnat2goto/tests/enum_symbols_range_constraint/test.py b/testsuite/gnat2goto/tests/enum_symbols_range_constraint/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/enum_symbols_range_constraint/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove() diff --git a/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/range_constraint.adb b/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/range_constraint.adb new file mode 100644 index 000000000..fd8d38814 --- /dev/null +++ b/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/range_constraint.adb @@ -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; diff --git a/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.opt b/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.opt new file mode 100644 index 000000000..2c44c9bfb --- /dev/null +++ b/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.opt @@ -0,0 +1 @@ +ALL XFAIL symex is crashing at the assignment because of wrong code generation. diff --git a/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.out b/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.out new file mode 100644 index 000000000..c0794a357 --- /dev/null +++ b/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.out @@ -0,0 +1 @@ +VERIFICATION SUCCESSFUL diff --git a/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.py b/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove() diff --git a/testsuite/gnat2goto/tests/range_second/range_second.adb b/testsuite/gnat2goto/tests/range_second/range_second.adb new file mode 100644 index 000000000..eca6d93fd --- /dev/null +++ b/testsuite/gnat2goto/tests/range_second/range_second.adb @@ -0,0 +1,20 @@ +procedure Range_Second 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; + + procedure Testable (Result : Result_Indicator_Type) is + begin + null; + end Testable; + +begin + Testable (CALIBRATION_PASS); + Testable (MEASUREMENT_PRESENT); +end Range_Second; diff --git a/testsuite/gnat2goto/tests/range_second/range_third.adb b/testsuite/gnat2goto/tests/range_second/range_third.adb new file mode 100644 index 000000000..8da24a56e --- /dev/null +++ b/testsuite/gnat2goto/tests/range_second/range_third.adb @@ -0,0 +1,14 @@ +procedure Range_Second is + type An_Int is range 1..1000; + subtype Another_Int is An_Int range 5..100; + + procedure Testable (Result : An_Int) is + test_val : Another_Int := Result; + begin + null; + end Testable; + +begin + Testable (50); + Testable (200); +end Range_Second; diff --git a/testsuite/gnat2goto/tests/range_second/test.opt b/testsuite/gnat2goto/tests/range_second/test.opt new file mode 100644 index 000000000..376a501ed --- /dev/null +++ b/testsuite/gnat2goto/tests/range_second/test.opt @@ -0,0 +1,2 @@ +ALL XFAIL Doesn't crash anymore but cbmc does not perform range assertion checks + diff --git a/testsuite/gnat2goto/tests/range_second/test.py b/testsuite/gnat2goto/tests/range_second/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/range_second/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove() From 04008630785f66d1c47c93943295ab565983ea70 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 21 May 2019 11:57:13 +0100 Subject: [PATCH 2/2] Update golden results --- .../golden-results/SPARK-tetris-summary.txt | 5 ---- .../golden-results/StratoX-summary.txt | 27 +++++++---------- .../golden-results/Tokeneer-summary.txt | 10 ------- .../UKNI-Information-Barrier-summary.txt | 5 ---- experiments/golden-results/muen-summary.txt | 30 +++++++------------ experiments/golden-results/vct-summary.txt | 15 ++++++---- 6 files changed, 31 insertions(+), 61 deletions(-) diff --git a/experiments/golden-results/SPARK-tetris-summary.txt b/experiments/golden-results/SPARK-tetris-summary.txt index 834d885b3..a263f3812 100644 --- a/experiments/golden-results/SPARK-tetris-summary.txt +++ b/experiments/golden-results/SPARK-tetris-summary.txt @@ -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 diff --git a/experiments/golden-results/StratoX-summary.txt b/experiments/golden-results/StratoX-summary.txt index 23e0b1347..bfb1e1339 100644 --- a/experiments/golden-results/StratoX-summary.txt +++ b/experiments/golden-results/StratoX-summary.txt @@ -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 @@ -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 @@ -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 @@ -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 diff --git a/experiments/golden-results/Tokeneer-summary.txt b/experiments/golden-results/Tokeneer-summary.txt index 2bb0f131f..f31091125 100644 --- a/experiments/golden-results/Tokeneer-summary.txt +++ b/experiments/golden-results/Tokeneer-summary.txt @@ -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 diff --git a/experiments/golden-results/UKNI-Information-Barrier-summary.txt b/experiments/golden-results/UKNI-Information-Barrier-summary.txt index ea52c8144..6ed5d1e60 100644 --- a/experiments/golden-results/UKNI-Information-Barrier-summary.txt +++ b/experiments/golden-results/UKNI-Information-Barrier-summary.txt @@ -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 diff --git a/experiments/golden-results/muen-summary.txt b/experiments/golden-results/muen-summary.txt index df21e27ed..ff45b0ccf 100644 --- a/experiments/golden-results/muen-summary.txt +++ b/experiments/golden-results/muen-summary.txt @@ -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 @@ -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 @@ -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 @@ -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 diff --git a/experiments/golden-results/vct-summary.txt b/experiments/golden-results/vct-summary.txt index 674d4c027..f88af81d1 100644 --- a/experiments/golden-results/vct-summary.txt +++ b/experiments/golden-results/vct-summary.txt @@ -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 @@ -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 |