Merge pull request #220 from xbauch/feature/store-defined-symbols

Store defined symbols

Author: petr-bauch

experiments/golden-results/StratoX-summary.txt

@@ -124,11 +124,6 @@ Error message: Unsupported pragma: Suppress initialization
 Nkind: N_Pragma
 --
 Occurs: 6 times
-Calling function: Do_Constant
-Error message: Constant Type not in symbol table
-Nkind: N_Integer_Literal
---
-Occurs: 6 times
 Calling function: Process_Declaration
 Error message: Generic instantiation declaration
 Nkind: N_Procedure_Instantiation
@@ -169,6 +164,11 @@ Error message: Unsupported pragma: Unreferenced
 Nkind: N_Pragma
 --
 Occurs: 4 times
+Calling function: Do_Constant
+Error message: Constant Type not in symbol table
+Nkind: N_Integer_Literal
+--
+Occurs: 4 times
 Calling function: Process_Declaration
 Error message: Generic declaration
 Nkind: N_Generic_Package_Declaration
@@ -209,6 +209,216 @@ Error message: Unsupported pragma: Unreferenced
 Nkind: N_Pragma
 --
 Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: generic_types__saturate_mod__min
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: generic_types__saturate_mod__val
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: p4__f1__x
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: spark__arithmetic_lemmas__lemma_mult_scale__res
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: spark__constrained_array_lemmas__lemma_transitive_order__arr
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_quaternions__Oadd__left
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_quaternions__Oadd__right
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_quaternions__Omultiply__left
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_quaternions__Omultiply__right
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_quaternions__Osubtract__left
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_quaternions__conj__left
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__clear__self
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__empty__self
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__fill__self
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__full__self
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__get_all__self
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__get_back__element
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__get_back__self
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__get_front__element
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__get_front__self
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__get_nth_first__element
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__get_nth_first__self
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__get_nth_last__element
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__get_nth_last__nth
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__get_nth_last__self
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__haselements__self
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__length__self
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__overflows__self
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__p_get__self
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__p_get_all__self
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__pop_all__self
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__pop_back__element
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__pop_back__self
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__pop_front__element
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__pop_front__self
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__push_back__self
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__generic_queue__push_front__self
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: system__generic_array_operations__square_matrix_length__a
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: system__generic_c_math_interface__Oexpon__left
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: system__generic_c_math_interface__arccosh__x
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: system__generic_c_math_interface__arccot__x
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: system__generic_c_math_interface__arccoth__x
+Nkind: 
+--
+Occurs: 1 times
 Calling function: Process_Declaration
 Error message: Subprogram body stub declaration
 Nkind: N_Subprogram_Body_Stub

experiments/golden-results/muen-summary.txt

@@ -149,6 +149,36 @@ Error message: Exponentiation unhandled for non mod types at the moment
 Nkind: N_Op_Expon
 --
 Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__muchannel__readers__drain__channel
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__muchannel__readers__drain__reader
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__muchannel__writer__deactivate__channel
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__muchannel__writer__initialize__channel
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__muchannel__writer__initialize__epoch
+Nkind: 
+--
+Occurs: 1 times
+Calling function: New_Parameter_Symbol_Entry
+Error message: standard__muchannel__writer__write__channel
+Nkind: 
+--
+Occurs: 1 times
 Calling function: Process_Declaration
 Error message: Use package clause declaration
 Nkind: N_Use_Package_Clause

gnat2goto/driver/tree_walk.adb

@@ -1191,6 +1191,7 @@ package body Tree_Walk is
    function Do_Defining_Identifier (E : Entity_Id) return Irep is
       Sym          : constant Irep := New_Irep (I_Symbol_Expr);
       Result_Type  : constant Irep := Do_Type_Reference (Etype (E));
+      Sym_Id       : constant Symbol_Id := Intern (Unique_Name (E));
 
       Is_Out_Param : constant Boolean :=
         Ekind (E) in E_In_Out_Parameter | E_Out_Parameter;
@@ -1205,6 +1206,13 @@ package body Tree_Walk is
       Set_Identifier      (Sym, Unique_Name (E));
       Set_Type            (Sym, Symbol_Type);
 
+      if not Global_Symbol_Table.Contains (Sym_Id) then
+         New_Object_Symbol_Entry (Object_Name       => Sym_Id,
+                                  Object_Type       => Symbol_Type,
+                                  Object_Init_Value => Make_Nil (Sloc (E)),
+                                  A_Symbol_Table    => Global_Symbol_Table);
+      end if;
+
       if Is_Out_Param then
          return Deref : constant Irep := New_Irep (I_Dereference_Expr) do
             Set_Type   (Deref, Result_Type);
@@ -2925,6 +2933,13 @@ package body Tree_Walk is
          end if;
       end Make_Default_Initialiser;
 
+      procedure Update_Value (Key : Symbol_Id; Element : in out Symbol);
+      procedure Update_Value (Key : Symbol_Id; Element : in out Symbol) is
+      begin
+         pragma Assert (Unintern (Key) = Unintern (Obj_Id));
+         Element.Value := Init_Expr;
+      end Update_Value;
+
       --  Begin processing for Do_Object_Declaration_Full_Declaration
    begin
       Set_Source_Location (Decl, (Sloc (N)));
@@ -2946,12 +2961,17 @@ package body Tree_Walk is
          end;
       end if;
 
+      pragma Assert (Get_Identifier (Id) = Unintern (Obj_Id));
       if not Global_Symbol_Table.Contains (Obj_Id)
       then
          New_Object_Symbol_Entry (Object_Name       => Obj_Id,
                                   Object_Type       => Obj_Type,
                                   Object_Init_Value => Init_Expr,
                                   A_Symbol_Table    => Global_Symbol_Table);
+      elsif Init_Expr /= Ireps.Empty then
+         Global_Symbol_Table.Update_Element
+           (Position => Global_Symbol_Table.Find (Obj_Id),
+            Process  => Update_Value'Access);
       end if;
 
       if Init_Expr /= Ireps.Empty then
@@ -2960,12 +2980,6 @@ package body Tree_Walk is
                                               Global_Symbol_Table),
                                              Source_Location => Sloc (N)));
       end if;
-
-      if not Global_Symbol_Table.Contains (Intern (Get_Identifier (Id))) then
-         Register_Identifier_In_Symbol_Table
-            (Id, Init_Expr, Global_Symbol_Table);
-      end if;
-
    end Do_Object_Declaration_Full;
 
    -------------------------