instrument_spec_assigns.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Instrument assigns clauses in code contracts.
 
Author: Remi Delmas
 
Date: January 2022
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_INSTRUMENT_SPEC_ASSIGNS_H
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_INSTRUMENT_SPEC_ASSIGNS_H
 
#include <util/expr_util.h>
#include <util/message.h>
#include <util/namespace.h>
#include <util/symbol_table_base.h>
 
#include <goto-programs/goto_program.h>
 
#include <algorithm>
#include <unordered_map>
#include <unordered_set>
 
// forward declarations
class conditional_target_group_exprt;
class cfg_infot;
class goto_functionst;
 
class conditional_target_exprt : public exprt
{
public:
  conditional_target_exprt(const exprt &_condition, const exprt &_target)
    : exprt(irep_idt{}, typet{}, {_condition, _target})
  {
    INVARIANT(
      !has_subexpr(_condition, ID_side_effect),
      "condition must have no side_effect sub-expression");
    add_source_location() = _target.source_location();
  }
 
  const exprt &condition() const
  {
    return operands()[0];
  }
 
  const exprt &target() const
  {
    return operands()[1];
  }
};
 
enum class car_havoc_methodt
{
  HAVOC_OBJECT,
  HAVOC_SLICE,
  NONDET_ASSIGN
};
 
class car_exprt : public exprt
{
public:
  car_exprt(
    const exprt &_condition,
    const exprt &_target,
    const exprt &_target_start_address,
    const exprt &_target_size,
    const symbol_exprt &_validity_var,
    const symbol_exprt &_lower_bound_var,
    const symbol_exprt &_upper_bound_var,
    const car_havoc_methodt _havoc_method)
    : exprt(
        irep_idt{},
        typet{},
        {_condition,
         _target,
         _target_start_address,
         _target_size,
         _validity_var,
         _lower_bound_var,
         _upper_bound_var}),
      havoc_method(_havoc_method)
  {
    add_source_location() = _target.source_location();
  }
 
  const car_havoc_methodt havoc_method;
 
  const exprt &condition() const
  {
    return operands()[0];
  }
 
  const exprt &target() const
  {
    return operands()[1];
  }
 
  const exprt &target_start_address() const
  {
    return operands()[2];
  }
 
  const exprt &target_size() const
  {
    return operands()[3];
  }
 
  const symbol_exprt &valid_var() const
  {
    return to_symbol_expr(operands()[4]);
  }
 
  const symbol_exprt &lower_bound_var() const
  {
    return to_symbol_expr(operands()[5]);
  }
 
  const symbol_exprt &upper_bound_var() const
  {
    return to_symbol_expr(operands()[6]);
  }
};
 
bool has_propagate_static_local_pragma(source_locationt &source_location);
 
void add_propagate_static_local_pragma(source_locationt &source_location);
 
//  "unsigned-overflow-check", "conversion-check".
void add_pragma_disable_pointer_checks(source_locationt &source_location);
 
void add_pragma_disable_assigns_check(source_locationt &source_location);
 
goto_programt::instructiont &
add_pragma_disable_assigns_check(goto_programt::instructiont &instr);
 
goto_programt &add_pragma_disable_assigns_check(goto_programt &prog);
 
class instrument_spec_assignst
{
public:
  instrument_spec_assignst(
    const irep_idt &_function_id,
    const goto_functionst &_functions,
    cfg_infot &_cfg_info,
    symbol_table_baset &_st,
    message_handlert &_message_handler)
    : function_id(_function_id),
      functions(_functions),
      cfg_info(_cfg_info),
      st(_st),
      ns(_st),
      log(_message_handler),
      mode(st.lookup_ref(function_id).mode)
  {
  }
 
  void track_spec_target(const exprt &expr, goto_programt &dest);
 
  void
  track_stack_allocated(const symbol_exprt &symbol_expr, goto_programt &dest);
 
  bool stack_allocated_is_tracked(const symbol_exprt &symbol_expr) const;
 
  void invalidate_stack_allocated(
    const symbol_exprt &symbol_expr,
    goto_programt &dest);
 
  void track_heap_allocated(const exprt &expr, goto_programt &dest);
 
  void track_static_locals(goto_programt &dest);
 
  void track_static_locals_between(
    goto_programt::const_targett it,
    const goto_programt::const_targett end,
    goto_programt &dest);
 
protected:
  class location_intervalt
  {
  public:
    location_intervalt()
    {
      min_line = std::numeric_limits<std::size_t>::max();
      min_col = std::numeric_limits<std::size_t>::max();
      max_line = std::numeric_limits<std::size_t>::min();
      max_col = std::numeric_limits<std::size_t>::min();
    }
 
    void anywhere()
    {
      min_line = std::numeric_limits<std::size_t>::min();
      min_col = std::numeric_limits<std::size_t>::min();
      max_line = std::numeric_limits<std::size_t>::max();
      max_col = std::numeric_limits<std::size_t>::max();
    }
 
    void update(const source_locationt &source_location)
    {
      PRECONDITION(source_location.is_not_nil());
      // use pessimistic lowest value to update min for undefined
      update_min(
        line_to_size_t(
          source_location, std::numeric_limits<std::size_t>::min()),
        col_to_size_t(
          source_location, std::numeric_limits<std::size_t>::min()));
 
      // use pessimistic highest value to update max for undefined
      update_max(
        line_to_size_t(
          source_location, std::numeric_limits<std::size_t>::max()),
        col_to_size_t(
          source_location, std::numeric_limits<std::size_t>::max()));
    }
 
    bool contains(const source_locationt &source_location)
    {
      if(source_location.is_not_nil())
      {
        return
          // use pessimistic highest value to compare to min for undefined
          is_lte(
            min_line,
            min_col,
            line_to_size_t(
              source_location, std::numeric_limits<std::size_t>::max()),
            col_to_size_t(
              source_location, std::numeric_limits<std::size_t>::max())) &&
          // use pessimistic lowest value to compare to max for undefined
          is_lte(
            line_to_size_t(
              source_location, std::numeric_limits<std::size_t>::min()),
            col_to_size_t(
              source_location, std::numeric_limits<std::size_t>::min()),
            max_line,
            max_col);
      }
      else
      {
        return true;
      }
    }
 
  private:
    std::size_t col_to_size_t(
      const source_locationt &source_location,
      std::size_t default_value)
    {
      if(
        source_location.get_line().empty() ||
        source_location.get_column().empty())
      {
        return default_value;
      }
      else
      {
        std::stringstream stream(id2string(source_location.get_column()));
        size_t res;
        stream >> res;
        return res;
      }
    }
 
    std::size_t line_to_size_t(
      const source_locationt &source_location,
      std::size_t default_value)
    {
      if(source_location.get_line().empty())
      {
        return default_value;
      }
      else
      {
        std::stringstream stream(id2string(source_location.get_line()));
        size_t res;
        stream >> res;
        return res;
      }
    }
 
    static bool is_lte(size_t line0, size_t col0, size_t line1, size_t col1)
    {
      return (line0 < line1) || ((line0 == line1) && (col0 <= col1));
    }
 
    void update_min(size_t line, size_t col)
    {
      if(is_lte(line, col, min_line, min_col))
      {
        min_line = line;
        min_col = col;
      }
    }
 
    void update_max(size_t line, size_t col)
    {
      if(is_lte(max_line, max_col, line, col))
      {
        max_line = line;
        max_col = col;
      }
    }
 
    std::size_t min_line;
    std::size_t min_col;
    std::size_t max_line;
    std::size_t max_col;
  };
 
  typedef std::unordered_map<irep_idt, location_intervalt> covered_locationst;
  typedef std::unordered_set<symbol_exprt, irep_hash> propagated_static_localst;
 
  void traverse_instructions(
    const irep_idt ambient_function_id,
    goto_programt::const_targett it,
    const goto_programt::const_targett end,
    covered_locationst &covered_locations,
    propagated_static_localst &propagated) const;
 
  void collect_static_symbols(
    covered_locationst &covered_locations,
    std::unordered_set<symbol_exprt, irep_hash> &dest);
 
public:
  void check_inclusion_assignment(const exprt &lhs, goto_programt &dest) const;
 
  void check_inclusion_heap_allocated_and_invalidate_aliases(
    const exprt &expr,
    goto_programt &dest);
 
  void instrument_instructions(
    goto_programt &body,
    goto_programt::targett instruction_it,
    const goto_programt::targett &instruction_end,
    const std::function<bool(const goto_programt::targett &)> &pred = {});
 
  template <typename C>
  void get_static_locals(std::insert_iterator<C> inserter) const
  {
    std::transform(
      from_static_local.cbegin(),
      from_static_local.cend(),
      inserter,
      // can use `const auto &` below once we switch to C++14
      [](const symbol_exprt_to_car_mapt::value_type &s) { return s.first; });
  }
 
protected:
  const irep_idt &function_id;
 
  const goto_functionst &functions;
 
  cfg_infot &cfg_info;
 
  symbol_table_baset &st;
 
  const namespacet ns;
 
  messaget log;
 
  const irep_idt &mode;
 
  void track_spec_target_group(
    const conditional_target_group_exprt &group,
    goto_programt &dest);
 
  void track_plain_spec_target(const exprt &expr, goto_programt &dest);
 
  void create_snapshot(const car_exprt &car, goto_programt &dest) const;
 
  exprt
  target_validity_expr(const car_exprt &car, bool allow_null_target) const;
 
  void target_validity_assertion(
    const car_exprt &car,
    bool allow_null_target,
    goto_programt &dest) const;
 
  exprt inclusion_check_single(
    const car_exprt &lhs,
    const car_exprt &candidate_car) const;
 
  exprt inclusion_check_full(
    const car_exprt &lhs,
    bool allow_null_lhs,
    bool include_stack_allocated) const;
 
  void inclusion_check_assertion(
    const car_exprt &lhs,
    bool allow_null_lhs,
    bool include_stack_allocated,
    goto_programt &dest) const;
 
  void invalidate_car(
    const car_exprt &tracked_car,
    const car_exprt &freed_car,
    goto_programt &result) const;
 
  void invalidate_heap_and_spec_aliases(
    const car_exprt &freed_car,
    goto_programt &dest) const;
 
  bool must_track_decl(const goto_programt::const_targett &target) const;
 
  bool must_track_dead(const goto_programt::const_targett &target) const;
 
  bool must_track_decl_or_dead(const irep_idt &ident) const;
 
  bool must_check_assign(const goto_programt::const_targett &target);
 
  void instrument_assign_statement(
    goto_programt::targett &instruction_it,
    goto_programt &body) const;
 
  void instrument_call_statement(
    goto_programt::targett &instruction_it,
    goto_programt &body);
 
  using cond_target_exprt_to_car_mapt = std::
    unordered_map<const conditional_target_exprt, const car_exprt, irep_hash>;
 
  cond_target_exprt_to_car_mapt from_spec_assigns;
 
  const car_exprt &
  create_car_from_spec_assigns(const exprt &condition, const exprt &target);
 
  using symbol_exprt_to_car_mapt =
    std::unordered_map<const symbol_exprt, const car_exprt, irep_hash>;
 
  symbol_exprt_to_car_mapt from_stack_alloc;
 
  const car_exprt &create_car_from_stack_alloc(const symbol_exprt &target);
 
  using exprt_to_car_mapt =
    std::unordered_map<const exprt, const car_exprt, irep_hash>;
 
  using car_expr_listt = std::list<car_exprt>;
  car_expr_listt from_heap_alloc;
 
  const car_exprt &create_car_from_heap_alloc(const exprt &target);
 
  symbol_exprt_to_car_mapt from_static_local;
 
  const car_exprt &create_car_from_static_local(const symbol_exprt &target);
 
  car_exprt create_car_expr(const exprt &condition, const exprt &target) const;
};
 
#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_INSTRUMENT_SPEC_ASSIGNS_H