Skip to content

Commit

Permalink
add path process logic in senryx
Browse files Browse the repository at this point in the history
  • Loading branch information
DiuDiu777 committed Oct 11, 2024
1 parent 55a980d commit 1b92416
Show file tree
Hide file tree
Showing 6 changed files with 157 additions and 34 deletions.
22 changes: 22 additions & 0 deletions rap/src/analysis/safedrop/graph.rs
Original file line number Diff line number Diff line change
Expand Up @@ -462,4 +462,26 @@ impl<'tcx> SafeDropGraph<'tcx> {
let mut time = 0;
self.tarjan(0, &mut stack, &mut instack, &mut dfn, &mut low, &mut time);
}

pub fn dfs_on_spanning_tree(&self, index: usize, stack: &mut Vec<usize>, paths: &mut Vec<Vec<usize>>) {
let curr_scc_index = self.scc_indices[index];
if self.blocks[curr_scc_index].next.len() == 0 {
paths.push(stack.to_vec());
} else {
for child in self.blocks[curr_scc_index].next.iter() {
stack.push(*child);
self.dfs_on_spanning_tree(*child, stack, paths);
}
}
stack.pop();
}

pub fn get_paths(&self) -> Vec<Vec<usize>> {
// rap_debug!("dfs here");
let mut paths: Vec<Vec<usize>> = Vec::new();
let mut stack: Vec<usize> = vec![0];
self.dfs_on_spanning_tree(0, &mut stack, &mut paths);

return paths;
}
}
9 changes: 5 additions & 4 deletions rap/src/analysis/senryx.rs
Original file line number Diff line number Diff line change
Expand Up @@ -48,20 +48,21 @@ impl<'tcx> SenryxCheck<'tcx>{
pub fn pre_handle_type(&self, def_id: DefId) {
let mut uig_checker = UnsafetyIsolationCheck::new(self.tcx);
let func_type = uig_checker.get_type(def_id);
let mut body_visitor = BodyVisitor::new(self.tcx);
let mut body_visitor = BodyVisitor::new(self.tcx, def_id);
if func_type == 1 {
let func_cons = uig_checker.search_constructor(def_id);
for func_con in func_cons {
body_visitor.path_forward_check(func_con);
let mut cons_body_visitor = BodyVisitor::new(self.tcx, func_con);
cons_body_visitor.path_forward_check();
// TODO: cache fields' states

// TODO: update method body's states

// analyze body's states
body_visitor.path_forward_check(def_id);
body_visitor.path_forward_check();
}
} else {
body_visitor.path_forward_check(def_id);
body_visitor.path_forward_check();
}
}

Expand Down
44 changes: 42 additions & 2 deletions rap/src/analysis/senryx/contracts/abstract_state.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
use std::{collections::{HashMap, HashSet}, hash::Hash};

use super::state_lattice::Lattice;

#[derive(Debug, PartialEq, PartialOrd, Copy, Clone)]
pub enum Value {
Usize(usize),
Expand Down Expand Up @@ -39,10 +41,17 @@ pub enum AllocatedState {
#[derive(Debug, PartialEq, Eq, Hash, Copy, Clone)]
pub enum AlignState {
Aligned,
Unaligned,
Small2BigCast,
Big2SmallCast,
}

#[derive(Debug, PartialEq)]
#[derive(Debug, PartialEq, Eq, Hash, Copy, Clone)]
pub enum InitState {
FullyInitialized,
PartlyInitialized,
}

#[derive(Debug, PartialEq, Clone)]
pub struct AbstractStateItem {
pub value: (Value,Value),
pub state: HashSet<StateType>,
Expand All @@ -55,6 +64,37 @@ impl AbstractStateItem {
state,
}
}

pub fn meet_state_item(&mut self, other_state:&AbstractStateItem) {
let mut new_state = HashSet::new();

// visit 'self.state' and 'other_state.state',matching states and calling meet method
for state_self in &self.state {
// if find the same state type in 'other_state', then meet it;
if let Some(matching_state) = other_state
.state
.iter()
.find(|state_other| std::mem::discriminant(*state_other) == std::mem::discriminant(state_self))
{
let merged_state = match (state_self, matching_state) {
(StateType::AllocatedState(s1), StateType::AllocatedState(s2)) => {
StateType::AllocatedState(s1.meet(*s2))
}
(StateType::AlignState(s1), StateType::AlignState(s2)) => {
StateType::AlignState(s1.meet(*s2))
}
_ => continue,
};
new_state.insert(merged_state);
} else {
// if 'other_state' does not have the same state,then reserve the current state
new_state.insert(*state_self);
}
}

// 更新 self 的状态
self.state = new_state;
}
}

pub struct AbstractState {
Expand Down
48 changes: 42 additions & 6 deletions rap/src/analysis/senryx/contracts/state_lattice.rs
Original file line number Diff line number Diff line change
Expand Up @@ -114,22 +114,58 @@ impl Lattice for AllocatedState {
impl Lattice for AlignState {
fn join(&self, other: Self) -> Self {
match (self, other) {
(AlignState::Aligned, AlignState::Unaligned) | (AlignState::Unaligned, AlignState::Aligned) => AlignState::Unaligned,
(AlignState::Aligned, AlignState::Aligned) => AlignState::Aligned,
(AlignState::Unaligned, AlignState::Unaligned) => AlignState::Unaligned,
(AlignState::Aligned, _) => AlignState::Aligned,
(AlignState::Big2SmallCast, AlignState::Big2SmallCast) => AlignState::Big2SmallCast,
(AlignState::Big2SmallCast, AlignState::Small2BigCast) => AlignState::Big2SmallCast,
(AlignState::Big2SmallCast, AlignState::Aligned) => AlignState::Aligned,
(AlignState::Small2BigCast, _) => other,
}
}

fn meet(&self, other: Self) -> Self {
match (self, other) {
(AlignState::Aligned, _) | (_, AlignState::Aligned) => AlignState::Aligned,
(AlignState::Unaligned, AlignState::Unaligned) => AlignState::Unaligned,
(AlignState::Aligned, _) => other,
(AlignState::Big2SmallCast, AlignState::Big2SmallCast) => AlignState::Big2SmallCast,
(AlignState::Big2SmallCast, AlignState::Small2BigCast) => AlignState::Small2BigCast,
(AlignState::Big2SmallCast, AlignState::Aligned) => AlignState::Big2SmallCast,
(AlignState::Small2BigCast, _) => AlignState::Small2BigCast,
}
}

fn less_than(&self, other: Self) -> bool {
match (self, other) {
(AlignState::Aligned, AlignState::Unaligned) => true,
(_, AlignState::Aligned) => true,
(AlignState::Small2BigCast, AlignState::Big2SmallCast) => true,
_ => false,
}
}

fn equal(&self, other: Self) -> bool {
*self == other
}
}

impl Lattice for InitState {
fn join(&self, other: Self) -> Self {
match (self, other) {
(InitState::FullyInitialized, _) => InitState::FullyInitialized,
(_, InitState::FullyInitialized) => InitState::FullyInitialized,
_ => InitState::PartlyInitialized,
}
}

fn meet(&self, other: Self) -> Self {
match (self, other) {
(InitState::FullyInitialized, _) => other,
(_, InitState::FullyInitialized) => *self,
_ => InitState::PartlyInitialized,
}
}

fn less_than(&self, other: Self) -> bool {
match (self, other) {
(InitState::FullyInitialized, InitState::FullyInitialized) => true,
(InitState::PartlyInitialized, _) => true,
_ => false,
}
}
Expand Down
2 changes: 1 addition & 1 deletion rap/src/analysis/senryx/matcher.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ use super::contracts::{abstract_state::AbstractState, checker::{Checker, SliceFr

pub fn match_unsafe_api_and_check_contracts<T>(func_name: &str, args:&Vec<Operand>, abstate:&AbstractState, _ty: T) {
let base_func_name = func_name.split::<&str>("<").next().unwrap_or(func_name);
println!("base name ---- {:?}",base_func_name);
// println!("base name ---- {:?}",base_func_name);
let checker: Option<Box<dyn Checker>> = match base_func_name {
"std::slice::from_raw_parts::" => {
Some(Box::new(SliceFromRawPartsChecker::<T>::new()))
Expand Down
66 changes: 45 additions & 21 deletions rap/src/analysis/senryx/visitor.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,7 @@
use std::collections::HashMap;

use crate::analysis::safedrop::graph::SafeDropGraph;

use super::contracts::abstract_state::AbstractState;
use super::matcher::match_unsafe_api_and_check_contracts;
use rustc_middle::ty::TyCtxt;
Expand All @@ -10,36 +14,42 @@ use rustc_hir::def_id::DefId;

pub struct BodyVisitor<'tcx> {
pub tcx: TyCtxt<'tcx>,
pub abstract_states: AbstractState,
pub scc_sub_blocks: Vec<Vec<usize>>,
pub def_id: DefId,
pub safedrop_graph: SafeDropGraph<'tcx>,
pub abstract_states: HashMap<usize,AbstractState>,
}

impl<'tcx> BodyVisitor<'tcx> {
pub fn new(tcx: TyCtxt<'tcx>) -> Self{
pub fn new(tcx: TyCtxt<'tcx>, def_id: DefId) -> Self{
let body = tcx.optimized_mir(def_id);
Self{
tcx,
abstract_states: AbstractState::new(),
scc_sub_blocks: Vec::new(),
def_id,
safedrop_graph: SafeDropGraph::new(body, tcx, def_id),
abstract_states: HashMap::new(),
}
}

pub fn path_forward_check(&mut self, def_id: DefId) {
let paths = self.get_all_paths(def_id);
let body = self.tcx.optimized_mir(def_id);
pub fn path_forward_check(&mut self) {
let paths = self.get_all_paths();
let body = self.tcx.optimized_mir(self.def_id);
for (index, path_info) in paths.iter().enumerate() {
self.abstract_states.insert(index, AbstractState::new());
for block_index in path_info.iter() {
if block_index >= &body.basic_blocks.len(){
continue;
}
self.path_analyze_block(&body.basic_blocks[BasicBlock::from_usize(*block_index)].clone(), index, *block_index);
// let tem_scc_sub_blocks = self.scc_sub_blocks[*block_index].clone();
// if tem_scc_sub_blocks.len() > 0{
// for sub_block in &tem_scc_sub_blocks {
// self.path_analyze_block(&body.basic_blocks[BasicBlock::from_usize(*sub_block)].clone(), index, *block_index);
// }
// }
let tem_scc_sub_blocks = self.safedrop_graph.blocks[*block_index].scc_sub_blocks.clone();
// println!("father block {:?} scc sub blocks {:?}", block_index, tem_scc_sub_blocks);
if tem_scc_sub_blocks.len() > 0{
for sub_block in &tem_scc_sub_blocks {
self.path_analyze_block(&body.basic_blocks[BasicBlock::from_usize(*sub_block)].clone(), index, *block_index);
}
}
}
}
self.abstract_states_mop();
}

pub fn path_analyze_block(&mut self, block:&BasicBlockData<'tcx>, path_index:usize, bb_index: usize,) {
Expand All @@ -49,7 +59,7 @@ impl<'tcx> BodyVisitor<'tcx> {
self.path_analyze_terminator(&block.terminator(), path_index, bb_index);
}

pub fn path_analyze_terminator(&mut self, terminator:&Terminator<'tcx>, _path_index:usize, _bb_index: usize) {
pub fn path_analyze_terminator(&mut self, terminator:&Terminator<'tcx>, path_index:usize, _bb_index: usize) {
match &terminator.kind {
TerminatorKind::Call{func, args, destination: _, target: _, ..} => {
let func_name = format!("{:?}",func);
Expand All @@ -58,7 +68,7 @@ impl<'tcx> BodyVisitor<'tcx> {
for generic_arg in raw_list.iter() {
match generic_arg.unpack() {
GenericArgKind::Type(ty) => {
match_unsafe_api_and_check_contracts(func_name.as_str(), args, &self.abstract_states, ty);
match_unsafe_api_and_check_contracts(func_name.as_str(), args, &self.abstract_states.get(&path_index).unwrap(), ty);
}
_ => {}
}
Expand Down Expand Up @@ -179,14 +189,28 @@ impl<'tcx> BodyVisitor<'tcx> {
return current_local;
}

pub fn get_all_paths(&self, def_id: DefId) -> Vec<Vec<usize>> {
// let results = Vec::new();
let results = vec![vec![0,1,2,3,4,5,6,7,8]];
let _body = self.tcx.optimized_mir(def_id);
// TODO: get all paths in a body
pub fn get_all_paths(&mut self) -> Vec<Vec<usize>> {
self.safedrop_graph.solve_scc();
let results = self.safedrop_graph.get_paths();
results
}

pub fn abstract_states_mop(&mut self) {
let mut result_state = AbstractState {
state_map: HashMap::new(),
};

for (_path_idx, abstract_state) in &self.abstract_states {
for (var_index, state_item) in &abstract_state.state_map {
if let Some(existing_state_item) = result_state.state_map.get_mut(&var_index) {
existing_state_item.meet_state_item(state_item);
} else {
result_state.state_map.insert(*var_index, state_item.clone());
}
}
}
}

pub fn get_all_callees(&self, def_id: DefId) -> Vec<String> {
let mut results = Vec::new();
let body = self.tcx.optimized_mir(def_id);
Expand Down

0 comments on commit 1b92416

Please sign in to comment.