Marco Campion
email: marco.campion@inria.fr

Caterina Urban
email: caterina.urban@inria.fr

Mila Dalla Preda
email: mila.dallapreda@univr.it

Roberto Giacobazzi
email: giacobazzi@arizona.edu

A Formal Framework to Measure the Incompleteness of Abstract Interpretations

Keywords: Abstract Interpretation, Partial Completeness, Completeness, Program Analysis, Distances

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

The theory of Abstract Interpretation introduced by Cousot and Cousot [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF][START_REF] Cousot | Systematic design of program analysis frameworks[END_REF][START_REF] Cousot | Abstract interpretation frameworks[END_REF], is a general theory for the approximation of formal program semantics based on a simple but striking idea that extracting properties of programs' execution means over-approximating their semantics. It is an invaluable framework that helps programmers design sound-by-construction program analysis tools as it makes possible to express mathematically the link between the output of a practical, approximated analysis, also called abstract semantics, and the original, uncomputable program semantics, also called concrete semantics.

The abstract interpretation of a program P consists of an abstract domain of properties of interest A ordered by a partial-order ≤ A , a concretization map γ and an abstract interpreter • A , designed for the language used to specify P and on the abstract domain A. Let P S be the result of the concrete (collecting) program semantics on a set of concrete inputs S. Soundness means that for all possible abstract inputs S ♯ ∈ A it holds P γ(S ♯ ) ⊆ γ( P A S ♯ ). Furthermore, when P A also satisfies P γ(S ♯ ) = γ( P A S ♯ ) then P A is said to be forward-complete [START_REF] Giacobazzi | Incompleteness, counterexamples, and refinements in abstract model-checking[END_REF], while if the equation holds for a given input S ♯ ∈ A, then it is locally forward-complete at S ♯ . In abstract interpretation forward-completeness intuitively encodes the greatest achievable precision for an abstract interpreter • A applied on a program P , meaning that P A S ♯ exactly matches the concrete result of the concrete counterpart P γ(S ♯ ). When the abstraction A also admits a Galois Connection (GC) with the concrete domain through an abstraction map α, then P A is said to be backward-complete when α( P S) = P A α(S) holds for all possible concrete set of inputs S, while locally backward-complete [START_REF] Bruni | A logic for locally complete abstract interpretations[END_REF][START_REF] Bruni | A correctness and incorrectness program logic[END_REF] at S if it holds for the input S. The backward-completeness property encodes an optimal behavior of the abstract interpreter • A with respect to the abstraction in A of the concrete behavior P S. Forward-and backward-completeness and their local versions are both highly desirable properties in program analysis for verifying safety properties of programs (also called correctness properties) [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF][START_REF] Giacobazzi | Making abstract interpretations complete[END_REF][START_REF] Giacobazzi | Analyzing program analyses[END_REF][START_REF] Miné | Tutorial on static inference of numeric invariants by abstract interpretation[END_REF]. Unfortunately, it is well known that whenever a non-trivial abstract domain is used, the analysis will be necessarily (locally) forward/backward-incomplete, meaning that false alarms or spurious counterexamples will arise also for correct programs [START_REF] Giacobazzi | Analyzing program analyses[END_REF][START_REF] Campion | Partial (in)completeness in abstract interpretation: limiting the imprecision in program analysis[END_REF]. In fact, forward/backward-completeness and their local definitions in program analysis are extremely hard, if not even impossible, to achieve [START_REF] Giacobazzi | Making abstract interpretations complete[END_REF][START_REF] Campion | Partial (in)completeness in abstract interpretation: limiting the imprecision in program analysis[END_REF]. For this reason, instead of trying to reach forward/backward-completeness, we need to deal with incompleteness of both and therefore with imprecision [START_REF] Distefano | Scaling static analyses at facebook[END_REF].

In this direction, the notion of partial completeness has been introduced in [START_REF] Campion | Partial (in)completeness in abstract interpretation: limiting the imprecision in program analysis[END_REF] in order to weaken the equality requirement of the local backwardcompleteness property. Partial completeness allows a limited amount of incompleteness and this amount is measured by quasi-metrics δ A : A×A → R ∞ ≥0 ∪{⊥} (where the symbol ⊥ means undefined) compatible with the underlying abstract domain partial-ordering, where A is assumed to be a complete lattice. More specifically, for a distance function δ A being a quasi-metric A-compatible means satisfying for all a 1 , a 2 , a 3 ∈ A: (i ) the partial-ordering ≤ A : a 1 ≤ A a 2 ⇔ δ A (a 1 , a 2 ) ̸ = ⊥; (ii ) identity of indiscernibles: a 1 = a 2 ⇔ δ(a 1 , a 2 ) = 0; and (iii ) the weak triangle inequality, namely, the triangle inequality only along chains a 1 ≤ A a 2 ≤ A a 3 . So for instance, consider the intervals abstract do-main [START_REF] Cousot | Static determination of dynamic properties of programs[END_REF]

Int def = {[a, b] | a, b ∈ Z * , a ≤ b} ∪ {⊥ Int }, where Z * def
= Z ∪ {-∞, +∞}, endowed with the standard ordering ≤ Int induced by the interval containment. We can consider as quasi-metric Int-compatible the distance δ w

Int that counts how many more integer values has one interval with respect to another comparable interval. For instance, δ w

Int ([0, 0], [0, 5]) = 5, δ w Int ([0, +∞], [-2, +∞]) = 2, while δ w

Int ([0, 5], [0, 0]) = ⊥ as [0, 5] ̸ ≤ Int [0, 0]. The analysis P A α(S) on a program P with input S is said to be ε-partial complete at input S for an amount ε ∈ R ∞ ≥0 whenever δ A (α( P S), P A α(S)) ≤ ε holds, namely, the distance between the abstraction of the concrete execution and the result of the abstract interpreter is at maximum ε. In this setting, requiring 0-partial completeness at S corresponds to require local backward-completeness at S.

Main Contribution. In this paper we generalize the partial completeness property in order to be able to weaken both the local backward-completeness property in presence of a GC, and the local forward-completeness property in case only the concretization function γ is available. In this last scenario, as we may need to define distances on concrete domains, a weakening of the definition of quasi-metrics A-compatible is necessary. This is because, in the original formalization [START_REF] Campion | Partial (in)completeness in abstract interpretation: limiting the imprecision in program analysis[END_REF], the definition of quasi-metric A-compatible is specifically tailored for the structure of abstract domains and their relative partial-ordering: the axiom (i ) forces the quasi-metric to return a value different from ⊥ only if the two elements are comparable according to ≤ A , namely δ A induces the partial-order ≤ A . This is in fact not necessary: as our aim is to measure the incompleteness of an abstract interpreter with respect to the concrete execution, these two results are guaranteed to be comparable by soundness, therefore the distance may even return values on non-comparable elements as long as it is defined on all comparable ones. Moreover, the identity of indiscernibles axiom (ii ) requires the quasi-metric to be precise enough to recognize equal elements since it constraints the distance to return zero whenever the two elements are equal. This is a too strong requirement especially in the scenario where only γ is available and we have to define a distance on the concrete domain where elements contain more information than what we are interested in for measuring the incompleteness. For instance, by considering the concrete domain ℘(Z n ) where n is the number of variables used in a program and elements in S ∈ ℘(Z n ) are program states, we might need a distance function δ ℘(Z n ) that measures the imprecision of certain variables only, say x and y. A possible estimate of this imprecision could be done by calculating the volume of their abstraction into the intervals abstract domain, namely, the area of the rectangle abstracting the values of x and y.

To this end, in Section 3 we reason on the weakest axioms that a distance function should meet so that it can be used to measure the local forward/backwardincompleteness. We just require a relaxed version of the identity of indiscernibles axiom (only the left-implication) and a condition on chains. As domains may not be complete lattices or partial-orders, such as the convex polyhedra abstract domain [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF], we only require one of the weakest form of ordering relation known as a pre-order. The resulting distance function will be called pre-metric ⪯ Dcompatible where D is a pre-ordered set according to the pre-order ⪯ D . We will provide several useful examples of pre-metrics compatible to generic pre-ordered sets, as well as well-known numerical abstract domains, that can be used in practice. In Section 4 we show how this newly defined notion of pre-metric ⪯ Dcompatible allows us to derive other pre-metrics from one domain to another by exploiting the concretization γ or, when available, the abstraction map α. Finally, in Section 5 we define the new properties partial backward-completeness and partial forward-completeness using pre-metrics compatible with the underlying domain ordering. We show that, when a certain condition on the precision of the pre-metric is met, then we can characterize the local forward/backwardcompleteness as the 0-partial forward/backward-completeness. The proposed framework is general enough to be instantiated by most known metrics for abstract interpretation [START_REF] Crazzolara | Quasi-metric spaces as domains for abstract interpretation[END_REF][START_REF] Logozzo | Towards a quantitative estimation of abstract interpretations[END_REF][START_REF] Sotin | Quantifying the precision of numerical abstract domains[END_REF][START_REF] Casso | Computing abstract distances in logic programs[END_REF][START_REF] Campion | Partial (in)completeness in abstract interpretation: limiting the imprecision in program analysis[END_REF]. Since imprecision, i.e., incompleteness, is unavoidable in program analysis, our ambition is to help abstract interpretation designers in defining distances able to measure the imprecision they want to track regardless of the domain on which they want to define the distance, hence providing the appropriate tools to fully control the imprecision propagation.

Background

Orderings. Given two sets S and T , ℘(S) denotes the powerset of S, ∅ is the empty set, S ⊆ T denotes sets inclusion, |S| denotes the cardinality where S is finite if |S| < ω, countably infinite if |S| = ω, countable if |S| ≤ ω. A binary relation ∼ over a set S is a subset of the Cartesian product ∼⊆ S × S. We will emphasize the set S on which a binary relation ∼ is defined by the subscript ∼ S except for the straightforward equivalence relation = unless it has a different definition. We denote with Z and R the sets of all, respectively, integer and real numbers. We will use subscripts in order to limit their range, while the superscript symbol ∞ denotes the inclusion of the infinite symbol. For example, R ∞ ≥0 denotes the set of all non-negative real numbers together with the symbol

∞ such that, for all ε ∈ R ≥0 , ε < ∞. A binary relation ⪯ L ∈ ℘(L×L) is a pre-order iff it is reflexive (∀l ∈ L. l ⪯ L l) and transitive (∀l 1 , l 2 , l 3 ∈ L. l 1 ⪯ L l 2 ∧ l 2 ⪯ L l 3 ⇒ l 1 ⪯ L l 3 ). A set L endowed with a pre-order relation ⪯ L is called a pre-ordered set, and it is denoted by (L, ⪯ L ). Furthermore, if ⪯ L is anti-symmetric (∀l 1 , l 2 ∈ L. l 1 ⪯ L l 2 ∧ l 2 ⪯ L l 1 ⇒ l 1 = l 2 )
then it is a partial-order and the pair (L, ⪯ L ) is called a partiallyordered set. Clearly, every partially-ordered set is also a pre-ordered set. A subset

Y ⊆ L of a pre-ordered set (L, ⪯ L ) is a chain iff for all y 1 , y 2 ∈ Y , y 1 ⪯ L y 2 or y 2 ⪯ L y 1 .
Measures and Distances. A σ-algebra on a set X is a collection of subsets of X that includes X itself, it is closed under complement and it is closed under countable unions. The definition implies that it also includes the empty set ∅ and that it is closed under countable intersections. Consider a σ-algebra A over X. The tuple (X, A) is called a measurable space.

Definition 1 (Measure). A function µ : A → R ∞ ≥0 is called a measure iff it satisfies the following properties:

(1) non-negativity: ∀S ∈ A. µ(S) ≥ 0;

(2) null empty set: µ(∅) = 0;

(3) countable additivity: if S i ∈ A is a countable sequence of disjoint sets, then µ( i S i ) = i µ(S i ). The triple (X, A, µ) is called a measure space. ■

A metric is a function that defines a distance between pairs of elements of a set S. Formally: Definition 2 (Metric). A metric on a non-empty set S is a map δ S : S × S → R ≥0 that ∀x, y, z ∈ S satisfies:

(1) identity of indiscernibles: x = y ⇔ δ S (x, y) = 0;

(2) symmetry: δ S (x, y) = δ S (y, x);

(3) triangle inequality: δ S (x, z) ≤ δ S (x, y) + δ S (y, z). A set provided with a metric is called a metric space. ■

A function δ S : S × S → R ≥0 satisfying all axioms of Definition 2 except for symmetry, is called a quasi-metric, while if δ S does not satisfy the ⇐ direction of the identity of indiscernibles axiom then it is called a pseudo-metric. A pseudoquasi-metric relaxes both the indiscernibility axiom and the symmetry axiom of a metric. δ S is said to be a pre-metric if it satisfies only the ⇐ implication of the identity of indiscernibility axiom (symmetry and triangle inequality may not hold).

Abstract Interpretation. We consider here the abstract interpretation framework as defined in [START_REF] Cousot | Abstract interpretation frameworks[END_REF] and based on the correspondence between a domain of concrete or exact properties C and a domain of abstract or approximate properties A.

Concrete and abstract domains are assumed to be at least pre-ordered sets, respectively (C, ⪯ C ) and (A, ⪯ A ), and be related by a monotone concretization function γ : A → C. Furthermore, when they enjoy a Galois Connection (GC) through a monotone abstraction function α : C → A, denoted by the symbols

(C, ⪯ C ) ---→ ← --- α γ (A, ⪯ A ), then for all a ∈ A and c ∈ C: α(c) ⪯ A a ⇔ c ⪯ C γ(a).
A GC is a Galois Insertion (GI), denoted by (C, ⪯ C ) ---→ -→ ← ---α γ (A, ⪯ A ), when it holds α • γ = id , where • denotes functions composition and id is the identity function. A concrete element c ∈ C is said to be exactly representable in the abstract domain A when γ(α(c)) = c. Soundness and Completeness. Let f C : C → C be a concrete monotone operator (to keep notation simple we consider unary functions) and let f A : A → A be a corresponding monotone abstract operator defined on some abstraction A. Then, f A is a sound (or correct) approximation of f C on A when for all a ∈ A, f C (γ(a)) ⪯ C γ(f A (a)) holds. When dealing with GCs, between all abstract functions that approximate a concrete one we can define the most precise one called best correct approximation (bca for short): [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. Given an abstract input a ∈ A, when the concretization of f A (a) matches the concrete counterpart f C (γ(a)) then f A is said to be locally forward-complete1 at the input a ∈ A.

f α A def = α • f C • γ. It turns out that any abstract function f A is a correct approximation of f C if and only if it holds f α A ⪯ A f A
Definition 3 (Local forward-completeness). Let f A : A → A be a sound approximation of f C : C → C. Given an input a ∈ A, f A is said to be locally forward-complete at the input a, when f C (γ(a)) = γ(f A (a)) holds. ■

When C and A admit a GC, then we can also define the property of local backward-completeness [START_REF] Bruni | A logic for locally complete abstract interpretations[END_REF][START_REF] Bruni | A correctness and incorrectness program logic[END_REF].

Definition 4 (Local backward-completeness). Let (C, ⪯ C ) ---→ ← --- α γ (A, ⪯ A ) and f A be a sound approximation of f C . Given an input c ∈ C, f A is said to be locally backward-complete at the input c, when α(f C (c)) = f A (α(c)). ■
The local forward-and backward-completeness properties are a weakening of the standard notions of forward- [START_REF] Giacobazzi | Incompleteness, counterexamples, and refinements in abstract model-checking[END_REF] and backward-completeness2 [20,21,33], respectively, which require Definition 3 and 4 to hold over all possible, respectively, abstract and concrete inputs. Intuitively, when f A is an abstract transfer function on A used in some static program analysis algorithm, local backwardcompleteness at input c ∈ C encodes an optimal precision for f A at input α(c), meaning that the abstract behavior of f A (α(c)) on A exactly matches the abstraction in A of the concrete behavior of f C (c). On the other hand, if f A is locally forward-complete at the abstract input a ∈ A means that f A acts on the abstract input a precisely as f C does on its concretization. As a remark, when f A is locally forward-complete on an input a ∈ A and (C,

⪯ C ) ---→ -→ ← ---- α γ (A, ⪯ A ), then f A is locally backward-complete at γ(a), namely, f A (a) corresponds to the bca f α A (a).
A relaxation of Definition 4 has been introduced in [START_REF] Campion | Partial (in)completeness in abstract interpretation: limiting the imprecision in program analysis[END_REF], called partial completeness, where quasi-metrics compatible with the underlying abstract domain are considered to measure the imprecision of f A (α(c)) compared to α(f C (c)).

Definition 5 (ε-Partial (backward-)completeness). Consider the Galois Connection

(C, ⪯ C ) ---→ ← --- α γ (A, ⪯ A ), a sound approximation f A of f C , a quasi- metric δ A A-compatible, and ε ∈ R ∞ ≥0 . The abstract operator f A is said to be an ε-partial (backward-)complete approximation of f C on input c ∈ C when the following inequality holds: δ A (α(f C (c)), f A (α A (c))) ≤ ε. ■ Establishing ε-partial (backward-)completeness at input c ∈ C of an abstract op- erator f A , means that when computing f A (α(c))
, the output result is allowed to have an imprecision limited to ε compared to the abstraction of the concrete execution at c, namely, α(f C (c)). The meaning of the value ε depends on the quasimetric A-compatible chosen. Note that the ε-partial (backward-)completeness property is always considered with respect to a specified input.

Distances on Orderings

The goal of this section is to set the minimum requirements that a distance function must meet so that it can be used to measure the local forward/backwardincompleteness generated by a sound abstract function f A : A → A, operating on a set of approximated properties A, with respect to the concrete function f C : C → C, operating on a set of properties C some of which may be undecidable. The target distance function could be defined either on the concrete domain C in order to calculate the distance between f C (γ(a)) and γ(f A (a)) for an input a ∈ A, that is the local forward-(in)completeness, or, e.g. when they enjoy a GC, directly on the abstract domain A for measuring the distance between α(f C (c)) and f A (α(c)) for c ∈ C, that is the local backward-(in)completeness (as, e.g., formalized in [START_REF] Campion | Partial (in)completeness in abstract interpretation: limiting the imprecision in program analysis[END_REF] through the use of quasi-metrics).

In abstract interpretation both C and A are often based on a qualitative notion of precision in order to know when an element is more precise respect to another. More generally, given an unordered set D, a basic relation able to accomplish this task is a pre-order relation ⪯ D ∈ ℘(D × D) where x ⪯ D y for x, y ∈ D intuitively means that y approximates x [START_REF] Cousot | Abstract interpretation frameworks[END_REF]. Therefore, we need to define a general notion of distance able to exploit any pre-ordered structure. Let us informally analyze each property that we may expect on a distance measuring the local incompleteness, either backward or forward, of abstract interpretations.

When comparing two elements x, y ∈ D in a pre-ordered set (D, ⪯ D ), the distance function δ D (x, y) must return a non-negative real value for all x, y ∈ D. We also give δ D the possibility to return the symbol ∞ meaning an infinite distance between two elements. Thus, the type of a distance function δ D will be:

δ D : D × D → R ∞ ≥0 (0)
If we are calculating the distance between two identical elements, then we expect δ D to output zero:

x = y ⇒ δ D (x, y) = 0
(1) However, we do not require the converse implication: we allow x ̸ = y even if δ D (x, y) = 0. This gives us the freedom to say that, e.g., the distance between two distinct elements is zero because the distance itself is considering the information represented by x and y up to some abstraction of interest. That is, the distance itself can be considered as another layer of approximation between the elements of D and, thus, it may output zero even if they are represented differently in D. For example, consider the poset (℘(Z), ⊆) corresponding to the powerset of integers together with the subset inclusion relation (i.e., a partialorder). Given two sets X, Y ∈ ℘(Z) such that X ⊆ Y (e.g., X = {2, 9, 19} and Y = {2, 9, 15, 19}), we might be interested in a function δ ℘(Z) that calculates the distance of an approximated representation of both X and Y , for instance, by taking their interval abstraction. In this case, it might happen that X and Y are mapped to the same interval (i.e., the interval [2, 19] for the chosen X and Y) and therefore δ ℘(Z) (X, Y ) = 0 even though X ̸ = Y . As another example, when considering the convex polyhedra domain (Poly, ⪯ Poly ) [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] over R n we might want that the distance between two polyhedra p 1 , p 2 ∈ Poly is zero when they represent the same set of vectors in R n . That is, if γ(p 1 ) = γ(p 2 ) then δ Poly (p 1 , p 2 ) = 0 even if p 1 and p 2 are represented by different inequalities in Poly, i.e., p 1 ̸ = p 2 . The requirements (0)-(1) define δ D to be a generalization of a metric: by relaxing the identity of indiscernibles axiom and dropping the symmetry and triangle inequality axioms of metrics, we get a pre-metric 3 . Similarly to the relation between pre-orders and other stronger orderings (e.g., partial-orders and equivalence relations), pre-metrics are more general than pseudoquasi-metrics, quasi-metrics and metrics (see Section 2): a pre-metric satisfying the triangle inequality axiom is a pseudoquasi-metric, furthermore if it also satisfies the identity of indiscernibles then it is a quasi-metric, while a symmetric quasi-metric is a metric. Pre-metrics can be considered as one of the weakest forms of distance functions from which we can build on top of pre-ordered sets.

Until now the definition of pre-metric does not consider the pre-order relation between elements of D. Recall that we are interested in computing a distance between the result of a concrete operator f C working on (C, ⪯ C ) and a sound abstract operator f A working on (A, ⪯ A ). Therefore, we already know that for any a ∈ A the two results f C (γ(a)) and γ(f A (a)) are comparable according to ⪯ C , namely f C (γ(a)) ⪯ C γ(f A (a)) thanks to the soundness assumption of f A . This means that our definition of distance should have a meaning when used to calculate distances between elements being part of the same chain, i.e., comparable according to ⪯ D , while we do not care about the result of δ D (x, y) when x ̸ ⪯ D y. That said, suppose x, y, z ∈ D are related by x ⪯ D y ⪯ D z, i.e., z is an approximation of y and y approximates x. If we ascend the chain from x to y, then we would expect that the remaining distance from y to z to be less than or equal the entire distance from x to z. Similarly, if we descend the chain from z to y then we would expect the remaining distance from x and y to be less than or equal the whole distance from x to z. Formally:

x ⪯ D y ⪯ D z ⇒ δ D (x, y) ≤ δ D (x, z) ∧ δ D (y, z) ≤ δ D (x, z) (2)
This axiom gives us the possibility to reason on distance results between elements on the same chain. For example, suppose that the concrete and abstract domains are related by a GC (C, ⪯ C ) ---→ ← --α γ (A, ⪯ A ) and that we have defined a distance δ A on the elements of A. Given an input c ∈ C, we already know that the result of the bca of f C on A is in the middle between the abstraction of f C (c) and the result of the abstract sound operator f A (α(c)), namely, it holds α(f

C (c)) ⪯ A f α A (α(c)) ⪯ A f A (α(c)).
In this case, we would expect that the distance between α(f C (c)) and the best possible approximation of f C , i.e., δ A (α(f C (c)), f α A (α(c))) to be less than or equal to the distance between the concrete and the chosen abstract operator f A , namely, δ A (α(f C (c)), f A (α(c))), and the same for δ A (f α A (α(c)), f A (α(c))). Note that the triangle inequality axiom required by metrics and some of their weakening, like pseudo-metrics and quasi-metrics, does not imply axiom (2), and (2) does not imply the triangle inequality. For example, if

D = {x, y, z} with x ⪯ D y ⪯ D z and δ D (x, y) = 2, δ D (y, z) = 1, δ D (x, z) = 1, then δ D (x, z) = 1 < 3 = δ D (x, y) + δ D (y, z) but δ D (x, y) = 2 > δ D (x, z) = 1. Instead, if δ D (x, y) = 1, δ D (y, z) = 1, δ D (x, z) = 3 then (2) holds while δ D (x, z) = 3 > 2 = δ D (x, y) + δ D (y, z).
In fact, we do not require the triangle inequality axiom (neither its weaker form on chains as formalized, e.g., in [START_REF] Crazzolara | Quasi-metric spaces as domains for abstract interpretation[END_REF][START_REF] Logozzo | Towards a quantitative estimation of abstract interpretations[END_REF][START_REF] Campion | Partial (in)completeness in abstract interpretation: limiting the imprecision in program analysis[END_REF]): as we are focusing on incompleteness results and, therefore, elements on chains according to the ordering ⪯ D , the distance δ D (x, z) could be greater or lower than the sum between δ D (x, y) and δ D (y, z) as long as it respects (2).

We now have all the ingredients needed to formalize the distance that matches our purposes: it must be a pre-metric (axioms (0)-( 1)) compatible with the underlying pre-order (axiom (2)). Functions that meet these requirements over a pre-ordered set (D, ⪯ D ) are called pre-metrics ⪯ D -compatible.

Definition 6 (Pre-metric ⪯ D -compatible). Let (D, ⪯ D ) be a pre-ordered set. The function δ D : D × D → R ∞
≥0 is a pre-metric ⪯ D -compatible if and only if the following axioms are satisfied for all x, y, z ∈ D:

(1) x = y ⇒ δ D (x, y) = 0; (2) x ⪯ D y ⪯ D z ⇒ δ D (x, y) ≤ δ D (x, z) ∧ δ D (y, z) ≤ δ D (x, z). ■
Pre-ordered sets equipped with a compatible pre-metric are called pre-metric ⪯ D -compatible spaces.

Definition 7 (Pre-metric ⪯ D -compatible space). Given a pre-ordered set (D, ⪯ D ) and a pre-metric ⪯ D -compatible δ D , the triple (D, ⪯ D , δ D ) is a premetric ⪯ D -compatible space. We use P re((D, ⪯ D )) to refer to the the set of all pre-metric ⪯ D -compatible spaces:

(D, ⪯ D , δ D ) ∈ P re((D, ⪯ D )). ■
The following is a list of pre-metrics compatible with a generic pre-ordered set (D, ⪯ D ) or tailored for specific domains.

Example 1 (Zero-distance). One of the most trivial pre-metric ⪯ D -compatible definable on any pre-ordered set is the distance that always returns the value zero for all x, y ∈ D:

δ 0 D (x, y) def = 0
Although it satisfies all axioms from Definition 6, it does not provide any information about the distance between elements in D since it treats them as they are close to each other. ♦

Example 2 (Ordering-distance). The following distance

δ ⪯ D D (x, y) def =    0 if x = y, 1 if x ̸ = y ∧ x ⪯ D y, ∞ otherwise
is clearly a pre-metric ⪯ D -compatible. In fact, it extends the pre-order relation ⪯ D with the function δ ⪯ D D having three output values: 0 for equal elements, 1 for not equal but comparable elements and ∞ for non-comparable elements. ♦ Example 3 (Measure-distance). Let (Z, D, µ) be a measure space, i.e., D be a domain that forms a σ-algebra over a set Z and µ : D → R ∞ ≥0 be a measure function. We define the function δ µ D for every X, Y ∈ D as follows:

δ µ D (X, Y ) def = Av(µ(Y ) -µ(X))
where Av is the absolute value function. Note that, because D is composed by measurable properties, δ µ D can exploit the measure function µ in order to quantify the distance between elements of D. However, depending on how ⪯ D is defined, it still may not be a pre-metric ⪯ D -compatible as axiom (2) may be violated. Let us show two examples where δ µ D is compatible with ⪯ D . Consider the measure space (D, ℘(D), µ c ), where (℘(D), ⊆) and µ c is the

counting measure, namely, for all X ∈ ℘(D), µ c (X) def = |X| if |X| is finite, ∞ otherwise. Intuitively, δ µ c ℘(D) (X, Y
) counts the elements in X and Y and returns the absolute value of their difference. Note that: axioms (0)-(1) are satisfied since δ µ c ℘(D) (X, Y ) is either non-negative or ∞, and if X = Y then they have the same number of elements which implies4 δ µ c ℘(D) (X, Y ) = 0. Furthermore, axiom (2) holds as X ⊆ Y ⊆ Z implies that Z has more elements than Y and Y has more elements than X, thus ascending (resp. descending) a chain implies that the distance will increase (resp. decrease). The function δ µ c ℘(D) fulfills all axioms (0)-(2) and, therefore, it is a pre-metric ⊆-compatible. Dually, the same reasoning holds with ℘(D) being partially-ordered by ⊇. This is one of the most common distance used for evaluating the outcome of a program analysis: you simply count the elements generated by the abstract analysis and the elements generated by the concrete execution and then the absolute value of the difference tells you the quality of the analysis result. The bigger this difference is, the worse the result will be. ♦

Example 4 (Volume-distance). Let us consider the pre-ordered domain of convex polyhedra (Poly, ⪯ Poly ). We define the pre-metric

δ Vol Poly (p 1 , p 2 ) def = Av(Vol(p 1 ) -Vol(p 2 ))
calculating the absolute value of the difference between the volume of two convex polyhedra p 1 , p 2 ∈ Poly. The volume function Vol : Poly → R ∞ ≥0 could be a monotone (namely, if γ(p 1 ) ⊆ γ(p 2 ) then Vol(p 1 ) ≤ Vol(p 2 )) overapproximation of the exact volume computation (see, e.g., [START_REF] Cohen | Two algorithms for determining volumes of convex polyhedra[END_REF][START_REF] Lawrence | Polytope volume computation[END_REF]). This means that Vol may not be a measure according to Definition 1 as the countable-additivity axiom may be violated. However, δ Vol

Poly satisfies the two axioms of Definition 6 and therefore it is ⪯ Poly -compatible. ♦

Example 5 (Trace-Length distance). Let Σ be a set of program states and let

Σ +∞ def = Σ + ∪ Σ ∞
be the set of all non-empty finite (Σ + ) and infinite (Σ ∞ ) sequences of program states. We consider the domain of sets of program traces ordered by set inclusion, i.e., (℘(Σ +∞ ), ⊆), and define the following function function Len : ℘(Σ +∞ ) → R ∞ ≥0 :

Len(T ) def =      0 if T = ∅, max{|σ| | σ ∈ T } if T ∩ Σ ∞ = ∅, ∞ otherwise
where |σ| applied on a trace denotes its length. Len computes the length of the longest program trace in a set of traces T . The following pre-metric

δ Len ℘(Σ +∞ ) (T 1 , T 2 ) def = Av(Len(T 1 ) -Len(T 2 ))
looking at the absolute value of the difference between the lengths of the longest traces in two sets T 1 , T 2 ∈ ℘(Σ +∞ ) is a pre-metric ⊆-compatible. Note that Len(T ) does not form a measure as the countable-additivity axiom does not hold. ♦

Example 6 (Weighted path-length distance). We consider the weighted path-length distance δ w D defined in [START_REF] Campion | Partial (in)completeness in abstract interpretation: limiting the imprecision in program analysis[END_REF] for posets. We propose a slightly modified version able to work with any pre-ordered structures (D, ⪯ D ). Intuitively, δ w D considers a preordered set as a directed weighted graph where the set of edges

E D ⊆ D × D is defined as E D def = {(x, y) | x ≺• D y}
, and w : E D → R ≥0 is the weight function which assigns a non-negative real value to each edge. The relation x ≺• D y is true whenever x ≺ D y and there is no element z ∈ D such that x ≺ D z ≺ D y. Clearly, if ⪯ D is a partial-order then the graph is acyclic. Given x, y ∈ D such that x ̸ = y, let C y x denotes the set of all possible chains c ⊆ E D between x and

y such that if (z, u) ∈ c then x ⪯ D z ≺• D u ⪯ D y. It is clear that if x ̸ ⪯ D y then C y x = ∅. The weighted path-length distance δ w D : D × D → R w ≥0 is defined as follows: δ w D (x, y) def =        0 if x = y, ∞ if ∀c ∈ C y x . |c| = ω, min e∈c w(e) c ∈ C y x |c| < ω if ∃c ∈ C y x . |c| < ω.
Intuitively, when δ w D is used to calculate the distance between x and y such that x ≺ D y then it outputs the minimum weighted path w.r.t. w between x and y, while if x ̸ ⪯ D y then it outputs ∞. Note that δ w D is a pre-metric that does not satisfy symmetry, while it satisfies the triangle inequality axiom only on chains. However, it may not be compatible with the underlying ordering ⪯ D as axiom (2) may turn false. For instance, consider the Sign def = {Z, -, 0, +, ∅} domain for sign analysis of integer variables [START_REF] Cousot | Static determination of dynamic properties of programs[END_REF]. Sign is ordered by the following partial-order: ∅ ⪯ Sign 0 ⪯ Sign -⪯ Sign Z and ∅ ⪯ Sign 0 ⪯ Sign + ⪯ Sign Z. Suppose the weight function w assigns w((0, -)) = 5 while for the others couple (a, b) ∈ E Sign , w((a, b)) = 1. Then, the weighted path-length δ w

Sign is not a pre-metric ⪯ Signcompatible as δ w Sign (0, -) = 5 > 2 = δ w Sign (0, Z) thus violating (2). On the other hand, if we set ∀(a, b) ∈ E Sign , w((a, b)) = 1 then we get a pre-metric ⪯ Signcompatible.

As a final case of application of δ w D , consider the domain of integer intervals Int also known as the box domain. Given any two intervals

i 1 , i 2 ∈ Int such that (i 1 , i 2 ) ∈ E Int , if we define w((i 1 , i 2 )) = 1, then δ w
Int is a pre-metric ⪯ Int -compatible. Intuitively, δ w Int (i 1 , i 2 ) for i 1 ⪯ Int i 2 counts how many more elements one interval has compared to the other: if δ w Int (i 1 , i 2 ) = k for some k ∈ N, then the interval i 2 contains exactly k more elements than i 1 . For instance, δ w

Int ([0, 0], [-1, 2]) = 3 as the interval [-1, 2] has 3 more elements than the singleton [0, 0], namely: -1, 1, 2; δ w Int ([0, 10], [0, +∞]) = ∞ as [0, +∞] has an infinite number of more elements than [0, 10], while δ w Int ([0, +∞], [-5, +∞]) = 5. ♦ When a pre-metric ⪯ D -compatible is precise enough to assign zero only when two comparable elements are identical, namely, when it satisfies the identity of indiscernibles axiom on chains, it will be called strong. Poly with Vol overapproximating the real volume, and the trace-length distance δ Len ℘(Σ +∞ ) defined in Example 5, are not. We will see in Section 5 that strong pre-metrics ⪯ D -compatible play an important rule when measuring the local forward/backward-incompleteness of abstract interpretations.

As a last note, it is worth noting that Definition 6 is general enough to be instantiated with other definitions of metrics specifically tailored in the context of abstract interpretation. For instance, if a pre-metric ⪯ D -compatible δ D is also symmetric and it satisfies the weak triangle inequality then it is a pseudo-metric ⪯ D -compatible according to [START_REF] Logozzo | Towards a quantitative estimation of abstract interpretations[END_REF], whereas if δ D both induces the underlying order relation, it is strong and it satisfies the weak triangle inequality then it is a quasi-metric ⪯ D -compatible [START_REF] Campion | Partial (in)completeness in abstract interpretation: limiting the imprecision in program analysis[END_REF][START_REF] Crazzolara | Quasi-metric spaces as domains for abstract interpretation[END_REF].

Deriving Pre-Metrics from Domains

Concrete C and abstract A domains of properties in abstract interpretation are often related by a monotonic concretization function γ : A → C and sometimes additionally by a monotonic abstraction function α : C → A that maps a concrete element to the best (i.e., the smallest according to ⪯ A ) abstract element approximating it, such that (C, ⪯ C ) ---→ ← --α γ (A, ⪯ A ) forms a GC. By exploiting these structures we can derive pre-metrics from one domain to another.

Given a pre-metric compatible with the concrete domain (C, ⪯ C ), we can exploit the concretization function γ to derive a pre-metric compatible with the underlying abstract domain ordering (A, ⪯ A ). Here a GC between C and A is not necessary. Definition 9 (Induced distance from the concrete domain). Consider (C, ⪯ C , δ C ) ∈ P re((C, ⪯ C )). For all a 1 , a 2 ∈ A, we define:

⇁ δ A (a 1 , a 2 ) def = δ C (γ(a 1 ), γ(a 2 ))
as the pre-metric induced on A from (C, ⪯ C , δ C ). ■ Proposition 1. The following statements hold:

(i) (A, ⪯ A , ⇁ δ A ) is a pre-metric ⪯ A -compatible space; (ii) if δ C is strong and γ is injective then ⇁ δ A is strong. ⊓ ⊔
Furthermore, given (A, ⪯ A , δ A ) ∈ P re((A, ⪯ A )), when the concrete and abstract domains admit a GC through an abstraction function α : C → A, we can derive the pre-metric ⪯ C -compatible on the concrete properties (C, ⪯ C ). This distance will be called the induced distance from the abstract pre-metric ⪯ Acompatible space.

Definition 10 (Induced distance from the abstract domain). Let the concrete and abstract domains be correlated by a GC (C, ⪯ C ) ---→ ← --α γ (A, ⪯ A ). Moreover, let (A, ⪯ A , δ A ) ∈ P re((A, ⪯ A )) be a pre-metric ⪯ A -compatible space. For all c 1 , c 2 ∈ C, we define:

↽ δ C (c 1 , c 2 ) def = δ A (α(c 1 ), α(c 2 )) as the pre-metric induced on C from (A, ⪯ A , δ A ). ■ Proposition 2. (C, ⪯ C , ↽ δ C ) is a pre-metric ⪯ C -compatible space. ⊓ ⊔
The derived pre-metric on the concrete properties is compatible with ⪯ C as it measures the distance between two concrete elements by throwing away nonrelevant information according to the abstraction α. Note how Definition 9 and Definition 10 define a way to build pre-metrics on domains correlated by a concretization function and/or an abstraction function.

This means that the distance itself δ D defined on a pre-ordered domain D, can view properties of D on different levels of precision: δ D can exploit a more approximated pre-metric δ A defined on an abstraction of properties A of D, e.g. we can use

↽ δ D when (D, ⪯ D ) ---→ ← --- α γ (A, ⪯ A ).
Alternatively, δ D can exploit a more precise distance δ C , for instance when δ C is defined on a more precise domain C related with D through the concretization γ : D → C, then we can use ⇁ δ D . We can also combine distances in a way similar to combining abstractions.

Example 7. Let Zone be the zone domain [START_REF] Miné | A new numerical abstract domain based on difference-bound matrices[END_REF], and Oct be the octagon domain [START_REF] Miné | The octagon abstract domain[END_REF]. Both are relational domains, with Oct more precise than Zone, able to infer affine relationships (inequalities) between variables, although in a more restricted form respect to Poly. Consider the volume-distance δ Vol

Poly defined on convex polyhedra in Example 4. We can systematically derive other volumedistances on domains which can be represented by Poly, e.g., Int, Zone and Oct. For instance, given γ Oct : Oct → Poly, γ Zone : Zone → Poly, γ Int :

Int → Poly, for all o 1 , o 2 ∈ Oct, z 1 , z 2 ∈ Zone, i 1 , i 2 ∈ Int we get ⇁ δ Vol Oct (o 1 , o 2 ) = δ Vol Poly (γ Oct (o 1 ), γ Oct (o 2 )) ⇁ δ Vol Zone (z 1 , z 2 ) = δ Vol Poly (γ Zone (z 1 ), γ Zone (z 2 )) ⇁ δ Vol Int (i 1 , i 2 ) = δ Vol Poly (γ Int (i 1 ), γ Int (i 2 )) ♦
Depending on a number of factors such as the imprecision we want to track, the quantity of information represented by a domain, and/or the computational complexity needed to implement δ D , we may switch from one domain to another. This procedure is also common in program analysis by abstract interpretation where it can be useful to convert between one abstract domain and another, for instance to switch abstract domains dynamically during the analysis or benefit from abstract operators available in other more abstract domains (see, e.g., [START_REF] Cousot | Principles of Abstract Interpretation[END_REF][START_REF] Miné | Tutorial on static inference of numeric invariants by abstract interpretation[END_REF]).

Example 8. Let us consider as concrete domain (℘(Z n ), ⊆) and the abstract pre-metric ⪯ Int -compatible space (Int, ⪯ Int , δ w Int ) of intervals together with the weighted path-length defined in Example 6. We can derive the pre-metric

↽ δ ℘(Z n ) (S 1 , S 2 ) = δ w Int (α i (S 1 ), α i (S 2 ))
where for all S 1 , S 2 ∈ ℘(Z n ), α i : ℘(Z n ) → Int calculates the interval of the i-th component only, with 1 ≤ i ≤ n, of set of vectors S 1 and S 2 . For instance, if n = 3 and S 1 = {⟨1, 9, 9⟩, ⟨1, 0, 10⟩}, S 2 = {⟨1, 5, 0⟩, ⟨-1, 0, 10⟩, ⟨5, 0, 0⟩} [START_REF] Bruni | A logic for locally complete abstract interpretations[END_REF], and their distance is

then α 1 (S 1 ) = [1, 1], α 1 (S 2 ) = [-1,
↽ δ ℘(Z n ) (S 1 , S 2 ) = δ w Int ([1, 1], [-1, 5]) = 6.
This can be useful, e.g., when σ ∈ S represents a program state and the i-th component of σ corresponds to the value of a program variable, thus,

↽ δ ℘(Z n ) (S 1 , S 2
) is interested in calculating the imprecision of that variable only. ♦

Partial Forward/Backward-Completeness Properties

As already mentioned in Section 2, Campion et al. in [START_REF] Campion | Partial (in)completeness in abstract interpretation: limiting the imprecision in program analysis[END_REF] proposed a relaxation of the local backward-completeness through the use of quasi-metrics, leading to Definition 5. More specifically, they require C and A to be complete lattices and related by a GC. In their formalization, the use of quasi-metrics enforces distance functions to adhere precisely to the underlying partial-ordering (namely, returning a distance for comparable elements only), and to output zero only when both elements are equal (corresponding to (1) but with both implications). These conditions imply that, if we want to define a quasi-metric on the concrete properties C, the distance function must be precise enough to distinguish when two concrete elements are equal, thus limiting the possibility to choose, e.g., computationally less expensive distances at the cost of losing precision. For instance, the volumedistance defined in Example 4 on Poly would not be possible as a quasi-metric Poly-compatible unless Vol exactly calculates the volume of a convex polytope, which has exponential complexity. Similarly, defining a distance that partially considers the information encoded in the concrete elements, e.g. the imprecision of a specific program variable (Example 8), is not allowed.

In this section we exploit the newly introduced notion of pre-metrics ⪯ Dcompatible to weaken both definitions of local forward-completeness (Definition 3) and local backward-completeness (Definition 4). Thanks to the weaker requirements of pre-metrics, we ask C and A to have fewer structures compared to [START_REF] Campion | Partial (in)completeness in abstract interpretation: limiting the imprecision in program analysis[END_REF]: they must be, at least, pre-ordered sets and be correlated by a monotone concretization function γ : A → C but not necessary forming a GC with an abstraction function α. Weakening the local forward-completeness property involves defining a pre-metric ⪯ C -compatible on the concrete domain (C, ⪯ C ): this can be achieved by either defining a pre-metric specifically tailored for (C, ⪯ C ) or, as showed in Section 4, by deriving a distance from another domain which may approximate the computation. The new notion of ε-partial forward-completeness is defined as follows.

Definition 11 (ε-Partial forward-completeness). Let us consider a premetric

⪯ C -compatible space (C, ⪯ C , δ C ) ∈ P re((C, ⪯ C )) and let f A : A → A be a sound approximation of f C : C → C. Given ε ∈ R ∞ ≥0
, we say that f A is an ε-partial forward-complete approximation of f C on input a ∈ A if and only if the following predicate holds:

δ C (f C (γ(a)), γ(f A (a))) ≤ ε ■
The value of the distance δ C between the result of the concrete operator f C (γ(a)) and the concretization of the abstract operator γ(f A (a))) can be interpreted as the measure of the approximation introduced by f A with respect to f C at input a. Therefore, this distance encodes a quantitative level of imprecision introduced by f A , more precisely, the imprecision that we want to measure according to how we have defined the pre-metric ⪯ C -compatible δ C . ). We want to analyze the partial forward-completeness of the Interproc5 [2] static analyzer when used to infer the numerical invariant of the while-loop of program P defined in Fig. 1 using the abstract domains A ∈ {Oct, Poly}. The imprecision generated by the abstract execution P A with respect to the concrete (collecting) execution P , is measured by using the following pre-metric ⊆-compatible on (℘(Z n ), ⊆):

%Vol(S 1 , S 2 ) def = (Vol(α Int n (S 2 )) -Vol(α Int n (S 1 ))) • 100 Vol(α Int n (S 1 ))
Intuitively, the value returned by %Vol(S 1 , S 2 ) is to be interpreted as the percentage of more volume that the abstraction (α Int n ) of S 2 into Int n has compared to the volume of the abstraction of S 1 into Int n , namely, Vol(α Int n (S 1 )) and Vol(α Int n (S 2 )) are the volumes of the two smallest hyperrectangles containing, respectively, S 1 and S 2 . Calculating the exact volume of hyperrectangles is generally much less computationally expensive than computing volumes of octagons and polyhedra, so this choice can be a good trade-off. In our case example, n = 2 since P has two variables so that Int 2 represents rectangles and Vol(α Int 2 (S)) is the area of the rectangle α Int 2 (S). Note that, since the concrete P and the two abstract executions P Poly , P Oct respect

P ⊆ γ ℘(Z 2 ) ( P Poly ) ⊆ γ ℘(Z 2 ) ( P Oct ) where γ ℘(Z 2 )
is the concretization of Oct and Poly into ℘(Z 2 ), then, thanks to axiom 2, we are sure that hold for program P . This means that %Vol estimates how more inaccurate is P Oct compared to P Poly , P Poly compared to P , and P Oct compared to P . Suppose our imprecision tolerance measured by %Vol is 20%. We want to verify when %Vol( P , γ ℘(Z 2 ) ( P A )) ≤ 20 holds, i.e., whether P Oct and P Poly are 20-partial forward-complete. By running Interproc using Oct and Poly6 we get the following inequalities representing the inferred while-loop invariants: P Oct = {x >= 0; -x + 10 >= 0; -x + y + 11 >= 0; x + y >= 0; y + 1 >= 0; -x -y + 17 >= 0; x -y >= 0; -y + 7 >= 0} P Poly = {-x -y + 10 >= 0; -x + 10 >= 0; y + 1 >= 0;

%Vol( P , γ ℘(Z 2 ) ( P Poly )) ≤ %Vol( P , γ ℘(Z 2 ) ( P Oct )) %Vol(γ ℘(Z 2 ) ( P Poly ), γ ℘(Z 2 ) ( P Oct )) ≤ %Vol( P , γ ℘(Z 2 ) ( P Oct ))
x -y >= 0; x + 6y >= 0} Fig. 3 and Fig. 4 depict, respectively, P Oct and P Poly . The pre-metric %Vol outputs:

%Vol(γ ℘(Z 2 ) ( P Poly ), γ ℘(Z 2 ) ( P Oct )) = 33.33 %Vol( P , γ ℘(Z 2 ) ( P Poly )) = 20 %Vol( P , γ ℘(Z 2 ) ( P Oct )) = 60
These numbers validate the better accuracy of P Poly compared to P Oct by providing us a quantitative estimation: the rectangle representing P Oct has 33.33% more volume than P Poly , the one representing P Poly has 20% more volume than the concrete execution P , while P Oct has 60% more volume than P . We can conclude that P Poly is 20-partial forward-complete whereas P Oct is not.

It is worth noting that, the same results can be drawn by defining a similar (computationally more efficient) pre-metric compatible with the Oct domain %Vol(o 1 , o 2 ) with o 1 , o 2 ∈ Oct which abstracts octagons into boxes, thus calculating for instance %Vol(α Oct ( P ), P Oct ) without passing through the concrete domain ℘(Z 2 ). ♦ When C and A enjoy a GC and a pre-metric ⪯ A -compatible is defined over the abstract elements of A, then we can weaken the notion of local backwardcompleteness to obtain the ε-partial backward-completeness property.

Definition 12 (ε-Partial backward-completeness). Let the concrete and abstract domains be correlated by a GC (C,

⪯ C ) ---→ ← --- α γ (A, ⪯ A ). Furthermore, as- sume (A, ⪯ A , δ A ) ∈ P re((A, ⪯ A )) and let f A : A → A be a sound approximation of f C : C → C. Given ε ∈ R ∞ ≥0
, we say that f A is an ε-partial backward-complete approximation of f C on input c ∈ C if and only if the following predicate holds:

δ A (α(f C (c)), f A (α(c))) ≤ ε ■
The ε-partial backward-completeness property of an abstract sound operator f A encodes a limited amount of imprecision measured by δ A , namely at maximum ε, between the abstraction of the concrete execution α(f C (c)) and the abstract execution f A (α(c)) over the concrete input c. Note the difference between the above definition and Definition 5 presented in [START_REF] Campion | Partial (in)completeness in abstract interpretation: limiting the imprecision in program analysis[END_REF]: here C and A are required to be at least pre-orders, and pre-metrics ⪯ A -compatible are employed as distance functions, instead of quasi-metrics A-compatible.

We conclude this section by showing some common characteristics between partial forward-and partial backward-completeness properties.

(i) f A ε-partial forward-complete at a ⇒ ∀ξ ≥ ε : f A ξ-partial forward- complete at a; (ii) f A ∞-partial forward-complete at a. ⊓ ⊔ Proposition 4. Let (C, ⪯ C ) ---→ ← --- α γ
(A, ⪯ A ) and (A, ⪯ A , δ A ) ∈ P re((A, ⪯ A )). The following hold for every c ∈ C:

(i) f A ε-partial backward-complete at c ⇒ ∀ξ ≥ ε : f A ξ-partial backward- complete at c; (ii) f A ∞-partial backward-complete at c. ⊓ ⊔
If f A is ε-partial forward-complete at a (resp. ε-partial backward-complete at c) then admitting a larger imprecision ξ according to δ C (resp. δ A ) results in the property of ξ-partial forward-completeness (resp. ξ-partial backwardcompleteness) which is always satisfied by f A . This implies that, if we define the class of all ε-partial forward-complete (sound) abstract operators with respect to f C and input a ∈ A, and the class of all ε-partial backward-complete (sound) abstract operators with respect to f C and input c ∈ C, namely

F ε f C ,a def = {f A | δ C (f C (γ(a)), γ(f A (a))) ≤ ε} B ε f C ,c def = {f A | δ A (α(f C (c)), f A (α(c))) ≤ ε}
then for all ξ ≥ ε:

F ε f C ,a ⊆ F ξ f C ,a and B ε f C ,c ⊆ B ξ f C ,c
. The second point of Proposition 3 and Proposition 4 simply states that any sound approximation f A of f C is partial forward/backward-complete when we admit an infinite level of imprecision.

Characterizing Local Forward/Backward-Completeness

In the original definition of partial (backward-)completeness given in [START_REF] Campion | Partial (in)completeness in abstract interpretation: limiting the imprecision in program analysis[END_REF] using quasi-metrics, asking for 0-partial (backward-)completeness at an input c ∈ C is equivalent to require local backward-completeness at c [START_REF] Campion | Partial (in)completeness in abstract interpretation: limiting the imprecision in program analysis[END_REF].

In our more relaxed framework where pre-metrics are involved and the identity of indiscernibles axiom is not satisfied, requiring 0-partial backward-completeness at c may not be the same as demanding local backward-completeness at c and, similarly, requiring 0-partial forward-completeness at input a ∈ A may not coincide with local forward-completeness at a. This is a consequence of the possible approximation introduced by the pre-metric when valuating the distance.

Example 10. Given (℘(Z 2 ), ⊆), consider the pre-metric ⊆-compatible %Vol defined in Example 9, and the two sets S 1 = {⟨0, 2⟩, ⟨3, 5⟩}, S 2 = {⟨0, 2⟩, ⟨1, 1⟩, ⟨3, 5⟩} such that S 1 ⊆ S 2 . The %Vol between S 1 and S 2 is %Vol(S 1 , S 2 ) = 0 even if S 1 ̸ = S 2 . This is because of the approximation made by %Vol which considers an approximated representation of S 1 and S 2 , namely, rectangles so that α Int 2 (S 1 ) = ⟨[0, 3], [1, 5]⟩ = α Int 2 (S 2 ). Therefore, if S 1 and S 2 are the results of, respectively, a concrete operator f ℘(Z 2 ) and and abstract operator f Int 2 , then f Int 2 is 0-partial forward-complete but not local forward-complete. ♦ However, it turns out that the 0-partial forward-completeness property coincides with the local forward-completeness property when the pre-metric ⪯ Ccompatible is strong.

Theorem 1. If δ C is strong then the following equivalence holds for all a ∈ A:

f A 0-partial forward-complete at a ⇔ f A locally forward-complete at a ⊓ ⊔ Example 11.
If we define the weighted path-length directly on (℘(Z), ⊆), namely, δ w ℘(Z) where w(S 1 , S 2 ) = 1 for all (S 1 , S 2 ) ∈ E ℘(Z) , then δ w ℘(Z) is strong. Consider the program Q defined in Fig. 2. We analyze the value of variable x at the end of the program having input the interval [START_REF] Campion | On the properties of partial completeness in abstract interpretation[END_REF][START_REF] Campion | On the properties of partial completeness in abstract interpretation[END_REF] using Interproc on the interval abstract domain Int with no widening at the first 10 loop iterations. The result of the analysis is γ( Q Int [START_REF] Campion | On the properties of partial completeness in abstract interpretation[END_REF][START_REF] Campion | On the properties of partial completeness in abstract interpretation[END_REF]) = {0} = Q γ( [START_REF] Campion | On the properties of partial completeness in abstract interpretation[END_REF][START_REF] Campion | On the properties of partial completeness in abstract interpretation[END_REF]), and the weighted path-length outputs

δ w ℘(Z) ( Q γ([10, 10
]), γ( Q Int [START_REF] Campion | On the properties of partial completeness in abstract interpretation[END_REF][START_REF] Campion | On the properties of partial completeness in abstract interpretation[END_REF])) = 0

i.e., Q Int is 0-partial forward-complete on input [START_REF] Campion | On the properties of partial completeness in abstract interpretation[END_REF][START_REF] Campion | On the properties of partial completeness in abstract interpretation[END_REF]

using δ w ℘(Z) . Since δ w ℘(Z)
is strong, then we are sure that Q γ([10, 10]) = γ( Q Int [START_REF] Campion | On the properties of partial completeness in abstract interpretation[END_REF][START_REF] Campion | On the properties of partial completeness in abstract interpretation[END_REF]), i.e., Q Int is locally forward-complete. ♦

A similar reasoning also applies to the 0-partial backward-completeness property when strong pre-metrics ⪯ A -compatible are employed.

Theorem 2. If δ A is strong then the following equivalence holds for all c ∈ C:

f A 0-partial backward-complete at c ⇔ f A locally backward-complete at c ⊓ ⊔
As a final observation, in cases where the concrete and abstract domains enjoy a GI through an abstraction function α : C → A and A is equipped with a strong pre-metric ⪯ A -compatible δ A , we can characterize the local backwardcompleteness property over exactly representable elements of C as an instance of the 0-partial forward-completeness property by exploiting the induced pre-metric ↽ δ C from the abstract pre-metric ⪯ A -compatible space. Int is a strong pre-metric ⪯ Int -compatible. We get the following equalities:

Theorem 3. Let (C, ⪯ C ) ---→ -→ ← ---- α γ (A, ⪯ A ), (A, ⪯ A , δ A ) ∈ P re((A, ⪯ A )) and (C, ⪯ C , ↽ δ C ) ∈ P re((C, ⪯ C )). If δ A is
↽ δ ℘(Z) ( Q γ([10, 10]), γ( Q Int [10, 10])) = δ w Int (α( Q γ([10, 10])), Q Int [10, 10]) = 0 namely, Q Int is 0-partial forward-complete on input [10, 10] using ↽ δ ℘(Z) . Since δ w Int is strong, this implies that α( Q γ([10, 10])) = Q Int [10, 10], i.e., Q Int is locally backward-complete at {10}. ♦ 7

Related Work

Forward and backward completeness are well known notions in abstract interpretation, especially in static program analysis for verifying safety program properties [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF][START_REF] Giacobazzi | Making abstract interpretations complete[END_REF][START_REF] Giacobazzi | Analyzing program analyses[END_REF]. The first attempt to weaken the notion of backward-completeness in abstract interpretation has been defined in [START_REF] Bruni | A logic for locally complete abstract interpretations[END_REF]. Here the authors introduced the notion of local completeness which corresponds to our definition of local backward-completeness (Definition 3). Partial completeness has been recently introduced as a further weakening of the local completeness property by admitting a limited amount of imprecision measured by a quasi-metric compatible with the underlying abstract domain [START_REF] Campion | Partial (in)completeness in abstract interpretation: limiting the imprecision in program analysis[END_REF][START_REF] Campion | On the properties of partial completeness in abstract interpretation[END_REF].

Besides the partial completeness property, the problem of measuring the imprecision of abstract interpretations is not new. Sotin [START_REF] Sotin | Quantifying the precision of numerical abstract domains[END_REF] defines a metric to quantify the result of numerical invariants by calculating the size of the concretization into R n . This metric can be considered as an instance of pre-metric ⊆-compatible, thus it can be used as distance function for formalizing the partial forward/backward-completeness property of interest.

Crazzolara [START_REF] Crazzolara | Quasi-metric spaces as domains for abstract interpretation[END_REF] proposes to substitute partial-orders with quasi-metrics, i.e., the concrete and abstract partially-ordered set turn into quasi-metric spaces. Our approach, instead, preserves the standard abstract interpretation framework and considers the distances as external tools for measuring the incompleteness of abstract operators. A similar idea is proposed by Di Pierro and Wiklicky [START_REF] Pierro | Measuring the precision of abstract interpretations[END_REF] where partially-ordered domains are replaced by vector spaces lifting abstract interpretation to a probabilistic version where it is possible to apply some wellknown distances in linear spaces.

Logozzo et al. [START_REF] Logozzo | Towards a quantitative estimation of abstract interpretations[END_REF] adapt the notion of pseudo-metric to be compatible with partially-ordered sets in order to measure the distance between two elements. Their definition of pseudo-metric requires the weak triangle inequality axiom and symmetry, while our definition of pre-metric relaxes those axioms. Moreover, axiom 2 may not be satisfied by pseudo-metrics, therefore their distances may not fit well in our framework.

Casso et al. [START_REF] Casso | Computing abstract distances in logic programs[END_REF] proposes a list of observations about distance functions when used to measure distances between elements of abstract domains in the context of logic programming. They show that it is possible to induce other distances from one domain to another through the concretization and abstraction functions in a similar way we did in Section 4. However, their notion of distance requires more compatibility with the underlying lattice than our approach as they focus on abstract domains commonly used for analyzing logic programs. For instance, they assume abstract domains to be complete lattices related by a GI with the concrete domains, they require another type of triangle inequality called diamond inequality, and consider distances between comparable elements only. As our notion of pre-metric is weaker than what they require for distances, our framework can be easily instantiated with their distances.

Conclusion

We weakened both the local backward-completeness, in presence of a GC, and the local forward-completeness properties in case only a concretization function is available (e.g., the case of convex polyhedra or the domain of formal languages [START_REF] Campion | Abstract interpretation of indexed grammars[END_REF]) in order to allow a limited amount of imprecision. This imprecision is measured according to a distance function formalized as a pre-metric compatible with the underlying pre-order relation. The definition of pre-metrics is general enough to be instantiated by distance functions having different "levels of view". For instance, a distance may be precise enough to satisfies the identity of indiscernibles axiom on the concrete domain, so that it can be used to reason on the local forward-completeness. Different levels of approximation can be obtain by inducing pre-metrics from one domain to another by the use of the concretization or the abstraction maps. Our framework could assist program analysis designers in controlling the propagation of incompleteness, e.g., by choosing the preferred pre-metric according to the imprecision they want to measure and at which level of details, and then by using it for checking how an invariant generated by the analysis grows with respect to the concrete execution or another comparable analysis. This checking process could also be combined with other repairing techniques that aim to enrich the expressiveness of abstract domains [START_REF] Giacobazzi | Making abstract interpretations complete[END_REF][START_REF] Bruni | Abstract interpretation repair[END_REF].

Similarly to the other completeness properties [START_REF] Giacobazzi | Analyzing program analyses[END_REF][START_REF] Bruni | Abstract extensionality: on the properties of incomplete abstract interpretations[END_REF][START_REF] Campion | Partial (in)completeness in abstract interpretation: limiting the imprecision in program analysis[END_REF][START_REF] Campion | On the properties of partial completeness in abstract interpretation[END_REF] both partial forward and backward-completeness properties are undecidable. As a future work we plan to extend the proof system proposed in [START_REF] Campion | Partial (in)completeness in abstract interpretation: limiting the imprecision in program analysis[END_REF] in order to be able to overestimate, according to δ D , a bound of incompleteness (either forward or backward) generated by the abstract interpreter without actually executing the program. This, in fact, can be considered as another abstract interpretation analyzing the abstract interpreter [START_REF] Cousot | A²i: Abstract² interpretation[END_REF].

Understanding the propagation of incompleteness through pre-metrics is closely linked to code obfuscation [START_REF] Collberg | Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection[END_REF], which finds application in software protection [START_REF] Giacobazzi | Hiding information in completeness holes: New perspectives in code obfuscation and watermarking[END_REF][START_REF] Giacobazzi | Making abstract interpretation incomplete: Modeling the potency of obfuscation[END_REF][START_REF] Giacobazzi | Maximal incompleteness as obfuscation potency[END_REF] and malware analysis [START_REF] Moser | Limits of static analysis for malware detection[END_REF][START_REF] You | Malware obfuscation techniques: A brief survey[END_REF][START_REF] Dalla Preda | Unveiling metamorphism by abstract interpretation of code properties[END_REF][START_REF] Campion | Learning metamorphic malware signatures from samples[END_REF]. Being able to quantify the amount of incompleteness induced in the abstract interpretation by a codeobfuscating program transformation could enable us to measure the potency of these transformations. This remains one of the primary open challenges in software protection [START_REF] Sutter | Software protection decision support and evaluation methodologies (dagstuhl seminar 19331)[END_REF][START_REF] Ceccato | Understanding the behaviour of hackers while performing attack tasks in a professional setting and in a public challenge[END_REF][START_REF] Collberg | Toward digital asset protection[END_REF].

Definition 8 (

 8 Strong pre-metric ⪯ D -compatible). Consider the pre-ordered space (D, ⪯ D , δ D ). The pre-metric ⪯ D -compatible δ D is said to be strong if and only if the following implication holds for every x, y ∈ D: x ⪯ D y ⇒ (δ D (x, y) = 0 ⇒ x = y) ■ For instance, the ordering-distance δ ⪯ D D of Example 2, the weighted path-length δ w Int defined on intervals in Example 6, δ Vol Poly of Example 4 with Vol calculating the exact volume, and the counting measure-distance on integer sets δ µ c ℘(Z) , are strong. Conversely, the zero-distance δ 0 D of Examples 1, the volume-distance δ Vol

Example 9 (

 9 Fig. 1: The Program P

Fig. 3 :Fig. 4 :

 34 Fig. 3: Invariant generated by P Oct

Proposition 3 .

 3 Let (C, ⪯ C , δ C ) ∈ P re((C, ⪯ C )) and f A : A → A be a correct approximation of f C : C → C. The following hold for every a ∈ A:

Example 12 .

 12 strong then the following equivalence holds for every a ∈ A: f A 0-partial forward-complete at a ⇔ f A locally backward-complete at γ(a) ⊓ ⊔ Consider again Example 11 analyzing program Q defined in Fig. 2. Let us use this time the weighted path-length δ w Int on intervals for reasoning on the partial backward-completeness at input γ([10, 10]) = {10} of variable x at the end of program Q. Recall that δ w

The term "forward-completeness" was introduced in[START_REF] Giacobazzi | Incompleteness, counterexamples, and refinements in abstract model-checking[END_REF] in order to distinguish it from the well known backward-completeness property requiring an abstraction function.

 2 In the standard abstract interpretation framework[START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF][START_REF] Cousot | Systematic design of program analysis frameworks[END_REF] dealing with GCs, the backward-completeness property is simply called completeness or exactness.

This is not a standard term in the literature: sometimes it is used to refer to other generalizations of metrics such as pseudosemi-metrics[START_REF] Buldygin | Metric characterization of random variables and random processes[END_REF] or pseudo-metrics[START_REF] Helemskii | Lectures and Exercises on Functional Analysis[END_REF]; it sometimes appears as pra-metric[START_REF] Arkhangel'skii | General topology I: basic concepts and constructions dimension theory[END_REF]. This definition is taken from Wikipedia [1].

We assume the following results when the ∞ symbol is involved:Av(k -∞) = Av(∞ -k) = ∞ with k ∈ R, while ∞ -∞ = 0.

Interproc is freely available at http://pop-art.inrialpes.fr/interproc/ interprocweb.cgi

For the convex polyhedra analysis, we activated the option of 2 descending steps.

Acknowledgements We wish to thank the anonymous reviewers of SAS 2023 for their detailed comments. This work has been partially supported by the grant PRIN2017 (code: 201784YSZ5) "AnalysiS of PRogram Analyses (ASPRA)".


Saber Sabri's Mamluk

Cairo

Appropriating Orientalism ?

As far as can be actually documented, Mamluk revivals in modern Cairene architecture can be traced back to Pascal Coste's (17891879) designs for the Citadel mosque (1823). Its aesthetics may appear awkward to the contemporary eye ; yet, the project was anchored on direct and indepth knowledge of Mamluk architecture. Since his arrival in Egypt in 1817, the French architect had spent considerable time surveying in detail major monuments in Cairo, accumulating hundreds of sketches and drawings, now kept in his archive in Marseilles 1 . His proposal was at one point abandoned a structure recalling Istanbul models was built instead but the story exemplifies a typical attitude that was to be followed by many European professionals in Egypt throughout the 19 th century, and beyond.

Documenting local architecture, and reusing its devices and patterns (eventually integrating authentic fragments as well), became central to the process of designing new structures meant to fit the Egyptian context [START_REF] Crinson | La tradition revisitée: réflexions sur un thème récurrent de la production architecturale européenne en Egypte[END_REF] .

Mamlukinspired compositions were not to be restricted to religious or public buildings; they were experienced in domestic and palatial architecture as well. Striking examples of suburban houses in the Mamluk style (or "Arab style" as it was termed at the time), along with orientalizing interior designs for the ruling family, can be found in the work of another French architect, Ambroise Baudry (1838 1906) 3 . Established in Cairo from 1871 to 1886 and an early collector of Islamic art, Baudry belonged to the group of connoisseurs that actively campaigned in the late 1870s for the conservation of Cairo architectural heritage, and furthermore, for an expert control over restoration works [START_REF] Volait | Amateurs français et dynamique patrimoniale : aux origines du Comité de conservation des monuments de l'art arabe[END_REF] . A Comité de conservation des monuments de l'art arabe was eventually formed in 1881; its impressive contribution to the changing face of "mediaeval" Cairo in the subsequent decades is getting increasing attention from scholars [START_REF] Sanders | Preservation and restoration : the methods of Max Herz Pasha, Chief architect of the Comité de conservation des monuments de l'art arabe, 1890-1914[END_REF] .

Nor were neoMamluk elaborations an exclusivity of Western architects [START_REF]An early interesting case is the proposal for the new al-Rifa'î mosque by Husayn Fahmî in 1868 ; on this figure and the fate of his project, see Mercedes Volait, Architectes et architectures de l'Egypte moderne (1830-1950), Genèse et essor d'une expertise locale, Paris: Karthala, forthcoming ; see also Nasser Rabbat[END_REF] . Although only some 19 th century local designs in the Mamluk style have been identified so far, the architecture produced by the Waqfs' Administration during the first years of 'Abbâs Hilmî's rule (18921914) offers an opportunity to discuss some specific expressions of it and to question their possible significance.

Waqf architecture in late 19 th century Cairo

An administrative body formed in 1835 to control the management of religious foundations, the Awqâf had been reorganised in 1851 as a Dîwân with authority over endowments with no living beneficiary or intendant, later becoming a Ministry (1879) ; more importantly, it had gained, or rather recovered, significant autonomy when transformed into an "Administration" on 23 January 1884, on the ground that waqfs had to be administrated along the prescriptions of the Shari'a and therefore required a separate agency under direct tutelage of the khedive [START_REF]Rapport administratif pour l'année 1910 présenté à son Altesse le khédive par le directeur général des Waqfs[END_REF] . The independence of this new Administration was to be shortlived, since it was reverted to a ministry on 20 November 1913 when the British decided to regain control over revenues that were mainly used, in their views, to strengthen what they called "national agitation" in the country [START_REF] Younan | The development of the ministerial system in Egypt : 1878 -1923[END_REF] . Yet, the interlude proved to be a period of remarkable building activity, especially after 'Abbâs Hilmî's accession to the throne in 1892. Among the new officials appointed at highranking positions in the Awqâf was Saber Sabri (c. 18451915), as

Chief Engineer (Bachmuhandis alAwqâf). He remained in charge until 1906.

If we are to believe a report submitted by Sabri on the eve of his retirement, the Awqâf had been responsible, since 1892, for the building or renewal of about a hundred mosques and shrines, while over two hundred residential and commercial buildings had been remodelled (the figures do not include repairs, that would amount to thousands of cases according to the data provided) [START_REF] Dîwân | Sura al-muzakirra allati rufû'at li-al-janâb al-'ali al-khidiwi 'an al-masâgid wa al-mahalât allatî gadidiha dîwân 'umûm al-awqâf fî 'ahd ta'ssîssihu lighayit 1323 H[END_REF] . These are rather impressive numbers when compared to Awqâf activity under the previous reigns. During the rule of 'Abbâs' father, khedive Tawfîq (r. 1879 to 1892), 20 places of worship were built or restored and 30 civil buildings were renewed by the Administration; for Ismâ'îl's times (18631879), the figures respectively dropped to merely 10 religious buildings and 21 civil ones.

Most of the buildings listed in the report for the years 18921906 belong to what has come to be termed "Mamluk revivals", and moreover to a rather rigorist form of such historicism [START_REF]For stimulating analysis of 19th c. eclecticisms and historicisms[END_REF] . Needless to say, these modern interpretations of the Mamluk repertoire can hardly be confused with their historical models, but they reveal a fairly good acquaintance with Mamluk monuments and a honest mastering of the classical vocabulary -at least, when compared to previous attempts in the "Arab style". Islamic art specialists may view the issue with other eyes; indeed it must be stated upfront that the comments proposed are embedded in another point view, that of the architectural history of modern Egypt, from the mid19 th century onwards.

Anyhow, Sabri's hypothesised historicism brings in turn the question of its meaning, of the significance of such stylistic option. Three possible interpretations, all speculative, are offered here, depending on how the buildings are looked at. Accordingly, Sabri's designs will be discussed first in the light of his formation and professional career, second within their patronage and political context at large, and finally through the prism of the architectural production of their days.

Three historicist designs

Among the multiple works supervised by Sabri in his capacity of Bachmuhandis alAwqâf from 1892 to 1906, the Awlâd 'Inân mosque, the Sayyida Nafîssa mosque and the premises of the Waqfs Administration itself, will be considered here. Apart from what can be inferred from diverse historical sources, and from the observation of the buildings themselves, the material available fortunately includes initial drawings, that were reproduced in a photographic album assembled in 1899 [START_REF]Souvenir inauguration du nouveau local des Wakfs[END_REF] .

"Archeological historicism" : the Awlâd Inân mosque

The Awlâd 'Inân mosque represented an early project of Saber Sabri at the Awqâf ; it was to be built at Bâb alHadîd, opposite to the Cairo Railway station, where the alFath mosque (c. 1983) stands now. (Interestingly enough, Awlâd 'Inân survived this successive new construction : in 1979, it was dismantled and relocated on the large maydân below the Citadel, and renamed as Sayyida 'Aycha mosque). The new Awlâd 'Inân was meant to replace an ancient shrine, rebuilt in the late 14 th century, and that had been demolished during the French occupation (17981801) [START_REF] Mubârak | [END_REF] . The foundation and its endowments had been transferred to the Waqfs' Administration in 1893, upon the death of its last nazîr, Muhammad 'Abd alWâhid alHarîrî 13 ; on the following year, the affluent vicepresident of the Legislative Council (a consultative assembly created by Ismâ'îl to associate the rural notability to the khedivial regime), one Hasan Pasha Hilmî, had bestowed about 4000 E.P. on the Waqfs Administration for the erasing of the old structure and its replacement by a new mosque and a maktâb (elementary school). The construction was started in October 1894 ; after the patron's death a few months later, it was continued by khedivial order at the expenses of the Awqâf. The mosque was inaugurated at the end of 1896 with a final cost of 7000 E.P., almost the double than what had been initially forecast. According to a description of the project in a French architectural magazine, its "interior decoration was extremely rich" indeed [START_REF]Mosquée Oulad Enane[END_REF] . Both this article and the surviving reproduction of the designs tend to attest Sabri's authorship of the work. The former clearly states that the mosque is "l'oeuvre de Saber bey Sabri, l'éminent architecte en chef des Waqfs"; the latter, dated 29 October 1894, bear the signatures of Saber Sabri and of an assistant, Iskandâr 'Azîz [START_REF]Iskandâr 'Azîz was an engineer already working in the Awqâf in 1891[END_REF] , preceded by the formula frequently found on 19 t h c. designs and that reads "'Amal wa naql hazihi alrasm bima'rifitnâ…".

The mosque was built in stone, with the usual alternating layers of red and white stone from the Muqattam quarries (Plate 1). The plan featured a covered prayer hall, lightened by a central lantern (as was the case in many Mamluk madrasas) ; it included a kuttâb at the first floor. Revenues for the maintenance of the building were to be produced by the rent of an attached flat and store. These were located in the triangular zones produced by the classical distortion resulting from the adjustment to the Mecca orientation and to the street alignment (Plate 2). Literal quotations from existing monuments are evident in the ornamentation of the minaret, which combines the shaft and lower part of the Qayt bay minaret at alAzhar (1494), with the top of another Qayt bay's minaret, the one attached to his mausoleum in the southern cemetery (1472) [START_REF] Doris Behrens-Abouseif | The Minarets of Cairo[END_REF] . A detailed analysis of the architectonic decoration of the façade would probably show similar arrangements. The carved dome of the mosque, as visible at its current location by the Citadel, also evokes Qayt bay's buildings. A late Mamluk distinctive architecture formed thus the essential source of inspiration of Awlâd 'Inân, in conformity with the requirements of an "archeological historicism" [START_REF] Loyer | [END_REF] .

Subverting historicism : the Sayyida Nafîssa mosque

A subsequent project of the Awqâf was the rebuilding of the Sayyida Nafîssa mosque. The initial structure had been greatly damaged by a fire in 1892 and required a large reconstruction [START_REF]The Mosques of Egypt from 21 H[END_REF] . The surviving drawings are dated September 1895, and bear again the signatures of 'Iskandâr 'Azîz, this time as ra'is qalm altasmîmât (chief of the architectural drawings department) and of Saber Sabri.

The rather complicated plan of the mosque may be due to the fact that it integrates parts of the burnt structure. The reconstructed building displays several components that evoke again a strict historicist vein.

The minaret is a case in point, at least the original one as documented in period pictures. It was far from resembling its current shape. The latter, characterised by a central shaft with ceramic decoration (Plate 3), is probably related to the extant renewal of the building undertaken in 1972, when a new prayer hall was added 19 . This methodological point is of importance ; it gives the opportunity to stress that original designs can not be discussed on the sole basis of what can be observed today on the ground, even for quite recent structures. In any case, what could be eventually deduced from the use of Iznik tiles (basically a feature alien to the Mamluk period, adopted from Ottoman architecture) in a supposedly neoMamluk mosque does not apply to the building designed by Saber Sabri. The eclectic touch here is the result of a much later intervention.

As in the case of the Awlâd 'Inân mosque, the Sayyida Nafîssa minaret is clearly a replica of existing models. It reproduces the two main storeys of the Qayt bay mausoleum minaret, topped with the usual finial. Still, the historicism of the building is a mixed one, since the dome at least the present one (Plate 4) is closer to that of Barqûq mausoleum (1399) in the northern cemetery, rather than to any Qayt bay dome. Another example of how the classical repertoire is played with is illustrated by the subverted use of the blazons on the external walls (Plate 5): rather than giving the name and titles of the patron of the mosque, the pseudo ranks bear here Coranic epigraphy (laallah illa Allah wa Muhamad rassul illah). Yet, whether these are a later addition or date from the construction of the mosque, remains an open question.

Inventing tradition: the Awqâf premises

The third example considered is the premises of the Waqfs administration itself. The building still stands (with substantial additions in 1911 and 1929 by successive chief engineers of the Awqâf 20 ) in downtown Cairo (Plates 6 and 7). The plan conforms the administrative function of the building, and is organised around an inner courtyard. The drawings bear this time the name of an unknown European architect : one "F. Ségèz or Légèz, architecte" who states that he drafted and copied the drawings in June 1896 (« 'Amal wa naql hazihi alrasm bima'rifatnâ 20 juin 1896 »). Saber

Sabri signed the project on the following day. According to inscriptions on the façade, the building was completed in 1898. The photographic album, where it is recorded, dates from the following year.

The building is an eclectic collage of features borrowed from diverse Mamluk monuments :

recessed panels crowned by stalactites, ablaq and stucco decoration, Qalawun set of windows, trefoil crenelations…. The eclecticism is emphasized in this case by the fact that no historical example could be resorted to for the design of such type of building. It implied necessarily heavy inventions.

A man of classical formation and multiple commitments

One possible interpretation of the more or less marked historicism of these buildings could be grounded on Sabri's biography. His life and career are still quite obscure, but recent light has been shed on the man [START_REF]Valuable information on Sabri's career, including an obituary, is provided by Pascal Crozet[END_REF] . What can be reconstructed from miscellaneous and fragmentary sources is that Saber Sabri was trained as an engineer around 18661870, which means that he was probably born established that the classical methods of land surveying used in Egypt by the specialized guild of the misahiyyin could produce errors of about 15%. Consequently, he embarked on listing the necessary corrections [START_REF] Sabri | Les défauts du système d'arpentage à la kassaba et les corrections à y faire[END_REF] . Yet, his skills in mathematics can easily relate him to a classical muhandis [START_REF] Behrens-Abouseif | Muhandis, Shâd, Mu'allim -Note on the building craft in the Mamluk Period[END_REF] .

When appointed Chief engineer of the Awqâf in 1892, Sabri also became, in this official capacity, a member of the Comité de conservation des monuments de l'art arabe. He continued to participate in its activities well after his retirement, in fact until his death in 1915 -he was on this occasion celebrated by fellow members as an "erudite professional and a hard worker" [START_REF]Comité de conservation des monuments de l'Art arabe[END_REF] . The few interventions of Sabri documented in the minutes of the Comité's meetings depict a man with doctrines regarding restoration that evoke the ViolletleDuc's approach. In 1897, for instance, he opposed the choices made by Max Herz, the then chief architect of the Comité, concerning an interior frieze of the mosque of Barqûq (at Nahassin), because he considered the colours chosen to repaint the wood as being too pale, while Herz' concern was to get the old paint reproduced as faithfully as possible to its current condition [START_REF] Idem | The preservation of Egyptian cultural heritage through Egyptian eyes : the case of the Comité de conservation des monuments de l'art arabe[END_REF] . However and interestingly enough, Sabri also added on that occasion that the (limited) available resources might be best used by being invested on conservation issues (consolidating additional monuments, for example) rather than on showy restorations -a quite balanced view on the matter, considering the debate that was by then opposing the antirestoration posture defended by Ruskin and its followers to the learned "restorations" advocated by ViolletleDuc.

There is no evidence that Sabri's revivalism should be understood primarily as the product both of a muhandis' classical education in mathematics (which could have facilitated achieving the revival of historical models of architecture, concerning i.e. the execution of stalactites) and of a committed concern for the conservation and restoration of Cairo historical monuments (that would have reinforced an interest in reviving such heritage). The hypothesis is tempting if one admits that individual agency is worth considering in historical interpretation, following the microstoria approach to historiography [START_REF] Levi | On microhistory[END_REF] . One is led in turn to wonder whether such revivalisms should be considered as late resurgences of, or eventual continuities with, customary practices, or should rather be analyzed as expressions of a local domestication of Western Orientalism, one filtered through a partly traditional background. Lack of evidence advocates to be cautious in the respect, but it does suggest to consider the eventual existence of an indigenous "Orientalism" in late 19 th c. Cairo [START_REF]For a general discussion of a related idea in the Ottoman context, see Ussama Makdisi, "Ottoman Orientalism[END_REF] .

Patronage and politics of Mamluk Revivalism :

Another speculative reading of Sabri's architectural achievements is connected to politics. It has been argued that, under 'Abbâs Hilmî, "architecture returned to Mamluk style in order to show independence of Egypt from Ottoman control" 29 . However, the khedive's turn towards Egyptian nationalism is known to have taken place at a later stage : around 1895, when the Waqf administration started developing Mamluk revivalism, the young ruler was on the contrary attempting to mobilize Ottoman support to assert his positions over the British High Commissioner 30 . Hilmî's memoirs, though conveying in fact the image of a man more concerned in the early years of his rule by independence from the British rather than from the Porte, are of little help in this respect. They do mention in passing his building activity, but only as patron of blocks of flats in Cairo's Tawfîqiyya quarter [START_REF] Hilmi | Mémoires d'un souverain, présentées par Amira Sonbol[END_REF] .

Should we thus understand the Mamluk style as evidence of the khedivial family's social and cultural commitment to the country, as a form of localism ? [START_REF] Rabbat | The formation…[END_REF] The earliest Mamlukstyle building commissioned by 'Abbâs Hilmî suggests another possible reading of the use of the style. It concerns the mausoleum erected in memoir of his father Tawfîq (Plate 8), in the Eastern cemetery in Cairo. The building was inaugurated on 15 January 1894 and was designed by Dimitri Fabricius Bey (1848 1907), the chief architect of khedivial buildings 33 . In this case, the Mamluk style was explicitly used to give the mausoleum an "imposing character", because it was perceived as representing the "best epoch of Arab architecture" [START_REF] Mausolée D'afifi | érigé à la mémoire de feu Son Altesse le Khedive Tewfiq[END_REF] .

In the case of another Mamluk revival project designed and executed by Saber Sabri, the new Riwâq al'Abbâssî (18941898) attached to the mosque of alAzhar, the "Arab style" was imposed by the Comité de conservation des monuments de l'art arabe because of the function and location of the building. Commissioned by the khedive, the Riwâq was built in order to "enhance the religious character of the mosque by giving it a larger façade". The Comité asked furthermore that its design be prepared following the façade of an old house that was to be demolished in order to enlarge the street bordering the new building and alAzhar gate [START_REF]Comité de conservation des monuments de l'art arabe[END_REF] .

Finally, the specific history of the Awlâd 'Inân mosque as a sufi shrine 36 may corroborate the diversity of situations in which the Mamluk style could be used then, and the range of meanings. The old Awlâd 'Inân mosque, as rebuilt in the late 14 th century, included the tomb of a saint, Muhamad Ibn 'Inâni (d. 920 H.), associated with women (and still venerated as such in the 1960s 37 ) ; in addition, it was home of al'Inâniyya, at the time a dissident sufi order, in conflict with the central authority on mystic groups, but that had obtained in 1886 the protection of khedive Tawfîq and the recognition of a special status, due to the fact that the order possessed an authentic chain going back to 'Umar Ibn al Khattâb (586644) ; al'Inâniyya was indeed known as one of the older tariqas in Egypt [START_REF] Jong | Turuq and Turuq-linked institutions in 19th. c. Egypt[END_REF] . The decision that placed in 1893 the foundation under the authority of the Awqâf, despite the existence of descendants of the venerated saint and of the family in charge of the shrine, both reclaiming rights on it [START_REF]Letter from al-'Inânî brothers to the khedivial cabinet[END_REF] , could well indicate the determination of the new ruler to regain control on al'Inâniyya and its properties. In this perspective, the Mamluk style may have had a complete different connotation, either as a recognition of the long history of the al'Inâniyya or as a mark of its new suzerainty to the khedive, or furthermore as a combination of both. that he had turned to, when he considered developing pottery manufacturing in Egypt [START_REF] De | Report on the feasibility of a manufacture of glazed pottery in Egypt[END_REF] .

The Mamluk style in architectural perspective

Ultimately, it must be added that the shift to "archeological historicism", expressed by most of Mamluk revivals of the 1890s and 1900s in Egypt, in contrast with preceding examples of "Moorish"

or "Arabesque" architecture and design, was been experienced simultaneously in France. By 1887, prior advocates of the most extravagant eclecticisms (as mixes of a large range of historical references coupled with modern devices and patterns) were now defending a dedicated mimicry of historical styles : "whatever the style referred to, the quotation was becoming literal", as observable on most Belle Epoque landmarks in Paris 45 . Appreciations of literality in citation will, in turn, vary in time along the evolving agenda of taste : for a critic writing in 1915, the Awlâd 'Inân mosque drew without doubt on an ancient model, but the building was now perceived as showing a disproportionate minaret and "corrupted" historical references [START_REF] Bay | L'art ancien et l'art moderne du Caire[END_REF] what was at stake now was a modernity with no link with the past.

As a whole, Mamluk revival in Cairo at the end of the 19 th c. emerges as a somewhat complex phenomenon, with varied possible meanings and readings, beyond the political symbolism commonly attached to the style. More documentary evidence is needed to better apprehend an architectural practice that was both deeply rooted in its local context (moreover, there had been Mamluk archaisms already during Ottoman times [START_REF]After the Ottoman conquest, many Mamluk-style elements continued to be incorporated into the buildings, whether secular or religious, see Doris Behrens-Abouseif, Islamic Architecture in Cairo[END_REF] ) and yet in perfect syntony with contemporary developments in Europe. It is telling, in this perspective, that Sabri's designs for the Awlâd 'Inân mosque found their way to a French architectural magazine : this was an exceptional situation for a Middle Eastern architect at the time.

However, besides a need for primary sources, what may be equally necessary is to question the discursive categories in common use when analysing the material culture under scrutiny here, starting with some basic interrogations. Is Islamic architecture, the adequate and performing classification to analyze all, or some, or none of the works mentioned above ? Does orientalism solely apply to European attitudes and artistic expressions ? If not, does it make sense to differentiate between European and indigenous orientalism ? And so on… Adopting essentializing and globalizing notions, or simplifying dichotomies, based on allegedly clear cultural distinctions, may be a preliminary step to gain familiarity with artistic productions alien to one's culture -it has been argued in fact that "essentialism is a fundamental constraint of crosscultural cognizance" [START_REF] Salvatore | Beyond Orientalism ?[END_REF] . When studying buildings that are caught into multiple influences and varied processes of hybridization, as is the case with 19 th century architecture in Egypt, it is all the more essential to proceed further on and to search for new ways and words that can allow to fully grasp complex architectural formalisations.

Illustrations :

around 18451850 .

 18451850 Contrary to many of his colleagues who were sent abroad to acquire modern knowledge and skills, his was a pure local training, achieved at the Muhandiskhanâ (Cairo's Polytechnical school), possibly under the supervision of Ibrahim Adhâm (1785 c. 1870), a Turkish engineer who is believed himself to have received his technical education both from the military school in Istanbul, and then from studying in England. In 1881, Saber Sabri is recorded as a teacher in mathematics at the Muhandiskhanâ and is known to have translated two manuals, one on analytical geometry with special focus on the curves, and another on descriptive geometry. Five years later, he had the chair of mathematics at the Muhandiskhanâ 22 ; he acted as its deputydirector in the following years. His interest and knowledge in mathematics was to be a lasting one : as an active member during 23 years of the Gama'iyya alKhayriyya alIslamiyya (The Islamic Benevolent Society), an Islamic charity that helped founding many elementary schools, he worked to encourage the teaching of mathematics to young Egyptians. In 1909 and 1910, he was still lecturing in mathematics at the newly born Egyptian University created 2 years before. His understanding of the discipline does not appear to have been particularly imprisoned into traditional knowledge : in an article published in 1891, he

Situating

  Sabri's designs within the architectural production of his days brings about further facets of Mamluk revivalism. At the time, the style was actually gaining popularity in Egypt. It was adopted in a variety of circumstances with, presumably, an even larger range of significance. The Cairo Railway Station was, for example, completely rebuilt between 1891 and 1893 in the same style (Plate 9) following a destruction by fire in 1882[START_REF] Al-Rahman Zakî | Mawsû' madîna al-Qâhira fî alf 'âmm[END_REF] . A political connotation, in the sense of nationalist symbolism, seems unlikely in the circumstance ; the European taste for exoticism, or a loose association with travel and tourism, would be better candidates to explain the stylistic choice. Other contemporary Mamluk revivals include examples as varied as the grand hall at the famous old Shepheard's Hotel, a design attributed to the Furino brothers (an Italian firm specialized in what had come to be called the "Arabesque style", especially fashionable for furniture[START_REF]Twentieth Century Impressions of Egypt[END_REF] ) (Plate 10) or the neo Classical palace that was "islamicized" in 1891 when turned into a Tobacco factory by the Greek merchant Nestor Gianaclis now in the main campus of the American University in Cairo, with an entrance door reproducing the portal of the takiyya alDin alBistami (1443), that was being restored at the same period[START_REF] Volait | La tradition revisitée…[END_REF] . The association of Mamluk revival with tobacco directly echoes earlier European uses of the Moorish style, from the "fumoir mauresque" (Moorish smoking room), fashionable since the 1830s in French mansions, to imposing cigarette factories in Germany 43 . Exoticism and European representations of Oriental leisure were powerful drives for the popularisation of the Mamluk style. As already mentioned, it was also closely associated with Islamic art collecting in the 1870s, and was to remain related to it in the following decades, as the houses, pavilions or rooms built for the collections of Count Zughayb in 1898, of 'Umar Sultân in 1907 or of prince Yusuf Kâmal in 1920 suggest -Islamic art collectors in Cairo were not only Europeans. For those amateurs, the Mamluk style was a matter of aesthetics. It may have been the case as well with khedive 'Abbâs. Significantly, it was to a ceramic artist and tile designer known for his orientalizing designs, William de Morgan (18391917),

Plate 1 :Plate 2 :Plate 4 :Plate 5 :Plate 6 :Plate 7 :Plate 8 :Plate 9 :

 12456789 Awlâd 'Inân mosque upon completion (Dîwân 'umûm alawqâf, Sura almuzakira…, Cairo, Rare books and special collections, American University in Cairo) Elevations and plan of the Awlâd 'Inân mosque (from La construction moderne, vol. XIII, 1897/98, pl. 92, Paris, Ecole Nationale Supérieure des BeauxArts) Plate 3 : Detail of the minaret of Sayyida Nafîssa mosque, 2003 (Photo : M. Volait) The dome of Sayyida Nafîssa mosque, 2003 (Photo : M. Volait) Detail of a rank at the Sayyida Nafîssa mosque, 2003 (Photo : M. Volait) The main entrance of the Awqâf premises, c. 1940 (Cairo, Lehnert and Landrock collection) The rear façade of the Awqâf premises, 2003 (Photo : M. Volait) Tawfîq mausoleum upon completion, 1894 (Cairo, Rare books and special collections, American University in Cairo) The Cairo Railway Station, c. 1915 (Cairo, Lehnert and Landrock collection) Plate 10 : The grand hall at the old Shepheard's Hotel, c. 1915 (Cairo, Lehnert and Landrock collection)