Skip to content

Commit 16b6c20

Browse files
author
Thomas Kiley
authored
Merge pull request #2046 from thk123/gs_tg2922
[TG-2922] Improve logging for byte flatten exceptions
2 parents 04cb909 + 9874a6b commit 16b6c20

15 files changed

+612
-26
lines changed

‎regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.class

399 Bytes
Binary file not shown.

‎regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.java

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
public class TestClass {
2+
public static void f(int y) {
3+
float[][] a1 = new float[y][3];
4+
int j = 0;
5+
a1[j][0] = 34.5f;
6+
}
7+
}

‎regression/cbmc-java/dynamic-multi-dimensional-array/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
TestClass.class
3+
--function TestClass.f --cover location --unwind 2
4+
Source GOTO statement: .*
5+
(^ exception: Can't convert byte_extraction|Nested exception printing not supported on Windows)
6+
^EXIT=6$
7+
--
8+
--
9+
The exception thrown in this test is the symptom of a bug; the purpose of this
10+
test is the validate the output of that exception

‎src/goto-symex/equation_conversion_exceptions.h

+47
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
/*******************************************************************\
2+
3+
Module: Symbolic Execution
4+
5+
Author: Diffblue Ltd.
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Exceptions that can be raised during the equation conversion phase
11+
12+
#ifndef CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H
13+
#define CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H
14+
15+
#include <ostream>
16+
17+
#include <util/format_expr.h>
18+
19+
#include "symex_target_equation.h"
20+
21+
class equation_conversion_exceptiont : public std::runtime_error
22+
{
23+
public:
24+
equation_conversion_exceptiont(
25+
const std::string &message,
26+
const symex_target_equationt::SSA_stept &step)
27+
: runtime_error(message), step(step)
28+
{
29+
std::ostringstream error_msg;
30+
error_msg << runtime_error::what();
31+
error_msg << "\nSource GOTO statement: " << format(step.source.pc->code);
32+
error_msg << "\nStep:\n";
33+
step.output(error_msg);
34+
error_message = error_msg.str();
35+
}
36+
37+
const char *what() const optional_noexcept override
38+
{
39+
return error_message.c_str();
40+
}
41+
42+
private:
43+
symex_target_equationt::SSA_stept step;
44+
std::string error_message;
45+
};
46+
47+
#endif // CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H

‎src/goto-symex/symex_target_equation.cpp

+197-15
Original file line numberDiff line numberDiff line change
@@ -11,13 +11,20 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "symex_target_equation.h"
1313

14+
#include <util/format_expr.h>
1415
#include <util/std_expr.h>
16+
#include <util/throw_with_nested.h>
17+
#include <util/unwrap_nested_exception.h>
1518

19+
// Can be removed once deprecated SSA_stept::output is removed
1620
#include <langapi/language_util.h>
17-
#include <solvers/prop/prop_conv.h>
18-
#include <solvers/prop/prop.h>
21+
22+
#include <solvers/flattening/bv_conversion_exceptions.h>
1923
#include <solvers/prop/literal_expr.h>
24+
#include <solvers/prop/prop.h>
25+
#include <solvers/prop/prop_conv.h>
2026

27+
#include "equation_conversion_exceptions.h"
2128
#include "goto_symex_state.h"
2229

2330
/// read from a shared variable
@@ -368,14 +375,23 @@ void symex_target_equationt::constraint(
368375
void symex_target_equationt::convert(
369376
prop_convt &prop_conv)
370377
{
371-
convert_guards(prop_conv);
372-
convert_assignments(prop_conv);
373-
convert_decls(prop_conv);
374-
convert_assumptions(prop_conv);
375-
convert_assertions(prop_conv);
376-
convert_goto_instructions(prop_conv);
377-
convert_io(prop_conv);
378-
convert_constraints(prop_conv);
378+
try
379+
{
380+
convert_guards(prop_conv);
381+
convert_assignments(prop_conv);
382+
convert_decls(prop_conv);
383+
convert_assumptions(prop_conv);
384+
convert_assertions(prop_conv);
385+
convert_goto_instructions(prop_conv);
386+
convert_io(prop_conv);
387+
convert_constraints(prop_conv);
388+
}
389+
catch(const equation_conversion_exceptiont &conversion_exception)
390+
{
391+
// unwrap the except and throw like normal
392+
const std::string full_error = unwrap_exception(conversion_exception);
393+
throw full_error;
394+
}
379395
}
380396

381397
/// converts assignments
@@ -402,7 +418,16 @@ void symex_target_equationt::convert_decls(
402418
{
403419
// The result is not used, these have no impact on
404420
// the satisfiability of the formula.
405-
prop_conv.convert(step.cond_expr);
421+
try
422+
{
423+
prop_conv.convert(step.cond_expr);
424+
}
425+
catch(const bitvector_conversion_exceptiont &conversion_exception)
426+
{
427+
util_throw_with_nested(
428+
equation_conversion_exceptiont(
429+
"Error converting decls for step", step));
430+
}
406431
}
407432
}
408433
}
@@ -417,7 +442,18 @@ void symex_target_equationt::convert_guards(
417442
if(step.ignore)
418443
step.guard_literal=const_literal(false);
419444
else
420-
step.guard_literal=prop_conv.convert(step.guard);
445+
{
446+
try
447+
{
448+
step.guard_literal = prop_conv.convert(step.guard);
449+
}
450+
catch(const bitvector_conversion_exceptiont &conversion_exception)
451+
{
452+
util_throw_with_nested(
453+
equation_conversion_exceptiont(
454+
"Error converting guard for step", step));
455+
}
456+
}
421457
}
422458
}
423459

@@ -433,7 +469,18 @@ void symex_target_equationt::convert_assumptions(
433469
if(step.ignore)
434470
step.cond_literal=const_literal(true);
435471
else
436-
step.cond_literal=prop_conv.convert(step.cond_expr);
472+
{
473+
try
474+
{
475+
step.cond_literal = prop_conv.convert(step.cond_expr);
476+
}
477+
catch(const bitvector_conversion_exceptiont &conversion_exception)
478+
{
479+
util_throw_with_nested(
480+
equation_conversion_exceptiont(
481+
"Error converting assumptions for step", step));
482+
}
483+
}
437484
}
438485
}
439486
}
@@ -450,7 +497,18 @@ void symex_target_equationt::convert_goto_instructions(
450497
if(step.ignore)
451498
step.cond_literal=const_literal(true);
452499
else
453-
step.cond_literal=prop_conv.convert(step.cond_expr);
500+
{
501+
try
502+
{
503+
step.cond_literal = prop_conv.convert(step.cond_expr);
504+
}
505+
catch(const bitvector_conversion_exceptiont &conversion_exception)
506+
{
507+
util_throw_with_nested(
508+
equation_conversion_exceptiont(
509+
"Error converting goto instructions for step", step));
510+
}
511+
}
454512
}
455513
}
456514
}
@@ -519,7 +577,16 @@ void symex_target_equationt::convert_assertions(
519577
step.cond_expr);
520578

521579
// do the conversion
522-
step.cond_literal=prop_conv.convert(implication);
580+
try
581+
{
582+
step.cond_literal = prop_conv.convert(implication);
583+
}
584+
catch(const bitvector_conversion_exceptiont &conversion_exception)
585+
{
586+
util_throw_with_nested(
587+
equation_conversion_exceptiont(
588+
"Error converting assertions for step", step));
589+
}
523590

524591
// store disjunct
525592
disjuncts.push_back(literal_exprt(!step.cond_literal));
@@ -703,3 +770,118 @@ void symex_target_equationt::SSA_stept::output(
703770

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

‎src/goto-symex/symex_target_equation.h

+3-1
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,6 @@ class prop_convt;
3232
class symex_target_equationt:public symex_targett
3333
{
3434
public:
35-
symex_target_equationt() = default;
3635
virtual ~symex_target_equationt() = default;
3736

3837
// read event
@@ -257,9 +256,12 @@ class symex_target_equationt:public symex_targett
257256
{
258257
}
259258

259+
DEPRECATED("Use output without ns param")
260260
void output(
261261
const namespacet &ns,
262262
std::ostream &out) const;
263+
264+
void output(std::ostream &out) const;
263265
};
264266

265267
std::size_t count_assertions() const

‎src/solvers/flattening/boolbv.cpp

+8
Original file line numberDiff line numberDiff line change
@@ -152,6 +152,14 @@ bvt boolbvt::conversion_failed(const exprt &expr)
152152
return prop.new_variables(width);
153153
}
154154

155+
/// Converts an expression into its gate-level representation and returns a
156+
/// vector of literals corresponding to the outputs of the Boolean circuit.
157+
/// \param expr: Expression to convert
158+
/// \return A vector of literals corresponding to the outputs of the Boolean
159+
/// circuit
160+
/// \throws bitvector_conversion_exceptiont raised if converting byte_extraction
161+
/// goes wrong.
162+
/// TODO: extend for other types of conversion exception (diffblue/cbmc#2103).
155163
bvt boolbvt::convert_bitvector(const exprt &expr)
156164
{
157165
if(expr.type().id()==ID_bool)

0 commit comments

Comments
 (0)