Skip to content

Commit 4fdf604

Browse files
gilthogiltho
authored
Refactor machine_model to make-it non-oop (rust-lang#1291)
1 parent 42a88bc commit 4fdf604

File tree

8 files changed

+105
-237
lines changed

8 files changed

+105
-237
lines changed

‎cprover_bindings/src/env.rs

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -34,31 +34,31 @@ fn string_constant(name: &str, value: &str) -> Symbol {
3434

3535
pub fn machine_model_symbols(mm: &MachineModel) -> Vec<Symbol> {
3636
vec![
37-
string_constant("__CPROVER_architecture_arch", mm.architecture()),
38-
int_constant_from_bool("__CPROVER_architecture_NULL_is_zero", mm.null_is_zero()),
39-
int_constant("__CPROVER_architecture_alignment", mm.alignment()),
40-
int_constant("__CPROVER_architecture_bool_width", mm.bool_width()),
41-
int_constant_from_bool("__CPROVER_architecture_char_is_unsigned", mm.char_is_unsigned()),
42-
int_constant("__CPROVER_architecture_char_width", mm.char_width()),
43-
int_constant("__CPROVER_architecture_double_width", mm.double_width()),
37+
string_constant("__CPROVER_architecture_arch", &mm.architecture),
38+
int_constant_from_bool("__CPROVER_architecture_NULL_is_zero", mm.null_is_zero),
39+
int_constant("__CPROVER_architecture_alignment", mm.alignment),
40+
int_constant("__CPROVER_architecture_bool_width", mm.bool_width),
41+
int_constant_from_bool("__CPROVER_architecture_char_is_unsigned", mm.char_is_unsigned),
42+
int_constant("__CPROVER_architecture_char_width", mm.char_width),
43+
int_constant("__CPROVER_architecture_double_width", mm.double_width),
4444
// c.f. https://github.com/diffblue/cbmc/blob/develop/src/util/config.h
4545
// the numbers are from endiannesst
46-
int_constant("__CPROVER_architecture_endianness", if mm.is_big_endian() { 2 } else { 1 }),
47-
int_constant("__CPROVER_architecture_int_width", mm.int_width()),
48-
int_constant("__CPROVER_architecture_long_double_width", mm.long_double_width()),
49-
int_constant("__CPROVER_architecture_long_int_width", mm.long_int_width()),
50-
int_constant("__CPROVER_architecture_long_long_int_width", mm.long_long_int_width()),
51-
int_constant("__CPROVER_architecture_memory_operand_size", mm.memory_operand_size()),
52-
int_constant("__CPROVER_architecture_pointer_width", mm.pointer_width()),
53-
int_constant("__CPROVER_architecture_short_int_width", mm.short_int_width()),
54-
int_constant("__CPROVER_architecture_single_width", mm.single_width()),
46+
int_constant("__CPROVER_architecture_endianness", if mm.is_big_endian { 2 } else { 1 }),
47+
int_constant("__CPROVER_architecture_int_width", mm.int_width),
48+
int_constant("__CPROVER_architecture_long_double_width", mm.long_double_width),
49+
int_constant("__CPROVER_architecture_long_int_width", mm.long_int_width),
50+
int_constant("__CPROVER_architecture_long_long_int_width", mm.long_long_int_width),
51+
int_constant("__CPROVER_architecture_memory_operand_size", mm.memory_operand_size),
52+
int_constant("__CPROVER_architecture_pointer_width", mm.pointer_width),
53+
int_constant("__CPROVER_architecture_short_int_width", mm.short_int_width),
54+
int_constant("__CPROVER_architecture_single_width", mm.single_width),
5555
int_constant_from_bool(
5656
"__CPROVER_architecture_wchar_t_is_unsigned",
57-
mm.wchar_t_is_unsigned(),
57+
mm.wchar_t_is_unsigned,
5858
),
59-
int_constant("__CPROVER_architecture_wchar_t_width", mm.wchar_t_width()),
60-
int_constant("__CPROVER_architecture_word_size", mm.word_size()),
61-
int_constant("__CPROVER_rounding_mode", mm.rounding_mode()),
59+
int_constant("__CPROVER_architecture_wchar_t_width", mm.wchar_t_width),
60+
int_constant("__CPROVER_architecture_word_size", mm.word_size),
61+
int_constant("__CPROVER_rounding_mode", mm.rounding_mode),
6262
]
6363
}
6464

‎cprover_bindings/src/goto_program/typ.rs

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -229,11 +229,11 @@ impl Parameter {
229229
impl CIntType {
230230
pub fn sizeof_in_bits(&self, st: &SymbolTable) -> u64 {
231231
match self {
232-
CIntType::Bool => st.machine_model().bool_width(),
233-
CIntType::Char => st.machine_model().char_width(),
234-
CIntType::Int => st.machine_model().int_width(),
235-
CIntType::SizeT => st.machine_model().pointer_width(),
236-
CIntType::SSizeT => st.machine_model().pointer_width(),
232+
CIntType::Bool => st.machine_model().bool_width,
233+
CIntType::Char => st.machine_model().char_width,
234+
CIntType::Int => st.machine_model().int_width,
235+
CIntType::SizeT => st.machine_model().pointer_width,
236+
CIntType::SSizeT => st.machine_model().pointer_width,
237237
}
238238
}
239239
}
@@ -282,11 +282,11 @@ impl Type {
282282
let concrete = self.unwrap_typedef();
283283
match concrete {
284284
CInteger(CIntType::SizeT) | CInteger(CIntType::SSizeT) | Pointer { .. } => {
285-
Some(mm.pointer_width())
285+
Some(mm.pointer_width)
286286
}
287-
CInteger(CIntType::Bool) => Some(mm.bool_width()),
288-
CInteger(CIntType::Char) => Some(mm.char_width()),
289-
CInteger(CIntType::Int) => Some(mm.int_width()),
287+
CInteger(CIntType::Bool) => Some(mm.bool_width),
288+
CInteger(CIntType::Char) => Some(mm.char_width),
289+
CInteger(CIntType::Int) => Some(mm.int_width),
290290
Signedbv { width } | Unsignedbv { width } => Some(*width),
291291
_ => None,
292292
}
@@ -308,7 +308,7 @@ impl Type {
308308

309309
pub fn sizeof(&self, st: &SymbolTable) -> u64 {
310310
let bits = self.sizeof_in_bits(st);
311-
let char_width = st.machine_model().char_width();
311+
let char_width = st.machine_model().char_width;
312312
assert_eq!(0, bits % char_width);
313313
bits / char_width
314314
}
@@ -337,14 +337,14 @@ impl Type {
337337
// FnDef case in layout_raw_uncached, compiler/rustc_middle/src/ty/layout.rs
338338
Code { .. } => 0,
339339
Constructor => unreachable!("Constructor doesn't have a sizeof"),
340-
Double => st.machine_model().double_width(),
340+
Double => st.machine_model().double_width,
341341
Empty => 0,
342342
FlexibleArray { .. } => 0,
343-
Float => st.machine_model().float_width(),
343+
Float => st.machine_model().float_width,
344344
IncompleteStruct { .. } => unreachable!("IncompleteStruct doesn't have a sizeof"),
345345
IncompleteUnion { .. } => unreachable!("IncompleteUnion doesn't have a sizeof"),
346346
InfiniteArray { .. } => unreachable!("InfiniteArray doesn't have a sizeof"),
347-
Pointer { .. } => st.machine_model().pointer_width(),
347+
Pointer { .. } => st.machine_model().pointer_width,
348348
Signedbv { width } => *width,
349349
Struct { components, .. } => {
350350
components.iter().map(|x| x.typ().sizeof_in_bits(st)).sum()
@@ -618,7 +618,7 @@ impl Type {
618618
let concrete = self.unwrap_typedef();
619619
match concrete {
620620
CInteger(CIntType::Int) | CInteger(CIntType::SSizeT) | Signedbv { .. } => true,
621-
CInteger(CIntType::Char) => !mm.char_is_unsigned(),
621+
CInteger(CIntType::Char) => !mm.char_is_unsigned,
622622
_ => false,
623623
}
624624
}
@@ -680,7 +680,7 @@ impl Type {
680680
let concrete = self.unwrap_typedef();
681681
match concrete {
682682
CInteger(CIntType::Bool) | CInteger(CIntType::SizeT) | Unsignedbv { .. } => true,
683-
CInteger(CIntType::Char) => mm.char_is_unsigned(),
683+
CInteger(CIntType::Char) => mm.char_is_unsigned,
684684
_ => false,
685685
}
686686
}

‎cprover_bindings/src/irep/to_irep.rs

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -185,7 +185,7 @@ impl ToIrep for ExprValue {
185185
)],
186186
},
187187
ExprValue::ByteExtract { e, offset } => Irep {
188-
id: if mm.is_big_endian() {
188+
id: if mm.is_big_endian {
189189
IrepId::ByteExtractBigEndian
190190
} else {
191191
IrepId::ByteExtractLittleEndian
@@ -198,7 +198,7 @@ impl ToIrep for ExprValue {
198198
sub: vec![],
199199
named_sub: linear_map![(
200200
IrepId::Value,
201-
Irep::just_bitpattern_id(if *i { 1u8 } else { 0 }, mm.bool_width(), false)
201+
Irep::just_bitpattern_id(if *i { 1u8 } else { 0 }, mm.bool_width, false)
202202
)],
203203
},
204204
ExprValue::Dereference(e) => {
@@ -212,7 +212,7 @@ impl ToIrep for ExprValue {
212212
sub: vec![],
213213
named_sub: linear_map![(
214214
IrepId::Value,
215-
Irep::just_bitpattern_id(c, mm.double_width(), false)
215+
Irep::just_bitpattern_id(c, mm.double_width, false)
216216
)],
217217
}
218218
}
@@ -223,7 +223,7 @@ impl ToIrep for ExprValue {
223223
sub: vec![],
224224
named_sub: linear_map![(
225225
IrepId::Value,
226-
Irep::just_bitpattern_id(c, mm.float_width(), false)
226+
Irep::just_bitpattern_id(c, mm.float_width, false)
227227
)],
228228
}
229229
}
@@ -263,7 +263,7 @@ impl ToIrep for ExprValue {
263263
sub: vec![],
264264
named_sub: linear_map![(
265265
IrepId::Value,
266-
Irep::just_bitpattern_id(*i, mm.pointer_width(), false)
266+
Irep::just_bitpattern_id(*i, mm.pointer_width, false)
267267
)],
268268
},
269269
ExprValue::SelfOp { op, e } => side_effect_irep(op.to_irep_id(), vec![e.to_irep(mm)]),
@@ -555,27 +555,27 @@ impl ToIrep for Type {
555555
Type::CInteger(CIntType::Bool) => Irep {
556556
id: IrepId::CBool,
557557
sub: vec![],
558-
named_sub: linear_map![(IrepId::Width, Irep::just_int_id(mm.bool_width()))],
558+
named_sub: linear_map![(IrepId::Width, Irep::just_int_id(mm.bool_width))],
559559
},
560560
Type::CInteger(CIntType::Char) => Irep {
561-
id: if mm.char_is_unsigned() { IrepId::Unsignedbv } else { IrepId::Signedbv },
561+
id: if mm.char_is_unsigned { IrepId::Unsignedbv } else { IrepId::Signedbv },
562562
sub: vec![],
563-
named_sub: linear_map![(IrepId::Width, Irep::just_int_id(mm.char_width()),)],
563+
named_sub: linear_map![(IrepId::Width, Irep::just_int_id(mm.char_width),)],
564564
},
565565
Type::CInteger(CIntType::Int) => Irep {
566566
id: IrepId::Signedbv,
567567
sub: vec![],
568-
named_sub: linear_map![(IrepId::Width, Irep::just_int_id(mm.int_width()),)],
568+
named_sub: linear_map![(IrepId::Width, Irep::just_int_id(mm.int_width),)],
569569
},
570570
Type::CInteger(CIntType::SizeT) => Irep {
571571
id: IrepId::Unsignedbv,
572572
sub: vec![],
573-
named_sub: linear_map![(IrepId::Width, Irep::just_int_id(mm.pointer_width()),)],
573+
named_sub: linear_map![(IrepId::Width, Irep::just_int_id(mm.pointer_width),)],
574574
},
575575
Type::CInteger(CIntType::SSizeT) => Irep {
576576
id: IrepId::Signedbv,
577577
sub: vec![],
578-
named_sub: linear_map![(IrepId::Width, Irep::just_int_id(mm.pointer_width()),)],
578+
named_sub: linear_map![(IrepId::Width, Irep::just_int_id(mm.pointer_width),)],
579579
},
580580
Type::Code { parameters, return_type } => Irep {
581581
id: IrepId::Code,
@@ -645,7 +645,7 @@ impl ToIrep for Type {
645645
Type::Pointer { typ } => Irep {
646646
id: IrepId::Pointer,
647647
sub: vec![typ.to_irep(mm)],
648-
named_sub: linear_map![(IrepId::Width, Irep::just_int_id(mm.pointer_width()),)],
648+
named_sub: linear_map![(IrepId::Width, Irep::just_int_id(mm.pointer_width),)],
649649
},
650650
Type::Signedbv { width } => Irep {
651651
id: IrepId::Signedbv,

0 commit comments

Comments
 (0)