restrict_function_pointers.h File Reference

Given goto functions and a list of function parameters or globals that are function pointers with lists of possible candidates, replace use of these function pointers with calls to the candidate. More...

#include <unordered_map>
#include <unordered_set>
#include <util/exception_utils.h>
#include <util/irep.h>
#include "goto_program.h"

Include dependency graph for restrict_function_pointers.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	invalid_restriction_exceptiont
class	function_pointer_restrictionst

Macros
#define	RESTRICT_FUNCTION_POINTER_OPT   "restrict-function-pointer"
#define	RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT    "function-pointer-restrictions-file"
#define	RESTRICT_FUNCTION_POINTER_BY_NAME_OPT    "restrict-function-pointer-by-name"
#define	OPT_RESTRICT_FUNCTION_POINTER
#define	HELP_RESTRICT_FUNCTION_POINTER

Functions
void	parse_function_pointer_restriction_options_from_cmdline (const cmdlinet &cmdline, optionst &options)
void	restrict_function_pointers (message_handlert &message_handler, goto_modelt &goto_model, const optionst &options)
	Apply function pointer restrictions to a goto_model. More...

Detailed Description

Given goto functions and a list of function parameters or globals that are function pointers with lists of possible candidates, replace use of these function pointers with calls to the candidate.

The purpose here is to avoid unnecessary branching i.e. "there are 600 functions with this signature, but I know it's always going to be one of these two"

Definition in file restrict_function_pointers.h.

Macro Definition Documentation

HELP_RESTRICT_FUNCTION_POINTER

#define HELP_RESTRICT_FUNCTION_POINTER

Value:

  " {y--" RESTRICT_FUNCTION_POINTER_OPT                                        \
  "} "                                                                         \
  "{upointer_name}/{utarget[,targets]*} \t "                                   \
  "restrict a function pointer to a set of possible targets; targets must "    \
  "all exist in the symbol table with a matching type; works for globals "     \
  "and function parameters right now\n"                                        \
  " {y--" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT                              \
  "} {ufile_name} \t "                                                         \
  "add function pointer restrictions from file {ufile_name}\n"                 \
  " {y--" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT                                \
  "} "                                                                         \
  "{usymbol_name}/{utarget[targets]*} \t "                                     \
  "restrict a function pointer where {usymbol_name} is the unmangled "         \
  "name, before labelling function pointers\n"

Definition at line 48 of file restrict_function_pointers.h.

OPT_RESTRICT_FUNCTION_POINTER

#define OPT_RESTRICT_FUNCTION_POINTER

Value:

  "(" RESTRICT_FUNCTION_POINTER_OPT                                            \
  "):"                                                                         \
  "(" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT                                  \
  "):"                                                                         \
  "(" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT "):"

Definition at line 41 of file restrict_function_pointers.h.

RESTRICT_FUNCTION_POINTER_BY_NAME_OPT

#define RESTRICT_FUNCTION_POINTER_BY_NAME_OPT    "restrict-function-pointer-by-name"

Definition at line 38 of file restrict_function_pointers.h.

RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT

#define RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT    "function-pointer-restrictions-file"

Definition at line 36 of file restrict_function_pointers.h.

RESTRICT_FUNCTION_POINTER_OPT

#define RESTRICT_FUNCTION_POINTER_OPT   "restrict-function-pointer"

Definition at line 35 of file restrict_function_pointers.h.

Function Documentation

parse_function_pointer_restriction_options_from_cmdline()

void parse_function_pointer_restriction_options_from_cmdline	(	const cmdlinet &	cmdline,
		optionst &	options
	)

Definition at line 201 of file restrict_function_pointers.cpp.

restrict_function_pointers()

void restrict_function_pointers	(	message_handlert &	message_handler,
		goto_modelt &	goto_model,
		const optionst &	options
	)

Apply function pointer restrictions to a goto_model.

Each restriction is a mapping from a pointer name to a set of possible targets. Replace calls of these "restricted" pointers with a branch on the value of the function pointer, comparing it to the set of possible targets. This also adds an assertion that the pointer actually has one of the listed values.

Note: This requires label_function_pointer_call_sites to be run before

Definition at line 171 of file restrict_function_pointers.cpp.