Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
95 changes: 95 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,95 @@
# Web UI for Rust Unsafety Propogation Graph

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.

[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
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)

<details>

<summary>The search interface renders tags as badges adjacent to the function name.</summary>

![](https://github.com/user-attachments/assets/f247945f-0806-42dd-987a-6148f2412a27)

![](https://github.com/user-attachments/assets/4cf9956f-bdbf-4a62-a3aa-c7d7bdb4737b)

</details>

### 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)

## Build the project

Commands to build the UI project:

```bash
cd ui
# Install dependencies
npm install
# Generate static webpage artifacts
npm run generate
# Start the development server on `http://localhost:3000`:
npm run dev
# Locally preview production build:
npm run preview
```

17 changes: 0 additions & 17 deletions ui/README.md

This file was deleted.

7 changes: 2 additions & 5 deletions ui/app/components/UPG.vue
Original file line number Diff line number Diff line change
Expand Up @@ -92,14 +92,11 @@ const adtOpts = ref<AdtOpts>({});

const adtClicked = ref<AdtClicked>({ open: false })
watch(() => ({
isAdtPanel: upPanel.value === Panel.Adt || downPanel.value === Panel.Adt,
isClicked: adtClicked.value.clickedAdt || adtClicked.value.clickedField,
adt: adtClicked.value
}), ({ isAdtPanel, isClicked, adt }) => {
// Auto open adt panel when side panels doesn't show adt panel, and user clicked adt or field.
if (!isAdtPanel && isClicked) {
}), ({ isClicked, adt }) => {
if (isClicked)
adtClicked.value = { open: true, lastClickedAdt: adt.clickedAdt, lastClickedField: adt.clickedField }
}
})

const share = ref<boolean>(false)
Expand Down
4 changes: 2 additions & 2 deletions ui/app/components/code/AdtPopup.vue
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
<template>
<div class="min-h-[75vh] flex">
<UTree :items="items" :get-key="item => item.id" v-model="active" class="w-50 h-full"
expanded-icon="tabler:square-letter-f" />
expandedIcon="tabler:square-letter-f" collapsedIcon="tabler:square-letter-f" />

<div class="w-full">
<WidgetSearchFn :v_fn="adtItem.v_fn" :unsafeFns="unsafeFns" v-model="search" :title="adtItem.desc" />
Expand Down Expand Up @@ -142,7 +142,7 @@ const initAdtItem = () => {
if (item) return { item, selected, selectedIdx }
}

const search = ref<Search>({ withTags: false, unsafeOnly: true, text: "", page: 1, itemsPerPage: 20 })
const search = ref<Search>({ withTags: false, unsafeOnly: false, text: "", page: 1, itemsPerPage: 20 })

const items = computed<TreeItem[]>(() => {
const tree: TreeItem[] = []
Expand Down
7 changes: 5 additions & 2 deletions ui/app/components/widget/SearchFn.vue
Original file line number Diff line number Diff line change
Expand Up @@ -23,12 +23,15 @@
</template>

<script setup lang="ts">
import type { Search, SearchFnItem, UnsafeFns } from '~/lib/topbar';
import { Unsafe, type Search, type SearchFnItem, type UnsafeFns } from '~/lib/topbar';

const props = defineProps<{ v_fn: SearchFnItem[], title: string, unsafeFns: UnsafeFns }>()

function isUnsafe(name: string): boolean {
return props.unsafeFns[name] ? true : false
switch (props.unsafeFns[name]) {
case Unsafe.Caller: case Unsafe.Both: return true;
default: return false;
}
}

const search = defineModel<Search>({ required: true })
Expand Down
8 changes: 4 additions & 4 deletions ui/app/components/widget/Tag.vue
Original file line number Diff line number Diff line change
Expand Up @@ -21,10 +21,10 @@
<div v-if="item.spec.types.length !== 0">
<UBadge color="neutral" variant="outline">Types</UBadge> {{ item.spec.types }}
</div>
<div v-if="item.spec.url">
<UBadge color="neutral" variant="outline">Ref</UBadge> <span class="w-2" />
<ULink external :to="item.spec.url" target="_blank">{{ item.spec.url }}</ULink>
</div>
<!-- <div v-if="item.spec.url"> -->
<!-- <UBadge color="neutral" variant="outline">Ref</UBadge> <span class="w-2" /> -->
<!-- <ULink external :to="item.spec.url" target="_blank">{{ item.spec.url }}</ULink> -->
<!-- </div> -->
<div v-if="item.occurence">
<UBadge color="neutral" variant="outline">Occurence</UBadge> {{ item.occurence }}
<div class="mt-2" v-if="showFunction">
Expand Down
6 changes: 3 additions & 3 deletions ui/app/lib/topbar.ts
Original file line number Diff line number Diff line change
Expand Up @@ -148,8 +148,8 @@ export const CRATES: Crate[] = [Crate.std, Crate.core, Crate.alloc, Crate.ostd];

export function defaultCrateItemQuery(crate: Crate): string {
switch (crate) {
case Crate.std: return "std::time::Instant::now";
case Crate.core: return "core::str::<impl str>::len";
case Crate.std: return "std::<os::unix::net::listener::UnixListener as os::fd::raw::FromRawFd>::from_raw_fd";
case Crate.core: return "core::ptr::write_volatile";
case Crate.alloc: return "alloc::vec::Vec::<T, A>::set_len";
case Crate.ostd: return "ostd::init";
default: return "";
Expand Down Expand Up @@ -208,5 +208,5 @@ export type UnsafeFns = {
}

export enum Unsafe {
Caller, Callee, Both,
Caller = "Caller", Callee = " Callee", Both = "Both",
}
3 changes: 2 additions & 1 deletion ui/app/utils/graph.ts
Original file line number Diff line number Diff line change
Expand Up @@ -551,7 +551,8 @@ export class Plot {
switch (kind) {
case AdtFnKind.MethodImmutableRefReceiver:
case AdtFnKind.MethodMutableRefReceiver:
case AdtFnKind.MethodOwnedReceiver: {
case AdtFnKind.MethodOwnedReceiver:
case AdtFnKind.Constructor: {
const field = Object.entries(info.field)
.map(([name, access]) => ({ name, access }))
.filter(f => f.access !== FieldAccessKind.Other)
Expand Down