Merge pull request #5373 from NlightNFotis/fix-weird-identifier-names

Filter out illegal characters from identifiers in typecheck_expr.

Author: NlightNFotis

regression/CMakeLists.txt

@@ -38,6 +38,7 @@ add_subdirectory(smt2_strings)
 add_subdirectory(strings)
 add_subdirectory(invariants)
 add_subdirectory(goto-diff)
+add_subdirectory(goto-cc-instrument-cbmc)
 add_subdirectory(test-script)
 add_subdirectory(goto-analyzer-taint)
 if(NOT WIN32)

regression/goto-cc-instrument-cbmc/CMakeLists.txt

@@ -0,0 +1,9 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:cbmc> $<TARGET_FILE:goto-instrument> ${is_windows}"
+)

regression/goto-cc-instrument-cbmc/Makefile

@@ -0,0 +1,38 @@
+default: tests.log
+
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+	is_windows=true
+else
+	exe=../../../src/goto-cc/goto-cc
+	is_windows=false
+endif
+
+cbmc=../../../src/cbmc/cbmc
+goto-instrument=../../../src/goto-instrument/goto-instrument
+
+test:
+	@../test.pl -e -p -c '../chain.sh $(exe) $(cbmc) $(goto-instrument) $(is_windows)'
+
+tests.log:
+	@../test.pl -e -p -c '../chain.sh $(exe) $(cbmc) $(goto-instrument) $(is_windows)'
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@for dir in *; do \
+		$(RM) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb; \
+			cd ..; \
+		fi \
+	done

regression/goto-cc-instrument-cbmc/chain.sh

@@ -0,0 +1,21 @@
+#!/usr/bin/env bash
+
+goto_cc=$1
+cbmc=$2
+goto_instrument=$3
+is_windows=$4
+
+name=${*:$#}
+base_name=${name%.c}
+modified_name=${base_name}.modified.c
+
+if [[ "${is_windows}" == "true" ]]; then
+  "${goto_cc}" "${name}"
+  mv "${base_name}.exe" "${base_name}.gb"
+else
+  "${goto_cc}" "${name}" -o "${base_name}.gb"
+fi
+
+"${goto_instrument}" "${base_name}.gb" --dump-c "${modified_name}"
+
+"${cbmc}" "${modified_name}"

regression/goto-cc-instrument-cbmc/identifier_names_illegal_characters/test.c

@@ -0,0 +1,7 @@
+int main(void)
+{
+  void *v, *x, *x_before;
+  x_before = x;
+  __atomic_store_n(&x, 42, 0);
+  __atomic_exchange_n(&x, 42, 0);
+}

regression/goto-cc-instrument-cbmc/identifier_names_illegal_characters/test.desc

@@ -0,0 +1,15 @@
+CORE
+test.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^PARSING ERROR$
+^CONVERSION ERROR$
+--
+Example of an illegal identifier name we crashed on before:
+__atomic_compare_exchange_n_*{V}$V$
+
+Example of the substitutes we are producing now.
+__atomic_compare_exchange__ptr__start_sub_V_end_sub_

src/ansi-c/c_typecheck_expr.cpp

@@ -1890,16 +1890,18 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
         INVARIANT(
           !parameters.empty(),
           "GCC polymorphic built-ins should have at least one parameter");
+        /// XXX why are we only looking at the type of the first parameter?
         if(parameters.front().type().id() == ID_pointer)
         {
           identifier_with_type =
             id2string(identifier) + "_" +
-            type2name(parameters.front().type().subtype(), *this);
+            type2identifier(parameters.front().type().subtype(), *this);
         }
         else
         {
-          identifier_with_type = id2string(identifier) + "_" +
-                                 type2name(parameters.front().type(), *this);
+          identifier_with_type =
+            id2string(identifier) + "_" +
+            type2identifier(parameters.front().type(), *this);
         }
         gcc_polymorphic->set_identifier(identifier_with_type);
 

src/ansi-c/type2name.cpp

@@ -272,3 +272,32 @@ std::string type2name(const typet &type, const namespacet &ns)
   symbol_numbert symbol_number;
   return type2name(type, ns, symbol_number);
 }
+
+/// type2name generates strings that aren't valid C identifiers
+/// If we want utilities like dump_c to work properly identifiers
+/// should ideally always be valid C identifiers
+/// This replaces some invalid characters that can appear in type2name output.
+std::string type2identifier(const typet &type, const namespacet &ns)
+{
+  auto type2name_res = type2name(type, ns);
+  std::string result{};
+  for(char c : type2name_res)
+  {
+    switch(c)
+    {
+    case '*':
+      result += "_ptr_";
+      break;
+    case '{':
+      result += "_start_sub_";
+      break;
+    case '}':
+      result += "_end_sub_";
+      break;
+    default:
+      result += c;
+      break;
+    }
+  }
+  return result;
+}

src/ansi-c/type2name.h

@@ -20,4 +20,6 @@ class namespacet;
 
 std::string type2name(const typet &type, const namespacet &ns);
 
+std::string type2identifier(const typet &type, const namespacet &ns);
+
 #endif // CPROVER_ANSI_C_TYPE2NAME_H