Skip to content

Commit 76318ce

Browse files
NathanJPhillipsNathanJPhillips
committed
Protect extended trace behind a command line option
1 parent 69b0ff1 commit 76318ce

File tree

12 files changed

+94
-34
lines changed

12 files changed

+94
-34
lines changed

‎src/cbmc/all_properties.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -219,7 +219,7 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
219219
if(g.second.status==goalt::statust::FAILURE)
220220
{
221221
jsont &json_trace=result["trace"];
222-
convert(bmc.ns, g.second.goto_trace, json_trace);
222+
convert(bmc.ns, g.second.goto_trace, json_trace, bmc.trace_options());
223223
}
224224
}
225225

‎src/cbmc/bmc.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -91,7 +91,7 @@ void bmct::error_trace()
9191
json_stringt(id2string(step.pc->source_location.get_comment()));
9292
json_result["status"]=json_stringt("failed");
9393
jsont &json_trace=json_result["trace"];
94-
convert(ns, goto_trace, json_trace);
94+
convert(ns, goto_trace, json_trace, trace_options());
9595
status() << json_result;
9696
}
9797
break;

‎src/cbmc/bmc.h‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,8 @@ Author: Daniel Kroening, [email protected]
2525
#include <solvers/smt1/smt1_dec.h>
2626
#include <solvers/smt2/smt2_dec.h>
2727

28+
#include <goto-programs/goto_trace.h>
29+
2830
#include <goto-symex/symex_target_equation.h>
2931
#include <goto-programs/safety_checker.h>
3032
#include <goto-symex/memory_model.h>
@@ -98,6 +100,11 @@ class bmct:public safety_checkert
98100
virtual void show_vcc_plain(std::ostream &out);
99101
virtual void show_vcc_json(std::ostream &out);
100102

103+
trace_optionst trace_options()
104+
{
105+
return trace_optionst(options);
106+
}
107+
101108
virtual resultt all_properties(
102109
const goto_functionst &goto_functions,
103110
prop_convt &solver);

‎src/cbmc/bmc_cover.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -370,7 +370,7 @@ bool bmc_covert::operator()()
370370
if(bmc.options.get_bool_option("trace"))
371371
{
372372
jsont &json_trace=result["trace"];
373-
convert(bmc.ns, test.goto_trace, json_trace);
373+
convert(bmc.ns, test.goto_trace, json_trace, bmc.trace_options());
374374
}
375375
else
376376
{

‎src/cbmc/cbmc_parse_options.cpp‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -408,6 +408,8 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
408408
options.set_option(
409409
"symex-coverage-report",
410410
cmdline.get_value("symex-coverage-report"));
411+
412+
PARSE_OPTIONS_GOTO_TRACE(cmdline, options);
411413
}
412414

413415
/// invoke main modules
@@ -1020,6 +1022,7 @@ void cbmc_parse_optionst::help()
10201022
" --xml-ui use XML-formatted output\n"
10211023
" --xml-interface bi-directional XML interface\n"
10221024
" --json-ui use JSON-formatted output\n"
1025+
HELP_GOTO_TRACE
10231026
" --verbosity # verbosity level\n"
10241027
"\n";
10251028
}

‎src/cbmc/cbmc_parse_options.h‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,8 @@ Author: Daniel Kroening, [email protected]
1818

1919
#include <analyses/goto_check.h>
2020

21+
#include <goto-programs/goto_trace.h>
22+
2123
#include "xml_interface.h"
2224

2325
class bmct;
@@ -65,6 +67,7 @@ class optionst;
6567
"(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
6668
"(graphml-witness):" \
6769
"(localize-faults)(localize-faults-method):" \
70+
OPT_GOTO_TRACE \
6871
"(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
6972

7073
class cbmc_parse_optionst:

‎src/goto-programs/goto_trace.cpp‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -395,3 +395,6 @@ void show_goto_trace(
395395
}
396396
}
397397
}
398+
399+
400+
const trace_optionst trace_optionst::default_options = trace_optionst();

‎src/goto-programs/goto_trace.h‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ Date: July 2005
2525
#include <vector>
2626

2727
#include <util/namespace.h>
28+
#include <util/options.h>
2829
#include <util/ssa_expr.h>
2930

3031
#include <goto-programs/goto_program.h>
@@ -206,4 +207,33 @@ void trace_value(
206207
const exprt &full_lhs,
207208
const exprt &value);
208209

210+
211+
struct trace_optionst
212+
{
213+
bool json_full_lhs;
214+
215+
static const trace_optionst default_options;
216+
217+
explicit trace_optionst(const optionst &options)
218+
{
219+
json_full_lhs = options.get_bool_option("trace-json-extended");
220+
};
221+
222+
private:
223+
trace_optionst()
224+
{
225+
json_full_lhs = false;
226+
};
227+
};
228+
229+
#define OPT_GOTO_TRACE "(trace-json-extended)"
230+
231+
#define HELP_GOTO_TRACE \
232+
" --trace-json-extended add rawLhs property to trace\n"
233+
234+
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options) \
235+
if(cmdline.isset("trace-json-extended")) \
236+
options.set_option("trace-json-extended", true);
237+
238+
209239
#endif // CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H

‎src/goto-programs/json_goto_trace.cpp‎

Lines changed: 36 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,8 @@ Author: Daniel Kroening
3030
void convert(
3131
const namespacet &ns,
3232
const goto_tracet &goto_trace,
33-
jsont &dest)
33+
jsont &dest,
34+
trace_optionst trace_options)
3435
{
3536
json_arrayt &dest_array=dest.make_array();
3637

@@ -96,36 +97,39 @@ void convert(
9697
"full_lhs in assignment must not be nil");
9798
exprt simplified=simplify_expr(step.full_lhs, ns);
9899

99-
class comment_base_name_visitort : public expr_visitort
100+
if(trace_options.json_full_lhs)
100101
{
101-
private:
102-
const namespacet &ns;
103-
104-
public:
105-
explicit comment_base_name_visitort(const namespacet &ns) : ns(ns)
102+
class comment_base_name_visitort : public expr_visitort
106103
{
107-
}
104+
private:
105+
const namespacet &ns;
108106

109-
void operator()(exprt &expr) override
110-
{
111-
if(expr.id() == ID_symbol)
107+
public:
108+
explicit comment_base_name_visitort(const namespacet &ns) : ns(ns)
109+
{
110+
}
111+
112+
void operator()(exprt &expr) override
112113
{
113-
const symbolt &symbol = ns.lookup(expr.get(ID_identifier));
114-
// Don't break sharing unless need to write to it
115-
const irept::named_subt &comments =
116-
static_cast<const exprt &>(expr).get_comments();
117-
if(comments.count(ID_C_base_name) != 0)
118-
INVARIANT(
119-
comments.at(ID_C_base_name).id() == symbol.base_name,
120-
"base_name comment does not match symbol's base_name");
121-
else
122-
expr.get_comments().emplace(
123-
ID_C_base_name, irept(symbol.base_name));
114+
if(expr.id() == ID_symbol)
115+
{
116+
const symbolt &symbol = ns.lookup(expr.get(ID_identifier));
117+
// Don't break sharing unless need to write to it
118+
const irept::named_subt &comments =
119+
static_cast<const exprt &>(expr).get_comments();
120+
if(comments.count(ID_C_base_name) != 0)
121+
INVARIANT(
122+
comments.at(ID_C_base_name).id() == symbol.base_name,
123+
"base_name comment does not match symbol's base_name");
124+
else
125+
expr.get_comments().emplace(
126+
ID_C_base_name, irept(symbol.base_name));
127+
}
124128
}
125-
}
126-
};
127-
comment_base_name_visitort comment_base_name_visitor(ns);
128-
simplified.visit(comment_base_name_visitor);
129+
};
130+
comment_base_name_visitort comment_base_name_visitor(ns);
131+
simplified.visit(comment_base_name_visitor);
132+
}
129133

130134
full_lhs_string=from_expr(ns, identifier, simplified);
131135

@@ -154,9 +158,12 @@ void convert(
154158

155159
json_assignment["value"]=full_lhs_value;
156160
json_assignment["lhs"]=json_stringt(full_lhs_string);
157-
// Not language specific, still mangled, fully-qualified name of lhs:
158-
json_assignment["rawLhs"] =
159-
json_irept(true).convert_from_irep(simplified);
161+
if(trace_options.json_full_lhs)
162+
{
163+
// Not language specific, still mangled, fully-qualified name of lhs
164+
json_assignment["rawLhs"] =
165+
json_irept(true).convert_from_irep(simplified);
166+
}
160167
json_assignment["hidden"]=jsont::json_boolean(step.hidden);
161168
json_assignment["internal"]=jsont::json_boolean(step.internal);
162169
json_assignment["thread"]=json_numbert(std::to_string(step.thread_nr));

‎src/goto-programs/json_goto_trace.h‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ Date: November 2005
2121
void convert(
2222
const namespacet &,
2323
const goto_tracet &,
24-
jsont &);
24+
jsont &,
25+
trace_optionst trace_options = trace_optionst::default_options);
2526

2627
#endif // CPROVER_GOTO_PROGRAMS_JSON_GOTO_TRACE_H

0 commit comments

Comments
 (0)