remove_asm.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Remove 'asm' statements by compiling them into suitable
        standard goto program instructions
 
Author: Daniel Kroening
 
Date:   December 2014
 
\*******************************************************************/
 
 
#include "remove_asm.h"
 
#include <util/c_types.h>
#include <util/pointer_expr.h>
#include <util/prefix.h>
#include <util/range.h>
#include <util/std_code.h>
#include <util/string_constant.h>
 
#include <goto-programs/goto_model.h>
#include <goto-programs/remove_skip.h>
 
#include "assembler_parser.h"
 
class remove_asmt
{
public:
  remove_asmt(
    symbol_tablet &_symbol_table,
    goto_functionst &_goto_functions,
    message_handlert &message_handler)
    : symbol_table(_symbol_table),
      goto_functions(_goto_functions),
      message_handler(message_handler)
  {
  }
  remove_asmt( {…}
 
  void operator()()
  {
    for(auto &f : goto_functions.function_map)
      process_function(f.first, f.second);
  }
  void operator()() {…}
 
protected:
  symbol_tablet &symbol_table;
  goto_functionst &goto_functions;
  message_handlert &message_handler;
 
  void process_function(const irep_idt &, goto_functionst::goto_functiont &);
 
  void process_instruction(
    const irep_idt &function_id,
    goto_programt::instructiont &instruction,
    goto_programt &dest);
 
  void process_instruction_gcc(const code_asm_gcct &, goto_programt &dest);
 
  void process_instruction_msc(
    const irep_idt &,
    const code_asmt &,
    goto_programt &dest);
 
  void gcc_asm_function_call(
    const irep_idt &function_base_name,
    const code_asm_gcct &code,
    std::size_t n_args,
    goto_programt &dest);
 
  void msc_asm_function_call(
    const irep_idt &function_base_name,
    const exprt::operandst &operands,
    const code_asmt &code,
    goto_programt &dest);
};
class remove_asmt {…};
 
void remove_asmt::gcc_asm_function_call(
  const irep_idt &function_base_name,
  const code_asm_gcct &code,
  std::size_t n_args,
  goto_programt &dest)
{
  irep_idt function_identifier = function_base_name;
 
  code_function_callt::argumentst arguments;
 
  const typet void_pointer = pointer_type(empty_typet());
 
  // outputs
  forall_operands(it, code.outputs())
  {
    if(it->operands().size() == 2)
    {
      arguments.push_back(typecast_exprt(
        address_of_exprt(to_binary_expr(*it).op1()), void_pointer));
    }
  }
 
  // inputs
  forall_operands(it, code.inputs())
  {
    if(it->operands().size() == 2)
    {
      arguments.push_back(typecast_exprt(
        address_of_exprt(to_binary_expr(*it).op1()), void_pointer));
    }
  }
 
  // An inline asm statement may consist of multiple commands, not all of which
  // use all of the inputs/outputs of the inline asm statement.
  DATA_INVARIANT_WITH_DIAGNOSTICS(
    arguments.size() >= n_args,
    "insufficient number of arguments for calling " +
      id2string(function_identifier),
    "required arguments: " + std::to_string(n_args),
    code.pretty());
  arguments.resize(n_args);
 
  code_typet fkt_type{
    code_typet::parameterst{
      arguments.size(), code_typet::parametert{void_pointer}},
    empty_typet()};
 
  auto fkt = symbol_exprt{function_identifier, fkt_type}.with_source_location(
    code.source_location());
 
  code_function_callt function_call(std::move(fkt), std::move(arguments));
 
  dest.add(
    goto_programt::make_function_call(function_call, code.source_location()));
 
  // do we have it?
  if(!symbol_table.has_symbol(function_identifier))
  {
    symbolt symbol{function_identifier, fkt_type, ID_C};
    symbol.base_name = function_base_name;
 
    symbol_table.add(symbol);
 
    goto_functions.function_map.emplace(function_identifier, goto_functiont());
  }
  else
  {
    DATA_INVARIANT_WITH_DIAGNOSTICS(
      symbol_table.lookup_ref(function_identifier).type == fkt_type,
      "types of function " + id2string(function_identifier) + " should match",
      code.pretty(),
      symbol_table.lookup_ref(function_identifier).type.pretty(),
      fkt_type.pretty());
  }
}
void remove_asmt::gcc_asm_function_call( {…}
 
void remove_asmt::msc_asm_function_call(
  const irep_idt &function_base_name,
  const exprt::operandst &operands,
  const code_asmt &code,
  goto_programt &dest)
{
  irep_idt function_identifier = function_base_name;
 
  code_function_callt::argumentst arguments;
 
  const typet void_pointer = pointer_type(empty_typet());
 
  for(const auto &op : operands)
    arguments.push_back(typecast_exprt::conditional_cast(op, void_pointer));
 
  code_typet fkt_type{
    code_typet::parameterst{
      arguments.size(), code_typet::parametert{void_pointer}},
    empty_typet()};
 
  auto fkt = symbol_exprt{function_identifier, fkt_type}.with_source_location(
    code.source_location());
  code_function_callt function_call(std::move(fkt), std::move(arguments));
 
  dest.add(
    goto_programt::make_function_call(function_call, code.source_location()));
 
  // do we have it?
  if(!symbol_table.has_symbol(function_identifier))
  {
    symbolt symbol{function_identifier, fkt_type, ID_C};
    symbol.base_name = function_base_name;
 
    symbol_table.add(symbol);
 
    goto_functions.function_map.emplace(function_identifier, goto_functiont());
  }
  else
  {
    DATA_INVARIANT(
      symbol_table.lookup_ref(function_identifier).type == fkt_type,
      "function types should match");
  }
}
void remove_asmt::msc_asm_function_call( {…}
 
void remove_asmt::process_instruction(
  const irep_idt &function_id,
  goto_programt::instructiont &instruction,
  goto_programt &dest)
{
  const code_asmt &code = to_code_asm(instruction.get_other());
 
  const irep_idt &flavor = code.get_flavor();
 
  if(flavor == ID_gcc)
    process_instruction_gcc(to_code_asm_gcc(code), dest);
  else if(flavor == ID_msc)
    process_instruction_msc(function_id, code, dest);
  else
    DATA_INVARIANT(false, "unexpected assembler flavor");
}
void remove_asmt::process_instruction( {…}
 
void remove_asmt::process_instruction_gcc(
  const code_asm_gcct &code,
  goto_programt &dest)
{
  const irep_idt &i_str = to_string_constant(code.asm_text()).value();
 
  std::istringstream str(id2string(i_str));
  assembler_parsert assembler_parser{message_handler};
  assembler_parser.in = &str;
  assembler_parser.parse();
 
  goto_programt tmp_dest;
  bool unknown = false;
  bool x86_32_locked_atomic = false;
 
  for(const auto &instruction : assembler_parser.instructions)
  {
    if(instruction.empty())
      continue;
 
#if 0
    std::cout << "A ********************\n";
    for(const auto &ins : instruction)
    {
      std::cout << "XX: " << ins.pretty() << '\n';
    }
 
    std::cout << "B ********************\n";
#endif
 
    // deal with prefixes
    irep_idt command;
    unsigned pos = 0;
 
    if(
      instruction.front().id() == ID_symbol &&
      instruction.front().get(ID_identifier) == "lock")
    {
      x86_32_locked_atomic = true;
      pos++;
    }
 
    // done?
    if(pos == instruction.size())
      continue;
 
    if(instruction[pos].id() == ID_symbol)
    {
      command = instruction[pos].get(ID_identifier);
      pos++;
    }
 
    if(command == "xchg" || command == "xchgl")
      x86_32_locked_atomic = true;
 
    if(x86_32_locked_atomic)
    {
      tmp_dest.add(goto_programt::make_atomic_begin(code.source_location()));
 
      codet code_fence(ID_fence);
      code_fence.add_source_location() = code.source_location();
      code_fence.set(ID_WWfence, true);
      code_fence.set(ID_RRfence, true);
      code_fence.set(ID_RWfence, true);
      code_fence.set(ID_WRfence, true);
 
      tmp_dest.add(
        goto_programt::make_other(code_fence, code.source_location()));
    }
 
    if(command == "fstcw" || command == "fnstcw" || command == "fldcw") // x86
    {
      gcc_asm_function_call("__asm_" + id2string(command), code, 1, tmp_dest);
    }
    else if(
      command == "mfence" || command == "lfence" || command == "sfence") // x86
    {
      gcc_asm_function_call("__asm_" + id2string(command), code, 0, tmp_dest);
    }
    else if(command == ID_sync) // Power
    {
      codet code_fence(ID_fence);
      code_fence.add_source_location() = code.source_location();
      code_fence.set(ID_WWfence, true);
      code_fence.set(ID_RRfence, true);
      code_fence.set(ID_RWfence, true);
      code_fence.set(ID_WRfence, true);
      code_fence.set(ID_WWcumul, true);
      code_fence.set(ID_RWcumul, true);
      code_fence.set(ID_RRcumul, true);
      code_fence.set(ID_WRcumul, true);
 
      tmp_dest.add(
        goto_programt::make_other(code_fence, code.source_location()));
    }
    else if(command == ID_lwsync) // Power
    {
      codet code_fence(ID_fence);
      code_fence.add_source_location() = code.source_location();
      code_fence.set(ID_WWfence, true);
      code_fence.set(ID_RRfence, true);
      code_fence.set(ID_RWfence, true);
      code_fence.set(ID_WWcumul, true);
      code_fence.set(ID_RWcumul, true);
      code_fence.set(ID_RRcumul, true);
 
      tmp_dest.add(
        goto_programt::make_other(code_fence, code.source_location()));
    }
    else if(command == ID_isync) // Power
    {
      codet code_fence(ID_fence);
      code_fence.add_source_location() = code.source_location();
 
      tmp_dest.add(
        goto_programt::make_other(code_fence, code.source_location()));
      // doesn't do anything by itself,
      // needs to be combined with branch
    }
    else if(command == "dmb" || command == "dsb") // ARM
    {
      codet code_fence(ID_fence);
      code_fence.add_source_location() = code.source_location();
      code_fence.set(ID_WWfence, true);
      code_fence.set(ID_RRfence, true);
      code_fence.set(ID_RWfence, true);
      code_fence.set(ID_WRfence, true);
      code_fence.set(ID_WWcumul, true);
      code_fence.set(ID_RWcumul, true);
      code_fence.set(ID_RRcumul, true);
      code_fence.set(ID_WRcumul, true);
 
      tmp_dest.add(
        goto_programt::make_other(code_fence, code.source_location()));
    }
    else if(command == "isb") // ARM
    {
      codet code_fence(ID_fence);
      code_fence.add_source_location() = code.source_location();
 
      tmp_dest.add(
        goto_programt::make_other(code_fence, code.source_location()));
      // doesn't do anything by itself,
      // needs to be combined with branch
    }
    else
      unknown = true; // give up
 
    if(x86_32_locked_atomic)
    {
      tmp_dest.add(goto_programt::make_atomic_end(code.source_location()));
 
      x86_32_locked_atomic = false;
    }
  }
 
  if(unknown)
  {
    // we give up; we should perhaps print a warning
  }
  else
    dest.destructive_append(tmp_dest);
}
void remove_asmt::process_instruction_gcc( {…}
 
void remove_asmt::process_instruction_msc(
  const irep_idt &function_id,
  const code_asmt &code,
  goto_programt &dest)
{
  const irep_idt &i_str = to_string_constant(code.op0()).value();
 
  std::istringstream str(id2string(i_str));
  assembler_parsert assembler_parser{message_handler};
  assembler_parser.in = &str;
  assembler_parser.parse();
 
  goto_programt tmp_dest;
  bool unknown = false;
  bool x86_32_locked_atomic = false;
 
  for(const auto &instruction : assembler_parser.instructions)
  {
    if(instruction.empty())
      continue;
 
#if 0
    std::cout << "A ********************\n";
    for(const auto &ins : instruction)
    {
      std::cout << "XX: " << ins.pretty() << '\n';
    }
 
    std::cout << "B ********************\n";
#endif
 
    // deal with prefixes
    irep_idt command;
    unsigned pos = 0;
 
    if(
      instruction.front().id() == ID_symbol &&
      instruction.front().get(ID_identifier) == "lock")
    {
      x86_32_locked_atomic = true;
      pos++;
    }
 
    // done?
    if(pos == instruction.size())
      continue;
 
    if(instruction[pos].id() == ID_symbol)
    {
      command = instruction[pos].get(ID_identifier);
      pos++;
    }
 
    if(command == "xchg" || command == "xchgl")
      x86_32_locked_atomic = true;
 
    if(x86_32_locked_atomic)
    {
      tmp_dest.add(goto_programt::make_atomic_begin(code.source_location()));
 
      codet code_fence(ID_fence);
      code_fence.add_source_location() = code.source_location();
      code_fence.set(ID_WWfence, true);
      code_fence.set(ID_RRfence, true);
      code_fence.set(ID_RWfence, true);
      code_fence.set(ID_WRfence, true);
 
      tmp_dest.add(
        goto_programt::make_other(code_fence, code.source_location()));
    }
 
    if(command == "fstcw" || command == "fnstcw" || command == "fldcw") // x86
    {
      exprt::operandst args{null_pointer_exprt{pointer_type(empty_typet{})}};
      // try to typecheck the argument
      if(pos != instruction.size() && instruction[pos].id() == ID_symbol)
      {
        const irep_idt &name = instruction[pos].get(ID_identifier);
        for(const auto &entry : equal_range(symbol_table.symbol_base_map, name))
        {
          // global scope symbol, don't replace a local one
          if(entry.second == name && args[0].id() != ID_address_of)
          {
            args[0] =
              address_of_exprt{symbol_table.lookup_ref(name).symbol_expr()};
          }
          // parameter or symbol in local scope
          else if(has_prefix(
                    id2string(entry.second), id2string(function_id) + "::"))
          {
            args[0] = address_of_exprt{
              symbol_table.lookup_ref(entry.second).symbol_expr()};
          }
        }
      }
      msc_asm_function_call(
        "__asm_" + id2string(command), args, code, tmp_dest);
    }
    else if(
      command == "mfence" || command == "lfence" || command == "sfence") // x86
    {
      msc_asm_function_call("__asm_" + id2string(command), {}, code, tmp_dest);
    }
    else
      unknown = true; // give up
 
    if(x86_32_locked_atomic)
    {
      tmp_dest.add(goto_programt::make_atomic_end(code.source_location()));
 
      x86_32_locked_atomic = false;
    }
  }
 
  if(unknown)
  {
    // we give up; we should perhaps print a warning
  }
  else
    dest.destructive_append(tmp_dest);
}
void remove_asmt::process_instruction_msc( {…}
 
void remove_asmt::process_function(
  const irep_idt &function_id,
  goto_functionst::goto_functiont &goto_function)
{
  bool did_something = false;
 
  Forall_goto_program_instructions(it, goto_function.body)
  {
    if(it->is_other() && it->get_other().get_statement() == ID_asm)
    {
      goto_programt tmp_dest;
      process_instruction(function_id, *it, tmp_dest);
      it->turn_into_skip();
      did_something = true;
 
      goto_programt::targett next = it;
      next++;
 
      goto_function.body.destructive_insert(next, tmp_dest);
    }
  }
 
  if(did_something)
    remove_skip(goto_function.body);
}
void remove_asmt::process_function( {…}
 
void remove_asm(
  goto_functionst &goto_functions,
  symbol_tablet &symbol_table,
  message_handlert &message_handler)
{
  remove_asmt rem(symbol_table, goto_functions, message_handler);
  rem();
}
void remove_asm( {…}
 
void remove_asm(goto_modelt &goto_model, message_handlert &message_handler)
{
  remove_asm(
    goto_model.goto_functions, goto_model.symbol_table, message_handler);
}
void remove_asm(goto_modelt &goto_model, message_handlert &message_handler) {…}
 
bool has_asm(const goto_functionst &goto_functions)
{
  for(auto &function_it : goto_functions.function_map)
    for(auto &instruction : function_it.second.body.instructions)
      if(
        instruction.is_other() &&
        instruction.get_other().get_statement() == ID_asm)
      {
        return true;
      }
 
  return false;
}
bool has_asm(const goto_functionst &goto_functions) {…}
 
bool has_asm(const goto_modelt &goto_model)
{
  return has_asm(goto_model.goto_functions);
}
bool has_asm(const goto_modelt &goto_model) {…}