Properly report branch coverage

Author: tautschnig

src/cbmc/symex_bmc.cpp

@@ -63,11 +63,52 @@ void symex_bmct::symex_step(
     last_source_location=source_location;
   }
 
-  if(record_coverage &&
-     !state.guard.is_false())
-    symex_coverage.covered(state.source.pc);
+  const goto_programt::const_targett cur_pc=state.source.pc;
 
   goto_symext::symex_step(goto_functions, state);
+
+  if(record_coverage &&
+     // is the instruction being executed
+     !state.guard.is_false() &&
+     // avoid an invalid iterator in state.source.pc
+     (!cur_pc->is_end_function() ||
+      cur_pc->function!=ID__start) &&
+     // ignore transition to next instruction when goto points elsewhere
+     (!cur_pc->is_goto() ||
+      cur_pc->get_target()==state.source.pc ||
+      !cur_pc->guard.is_true()))
+    symex_coverage.covered(cur_pc, state.source.pc);
+}
+
+/*******************************************************************\
+
+Function: symex_bmct::merge_goto
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void symex_bmct::merge_goto(
+  const statet::goto_statet &goto_state,
+  statet &state)
+{
+  const goto_programt::const_targett prev_pc=goto_state.source.pc;
+  const guardt prev_guard=goto_state.guard;
+
+  goto_symext::merge_goto(goto_state, state);
+
+  assert(prev_pc->is_goto());
+  if(record_coverage &&
+     // could the branch possibly be taken?
+     !prev_guard.is_false() &&
+     !state.guard.is_false() &&
+     // branches only, no single-successor goto
+     !prev_pc->guard.is_true())
+    symex_coverage.covered(prev_pc, state.source.pc);
 }
 
 /*******************************************************************\

src/cbmc/symex_bmc.h

@@ -83,6 +83,10 @@ class symex_bmct:
     const goto_functionst &goto_functions,
     statet &state);
 
+  virtual void merge_goto(
+    const statet::goto_statet &goto_state,
+    statet &state);
+
   // for loop unwinding
   virtual bool get_unwind(
     const symex_targett::sourcet &source,

src/cbmc/symex_coverage.cpp

@@ -58,26 +58,37 @@ class goto_program_coverage_recordt:public coverage_recordt
 protected:
   irep_idt file_name;
 
-  struct line_coverage_recordt
+  struct coverage_conditiont
   {
-    line_coverage_recordt():
-      hits(0), is_branch(false), branch_covered(false)
+    coverage_conditiont():
+      false_taken(false), true_taken(false)
+    {
+    }
+
+    bool false_taken;
+    bool true_taken;
+  };
+
+  struct coverage_linet
+  {
+    coverage_linet():
+      hits(0)
     {
     }
 
     unsigned hits;
-    bool is_branch;
-    bool branch_covered;
+    std::map<goto_programt::const_targett, coverage_conditiont>
+      conditions;
   };
 
-  typedef std::map<unsigned, line_coverage_recordt>
-    line_coverage_mapt;
+  typedef std::map<unsigned, coverage_linet>
+    coverage_lines_mapt;
 
-  void compute_line_coverage(
+  void compute_coverage_lines(
     const goto_programt &goto_program,
     const irep_idt &file_name,
     const symex_coveraget::coveraget &coverage,
-    line_coverage_mapt &dest);
+    coverage_lines_mapt &dest);
 };
 
 /*******************************************************************\
@@ -92,17 +103,26 @@ Function: rate
 
 \*******************************************************************/
 
-static std::string rate(std::size_t covered, std::size_t total)
+static std::string rate(
+  std::size_t covered,
+  std::size_t total,
+  bool per_cent=false)
 {
+  std::ostringstream oss;
+
 #if 1
-  if(total==0)
-    return "1.0";
+  float fraction;
 
-  std::ostringstream oss;
+  if(total==0)
+    fraction=1.0;
+  else
+    fraction=static_cast<float>(covered)/static_cast<float>(total);
 
-  oss << static_cast<float>(covered)/static_cast<float>(total);
+  if(per_cent)
+    oss << fraction*100.0 << '%';
+  else
+    oss << fraction;
 #else
-  std::ostringstream oss;
   oss << covered << " of " << total;
 #endif
 
@@ -138,12 +158,12 @@ goto_program_coverage_recordt::goto_program_coverage_recordt(
   assert(!file_name.empty());
 
   // compute the maximum coverage of individual source-code lines
-  line_coverage_mapt line_coverage_map;
-  compute_line_coverage(
+  coverage_lines_mapt coverage_lines_map;
+  compute_coverage_lines(
     gf_it->second.body,
     file_name,
     coverage,
-    line_coverage_map);
+    coverage_lines_map);
 
   // <method name="foo" signature="int(int)" line-rate="1.0" branch-rate="1.0">
   //   <lines>
@@ -173,28 +193,43 @@ goto_program_coverage_recordt::goto_program_coverage_recordt(
 
   xmlt &lines=xml.new_element("lines");
 
-  for(line_coverage_mapt::const_iterator
-      it=line_coverage_map.begin();
-      it!=line_coverage_map.end();
-      ++it)
+  for(const auto &cov_line : coverage_lines_map)
   {
     xmlt &line=lines.new_element("line");
 
-    line.set_attribute("number", std::to_string(it->first));
-    line.set_attribute("hits", std::to_string(it->second.hits));
-    if(!it->second.is_branch)
+    line.set_attribute("number", std::to_string(cov_line.first));
+    line.set_attribute("hits", std::to_string(cov_line.second.hits));
+    if(cov_line.second.conditions.empty())
       line.set_attribute("branch", "false");
     else
     {
-      // TODO: conditions
       line.set_attribute("branch", "true");
+
+      xmlt &conditions=line.new_element("conditions");
+
+      std::size_t number=0, total_taken=0;
+      for(const auto &c : cov_line.second.conditions)
+      {
+        // <condition number="0" type="jump" coverage="50%"/>
+        xmlt &condition=conditions.new_element("condition");
+        condition.set_attribute("number", std::to_string(number++));
+        condition.set_attribute("type", "jump");
+        unsigned taken=c.second.false_taken+c.second.true_taken;
+        total_taken+=taken;
+        condition.set_attribute("coverage", rate(taken, 2, true));
+      }
+
+      std::ostringstream oss;
+      oss << rate(total_taken, number*2, true)
+          << " (" << total_taken << '/' << number*2 << ')';
+      line.set_attribute("condition-coverage", oss.str());
     }
   }
 }
 
 /*******************************************************************\
 
-Function: goto_program_coverage_recordt::compute_line_coverage
+Function: goto_program_coverage_recordt::compute_coverage_lines
 
   Inputs:
 
@@ -204,58 +239,83 @@ Function: goto_program_coverage_recordt::compute_line_coverage
 
 \*******************************************************************/
 
-void goto_program_coverage_recordt::compute_line_coverage(
+void goto_program_coverage_recordt::compute_coverage_lines(
     const goto_programt &goto_program,
     const irep_idt &file_name,
     const symex_coveraget::coveraget &coverage,
-    line_coverage_mapt &dest)
+    coverage_lines_mapt &dest)
 {
   forall_goto_program_instructions(it, goto_program)
   {
     if(it->source_location.is_nil() ||
-       it->source_location.get_file()!=file_name)
+       it->source_location.get_file()!=file_name ||
+       it->is_dead() ||
+       it->is_end_function())
       continue;
 
     const bool is_branch=it->is_goto() && !it->guard.is_constant();
 
     unsigned l=
       safe_string2unsigned(id2string(it->source_location.get_line()));
-    std::pair<line_coverage_mapt::iterator, bool> entry=
-      dest.insert(std::make_pair(l, line_coverage_recordt()));
+    std::pair<coverage_lines_mapt::iterator, bool> entry=
+      dest.insert(std::make_pair(l, coverage_linet()));
 
     if(entry.second)
-    {
       ++lines_total;
-      if(is_branch)
-        ++branches_total;
-    }
 
     // mark as branch if any instruction in this source code line is
     // a branching instruction
-    if(is_branch &&
-       !entry.first->second.is_branch)
+    if(is_branch)
     {
-      ++branches_total;
-      entry.first->second.is_branch=true;
+      branches_total+=2;
+      if(!entry.first->second.conditions.insert(
+          {it, coverage_conditiont()}).second)
+        assert(false);
     }
 
     symex_coveraget::coveraget::const_iterator c_entry=
       coverage.find(it);
-    if(c_entry!=coverage.end() &&
-       c_entry->second.num_executions>0)
+    if(c_entry!=coverage.end())
     {
-      // maximum over all instructions in this source code line
-      if(c_entry->second.num_executions>entry.first->second.hits)
+      if(!(c_entry->second.size()==1 || is_branch))
       {
-        if(entry.first->second.hits==0)
-          ++lines_covered;
-        entry.first->second.hits=c_entry->second.num_executions;
+        std::cerr << it->location_number << std::endl;
+        for(const auto &cov : c_entry->second)
+          std::cerr << cov.second.succ->location_number << std::endl;
       }
+      assert(c_entry->second.size()==1 || is_branch);
 
-      if(is_branch && !entry.first->second.branch_covered)
+      for(const auto &cov : c_entry->second)
       {
-        ++branches_covered;
-        entry.first->second.branch_covered=true;
+        assert(cov.second.num_executions>0);
+
+        if(entry.first->second.hits==0)
+          ++lines_covered;
+
+        entry.first->second.hits+=cov.second.num_executions;
+
+        if(is_branch)
+        {
+          auto cond_entry=entry.first->second.conditions.find(it);
+          assert(cond_entry!=entry.first->second.conditions.end());
+
+          if(it->get_target()==cov.second.succ)
+          {
+            if(!cond_entry->second.false_taken)
+            {
+              cond_entry->second.false_taken=true;
+              ++branches_covered;
+            }
+          }
+          else
+          {
+            if(!cond_entry->second.true_taken)
+            {
+              cond_entry->second.true_taken=true;
+              ++branches_covered;
+            }
+          }
+        }
       }
     }
   }

src/cbmc/symex_coverage.h

@@ -29,11 +29,12 @@ class symex_coveraget
   {
   }
 
-  void covered(goto_programt::const_targett location)
+  void covered(
+    goto_programt::const_targett from,
+    goto_programt::const_targett to)
   {
-    std::pair<coveraget::iterator, bool> entry=
-      coverage.insert(std::make_pair(location,
-                                     coverage_infot(location, 1)));
+    std::pair<coverage_innert::iterator, bool> entry=
+      coverage[from].insert({to, coverage_infot(from, to, 1)});
 
     if(!entry.second)
       ++(entry.first->second.num_executions);
@@ -49,17 +50,22 @@ class symex_coveraget
   struct coverage_infot
   {
     coverage_infot(
-      goto_programt::const_targett _location,
+      goto_programt::const_targett _from,
+      goto_programt::const_targett _to,
       unsigned _num_executions):
-      location(_location), num_executions(_num_executions)
+      location(_from), num_executions(_num_executions),
+      succ(_to)
     {
     }
 
     goto_programt::const_targett location;
     unsigned num_executions;
+    goto_programt::const_targett succ;
   };
 
   typedef std::map<goto_programt::const_targett, coverage_infot>
+    coverage_innert;
+  typedef std::map<goto_programt::const_targett, coverage_innert>
     coveraget;
   coveraget coverage;