Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
112 changes: 30 additions & 82 deletions README.org
Original file line number Diff line number Diff line change
@@ -1,103 +1,51 @@
#+TITLE: Runtime Framework
* About

A Java Agent-based framework designed to enforce pluggable type systems at runtime. By instrumenting bytecode at load-time, the framework ensures that type contracts (such as @NonNull) are respected at the boundary between annotated and unannotated code. This provides a traceable safety net when integrating code verified by tools like the [[https://github.com/eisop/checker-framework][EISOP Checker Framework]] with legacy or unchecked external libraries.

** Project Structure
* About

- ~framework/~: The core agent and instrumentation logic.
- ~agent~: The Java Agent entry point and transformer.
- ~core~: The main instrumentation engine
- ~policy~: Defines /when/ checks are injected.
- Currently, there are two defined policies: a *Standard Policy* and a *Global Policy*.
- The **Standard Policy** instruments only code that has been marked as "Checked".
- The **Global Policy** extends this to instrument Unchecked code as well.
- ~resolution~: Handles class hierarchy analysis for bridge methods.
- ~filter~: Controls which classes are instrumented.
- ~runtime~: The runtime library that instrumented code calls.
- ~checker/~: Concrete implementations of type systems (currently Nullness).
- ~test-utils/~: Shared testing infrastructure for writing integration tests.

** Requirements
The EISOP Runtime Framework is an experimental, work-in-progress framework for enforcing and supporting Java annotated type systems at runtime.

This project requires JDK25+.
It utilizes Java agents to instrument bytecode at class load time. The current focus is gradual typing for pluggable type systems, especially those built with the [[https://github.com/eisop/checker-framework][Checker Framework]].

** Status
* Requirements

This project is in early development and will still go through many breaking changes regarding API and configuration. Its overall design goal is to be flexible enough to support any pluggable type system but is currently focused on Nullness.
- JDK 25 or newer.

* Building the Project
* Build

This project uses Gradle 9.0. To build the agent and runtime libraries:
Build the agent, checker, and test artifacts:

#+begin_src bash
./gradlew build
#+end_src

Note: This will also run the test suite located under ~checker/src/test/java/~ (executing integration tests via ~NullnessDirectoryTest~).

This will generate the artifacts in ~build/dist/~:
- ~framework.jar~ (The Java Agent)
- ~checker.jar~ (The Runtime Nullness Checker)
- ~test-utils.jar~ (Testing helpers)
- ~checker-qual.jar~ (Annotations)

* Usage

To use the agent, you need to launch your Java application with the ~-javaagent~ flag and configure the classpath.

** 1. Standard Policy Example

There are two examples under ~examples/~ that demonstrate basic usage. These examples catch exceptions to print success messages instead of crashing, allowing you to see multiple violations in one run while still using the exception handler.

The **Standard Policy** example demonstrates instrumentation on only checked code, where checked code is defined as code within the scope of an ~AnnotatedFor~ annotation. This policy is limited insofar as it will not instrument code outside of an ~AnnotatedFor~ scope, leaving field wrties from unchecked to checked code and the checked parent, unchecked child relationship unaccounted for. However, limiting checks to only a checked scope could be prefered in some situations.
Build outputs are copied to ~build/dist/~. The important artifacts are:

To compile the standard policy example:
- ~framework.jar~: the Java agent and shared runtime framework.
- ~checker.jar~: the nullness runtime checker.
- ~checker-qual.jar~: Checker Framework qualifier annotations.
- ~test-utils.jar~: test helpers.

#+BEGIN_SRC bash
javac -cp 'build/dist/*' -d examples/standard-policy/ examples/standard-policy/*.java
#+END_SRC
* Running

To run the example:

#+BEGIN_SRC bash
java \
-javaagent:build/dist/framework.jar \
-Druntime.checker=io.github.eisop.runtimeframework.checker.nullness.NullnessRuntimeChecker \
-Druntime.trustAnnotatedFor=true \
-cp 'examples/standard-policy:build/dist/*' \
standard.StandardDemo
#+END_SRC


** 2. Global Policy Example

The global policy instruments both checked and unchecked code. It applies all the same checks present in the standard policy, but now field writes from unchecked -> checked and Checked Parent Unchecked child relationships can be handled accordingly.

To compile the global policy example:

#+BEGIN_SRC bash
javac -cp 'build/dist/*' -d examples/global-policy/ examples/global-policy/*.java
#+END_SRC

To run the example:
Run with the agent:

#+begin_src bash
java \
-javaagent:build/dist/framework.jar \
-Druntime.global=true \
-Druntime.checker=io.github.eisop.runtimeframework.checker.nullness.NullnessRuntimeChecker \
-Druntime.trustAnnotatedFor=true \
-cp 'examples/global-policy:build/dist/*' \
global.GlobalDemo
java \
-javaagent:build/dist/framework.jar \
-Druntime.checker=io.github.eisop.runtimeframework.checker.nullness.NullnessRuntimeChecker \
-Druntime.trustAnnotatedFor=true \
-cp 'out:build/dist/*' \
your.main.Class
#+end_src

** Configuration Properties
Enable global instrumentation mode when unchecked code also needs to be instrumented:

| Property | Description | Example |
|-----------------------------+-------------------------------------------------------------------------+--------------------------------------------------|
| ~runtime.checker~ | Fully qualified class name of the ~RuntimeChecker~ implementation. | ~...checker.nullness.NullnessRuntimeChecker~ |
| ~runtime.classes~ | Comma-separated list of classes to treat as "Checked" (Safe). | ~com.app.Main,com.app.Utils~ |
| ~runtime.global~ | ~true~ to enable Global Policy (scans all classes for external writes). | ~true~ |
| ~runtime.trustAnnotatedFor~ | ~true~ to automatically treat classes with ~@AnnotatedFor~ as Checked. | ~true~ |
| ~runtime.handler~ | ~ViolationHandler~ class to use (defaults to Throwing). | ~io.github.eisop.testutils.TestViolationHandler~ |
#+begin_src bash
java \
-javaagent:build/dist/framework.jar \
-Druntime.global=true \
-Druntime.checker=io.github.eisop.runtimeframework.checker.nullness.NullnessRuntimeChecker \
-Druntime.trustAnnotatedFor=true \
-cp 'out:build/dist/*' \
your.main.Class
#+end_src
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
package io.github.eisop.runtimeframework.checker.nullness;

import io.github.eisop.runtimeframework.config.RuntimeOptions;
import io.github.eisop.runtimeframework.core.RuntimeChecker;
import io.github.eisop.runtimeframework.semantics.CheckerSemantics;

Expand All @@ -16,4 +17,9 @@ public String getName() {
public CheckerSemantics getSemantics() {
return SEMANTICS;
}

@Override
public CheckerSemantics getSemantics(RuntimeOptions options) {
return new NullnessSemantics(options.trustExplicitQualifiers());
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -8,10 +8,19 @@
/** Nullness runtime semantics expressed through contracts and property emission. */
public final class NullnessSemantics implements CheckerSemantics {

private final TypeMetadataResolver typeMetadata = new NullnessTypeMetadataResolver();
private final ContractResolver contracts = new NullnessContractResolver(typeMetadata);
private final TypeMetadataResolver typeMetadata;
private final ContractResolver contracts;
private final PropertyEmitter emitter = new NullnessPropertyEmitter();

public NullnessSemantics() {
this(true);
}

public NullnessSemantics(boolean trustExplicitQualifiers) {
this.typeMetadata = new NullnessTypeMetadataResolver(trustExplicitQualifiers);
this.contracts = new NullnessContractResolver(typeMetadata);
}

@Override
public ContractResolver contracts() {
return contracts;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,15 @@ public final class NullnessTypeMetadataResolver implements TypeMetadataResolver

private static final String NON_NULL_DESC = NonNull.class.descriptorString();
private static final String NULLABLE_DESC = Nullable.class.descriptorString();
private final boolean trustExplicitQualifiers;

public NullnessTypeMetadataResolver() {
this(true);
}

public NullnessTypeMetadataResolver(boolean trustExplicitQualifiers) {
this.trustExplicitQualifiers = trustExplicitQualifiers;
}

@Override
public TypeUseMetadata resolve(TargetRef target, ResolutionContext context) {
Expand Down Expand Up @@ -91,6 +100,9 @@ private TypeUseMetadata methodParameterTypeUse(MethodModel method, int parameter
if (!isReferenceDescriptor(descriptor)) {
return TypeUseMetadata.empty(descriptor);
}
if (!trustExplicitQualifiers) {
return TypeUseMetadata.empty(descriptor);
}

List<TypeUseQualifier> qualifiers = new ArrayList<>();
method
Expand Down Expand Up @@ -123,6 +135,9 @@ private TypeUseMetadata methodReturnTypeUse(MethodModel method) {
if (!isReferenceDescriptor(descriptor)) {
return TypeUseMetadata.empty(descriptor);
}
if (!trustExplicitQualifiers) {
return TypeUseMetadata.empty(descriptor);
}

List<TypeUseQualifier> qualifiers = new ArrayList<>();
method
Expand Down Expand Up @@ -179,6 +194,9 @@ private TypeUseMetadata fieldTypeUse(FieldModel field) {
if (!isReferenceDescriptor(descriptor)) {
return TypeUseMetadata.empty(descriptor);
}
if (!trustExplicitQualifiers) {
return TypeUseMetadata.empty(descriptor);
}

List<TypeUseQualifier> qualifiers = new ArrayList<>();
field
Expand All @@ -201,6 +219,10 @@ private TypeUseMetadata fieldTypeUse(FieldModel field) {

private TypeUseMetadata localTypeUse(
TargetRef.Local target, String descriptorHint, ResolutionContext context) {
if (!trustExplicitQualifiers) {
return TypeUseMetadata.empty(descriptorHint);
}

List<TypeUseQualifier> qualifiers = new ArrayList<>();
for (ResolutionEnvironment.LocalVariableTypeAnnotation localAnnotation :
context
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
package io.github.eisop.checker.nullness;

import io.github.eisop.runtimeframework.config.RuntimeOptions;
import io.github.eisop.testutils.RuntimeTestRunner;
import java.util.List;
import org.junit.jupiter.api.Test;

public class NullnessDirectoryTest extends RuntimeTestRunner {
Expand All @@ -13,6 +15,15 @@ public void testParameterScenarios() throws Exception {
false);
}

@Test
public void testUntrustedExplicitQualifierScenarios() throws Exception {
runDirectoryTest(
"nullness-untrusted-explicit-qualifiers",
"io.github.eisop.runtimeframework.checker.nullness.NullnessRuntimeChecker",
false,
List.of(systemProperty(RuntimeOptions.TRUST_EXPLICIT_QUALIFIERS_PROPERTY, false)));
}

@Test
public void testInvokeScenarios() throws Exception {
runDirectoryTest(
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
import io.github.eisop.runtimeframework.qual.AnnotatedFor;
import org.checkerframework.checker.nullness.qual.Nullable;

@AnnotatedFor("nullness")
public class NullableConstructorParameter {
public static void main(String[] args) {
// :: error: (Parameter 0 must be NonNull)
new NullableConstructorParameter(null);
}

NullableConstructorParameter(@Nullable String value) {}
}
28 changes: 28 additions & 0 deletions docs/todo.org
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
#+TITLE: Runtime Framework TODOs

* Framework-level explicit qualifier trust

The current first pass wires ~runtime.trustExplicitQualifiers~ through the Nullness checker:

#+begin_src java
@Override
public CheckerSemantics getSemantics(RuntimeOptions options) {
return new NullnessSemantics(options.trustExplicitQualifiers());
}
#+end_src

This is acceptable for the initial nullness-only implementation, but the flag is a framework-level
configuration concept. Before adding more checkers, move enforcement of this flag into the framework
semantics layer.

Suggested design:

- Add qualifier origin metadata, for example ~EXPLICIT~, ~DEFAULT~, and ~SYNTHETIC~.
- Make checker-specific resolvers mark explicit bytecode annotations as ~EXPLICIT~.
- Mark checker defaults, such as nullness default non-null, as ~DEFAULT~.
- Add a framework-owned semantics/type-metadata wrapper that filters ~EXPLICIT~ qualifiers when
~runtime.trustExplicitQualifiers=false~.
- Keep checker-specific logic responsible for identifying its qualifiers, but let ~RuntimeChecker~
apply the trust flag consistently for all checkers.
- Once this exists, remove the Nullness-specific boolean constructor path for explicit qualifier
trust.
Original file line number Diff line number Diff line change
Expand Up @@ -8,20 +8,23 @@ public record RuntimeOptions(
String checkedClasses,
boolean globalMode,
boolean trustAnnotatedFor,
boolean trustExplicitQualifiers,
String handlerClassName,
String checkerClassName,
boolean indyBoundaryEnabled) {

public static final String CHECKED_CLASSES_PROPERTY = "runtime.classes";
public static final String GLOBAL_MODE_PROPERTY = "runtime.global";
public static final String TRUST_ANNOTATED_FOR_PROPERTY = "runtime.trustAnnotatedFor";
public static final String TRUST_EXPLICIT_QUALIFIERS_PROPERTY = "runtime.trustExplicitQualifiers";
public static final String HANDLER_CLASS_PROPERTY = "runtime.handler";
public static final String CHECKER_CLASS_PROPERTY = "runtime.checker";
public static final String INDY_BOUNDARY_PROPERTY = "runtime.indy.boundary";

public static final String DEFAULT_CHECKED_CLASSES = "";
public static final boolean DEFAULT_GLOBAL_MODE = false;
public static final boolean DEFAULT_TRUST_ANNOTATED_FOR = false;
public static final boolean DEFAULT_TRUST_EXPLICIT_QUALIFIERS = true;
public static final String DEFAULT_HANDLER_CLASS = "";
public static final String DEFAULT_CHECKER_CLASS =
"io.github.eisop.runtimeframework.checker.nullness.NullnessRuntimeChecker";
Expand All @@ -41,6 +44,7 @@ public static RuntimeOptions defaults() {
DEFAULT_CHECKED_CLASSES,
DEFAULT_GLOBAL_MODE,
DEFAULT_TRUST_ANNOTATED_FOR,
DEFAULT_TRUST_EXPLICIT_QUALIFIERS,
DEFAULT_HANDLER_CLASS,
DEFAULT_CHECKER_CLASS,
DEFAULT_INDY_BOUNDARY_ENABLED);
Expand All @@ -56,6 +60,8 @@ public static RuntimeOptions fromProperties(Properties properties) {
stringProperty(properties, CHECKED_CLASSES_PROPERTY, DEFAULT_CHECKED_CLASSES),
booleanProperty(properties, GLOBAL_MODE_PROPERTY, DEFAULT_GLOBAL_MODE),
booleanProperty(properties, TRUST_ANNOTATED_FOR_PROPERTY, DEFAULT_TRUST_ANNOTATED_FOR),
booleanProperty(
properties, TRUST_EXPLICIT_QUALIFIERS_PROPERTY, DEFAULT_TRUST_EXPLICIT_QUALIFIERS),
stringProperty(properties, HANDLER_CLASS_PROPERTY, DEFAULT_HANDLER_CLASS),
stringProperty(properties, CHECKER_CLASS_PROPERTY, DEFAULT_CHECKER_CLASS),
booleanProperty(properties, INDY_BOUNDARY_PROPERTY, DEFAULT_INDY_BOUNDARY_ENABLED));
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,11 @@ public abstract class RuntimeChecker {
/** Returns the semantic model used by the framework planner for this checker. */
public abstract CheckerSemantics getSemantics();

/** Returns the semantic model used by the framework planner for this checker and option set. */
public CheckerSemantics getSemantics(RuntimeOptions options) {
return getSemantics();
}

public final RuntimeInstrumenter createInstrumenter(RuntimePolicy policy) {
return createInstrumenter(policy, RuntimeOptions.fromSystemProperties());
}
Expand All @@ -38,7 +43,7 @@ public RuntimeInstrumenter createInstrumenter(

public RuntimeInstrumenter createInstrumenter(
RuntimePolicy policy, ResolutionEnvironment resolutionEnvironment, RuntimeOptions options) {
CheckerSemantics semantics = getSemantics();
CheckerSemantics semantics = getSemantics(options);
HierarchyResolver resolver =
new BytecodeHierarchyResolver(info -> policy.isChecked(info), resolutionEnvironment);
return new EnforcementInstrumenter(
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
package io.github.eisop.runtimeframework.qual;

import java.lang.annotation.Documented;
import java.lang.annotation.ElementType;
import java.lang.annotation.Retention;
import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;

/**
* Indicates that this declaration should be treated as not annotated for the given type system.
*
* <p>This is the negative counterpart to {@link AnnotatedFor}. Scope resolution can use it to let
* narrower declarations opt out of a checked enclosing class or package.
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE, ElementType.METHOD, ElementType.CONSTRUCTOR, ElementType.PACKAGE})
public @interface UnannotatedFor {
/**
* Returns the type systems for which this declaration should be treated as unannotated.
*
* @return the type systems for which this declaration should be treated as unannotated
*/
String[] value();
}
Loading
Loading