Only run QuickCheck on subset of POs that are visible when filtering

CHANGELOG.md

@@ -1,5 +1,9 @@
+### 1.4.0-beta.3
+- QuickCheck now only runs on the visible subset of proof obligations.
+- Fixed bug where QuickCheck info would become stale when changing settings and subsequently running QuickCheck. 
+
 ### 1.4.0-beta.2
-- Fix char literals syntax highligting (issue #190)
+- Fix char literals syntax highlighting (issue #190)
 - Fix name of generated debug configuration (issue #214)
 - Fix code lenses on polymorphic functions (issue #188)
 - Add the ability to configure QuickCheck using JSON

package.json

@@ -1,6 +1,6 @@
 {
     "name": "vdm-vscode",
-    "version": "1.4.0-beta.2",
+    "version": "1.4.0-beta.3",
     "publisher": "overturetool",
     "engines": {
         "vscode": "^1.64.0",

src/slsp/features/ProofObligationGenerationFeature.ts

@@ -13,10 +13,11 @@ import {
     ProofObligationGenerationServerCapabilities,
     QuickCheckInfo,
     RunQuickCheckRequest,
+    RunQuickCheckRequestParams,
 } from "../protocol/ProofObligationGeneration";
 import { SpecificationLanguageClient } from "../SpecificationLanguageClient";
 import { ProofObligation as CodeProofObligation } from "../views/ProofObligationPanel";
-import { readOptionalConfiguration } from "../../util/PluginConfigurationUtil";
+import { mergeDeep, readOptionalConfiguration } from "../../util/PluginConfigurationUtil";
 
 export default class ProofObligationGenerationFeature implements StaticFeature {
     private _onDidChangeProofObligations: EventEmitter<boolean>;
@@ -46,7 +47,7 @@ export default class ProofObligationGenerationFeature implements StaticFeature {
             provideProofObligations: (uri: Uri) => this.requestPOG(uri),
             onDidChangeProofObligations: this._onDidChangeProofObligations.event,
             quickCheckProvider: quickCheckEnabled,
-            runQuickCheck: (wsFolder: Uri) => this.runQuickCheck(wsFolder),
+            runQuickCheck: (wsFolder: Uri, poIds: number[]) => this.runQuickCheck(wsFolder, poIds),
         };
         this._disposables.push(ProofObligationPanel.registerProofObligationProvider(this._selector, provider));
     }
@@ -81,11 +82,17 @@ export default class ProofObligationGenerationFeature implements StaticFeature {
         });
     }
 
-    private runQuickCheck(wsFolder: Uri): Thenable<QuickCheckInfo[]> {
+    private runQuickCheck(wsFolder: Uri, poIds: number[]): Thenable<QuickCheckInfo[]> {
         return new Promise((resolve, reject) => {
-            readOptionalConfiguration(wsFolder, "quickcheck.json", (config) => {
+            readOptionalConfiguration(wsFolder, "quickcheck.json", (config: RunQuickCheckRequestParams) => {
+                const configWithObligations = mergeDeep(config ?? {}, {
+                    config: {
+                        obligations: poIds,
+                    },
+                });
+
                 this._client
-                    .sendRequest(RunQuickCheckRequest.type, config ?? {})
+                    .sendRequest(RunQuickCheckRequest.type, configWithObligations)
                     .then((qcInfos) => resolve(qcInfos))
                     .catch((e) => reject(`QuickCheck failed. ${e}`));
             });

src/slsp/protocol/ProofObligationGeneration.ts

@@ -186,5 +186,8 @@ export namespace RunQuickCheckRequest {
 export interface RunQuickCheckRequestParams {
     strategies: Array<unknown>;
     timeout: number;
-    pattern: string;
+    config: {
+        timeout: number;
+        obligations: Array<number>;
+    };
 }

src/slsp/views/ProofObligationPanel.ts

@@ -39,7 +39,7 @@ export interface ProofObligationProvider {
     onDidChangeProofObligations: Event<boolean>;
     provideProofObligations(uri: Uri): Thenable<ProofObligation[]>;
     quickCheckProvider: boolean;
-    runQuickCheck(wsFolder: Uri): Thenable<QuickCheckInfo[]>;
+    runQuickCheck(wsFolder: Uri, poIds: number[]): Thenable<QuickCheckInfo[]>;
 }
 
 interface Message {
@@ -168,11 +168,11 @@ export class ProofObligationPanel implements Disposable {
         this._lastWsFolder = wsFolder;
     }
 
-    protected async onRunQuickCheck(uri: Uri) {
+    protected async onRunQuickCheck(uri: Uri, poIds: number[]) {
         const poProvider = this.getPOProvider(uri);
 
         try {
-            return await poProvider.provider.runQuickCheck(this._lastWsFolder.uri);
+            return await poProvider.provider.runQuickCheck(this._lastWsFolder.uri, poIds);
         } catch (e) {
             window.showErrorMessage(e);
             console.warn(`[Proof Obligation View] QuickCheck provider failed.`);
@@ -204,17 +204,29 @@ export class ProofObligationPanel implements Disposable {
         }
     }
 
+    private deleteQcInfo(po: ProofObligation): ProofObligation {
+        delete po["provedBy"];
+        delete po["message"];
+        delete po["counterexample"];
+        delete po["witness"];
+
+        return po;
+    }
+
     private addQuickCheckInfoToPos(pos: Array<ProofObligation>, qcInfos: Array<QuickCheckInfo>): Array<ProofObligation> {
-        const poMap: Record<number, ProofObligation> = pos.reduce((_poMap, _po) => {
-            _poMap[_po.id] = _po;
-            return _poMap;
+        const qcInfoMap: Record<number, QuickCheckInfo> = qcInfos.reduce((_qcInfoMap, _qcInfo) => {
+            _qcInfoMap[_qcInfo.id] = _qcInfo;
+            return _qcInfoMap;
         }, {});
 
-        return qcInfos.reduce((newPos, qcInfo) => {
-            const matchingPo = poMap[qcInfo.id];
+        return pos.reduce((newPos, po) => {
+            const matchingInfo = qcInfoMap[po.id];
 
-            if (matchingPo) {
-                newPos.push(Object.assign(matchingPo, qcInfo));
+            if (matchingInfo) {
+                this.deleteQcInfo(po);
+                newPos.push(Object.assign(po, matchingInfo));
+            } else {
+                newPos.push(po);
             }
 
             return newPos;
@@ -291,11 +303,10 @@ export class ProofObligationPanel implements Disposable {
                             });
                             break;
                         case "runQC":
-                            const qcInfos = await this.onRunQuickCheck(wsFolder.uri);
+                            const qcInfos = await this.onRunQuickCheck(wsFolder.uri, message.data.poIds ?? []);
                             const posWithQc = this.addQuickCheckInfoToPos(this._pos, qcInfos);
 
                             this._panel.webview.postMessage({ command: "newPOs", pos: posWithQc });
-
                             break;
                     }
                 },

src/util/PluginConfigurationUtil.ts

@@ -11,3 +11,28 @@ export async function readOptionalConfiguration(wsFolder: Uri, filename: string,
 
     callback(callbackValue);
 }
+
+function isObject(value: unknown): value is Object {
+    return value !== null && typeof value === "object" && !Array.isArray(value);
+}
+
+export function mergeDeep(target: Object, ...sources: Object[]): Object {
+    if (!sources.length) {
+        return target;
+    }
+    const source = sources.shift();
+
+    for (const key in source) {
+        if (isObject(source[key])) {
+            if (!target[key]) {
+                Object.assign(target, { [key]: {} });
+            }
+
+            mergeDeep(target[key], source[key]);
+        } else {
+            Object.assign(target, { [key]: source[key] });
+        }
+    }
+
+    return mergeDeep(target, ...sources);
+}

src/webviews/proof_obligations/ProofObligationsView.tsx

@@ -44,21 +44,19 @@ interface FilterState {
 interface ProofObligationsHeaderMenuProps {
     onFilterChanged: (newFilterText: string) => void;
     onExpandCollapse: () => void;
-    vscodeApi: VSCodeAPI;
     enableQuickCheck: boolean;
     openPos: Set<number>;
-    pos: Array<FormattedProofObligation>;
     filterState?: FilterState;
+    onClickQuickCheck?: () => void;
 }
 
 const ProofObligationsHeaderMenu = ({
     onFilterChanged,
     onExpandCollapse,
-    vscodeApi,
     enableQuickCheck,
     openPos,
-    pos,
-    filterState
+    filterState,
+    onClickQuickCheck,
 }: ProofObligationsHeaderMenuProps) => {
     return (
         <div
@@ -70,26 +68,20 @@ const ProofObligationsHeaderMenu = ({
                 alignItems: "center",
             }}
         >
-            <VSCodeTextField css={{flexShrink: 1}} onInput={(e) => {
-                onFilterChanged((e.target as HTMLInputElement).value)
-            }} type="text">
+            <VSCodeTextField
+                css={{ flexShrink: 1 }}
+                onInput={(e) => {
+                    onFilterChanged((e.target as HTMLInputElement).value);
+                }}
+                type="text"
+            >
                 Filter {filterState ? `(Showing ${filterState.matchingRows} of ${filterState.totalRows} rows.)` : null}
             </VSCodeTextField>
-            <div css={{flexShrink: 0}}>
+            <div css={{ flexShrink: 0 }}>
                 <VSCodeButton css={{ margin: "0 1em" }} appearance="secondary" onClick={onExpandCollapse}>
-                    {openPos.size === pos.length ? "Collapse all proof obligations" : "Expand all proof obligations"}
+                    {openPos.size === filterState?.totalRows ? "Collapse all proof obligations" : "Expand all proof obligations"}
                 </VSCodeButton>
-                {enableQuickCheck ? (
-                    <VSCodeButton
-                        onClick={() =>
-                            vscodeApi.postMessage({
-                                command: "runQC"
-                            })
-                        }
-                    >
-                        Run QuickCheck
-                    </VSCodeButton>
-                ) : null}
+                {enableQuickCheck ? <VSCodeButton onClick={onClickQuickCheck}>Run QuickCheck</VSCodeButton> : null}
             </div>
         </div>
     );
@@ -102,9 +94,11 @@ const filterPOs = (proofObligations: Array<FormattedProofObligation>, filterText
     const filterableHeaders: Array<keyof FormattedProofObligation> = ["id", "kind", "name", "status"];
 
     // Check if any one term is found in the proof obligation
-    const disjunctMatch = (po: FormattedProofObligation, orTerms: Array<string>) => filterableHeaders.some((id) => orTerms.some((term) => (po[id] ?? "").toString().toLowerCase().includes(term.toLowerCase())))
+    const disjunctMatch = (po: FormattedProofObligation, orTerms: Array<string>) =>
+        filterableHeaders.some((id) => orTerms.some((term) => (po[id] ?? "").toString().toLowerCase().includes(term.toLowerCase())));
     // Check if all terms are found in the proof obligation
-    const conjunctMatch = (po: FormattedProofObligation, andTerms: Array<Array<string>>) => andTerms.every((orTerms) => disjunctMatch(po, orTerms));
+    const conjunctMatch = (po: FormattedProofObligation, andTerms: Array<Array<string>>) =>
+        andTerms.every((orTerms) => disjunctMatch(po, orTerms));
 
     return proofObligations.filter((po) => conjunctMatch(po, conjunctionTerms));
 };
@@ -121,23 +115,34 @@ export const ProofObligationsView = ({ vscodeApi, enableQuickCheck = false }: Pr
     const [openPos, setOpenPos] = useState<Set<number>>(new Set<number>());
     const [filterText, setFilterText] = useState<string>("");
 
+    const filteredPos = useMemo(() => filterPOs(pos, filterText), [filterText, pos]);
+    const currentFilterState: FilterState | undefined =
+        filterText === ""
+            ? undefined
+            : {
+                  matchingRows: filteredPos.length,
+                  totalRows: pos.length,
+              };
 
-    const filteredPos = useMemo(() => filterPOs(pos, filterText), [filterText, pos]); 
-    const currentFilterState: FilterState | undefined = filterText === "" ? undefined : {
-        matchingRows: filteredPos.length,
-        totalRows: pos.length
-    }
+    const handleQuickCheck = () => {
+        vscodeApi.postMessage({
+            command: "runQC",
+            data: {
+                poIds: filteredPos.map((po) => po.id),
+            },
+        });
+    };
 
     const handleJumpToSource = (po: FormattedProofObligation) => {
         vscodeApi.postMessage({
             command: "goToSymbol",
-            data: po.id
+            data: po.id,
         });
     };
 
     const handleOpenQuickCheck = (po: FormattedProofObligation) => {
         setProofObligation(po);
-    }
+    };
 
     const handleRowClick = (row: FormattedProofObligation) => {
         const id = row.id;
@@ -198,13 +203,12 @@ export const ProofObligationsView = ({ vscodeApi, enableQuickCheck = false }: Pr
     return (
         <ProofObligationContainer>
             <ProofObligationsHeaderMenu
-                vscodeApi={vscodeApi}
                 onFilterChanged={setFilterText}
                 onExpandCollapse={handleExpandCollapseClick}
                 enableQuickCheck={enableQuickCheck}
                 openPos={openPos}
-                pos={pos}
                 filterState={currentFilterState}
+                onClickQuickCheck={handleQuickCheck}
             />
 
             <div