项目进展不足，拖延有余。

目前我已经了解了 Scala 的基本用法和 SAFE 2.0 的源代码结构。总体来说 SAFE 新版的 generality 还是比较高的。

一个有趣的问题

safe 如果不手动通过选项指定 context-sensitivity，则 k （CFA 的 call limit）默认为 0。也就是说，每个 call-site 都会在函数 exit edge 的 propagation 目标里面。简单来说，就是每次分析一个调用，以前的调用点的调用完成后 state 都会受到影响。这样不仅仅不精确，而且效率非常差（quaradic）。比如下面的程序：

function f() {
    return 1;
}

f(); f(); f(); f(); f();
f(); f(); f(); f(); f();
f(); f(); f(); f(); f();

分别为 k = 0 和 k = 1 时的费时差距极大。

当 k = 1 时，进入函数时 call trace 也是状态的一部分，所以在结束时可以“返回”正确的调用点 – 也就是说返回时的 propagation 只会影响一个 callsite 而不是所有的。

SAFE 源码重点分析

简而言之，我需要知道 “call a function” 这个 AST expression node 被分析器遇到时，所引发的动作（control），以及我能得到的分析器中的数据类型（data）。

在 SAFE 2.0 中，这不显然。

首先我们从 Safe.scala 看起 – 这个 object 的 main 函数中按照功能选择对应的模块，我们关心的 analyze 功能，所以看 Analyze.scala 的部分。

在 Analyze.apply 中，一系列初始化动作被触发：

  • register all kinds of configurations
  • initialize (abstract) state from CFG
  • handle special modes
    • Test: addTest
    • DOM modeling: addDOM
  • Call context initialization
  • Set up the global entry, add it into the initialized worklist
  • Initialize semantics (which is approx. “transfer functions”) with CFG
  • Start up fix-point computing (it looks like just a naïve chaotic iteration, without much heuristics involved)

我们关系的是两部分：

  1. DOM modeling 是怎么做的（DOM 相对于 JS 来说是额外的环境信息，xWIDL 相当于 generalize 这种运行环境）
  2. compute 中函数调用时怎么处理的

From DOM modeling to Built-in functions

打开这个 dom.Document，你会发现一个大写的 TODO，然后就没了。但是返回上一层源码目录 models，这里有所有的 “modelling” 部分，包括对 JS primitive values 的 model，对 object 的 model, 对 function 的 model 等等。在往上翻一层，另一个 module 叫做 builtin，里面是对大量 JS 内置函数行为的 hard-coding，这正是我们针对的目标。

我们来看下 FuncModel.scala，这里记载了初始化 heap 并最后 newFunctionObject 的过程。但是这似乎并不能处理 API 的问题 – 因为 fid 是从 CFG 里来的！（val func = code.getCFGFunc(cg, name)）。

重新看 Initialize 中初始化的过程，会有 BuiltinGlobal.initHeap(initHeap, cfg) 这一句，其中 BuiltinGlobal 作为一个 abstract object，其 properties（数据或函数成员）已经写死。

所以，BuiltIn 中指定函数行为的方式是通过初始化 BasicCode 中的一个 (AbaValue, AbsState) -> (AbsState, AbsState, AbsValue) 的闭包实现。我们只需要将这个 PureCode 改成自己想要的即可。

Fix-point computation

数据流分析的核心是对 state 的抽象 – 一个 CFG node 的 state 可以是所有执行路径经过这个节点时的 state 综合（summary），也可以是某个 call context 上所有 intra-procedural 的路径综合，也可以是对分支敏感的路径综合。同时，这种 summarization 一般来说是一种 efficiency 和 precision 的 trade-off，为了提升效率（节省存储状态的空间，加快状态合并的计算），也为了保证终止性，一般会将 state 抽象成一个 finite-height semi-lattice 模型，一个 trivial 的例子是整数：

    ___ Top ___
  /      |      \
 /       |       \
Pos     Zero    Neg
 \       |       /
  \____  |  ____/
        Bot

一个不怎么 trivial 的例子是 heap。

回到正题，Fixpoint.compute 中的核心一步在于 semantics.C(cp, st)，这一步相当于一步计算，返回了之后的新状态（一般来说这一步叫做 transfer functions，但是 SAFE 似乎用 OOP 包装了一下所以 function 不是很明显）。

进入 C 中，可以找到 call: Call => CI(cp, call.callInst, st, AbsState.Bot) ，于是便找到了处理函数调用的 CI。CI 比较复杂，要为每一个这个名字可能指向的函数（论 points-to analysis 的重要性）加入新的 call edge。

这里我们知道关键在于 getFunc 是怎么工作的。每个函数，不管是 built-in 还是 user space，都可以看作一个 callable object，所以通过名字得到 location set 之后，还要进一步通过 abstract heap 映射得到 abstract object, 但是这个 object 是抽象的 – 又可以代表很多 function，所以进一步对每个 fid 去分析。

目前修改的部分

目前已经加入的部分是：

  • Interface 和相关的 xWIDL 抽象语法树：不完全，但每个节点都实现了输出成 Dafny 的对应实现的翻译部分
  • ObjBuilder – 通过接口定义检查函数调用情况
    • 已经可以检查类型和参数数目的问题
  • XWIDLCode – 类似 PureCode，但是包装的是基于接口定义检查函数
  • askDafny – 与 Dafny 的通信模块
  • PPrint – 根据 A Prettier Printer 在 Scala 中重新实现的 pretty printing combinator 库
  • 散落在各个抽象值定义中的 concretization 为 expression 的过程，如 AbsBool.pack
  • 用 Declarative 的 Interface Spec 来重写原有的 Math 定义

一些简单的函数，如 Math.abs，已经可以生成靠谱的 Dafny 代码。

有趣的一点是，相比我在 TAJS 开发原型时的”完全替代”，这次通过一个 optSem 可以保留对函数抽象语义建模的选项（相比 SMT 求解更高效），但是由于已经做过 generalized type checking，所以实现起来 boilerplates 更少。

下一步计划：

  • Variadic function 如何处理
  • 如何输出有用的 type check 信息
  • xWIDL 的其他功能