From 661cfd6d1a00f60c7e660910d7b3f31643738a95 Mon Sep 17 00:00:00 2001
From: zjp <jiping_zhou@foxmail.com>
Date: Sat, 31 Jan 2026 14:14:22 +0000
Subject: [PATCH 1/5] feat(ui): add help button and render README

---
 ui/app/components/code/Help.vue     | 80 +++++++++++++++++++++++++++++
 ui/app/components/widget/TopBar.vue |  9 ++++
 ui/nuxt.config.ts                   |  1 +
 3 files changed, 90 insertions(+)
 create mode 100644 ui/app/components/code/Help.vue

diff --git a/ui/app/components/code/Help.vue b/ui/app/components/code/Help.vue
new file mode 100644
index 0000000..93d01b8
--- /dev/null
+++ b/ui/app/components/code/Help.vue
@@ -0,0 +1,80 @@
+<template>
+  <div class="overflow-y-auto p-10">
+    <CodeMarkdown :doc="help" :isWrapped="true" />
+  </div>
+</template>
+
+<script setup lang="ts">
+
+const help = `
+  This is a visual tool for safety tag analysis.
+
+## Features
+
+### Render safety tags in a direct call graph
+
+Achieving a complete soundness guarantee requires the analysis of both endogenous and
+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
+simply attaches tags as child nodes to the function-level nodes.
+
+![](https://github.com/user-attachments/assets/e8e41752-e147-4bd0-8de9-f3bceb5c4e19)
+
+The side panels juxtapose tag-derived safety documentation with the original safety
+section, allowing for easier reconciliation.
+
+### Explore tag specifications and usage frequencies
+
+A dedicated toolbar button opens a global registry of all tag specifications. Users can
+explore tag arguments, types, and their associated functions. The interface also includes
+a bar chart illustrating usage statistics for each tag.
+
+![](https://github.com/user-attachments/assets/6794a20f-e0a9-42b3-952e-4c29cf263470)
+
+The search interface renders tags as badges adjacent to the function name.
+
+![](https://github.com/user-attachments/assets/f247945f-0806-42dd-987a-6148f2412a27)
+
+### Inspect exogenous functions for ADTs in a popup view
+
+Exogenous functions are defined as functions that, while not directly invoked, may
+compromise the caller's invariants within the local or downstream crates upon composition.
+
+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)
+
+### Streamline auditing in side panels
+
+**Side panels** streamline the audit process by providing centralized access to critical
+analysis materials, allowing users to switch contexts effortlessly. The panel view
+consists of:
+*   **ADT Exogenous Functions**: Provides a condensed equivalent of the ADT popup's
+interface. Users can trigger specialized popups through the following buttons:
+    *   **Constructors**: Lists functions that return the ADT.
+    *   **Fields**: Displays functions that access ADT fields, categorized by
+    **read** and **write** operations.
+    *   **Arguments**: Identifies functions where the ADT is passed as an argument,
+    separating **read** and **write** access.
+    *   **Locals**: Shows functions where the ADT is used as a local variable, categorized
+    by **read/write** access.
+*   **Safety Properties**: Renders detailed safety documentation for tagged functions,
+derived from both tag usage and specifications.
+*   **Documentation**: Displays a richly rendered HTML view derived from Markdown
+docstrings.
+*   **Source Code**: Provides a full-view display of the function's source code.
+*   **MIR**: Displays the MIR for a function instance.
+
+![](https://github.com/user-attachments/assets/bc038c70-f1a6-4e1d-b8aa-d8ae158380b5)
+
+`
+</script>
diff --git a/ui/app/components/widget/TopBar.vue b/ui/app/components/widget/TopBar.vue
index ccbd91c..0f47e76 100644
--- a/ui/app/components/widget/TopBar.vue
+++ b/ui/app/components/widget/TopBar.vue
@@ -60,6 +60,15 @@
       <!--   <USelect v-model="flowOpts.view" multiple :items="VIEW_TYPES" class="w-50" icon="tabler:braces" /> -->
       <!-- </UTooltip> -->
 
+      <UModal :ui="{ content: 'w-[70vw] max-w-none' }">
+        <UTooltip text="Help">
+          <UButton icon="tabler:question-mark" color="neutral" variant="ghost" />
+        </UTooltip>
+        <template #content>
+          <CodeHelp />
+        </template>
+      </UModal>
+
       <UColorModeButton />
       <!-- <ULink to="https://artisan-lab.github.io/RAPx-Book/6.4-unsafe.html" :external="true" target="_blank">Help</ULink> -->
     </div>
diff --git a/ui/nuxt.config.ts b/ui/nuxt.config.ts
index 83627fa..dd423e9 100644
--- a/ui/nuxt.config.ts
+++ b/ui/nuxt.config.ts
@@ -35,6 +35,7 @@ export default defineNuxtConfig({
         'tabler:hexagon-letter-f-filled', // field
         'tabler:hexagon-letter-a-filled', // argument
         'tabler:hexagon-letter-l-filled', // locals
+        'tabler:question-mark', // help
       ],
     }
   },

From 4c8ffb9c9eb03252e2a2b2b8033dfdb38b3afa91 Mon Sep 17 00:00:00 2001
From: zjp <jiping_zhou@foxmail.com>
Date: Sat, 31 Jan 2026 14:18:25 +0000
Subject: [PATCH 2/5] data(adt): add body src if available

---
 data                |  2 +-
 src/output/utils.rs | 15 +++++++++++++--
 2 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/data b/data
index aafdd70..7d71849 160000
--- a/data
+++ b/data
@@ -1 +1 @@
-Subproject commit aafdd706df0de038b0bcf661962fb12e0013b5bf
+Subproject commit 7d718494630194493aa4e4cb12d04bd81ed117a9
diff --git a/src/output/utils.rs b/src/output/utils.rs
index 6f4d889..03897d5 100644
--- a/src/output/utils.rs
+++ b/src/output/utils.rs
@@ -43,12 +43,23 @@ pub fn span<T: CrateDef>(item: T, tcx: TyCtxt) -> String {
     src_map.span_to_string(span, rustc_span::FileNameDisplayPreference::Remapped)
 }
 
-pub fn src<T: CrateDef>(item: T, tcx: TyCtxt) -> String {
-    src_from_span(item.span(), tcx)
+pub fn src<T: CrateDef + Copy>(item: T, tcx: TyCtxt) -> String {
+    let span = if let Some(did) = did(item, tcx).as_local()
+        && let rustc_hir::Node::Item(item) = tcx.hir_node_by_def_id(did)
+    {
+        tcx.hir_span_with_body(item.hir_id())
+    } else {
+        internal(tcx, item.span())
+    };
+    src_from_span_internal(span, tcx)
 }
 
 pub fn src_from_span(span: Span, tcx: TyCtxt) -> String {
     let span = internal(tcx, span);
+    src_from_span_internal(span, tcx)
+}
+
+fn src_from_span_internal(span: rustc_span::Span, tcx: TyCtxt) -> String {
     let src_map = tcx.sess.source_map();
     src_map.span_to_snippet(span).unwrap_or_default()
 }

From 657206158783a93d042261df47aa3929cf4c8bf1 Mon Sep 17 00:00:00 2001
From: zjp <jiping_zhou@foxmail.com>
Date: Sat, 31 Jan 2026 15:25:54 +0000
Subject: [PATCH 3/5] ui: adjust margins

---
 ui/app/components/code/AdtPopup.vue | 2 +-
 ui/app/components/code/Help.vue     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/ui/app/components/code/AdtPopup.vue b/ui/app/components/code/AdtPopup.vue
index e151538..2cfe525 100644
--- a/ui/app/components/code/AdtPopup.vue
+++ b/ui/app/components/code/AdtPopup.vue
@@ -1,6 +1,6 @@
 <template>
   <div class="min-h-[75vh] flex">
-    <UTree :items="items" :get-key="item => item.id" v-model="active" class="w-50 h-full"
+    <UTree :items="items" :get-key="item => item.id" v-model="active" class="w-50 h-full m-2"
       expandedIcon="tabler:square-letter-f" collapsedIcon="tabler:square-letter-f" />
 
     <div class="w-full">
diff --git a/ui/app/components/code/Help.vue b/ui/app/components/code/Help.vue
index 93d01b8..758ff8e 100644
--- a/ui/app/components/code/Help.vue
+++ b/ui/app/components/code/Help.vue
@@ -1,5 +1,5 @@
 <template>
-  <div class="overflow-y-auto p-10">
+  <div class="overflow-y-auto p-10 h-[80vh]">
     <CodeMarkdown :doc="help" :isWrapped="true" />
   </div>
 </template>

From cd7e8816362e8ba8aaf66ff6420703b37e749541 Mon Sep 17 00:00:00 2001
From: zjp <jiping_zhou@foxmail.com>
Date: Sat, 31 Jan 2026 15:29:14 +0000
Subject: [PATCH 4/5] out: add attributes in src

---
 data                |  2 +-
 src/output/utils.rs | 58 ++++++++++++++++++++++++++++++++++++++++-----
 2 files changed, 53 insertions(+), 7 deletions(-)

diff --git a/data b/data
index 7d71849..60095b4 160000
--- a/data
+++ b/data
@@ -1 +1 @@
-Subproject commit 7d718494630194493aa4e4cb12d04bd81ed117a9
+Subproject commit 60095b443a0cb6c5d54cd6259c433cfcdba1ea95
diff --git a/src/output/utils.rs b/src/output/utils.rs
index 03897d5..f5475eb 100644
--- a/src/output/utils.rs
+++ b/src/output/utils.rs
@@ -1,4 +1,6 @@
-use rustc_hir::def_id::DefId as IDefId;
+extern crate rustc_hir_pretty;
+use itertools::Itertools;
+use rustc_hir::{Attribute, attrs::AttributeKind, def_id::DefId as IDefId};
 use rustc_middle::ty::TyCtxt;
 use rustc_public::{
     CrateDef,
@@ -44,14 +46,58 @@ pub fn span<T: CrateDef>(item: T, tcx: TyCtxt) -> String {
 }
 
 pub fn src<T: CrateDef + Copy>(item: T, tcx: TyCtxt) -> String {
-    let span = if let Some(did) = did(item, tcx).as_local()
-        && let rustc_hir::Node::Item(item) = tcx.hir_node_by_def_id(did)
+    let [attrs, item_src] = if let Some(did) = did(item, tcx).as_local()
+        && let rustc_hir::Node::Item(hir_item) = tcx.hir_node_by_def_id(did)
     {
-        tcx.hir_span_with_body(item.hir_id())
+        let hir_id = hir_item.hir_id();
+        let span = tcx.hir_span_with_body(hir_id);
+        let item_src = src_from_span_internal(span, tcx);
+
+        let attrs = tcx
+            .hir_attrs(hir_id)
+            .iter()
+            .filter_map(|attr| match attr {
+                Attribute::Parsed(parsed) => {
+                    if let AttributeKind::Align { .. }
+                    | AttributeKind::AutomaticallyDerived(_)
+                    | AttributeKind::Deprecation { .. }
+                    | AttributeKind::ExportName { .. }
+                    | AttributeKind::LinkName { .. }
+                    | AttributeKind::LinkSection { .. }
+                    | AttributeKind::Fundamental
+                    | AttributeKind::Link(..)
+                    | AttributeKind::MayDangle(..)
+                    | AttributeKind::Marker(..)
+                    | AttributeKind::Naked(..)
+                    | AttributeKind::NoMangle(..)
+                    | AttributeKind::NonExhaustive(..)
+                    | AttributeKind::Pointee(..)
+                    | AttributeKind::Repr { .. }
+                    | AttributeKind::TargetFeature { .. } = parsed
+                    {
+                        Some(rustc_hir_pretty::attribute_to_string(&tcx, attr))
+                    } else {
+                        None
+                    }
+                }
+                // Doc and rustc attribute can still apear, so we collect tool attribute below.
+                Attribute::Unparsed(_) => None,
+            })
+            .chain(item.all_tool_attrs().iter().map(|a| a.as_str().to_owned()))
+            .join("");
+
+        [attrs, item_src]
     } else {
-        internal(tcx, item.span())
+        // Non-local items are hard to query span with body and full attributes.
+        let item_src = src_from_span(item.span(), tcx);
+        let attrs = item.all_tool_attrs().iter().map(|a| a.as_str()).join("");
+        [attrs, item_src]
     };
-    src_from_span_internal(span, tcx)
+    if attrs.is_empty() {
+        item_src
+    } else {
+        format!("{attrs}{item_src}")
+    }
 }
 
 pub fn src_from_span(span: Span, tcx: TyCtxt) -> String {

From 6eeb1635c71434d602d3dc3d5edac0f078e480c3 Mon Sep 17 00:00:00 2001
From: zjp <jiping_zhou@foxmail.com>
Date: Sat, 31 Jan 2026 16:23:09 +0000
Subject: [PATCH 5/5] ui(AdtPopup): fix tree and panel size with grid layout

---
 ui/app/components/code/AdtPopup.vue   | 4 ++--
 ui/app/components/widget/SearchFn.vue | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/ui/app/components/code/AdtPopup.vue b/ui/app/components/code/AdtPopup.vue
index 2cfe525..2ce3a01 100644
--- a/ui/app/components/code/AdtPopup.vue
+++ b/ui/app/components/code/AdtPopup.vue
@@ -1,6 +1,6 @@
 <template>
-  <div class="min-h-[75vh] flex">
-    <UTree :items="items" :get-key="item => item.id" v-model="active" class="w-50 h-full m-2"
+  <div class="grid grid-cols-[auto_1fr]">
+    <UTree :items="items" :get-key="item => item.id" v-model="active" class="m-2 overflow-y-auto h-0 min-h-full"
       expandedIcon="tabler:square-letter-f" collapsedIcon="tabler:square-letter-f" />
 
     <div class="w-full">
diff --git a/ui/app/components/widget/SearchFn.vue b/ui/app/components/widget/SearchFn.vue
index 80dad8b..7efc5fa 100644
--- a/ui/app/components/widget/SearchFn.vue
+++ b/ui/app/components/widget/SearchFn.vue
@@ -10,7 +10,7 @@
       </li>
     </ol>
   </div>
-  <div class="flex justify-between items-center m-2">
+  <div class="min-h-fit flex justify-between items-center m-2">
     <WidgetPaginator :total="fullFns.length" v-model:itemsPerPage="search.itemsPerPage" v-model:page="search.page" />
 
     <div class="flex justify-end items-center gap-2">