From 2f5ed3e5549afe29e8985cb8c7b0a10dad124c5e Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 31 Oct 2018 11:16:13 -0700 Subject: [PATCH] [sledge] Clamp result of binary Z ops to bitwidth Summary: Previously only the arguments of binary operations on integers were clamped to the given bitwidth, but the results could overflow. This was incorrect. Also, use a clamped version of equality to simplify equality expressions. This was previously overlooked. Reviewed By: mbouaziz Differential Revision: D12854502 fbshipit-source-id: 8786b4217 --- sledge/src/llair/exp.ml | 49 ++++++++++++++++++++--------------- sledge/src/llair/exp_test.ml | 50 ++++++++++++++++++++++++++++++++++++ 2 files changed, 78 insertions(+), 21 deletions(-) create mode 100644 sledge/src/llair/exp_test.ml diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index 7dbc0fb58..13179fbd1 100644 --- a/sledge/src/llair/exp.ml +++ b/sledge/src/llair/exp.ml @@ -30,28 +30,33 @@ module Z = struct let clamp ~signed bits z = if signed then Z.signed_extract z 0 bits else Z.extract z 0 bits - let clamp_binop ~signed bits op x y = + let clamp_cmp ~signed bits op x y = op (clamp ~signed bits x) (clamp ~signed bits y) - let leq ~bits x y = clamp_binop ~signed:true bits Z.leq x y - let geq ~bits x y = clamp_binop ~signed:true bits Z.geq x y - let lt ~bits x y = clamp_binop ~signed:true bits Z.lt x y - let gt ~bits x y = clamp_binop ~signed:true bits Z.gt x y - let uleq ~bits x y = clamp_binop ~signed:false bits Z.leq x y - let ugeq ~bits x y = clamp_binop ~signed:false bits Z.geq x y - let ult ~bits x y = clamp_binop ~signed:false bits Z.lt x y - let ugt ~bits x y = clamp_binop ~signed:false bits Z.gt x y let neg ~bits z = Z.neg (clamp bits ~signed:true z) - let add ~bits x y = clamp_binop ~signed:true bits Z.add x y - let sub ~bits x y = clamp_binop ~signed:true bits Z.sub x y - let mul ~bits x y = clamp_binop ~signed:true bits Z.mul x y - let div ~bits x y = clamp_binop ~signed:true bits Z.div x y - let rem ~bits x y = clamp_binop ~signed:true bits Z.rem x y - let udiv ~bits x y = clamp_binop ~signed:false bits Z.div x y - let urem ~bits x y = clamp_binop ~signed:false bits Z.rem x y - let logand ~bits x y = clamp_binop ~signed:true bits Z.logand x y - let logor ~bits x y = clamp_binop ~signed:true bits Z.logor x y - let logxor ~bits x y = clamp_binop ~signed:true bits Z.logxor x y + + let clamp_bop ~signed bits op x y = + clamp ~signed bits (op (clamp ~signed bits x) (clamp ~signed bits y)) + + let eq ~bits x y = clamp_cmp ~signed:true bits Z.equal x y + let leq ~bits x y = clamp_cmp ~signed:true bits Z.leq x y + let geq ~bits x y = clamp_cmp ~signed:true bits Z.geq x y + let lt ~bits x y = clamp_cmp ~signed:true bits Z.lt x y + let gt ~bits x y = clamp_cmp ~signed:true bits Z.gt x y + let uleq ~bits x y = clamp_cmp ~signed:false bits Z.leq x y + let ugeq ~bits x y = clamp_cmp ~signed:false bits Z.geq x y + let ult ~bits x y = clamp_cmp ~signed:false bits Z.lt x y + let ugt ~bits x y = clamp_cmp ~signed:false bits Z.gt x y + let add ~bits x y = clamp_bop ~signed:true bits Z.add x y + let sub ~bits x y = clamp_bop ~signed:true bits Z.sub x y + let mul ~bits x y = clamp_bop ~signed:true bits Z.mul x y + let div ~bits x y = clamp_bop ~signed:true bits Z.div x y + let rem ~bits x y = clamp_bop ~signed:true bits Z.rem x y + let udiv ~bits x y = clamp_bop ~signed:false bits Z.div x y + let urem ~bits x y = clamp_bop ~signed:false bits Z.rem x y + let logand ~bits x y = clamp_bop ~signed:true bits Z.logand x y + let logor ~bits x y = clamp_bop ~signed:true bits Z.logor x y + let logxor ~bits x y = clamp_bop ~signed:true bits Z.logxor x y let shift_left ~bits z i = Z.shift_left (clamp bits ~signed:true z) i let shift_right ~bits z i = Z.shift_right (clamp bits ~signed:true z) i @@ -552,7 +557,8 @@ let rec simp_not (typ : Typ.t) exp = and simp_eq x y = match (x, y) with (* i = j *) - | Integer {data= i}, Integer {data= j} -> bool (Z.equal i j) + | Integer {data= i; typ= Integer {bits}}, Integer {data= j} -> + bool (Z.eq ~bits i j) (* e+i = j ==> e = j-i *) | ( App {op= App {op= Add; arg= e}; arg= Integer {data= i}} , Integer {data= j; typ= Integer {bits} as typ} ) -> @@ -577,7 +583,8 @@ and simp_eq x y = and simp_dq x y = match (x, y) with (* i != j *) - | Integer {data= i}, Integer {data= j} -> bool (not (Z.equal i j)) + | Integer {data= i; typ= Integer {bits}}, Integer {data= j} -> + bool (not (Z.eq ~bits i j)) (* e+i != j ==> e != j-i *) | ( App {op= App {op= Add; arg= e}; arg= Integer {data= i}} , Integer {data= j; typ= Integer {bits} as typ} ) -> diff --git a/sledge/src/llair/exp_test.ml b/sledge/src/llair/exp_test.ml new file mode 100644 index 000000000..671d6aff7 --- /dev/null +++ b/sledge/src/llair/exp_test.ml @@ -0,0 +1,50 @@ +(* + * Copyright (c) 2018-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +let%test_module _ = + ( module struct + let pf = Format.printf "%t%a@." (fun _ -> Trace.flush ()) Exp.pp + let char = Typ.integer ~bits:8 + let ( ! ) i = Exp.integer (Z.of_int i) char + let ( + ) = Exp.add + let ( && ) = Exp.and_ + let ( || ) = Exp.or_ + + let%test "booleans distinct" = + Exp.is_false + (Exp.eq + (Exp.integer Z.minus_one Typ.bool) + (Exp.integer Z.zero Typ.bool)) + + let%test "unsigned booleans distinct" = + Exp.is_false + (Exp.eq (Exp.integer Z.one Typ.bool) (Exp.integer Z.zero Typ.bool)) + + let%test "boolean overflow" = + Exp.is_true + (Exp.eq + (Exp.integer Z.minus_one Typ.bool) + (Exp.integer Z.one Typ.bool)) + + let%test "unsigned boolean overflow" = + Exp.is_true + (Exp.uge + (Exp.integer Z.minus_one Typ.bool) + (Exp.integer Z.one Typ.bool)) + + let%expect_test _ = + pf (!42 + !13) ; + [%expect {| 55 |}] + + let%expect_test _ = + pf (!(-128) && !127) ; + [%expect {| 0 |}] + + let%expect_test _ = + pf (!(-128) || !127) ; + [%expect {| -1 |}] + end )