Skip to content

Commit a41ce86

Browse files
zhassan-awszhassan-aws
committed
Additional changes needed for Kani to work with the stable release
The number of changes needed will go down with every new Rust release as some of them were already made in main, and so will be brought in as we merge changes from main into the stable branch.
1 parent e72e75b commit a41ce86

File tree

20 files changed

+365
-314
lines changed

20 files changed

+365
-314
lines changed

‎.cargo/config.toml‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,8 @@ KANI_SYSROOT ={value = "target/kani", relative = true}
2020
KANI_BUILD_LIBS ={value = "target/build-libs", relative = true}
2121
# Build Kani library without `build-std`.
2222
KANI_LEGACY_LIBS ={value = "target/legacy-libs", relative = true}
23+
# This is only required for stable but is a no-op for nightly channels
24+
RUSTC_BOOTSTRAP = "1"
2325

2426
[target.'cfg(all())']
2527
rustflags = [ # Global lints/warnings. Need to use underscore instead of -.

‎cprover_bindings/src/goto_program/expr.rs‎

Lines changed: 7 additions & 4 deletions
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‎

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(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‎

Lines changed: 114 additions & 110 deletions
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‎

Lines changed: 33 additions & 34 deletions
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)