From 7cb8f2f59db7805fd14a9d84c81b36e2c64a7fe5 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 22 Mar 2019 11:04:14 +0000 Subject: [PATCH 1/5] Implement support for case statements in Ada. --- gnat2goto/driver/tree_walk.adb | 57 +++++++++++++++++++++++++++++++++- 1 file changed, 56 insertions(+), 1 deletion(-) diff --git a/gnat2goto/driver/tree_walk.adb b/gnat2goto/driver/tree_walk.adb index 55d631d12..a71361d89 100644 --- a/gnat2goto/driver/tree_walk.adb +++ b/gnat2goto/driver/tree_walk.adb @@ -146,6 +146,10 @@ package body Tree_Walk is with Pre => Nkind (N) = N_Loop_Statement, Post => Kind (Do_Loop_Statement'Result) in Class_Code; + function Do_Case_Statement (N : Node_Id) return Irep + with Pre => Nkind (N) = N_Case_Statement, + Post => Kind (Do_Case_Statement'Result) = I_Code_Block; + function Do_N_Block_Statement (N : Node_Id) return Irep with Pre => Nkind (N) = N_Block_Statement, Post => Kind (Do_N_Block_Statement'Result) = I_Code_Block; @@ -1764,6 +1768,57 @@ package body Tree_Walk is Do_Type_Declaration (New_Type, Typedef); end Do_Itype_Reference; + ----------------------- + -- Do_Case_Statement -- + ----------------------- + + function Do_Case_Statement (N : Node_Id) return Irep is + Ret : constant Irep := New_Irep (I_Code_Block); + Value : constant Irep := Do_Expression (Expression (N)); + + -- Auxiliary function to create a single test case + -- to emplace in a condition from a list of alternative + -- values. + function Make_Single_Test (Alt : Node_Id) return Irep; + function Make_Single_Test (Alt : Node_Id) return Irep is + Ret : constant Irep := New_Irep (I_Op_Eq); + Rhs : constant Irep := Do_Expression (Alt); + begin + Set_Lhs (Ret, Value); + Set_Rhs (Ret, Rhs); + Set_Type (Ret, New_Irep (I_Bool_Type)); + return Ret; + end Make_Single_Test; + + This_Alt : Node_Id := First (Alternatives (N)); + begin + -- Do-while loop because there must be at least one alternative. + loop + declare + This_Stmt : constant Irep := + Process_Statements (Statements (This_Alt)); + This_Alt_Copy : constant Node_Id := This_Alt; + This_Test : Irep; + begin + Next (This_Alt); + if not Present (This_Alt) then + -- Omit test, this is either `others` + -- or the last case of complete coverage + This_Test := This_Stmt; + else + This_Test := New_Irep (I_Code_Ifthenelse); + Set_Cond (This_Test, + Make_Single_Test + (First (Discrete_Choices (This_Alt_Copy)))); + Set_Then_Case (This_Test, This_Stmt); + Append_Op (Ret, This_Test); + end if; + end; + exit when not Present (This_Alt); + end loop; + return Ret; + end Do_Case_Statement; + ----------------------- -- Do_Loop_Statement -- ----------------------- @@ -4031,7 +4086,7 @@ package body Tree_Walk is Append_Op (Block, Do_If_Statement (N)); when N_Case_Statement => - Warn_Unhandled_Construct (Statement, "case"); + Append_Op (Block, Do_Case_Statement (N)); when N_Loop_Statement => Append_Op (Block, Do_Loop_Statement (N)); From 8bcddceb261bd08c32e0e47db55d6717cabb632d Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Mon, 25 Mar 2019 10:23:40 +0000 Subject: [PATCH 2/5] Add a small fix to support others, and add tests. --- gnat2goto/driver/tree_walk.adb | 1 + .../gnat2goto/tests/case_statement/case_statement.adb | 11 +++++++++++ testsuite/gnat2goto/tests/case_statement/test.out | 1 + testsuite/gnat2goto/tests/case_statement/test.py | 3 +++ .../case_statement_others_only.adb | 8 ++++++++ .../tests/case_statement_others_only/test.out | 1 + .../tests/case_statement_others_only/test.py | 3 +++ 7 files changed, 28 insertions(+) create mode 100644 testsuite/gnat2goto/tests/case_statement/case_statement.adb create mode 100644 testsuite/gnat2goto/tests/case_statement/test.out create mode 100644 testsuite/gnat2goto/tests/case_statement/test.py create mode 100644 testsuite/gnat2goto/tests/case_statement_others_only/case_statement_others_only.adb create mode 100644 testsuite/gnat2goto/tests/case_statement_others_only/test.out create mode 100644 testsuite/gnat2goto/tests/case_statement_others_only/test.py diff --git a/gnat2goto/driver/tree_walk.adb b/gnat2goto/driver/tree_walk.adb index a71361d89..7c6293c78 100644 --- a/gnat2goto/driver/tree_walk.adb +++ b/gnat2goto/driver/tree_walk.adb @@ -1805,6 +1805,7 @@ package body Tree_Walk is -- Omit test, this is either `others` -- or the last case of complete coverage This_Test := This_Stmt; + Append_Op (Ret, This_Test); else This_Test := New_Irep (I_Code_Ifthenelse); Set_Cond (This_Test, diff --git a/testsuite/gnat2goto/tests/case_statement/case_statement.adb b/testsuite/gnat2goto/tests/case_statement/case_statement.adb new file mode 100644 index 000000000..7e797c46b --- /dev/null +++ b/testsuite/gnat2goto/tests/case_statement/case_statement.adb @@ -0,0 +1,11 @@ +function Case_Statement return String is + type Sensor_Type is (Elevation, Azimuth, Distance); + Sensor : Sensor_Type := Elevation; +begin + case Sensor is + when Elevation => return "Elevation sensor"; + when Azimuth => return "Azimuth sensor"; + when Distance => return "Distance sensor"; + when others => return ""; + end case; +end Case_Statement; diff --git a/testsuite/gnat2goto/tests/case_statement/test.out b/testsuite/gnat2goto/tests/case_statement/test.out new file mode 100644 index 000000000..c0794a357 --- /dev/null +++ b/testsuite/gnat2goto/tests/case_statement/test.out @@ -0,0 +1 @@ +VERIFICATION SUCCESSFUL diff --git a/testsuite/gnat2goto/tests/case_statement/test.py b/testsuite/gnat2goto/tests/case_statement/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/case_statement/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove() diff --git a/testsuite/gnat2goto/tests/case_statement_others_only/case_statement_others_only.adb b/testsuite/gnat2goto/tests/case_statement_others_only/case_statement_others_only.adb new file mode 100644 index 000000000..a91641f72 --- /dev/null +++ b/testsuite/gnat2goto/tests/case_statement_others_only/case_statement_others_only.adb @@ -0,0 +1,8 @@ +function Case_Statement_Others_Only return String is + type Sensor_Type is (Elevation, Azimuth, Distance); + Sensor : Sensor_Type := Elevation; +begin + case Sensor is + when others => return ""; + end case; +end Case_Statement_Others_Only; diff --git a/testsuite/gnat2goto/tests/case_statement_others_only/test.out b/testsuite/gnat2goto/tests/case_statement_others_only/test.out new file mode 100644 index 000000000..c0794a357 --- /dev/null +++ b/testsuite/gnat2goto/tests/case_statement_others_only/test.out @@ -0,0 +1 @@ +VERIFICATION SUCCESSFUL diff --git a/testsuite/gnat2goto/tests/case_statement_others_only/test.py b/testsuite/gnat2goto/tests/case_statement_others_only/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/case_statement_others_only/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove() From 848a008929d628ebe1918b72f258d672fdfa547a Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 26 Mar 2019 09:59:01 +0000 Subject: [PATCH 3/5] Handle multiple values in case statement and add tests --- gnat2goto/driver/tree_walk.adb | 43 ++++++++++++++----- .../case_statement_vals.adb | 9 ++++ .../tests/case_statement_vals/test.out | 1 + .../tests/case_statement_vals/test.py | 3 ++ 4 files changed, 45 insertions(+), 11 deletions(-) create mode 100644 testsuite/gnat2goto/tests/case_statement_vals/case_statement_vals.adb create mode 100644 testsuite/gnat2goto/tests/case_statement_vals/test.out create mode 100644 testsuite/gnat2goto/tests/case_statement_vals/test.py diff --git a/gnat2goto/driver/tree_walk.adb b/gnat2goto/driver/tree_walk.adb index 7c6293c78..5eccc73bb 100644 --- a/gnat2goto/driver/tree_walk.adb +++ b/gnat2goto/driver/tree_walk.adb @@ -1779,16 +1779,37 @@ package body Tree_Walk is -- Auxiliary function to create a single test case -- to emplace in a condition from a list of alternative -- values. - function Make_Single_Test (Alt : Node_Id) return Irep; - function Make_Single_Test (Alt : Node_Id) return Irep is - Ret : constant Irep := New_Irep (I_Op_Eq); - Rhs : constant Irep := Do_Expression (Alt); + function Make_Case_Test (Alts : List_Id) return Irep; + function Make_Case_Test (Alts : List_Id) return Irep is + function Make_Single_Test (Alt : Node_Id) return Irep; + function Make_Single_Test (Alt : Node_Id) return Irep is + Ret : constant Irep := New_Irep (I_Op_Eq); + Rhs : constant Irep := Do_Expression (Alt); + begin + Set_Lhs (Ret, Value); + Set_Rhs (Ret, Rhs); + Set_Type (Ret, New_Irep (I_Bool_Type)); + return Ret; + end Make_Single_Test; + First_Alt_Test : constant Irep := Make_Single_Test (First (Alts)); + This_Alt : Node_Id := First (Alts); begin - Set_Lhs (Ret, Value); - Set_Rhs (Ret, Rhs); - Set_Type (Ret, New_Irep (I_Bool_Type)); - return Ret; - end Make_Single_Test; + Next (This_Alt); + if not Present (This_Alt) then + return First_Alt_Test; + end if; + declare + Big_Or : constant Irep := New_Irep (I_Op_Or); + begin + Append_Op (Big_Or, First_Alt_Test); + Set_Type (Big_Or, New_Irep (I_Bool_Type)); + while Present (This_Alt) loop + Append_Op (Big_Or, Make_Single_Test (This_Alt)); + Next (This_Alt); + end loop; + return Big_Or; + end; + end Make_Case_Test; This_Alt : Node_Id := First (Alternatives (N)); begin @@ -1809,8 +1830,8 @@ package body Tree_Walk is else This_Test := New_Irep (I_Code_Ifthenelse); Set_Cond (This_Test, - Make_Single_Test - (First (Discrete_Choices (This_Alt_Copy)))); + Make_Case_Test + (Discrete_Choices (This_Alt_Copy))); Set_Then_Case (This_Test, This_Stmt); Append_Op (Ret, This_Test); end if; diff --git a/testsuite/gnat2goto/tests/case_statement_vals/case_statement_vals.adb b/testsuite/gnat2goto/tests/case_statement_vals/case_statement_vals.adb new file mode 100644 index 000000000..64591721a --- /dev/null +++ b/testsuite/gnat2goto/tests/case_statement_vals/case_statement_vals.adb @@ -0,0 +1,9 @@ +function Case_Statement_Vals return String is + I : Integer := 3; +begin + case I is + when 0 | 1 | 2 => return "Valid ternary"; + when 3 => return "Invalid ternary"; + when others => return ""; + end case; +end Case_Statement_Vals; diff --git a/testsuite/gnat2goto/tests/case_statement_vals/test.out b/testsuite/gnat2goto/tests/case_statement_vals/test.out new file mode 100644 index 000000000..c0794a357 --- /dev/null +++ b/testsuite/gnat2goto/tests/case_statement_vals/test.out @@ -0,0 +1 @@ +VERIFICATION SUCCESSFUL diff --git a/testsuite/gnat2goto/tests/case_statement_vals/test.py b/testsuite/gnat2goto/tests/case_statement_vals/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/case_statement_vals/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove() From 1e639b3a80fc5e019b4664c65f89ee291588ffbf Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 26 Mar 2019 10:47:00 +0000 Subject: [PATCH 4/5] Add failing test for case statement and ranges --- .../case_statement_range/case_statement_range.adb | 10 ++++++++++ .../gnat2goto/tests/case_statement_range/test.opt | 1 + .../gnat2goto/tests/case_statement_range/test.out | 1 + testsuite/gnat2goto/tests/case_statement_range/test.py | 3 +++ 4 files changed, 15 insertions(+) create mode 100644 testsuite/gnat2goto/tests/case_statement_range/case_statement_range.adb create mode 100644 testsuite/gnat2goto/tests/case_statement_range/test.opt create mode 100644 testsuite/gnat2goto/tests/case_statement_range/test.out create mode 100644 testsuite/gnat2goto/tests/case_statement_range/test.py diff --git a/testsuite/gnat2goto/tests/case_statement_range/case_statement_range.adb b/testsuite/gnat2goto/tests/case_statement_range/case_statement_range.adb new file mode 100644 index 000000000..3aa95a72e --- /dev/null +++ b/testsuite/gnat2goto/tests/case_statement_range/case_statement_range.adb @@ -0,0 +1,10 @@ +function Case_Statement_Range return String is + type T is range 0 .. 10; + X : T := 6; +begin + case X is + when 0 .. 5 => return "Zero to five"; + when 6 .. 10 => return "Six to ten"; + when others => return "Invalid"; + end case; +end Case_Statement_Range; diff --git a/testsuite/gnat2goto/tests/case_statement_range/test.opt b/testsuite/gnat2goto/tests/case_statement_range/test.opt new file mode 100644 index 000000000..7fbffec2f --- /dev/null +++ b/testsuite/gnat2goto/tests/case_statement_range/test.opt @@ -0,0 +1 @@ +ALL XFAIL gnat2goto can't handle ranges in case statements diff --git a/testsuite/gnat2goto/tests/case_statement_range/test.out b/testsuite/gnat2goto/tests/case_statement_range/test.out new file mode 100644 index 000000000..c0794a357 --- /dev/null +++ b/testsuite/gnat2goto/tests/case_statement_range/test.out @@ -0,0 +1 @@ +VERIFICATION SUCCESSFUL diff --git a/testsuite/gnat2goto/tests/case_statement_range/test.py b/testsuite/gnat2goto/tests/case_statement_range/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/case_statement_range/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove() From 4e64f08e0cf76122c6a843b5128aecc1ca762af5 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 27 Mar 2019 14:52:07 +0000 Subject: [PATCH 5/5] Implement comment suggestions and change tests to return ints --- gnat2goto/driver/tree_walk.adb | 3 ++- .../tests/case_statement/case_statement.adb | 25 ++++++++++++------- .../gnat2goto/tests/case_statement/test.out | 2 ++ .../case_statement_others_only.adb | 18 ++++++++----- .../tests/case_statement_others_only/test.out | 1 + .../case_statement_vals.adb | 22 ++++++++++------ .../tests/case_statement_vals/test.out | 3 +++ 7 files changed, 51 insertions(+), 23 deletions(-) diff --git a/gnat2goto/driver/tree_walk.adb b/gnat2goto/driver/tree_walk.adb index 5eccc73bb..dc9ffd7ab 100644 --- a/gnat2goto/driver/tree_walk.adb +++ b/gnat2goto/driver/tree_walk.adb @@ -1788,7 +1788,7 @@ package body Tree_Walk is begin Set_Lhs (Ret, Value); Set_Rhs (Ret, Rhs); - Set_Type (Ret, New_Irep (I_Bool_Type)); + Set_Type (Ret, Make_Bool_Type); return Ret; end Make_Single_Test; First_Alt_Test : constant Irep := Make_Single_Test (First (Alts)); @@ -1813,6 +1813,7 @@ package body Tree_Walk is This_Alt : Node_Id := First (Alternatives (N)); begin + pragma Assert (List_Length (Alternatives (N)) >= 1); -- Do-while loop because there must be at least one alternative. loop declare diff --git a/testsuite/gnat2goto/tests/case_statement/case_statement.adb b/testsuite/gnat2goto/tests/case_statement/case_statement.adb index 7e797c46b..46e8c0fa6 100644 --- a/testsuite/gnat2goto/tests/case_statement/case_statement.adb +++ b/testsuite/gnat2goto/tests/case_statement/case_statement.adb @@ -1,11 +1,18 @@ -function Case_Statement return String is - type Sensor_Type is (Elevation, Azimuth, Distance); - Sensor : Sensor_Type := Elevation; +procedure Case_Statement is + function Case_Statement_Return return Integer is + type Sensor_Type is (Elevation, Azimuth, Distance); + Sensor : Sensor_Type := Elevation; + begin + case Sensor is + when Elevation => return 1; + when Azimuth => return 2; + when Distance => return 3; + when others => return 4; + end case; + end Case_Statement_Return; + + Result : Integer := Case_Statement_Return; begin - case Sensor is - when Elevation => return "Elevation sensor"; - when Azimuth => return "Azimuth sensor"; - when Distance => return "Distance sensor"; - when others => return ""; - end case; + pragma Assert (Result = 1); + pragma Assert (Result /= 4); end Case_Statement; diff --git a/testsuite/gnat2goto/tests/case_statement/test.out b/testsuite/gnat2goto/tests/case_statement/test.out index c0794a357..db3e9010f 100644 --- a/testsuite/gnat2goto/tests/case_statement/test.out +++ b/testsuite/gnat2goto/tests/case_statement/test.out @@ -1 +1,3 @@ +[1] file case_statement.adb line 16 assertion: SUCCESS +[2] file case_statement.adb line 17 assertion: SUCCESS VERIFICATION SUCCESSFUL diff --git a/testsuite/gnat2goto/tests/case_statement_others_only/case_statement_others_only.adb b/testsuite/gnat2goto/tests/case_statement_others_only/case_statement_others_only.adb index a91641f72..9ee676f87 100644 --- a/testsuite/gnat2goto/tests/case_statement_others_only/case_statement_others_only.adb +++ b/testsuite/gnat2goto/tests/case_statement_others_only/case_statement_others_only.adb @@ -1,8 +1,14 @@ -function Case_Statement_Others_Only return String is - type Sensor_Type is (Elevation, Azimuth, Distance); - Sensor : Sensor_Type := Elevation; +procedure Case_Statement_Others_Only is + function Case_Statement_Return return Integer is + type Sensor_Type is (Elevation, Azimuth, Distance); + Sensor : Sensor_Type := Elevation; + begin + case Sensor is + when others => return 1; + end case; + end Case_Statement_Return; + + Result : Integer := Case_Statement_Return; begin - case Sensor is - when others => return ""; - end case; + pragma Assert (Result = 1); end Case_Statement_Others_Only; diff --git a/testsuite/gnat2goto/tests/case_statement_others_only/test.out b/testsuite/gnat2goto/tests/case_statement_others_only/test.out index c0794a357..bf6e7ad67 100644 --- a/testsuite/gnat2goto/tests/case_statement_others_only/test.out +++ b/testsuite/gnat2goto/tests/case_statement_others_only/test.out @@ -1 +1,2 @@ +[1] file case_statement_others_only.adb line 13 assertion: SUCCESS VERIFICATION SUCCESSFUL diff --git a/testsuite/gnat2goto/tests/case_statement_vals/case_statement_vals.adb b/testsuite/gnat2goto/tests/case_statement_vals/case_statement_vals.adb index 64591721a..898229f04 100644 --- a/testsuite/gnat2goto/tests/case_statement_vals/case_statement_vals.adb +++ b/testsuite/gnat2goto/tests/case_statement_vals/case_statement_vals.adb @@ -1,9 +1,17 @@ -function Case_Statement_Vals return String is - I : Integer := 3; +procedure Case_Statement_Vals is + function Case_Statement_Return return Integer is + I : Integer := 3; + begin + case I is + when 0 | 1 | 2 => return 0; + when 3 => return 1; + when others => return 2; + end case; + end Case_Statement_Return; + + Result : Integer := Case_Statement_Return; begin - case I is - when 0 | 1 | 2 => return "Valid ternary"; - when 3 => return "Invalid ternary"; - when others => return ""; - end case; + pragma Assert (Result /= 0); + pragma Assert (Result = 1); + pragma Assert (Result /= 2); end Case_Statement_Vals; diff --git a/testsuite/gnat2goto/tests/case_statement_vals/test.out b/testsuite/gnat2goto/tests/case_statement_vals/test.out index c0794a357..13f950fef 100644 --- a/testsuite/gnat2goto/tests/case_statement_vals/test.out +++ b/testsuite/gnat2goto/tests/case_statement_vals/test.out @@ -1 +1,4 @@ +[1] file case_statement_vals.adb line 14 assertion: SUCCESS +[2] file case_statement_vals.adb line 15 assertion: SUCCESS +[3] file case_statement_vals.adb line 16 assertion: SUCCESS VERIFICATION SUCCESSFUL