Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
29 commits
Select commit Hold shift + click to select a range
40167f0
Update toolchain to `2025-04-04`
davidsemakula Oct 16, 2025
5c9af37
Replace `rustc_target::abi` with `rustc_abi`
davidsemakula Oct 16, 2025
efc5e7c
Update unified fp intrinsics
davidsemakula Oct 16, 2025
37a142a
Update const value and val tree patterns
davidsemakula Oct 16, 2025
4b3cc56
Use new HIR methods
davidsemakula Oct 16, 2025
1200a96
Handle optional type names in `DefPathData`
davidsemakula Oct 16, 2025
c32a345
Add null pointer dereference assertion message
davidsemakula Oct 17, 2025
854bb01
Handle `NullOp::ContractChecks`
davidsemakula Oct 17, 2025
1955b66
Use new `rustc` entrypoint
davidsemakula Oct 17, 2025
ad8fbc7
Handle `Rvalue::Len`
davidsemakula Oct 17, 2025
74ac81c
Handle unsafe binder types
davidsemakula Oct 16, 2025
2194555
Fix `FieldIdx` and `VariantIdx` type inference issues
davidsemakula Oct 16, 2025
f2bf3c7
Update `Cargo.lock`
davidsemakula Oct 16, 2025
7f0c38d
Normalize associated types
davidsemakula Oct 18, 2025
ff1e3db
Normalize field types when transmuting and copying
davidsemakula Dec 25, 2025
cfd18c1
Add null pointer dereference analysis
davidsemakula Dec 28, 2025
ca031d3
Fix active calls map tracking
davidsemakula Dec 29, 2025
0728ff4
Add equality expression refinement/simplification for casting and tra…
davidsemakula Dec 27, 2025
09284f8
tests: Update call graphs
davidsemakula Dec 29, 2025
af5a356
Rebuild summary store
davidsemakula Dec 29, 2025
9a65635
Update toolchain to `2025-05-09`
davidsemakula Dec 23, 2025
e6a0590
revert: Handle optional type names in `DefPathData`
davidsemakula Dec 23, 2025
b4b43ec
Handle `AssertKind::ResumedAfterDrop`
davidsemakula Dec 24, 2025
c54e6ca
Update `TerminatorKind::Drop`
davidsemakula Dec 24, 2025
e321338
Update `Cargo.lock`
davidsemakula Dec 30, 2025
1534190
clippy
davidsemakula Dec 30, 2025
7b80251
tests: Update call graphs
davidsemakula Dec 30, 2025
3bad710
Rebuild summary store
davidsemakula Dec 30, 2025
2b8b71d
Handle new `DefPathData` variants in `component_name`
davidsemakula Jan 14, 2026
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
543 changes: 303 additions & 240 deletions Cargo.lock

Large diffs are not rendered by default.

Binary file modified binaries/summary_store.tar
Binary file not shown.
56 changes: 38 additions & 18 deletions checker/src/abstract_value.rs
Original file line number Diff line number Diff line change
Expand Up @@ -197,11 +197,11 @@ impl AbstractValue {
// The overall expression is going to overflow, so pre-compute the simpler domains from
// the larger expression and then replace its expression with TOP.
if left.expression_size < right.expression_size {
debug!("binary expression right operand abstracted: {:?}", right);
debug!("binary expression right operand abstracted: {right:?}");
right = AbstractValue::make_from(right.expression.clone(), u64::MAX);
expression_size = left.expression_size + 1;
} else {
debug!("binary expression left operand abstracted: {:?}", left);
debug!("binary expression left operand abstracted: {left:?}");
left = AbstractValue::make_from(left.expression.clone(), u64::MAX);
expression_size = right.expression_size + 1;
}
Expand All @@ -228,11 +228,11 @@ impl AbstractValue {
// The overall expression is going to overflow, so pre-compute the simpler domains from
// the larger expression and then replace its expression with TOP.
if left.expression_size < right.expression_size {
debug!("binary expression right operand abstracted: {:?}", right);
debug!("binary expression right operand abstracted: {right:?}");
right = AbstractValue::make_from(right.expression.clone(), u64::MAX);
expression_size = left.expression_size + 1;
} else {
debug!("binary expression left operand abstracted: {:?}", left);
debug!("binary expression left operand abstracted: {left:?}");
left = AbstractValue::make_from(left.expression.clone(), u64::MAX);
expression_size = right.expression_size + 1;
}
Expand Down Expand Up @@ -668,7 +668,7 @@ impl AbstractValue {
pub fn make_from(expression: Expression, expression_size: u64) -> Rc<AbstractValue> {
if expression_size > k_limits::MAX_EXPRESSION_SIZE {
if expression_size < u64::MAX {
debug!("expression abstracted: {:?}", expression);
debug!("expression abstracted: {expression:?}");
}
// If the expression gets too large, refining it gets expensive and composing it
// into other expressions leads to exponential growth. We therefore need to abstract
Expand Down Expand Up @@ -1737,7 +1737,7 @@ impl AbstractValueTrait for Rc<AbstractValue> {
if let Some(trimmed) = self
.trim_prefix_conjuncts(k_limits::MAX_EXPRESSION_SIZE - other.expression_size)
{
debug!("and expression prefix trimmed, self: {:?}", self);
debug!("and expression prefix trimmed, self: {self:?}");
trimmed_self = trimmed;
} else {
return other;
Expand Down Expand Up @@ -2024,7 +2024,6 @@ impl AbstractValueTrait for Rc<AbstractValue> {

/// Returns an element that is "self.cmp(other)".
#[logfn_inputs(TRACE)]
#[must_use]
fn compare(&self, other: Self) -> Self {
let zero = Rc::new(ConstantDomain::I128(0).into());
let one = Rc::new(ConstantDomain::I128(1).into());
Expand Down Expand Up @@ -2456,8 +2455,7 @@ impl AbstractValueTrait for Rc<AbstractValue> {
&& !(consequent.is_top() || alternate.is_top())
{
debug!(
"conditional with mismatched types {:?}: {:?} {:?}: {:?}",
consequent_type, consequent, alternate_type, alternate
"conditional with mismatched types {consequent_type:?}: {consequent:?} {alternate_type:?}: {alternate:?}"
);
return Rc::new(TOP);
}
Expand All @@ -2467,23 +2465,23 @@ impl AbstractValueTrait for Rc<AbstractValue> {
.expression_size
.saturating_add(consequent.expression_size);
if condition_plus_consequent < k_limits::MAX_EXPRESSION_SIZE - 1 {
debug!("alternate abstracted: {:?}", alternate);
debug!("alternate abstracted: {alternate:?}");
alternate = AbstractValue::make_from(alternate.expression.clone(), u64::MAX);
expression_size = condition_plus_consequent + 1;
} else {
let condition_plus_alternate = self
.expression_size
.saturating_add(alternate.expression_size);
if condition_plus_alternate < k_limits::MAX_EXPRESSION_SIZE - 1 {
debug!("consequent abstracted: {:?}", consequent);
debug!("consequent abstracted: {consequent:?}");
consequent = AbstractValue::make_from(consequent.expression.clone(), u64::MAX);
expression_size = condition_plus_alternate + 1;
} else {
let consequent_plus_alternate = consequent
.expression_size
.saturating_add(alternate.expression_size);
if consequent_plus_alternate < k_limits::MAX_EXPRESSION_SIZE - 1 {
debug!("condition abstracted: {:?}", condition);
debug!("condition abstracted: {condition:?}");
condition =
AbstractValue::make_from(condition.expression.clone(), u64::MAX);
expression_size = consequent_plus_alternate + 1;
Expand Down Expand Up @@ -2827,10 +2825,33 @@ impl AbstractValueTrait for Rc<AbstractValue> {
operand,
target_type,
},
) => {
if *val == 0 && *target_type == ExpressionType::ThinPointer {
return self.equals(operand.clone());
}
) if *val == 0 && *target_type == ExpressionType::ThinPointer => {
return self.equals(operand.clone());
}

// [0 == cast(x, integer)] -> 0 == x
(
Expression::CompileTimeConstant(ConstantDomain::U128(val)),
Expression::Cast {
operand,
target_type,
},
) if *val == 0 && target_type.is_integer() => {
return self.equals(operand.clone());
}

// [0 == transmute(x, integer)] -> 0 == x
(
Expression::CompileTimeConstant(ConstantDomain::U128(val)),
Expression::Transmute {
operand,
target_type,
},
) if *val == 0
&& target_type.is_integer()
&& target_type.bit_length() == operand.expression.infer_type().bit_length() =>
{
return self.equals(operand.clone());
}

// [0 == !x] -> x when x is Boolean. Canonicalize it to the latter.
Expand Down Expand Up @@ -6858,8 +6879,7 @@ impl AbstractValueTrait for Rc<AbstractValue> {
return self.clone();
}
info!(
"replacing embedded path root of {:?}, old_root {:?}, new_root {:?}",
self, old_root, new_root
"replacing embedded path root of {self:?}, old_root {old_root:?}, new_root {new_root:?}"
);
self.clone()
}
Expand Down
Loading
Loading