Skip to content

Commit

Permalink
deref refactoring
Browse files Browse the repository at this point in the history
  • Loading branch information
@Medowhill
Medowhill committed Jan 12, 2024
1 parent b637699 commit 8074f32
Show file tree
Hide file tree
Showing 2 changed files with 45 additions and 117 deletions.
148 changes: 42 additions & 106 deletions src/relational/domains.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -288,26 +288,9 @@ impl Graph {

pub fn assign(&mut self, l: &AccPath, l_deref: bool, r: &OpVal) {
match r {
OpVal::Place(r, r_deref) => match (l_deref, r_deref) {
(true, true) => panic!(),
(true, false) => self.deref_x_eq_y(l, r),
(false, true) => self.x_eq_deref_y(l, r),
(false, false) => self.x_eq_y(l, r),
},
OpVal::Int(n) => {
if l_deref {
self.deref_x_eq_int(l, *n);
} else {
self.x_eq_int(l, *n);
}
}
OpVal::Other => {
if l_deref {
self.deref_x_eq(l);
} else {
self.x_eq(l);
}
}
OpVal::Place(r, r_deref) => self.x_eq_y(l, l_deref, r, *r_deref),
OpVal::Int(n) => self.x_eq_int(l, l_deref, *n),
OpVal::Other => self.x_eq(l, l_deref),
}
}

Expand All @@ -325,105 +308,63 @@ impl Graph {
}
}

fn x_eq_y(&mut self, x: &AccPath, y: &AccPath) {
let (id, _) = self.get_local_node_mut(y.local);
let loc = self.get_pointed_loc_mut(id, &y.projection);

let obj = self.get_obj_mut(x);
*obj = Obj::Ptr(loc);
}

fn x_eq_deref_y(&mut self, x: &AccPath, y: &AccPath) {
let (id, _) = self.get_local_node_mut(y.local);
let mut loc = self.get_pointed_loc_mut(id, &[]);
loc.projection.extend(y.projection.to_owned());
let loc = self.get_pointed_loc_mut(loc.root, &loc.projection);

let obj = self.get_obj_mut(x);
*obj = Obj::Ptr(loc);
fn lvalue(&mut self, x: &AccPath, deref: bool) -> &mut Obj {
if deref {
let (id, _) = self.get_local_node_mut(x.local);
let mut loc = self.get_pointed_loc_mut(id, &[]);
loc.projection.extend(x.projection.to_owned());
let node = &mut self.nodes[loc.root];
node.obj.project_mut(&loc.projection)
} else {
let (_, node) = self.get_local_node_mut(x.local);
node.obj.project_mut(&x.projection)
}
}

fn deref_x_eq_y(&mut self, x: &AccPath, y: &AccPath) {
let (id, _) = self.get_local_node_mut(y.local);
let loc_y = self.get_pointed_loc_mut(id, &y.projection);

fn rvalue(&mut self, x: &AccPath, deref: bool) -> Location {
let (id, _) = self.get_local_node_mut(x.local);
let mut loc_x = self.get_pointed_loc_mut(id, &[]);
loc_x.projection.extend(x.projection.to_owned());

let node = &mut self.nodes[loc_x.root];
let obj = node.obj.project_mut(&loc_x.projection);
*obj = Obj::Ptr(loc_y);
}

pub fn x_eq_ref_y(&mut self, x: &AccPath, y: &AccPath) {
let (id, _) = self.get_local_node_mut(y.local);
let loc = Location::new(id, y.projection.to_owned());

let obj = self.get_obj_mut(x);
*obj = Obj::Ptr(loc);
if deref {
let mut loc = self.get_pointed_loc_mut(id, &[]);
loc.projection.extend(x.projection.to_owned());
self.get_pointed_loc_mut(loc.root, &loc.projection)
} else {
self.get_pointed_loc_mut(id, &x.projection)
}
}

pub fn x_eq_ref_deref_y(&mut self, x: &AccPath, y: &AccPath) {
let (id, _) = self.get_local_node_mut(y.local);
let mut loc = self.get_pointed_loc_mut(id, &[]);
loc.projection.extend(y.projection.to_owned());

let obj = self.get_obj_mut(x);
fn x_eq_y(&mut self, x: &AccPath, x_deref: bool, y: &AccPath, y_deref: bool) {
let loc = self.rvalue(y, y_deref);
let obj = self.lvalue(x, x_deref);
*obj = Obj::Ptr(loc);
}

fn x_eq_int(&mut self, x: &AccPath, n: Int) {
fn x_eq_int(&mut self, x: &AccPath, deref: bool, n: Int) {
let id = self.get_int_node(n);
let obj = self.get_obj_mut(x);
let obj = self.lvalue(x, deref);
*obj = Obj::Ptr(Location::new(id, vec![]));
}

fn deref_x_eq_int(&mut self, x: &AccPath, n: Int) {
let n_id = self.get_int_node(n);
let (id, _) = self.get_local_node_mut(x.local);
let mut loc = self.get_pointed_loc_mut(id, &[]);
loc.projection.extend(x.projection.to_owned());
let node = &mut self.nodes[loc.root];
let obj = node.obj.project_mut(&loc.projection);
*obj = Obj::Ptr(Location::new(n_id, vec![]));
}

fn x_eq(&mut self, x: &AccPath) {
let obj = self.get_obj_mut(x);
*obj = Obj::new();
}

fn deref_x_eq(&mut self, x: &AccPath) {
let (id, _) = self.get_local_node_mut(x.local);
let mut loc = self.get_pointed_loc_mut(id, &[]);
loc.projection.extend(x.projection.to_owned());
let node = &mut self.nodes[loc.root];
let obj = node.obj.project_mut(&loc.projection);
fn x_eq(&mut self, x: &AccPath, deref: bool) {
let obj = self.lvalue(x, deref);
*obj = Obj::new();
}

pub fn filter_x_int(&mut self, x: &AccPath, n: Int) {
let obj = self.get_obj_mut(x);
let Obj::Ptr(ptr) = obj else { unreachable!() };
assert!(ptr.projection.is_empty());
let id = ptr.root;

if let Some(n_id) = self.ints.get(&n) {
let n_id = *n_id;
self.substitute(id, n_id);
pub fn x_eq_ref_y(&mut self, x: &AccPath, y: &AccPath, y_deref: bool) {
let (id, _) = self.get_local_node_mut(y.local);
let loc = if y_deref {
let mut loc = self.get_pointed_loc_mut(id, &[]);
loc.projection.extend(y.projection.to_owned());
loc
} else {
self.nodes[id].at_addr = Some(n);
self.ints.insert(n, id);
}
Location::new(id, y.projection.to_owned())
};

let obj = self.lvalue(x, false);
*obj = Obj::Ptr(loc);
}

pub fn filter_deref_x_int(&mut self, x: &AccPath, n: Int) {
let (id, _) = self.get_local_node_mut(x.local);
let mut loc = self.get_pointed_loc_mut(id, &[]);
loc.projection.extend(x.projection.to_owned());
let node = &mut self.nodes[loc.root];
let obj = node.obj.project_mut(&loc.projection);
pub fn filter_x_int(&mut self, x: &AccPath, deref: bool, n: Int) {
let obj = self.lvalue(x, deref);
let Obj::Ptr(ptr) = obj else { unreachable!() };
assert!(ptr.projection.is_empty());
let id = ptr.root;
Expand Down Expand Up @@ -508,11 +449,6 @@ impl Graph {
}
loc
}

fn get_obj_mut(&mut self, x: &AccPath) -> &mut Obj {
let (_, node) = self.get_local_node_mut(x.local);
node.obj.project_mut(&x.projection)
}
}

fn join_objs(
Expand Down
14 changes: 3 additions & 11 deletions src/relational/semantics.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -79,12 +79,8 @@ impl<'tcx> Analyzer<'tcx> {
Rvalue::Ref(_, _, r) => {
assert!(suffixes.is_empty());
assert!(!l_deref);
let (path, is_deref) = AccPath::from_place(*r, state);
if is_deref {
state.gm().x_eq_ref_deref_y(&l, &path);
} else {
state.gm().x_eq_ref_y(&l, &path);
}
let (r, r_deref) = AccPath::from_place(*r, state);
state.gm().x_eq_ref_y(&l, &r, r_deref);
}
Rvalue::ThreadLocalRef(_) => {
assert!(suffixes.is_empty());
Expand Down Expand Up @@ -270,11 +266,7 @@ impl<'tcx> Analyzer<'tcx> {
};
let v = Int::from_u128(v, ty);
let mut state = state.clone();
if is_deref {
state.gm().filter_deref_x_int(&discr, v);
} else {
state.gm().filter_x_int(&discr, v);
}
state.gm().filter_x_int(&discr, is_deref, v);
(location, state)
})
.chain(std::iter::once((
Expand Down

0 comments on commit 8074f32

Please sign in to comment.