Skip to content

Commit 069eeb1

Browse files
author
thk123
committed
Use format rather than from_expr for output
1 parent 74922b2 commit 069eeb1

File tree

6 files changed

+117
-39
lines changed

6 files changed

+117
-39
lines changed

‎src/cbmc/bmc.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,7 @@ class bmct:public safety_checkert
7878
options(_options),
7979
outer_symbol_table(outer_symbol_table),
8080
ns(outer_symbol_table, symex_symbol_table),
81-
equation(ns),
81+
equation(),
8282
branch_worklist(_branch_worklist),
8383
symex(_message_handler, outer_symbol_table, equation, branch_worklist),
8484
prop_conv(_prop_conv),

‎src/goto-instrument/accelerate/scratch_program.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ class scratch_programt:public goto_programt
4040
symbol_table(_symbol_table),
4141
symex_symbol_table(),
4242
ns(symbol_table, symex_symbol_table),
43-
equation(ns),
43+
equation(),
4444
branch_worklist(),
4545
symex(mh, symbol_table, equation, branch_worklist),
4646
satcheck(util_make_unique<satcheckt>()),

‎src/goto-symex/equation_conversion_exceptions.h

+6-25
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ Author: Diffblue Ltd.
1717
#include <util/namespace.h>
1818

1919
#include <langapi/language_util.h>
20+
#include <util/format.h>
2021

2122
#include "symex_target_equation.h"
2223

@@ -25,26 +26,17 @@ class equation_conversion_exceptiont : public std::runtime_error
2526
public:
2627
equation_conversion_exceptiont(
2728
const std::string &message,
28-
const symex_target_equationt::SSA_stept &step,
29-
const namespacet &ns)
29+
const symex_target_equationt::SSA_stept &step)
3030
: runtime_error(message), step(step)
3131
{
3232
std::ostringstream error_msg;
3333
error_msg << runtime_error::what();
34-
error_msg << "\nSource GOTO statement: "
35-
<< from_expr(ns, "java", step.source.pc->code);
34+
error_msg << "\nSource GOTO statement: " << format(step.source.pc->code);
3635
error_msg << "\nStep:\n";
37-
step.output(ns, error_msg);
36+
step.output(error_msg);
3837
error_message = error_msg.str();
3938
}
4039

41-
explicit equation_conversion_exceptiont(
42-
const std::string &message,
43-
const symex_target_equationt::SSA_stept &step)
44-
: equation_conversion_exceptiont(message, step, namespacet{symbol_tablet{}})
45-
{
46-
}
47-
4840
const char *what() const optional_noexcept override
4941
{
5042
return error_message.c_str();
@@ -58,19 +50,8 @@ class equation_conversion_exceptiont : public std::runtime_error
5850
class guard_conversion_exceptiont : public equation_conversion_exceptiont
5951
{
6052
public:
61-
guard_conversion_exceptiont(
62-
const symex_target_equationt::SSA_stept &step,
63-
const namespacet &ns)
64-
: equation_conversion_exceptiont(
65-
"Error converting guard for step",
66-
step,
67-
ns)
68-
{
69-
}
70-
71-
explicit guard_conversion_exceptiont(
72-
const symex_target_equationt::SSA_stept &step)
73-
: guard_conversion_exceptiont(step, namespacet{symbol_tablet{}})
53+
guard_conversion_exceptiont(const symex_target_equationt::SSA_stept &step)
54+
: equation_conversion_exceptiont("Error converting guard for step", step)
7455
{
7556
}
7657
};

‎src/goto-symex/symex_target_equation.cpp

+104-5
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
2020
#include <solvers/prop/literal_expr.h>
2121
#include <solvers/prop/prop.h>
2222
#include <solvers/prop/prop_conv.h>
23+
#include <util/format.h>
2324

2425
#include "equation_conversion_exceptions.h"
2526
#include "goto_symex_state.h"
@@ -423,7 +424,7 @@ void symex_target_equationt::convert_decls(
423424
{
424425
util_throw_with_nested(
425426
equation_conversion_exceptiont(
426-
"Error converting decls for step", step, ns));
427+
"Error converting decls for step", step));
427428
}
428429
}
429430
}
@@ -448,7 +449,7 @@ void symex_target_equationt::convert_guards(
448449
{
449450
util_throw_with_nested(
450451
equation_conversion_exceptiont(
451-
"Error converting guard for step", step, ns));
452+
"Error converting guard for step", step));
452453
}
453454
}
454455
}
@@ -475,7 +476,7 @@ void symex_target_equationt::convert_assumptions(
475476
{
476477
util_throw_with_nested(
477478
equation_conversion_exceptiont(
478-
"Error converting assumptions for step", step, ns));
479+
"Error converting assumptions for step", step));
479480
}
480481
}
481482
}
@@ -503,7 +504,7 @@ void symex_target_equationt::convert_goto_instructions(
503504
{
504505
util_throw_with_nested(
505506
equation_conversion_exceptiont(
506-
"Error converting goto instructions for step", step, ns));
507+
"Error converting goto instructions for step", step));
507508
}
508509
}
509510
}
@@ -582,7 +583,7 @@ void symex_target_equationt::convert_assertions(
582583
{
583584
util_throw_with_nested(
584585
equation_conversion_exceptiont(
585-
"Error converting assertions for step", step, ns));
586+
"Error converting assertions for step", step));
586587
}
587588

588589
// store disjunct
@@ -767,3 +768,101 @@ void symex_target_equationt::SSA_stept::output(
767768

768769
out << "Guard: " << from_expr(ns, source.pc->function, guard) << '\n';
769770
}
771+
772+
void symex_target_equationt::SSA_stept::output(std::ostream &out) const
773+
{
774+
if(source.is_set)
775+
{
776+
out << "Thread " << source.thread_nr;
777+
778+
if(source.pc->source_location.is_not_nil())
779+
out << " " << source.pc->source_location << '\n';
780+
else
781+
out << '\n';
782+
}
783+
784+
switch(type)
785+
{
786+
case goto_trace_stept::typet::ASSERT:
787+
out << "ASSERT " << format(cond_expr) << '\n'; break;
788+
case goto_trace_stept::typet::ASSUME:
789+
out << "ASSUME " << format(cond_expr) << '\n'; break;
790+
case goto_trace_stept::typet::LOCATION:
791+
out << "LOCATION" << '\n'; break;
792+
case goto_trace_stept::typet::INPUT:
793+
out << "INPUT" << '\n'; break;
794+
case goto_trace_stept::typet::OUTPUT:
795+
out << "OUTPUT" << '\n'; break;
796+
797+
case goto_trace_stept::typet::DECL:
798+
out << "DECL" << '\n';
799+
out << format(ssa_lhs) << '\n';
800+
break;
801+
802+
case goto_trace_stept::typet::ASSIGNMENT:
803+
out << "ASSIGNMENT (";
804+
switch(assignment_type)
805+
{
806+
case assignment_typet::HIDDEN:
807+
out << "HIDDEN";
808+
break;
809+
case assignment_typet::STATE:
810+
out << "STATE";
811+
break;
812+
case assignment_typet::VISIBLE_ACTUAL_PARAMETER:
813+
out << "VISIBLE_ACTUAL_PARAMETER";
814+
break;
815+
case assignment_typet::HIDDEN_ACTUAL_PARAMETER:
816+
out << "HIDDEN_ACTUAL_PARAMETER";
817+
break;
818+
case assignment_typet::PHI:
819+
out << "PHI";
820+
break;
821+
case assignment_typet::GUARD:
822+
out << "GUARD";
823+
break;
824+
default:
825+
{
826+
}
827+
}
828+
829+
out << ")\n";
830+
break;
831+
832+
case goto_trace_stept::typet::DEAD:
833+
out << "DEAD\n"; break;
834+
case goto_trace_stept::typet::FUNCTION_CALL:
835+
out << "FUNCTION_CALL\n"; break;
836+
case goto_trace_stept::typet::FUNCTION_RETURN:
837+
out << "FUNCTION_RETURN\n"; break;
838+
case goto_trace_stept::typet::CONSTRAINT:
839+
out << "CONSTRAINT\n"; break;
840+
case goto_trace_stept::typet::SHARED_READ:
841+
out << "SHARED READ\n"; break;
842+
case goto_trace_stept::typet::SHARED_WRITE:
843+
out << "SHARED WRITE\n"; break;
844+
case goto_trace_stept::typet::ATOMIC_BEGIN:
845+
out << "ATOMIC_BEGIN\n"; break;
846+
case goto_trace_stept::typet::ATOMIC_END:
847+
out << "AUTOMIC_END\n"; break;
848+
case goto_trace_stept::typet::SPAWN:
849+
out << "SPAWN\n"; break;
850+
case goto_trace_stept::typet::MEMORY_BARRIER:
851+
out << "MEMORY_BARRIER\n"; break;
852+
case goto_trace_stept::typet::GOTO:
853+
out << "IF " << format(cond_expr) << " GOTO\n"; break;
854+
855+
default: UNREACHABLE;
856+
}
857+
858+
if(is_assert() || is_assume() || is_assignment() || is_constraint())
859+
out << format(cond_expr) << '\n';
860+
861+
if(is_assert() || is_constraint())
862+
out << comment << '\n';
863+
864+
if(is_shared_read() || is_shared_write())
865+
out << format(ssa_lhs) << '\n';
866+
867+
out << "Guard: " << format(guard) << '\n';
868+
}

‎src/goto-symex/symex_target_equation.h

+3-7
Original file line numberDiff line numberDiff line change
@@ -32,10 +32,6 @@ class prop_convt;
3232
class symex_target_equationt:public symex_targett
3333
{
3434
public:
35-
explicit symex_target_equationt(const namespacet &ns) : ns(ns)
36-
{
37-
}
38-
3935
virtual ~symex_target_equationt() = default;
4036

4137
// read event
@@ -260,9 +256,12 @@ class symex_target_equationt:public symex_targett
260256
{
261257
}
262258

259+
DEPRECATED("Use output without ns param")
263260
void output(
264261
const namespacet &ns,
265262
std::ostream &out) const;
263+
264+
void output(std::ostream &out) const;
266265
};
267266

268267
std::size_t count_assertions() const
@@ -323,9 +322,6 @@ class symex_target_equationt:public symex_targett
323322
// for enforcing sharing in the expressions stored
324323
merge_irept merge_irep;
325324
void merge_ireps(SSA_stept &SSA_step);
326-
327-
private:
328-
const namespacet &ns;
329325
};
330326

331327
inline bool operator<(

‎src/util/format.h

+2
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,8 @@ Author: Daniel Kroening, [email protected]
1010
#define CPROVER_UTIL_FORMAT_H
1111

1212
#include <iosfwd>
13+
#include "format_expr.h"
14+
#include "format_type.h"
1315

1416
//! The below enables convenient syntax for feeding
1517
//! objects into streams, via stream << format(o)

0 commit comments

Comments
 (0)