Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
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
25 changes: 25 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 @@ -698,6 +698,27 @@ impl Expr {
Expr::struct_expr_with_explicit_padding(typ, fields, values)
}

/// Struct initializer
/// `struct foo the_foo = >>> {field1, padding2, field3, ... } <<<`
/// Note that padding fields should be explicitiy given.
pub fn struct_expr_from_padded_values(
typ: Type,
mut values: Vec<Expr>,
symbol_table: &SymbolTable,
) -> Self {
assert!(typ.is_struct_tag(), "Error in struct_expr\n\t{:?}\n\t{:?}", typ, values);
let fields = symbol_table.lookup_fields_in_type(&typ).unwrap();
assert_eq!(fields.len(), values.len(), "Error in struct_expr\n\t{:?}\n\t{:?}", typ, values);
assert!(
fields.iter().zip(values.iter()).all(|(f, v)| &f.typ() == v.typ()),
"Error in struct_expr\n\t{:?}\n\t{:?}",
typ,
values
);

Expr::struct_expr_with_explicit_padding(typ, fields, values)
}

/// `identifier`
pub fn symbol_expression(identifier: String, typ: Type) -> Self {
expr!(Symbol { identifier }, typ)
Expand Down Expand Up @@ -1213,6 +1234,10 @@ impl Expr {
expr!(StringConstant { s: s.to_string() }, Type::c_char().array_of(s.len() + 1))
.array_to_ptr()
}

pub fn raw_string_constant(s: &str) -> Self {
expr!(StringConstant { s: s.to_string() }, Type::c_char().array_of(s.len() + 1))
}
}
/// Conversions to statements
/// The statement constructors do typechecking, so we don't redundantly do that here.
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,182 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT

use super::{
CIntType, DatatypeComponent, Expr, Location, Parameter, Stmt, StmtBody, Symbol, SymbolTable,
SymbolValues, Transformer, Type,
};
use std::collections::{BTreeMap, HashMap, HashSet};

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Add a check that injective

fn normalize_identifier(name: &str) -> String {
let valid_chars = name.replace(|ch: char| !(ch.is_alphanumeric() || ch == '_'), "_");
let new_name = match valid_chars.chars().next() {
Some(first) => {
if first.is_numeric() {
let mut name = "_".to_string();
name.push_str(&valid_chars);
name
} else {
valid_chars
}
}
None => "_".to_string(),
};

let mut illegal_names: HashMap<_, _> = [("case", "case_"), ("main", "main_")]
.iter()
.map(|(key, value)| (key.to_string(), value.to_string()))
.collect();

illegal_names.remove(&new_name).unwrap_or(new_name)
}

pub struct GenCTransformer {
new_symbol_table: SymbolTable,
}

impl GenCTransformer {
pub fn transform(original_symbol_table: &SymbolTable) -> SymbolTable {
let new_symbol_table = SymbolTable::new(original_symbol_table.machine_model().clone());
GenCTransformer { new_symbol_table }.transform_symbol_table(original_symbol_table)
}
}

impl Transformer for GenCTransformer {
fn symbol_table(&self) -> &SymbolTable {
&self.new_symbol_table
}

fn mut_symbol_table(&mut self) -> &mut SymbolTable {
&mut self.new_symbol_table
}

fn extract_symbol_table(self) -> SymbolTable {
self.new_symbol_table
}

fn transform_parameter(&self, parameter: &Parameter) -> Parameter {
Type::parameter(
parameter.identifier().map(|name| normalize_identifier(name)),
parameter.base_name().map(|name| normalize_identifier(name)),
self.transform_type(parameter.typ()),
)
}

fn transform_member_expr(&self, _typ: &Type, lhs: &Expr, field: &str) -> Expr {
let transformed_lhs = self.transform_expr(lhs);
transformed_lhs.member(&normalize_identifier(field), self.symbol_table())
}

fn transform_symbol_expr(&self, typ: &Type, identifier: &str) -> Expr {
let transformed_typ = self.transform_type(typ);
Expr::symbol_expression(normalize_identifier(identifier), transformed_typ)
}

fn transform_union_expr(&self, typ: &Type, value: &Expr, field: &str) -> Expr {
let transformed_typ = self.transform_type(typ);
let transformed_value = self.transform_expr(value);
Expr::union_expr(
transformed_typ,
&normalize_identifier(field),
transformed_value,
self.symbol_table(),
)
}

fn transform_incomplete_struct_type(&self, tag: &str) -> Type {
Type::incomplete_struct(&normalize_identifier(tag))
}

fn transform_incomplete_union_type(&self, tag: &str) -> Type {
Type::incomplete_union(&normalize_identifier(tag))
}

fn transform_datatype_component(&self, component: &DatatypeComponent) -> DatatypeComponent {
match component {
DatatypeComponent::Field { name, typ } => DatatypeComponent::Field {
name: normalize_identifier(name),
typ: self.transform_type(typ),
},
DatatypeComponent::Padding { name, bits } => {
DatatypeComponent::Padding { name: normalize_identifier(name), bits: *bits }
}
}
}

fn transform_struct_type(&self, tag: &str, components: &[DatatypeComponent]) -> Type {
let transformed_components = components
.iter()
.map(|component| self.transform_datatype_component(component))
.collect();
Type::struct_type(&normalize_identifier(tag), transformed_components)
}

fn transform_struct_tag_type(&self, tag: &str) -> Type {
Type::struct_tag_raw(&normalize_identifier(tag))
}

fn transform_union_type(&self, tag: &str, components: &[DatatypeComponent]) -> Type {
let transformed_components = components
.iter()
.map(|component| self.transform_datatype_component(component))
.collect();
Type::union_type(&normalize_identifier(tag), transformed_components)
}

fn transform_union_tag_type(&self, tag: &str) -> Type {
Type::union_tag_raw(&normalize_identifier(tag))
}

fn transform_goto_stmt(&self, label: &str) -> Stmt {
Stmt::goto(normalize_identifier(label), Location::none())
}

fn transform_label_stmt(&self, label: &str, body: &Stmt) -> Stmt {
let transformed_body = self.transform_stmt(body);
transformed_body.with_label(normalize_identifier(label))
}

fn transform_symbol(&self, symbol: &Symbol) -> Symbol {
let new_typ = self.transform_type(&symbol.typ);
let new_value = self.transform_value(&symbol.value);
let mut new_symbol = symbol.clone();
new_symbol.value = new_value;
new_symbol.typ = new_typ;
new_symbol.name = normalize_identifier(&new_symbol.name);
new_symbol.base_name = new_symbol.base_name.map(|name| normalize_identifier(&name));
new_symbol.pretty_name = new_symbol.pretty_name.map(|name| normalize_identifier(&name));
new_symbol
}

fn postprocess(&mut self) {
let memcpy = self.mut_symbol_table().remove("memcpy");
assert!(memcpy.is_some());
let memmove = self.mut_symbol_table().remove("memmove");
assert!(memmove.is_some());

let old_main = self.symbol_table().lookup("main_");
if let Some(old_main) = old_main {
let new_main = Symbol::function(
"main",
Type::code(Vec::new(), Type::CInteger(CIntType::Int)),
Some(Stmt::block(
vec![
Stmt::code_expression(
Expr::symbol_expression("main_".to_string(), old_main.typ.clone())
.call(Vec::new()),
Location::none(),
),
Stmt::ret(
Some(Expr::int_constant(0, Type::CInteger(CIntType::Int))),
Location::none(),
),
],
Location::none(),
)),
Some("main".to_string()),
Location::none(),
);
self.mut_symbol_table().insert(new_main);
}
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT

use super::{
DatatypeComponent, Expr, Location, Stmt, Symbol, SymbolTable, SymbolValues, Transformer, Type,
};
use std::collections::{BTreeMap, HashSet};

pub struct IdentityTransformer {
new_symbol_table: SymbolTable,
}

impl IdentityTransformer {
pub fn transform(original_symbol_table: &SymbolTable) -> SymbolTable {
let new_symbol_table = SymbolTable::new(original_symbol_table.machine_model().clone());
IdentityTransformer { new_symbol_table }.transform_symbol_table(original_symbol_table)
}
}

impl Transformer for IdentityTransformer {
fn symbol_table(&self) -> &SymbolTable {
&self.new_symbol_table
}

fn mut_symbol_table(&mut self) -> &mut SymbolTable {
&mut self.new_symbol_table
}

fn extract_symbol_table(self) -> SymbolTable {
self.new_symbol_table
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -4,18 +4,24 @@

mod builtin;
mod expr;
mod gen_c_transformer;
mod identity_transformer;
mod location;
mod stmt;
mod symbol;
mod symbol_table;
mod transformer;
mod typ;

pub use builtin::BuiltinFn;
pub use expr::{
ArithmeticOverflowResult, BinaryOperand, Expr, ExprValue, SelfOperand, UnaryOperand,
};
pub use gen_c_transformer::GenCTransformer;
pub use identity_transformer::IdentityTransformer;
pub use location::Location;
pub use stmt::{Stmt, StmtBody, SwitchCase};
pub use symbol::{Symbol, SymbolValues};
pub use symbol_table::SymbolTable;
pub use transformer::Transformer;
pub use typ::{CIntType, DatatypeComponent, Parameter, Type};
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,10 @@ impl SymbolTable {
pub fn update_fn_declaration_with_definition(&mut self, name: &str, body: Stmt) {
self.symbol_table.get_mut(name).unwrap().update_fn_declaration_with_definition(body);
}

pub fn remove(&mut self, name: &str) -> Option<Symbol> {
self.symbol_table.remove(name)
}
}

/// Getters
Expand Down
Loading