Skip to content

Commit

Permalink
Implement LZCOUNT P-Code operation (#444)
Browse files Browse the repository at this point in the history
  • Loading branch information
Enkelmann authored Mar 6, 2024
1 parent 625b3d7 commit 520cede
Show file tree
Hide file tree
Showing 8 changed files with 69 additions and 10 deletions.
11 changes: 10 additions & 1 deletion src/cwe_checker_lib/src/abstract_domain/bitvector.rs
Original file line number Diff line number Diff line change
Expand Up @@ -245,7 +245,16 @@ pub mod tests {
assert_eq!(
BitvectorDomain::Value(bitvec!("-1:4")).cast(PopCount, ByteSize::new(8)),
bv(32)
)
);

assert_eq!(
BitvectorDomain::Value(bitvec!("-1:4")).cast(LzCount, ByteSize::new(8)),
bv(0)
);
assert_eq!(
BitvectorDomain::Value(bitvec!("0:4")).cast(LzCount, ByteSize::new(8)),
bv(32)
);
}

#[test]
Expand Down
28 changes: 26 additions & 2 deletions src/cwe_checker_lib/src/abstract_domain/interval.rs
Original file line number Diff line number Diff line change
Expand Up @@ -674,8 +674,32 @@ impl RegisterDomain for IntervalDomain {
IntervalDomain::new(
Bitvector::zero(width.into()),
Bitvector::from_u64(self.bytesize().as_bit_length() as u64)
.into_truncate(width)
.unwrap(),
.into_zero_resize(width),
)
}
}
LzCount => {
if let Ok(interval) = self.try_to_interval() {
let start_lz = interval.start.leading_zeros() as u64;
let end_lz = interval.end.leading_zeros() as u64;
// "leading zeroes" is monotonically decreasing for non-negative numbers.
if start_lz >= end_lz {
IntervalDomain::new(
Bitvector::from_u64(end_lz).into_zero_resize(width),
Bitvector::from_u64(start_lz).into_zero_resize(width),
)
} else {
IntervalDomain::new(
Bitvector::zero(width.into()),
Bitvector::from_u64(self.bytesize().as_bit_length() as u64)
.into_zero_resize(width),
)
}
} else {
IntervalDomain::new(
Bitvector::zero(width.into()),
Bitvector::from_u64(self.bytesize().as_bit_length() as u64)
.into_zero_resize(width),
)
}
}
Expand Down
20 changes: 20 additions & 0 deletions src/cwe_checker_lib/src/abstract_domain/interval/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -652,3 +652,23 @@ fn stride_rounding() {
);
assert_eq!(bitvec!("-123:1").round_down_to_stride_of(&interval), None);
}

#[test]
fn lzcount_op() {
use super::RegisterDomain;
// Test exact computation
let interval: IntervalDomain = Interval::mock_i8(3, 3).into();
let result = interval.cast(CastOpType::LzCount, ByteSize::new(2));
assert_eq!(result, bitvec!("0x6:2").into()); // leading 6 bits of the 8-bit value are zeroes

// Test result for non-exact interval
let interval: IntervalDomain = Interval::mock(3, 53).with_stride(5).into();
let result = interval.cast(CastOpType::LzCount, ByteSize::new(8));
assert_eq!(result, Interval::mock(58, 62).into());
let interval: IntervalDomain = Interval::mock(-1, 1).into();
let result = interval.cast(CastOpType::LzCount, ByteSize::new(8));
assert_eq!(result, Interval::mock(0, 64).into());
let interval: IntervalDomain = Interval::mock(-10, -4).into();
let result = interval.cast(CastOpType::LzCount, ByteSize::new(8));
assert_eq!(result, Interval::mock(0, 0).into());
}
2 changes: 1 addition & 1 deletion src/cwe_checker_lib/src/abstract_domain/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -129,7 +129,7 @@ pub trait TryToInterval {
fn try_to_interval(&self) -> Result<Interval, Error>;

/// If `self` represents an interval of absolute values (or can be widened to represent such an interval)
/// then return it as an interval of signed integers if the interval is bounded.
/// then return it as an interval of signed integers of the form `(start, end)` if the interval is bounded.
/// Else return an error.
/// Note that the conversion loses information about the bytesize of the values contained in the interval.
fn try_to_offset_interval(&self) -> Result<(i64, i64), Error> {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -58,9 +58,12 @@ impl BitvectorExtended for Bitvector {
CastOpType::Int2Float | CastOpType::Float2Float | CastOpType::Trunc => {
Err(anyhow!("Float operations not yet implemented"))
}
CastOpType::PopCount => Ok(Bitvector::from_u64(self.count_ones() as u64)
.into_truncate(width)
.unwrap()),
CastOpType::PopCount => {
Ok(Bitvector::from_u64(self.count_ones() as u64).into_resize_unsigned(width))
}
CastOpType::LzCount => {
Ok(Bitvector::from_u64(self.leading_zeros() as u64).into_resize_unsigned(width))
}
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -128,6 +128,7 @@ pub enum CastOpType {
Float2Float,
Trunc,
PopCount,
LzCount,
}

/// The type/mnemonic of an unary operation
Expand Down
6 changes: 4 additions & 2 deletions src/cwe_checker_lib/src/pcode/expressions.rs
Original file line number Diff line number Diff line change
Expand Up @@ -164,7 +164,7 @@ impl From<Expression> for IrExpression {
/// Cases where translation is not possible:
/// - `LOAD` and `STORE`, since these are not expressions (they have side effects).
/// - Expressions which store the size of their output in the output variable (to which we do not have access here).
/// These include `SUBPIECE`, `INT_ZEXT`, `INT_SEXT`, `INT2FLOAT`, `FLOAT2FLOAT`, `TRUNC` and `POPCOUNT`.
/// These include `SUBPIECE`, `INT_ZEXT`, `INT_SEXT`, `INT2FLOAT`, `FLOAT2FLOAT`, `TRUNC`, `LZCOUNT` and `POPCOUNT`.
/// Translation of these expressions is handled explicitly during translation of `Def`.
fn from(expr: Expression) -> IrExpression {
use ExpressionType::*;
Expand All @@ -186,7 +186,7 @@ impl From<Expression> for IrExpression {
op: expr.mnemonic.into(),
arg: Box::new(expr.input0.unwrap().into()),
},
INT_ZEXT | INT_SEXT | INT2FLOAT | FLOAT2FLOAT | TRUNC | POPCOUNT => panic!(),
INT_ZEXT | INT_SEXT | INT2FLOAT | FLOAT2FLOAT | TRUNC | POPCOUNT | LZCOUNT => panic!(),
}
}
}
Expand All @@ -203,6 +203,7 @@ pub enum ExpressionType {
PIECE,
SUBPIECE,
POPCOUNT,
LZCOUNT,

INT_EQUAL,
INT_NOTEQUAL,
Expand Down Expand Up @@ -353,6 +354,7 @@ impl From<ExpressionType> for IrCastOpType {
FLOAT2FLOAT => IrCastOpType::Float2Float,
TRUNC => IrCastOpType::Trunc,
POPCOUNT => IrCastOpType::PopCount,
LZCOUNT => IrCastOpType::LzCount,
_ => panic!(),
}
}
Expand Down
2 changes: 1 addition & 1 deletion src/cwe_checker_lib/src/pcode/term.rs
Original file line number Diff line number Diff line change
Expand Up @@ -166,7 +166,7 @@ impl Def {
size: target_var.size,
arg: Box::new(self.rhs.input0.unwrap().into()),
},
INT_ZEXT | INT_SEXT | INT2FLOAT | FLOAT2FLOAT | TRUNC | POPCOUNT => {
INT_ZEXT | INT_SEXT | INT2FLOAT | FLOAT2FLOAT | TRUNC | POPCOUNT | LZCOUNT => {
IrExpression::Cast {
op: self.rhs.mnemonic.into(),
size: target_var.size,
Expand Down

0 comments on commit 520cede

Please sign in to comment.