Skip to content

Commit

Permalink
Complete and replace the unsized pointer cast implementation (#88)
Browse files Browse the repository at this point in the history
* Complete and replace the unsized pointer cast implementation

* Respond to code review of unsized pointer cast implementation

Co-authored-by: Mark R. Tuttle <mrtuttle@amazon.com>
  • Loading branch information
2 people authored and adpaco-aws committed Aug 2, 2021
1 parent f40daab commit 286f9d2
Show file tree
Hide file tree
Showing 6 changed files with 379 additions and 108 deletions.
41 changes: 41 additions & 0 deletions compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1205,3 +1205,44 @@ impl Expr {
SwitchCase::new(self, body)
}
}

impl Expr {
/// Given a struct value (Expr), construct a mapping from struct field names
/// (Strings) to struct field values (Exprs).
///
/// The Struct variant of the Expr enum models the fields of a struct as a
/// list of pairs (data type components) consisting of a field name and a
/// field value. A pair may represent an actual field in the struct or just
/// padding in the layout of the struct. This function returns a mapping of
/// field names (ignoring the padding fields) to field values. The result
/// is suitable for use in the struct_expr constructor. This makes it
/// easier to look up or modify field values of a struct.
pub fn struct_field_exprs(&self, symbol_table: &SymbolTable) -> BTreeMap<String, Expr> {
let struct_type = self.typ();
assert!(struct_type.is_struct_tag());

let mut exprs: BTreeMap<String, Expr> = BTreeMap::new();
let fields = symbol_table.lookup_fields_in_type(struct_type).unwrap();
match self.struct_expr_values() {
Some(values) => {
assert!(fields.len() == values.len());
for i in 0..fields.len() {
if fields[i].is_padding() {
continue;
}
exprs.insert(fields[i].name().to_string(), values[i].clone());
}
}
None => {
for i in 0..fields.len() {
if fields[i].is_padding() {
continue;
}
let name = fields[i].name();
exprs.insert(name.to_string(), self.clone().member(name, &symbol_table));
}
}
}
exprs
}
}
28 changes: 28 additions & 0 deletions compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ use self::Type::*;
use super::super::utils::aggr_name;
use super::super::MachineModel;
use super::{Expr, SymbolTable};
use std::collections::BTreeMap;
use std::convert::TryInto;
use std::fmt::Debug;

Expand Down Expand Up @@ -782,3 +783,30 @@ impl Type {
}
}
}

impl Type {
/// Given a struct type, construct a mapping from struct field names
/// (Strings) to struct field types (Types).
///
/// The Struct variant of the Type enum models the fields of a struct as a
/// list of pairs (data type components) consisting of a field name and a
/// field type. A pair may represent an actual field in the struct or just
/// padding in the layout of the struct. This function returns a mapping of
/// field names (ignoring the padding fields) to field types. This makes it
/// easier to look up field types (and modestly easier to interate over
/// field types).
pub fn struct_field_types(&self, symbol_table: &SymbolTable) -> BTreeMap<String, Type> {
// TODO: Accept a Struct type, too, and not just a StructTag assumed below.
assert!(self.is_struct_tag());

let mut types: BTreeMap<String, Type> = BTreeMap::new();
let fields = symbol_table.lookup_fields_in_type(self).unwrap();
for field in fields {
if field.is_padding() {
continue;
}
types.insert(field.name().to_string(), field.typ());
}
types
}
}
2 changes: 1 addition & 1 deletion compiler/rustc_codegen_llvm/src/gotoc/place.rs
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,7 @@ impl<'tcx> ProjectedPlace<'tcx> {

/// Constructor
impl<'tcx> ProjectedPlace<'tcx> {
fn check_expr_typ(expr: &Expr, typ: &TypeOrVariant<'tcx>, ctx: &mut GotocCtx<'tcx>) -> bool {
fn _check_expr_typ(expr: &Expr, typ: &TypeOrVariant<'tcx>, ctx: &mut GotocCtx<'tcx>) -> bool {
match typ {
TypeOrVariant::Type(t) => &ctx.codegen_ty(t) == expr.typ(),
TypeOrVariant::Variant(_) => true, //TODO, what to do here?
Expand Down
Loading

0 comments on commit 286f9d2

Please sign in to comment.