Formalisation and Static Analysis of CSS3 Selectors

Matthew Hague   Anthony Widjaja Lin

Royal Holloway, University of London   Yale-NUS College, Singapore

Abstract: Cascading Style Sheets (CSS) is the de facto language for styling a webpage, as developed and maintained by World Wide Web Consortium (W3C). Together with HTML and JavaScript, CSS has played an integral role in modern web technologies. At the heart of CSS are CSS selectors, which are formal specifications of which nodes in a given document object model (DOM) are to be selected for declarations of certain visual properties (e.g. set colour to red). Despite the apparent simplicity of CSS selectors, CSS selectors allow many complex features, e.g., tree traversals, string constraints on attributes, constraints for counting the number of children, and restricted negations. This paper describes the first precise formalisation of CSS Level 3 (CSS3) selector language, currently the stable version of the language. Unlike previous formalisations, our formalisation attempts to capture CSS3 in its entirety, as specified in the latest W3C Recommendation. We then study two fundamental static analysis problems which have found applications in optimisation of CSS files: (1) satisfiability: given a CSS selector, decide whether it can ever select a node in some DOM tree (2) intersection: given two CSS selectors, decide whether they can ever select the same node in some DOM tree. The second problem, in particular, has immediate applications in minimisation of CSS files by refactoring similar styling rules. We show that they are decidable and, in fact, NP-complete. Furthermore, we show that both problems can be reduced in polynomial-time to satisfiability of quantifier-free Presburger formulas, for which highly optimised SMT solvers are available.

1  Introduction

Cascading Style Sheets (CSS), together with HTML and JavaScript, has been a cornerstone language for the web since its inception in 1996. The language facilitates a clear separation between presentation and web content, and plays a pivotal role in the design of a semantically meaningful HTML.

CSS is widely perceived to be a simple language. One simply needs to define a sequence of (styling) rules, each containing a set of (node) selectors (e.g. h1, h2, which select h1 and h2 HTML elements in a given document) and a set of property declarations (e.g. font-weight: normal; and margin-bottom: 10px;) that will be assigned to all selected nodes1. The power of CSS comes from its powerful selectors in that they can express navigational properties over web documents, constraints for counting the number of children, string constraints for reasoning about attributes, conjunctions, and negations, to name a few. For example, the CSS selector

selects all nodes with class .moon but not class .water such that it has an ancestor with class .planet such that it is the ith child of the parent where i ≡ 1 (mod 7 ). In this respect, CSS selectors exhibit a striking similarity to XPath [1] which is a popular query language for selecting nodes or node-sets in an XML document. Both CSS and XPath are defined and maintained by World Wide Web Consortium (W3C).

Despite the apparent simplicity of the language, CSS selectors can be quite subtle. For example, let us take the latest evolution of the CSS language, i.e., CSS3 [7]. Consider the following properties over web documents:

  1. An element div with at least one child
  2. An element div with no more than three children
  3. An element div with at least one child with class .a.
  4. An element with class .a, and it is the second child, and it does not have a sibling at position 3.
  5. An element h3 with an ancestor with an ID attribute that matches the regular language (ab)*.
  6. An element h2 whose ID attribute matches the regular language (aa)*.

It might come as a surprise that (1), (4), (5) are expressible as CSS selectors, while (2), (3), and (6) are not expressible as CSS selectors. [See Remark 1 for why Property (6) is not expressible.] Again, it might come as a surprise that (3) is in fact expressible in the XPath query language2. This suggests that the resemblance to XPath, whose expressivity issues have received a lot of attention in databases [21, 22, 32, 33, 31], is again not as straightforward.

In recent years there have been a lot of work on static analysis and optimisation/minimisation of CSS styling rules in HTML applications, e.g., [12, 24, 6, 23, 14, 29]. Such work has been motivated by the well-known issues of CSS bloat — typically caused by HTML plugins with generic style sheets and CSS preprocessors, to name a few — whose amount has been estimated to be around 60% on average for typical industrial applications [24]. The latest W3C Recommendation of CSS Selectors Level 3 [7] gives an informal, natural language specification (more than 30 pages in printed form), which is not easy to work with when developing static analysis and optimisation tools for CSS. For this reason, researchers have attempted to develop concise formalisations of the CSS selector language, e.g., in µ-calculus [12].

Despite the amount of work in developing practical static analysis and optimisation tools for CSS, many basic foundational issues for static analysis of CSS have remained unsolved. Perhaps the simplest and the most fundamental static analysis problem for CSS concerns the decidability of satisfiability (a.k.a. non-emptiness) of CSS3 selectors: given a CSS selector, check whether it is satisfiable (i.e. the selector may match some node in some tree). If decidable, what is its computational complexity? Satisfiability often forms a basis of other static analysis problems. One such static analysis problem that is of immediate practical importance concerns the non-disjointness (a.k.a. intersection) problem for the CSS3 selectors: given two CSS selectors, decide whether they can simultaneously select the same node on some tree. Decidability and complexity for the intersection problem for CSS is currently not known. A solution to this problem is required to be able to perform CSS file minimisation [23] via the reordering and merging of styling rules (see Section 2 for an example). In particular, if two styling rules match the same node, the order of declarations in a file can determine the appearance of the document. To be able to safely reorder two rules, one must be sure that the selectors of the two rules will never match the same node in a tree. Existing solutions (e.g. [23]) only overapproximate the order dependency relation. A more precise relation would allow more CSS rules to be reordered (and therefore optimised).

Finally, we shall remark that these questions are not only of theoretical interest, but they are also useful for actual static analysis tools, which currently cannot handle the CSS selector language in its entirety (e.g. [6] handle ∼ 70% of the selectors from their benchmarks). Part of the problem seems to be that hitherto there is no formalisation of CSS3 selectors as specified in the W3C Recommendation [7]. For example, the tree logic defined in [12] can express Property (3) above, which is not expressible as a CSS3 selector, but did not incorporate constraints on attributes (i.e. strings).

Contributions.

In this paper we present a 1.5-page formalisation of the CSS3 selector language. Unlike previous formalisations, our formalisation attempt captures CSS3 in its entirety, as specified in the latest W3C Recommendation [7]. In particular, our formalisation models CSS3 constraints on attributes (i.e. strings), which yields semantics of CSS selectors as a set of finite “data trees” (i.e. whose node labels range over an infinite set). Equipped with the new formalisation, we then study the two aforementioned fundamental static analysis problems for CSS3: (1) satisfiability (a.k.a. non-emptiness) of CSS3 selectors, and (2) non-disjointness (a.k.a. non-emptiness-of-intersection, or simply “intersection”) of two CSS3 selectors. We show that both problems are decidable and, in fact, NP-complete. This is in contrast to the previous formalisation of CSS selectors as a tree logic (which do not cover CSS3 in its entirety), in which both problems would be EXPTIME-complete.

With a very simple set of navigational axes (i.e. up, left, but neither down nor right), it might be a surprise that CSS satisfiability is NP-hard especially in the light of the polynomial-time solvability result for satisfiability for the XPath fragment3 that uses only this set of navigational axes, e.g., see [15]. It turns out that one cause of this NP-hardness is CSS selectors’ ability to do modulo arithmetic, conjunctions, and restricted negations; these can be used to encode the satisfiability of intersections of negations of arithmetic progressions, which is known to be NP-complete [30].

For the upper bound, we show that both problems can be reduced in polynomial-time to satisfiability of existential Presburger formulas, for which highly optimised SMT solvers are available. Our result suggests the potential application of SMT solvers for providing an efficient solution for static analysis of CSS3 selectors. Several tricky features of CSS3 that have to be handled in this reduction includes constraints for counting the number of children (which could express the existence of exponentially many children in the tree), built-in regular string matching constraints for the attribute values, uniqueness of id attributes in the tree, conjunctions, and restricted negations. A careful analysis of the language is required in pinpointing the exact computational complexity. For example, if CSS3 were to allow unrestricted unrestricted regular string matching constraints, it would be able to encode intersection of regular languages, which is PSPACE-complete [16].

Related Work.

Although there has not been much work on the foundation of CSS, a lot of fundamental work exists on its cousin XPath. The first formalisation of XPath was given by Wadler [34]. Database researchers then developed several the core logical versions of the language that allows them to study expressiveness and static analysis issues in a cleaner setting, e.g., see [21, 5, 13, 32, 33, 31, 22]. To obtain a cleaner version of XPath, one often makes the assumption that there are only finitely many attribute values, which is not true for XPath in its entirety. XPath is also known to share many similarities to logics and automata over unranked trees, e.g., see [18] for a readable survey on this. Many results on the decidability and complexity of static analysis of XPath in this setting (with or without DTDs, and possibly with some navigational directions disallowed) are available, e.g., see [15, 4, 26, 10, 20, 11]. Note that the static analysis problems for CSS that we consider in this paper do not come with a schema (e.g. in DTD), which is also the case for most existing work in static analysis and optimisation/minimisation on CSS [12, 24, 6, 23, 14, 29]. As we previously mentioned, if one were to make a similar simplification (e.g. finitely many attributes, no global id constraints, and no modular counting constraints on the number of children), CSS would be an XPath fragment in the database setting with only upward and leftward navigational combinators, which is known to be polynomial-time solvable [15]. This is in contrast to our NP-completeness for satisfiability for CSS3 selectors. The simplified setting of XML has recently been extended (e.g. see [9]) to models that allow reasoning of attribute values (from an abstract infinite domain), but this mostly results in models whose satisfiability problems exhibit high computational complexity (at least EXPTIME-hard) since they allow general comparisons of data values.

We also mention the work on automata on unranked trees (labels in the trees from a finite alphabet) that allow counting constraints on the number of children, e.g., see [28]. Such work typically allow counting constraints that are much more complex than what CSS3 allow, which is the reason for that checking emptiness for such automata is PSPACE-complete.

Organisation.

Section 2 provides a CSS primer. We fix mathematical notation and terminologies that we use throughout the paper in Section 3. Section 4 provides a formalisation of CSS3 selectors. In Section 5 we provide an overview of results on satisfiability and intersection of CSS3 selectors and, in particular, proofs of the NP lower bounds. Section 6 and 7 develop the machinery for proving an NP upper bound for these problems. We conclude with future work in Section 8. See Appendix for omitted details.

2  CSS By Example

We give a brief overview of CSS selectors and motivate the problems studied in this paper by means of an example. We refer the readers to [2] for a gentle and more complete introduction to CSS.

A very simple web page is given in Figure 1. In this section we describe both HTML and CSS. The page contents are given by the HTML document shown in Figure 2. In Figure 3 we give the CSS file used to style the page. Although our example uses HTML, we note that CSS can also be used to identify nodes in XML trees.

2.1  Basics

HTML documents are written in a markup language that gives a tree structure. Each node in the tree is an element e. The description of the node begins with a tag ⟨e⟩ and ends with a tag ⟨/e⟩. Nodes appearing between these tags describe the children. As can be seen in Figure 2 the root of the tree is an HTML element containing two children: a head and a body. The head element contains metadata about the page, while the body element contains the page contents. The h1 element is the heading, while the table element contains the prices. Each row of the table is a tr element, and each data item is a td element.

The opening tag of some of these elements contains additional information. E.g. id=‘‘prices’’ and class=‘‘fruit’’. These are attributes that label a node. There are many possible attributes, but the id and class attributes have a special purpose for CSS selectors, as will be seen below. Note the table row containing tomatoes has two class values: fruit and vegetable.


Figure 1: An example web page.


Figure 2: The HTML DOM Tree of the web page in Figure 1

The CSS stylesheet given in Figure 3 is used to customise its appearance. The stylesheet is a list of rules, each having the form

selectors { declarations }

where selectors is a comma-separated list of selectors and declarations is a semi-colon separated list of (property) declarations. Selectors are used to identify nodes in the document tree. A rule is applied to a node if one of its selectors matches the node. Each declaration in a rule specifies how some aspect of the node is displayed.

For example, the simplest rule is the first

In this rule the selector identifies any h1 element. The declaration specifies that the background should be light green. Hence, the heading of the webpage has a light green background.

The next rule

has a selector that identifies any node whose class attribute contains “fruit”. The syntax “.” is used to specify classes. However, this is just syntactic sugar. CSS allows selectors to specify the contents of arbitrary attributes. The above rule could have been alternatively written

where ~= is an operator specifying that the attribute is a space-separated list of words, one of which is the value on the right. Similarly, #ι asserts that the id attribute is ι, or, equivalently, [id = ι].


Figure 3: A stylesheet for the webpage in Figure 1.

The selector

demonstrates several more complex features of CSS. The first thing to notice is that the selector is split into two parts: table#prices and tr:nth-child(2n + 1). These two parts put constraints on two separate nodes. The node identified by the selector is the node matched by tr:nth-child(2n + 1). The whitespace between the two parts indicates that the second (matched) node should be a descendent of the first. CSS also allows the operators >, +, and ~ to indicate a child-of, neighbour-of, and sibling-of relationship respectively.

The first part table#prices is a conjunction, asserting that the first node is both a table element and has the ID “prices”. The second part tr:nth-child(2n + 1) is also a conjunction. It asserts that the matched element is a tr element and satisfies :nth-child(2n + 1). The :nth-child(2n + 1) asserts that the node is the ιth child of its parent such that ι = 2n + 1 for some integer value n. [The leftmost child is the first, instead of zeroth, child of the parent node.] Thus, the stylesheet in Figure 3 renders even rows of the table with a normal font weight, and odd rows in bold.

2.2  Static Analysis

In this section we discuss applications of the intersection problem. Consider from Figure 3. Readers familiar with CSS might be tempted to minimise the CSS in Figure 3 by replacing the first three rules with

Here, the first rule has a comma-separated list of selectors that identify which nodes should have a light green background. Merging the rules like this avoids the declaration “background: lightgreen” appearing twice, reducing the size of the file. However, such a transformation will change the appearance of the page. In particular, the tomato row will display in yellow rather than green. This is because the tomato row matches both .fruit and .vegetable. In cases when such a conflict arises, the CSS specification first uses a notion called specificity – which is a measure easily calculated from a selector’s syntax that we will not discuss here. In this case both selectors have the same specificity so the rule appearing latest in the file is used. The optimisation proposed above changes the order of the rules in the file and as a result changes the appearance. Hence, before attempting to minimise a file by merging related rules, we must first check whether selectors may overlap. Note, since industrial CSS files may contain thousands of rules, potentially millions of (pairwise) comparisons must be performed. Hence, it is important to pinpoint the precise complexity of the problem.

3  Preliminaries

3.1  Maths

As usual, ℤ denotes the set of all integers. We use ℕ to denote the set {0,1,…,} of all natural numbers. Let ℕ>0 = ℕ ∖{0} denote the set of all positive integers. For an integer x we define |x| to be the absolute value of x. In the sequel, for a set S, we will use S* (resp. S+) to denote the set of sequences (resp. non-empty sequences) of elements from S. When the meaning is clear, if S is a singleton {s}, we will denote {s}* (resp. {s}+) by s* (resp. s+).

3.2  Trees

A tree domain is a set D ⊆ (ℕ>0) of nodes that is both prefix-closed and younger-sibling closed. That is ηι ∈ D implies both η ∈ D, and ηι′ ∈ D for all ι′ < ι.

A Σ-labelled tree is a pair T = (D, λ) where D is a tree domain, and λ : D → Σ is a labelling function of the nodes of T.

Next we recall terminologies for relationships between nodes in trees. To avoid notational clutter, we deliberately choose notation that resembles the syntax of CSS. In the following, take η, η′ ∈ D. We write η ≫ η′ if η is a (strict) ancestor of η′, i.e., there is some η″ ∈ ℕ>0+ such that η′ = ηη″. We write η > η′ if η is the parent of η′, i.e., there is some ι ∈ ℕ>0 such that η′ = η ι. We write η + η′ if η is the direct younger sibling of η′, i.e., there is some η″ and ι ∈ ℕ>0 such that η = η″ ι and η′ = η″ (ι − 1). We write η ∼ η′ if η is a younger sibling of η′, i.e., there is some η″ and ι, ι′ ∈ ℕ>0 with ι < ι′ such that η = η″ ι′ and η′ = η″ ι. Finally, є is the root node in any tree.

3.3  Existential Presburger Arithmetic

Recall that Presburger arithmetic is a first-order theory for reasoning about integer linear arithmetic [17]. In the sequel, we will only use the existential fragment of the theory (a.k.a. existential Presburger arithmetic), which is well-known to be NP-complete [27]. Formulas θ of existential Presburger arithmetic have the form

    θ, θ′ = E ∼ E  
  ∃ x . θ  
  θ ∧ θ′  
  θ ∨ θ′

where ∼ ∈ {=, >, ≥, <, ≤} and E are (integer) expressions E of the form a0 + a1x1 + ⋯ + anxn where each ai is an integer (with a binary representation) and each xi denotes an (integer) variable. We assume a standard semantics of Presburger arithmetic. Note, the existential operator ∃ quantifies over non-negative integers ℕ. We will implicitly assume that all free variables are existentially quantified. Moreover, we will occasionally allow quantification over a finite set of elements. It is straightforward to encode this into a quantification over integers of a bounded range.

4  Formalisation of DOM and CSS

In this section we give a formal definition of document trees and CSS3 selectors. Our formalisation follows the latest version of W3C recommendation of CSS3 selectors [7].

4.1  Definition of Document Trees

In this section we introduce Documents Objects Models (DOMs), which we also refer to as document trees. A document consists of a number of elements, which in turn may have sub-elements as children. Each node in the tree is given a type consisting of an element name and a namespace. For example an element P in the HTML namespace is a paragraph in an HTML document. In addition each node may be labelled by attributes. Each attribute is identified by a namespace (which may differ from that of the node) and an attribute name. The attributes take string values. Finally, a node may be labelled by a number of pseudo-classes which specify properties of the node in the document. For example :enabled means that the node is enabled and the user may interact with it, while :empty indicates that the node has no children. The set of pseudo-classes is fixed by the CSS specification.

In the formal definition below we permit a possibly infinite set of namespace, element, and attribute names. This is because the document writer can use any string of characters as a name. Thus, the sets of possible names cannot be fixed to a finite set from the point of view of CSS selectors, which may be applied to any document.

We denote the set of pseudo-classes as

    P = 



 
:link:visited:hover:active:focus
:target:enabled:disabled:checked
:root:empty 
 



 . 

Then, given a possibly infinite set of namespaces NS, a possibly infinite set of elements E, a possibly infinite set of attribute names A, and a possibly infinite alphabet4 Γ containing the special characters ␣ and - (space and dash respectively), a document tree is a Σ-labelled tree (D, λ), where

    Σ := 
NS × E × Ffin
NS × A, Γ
× 2P

 .

Here the notation Ffin(NS × A, Γ) denotes the set of partial functions from (NS × A) to Γ whose domain is finite. In other words, each node in a document tree is labeled by a namespace, an element, a function associating a finite number of namespace-attribute pairs to an attribute value (string), and one or more of the pseudo-classes. For a function fAFfin(NS × A, Γ) we say fA(s, a) = ⊥ when fA is undefined over sNS and aA, where ⊥ ∉ Γ is a special undefined value.

Furthermore, we assume special attribute names class, idA that will be used to attach classes (see later) and IDs to nodes.

We will write s:e for an element e with namespace s in NS × E and s:a for an attribute a with namespace s in NS × A. For convenience, when λ(η) = (s, e, fA, P) we write

        λS
η
s,  λE
η
e,  λA
η
fA,  λP
η
P .

There are several consistency constraints on the pseudo-classes labelling a node.

In the sequel, we will tacitly assume that document trees satisfy these consistency constraints.

We write Trees(NS, E, A, Γ) for the set of such trees.

Note, readers familiar with HTML may have expected clauses asserting, for example, that if an node matches :hover, then its parent and “label controls” should also match :hover. However, this is part of the HTML5 specification, not of CSS3. In fact, the CSS3 selectors specification explicitly states that a node matching :hover does not imply its parent must also match :hover.

Finally, note that CSS selectors can be applied to any document tree, e.g. XML or HTML. The semantics of CSS3 from the CSS3 selector specification [7] may allow document formats that are forbidden by the HTML5 specification.

4.2  Definition of CSS3

In the following sections we define CSS syntax and semantics. In formally, as CSS selector consists of node selectors σ – which match individual nodes in the tree – combined using the operators >>, >, +, and ~. These operators express the descendant-of, child-of, neighbour-of, and sibling-of relations respectively. Note, we use slightly different syntax to their counterpart semantical operators ≫, >, +, and ∼ in order to distinguish syntax from meaning.

A node selector σ has the form τΘ where τ constrains the type of the node. That is, τ places restrictions on the namespace and element labels of the node. The rest of the selector is a set Θ of simple selectors that assert atomic properties of the node. These may take several forms.

Class and ID selectors .v and #v assert that the node has a class or ID v respectively. Note, a node may have several classes (given as a string by a space-separated list of classes) but only one ID.

The next type of simple selector is the attribute selectors that generally take the form [s|a op v] for some namespace s, attribute a, operator op ∈ {=, ~=, |=, ^=, $=, *=}, and some string v ∈ Γ. The namespace may be omitted if the specification is agnostic about the namespace of the attribute. The operators =, ^=, $=, and *= take their meaning from regular expressions. That is, equals, begins-with, ends-with, and contains respectively. The remaining operators are more subtle. The ~= operator means the attribute is a string of space-separated values, one of which is v. The |= operator is intended for use with language identification (e.g. en-GB means “English” as spoken in Great Britain). Thus |= asserts that either the attribute has value v or is a string of the form v-v′ where - is the dash character, and v′ is some string.

Attribute selectors may also take the form [s|a] or [a] to assert that the attribute is merely defined on the node.

Next, simple selectors may specify which pseudo-classes label a node. E.g. the selector :enabled ensures the node is currently enabled in the document.

There are several further kinds of pseudo-classes. Of particular interest are selectors such as :nth-child(αn + β). These assert that the node has a particular position in the sibling order. For example :nth-child(2n + 1) means there is some n ≥ 0 such that the node is the (2n + 1)th node in the sibling order. That is, the node is at an odd position.

Finally, simple selectors may be negations :not(θ) of a simple selector θ with the condition that negations cannot be nested.

4.2.1  Syntax

Fix NS, E, A, and Γ as in the previous section. We define Sel for the set of (CSS) selectors and NSel for the set of node selectors. The set Sel is the set of formulas ψ defined as:

    
ψ  ::=
ϕ  
  ϕ::first-line  
  ϕ::first-letter  
  
  
ϕ::before  
  ϕ::after 
 

where

    ϕ ::= σ  
  ϕ >> σ  
  ϕ > σ  
  ϕ + σ  
  ϕ ~ σ  
  

where σ ∈ NSel is a node selector with syntax σ ::= τ Θ with τ having the form

    τ ::= *  
  (s|*)  
  e  
  (s|e)

where sNS and eE and Θ is a possibly empty set of conditions θ with syntax

    θ ::= θ¬  
  :not(σ¬)

where θ¬ and σ¬ are conditions that do not contain negation, i.e.:

    σ¬ ::= *  
  (s|*)  
  e  
  (s|e)  
  θ¬

and θ¬ =

    
.v  
  #v  
  
[a]  
  [a = v]  
  [a ~= v]  
  [a |= v]  
  
[a ^= v]  
  [a $= v]  
  [a *= v]  
  
[s|a]  
  [s|a = v]  
  [s|a ~= v]  
  [s|a |= v]  
  
[s|a ^= v]  
  [s|a $= v]  
  [s|a *= v]  
  
:link  
  :visited  
  :hover  
  :active  
  :focus  
  
:enabled  
  :disabled  
  :checked  
  
:root  
  :empty  
  :target  
  
:nth-child(αn + β)  
  :nth-last-child(αn + β)  
  
:nth-of-type(αn + β)  
  :nth-last-of-type(αn + β) 
:only-child  
  :only-of-type 
 

with sNS, eE, aA, v ∈ Γ, and α, β ∈ ℤ. Note, we will omit Θ when is it empty.

4.2.2  Removing Pseudo-Elements

CSS selectors can also finish with a pseudo-element. For example ϕ::before. These match nodes that are not formally part of a document tree. In the case of ϕ::before the selector matches a phantom node appearing before the node matched by ϕ. These can be used to insert content into the tree for stylistic purposes. For example places a “>” symbol before the rendering of any node with class a.

We divide CSS selectors into five different types depending on the pseudo-element appearing at the end of the selector.

    
ϕ  
  ϕ::first-line  
  ϕ::first-letter  
  
ϕ::before  
  ϕ::after 
 

We are interested here in the nodes matched by a selector. The pseudo-elements ::first-line, ::first-letter, ::before, and ::after essentially match nodes inserted into the DOM tree. The CCS3 specification outlines how these nodes should be created. For our purposes we only need to know that the five syntactic cases in the above grammar can never match the same inserted node, and the selectors ::first-letter and ::first-line require that the node matched by ϕ is not empty.

Since we are interested here in the non-emptiness and non-emptiness-of-intersection problems, we will omit pseudo-elements in the sequel, under the assumptions that

In this way, we can test non-emptiness of a selector by testing its replacement. For non-emptiness-of-intersection, we know if two selectors end with different pseudo-elements (or one does not contain a pseudo-element, and one does), their intersection is necessarily empty. Thus, to check non-emptiness-of-intersection, we immediately return “empty” for any two selectors ending with different pseudo-elements. To check two selectors ending with the same pseudo-element, the problem reduces to testing the intersection of their replacements.

4.2.3  Semantics

We now define the semantics of CSS3 selectors. The semantics of a selector is defined with respect to a document tree and a node in the tree.

More precisely, the semantics of CSS3 selectors ϕ is defined inductively with respect to a document tree T = (D, λ) and a node η ∈ D as follows:

    
T, ηϕ >> σ 
def
 
∃ η′ ≫ η  . 
T, η′ ⊨ ϕ
∧ 
T, η ⊨ σ
T, ηϕ > σ 
def
 
∃ η′ > η  . 
T, η′ ⊨ ϕ
∧ 
T, η ⊨ σ
T, ηϕ + σ 
def
 
∃ η′ + η  . 
T, η′ ⊨ ϕ
∧ 
T, η ⊨ σ
T, ηϕ ~ σ 
def
 
∃ η′ ∼ η  . 
T, η′ ⊨ ϕ
∧ 
T, η ⊨ σ
 

and for node selectors we have

    
T, ητ Θ 
def
 

T, η ⊨ τ
∧ ∀ θ ∈ Θ  . 
T, η ⊨ θ
T, η* 
def
 
⊤ 
T, η(s|*) 
def
 
s = λS
η
T, ηe 
def
 
e = λE
η
T, η(s|e) 
def
 
s = λS
η
∧ e = λE
η
p ∈ P  . T, ηp 
def
 
p ∈ λP
η
 

and, for the remaining selectors we have (noting vv′ is the concatenation of the strings v and v′ and v-v′ is the concatenation of v and v′ with a “-” in between)

    
T, η:not(θ¬) 
def
 
¬
T, η ⊨ θ¬
T, η.v 
def
 
∃ s ∈ NS  . T, η ⊨ [s|class ~= v] 
T, η#v 
def
 
∃ s ∈ NS  . T, η ⊨ [s|id = v] 
T, η[a] 
def
 
∃ s ∈ NS  . T, η ⊨ [s|a] 
T, η[a op v] 
def
 
∃ s ∈ NS  . T, η ⊨ [s|a op v] 
T, η[s|a] 
def
 
λA
η

sa
≠ ⊥ 
T, η[s|a = v] 
def
 
λA
η

sa
v 
T, η[s|a |= v] 
def
 




 

λA
η

sa
v

 ∨ 
∃ v′  . 
 
λA
η

sa
v - v′ 

 




T, η[s|a ^= v] 
def
 
∃ v′ ∈ Γ . 
λA
η

sa
v v′ 
T, η[s|a $= v] 
def
 
∃ v′ ∈ Γ . 
λA
η

sa
v′ v 
T, η[s|a *= v] 
def
 
∃ v1v2 ∈ Γ . 
λA
η

sa
v1 v v2 
 

with the missing attribute selector being (noting vv′ is the concatenation of v and v′ with the space character ␣ in between)

    
T, η ⊨ [s|a ~= v] 
def
 








 
λA
η

sa
v  ∨ 
∃ v′   . 
 
λA
η

sa
v ␣ v′ 

 ∨ 
∃ v′  . 
 
λA
η

sa
v′ ␣ v 

 ∨ 
∃ v1v2  . 
 
λA
η

sa
v1 ␣ v ␣ v2 

 








 

then, for the counting selectors

    
T, η ⊨ :nth-child(αn + β) 
def
 
∃ n . ∃ η′, ι  . 

 
η = η′ι  ∧ 
ι = αn + β 
 


 
T, η ⊨ :nth-last-child(αn + β) 
def
 
∃ n  . ∃ η′, ι, ι′  . 


 
η = η′ι ∧ η′ι′ ∈ D  ∧ 
η′(ι′+1) ∉ D  ∧ 
ι′ − ι + 1 = αn + β 
 



 
T, η ⊨ :nth-of-type(αn + β) 
def
 
∃ n  . ∃ η′, ι  . 







 
η = η′ι  ∧ 






 





η′ι′ | 
ι′ ≤ ι  ∧ 
λS
η′ι′
= λS
η
 ∧ 
λE
η′ι′
= λE
η












= αn + β 
 








 
T, η ⊨ :nth-last-of-type(αn + β) 
def
 
∃ n  . ∃ η′, ι  . 







 
η = η′ι  ∧ 






 





η′ι′ | 
ι′ ≥ ι  ∧ η′ι′ ∈ D  ∧ 
λS
η′ι′
= λS
η
 ∧ 
λE
η′ι′
= λE
η












= αn + β 
 








 
Remark 1   An interesting sidenote is that our formalisation allows one to prove certain inexpressibility results. A simple question is the following: what class of string languages can the attribute selectors not express? Answer: regular languages that are not star-free (i.e. can be described by regular expressions that do not allow Kleene star, but allow language complementation. A typical example of languages that are not star-free is (aa)*, e.g., see [19]. To see this, one simply notes the attribute selectors can be translated to first-order formulas over strings (whose domains are string positions, whose unary predicates Ua can test the symbol at a given position is a, and whose binary predicate can test the precedence of two string positions).

4.2.4  Divergences from full CSS

Note, we diverge from the full CSS specification in a number of places. However, we do not lose expressivity.

5  Static Analysis

Having formalised CSS3 selectors, we now consider basic static analsis problems for CSS3, especially non-emptiness (a.k.a. satisfiability) and intersection (a.k.a. non-disjointness) problems. Our main result is that both problems are NP-complete. The complexity holds whether or not numbers in CSS3 selectors are represented in unary or binary.

Theorem 1 (Non-Emptiness)   Given a CSS selector ϕ, deciding T, η . T, η ⊨ ϕ is NP-complete.
Theorem 2 (Intersection)   Given two CSS selectors ϕ1 and ϕ2, deciding T, η . T, η ⊨ ϕ1T, η ⊨ ϕ2 is NP-complete.

We give the hardness results below. Membership is shown in the following sections. We introduce CSS automata for this purpose. In Proposition 5 we show each CSS selector can be translated in polynomial time into an equivalent CSS automaton. In Lemma 10 we show non-emptiness of CSS automata can be reduced to satisfiability of existential Presburger arithmetic, which is well-known to be in NP. This gives us membership of non-emptiness in NP. For intersection, we show in Proposition 6 that CSS automata are closed under intersection, and two automata can be intersected in polynomial time. Thus we reduce intersection in polynomial time to non-emptiness of a CSS automaton, which is in NP.

Lemma 3   Given a CSS selector ϕ, deciding T, η . T, η ⊨ ϕ is NP-hard.

We give a polynomial-time reduction from the NP-complete problem of non-universality of unions of arithmetic progressions [30, Proof of Theorem 6.1]. To define this, we first fix some notation. Given a pair (α, β) ∈ ℕ × ℕ, we define [[(α,β) ]] to be the set of natural numbers of the form α n + β for n ∈ ℕ. That is, [[(α,β) ]] represents an arithmetic progression, where α represents the period and β represents the offset. Let E ⊆ ℕ × ℕ be a finite subset of pairs (α, β). We define [[E ]] = ∪(α,β)∈ E [[(α,β) ]]. The NP-complete problem is: given E (where numbers may be represented in unary or in binary representation), is [[E ]] ≠ ℕ? Observe that this problem is equivalent to checking whether [[E+1 ]] ≠ ℕ>0 where E+1 is defined by adding 1 to the period β of each arithmetic progression (α,β) in E. By complementation, this last problem is equivalent to checking whether ℕ>0 ∖ [[E+1 ]] ≠ ∅. Since ℕ>0 ∖ [[E+1 ]] = ∩(α,β) ∈ E [[α,β+1 ]], the problem can be seen to be equivalent to testing the non-emptiness of

        *

:not(:nth-child(αn + (β+1))) | 

α, β
∈ E


 .

Thus, non-emptiness is NP-hard. ▫

Lemma 4   Given two CSS selectors ϕ1 and ϕ2, deciding whether T, η . T, η ⊨ ϕ1T, η ⊨ ϕ2 is NP-hard.

Non-emptiness reduces to non-emptiness-of-intersection. That is, ϕ is not empty iff the intersection of ϕ and * is non-empty. From Lemma 3 we get the result. ▫

6  CSS Automata

We will now develop a technique that allows us to simultaneously derive an NP upper bound for both the non-emptiness and the intersection problems for CSS3 selectors. Loosely speaking, these problems would be equivalent if CSS3 selectors were closed under intersection, which unfortunately are not due to the presence of CSS combinators in general. To this end, we follow a standard automata-theoretic approach: develop a general class of (tree) automata that subsume CSS3 selectors and are furthermore closed under intersection. We call these automata CSS automata. The result in this section shows that both non-emptiness and intersection problems for CSS3 selectors can be cast into the non-emptiness problem for CSS automata.

A CSS automaton navigates a tree structure in a similar manner to a CSS selector. That is, transitions may only move down the tree, or to a sibling. Furthermore, at each transition, a number of properties can be checked.

The reason we use automata as an intermediate step is that the automata navigate the tree in a uniform fashion. A direct intersection of two selectors is non-trivial since selectors may descend to different child nodes, and then meet again after the application of a number of sibling combinators. Thus their paths may diverge and combine several times. The automata are designed to always navigate to the first child, and then move from sibling to sibling. Thus, the intersection of CSS automata can be done with a straightforward product construction.

Intuitively, the modalities ↓, →, →+, and ∘ perform the following operations. The ↓ operator moves to the first child of the current node. The → operator moves to the next sibling of the current node. Finally, the →+ operator moves an arbitrary number of siblings to the right.

Note, we only allow self loops in the automata, since CSS does not have loops. Loops in the automata are used to skip over nodes that are not matched by a node selector in the full selector (e.g. .v ~ .v′ matches two sibling nodes with classes v and v′ respectively; loops will be used to skip over all nodes appearing between these two matched nodes). We do not allow → to label a loop – this is for the purposes of the NP proof: a sequence of transitions over a loop → can be more succinctly represented as a single loop transition labelled →+.

An astute reader may complain that →+ does not need to appear on a loop since it can already pass over an arbitrary number of nodes. However, the product construction used for intersection becomes easier if →+ appears only on loops. This is because a single →+ transition in one automaton may correspond to several transitions of the other. Hence, it is convenient to be able to use the →+ transition several times instead of splitting a single transition into several parts.

There is no analogue of →+ for ↓ because →+ is needed to handle selectors such as :nth-child(αn + β) which enforce the existence of a number of preceding children. There is no such CSS selector to count the depth of the tree. Finally ∘ marks the node matched by the selector.

Definition 1 (CSS Automata)   A CSS Automaton A is a tuple (Q, Δ, qin, qf) where Q is a finite set of states, Δ ⊆ Q × {↓, →, →+, ∘} × NSel × Q is a transition relation, qinQ is the initial state, and qfQ is the final state. Moreover,
  1. (only self-loops) there exists a partial order such that (q, d, σ, q′) ∈ Δ implies q′ ≲ q,
  2. (+ loops and doesn’t check nodes) for all (q, →+, σ, q′) ∈ Δ we have q = q and σ = *, and
  3. ( doesn’t label loops) for all (q, d, σ, q) ∈ Δ we have d ≠ → and σ = *.
  4. ( checks last node only) for all (q, d, σ, q′) ∈ Δ we have q′ = qf iff d = ∘.
  5. (qf is a sink) for all (q, d, σ, q′) ∈ Δ we have qqf.

We write q –[σ, d]→ q′ to denote a transition (q, d, σ, q′) ∈ Δ.

A document tree T = (D, λ) and node η ∈ D is accepted by a CSS automaton A, written (T, η) ∈ L(A), if there exists a sequence

    q0, η0, q1, η1, …, q, η, qℓ+1
Q × D
× 

qf

such that

  1. q0 = qin is the initial state and η0 = ε is the root node,
  2. qℓ+1 = qf and η= η,
  3. for all i, there is some transition qi–[σ, d]→ qi+1 with ηi satisfying σ and if i ≤ ℓ,
    1. if d = ↓ then ηi+1 = ηi1, (i.e., the youngest child of ηi)
    2. if d = → then there is some η′ and ι such that ηi= η′ ι and ηi+1 = η′ (ι + 1), and
    3. if d = →+ then there is some η′, ι and ι′ such that ηi= η′ ι and ηi+1 = η′ ι′ and ι′ > ι.

6.1  CSS Selectors to CSS Automata

For each CSS selector ϕ we can construct a CSS automaton Aϕ such that for all trees T

    T, η ⊨ ϕ ⇔
T, η
∈ L
Aϕ
 .

Given a CSS selector ϕ, we define Aϕ as follows. We can write ϕ uniquely in the form σ1 o1 σ2 o2on−1 σn where each σi is a node selector, and each oi∈ {>>, >, +, ~}. We define

    Aϕ = 
QE, Δ, qinqf

where

    
Q =


i, •i | 1 ≤ i ≤ n

⊎ 

qf

qin =1 
 

and we define the transition relation Δ to contain the following transitions, which are used to navigate from the root of the tree to the node matched by σ1, and to read the final node matched by σn (and the selector as a whole) respectively.

    ∘1 –[*, ↓, →+]→  ∘1      and      ∘n –[σn, ∘]→  qf

and for each 1 ≤ i < n,

We prove the following in Lemma 11 (soundness) and Lemma 12 (completeness) in Appendix A.1.

Proposition 5   For each CSS selector ϕ and tree T, we have T, η ⊨ ϕ iff (T, η) ∈ L(Aϕ).

6.2  Intersection of CSS Automata

Intersection of CSS automata is a standard product construction where →+ can match a sequence of → transitions. We first define the intersection of two node selectors. Note node selectors are of the form τ Θ where τ ∈ { *, (s|*), e, (s|e) | sNSeE }. Hence, letting Θ = Θ1 ∪ Θ2. we define

    τ1 Θ1 ⋂ τ2 Θ2 =
















 τ2 Θ τ1 = * 
τ1 Θ τ2 = * 
τ2 Θ 
τ1 = (s|*) ∧ 

 
τ2 = (s|*)  ∨ 
τ2 = (s|e) 


(s|e) Θ τ1 = (s|*) ∧ τ2 = e 
τ1 Θ 
τ1 = (s|e) ∧ 


 
τ2 = (s|e)  ∨ 
τ2 = e  ∨ 
τ2 = (s|*) 
 



τ2 Θ 
τ1 = e ∧ 
 τ2 = (s|e) ∨ τ2 = e 
(s|e) Θ τ1 = e ∧ τ2 = (s|*) 
:not(*) otherwise.
 

We give the product construction required for intersection below. Note that the synchronisation of a transition labelled → with a transition labelled →+ relies on →+ only labelling loops7.

Definition 2 (A1A2)   Given A1 = (Q1, E, Δ1, q1in, qf1) and A2 = (Q2, E, Δ2, q2in, qf2) we define
        A1 ⋂ A2 =
Q1 × Q2, E, Δ,
q1inq2in
,
qf1qf2

where Δ =
        
            


q1q2
–[σ1 ⋂ σ2, ↓]→ 
q1q2
 | q1 –[σ1, ↓]→  q1q2 –[σ2, ↓]→  q2

 ⋃ 
            


q1q2
–[σ1 ⋂ σ2, →]→ 
q1q2
 | q1 –[σ1, →]→  q1q2 –[σ2, →]→  q2

 ⋃ 
            


q1q2
–[σ1, →]→ 
q1q2
 | q1 –[σ1, →]→  q1q2 –[*, →+]→  q2

 ⋃ 
            


q1q2
–[σ2, →]→ 
q1q2
 | q1 –[*, →+]→  q1q2 –[σ2, →]→  q2

 ⋃ 
            


q1q2
–[*, →+]→ 
q1q2
 | q1 –[*, →+]→  q1q2 –[*, →+]→  q2

 ⋃ 
            


q1q2
–[σ1 ⋂ σ2, ∘]→ 
qf1qf2
 | q1 –[σ1, ∘]→  qf1q2 –[σ2, ∘]→  qf2

 .

The following proposition asserts correctness of the above construction, which we prove in Appendix A.2.

Proposition 6   Given two CSS automata A1 and A2, we have for all trees T and nodes η,
        
T, η
∈ L
A1

T, η
∈ L
A2

T, η
∈ L
A1 ⋂ A2
 .

7  Non-Emptiness Algorithm

We show non-emptiness of a CSS automaton can be decided in NP by a polynomial-time reduction to existential Presburger arithmetic. That is, given a CSS automaton A, our algorithm constructs an existential Presburger formula θA such that A accepts a non-empty language iff θA is satisfiable. Our existential Presburger encoding relies on the fact that any loop in the automaton is a self loop that only needs to be taken at most once. In the case of loops labelled ↓, a CSS formula cannot track the depth in the tree, so repeated uses of the loop will only introduce redundant nodes. For loops labelled →+, it may be that selectors such as :nth-child(αn + β) enforce the existence of a number of intermediate nodes. However, since →+ can cross several nodes, such loops also only needs to be taken once. Hence, each transition only needs to appear once in an accepting run. That is, if there is an accepting run of a CSS automaton with n transitions, there is also an accepting run of length at most n.

For the remainder of the section, we fix a CSS automaton A = (Q, Δ, qin, qf) and show how to construct the formula θA in polynomial-time.

7.1  Bounding Namespaces and Elements

Before giving the details of the reduction to existential Presburger, we first show that the number of namespaces and elements can be bounded linearly in the size of the automaton.

We write

  1. EA to denote the set of namespaced elements s:e such that there is some transition q –[σ, d]→ q′ ∈ Δ with σ = (s|e) Θ for some s, e, and Θ,
  2. SA is the set of transitions q –[σ, d]→ q′ ∈ Δ with σ ≠ * and |A|σ denotes the cardinality of SA.

Let {τ1, …, τ|A|σ} be a set of fresh namespaced elements and

    ⇃
EA
EA ⊎

τ1, …, τ
 

A
σ






where there is a bijection θ : SA → {τ1, …, τ|A|σ} such that for each tSA we have θ(t) = τ and

  1. τ = s:e if σ can only match elements s:e,
  2. τ = s:e for some fresh element e if σ can only match elements of the form s:e′ for all elements e′, and
  3. τ = s:e for some fresh namespace s if σ can only match elements of the form s′:e for all namespaces s′, and
  4. τ = s:e for fresh s and fresh e if σ places no restrictions on the element type.

We prove the following proposition in Appendix B.1. Intuitively, since only a finite number of nodes can be directly inspected by a CSS automaton, all others can be relabelled to a dummy type unless their type matches one of the inspected nodes.

Proposition 7 (Bounded Types)   Given a CSS Automaton A = (Q, Δ, qin, qf) if there exists (T, η) ∈ L(A) with T = (D,λ), then there exists (T′, η) ∈ L(A) where T′ = (D, λ′) and that the image of λ′ contains only namespaced elements in ⇃(EA).

Thus, we can define bounded sets of namespaces and elements

    

E
=


e | 
∃ s . s:e ∈ ⇃
EA



NS
=


s | 
∃ e . s:e ∈ ⇃
EA


 . 
 

7.2  Encoding Attribute Selectors

When encoding non-emptiness checks we will need to encode the satisfiability of conjunctions of attribute selectors. We show here how to perform this encoding. First we collect attribute selectors that apply to individual attributes. Next, we argue that if a collection of selectors can be satisfied by an attribute value, then there is a value of polynomially bounded length. Using this bound, we can encode the selectors as an existential Presburger formula.

7.2.1  Polynomial Bound

We begin by arguing the existence of a polynomial bound for the solutions to any finite set C of constraints of the form [s|a op v] or :not([s|a op v]), for some fixed s and a. We say that C is a set of constraints over s and a.

In fact, the situation is a little more complicated because it may be the case that a is id. In this case we need to be able to enforce a global uniqueness constraint on the attribute values. Thus, for constraints on an ID attribute, we need a bound that is large enough to allow to all constraints on the same ID appearing throughout the automaton to be satisfied by unique values. Thus, for a given automaton, we might ask for a bound N such that if there exists unique ID values for each transition, then there exist values of length bounded by N.

However, the bound on the length must still work when we account for the fact that not all transitions in the automaton will be used during a run. Consider the following illustrative example.

In this case we have two transitions with ID constraints, and hence two sets of constraints C1 = C2 = {[s|id = v]}. Since these two sets of constraints cannot be satisfied simultaneously with unique values, even the bound N = 0 will satisfy our naive formulation of the required property (since the property had the existence of a solution as an antecedent). However, it is easy to see that any run of the automaton does not use both sets of constraints, and that the bound N = |v| should suffice. Hence, we formulate the property of our bound to hold for all sub-collections of the collection of sets of constraints appearing in the automaton.

Lemma 8 (Bounded Attribute Values)   Given a collection of constraints C1, …, Cn over some s and a, there exists a bound N polynomial in the size of C1, …, Cn such that for any subsequence Ci1, …, Cim if there is a sequence of words v1, …, vm such that all vj are unique and vj satisfies the constraints in Cij, then there is a sequence of words such that the length of each vj is bounded by N, all vj are unique, and vj satisfies the constraints in Cij,

The proof uses ideas from Muscholl and Walukiewicz’s NP fragment of LTL [25]. We first, for each set of constraints C, construct a deterministic finite word automaton A that accepts only words satisfying all constraints in C. This automaton has a polynomial number of states and can easily be seen to have a short solution by a standard pumping argument. Given automata A1, …, An with at most Ns states and Nc constraints in each set of constraints, we can again use pumping to show there is a sequence of distinct words v1, …, vn such that each vi is accepted by Ai and the length of vi is at most n·Ns·Nc.

The Automata

We define a type of word automata based on a model by Muscholl and Walukiewicz to show and NP upper bound for a variant of LTL. These automata read words and keep track of which constraints in C have been satisfied or violated. They accept once all positive constraints have been satisfied and no negative constraints have been observed.

In the following, let Prefs(C) be the set of words v′ such that v′ is a prefix of some v with [s|a op v]C or :not([s|a op v])C. Moreover, let ^ and $ be characters not in Γ that will mark the beginning and end of the word respectively. Additionally, let ε denote the empty word. Finally, we write vv′ if v is a factor of v′, i.e., v′ = v1 v v2 for some v1 and v2.

Definition 3 (AC)   Given a set C of constraints over s and a, we define AC = (Q, Δ, C) where

Observe that the size of the automaton AC is polynomial in the size of C.

A run of AC over a word with beginning and end marked a1an∈ ^ Γ$ is

    
v0S0V0
–[a1]→ 
v1S1V1
–[a2]→  ⋯ –[an]→ 
vnSnVn

where v0 = ε and for all 1 ≤ in we have vi − 1 –[ai]→ vi and Si, ViC track the satisfied and violated constraints respectively. That is S0 = V0 = ∅, and for all 1 ≤ in we have (noting ^vvi implies ^v is a prefix of vi, and similar for v$) Si=

    
        Si−1 ⋃

[s|a = v] ∈ C | ^ v $ = vi

 ⋃
        

[s|a ~= v] ∈ C | 
a1 ∈ 

^, ␣

, a2 ∈ 

␣, $

 . a1 v a2 ≼ vi


 ⋃
        

[s|a |= v] ∈ C | 
a2 ∈ 

$, -

 . ^ v a2 ≼ vi


 ⋃
        

[s|a ^= v] ∈ C | ^ v ≼ vi



[s|a $= v] ∈ C | v $ ≼ vi

 ⋃
        

[s|a *= v] ∈ C | v ≼ vi

and Vi=

    
Vi−1 ⋃ 

:not([s|a = v]) ∈ C | ^v$ = vi

 ⋃ 






:not([s|a ~= v]) ∈ C | 
∃ 
a1 ∈ 

^, ␣

a2 ∈ 

␣, $

  . a1 v a2 ≼ vi






 ⋃ 


:not([s|a |= v]) ∈ C | 
∃ a2 ∈ 

$, -

 . ^ v a2 ≼ vi


 ⋃ 


:not([s|a ^= v]) ∈ C | ^ v ≼ vi

 ⋃ 


:not([s|a $= v]) ∈ C | v $ ≼ vi

 ⋃ 


:not([s|a *= v]) ∈ C | v ≼ vi

 . 
 

Such a run is accepting if Sn= {[s|a op v] | [s|a op v]C} and Vn= ∅. That is, all positive constraints have been satisfied and no negative constraints have been violated.

Short Solutions

We show the existence of short solutions via the following lemma. The proof of this lemma is a simple pumping argument which appears in Appendix B.2. Intuitively, if a satisfying word is shorter than Ns · Nc we do not change it. If it is longer than Ns · Nc any accepting run of the automaton on this word must contain a repeated (v, S, V). We can thus pump down this word to ensure that it is shorter than Ns · Nc. Then, to ensure it is unique, we pump it up to some unique length of at most n · Ns · Nc.

Lemma 9 (Short Attribute Values)   Given a sequence of sets of constraint automata AC1, …, ACn each with at most Ns states and at most Nc constraints in each Ci, if there is a sequence of pairwise unique words v1, …, vn such that for all 1 ≤ in there is an accepting run of ACi over vi, then there exists such a sequence where the length of each vi is at most n · Ns · Nc.

To obtain Lemma 8 (Bounded Attribute Values) we observe that for any subsequence Ci1, …, Cim we have m · Ns′ · Nc′ ≤ n · Ns · Nc since mn and the max number of states Ns′ and constraints Nc′ in the subsequence have Ns′ ≤ Ns and Nc′ ≤ Nc.

7.2.2  Presburger Encoding

Since short witnessing strings suffice for satisfiable attribute attribute selectors, we may use quantifier-free Presburger formulas to “guess” these witnessing strings; the letter in each position in a witnessing string is encoded by a number. [In fact, boolean formulas suffice, though we shall use integer variables since they are cleaner to work with and do not yield worse computational complexity.]

In the following encoding, we use the fact that we can assume each positive attribute selector that does not specify a namespace applies to a unique, fresh, namespace. Thus, these selectors do not interact with any other positive attribute selectors. Note, these fresh namespaces do not appear in ⇃(NS).

Let op range over {=, ~=, |=, ^=, $=, *=}. Let τΘ be a node selector. For each s and a, let Θas be the set of conditions in Θ of the form θ or :not(θ) where θ is of the form [s|a] or [s|a op v]. Recall we are encoding runs of a CSS automaton of length at most n. For a given position i in the run, we define AttsPres(τΘ, i) to be the conjunction of the following constraints, where the encoding for sets of selectors is presented in the sequel. Let Neg(s, a) = {:not([s|a op v]) | :not([a op v]) ∈ Θ}.

It remains to encode AttsPress:a(C, i) for some set of attribute selectors C all applying to s and a.

We can obtain a polynomially-sized global bound (N − 1) on the length of any satisfying value of an attribute s:a at some position i of the run. We obtain this by, for each s and a, collecting the sets of constraints over s and a from each transition, and applying Lemma 8 (Bounded Attribute Values). We then take the maximum of all bounds obtained in this way8. Finally, we increment the bound by one to allow space for a trailing null character.

Once we have a bound on the length of a satisfying value, we can introduce variables for each character position of the satisfying value, and encode the constraints almost directly. That is, letting θ range over positive attribute selectors, we define9

    
AttsPress:a
Ci
=
 
θ ∈ C
 AttsPres


θ, 
x
 



 ∧ 
  
 
:not(θ) ∈ C
 ¬ AttsPres


θ, 
x
 



 ∧ 
  
Nulls


x
 



 

where x = xi, 1s:a, …, xi, Ns:a will be existentially quantified later in the encoding and whose values will range10 over Γ ⊎ {0} where 0 is a null character used to pad the suffix of each word. We define AttsPres(θ, x) for several θ, the rest can be defined in the same way (see Appendix B.3). Letting v = a1am,

    
AttsPres


[s|a]
x
 



=⊤ 
AttsPres


[s|a = v]
x
 



=
 
1 ≤ i ≤ m
 xijs:a = aj∧ xim+1s:a = 0 
AttsPres


[s|a ^= v]
x
 



=
 
1 ≤ j ≤ m
 xijs:a = aj
AttsPres


[s|a *= v]
x
 



=
 
0 ≤ j ≤ N − m − 1
 
 
1 ≤ j′ ≤ m
 xij + js:a = aj
 

Finally, we enforce correct use of the null character

    Nulls


x
 



=
 
1 ≤ j ≤ N
 
j ≤ j′ ≤ N
xijs:a = 0  .

7.3  Encoding Non-Emptiness

We encode non-emptiness using the following variables for 0 ≤ in, representing the node at the ith step of the run:

Note, we do not need a variable for :root since it necessarily holds uniquely at the 0th position of the run.

Before we give the reduction for CSS automaton we first show how to negate a formula of the form ∃ n . x = α n + β where x is a variable, and α and β are constants, while still remaining inside existential Presburger arithmetic. This is not difficult, but one has to take care since the numbers α and β are represented in binary. Then we show how to construct an existential Presburger formula from a node selector, and a position i.

7.3.1  Negating Positional Formulas

We need formulas to negate selectors like :nth-child(αn + β), For completeness, we give the definition of the negation below. We prove its correctness in Appendix B.4.

We decompose β according to the period α. I.e. β = α β1 + β2, where β1 and β2 are the unique integers such that |β2| < |α| and β1 α < 0 implies β2 ≤ 0 and β1 α > 0 implies β2 ≥ 0.

Definition 4 (NoMatch(x, α, β))   Given constants α, β, β1, and β2 as above, we define NoMatch(x, α, β) to be
        


0 ≥ α ∧ 
x
 < β


∨ 

0 ≤ α ∧ 
x
 > β


 ∨ 
















 ∃ 
n
  . ∃ 
β
2 . 















 


β
2


α
 ∧ 


β1α < 0 ⇒ 
β
2 ≤ 0


 ∧ 


β1α > 0 ⇒ 
β
2 ≥ 0


 ∧ 
β
2 ≠ β2  ∧ 
x
 = α
n
 + αβ1 + 
β
2 
 
































 

7.3.2  Encoding Node Selectors

We define the encoding of node selectors below. This encoding uses the variables defined in the previous section. Note, this translation is not correct in isolation: global constraints such as “no ID appears twice in the tree” will be enforced later.

In the following, let NoAtts(Θ) be Θ less all selectors of the form [s|a], [s|a op v], [a], or [a op v], or :not([s|a]), :not([s|a op v]), :not([a]), or :not([a op v]).

Definition 5 (Pres(σ, i))   Given a node selector τΘ, we define
        Pres
τΘ, i








 
Pres
τ, i
∧ 



 
 
θ ∈ NoAtts
Θ
 Pres
θ, i



∧ 
AttsPres
τΘ, i
 








where we define Pres(θ, i) and Pres¬(θ, i) as follows:
        
Pres
*i
=⊤ 
Pres
(s|*)i
=


s
i = s


Pres
ei
=


e
i = e


Pres
(s|e)i
=


 
s
i = s ∧ 
e
i = e 


Pres
:not(σ¬)i
=
Pres¬
σ¬i
Pres
:rooti
=


 ⊤i = 0 
otherwise 
 
∀ p ∈ P ∖ 

:root

 . Pres
pi
=
p
i 
 
and, finally, for the remaining selectors, we have
        
            Pres
:nth-child(αn + β), 0
=            ⊥
            Pres
:nth-last-child(αn + β), 0
=            ⊥
            Pres
:nth-of-type(αn + β), 0
=            ⊥
            Pres
:nth-last-of-type(αn + β), 0
=            ⊥
            Pres
:only-child, 0
=            ⊥
            Pres
:only-of-type, 0
=            ⊥
and when i > 0
 Pres
:nth-child(αn + β)i
= ∃ 
n
 . 
n
i = α 
n
 + β  
 Pres
:nth-last-child(αn + β)i
= ∃ 
n
 . 
N
i = α 
n
 + β  
 Pres
:nth-of-type(αn + β)i
 
 
 s ∈ 
NS
e ∈ 
E






 
s
i = s ∧ 
e
i = e ∧ 
∃ 
n
 . 
n
is:e + 1 = α 
n
 + β 
 






 Pres
:nth-last-of-type(αn + β)i
 
 
 s ∈ 
NS
e ∈ 
E






 
s
i = s ∧ 
e
i = e ∧ 
∃ 
n
 . 
N
is:e + 1 = α 
n
 + β 
 






 Pres
:only-childi
n
i = 1 ∧ 
N
i = 1  
 Pres
:only-of-typei
 
 
 s ∈ 
NS
e ∈ 
E






 
s
i = s ∧ 
e
i = e ∧ 
n
is:e = 0 ∧ 
N
is:e = 0 
 






and we define the translation of negated simple CSS selectors as
     
Pres¬
*i
= ⊥          
 Pres¬
(s|*)i


s
i ≠ s


         
 Pres¬
ei


e
i ≠ e


         
 Pres¬
(s|e)i


s
i ≠ s ∨ 
e
i ≠ e


         
 Pres¬
:rooti


 ⊥i = 0 
otherwise 
 
         
 ∀ p ∈ P ∖ 

:root

 . Pres¬
pi
= ¬ 
p
i 
         
and finally, for the remaining selectors
Pres¬
:nth-child(αn + β), 0
=⊤ 
Pres¬
:nth-last-child(αn + β), 0
=⊤ 
Pres¬
:nth-of-type(αn + β), 0
=⊤ 
Pres¬
:nth-last-of-type(αn + β), 0
=⊤ 
Pres¬
:only-child, 0
=⊤ 
Pres¬
:only-of-type, 0
=⊤ 
 
and when i > 0
 Pres¬
:nth-child(αn + β)i
NoMatch

n
i, α, β


 
 Pres¬
:nth-last-child(αn + β)i
NoMatch

N
i, α, β


 
 Pres¬
:nth-of-type(αn + β)i
 
 
 s ∈ 
NS
e ∈ 
E






 
s
i = s ∧ 
e
i = e ∧ 
NoMatch

n
is:e + 1, α, β


 






 Pres¬
:nth-last-of-type(αn + β)i
 
 
 s ∈ 
NS
e ∈ 
E






 
s
i = s ∧ 
e
i = e ∧ 
NoMatch

N
is:e + 1, α, β


 






 Pres¬
:only-childi
n
i > 1 ∨ 
N
i > 1  
 Pres¬
:only-of-typei
 
 
 s ∈ 
NS
e ∈ 
E






 
s
i = s ∧ 
e
i = e ∧ 
n
is:e > 0 ∨ 
N
is:e > 0 
 






 . 

7.3.3  Reducing CSS Automata

Since we know, if there is an accepting run, that there is a run of length at most n where n is the number of transitions in Δ, we encode the possibility of an accepting run using the variables discussed above for all 0 ≤ in. We encode non-emptiness of a CSS automaton using the encoding below.

Definition 6  θA Given a CSS automaton A we define
        θA = 






 






 
q
0 = qin 
∧ 
q
n = qf 
 







∧ 
 
0 ≤ i < n
 





 
Tran
i
∨ 
q
i = qf 
 






∧ Consistent 







where Tran(i) and Consistent are defined below.

Intuitively, the first two conjuncts asserts that a final state is reached from an initial state. Next, we use Tran(i) to encodes a single step of the transition relation, or allows the run to finish early. Finally Consistent asserts consistency constraints.

We define Tran(i) = ∨t ∈ Δ Tran(i, t) where Tran(i, t) is defined below by cases. To ease presentation, we write si:ei = s:e as shorthand for ( si = sei = e ) and si:eis:e as shorthand for ( siseie ).

  1. When t = q –[σ, ↓]→ q′ we define Tran(i, t) to be
            


    q
    i = q


    ∧ 

    q
    i+1 = q


    ∧ ¬
    :empty
    i
     ∧ Pres
    σ, i
     ∧ 


    n
    i+1 = 1


    ∧ 
     
     s ∈ 
    NS
    e ∈ 
    E


     
    n
    i+1s:e = 0 


     . 
     
  2. When t = q –[σ, →]→ q′ we define Tran(i, t) to be false when i = 0 (since the root has no siblings) and otherwise
            


    q
    i = q


    ∧ 

    q
    i+1 = q


    ∧ Pres
    σ, i
     ∧ 


    n
    i+1 = 
    n
    i + 1


    ∧ 

    N
    i+1 = 
    N
    i − 1


     ∧ 
     
     s ∈ 
    NS
    e ∈ 
    E
     











     


     

     
    s
    i:
    e
    i = s:e 


    ⇒ 

     
    n
    i+1s:e = 
    n
    is:e + 1 




     ∧ 


     

     
    s
    i:
    e
    i ≠ s:e 


    ⇒ 

     
    n
    i+1s:e = 
    n
    is:e 




     ∧ 


     

     
    s
    i+1:
    e
    i+1 = s:e 


    ⇒ 

     
    N
    i+1s:e = 
    N
    is:e − 1 




     ∧ 


     

     
    s
    i+1:
    e
    i+1 ≠ s:e 


    ⇒ 

     
    N
    i+1s:e = 
    N
    is:e 




     












     . 
  3. When t = q –[*, →+]→ q we define Tran(i, t) to be false when i = 0 and otherwise
            


    q
    i = q


    ∧ 

    q
    i+1 = q


     ∧ 
    ∃ 
    δ
     . 

     

    n
    i+1 = 
    n
    i + 
    δ


    ∧ 

    N
    i+1 = 
    N
    i − 
    δ




     ∧ 
     
     s ∈ 
    NS
    e ∈ 
    E
     ∃ 
    δ
    s:e .  



























     






     


     
    s
    i:
    e
    i = s:e 


     ⇒ 
       

     
    n
    i+1s:e = 
    n
    is:e + 
    δ
    s:e + 1 


     






     ∧ 






     


     
    s
    i:
    e
    i ≠ s:e 


     ⇒ 
       

     
    n
    i+1s:e = 
    n
    is:e + 
    δ
    s:e 


     






     ∧ 






     


     
    s
    i+1:
    e
    i+1 = s:e 


     ⇒ 
       

     
    N
    i+1s:e = 
    N
    is:e − 
    δ
    s:e − 1 


     






     ∧ 






     


     
    s
    i+1:
    e
    i+1 ≠ s:e 


     ⇒ 
       

     
    N
    i+1s:e = 
    N
    is:e − 
    δ
    s:e 


     






     




























     . 
     
  4. When t = q –[σ, ∘]→ q′ we define Tran(i, t) to be
            

    q
    i = q




    q
    i+1 = q


    Pres
    σ, i
     .

The consistency constraint on the run asserts

    Consistent = ConsistentnConsistentiConsistentp

where each conjunct is defined below.

Lemma 10 (Correctness of θA)   For a CSS automaton A, we have
        L
A
≠ ∅ ⇔θA is satisfiable.

See Lemma 14 and Lemma 15 in Appendix B.5. ▫

8  Conclusion and Future Work

This paper presents a formalisation of CSS3 selectors and fundamental results concerning static analysis of CSS3 selectors. In particular, we chose to study the problems of satisfiability and disjointness of CSS3 selectors since they are arguably the most basic static analysis problems for CSS3 selectors and they have found applications in CSS optimisation. To the best of our knowledge, we are the first to successfully argue that these static analysis problems are decidable and, in fact, NP-complete. Our reduction to existential Presburger formulas (for which highly optimised SMT solvers are available) could potentially lead to efficient solutions to these static analysis problems that can handle CSS3 in its entirety. We leave this implementation task for future work.

Another future research avenue is to study other fundamental static analysis and optimisation problems for CSS3. One such problem is the problem of inclusion-checking for CSS selectors (which have found applications in CSS optimisation; see [6]). It is possible to use the technique developed in this paper to show that the problem is decidable, though it is far from obvious what the actual computational complexity is. Finally, since CSS is an evolving language (e.g. see [8] for the latest draft for the currently unstable CSS4, but seems to be substantially more expressive than CSS3), we believe that academics could play an important role in providing constructive feedback on the expressiveness of the language. Our formalisation of CSS3 is a starting point. We leave it for future work to address this issue in more depth.

References

[1]
W3C Recommendation of XPath 3.0 (referred in June 2016). .
[2]
W3Schools Gentle Introduction to CSS (referred in June 2016). .
[3]
The Unicode Standard, Version 6.0 (referred in June 2016). .
[4]
Michael Benedikt, Wenfei Fan, and Floris Geerts. XPath satisfiability in the presence of dtds. In Proceedings of the Twenty-fourth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 13-15, 2005, Baltimore, Maryland, USA, pages 25–36, 2005.
[5]
Michael Benedikt, Wenfei Fan, and Gabriel M. Kuper. Structural properties of XPath fragments. In Database Theory - ICDT 2003, 9th International Conference, Siena, Italy, January 8-10, 2003, Proceedings, pages 79–95, 2003.
[6]
Martí Bosch, Pierre Genevès, and Nabil Layaïda. Reasoning with style. In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pages 2227–2233, 2015.
[7]
T. Çelik, E. J. Etemad, D. Glazman, I. Hickson, P. Linss, and J. Williams. Selectors level 3: W3c recommendation 29 september 2011, 2011.
[8]
Elika J. Etemad and Tab Atkins Jr. Selectors Level 4: W3C Working Draft 2 May 2013, 2013.
[9]
Diego Figueira. Reasoning on words and trees with data: On decidable automata on data words and data trees in relation to satisfiability of LTL and XPath. PhD thesis, Ecole Normale Superieure de Cachan, 2010.
[10]
Floris Geerts and Wenfei Fan. Satisfiability of XPath queries with sibling axes. In Database Programming Languages, 10th International Symposium, DBPL 2005, Trondheim, Norway, August 28-29, 2005, Revised Selected Papers, pages 122–137, 2005.
[11]
Pierre Genevès and Nabil Layaïda. A system for the static analysis of XPath. ACM Trans. Inf. Syst., 24(4):475–502, 2006.
[12]
Pierre Genevès, Nabil Layaïda, and Vincent Quint. On the analysis of cascading style sheets. In Proceedings of the 21st World Wide Web Conference 2012, WWW 2012, Lyon, France, April 16-20, 2012, pages 809–818, 2012.
[13]
Georg Gottlob and Christoph Koch. Monadic queries over tree-structured data. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, pages 189–202, 2002.
[14]
Matthew Hague, Anthony Widjaja Lin, and C.-H. Luke Ong. Detecting redundant CSS rules in HTML5 applications: a tree rewriting approach. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SPLASH 2015, Pittsburgh, PA, USA, October 25-30, 2015, pages 1–19, 2015.
[15]
Jan Hidders. Satisfiability of XPath expressions. In Database Programming Languages, 9th International Workshop, DBPL 2003, Potsdam, Germany, September 6-8, 2003, Revised Papers, pages 21–36, 2003.
[16]
Dexter Kozen. Lower bounds for natural proof systems. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 254–266, 1977.
[17]
Dexter C. Kozen. Theory of Computation. Springer, 2006.
[18]
Leonid Libkin. Logics for unranked trees: An overview. Logical Methods in Computer Science, 2(3), 2006.
[19]
Leonid Libkin. Elements of Finite Model Theory. Springer, 2010.
[20]
Leonid Libkin and Cristina Sirangelo. Reasoning about XML with temporal logics and automata. J. Applied Logic, 8(2):210–232, 2010.
[21]
Maarten Marx. Conditional xpath. ACM Trans. Database Syst., 30(4):929–959, 2005.
[22]
Maarten Marx and Maarten de Rijke. Semantic characterizations of navigational xpath. SIGMOD Record, 34(2):41–46, 2005.
[23]
Davood Mazinanian, Nikolaos Tsantalis, and Ali Mesbah. Discovering refactoring opportunities in cascading style sheets. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, (FSE-22), Hong Kong, China, November 16 - 22, 2014, pages 496–506, 2014.
[24]
Ali Mesbah and Shabnam Mirshokraie. Automated Analysis of CSS Rules to Support Style Maintenance. In ICSE, pages 408–418, 2012.
[25]
A. Muscholl and I. Walukiewicz. An np-complete fragment of LTL. Int. J. Found. Comput. Sci., 16(4):743–753, 2005.
[26]
Frank Neven and Thomas Schwentick. On the complexity of xpath containment in the presence of disjunction, dtds, and variables. Logical Methods in Computer Science, 2(3), 2006.
[27]
B. Scarpellini. Complexity of subcases of presburger arithmetic. Trans. of AMS, 284(1):203–218, 1984.
[28]
Helmut Seidl, Thomas Schwentick, Anca Muscholl, and Peter Habermehl. Counting in trees for free. In Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings, pages 1136–1149, 2004.
[29]
Steve Souders. High Performance Web Sites: Essential Knowledge for Front-End Engineers. O’Reilly Media, 2007.
[30]
Larry J. Stockmeyer and Albert R. Meyer. Word problems requiring exponential time: Preliminary report. In Proceedings of the 5th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1973, Austin, Texas, USA, pages 1–9, 1973.
[31]
Balder ten Cate, Tadeusz Litak, and Maarten Marx. Complete axiomatizations for XPath fragments. J. Applied Logic, 8(2):153–172, 2010.
[32]
Balder ten Cate and Maarten Marx. Navigational XPath: calculus and algebra. SIGMOD Record, 36(2):19–26, 2007.
[33]
Balder ten Cate and Maarten Marx. Axiomatizing the logical core of XPath 2.0. Theory Comput. Syst., 44(4):561–589, 2009.
[34]
Philip Wadler. Two semantics of XPath, 2000. Tech. rep., Bell Labs.

A  Proofs for CSS Automata

A.1  Correctness of Aϕ

We show both soundness and completeness of Aϕ.

Lemma 11   For each CSS selector ϕ and tree T, we have
        
T, η
∈ L
Aϕ
T, η ⊨ ϕ  .

Suppose (T, η) ∈ L(Aϕ). By construction of Aϕ we know that the accepting run must pass through all states ∘1, …, ∘n where ϕ = σ1 o1on−1 σn. Notice, in order to exit each state ∘i a transition labelled by σi must be taken. Let ηi we the node read by this transition, which necessarily satisfies σi. Observe ηn= η. We proceed by induction. We have η1 satisfies σ1. Hence, assume ηi satisfies σ1 o1oi−1 σi. We show ηi+1 satisfies σ1 o1oi σi+1.

We case split on oi.

Thus, by induction, ηn= η satisfies σ1 o1on−1 σn= ϕ. ▫

Lemma 12   For each CSS selector ϕ and tree T, we have
        T, η ⊨ ϕ  . ⇒
T, η
∈ L
Aϕ

Assume T, η ⊨ ϕ. Thus, since ϕ = σ1 o1on−1 σn, we have a sequence of nodes η1, …, ηn such that for each i we have T, ηi⊨ σ1 o1oi−1 σi. Note ηn= η. We build a run of Aϕ from σ1 to ∘i by induction. When i = 1 we have the run constructed by taking the loops on the initial state ∘1 labelled ↓ and →+ to navigate to η1. Assume we have a run to ∘i. We build a run to ∘i+1 we consider oi.

Thus, by induction, we construct a run to ηn ending in state ∘n. We transform this to an accepting run by taking the transition ∘n –[σn, ∘]→ qf, using the fact that ηn satisfies σn. ▫

A.2  Correctness of Intersection

We show that

    
T, η
∈ L
A1

T, η
∈ L
A2

T, η
∈ L
A1 ⋂ A2
 .

We begin by observing that that all runs of a CSS automaton showing acceptance of a node η in T must follow a sequence of nodes η1, …, ηn such that

that defines the path taken by the automaton. Each node is “read” by some transition on each run. Note a transition labelled →+ may read sequence nodes that is a factor of the path above. However, since these transitions are loops that do not check the nodes, without loss of generality we can assume each →+ in fact reads only a single node. That is, →+ behaves like →. Recall, →+ was only introduced to ensure the existence of “short” runs.

Because of the above, any two runs accepting η in T must follow the same sequence of nodes and be of the same length.

We have (T, η) ∈ L(A1) ∧ (T, η) ∈ L(A2) iff there are accepting runs

    q1i –[σ1id1i]→  ⋯ –[σnidni]→  qn+1i

of Ai over T reaching node η for both i ∈ {1,2}. We argue these two runs exist iff we have a run

    
q11q12
–[σ1d1]→  ⋯ –[σndn]→ 
qn+11qn+12

of A1A2 where each dj and σj depends on (dj1, dj2).

The existence of the transitions comes from the definition of A1A2. We have to argue that ηj satisfies both σji iff it also satisfies σj. By observing σ ∩ * = * ∩ σ = σ we always have σj= σj1∩ σj2.

Let σji= τiΘi and σj= τΘ. It is immediate that ηj satisfies Θ = Θ1 ∪ Θ2 iff it satisfies both Θi.

To complete the proof we need to show ηj satisfies τ iff it satisfies both τi. Note, we must have some s and e such that τ, τ1, τ2 ∈ {*,(s|*),(s|e),e} else the type selectors cannot be satisfied (either τ = :not(*) or τ1 and τ2 assert conflicting namespaces or elements).

If some τi= * the property follows by definition. Otherwise, if τ = τ2 then in all cases the conjunction of τ1 and τ2 is equivalent to τ2 and we are done. The situation is similar when τ = τ1. Otherwise τ = (s|e) and τ1 = (s|*) and τ2 = e or vice versa, and it is easy to see τ is equivalent to the intersection of τ1 and τ2. Thus, we are done.

B  Proofs for Non-Emptiness of CSS Automata

B.1  Bounding Namespaces and Elements

We show Proposition 7 (Bounded Types). That is, if some tree T is accepted A, we can define another tree T′ that also is accepted by A but only uses types in ⇃(EA).

We take (T, η) ∈ L(A) with T = (D, λ) and we define T′ = (D, λ′) satisfying the proposition. Let

    q0, η0, q1, η1, …, q, η, qℓ+1

be the accepting run of A, by the sequence of transitions t0, …, t. As noted above, we can assume each transition in Δ appears only once in this sequence. Let {σ1, …, σ|A|σ} be the set of selectors appearing in A. We perform the following modifications to λ to obtain λ′.

We obtain λ′ from λ by changing the element labelling. We first consider all 0 ≤ i ≤ ℓ such that ηi is labelled by some element s:eEA. Let Nodess:e be the set of nodes labelled by s:e in λ. In λ′ we label all nodes in Nodess:e by s:e. That is, we do not relabel nodes labelled by s:e. Let Nodes be the union of all such Nodess:e.

Next we consider all 0 ≤ i ≤ ℓ such that ηiNodes (i.e. was not labelled in the previous case) and ti= qi–[σ, d]→ qi+1 with σ ≠ *. Let s:eEA be the element labelling of ηi in λ. Moreover, take τ such that θ(ti) = τ. In λ′ we label all nodes in Nodess:e (i.e. labelled by s:e) in λ by τ. That is, we globally replace s:e by τ. Let Nodes′ be Nodes union all such Nodese.

Finally, we label all nodes not in Nodes′ with the null element ⊥.

To see that

    q0, η0, q1, η1, …, q, η, qℓ+1

via t0, …, t is an accepting run of (D, λ′) we only need to show that for each ti= qi–[σ, d]→ qi+1 that ηi satisfies σ. This can be shown by induction over σ. Most atomic cases are straightforward (e.g. the truth of :hover is not affected by our transformations). The case of e, (s|*), or (s|e) appearing positively follows since in these cases the labelling remained the same or changed to some τ consistent with the selector. When such selectors appear negatively, the result follows since we only changed elements and namespaces to fresh ones. The truth of attribute selectors remains unchanged since we did not change the attribute labelling. The cases of :nth-child(αn + β) and :nth-last-child(αn + β) follow since we did not change the number of nodes. For the selectors :nth-of-type(αn + β) and :nth-last-of-type(αn + β) there are two cases. If we did not change the element label s:e of ηi, then we also did not change the label of its siblings. Moreover, we did not add any s:e labels elsewhere in the tree. Hence the truth of the formulas remains the same. If we did change the label from s:e to τ for some τ then observe that we also relabelled all other nodes in the tree labelled by s:e. In particular, all siblings of ηi. Moreover, since θ is a bijection and each transition appears only once in the run, we did not label any node not labelled s:e with τ. Hence the truth of the formulas also remains the same. Similar arguments hold for :only-child and :only-of-type.

Thus, (D, λ′) is accepted, and only uses elements in ⇃(EA) as required.

B.2  Proof of Lemma 9 (Short Attribute Values)

We give the proof of Lemma 9. That is, given a sequence of sets of constraint automata AC1, …, ACn each with at most Ns states and at most Nc constraints in each Ci, if there is a sequence of pairwise unique words v1, …, vn such that for all 1 ≤ in there is an accepting run of ACi over vi, then there exists such a sequence where the length of each vi is at most n · Ns · Nc.

To prove the lemma, take a sequence v1, …, vn such that each vi is unique and accepted by ACi. We proceed by induction, constructing v1, …, vi such that each vj is unique, accepted by ACj, and of length ℓ such that either

When i = 0 the result is vacuous. For the induction there are two cases.

When the length ℓ of vi is such that ℓ ≤ Ns · Nc we set vi= vi. We know vi is unique amongst v1, …, vi since for all j < i either vj is longer than vi or is equal to vj and thus distinct from vi.

When ℓ > Ns · Nc we use a pumping argument to pick some vi of length ℓ′ such that i · Ns · Nc ≤ ℓ′ ≤ (i + 1) · Ns · Nc. This ensures that vi is unique since it is the only word whose length lies within the bound. We take the accepting run

    
u0S0V0
–[a1]→ 
u1S1V1
–[a2]→  ⋯ –[an]→ 
uSnV

of vi and observe that the values of Sj and Vj are increasing by definition. That is SjSj+1 and VjVj+1. By a standard down pumping argument, we can construct a short accepting run containing only distinct configurations of length bound by Ns · Nc. We construct this run by removing all cycles from the original run. This maintains the acceptance condition. Next we obtain an accepted word of length i · Ns · Nc ≤ ℓ′ ≤ (i + 1) · Ns · Nc. Since ℓ > Ns · Nc we know there exists at least one configuration (u, S, V) in the short run that appeared twice in the original run. Thus there is a run of the automaton from (u, S, V) back to (u, S, V) which can be bounded by Ns · Nc by the same downward pumping argument as before. Thus, we insert this run into the short run the required number of times to obtain an accepted word vi of the required length.

Thus, by induction, we are able to obtain the required short words v1, …, vn as needed.

B.3  Missing definitions for AttsPres(θ, x)

 AttsPres


[s|a ~= v]
x
 



 
 
1 ≤ j ≤ m





 
xijs:a = aj ∧ 



 
xim+1s:a = 0 
∨ 
xim+1s:a = ␣ 
 



 





∨ 
 
 
1 ≤ j ≤ N − m − 1
 






 
xij − 1s:a = ␣  ∧ 
 
1 ≤ j′ ≤ m
 xij + js:a = aj ∧ 

xij + m + 1s:a = 0 ∨ xij + m + 1s:a = ␣
 







 AttsPres


[s|a |= v]
x
 



 
 
1 ≤ j ≤ m
 xijs:a = aj∧ 
xim+1s:a = 0 ∨ xim+1s:a = -
 AttsPres


[s|a $= v]
x
 



 
 
0 ≤ j ≤ N − m − 1
 




 
 
1 ≤ j′ ≤ m
 xij + js:a = aj ∧ 
xij + m + 1s:a = 0 
 





B.4  Correctness of NoMatch(x, α, β)

We show that our negation of periodic constraints is correct.

Proposition 13 (Correctness of NoMatch(x, α, β))   Given constants α and β, we have
        ¬

∃ 
n
 . 
x
 = α 
n
 + β


NoMatch

x
, α, β


 .

We first consider α = 0. Since there is no β′2 with |β′2| < 0 we have to prove

        ¬

x
 = β




x
 < β


∨ 

x
 > β


which is immediate.

In all other cases, the conditions on β2 and β′2 ensure that we always have 0 < |β2 − β′2| < |α|.

If ∃ n . x = α n + α β1 + β2 then if α > 0 it is easy to verify that we don’t have x < β (since n = 0 gives x = β as the smallest value of x) and similarly when α < 0 we don’t have x < β. To disprove the final disjunct of of NoMatch(x, α, β) we observe there can be no n′ s.t. x = α n′ + α β1 + β′2 since x = α n + α β1 + β2 and 0 < |β2 − β′2| < |α|.

In the other direction, we have three cases depending on the satisfied disjunct of NoMatch(x, α, β). Consider α > 0 and x < β. In this case there is no n such that x = α n + α β1 + β2 = α n + β since n = 0 gives the smallest value of x, which is β. The case is similar for the second disjunct with α < 0.

The final disjunct gives some n′ such that x = α n′ + α β1 + β′2 with 0 < |β2 − β′2| < |α|. Hence, there can be no n with x = α n + α β1 + β2. ▫

B.5  Correctness of Presburger Encoding

We prove soundness and completeness of the Presburger encoding of CSS automata non-emptiness in the two lemmas below.

Lemma 14   For a CSS automaton A, we have
        L
A
≠ ∅ ⇒ θA is satisfiable.

We take a run of A and construct a satisfying assignment to the variables in θA. That is take a document tree T = (D, λ), node η ∈ D, and sequence

        q0, η0, q1, η1, …, q, η, qℓ+1
Q × D
× 

qf

that is an accepting run. We know from Proposition 7 (Bounded Types) that T can only use namespaces from ⇃(NS) and elements from ⇃(E). Let t0, …, t be the sequence of transitions used in the accepting run. We assume (w.l.o.g.) that no transition is used twice. We construct a satisfying assignment to the variables as follows.

It remains to prove that the given assignment satisfies the formula.

Recall

        θA = 







 
q
0 = qin ∧ 
q
n = qf ∧ 
 
0 ≤ i < n
 

 Tran
i
∨ 
q
i = qf 


∧ 
Consistent 
 








 . 

The first two conjuncts follow immediately from our assignment to qi and that the chosen run was accepting. Next we look at the third conjunct and simultaneously prove Consistentn. When i ≥ ℓ + 1 we assigned qf to qi and can choose any assignment that satisfies Consistentn. Otherwise we show we satisfy Tran(i) by showing we satisfy Tran(i, ti). We also show Consistentn is satsfied by induction, noting it is immediate for i = 0 and that for i = 1 we must have either the first orlast case which do not depend on the induction hypothesis. Consider the form of ti.

  1. When ti= qi–[σ, ↓]→ qi+1 we immediately confirm the values of qi, qi+1, ni+1, ni+1s:e satisfy the constraint. Similarly for ¬:emptyi since we know :empty ∉ λPi). We defer the argument for Pres(σ, i) until after the case split. That Consistentn is satisfied can also be seen directly.
  2. When ti= qi–[σ, →]→ qi+1 we know ηi= η′ι and ηi+1 = η′(ι+1) for some η′ and ι. We can easily check the values of qi, qi+1, ni+1, Ni, ni+1s:e, and Ni+1s:e satisfy the constraint. We defer the argument for Pres(σ, i) until after the case split. To show Consistentn we observe ni+1 is increased by 1 and only one ni+1s:e is increased by 1, the others being increased by 0. Similarly for Ni and ni+1s:e. Hence the result follows from induction.
  3. When ti= qi–[*, →+]→ qi+1 we know ηi= η′ι and ηi+1 = η′(ι′) for some η′, ι, and ι < ι′. We can easily check the values of qi, qi+1, ni+1, Ni, ni+1s:e, and Ni+1s:e satisfy the constraint. We defer the argument for Pres(σ, i) until after the case split. To satisfy the constraints over the position variables, we observe that values for δ and δs:e can be chosen easily for the specified assignment. Combined with induction this shows Consistentn as required.
  4. When ti= qi–[σ, ∘]→ qi+1

    We can easily check the values of qi and qi+1. We defer the argument for Pres(σ, i) until after the case split. By induction we immediately obtain Consistentn.

We show Pres(σ, i) is satisfied for each ηi and σ labelling ti. Take a node η and σ = τΘ from this sequence. Note η satisfies σ since thw run is accepting. Recall

    Pres
τΘ, i








 
Pres
τ, i
∧ 



 
 
θ ∈ NoAtts
Θ
 Pres
θ, i



∧ 
AttsPres
τΘ, i
 








 . 

From the type information of η we immediately satisfy Pres(τ, i).

For a positive θ ∈ Θ there are several cases. If θ = :root then we know we are in η0 and the encoding is ⊤. If θ is some other pseudo class p then the encoding of θ is pi and we assigned true to this variable. For :nth-child(αn + β) and :nth-last-child(αn + β) satisfaction of the encoding follows immediately from η satisfying θ and our assignment to ni and Ni. Similarly we satisfy encodings of :nth-of-type(αn + β), :nth-last-of-type(αn + β), :only-child, and :only-of-type. The latter follow since an only child is position 1 from the start and end, and an only of type node has 0 strict predecessors or successors of thesame type.

For a negative θ ∈ Θ there are several cases. If θ = :not(:root) then we know we are not in η0 and the encoding is ⊤. If θ is the negation of some other pseudo class p then the encoding of θ is ¬pi and we assigned false to this variable. For the selectors :not(:nth-child(αn + β)) and the opposite selector :not(:nth-last-child(αn + β)) satisfaction of the encoding follows immediately from η satisfying θ, our assignment to ni and Ni as well as Proposition 13 (Correctness of NoMatch(x, α, β)). Similarly we satisfy encodings of :not(:nth-of-type(αn + β)) and also of the selector :not(:nth-last-of-type(αn + β)). For :not(:only-child), and :not(:only-of-type) the latter follow since an with multiple children the node must either not be position 1 from the start or end, and a not only of type node has more than 0 strict predecessors or successors of the same type.

Next, to satisfy AttsPres(τΘ, i) we have to satisfy a number of conjuncts. First, if we have a word a1an we assign it to the variables xi, js:a (where η is the ith in the run and j ranges over all word positions within the cimputed bound) ny assigning xi, js:a = aj when jn and xi, js:a = 0 otherwise.

In all cases below, it is straightforward to observe that it a word (within the computed length bound) satisfies [s|a op v] or :not([s|a op v]) then the encoding AttsPress:a([s|a op v], i) or ¬AttsPress:a([s|a op v], i) is satisfied by our variable assignment. Similarly Nulls(x) is straightforwardly satisfied. Hence, if a word satisfies C then our assignment to the variables means AttsPress:a(C, i) is also satisfied.

There are a number of cases of conjuncts for attribute selectors. The simplest is for sets Θas where we see immediately that all constraints are satisfied for λA(η)(s, a) and hence we assign this value to the appropriate variables and the conjuct is satisfied also. For each [a] and [a op v] ∈ Θ we have in the document some namespace s such that λA(η)(s, a) satisfies the attribute selector and all negative selectors applying to all namespaces. Let s′ be the fresh name space assigned to the selector during the encoding and C be the full set of constraints belonging to the conjunct (i.e. including negative ones). We assign to the variable xi, js:a the jth character of λA(η)(s, a) (where η is the ith in the run) and satisfy the conjuct as above. Note here that a single value of s:a is assigned to several s′:a. This is benign with respect to the global uniqueness required by ID attributes because each copy has a different namespace.

Finally, we have to satisfy the consistency constraints. We showed Consistentn above. The remaining consistency constraints are easily seen to be satisfied: Consistenti because each ID is unique causing at least one pair of characters to differ in every value; Consistentp since it encodes basic consistency constraints on the appearence of pseudo elements in the tree.

Thus, we have satisfied the encoded formula, completing the first direction of the proof. ▫

Lemma 15   For a CSS automaton A, we have
        θA is satisfiable. ⇒ L
A
≠ ∅

Take a satisfying assignment ρ to the free variables of θA. We construct a tree and node (T, η) as well as a run of A accepting (T, η).

We begin by taking the sequence of states q0, …, qℓ+1 which is the prefix of the assignment to q0, …, qn where q is the first occurrence of qf. We will construct a series of transitions t0, …, t with ti= qi–[σi, di]→ qi+1 for all 0 ≤ i ≤ ℓ. We will define each di and σi, as well as construct T and η by induction. We construct the tree inductively, then show σi is satisfied for each i.

At first let T0 contain only a root node. Thus η0 is necessarily this root. Throughout the proof we label each ηi as follows.

We pick ti as the transition corresponding to a satisfied disjunct of Tran(i) (of which there is at least one since qiqf when i ≤ ℓ). Thus, take ti= qi–[σi, di]→ qi. We proceed by a case split on di. Note only cases di= ↓ and di= ∘ may apply when i = 0.

The tree and node we require are the tree and node obtained after reaching some di= ∘, for which we necessairily have i = ℓ since ∘ must be and can only be used to reach qf. In constructing this tree we have almost demonstrated an accepting run of A. To complete the proof we need to argue that all σi are satisfied by ηi and that the obtained is valid. Let τΘ = σi.

To check τ we observe that Pres(τ, i) constrains si and ei to values, which when assigned to ηi as above mean ηi directly satisfies τ.

Now, take some θ ∈ Θ. In each case we argue that Pres(τ, i) ensures the needed properties. Note this is straightforward for the attribute selectors due to the directness of the Presburger encoding. Consider the remaining selectors.

First assume θ is positive. If it is :root then we must have i = 0 and ηi is the root node as required. For other pseudo classes p we asserted pi hence we have p ∈ λPi). The encoding of the remaining positive constraints can only be satisfied when i > 0. That is, ηi is not the root node.

For :nth-child(αn + β) observe we constructed T such that ηi= η ρ(ni) for some η. From the defined encoding of Pres(:nth-child(αn + β), i) we directly obtain that ηi satisfies :nth-child(αn + β). Similarly for :nth-last-child(αn + β) as we always pad the end of the sibling order to ensure the correct number of succeeding siblings.

For :nth-of-type(αn + β) and :nth-last-of-type(αn + β) selectors, by similar arguments to the previous selectors, we have ensured that there are enough preceeding or succeeding nodes (along with the directness of their Presburger encoding) to ensure these selectors are satisfied by ηi in T.

For :only-child we know there are no other children since ρ(ni) = ρ(Ni) = 1. Finally for :only-of-type we know there are no other children of the same type since ρ(nis:e) = ρ(Nis:e) = 0 where ηi has type s:e.

When θ is negative there are several cases. If it is :not(:root) then we must have i > 0 and ηi is not the root node. For other pseudo classes p we asserted ¬pi hence we have p ∉ λPi). The encoding of the remaining positive constraints are always satisfied on the root node. That is, i = 0. When ηi is not the root node we have i > 0.

For :not(:nth-child(αn + β)) observe we constructed T such that ηi= η ρ(ni) for some η. From the definition of Pres(:not(:nth-child(αn + β)), i) we obtain via Proposition 13 (Correctness of NoMatch(x, α, β)) that ηi does not satisfy the selector :nth-child(αn + β). Similarly for the last child selector :not(:nth-last-child(αn + β)).

For the :not(:nth-of-type(αn + β)) selector and the opposite selector :not(:nth-last-of-type(αn + β)), by similar arguments to the previous selectors, we have ensured that there are enough preceeding or succeeding nodes (along with their Presburger encodings and Proposition 13 (Correctness of NoMatch(x, α, β))) to ensure these selectors are satisfied by ηi in T.

For :not(:only-child) we know there are some other children since ρ(ni) > 1 or ρ(Ni) > 1. Finally for :not(:only-of-type) we know there are other children of the same type since ρ(nis:e) > 0 or ρ(Nis:e) > 0 where ηi has type s:e.

Thus we have an accepting run of A over some (T, η). However, we finally have to argue that T is a valid document tree. This is enforced by Consistenti and Consistentp.

First, Consistenti ensures all IDs satisfying the Presburger encoding are unique. Since we transferred these values directly to T our tree also has unique IDs.

Next, we have to ensure properties such as no node is both active and inactive. These are all directly taken care of by Consistentp. Thus, we are done. ▫


1
For readers unfamiliar with CSS, we provide a primer in Section 2.
2
XPath has a slightly different document object model in comparison to HTML. This statement is true if “class” is substituted by “tag”
3
XPath fragments that are commonly studied in database theory often assume a finite set of attribute values, no global id attribute constraints (i.e. no two nodes share the same id), and no counting constraints on the number of children, which is not the case for CSS3.
4
See the notes at the end of the section.
5
The CSS specification defines :lang(l) in this way. A restriction of the language values to standardised language codes is only a recommendation.
6
Recall →+ appears on loops only as this eases the intersection construction later.
7
Else we would have to deal with the case where →+ could read several nodes while → can only read one.
8
Of course, we could obtain individual bounds for each s and a if we wanted to streamline the encoding.
9
Note, we allow negation in this formula. This is for convenience only as the formulas we negate can easily be transformed into existential Presburger.
10
Strictly speaking, Presburger variables range over natural numbers. It is straightforward to range over a finite number of values. That is, we can assume, w.l.o.g. that Γ ⊎ 0 ⊆ ℕ and the quantification is suitably restricted.
11
Recall s is not necessarily in ⇃(NS) as it may be some fresh value.

This document was translated from LATEX by HEVEA.