Wrap selected symbol in a dereference expression

And that those for which the address was specified (via clause). We chase them
using the same idea as follow_irep and replace their symbol expression with
dereference expression to the newly introduced pointer-to symbol.

Author: petr-bauch

gnat2goto/driver/driver.adb

@@ -705,10 +705,20 @@ package body Driver is
          begin
             Modified_Symbol.SymType :=
               Remove_Extra_Type_Information
-              (Follow_Irep (SymType, Follow_Symbol'Access));
+                (Follow_Irep (SymType, Follow_Symbol'Access));
+            for K in 1 .. Addressed_Variables.Last loop
+               Modified_Symbol.SymType := Wrap_Pointer
+                 (Modified_Symbol.SymType,
+                  Addressed_Variables.Table (K).all);
+            end loop;
             Modified_Symbol.Value :=
-              Remove_Extra_Type_Information
-              (Follow_Irep (Value, Follow_Symbol'Access));
+                 Remove_Extra_Type_Information
+                    (Follow_Irep (Value, Follow_Symbol'Access));
+            for K in 1 .. Addressed_Variables.Last loop
+               Modified_Symbol.Value := Wrap_Pointer
+                 (Modified_Symbol.Value,
+                  Addressed_Variables.Table (K).all);
+            end loop;
 
             New_Table.Insert
                  (Key      => Symbol_Maps.Key (Sym_Iter),

gnat2goto/ireps/ireps-wrap_pointer.adb

@@ -0,0 +1,42 @@
+-------------------------------------------------------------------------------
+--  Separate definition for following the symbol types throughout Irep_Lists(s)
+--  Implementation is adopted from ireps-to_json.adb
+--  The rationale is to create a new list only when a new irep was created
+--  by the respective Follow_Irep. First, that sounds efficient and second
+--  Ireps were disappearing when new list was created (even if it was filled
+--  with the same ireps).
+-------------------------------------------------------------------------------
+separate (Ireps)
+function Wrap_Pointer (L : Irep_List; Name : String) return Irep_List
+is
+   The_List : Irep_List_Node;
+   Ptr      : Internal_Irep_List;
+   Arr      : constant Irep_List := New_List;
+   Modified : Boolean := False;
+begin
+   if L /= 0 then
+      The_List := Irep_List_Table.Table (To_Internal_List (L));
+      Ptr      := To_Internal_List (Irep_List (The_List.A));
+      while Ptr /= 0 loop
+         declare
+            Orig_Irep : constant Irep := Irep (Irep_List_Table.Table (Ptr).A);
+            New_Irep  : constant Irep := Wrap_Pointer (Orig_Irep, Name);
+         begin
+            if Orig_Irep /= New_Irep then
+               Append (Arr, New_Irep);
+               Modified := True;
+            else
+               Append (Arr, Orig_Irep);
+            end if;
+            Ptr := Irep_List_Table.Table (Ptr).B;
+         end;
+      end loop;
+   end if;
+
+   pragma Assert (L'Size = Arr'Size);
+   if Modified then
+      return Arr;
+   else
+      return L;
+   end if;
+end Wrap_Pointer;

gnat2goto/ireps/ireps_generator.py

@@ -368,6 +368,25 @@ def follow_irep_set_all_subs(self, b, sn, subs, i, needs_null):
                 write(b, "Integer (Follow_Irep (Irep (%s), Follow_Symbol));" % tbl_field)
         return needs_null
 
+    def wrap_pointer_set_all_subs(self, b, sn, subs, i, needs_null):
+        needs_null = False
+        setter_name, is_list = subs[i]
+        layout_kind, layout_index, layout_typ =\
+            self.layout[sn][setter_name]
+        tbl_index = ada_component_name(layout_kind,
+                                       layout_index)
+        tbl_field = "N." + tbl_index
+        if is_list:
+            assert len(subs) == 1
+            write(b, "Irep_Table.Table (I).%s :=" % tbl_index)
+            with indent(b):
+                write(b, "Integer (Wrap_Pointer (Irep_List (%s), Name));" % tbl_field)
+        else:
+            write(b, "Irep_Table.Table (I).%s :=" % tbl_index)
+            with indent(b):
+                write(b, "Integer (Wrap_Pointer (Irep (%s), Name));" % tbl_field)
+        return needs_null
+
     def remove_extra_type_information_set_all_subs(self, b, sn, subs, i, needs_null):
         needs_null = False
         setter_name, is_list = subs[i]
@@ -444,6 +463,26 @@ def follow_irep_set_all_namedsubs_and_comments(self, b, sn, setter_name, needs_n
                     needs_null = False
         return needs_null
 
+    def wrap_pointer_set_all_namedsubs_and_comments(self, b, sn, setter_name, needs_null):
+        needs_null = True
+        for kind in self.named_setters[setter_name]:
+            assert kind in ("irep", "list", "trivial")
+            if sn in self.named_setters[setter_name][kind]:
+                is_comment, _, _ =\
+                    self.named_setters[setter_name][kind][sn]
+                layout_kind, layout_index, layout_typ =\
+                    self.layout[sn][setter_name]
+                tbl_index = ada_component_name(layout_kind,
+                                               layout_index)
+                tbl_field = "N." + tbl_index
+
+                if kind == "irep":
+                    write(b, "Irep_Table.Table (I).%s :=" % tbl_index)
+                    with indent(b):
+                        write(b, "Integer (Wrap_Pointer (Irep (%s), Name));" % tbl_field)
+                    needs_null = False
+        return needs_null
+
     def remove_extra_type_information_set_all_namedsubs_and_comments(self, b, sn, setter_name, needs_null):
         needs_null = True
         for kind in self.named_setters[setter_name]:
@@ -530,6 +569,28 @@ def follow_irep_single_schema_name(self, b, sn):
                     write(b, "null;")
                 write(b, "")
 
+    def wrap_pointer_single_schema_name(self, b, sn):
+        schema = self.schemata[sn]
+        with indent(b):
+            write(b, "when %s =>" % schema["ada_name"])
+            with indent(b):
+                # the ensuing case analysis may end up doing nothing for some irep kinds
+                # in Ada cases cannot be empty hence we insert null statement if necessary
+                needs_null = True
+
+                # Set all subs
+                subs = self.collect_subs(sn)
+                for i in xrange(len(subs)):
+                    needs_null = self.wrap_pointer_set_all_subs(b, sn, subs, i, needs_null)
+
+                # Set all namedSub and comments
+                for setter_name in self.named_setters:
+                    needs_null = self.wrap_pointer_set_all_namedsubs_and_comments(b, sn, setter_name, needs_null)
+
+                if needs_null:
+                    write(b, "null;")
+                write(b, "")
+
     def remove_extra_type_information_single_schema_name(self, b, sn):
         schema = self.schemata[sn]
         with indent(b):
@@ -1813,6 +1874,10 @@ def generate_code(self, optimize, schema_file_names):
         write(s, "--  Replace Symbol Types")
         write(s, "")
 
+        write(s, "function Wrap_Pointer (I : Irep; Name : String) return Irep;")
+        write(s, "--  Increase Pointer Depth")
+        write(s, "")
+
         write(s, "function Remove_Extra_Type_Information (I : Irep) return Irep;")
         write(s, "--  Remove Type Bounds")
         write(s, "")
@@ -1829,6 +1894,10 @@ def generate_code(self, optimize, schema_file_names):
         write(b, "--  Replace Symbol Types")
         write(b, "")
 
+        write(b, "function Wrap_Pointer (L : Irep_List; Name : String) return Irep_List;")
+        write(b, "--  Increase Pointer Depth")
+        write(b, "")
+
         write(b, "function Remove_Extra_Type_Information (L : Irep_List) return Irep_List;")
         write(b, "--  Remove Type Bounds")
         write(b, "")
@@ -1880,6 +1949,11 @@ def generate_code(self, optimize, schema_file_names):
         continuation(b)
         write(b, "")
 
+        write(b, "function Wrap_Pointer (L : Irep_List; Name : String) return Irep_List")
+        write(b, "is separate;")
+        continuation(b)
+        write(b, "")
+
         write(b, "function Remove_Extra_Type_Information (L : Irep_List) return Irep_List")
         write(b, "is separate;")
         continuation(b)
@@ -2036,6 +2110,47 @@ def generate_code(self, optimize, schema_file_names):
         write(b, "end Follow_Irep;")
         write(b, "")
 
+        write_comment_block(b, "Wrap_Pointer")
+        write(b, "function Wrap_Pointer (I : Irep; Name : String) return Irep")
+        write(b, "is")
+        write(b, "begin")
+        manual_indent(b)
+        write(b, "if I = 0 then")
+        with indent(b):
+            write(b, "return I;")
+        write(b, "end if;")
+        write(b, "")
+        write(b, "if Kind (I) = I_Code_Decl then")
+        with indent(b):
+            write(b, "return I;")
+        write(b, "end if;")
+        write(b, "")
+        write(b, "if Kind (I) = I_Symbol_Expr and then Get_Identifier (I) = Name")
+        write(b, "then")
+        with indent(b):
+            write(b, "return Make_Dereference_Expr (Make_Symbol_Expr (Get_Source_Location (I),")
+            with indent(b):
+                write(b, "Make_Pointer_Type (Get_Type (I), 64), False, \"Ptr_\" & Name),")
+                write(b, "Get_Source_Location (I), Get_Type (I));")
+        write(b, "end if;")
+        write(b, "")
+        write(b, "declare")
+        with indent(b):
+            write(b, "N : Irep_Node renames Irep_Table.Table (I);")
+        write(b, "begin")
+        manual_indent(b)
+        write(b, "case N.Kind is")
+
+        for sn in self.top_sorted_sn:
+            self.wrap_pointer_single_schema_name(b, sn)
+        write(b, "end case;")
+        manual_outdent(b)
+        write(b, "end;")
+        write(b, "return I;")
+        manual_outdent(b)
+        write(b, "end Wrap_Pointer;")
+        write(b, "")
+
         write_comment_block(b, "Remove_Extra_Type_Information")
         write(b, "function Remove_Extra_Type_Information (I : Irep) return Irep")
         write(b, "is")