1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
/*++
Module Name:
dl_mk_array_instantiation.h
Abstract:
Transforms predicates so that array invariants can be discovered.
Motivation : Given a predicate P(a), no quantifier-free solution can express that P(a) <=> forall i, P(a[i]) = 0
Solution : Introduce a fresh variable i, and transform P(a) into P!inst(i, a).
Now, (P!inst(i,a) := a[i] = 0) <=> P(a) := forall i, a[i] = 0.
Transformation on Horn rules:
P(a, args) /\ phi(a, args, args') => P'(args') (for simplicity, assume there are no arrays in args').
Is transformed into:
(/\_r in read_indices(phi) P!inst(r, a, args)) /\ phi(a, args, args') => P'(args')
Limitations : This technique can only discover invariants on arrays that depend on one quantifier.
Related work : Techniques relying on adding quantifiers and eliminating them. See dl_mk_quantifier_abstraction and dl_mk_quantifier_instantiation
Implementation:
The implementation follows the solution suggested above, with more options. The addition of options implies that in the simple
case described above, we in fact have P(a) transformed into P(i, a[i], a).
1) Dealing with multiple quantifiers -> The options fixedpoint.xform.instantiate_arrays.nb_quantifier gives the number of quantifiers per array.
2) Enforcing the instantiation -> We suggest an option (enforce_instantiation) to enforce this abstraction. This transforms
P(a) into P(i, a[i]). This enforces the solver to limit the space search at the cost of imprecise results. This option
corresponds to fixedpoint.xform.instantiate_arrays.enforce
3) Adding slices in the mix -> We wish to have the possibility to further restrict the search space: we want to smash cells, given a smashing rule.
For example, in for loops j=0; j<n; j++, it might be relevant to restrict the search space and look for invariants that only depend on whether
0<=i<j or j<=i, where i is the quantified variable.
Formally, a smashing rule is a function from the Index set (usually integer) to integers (the id set).
GetId(i) should return the id of the set i belongs in.
In our example, we can give 0 as the id of the set {n, 0<=n<j} and 1 for the set {n, j<=n}, and -1 for the set {n, n<0}. We then have
GetId(i) = ite(i<0, -1, ite(i<j, 0, 1))
Given that GetId function, P(a) /\ phi(a, ...) => P'(...) is transformed into
(/\_r in read_indices(phi) P!inst(id_r, a[r], a) /\ GetId(r) = id_r) /\ phi(a, ...) => P'(...).
Note : when no slicing is done, GetId(i) = i.
This option corresponds to fixedpoint.xform.instantiate_arrays.slice_technique
Although we described GetId as returning integers, there is no reason to restrict the type of ids to integers. A more direct method,
for the 0<=i<j or j<=i case could be :
GetId(i) = (i<0, i<j)
GetId is even more powerful as we deal with the multiple quantifiers on multiple arrays.
For example, we can use GetId to look for the same quantifiers in each array.
Assume we have arrays a and b, instantiated with one quantifier each i and j.
We can have GetId(i,j) = ite(i=j, (i, true), (fresh, false))
4) Reducing the set of r in read_indices(phi): in fact, we do not need to "instantiate" on all read indices of phi,
we can restrict ourselves to those "linked" to a, through equalities and stores.
Author:
Julien Braine
Revision History:
--*/
namespace datalog ;