contracts.h

Go to the documentation of this file.

/*
 * This function is used to check function contracts.
 *
 * Verification Strategy: Abstraction and Hierarchical Verification
 *
 * Function contracts enable a manual abstraction approach to assist
 * over-approximation verification logic. By splitting verification into
 * system-level and function-level, we should be able to reduce verification
 * complexity.
 *
 * 1. Function-level verification (enforce_contracts):
 *    - Verify each function independently against its contract
 *    - Use contract as specification: assume requires -> execute function ->
 * assert ensures
 *    - This provides over-approximation: if function satisfies contract, it's
 * correct
 *    - Complexity: O(n) where n is function size, not system size
 *
 * 2. System-level verification (replace_calls):
 *    - Replace function calls with contract semantics
 *    - Use contract as abstraction: assert requires -> havoc assigns -> assume
 * ensures
 *    - This avoids exploring function body, reducing state space
 *    - Complexity: O(m) where m is call sites, not function implementations
 *
 * Benefits:
 * - Modularity: Verify functions separately from system
 * - Scalability: System verification doesn't need to explore function internals
 * - Reusability: Once function is verified, contract can be used in any context
 * - Over-approximation: Contract provides safe abstraction (may have false
 * positives)
 *
 * This approach transforms a complex system verification problem into:
 * - Multiple simpler function verification problems
 * - One system verification problem using abstracted functions
 *
 * It takes phases:
 * 1. Extract contract clauses (requires, ensures, assigns) from contract symbol
 * 2. For contract checking: rename original function, generate wrapper with
 * assume requires -> call -> assert ensures
 * 3. For contract replacement: replace calls with assert requires -> havoc
 * assigns -> assume ensures
 */
 
#ifndef ESBMC_CONTRACTS_H
#define ESBMC_CONTRACTS_H
 
#include <goto-programs/goto_functions.h>
#include <goto-programs/frame_enforcer.h>
#include <util/symtab/context.h>
#include <util/symtab/namespace.h>
#include <functional>
#include <map>
#include <set>
#include <string>

class code_contractst
{
public:
  // ========== __ESBMC_is_fresh support for ensures ==========

  struct is_fresh_mapping_t
  {
    irep_idt temp_var_name; 
    expr2tc ptr_expr;       
    expr2tc size_expr; 
  };
 
  code_contractst(
    goto_functionst &goto_functions,
    contextt &context,
    const namespacet &ns);

  std::set<std::string> enforce_contracts(
    const std::set<std::string> &to_enforce,
    const std::string &entry_function = "",
    bool check_assigns_compliance = false);

  void replace_calls(const std::set<std::string> &to_replace);

  void remove_inactive_clauses();

  bool has_contracts(const goto_programt &function_body) const;

  bool is_annotated_contract_function(const symbolt &func_sym) const;

  std::string clause_call_callee(const goto_programt &body) const;

  std::string clause_call_reason(const goto_programt &body) const;

  bool declares_contracts(const symbolt &func_sym) const;

  std::vector<symbolt *> short_name_candidates(
    const std::string &short_name,
    const std::function<bool(const symbolt &)> &accept);

  struct ptr_field_snapshot_t
  {
    expr2tc ptr_sym;      
    type2tc pointee_type; 
    irep_idt field_name;  
    type2tc field_type;   
    expr2tc snapshot_sym; 
  };

  struct ptr_deref_snapshot_t
  {
    expr2tc ptr_sym;      
    type2tc pointee_type; 
    irep_idt field_name;  
    type2tc value_type;   
    expr2tc snapshot_sym; 
    expr2tc
      array_index; 
    type2tc
      member_type; 
    expr2tc alias_exemption; 
  };

  struct arr_elem_snapshot_t
  {
    expr2tc arr_ptr;      
    type2tc arr_add_type; 
    type2tc elem_type;    
    std::vector<expr2tc> declared_indices;
    expr2tc witness_idx;  
    expr2tc snapshot_sym; 
  };

  struct param_extentt
  {
    expr2tc bytes;              
    bool justified;             
    bool from_is_fresh = false; 
  };

  bool is_compiler_generated(const std::string &function_name) const;

  std::string
  diagnose_contract_target(const std::string &function_name, bool for_replace);
 
private:
  goto_functionst &goto_functions;
  contextt &context;
  const namespacet &ns;
  frame_enforcert frame_enforcer;
  size_t ptr_field_snap_counter =
    0; 
  size_t ptr_deref_snap_counter =
    0; 
  size_t arr_elem_snap_counter =
    0; 

  static constexpr size_t WITNESS_IDX_FALLBACK_ELEMS = 100;

  symbolt *find_function_symbol(const std::string &function_name);

  void rename_function(const irep_idt &old_id, const irep_idt &new_id);

  goto_programt generate_checking_wrapper(
    const symbolt &original_func,
    const expr2tc &requires_clause,
    const expr2tc &ensures_clause,
    const irep_idt &original_func_id,
    const goto_programt &original_body,
    const std::vector<is_fresh_mapping_t> &is_fresh_mappings,
    bool alloc_ptr_params = false,
    const std::vector<expr2tc> &assigns_targets = {},
    bool check_assigns_compliance = false);

  expr2tc
  declare_local_symbol(const std::string &name, const type2tc &type) const;

  expr2tc declare_call_result(
    const symbolt &function_symbol,
    const expr2tc &ret_val,
    const locationt &call_location,
    goto_programt &replacement) const;

  void generate_replacement_at_call(
    const symbolt &function_symbol,
    const goto_programt &function_body,
    goto_programt::targett call_instruction,
    goto_programt &caller_body);

  expr2tc extract_requires_clause(const symbolt &contract_symbol);

  expr2tc extract_ensures_clause(const symbolt &contract_symbol);

  expr2tc extract_requires_from_body(const goto_programt &function_body);

  expr2tc extract_ensures_from_body(const goto_programt &function_body);

  std::vector<expr2tc>
  extract_assigns_from_body(const goto_programt &function_body);

  expr2tc extract_assigns_clause(const symbolt &contract_symbol);

  expr2tc replace_return_value_in_expr(
    const expr2tc &expr,
    const expr2tc &ret_val) const;

  expr2tc extract_struct_members_to_temps(
    const expr2tc &expr,
    const expr2tc &ret_val,
    goto_programt &wrapper,
    const locationt &location);

  expr2tc replace_symbol_in_expr(
    const expr2tc &expr,
    const expr2tc &old_symbol,
    const expr2tc &new_expr) const;

  expr2tc instantiate_assigns_target(
    const expr2tc &target_expr,
    const symbolt &function_symbol,
    const std::vector<expr2tc> &actual_args,
    bool &is_pointer_param) const;
 
  // ========== __ESBMC_old support ==========

  struct old_snapshot_t
  {
    expr2tc original_expr; 
    expr2tc snapshot_var;  

    bool is_ptr_region = false;
    type2tc region_elem_type = type2tc(); 
  };

  bool is_old_call(const expr2tc &expr) const;

  expr2tc create_snapshot_variable(
    const expr2tc &expr,
    const std::string &func_name,
    size_t index) const;

  static expr2tc find_snapshot_by_symbol(
    const irep_idt &thename,
    const std::vector<old_snapshot_t> &snapshots,
    bool want_region);

  static expr2tc try_replace_ptr_region_old(
    const type2tc &result_type,
    const expr2tc &ptr_expr,
    const std::vector<old_snapshot_t> &snapshots,
    const namespacet &ns);

  expr2tc replace_old_in_expr(
    const expr2tc &expr,
    const std::vector<old_snapshot_t> &snapshots) const;

  static void classify_ptr_region_snapshots(
    std::vector<old_snapshot_t> &old_snapshots,
    const goto_programt &function_body);

  static void check_old_snapshot_pointer_ambiguity(
    const std::vector<old_snapshot_t> &old_snapshots);

  std::vector<old_snapshot_t>
  collect_old_snapshots_from_body(const goto_programt &function_body) const;

  std::vector<ptr_field_snapshot_t> materialize_ptr_field_snapshots(
    const frame_enforcert::classified_assignst &classified,
    const symbolt &original_func,
    goto_programt &wrapper,
    const locationt &location,
    const std::string &func_name);

  void emit_ptr_field_assertions(
    const std::vector<ptr_field_snapshot_t> &snapshots,
    goto_programt &wrapper,
    const locationt &location);
 
  // ========== Phase 2C: pointer-parameter dereference assigns compliance
  // ==========

  std::vector<ptr_deref_snapshot_t> materialize_ptr_deref_snapshots(
    const frame_enforcert::classified_assignst &classified,
    const std::vector<expr2tc> &assigns_targets,
    const symbolt &original_func,
    goto_programt &wrapper,
    const locationt &location,
    const std::string &func_name,
    const std::map<irep_idt, param_extentt> &param_extents);

  void materialize_ptr_deref_array_field(
    const irep_idt &param_id,
    const irep_idt &field,
    const type2tc &ftype,
    const type2tc &pointee,
    const expr2tc &ptr_sym,
    const expr2tc &deref_expr,
    goto_programt &wrapper,
    const locationt &location,
    const std::string &func_name,
    std::vector<ptr_deref_snapshot_t> &result);

  void emit_ptr_deref_assertions(
    const std::vector<ptr_deref_snapshot_t> &snapshots,
    goto_programt &wrapper,
    const locationt &location);
 
  // ========== Phase 2B: array element assigns compliance ==========

  std::vector<arr_elem_snapshot_t> materialize_arr_elem_snapshots(
    const frame_enforcert::classified_assignst &classified,
    const std::vector<expr2tc> &assigns_targets,
    goto_programt &wrapper,
    const locationt &location,
    const std::string &func_name,
    const std::map<irep_idt, param_extentt> &param_extents);

  void emit_arr_elem_assertions(
    const std::vector<arr_elem_snapshot_t> &snapshots,
    goto_programt &wrapper,
    const locationt &location);

  expr2tc materialize_ptr_region_old_snapshot(
    const expr2tc &original_expr,
    const type2tc &region_elem_type,
    goto_programt &wrapper,
    const std::string &func_name,
    const locationt &location,
    const expr2tc &extent_bytes,
    size_t snap_idx) const;

  void materialize_old_snapshots_at_wrapper(
    std::vector<old_snapshot_t> &old_snapshots,
    goto_programt &wrapper,
    const std::string &func_name,
    const locationt &location,
    const std::map<irep_idt, param_extentt> &param_extents) const;

  std::vector<old_snapshot_t> materialize_old_snapshots_at_callsite(
    const std::vector<old_snapshot_t> &old_snapshots,
    const symbolt &function_symbol,
    const goto_programt &function_body,
    const expr2tc &requires_clause,
    const std::vector<expr2tc> &actual_args,
    goto_programt &replacement,
    const locationt &call_location) const;

  bool find_callsite_is_fresh_extent(
    const goto_programt &function_body,
    const expr2tc &target_param,
    const expr2tc &requires_clause,
    const code_typet::argumentst &params,
    const std::vector<expr2tc> &actual_args,
    expr2tc &out_size) const;
 
  // ========== Type fixing for return value comparisons ==========

  bool is_return_value_symbol(const symbol2t &sym) const;

  expr2tc
  remove_incorrect_casts(const expr2tc &expr, const expr2tc &ret_val) const;

  expr2tc
  fix_comparison_types(const expr2tc &expr, const expr2tc &ret_val) const;

  expr2tc normalize_fp_add_in_ensures(const expr2tc &expr) const;

  expr2tc normalize_ensures_guard_for_return_value(
    const expr2tc &ensures_clause,
    const expr2tc &ret_val) const;
 
  // ========== __ESBMC_is_fresh support for ensures ==========

  std::vector<is_fresh_mapping_t>
  extract_is_fresh_mappings_from_body(const goto_programt &function_body) const;

  expr2tc replace_is_fresh_temps(
    const expr2tc &expr,
    const std::vector<is_fresh_mapping_t> &mappings,
    bool require_dynamic) const;

  void havoc_assigns_targets(
    const expr2tc &assigns_clause,
    goto_programt &dest,
    const locationt &location);

  std::vector<expr2tc> extract_assigns_targets(const expr2tc &assigns_clause);

  void havoc_function_parameters(
    const symbolt &original_func,
    goto_programt &dest,
    const locationt &location);

  void havoc_static_globals(goto_programt &dest, const locationt &location);

  void havoc_globals_for_entry_harness(
    goto_programt &dest,
    const locationt &location,
    bool is_entry_harness);

  void add_pointer_validity_assumptions(
    goto_programt &wrapper,
    const symbolt &func,
    const locationt &location,
    const std::set<irep_idt> &skip_params,
    const std::set<irep_idt> &separated_params,
    std::vector<expr2tc> &allocated_ptrs,
    std::map<irep_idt, param_extentt> &param_extents);

  bool
  param_extent_is_observable(const symbolt &func, const irep_idt &param) const;

  expr2tc lower_is_fresh_in_requires(
    const symbolt &function_symbol,
    const goto_programt &function_body,
    const std::vector<expr2tc> &actual_args,
    expr2tc requires_clause,
    std::vector<expr2tc> &separation);

  void attach_alias_exemptions(
    std::vector<ptr_deref_snapshot_t> &result,
    const std::vector<expr2tc> &assigns_targets,
    const symbolt &original_func,
    goto_programt &wrapper,
    const locationt &location,
    const std::string &func_name);

  expr2tc retain_allocation_for_free(
    goto_programt &wrapper,
    const expr2tc &allocated,
    const std::string &name,
    const symbolt &func,
    const locationt &location);

  void emit_pointer_param_aliasing(
    goto_programt &wrapper,
    const symbolt &func,
    const locationt &location,
    const std::vector<std::pair<expr2tc, std::string>> &params);

  void emit_receiver_backing(
    goto_programt &wrapper,
    const expr2tc &p,
    const std::string &param_name,
    const type2tc &pointee,
    const symbolt &func,
    const locationt &location);

  expr2tc emit_pointer_param_malloc(
    goto_programt &wrapper,
    const expr2tc &p,
    const std::string &param_name,
    const symbolt &func,
    const locationt &location);
};
 
#endif // ESBMC_CONTRACTS_H