Skip to content

Commit

Permalink
Fix many clippy warnings across Kani (#1287)
Browse files Browse the repository at this point in the history
  • Loading branch information
tedinski authored Jun 17, 2022
1 parent 4e4917a commit 12660b8
Show file tree
Hide file tree
Showing 46 changed files with 228 additions and 267 deletions.
2 changes: 1 addition & 1 deletion cprover_bindings/src/goto_program/builtin.rs
Original file line number Diff line number Diff line change
Expand Up @@ -312,6 +312,6 @@ impl BuiltinFn {
}

pub fn call(&self, arguments: Vec<Expr>, loc: Location) -> Expr {
self.as_expr().with_location(loc.clone()).call(arguments).with_location(loc)
self.as_expr().with_location(loc).call(arguments).with_location(loc)
}
}
24 changes: 14 additions & 10 deletions cprover_bindings/src/goto_program/expr.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,9 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

// This file has a lot of function with names like "div"
#![allow(clippy::should_implement_trait)]

use self::BinaryOperand::*;
use self::ExprValue::*;
use self::UnaryOperand::*;
Expand Down Expand Up @@ -488,7 +492,7 @@ impl Expr {
let mut rval: Vec<_> = parameters
.iter()
.map(|parameter| {
arguments.remove(0).cast_to_machine_equivalent_type(&parameter.typ(), mm)
arguments.remove(0).cast_to_machine_equivalent_type(parameter.typ(), mm)
})
.collect();

Expand All @@ -510,7 +514,7 @@ impl Expr {

/// `union {double d; uint64_t bp} u = {.bp = 0x1234}; >>> u.d <<<`
pub fn double_constant_from_bitpattern(bp: u64) -> Self {
let c = unsafe { std::mem::transmute(bp) };
let c = f64::from_bits(bp);
Self::double_constant(c)
}

Expand All @@ -521,7 +525,7 @@ impl Expr {

/// `union {float f; uint32_t bp} u = {.bp = 0x1234}; >>> u.f <<<`
pub fn float_constant_from_bitpattern(bp: u32) -> Self {
let c = unsafe { std::mem::transmute(bp) };
let c = f32::from_bits(bp);
Self::float_constant(c)
}

Expand Down Expand Up @@ -622,7 +626,7 @@ impl Expr {
/// e.g. `({ int y = foo (); int z; if (y > 0) z = y; else z = - y; z; })`
/// `({ op1; op2; ...})`
pub fn statement_expression(ops: Vec<Stmt>, typ: Type) -> Self {
assert!(ops.len() > 0);
assert!(!ops.is_empty());
assert_eq!(ops.last().unwrap().get_expression().unwrap().typ, typ);
expr!(StatementExpression { statements: ops }, typ)
}
Expand Down Expand Up @@ -1350,7 +1354,7 @@ impl Expr {
assert!(self.typ.is_integer());
assert_eq!(self.typ, e.typ);
let typ = self.typ.clone();
let res = self.clone().add_overflow(e.clone());
let res = self.clone().add_overflow(e);
// If negative + something overflowed, the something must have been negative too, so we saturate to min.
// (self < 0) ? min_int : max_int
let saturating_val = self.is_negative().ternary(typ.min_int_expr(mm), typ.max_int_expr(mm));
Expand All @@ -1362,7 +1366,7 @@ impl Expr {
assert!(self.typ.is_integer());
assert_eq!(self.typ, e.typ);
let typ = self.typ.clone();
let res = self.clone().sub_overflow(e.clone());
let res = self.sub_overflow(e.clone());
// If something minus a negative overflowed, it must have overflowed past positive max. Saturate there.
// Otherwise, if something minus a positive overflowed, it must have overflowed to past min. Saturate there.
let saturating_val = e.is_negative().ternary(typ.max_int_expr(mm), typ.min_int_expr(mm));
Expand Down Expand Up @@ -1446,12 +1450,12 @@ impl Expr {
}
}
None => {
for i in 0..fields.len() {
if fields[i].is_padding() {
for field in fields {
if field.is_padding() {
continue;
}
let name = fields[i].name();
exprs.insert(name, self.clone().member(&name.to_string(), &symbol_table));
let name = field.name();
exprs.insert(name, self.clone().member(&name.to_string(), symbol_table));
}
}
}
Expand Down
2 changes: 1 addition & 1 deletion cprover_bindings/src/goto_program/location.rs
Original file line number Diff line number Diff line change
Expand Up @@ -138,7 +138,7 @@ impl Location {
file.into(),
function.intern(),
line,
col.map(|x| x.try_into().unwrap()),
col,
comment.into(),
property_name.into(),
),
Expand Down
5 changes: 5 additions & 0 deletions cprover_bindings/src/goto_program/mod.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,12 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

//! This module contains typesafe representations of CBMC's data structures
// There are a fair number of constructs in this module that are better maintained as
// explicit pattern matching versus using the `matches!` macro.
#![allow(clippy::match_like_matches_macro)]

mod builtin;
mod expr;
mod location;
Expand Down
8 changes: 4 additions & 4 deletions cprover_bindings/src/goto_program/stmt.rs
Original file line number Diff line number Diff line change
Expand Up @@ -205,10 +205,10 @@ impl Stmt {
Stmt::block(
vec![
// Assert our expected true expression.
Stmt::assert(expect_true.clone(), "sanity_check", &assert_msg, loc.clone()),
Stmt::assert(expect_true.clone(), "sanity_check", &assert_msg, loc),
// If expect_true is false, assume false to block any further
// exploration of this path.
Stmt::assume(expect_true, loc.clone()),
Stmt::assume(expect_true, loc),
],
loc,
)
Expand Down Expand Up @@ -246,7 +246,7 @@ impl Stmt {
/// SUCCESS/FAILURE, it uses SATISFIED/FAILED
pub fn cover(cond: Expr, loc: Location) -> Self {
assert!(cond.typ().is_bool());
BuiltinFn::CProverCover.call(vec![cond], loc.clone()).as_stmt(loc)
BuiltinFn::CProverCover.call(vec![cond], loc).as_stmt(loc)
}

/// `lhs.typ lhs = value;` or `lhs.typ lhs;`
Expand Down Expand Up @@ -330,7 +330,7 @@ impl Stmt {
pub fn with_label<T: Into<InternedString>>(self, label: T) -> Self {
let label = label.into();
assert!(!label.is_empty());
stmt!(Label { label, body: self }, self.location().clone())
stmt!(Label { label, body: self }, *self.location())
}
}

Expand Down
2 changes: 1 addition & 1 deletion cprover_bindings/src/goto_program/symbol.rs
Original file line number Diff line number Diff line change
Expand Up @@ -159,7 +159,7 @@ impl Symbol {
name.to_string(),
loc,
typ,
body.map_or(SymbolValues::None, |x| SymbolValues::Stmt(x)),
body.map_or(SymbolValues::None, SymbolValues::Stmt),
Some(name),
pretty_name,
)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ impl ExprTransformer {

/// Extract `empty_statics` map for final processing.
fn empty_statics_owned(&mut self) -> HashMap<InternedString, Expr> {
std::mem::replace(&mut self.empty_statics, HashMap::default())
std::mem::take(&mut self.empty_statics)
}

/// Add identifier to a transformed parameter if it's missing;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -48,8 +48,8 @@ impl NameTransformer {
}

// Don't tranform the `tag-` prefix of identifiers
let (prefix, name) = if orig_name.starts_with("tag-") {
(&orig_name[..4], &orig_name[4..])
let (prefix, name) = if let Some(tag) = orig_name.strip_prefix("tag-") {
("tag-", tag)
} else {
("", orig_name)
};
Expand Down Expand Up @@ -95,7 +95,8 @@ impl NameTransformer {
return new_name.replace(illegal, replacement);
}
}
return new_name;

new_name
}

let name = fix_name(name);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ impl NondetTransformer {

/// Extract `nondet_types` map for final processing.
pub fn nondet_types_owned(&mut self) -> HashMap<String, Type> {
std::mem::replace(&mut self.nondet_types, HashMap::default())
std::mem::take(&mut self.nondet_types)
}
}

Expand Down Expand Up @@ -87,7 +87,7 @@ impl Transformer for NondetTransformer {
let fields = transformed_typ.lookup_components(self.symbol_table()).unwrap().clone();
let transformed_values: Vec<_> = fields
.into_iter()
.zip(values.into_iter())
.zip(values.iter())
.map(
|(field, value)| {
if field.is_padding() { value.clone() } else { self.transform_expr(value) }
Expand Down
38 changes: 19 additions & 19 deletions cprover_bindings/src/goto_program/symtab_transformer/transformer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -70,8 +70,8 @@ pub trait Transformer: Sized {
}

/// Transforms an array type (`typ x[size]`)
fn transform_type_array(&mut self, typ: &Box<Type>, size: &u64) -> Type {
let transformed_typ = self.transform_type(typ.as_ref());
fn transform_type_array(&mut self, typ: &Type, size: &u64) -> Type {
let transformed_typ = self.transform_type(typ);
transformed_typ.array_of(*size)
}

Expand All @@ -81,8 +81,8 @@ pub trait Transformer: Sized {
}

/// Transforms a c bit field type (`typ x : width`)
fn transform_type_c_bit_field(&mut self, typ: &Box<Type>, width: &u64) -> Type {
let transformed_typ = self.transform_type(typ.as_ref());
fn transform_type_c_bit_field(&mut self, typ: &Type, width: &u64) -> Type {
let transformed_typ = self.transform_type(typ);
transformed_typ.as_bitfield(*width)
}

Expand All @@ -104,7 +104,7 @@ pub trait Transformer: Sized {
}

/// Transforms a function type (`return_type x(parameters)`)
fn transform_type_code(&mut self, parameters: &[Parameter], return_type: &Box<Type>) -> Type {
fn transform_type_code(&mut self, parameters: &[Parameter], return_type: &Type) -> Type {
let transformed_parameters =
parameters.iter().map(|parameter| self.transform_type_parameter(parameter)).collect();
let transformed_return_type = self.transform_type(return_type);
Expand All @@ -127,7 +127,7 @@ pub trait Transformer: Sized {
}

/// Transforms a flexible array type (`typ x[]`)
fn transform_type_flexible_array(&mut self, typ: &Box<Type>) -> Type {
fn transform_type_flexible_array(&mut self, typ: &Type) -> Type {
let transformed_typ = self.transform_type(typ);
Type::flexible_array_of(transformed_typ)
}
Expand All @@ -148,14 +148,14 @@ pub trait Transformer: Sized {
}

/// Transforms an infinite array type (`typ x[__CPROVER_infinity()]`)
fn transform_type_infinite_array(&mut self, typ: &Box<Type>) -> Type {
let transformed_typ = self.transform_type(typ.as_ref());
fn transform_type_infinite_array(&mut self, typ: &Type) -> Type {
let transformed_typ = self.transform_type(typ);
transformed_typ.infinite_array_of()
}

/// Transforms a pointer type (`typ*`)
fn transform_type_pointer(&mut self, typ: &Box<Type>) -> Type {
let transformed_typ = self.transform_type(typ.as_ref());
fn transform_type_pointer(&mut self, typ: &Type) -> Type {
let transformed_typ = self.transform_type(typ);
transformed_typ.to_pointer()
}

Expand Down Expand Up @@ -219,23 +219,23 @@ pub trait Transformer: Sized {
fn transform_type_variadic_code(
&mut self,
parameters: &[Parameter],
return_type: &Box<Type>,
return_type: &Type,
) -> Type {
let transformed_parameters =
parameters.iter().map(|parameter| self.transform_type_parameter(parameter)).collect();
let transformed_return_type = self.transform_type(return_type.as_ref());
let transformed_return_type = self.transform_type(return_type);
Type::variadic_code(transformed_parameters, transformed_return_type)
}

/// Transforms a vector type (`typ __attribute__((vector_size (size * sizeof(typ)))) var;`)
fn transform_type_vector(&mut self, typ: &Box<Type>, size: &u64) -> Type {
let transformed_typ = self.transform_type(typ.as_ref());
fn transform_type_vector(&mut self, typ: &Type, size: &u64) -> Type {
let transformed_typ = self.transform_type(typ);
Type::vector(transformed_typ, *size)
}

/// Transforms a type def (`typedef typ tag`)
fn transform_type_def(&mut self, tag: InternedString, typ: &Box<Type>) -> Type {
let transformed_typ = self.transform_type(typ.as_ref());
fn transform_type_def(&mut self, tag: InternedString, typ: &Type) -> Type {
let transformed_typ = self.transform_type(typ);
transformed_typ.to_typedef(tag)
}

Expand Down Expand Up @@ -279,7 +279,7 @@ pub trait Transformer: Sized {
ExprValue::UnOp { op, e } => self.transform_expr_un_op(typ, op, e),
ExprValue::Vector { elems } => self.transform_expr_vector(typ, elems),
}
.with_location(e.location().clone())
.with_location(*e.location())
}

/// Transforms a reference expr (`&self`)
Expand Down Expand Up @@ -450,7 +450,7 @@ pub trait Transformer: Sized {
transformed_typ
);
let transformed_values: Vec<_> =
values.into_iter().map(|value| self.transform_expr(value)).collect();
values.iter().map(|value| self.transform_expr(value)).collect();
Expr::struct_expr_from_padded_values(
transformed_typ,
transformed_values,
Expand Down Expand Up @@ -530,7 +530,7 @@ pub trait Transformer: Sized {
}
StmtBody::While { cond, body } => self.transform_stmt_while(cond, body),
}
.with_location(stmt.location().clone())
.with_location(*stmt.location())
}

/// Transforms an assign stmt (`lhs = rhs;`)
Expand Down
16 changes: 8 additions & 8 deletions cprover_bindings/src/goto_program/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ pub enum Type {
}

/// Machine dependent integers: `bool`, `char`, `int`, `size_t`, etc.
#[derive(PartialEq, Debug, Clone, Copy)]
#[derive(PartialEq, Eq, Debug, Clone, Copy)]
pub enum CIntType {
/// `bool`
Bool,
Expand Down Expand Up @@ -769,10 +769,10 @@ impl Type {

/// If typ.field_name exists in the symbol table, return Some(field.typ),
/// otherwise, return none.
pub fn lookup_field_type<'a, T: Into<InternedString>>(
pub fn lookup_field_type<T: Into<InternedString>>(
&self,
field_name: T,
st: &'a SymbolTable,
st: &SymbolTable,
) -> Option<Type> {
self.lookup_field(field_name, st).map(|f| f.typ())
}
Expand Down Expand Up @@ -1279,7 +1279,7 @@ impl Type {
Type::Array { typ, size } => {
format!("array_of_{}_{}", size, typ.to_identifier())
}
Type::Bool => format!("bool"),
Type::Bool => "bool".to_string(),
Type::CBitField { width, typ } => {
format!("cbitfield_of_{}_{}", width, typ.to_identifier())
}
Expand All @@ -1295,11 +1295,11 @@ impl Type {
let return_string = return_type.to_identifier();
format!("code_from_{}_to_{}", parameter_string, return_string)
}
Type::Constructor => format!("constructor"),
Type::Double => format!("double"),
Type::Empty => format!("empty"),
Type::Constructor => "constructor".to_string(),
Type::Double => "double".to_string(),
Type::Empty => "empty".to_string(),
Type::FlexibleArray { typ } => format!("flexarray_of_{}", typ.to_identifier()),
Type::Float => format!("float"),
Type::Float => "float".to_string(),
Type::IncompleteStruct { tag } => tag.to_string(),
Type::IncompleteUnion { tag } => tag.to_string(),
Type::InfiniteArray { typ } => {
Expand Down
8 changes: 4 additions & 4 deletions cprover_bindings/src/irep/irep.rs
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ impl Irep {
impl Irep {
pub fn with_location(self, l: &Location, mm: &MachineModel) -> Self {
if !l.is_none() {
self.with_named_sub(IrepId::CSourceLocation, l.to_irep(&mm))
self.with_named_sub(IrepId::CSourceLocation, l.to_irep(mm))
} else {
self
}
Expand Down Expand Up @@ -102,7 +102,7 @@ impl Irep {
}

pub fn just_id(id: IrepId) -> Irep {
Irep { id: id, sub: Vec::new(), named_sub: LinearMap::new() }
Irep { id, sub: Vec::new(), named_sub: LinearMap::new() }
}

pub fn just_int_id<T>(i: T) -> Irep
Expand All @@ -112,15 +112,15 @@ impl Irep {
Irep::just_id(IrepId::from_int(i))
}
pub fn just_named_sub(named_sub: LinearMap<IrepId, Irep>) -> Irep {
Irep { id: IrepId::EmptyString, sub: vec![], named_sub: named_sub }
Irep { id: IrepId::EmptyString, sub: vec![], named_sub }
}

pub fn just_string_id<T: Into<InternedString>>(s: T) -> Irep {
Irep::just_id(IrepId::from_string(s))
}

pub fn just_sub(sub: Vec<Irep>) -> Irep {
Irep { id: IrepId::EmptyString, sub: sub, named_sub: LinearMap::new() }
Irep { id: IrepId::EmptyString, sub, named_sub: LinearMap::new() }
}

pub fn nil() -> Irep {
Expand Down
Loading

0 comments on commit 12660b8

Please sign in to comment.