diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 80572a3b14..9352635dc5 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -223,7 +223,21 @@ struct | Bot -> Bot | _ -> VD.top () - let binop_ID (result_ik: Cil.ikind) = function + let binop_ID (result_ik: Cil.ikind) = + (* Check the shift amount for negative values (undefined behavior in C), emitting + appropriate warnings/errors based on bounds analysis. *) + let check_shift_neg dir y = + match ID.minimal y, ID.maximal y with + | Some min_y, _ when Z.geq min_y Z.zero -> + Checks.safe Checks.Category.InvalidShift + | _, Some max_y when Z.lt max_y Z.zero -> + M.error ~category:M.Category.Behavior.Undefined.other ~tags:[CWE 758] "Shift-%s by negative amount is undefined behavior" dir; + Checks.error Checks.Category.InvalidShift "Shift-%s by negative amount is undefined behavior" dir + | _ -> + M.warn ~category:M.Category.Behavior.Undefined.other ~tags:[CWE 758] "Shift-%s by possibly negative amount may be undefined behavior" dir; + Checks.warn Checks.Category.InvalidShift "Shift-%s by possibly negative amount may be undefined behavior" dir + in + function | PlusA -> ID.add | MinusA -> ID.sub | Mult -> ID.mul @@ -265,8 +279,14 @@ struct | BAnd -> ID.logand | BOr -> ID.logor | BXor -> ID.logxor - | Shiftlt -> ID.shift_left - | Shiftrt -> ID.shift_right + | Shiftlt -> + fun x y -> + check_shift_neg "left" y; + ID.shift_left x y + | Shiftrt -> + fun x y -> + check_shift_neg "right" y; + ID.shift_right x y | LAnd -> id_binary_log (&&) ~annihilator:false result_ik | LOr -> id_binary_log (||) ~annihilator:true result_ik | b -> (fun x y -> (ID.top_of result_ik)) diff --git a/tests/regression/98-bitwise-operations/09-shift-neg.c b/tests/regression/98-bitwise-operations/09-shift-neg.c new file mode 100644 index 0000000000..797f374162 --- /dev/null +++ b/tests/regression/98-bitwise-operations/09-shift-neg.c @@ -0,0 +1,37 @@ +// PARAM: --enable ana.int.interval +#include + +int main() { + int res; + int top; + int neg; + + // Definitely negative shift amount: error + res = 8 << -2; //WARN + + // Definitely negative shift amount in right shift: error + res = 8 >> -1; //WARN + + // Non-negative shift amount: no warning + res = 8 << 2; //NOWARN + res = 8 >> 2; //NOWARN + + // Zero shift amount: no warning + res = 8 << 0; //NOWARN + res = 8 >> 0; //NOWARN + + // Possibly negative shift amount: warn + // (top is uninitialized, representing a non-deterministic value — a common convention in goblint tests) + if (top) { neg = -1; } else { neg = 1; } + res = 8 << neg; //WARN + res = 8 >> neg; //WARN + + // Provably non-negative, bounded interval: no warning + // (pos_shift is [0,5] — non-negative and within valid shift range) + int pos_shift = 0; + if (top) { pos_shift = 5; } + res = 8 << pos_shift; //NOWARN + res = 8 >> pos_shift; //NOWARN + + return 0; +}