Merge pull request #107 from os-checker/ui-time-column

UI: add column of execution time

Author: zjp-CN

ui/app/components/Kani.vue

@@ -41,8 +41,8 @@ type ModName = { name: string, n: number };
 const selectedMods = ref<string[]>([]);
 const mod_names = computed<ModName[]>(() => {
   return Object.entries(
-    raw.value.reduce((acc, { func }) => {
-      const prefix = func.split("::")[0] ?? func;
+    raw.value.reduce((acc, { harness }) => {
+      const prefix = harness.split("::")[0] ?? harness;
       acc[prefix] = (acc[prefix] || 0) + 1;
       return acc;
     }, {} as { [key: string]: number })
@@ -72,7 +72,7 @@ watch([selectedMods, selectedProofKind], ([mods, proofs]) => {
     // consider func mod
     push = empty_mod;
     for (const name of mods) {
-      if (val.func.startsWith(`${name}::`)) { push = true; break; }
+      if (val.harness.startsWith(`${name}::`)) { push = true; break; }
     }
     if (push) v.push(val);
   }

ui/app/shared/utils/kani.ts

@@ -1,15 +1,24 @@
 import type { DataTableSortMeta } from "primevue";
 import { FilterMatchMode } from '@primevue/core/api';
 
-export const URL_MERGE_DIFF = "https://raw.githubusercontent.com/os-checker/verify-rust-std_data/refs/heads/main/merge_diff-proofs-only.json";
+export const URL_MERGE_DIFF = "https://raw.githubusercontent.com/os-checker/verify-rust-std_data/refs/heads/main/merge_results-core.json";
 
 export type VecMergeHashKaniList = MergeHashKaniList[];
 
 export interface MergeHashKaniList {
-  file: string;
-  func: string;
-  hash?: string;
-  proof_kind?: ProofKind;
+  file: string,
+  harness: string,
+  proof_kind?: ProofKind,
+  hash?: string,
+  time?: number,
+  props: number,
+  func: {
+    name: string,
+    safe: string,
+    file: String,
+  },
+  ok?: boolean,
+  n_fialed_properties?: number,
 }
 
 export enum ProofKind {
@@ -35,15 +44,19 @@ export const center = {
   columnHeaderContent: { style: { "justify-content": "center" } },
   bodyCell: { style: { "text-align": "center" } }
 };
+export const right = {
+  columnHeaderContent: { style: { "justify-content": "flex-end" } },
+  bodyCell: { style: { "text-align": "right" } }
+};
 
 export const MergeKaniColumns: MergeKaniColumn[] = [
   {
     key: "file",
     col: { field: "file", header: "File Path", width: "15%", sortable: true },
   },
   {
-    key: "func",
-    col: { field: "func", header: "Function", width: "25%", sortable: true },
+    key: "harness",
+    col: { field: "harness", header: "Harness", width: "25%", sortable: true },
   },
   {
     key: "hash",
@@ -53,6 +66,10 @@ export const MergeKaniColumns: MergeKaniColumn[] = [
     key: "proof_kind",
     col: { field: "proof_kind", header: "Proof Kind", width: "12%", sortable: true, pt: center },
   },
+  {
+    key: "time",
+    col: { field: "time", header: "Time (ms)", width: "5%", sortable: true, pt: right },
+  },
 ];
 
 export const multiSort: DataTableSortMeta[] = [
@@ -64,7 +81,7 @@ export const FILTERS = {
   filters: {
     global: { value: null, matchMode: FilterMatchMode.CONTAINS },
   },
-  fields: ["file", "func"]
+  fields: ["file", "harness"]
 };
 
 export const optionsProofKind: string[] = [ProofKind.Standard, ProofKind.Contract];