Algebraic Data Types for Object-oriented Datalog

Value lookup(Context ctxt, Parameter p) { exists(Function f, int i | appliesTo(ctxt, f) and p = f.getParameter(i) and result = get(ctxt, i)) } With these preparations out of the way, we now show three representative clauses of the eval predicate: analysis of numeric literals as an example of a simple base case (where we use appliesTo to restrict the range of the otherwise unused parameter ctxt), and the two crucial cases of parameter and return value passing. To analyse a use of a parameter p we look it up in the context; to analyse a function call, we construct the appropriate calling context, and use the auxiliary predicate retval to determine the possible return values of the callee in that context. That predicate, in turn, considers the return statements in the function to determine possible return values: AbstractValue eval(Context ctxt, Expr e) { e instanceof NumberLiteral and appliesTo(ctxt, e.getEnclosingFunction()) and result = Number() or exists(SimpleParameter p | e = p.getVariable().getAnAccess() and result = ctxt.lookup(p)) or exists(Function f | calls(ctxt, e, f) and result = retval(evalArgs(ctxt, e, f, 0), f)) or ... } AbstractValue retval(Context ctxt, Function f) { exists(ReturnStmt ret | ret = f.getAReturnStmt() and result = eval(ctxt, ret.getExpr())) }Value retval(Context ctxt, Function f) { exists(ReturnStmt ret | ret = f.getAReturnStmt() and result = eval(ctxt, ret.getExpr())) } Extending these predicates to model all of ECMAScript 2016 is a non-trivial task, but takes no more than about 500 lines of QL. We want to emphasise, however, that we do not mean to claim that CPA is a silver bullet for the analysis of JavaScript, the challenges of which are manifold and extensively documented in the literature (Jensen et al. 2009; Kashyap et al. 2014; Park and Ryu 2015; Schäfer et al. 2013; Sridharan et al. 2012), we simply use it as an example of a non-trivial context sensitivity policy that nicely demonstrates the use of recursive algebraic data types: since contexts can be lists of arbitrary length, it is not clear how they could be represented in plain QL. 6.2 Constructing control flow graphs As our next example, we show how to construct intra-procedural control ow graphs for programs written in a very small subset of Java, comprising just four kinds of statements: expression statements, throw, try with catch (but no finally) and block statements. We ignore any control ow resulting from expression evaluation. The CFG contains one node for each statement, plus one entry node and one exit node for each callable (that is, method or constructor): newtype CfgNode = StmtNode(Stmt s) or EntryNode(Callable c) or ExitNode(Callable c) CFG edges are labelled with completions that indicate the reason for the ow. We have two kinds of completions: the normal completion indicating normal termination of a statement; and throw completions, indicating that a statement has thrown an exception: , Vol. 1, No. 1, Article 1. Publication date: April 2017.