6910JSExplain：JavaScript的双调试器0Arthur Charguéraud Inria &Université de Strasbourg,CNRS, ICube UMR 7357arthur.chargueraud@inria.fr0Alan Schmitt Inria & UnivRennes, CNRS, IRISAalan.schmitt@inria.fr0Thomas Wood Imperial CollegeLondonthomas.wood09@imperial.ac.uk0摘要0我们提供了JSExplain，一个紧密遵循规范并生成执行跟踪的JavaScript参考解释器。这些跟踪可以在浏览器中进行交互式调查，界面不仅显示解释器的代码和状态，还显示被解释程序的代码和状态。可以根据解释器和被解释程序来表达条件断点。在这方面，JSExplain是JavaScript规范的双调试器。0ACM参考格式：Arthur Charguéraud，Alan Schmitt和ThomasWood。2018。JSExplain：JavaScript的双调试器。在WWW '18Companion：2018年Web会议伴侣，2018年4月23日至27日，法国里昂。ACM，纽约，纽约，美国，9页。https://doi.org/10.1145/3184558.318596901 引言 1.1 JS的参考解释器0JavaScript（JS）具有复杂的语义。截至2017年，ECMA的规范由885页的英文散文组成[6]（详见§1.2）。毫不奇怪，这种基于散文的规范呈现不能满足JavaScript设计师和实现者的需求。特别是，JavaScript标准化委员会（TC39）已经多次表达了对描述和与语义交互的更好工具的需求（§1.3）。关于JS语义的形式化之前的工作，特别是JSCert [3]和KJS[11]，取得了一些进展，但未能提供TC39所需的几个功能（§1.4）。在这项工作中，我们旨在解决这些要求：我们通过给JSCert语义提供一个对JavaScript社区更易于理解的表达方式来重新审视它。我们的表达方式旨在适合编写和阅读规范、执行测试用例、检查覆盖率和交互式调试规范（§1.5）。JS规范本质上描述了一个参考解释器。尽管它由英文散文组成，但ECMA标准几乎读起来像伪代码。大多数在ECMA3和ECMA5中存在的模糊和不清晰的段落在随后的版本中逐渐解决。因此，将ECMA伪代码转换为实际代码，即用真实的编程语言表达的代码，并不那么困难。然而，有两个非平凡的方面：处理状态的表示和处理异常终止，如异常、返回、中断和继续语句。0本文根据知识共享署名4.0国际（CC BY4.0）许可发布。作者保留在其个人和公司网站上传播作品的权利，并附上适当的归属。WWW'18 Companion，2018年4月23日至27日，法国里昂© 2018IW3C2（国际万维网会议委员会），根据知识共享CC BY 4.0许可发布。ACM ISBN978-1-4503-5640-4/18/04。https://doi.org/10.1145/3184558.31859690事实上，在JS中，任何子表达式的求值，任何类型转换的求值，以及大多数来自规范的内部操作的求值都可能导致用户代码的执行，从而引发异常，中断正常的控制流程。通过连续的版本，ECMA标准逐渐引入了类似于异常单子的符号（§1.2）。这种符号自然地通过异常单子的适当单子绑定运算符转换为实际代码。关于状态，标准假设存在一个全局状态。一个参考解释器可以假设一个带有副作用的全局状态，或者以纯函数式风格显式地传递状态。我们选择了后者的方法，有三个原因。首先，我们已经需要一个异常单子，所以我们可以很容易地扩展这个单子来处理状态。其次，从具有显式状态的代码开始，可以更容易地生成相应的归纳定义在形式逻辑（例如Coq）中，我们将来希望进行研究。第三，为了方便阅读，可以很容易地隐藏一个显式线程的状态；相反，实现一个隐含状态的状态将更具挑战性。因此，我们使用纯函数式语言编写我们的参考解释器，该语言扩展了用于状态和突然终止传播的单子符号的语法糖（§2）。出于历史原因，我们选择了OCaml的子集作为源语法，但也可以使用其他语言。事实上，我们实现了一个从我们的OCaml子集到JS子集的翻译器（一个不涉及副作用和类型转换的子集）。因此，我们获得了一个能够在JS虚拟机内执行JS程序的JS解释器，JS的粉丝应该会很高兴。为了进一步提高对JS程序员的可访问性，我们还将解释器的源代码翻译成了一种可读性较强的JS风格语法，我们称之为伪JS，它基本上由JS语法加上单子符号和基本模式匹配组成。我们对JS的参考语义本质上是可执行的。因此，我们可以在测试套件上执行我们的解释器，可以通过编译和执行OCaml代码，或者通过执行该代码的JS翻译来执行。确实有必要能够检查JS测试套件中的示例的评估是否产生所需的输出。更有趣的是，可以逐步调查给定测试用例上解释器的评估。这样的调查可以帮助理解为什么特定测试用例的评估会产生特定的输出-鉴于JS的复杂性，即使是专家也很容易被某段代码的输出值困惑。此外，交互式执行使得新的JS功能的贡献者更容易添加新的测试用例，并检查这些测试用例是否触发了新功能，并与现有功能正确交互。在本文中，我们介绍了一个名为JSExplain的工具，用于研究JS的执行。这个工具可以被看作是一个双调试器，它同时针对JavaScript的规范和解释程序进行调试。0Track: Web Programming WWW 2018, 2018年4月23日至27日，法国里昂6920显示解释程序和被解释程序的状态。特别是，我们的工具支持同时在解释程序和被解释程序上表达条件断点。为了实现这个工具，我们生成了一个被用于生成执行跟踪的解释器版本（§3），并提供了一个基于 Web的工具来浏览这样的跟踪（§4）。据我们所知，我们的工具是第一个这样的双重调试器，即具有用于处理解释其他程序的程序的特定附加功能的调试器（§5）。01.2 JavaScript 的英文规范0为了说明 JavaScript 标准（ECMA）[6]的编写风格，我们以加法的描述为例，这将是本文中的运行示例。在JS中，加法运算符将其参数转换为整数并计算它们的和，除非两个参数中的一个是字符串，在这种情况下，另一个参数将被转换为字符串，并将两个字符串连接起来。ECMA5（2016年6月之前）的描述如图1所示。首先，观察到该描述同时描述了加法的解析规则和求值规则。为了提高可访问性，JS标准没有明确说明抽象语法树（AST）的概念。加法的语义如下：首先将左分支评估为一个值，然后将右分支评估为一个值，然后将这两个值（可能是对象）转换为原始值（例如，字符串、数字等），然后测试两个参数中是否有一个是字符串。如果是，则将两个参数都转换为字符串并返回它们的连接；否则将两个参数都转换为数字并返回它们的和。ECMA5中使用的这种呈现风格没有提供关于异常传播的详细信息。虽然对于语句，异常的处理是显式的，但对于表达式，它是隐含的。例如，如果左分支的评估引发异常，则不应该评估右分支。事实证明，将异常处理方式留下来是隐含的，可能会导致在触发异常时对应该评估什么或不应该评估什么产生歧义。ECMA委员会讨厌这种歧义，因为它可能（并通常）导致不同的浏览器展示不同的行为，这是 Web 开发人员的噩梦。在 ECMA6中，通过使异常的传播变得明确来解决了这种歧义。图2显示了加法运算符的更新规范。有两个主要的变化。首先，每个评估部分都在自己的一行上进行描述，从而使评估顺序清晰明了。其次，每个中间结果都调用了元操作ReturnIfAbrupt。这个元操作本质上对应于一个异常单子。ECMA6标准旨在面向广大受众，避免引入“单子”一词。相反，它将ReturnIfAbrupt指定为一个“宏”，如图3所示。实质上，每个结果都包含一个“完成记录”，它对应于一个总和类型，用于区分正常结果和异常。在除了 try-catch块之外的所有结构中，异常会中断评估的正常流程。因此，ECMA6规范中散布着大约 1100 处 ReturnIfAbrupt操作。意识到这种规范风格的不可行性，标准化委员会决定在ECMA7 中引入一层额外的语法糖，以后的版本中也会如此。0评估：AdditiveExpression: AdditiveExpression +MultiplicativeExpression01. 让 lref 成为评估 AdditiveExpression 的结果。2. 让 lval 成为GetValue(lref) 的结果。3. 让 rref 成为评估MultiplicativeExpression 的结果。4. 让 rval 成为GetValue(rref) 的结果。5. 让 lprim 成为 ToPrimitive(lval)的结果。6. 让 rprim 成为 ToPrimitive(rval) 的结果。7. 如果Type(lprim) 是字符串或 Type(rprim) 是字符串，则返回将ToString(lprim) 后跟 ToString(rprim) 的结果的字符串。8.返回将 ToNumber(lprim) 和 ToNumber(rprim)应用于加法操作的结果。0图1：加法的 ECMA5 规范。0评估：AdditiveExpression : AdditiveExpression +MultiplicativeExpression01. 令 lref 为评估 AdditiveExpression 的结果。2. 令 lval 为GetValue(lref)。3. 如果出现异常，返回 lval 的结果。4. 令 rref为评估 MultiplicativeExpression 的结果。5. 令 rval 为GetValue(rref)。6. 如果出现异常，返回 rval 的结果。7. 令 lprim为 ToPrimitive(lval)。8. 如果出现异常，返回 lprim 的结果。9. 令rprim 为 ToPrimitive(rval)。10. 如果出现异常，返回 rprim的结果。11. 如果 Type(lprim) 是 String 或者 Type(rprim) 是String，则a. 令 lstr 为 ToString(lprim)。b. 如果出现异常，返回lstr 的结果。c. 令 rstr 为 ToString(rprim)。d.如果出现异常，返回 rstr 的结果。e. 返回将 lstr 和 rstr连接起来的字符串的结果。12. 令 lnum 为ToNumber(lprim)。13. 如果出现异常，返回 lnum 的结果。14.令 rnum 为 ToNumber(rprim)。15. 如果出现异常，返回 rnum的结果。16. 返回将 lnum 和 rnum 应用加法操作的结果。0图2：加法的 ECMA6 规范。0规范。如图4所示，它们将问号符号定义为 ReturnIfAbrupt步骤的轻量级简写。该新风格中加法的规范如图5所示。ECMA7和ECMA8（图5）的呈现既比ECMA6（图2）更简洁，又比ECMA5（图1）更正式。问号的使用在第2节中与我们用于形式语义的单子符号进行比较。01.3 来自JS委员会的请求0JavaScript的标准化机构，是ECMA的一部分，被称为TC39，包括来自浏览器供应商、主要0Track: Web Programming WWW 2018, 2018年4月23日至27日，法国里昂`hello ${name}`;"hello " + name;Track: Web Programming WWW 2018, April 23-27, 2018, Lyon, France6930评估：ReturnIfAbrupt0算法步骤说01. 返回 ReturnIfAbrupt 的参数。0意思与以下内容相同：01. 如果 argument 是一个突然终止的完成，返回 argument。2. 否则，如果 argument 是一个完成记录，则令argument 为 argument .[[value]]。0图3：ReturnIfAbrupt 的 ECMA6 解释。0算法步骤说或等效于：01. 如果出现异常，返回 AbstractOperation() 的结果。0意思与以下内容相同：01. 令 hygienicTemp 为 AbstractOperation() 的结果。2. 如果hygienicTemp 是一个突然终止的完成，返回 hygienicTemp 。3.否则，如果 hygienicTemp 是一个完成记录，则令 hygienicTemp为 hygienicTemp .[[Value]]。其中 hygienicTemp是短暂的，只在与 ReturnIfAbrupt 相关的步骤中可见。0以 ? 开头的抽象操作和语法导向操作的调用表示应将ReturnIfAbrupt 应用于生成的完成记录。例如，步骤：01. ？操作名称的结果。0等效于以下步骤：01. 如果出现异常，返回操作名称的结果。0图4：ECMA7和ECMA8中的 ReturnIfAbrupt 的加法。0Web的演员和学者。它旨在定义所有浏览器都应该实现的公共语义。TC39面临着重大挑战。一方面，它必须确保完全向后兼容，以避免“破坏Web”。特别是，规范中从未删除过的任何在野外使用的功能。另一方面，委员会规定，在至少两个不同的主要浏览器中实施、发布和测试之前，不得将任何功能添加到标准中。委员会的任何成员都可以提出新的功能提案，因此有许多提案正在积极开发中，处于不同的形式化阶段[14]。标准的快速演变强调了在重写、测试和调试语义时需要适当的工具。特别是，我们与一些成员进行互动时，他们表达了对一些基本工具的需求，例如：•一种工具，用于了解规范中出现的所有变量是否在某个地方正确定义（绑定）;•一种工具，用于对元函数和规范中涉及的变量进行基本类型检查;•一种工具，用于检查有副作用的操作是否在自己的行上进行，以避免评估顺序的歧义;• 一种工具，用于检查在所有情况下都规定了行为;0评估：AdditiveExpression : AdditiveExpression +MultiplicativeExpression01. 让 lref 成为评估 AdditiveExpression 的结果。 2. 让 lval 成为 ?GetValue(lref)。 3. 让 rref 成为评估 MultiplicativeExpression的结果。 4. 让 rval 成为 ? GetValue(rref)。 5. 让 lprim 成为 ?ToPrimitive(lval)。 6. 让 rprim 成为 ? ToPrimitive(rval)。 7.如果 Type(lprim) 是 String 或者 Type(rprim) 是 String，那么 a.让 lstr 成为 ? ToString(lprim)。 b. 让 rstr 成为 ?ToString(rprim)。 c. 返回将 lstr 和 rstr 连接起来的字符串。 8. 让lnum 成为 ? ToNumber(lprim)。 9. 让 rnum 成为 ?ToNumber(rprim)。 10. 返回将 lnum 和 rnum应用加法操作的结果。0图5：ECMA7和ECMA8关于加法的规范。0• 一个能够告诉我们规范中哪些行没有被主要测试套件（test262[15]）中的任何测试覆盖的工具； •一个能够逐步执行规范在具体JS程序上的工具，并检查变量的值。0特别是，逐步执行对于评估新功能至关重要。当委员会决定将一个功能提案纳入时，通常不会原样接受该提案，而是以一种适合于简单、清晰的规范且没有边界情况的方式修改该提案，小心地尝试避免与其他现有功能（或计划中的功能）产生有害的相互作用。在此过程中，委员会成员手中有扩展语义的草稿以及一系列说明新行为的测试用例。自然地，他们希望检查扩展语义的形式化是否为每个测试用例分配了预期的行为。有人可能会认为这样的任务可以通过修改主流浏览器之一来完成。然而，现有的JS运行时是以效率为目标构建的，具有涉及大量优化的庞大代码库。因此，以任何方式修改代码对于委员会成员来说都是代价太高，无法调查功能请求的变化。即使他们可以投入努力，英文散文规范与实现之间的距离太大，无法确保两者匹配，即代码中实现的行为与散文中描述的行为相匹配。测试新功能的另一种替代方法是将该功能开发为纯JS的详细说明（本地翻译）。这可以采用添加缺失API的语法糖形式，即polyfill，或者采用源到源的转换形式，即transpiler。例如，可以将所谓的“模板字面量”转换为简单的字符串连接。0/* 新特性 */ /* 纯JavaScript */0var name = "me"; var name = "me";Track: Web Programming WWW 2018, April 23-27, 2018, Lyon, France6940尽管polyfills和transpilers是测试新功能的简单方法，但它们有两个主要限制。首先，编码可能会非常侵入。例如，ECMAScript2015版本添加了代理，因此显着改变了语言的内部方法；代理的Babel[1]转换器[2]能够在JS的早期版本中模拟此功能，但代价是将所有字段访问操作替换为对包装函数的调用。其次，使用这些方法实现的几个新功能之间的交互非常难以预测。01.4 JS的形式化规范0近年来，两个项目JSCert [3]和KJS[11]提出了JS的一个重要子集的形式化规范。JSCert在Coq证明助手[16]中形式化了ECMA5的一个大步归纳定义（技术上是一个相当大的步骤规范[5]）。JSCert附带了一个称为JSRef的参考解释器，该解释器在归纳定义方面被证明是正确的。JSRef可以被提取为可执行的OCaml代码以执行测试。KJS使用K框架[13]将JS描述为一组重写规则的小步语义。该框架已被用于形式化其他几种现实世界的语言的语义。它特别提供了执行（语法导向的）转换规则在具体输入程序上的工具支持。乍一看，似乎形式化规范可以满足委员会的所有要求。定义经过了彻底的类型检查；特别是，所有变量必须正确绑定。定义以形式语言定义，没有歧义；特别是，评估顺序和异常传播被准确指定。语义可以在具体输入程序上执行；此外，通过一些额外的工具，可以执行一组程序并报告测试覆盖范围。鉴于形式语义的所有优点，为什么标准化委员会TC39不考虑将JSCert或KJS等形式语义作为语言的参考呢？经过与TC39的高级成员讨论，我们了解到至少有三个主要原因，为什么JSCert或KJS等形式语义不可能被采用为参考语义。0（1）Coq或K中的形式化规范使用对JS程序员来说不太容易理解的语法和概念。然而，规范旨在被广泛读者阅读。（2）这些形式化语言的入门成本对于委员会成员来说太高，以至于他们无法达到自己贡献新定义所需的熟练程度。（3）JSCert和KJS提供可以执行的规范，但不提供以调试器方式支持交互式导航和可视化状态和变量值的功能，因此在调整新功能的描述方面帮助有限。0在本研究中，我们暂时搁置了给JS提供形式化语义的动机，这样可以用来形式化语言的属性（例如安全属性），而是专注于试图提供更好地满足TC39委员会日常需求的形式化语义。01.5贡献0在本文中，我们提出了一个名为JSExplain的工具，旨在为JS提供一个形式化语义，以解决先前工作中提到的限制。我们的贡献有两个方面。首先，我们提出了一个JS规范，用一个我们认为JS程序员可以轻松阅读和编写的语言来表达（§2）。其次，我们提供了一个交互式工具，支持对输入的JS程序逐步执行规范（§3和§4）。我们的工具模拟了调试器的功能，如导航控制、状态和变量可视化以及条件断点，但同时适用于解释器程序和被解释程序。我们用于显示规范的语言由JS的一个子集组成，扩展了单子和基本模式匹配的语法糖。这种语言，我们称之为伪JS，可以是我们规范的源语法。然而，出于历史和技术原因，我们使用OCaml的一个子集作为输入语法，该子集使用OCaml类型检查器进行处理。我们当前的工具会自动将OCamlAST转换为伪JS代码。将来，我们也可以直接将我们的参考解释器编写为伪JS语法，并且可以通过将其转换为OCaml或重新实现基本的ML类型检查器来对该代码进行类型检查。第三种选择是使用Reason语法[12]，这是一种用于OCaml程序的类似JS的语法。这些方法之间的唯一区别在于TC39委员会成员是否更喜欢编写OCaml风格或JS风格的代码。02规范语言2.1语言的构造0我们编写和显示规范的输入语法是一种纯函数语言，包括以下构造：变量、常量、序列、条件、let绑定、函数定义、函数应用（支持前缀和中缀函数）、数据构造函数、记录（包括记录投影和“record-with”构造以构建具有多个字段更新的记录副本）、元组（即匿名记录）和简单模式匹配（仅限非嵌套模式，限于数据构造函数、常量、变量和通配符）。为了方便起见，let绑定和函数可以绑定模式（而不仅仅是变量）。我们有意地针对一种具有有限数量构造和非常标准语义的规范语言，以尽量减少进入该语言的成本。请注意，输入代码在ML中进行类型检查。（多态主要用于对选项和列表进行类型检查以及对它们的操作。）如前所述（§1.2），语义涉及异常和其他突发行为（break、continue和return）的传播。它们的传播可以在我们的小语言中用函数和模式匹配来描述。然而，引入一点点语法糖可以极大地提高可读性。例如，我们写“let % run x = e1 in e2”来表示“if_rune1 (fun x ->e2)”，其中if_run是实现我们的monad的函数。单子运算符if_run具有多态类型，因此规范中的函数可以返回各种类型的对象。然而，在实践中，ECMA标准的大多数函数都是返回对象的。6950and run_binary_op s c op v1 v2 =0match op with | C_binary_op_add -> run_binary_op_add sc v1 v2 ...0and run_binary_op_add s0 c v1 v2 =0let % prim (s1, w1) = to_primitive_def s0 c v1 in let % prim (s2, w2) =to_primitive_def s1 c v2 in if (type_compare (type_of (Coq_value_prim w1))Coq_type_string) || (type_compare (type_of (Coq_value_prim w2))Coq_type_string)0then let % string (s3, str1) = to_string s2 c (Coq_value_prim w1) in let % string (s4, str2) = to_string s3 c(Coq_value_prim w2) in res_out (Coq_out_ter (s4, (res_val (Coq_value_prim (Coq_prim_string (strappend str1str2))))))0else let % number (s3, n1) = to_number s2 c (Coq_value_prim w1) in let %number (s4, n2) = to_number s3 c (Coq_value_prim w2) in0res_out (Coq_out_ter (s4, (res_val (Coq_value_prim (Coq_prim_number (n1 +. n2))))))0Figure 6: 我们规范语言的当前输入语法：OCaml的一个子集，扩展了单子表示法。0被描述为返回“完成三元组”，它们要么描述突然终止，要么描述一个值。在许多情况下，该值实际上被限制为特定类型。例如，如果to_number产生一个值，那么这个值必然是一个数字。标准在隐式地利用这个不变量，如“让n成为通过调用to_number产生的数字”。相比之下，我们的代码需要从返回的值中显式地提取数字。为此，我们引入了特殊的单子，如if_number，实际上写作“let % number n =e1 ine2”。（另一种方法是给完成三元组分配多态类型，但是按照这个路线需要在许多地方稍微偏离ECMA的规范。）图6显示了我们参考解释器中加法的规范，使用OCaml语法扩展了单子表示法。这段代码实现了图2中的非正式等价物。在该代码中，s表示状态，c表示环境（变量和词法环境，在JS术语中），op对应于运算符（这里，构造函数C_binary_op_add对应于描述运算符+的AST标记），v1和v2对应于参数，w1和w2对应于它们的原始值。函数strappend表示字符串连接，而“+.”表示浮点数加法（即JS的数字）。首先注意，正如前面解释的（§1.1），状态在整个代码中被线程化。我们将在下一节中展示如何隐藏状态变量（§2.2）。还要注意的是，代码还依赖于一些辅助函数。函数type_compare实现了JS类型的比较——为了使我们的语言简洁明了，我们不想假设一个具有非平凡规范的通用比较函数。函数to_primitive_def、to_string和to_number是规范中的内部函数，用于实现转换。这些操作可能会评估任意用户代码，因此可能会执行副作用或引发异常，因此需要将它们包装在单子的let绑定中。这种源语言的一个重要特点是它不涉及任何“隐式”机制。所有类型转换在代码中都是显式的，因此始终清楚其含义。特别是，无需对代码进行类型检查以确定其语义。总之，解释器的OCaml代码（例如，0var run_binary_op = function (op, v1, v2) { switch(op) { case C_binary_op_add:0返回（run_binary_op_add(v1, v2)); ... } }; varrun_binary_op_add = function(v1, v2) {0var％prim w1 = to_primitive_def（v1）; var％prim w2 =to_primitive_def（v2）;if（（type_compare（type_of（w1），Type_string）0|| type_compare（type_of（w2），Type_string））{0var％string str1 = to_string（w1）;var％string str2 = to_string（w2）;return strappend（str1，str2）; } else {0var％number n1 = to_number（w1）;var％number n2 = to_number（w2）;return（n1 + n2）; } };0图7：伪JS语法的解释器生成的代码，带有隐式环境、状态和转换。0图6）非常适合作为一个非歧义的输入语言。请注意，可以使用OCaml的编译器编译此代码以运行测试用例；我们的解释器的当前版本通过了来自官方测试套件（test262）的5000多个测试用例。02.2 转换为伪JS语法0尽管我们认为将源语言完全明确化是一个理想的特性，但在我们的解释器中以更简洁的语法打印源代码也是有优点的。正式规范中出现的“噪音”（例如图6）来自三个主要来源：0（1）每个函数都以环境作为参数；（2）每个函数都以参数作为参数，并返回可变状态的描述（也称为堆）；0Track: Web Programming WWW 2018，2018年4月23日至27日，法国里昂6960（3）通常使用多个构造函数来构建值，例如0C_value_prim，它将一个数字（OCaml类型为float的值）提升为一个JS值（OCaml类型为value的值）。0幸运的是，我们可以轻松消除这三个噪音的来源。首先，环境几乎总是不变地传递。它只能在函数调用、with结构或块的范围内进行修改。当它被修改时，新的绑定只是简单地推入环境中（它的行为类似于堆栈），然后被弹出。因此，我们可以假设，就像ECMA规范一样，环境存储在全局状态中。这样可以避免传递名为“c”的参数的需要。其次，可变状态的描述通过代码进行传递。将“当前状态”作为参数传递给可能执行副作用的每个函数，并对称地将“更新状态”返回给调用者，调用者为其绑定一个新的名称。考虑到在执行的任何给定点上只有一个版本的状态，我们可以假设，就像ECMA规范一样，状态存储在全局变量中。这样可以避免传递名为“s1”、“s2”等的值的需要。第三，许多构造函数的存在是由于需要转换。然而，这些转换中的许多可以被视为“隐式转换”（或Coq术语中的“强制转换”）。对于一组经过精心选择的、一次性定义的转换以及具有隐式转换的类型正确的程序，存在一种唯一（非歧义）的方式来插入转换以使程序通过类型检查。尽管我们之前认为显式转换是有用的，因为它们允许给出一个不依赖于类型检查的语义，但我们现在认为，假设隐式转换的情况下，也可以通过漂亮地打印代码来提高可读性。总之，我们向规范的读者提供了一个具有隐式状态、隐式上下文和隐式转换的版本。鉴于我们正在进行漂亮打印语法的游戏，我们借此机会切换到JS友好的语法，使用括号和分号。这个目标语言称为伪JS语法，它由JS语法的一个子集组成，扩展了单子符号表示法，并且具有一个扩展的switch结构，能够绑定变量（类似于OCaml的模式匹配，但为了简单起见，限制为非嵌套模式）。伪JS语法中加法运算符的漂亮打印如图7所示。为了说明我们的伪JS扩展模式匹配语法特性，我们在下面展示了一个从解释表达式的主switch中摘录的片段。0switch (t) {0case Coq_expr_identifier(x):0var % run r = identifier_resolution(x); return (r);0case Coq_expr_binary_op(e1, op, e2): ...03个生成跟踪的执行0JSExplain是一个用于交互式研究我们的JS解释器执行示例JS程序的执行跟踪的工具。界面由一个嵌入了JS解析器和一个用标准JS实现的生成跟踪版本的网页[8]组成。到目前为止，我们已经展示了如何将OCaml源代码转换为伪JS语法（§2.2）。在本节中，我们将解释如何将OCaml源代码转换为正确的JS语法，然后如何以系统化的方式为生成执行跟踪的JS代码进行仪器化。0图8展示了从我们的OCaml子集向JS的翻译输出。请注意，这段代码不适合人类阅读。我们将单子操作符实现为函数调用，必要时引入return关键字，使用带有tag字段的对象字面量来编码和类型，使用数组来编码元组（也可以使用对象字面量来编码元组），将构造函数应用转换为函数调用，通过首先切换到tag字段然后绑定新变量来实现模式匹配以表示构造函数的参数。因此，我们得到了一个在JS中可执行的JS解释器，就像我们在OCaml中的JS解释器一样，可以用于执行测试用例。JS版本的一个优点是它可以很容易地在浏览器中执行，这对于许多用户来说可能更方便。然而，一个限制是在不优化尾递归函数调用的JS虚拟机上，可以模拟的步骤数量可能有限。实际上，单子代码的执行涉及对延续的重复调用，其（尾调用）调用不必要地增加了调用堆栈。为了设置我们的交互式调试器，我们从我们的OCaml源代码生成了JS翻译的带有仪器的版本。这个带有仪器的代码根据解释输入的JS程序产生执行跟踪。这些跟踪存储了解释器经过的所有状态的信息。特别是，跟踪中的每个事件提供了有关代码指针和解释器代码中局部变量的实例化的信息。更准确地说，我们在每个函数的入口点、每个退出点和每个变量绑定处记录事件。每个事件在触发事件的解释器代码点捕获了作用域内解释器代码的状态、堆栈和所有局部变量的值。为了减少跟踪中的噪音，我们只记录解释器核心代码中的事件，而不记录辅助库中的代码。总的来说，对某个输入JS程序的带有仪器的解释器的执行会产生一个事件数组。然后可以使用我们的双调试器（§4）来研究这个数组。图9显示了一个代码片段的示例，给出了机制的一个概念。再次注意，这段代码不适合人类阅读。函数log_event增加了跟踪。例如，考虑log_event("Main.js", 4033, ctx_747,"enter")。前两个参数标识源文件中的位置，作为文件名和用于恢复行号的唯一标记。第三个参数是描述局部变量值的上下文，第四个参数描述事件的类型。在研究跟踪时，我们需要能够突出显示解释器代码的相应行。我们希望能够为解释器代码的三个版本实现这个功能：OCaml版本、伪JS版本和纯JS版本。为了实现这个功能，我们的生成器在处理OCaml源代码时，还会生成一个表，将每个版本和解释器的每个文件的事件标记映射到行号。事件中存储的上下文在每次进入函数、声明新变量或函数返回时都会扩展（以捕获返回的值）。上下文被表示为纯函数的链接列表，其中变量名和值之间的映射。这种表示最大化共享，从而最小化生成跟踪的内存占用。跟踪的长度随执行步骤的数量线性增长。例如，简单的程序“var i = 0; while (i < N) {i++ }”0Track: Web Programming WWW 2018, April 23-27, 2018, Lyon, France6970var run_binary_op_add = function (s0, c, v1, v2) {0return (if_prim(to_primitive_def(s0, c, v1), function (s1, w1) {0return (if_prim(to_primitive_def(s1, c, v2), function (s2, w2) {0if ((type_compare(type_of(Coq_value_prim(w1)), Coq_type_string()))0|| type_compare(type_of(Coq_value_prim(w2)), Coq_type_string())) {0return (if_string(to_string(s2, c, Coq_value_prim(w1)), function (s3, str1) {0return (if_string(to_string(s3, c, Coq_value_prim(w2)), function (s4, str2) {0return (res_out(Coq_out_ter(s4, res_val(Coq_value_prim(Coq_prim_string(strappend(str1, str2))))))); }));})); }else { ... }})); })); };0图8：不带跟踪仪器的标准JS语法解释器生成代码片段。0var run_binary_op_add = function (s0, c, v1, v2) {0var ctx_747 = ctx_push(ctx_empty, [{ key: "s0", val: s0 }, { key: "c", val: c }, { key: "v1", val: v1 }, { key: "v2", val: v2 }]); log_event("JsInterpreter.js",4033, ctx_747, "enter"); var _return_1719 = if_prim((function () { log_event("JsInterpreter.js", 3985, ctx_747, "call"); var
我的内容管理
展开
