Skip to content
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

Upgrade toolchain to 2/10 #3883

Merged
merged 10 commits into from
Feb 11, 2025
Merged

Upgrade toolchain to 2/10 #3883

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
5b98755
Update toolchain to 1/29
carolynzech Feb 7, 2025
cc35317
Update toolchain to 2/1 - functionality changes
carolynzech Feb 8, 2025
a287dee
Update toolchain to 2/1 - formatting changes only
carolynzech Feb 8, 2025
028b235
Update toolchain to 2/2
carolynzech Feb 8, 2025
318a4e6
Update toolchain to 2/5
carolynzech Feb 8, 2025
437ed4f
Upgrade toolchain to 2/6
carolynzech Feb 9, 2025
4cb50ee
Update toolchain to 2/7
carolynzech Feb 9, 2025
90ddd72
Upgrade toolchain to 2/8
carolynzech Feb 9, 2025
b972a5b
Upgrade toolchain to 2/10
carolynzech Feb 10, 2025
7eb5e89
Add comment about len()
carolynzech Feb 11, 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
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
Loading