Skip to content

Commit 81e9aa3

Browse files
carolynzechcarolynzech
authored
Upgrade toolchain to 2/10 (#3883)
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.
1 parent 8b2ec77 commit 81e9aa3

35 files changed

+431
-364
lines changed

‎cprover_bindings/src/goto_program/expr.rs

+7-4
Original file line numberDiff line numberDiff line change
@@ -285,10 +285,13 @@ pub fn arithmetic_overflow_result_type(operand_type: Type) -> Type {
285285
// give the struct the name "overflow_result_<type>", e.g.
286286
// "overflow_result_Unsignedbv"
287287
let name: InternedString = format!("overflow_result_{operand_type:?}").into();
288-
Type::struct_type(name, vec![
289-
DatatypeComponent::field(ARITH_OVERFLOW_RESULT_FIELD, operand_type),
290-
DatatypeComponent::field(ARITH_OVERFLOW_OVERFLOWED_FIELD, Type::bool()),
291-
])
288+
Type::struct_type(
289+
name,
290+
vec![
291+
DatatypeComponent::field(ARITH_OVERFLOW_RESULT_FIELD, operand_type),
292+
DatatypeComponent::field(ARITH_OVERFLOW_OVERFLOWED_FIELD, Type::bool()),
293+
],
294+
)
292295
}
293296

294297
///////////////////////////////////////////////////////////////////////////////////////////////

‎cprover_bindings/src/goto_program/typ.rs

+4-4
Original file line numberDiff line numberDiff line change
@@ -1594,10 +1594,10 @@ mod type_tests {
15941594
fn check_typedef_struct_properties() {
15951595
// Create a struct with a random field.
15961596
let struct_name: InternedString = "MyStruct".into();
1597-
let struct_type = Type::struct_type(struct_name, vec![DatatypeComponent::Field {
1598-
name: "field".into(),
1599-
typ: Double,
1600-
}]);
1597+
let struct_type = Type::struct_type(
1598+
struct_name,
1599+
vec![DatatypeComponent::Field { name: "field".into(), typ: Double }],
1600+
);
16011601
// Insert a field to the sym table to represent the struct field.
16021602
let mut sym_table = SymbolTable::new(machine_model_test_stub());
16031603
sym_table.ensure(struct_type.type_name().unwrap(), |_, name| {

‎cprover_bindings/src/irep/serialize.rs

+114-110
Original file line numberDiff line numberDiff line change
@@ -149,12 +149,10 @@ mod test {
149149
#[test]
150150
fn serialize_irep() {
151151
let irep = Irep::empty();
152-
assert_ser_tokens(&irep, &[
153-
Token::Map { len: None },
154-
Token::String("id"),
155-
Token::String("empty"),
156-
Token::MapEnd,
157-
]);
152+
assert_ser_tokens(
153+
&irep,
154+
&[Token::Map { len: None }, Token::String("id"), Token::String("empty"), Token::MapEnd],
155+
);
158156
}
159157

160158
#[test]
@@ -189,77 +187,80 @@ mod test {
189187
is_weak: false,
190188
};
191189
sym_table.insert(symbol);
192-
assert_ser_tokens(&sym_table, &[
193-
Token::Map { len: None },
194-
Token::String("symbolTable"),
195-
Token::Map { len: Some(1) },
196-
Token::String("my_name"),
197-
// symbol start
198-
Token::Map { len: None },
199-
// type irep
200-
Token::String("type"),
201-
Token::Map { len: None },
202-
Token::String("id"),
203-
Token::String("empty"),
204-
Token::MapEnd,
205-
// value irep
206-
Token::String("value"),
207-
Token::Map { len: None },
208-
Token::String("id"),
209-
Token::String("empty"),
210-
Token::MapEnd,
211-
// value locaton
212-
Token::String("location"),
213-
Token::Map { len: None },
214-
Token::String("id"),
215-
Token::String("empty"),
216-
Token::MapEnd,
217-
Token::String("name"),
218-
Token::String("my_name"),
219-
Token::String("module"),
220-
Token::String(""),
221-
Token::String("baseName"),
222-
Token::String(""),
223-
Token::String("prettyName"),
224-
Token::String(""),
225-
Token::String("mode"),
226-
Token::String(""),
227-
Token::String("isType"),
228-
Token::Bool(false),
229-
Token::String("isMacro"),
230-
Token::Bool(false),
231-
Token::String("isExported"),
232-
Token::Bool(false),
233-
Token::String("isInput"),
234-
Token::Bool(false),
235-
Token::String("isOutput"),
236-
Token::Bool(false),
237-
Token::String("isStateVar"),
238-
Token::Bool(false),
239-
Token::String("isProperty"),
240-
Token::Bool(false),
241-
Token::String("isStaticLifetime"),
242-
Token::Bool(false),
243-
Token::String("isThreadLocal"),
244-
Token::Bool(false),
245-
Token::String("isLvalue"),
246-
Token::Bool(false),
247-
Token::String("isFileLocal"),
248-
Token::Bool(false),
249-
Token::String("isExtern"),
250-
Token::Bool(false),
251-
Token::String("isVolatile"),
252-
Token::Bool(false),
253-
Token::String("isParameter"),
254-
Token::Bool(false),
255-
Token::String("isAuxiliary"),
256-
Token::Bool(false),
257-
Token::String("isWeak"),
258-
Token::Bool(false),
259-
Token::MapEnd,
260-
Token::MapEnd,
261-
Token::MapEnd,
262-
]);
190+
assert_ser_tokens(
191+
&sym_table,
192+
&[
193+
Token::Map { len: None },
194+
Token::String("symbolTable"),
195+
Token::Map { len: Some(1) },
196+
Token::String("my_name"),
197+
// symbol start
198+
Token::Map { len: None },
199+
// type irep
200+
Token::String("type"),
201+
Token::Map { len: None },
202+
Token::String("id"),
203+
Token::String("empty"),
204+
Token::MapEnd,
205+
// value irep
206+
Token::String("value"),
207+
Token::Map { len: None },
208+
Token::String("id"),
209+
Token::String("empty"),
210+
Token::MapEnd,
211+
// value locaton
212+
Token::String("location"),
213+
Token::Map { len: None },
214+
Token::String("id"),
215+
Token::String("empty"),
216+
Token::MapEnd,
217+
Token::String("name"),
218+
Token::String("my_name"),
219+
Token::String("module"),
220+
Token::String(""),
221+
Token::String("baseName"),
222+
Token::String(""),
223+
Token::String("prettyName"),
224+
Token::String(""),
225+
Token::String("mode"),
226+
Token::String(""),
227+
Token::String("isType"),
228+
Token::Bool(false),
229+
Token::String("isMacro"),
230+
Token::Bool(false),
231+
Token::String("isExported"),
232+
Token::Bool(false),
233+
Token::String("isInput"),
234+
Token::Bool(false),
235+
Token::String("isOutput"),
236+
Token::Bool(false),
237+
Token::String("isStateVar"),
238+
Token::Bool(false),
239+
Token::String("isProperty"),
240+
Token::Bool(false),
241+
Token::String("isStaticLifetime"),
242+
Token::Bool(false),
243+
Token::String("isThreadLocal"),
244+
Token::Bool(false),
245+
Token::String("isLvalue"),
246+
Token::Bool(false),
247+
Token::String("isFileLocal"),
248+
Token::Bool(false),
249+
Token::String("isExtern"),
250+
Token::Bool(false),
251+
Token::String("isVolatile"),
252+
Token::Bool(false),
253+
Token::String("isParameter"),
254+
Token::Bool(false),
255+
Token::String("isAuxiliary"),
256+
Token::Bool(false),
257+
Token::String("isWeak"),
258+
Token::Bool(false),
259+
Token::MapEnd,
260+
Token::MapEnd,
261+
Token::MapEnd,
262+
],
263+
);
263264
}
264265

265266
#[test]
@@ -268,38 +269,41 @@ mod test {
268269
let one_irep = Irep::one();
269270
let sub_irep = Irep::just_sub(vec![empty_irep.clone(), one_irep]);
270271
let top_irep = Irep::just_sub(vec![sub_irep, empty_irep]);
271-
assert_ser_tokens(&top_irep, &[
272-
// top_irep
273-
Token::Map { len: None },
274-
Token::String("id"),
275-
Token::String(""),
276-
Token::String("sub"),
277-
Token::Seq { len: Some(2) },
278-
// sub_irep
279-
Token::Map { len: None },
280-
Token::String("id"),
281-
Token::String(""),
282-
Token::String("sub"),
283-
Token::Seq { len: Some(2) },
284-
// empty_irep
285-
Token::Map { len: None },
286-
Token::String("id"),
287-
Token::String("empty"),
288-
Token::MapEnd,
289-
// one_irep
290-
Token::Map { len: None },
291-
Token::String("id"),
292-
Token::String("1"),
293-
Token::MapEnd,
294-
Token::SeqEnd,
295-
Token::MapEnd,
296-
// empty_irep
297-
Token::Map { len: None },
298-
Token::String("id"),
299-
Token::String("empty"),
300-
Token::MapEnd,
301-
Token::SeqEnd,
302-
Token::MapEnd,
303-
]);
272+
assert_ser_tokens(
273+
&top_irep,
274+
&[
275+
// top_irep
276+
Token::Map { len: None },
277+
Token::String("id"),
278+
Token::String(""),
279+
Token::String("sub"),
280+
Token::Seq { len: Some(2) },
281+
// sub_irep
282+
Token::Map { len: None },
283+
Token::String("id"),
284+
Token::String(""),
285+
Token::String("sub"),
286+
Token::Seq { len: Some(2) },
287+
// empty_irep
288+
Token::Map { len: None },
289+
Token::String("id"),
290+
Token::String("empty"),
291+
Token::MapEnd,
292+
// one_irep
293+
Token::Map { len: None },
294+
Token::String("id"),
295+
Token::String("1"),
296+
Token::MapEnd,
297+
Token::SeqEnd,
298+
Token::MapEnd,
299+
// empty_irep
300+
Token::Map { len: None },
301+
Token::String("id"),
302+
Token::String("empty"),
303+
Token::MapEnd,
304+
Token::SeqEnd,
305+
Token::MapEnd,
306+
],
307+
);
304308
}
305309
}

‎cprover_bindings/src/irep/to_irep.rs

+33-34
Original file line numberDiff line numberDiff line change
@@ -273,12 +273,10 @@ impl ToIrep for ExprValue {
273273
)],
274274
}
275275
}
276-
ExprValue::FunctionCall { function, arguments } => {
277-
side_effect_irep(IrepId::FunctionCall, vec![
278-
function.to_irep(mm),
279-
arguments_irep(arguments.iter(), mm),
280-
])
281-
}
276+
ExprValue::FunctionCall { function, arguments } => side_effect_irep(
277+
IrepId::FunctionCall,
278+
vec![function.to_irep(mm), arguments_irep(arguments.iter(), mm)],
279+
),
282280
ExprValue::If { c, t, e } => Irep {
283281
id: IrepId::If,
284282
sub: vec![c.to_irep(mm), t.to_irep(mm), e.to_irep(mm)],
@@ -320,11 +318,10 @@ impl ToIrep for ExprValue {
320318
named_sub: linear_map![],
321319
},
322320
ExprValue::SelfOp { op, e } => side_effect_irep(op.to_irep_id(), vec![e.to_irep(mm)]),
323-
ExprValue::StatementExpression { statements: ops, location: loc } => {
324-
side_effect_irep(IrepId::StatementExpression, vec![
325-
Stmt::block(ops.to_vec(), *loc).to_irep(mm),
326-
])
327-
}
321+
ExprValue::StatementExpression { statements: ops, location: loc } => side_effect_irep(
322+
IrepId::StatementExpression,
323+
vec![Stmt::block(ops.to_vec(), *loc).to_irep(mm)],
324+
),
328325
ExprValue::StringConstant { s } => Irep {
329326
id: IrepId::StringConstant,
330327
sub: vec![],
@@ -491,10 +488,10 @@ impl ToIrep for StmtBody {
491488
StmtBody::Dead(symbol) => code_irep(IrepId::Dead, vec![symbol.to_irep(mm)]),
492489
StmtBody::Decl { lhs, value } => {
493490
if value.is_some() {
494-
code_irep(IrepId::Decl, vec![
495-
lhs.to_irep(mm),
496-
value.as_ref().unwrap().to_irep(mm),
497-
])
491+
code_irep(
492+
IrepId::Decl,
493+
vec![lhs.to_irep(mm), value.as_ref().unwrap().to_irep(mm)],
494+
)
498495
} else {
499496
code_irep(IrepId::Decl, vec![lhs.to_irep(mm)])
500497
}
@@ -507,19 +504,18 @@ impl ToIrep for StmtBody {
507504
.with_comment("deinit")
508505
}
509506
StmtBody::Expression(e) => code_irep(IrepId::Expression, vec![e.to_irep(mm)]),
510-
StmtBody::For { init, cond, update, body } => code_irep(IrepId::For, vec![
511-
init.to_irep(mm),
512-
cond.to_irep(mm),
513-
update.to_irep(mm),
514-
body.to_irep(mm),
515-
]),
516-
StmtBody::FunctionCall { lhs, function, arguments } => {
517-
code_irep(IrepId::FunctionCall, vec![
507+
StmtBody::For { init, cond, update, body } => code_irep(
508+
IrepId::For,
509+
vec![init.to_irep(mm), cond.to_irep(mm), update.to_irep(mm), body.to_irep(mm)],
510+
),
511+
StmtBody::FunctionCall { lhs, function, arguments } => code_irep(
512+
IrepId::FunctionCall,
513+
vec![
518514
lhs.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)),
519515
function.to_irep(mm),
520516
arguments_irep(arguments.iter(), mm),
521-
])
522-
}
517+
],
518+
),
523519
StmtBody::Goto { dest, loop_invariants } => {
524520
let stmt_goto = code_irep(IrepId::Goto, vec![])
525521
.with_named_sub(IrepId::Destination, Irep::just_string_id(dest.to_string()));
@@ -532,11 +528,14 @@ impl ToIrep for StmtBody {
532528
stmt_goto
533529
}
534530
}
535-
StmtBody::Ifthenelse { i, t, e } => code_irep(IrepId::Ifthenelse, vec![
536-
i.to_irep(mm),
537-
t.to_irep(mm),
538-
e.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)),
539-
]),
531+
StmtBody::Ifthenelse { i, t, e } => code_irep(
532+
IrepId::Ifthenelse,
533+
vec![
534+
i.to_irep(mm),
535+
t.to_irep(mm),
536+
e.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)),
537+
],
538+
),
540539
StmtBody::Label { label, body } => code_irep(IrepId::Label, vec![body.to_irep(mm)])
541540
.with_named_sub(IrepId::Label, Irep::just_string_id(label.to_string())),
542541
StmtBody::Return(e) => {
@@ -548,10 +547,10 @@ impl ToIrep for StmtBody {
548547
if default.is_some() {
549548
switch_arms.push(switch_default_irep(default.as_ref().unwrap(), mm));
550549
}
551-
code_irep(IrepId::Switch, vec![
552-
control.to_irep(mm),
553-
code_irep(IrepId::Block, switch_arms),
554-
])
550+
code_irep(
551+
IrepId::Switch,
552+
vec![control.to_irep(mm), code_irep(IrepId::Block, switch_arms)],
553+
)
555554
}
556555
StmtBody::While { cond, body } => {
557556
code_irep(IrepId::While, vec![cond.to_irep(mm), body.to_irep(mm)])

0 commit comments

Comments
 (0)