IndexedNamesAndTypedVariables

Indexed Variable Names

An indexed variable name is essentially an index (i.e., uint64_t). These indexes are used as keys in Patricia trees which implement variable environments and are also directly translated to dimensions in numerical domains such as Zones, Octagons, and so on. The class indexed_varname defined in https://github.com/seahorn/crab/blob/master/include/crab/types/varname_factory.hpp provides indexed names in Crab. Among other things, this class provides also a string to name these numerical indexes.

Indexed variable names can be only generated by variable factories (see e.g., class variable_factory).

Typed Variables

An indexed variable name does not carry out type information. The class variable defined https://github.com/seahorn/crab/blob/master/include/crab/types/variable.hpp is a wrapper to an indexed variable name that, in addition, provides the type of the variable (see variable_type_kind enum type). For instance, a typed variable can tell whether a variable represents an integer of 32 bits, a pointer (called references in Crab), or a region.

Type Checking of the CFG and abstract transformers

Both CrabIR CFGs and abstract transformers are defined over typed variables. Crab has a simple algorithm that checks whether a CFG is well-typed. However, the CFG type-checker is bypassed when either an user calls directly abstract transformers via the C++ API or when an abstract domain calls another abstract domain.

Very importantly, all abstract domains assume that abstract transformers are called with the expected types. For instance, the abstract operation apply(op, x, y, z) performs the arithmetic operation y op z and stores the result in x. Therefore, the interpretation of x, y, z is always either integers or reals (remember that we don't allow to mix integers with reals). However, it is possible that an abstract domain does not check that x,y,z are numbers and instead, it just assumes that. Therefore, it's the responsability of the caller to make sure that abstract transformers are called with the expected types.

Warning: note that some numerical abstract domains might completely ignore the type of a variable. This is possible, for instance, if the domain assumes that all variables must be defined over mathematical integers. In this case, if a variable has a wrong type (e.g., a region or reference), things might work and no runtime error is reported. This is just simply because the abstract domain only uses the indexed variable name. Nevertheless, this situation shouldn't be allowed.