Commit 77e14a4e authored by David Bühler's avatar David Bühler
Browse files

[rte] Rewrites the emission of downcast alarms into one function.

parent b2b8be59
......@@ -357,88 +357,38 @@ let shift_overflow_assertion ~signed ~remove_trivial ~on_alarm (exp, op, lexp, r
end
else overflow_alarm ()
(* assertion for downcasting an integer to an unsigned integer type
without requiring modification of value to reach target domain
(well-defined behavior though) *)
let unsigned_downcast_assertion ~remove_trivial ~on_alarm (ty, exp) =
let e_typ = Cil.unrollType (Cil.typeOf exp) in
match e_typ with
| TInt (kind,_) ->
let szTo = Cil.bitsSizeOfBitfield ty in
let szFrom = Cil.bitsSizeOf e_typ in
(if szTo < szFrom || Cil.isSigned kind then
(* case signed to unsigned:
requires signed to be >= 0 and also <= max of unsigned size *)
(* cast unsigned to unsigned:
ok is same bit size ;
if target is <, requires <= max target *)
let max_ty = Cil.max_unsigned_number szTo in
let alarm ?(invalid=false) bk =
let b = match bk with
| Lower_bound -> Integer.zero
| Upper_bound -> max_ty
in
let a = Alarms.Overflow (Alarms.Unsigned_downcast, exp, b, bk) in
on_alarm ~invalid a;
in
let alarms () =
if Cil.isSigned kind then begin (* signed to unsigned *)
alarm Upper_bound;
alarm Lower_bound;
end else (* unsigned to unsigned; cannot overflow in the negative *)
alarm Upper_bound;
in
if remove_trivial then begin
match get_expr_val exp with
| None -> alarms ()
| Some a64 ->
if Integer.lt a64 Integer.zero then
alarm ~invalid:true Lower_bound
else if Integer.gt a64 max_ty then
alarm ~invalid:true Upper_bound
end
else alarms ())
| _ -> ()
(* assertion for downcasting an integer to a signed integer type
which can raise an implementation defined behavior *)
let signed_downcast_assertion ~remove_trivial ~on_alarm (ty, exp) =
let e_typ = Cil.unrollType (Cil.typeOf exp) in
match e_typ with
| TInt (kind,_) ->
(let szTo = Cil.bitsSizeOfBitfield ty in
let szFrom = Cil.bitsSizeOf e_typ in
if szTo < szFrom || (szTo == szFrom && not (Cil.isSigned kind)) then
(* downcast: the expression result should fit on szTo bits *)
let min_ty = Cil.min_signed_number szTo in
let max_ty = Cil.max_signed_number szTo in
let alarm ?(invalid=false) bk =
let b = match bk with
| Lower_bound -> min_ty
| Upper_bound -> max_ty
in
let a = Alarms.Overflow (Alarms.Signed_downcast, exp, b, bk) in
on_alarm ~invalid a;
in
let alarms () =
if Cil.isSigned kind then begin
(* signed to signed *)
alarm Upper_bound;
alarm Lower_bound
end else (* (unsigned to signed; cannot overflow in the negative *)
alarm Upper_bound
in
if remove_trivial then begin
match get_expr_val exp with
| None -> alarms ()
| Some a64 ->
(if Integer.lt a64 min_ty then
alarm ~invalid:true Lower_bound
else if Integer.gt a64 max_ty then
alarm ~invalid:true Upper_bound)
end
else alarms ())
| _ -> ()
(* Assertion for downcasts. *)
let downcast_assertion ~remove_trivial ~on_alarm (dst_type, exp) =
let src_type = Cil.typeOf exp in
let src_signed = Cil.isSignedInteger src_type in
let dst_signed = Cil.isSignedInteger dst_type in
let src_size = Cil.bitsSizeOf src_type in
let dst_size = Cil.bitsSizeOfBitfield dst_type in
if dst_size < src_size || dst_size == src_size && dst_signed <> src_signed
then
let dst_min, dst_max =
if dst_signed
then Cil.min_signed_number dst_size, Cil.max_signed_number dst_size
else Integer.zero, Cil.max_unsigned_number dst_size
in
let overflow_kind =
if dst_signed then Alarms.Signed_downcast else Alarms.Unsigned_downcast
in
let alarm ?(invalid=false) bound bound_kind =
let a = Alarms.Overflow (overflow_kind, exp, bound, bound_kind) in
on_alarm ~invalid a;
in
let alarms () =
alarm dst_max Upper_bound;
(* unsigned values cannot overflow in the negative *)
if src_signed then alarm dst_min Lower_bound;
in
match remove_trivial, get_expr_val exp with
| true, Some a64 ->
let invalid = true in
if Integer.lt a64 dst_min then alarm ~invalid dst_min Lower_bound
else if Integer.gt a64 dst_max then alarm ~invalid dst_max Upper_bound
| _ -> alarms ()
(* assertion for casting a floating-point value to an integer *)
let float_to_int_assertion ~remove_trivial ~on_alarm (ty, exp) =
......
......@@ -40,8 +40,7 @@ val shift_negative_assertion: exp alarm_gen
val shift_overflow_assertion: signed:bool -> (exp * binop * exp * exp) alarm_gen
val mult_sub_add_assertion: signed:bool -> (exp * binop * exp * exp) alarm_gen
val uminus_assertion: exp alarm_gen
val signed_downcast_assertion: (typ * exp) alarm_gen
val unsigned_downcast_assertion: (typ * exp) alarm_gen
val downcast_assertion: (typ * exp) alarm_gen
val float_to_int_assertion: (typ * exp) alarm_gen
val finite_float_assertion: (fkind * exp) alarm_gen
val pointer_call: (exp * exp list) alarm_gen
......
......@@ -308,14 +308,12 @@ class annot_visitor kf flags on_alarm = object (self)
(match Cil.unrollType ty, Cil.unrollType (Cil.typeOf e) with
(* to , from *)
| TInt(kind,_), TInt (_, _) ->
if Cil.isSigned kind then begin
if self#do_signed_downcast () then begin
self#generate_assertion Rte.signed_downcast_assertion (ty, e);
self#mark_to_skip e;
end
end
else if self#do_unsigned_downcast () then
self#generate_assertion Rte.unsigned_downcast_assertion (ty, e)
let signed = Cil.isSigned kind in
if signed && self#do_signed_downcast ()
|| not signed && self#do_unsigned_downcast ()
then self#generate_assertion Rte.downcast_assertion (ty, e);
if signed && self#do_signed_downcast ()
then self#mark_to_skip e;
| TInt _, TFloat _ ->
if self#do_float_to_int () then
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment