Skip to content

Commit 4c4708d

Browse files
petr-bauchpetr-bauch
committed
Testing commit
1 parent c243f55 commit 4c4708d

File tree

8 files changed

+276
-30
lines changed

8 files changed

+276
-30
lines changed

‎gnat2goto/driver/driver.adb‎

Lines changed: 40 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -200,7 +200,7 @@ package body Driver is
200200
(I_Type => Dead_Object_Type,
201201
Identifier => "__CPROVER_dead_object",
202202
Source_Location => No_Location);
203-
Dead_Object_Val : constant Irep := Integer_Constant_To_Expr
203+
Dead_Object_Val : constant Irep := Integer_Constant_To_BV_Expr
204204
(Value => Uint_0,
205205
Expr_Type => Dead_Object_Type,
206206
Source_Location => No_Location);
@@ -223,7 +223,7 @@ package body Driver is
223223
(I_Type => Deallocated_Type,
224224
Identifier => "__CPROVER_deallocated",
225225
Source_Location => No_Location);
226-
Deallocated_Val : constant Irep := Integer_Constant_To_Expr
226+
Deallocated_Val : constant Irep := Integer_Constant_To_BV_Expr
227227
(Value => Uint_0,
228228
Expr_Type => Deallocated_Type,
229229
Source_Location => No_Location);
@@ -246,7 +246,7 @@ package body Driver is
246246
(I_Type => Malloc_Object_Type,
247247
Identifier => "__CPROVER_malloc_object",
248248
Source_Location => No_Location);
249-
Malloc_Object_Val : constant Irep := Integer_Constant_To_Expr
249+
Malloc_Object_Val : constant Irep := Integer_Constant_To_BV_Expr
250250
(Value => Uint_0,
251251
Expr_Type => Malloc_Object_Type,
252252
Source_Location => No_Location);
@@ -260,6 +260,29 @@ package body Driver is
260260
Source_Location => No_Location));
261261
end Initialize_CProver_Malloc_Object;
262262

263+
procedure Initialize_CProver_Memory;
264+
procedure Initialize_CProver_Memory is
265+
Memory_Type : constant Irep := Make_Pointer_Type
266+
(I_Subtype => Make_Void_Type,
267+
Width => Pointer_Type_Width);
268+
Memory_Sym : constant Irep := Make_Symbol_Expr
269+
(I_Type => Memory_Type,
270+
Identifier => "__CPROVER_memory",
271+
Source_Location => No_Location);
272+
Memory_Val : constant Irep := Integer_Constant_To_BV_Expr
273+
(Value => Uint_0,
274+
Expr_Type => Memory_Type,
275+
Source_Location => No_Location);
276+
begin
277+
Declare_Missing_Global (Memory_Sym);
278+
Append_Op
279+
(Start_Body,
280+
Make_Code_Assign
281+
(Lhs => Memory_Sym,
282+
Rhs => Memory_Val,
283+
Source_Location => No_Location));
284+
end Initialize_CProver_Memory;
285+
263286
procedure Initialize_Enum_Values;
264287
procedure Initialize_Enum_Values is
265288

@@ -348,6 +371,7 @@ package body Driver is
348371
Initialize_CProver_Dead_Object;
349372
Initialize_CProver_Deallocated;
350373
Initialize_CProver_Malloc_Object;
374+
Initialize_CProver_Memory;
351375
Initialize_Enum_Values;
352376
Initialize_Boolean_Values;
353377
end Initialize_CProver_Internal_Variables;
@@ -705,10 +729,20 @@ package body Driver is
705729
begin
706730
Modified_Symbol.SymType :=
707731
Remove_Extra_Type_Information
708-
(Follow_Irep (SymType, Follow_Symbol'Access));
732+
(Follow_Irep (SymType, Follow_Symbol'Access));
733+
for K in 1 .. Addressed_Variables.Last loop
734+
Modified_Symbol.SymType := Wrap_Pointer
735+
(Modified_Symbol.SymType,
736+
Addressed_Variables.Table (K).all);
737+
end loop;
709738
Modified_Symbol.Value :=
710-
Remove_Extra_Type_Information
711-
(Follow_Irep (Value, Follow_Symbol'Access));
739+
Remove_Extra_Type_Information
740+
(Follow_Irep (Value, Follow_Symbol'Access));
741+
for K in 1 .. Addressed_Variables.Last loop
742+
Modified_Symbol.Value := Wrap_Pointer
743+
(Modified_Symbol.Value,
744+
Addressed_Variables.Table (K).all);
745+
end loop;
712746

713747
New_Table.Insert
714748
(Key => Symbol_Maps.Key (Sym_Iter),

‎gnat2goto/driver/goto_utils.adb‎

Lines changed: 15 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -354,14 +354,9 @@ package body GOTO_Utils is
354354
function Build_Index_Constant (Value : Int; Source_Loc : Source_Ptr)
355355
return Irep
356356
is
357-
Value_Hex : constant String :=
358-
Convert_Uint_To_Hex (Value => UI_From_Int (Value),
359-
Bit_Width => Size_T_Width);
360-
begin
361-
return Make_Constant_Expr (Source_Location => Source_Loc,
362-
I_Type => CProver_Size_T,
363-
Range_Check => False,
364-
Value => Value_Hex);
357+
begin
358+
return Integer_Constant_To_Expr (UI_From_Int (Value), CProver_Size_T,
359+
Size_T_Width, Source_Loc);
365360
end Build_Index_Constant;
366361

367362
function Build_Array_Size (First : Irep; Last : Irep) return Irep
@@ -503,14 +498,25 @@ package body GOTO_Utils is
503498
return False;
504499
end Has_GNAT2goto_Annotation;
505500

501+
function Integer_Constant_To_BV_Expr
502+
(Value : Uint;
503+
Expr_Type : Irep;
504+
Source_Location : Source_Ptr)
505+
return Irep is
506+
begin
507+
return Integer_Constant_To_Expr (Value, Expr_Type, Get_Width (Expr_Type),
508+
Source_Location);
509+
end Integer_Constant_To_BV_Expr;
510+
506511
function Integer_Constant_To_Expr
507512
(Value : Uint;
508513
Expr_Type : Irep;
514+
Type_Width : Integer;
509515
Source_Location : Source_Ptr)
510516
return Irep is
511517
Value_Hex : constant String := Convert_Uint_To_Hex
512518
(Value => Value,
513-
Bit_Width => Pos (Get_Width (Expr_Type)));
519+
Bit_Width => Pos (Type_Width));
514520
begin
515521
return Make_Constant_Expr
516522
(Source_Location => Source_Location,

‎gnat2goto/driver/goto_utils.ads‎

Lines changed: 25 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ with Atree; use Atree;
44
with Sinfo; use Sinfo;
55
with Symbol_Table_Info; use Symbol_Table_Info;
66
with Uintp; use Uintp;
7+
with GNAT.Table;
78

89
package GOTO_Utils is
910

@@ -14,11 +15,21 @@ package GOTO_Utils is
1415
-- Utility routines for high-level GOTO AST construction
1516

1617
Pointer_Type_Width : constant Positive := 64;
17-
Size_T_Width : constant Int := 64;
18+
Size_T_Width : constant Integer := 64;
1819
-- ??? this should be queried at runtime from GNAT
1920

2021
Synthetic_Variable_Counter : Positive := 1;
2122

23+
type String_Access is access String;
24+
25+
package Addressed_Variables is new
26+
GNAT.Table (Table_Component_Type => String_Access,
27+
Table_Index_Type => Natural,
28+
Table_Low_Bound => 1,
29+
Table_Initial => 1,
30+
Table_Increment => 20);
31+
-- Addressed_Variables : Addressed_Variables_Table.Table;
32+
2233
function Fresh_Var_Name (Infix : String) return String;
2334
function Fresh_Var_Symbol_Expr (Ty : Irep; Infix : String) return Irep;
2435

@@ -129,7 +140,8 @@ package GOTO_Utils is
129140
function Float_Mantissa_Size (Float_Type : Irep) return Integer;
130141

131142
function Build_Index_Constant (Value : Int;
132-
Source_Loc : Source_Ptr) return Irep;
143+
Source_Loc : Source_Ptr) return Irep
144+
with Post => Kind (Build_Index_Constant'Result) = I_Constant_Expr;
133145

134146
function Name_Has_Prefix (N : Node_Id; Prefix : String) return Boolean;
135147

@@ -140,13 +152,22 @@ package GOTO_Utils is
140152
-- checks whether an entity has a certain GNAT2goto annotation.
141153
-- This can be either an aspect, or a pragma.
142154

143-
function Integer_Constant_To_Expr
155+
function Integer_Constant_To_BV_Expr
144156
(Value : Uint;
145157
Expr_Type : Irep;
146158
Source_Location : Source_Ptr)
147159
return Irep
148160
with Pre => Kind (Expr_Type) in Class_Bitvector_Type,
149-
Post => Kind (Integer_Constant_To_Expr'Result) = I_Constant_Expr;
161+
Post => Kind (Integer_Constant_To_BV_Expr'Result) = I_Constant_Expr;
162+
163+
function Integer_Constant_To_Expr
164+
(Value : Uint;
165+
Expr_Type : Irep;
166+
Type_Width : Integer;
167+
Source_Location : Source_Ptr)
168+
return Irep
169+
with Pre => Kind (Expr_Type) in Class_Type,
170+
Post => Kind (Integer_Constant_To_Expr'Result) = I_Constant_Expr;
150171

151172
function Make_Simple_Side_Effect_Expr_Function_Call
152173
(Arguments : Irep_Array;

‎gnat2goto/driver/tree_walk.adb‎

Lines changed: 66 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -3203,30 +3203,30 @@ package body Tree_Walk is
32033203
Expon_Divisible_By_Two : constant Irep := Make_Op_Eq
32043204
(Lhs => Make_Op_Mod
32053205
(Lhs => Exponent_Sym,
3206-
Rhs => Integer_Constant_To_Expr
3206+
Rhs => Integer_Constant_To_BV_Expr
32073207
(Value => Uint_2,
32083208
Expr_Type => Exponent_Type,
32093209
Source_Location => Source_Location),
32103210
Source_Location => Source_Location,
32113211
Div_By_Zero_Check => False,
32123212
I_Type => Exponent_Type),
3213-
Rhs => Integer_Constant_To_Expr
3213+
Rhs => Integer_Constant_To_BV_Expr
32143214
(Value => Uint_0,
32153215
Expr_Type => Exponent_Type,
32163216
Source_Location => Source_Location),
32173217
I_Type => Make_Bool_Type,
32183218
Source_Location => Source_Location);
32193219
Expon_Greater_Zero : constant Irep := Make_Op_Gt
32203220
(Lhs => Exponent_Sym,
3221-
Rhs => Integer_Constant_To_Expr
3221+
Rhs => Integer_Constant_To_BV_Expr
32223222
(Value => Uint_0,
32233223
Expr_Type => Exponent_Type,
32243224
Source_Location => Source_Location),
32253225
Source_Location => Source_Location,
32263226
I_Type => Make_Bool_Type);
32273227
Set_Expon_Result_To_One : constant Irep := Make_Code_Assign
32283228
(Lhs => Expon_Result,
3229-
Rhs => Integer_Constant_To_Expr
3229+
Rhs => Integer_Constant_To_BV_Expr
32303230
(Value => Uint_1,
32313231
Expr_Type => Mod_Type,
32323232
Source_Location => Source_Location),
@@ -3243,7 +3243,7 @@ package body Tree_Walk is
32433243
(Lhs => Exponent_Sym,
32443244
Rhs => Make_Op_Div
32453245
(Lhs => Exponent_Sym,
3246-
Rhs => Integer_Constant_To_Expr
3246+
Rhs => Integer_Constant_To_BV_Expr
32473247
(Value => Uint_2,
32483248
Expr_Type => Exponent_Type,
32493249
Source_Location => Source_Location),
@@ -3263,7 +3263,7 @@ package body Tree_Walk is
32633263
(Lhs => Exponent_Sym,
32643264
Rhs => Make_Op_Sub
32653265
(Lhs => Exponent_Sym,
3266-
Rhs => Integer_Constant_To_Expr
3266+
Rhs => Integer_Constant_To_BV_Expr
32673267
(Value => Uint_1,
32683268
Expr_Type => Exponent_Type,
32693269
Source_Location => Source_Location),
@@ -4633,18 +4633,16 @@ package body Tree_Walk is
46334633
Entity_Esize : constant Uint := Esize (Entity (N));
46344634
Target_Type_Irep : constant Irep :=
46354635
Follow_Symbol_Type (Get_Type (Target_Name), Global_Symbol_Table);
4636-
Expression_Value : constant Uint := Intval (Expression (N));
46374636
begin
46384637
pragma Assert (Kind (Target_Type_Irep) in Class_Type);
46394638
if Attr_Id = "size" then
4640-
46414639
-- Just check that the front-end already applied this size
46424640
-- clause, i .e. that the size of type-irep we already had
46434641
-- equals the entity type this clause is applied to (and the
46444642
-- size specified in this clause).
46454643
pragma Assert (Entity_Esize =
46464644
UI_From_Int (Int (Get_Width (Target_Type_Irep)))
4647-
and Entity_Esize = Expression_Value);
4645+
and Entity_Esize = Intval (Expression (N)));
46484646
return;
46494647
elsif Attr_Id = "component_size" then
46504648
if not Is_Array_Type (Entity (N)) then
@@ -4660,6 +4658,7 @@ package body Tree_Walk is
46604658
Global_Symbol_Table);
46614659
Target_Subtype_Width : constant Uint :=
46624660
UI_From_Int (Int (Get_Width (Target_Subtype)));
4661+
Expression_Value : constant Uint := Intval (Expression (N));
46634662
begin
46644663
if Component_Size (Entity (N)) /= Expression_Value or
46654664
Target_Subtype_Width /= Expression_Value
@@ -4670,10 +4669,66 @@ package body Tree_Walk is
46704669
end if;
46714670
end;
46724671
return;
4673-
end if;
46744672

4675-
Report_Unhandled_Node_Empty (N, "Process_Declaration",
4673+
elsif Attr_Id = "address" then
4674+
-- Assuming this Ada code:
4675+
--------------------
4676+
-- Var : VarType;
4677+
-- for Var'Address use System'To_Address (hex_address);
4678+
--------------------
4679+
--
4680+
-- Produce this C code:
4681+
--------------------
4682+
-- VarType *Ptr_Var;
4683+
-- Ptr_Var = (VarType*)hex_address;
4684+
--------------------
4685+
pragma Assert (Global_Symbol_Table.Contains (Intern
4686+
(Get_Identifier (Target_Name))));
4687+
4688+
declare
4689+
-- Address_Expr : constant Irep :=
4690+
-- Do_Expression (Expression (N));
4691+
-- TODO : we assume function call, either check or generalise
4692+
Function_Call : constant Node_Id := Expression (N);
4693+
Parameters : constant List_Id :=
4694+
Parameter_Associations (Function_Call);
4695+
Address_Uint : constant Uint := Intval (First (Parameters));
4696+
Source_Loc : constant Source_Ptr := Sloc (N);
4697+
Address_Expr : constant Irep :=
4698+
Integer_Constant_To_Expr (Value => Address_Uint,
4699+
Expr_Type => CProver_Size_T,
4700+
Type_Width => Size_T_Width,
4701+
Source_Location => Source_Loc);
4702+
Address_Type : constant Irep :=
4703+
Make_Pointer_Type (Target_Type_Irep);
4704+
Lhs_Expr : constant Irep :=
4705+
Make_Symbol_Expr (Source_Location => Source_Loc,
4706+
I_Type => Address_Type,
4707+
Range_Check => False,
4708+
Identifier =>
4709+
"Ptr_" & Get_Identifier (Target_Name));
4710+
Rhs_Expr : constant Irep :=
4711+
Typecast_If_Necessary (Expr => Address_Expr,
4712+
New_Type => Address_Type,
4713+
A_Symbol_Table => Global_Symbol_Table);
4714+
begin
4715+
New_Object_Symbol_Entry
4716+
(Object_Name =>
4717+
Intern ("Ptr_" & Get_Identifier (Target_Name)),
4718+
Object_Type => Address_Type,
4719+
Object_Init_Value => Rhs_Expr,
4720+
A_Symbol_Table => Global_Symbol_Table);
4721+
Append_Declare_And_Init (Symbol => Lhs_Expr,
4722+
Value => Rhs_Expr,
4723+
Block => Block,
4724+
Source_Loc => Source_Loc);
4725+
Addressed_Variables.Append (
4726+
new String'(Get_Identifier (Target_Name)));
4727+
end;
4728+
else
4729+
Report_Unhandled_Node_Empty (N, "Process_Declaration",
46764730
"Representation clause unsupported: " & Attr_Id);
4731+
end if;
46774732
end Handle_Representation_Clause;
46784733

46794734
begin

0 commit comments

Comments
 (0)