Merge pull request #324 from peterschrammel/refactor-graphml-witnesses

Refactor graphml witnesses

Author: kroening

regression/cbmc/graphml_witness1/main.c

@@ -0,0 +1,34 @@
+extern int __VERIFIER_nondet_int(void);
+
+typedef enum {
+  LIST_BEG,
+  LIST_END
+} end_point_t;
+
+typedef enum {
+  ITEM_PREV,
+  ITEM_NEXT
+} direction_t;
+
+void remove_one(end_point_t from)
+{
+  const direction_t next_field = (LIST_BEG == from) ? ITEM_NEXT : ITEM_PREV;
+}
+
+end_point_t rand_end_point(void)
+{
+  _Bool choice;
+  if (choice)
+    return LIST_BEG;
+  else
+    return LIST_END;
+}
+
+int main()
+{
+  remove_one(rand_end_point());
+
+  __CPROVER_assert(0, "");
+
+  return 0;
+}

regression/cbmc/graphml_witness1/test.desc

@@ -0,0 +1,78 @@
+CORE
+main.c
+--graphml-witness -
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+<graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
+  <key attr.name="invariant" attr.type="string" for="node" id="invariant"/>
+  <key attr.name="invariant.scope" attr.type="string" for="node" id="invariant.scope"/>
+  <key attr.name="nodeType" attr.type="string" for="node" id="nodetype">
+    <default>path</default>
+  </key>
+  <key attr.name="isFrontierNode" attr.type="boolean" for="node" id="frontier">
+    <default>false</default>
+  </key>
+  <key attr.name="isViolationNode" attr.type="boolean" for="node" id="violation">
+    <default>false</default>
+  </key>
+  <key attr.name="isEntryNode" attr.type="boolean" for="node" id="entry">
+    <default>false</default>
+  </key>
+  <key attr.name="isSinkNode" attr.type="boolean" for="node" id="sink">
+    <default>false</default>
+  </key>
+  <key attr.name="enterLoopHead" attr.type="boolean" for="edge" id="enterLoopHead">
+    <default>false</default>
+  </key>
+  <key attr.name="threadNumber" attr.type="int" for="node" id="thread">
+    <default>0</default>
+  </key>
+  <key attr.name="sourcecodeLanguage" attr.type="string" for="graph" id="sourcecodelang"/>
+  <key attr.name="programFile" attr.type="string" for="graph" id="programfile"/>
+  <key attr.name="programHash" attr.type="string" for="graph" id="programhash"/>
+  <key attr.name="specification" attr.type="string" for="graph" id="specification"/>
+  <key attr.name="architecture" attr.type="string" for="graph" id="architecture"/>
+  <key attr.name="producer" attr.type="string" for="graph" id="producer"/>
+  <key attr.name="sourcecode" attr.type="string" for="edge" id="sourcecode"/>
+  <key attr.name="startline" attr.type="int" for="edge" id="startline"/>
+  <key attr.name="control" attr.type="string" for="edge" id="control"/>
+  <key attr.name="assumption" attr.type="string" for="edge" id="assumption"/>
+  <key attr.name="assumption.resultfunction" attr.type="string" for="edge" id="assumption.resultfunction"/>
+  <key attr.name="assumption.scope" attr.type="string" for="edge" id="assumption.scope"/>
+  <key attr.name="enterFunction" attr.type="string" for="edge" id="enterFunction"/>
+  <key attr.name="returnFromFunction" attr.type="string" for="edge" id="returnFrom"/>
+  <key attr.name="witness-type" attr.type="string" for="graph" id="witness-type"/>
+  <graph edgedefault="directed">
+    <data key="sourcecodelang">C</data>
+    <node id="sink"/>
+    <node id="33.22">
+      <data key="entry">true</data>
+    </node>
+    <edge source="33.22" target="4.29">
+      <data key="originfile">main.c</data>
+      <data key="startline">21</data>
+    </edge>
+    <node id="4.29"/>
+    <edge source="4.29" target="29.31">
+      <data key="originfile">main.c</data>
+      <data key="startline">29</data>
+      <data key="assumption.scope">main</data>
+    </edge>
+    <node id="29.31"/>
+    <edge source="29.31" target="5.33">
+      <data key="originfile">main.c</data>
+      <data key="startline">15</data>
+      <data key="assumption.scope">remove_one</data>
+    </edge>
+    <node id="5.33">
+      <data key="violation">true</data>
+    </node>
+    <edge source="5.33" target="sink">
+      <data key="originfile">main.c</data>
+      <data key="startline">31</data>
+    </edge>
+  </graph>
+</graphml>
+--
+^warning: ignoring

src/cbmc/bmc.cpp

@@ -25,7 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/xml_goto_trace.h>
 #include <goto-programs/json_goto_trace.h>
-#include <goto-programs/graphml_goto_trace.h>
+#include <goto-programs/graphml_witness.h>
 
 #include <goto-symex/build_goto_trace.h>
 #include <goto-symex/slice.h>
@@ -106,20 +106,40 @@ void bmct::error_trace()
     }
     break;
   }
+}
 
-  const std::string graphml=options.get_option("graphml-cex");
-  if(!graphml.empty())
-  {
-    graphmlt cex_graph;
-    convert(ns, goto_trace, cex_graph);
+/*******************************************************************\
 
-    if(graphml=="-")
-      write_graphml(cex_graph, std::cout);
-    else
-    {
-      std::ofstream out(graphml);
-      write_graphml(cex_graph, out);
-    }
+Function: bmct::output_graphml
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: outputs witnesses in graphml format
+
+\*******************************************************************/
+
+void bmct::output_graphml(
+  resultt result,
+  const goto_functionst &goto_functions)
+{
+  const std::string graphml=options.get_option("graphml-witness");
+  if(graphml.empty())
+    return;
+
+  graphml_witnesst graphml_witness(ns);
+  if(result==UNSAFE)
+    graphml_witness(safety_checkert::error_trace);
+  else
+    return;
+
+  if(graphml=="-")
+    write_graphml(graphml_witness.graph(), std::cout);
+  else
+  {
+    std::ofstream out(graphml);
+    write_graphml(graphml_witness.graph(), out);
   }
 }
 
@@ -294,79 +314,77 @@ void bmct::show_program()
 
   std::cout << "\n" << "Program constraints:" << "\n";
 
-  for(symex_target_equationt::SSA_stepst::const_iterator
-      it=equation.SSA_steps.begin();
-      it!=equation.SSA_steps.end(); it++)
+  for(const auto &step : equation.SSA_steps)
   {
-    std::cout << "// " << it->source.pc->location_number << " ";
-    std::cout << it->source.pc->source_location.as_string() << "\n";
+    std::cout << "// " << step.source.pc->location_number << " ";
+    std::cout << step.source.pc->source_location.as_string() << "\n";
 
-    if(it->is_assignment())
+    if(step.is_assignment())
     {
       std::string string_value;
-      languages.from_expr(it->cond_expr, string_value);
+      languages.from_expr(step.cond_expr, string_value);
       std::cout << "(" << count << ") " << string_value << "\n";
 
-      if(!it->guard.is_true())
+      if(!step.guard.is_true())
       {
-        languages.from_expr(it->guard, string_value);
+        languages.from_expr(step.guard, string_value);
         std::cout << std::string(i2string(count).size()+3, ' ');
         std::cout << "guard: " << string_value << "\n";
       }
 
       count++;
     }
-    else if(it->is_assert())
+    else if(step.is_assert())
     {
       std::string string_value;
-      languages.from_expr(it->cond_expr, string_value);
+      languages.from_expr(step.cond_expr, string_value);
       std::cout << "(" << count << ") ASSERT("
                 << string_value <<") " << "\n";
 
-      if(!it->guard.is_true())
+      if(!step.guard.is_true())
       {
-        languages.from_expr(it->guard, string_value);
+        languages.from_expr(step.guard, string_value);
         std::cout << std::string(i2string(count).size()+3, ' ');
         std::cout << "guard: " << string_value << "\n";
       }
 
       count++;
     }
-    else if(it->is_assume())
+    else if(step.is_assume())
     {
       std::string string_value;
-      languages.from_expr(it->cond_expr, string_value);
+      languages.from_expr(step.cond_expr, string_value);
       std::cout << "(" << count << ") ASSUME("
                 << string_value <<") " << "\n";
 
-      if(!it->guard.is_true())
+      if(!step.guard.is_true())
       {
-        languages.from_expr(it->guard, string_value);
+        languages.from_expr(step.guard, string_value);
         std::cout << std::string(i2string(count).size()+3, ' ');
         std::cout << "guard: " << string_value << "\n";
       }
 
       count++;
     }
-    else if(it->is_constraint())
+    else if(step.is_constraint())
     {
       std::string string_value;
-      languages.from_expr(it->cond_expr, string_value);
+      languages.from_expr(step.cond_expr, string_value);
       std::cout << "(" << count << ") CONSTRAINT("
                 << string_value <<") " << "\n";
 
       count++;
     }
-    else if(it->is_shared_read() || it->is_shared_write())
+    else if(step.is_shared_read() || step.is_shared_write())
     {
       std::string string_value;
-      languages.from_expr(it->ssa_lhs, string_value);
-      std::cout << "(" << count << ") SHARED_" << (it->is_shared_write()?"WRITE":"READ") << "("
+      languages.from_expr(step.ssa_lhs, string_value);
+      std::cout << "(" << count << ") SHARED_" << (step.is_shared_write()?"WRITE":"READ") << "("
                 << string_value <<") " << "\n";
 
-      if(!it->guard.is_true())
+      if(!step.guard.is_true())
       {
-        languages.from_expr(it->guard, string_value);
+        languages.from_expr(step.guard, string_value);
         std::cout << std::string(i2string(count).size()+3, ' ');
         std::cout << "guard: " << string_value << "\n";
       }
@@ -611,6 +629,7 @@ safety_checkert::resultt bmct::stop_on_fail(
           dynamic_cast<bv_cbmct &>(prop_conv), equation, ns);
 
       error_trace();
+      output_graphml(UNSAFE, goto_functions);
     }
 
     report_failure();

src/cbmc/bmc.h

@@ -103,7 +103,10 @@ class bmct:public safety_checkert
   virtual void report_failure();
 
   virtual void error_trace();
-
+  void output_graphml(
+    resultt result,
+    const goto_functionst &goto_functions);
+  
   bool cover(
     const goto_functionst &goto_functions,
     const optionst::value_listt &criteria);

src/cbmc/cbmc_parse_options.cpp

@@ -454,8 +454,12 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("outfile"))
     options.set_option("outfile", cmdline.get_value("outfile"));
 
-  if(cmdline.isset("graphml-cex"))
-    options.set_option("graphml-cex", cmdline.get_value("graphml-cex"));
+  if(cmdline.isset("graphml-witness"))
+  {
+    options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
+    options.set_option("stop-on-fail", true);
+    options.set_option("trace", true);
+  }
 }
 
 /*******************************************************************\
@@ -1170,7 +1174,7 @@ void cbmc_parse_optionst::help()
     " --unwinding-assertions       generate unwinding assertions\n"
     " --partial-loops              permit paths with partial loops\n"
     " --no-pretty-names            do not simplify identifiers\n"
-    " --graphml-cex filename       write the counterexample in GraphML format to filename\n"
+    " --graphml-witness filename   write the witness in GraphML format to filename\n"
     "\n"
     "Backend options:\n"
     " --dimacs                     generate CNF in DIMACS format\n"

src/cbmc/cbmc_parse_options.h

@@ -53,7 +53,7 @@ class optionst;
   "(arrays-uf-always)(arrays-uf-never)" \
   "(string-abstraction)(no-arch)(arch):" \
   "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
-  "(graphml-cex):" \
+  "(graphml-witness):" \
   "(localize-faults)(localize-faults-method):" \
   "(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear
 

src/goto-programs/Makefile

@@ -15,7 +15,7 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \
       compute_called_functions.cpp link_to_library.cpp \
       remove_returns.cpp osx_fat_reader.cpp remove_complex.cpp \
       goto_trace.cpp xml_goto_trace.cpp vcd_goto_trace.cpp \
-      graphml_goto_trace.cpp remove_virtual_functions.cpp \
+      graphml_witness.cpp remove_virtual_functions.cpp \
       class_hierarchy.cpp show_goto_functions.cpp get_goto_model.cpp
 
 INCLUDES= -I ..