Merge pull request #204 from peterschrammel/test-output

Split test output into goals and tests

Author: Daniel Kroening

src/cbmc/bmc_cover.cpp

@@ -117,7 +117,6 @@ class bmc_covert:
 
     // if satisified, we compute a goto_trace
     bool satisfied;
-    goto_tracet goto_trace;
 
     goalt(
       const std::string &_description,
@@ -143,6 +142,12 @@ class bmc_covert:
       return disjunction(tmp);
     }
   };
+
+  struct testt
+  {
+    goto_tracet goto_trace;
+    std::vector<irep_idt> covered_goals;
+  };
 
   inline irep_idt id(goto_programt::const_targett loc)
   {
@@ -151,8 +156,10 @@ class bmc_covert:
 
   typedef std::map<irep_idt, goalt> goal_mapt;
   goal_mapt goal_map;
+  typedef std::vector<testt> testst;
+  testst tests;
 
-  std::string get_test(const goto_tracet &goto_trace)
+  std::string get_test(const goto_tracet &goto_trace) const
   {
     bool first=true;
     std::string test;
@@ -196,6 +203,8 @@ Function: bmc_covert::satisfying_assignment
 
 void bmc_covert::satisfying_assignment()
 {
+  tests.push_back(testt());
+  testt &test = tests.back();
   for(auto &g_it : goal_map)
   {
     goalt &g=g_it.second;
@@ -212,13 +221,13 @@ void bmc_covert::satisfying_assignment()
       {
         status() << "Covered " << g.description << messaget::eom;
         g.satisfied=true;
-        symex_target_equationt::SSA_stepst::iterator next=c_it.step;
-        next++; // include the instruction itself
-        build_goto_trace(bmc.equation, next, solver, bmc.ns, g.goto_trace);
+        test.covered_goals.push_back(g_it.first);
         break;
       }
     }
   }
+  build_goto_trace(bmc.equation, bmc.equation.SSA_steps.end(), 
+                   solver, bmc.ns, test.goto_trace);
 }
 
 /*******************************************************************\
@@ -378,88 +387,101 @@ bool bmc_covert::operator()()
       {
         const goalt &goal=it.second;
 
-        xmlt xml_result("result");
-        xml_result.set_attribute("goal", id2string(it.first));
+        xmlt xml_result("goal");
+        xml_result.set_attribute("id", id2string(it.first));
         xml_result.set_attribute("description", goal.description);
         xml_result.set_attribute("status", goal.satisfied?"SATISFIED":"FAILED");
 
         if(goal.source_location.is_not_nil())
           xml_result.new_element()=xml(goal.source_location);
 
-        if(goal.satisfied)
+        std::cout << xml_result << "\n";
+      }
+
+      for(const auto & test : tests)
+      {
+        xmlt xml_result("test");
+        if(bmc.options.get_bool_option("trace"))
         {
-          if(bmc.options.get_bool_option("trace"))
-          {
-            convert(bmc.ns, goal.goto_trace, xml_result.new_element());
-          }
-          else
-          {
-            xmlt &xml_test=xml_result.new_element("test");
+          convert(bmc.ns, test.goto_trace, xml_result.new_element());
+        }
+        else
+        {
+          xmlt &xml_test=xml_result.new_element("inputs");
 
-            for(const auto & step : goal.goto_trace.steps)
+          for(const auto & step : test.goto_trace.steps)
+          {
+            if(step.is_input())
             {
-              if(step.is_input())
-              {
-                xmlt &xml_input=xml_test.new_element("input");
-                xml_input.set_attribute("id", id2string(step.io_id));
-                if(step.io_args.size()==1)
-                  xml_input.new_element("value")=
-                    xml(step.io_args.front(), bmc.ns);
-              }
+              xmlt &xml_input=xml_test.new_element("input");
+              xml_input.set_attribute("id", id2string(step.io_id));
+              if(step.io_args.size()==1)
+                xml_input.new_element("value")=
+                  xml(step.io_args.front(), bmc.ns);
             }
-            
           }
         }
 
+        for(const auto & goal_id : test.covered_goals)
+        {
+          xmlt &xml_goal=xml_result.new_element("goal");
+          xml_goal.set_attribute("id", id2string(goal_id));
+        }
+    
         std::cout << xml_result << "\n";
       }
-
       break;
     }
     case ui_message_handlert::JSON_UI:
     {
       json_objectt json_result;
-      json_arrayt &result_array=json_result["results"].make_array();
+      json_arrayt &goals_array=json_result["goals"].make_array();
       for(const auto & it : goal_map)
       {
         const goalt &goal=it.second;
 
-        json_objectt &result=result_array.push_back().make_object();
+        json_objectt &result=goals_array.push_back().make_object();
         result["status"]=json_stringt(goal.satisfied?"satisfied":"failed");
         result["goal"]=json_stringt(id2string(it.first));
         result["description"]=json_stringt(goal.description);
 
         if(goal.source_location.is_not_nil())
           result["sourceLocation"]=json(goal.source_location);
+      }
+      json_result["totalGoals"]=json_numbert(i2string(goal_map.size()));
+      json_result["goalsCovered"]=json_numbert(i2string(goals_covered));
 
-        if(goal.satisfied)
+      json_arrayt &tests_array=json_result["tests"].make_array();
+      for(const auto & test : tests)
+      {
+        json_objectt &result=tests_array.push_back().make_object();
+        if(bmc.options.get_bool_option("trace"))
         {
-          if(bmc.options.get_bool_option("trace"))
-          {
-            jsont &json_trace=result["trace"];
-            convert(bmc.ns, goal.goto_trace, json_trace);
-          }
-          else
-          {
-            json_arrayt &json_test=result["test"].make_array();
+          jsont &json_trace=result["trace"];
+          convert(bmc.ns, test.goto_trace, json_trace);
+        }
+        else
+        {
+          json_arrayt &json_test=result["inputs"].make_array();
 
-            for(const auto & step : goal.goto_trace.steps)
+          for(const auto & step : test.goto_trace.steps)
+          {
+            if(step.is_input())
             {
-              if(step.is_input())
-              {
-                json_objectt json_input;
-                json_input["id"]=json_stringt(id2string(step.io_id));
-                if(step.io_args.size()==1)
-                  json_input["value"]=json(step.io_args.front(), bmc.ns);
-                json_test.push_back(json_input);
-              }
+              json_objectt json_input;
+              json_input["id"]=json_stringt(id2string(step.io_id));
+              if(step.io_args.size()==1)
+                json_input["value"]=json(step.io_args.front(), bmc.ns);
+              json_test.push_back(json_input);
             }
-            
           }
         }
+        json_arrayt &goal_refs=result["coveredGoals"].make_array();
+        for(const auto & goal_id : test.covered_goals)
+        {
+          goal_refs.push_back(json_stringt(id2string(goal_id)));
+        }
       }
-      json_result["totalGoals"]=json_numbert(i2string(goal_map.size()));
-      json_result["goalsCovered"]=json_numbert(i2string(goals_covered));
       std::cout << ",\n" << json_result;
       break;
     }
@@ -478,16 +500,10 @@ bool bmc_covert::operator()()
 
   if(bmc.ui==ui_message_handlert::PLAIN)
   {
-    std::set<std::string> tests;
-
-    for(const auto & it : goal_map)
-      if(it.second.satisfied)
-        tests.insert(get_test(it.second.goto_trace));
-    
     std::cout << "Test suite:" << '\n';
 
-    for(const auto & t : tests)
-      std::cout << t << '\n';
+    for(const auto & test : tests)
+      std::cout << get_test(test.goto_trace) << '\n';
   }
 
   return false;

src/goto-programs/json_goto_trace.cpp

@@ -89,20 +89,19 @@ void convert(
         if(!json_location.is_null())
           json_assignment["sourceLocation"]=json_location;
 
-        std::string value_string, binary_string, type_string,
-                    full_lhs_string, full_lhs_value_string;
-        
-        //if(it.lhs_object_value.is_not_nil())
-        //  value_string=from_expr(ns, identifier, it.lhs_object_value);
+        std::string value_string, binary_string, type_string, full_lhs_string;
+        json_objectt full_lhs_value;
 
         if(it.full_lhs.is_not_nil())
           full_lhs_string=from_expr(ns, identifier, it.full_lhs);
 
+#if 0
         if(it.full_lhs_value.is_not_nil())
           full_lhs_value_string=from_expr(ns, identifier, it.full_lhs_value);
+#endif
 
-        //if(it.lhs_object_value.type().is_not_nil())
-        //  type_string=from_type(ns, identifier, it.lhs_object_value.type());
+        if(it.full_lhs_value.is_not_nil())
+          full_lhs_value = json(it.full_lhs_value, ns);
 
         const symbolt *symbol;
         irep_idt base_name, display_name;
@@ -117,7 +116,7 @@ void convert(
           json_assignment["mode"]=json_stringt(id2string(symbol->mode));
         }
 
-        json_assignment["value"]=json_stringt(full_lhs_value_string);
+        json_assignment["value"]=full_lhs_value;
         json_assignment["lhs"]=json_stringt(full_lhs_string);
         json_assignment["hidden"]=jsont::json_boolean(it.hidden);
         json_assignment["thread"]=json_numbert(i2string(it.thread_nr));
@@ -144,8 +143,7 @@ void convert(
           if(l_it.is_nil())
             json_values.push_back(json_stringt(""));
           else
-            json_values.push_back(
-              json_stringt(from_expr(ns, "", l_it)));
+            json_values.push_back(json(l_it, ns));
         }
 
         if(!json_location.is_null())
@@ -169,8 +167,7 @@ void convert(
           if(l_it.is_nil())
             json_values.push_back(json_stringt(""));
           else
-            json_values.push_back(
-              json_stringt(from_expr(ns, "", l_it)));
+            json_values.push_back(json(l_it, ns));
         }
 
         if(!json_location.is_null())

src/util/json_expr.cpp

@@ -130,7 +130,7 @@ json_objectt json(
   else if(type.id()==ID_struct)
   {
     result["name"]=json_stringt("struct");
-    json_arrayt members=result["members"].make_array();
+    json_arrayt &members=result["members"].make_array();
     const union_typet::componentst &components=
       to_union_type(type).components();
     for(const auto & it : components)
@@ -143,7 +143,7 @@ json_objectt json(
   else if(type.id()==ID_union)
   {
     result["name"]=json_stringt("union");
-    json_arrayt members=result["members"].make_array();
+    json_arrayt &members=result["members"].make_array();
     const union_typet::componentst &components=
       to_union_type(type).components();
     for(const auto & it : components)
@@ -274,7 +274,7 @@ json_objectt json(
   else if(expr.id()==ID_array)
   {
     result["name"]=json_stringt("array");
-    json_arrayt elements=result["elements"].make_array();
+    json_arrayt &elements=result["elements"].make_array();
 
     unsigned index=0;
 
@@ -297,7 +297,7 @@ json_objectt json(
       const struct_typet::componentst &components=struct_type.components();
       assert(components.size()==expr.operands().size());
 
-      json_arrayt members=result["members"].make_array();
+      json_arrayt &members=result["members"].make_array();
       for(unsigned m=0; m<expr.operands().size(); m++)
       {
         json_objectt &e=members.push_back().make_object();