Spécification de JavaScript

La spécification d'un langage est une définition de la syntaxe et de la sémantique du langage. Cette définition est en général un ensemble de règles syntaxiques définies dans une grammaire.

Initialement dédiés au partage de contenus statiques sur Internet, les sites web sont devenus de véritables applications accessibles à partir de n'importe quel navigateur.

Afin de rendre les sites plus interactifs et dynamiques, il a été nécessaire de mettre en place des langages de script tel que l'ActionScript ou le JavaScript. Ce dernier est actuellement le langage le plus utilisé pour les applications côté client, c'est-à-dire sur le navigateur.

L'ECMAScript a vu le jour en 1997 dans le but d'uniformiser l'interprétation de ces différents langages de script. Cette spécification décrit la syntaxe et la sémantique que ces langages doivent respecter, sous forme de phrases littérales. Ces définitions étant sujettes a interprétation, on a vu apparaître des divergences d'un langage, ou d'une de ses implémentations, à l'autre. La formalisation de cette spécification EcmaScript permettrait de lisser ces différences d'interprétation.

Motivations

La norme ECMAscript ne décrit pas le comportement à adopter par JavaScript de façon précise du fait que les règles sont définies avec des phrases littérales. En effet, chaque description de la spécification peut être comprise et interprétée différemment, ce qui a mené à l'apparition de divers interpréteurs JavaScript, ou même encore de primitives spécifiques aux moteurs de certains navigateurs, notamment entre Internet Explorer et Mozilla Firefox. Cette différence d'interprétation entre Internet Explorer et les autres navigateurs provient du fait que lors de la création du JavaScript par Brendan Eich en 1995, Microsoft a développé sa propre version avant que la norme EcmaScript apparaisse. Ceci est la raison pour laquelle un script fonctionnant correctement sous Internet Explorer ne fonctionnera pas forcément sur un autre navigateur. Dans le but d'assurer une compatibilité optimale entre les différents navigateurs, il est nécessaire de définir une spécification formelle afin que tous les interpréteurs acceptent la même syntaxe.

De plus, le JavaScript possède des vulnérabilités, quant au bon déroulement d'un programme, dues à certains cas non décrits dans la norme ECMAScript. Prenons par exemple le cas de l'opérateur typeof : la norme ne décrit pas explicitement quel comportement adopter si l'évaluation de l'expression unitaire provoque une erreur, laissant la possibilité ici d'un comportement variable selon les implémentations. Il est ainsi nécessaire aux analyseurs de gérer ce genre de problèmes. Les différentes interprétations n'assurent donc pas un comportement uniforme des programmes JavaScript, c'est pourquoi plusieurs recherches se portent sur la formalisation de ce langage.

Approches

On relève dans la communauté scientifique au moins 3 approches sur cette question.

λJS : l'essence de JavaScript

Cette approche part de deux constats : d'une part, le JavaScript n'est pas sécurisé à cause d'une sémantique non conventionnelle ; d'autre part, le langage est trop complexe pour être testé par des outils de tests standard. C'est sur ces deux points que se sont portés les travaux de Arjun Guha, Claudiu Saftoiu et Shriram Krishnamurthi.

Leur premier travail a été de concevoir un noyau, nommé λJS, qui ne contient que les fonctions essentielles du langage, sorte de sous-ensemble complet de JavaScript. Bien sûr, le fait de ne garder que l'essence du langage fait que beaucoup de sucre syntaxique n'existe plus. Prenons, par exemple, l'implémentation des objets, où certaines syntaxes ont été supprimées, au privilège d'une seule lorsque plusieurs sont envisageables. Afin d'accéder à l'attribut x d'un objet Y, il est normalement possible d'écrire Y['x'] ou Y.x. Cependant, λJS ne possède que l'écriture Y['x'] et n'implémente pas d'écriture alternative afin de garder le noyau de langage le plus petit possible. Une autre modification majeure est la disparation de l'utilisation implicite du this. En effet, lorsque l'on utilise le mot clé this, le programme fait référence à l'objet sur lequel est appelée la fonction. Toutefois, ce paramètre est implicite, il n'est donc pas nécessaire de le renseigner lors de l'appel de la méthode d'un objet, ce qui n'est pas le cas avec λJS. Ils ont ainsi fait disparaître un grand nombre de sucres syntaxiques dans le but de minimiser l'implémentation des fonctions pour permettre plus facilement la vérification d'un programme.

Cependant, afin de faire accepter leur noyau par les autres développeurs, il est nécessaire pour eux de prouver que n'importe quel programme écrit en JavaScript peut être réduit en un programme basé sur λJS. Pour réaliser leurs tests, l'équipe s'est basée sur trois implémentations de Javascript : SpiderMonkey (Firefox), V8 (Chrome), et Rhino (implémentation en Java). Ils ont transformé différents programmes compatibles sur ces implémentations vers un programme λJS, et ont ensuite vérifié que la sortie du nouveau programme correspond à celle de la version d'origine. Afin de couvrir un maximum de cas, les programmes sont un échantillon important de la série de test JavaScript de Mozilla. Les tests ont été concluants : l'intégralité de la série de tests produit exactement le même résultat que les trois autres implémentations.

L'objectif final étant de fournir un langage sûr, il est nécessaire de fournir un outil permettant de vérifier ce résultat. Le λJS étant une implémentation simplifiée du JavaScript, et étant donné qu'un programme peut être réduit en λJS, il est nécessaire de montrer que λJS est sûr. Pour prouver ceci, ils ont décomposé chaque propriété en sous-problèmes. Pour illustrer, prenons le cas de l'addition : ils jugent qu'une addition e1 + e2 est sûre si les expressions e1 et e2 sont sûres. En posant plusieurs lemmes, ils démontrent que l'addition est sûre et qu'elle peut être incluse dans le λJS. En appliquant cette démarche sur plusieurs éléments du langage, ils ont réussi à inclure un grand nombre de fonctionnalités à leur noyau en le gardant sûr. Ceci a permis en 2012 de définir le λJS comme base pour le langage JavaScript par ECMAScript 6, toutefois cette version n'est pas encore totalement supportée par tous les navigateurs.

SAFE : une autre specification pour EcmaScript

SAFE (Scalable Framework Analysis for ECMAScript) est un projet mené par le groupe de recherche en langage de programmation de l'Institut supérieur coréen des sciences et technologies (KAIST).

Tout comme le papier précédent, l'équipe se penche ici sur le constat que la spécification informelle du langage rend celui-ci sujet à interprétation. L'équipe relève également que les différents moteurs Javascript ne sont pas assez documentés, rendant leur compréhension et leur modification difficile. Ceci était le cas avec λJS qu'ils ont souhaité utiliser : ils ont jugé que la documentation concernant la réduction du Javascript en leur noyau n'était pas assez détaillée. C'est en partant de ces deux propositions qu'ils ont débuté le projet SAFE qui a pour but d'améliorer l'analyse d'un programme Javascript ainsi que de fournir un outil documenté pour la recherche.

SAFE est développé à destination de la communauté de recherche en JavaScript, c'est un projet open-source dont le code est accessible en ligne. L'implémentation est réalisée en Java et en Scala.

Comparé à l'approche de λJS, l'équipe ne s'est pas contentée de réduire un maximum de langage afin de fournir une spécification simplifiée mais a préféré réaliser une spécification de l'ensemble du langage. C'est dans ce sens qu'ils ont défini une spécification sur chaque niveau de représentation d'un programme Javascript.

L'arbre de syntaxe abstrait : AST

Afin de réaliser leur framework, il a été dans un premier temps nécessaire de transformer le code Javascript en un code facilement analysable.

Pour ce faire, le framework se base sur 3 niveaux de représentation d'un programme Javascript. La première représentation (qui est la plus proche du code source) est un AST (Arbre syntaxique abstrait). Afin d'obtenir l'AST correspondant au code source analysé, l'équipe s'est intéressée aux parsers JavaScript existants (ANTLR, les combinateurs de parseur de Scala, Rhino, SpiderMonkey, Closure Tools de Google, JSConTest, ou encore JSure) sans trouver entière satisfaction. Elle a finalement utilisé l'outil de génération Rats! se trouvant dans le projet eXTensible Compiler développé par une équipe de New York. Elle fournit à Rats! une grammaire de style BNF dont voici l'extrait concernant les instructions de boucle (l'indentation représente une relation de sous-classe) :

	/**
	* SourceElement ::= Stmt
	*/
	abstract Stmt();
		/**
		* Stmt ::= do Stmt while ( Expr ) ;
		*/
		DoWhile(Stmt body, Expr cond);
		/**
		* Stmt ::= while ( Expr ) Stmt
		*/
		While(Expr cond, Stmt body);
		/**
		* Stmt ::= for ( Expr? ; Expr? ; Expr? ) Stmt
		*/
		For(Option<Expr> init, Option<Expr> cond,
		Option<Expr> action, Stmt body);
		/**
		* Stmt ::= for ( lhs in Expr ) Stmt
		*/
		ForIn(LHS lhs, Expr expr, Stmt body);
		/**
		* Stmt ::= for ( var VarDecl(, VarDecl)* ;
		*
		Expr? ; Expr? ) Stmt
		*/
		ForVar(List<VarDecl> vars, Option<Expr> cond,
		Option<Expr> action, Stmt body);
		/**
		* Stmt ::= for ( var VarDecl in Expr ) Stmt
		*/
		ForVarIn(VarDecl var, Expr expr, Stmt body);

Rats! génère alors un parser JavaScript en langage Java, qui couplé à ASTGen, qui génère les classes Java représentant l'AST à partir d'une description fournie, va permettre de transformer le code JavaScript en représentation intermédiaire.

La représentation intermédiaire : IR

Dans un second temps, le framework transforme l'AST en une représentation intermédiaire IR qui permet de fournir une spécification de chaque fonctionnalité du langage Javascript définie par ECMAScript. Par exemple, chaque fonction possède au moins l'argument this afin de respecter cette norme. C'est cette représentation qui est utilisée pour l'évaluation du programme par un interpréteur. C'est à ce niveau qu'intervient SAFE en fournissant une spécification formelle et une implémentation de chaque fonctionnalité.

Grammaire de JavaScript IR :

  p ::= s*
  s ::= x = e
    |  x = delete x
    |  x = delete x [x]
    |  x = {(m,)* }
    |  x = [(e,)* ]
    |  x = x(x(, x)?)
    |  x = new x((x,)* )
    |  x = function f(x, x) { s*  }
    |  function f(x, x) { s*  }
    |  x = eval(e)
    |  x [x] = e
    |  break x
    |  return e?
    |  with (x) s
    |  x : { s }
    |  var x
    |  throw e
    |  s* 
    |  if (e) then s (else s)?
    |  while(e) s
    |  try { s } (catch (x){ s })?  (finally { s })?
    |  (s* )
  e ::= e ⊗ e
    | ɵ e
    | x [e]
    | x
    | this
    | num
    | str
    | true
    | false
    | undefined
    | null
  m ::= x : x
    | get f(x, x) { s*  }
    | set f(x, x) { s*  }
  ⊗ ::= | | & | ^ | << | >> | >>> | + | - | * | / | % | == | != | === | !== | < | > | <= | >= | instanceof | in
  ɵ ::= ~ | ! | + | - | void | typeof

Le graphe de flot de contrôle : CFG

Le troisième niveau de représentation est le CFG (Graphe de flot de contrôle) qui est utilisé uniquement pour l'analyse des performances. Afin de générer ce graphe, le projet utilise CFGBuilder qui est un composant du compilateur Polyglot. Ce programme prend en paramètre une représentation intermédiaire et génère un graphe correspondant qui pourra ensuite être analysé par le framework afin de réaliser plusieurs analyses.

Un exemple de transformation du code JavaScript au graphe de contrôle de flot en passant par la représentation intermédiaire, proposé dans le paragraphe 3.3 dans la publication présentant SAFE, illustre bien le résultat obtenu à ce stade.

Applications

Leur framework est disponible au public. Afin de permettre l'utilisation de leur projet par le plus grand nombre, SAFE fournit, en plus de la spécification et d'une documentation fournie, une implémentation des différentes fonctionnalités. Ceci permet d'utiliser leurs recherches plus facilement que les autres projets qui n'ont pas ou peu de documentation.

Les 3 niveaux de représentation du code JavaScript (AST, IR, CFG) rendent SAFE plus flexible, évolutif, et connectable, proposant ainsi un outil puissant dans la recherche et le développement de JavaScript.

JSCert : une spécification mécanisée et sûre de JavaScript

"Le projet JSCert a pour but de vraiment comprendre JavaScript", annonce le site du projet. Une équipe de chercheurs des laboratoires de l'INRIA et de l'Imperial College London se sont intéressés à la nécessité de clarifier les ambiguïtés liées à la longueur et aux nombreux recoins du standard ECMAScript.

JSCert

JSCert est une spécification mécanisée du standard ECMAScript, écrite dans l'assistant interactif de preuve Coq, conçue pour être la plus proche de la norme ECMAScript5. Elle se base sur le développement en 2008, mené par Sergio Maffeis, d'une sémantique de description formelle du comportement complet de JavaScript suivant fidèlement ECMAScript3, à l'exception des parties ambiguës de ce standard. Cette formalisation se limite au cœur du langage JavaScript.

JSRef

En parallèle a été développé JSRef, un interpréteur exécutable de référence, certifié dans le respect de JSCert, et testé en utilisant la suite de tests de confirmité d'ECMAScript, test262.

JSCert n'est pas directement utilisable, de par sa conception : c'est une définition inductive à destination du développement de preuves de sûreté, qui compense l'imprécision concernant les fonctionnalités dépendantes de l'implémentation dans ECMAScript5. En tant que spécification Coq calculable, on en a extrait automatiquement le code OCaml correspondant, obtenant ainsi l'interpréteur JSRef. Celui-ci respecte la norme ECMAScript5 autant qu'il était possible de la formaliser par JSCert.

De ECMAScript à JSRef

La vérification de JSCert dans cette sémantique mécanisée est dû à sa proximité avec la norme ECMAScript5 : la prose anglaise de celle-ci et les règles formelles qui en découlent peuvent être mises côte-à-côte, chaque ligne de pseudo-code correspondant à une ou deux règles formelles de JSCert. JSRef se vérifie par le mécanisme automatique par lequel il est extrait de JSCert.

Le pseudo-code correspondant à la boucle while dans ECMAScript5 :

	1. Let V = empty.
	2. Repeat
	   a. Let exprRef be the result of evaluating Expression.
	   b. If ToBoolean(GetValue(exprRef)) is false, return (normal,V,empty).
	   c. Let stmt be the result of evaluating Statement.
	   d. If stmt.value is not empty, let V = stmt.value.
	   e. If stmt.type is not continue || stmt._target is not in the current label set, then
	       i. If stmt.type is break and stmt._target is in the current label set, then return (normal,V,empty).
	      ii. If stmt is an abrupt completion, return stmt.

La sémantique JSCert implémentée dans Coq correspondant à la boucle while, et traduisant la sémantique définie dans la publication de JSCert :

	(* Step 1: red_while_1 *)
	| red_stat_while : forall S C labs e1 t2 o,
		red_stat S C (stat_while_1 labs e1 t2 resvalue_empty) o ->
		red_stat S C (stat_while labs e1 t2) o

	(* Steps 2a and 2b: red_while_2a_2b *)
	| red_stat_while_1 : forall S C labs e1 t2 rv y1 o,
		red_spec S C (spec_expr_get_value_conv spec_to_boolean e1) y1 ->
		red_stat S C (stat_while_2 labs e1 t2 rv y1) o ->
		red_stat S C (stat_while_1 labs e1 t2 rv) o

	(* Step 2b False: red_while_2b'_false *)
	| red_stat_while_2_false : forall S0 S C labs e1 t2 rv,
		red_stat S0 C (stat_while_2 labs e1 t2 rv (vret S false)) (out_ter S rv)

	(* Step 2b True and 2c: red_while_2b'_true_2c *)
	| red_stat_while_2_true : forall S0 S C labs e1 t2 rv o1 o,
		red_stat S C t2 o1 ->
		red_stat S C (stat_while_3 labs e1 t2 rv o1) o ->
		red_stat S0 C (stat_while_2 labs e1 t2 rv (vret S true)) o

	(* Step 2d: red_while_2d *)
	| red_stat_while_3 : forall rv S0 S C labs e1 t2 rv' R o,
		rv' = (If res_value R <> resvalue_empty then res_value R else rv) ->
		red_stat S C (stat_while_4 labs e1 t2 rv' R) o ->
		red_stat S0 C (stat_while_3 labs e1 t2 rv (out_ter S R)) o

	(* Step 2e False: red_while_2e_false *)
	| red_stat_while_4_continue : forall S C labs e1 t2 rv R o,
		res_type R = restype_continue /\ res_label_in R labs ->
		red_stat S C (stat_while_1 labs e1 t2 rv) o ->
		red_stat S C (stat_while_4 labs e1 t2 rv R) o

	(* Step 2e True: red_while_2e_true *)
	| red_stat_while_4_not_continue : forall S C labs e1 t2 rv R o,
		~ (res_type R = restype_continue /\ res_label_in R labs) ->
		red_stat S C (stat_while_5 labs e1 t2 rv R) o ->
		red_stat S C (stat_while_4 labs e1 t2 rv R) o

	(* Step 2e i True: red_while_2e_i_true *)
	| red_stat_while_5_break : forall S C labs e1 t2 rv R,
		res_type R = restype_break /\ res_label_in R labs ->
		red_stat S C (stat_while_5 labs e1 t2 rv R) (out_ter S rv)

	(* Step 2e i False: red_while_2e_i_false *)
	| red_stat_while_5_not_break : forall S C labs e1 t2 rv R o,
		~ (res_type R = restype_break /\ res_label_in R labs) ->
		red_stat S C (stat_while_6 labs e1 t2 rv R) o ->
	red_stat S C (stat_while_5 labs e1 t2 rv R) o

	(* Step 2e ii True: red_while_2e_ii_true *)
	| red_stat_while_6_abort : forall S C labs e1 t2 rv R,
		res_type R <> restype_normal ->
		red_stat S C (stat_while_6 labs e1 t2 rv R) (out_ter S R)

	(* Step 2e ii False: red_while_2e_ii_false *)
	| red_stat_while_6_normal : forall S C labs e1 t2 rv R o,
		res_type R = restype_normal ->
		red_stat S C (stat_while_1 labs e1 t2 rv) o ->
		red_stat S C (stat_while_6 labs e1 t2 rv R) o

La sémantique JSRef de la boucle while :

Definition run_stat_while runs S C rv labs e1 t2 : result :=
	if_spec (run_expr_get_value runs S C e1) (fun S1 v1 => 
		Let b := convert_value_to_boolean v1 in
			if b then
				if_ter (runs.runs_type_stat S1 C t2) (fun S2 R =>
					Let rv' := ifb res_value R != resvalue_empty
						then res_value R else rv in
							Let loop := fun _ => runs.runs_type_stat_while S2 C rv' labs e1 t2 in
								ifb res_type R != restype_continue
									|| res_label_in R labs
								then (ifb res_type R = restype_break
										&& res_label_in R labs
									then res_ter S2 rv'
									else (ifb res_type R != restype_normal
										then res_ter S2 R else loop tt))
								else loop tt)
						else res_ter S1 rv).

Definition run_stat runs S C t : result :=
	match t with
	|stat_while ls e1 t2 => runs.runs_type_stat_while S C ls e1 t2 resvalue_empt...

Applications

On peut envisager plusieurs utilisations potentielles de JSCert et JSRef :

• analyser des morceaux de code JavaScript
• vérifier la bonne implémentation d'un compilateur d'un langage de plus haut niveau en JavaScript
• comparer l'implémentation d'un interpréteur avec celle de JSRef

On peut imaginer que cette spécification formelle et mécanisée soit intégrée dans une future édition d'ECMAScript.

Synthèse

	λJS	SAFE	JSCert
Motivation	Pouvoir tester plus efficacement des programmes Diminuer la complexité des programmes	Améliorer l'analyse des programmes Fournir des outils pour la recherche	Fournir une représentation formelle de l'ECMASCRIPT Clarifier ECMAScript en cas de doute sur l'interprétation Fournir un interpréteur vérifiant qu'un programme respecte cette spécification
Réalisations	Réalisation d'un noyau minimal de Javascript Assurer la sureté de ce noyau Ramener le sucre syntaxique aux fonctions de base	Fournir une spécification et une implémentation de l'ECMAScript Convertir l'AST d'un programme Javascript vers une représentation intermédiaire	Réalisation d'une spécification formelle des fonctionnalités de Javascript Réalisation d'un interpréteur respectant JSCert
Spécification effectuée	Réduction du Javascript en un ensemble de fonction minimale	Spécification sur chaque niveau de représentation d'un programme Javascript	Réalisation d'une spécification en Coq

Liens externes

Bibliographie

(en) Arjun Guha, Claudiu Saftoiu et Shriram Krishnamurthi, « The Essence of JavaScript », ECOOP '10 Proceedings of the 24th European conference on Object-oriented programming,‎ 21 juin 2010, p. 126-150 (ISBN 3-642-14106-4 et 978-3-642-14106-5, lire en ligne)

Brown University

(en) Hongki Lee, Sooncheol Won, Joonho Jin, Junhee Cho et Sukyoung Ryu, « SAFE: Formal Specification and Implementation of a Scalable Analysis Framework for ECMAScript », FOOL '12 Foundations of Object-Oriented Languages,‎ 22 octobre 2012 (CiteSeer^x 10.1.1.387.1030, lire en ligne)

KAIST

(en) Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudžiuniene, Alan Schmitt et Gareth Smith, « A Trusted Mechanised JavaScript Specification », POPL '14 Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,‎ 22 janvier 2014 (ISBN 978-1-4503-2544-8, DOI 10.1145/2535838.2535876, lire en ligne)

INRIA & Imperial College London

(en) Sergio Maffeis, John C. Michell et Ankur Taly, « An Operational Semantics for JavaScript », APLAS '08,‎ 2008 (lire en ligne)

Articles connexes

• JavaScript
• ECMAScript