Refactor symtab inserts #240

xbauch · 2019-05-21T09:12:24Z

We were adding into the symbol table in a number of places across tree_walk. This PR wraps every access into a helper function in goto_utils. Checks that declared objects are present in the symbol table and introduces them otherwise. In the last bit, there is an overlap with #238.

hannes-steffenhagen-diffblue · 2019-05-21T09:35:38Z

gnat2goto/driver/goto_utils.adb

@@ -120,6 +120,23 @@ package body GOTO_Utils is
      return Ret;
   end Symbol_Expr;

+   procedure New_Member_Symbol_Entry (Member_Name : String; Base_Name : String;


What's a Member symbol?

Element of a product type?

For now it is enum specific. Renamed to New_Enum_Member_Symbol_Entry.

hannes-steffenhagen-diffblue · 2019-05-21T09:35:48Z

gnat2goto/driver/goto_utils.ads

+     with Post => Kind (Symbol_Expr'Result) = I_Symbol_Expr;
+
+   procedure New_Member_Symbol_Entry (Member_Name : String; Base_Name : String;
+                                     Enum_Type : Irep; Value_Expr : Irep;


Why Enum_Type? If this is enum specific, this should be made explicit in the name I'd say.

I renamed the procedure.

hannes-steffenhagen-diffblue · 2019-05-21T09:35:57Z

gnat2goto/driver/goto_utils.ads

+   procedure New_Member_Symbol_Entry (Member_Name : String; Base_Name : String;
+                                     Enum_Type : Irep; Value_Expr : Irep;
+                                     A_Symbol_Table : in out Symbol_Table)
+     with Pre => Kind (Enum_Type) = I_Symbol_Type;


Why does this need to a be a symbol type?

hannes-steffenhagen-diffblue · 2019-05-21T09:59:32Z

gnat2goto/driver/tree_walk.adb

@@ -1221,7 +1221,7 @@ package body Tree_Walk is
              UI_Image (Enumeration_Rep (Member));
            Val_Name : constant String := Unique_Name (Member);
            Base_Name : constant String := Get_Name_String (Chars (Member));
-            Member_Symbol : Symbol;
+


Empty line?

Un-removed.

hannes-steffenhagen-diffblue · 2019-05-21T10:01:18Z

gnat2goto/driver/goto_utils.adb

@@ -120,6 +121,22 @@ package body GOTO_Utils is
      return Ret;
   end Symbol_Expr;

+   procedure New_Constant_Symbol_Entry (N : Node_Id;


If the Node_Id is just used to get a name and a source location, can we just pass those to the function instead? The function doesn't seem node specific.

Inlined into the calls. This procedure now takes Symbol_Id.

hannes-steffenhagen-diffblue · 2019-05-21T10:02:07Z

gnat2goto/driver/goto_utils.ads

+                                        A_Symbol_Table : in out Symbol_Table)
+     with Pre => Nkind (N) = N_Object_Declaration;
+     --  Adds a dummy entry to the symbol table to register that a
+     --  constant has already been processed.


What does this mean?

Petr didn't add this, this was already there, and I agree that it was weird.

I can see that, but if we're changing this already my opinion is

A) Either we figure out what this means and reword it so it's easier to understand
B) If we can't figure out what this means between the 3 of us I'd posit it's clearly not a very useful comment, so I'd rather remove it in that case.

Maybe the comment makes more sense in the call-site: we call it when declaring a constant object, that does not have initial expression -- deferred constant declaration. It's completion is somewhere down the tree but we do not want to process is again which is why store it in the symbol table without the value it will be eventually initialised with.

I moved the comment to the call-site.

I also renamed the procedure to New_Valueless_Object_Symbol_Entry.

hannes-steffenhagen-diffblue · 2019-05-21T10:03:02Z

gnat2goto/driver/goto_utils.adb

@@ -121,6 +121,19 @@ package body GOTO_Utils is
      return Ret;
   end Symbol_Expr;

+   procedure New_Type_Symbol_Entry (Type_Name : String; Type_Type : Irep;


Type_Type type type type type.

What about Type_Of_Type?

hannes-steffenhagen-diffblue · 2019-05-21T10:04:55Z

gnat2goto/driver/goto_utils.ads

@@ -40,6 +40,10 @@ package GOTO_Utils is
   function Symbol_Expr (Sym : Symbol) return Irep
     with Post => Kind (Symbol_Expr'Result) = I_Symbol_Expr;

+   procedure New_Type_Symbol_Entry (Type_Name : String; Type_Type : Irep;


The Type_Name is only used Intern'ed, so IMHO this should probably just use a Symbol_Id

Intern was inlined at call-site.

hannes-steffenhagen-diffblue · 2019-05-21T10:06:06Z

gnat2goto/driver/tree_walk.adb

-            Fn_Symbol.Value := Assertion;
-            Fn_Symbol.SymType := Fn_Type;
-            Global_Symbol_Table.Insert (Fn_Symbol.Name, Fn_Symbol);
+            Fn_Symbol :=


Can this be moved up to the declaration, and the symbol be made constant now?

Well we are changing the assertion that will comprise the value of this symbol.

hannes-steffenhagen-diffblue · 2019-05-21T11:37:49Z

gnat2goto/driver/goto_utils.adb

@@ -121,6 +121,23 @@ package body GOTO_Utils is
      return Ret;
   end Symbol_Expr;

+   procedure New_Object_Symbol_Entry (Object_Name : Symbol_Id;


What's "object" in this context? We don't usually use that terminology in CBMC. I believe that's what GNAT calls an LValue? If so, this should have IsLValue set to true.

The object from do_object_declaration. I this it takes place when we declare variables. I've added setting the lvalue flag.

NlightNFotis · 2019-05-21T15:23:28Z

gnat2goto/driver/goto_utils.adb

+      Member_Symbol : Symbol;
+   begin
+      Member_Symbol.Name := Intern (Member_Name);
+      Member_Symbol.PrettyName := Intern (Base_Name);


Why are the symbols getting interned here? In all the similar implementations of this we had the symbols where not interned.

Intern was inline at call-site.

NlightNFotis · 2019-05-21T15:24:52Z

gnat2goto/driver/goto_utils.adb

@@ -120,6 +120,23 @@ package body GOTO_Utils is
      return Ret;
   end Symbol_Expr;

+   procedure New_Member_Symbol_Entry (Member_Name : String; Base_Name : String;


Element of a product type?

NlightNFotis · 2019-05-21T15:25:39Z

gnat2goto/driver/goto_utils.ads

+                                        A_Symbol_Table : in out Symbol_Table)
+     with Pre => Nkind (N) = N_Object_Declaration;
+     --  Adds a dummy entry to the symbol table to register that a
+     --  constant has already been processed.


Petr didn't add this, this was already there, and I agree that it was weird.

hannes-steffenhagen-diffblue · 2019-05-31T14:13:31Z

gnat2goto/driver/goto_utils.adb

@@ -154,52 +154,51 @@ package body GOTO_Utils is
      A_Symbol_Table.Insert (Subprog_Name, Subprog_Symbol);
   end New_Subprogram_Symbol_Entry;

-   procedure New_Type_Symbol_Entry (Type_Name : String; Type_Type : Irep;
+   procedure New_Type_Symbol_Entry (Type_Name : Symbol_Id; Type_Of_Type : Irep;


That kind of makes it sound like we have higher kinded types? I honestly don't really have a fantastic idea of what to name this either though.

NlightNFotis

LGTM

and create a new wrapper in goto_utils.

and introduce a new wrapper in goto_utils.

and create a wrapper for it.

in make_runtime_check.

into a wrapper.

in do_subprogram_specification.

and check that everything declared is there after declaration.

hannes-steffenhagen-diffblue reviewed May 21, 2019

View reviewed changes

NlightNFotis reviewed May 21, 2019

View reviewed changes

xbauch force-pushed the refactor-symtab-inserts branch from adeb7fc to 3e48299 Compare May 22, 2019 08:01

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

View reviewed changes

NlightNFotis approved these changes Jun 3, 2019

View reviewed changes

xbauch force-pushed the refactor-symtab-inserts branch from 3e48299 to 0eec6b1 Compare June 3, 2019 15:48

petr-bauch added 7 commits June 3, 2019 19:39

Extract symbol intro from do_enumeration_definition

9b802b3

and create a new wrapper in goto_utils.

Extract constant entry from do_object_declaration

732eec8

and introduce a new wrapper in goto_utils.

Extract new type entry

ea55211

and create a wrapper for it.

Call function-symbol-entry wrapper

bede848

in make_runtime_check.

Extract subprogram symbol entry

e5dfde8

into a wrapper.

Use wrapper for new param symbol

06173f9

in do_subprogram_specification.

Introduce declared object into symbol table

30ea446

and check that everything declared is there after declaration.

xbauch force-pushed the refactor-symtab-inserts branch 2 times, most recently from 211717d to 30ea446 Compare June 3, 2019 19:09

xbauch merged commit 7aedc79 into diffblue:master Jun 3, 2019

xbauch deleted the refactor-symtab-inserts branch June 10, 2019 12:42

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Refactor symtab inserts #240

Refactor symtab inserts #240

xbauch commented May 21, 2019

hannes-steffenhagen-diffblue May 21, 2019

NlightNFotis May 21, 2019

xbauch May 21, 2019 •

edited

Loading

hannes-steffenhagen-diffblue May 21, 2019

xbauch May 21, 2019 •

edited

Loading

hannes-steffenhagen-diffblue May 21, 2019

xbauch May 21, 2019 •

edited

Loading

hannes-steffenhagen-diffblue May 21, 2019

xbauch May 22, 2019

hannes-steffenhagen-diffblue May 21, 2019

xbauch May 21, 2019 •

edited

Loading

hannes-steffenhagen-diffblue May 21, 2019

NlightNFotis May 21, 2019

hannes-steffenhagen-diffblue May 21, 2019

xbauch May 22, 2019

xbauch May 22, 2019

hannes-steffenhagen-diffblue May 21, 2019

xbauch May 21, 2019 •

edited

Loading

hannes-steffenhagen-diffblue May 21, 2019

xbauch May 22, 2019

hannes-steffenhagen-diffblue May 21, 2019

xbauch May 21, 2019

hannes-steffenhagen-diffblue May 21, 2019

xbauch May 21, 2019 •

edited

Loading

NlightNFotis May 21, 2019

xbauch May 21, 2019 •

edited

Loading

NlightNFotis May 21, 2019

NlightNFotis May 21, 2019

hannes-steffenhagen-diffblue May 31, 2019

NlightNFotis left a comment

Refactor symtab inserts #240

Refactor symtab inserts #240

Conversation

xbauch commented May 21, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

xbauch May 21, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

xbauch May 21, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

xbauch May 21, 2019 • edited Loading

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 May 21, 2019 • edited Loading

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 May 21, 2019 • edited Loading

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 May 21, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

xbauch May 21, 2019 • edited Loading

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 left a comment

Choose a reason for hiding this comment

xbauch May 21, 2019 •

edited

Loading

xbauch May 21, 2019 •

edited

Loading

xbauch May 21, 2019 •

edited

Loading

xbauch May 21, 2019 •

edited

Loading

xbauch May 21, 2019 •

edited

Loading

xbauch May 21, 2019 •

edited

Loading

xbauch May 21, 2019 •

edited

Loading