From 1041d9dda3cadb0fc0e7dd395c780a5fa0bb7fe8 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Thu, 22 Oct 2026 00:23:45 +0100 Subject: [PATCH] Build each class's state machine once per checker The state machine only depends on specifications, which are all known before a checker starts, so it is built on the first state error in a class and reused for the next ones. Co-Authored-By: Claude Opus 5.5 --- .../refinement_checker/TypeChecker.java | 17 +++++++++++++++++ .../object_checkers/AuxStateHandler.java | 7 +++---- 2 files changed, 20 insertions(+), 4 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 776367d8..f0c51e18 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -2,6 +2,7 @@ import java.lang.annotation.Annotation; import java.util.Collections; +import java.util.HashMap; import java.util.List; import java.util.Map; import java.util.Optional; @@ -17,6 +18,9 @@ import liquidjava.processor.context.RefinedVariable; import liquidjava.processor.facade.AliasDTO; import liquidjava.processor.facade.GhostDTO; +import liquidjava.processor.state_machine.StateMachine; +import liquidjava.processor.state_machine.StateMachineBuilder; +import liquidjava.processor.state_machine.StateSolver; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.parsing.RefinementsParser; import liquidjava.smt.SMTEvaluator; @@ -49,6 +53,7 @@ public abstract class TypeChecker extends CtScanner { protected final Factory factory; protected final VCChecker vcChecker; private final Diagnostics diagnostics = Diagnostics.getInstance(); + private final Map> stateMachines = new HashMap<>(); public TypeChecker(Context context, Factory factory) { this.context = context; @@ -64,6 +69,18 @@ public Factory getFactory() { return factory; } + /** + * The state machine of {@code className}, built once per checker: the specifications it is built from are all known + * before a checker starts + */ + public Optional getStateMachine(String className, CtElement element) throws LJError { + if (!stateMachines.containsKey(className)) { + StateSolver solver = new StateSolver(this, element.getPosition()); + stateMachines.put(className, StateMachineBuilder.build(this, solver, className, element)); + } + return stateMachines.get(className); + } + @Override public void scan(CtElement element) { try { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 18555583..69eb89ff 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -659,12 +659,11 @@ private static List stateHints(TypeChecker tc, RefinedFunction function, S if (receiver.isEmpty() || !StateMachineBuilder.canModel(function)) return List.of(); try { - StateSolver solver = new StateSolver(tc, invocation.getPosition()); - Optional machine = StateMachineBuilder.build(tc, solver, function.getTargetClass(), - invocation); + Optional machine = tc.getStateMachine(function.getTargetClass(), invocation); if (machine.isEmpty()) return List.of(); - Set current = solver.possibleStates(machine.get().states(), state, instanceName); + Set current = new StateSolver(tc, invocation.getPosition()).possibleStates(machine.get().states(), + state, instanceName); return StateHints.forCall(machine.get(), function, current, receiver.get()); } catch (RuntimeException e) { // a failure to compute hints must not replace the error being reported