Skip to content

Commit

Permalink
Clean up warnings
Browse files Browse the repository at this point in the history
  • Loading branch information
gavinleroy committed Feb 20, 2024
1 parent 31966ae commit cf6c76b
Show file tree
Hide file tree
Showing 36 changed files with 441 additions and 433 deletions.
14 changes: 14 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -18,3 +18,17 @@ $ cargo install --path crates/argus_cli

$ cd ide && depot build
```

## FAQ

<h3 id="rustup-fails-on-install">rustup fails on installation</h3>

If rustup fails, especially with an error like "could not rename downloaded file", this is probably because Flowistry is running rustup concurrently with another tool (like rust-analyzer). Until [rustup#988](https://github.com/rust-lang/rustup/issues/988) is resolved, there is unfortunately no automated way around this.

To solve the issue, go to the command line and run:

```
rustup toolchain install nightly-2024-01-21 -c rust-src -c rustc-dev -c llvm-tools-preview
```

Then go back to VSCode and click "Continue" to let Flowistry continue installing.
5 changes: 0 additions & 5 deletions crates/argus/src/analysis/entry.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@ use rustc_hir::BodyId;
use rustc_infer::{infer::InferCtxt, traits::PredicateObligation};
use rustc_middle::ty::{Predicate, TyCtxt, TypeckResults};
use rustc_trait_selection::traits::solve::Goal;
use rustc_utils::source_map::range::CharRange;
use serde::Serialize;

use crate::{
Expand Down Expand Up @@ -209,10 +208,6 @@ pub(in crate::analysis) fn build_obligations_in_body<'tcx>(
body_id: BodyId,
typeck_results: &'tcx TypeckResults<'tcx>,
) -> (FullData<'tcx>, ObligationsInBody) {
let hir = tcx.hir();
let source_map = tcx.sess.source_map();
let body = hir.body(body_id);

let obligations = tls::take_obligations();
let obligation_data = tls::unsafe_take_data();

Expand Down
6 changes: 4 additions & 2 deletions crates/argus/src/analysis/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,16 +6,18 @@ mod transform;
use anyhow::Result;
use fluid_let::fluid_let;
use rustc_hir::BodyId;
use rustc_middle::ty::{print, TyCtxt};
use rustc_middle::ty::TyCtxt;
pub(crate) use tls::{FullObligationData, SynIdx, UODIdx};

#[cfg(feature = "testing")]
use crate::types::intermediate::FullData;
pub(crate) use crate::types::intermediate::{
EvaluationResult, FulfillmentData,
};
use crate::{
ext::TyCtxtExt,
proof_tree::SerializedTree,
types::{intermediate::FullData, ObligationsInBody, Target},
types::{ObligationsInBody, Target},
};

fluid_let! {
Expand Down
3 changes: 1 addition & 2 deletions crates/argus/src/analysis/transform.rs
Original file line number Diff line number Diff line change
Expand Up @@ -249,7 +249,7 @@ impl<'a, 'tcx: 'a> ObligationsBuilder<'a, 'tcx> {
.filter(|(_, that_id)| self.tcx.is_parent_of(**that_id, this_id))
.collect::<Vec<_>>();

let Some((expr_id, hir_id)) =
let Some((expr_id, _hir_id)) =
matching_expressions.iter().copied().find(|(_, this_id)| {
matching_expressions
.iter()
Expand Down Expand Up @@ -497,7 +497,6 @@ impl<'a, 'tcx: 'a> ObligationsBuilder<'a, 'tcx> {
let syn_id = self.synthetic_data.add(SyntheticData {
full_data: full_query_idx,
obligation: obligation.clone(),
result: res,
});

let with_provenance = compute_provenance(
Expand Down
21 changes: 5 additions & 16 deletions crates/argus/src/proof_tree/ext.rs
Original file line number Diff line number Diff line change
@@ -1,9 +1,5 @@
use rustc_hir::{def::Namespace, def_id::DefId, definitions::DefPathData};
use rustc_hir::def_id::DefId;
use rustc_infer::infer::InferCtxt;
use rustc_middle::ty::{
print::{FmtPrinter, Print},
TyCtxt,
};
use rustc_trait_selection::{
solve::inspect::InspectCandidate,
traits::{
Expand All @@ -12,8 +8,10 @@ use rustc_trait_selection::{
},
};

use crate::types::intermediate::EvaluationResult;

/// Pretty printing for results.
pub trait PrettyResultExt {
pub trait EvaluationResultExt {
fn pretty(&self) -> String;
fn is_yes(&self) -> bool;
}
Expand All @@ -25,17 +23,8 @@ pub trait CandidateExt {
fn is_informative_probe(&self) -> bool;
}

// -----------------------------------------------
// Impls

// impl<'a, 'tcx, T: Print<'tcx, FmtPrinter<'a, 'tcx>>> PrettyPrintExt<'a, 'tcx>
// for T
// {
// /* intentionally blank */
// }

/// Pretty printer for results
impl PrettyResultExt for Result<Certainty, NoSolution> {
impl EvaluationResultExt for EvaluationResult {
fn is_yes(&self) -> bool {
matches!(self, Ok(Certainty::Yes))
}
Expand Down
4 changes: 3 additions & 1 deletion crates/argus/src/proof_tree/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -119,9 +119,11 @@ impl Goal {
result: EvaluationResult,
) -> Self {
let necessity = infcx.guess_predicate_necessity(&goal.predicate);
let goal = infcx.resolve_vars_if_possible(*goal);
let num_vars =
serialize::var_counter::count_vars(infcx.tcx, goal.predicate);
let goal_value = serialize_to_value(infcx, &GoalPredicateDef(*goal))

let goal_value = serialize_to_value(infcx, &GoalPredicateDef(goal))
.expect("failed to serialize goal");

Self {
Expand Down
30 changes: 17 additions & 13 deletions crates/argus/src/proof_tree/serialize.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
use std::{collections::HashSet, ops::ControlFlow};

use anyhow::{bail, Result};
use ext::*;
use ext::{CandidateExt, EvaluationResultExt};
use index_vec::IndexVec;
use rustc_hir::def_id::DefId;
use rustc_infer::infer::InferCtxt;
Expand Down Expand Up @@ -65,22 +65,26 @@ impl SerializedTreeVisitor {
})
}

fn check_for_cycle_from(&mut self, from: ProofNodeIdx) {
// TODO: cycle detection is too expensive for large trees, and strictly
// comparing the JSON values is a bad idea in general. We should wait
// until the new trait solver has some mechanism for detecting cycles
// and piggy back off that.
fn check_for_cycle_from(&mut self, _from: ProofNodeIdx) {
return;

if self.cycle.is_some() {
return;
}
// if self.cycle.is_some() {
// return;
// }

let to_root = self.topology.path_to_root(from);
// let to_root = self.topology.path_to_root(from);

let node_start = &self.nodes[from];
if to_root.iter_exclusive().any(|idx| {
let n = &self.nodes[*idx];
n == node_start
}) {
self.cycle = Some(to_root.into());
}
// let node_start = &self.nodes[from];
// if to_root.iter_exclusive().any(|idx| {
// let n = &self.nodes[*idx];
// n == node_start
// }) {
// self.cycle = Some(to_root.into());
// }
}
}

Expand Down
63 changes: 2 additions & 61 deletions crates/argus/src/proof_tree/topology.rs
Original file line number Diff line number Diff line change
Expand Up @@ -106,78 +106,19 @@ impl TreeTopology {
}
}

// pub fn children(
// &self,
// from: ProofNodeIdx,
// ) -> impl Iterator<Item = ProofNodeIdx> {
// let v = match self.children.get(&from) {
// // Normally there are relatively few children.
// Some(kids) => kids
// .iter()
// .copied()
// .collect::<SmallVec<[ProofNodeIdx; 8]>>(),
// None => SmallVec::<[ProofNodeIdx; 8]>::default(),
// };

// v.into_iter()
// }

pub fn parent(&self, to: ProofNodeIdx) -> Option<ProofNodeIdx> {
self.parent.get(&to).copied()
}

// pub fn is_parent_of(
// &self,
// parent: ProofNodeIdx,
// child: ProofNodeIdx,
// ) -> bool {
// if let Some(p) = self.parent(child) {
// p == parent
// } else {
// false
// }
// }

// pub fn is_child_of(&self, child: ProofNodeIdx, parent: ProofNodeIdx) -> bool {
// self.is_parent_of(parent, child)
// }

// #[must_use]
// pub fn add_in(&mut self, rhs: Self) -> Option<()> {
// let lhs_keys = self.children.keys().collect::<HashSet<_>>();
// for key in rhs.children.keys() {
// if lhs_keys.contains(key) {
// return None;
// }
// }

// self.children.extend(rhs.children.into_iter());
// self.parent.extend(rhs.parent.into_iter());

// Some(())
// }

// pub fn is_member(&self, node: ProofNodeIdx) -> bool {
// self
// .children
// .keys()
// .chain(self.parent.keys())
// .find(|&&n| n == node)
// .is_some()
// }

// pub fn leaves(&self) -> impl Iterator<Item = ProofNodeIdx> + '_ {
// self.parent.keys().filter(|n| self.is_leaf(**n)).copied()
// }

pub fn path_to_root(&self, node: ProofNodeIdx) -> Path<ProofNodeIdx, ToRoot> {
let mut root = node;
let mut curr = Some(node);
let path = std::iter::from_fn(move || {
let rootp = &mut root;
let prev = curr;
if let Some(n) = curr {
curr = self.parent(n);
root = n;
*rootp = n;
}

prev
Expand Down
Loading

0 comments on commit cf6c76b

Please sign in to comment.