From d590932f46732b92655cdba2938f2a4c10eeb54c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 21 Dec 2021 15:30:42 +0000 Subject: [PATCH 1/2] Improving linker warning diagnostics We previously just reported pointer type conflicts without elaborating what the exact difference was. To produce type-consistent goto programs, we chose to use the type that the definition had, but lacked any test that doing so would actually result in a program that can be analysed successfully. This commit fixes bugs in the code producing diagnostics, enables diagnostics for the case of pointer type conflicts, and adds a test to demonstrate that we successfully analyse programs after type conflict resolution. Despite this, however, inconsistencies in the goto program remain: the call types still need fixing up. Fixes: #198 --- .../ansi-c/incomplete-structs/test.desc | 12 ++ regression/ansi-c/incomplete-structs/types1.c | 9 ++ regression/ansi-c/incomplete-structs/types2.c | 16 +++ regression/ansi-c/incomplete-structs/types3.c | 17 +++ .../ansi-c/incomplete-structs/typesmain.c | 29 +++++ src/linking/linking.cpp | 105 +++++++++++------- src/linking/linking_class.h | 5 +- 7 files changed, 150 insertions(+), 43 deletions(-) create mode 100644 regression/ansi-c/incomplete-structs/test.desc create mode 100644 regression/ansi-c/incomplete-structs/types1.c create mode 100644 regression/ansi-c/incomplete-structs/types2.c create mode 100644 regression/ansi-c/incomplete-structs/types3.c create mode 100644 regression/ansi-c/incomplete-structs/typesmain.c diff --git a/regression/ansi-c/incomplete-structs/test.desc b/regression/ansi-c/incomplete-structs/test.desc new file mode 100644 index 00000000000..8a45a7a50ea --- /dev/null +++ b/regression/ansi-c/incomplete-structs/test.desc @@ -0,0 +1,12 @@ +CORE +typesmain.c +types1.c types2.c types3.c --verbosity 2 +reason for conflict at \*#this.u: number of members is different \(3/0\) +reason for conflict at \*#this.u: number of members is different \(0/3\) +struct U \(incomplete\) +warning: pointer parameter types differ between declaration and definition "bar" +warning: pointer parameter types differ between declaration and definition "foo" +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/ansi-c/incomplete-structs/types1.c b/regression/ansi-c/incomplete-structs/types1.c new file mode 100644 index 00000000000..43dec03a9e4 --- /dev/null +++ b/regression/ansi-c/incomplete-structs/types1.c @@ -0,0 +1,9 @@ +struct S +{ + int s; +} s_object; + +int foobar() +{ + return s_object.s; +} diff --git a/regression/ansi-c/incomplete-structs/types2.c b/regression/ansi-c/incomplete-structs/types2.c new file mode 100644 index 00000000000..77cb91d53cd --- /dev/null +++ b/regression/ansi-c/incomplete-structs/types2.c @@ -0,0 +1,16 @@ +struct S +{ + struct T *t; + struct U *u; +}; + +struct U +{ + struct S *s; + int j; +}; + +int bar(struct S *s) +{ + return s->u->j; +} diff --git a/regression/ansi-c/incomplete-structs/types3.c b/regression/ansi-c/incomplete-structs/types3.c new file mode 100644 index 00000000000..d3e0617b180 --- /dev/null +++ b/regression/ansi-c/incomplete-structs/types3.c @@ -0,0 +1,17 @@ +struct T +{ + int i; +}; + +struct S +{ + struct T *t; + struct U *u; +}; + +int bar(struct S *); + +int foo(struct S *s) +{ + return bar(s) + s->t->i; +} diff --git a/regression/ansi-c/incomplete-structs/typesmain.c b/regression/ansi-c/incomplete-structs/typesmain.c new file mode 100644 index 00000000000..13e80a03bb2 --- /dev/null +++ b/regression/ansi-c/incomplete-structs/typesmain.c @@ -0,0 +1,29 @@ +#include + +struct T +{ + int i; +}; + +struct U +{ + struct S *s; + int j; +}; + +struct S +{ + struct T *t; + struct U *u; +}; + +int foo(struct S *s); + +int main() +{ + struct T t = {10}; + struct U u = {0, 32}; + struct S s = {&t, &u}; + int res = foo(&s); + assert(res == 42); +} diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index 0b175ddc522..dc37e7cc192 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -126,7 +126,7 @@ std::string linkingt::type_to_string_verbose( return type_to_string(symbol.name, type); } -void linkingt::detailed_conflict_report_rec( +bool linkingt::detailed_conflict_report_rec( const symbolt &old_symbol, const symbolt &new_symbol, const typet &type1, @@ -134,9 +134,11 @@ void linkingt::detailed_conflict_report_rec( unsigned depth, exprt &conflict_path) { - #ifdef DEBUG + bool conclusive = false; + +#ifdef DEBUG debug() << "" << eom; - #endif +#endif std::string msg; @@ -144,7 +146,10 @@ void linkingt::detailed_conflict_report_rec( const typet &t2=follow_tags_symbols(ns, type2); if(t1.id()!=t2.id()) + { msg="type classes differ"; + conclusive = true; + } else if(t1.id()==ID_pointer || t1.id()==ID_array) { @@ -155,7 +160,7 @@ void linkingt::detailed_conflict_report_rec( if(conflict_path.type().id() == ID_pointer) conflict_path = dereference_exprt(conflict_path); - detailed_conflict_report_rec( + conclusive = detailed_conflict_report_rec( old_symbol, new_symbol, to_type_with_subtype(t1).subtype(), @@ -184,6 +189,7 @@ void linkingt::detailed_conflict_report_rec( msg="number of members is different ("; msg+=std::to_string(components1.size())+'/'; msg+=std::to_string(components2.size())+')'; + conclusive = true; } else { @@ -197,7 +203,7 @@ void linkingt::detailed_conflict_report_rec( msg="names of member "+std::to_string(i)+" differ ("; msg+=id2string(components1[i].get_name())+'/'; msg+=id2string(components2[i].get_name())+')'; - break; + conclusive = true; } else if(subtype1 != subtype2) { @@ -210,6 +216,7 @@ void linkingt::detailed_conflict_report_rec( e.id()==ID_index) { parent_types.insert(e.type()); + parent_types.insert(follow_tags_symbols(ns, e.type())); if(e.id() == ID_dereference) e = to_dereference_expr(e).pointer(); else if(e.id() == ID_member) @@ -220,44 +227,32 @@ void linkingt::detailed_conflict_report_rec( UNREACHABLE; } - conflict_path=conflict_path_before; - conflict_path.type()=t1; - conflict_path= - member_exprt(conflict_path, components1[i]); - - if(depth>0 && - parent_types.find(t1)==parent_types.end()) - detailed_conflict_report_rec( - old_symbol, - new_symbol, - subtype1, - subtype2, - depth-1, - conflict_path); - else + if(parent_types.find(subtype1) == parent_types.end()) { - msg="type of member "+ - id2string(components1[i].get_name())+ - " differs"; - if(depth>0) + conflict_path = conflict_path_before; + conflict_path.type() = t1; + conflict_path = member_exprt(conflict_path, components1[i]); + + if(depth > 0) { - std::string msg_bak; - msg_bak.swap(msg); - symbol_exprt c = symbol_exprt::typeless(ID_C_this); - detailed_conflict_report_rec( + conclusive = detailed_conflict_report_rec( old_symbol, new_symbol, subtype1, subtype2, - depth-1, - c); - msg.swap(msg_bak); + depth - 1, + conflict_path); } } - - if(parent_types.find(t1)==parent_types.end()) - break; + else + { + msg = "type of member " + id2string(components1[i].get_name()) + + " differs (recursive)"; + } } + + if(conclusive) + break; } } } @@ -280,12 +275,14 @@ void linkingt::detailed_conflict_report_rec( msg += type_to_string(new_symbol.name, to_c_enum_type(t2).underlying_type()) + ')'; + conclusive = true; } else if(members1.size()!=members2.size()) { msg="number of enum members is different ("; msg+=std::to_string(members1.size())+'/'; msg+=std::to_string(members2.size())+')'; + conclusive = true; } else { @@ -296,15 +293,18 @@ void linkingt::detailed_conflict_report_rec( msg="names of member "+std::to_string(i)+" differ ("; msg+=id2string(members1[i].get_base_name())+'/'; msg+=id2string(members2[i].get_base_name())+')'; - break; + conclusive = true; } else if(members1[i].get_value()!=members2[i].get_value()) { msg="values of member "+std::to_string(i)+" differ ("; msg+=id2string(members1[i].get_value())+'/'; msg+=id2string(members2[i].get_value())+')'; - break; + conclusive = true; } + + if(conclusive) + break; } } @@ -328,21 +328,25 @@ void linkingt::detailed_conflict_report_rec( msg="parameter counts differ ("; msg+=std::to_string(parameters1.size())+'/'; msg+=std::to_string(parameters2.size())+')'; + conclusive = true; } else if(return_type1 != return_type2) { + conflict_path.type() = array_typet{void_type(), nil_exprt{}}; conflict_path= index_exprt(conflict_path, constant_exprt(std::to_string(-1), integer_typet())); if(depth>0) - detailed_conflict_report_rec( + { + conclusive = detailed_conflict_report_rec( old_symbol, new_symbol, return_type1, return_type2, - depth-1, + depth - 1, conflict_path); + } else msg="return types differ"; } @@ -355,30 +359,37 @@ void linkingt::detailed_conflict_report_rec( if(subtype1 != subtype2) { + conflict_path.type() = array_typet{void_type(), nil_exprt{}}; conflict_path= index_exprt(conflict_path, constant_exprt(std::to_string(i), integer_typet())); if(depth>0) - detailed_conflict_report_rec( + { + conclusive = detailed_conflict_report_rec( old_symbol, new_symbol, subtype1, subtype2, - depth-1, + depth - 1, conflict_path); + } else msg="parameter types differ"; + } + if(conclusive) break; - } } } } else + { msg="conflict on POD"; + conclusive = true; + } - if(!msg.empty()) + if(conclusive && !msg.empty()) { error() << '\n'; error() << "reason for conflict at " @@ -392,6 +403,8 @@ void linkingt::detailed_conflict_report_rec( #ifdef DEBUG debug() << "" << eom; #endif + + return conclusive; } void linkingt::link_error( @@ -685,8 +698,16 @@ void linkingt::duplicate_code_symbol( old_symbol.value.is_nil()!=new_symbol.value.is_nil()) { if(warn_msg.empty()) + { warn_msg="pointer parameter types differ between " "declaration and definition"; + detailed_conflict_report( + old_symbol, + new_symbol, + conflicts.front().first, + conflicts.front().second); + } + replace=new_symbol.value.is_not_nil(); } // transparent union with (or entirely without) implementation is diff --git a/src/linking/linking_class.h b/src/linking/linking_class.h index c445fb1dc94..2586597e769 100644 --- a/src/linking/linking_class.h +++ b/src/linking/linking_class.h @@ -131,7 +131,10 @@ class linkingt:public typecheckt return type_to_string_verbose(symbol, symbol.type); } - void detailed_conflict_report_rec( + /// Returns true iff the conflict report on a particular branch of the tree of + /// types was a definitive result, and not contingent on conflicts within a + /// tag type. + bool detailed_conflict_report_rec( const symbolt &old_symbol, const symbolt &new_symbol, const typet &type1, From 39e7078c1381557c1f179105f752e0bc0c22e2ee Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 25 Dec 2021 21:45:41 +0000 Subject: [PATCH 2/2] Linking: actually replace code type information in expressions The linker already accepted a number of type mismatches for function declarations, but did not actually modify the goto functions to reflect these type mismatches, just the type information in the symbol table was updated. These changes enable support for conflicts on function return types, which are now resolved by introducing type casts. --- regression/ansi-c/undeclared_function/fileB.c | 5 +- .../undeclared_function1.desc | 2 +- .../incomplete-structs/test.desc | 3 +- .../incomplete-structs/types1.c | 0 .../incomplete-structs/types2.c | 0 .../incomplete-structs/types3.c | 0 .../incomplete-structs/typesmain.c | 0 regression/cbmc/return6/test.desc | 5 +- regression/linking-goto-binaries/chain.sh | 2 +- .../type_conflicts/Linking7-main.c | 19 +++ .../type_conflicts/Linking7-module.c | 32 ++++ .../type_conflicts/Linking7-module2.c | 32 ++++ .../type_conflicts/Linking7-return_type1.c | 13 ++ .../type_conflicts/Linking7-return_type2.c | 10 ++ .../type_conflicts/member-name-mismatch.desc | 11 ++ .../type_conflicts/return_type.desc | 10 ++ .../type_conflicts/test.desc | 11 ++ src/goto-programs/link_goto_model.cpp | 30 +++- src/linking/linking.cpp | 147 ++++++++++++------ src/linking/linking_class.h | 5 + 20 files changed, 274 insertions(+), 63 deletions(-) rename regression/{ansi-c => cbmc}/incomplete-structs/test.desc (88%) rename regression/{ansi-c => cbmc}/incomplete-structs/types1.c (100%) rename regression/{ansi-c => cbmc}/incomplete-structs/types2.c (100%) rename regression/{ansi-c => cbmc}/incomplete-structs/types3.c (100%) rename regression/{ansi-c => cbmc}/incomplete-structs/typesmain.c (100%) create mode 100644 regression/linking-goto-binaries/type_conflicts/Linking7-main.c create mode 100644 regression/linking-goto-binaries/type_conflicts/Linking7-module.c create mode 100644 regression/linking-goto-binaries/type_conflicts/Linking7-module2.c create mode 100644 regression/linking-goto-binaries/type_conflicts/Linking7-return_type1.c create mode 100644 regression/linking-goto-binaries/type_conflicts/Linking7-return_type2.c create mode 100644 regression/linking-goto-binaries/type_conflicts/member-name-mismatch.desc create mode 100644 regression/linking-goto-binaries/type_conflicts/return_type.desc create mode 100644 regression/linking-goto-binaries/type_conflicts/test.desc diff --git a/regression/ansi-c/undeclared_function/fileB.c b/regression/ansi-c/undeclared_function/fileB.c index 08bdda49110..5ac12a5caa1 100644 --- a/regression/ansi-c/undeclared_function/fileB.c +++ b/regression/ansi-c/undeclared_function/fileB.c @@ -1,4 +1,7 @@ -#include +void *malloc(__CPROVER_size_t s) +{ + return (void *)0 + s; +} int f() { diff --git a/regression/ansi-c/undeclared_function/undeclared_function1.desc b/regression/ansi-c/undeclared_function/undeclared_function1.desc index d002ebcf531..a1d43feedbd 100644 --- a/regression/ansi-c/undeclared_function/undeclared_function1.desc +++ b/regression/ansi-c/undeclared_function/undeclared_function1.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE gcc-only fileA.c fileB.c --validate-goto-model ^EXIT=0$ diff --git a/regression/ansi-c/incomplete-structs/test.desc b/regression/cbmc/incomplete-structs/test.desc similarity index 88% rename from regression/ansi-c/incomplete-structs/test.desc rename to regression/cbmc/incomplete-structs/test.desc index 8a45a7a50ea..47de5a75263 100644 --- a/regression/ansi-c/incomplete-structs/test.desc +++ b/regression/cbmc/incomplete-structs/test.desc @@ -1,11 +1,12 @@ CORE typesmain.c -types1.c types2.c types3.c --verbosity 2 +types1.c types2.c types3.c reason for conflict at \*#this.u: number of members is different \(3/0\) reason for conflict at \*#this.u: number of members is different \(0/3\) struct U \(incomplete\) warning: pointer parameter types differ between declaration and definition "bar" warning: pointer parameter types differ between declaration and definition "foo" +^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/ansi-c/incomplete-structs/types1.c b/regression/cbmc/incomplete-structs/types1.c similarity index 100% rename from regression/ansi-c/incomplete-structs/types1.c rename to regression/cbmc/incomplete-structs/types1.c diff --git a/regression/ansi-c/incomplete-structs/types2.c b/regression/cbmc/incomplete-structs/types2.c similarity index 100% rename from regression/ansi-c/incomplete-structs/types2.c rename to regression/cbmc/incomplete-structs/types2.c diff --git a/regression/ansi-c/incomplete-structs/types3.c b/regression/cbmc/incomplete-structs/types3.c similarity index 100% rename from regression/ansi-c/incomplete-structs/types3.c rename to regression/cbmc/incomplete-structs/types3.c diff --git a/regression/ansi-c/incomplete-structs/typesmain.c b/regression/cbmc/incomplete-structs/typesmain.c similarity index 100% rename from regression/ansi-c/incomplete-structs/typesmain.c rename to regression/cbmc/incomplete-structs/typesmain.c diff --git a/regression/cbmc/return6/test.desc b/regression/cbmc/return6/test.desc index 2fc10d239b2..bf09360fa4c 100644 --- a/regression/cbmc/return6/test.desc +++ b/regression/cbmc/return6/test.desc @@ -1,9 +1,8 @@ CORE main.c f_def.c -^EXIT=6$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ ^SIGNAL=0$ -CONVERSION ERROR -- ^warning: ignoring -^VERIFICATION SUCCESSFUL$ diff --git a/regression/linking-goto-binaries/chain.sh b/regression/linking-goto-binaries/chain.sh index efe0cdf23a9..d74593341a0 100755 --- a/regression/linking-goto-binaries/chain.sh +++ b/regression/linking-goto-binaries/chain.sh @@ -21,4 +21,4 @@ else $goto_cc "${main}.gb" "${next}.gb" -o "final.gb" fi -$cbmc "final.gb" +$cbmc --validate-goto-model "final.gb" diff --git a/regression/linking-goto-binaries/type_conflicts/Linking7-main.c b/regression/linking-goto-binaries/type_conflicts/Linking7-main.c new file mode 100644 index 00000000000..5233bb3b3ff --- /dev/null +++ b/regression/linking-goto-binaries/type_conflicts/Linking7-main.c @@ -0,0 +1,19 @@ +struct S +{ + void *a; + void *b; +}; + +typedef void (*fptr)(struct S); + +extern void foo(struct S s); + +fptr A[] = {foo}; + +extern void bar(); + +int main() +{ + bar(); + return 0; +} diff --git a/regression/linking-goto-binaries/type_conflicts/Linking7-module.c b/regression/linking-goto-binaries/type_conflicts/Linking7-module.c new file mode 100644 index 00000000000..8a790b3f49d --- /dev/null +++ b/regression/linking-goto-binaries/type_conflicts/Linking7-module.c @@ -0,0 +1,32 @@ +#include + +struct S +{ + void *a; + void *b; +}; + +typedef void (*fptr)(struct S); + +extern fptr A[1]; + +struct real_S +{ + int *a; + int *b; +}; + +void foo(struct real_S g) +{ + assert(*g.a == 42); + assert(*g.b == 41); +} + +void bar() +{ + int x = 42; + struct real_S s; + s.a = &x; + s.b = &x; + A[0]((struct S){s.a, s.b}); +} diff --git a/regression/linking-goto-binaries/type_conflicts/Linking7-module2.c b/regression/linking-goto-binaries/type_conflicts/Linking7-module2.c new file mode 100644 index 00000000000..bf7f87eaf8f --- /dev/null +++ b/regression/linking-goto-binaries/type_conflicts/Linking7-module2.c @@ -0,0 +1,32 @@ +#include + +struct S +{ + void *a; + void *b; +}; + +typedef void (*fptr)(struct S); + +extern fptr A[1]; + +struct real_S +{ + int *a; + int *c; +}; + +void foo(struct real_S g) +{ + assert(*g.a == 42); + assert(*g.c == 41); +} + +void bar() +{ + int x = 42; + struct real_S s; + s.a = &x; + s.c = &x; + A[0]((struct S){s.a, s.c}); +} diff --git a/regression/linking-goto-binaries/type_conflicts/Linking7-return_type1.c b/regression/linking-goto-binaries/type_conflicts/Linking7-return_type1.c new file mode 100644 index 00000000000..eb05a3e45c8 --- /dev/null +++ b/regression/linking-goto-binaries/type_conflicts/Linking7-return_type1.c @@ -0,0 +1,13 @@ +#include + +struct S +{ + int i; +}; + +struct S *function(); + +int main() +{ + assert(function() != 0); +} diff --git a/regression/linking-goto-binaries/type_conflicts/Linking7-return_type2.c b/regression/linking-goto-binaries/type_conflicts/Linking7-return_type2.c new file mode 100644 index 00000000000..598484e7095 --- /dev/null +++ b/regression/linking-goto-binaries/type_conflicts/Linking7-return_type2.c @@ -0,0 +1,10 @@ +struct S +{ + int i; + int j; // extra member +} some_var; + +struct S *function() +{ + return &some_var; +} diff --git a/regression/linking-goto-binaries/type_conflicts/member-name-mismatch.desc b/regression/linking-goto-binaries/type_conflicts/member-name-mismatch.desc new file mode 100644 index 00000000000..317b01d93d1 --- /dev/null +++ b/regression/linking-goto-binaries/type_conflicts/member-name-mismatch.desc @@ -0,0 +1,11 @@ +CORE +Linking7-main.c +Linking7-module2.c +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +line 21 assertion \*g\.a == 42: SUCCESS +line 22 assertion \*g\.c == 41: FAILURE +^\*\* 1 of 3 failed +-- +^warning: ignoring diff --git a/regression/linking-goto-binaries/type_conflicts/return_type.desc b/regression/linking-goto-binaries/type_conflicts/return_type.desc new file mode 100644 index 00000000000..2854da5c7c6 --- /dev/null +++ b/regression/linking-goto-binaries/type_conflicts/return_type.desc @@ -0,0 +1,10 @@ +CORE +Linking7-return_type1.c +Linking7-return_type2.c +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Note issue #3081 diff --git a/regression/linking-goto-binaries/type_conflicts/test.desc b/regression/linking-goto-binaries/type_conflicts/test.desc new file mode 100644 index 00000000000..938fac85344 --- /dev/null +++ b/regression/linking-goto-binaries/type_conflicts/test.desc @@ -0,0 +1,11 @@ +CORE +Linking7-main.c +Linking7-module.c +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +^\*\* 1 of 3 failed +line 21 assertion \*g\.a == 42: SUCCESS +line 22 assertion \*g\.b == 41: FAILURE +-- +^warning: ignoring diff --git a/src/goto-programs/link_goto_model.cpp b/src/goto-programs/link_goto_model.cpp index 75141785e53..f3207e6a5fa 100644 --- a/src/goto-programs/link_goto_model.cpp +++ b/src/goto-programs/link_goto_model.cpp @@ -148,7 +148,7 @@ void finalize_linking( goto_modelt &dest, const replace_symbolt::expr_mapt &type_updates) { - unchecked_replace_symbolt object_type_updates; + casting_replace_symbolt object_type_updates; object_type_updates.get_expr_map().insert( type_updates.begin(), type_updates.end()); @@ -196,10 +196,30 @@ void finalize_linking( { for(auto &instruction : gf_entry.second.body.instructions) { - instruction.transform([&object_type_updates](exprt expr) { - object_type_updates(expr); - return expr; - }); + if(instruction.is_function_call()) + { + const bool changed = + !object_type_updates.replace(instruction.call_function()); + if(changed && instruction.call_lhs().is_not_nil()) + { + object_type_updates(instruction.call_lhs()); + if( + instruction.call_lhs().type() != + to_code_type(instruction.call_function().type()).return_type()) + { + instruction.call_lhs() = typecast_exprt{ + instruction.call_lhs(), + to_code_type(instruction.call_function().type()).return_type()}; + } + } + } + else + { + instruction.transform([&object_type_updates](exprt expr) { + const bool changed = !object_type_updates.replace(expr); + return changed ? optionalt{expr} : nullopt; + }); + } } } } diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index dc37e7cc192..c365be90f2e 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -10,9 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com /// ANSI-C Linking #include "linking.h" - -#include -#include +#include "linking_class.h" #include #include @@ -20,11 +18,77 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include -#include "linking_class.h" +#include + +bool casting_replace_symbolt::replace(exprt &dest) const +{ + bool result = true; // unchanged + + // first look at type + + const exprt &const_dest(dest); + if(have_to_replace(const_dest.type())) + if(!replace_symbolt::replace(dest.type())) + result = false; + + // now do expression itself + + if(!have_to_replace(dest)) + return result; + + if(dest.id() == ID_side_effect) + { + if(auto call = expr_try_dynamic_cast(dest)) + { + if(!have_to_replace(call->function())) + return replace_symbolt::replace(dest); + + exprt before = dest; + code_typet type = to_code_type(call->function().type()); + + result &= replace_symbolt::replace(call->function()); + + // maybe add type casts here? + for(auto &arg : call->arguments()) + result &= replace_symbolt::replace(arg); + + if( + type.return_type() != + to_code_type(call->function().type()).return_type()) + { + call->type() = to_code_type(call->function().type()).return_type(); + dest = typecast_exprt(*call, type.return_type()); + result = true; + } + + return result; + } + } + else if(dest.id() == ID_address_of) + { + pointer_typet ptr_type = to_pointer_type(dest.type()); + + result &= replace_symbolt::replace(dest); + + address_of_exprt address_of = to_address_of_expr(dest); + if(address_of.object().type() != ptr_type.base_type()) + { + to_pointer_type(address_of.type()).base_type() = + address_of.object().type(); + dest = typecast_exprt{address_of, std::move(ptr_type)}; + result = true; + } + + return result; + } + + return replace_symbolt::replace(dest); +} bool casting_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const { @@ -35,7 +99,7 @@ bool casting_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const const exprt &e = it->second; - if(e.type().id() != ID_array) + if(e.type().id() != ID_array && e.type().id() != ID_code) { typet type = s.type(); static_cast(s) = typecast_exprt::conditional_cast(e, type); @@ -490,19 +554,9 @@ void linkingt::duplicate_code_symbol( const code_typet &old_t=to_code_type(old_symbol.type); const code_typet &new_t=to_code_type(new_symbol.type); - // if one of them was an implicit declaration then only conflicts on the - // return type are an error as we would end up with assignments with - // mismatching types; as we currently do not patch these by inserting type - // casts we need to fail hard if(old_symbol.type.get_bool(ID_C_incomplete) && old_symbol.value.is_nil()) { - if(old_t.return_type() == new_t.return_type()) - link_warning(old_symbol, new_symbol, "implicit function declaration"); - else - link_error( - old_symbol, - new_symbol, - "implicit function declaration"); + link_warning(old_symbol, new_symbol, "implicit function declaration"); old_symbol.type=new_symbol.type; old_symbol.location=new_symbol.location; @@ -511,24 +565,16 @@ void linkingt::duplicate_code_symbol( else if( new_symbol.type.get_bool(ID_C_incomplete) && new_symbol.value.is_nil()) { - if(old_t.return_type() == new_t.return_type()) - link_warning( - old_symbol, - new_symbol, - "ignoring conflicting implicit function declaration"); - else - link_error( - old_symbol, - new_symbol, - "implicit function declaration"); + link_warning( + old_symbol, + new_symbol, + "ignoring conflicting implicit function declaration"); } // handle (incomplete) function prototypes - else if( - old_t.return_type() == new_t.return_type() && - ((old_t.parameters().empty() && old_t.has_ellipsis() && - old_symbol.value.is_nil()) || - (new_t.parameters().empty() && new_t.has_ellipsis() && - new_symbol.value.is_nil()))) + else if(((old_t.parameters().empty() && old_t.has_ellipsis() && + old_symbol.value.is_nil()) || + (new_t.parameters().empty() && new_t.has_ellipsis() && + new_symbol.value.is_nil()))) { if(old_t.parameters().empty() && old_t.has_ellipsis() && @@ -578,9 +624,7 @@ void linkingt::duplicate_code_symbol( } // conflicting declarations without a definition, matching return // types - else if( - old_t.return_type() == new_t.return_type() && old_symbol.value.is_nil() && - new_symbol.value.is_nil()) + else if(old_symbol.value.is_nil() && new_symbol.value.is_nil()) { link_warning( old_symbol, @@ -620,8 +664,11 @@ void linkingt::duplicate_code_symbol( conflictst conflicts; if(old_t.return_type() != new_t.return_type()) - conflicts.push_back( - std::make_pair(old_t.return_type(), new_t.return_type())); + { + link_warning(old_symbol, new_symbol, "conflicting return types"); + + conflicts.emplace_back(old_t.return_type(), new_t.return_type()); + } code_typet::parameterst::const_iterator n_it=new_t.parameters().begin(), @@ -671,21 +718,11 @@ void linkingt::duplicate_code_symbol( const typet &t1=follow_tags_symbols(ns, conflicts.front().first); const typet &t2=follow_tags_symbols(ns, conflicts.front().second); - // void vs. non-void return type may be acceptable if the - // return value is never used - if((t1.id()==ID_empty || t2.id()==ID_empty) && - (old_symbol.value.is_nil() || new_symbol.value.is_nil())) - { - if(warn_msg.empty()) - warn_msg="void/non-void return type conflict on function"; - replace= - new_symbol.value.is_not_nil() || - (old_symbol.value.is_nil() && t2.id()==ID_empty); - } // different pointer arguments without implementation may work - else if((t1.id()==ID_pointer || t2.id()==ID_pointer) && - pointer_offset_bits(t1, ns)==pointer_offset_bits(t2, ns) && - old_symbol.value.is_nil() && new_symbol.value.is_nil()) + if( + (t1.id() == ID_pointer || t2.id() == ID_pointer) && + pointer_offset_bits(t1, ns) == pointer_offset_bits(t2, ns) && + old_symbol.value.is_nil() && new_symbol.value.is_nil()) { if(warn_msg.empty()) warn_msg="different pointer types in extern function"; @@ -788,6 +825,9 @@ void linkingt::duplicate_code_symbol( } } } + + object_type_updates.insert( + old_symbol.symbol_expr(), old_symbol.symbol_expr()); } if(!new_symbol.value.is_nil()) @@ -802,6 +842,11 @@ void linkingt::duplicate_code_symbol( old_symbol.is_weak=new_symbol.is_weak; old_symbol.location=new_symbol.location; old_symbol.is_macro=new_symbol.is_macro; + + // replace any previous update + object_type_updates.erase(old_symbol.name); + object_type_updates.insert( + old_symbol.symbol_expr(), old_symbol.symbol_expr()); } else if(to_code_type(old_symbol.type).get_inlined()) { diff --git a/src/linking/linking_class.h b/src/linking/linking_class.h index 2586597e769..9fbb9c9b6b5 100644 --- a/src/linking/linking_class.h +++ b/src/linking/linking_class.h @@ -19,8 +19,13 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + class casting_replace_symbolt : public replace_symbolt { +public: + bool replace(exprt &dest) const override; + private: bool replace_symbol_expr(symbol_exprt &dest) const override; };