From 98e53652eb6d270d4d2c1b5c21853c675eba07f0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 27 Jan 2019 18:00:22 +0000 Subject: [PATCH 1/4] Revert "Revert "goto_symex: rename type symbols only when needed"" This reverts commit 60ce9975e69cc388b88fdcd57dc2fbb89a98fff1. --- src/goto-symex/goto_symex_state.cpp | 51 +++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 24e1030dca0..404bb731584 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -611,12 +611,63 @@ void goto_symex_statet::rename_address( } } +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) + return requires_renaming(component.type(), ns); + } + + 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 From d9e27b2fbc1a4d58b87dfef09c855b21590c0006 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 27 Jan 2019 18:00:30 +0000 Subject: [PATCH 2/4] Revert "Revert "Check all struct members for possible need for renaming"" This reverts commit ec7e041140c6a196093d8cdb53e51d32cc123a2e. --- regression/cbmc/vla1/main.c | 30 +++++++++++++++++++++++++++++ regression/cbmc/vla1/test.desc | 8 ++++++++ src/goto-symex/goto_symex_state.cpp | 11 +++++++++-- 3 files changed, 47 insertions(+), 2 deletions(-) create mode 100644 regression/cbmc/vla1/main.c create mode 100644 regression/cbmc/vla1/test.desc 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/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/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 404bb731584..5aef628f991 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -611,6 +611,9 @@ 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) @@ -628,8 +631,12 @@ static bool requires_renaming(const typet &type, const namespacet &ns) for(auto &component : components) { // be careful, or it might get cyclic - if(component.type().id() != ID_pointer) - return requires_renaming(component.type(), ns); + if( + component.type().id() != ID_pointer && + requires_renaming(component.type(), ns)) + { + return true; + } } return false; From bc9233edd64d9bc24eb5095370a5200fd4610393 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 27 Jan 2019 18:00:49 +0000 Subject: [PATCH 3/4] Revert "clang-format reverted code - must be reverted in future as well" This reverts commit ea539edd7d2a260fc553ea5965df67dce15612d3. --- src/ansi-c/c_typecheck_type.cpp | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 901c592819c..e642b337065 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -615,26 +615,27 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type) } // Need to pull out! We insert new symbol. - unsigned count = 0; + 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; + 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()); + } + 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(); + 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(); new_symbol.type.set(ID_C_constant, true); - new_symbol.value = size; + new_symbol.value=size; new_symbol.location = size_source_location; new_symbol.mode = mode; @@ -648,7 +649,7 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type) code_assignt assignment; assignment.lhs()=symbol_expr; - assignment.rhs() = size; + assignment.rhs()=size; assignment.add_source_location() = size_source_location; // store the code From 94dacc5416d3de4ceb680d76d8ae4e14dd1eb3d7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 27 Jan 2019 18:00:56 +0000 Subject: [PATCH 4/4] Revert "Revert "Use get_fresh_aux_symbol to create $array_size and fix its type"" This reverts commit 9e204fd5434c025f9e1c4fce61ffbc0821f2a93b. --- regression/cbmc/vla1/program-only.desc | 12 ++++++++ src/ansi-c/c_typecheck_type.cpp | 38 ++++++++------------------ 2 files changed, 23 insertions(+), 27 deletions(-) create mode 100644 regression/cbmc/vla1/program-only.desc 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/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index e642b337065..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,42 +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