Skip to content

Commit

Permalink
Update toolchain to 2024-09-24
Browse files Browse the repository at this point in the history 
Changes required due to:
- rust-lang/rust#130593 Sync from rustfmt

With the exception of changes to `rust-toolchain.toml` and
`rustfmt.toml` all changes were automatically created by running
`scripts/kani-fmt.sh`.
  • Loading branch information
@tautschnig
tautschnig committed Sep 24, 2024
1 parent 2755592 commit b74a220
Show file tree
Hide file tree
Showing 130 changed files with 500 additions and 546 deletions.
2 changes: 1 addition & 1 deletion cprover_bindings/src/cbmc_string.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,9 @@

use lazy_static::lazy_static;
use std::sync::Mutex;
use string_interner::StringInterner;
use string_interner::backend::StringBackend;
use string_interner::symbol::SymbolU32;
use string_interner::StringInterner;

/// This class implements an interner for Strings.
/// CBMC objects to have a large number of strings which refer to names: symbols, files, etc.
Expand Down
2 changes: 1 addition & 1 deletion cprover_bindings/src/env.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,8 @@
//! c.f. CBMC code [src/ansi-c/ansi_c_internal_additions.cpp].
//! One possible invocation of this insertion in CBMC can be found in \[ansi_c_languaget::parse\].
use super::goto_program::{Expr, Location, Symbol, SymbolTable, Type};
use super::MachineModel;
use super::goto_program::{Expr, Location, Symbol, SymbolTable, Type};
use num::bigint::BigInt;
fn int_constant<T>(name: &str, value: T) -> Symbol
where
Expand Down
11 changes: 4 additions & 7 deletions cprover_bindings/src/goto_program/expr.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -285,13 +285,10 @@ pub fn arithmetic_overflow_result_type(operand_type: Type) -> Type {
// give the struct the name "overflow_result_<type>", e.g.
// "overflow_result_Unsignedbv"
let name: InternedString = format!("overflow_result_{operand_type:?}").into();
Type::struct_type(
name,
vec![
DatatypeComponent::field(ARITH_OVERFLOW_RESULT_FIELD, operand_type),
DatatypeComponent::field(ARITH_OVERFLOW_OVERFLOWED_FIELD, Type::bool()),
],
)
Type::struct_type(name, vec![
DatatypeComponent::field(ARITH_OVERFLOW_RESULT_FIELD, operand_type),
DatatypeComponent::field(ARITH_OVERFLOW_OVERFLOWED_FIELD, Type::bool()),
])
}

///////////////////////////////////////////////////////////////////////////////////////////////
Expand Down
4 changes: 2 additions & 2 deletions cprover_bindings/src/goto_program/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,8 @@ mod typ;

pub use builtin::BuiltinFn;
pub use expr::{
arithmetic_overflow_result_type, ArithmeticOverflowResult, BinaryOperator, Expr, ExprValue,
SelfOperator, UnaryOperator, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD,
ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD, ArithmeticOverflowResult,
BinaryOperator, Expr, ExprValue, SelfOperator, UnaryOperator, arithmetic_overflow_result_type,
};
pub use location::Location;
pub use stmt::{Stmt, StmtBody, SwitchCase};
Expand Down
2 changes: 1 addition & 1 deletion cprover_bindings/src/goto_program/symbol_table.rs
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
use super::super::{env, MachineModel};
use super::super::{MachineModel, env};
use super::{BuiltinFn, FunctionContract, Stmt, Symbol};
use crate::InternedString;
use std::collections::BTreeMap;
Expand Down
10 changes: 5 additions & 5 deletions cprover_bindings/src/goto_program/typ.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT
use self::DatatypeComponent::*;
use self::Type::*;
use super::super::utils::{aggr_tag, max_int, min_int};
use super::super::MachineModel;
use super::super::utils::{aggr_tag, max_int, min_int};
use super::{Expr, SymbolTable};
use crate::cbmc_string::InternedString;
use std::collections::BTreeMap;
Expand Down Expand Up @@ -1598,10 +1598,10 @@ mod type_tests {
fn check_typedef_struct_properties() {
// Create a struct with a random field.
let struct_name: InternedString = "MyStruct".into();
let struct_type = Type::struct_type(
struct_name,
vec![DatatypeComponent::Field { name: "field".into(), typ: Double }],
);
let struct_type = Type::struct_type(struct_name, vec![DatatypeComponent::Field {
name: "field".into(),
typ: Double,
}]);
// Insert a field to the sym table to represent the struct field.
let mut sym_table = SymbolTable::new(machine_model_test_stub());
sym_table.ensure(struct_type.type_name().unwrap(), |_, name| {
Expand Down
4 changes: 2 additions & 2 deletions cprover_bindings/src/irep/goto_binary_serde.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1205,12 +1205,12 @@ mod sharing_stats {
mod tests {
use super::GotoBinarySerializer;
use super::IrepNumbering;
use crate::InternedString;
use crate::cbmc_string::InternString;
use crate::irep::goto_binary_serde::GotoBinaryDeserializer;
use crate::irep::Irep;
use crate::irep::IrepId;
use crate::irep::goto_binary_serde::GotoBinaryDeserializer;
use crate::linear_map;
use crate::InternedString;
use linear_map::LinearMap;
use std::io::BufWriter;
/// Utility function : creates a Irep representing a single symbol.
Expand Down
2 changes: 1 addition & 1 deletion cprover_bindings/src/irep/irep.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT
//! The actual `Irep` structure, and associated constructors, getters, and setters.
use super::super::goto_program::{Location, Type};
use super::super::MachineModel;
use super::super::goto_program::{Location, Type};
use super::{IrepId, ToIrep};
use crate::cbmc_string::InternedString;
use crate::linear_map;
Expand Down
230 changes: 113 additions & 117 deletions cprover_bindings/src/irep/serialize.rs
View file
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//! This crate implements irep serialization using serde Serializer.
use crate::irep::{Irep, IrepId, Symbol, SymbolTable};
use crate::InternedString;
use serde::ser::{SerializeMap, Serializer};
use crate::irep::{Irep, IrepId, Symbol, SymbolTable};
use serde::Serialize;
use serde::ser::{SerializeMap, Serializer};

impl Serialize for Irep {
fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
Expand Down Expand Up @@ -145,14 +145,16 @@ impl Serialize for Symbol {
#[cfg(test)]
mod test {
use super::*;
use serde_test::{assert_ser_tokens, Token};
use serde_test::{Token, assert_ser_tokens};
#[test]
fn serialize_irep() {
let irep = Irep::empty();
assert_ser_tokens(
&irep,
&[Token::Map { len: None }, Token::String("id"), Token::String("empty"), Token::MapEnd],
);
assert_ser_tokens(&irep, &[
Token::Map { len: None },
Token::String("id"),
Token::String("empty"),
Token::MapEnd,
]);
}

#[test]
Expand Down Expand Up @@ -187,80 +189,77 @@ mod test {
is_weak: false,
};
sym_table.insert(symbol);
assert_ser_tokens(
&sym_table,
&[
Token::Map { len: None },
Token::String("symbolTable"),
Token::Map { len: Some(1) },
Token::String("my_name"),
// symbol start
Token::Map { len: None },
// type irep
Token::String("type"),
Token::Map { len: None },
Token::String("id"),
Token::String("empty"),
Token::MapEnd,
// value irep
Token::String("value"),
Token::Map { len: None },
Token::String("id"),
Token::String("empty"),
Token::MapEnd,
// value locaton
Token::String("location"),
Token::Map { len: None },
Token::String("id"),
Token::String("empty"),
Token::MapEnd,
Token::String("name"),
Token::String("my_name"),
Token::String("module"),
Token::String(""),
Token::String("baseName"),
Token::String(""),
Token::String("prettyName"),
Token::String(""),
Token::String("mode"),
Token::String(""),
Token::String("isType"),
Token::Bool(false),
Token::String("isMacro"),
Token::Bool(false),
Token::String("isExported"),
Token::Bool(false),
Token::String("isInput"),
Token::Bool(false),
Token::String("isOutput"),
Token::Bool(false),
Token::String("isStateVar"),
Token::Bool(false),
Token::String("isProperty"),
Token::Bool(false),
Token::String("isStaticLifetime"),
Token::Bool(false),
Token::String("isThreadLocal"),
Token::Bool(false),
Token::String("isLvalue"),
Token::Bool(false),
Token::String("isFileLocal"),
Token::Bool(false),
Token::String("isExtern"),
Token::Bool(false),
Token::String("isVolatile"),
Token::Bool(false),
Token::String("isParameter"),
Token::Bool(false),
Token::String("isAuxiliary"),
Token::Bool(false),
Token::String("isWeak"),
Token::Bool(false),
Token::MapEnd,
Token::MapEnd,
Token::MapEnd,
],
);
assert_ser_tokens(&sym_table, &[
Token::Map { len: None },
Token::String("symbolTable"),
Token::Map { len: Some(1) },
Token::String("my_name"),
// symbol start
Token::Map { len: None },
// type irep
Token::String("type"),
Token::Map { len: None },
Token::String("id"),
Token::String("empty"),
Token::MapEnd,
// value irep
Token::String("value"),
Token::Map { len: None },
Token::String("id"),
Token::String("empty"),
Token::MapEnd,
// value locaton
Token::String("location"),
Token::Map { len: None },
Token::String("id"),
Token::String("empty"),
Token::MapEnd,
Token::String("name"),
Token::String("my_name"),
Token::String("module"),
Token::String(""),
Token::String("baseName"),
Token::String(""),
Token::String("prettyName"),
Token::String(""),
Token::String("mode"),
Token::String(""),
Token::String("isType"),
Token::Bool(false),
Token::String("isMacro"),
Token::Bool(false),
Token::String("isExported"),
Token::Bool(false),
Token::String("isInput"),
Token::Bool(false),
Token::String("isOutput"),
Token::Bool(false),
Token::String("isStateVar"),
Token::Bool(false),
Token::String("isProperty"),
Token::Bool(false),
Token::String("isStaticLifetime"),
Token::Bool(false),
Token::String("isThreadLocal"),
Token::Bool(false),
Token::String("isLvalue"),
Token::Bool(false),
Token::String("isFileLocal"),
Token::Bool(false),
Token::String("isExtern"),
Token::Bool(false),
Token::String("isVolatile"),
Token::Bool(false),
Token::String("isParameter"),
Token::Bool(false),
Token::String("isAuxiliary"),
Token::Bool(false),
Token::String("isWeak"),
Token::Bool(false),
Token::MapEnd,
Token::MapEnd,
Token::MapEnd,
]);
}

#[test]
Expand All @@ -269,41 +268,38 @@ mod test {
let one_irep = Irep::one();
let sub_irep = Irep::just_sub(vec![empty_irep.clone(), one_irep]);
let top_irep = Irep::just_sub(vec![sub_irep, empty_irep]);
assert_ser_tokens(
&top_irep,
&[
// top_irep
Token::Map { len: None },
Token::String("id"),
Token::String(""),
Token::String("sub"),
Token::Seq { len: Some(2) },
// sub_irep
Token::Map { len: None },
Token::String("id"),
Token::String(""),
Token::String("sub"),
Token::Seq { len: Some(2) },
// empty_irep
Token::Map { len: None },
Token::String("id"),
Token::String("empty"),
Token::MapEnd,
// one_irep
Token::Map { len: None },
Token::String("id"),
Token::String("1"),
Token::MapEnd,
Token::SeqEnd,
Token::MapEnd,
// empty_irep
Token::Map { len: None },
Token::String("id"),
Token::String("empty"),
Token::MapEnd,
Token::SeqEnd,
Token::MapEnd,
],
);
assert_ser_tokens(&top_irep, &[
// top_irep
Token::Map { len: None },
Token::String("id"),
Token::String(""),
Token::String("sub"),
Token::Seq { len: Some(2) },
// sub_irep
Token::Map { len: None },
Token::String("id"),
Token::String(""),
Token::String("sub"),
Token::Seq { len: Some(2) },
// empty_irep
Token::Map { len: None },
Token::String("id"),
Token::String("empty"),
Token::MapEnd,
// one_irep
Token::Map { len: None },
Token::String("id"),
Token::String("1"),
Token::MapEnd,
Token::SeqEnd,
Token::MapEnd,
// empty_irep
Token::Map { len: None },
Token::String("id"),
Token::String("empty"),
Token::MapEnd,
Token::SeqEnd,
Token::MapEnd,
]);
}
}
Loading

0 comments on commit b74a220

Please sign in to comment.