CBMC

Entry point into the contracts transformation. More...

#include <dfcc.h>

+ Collaboration diagram for dfcct:

Public Member Functions

 dfcct (const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, const std::optional< std::pair< irep_idt, irep_idt >> &to_check, const bool allow_recursive_calls, const std::map< irep_idt, irep_idt > &to_replace, const loop_contract_configt loop_contract_config, message_handlert &message_handler, const std::set< std::string > &to_exclude_from_nondet_static)
 Class constructor. More...
 
void transform_goto_model ()
 Applies function contracts and loop contracts transformation to GOTO model using the dynamic frame condition checking approach. More...
 

Protected Member Functions

void check_transform_goto_model_preconditions ()
 Checks preconditions on arguments of transform_goto_model. More...
 
void partition_function_symbols (std::set< irep_idt > &pure_contract_symbols, std::set< irep_idt > &other_symbols)
 Partitions the function symbols of the symbol table into pure contracts and other function symbols symbols. More...
 
void link_model_and_load_dfcc_library ()
 
void instrument_harness_function ()
 
void lift_memory_predicates ()
 
void wrap_checked_function ()
 
void wrap_replaced_functions ()
 
void wrap_discovered_function_pointer_contracts ()
 
void instrument_other_functions ()
 
void reinitialize_model ()
 Re-initialise the GOTO model. More...
 

Protected Attributes

const optionstoptions
 
goto_modeltgoto_model
 
const irep_idtharness_id
 
const std::optional< std::pair< irep_idt, irep_idt > > & to_check
 
const bool allow_recursive_calls
 
const std::map< irep_idt, irep_idt > & to_replace
 
const loop_contract_configt loop_contract_config
 
const std::set< std::string > & to_exclude_from_nondet_static
 
message_handlertmessage_handler
 
messaget log
 
dfcc_libraryt library
 
namespacet ns
 
dfcc_spec_functionst spec_functions
 
dfcc_contract_clauses_codegent contract_clauses_codegen
 
dfcc_instrumentt instrument
 
dfcc_lift_memory_predicatest memory_predicates
 
dfcc_contract_handlert contract_handler
 
dfcc_swap_and_wrapt swap_and_wrap
 
std::size_t max_assigns_clause_size
 Tracks the maximum number of targets in any assigns clause handled in the transformation (used to specialize/unwind loops in DFCC library functions) More...
 
std::set< irep_idtpure_contract_symbols
 
std::set< irep_idtother_symbols
 
std::set< irep_idtfunction_pointer_contracts
 

Detailed Description

Entry point into the contracts transformation.

Definition at line 115 of file dfcc.h.

Constructor & Destructor Documentation

◆ dfcct()

dfcct::dfcct ( const optionst options,
goto_modelt goto_model,
const irep_idt harness_id,
const std::optional< std::pair< irep_idt, irep_idt >> &  to_check,
const bool  allow_recursive_calls,
const std::map< irep_idt, irep_idt > &  to_replace,
const loop_contract_configt  loop_contract_config,
message_handlert message_handler,
const std::set< std::string > &  to_exclude_from_nondet_static 
)

Class constructor.

Parameters
optionsCLI options (used to lookup options for language config when re-defining the model's entry point)
goto_modelGOTO model to transform
harness_idProof harness name, must be the entry point of the model
to_check(function,contract) pair for contract checking
allow_recursive_callsAllow the checked function to be recursive
to_replacefunctions-to-contract mapping for replacement
loop_contract_configconfiguration for applying loop contracts
message_handlerused for debug/warning/error messages
to_exclude_from_nondet_staticset of symbols to exclude when

Definition at line 141 of file dfcc.cpp.

Member Function Documentation

◆ check_transform_goto_model_preconditions()

void dfcct::check_transform_goto_model_preconditions ( )
protected

Checks preconditions on arguments of transform_goto_model.

The preconditions are:

  • The harness function exists in the model and has a body,
  • The model's entry point is the harness function,
  • The harness function is distinct from any checked or replaced function,
  • The harness function is distinct from any contract,
  • All function to check exist and have a body available,
  • All function to replace exist (body is not necessary),
  • All contracts to check or replace exist as pure contract symbols,
  • The checked function cannot be also replaced,
  • compiler built-ins or __CPROVER_* functions cannot be checked against a contract (because they cannot be instrumented),
  • all symbols of to_exclude_from_nondet_static exist in the model.

Definition at line 192 of file dfcc.cpp.

◆ instrument_harness_function()

void dfcct::instrument_harness_function ( )
protected

Definition at line 305 of file dfcc.cpp.

◆ instrument_other_functions()

void dfcct::instrument_other_functions ( )
protected

Definition at line 446 of file dfcc.cpp.

◆ lift_memory_predicates()

void dfcct::lift_memory_predicates ( )
protected

Definition at line 318 of file dfcc.cpp.

◆ link_model_and_load_dfcc_library()

void dfcct::link_model_and_load_dfcc_library ( )
protected

Definition at line 283 of file dfcc.cpp.

◆ partition_function_symbols()

void dfcct::partition_function_symbols ( std::set< irep_idt > &  pure_contract_symbols,
std::set< irep_idt > &  other_symbols 
)
protected

Partitions the function symbols of the symbol table into pure contracts and other function symbols symbols.

Definition at line 256 of file dfcc.cpp.

◆ reinitialize_model()

void dfcct::reinitialize_model ( )
protected

Re-initialise the GOTO model.

The new entry point must be the proof harness function specified for instrumentation.

The "initialize" (aka INITIALIZE_FUNCTION) is the function that assigns initial values to all statics of the model;

The initialize function must do the following:

  • assign a nondet value to all statics of the user program
  • assign the specified initial value to all instrumentation statics
  • add an entry in the static unbounded map of instrumented functions for each instrumented function

A call to nondet_static will re-generate the initialize function with nondet values. The instrumentation statics will not get nondet initialised by virtue of being tagged with ID_C_no_nondet_initialization.

However, nondet_static expects instructions to be either function calls or assignments with a symbol_exprt LHS. Since entries for the instrumented function maps are not symbol_exprts but index_exprts they need to be moved to the harness function.

The "start" function (aka goto_functionst::entry_point()) is the function from which SymEx starts.

The start function must do the following:

  • call the initialize function,
  • generate nondet values for the arguments of the proof harness function
  • call the harness function with said nondet arguments

All of which can be done using a call to generate_ansi_c_start_function, assuming the initialize function is already available in the symbol table.

So we do the following:

  • regenerate the "initialize" function
  • call nondet_static
  • add extra instructions at the end of the harness function for the instrumented functions map
  • call generate_ansi_c_start_function Make all user-defined statics nondet. Other statics added by the instrumentation will be unaffected because they are tagged with ID_C_no_nondet_initialization when created Update statics and static function maps

Definition at line 521 of file dfcc.cpp.

◆ transform_goto_model()

void dfcct::transform_goto_model ( )

Applies function contracts and loop contracts transformation to GOTO model using the dynamic frame condition checking approach.

Functions to check/replace are explicitly mapped to contracts. When checking function foo against contract bar, we require the actual contract symbol to exist as contract::bar in the symbol table.

Transformation steps:

  • check preconditions on existence and absence of clash between harness, functions and contract symbols parameters.
  • link the goto model to the standard library
  • instrument the harness function.
  • partition function symbols of the model into
    • contract:: symbols
    • assigns/frees clause specification functions (not instrumented)
    • all other functions (instrumented)
  • swap-and-wrap/instrument functions to check with their contract
  • swap-and-wrap/instrument functions to replace with their contract
  • swap-and-wrap all discovered function pointer contracts with themselves (replacement mode)
  • instrument all remaining functions GOTO model
  • (this includes standard library functions).
  • specialise the instrumentation functions by unwinding loops they contain to the maximum size of any assigns clause involved in the model.

Definition at line 466 of file dfcc.cpp.

◆ wrap_checked_function()

void dfcct::wrap_checked_function ( )
protected

Definition at line 330 of file dfcc.cpp.

◆ wrap_discovered_function_pointer_contracts()

void dfcct::wrap_discovered_function_pointer_contracts ( )
protected

Definition at line 376 of file dfcc.cpp.

◆ wrap_replaced_functions()

void dfcct::wrap_replaced_functions ( )
protected

Definition at line 359 of file dfcc.cpp.

Member Data Documentation

◆ allow_recursive_calls

const bool dfcct::allow_recursive_calls
protected

Definition at line 171 of file dfcc.h.

◆ contract_clauses_codegen

dfcc_contract_clauses_codegent dfcct::contract_clauses_codegen
protected

Definition at line 183 of file dfcc.h.

◆ contract_handler

dfcc_contract_handlert dfcct::contract_handler
protected

Definition at line 186 of file dfcc.h.

◆ function_pointer_contracts

std::set<irep_idt> dfcct::function_pointer_contracts
protected

Definition at line 196 of file dfcc.h.

◆ goto_model

goto_modelt& dfcct::goto_model
protected

Definition at line 168 of file dfcc.h.

◆ harness_id

const irep_idt& dfcct::harness_id
protected

Definition at line 169 of file dfcc.h.

◆ instrument

dfcc_instrumentt dfcct::instrument
protected

Definition at line 184 of file dfcc.h.

◆ library

dfcc_libraryt dfcct::library
protected

Definition at line 180 of file dfcc.h.

◆ log

messaget dfcct::log
protected

Definition at line 176 of file dfcc.h.

◆ loop_contract_config

const loop_contract_configt dfcct::loop_contract_config
protected

Definition at line 173 of file dfcc.h.

◆ max_assigns_clause_size

std::size_t dfcct::max_assigns_clause_size
protected

Tracks the maximum number of targets in any assigns clause handled in the transformation (used to specialize/unwind loops in DFCC library functions)

Definition at line 191 of file dfcc.h.

◆ memory_predicates

dfcc_lift_memory_predicatest dfcct::memory_predicates
protected

Definition at line 185 of file dfcc.h.

◆ message_handler

message_handlert& dfcct::message_handler
protected

Definition at line 175 of file dfcc.h.

◆ ns

namespacet dfcct::ns
protected

Definition at line 181 of file dfcc.h.

◆ options

const optionst& dfcct::options
protected

Definition at line 167 of file dfcc.h.

◆ other_symbols

std::set<irep_idt> dfcct::other_symbols
protected

Definition at line 195 of file dfcc.h.

◆ pure_contract_symbols

std::set<irep_idt> dfcct::pure_contract_symbols
protected

Definition at line 194 of file dfcc.h.

◆ spec_functions

dfcc_spec_functionst dfcct::spec_functions
protected

Definition at line 182 of file dfcc.h.

◆ swap_and_wrap

dfcc_swap_and_wrapt dfcct::swap_and_wrap
protected

Definition at line 187 of file dfcc.h.

◆ to_check

const std::optional<std::pair<irep_idt, irep_idt> >& dfcct::to_check
protected

Definition at line 170 of file dfcc.h.

◆ to_exclude_from_nondet_static

const std::set<std::string>& dfcct::to_exclude_from_nondet_static
protected

Definition at line 174 of file dfcc.h.

◆ to_replace

const std::map<irep_idt, irep_idt>& dfcct::to_replace
protected

Definition at line 172 of file dfcc.h.


The documentation for this class was generated from the following files: