[depends: #1357] goto-gcc removes CPROVER macros for native gcc

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

@@ -3,16 +3,22 @@ DIRS = ansi-c \
        cpp \
        cbmc-java \
        goto-analyzer \
+       goto-diff \
+       goto-gcc \
        goto-instrument \
        goto-instrument-typedef \
-       goto-diff \
        invariants \
        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();
     }
@@ -617,6 +620,7 @@ bool compilet::write_bin_object_file(
                << "; " << cnt << " have a body." << eom;
 
   outfile.close();
+  wrote_object=true;
 
   return false;
 }
@@ -651,6 +655,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();
 }
 
@@ -725,3 +730,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