From b1567bc743197df925ec4caa7d2960120fa6789d Mon Sep 17 00:00:00 2001 From: xbauch Date: Thu, 6 Jun 2019 14:12:23 +0100 Subject: [PATCH 01/11] Unify creating integer constants We now have three wrappers: 1: takes values (results has type cprover_size_t) 2: takes value, type (type is assumed to be bit-vector) 3: takes value, type, bit-width. --- gnat2goto/driver/driver.adb | 6 +++--- gnat2goto/driver/goto_utils.adb | 24 +++++++++++++++--------- gnat2goto/driver/goto_utils.ads | 18 ++++++++++++++---- gnat2goto/driver/tree_walk.adb | 12 ++++++------ 4 files changed, 38 insertions(+), 22 deletions(-) diff --git a/gnat2goto/driver/driver.adb b/gnat2goto/driver/driver.adb index ca20e99b1..16f207ea7 100644 --- a/gnat2goto/driver/driver.adb +++ b/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); diff --git a/gnat2goto/driver/goto_utils.adb b/gnat2goto/driver/goto_utils.adb index 089e723a9..344d34fc6 100644 --- a/gnat2goto/driver/goto_utils.adb +++ b/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, diff --git a/gnat2goto/driver/goto_utils.ads b/gnat2goto/driver/goto_utils.ads index 66f24b86f..26298c3fd 100644 --- a/gnat2goto/driver/goto_utils.ads +++ b/gnat2goto/driver/goto_utils.ads @@ -14,7 +14,7 @@ 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; @@ -129,7 +129,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 +141,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; diff --git a/gnat2goto/driver/tree_walk.adb b/gnat2goto/driver/tree_walk.adb index 57faed738..19ed60c83 100644 --- a/gnat2goto/driver/tree_walk.adb +++ b/gnat2goto/driver/tree_walk.adb @@ -3203,14 +3203,14 @@ 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), @@ -3218,7 +3218,7 @@ package body Tree_Walk is 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), @@ -3226,7 +3226,7 @@ package body Tree_Walk is 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), From 1f7f49a4bb5a72b4b89468fc83e3998cd280f1e8 Mon Sep 17 00:00:00 2001 From: xbauch Date: Thu, 6 Jun 2019 14:30:25 +0100 Subject: [PATCH 02/11] Implement representation clause address We handle it by 1: declaring a new variable with type one pointer deeper 2: assign the address to it 3: store the name (we'll need to replace it in the symbol table -- next commit) --- gnat2goto/driver/goto_utils.ads | 10 +++++ gnat2goto/driver/tree_walk.adb | 76 ++++++++++++++++++++++++++++++--- 2 files changed, 81 insertions(+), 5 deletions(-) diff --git a/gnat2goto/driver/goto_utils.ads b/gnat2goto/driver/goto_utils.ads index 26298c3fd..12ab65116 100644 --- a/gnat2goto/driver/goto_utils.ads +++ b/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 @@ -19,6 +20,15 @@ package GOTO_Utils is 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); + function Fresh_Var_Name (Infix : String) return String; function Fresh_Var_Symbol_Expr (Ty : Irep; Infix : String) return Irep; diff --git a/gnat2goto/driver/tree_walk.adb b/gnat2goto/driver/tree_walk.adb index 19ed60c83..872c98989 100644 --- a/gnat2goto/driver/tree_walk.adb +++ b/gnat2goto/driver/tree_walk.adb @@ -4634,18 +4634,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 @@ -4661,6 +4659,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 @@ -4671,10 +4670,77 @@ 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 + Source_Loc : constant Source_Ptr := Sloc (N); + function Get_Address_Expr return Irep; + function Get_Address_Expr return Irep is + begin + if Nkind (Expression (N)) = N_Function_Call then + declare + Parameters : constant List_Id := + Parameter_Associations (Expression (N)); + begin + pragma Assert (not Is_Empty_List (Parameters) and then + Nkind (First (Parameters)) = N_Integer_Literal); + return + Integer_Constant_To_Expr + (Value => Intval (First (Parameters)), + Expr_Type => CProver_Size_T, + Type_Width => Size_T_Width, + Source_Location => Source_Loc); + end; + else + return Do_Expression (Expression (N)); + end if; + end Get_Address_Expr; + + Address_Expr : constant Irep := Get_Address_Expr; + 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 From 2db62c7182cfe21013e13d302aec513c33426060 Mon Sep 17 00:00:00 2001 From: xbauch Date: Thu, 6 Jun 2019 14:33:35 +0100 Subject: [PATCH 03/11] 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. --- gnat2goto/driver/driver.adb | 16 +++- gnat2goto/ireps/ireps-wrap_pointer.adb | 42 +++++++++ gnat2goto/ireps/ireps_generator.py | 115 +++++++++++++++++++++++++ 3 files changed, 170 insertions(+), 3 deletions(-) create mode 100644 gnat2goto/ireps/ireps-wrap_pointer.adb diff --git a/gnat2goto/driver/driver.adb b/gnat2goto/driver/driver.adb index 16f207ea7..b772ca1e6 100644 --- a/gnat2goto/driver/driver.adb +++ b/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), diff --git a/gnat2goto/ireps/ireps-wrap_pointer.adb b/gnat2goto/ireps/ireps-wrap_pointer.adb new file mode 100644 index 000000000..bffe0e3c2 --- /dev/null +++ b/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; diff --git a/gnat2goto/ireps/ireps_generator.py b/gnat2goto/ireps/ireps_generator.py index 7547bc382..24d531da8 100755 --- a/gnat2goto/ireps/ireps_generator.py +++ b/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") From 3f2cd54824db0a4699416fe2e24797c7aa2a7547 Mon Sep 17 00:00:00 2001 From: xbauch Date: Thu, 6 Jun 2019 14:36:36 +0100 Subject: [PATCH 04/11] Introduce cprover_memory into the symbol table. Since it was missing and CBMC need it for pointer analysis. --- gnat2goto/driver/driver.adb | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/gnat2goto/driver/driver.adb b/gnat2goto/driver/driver.adb index b772ca1e6..eb0462c8a 100644 --- a/gnat2goto/driver/driver.adb +++ b/gnat2goto/driver/driver.adb @@ -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; From 22d8f04dc5a94608069dbe9aa767c4f669f4aa7c Mon Sep 17 00:00:00 2001 From: xbauch Date: Thu, 6 Jun 2019 14:39:38 +0100 Subject: [PATCH 05/11] Testcase for representation clause address --- .../tests/representation_clause_address/test.adb | 11 +++++++++++ .../tests/representation_clause_address/test.out | 2 ++ .../tests/representation_clause_address/test.py | 3 +++ 3 files changed, 16 insertions(+) create mode 100644 testsuite/gnat2goto/tests/representation_clause_address/test.adb create mode 100644 testsuite/gnat2goto/tests/representation_clause_address/test.out create mode 100644 testsuite/gnat2goto/tests/representation_clause_address/test.py diff --git a/testsuite/gnat2goto/tests/representation_clause_address/test.adb b/testsuite/gnat2goto/tests/representation_clause_address/test.adb new file mode 100644 index 000000000..f5a8212dd --- /dev/null +++ b/testsuite/gnat2goto/tests/representation_clause_address/test.adb @@ -0,0 +1,11 @@ +with System; + +procedure Test is + -- A 32 bit hardware register + type Unsigned_32 is mod 2 ** 32; + Device_Input_Value: Unsigned_32; + for Device_Input_Value'Address use System'To_Address (16#8000_05C4#); +begin + Device_Input_Value := 5; + pragma Assert (Device_Input_Value + 1 = 6); +end Test; diff --git a/testsuite/gnat2goto/tests/representation_clause_address/test.out b/testsuite/gnat2goto/tests/representation_clause_address/test.out new file mode 100644 index 000000000..f6fc93b95 --- /dev/null +++ b/testsuite/gnat2goto/tests/representation_clause_address/test.out @@ -0,0 +1,2 @@ +[1] file test.adb line 10 assertion: SUCCESS +VERIFICATION SUCCESSFUL diff --git a/testsuite/gnat2goto/tests/representation_clause_address/test.py b/testsuite/gnat2goto/tests/representation_clause_address/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/representation_clause_address/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove() From a80baf8ce529db9ba31c5073fe149b47cf3cd9e6 Mon Sep 17 00:00:00 2001 From: xbauch Date: Fri, 7 Jun 2019 10:03:11 +0100 Subject: [PATCH 06/11] Decorate addressed variables with dollar sign and via a helper function. --- gnat2goto/driver/tree_walk.adb | 8 ++++---- gnat2goto/ireps/ireps_generator.py | 16 +++++++++++++++- 2 files changed, 19 insertions(+), 5 deletions(-) diff --git a/gnat2goto/driver/tree_walk.adb b/gnat2goto/driver/tree_walk.adb index 872c98989..33e38d95b 100644 --- a/gnat2goto/driver/tree_walk.adb +++ b/gnat2goto/driver/tree_walk.adb @@ -4713,20 +4713,20 @@ package body Tree_Walk is Address_Expr : constant Irep := Get_Address_Expr; Address_Type : constant Irep := Make_Pointer_Type (Target_Type_Irep); + Decorated_Name : constant String := + Decorate_Addressed_Variables (Get_Identifier (Target_Name)); Lhs_Expr : constant Irep := Make_Symbol_Expr (Source_Location => Source_Loc, I_Type => Address_Type, Range_Check => False, - Identifier => - "Ptr_" & Get_Identifier (Target_Name)); + Identifier => Decorated_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_Name => Intern (Decorated_Name), Object_Type => Address_Type, Object_Init_Value => Rhs_Expr, A_Symbol_Table => Global_Symbol_Table); diff --git a/gnat2goto/ireps/ireps_generator.py b/gnat2goto/ireps/ireps_generator.py index 24d531da8..9f86d85bc 100755 --- a/gnat2goto/ireps/ireps_generator.py +++ b/gnat2goto/ireps/ireps_generator.py @@ -1878,6 +1878,10 @@ def generate_code(self, optimize, schema_file_names): write(s, "-- Increase Pointer Depth") write(s, "") + write(s, "function Decorate_Addressed_Variables (Name : String) return String;") + write(s, "-- Create Decorated Name") + write(s, "") + write(s, "function Remove_Extra_Type_Information (I : Irep) return Irep;") write(s, "-- Remove Type Bounds") write(s, "") @@ -2130,7 +2134,8 @@ def generate_code(self, optimize, schema_file_names): 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, "Make_Pointer_Type (Get_Type (I), 64), False,") + write(b, "Decorate_Addressed_Variables (Name)),") write(b, "Get_Source_Location (I), Get_Type (I));") write(b, "end if;") write(b, "") @@ -2151,6 +2156,15 @@ def generate_code(self, optimize, schema_file_names): write(b, "end Wrap_Pointer;") write(b, "") + write_comment_block(b, "Decorate_Addressed_Variables") + write(b, "function Decorate_Addressed_Variables (Name : String) return String") + write(b, "is") + write(b, "begin") + with indent(b): + write(b, "return Name & \"$Ptr\";") + write(b, "end Decorate_Addressed_Variables;") + write(b, "") + write_comment_block(b, "Remove_Extra_Type_Information") write(b, "function Remove_Extra_Type_Information (I : Irep) return Irep") write(b, "is") From 1b3ba7f61920558a28a5e5d5afab1e8159505cca Mon Sep 17 00:00:00 2001 From: xbauch Date: Fri, 7 Jun 2019 10:04:14 +0100 Subject: [PATCH 07/11] Implement handling the address attribute by returning address-of expression. --- gnat2goto/driver/tree_walk.adb | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/gnat2goto/driver/tree_walk.adb b/gnat2goto/driver/tree_walk.adb index 33e38d95b..ec3848ce2 100644 --- a/gnat2goto/driver/tree_walk.adb +++ b/gnat2goto/driver/tree_walk.adb @@ -384,6 +384,12 @@ package body Tree_Walk is and then List_Length (Expressions (N)) = 1), Post => Kind (Do_Attribute_Succ_Discrete'Result) in Class_Expr; + function Do_Attribute_Address (N : Node_Id) return Irep + with Pre => (Nkind (N) = N_Attribute_Reference + and then Get_Attribute_Id (Attribute_Name (N)) = + Attribute_Address), + Post => Kind (Do_Attribute_Address'Result) in Class_Expr; + function Make_Malloc_Function_Call_Expr (Num_Elem : Irep; Element_Type_Size : Uint; Source_Loc : Source_Ptr) @@ -1358,6 +1364,12 @@ package body Tree_Walk is I_Type => Result_Type); end Do_Attribute_Succ_Discrete; + function Do_Attribute_Address (N : Node_Id) return Irep is + Arg_Expr : constant Irep := Do_Expression (Prefix (N)); + begin + return Make_Address_Of (Arg_Expr); + end Do_Attribute_Address; + ------------------- -- Do_Expression -- ------------------- @@ -1399,6 +1411,8 @@ package body Tree_Walk is return Do_Attribute_Pred_Discrete (N); when Attribute_Succ => return Do_Attribute_Succ_Discrete (N); + when Attribute_Address => + return Do_Attribute_Address (N); when others => return Report_Unhandled_Node_Irep (N, "Do_Expression", "Unknown attribute"); From 2e228e290f053ac011042557812dc96d02568aeb Mon Sep 17 00:00:00 2001 From: xbauch Date: Fri, 7 Jun 2019 12:33:30 +0100 Subject: [PATCH 08/11] Implement checking string prefix --- gnat2goto/driver/goto_utils.adb | 12 ++++++++++++ gnat2goto/driver/goto_utils.ads | 2 ++ 2 files changed, 14 insertions(+) diff --git a/gnat2goto/driver/goto_utils.adb b/gnat2goto/driver/goto_utils.adb index 344d34fc6..07bd30797 100644 --- a/gnat2goto/driver/goto_utils.adb +++ b/gnat2goto/driver/goto_utils.adb @@ -30,6 +30,18 @@ package body GOTO_Utils is return R; end Make_Address_Of; + function Is_Prefix (Prefix : String; Base_String : String) return Boolean + is + begin + if Prefix'Length < Base_String'Length and then + Prefix = Base_String (Base_String'First .. Prefix'Length) + then + return True; + else + return False; + end if; + end Is_Prefix; + ------------------- -- Make_Int_Type -- ------------------- diff --git a/gnat2goto/driver/goto_utils.ads b/gnat2goto/driver/goto_utils.ads index 12ab65116..51851fe5c 100644 --- a/gnat2goto/driver/goto_utils.ads +++ b/gnat2goto/driver/goto_utils.ads @@ -22,6 +22,8 @@ package GOTO_Utils is type String_Access is access String; + function Is_Prefix (Prefix : String; Base_String : String) return Boolean; + package Addressed_Variables is new GNAT.Table (Table_Component_Type => String_Access, Table_Index_Type => Natural, From 35808eb2f45a1aa8f5433d5236a34f8ab4a5bef0 Mon Sep 17 00:00:00 2001 From: xbauch Date: Fri, 7 Jun 2019 12:33:46 +0100 Subject: [PATCH 09/11] Add default body for some subprograms and that to those that have identity-like type: A -> A. The default body is exactly that identity. And their name starts with "system". --- gnat2goto/driver/goto_utils.adb | 20 +++++++++++++++++++- gnat2goto/driver/goto_utils.ads | 8 +++++++- gnat2goto/driver/tree_walk.adb | 8 ++++++++ 3 files changed, 34 insertions(+), 2 deletions(-) diff --git a/gnat2goto/driver/goto_utils.adb b/gnat2goto/driver/goto_utils.adb index 07bd30797..2134ef418 100644 --- a/gnat2goto/driver/goto_utils.adb +++ b/gnat2goto/driver/goto_utils.adb @@ -153,6 +153,7 @@ package body GOTO_Utils is procedure New_Subprogram_Symbol_Entry (Subprog_Name : Symbol_Id; Subprog_Type : Irep; + Subprog_Body : Irep; A_Symbol_Table : in out Symbol_Table) is Subprog_Symbol : Symbol; @@ -162,7 +163,7 @@ package body GOTO_Utils is Subprog_Symbol.PrettyName := Subprog_Name; Subprog_Symbol.SymType := Subprog_Type; Subprog_Symbol.Mode := Intern ("C"); - Subprog_Symbol.Value := Make_Nil (No_Location); + Subprog_Symbol.Value := Subprog_Body; A_Symbol_Table.Insert (Subprog_Name, Subprog_Symbol); end New_Subprogram_Symbol_Entry; @@ -363,6 +364,23 @@ package body GOTO_Utils is A_Symbol_Table => A_Symbol_Table); end Build_Function; + function Build_Identity_Body (Parameters : Irep) return Irep + is + Parameter_List : constant Irep_List := Get_Parameter (Parameters); + First_Cursor : constant List_Cursor := List_First (Parameter_List); + Body_Block : constant Irep := + Make_Code_Block (Source_Location => No_Location, + I_Type => Make_Nil_Type); + begin + pragma Assert (List_Has_Element (Parameter_List, First_Cursor)); + Append_Op (Body_Block, + Make_Code_Return (Return_Value => + Param_Symbol (List_Element (Parameter_List, First_Cursor)), + Source_Location => No_Location, + I_Type => Make_Nil_Type)); + return Body_Block; + end Build_Identity_Body; + function Build_Index_Constant (Value : Int; Source_Loc : Source_Ptr) return Irep is diff --git a/gnat2goto/driver/goto_utils.ads b/gnat2goto/driver/goto_utils.ads index 51851fe5c..d665e13d2 100644 --- a/gnat2goto/driver/goto_utils.ads +++ b/gnat2goto/driver/goto_utils.ads @@ -63,8 +63,10 @@ package GOTO_Utils is procedure New_Subprogram_Symbol_Entry (Subprog_Name : Symbol_Id; Subprog_Type : Irep; + Subprog_Body : Irep; A_Symbol_Table : in out Symbol_Table) - with Pre => Kind (Subprog_Type) = I_Code_Type; + with Pre => Kind (Subprog_Type) = I_Code_Type + and Kind (Subprog_Body) in I_Nil | I_Code_Block; -- Insert the subprogram specification into the symbol table procedure New_Type_Symbol_Entry (Type_Name : Symbol_Id; Type_Of_Type : Irep; @@ -116,6 +118,10 @@ package GOTO_Utils is and then Kind (Func_Params) = I_Parameter_List and then Kind (FBody) in Class_Code); + function Build_Identity_Body (Parameters : Irep) return Irep + with Pre => Kind (Parameters) = I_Parameter_List, + Post => Kind (Build_Identity_Body'Result) = I_Code_Block; + function Build_Array_Size (Array_Comp : Irep) return Irep with Pre => Kind (Array_Comp) in Class_Expr, Post => Kind (Build_Array_Size'Result) = I_Op_Add; diff --git a/gnat2goto/driver/tree_walk.adb b/gnat2goto/driver/tree_walk.adb index ec3848ce2..7a8037e56 100644 --- a/gnat2goto/driver/tree_walk.adb +++ b/gnat2goto/driver/tree_walk.adb @@ -5458,9 +5458,17 @@ package body Tree_Walk is Do_Subprogram_Specification (N); Subprog_Name : constant Symbol_Id := Intern (Unique_Name (Defining_Unit_Name (N))); + Default_Body : Irep := Make_Nil (Sloc (N)); begin + if List_Length (Parameter_Specifications (N)) = 1 and + not (Kind (Get_Return_Type (Subprog_Type)) = I_Void_Type) and + Is_Prefix ("system", Unique_Name (Defining_Unit_Name (N))) + then + Default_Body := Build_Identity_Body (Get_Parameters (Subprog_Type)); + end if; New_Subprogram_Symbol_Entry (Subprog_Name => Subprog_Name, Subprog_Type => Subprog_Type, + Subprog_Body => Default_Body, A_Symbol_Table => Global_Symbol_Table); end Register_Subprogram_Specification; From 0c60e2b06521748e93a5512b27d04720a660b091 Mon Sep 17 00:00:00 2001 From: xbauch Date: Fri, 7 Jun 2019 12:34:15 +0100 Subject: [PATCH 10/11] Extend the test to check the address --- .../gnat2goto/tests/representation_clause_address/test.adb | 3 ++- .../gnat2goto/tests/representation_clause_address/test.out | 1 + 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/testsuite/gnat2goto/tests/representation_clause_address/test.adb b/testsuite/gnat2goto/tests/representation_clause_address/test.adb index f5a8212dd..c585871c0 100644 --- a/testsuite/gnat2goto/tests/representation_clause_address/test.adb +++ b/testsuite/gnat2goto/tests/representation_clause_address/test.adb @@ -1,4 +1,4 @@ -with System; +with System; use System; procedure Test is -- A 32 bit hardware register @@ -8,4 +8,5 @@ procedure Test is begin Device_Input_Value := 5; pragma Assert (Device_Input_Value + 1 = 6); + pragma Assert (Device_Input_Value'Address = System'To_Address (16#8000_05C4#)); end Test; diff --git a/testsuite/gnat2goto/tests/representation_clause_address/test.out b/testsuite/gnat2goto/tests/representation_clause_address/test.out index f6fc93b95..ee7d89a5f 100644 --- a/testsuite/gnat2goto/tests/representation_clause_address/test.out +++ b/testsuite/gnat2goto/tests/representation_clause_address/test.out @@ -1,2 +1,3 @@ [1] file test.adb line 10 assertion: SUCCESS +[2] file test.adb line 11 assertion: SUCCESS VERIFICATION SUCCESSFUL From 743d8d91e434f0209020967cb4fe0d1cda13cba2 Mon Sep 17 00:00:00 2001 From: xbauch Date: Fri, 7 Jun 2019 13:11:29 +0100 Subject: [PATCH 11/11] Update golden results --- experiments/golden-results/StratoX-summary.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/experiments/golden-results/StratoX-summary.txt b/experiments/golden-results/StratoX-summary.txt index 79d832f2c..c07992158 100644 --- a/experiments/golden-results/StratoX-summary.txt +++ b/experiments/golden-results/StratoX-summary.txt @@ -23,7 +23,7 @@ Calling function: Do_Type_Definition Error message: Access type unsupported Nkind: N_Access_To_Object_Definition -- -Occurs: 42 times +Occurs: 39 times Calling function: Do_Expression Error message: Unknown attribute Nkind: N_Attribute_Reference