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
2 changes: 1 addition & 1 deletion data
Submodule data updated 3456 files
63 changes: 60 additions & 3 deletions src/output/utils.rs
Original file line number Diff line number Diff line change
@@ -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,
Expand Down Expand Up @@ -43,12 +45,67 @@ 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 [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)
{
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 {
// 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]
};
if attrs.is_empty() {
item_src
} else {
format!("{attrs}{item_src}")
}
}

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()
}
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,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"
<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">
Expand Down
80 changes: 80 additions & 0 deletions ui/app/components/code/Help.vue
Original file line number Diff line number Diff line change
@@ -0,0 +1,80 @@
<template>
<div class="overflow-y-auto p-10 h-[80vh]">
<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>
2 changes: 1 addition & 1 deletion ui/app/components/widget/SearchFn.vue
Original file line number Diff line number Diff line change
Expand Up @@ -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">
Expand Down
9 changes: 9 additions & 0 deletions ui/app/components/widget/TopBar.vue
Original file line number Diff line number Diff line change
Expand Up @@ -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>
Expand Down
1 change: 1 addition & 0 deletions ui/nuxt.config.ts
Original file line number Diff line number Diff line change
Expand Up @@ -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
],
}
},
Expand Down