diff --git a/Cargo.lock b/Cargo.lock index d0927124..5a241d46 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -188,6 +188,15 @@ dependencies = [ "lazy_static", ] +[[package]] +name = "divisors" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bbb1463b94567b1d22f0e07d13a70dcc25f39f88ad8cc197ecb978efddb9136e" +dependencies = [ + "num", +] + [[package]] name = "either" version = "1.6.1" @@ -339,6 +348,7 @@ dependencies = [ "bytesize", "cargo-husky", "clap", + "divisors", "env_logger", "goblin", "itertools", @@ -353,6 +363,41 @@ dependencies = [ "z3", ] +[[package]] +name = "num" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b8536030f9fea7127f841b45bb6243b27255787fb4eb83958aa1ef9d2fdc0c36" +dependencies = [ + "num-bigint", + "num-complex", + "num-integer", + "num-iter", + "num-rational", + "num-traits", +] + +[[package]] +name = "num-bigint" +version = "0.2.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "090c7f9998ee0ff65aa5b723e4009f7b217707f1fb5ea551329cc4d6231fb304" +dependencies = [ + "autocfg", + "num-integer", + "num-traits", +] + +[[package]] +name = "num-complex" +version = "0.2.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b6b19411a9719e753aff12e5187b74d60d3dc449ec3f4dc21e3989c3f554bc95" +dependencies = [ + "autocfg", + "num-traits", +] + [[package]] name = "num-integer" version = "0.1.44" @@ -363,6 +408,29 @@ dependencies = [ "num-traits", ] +[[package]] +name = "num-iter" +version = "0.1.42" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b2021c8337a54d21aca0d59a92577a029af9431cb59b909b03252b9c164fad59" +dependencies = [ + "autocfg", + "num-integer", + "num-traits", +] + +[[package]] +name = "num-rational" +version = "0.2.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5c000134b5dbf44adc5cb772486d335293351644b801551abe8f75c84cfa4aef" +dependencies = [ + "autocfg", + "num-bigint", + "num-integer", + "num-traits", +] + [[package]] name = "num-traits" version = "0.2.14" diff --git a/Cargo.toml b/Cargo.toml index d228caec..df70d605 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -38,6 +38,7 @@ bytesize = "~1.0.1" itertools = "~0.9.0" anyhow = "~1.0.34" thiserror = "~1.0.22" +divisors = "~0.2.1" [dev-dependencies] rayon = "~1.5.0" diff --git a/examples/arithmetic.c b/examples/arithmetic.c index 79d44de9..689a86a4 100644 --- a/examples/arithmetic.c +++ b/examples/arithmetic.c @@ -22,5 +22,7 @@ uint64_t main() { c = b - c; + c = c % b; + return c; } diff --git a/src/bitvec.rs b/src/bitvec.rs index 2ad65d4d..e774f53d 100644 --- a/src/bitvec.rs +++ b/src/bitvec.rs @@ -1,5 +1,5 @@ use std::fmt; -use std::ops::{Add, BitAnd, BitOr, BitXor, Div, Mul, Neg, Not, Shl, Shr, Sub}; +use std::ops::{Add, BitAnd, BitOr, BitXor, Div, Mul, Neg, Not, Rem, Shl, Shr, Sub}; #[derive(Clone, Copy, Eq, Hash, PartialEq, PartialOrd)] pub struct BitVector(pub u64); @@ -81,6 +81,18 @@ impl Div for BitVector { } } +impl Rem for BitVector { + type Output = BitVector; + + fn rem(self, other: BitVector) -> Self::Output { + if other == BitVector(0) { + self + } else { + Self(self.0.wrapping_rem(other.0)) + } + } +} + impl BitOr for BitVector { type Output = BitVector; diff --git a/src/boolector.rs b/src/boolector.rs index b66bae03..7fdbce7e 100644 --- a/src/boolector.rs +++ b/src/boolector.rs @@ -93,6 +93,8 @@ fn traverse<'a>( .and(&traverse(graph, rhs, solver, bvs)), BVOperator::Divu => traverse(graph, lhs, solver, bvs) .udiv(&traverse(graph, rhs, solver, bvs)), + BVOperator::Remu => traverse(graph, lhs, solver, bvs) + .urem(&traverse(graph, rhs, solver, bvs)), BVOperator::Sltu => traverse(graph, lhs, solver, bvs) .ult(&traverse(graph, rhs, solver, bvs)) .uext(63), diff --git a/src/engine.rs b/src/engine.rs index 3113784b..d7b10432 100644 --- a/src/engine.rs +++ b/src/engine.rs @@ -1,3 +1,5 @@ + + use crate::{ boolector::Boolector, bug::{BasicInfo, Bug}, @@ -323,21 +325,31 @@ where Ok(None) } - fn execute_divu( + fn execute_divu_remu( &mut self, instruction: Instruction, rtype: RType, - ) -> Result, EngineError> { + op: Op, + ) -> Result, EngineError> + where + Op: FnOnce(u64, u64) -> u64, + { let bug = match self.regs[rtype.rs2() as usize] { Value::Symbolic(divisor) => { - trace!("divu: symbolic divisor -> find input for divisor == 0"); + trace!( + "{}: symbolic divisor -> find input for divisor == 0", + instruction_to_str(instruction) + ); self.execute_query(Query::Equals((divisor, 0)), |info| Bug::DivisionByZero { info, })? } Value::Concrete(divisor) if divisor == 0 => { - trace!("divu: divisor == 0 -> compute reachability"); + trace!( + "{}: divisor == 0 -> compute reachability", + instruction_to_str(instruction) + ); self.execute_query(Query::Reachable, |info| Bug::DivisionByZero { info })? } @@ -345,7 +357,7 @@ where }; if bug.is_none() { - self.execute_rtype(instruction, rtype, u64::wrapping_div) + self.execute_rtype(instruction, rtype, op) } else { Ok(bug) } @@ -614,7 +626,10 @@ where let result = self.run(); - if !matches!(result, Err(EngineError::ExecutionDepthReached(_)) | Ok(None)) { + if !matches!( + result, + Err(EngineError::ExecutionDepthReached(_)) | Ok(None) + ) { return result; } @@ -895,8 +910,12 @@ where Instruction::Add(rtype) => self.execute_rtype(instruction, rtype, u64::wrapping_add), Instruction::Sub(rtype) => self.execute_rtype(instruction, rtype, u64::wrapping_sub), Instruction::Mul(rtype) => self.execute_rtype(instruction, rtype, u64::wrapping_mul), - Instruction::Divu(rtype) => self.execute_divu(instruction, rtype), - Instruction::Remu(rtype) => self.execute_rtype(instruction, rtype, u64::wrapping_rem), + Instruction::Divu(rtype) => { + self.execute_divu_remu(instruction, rtype, u64::wrapping_div) + } + Instruction::Remu(rtype) => { + self.execute_divu_remu(instruction, rtype, u64::wrapping_rem) + } Instruction::Sltu(rtype) => { self.execute_rtype(instruction, rtype, |l, r| if l < r { 1 } else { 0 }) } diff --git a/src/solver.rs b/src/solver.rs index 914ad502..4b5cb937 100644 --- a/src/solver.rs +++ b/src/solver.rs @@ -6,9 +6,10 @@ use crate::{ bitvec::*, symbolic_state::{get_operands, BVOperator, Formula, Node, OperandSide, SymbolId}, }; +use divisors::get_divisors; use log::{debug, log_enabled, trace, Level}; use petgraph::{visit::EdgeRef, Direction}; -use rand::{distributions::Uniform, random, thread_rng, Rng}; +use rand::{distributions::Uniform, random, seq::SliceRandom, thread_rng, Rng}; use std::time::{Duration, Instant}; use thiserror::Error; @@ -120,6 +121,12 @@ fn is_invertable(op: BVOperator, s: BitVector, t: BitVector, d: OperandSide) -> true } } + BVOperator::Remu => match d { + OperandSide::Lhs => !(s <= t), + OperandSide::Rhs => { + !(s < t) || ((t != BitVector(0)) && t == s - BitVector(1)) || (s - t <= t) + } + }, BVOperator::Not => true, BVOperator::BitwiseAnd => (t & s) == t, BVOperator::Equals => true, @@ -277,6 +284,36 @@ fn compute_inverse_value(op: BVOperator, s: BitVector, t: BitVector, d: OperandS } } }, + BVOperator::Remu => match d { + OperandSide::Lhs => { + let y = BitVector( + thread_rng().sample(Uniform::new_inclusive(1, (BitVector::ones() - t / s).0)), + ); + if !(s.0.overflowing_mul(y.0).1) && !(t.0.overflowing_add(y.0 * s.0).1) { + return y; + } + panic!("Big Error in REMU Inverse Value (LHS)") + } + OperandSide::Rhs => { + if s == t { + let x = BitVector( + thread_rng().sample(Uniform::new_inclusive(t.0, BitVector::ones().0)), + ); + if x == t { + BitVector(0) + } else { + x + } + } else { + let mut v = get_divisors(s.0 - t.0); + v.push(1); + v.push(s.0 - t.0); + v = v.into_iter().filter(|x| x > &t.0).collect(); + + return BitVector(*v.choose(&mut rand::thread_rng()).unwrap()); + } + } + }, BVOperator::BitwiseAnd => BitVector(random::()) | t, BVOperator::Equals => { if t == BitVector(0) { @@ -357,6 +394,24 @@ fn compute_consistent_value(op: BVOperator, t: BitVector, d: OperandSide) -> Bit BitVector(thread_rng().sample(Uniform::new(1, BitVector::ones().0))) } } + BVOperator::Remu => match d { + OperandSide::Lhs => { + if t == BitVector::ones() { + BitVector::ones() + } else { + BitVector(thread_rng().sample(Uniform::new_inclusive(t.0, BitVector::ones().0))) + } + } + OperandSide::Rhs => { + if t == BitVector::ones() { + BitVector(0) + } else { + BitVector( + thread_rng().sample(Uniform::new_inclusive(t.0 + 1, BitVector::ones().0)), + ) + } + } + }, BVOperator::BitwiseAnd => BitVector(random::()) | t, _ => unreachable!("unknown operator for consistent value: {:?}", op), } @@ -513,6 +568,7 @@ fn propagate_assignment(f: &Formula, ab: &mut Assignment, n: SymbolId BitVector(0) } }), + BVOperator::Remu => update_binary(f, ab, n, "%", |l, r| l % r), BVOperator::Equals => update_binary(f, ab, n, "=", |l, r| { if l == r { BitVector(1) diff --git a/src/symbolic_state.rs b/src/symbolic_state.rs index 6e208770..cd77f992 100644 --- a/src/symbolic_state.rs +++ b/src/symbolic_state.rs @@ -32,6 +32,7 @@ pub enum BVOperator { Mul, Divu, Sltu, + Remu, Not, Equals, BitwiseAnd, @@ -57,6 +58,7 @@ impl fmt::Display for BVOperator { BVOperator::Mul => "*", BVOperator::Divu => "/", BVOperator::Not => "!", + BVOperator::Remu => "%", BVOperator::Equals => "=", BVOperator::BitwiseAnd => "&", BVOperator::Sltu => "<", @@ -87,6 +89,7 @@ fn instruction_to_bv_operator(instruction: Instruction) -> BVOperator { Instruction::Sub(_) => BVOperator::Sub, Instruction::Mul(_) => BVOperator::Mul, Instruction::Divu(_) => BVOperator::Divu, + Instruction::Remu(_) => BVOperator::Remu, Instruction::Sltu(_) => BVOperator::Sltu, _ => unimplemented!("can not translate {:?} to Operator", instruction), } diff --git a/src/z3.rs b/src/z3.rs index 726be632..9414048c 100644 --- a/src/z3.rs +++ b/src/z3.rs @@ -152,6 +152,7 @@ impl<'a, 'ctx> Z3Translator<'a, 'ctx> { BVOperator::Sub => traverse_binary!(self, lhs, bvsub, rhs), BVOperator::Mul => traverse_binary!(self, lhs, bvmul, rhs), BVOperator::Divu => traverse_binary!(self, lhs, bvudiv, rhs), + BVOperator::Remu => traverse_binary!(self, lhs, bvurem, rhs), BVOperator::Equals => traverse_binary!(self, lhs, _eq, rhs) .as_bool() .unwrap() diff --git a/tests/engine.rs b/tests/engine.rs index d8d522b4..c7747671 100644 --- a/tests/engine.rs +++ b/tests/engine.rs @@ -58,7 +58,8 @@ fn execute_riscu(names: &'static [&str], solver: Backend) { let bug = possible_bug.unwrap(); assert!( - matches!((file_name, bug.clone()), + matches!( + (file_name, bug.clone()), ("arithmetic.c", Bug::ExitCodeGreaterZero { .. }) | ("invalid-memory-access-2-35.c", Bug::AccessToOutOfRangeAddress { .. }) | ("if-else.c", Bug::ExitCodeGreaterZero { .. }) | @@ -73,7 +74,8 @@ fn execute_riscu(names: &'static [&str], solver: Backend) { ("recursive-fibonacci-1-10.c", Bug::ExitCodeGreaterZero { .. }) | ("simple-if-else-1-35.c", Bug::ExitCodeGreaterZero { .. }) | ("simple-increasing-loop-1-35.c", Bug::ExitCodeGreaterZero { .. }) | - ("two-level-nested-loop-1-35.c", Bug::ExitCodeGreaterZero { .. })), + ("two-level-nested-loop-1-35.c", Bug::ExitCodeGreaterZero { .. }) + ), "found right bug type (actual: {}) for {}", bug, file_name