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

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/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,61 @@
+// Copyright 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+
+/// \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,31 @@
+// Copyright 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+
+/// \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>
+
+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