Merge pull request diffblue#1888 from tautschnig/linker-script-fixes

Linker-script processing fixes

Author: Daniel Kroening

src/goto-cc/compile.cpp

@@ -346,11 +346,8 @@ bool compilet::link()
   convert_symbols(compiled_functions);
 
   // parse object files
-  while(!object_files.empty())
+  for(const auto &file_name : object_files)
   {
-    std::string file_name=object_files.front();
-    object_files.pop_front();
-
     if(read_object_and_link(file_name, symbol_table,
                             compiled_functions, get_message_handler()))
       return true;

src/goto-cc/dist-linux

@@ -14,9 +14,10 @@ mkdir /tmp/goto-cc-dist
 cp goto-cc /tmp/goto-cc-dist/
 cp ../goto-instrument/goto-instrument /tmp/goto-cc-dist/
 cp ../../LICENSE /tmp/goto-cc-dist/
+cp ../../scripts/ls_parse.py /tmp/goto-cc-dist/
 cd /tmp/goto-cc-dist
 tar cfz goto-cc-${VERSION_FILE}-linux.tgz goto-cc \
-  goto-instrument LICENSE
+  goto-instrument LICENSE ls_parse.py
 
 echo Copying.
 scp goto-cc-${VERSION_FILE}-linux.tgz [email protected]:/home/www/cprover.org/goto-cc/download/

src/goto-cc/gcc_mode.cpp

@@ -813,7 +813,7 @@ int gcc_modet::run_gcc(const compilet &compiler)
   for(const auto &a : cmdline.parsed_argv)
     new_argv.push_back(a.arg);
 
-  if(compiler.wrote_object_files())
+  if(!act_as_ld && compiler.wrote_object_files())
   {
     // Undefine all __CPROVER macros for the system compiler
     std::map<irep_idt, std::size_t> arities;
@@ -935,12 +935,7 @@ int gcc_modet::gcc_hybrid_binary(compilet &compiler)
   {
     linker_script_merget ls_merge(
         compiler, output_files, goto_binaries, cmdline, gcc_message_handler);
-    const int fail=ls_merge.add_linker_script_definitions();
-    if(fail!=0)
-    {
-      error() << "Unable to merge linker script symbols" << eom;
-      return fail;
-    }
+    result=ls_merge.add_linker_script_definitions();
   }
 
   // merge output from gcc with goto-binaries

src/goto-cc/linker_script_merge.cpp

@@ -38,12 +38,25 @@ int linker_script_merget::add_linker_script_definitions()
   const std::string &elf_file=*elf_binaries.begin();
   const std::string &goto_file=*goto_binaries.begin();
 
-  jsont data;
+  temporary_filet linker_def_outfile("goto-cc-linker-info", ".json");
   std::list<irep_idt> linker_defined_symbols;
-  int fail=get_linker_script_data(
-      data, linker_defined_symbols, compiler.symbol_table, elf_file);
+  int fail=
+    get_linker_script_data(
+      linker_defined_symbols,
+      compiler.symbol_table,
+      elf_file,
+      linker_def_outfile());
+  // ignore linker script parsing failures until the code is tested more widely
+  if(fail!=0)
+    return 0;
+
+  jsont data;
+  fail=parse_json(linker_def_outfile(), get_message_handler(), data);
   if(fail!=0)
+  {
+    error() << "Problem parsing linker script JSON data" << eom;
     return fail;
+  }
 
   fail=linker_data_is_malformed(data);
   if(fail!=0)
@@ -117,8 +130,9 @@ linker_script_merget::linker_script_merget(
     replacement_predicates(
     {
       replacement_predicatet("address of array's first member",
-        [](const exprt expr){ return to_symbol_expr(expr.op0().op0()); },
-        [](const exprt expr)
+        [](const exprt &expr) -> const symbol_exprt&
+        { return to_symbol_expr(expr.op0().op0()); },
+        [](const exprt &expr, const namespacet &ns)
         {
           return expr.id()==ID_address_of &&
                  expr.type().id()==ID_pointer &&
@@ -133,25 +147,39 @@ linker_script_merget::linker_script_merget(
                  expr.op0().op1().type().id()==ID_signedbv;
         }),
       replacement_predicatet("address of array",
-        [](const exprt expr){ return to_symbol_expr(expr.op0()); },
-        [](const exprt expr)
+        [](const exprt &expr) -> const symbol_exprt&
+        { return to_symbol_expr(expr.op0()); },
+        [](const exprt &expr, const namespacet &ns)
         {
           return expr.id()==ID_address_of &&
                  expr.type().id()==ID_pointer &&
 
                  expr.op0().id()==ID_symbol &&
                  expr.op0().type().id()==ID_array;
         }),
+      replacement_predicatet("address of struct",
+        [](const exprt &expr) -> const symbol_exprt&
+        { return to_symbol_expr(expr.op0()); },
+        [](const exprt &expr, const namespacet &ns)
+        {
+          return expr.id()==ID_address_of &&
+                 expr.type().id()==ID_pointer &&
+
+                 expr.op0().id()==ID_symbol &&
+                 ns.follow(expr.op0().type()).id()==ID_struct;
+        }),
       replacement_predicatet("array variable",
-        [](const exprt expr){ return to_symbol_expr(expr); },
-        [](const exprt expr)
+        [](const exprt &expr) -> const symbol_exprt&
+        { return to_symbol_expr(expr); },
+        [](const exprt &expr, const namespacet &ns)
         {
           return expr.id()==ID_symbol &&
                  expr.type().id()==ID_array;
         }),
       replacement_predicatet("pointer (does not need pointerizing)",
-        [](const exprt expr){ return to_symbol_expr(expr); },
-        [](const exprt expr)
+        [](const exprt &expr) -> const symbol_exprt&
+        { return to_symbol_expr(expr); },
+        [](const exprt &expr, const namespacet &ns)
         {
           return expr.id()==ID_symbol &&
                  expr.type().id()==ID_pointer;
@@ -164,6 +192,8 @@ int linker_script_merget::pointerize_linker_defined_symbols(
       symbol_tablet &symbol_table,
       const linker_valuest &linker_values)
 {
+  const namespacet ns(symbol_table);
+
   int ret=0;
   // First, pointerize the actual linker-defined symbols
   for(const auto &pair : linker_values)
@@ -191,7 +221,8 @@ int linker_script_merget::pointerize_linker_defined_symbols(
     int fail=pointerize_subexprs_of(
       symbol_table.get_writeable_ref(pair.first).value,
       to_pointerize,
-      linker_values);
+      linker_values,
+      ns);
     if(to_pointerize.empty() && fail==0)
       continue;
     ret=1;
@@ -216,7 +247,8 @@ int linker_script_merget::pointerize_linker_defined_symbols(
         if(to_pointerize.empty())
           continue;
         debug() << "Pointerizing a program expression..." << eom;
-        int fail=pointerize_subexprs_of(*insts, to_pointerize, linker_values);
+        int fail = pointerize_subexprs_of(
+          *insts, to_pointerize, linker_values, ns);
         if(to_pointerize.empty() && fail==0)
           continue;
         ret=1;
@@ -259,15 +291,17 @@ int linker_script_merget::replace_expr(
 int linker_script_merget::pointerize_subexprs_of(
     exprt &expr,
     std::list<symbol_exprt> &to_pointerize,
-    const linker_valuest &linker_values)
+    const linker_valuest &linker_values,
+    const namespacet &ns)
 {
   int fail=0, tmp=0;
   for(auto const &pair : linker_values)
     for(auto const &pattern : replacement_predicates)
     {
-      if(!pattern.match(expr))
+      if(!pattern.match(expr, ns))
         continue;
-      const symbol_exprt &inner_symbol=pattern.inner_symbol(expr);
+      // take a copy, expr will be changed below
+      const symbol_exprt inner_symbol=pattern.inner_symbol(expr);
       if(pair.first!=inner_symbol.get_identifier())
         continue;
       tmp=replace_expr(expr, linker_values, inner_symbol, pair.first,
@@ -292,7 +326,7 @@ int linker_script_merget::pointerize_subexprs_of(
 
   for(auto &op : expr.operands())
   {
-    tmp=pointerize_subexprs_of(op, to_pointerize, linker_values);
+    tmp=pointerize_subexprs_of(op, to_pointerize, linker_values, ns);
     fail=tmp?tmp:fail;
   }
   return fail;
@@ -625,23 +659,24 @@ int linker_script_merget::ls_data2instructions(
 #endif
 
 int linker_script_merget::get_linker_script_data(
-    jsont &linker_data,
     std::list<irep_idt> &linker_defined_symbols,
     const symbol_tablet &symbol_table,
-    const std::string &out_file)
+    const std::string &out_file,
+    const std::string &def_out_file)
 {
   for(auto const &pair : symbol_table.symbols)
-    if(pair.second.is_extern && pair.second.value.is_nil()
-    && pair.second.name!="__CPROVER_memory")
+    if(pair.second.is_extern && pair.second.value.is_nil() &&
+       pair.second.name!="__CPROVER_memory")
       linker_defined_symbols.push_back(pair.second.name);
 
   std::ostringstream linker_def_str;
-  std::copy(linker_defined_symbols.begin(), linker_defined_symbols.end(),
-      std::ostream_iterator<irep_idt>(linker_def_str, "\n"));
+  std::copy(
+    linker_defined_symbols.begin(),
+    linker_defined_symbols.end(),
+    std::ostream_iterator<irep_idt>(linker_def_str, "\n"));
   debug() << "Linker-defined symbols: [" << linker_def_str.str() << "]\n"
           << eom;
 
-  temporary_filet linker_def_outfile("goto-cc-linker-info", ".json");
   temporary_filet linker_def_infile("goto-cc-linker-defs", "");
   std::ofstream linker_def_file(linker_def_infile());
   linker_def_file << linker_def_str.str();
@@ -653,29 +688,24 @@ int linker_script_merget::get_linker_script_data(
     "--script",   cmdline.get_value('T'),
     "--object",   out_file,
     "--sym-file", linker_def_infile(),
-    "--out-file", linker_def_outfile()
+    "--out-file", def_out_file
   };
-  if(cmdline.isset("verbosity"))
-  {
-    unsigned verb=safe_string2unsigned(cmdline.get_value("verbosity"));
-    if(verb>9)
-      argv.push_back("--very-verbose");
-    else if(verb>4)
-      argv.push_back("--verbose");
-  }
 
-  int rc=run(argv[0], argv, linker_def_infile(), linker_def_outfile());
+  if(get_message_handler().get_verbosity()>9)
+    argv.push_back("--very-verbose");
+  else if(get_message_handler().get_verbosity()>4)
+    argv.push_back("--verbose");
+
+  debug() << "RUN:";
+  for(std::size_t i=0; i<argv.size(); i++)
+    debug() << " " << argv[i];
+  debug() << eom;
+
+  int rc=run(argv[0], argv, linker_def_infile(), def_out_file);
   if(rc!=0)
-  {
-    error() << "Problem parsing linker script" << eom;
-    return rc;
-  }
+    warning() << "Problem parsing linker script" << eom;
 
-  int fail=parse_json(linker_def_outfile(), get_message_handler(),
-      linker_data);
-  if(fail!=0)
-    error() << "Problem parsing linker script JSON data" << eom;
-  return fail;
+  return rc;
 }
 
 int linker_script_merget::goto_and_object_mismatch(

src/goto-cc/linker_script_merge.h

@@ -26,7 +26,7 @@ class replacement_predicatet
   replacement_predicatet(
       const std::string &description,
       const std::function<const symbol_exprt&(const exprt&)> inner_symbol,
-      const std::function<bool(const exprt&)> match)
+      const std::function<bool(const exprt&, const namespacet&)> match)
     : _description(description),
       _inner_symbol(inner_symbol),
       _match(match)
@@ -50,15 +50,15 @@ class replacement_predicatet
   /// If this function returns true, the entire expression should be replaced by
   /// a pointer whose underlying symbol is the symbol returned by
   /// replacement_predicatet::inner_symbol().
-  const bool match(const exprt &expr) const
+  const bool match(const exprt &expr, const namespacet &ns) const
   {
-    return _match(expr);
+    return _match(expr, ns);
   };
 
 private:
   std::string _description;
   std::function<const symbol_exprt&(const exprt&)> _inner_symbol;
-  std::function<bool(const exprt&)> _match;
+  std::function<bool(const exprt&, const namespacet&)> _match;
 };
 
 /// \brief Synthesise definitions of symbols that are defined in linker scripts
@@ -105,10 +105,10 @@ class linker_script_merget:public messaget
 
   /// \brief Write linker script definitions to `linker_data`.
   int get_linker_script_data(
-      jsont &linker_data,
       std::list<irep_idt> &linker_defined_symbols,
       const symbol_tablet &symbol_table,
-      const std::string &out_file);
+      const std::string &out_file,
+      const std::string &def_out_file);
 
   /// \brief Write a list of definitions derived from `data` into gp's
   ///        `instructions` member.
@@ -165,6 +165,7 @@ class linker_script_merget:public messaget
   /// \param to_pointerize  The symbols that are contained in the subexpressions
   ///                       that we will pointerize.
   /// \param linker_values the names of symbols defined in linker scripts.
+  /// \param ns a namespace to look up types.
   ///
   /// The subexpressions that we pointerize should be in one-to-one
   /// correspondence with the symbols in `to_pointerize`. Every time we
@@ -175,7 +176,8 @@ class linker_script_merget:public messaget
   int pointerize_subexprs_of(
       exprt &expr,
       std::list<symbol_exprt> &to_pointerize,
-      const linker_valuest &linker_values);
+      const linker_valuest &linker_values,
+      const namespacet &ns);
 
   /// \brief do the actual replacement of an expr with a new pointer expr
   int replace_expr(