Merge pull request #5265 from danpoe/refactor/get-goto-model

Function to get a goto model from a C program for use in unit tests

Author: danpoe

unit/Makefile

@@ -16,6 +16,7 @@ SRC += analyses/ai/ai.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
        big-int/big-int.cpp \
        compound_block_locations.cpp \
+       get_goto_model_from_c_test.cpp \
        goto-checker/report_util/is_property_less_than.cpp \
        goto-instrument/cover_instrument.cpp \
        goto-instrument/cover/cover_only.cpp \

unit/get_goto_model_from_c_test.cpp

@@ -0,0 +1,40 @@
+/*******************************************************************\
+
+Module: Get goto model test
+
+Author: Daniel Poetzl
+
+\*******************************************************************/
+
+#include <testing-utils/get_goto_model_from_c.h>
+#include <testing-utils/use_catch.h>
+
+TEST_CASE("Get goto model from C test", "[core]")
+{
+  const std::string code =
+    "int g;"
+    "void f(int a) { int b; }"
+    "void main() {}";
+
+  const auto goto_model = get_goto_model_from_c(code);
+
+  const auto &function_map = goto_model.goto_functions.function_map;
+
+  REQUIRE(function_map.find("main") != function_map.end());
+  REQUIRE(function_map.find(CPROVER_PREFIX "_start") != function_map.end());
+  REQUIRE(function_map.find("f") != function_map.end());
+
+  const auto &main_instructions = function_map.at("main").body.instructions;
+  REQUIRE(!main_instructions.empty());
+
+  const auto &f_instructions = function_map.at("f").body.instructions;
+  REQUIRE(f_instructions.size() >= 2);
+
+  const auto &symbol_table = goto_model.symbol_table;
+
+  REQUIRE(symbol_table.has_symbol("main"));
+  REQUIRE(symbol_table.has_symbol(CPROVER_PREFIX "_start"));
+  REQUIRE(symbol_table.has_symbol("g"));
+  REQUIRE(symbol_table.has_symbol("f::a"));
+  REQUIRE(symbol_table.has_symbol("f::1::b"));
+}

unit/json_symbol_table.cpp

@@ -23,6 +23,7 @@
 #include <util/options.h>
 #include <util/symbol_table.h>
 
+#include <testing-utils/get_goto_model_from_c.h>
 #include <testing-utils/message.h>
 #include <testing-utils/use_catch.h>
 
@@ -49,67 +50,11 @@ class test_ui_message_handlert : public ui_message_handlert
   json_stream_arrayt json_stream_array;
 };
 
-void get_goto_model(std::istream &in, goto_modelt &goto_model)
-{
-  optionst options;
-  cbmc_parse_optionst::set_default_options(options);
-
-  messaget null_message(null_message_handler);
-
-  language_filest language_files;
-  language_files.set_message_handler(null_message_handler);
-
-  std::string filename;
-
-  language_filet &language_file = language_files.add_file(filename);
-
-  language_file.language = get_default_language();
-
-  languaget &language = *language_file.language;
-  language.set_message_handler(null_message_handler);
-  language.set_language_options(options);
-
-  {
-    bool r = language.parse(in, filename);
-    REQUIRE(!r);
-  }
-
-  language_file.get_modules();
-
-  {
-    bool r = language_files.typecheck(goto_model.symbol_table);
-    REQUIRE(!r);
-  }
-
-  REQUIRE(!goto_model.symbol_table.has_symbol(goto_functionst::entry_point()));
-
-  {
-    bool r = language_files.generate_support_functions(goto_model.symbol_table);
-    REQUIRE(!r);
-  }
-
-  goto_convert(
-    goto_model.symbol_table, goto_model.goto_functions, null_message_handler);
-}
-
 TEST_CASE("json symbol table read/write consistency")
 {
-  register_language(new_ansi_c_language);
-
-  cmdlinet cmdline;
-  config.main = std::string("main");
-  config.set(cmdline);
-
-  goto_modelt goto_model;
-
   // Get symbol table associated with goto program
-
-  {
-    std::string program = "int main() { return 0; }\n";
-
-    std::istringstream in(program);
-    get_goto_model(in, goto_model);
-  }
+  const std::string program = "int main() { return 0; }\n";
+  const auto goto_model = get_goto_model_from_c(program);
 
   const symbol_tablet &symbol_table1 = goto_model.symbol_table;
 

unit/testing-utils/Makefile

@@ -1,6 +1,7 @@
 SRC = \
   call_graph_test_utils.cpp \
   free_form_cmdline.cpp \
+  get_goto_model_from_c.cpp \
   invariant.cpp \
   message.cpp \
   require_expr.cpp \

unit/testing-utils/get_goto_model_from_c.cpp

@@ -0,0 +1,95 @@
+/*******************************************************************\
+
+Module: Get goto model
+
+Author: Daniel Poetzl
+
+\*******************************************************************/
+
+#include "get_goto_model_from_c.h"
+
+#include <ansi-c/ansi_c_language.h>
+
+#include <goto-programs/goto_convert_functions.h>
+
+#include <langapi/language_file.h>
+#include <langapi/mode.h>
+
+#include <util/cmdline.h>
+#include <util/config.h>
+#include <util/exception_utils.h>
+#include <util/invariant.h>
+#include <util/message.h>
+#include <util/options.h>
+#include <util/symbol_table.h>
+
+#include <testing-utils/message.h>
+
+goto_modelt get_goto_model_from_c(std::istream &in)
+{
+  {
+    const bool has_language = get_language_from_mode(ID_C) != nullptr;
+
+    if(!has_language)
+    {
+      register_language(new_ansi_c_language);
+    }
+  }
+
+  {
+    cmdlinet cmdline;
+
+    config = configt{};
+    config.main = std::string("main");
+    config.set(cmdline);
+  }
+
+  language_filest language_files;
+  language_files.set_message_handler(null_message_handler);
+
+  language_filet &language_file = language_files.add_file("");
+
+  language_file.language = get_language_from_mode(ID_C);
+  CHECK_RETURN(language_file.language);
+
+  languaget &language = *language_file.language;
+  language.set_message_handler(null_message_handler);
+
+  {
+    const bool error = language.parse(in, "");
+
+    if(error)
+      throw invalid_source_file_exceptiont("parsing failed");
+  }
+
+  language_file.get_modules();
+
+  goto_modelt goto_model;
+
+  {
+    const bool error = language_files.typecheck(goto_model.symbol_table);
+
+    if(error)
+      throw invalid_source_file_exceptiont("typechecking failed");
+  }
+
+  {
+    const bool error =
+      language_files.generate_support_functions(goto_model.symbol_table);
+
+    if(error)
+      throw invalid_source_file_exceptiont(
+        "support function generation failed");
+  }
+
+  goto_convert(
+    goto_model.symbol_table, goto_model.goto_functions, null_message_handler);
+
+  return goto_model;
+}
+
+goto_modelt get_goto_model_from_c(const std::string &code)
+{
+  std::istringstream in(code);
+  return get_goto_model_from_c(in);
+}

unit/testing-utils/get_goto_model_from_c.h

@@ -0,0 +1,28 @@
+/*******************************************************************\
+
+Module: Get goto model
+
+Author: Daniel Poetzl
+
+\*******************************************************************/
+
+#ifndef CPROVER_TESTING_UTILS_GET_GOTO_MODEL_FROM_C_H
+#define CPROVER_TESTING_UTILS_GET_GOTO_MODEL_FROM_C_H
+
+#include <goto-programs/goto_model.h>
+
+#include <iosfwd>
+
+/// Convert C program to a goto model
+///
+/// \param code: string giving the C program
+/// \return goto model
+goto_modelt get_goto_model_from_c(const std::string &code);
+
+/// Convert C program to a goto model
+///
+/// \param in: input stream to read a C program from
+/// \return goto model
+goto_modelt get_goto_model_from_c(const std::istream &in);
+
+#endif /* CPROVER_TESTING_UTILS_GET_GOTO_MODEL_FROM_C_H_ */

unit/testing-utils/module_dependencies.txt

@@ -1,5 +1,7 @@
+analyses
 ansi-c
 catch
+goto-programs
+langapi
 testing-utils
-util
-analyses
+util