From cb9fc73d7a816738745fc7920cbac34d0ca33728 Mon Sep 17 00:00:00 2001 From: Chris Ryder Date: Fri, 11 Jan 2019 16:36:04 +0000 Subject: [PATCH 01/11] Fix base_name of return' symbol to match its name --- regression/cbmc/typedef-return-anon-struct1/test.desc | 2 +- .../typedef-return-anon-struct1/test.desc | 2 +- src/ansi-c/ansi_c_entry_point.cpp | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/regression/cbmc/typedef-return-anon-struct1/test.desc b/regression/cbmc/typedef-return-anon-struct1/test.desc index 420ac1295ac..d7f63e586ae 100644 --- a/regression/cbmc/typedef-return-anon-struct1/test.desc +++ b/regression/cbmc/typedef-return-anon-struct1/test.desc @@ -5,7 +5,7 @@ main.c activate-multi-line-match EXIT=0 SIGNAL=0 -Base name\.+: return\nMode\.+: C\nType\.+: MYSTRUCT +Base name\.+: return'\nMode\.+: C\nType\.+: MYSTRUCT Base name\.+: fun\nMode\.+: C\nType\.+: MYSTRUCT \(\) -- warning: ignoring diff --git a/regression/goto-instrument-typedef/typedef-return-anon-struct1/test.desc b/regression/goto-instrument-typedef/typedef-return-anon-struct1/test.desc index 1cdd14e9ba4..15b07e2d754 100644 --- a/regression/goto-instrument-typedef/typedef-return-anon-struct1/test.desc +++ b/regression/goto-instrument-typedef/typedef-return-anon-struct1/test.desc @@ -5,7 +5,7 @@ main.c activate-multi-line-match EXIT=0 SIGNAL=0 -Base name\.+: return\nMode\.+: C\nType\.+: MYSTRUCT +Base name\.+: return'\nMode\.+: C\nType\.+: MYSTRUCT Base name\.+: fun\nMode\.+: C\nType\.+: MYSTRUCT \(\) -- warning: ignoring diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index ea08e404cb8..b5fa578671c 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -238,7 +238,7 @@ bool generate_ansi_c_start_function( return_symbol.mode=ID_C; return_symbol.is_static_lifetime=false; return_symbol.name="return'"; - return_symbol.base_name="return"; + return_symbol.base_name = "return'"; return_symbol.type=to_code_type(symbol.type).return_type(); symbol_table.add(return_symbol); From f13dbea3a919628b1f12e35a3e7f282fb2e8673b Mon Sep 17 00:00:00 2001 From: Chris Ryder Date: Fri, 11 Jan 2019 16:36:58 +0000 Subject: [PATCH 02/11] Fix base_name of argc' symbol to match its name --- src/ansi-c/ansi_c_entry_point.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index b5fa578671c..02033a2e39b 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -261,7 +261,7 @@ bool generate_ansi_c_start_function( { symbolt argc_symbol; - argc_symbol.base_name = "argc"; + argc_symbol.base_name = "argc'"; argc_symbol.name = "argc'"; argc_symbol.type = signed_int_type(); argc_symbol.is_static_lifetime = true; From 21300739f6606f8be6281ef3f3d65e92daea1e54 Mon Sep 17 00:00:00 2001 From: Chris Ryder Date: Fri, 11 Jan 2019 16:39:39 +0000 Subject: [PATCH 03/11] Ensure the gcc_builtin_va_arg symbol has a mode --- src/ansi-c/c_typecheck_expr.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 3e085b964aa..218a1fbff5a 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -538,6 +538,7 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr) symbol.base_name=ID_gcc_builtin_va_arg; symbol.name=ID_gcc_builtin_va_arg; symbol.type=symbol_type; + symbol.mode = ID_C; symbol_table.insert(std::move(symbol)); } From 03518c9b00f37e8fc9129c828ab37dc3fa6eddcf Mon Sep 17 00:00:00 2001 From: Chris Ryder Date: Fri, 11 Jan 2019 16:50:18 +0000 Subject: [PATCH 04/11] Make #anon symbols have consistent naming between base_name and name --- src/ansi-c/c_typecheck_type.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index f0b4e24b11c..5bf1767e6f5 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -769,7 +769,7 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type) typecheck_compound_body(to_struct_union_type(compound_symbol.type)); std::string typestr = type2name(compound_symbol.type, *this); - compound_symbol.base_name="#anon-"+typestr; + compound_symbol.base_name = "#anon#" + typestr; compound_symbol.name="tag-#anon#"+typestr; identifier=compound_symbol.name; From e5bae7e55023d675169c07ad19d4f496ca55131e Mon Sep 17 00:00:00 2001 From: Chris Ryder Date: Fri, 11 Jan 2019 17:01:43 +0000 Subject: [PATCH 05/11] Ensure the '$exception_flag' symbol has a valid mode --- src/goto-programs/goto_convert_class.h | 2 +- src/goto-programs/goto_convert_exceptions.cpp | 7 ++++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index c5297663744..55b6a2de569 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -335,7 +335,7 @@ class goto_convertt:public messaget typedef std::vector destructor_stackt; - symbol_exprt exception_flag(); + symbol_exprt exception_flag(const irep_idt &mode); void unwind_destructor_stack( const source_locationt &, std::size_t stack_size, diff --git a/src/goto-programs/goto_convert_exceptions.cpp b/src/goto-programs/goto_convert_exceptions.cpp index d8f4791a80a..f05214c8fd1 100644 --- a/src/goto-programs/goto_convert_exceptions.cpp +++ b/src/goto-programs/goto_convert_exceptions.cpp @@ -168,7 +168,7 @@ void goto_convertt::convert_CPROVER_try_catch( targets.set_throw(tmp.instructions.begin()); // now put 'catch' code onto destructor stack - code_ifthenelset catch_code(exception_flag(), to_code(code.op1())); + code_ifthenelset catch_code(exception_flag(mode), to_code(code.op1())); catch_code.add_source_location()=code.source_location(); targets.destructor_stack.push_back(std::move(catch_code)); @@ -194,7 +194,7 @@ void goto_convertt::convert_CPROVER_throw( dest.add_instruction(ASSIGN); t_set_exception->source_location=code.source_location(); - t_set_exception->code=code_assignt(exception_flag(), true_exprt()); + t_set_exception->code = code_assignt(exception_flag(mode), true_exprt()); } // do we catch locally? @@ -244,7 +244,7 @@ void goto_convertt::convert_CPROVER_try_finally( convert(to_code(code.op1()), dest, mode); } -symbol_exprt goto_convertt::exception_flag() +symbol_exprt goto_convertt::exception_flag(const irep_idt &mode) { irep_idt id="$exception_flag"; @@ -260,6 +260,7 @@ symbol_exprt goto_convertt::exception_flag() new_symbol.is_thread_local=true; new_symbol.is_file_local=false; new_symbol.type=bool_typet(); + new_symbol.mode = mode; symbol_table.insert(std::move(new_symbol)); } From 73ff6758546e924f2ae6ba078e8a65e30987267b Mon Sep 17 00:00:00 2001 From: Chris Ryder Date: Fri, 11 Jan 2019 17:05:31 +0000 Subject: [PATCH 06/11] Refine symbol well-formedness checks to handle special cases The symbol naming check added in df616e4 attempts to assert that the 'base_name' of a symbol is a suffix of that symbol's 'name'. In general, this should be the case, but there are certain classes of symbols where this does not currently hold. This commit adds special cases to handle: * Type symbols that are typedefs or tags * Symbols that have been renamed by the linker With these special cases handled, it is possible to run the CORE regression tests with --validate-goto-model enabled. --- src/util/symbol.cpp | 54 ++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 53 insertions(+), 1 deletion(-) diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp index 73225b1e502..6a0f1179b2c 100644 --- a/src/util/symbol.cpp +++ b/src/util/symbol.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "source_location.h" #include "std_expr.h" +#include "string_utils.h" #include "suffix.h" /// Dump the state of a symbol object to a given output stream. @@ -137,11 +138,62 @@ bool symbolt::is_well_formed() const // Well-formedness criterion number 2 is for a symbol // to have it's base name as a suffix to it's more // general name. + // Exception: Java symbols' base names do not have type signatures // (for example, they can have name "someclass.method:(II)V" and base name // "method") if(!has_suffix(id2string(name), id2string(base_name)) && mode != ID_java) - return false; + { + bool criterion_must_hold = true; + + // There are some special cases where this criterion doesn't hold, check + // to see if we have one of those cases + + if(is_type) + { + // Typedefs + if( + type.find(ID_C_typedef).is_not_nil() && + type.find(ID_C_typedef).id() == base_name) + { + criterion_must_hold = false; + } + + // Tag types + if(type.find(ID_tag).is_not_nil() && type.find(ID_tag).id() == base_name) + { + criterion_must_hold = false; + } + } + + // Linker renaming may have added $linkN suffixes to the name, and other + // suffixes such as #return_value may have then be subsequently added. + // Strip out the first $linkN substring and then see if the criterion holds + const auto &unstripped_name = id2string(name); + const size_t dollar_link_start_pos = unstripped_name.find("$link"); + + if(dollar_link_start_pos != std::string::npos) + { + size_t dollar_link_end_pos = dollar_link_start_pos + 5; + while(isdigit(unstripped_name[dollar_link_end_pos])) + { + ++dollar_link_end_pos; + } + + const auto stripped_name = + unstripped_name.substr(0, dollar_link_start_pos) + + unstripped_name.substr(dollar_link_end_pos, std::string::npos); + + if(has_suffix(stripped_name, id2string(base_name))) + criterion_must_hold = false; + } + + if(criterion_must_hold) + { + // For all other cases this criterion should hold + return false; + } + } return true; } From 33be52420501259df12d9822bd88b6300090a668 Mon Sep 17 00:00:00 2001 From: Chris Ryder Date: Fri, 18 Jan 2019 16:17:35 +0000 Subject: [PATCH 07/11] Correct validation check for return statements from void functions --- src/goto-programs/goto_function.cpp | 33 +++++++++++++++++++++++++++++ src/goto-programs/goto_function.h | 18 +--------------- src/util/std_code.h | 7 +----- 3 files changed, 35 insertions(+), 23 deletions(-) diff --git a/src/goto-programs/goto_function.cpp b/src/goto-programs/goto_function.cpp index e4fd3856369..52216f4c211 100644 --- a/src/goto-programs/goto_function.cpp +++ b/src/goto-programs/goto_function.cpp @@ -31,3 +31,36 @@ void get_local_identifiers( dest.insert(identifier); } } + +/// Check that the goto function is well-formed +/// +/// The validation mode indicates whether well-formedness check failures are +/// reported via DATA_INVARIANT violations or exceptions. +void goto_functiont::validate(const namespacet &ns, const validation_modet vm) + const +{ + body.validate(ns, vm); + + find_symbols_sett typetags; + find_type_symbols(type, typetags); + const symbolt *symbol; + for(const auto &identifier : typetags) + { + DATA_CHECK( + vm, !ns.lookup(identifier, symbol), id2string(identifier) + " not found"); + } + + // Check that a void function does not contain any RETURN instructions + if(to_code_type(type).return_type().id() == ID_empty) + { + forall_goto_program_instructions(instruction, body) + { + DATA_CHECK( + vm, + !instruction->is_return(), + "void function should not return a value"); + } + } + + validate_full_type(type, ns, vm); +} diff --git a/src/goto-programs/goto_function.h b/src/goto-programs/goto_function.h index a73d538c8fb..c3634675a58 100644 --- a/src/goto-programs/goto_function.h +++ b/src/goto-programs/goto_function.h @@ -116,23 +116,7 @@ class goto_functiont /// /// The validation mode indicates whether well-formedness check failures are /// reported via DATA_INVARIANT violations or exceptions. - void validate(const namespacet &ns, const validation_modet vm) const - { - body.validate(ns, vm); - - find_symbols_sett typetags; - find_type_symbols(type, typetags); - const symbolt *symbol; - for(const auto &identifier : typetags) - { - DATA_CHECK( - vm, - !ns.lookup(identifier, symbol), - id2string(identifier) + " not found"); - } - - validate_full_type(type, ns, vm); - } + void validate(const namespacet &ns, const validation_modet vm) const; }; void get_local_identifiers(const goto_functiont &, std::set &dest); diff --git a/src/util/std_code.h b/src/util/std_code.h index 24400b7eca2..54995198239 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -1135,12 +1135,7 @@ class code_function_callt:public codet { check(code, vm); - if(code.op0().id() == ID_nil) - DATA_CHECK( - vm, - to_code_type(code.op1().type()).return_type().id() == ID_empty, - "void function should not return value"); - else + if(code.op0().id() != ID_nil) DATA_CHECK( vm, base_type_eq( From f6dc11741825a739ba5c63374bac9f2380b21eaf Mon Sep 17 00:00:00 2001 From: Chris Ryder Date: Wed, 23 Jan 2019 16:31:51 +0000 Subject: [PATCH 08/11] Correct symbol table type check in cases where return removal has modified types Return removal sets the return type of a function symbol table entry to 'void', but some callsites still expect the original type (e.g. if a function is passed as a parameter to a different function) --- src/goto-programs/goto_program.cpp | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 998eda53bd8..20ea0a95538 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -22,6 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "remove_returns.h" + /// Writes to \p out a two/three line string representation of a given /// \p instruction. The output is of the format: /// ``` @@ -709,13 +711,31 @@ void goto_programt::instructiont::validate( const auto &goto_id = goto_symbol_expr.get_identifier(); if(!ns.lookup(goto_id, table_symbol)) + { + bool symbol_expr_type_matches_symbol_table = + base_type_eq(goto_symbol_expr.type(), table_symbol->type, ns); + + if( + !symbol_expr_type_matches_symbol_table && + table_symbol->type.id() == ID_code) + { + // Return removal sets the return type of a function symbol table + // entry to 'void', but some callsites still expect the original + // type (e.g. if a function is passed as a parameter) + symbol_expr_type_matches_symbol_table = base_type_eq( + goto_symbol_expr.type(), + original_return_type(ns.get_symbol_table(), goto_id), + ns); + } + DATA_CHECK_WITH_DIAGNOSTICS( vm, - base_type_eq(goto_symbol_expr.type(), table_symbol->type, ns), + symbol_expr_type_matches_symbol_table, id2string(goto_id) + " type inconsistency\n" + "goto program type: " + goto_symbol_expr.type().id_string() + "\n" + "symbol table type: " + table_symbol->type.id_string(), current_source_location); + } } }; From 1447ad64eead2ce808692efbbb6233340940da04 Mon Sep 17 00:00:00 2001 From: Chris Ryder Date: Thu, 24 Jan 2019 16:31:38 +0000 Subject: [PATCH 09/11] Make goto_programt::instructiont::validate() accept incomplete array types --- src/goto-programs/goto_program.cpp | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 20ea0a95538..9f0e1080e5a 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -728,6 +728,24 @@ void goto_programt::instructiont::validate( ns); } + if( + !symbol_expr_type_matches_symbol_table && + goto_symbol_expr.type().id() == ID_array && + to_array_type(goto_symbol_expr.type()).is_incomplete()) + { + // If the symbol expr has an incomplete array type, it may not have + // a constant size value, whereas the symbol table entry may have + // an (assumed) constant size of 1 (which mimics gcc behaviour) + if(table_symbol->type.id() == ID_array) + { + auto symbol_table_array_type = to_array_type(table_symbol->type); + symbol_table_array_type.size() = nil_exprt(); + + symbol_expr_type_matches_symbol_table = base_type_eq( + goto_symbol_expr.type(), symbol_table_array_type, ns); + } + } + DATA_CHECK_WITH_DIAGNOSTICS( vm, symbol_expr_type_matches_symbol_table, From 1d40d383ac7d1c6cdb4595543114644aeafec482 Mon Sep 17 00:00:00 2001 From: Chris Ryder Date: Thu, 24 Jan 2019 17:51:30 +0000 Subject: [PATCH 10/11] Make goto_programt::instructiont::validate() accept differing return types When a function declaration and its definition appear in different translation units they may have different return types. This commit relaxes the checks in goto_programt::instructiont::validate() in these circumstances. --- src/goto-programs/goto_program.cpp | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 9f0e1080e5a..e86093907bd 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -726,6 +726,32 @@ void goto_programt::instructiont::validate( goto_symbol_expr.type(), original_return_type(ns.get_symbol_table(), goto_id), ns); + + if( + !symbol_expr_type_matches_symbol_table && + goto_symbol_expr.type().id() == ID_code) + { + // If a function declaration and its definition are in different + // translation units they may have different return types, + // which remove_returns patches up with a typecast. If thats + // the case, then the return type in the symbol table may differ + // from the return type in the symbol expr + if( + goto_symbol_expr.type().source_location().get_file() != + table_symbol->type.source_location().get_file()) + { + // temporarily fixup the return types + auto goto_symbol_expr_type = + to_code_type(goto_symbol_expr.type()); + auto table_symbol_type = to_code_type(table_symbol->type); + + goto_symbol_expr_type.return_type() = + table_symbol_type.return_type(); + + symbol_expr_type_matches_symbol_table = + base_type_eq(goto_symbol_expr_type, table_symbol_type, ns); + } + } } if( From 933c2ef117821f05879046b6fea74ada8c9b9333 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 3 Jan 2019 13:32:33 +0000 Subject: [PATCH 11/11] enable --validate-goto-model for all cbmc regressions This will prevent the introduction of changes that violate the checks in the goto-validation procedure. --- regression/cbmc/CMakeLists.txt | 2 +- regression/cbmc/Makefile | 7 +++---- regression/cbmc/trace-values/trace-values.c | 2 ++ 3 files changed, 6 insertions(+), 5 deletions(-) diff --git a/regression/cbmc/CMakeLists.txt b/regression/cbmc/CMakeLists.txt index 1785e0f124b..bb900107e38 100644 --- a/regression/cbmc/CMakeLists.txt +++ b/regression/cbmc/CMakeLists.txt @@ -1,3 +1,3 @@ add_test_pl_tests( - "$" -X smt-backend + "$ --validate-goto-model" -X smt-backend ) diff --git a/regression/cbmc/Makefile b/regression/cbmc/Makefile index d86a43477e6..41cc877803e 100644 --- a/regression/cbmc/Makefile +++ b/regression/cbmc/Makefile @@ -1,13 +1,12 @@ -default: tests.log +default: test test: - @../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend + @../test.pl -p -c "../../../src/cbmc/cbmc --validate-goto-model" -X smt-backend test-cprover-smt2: @../test.pl -p -c "../../../src/cbmc/cbmc --cprover-smt2" -tests.log: ../test.pl - @../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend +tests.log: ../test.pl test show: @for dir in *; do \ diff --git a/regression/cbmc/trace-values/trace-values.c b/regression/cbmc/trace-values/trace-values.c index d0560a76284..da99366709d 100644 --- a/regression/cbmc/trace-values/trace-values.c +++ b/regression/cbmc/trace-values/trace-values.c @@ -1,3 +1,5 @@ +#include + int global_var; struct S