goto_model.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Symbol Table + CFG
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H
#define CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H
 
#include <util/symbol_table.h>
#include <util/journalling_symbol_table.h>
 
#include "abstract_goto_model.h"
#include "goto_functions.h"
#include "validate_goto_model.h"
 
// A model is a pair consisting of a symbol table
// and the CFGs for the functions.
 
class goto_modelt : public abstract_goto_modelt
{
public:
  symbol_tablet symbol_table;
  goto_functionst goto_functions;
 
  void clear()
  {
    symbol_table.clear();
    goto_functions.clear();
  }
 
  goto_modelt()
  {
  }
 
  // Copying is normally too expensive
  goto_modelt(const goto_modelt &)=delete;
  goto_modelt &operator=(const goto_modelt &)=delete;
 
  // Move operations need to be explicitly enabled as they are deleted with the
  // copy operations
  // default for move operations isn't available on Windows yet, so define
  //  explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx
  //  under "Defaulted and Deleted Functions")
 
  goto_modelt(goto_modelt &&other):
    symbol_table(std::move(other.symbol_table)),
    goto_functions(std::move(other.goto_functions))
  {
  }
 
  goto_modelt &operator=(goto_modelt &&other)
  {
    symbol_table=std::move(other.symbol_table);
    goto_functions=std::move(other.goto_functions);
    return *this;
  }
 
  void unload(const irep_idt &name) { goto_functions.unload(name); }
 
  // Implement the abstract goto model interface:
 
  const goto_functionst &get_goto_functions() const override
  {
    return goto_functions;
  }
 
  const symbol_tablet &get_symbol_table() const override
  {
    return symbol_table;
  }
 
  const goto_functionst::goto_functiont &get_goto_function(
    const irep_idt &id) override
  {
    return goto_functions.function_map.at(id);
  }
 
  bool can_produce_function(const irep_idt &id) const override
  {
    return goto_functions.function_map.find(id) !=
           goto_functions.function_map.end();
  }
 
  void validate(
    const validation_modet vm = validation_modet::INVARIANT,
    const goto_model_validation_optionst &goto_model_validation_options =
      goto_model_validation_optionst{}) const override
  {
    symbol_table.validate(vm);
 
    // Does a number of checks at the function_mapt level to ensure the
    // goto_program is well formed. Does not call any validate methods
    // (at the goto_functiont level or below)
    validate_goto_model(goto_functions, vm, goto_model_validation_options);
 
    const namespacet ns(symbol_table);
    goto_functions.validate(ns, vm);
  }
};
 
class wrapper_goto_modelt : public abstract_goto_modelt
{
public:
  wrapper_goto_modelt(
    const symbol_tablet &symbol_table,
    const goto_functionst &goto_functions) :
    symbol_table(symbol_table),
    goto_functions(goto_functions)
  {
  }
 
  const goto_functionst &get_goto_functions() const override
  {
    return goto_functions;
  }
 
  const symbol_tablet &get_symbol_table() const override
  {
    return symbol_table;
  }
 
  const goto_functionst::goto_functiont &get_goto_function(
    const irep_idt &id) override
  {
    return goto_functions.function_map.at(id);
  }
 
  bool can_produce_function(const irep_idt &id) const override
  {
    return goto_functions.function_map.find(id) !=
           goto_functions.function_map.end();
  }
 
  void validate(
    const validation_modet vm,
    const goto_model_validation_optionst &goto_model_validation_options)
    const override
  {
    symbol_table.validate(vm);
 
    // Does a number of checks at the function_mapt level to ensure the
    // goto_program is well formed. Does not call any validate methods
    // (at the goto_functiont level or below)
    validate_goto_model(goto_functions, vm, goto_model_validation_options);
 
    const namespacet ns(symbol_table);
    goto_functions.validate(ns, vm);
  }
 
private:
  const symbol_tablet &symbol_table;
  const goto_functionst &goto_functions;
};
 
class goto_model_functiont
{
public:
  goto_model_functiont(
    journalling_symbol_tablet &symbol_table,
    goto_functionst &goto_functions,
    const irep_idt &function_id,
    goto_functionst::goto_functiont &goto_function):
  symbol_table(symbol_table),
  goto_functions(goto_functions),
  function_id(function_id),
  goto_function(goto_function)
  {
  }
 
  void compute_location_numbers()
  {
    goto_functions.compute_location_numbers(goto_function.body);
  }
 
  journalling_symbol_tablet &get_symbol_table()
  {
    return symbol_table;
  }
 
  goto_functionst::goto_functiont &get_goto_function()
  {
    return goto_function;
  }
 
  const irep_idt &get_function_id()
  {
    return function_id;
  }
 
private:
  journalling_symbol_tablet &symbol_table;
  goto_functionst &goto_functions;
  irep_idt function_id;
  goto_functionst::goto_functiont &goto_function;
};
 
#endif // CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H