From 4fb06030089121d9ff7e113177716798b16972b1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 26 May 2017 16:11:21 +0100 Subject: [PATCH 1/4] Make is_skip publicly available and use constant argument --- src/goto-programs/remove_skip.cpp | 16 ++++++++++------ src/goto-programs/remove_skip.h | 1 + 2 files changed, 11 insertions(+), 6 deletions(-) diff --git a/src/goto-programs/remove_skip.cpp b/src/goto-programs/remove_skip.cpp index 4ce2a74fb04..a41bb59aa26 100644 --- a/src/goto-programs/remove_skip.cpp +++ b/src/goto-programs/remove_skip.cpp @@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "remove_skip.h" #include "goto_model.h" -static bool is_skip(goto_programt::instructionst::iterator it) +bool is_skip(const goto_programt &body, goto_programt::const_targett it) { // we won't remove labelled statements // (think about error labels or the like) @@ -28,9 +28,12 @@ static bool is_skip(goto_programt::instructionst::iterator it) if(it->guard.is_false()) return true; - goto_programt::instructionst::iterator next_it=it; + goto_programt::const_targett next_it = it; next_it++; + if(next_it == body.instructions.end()) + return false; + // A branch to the next instruction is a skip // We also require the guard to be 'true' return it->guard.is_true() && @@ -92,7 +95,7 @@ void remove_skip(goto_programt &goto_program) // for collecting labels std::list labels; - while(is_skip(it)) + while(is_skip(goto_program, it)) { // don't remove the last skip statement, // it could be a target @@ -144,9 +147,10 @@ void remove_skip(goto_programt &goto_program) // remove the last skip statement unless it's a target goto_program.compute_incoming_edges(); - if(!goto_program.instructions.empty() && - is_skip(--goto_program.instructions.end()) && - !goto_program.instructions.back().is_target()) + if( + !goto_program.instructions.empty() && + is_skip(goto_program, --goto_program.instructions.end()) && + !goto_program.instructions.back().is_target()) goto_program.instructions.pop_back(); } while(goto_program.instructions.size() Date: Fri, 26 May 2017 16:20:48 +0100 Subject: [PATCH 2/4] Do not generate redundant if statements in assert expansions Fixes: #755 --- regression/goto-instrument/assert1/main.c | 7 +++++++ regression/goto-instrument/assert1/test.desc | 8 ++++++++ src/goto-programs/goto_convert.cpp | 11 +++++++++++ 3 files changed, 26 insertions(+) create mode 100644 regression/goto-instrument/assert1/main.c create mode 100644 regression/goto-instrument/assert1/test.desc diff --git a/regression/goto-instrument/assert1/main.c b/regression/goto-instrument/assert1/main.c new file mode 100644 index 00000000000..e9cf26ef226 --- /dev/null +++ b/regression/goto-instrument/assert1/main.c @@ -0,0 +1,7 @@ +#include + +int main(int argc, char *argv[]) +{ + assert(0); + return 0; +} diff --git a/regression/goto-instrument/assert1/test.desc b/regression/goto-instrument/assert1/test.desc new file mode 100644 index 00000000000..c2d2fa95ee8 --- /dev/null +++ b/regression/goto-instrument/assert1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--dump-c +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +^[[:space:]]*IF diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 7f8095c2a05..80e9ec1432e 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -26,6 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_convert_class.h" #include "destructor.h" +#include "remove_skip.h" static bool is_empty(const goto_programt &goto_program) { @@ -1723,6 +1724,11 @@ void goto_convertt::generate_ifthenelse( true_case.instructions.back().guard=boolean_negate(guard); dest.destructive_append(true_case); true_case.instructions.clear(); + if( + is_empty(false_case) || + (is_size_one(false_case) && + is_skip(false_case, false_case.instructions.begin()))) + return; } // similarly, do guarded assertions directly @@ -1736,6 +1742,11 @@ void goto_convertt::generate_ifthenelse( false_case.instructions.back().guard=guard; dest.destructive_append(false_case); false_case.instructions.clear(); + if( + is_empty(true_case) || + (is_size_one(true_case) && + is_skip(true_case, true_case.instructions.begin()))) + return; } // Flip around if no 'true' case code. From d44bfd3a1545b5fb2ae2a411871b8197fc3eae08 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 26 May 2017 18:04:44 +0100 Subject: [PATCH 3/4] Also simplify assert structure found on alpine linux --- src/goto-programs/goto_clean_expr.cpp | 10 ++++++++-- src/goto-programs/goto_convert.cpp | 21 ++++++++++++++++++--- 2 files changed, 26 insertions(+), 5 deletions(-) diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp index ad5fea6ac5f..8c82a34a582 100644 --- a/src/goto-programs/goto_clean_expr.cpp +++ b/src/goto-programs/goto_clean_expr.cpp @@ -260,13 +260,19 @@ void goto_convertt::clean_expr( // preserve the expressions for possible later checks if(if_expr.true_case().is_not_nil()) { - code_expressiont code_expression(if_expr.true_case()); + // add a (void) type cast so that is_skip catches it in case the + // expression is just a constant + code_expressiont code_expression( + typecast_exprt(if_expr.true_case(), empty_typet())); convert(code_expression, tmp_true); } if(if_expr.false_case().is_not_nil()) { - code_expressiont code_expression(if_expr.false_case()); + // add a (void) type cast so that is_skip catches it in case the + // expression is just a constant + code_expressiont code_expression( + typecast_exprt(if_expr.false_case(), empty_typet())); convert(code_expression, tmp_false); } diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 80e9ec1432e..2bca47c7723 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -31,9 +31,7 @@ Author: Daniel Kroening, kroening@kroening.com static bool is_empty(const goto_programt &goto_program) { forall_goto_program_instructions(it, goto_program) - if(!it->is_skip() || - !it->labels.empty() || - !it->code.is_nil()) + if(!is_skip(goto_program, it)) return false; return true; @@ -1749,6 +1747,23 @@ void goto_convertt::generate_ifthenelse( return; } + // a special case for C libraries that use + // (void)((cond) || (assert(0),0)) + if( + is_empty(false_case) && true_case.instructions.size() == 2 && + true_case.instructions.front().is_assert() && + true_case.instructions.front().guard.is_false() && + true_case.instructions.front().labels.empty() && + true_case.instructions.back().labels.empty()) + { + true_case.instructions.front().guard = boolean_negate(guard); + true_case.instructions.erase(--true_case.instructions.end()); + dest.destructive_append(true_case); + true_case.instructions.clear(); + + return; + } + // Flip around if no 'true' case code. if(is_empty(true_case)) return generate_ifthenelse( From 4122a28b8958f6c528707bcf10a2098740b76b56 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 29 Mar 2017 16:18:08 +0100 Subject: [PATCH 4/4] Test to demonstrate assert bug on alpine The user added assert in this test does not get coverage under alpine linux. --- regression/cbmc/simple_assert/main.c | 9 +++++++++ regression/cbmc/simple_assert/test.desc | 13 +++++++++++++ 2 files changed, 22 insertions(+) create mode 100644 regression/cbmc/simple_assert/main.c create mode 100644 regression/cbmc/simple_assert/test.desc diff --git a/regression/cbmc/simple_assert/main.c b/regression/cbmc/simple_assert/main.c new file mode 100644 index 00000000000..14c6fc0f682 --- /dev/null +++ b/regression/cbmc/simple_assert/main.c @@ -0,0 +1,9 @@ +#include + +int main(int argc, char *argv[]) +{ + int x = 5; + assert(x == 5); + + return 0; +} diff --git a/regression/cbmc/simple_assert/test.desc b/regression/cbmc/simple_assert/test.desc new file mode 100644 index 00000000000..57c877afe23 --- /dev/null +++ b/regression/cbmc/simple_assert/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--cover location +^EXIT=0$ +^SIGNAL=0$ +^\[main\.coverage\.1\] .* function main block 1: SATISFIED$ +(1 of 1|3 of 3) covered \(100\.0%\)$ +-- +^warning: ignoring +^CONVERSION ERROR$ +^\[main\.coverage\..\] .* function main block .: FAILED$ +-- +On Windows/Visual Studio, "assert" does not introduce any branching.