The general idea of VyPR is that the developer writes queries over specific functions in a Python program. These queries take the form of properties that should hold at runtime. VyPR decides at runtime whether these properties are satisfied. The results of the queries are given in the form of data describing the satisfaction by the program of the properties.
Queries are written in a central file called VyPR_queries.py in the root of a project's directory structure. This file is written in Python using VyPR's query building library as such:
verification_conf = {
"package.module" : {
"class.method" : [
Forall(
q = changes('x')
).Check(
lambda q : (
q.next_call('g').duration()._in([0, 0.1])
)
)
]# class.method
}# package.module
}# verification_conf
The structure is explained below.
In order to tell VyPR where to apply instrumentation and subsequently query at runtime, you need to give the path to each function that you want to monitor.
In the query above, the first level strings tell VyPR which module to look inside and the second level strings tell VyPR which function inside that module.
In order to write a query, you should:
We break down function runs into sequences of states (variables and their values) and operations that take place to transform those values.
VyPR currently supports writing constraints over variables' values and function calls. These are treated as objects on which you can call methods to build up constraints.
Suppose that q holds a state. Then we can check that the value given to x by q is no more than 1:
q('x')._in([0, 1])
Currently the only transitions that are supported are function calls. We can take a call t that corresponds to a function call and check that it lasts for no more than 2 seconds:
t.duration()._in([0, 2])
Given a variable, say q, you can obtain the earliest state or call in the future based on some criteria, and then use the result like a normal variable:
q.next_call('f').duration()._in([0, 1])
Given any variable t that represents a call, we can ask for the states at either side with
t.input()
and
t.result()We can then treat these like any other states, for example by measuring the value to which they map a program variable:
t.result()('x')
Measured quantities can also be compared to each other. We can compare state, for example to check that a function is not modifying a variable:
t.input()('x').equals(t.result()('x'))
or to check that the duration of a function call has a certain relation to some state:
q.next_call('f').duration().lessThan(q('val'))
There are standard propositional operators for you to link predicates on variables. For example, you can place a constraint on the next call along from the state q, but guarded by a constraint on q:
If(q('x')._in([0, 10])).then(
q.next_call('f').duration()._in([0, 0.5])
)
We could combine the if-then construct to write something like
If(q.next_call('f').input()('x')._in([0, 10])).then(
q.next_call('f').duration()._in([0, 0.5])
)
which asserts that, for some state held by the variable q, if the value of x immediately before the next call to f is no more than 10, then the next call to f should take no more than 0.5 seconds.
Once a property is defined, VyPR must be told where in the program to check. Without this, the variables you use in your property have no meaning. Suppose that you want to take
If(q('x')._in([0, 10])).then(
q.next_call('f')._in([0, 0.5])
)
and check it whenever x changes (so q holds the state in which x has changed). You can do this with:
Forall(q = changes('x')).\
Check(
lambda q :
If(q('x')._in([0, 10])).then(
q.next_call('f')._in([0, 0.5])
)
)
The Forall tells VyPR that the property given to Check should be checked whenever x changes at runtime. Further, each time x changes, the state induced will be bound to the variable q.
Suppose you want to check that, whenever file changes, if file is equal to some string, every future call to write should satisfy some constraint. Then you can write the query:
Forall(q = changes('file')).\
Forall(t = calls('write', after='q')).\
Check(
lambda q, t :
If(q('file').equals('some file name')).then(
t.duration()._in([0, 1])
)
)
For the value to which a state q maps x, you can construct the predicates:
q('x').equals(v)
q('x')._in([n, m])
q('x')._in((n, m))
Here, v is either a constant or another measurable quantity (see above).
You can find the next call in time to the function f with:
q.next_call('f')
and treat the result as a call.
For a call t, you can measure the duration with:
t.duration()
and write predicates on this duration:
t.duration()._in([n, m])
Durations of calls can be compared to other measurable quantities:
t.duration() < v
where v is some other measurable quantity.
Currently arithmetic with measurable quantities with respect to constants is supported in a limited form:
t.duration() < v * n
where n is some constant of the same type of the measured quantity v. NB: here, multiplication must be on the right-hand side.
The states at either side of a call can be obtained with:
t.input(), t.result()which gives a state object like any other.
The time between two states can be measured with:
timeBetween(q1, q2)
which can then be subject to a constraint by writing:
timeBetween(q1, q2)._in([n, m])
You can use boolean operators to combine predicates:
land(a1, a2, ..., a_n) lor(a_1, ..., a_n) lnot(a)
There is syntactic sugar for things like implication, which you can write as:
If(a).then(b)
You must wrap your final property in a lambda; VyPR will use this at runtime:
lambda q1, ..., qn : (...)
You can select points of interest based on states or calls with:
q = changes('x')
t = calls('f')
If a selection predicate is given after the first one in the list, it must depend on the previous one:
Forall(q = changes('x')).Forall(t = calls('f', after='q'))...
And the property to check at each point of interest is given by:
Forall(q1 = ...). ... .Forall(qn = ...)\
.Check(
lambda q1, ..., qn :
(...)
)