From 9e204fd5434c025f9e1c4fce61ffbc0821f2a93b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 25 Jan 2019 12:57:03 +0000 Subject: [PATCH 1/4] Revert "Use get_fresh_aux_symbol to create $array_size and fix its type" This reverts commit 0e01c893aa938a3ba5e188e5e012ee8ea531ca62. --- regression/cbmc/vla1/program-only.desc | 12 -------- src/ansi-c/c_typecheck_type.cpp | 40 +++++++++++++++++++------- 2 files changed, 29 insertions(+), 23 deletions(-) delete mode 100644 regression/cbmc/vla1/program-only.desc diff --git a/regression/cbmc/vla1/program-only.desc b/regression/cbmc/vla1/program-only.desc deleted file mode 100644 index 35f671bf4a5..00000000000 --- a/regression/cbmc/vla1/program-only.desc +++ /dev/null @@ -1,12 +0,0 @@ -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 036981b126d..46a42be2405 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -609,25 +608,44 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type) throw 0; } - 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); + // 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(); new_symbol.type.set(ID_C_constant, true); - new_symbol.value = typecast_exprt::conditional_cast(size, size_type()); + new_symbol.value=size; + new_symbol.location = size_source_location; + new_symbol.mode = mode; + + symbol_table.add(new_symbol); // produce the code that declares and initializes the symbol - symbol_exprt symbol_expr = new_symbol.symbol_expr(); + symbol_exprt symbol_expr; + symbol_expr.set_identifier(temp_identifier); + symbol_expr.type()=new_symbol.type; code_declt declaration(symbol_expr); declaration.add_source_location() = size_source_location; code_assignt assignment; assignment.lhs()=symbol_expr; - assignment.rhs() = new_symbol.value; + assignment.rhs()=size; assignment.add_source_location() = size_source_location; // store the code From ea539edd7d2a260fc553ea5965df67dce15612d3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 25 Jan 2019 15:25:15 +0000 Subject: [PATCH 2/4] clang-format reverted code - must be reverted in future as well --- src/ansi-c/c_typecheck_type.cpp | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 46a42be2405..f0b4e24b11c 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -609,27 +609,26 @@ 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; @@ -638,14 +637,14 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type) // produce the code that declares and initializes the symbol symbol_exprt symbol_expr; symbol_expr.set_identifier(temp_identifier); - symbol_expr.type()=new_symbol.type; + symbol_expr.type() = new_symbol.type; code_declt declaration(symbol_expr); declaration.add_source_location() = size_source_location; code_assignt assignment; assignment.lhs()=symbol_expr; - assignment.rhs()=size; + assignment.rhs() = size; assignment.add_source_location() = size_source_location; // store the code From ec7e041140c6a196093d8cdb53e51d32cc123a2e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 25 Jan 2019 12:52:06 +0000 Subject: [PATCH 3/4] Revert "Check all struct members for possible need for renaming" This reverts commit 480f19e05e7255d970754e10a3383210f8230a90. --- regression/cbmc/vla1/main.c | 30 ----------------------------- regression/cbmc/vla1/test.desc | 8 -------- src/goto-symex/goto_symex_state.cpp | 11 ++--------- 3 files changed, 2 insertions(+), 47 deletions(-) delete mode 100644 regression/cbmc/vla1/main.c delete mode 100644 regression/cbmc/vla1/test.desc diff --git a/regression/cbmc/vla1/main.c b/regression/cbmc/vla1/main.c deleted file mode 100644 index 0e97523b6fc..00000000000 --- a/regression/cbmc/vla1/main.c +++ /dev/null @@ -1,30 +0,0 @@ -#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 deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/cbmc/vla1/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -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 0b0fc90e74f..bddad21b483 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -618,9 +618,6 @@ 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) @@ -638,12 +635,8 @@ 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 && - requires_renaming(component.type(), ns)) - { - return true; - } + if(component.type().id() != ID_pointer) + return requires_renaming(component.type(), ns); } return false; From 60ce9975e69cc388b88fdcd57dc2fbb89a98fff1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 25 Jan 2019 12:52:16 +0000 Subject: [PATCH 4/4] Revert "goto_symex: rename type symbols only when needed" This reverts commit 8c1ae4ca0d3b55ae8ea6aecfff55dd4c5fcdf54d. --- src/goto-symex/goto_symex_state.cpp | 51 ----------------------------- 1 file changed, 51 deletions(-) diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index bddad21b483..44b3b58e4ca 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -618,63 +618,12 @@ 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