PKU Software Analysis — Pointer Analysis & Program Synthesis

Two program-analysis systems built from the course skeletons of 北京大学 软件分析技术 (Peking University — Software Analysis) by 熊英飞 (Xiong Yingfei), part of a csdiy.wiki full-catalog build.

Overview

The course's two hands-on projects are both implemented in full and verified with the course's own oracles:

1. Project 1 — Pointer Analysis (project1-pointer-analysis/): an Andersen-style, field-sensitive, interprocedural pointer-analysis system for Java, built on SOOT. It reads a benchmark whose allocation sites and query points are tagged with BenchmarkN.alloc(id) / BenchmarkN.test(id, var) markers and writes, for each query, the set of allocation-site ids the variable may point to. The analysis is written from scratch — SOOT's own pointer analysis (Spark) is not used, only its Jimple IR and call-graph construction.

2. Project 2 — SyGuS Program Synthesis (project2-sygus-synthesis/): a CEGIS + EUSolver-style decision-tree synthesizer for Syntax-Guided Synthesis problems (SyGuS-IF, LIA). It replaces the course baseline's naive top-down enumeration with observational-equivalence-pruned enumeration and a divide-and-conquer decision-tree learner, using Z3 as the verification oracle.

The written/theory exercises are summarised in notes/theory-assignments.md.

Results (measured on Windows, JDK 21, Python 3.11, CPU)

Project 1 — pointer analysis (exact-match against the course examples)

Benchmark	Exercises	Result (measured)
test.Hello	local copy + branch join	1: 1 2 / 2: 3 — matches the course spec's example output
test.FieldSensitivity	field sensitivity + interprocedural assign(a,c) + constructor this.f=b	1: 0 1 / 2: 0 5 / 3: 0 6 — sound & precise
test.VirtualDispatch (custom)	virtual dispatch + return-value flow + getter	1: 1 2 / 2: 3 / 3: 4

Full run logs and result.txt outputs are under results/project1/.

Project 2 — SyGuS synthesis (Z3-verified)

32 of 33 open benchmarks are solved and independently re-verified with Z3 (verify.py): every array_search_* (2–15), every max* (max2–max15, max_11), s2, s3, three (f(x) = (x·3) mod 10), and tutorial. Times range from under a second to ~40 s. The full solve-and-verify table is in results/project2/run_all.txt.

The single unsolved benchmark, s1.sl, is a documented partial — see Deviations.

Implemented assignments

• Project 1 — Pointer analysis — Andersen inclusion-constraint solver with new / copy / cast, instance & static field load-store (field-sensitive), array load-store, and interprocedural parameter/this/return binding with on-the-fly virtual dispatch (CHA).
• Project 2 — SyGuS synthesis — CEGIS with bottom-up OE-pruned enumeration and an EUSolver-style decision-tree learner; SMT-LIB Euclidean div/mod; structured dominance predicates for max-of-N.
• Theory notes — data-flow (monotone framework, MOP vs MFP), interprocedural (call-strings vs IFDS/summaries), abstract interpretation (Galois connection, intervals, widening), SAT/SMT (DPLL(T)), synthesis families.

Project structure

pku-software-analysis/
├── project1-pointer-analysis/      # SOOT-based Java pointer analysis (Maven)
│   ├── pom.xml                     # builds a runnable fat jar: target/analyzer.jar
│   ├── src/main/java/pku/
│   │   ├── Main.java               # CLI driver (java -jar analyzer.jar [src] [Main])
│   │   ├── PointsToTransformer.java# Jimple walk + constraint gen + call binding
│   │   ├── AnswerPrinter.java      # writes result.txt
│   │   └── core/
│   │       ├── Pointer.java        # locals / fields / static fields / array cells
│   │       └── PointerAnalysis.java# worklist Andersen solver
│   └── benchmark/                  # course example programs + markers (rt.jar gitignored)
├── project2-sygus-synthesis/       # SyGuS synthesizer (Python + Z3)
│   ├── main.py  verify.py  run_all.py
│   ├── synthesizer.py              # CEGIS loop
│   ├── dt_synth.py                 # EUSolver-style decision-tree learner
│   ├── enumerator.py sexp.py       # grammar model, evaluator, parser
│   ├── translator.py               # course Z3 checker (verification oracle)
│   └── tests/                      # 33 SyGuS-IF benchmarks
├── notes/theory-assignments.md
└── results/

How to run

Project 1 (pointer analysis)

Requires JDK 21 and Maven; SOOT 4.6.0 is pulled from Maven Central. The benchmark needs a JDK-1.7 rt.jar + jce.jar on SOOT's class path (Oracle-copyrighted, so git-ignored — copy them into project1-pointer-analysis/benchmark/ from any JDK 7 / OpenJDK 7 install, or the course's course_project_1.zip).

cd project1-pointer-analysis
mvn -B package                       # -> target/analyzer.jar (a fat jar)
java -jar target/analyzer.jar benchmark test.Hello
cat result.txt                       # 1: 1 2 / 2: 3
java -jar target/analyzer.jar benchmark test.FieldSensitivity
java -jar target/analyzer.jar benchmark test.VirtualDispatch

Project 2 (SyGuS synthesis)

Requires Python 3.11 and z3-solver.

cd project2-sygus-synthesis
python -m pip install z3-solver       # or reuse the shared csdiy venv
python main.py tests/max5.sl          # prints a (define-fun ...)
python verify.py tests/max5.sl "$(python main.py tests/max5.sl)"   # -> CORRECT
python run_all.py                     # solve + Z3-verify every benchmark

Verification

• Project 1 is validated by exact-matching the course specification's worked example (test.Hello → 1: 1 2 / 2: 3) and by hand-derived ground truth for the field-sensitive / interprocedural test.FieldSensitivity and the custom test.VirtualDispatch. Captured runs live in results/project1/.
• Project 2 is validated by the course's own Z3 checker: run_all.py synthesizes each benchmark and verify.py re-checks the result independently (an unsat on ¬spec certifies correctness for all inputs). 32/33 report CORRECT; see results/project2/run_all.txt.

Deviations / partials

• SOOT version. The course ships a 2015 soot-trunk.jar; its malformed ./ zip entry makes JDK 21's class-path reader reject it, so this repo depends on the maintained org.soot-oss:soot:4.6.0 instead. It exposes the same Jimple/CFG/call-graph API and, crucially, we still implement the pointer analysis ourselves rather than calling SOOT's Spark.
• s1.sl (Project 2). Unsolved within the time budget. Its constraints apply the target function to both fixed constants (f(0)=0 … f(5)=50) and a symbolic variable (f(x)=x for x>5), so a single example induces multiple argument tuples — the per-point decision-tree model does not apply, and plain enumeration cannot reach the ~size-20 lookup ite. All other 32 benchmarks (including every array_search_* and max*) are solved and Z3-verified.

Tech stack

Java 21, SOOT 4.6.0, Maven (shade plugin) · Python 3.11, Z3 (z3-solver).

Key ideas / what I learned

• Andersen pointer analysis as an inclusion-constraint system solved to a least fixed point with a worklist; field sensitivity via allocation-site-keyed abstract objects; interprocedural flow via on-the-fly call binding.
• Why SOOT models A a = new A() as tmp = new A; a = tmp and how the alloc(id) marker attaches an allocation-site id to the following new.
• CEGIS: separate synthesis (cheap, concrete, example-driven) from verification (expensive, symbolic, Z3), letting counter-examples drive refinement.
• Observational-equivalence pruning must be measured over the synth-fun's own parameter space, and EUSolver's divide-and-conquer decision-tree learning turns intractable ite-heavy grammars into fast decision-tree synthesis — with structured dominance predicates the key to making max-of-N converge.

Credits & license

Based on the projects of 软件分析技术 (Software Analysis) by 熊英飞 (Xiong Yingfei), Peking University — course site. This repository is an independent educational reimplementation; all course materials, skeletons and benchmarks belong to their original authors. Original code here is released under the MIT License.