Skip to content

Commit 9e32aee

Browse files
petr-bauchpetr-bauch
committed
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.
1 parent bad10de commit 9e32aee

File tree

4 files changed

+38
-22
lines changed

4 files changed

+38
-22
lines changed

‎gnat2goto/driver/driver.adb‎

Lines changed: 3 additions & 3 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);

‎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: 14 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ package GOTO_Utils is
1414
-- Utility routines for high-level GOTO AST construction
1515

1616
Pointer_Type_Width : constant Positive := 64;
17-
Size_T_Width : constant Int := 64;
17+
Size_T_Width : constant Integer := 64;
1818
-- ??? this should be queried at runtime from GNAT
1919

2020
Synthetic_Variable_Counter : Positive := 1;
@@ -129,7 +129,8 @@ package GOTO_Utils is
129129
function Float_Mantissa_Size (Float_Type : Irep) return Integer;
130130

131131
function Build_Index_Constant (Value : Int;
132-
Source_Loc : Source_Ptr) return Irep;
132+
Source_Loc : Source_Ptr) return Irep
133+
with Post => Kind (Build_Index_Constant'Result) = I_Constant_Expr;
133134

134135
function Name_Has_Prefix (N : Node_Id; Prefix : String) return Boolean;
135136

@@ -140,13 +141,22 @@ package GOTO_Utils is
140141
-- checks whether an entity has a certain GNAT2goto annotation.
141142
-- This can be either an aspect, or a pragma.
142143

143-
function Integer_Constant_To_Expr
144+
function Integer_Constant_To_BV_Expr
144145
(Value : Uint;
145146
Expr_Type : Irep;
146147
Source_Location : Source_Ptr)
147148
return Irep
148149
with Pre => Kind (Expr_Type) in Class_Bitvector_Type,
149-
Post => Kind (Integer_Constant_To_Expr'Result) = I_Constant_Expr;
150+
Post => Kind (Integer_Constant_To_BV_Expr'Result) = I_Constant_Expr;
151+
152+
function Integer_Constant_To_Expr
153+
(Value : Uint;
154+
Expr_Type : Irep;
155+
Type_Width : Integer;
156+
Source_Location : Source_Ptr)
157+
return Irep
158+
with Pre => Kind (Expr_Type) in Class_Type,
159+
Post => Kind (Integer_Constant_To_Expr'Result) = I_Constant_Expr;
150160

151161
function Make_Simple_Side_Effect_Expr_Function_Call
152162
(Arguments : Irep_Array;

‎gnat2goto/driver/tree_walk.adb‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3201,30 +3201,30 @@ package body Tree_Walk is
32013201
Expon_Divisible_By_Two : constant Irep := Make_Op_Eq
32023202
(Lhs => Make_Op_Mod
32033203
(Lhs => Exponent_Sym,
3204-
Rhs => Integer_Constant_To_Expr
3204+
Rhs => Integer_Constant_To_BV_Expr
32053205
(Value => Uint_2,
32063206
Expr_Type => Exponent_Type,
32073207
Source_Location => Source_Location),
32083208
Source_Location => Source_Location,
32093209
Div_By_Zero_Check => False,
32103210
I_Type => Exponent_Type),
3211-
Rhs => Integer_Constant_To_Expr
3211+
Rhs => Integer_Constant_To_BV_Expr
32123212
(Value => Uint_0,
32133213
Expr_Type => Exponent_Type,
32143214
Source_Location => Source_Location),
32153215
I_Type => Make_Bool_Type,
32163216
Source_Location => Source_Location);
32173217
Expon_Greater_Zero : constant Irep := Make_Op_Gt
32183218
(Lhs => Exponent_Sym,
3219-
Rhs => Integer_Constant_To_Expr
3219+
Rhs => Integer_Constant_To_BV_Expr
32203220
(Value => Uint_0,
32213221
Expr_Type => Exponent_Type,
32223222
Source_Location => Source_Location),
32233223
Source_Location => Source_Location,
32243224
I_Type => Make_Bool_Type);
32253225
Set_Expon_Result_To_One : constant Irep := Make_Code_Assign
32263226
(Lhs => Expon_Result,
3227-
Rhs => Integer_Constant_To_Expr
3227+
Rhs => Integer_Constant_To_BV_Expr
32283228
(Value => Uint_1,
32293229
Expr_Type => Mod_Type,
32303230
Source_Location => Source_Location),
@@ -3241,7 +3241,7 @@ package body Tree_Walk is
32413241
(Lhs => Exponent_Sym,
32423242
Rhs => Make_Op_Div
32433243
(Lhs => Exponent_Sym,
3244-
Rhs => Integer_Constant_To_Expr
3244+
Rhs => Integer_Constant_To_BV_Expr
32453245
(Value => Uint_2,
32463246
Expr_Type => Exponent_Type,
32473247
Source_Location => Source_Location),
@@ -3261,7 +3261,7 @@ package body Tree_Walk is
32613261
(Lhs => Exponent_Sym,
32623262
Rhs => Make_Op_Sub
32633263
(Lhs => Exponent_Sym,
3264-
Rhs => Integer_Constant_To_Expr
3264+
Rhs => Integer_Constant_To_BV_Expr
32653265
(Value => Uint_1,
32663266
Expr_Type => Exponent_Type,
32673267
Source_Location => Source_Location),

0 commit comments

Comments
 (0)