Skip to content

Commit 5cf5b8c

Browse files
zhassan-awszhassan-aws
committed
Revert "Upgrade toolchain to 2/10 (model-checking#3883)"
This reverts commit 81e9aa3.
1 parent 8d29d3a commit 5cf5b8c

File tree

32 files changed

+339
-404
lines changed

32 files changed

+339
-404
lines changed

‎cprover_bindings/src/goto_program/expr.rs

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

298295
///////////////////////////////////////////////////////////////////////////////////////////////

‎cprover_bindings/src/goto_program/typ.rs

Lines changed: 4 additions & 4 deletions
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(
1598-
struct_name,
1599-
vec![DatatypeComponent::Field { name: "field".into(), typ: Double }],
1600-
);
1597+
let struct_type = Type::struct_type(struct_name, vec![DatatypeComponent::Field {
1598+
name: "field".into(),
1599+
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

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

158160
#[test]
@@ -187,80 +189,77 @@ mod test {
187189
is_weak: false,
188190
};
189191
sym_table.insert(symbol);
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-
);
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+
]);
264263
}
265264

266265
#[test]
@@ -269,41 +268,38 @@ mod test {
269268
let one_irep = Irep::one();
270269
let sub_irep = Irep::just_sub(vec![empty_irep.clone(), one_irep]);
271270
let top_irep = Irep::just_sub(vec![sub_irep, empty_irep]);
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-
);
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+
]);
308304
}
309305
}

‎cprover_bindings/src/irep/to_irep.rs

Lines changed: 34 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -274,10 +274,12 @@ impl ToIrep for ExprValue {
274274
)],
275275
}
276276
}
277-
ExprValue::FunctionCall { function, arguments } => side_effect_irep(
278-
IrepId::FunctionCall,
279-
vec![function.to_irep(mm), arguments_irep(arguments.iter(), mm)],
280-
),
277+
ExprValue::FunctionCall { function, arguments } => {
278+
side_effect_irep(IrepId::FunctionCall, vec![
279+
function.to_irep(mm),
280+
arguments_irep(arguments.iter(), mm),
281+
])
282+
}
281283
ExprValue::If { c, t, e } => Irep {
282284
id: IrepId::If,
283285
sub: vec![c.to_irep(mm), t.to_irep(mm), e.to_irep(mm)],
@@ -319,10 +321,11 @@ impl ToIrep for ExprValue {
319321
named_sub: linear_map![],
320322
},
321323
ExprValue::SelfOp { op, e } => side_effect_irep(op.to_irep_id(), vec![e.to_irep(mm)]),
322-
ExprValue::StatementExpression { statements: ops, location: loc } => side_effect_irep(
323-
IrepId::StatementExpression,
324-
vec![Stmt::block(ops.to_vec(), *loc).to_irep(mm)],
325-
),
324+
ExprValue::StatementExpression { statements: ops, location: loc } => {
325+
side_effect_irep(IrepId::StatementExpression, vec![
326+
Stmt::block(ops.to_vec(), *loc).to_irep(mm),
327+
])
328+
}
326329
ExprValue::StringConstant { s } => Irep {
327330
id: IrepId::StringConstant,
328331
sub: vec![],
@@ -489,10 +492,10 @@ impl ToIrep for StmtBody {
489492
StmtBody::Dead(symbol) => code_irep(IrepId::Dead, vec![symbol.to_irep(mm)]),
490493
StmtBody::Decl { lhs, value } => {
491494
if value.is_some() {
492-
code_irep(
493-
IrepId::Decl,
494-
vec![lhs.to_irep(mm), value.as_ref().unwrap().to_irep(mm)],
495-
)
495+
code_irep(IrepId::Decl, vec![
496+
lhs.to_irep(mm),
497+
value.as_ref().unwrap().to_irep(mm),
498+
])
496499
} else {
497500
code_irep(IrepId::Decl, vec![lhs.to_irep(mm)])
498501
}
@@ -505,18 +508,19 @@ impl ToIrep for StmtBody {
505508
.with_comment("deinit")
506509
}
507510
StmtBody::Expression(e) => code_irep(IrepId::Expression, vec![e.to_irep(mm)]),
508-
StmtBody::For { init, cond, update, body } => code_irep(
509-
IrepId::For,
510-
vec![init.to_irep(mm), cond.to_irep(mm), update.to_irep(mm), body.to_irep(mm)],
511-
),
512-
StmtBody::FunctionCall { lhs, function, arguments } => code_irep(
513-
IrepId::FunctionCall,
514-
vec![
511+
StmtBody::For { init, cond, update, body } => code_irep(IrepId::For, vec![
512+
init.to_irep(mm),
513+
cond.to_irep(mm),
514+
update.to_irep(mm),
515+
body.to_irep(mm),
516+
]),
517+
StmtBody::FunctionCall { lhs, function, arguments } => {
518+
code_irep(IrepId::FunctionCall, vec![
515519
lhs.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)),
516520
function.to_irep(mm),
517521
arguments_irep(arguments.iter(), mm),
518-
],
519-
),
522+
])
523+
}
520524
StmtBody::Goto { dest, loop_invariants } => {
521525
let stmt_goto = code_irep(IrepId::Goto, vec![])
522526
.with_named_sub(IrepId::Destination, Irep::just_string_id(dest.to_string()));
@@ -529,14 +533,11 @@ impl ToIrep for StmtBody {
529533
stmt_goto
530534
}
531535
}
532-
StmtBody::Ifthenelse { i, t, e } => code_irep(
533-
IrepId::Ifthenelse,
534-
vec![
535-
i.to_irep(mm),
536-
t.to_irep(mm),
537-
e.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)),
538-
],
539-
),
536+
StmtBody::Ifthenelse { i, t, e } => code_irep(IrepId::Ifthenelse, vec![
537+
i.to_irep(mm),
538+
t.to_irep(mm),
539+
e.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)),
540+
]),
540541
StmtBody::Label { label, body } => code_irep(IrepId::Label, vec![body.to_irep(mm)])
541542
.with_named_sub(IrepId::Label, Irep::just_string_id(label.to_string())),
542543
StmtBody::Return(e) => {
@@ -548,10 +549,10 @@ impl ToIrep for StmtBody {
548549
if default.is_some() {
549550
switch_arms.push(switch_default_irep(default.as_ref().unwrap(), mm));
550551
}
551-
code_irep(
552-
IrepId::Switch,
553-
vec![control.to_irep(mm), code_irep(IrepId::Block, switch_arms)],
554-
)
552+
code_irep(IrepId::Switch, vec![
553+
control.to_irep(mm),
554+
code_irep(IrepId::Block, switch_arms),
555+
])
555556
}
556557
StmtBody::While { cond, body } => {
557558
code_irep(IrepId::While, vec![cond.to_irep(mm), body.to_irep(mm)])

0 commit comments

Comments
 (0)