Skip to content

Commit 00ae5a8

Browse files
tautschnigtautschnig
committed
Support length modifiers in printf formatting
Handle all length modifiers and conversion specifiers as laid out in printf's man page. Fixes: #7147
1 parent df4668e commit 00ae5a8

File tree

4 files changed

+167
-28
lines changed

4 files changed

+167
-28
lines changed

‎.github/workflows/pull-request-checks.yaml

+1-1
Original file line numberDiff line numberDiff line change
@@ -540,7 +540,7 @@ jobs:
540540
cd ../regression/cbmc
541541
sed -i '1s/^CORE\(.*\)broken-smt-backend/KNOWNBUG\1broken-smt-backend/' */*.desc
542542
# the following tests fail on Windows only
543-
git checkout -- memory_allocation1 printf1 union12 va_list3
543+
git checkout -- memory_allocation1 printf1 printf3 union12 va_list3
544544
../test.pl -c "cbmc --cprover-smt2" -I broken-smt-backend -K
545545
546546
# This job takes approximately 8 to 30 minutes

‎regression/cbmc/printf3/main.c

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#include <assert.h>
2+
#include <stdio.h>
3+
4+
int main()
5+
{
6+
printf("%ld", 10);
7+
printf("%llu", 11);
8+
printf("%hhd", 12);
9+
printf("%lf", 10.0);
10+
printf("%Lf", 11.0);
11+
assert(0);
12+
}

‎regression/cbmc/printf3/test.desc

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE broken-smt-backend no-new-smt
2+
main.c
3+
--trace
4+
^10$
5+
^11$
6+
^12$
7+
^10.0+$
8+
^11.0+$
9+
^EXIT=10$
10+
^SIGNAL=0$
11+
--
12+
^warning: ignoring

‎src/goto-programs/printf_formatter.cpp

+142-27
Original file line numberDiff line numberDiff line change
@@ -11,14 +11,15 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "printf_formatter.h"
1313

14-
#include <sstream>
15-
1614
#include <util/c_types.h>
15+
#include <util/expr_util.h>
1716
#include <util/format_constant.h>
1817
#include <util/pointer_expr.h>
1918
#include <util/simplify_expr.h>
2019
#include <util/std_expr.h>
2120

21+
#include <sstream>
22+
2223
const exprt printf_formattert::make_type(
2324
const exprt &src, const typet &dest)
2425
{
@@ -66,6 +67,8 @@ void printf_formattert::process_format(std::ostream &out)
6667
format_constant.min_width=0;
6768
format_constant.zero_padding=false;
6869

70+
std::string length_modifier;
71+
6972
char ch=next();
7073

7174
if(ch=='0') // leading zeros
@@ -94,6 +97,56 @@ void printf_formattert::process_format(std::ostream &out)
9497
}
9598
}
9699

100+
switch(ch)
101+
{
102+
case 'h':
103+
ch = next();
104+
if(ch == 'h')
105+
{
106+
length_modifier = "hh";
107+
ch = next();
108+
}
109+
else
110+
{
111+
length_modifier = "h";
112+
}
113+
break;
114+
115+
case 'l':
116+
ch = next();
117+
if(ch == 'l')
118+
{
119+
length_modifier = "ll";
120+
ch = next();
121+
}
122+
else
123+
{
124+
length_modifier = "l";
125+
}
126+
break;
127+
128+
case 'q':
129+
ch = next();
130+
length_modifier = "ll";
131+
break;
132+
133+
case 'L':
134+
case 'j':
135+
case 'z':
136+
case 't':
137+
length_modifier = ch;
138+
ch = next();
139+
break;
140+
141+
case 'Z':
142+
ch = next();
143+
length_modifier = "z";
144+
break;
145+
146+
default:
147+
break;
148+
}
149+
97150
switch(ch)
98151
{
99152
case '%':
@@ -105,17 +158,23 @@ void printf_formattert::process_format(std::ostream &out)
105158
format_constant.style=format_spect::stylet::SCIENTIFIC;
106159
if(next_operand==operands.end())
107160
break;
108-
out << format_constant(
109-
make_type(*(next_operand++), double_type()));
161+
if(length_modifier == "L")
162+
out << format_constant(make_type(*(next_operand++), long_double_type()));
163+
else
164+
out << format_constant(make_type(*(next_operand++), double_type()));
110165
break;
111166

167+
case 'a': // TODO: hexadecimal output
168+
case 'A': // TODO: hexadecimal output
112169
case 'f':
113170
case 'F':
114171
format_constant.style=format_spect::stylet::DECIMAL;
115172
if(next_operand==operands.end())
116173
break;
117-
out << format_constant(
118-
make_type(*(next_operand++), double_type()));
174+
if(length_modifier == "L")
175+
out << format_constant(make_type(*(next_operand++), long_double_type()));
176+
else
177+
out << format_constant(make_type(*(next_operand++), double_type()));
119178
break;
120179

121180
case 'g':
@@ -125,10 +184,14 @@ void printf_formattert::process_format(std::ostream &out)
125184
format_constant.precision=1;
126185
if(next_operand==operands.end())
127186
break;
128-
out << format_constant(
129-
make_type(*(next_operand++), double_type()));
187+
if(length_modifier == "L")
188+
out << format_constant(make_type(*(next_operand++), long_double_type()));
189+
else
190+
out << format_constant(make_type(*(next_operand++), double_type()));
130191
break;
131192

193+
case 'S':
194+
length_modifier = 'l';
132195
case 's':
133196
{
134197
if(next_operand==operands.end())
@@ -164,35 +227,87 @@ void printf_formattert::process_format(std::ostream &out)
164227
break;
165228

166229
case 'd':
230+
case 'i':
231+
{
167232
if(next_operand==operands.end())
168233
break;
169-
out << format_constant(
170-
make_type(*(next_operand++), signed_int_type()));
234+
typet conversion_type;
235+
if(length_modifier == "hh")
236+
conversion_type = signed_char_type();
237+
else if(length_modifier == "h")
238+
conversion_type = signed_short_int_type();
239+
else if(length_modifier == "l")
240+
conversion_type = signed_long_int_type();
241+
else if(length_modifier == "ll")
242+
conversion_type = signed_long_long_int_type();
243+
else if(length_modifier == "j") // intmax_t
244+
conversion_type = signed_long_long_int_type();
245+
else if(length_modifier == "z")
246+
conversion_type = signed_size_type();
247+
else if(length_modifier == "t")
248+
conversion_type = pointer_diff_type();
249+
else
250+
conversion_type = signed_int_type();
251+
out << format_constant(make_type(*(next_operand++), conversion_type));
252+
}
171253
break;
172254

173-
case 'D':
174-
if(next_operand==operands.end())
175-
break;
176-
out << format_constant(
177-
make_type(*(next_operand++), signed_long_int_type()));
255+
case 'o': // TODO: octal output
256+
case 'x': // TODO: hexadecimal output
257+
case 'X': // TODO: hexadecimal output
258+
case 'u':
259+
{
260+
if(next_operand == operands.end())
261+
break;
262+
typet conversion_type;
263+
if(length_modifier == "hh")
264+
conversion_type = unsigned_char_type();
265+
else if(length_modifier == "h")
266+
conversion_type = unsigned_short_int_type();
267+
else if(length_modifier == "l")
268+
conversion_type = unsigned_long_int_type();
269+
else if(length_modifier == "ll")
270+
conversion_type = unsigned_long_long_int_type();
271+
else if(length_modifier == "j") // intmax_t
272+
conversion_type = unsigned_long_long_int_type();
273+
else if(length_modifier == "z")
274+
conversion_type = size_type();
275+
else if(length_modifier == "t")
276+
conversion_type = pointer_diff_type();
277+
else
278+
conversion_type = unsigned_int_type();
279+
out << format_constant(make_type(*(next_operand++), conversion_type));
280+
}
178281
break;
179282

180-
case 'u':
181-
if(next_operand==operands.end())
283+
case 'C':
284+
length_modifier = 'l';
285+
case 'c':
286+
if(next_operand == operands.end())
287+
break;
288+
if(length_modifier == "l")
289+
out << format_constant(make_type(*(next_operand++), wchar_t_type()));
290+
else
291+
out << format_constant(
292+
make_type(*(next_operand++), unsigned_char_type()));
182293
break;
183-
out << format_constant(
184-
make_type(*(next_operand++), unsigned_int_type()));
185-
break;
186294

187-
case 'U':
188-
if(next_operand==operands.end())
295+
case 'p':
296+
// TODO: hexadecimal output
297+
out << format_constant(make_type(*(next_operand++), size_type()));
189298
break;
190-
out << format_constant(
191-
make_type(*(next_operand++), unsigned_long_int_type()));
192-
break;
193299

194-
default:
195-
out << '%' << ch;
300+
case 'n':
301+
if(next_operand == operands.end())
302+
break;
303+
// printf would store the number of characters written so far in the
304+
// object pointed to by this operand. We do not implement this side-effect
305+
// here, and just skip one operand.
306+
++next_operand;
307+
break;
308+
309+
default:
310+
out << '%' << ch;
196311
}
197312
}
198313

0 commit comments

Comments
 (0)