Chore: Fix small UI bugs; Add audit.md and update README

README.md

@@ -12,11 +12,9 @@ exogenous functions.
 For endogenous soundness, safety tags should be correctly discharged at the call site,
 delegated upward, or transformed into new tags associated with the caller.
 
-While tag checking and enforcement are managed by the [safety-tool] linter, the UI
+While tag checking and enforcement are executed by the `safety-tool` linter, the UI
 simply attaches tags as child nodes to the function-level nodes.
 
-[safety-tool]: https://github.com/Artisan-Lab/tag-std/tree/main/safety-tool
-
 ![](https://github.com/user-attachments/assets/e8e41752-e147-4bd0-8de9-f3bceb5c4e19)
 
 The side panels juxtapose tag-derived safety documentation with the original safety
@@ -77,6 +75,31 @@ docstrings.
 
 ![](https://github.com/user-attachments/assets/bc038c70-f1a6-4e1d-b8aa-d8ae158380b5)
 
+## Explanations
+
+### Start an unsafe function
+
+The interface offers multiple ways to locate or navigate to specific functions:
+* Global Search: Click the search icon in the top bar to access a complete list of
+functions. You can refine the results by filtering for function names or specific tags.
+* Module Navigation: Click the navigation icon to toggle the left sidebar. This displays a
+module-based tree view, where you can browse and select functions within expanded modules.
+* Safety Tag Association: Click the tag icon to view the tag specifications and choose a 
+function the interested tag is annotated on.
+* Quick Start: The tool automatically displays a default unsafe function when you switch
+between crates. Current supported crates are core, alloc, std, and ostd (AsterinasOS).
+
+### Tag-derived documentation
+
+To ensure reusability, tags are designed as templates for backfilling specific variables.
+However, our present annotations in the standard library consists only of tag names
+without arguments, resulting in generic and incomplete documentation. You'll find more
+readable tag-derived output in the ostd crate, as it utilizes full arguments.
+
+This difference stems from the standard library's audit predating the creation of
+safety-tool, leading to its reliance on JSON manipulation, while AsterinasOS was audited
+using attribute syntax and the linter.
+
 ## Build the project
 
 Commands to build the UI project:
@@ -89,7 +112,10 @@ npm install
 npm run generate
 # Start the development server on `http://localhost:3000`:
 npm run dev
-# Locally preview production build:
-npm run preview
 ```
 
+To collect the data, we implemented a custom rustc driver and a cargo wrapper that extract
+API information, such as call graphs and ADT-related functions, into JSON format. The
+safety tags are sourced from the `tag-std` project.
+
+The application is a fully static webpage that fetches data hosted in a GitHub repository.

audit.md

@@ -0,0 +1,42 @@
+
+# Auditing Code with the UI Tool
+
+We've built a visualization tool for safety tag analysis, deployed as a fully static
+webpage at <https://unsafety-propagation-graph.vercel.app>.
+
+The tool aids human review of safety tags and unsafe code through visualization, by
+orchestrating necessary audit information.
+
+Tag checking and enforcement are implemented by the `#[safety::<predicate>(...)]`
+attributes and `safety-tool` linter, so they fall outside the current UI's purview.
+
+We use the unsafe `Vec::set_len` function from the `alloc` crate as the default example.
+In this view, `InBound` and `ValidNum` tags are displayed within the caller function node,
+while their definitions are rendered in the Safety Property panel.
+
+The graph interface streamlines the representation of UPG edges, presenting only two
+categories:
+* Caller-to-callee edges: Callee nodes are situated to the right of the caller nodes, and
+unsafe functions are marked with a red background.
+* Caller-to-field edges: Each is labeled to specify the access type as either read or
+write.
+
+The call graph features the following node interactions:
+* A click on a function node updates the side panels to show its tag-derived
+documentation, original documentation, source code, and MIR.
+  * When a function node is selcted, the name will be rendered as a hyperlink in the
+  documentation panel, allowing you to drill down and audit that specific unit in greater
+  detail.
+* A click on an ADT or field node opens a window for navigating between functions
+identified as compromising exogenous soundness in our paper.
+  * Our analysis focuses on functions associated with ADTs, specifically those where the
+  ADT serves as the receiver type of the current method (the caller). This scope
+  encompasses not only constructors but also functions that manipulate the ADT’s state
+  through direct field access, arguments, or local variables.
+
+![](https://github.com/user-attachments/assets/d14ba2cd-fec0-4663-8c3c-0ae10992c1c3)
+
+![](https://github.com/user-attachments/assets/b7253f2a-7fd3-43bf-96d3-0900d3c7283c)
+
+The top bar includes a help button that displays the README content and offers a feature
+overview.

ui/app/assets/css/main.css

@@ -7,6 +7,13 @@
 /* this contains the default theme, these are optional styles */
 @import '@vue-flow/core/dist/theme-default.css';
 
+@theme {
+  /* unsafe text (bg) */
+  --color-unsafe: oklch(0.69 0.25 12.26);
+  /* unsafe node (bg) */
+  --color-unsafe-node: oklch(0.28 0.11 14.75);
+}
+
 /* General codeblock styles. */
 .shiki, .shiki span {
   @apply !leading-tight !text-base;
@@ -128,7 +135,7 @@ html, body {
   };
 }
 .upg-node-unsafe-fn {
-  @apply bg-red-100 dark:bg-red-900/30;
+  @apply bg-red-100 dark:bg-unsafe-node;
 }
 
 .upg-node-tag {
@@ -216,5 +223,5 @@ html, body {
 
 .unsafeFnLink {
   @apply text-rose-700 hover:text-rose-500 font-bold transition-colors
-    dark:hover:text-rose-400 dark:hover:text-rose-300;
+    dark:text-unsafe dark:hover:text-rose-300;
 }

ui/app/components/UPG.vue

@@ -106,7 +106,7 @@ watch(share, val => {
   router.push({
     query: {
       item: nodeItem.value,
-      view: flowOpts.value.view.join(","),
+      // view: flowOpts.value.view.join(","),
       up: toPanelStr(upPanel.value),
       down: toPanelStr(downPanel.value),
     }

ui/app/components/code/AdtPopup.vue

@@ -143,6 +143,7 @@ const initAdtItem = () => {
 }
 
 const search = ref<Search>({ withTags: false, unsafeOnly: false, text: "", page: 1, itemsPerPage: 20 })
+watch(active, () => search.value.page = 1)
 
 const items = computed<TreeItem[]>(() => {
   const tree: TreeItem[] = []

ui/app/components/code/Help.vue

@@ -7,7 +7,7 @@
 <script setup lang="ts">
 
 const help = `
-  This is a visual tool for safety tag analysis.
+This is a visual tool for safety tag analysis.
 
 ## Features
 
@@ -19,7 +19,7 @@ exogenous functions.
 For endogenous soundness, safety tags should be correctly discharged at the call site,
 delegated upward, or transformed into new tags associated with the caller.
 
-While tag checking and enforcement are managed by the \`safety-tool\` linter, the UI
+While tag checking and enforcement are executed by the \`safety-tool\` linter, the UI
 simply attaches tags as child nodes to the function-level nodes.
 
 ![](https://github.com/user-attachments/assets/e8e41752-e147-4bd0-8de9-f3bceb5c4e19)
@@ -76,5 +76,30 @@ docstrings.
 
 ![](https://github.com/user-attachments/assets/bc038c70-f1a6-4e1d-b8aa-d8ae158380b5)
 
+## Explanations
+
+### Start an unsafe function
+
+The interface offers multiple ways to locate or navigate to specific functions:
+* Global Search: Click the search icon in the top bar to access a complete list of
+functions. You can refine the results by filtering for function names or specific tags.
+* Module Navigation: Click the navigation icon to toggle the left sidebar. This displays a
+module-based tree view, where you can browse and select functions within expanded modules.
+* Safety Tag Association: Click the tag icon to view the tag specifications and choose a 
+function the interested tag is annotated on.
+* Quick Start: The tool automatically displays a default unsafe function when you switch
+between crates. Current supported crates are core, alloc, std, and ostd (AsterinasOS).
+
+### Tag-derived documentation
+
+To ensure reusability, tags are designed as templates for backfilling specific variables.
+However, our present annotations in the standard library consists only of tag names
+without arguments, resulting in generic and incomplete documentation. You'll find more
+readable tag-derived output in the ostd crate, as it utilizes full arguments.
+
+This difference stems from the standard library's audit predating the creation of
+safety-tool, leading to its reliance on JSON manipulation, while AsterinasOS was audited
+using attribute syntax and the linter.
+
 `
 </script>

ui/app/lib/output/adt.ts

@@ -37,7 +37,7 @@ export function adtDoc(adt: DataAdt) {
     const field_doc = field.doc ? `: ${field.doc}` : ""
     doc += `* \`${field.name}\`${field_doc}\n\n`
   }
-  doc += `### Adt Doc:\n\n${adt.doc_adt}`
+  doc += `### ADT Doc:\n\n${adt.doc_adt}`
   return doc
 }