[ ]

library(COLIBRI_DOC)

Simple COLIBRI interface

Predicates

Arithmetic operators
Operators allowed in numerical expressions.
use_3B
Enable 3B filtering.
no_3B
Disable 3B filtering.
use_delta
Enable difference logics and simplex.
no_delta
Disable difference logics and simplex.
solve_cstrs
Asks to solve current constraints.
no_solve
Disable constraints solving.
set_timeout(T)
Define time limit.
set_threshold(T)
Change reduction threshold.
get_threshold(T)
Return current reduction threshold.
int_vars(Type,Vars)
Typing constraints for "integer" variables Vars.
set_default_int_bounds(Low,High)
Default range for int variables
Vars #: Range
Range definition for "integer" types: int, int(N) and uint(N) (where N is the size in bits).
X #< Y
X is strictly less than Y.
X #= Y
X is equal to Y.
X #=< Y
X is less or equal to Y.
X #> Y
X is strictly greater than Y.
X #>= Y
X is greater or equal to Y.
X #\= Y
X is not equal to Y.
real_vars(+Type,Vars)
Typing constraints for "real" vars.
Vars $: +Range
Range definition for "real" types: real, float and double.
X $< Y
X is stricly less than Y.
X $= Y
X is equal to Y.
X $=< Y
X is less or equal to Y.
X $> Y
X is strictly greater than Y.
X $>= Y
X is greater or equal to Y.
X $\= Y
X is not equal to Y.
isFinite(X)
Restriction to finite values.
isInfinite(X)
Restriction to infinite values.
isNormal(X)
Restriction to normal values.
isSubnormal(X)
Restriction to subnormal values.
isPositive(X)
Restriction to positive floating point values.
isNegative(X)
Restriction to negative floating point values.
neg(X)
The negation of X is true.
X and Y
X is true and Y is true.
X or Y
X is true or Y is true.
X xor Y
Eclusive or of X and Y.
X => Y
X implies Y.
ite(Cond,Then,Else)
if Cond then Then else Else.

Description

A simple solver using COLIBRI

Usage
  colibri.(sh|bat) File
or
  colibri.(sh|bat)

The sh and bat extentions corresponds to linux and windows environments. In the first form the script colibri reads query from file File. In the second form the input is searched in a file colibri.in in the directory from where the script is called. Results are sent to stdout.

Constraint solving techniques are widely recognized as a powerful tool for Validation and Verification activities such as test data generation or counter-example generation from a formal model, program source code or binary code. A constraint solver maintains a list of posted constraints (constraint store) over a set of variables and a set of allowed values (domain) for each variable, and provides facilities for constraint propagation (filtering) and for instantiation of variables (labeling) in order to find a solution.

We present here a simple interface to the COLIBRI library (COnstraint LIBrary for veRIfication) developed at CEA List and used inside the GATeL tool for model based testing and verification from Lustre/SCADE. The variety of types and constraints provided by COLIBRI makes it possible to use it in other validation tools at CEA LIST like PathCrawle for test data generation purposes and Osmose for structural testing from binary code.

COLIBRI provides basic constraints for arithmetic operations and comparisons of various numeric types (integers, reals and floats). Cast constraints are available for cast operations between these types. COLIBRI also provides basic procedures allowing to instantiate variables in their domains making it possible to design specific labelling procedures. Thus the three aforementioned testing tools have designed their own labelling procedures on the basis of COLIBRI primitives.

The domains of numerical variables are represented by unions of disjoint intervals (no NaNs for floats): integer bounds for integers, double float bounds for reals, and double/simple float bounds for double/simple floating point formats. These unions of intervals make it possible to accurately handle domain differences. For each numeric type and each basic unary/binary operation or comparison, COLIBRI provides the corresponding constraint.

Moreover, for each arithmetic operation, additional filtering rules apply algebraic simplifications, which are very similar for integer and real arithmetics, whereas floating arithmetics uses specific rules. Here are a few examples of basic algebraic simplifications.

Bounded and modular integer arithmetics

COLIBRI provides two kinds of arithmetics for integers: bounded arithmetics for ideal finite integers and modular arithmetics for signed/unsigned computer integers. Bounded arithmetics is implemented with classical filtering rules for integer interval arithmetics. These rules are managed in the projection functions of each arithmetic constraint. Moreover, a congruence domain is associated to each integer variable. Filtering rules handle these congruences in order to compute new ones and maintain the consistency of interval bounds with congruences. The congruences are introduced by multiplications by a constant and propagated in the projection functions of each arithmetic constraint.

Modular arithmetics constraints are implemented by a combination of bounded arithmetics constraints with modulus constraints. Thus they benefit from the mechanisms provided for bounded integer arithmetics. Notice that using the unions of disjoint intervals for the domain representation makes it possible to precisely represent the domain of signed/unsigned integers. For example, consider the constraint A + B = C over 3-bit unsigned integers where A in 2..4, B in 4..7 and C in 0..7. This constraint is handled by the constraints corresponding to the bounded arithmetic expression C = A + B - K * 8
where K in 0..1 represents the overflow status.
The filtering of these constraints converges to the interval C in [0..3, 6..7] where the sub-interval 0..3 of C is reached when there is an overflow (i.e. K = 1).
The domain representation by compact intervals in this case would be less precise and result in a complete interval C in [0..7] without any reduction.

Real and floating point arithmetics

Real arithmetics is implemented with classical filtering rules for real interval arithmetics where interval bounds are double floats. In real interval arithmetics each projection function is computed using different rounding modes for the lower and the upper bounds of the resulting intervals. The lower bound is computed by rounding downward, towards  -1.0Inf, while the upper bound is computed by rounding upward, towards +1.0Inf. This enlarging ensures that the resulting interval is the smallest interval of doubles including all real solutions.

Floating point arithmetics is implemented with a specific interval. Notice that properties like associativity or distributivity do not hold in floating point calculus.
The projection functions in this arithmetics have to take into account absorption and cancellation phenomena specific to floating point computations. These phenomena are handled by specific filtering rules allowing to further reduce  the domains of floating point variables. For example, the constraint A+X=A over floating point numbers means that X is absorbed by A.
The minimal absolute value in the domain of X can be used to eliminate all the values in the domain of A that do not absorb this minimum. Thus, in double precision with the default rounding mode (called nearest to even), for
X = 1.0 the domain of A is strongly reduced to the union of two intervals of values that can absorb X:
[MinDouble .. -9007199254740996.0,  9007199254740992.0 .. MaxDouble].

COLIBRI uses very general and powerful filtering rules for addition and subtraction operations. For example, for the constraint A+B=1.0 in double precision with the nearest to even rounding mode, such filtering rules converge to the same interval for A and B
[-9007199254740991.0 .. 9007199254740992.0].

Implementation details

COLIBRI is implemented in ECLiPSe Prolog. Its suspensions, generic unification and meta-term mechanisms make it possible to easily design new abstract domains and associated constraints. Incremental constraint posting with on-the-fly filtering and automatic backtracking to a previous constraint state provided by COLIBRI are important benefits for search-based state exploration tools, and in particular, for test generation tools.

About


Generated from COLIBRI_DOC.eci on Wed Mar 23 17:46:17 2016