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

NlightNFotis · 2019-05-17T16:06:05Z

Fix the range exception problem for UKNI, and also fix another bug where symbols where not being added to the symbol table at the appropriate stage.

This contains two tests that are not fully functional right now due to the problem described in #226

xbauch · 2019-05-17T20:02:34Z

gnat2goto/driver/tree_walk.adb

+               return Val;
+            end;
+         else
+            return Mem;


So the function is identity for non-C_Enum_Type?

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

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

Maybe worth spelling out if it's not obvious.

xbauch · 2019-05-17T20:06:10Z

gnat2goto/driver/tree_walk.adb

+                 (Intern
+                    (Get_Identifier
+                     (Mem)))
+                 .Value;


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

I will need to get back to you on that.

@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.

NlightNFotis · 2019-05-20T09:28:27Z

@xbauch I updated the golden results, but something in them doesn't look right. Can you also take a look if there's something out of place?

hannes-steffenhagen-diffblue · 2019-05-20T14:54:46Z

gnat2goto/driver/tree_walk.adb

@@ -792,23 +805,44 @@ package body Tree_Walk is

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

+      function Handle_Enum_Symbol_Members (Mem : Irep) return Irep;


What's Mem?

This refers to the Member.

hannes-steffenhagen-diffblue · 2019-05-20T14:56:53Z

gnat2goto/driver/tree_walk.adb

+                 (Intern
+                    (Get_Identifier
+                     (Mem)))
+                 .Value;


@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.

hannes-steffenhagen-diffblue · 2019-05-20T14:57:17Z

gnat2goto/driver/tree_walk.adb

+               return Val;
+            end;
+         else
+            return Mem;


Maybe worth spelling out if it's not obvious.

hannes-steffenhagen-diffblue · 2019-05-20T14:58:24Z

gnat2goto/driver/tree_walk.adb

@@ -2882,6 +2916,24 @@ package body Tree_Walk is

      --  Begin processing for Do_Object_Declaration_Full_Declaration

+      procedure Register_Identifier_In_Symbol_Table (N : Irep; Val : Irep)


This seems very similar to other functions we already have. Can you check if something like this doesn't already exist in goto_utils or the like?

There's nothing there now, but I remember a PR by Petr that was adding like a couple more similar functions. They should be refactored in the future into one, but not as part of this PR.

This should probably go into the symbol table. I'm not sure about the arguments either; Rather than having an Irep and requiring ito to be a Symbol_Expr, why not pass in the name and type (which are ultimately what you need) as parameters?

Should also be called something like Declare_Global_Variable?

Also this should probably go into goto_utils

Again, because a number of similar functions were introduced recently for very similar reasons, just in different paths, I suggest that this be done as a more organised attempt to refactor these functions and this one, and make sure that the refactored version gets appropriately invoked in the correct places. But I don't think it's within the scope of this PR for this to happen.

hannes-steffenhagen-diffblue · 2019-05-20T14:59:05Z

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 


Can you add a test that doesn't fail? I believe this should still be doing a range check for things like explicit casts. Also I think @xbauch changed the test script so multiple .adb files in the same directory are linked together instead of running separately?

I don't think there's any relevant test for this. The range of this PR was for a very particular piece of code (using enum symbols as range constraints) to not crash. This has been fixed, but gnat2goto suffers from a different problem now (it doesn't handle constraints of subtypes correctly). I can't easily think of something that can exercise the fix without falling on its face because of the subtype issue.

xbauch

Looks good.

hannes-steffenhagen-diffblue · 2019-05-23T16:06:08Z

gnat2goto/driver/tree_walk.adb

         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


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

The enumeration_typet doesn't have a width field, but it has a subtype that has a width field.

hannes-steffenhagen-diffblue · 2019-05-23T16:11:37Z

gnat2goto/driver/tree_walk.adb

+         Identifier_Symbol.SymType    := Get_Type (N);
+         Identifier_Symbol.Mode       := Intern ("C");
+         Identifier_Symbol.Value      := Val;
+         Global_Symbol_Table.Insert (Identifier_Name, Identifier_Symbol);


Should have IsLValue => True and IsStaticLifetime => True

hannes-steffenhagen-diffblue · 2019-05-23T16:11:44Z

gnat2goto/driver/tree_walk.adb

@@ -2882,6 +2916,24 @@ package body Tree_Walk is

      --  Begin processing for Do_Object_Declaration_Full_Declaration

+      procedure Register_Identifier_In_Symbol_Table (N : Irep; Val : Irep)


This should probably go into the symbol table. I'm not sure about the arguments either; Rather than having an Irep and requiring ito to be a Symbol_Expr, why not pass in the name and type (which are ultimately what you need) as parameters?

Should also be called something like Declare_Global_Variable?

Also this should probably go into goto_utils

hannes-steffenhagen-diffblue · 2019-05-23T16:15:26Z

gnat2goto/driver/tree_walk.adb

@@ -2907,6 +2961,11 @@ 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);


I'm not sure I quite understand what what this here does?

What this does is that there was a problem where symbols where not added to the symbol table with the values they should have at one path that handled object declarations in the past, and these caused symbol table lookups to fail. This was fixing this.

xbauch reviewed May 17, 2019

View reviewed changes

NlightNFotis force-pushed the Range_Exception branch 2 times, most recently from 305c4de to 6cda576 Compare May 20, 2019 11:32

hannes-steffenhagen-diffblue reviewed May 20, 2019

View reviewed changes

xbauch approved these changes May 21, 2019

View reviewed changes

xbauch mentioned this pull request May 21, 2019

Refactor symtab inserts #240

Merged

NlightNFotis force-pushed the Range_Exception branch 2 times, most recently from d80b716 to 2a6c6fc Compare May 23, 2019 14:48

hannes-steffenhagen-diffblue reviewed May 23, 2019

View reviewed changes

NlightNFotis force-pushed the Range_Exception branch from a678bb8 to a52479f Compare May 24, 2019 09:33

NlightNFotis added 2 commits May 28, 2019 10:26

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

f9279d5

Update golden results

0400863

NlightNFotis force-pushed the Range_Exception branch from a52479f to 0400863 Compare May 28, 2019 09:26

hannes-steffenhagen-diffblue approved these changes May 28, 2019

View reviewed changes

NlightNFotis merged commit 848a85b into diffblue:master May 28, 2019

NlightNFotis deleted the Range_Exception branch May 28, 2019 09:51

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

NlightNFotis commented May 17, 2019

xbauch May 17, 2019

NlightNFotis May 20, 2019

xbauch May 20, 2019

hannes-steffenhagen-diffblue May 20, 2019

xbauch May 17, 2019

NlightNFotis May 20, 2019

hannes-steffenhagen-diffblue May 20, 2019

NlightNFotis commented May 20, 2019

hannes-steffenhagen-diffblue May 20, 2019

NlightNFotis May 21, 2019

hannes-steffenhagen-diffblue May 20, 2019

hannes-steffenhagen-diffblue May 20, 2019

hannes-steffenhagen-diffblue May 20, 2019

NlightNFotis May 23, 2019

hannes-steffenhagen-diffblue May 23, 2019

NlightNFotis May 24, 2019

hannes-steffenhagen-diffblue May 20, 2019

NlightNFotis May 23, 2019

xbauch left a comment

hannes-steffenhagen-diffblue May 23, 2019

NlightNFotis May 24, 2019

hannes-steffenhagen-diffblue May 23, 2019

hannes-steffenhagen-diffblue May 23, 2019

hannes-steffenhagen-diffblue May 23, 2019

NlightNFotis May 23, 2019

		@@ -792,23 +805,44 @@ package body Tree_Walk is

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

		function Handle_Enum_Symbol_Members (Mem : Irep) return Irep;

		@@ -2882,6 +2916,24 @@ package body Tree_Walk is

		-- Begin processing for Do_Object_Declaration_Full_Declaration

		procedure Register_Identifier_In_Symbol_Table (N : Irep; Val : Irep)

		@@ -0,0 +1,2 @@
		ALL XFAIL Doesn't crash anymore but cbmc does not perform range assertion checks

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

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

Conversation

NlightNFotis commented May 17, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NlightNFotis commented May 20, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

xbauch left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment