Frédéric Besson
email: frederic.besson@inria.fr

CPA beats oo-CFA

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

INTRODUCTION

Context-sensitive points-to analysis is a scalable technology for constructing precise control-flow graphs of objectoriented programs. It allows for aggressive inter-procedural optimisations and improves the precision of client analyses [START_REF] Grove | A framework for call graph construction algorithms[END_REF][START_REF] Milanova | Parameterized object sensitivity for points-to analysis for Java[END_REF][START_REF] Lhoták | Evaluating the benefits of context-sensitive points-to analysis using a bdd-based implementation[END_REF]. The output of the analysis is a control-flow graph and a points-to graph abstracting the memory heap. For the baseline (context-insensitive) analysis, nodes in the control-flow graph are method names and nodes in the pointsto graph are class names. For object-oriented programs such context insensitive graphs are far too imprecise. To improve the accuracy context-sensitive analyses account for the fact that the same method can be run in different call-contexts and that the same class can be instantiated in different allocation-contexts. For context-sensitive analyses, a node in the control-flow graph is a method name tagged by a callcontext and a node in the points-to graph is a class name tagged with an allocation-context.

As early as 1991, Palsberg and Schwartzbach [START_REF] Palsberg | Object-oriented type inference[END_REF][START_REF] Palsberg | Object-Oriented Type Systems[END_REF] propose a theoretical parametric framework for typing objectoriented programs. In their setting, context-sensitivity is obtained by explicit code duplication and typing amounts to analysing the expanded code in a context-insensitive manner. The framework accommodates for both call-contexts and allocation-contexts. In particular, it accommodates for the well-known k-CFA hierarchy abstracting the call-context by a call-string made of the last k invocation sites. For Self, a language with multiple dispatch, Agesen [START_REF] Agesen | The Cartesian Product Algorithm: Simple and Precise Type Inference Of Parametric Polymorphism[END_REF] proposes the Cartesian Product Algorithm (CPA) which abstracts the call-context by the cartesian product of the abstract objects argument of the call.

To assess the respective merits of different instantiations, scalable implementations are needed. For Cecil and Java programs, Grove et al., [START_REF] Grove | Call graph construction in object-oriented languages[END_REF][START_REF] Grove | A framework for call graph construction algorithms[END_REF] have explored the algorithmic design space of contexts for benchmarks of significant size. Latter on, Milanova et. al., [START_REF] Milanova | Parameterized object sensitivity for points-to analysis for Java[END_REF] have evaluated, for Java programs, a notion of context called object-sensitivity which abstracts the call-context by the abstraction of the this pointer1 . More recently, Lhotak and Hendren [START_REF] Lhoták | Evaluating the benefits of context-sensitive points-to analysis using a bdd-based implementation[END_REF] have extended the empiric evaluation of object-sensitivity using a BDD implementation allowing to cope with benchmarks otherwise out-of-scope. The findings of the more recent empiric studies are consistent and conclude that object-sensitivity performs better than call-string sensitivity -for the Java benchmarks considered.

Hind [START_REF] Hind | Pointer Analysis: Haven't We Solved This Problem Yet[END_REF] discusses the difficulty of assessing the merits of a pointer analysis: it depends on various factors including the language, benchmarks and client analyses. Yet, from a theoretical standpoint, there are known facts about the respective precision of context-sensitive points-to analyses. Grove and Chambers [2, Figure 19] picture a comprehensive map of context-sensitive analyses ordered by precision of the computed graph. In this map there are analyses for which the relative precision is only conjectured. In particular, CPA is conjectured to be (strictly) more precise than ∞-CFA.

The main contribution of this paper is a formal proof that CPA is strictly more precise than ∞-CFA. Other contributions include the definition of a minimal object-oriented calculus modeling standard dispatch mechanisms in a uniform manner; and a generic soundness proof of context-sensitive points-to analyses. Moreover, the formal development is mechanised inside the Coq proof assistant 2The rest of the paper is organised as follows. Notations are gathered in Section 2. In Section 3, we introduce the syntax and semantics of our core object-oriented language. In Section 4, we present the specification and generic soundness proof of context-sensitive analyses. In Section 5, we formally show how to relate different analyses and prove that CPA is strictly more precise than ∞-CFA. Section 6 concludes.

NOTATIONS

Given sets A and B, we write Ae for the set A ∪ {e} such that e / ∈ A and A → B ⊥ for the set of partial functions from A to B. Let f : A → B, f [x → v] is the function identical to f everywhere except for x for which it returns v. For a function f : A → B ⊥ , when we write f (x) = y, y is (implicitly) an element of B i.e, y = ⊥. Tuples with k elements are written e1, . . . e k . When it is clear from the context, brackets are dropped. We write A * for the sets of lists with elements in A. The empty list is written ǫ and e::l is the list whose head is e and tail is l. The null pointer, written 0, is always distinct from any other addresses Addr. Therefore, we shall write Addr0 for the set of addresses extended with the null pointer. We write α for an arbitrary address distinct from 0.

A CORE O-O LANGUAGE

In this section we define a minimal core language for reasoning about the inter-procedural control-flow of imperative object-oriented languages. Unlike e.g., Featherweight Java [START_REF] Igarashi | Featherweight Java: a minimal core calculus for Java and GJ[END_REF], our language is not about high-level object-oriented concepts such as classes and inheritance. Even methods are absent and a program is simply given by a list of statements and a dynamic method lookup function.

Syntax and semantics

We consider (finite) sets of class names Class, method names Meth, field names Field and variables names Var ({v0, v1} ⊆ Var ). A program p ∈ Prog is a list of statements together with a lookup function.

S △ = copy(v, v ′ ) | new(c) | read(f ) | write(f ) | call(m) | ret Lkup △ = (Var → Class) → Meth → N Prog △ = S * × Lkup where v, v ′ ∈ Var , c ∈ Class, f ∈ F ield, m ∈ Meth.
Our statements are a restricted form of 3 address code. To give them an intuitive meaning, the syntactic translation between these formats is given below.

copy(v, v ′ ) v := v ′ new(c) v0 := new(c) read(f ) v0 := v0.f write(f ) v0.f := v1
Because the lookup function has type (Var → Class) → Meth → N, it models uniformly different kinds of dispatch.

In general, we get multiple-dispatch for which the target of the call depends on all of the arguments of the caller. Single dispatch is obtained if only the receiver, say v0, selects the target of the call. Function pointers are degenerated cases of single dispatch for which Class = N and Meth = {•}. A static method call is a further specialisation for which only the method name m is used to resolve the call. The language is equipped with a standard small-steps operational semantics. A program state is a pair h, pc, e ::f ∈ Heap × F rame + where 1) pc ∈ N is the current program counter i.e., the index in the program of the instruction to be executed next; 2) e ∈ Env is a local environment mapping variables to addresses; 3) h ∈ Heap maps allocated addresses to objects; 4) f ∈ F rame * is a stack of frames recording caller contexts. Formal definitions of the semantics domains are given below:

Env △ = Var → Addr0 Frame △ = N × Env Object △ = Class × (F ield → Addr0) Heap △ = Addr → Object ⊥ State △ = Heap × F rame +
We consider an uninterpreted infinite set of addresses Addr. An object is a pair c, o ∈ Object where c is a class name and o is a mapping from fields to addresses. The heap is a partial mapping from addresses to objects.

The definition of the transition relation ⊆ State×State is in Figure 1. The function nth : N → S ⊥ is such that nth(pc) is either the pc th statement of the program or ⊥ if the index is out-of-bounds. Therefore, the execution blocks when the program counter pc is indexing a non-existent statement. The statements copy, new, read and write are intra-procedural and do not modify the stack of frames. After executing an intra-procedural statement, execution continues in sequence from the next instruction. The new(c) statement picks in the heap an unallocated address α and allocates at that address an object of class c whose fields are all null. The statements read and write require addresses to be non-null. In our model, the de-reference of null pointers is thus blocking. To resolve a method call call(m), the dispatch dp first computes a (finite) function mapping variables to the class name of the object they point to -the null pointer being mapped to the undefined class udf . Then, the lookup function is called with as argument theses classes and the method name m. It returns the index of the first statement of the callee.

The semantics starts from an undefined heap h0 = λα.⊥ and an environment mapping all variables to 0 (e0 = λv.0). The set of reachable states Acc is the set of states accessible from the initial state s0 = (h0, 0, e0 ::ǫ) by the reflexive transitive closure of the relation .

Acc = {s | s0 * s}

POINTS-TO ANALYSIS

An instance of a context-sensitive analysis is obtained by defining a domain CC of call-contexts, a domain AC of allocation contexts -or abstract addresses -an initial call context • : CC and two functions alloc modeling abstract object creation and push abstracting the push operation on frames at the level of call contexts.

alloc : CC × N × Class × (Var → AC0) → AC push : CC × N × Meth × (Var → AC0) → CC
It is worth noticing that the soundness of the analysis does not depend on the actual definitions of alloc and push. For CPA and ∞-CFA objects are abstracted by their creation site. CPA and ∞-CFA differ in their abstraction of the call context. For CPA, the call-context is either the initial call-context • or a pair made-of the current method being executed and its abstract arguments. For infinite CFA, the

nth(pc) = copy(v, v ′ ) e ′ = e[v → e(v ′ )] h, pc, e ::f h, pc+1, e ′ ::f nth(pc) = new(c) e ′ = e[v0 → α] h(α) = ⊥ h ′ = h[α → c, λf.0 ] h, pc, e ::f h ′ , pc+1, e ′ ::f nth(pc) = read(f ) e(v0) = α h(α) = c, o e ′ = e[v0 → o(f )]
h, pc, e ::f h, pc+1, e ′ ::f

nth(pc) = write(f ) e(v0) = α h(α) = c, o h ′ = h[α → c, o[f → e(v1)] ] h,

Context-sensitive instrumentation

In order to state and prove correct context-sensitive analyses, the standard approach consists in instrumenting the semantics with an address cache [START_REF] Nielson | Infinitary control flow analysis: a collecting semantics for closure analysis[END_REF][START_REF] Nielson | Principles of Program Analysis[END_REF]. The address cache is used to dynamically map addresses to their allocation context.

Acache △ = Addr → AC0
We also carry along the computation the current abstract call-context. The instrumentation is not intrusive and neither enable new semantic transitions nor disable existing ones. The instrumented semantic relation is defined over an extended state

IFrame △ = F rame × CC IState △ = Heap × IFrame + × Acache
At the intra-procedural level, all statements except object allocation keep the instrumentation unchanged. The new(c) statement maps the newly allocated address to its allocation context computed by the alloc function. At the interprocedural level, the address cache is threaded along the execution while call contexts follow the stack discipline. The modified transitions are given in Figure 2. For an address cache ac : Addr → AC0, we write ac0 : Addr0 → AC0 an extended address cache mapping null to null and e ac = λv.ac0(e(v)) the abstraction of the environment with respect to the address cache. IAcc is the set of instrumented reachable states from is0 = λα.⊥, 0, λv.0, • ::ǫ by the reflexive transitive closure of the instrumented semantics relation.

Context-sensitive points-to analysis

The principle of a context-sensitive points-to analysis is to abstract addresses by their allocation context and the stack of frame by a call-context. Moreover, environments are abstracted in a set-based manner by a mapping from variables

nth(pc) = new(c) e ′ = e[v0 → α] h(α) = ⊥ h ′ = h[α → c, λf.0 ]
ac ′ = ac[α → alloc(cc, pc, c, e ac )] h, pc, e, cc ::f, ac h ′ , pc+1, e ′ , cc ::f, ac ′ nth(pc) = call(m) cc ′ = push(cc, pc, m, e ac ) pc ′ = lk(dp(h, e), m) h, pc, e, cc ::f, ac h, pc ′ , e, cc ′ :: pc, e, cc ::f, ac nth(pc) = ret er = e ′ [v0 → e(v0)] h, pc, e, cc :: pc ′ , e ′ , cc ′ ::f ), ac h, pc ′ +1, er, cc ′ ::f, ac

IState ♯ △ = HClass × HObject × CCEnv
The result of the analysis is a triple (hc ♯ , ho ♯ , e ♯ ) ∈ IState ♯ defined as the least solution to the constraints defined in Figure 3. The analysis is demand-driven and only propagates information about reachable code. For this purpose, we use a predicate isdef to ensure that an abstract environment pe ∈ Env ♯ binds all the variables to at least one abstract value. For e ∈ (Var → AC0) and pe ∈ Env ♯ , we write e ∈ pe if ∀v, e(v) ∈ pe(v) and define isdef (pe) by ∃e, e ∈ pe. To resolve virtual calls in the abstract, we define the abstract dispatch relation.

dp ♯ ⊆ (Var → AC0) × (Var → Class) (e, d) ∈ dp ♯ iff ∀v, e(v) = 0 ⇒ d(v) = udf e(v) = α ♯ ⇒ (α ♯ , d(v)) ∈ hc ♯
We write ⊑ the point-wise ordering i.e., e1 ⊑ e2 if and only if ∀v, e1(v) ⊆ e2(v). As a result, a constraint of the form e[vi → s] ⊑ e ′ denotes a set of subset constraints of the form e(v0) ⊆ e ′ (v0), . . . , e(vi-1) ⊆ e ′ (vi-1), s ⊆ e ′ (vi), e(vi+1) ⊆ e ′ (vi+1) . . . e(vn) ⊆ e ′ (vn).

For intra-procedural statements, constraints have the form f ♯ (e ♯ (cc, pc)) ⊑ e ♯ (cc, pc+1) where f ♯ denotes the abstract semantics of the statement. If before statement copy(v, v ′ ) v ′ is referencing α then v is referencing α after the statement. The abstraction of the other variables is unchanged. If before statement read(f ), v0 is referencing α and if there is an edge (α, f, β) in the points-to graph, then after read(f ), v0 is referencing β. After new(c), the abstraction of v0 is a singleton α computed by the alloc function with respect to the current context cc, program counter pc and class c. The write(f ) rule does not modify abstract environments but updates the points-to graph with new edges. As this is a weak update, edges are never removed.

Inter-procedural rules are dealing with call-contexts. The rule call(m) is splitting the current environment with respect to the dispatch function and the abstract push function. The target of the call identified by a call-context cc ′ and a computed program counter lk(d, m) collects (pointwise) the environments resolved there. The rule modelling a return is the one departing the most from the concrete semantics. Its role is to match a call and a return by making sure that the call-context of the callee cc is obtained by a push from the call-context of the caller cc ′ . The return i.e., variable v0 is then copied from callee to caller.

Correctness theorem

The correctness theorem states that the result of a contextsensitive points-to analysis i.e., the triple (hc ♯ , ho ♯ , e ♯ ) overapproximates the reachable states IAcc of the concrete (instrumented) semantics. To formalise the over-approximation, we define a concretisation function γ : IState ♯ → P(IState).

A key component of the concretisation is the address cache ac which establishes the correspondence between concrete addresses and allocation contexts. Concretisations of environments γP , heaps γH and stack of frames γF are therefore indexed by an address cache ac. Figure 4 summarises the formal definition of all those concretisation functions.

Theorem 1. Let hc ♯ , ho ♯ , e ♯ be a solution to the constraints, we have IAcc ⊆ γ(hc ♯ , ho ♯ , e ♯ ).

The correctness proof relies on key invariants of the instrumented semantics.

• Absence of dangling pointers. All the addresses in the stack frame are bound in the heap and all the fields of the objects in the heap refer themselves to addresses allocated in the heap (or possibly the null pointer).

• Monotonic and faithful address cache. In the address cache, allocated addresses are mapped to their allocation context. Hence, the address cache is only growing and allocation contexts of allocated addresses are invariant.

• Instrumented stack discipline. When a return point is reached with state h, pc, e, cc :: pc ′ , e ′ , cc ′ ::f, ac then there exists a state h ′ , pc ′ , e ′ , cc ′ ::f, ac ′ such that nth(pc ′ ) = call(m) and push(cc ′ , pc ′ , m, e ′ac = cc and if ac ′ (α) = α ♯ then ac(α) = α ♯ .

Given these invariants, the proof is by induction over the length of the derivation.

CPA BEATS OO-CFA

In this section, we shall prove that CPA is more precise than ∞-CFA. In the sequel, CPA is identified by a subscript and ∞-CFA by a ∞ subscript. In particular, we write A = hc , ho , e for the result of CPA and A∞ = hc∞, ho∞, e∞ for the result of ∞-CFA. CPA is more precise than ∞-CFA if it captures less concrete states. As the soundness of our points-to analyses is stated over instrumented states, to compare their relative precision, we introduce an erasure function E : P(IState) → P(State) which given a set of instrumented states removes their instrumentation i.e., address caches and call-contexts of the stack of frames. Hence, proving that CPA is more precise than ∞-CFA amounts to proving the following theorem.

Theorem 2. E • γ (A ) ⊆ E • γ∞(A∞)
To structure the proof we introduce another points-to analysis Ω-CFA that keeps more context information than both ∞-CFA and CPA. As far as allocation context is concerned, Ω-CFA is like CPA and ∞-CFA and abstracts addresses by their allocation site (alloc(cc, pc, c, e) = pc). However, it keeps more information about call-contexts than CPA and ∞-CFA: pushΩ(cc, pc, m, e) = m, e, pc ::cc. Hence, by construction, Ω-CFA is more precise than ∞-CFA and CPA. Therefore, to prove our theorem, it remains to prove that CPA is also at least as precise as Ω-CFA. To do so, we exhibit a precise translation function T : IState ♯ Ω → IState ♯ mapping the result of Ω-CPA to the result of CPA such that:

P 1 : A ⊑ T (AΩ) P 2 : E • γ • T (AΩ) ⊆ E • γΩ(AΩ)
Property P 1 means that the result of AΩ can be plunged (by applying T ) into the CPA domain in such a way that A is more precise. There are many imprecise T functions with this property. Property P 2 ensures the precision of the translation by requiring that T is compatible with the concretisations γ and γΩ.

Lemma 1. Given P 1 and P 2, we have

E • γ (A ) ⊆ E • γ∞(A∞)
Proof. By applying the monotony of E and γ over P 1, we get E • γ (A ) ⊆ E • γ • T (AΩ). By P 2 and transitivity of ⊆ we get E • γ (A ) ⊆ E • γΩ(AΩ). Because AΩ is more precise than A∞, this concludes the proof.

The formal definition of T is given below: Because the two analyses are sharing the same heap abstraction, no translation occurs for hc ♯ and ho ♯ . For the environments, the function TE merges all the abstract environments for which the top-element of the call-context stack matches the context of CPA. Lemma 2 states that the merging of Ω-contexts is benign and does not introduce spurious environments.

nth(pc) = ret isdef (e ♯ (cc, pc)) nth(pc ′ ) = call(m) e ′ ∈ e ♯ (cc ′ , pc ′ ) cc = push(cc ′ , pc ′ , m, e ′ ) r = e ♯ (cc, pc)(v0) e ♯ (cc ′ , pc ′ )[v0 → r] ⊑ e ♯ (cc ′ , pc ′ +1)
γ ac H (hc ♯ , ho ♯ ) =    h h(α) = ⊥ ⇒ ac(α) = ⊥ h(α) = c, o ⇒ ∃α ♯ .ac(α) = α ♯ , (α ♯ , c) ∈ hc ∧∀f, α ♯ , f, ac0(o(f )) ∈ ho    γF : Acache → CCEnv → P(IFrame + )
γ ac F (e ♯ ) = pcn, en, ccn :: . . . :: pc0, e0, • ::ǫ nth(pci) = mi ei ∈ γ ac P (e ♯ )(cci, pci) cci+1 = push(cci, pci, mi, e ac i )

γ : IState ♯ → P(IState) γ(hc ♯ , ho ♯ , e ♯ ) = h, f, ac h ∈ γ ac H (hc ♯ , ho ♯ ) ∧ f ∈ γ ac F (e ♯ )
Figure 4: Concretisation functions

TE : CCEnv Ω → CCEnv TE(e ♯ )(• , pc) = e ♯ (•Ω, pc) TE(e ♯ )((m, o), pc) = e ♯ ((m, o, pco)::l, pc) l ∈ CC Ω nth(pco) = call(m) T : IState ♯ Ω → IState ♯ T (hc ♯ , ho ♯ , e ♯ ) = (hc ♯ , ho ♯ , TE(e ♯ ))
where S = λv. {e(v) | e ∈ S}. We prove that it is possible to swap quantifiers and exhibit a single stack l and pco such that nth(pco) = call(m) ∧ e ∈ e ♯ ((m, o, pco)::l, pc). The intuition is that the prefix stack l has no impact on abstract environments in the scope of the callees of m -much as in the concrete semantics. For instance, if pc is the target of the call to m, the abstract environment is o and is thus independent from l. By induction over the depth of subsequent calls, we can conclude that all prefix stacks are equivalent and cannot be distinguished. As a result, we can pick any stack l and pco such that for some v, nth(pco) = call(m) ∧ e(v) ∈ e ♯ Ω ((m, o, pco) :: l, pc)(v). For any other variable v ′ , we will also have e(v ′ ) ∈ e ♯ Ω ((m, o, pco) :: l, pc)(v ′ ). Lemma 3 states that for a given abstract heap, CPA is more precise than Ω-CFA Lemma 3. Given an abstract heap (hc ♯ , ho ♯ ), we have e ♯ ⊑ T (e ♯ Ω ). Proof. The proof is by induction over the definition of e ♯ . Suppose that e ∈ e ♯ ((m, o), pc), by induction hypothesis we have that e ∈ TE(e ♯ )((m, o), pc). By Lemma 2 we can exhibit a stack l and pco such that nth(pco) = call(m) ∧ e(v) ∈ e ♯ Ω ((m, o, pco) :: l, pc)(v). The proof follows by case analysis over the rules defining e ♯ and e ♯ Ω .

Lemma 4. A ⊑ T (AΩ)

Proof. The proof is straightforward because we already proved that e ♯ ⊑ T (e ♯ Ω ) and because both analyses are using the same alloc function.

It remains to prove that E • γ • T (AΩ) ⊆ E • γΩ(AΩ). As AΩ and A are using the same heap abstraction, they compute the same address cache. Once again, the key argument is Lemma 2 allowing to show that T (AΩ) retains enough information to rebuild the call-stack of AΩ.

The origin of oo-CFA imprecision

An interesting point not elucidated by the proof is the reason why CPA is strictly more precise than ∞-CFA. A reason already discussed in [START_REF] Grove | A framework for call graph construction algorithms[END_REF] is that the abstraction of environments is set-based thus responsible for a loss of precision. This precision loss is not specific to ∞-CFA but shared by all context-sensitive points-to analyses. Yet, an effect of CPA context-sensitivity is that environments often map variables to singletons (a property identified by Agesen [START_REF] Agesen | The Cartesian Product Algorithm: Simple and Precise Type Inference Of Parametric Polymorphism[END_REF]) thus minimising the effect of the non-relational abstraction of environments. CPA obtains a precise result concluding that f1 is called in context (A, A) or (B, B). ∞-CFA incurs a loss pf precision because it considers a single context per call. It thus concludes that f1 is called with arguments (A, A) ⊔ (B, B) = ({A, B}, {A, B}) and thus looses precision.

CONCLUSION

A few years back, Grove and Chambers [START_REF] Grove | A framework for call graph construction algorithms[END_REF] conjectured that CPA was more precise than ∞-CFA. To our knowledge, our proof is the first to firmly establish this result. As CPA is a form of object-sensitivity and ∞-CFA is the ultimate call-string sensitivity, this theoretical result backs up recent empirical studies [START_REF] Milanova | Parameterized object sensitivity for points-to analysis for Java[END_REF][START_REF] Lhoták | Evaluating the benefits of context-sensitive points-to analysis using a bdd-based implementation[END_REF] concluding than objectsensitivity performs better than call-string sensitivity.

Compared to the object-oriented community, researchers in the functional community are better equipped to carryout formal proofs: various flavors of the lambda-calculus, many alternative semantics and a variety of abstract machines. For our formalisation, we introduce a core objectoriented language well-suited for reasoning about controlflow analyses. The language is minimal allowing, with little overhead, a mechanised reasoning into a proof-assistant.

As further work we shall investigate how to effectively compute context-sensitive analyses with an infinite number of contexts. At the top of the list is ∞-CFA but other instances such as infinite object-sensitivity of allocation contexts are of interest.

Figure 1 :

 1 Figure 1: Semantics

Figure 2 :△=

 2 Figure 2: Instrumented semantics

Lemma 2 .

 2 If e ∈ TE(e ♯ )((m, o), pc) then there exists l and pco such that nth(pco) = call(m) ∧ e ∈ e ♯ ((m, o, pco)::l, pc).Proof. If e ∈ TE(e ♯ )((m, o), pc) then by definition of TE, we have that forall v, there exists l and pco such thatnth(pco) = call(m), e(v) ∈ e ♯ Ω ((m, o, pco) :: l, pc)(v) nth(pc) = copy(v, v ′ ) isdef (e ♯ (cc, pc)) e ♯ (cc, pc)[v → e ♯ (cc, pc)(v ′ )] ⊑ e ♯ (cc, pc+1) nth(pc) = new(c) e ∈ e ♯ (cc, pc) α = alloc(cc, pc, c, e) e ♯ (cc, pc)[v0 → {α}] ⊑ e ♯ (cc, pc+1) nth(pc) = read(f ) isdef (e ♯ (cc, pc)) s = {β | α ∈ e ♯ (cc, pc)(v0), (α, f, β) ∈ ho ♯ } e ♯ (cc, pc)[v0 → s] ⊑ e ♯ (cc, pc+1) nthp(pc) = write(f ) isdef (e ♯ (cc, pc)) e ♯ (cc, pc) ⊑ e ♯ (cc, pc+1) nth(pc) = new(c) e ∈ e ♯ (cc, pc) α = alloc(cc, pc, c, e) α, c ∈ hc ♯ α, f, 0 ∈ ho ♯ nthp(pc) = write(f ) isdef (e ♯ (cc, pc)) α ∈ e ♯ (cc, pc)(v0) β ∈ e ♯ (cc, pc)(v1) α, f, β ∈ ho ♯ λv.{0} ⊑ e ♯ (•, 0) nth(pc) = call(m)e ∈ e ♯ (cc, pc) (e, d) ∈ dp ♯ cc ′ = push(cc, pc, m, e) λv.{e(v)} ⊑ e ♯ (cc ′ , lk(d, m))

Figure 3 :

 3 Figure 3: Points-to analysis

Figure 5 :

 5 Figure 5: Translation function

Example 1 .

 1 Suppose a function f(x,y) dispatched as follows: (A, A) → f1; (B, B) → f1; (A, B) → f2; (B, A) → f2.After running the following pseudo-code,x : = ( ? : new A ( ) ; new B ( ) ) ; y : = ( ? : new A ( ) ; new B ( ) ) ; f ( x , y )f1 is called with arguments {(A, A), (B, B)}.

At level 1, object-sensitivity is a trimmed down version of the CPA.

The commented Coq source code can be browsed at http://www.irisa.fr/celtique/fbesson/CPABeatsCFA

* This work was partly funded by the IST-FET programme of the European Commission, under the IST-2005-015905 MOBIUS project.


Fabien Despinoy
email: despinoy@lirmm.fr

Alonso Sánchez
email: sanchezsec@lirmm.fr

Nabil Zemiti
email: zemiti@lirmm.fr

Pierre Jannin
email: pierre.jannin@univ-rennes1.fr

Philippe Poignet
email: poignet@lirmm.fr

Comparative assessment of a novel optical human-machine interface for laparoscopic telesurgery

Keywords: Infrared stereoscopic camera, human-machine interface, teleoperation, laparoscopic surgery, hand tracking

This paper introduces a novel type of human-machine interface for laparoscopic telesurgery that employs an optical sensor. A Raven-II laparascopic robot (Applied Dexterity Inc) was teleoperated using two different human-machine interfaces, namely the Sigma 7 electromechanical device (Force Dimension Sarl) and the Leap Motion (Leap Motion Inc) infrared stereoscopic camera. Based on this hardware platform, a comparative study of both systems was performed through objective and subjective metrics, which were obtained from a population of 10 subjects. The participants were asked to perform a peg transferring task and to answer a questionnaire. Obtained results allow to confirm that fine tracking of the hand could be performed with the Leap Motion sensor. Such tracking comprises accurate finger motion acquisition to control the robot's laparoscopic instrument jaws. Furthermore, the observed performance of the optical interface proved to be comparable to that of traditional electro-mechanical devices, such as the Sigma 7, during adequate execution of highly-dexterous laparascopic gestures.

Introduction

During the last three decades, the field of laparoscopic surgery was constantly subject to technological advances looking to offer better healthcare in terms of safety, patient outcome, medical staff coordination and comfort [START_REF] Sanchez | A Design Framework for Surgical Robots: Example of the Araknes Robot Controller[END_REF]. Among these advances, the appearance of telesurgical systems represents a major breakthrough. Teleoperated systems enabled surgeons to interact with a distant environment, while providing them with a sense of immersion within the remote environment. To that end, high-resolution endoscopic cameras and intuitive humanmachine interfaces (HMIs) for controlling the robotized laparoscopic tools have been developed. Moreover, it is well-known that telesurgical systems allow further performance improvements for surgeons by scaling down the hand motions (i.e. to perform more accurate gestures), filtering involuntary hand tremor and offering, in some cases, force-feedback information [START_REF] Rosen | Force Controlled and Teleoperated Endoscopic Grasper for Minimally Invasive Surgery-Experimental Performance Evaluation[END_REF]. However, the lack of costeffective, sterilizable, precise and repeatable force sensing solutions represents an open issue, which is clearly reflected in currently available commercial robotic systems such as the Da Vinci R surgical system (Intuitive Surgical Inc) or the Raven-II platform [START_REF] Lum | The raven: Design and Validation of a Telesurgery System[END_REF] [START_REF] Hannaford | Raven-II: An Open Platform for Surgical Robotics Research[END_REF].

The majority of master-slave systems used in telesurgery exchange kinematic information of the operator's hands (e.g. through the system's position and/or velocity channels) in order to define the control reference of the robotic endeffectors [START_REF] Lawrence | Stability and Transparency in Bilateral Teleoperation[END_REF]. Hence, the HMIs that are used to recover kinematic information from the surgeon do have a direct impact on the overall robotic system performance. For that reason, some recent research focused on the development of novel HMIs to improve dexterity and ergonomy. In [START_REF] Santos-Carreras | Survey on Surgical Instrument Handle Design: Ergonomics and Acceptance[END_REF], for instance, the authors presented an analysis of an electro-mechanical HMI for minimally invasive surgery, which is based on ergonomic principles and on polls carried out within the surgical community. Their results suggested that surgeons' preferences are mainly driven by 2 factors: comfort and precision. Nevertheless, the proposed electro-mechanical HMI is unable of fully exploiting the capabilities of the surgeon's hands. For example, their workspace is limited in order to avoid collisions between the left and right hand devices, whereas a human operator is capable of highly-dexterous and accurate bi-manual surgical manipulations within the frontal region that is unexploited by conventional electro-mechanical HMIs (e.g. the Sigma 7 employed in this work, or the Omega 7 modified in [START_REF] Santos-Carreras | Survey on Surgical Instrument Handle Design: Ergonomics and Acceptance[END_REF]). Therefore, ergonomy and intuitiveness of today's HMIs might be further improved.

In this paper, we address the issue of validating the possibility of performing highly-dexterous and precise telesurgical tasks by means of an infrared stereoscopic camera, the Leap Motion. Furthermore, initial results on the novel possibilities that could be offered by such type of interfaces are also introduced through a comparative study with a high-performance commercial electromechanical HMI, the Sigma 7.

Previous works employing optical based sensors in the context of teleoperation can be found in the literature. In [START_REF] Dragan | Teleoperation with Intelligent and Customizable Interfaces[END_REF], the Kinect device (Microsoft Corp) was employed to track the user's upper limbs and to control two industrial robot arms to perform pick and place tasks. Thanks to the anthropomorphic configuration of the robot arms, the user can easily control their motion by using joint angle inputs without major kinematic issues. Similarly, [START_REF] Du | Markerless Kinect-Based Hand Tracking for Robot Teleoperation[END_REF] implemented tracking algorithms to segment and detect the hand's thumb and index fingers in order to control the robot end-effector. However, their algorithms were highly sensitive to optical occlusions, and also relied on the detection of the entire forearm. Finally, whether a surgical application is considered, these approaches would fail to accurately distinguish finger motions for fine control of the instrument tips. In consequence, it might be more suitable to state that [START_REF] Dragan | Teleoperation with Intelligent and Customizable Interfaces[END_REF] and [START_REF] Du | Markerless Kinect-Based Hand Tracking for Robot Teleoperation[END_REF] employed less accurate hand gesture recognition techniques (e.g. open hand and fist gestures) for control of the robotic end-effectors. Finally, in [START_REF] Oikonomidis | Tracking the Articulated Motion of Two Strongly Interacting Hands[END_REF] the authors performed simultaneous tracking of both hands and fingers in a robust manner, accounting for possible optical occlusions by estimating two 26 degrees of freedom (DoFs) hand models and performing optimization to find an unique fitted solution based on Kinect sensor measurements. Nevertheless, one major issue of their work regards its considerable computational complexity due to the solution of a high-order optimization problem using stochastic algorithms. Indeed, time delay and synchronization are two key factors which affect the performance of the entire teleoperation system. Therefore, a simplified and less computationally expensive solution using a 7 DoF hand model is introduced in this paper for tracking of the hand within the context of laparoscopic surgery.

The remaining sections are structured as follows. Section II introduces the teleoperation platform with the two different HMIs that were compared. Section III describes the methods employed for evaluating the performance of the system and the obtained results are also presented and analyzed. Lastly, in section IV concluding remarks and future works are discussed.

The teleoperation setup

In order to effectively compare the relative performance of both HMI technologies, the platform depicted in Figure 1 was employed. Such a scheme was proposed to isolate the influence of the HMIs by keeping constant the other hardware components (i.e master components and the slave robot system). For that reason, an unified HMI application programming interface (API), which allows quick exchange of the interfaces, was implemented by software wrapping of the corresponding device drivers. A footpedal was used in order to activate/deactivate teleoperation when required. In Figure 2, pictures of the actual slave side system components are provided, including the peg board used for laparoscopic task evaluation. The Raven-II robot comprises two robotic arms of 7 DoFs, in which the two distal DoFs are decoupled and allow independent movements of each grasping jaw. During the experiments with both HMIs, the same Cartesian position servoing software routines were employed at a control frequency of 1kHz. Regarding the Leap Motion HMI, visible in Figure 4(a), three infrared sensors coupled with an array of two cameras is used to create a depth map of the scene. The Leap Motion's Cartesian position measurement accuracy is about 0.01 mm, and the employed hand tracking refresh rates were ≈110 Hz. The API provided by the manufacturer allows tracking of hand palms and fingers, the latter being classified as pointy objects. Such device could also allow left and right hand workspaces overlapping without the associated risks of HMI collisions. Such possibility might be advantageous during some laparascopic tasks (e.g. intracorporeal knotting and peg or needle transfers from one hand to another), which could otherwise turn to be less comfortable and intuitive. Nonetheless, whether the hand workspaces intersect, particular care should be taken when optical hand occlusions arise. For that reason, a simple model consisting of three points (i.e. index finger, thumb finger and hand palm) was defined in order to allow robust model based tracking using a simple time-consistent Kalman filter. The model geometry is depicted in Figures 4(a Tremor filtering is applied in both HMIs through an autoregressive movingaverage (ARMA) low-pass filter, having an attenuation of ≈25 dB at 2 Hz [START_REF] Bo | Pathological Tremor and Voluntary Motion Modeling and Online Estimation for Active Compensation[END_REF]. Finally, whenever hand tracking is lost, special care was taken in order to stop teleoperation (i.e. overriding the footpedal), while avoiding bumps when the tracking is recovered.

3 Performance assessment of the HMIs

Methods

A population of ten researchers from the LIRMM Lab were enrolled in the comparative performance evaluation of the HMIs. A video was shown to each candidate in order to introduce the overall system functioning and the demanded peg transferring sequence. The latter sequence consisted in transferring some pegs directly from one pin to another, and takes into account guidelines provided by SAGES and FLS organizations [START_REF] Derossis | Development of a Model for Training and Evaluation of Laparoscopic Skills[END_REF]. The sequence is defined as follows:

1. Pick the first peg with the left tool and insert it in target 1 (leftmost pin of Fig. 2(b)) 2. Pick the second peg with the right tool and insert it in target 2 (rightmost pin) 3. Pick the latest peg with the left or right tool, then advance towards the center of the peg board to grab it with the other available tool in order to finally insert it in target 3 (uppermost pin)

Each subject began the protocol with a randomly selected HMI and was allowed to freely use the device during 5 minutes, allowing him/her to test-drive the teleoperated system, familiarize with movements and hand coordination. During this test-drive, the participant was taught how the system works, about its possibilities and limitations (i.e. avoiding prolonged-time occlusions when using the Leap Motion or engaging teleoperation at the workspace limits of the Sigma 7). Subsequently, the candidates were asked to repeat the presented peg transferring sequence five times with each device. The last three trials were used for the statistical analysis. Finally, the subjects were asked to grade each HMI through multiple measurements.

Results

Recorded data was analyzed using the JMP 11 software (SAS Institute Inc). A one-way analysis of variance (ANOVA) was carried out by defining the HMI device as a fixed factor and the duration as the response variable. ANOVA relies on the variance analysis from multiple samples to determine their affiliation and whether a difference between mean durations exists, and thus, to accept or discredit H 0 hypothesis, which means that each device allows to perform the same task with the same duration time. Before performing ANOVA calculation, we ensured that data respect a normality function for an homogeneous repartition (i.e. χ 2 normality test).

Figure 5(a) depicts the average value and standard deviation of the total task completion time for all subject trials with each device. It is observed that the candidates were able to execute the task 13% faster in the case of the Sigma 7 device. ANOVA computation results are summarized in Figure 5(b), which shows the mean difference of duration times for each device. With a p-value of 0.0172, this analysis highlights that a significant difference between both devices can be confirmed, so that they can constitute two distinct populations. Nevertheless, even though a difference is confirmed, there is only a small gap between both devices (i.e. 14 seconds for a task requiring ≈1 min 50 secs). higher success rate was observed in the case of the Leap Motion, signifying that, in spite of the slightly larger task completion times, the operators committed less mistakes with this device.

Similarly, the number of times the users had to clutch the teleoperation system through the footpedal was recorded (see "Clutching" column in Figure 6(b)). Subjects had to do this in order to reposition themselves for being able to carry on with the peg transferring task (e.g. hand tracking loss, reaching the workspace limits). It can be observed that better clutching results could be obtained with the Sigma 7 device, mainly due to the simple occlusions handling strategy that was implemented for the Leap Motion device. Consequently, operators were not able to properly detect the limit of the manipulation workspace, leading to a security lock and forced subjects to clutch in order to recover the hand tracking. Indeed, similar completion times, clutching and success rates can be obtained with both devices (see "Time", "Success" and "Clutching" columns in Figure 6(b)), whereas two additional metrics highlight a significant difference between the HMIs. On the one hand, the cost of each interface is taken into account (see "Cost" column in Figure 6(b)), in favor of the Leap Motion sensor. Even so, the high cost of the Sigma 7 interface is mainly explained by the force-feedback embedded technology which is not employed during the experimentations. Alternative positioning systems such as the MicroScribe R (Solution Technologies Inc) or the Phantom Omni R haptic device (Sensable, now part of Geomagic) can be taken on board for a more relevant comparison. Nevertheless, the Leap Motion device is still one of the cheaper interactive device present on the market. On the other hand, the sterilization capacity was compared (see "Sterilization" column in Figure 6(b)). This latter measurement refers to the possibility for the surgeon of preserving asepsis (i.e. hygiene without considering the certification requirements) during the whole duration of the procedure, so that he/she can directly operate in the patient, if required, without forced to change surgical gloves. An upper grade was attributed to the Leap Motion device, since infrared light can easily traverse a thin film of plastic to prevent it from contaminating the sterile environment. In the case of the Sigma 7, a lower grade was attributed to the device, since the presented system is not certified to meet such requirement. Figure 7 summarizes the results that were obtained after questioning each operator. It can be confirmed that the Sigma 7 device outperformed the Leap Motion in terms of perceived reactivity, precision, robustness and comfort. Nevertheless, in terms of intuitiveness, the operators were more satisfied with the contact-less optical device. It is also observed that important ameliorations in terms of robustness are imperative for future experimentations, including an accurate optical occlusion management.

Reac0vity"

Precision" Intui0veness" Robustness" Comfort"

Ra#ng&

Sigma" Leap"Mo0on" Fig. 7. Attributed grades, for each subjective factor, by all operators.

Considering the advantages and disadvantages of the Sigma 7 and the Leap Motion devices, together with their relative performance during the peg transferring task, our initial results suggest that infrared stereoscopic camera sensors have a promising potential for the development of cost-effective, sterilization compatible, more intuitive and accurate HMIs for laparoscopic telesurgery. Nonetheless, the obtained results also indicate that imperative development are required to improve the robustness of the hand tracking algorithms in the presence of optical occlusions.

Some design recommendations for next-generation HMIs could also be suggested from this first study. Report from experimentation highlights that the enlarged workspace and the freedom of bi-manual interactions between hands was appreciated by subjects. Furthermore, alternative solutions allowing forcereflecting teleoperation might be considered in the future, whether appropriate force sensing solutions for the medical field become available, through the development of wearable antagonistic tendon-like systems, exoskeletons, or through the application of model based electrical stimulation of the upper limbs.

Immediate future works mainly regard the development of a more robust model based hand tracking. Unfortunately, the API of the Leap Motion is closed by the device provider. Therefore, other specific sensors with open APIs, such as the Senz3D (Creative Labs Ltd, time-of-flight sensor), might be employed in the future. Additionally, a complementary study relying on trajectory analysis, from both master and slave sides, should be considered in order to enhance the interpretation of the results obtained during these experimentations.

Finally, other surgical tasks requiring higher accuracy, such as dissection of small targets, suturing and clip application should be studied, including expert and novice surgeon operators, in order to improve the statistical significance of our first results.

Fig. 1 .

 1 Fig. 1. Overall diagram of the teleoperation setup.

Fig. 2 .

 2 Fig. 2. Slave side hardware.

Figure 3

 3 Figure 3 depicts the main master side system components. Each of the Sigma devices has 7 active DoFs. A Cartesian position measurement accuracy of about 0.005 mm (including translation and grasping motions) is reported by the manufacturer. During tests, these devices were polled at a 1 kHz rate. Since the Sigma interfaces were disposed in order to avoid workspace overlapping of the left and right hands, no risk of collision between the HMIs exists.

Fig. 3 .Fig. 4 .

 34 Fig. 3. Sigma 7 based master side hardware.

  ) and (b).

Figure 6 (Fig. 5 .

 65 Figure 6(a) shows the success rate of peg transfers. A fail was attributed to the operator whenever a peg was dropped before reaching the intended target. A

Fig. 6 .

 6 Fig.6. Success of the pick and place task for all subjects and repetitions. Evaluation of the system through five normalized objective metrics.

Acknowledgements

This work was partially supported by French state funds managed by the ANR within the Investissements d'Avenir programme (Labex CAMI) under reference ANR-11-LABX-0004.