Merge pull request #1108 from karkhaz/kk-neu-cprover-remove

goto-gcc removes CPROVER macros for native gcc

Author: tautschnig

appveyor.yml

@@ -109,6 +109,7 @@ test_script:
     rmdir /s /q cbmc-java\classpath1
     rmdir /s /q cbmc-java\jar-file3
     rmdir /s /q cbmc-java\tableswitch2
+    rmdir /s /q goto-gcc
     rmdir /s /q goto-instrument\slice08
 
     make test

regression/Makefile

@@ -6,6 +6,7 @@ DIRS = ansi-c \
        cbmc-cover \
        goto-analyzer \
        goto-diff \
+       goto-gcc \
        goto-instrument \
        goto-instrument-typedef \
        invariants \
@@ -14,9 +15,14 @@ DIRS = ansi-c \
        test-script \
        # Empty last line
 
-
+# Check for the existence of $dir. Tests under goto-gcc cannot be run on
+# Windows, so appveyor.yml unlinks the entire directory under Windows.
 test:
-	$(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;)
+	@for dir in $(DIRS); do \
+	  if [ -d "$$dir" ]; then \
+	    $(MAKE) -C "$$dir" test || exit 1; \
+	  fi; \
+	done;
 
 clean:
 	@for dir in *; do \

regression/goto-gcc/Makefile

@@ -0,0 +1,27 @@
+default: tests.log
+
+test:
+	-@ln -s goto-cc ../../src/goto-cc/goto-gcc
+	@if ! ../test.pl -c ../../../src/goto-cc/goto-gcc ; then \
+	  ../failed-tests-printer.pl ; \
+	  exit 1 ; \
+	fi
+
+tests.log: ../test.pl
+	-@ln -s goto-cc ../../src/goto-cc/goto-gcc
+	@if ! ../test.pl -c ../../../src/goto-cc/goto-gcc ; then \
+	  ../failed-tests-printer.pl ; \
+	  exit 1 ; \
+	fi
+
+show:
+	@for dir in *; do \
+	  if [ -d "$$dir" ]; then \
+	    vim -o "$$dir/*.c" "$$dir/*.out"; \
+	  fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log

regression/goto-gcc/ignore_cprover_macros/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  unsigned x;
+  __CPROVER_assume(x);
+  __CPROVER_assert(x, "");
+}

regression/goto-gcc/ignore_cprover_macros/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+--
+goto-gcc must define out all CPROVER macros that are used in the
+codebase. This test succeeds iff GCC doesn't see the CPROVER macros in
+the test file.

src/goto-cc/compile.cpp

@@ -379,7 +379,7 @@ bool compilet::link()
       output_file_executable, symbol_table, compiled_functions))
     return true;
 
-  return false;
+  return add_written_cprover_symbols(symbol_table);
 }
 
 /// parses source files and writes object files, or keeps the symbols in the
@@ -430,6 +430,9 @@ bool compilet::compile()
       if(write_object_file(cfn, symbol_table, compiled_functions))
         return true;
 
+      if(add_written_cprover_symbols(symbol_table))
+        return true;
+
       symbol_table.clear(); // clean symbol table for next source file.
       compiled_functions.clear();
     }
@@ -616,6 +619,7 @@ bool compilet::write_bin_object_file(
                << "; " << cnt << " have a body." << eom;
 
   outfile.close();
+  wrote_object=true;
 
   return false;
 }
@@ -650,6 +654,7 @@ compilet::compilet(cmdlinet &_cmdline, ui_message_handlert &mh, bool Werror):
 {
   mode=COMPILE_LINK_EXECUTABLE;
   echo_file_name=false;
+  wrote_object=false;
   working_directory=get_current_working_directory();
 }
 
@@ -724,3 +729,28 @@ void compilet::convert_symbols(goto_functionst &dest)
     }
   }
 }
+
+bool compilet::add_written_cprover_symbols(const symbol_tablet &symbol_table)
+{
+  for(const auto &pair : symbol_table.symbols)
+  {
+    const irep_idt &name=pair.second.name;
+    const typet &new_type=pair.second.type;
+    if(!(has_prefix(id2string(name), CPROVER_PREFIX) && new_type.id()==ID_code))
+      continue;
+
+    bool inserted;
+    std::map<irep_idt, symbolt>::iterator old;
+    std::tie(old, inserted)=written_macros.insert({name, pair.second});
+
+    if(!inserted && old->second.type!=new_type)
+    {
+      error() << "Incompatible CPROVER macro symbol types:" << eom
+              << old->second.type.pretty() << "(at " << old->second.location
+              << ")" << eom << "and" << eom << new_type.pretty()
+              << "(at " << pair.second.location << ")" << eom;
+      return true;
+    }
+  }
+  return false;
+}

src/goto-cc/compile.h

@@ -72,6 +72,23 @@ class compilet:public language_uit
     const symbol_tablet &,
     goto_functionst &);
 
+  /// \brief Has this compiler written any object files?
+  bool wrote_object_files() const { return wrote_object; }
+
+  /// \brief `__CPROVER_...` macros written to object files and their arities
+  ///
+  /// \return A mapping from every `__CPROVER` macro that this compiler
+  /// wrote to one or more object files, to how many parameters that
+  /// `__CPROVER` macro has.
+  void cprover_macro_arities(std::map<irep_idt,
+                                      std::size_t> &cprover_macros) const
+  {
+    PRECONDITION(wrote_object);
+    for(const auto &pair : written_macros)
+      cprover_macros.insert({pair.first,
+        to_code_type(pair.second.type).parameters().size()});
+  }
+
 protected:
   cmdlinet &cmdline;
   bool warning_is_fatal;
@@ -81,6 +98,16 @@ class compilet:public language_uit
   void add_compiler_specific_defines(class configt &config) const;
 
   void convert_symbols(goto_functionst &dest);
+
+  bool add_written_cprover_symbols(const symbol_tablet &symbol_table);
+  std::map<irep_idt, symbolt> written_macros;
+
+  // clients must only call add_written_cprover_symbols() if an object
+  // file has been written. The case where an object file was written
+  // but there were no __CPROVER symbols in the goto-program is distinct
+  // from the case where the user forgot to write an object file before
+  // calling add_written_cprover_symbols().
+  bool wrote_object;
 };
 
 #endif // CPROVER_GOTO_CC_COMPILE_H

src/goto-cc/gcc_mode.cpp

@@ -19,10 +19,13 @@ Author: CM Wintersteiger, 2006
 #include <sysexits.h>
 #endif
 
+#include <cstddef>
 #include <cstdio>
 #include <iostream>
 #include <fstream>
 #include <cstring>
+#include <numeric>
+#include <sstream>
 
 #include <util/string2int.h>
 #include <util/invariant.h>
@@ -337,10 +340,16 @@ int gcc_modet::doit()
       std::cout << "gcc version 3.4.4 (goto-cc " CBMC_VERSION ")\n";
   }
 
+  compilet compiler(cmdline,
+                    gcc_message_handler,
+                    cmdline.isset("Werror") &&
+                    cmdline.isset("Wextra") &&
+                    !cmdline.isset("Wno-error"));
+
   if(cmdline.isset("version"))
   {
     if(produce_hybrid_binary)
-      return run_gcc();
+      return run_gcc(compiler);
 
     std::cout << '\n' <<
       "Copyright (C) 2006-2014 Daniel Kroening, Christoph Wintersteiger\n" <<
@@ -354,7 +363,7 @@ int gcc_modet::doit()
   if(cmdline.isset("dumpversion"))
   {
     if(produce_hybrid_binary)
-      return run_gcc();
+      return run_gcc(compiler);
 
     std::cout << "3.4.4\n";
     return EX_OK;
@@ -390,6 +399,24 @@ int gcc_modet::doit()
       debug() << "GCC mode" << eom;
   }
 
+  // determine actions to be undertaken
+  if(act_as_ld)
+    compiler.mode=compilet::LINK_LIBRARY;
+  else if(cmdline.isset('S'))
+    compiler.mode=compilet::ASSEMBLE_ONLY;
+  else if(cmdline.isset('c'))
+    compiler.mode=compilet::COMPILE_ONLY;
+  else if(cmdline.isset('E'))
+  {
+    compiler.mode=compilet::PREPROCESS_ONLY;
+    UNREACHABLE;
+  }
+  else if(cmdline.isset("shared") ||
+          cmdline.isset('r')) // really not well documented
+    compiler.mode=compilet::COMPILE_LINK;
+  else
+    compiler.mode=compilet::COMPILE_LINK_EXECUTABLE;
+
   // In gcc mode, we have just pass on to gcc to handle the following:
   // * if -M or -MM is given, we do dependencies only
   // * preprocessing (-E)
@@ -402,7 +429,7 @@ int gcc_modet::doit()
           cmdline.isset("MM") ||
           cmdline.isset('E') ||
           !cmdline.have_infile_arg())
-    return run_gcc(); // exit!
+    return run_gcc(compiler); // exit!
 
   // get configuration
   config.set(cmdline);
@@ -489,30 +516,6 @@ int gcc_modet::doit()
   if(cmdline.isset("fshort-double"))
     config.ansi_c.double_width=config.ansi_c.single_width;
 
-  // determine actions to be undertaken
-  compilet compiler(cmdline,
-                    gcc_message_handler,
-                    cmdline.isset("Werror") &&
-                    cmdline.isset("Wextra") &&
-                    !cmdline.isset("Wno-error"));
-
-  if(act_as_ld)
-    compiler.mode=compilet::LINK_LIBRARY;
-  else if(cmdline.isset('S'))
-    compiler.mode=compilet::ASSEMBLE_ONLY;
-  else if(cmdline.isset('c'))
-    compiler.mode=compilet::COMPILE_ONLY;
-  else if(cmdline.isset('E'))
-  {
-    compiler.mode=compilet::PREPROCESS_ONLY;
-    UNREACHABLE;
-  }
-  else if(cmdline.isset("shared") ||
-          cmdline.isset('r')) // really not well documented
-    compiler.mode=compilet::COMPILE_LINK;
-  else
-    compiler.mode=compilet::COMPILE_LINK_EXECUTABLE;
-
   switch(compiler.mode)
   {
   case compilet::LINK_LIBRARY:
@@ -695,10 +698,10 @@ int gcc_modet::doit()
 
   if(compiler.source_files.empty() &&
      compiler.object_files.empty())
-    return run_gcc(); // exit!
+    return run_gcc(compiler); // exit!
 
   if(compiler.mode==compilet::ASSEMBLE_ONLY)
-    return asm_output(act_as_bcc, compiler.source_files);
+    return asm_output(act_as_bcc, compiler.source_files, compiler);
 
   // do all the rest
   if(compiler.doit())
@@ -707,7 +710,7 @@ int gcc_modet::doit()
   // We can generate hybrid ELF and Mach-O binaries
   // containing both executable machine code and the goto-binary.
   if(produce_hybrid_binary && !act_as_bcc)
-    return gcc_hybrid_binary();
+    return gcc_hybrid_binary(compiler);
 
   return EX_OK;
 }
@@ -791,8 +794,7 @@ int gcc_modet::preprocess(
   return run(new_argv[0], new_argv, cmdline.stdin_file, stdout_file);
 }
 
-/// run gcc or clang with original command line
-int gcc_modet::run_gcc()
+int gcc_modet::run_gcc(const compilet &compiler)
 {
   PRECONDITION(!cmdline.parsed_argv.empty());
 
@@ -802,6 +804,28 @@ int gcc_modet::run_gcc()
   for(const auto &a : cmdline.parsed_argv)
     new_argv.push_back(a.arg);
 
+  if(compiler.wrote_object_files())
+  {
+    // Undefine all __CPROVER macros for the system compiler
+    std::map<irep_idt, std::size_t> arities;
+    compiler.cprover_macro_arities(arities);
+    for(const auto &pair : arities)
+    {
+      std::ostringstream addition;
+      addition << "-D" << id2string(pair.first) << "(";
+      std::vector<char> params(pair.second);
+      std::iota(params.begin(), params.end(), 'a');
+      for(std::vector<char>::iterator it=params.begin(); it!=params.end(); ++it)
+      {
+        addition << *it;
+        if(it+1!=params.end())
+          addition << ",";
+      }
+      addition << ")= ";
+      new_argv.push_back(addition.str());
+    }
+  }
+
   // overwrite argv[0]
   new_argv[0]=native_tool_name;
 
@@ -813,7 +837,7 @@ int gcc_modet::run_gcc()
   return run(new_argv[0], new_argv, cmdline.stdin_file, "");
 }
 
-int gcc_modet::gcc_hybrid_binary()
+int gcc_modet::gcc_hybrid_binary(const compilet &compiler)
 {
   {
     bool have_files=false;
@@ -861,7 +885,7 @@ int gcc_modet::gcc_hybrid_binary()
   if(output_files.empty() ||
      (output_files.size()==1 &&
       output_files.front()=="/dev/null"))
-    return run_gcc();
+    return EX_OK;
 
   debug() << "Running " << native_tool_name
           << " to generate hybrid binary" << eom;
@@ -893,7 +917,7 @@ int gcc_modet::gcc_hybrid_binary()
   }
   objcopy_cmd+="objcopy";
 
-  int result=run_gcc();
+  int result=run_gcc(compiler);
 
   // merge output from gcc with goto-binaries
   // using objcopy, or do cleanup if an earlier call failed
@@ -975,7 +999,8 @@ int gcc_modet::gcc_hybrid_binary()
 
 int gcc_modet::asm_output(
   bool act_as_bcc,
-  const std::list<std::string> &preprocessed_source_files)
+  const std::list<std::string> &preprocessed_source_files,
+  const compilet &compiler)
 {
   {
     bool have_files=false;
@@ -996,7 +1021,7 @@ int gcc_modet::asm_output(
     debug() << "Running " << native_tool_name
       << " to generate native asm output" << eom;
 
-    int result=run_gcc();
+    int result=run_gcc(compiler);
     if(result!=0)
       // native tool failed
       return result;