Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Update toolchain to 2024-09-23 #3544

Merged
merged 3 commits into from
Sep 24, 2024
Merged

Update toolchain to 2024-09-23 #3544

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
b74a220
Update toolchain to 2024-09-24
tautschnig Sep 23, 2024
7fbbc48
Silence warnings about mutable reference to mutable static
tautschnig Sep 24, 2024
0605e85
Toolchain of 24th is ICEs in doc build
tautschnig Sep 24, 2024
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
2 changes: 1 addition & 1 deletion cprover_bindings/src/cbmc_string.rs
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Loading