Merge pull request #165 from diffblue/feature/wrap_entry_point

[TYT-2] Support for wrapping the entry point in an infinite loop in the different tools

Author: NlightNFotis

regression/cbmc/wrap_entry_point_in_while_true/main.c

@@ -0,0 +1,4 @@
+int main(int argc, char **argv)
+{
+    return 0;
+}

regression/cbmc/wrap_entry_point_in_while_true/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-goto-functions --wrap-entry-point-in-while
+^EXIT=0$
+^SIGNAL=0$
+^     1: main\(argc', argv'\);$
+^        GOTO 1$
+--

regression/cbmc/wrap_entry_point_in_while_true_custom_entry_point/main.c

@@ -0,0 +1,4 @@
+int skipWhitespace()
+{
+    return 120;
+}

regression/cbmc/wrap_entry_point_in_while_true_custom_entry_point/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-goto-functions --wrap-entry-point-in-while --function skipWhitespace
+^EXIT=0$
+^SIGNAL=0$
+^     1: skipWhitespace\(\);$
+^        GOTO 1$
+--

regression/goto-analyzer/wrap_entry_point_in_while_true/main.c

@@ -0,0 +1,4 @@
+int main(int argc, char **argv)
+{
+    return 0;
+}

regression/goto-analyzer/wrap_entry_point_in_while_true/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--show-goto-functions --wrap-entry-point-in-while
+^EXIT=6$
+^SIGNAL=0$
+^     1: IF FALSE THEN GOTO 2$
+^        main\(argc', argv'\);$
+^        GOTO 1$
+--

regression/goto-analyzer/wrap_entry_point_in_while_true_custom_entry_point/main.c

@@ -0,0 +1,4 @@
+int skipWhitespace()
+{
+    return 120;
+}

regression/goto-analyzer/wrap_entry_point_in_while_true_custom_entry_point/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--show-goto-functions --wrap-entry-point-in-while --function skipWhitespace
+^EXIT=6$
+^SIGNAL=0$
+^     1: IF FALSE THEN GOTO 2$
+^        skipWhitespace\(\);$
+^        GOTO 1$
+--

regression/goto-instrument/wrap_entry_point_in_while_true/main.c

@@ -0,0 +1,4 @@
+int main(int argc, char **argv)
+{
+    return 0;
+}

regression/goto-instrument/wrap_entry_point_in_while_true/test.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+--show-goto-functions --wrap-entry-point-in-while
+^EXIT=0$
+^SIGNAL=0$
+^     1: main\(argc', argv'\);$
+^        GOTO 1$
+--
+--
+This is tracked by the JIRA issue TYT-4: https://diffblue.atlassian.net/projects/TYT/issues/TYT-4

regression/goto-instrument/wrap_entry_point_in_while_true_custom_entry_point/main.c

@@ -0,0 +1,4 @@
+int skipWhitespace()
+{
+    return 120;
+}

regression/goto-instrument/wrap_entry_point_in_while_true_custom_entry_point/test.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+--show-goto-functions --wrap-entry-point-in-while --function skipWhitespace
+^EXIT=0$
+^SIGNAL=0$
+^     1: skipWhitespace\(\);$
+^        GOTO 1$
+--
+--
+This is tracked by the JIRA issue TYT-4: https://diffblue.atlassian.net/projects/TYT/issues/TYT-4

src/ansi-c/ansi_c_entry_point.cpp

@@ -22,9 +22,11 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/string_constant.h>
 
 #include <goto-programs/goto_functions.h>
+#include <langapi/wrap_entry_point.h>
 #include <linking/static_lifetime_init.h>
 
 #include "ansi_c_entry_point.h"
+#include "ansi_c_language.h"
 #include "c_nondet_symbol_factory.h"
 
 exprt::operandst build_function_environment(
@@ -121,7 +123,8 @@ void record_function_outputs(
 bool ansi_c_entry_point(
   symbol_tablet &symbol_table,
   const std::string &standard_main,
-  message_handlert &message_handler)
+  message_handlert &message_handler,
+  bool wrap_entry_point)
 {
   // check if entry point is already there
   if(symbol_table.symbols.find(goto_functionst::entry_point())!=
@@ -444,7 +447,15 @@ bool ansi_c_entry_point(
         message_handler);
   }
 
-  init_code.move_to_operands(call_main);
+  if(wrap_entry_point)
+  {
+    code_whilet wrapped_main=wrap_entry_point_in_while(call_main);
+    init_code.move_to_operands(wrapped_main);
+  }
+  else
+  {
+    init_code.move_to_operands(call_main);
+  }
 
   // TODO: add read/modified (recursively in call graph) globals as INPUT/OUTPUT
 

src/ansi-c/ansi_c_entry_point.h

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 bool ansi_c_entry_point(
   symbol_tablet &symbol_table,
   const std::string &standard_main,
-  message_handlert &message_handler);
+  message_handlert &message_handler,
+  bool wrap_entry_point);
 
 #endif // CPROVER_ANSI_C_ANSI_C_ENTRY_POINT_H

src/ansi-c/ansi_c_language.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/config.h>
 #include <util/get_base_name.h>
+#include <util/cmdline.h>
 
 #include <linking/linking.h>
 #include <linking/remove_internal_symbols.h>
@@ -26,6 +27,11 @@ Author: Daniel Kroening, [email protected]
 #include "ansi_c_internal_additions.h"
 #include "type2name.h"
 
+void ansi_c_languaget::get_language_options(const cmdlinet &cmd)
+{
+  wrap_entry_point=cmd.isset("wrap-entry-point-in-while");
+}
+
 std::set<std::string> ansi_c_languaget::extensions() const
 {
   return { "c", "i" };
@@ -126,8 +132,11 @@ bool ansi_c_languaget::typecheck(
 
 bool ansi_c_languaget::final(symbol_tablet &symbol_table)
 {
-  if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
+  if(ansi_c_entry_point(symbol_table, "main", get_message_handler(),
+     wrap_entry_point_in_while()))
+  {
     return true;
+  }
 
   return false;
 }

src/ansi-c/ansi_c_language.h

@@ -22,6 +22,9 @@ Author: Daniel Kroening, [email protected]
 class ansi_c_languaget:public languaget
 {
 public:
+  virtual void get_language_options(
+    const cmdlinet &) override;
+
   bool preprocess(
     std::istream &instream,
     const std::string &path,
@@ -76,6 +79,12 @@ class ansi_c_languaget:public languaget
 protected:
   ansi_c_parse_treet parse_tree;
   std::string parse_path;
+
+  bool wrap_entry_point_in_while() const
+  { return wrap_entry_point; }
+
+private:
+  bool wrap_entry_point;
 };
 
 languaget *new_ansi_c_language();

src/cbmc/cbmc_parse_options.cpp

@@ -57,6 +57,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/mode.h>
 
+#include <ansi-c/ansi_c_language.h>
+
 #include "cbmc_solvers.h"
 #include "cbmc_parse_options.h"
 #include "bmc.h"
@@ -1017,6 +1019,7 @@ void cbmc_parse_optionst::help()
     " --round-to-minus-inf         rounding towards minus infinity\n"
     " --round-to-zero              rounding towards zero\n"
     " --function name              set main function name\n"
+    HELP_WRAP_ENTRY_POINT_IN_WHILE_TRUE
     "\n"
     "Program representations:\n"
     " --show-parse-tree            show parse tree\n"

src/cbmc/cbmc_parse_options.h

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/parse_options.h>
 
 #include <langapi/language_ui.h>
+#include <langapi/wrap_entry_point.h>
 
 #include <analyses/goto_check.h>
 
@@ -63,6 +64,7 @@ class optionst;
   "(java-cp-include-files):" \
   "(localize-faults)(localize-faults-method):" \
   "(lazy-methods)" \
+  WRAP_ENTRY_POINT_IN_WHILE_TRUE \
   "(test-invariant-failure)" \
   "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 

src/cpp/cpp_language.cpp

@@ -16,7 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/config.h>
 #include <util/replace_symbol.h>
 #include <util/get_base_name.h>
-
+#include <util/cmdline.h>
 #include <linking/linking.h>
 
 #include <ansi-c/ansi_c_entry_point.h>
@@ -29,6 +29,11 @@ Author: Daniel Kroening, [email protected]
 #include "cpp_typecheck.h"
 #include "cpp_type2name.h"
 
+void cpp_languaget::get_language_options(const cmdlinet &cmd)
+{
+  wrap_entry_point=cmd.isset("wrap-entry-point-in-while");
+}
+
 std::set<std::string> cpp_languaget::extensions() const
 {
   std::set<std::string> s;
@@ -135,8 +140,11 @@ bool cpp_languaget::typecheck(
 
 bool cpp_languaget::final(symbol_tablet &symbol_table)
 {
-  if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
+  if(ansi_c_entry_point(symbol_table, "main", get_message_handler(),
+     wrap_entry_point_in_while()))
+  {
     return true;
+  }
 
   return false;
 }

src/cpp/cpp_language.h

@@ -24,6 +24,9 @@ Author: Daniel Kroening, [email protected]
 class cpp_languaget:public languaget
 {
 public:
+  virtual void get_language_options(
+    const cmdlinet &cmd) override;
+
   bool preprocess(
     std::istream &instream,
     const std::string &path,
@@ -85,6 +88,9 @@ class cpp_languaget:public languaget
 
   void modules_provided(std::set<std::string> &modules) override;
 
+  bool wrap_entry_point_in_while() const
+  { return wrap_entry_point; }
+
 protected:
   cpp_parse_treet cpp_parse_tree;
   std::string parse_path;
@@ -95,6 +101,9 @@ class cpp_languaget:public languaget
   {
     return "main";
   }
+
+private:
+  bool wrap_entry_point;
 };
 
 languaget *new_cpp_language();

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -757,6 +757,7 @@ void goto_analyzer_parse_optionst::help()
     " --gcc                        use GCC as preprocessor\n"
     #endif
     " --no-library                 disable built-in abstract C library\n"
+    HELP_WRAP_ENTRY_POINT_IN_WHILE_TRUE
     "\n"
     "Java Bytecode frontend options:\n"
     " --classpath dir/jar          set the classpath\n"

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -108,6 +108,7 @@ graphs in DOT format.
 #include <util/parse_options.h>
 
 #include <langapi/language_ui.h>
+#include <langapi/wrap_entry_point.h>
 
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
@@ -149,6 +150,7 @@ class optionst;
   "(unwind-bounds)" \
   "(unwind-bounds-threshold):" \
   "(unwindset)" \
+  WRAP_ENTRY_POINT_IN_WHILE_TRUE \
   "(functions-ignore)" \
   "(functions-full)"
 

src/goto-cc/compile.cpp

@@ -368,7 +368,7 @@ bool compilet::link()
     symbol_table.remove(goto_functionst::entry_point());
     compiled_functions.function_map.erase(goto_functionst::entry_point());
 
-    if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
+    if(ansi_c_entry_point(symbol_table, "main", get_message_handler(), false))
       return true;
 
     // entry_point may (should) add some more functions.

src/langapi/Makefile

@@ -2,6 +2,7 @@ SRC = language_ui.cpp \
       language_util.cpp \
       languages.cpp \
       mode.cpp \
+      wrap_entry_point.cpp \
       # Empty last line
 INCLUDES= -I ..
 

src/langapi/wrap_entry_point.cpp

@@ -0,0 +1,27 @@
+/*******************************************************************\
+
+Module: Wrap the designated entry point into a while(true) loop.
+
+Author: Diffblue Limited (c) 2017
+
+Date: August 2017
+
+\*******************************************************************/
+
+/// \file
+/// Wrap the designated entry point into a while(true) loop.
+
+#include "wrap_entry_point.h"
+
+// Build and return a while(true) statement nesting the function call
+// passed as a parameter.
+code_whilet wrap_entry_point_in_while(code_function_callt &call_main)
+{
+  exprt true_expr;
+  code_whilet while_expr;
+  true_expr.make_true();
+  while_expr.cond()=true_expr;
+  while_expr.body()=call_main;
+
+  return while_expr;
+}

src/langapi/wrap_entry_point.h

@@ -0,0 +1,26 @@
+/*******************************************************************\
+
+Module: Wrap the designated entry point into a while(true) loop.
+
+Author: Diffblue Limited (c) 2017
+
+Date: August 2017
+
+\*******************************************************************/
+
+#ifndef CPROVER_LANGAPI_WRAP_ENTRY_POINT_H
+#define CPROVER_LANGAPI_WRAP_ENTRY_POINT_H
+
+#include <util/std_code.h>
+
+/// Command line option (to be shared by the different tools)
+#define WRAP_ENTRY_POINT_IN_WHILE_TRUE "(wrap-entry-point-in-while)"
+
+/// Command line help text
+#define HELP_WRAP_ENTRY_POINT_IN_WHILE_TRUE \
+  " --wrap-entry-point-in-while  wrap the designated entry point function in a while(true) statement\n" // NOLINT(*)
+
+code_whilet wrap_entry_point_in_while(
+  code_function_callt &call_main);
+
+#endif // CPROVER_LANGAPI_WRAP_ENTRY_POINT_H