memory_snapshot_harness_generator.h

Go to the documentation of this file.

/******************************************************************\
 
Module: Harness to initialise memory from memory snapshot
 
Author: Daniel Poetzl
 
\******************************************************************/
 
#ifndef CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_H
#define CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_H
 
#include <list>
#include <string>
 
#include "goto_harness_generator.h"
#include "recursive_initialization.h"
 
#include <goto-programs/goto_model.h>
 
#include <util/message.h>
#include <util/optional.h>
 
class memory_snapshot_harness_generatort : public goto_harness_generatort
{
public:
  explicit memory_snapshot_harness_generatort(message_handlert &message_handler)
    : message_handler(message_handler)
  {
  }
 
  void generate(goto_modelt &goto_model, const irep_idt &harness_function_name)
    override;
 
protected:
  struct entry_goto_locationt
  {
    irep_idt function_name;
    optionalt<unsigned> location_number;
 
    entry_goto_locationt() = delete;
    explicit entry_goto_locationt(irep_idt function_name)
      : function_name(function_name)
    {
    }
    explicit entry_goto_locationt(
      irep_idt function_name,
      unsigned location_number)
      : function_name(function_name), location_number(location_number)
    {
    }
 
    goto_programt::const_targett find_first_corresponding_instruction(
      const goto_programt::instructionst &instructions) const;
  };
 
  entry_goto_locationt parse_goto_location(const std::string &cmdl_option);
 
  struct entry_source_locationt
  {
    irep_idt file_name;
    unsigned line_number;
 
    entry_source_locationt() = delete;
    explicit entry_source_locationt(irep_idt file_name, unsigned line_number)
      : file_name(file_name), line_number(line_number)
    {
    }
 
    std::pair<goto_programt::const_targett, size_t>
    find_first_corresponding_instruction(
      const goto_programt::instructionst &instructions) const;
  };
 
  entry_source_locationt parse_source_location(const std::string &cmdl_option);
 
  struct entry_locationt
  {
    irep_idt function_name;
    goto_programt::const_targett start_instruction;
 
    entry_locationt() = default;
    explicit entry_locationt(
      irep_idt function_name,
      goto_programt::const_targett start_instruction)
      : function_name(function_name), start_instruction(start_instruction)
    {
    }
  };
 
  struct source_location_matcht
  {
    size_t distance;
    irep_idt function_name;
    goto_programt::const_targett instruction;
    bool match_found;
 
    source_location_matcht() : distance(0), match_found(false)
    {
    }
 
    void match_up(
      const size_t &candidate_distance,
      const irep_idt &candidate_function_name,
      const goto_programt::const_targett &candidate_instruction)
    {
      if(match_found && distance <= candidate_distance)
        return;
 
      match_found = true;
      distance = candidate_distance;
      function_name = candidate_function_name;
      instruction = candidate_instruction;
    }
  };
 
  entry_locationt initialize_entry_via_goto(
    const entry_goto_locationt &entry_goto_location,
    const goto_functionst &goto_functions);
 
  entry_locationt initialize_entry_via_source(
    const entry_source_locationt &entry_source_location,
    const goto_functionst &goto_functions);
 
  void handle_option(
    const std::string &option,
    const std::list<std::string> &values) override;
 
  void validate_options(const goto_modelt &goto_model) override;
 
  void
  get_memory_snapshot(const std::string &file, symbol_tablet &snapshot) const;
 
  void add_init_section(
    const symbol_exprt &func_init_done_var,
    goto_modelt &goto_model) const;
 
  const symbolt &fresh_symbol_copy(
    const symbolt &snapshot_symbol,
    symbol_tablet &symbol_table) const;
 
  code_blockt add_assignments_to_globals(
    const symbol_tablet &snapshot,
    goto_modelt &goto_model) const;
 
  void add_call_with_nondet_arguments(
    const symbolt &called_function_symbol,
    code_blockt &code) const;
 
  void insert_harness_function_into_goto_model(
    goto_modelt &goto_model,
    const symbolt &function) const;
 
  size_t pointer_depth(const typet &t) const;
 
  template <typename Adder>
  void collect_references(const exprt &expr, Adder &&add_reference) const
  {
    if(expr.id() == ID_symbol)
      add_reference(to_symbol_expr(expr).get_identifier());
    for(const auto &operand : expr.operands())
    {
      collect_references(operand, add_reference);
    }
  }
 
  template <typename Key>
  struct preordert
  {
  public:
    using relationt = std::multimap<Key, Key>;
    using keyst = std::set<Key>;
 
    explicit preordert(const relationt &preorder_relation)
      : preorder_relation(preorder_relation)
    {
    }
 
    template <typename T>
    void sort(
      const std::vector<std::pair<Key, T>> &input,
      std::vector<std::pair<Key, T>> &output)
    {
      std::unordered_map<Key, T> searchable_input;
      using valuet = std::pair<Key, T>;
 
      for(const auto &item : input)
      {
        searchable_input[item.first] = item.second;
      }
      auto associate_key_with_t =
        [&searchable_input](const Key &key) -> optionalt<valuet> {
        if(searchable_input.count(key) != 0)
          return valuet(key, searchable_input[key]);
        else
          return {};
      };
      auto push_to_output = [&output](const valuet &value) {
        output.push_back(value);
      };
      for(const auto &item : input)
      {
        dfs(item, associate_key_with_t, push_to_output);
      }
    }
 
  private:
    const relationt &preorder_relation;
 
    keyst seen;
    keyst inserted;
 
    template <typename Value, typename Map, typename Handler>
    void dfs(Value &&node, Map &&key_to_t, Handler &&handle)
    {
      PRECONDITION(seen.empty() && inserted.empty());
      dfs_inner(node, key_to_t, handle);
      seen.clear();
      inserted.clear();
    }
 
    template <typename Value, typename Map, typename Handler>
    void dfs_inner(Value &&node, Map &&key_to_t, Handler &&handle)
    {
      const Key &key = node.first;
      if(seen.count(key) == 0)
      {
        seen.insert(key);
        auto key_range = preorder_relation.equal_range(key);
        for(auto it = key_range.first; it != key_range.second; ++it)
        {
          auto maybe_value = key_to_t(it->second);
          if(maybe_value.has_value())
            dfs_inner(*maybe_value, key_to_t, handle);
        }
      }
      if(inserted.count(key) != 0)
        return;
      handle(node);
      inserted.insert(key);
    }
  };
 
  std::string memory_snapshot_file;
  std::string initial_goto_location_line;
  std::string initial_source_location_line;
  std::unordered_set<irep_idt> variables_to_havoc;
 
  entry_locationt entry_location;
 
  message_handlert &message_handler;
 
  recursive_initialization_configt recursive_initialization_config;
};
 
#endif // CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_H