Skip to content

Commit f1cfe44

Browse files
polgreenpolgreen
committed
represent numerical values in CBMC trace in hex
1 parent b58813b commit f1cfe44

File tree

6 files changed

+130
-44
lines changed

6 files changed

+130
-44
lines changed

‎regression/cbmc/hex_trace/main.c

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
int main()
2+
{
3+
int a;
4+
unsigned int b;
5+
a = 0;
6+
a = -100;
7+
a = 2147483647;
8+
b = a*2;
9+
a = -2147483647;
10+
__CPROVER_assert(0,"");
11+
12+
}

‎regression/cbmc/hex_trace/test.desc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
--trace-hex --trace
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
a=0 \s*\(0x0\)
7+
b=0u \s*\(0x0\)
8+
a=-100 \s*\(0xFFFFFF9C\)
9+
a=2147483647 \s*\(0x7FFFFFFF\)
10+
b=4294967294u \s*\(0xFFFFFFFE\)
11+
a=-2147483647 \s*\(0x80000001\)
12+
^VERIFICATION FAILED$
13+
--
14+
^warning: ignoring

‎src/cbmc/all_properties.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -175,7 +175,8 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
175175
if(g.second.status==goalt::statust::FAILURE)
176176
{
177177
result() << "\n" << "Trace for " << g.first << ":" << "\n";
178-
show_goto_trace(result(), bmc.ns, g.second.goto_trace);
178+
show_goto_trace(
179+
result(), bmc.ns, g.second.goto_trace, bmc.trace_options());
179180
}
180181
}
181182
result() << eom;

‎src/cbmc/bmc.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ void bmct::error_trace()
5555
{
5656
case ui_message_handlert::uit::PLAIN:
5757
result() << "Counterexample:" << eom;
58-
show_goto_trace(result(), ns, goto_trace);
58+
show_goto_trace(result(), ns, goto_trace, trace_options());
5959
result() << eom;
6060
break;
6161

‎src/goto-programs/goto_trace.cpp

Lines changed: 69 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -104,9 +104,42 @@ void goto_trace_stept::output(
104104
out << '\n';
105105
}
106106

107-
std::string trace_value_binary(
107+
static std::string
108+
numeric_representation(const exprt &expr, const trace_optionst &options)
109+
{
110+
std::string result;
111+
std::string prefix;
112+
if(options.hex_representation)
113+
{
114+
mp_integer value_int =
115+
binary2integer(id2string(to_constant_expr(expr).get_value()), false);
116+
result = integer2string(value_int, 16);
117+
prefix = "0x";
118+
}
119+
else
120+
{
121+
prefix = "0b";
122+
result = expr.get_string(ID_value);
123+
}
124+
125+
std::ostringstream oss;
126+
std::string::size_type i = 0;
127+
for(const auto c : result)
128+
{
129+
oss << c;
130+
if(++i % 8 == 0 && result.size() != i)
131+
oss << ' ';
132+
}
133+
if(options.base_prefix)
134+
return prefix + oss.str();
135+
else
136+
return oss.str();
137+
}
138+
139+
std::string trace_value_lowlevel(
108140
const exprt &expr,
109-
const namespacet &ns)
141+
const namespacet &ns,
142+
const trace_optionst &options)
110143
{
111144
const typet &type=ns.follow(expr.type());
112145

@@ -123,18 +156,8 @@ std::string trace_value_binary(
123156
type.id()==ID_c_enum ||
124157
type.id()==ID_c_enum_tag)
125158
{
126-
const std::string & str = expr.get_string(ID_value);
127-
128-
std::ostringstream oss;
129-
std::string::size_type i = 0;
130-
for(const auto c : str)
131-
{
132-
oss << c;
133-
if(++i % 8 == 0 && str.size() != i)
134-
oss << ' ';
135-
}
136-
137-
return oss.str();
159+
const std::string &str = numeric_representation(expr, options);
160+
return str;
138161
}
139162
else if(type.id()==ID_bool)
140163
{
@@ -157,7 +180,7 @@ std::string trace_value_binary(
157180
result="{ ";
158181
else
159182
result+=", ";
160-
result+=trace_value_binary(*it, ns);
183+
result+=trace_value_lowlevel(*it, ns, options);
161184
}
162185

163186
return result+" }";
@@ -170,15 +193,15 @@ std::string trace_value_binary(
170193
{
171194
if(it!=expr.operands().begin())
172195
result+=", ";
173-
result+=trace_value_binary(*it, ns);
196+
result+=trace_value_lowlevel(*it, ns, options);
174197
}
175198

176199
return result+" }";
177200
}
178201
else if(expr.id()==ID_union)
179202
{
180-
assert(expr.operands().size()==1);
181-
return trace_value_binary(expr.op0(), ns);
203+
PRECONDITION(expr.operands().size()==1);
204+
return trace_value_lowlevel(expr.op0(), ns, options);
182205
}
183206

184207
return "?";
@@ -189,7 +212,8 @@ void trace_value(
189212
const namespacet &ns,
190213
const ssa_exprt &lhs_object,
191214
const exprt &full_lhs,
192-
const exprt &value)
215+
const exprt &value,
216+
const trace_optionst &options)
193217
{
194218
irep_idt identifier;
195219

@@ -205,7 +229,7 @@ void trace_value(
205229
value_string=from_expr(ns, identifier, value);
206230

207231
// the binary representation
208-
value_string+=" ("+trace_value_binary(value, ns)+")";
232+
value_string += " (" + trace_value_lowlevel(value, ns, options) + ")";
209233
}
210234

211235
out << " "
@@ -247,7 +271,8 @@ bool is_index_member_symbol(const exprt &src)
247271
void show_goto_trace(
248272
std::ostream &out,
249273
const namespacet &ns,
250-
const goto_tracet &goto_trace)
274+
const goto_tracet &goto_trace,
275+
const trace_optionst &options)
251276
{
252277
unsigned prev_step_nr=0;
253278
bool first_step=true;
@@ -315,10 +340,20 @@ void show_goto_trace(
315340
// see if the full lhs is something clean
316341
if(is_index_member_symbol(step.full_lhs))
317342
trace_value(
318-
out, ns, step.lhs_object, step.full_lhs, step.full_lhs_value);
343+
out,
344+
ns,
345+
step.lhs_object,
346+
step.full_lhs,
347+
step.full_lhs_value,
348+
options);
319349
else
320350
trace_value(
321-
out, ns, step.lhs_object, step.lhs_object, step.lhs_object_value);
351+
out,
352+
ns,
353+
step.lhs_object,
354+
step.lhs_object,
355+
step.lhs_object_value,
356+
options);
322357
}
323358
break;
324359

@@ -330,7 +365,8 @@ void show_goto_trace(
330365
show_state_header(out, step, step.pc->source_location, step.step_nr);
331366
}
332367

333-
trace_value(out, ns, step.lhs_object, step.full_lhs, step.full_lhs_value);
368+
trace_value(
369+
out, ns, step.lhs_object, step.full_lhs, step.full_lhs_value, options);
334370
break;
335371

336372
case goto_trace_stept::typet::OUTPUT:
@@ -356,7 +392,7 @@ void show_goto_trace(
356392
out << " " << from_expr(ns, step.pc->function, *l_it);
357393

358394
// the binary representation
359-
out << " (" << trace_value_binary(*l_it, ns) << ")";
395+
out << " (" << trace_value_lowlevel(*l_it, ns, options) << ")";
360396
}
361397

362398
out << "\n";
@@ -377,7 +413,7 @@ void show_goto_trace(
377413
out << " " << from_expr(ns, step.pc->function, *l_it);
378414

379415
// the binary representation
380-
out << " (" << trace_value_binary(*l_it, ns) << ")";
416+
out << " (" << trace_value_lowlevel(*l_it, ns, options) << ")";
381417
}
382418

383419
out << "\n";
@@ -401,5 +437,12 @@ void show_goto_trace(
401437
}
402438
}
403439

440+
void show_goto_trace(
441+
std::ostream &out,
442+
const namespacet &ns,
443+
const goto_tracet &goto_trace)
444+
{
445+
show_goto_trace(out, ns, goto_trace, trace_optionst::default_options);
446+
}
404447

405448
const trace_optionst trace_optionst::default_options = trace_optionst();

‎src/goto-programs/goto_trace.h

Lines changed: 32 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -195,45 +195,61 @@ class goto_tracet
195195
}
196196
};
197197

198-
void show_goto_trace(
199-
std::ostream &out,
200-
const namespacet &,
201-
const goto_tracet &);
202-
203-
void trace_value(
204-
std::ostream &out,
205-
const namespacet &,
206-
const ssa_exprt &lhs_object,
207-
const exprt &full_lhs,
208-
const exprt &value);
209-
210-
211198
struct trace_optionst
212199
{
213200
bool json_full_lhs;
201+
bool hex_representation;
202+
bool base_prefix;
214203

215204
static const trace_optionst default_options;
216205

217206
explicit trace_optionst(const optionst &options)
218207
{
219208
json_full_lhs = options.get_bool_option("trace-json-extended");
209+
hex_representation = options.get_bool_option("trace-hex");
210+
base_prefix = hex_representation;
220211
};
221212

222213
private:
223214
trace_optionst()
224215
{
225216
json_full_lhs = false;
217+
hex_representation = false;
218+
base_prefix = false;
226219
};
227220
};
228221

229-
#define OPT_GOTO_TRACE "(trace-json-extended)"
222+
void show_goto_trace(
223+
std::ostream &out,
224+
const namespacet &,
225+
const goto_tracet &);
226+
227+
void show_goto_trace(
228+
std::ostream &out,
229+
const namespacet &,
230+
const goto_tracet &,
231+
const trace_optionst &);
232+
233+
void trace_value(
234+
std::ostream &out,
235+
const namespacet &,
236+
const ssa_exprt &lhs_object,
237+
const exprt &full_lhs,
238+
const exprt &value);
239+
240+
241+
#define OPT_GOTO_TRACE "(trace-json-extended)" \
242+
"(trace-hex)"
230243

231244
#define HELP_GOTO_TRACE \
232-
" --trace-json-extended add rawLhs property to trace\n"
245+
" --trace-json-extended add rawLhs property to trace\n" \
246+
" --trace-hex represent plain trace values in hex\n"
233247

234248
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options) \
235249
if(cmdline.isset("trace-json-extended")) \
236-
options.set_option("trace-json-extended", true);
250+
options.set_option("trace-json-extended", true); \
251+
if(cmdline.isset("trace-hex")) \
252+
options.set_option("trace-hex", true);
237253

238254

239255
#endif // CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H

0 commit comments

Comments
 (0)