Skip to content

Commit

Permalink
New nightly (#22)
Browse files Browse the repository at this point in the history
* nightly-2024-12-05

* nightly-2024-12-12
  • Loading branch information
hermanventer authored Dec 12, 2024
1 parent 7afcd5f commit 0d2b4d0
Show file tree
Hide file tree
Showing 22 changed files with 148 additions and 96 deletions.
14 changes: 7 additions & 7 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Binary file modified binaries/summary_store.tar
Binary file not shown.
59 changes: 46 additions & 13 deletions checker/src/abstract_value.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1955,6 +1955,10 @@ impl AbstractValueTrait for Rc<AbstractValue> {
return left.cast(target_type);
}
}
Expression::Reference(..) if target_type.is_integer() => {
// [(&x) as t] -> &x if t is an integer
return self.clone();
}
// [(v : t1) as target_type] -> (v: t1) if t1.max_value() == target_type.max_value()
Expression::Variable { var_type: t1, .. }
| Expression::InitialParameterValue { var_type: t1, .. } => {
Expand Down Expand Up @@ -2084,15 +2088,15 @@ impl AbstractValueTrait for Rc<AbstractValue> {
// [if !(x) { a } else { b }] -> if x { b } else { a }
return operand.conditional_expression(alternate, consequent);
}
// [if 0 == x { y } else { true }] -> x || y
// [if 0 == x { false } else { y }] -> x && y
// [if 0 == x { y } else { true }] -> x != 0 || y
// [if 0 == x { false } else { y }] -> x != 0 && y
if let Expression::Equals { left: z, right: x } = &self.expression {
if let Expression::CompileTimeConstant(ConstantDomain::U128(0)) = z.expression {
if alternate.as_bool_if_known().unwrap_or(false) {
return x.or(consequent);
return x.not_equals(z.clone()).or(consequent);
}
if !consequent.as_bool_if_known().unwrap_or(true) {
return x.and(alternate);
return x.not_equals(z.clone()).and(alternate);
}
}
}
Expand Down Expand Up @@ -4851,6 +4855,13 @@ impl AbstractValueTrait for Rc<AbstractValue> {
/// Returns an element that is "self % other".
#[logfn_inputs(TRACE)]
fn remainder(&self, other: Rc<AbstractValue>) -> Rc<AbstractValue> {
// [(x % y) % y] -> x % y
if let Expression::Rem { left: x, right: y } = &self.expression {
if y.eq(&other) {
return x.clone();
}
}

// [(x as t) % c] -> x % c if c.is_power_of_two() && c <= t.modulo_value()
if let Expression::Cast { operand: x, .. } = &self.expression {
let ct = x.expression.infer_type();
Expand Down Expand Up @@ -6842,9 +6853,26 @@ impl AbstractValueTrait for Rc<AbstractValue> {
/// or zero filled as appropriate.
#[logfn_inputs(TRACE)]
fn transmute(&self, target_type: ExpressionType) -> Rc<AbstractValue> {
if target_type.is_integer() && self.expression.infer_type().is_integer() {
let expression_type = self.expression.infer_type();
if expression_type == target_type {
self.clone()
} else if target_type.is_integer()
|| target_type == ExpressionType::ThinPointer && expression_type.is_integer()
{
self.unsigned_modulo(target_type.bit_length())
.cast(target_type)
.try_to_constant_fold_and_distribute_typed_unary_op(
target_type,
ConstantDomain::transmute,
Self::transmute,
|o, t| {
AbstractValue::make_typed_unary(o, t, |operand, target_type| {
Expression::Transmute {
operand,
target_type,
}
})
},
)
} else if target_type == ExpressionType::Bool {
self.unsigned_modulo(target_type.bit_length())
.not_equals(Rc::new(ConstantDomain::U128(0).into()))
Expand Down Expand Up @@ -6943,17 +6971,22 @@ impl AbstractValueTrait for Rc<AbstractValue> {
}

/// Returns an expression that discards (zero fills) bits that are not in the specified number
/// of least significant bits. The result is an unsigned integer.
#[logfn(TRACE)]
/// of least-significant bits. The result is an unsigned integer.
#[logfn_inputs(TRACE)]
fn unsigned_modulo(&self, num_bits: u8) -> Rc<AbstractValue> {
if let Expression::CompileTimeConstant(c) = &self.expression {
Rc::new(c.unsigned_modulo(num_bits).into())
} else if num_bits == 128 {
self.try_to_retype_as(ExpressionType::U128)
} else {
let power_of_two = Rc::new(ConstantDomain::U128(1 << num_bits).into());
let unsigned = self.try_to_retype_as(ExpressionType::U128);
unsigned.remainder(power_of_two)
let expression_type = self.expression.infer_type();
if expression_type.bit_length() == num_bits {
self.clone()
} else if num_bits == 128 {
self.try_to_retype_as(ExpressionType::U128)
} else {
let power_of_two = Rc::new(ConstantDomain::U128(1 << num_bits).into());
let unsigned = self.try_to_retype_as(ExpressionType::U128);
unsigned.remainder(power_of_two)
}
}
}

Expand Down
23 changes: 15 additions & 8 deletions checker/src/block_visitor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2197,17 +2197,24 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
}
mir::CastKind::Transmute => {
let source_type = self.get_operand_rustc_type(operand);
let source_value = self.visit_operand(operand);
let source_path = Path::get_as_path(source_value.clone());
let path = if source_value.is_function() {
Path::new_function(path)
} else {
path
let (source_path, target_path) = match operand {
mir::Operand::Copy(place) |
mir::Operand::Move(place) => (self.visit_lh_place(place), path),
mir::Operand::Constant(..) => {
let source_value = self.visit_operand(operand);
let source_path = Path::get_as_path(source_value.clone());
let target_path = if source_value.is_function() {
Path::new_function(path)
} else {
path
};
(source_path, target_path)
}
};
self.bv.copy_and_transmute(
source_path,
source_type,
path,
target_path,
ty,
);
}
Expand Down Expand Up @@ -2241,7 +2248,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
.get_operand_path(operand)
.canonicalize(&self.bv.current_environment);
if !self.type_visitor().is_slice_pointer(ty.kind()) {
source_path = Path::new_field(source_path, 0);
source_path = Path::new_field(source_path, 0).canonicalize(&self.bv.current_environment);
}
if let mir::Operand::Move(..) = operand {
self.bv
Expand Down
104 changes: 58 additions & 46 deletions checker/src/body_visitor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -412,7 +412,7 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> {
}
}
}
_ => {}
_ => (),
}
let refined_val = {
let top = abstract_value::TOP.into();
Expand Down Expand Up @@ -1784,6 +1784,60 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> {
)
}

fn add_leaf_fields_for(
&self,
path: Rc<Path>,
def: &'tcx AdtDef,
args: GenericArgsRef<'tcx>,
tcx: TyCtxt<'tcx>,
accumulator: &mut Vec<(Rc<Path>, Ty<'tcx>)>,
) {
if let Some(int_ty) = def.repr().int {
let ty = match int_ty {
rustc_abi::IntegerType::Fixed(t, true) => match t {
rustc_abi::Integer::I8 => tcx.types.i8,
rustc_abi::Integer::I16 => tcx.types.i16,
rustc_abi::Integer::I32 => tcx.types.i32,
rustc_abi::Integer::I64 => tcx.types.i64,
rustc_abi::Integer::I128 => tcx.types.i128,
},
rustc_abi::IntegerType::Fixed(t, false) => match t {
rustc_abi::Integer::I8 => tcx.types.u8,
rustc_abi::Integer::I16 => tcx.types.u16,
rustc_abi::Integer::I32 => tcx.types.u32,
rustc_abi::Integer::I64 => tcx.types.u64,
rustc_abi::Integer::I128 => tcx.types.u128,
},
rustc_abi::IntegerType::Pointer(true) => tcx.types.isize,
rustc_abi::IntegerType::Pointer(false) => tcx.types.usize,
};
let discr_path = Path::new_discriminant(path);
accumulator.push((discr_path, ty));
} else if !def.variants().is_empty() {
let variant = def.variants().iter().next().expect("at least one variant");
for (i, field) in variant.fields.iter().enumerate() {
let field_path = Path::new_field(path.clone(), i);
let field_ty = field.ty(tcx, args);
debug!("field_path: {:?}, field_ty: {:?}", field_path, field_ty);
if let TyKind::Adt(def, args) = field_ty.kind() {
self.add_leaf_fields_for(field_path, def, args, tcx, accumulator)
} else if self.type_visitor().is_slice_pointer(field_ty.kind()) {
let ptr_path = Path::new_field(field_path.clone(), 0);
let len_path = Path::new_length(field_path.clone());
let pointer_type = Ty::new_ptr(
self.tcx,
self.type_visitor.get_element_type(field_ty),
rustc_hir::Mutability::Not,
);
accumulator.push((ptr_path, pointer_type));
accumulator.push((len_path, tcx.types.usize));
} else {
accumulator.push((field_path, field_ty))
}
}
}
}

/// Copy the heap model at source_path to a heap model at target_path.
/// If the type of value at source_path is different from that at target_path, the value is transmuted.
#[logfn_inputs(TRACE)]
Expand All @@ -1794,52 +1848,10 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> {
target_path: Rc<Path>,
target_rustc_type: Ty<'tcx>,
) {
fn add_leaf_fields_for<'a>(
path: Rc<Path>,
def: &'a AdtDef,
args: GenericArgsRef<'a>,
tcx: TyCtxt<'a>,
accumulator: &mut Vec<(Rc<Path>, Ty<'a>)>,
) {
if let Some(int_ty) = def.repr().int {
let ty = match int_ty {
rustc_abi::IntegerType::Fixed(t, true) => match t {
rustc_abi::Integer::I8 => tcx.types.i8,
rustc_abi::Integer::I16 => tcx.types.i16,
rustc_abi::Integer::I32 => tcx.types.i32,
rustc_abi::Integer::I64 => tcx.types.i64,
rustc_abi::Integer::I128 => tcx.types.i128,
},
rustc_abi::IntegerType::Fixed(t, false) => match t {
rustc_abi::Integer::I8 => tcx.types.u8,
rustc_abi::Integer::I16 => tcx.types.u16,
rustc_abi::Integer::I32 => tcx.types.u32,
rustc_abi::Integer::I64 => tcx.types.u64,
rustc_abi::Integer::I128 => tcx.types.u128,
},
rustc_abi::IntegerType::Pointer(true) => tcx.types.isize,
rustc_abi::IntegerType::Pointer(false) => tcx.types.usize,
};
let discr_path = Path::new_discriminant(path);
accumulator.push((discr_path, ty));
} else if !def.variants().is_empty() {
let variant = def.variants().iter().next().expect("at least one variant");
for (i, field) in variant.fields.iter().enumerate() {
let field_path = Path::new_field(path.clone(), i);
let field_ty = field.ty(tcx, args);
if let TyKind::Adt(def, args) = field_ty.kind() {
add_leaf_fields_for(field_path, def, args, tcx, accumulator)
} else {
accumulator.push((field_path, field_ty))
}
}
}
}

let mut source_fields = Vec::new();
match source_rustc_type.kind() {
TyKind::Adt(source_def, source_substs) => {
add_leaf_fields_for(
self.add_leaf_fields_for(
source_path,
source_def,
source_substs,
Expand Down Expand Up @@ -1904,7 +1916,7 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> {
let mut target_fields = Vec::new();
match target_rustc_type.kind() {
TyKind::Adt(target_def, target_substs) => {
add_leaf_fields_for(
self.add_leaf_fields_for(
target_path,
target_def,
target_substs,
Expand Down Expand Up @@ -2063,7 +2075,7 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> {
} else if source_bits - copied_source_bits >= target_bits_to_write {
// target field can be completely assigned from bits of source field value
if source_bits - copied_source_bits > target_bits_to_write {
// discard higher order bits since they wont fit into the target field
// discard higher order bits since they won't fit into the target field
val = val.unsigned_modulo(target_bits_to_write);
}
if let Expression::Reference(p) = &val.expression {
Expand Down
2 changes: 1 addition & 1 deletion checker/src/call_visitor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3002,7 +3002,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx>
}

/// Updates the current state to reflect the effects of a normal return from the function call.
/// The paths and expressions of the side-effects are refined in the context of the pre-state
/// The paths and expressions of the side effects are refined in the context of the pre-state
/// (the environment before the call executed), while the refined effects are applied to the
/// current state.
#[logfn_inputs(TRACE)]
Expand Down
2 changes: 1 addition & 1 deletion checker/src/expression.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1529,7 +1529,7 @@ impl ExpressionType {
#[logfn_inputs(TRACE)]
pub fn is_floating_point_number(&self) -> bool {
use self::ExpressionType::*;
matches!(self, F32 | F64)
matches!(self, F16 | F32 | F64)
}

/// Returns true if this type is one of the integer types.
Expand Down
2 changes: 1 addition & 1 deletion checker/src/fixed_point_visitor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,7 @@ impl<'fixed, 'analysis, 'compilation, 'tcx>
}
}

/// Visits a single basic block, starting with an in_state that is the join of all of
/// Visits a single basic block, starting with an in_state that is the join of all
/// the out_state values of its predecessors and then updating out_state with the final
/// current_environment of the block. Also adds the block to the already_visited set.
#[logfn_inputs(TRACE)]
Expand Down
2 changes: 1 addition & 1 deletion checker/tests/call_graph/fnptr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@ commit;
],
"callables": [
{
"name": "/fnptr/fn1(u32,&'^0.Named(DefId(0:7 ~ fnptr[03cc]::fn1::'_), \"'_\") Binder { value: fn(u32) -> u32, bound_vars: [] })->u32",
"name": "/fnptr/fn1(u32,&'^0.Named(DefId(0:7 ~ fnptr[35c1]::fn1::'_), \"'_\") Binder { value: fn(u32) -> u32, bound_vars: [] })->u32",
"file_index": 0,
"first_line": 9,
"local": true
Expand Down
2 changes: 1 addition & 1 deletion checker/tests/call_graph/fnptr_clean.rs
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@ commit;
],
"callables": [
{
"name": "/fnptr_clean/fn1(u32,&'^0.Named(DefId(0:8 ~ fnptr_clean[123f]::fn1::'_), \"'_\") Binder { value: fn(u32) -> u32, bound_vars: [] })->u32",
"name": "/fnptr_clean/fn1(u32,&'^0.Named(DefId(0:8 ~ fnptr_clean[fae2]::fn1::'_), \"'_\") Binder { value: fn(u32) -> u32, bound_vars: [] })->u32",
"file_index": 0,
"first_line": 14,
"local": true
Expand Down
2 changes: 1 addition & 1 deletion checker/tests/call_graph/fnptr_deduplicate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ commit;
],
"callables": [
{
"name": "/fnptr_deduplicate/fn1(u32,&'^0.Named(DefId(0:7 ~ fnptr_deduplicate[324d]::fn1::'_), \"'_\") Binder { value: fn(u32) -> u32, bound_vars: [] })->u32",
"name": "/fnptr_deduplicate/fn1(u32,&'^0.Named(DefId(0:7 ~ fnptr_deduplicate[7eb2]::fn1::'_), \"'_\") Binder { value: fn(u32) -> u32, bound_vars: [] })->u32",
"file_index": 0,
"first_line": 10,
"local": true
Expand Down
2 changes: 1 addition & 1 deletion checker/tests/call_graph/fnptr_dom.rs
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ commit;
],
"callables": [
{
"name": "/fnptr_dom/fn1(u32,&'^0.Named(DefId(0:7 ~ fnptr_dom[e414]::fn1::'_), \"'_\") Binder { value: fn(u32) -> u32, bound_vars: [] },&'^1.Named(DefId(0:8 ~ fnptr_dom[e414]::fn1::'_#1), \"'_\") Binder { value: fn(u32) -> u32, bound_vars: [] })->u32",
"name": "/fnptr_dom/fn1(u32,&'^0.Named(DefId(0:7 ~ fnptr_dom[755f]::fn1::'_), \"'_\") Binder { value: fn(u32) -> u32, bound_vars: [] },&'^1.Named(DefId(0:8 ~ fnptr_dom[755f]::fn1::'_#1), \"'_\") Binder { value: fn(u32) -> u32, bound_vars: [] })->u32",
"file_index": 0,
"first_line": 9,
"local": true
Expand Down
Loading

0 comments on commit 0d2b4d0

Please sign in to comment.