Skip to content

Commit

Permalink
fixes type unification on binary operation application (#1486)
Browse files Browse the repository at this point in the history
In #1422 the preconditions of Bil.Apply.binop were relaxed to allow
operands of different types. This introduced a subtle bug wrt the
shifting operations, in particular when the shift right-hand side
operand was larger then the left-hand one, the latter was extended and
the resulting type and value was incorrect.
  • Loading branch information
ivg authored May 5, 2022
1 parent 286b5f7 commit 56e984c
Showing 1 changed file with 22 additions and 19 deletions.
41 changes: 22 additions & 19 deletions lib/bap_types/bap_helpers.ml
Original file line number Diff line number Diff line change
Expand Up @@ -127,29 +127,32 @@ module Apply = struct

let binop op u v =
let open Word in
let hi = Int.(max (bitwidth u) (bitwidth v) - 1) in
let u = extract_exn ~hi u
and v = extract_exn ~hi v in
match op with
| PLUS -> u + v
| MINUS -> u - v
| TIMES -> u * v
| DIVIDE -> u / v
| SDIVIDE -> signed u / signed v
| MOD -> u mod v
| SMOD -> signed u mod signed v
| LSHIFT -> u lsl v
| RSHIFT -> u lsr v
| ARSHIFT -> u asr v
| AND -> u land v
| OR -> u lor v
| XOR -> u lxor v
| EQ -> Bitvector.(of_bool (u = v))
| NEQ -> Bitvector.(of_bool (u <> v))
| LT -> Bitvector.(of_bool (u < v))
| LE -> Bitvector.(of_bool (u <= v))
| SLT -> Bitvector.(of_bool (signed u < signed v))
| SLE -> Bitvector.(of_bool (signed u <= signed v))
| _ ->
let hi = Int.(max (bitwidth u) (bitwidth v) - 1) in
let u = extract_exn ~hi u
and v = extract_exn ~hi v in
match op with
| PLUS -> u + v
| MINUS -> u - v
| TIMES -> u * v
| DIVIDE -> u / v
| SDIVIDE -> signed u / signed v
| MOD -> u mod v
| SMOD -> signed u mod signed v
| AND -> u land v
| OR -> u lor v
| XOR -> u lxor v
| EQ -> Bitvector.(of_bool (u = v))
| NEQ -> Bitvector.(of_bool (u <> v))
| LT -> Bitvector.(of_bool (u < v))
| LE -> Bitvector.(of_bool (u <= v))
| SLT -> Bitvector.(of_bool (signed u < signed v))
| SLE -> Bitvector.(of_bool (signed u <= signed v))
| (LSHIFT|RSHIFT|ARSHIFT) -> assert false

let cast ct sz u =
let ext = Bitvector.extract_exn in
Expand Down

0 comments on commit 56e984c

Please sign in to comment.