diff --git a/client/src/types/context.ts b/client/src/types/context.ts index 3c5d4d23..90ec9d73 100644 --- a/client/src/types/context.ts +++ b/client/src/types/context.ts @@ -4,6 +4,7 @@ import { SourcePosition } from "./diagnostics"; export type LJVariable = { name: string; + displayName: string; // as error messages name it, such as x@12 for the value x takes at line 12 internalName: string; type: string; refinement: string; @@ -19,6 +20,7 @@ export type LJGhost = { parameterTypes: string[]; refinement: string; isState: boolean; + stateSet: string | null; // the name of the state's set, when it is not a generated one file: string; } diff --git a/client/src/webview/script.spec.ts b/client/src/webview/script.spec.ts index 270f4c32..f12dc800 100644 --- a/client/src/webview/script.spec.ts +++ b/client/src/webview/script.spec.ts @@ -30,6 +30,7 @@ function diagnostic(file: string, title: string, category: 'error' | 'warning' = function context(file = currentFile): LJContext { const variable: LJVariable = { name: 'count', + displayName: 'count', internalName: 'count_1', type: 'int', refinement: 'count > 0', diff --git a/client/src/webview/views/context/context.spec.ts b/client/src/webview/views/context/context.spec.ts index 8fe71245..adb357dc 100644 --- a/client/src/webview/views/context/context.spec.ts +++ b/client/src/webview/views/context/context.spec.ts @@ -5,10 +5,10 @@ import { renderContextView } from './context'; const currentFile = 'file:///workspace/Current.java'; const sectionState = { aliases: true, ghosts: true, vars: true }; -function ghost(name: string, file = currentFile, isState = false): LJGhost { +function ghost(name: string, file = currentFile, stateSet: string | null = null): LJGhost { return { - name, qualifiedName: `Example.${name}`, returnType: isState ? 'boolean' : 'int', - parameterTypes: ['Example'], refinement: '', isState, file, + name, qualifiedName: `Example.${name}`, returnType: stateSet ? 'boolean' : 'int', + parameterTypes: ['Example'], refinement: '', isState: stateSet !== null, stateSet, file, }; } @@ -29,9 +29,9 @@ describe('context view', () => { it('renders aliases, current-file ghosts and states, and variables', () => { document.body.innerHTML = renderContextView(context({ aliases: [{ name: 'Positive', parameters: ['x'], types: ['int'], predicate: 'x > 0' }], - ghosts: [ghost('size'), ghost('open', currentFile, true), ghost('other', 'file:///workspace/Other.java')], + ghosts: [ghost('size'), ghost('open', currentFile, 'phase'), ghost('other', 'file:///workspace/Other.java')], allVars: [{ - name: 'count', internalName: 'count#1', type: 'int', refinement: 'count > 0', + name: 'count', displayName: 'count@3', internalName: '#count_1', type: 'int', refinement: 'count@3 > 0', mainRefinement: 'count > 0', position: null, annotationPosition: null, }], }), currentFile, sectionState); @@ -42,9 +42,10 @@ describe('context view', () => { expect(document.querySelectorAll('#context-ghosts tr')).toHaveLength(2); expect(text('#context-ghosts tr:first-child td:first-child')).toBe('int size(Example)'); expect(text('#context-ghosts tr:first-child td:last-child')).toBe('ghost'); + expect(text('#context-ghosts tr:last-child td:first-child')).toBe('phase(Example) == open'); expect(text('#context-ghosts tr:last-child td:last-child')).toBe('state'); - expect(text('#context-vars tbody td:first-child')).toBe('count'); - expect(text('#context-vars tbody td:last-child')).toBe('count > 0'); + expect(text('#context-vars tbody td:first-child')).toBe('count@3'); + expect(text('#context-vars tbody td:last-child')).toBe('count@3 > 0'); expect(Array.from(document.querySelectorAll('.context-toggle-btn'), node => node.getAttribute('aria-expanded'))).toEqual(['true', 'true', 'true']); expect(document.querySelectorAll('.context-section-content.collapsed')).toHaveLength(0); }); diff --git a/client/src/webview/views/context/ghosts.ts b/client/src/webview/views/context/ghosts.ts index 6b758ac2..b92b8ee3 100644 --- a/client/src/webview/views/context/ghosts.ts +++ b/client/src/webview/views/context/ghosts.ts @@ -25,6 +25,9 @@ export function renderContextGhosts(ghosts: LJGhost[], isExpanded: boolean): str `; } +// a state of a named set is written as a value of its set, as error messages write it function renderGhost(ghost: LJGhost): string { - return `${ghost.returnType} ${ghost.name}(${ghost.parameterTypes.map(getSimpleName).join(', ')})`; + const parameters = ghost.parameterTypes.map(getSimpleName).join(', '); + if (ghost.stateSet) return `${ghost.stateSet}(${parameters}) == ${ghost.name}`; + return `${ghost.returnType} ${ghost.name}(${parameters})`; } diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index c7f66667..6941ca79 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -1,5 +1,5 @@ import type { LJDiagnostic, LJHint, SourcePosition } from "../../types/diagnostics"; -import { escapeHtml, getFileName, getSimpleName } from "../utils"; +import { escapeHtml, getFileName } from "../utils"; import { renderHighlightedExpression, renderHighlightedInlineExpression } from "../highlighting"; import { getDiagnosticRevealTarget, getDiagnosticRevealTargetKey } from "../diagnostic-reveal"; import { renderCodicon, renderCodiconButton } from "../icons"; @@ -98,7 +98,7 @@ export const renderLocation = (diagnostic: LJDiagnostic): string => { }; export function renderVariableHighlightButton(variable: LJVariable): string { - const displayName = getSimpleName(variable.name); + const displayName = variable.displayName; const position = variable.position; if (!position || !position.file) return `${displayName}`; return renderSourceHighlightButton( diff --git a/server/src/main/java/dtos/context/ContextDisplay.java b/server/src/main/java/dtos/context/ContextDisplay.java new file mode 100644 index 00000000..7c1daee0 --- /dev/null +++ b/server/src/main/java/dtos/context/ContextDisplay.java @@ -0,0 +1,137 @@ +package dtos.context; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Objects; +import java.util.Optional; +import java.util.Set; +import java.util.stream.Stream; + +import liquidjava.processor.context.ContextHistory; +import liquidjava.processor.context.GhostFunction; +import liquidjava.processor.context.GhostState; +import liquidjava.processor.context.RefinedVariable; +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.StateValues; +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.LiteralBoolean; +import liquidjava.rj_language.ast.Var; +import liquidjava.rj_language.ast.formatter.DisplayNames; +import liquidjava.rj_language.ast.formatter.ExpressionFormatter; +import liquidjava.utils.GeneratedNames; + +/** + * Shows the variables of a context as the verifier's error messages do: the states of a named set as values of the + * set, {@code display(host) == notDisplayable}, and variables written alike told apart by the line of their value, + * {@code host@23}. The values the verifier introduces are not variables of the program: one that stands for a single + * expression is replaced by it, and a fact about one that is not constrained at all is left out + */ +public final class ContextDisplay { + private final DisplayNames names; + private final List states; + private final List stateSets; + private final Map generatedValues; + private final Set unconstrained; + + private ContextDisplay(DisplayNames names, List states, Map generatedValues, + Set unconstrained) { + this.names = names; + this.states = states; + // the verifier also passes its other ghost functions, which the context history does not keep + this.stateSets = states.stream().map(GhostState::getParent).filter(Objects::nonNull).distinct().toList(); + this.generatedValues = generatedValues; + this.unconstrained = unconstrained; + } + + public static ContextDisplay of(ContextHistory history) { + List variables = Stream.concat(history.getLocalVars().stream(), + history.getGlobalVars().stream()).toList(); + // the variables of the context first, then the others its refinements mention + List shown = new ArrayList<>(); + List others = new ArrayList<>(); + Map> generatedFacts = new HashMap<>(); + for (RefinedVariable variable : variables) { + Expression refinement = variable.getRefinement().getExpression(); + refinement.getVariableNames(others); + if (!GeneratedNames.isGenerated(variable.getName())) + shown.add(variable.getName()); + else { + others.add(variable.getName()); + generatedFacts.computeIfAbsent(variable.getName(), name -> new ArrayList<>()).add(refinement); + } + } + Map values = new HashMap<>(); + Set unconstrained = new HashSet<>(); + generatedFacts.forEach((name, facts) -> { + if (facts.stream().allMatch(Expression::isBooleanTrue)) + unconstrained.add(name); + else + valueOf(name, facts).ifPresent(value -> values.put(name, value)); + }); + return new ContextDisplay(DisplayNames.of(shown, others, history::lineOf), new ArrayList<>(history.getGhosts()), + values, unconstrained); + } + + public String name(String variable) { + return names.get(variable); + } + + public String format(Predicate refinement) { + Expression expression = withoutUnconstrained(inlineGenerated(refinement.getExpression())); + return ExpressionFormatter.format(StateValues.toSetForm(expression, states, stateSets), names); + } + + /** The expression a generated value stands for, when every fact about it is {@code name == expression} */ + private static Optional valueOf(String name, List facts) { + Set values = new HashSet<>(); + for (Expression fact : facts) { + Optional value = equatedTo(name, fact); + if (value.isEmpty()) + return Optional.empty(); + values.add(value.get()); + } + return values.size() == 1 ? values.stream().findFirst() : Optional.empty(); + } + + private static Optional equatedTo(String name, Expression fact) { + if (!(fact instanceof BinaryExpression equality && equality.getOperator().equals("=="))) + return Optional.empty(); + Var variable = new Var(name); + Expression other = variable.equals(equality.getFirstOperand()) ? equality.getSecondOperand() + : variable.equals(equality.getSecondOperand()) ? equality.getFirstOperand() : null; + return other == null || mentions(other, name) ? Optional.empty() : Optional.of(other); + } + + // a value can stand for an expression over other generated values, so it is replaced until none is left + private Expression inlineGenerated(Expression expression) { + for (int i = 0; i <= generatedValues.size(); i++) { + Optional generated = variablesOf(expression).stream().filter(generatedValues::containsKey) + .findFirst(); + if (generated.isEmpty()) + break; + expression = expression.substitute(new Var(generated.get()), generatedValues.get(generated.get())); + } + return expression; + } + + private Expression withoutUnconstrained(Expression expression) { + return expression.getConjuncts().stream() + .filter(conjunct -> variablesOf(conjunct).stream().noneMatch(unconstrained::contains)) + .reduce((left, right) -> new BinaryExpression(left, "&&", right)) + .orElse(new LiteralBoolean(true)); + } + + private static boolean mentions(Expression expression, String name) { + return variablesOf(expression).contains(name); + } + + private static List variablesOf(Expression expression) { + List variables = new ArrayList<>(); + expression.getVariableNames(variables); + return variables; + } +} diff --git a/server/src/main/java/dtos/context/GhostDTO.java b/server/src/main/java/dtos/context/GhostDTO.java index 825d796c..c3676ac8 100644 --- a/server/src/main/java/dtos/context/GhostDTO.java +++ b/server/src/main/java/dtos/context/GhostDTO.java @@ -1,10 +1,11 @@ package dtos.context; import java.util.List; -import java.util.regex.Pattern; import java.util.stream.Collectors; +import liquidjava.processor.context.GhostFunction; import liquidjava.processor.context.GhostState; +import liquidjava.utils.constants.Formats; /** * DTO for serializing GhostState instances to JSON. @@ -16,21 +17,22 @@ public record GhostDTO( List parameterTypes, String refinement, boolean isState, + String stateSet, String file ) { - private static final Pattern STATE_REFINEMENT_PATTERN = Pattern.compile("^state\\d+\\(_\\) == \\d+$"); - public static GhostDTO from(GhostState ghostState) { - String refinement = ghostState.getRefinement() != null ? ghostState.getRefinement().toString() : null; - boolean isState = refinement != null && STATE_REFINEMENT_PATTERN.matcher(refinement).matches(); + GhostFunction set = ghostState.getParent(); + // a state of a set with a generated name, such as state1, is written as the state alone + boolean isNamedSet = set != null && !set.getName().matches(Formats.STATE_SET_NAMES); return new GhostDTO( ghostState.getName(), ghostState.getQualifiedName(), ContextHistoryDTO.stringifyType(ghostState.getReturnType()), ghostState.getParametersTypes().stream().map(ContextHistoryDTO::stringifyType).collect(Collectors.toList()), - refinement, - isState, + ghostState.getRefinement() != null ? ghostState.getRefinement().toString() : null, + set != null, + isNamedSet ? set.getName() : null, ghostState.getFile() ); } diff --git a/server/src/main/java/dtos/context/VariableDTO.java b/server/src/main/java/dtos/context/VariableDTO.java index f643266a..63818791 100644 --- a/server/src/main/java/dtos/context/VariableDTO.java +++ b/server/src/main/java/dtos/context/VariableDTO.java @@ -1,8 +1,12 @@ package dtos.context; +import java.util.function.Function; +import java.util.function.UnaryOperator; + import dtos.diagnostics.SourcePositionDTO; import liquidjava.processor.context.PlacementInCode; import liquidjava.processor.context.RefinedVariable; +import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.formatter.ExpressionFormatter; import liquidjava.rj_language.ast.formatter.VariableFormatter; @@ -11,6 +15,7 @@ */ public record VariableDTO( String name, + String displayName, String internalName, String type, String refinement, @@ -18,14 +23,27 @@ public record VariableDTO( SourcePositionDTO position, SourcePositionDTO annotationPosition ) { + /** A variable on its own, such as a method parameter */ public static VariableDTO from(RefinedVariable refinedVariable) { + return from(refinedVariable, VariableFormatter::format, ExpressionFormatter::format); + } + + /** A variable of a context, shown as the context shows it */ + public static VariableDTO from(RefinedVariable refinedVariable, ContextDisplay display) { + return from(refinedVariable, display::name, display::format); + } + + private static VariableDTO from(RefinedVariable refinedVariable, UnaryOperator displayName, + Function format) { PlacementInCode placement = refinedVariable.getPlacementInCode(); if (placement == null) return null; return new VariableDTO( VariableFormatter.format(refinedVariable.getName()), + displayName.apply(refinedVariable.getName()), refinedVariable.getName(), ContextHistoryDTO.stringifyType(refinedVariable.getType()), - ExpressionFormatter.format(refinedVariable.getRefinement()), + format.apply(refinedVariable.getRefinement()), + // the annotation as it is written in code, for hovers and completions ExpressionFormatter.format(refinedVariable.getMainRefinement()), SourcePositionDTO.from(placement.getPosition()), SourcePositionDTO.from(placement.getAnnotationPosition()) diff --git a/server/src/main/java/utils/ContextHistoryConverter.java b/server/src/main/java/utils/ContextHistoryConverter.java index aab0e1b2..1685aba5 100644 --- a/server/src/main/java/utils/ContextHistoryConverter.java +++ b/server/src/main/java/utils/ContextHistoryConverter.java @@ -1,5 +1,6 @@ package utils; +import java.util.Comparator; import java.util.HashMap; import java.util.List; import java.util.Map; @@ -7,34 +8,70 @@ import java.util.stream.Collectors; import dtos.context.AliasDTO; +import dtos.context.ContextDisplay; import dtos.context.ContextHistoryDTO; import dtos.context.MethodDTO; import dtos.context.GhostDTO; import dtos.context.VariableDTO; import dtos.diagnostics.SourcePositionDTO; import liquidjava.processor.context.ContextHistory; +import liquidjava.processor.context.GhostFunction; +import liquidjava.processor.context.GhostState; +import liquidjava.processor.context.RefinedVariable; +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.LiteralInt; +import liquidjava.utils.GeneratedNames; /** * Utility class for converting LiquidJava context objects to DTOs. */ public class ContextHistoryConverter { + // the ghosts first, then the states of each set together, in the order they are declared + private static final Comparator GHOST_ORDER = Comparator + .comparing(ContextHistoryConverter::setOf) + .thenComparingInt(ContextHistoryConverter::stateIndex) + .thenComparing(GhostState::getName); + /** * Converts a ContextHistory to its DTO type. * @param contextHistory the context history to convert * @return the corresponding DTO */ public static ContextHistoryDTO convertToDTO(ContextHistory contextHistory) { + ContextDisplay display = ContextDisplay.of(contextHistory); return new ContextHistoryDTO( - contextHistory.getLocalVars().stream().map(VariableDTO::from).filter(v -> v != null).collect(Collectors.toList()), - contextHistory.getGlobalVars().stream().map(VariableDTO::from).filter(v -> v != null).collect(Collectors.toList()), - contextHistory.getGhosts().stream().map(GhostDTO::from).collect(Collectors.toList()), + convertVariables(contextHistory.getLocalVars(), display), + convertVariables(contextHistory.getGlobalVars(), display), + contextHistory.getGhosts().stream().sorted(GHOST_ORDER).map(GhostDTO::from).collect(Collectors.toList()), contextHistory.getAliases().stream().map(AliasDTO::from).collect(Collectors.toList()), contextHistory.getMethods().stream().map(MethodDTO::from).filter(f -> f != null).collect(Collectors.toList()), parseFileScopes(contextHistory.getFileScopes()) ); } + private static String setOf(GhostState ghost) { + GhostFunction set = ghost.getParent(); + return set == null ? "" : set.getPrefix() + "." + set.getName(); + } + + // a state of a set is refined as set(_) == index + private static int stateIndex(GhostState ghost) { + Expression refinement = ghost.getRefinement() == null ? null : ghost.getRefinement().getExpression(); + return refinement instanceof BinaryExpression b && b.getSecondOperand() instanceof LiteralInt index + ? index.getValue() : -1; + } + + // the values the verifier introduces are not variables of the program + private static List convertVariables(Set variables, ContextDisplay display) { + return variables.stream() + .filter(v -> !GeneratedNames.isGenerated(v.getName())) + .map(v -> VariableDTO.from(v, display)) + .filter(v -> v != null) + .collect(Collectors.toList()); + } + private static Map> parseFileScopes(Map> fileScopes) { return fileScopes.entrySet().stream().collect(Collectors.toMap( Map.Entry::getKey, diff --git a/server/src/test/java/utils/ContextHistoryConverterTest.java b/server/src/test/java/utils/ContextHistoryConverterTest.java index 64851421..b44d55b1 100644 --- a/server/src/test/java/utils/ContextHistoryConverterTest.java +++ b/server/src/test/java/utils/ContextHistoryConverterTest.java @@ -2,23 +2,41 @@ import static org.junit.jupiter.api.Assertions.*; +import java.nio.file.Path; import java.util.List; +import java.util.Map; import java.util.Set; +import java.util.stream.Collectors; import org.junit.jupiter.api.AfterEach; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; import dtos.context.ContextHistoryDTO; +import dtos.context.GhostDTO; +import dtos.context.VariableDTO; import dtos.diagnostics.SourcePositionDTO; +import liquidjava.api.CommandLineLauncher; import liquidjava.processor.context.ContextHistory; import liquidjava.processor.context.Variable; import liquidjava.rj_language.Predicate; import spoon.Launcher; class ContextHistoryConverterTest { + private static final Path DOOR = Path.of("src", "test", "resources", "context").toAbsolutePath(); private final ContextHistory history = ContextHistory.getInstance(); + private ContextHistoryDTO verify(Path path) { + boolean lspMode = CommandLineLauncher.cmdArgs.lspMode; + CommandLineLauncher.cmdArgs.lspMode = true; // the verifier only keeps its context history in the IDE + try { + CommandLineLauncher.launch(path.toString()); + } finally { + CommandLineLauncher.cmdArgs.lspMode = lspMode; + } + return ContextHistoryConverter.convertToDTO(history); + } + @BeforeEach @AfterEach void clearHistory() { @@ -57,4 +75,23 @@ void omitsVariablesWithoutCodePlacement() { assertTrue(dto.localVars().isEmpty()); assertTrue(dto.globalVars().isEmpty()); } + + @Test + void showsVariablesAsErrorMessagesDo() { + List variables = verify(DOOR).localVars(); + Map refinements = variables.stream() + .collect(Collectors.toMap(VariableDTO::displayName, VariableDTO::refinement, (left, right) -> left)); + assertEquals("phase(door@13) == open", refinements.get("door@13")); + assertEquals("door == door@13", refinements.get("door")); + // the array length the verifier introduces is replaced by its value + assertEquals("length(keys@14) == 2", refinements.get("keys@14")); + assertTrue(variables.stream().noneMatch(v -> v.displayName().startsWith("#")), refinements.toString()); + } + + @Test + void showsTheStatesOfANamedSetAsValuesOfTheSet() { + List ghosts = verify(DOOR).ghosts(); + assertEquals(List.of("open", "closed"), ghosts.stream().map(GhostDTO::name).toList()); + assertTrue(ghosts.stream().allMatch(g -> g.isState() && "phase".equals(g.stateSet()))); + } } diff --git a/server/src/test/resources/context/Door.java b/server/src/test/resources/context/Door.java new file mode 100644 index 00000000..6d1869f6 --- /dev/null +++ b/server/src/test/resources/context/Door.java @@ -0,0 +1,16 @@ +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet(name = "phase", value = {"open", "closed"}) +class Door { + @StateRefinement(to = "phase(this) == open") + Door() {} + + @StateRefinement(from = "phase(this) == open", to = "phase(this) == closed") + void close() {} + + static void use() { + Door door = new Door(); + int[] keys = new int[2]; + } +}