Skip to content

[DO NOT MERGE] Use stable 1.85.1 release #3960

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

Closed
wants to merge 6 commits into from
Closed

[DO NOT MERGE] Use stable 1.85.1 release #3960

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
29c2c88
Switch to 1.85.1 channel and use RUSTC_BOOTSTRAP
zhassan-aws Mar 26, 2025
a491cd0
Update formatting script to remove unstable-features
zhassan-aws Mar 26, 2025
9250546
Add feature
zhassan-aws Mar 26, 2025
0bc4755
Formatting changes
zhassan-aws Mar 26, 2025
b72d230
Update tests
zhassan-aws Mar 26, 2025
901db00
Address comments
zhassan-aws Mar 27, 2025
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: 2 additions & 0 deletions .cargo/config.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,8 @@ KANI_SYSROOT ={value = "target/kani", relative = true}
KANI_BUILD_LIBS ={value = "target/build-libs", relative = true}
# Build Kani library without `build-std`.
KANI_LEGACY_LIBS ={value = "target/legacy-libs", relative = true}
# This is only required for stable but is a no-op for nightly channels
RUSTC_BOOTSTRAP = "1"

[target.'cfg(all())']
rustflags = [ # Global lints/warnings. Need to use underscore instead of -.
Expand Down
11 changes: 7 additions & 4 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,10 +285,13 @@ 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
8 changes: 4 additions & 4 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 @@ -1594,10 +1594,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
224 changes: 114 additions & 110 deletions cprover_bindings/src/irep/serialize.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -149,12 +149,10 @@ mod test {
#[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 @@ -189,77 +187,80 @@ 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 @@ -268,38 +269,41 @@ 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,
],
);
}
}
67 changes: 33 additions & 34 deletions cprover_bindings/src/irep/to_irep.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -273,12 +273,10 @@ impl ToIrep for ExprValue {
)],
}
}
ExprValue::FunctionCall { function, arguments } => {
side_effect_irep(IrepId::FunctionCall, vec![
function.to_irep(mm),
arguments_irep(arguments.iter(), mm),
])
}
ExprValue::FunctionCall { function, arguments } => side_effect_irep(
IrepId::FunctionCall,
vec![function.to_irep(mm), arguments_irep(arguments.iter(), mm)],
),
ExprValue::If { c, t, e } => Irep {
id: IrepId::If,
sub: vec![c.to_irep(mm), t.to_irep(mm), e.to_irep(mm)],
Expand Down Expand Up @@ -320,11 +318,10 @@ impl ToIrep for ExprValue {
named_sub: linear_map![],
},
ExprValue::SelfOp { op, e } => side_effect_irep(op.to_irep_id(), vec![e.to_irep(mm)]),
ExprValue::StatementExpression { statements: ops, location: loc } => {
side_effect_irep(IrepId::StatementExpression, vec![
Stmt::block(ops.to_vec(), *loc).to_irep(mm),
])
}
ExprValue::StatementExpression { statements: ops, location: loc } => side_effect_irep(
IrepId::StatementExpression,
vec![Stmt::block(ops.to_vec(), *loc).to_irep(mm)],
),
ExprValue::StringConstant { s } => Irep {
id: IrepId::StringConstant,
sub: vec![],
Expand Down Expand Up @@ -491,10 +488,10 @@ impl ToIrep for StmtBody {
StmtBody::Dead(symbol) => code_irep(IrepId::Dead, vec![symbol.to_irep(mm)]),
StmtBody::Decl { lhs, value } => {
if value.is_some() {
code_irep(IrepId::Decl, vec![
lhs.to_irep(mm),
value.as_ref().unwrap().to_irep(mm),
])
code_irep(
IrepId::Decl,
vec![lhs.to_irep(mm), value.as_ref().unwrap().to_irep(mm)],
)
} else {
code_irep(IrepId::Decl, vec![lhs.to_irep(mm)])
}
Expand All @@ -507,19 +504,18 @@ impl ToIrep for StmtBody {
.with_comment("deinit")
}
StmtBody::Expression(e) => code_irep(IrepId::Expression, vec![e.to_irep(mm)]),
StmtBody::For { init, cond, update, body } => code_irep(IrepId::For, vec![
init.to_irep(mm),
cond.to_irep(mm),
update.to_irep(mm),
body.to_irep(mm),
]),
StmtBody::FunctionCall { lhs, function, arguments } => {
code_irep(IrepId::FunctionCall, vec![
StmtBody::For { init, cond, update, body } => code_irep(
IrepId::For,
vec![init.to_irep(mm), cond.to_irep(mm), update.to_irep(mm), body.to_irep(mm)],
),
StmtBody::FunctionCall { lhs, function, arguments } => code_irep(
IrepId::FunctionCall,
vec![
lhs.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)),
function.to_irep(mm),
arguments_irep(arguments.iter(), mm),
])
}
],
),
StmtBody::Goto { dest, loop_invariants } => {
let stmt_goto = code_irep(IrepId::Goto, vec![])
.with_named_sub(IrepId::Destination, Irep::just_string_id(dest.to_string()));
Expand All @@ -532,11 +528,14 @@ impl ToIrep for StmtBody {
stmt_goto
}
}
StmtBody::Ifthenelse { i, t, e } => code_irep(IrepId::Ifthenelse, vec![
i.to_irep(mm),
t.to_irep(mm),
e.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)),
]),
StmtBody::Ifthenelse { i, t, e } => code_irep(
IrepId::Ifthenelse,
vec![
i.to_irep(mm),
t.to_irep(mm),
e.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)),
],
),
StmtBody::Label { label, body } => code_irep(IrepId::Label, vec![body.to_irep(mm)])
.with_named_sub(IrepId::Label, Irep::just_string_id(label.to_string())),
StmtBody::Return(e) => {
Expand All @@ -548,10 +547,10 @@ impl ToIrep for StmtBody {
if default.is_some() {
switch_arms.push(switch_default_irep(default.as_ref().unwrap(), mm));
}
code_irep(IrepId::Switch, vec![
control.to_irep(mm),
code_irep(IrepId::Block, switch_arms),
])
code_irep(
IrepId::Switch,
vec![control.to_irep(mm), code_irep(IrepId::Block, switch_arms)],
)
}
StmtBody::While { cond, body } => {
code_irep(IrepId::While, vec![cond.to_irep(mm), body.to_irep(mm)])
Expand Down
Loading