[PDF] invest in 7 eleven
[PDF] investigatory project in physics for class 12 cbse pdf
[PDF] investing in hilton hotels
[PDF] investment grade rating
[PDF] investor pitch presentation example
[PDF] investor presentation (pdf)
[PDF] investor presentation ppt template
[PDF] invité politique dimanche france inter
[PDF] invité politique matinale france inter
[PDF] invoice declaration
[PDF] involuntary servitude
[PDF] inward mc delivered no signature
[PDF] io sono francese in inglese traduzione
[PDF] iodine test for starch
[PDF] iodoform test for alcohols
Invertible Linear Transforms of
Numerical Abstract Domains
Francesco Ranzato
[0000000301590068]and Marco Zanella Dipartimento di Matematica, University of Padova, Italy Abstract.We study systematic changes of numerical domains in abstract in- terpretation through invertible linear transforms of the Euclidean vector space, namely, through invertible real square matrices. We provide a full generalization, including abstract transfer functions, of the parallelotopes abstract domain, which turns out to be an instantiation of an invertible linear transform to the interval ab- straction. Given an invertible square matrixMand a numerical abstractionA, we show that for a linear programP(i.e., using linear assignments and linear tests only), the analysis using the linearly transformed domainM(A)can be obtained by analysing on the original domainAa linearly transformed programPM. We also investigate completeness of abstract domains for invertible linear transforms. In particular, we show that, perhaps counterintuitively, octagons are not complete for45degrees rotations and, additionally, cannot be derived as a complete refine- ment of intervals for some family of invertible linear transforms.
1 Introduction
In abstract interpretation [
6 7 ], the choice of an abstract domain determines which pro- gram properties will be analysed as well as the precision and efficiency of the corre- sponding program analysis. A vast array of abstract domains for analysing properties of numerical program variables is available as well as a number of operators for their com- bination, refinement and transformation which have been defined since the beginning of abstract interpretation [ 6 7 9 10 11 12 ] - see [ 18 ] for a recent and comprehensive tutorial on numerical abstract domains. The abstract domain of parallelotopes has been introduced and studied in [ 1 2 3 4 ] as a linear transform of the standard interval abstract domain [ 6 ]. Any invertiblennreal matrixMdefines a domain ofM-parallelotopes which consists of (vectors of) intervalsh[li;ui]ini=1, forl;u2(R[ f1g)n, whose concrete meaning is recast as the set of vectorsx2Rnsuch thatlMxu. The basic idea is that the matrixMrepresents a change of basis of the Euclidean vector spaceRn, which can be always converted back through its inverse matrixM1. Hence, h[li;ui]ini=1is a symbolic representation of the vectorsfx2RnjlMxugin the new coordinate system based onM, which is therefore its concretization for the parallelotopes domain. Parallelotopes can be used in program analysis in two different ways. In the first approach described in [ 1 2 ], the matrixMis fixed and is purposely synthesized for a ofP, typically a variation of principal component analysis. On the other hand, [3,4] put forward a program analysis where the abstract values are pairs consisting of an interval together with a matrixM, so that here the matrix is not computed a priori but rather the abstract transfer functions may change it during program analysis (as happens for convex polyhedra). We study here a generalization of the first approach to the abstract domain of paral- lelotopes. An invertible square matrixMcan be applied for systematically transforming any numerical abstract domainAtogether with all its abstract transfer functions. This is called an invertible linear transform ofAand denoted byAM. This linear transformM preserves the whole structure of the abstract domainA, meaning that ifAis defined by a Galois connection/insertion then this also holds forAM, although thisM-transform may also preserve domains defined through a concretization map only. Furthermore, it turns out thatMsystematically transforms the abstract transfer functions available in A. More precisely, for the standard abstract transfer functions and operators used in abstract interpretation, namely, lub and glb, (single, parallel and backward) assignment, Boolean test, widening and narrowing, we provide a simple technique for designing the abstract transfer functions in the transformed domainAMin terms of the abstract transfer functions in the original domainA. Moreover, this transform of abstract func- tions preserves all their significant properties: soundness, best correct approximation, completeness and exactness. As a consequence, we show that an analysis with the trans- is obtained fromPby transforming all its linear assignments and tests while maintain- ing the same control flow graph. It should be remarked that this program change may transform single linear assignments ofPinto parallel linear assignments inPM. If the analysis inAof the transformed programPMrelies on abstract transfer functions which are best correct approximations then this technique computes at each program point ofPMprecisely the best abstract value forAMat the same program point ofP. This technique is illustrated through a couple of examples different from parallelotopes, namely linear transforms of constant propagation and octagon analysis.
As an example, a linear transform of Kildall"s [
15 ] standard constant propagation domainConstfor three program variables through the invertible matrixM= 1 0 0 1 1 0 1 0 1 results in a transformed domainConstMwhich is able to represent program invariants of typex1=k1,x1+x2=k2,x1+x3=k3, wherexi"s are variables andki"s range inConstand therefore represent either a constant value or unreachability or no information. For instance, an analysis based onConstMof the following program: x
1:= 2;x2:= 3;x3:= 6;
while(x2< x3)do fx1:=x12;x3:=x1+x2+x31;x2:=x2+ 2;g is able to compute the abstract loop invarianth>;5;8imeaning that the additionsx1+ x
2andx1+x3are always equal to, respectively,5and8.
We also investigate completeness and exactness [
7 13 ] of abstract domains for in- vertible linear transforms. Firstly, we show that a linearly transformed domainAMis useless - meaning that it is equivalent toAitself - precisely whenAis both com- plete and exact for the linear transformM. In particular, as expected, it turns out that 2 any linear transform of Karr"s [14], templates [19] and convex polyhedra [8] abstract domains is ineffective. Instead, we prove that a linear transformMof intervals and octagons [ 17 ] is useless exactly whenMis a monomial matrix, namely each row and column ofMhas exactly one nonzero entry. This characterization is expected since monomial matrices intuitively encode nonrelational linear transforms. Finally, we show that octagons cannot be obtained from intervals as the minimal refinement which is complete for some family of invertible linear transforms (this is called complete shell in [ 13 ]). This is somehow against the graphical intuition that octagons are complete for rotations of 4 radians and therefore could be designed through a complete shell of intervals for this family of rotations. Rather, this intuition holds just in 2D, namely for two variables only. What we instead prove is that octagons can be synthesized through a suitable reduced product of 4 rotations of intervals.
Due to lack of space all the proofs are omitted.
2 Background
Linear Transformations.We denote byRthe set of real numbersRaugmented with +1and1, where ordering and numeric operations are extended fromRtoRin the standard way. Vectorsx2Rn(orx2R n) are usually intended as column vectors, whilexTdenotes the corresponding (transpose) row vector andxi2R, withi2[1;n], denotes itsi-th component. Ifx;y2Rnanda2Rthenxy,x+yandaxdenote, respectively, scalar product, addition of vectors and scalar multiplication inRn. The canonical orthonormal basis ofRnis denoted byhe1;:::;eni, whereeii= 1and, for anyj6=i,eij= 0.Rmndenotes the set of allmnmatrices with entries inR, while GL(n)denotes the general linear group ofnninvertible square matrices with entries inR.0n2Rnndenotes the square zero matrix,In2GL(n)denotes the identity matrix andA1andATdenote, respectively, the inverse and transpose ofA. A1n matrix is also used as a row vector, while an1matrix as a column vector. A linear transformation of then-dimensional Euclidean spaceRnis a function inRn!Rnof the formx7!Mx, whereM2Rnn, which is simply denoted byM:Rn!Rn. Given any setX2}(Rn), we use the notationMX,fMx2Rnjx2Xg to denote the pointwise extension ofM, and we also useTM:}(Rn)!}(Rn)to denote the corresponding function on sets of vectors. Noteworthy examples of linear transformations include scalings, rotations, shearings and projections. Linear transfor- mationsMare partitioned between noninvertible and invertible: for example, (orthog- onal or oblique) projections are noninvertible while rotations are always invertible. The set of invertible linear transformations ofRnendowed with function composition forms the well-known (noncommutative) general linear groupGL(n). Let us also recall that
MXY,XM1Yalways holds for anyM2GL(n).
An affine transformation ofRnis a composition of a linear transformation with a transalation, i.e., it is a function inRn!Rnof the formx7!Nx+t, where N2Rnnandt2Rn. A pure translationTrt(x),x+t, for some vectort2Rn, is the simplest example of (invertible) affine transformation. Notable Linear Transformations.Ascalingby a vectors2Rnis the linear transfor- mationx7!Dsx, whereDs2Rnnis the diagonal matrix defined by(Ds)ii,si and fori6=j,(Ds)ij,0. A scaling transform is invertible iff for anyi,si6= 0. 3
Shearing
ABC D7! A 0B 0C 0D 0 x01 x02 =1 cot() 0 1 x 1 x 2
RotationABC
D7! A 0D 0C 0B 0 x01 x02 =cossin sincos x 1 x 2 Fig.1: An example of shearing and rotation transforms for two variables. Letn2. Given some2Randa;b2[1;n]witha6=b, the invertible shear matrixSha;b;2GL(n)is defined as follows:(Sha;b;)ii= 1,(Sha;b;)ab=, oth- erwise(Sha;b;)ij= 0. This defines an invertible linear transformation calledshearing (often used in computer graphics) which preserves the area of geometric figures and the alignment and relative distances of collinear points (a 2D example is in Fig. 1 ). The inverse ofSha;b;is simply the shearingSha;b;and, in general, shearings are not closed w.r.t. composition and their composition is not commutative. AGivens rotation(or principal rotation) is the linear transformation which maps x2Rninto the pointx02Rnobtained by rotatingxcounterclockwise in a(a;b) plane ofRn(i.e., generated byeaandea), wherea;b2[1;n]witha6=b, by an angle of2Rradians around the origin (a 2D example is in Fig.1 ). This transformation is represented by an invertible Givens rotation matrixRa;b;2GL(n)which is defined as follows:Ra;b;differs from the identity matrixInin the four entries(a;a),(a;b),(b;a), (b;b), where it assumes, respectively, the valuescos,sin,sin,cos. Clearly, R a;b;is the inverse ofRa;b;. Givens rotations are closed by composition and When the rotation angle is= (2)=mfor somem2N rf0g, it turns out thatRa;b;is cyclic, namely(Ra;b;)k=Infor some integerk >0. Numerical Abstract Domains.According to the most general definition, a numerical abstract domain is a tuplehA;; iwherehA;iis at least a preordered set and the concretization function :A!}(Rn), wheren1, preserves the relation, i.e., aa0implies (a) (a0). Thus,Aplays the usual role of set of symbolic rep- resentations for sets of vectors ofRn. If the base field of real numbersRis replaced by the field of rationalsQ, which is a possible choice for an abstract interpretation framework (see [ 18 ]), then completeness of the latticehR;iis lost (i.e.,hQ;iis not a complete lattice) so that some linear transformations cannot be taken into ac- count, e.g., a Givens rotation of=4. Also, linear transformations preserving integer vectors inZn(then-dimensional integer lattice) have a narrow scope (they are studied in lattice geometry) and are not considered here (see [ 2 , Section 7.5] for a discussion). Well-known examples of numerical abstract domains include signs, constants, inter- vals, affine equalities, zones, pentagons, octagons, parallelotopes, templates, convex polyhedra (the interested reader is referred to the recent tutorial [ 18 ]). Some numerical 4 domains just form preorders (e.g., standard representations of octagons by DBMs allow multiple representations) while other domains give rise to posets (e.g., signs, constants and intervals). Of course, any preordered abstract domainhA;; ican be canonically quotiented to a posethA==;; iwherea=a0iffaa0anda0a. While a mono- tone concretization is enough for reasoning about soundness of static analysis on numerical domains, the notions of best correct approximation and completeness rely on the existence of an abstraction function:}(Rn)!Awhich requires thathA;i is (at least) a poset and that the pair(; )forms a Galois connection (GC), i.e. for anyXRn;a2A,(X)a,X (a)holds, which becomes a Galois in- sertion when is injective (or, equivalently,is surjective). Most numerical domains admit a definition through Galois connections, while for some domains this is impossi- ble, notably for convex polyhedra. Let us recall that the nonrelational interval domain
Int=hInt;;
;iis defined by:Int,fh[li;ui]ii2[1;n]jli;ui2R; liuig [ ?, (h[li;ui]ii2[1;n]) =fx2Rnj 8i2[1;n]: lixiuig, (?) =?, and (X),hinfx2Xxi;supx2Xxiii2[1;n]. A functionf]:A!Ais a sound approximation of a concrete (transfer) function f:}(Rn)!}(Rn)when, for anya2A,f( (a)) (f](a))holds, whilef] is forward-complete (or f-complete or exact) whenf f]holds. Assume that a Galois connection(; )forAexists. The abstract functionfA,f is called the best correct approximation (bca) offonA. Also, soundness off]can be equivalently stated by(f(X))f]((X)), for anyX2}(Rn), whilef]is defined to be backward-complete (or b-complete or just complete) whenf=f]holds.
3 Linear Transforms of Abstract Domains
Linear transformations can be used to recast any existing numerical abstract domains: an invertible linear transformation performs a change of basis of then-dimensional Euclidean spaceRnand the transformed abstract domain is accordingly interpreted with this transformed coordinate system.
Definition 3.1
(Linear T ransformof Abstractions). Consider any invertible matrix
M2GL(n)and a numerical abstract domainA=hA;;
i. TheM-transformofA is given byAM,hA;; Mi, also denoted byM(A), where the concretization map
M:A!}(Rn)is defined by
M(a),M1
(a). IfAadmits an abstraction map :}(Rn)!AthenAMis also endowed with a functionM:}(Rn)!Adefined byM(X),(MX).ut
Equivalently, we have that
M=TM1 andM=TM. The basic idea is that the invertible matrixMrepresents a change of basis forRn, which can be always converted back through its inverse matrixM1. According to this view, an abstract valuea2Abecomes a symbolic representation of the set of vectors (a)2}(Rn) in the new coordinate system based onM, so that the concretization
Mofain the
original coordinate system ofRnis given by the conversion of (a)throughM1 back to the original basis ofRn, namely
M(a) =M1
(a)2}(Rn). Dually, if Aadmits an abstraction function, so thathA;iis (at least) partially ordered, then A Malso has an abstraction mapMwhich provides the best approximation of some 5 M(X) =(MX). Hence, Definition3.1 is a straightforw ardgeneralization of the parallelotope domain defined in [ 2 , Definition 2], since a parallelotope domain indexed byM2GL(n)boils down to theM-transform of the interval abstractionInt. IfAis a numerical domain equipped with a concretization map only, thenAMis clearly a sound numerical domain, since we just need to check that
Mstill preserves
the relationonA: ifaa0then (a) (a0), so that
M(a) =M1
(a) M 1 (a0) = M(a0). Moreover, any order-theoretic property of the abstract domain Ais obviously preserved when interpreted in itsM-transform, e.g., bottom and top elements, lub"s and glb"s, chains, etc. It is also easy to observe that linear transforms of numerical domains also preserve the existence of abstraction maps.
Lemma 3.2.IfA=hA;;
;iis a Galois connection (insertion) then itsM-trans- formAM=hA;;
M;Miis a Galois connection (insertion).
Example 3.3 (Linear Transform of Constant Propagation)Constant propagation is a well-known and simple abstract interpretation used in compiler optimization for de- tecting whether a variable at some program point always stores a single constant value for all possible program executions (see, e.g., [ 18 , Section 4.3]). Constant propagation relies on the nonrelational constant abstract domain, which is here given for variables assuming real values:Const,R[f?;>g.Constis endowed with the usual flat partial order: for anyx2Const,? x >(andxx), which makes it an infinite com- plete lattice with height 2.Constis easily defined by a Galois insertion with its standard abstraction and concretization maps:}(R)!Constand : Const!}(R). (X),8 :?ifX=? zifX=fzg >otherwise (a),8 :?ifa=? fagifa2R
Rifa=>
1 0 0 1 1 0 0 0 1 1 0 0 0 1 0 1 0 1 1 0 0 1 1 0 1 0 1 which is obtained as composition of the two shearing matricesSh2;1;1andSh3;1;1.
Its inverse isS1=
1 0 0 1 1 0 1 0 1 . Let us considerConstfor three variables, namely as an abstraction of}(R3). The matrixSthus induces the transformed domainConstS, where a vectorha1;a2;a3i 2ConstS, by Definition3.1 , has the following meaning:
S(ha1;a2;a3i) =S1
(ha1;a2;a3i) = fhz1;z1+z2;z1+z3i 2R3jz12 (a1);z22 (a2);z32 (a3)g: Moreover, ifki2RthenS(fhk1;k2;k3ig) =(Shk1;k2;k3i) =(fhk1;k2 k
1;k3k1ig) =hk1;k2k1;k3k1i. For instance, ifki2Rthen
S(h>;k2;k3i) =
fhz;z+k2;z+k3i jz2Rg,
S(hk1;>;k3i) =fhk1;z;k1+k3i jz2Rg, while
S(fh1;0;1i;h1;1;3ig) =h>;>;2iandS(fh1;0;1i;h1;2;3ig) =h>;1;2i. This abstractionConstSis therefore able to represent invariants for program variables x iof typex12 (a1)^x1+x22 (a2)^x1+x32 (a3), whereai2Const. For instance, for the following programPalready considered in Section1 and here decorated with program points: 6 (1)x1:= 2;x2:= 3;x3:= 6; (2) while(3)(x2< x3)do (4)x1:=x12; (5)x3:=x1+x2+x31; (6)x2:=x2+ 2; od(7) while a constant analysis withConstderives no information at program point (3), namely the abstract valueh>;>;>i, we expect that an analysis based onConstSis able to compute the abstract valueh>;5;8iwhich represents that at program point (3) the additionsx1+x2andx1+x3are always equal to, respectively,5and8.ut
4 Linear Transforms of Abstract Functions
Background.An abstract interpretation-based static analysis of programs with numeric variables relies on sound approximations of the standard transfer functions on the con- crete domain}(Rn)used by the collecting program semantics (see, e.g., [18]): binary set unions and intersections, variable assignments, Boolean tests, widening and narrow- ing operators. Let us briefly recall the definitions for assignments and tests. The most general form of variable assignment is given by a parallel (or simultane- ous) assignment[xi:=fi(x)]i2[1;n](as in Python and JavaScript), with generic (pos- sibly nonlinear) functionsfi:Rn!Rwhich define an-dimensional transformf: R n!Rnbyf(x),hf1(x);:::;fn(x)i. The transfer functionassign(f) :}(Rn)! }(Rn)is the corresponding pointwise extension offdefined byassign(f)(X), ff(x)jx2Xg. Ifi2[1;n]andf:Rn!Rthen a single assignmentxi:=f(x) for thei-th variable is defined byassign(i;f) :}(Rn)!}(Rn)as the following specific instance:assign(i;f)(X),fhx1;:::;xi1;f(x);xi+1;:::;xni jx2Xg. Linear parallel assignments rely on a square matrixN2Rnnand a vectorb2 R nwhich define the transfer functionassign(N;b) :}(Rn)!}(Rn)as follows: assign(N;b)(X),fNx+bjx2Xg. As a particular case, linear (single) assign- ments for thei-th variable consider a vectora2Rnand a constantb2Rwhich define the affine transformationx7!(eiaT)x+beiwhose corresponding transfer function is assign(i;a;b),assign(ei(aei)T+I;bei), namely, assign(i;a;b)(X) =fhx1;:::;xi1;ax+b;xi+1;:::;xni jx2Xg: Let us also recall backward assignment, namely the adjoint of a (forward) assignment, which is typically used in backward abstract interpretation [ 5 ] for refining the output of a forward abstract interpretation. In general, the transfer functionassign(f) : }(Rn)!}(Rn)of the backward parallel assignment for[x:=f(x)]is simply given by the inverse imageassign(f)(Y),f1(Y) =fx2Rnjf(x)2Yg, so that for a single assignmentxi:=f(x), we have thatassign(i;f)(Y),fx2 R nj hx1;:::;f(x);:::;xni 2Yg. In turn, the transfer function of the backward linear parallel assignment forN2Rnnandb2Rnisassign(N;b) :}(Rn)!}(Rn) defined byassign(N;b)(Y),fx2RnjNx+b2Yg. A nondeterministic assignment for thei-th variablexi:= ?is modeled by the transfer functionforget(i) :}(Rn)!}(Rn)defined as follows:forget(i)(X), 7 fhx1;:::;xi1;z;xi+1;:::;xni jx2X; z2Rg. This can be viewed as an instance of a more general functionforget(v) :}(Rn)!}(Rn)indexed by a vectorv2Rn and defined byforget(v)(X),fx+zvjx2X; z2Rg. Thus, it turns out that forget(i)can be retrieved by consideringv=ei, that is,forget(i) =forget(ei). The most general form of Boolean test considers any predicatep:Rn! ft;fgand selects those program states that make the predicateptrue. This is modeled by a transfer functiontest(p) :}(Rn)!}(Rn)defined bytest(p)(X),X\ fx2Rnjp(x) = tg. A linear Boolean test is defined by a matrixN2Rmn, a vectorb2Rmand some comparison relation./RmRm, here used in infix notation, which define a transfer functiontest(N;b;./) :}(Rn)!}(Rn)as follows:test(N;b;./)(X), X\ fx2RnjNx./bg. As a particular case, we have that ifa2Rnandb2Rthen test(a;b;./)(X),X\ fx2Rnjax./ bg. Linear Transforms.Let us consider how abstract operations can be defined on a lin- ear transform of a numerical abstract domain. Consider a numerical abstract domain
A=hA;;
i, possibly endowed with an abstraction function. Consider any con- crete transfer functionf:}(Rn)!}(Rn)and a corresponding abstract transferquotesdbs_dbs20.pdfusesText_26
[PDF] Invertible Transformations and Isomorphic Vector - Sites at Lafayette