Improve widening hint generation (#338)

src/cwe_checker_lib/src/abstract_domain/data/conditional_specialization.rs

@@ -105,6 +105,14 @@ impl<T: SpecializeByConditional + RegisterDomain> SpecializeByConditional for Da
             Ok(result)
         }
     }
+
+    fn without_widening_hints(mut self) -> Self {
+        for offset in self.relative_values.values_mut() {
+            *offset = offset.clone().without_widening_hints();
+        }
+        self.absolute_value = self.absolute_value.map(|val| val.without_widening_hints());
+        self
+    }
 }
 
 #[cfg(test)]

src/cwe_checker_lib/src/abstract_domain/interval.rs

@@ -503,6 +503,13 @@ impl SpecializeByConditional for IntervalDomain {
 
         Ok(intersected_domain)
     }
+
+    fn without_widening_hints(mut self) -> Self {
+        self.widening_lower_bound = None;
+        self.widening_upper_bound = None;
+        self.widening_delay = 0;
+        self
+    }
 }
 
 impl AbstractDomain for IntervalDomain {

src/cwe_checker_lib/src/abstract_domain/mod.rs

@@ -166,4 +166,9 @@ pub trait SpecializeByConditional: Sized {
 
     /// Return the intersection of two values or an error if the intersection is empty.
     fn intersect(self, other: &Self) -> Result<Self, Error>;
+
+    /// Remove all widening hints from `self`.
+    /// Necessary for cases where several sources have widening hints,
+    /// but only one source should contribute widening hints to the result.
+    fn without_widening_hints(self) -> Self;
 }

src/cwe_checker_lib/src/analysis/pointer_inference/state/tests.rs

@@ -864,6 +864,52 @@ fn specialize_pointer_comparison() {
     assert_eq!(state.get_register(&register("RAX")), specialized_pointer);
 }
 
+/// Test that value specialization does not introduce unintended widening hints.
+/// This is a regression test for cases where pointer comparisons introduced two-sided bounds
+/// (resulting in two-sided widenings) instead of one-sided bounds.
+#[test]
+fn test_widening_hints_after_pointer_specialization() {
+    let mut state = State::new(&register("RSP"), Tid::new("func_tid"));
+    state.set_register(
+        &register("RAX"),
+        Data::from_target(new_id("func_tid", "RSP"), Bitvector::from_i64(10).into()),
+    );
+    state.set_register(
+        &register("RBX"),
+        Data::from_target(new_id("func_tid", "RSP"), Bitvector::from_i64(10).into()),
+    );
+    let expression = Expression::BinOp {
+        op: BinOpType::IntSub,
+        lhs: Box::new(Expression::Var(Variable::mock("RAX", 8))),
+        rhs: Box::new(Expression::Var(Variable::mock("RBX", 8))),
+    };
+    let neq_expression = Expression::BinOp {
+        op: BinOpType::IntNotEqual,
+        lhs: Box::new(Expression::Const(Bitvector::from_i64(5))),
+        rhs: Box::new(expression),
+    };
+    state
+        .specialize_by_expression_result(&neq_expression, Bitvector::from_i8(1).into())
+        .unwrap();
+    state
+        .specialize_by_expression_result(&neq_expression, Bitvector::from_i8(1).into())
+        .unwrap();
+
+    let offset_with_upper_bound: IntervalDomain = Bitvector::from_i64(10).into();
+    let offset_with_upper_bound = offset_with_upper_bound
+        .add_signed_less_equal_bound(&Bitvector::from_i64(14))
+        .unwrap();
+    let expected_val = Data::from_target(new_id("func_tid", "RSP"), offset_with_upper_bound);
+    assert_eq!(state.get_register(&Variable::mock("RAX", 8)), expected_val);
+
+    let offset_with_lower_bound: IntervalDomain = Bitvector::from_i64(10).into();
+    let offset_with_lower_bound = offset_with_lower_bound
+        .add_signed_greater_equal_bound(&Bitvector::from_i64(6))
+        .unwrap();
+    let expected_val = Data::from_target(new_id("func_tid", "RSP"), offset_with_lower_bound);
+    assert_eq!(state.get_register(&Variable::mock("RBX", 8)), expected_val);
+}
+
 #[test]
 fn test_check_def_for_null_dereferences() {
     let mut state = State::new(&register("RSP"), Tid::new("func_tid"));

src/cwe_checker_lib/src/analysis/pointer_inference/state/value_specialization.rs

@@ -92,19 +92,20 @@ impl State {
     ) -> Result<(), Error> {
         match op {
             BinOpType::IntAdd => {
-                let intermediate_result = result.clone() - self.eval(lhs);
+                let intermediate_result = result.clone() - self.eval(lhs).without_widening_hints();
                 self.specialize_by_expression_result(rhs, intermediate_result)?;
 
-                let intermediate_result = result - self.eval(rhs);
+                let intermediate_result = result - self.eval(rhs).without_widening_hints();
                 self.specialize_by_expression_result(lhs, intermediate_result)?;
 
                 return Ok(());
             }
             BinOpType::IntSub => {
-                let intermediate_result: Data = self.eval(lhs) - result.clone();
+                let intermediate_result: Data =
+                    self.eval(lhs).without_widening_hints() - result.clone();
                 self.specialize_by_expression_result(rhs, intermediate_result)?;
 
-                let intermediate_result = result + self.eval(rhs);
+                let intermediate_result = result + self.eval(rhs).without_widening_hints();
                 self.specialize_by_expression_result(lhs, intermediate_result)?;
 
                 return Ok(());
@@ -185,11 +186,17 @@ impl State {
                         (BinOpType::IntEqual, false) | (BinOpType::IntNotEqual, true) => {
                             // lhs != rhs
                             if let Ok(bitvec) = self.eval(lhs).try_to_bitvec() {
-                                let new_result = self.eval(rhs).add_not_equal_bound(&bitvec)?;
+                                let new_result = self
+                                    .eval(rhs)
+                                    .without_widening_hints()
+                                    .add_not_equal_bound(&bitvec)?;
                                 self.specialize_by_expression_result(rhs, new_result)?;
                             }
                             if let Ok(bitvec) = self.eval(rhs).try_to_bitvec() {
-                                let new_result = self.eval(lhs).add_not_equal_bound(&bitvec)?;
+                                let new_result = self
+                                    .eval(lhs)
+                                    .without_widening_hints()
+                                    .add_not_equal_bound(&bitvec)?;
                                 self.specialize_by_expression_result(lhs, new_result)?;
                             }
                             // Also specialize cases of pointer comparisons
@@ -251,7 +258,10 @@ impl State {
         lhs: &Expression,
         rhs: &Expression,
     ) -> Result<(), Error> {
-        let (lhs_pointer, rhs_pointer) = (self.eval(lhs), self.eval(rhs));
+        let (lhs_pointer, rhs_pointer) = (
+            self.eval(lhs).without_widening_hints(),
+            self.eval(rhs).without_widening_hints(),
+        );
         match (
             lhs_pointer.get_if_unique_target(),
             rhs_pointer.get_if_unique_target(),
@@ -308,11 +318,17 @@ impl State {
                         return Err(anyhow!("Unsatisfiable bound"));
                     }
                     lhs_bound += &Bitvector::one(lhs_bound.width());
-                    let new_result = self.eval(rhs).add_signed_greater_equal_bound(&lhs_bound)?;
+                    let new_result = self
+                        .eval(rhs)
+                        .without_widening_hints()
+                        .add_signed_greater_equal_bound(&lhs_bound)?;
                     self.specialize_by_expression_result(rhs, new_result)?;
                 }
                 IntSLessEqual => {
-                    let new_result = self.eval(rhs).add_signed_greater_equal_bound(&lhs_bound)?;
+                    let new_result = self
+                        .eval(rhs)
+                        .without_widening_hints()
+                        .add_signed_greater_equal_bound(&lhs_bound)?;
                     self.specialize_by_expression_result(rhs, new_result)?;
                 }
                 IntLess => {
@@ -322,12 +338,14 @@ impl State {
                     lhs_bound += &Bitvector::one(lhs_bound.width());
                     let new_result = self
                         .eval(rhs)
+                        .without_widening_hints()
                         .add_unsigned_greater_equal_bound(&lhs_bound)?;
                     self.specialize_by_expression_result(rhs, new_result)?;
                 }
                 IntLessEqual => {
                     let new_result = self
                         .eval(rhs)
+                        .without_widening_hints()
                         .add_unsigned_greater_equal_bound(&lhs_bound)?;
                     self.specialize_by_expression_result(rhs, new_result)?;
                 }
@@ -341,11 +359,17 @@ impl State {
                         return Err(anyhow!("Unsatisfiable bound"));
                     }
                     rhs_bound -= &Bitvector::one(rhs_bound.width());
-                    let new_result = self.eval(lhs).add_signed_less_equal_bound(&rhs_bound)?;
+                    let new_result = self
+                        .eval(lhs)
+                        .without_widening_hints()
+                        .add_signed_less_equal_bound(&rhs_bound)?;
                     self.specialize_by_expression_result(lhs, new_result)?;
                 }
                 IntSLessEqual => {
-                    let new_result = self.eval(lhs).add_signed_less_equal_bound(&rhs_bound)?;
+                    let new_result = self
+                        .eval(lhs)
+                        .without_widening_hints()
+                        .add_signed_less_equal_bound(&rhs_bound)?;
                     self.specialize_by_expression_result(lhs, new_result)?;
                 }
                 IntLess => {
@@ -353,11 +377,17 @@ impl State {
                         return Err(anyhow!("Unsatisfiable bound"));
                     }
                     rhs_bound -= &Bitvector::one(rhs_bound.width());
-                    let new_result = self.eval(lhs).add_unsigned_less_equal_bound(&rhs_bound)?;
+                    let new_result = self
+                        .eval(lhs)
+                        .without_widening_hints()
+                        .add_unsigned_less_equal_bound(&rhs_bound)?;
                     self.specialize_by_expression_result(lhs, new_result)?;
                 }
                 IntLessEqual => {
-                    let new_result = self.eval(lhs).add_unsigned_less_equal_bound(&rhs_bound)?;
+                    let new_result = self
+                        .eval(lhs)
+                        .without_widening_hints()
+                        .add_unsigned_less_equal_bound(&rhs_bound)?;
                     self.specialize_by_expression_result(lhs, new_result)?;
                 }
                 _ => panic!(),

src/cwe_checker_lib/src/intermediate_representation/expression/tests.rs

@@ -163,7 +163,7 @@ fn trivial_expression_substitution() {
             rhs: Box::new(setup.rcx_variable.clone()),
         }
     );
-
+    // Test `x < y || x == y` substitutes to `x <= y`
     let mut expr = Expression::BinOp {
         lhs: Box::new(Expression::BinOp {
             lhs: Box::new(setup.rax_variable.clone()),
@@ -186,6 +186,29 @@ fn trivial_expression_substitution() {
             rhs: Box::new(setup.rcx_variable.clone()),
         }
     );
+    // Test `x <= y && x != y` transforms to `x < y`
+    let mut expr = Expression::BinOp {
+        lhs: Box::new(Expression::BinOp {
+            lhs: Box::new(setup.rax_variable.clone()),
+            op: BinOpType::IntSLessEqual,
+            rhs: Box::new(setup.rcx_variable.clone()),
+        }),
+        op: BinOpType::BoolAnd,
+        rhs: Box::new(Expression::BinOp {
+            lhs: Box::new(setup.rcx_variable.clone()),
+            op: BinOpType::IntNotEqual,
+            rhs: Box::new(setup.rax_variable.clone()),
+        }),
+    };
+    expr.substitute_trivial_operations();
+    assert_eq!(
+        expr,
+        Expression::BinOp {
+            lhs: Box::new(setup.rax_variable.clone()),
+            op: BinOpType::IntSLess,
+            rhs: Box::new(setup.rcx_variable.clone()),
+        }
+    );
 
     let mut expr = Expression::Subpiece {
         low_byte: ByteSize::new(0),

src/cwe_checker_lib/src/intermediate_representation/expression/trivial_operation_substitution.rs

@@ -145,6 +145,78 @@ impl Expression {
                             rhs: less_right.clone(),
                         };
                     }
+                    (
+                        Expression::BinOp {
+                            lhs: lessequal_left,
+                            op: IntLessEqual,
+                            rhs: lessequal_right,
+                        },
+                        BoolAnd,
+                        Expression::BinOp {
+                            lhs: notequal_left,
+                            op: IntNotEqual,
+                            rhs: notequal_right,
+                        },
+                    )
+                    | (
+                        Expression::BinOp {
+                            lhs: notequal_left,
+                            op: IntNotEqual,
+                            rhs: notequal_right,
+                        },
+                        BoolAnd,
+                        Expression::BinOp {
+                            lhs: lessequal_left,
+                            op: IntLessEqual,
+                            rhs: lessequal_right,
+                        },
+                    ) if (lessequal_left == notequal_left && lessequal_right == notequal_right)
+                        || (lessequal_left == notequal_right
+                            && lessequal_right == notequal_left) =>
+                    {
+                        // `x <= y and x != y` is equivalent to `x < y `
+                        *self = Expression::BinOp {
+                            lhs: lessequal_left.clone(),
+                            op: IntLess,
+                            rhs: lessequal_right.clone(),
+                        };
+                    }
+                    (
+                        Expression::BinOp {
+                            lhs: lessequal_left,
+                            op: IntSLessEqual,
+                            rhs: lessequal_right,
+                        },
+                        BoolAnd,
+                        Expression::BinOp {
+                            lhs: notequal_left,
+                            op: IntNotEqual,
+                            rhs: notequal_right,
+                        },
+                    )
+                    | (
+                        Expression::BinOp {
+                            lhs: notequal_left,
+                            op: IntNotEqual,
+                            rhs: notequal_right,
+                        },
+                        BoolAnd,
+                        Expression::BinOp {
+                            lhs: lessequal_left,
+                            op: IntSLessEqual,
+                            rhs: lessequal_right,
+                        },
+                    ) if (lessequal_left == notequal_left && lessequal_right == notequal_right)
+                        || (lessequal_left == notequal_right
+                            && lessequal_right == notequal_left) =>
+                    {
+                        // `x <= y and x != y` is equivalent to `x < y `
+                        *self = Expression::BinOp {
+                            lhs: lessequal_left.clone(),
+                            op: IntSLess,
+                            rhs: lessequal_right.clone(),
+                        };
+                    }
                     _ => (),
                 }
             }