Testing commit

Author: petr-bauch

gnat2goto/driver/driver.adb

@@ -200,7 +200,7 @@ package body Driver is
            (I_Type => Dead_Object_Type,
             Identifier => "__CPROVER_dead_object",
             Source_Location => No_Location);
-         Dead_Object_Val : constant Irep := Integer_Constant_To_Expr
+         Dead_Object_Val : constant Irep := Integer_Constant_To_BV_Expr
            (Value => Uint_0,
             Expr_Type => Dead_Object_Type,
             Source_Location => No_Location);
@@ -223,7 +223,7 @@ package body Driver is
            (I_Type => Deallocated_Type,
             Identifier => "__CPROVER_deallocated",
             Source_Location => No_Location);
-         Deallocated_Val : constant Irep := Integer_Constant_To_Expr
+         Deallocated_Val : constant Irep := Integer_Constant_To_BV_Expr
            (Value => Uint_0,
             Expr_Type => Deallocated_Type,
             Source_Location => No_Location);
@@ -246,7 +246,7 @@ package body Driver is
            (I_Type => Malloc_Object_Type,
             Identifier => "__CPROVER_malloc_object",
             Source_Location => No_Location);
-         Malloc_Object_Val : constant Irep := Integer_Constant_To_Expr
+         Malloc_Object_Val : constant Irep := Integer_Constant_To_BV_Expr
            (Value => Uint_0,
             Expr_Type => Malloc_Object_Type,
             Source_Location => No_Location);
@@ -260,6 +260,29 @@ package body Driver is
                Source_Location => No_Location));
       end Initialize_CProver_Malloc_Object;
 
+      procedure Initialize_CProver_Memory;
+      procedure Initialize_CProver_Memory is
+         Memory_Type : constant Irep := Make_Pointer_Type
+           (I_Subtype => Make_Void_Type,
+            Width => Pointer_Type_Width);
+         Memory_Sym : constant Irep := Make_Symbol_Expr
+           (I_Type => Memory_Type,
+            Identifier => "__CPROVER_memory",
+            Source_Location => No_Location);
+         Memory_Val : constant Irep := Integer_Constant_To_BV_Expr
+           (Value => Uint_0,
+            Expr_Type => Memory_Type,
+            Source_Location => No_Location);
+      begin
+         Declare_Missing_Global (Memory_Sym);
+         Append_Op
+           (Start_Body,
+            Make_Code_Assign
+             (Lhs => Memory_Sym,
+              Rhs => Memory_Val,
+              Source_Location => No_Location));
+      end Initialize_CProver_Memory;
+
       procedure Initialize_Enum_Values;
       procedure Initialize_Enum_Values is
 
@@ -348,6 +371,7 @@ package body Driver is
       Initialize_CProver_Dead_Object;
       Initialize_CProver_Deallocated;
       Initialize_CProver_Malloc_Object;
+      Initialize_CProver_Memory;
       Initialize_Enum_Values;
       Initialize_Boolean_Values;
    end Initialize_CProver_Internal_Variables;
@@ -705,10 +729,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/driver/goto_utils.adb

@@ -354,14 +354,9 @@ package body GOTO_Utils is
    function Build_Index_Constant (Value : Int; Source_Loc : Source_Ptr)
                                   return Irep
    is
-      Value_Hex : constant String :=
-        Convert_Uint_To_Hex (Value     => UI_From_Int (Value),
-                             Bit_Width => Size_T_Width);
-   begin
-      return Make_Constant_Expr (Source_Location => Source_Loc,
-                                 I_Type          => CProver_Size_T,
-                                 Range_Check     => False,
-                                 Value           => Value_Hex);
+   begin
+      return Integer_Constant_To_Expr (UI_From_Int (Value), CProver_Size_T,
+                                       Size_T_Width, Source_Loc);
    end Build_Index_Constant;
 
    function Build_Array_Size (First : Irep; Last : Irep) return Irep
@@ -503,14 +498,25 @@ package body GOTO_Utils is
       return False;
    end Has_GNAT2goto_Annotation;
 
+   function Integer_Constant_To_BV_Expr
+     (Value : Uint;
+      Expr_Type : Irep;
+      Source_Location : Source_Ptr)
+      return Irep is
+   begin
+      return Integer_Constant_To_Expr (Value, Expr_Type, Get_Width (Expr_Type),
+                                       Source_Location);
+   end Integer_Constant_To_BV_Expr;
+
    function Integer_Constant_To_Expr
      (Value : Uint;
       Expr_Type : Irep;
+      Type_Width : Integer;
       Source_Location : Source_Ptr)
    return Irep is
       Value_Hex : constant String := Convert_Uint_To_Hex
         (Value => Value,
-         Bit_Width => Pos (Get_Width (Expr_Type)));
+         Bit_Width => Pos (Type_Width));
    begin
       return Make_Constant_Expr
         (Source_Location => Source_Location,

gnat2goto/driver/goto_utils.ads

@@ -4,6 +4,7 @@ with Atree;             use Atree;
 with Sinfo;             use Sinfo;
 with Symbol_Table_Info; use Symbol_Table_Info;
 with Uintp;                 use Uintp;
+with GNAT.Table;
 
 package GOTO_Utils is
 
@@ -14,11 +15,21 @@ package GOTO_Utils is
    --  Utility routines for high-level GOTO AST construction
 
    Pointer_Type_Width : constant Positive := 64;
-   Size_T_Width : constant Int := 64;
+   Size_T_Width : constant Integer := 64;
    --  ??? this should be queried at runtime from GNAT
 
    Synthetic_Variable_Counter : Positive := 1;
 
+   type String_Access is access String;
+
+   package Addressed_Variables is new
+     GNAT.Table (Table_Component_Type => String_Access,
+            Table_Index_Type     => Natural,
+            Table_Low_Bound      => 1,
+            Table_Initial        => 1,
+            Table_Increment      => 20);
+   --  Addressed_Variables : Addressed_Variables_Table.Table;
+
    function Fresh_Var_Name (Infix : String) return String;
    function Fresh_Var_Symbol_Expr (Ty : Irep; Infix : String) return Irep;
 
@@ -129,7 +140,8 @@ package GOTO_Utils is
    function Float_Mantissa_Size (Float_Type : Irep) return Integer;
 
    function Build_Index_Constant (Value : Int;
-                                  Source_Loc : Source_Ptr) return Irep;
+                                  Source_Loc : Source_Ptr) return Irep
+     with Post => Kind (Build_Index_Constant'Result) = I_Constant_Expr;
 
    function Name_Has_Prefix (N : Node_Id; Prefix : String) return Boolean;
 
@@ -140,13 +152,22 @@ package GOTO_Utils is
    --  checks whether an entity has a certain GNAT2goto annotation.
    --  This can be either an aspect, or a pragma.
 
-   function Integer_Constant_To_Expr
+   function Integer_Constant_To_BV_Expr
      (Value : Uint;
       Expr_Type : Irep;
       Source_Location : Source_Ptr)
    return Irep
    with Pre => Kind (Expr_Type) in Class_Bitvector_Type,
-        Post => Kind (Integer_Constant_To_Expr'Result) = I_Constant_Expr;
+     Post => Kind (Integer_Constant_To_BV_Expr'Result) = I_Constant_Expr;
+
+   function Integer_Constant_To_Expr
+     (Value : Uint;
+      Expr_Type : Irep;
+      Type_Width : Integer;
+      Source_Location : Source_Ptr)
+      return Irep
+     with Pre => Kind (Expr_Type) in Class_Type,
+     Post => Kind (Integer_Constant_To_Expr'Result) = I_Constant_Expr;
 
    function Make_Simple_Side_Effect_Expr_Function_Call
      (Arguments : Irep_Array;

gnat2goto/driver/tree_walk.adb

@@ -3203,30 +3203,30 @@ package body Tree_Walk is
       Expon_Divisible_By_Two : constant Irep := Make_Op_Eq
         (Lhs => Make_Op_Mod
            (Lhs => Exponent_Sym,
-            Rhs => Integer_Constant_To_Expr
+            Rhs => Integer_Constant_To_BV_Expr
               (Value => Uint_2,
                Expr_Type => Exponent_Type,
                Source_Location => Source_Location),
             Source_Location => Source_Location,
             Div_By_Zero_Check => False,
             I_Type => Exponent_Type),
-         Rhs => Integer_Constant_To_Expr
+         Rhs => Integer_Constant_To_BV_Expr
            (Value => Uint_0,
             Expr_Type => Exponent_Type,
             Source_Location => Source_Location),
          I_Type => Make_Bool_Type,
          Source_Location => Source_Location);
       Expon_Greater_Zero : constant Irep := Make_Op_Gt
         (Lhs => Exponent_Sym,
-         Rhs => Integer_Constant_To_Expr
+         Rhs => Integer_Constant_To_BV_Expr
            (Value => Uint_0,
             Expr_Type => Exponent_Type,
             Source_Location => Source_Location),
          Source_Location => Source_Location,
          I_Type => Make_Bool_Type);
       Set_Expon_Result_To_One : constant Irep := Make_Code_Assign
         (Lhs => Expon_Result,
-         Rhs => Integer_Constant_To_Expr
+         Rhs => Integer_Constant_To_BV_Expr
            (Value => Uint_1,
             Expr_Type => Mod_Type,
             Source_Location => Source_Location),
@@ -3243,7 +3243,7 @@ package body Tree_Walk is
         (Lhs => Exponent_Sym,
          Rhs => Make_Op_Div
            (Lhs => Exponent_Sym,
-            Rhs => Integer_Constant_To_Expr
+            Rhs => Integer_Constant_To_BV_Expr
               (Value => Uint_2,
                Expr_Type => Exponent_Type,
                Source_Location => Source_Location),
@@ -3263,7 +3263,7 @@ package body Tree_Walk is
         (Lhs => Exponent_Sym,
          Rhs => Make_Op_Sub
            (Lhs => Exponent_Sym,
-            Rhs => Integer_Constant_To_Expr
+            Rhs => Integer_Constant_To_BV_Expr
               (Value => Uint_1,
                Expr_Type => Exponent_Type,
                Source_Location => Source_Location),
@@ -4633,18 +4633,16 @@ package body Tree_Walk is
          Entity_Esize : constant Uint := Esize (Entity (N));
          Target_Type_Irep : constant Irep :=
            Follow_Symbol_Type (Get_Type (Target_Name), Global_Symbol_Table);
-         Expression_Value : constant Uint := Intval (Expression (N));
       begin
          pragma Assert (Kind (Target_Type_Irep) in Class_Type);
          if Attr_Id = "size" then
-
             --  Just check that the front-end already applied this size
             --  clause, i .e. that the size of type-irep we already had
             --  equals the entity type this clause is applied to (and the
             --  size specified in this clause).
             pragma Assert (Entity_Esize =
                              UI_From_Int (Int (Get_Width (Target_Type_Irep)))
-                           and Entity_Esize = Expression_Value);
+                           and Entity_Esize = Intval (Expression (N)));
             return;
          elsif Attr_Id = "component_size" then
             if not Is_Array_Type (Entity (N)) then
@@ -4660,6 +4658,7 @@ package body Tree_Walk is
                                      Global_Symbol_Table);
                Target_Subtype_Width : constant Uint :=
                  UI_From_Int (Int (Get_Width (Target_Subtype)));
+               Expression_Value : constant Uint := Intval (Expression (N));
             begin
                if Component_Size (Entity (N)) /= Expression_Value or
                  Target_Subtype_Width /= Expression_Value
@@ -4670,10 +4669,66 @@ package body Tree_Walk is
                end if;
             end;
             return;
-         end if;
 
-         Report_Unhandled_Node_Empty (N, "Process_Declaration",
+         elsif Attr_Id = "address" then
+            --  Assuming this Ada code:
+            --------------------
+            --  Var : VarType;
+            --  for Var'Address use System'To_Address (hex_address);
+            --------------------
+            --
+            --  Produce this C code:
+            --------------------
+            --  VarType *Ptr_Var;
+            --  Ptr_Var = (VarType*)hex_address;
+            --------------------
+            pragma Assert (Global_Symbol_Table.Contains (Intern
+                           (Get_Identifier (Target_Name))));
+
+            declare
+               --  Address_Expr : constant Irep :=
+               --    Do_Expression (Expression (N));
+               --  TODO : we assume function call, either check or generalise
+               Function_Call : constant Node_Id := Expression (N);
+               Parameters : constant List_Id :=
+                 Parameter_Associations (Function_Call);
+               Address_Uint : constant Uint := Intval (First (Parameters));
+               Source_Loc : constant Source_Ptr := Sloc (N);
+               Address_Expr : constant Irep :=
+                 Integer_Constant_To_Expr (Value           => Address_Uint,
+                                           Expr_Type       => CProver_Size_T,
+                                           Type_Width      => Size_T_Width,
+                                           Source_Location => Source_Loc);
+               Address_Type : constant Irep :=
+                 Make_Pointer_Type (Target_Type_Irep);
+               Lhs_Expr : constant Irep :=
+                 Make_Symbol_Expr (Source_Location => Source_Loc,
+                                   I_Type          => Address_Type,
+                                   Range_Check     => False,
+                                   Identifier      =>
+                                     "Ptr_" & Get_Identifier (Target_Name));
+               Rhs_Expr : constant Irep :=
+                 Typecast_If_Necessary (Expr     => Address_Expr,
+                                        New_Type => Address_Type,
+                                        A_Symbol_Table => Global_Symbol_Table);
+            begin
+               New_Object_Symbol_Entry
+                 (Object_Name       =>
+                    Intern ("Ptr_" & Get_Identifier (Target_Name)),
+                  Object_Type       => Address_Type,
+                  Object_Init_Value => Rhs_Expr,
+                  A_Symbol_Table    => Global_Symbol_Table);
+               Append_Declare_And_Init (Symbol     => Lhs_Expr,
+                                        Value      => Rhs_Expr,
+                                        Block      => Block,
+                                        Source_Loc => Source_Loc);
+               Addressed_Variables.Append (
+                     new String'(Get_Identifier (Target_Name)));
+            end;
+         else
+            Report_Unhandled_Node_Empty (N, "Process_Declaration",
                               "Representation clause unsupported: " & Attr_Id);
+         end if;
       end Handle_Representation_Clause;
 
    begin