Skip to content

Commit 0e612c0

Browse files
jfmcjfmc
committed
(ciaopp) added basicdom base code, examples, and tutorial (by Daniel Jurjo)
Src-commit: 98c9de33d110b24b2bc9207886fb6b60f6d1cb17
1 parent 39cef05 commit 0e612c0

File tree

11 files changed

+2088
-0
lines changed

11 files changed

+2088
-0
lines changed

‎doc/tutorials/basicdom_tutorial/SETTINGS.pl

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
:- module(_, [], [doccfg]).
2+
3+
filepath := '..'.
4+
5+
doc_structure := 'tut'-
6+
[
7+
'sign',
8+
'polyhedra_clpq'
9+
].
10+
11+
commonopts := no_patches|no_bugs|no_biblio.
12+
doc_mainopts := ~commonopts.
13+
doc_compopts := ~commonopts.
14+
15+
% TODO: enable by default?
16+
syntax_highlight := yes.

‎doc/tutorials/basicdom_tutorial/polyhedra_clpq.pl

Lines changed: 307 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,307 @@
1+
:- module(_, [], [assertions, regtypes, nativeprops, modes]).
2+
3+
:- doc(title, "Implementing a Polyhedra analysis in CiaoPP").
4+
5+
:- doc(module, "
6+
7+
8+
In this tutorial we show how to implement a relational Abstract Domain
9+
in CiaoPP. We implement a Polyhedra analysis to abstract numerical relations.
10+
11+
In order to keep this tutorial simple, we will not discuss technical
12+
details about how to represent polyhedra nor how to implement some
13+
complex operations. To ease the development of this domains we use an
14+
already implemented library in the Ciao system: the @tt{poly_clpq} library
15+
which implements a number of operations to manipulate (rational,
16+
closed) polyhedra based on CLP(Q) operations. Concretely we will use
17+
the @tt{project/3}, @tt{convexhull/3}, @tt{simplify/2}, and
18+
@tt{contains/2} predicates. The two first predicates are based on the
19+
paper:
20+
21+
@begin{verbatim} \"Computing convex hulls with a linear
22+
solver\", Florence Benoy, Andy King, Frédéric Mesnard. TPLP 5(1-2):
23+
259-271 (2005). @end{verbatim}
24+
25+
We begin by describing the abstraction and some operations to manipulate it:
26+
27+
28+
@section{Operations over the Abstract Substitution}
29+
30+
Since we aim to abstract a rather complex property a substitution-like
31+
abstraction pairing variables with values would not be very useful.
32+
Instead of that, we define our abstraction as a pair @tt{(Ctrs, Vars)} such that:
33+
@begin{itemize}
34+
@item @tt{Ctrs} is a set of closed constraints defining a polyhedron and,
35+
@item @tt{Vars} is the set of variables over which the polyhedron is defined.
36+
@end{itemize}
37+
38+
Notice that all the variables appearing in @tt{Ctrs} must appear in
39+
@tt{Vars}. Moreover, carrying @tt{Vars} we are also inferring a type
40+
property, only numerical variables can be in @tt{Vars}.
41+
42+
Finally, given a polyhedron @tt{([], [X])} we can infer that @tt{X} is
43+
a numerical variable over which nothing else is known.
44+
45+
Now that we have defined how our abstraction looks like we can
46+
implement the first predicate that CiaoPP requires:
47+
48+
@subsubsection{@var{asub(+ASub)}}
49+
The predicate @tt{asub/1} is used to define the regtype @tt{asub/1}.
50+
In our case is defined as follows:
51+
```ciao
52+
53+
asub('$bottom'):-!.
54+
asub(([], _)) :- !.
55+
asub((Ctr, Vs)) :-
56+
varset(Ctr, CtrVs),
57+
ord_subset(CtrVs, Vs), !,
58+
valid_ctrs(Ctr).
59+
60+
valid_ctrs([]).
61+
valid_ctrs([>=(_, _)|Cs]) :-
62+
valid_ctrs(Cs).
63+
valid_ctrs([=(_, _)|Cs]) :-
64+
valid_ctrs(Cs).
65+
valid_ctrs([=<(_, _)|Cs]) :-
66+
valid_ctrs(Cs).
67+
```
68+
69+
@subsubsection{@var{project(+Vars, +ASub, -Proj)}}
70+
71+
The predicate @tt{project/3} projects the information captured by
72+
@var{ASub} over the set of variables @tt{Vars}. Luckily, the library
73+
@tt{poly_clpq} already defines a project predicate which keeps the
74+
constraints related with the given set of variables. However, the
75+
obtained polyhedron may not be minimal (and we want to keep the
76+
minimal representation). Because of that, we also invoke the
77+
@tt{simplify_poly/2} predicate which yields a reduced polyhedron.
78+
79+
```ciao
80+
project(_, '$bottom', '$bottom').
81+
project(Vs, (Ctrs, CVs), Proj) :-
82+
ord_intersection(Vs, CVs, Vs_pr),
83+
poly_clpq:project(Vs_pr, Ctrs, Ctr_pr),
84+
simplify_poly((Ctr_pr, Vs_pr), Proj).
85+
```
86+
87+
@subsubsection{@var{augment(+Vars, +ASub, -ASub_aug)}}
88+
89+
The predicate @tt{augment/3} increases the abstraction with the
90+
variables in @var{Vars}. This variables are @em{free, fresh
91+
variables}. Because of that, we know that they are not numerical at
92+
this analysis point. Thus the predicate has to unify @var{ASub} with
93+
@var{ASub_aug}.
94+
95+
```ciao
96+
augment(_Vars, Poly, Poly) :- !. %% They are free fresh vars so they are not in the polyhedron (yet)
97+
```
98+
99+
@subsubsection{@var{extend(+Sv, +Prime, +Call, -Success)}}
100+
101+
The @tt{extend/4} operation is used to update the information that
102+
exists at call-time @var{Call} with the inferred information
103+
@var{Prime}. In this case, we can just merge the constraints at
104+
call-time whith the \"prime\" constraints and then simplify the
105+
resulting constraint store.
106+
107+
108+
```ciao
109+
extend(_Sv,'$bottom',_Call,'$bottom').
110+
extend(_Sv, Prime, Call,Success):-
111+
Prime = (Poly_pr, Vars_pr),
112+
Call = (Poly_cl, Vars_cl),
113+
ord_union(Poly_pr, Poly_cl, Poly_mr), %% Merge Poly
114+
ord_union(Vars_pr, Vars_cl, Vars_mr), %% Merge Vars
115+
simplify_poly((Poly_mr, Vars_mr), Success).
116+
```
117+
118+
Now that we have defined the operations required by CiaoPP to operate
119+
over the abstraction, we turn our attention to define the operations
120+
over the lattice:
121+
122+
@section{Operations over the Lattice}
123+
124+
@subsubsection{@var{less_or_equal(+ASub1, +ASub2)}}
125+
126+
The @tt{less_or_equal/2} predicate succeeds if the abstraction
127+
@var{ASub1} is less or equal than @var{ASub2}. In this case we use the
128+
@tt{contains/2} predicate to check whether @var{ASub2} contains
129+
@var{ASub1}.
130+
131+
```ciao
132+
133+
less_or_equal('$bottom', _) :- !.
134+
less_or_equal((Poly1, Vars), (Poly2, Vars)) :-
135+
poly_clpq:contains(Poly2, Poly1), !.
136+
```
137+
138+
@subsubsection{@var{lub(+ASub1, +ASub2, -Lub)} and @var{widen(+ASub1, +ASub2, -Widen)}}
139+
140+
The predicate @tt{lub/3} is used to compute the @em{least upper bound}
141+
of two abstractions. Thus, given two polyhedrons, their convexhull is
142+
a safe candidate for least upper bound. Before, computing the
143+
convexhull we invoke the predicate @tt{match_dimensions/4} which will
144+
keep both abstractions defined over the variables appearing in both polyhedra.
145+
146+
The predicate @tt{widen/3} is used to acelerate the computation of the fixpoint. Many different widens can be defined for a polyhedra domain. That is outside of the scope of this tutorial, thus we use @tt{lub/3}.
147+
148+
```ciao
149+
150+
lub(ASub1,'$bottom',ASub1):- !.
151+
lub('$bottom',ASub2,ASub2):- !.
152+
lub(ASub1,ASub2,Lub):-
153+
match_dimensions(ASub1,ASub2,New_ASub1,New_ASub2),
154+
New_ASub1 = (Poly1,Vars),
155+
New_ASub2 = (Poly2,Vars),
156+
poly_clpq:convhull(Poly1, Poly2, Poly_h),!,
157+
Lub = (Poly_h,Vars).
158+
lub(_ASub1,_ASub2,'$top').
159+
160+
widen(L1, L2, W) :-
161+
lub(L1, L2, W).
162+
163+
match_dimensions(ASub1,ASub2,ASub1,ASub2):-
164+
ASub1 = (_Poly1,Vars1),
165+
ASub2 = (_Poly2,Vars2),
166+
Vars1 == Vars2,!.
167+
match_dimensions(ASub1,ASub2,New_ASub1,New_ASub2):-
168+
ASub1 = (_Poly1,Vars1),
169+
ASub2 = (_Poly2,Vars2),
170+
ord_intersection(Vars1,Vars2,Vars),
171+
polyhedra_clpq:project(Vars, ASub1,New_ASub1),
172+
polyhedra_clpq:project(Vars,ASub2,New_ASub2).
173+
174+
175+
```
176+
177+
@section{Abstracting operations}
178+
179+
Now that we have described the lattice and the abstract representation used, we describe how the elements of the concrete program are abstracted.
180+
181+
@subsubsection{@var{topmost(+Vars, +MaybeCall, -TopAbs)}}
182+
183+
The predicate @tt{topmost/3} is used to compute an abstraction such that nothing is known about the variables in @var{Vars}. We have to consider the case in which @var{MaybeCall} unifies with an atom @tt{not_provided}, that means that a top-most abstraction over the variables in @var{Vars} has to be defined.
184+
```ciao
185+
186+
topmost(_, not_provided, ([],[])).
187+
topmost(_, Poly, Poly) :- !.
188+
```
189+
190+
191+
@subsubsection{@var{amgu(+Var, +Term, +Call, -Succ)}}
192+
The predicate @tt{amgu/4} computes the @em{abstract most general unifier} for the unification @var{Var=Term} given the current abstracted information @var{Call}. Hence, @var{Succ} is the result of update @var{Call} with such an information.
193+
Is important to note that @var{Var} is indeed a variable so cases are only need to be considered about @var{Term}.
194+
195+
For our polyhedra domain, defining @tt{amgu/4} is pretty straightforward:
196+
197+
```ciao
198+
amgu(Var, Term, Poly1, Poly2) :-
199+
number(Term), !,
200+
poly_add_constraint(Poly1, Var=Term, Poly2).
201+
amgu(Var, Term, Poly1, Poly2) :-
202+
var(Term), !,
203+
poly_add_constraint(Poly1, Var=Term, Poly2).
204+
amgu(_, _, Poly1, Poly1).
205+
206+
207+
poly_add_constraint('$bottom', _, '$bottom').
208+
poly_add_constraint((Poly, Vars), Const, NASub) :-
209+
varset(Const, ConstVars), sort(ConstVars, ConstVars_s),
210+
Poly_add = [Const|Poly],
211+
ord_union(Vars, ConstVars_s, Vars_add),
212+
simplify_poly((Poly_add, Vars_add), NASub).
213+
```
214+
215+
@subsubsection{@var{known_builtin(+Sg_Key)}}
216+
217+
This flag allow the analyzer to know whith literals our domain can
218+
abstract. By default, the analyzer will consider that is analyzing a
219+
pure program, i.e., only unifications and predicate calls are present.
220+
However, we may want to predefine the abstraction for some known
221+
predicates or, as in this case, capture arithmetical expressions.
222+
223+
```ciao
224+
225+
known_builtin('is/2').
226+
known_builtin('>/2').
227+
known_builtin('>=/2').
228+
known_builtin('</2').
229+
known_builtin('=</2').
230+
```
231+
232+
@subsubsection{@var{abstract_literal(+Sg_key, +Sg, +Call, -Succ)}}
233+
234+
Now that we have declared which builtins our domain knows how to
235+
handle we have to describe their abstraction. The predicate
236+
@tt{abstract_literal/4} implements how to abstract a literal
237+
(@var{Sg}) which has a known @var{Sg_key} key.
238+
In our case we can add the new constraints to the polyhedron in @var{Call} and then simplify it to obtain the success abstraction @var{Succ}.
239+
240+
```ciao
241+
242+
abstract_literal('is/2', is(X, Y), Poly_call, Poly_succ) :-
243+
%% Once again, we are keeping it simple
244+
poly_add_constraint(Poly_call, X=Y, Poly_succ).
245+
abstract_literal('>=/2', >=(X, Y), Poly_call, Poly_succ) :-
246+
poly_add_constraint(Poly_call, >=(X,Y), Poly_succ).
247+
abstract_literal('>/2', >(X, Y), Poly_call, Poly_succ) :-
248+
abstract_literal('>=/2', '>='(X, Y+1),Poly_call, Poly_succ).
249+
abstract_literal('=</2', =<(X, Y), Poly_call, Poly_succ) :-
250+
abstract_literal('>=/2', '>='(Y,X),Poly_call, Poly_succ).
251+
abstract_literal('</2', <(X, Y), Poly_call, Poly_succ) :-
252+
abstract_literal('>/2', '>'(Y,X), Poly_call, Poly_succ).
253+
```
254+
255+
@section{Other Auxiliary Predicates and Input-Output Operations}
256+
257+
Finally, a number of extra predicates can be defined. Among those, the
258+
following are predefined but may need to be redefined.
259+
260+
@subsubsection{@var{needs(+Option)}}
261+
262+
Succeeds if the domains needs an operation @var{+Option} for termination
263+
or correctness. The supported operations are:
264+
265+
@begin{enumerate}
266+
@item @tt{widen} : whether widening is necessary for termination,
267+
@item @tt{clauses_lub} : whether the lub must be performed over the
268+
abstract substitution split by clase,
269+
@item @tt{aux_info} :whether the information in the abstract
270+
substitutions is not complete and an external solver may be
271+
needed,currently only used when outputing the analysis in a
272+
@tt{.dump} file.
273+
@end{enumerate}
274+
by default it is assumed that nothing is needed. However, we will set widen as needed in this case.
275+
276+
@subsubsection{@var{asub_to_native(+ASub,+Qv,+OutFlag,-NativeStat,-NativeComp}}
277+
278+
@var{NativeStat} and @var{NativeComp} are the list of native (state
279+
and computational, resp.) properties that are the concretization of
280+
abstract substitution @var{ASub} on variables @var{Qv} for the
281+
domain. These are later translated to the properties which are visible
282+
in the preprocessing unit.
283+
284+
@subsubsection{@var{input_interface(+Prop, +Kind, ?Struct0, -Struct1)}}
285+
@var{Prop} is a native property that is relevant to domain
286+
(i.e., the domain knows how to fully --@var{+Kind}=perfect-- or
287+
approximately --@var{-Kind}=approx-- abstract it) and
288+
@var{Struct1} is a (domain defined) structure resulting of
289+
adding the (domain dependent) information conveyed by @var{Prop}
290+
to structure @var{Struct0}. This way, the properties relevant to
291+
a domain are being accumulated.
292+
293+
@subsubsection{@var{input_user_interface(+Struct, +Qv, -ASub, +Sg, ?MaybeCallASub)}}
294+
@var{ASub} is the abstraction of the information collected in
295+
@var{Struct} (a domain defined structure) on variables
296+
@var{Qv}.
297+
298+
```ciao
299+
needs(widen) :- !.
300+
301+
asub_to_native(ASub, _, _, [ASub], []).
302+
303+
input_interface(_Prop, _Kind, _Struct0, _Struct1) :- fail.
304+
305+
input_user_interface(Struct, Qv, ASub, _, _) :- topmost(Qv, Struct, ASub).
306+
```
307+
").

0 commit comments

Comments
 (0)