add the crangler tool

This is a command-line utility that makes changes to a preprocessed C file
that are prescribed in a JSON configuration file.

The initial set of transformations is as follows.
 * add a contract (pre/post/assigns) to a named C function
 * add a loop invariant to a loop identified by the name
   of the function its in and a loop number
 * remove the 'static' storage classifier from a function

The resulting source file is written into the directory of the original
file using the file extension ".i".

Author: kroening

regression/Makefile

@@ -3,6 +3,7 @@
 # listed with decreasing runtimes (i.e. longest running at the top)
 DIRS = cbmc \
        cbmc-library \
+       crangler \
        goto-analyzer \
        ansi-c \
        goto-instrument \

regression/crangler/Makefile

@@ -0,0 +1,20 @@
+default: tests.log
+
+include ../../src/config.inc
+include ../../src/common
+
+test:
+	@../test.pl -e -p -c '../../../src/crangler/crangler'
+
+tests.log:
+	@../test.pl -e -p -c '../../../src/crangler/crangler'
+
+clean:
+	@for dir in *; do \
+		$(RM) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb; \
+			cd ..; \
+		fi \
+	done

regression/crangler/remove-static/remove_static1.c

@@ -0,0 +1,14 @@
+int foo()
+{
+  return 0;
+}
+
+int bar();
+
+static void foobar1()
+{
+}
+
+void static foobar2()
+{
+}

regression/crangler/remove-static/remove_static1.desc

@@ -0,0 +1,8 @@
+CORE
+remove_static1.json
+
+^ void foobar1\(\)$
+^void  foobar2\(\)$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/crangler/remove-static/remove_static1.json

@@ -0,0 +1,14 @@
+{
+  "sources": [
+    "remove_static1.c"
+  ],
+  "functions": {
+    "foobar1": [
+      "remove static"
+    ],
+    "foobar2": [
+      "remove static"
+    ]
+  },
+  "output": "stdout"
+}

src/CMakeLists.txt

@@ -106,6 +106,7 @@ add_subdirectory(statement-list)
 add_subdirectory(util)
 
 add_subdirectory(cbmc)
+add_subdirectory(crangler)
 add_subdirectory(goto-cc)
 add_subdirectory(goto-instrument)
 add_subdirectory(goto-analyzer)

src/Makefile

@@ -4,6 +4,7 @@ DIRS = analyses \
        big-int \
        cbmc \
        cpp \
+       crangler \
        goto-analyzer \
        goto-cc \
        goto-checker \
@@ -27,6 +28,7 @@ DIRS = analyses \
        # Empty last line
 
 all: cbmc.dir \
+     crangler.dir \
      goto-analyzer.dir \
      goto-cc.dir \
      goto-diff.dir \
@@ -59,6 +61,8 @@ $(patsubst %, %.dir, $(filter-out big-int util, $(DIRS))): util.dir
 
 cpp.dir: ansi-c.dir linking.dir
 
+crangler.dir: util.dir json.dir
+
 languages: util.dir langapi.dir \
            cpp.dir ansi-c.dir xmllang.dir assembler.dir \
            jsil.dir json.dir json-symtab-language.dir statement-list.dir

src/crangler/CMakeLists.txt

@@ -0,0 +1,28 @@
+
+generic_flex(c)
+
+# Library
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+list(REMOVE_ITEM sources
+    ${CMAKE_CURRENT_SOURCE_DIR}/crangler_main.cpp
+)
+
+add_library(crangler-lib
+    ${sources}
+    ${BISON_parser_OUTPUTS}
+)
+
+generic_includes(crangler-lib)
+
+target_link_libraries(crangler-lib
+    big-int
+    util
+    json
+)
+
+# Executable
+add_executable(crangler crangler_main.cpp)
+target_link_libraries(crangler crangler-lib)
+
+install(TARGETS crangler DESTINATION ${CMAKE_INSTALL_BINDIR})
+

src/crangler/Makefile

@@ -0,0 +1,36 @@
+SRC = c_defines.cpp \
+      c_lex.yy.cpp \
+      c_wrangler.cpp \
+      crangler_main.cpp \
+      crangler_parse_options.cpp \
+      cscanner.cpp \
+      ctokenit.cpp \
+      mini_c_parser.cpp \
+      # Empty last line
+
+OBJ += ../big-int/big-int$(LIBEXT) \
+       ../json/json$(LIBEXT) \
+       ../util/util$(LIBEXT)
+
+INCLUDES= -I ..
+
+include ../config.inc
+include ../../$(CPROVER_DIR)/src/common
+
+CLEANFILES = crangler$(LIBEXT)
+
+all: crangler$(EXEEXT)
+
+###############################################################################
+
+c_lex.yy.cpp: scanner.l
+	$(LEX) -Pyyc -o$@ scanner.l
+
+###############################################################################
+
+generated_files: c_lex.yy.cpp
+
+###############################################################################
+
+crangler$(EXEEXT): $(OBJ)
+	$(LINKBIN)

src/crangler/c_defines.cpp

@@ -0,0 +1,67 @@
+/*******************************************************************\
+
+Module: C Defines
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// c_defines
+
+#include "c_defines.h"
+
+#include "cscanner.h"
+
+#include <util/prefix.h>
+#include <util/string_utils.h>
+
+#include <sstream>
+
+void c_definest::parse(const std::string &src)
+{
+  const auto lines = split_string(src, '\n');
+  for(const auto &line : lines)
+  {
+    // #define __x86_64__ 1
+    // #define getc_unlocked(fp) __sgetc(fp)
+    if(!has_prefix(line, "#define "))
+      continue;
+
+    auto space_pos = line.find(' ', 8);
+    if(space_pos == std::string::npos)
+      continue;
+
+    auto id = line.substr(8, space_pos - 8);
+    auto value = line.substr(space_pos + 1, std::string::npos);
+    map[id].value = value;
+  }
+}
+
+std::string c_definest::operator()(const std::string &src) const
+{
+  // tokenize
+  std::istringstream in(src);
+  cscannert cscanner(in);
+  const auto tokens = cscanner.get_tokens();
+
+  // output
+  std::ostringstream out;
+  for(auto &t : tokens)
+  {
+    if(is_identifier(t))
+    {
+      auto m_it = map.find(t.text);
+      if(m_it != map.end())
+      {
+        out << m_it->second.value;
+      }
+      else
+        out << t.text;
+    }
+    else
+      out << t.text;
+  }
+
+  return out.str();
+}

src/crangler/c_defines.h

@@ -0,0 +1,39 @@
+/*******************************************************************\
+
+Module: C Defines
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// c_defines
+
+#ifndef CPROVER_CRANGLER_C_DEFINES_H
+#define CPROVER_CRANGLER_C_DEFINES_H
+
+#include <util/optional.h>
+
+#include <string>
+#include <unordered_map>
+#include <vector>
+
+/// This class maintains a representation of one assignment to the
+/// preprocessor macros in a C program.
+class c_definest
+{
+public:
+  struct definet
+  {
+    optionalt<std::vector<std::string>> parameters;
+    std::string value;
+  };
+
+  using mapt = std::unordered_map<std::string, definet>;
+  mapt map;
+
+  void parse(const std::string &);
+  std::string operator()(const std::string &) const;
+};
+
+#endif // CPROVER_CRANGLER_C_DEFINES_H