Merge pull request #974 from tautschnig/fix-assert-encoding

Do not generate redundant if statements in assert expansions

Author: tautschnig

regression/cbmc/simple_assert/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+int main(int argc, char *argv[])
+{
+  int x = 5;
+  assert(x == 5);
+
+  return 0;
+}

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.

regression/goto-instrument/assert1/main.c

@@ -0,0 +1,7 @@
+#include <assert.h>
+
+int main(int argc, char *argv[])
+{
+  assert(0);
+  return 0;
+}

regression/goto-instrument/assert1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--dump-c
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+^[[:space:]]*IF

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);
       }
 

src/goto-programs/goto_convert.cpp

@@ -26,13 +26,12 @@ 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)
 {
   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;
@@ -1723,6 +1722,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 +1740,28 @@ 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;
+  }
+
+  // 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.

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<irep_idt> 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()<old_size);

src/goto-programs/remove_skip.h

@@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 class goto_modelt;
 
+bool is_skip(const goto_programt &, goto_programt::const_targett);
 void remove_skip(goto_programt &);
 void remove_skip(goto_functionst &);
 void remove_skip(goto_modelt &);