【正文】 Chord: A Versatile Platform for Program Analysis Mayur Naik Intel Labs, Berkeley PLDI 2020 Tutorial What is Chord? ? Static and dynamic program analysis framework for Java ? Started in 2020 as static Checker of races and deadlocks ? Publicly available under New BSD License ? Key goals: – versatile: applies to various analyses, domains, platforms – extensible: users can build own analyses atop given ones – productive: facilitates rapid prototyping of analyses – robust: deterministic, handles partial programs, etc. Key Features of Chord ? Many standard static and dynamic analyses ? Writing/solving analyses using Datalog/BDDs ? Analyses as “building blocks” ? Contextsensitive static analysis framework ? Dynamic analysis framework Outline of Tutorial ? Part 1: ? Getting Started With Chord ? Program Representation ? Part 2: ? Analysis Using Datalog/BDDs ? Chaining Analyses Together ? Part 3: ? ContextSensitive Analysis ? Dynamic Analysis Downloading Chord ? Stable Binary Release – ? Stable Source Release 1. (mandatory) – Chord?s source code + JARs of libraries used by Chord 2. (optional) – (adapted) Java source code of libraries used by Chord ? Latest Development Snapshot svn checkout chord Or checkout only relevant directories under trunk/: – main/ (released as 1 above) – libsrc/ (released as 2 above) – test/ (Chord?s regression test suite) – … (many more) Compiling Chord ? Requirements: – JVM for Java 5 or higher – Apache Ant – C++ piler (not needed by default) ? Optional: edit – to enable C BuDDy library: set =true – to enable C++ JVMTI agent: set =true ? Run in main directory: ant pile main/ agent/ bdd/ doc/ examples/ lib/ src/ web/ | | Running Chord ? Requirements: JVM for Java 5 or higher ? no other dependencies (., Eclipse) ? Run either mand in any directory: ? ant –f .../ [–Dkeyi=vali]* run ? requires Apache Ant ? not available in Binary Release ? java –cp …/ [–Dkeyi=vali]* where … denotes path of Chord?s main/ directory –Dkeyi=vali sets value of system property keyi to vali Chord Properties ? All inputs to Chord are specified via System Properties ? conventionally named chord.* (., ) ? Three choices with decreasing precedence: 1. On mand line via –Dkey=val format ? use to specify properties specific to the current Chord run 2. Via userspecified file denoted by ? use to specify properties specific to program being analyzed (. its main class, classpath, etc.) ? default value = []/ 3. Via predefined file main/ ? use to specify properties that must hold in every Chord run (., maximum memory to be used by JVM) Architecture of Chord Classic or Modern Runtime bytecode translator (joeq) bytecode instrumentor (javassist) saxon XSLT bddbddb BuDDy Java2HTML static analysis Datalog analysis dynamic analysis program bytecode domain D1 relation R12 relation R1 domain D2 relation R2 analysis result in XML analysis result in HTML program source program quadcode relation R12 analysis program inputs domain D1 analysis domain D2 analysis example program analysis Java program user demands this to run starts, blocks on R2, D2 starts, runs to finish starts, runs to finish ? ? ? ? ? starts, blocks on D1, D2, R1, R12 starts, blocks on D1 resumes, runs to finish resumes, runs to finish starts, blocks on D1 resumes, runs to finish resumes, runs to finish Setting Up a Java Program for Analysis Command to run in Chord?s main directory: ant –=…/example run example/ src/ foo/ ... classes/ foo/ ... lib/ src/ taz/ ... jar/ chord_output/ bddbddb/ = =classes:lib/jar/ =src:lib/src =0,1 =thread 1 n 10 =thread 2 n 50 Java Program Representations Java source code .java Java bytecode .class javac Disassembled Java bytecode javap Example: Java Source Code 1: package test。 2: 3: public class HelloWorld { 4: public static void main(String[] args) { 5: (Hello World!)。 6: } 7: } File test/: PrettyPrinting Java Bytecode public class extends Constant pool: const 1 = Method 6.20。 // java/lang/Object.init:()V ... public static void main([])。 Code: Stack=2, Locals=1, Args_size=1 0: getstatic 2。 // Field java/lang/:Ljava/io/PrintStream。 3: ldc 3。 // String Hello World! 5: invokevirtual 4。 // Method java/io/:... 8: return javap –private –verbose –classpath CLASS_PATH [–bootclasspath BOOT_CLASS_PATH] CLASS_NAME SourceFile: LineNumberTable: line 5: 0 line 6: 8 LocalVariableTable: Start Length Slot Name Signature 0 9 0 args [Ljava/lang/String。 Run javac –g on .java files to keep debug info (lines, vars, source) in .class files Java Program Representations Java source code .java Quadcode Java bytecode .class javac Joeq Disassembled Java bytecode javap PrettyPrinting Quadcode Class: Method: main:([Ljava/lang/String。) 01 53 52 84 Control flow graph: BB0 (ENTRY) (in: none, out: BB2) BB2 (in: BB0 (ENTRY), out: BB1 (EXIT)) 1: GETSTATIC_A T1, .out 3: MOVE_A T2, AConst: Hello World! 2: INVOKEVIRTUAL_V println:(Ljava