From 51eb521f55e6e50c1fa60c84d9744af7a4babe22 Mon Sep 17 00:00:00 2001 From: Jay Lee Date: Fri, 17 Nov 2023 23:23:26 +0900 Subject: [PATCH 1/2] Treat numeric transmute specially Fixes issues with integer binary operations with floating point numbers transmuted to integers. Fixes https://github.com/facebookexperimental/MIRAI/issues/1252#issue-1999028242 --- checker/src/z3_solver.rs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/checker/src/z3_solver.rs b/checker/src/z3_solver.rs index b681985f..e3c8ad46 100644 --- a/checker/src/z3_solver.rs +++ b/checker/src/z3_solver.rs @@ -1139,8 +1139,12 @@ impl Z3Solver { Expression::TaggedExpression { operand, .. } => { self.get_as_numeric_z3_ast(&operand.expression) } - Expression::Transmute { operand, .. } => { - self.get_as_numeric_z3_ast(&operand.expression) + Expression::Transmute { operand, target_type } => { + if target_type.is_integer() || target_type.is_floating_point_number() { + self.numeric_cast(&operand.expression, *target_type) + } else { + self.get_as_numeric_z3_ast(&operand.expression) + } } Expression::Top | Expression::Bottom => unsafe { ( From e49cedd8928cb5003e1c944f9597121174137c39 Mon Sep 17 00:00:00 2001 From: Jay Lee Date: Sat, 18 Nov 2023 17:47:14 +0900 Subject: [PATCH 2/2] Fix the return type of `bv_overflows` to be of sort BitVector Resolves https://github.com/facebookexperimental/MIRAI/issues/1252#issue-1999028242 --- checker/src/z3_solver.rs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/checker/src/z3_solver.rs b/checker/src/z3_solver.rs index e3c8ad46..0a8be055 100644 --- a/checker/src/z3_solver.rs +++ b/checker/src/z3_solver.rs @@ -1952,14 +1952,17 @@ impl Z3Solver { let right_bv = self.get_as_bv_z3_ast(&right.expression, num_bits); unsafe { let does_not_overflow = no_overflow(self.z3_context, left_bv, right_bv, is_signed); - if is_signed { + let overflows = if is_signed { let does_not_underflow = no_underflow(self.z3_context, left_bv, right_bv); let tmp = vec![does_not_overflow, does_not_underflow]; let stays_in_range = z3_sys::Z3_mk_and(self.z3_context, 2, tmp.as_ptr()); z3_sys::Z3_mk_not(self.z3_context, stays_in_range) } else { z3_sys::Z3_mk_not(self.z3_context, does_not_overflow) - } + }; + let bv_true = self.bv_constant(num_bits, &ConstantDomain::True); + let bv_false = self.bv_constant(num_bits, &ConstantDomain::False); + z3_sys::Z3_mk_ite(self.z3_context, overflows, bv_true, bv_false) } }