Skip to content

Commit

Permalink
Upgrade toolchain to 2/10 (#3883)
Browse files Browse the repository at this point in the history 
Upgrade toolchain to 2/10.

I **highly recommend** reviewing this PR commit-by-commit. The
description in each commit message links to the upstream PRs that
prompted those particular changes.

## Callouts
- 2/1 had a lot of formatting changes. I split the commits for that day
into formatting changes and functionality changes accordingly.
- 2/5 introduced a regression in our delayed UB instrumentation, so I
made a new fixme test. See #3881 for details.


## Culprit PRs:
rust-lang/rust#134424 
rust-lang/rust#130514
rust-lang/rust#135748
rust-lang/rust#136590
rust-lang/rust#135318
rust-lang/rust#135265

rust-lang/rust@bcb8565
rust-lang/rust#136471
rust-lang/rust#136645

Resolves #3863

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
  • Loading branch information
@carolynzech
carolynzech authored Feb 11, 2025
1 parent 8b2ec77 commit 81e9aa3
Show file tree
Hide file tree
Showing 35 changed files with 431 additions and 364 deletions.
11 changes: 7 additions & 4 deletions cprover_bindings/src/goto_program/expr.rs
View file
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
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
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
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

0 comments on commit 81e9aa3

Please sign in to comment.