relaxes the Apply.binop function to allow not well-typed operations (#1422)

We are not changing the typing rules of BIL or Core Theory, but
providing a well-defined behavior for application of binary operations
on bitvectors with unequal lengths. Before that, the behavior was
undefined and the precondition of the function was clearly specifying
that the inputs should be of equal lengths.

The new behavior is to promote words to the equal length, (much like
in C, which implicitly coerces the narrow type to the wider type).

The motivation is simple. It is hard to ensure this precondition in
general. Yes, our lifters produce well-typed code, so there are no
issues when we interpret code from the lifters. But we also have a lot
of different interpreters, extensible via primitives. And those
interpreters sometimes don't have any means (or at least efficient
means) to ensure that all binary operations have matching widths. A
concrete example of such interpreter is Veri that is used for
bi-interpretation of traces and BIL programs for
verification. Sometimes, the tracers organically produce ill-typed
code, as they rely on their own typing rules. For example, qemu-based
tracer just represent every register (including flags) and every
number (including bools) with a word-sized bitvector. We still want to
be able to perform calculations on such inputs and, to be honest, the
results are quite well-defined, no hacks required. In other words,
this change tries to follow the robustness principle, i.e., "be
conservative in what you do, be liberal in what you accept from
others". Our lifters, i.e., the code that we produce, are still much
conservative, but our interpreters tend to be more liberal and
understand even the ill-typed code, especially if this code has clear
semantics.

Author: ivg

lib/bap/bap.mli

@@ -2444,20 +2444,27 @@ module Std : sig
     *)
     module Apply : sig
 
-      (** [binop op x y] applies the binary operation [op] to [x] and
-          [y].
-          precondition: the expression [BinOp(op,Int x,Int y)] shall be well-typed.*)
+      (** [binop op x y] applies [op] to [x] and [y].
+
+          @before 2.5.0 precondition: the expression [BinOp(op,Intx,Int y)]
+          shall be well-typed.
+
+          @after 2.5.0 if [x] and [y] have different widths then they
+          are extended to the same width, which is the width of the
+          largest operand. If an operator is signed, then it will be
+          correctly sign-extended.
+      *)
       val binop : binop -> word -> word -> word
 
-      (** [unop op x] applies the unary operation [op] to [x].
-          precondition: the expression [Unop(op,Int x)] shall be
-          well-typed.     *)
+      (** [unop op x] applies the unary operation [op] to [x]. *)
       val unop : unop -> word -> word
 
       (** [cast t s x] casts [x] using the cast type [t] to the given
           size [s].
+
           precondition: the expression [Cast(t,s,Int x)] shall be
-          well-typed.  *)
+          well-typed.
+      *)
       val cast : cast -> int -> word -> word
     end
 

lib/bap_types/bap_helpers.ml

@@ -127,11 +127,9 @@ module Apply = struct
 
   let binop op u v =
     let open Word in
-    if Int.(bitwidth u <> bitwidth v) && not (is_shift op)
-    then failwithf "binop type error - %s %s %s"
-        (to_string u)
-        (Bap_exp.Binop.string_of_binop op)
-        (to_string 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