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 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..02033a2e39b 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); @@ -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; 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)); } 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; 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)); } 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/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 998eda53bd8..e86093907bd 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,75 @@ 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); + + 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( + !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, - 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); + } } }; 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( 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; }