Expression propagation (#185)

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

@@ -395,97 +395,28 @@ fn specialize_conditional() {
     let mut state = State::new(&register("RSP"), Tid::new("func"));
     state.set_register(&register("RAX"), IntervalDomain::mock(-10, 20).into());
 
-    let condition = Expression::Var(Variable::mock("FLAG", 1));
-
-    // A complicated way of computing the result of `RAX <= 0`
-    // and assigning the result to the `FLAG` register.
-    let defs = vec![
-        Def::assign("def1", register("RAX"), Expression::Var(register("RAX"))),
-        Def::assign(
-            "def_that_should_be_ignored",
-            Variable::mock("FLAG", 1),
-            Expression::Const(Bitvector::from_u8(42)),
-        ),
-        Def::assign(
-            "def2",
-            Variable::mock("FLAG_SLESS", 1),
-            Expression::BinOp {
+    let condition = Expression::BinOp {
         lhs: Box::new(Expression::Var(register("RAX"))),
-                op: BinOpType::IntSLess,
-                rhs: Box::new(Expression::Const(Bitvector::from_u64(0))),
-            },
-        ),
-        Def::assign(
-            "def3",
-            Variable::mock("FLAG_EQUAL", 1),
-            Expression::BinOp {
-                lhs: Box::new(Expression::Var(register("RAX"))),
-                op: BinOpType::IntEqual,
-                rhs: Box::new(Expression::Const(Bitvector::from_u64(0))),
-            },
-        ),
-        Def::assign(
-            "def4",
-            Variable::mock("FLAG_NOTEQUAL", 1),
-            Expression::BinOp {
-                lhs: Box::new(Expression::Var(Variable::mock("FLAG_SLESS", 1))),
-                op: BinOpType::IntNotEqual,
-                rhs: Box::new(Expression::Const(Bitvector::from_u8(0))),
-            },
-        ),
-        Def::assign(
-            "def5",
-            Variable::mock("FLAG", 1),
-            Expression::BinOp {
-                lhs: Box::new(Expression::Var(Variable::mock("FLAG_EQUAL", 1))),
-                op: BinOpType::BoolOr,
-                rhs: Box::new(Expression::Var(Variable::mock("FLAG_NOTEQUAL", 1))),
-            },
-        ),
-    ];
-
-    let block = Term {
-        tid: Tid::new("block"),
-        term: Blk {
-            defs,
-            jmps: Vec::new(),
-            indirect_jmp_targets: Vec::new(),
-        },
+        op: BinOpType::IntSLessEqual,
+        rhs: Box::new(Expression::Const(Bitvector::zero(ByteSize::new(8).into()))),
     };
+    let block = Blk::mock();
 
     let result = context
         .specialize_conditional(&state, &condition, &block, false)
         .unwrap();
     assert_eq!(
-        result.get_register(&Variable::mock("FLAG", 1)),
-        Bitvector::from_u8(0).into()
-    );
-    assert_eq!(
-        result.get_register(&Variable::mock("FLAG_NOTEQUAL", 1)),
-        Bitvector::from_u8(0).into()
-    );
-    assert_eq!(
-        result.get_register(&Variable::mock("FLAG_EQUAL", 1)),
-        Bitvector::from_u8(0).into()
-    );
-    assert_eq!(
-        result.get_register(&Variable::mock("FLAG_SLESS", 1)),
-        Bitvector::from_u8(0).into()
-    );
-    // The result is technically false, since RAX == 0 should be excluded.
-    // This impreciseness is due to the way that the result is calculated.
-    assert_eq!(
         result.get_register(&register("RAX")),
-        IntervalDomain::mock(0, 20).into()
+        IntervalDomain::mock(1, 20).into()
     );
 
     state.set_register(&register("RAX"), IntervalDomain::mock(0, 20).into());
     let result = context
-        .specialize_conditional(&state, &condition, &block, false)
+        .specialize_conditional(&state, &condition, &block, true)
         .unwrap();
     assert_eq!(
         result.get_register(&register("RAX")),
-        IntervalDomain::mock_with_bounds(Some(0), 1, 20, None).into()
+        IntervalDomain::mock_with_bounds(None, 0, 0, None).into()
     );
 
     state.set_register(&register("RAX"), IntervalDomain::mock(-20, 0).into());

src/cwe_checker_lib/src/analysis/pointer_inference/context/trait_impls.rs

 use super::*;
-use std::collections::HashSet;
 
 impl<'a> crate::analysis::forward_interprocedural_fixpoint::Context<'a> for Context<'a> {
     type Value = State;
@@ -346,12 +345,12 @@ impl<'a> crate::analysis::forward_interprocedural_fixpoint::Context<'a> for Cont
     /// Update the state with the knowledge that some conditional evaluated to true or false.
     fn specialize_conditional(
         &self,
-        value: &State,
+        state: &State,
         condition: &Expression,
-        block_before_condition: &Term<Blk>,
+        _block_before_condition: &Term<Blk>,
         is_true: bool,
     ) -> Option<State> {
-        let mut specialized_state = value.clone();
+        let mut specialized_state = state.clone();
         if specialized_state
             .specialize_by_expression_result(condition, Bitvector::from_u8(is_true as u8).into())
             .is_err()
@@ -359,40 +358,6 @@ impl<'a> crate::analysis::forward_interprocedural_fixpoint::Context<'a> for Cont
             // State is unsatisfiable
             return None;
         }
-        let mut modified_vars: HashSet<Variable> = HashSet::new();
-        for def in block_before_condition.term.defs.iter().rev() {
-            match &def.term {
-                Def::Store { .. } => (),
-                Def::Load { var, .. } => {
-                    modified_vars.insert(var.clone());
-                }
-                Def::Assign {
-                    var,
-                    value: input_expr,
-                } => {
-                    if !modified_vars.contains(var) {
-                        // Register is not modified again between the `Def` and the end of the block.
-                        modified_vars.insert(var.clone());
-                        if input_expr
-                            .input_vars()
-                            .into_iter()
-                            .find(|input_var| modified_vars.contains(input_var))
-                            .is_none()
-                        {
-                            // Values of input registers did not change between the `Def` and the end of the block.
-                            let expr_result = specialized_state.get_register(var);
-                            if specialized_state
-                                .specialize_by_expression_result(input_expr, expr_result.clone())
-                                .is_err()
-                            {
-                                // State is unsatisfiable
-                                return None;
-                            }
-                        }
-                    }
-                }
-            }
-        }
         Some(specialized_state)
     }
 }

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

@@ -15,6 +15,7 @@ struct Setup<'a> {
     int_sub_subpiece_expr: Expression,
     eax_variable: Expression,
     rax_variable: Expression,
+    rcx_variable: Expression,
 }
 
 impl<'a> Setup<'a> {
@@ -99,6 +100,11 @@ impl<'a> Setup<'a> {
                 size: ByteSize::new(8),
                 is_temp: false,
             }),
+            rcx_variable: Expression::Var(Variable {
+                name: String::from("RCX"),
+                size: ByteSize::new(8),
+                is_temp: false,
+            }),
         }
     }
 }
@@ -123,6 +129,122 @@ fn trivial_expression_substitution() {
     };
     expr.substitute_trivial_operations();
     assert_eq!(expr, setup.rax_variable);
+
+    let sub_expr = Expression::BinOp {
+        lhs: Box::new(setup.rax_variable.clone()),
+        op: BinOpType::IntSub,
+        rhs: Box::new(setup.rcx_variable.clone()),
+    };
+    let mut expr = Expression::BinOp {
+        op: BinOpType::IntEqual,
+        lhs: Box::new(Expression::Const(Bitvector::zero(ByteSize::new(1).into()))),
+        rhs: Box::new(sub_expr.clone()),
+    };
+    expr.substitute_trivial_operations();
+    assert_eq!(
+        expr,
+        Expression::BinOp {
+            lhs: Box::new(setup.rax_variable.clone()),
+            op: BinOpType::IntEqual,
+            rhs: Box::new(setup.rcx_variable.clone()),
+        }
+    );
+    let mut expr = Expression::BinOp {
+        op: BinOpType::IntNotEqual,
+        lhs: Box::new(sub_expr.clone()),
+        rhs: Box::new(Expression::Const(Bitvector::zero(ByteSize::new(1).into()))),
+    };
+    expr.substitute_trivial_operations();
+    assert_eq!(
+        expr,
+        Expression::BinOp {
+            lhs: Box::new(setup.rax_variable.clone()),
+            op: BinOpType::IntNotEqual,
+            rhs: Box::new(setup.rcx_variable.clone()),
+        }
+    );
+
+    let mut expr = Expression::BinOp {
+        lhs: Box::new(Expression::BinOp {
+            lhs: Box::new(setup.rax_variable.clone()),
+            op: BinOpType::IntLess,
+            rhs: Box::new(setup.rcx_variable.clone()),
+        }),
+        op: BinOpType::BoolOr,
+        rhs: Box::new(Expression::BinOp {
+            lhs: Box::new(setup.rax_variable.clone()),
+            op: BinOpType::IntEqual,
+            rhs: Box::new(setup.rcx_variable.clone()),
+        }),
+    };
+    expr.substitute_trivial_operations();
+    assert_eq!(
+        expr,
+        Expression::BinOp {
+            lhs: Box::new(setup.rax_variable.clone()),
+            op: BinOpType::IntLessEqual,
+            rhs: Box::new(setup.rcx_variable.clone()),
+        }
+    );
+
+    let mut expr = Expression::Subpiece {
+        low_byte: ByteSize::new(0),
+        size: ByteSize::new(4),
+        arg: Box::new(Expression::Cast {
+            op: CastOpType::IntSExt,
+            size: ByteSize::new(8),
+            arg: Box::new(Expression::Var(Variable::mock("EAX", 4))),
+        }),
+    };
+    expr.substitute_trivial_operations();
+    assert_eq!(expr, Expression::Var(Variable::mock("EAX", 4)));
+    let mut expr = Expression::Subpiece {
+        low_byte: ByteSize::new(4),
+        size: ByteSize::new(4),
+        arg: Box::new(Expression::BinOp {
+            op: BinOpType::Piece,
+            lhs: Box::new(Expression::Var(Variable::mock("EAX", 4))),
+            rhs: Box::new(Expression::Var(Variable::mock("EBX", 4))),
+        }),
+    };
+    expr.substitute_trivial_operations();
+    assert_eq!(expr, Expression::Var(Variable::mock("EAX", 4)));
+    let mut expr = Expression::Subpiece {
+        low_byte: ByteSize::new(0),
+        size: ByteSize::new(4),
+        arg: Box::new(Expression::Subpiece {
+            low_byte: ByteSize::new(2),
+            size: ByteSize::new(6),
+            arg: Box::new(Expression::Var(Variable::mock("RAX", 8))),
+        }),
+    };
+    expr.substitute_trivial_operations();
+    assert_eq!(
+        expr,
+        Expression::Subpiece {
+            low_byte: ByteSize::new(2),
+            size: ByteSize::new(4),
+            arg: Box::new(Expression::Var(Variable::mock("RAX", 8))),
+        }
+    );
+
+    let mut expr = Expression::UnOp {
+        op: UnOpType::BoolNegate,
+        arg: Box::new(Expression::BinOp {
+            lhs: Box::new(setup.rax_variable.clone()),
+            op: BinOpType::IntLess,
+            rhs: Box::new(setup.rcx_variable.clone()),
+        }),
+    };
+    expr.substitute_trivial_operations();
+    assert_eq!(
+        expr,
+        Expression::BinOp {
+            lhs: Box::new(setup.rcx_variable.clone()),
+            op: BinOpType::IntLessEqual,
+            rhs: Box::new(setup.rax_variable.clone()),
+        }
+    );
 }
 
 #[test]

test/artificial_samples/cwe_78.c

 #include <string.h>
 #include <stdlib.h>
 
-int constant_system() {
+void constant_system() {
     system("ls");
 }
 
 int main(int argc, char **argv) {
-    char *dest = "usr/bin/cat ";
+    char dest[30] = "usr/bin/cat ";
     strcat(dest, argv[1]);
     system(dest);
     constant_system();

test/src/lib.rs

@@ -185,6 +185,8 @@ mod tests {
         mark_architecture_skipped(&mut tests, "ppc64le"); // Ghidra generates mangled function names here for some reason.
 
         mark_skipped(&mut tests, "x86", "clang"); // Return value detection insufficient for x86
+        mark_skipped(&mut tests, "arm", "clang"); // Loss of stack pointer position
+        mark_skipped(&mut tests, "aarch64", "clang"); // Loss of stack pointer position
 
         mark_compiler_skipped(&mut tests, "mingw32-gcc"); // Pointer Inference returns insufficient results for PE