Google Summer of Code 2025 Final Work Product

Modernizing Java PathFinder Extensions: Support for Java 11/17 Features

Student

Mahmoud Khawaja

Mahmoud-Khawaja

mahmoud.khawaja97@gmail.com

Project Details

Organization: The JPF team

Mentor: Cyrille Artho

Duration: May - September 2025

Project Abstract

This project successfully modernized the Java PathFinder (JPF) ecosystem to support Java 11 and Java 17 features, addressing critical compatibility issues that prevented JPF from analyzing contemporary Java applications.

Over five months, I implemented 16 significant pull requests across three key repositories: JPF-Core (14 PRs), JPF-NAS (1 comprehensive PR), and JPF-NHandler (1 PR).

Java Records Support

Automatic method generation with deep equality checking

Bootstrap Methods

Dynamic method invocation for modern Java features

Sealed Classes

Inheritance constraints and validation for Java 17

SharedSecrets

Java 11+ networking compatibility interfaces

Build Modernization

Complete migration from Ant to Gradle

Testing Framework

Enhanced CI/CD with parallel testing

JPF-Core Contributions

14 Pull Requests - Foundation Engine Modernization

PR # Title & Link Description
#556 Enhanced SharedSecrets for Java 11 integration Added JavaNetInetAddressAccess and JavaSecurityAccess interfaces to SharedSecrets with missing accessor methods for Java 11 compatibility
#554 Added direct execution for records Implemented direct execution optimization for Java record types in INVOKEDYNAMIC bytecode handling
#553 Added JavaNetSocketAccess support to SharedSecrets Added socket access support to SharedSecrets for network-related JPF extensions to function with Java 11
#552 Added the direct approach for handling lambda Implemented direct approach for lambda expression handling with enhanced bootstrap method processing
#550 String concat call site Implemented call site generation for string concatenation operations using StringConcatFactory
#545 Sealed classes full Complete implementation of Java 17 sealed classes with inheritance constraints and validation
#543 Enabled ParallelTesting Enhanced build system with parallel testing capabilities and improved CI/CD workflows
#540 Fixed the field access for records Fixed field access mechanisms for Java record types with proper final field handling
#530 Adding support for internals Major implementation of Java record internals including bootstrap methods, equals(), hashCode(), toString()
#528 Class version check Updated class version validation to accept Java 17 bytecode (version 61)

Technical Highlights

Java Records Implementation

  • Automatic generation of equals(), hashCode(), and toString() methods
  • Deep equality checking for complex types and arrays
  • Generic record support with proper type parameters
  • Integration with JPF's object lifecycle management

Bootstrap Methods & Call Sites

  • StringConcatFactory for modern string concatenation
  • LambdaMetafactory for dynamic lambda initialization
  • Method handle resolution for dynamic invocation
  • Direct execution optimization for record methods

Sealed Classes Support

  • Compile-time and runtime constraint validation
  • Inheritance restriction enforcement
  • Permitted subclasses declaration handling
  • Pattern matching infrastructure foundation

JPF-NAS Contributions

1 Comprehensive Pull Request - Network Simulation Modernization

#5

Gradle support

Comprehensive migration to Gradle build system with Java 11 support, including 24 commits covering build modernization, socket implementation, and peer class development

+1,952 additions -1,202 deletions

Technical Implementation

Build System Modernization

  • Complete Gradle migration with Java 11 compatibility
  • Automated testing with JUnit framework integration
  • GitHub Actions CI/CD workflow implementation
  • Custom JAR creation for model classes and examples

Java 11 Socket Support

  • JPF_java_net_PlainSocketImpl: Socket initialization
  • JPF_java_net_InetAddress: Address management
  • JPF_java_net_SocketCleanable: Resource cleanup
  • JPF_jdk_internal_ref_CleanerFactory: Cleaner integration

Critical Compatibility Resolution

  • Fixed SharedSecrets NoSuchMethodException issues
  • Resolved module system conflicts with --patch-module
  • Implemented ExtendedSocketOptions peer classes
  • Enhanced classpath configuration for JPF testing

JPF-NHandler Contributions

1 Pull Request - Native Method Handling Modernization

#15

Gradle java 11

Migrated build system to Gradle with Java 11 compatibility, resolved API dependencies, and excluded deprecated Google Translate examples

Java 11 Compatibility Dynamic Path Resolution API Cleanup Integration Testing

Impact & Results

Immediate Benefits

  • Modern Java Support: JPF can analyze Java 11/17 applications with Records, Sealed Classes, and enhanced APIs
  • Framework Compatibility: Support for contemporary frameworks using modern Java features
  • Build Modernization: Improved development workflow through Gradle and GitHub Actions
  • Performance Enhancement: Parallel testing and optimized bootstrap method handling

Long-term Value

  • Community Growth: Expanded user base to modern Java developers
  • Future Foundation: Established patterns for upcoming Java version support
  • Best Practices: Enhanced documentation, testing, and build practices
  • Ecosystem Health: Modernized infrastructure for sustained development

Major Challenges & Solutions

Java Module System Integration

Challenge: Conflicts between JPF model classes and JPMS

Solution: Implemented --patch-module compilation approach

Bootstrap Method Complexity

Challenge: Understanding JVM invokedynamic instructions

Solution: Created robust call site generation framework

SharedSecrets API Changes

Challenge: Java 11 NoSuchMethodException issues

Solution: Implemented proper interface registration

Record Type Semantics

Challenge: Ensuring JVM-precise method generation

Solution: Comprehensive implementation with lifecycle integration

Complete Technical Documentation

Access the comprehensive technical report with detailed implementation analysis, code examples, and complete project documentation.

Download Complete Technical Report (PDF)

Primary Repositories

JPF-Core JPF-NAS JPF-NHandler