CBMC
dfcc_spec_functionst Class Reference

This class rewrites GOTO functions that use the built-ins: More...

#include <dfcc_spec_functions.h>

+ Collaboration diagram for dfcc_spec_functionst:

Public Member Functions

 dfcc_spec_functionst (goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library)
 
void generate_havoc_function (const irep_idt &function_id, const irep_idt &havoc_function_id, std::size_t &nof_targets)
 From a function: More...
 
void generate_havoc_instructions (const irep_idt &function_id, const goto_programt &original_program, const exprt &write_set_to_havoc, goto_programt &havoc_program, std::size_t &nof_targets)
 Translates original_program that specifies assignable targets into a program that havocs the targets. More...
 
void to_spec_assigns_function (const irep_idt &function_id, std::size_t &nof_targets)
 Transforms (in place) a function. More...
 
void to_spec_assigns_instructions (const exprt &write_set_to_fill, const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets)
 Rewrites in place program expressed in terms of built-ins specifying assignable targets declaratively using __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_from, __CPROVER_object_upto into a program populating write_set_to_fill. More...
 
void to_spec_frees_function (const irep_idt &function_id, std::size_t &nof_targets)
 Transforms (in place) a function. More...
 
void to_spec_frees_instructions (const exprt &write_set_to_fill, const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets)
 Rewrites in place program expressed in terms of built-ins specifying freeable targets declaratively using __CPROVER_freeable into a program populating write_set_to_fill. More...
 

Protected Member Functions

const typetget_target_type (const exprt &expr)
 Extracts the type of an assigns clause target expression The expression must be of the form: expr = cast(address_of(target), empty*) More...
 

Protected Attributes

goto_modeltgoto_model
 
message_handlertmessage_handler
 
messaget log
 
dfcc_librarytlibrary
 
namespacet ns
 

Detailed Description

This class rewrites GOTO functions that use the built-ins:

  • __CPROVER_assignable,
  • __CPROVER_object_whole,
  • __CRPOVER_object_from,
  • __CPROVER_object_upto,
  • __CPROVER_freeable into GOTO functions that populate a write set instance or havoc a write set by calling the library implementation of these built-ins.

Definition at line 43 of file dfcc_spec_functions.h.

Constructor & Destructor Documentation

◆ dfcc_spec_functionst()

dfcc_spec_functionst::dfcc_spec_functionst ( goto_modelt goto_model,
message_handlert message_handler,
dfcc_libraryt library 
)

Definition at line 21 of file dfcc_spec_functions.cpp.

Member Function Documentation

◆ generate_havoc_function()

void dfcc_spec_functionst::generate_havoc_function ( const irep_idt function_id,
const irep_idt havoc_function_id,
std::size_t &  nof_targets 
)

From a function:

void function_id(params);

generates a new function:

void havoc_function_id(__CPROVER_assignable_set_ptr_t write_set_to_havoc);

Which havocs the targets specified by function_id, passed

Parameters
function_idfunction to generate instructions from
havoc_function_idwrite set variable to havoc
nof_targetsmaximum number of targets to havoc

Definition at line 43 of file dfcc_spec_functions.cpp.

◆ generate_havoc_instructions()

void dfcc_spec_functionst::generate_havoc_instructions ( const irep_idt function_id,
const goto_programt original_program,
const exprt write_set_to_havoc,
goto_programt havoc_program,
std::size_t &  nof_targets 
)

Translates original_program that specifies assignable targets into a program that havocs the targets.

Precondition
The original_program must be already fully inlined, and the only function calls allowed are to the built-ins that specify assignable targets: __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_from, __CPROVER_object_upto.

The original_program is assumed to encode an assigns clause using the built-ins __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_from, __CPROVER_object_upto. The method traverses original_program and emits a sequence of GOTO instructions in havoc_program that encode the havocing of the target write set write_set_to_havoc.

Parameters
[in]function_idfunction id to use for prefixing fresh variables
[in]original_programprogram from which to derive the havoc program
[in]write_set_to_havocwrite set symbol to havoc
[out]havoc_programdestination program for havoc instructions
[out]nof_targetsmax number of havoc targets discovered

Definition at line 143 of file dfcc_spec_functions.cpp.

◆ get_target_type()

const typet & dfcc_spec_functionst::get_target_type ( const exprt expr)
protected

Extracts the type of an assigns clause target expression The expression must be of the form: expr = cast(address_of(target), empty*)

Definition at line 33 of file dfcc_spec_functions.cpp.

◆ to_spec_assigns_function()

void dfcc_spec_functionst::to_spec_assigns_function ( const irep_idt function_id,
std::size_t &  nof_targets 
)

Transforms (in place) a function.

void function_id(params);

into a function

void function_id(
params,
__CPROVER_assignable_set_t write_set_to_fill,
)

Where:

  • write_set_to_fill is the write set to populate.
Parameters
function_idfunction to transform in place
nof_targetsreceives the estimated size of the write set

Definition at line 246 of file dfcc_spec_functions.cpp.

◆ to_spec_assigns_instructions()

void dfcc_spec_functionst::to_spec_assigns_instructions ( const exprt write_set_to_fill,
const irep_idt language_mode,
goto_programt program,
std::size_t &  nof_targets 
)

Rewrites in place program expressed in terms of built-ins specifying assignable targets declaratively using __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_from, __CPROVER_object_upto into a program populating write_set_to_fill.

It is the responsibility of the caller of this method to instrument the resulting program against another write set instance to check them for unwanted side effects.

Precondition
The program must be already fully inlined, and the only function calls allowed are to the built-ins that specify assignable targets: __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_from, __CPROVER_object_upto.
Parameters
[in]write_set_to_fillwrite set to populate.
[in]language_modeused to format expressions.
[in,out]programfunction to transform in place
[out]nof_targetsreceives the estimated size of the write set

Definition at line 272 of file dfcc_spec_functions.cpp.

◆ to_spec_frees_function()

void dfcc_spec_functionst::to_spec_frees_function ( const irep_idt function_id,
std::size_t &  nof_targets 
)

Transforms (in place) a function.

void function_id(params);

into a function

void function_id(
params,
__CPROVER_assignable_set_t write_set_to_fill,
)

Where:

  • write_set_to_fill is the write set to populate.

The function must be fully inlined and loop free.

Parameters
function_idfunction to transform in place
nof_targetsreceives the estimated size of the write set

Definition at line 329 of file dfcc_spec_functions.cpp.

◆ to_spec_frees_instructions()

void dfcc_spec_functionst::to_spec_frees_instructions ( const exprt write_set_to_fill,
const irep_idt language_mode,
goto_programt program,
std::size_t &  nof_targets 
)

Rewrites in place program expressed in terms of built-ins specifying freeable targets declaratively using __CPROVER_freeable into a program populating write_set_to_fill.

It is the responsibility of the caller of this method to instrument the resulting program against another write set instance to check them for unwanted side effects.

Precondition
The program must be already fully inlined, and the only function calls allowed are to the built-ins that specify freeable targets: __CPROVER_freeable.
Parameters
[in]write_set_to_fillwrite set to populate.
[in]language_modeused to format expressions.
[in,out]programfunction to transform in place
[out]nof_targetsreceives the estimated size of the write set

Definition at line 355 of file dfcc_spec_functions.cpp.

Member Data Documentation

◆ goto_model

goto_modelt& dfcc_spec_functionst::goto_model
protected

Definition at line 202 of file dfcc_spec_functions.h.

◆ library

dfcc_libraryt& dfcc_spec_functionst::library
protected

Definition at line 205 of file dfcc_spec_functions.h.

◆ log

messaget dfcc_spec_functionst::log
protected

Definition at line 204 of file dfcc_spec_functions.h.

◆ message_handler

message_handlert& dfcc_spec_functionst::message_handler
protected

Definition at line 203 of file dfcc_spec_functions.h.

◆ ns

namespacet dfcc_spec_functionst::ns
protected

Definition at line 206 of file dfcc_spec_functions.h.


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