Ridiculously Generic Program Analysis Overview
Analyzing the challenges and goals of the Ridiculously Generic Program Analysis by James Koppel from MIT. Exploring problems faced, ideas for improvement, and the concept of parametric interpretation. Unveiling the ambitions to define analyzers semantically, share knowledge automatically, and combine different tools efficiently.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Ridiculously Generic Program Analysis James Koppel, MIT
Actually writing a static analyzer Value val=null; if (left==NullConstant.v()) { if (right!=NullConstant.v()) { val = right; } } else if (right==NullConstant.v()) { if (left!=NullConstant.v()) { val = left; } } NullnessAnalysis Source: Soot Framework if (val!=null && val instanceof Local) { if (eqExpr instanceof JEqExpr) //a==null handleEquality(val,outBranch); else if .. }
Problems Syntactic pattern-matching Runs on IR Lots of cases; easy to miss Specific to one version of one language Must hard-code use of other analyzers
Goals Define analyzers semantically Derive most of tool automatically Reuse work between languages Reuse work between tools Analyzers can automatically share knowledge
Ideas Parametric interpretation, parametric syntax From one program, multiple tools for multiple languages Type-level obligations Constrain what analyzers and languages may combine Generalized nodes One type definition gives AST, CFG, etc Modular monadic semantics Automatically combine different analyzers Monads without lambdas!
General Type public interface Exp<C,L,S> { .} Eval Context Language Sort
Parametric Interpretation Interpreter cond.eval(); // returns false elseBranch.eval(); ConcreteEvalContext Compiler <cond code> test eax jnz else_branch <stmt 1 code> jmp end else_branch: <stmt2 code> end: Single Source of Truth public class If { . public void eval(EvalContext ctx) { ctx.eval(cond).branch( () -> ctx.eval(thenBranch), () -> ctx.eval(elseBranch)); } } DeferredEvalContext Abstract boolean type Control flow graph FlowGraphContext Dataflow analysis Symbolic execution
Parametric Syntax (C_PP, Assign) Has (C_PP, Deref) ) Has (Java, Assign) Has public class Assign<L> { . public Assign(Var<L> lhs, Exp<L> rhs, Has<L, Assign> h) { . } }
Statically checking compatibility Assign[U Stateful[U]] CallCC[U Cont [U]] Each expression constrains what EvalContext s the program can run in prog :: c Stateful[c] Cont[c], Exp[c] prog[ConcreteEvalContext] prog[FlowGraphContext]
Generalized representation 1 + * x ConcreteExp public class BinOp extends ConcreteExp { private Exp lhs; private Exp rhs; } y z DataflowExp t1 := y *z t2 := x + t1
Generalized Representation 2 public class Seq<C> extends ConcreteExp<C, Void> { public ContextVal<C, Void> eval(C c) { } } public class IntLit<C> extends ConcreteExp<C, Integer> { public ContextVal<C, Integer> eval(C c) { } }
Monadic Combination Transfer: (Label -> Bool, Var -> NullnessLattice) -> (Var -> NullnessLattice, Label -> Bool) ReachabilityAnalyzer lift NullnessAnalyzer Transfer: (Var -> NullnessLattice) -> (Var -> NullnessLattice)
Monads without Lambdas public class Seq { public void eval(EvalContext ctx) { ctx.eval(stmt1); ctx.eval(stmt2); } } Could both be nondeterministic
Result: Nullness Analysis Analyzer a = new Analyzer(); a.addDataflowState( new NullnessLattice()); a.overrideTransferFunction( new BooleanConstantProp()); Evaluation will automatically case-split on (x == null) if (x != null || y != null) { } else { } Evaluate condition; propagate states to branches
