Decidable XPath Fragments in the Real World
Baelde, David
Lick, Anthony
Schmitz, Sylvain
XPath is arguably the most popular query language for selecting elements in XML documents. Besides query evaluation, query satisfiability and containment are the main computational problems for XPath; they are useful, for instance, to detect dead code or validate query optimisations. These problems are undecidable in general, but several fragments have been identified over time for which satisfiability (or query containment) is decidable: CoreXPath 1.0 and 2.0 without so-called data joins, fragments with data joins but limited navigation, etc. However, these fragments are often given in a simplified syntax, and sometimes w.r.t. a simplified XPath semantics. Moreover, they have been studied mostly with theoretical motivations, with little consideration for the practically relevant features of XPath. To investigate the practical impact of these theoretical fragments, we design a benchmark compiling thousands of real-world XPath queries extracted from open-source projects, and match them against syntactic fragments from the literature. We investigate how to extend these fragments with seldom-considered features such as free variables, data tests, data joins, and the last () and id () functions, for which we provide both undecidability and decidability results. We analyse the coverage of the original and extended fragments, and further provide a glimpse at which other practical features might be worth investigating in the future.
 It's a joint work with David Bald and Anthony Lick back at TNS in Cachon. And the topic is pretty practical. It's about what can we say about X-path queries in the real world. And here's somehow the picture of what I want to talk about. So somehow in the ether, in space, you have those really nice results. Talking about decidable fragments. And here decidability is about satisfiability of a query. And this is a bit in the abstract. The question is about, does there exist a data tree, which is a model of the formula? And the kind of fragments that people look at typically concentrate on navigation plus a bit of a few data tests or data joints inside your queries. But those things have to be restricted quite a bit. Otherwise, you will get some decidable. On the other hand, they don't talk much about many other things that people use in X-path, maybe function applications and so on. And now down on Earth, you have this, well, the real X-path somehow, right? The one that is used by people to query XML documents, which has been evolving quite a bit right now. This revision, which is quite recent, includes like lambda abstractions for functions and many things, advanced programming constructs. So there's a kind of a gap in between the two. And we wanted to, well, get a hand at what is this gap, what it looks like. So the way we do it really is to build a benchmark of X-path queries. So it's an open source benchmark, so people can also play with it now. It's reasonably big, about 20,000 queries. And then we measured the coverage of those decidable fragments compared to this particular benchmark. So we first started with, let's say, Vania implementation somehow, these fragments, the way they're written in the papers, in the various papers. What does that give you? And of course, as expected, that was not very good because those papers were not having to deal with concrete X-path queries. But there are some very straightforward extensions, most of them, that one can do in order to get much better coverage. And I will say a few words, of course, about what kind of results we will obtain this way. So let's start with how we constructed this benchmark. So we focused on two kinds of sources. One are XSL documents, the other are Xquery documents. Those are all open source projects so that we could also distribute the results. There's, I think, around 20 different projects that are used. One of the advantages of using XSL and Xquery, let's say, instead of X-path embedded in Java or C-sharp or whatever, is that it's reasonably easy to extract the queries from the source. So in XSL, it's just some attribute values inside your XSLT document. So it's very easy. In the case of Xquery, using a parser for Xquery, you can essentially find which are the maximal sub-trees in your parse trees which are X-path and the rest is Xquery stuff. So you can also identify what is X-path inside an Xquery document. So in order to do that, we tuned a parser which is also provided by the W3C and the output we get is a bunch of syntax trees and we actually express all these in an XML format which is also a W3C format which is called XqueryX. It's a XML presentation of Xquery documents. Now that we have those syntax trees, we can also look at all those fragments that were defined in the literature and for each one of them write down some schemas. So here it turns out that reXNG was a nice formalism to write those down. And then check for each one of those queries, is it yes or no inside the syntactic fragments that has been considered in the literature. So what do we get? First of all, a few words about what we find in the benchmark itself. So we also checked what is the coverage of the various revisions of Xpath and we make a big distinction between XSLT and Xquery sources because the kind of queries you find in those types of documents tend to be pretty different. So already looking at this, you can see that in XSLT typically people use Xpath 1 mostly, whereas in Xquery they would use more advanced syntactic constructs using Xpath 2 or Xpath 3 constructs in there. Another point that will become quite important later is the use of functions. So Xpath and then Xquery as well come with a bunch of standard functions. So those functions are typically not supported at all in those, let's say, theoretical fragments looked at in the literature but they are extensively used in practice and this you can also see inside the benchmark. So here's a graph showing you how those functions are used and we make a distinction between standard functions, those that appear in this document here on the left, and non-standard ones and those are user defined either by extending maybe your Xpath engine so you can write this down in Java or if you're in Xquery you can define those non-standard functions pretty easily. And what we find is that well functions are used quite a bit, around 60% of the queries use some function calls. XSLT is a bit better behaved, so it's 57.23 here is the number of function calls which are using standard functions. And so in XSLT it's a bit better behaved, people are using standard functions more than other ones in Xquery. So what it means is that if you're basing let's say a tool for satisfiability of Xpath and you don't have support for user defined function, there's really a bound on how much you can do and here is the bound. This new column here is showing how many queries would fit inside Xpath 3 but restricted to standard functions. You see that for XSLT it's still a pretty large number of queries but for Xquery you won't cover more than 46%. So already we can see that any attempt at building a tool for Xpath satisfiability in Xquery documents will have to somehow manage user defined functions eventually. All right so now I'll tell you the coverage if you implement things pre-innavably, really taking those fragments, those syntactic fragments and looking at what you get, the coverage is pretty poor especially in Xquery documents it's almost negligible for several of those fragments and there's only one fragment that does pretty well. So it's this non-mixing fragment, it has been defined to work on three patterns for XML documents and it's essentially MSO but you have data tests and data joints as long as you are not mixing equality and disequity tests inside your patterns and there you see it's sort of okay, it works pretty nicely. But okay, those fragments were not defined to cope with concrete syntax and what can we do about this? So the idea is now to extend those fragments and let's say that a syntactic construct can be expressed in a fragment if you can just find or construct ideally an equivalent request and we say it's encoded if you can find an equisatisfiable request and of course for practical purposes you would like for all this stuff to be done in perennial time because this essentially defines a front-end to your tool that takes in concrete syntax and outputs abstracted syntax with which you can work in a core logic as defined in those theoretical papers. So what kind of extensions we've looked at? They're pretty straightforward ones really. So root navigations allow you to go just to the root of your XML document. You have three variables, that's used quite a lot in practice. So it means you have a variation that associates a bunch of nodes in elements in your XML tree to a variable like this variable $module and you are going to go in one of those and then continue your path. You have data tests against constants, so that's pretty straightforward. Data joins means that you're going here, you're checking whether you can find a path on the left side of this equality symbol that reaches an attribute href here which has the same value as whatever you can find using the right path. So can you find two paths such that those two attribute values are going to be equal? So here it means kind of find a preceding least item which has the same href value. And another one is positional predicates, so that's used quite a bit as well. And that's a function that you can support at least a bit, so one step positional predicates, we looked at this how you could encode things. And those encodings, most of them are really, really straightforward. So for instance, root navigation is expressible in most fragments because, well, you can just, in order to find the root, you can just go up and then test that you cannot go up anymore. It means you are at the root, so this is something you can do in most fragments. But surprisingly, you cannot do that everywhere, well, let's say if you're in downward x path, just simply you don't have those axes, ancestor, self, and parent, so you cannot express it directly. And counting things, there you have a bit more power, so you are looking for an equisatisfiable request, right? And here, for instance, free variables, again, it's pretty straightforward. You might just extend your label set to account for those free variables, for those positions where the valuation will put those free variables. So you can just do that. But there are some fragments where you cannot do that. So for instance, in forward x path, if you add either root navigation or free variables, you will get indecidable, and this is an easy adaptation of proofs that were done by Funtiago Figer and Luke Segoufarm. Another example of something which is not polynomially encodable is satisfiability in downward x path. If you extend it with navigation predicates like position equal last and position different from last, then it becomes a common heart, so definitely not polynomially encodable. So here's the kind of things we get. First, some of those syntactic constructs are actually native to those fragments. And then we can look at which ones are expressible. As I told you, root navigation is pretty straightforward, for instance, which ones can be encoded and which ones cannot be encoded or not polynomial encoded. So what we get with those easy transformations is actually quite better results already. So if you look at the combined coverage of the entire benchmark and saying if some of those extended fragments manages to capture some of these. So you get around 60% coverage. And the best individual fragment is code 2 x path. And with these extensions, it reaches 75% of XSLT and 28% of x-way. All right. We also compared those fragments. And here if you feel like playing around and seeing what kind of query is falling to this or that fragment, there's an interactive interface that allows you to click around. And it shows you the list of all those queries which are captured in this fragment, but not that fragment inside the corpus. So this is a much more interactive way of looking at things. And now about functions again. If you focus just on those queries which fall into X path 3, but only using standard functions. And then because essentially none of those techniques can work if you're not using standard functions, then the combined coverage is around 78%. And code 2 now has a pretty good coverage over this XSLT and is getting a bit reasonable for X-way. So it's a good sign that if you're not using non-standard functions, you can actually get results. But what about going further? How could we use functions nevertheless? There's a lot of functions that are used in X path. Very linear arithmetic and string manipulating functions. And it turns out this hasn't been done, but it really looks like something could be done along those lines in the positive X path fragment. Because in there you can do some classical interval encoding of trees and send all of these to a SMT solver. So presumably some of those things are undecidable actually, but in practice it might work pretty well. And so we looked at what kind of coverage we could hope for with this and that's the best coverage of all actually. 62.75 coverage overall and nearly 85% for XSLT if you restrict yourself to standard functions. And also good news is that positive is the easiest fragments of all. It's an NP complete fragment. If you're using all those theories, maybe it becomes undecidable. And in practice this is really something that might work in the future. So this is this yellow extra line that you see. That's it. So for some conclusions now, so the benchmark and the modified parser are available. It's even on this software heritage repository of software. So it should be available for a long time. Some conclusions about satisfiability checking. So if you want to build a tool, I think one thing we can have demonstrated here is that the front end is really an important piece to put in for your tool. And that, yeah, you can hope to get some reasonable support for simple navigational X path as found in XSLT typically. But in Xquery somehow you have to really do some kind of program analysis, build summaries for those user defined functions and do this kind of stuff. So this becomes much more like full blown program analysis. You won't get away with just thinking of X path as a simple navigation language anymore. And the main challenge here is, yeah, how to support functions, both the standard ones and the user defined ones. And possibly if you want to have good results, it looks like SMT techniques should be the way to go. That's it. Thank you.
 It's a joint work with David Bald and Anthony Lick back at TNS in Cachon.  And the topic is pretty practical.  It's about what can we say about X-path queries in the real world.  And here's somehow the picture of what I want to talk about.  So somehow in the ether, in space, you have those really nice results.  Talking about decidable fragments.  And here decidability is about satisfiability of a query.  And this is a bit in the abstract.  The question is about, does there exist a data tree, which is a model of the formula?  And the kind of fragments that people look at typically concentrate on navigation plus  a bit of a few data tests or data joints inside your queries.  But those things have to be restricted quite a bit.  Otherwise, you will get some decidable.  On the other hand, they don't talk much about many other things that people use in X-path,  maybe function applications and so on.  And now down on Earth, you have this, well, the real X-path somehow, right?  The one that is used by people to query XML documents, which has been evolving quite a  bit right now.  This revision, which is quite recent, includes like lambda abstractions for functions and  many things, advanced programming constructs.  So there's a kind of a gap in between the two.  And we wanted to, well, get a hand at what is this gap, what it looks like.  So the way we do it really is to build a benchmark of X-path queries.  So it's an open source benchmark, so people can also play with it now.  It's reasonably big, about 20,000 queries.  And then we measured the coverage of those decidable fragments compared to this particular  benchmark.  So we first started with, let's say, Vania implementation somehow, these fragments, the  way they're written in the papers, in the various papers.  What does that give you?  And of course, as expected, that was not very good because those papers were not having  to deal with concrete X-path queries.  But there are some very straightforward extensions, most of them, that one can do in order to  get much better coverage.  And I will say a few words, of course, about what kind of results we will obtain this way.  So let's start with how we constructed this benchmark.  So we focused on two kinds of sources.  One are XSL documents, the other are Xquery documents.  Those are all open source projects so that we could also distribute the results.  There's, I think, around 20 different projects that are used.  One of the advantages of using XSL and Xquery, let's say, instead of X-path embedded in Java  or C-sharp or whatever, is that it's reasonably easy to extract the queries from the source.  So in XSL, it's just some attribute values inside your XSLT document.  So it's very easy.  In the case of Xquery, using a parser for Xquery, you can essentially find which are  the maximal sub-trees in your parse trees which are X-path and the rest is Xquery stuff.  So you can also identify what is X-path inside an Xquery document.  So in order to do that, we tuned a parser which is also provided by the W3C and the  output we get is a bunch of syntax trees and we actually express all these in an XML format  which is also a W3C format which is called XqueryX.  It's a XML presentation of Xquery documents.  Now that we have those syntax trees, we can also look at all those fragments that were  defined in the literature and for each one of them write down some schemas.  So here it turns out that reXNG was a nice formalism to write those down.  And then check for each one of those queries, is it yes or no inside the syntactic fragments  that has been considered in the literature.  So what do we get?  First of all, a few words about what we find in the benchmark itself.  So we also checked what is the coverage of the various revisions of Xpath and we make  a big distinction between XSLT and Xquery sources because the kind of queries you find  in those types of documents tend to be pretty different.  So already looking at this, you can see that in XSLT typically people use Xpath 1 mostly,  whereas in Xquery they would use more advanced syntactic constructs using Xpath 2 or Xpath  3 constructs in there.  Another point that will become quite important later is the use of functions.  So Xpath and then Xquery as well come with a bunch of standard functions.  So those functions are typically not supported at all in those, let's say, theoretical fragments  looked at in the literature but they are extensively used in practice and this you can also see  inside the benchmark.  So here's a graph showing you how those functions are used and we make a distinction between  standard functions, those that appear in this document here on the left, and non-standard  ones and those are user defined either by extending maybe your Xpath engine so you can  write this down in Java or if you're in Xquery you can define those non-standard functions  pretty easily.  And what we find is that well functions are used quite a bit, around 60% of the queries  use some function calls.  XSLT is a bit better behaved, so it's 57.23 here is the number of function calls which  are using standard functions.  And so in XSLT it's a bit better behaved, people are using standard functions more than  other ones in Xquery.  So what it means is that if you're basing let's say a tool for satisfiability of Xpath  and you don't have support for user defined function, there's really a bound on how much  you can do and here is the bound.  This new column here is showing how many queries would fit inside Xpath 3 but restricted to  standard functions.  You see that for XSLT it's still a pretty large number of queries but for Xquery you  won't cover more than 46%.  So already we can see that any attempt at building a tool for Xpath satisfiability in  Xquery documents will have to somehow manage user defined functions eventually.  All right so now I'll tell you the coverage if you implement things pre-innavably, really  taking those fragments, those syntactic fragments and looking at what you get, the coverage  is pretty poor especially in Xquery documents it's almost negligible for several of those  fragments and there's only one fragment that does pretty well.  So it's this non-mixing fragment, it has been defined to work on three patterns for XML  documents and it's essentially MSO but you have data tests and data joints as long as  you are not mixing equality and disequity tests inside your patterns and there you see  it's sort of okay, it works pretty nicely.  But okay, those fragments were not defined to cope with concrete syntax and what can  we do about this?  So the idea is now to extend those fragments and let's say that a syntactic construct can  be expressed in a fragment if you can just find or construct ideally an equivalent request  and we say it's encoded if you can find an equisatisfiable request and of course for  practical purposes you would like for all this stuff to be done in perennial time because  this essentially defines a front-end to your tool that takes in concrete syntax and outputs  abstracted syntax with which you can work in a core logic as defined in those theoretical  papers.  So what kind of extensions we've looked at?  They're pretty straightforward ones really.  So root navigations allow you to go just to the root of your XML document.  You have three variables, that's used quite a lot in practice.  So it means you have a variation that associates a bunch of nodes in elements in your XML tree  to a variable like this variable $module and you are going to go in one of those and then  continue your path.  You have data tests against constants, so that's pretty straightforward.  Data joins means that you're going here, you're checking whether you can find a path on the  left side of this equality symbol that reaches an attribute href here which has the same value  as whatever you can find using the right path.  So can you find two paths such that those two attribute values are going to be equal?  So here it means kind of find a preceding least item which has the same href value.  And another one is positional predicates, so that's used quite a bit as well.  And that's a function that you can support at least a bit, so one step positional predicates,  we looked at this how you could encode things.  And those encodings, most of them are really, really straightforward.  So for instance, root navigation is expressible in most fragments because, well, you can just,  in order to find the root, you can just go up and then test that you cannot go up anymore.  It means you are at the root, so this is something you can do in most fragments.  But surprisingly, you cannot do that everywhere, well, let's say if you're in downward x path,  just simply you don't have those axes, ancestor, self, and parent, so you cannot express it  directly.  And counting things, there you have a bit more power, so you are looking for an equisatisfiable  request, right?  And here, for instance, free variables, again, it's pretty straightforward.  You might just extend your label set to account for those free variables, for those positions  where the valuation will put those free variables.  So you can just do that.  But there are some fragments where you cannot do that.  So for instance, in forward x path, if you add either root navigation or free variables,  you will get indecidable, and this is an easy adaptation of proofs that were done by Funtiago  Figer and Luke Segoufarm.  Another example of something which is not polynomially encodable is satisfiability in  downward x path.  If you extend it with navigation predicates like position equal last and position different  from last, then it becomes a common heart, so definitely not polynomially encodable.  So here's the kind of things we get.  First, some of those syntactic constructs are actually native to those fragments.  And then we can look at which ones are expressible.  As I told you, root navigation is pretty straightforward, for instance, which ones can be encoded and  which ones cannot be encoded or not polynomial encoded.  So what we get with those easy transformations is actually quite better results already.  So if you look at the combined coverage of the entire benchmark and saying if some of  those extended fragments manages to capture some of these.  So you get around 60% coverage.  And the best individual fragment is code 2 x path.  And with these extensions, it reaches 75% of XSLT and 28% of x-way.  All right.  We also compared those fragments.  And here if you feel like playing around and seeing what kind of query is falling to this  or that fragment, there's an interactive interface that allows you to click around.  And it shows you the list of all those queries which are captured in this fragment, but not  that fragment inside the corpus.  So this is a much more interactive way of looking at things.  And now about functions again.  If you focus just on those queries which fall into X path 3, but only using standard  functions.  And then because essentially none of those techniques can work if you're not using standard  functions, then the combined coverage is around 78%.  And code 2 now has a pretty good coverage over this XSLT and is getting a bit reasonable  for X-way.  So it's a good sign that if you're not using non-standard functions, you can actually get  results.  But what about going further?  How could we use functions nevertheless?  There's a lot of functions that are used in X path.  Very linear arithmetic and string manipulating functions.  And it turns out this hasn't been done, but it really looks like something could be done  along those lines in the positive X path fragment.  Because in there you can do some classical interval encoding of trees and send all of  these to a SMT solver.  So presumably some of those things are undecidable actually, but in practice it might work pretty  well.  And so we looked at what kind of coverage we could hope for with this and that's the  best coverage of all actually.  62.75 coverage overall and nearly 85% for XSLT if you restrict yourself to standard functions.  And also good news is that positive is the easiest fragments of all.  It's an NP complete fragment.  If you're using all those theories, maybe it becomes undecidable.  And in practice this is really something that might work in the future.  So this is this yellow extra line that you see.  That's it.  So for some conclusions now, so the benchmark and the modified parser are available.  It's even on this software heritage repository of software.  So it should be available for a long time.  Some conclusions about satisfiability checking.  So if you want to build a tool, I think one thing we can have demonstrated here is that  the front end is really an important piece to put in for your tool.  And that, yeah, you can hope to get some reasonable support for simple navigational X path as  found in XSLT typically.  But in Xquery somehow you have to really do some kind of program analysis, build summaries  for those user defined functions and do this kind of stuff.  So this becomes much more like full blown program analysis.  You won't get away with just thinking of X path as a simple navigation language anymore.  And the main challenge here is, yeah, how to support functions, both the standard ones  and the user defined ones.  And possibly if you want to have good results, it looks like SMT techniques should be the  way to go.  That's it.  Thank you.
Baelde_Lick_Schmitz_0_155.png Baelde_Lick_Schmitz_156_467.png Baelde_Lick_Schmitz_468_635.png Baelde_Lick_Schmitz_636_1715.png Baelde_Lick_Schmitz_1716_2399.png Baelde_Lick_Schmitz_2400_3803.png Baelde_Lick_Schmitz_3804_4295.png Baelde_Lick_Schmitz_4296_5267.png Baelde_Lick_Schmitz_5268_7583.png Baelde_Lick_Schmitz_7584_7835.png Baelde_Lick_Schmitz_7836_8039.png Baelde_Lick_Schmitz_8040_8111.png Baelde_Lick_Schmitz_8112_9911.png Baelde_Lick_Schmitz_9912_10691.png Baelde_Lick_Schmitz_10692_11975.png Baelde_Lick_Schmitz_11976_12491.png Baelde_Lick_Schmitz_12492_13019.png Baelde_Lick_Schmitz_13020_13259.png Baelde_Lick_Schmitz_13260_14999.png Baelde_Lick_Schmitz_15000_15767.png Baelde_Lick_Schmitz_15768_17339.png Baelde_Lick_Schmitz_17340_17939.png Baelde_Lick_Schmitz_17940_18707.png Baelde_Lick_Schmitz_18708_19319.png Baelde_Lick_Schmitz_19320_21023.png Baelde_Lick_Schmitz_21024_21863.png Baelde_Lick_Schmitz_21864_23663.png Baelde_Lick_Schmitz_23664_23814.png
It's a joint work with David Bald and Anthony Lick back at TNS in Cachon. And the topic is pretty practical. It's about what can we say about X-path queries in the real world. And here's somehow the picture of what I want to talk about. So somehow in the ether, in space, you have those really nice results. Talking about decidable fragments. And here decidability is about satisfiability of a query. And this is a bit in the abstract. The question is about, does there exist a data tree, which is a model of the formula? And the kind of fragments that people look at typically concentrate on navigation plus a bit of a few data tests or data joints inside your queries. But those things have to be restricted quite a bit. Otherwise, you will get some decidable. On the other hand, they don't talk much about many other things that people use in X-path, maybe function applications and so on. And now down on Earth, you have this, well, the real X-path somehow, right? The one that is used by people to query XML documents, which has been evolving quite a bit right now. This revision, which is quite recent, includes like lambda abstractions for functions and many things, advanced programming constructs. So there's a kind of a gap in between the two. And we wanted to, well, get a hand at what is this gap, what it looks like. So the way we do it really is to build a benchmark of X-path queries. So it's an open source benchmark, so people can also play with it now. It's reasonably big, about 20,000 queries. And then we measured the coverage of those decidable fragments compared to this particular benchmark. So we first started with, let's say, Vania implementation somehow, these fragments, the way they're written in the papers, in the various papers. What does that give you? And of course, as expected, that was not very good because those papers were not having to deal with concrete X-path queries. But there are some very straightforward extensions, most of them, that one can do in order to get much better coverage. And I will say a few words, of course, about what kind of results we will obtain this way. So let's start with how we constructed this benchmark. So we focused on two kinds of sources. One are XSL documents, the other are Xquery documents. Those are all open source projects so that we could also distribute the results. There's, I think, around 20 different projects that are used. One of the advantages of using XSL and Xquery, let's say, instead of X-path embedded in Java or C-sharp or whatever, is that it's reasonably easy to extract the queries from the source. So in XSL, it's just some attribute values inside your XSLT document. So it's very easy. In the case of Xquery, using a parser for Xquery, you can essentially find which are the maximal sub-trees in your parse trees which are X-path and the rest is Xquery stuff. So you can also identify what is X-path inside an Xquery document. So in order to do that, we tuned a parser which is also provided by the W3C and the output we get is a bunch of syntax trees and we actually express all these in an XML format which is also a W3C format which is called XqueryX. It's a XML presentation of Xquery documents. Now that we have those syntax trees, we can also look at all those fragments that were defined in the literature and for each one of them write down some schemas. So here it turns out that reXNG was a nice formalism to write those down. And then check for each one of those queries, is it yes or no inside the syntactic fragments that has been considered in the literature. So what do we get? First of all, a few words about what we find in the benchmark itself. So we also checked what is the coverage of the various revisions of Xpath and we make a big distinction between XSLT and Xquery sources because the kind of queries you find in those types of documents tend to be pretty different. So already looking at this, you can see that in XSLT typically people use Xpath 1 mostly, whereas in Xquery they would use more advanced syntactic constructs using Xpath 2 or Xpath 3 constructs in there. Another point that will become quite important later is the use of functions. So Xpath and then Xquery as well come with a bunch of standard functions. So those functions are typically not supported at all in those, let's say, theoretical fragments looked at in the literature but they are extensively used in practice and this you can also see inside the benchmark. So here's a graph showing you how those functions are used and we make a distinction between standard functions, those that appear in this document here on the left, and non-standard ones and those are user defined either by extending maybe your Xpath engine so you can write this down in Java or if you're in Xquery you can define those non-standard functions pretty easily. And what we find is that well functions are used quite a bit, around 60% of the queries use some function calls. XSLT is a bit better behaved, so it's 57.23 here is the number of function calls which are using standard functions. And so in XSLT it's a bit better behaved, people are using standard functions more than other ones in Xquery. So what it means is that if you're basing let's say a tool for satisfiability of Xpath and you don't have support for user defined function, there's really a bound on how much you can do and here is the bound. This new column here is showing how many queries would fit inside Xpath 3 but restricted to standard functions. You see that for XSLT it's still a pretty large number of queries but for Xquery you won't cover more than 46%. So already we can see that any attempt at building a tool for Xpath satisfiability in Xquery documents will have to somehow manage user defined functions eventually. All right so now I'll tell you the coverage if you implement things pre-innavably, really taking those fragments, those syntactic fragments and looking at what you get, the coverage is pretty poor especially in Xquery documents it's almost negligible for several of those fragments and there's only one fragment that does pretty well. So it's this non-mixing fragment, it has been defined to work on three patterns for XML documents and it's essentially MSO but you have data tests and data joints as long as you are not mixing equality and disequity tests inside your patterns and there you see it's sort of okay, it works pretty nicely. But okay, those fragments were not defined to cope with concrete syntax and what can we do about this? So the idea is now to extend those fragments and let's say that a syntactic construct can be expressed in a fragment if you can just find or construct ideally an equivalent request and we say it's encoded if you can find an equisatisfiable request and of course for practical purposes you would like for all this stuff to be done in perennial time because this essentially defines a front-end to your tool that takes in concrete syntax and outputs abstracted syntax with which you can work in a core logic as defined in those theoretical papers. So what kind of extensions we've looked at? They're pretty straightforward ones really. So root navigations allow you to go just to the root of your XML document. You have three variables, that's used quite a lot in practice. So it means you have a variation that associates a bunch of nodes in elements in your XML tree to a variable like this variable $module and you are going to go in one of those and then continue your path. You have data tests against constants, so that's pretty straightforward. Data joins means that you're going here, you're checking whether you can find a path on the left side of this equality symbol that reaches an attribute href here which has the same value as whatever you can find using the right path. So can you find two paths such that those two attribute values are going to be equal? So here it means kind of find a preceding least item which has the same href value. And another one is positional predicates, so that's used quite a bit as well. And that's a function that you can support at least a bit, so one step positional predicates, we looked at this how you could encode things. And those encodings, most of them are really, really straightforward. So for instance, root navigation is expressible in most fragments because, well, you can just, in order to find the root, you can just go up and then test that you cannot go up anymore. It means you are at the root, so this is something you can do in most fragments. But surprisingly, you cannot do that everywhere, well, let's say if you're in downward x path, just simply you don't have those axes, ancestor, self, and parent, so you cannot express it directly. And counting things, there you have a bit more power, so you are looking for an equisatisfiable request, right? And here, for instance, free variables, again, it's pretty straightforward. You might just extend your label set to account for those free variables, for those positions where the valuation will put those free variables. So you can just do that. But there are some fragments where you cannot do that. So for instance, in forward x path, if you add either root navigation or free variables, you will get indecidable, and this is an easy adaptation of proofs that were done by Funtiago Figer and Luke Segoufarm. Another example of something which is not polynomially encodable is satisfiability in downward x path. If you extend it with navigation predicates like position equal last and position different from last, then it becomes a common heart, so definitely not polynomially encodable. So here's the kind of things we get. First, some of those syntactic constructs are actually native to those fragments. And then we can look at which ones are expressible. As I told you, root navigation is pretty straightforward, for instance, which ones can be encoded and which ones cannot be encoded or not polynomial encoded. So what we get with those easy transformations is actually quite better results already. So if you look at the combined coverage of the entire benchmark and saying if some of those extended fragments manages to capture some of these. So you get around 60% coverage. And the best individual fragment is code 2 x path. And with these extensions, it reaches 75% of XSLT and 28% of x-way. All right. We also compared those fragments. And here if you feel like playing around and seeing what kind of query is falling to this or that fragment, there's an interactive interface that allows you to click around. And it shows you the list of all those queries which are captured in this fragment, but not that fragment inside the corpus. So this is a much more interactive way of looking at things. And now about functions again. If you focus just on those queries which fall into X path 3, but only using standard functions. And then because essentially none of those techniques can work if you're not using standard functions, then the combined coverage is around 78%. And code 2 now has a pretty good coverage over this XSLT and is getting a bit reasonable for X-way. So it's a good sign that if you're not using non-standard functions, you can actually get results. But what about going further? How could we use functions nevertheless? There's a lot of functions that are used in X path. Very linear arithmetic and string manipulating functions. And it turns out this hasn't been done, but it really looks like something could be done along those lines in the positive X path fragment. Because in there you can do some classical interval encoding of trees and send all of these to a SMT solver. So presumably some of those things are undecidable actually, but in practice it might work pretty well. And so we looked at what kind of coverage we could hope for with this and that's the best coverage of all actually. 62.75 coverage overall and nearly 85% for XSLT if you restrict yourself to standard functions. And also good news is that positive is the easiest fragments of all. It's an NP complete fragment. If you're using all those theories, maybe it becomes undecidable. And in practice this is really something that might work in the future. So this is this yellow extra line that you see. That's it. So for some conclusions now, so the benchmark and the modified parser are available. It's even on this software heritage repository of software. So it should be available for a long time. Some conclusions about satisfiability checking. So if you want to build a tool, I think one thing we can have demonstrated here is that the front end is really an important piece to put in for your tool. And that, yeah, you can hope to get some reasonable support for simple navigational X path as found in XSLT typically. But in Xquery somehow you have to really do some kind of program analysis, build summaries for those user defined functions and do this kind of stuff. So this becomes much more like full blown program analysis. You won't get away with just thinking of X path as a simple navigation language anymore. And the main challenge here is, yeah, how to support functions, both the standard ones and the user defined ones. And possibly if you want to have good results, it looks like SMT techniques should be the way to go. That's it. Thank you.
decidable fragments. And here decidability is your queries. But those things have to be by people to query XML documents, which has been queries. And then we measured the coverage of very straightforward extensions, most of them, There's, I think, around 20 different projects no inside the syntactic fragments that has been those, let's say, theoretical fragments looked at in the literature but they are extensively used satisfiability of Xpath and you don't have the idea is now to extend those fragments and syntax with which you can work in a core logic as elements in your XML tree to a variable like this data tests against constants, so that's pretty add either root navigation or free variables, you last and position different from last, then it fragments. And then we can look at which ones are pretty straightforward, for instance, which ones combined coverage of the entire benchmark and saying if some of those extended fragments manages to capture some of these. So you get functions, you can actually get results. But what presumably some of those things are undecidable actually, but in practice it might work pretty in the future. So this is this yellow extra line navigation language anymore. And the main challenge here is, yeah, how to support functions, both the standard ones and the user