Emmanuel Hainry

Romain Péchoux

Type-based heap and stack space analysis in Java

A type system is introduced for a strict but expressive subset of Java in order to infer resource upper bounds on both the heap-space and the stack-space requirements of typed programs. The type system is inspired by previous works on Implicit Computational Complexity, using tiering and non-interference techniques. The presented methodology has several advantages. First, it provides explicit polynomial upper bounds to the programmer, hence its use could allow the programmer to avoid memory errors. Second, type checking is decidable in linear time. Last but not least, it has a good expressivity since it analyzes most object oriented features like overload, inheritance, override and can also handle statements that alter the control flow like break or return. In particular, it improves previous analyses on the complexity of OO and imperative programs since it can deal with loops guarded by objects (list, trees, cyclic data).

Introduction

Motivations. In the last decade, the development of embedded systems and mobile computing has led to a renewal of interest in predicting program resource consumption. This kind of issue is highly challenging for popular object oriented programming languages which come equipped with environments for applications running on mobile and other embedded devices (e.g. Dalvik, Java Platform Micro Edition (Java ME), Java Card and Oracle Java ME Embedded).

The current paper tackles such an issue by introducing a type system for a compile-time analysis of both heap and stack space requirements of Java-like programs thus avoiding OutOfMemory and StackOverFlow errors, respectively. The set of analyzed programs is a strict but expressive subset of Java, named core Java; features like recursion, while loops, inheritance, override, overload are handled by the presented analysis. Core Java can be seen as a language strictly more expressive than Featherweight Java [START_REF] Igarashi | Featherweight java: a minimal core calculus for java and GJ[END_REF] enriched with features like variable updates and while loops. Contribution. The presented type system combines ideas coming from tiering discipline, used for complexity analysis of function algebra [START_REF] Bellantoni | A new recursion-theoretic characterization of the poly-time functions[END_REF][START_REF] Leivant | Lambda calculus characterizations of poly-time[END_REF], together with ideas coming from non-interference, used for secure information flow analysis [START_REF] Volpano | A sound type system for secure flow analysis[END_REF]. It is inspired by two previous works: the seminal paper [START_REF] Marion | A type system for complexity flow analysis[END_REF], initiating imperative programs type-based complexity analysis using secure information flow, which provides a characterization of polynomial time computable functions; and the paper [START_REF] Hainry | Type-based complexity analysis for fork processes[END_REF], extending previous analysis to C processes with a fork/wait mechanism, which provides a characterization of polynomial space computable functions, but the current work improves the following points:

• first, it is a non trivial extension to the object-oriented paradigm (although imperative features can be dealt with) allowing to study both the complexity of object instantiation (using the new operator) and of loops guarded by objects. The difficulty in such a study is that the underlying structure is no more a string or a stack but a graph of memory references. Moreover, our work characterizes the complexity of recursive and non-recursive method calls whereas previous works were restricted to while loops,

• second, it studies both program extensional and intensional properties (like heap and stack) whereas previous papers were focusing on the extensional part (characterizing function spaces). Consequently, it is a wider study that is closer to a programmer's expectations,

• third, it provides explicit big O polynomial upper bounds while the two aforementioned studies were only certifying algorithms to compute a function belonging to some fixed complexity class.

Intuition. In the introduced type system, the heap is represented by a directed graph where nodes are object addresses and arrows relate an object address to its field addresses. The type system splits variables into two universes: tier 0 universe and tier 1 universe. While tier 1 variables are pointers to nodes of the initial heap, tier 0 variables may point to newly created addresses. The information may flow from tier 1 to tier 0, that is a tier 0 variable may depend on tier 1 variables. However our type system precludes flows from 0 to 1. Indeed once a variable has stored a newly created instance, it can only be of tier 0. Tier 1 variables are the ones that can be used either as guards of a while loop or as a recursive argument in a method call whereas tier 0 variables are just used as a storage for computed data. The polynomial upper bound is obtained as follows: if the input graph structure has size n then the number of distinct possible configurations for k tier 1 variables is at most O(n k ).

Motivating example. Consider the following Java code doubling the length of a boolean List as an illustrating example: y=x; while (x!=null){ y=new List(true,y); x=x.getTail(); } The tier of variable x will be enforced to be 1 since it is used in a while loop guard. On the opposite, the tier of variable y will be enforced to be 0 since the y=new List(true,y); instruction enlarges its memory use. For each assignment, we will check that the tier of the variable assigned to is smaller than the tier of the assigned expression. Consequently, the assignment y=x; is typable in this code (since 0 is smaller than 1 ; a flow from tier 1 to 0 being admissible) whereas x=y; or x=new List(true,x); are not typable wrt to this code as they might lead to unbounded computations. As explained above, it means that x never points to newly created addresses while y may. This typing discipline is illustrated by the following figure:

null List • • • • • • List y 0 , x 0 x n-1 x n List • • • • • • List y 1 y n
x i and y i represent the object referred to by x and, respectively, y just before the i+1-th iteration of the while loop. The dashed rectangle represents the tier 0 universe whereas the plain rectangle represents tier 1 universe. As explained above, tier 0 variables may grow and can also access to the tier 1 memory, but not the contrary. This is the reason why y 0 can point to the tier 1 memory at the beginning of the execution. To conclude, the loop guard in this small example could also been adapted to include circular structures like circular buffers and can be handled provided that the size of the guard is left unchanged. It is worth noticing that the studies mentioned below in the related works cannot deal with such programs. Related works. On imperative languages, the papers [START_REF] Niggl | Certifying polynomial time and linear/polynomial space for imperative programs[END_REF][START_REF] Moyen | Resource control graphs[END_REF][START_REF] Jones | A flow calculus of wp-bounds for complexity analysis[END_REF]] study theoretically the heap-space complexity of core-languages using type systems based on a matrix calculus.

On OO programming languages, the papers [START_REF]Type-based amortised heap-space analysis[END_REF][START_REF] Hofmann | Efficient type-checking for amortised heap-space analysis[END_REF] control the heap-space consumption using type systems based on amortized complexity introduced in previous works on functional languages [START_REF] Hofmann | Static prediction of heap space usage for first-order functional programs[END_REF][START_REF] Jost | Static determination of quantitative resource usage for higher-order programs[END_REF][START_REF] Beringer | Automatic certification of heap consumption[END_REF]. Though similar, our result differs on several points with this line of work. First, our analysis is not restricted to linear heap-space upper bounds. Second, it also applies to stack-space upper bounds. Last but not least, our language is not restricted to the expressive power of method calls and includes a while statement, controlling the interlacing of such a purely imperative feature with functional features like recursion being a very hard task from a complexity perspective.

Another interesting line of research is based on the analysis of heap-space and time consumption of Java bytecode [START_REF] Albert | Costa: Design and implementation of a cost and termination analyzer for java bytecode[END_REF][START_REF]Cost analysis of object-oriented bytecode programs[END_REF][START_REF] Kersten | Making resource analysis practical for real-time java[END_REF][START_REF] Cachera | Certified memory usage analysis[END_REF]. The results from [START_REF] Albert | Costa: Design and implementation of a cost and termination analyzer for java bytecode[END_REF][START_REF]Cost analysis of object-oriented bytecode programs[END_REF][START_REF] Kersten | Making resource analysis practical for real-time java[END_REF]] make use of abstract interpretations to infer efficiently symbolic upper bounds on resource consumption of Java programs. A constraint-based static analysis is used in [START_REF] Cachera | Certified memory usage analysis[END_REF] and focuses on certifying memory bounds for Java Card. Our analysis can be seen as a complementary approach since we try to obtain practical upper bounds through a cleaner theoretically oriented treatment. Consequently, this approach allows us to deal with our typing discipline on the original Java code without considering the corresponding Java bytecode. Moreover, our approach handles very elegantly while loops guarded by a variable of reference type whereas most of the aforementioned studies are based on invariants generation for primitive types only. A complex type-system that allows the programmer to verify linear properties on heap-space is presented in [START_REF] Chin | Memory usage verification for OO programs[END_REF]. Our result in contrast presents a very simple type system that however guarantees a polynomial bound.

In a similar vein, characterizing complexity classes below polynomial time is studied in [START_REF] Hofmann | Pointer programs and undirected reachability[END_REF][START_REF]Pure pointer programs with iteration[END_REF]. This work relies on a programming language called PURPLE combining imperative statements together with pointers on a fixed graph structure. Although not directly related, our type system was inspired by this work.

The presented work is independent from termination analysis but our main result relies on such analysis. Indeed, the polynomial upper bounds on both the stack and the heap space consumption of a typed program provided by Theorem 1 only hold for a terminating computation. Consequently, our analysis can be combined with termination analysis in order to certify the upper bounds on any input. Possible candidates for the imperative fragment are Size Change Termination [START_REF] Ben-Amram | Size-change termination, monotonicity constraints and ranking functions[END_REF][START_REF] Ben-Amram | On the termination of integer loops[END_REF], tools like Terminator [START_REF] Cook | Terminator: Beyond safety[END_REF] based on Transition predicate abstraction [START_REF] Podelski | Transition predicate abstraction and fair termination[END_REF] or symbolic complexity bound generation based on abstract interpretations, see [START_REF] Gulwani | Speed: Symbolic complexity bound analysis[END_REF][START_REF] Gulwani | Speed: precise and efficient static estimation of program computational complexity[END_REF] for example. Outline. In Section 2, we introduce the syntax of core Java and the notion of well-formed program. Section 3 describes the semantics of core Java based on graph structures called pointer graphs. In Section 4, the type system, which is the main contribution of the paper, is presented and explained. A full example is provided in Section 5 to explain the subtlety of the typing rules. Section 6 is devoted to present our main result, Theorem 1, direct corollaries as well as a decidability result on type inference. Finally, we show direct extensions in Section 7 to inheritance and to statements that break program control flow (break, return,...).

Core Java syntax

In this section, we introduce the syntax of the considered core Java language a strict but expressive subset of Java.

Syntax of classes

Expressions, instructions, constructors, methods and classes are defined by the grammar of Figure 1, with x ∈ V, op ∈ O, C ∈ C, m ∈ M, V being the set of variables, O the set of operators,

Expressions E ::= x | null | this | true | false | op(E 1 , . . . , E n ) | new C(E 1 , . . . , E n ) | E .m(E 1 , . . . , E n ) Instructions I ::= ; | [τ ] x:=E ; | I 1 I 2 | while(E ){I } | if(E ){I 1 }else{I 2 } | E .m(E 1 , . . . , E n ); Methods M C ::= τ m(τ 1 x 1 , . . . , τ n x n ){I [return x; ]} Cons K C ::= C(τ 1 y 1 , . . . , τ n y n ){x 1 :=y 1 ; . . . x n :=y n ; } Classes C ::= C{τ 1 x 1 ; . . . ; τ n x n ; K C M 1 C . . . M k C } Figure 1: Syntax of core Java
M the set of method names and C the set of class names. The τ s are type annotations ranging over C∪{void, boolean}. As usual, let [e] denote some optional element e. Moreover, as in Java ; denotes the empty instruction. The core Java syntax does not include a for instruction based on the premise that, as in Java, a for statement for(τ x:=E ; condition; Increment){Ins} can be simulated by the statement τ x:=E ; while(condition) {Ins Increment; }. Also notice that there is no field access in our syntax using the "." operator. Consequently, all fields are implicitly private. In contrast, methods and classes are all public. This is not a huge restriction for a Java programmer since any field can be accessed and updated in an outter class by writing the corresponding getter and setter.

Definition 1. A core Java program is a collection of classes together with exactly one executable:

Exe{main(){τ 1 x 1 := E 1 ; . . . ; τ n x n := E n ; I }}
In an executable, the instruction τ 1 x 1 := E 1 ; . . . ; τ n x n := E n ; is called the initialization instruction whereas I is called the computational instruction.

In a class C = C{τ 1 x 1 ; . . . ; τ n x n ; K C M 1 C . . . M k C }, the x i s are called fields. Moreover let C.A denote the set of the fields of C, i.e. C.A = {x 1 , . . . , x n }. In a method or constructor, the arguments are called parameters. Finally, each variable declared in an assignment of the shape τ x:=E ; is called a local variable. Given a method τ m(τ 1 x 1 , . . . , τ n x n ){I [return x; ]} of C, we say that its signature is τ m C (τ 1 , . . . , τ n ) ; the notation m C denoting that m is declared in C.

For readability, we assume classes have exactly one constructor initializing all the class fields. Also, the only considered primitive data are boolean values true and false. Other primitive data types such as floats, integers and characters could be considered, as explained in Subsection 4.4.1. In the presented syntax, there is no inheritance and, consequently, no overrides even if those features can be handled by our type system. For simplicity and readability, their treatment will be delayed to Section 7. Notice however that overload is possible in the initial core Java syntax.

Well-formed programs

Throughout the paper, only well-formed programs satisfying the following conditions will be considered:

• Each class name C appearing in the collection of classes corresponds to exactly one class of name C within the collection.

• A variable appearing in the collection of classes is either a local variable, a field or a parameter. For simplicity, we assume that programs are statically transformed up-to α-conversion so that each variable (local variable, field or parameter) has a distinct name, hence preventing name clashes.

• Each local variable x is both declared and initialized exactly once by a τ x := E ; instruction before its first use.

• A method output type is void iff it has no return statement.

• Each method signature is unique.

3 Core Java pointer graph semantics

In this section, a pointer graph semantics of core Java programs is provided. A pointer graph is basically a graph structure representing the memory heap, whose nodes are references, together with a mapping associating a reference to a given variable. The pointer graph semantics is designed to work on such a structure together with a stack, for method calls, and a store, for primitive values. The semantics will be defined on meta-instructions, flattened instructions with stack operations.

Pointer graph

Definition 2. A pointer graph G P is a directed multigraph G = (V, A) together with a mapping P.

The nodes in V are references labeled by class names and the arrows in A link one reference to a reference of its fields and are labeled by the field name. In what follows, let l be the node label mapping from V to C and i be the arrow label mapping from A to ∪ C∈C C.A.

The partial mapping P : V ∪ {this} → V associates a node of the graph in V to some variables in V or to the current object this and is called a pointer mapping. Let dom(P) be the domain of P.

The memory used by a core Java program will be represented by a pointer graph. Each constructor call will create a new node of the graph and arrows to its fields. It also respects the dynamic binding principle found in Object Oriented Languages. Those arrows are annotated by the field name. The semantics of an assignment x := E ; consists in updating the pointer mapping in such a way that P(x) will be the reference of the object computed by E .

The heap in which the objects are stored corresponds to the graph. Consequently, bounding the heap memory use consists in bounding the size of the computed graph, the size of a graph being the number of nodes.

Figure 2 illustrates the pointer graph associated to a sequence of object creations. The figure contains both the graph of labeled nodes and arrows together with the pointer mapping whose domain is represented by boxed variables and whose application is symbolized by snake arrows.

Pointer stack

The pointer stack of a program is used when calling a method: references to the parameters are pushed on the stack. In our context, the pointer stack will contain pointer mappings: Definition 3. A pointer stack S G is a LIFO structure S of pointer mappings corresponding to the same directed graph G. Given a pointer stack S G , define S to be the topmost pointer mapping of S.

Intuitively, the pointer mappings of a pointer stack S G map method parameters to the references of the arguments on which they are applied. Notice that all parameters can be mapped in such a way since they are of reference type by well-formedness assumption. Consequently, they are distinct from the pointer mapping in the pointer graph. For example, considering a method m defined as τ m(τ 1 y){J ; return z} in a method call x := E .m(F ); will push a new pointer mapping P on pointer stack S G such that P(y) points to the node corresponding to the object computed by F . We will see in the next subsection that pop operation removing the top pointer mapping from the pointer stack will correspond, as expected, to the evaluation of a return statement in a method body.

[τ ] x:=E

; = [τ ] x:=E ; if E ∈ V ∪ {this, null, true, false} [τ ] x:=op(E 1 , . . . , E n ); = τ 1 x 1 :=E 1 ; . . . τ n x n :=E n ; [τ ] x = op(x 1 , . . . , x n ); [τ ] x:=new C(E 1 , . . . , E n ); = τ 1 x 1 :=E 1 ; . . . τ n x n :=E n ; [τ ] x:=new C(x 1 , . . . , x n ); [[τ ] x:=]E .m(E 1 , . . . , E n ); = τ 1 x 1 :=E 1 ; . . . τ n x n :=E n ; τ n+1 x n+1 = E ; [[τ ] x:=]x n+1 .m(x 1 , . . . , x n ); I 1 I 2 = I 1 I 2 while(E ){I } = boolean x 1 := E ; while(x 1 ){I x 1 := E ;} if(E ){I 1 }else{I 2 } = boolean x 1 := E ; if(x 1 ){I 1 }else{I 2 }
All x i represent fresh variables and the types τ i match the expressions E i types

Memory configuration

A primitive store σ is a partial mapping σ : V → {true, false} associating a boolean value to some variable of primitive data type in V. As usual, the domain of a primitive store σ is denoted dom(σ).

A memory configuration consists in a heap together with a stack and a store:

Definition 4.
A memory configuration C is a quadruple G, P, S, σ such that G P is a pointer graph, S G is a pointer stack and σ is a primitive store. Among memory configurations, the initial configuration C 0 defined by

C 0 = ({&null}, ∅), ∅, [], ∅
where the notation ∅ is used both for empty set and empty mapping, [] denotes the empty pointer stack, and &null is the reference of the null object (i.e. l(&null) = null).

Meta-language and flattening

The semantics of core Java programs will be defined on a meta-language of expressions and instructions. Meta-expressions are flat expressions. Meta-instructions consist in flattened instructions and pop and push operations for managing method calls. Meta-expressions and meta-instructions are defined formally by the following grammar:

ME ::= x | null | this | true | false | op(x 1 , . . . , x n ) | new C(x 1 , . . . , x n ) | y.m(x 1 , . . . , x n ) MI ::= ; | [τ ] x:=ME ; | MI 1 MI 2 | x.m(y 1 , . . . , y n ); | while(x){MI } | if(x){MI 1 }else{MI 2 } | pop; | push(P); |
where denotes the empty meta-instruction.

Flattening an instruction I into a meta-instruction I will consist in adding fresh intermediate variables for each complex parameter. This procedure is standard and defined in Figure 3. The flattened meta-instruction will keep the semantics of the initial instruction unchanged. The main interest in such a program transformation is just that all the variables will be statically defined in a meta-instruction whereas they could be dynamically created by an instruction,

(C, ; MI ) → (C, MI ) (1) (C, [τ ] x:=null; MI ) → (C[P : x → null], MI ) (2) (C, [τ ] x:=w; MI ) → (C[σ : x → w], MI ) w ∈ {true, false} (3)
(C, [τ ] x:=y; MI ) → (C[µ : x → C(y)], MI ) µ ∈ {σ, P, S} (4)
(C, [τ ] x:=this; MI ) → (C[P : x → S(this)], MI ) (5) (C, [τ ] x:=op(y 1 , . . . , y n ); MI ) → (C[σ : x → op (C(y 1 ), . . . , C(y n ))], MI ) (6) (C, [τ ] x:=new C(y 1 , . . . , y n ); MI ) → (C[V : v → C][A : (v, C(y i )) → z i ][P : x → v], MI )
where v is a fresh node and C.A = {z 1 , . . . , Proof. By induction on the definition of flattening.

z n } (7) (C, [[τ ] x:=]y n+1 .m(y 1 , . . . , y n ); MI ) → (C, push({this → C(y n+1 ), z i → C(y i )}); MI [x:=z; ] pop; MI ) if m is a flattened method τ m(τ 1 z 1 , . . . τ n z n ){MI [return z; ]} (8) (C, push(P); MI ) → (C[S : push(P)], MI ) (9) (C, pop; MI ) → (C[S : pop], MI ) (10) (C, while(x){MI } MI ) → (C, MI while(x){MI } MI ) if C(x) = true (11) (C, while(x){MI } MI ) → (C, MI ) if C(x) = false (12) (C, if(x){MI true }else{MI false } MI ) → (C, MI C(x) MI ) if C(x) ∈ {true, false} (13)

Program semantics

Informally, the small step semantics → of core Java relates a pair (C, MI ) of memory configuration C and meta-instruction MI to another pair (C , MI ) consisting of a new memory configuration C and of the next meta-instruction MI to be executed. Let → * (respectively → + ) be its reflexive and transitive (respectively transitive) closure. In the special case where (C, MI ) → * (C , ), we say that MI terminates on memory configuration C.

Definition 5. A core Java program of executable Exe{main(){τ 1 x 1 := E 1 ; . . . ; τ n x n := E n ; I }} terminates if the following conditions hold: 1. (C 0 , τ 1 x 1 := E 1 ; . . . ; τ n x n := E n ;) → * (C, ) 2. (C, I ) → * (C , )
The memory configuration C computed by the initialization instruction is called the input. Now we introduce some preliminary notations. Given a memory configuration C = G, P, S, σ , let C(x) be defined by: The rules of → are defined formally in Figure 4. Rules ( 2) to ( 8) are transitions for the distinct assignment of an expression to a variable. Rule ( 2) is the assignment of the null reference &null to a variable. Consequently, it updates the pointer mapping P. Rule (3) is the assignment of a primitive boolean value to a variable. Consequently, it updates the primitive store σ. Rule (4) describes the assignment of a variable to another. It updates the primitive store if it is a primitive value, or updates the current pointer mapping or the top pointer mapping in the pointer stack, depending on whether the considered variable is a parameter or not. Rule (5) consists in the assignment of the self-reference. Consequently, it updates the pointer mapping P after searching the reference of the current object at the top of the pointer stack (i.e. S(this)). Notice that such an assignment may only occur in a method body (because of well-formedness assumptions) and consequently the stack is non-empty and must contain a reference to this. Rules [START_REF] Ben-Amram | On the termination of integer loops[END_REF][START_REF] Cachera | Certified memory usage analysis[END_REF][START_REF] Cook | Terminator: Beyond safety[END_REF] are just structural rules introducing fresh local variables x i s in order to evaluate parameters in a operator evaluation, object creation or method call. Consequently, they need to enforce that the x i s are fresh variables, i.e. x i / ∈ dom(C). Rule (6) consists in operator evaluation and updates the primitive store since operator outputs are restricted to be of boolean type. Rule [START_REF] Cachera | Certified memory usage analysis[END_REF] consists in the creation of a new instance. Consequently, this rule adds a new node v of label C and the corresponding arrows (v, C(y i )) of label z i in the graph. C(y i ) are the nodes of the graph corresponding to the parameters of the constructor call (or the boolean values if they are of type boolean) and z i is the corresponding field name in the class C. Finally, this rule adds a link from the variable x to the new reference v in the pointer mapping P. Rule (8) consists in a call to method m. It adds a new instruction for pushing a new pointer mapping on the stack, containing references of the current object this on which m is applied and references of the parameters. After adding the flattened body MI of m to the evaluated instruction, it adds an assignment storing the returned value z in the assigned variable x, whenever the method is not a procedure, and a pop; instruction. Rules ( 9) and ( 10) are standard rules for manipulating the pointer stack through the use of pop and push instructions.

C(x) =      σ(x) if x ∈ dom(σ) S(x) if x ∈ dom( S) P(x) if x ∈ dom(P) and let C[µ : x → v], µ ∈
Rules [START_REF] Gulwani | Speed: precise and efficient static estimation of program computational complexity[END_REF] to ( 13) are standard rules for control flow statements.

α i = 1).
A tiered type is a pair τ (α) consisting of a type τ ∈ T together with a tier α ∈ {0, 1}. Given a tiered type, the two projections π 1 and π 2 are defined by π 1 (τ (α)) = τ and π 2 (τ (α)) = α.

Intuitively, tier 0 will be used to type variables whose stored values might increase during a computation whereas tier 1 will be used to type variables used in the guard of a while loop or as an argument of a recursive method call. The values stored in a tier 1 variable will not be allowed to increase during a computation.

Environments

A field typing environment δ m C for a method m of class C maps each field v ∈ C.A to a tiered type.

A local variable and parameter typing environment δ maps each non-field variable in V to a tiered type.

A typing environment ∆ is a list containing the unions δ m C δ, for each field typing environment δ m C and for the local variable and parameter typing environment δ. Let ∆(m C ) denote δ m C δ.

The main reason for defining typing environments this way is to allow the programmer to type a field with distinct tiers depending on the considered method. Indeed, a field can be used as a guard of a while loop (and will be of tier 1) in some method whereas it can store freshly created objects (and will be of tier 0) in some other method. In order to simplify our type system, one could consider all the field typing environments to be the same but this would impact negatively the expressivity of our type system.

Since a field can have distinct tiered types depending on the considered method, our type system has to keep information on the context (i.e. the method) while typing an expression or an instruction. In order to overcome this problem, we introduce the notion of contextual typing environment.

A contextual typing environment Γ = (m C , ∆) is a pair consisting in a method and a typing environment. The method m C in the contextual typing environment (m C , ∆) indicates under which context the fields should be typed, in other words which field typing environment is considered. We will write ( , ∆) when the context is empty. We assume that ∆( ) represents the local variable and parameter typing environment δ.

Well-typed programs 4.3.1 Operator signature

The language is restricted to operators whose return type is boolean1 . An operator of arity n comes equipped with a signature of the shape τ 1 × • • • × τ n → boolean, fixed by the language implementation. In the type system, the notation op ::

τ 1 × • • • × τ n → boolean denotes that op has signature 2 τ 1 × • • • × τ n → boolean.

Judgments

Expressions and instructions will be typed using tiered types whereas constructors and methods of arity n have types of the shape:

τ 1 (α 1 )×. . .×τ n (α n ) → τ (α) and C(β)×τ 1 (α 1 )×. . .×τ n (α n ) → τ (α)
, respectively. Given a contextual typing environment Γ, there are four kinds of typing judgments:

• The judgment Γ E : τ (α) means that expression E corresponds to values of tiered type τ (α).

• The judgment Γ I : void(α) is similar. The type is enforced to be void, meaning that instructions have no return value3 .

• The judgment Γ K C : τ 1 (α 1 ) × • • • × τ n (α n ) → C(0)
enforces the output of a constructor to be of the correct type C and to be of tier 0. This important tiering restriction will prevent object instantiation in variables of tier 1.

• The last judgment Γ M C : C(β) × τ 1 (α 1 ) × • • • × τ n (α n ) → τ (α)
for methods is similar but with unrestricted tiers. The first tiered type C(β) is the tiered type of the current object this and, consequently, its base type C is enforced to match the class of the considered method.

Well-typedness

Let us now introduce the notion of well-typed program. Intuitively, a well-typed program has an executable whose initialization instruction is only constrained by types and whose computational instruction is both constrained on types and tiers. The type system propagates these constraints on all the classes, methods and instructions used within these instructions. (Null)

Γ null : C(1) ∆(m C )(x) = τ (α) (Var) (m C , ∆) x : τ (α) α ∆(m C ) (Self ) (m C , ∆) this : C(α) ∀i, Γ E i : τ i (α) op :: τ 1 × • • • × τ n → boolean (Op) Γ op(E 1 , . . . , E n ) : boolean(α) ∀i (m C , ∆) E i : τ i (β i ) α i β i ( , ∆) C(. . . τ i y i . . .){. . . x i := y i ; . . .} : τ 1 (α 1 ) × • • • × τ n (α n ) → C(0) (New) (m C , ∆) new C(E 1 , . . . , E n ) : C(0) ∀i (n D , ∆) E i : τ i (β i ) α i β i ( , ∆) m : C(β) × τ 1 (α 1 ) × • • • × τ n (α n ) → τ (α) (n D , ∆) E : C(β) (Call) (n D , ∆) E .m(E 1 , . . . , E n ) : τ (α) (a) Expressions Γ x : τ (α) Γ E : τ (β) α β (Ass) Γ [τ ]
x:=E ; :

void(α) Γ I : void(α) α β (Sub) Γ I : void(β) ∀i, Γ I i : void(α i ) (Seq) Γ I 1 I 2 : void(α 1 ∨ α 2 ) Γ E : boolean(1) Γ I : void(1) (Wh)
Γ while(E ){I } :

void(1) (Skip)
Γ ; :

void(0) Γ E : boolean(α) ∀i, Γ I i : void(α) (If ) Γ if(E ){I 1 }else{I 2 } : void(α) (b) Instructions
∀i, ( , ∆)

y i : τ i (α i ) (K C ) ( , ∆) C(τ 1 y 1 , . . . , τ n y n ){x 1 := y 1 ; . . . x n := y n } : τ 1 (α 1 ) × • • • × τ n (α n ) → C(0) (m C , ∆) this : C(β) ∀i, (m C
, ∆)

x i : τ i (α i ) (m C , ∆) x : τ (α) (m C , ∆) I : void(α) (M C ) ( , ∆) τ m(τ 1 x 1 , . . . , τ n x n ){I return x; } : C(β) × τ 1 (α 1 ) × • • • × τ n (α n ) → τ (α) (m C , ∆) this : C(β) ∀i, (m C , ∆) x i : τ i (α i ) (m C , ∆) I : void(α) (M void C ) ( , ∆) void m(τ 1 x 1 , . . . , τ n x n ){I } : C(β) × τ 1 (α 1 ) × • • • × τ n (α n ) → void(α)
( , ∆) I : void(1) ∀i, ( , ∆)

x i : τ i (α i ) ∀i, ( , ∆) E i : τ i (β i ) (Main)
( , ∆) Exe{main(){τ The typing rules for expressions are provided in Figure 5a. Rules (True) and (False) mean that boolean constants are of type boolean and tier 1 as they cannot increase. It is possible to add other Java primitive data types such as float, integer, char. As for booleans, they will be associated to tiered types of tier 1 since a value of primitive data type can be considered as a constant. Note that this is counter-intuitive since a while loop controlled by a guard of primitive data type will be treated as a constant time instruction but not surprising since all primitive data type values are stored on a constant number of bits.

Rule (Null) means that, as in Java and for polymorphic reasons, null can be considered of any class C and of tier 1 as it cannot increase.

The (Self ) rule explicits that the self reference this belongs to class C (the class of the context) and has a tier lower than the minimum of the fields' tiers under the typing environment ∆(m C ), denoted by ∆(m C ) and defined formally by:

∆(m C ) = ∧ x∈C.A (π 2 (∆(m C )(x))).
This entails that an object of tier 1 has no field of tier 0. In other words, no arrow will go from a node corresponding to a tier 1 variable to a field node of tier 0.

Rule (Var) is standard. Rule (Op) describes how to type an expression consisting of an operator of a given signature applied to n arguments. The n arguments must be expressions of types corresponding to the operator signature. The expressions must be of the same tier α which will also be the tier of the whole expression. It prevents information to flow from tier 0 to tier 1. Note that flows from tier 1 to tier 0 are also prohibited in this rule. This is not a restriction since they are useless: operators only return booleans and, consequently, their computations cannot increase the memory.

Rule (New) describes the typing of object instantiation. It checks that the constructor arguments have tiered types τ i (β i ) of the same types τ i and of tier not lower than the admissible tiers α i in the constructor typing judgment. Note that the new instance has type of the right class and tier 0 since its creation makes the memory grow (hence it cannot be of tier 1).

Rule (Call) represents how to type method calls of the shape E .m(E 1 , . . . , E n ). First, we check that the tiered type C(β) of the self reference in the method m is equal to the tiered type of the instance E . While checking the method's type, the current method in the contextual typing environment is updated to m C . We check that the arguments' types match the parameters' types in m's signature and that the tiers of those arguments β i are not lower than the tiers α i in the method typing judgment. An important point to stress is that the tier of the evaluated expression (or instruction) in a method call matches the tier of the return variable in the method, hence avoiding forbidden information flows.

Instructions

The typing rules for instructions are provided in Figure 5b.

Rule (Ass) explains how to type an assignment: it is an instruction, hence of type void. It is only possible to assign an expression E to a variable x if both the types match and the tier β of E is higher than the tier α of x. The tier of the instruction will be α. This rule implies that information may flow from tier 1 to tier 0 but not the contrary. In other words, a tier 1 variable cannot be assigned to in a tier 0 instruction block whereas a tier 0 variable can be assigned to without any constraint, hence allowing an implicit sub-typing for expressions. This rule can be used both if the assignment is a declaration (the type τ is given) or not.

Rule (Sub) is a sub-typing rule. An instruction of tier α can also be tiered by β with α β. This means that a tier 0 instruction, where tier 1 variables cannot be modified, can be considered as a tier 1 instruction where tier 1 variables might be modified, thus relaxing confidentiality constraints.

Rule (Seq) types the sequence of two instructions I 1 and I 2 . Once again, the type of instructions is void. The sequence's tier will be the maximum of the tiers of I 1 and I 2 . The intuition is the same as for the (Sub) rule.

Rule (Wh) is the most important typing rule as it will constrain the use of while loops. In a statement while(E ){I }, the guard of the loop E must be a boolean expression of tier 1 so that the guard is controlled. The instruction I , of type void, has to be of tier 1 since we expect the guard variables to be modified (i.e. assigned to). The whole statement is an instruction of type void and tier 1.

Rule (Skip) is standard. Rule (If ) describes the typing discipline for a if(E ){I 1 }else{I 2 } statement. E needs to be a boolean expression of tier α. I 1 and I 2 are instructions, hence of type void, with the same tier α. Combined with rule (Seq), it prevents assignments of tier 1 variables in the instructions I 1 and I 2 to be controlled by a tier 0 expression.

Methods, constructors and executable

The typing rules for constructors and methods are provided in Figure 5c.

Rule (K C ) describes the typing of a constructor definition. Constructors are of fixed form, so the only thing to check is that the parameters are of the desired tiered types. As explained in Rule (New) the output tier can only be 0.

Rules (M void

C

) and (M C ) show how to type method definitions in the case where the method is a procedure (i.e. there is no return statement) and in the case where it returns a value. A procedure is defined with the void return type. If a method has a return type τ , its body must finish by a return x statement with x of tiered-type τ (α). In this case, the output type of the method will also be τ (α). In both cases, the types and number of parameters need to match the method signature, the instruction I in the body of the method needs to be of type void(α), i.e. the tier matches the output tier so that there is no forbidden information flow.

Finally, typing an executable is done through the rule (Main) and consists in verifying that the initialization instruction respects types and that the computational instruction (denoted by instruction I ) is of tier 1. Notice that no tier constraints are checked in the initialization instruction: this means that we do not control the complexity of this latter instruction ; the main reason for this choice is that this instruction is considered to be building the program input. In contrast, the computational instruction I is considered to be the computational part of the program and has to respect the tiering discipline.

Type preservation under flattening

We show that the flattening of a typable instruction has a type preservation property. A direct consequence is that the flattened program can be considered instead of the initial program.

Proposition 1. Given an instruction I and a contextual typing environment Γ = (m C , ∆) such that Γ I : void(α) holds, there is a contextual typing environment Γ = (m C , ∆ ) such that the following holds:

• ∀n D , ∀x ∈ dom(∆(n D )), ∆(n D )(x) = ∆ (n D )(x) • Γ I : void(α)
Conversely, if Γ I : void(α), then Γ I : void(α).

Proof.

By induction on program flattening on instructions. Consider a method call I = τ x = E .m (E 1 , . . . , E n ); such that Γ I : void(α) and Γ = (m C , ∆). This means that Γ E i : τ i (α i ), Γ x : τ (α) and Γ E : C (β) hold, for some α i , β and C . The flattening of I is of the shape J [τ ] x = x n+1 .m (x 1 , . . . , x n ); with J = τ 1 x 1 :=E 1 ; . . . τ n x n :=E n ; τ n+1 x n+1 :=E ;. Let Γ = (m C , ∆ ) for the environment ∆ defined, for each method n D , by:

∆ (n D )(y) =            τ (α) if y = x τ i (α i ) if y ∈ {x 1 , . . . , x n } C (β) if y = x n+1 ∆(n D )(y) otherwise
We have Γ J [τ ] x = x n+1 .m (x 1 , . . . , x n ); : void(α) and Γ J : void(α) (sub-typing might be used). By induction hypothesis, there is a contextual typing environment Γ = (m C , ∆ ) such that Γ J : void(α) and ∀n D , ∀x ∈ dom(∆ (n D )), ∆ (n D )(x) = ∆ (n D )(x) and, consequently, Γ I : void(α). All the other cases are treated similarly.

5 Illustrating examples

Sorting lists

Let us apply our framework to a simple list sorting program. We define two classes : BList for encoding binary integers as binary lists (with the least significant bit in head) and IList for encoding lists of integers. Tiers are made explicit in the code: The notation x α means that x has tier α under the considered contextual typing environment Γ, i.e. Γ x : τ (α), for some τ , whereas I : α means that Γ I : void(α). The method getQueue can be typed by BList(1) → BList(1) or BList(0) → BList(1), if ∆(getQueue BList )(queue)=1, and by BList(0) → BList(0), if ∆(getQueue BList )(queue)=0, by rules (M C ) and (Self).

The type BList(1) → BList(0) is prohibited by rule (Self) since the tier of the current object 1 has to be lower than the minimum tier of its arguments 0.

12 void setQueue ( B L i s t q ) { 13 queue = q ; 14 }

The method setQueue can be given the types BList(1) × BList(1) → void(1), BList(0) × BList(1) → void(α), or BList(0) × BList(0) → void(α), α ∈ {0, 1}.

The input type BList(1) × BList(0) is prohibited since the tier of parameter q (0) has to be greater than the tier of the field queue, by rule (Ass); but this latter tier has to be greater than the tier of the current object (1), by rule (Self). Finally, the output tier corresponds to the tier of the typed instruction by rule (M C ). Consequently, it also corresponds to the tier of the field queue by rule (Ass) and is enforced to be 1 when the current object has type 1, by the rule (Self). Notice that it can be 1 whenever the object's current tier is 0 using the subtyping rule (Sub).

15

boolean g e t V a l u e ( ) { 16 return v a l u e ; 17 } getValue can be given the types BList(1) → boolean(1), BList(0) → boolean [START_REF] Albert | Costa: Design and implementation of a cost and termination analyzer for java bytecode[END_REF] or BList(0) → boolean(0) (the explanations are the same than for the getQueue getter). The method double can be typed by BList(0) → BList(0) or BList(1) → BList(0). Indeed the local variable n is enforced to be of tier 0 by a combination of rules (K C ) and (Ass). Consequently, the method output type is BList(0) since it has to match the type of the returned variable. Finally, there is no constraint on the current object admissible types since it is left unchanged by the method. The method decrement is recursive and can be given the BList(1) → void(1) (as we shall see later in Subsection 6.2, this type is mandatory by safety condition). This type enforces the tier of the each field to be 1 by rule (Self). Finally, the method body can be typed using a combination of rules (Ass), (If) and (Call). The explanations are the same as the ones for the isEqual method. Consequently, the admissible types are BList(1) × BList(1) → boolean(α), α ∈ {0, 1}. Now we let the reader check the methods of the class IList can be typed as follows using the typing environment ∆ such that: ∆(m IList )(value)=1 and ∆(m IList )(queue)=1, for each method m of the class IList. Now we show that the executable Exe using instances of both BList and IList is well-typed. First notice that the type system only checks constraints on base type in the initialization instruction. Second, constraints on tiered types are checked in the computational instruction: since the method sort can be given IList(1) → IList(0), the variable s is enforced to be of the tiered type IList(0) (as the corresponding data might increase though it is not the case in this particular example) whereas variable l is enforced to be of tier 1 (as the method sort iterates on its data). Finally, i3 has to be of tier 1 because of the type given to the method decrement (for more details, see also the definition of safety in Subsection 6.2). Note that this implementation of sort creates a new structure (of tier 0), hence is not composable with itself. In the case of sort, it is possible to do it in place, meaning that it would be of type IList(1) → IList(1) which in turn would be composable. This illustrates the fact that if one wants to compose methods in a typable way, there needs to be at most one method from tier 1 to tier 0.

void c o n c a t ( B L i s t o t h e r

Cyclic structure

As we have previously defined a list of booleans (for simulating integers), we can design classes for cyclic data. This is illustrated by the following example.

Ring { // c l a s s i m p l e m e n t i n g a r i n g as a c y c l i c l i s t boolean data ; Ring next ; Ring prev ; Ring ( boolean data , Ring next , Ring prev ) { t h i s . data = data ; t h i s . next = next ; t h i s . prev = prev ; } void i n i t ( ) { // t o be c a l l e d a f t e r t h e c o n s t r u c t o r .

i f ( next == null ) { next = t h i s ; prev = t h i s ;

• The size of a pointer stack S G is defined to be the number of pointer mappings in the stack S and denoted |S G |.

• The size of a memory configuration G, P, S, σ is equal to

|G P |+|dom(P)|+|S G |+|dom(σ)|.
Since a pointer graph contains both references to the objects (the nodes) and references to the field instances (the arrows), it would make sense to bound both the number of nodes and the number of arrows in order to control the heap-space, for a practical application. Notice that the out-degree of a node is bounded by a constant of the program (the maximum number of fields in a class) and, consequently, bounding the number of nodes is sufficient to obtain a big O bound. The size of a pointer stack is very close to the size of the Java Virtual Machine stack since it counts the number of nested method calls.

Given two methods M C and M C of respective signatures s and s and respective names m and m , define the relation on method signatures by s s if m is called in M C , i.e. in the body of M C (this check is fully static as long as we do not consider inheritance). Let + be its transitive closure. A method of signature s is recursive if s + s holds. Given two method signatures s and s , s ≡ s holds if both s + s and s + s hold. Given a signature s, the equivalence class [s] is defined as usual by [s] = {s | s ≡ s}. When the signature s of a given method M C of name m is clear from the context, we will write [m] as an abuse of notation for [s] and say that M C is a recursive method. Finally, we write s + s if s + s holds and s + s does not hold.

The notion of level of a meta-instruction is introduced to compute an upper bound on the number of recursive steps for a method call evaluation. Definition 8 (Level). Let the level λ of a method signature be defined as follows:

• λ(s) = 0 if s / ∈ [s] • λ(s) = 1 + max{λ(s ) | s + s } otherwise. 4
By abuse of notation, we will write λ(m) when the signature of m is clear from the context. For a given program, we denote the maximal level of a method by λ.

The notion of intricacy corresponds to the number of nested while loops in a meta-instruction and will be used to compute the requested upper bounds. Definition 9 (Intricacy). Let the intricacy ν of a meta-instruction be defined as follows:

• ν(; ) = ν(pop; ) = ν(push(P); ) = ν(x:=ME ; ) = 0 • ν(MI MI ) = max(ν(MI ), ν(MI )) • ν(if(x){MI }else{MI }) = max(ν(MI ), ν(MI )) • ν(while(x){MI }) = 1 + ν(MI )
Moreover, let ν be the maximal intricacy of a meta-instruction within a given program.

Notice that both intricacy ν and level λ are bounded by the size of their corresponding program.

Safety restriction on recursive methods

Now we put some side restrictions on recursive methods to ensure that their computations remain polynomially bounded. Recursive methods will be restricted to have only one recursive call and no while loop in their body (to prevent exponential growth) and must have tier 1 input (as the guard of a while) and output (to prevent a recursive dependence on a tier 0 variable). Definition 10 (Safety). A well-typed program wrt a typing environment ∆ is safe if for each recursive method M C = τ m(τ 1 y 1 , . . . , τ n y n ){MI [return x; ]}:

• there is exactly one call to some m ∈ [m] in MI ,

• there is no while loop inside MI , i.e. ν(MI ) = 0,

• and the following judgment can be derived:

( , ∆) M C : C(1) × τ 1 (1) × • • • × τ n (1) → τ (1).
Remark 1. A program is safe with respect to a typing environment ∆ iff its flattened version is safe with respect to the contextual typing environment ( , ∆ ) that is obtained using Proposition 1.

Example 1. The program of Section 5 is safe. Indeed the recursive method decrement can be typed by BList(1) → void(1), does not contain any while loop and has only one recursive call in its body.

Intermediate lemmata

In this section, we introduce intermediate lemmata that allow us to prove the main result. In order to present a simple proof, we will make the assumption that all the fields of each class C have the same tier under all the distinct field typing environment (i.e. ∀x, ∀m, m , ∆(m C )(x) = ∆(m C )(x)). This assumption is not strong in the sense that a class C with a field x having distinct tiers depending on the considered method can be easily transformed into a typable class satisfying this condition. For this purpose, it suffices to replace x by two new fields x 0 and x 1 of the same base type τ such that x α will only be used in methods m C where ∆(m C )(x) = τ (α). Given a memory configuration C and a typing environment ∆, define the tier 1 memory configuration C ∆ 1 by:

C ∆ 1 (x) = C(x) if ∆(m C )(x) = τ (1), τ ∈ C ∪ {boolean} ⊥ otherwise
where the symbol ⊥ means that C ∆ 1 is undefined on the given input. Given a configuration C and a meta-instruction MI , the distinct tier 1 configuration sequence ξ ∆ 1 (C, MI ) wrt contextual typing environment ∆, is defined by:

• If (C, MI ) → (C , MI ) then: ξ ∆ 1 (C, MI ) = C ∆ 1 .ξ ∆ 1 (C , MI ) if C ∆ 1 = C ∆ 1 ξ ∆ 1 (C , MI ) otherwise • If MI = then ξ ∆ 1 (C, MI ) = C ∆ 1 .
As usual, the size |s| of a sequence s (respectively the cardinal #S of a set S) is the number of elements in s (resp. S).

Informally, ξ ∆ 1 (C, MI ) is a record of the distinct tier 1 memory configurations encountered during the evaluation of (C, MI ). Now we can show a non-interference property à la Volpano et al. [START_REF] Volpano | A sound type system for secure flow analysis[END_REF] stating that given a safe program, there is no information flow from tier 0 variables to 1 variables.

Lemma 2 (Non-interference). Given a meta-instruction MI of a safe program with respect to typing environment ∆, let C and C be two memory configurations, if

C ∆ 1 = C ∆ 1 then ξ ∆ 1 (C, MI ) = ξ ∆ 1 (C , MI ).
In other words, tier 1 variables do not depend on tier 0 variables.

Proof. First, note that Rule (Wh) of Figure 5b and the definition of safe programs enforce all the guards of a safe program (in a while loop and in a recursive call) to be of tier 1. Applying Proposition 1, tier 1 meta-instructions do not depend on loops controlled by tier 0 expressions. Second, in a if meta-instruction of tier 0 guard, all the commands are of tier 0 by Rule (If ). Consequently, no tier 1 variable is updated in these commands. Indeed a tier 1 variable assignment enforces the containing command to be of tier 1 using Rule (Ass) and Rule (Seq). Finally, the rule (Ass) in Figure 5b enforces that tier 1 variables of a safe program are only updated by assignments of the shape Γ x:=E ; : void(1). All the variables contained in E are enforced to be of tier 1 (except the current object or the parameters in the special case of non recursive methods) by the type system. Consequently, if C ∆ 1 = C ∆ 1 and (C, x:=E ; MI ) → (D, MI ) then (C , x:=E ; MI ) → (D , MI ) and D ∆ 1 = D ∆ 1 . Now the case of a non recursive method is trivial since its code can be inlined while still being typed under ∆. And so is the case where the current object variable is of tier 0 since the method return variable tier is enforced to be 1 by Rules (Ass), (Call) and (M C ). Consequently, there is no information flow from the current object to the return variable in the method body in this particular case.

Using Lemma 2, if a safe program evaluation encounters twice the same meta-instruction under two configurations equal on tier 1 variables then the considered meta-instruction does not terminate on both configurations. Proof. Assume that during the transition (C, MI ) → + (C , MI ) there is a C such that

C ∆ 1 = C ∆ 1 , then the distinct tier 1 configuration sequence ξ ∆ 1 (C, MI ) contains this C ∆ 1 before C ∆ 1 .
From the construction of the sequence, we deduce that ξ ∆ 1 (C, MI ) is of the shape . . . C ∆ 1 . . . ξ ∆ 1 (C , MI ). However from Lemma 2, ξ ∆ 1 (C, MI ) = ξ ∆ 1 (C , MI ), hence it is infinite and the meta-instruction MI does not terminate on memory configuration C.

Otherwise, we are in a state (C, MI ) from which the set of variables of tier 1 will never change. If (C, MI ) → + (C , MI ) then this means that the meta-instruction MI contains either a while loop or a recursive call (otherwise the meta-instruction MI cannot be the same). Since while loops and recursive call parameters are of tier 1, by definition of safe programs, this means that they remain unchanged and consequently the meta-instruction MI does not terminate on C.

Lemma 3 permits to demonstrate that the number of distinct tier 1 memory configurations encountered during the evaluation of a terminating and safe program is polynomially bounded in the input size. Indeed, as tier 1 variables cannot grow, they can only refer to some node of the input memory configuration. As the number of such variables is bounded by the program size.

Lemma 4. Given an input C and a meta-instruction MI of a safe program with respect to typing environment ∆, the following holds:

# C ∆ 1 | (C, MI ) → * (C , MI ) ≤ |C| n 1 .
where n 1 is the number of tier 1 variables in the whole program.

Proof. By Lemma 2, there is no information flow from tier 0 to tier 1. Moreover, Rule (New) of Figure 5a Proof. By induction on the intricacy. First, notice that a while loop meta-instruction has an intricacy strictly greater than 0. Now consider a meta-instruction of the shape MI such that ν(MI ) = 1 then we have:

MI = MI 1 while(x){MI } MI 2 ,
for some meta-instructions MI i and MI such that ν(MI i ) ≤ 1 and ν(MI ) = 0, since the while loop cannot be nested. From the semantics, we trivially infer that either the guard x is evaluated to false and we will never encounter this while statement again, either it evaluates to true and the next time the while is encountered, the meta-instruction will be the same. From Lemma 3, we know that if we encounter a meta-instruction twice with configurations that match on tier 1 variables, the meta-instruction does not terminate on said configuration. That means that the while loop can only be executed once per distinct tier 1 configuration, which is bounded by |C| n 1 , by Lemma 4. Now suppose that it holds for a meta-instruction of intricacy k and consider a meta-instruction MI of intricacy k + 1, then clearly MI = MI 1 while(x){MI } MI 2 with ν(MI ) ≥ ν(MI ) + 1. Using the same argument than for the base case, this meta-instruction can be transformed into the following equivalent meta-instruction MI 1 MI . . . MI k times MI 2 for some k such that k ≤ |C| n 1 . By induction hypothesis, any while loop within MI can be executed at most |C| n 1 ×ν(MI ) and, consequently, it can be executed at most k × |C| n 1 ×ν(MI ) ≤ |C| n 1 ×(ν(MI )+1) ≤ |C| n 1 ×ν(MI ) in MI . If MI 1 or MI 2 also has intricacy k + 1, the same argument can be applied. Now we show a bound similar to the bound of Lemma 5 on method calls wrt the level: i.e. the method m is not recursive. Hence, by Lemma 5, each meta-instruction can be executed at most |C| n 1 ×(ν(MI )+1) (The constant 1 comes from the fact that an instruction is executed at least once even if it is not located within a while statement). Consequently, there are at most |MI | × |C| n 1 ×(ν(MI )+1) executed meta-instruction before the program terminates. i.e. k = O(|C| n 1 ×((ν+1)×1) ).

Assume λ(m) = i + 1. Either m is recursive, this means m ∈ [m]. Hence, by safety assumption and by Lemma 4, we know that there are at most |C| n 1 nested recursive calls to m in the evaluation of MI since all the arguments are of tier 1, there is at most one recursive call in the method body (and no while loop) and the meta-instruction terminates. Consequently, the number of meta-instructions unfolded by a method call on m is at most |MI | × |C| n 1 . Consequently, the number of meta-instructions unfolded by method calls of [m] is at most O(|C| n 1 ) (indeed just take the finite sum of |MI | × |C| n 1 , for each method of the equivalence class). In the worst case, all the other meta-instructions correspond to method calls of level i. Applying the induction hypothesis, we know each of these calls will generate at most O(|C| n 1 ×((ν+1)×i) ). Putting all together, it generates at most O(|C|

n 1 × |C| n 1 ×((ν+1)×i) ) = O(|C| n 1 ×((ν+1)×λ(m)) ) meta-instructions.
Or m is not recursive, this means that it may contain while meta-instructions. In the worst case, the calls to methods of level i can be in a while that is nested ν times. This means that the |MI | meta-instructions of level i can be unfolded |C| n 1 ν times from Lemma 4. Since by induction hypothesis, each can yield O(|C| n 1 ×((ν+1)×i) ) meta-instructions, it finally gives O |C| n 1 ×((ν+1)×(i+1)) meta-instructions.

Main results

First, the presented type system allows us to infer polynomial upper bounds on the stack and the heap of safe programs.

Theorem 1. If a core Java program of computational instruction I is safe wrt to typing environment ∆ and terminates on input C then for each memory configuration C and metainstruction MI s.t. (C, I ) → * (C , MI ) we have:

|C | = O(|C| n 1 ((ν+1)λ) ).
In other words, if C = G, P, S, σ then both

|G P | and |S G | are in O(|C| n 1 ((ν+1)λ) ).
Proof. Proposition 1 guarantees that types remain stable under flattening. Safety is also preserved by Remark 1. Moreover, the size of a flattened program remains linear in the size of the initial program, by Lemma 1. Consequently, we can consider the flattened program instead of the initial program. The heap-space upper bound is a consequence of Lemmata 4 and 6 that bound the number of assignments executed in a terminating and safe program. Since each assignment creates a bounded number of new nodes in the graph, we obtain the requested upper bound. The stack upper bound is obtained by Lemma 6 since the maximal size of the stack is bounded by the number of executed push instructions, also bounded by the number of executed instructions (i.e. the reduction depth).

Example 2. Consider the program presented in Section 5. This program is clearly terminating and safe wrt to the provided typing environment. Moreover its maximal intricacy ν is equal to 1 since there is no nested while loops in its methods. Moreover, its maximal level λ is equal to 2 since there is one level of recursion in the method decrement. Consequently, applying Theorem 1, we obtain a O(|C| 4×n 1 ) upper bound on the memory use. Notice that this global upper bound can be improved to obtain a tighter upper bound (at the price of a non-uniform formula) by only considering particular instructions. For example, the instruction IList s 0 = l 1 .sort(); : 0 will have a O(|C| 2 ) complexity since there is only one tier 1 variable l, ν(sort) = 1 and λ(sort) = 1. The instruction i3 1 .decrement(); : 1 will have a linear complexity since there is only one tier 1 variable i3, one recursive call and ν(decrement) = 0.

As a corollary, if the program terminates on all input configurations, then we may infer a polynomial time upper bound on its execution time.

Corollary 1. If a core Java program of computational instruction I is safe wrt to typing environment ∆ and terminates on input C then it does terminate in time O(|C| n 1 ((ν+1)λ) ).

Another corollary of interest is that tier 1 variables remain polynomially bounded even if the program does not terminate. This is particularly interesting in the sense that we can guarantee security properties on the data stored in such variables even if we are unable to prove program termination. where |C (x)| denotes the size of the subgraph of nodes reachable from node C (x) whenever x is of reference type.

Another direct result is that our characterization is complete with respect to the class of functions computable in polynomial time as a direct consequence of Marion's result [START_REF] Marion | A type system for complexity flow analysis[END_REF] since both our language and type system can be viewed as an extension of the considered imperative language. This means that our type system has a good expressivity. Finally, we show the decidability of type inference: Proposition 2 (Type inference). Deciding if there exists a typing environment ∆ such that typing rules are satisfied can be done in time linear in the size of the program.

Proof. Types can be checked in linear time in the size of the program as typing mainly consists in checking type annotations with respect to method signatures, operator signatures and fields declarations. We encode the tier of each field x within the method m of class C by a boolean variable x m C that will be true if the variable is of tier 1, false if it is of tier 0 in the context of m C . All local variables and parameters can be encoded by a single variable as their tier is independent from the context. Each instruction generates some constraints. For example, in the case of an assignment x := y; in the context m C , we have to check π 2 (∆(m C )(x)) π 2 (∆(m C )(y))), which can be represented as (y m C ∨ ¬x m C ). All these constraints generate a conjunction of such clauses which are in number linear in the size of the program. As a result, the type inference problem is reduced to 2-SAT and can be solved in linear time.

Extensions

Control flow alteration

Constructs altering the control flow like break, return and continue can also be considered in our fragment. For example, a break statement has to be constrained to be of tier 1 so that if such an instruction is to be executed, then we know that it does not depend on tier 0 expressions. More precisely, it can be typed by the rule:

(Break) Γ break; : void [START_REF] Albert | Costa: Design and implementation of a cost and termination analyzer for java bytecode[END_REF] This prevent the programmer from writing conditionals of the shape: Using the same kind of typing rule, return statements can also be used in a more flexible manner by allowing the execution to leave the current subroutine anywhere in the method body.

Inheritance

Inheritance is a major trait of OOP that has to be treated by any reasonable static analysis tool on Java like programs. In this subsection, we present an extension of the language with inheritance and provide some adjustments needed in our analysis in order to preserve the stack and heap-space upper bounds of Theorem 1. Syntax. We extend the class grammar by class declarations of the shape: Semantics. The semantics can be extended by creating a new node of label D in the graph each time a new D(. . .) expression is evaluated. The only difficulty to face is the semantics of method calls. As in Java, the method to be executed can only be chosen dynamically as it can be overridden in the subclass to which the object belongs. Consequently, a check on the current object type has to be done before evaluating the method call. Once the type D is known the evaluation searches for the method signature in the corresponding class and evaluates its body once found. In the particular case where this signature does not exist, the search is extended to the super class C and, so on. Type system. The corresponding type system has to be extended in two ways. First, it must allow polymorphism but must also keep the tiers unchanged to prevent information flows. This can be done by adding the following rule:

Γ E : D(α) D C (Pol) Γ E : C(α)
Second, it must check the tiered types of overridden methods in such a way that they are at least as liberal on their arguments tiers and as constrained on the output tier:

∀i, β i α i α β D C Γ τ M C : τ 1 (α 1 ) × • • • × τ n (α n ) → τ (α) (OverR) Γ τ M D : τ 1 (β 1 ) × • • • × τ n (β n ) → τ (β)
provided that M D overrides M C . Finally, the constructor of the subclass has to follow a similar rule on its inherited fields. Safety. Now a method call can be evaluated dynamically depending on the current object type. It can lead to the creation of unexpected recursive calls. Hence the safety notion has to be changed in order to capture this behavior. For that purpose, it just suffices to extend the notion of recursive method signature by the following rule: τ m C (τ 1 , . . . , τ n ) τ m D (τ 1 , . . . , τ n ), if D C i.e. m C is considered to call its override m D by dynamic binding.

Conclusion

This work presents a simple but highly expressive type-system that can be checked in linear time and that provides explicit polynomial upper bounds on the heap and stack size of an object oriented program allowing (recursive) method calls. As the system is purely static, the bounds are not as tight as may be desirable. It would indeed be possible to refine the framework to obtain a better exponent at the price of a non-uniform formula (for example not considering all tier 1 variables but only those modified in each while loop or recursive method would reduce the computed complexity. See Example 2). OO features, such as abstract classes, interfaces and static fields and methods, were not considered here, but we claim that they can be treated by our analysis. Finally, notice that the safety condition can be alleviated by ensuring that only one recursive call is reachable in the execution of the method body thus improving expressivity.

Figure 2 :

 2 Figure 2: Example of a pointer graph

Figure 3 :

 3 Figure 3: Instruction flattening

Figure 4 :Lemma 1 .

 41 Figure 4: Semantics of core Java

  {σ, P, S}, be a notation for the memory configuration C that is equal to C but on µ where C (x) = v. Moreover let C[S : push(P)] and C[S : pop] be notations for the memory configuration where the pointer mapping P has been pushed to the top of the stack and where the top pointer mapping has been removed from the top of the stack, respectively. Finally, let C[V : v → C] denote a memory configuration C whose graph contains the new node v labeled by C (i.e. l(v) = C) and let C[A : (v, w) → x] denote a memory configuration C whose graph contains the new arrow (v, w) labeled by x (i.e. i((v, w)) = x. We define dom(C) = dom(P) dom( S) dom(σ) (the domains are clearly disjoint by well-formedness) and op to be the function computed by the language implementation of operator op.

Definition 6 (

 6 Well-typed program). Given a program of executable Exe and a contextual typing environment Γ = ( , ∆), the judgment Γ Exe : means that the program is well-typed wrt Γ and is defined in rule (Main) of Figure5c.

1 x 1 := E 1 ;Figure 5 :

 1115 Figure 5: Type system for core Java

18 B

 18 L i s t double ( ) { 19 B L i s t n 0 = new B L i s t ( f a l s e , t h i s ) ; 20 return n 0 ; 21 }

  22 void decrement ( ) { 23 i f ( v a l u e 1 == true o r v a l u e 1 == null ) { 24 v a l u e 1 = f a l s e ; : 1 25 } e l s e { 26 i f ( queue 1 != null ) { 27 v a l u e = true ; 28 queue 1 . decrement ( ) ; : 1 29 } e l s e { 30 v a l u e 1 = f a l s e ; :

Lemma 3 .

 3 Given a memory configuration C and a meta-instruction MI of a safe program with respect to typing environment ∆, if (C, MI ) → + (C , MI ) and C ∆ 1 = C ∆ 1 , then the meta-instruction MI does not terminate on memory configuration C.

Lemma 5 .

 5 enforces that tier 1 expressions cannot correspond to the creation of a new instance. Indeed in an assignment of the shape x:=new C(y 1 , . . . , y n ), the judgment Γ new C(y 1 , . . . , y n ) : C(0) holds and, consequently, the judgment Γ x : C(1) cannot hold because of Rule (Ass). Consequently, variables of tiered type C(1) may only point to nodes of the initial pointer graph corresponding to input C. The number of such nodes is bounded by |C|. A boolean variable x of tier 1 has only two possible distinct values and clearly 2 ≤ |C|, since the graph of C has at least one node (the null reference) and x is in the domain of the primitive store of C. The number of tier 1 variables being at most n 1 = δ 1 ∈∆ 1 #dom(δ 1 ), by definition of ∆ 1 , the number of distinct configurations is bounded by |C| n 1 .It follows from Lemma 4 that the while loops of a safe and terminating program are polynomial time instructions. Given a meta-instruction MI of a safe program with respect to typing environment ∆ such that MI terminates on input C. Each while loop in MI can be executed at most |C| n 1 ×ν(MI ) times.

Lemma 6 .

 6 Given a meta-instruction MI = [[τ ]x:=]y.m(y 1 , . . . , y n ); of a safe program with respect to typing environment ∆. If (C, MI ) → k (C , ) (i.e. MI terminates on input C in k steps) then k = O(|C| n 1 ×(ν+1)×λ(m) ). Proof. By induction on the level. Consider a method of the shape: τ m(. . .){MI [return z; ]}. If λ(m) = 1. By definition of the level, this means m / ∈ [m],

Corollary 2 .

 2 If a core Java program of computational instruction I is safe wrt to typing environment ∆ then, on input C, for each memory configuration C , meta-instruction MI s.t. (C, MI ) → * (C , MI ) and a local variable x of tier 1 we have: |C (x)| = O(|C| n 1 ((ν+1)λ) ).

D

  extends C{τ 1 x 1 ; . . . ; τ n x n ; K D M 1 D . . . M k D } with D ∈ C and K D being a constructor initializing both the fields of C and the fields of D. As in Java multiple inheritance is prohibited. Inheritance defines a partial order on classes denoted by D C. Considering this extended syntax makes method overriding, subtyping and polymorphism possible.

  The set of base types T is defined to be the set including a reference type C for each class name C, the special type void and the primitive type boolean. In other words, T = {void, boolean} ∪ C.Tiers are two elements of the lattice ({0, 1}, ∨, ∧) where ∧ and ∨ are the greatest lower bound operator and the least upper bound operator, respectively. The induced order, denoted , is such that 0 1. In what follows, let α, β, . . . denote tiers in {0, 1}. Let the minimum ∧ i∈S α i of a finite set of tiers {α i | i ∈ S}, indexed by the finite set S, be defined in a standard way (setting ∧

	4 Type system
	4.1 Tiered types
	i∈∅

  In the concat method, the presence of the method call o.getQueue() in the guard of the while loop enforces its ouput tier to be 1 by rules (Wh), (Null) and (Op). Consequently, the type of getQueue has to be BList(1) → BList(1) under the considered contextual typing environment (see the admissible types of getQueue). It also enforces the object o to be of tier 1. Consequently, the current object this is also enforced to be of tier 1 by rule (Ass) and the tier of the parameter other is enforced to be 1 (see the setQueue admissible types). Consequently, the only admissible type for concat is BList(1) × BList(1) → void(1), using rule (Seq).

	62		b2 1 != null ) {
	63		i f ( ! b1 . g e t V a l u e ( ) &&
	64		b2 . g e t V a l u e ( ) ) {
	65		r e s = true ;
	66 35 67 36 68 37 69 38 70 39 71 40 72 73	}	} e l s e { ; } i f ( b1 . g e t V a l u e ( ) && 1 ) { B L i s t o 1 = t h i s 1 ; : 1 ! b2 . g e t V a l u e ( ) ) { while ( o 1 . getQueue ( ) != null ) { r e s = f a l s e ; o 1 = o 1 . getQueue ( ) ; : 1 } e l s e { ; } } i f ( b1 . getQueue ( ) == null && o 1 . setQueue ( o t h e r 1 ) ; : 1 b2 . getQueue ( ) != null ) { r e s = true ;
	74		} e l s e { ; }
	75		i f ( b2 . getQueue ( ) == null &&
	76		b1 . getQueue ( ) != null ) {
	77		r e s = f a l s e ;
	78		} e l s e { ; }
	79		b1 = b1 . getQueue ( ) ;
	80		b2 = b2 . getQueue ( ) ;
	81		}
	82		return r e s 1 ;
	83	}
	84 }

It could be extended to other primitive data types as explained in Subsection 4.4.1.

For simplicity, each operator is supposed to have a single signature. This is a slight distinction with Java to simplify our treatment. Notice however that multiple signatures could be handled by the complexity analysis.

This is also a minor distinction with Java, where an assignment has return type of the evaluated expression, used in order to simplify the type system.

As usual, we assume that max ∅ = 0

boolean i s E q u a l ( B L i s t o t h e r 1 ) { 42 boolean r e s 0 = true ; : 1 // u s i n g ( Sub ) 43 B L i s t b1 1 = t h i s 1 ; : 1 44 B L i s t b2 1 = o t h e r 1 ; : 1 45 while ( b1 1 != null && b2 1 != null ) { 46 i f ( b1 1 . g e t V a l u e ( ) ! = b2 1 . g e t V a l u e ( ) ) { 47 r e s 0 = f a l s e ; : 1 // u s i n g ( Sub ) 48 } e l s e { ; } 49 b1 1 = b1 1 . getQueue ( ) ; : 1 50 b2 1 = b2 1 . getQueue ( ) ; :

r e s 0 =f a l s e ; : 1 // u s i n g ( Sub ) 54 } e l s e { ; } : 1 // u s i n g ( Sub ) 55 return r e s 0 ; 56 }

The local variables b1 and b2 are enforced to be of tier 1 by rule (Wh). Consequently, this and other are also of tier 1 using twice rule (Ass). Moreover, the methods getValue and getQueue will be typed by BList(1) → boolean(1) and BList(1) → BList(1), respectively. Finally, the local variable can be given type boolean [START_REF] Albert | Costa: Design and implementation of a cost and termination analyzer for java bytecode[END_REF] or boolean(0) (in the latter case, the subtyping rule (Sub) will be needed) and, consequently, the admissible types for isEqual are BList( Search f o r a f a l s e i n t h e i n p u t . copy 1 = i n p u t 1 ; while ( copy 1 . getData ( ) != f a l s e ) { copy 1 = copy 1 . getNext ( ) ; } }

The main program can be typed by the above annotations. It is obvious that if the main program halts, it will do so in time linear in the size of the input. But it can loop infinitely if the ring does not contain any false.

6 Upper bound on the stack size and the heap size

In this section, we state our main result showing that well-typed programs have both pointer stack size and pointer graph size bounded polynomially by the input size under termination and safety assumptions. Moreover, precise upper bounds can be extracted.

Size, level and intricacy

For that purpose, we need to define the notion of size for pointer stack, pointer graph and memory configuration.

Definition 7 (Sizes).

• The size of a pointer graph G P is defined to be the number of nodes in G and denoted |G P |.