variable_sensitivity_domain.h File Reference

There are different ways of handling arrays, structures, unions and pointers. More...

#include <iosfwd>
#include <memory>
#include <analyses/ai_domain.h>
#include <analyses/variable-sensitivity/abstract_environment.h>
#include <analyses/variable-sensitivity/variable_sensitivity_configuration.h>

Include dependency graph for variable_sensitivity_domain.h:

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

Go to the source code of this file.

Classes
class	variable_sensitivity_domaint
class	variable_sensitivity_domain_factoryt

Macros
#define	OPT_VSD
#define	HELP_VSD
#define	PARSE_OPTIONS_VSD(cmdline, options)

Detailed Description

There are different ways of handling arrays, structures, unions and pointers.

interval_domaint and constant_propagator_domaint basically ignores them which is imprecise at best and out-right wrong at worst. For one project we needed to do better. We could have implemented a particular way of handling them in an existing domain, created a new one with it, etc. This would work but it means duplicate code and it is is inflexible when the same person / the next person comes along and says "actually, we really care about the pointer precision but less so the array so could you just ...". Thus the idea was to do this properly:

1. Build a "non-relational domain" and allow the abstractions used for individual variables to be different.
2. Give the user the option of which abstractions are used for structs, unions, arrays and pointers. These are the sensitivity options discussed above.
3. Have the domain options control which kind of abstractions are used for the individual values, i.e. constants, intervals, etc.

This is implemented in three parts:

abstract_objectt : The base / interface for abstractions of a single variable. The interface for these is effectively create (as top, bottom, from a constant or copy), transform, merge, convert to constant if possible. Child classes add additional bits of interface, for example array abstractions need a "read element" and a "write element" method, structures need a "read field" and "write field", etc. These objects are intended to be immutable and thus operations tend to produce pointers. This is so that we can easily produce copy-on-write maps of them which we need for scaling and performance. There are also children of these for the constant abstraction of one value, the interval abstraction of one value (to be implemented), etc.

abstract_environment : This contains the map from variable names for abstract_objectt's (the "non-relational" part of the domain). The map itself if copy-on-write for performance and scalability but this is all wrapped up nicely in danpoe's sharing_map. The interface here is evaluate (exprt -> abstract_objectt*), assign (name, abstract_objectt* -> bool), assume (exprt -> bool) and merge. It has a factory to build abstract_objectt* from types or constants but apart from that, doesn't know anything about which actual abstract_objectt's are being used. As long as program variables that are arrays have an abstract_objectt which has the array interface, and so on for structs, unions, etc. then the abstractions used for values can be freely mixed and matched in any way the user can get the factory to build.

variable_sensitivity_domaint : Implements the ai_domain_baset interface using an abstract_environment. The only real code here is the 'transform' method which looks at the instruction type and converts that into calls to eval, assume, assign and merge.

Definition in file variable_sensitivity_domain.h.

Macro Definition Documentation

HELP_VSD

#define HELP_VSD

Value:

  " {y--vsd-values} [{yconstants}|{yintervals}|{yset-of-constants}] \t "       \
  "value tracking\n"                                                           \
  " {y--vsd-structs} [{ytop-bottom}|{yevery-field}] \t "                       \
  "struct field sensitive analysis\n"                                          \
  " {y--vsd-arrays} [{ytop-bottom}|{ysmash}|{yup-to-n-elements}|"              \
  "{yevery-element}] \t "                                                      \
  "array entry sensitive analysis\n"                                           \
  " {y--vsd-array-max-elements} {uN} \t "                                      \
  "set the {un} in {y--vsd-arrays} {yup-to-n-elements} (defaults to 10 if "    \
  "not given)\n"                                                               \
  " {y--vsd-pointers} [{ytop-bottom}|{yconstants}|{yvalue-set}] \t "           \
  "pointer sensitive analysis\n"                                               \
  " {y--vsd-unions} [{ytop-bottom}] \t union sensitive analysis\n"             \
  " {y--vsd-data-dependencies} \t track data dependencies\n"                   \
  " {y--vsd-liveness} \t track variable liveness\n"                            \
  " {y--vsd-flow-insensitive} \t disables flow sensitivity\n"

Definition at line 85 of file variable_sensitivity_domain.h.

OPT_VSD

#define OPT_VSD

Value:

  "(vsd-values):"                                                              \
  "(vsd-structs):"                                                             \
  "(vsd-arrays):"                                                              \
  "(vsd-array-max-elements):"                                                  \
  "(vsd-pointers):"                                                            \
  "(vsd-unions):"                                                              \
  "(vsd-flow-insensitive)"                                                     \
  "(vsd-data-dependencies)"                                                    \
  "(vsd-liveness)"

Definition at line 74 of file variable_sensitivity_domain.h.

PARSE_OPTIONS_VSD

#define PARSE_OPTIONS_VSD	(		cmdline,
			options
	)

Value:

  options.set_option("values", cmdline.get_value("vsd-values"));               \
  options.set_option("pointers", cmdline.get_value("vsd-pointers"));           \
  options.set_option("arrays", cmdline.get_value("vsd-arrays"));               \
  options.set_option("array-max-elements", cmdline.get_value("vsd-array-max-elements")); /* NOLINT(whitespace/line_length) */ \
  options.set_option("structs", cmdline.get_value("vsd-structs"));             \
  options.set_option("unions", cmdline.get_value("vsd-unions"));               \
  options.set_option("flow-insensitive", cmdline.isset("vsd-flow-insensitive")); /* NOLINT(whitespace/line_length) */ \
  options.set_option("data-dependencies", cmdline.isset("vsd-data-dependencies")); /* NOLINT(whitespace/line_length) */ \
  options.set_option("liveness", cmdline.isset("vsd-liveness")); /* NOLINT(whitespace/line_length) */ \
  (void)0

Definition at line 103 of file variable_sensitivity_domain.h.