Skip to content

Commit

Permalink
Marker unsoundness warnings (#72)
Browse files Browse the repository at this point in the history
## What Changed?

Emits two new warnings:

1. If a marked type is constructed inline
2. If a function is not inlined but a marker is reachable inside

## Why Does It Need To?

Both of these cases are indicative of unsoundness so we want to make the
developer aware.

## Checklist

- [x] Above description has been filled out so that upon quash merge we
have a
  good record of what changed.
- [ ] New functions, methods, types are documented. Old documentation is
updated
  if necessary
- [x] Documentation in Notion has been updated
- [ ] Tests for new behaviors are provided
  - [ ] New test suites (if any) ave been added to the CI tests (in
`.github/workflows/rust.yml`) either as compiler test or integration
test.
*Or* justification for their omission from CI has been provided in this
PR
    description.
  • Loading branch information
JustusAdam authored Oct 9, 2023
1 parent 1758539 commit 505cd31
Show file tree
Hide file tree
Showing 5 changed files with 99 additions and 5 deletions.
9 changes: 9 additions & 0 deletions crates/paralegal-flow/src/ana/inline/judge.rs
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,15 @@ impl<'tcx> InlineJudge<'tcx> {
self.analysis_control.use_recursive_analysis() && !self.function_has_markers(function)
}

/// Access to uninterpreted marker information
///
/// This should only be used to issue warnings. For semnatically meaningful
/// interpretations of markers on function should be implemented on this
/// judge instead.
pub fn marker_ctx(&self) -> &MarkerCtx<'tcx> {
&self.marker_ctx
}

/// Is a marker reachable from this item?
fn marker_is_reachable(&self, def_id: DefId) -> bool {
self.marker_ctx.marker_is_reachable(def_id)
Expand Down
14 changes: 12 additions & 2 deletions crates/paralegal-flow/src/ana/inline/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ use crate::{
ty,
utils::{
body_name_pls, dump_file_pls, time, write_sep, DisplayViaDebug, FnResolution, Print,
RecursionBreakingCache, TyCtxtExt,
RecursionBreakingCache, Spanned, TyCtxtExt,
},
AnalysisCtrl, DumpArgs, Either, HashMap, HashSet, MarkerCtx, Symbol, TyCtxt,
};
Expand Down Expand Up @@ -631,6 +631,7 @@ impl<'tcx> Inliner<'tcx> {
i_graph: &mut InlinedGraph<'tcx>,
def_id: DefId,
) -> EdgeSet<'tcx> {
let caller_local_def_id = def_id.expect_local();
let recursive_analysis_enabled = self.ana_ctrl.use_recursive_analysis();
let mut queue_for_pruning = HashSet::new();
if recursive_analysis_enabled && self.try_inline_as_async_fn(i_graph, def_id) {
Expand All @@ -645,6 +646,7 @@ impl<'tcx> Inliner<'tcx> {
})
.filter_map(|(id, location, function)| {
if recursive_analysis_enabled {
let def_id = function.def_id();
debug!("Recursive analysis enabled");
if let Some(ac) = self.classify_special_function_handling(
function.def_id(),
Expand All @@ -653,11 +655,19 @@ impl<'tcx> Inliner<'tcx> {
) {
return Some((id, *location, InlineAction::Drop(ac)));
}
if let Some(local_id) = function.def_id().as_local()
if let Some(local_id) = def_id.as_local()
&& self.marker_carrying.should_inline(*function)
{
debug!("Inlining {function:?}");
return Some((id, *location, InlineAction::SimpleInline(local_id)));
} else if self.marker_carrying.marker_ctx().has_transitive_reachable_markers(def_id) {
self.tcx.sess.struct_span_warn(
self.tcx.def_span(def_id),
"This function is not being inlined, but a marker is reachable from its inside.",
).span_note(
(caller_local_def_id, location.innermost_location()).span(self.tcx),
"Called from here"
).emit()
}
}
let local_as_global = GlobalLocal::at_root;
Expand Down
40 changes: 39 additions & 1 deletion crates/paralegal-flow/src/ir/regal.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ use flowistry::indexed::{
impls::{build_location_arg_domain, LocationOrArg},
IndexedDomain,
};
use mir::{AggregateKind, Rvalue};
use paralegal_spdg::rustc_portable::DefId;
use rustc_utils::{mir::control_dependencies::ControlDependencies, BodyExt};

Expand All @@ -18,7 +19,7 @@ use crate::{
body_name_pls, dump_file_pls, time, write_sep, AsFnAndArgs, AsFnAndArgsErr,
DisplayViaDebug, FnResolution, TyCtxtExt,
},
DumpArgs, Either, HashMap, HashSet, TyCtxt,
DumpArgs, Either, HashMap, HashSet, MarkerCtx, TyCtxt,
};

use std::fmt::{Display, Write};
Expand Down Expand Up @@ -551,6 +552,37 @@ fn recursive_ctrl_deps<
dependencies
}

fn warn_if_marked_type_constructed<'tcx>(
tcx: TyCtxt<'tcx>,
marker_ctx: MarkerCtx<'tcx>,
def_id: crate::DefId,
body: &mir::Body<'tcx>,
) {
struct WarnVisitor<'tcx> {
marker_ctx: MarkerCtx<'tcx>,
tcx: TyCtxt<'tcx>,
fun: crate::DefId,
}

impl<'tcx> mir::visit::Visitor<'tcx> for WarnVisitor<'tcx> {
fn visit_rvalue(&mut self, rvalue: &mir::Rvalue<'tcx>, location: Location) {
if let Rvalue::Aggregate(box AggregateKind::Adt(did, ..), _) = rvalue
&& self.marker_ctx.is_marked(did)
{
warn!("Found constructor for marked ADT type {} in {} at {:?}. This can cause unsoundness as this value will not carry the marker.", self.tcx.def_path_debug_str(*did), self.tcx.def_path_debug_str(self.fun), location)
}
}
}

let mut vis = WarnVisitor {
tcx,
fun: def_id,
marker_ctx,
};

mir::visit::Visitor::visit_body(&mut vis, body)
}

pub fn compute_from_def_id<'tcx>(
dbg_opts: &DumpArgs,
def_id: DefId,
Expand All @@ -561,6 +593,12 @@ pub fn compute_from_def_id<'tcx>(
info!("Analyzing function {}", body_name_pls(tcx, local_def_id));
let body_with_facts = tcx.body_for_def_id(def_id).unwrap();
let body = body_with_facts.simplified_body();
warn_if_marked_type_constructed(
tcx,
carries_marker.marker_ctx().clone(),
local_def_id.to_def_id(),
body,
);
let flow = df::compute_flow_internal(tcx, def_id, body_with_facts, carries_marker);
if dbg_opts.dump_callee_mir() {
mir::pretty::write_mir_fn(
Expand Down
2 changes: 1 addition & 1 deletion crates/paralegal-flow/src/marker_db.rs
Original file line number Diff line number Diff line change
Expand Up @@ -136,7 +136,7 @@ impl<'tcx> MarkerCtx<'tcx> {
}

/// Queries the transitive marker cache.
fn has_transitive_reachable_markers(&self, def_id: DefId) -> bool {
pub fn has_transitive_reachable_markers(&self, def_id: DefId) -> bool {
self.db()
.marker_reachable_cache
.get_maybe_recursive(def_id, |_| self.compute_marker_reachable(def_id))
Expand Down
39 changes: 38 additions & 1 deletion crates/paralegal-flow/src/utils/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ use crate::{
mir::{self, Location, Place, ProjectionElem, Statement, Terminator},
rustc_data_structures::fx::{FxHashMap, FxHashSet},
rustc_data_structures::intern::Interned,
rustc_span::symbol::Ident,
rustc_span::{symbol::Ident, Span},
rustc_target::spec::abi::Abi,
ty,
},
Expand Down Expand Up @@ -1204,3 +1204,40 @@ pub fn data_source_from_global_location<F: FnOnce(mir::Location) -> bool>(
))
}
}

pub trait Spanned<'tcx> {
fn span(&self, tcx: TyCtxt<'tcx>) -> Span;
}

impl<'tcx> Spanned<'tcx> for mir::Terminator<'tcx> {
fn span(&self, _tcx: TyCtxt<'tcx>) -> Span {
self.source_info.span
}
}

impl<'tcx> Spanned<'tcx> for mir::Statement<'tcx> {
fn span(&self, _tcx: TyCtxt<'tcx>) -> Span {
self.source_info.span
}
}

impl<'tcx> Spanned<'tcx> for (&mir::Body<'tcx>, mir::Location) {
fn span(&self, tcx: TyCtxt<'tcx>) -> Span {
self.0
.stmt_at(self.1)
.either(|e| e.span(tcx), |e| e.span(tcx))
}
}

impl<'tcx> Spanned<'tcx> for DefId {
fn span(&self, tcx: TyCtxt<'tcx>) -> Span {
tcx.def_span(*self)
}
}

impl<'tcx> Spanned<'tcx> for (LocalDefId, mir::Location) {
fn span(&self, tcx: TyCtxt<'tcx>) -> Span {
let body = tcx.body_for_def_id(self.0.to_def_id()).unwrap();
(body.simplified_body(), self.1).span(tcx)
}
}

0 comments on commit 505cd31

Please sign in to comment.