# Parametric Denotational Semantics for Extensible Language Definition and
Program Analysis

In-Ho Yi
Department of Computing and Information Systems
The University of Melbourne, Victoria 3010, Australia
<EMAIL_ADDRESS>
(25th October 2012)

###### Abstract

We present a novel approach to construction of a formal semantics for a
programming language. Our approach, using a parametric denotational semantics,
allows the semantics to be easily extended to support new language features,
and abstracted to define program analyses. We apply this in analysing a duck-
typed, reflective, curried dynamic language. The benefits of this approach
include its terseness and modularity, and the ease with which one can
gradually build language features and analyses on top of a previous
incarnation of a semantics.

###### Contents

  1. 1 Introduction
  2. 2 Related work
  3. 3 Overview
  4. 4 Analytic framework
  5. 5 Semantic functions
  6. 6 The language under study
    1. 6.1 The procedural core language
      1. 6.1.1 Concrete interpretation
      2. 6.1.2 Abstract interpretation
    2. 6.2 Function currying
      1. 6.2.1 Concrete interpretation
      2. 6.2.2 Abstract interpretation
    3. 6.3 Object oriented features
      1. 6.3.1 Concrete interpretation
      2. 6.3.2 Abstract interpretation
    4. 6.4 Exception handling
      1. 6.4.1 Concrete interpretation
      2. 6.4.2 Abstract interpretation
  7. 7 Well-definedness
  8. 8 Correctness
    1. 8.1 Definition of correct abstraction
    2. 8.2 Morphism
  9. 9 Conclusion and future direction
  10. A Haskell Implementation
    1. A.1 Syntax parser
    2. A.2 Semantic functions
    3. A.3 Concrete interpretation
    4. A.4 Abstract interpretation

##  1 Introduction

Programming language semantics is a sub-field within theoretical computer
science where researchers develop formal descriptions for the meaning of
computer programs. Over the years, we have seen the development of
denotational semantics, where we mathematically model the effect of an
execution of a language construct. Operational semantics formalise mechanical
steps that transform program states given a particular program. As we shall
argue in this thesis, the challenge of analysing dynamic languages, in both
concrete and abstract manner, necessitates a semantics that bridges the gap
between the two different semantics in order for such task to be feasible.

Abstract interpretation is a unifying theory for program analysis and
verification with which we ascertain run-time properties of a program by
approximating its semantics. The properties of interest are almost always
undecidable. The task of abstraction interpretation can be thought of as over-
approximating a set of concrete states in a finite number of steps. The usual
semantic domain is replaced by an _abstract_ domain whose elements describe a
set of run-time states. Mathematically, such an abstract domain is a partially
ordered set (forming a lattice), the ordering corresponding to subset ordering
of the powerset of concrete states.

Two distinct needs motivated the development of the present work. First, there
is the theoretician’s need for a simple, concise, elegant way of presenting a
formal semantics for a programming language and of developing that into
various static analyses. We base our approach on a parametric denotational
semantics that is modularised to allow the concrete semantics and the abstract
interpretation to share a common framework that uniformly handles most aspects
of the programming language. Use of denotational semantics provides a strong
foundation in proving correctness of an abstract interpretation, and allows us
to focus on algorithmic details of analysis.

Second, there is a practical need for program analyses suitable for the
dynamic languages that have been growing in popularity in recent years.
Traditionally these languages were called “scripting” languages, as they were
mainly used for automating tasks and processing strings. However, with the
advent of web applications, languages such as Perl and PHP gained popularity
as languages for web application development. On the client side, web pages
make heavy use of JavaScript, a dynamically typed language, to deliver dynamic
contents to the browser. Recent years have seen an increasing use of
JavaScript on the server side, as well.

What these languages provide is an ability to rapidly prototype and validate
application models in a real time read-eval-print loop. Another strength comes
from the fact that programmers do not need to have a class structure defined
upfront. Rather, class structures and types of variables in general are
dynamically built. This reduces the initial overhead of software design.

However, these features come at a cost. The lack of a formal, static
definition of type information makes dynamically typed languages harder to
analyse. This difficulty causes several practical problems.

  * •

As applications become more mature, more effort is devoted to program unit
testing and writing assertions to ensure type safety of systems. This extra
effort can sometimes outweigh the benefit of having a dynamically typed
language.

  * •

Whereas programmers using statically typed languages enjoy an abundance of
development tools, the choice of tools for development in dynamically typed
languages is limited, and the tools that do exist lack much of the power of
the tools for statically typed languages, owing largely to the difficulty or
infeasibility of type analysis for such languages.

  * •

Lack of static type structure has a significant impact on the performance of
dynamically typed languages.

With these problems in mind, we have designed a model language that has a
dynamism comparable to that of the aforementioned scripting languages, such as
duck typing, reflection, and partial function application. A notable omission
is closure scoping. However, allowing function currying gives expressive power
to the language comparable to that of languages with closure or lexical
scoping.

The two concerns are not distinct ones, but an interconnected dialectic. The
theoretical need is there because of the difficulty of describing the abstract
and concrete meaning of dynamic languages, which often allow side-effect
causing, type-altering functions. With such complexity, duck-typed languages
are interesting test cases for which we formulate concrete semantics, abstract
interpretation and the proof of correctness. Our Haskell implementation of
both concrete and abstract analysis, appearing in the appendix to this thesis,
illustrates the practicality of the proposed programming language semantics.

This work is inspired by Haskell’s use of monads, and we assume the reader’s
familiarity with monadic style Haskell programming. We also assume knowledge
of lambda notation, denotational semantics, order and fixed point theory at
the level of the textbook of Nielson and Nielson’s [1].

In the following section, we discuss other works in the field of language
semantics and differentiate our work from them. In section 3, we give a
general overview of the proposed language semantics framework and analysis. In
sections 4 and 5, we formally introduce our framework. In section 6, we
develop a model language with features gradually added on. We also present
concrete and abstract analysis of the language in each stage of development in
parallel. In sections 7 and 8, we argue formal properties of the language
analysis. Finally, in section 9, we conclude this thesis and discuss future
direction.

##  2 Related work

Denotational semantics is the starting point of our development of a formal
framework. The idea of incorporating monads into denotational definitions was
developed by Liang and Hudak [2, 3]. Whereas these works modularise an
analytic framework by having multiple layers of monadic transformations, we
instead parametrise the definition of a program state.

Action semantics, as advanced by Mosses [4], shares the motivation that
semantics ought to be pragmatic, yet expressive enough to deal with non-
trivial, feature-rich languages. While action semantics endeavours to devise a
new meta-language for describing semantics, we constrain ourself to the
language of denotational semantics, and seek to devise a formalism largely
compatible with denotational semantics.

The idea of constructing formulae with parametric types can be found in
Wadler’s work [5]. The present work is a special application of the
parametricity in the field of language semantics and analysis.

Regarding the type analysis of dynamic languages, there have been numerous
studies [6, 7, 8, 9] that consider simple toy languages and their semantics
for the purpose of static analysis of dynamic languages. A major difference
between those languages and the model language presented in this paper is that
our language is designed to capture the critical feature of real world
languages which allows functions to alter types through side-effect causing
statements. We point out similarities and differences of this work compared to
the cited works as we encounter them in this thesis.

Type analysis plays a crucial part in compiling scripting languages, mainly to
improve performance. Ancona et al [10] and Dufour [11] design restricted
versions of scripting languages so that static inference of types can be
performed. We adopt several techniques employed in those projects, such as the
use of named memory allocation sites as static references.

An important use case of functions in dynamically typed languages is “mixin”
functions [12]. By passing arguments to a mixin function, objects can be
extended with extra methods; that is, functionality can be added dynamically.
There are model languages and formalisations of mixin functions, such as the
works of Anderson et al [6] and Mens et al [13]. Where those works seek to
find functional models for mixins, we define instead a language (with side-
effect causing functions) that is expressive enough to program mixin
inheritance.

Jensen et al [14] describe a feature-complete analyser for the JavaScript
language. Our work can be extended further to provide the semantic foundation
for such an analyser. Such an attempt to formalise the analysis might pave the
way for further refinement and improvement.

##  3 Overview

Our semantic framework is comprised of two components: one for the syntactic
structure, and the other for giving meanings to the primitive operations. What
divides the two is the following separation of concerns:

  1. 1.

What are the semantic operations entailed in a particular syntactic structure?
For example, syntactic structure $\llbracket a=30\rrbracket$ entails a
primitive operation $\mathtt{asg}\left(a,30\right)$.

  2. 2.

How do we interpret such semantic operations in a particular point of view? If
we were to give a concrete interpretation, we would interpret
$\mathtt{asg}\left(a,30\right)$ as updating an environment with a newly
defined variable e.g., $Env\left[a=30\right]$.

Observe that an interpretation of syntactic structure can remain agnostic of
the structure of a program state at a given point. Therefore, once we remove
the actual interpretation of primitive operations, what remains in a semantics
can be re-used for multiple interpretations of the language. Hence, not only
are the primitive operations parametrised, but so is the whole definition of
the domain of the program state. Such a separation of concerns also helps to
define an extensible semantics, to which adding a new feature takes as little
effort as possible.

Now we give a formal definition of our framework.

######  Definition 1 (Parametric semantics).

A parametric semantics $Q$ is a quintuple $\left(X,State,Value,s,P\right)$
where $X$ is a collection of semantic functions for syntactic structures, as
outlined below; $State$ is a set of representations of computation state,
which can be anything to suit a particular analysis; $Value$ is a set of all
possible values that an expression can be evaluated to be; $s$ is an initial
program state; and $P$ is the set of primitive operations of the semantics. We
assume throughout that different states are incomparable. In other words,
$State$ is ordered by identity.

Throughout the analysis, these primitive operations are the parameters of our
analysis:

  * •

$\mathtt{esc}$ takes a state and reports whether it is escaping (i.e., whether
or not control flow reaches the successor statement)

  * •

$\mathtt{cond}$ interprets the meaning of a branching point when a value and
two transformations (one for true and another for false) are given

  * •

$\mathtt{asg}$ takes an identifier and a value, and performs assignment

  * •

$\mathtt{val}$ takes an identifier and produces its meaning

  * •

$\mathtt{conval}$ takes a constant and produces its meaning

  * •

$\mathtt{getinput}$ and $\mathtt{dooutput}$ define the meanings of console I/O
operations

  * •

$\mathtt{bin}$ defines the meaning of all binary operations given two values

  * •

$\mathtt{ret}$ defines the meaning of a return statement given the value to be
returned

  * •

$\mathtt{fundecl}$ defines the meaning of dynamic execution of a function
declaration

  * •

$\mathtt{apply}$ defines the meaning of (possibly partially) applying a
function to a list of values

  * •

$\mathtt{get}$ and $\mathtt{set}$ define the meaning of getting or setting a
member of an object

  * •

$\mathtt{getglobal}$ and $\mathtt{getthis}$ define the meanings of keywords
$\mathtt{global}$ and $\mathtt{this}$, respectively

  * •

$\mathtt{newobj}$ defines the meaning of instantiating a new object from a
particular allocation site

Types of these operations are given in section 6 as we introduce them.

Our model language, as we let it evolve through this thesis, has a set of
features found commonly in scripting languages. In the remainder of the thesis
we provide the semantics for a language with many different features. We
introduce the components of the language step by step. The aim is to
demonstrate that the semantic formalism enables such a stepwise development,
each step being incremental in the sense that it does not require revision of
the semantic equations developed in earlier steps.

⬇

1function fact(f,x) {

2 if(x < 2) { return 1; }

3 return x * f(f,x-1);

4}

5output fact(fact,input);

6

7fa=fact(fact);

8output fa(input);

9

10function Fruit(v) {

11 this.value = v;

12}

13

14global.answer = 0;

15

16function juicible(fruit, juice) {

17 function juiceMe(j,x) {

18 return this.value + j + x;

19 }

20 fruit.juice = juiceMe(juice); #currying

21 global.answer=42;

22}

23

24# Juicibles

25apple = new Fruit(15);

26juicible(apple, 20);

27grape = new Fruit(30);

28juicible(grape, 50);

29

30# Non-juicibles

31banana = new Fruit(20);

32watermelon = new Fruit(25);

33

34output apple.juice(10); # 15 + 20 + 10

35output grape.juice(10); # 30 + 50 + 10

36output global.answer; # 42

37

38try {

39 if(input > 42) {throw 42;}

40} catch(e) {

41 output e;

42}

Figure 3.1: Example SDTL program

Figure 3.1 is an example of a program written in the model language. We call
this model language Simple Duck-Typed Language(SDTL). A locally-scoped
procedural language with support for higher order functions (lines 1 to 5) is
introduced in Section 6.1. Function currying (lines 7, 8 and 20) is introduced
in Section 6.2. Object oriented features, including duck-typing and
reflection, are introduced in Section 6.3. Finally, exception handling (lines
38 to 42) is introduced in Section 6.4.

##  4 Analytic framework

In this section we introduce a monadic construct specifically designed for the
purpose of program analysis. We then introduce polymorphic auxiliary functions
that are useful in extending theories in a modular manner.

First we define the monadic constructions. We define a type constructor $M$
and a bind operator $\Yright$.

######  Definition 2 (Type constructor).

The type constructor $M$ has the following polymorphic definition. $F$ is the
set of program semantics. It is necessary to have this as an input to the
state transformation in order to give the fixed point characterisation of
semantics. $F$ is given a formal definition in section 5. The $a$ parameter to
the type is used in different context to extract different information from
the semantics.

$M\ a=F\rightarrow State\rightarrow\wp\left(State\times
a\cup\left\\{\mathsf{Null}\right\\}\right)$

Observe that a single state can give rise to multiple corresponding successor
states. We are essentially modelling a non-deterministic state transformation.
This gives us the flexibility to handle both concrete and abstract semantics
within a single framework.

Every statement is understood as a state transformer. We distinguish between
“normal” and “escaping” statements, the latter yielding an “escape” state. For
example, when a function returns, the return statement transforms the current
state into an escape state. Our “bind” operator relies on a parametric
operation $\mathtt{esc}$ to spell out the precise mechanism for escaping the
current program execution flow. The $\mathtt{esc}$ function returns true if a
state does not continue to the next expression or statement (having
encountered a return statement, for example). This provides a flexible and
general formalisation of a control flow, and it allows the handling of
exceptions as well as function return statements.

In such escaping cases, there is no appropriate value of the type $a$ to be
associated with the successor states. Hence, we introduce $\bot$ to be
assigned to successor states of the escaping states.

######  Definition 3 (Bind operator).

We define a bind operator $\Yright$.

$\displaystyle\left(\Yright\right)$ $\displaystyle:$ $\displaystyle M\
a\rightarrow\left(a\rightarrow M\ b\right)\rightarrow M\ b$ $\displaystyle T\
\Yright\ U$ $\displaystyle=$ $\displaystyle\lambda f\lambda s.\>\mathbf{let}\
S=T\ f\ s\ \mathbf{in}\underset{\left\langle s^{\prime},a\right\rangle\in
S}{\bigcup}\left(\begin{gathered}\mbox{if}\
\mathtt{esc}\left(s^{\prime}\right)\ \mbox{then}\ \left\\{\left\langle
s^{\prime},\mathsf{Null}\right\rangle\right\\}\ \mbox{else}\ U\ a\ f\
s^{\prime}\end{gathered}\right)$

######  Definition 4 (Point-wise ordering of state transformations).

Given $T,U\in State\rightarrow\wp\left(State\times
a\cup\left\\{\mathsf{Null}\right\\}\right)$,
$T\sqsubseteq U$ iff $\forall x\in State,\left(T\ x\right)\subseteq\left(U\
x\right)$

######  Definition 5 (Point-wise ordering of monadic functions).

Given $T,U\in M\ a$, $T\sqsubseteq U$ iff $\forall f\in F,\left(T\
f\right)\sqsubseteq\left(U\ f\right)$

######  Theorem 6 (Preservation of monotonicity).

Given monads $T$, $T^{\prime}$ and $U$, $T\sqsubseteq T^{\prime}\implies
T\Yright U\sqsubseteq T^{\prime}\Yright U$

###### Proof.

When a state $x$ is a member of $T\Yright U$ for some $f\in F$ and an initial
state $s$, there exists an intermediate state $x^{\prime}\in\left(T\ f\
s\right)$ from which $x$ is derived by $U$. Clearly, such intermediate state
is also a member of $T^{\prime}\ f\ s$ by definition of point-wise ordering.

Formally, $\forall f\in F\forall s\in State,\exists x,x\in\left(\left(T\Yright
U\right)\ f\ s\right)\Leftrightarrow\exists x^{\prime},x^{\prime}\in\left(T\
f\ s\right)\wedge x\in\left(U\ f\ x^{\prime}\right)$ by the definition of bind
operation. Now, $T\sqsubseteq T^{\prime}\implies
x^{\prime}\in\left(T^{\prime}\ f\ s\right)$. Hence,
$x\in\left(\left(T^{\prime}\Yright U\right)\ f\ s\right)$. ∎

Having a monadic structure helps provide modularity. For example, if a
particular parametrised operation takes a state but only produces a value, it
would be redundant to include a state as a part of returning type, to match
the definition of monadic binding. In such a case, we take a function that
returns only a value, then lift it to be used in the monadic context.

######  Definition 7 (Monadic functions).

We define the following auxiliary functions to incorporate non-monadic
functions as a part of monadic transformation:

  * •

(return for $M$) $I_{A}$ is an identity state transformer that takes a
constant and lifts it to an identity state transformer with the constant as a
return value

$I_{A}:a\rightarrow M\ a$

$I_{A}\ v=\lambda f\lambda s.\left\\{\left\langle s,v\right\rangle\right\\}$

  * •

(lift for $M$) $I_{V}$ lifts a function that takes a state and returns a value
to a monadic function

$I_{V}:\left(State\rightarrow a\right)\rightarrow M\ a$

$I_{V}\ t=\lambda f\lambda s.\left\langle\left\\{\left\langle s,t\
s\right\rangle\right\\},\emptyset\right\rangle$

  * •

$I_{S}$ takes a non-deterministic transformation and lifts it to a monadic
function

$I_{S}:\left(State\rightarrow\wp\left(State\right)\right)\rightarrow M\ a$

$I_{S}\ T=\lambda f\lambda s.\left\\{\left\langle
s^{\prime},\mathsf{Unit}\right\rangle\mid s^{\prime}\in T\ s\right\\}$

######  Definition 8 (Record updater).

We model a state as a record with named fields. In this way, an update
operation written for a particular set of fields can be reused without
redefining it when we add extra dimensions to a $State$ domain to accommodate
features that are orthogonal to the features of the previous version.

When we have a record $\rho$ with named fields $\left\langle
c_{1},\ldots,c_{k}\right\rangle$, and when an updater function $U$ updates
fields $c_{i},\ldots,c_{j}$, we define a function $\Upsilon$ that takes a
record, projects its fields into an n-tuple corresponding to the selected
fields ($P_{c_{i},\ldots,c_{j}}$), lets $U$ update the tuple, and finally
updates the whole record with the updated tuple ($J_{c_{i},\ldots,c_{j}}$).

$\displaystyle P_{c_{i},\ldots,c_{j}}$ $\displaystyle=$
$\displaystyle\lambda\rho.\left\langle a_{i},\ldots,a_{j}\right\rangle$
$\displaystyle J_{c_{i},\ldots,c_{j}}$ $\displaystyle=$
$\displaystyle\lambda\left\langle
a_{i},\ldots,a_{j}\right\rangle\lambda\rho.\rho\left[c_{n}=a_{n},n\in\left\\{i,\ldots,j\right\\}\right]$
$\displaystyle\Upsilon_{c_{i},\ldots,c_{j}}\ U$ $\displaystyle=$
$\displaystyle J_{c_{i},\ldots,c_{j}}\circ U\circ P_{c_{i},\ldots,c_{j}}$

where $a_{i}$ is a value for the field $c_{i}$ of a record $\rho$

Similarly, we define an operation to update a record and return a value.

$\Psi_{c_{i},\ldots,c_{j}}\
U=\lambda\rho.\left\langle\rho^{\prime},a\right\rangle$

where $\left\langle\upsilon,a\right\rangle=U\ \left(P_{c_{i},\ldots,c_{j}}\
\rho\right)$ and $\rho^{\prime}=J_{c_{i},\ldots,c_{j}}\ \upsilon$

Finally, we define a value extractor, that takes a record and selects a value
from it.

$\Theta{}_{c_{i},\ldots,c_{j}}\ U=U\circ P_{c_{i},\ldots,c_{j}}$

When $c$ is an n-tuple space for chosen fields and $r$ is a domain of a
$State$ record, the functions defined here have the following type signatures:

$\displaystyle\Upsilon$ $\displaystyle:$ $\displaystyle\left(c\rightarrow
c\right)\rightarrow\left(r\rightarrow r\right)$ $\displaystyle\Psi$
$\displaystyle:$ $\displaystyle\left(c\rightarrow c\times
a\right)\rightarrow\left(r\rightarrow r\times a\right)$ $\displaystyle\Theta$
$\displaystyle:$ $\displaystyle\left(c\rightarrow
a\right)\rightarrow\left(r\rightarrow a\right)$

######  Example 9 (Record updater example).

To see these functions in use, suppose we have a simple record structure for
personal contacts.

$\displaystyle Name$ $\displaystyle=$ $\displaystyle String$ $\displaystyle
Address$ $\displaystyle=$ $\displaystyle String$ $\displaystyle Age$
$\displaystyle=$ $\displaystyle\mathbb{N}$ $\displaystyle Contact$
$\displaystyle=$ $\displaystyle Name\times Address\times Age$

  * •

$\mathtt{addAge}$ updates age field of a contact record.

$\mathtt{addAge}\left(n\right)=\Upsilon_{Age}\ \lambda a.\left(a+n\right)$

  * •

$\mathtt{getAgeAndAdd}$ returns the previous age field value while updating
the age field.

$\mathtt{getAgeAndAll}\left(n\right)=\Psi_{Age}\ \lambda a.\left\langle
a+n,a\right\rangle$

  * •

$\mathtt{getAge}$ extracts age information from a contact record.

$\mathtt{getAge}=\Theta_{Age}\ \lambda a.a$

######  Definition 10 (Singleton lifting).

Another commonly occurring pattern is that functions often return a singleton
set. We define a function that takes a function returning a value and lifts it
to be a function that returns a singleton set.

$\displaystyle\Gamma$ $\displaystyle:$ $\displaystyle\left(a\rightarrow
b\right)\rightarrow\left(a\rightarrow\wp\left(b\right)\right)$
$\displaystyle\Gamma\ F\ x$ $\displaystyle=$ $\displaystyle\left\\{F\
x\right\\}$

For simplicity of notation, we compose this function with the other functions
from Definition 8.

$\displaystyle\bar{\Upsilon}$ $\displaystyle=$
$\displaystyle\Gamma\circ\Upsilon$ $\displaystyle\bar{\Psi}$ $\displaystyle=$
$\displaystyle\Gamma\circ\Psi$ $\displaystyle\bar{\Theta}$ $\displaystyle=$
$\displaystyle\Gamma\circ\Theta$

We now have monadic constructs and auxiliary functions to describe the
semantic functions of the model language. We can now define the semantic
functions of the language.

##  5 Semantic functions

We use syntax nodes as references to various items constituting program
environment. To all statements and expressions in a program, we designate
unique identifiers in order to reference them. For that purpose, we define the
following syntactic nodes and unique identifier spaces.

  * $Stm$

is the set of statement nodes.

  * $Exp$

is the set of expression nodes.

  * $Lexp$

is the set of left-expression nodes.

  * $Sid$

is the set of statement identifiers.

  * $Eid$

is the set of expression identifiers.

  * $Id$

is the set of alphanumeric identifiers.

Note that we use an sid of a function declaration statement as a reference
point for the function defined. The $\mathtt{param}$ and $\mathtt{arity}$
functions take such an sid and return a list of parameter names, and the arity
of the function, respectively.

Where we specifically refer to an identifier to a syntactic construct, we
write $\llbracket\left|X\right|_{x}\rrbracket$ to mean a statement or
expression $X$ with an id $x$. In cases where such identifiers are not
directly referenced, we omit them for simplicity.

######  Definition 11 (Semantic functions).

The analytic framework contains the following semantic functions:

$\displaystyle F$ $\displaystyle=$ $\displaystyle Sid\rightarrow
Stm\times\left(State\rightarrow\wp\left(State\right)\right)$
$\displaystyle\mathcal{S}$ $\displaystyle:$ $\displaystyle Stm\rightarrow
F\rightarrow
State\rightarrow\wp\left(State\times\left\\{\mathsf{Unit},\mathsf{Null}\right\\}\right)$
$\displaystyle\mathcal{E}$ $\displaystyle:$ $\displaystyle Exp\rightarrow
F\rightarrow State\rightarrow\wp\left(State\times
Value\cup\left\\{\mathsf{Null}\right\\}\right)$ $\displaystyle\mathcal{L}$
$\displaystyle:$ $\displaystyle Lexp\rightarrow F\rightarrow
State\rightarrow\wp\left(State\times
Value\cup\left\\{\mathsf{Null}\right\\}\right)$

$\mathcal{S},\mathcal{E}$ and $\mathcal{L}$ are semantic functions for
statements, expressions and left expressions, respectively. $F$ is a function
space to model the collection of functions in a program. Given the sid of a
function declaration site, it gives a statement node for function declaration
and a state transformer. Note that in this picture a function “returns” a
value by giving a state transformation. Incorporating such a concept as a
return value in a $State$ itself provides a greater flexibility in describing
the effects of executing a statement or an expression at a particular program
point.

We define following auxiliary functions to describe the use of the references
to syntax nodes.

$\displaystyle\mathtt{stm}$ $\displaystyle:$ $\displaystyle F\rightarrow
Sid\rightarrow Stm$ $\displaystyle\mathtt{param}$ $\displaystyle:$
$\displaystyle F\rightarrow Sid\rightarrow\left[Id\right]$
$\displaystyle\mathtt{arity}$ $\displaystyle:$ $\displaystyle F\rightarrow
Sid\rightarrow\mathbb{N}\cup\left\\{0\right\\}$ $\displaystyle\mathtt{run}$
$\displaystyle:$ $\displaystyle F\rightarrow Sid\rightarrow
State\rightarrow\wp\left(State\right)$

##  6 The language under study

We define the model language, the SDTL (Simple Duck-Typed Language).

###  6.1 The procedural core language

We start off with a procedural language with C-like syntax.

<con> ::= <Num> | <Bool>

<Lexp> ::= ID

<Exp> ::= <con> | <Lexp> | ‘input’ <Lexp> ‘(’ [<Exp> [,<Exp>]*]? ‘)’ <Exp> <binop> <Exp> ‘(’ <Exp> ‘)’

<binop> ::= ‘+’ | ‘-’ | ‘*’ | ‘/’ | ‘>’ | ‘<’ | ‘==’

<Stm> ::= nil | <Stm> ‘;’ <Stm> | <Exp> ‘output’ <Exp> <Lexp> ‘=’ <Exp> ‘if’ ‘(’ <Exp> ‘)’ ‘’ <Stm> ‘’ ‘if’ ‘(’ <Exp> ‘)’ ‘’ <Stm> ‘’ ‘else’ ‘’ <Stm> ‘’ ‘while’ ‘(’ <Exp> ‘)’ ‘’ <Stm> ‘’ ‘function’ Id ‘(’ [Id [, Id]*]? ‘)’ ‘’ <Stm> ‘’ ‘return’ <Exp>

Here _Num_ and _Bool_ are the syntactic categories for integers and boolean
values.

SDTL does not have a separate category for function and variable declarations.
Variables are declared _ad hoc_ whenever such variables appear as a left
expression to assignment statements. Function declarations are statements
themselves, which allow them to appear anywhere in the program.

SDTL supports higher-order functions, which allows functions to be recursively
referenced. For example, we can define a factorial function in a recursive
manner.

######  Example 12 (Recursively defined factorial function).

In SDTL, the factorial function can be implemented in a recursive way.

⬇

1function fact(f,n) {

2 if(n>1) { return f(f,n-1) * n; } else { return 1; }

3}

4

5z=fact(fact,input);

6output z;

In this example, the function $\mathtt{fact}$ takes two arguments. The first
is the function pointer to recursively invoke, and the second is the usual
argument to the function. This example illustrates that recursive functions
are possible even in the absence of lexical scoping or other special scoping
rules to allow a function body to refer to the function itself.

Given the availability of higher-order functions, we formulate the meaning of
a function as a fixed point (see the definition of $F$). The semantic
functions for SDTL are defined in figure 6.1. We use auxiliary functions
$\mathtt{evalParams}$ and $\mathtt{call}$ to describe a function call. (Note
that we use $\epsilon$ for the empty sequence, $\left[a\right]$ for the set of
sequences of any number of values of type $a$, and the notation $a\smallfrown
b$ to denote concatenation of sequences $a$ and $b$.)

$\displaystyle\mathtt{call}$ $\displaystyle:$ $\displaystyle
Sid\rightarrow\left[Value\right]\rightarrow M\ Value$
$\displaystyle\mathtt{call}\left(n,p\right)$ $\displaystyle=$
$\displaystyle\lambda f\lambda\rho.\left\\{\mathtt{leave}\ \rho\
\rho^{\prime}\mid\rho^{\prime}\in S\right\\}\ \mbox{where}\
S=\mathtt{run}\left(f,n\right)\ \left(\mathtt{enter}\ \rho\ n\ p\
\mathtt{param}\left(f,n\right)\right)$

$\displaystyle\mathtt{evalParams}$ $\displaystyle:$
$\displaystyle\left[Exp\right]\times\left[Value\right]\rightarrow F\rightarrow
State\rightarrow\wp\left(State\times\left[Value\right]\right)$
$\displaystyle\mathtt{evalParams}\ \epsilon\ ps\ f\ \rho$ $\displaystyle=$
$\displaystyle\lambda
f\lambda\rho.\left\\{\left\langle\rho,ps\right\rangle\right\\}$
$\displaystyle\mathtt{evalParams}\ \llbracket E\rrbracket\smallfrown Exps\ ps$
$\displaystyle=$ $\displaystyle\lambda
f\lambda\rho.\underset{\left\langle\rho^{\prime},con\right\rangle\in
S}{\bigcup}\left\\{\mathtt{evalParams}\ Exps\ \left(ps\smallfrown con\right)\
f\ \rho^{\prime}\right\\}$ $\displaystyle\mbox{where}\;S\ =\ \mathcal{E}\
\llbracket E\rrbracket\ f\ \rho$

$\mathtt{enter}$ is a parametrised function that takes a caller’s state at the
time of function invocation and an id-to-constant value mapping, and
constructs an initial state for a callee. $\mathtt{leave}$ takes both the
caller’s state and the resulting states of callee’s, and constructs the
caller’s states after the function call. These functions are parametrised so
as to allow each interpretation to define the exact shape of a program state
and its manipulation during a function call and return. These functions have
the following types:

$\displaystyle\mathtt{enter}$ $\displaystyle:$ $\displaystyle State\rightarrow
Sid\rightarrow\left[Value\right]\rightarrow\left[Id\right]\rightarrow State$
$\displaystyle\mathtt{leave}$ $\displaystyle:$ $\displaystyle State\rightarrow
State\rightarrow State$

$\displaystyle\mathcal{F}$ $\displaystyle=$ $\displaystyle Y\left(\lambda
f.\lambda n.\left\langle\mathtt{stm}\left(f,n\right),\mathcal{S}\
\llbracket\mathtt{stm}\left(f,n\right)\rrbracket\ f\right\rangle\right)$
$\displaystyle\mathcal{S}\llbracket\epsilon\rrbracket$ $\displaystyle=$
$\displaystyle I_{A}\bot$ $\displaystyle\mathcal{S}\llbracket
S_{1};S_{2}\rrbracket$ $\displaystyle=$ $\displaystyle\begin{aligned}
\mathcal{S}\ \llbracket S_{1}\rrbracket\Yright\lambda\\_.\mathcal{S}\
\llbracket S_{2}\rrbracket\end{aligned}$ $\displaystyle\mathcal{S}\llbracket
E\rrbracket$ $\displaystyle=$ $\displaystyle\mathcal{E}\ \llbracket
E\rrbracket\Yright\lambda\\_.I_{A}\mathsf{Unit}$
$\displaystyle\mathcal{S}\llbracket\mathtt{return}\ E\rrbracket$
$\displaystyle=$ $\displaystyle\mathcal{E}\ \llbracket
E\rrbracket\Yright\lambda v.I_{S}\ \mathtt{ret}\left(V\right)$
$\displaystyle\mathcal{S}\llbracket\mathtt{if}\left(E\right)\ S_{1}\rrbracket$
$\displaystyle=$ $\displaystyle\mathcal{E}\ \llbracket
E\rrbracket\Yright\lambda v.\mathtt{cond}\left(v,\mathcal{S}\ \llbracket
S_{1}\rrbracket,I_{A}\mathsf{Unit}\right)$
$\displaystyle\mathcal{S}\llbracket\mathtt{if}\left(E\right)\ S_{1}\
\mathtt{else}\ S_{2}\rrbracket$ $\displaystyle=$ $\displaystyle\mathcal{E}\
\llbracket E\rrbracket\Yright\lambda v.\mathtt{cond}\left(v,\mathcal{S}\
\llbracket S_{1}\rrbracket,\mathcal{S}\ \llbracket S_{2}\rrbracket\right)$
$\displaystyle\mathcal{S}\llbracket id=E\rrbracket$ $\displaystyle=$
$\displaystyle\begin{aligned} \mathcal{E}\ \llbracket
E\rrbracket&\Yright\lambda v.I_{S}\
\mathtt{asg}\left(id,v\right)\end{aligned}$
$\displaystyle\mathcal{S}\llbracket\mathtt{while}\left(E\right)\
S_{1}\rrbracket$ $\displaystyle=$ $\displaystyle Y\lambda x.\lambda f\lambda
r.\left(\begin{aligned} \mathcal{E}\ \llbracket E\rrbracket\Yright\lambda
v.\mathtt{cond}\left(\begin{gathered}v,\left(\mathcal{S}\ \llbracket
S_{1}\rrbracket\right)\Yright\lambda\\_.x,I_{A}\mathsf{Unit}\end{gathered}\right)\end{aligned}\right)$
$\displaystyle\mathcal{S}\llbracket\mathtt{output}\ E\rrbracket$
$\displaystyle=$ $\displaystyle\mathcal{E}\ \llbracket
E\rrbracket\Yright\lambda v.I_{S}\ \mathtt{dooutput}\left(v\right)$
$\displaystyle S\llbracket\left|\mathtt{function}\
Id_{1}\left(\vec{Id}\right)\ S_{1}\right|_{s}\rrbracket$ $\displaystyle=$
$\displaystyle I_{S}\ \mathtt{fundecl}\left(Id_{1},s\right)$
$\displaystyle\mathcal{E}\llbracket con\rrbracket$ $\displaystyle=$
$\displaystyle I_{A}\ \mathtt{conval}\left(con\right)$
$\displaystyle\mathcal{E}\llbracket L\rrbracket$ $\displaystyle=$
$\displaystyle\mathcal{L}\ \llbracket L\rrbracket$
$\displaystyle\mathcal{E}\llbracket\mathtt{input}\rrbracket$ $\displaystyle=$
$\displaystyle\mathtt{getinput}$ $\displaystyle\mathcal{E}\llbracket
L\left(\vec{E}\right)\rrbracket$ $\displaystyle=$ $\displaystyle\mathcal{L}\
\llbracket L\rrbracket\Yright\lambda n.\left(\mathtt{evalParams}\ \vec{E}\
\emptyset\right)\Yright\lambda p.\mathtt{call}\left(n,p\right)$
$\displaystyle\mathcal{E}\llbracket E_{1}\ binop\ E_{2}\rrbracket$
$\displaystyle=$ $\displaystyle\mathcal{E}\ \llbracket
E_{1}\rrbracket\Yright\lambda c_{1}.\mathcal{E}\ \llbracket
E_{2}\rrbracket\Yright\lambda c_{2}.I_{V}\
\mathtt{bin}\left(binop,c_{1},c_{2}\right)$
$\displaystyle\mathcal{L}\llbracket Id\rrbracket$ $\displaystyle=$
$\displaystyle I_{A}\ \mathtt{val}\left(Id\right)$

Figure 6.1: Semantic equations for a procedural core of SDTL

The types of primitive operations are as follows.

$\displaystyle\mathtt{ret}$ $\displaystyle:$ $\displaystyle Value\rightarrow
State\rightarrow\wp\left(State\right)$ $\displaystyle\mathtt{cond}$
$\displaystyle:$ $\displaystyle Value\rightarrow M\ Value\rightarrow M\
Value\rightarrow M\ Value$ $\displaystyle\mathtt{asg}$ $\displaystyle:$
$\displaystyle Id\rightarrow Value\rightarrow
State\rightarrow\wp\left(State\right)$ $\displaystyle\mathtt{dooutput}$
$\displaystyle:$ $\displaystyle Value\rightarrow
State\rightarrow\wp\left(State\right)$ $\displaystyle\mathtt{fundecl}$
$\displaystyle:$ $\displaystyle Id\rightarrow Sid\rightarrow
State\rightarrow\wp\left(State\right)$ $\displaystyle\mathtt{conval}$
$\displaystyle:$
$\displaystyle\mathbb{Z}\cup\left\\{\mathsf{true},\mathsf{false}\right\\}\rightarrow
Value$ $\displaystyle\mathtt{getinput}$ $\displaystyle:$ $\displaystyle M\
Value$ $\displaystyle\mathtt{bin}$ $\displaystyle:$
$\displaystyle\left\\{+,-,*,/\right\\}\rightarrow\mathbb{Z}\cup\left\\{\mathsf{true},\mathsf{false}\right\\}\rightarrow\mathbb{Z}\cup\left\\{\mathsf{true},\mathsf{false}\right\\}\rightarrow
Value$ $\displaystyle\mathtt{val}$ $\displaystyle:$ $\displaystyle
Id\rightarrow State\rightarrow Value$

####  6.1.1 Concrete interpretation

##### Domain

$\displaystyle FunPointer$ $\displaystyle=$ $\displaystyle Sid$ $\displaystyle
Value$ $\displaystyle=$
$\displaystyle\mathbb{Z}\cup\left\\{\mathsf{true},\mathsf{false}\right\\}\cup\>FunPointer$
$\displaystyle Env$ $\displaystyle=$ $\displaystyle Id\rightarrow Value$
$\displaystyle Return$ $\displaystyle=$ $\displaystyle
Value\cup\left\\{\mathsf{Void}\right\\}$ $\displaystyle CState$
$\displaystyle=$ $\displaystyle Env\times IO\times Return$

$CState$ is a Cartesian product of environment, input/output state and a
return value. The return value is set to be a value when a function is
returning any value inside a function body. This has been incorporated as a
part of a program state so that we can signal escaping from a program flow.
The initial program state is
$\left\langle\emptyset,io,\mathsf{Void}\right\rangle,$ where $io$ is an
initial IO state.

##### Functions

$\displaystyle\mathtt{enter}$ $\displaystyle=$
$\displaystyle\lambda\left\langle\\_,IO,\\_\right\rangle,n,P,p.\left\langle\left[p_{k}\mapsto
P_{k}\right],IO,\mathsf{Void}\right\rangle$ $\displaystyle\mathtt{leave}$
$\displaystyle=$ $\displaystyle\lambda\left\langle
V,\\_,\\_\right\rangle,\left\langle\\_,IO^{\prime},R\right\rangle.\left\langle\left\langle
V,IO^{\prime},\mathsf{Void}\right\rangle,R\right\rangle$

$\displaystyle\mathtt{esc}$ $\displaystyle=$
$\displaystyle\bar{\Theta}_{Return}\ \left(\lambda
R.\left(R\neq\mathsf{Void}\right)\right)$
$\displaystyle\mathtt{cond}\left(v,s_{1},s_{2}\right)$ $\displaystyle=$
$\displaystyle\begin{cases}s_{1}&\mbox{if}\ v=\mathsf{true}\\\
s_{2}&\mbox{if}\ v=\mathsf{\mathsf{false}}\end{cases}$
$\displaystyle\mathtt{asg}\left(id,v\right)$ $\displaystyle=$
$\displaystyle\bar{\Upsilon}_{Env}\ \left(\lambda V.V\left[id\mapsto
v\right]\right)$ $\displaystyle\mathtt{val}\left(id\right)$ $\displaystyle=$
$\displaystyle\bar{\Upsilon}_{Env}\ \left(\lambda V.V\left(id\right)\right)$
$\displaystyle\mathtt{conval}\left(con\right)$ $\displaystyle=$
$\displaystyle\left\\{con\right\\}$
$\displaystyle\mathtt{getinput\left(\rho\right)}$ $\displaystyle=$
$\displaystyle\bar{\Psi}_{IO}\ \lambda O.\left\langle O^{\prime},\mbox{user
input integer}\right\rangle\ \mbox{see note}$
$\displaystyle\mathtt{dooutput}\left(v\right)$ $\displaystyle=$
$\displaystyle\bar{\Upsilon}_{IO}\ \lambda O.O^{\prime}\ \mbox{see note}$
$\displaystyle\mathtt{fundecl}(id,n)$ $\displaystyle=$
$\displaystyle\bar{\Upsilon}_{Env}\ \left(\lambda V.V\left[id\mapsto
n\right]\right)$ $\displaystyle\mathtt{ret}\left(v\right)$ $\displaystyle=$
$\displaystyle\bar{\Upsilon}_{Return}\ \left(\lambda R.v\right)$
$\displaystyle\mathtt{bin}\left(op,c_{1},c_{2}\right)$ $\displaystyle=$
$\displaystyle c_{1}\ op\ c_{2}\ \mbox{(perform binary operation between two
constants)}$

We omit a detailed description of the IO environment. Normally, IO can be
modelled as a queue of inputs and outputs as they are given and produced
during the execution of a program.

######  Example 13 (Concrete interpretation of recursive factorial function).

The program in example 12 is concretely interpreted as follows.

  * •

At line 1, $\mathtt{fundecl}\left(\mathtt{fact},1\right)$ updates environment
to be $\left[\mathtt{fact}\mapsto\mathsf{Function}\ 1\right]$ assuming the
function declaration has a unique id of 1.

  * •

At line 5, $\mathtt{getinput}$ gives a user input. Assume that the input was
2. $\mathtt{evalParam}$ gives $\left[\left(\mathsf{Function}\
1\right),2\right]$. In a function call
$\mathtt{call}\left(1,\left[\left(\mathsf{Function}\
1\right),2\right]\right)$, we first construct the initial state of a function
call. $\mathtt{enter}$ gives
$\left\langle\left[\mathtt{f}\mapsto\left(\mathsf{Function}\
1\right),\mathtt{n}\mapsto 2\right],IO,Void\right\rangle$.

  * •

At line 2, evaluating expression $\mathtt{n}>1$ yields true. $\mathtt{cond}$
invokes another function call, with initial state
$\left\langle\left[\mathtt{f}\mapsto\left(\mathsf{Function}\
1\right),\mathtt{n}\mapsto 1\right],IO,Void\right\rangle$.

  * •

On the second call fact(f,1), $\mathtt{n}>1$ yields false. Hence,
$\mathtt{cond}$ invokes $\mathtt{ret}\left(1\right)$ which gives final state
of $\left\langle\left[\mathtt{f}\mapsto\left(\mathsf{Function}\
1\right),\mathtt{n}\mapsto 1\right],IO,1\right\rangle$.

  * •

On the first call, this state is first evaluated to yield value $1$ by
$\mathtt{leave}$. Then, f(f,1) * 2 evaluates to 2, which becomes the ultimate
return value.

  * •

At line 5, after the function call $\mathtt{leave}$ gives
$\left\langle\left[\mathtt{fact}\mapsto\mathsf{Function}\
1\right],IO,\mathsf{Void}\right\rangle$ as the final state. $\mathtt{asg}$
adds symbol $\mathtt{z}$ to the environment: $\mathtt{z}\mapsto 2$

  * •

At line 6, $\mathtt{val\left(z\right)}$ evaluates to 2, which is the final
output of the program.

####  6.1.2 Abstract interpretation

At this stage, abstract interpretation looks largely similar to concrete
interpretation. Notable differences are that we approximate each constant by
its type, and that $\mathtt{cond}$ is a non-deterministic transformation where
it collects effects of both branches at a branching point.

##### Domain

$\displaystyle FunPointer$ $\displaystyle=$ $\displaystyle Sid$ $\displaystyle
AVal$ $\displaystyle=$
$\displaystyle\left\\{\mathsf{Num},\mathsf{Bool}\right\\}\cup FunPointer$
$\displaystyle AEnv$ $\displaystyle=$ $\displaystyle Id\rightarrow AVal$
$\displaystyle AReturn$ $\displaystyle=$ $\displaystyle
AVal\cup\left\\{\mathsf{Void}\right\\}$ $\displaystyle AState$
$\displaystyle=$ $\displaystyle AEnv\times AReturn$

Composition of an abstract domain is similar to that of the concrete
counterpart, except that it does not include an IO state. $\bot$ is an
undetermined value, which is used to approximate unknown function calls at an
initial stage. The initial program state is
$\left\langle\emptyset,\mathsf{Void}\right\rangle$.

##### Functions

$\displaystyle\mathtt{enter}$ $\displaystyle=$
$\displaystyle\lambda\left\langle\\_,\\_\right\rangle,n,P,p.\left\langle\left[p_{k}\mapsto
P_{k}\right],\mathsf{Void}\right\rangle$ $\displaystyle\mathtt{leave}$
$\displaystyle=$ $\displaystyle\lambda\left\langle
V,\\_\right\rangle,\left\langle\\_,R\right\rangle.\left\langle\left\langle
V,\mathsf{Void}\right\rangle,R\right\rangle$

$\displaystyle\mathtt{esc}$ $\displaystyle=$
$\displaystyle\bar{\Theta}_{AReturn}\ \left(\lambda
R.\left(R\neq\mathsf{Void}\right)\right)$
$\displaystyle\mathtt{cond}\left(v,s_{1},s_{2}\right)$ $\displaystyle=$
$\displaystyle\lambda f\lambda\eta.\left(s_{1}\ f\ \eta\right)\cup\left(s_{2}\
f\ \eta\right)$ $\displaystyle\mathtt{asg}\left(id,v\right)$ $\displaystyle=$
$\displaystyle\bar{\Upsilon}_{AEnv}\
\left(\lambda\sigma.\sigma\left[id=v\right]\right)$
$\displaystyle\mathtt{val}\left(id,v\right)$ $\displaystyle=$
$\displaystyle\bar{\Upsilon}_{AEnv}\
\left(\lambda\sigma.\sigma\left(id\right)\right)$
$\displaystyle\mathtt{conval}\left(con\right)$ $\displaystyle=$
$\displaystyle\begin{cases}\Gamma\ \mathsf{Num}&\mbox{if}\ con\in\mathbb{N}\\\
\Gamma\ \mathsf{Bool}&\mbox{if}\ con\in\mathbb{B}\end{cases}$
$\displaystyle\mathtt{getinput}$ $\displaystyle=$ $\displaystyle\Gamma\
\left(\lambda\eta.\left\langle\eta,\mathsf{Num}\right\rangle\right)$
$\displaystyle\mathtt{dooutput}\left(v\right)$ $\displaystyle=$
$\displaystyle\Gamma\ \left(\lambda\eta.\eta\right)$
$\displaystyle\mathtt{fundecl}\left(id,n\right)$ $\displaystyle=$
$\displaystyle\bar{\Upsilon}_{AEnv}\ \left(\lambda\sigma.\sigma\left[id\mapsto
n\right]\right)$ $\displaystyle\mathtt{ret}\left(v\right)$ $\displaystyle=$
$\displaystyle\bar{\Upsilon}_{AReturn}\ \left(\lambda R:AReturn.v\right)$
$\displaystyle\mathtt{bin}\left(op,c_{1},c_{2}\right)$ $\displaystyle=$
$\displaystyle\begin{cases}\Gamma\ \mathsf{Num}&\mbox{if}\
op\in{\scriptstyle\left\\{+,-,*,/\right\\}}\\\ \Gamma\
\mathsf{Bool}&\mbox{otherwise}\end{cases}$

Function definitions are largely similar to that of concrete definition.

######  Example 14 (Abstract interpretation of recursive factorial function).

The program in example 12 is abstractly interpreted as follows.

  * •

At line 1, $\mathtt{fundecl}\left(\mathtt{fact},1\right)$ updates environment
to be $\left[\mathtt{fact}\mapsto\mathsf{Function}\ 1\right]$ assuming the
function declaration has a unique id of 1.

  * •

At line 5, $\mathtt{getinput}$ gives an abstract value
$\mathsf{\mathsf{Num}}$. $\mathtt{evalParam}$ gives
$\left[\left(\mathsf{Function}\ 1\right),\mathsf{\mathsf{Num}}\right]$. In a
function call $\mathtt{call}\left(1,\left[\left(\mathsf{Function}\
1\right),\mathsf{\mathsf{Num}}\right]\right)$, we first construct initial
state of a function call. $\mathtt{enter}$ gives

$\left\langle\left[\mathtt{f}\mapsto\left(\mathsf{Function}\
1\right),\mathtt{n}\mapsto\mathsf{Num}\right],IO,\mathsf{Void}\right\rangle$

  * •

The meaning of this function call is determined via a fixed point iteration by
progressively updating the current approximation of the meaning of the
function call, starting from a null hypothesis that the function call does not
return any state.

Current approximation | Meaning of function call | Note
---|---|---
$\emptyset$ | $\left\\{\left\langle\left[\mathtt{fact}\mapsto\left(\mathsf{Function}\ 1\right)\right],\mathsf{\mathsf{Num}}\right\rangle\right\\}$ |
$\left\\{\left\langle\left[\mathtt{fact}\mapsto\left(\mathsf{Function}\ 1\right)\right],\mathsf{\mathsf{Num}}\right\rangle\right\\}$ | $\left\\{\left\langle\left[\mathtt{fact}\mapsto\left(\mathsf{Function}\ 1\right)\right],\mathsf{\mathsf{Num}}\right\rangle\right\\}$ | Fixed point

Implementation of this fixed point iteration is found in the $\mathtt{fun}$
function in appendix A.4.

  * •

This yields $\left\langle\left[\mathtt{fact}\mapsto\left(\mathsf{Function}\
1\right)\right],\mathsf{\mathsf{Num}}\right\rangle$

  * •

After $\mathtt{leave}$,$\mathtt{asg}$ and $\mathtt{dooutput}$, we have the
final state of the program: $\left[\mathtt{fact}\mapsto\mathsf{Function}\
1,\mathtt{z}\mapsto\mathsf{\mathsf{Num}}\right]$

######  Example 15 (Abstract interpretation of a while loop).

The following example illustrates an interpretation of a while loop through a
fixed point iteration.

The program calculates sum of a sequence. For the purpose of illustration, we
have added variable $\mathtt{x}$ that changes its type inside a while loop.

⬇

1sum = 0;

2z = input;

3x = 50;

4while(z>0) {

5 sum = sum + z;

6 z = z - 1;

7 x = true;

8}

9

10output sum;

  * •

At line 4, we have environment
$\left[\mathtt{sum}\mapsto\mathsf{\mathsf{Num}},\mathtt{z}\mapsto\mathsf{\mathsf{Num}},\mathtt{x}\mapsto\mathsf{\mathsf{Num}}\right]$.

  * •

As an initial hypothesis, we assume that the statement body of a while loop
does not cause any change in the program state for any given initial state. We
progressively update this approximation until we meet a fixed point.

Current Approximation | Init $\rightarrow$ Final State
---|---
$\emptyset$ | $\left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\ \mathtt{z}&\mapsto&\mathsf{Num}\\\ \mathtt{x}&\mapsto&\mathsf{Num}\end{array}\right]\rightarrow\left\\{\begin{gathered}\left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\ \mathtt{z}&\mapsto&\mathsf{Num}\\\ \mathtt{x}&\mapsto&\mathsf{Num}\end{array}\right]\\\ \left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\ \mathtt{z}&\mapsto&\mathsf{Num}\\\ \mathtt{x}&\mapsto&\mathsf{Bool}\end{array}\right]\end{gathered}\right\\}$
$\left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\ \mathtt{z}&\mapsto&\mathsf{Num}\\\ \mathtt{x}&\mapsto&\mathsf{Num}\end{array}\right]\rightarrow\left\\{\begin{gathered}\left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\ \mathtt{z}&\mapsto&\mathsf{Num}\\\ \mathtt{x}&\mapsto&\mathsf{Num}\end{array}\right]\\\ \left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\ \mathtt{z}&\mapsto&\mathsf{Num}\\\ \mathtt{x}&\mapsto&\mathsf{Bool}\end{array}\right]\end{gathered}\right\\}$ | $\begin{gathered}\left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\ \mathtt{z}&\mapsto&\mathsf{Num}\\\ \mathtt{x}&\mapsto&\mathsf{Num}\end{array}\right]\rightarrow\left\\{\begin{gathered}\left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\ \mathtt{z}&\mapsto&\mathsf{Num}\\\ \mathtt{x}&\mapsto&\mathsf{Num}\end{array}\right]\\\ \left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\ \mathtt{z}&\mapsto&\mathsf{Num}\\\ \mathtt{x}&\mapsto&\mathsf{Bool}\end{array}\right]\end{gathered}\right\\}\\\ \left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\ \mathtt{z}&\mapsto&\mathsf{Num}\\\ \mathtt{x}&\mapsto&\mathsf{Bool}\end{array}\right]\rightarrow\left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\ \mathtt{z}&\mapsto&\mathsf{Num}\\\ \mathtt{x}&\mapsto&\mathsf{Bool}\end{array}\right]\end{gathered}$
$\begin{gathered}\left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\ \mathtt{z}&\mapsto&\mathsf{Num}\\\ \mathtt{x}&\mapsto&\mathsf{Num}\end{array}\right]\rightarrow\left\\{\begin{gathered}\left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\ \mathtt{z}&\mapsto&\mathsf{Num}\\\ \mathtt{x}&\mapsto&\mathsf{Num}\end{array}\right]\\\ \left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\ \mathtt{z}&\mapsto&\mathsf{Num}\\\ \mathtt{x}&\mapsto&\mathsf{Bool}\end{array}\right]\end{gathered}\right\\}\\\ \left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\ \mathtt{z}&\mapsto&\mathsf{Num}\\\ \mathtt{x}&\mapsto&\mathsf{Bool}\end{array}\right]\rightarrow\left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\ \mathtt{z}&\mapsto&\mathsf{Num}\\\ \mathtt{x}&\mapsto&\mathsf{Bool}\end{array}\right]\end{gathered}$ | $\begin{gathered}\left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\ \mathtt{z}&\mapsto&\mathsf{Num}\\\ \mathtt{x}&\mapsto&\mathsf{Num}\end{array}\right]\rightarrow\left\\{\begin{gathered}\left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\ \mathtt{z}&\mapsto&\mathsf{Num}\\\ \mathtt{x}&\mapsto&\mathsf{Num}\end{array}\right]\\\ \left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\ \mathtt{z}&\mapsto&\mathsf{Num}\\\ \mathtt{x}&\mapsto&\mathsf{Bool}\end{array}\right]\end{gathered}\right\\}\\\ \left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\ \mathtt{z}&\mapsto&\mathsf{Num}\\\ \mathtt{x}&\mapsto&\mathsf{Bool}\end{array}\right]\rightarrow\left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\ \mathtt{z}&\mapsto&\mathsf{Num}\\\ \mathtt{x}&\mapsto&\mathsf{Bool}\end{array}\right]\end{gathered}$

Implementation of this fixed point iteration can be found in the$\mathtt{fix}$
function in appendix A.4.

  * •

The resulting final states of the program is calculated to be
$\left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\
\mathtt{z}&\mapsto&\mathsf{Num}\\\
\mathtt{x}&\mapsto&\mathsf{Num}\end{array}\right],\left[\begin{array}[]{ccc}\mathtt{sum}&\mapsto&\mathsf{Num}\\\
\mathtt{z}&\mapsto&\mathsf{Num}\\\
\mathtt{x}&\mapsto&\mathsf{Bool}\end{array}\right]$

###  6.2 Function currying

We now introduce function currying to the SDTL language. Introduction of this
language feature allows the language to be flexible enough to express what
JavaScript programmers would do with lexical scoping.

######  Example 16 (Function currying).

We take a simple add function, and curry one argument to produce different
adders.

⬇

1function add(x,y) {

2 return x+y;

3}

4

5add5 = add(5);

6add7 = add(7);

7

8output add5(input) + add7(input);

If we were to write this in JavaScript, we could have written the following
for the same effect.

⬇

1function adder(toadd) {

2 return function(y) {

3 return toadd+y;

4 }

5}

6

7add5 = adder(5);

8add7 = adder(7);

9// suppose input is a platform-specific console input function

10console.log(add5(input()) + add7(input()));

The introduction of function currying does not change the syntax of the
language. Therefore, there is no inherent reason for changing semantic
functions. However, we do redefine the semantics of function calls to include
an eid as an input, for the reason explained below.

$\mathcal{E}\llbracket\left|L\left(\vec{E}\right)\right|_{e}\rrbracket=\mathcal{L}\
\llbracket L\rrbracket\Yright\lambda n.\mathtt{evalParams}\ \vec{E}\
\emptyset\Yright\lambda p.\mathtt{apply}\left(n,p,e\right)$

Here we introduce the $\mathtt{apply}$ function. It invokes the
$\mathtt{call}$ function when the function arguments are saturated, or it
returns a pointer to a curried function otherwise. Its type is as follows.

$\displaystyle\mathtt{apply}$ $\displaystyle:$ $\displaystyle
Value\rightarrow\left[Value\right]\rightarrow Eid\rightarrow M\ Value$

####  6.2.1 Concrete interpretation

We need to extend the definition of $FunPointer$ to hold curried parameters.
This means that the $\mathtt{fundecl}$ function also needs to be modified to
match the new type signature.

##### Domain

$FunPointer=Sid\times\left[Value\right]$

The initial program state is unchanged.

##### Functions

$\displaystyle\mathtt{apply}\left(\left\langle n,C\right\rangle,p,\\_\right)$
$\displaystyle=\lambda f.$
$\displaystyle\begin{cases}\mathtt{call}\left(n,C\smallfrown p\right)\
f&\mbox{if}\begin{gathered}\>\left\|C\smallfrown
p\right\|=\mathtt{arity}\left(f,n\right)\end{gathered}\\\
\lambda\rho.\left\\{\left\langle\rho,\left\langle n,C\smallfrown
p\right\rangle\right\rangle\right\\}\ &\mbox{otherwise}\end{cases}$
$\displaystyle\mathtt{fundecl}(id,n)$ $\displaystyle=$
$\displaystyle\bar{\Upsilon}_{Env}\ \lambda V.V\left[id\mapsto\left\langle
n,\emptyset\right\rangle\right]$

Here, $\left\|s\right\|$ is the length of a sequence $s$.

######  Example 17 (Concrete interpretation of a function currying).

Consider the program shown in example 16.

  * •

At line 1, we are presented with a function declaration. $\mathtt{fundecl}$
adds the identifier as a reference to a function pointer with no curried
value. Assuming $add$ has given a unique id of $1$ during the parsing of the
program, we have in environment $\left[\mathtt{add}\mapsto\left\langle
1,\emptyset\right\rangle\right]$.

  * •

At lines 5 and 7, we partially apply the $\mathtt{add}$ function. Since the
number of arguments is not saturated, $\mathtt{apply}\left(\left\langle
1,\emptyset\right\rangle,\left[5\right],\\_\right)$ gives $\left\langle
1,\left[5\right]\right\rangle$ for $\mathtt{add5}$. Similarly, $\mathtt{add7}$
gets $\left\langle 1,\left[7\right]\right\rangle$.

  * •

At line 8, we saturate the parameters, $\mathtt{apply}\left(\left\langle
1,\left[5\right]\right\rangle,\left[x\right],\\_\right)$ give
$\mathtt{call}\left(1,\left[5,x\right]\right)$, where $x$ is an arbitrary
number given from user input. Hence we have the addition done. It works
similarly for $\mathtt{add7}$.

####  6.2.2 Abstract interpretation

Note that curried functions introduce a possibility of creating closures
requiring an infinite number of arguments.

######  Example 18 (Currying loop).

Consider the following program.

⬇

1function foo(a,b) {

2 return a;

3}

4

5x = 0;

6while(true) {

7 x = foo(x);

8}

If we naively interpret this program, we would not be able to reach a fixed
point in analysis. Instead, we would have:

$\displaystyle\mathtt{x}$ $\displaystyle=$
$\displaystyle\mathtt{foo}\left(Num\right)$ $\displaystyle\mathtt{x}$
$\displaystyle=$
$\displaystyle\mathtt{foo}\left(\mathtt{foo}\left(Num\right)\right)$
$\displaystyle\mathtt{x}$ $\displaystyle=$
$\displaystyle\mathtt{foo}\left(\mathtt{foo}\left(\mathtt{foo}\left(Num\right)\right)\right)$
$\displaystyle\vdots$

A solution to this problem is to have a curried function anchored to a
particular language construct. In this case, we can use an eid of a curried
expression as a point of reference (or ’0’ if not curried).

##### Domain

$\displaystyle FunPointer$ $\displaystyle=$ $\displaystyle Sid\times
c\times\left(Eid\cup\left\\{0\right\\}\right)$ $\displaystyle Curried$
$\displaystyle=$ $\displaystyle Sid\times c\times
Eid\rightarrow\left[AVal\right]\ \mbox{where}\ c\mbox{ is a number of
parameters given}$ $\displaystyle AState$ $\displaystyle=$ $\displaystyle
AEnv\times Curried\times AReturn$

$Curried$ takes a function id, number of argument curried and the eid of a
calling site, and gives the list of curried values. The initial program state
is $\left\langle\emptyset,\emptyset,\mathsf{Void}\right\rangle$.

##### Functions

Definitions are given in figure 6.2

$\displaystyle\mathtt{apply}\left(\left\langle
n,c,e\right\rangle,p,e^{\prime}\right)$
$\displaystyle=\begin{cases}\Theta_{{\scriptscriptstyle Curried}}\
\lambda\nu.\underset{C\in\nu\left(n,c,e\right)}{\bigcup}\mathtt{call}\left(n,C\smallfrown
p\right)\ \mbox{if }c+\left\|p\right\|=\mathtt{{arity}\left(n\right)}\\\
\Psi_{{\scriptscriptstyle Curried}}\
\lambda\nu.\underset{C\in\nu\left(n,c,e\right)}{\bigcup}\left\langle\nu\left[\left\langle
n,c+\left\|p\right\|,e^{\prime}\right\rangle\mapsto\left(C\smallfrown
p\right)\right],\left\langle
n,c+\left\|p\right\|,e^{\prime}\right\rangle\right\rangle\
{\scriptstyle\mbox{otherwise}}\end{cases}$
$\displaystyle\mathtt{fundecl}\left(id,n\right)$
$\displaystyle=\bar{\Upsilon}_{AEnv}\
\lambda\sigma.\sigma\left[id\mapsto\left\langle n,0,0\right\rangle\right]$

Figure 6.2: Abstract functions for curried functions

######  Example 19 (Abstract interpretation of a currying loop).

The program shown in example 18 can be analysed as follows:

  * •

At line 1, $\mathtt{fundecl}\left(\mathtt{foo},1\right)$ gives
$\left[\mathtt{foo}\mapsto\left\langle 1,0,0\right\rangle\right]$, assuming
$1$ is a unique id given to the function.

  * •

At line 7, assuming the partial application expression has a unique id of 7,
$\mathtt{apply}\left(\left\langle
1,0,0\right\rangle,\left[\mathsf{Num}\right],7\right)$ gives
$\left[x\mapsto\left\langle 1,1,7\right\rangle\right]$ for environment and
$\left[\left\langle 1,1,7\right\rangle\mapsto\left[\mathsf{Num}\right]\right]$
for curried in the first iteration. Subsequently, we have
$\mathtt{apply}\left(\left\langle 1,0,0\right\rangle,\left\langle
1,1,7\right\rangle,7\right)$ gives $\left[x\mapsto\left\langle
1,1,7\right\rangle\right]$ for environment and $\left[\left\langle
1,1,7\right\rangle\mapsto\left[\left\langle 1,1,7\right\rangle\right]\right]$
for the list of curried value. Here we reach a fixed point.

  * •

All possible final states calculated by the interpretation are:

Environment | Curried
---|---
$x\mapsto\mathsf{Num}$ | None
$x\mapsto\left\langle 1,1,7\right\rangle$ | $\left\langle 1,1,7\right\rangle\mapsto\left[\mathsf{Num}\right]$
$x\mapsto\left\langle 1,1,7\right\rangle$ | $\left\langle 1,1,7\right\rangle\mapsto\left[\left\langle 1,1,7\right\rangle\right]$

###  6.3 Object oriented features

We now extend our language to support objects.

<Lexp> ::= <Exp> ‘.’ ID

<Exp> ::= ‘global’ | ‘this’ | ‘new’ <Lexp> ‘(’ [<Exp> [,<Exp>]*]? ‘)’

$\mathtt{global}$ is a reference to a global object, and the reference to
global object is program invariant (akin to ‘window’ in Client-side JavaScript
or ‘global’ in Node.js). $\mathtt{this}$ is the usual reference to the
receiver object of a method call.

As this extension introduces new syntactic structure, extra definitions for
semantic functions are given in figure 6.3. Note, however, that _existing
semantic equations are not impacted by this_.

$\displaystyle\mathcal{S}\llbracket E_{1}.id=E_{2}\rrbracket$ $\displaystyle=$
$\displaystyle\mathcal{E}\ \llbracket E_{1}\rrbracket\Yright\lambda
r.\mathcal{E}\ \llbracket E_{2}\rrbracket\Yright\lambda v.I_{S}\
\mathtt{set}\left(r,id,v\right)$
$\displaystyle\mathcal{E}\llbracket\mathtt{global}\rrbracket$ $\displaystyle=$
$\displaystyle I_{V}\ \mathtt{getglobal}$
$\displaystyle\mathcal{E}\llbracket\mathtt{this}\rrbracket$ $\displaystyle=$
$\displaystyle I_{V}\ \mathtt{getthis}$
$\displaystyle\mathcal{E}\llbracket\left|L\left(\vec{E}\right)\right|_{e}\rrbracket$
$\displaystyle=$ $\displaystyle\left(\begin{aligned} \mathcal{L}\ \llbracket
L\rrbracket&\Yright\lambda n.\\\ \left(\mathtt{evalParams}\ \vec{E}\
\emptyset\right)&\Yright\lambda p.\\\ I_{V}\ \mathtt{getthis}&\Yright\lambda
t.\\\ \mathtt{apply}\left(n,p,t,e\right)\end{aligned}\right)$
$\displaystyle\mathcal{E}\llbracket\left|\mathtt{new}\
L\left(\vec{E}\right)\right|_{e}\rrbracket$ $\displaystyle=$
$\displaystyle\left(\begin{aligned} \mathcal{L}\ \llbracket
L\rrbracket&\Yright\lambda n.\\\ \mathtt{evalParams}\ \vec{E}\
\emptyset&\Yright\lambda p.\\\ \mathtt{newobj}\left(e\right)&\Yright\lambda
m.\\\ \mathtt{apply}\left(n,p,m,e\right)&\Yright\lambda\\_.\\\ I_{A}\
m\end{aligned}\right)$
$\displaystyle\mathcal{E}\llbracket\left|E_{1}.id\left(\vec{E}\right)\right|_{e}\rrbracket$
$\displaystyle=$ $\displaystyle\left(\begin{aligned} \mathcal{E}\ \llbracket
E_{1}\rrbracket&\Yright\lambda t.\\\ I_{V}\ \mathtt{get}(t,id)&\Yright\lambda
n.\\\ \mathtt{evalParams}\ \vec{E}\ \emptyset&\Yright\lambda p.\\\
\mathtt{apply}\left(n,p,t,e\right)\end{aligned}\right)$
$\displaystyle\mathcal{L}\llbracket E_{1}.id\rrbracket$ $\displaystyle=$
$\displaystyle\mathcal{E}\ \llbracket E_{1}\rrbracket\Yright\lambda v.I_{V}\
\mathtt{get}\left(v,id\right)$

Figure 6.3: Semantic equations for the object-oriented extension of the
language

We redefine the $\mathtt{call}$ function to include receiver object reference,
and to account for side-effects that functions can have on object memories.

$\displaystyle\mathtt{call}$ $\displaystyle:$ $\displaystyle
Sid\rightarrow\left[Value\right]\rightarrow Value\rightarrow M\ Value$
$\displaystyle\mathtt{call}\left(n,p,t\right)$ $\displaystyle=$
$\displaystyle\lambda f\lambda\rho,\gamma.\Theta\
\left\langle\left\\{\mathtt{leave}\ \rho\ \rho^{\prime}\mid\rho^{\prime}\in
S\right\\},\gamma^{\prime}\right\rangle\ \mbox{where}\left\langle
S,\gamma^{\prime}\right\rangle=f\ n\ \left(\mathtt{enter}\ \rho\ n\ p\ t\
\mathtt{param}\left(f,n\right)\right)\ \gamma$

$\displaystyle\mathtt{enter}$ $\displaystyle:$ $\displaystyle State\rightarrow
Sid\rightarrow\left[Value\right]\rightarrow
Value\rightarrow\left[Id\right]\rightarrow State$
$\displaystyle\mathtt{leavel}$ $\displaystyle:$ $\displaystyle
State\rightarrow State\rightarrow State$

Note that by modelling function calls as an effect on a state, we can readily
model such concepts as mixins. In the $\mbox{JS}_{0}$ language [6, 7], mixin
creating behaviour is modelled in a functional language. A similar approach
has been taken in the discussion of the $\lambda_{S}$ language by Guha et al
[8]. However, with languages like JavaScript, it is in the nature of such a
language that functions are side-effect causing, and much of the type
operations are being done by the side-effects. Hence our deviation from a
purely functional approach to devise a model language that resembles a real-
life language.

####  6.3.1 Concrete interpretation

We extend the domain to include object memory (where object references are
mapped to a symbol mapping), and a reference to $\mathtt{this}$ object.

##### Domain

$\displaystyle Value$ $\displaystyle=$
$\displaystyle\mathbb{Z}\cup\left\\{\mathsf{true},\mathsf{false}\right\\}\cup
Object\cup FunPointer$ $\displaystyle Object$ $\displaystyle=$
$\displaystyle\mathbb{N}$ $\displaystyle ObjMem$ $\displaystyle=$
$\displaystyle n\rightarrow Env$ $\displaystyle This$ $\displaystyle=$
$\displaystyle Object$ $\displaystyle CState$ $\displaystyle=$ $\displaystyle
Env\times ObjMem\times This\times Return$

The initial program state is
$\left\langle\emptyset,\left\\{0\mapsto\emptyset\right\\},0,\mathsf{Void}\right\rangle$.
$0$ is a unique id referring to the global object.

##### Functions

We redefine $\mathtt{enter}$ and $\mathtt{leave}$ functions to allow passing
of a receiver object.

$\displaystyle\mathtt{enter}$ $\displaystyle=$
$\displaystyle\lambda\left\langle\\_,\Omega,\\_,\\_\right\rangle,n,P,T^{\prime}.\left\langle\left[\mathtt{param}\left(n\right)_{k}\mapsto
P_{k}\right],\Omega,T^{\prime},\mathsf{Void}\right\rangle$
$\displaystyle\mathtt{leave}$ $\displaystyle=$
$\displaystyle\lambda\left\langle
V,\\_,T,\\_\right\rangle,\left\langle\\_,\Omega^{\prime},\\_,r\right\rangle.\left\langle\left\langle
V,\Omega^{\prime},T,\mathsf{Void}\right\rangle,r\right\rangle$

The other functions are given in figure 6.4.

$\displaystyle\mathtt{get}\left(n,id\right)$ $\displaystyle=$
$\displaystyle\bar{\Theta}_{ObjMem}\
\left(\lambda\Omega.\Omega\left(n\right)\left(id\right)\right)$
$\displaystyle\mathtt{set}\left(n,id,v\right)$ $\displaystyle=$
$\displaystyle\bar{\Upsilon}_{ObjMem}\
\left(\lambda\Omega.\Omega\left[n\mapsto\Omega\left(n\right)\left[id\mapsto
v\right]\right]\right)$ $\displaystyle\mathtt{getglobal}$ $\displaystyle=$
$\displaystyle\bar{\Theta}_{ObjMem}\
\left(\lambda\Omega.\Omega\left(0\right)\right)$
$\displaystyle\mathtt{getthis}$ $\displaystyle=$
$\displaystyle\bar{\Theta}_{This}\ \left(\lambda T.T\right)$
$\displaystyle\mathtt{apply}\left(\left\langle
n,C\right\rangle,p,t,\\_\right)$ $\displaystyle=$
$\displaystyle\begin{cases}\mathtt{call}\left(n,C\smallfrown
p,t\right)&\mbox{if}\ \left\|C\smallfrown
p\right\|=\mathtt{arity}\left(n\right)\\\ \Gamma\
\left(\lambda\rho.\left\langle\rho,\left\langle n,C\smallfrown
p\right\rangle\right\rangle\right)&\mbox{otherwise}\end{cases}$
$\displaystyle\mathtt{newobj}\left(\\_\right)$ $\displaystyle=$
$\displaystyle\bar{\Psi}_{ObjMem}\
\left(\lambda\Omega.\left\langle\Omega\left[n\mapsto\emptyset\right],n\right\rangle\right)\
\mbox{where}\ n=\left\|\Omega\right\|$

Figure 6.4: Concrete functions for the object-oriented extension

######  Example 20 (Concrete analysis of objects).

Consider the following program.

⬇

1function Fruit(v) {

2 this.value = v;

3}

4

5function juicible(fruit, juice) {

6 function juiceMe(j,x) {

7 return this.value + j + x;

8 }

9 fruit.juice = juiceMe(juice);

10}

11

12apple = new Fruit(15);

13juicible(apple, 20);

14

15output apple.juice(10); # 15 + 20 + 10

  * •

Assume that $\mathtt{Fruit}$ has an id of 1, $\mathtt{juicible}$ has 2, and
$\mathtt{juiceMe}$ has 3.

  * •

Right before line 12, we have $\left[\mathtt{Fruit}\mapsto\left\langle
1,\emptyset\right\rangle,\mathtt{juicible}\mapsto\left\langle
2,\emptyset\right\rangle\right]$ . At line 12, the $\mathtt{new}$ expression
creates an object in object memory through $\mathtt{newobj}\left(\\_\right)$,
then passes it on as a receiver of a method call to $\mathtt{Fruit}$. Inside
the Fruit function, the new object gets the member value. After the line, we
have $Env=\left[\mathtt{Fruit}\mapsto\left\langle
1,\emptyset\right\rangle,\mathtt{juicible}\mapsto\left\langle
2,\emptyset\right\rangle,\mathtt{apple}\mapsto\mathsf{Obj}\ 1\right]$ and
$ObjMem=\left[1\mapsto\left[\mathtt{value}\mapsto 15\right]\right]$.

  * •

At line 13, $\mathtt{apply}\left(\left\langle
2,\emptyset\right\rangle,\left[\mathsf{Obj}\ 1,20\right],global,\\_\right)$
gives $\mathtt{call}\left(2,\left[\mathsf{Obj}\ 1,20\right],global\right)$.
Inside the juicible function, object memory is manipulated in line 9 to be
$\left[1\mapsto\left[\mathtt{value}\mapsto
15,\mathtt{juice}\mapsto\left\langle
3,\left[20\right]\right\rangle\right]\right]$.

  * •

At line 15, by the method call semantics, $\mathtt{apply}\left(\left\langle
3,\left[20\right]\right\rangle,\left[10\right],\mathsf{Obj}\ 1,\\_\right)$ is
invoked, which gives 45 as a final result.

####  6.3.2 Abstract interpretation

Similarly, we extend the abstract interpretation. Note that, whereas in a
concrete interpretation we generate a unique id for each of the objects
instantiated at run-time, in abstract interpretation we use a reference to the
allocation site of an object as a reference to a particular object, hence we
contain object memory in a finite domain.

##### Domain

$\displaystyle AObj$ $\displaystyle=$ $\displaystyle\left\\{0\right\\}\cup
Eid$ $\displaystyle AVal$ $\displaystyle=$
$\displaystyle\left\\{\mathsf{Num},\mathsf{Bool}\right\\}\cup AObj\cup
FunPointer$ $\displaystyle AObjMem$ $\displaystyle=$ $\displaystyle
AObj\rightarrow AEnv$ $\displaystyle AThis$ $\displaystyle=$ $\displaystyle
AObj$ $\displaystyle AState$ $\displaystyle=$ $\displaystyle AEnv\times
AObjMem\times AThis\times Curried\times AReturn$

The initial program state is
$\left\langle\emptyset,\left\\{0\mapsto\emptyset\right\\},0,\emptyset,\mathsf{Void}\right\rangle$.
$0$ is a unique id referring to the global object.

##### Functions

$\displaystyle\mathtt{enter}$ $\displaystyle=$
$\displaystyle\lambda\left\langle\\_,\alpha,\\_,\nu,\\_\right\rangle,n,P,\tau^{\prime}.\left\langle\left[\mathtt{param}\left(n\right)_{k}\mapsto
P_{k}\right],\alpha,\tau^{\prime},\nu,\mathsf{Void}\right\rangle$
$\displaystyle\mathtt{leave}$ $\displaystyle=$
$\displaystyle\lambda\left\langle\sigma,\\_,\tau,\\_,\\_\right\rangle,\left\langle\\_,\alpha^{\prime},\\_,\nu^{\prime},r\right\rangle.\left\langle\left\langle\sigma,\alpha^{\prime},\tau,\nu^{\prime},\mathsf{Void}\right\rangle,r\right\rangle$

Other functions are defined in figure 6.5.

$\displaystyle\mathtt{get}\left(n,id\right)$
$\displaystyle=\bar{\Theta}_{AObjMem}\ \lambda\alpha.\alpha\left(n\right)$
$\displaystyle\mathtt{set}\left(n,id,v\right)$
$\displaystyle=\bar{\Upsilon}_{AObjMem}\
\lambda\alpha.\alpha\left(n\right)\left[id\mapsto v\right]$
$\displaystyle\mathtt{obj}\left(j\right)$
$\displaystyle=\bar{\Theta}_{AObjMem}\ \lambda\alpha.\alpha\left(j\right)$
$\displaystyle\mathtt{getthis}$ $\displaystyle=\bar{\Theta}_{AThis}\
\lambda\tau.\tau$ $\displaystyle\mathtt{newobj}\left(n\right)$
$\displaystyle=\bar{\Psi}_{AObjMem}\
\lambda\alpha.\left\langle\alpha\left[n\mapsto\emptyset\right],n\right\rangle$
$\displaystyle\mathtt{apply}\left(\left\langle
n,c,e\right\rangle,p,t,e\right)$
$\displaystyle=\begin{cases}\Theta_{{\scriptscriptstyle Curried}}\
\lambda\nu.\underset{C\in\nu\left(n,c,e\right)}{\bigcup}\mathtt{call}\left(n,C\smallfrown
p,t\right)\ \mbox{if}\ c+\left\|p\right\|=\mathtt{arity}\left(n\right)\\\
\Psi_{{\scriptscriptstyle Curried}}\
\lambda\nu.\underset{C\in\nu\left(n,c,e\right)}{\bigcup}\left\langle\nu\left[\left\langle
n,c+\left\|p\right\|,e\right\rangle\mapsto C\smallfrown p\right],\left\langle
n,c+\left\|p\right\|,e\right\rangle\right\rangle&\mbox{otherwise}\end{cases}$

Figure 6.5: Abstract functions for the object-oriented extension

######  Example 21 (Abstract interpretation of objects).

The program in example 20 results in the following final state.

Environment | Object Memory | Curried
---|---|---
$\begin{aligned} \mathtt{Fruit}&\mapsto&\left\langle 1,0,0\right\rangle\\\ \mathtt{juicible}&\mapsto&\left\langle 2,0,0\right\rangle\\\ \mathtt{juiceMe}&\mapsto&\left\langle 3,0,0\right\rangle\\\ \mathtt{apple}&\mapsto&\mathsf{Obj}\ 1\end{aligned}$ | $\mathsf{Obj}\ 1\mapsto\left(\begin{aligned} \mathtt{value}&\mapsto&\mathsf{\mathsf{Num}}\\\ \mathtt{juice}&\mapsto&\left\langle 3,1,9\right\rangle\end{aligned}\right)$ | $\left\langle 3,1,9\right\rangle\mapsto\left[\mathsf{\mathsf{Num}}\right]$

Notice that as we add object oriented programming to the programming language,
the functions are now capable of causing side-effects. The following modified
example illustrates how the meaning of recursive function call is calculated
when the function causes side-effects.

######  Example 22 (Side-effect causing factorial function).

Consider the following modification of program analysed in example 14.

⬇

1function fact(f,n) {

2 if(n>1) { global.x=5; return f(f,n-1) * n; } else { return 1; }

3}

4

5z=fact(fact,input);

6output z;

  * •

At line 5, the meaning of the function call is calculated as follows. For
simplicity, we only record $AEnv,AObjMem$ and $AReturn$. The rest of the
components remain unchanged.

Current approximation | Meaning of function call | Note
---|---|---
$\emptyset$ | $\left\\{\left\langle\begin{gathered}\left[\mathtt{fact}\mapsto\mathsf{Function}\ 1\right],\\\ \left[0\mapsto\emptyset\right],\\\ \mathsf{\mathsf{Num}}\end{gathered}\right\rangle\right\\}$ |
$\left\\{\left\langle\begin{gathered}\left[\mathtt{fact}\mapsto\mathsf{Function}\ 1\right],\\\ \left[0\mapsto\emptyset\right],\\\ \mathsf{\mathsf{Num}}\end{gathered}\right\rangle\right\\}$ | $\left\\{\begin{gathered}\left\langle\begin{gathered}\left[\mathtt{fact}\mapsto\mathsf{Function}\ 1\right],\\\ \left[0\mapsto\emptyset\right],\\\ \mathsf{\mathsf{Num}}\end{gathered}\right\rangle,\\\ \left\langle\begin{gathered}\left[\mathtt{fact}\mapsto\mathsf{Function}\ 1\right],\\\ \left[0\mapsto\left[x\mapsto\mathsf{\mathsf{Num}}\right]\right],\\\ \mathsf{\mathsf{Num}}\end{gathered}\right\rangle\end{gathered}\right\\}$ |
$\left\\{\begin{gathered}\left\langle\begin{gathered}\left[\mathtt{fact}\mapsto\mathsf{Function}\ 1\right],\\\ \left[0\mapsto\emptyset\right],\\\ \mathsf{\mathsf{Num}}\end{gathered}\right\rangle,\\\ \left\langle\begin{gathered}\left[\mathtt{fact}\mapsto\mathsf{Function}\ 1\right],\\\ \left[0\mapsto\left[x\mapsto\mathsf{\mathsf{Num}}\right]\right],\\\ \mathsf{\mathsf{Num}}\end{gathered}\right\rangle\end{gathered}\right\\}$ | $\left\\{\begin{gathered}\left\langle\begin{gathered}\left[\mathtt{fact}\mapsto\mathsf{Function}\ 1\right],\\\ \left[0\mapsto\emptyset\right],\\\ \mathsf{\mathsf{Num}}\end{gathered}\right\rangle,\\\ \left\langle\begin{gathered}\left[\mathtt{fact}\mapsto\mathsf{Function}\ 1\right],\\\ \left[0\mapsto\left[x\mapsto\mathsf{\mathsf{Num}}\right]\right],\\\ \mathsf{\mathsf{Num}}\end{gathered}\right\rangle\end{gathered}\right\\}$ | Fixed point

###  6.4 Exception handling

As a final extension to SDTL, we introduce exception throwing and handling.
First, we introduce a familiar syntax for exception handling.

<Stm> ::= ‘try’ ‘’ <Stm> ‘’ ‘catch’ ‘(’ id ‘)’ ‘’ <Stm> ‘’ | ‘throw’ <Exp>

Following functions are the semantic functions for the newly introduced
syntax.

$\displaystyle\mathcal{S}\llbracket\mathtt{try}\ S_{1}\
\mathtt{catch}\left(id\right)\ S_{2}\rrbracket$ $\displaystyle=$
$\displaystyle\mathcal{S}\ \llbracket
S_{1}\rrbracket\Yright_{noesc}\mathtt{catch}\left(id,\mathcal{S}\ \llbracket
S_{2}\rrbracket\right)$ $\displaystyle\mathcal{S}\llbracket\mathtt{throw}\
E\rrbracket$ $\displaystyle=$ $\displaystyle\mathcal{E}\ \llbracket
E\rrbracket\Yright\lambda v.\mathtt{throw}\left(v\right)$

$\displaystyle\mathtt{throw}$ $\displaystyle:$ $\displaystyle Value\rightarrow
M\ Value$ $\displaystyle\mathtt{catch}$ $\displaystyle:$ $\displaystyle
Id\rightarrow M\ Value\rightarrow M\ Value$

Note that we cannot use $\Yright$ to combine the try code body and catch,
since the $\Yright$ operator has $\mathtt{esc}$ built into its definition,
which will terminate the program flow when the exception is raised. In order
to allow exception-raising transformations to flow through, we introduce a
non-escaping bind operator, $\Yright_{noesc}$. $\mathtt{catch}$ primitive
operator takes an exception variable name and the meaning of a catch code
block, and produces the meaning of a language construct in which an exception
is caught and handled.

######  Definition 23 (Non-escaping bind operator).

We define a non-escaping bind operator, $\Yright_{noesc}$

$\displaystyle\left(\Yright_{noesc}\right)$ $\displaystyle:$ $\displaystyle M\
a\rightarrow\left(a\cup\left\\{\mathsf{Null}\right\\}\rightarrow M\
a\right)\rightarrow M\ a$ $\displaystyle T\ \Yright_{noesc}\ U$
$\displaystyle=$ $\displaystyle\lambda f\lambda s.\>\mathbf{let}\ S=T\ f\ s\
\mathbf{in}\underset{\left\langle s^{\prime},a\right\rangle\in
S}{\bigcup}\left(U\ a\ f\ s^{\prime}\right)$

####  6.4.1 Concrete interpretation

As the control flow of the execution is abstracted out and parametrised as a
function $\mathtt{esc}$, it is not very surprising that introducing exceptions
to a program does not necessitate a heavy modification to the interpretation
of the language.

##### Domain

$\displaystyle Ex$ $\displaystyle=$ $\displaystyle
Value\cup\left\\{\mathsf{Void}\right\\}$ $\displaystyle CState$
$\displaystyle=$ $\displaystyle Env\times ObjMem\times This\times Return\times
Ex$

The initial program state is
$\left\langle\emptyset,\left\\{0\mapsto\emptyset\right\\},0,\mathsf{Void},\mathsf{Void}\right\rangle$.

##### Functions

$\displaystyle\mathtt{enter}$ $\displaystyle=$
$\displaystyle\lambda\left\langle\\_,\Omega,\\_,\\_,\\_\right\rangle,\left\langle
P,T^{\prime}\right\rangle,n.\left\langle\left[\mathtt{param}\left(n\right)_{k}\mapsto
P_{k}\right],\Omega,T^{\prime},\mathsf{Void},\mathsf{Void}\right\rangle$
$\displaystyle\mathtt{leave}$ $\displaystyle=$
$\displaystyle\lambda\left\langle
V,\\_,T,\\_,\\_\right\rangle,\left\langle\\_,\Omega^{\prime},\\_,r,e\right\rangle.\left\langle\left\langle
V,\Omega^{\prime},T,\mathsf{Void},e\right\rangle,r\right\rangle$

$\displaystyle\mathtt{esc}$ $\displaystyle=$ $\displaystyle\Theta_{Return,Ex}\
\lambda
R,E.\left(R\neq\mathsf{Void}\right)\wedge\left(E\neq\mathsf{Void}\right)$
$\displaystyle\mathtt{throw}\left(v\right)$ $\displaystyle=$
$\displaystyle\bar{\Upsilon}_{Ex}\ \lambda E.v$
$\displaystyle\mathtt{catch}\left(id,s\right)$ $\displaystyle=$
$\displaystyle\Theta_{Ex}\ \lambda
E.\begin{cases}I_{A}\mathsf{Unit}&\mbox{if}\ E=\mathsf{Void}\\\ \lambda f,r.s\
f\ \mathtt{exs}\left(\rho,id\right)&\mbox{otherwise}\end{cases}$
$\displaystyle\mathtt{exs}\left(id\right)$ $\displaystyle=$
$\displaystyle\Upsilon_{Env,Ex}\ \lambda V,E.\left\langle V\left[id\mapsto
E\right],\mathsf{Void}\right\rangle$

$\mathtt{exs}$ helps constructing an entering state to a catch block if an
exception was caught. As we do not support lexical scoping, an exception
variable enters a variable mapping as we enter the block.

######  Example 24 (Concrete interpretation of exception handling).

The following program illustrates exception handling in SDTL.

⬇

1x = input;

2try {

3 if(x<0) {

4 throw 0;

5 }

6 output x;

7 j = 3;

8} catch(e) {

9 output x;

10 output e;

11}

  * •

At line 3, we have $\left[\mathtt{x}\mapsto a\right]$ where $a$ is a user
input. Suppose $a$ is less than 0, then if leads to
$\mathtt{throw}\left(0\right)$ which gives $Ex:0$.

  * •

The resulting state is deemed to be an escaping state by $\mathtt{esc}$.
Hence, the code block of the try clause gives the resulting program state of
$\left\langle\left[x\mapsto
a\right],\left\\{0\mapsto\emptyset\right\\},0,\mathsf{Void},0\right\rangle$

  * •

With non-escaping binding to a $\mathtt{catch}$ primitive function afterwards,
catch yields the state with environment of $\left[x\mapsto a,e\mapsto
0\right]$ then it evaluates the catch clause, which outputs $a$ and $0$.

It is important that this exception handling does not interfere with other
control flow. The following example shows how it interacts with return state.

######  Example 25 (Function call, return and exception handling control
flow).

Consider the following example.

⬇

1function tryorerror(func, error, a) {

2 try {

3 return func(a);

4 } catch(e) {

5 return error;

6 }

7}

8

9function positive(a) {

10 if(a>0) { return a; }

11 throw 0;

12}

13

14gracefulpositive = tryorerror(positive, -1);

15

16function doandprint(func,a) {

17 output func(a);

18}

19

20try {

21 doandprint(positive,50);

22 doandprint(gracefulpositive,-50);

23 doandprint(positive,-50);

24} catch (e) {

25 output e;

26}

  * •

At line 3, when $\mathtt{tryorerror}$ is called from line 21, it sets a return
state with Void exception state. As $Ex$ is set to Void, the $\mathtt{catch}$
primitive operation does not interfere, and the control flow proceeds to
return the value of 50.

  * •

When called from line 22, the call to $\mathtt{positive}$ function sets an
exception state. Observe that, during the evaluation of the return statement,
if the exception is set while evaluating the returning expression, the control
flow does not proceed to set a return state. the $\mathtt{catch}$ primitive
operation notices exception state being set, and proceeds to evaluate the
exception handling block, which returns -1. The meaning of the whole try-catch
block, then, is evaluated to be setting a return state of -1.

  * •

Finally, when the exception throwing function $\mathtt{positive}$ is directly
called, at line 23, the exception state is set to be -50, and $\mathtt{catch}$
primitive operation proceeds to line 25, printing 0 to the output.

####  6.4.2 Abstract interpretation

Abstract definitions are largely similar to that of concrete ones. Notice that
we carry on modified exception state returned from a function call, thereby
allowing exception propagation.

##### Domain

$\displaystyle AEx$ $\displaystyle=$ $\displaystyle
AVal\cup\left\\{\mathsf{Void}\right\\}$ $\displaystyle AState$
$\displaystyle=$ $\displaystyle AEnv\times AObjMem\times AThisCurried\times
AReturn\times AEx$

The initial program state is
$\left\langle\emptyset,\left\\{0\mapsto\emptyset\right\\},0,\emptyset,\mathsf{Void},\mathsf{Void}\right\rangle$.

##### Functions

$\displaystyle\mathtt{enter}$ $\displaystyle=$
$\displaystyle\lambda\left\langle\\_,\alpha,\\_,\nu,\\_,\\_\right\rangle,\left\langle
P,\tau^{\prime}\right\rangle,n.\left\langle\left[\mathtt{param}\left(n\right)_{k}\mapsto
P_{k}\right],\alpha,\tau^{\prime},\nu,\mathsf{Void},\mathsf{Void}\right\rangle$
$\displaystyle\mathtt{leave}$ $\displaystyle=$
$\displaystyle\lambda\left\langle\sigma,\\_,\tau,\\_,\\_,\\_\right\rangle,\left\langle\\_,\alpha^{\prime},\\_,\nu^{\prime},r,e\right\rangle.\left\langle\left\langle\sigma,\alpha^{\prime},\tau,\nu^{\prime},\mathsf{Void},e\right\rangle,r\right\rangle$

$\displaystyle\mathtt{esc}$ $\displaystyle=$
$\displaystyle\Theta_{AReturn,AEx}\ \lambda
R,E.\left(R\neq\mathsf{Void}\right)\wedge\left(E\neq\mathsf{Void}\right)$
$\displaystyle\mathtt{throw}\left(v\right)$ $\displaystyle=$
$\displaystyle\bar{\Upsilon}_{AEx}\ \lambda E.v$
$\displaystyle\mathtt{catch}\left(id,s\right)$ $\displaystyle=$
$\displaystyle\Theta_{AEx}\ \lambda
E.\begin{cases}I_{A}\mathsf{Unit}&\mbox{if}\ E=\mathsf{Void}\\\ \lambda
f\lambda\eta.s\ f\
\mathtt{exs}\left(\eta,id\right)&\mbox{otherwise}\end{cases}$
$\displaystyle\mathtt{exs}\left(id\right)$ $\displaystyle=$
$\displaystyle\Upsilon_{AEnv,AEx}\
\lambda\sigma,E.\left\langle\sigma\left[id\mapsto
E\right],\mathsf{Void}\right\rangle$

######  Example 26 (Abstract interpretation of exception handling).

The program in example 24 can be abstractly interpreted as follows.

  * •

After lines 3-5, we have two possible states
$\left\langle\left[\mathtt{x}\mapsto\mathsf{Num}\right],\left\\{0\mapsto\emptyset\right\\},0,\emptyset,\mathsf{Void},\mathsf{Void}\right\rangle$
and
$\left\langle\left[\mathtt{x}\mapsto\mathsf{Num}\right],\left\\{0\mapsto\emptyset\right\\},0,\emptyset,\mathsf{Void},\mathsf{Num}\right\rangle$

  * •

By the bind operation, the latter state becomes the final state of the try
clause. The former state progresses further, and updates its environment to
$\left[\mathtt{x}\mapsto\mathsf{Num},\mathtt{j}\mapsto\mathsf{Num}\right]$

  * •

At line 8, the environment of exception throwing state is updated to be
$\left[\mathtt{x}\mapsto\mathsf{Num},\mathtt{e}\mapsto\mathsf{Num}\right]$,
then the catch clause is evaluated, which does not cause any state update.

  * •

The final states are
$\left\langle\left[\mathtt{x}\mapsto\mathsf{Num},\mathtt{j}\mapsto\mathsf{Num}\right],\left\\{0\mapsto\emptyset\right\\},0,\emptyset,\mathsf{Void},\mathsf{Void}\right\rangle$
and
$\left\langle\left[\mathtt{x}\mapsto\mathsf{Num},\mathtt{e}\mapsto\mathsf{Num}\right],\left\\{0\mapsto\emptyset\right\\},0,\emptyset,\mathsf{Void},\mathsf{Void}\right\rangle$

##  7 Well-definedness

All the functions appearing in both concrete and abstract versions of
interpretations are ordered point-wise. Recall that the bind operation
preserves the monotonicity when binding two monotonic functions. Observe that
all of the primitive operations that yield a state transformer, and the value-
returning operations lifted to yield one, are monotonic. This follows from the
fact that the domain of such transformers are ordered by identity. Then, it
follows that $\mathcal{S}$, $\mathcal{E}$ and $\mathcal{L}$ are monotonic for
any given $f\in F$.

Now, observe the monotonic relationship between $F$ and monadic functions.

######  Definition 27 (Point-wise ordering of function approximation).

Given $f,f^{\prime}\in F$, then $f\sqsubseteq f^{\prime}$ iff $\forall s\in
Sid,\forall\sigma\in State,\left(f\ s\ \sigma\right)\subseteq\left(f^{\prime}\
s\ \sigma\right)$

######  Theorem 28.

$\forall f,f^{\prime}\in F,f\sqsubseteq f^{\prime}\implies\forall
s\in\mathcal{S}\forall t\in Stm,\left(s\ t\ f\right)\sqsubseteq\left(s\ t\
f^{\prime}\right)$

###### Proof.

Clearly, the $\mathtt{call}$ auxiliary function is monotonic with regards to
the function approximation. The $\mathtt{call}$ function is the only function
for which the function approximation value is referenced. Recall the
preservation of monotonicity of bind operation. Then, this theorem immediately
follows. ∎

It follows from this theorem that there exists a least fixed point of the
meaning of function $f\in F$ for a particular program. Hence the well-
definedness of the fixed point of $F$ in a particular analysis, and that of
the semantics both in concrete and abstract interpretations.

##  8 Correctness

We define an abstraction relation $\succ$between concrete and abstract states.

###  8.1 Definition of correct abstraction

First, we define an abstraction between values and other components of the
states.

######  Definition 29.

$\mathsf{Num}\succ\mathbb{Z}$, $\mathsf{\mathsf{Bool}}\succ\mathbb{B}$,
$\mathsf{Void}\succ\mathsf{Void}$

######  Definition 30 (Abstraction of objects and symbol maps).

$\alpha,\Omega\vdash n\succ m$ if
$\alpha\left(n\right)\succ\Omega\left(m\right)$

$\sigma:AEnv\succ V:Env$ if $\forall id\in
dom\left(V\right),\sigma\left(id\right)\succ V\left(id\right)$

######  Definition 31 (Function pointers).

$C:Curried\vdash\left\langle n,c,e\right\rangle\succ\left\langle
m,P\right\rangle$ if $n=m$, $c=\left\|P\right\|$
and $\exists A\in C\left(n,c,e\right),A_{k}\succ P_{k}$ for $1\leq k\leq c$

Now we are ready to define an abstraction between concrete and abstract
states.

######  Definition 32 (Abstraction relation).

Given

$\rho=\left(\begin{gathered}V:Env,\Omega:ObjMem,T:This,R:Return,E:Ex\end{gathered}\right)\in
CState$

$\eta=\left(\begin{gathered}\sigma:AEnv,\alpha:AObjMem,\tau:AThis,C:Curried,r:AReturn,e:AEx\end{gathered}\right)\in
AState$

$\eta\succ\rho$ if $\left(\sigma\succ V\right)\wedge\left(\forall m\in
dom\left(\Omega\right)\exists n\in
dom\left(\alpha\right),\alpha\left(n\right)\succ\Omega\left(m\right)\right)\wedge\left(\tau\succ
T\wedge r\succ R\wedge e\succ E\right)$

######  Definition 33 (Abstraction between powersets).

Given an abstract value $a$, a concrete value $c$,
$p\in\wp\left(AState\times a\right)\mbox{ and }q\in\wp\left(CState\times
c\right),p\succ q$ if

$\forall\rho\in q\exists\eta\in
p,\left(\eta\succ\rho\right)\wedge\left(\rho,\eta\vdash a\succ c\right)$

###  8.2 Morphism

First, we observe that the bind operation preserves morphisms of the functions

######  Definition 34.

A pair of functions$\left\langle F,F^{\prime}\right\rangle$ shows a morphism
over $\succ$ if the following condition is met

$a\succ b\implies F^{\prime}\left(a\right)\succ F\left(b\right)$

######  Theorem 35.

If $\left\langle F,F^{\prime}\right\rangle$ and $\left\langle
G,G^{\prime}\right\rangle$ are pairs of functions that show a morphism over
$\succ$, then $\left\langle F\Yright G,F^{\prime}\Yright
G^{\prime}\right\rangle$ is also such pair.

###### Proof.

$\forall\rho\in CState$, let $p=F\left(\rho\right)$,$p^{\prime}=F\Yright
G\left(\rho\right)$, $\eta\in AState\mbox{ such that
}\eta\succ\rho,$$q=F^{\prime}\left(\eta\right)$,$q^{\prime}=F^{\prime}\Yright
G^{\prime}\left(\eta\right)$.
Then, $\forall p_{1}\in p,$

  1. 1.

when $\mathtt{esc}\left(p_{1}\right)$ is true, then the morphism and $\succ$
relation imply that $\exists q_{1}\in q,\mathtt{esc}\left(q_{1}\right)$. Given
the definition of $\Yright$ operation, $p_{1}$ and $q_{1}$are also elements of
$p^{\prime}$ and $q^{\prime}$.

  2. 2.

otherwise, morphism of $\left\langle G,G^{\prime}\right\rangle$ gives that
$\forall p_{2}\in G\left(p_{1}\right)\exists q_{2}\in
G^{\prime}\left(q_{1}\right)\mbox{ such that }q_{2}\succ p_{2}$. Such entities
also exist in $q^{\prime}$.

∎

Finally, we observe that operations resulting from abstract functions and
their corresponding concrete functions form such a morphism over $\succ$. We
omit function-by-function proof, as such proof would be a mechanical exercise.

##  9 Conclusion and future direction

As we have noted in the introduction, this work is a snapshot of an ongoing
dialogue between theory and practice, positively informing each other to
gradually move towards a better theorisation (and practical implementation) of
the difficult task of analysing dynamic languages. We have sought to
modularise the theoretical framework so that we can take an incremental
approach. We anticipate that, as a result of having such a theory, adding new
features to the current model language while maintaining formality and rigour
will be considerably less laborious than to invent a new incarnation of a more
feature-complete model language and produce theory for it.

## References

  * [1] H. R. Nielson and F. Nielson, _Semantics with applications: a formal introduction_. New York, NY, USA: John Wiley & Sons, Inc., 1992.
  * [2] S. Liang, “Modular monadic semantics and compilation,” Ph.D. dissertation, Yale University, 1998.
  * [3] S. Liang and P. Hudak, “Modular denotational semantics for compiler construction,” in _Proceedings of the Sixth European Symposium on Programming (ESOP’96)_ , ser. Lecture Notes in Computer Science, H. R. Nielson, Ed., vol. 1058. Springer, 1996, pp. 219–234.
  * [4] P. D. Mosses, “Theory and practice of action semantics,” in _Proceedings of the 21st International Symposium on Mathematical Foundations of Computer Science (MFCS’96)_ , ser. Lecture Notes in Computer Science, W. Penczek and A. Szalas, Eds., vol. 1113. Springer, 1996, pp. 37–61.
  * [5] P. Wadler, “Theorems for free!” in _Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture (FPCA’89)_. New York, NY, USA: ACM Press, 1989, pp. 347–359. [Online]. Available: http://doi.acm.org/10.1145/99370.99404
  * [6] C. Anderson, S. Drossopoulou, and P. Giannini, “Towards type inference for JavaScript,” in _Proceedings of the 19th European Conference on Object-Oriented Programming (ECOOP 2005)_ , ser. Lecture Notes in Computer Science, A. P. Black, Ed., vol. 3586. Springer, 2005, pp. 428–452.
  * [7] C. Anderson and P. Giannini, “Type checking for JavaScript,” _Electronic Notes in Theoretical Computer Science_ , vol. 138, no. 2, pp. 37–58, 2005.
  * [8] A. Guha, C. Saftoiu, and S. Krishnamurthi, “Typing local control and state using flow analysis,” in _Programming Languages and Systems: Proceedings of the 20th European Symposium on Programming_ , ser. Lecture Notes in Computer Science, G. Barthe, Ed., vol. 6602. Springer, 2011, pp. 256–275.
  * [9] T. Wrigstad, F. Z. Nardelli, S. Lebresne, J. Östlund, and J. Vitek, “Integrating typed and untyped code in a scripting language,” in _Proceedings of the 37th Annual ACM Symposium on Principles of Programming Languages (POPL 2010)_. ACM Press, 2010, pp. 377–388.
  * [10] D. Ancona, M. Ancona, A. Cuni, and N. D. Matsakis, “RPython: A step towards reconciling dynamically and statically typed OO languages,” in _Proceedings of the 2007 Symposium on Dynamic Languages (DLS’07)_. New York, NY, USA: ACM Press, 2007, pp. 53–64. [Online]. Available: http://doi.acm.org/10.1145/1297081.1297091
  * [11] M. Dufour, “Shed Skin: An optimizing Python-to-C++ compiler,” Master’s thesis, Delft University of Technology, the Netherlands, 2006.
  * [12] G. Bracha and W. Cook, “Mixin-based inheritance,” _SIGPLAN Notices_ , vol. 25, no. 10, pp. 303–311, 1990. [Online]. Available: http://doi.acm.org/10.1145/97946.97982
  * [13] K. Mens, K. De Volder, and T. Mens, “A formalisation of encapsulated modification of objects,” Vrije Universiteit Brussel, Faculteit Wetenschappen, Tech. Rep. vub-prog-tr-96-06, 1996.
  * [14] S. H. Jensen, A. Møller, and P. Thiemann, “Type analysis for JavaScript,” in _Static Analysis: Proceedings of the 16th International Symposium_ , ser. Lecture Notes in Computer Science, J. Palsberg and Z. Su, Eds., vol. 5673. Springer, 2009, pp. 238–255.

##  Appendix A Haskell Implementation

###  A.1 Syntax parser

Creates an augmented syntax tree with unique id numbers.

⬇

{

module Sdtl where

import Data.Char

import Control.Monad.State

import Data.Map

}

%name sdtl

%tokentype { Token }

%token

if {TokenIf}

else {TokenElse}

while {TokenWhile}

input {TokenInput}

output {TokenOutput}

new {TokenNew}

this {TokenThis}

function {TokenFunction}

return {TokenReturn}

true {TokenTrue}

false {TokenFalse}

global {TokenGlobal}

try {TokenTry}

catch {TokenCatch}

throw {TokenThrow}

id {TokenId $$}

’=’ {TokenAsg}

’+’ {TokenPlus}

’-’ {TokenMinus}

’*’ {TokenMult}

’/’ {TokenDiv}

gt {TokenGreaterThan}

lt {TokenLessThan}

eq {TokenEqual}

’(’ {TokenLP}

’)’ {TokenRP}

’{’ {TokenLC}

’}’ {TokenRC}

’;’ {TokenScol}

’.’ {TokenDot}

’,’ {TokenComma}

number {TokenNumber $$}

%nonassoc gt lt eq

%left ’+’ ’-’

%left ’*’ ’/’

%monad {P}

%%

Program :: { SdtlProgram }

Program : Stmts {% state $ \\(s0, m0) -> (SdtlProgram $1 m0, (s0,m0)) }

Stmts :: { AStmt }

Stmts : Stmts AStmt {% augStmt $ Stmts $1 $2}

| {% augStmt Empty}

AStmt :: { AStmt }

ASTmt : Stmt {% augStmt $1}

Cblock :: { AStmt }

Cblock : ’{’ Stmts ’}’ { $2 }

| Stmt {% augStmt $1 }

Stmt :: {Stmt}

Stmt : AExpr ’;’ {Expr $1}

| Lexpr ’=’ AExpr ’;’ {Asg $1 $3}

| if ’(’ AExpr ’)’ Cblock else Cblock {Ite $3 $5 $7}

| if ’(’ AExpr ’)’ Cblock {If $3 $5}

| while ’(’ AExpr ’)’ Cblock {While $3 $5}

| output AExpr ’;’ {Output $2}

| return AExpr ’;’ {Return $2}

| function id ’(’ Idlist ’)’ Cblock {Function $2 $4 $6}

| try Cblock catch ’(’ id ’)’ Cblock {TryCatch $2 $5 $7}

| throw AExpr ’;’ {Throw $2}

Params :: {[AExpr]}

Params : {[]}

| AExpr {[$1]}

| AExpr ’,’ Params {$1:$3}

Idlist :: {[String]}

Idlist : {[]}

| id {[$1]}

| id ’,’ Idlist {$1:$3}

AExpr :: {AExpr}

AExpr : Expr {% augExpr $1}

Expr :: {Expr}

Expr : Lexpr {Lexpr $1}

| true {Boolean True}

| false {Boolean False}

| number {Number $1}

| AExpr ’+’ AExpr {Binop Plus $1 $3}

| AExpr ’-’ AExpr {Binop Minus $1 $3}

| AExpr ’*’ AExpr {Binop Mult $1 $3}

| AExpr ’/’ AExpr {Binop Div $1 $3}

| AExpr gt AExpr {Binop GreaterThan $1 $3}

| AExpr lt AExpr {Binop LessThan $1 $3}

| AExpr eq AExpr {Binop Equal $1 $3}

| input {Input}

| new AExpr {New $2}

| Lexpr ’(’ Params ’)’ {Call $1 $3}

| ’(’ Expr ’)’ {$2}

| this {This}

| global {Global}

Lexpr :: {Lexpr}

Lexpr : ’(’ Lexpr ’)’ {$2}

| AExpr ’.’ id {Ref $1 $3}

| id {Id $1}

{

type Sid = Int

type Eid = Int

data SdtlProgram = SdtlProgram AStmt (Map Int AStmt) deriving (Show)

data Lexpr =

Ref AExpr String

| Id String

deriving Show

data Op = Plus | Minus | Mult | Div | GreaterThan | LessThan | Equal

deriving Show

data AExpr = AExpr Expr Eid deriving Show

data Expr =

Lexpr Lexpr

| Boolean Bool

| Number Int

| Binop Op AExpr AExpr

| Input

| New AExpr

| Call Lexpr [AExpr]

| This

| Global

deriving Show

data AStmt =

AStmt Stmt Sid

deriving Show

data Stmt =

Asg Lexpr AExpr

| Ite AExpr AStmt AStmt

| If AExpr AStmt

| While AExpr AStmt

| Output AExpr

| Expr AExpr

| Return AExpr

| Function String [String] AStmt

| TryCatch AStmt String AStmt

| Empty

| Stmts AStmt AStmt

| Throw AExpr

deriving Show

data Token =

TokenIf

| TokenElse

| TokenWhile

| TokenInput

| TokenOutput

| TokenNew

| TokenThis

| TokenFunction

| TokenReturn

| TokenTrue

| TokenFalse

| TokenGlobal

| TokenId String

| TokenAsg

| TokenPlus

| TokenMinus

| TokenMult

| TokenDiv

| TokenGreaterThan

| TokenLessThan

| TokenEqual

| TokenLP

| TokenRP

| TokenLC

| TokenRC

| TokenScol

| TokenDot

| TokenComma

| TokenNumber Int

| TokenTry

| TokenCatch

| TokenThrow

deriving Show

type P = State (Int, Map Int AStmt)

augStmt :: Stmt -> P AStmt

augStmt s = state $ \\(s0, m0) -> let news = AStmt s s0 in (news, (s0+1,
insert s0 news m0 ))

augExpr :: Expr -> P AExpr

augExpr e = state $ \\(s0, m0) -> (AExpr e s0, (s0+1, m0))

lexer :: String -> [Token]

lexer s = lexer1 s

lexer1 :: String -> [Token]

lexer1 [] = []

lexer1 (c:cs)

| isSpace c = lexer1 cs

| c == ’\t’ = lexer1 cs

| c == ’\r’ = lexer1 cs

| c == ’\n’ = lexer1 cs

| isAlpha c = lexVar (c:cs)

| isDigit c = lexNum (c:cs)

| c == ’-’ = lexNegativeNum (cs)

| c == ’#’ = lexer1 (dropWhile (/= ’\n’) cs)

lexer1 (’=’:cs) =

case cs of

(’=’:ss) -> TokenEqual : lexer1 ss

_ -> TokenAsg : lexer1 cs

lexer1 (’+’:cs) = TokenPlus : lexer1 cs

lexer1 (’-’:cs) = TokenMinus : lexer1 cs

lexer1 (’*’:cs) = TokenMult : lexer1 cs

lexer1 (’/’:cs) = TokenDiv : lexer1 cs

lexer1 (’(’:cs) = TokenLP : lexer1 cs

lexer1 (’)’:cs) = TokenRP : lexer1 cs

lexer1 (’{’:cs) = TokenLC : lexer1 cs

lexer1 (’}’:cs) = TokenRC : lexer1 cs

lexer1 (’.’:cs) = TokenDot : lexer1 cs

lexer1 (’;’:cs) = TokenScol : lexer1 cs

lexer1 (’>’:cs) = TokenGreaterThan : lexer1 cs

lexer1 (’<’:cs) = TokenLessThan : lexer1 cs

lexer1 (’,’:cs) = TokenComma : lexer1 cs

lexNum cs = TokenNumber (read num) : lexer1 rest

where (num,rest) = span isDigit cs

lexNegativeNum cs = TokenNumber (-1 * (read num)) : lexer1 rest

where (num,rest) = span isDigit cs

lexVar cs =

case span isAlphaNum cs of

("if", rest) -> TokenIf : lexer1 rest

("else", rest) -> TokenElse : lexer1 rest

("while", rest) -> TokenWhile : lexer1 rest

("input", rest) -> TokenInput : lexer1 rest

("output", rest) -> TokenOutput : lexer1 rest

("new", rest) -> TokenNew : lexer1 rest

("this", rest) -> TokenThis : lexer1 rest

("function", rest) -> TokenFunction : lexer1 rest

("return", rest) -> TokenReturn : lexer1 rest

("true", rest) -> TokenTrue : lexer1 rest

("false", rest) -> TokenFalse : lexer1 rest

("global", rest) -> TokenGlobal : lexer1 rest

("try", rest) -> TokenTry : lexer1 rest

("catch", rest) -> TokenCatch : lexer1 rest

("throw", rest) -> TokenThrow : lexer1 rest

(var, rest) -> TokenId var : lexer1 rest

happyError :: [Token] -> a

happyError _ = error "Parse␣error"

}

###  A.2 Semantic functions

⬇

{-# LANGUAGE GADTs, MultiParamTypeClasses #-}

module SemanticFunctions where

import Data.Maybe as Maybe

import Sdtl

import Data.Map as Map

import Debug.Trace

class (Eq v) => Value v where

conval :: Expr -> v

getSid :: v -> Sid

binop :: Op -> v -> v -> v

class (Eq s) => State s where

fundecl :: String -> [String] -> Sid -> s -> [s]

esc :: s -> Bool

class (State s, Value v) => StateValue s v where

ret :: v -> s -> [s]

cond :: (Eq a) => v -> (M s v a) -> (M s v a) -> (M s v a)

asg :: String -> v -> s -> [s]

dooutput :: v -> s -> [s]

getinput :: s -> [(s,v)]

val :: s -> String -> v

enter :: s -> Sid -> [v] -> v -> [String] -> s

leave :: s -> s -> (s, Maybe v)

fix :: ((M s v ()) -> (M s v ())) -> M s v ()

apply :: v -> [v] -> v -> Eid -> (M s v v)

set :: v -> String -> v -> s -> [s]

get :: v -> String -> s -> v

getglobal :: s -> v

getthis :: s -> v

newobj :: Eid -> (M s v v)

runthrow :: v -> s -> [s]

runcatch :: String -> (M s v ()) -> (M s v ())

data M s v a where

M :: (State s, Value v) => ((Sid -> (AStmt, (M s v ()))) -> s -> [(s,Maybe
a)]) -> M s v a

\--data (State s) => M s a = M (F s -> s -> [(s,Maybe a)])

instance (StateValue s v) => Monad (M s v) where

(M t) >>= u =

M $ (\f -> \s0 ->

let ss = t f s0

in

concat [ if esc s1 then [(s1, Nothing)]

else let

Just a’ = a

(M us) = u a’

in us f s1

| (s1, a) <- ss ])

return a = M $ \f -> \s0 -> [(s0, Just a)]

(>>>) :: (StateValue s v) => (M s v a) -> (Maybe a -> (M s v a)) -> (M s v a)

(M t) >>> u = M $ (\f -> \s0 ->

let ss = t f s0 in concat [ let (M us) = u a in us f s1 | (s1, a) <- ss ])

{- Takes a state transformer and transforms into a monad -}

liftS :: (StateValue s v) => (s -> [s]) -> M s v ()

liftS strans = M $ \f -> \s0 -> [(s1,Just ()) | s1 <- (strans s0)]

liftV :: (State s, Value v) => (s -> v) -> M s v v

liftV stov = M $ \f -> \s -> [(s, Just (stov s))]

getState :: (State s, Value v) => M s v s

getState = M $ \f -> \s0 -> [(s0,Just s0)]

sstmt :: (StateValue s v) => AStmt -> M s v ()

sstmt (AStmt Empty sid) = return ()

sstmt (AStmt (Stmts s1 s2) sid) = do

traceShow s1 $ sstmt s1

traceShow s2 $ sstmt s2

sstmt (AStmt (Expr e1) sid) = do

sexpr e1

return ()

sstmt (AStmt (Return e1) sid) = do

v <- sexpr e1

liftS $ ret v

sstmt (AStmt (If e1 s1) sid) = do

v <- sexpr e1

cond v (sstmt s1) (return ())

sstmt (AStmt (Ite e1 s1 s2) sid) = do

v <- sexpr e1

cond v (sstmt s1) (sstmt s2)

sstmt (AStmt (Asg (Id i1) e1) sid) = do

v <- sexpr e1

liftS $ asg i1 v

sstmt (AStmt (While e1 s1) sid) = fix $ \x -> do

v <- sexpr e1

cond v (sstmt s1 >> x) (return ())

sstmt (AStmt (Output e1) sid) = do

v <- sexpr e1

liftS $ dooutput v

sstmt (AStmt (Function id1 ids (AStmt _ s1)) sid) = liftS $ fundecl id1 ids
sid

sstmt (AStmt (Asg (Ref e1 id1) e2) sid) = do

r <- sexpr e1

v <- sexpr e2

liftS $ set r id1 v

sstmt (AStmt (TryCatch s1 id1 s2) sid) =

(sstmt s1) >>> \\_ -> runcatch id1 (sstmt s2)

sstmt (AStmt (Throw e1) sid) = do

v1 <- sexpr e1

liftS $ runthrow v1

sexpr :: (StateValue s v) => AExpr -> M s v v

sexpr (AExpr (Number n) eid) = return $ conval (Number n)

sexpr (AExpr (Boolean b) eid) = return $ conval (Boolean b)

sexpr (AExpr (Lexpr l1) eid) = slexpr l1

sexpr (AExpr Input eid) = M $ \f -> \s0 -> [(s, Just v) | (s,v) <- getinput s0]

sexpr (AExpr (Call (Ref e1 id1) es) eid) = do

t <- sexpr e1

n <- liftV $ get t id1

p <- evalParams es []

apply n p t eid

sexpr (AExpr (Call l1 es) eid) = do

n <- slexpr l1

p <- evalParams es []

t <- liftV $ getthis

apply n p t eid

sexpr (AExpr (Binop op e1 e2) eid) = do

v1 <- sexpr e1

v2 <- sexpr e2

return $ binop op v1 v2

sexpr (AExpr This eid) = liftV $ getthis

sexpr (AExpr Global eid) = liftV $ getglobal

sexpr (AExpr (New (AExpr (Call l1 es) eid1)) eid) = do

n <- slexpr l1

p <- evalParams es []

m <- newobj eid

apply n p m eid

return m

evalParams :: (StateValue s v) => [AExpr] -> [v] -> M s v [v]

evalParams [] vs = return vs

evalParams (e:es) vs = do

v <- sexpr e

evalParams es (vs ++ [v])

slexpr :: (StateValue s v) => Lexpr -> M s v v

slexpr (Id id1) = do

s0 <- getState

return $ val s0 id1

slexpr (Ref e1 id1) = do

v <- sexpr e1

liftV $ get v id1

\--putState :: (StateValue s v) => s -> (M s v ())

\--putState s = M $ \f -> \s0 -> [(s,Just ())]

\--getFunc :: (StateValue s v) => M s v (Sid -> (M s v ()))

\--getFunc = M $ \f -> \s -> [(s, Just f)]

call :: (StateValue s v) => Sid -> [v] -> v -> (M s v v)

call n p t = M $ \f -> \s0 ->

[leave s0 s | (s,_) <- let (AStmt (Function _ ids _) _, M x) = (f n) in x f (enter s0 n p t ids) ]

runMonad :: (StateValue s v) => AStmt -> (Sid -> (AStmt, (M s v ()))) -> s ->
v -> [s]

runMonad mainStmt = \f -> \s0 -> \\_ -> let M t = sstmt mainStmt in
(Prelude.map) fst (t f s0)

params :: (Sid -> (AStmt, (M s v ()))) -> Sid -> [String]

params f sid = let ((AStmt (Function _ ids _) _), _) = (f sid) in ids

arity :: (Sid -> (AStmt, (M s v ()))) -> Sid -> Int

arity f sid = length (params f sid)-}-}

###  A.3 Concrete interpretation

⬇

{-# LANGUAGE MagicHash, UnboxedTuples, GADTs, MultiParamTypeClasses #-}

module Main (main, runString) where

import SemanticFunctions

import Sdtl

import Data.Map

import qualified Control.Exception as E

import GHC.IO

import GHC.Exts

import System.Environment

import qualified Control.Monad.State as S

import System.IO.Unsafe

import Data.ByteString.Internal

import Debug.Trace

{-

fromState :: State# RealWorld -> RealWorld

fromState = unsafeCoerce#

toState :: RealWorld -> State# RealWorld

toState = unsafeCoerce#

execIO :: IO a -> RealWorld -> (RealWorld, a)

execIO (IO k) = \w -> case k (toState w) of (# s’, x #) -> (fromState s’, x)

-}

data CValue = Intval Int

| Boolval Bool

| FunPointer Sid [CValue]

| Object Int

deriving (Show, Eq)

instance Value CValue where

conval (Boolean True) = Boolval True

conval (Boolean False) = Boolval False

conval (Number i) = Intval i

getSid (FunPointer n []) = n

binop Plus (Intval i1) (Intval i2) = Intval $ i1 + i2

binop Minus (Intval i1) (Intval i2) = Intval $ i1 - i2

binop Mult (Intval i1) (Intval i2) = Intval $ i1 * i2

binop Div (Intval i1) (Intval i2) = Intval $ i1 ‘div‘ i2

binop GreaterThan (Intval i1) (Intval i2) = Boolval $ i1 > i2

binop LessThan (Intval i1) (Intval i2) = Boolval $ i1 < i2

binop Equal (Intval i1) (Intval i2) = Boolval $ i1 == i2

data CState = CState{

env :: Map String CValue,

\--io :: RealWorld,

objmem :: Map Int (Map String CValue),

returning :: Maybe CValue,

exception :: Maybe CValue,

this :: CValue

} deriving (Show)

instance Eq CState where

(==) _ _ = False

instance State (CState) where

esc (CState {returning = v, exception = e}) = case v of

Nothing -> case e of

Nothing -> False

_ -> True

_ -> True

\--fundecl :: String -> [String] -> Sid -> s -> [s]

fundecl fnname fnparams n s =

[s {env = insert fnname (FunPointer n []) (env s) }]

instance StateValue CState CValue where

ret v s = trace (show s) $ [s {returning = Just v}]

\--cond :: (CValue v) => v -> (M s v a) -> (M s v a) -> (M s v a)

cond (Boolval True) t u = t

cond _ t u = u

\--asg :: (CValue v) => String -> v -> s -> [s]

asg i v s = [s {env = (insert i v (env s))}]

\--dooutput :: (CValue v) => v -> s -> [s]

dooutput (Intval n) s =

\--let (io1, _) = (execIO $ putStrLn (show n)) (io s)

\--in [s {io = io1}]

let v = ($!) inlinePerformIO $ putStrLn (show n) in

if v == () then [s] else [s]

\--getinput :: (CValue v) => s -> [(s,v)]

getinput s =

\--let (io1, v) = (execIO $ getLine) (io s)

\--in [(s {io = io1}, Intval (read v))]

[(s,Intval (read (inlinePerformIO $ getLine)))]

\--val :: (CValue v) => s -> String -> v

val s i = (env s) ! i

\--enter :: (CValue v) => s -> Sid -> [v] -> s

enter s n vs t ids = s {env = fromList (zip ids vs), this = t}

\--leave :: (CValue v) => s -> s -> (s, Maybe v)

leave s0 s = trace (show s) $

(CState {env = (env s0), {-io = (io s), -}

returning = Nothing,

exception = (exception s),

objmem = (objmem s),

this = (this s0)}, (returning s))

fix x = x (fix x)

apply (FunPointer n c) p t _ =

M $ \f -> \s ->

if (arity f n) == (length (c ++ p))

then let (M tcall) = call n (c ++ p) t in (tcall f s)

else [(s, Just (FunPointer n (c++p)))]

set (Object n) id1 v = \s ->

let oldo = (objmem s) ! n

in [s {objmem = insert n (insert id1 v oldo) (objmem s)}]

get (Object n) id1 = \s -> (objmem s) ! n ! id1

getglobal = \s -> (Object 0)

getthis = \s -> (this s)

newobj _ = M $ \f -> \s ->

let newn = size (objmem s)

in

traceShow (Object newn) $

[(s {objmem = insert newn (fromList []) (objmem s)}, Just (Object newn))]

\--runthrow :: v -> s -> [s]

runthrow v = \s -> [s {exception=Just v}]

\--runcatch :: String -> (M s v ()) -> (M s v ())

runcatch id1 (M u) = M $ \f -> \s0 ->

case (exception s0) of

Nothing -> [(s0, Just ())]

Just v -> (u f (s0 {env = insert id1 v (env s0), exception=Nothing}))

{-

getWorld :: IO RealWorld

getWorld = IO (\s -> (# s, fromState s #))

putWorld :: RealWorld -> IO ()

putWorld s’ = IO (\\_ -> (# toState s’, () #))

-}

fun :: (StateValue s v) => (Map Int AStmt) -> Int -> (AStmt, (M s v ()))

fun sidMap sid = trace ("call sid " ++ (show sid)) $

let Just astmt = Data.Map.lookup sid sidMap

(AStmt (Function _ _ fbody) _) = astmt in (astmt, sstmt fbody)

runConcrete :: SdtlProgram -> IO ()

runConcrete (SdtlProgram mainStmt sdtlMap) = do

\--putStrLn $ show mainSid

putStrLn $ show sdtlMap

\--w <- getWorld

let [endState] =

runMonad mainStmt

(fun sdtlMap)

(CState {env = fromList [], {-io = w, -} returning = Nothing, exception =
Nothing,

objmem = fromList [(0, fromList [])], this = (Object 0)})

(Intval 0)

in do

\--putWorld (io endState)

putStrLn $ show (env endState)

runString :: String -> IO()

runString program = runConcrete (fst (S.runState (sdtl (lexer program)) (1,
fromList [])))

main = do

(sdtlfile:_) <- getArgs

program <- readFile sdtlfile

runString program-}-}-}-}-}

###  A.4 Abstract interpretation

⬇

{-# LANGUAGE MultiParamTypeClasses #-}

module Main (main, runString) where

import SemanticFunctions

import Sdtl

import Data.Map

import qualified Control.Exception as E

import System.Environment

import Data.ByteString.Internal

import Debug.Trace

import qualified Control.Monad.State as S

import qualified Data.List as L

data AValue = Intval

| Boolval

| FunPointer Sid Int Eid

| Object Int

deriving (Show, Eq, Ord)

instance Value AValue where

conval (Boolean True) = Boolval

conval (Boolean False) = Boolval

conval (Number i) = Intval

getSid (FunPointer n _ _) = n

binop Plus (Intval) (Intval) = Intval

binop Minus (Intval) (Intval) = Intval

binop Mult (Intval) (Intval) = Intval

binop Div (Intval) (Intval) = Intval

binop GreaterThan (Intval) (Intval) = Boolval

binop LessThan (Intval) (Intval) = Boolval

binop Equal (Intval) (Intval) = Boolval

data AState = AState{

env :: Map String AValue,

returning :: Maybe AValue,

exception :: Maybe AValue,

objmem :: Map Eid (Map String AValue),

this :: AValue,

curried :: Map (Sid, Int, Eid) [AValue]

} deriving (Show, Eq, Ord)

instance State (AState) where

esc (AState {returning = v, exception = e}) = case v of

Nothing -> case e of

Nothing -> False

_ -> True

_ -> True

\--fundecl :: String -> [String] -> Sid -> s -> [s]

fundecl fnname fnparams n s =

[s {env = insert fnname (FunPointer n 0 0) (env s) }]

y x = x (y x)

mapToMonad m = M $ \f -> \s -> if member s m then (m ! s) else [(s, Just ())]

instance StateValue AState AValue where

fix x = M $ \f -> \s ->

let (fixedMap) =

(y $ \x0 -> \m0 ->

let (M t1) = (x (mapToMonad m0))

newmap = traceShow m0 $

union m0 $

fromList

[(s1,t1 f s1) | s1 <- (L.map fst (L.nub $ concat $ elems m0)) ++ [s] ]

in

if m0 == newmap then newmap else x0 newmap) (fromList [])

in

trace ("final " ++ (show fixedMap)) $

L.nub $ concat $ elems fixedMap

ret v s = trace (show s) $ [s {returning = Just v}]

\--cond :: (CValue v) => v -> (M s v a) -> (M s v a) -> (M s v a)

cond (Boolval) (M t) (M u) = M $ \f -> \s0 ->

let s1 = t f s0

s2 = u f s0

in L.nub $ s1 ++ s2

\--cond _ t u = u

\--asg :: (CValue v) => String -> v -> s -> [s]

asg i v s = [s {env = (insert i v (env s))}]

\--dooutput :: (CValue v) => v -> s -> [s]

dooutput _ s = [s]

\--getinput :: (CValue v) => s -> [(s,v)]

getinput s =

[(s,Intval)]

\--val :: (CValue v) => s -> String -> v

val s i = (env s) ! i

\--enter :: (CValue v) => s -> Sid -> [v] -> s

enter s n vs t ids = s {env = fromList (zip ids vs), this = t}

\--leave :: (CValue v) => s -> s -> (s, Maybe v)

leave s0 s = trace (show s) $

(AState {env = (env s0), returning = Nothing, exception = (exception s),

curried = (curried s),

objmem = (objmem s),

this = (this s0)}, (returning s))

apply (FunPointer n c ce) p t e =

M $ \f -> \s ->

let cv=if c > 0 then ((curried s) ! (n, c, ce)) else [] in

if (arity f n) == c + (length p)

then let (M tcall) = (call n (cv ++ p) t) in (tcall f s)

else

[(s {curried = insert (n, (c + length p), e) (cv ++ p) (curried s)}

, Just (FunPointer n (c+(length p)) e))]

set (Object n) id1 v = \s ->

let oldo = (objmem s) ! n

in [s {objmem = insert n (insert id1 v oldo) (objmem s)}]

get (Object n) id1 = \s -> (objmem s) ! n ! id1

getglobal = \s -> (Object 0)

getthis = \s -> (this s)

newobj eid = M $ \f -> \s ->

[(s {objmem = insert eid (fromList []) (objmem s)}, Just (Object eid))]

\--runthrow :: v -> s -> [s]

runthrow v = \s -> [s {exception=Just v}]

\--runcatch :: String -> (M s v ()) -> (M s v ())

runcatch id1 (M u) = M $ \f -> \s0 ->

case (exception s0) of

Nothing -> [(s0, Just ())]

Just v -> (u f (s0 {env = insert id1 v (env s0), exception=Nothing}))

{-

getWorld :: IO RealWorld

getWorld = IO (\s -> (# s, fromState s #))

putWorld :: RealWorld -> IO ()

putWorld s’ = IO (\\_ -> (# toState s’, () #))

-}

fun :: (Map Int AStmt) -> (Map (Int,AState) [(AState, Maybe ())]) -> Int

-> (AStmt, (M AState AValue ()))

fun sidMap fapprox sid = trace ("call sid " ++ (show sid)) $

let Just astmt = Data.Map.lookup sid sidMap

(AStmt (Function _ _ fbody) _) = traceShow astmt $ astmt in

(astmt,

(M $ \f -> \s ->

if member (sid, s) fapprox then fapprox ! (sid, s)

else

(y $ \localx -> \prevresult ->

let

newapprox = (insert (sid, s) prevresult fapprox)

M t = (sstmt fbody)

result = t (fun sidMap newapprox) s

in

if result == prevresult then result

else localx result) []))

runAbstract :: SdtlProgram -> IO ()

runAbstract (SdtlProgram mainStmt sdtlMap) = do

\--putStrLn $ show mainSid

putStrLn $ show sdtlMap

\--w <- getWorld

let endStates =

runMonad mainStmt

(fun sdtlMap (fromList []))

(AState {env = fromList [],

returning = Nothing,

exception = Nothing,

curried = fromList [],

objmem = fromList [(0, fromList [])],

this = (Object 0)})

(Intval)

in do

\--putWorld (io endState)

putStrLn "Final States"

putStrLn $ show endStates

runString :: String -> IO()

runString program = runAbstract (fst (S.runState (sdtl (lexer program)) (1,
fromList [])))

main = do

(sdtlfile:_) <- getArgs

program <- readFile sdtlfile

runString program-}-}