Merge pull request #4584 from peterschrammel/move-xml-interface

Fix, refactor, move xml_interface

Author: tautschnig

regression/cbmc/xml-interface1/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+void foo(int x)
+{
+  for(int i = 0; i < 5; ++i)
+  {
+    if(x)
+      assert(0);
+    assert(0);
+  }
+  assert(0);
+}

regression/cbmc/xml-interface1/test.desc

@@ -0,0 +1,12 @@
+CORE
+--xml-interface
+< test.xml
+^EXIT=10$
+^SIGNAL=0$
+Not unwinding loop foo\.0 iteration 3 file main\.c line 5 function foo thread 0
+<result property="foo\.assertion\.3" status="SUCCESS"/>
+<result property="foo\.assertion\.1" status="FAILURE">
+<goto_trace>
+VERIFICATION FAILED
+--
+<result property="foo\.assertion\.2" status=

regression/cbmc/xml-interface1/test.xml

@@ -0,0 +1,9 @@
+<options>
+  <valueOption actual="main.c"/>
+  <valueOption name="function" actual="foo"/>
+  <valueOption name="unwind" actual="3"/>
+  <valueOption name="property" actual="foo.assertion.1"/>
+  <valueOption name="property" actual="foo.assertion.3"/>
+  <flagOption name="trace" actual="on"/>
+  <flagOption name="show-properties" actual="off"/>
+</options>

src/cbmc/Makefile

@@ -2,7 +2,6 @@ SRC = c_test_input_generator.cpp \
       cbmc_languages.cpp \
       cbmc_main.cpp \
       cbmc_parse_options.cpp \
-      xml_interface.cpp \
       # Empty last line
 
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \

src/cbmc/cbmc_parse_options.cpp

@@ -79,17 +79,18 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/mode.h>
 
+#include <xmllang/xml_interface.h>
+
 #include "c_test_input_generator.h"
-#include "xml_interface.h"
 
 cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
   : parse_options_baset(
       CBMC_OPTIONS,
       argc,
       argv,
-      std::string("CBMC ") + CBMC_VERSION),
-    xml_interfacet(cmdline)
+      std::string("CBMC ") + CBMC_VERSION)
 {
+  xml_interface(cmdline, ui_message_handler);
 }
 
 ::cbmc_parse_optionst::cbmc_parse_optionst(
@@ -100,9 +101,9 @@ ::cbmc_parse_optionst::cbmc_parse_optionst(
       CBMC_OPTIONS + extra_options,
       argc,
       argv,
-      std::string("CBMC ") + CBMC_VERSION),
-    xml_interfacet(cmdline)
+      std::string("CBMC ") + CBMC_VERSION)
 {
+  xml_interface(cmdline, ui_message_handler);
 }
 
 void cbmc_parse_optionst::set_default_options(optionst &options)

src/cbmc/cbmc_parse_options.h

@@ -31,8 +31,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <solvers/strings/string_refinement.h>
 
-#include "xml_interface.h"
-
 class goto_functionst;
 class optionst;
 
@@ -82,7 +80,7 @@ class optionst;
   "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 // clang-format on
 
-class cbmc_parse_optionst : public parse_options_baset, public xml_interfacet
+class cbmc_parse_optionst : public parse_options_baset
 {
 public:
   virtual int doit() override;

src/cbmc/xml_interface.h

@@ -65,18 +65,17 @@ ui_message_handlert::ui_message_handlert(
   const std::string &program)
   : ui_message_handlert(
       nullptr,
-      cmdline.isset("xml-ui") ? uit::XML_UI : cmdline.isset("json-ui")
-                                                ? uit::JSON_UI
-                                                : uit::PLAIN,
+      cmdline.isset("xml-ui") || cmdline.isset("xml-interface")
+        ? uit::XML_UI
+        : cmdline.isset("json-ui") ? uit::JSON_UI : uit::PLAIN,
       program,
       cmdline.isset("flush"),
-      cmdline.isset("timestamp")
-        ? cmdline.get_value("timestamp") == "monotonic"
-            ? timestampert::clockt::MONOTONIC
-            : cmdline.get_value("timestamp") == "wall"
-                ? timestampert::clockt::WALL_CLOCK
-                : timestampert::clockt::NONE
-        : timestampert::clockt::NONE)
+      cmdline.isset("timestamp") ? cmdline.get_value("timestamp") == "monotonic"
+                                     ? timestampert::clockt::MONOTONIC
+                                     : cmdline.get_value("timestamp") == "wall"
+                                         ? timestampert::clockt::WALL_CLOCK
+                                         : timestampert::clockt::NONE
+                                 : timestampert::clockt::NONE)
 {
   if(get_ui() == uit::PLAIN)
   {

src/util/ui_message.cpp

@@ -1,4 +1,5 @@
 SRC = graphml.cpp \
+      xml_interface.cpp \
       xml_lex.yy.cpp \
       xml_parse_tree.cpp \
       xml_parser.cpp \

src/xmllang/Makefile

@@ -13,52 +13,52 @@ Author: Daniel Kroening, [email protected]
 
 #include <iostream>
 
+#include <util/cmdline.h>
 #include <util/message.h>
 
 #include <xmllang/xml_parser.h>
 
-/// XML User Interface
-void xml_interfacet::get_xml_options(cmdlinet &cmdline)
-{
-  if(cmdline.isset("xml-interface"))
-  {
-    null_message_handlert message_handler;
-    xmlt xml;
-
-    parse_xml(std::cin, "", message_handler, xml);
-
-    get_xml_options(xml, cmdline);
-
-    cmdline.set("xml-ui");
-  }
-}
-
-/// XML User Interface
-void xml_interfacet::get_xml_options(
-  const xmlt &xml,
-  cmdlinet &cmdline)
+/// Parse commandline options from \p xml into \p cmdline
+static void get_xml_options(const xmlt &xml, cmdlinet &cmdline)
 {
   for(const auto &e : xml.elements)
   {
     // recursive call
     get_xml_options(e, cmdline);
   }
 
-  if(xml.name=="valueOption")
+  if(xml.name == "valueOption")
   {
-    std::string name=xml.get_attribute("name");
-    std::string value=xml.get_attribute("actual");
+    std::string name = xml.get_attribute("name");
+    std::string value = xml.get_attribute("actual");
 
-    if(name=="")
+    if(name == "")
       cmdline.args.push_back(value);
     else
       cmdline.set(name, value);
   }
-  else if(xml.name=="flagOption")
+  else if(xml.name == "flagOption")
   {
-    if(xml.get_attribute("actual")=="on")
+    if(xml.get_attribute("actual") == "on")
     {
       cmdline.set(xml.get_attribute("name"));
     }
   }
 }
+
+void xml_interface(cmdlinet &cmdline, message_handlert &message_handler)
+{
+  if(cmdline.isset("xml-interface"))
+  {
+    xmlt xml;
+
+    parse_xml(std::cin, "", message_handler, xml);
+
+    get_xml_options(xml, cmdline);
+
+    // Add this so that it gets propagated into optionst;
+    // the ui_message_handlert::uit has already been set on the basis
+    // of the xml-interface flag.
+    cmdline.set("xml-ui");
+  }
+}

src/cbmc/xml_interface.cpp renamed to src/xmllang/xml_interface.cpp

@@ -0,0 +1,34 @@
+/*******************************************************************\
+
+Module: XML Interface
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// XML Interface
+
+#ifndef CPROVER_XMLLANG_XML_INTERFACE_H
+#define CPROVER_XMLLANG_XML_INTERFACE_H
+
+class cmdlinet;
+class message_handlert;
+
+/// Parse XML-formatted commandline options from stdin.
+///
+/// Example:
+/// \code{.xml}
+/// <options>
+///   <valueOption actual="main.c"/>
+///   <valueOption name="function" actual="foo"/>
+///   <valueOption name="unwind" actual="3"/>
+///   <valueOption name="property" actual="foo.assertion.1"/>
+///   <valueOption name="property" actual="foo.assertion.3"/>
+///   <flagOption name="trace" actual="on"/>
+///   <flagOption name="show-properties" actual="off"/>
+/// </options>
+/// \endcode
+void xml_interface(cmdlinet &, message_handlert &);
+
+#endif // CPROVER_XMLLANG_XML_INTERFACE_H

src/xmllang/xml_interface.h

@@ -102,7 +102,6 @@ testing-utils-clean:
 BMC_DEPS =../src/cbmc/c_test_input_generator$(OBJEXT) \
           ../src/cbmc/cbmc_languages$(OBJEXT) \
           ../src/cbmc/cbmc_parse_options$(OBJEXT) \
-          ../src/cbmc/xml_interface$(OBJEXT) \
           ../src/goto-instrument/source_lines$(OBJEXT) \
           ../src/goto-instrument/cover$(OBJEXT) \
           ../src/goto-instrument/cover_basic_blocks$(OBJEXT) \