Skip to content

Commit e9ffdfa

Browse files
danielsntedinski
authored andcommitted
Add sanity checks when creating function parameter type (rust-lang#532)
1 parent 743f6f3 commit e9ffdfa

File tree

6 files changed

+53
-28
lines changed

6 files changed

+53
-28
lines changed

compiler/cbmc/src/goto_program/symbol.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -289,7 +289,7 @@ impl Symbol {
289289
impl Symbol {
290290
/// Makes a formal function parameter from a symbol.
291291
pub fn to_function_parameter(&self) -> Parameter {
292-
Type::parameter(Some(self.name.to_string()), self.base_name.clone(), self.typ.clone())
292+
self.typ.clone().as_parameter(Some(self.name.to_string()), self.base_name.clone())
293293
}
294294

295295
/// Makes an expression from a symbol.

compiler/cbmc/src/goto_program/symtab_transformer/gen_c_transformer/name_transformer.rs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -144,10 +144,9 @@ impl Transformer for NameTransformer {
144144

145145
/// Normalize parameter identifier.
146146
fn transform_type_parameter(&mut self, parameter: &Parameter) -> Parameter {
147-
Type::parameter(
147+
self.transform_type(parameter.typ()).as_parameter(
148148
parameter.identifier().map(|name| self.normalize_identifier(name)),
149149
parameter.base_name().map(|name| self.normalize_identifier(name)),
150-
self.transform_type(parameter.typ()),
151150
)
152151
}
153152

compiler/cbmc/src/goto_program/symtab_transformer/transformer.rs

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -97,11 +97,8 @@ pub trait Transformer: Sized {
9797

9898
/// Transforms a parameter for a function
9999
fn transform_type_parameter(&mut self, parameter: &Parameter) -> Parameter {
100-
Type::parameter(
101-
parameter.identifier().cloned(),
102-
parameter.base_name().cloned(),
103-
self.transform_type(parameter.typ()),
104-
)
100+
self.transform_type(parameter.typ())
101+
.as_parameter(parameter.identifier().cloned(), parameter.base_name().cloned())
105102
}
106103

107104
/// Transforms a function type (`return_type x(parameters)`)

compiler/cbmc/src/goto_program/typ.rs

Lines changed: 45 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -423,6 +423,34 @@ impl Type {
423423
}
424424
}
425425

426+
pub fn is_lvalue(&self) -> bool {
427+
match self {
428+
Bool
429+
| CBitField { .. }
430+
| CInteger(_)
431+
| Double
432+
| Float
433+
| Pointer { .. }
434+
| Signedbv { .. }
435+
| Struct { .. }
436+
| StructTag(_)
437+
| Union { .. }
438+
| UnionTag(_)
439+
| Unsignedbv { .. }
440+
| Vector { .. } => true,
441+
442+
Array { .. }
443+
| Code { .. }
444+
| Constructor
445+
| Empty
446+
| FlexibleArray { .. }
447+
| IncompleteStruct { .. }
448+
| IncompleteUnion { .. }
449+
| InfiniteArray { .. }
450+
| VariadicCode { .. } => false,
451+
}
452+
}
453+
426454
/// Is the current type either an integer or a floating point?
427455
pub fn is_numeric(&self) -> bool {
428456
self.is_floating_point() || self.is_integer()
@@ -543,6 +571,22 @@ impl Type {
543571
CBitField { width, typ: Box::new(self) }
544572
}
545573

574+
/// A formal function parameter.
575+
/// identifier: The unique identifier that refers to this parameter `foo12_bar17_x@1`
576+
/// base_name: the local name of the parameter within the function `x`
577+
/// typ: The type of the parameter
578+
pub fn as_parameter(self, identifier: Option<String>, base_name: Option<String>) -> Parameter {
579+
// FIXME: https://github.com/model-checking/rmc/issues/570
580+
assert!(
581+
self.is_empty() || self.is_lvalue(),
582+
"Expected lvalue from {:?} {:?} {:?}",
583+
self,
584+
identifier,
585+
base_name
586+
);
587+
Parameter { identifier, base_name, typ: self }
588+
}
589+
546590
pub fn bool() -> Self {
547591
Bool
548592
}
@@ -568,10 +612,7 @@ impl Type {
568612
/// CBMC, like c, allows function types to have unnamed formal paramaters
569613
/// `int foo(int, char, double)`
570614
pub fn code_with_unnamed_parameters(param_types: Vec<Type>, return_type: Type) -> Self {
571-
let parameters = param_types
572-
.into_iter()
573-
.map(|t| Parameter { identifier: None, base_name: None, typ: t })
574-
.collect();
615+
let parameters = param_types.into_iter().map(|t| t.as_parameter(None, None)).collect();
575616
Type::code(parameters, return_type)
576617
}
577618

@@ -618,18 +659,6 @@ impl Type {
618659
Float
619660
}
620661

621-
/// A formal function parameter.
622-
/// identifier: The unique identifier that refers to this parameter `foo12_bar17_x@1`
623-
/// base_name: the local name of the parameter within the function `x`
624-
/// typ: The type of the parameter
625-
pub fn parameter(
626-
identifier: Option<String>,
627-
base_name: Option<String>,
628-
typ: Type,
629-
) -> Parameter {
630-
Parameter { identifier, base_name, typ }
631-
}
632-
633662
/// A forward declared struct.
634663
/// struct foo;
635664
pub fn incomplete_struct(name: &str) -> Self {

compiler/cbmc/src/irep/from_irep.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -124,8 +124,8 @@ impl FromIrep for Parameter {
124124
assert!(i.sub.is_empty());
125125
let identifier = i.lookup_as_string(IrepId::CIdentifier);
126126
let base_name = i.lookup_as_string(IrepId::CBaseName);
127-
let typ = FromIrep::from_irep(i.lookup(IrepId::Type).unwrap());
128-
Type::parameter(identifier, base_name, typ)
127+
let typ: Type = FromIrep::from_irep(i.lookup(IrepId::Type).unwrap());
128+
typ.as_parameter(identifier, base_name)
129129
}
130130
}
131131

compiler/rustc_codegen_rmc/src/codegen/typ.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1202,7 +1202,7 @@ impl<'tcx> GotocCtx<'tcx> {
12021202
ident = name;
12031203
}
12041204
}
1205-
Some(Type::parameter(Some(ident.to_string()), Some(ident), self.codegen_ty(*t)))
1205+
Some(self.codegen_ty(*t).as_parameter(Some(ident.to_string()), Some(ident)))
12061206
}
12071207
})
12081208
.collect();
@@ -1214,7 +1214,7 @@ impl<'tcx> GotocCtx<'tcx> {
12141214
if let Some(self_param) = params.first() {
12151215
let ident = self_param.identifier().map(|i| i.to_string());
12161216
let ty = self_param.typ().clone();
1217-
params[0] = Type::parameter(ident.clone(), ident, ty.to_pointer());
1217+
params[0] = ty.to_pointer().as_parameter(ident.clone(), ident);
12181218
}
12191219
}
12201220

0 commit comments

Comments
 (0)