Skip to content

Commit ae04008

Browse files
petr-bauchpetr-bauch
committed
Add overflow-check
by slightly modifying the existing functionality for range-check and then calling the range-check building function with min/max value of the given type as bounds.
1 parent 365dd44 commit ae04008

File tree

2 files changed

+166
-96
lines changed

2 files changed

+166
-96
lines changed

‎gnat2goto/driver/range_check.adb

Lines changed: 157 additions & 88 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
with Sinfo; use Sinfo;
2-
31
with GOTO_Utils; use GOTO_Utils;
42

53
with Binary_To_Hex; use Binary_To_Hex;
@@ -92,12 +90,12 @@ package body Range_Check is
9290
else UI_From_Int (2 ** Type_Width - 1));
9391
begin
9492
return Make_Constant_Expr
95-
(Source_Location => Internal_Source_Location,
96-
I_Type => Bound_Type,
93+
(Source_Location => Get_Source_Location (N),
94+
I_Type => Maybe_Double_Type_Width (Bound_Type),
9795
Range_Check => False,
98-
Value =>
99-
Convert_Uint_To_Hex (Bound_Value,
100-
Types.Pos (Type_Width)));
96+
Value => Convert_Uint_To_Hex
97+
(Bound_Value,
98+
Types.Pos (Type_Width * 2)));
10199
end;
102100
when I_Signedbv_Type =>
103101
declare
@@ -108,12 +106,31 @@ package body Range_Check is
108106
else UI_From_Int (2 ** (Type_Width - 1) - 1));
109107
begin
110108
return Make_Constant_Expr
111-
(Source_Location => Internal_Source_Location,
112-
I_Type => Bound_Type,
109+
(Source_Location => Get_Source_Location (N),
110+
I_Type => Maybe_Double_Type_Width (Bound_Type),
111+
Range_Check => False,
112+
Value => Convert_Uint_To_Hex
113+
(Bound_Value,
114+
Types.Pos (Type_Width * 2)));
115+
end;
116+
when I_Floatbv_Type =>
117+
declare
118+
Smallest_Float : constant String := "C7EFFFFFE0000000";
119+
-- 0xff7fffff : single-precision min stored in double precision
120+
Largest_Float : constant String := "47EFFFFFE0000000";
121+
-- 0x7f7fffff : single-precision max stored in double precision
122+
Result_Type : constant Irep :=
123+
(case To_Float_Format (Get_Width (Bound_Type)) is
124+
when others => Float64_T);
125+
-- We may want to extend it here for wider floats
126+
begin
127+
return Make_Constant_Expr
128+
(Source_Location => Get_Source_Location (N),
129+
I_Type => Result_Type,
113130
Range_Check => False,
114-
Value =>
115-
Convert_Uint_To_Hex (Bound_Value,
116-
Types.Pos (Type_Width)));
131+
Value => (if Pos = Bound_Low
132+
then Smallest_Float
133+
else Largest_Float));
117134
end;
118135
when others =>
119136
return Report_Unhandled_Node_Irep (N, "Get_Bound",
@@ -145,19 +162,64 @@ package body Range_Check is
145162
end case;
146163
end Get_Bound_Of_Bounded_Type;
147164

148-
----------------------------
149-
-- Make_Range_Assert_Expr --
150-
----------------------------
165+
166+
function Make_Overflow_Assert_Expr (N : Node_Id; Value : Irep) return Irep
167+
is
168+
Value_Type : constant Irep :=
169+
Follow_Symbol_Type (Get_Type (Value), Global_Symbol_Table);
170+
Low_Value : constant Irep := Get_Bound (N, Value_Type, Bound_Low);
171+
High_Value : constant Irep := Get_Bound (N, Value_Type, Bound_High);
172+
Maybe_Casted_Value : constant Irep := Value;
173+
begin
174+
pragma Assert (Get_Type (Low_Value) = Get_Type (High_Value));
175+
176+
if Kind (Value) in Class_Binary_Expr
177+
then
178+
declare
179+
Cast_Lhs : constant Irep :=
180+
Typecast_If_Necessary (Get_Lhs (Value), Get_Type (Low_Value),
181+
Global_Symbol_Table);
182+
Cast_Rhs : constant Irep :=
183+
Typecast_If_Necessary (Get_Rhs (Value), Get_Type (Low_Value),
184+
Global_Symbol_Table);
185+
begin
186+
Set_Lhs (Maybe_Casted_Value, Cast_Lhs);
187+
Set_Rhs (Maybe_Casted_Value, Cast_Rhs);
188+
Set_Type (Maybe_Casted_Value, Get_Type (Low_Value));
189+
end;
190+
end if;
191+
192+
if Kind (Value) in Class_Unary_Expr
193+
then
194+
declare
195+
Cast_Op : constant Irep :=
196+
Typecast_If_Necessary (Get_Op0 (Value), Get_Type (Low_Value),
197+
Global_Symbol_Table);
198+
begin
199+
Set_Op0 (Maybe_Casted_Value, Cast_Op);
200+
Set_Type (Maybe_Casted_Value, Get_Type (Low_Value));
201+
end;
202+
end if;
203+
204+
return Make_Range_Assert_Expr (N => N,
205+
Value => Maybe_Casted_Value,
206+
Lower_Bound => Low_Value,
207+
Upper_Bound => High_Value,
208+
Expected_Return_Type => Value_Type,
209+
Check_Name => "__CPROVER_Ada_Overflow_Check");
210+
end Make_Overflow_Assert_Expr;
151211

152212
function Make_Range_Assert_Expr (N : Node_Id; Value : Irep;
153-
Bounds_Type : Irep)
213+
Lower_Bound : Irep; Upper_Bound : Irep;
214+
Expected_Return_Type : Irep;
215+
Check_Name : String)
154216
return Irep
155217
is
156218
Call_Args : constant Irep := Make_Argument_List;
157-
Actual_Type : constant Irep := Follow_Symbol_Type (Get_Type (Value),
158-
Global_Symbol_Table);
159-
Followed_Bound_Type : constant Irep := Follow_Symbol_Type (Bounds_Type,
160-
Global_Symbol_Table);
219+
Underlying_Lower_Type : constant Irep :=
220+
Follow_Symbol_Type (Get_Type (Lower_Bound), Global_Symbol_Table);
221+
Underlying_Upper_Type : constant Irep :=
222+
Follow_Symbol_Type (Get_Type (Upper_Bound), Global_Symbol_Table);
161223
Source_Loc : constant Irep := Get_Source_Location (N);
162224

163225
function Build_Assert_Function return Symbol;
@@ -169,38 +231,33 @@ package body Range_Check is
169231
-- Build a symbol for the following function
170232
-- Actual_Type range_check(Actual_Type value, Actual_Type lower_bound,
171233
-- Actual_Type upper_bound) {
172-
-- assert (value >= lower_bound && value <= upper_bound);
234+
-- `Check_Name` (value >= lower_bound && value <= upper_bound);
173235
-- return value;
174236
-- }
175237
function Build_Assert_Function return Symbol
176238
is
177239
Func_Name : constant String := Fresh_Var_Name ("range_check");
178240
Body_Block : constant Irep :=
179241
Make_Code_Block (Get_Source_Location (N));
180-
Description : constant Irep := Make_String_Constant_Expr (
181-
Source_Location => Source_Loc,
182-
I_Type => Ireps.Empty,
183-
Range_Check => False,
184-
Value => "Range Check");
185242
Func_Params : constant Irep := Make_Parameter_List;
186243
Value_Arg : constant Irep :=
187244
Create_Fun_Parameter (Fun_Name => Func_Name,
188245
Param_Name => "value",
189-
Param_Type => Actual_Type,
246+
Param_Type => Underlying_Lower_Type,
190247
Param_List => Func_Params,
191248
A_Symbol_Table => Global_Symbol_Table,
192249
Source_Location => Source_Loc);
193250
Lower_Bound_Arg : constant Irep :=
194251
Create_Fun_Parameter (Fun_Name => Func_Name,
195252
Param_Name => "low",
196-
Param_Type => Bounds_Type,
253+
Param_Type => Underlying_Lower_Type,
197254
Param_List => Func_Params,
198255
A_Symbol_Table => Global_Symbol_Table,
199256
Source_Location => Source_Loc);
200257
Upper_Bound_Arg : constant Irep :=
201258
Create_Fun_Parameter (Fun_Name => Func_Name,
202259
Param_Name => "high",
203-
Param_Type => Bounds_Type,
260+
Param_Type => Underlying_Upper_Type,
204261
Param_List => Func_Params,
205262
A_Symbol_Table => Global_Symbol_Table,
206263
Source_Location => Source_Loc);
@@ -209,49 +266,90 @@ package body Range_Check is
209266
-- Create_Fun_Parameter
210267
Parameters => Func_Params,
211268
Ellipsis => False,
212-
Return_Type => Actual_Type,
269+
Return_Type => Expected_Return_Type,
213270
Inlined => False,
214271
Knr => False);
215272
Value_Param : constant Irep := Param_Symbol (Value_Arg);
216273
Lower_Bound_Param : constant Irep := Param_Symbol (Lower_Bound_Arg);
217274
Upper_Bound_Param : constant Irep := Param_Symbol (Upper_Bound_Arg);
218275
--
219276
Return_Inst : constant Irep :=
220-
Make_Code_Return (Return_Value => Value_Param,
221-
Source_Location => Get_Source_Location (N),
277+
Make_Code_Return (Return_Value =>
278+
Typecast_If_Necessary (
279+
Value_Param, Expected_Return_Type,
280+
Global_Symbol_Table),
281+
Source_Location => Source_Loc,
222282
I_Type => Ireps.Empty);
283+
Range_Check_Args : constant Irep := Make_Argument_List;
284+
Range_Expr : constant Irep :=
285+
Make_Range_Expression (Value_Expr => Value_Param,
286+
Lower_Bound => Lower_Bound_Param,
287+
Upper_Bound => Upper_Bound_Param);
288+
Range_Expr_As_Int : constant Irep :=
289+
Typecast_If_Necessary (Expr => Range_Expr,
290+
New_Type => Int32_T,
291+
A_Symbol_Table => Global_Symbol_Table);
292+
Range_Check_Sym_Expr : constant Irep :=
293+
Symbol_Expr (Get_Ada_Check_Symbol (Check_Name,
294+
Global_Symbol_Table, Source_Loc));
295+
Range_Check_Call : constant Irep :=
296+
Make_Code_Function_Call (Arguments => Range_Check_Args,
297+
I_Function => Range_Check_Sym_Expr,
298+
Lhs => Make_Nil (Source_Loc),
299+
Source_Location => Source_Loc,
300+
I_Type => Make_Void_Type);
223301
begin
224-
Append_Op (Body_Block,
225-
Make_Assert_Call (Expression (N),
226-
Make_Range_Expression
227-
(Value_Param, Lower_Bound_Param, Upper_Bound_Param),
228-
Description));
302+
Append_Argument (Range_Check_Args, Range_Expr_As_Int);
303+
Append_Op (Body_Block, Range_Check_Call);
229304
Append_Op (Body_Block, Return_Inst);
230305

231-
return New_Function_Symbol_Entry (Name => Func_Name,
232-
Symbol_Type => Func_Type,
233-
Value => Body_Block,
234-
A_Symbol_Table => Global_Symbol_Table);
306+
return New_Function_Symbol_Entry
307+
(Name => Func_Name,
308+
Symbol_Type => Func_Type,
309+
Value => Body_Block,
310+
A_Symbol_Table => Global_Symbol_Table);
235311
end Build_Assert_Function;
236312

237-
Lower_Bound : constant Irep :=
238-
Get_Bound (N, Followed_Bound_Type, Bound_Low);
239-
Upper_Bound : constant Irep :=
240-
Get_Bound (N, Followed_Bound_Type, Bound_High);
241-
242-
Call_Inst : constant Irep := Make_Side_Effect_Expr_Function_Call (
243-
Arguments => Call_Args,
244-
I_Function => Symbol_Expr (Build_Assert_Function),
245-
Source_Location => Get_Source_Location (N),
246-
I_Type => Actual_Type);
313+
Call_Inst : constant Irep := Make_Side_Effect_Expr_Function_Call
314+
(Arguments => Call_Args,
315+
I_Function => Symbol_Expr (Build_Assert_Function),
316+
Source_Location => Get_Source_Location (N),
317+
I_Type => Expected_Return_Type);
247318
begin
248-
Append_Argument (Call_Args, Value);
319+
pragma Assert (Underlying_Lower_Type = Underlying_Upper_Type);
320+
321+
Append_Argument (Call_Args,
322+
Typecast_If_Necessary (Expr => Value,
323+
New_Type => Underlying_Lower_Type,
324+
A_Symbol_Table => Global_Symbol_Table));
325+
-- Value);
249326
Append_Argument (Call_Args, Lower_Bound);
250327
Append_Argument (Call_Args, Upper_Bound);
251328

252329
return Call_Inst;
253330
end Make_Range_Assert_Expr;
254331

332+
----------------------------
333+
-- Make_Range_Assert_Expr --
334+
----------------------------
335+
336+
function Make_Range_Assert_Expr (N : Node_Id; Value : Irep;
337+
Bounds_Type : Irep)
338+
return Irep
339+
is
340+
Followed_Bound_Type : constant Irep := Follow_Symbol_Type (Bounds_Type,
341+
Global_Symbol_Table);
342+
343+
begin
344+
return Make_Range_Assert_Expr (N => N,
345+
Value => Value,
346+
Lower_Bound => Get_Bound (N, Followed_Bound_Type, Bound_Low),
347+
Upper_Bound => Get_Bound (N, Followed_Bound_Type, Bound_High),
348+
Expected_Return_Type => Get_Type (Value),
349+
Check_Name => "__CPROVER_Ada_Range_Check");
350+
351+
end Make_Range_Assert_Expr;
352+
255353
-------------------------------
256354
-- Make_Range_Expression --
257355
-------------------------------
@@ -319,11 +417,13 @@ package body Range_Check is
319417
| I_Bounded_Signedbv_Type
320418
| I_Bounded_Floatbv_Type
321419
| I_Unsignedbv_Type
322-
| I_Signedbv_Type);
323-
324-
return R : constant Irep := Make_Op_And (
325-
Source_Location => Source_Location,
326-
I_Type => Make_Bool_Type) do
420+
| I_Signedbv_Type
421+
| I_Floatbv_Type
422+
| I_Ada_Mod_Type);
423+
return R : constant Irep := Make_Op_And
424+
(Source_Location => Source_Location,
425+
I_Type => Make_Bool_Type)
426+
do
327427
Append_Op (R, Op_Geq);
328428
Append_Op (R, Op_Leq);
329429
end return;
@@ -368,35 +468,4 @@ package body Range_Check is
368468
return Irep (Expr_Bounds_Table.Element (Index));
369469
end Load_Symbol_Bound;
370470

371-
----------------------
372-
-- Make_Assert_Call --
373-
----------------------
374-
375-
function Make_Assert_Call (N : Node_Id; Assertion : Irep;
376-
Description : Irep)
377-
return Irep is
378-
Assert_Args : constant Irep := Make_Argument_List;
379-
Sym_Assert : constant Irep := Make_Symbol_Expr (
380-
Source_Location => Get_Source_Location (N),
381-
I_Type => Make_Code_Type (
382-
Parameters => Make_Parameter_List,
383-
Ellipsis => False,
384-
Return_Type => Make_Void_Type,
385-
Inlined => False,
386-
Knr => False),
387-
Identifier => "__CPROVER_assert");
388-
SE_Call_Expr : constant Irep :=
389-
Make_Code_Function_Call (
390-
Arguments => Assert_Args,
391-
I_Function => Sym_Assert,
392-
Lhs => Make_Nil (Get_Source_Location (N)),
393-
Source_Location => Get_Source_Location (N),
394-
I_Type => Make_Void_Type);
395-
begin
396-
Append_Argument (Assert_Args, Assertion);
397-
Append_Argument (Assert_Args, Description);
398-
399-
return SE_Call_Expr;
400-
end Make_Assert_Call;
401-
402471
end Range_Check;

‎gnat2goto/driver/range_check.ads

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,8 @@ package Range_Check is
2323
return Irep
2424
with Pre => Kind (Bound_Type) in
2525
I_Bounded_Unsignedbv_Type | I_Bounded_Signedbv_Type
26-
| I_Bounded_Floatbv_Type | I_Unsignedbv_Type | I_Signedbv_Type,
27-
26+
| I_Bounded_Floatbv_Type | I_Unsignedbv_Type | I_Signedbv_Type
27+
| I_Floatbv_Type,
2828
Post => Kind (Get_Bound'Result) in Class_Expr;
2929

3030
function Get_Bound_Of_Bounded_Type (Bound_Type : Irep;
@@ -35,6 +35,13 @@ package Range_Check is
3535
| I_Bounded_Unsignedbv_Type,
3636
Post => Kind (Get_Bound_Of_Bounded_Type'Result) in Class_Expr;
3737

38+
function Make_Overflow_Assert_Expr (N : Node_Id; Value : Irep) return Irep;
39+
40+
function Make_Range_Assert_Expr (N : Node_Id; Value : Irep;
41+
Lower_Bound : Irep; Upper_Bound : Irep;
42+
Expected_Return_Type : Irep;
43+
Check_Name : String)
44+
return Irep;
3845
function Make_Range_Assert_Expr (N : Node_Id; Value : Irep;
3946
Bounds_Type : Irep) return Irep
4047
with Pre => Kind (Bounds_Type) in
@@ -82,10 +89,4 @@ private
8289
with Pre => Kind (Actual_Type) = I_Bounded_Floatbv_Type;
8390

8491
function Load_Symbol_Bound (Index : Integer) return Irep;
85-
86-
-- might be best if this is moved to a utility package in future
87-
-- atm placement documents it is only used by range_check
88-
function Make_Assert_Call (N : Node_Id; Assertion : Irep;
89-
Description : Irep) return Irep;
90-
9192
end Range_Check;

0 commit comments

Comments
 (0)