日本ソフトウェア科学会第 33 回大会 (2016 年度) 講演論文集

An Extended Behavioral Type System
for Memory-Leak Freedom
Qi TanKohei Suenaga

Atsushi Igarashi

In the previous work, we proposed a behavioral type system for a programming language with dynamic
memory allocation and deallocation. The behavioral type system, which uses sequential processes as types
where each action is related to an allocation and a deallocation, can estimate an upper bound of memory
consumption of a program. However, the previous type system did not deal with path-sensitivity, which
results in an imprecise abstraction even for a simple program. In order to address this problem, we propose
an extension of the previous type system with path-sensitive behavioral types. Our extended type system
can capture path-sensitive behavior of a program, which enables more precise analysis of the behavior of aprogram.

opment. Much eﬀort has been paid to powerful

1 Introductionand eﬃcient static analysis of a program with man-Several programming languages, such as the C

ual memory management [3, 11–14, 16] and devel-

language, allow very flexible memory management

opment of practical static analyzer such as Infer

by providing manual memory management primi-(http://fbinfer.com/).

tives (e.g. malloc and free in the C language).

We are interested in statically estimating an up-

One can write a program that dynamically allocatesper bound of memory consumption of a programand deallocates a memory cell during execution.

with manual memory management. We are espe-

However, manual memory management primi-

cially interested in the upper-bound analysis of atives often cause hard-to-find bugs. One can write

potentially nonterminating program such as Web

a program that deallocates a memory cell twice, aservers and operating systems. Such information

program that forgets to deallocate a memory cell,

about an upper bound of memory consumption isand a program that accesses to a memory cell that

useful as a certificate of memory-leak freedom ofis already deallocated. These bugs in manual mem-these important software.

ory management often leads to a serious security
problem.

As a first step to this goal, in the previous work,
we proposed a behavioral type system for imperative

Using a static analysis is one of the approaches

programs with manual memory management [15].

to detecting such bugs at the early stage of devel-

In order to show how our previous type system

An Extended Behavioral Type System for MemoryLeak Freedom.
Qi Tan, Kohei Suenaga and Atsushi Igarashi, Kyoto
University.
This is an unrefereed paper. Copyrights belong to the
Author(s).

works, consider the following C function h1.
void h1() {int *x, *y;x = malloc(sizeof(int));y = malloc(sizeof(int));

free(x); free(y);∗x is NULL and P2 if ∗x is not NULL. By using pathsensitive behavioral types, the type of h2 can be}
By using our previous type system, we can infer

expressed by (∗x)(malloc, 0); (∗x)(free, 0). With

that this function behaves according to a behavioral

the knowledge that the value of ∗x does not change

type malloc; malloc; free; free that expresses thatthroughout this function, which is expressed by an-

this function performs allocation twice and thenother constructor of a behavioral type introduced

deallocation twice. By inspecting this behavioral

later, we can conclude that the behavior of h2 istype, we can obtain information on how much mem-(malloc; free) + 0.

ory this program may consume at most. Our pre-In this paper, we define the syntax and thevious type system can also deal with more complex

semantics of the behavioral types extended with

control statement and recursive function calls.

path-sensitive ones, extend the typing rules. We

One problem in the previous type system consists

also discuss how the type inferred by the type sys-

in how we analyze a branch statement. Consider

tem can be used to estimate an upper bound of athe following function h2.

program. Although the soundness of the type sys-

void h2(int *x) {tem is still a conjecture, we expect our extension is

int *y;an important steppingstone for behavior analysis ofif (x == NULL) { /* (A) */a program with manual memory management.

y = malloc(sizeof(int));

The rest of this paper is structured as follows.

}

Section 2 describes an imperative language with al-if (x == NULL) { /* (B) */location and deallocation primitives and its opera-

free(y);}}This function contains two sequentially executed

tional semantics. Section 3 introduces the extended
behavioral type system with path-sensitive behavioral types. Section 4 discusses the related work.
Section 5 concludes this paper.

branch statements. Our previous type system infers (malloc + 0); (free + 0) as a behavioral type2 Language Lof h2 ignoring the guard conditions. The symbol +This section defines an imperative language L

in the behavioral type represents a nondeterminis-

with memory allocation and deallocation primi-

tic choice. Therefore, this type expresses that thistives.

function may or may not perform an allocation, andIn the rest of this paper, we write ⃗x for a finite se-then may or may not perform a deallocation. We

quence x1 , . . . , xn ; we assume that each element isdistinct. We write [x⃗′ /⃗x]s for the term obtained bycannot exclude the possibility that h2 allocates amemory cell once without a deallocation from thisinferred type. However, since the guard (A) holds if
and only if (B), this program actually performs anallocation and a deallocation sequentially or doesnothing.
The current paper tries to address this problem by introducing a path-sensitive behavioral type(∗x)(P1 , P2 ). This type expresses a behavior P1 if

replacing each free occurrence of ⃗x in s with variables x⃗′ . We write Dom(f ) for the partial function
f . We write f {x 7→ v}and f \x as follows.
 v
if x = w
f {x 7→ v}(w) = f (w) otherwise.
 undefined if x = w(f \x)(w) = f (w)otherwise.

x, y, z, . . . (variables)∈Vars (statements)::=

skip | s1 ; s2 | ∗x ← y | free(x)|let x = malloc()in s | let x = null in s|

let x = y in s | let x = ∗y in s|

ifnull (∗x) then s1 else s2 | f (⃗x)|

const(∗x)s | endconst(∗x)

d (proc. defs.)::={f 7→ (x1 , . . . , xn )s}

D (definitions)::=⟨d1 ∪ · · · ∪ dn ⟩P (programs)::=⟨D, s⟩

図1

Syntax of L.

A procedure definition f 7→ (x1 , . . . , xn )s defines

2. 1 Syntax
The syntax of the language L is defined by thea procedure f that takes x1 , . . . , xn as arguments

BNF in Figure 1. For simplicity, a value of ourand executes s. We use metavariable D for a set of

language is either a pointer or null. The Var isprocedure definitions. A program is a pair ⟨D, s⟩,a countably infinite set of variables. The state-

where D is the set of the procedure definitions thatment skip is a do-nothing statement. The state-

may be used in the execution of the main statement

ment s1 ; s2 is a sequential execution of s1 and s2 .

s.

The statement ∗x ← y changes the content of cellwhich is pointed to by x to the value y. The state-

2. 2 Operational semantics

ment free(x) deallocates a memory cell pointed toDefinition 1. A fact c is defined by the following

by the pointer x. The statement let x = e in s

BNF:

evaluates the expression e, binds x to the result,and executes s. The expression malloc() allocatesc ::= const(∗x) | null(∗x) | ¬null(∗x).
We use C for a multiset of facts.

a new memory cell. We assume that the size of ev-

A fact is used in the semantics to keep track of

ery memory cell is identical. The expression null

the information about constantness and nullness.

evaluates to the null pointer. The expression ∗y

The fact const(∗x) represents that ∗x is declaredevaluates to the content of the memory cell pointed

to be currently constant by a constantness annota-

to by y. The statement ifnull (∗x) then s1 else s2tion; null(∗x) and ¬null(∗x) represents that ∗x is

executes s1 if ∗x is null and executes s2 otherwise.

equal to null and not equal to null respectively.

The statement f (⃗x) executes the procedure f withFor definition of the operational semantics,

arguments ⃗x. The statement const(∗x)s is a con-

we designate a countable infinite set H ofstantness annotation. By writing this annotation,

heap addresses ranged over by l. A configurationa programmer declares that the value of ∗x does

is of the form ⟨H, R, s, n, C⟩. Each elements in the

not change during the execution of s. The state-configuration is as follows:

ment endconst(∗x) is a marker for the end of a

• H, a heap, is a finite mapping from H toconstantness annotation, which is used only in a

H ∪ {null} representing the state of memory,

runtime state.

• R, an environment, is a finite mapping from

Var to H∪{null} representing the value boundobtained by removing one const(∗x) from C. (Re-to each variable,

call that C is a multiset of facts.) If C ′ does not• s is the statement that is being executed,

contain const(∗x), then it deletes all the facts re-• n is the number of the memory cells available

lated to ∗x. Otherwise, it returns C ′ .

for allocation, andWe explain the rules related to path sensitiv-• C is a multiset of facts that holds at the current configuration.

ity and the constantness annotations; for the otherrules, see [15].

The operational semantics of the language• Sem-ConstSeq: The end of the const block

L is given by a labeled transition relation

is marked at the end of the current continua-

ρ

′

′

′

′

′

⟨H, R, s, n, C⟩ −→D ⟨H , R , s , n , C ⟩ where ρ istion. The fact const(∗x) is also added to C toa label defined by the BNF ρ ::= malloc | free |record that ∗x is declared to be constant untilnull(∗x) | ¬null(∗x) | τ . The label malloc ex-

endconst(∗x) is encountered.

presses an allocation of a new memory cell. The la-• Sem-Assign and Sem-ConstAssignExn: Thesebel free expresses a deallocation of a memory cell.

rules handle assignment statements. If con-

The label null(∗x) expresses making an assump-

stantness of ∗z is declared (i.e., const(∗z) ∈tion that ∗x is a null pointer; the label ¬null(∗x)C), then a write operation to ∗z leads to an

expresses not.

The label τ expresses an action

exception ConstEx. This exception is raised

other than the above; we often omit τ in the re-if a constantness annotation provided by a pro-τ

lation −→D . The metavariable σ is used for a fiρ1 ...ρnnite sequence of actions ρ1 . . . ρn . The −−−−−→D
ρ1

ρ2

ρn

ρ

is short for −→D −→D . . . −−→D . We write =⇒Dρ ...ρnρ1ρ
for −→∗D −→D −→∗D . We write ==1===⇒D for =⇒
D
ρn
... =
=⇒D .
ρ
The relation −→D is the least relation that sat-grammer is wrong.

The type system intro-

duced later does not guarantee unreachability
to this exceptional state.
• Sem-IfNullT, Sem-IfNullF, Sem-IfConstNullT,and Sem-IfConstNullF: These rules handle
an if -statements depending on whether ∗x is

isfies the rules in Figure 2. The operational seman-null or not.

tics is, except for the multiset of facts C, almost thebranch is taken to the multiset of facts C only

same as the previous framework [15]. Important in-

if C contains const(∗x). Otherwise, even if

variants of a configuration is that (1) if C contains

the semantics recorded null(∗x) or ¬null(∗x)

const(∗x), then the value of the expression ∗x is

to C, it may not be reliable in the sense of the

not changed in the next step and (2) if C contains

invariant (2) above since the value of ∗x maynull(∗x) (resp., ¬null(∗x)), then the value of ∗x is

be changed by an assignment via an alias of x.

equal to null (resp., not equal to null).

The semantics records which• Sem-ConstSkip: By using the function filter

In order to manipulate the C part of a configu-

above, this rule removes one endconst(∗x)

ration, we use a function filter (C, ∗x) in the rules

from C and conducts “garbage collection” offor the operational semantics defined as follows:
filter (C, ∗x) =the facts related to ∗x if necessary.

let C ′ = C − const(∗x) in• Sem-Malloc and Sem-OutOfMem: malloc
allocates a new memory cell by extending theif const(∗x) ∈ C ′ then C ′heap H and decreasing the value of n by 1.

else C ′ \{null(∗x), ¬null(∗x)}.
The function filter (C, ∗x) sets C ′ to the multiset

If there is no available cell (i.e., n = 0), thenmalloc raises OutOfMemory exception.

⟨H, R, skip; s, n, C⟩ −→D ⟨H, R, s, n, C⟩(Sem-Skip)ρ⟨H, R, s1 , n, C⟩ −→D ⟨H ′ , R′ , s′1 , n′ , C ′ ⟩ρ
⟨H, R, s1 ; s2 , n, C⟩ −→D ⟨H ′ , R′ , s′1 ; s2 , n′ , C ′ ⟩x′ ∈/ Dom(R)(Sem-Seq)⟨H, R, let x = null in s, n, C⟩ −→D ⟨H, R {x′ 7→ null} , [x′ /x] s, n, C⟩(Sem-LetNull)x′ ∈/ Dom(R)⟨H, R, let x = y in s, n, C⟩ −→D ⟨H, R {x′ 7→ R(y)} , [x′ /x] s, n, C⟩(Sem-LetEq)⟨H, R, const(∗x)s, n, C⟩ →D ⟨H, R, s; endconst(∗x), n, C + const(∗x)⟩(Sem-ConstSeq)

C ′ = filter (C, ∗x)(Sem-ConstSkip)⟨H, R, endconst(∗x), n, C⟩ →D ⟨H, R, skip, n, C ′ ⟩∀z.R(x) = R(z) =⇒ const(z) ∈/C(Sem-Assign)⟨H{R(x) 7→ v}, R, ∗x ← y, n, C⟩ −→D ⟨H {R(x) 7→ R(y)} , R, skip, n, C⟩
const(∗x) ∈/C

H(R(x)) = null(Sem-IfNullT)null(∗x)⟨H, R, ifnull (∗x) then s1 else s2 , n, C⟩ −−−−−−→D ⟨H, R, s1 , n, C⟩
H(R(x)) ̸= null

const(∗x) ∈/C(Sem-IfNullF)¬null(∗x)⟨H, R, ifnull (∗x) then s1 else s2 , n, C⟩ −−−−−−−→D ⟨H, R, s2 , n, C⟩
const(∗x) ∈ C

H(R(x)) = null(Sem-IfConstNullT)null(∗x)⟨H, R, ifnull (∗x) then s1 else s2 , n, C⟩ −−−−−−→D ⟨H, R, s1 , n, C + null(∗x)⟩
H(R(x)) ̸= null

const(∗x) ∈ C(Sem-IfConstNullF)¬null(∗x)⟨H, R, ifnull (∗x) then s1 else s2 , n, C⟩ −−−−−−−→D ⟨H, R, s2 , n, C + ¬null(∗x)⟩
x′ ∈/ Dom(R)R(y) ∈ Dom(H)⟨H, R, let x = ∗y in s, n, C⟩ −→D ⟨H, R {x′ 7→ H(R(y))} , [x′ /x] s, n, C⟩(Sem-LetDeref)R(x) ̸= null and R(x) ∈ Dom(H)(Sem-Free)

free⟨H{R(x) 7→ v}, R, free(x), n, C⟩ −−−→D ⟨H\R(x), R, skip, n + 1, C⟩l∈/ Dom(H)n>0malloc⟨H, R, let x = malloc() in s, n, C⟩ −−−−−→D ⟨H {l 7→ v} , R {x′ 7→ l} , [x′ /x] s, n − 1, C⟩(Sem-Malloc)

D(f ) = (⃗y )sR(x) = null or R(x) ∈/ Dom(H)(Sem-FreeExn)⟨H, R, f (⃗x), n, C⟩ −→D ⟨H, R, [⃗x/⃗y ] s, n, C⟩
free⟨H, R, free(x), n, C⟩ −−−→D MemEx(Sem-Call)R(y) = null or R(y) ∈/ Dom(H)R(x) = null or R(x) ∈/ Dom(H)⟨H, R, ∗x ← y, n, C⟩ −→D MemEx(Sem-AssignExn)⟨H, R, let x = ∗y in s, n, C⟩ −→D MemEx(Sem-DerefExn)∃z.const(∗z) ∈ C and R(x) = R(z)⟨H{R(x) 7→ v}, R, ∗x ← y, n, C⟩ −→D ConstEx
malloc⟨H, R, let x = malloc() in s, 0, C⟩ −−−−−→D OutOfMemory
図2• Sem-Free:(Sem-AssignConstExn)(Sem-OutOfMem)

Operational semantics of L.

free(x) removes the entry forR(x) from the heap H and increase the valueof n by 1.
• Sem-AssignExn, Sem-FreeExn and SemDerefExn: If a program tries to access toa deallocated memory cell, then the exception
MemEx is raised.
Definition 2. A program ⟨D, s⟩ is said to execute within n memory cells if ⟨∅, ∅, s, n, ∅⟩ ̸−→∗D
MemEx.

0 | P1 ; P2 | malloc | free | (x)P | (∗x)(P1 , P2 ) | const(∗x)P | endconst(∗x)

P(behavioral types)::=

Γ(variable type environment)::={x1 , x2 , . . . , xn }Ψ(dependent function type)

::=

(⃗x)P

Θ

(function type environment)::={f1 : Ψ1 , . . . , fn : Ψn }| α | µα.P

図3

Syntax of types.

fied by P , which may be dependent to ⃗x. Proce-

3 Type systemdure type environments, ranged over by Θ, assigns

3. 1 Typesa procedure type to a function name.

Figure 3 defines the syntax of types. Behavioral

Figure 4 defines the operational semantics of thetypes, ranged over by P , specify the behavior of

behavioral types. The semantics is defined by astatements. The type 0 represents the do-nothinglabeled transition system over configuration of the

behavior. The type P1 ; P2 is the sequential compo-

shape ⟨P, C⟩. Here, C is the multiset of facts thatsition of P1 and P2 . The types malloc and freehold. We add explanation to important rules.

represents one allocation and one deallocation, re-• Tr-Bind: The behavioral type (x)P picks

The type (x)P is the behavior thatup a fresh name x′ and makes transition tobinds a variable x and behaves as specified by P ;[x′ /x]P . To understand this definition, recall

the type P may be dependent to x. For example,

that the rules in Figure 2 for dealing with state-

the behavior of the statement let x = y in skip isments with a binder (i.e., Sem-LetNull, Sem-

represented by (x)0 since it binds the variable x and

LetEq, Sem-LetDeref, and Sem-Malloc)

spectively.

does nothing. The type (∗x)(P1 , P2 ) is the behavior

generate a fresh variable for the bound variableof a branching statement. This type represents theand add it to the environment R of the con-behavior P1 if ∗x is null; P2 otherwise. The typefiguration. The rule Tr-Bind simulates thisconst(∗x) represents the behavior of a statement

behavior.

that works as specified in P under the assumption• Tr-Const and Tr-EndConst: The behav-that the value of ∗x does not change. The typeioral type const(∗x)P adds the fact const(∗x)

endconst(∗x) represents the behavior that marks

to C and evolves to P ; endconst(∗x).

the end of the constantness annotation. The types

endconst(∗x) is encountered, then all the

α and µα.P allow to specify a recursive behavior.

facts related to ∗x in C is removed by filter .

The type µα.P represents the behavior P , in which

This is parallel to the semantics of const(∗x)s

α represents the behavior of µα.P itself. For ex-

and endconst(∗x) in Figure 2.

If

ample, µα.(malloc; free; α) represents a statement• Tr-ConstNondet1 and Tr-ConstNondet2:

that repeats an allocation followed by a dealloca-

If the fact const(∗x) is a member of C andtion forever. Γ, a type environment, is a set of vari-

there is no null(∗x) nor ¬null(∗x), then theables representing the set of free variables that may

behavioral type (∗x)(P1 , P2 ) nondeterministi-

appear in a statement.

cally chooses P1 or P2 . The fact null(∗x) (resp.

The types for procedures, ranged over by Ψ, is of¬null(∗x)) is added to C if the branch P1 (resp.

the form (⃗x)P . This type represents a procedureP2 ) is taken. This addition of the fact is con-that takes ⃗x as arguments and behaves as speci-

ducted only if const(∗x) is a member of C (cf.,Tr-NoConst1 and Tr-NoConst2).
• Tr-ConstNull and Tr-ConstNotNull: If
const(∗x) is a member of C and if null(∗x)

null(∗x). Another possible transition is⟨P, ∅⟩−→⟨P1 ; P2 ; endconst(∗x), C1 ⟩¬null(∗x)) is a member of C, then−→⟨0; P2 ; endconst(∗x), C1 ∪ C3 ⟩the behavioral type (∗x)(P1 , P2 ) evolves to P1−→⟨P2 ; endconst(∗x), C1 ∪ C3 ⟩(resp. P2 ). This happens only if (1) the behav-−→⟨0; endconst(∗x), C1 ∪ C3 ⟩ioral type (∗x)(P1 , P2 ) was inside the block of−→⟨endconst(∗x), C1 ∪ C3 ⟩(resp.

certain const(∗x){. . . } and (2) there was another (∗x)(P1′ , P2′ ) was in the same block before(∗x)(P1 , P2 ) is reached. Because the transitionof (∗x)(P1′ , P2′ ) should have registered null(∗x)
or ¬null(∗x) to C and both (∗x)(P1′ , P2′ ) and(∗x)(P1 , P2 ) are inside const(∗x){. . . }, it is−→ ⟨0, ∅⟩.
A transition to ⟨free; endconst(∗x), C1 ∪C3 ⟩ is notallowed because C1 ∪ C3 contains const(∗x) and¬null(∗x). Notice that the path-sensitive behavioral
malloctype excludes the possibility of ⟨P, ∅⟩ −−−−→ ⟨0, ∅⟩freeand ⟨P, ∅⟩ −−−→ ⟨0, ∅⟩.

safe to assume that (∗x)(P1 , P2 ) takes the samebranch as (∗x)(P1′ , P2′ ).
• Tr-NoConst1 and Tr-NoConst2: If const(∗x)
is not in the multiset of facts C, then the behavioral type (∗x)(P1 , P2 ) nondeterministically
evolves to P1 or P2 .
Example 3.1. Let P be the behavioral type
const(∗x){(∗x)(malloc, 0); (∗x)(free, 0)}.
We write P1 for (∗x)(malloc, 0), P2 for (∗x)(free, 0),
C1 for {const(∗x)}, C2 for {null(∗x)}, and C3
for {¬null(∗x)}. Then, the following transition sequence is possible.
⟨P, ∅⟩

3. 2 Type judgment
The type judgment for statements is of the form
Θ; Γ ⊢ s : P . The judgment reads “the behavior ofs is P under the function type environment Θ andthe variable type environment Γ”.
We incorporate subtyping to our type system defined as follows.
Definition 3 (Subtyping). C ⊢ P1 ≤ P2 is thelargest relation such that, for any P2′ , C ′ , and ρ, ifρ

⟨P2 , C⟩ −→ ⟨P2′ , C ′ ⟩, then there exists P1′ such thatρ

⟨P1 , C⟩ =⇒ ⟨P1′ , C ′ ⟩ and C ′ ⊢ P1′ ≤ P2′ . We write
P1 ≤ P2 if C ⊢ P1 ≤ P2 for any C.
The type judgment Θ; Γ ⊢ s : P is defined as the−→⟨P1 ; P2 ; endconst(∗x), C1 ⟩−→⟨malloc; P2 ; endconst(∗x), C1 ∪ C2 ⟩least relation that satisfies the rules in Figure 5.

malloc−−−−→⟨P2 ; endconst(∗x), C1 ∪ C2 ⟩We give explanation to several important rules.

−→⟨free; endconst(∗x), C1 ∪ C2 ⟩

free

−
−−
→

⟨endconst(∗x), C1 ∪ C2 ⟩• T-Malloc:
malloc() in

The statement let

x=s performs an allocation once,−→⟨0, ∅⟩.
Notice that, from the underlined configuration, thebinds the variable x, and then executes s. The

transition to ⟨0; endconst(∗x), C1 ∪ C2 ⟩ is not

malloc; (x)P .

allowed because the facts include const(∗x) andbehavior of the whole statement is therefore• T-LetEq: The statement let x = y in s
makes an alias x of y and then executes s.
Therefore, we rename x to y in the behavioral
type P of s.
• T-LetDeref and T-LetNull: The statements let x = ∗y in s and let x = null in s⟨0; P, C⟩ → ⟨P, C⟩(Tr-Skip)ρ⟨P1 , C⟩ −→ ⟨P1′ , C ′ ⟩(Tr-Seq)ρ⟨P1 ; P2 , C⟩ −→ ⟨P1′ ; P2 , C ′ ⟩malloc⟨malloc, C⟩ −−−−−→ ⟨0, C⟩(Tr-Malloc)

free⟨free, C⟩ −−−→ ⟨0, C⟩(Tr-Free)′x is fresh.
(Tr-Bind)⟨(x)P, C⟩ → ⟨[x′ /x]P, C⟩⟨const(∗x)P, C⟩ → ⟨P ; endconst(∗x), C + const(∗x)⟩(Tr-Const)′

C = filter (C, ∗x)(Tr-Endconst)⟨endconst(∗x), C⟩ → ⟨0, C ′ ⟩const(∗x) ∈/C

const(∗x) ∈/C(Tr-NoConst1)

null(∗x)¬null(∗x)⟨(∗x)(P1 , P2 ), C⟩ −−−−−−→ ⟨P2 , C⟩
(Tr-NoConst2)¬null(∗x), const(∗x) ∈ C(Tr-ConstNotNull)⟨(∗x)(P1 , P2 ), C⟩ → ⟨P2 , C⟩⟨(∗x)(P1 , P2 ), C⟩ −−−−−→ ⟨P1 , C⟩null(∗x), const(∗x) ∈ C⟨(∗x)(P1 , P2 ), C⟩ → ⟨P1 , C⟩

(Tr-ConstNull)null(∗x), ¬null(∗x) ∈/C

const(∗x) ∈ C(Tr-ConstNondet1)

null(∗x)⟨(∗x)(P1 , P2 ), C⟩ −−−−−→ ⟨P1 , C + null(∗x)⟩
null(∗x), ¬null(∗x) ∈/C

const(∗x) ∈ C(Tr-ConstNondet2)¬null(∗x)⟨(∗x)(P1 , P2 ), C⟩ −−−−−−→ ⟨P2 , C + ¬null(∗x)⟩⟨µα.P, C⟩ → ⟨[µα.P/α]P, C⟩
図4(Tr-Rec)semantics of behavioral types with dependent types.

bind x and then execute s. Therefore, the type⟨D, s⟩ are also shown in Figure 5. These rules areof the whole statement is (x)P . The type sys-

standard.

tem just ignores that what the variable x isbound to.
• T-IfNull: The statement

3. 3 Type soundness
Although we have not completed the proof con-ifnull (∗x) then s1 else s2

cretely, we conjecture that the following preserva-

branches depending on whether ∗x is null ortion theorem for the judgment Θ; Γ ⊢ s : P holds.

not. This behavior is abstracted by the type

Conjecture 3.1 (Preservation). Suppose that(∗x)(P1 , P2 ).

• ⊢ D : Θ,

• T-Call: If the type of the procedure f is

• Θ; Γ ⊢ s : P ,(⃗x)P , then the type of f (⃗y ) is [⃗y /⃗x]P ; notice• Γ ⊆ Dom(R),that P may depend on the arguments of the• ⟨H, R, s, n, C⟩ −→ ⟨H ′ , R′ , s′ , n′ , C ′ ⟩,procedure.
Typing rules for the declarations D and programs

ρ

Then, there exist Γ′ and P ′ such that• Θ; Γ′ ⊢ s′ : P ′ ,Θ; Γ ⊢ skip : 0(T-Skip)

Θ; Γ, x, y ⊢ ∗x ← y : 0(T-Assign)Θ; Γ ⊢ s1 : P1

Θ; Γ ⊢ s2 : P2

Θ; Γ, x ⊢ free(x) : freeΘ; Γ, x ⊢ s : P(T-Free)Θ; Γ, x, y ⊢ s : P

Θ; Γ ⊢ let x = malloc() in s : malloc; (x)P
(T-Malloc)
Θ; Γ, x, y ⊢ s : P(T-LetDeref)
Θ; Γ, y ⊢ let x = ∗y in s : (x)PΘ; Γ, y ⊢ let x = y in s : [y/x]PΘ; Γ, x ⊢ s : P
Θ; Γ ⊢ let x = null in s : (x)PΘ; Γ, x ⊢ endconst(∗x) : endconst(∗x)(T-Endconst)(T-Const)

Θ; Γ, x ⊢ const(∗x)s : const(∗x)PΘ; Γ, x ⊢ s2 : P2

(T-IfNull)Θ; Γ, x ⊢ ifnull (∗x) then s1 else s2 : (∗x)(P1 , P2 )Θ, f : (⃗x)P ; Γ, ⃗y ⊢ f (⃗y ) : [⃗y /⃗x]PΘ; Γ ⊢ s : P1

(T-LetEq)(T-LetNull)Θ; Γ, x ⊢ s : P

Θ; Γ, x ⊢ s1 : P1

(T-Seq)Θ; Γ ⊢ s1 ; s2 : P1 ; P2

(T-Call)P1 ≤ P2(T-Sub)Θ; Γ ⊢ s : P2
Θ(f ) = (⃗x)P

Θ; x1 , . . . , xn ⊢ s : P for each f 7→ (x1 , . . . , xn )s ∈ D

Dom(D) = Dom(Θ)

⊢ D:Θ
⊢D:Θ

Θ; ∅ ⊢ s : P(T-Program)⊢ ⟨D, s⟩ : P
図5Typing rules.

• Γ′ ⊆ Dom(R′ ),ρ′(T-Def)describes how the inferred type can be used to esti′• ⟨P, C⟩ =⇒ ⟨P , C ⟩.

mate an upper bound of memory consumption. We

The following fact is a corollary of Conjecture 3.1.

first define “memory consumption” of a behavioral

Conjecture

3.2.

If

σ

⊢

⟨D, s⟩

:

P

and

σ

⟨∅, ∅, s, n, ∅⟩ =⇒D , then ⟨P, ∅⟩ =⇒.

type.
Definition

4. We write OKn (P, C) if (1)⟨P, C⟩ −→ ⟨P , C ′ ⟩ implies ♯malloc (σ) − ♯free (σ) ≤σ

3. 4 Verification of memory-leak freedomof a program using the inferred behavioral type′n where ♯ρ (σ) is the number of ρ in σ.
Conjecture 3.3. If• Θ; Γ ⊢ s : P ,Conjecture 3.2 states that the behavior of a pro-• Γ ⊆ Dom(R),gram is soundly abstracted by its type. This section• OK n (P, C), and• n′ ≥ n,tem. We also described how the inferred behavioral′

σ ∗Then, ⟨H, R, s, n , C⟩ ̸=⇒ OutOfMemory.
The conjecture above states that, if ⊢ ⟨D, s⟩ : P

types can be used for estimating an upper boundof memory consumption.

and OK n (P, ∅) hold, then n is an upper bound of

We are currently designing and implementing a

the program. Therefore, by conducting type infer-type inference algorithm for our type system. We

ence to the program, obtaining a type, say, P , andcan infer a type of a program using essentially theestimating an upper bound of P , we can estimate

same algorithm as that of Kobayashi et al. [10]. We

an upper bound of the memory consumption of theneed to check the feasibility of our type system us-

program.

ing practical programs.
The current type system requires a programmer

4 Related Workto write constantness annotation const(∗x). The

Behavioral types are widely used in program

correctness of these annotations are currently the

analysis; a survey of this area can be foundresponsibility of the programmer: If the annotationin [5]. Several representative uses of the behavioral

is wrong, then the type system does not guaran-

types are ensuring correctness of the communica-

tee anything. We suppose that we can verify thetions conducted among several processes [1, 2, 4, 6],

correctness of these annotations using our previous

static deadlock-freedom verification [8,9] and static

work on fractional ownerships [12]. We also expect

correctness verification of resource-usage patterns

that we can automatically insert constantness an-(e.g., a file hanlder is closed before termination) [7,notations using the type inference algorithm of our10]. Our current work also can be seen as a static

previous work.

analysis of resource-usage patterns in which memory is a single and unique resource that is accessed

参 考 文 献via the primitives malloc and free.

[ 1 ] Caires, L. and Vieira, H. T.: Conversation types,
Theor. Comput. Sci., Vol. 411, No. 51-52(2010),
pp. 4399–4440.
[ 2 ] Deniélou, P., Yoshida, N., Bejleri, A., and
Hu, R.: Parameterised Multiparty Session Types,
Logical Methods in Computer Science, Vol. 8,
No. 4(2012).
[ 3 ] Heine, D. L. and Lam, M. S.: A practical flowsensitive and context-sensitive C and C++ memory leak detector, PLDI, Cytron, R. and Gupta,
R.(eds.), ACM, 2003, pp. 168–181.
[ 4 ] Honda, K., Yoshida, N., and Carbone, M.:
Multiparty asynchronous session types, Proceedingsof the 35th ACM SIGPLAN-SIGACT Symposiumon Principles of Programming Languages, POPL
2008, San Francisco, California, USA, January 712, 2008, 2008, pp. 273–284.
[ 5 ] Hüttel, H., Lanese, I., Vasconcelos, V. T.,
Caires, L., Carbone, M., Deniélou, P., Mostrous,D., Padovani, L., Ravara, A., Tuosto, E., Vieira,
H. T., and Zavattaro, G.: Foundations of Session
Types and Behavioural Contracts, ACM Comput.
Surv., Vol. 49, No. 1(2016), pp. 3.
[ 6 ] Igarashi, A. and Kobayashi, N.: A generic typesystem for the Pi-calculus, Theor. Comput. Sci.,
Vol. 311, No. 1-3(2004), pp. 121–163.

Static verification of memory-leak freedom has
been another interesting topic of program verification [3, 11–14, 16]. The main interest of the previous work is guaranteeing the following property:
A pointer to every allocated memory cell will bepassed to free eventually. Our work focuses on
the sequence of malloc and free that may be conducted by a program, forgetting about which freedeallocates which memory cell.

5 Conclusion
We presented a path-sensitive behavioral typesystem for an imperative language with manual
memory management. Our type system abstracts
the behavior of a program concerning the primitives
malloc and free for manual memory management.
We stated several conjectures about the type sys-[ 7 ] Igarashi, A. and Kobayashi, N.: Resource usage analysis, ACM Trans. Program. Lang. Syst.,
Vol. 27, No. 2(2005), pp. 264–313.
[ 8 ] Kobayashi, N.: Type-based information flow
analysis for the pi-calculus, Acta Inf., Vol. 42, No. 45(2005), pp. 291–347.
[ 9 ] Kobayashi, N.: A New Type System for
Deadlock-Free Processes, CONCUR 2006 - Concurrency Theory, 17th International Conference,
CONCUR 2006, Bonn, Germany, August 27-30,
2006, Proceedings, 2006, pp. 233–247.
[10] Kobayashi, N., Suenaga, K., and Wischik, L.:
Resource Usage Analysis for the π-Calculus, Logical
Methods in Computer Science, Vol. 2, No. 3(2006).
[11] Orlovich, M. and Rugina, R.: Memory Leak
Analysis by Contradiction, Static Analysis, 13th International Symposium, SAS 2006, Seoul, Korea,
August 29-31, 2006, Proceedings, 2006, pp. 405–424.
[12] Suenaga, K. and Kobayashi, N.: Fractional

Ownerships for Safe Memory Deallocation, APLAS,
Hu, Z.(ed.), Lecture Notes in Computer Science,Vol. 5904, Springer, 2009, pp. 128–143.
[13] Sui, Y., Ye, D., and Xue, J.: Static memory
leak detection using full-sparse value-flow analysis,
International Symposium on Software Testing andAnalysis, ISSTA 2012, Minneapolis, MN, USA,
July 15-20, 2012, 2012, pp. 254–264.
[14] Swamy, N., Hicks, M. W., Morrisett, G., Grossman, D., and Jim, T.: Safe manual memory
management in Cyclone, Sci. Comput. Program.,Vol. 62, No. 2(2006), pp. 122–144.
[15] Tan, Q., Suenaga, K., and Igarashi, A.: A Behavioral Type System for Memory-Leak Freedom,
Proceedings of PPL 2015, March 2015. http://www.
fos.kuis.kyoto-u.ac.jp/~tanki/memoryleak.pdf.
[16] Xie, Y. and Aiken, A.: Context- and pathsensitive memory leak detection, ESEC/SIGSOFT
FSE, Wermelinger, M. and Gall, H.(eds.), ACM,
2005, pp. 115–125.