diff --git a/regression/cbmc/vla1/main.c b/regression/cbmc/vla1/main.c new file mode 100644 index 00000000000..0e97523b6fc --- /dev/null +++ b/regression/cbmc/vla1/main.c @@ -0,0 +1,30 @@ +#include + +int main(int argc, char *argv[]) +{ + unsigned char x = argc; + // make sure int multiplication below won't overflow - type casting to + // unsigned long long would be possible, but puts yields a challenging problem + // for the SAT solver + __CPROVER_assume(x < 1ULL << (sizeof(int) * 8 / 2 - 1)); + + struct S + { + int a; + int b[x]; + int c; + }; + + if(x % 2 == 0) + x = 3; + + struct S s[x]; + + __CPROVER_assume(x < 255); + ++x; + + assert(sizeof(struct S) == ((unsigned char)argc + 2) * sizeof(int)); + assert(sizeof(s) == (x - 1) * ((unsigned char)argc + 2) * sizeof(int)); + + return 0; +} diff --git a/regression/cbmc/vla1/program-only.desc b/regression/cbmc/vla1/program-only.desc new file mode 100644 index 00000000000..35f671bf4a5 --- /dev/null +++ b/regression/cbmc/vla1/program-only.desc @@ -0,0 +1,12 @@ +CORE +main.c +--program-only +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +\(__CPROVER_size_t\)x\$array_size +-- +There should not be any type cast of x$array_size to __CPROVER_size_t, because +it already is of that type. diff --git a/regression/cbmc/vla1/test.desc b/regression/cbmc/vla1/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/cbmc/vla1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 901c592819c..61d713434a0 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -614,41 +615,25 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type) throw 0; } - // Need to pull out! We insert new symbol. - unsigned count = 0; - irep_idt temp_identifier; - std::string suffix; - - do - { - suffix = "$array_size" + std::to_string(count); - temp_identifier = id2string(current_symbol.name) + suffix; - count++; - } while(symbol_table.symbols.find(temp_identifier) != - symbol_table.symbols.end()); - - // add the symbol to symbol table - auxiliary_symbolt new_symbol; - new_symbol.name = temp_identifier; - new_symbol.pretty_name = id2string(current_symbol.pretty_name) + suffix; - new_symbol.base_name = id2string(current_symbol.base_name) + suffix; - new_symbol.type = size.type(); + symbolt &new_symbol = get_fresh_aux_symbol( + size_type(), + id2string(current_symbol.name) + "$array_size", + id2string(current_symbol.base_name) + "$array_size", + size_source_location, + mode, + symbol_table); new_symbol.type.set(ID_C_constant, true); - new_symbol.value = size; - new_symbol.location = size_source_location; - new_symbol.mode = mode; - - symbol_table.add(new_symbol); + new_symbol.value = typecast_exprt::conditional_cast(size, size_type()); // produce the code that declares and initializes the symbol - symbol_exprt symbol_expr(temp_identifier, new_symbol.type); + symbol_exprt symbol_expr = new_symbol.symbol_expr(); code_declt declaration(symbol_expr); declaration.add_source_location() = size_source_location; code_assignt assignment; assignment.lhs()=symbol_expr; - assignment.rhs() = size; + assignment.rhs() = new_symbol.value; assignment.add_source_location() = size_source_location; // store the code diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 24e1030dca0..5aef628f991 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -611,12 +611,70 @@ void goto_symex_statet::rename_address( } } +/// Return true if, and only if, the \p type or one of its subtypes requires SSA +/// renaming. Renaming is necessary when symbol expressions occur within the +/// type, which is the case for arrays of non-constant size. +static bool requires_renaming(const typet &type, const namespacet &ns) +{ + if(type.id() == ID_array) + { + const auto &array_type = to_array_type(type); + return requires_renaming(array_type.subtype(), ns) || + !array_type.size().is_constant(); + } + else if( + type.id() == ID_struct || type.id() == ID_union || type.id() == ID_class) + { + const struct_union_typet &s_u_type = to_struct_union_type(type); + const struct_union_typet::componentst &components = s_u_type.components(); + + for(auto &component : components) + { + // be careful, or it might get cyclic + if( + component.type().id() != ID_pointer && + requires_renaming(component.type(), ns)) + { + return true; + } + } + + return false; + } + else if(type.id() == ID_pointer) + { + return requires_renaming(to_pointer_type(type).subtype(), ns); + } + else if(type.id() == ID_symbol_type) + { + const symbolt &symbol = ns.lookup(to_symbol_type(type)); + return requires_renaming(symbol.type, ns); + } + else if(type.id() == ID_union_tag) + { + const symbolt &symbol = ns.lookup(to_union_tag_type(type)); + return requires_renaming(symbol.type, ns); + } + else if(type.id() == ID_struct_tag) + { + const symbolt &symbol = ns.lookup(to_struct_tag_type(type)); + return requires_renaming(symbol.type, ns); + } + + return false; +} + void goto_symex_statet::rename( typet &type, const irep_idt &l1_identifier, const namespacet &ns, levelt level) { + // check whether there are symbol expressions in the type; if not, there + // is no need to expand the struct/union tags in the type + if(!requires_renaming(type, ns)) + return; // no action + // rename all the symbols with their last known value // to the given level