diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index 3c07e7dd46f..c00f71d26a2 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -540,7 +540,7 @@ jobs: cd ../regression/cbmc sed -i '1s/^CORE\(.*\)broken-smt-backend/KNOWNBUG\1broken-smt-backend/' */*.desc # the following tests fail on Windows only - git checkout -- memory_allocation1 printf1 union12 va_list3 + git checkout -- memory_allocation1 printf1 printf3 union12 va_list3 ../test.pl -c "cbmc --cprover-smt2" -I broken-smt-backend -K # This job takes approximately 8 to 30 minutes diff --git a/regression/cbmc/printf2/main.c b/regression/cbmc/printf2/main.c new file mode 100644 index 00000000000..30739d5c343 --- /dev/null +++ b/regression/cbmc/printf2/main.c @@ -0,0 +1,8 @@ +#include +#include + +int main() +{ + printf("results: %s, %d", "five", 5); + assert(0); +} diff --git a/regression/cbmc/printf2/test.desc b/regression/cbmc/printf2/test.desc new file mode 100644 index 00000000000..acd0e87c59c --- /dev/null +++ b/regression/cbmc/printf2/test.desc @@ -0,0 +1,8 @@ +CORE no-new-smt +main.c +--trace +^results: five, 5$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/cbmc/printf3/main.c b/regression/cbmc/printf3/main.c new file mode 100644 index 00000000000..3afda07eca8 --- /dev/null +++ b/regression/cbmc/printf3/main.c @@ -0,0 +1,12 @@ +#include +#include + +int main() +{ + printf("%ld", 10); + printf("%llu", 11); + printf("%hhd", 12); + printf("%lf", 10.0); + printf("%Lf", 11.0); + assert(0); +} diff --git a/regression/cbmc/printf3/test.desc b/regression/cbmc/printf3/test.desc new file mode 100644 index 00000000000..5efaa7b6223 --- /dev/null +++ b/regression/cbmc/printf3/test.desc @@ -0,0 +1,12 @@ +CORE broken-smt-backend no-new-smt +main.c +--trace +^10$ +^11$ +^12$ +^10.0+$ +^11.0+$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/goto-programs/printf_formatter.cpp b/src/goto-programs/printf_formatter.cpp index 98e6db06e82..afc598fbfa6 100644 --- a/src/goto-programs/printf_formatter.cpp +++ b/src/goto-programs/printf_formatter.cpp @@ -11,14 +11,15 @@ Author: Daniel Kroening, kroening@kroening.com #include "printf_formatter.h" -#include - #include +#include #include #include #include #include +#include + const exprt printf_formattert::make_type( const exprt &src, const typet &dest) { @@ -66,6 +67,8 @@ void printf_formattert::process_format(std::ostream &out) format_constant.min_width=0; format_constant.zero_padding=false; + std::string length_modifier; + char ch=next(); if(ch=='0') // leading zeros @@ -94,6 +97,56 @@ void printf_formattert::process_format(std::ostream &out) } } + switch(ch) + { + case 'h': + ch = next(); + if(ch == 'h') + { + length_modifier = "hh"; + ch = next(); + } + else + { + length_modifier = "h"; + } + break; + + case 'l': + ch = next(); + if(ch == 'l') + { + length_modifier = "ll"; + ch = next(); + } + else + { + length_modifier = "l"; + } + break; + + case 'q': + ch = next(); + length_modifier = "ll"; + break; + + case 'L': + case 'j': + case 'z': + case 't': + length_modifier = ch; + ch = next(); + break; + + case 'Z': + ch = next(); + length_modifier = "z"; + break; + + default: + break; + } + switch(ch) { case '%': @@ -105,17 +158,23 @@ void printf_formattert::process_format(std::ostream &out) format_constant.style=format_spect::stylet::SCIENTIFIC; if(next_operand==operands.end()) break; - out << format_constant( - make_type(*(next_operand++), double_type())); + if(length_modifier == "L") + out << format_constant(make_type(*(next_operand++), long_double_type())); + else + out << format_constant(make_type(*(next_operand++), double_type())); break; + case 'a': // TODO: hexadecimal output + case 'A': // TODO: hexadecimal output case 'f': case 'F': format_constant.style=format_spect::stylet::DECIMAL; if(next_operand==operands.end()) break; - out << format_constant( - make_type(*(next_operand++), double_type())); + if(length_modifier == "L") + out << format_constant(make_type(*(next_operand++), long_double_type())); + else + out << format_constant(make_type(*(next_operand++), double_type())); break; case 'g': @@ -125,10 +184,14 @@ void printf_formattert::process_format(std::ostream &out) format_constant.precision=1; if(next_operand==operands.end()) break; - out << format_constant( - make_type(*(next_operand++), double_type())); + if(length_modifier == "L") + out << format_constant(make_type(*(next_operand++), long_double_type())); + else + out << format_constant(make_type(*(next_operand++), double_type())); break; + case 'S': + length_modifier = 'l'; case 's': { if(next_operand==operands.end()) @@ -136,47 +199,115 @@ void printf_formattert::process_format(std::ostream &out) // this is the address of a string const exprt &op=*(next_operand++); if( - op.id() == ID_address_of && - to_address_of_expr(op).object().id() == ID_index && - to_index_expr(to_address_of_expr(op).object()).array().id() == - ID_string_constant) + auto pointer_constant = + expr_try_dynamic_cast(op)) { - out << format_constant( - to_index_expr(to_address_of_expr(op).object()).array()); + if( + auto address_of = expr_try_dynamic_cast( + skip_typecast(pointer_constant->symbolic_pointer()))) + { + if(address_of->object().id() == ID_string_constant) + { + out << format_constant(address_of->object()); + } + else if( + auto index_expr = + expr_try_dynamic_cast(address_of->object())) + { + if( + index_expr->index().is_zero() && + index_expr->array().id() == ID_string_constant) + { + out << format_constant(index_expr->array()); + } + } + } } } break; case 'd': + case 'i': + { if(next_operand==operands.end()) break; - out << format_constant( - make_type(*(next_operand++), signed_int_type())); + typet conversion_type; + if(length_modifier == "hh") + conversion_type = signed_char_type(); + else if(length_modifier == "h") + conversion_type = signed_short_int_type(); + else if(length_modifier == "l") + conversion_type = signed_long_int_type(); + else if(length_modifier == "ll") + conversion_type = signed_long_long_int_type(); + else if(length_modifier == "j") // intmax_t + conversion_type = signed_long_long_int_type(); + else if(length_modifier == "z") + conversion_type = signed_size_type(); + else if(length_modifier == "t") + conversion_type = pointer_diff_type(); + else + conversion_type = signed_int_type(); + out << format_constant(make_type(*(next_operand++), conversion_type)); + } break; - case 'D': - if(next_operand==operands.end()) - break; - out << format_constant( - make_type(*(next_operand++), signed_long_int_type())); + case 'o': // TODO: octal output + case 'x': // TODO: hexadecimal output + case 'X': // TODO: hexadecimal output + case 'u': + { + if(next_operand == operands.end()) + break; + typet conversion_type; + if(length_modifier == "hh") + conversion_type = unsigned_char_type(); + else if(length_modifier == "h") + conversion_type = unsigned_short_int_type(); + else if(length_modifier == "l") + conversion_type = unsigned_long_int_type(); + else if(length_modifier == "ll") + conversion_type = unsigned_long_long_int_type(); + else if(length_modifier == "j") // intmax_t + conversion_type = unsigned_long_long_int_type(); + else if(length_modifier == "z") + conversion_type = size_type(); + else if(length_modifier == "t") + conversion_type = pointer_diff_type(); + else + conversion_type = unsigned_int_type(); + out << format_constant(make_type(*(next_operand++), conversion_type)); + } break; - case 'u': - if(next_operand==operands.end()) + case 'C': + length_modifier = 'l'; + case 'c': + if(next_operand == operands.end()) + break; + if(length_modifier == "l") + out << format_constant(make_type(*(next_operand++), wchar_t_type())); + else + out << format_constant( + make_type(*(next_operand++), unsigned_char_type())); break; - out << format_constant( - make_type(*(next_operand++), unsigned_int_type())); - break; - case 'U': - if(next_operand==operands.end()) + case 'p': + // TODO: hexadecimal output + out << format_constant(make_type(*(next_operand++), size_type())); break; - out << format_constant( - make_type(*(next_operand++), unsigned_long_int_type())); - break; - default: - out << '%' << ch; + case 'n': + if(next_operand == operands.end()) + break; + // printf would store the number of characters written so far in the + // object pointed to by this operand. We do not implement this side-effect + // here, and just skip one operand. + ++next_operand; + break; + + default: + out << '%' << ch; } } diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index f20cfc9c4f3..9d3797a7247 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -397,10 +397,16 @@ void goto_symext::symex_printf( return; } + // Visual Studio has va_list == char*, else we have va_list == void** and + // need to add dereferencing + const bool need_deref = + operands.back().type().id() == ID_pointer && + to_pointer_type(operands.back().type()).base_type().id() == ID_pointer; + for(const auto &op : va_args->operands()) { exprt parameter = skip_typecast(op); - if(parameter.id() == ID_address_of) + if(need_deref && parameter.id() == ID_address_of) parameter = to_address_of_expr(parameter).object(); clean_expr(parameter, state, false); parameter = state.rename(std::move(parameter), ns).get();