Skip to content

Commit 9e5e523

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 c243f55 commit 9e5e523

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
@@ -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),

0 commit comments

Comments
 (0)