Skip to content

Commit

Permalink
Encode tag checks as SMT queries
Browse files Browse the repository at this point in the history
  • Loading branch information
@stonebuddha
stonebuddha committed Jun 30, 2020
1 parent 0e6352a commit f6c18ab
Show file tree
Hide file tree
Showing 10 changed files with 424 additions and 182 deletions.
100 changes: 58 additions & 42 deletions checker/src/abstract_value.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -255,6 +255,35 @@ impl AbstractValue {
)
}

/// Returns a tag check on `operand`. If we can decide the presence/absence of tag, return
/// TRUE/FALSE. Otherwise, returns an unknown tag check.
#[logfn_inputs(TRACE)]
pub fn make_tag_check(
operand: Rc<AbstractValue>,
tag: Tag,
checking_presence: bool,
) -> Rc<AbstractValue> {
let check_value = if checking_presence {
operand.has_tag(&tag)
} else {
operand.does_not_have_tag(&tag)
};
if check_value.is_top() {
// Cannot refine this tag check. Return again an unknown tag check.
let expression_size = operand.expression_size.saturating_add(1);
AbstractValue::make_from(
Expression::UnknownTagCheck {
operand,
tag,
checking_presence,
},
expression_size,
)
} else {
check_value
}
}

/// Creates an abstract value from the given expression and size.
/// Initializes the optional domains to None.
#[logfn_inputs(TRACE)]
Expand Down Expand Up @@ -1585,9 +1614,12 @@ impl AbstractValueTrait for Rc<AbstractValue> {
match &self.expression {
Expression::HeapBlock { is_zeroed, .. } => *is_zeroed,
Expression::Offset { left, .. } => left.is_contained_in_zeroed_heap_block(),
Expression::Reference(path)
| Expression::UnknownTagCheck { path, .. }
| Expression::Variable { path, .. } => path.is_rooted_by_zeroed_heap_block(),
Expression::Reference(path) | Expression::Variable { path, .. } => {
path.is_rooted_by_zeroed_heap_block()
}
Expression::UnknownTagCheck { operand, .. } => {
operand.is_contained_in_zeroed_heap_block()
}
_ => false,
}
}
Expand Down Expand Up @@ -2089,9 +2121,9 @@ impl AbstractValueTrait for Rc<AbstractValue> {
#[logfn_inputs(TRACE)]
fn refers_to_unknown_location(&self) -> bool {
match &self.expression {
Expression::Cast { operand, .. } | Expression::TaggedExpression { operand, .. } => {
operand.refers_to_unknown_location()
}
Expression::Cast { operand, .. }
| Expression::TaggedExpression { operand, .. }
| Expression::UnknownTagCheck { operand, .. } => operand.refers_to_unknown_location(),
Expression::ConditionalExpression {
consequent,
alternate,
Expand All @@ -2111,7 +2143,6 @@ impl AbstractValueTrait for Rc<AbstractValue> {
|| cases.iter().any(|(_, v)| v.refers_to_unknown_location())
}
Expression::UninterpretedCall { path, .. }
| Expression::UnknownTagCheck { path, .. }
| Expression::Variable { path, .. }
| Expression::Widen { path, .. } => {
if let PathEnum::Alias { value } = &path.value {
Expand Down Expand Up @@ -2613,7 +2644,6 @@ impl AbstractValueTrait for Rc<AbstractValue> {
cases,
default,
} => {
// tags(discriminator) | (tags(cases) join tags(default))
// For each tag A, whether the switch expression has tag A or not is
// (discriminator has tag A) or ((case_0 has tag A) join .. join (case_n has tag A) join (default has tag A)).
let mut tags_from_cases = (*default.get_cached_tags()).clone();
Expand Down Expand Up @@ -2908,33 +2938,14 @@ impl AbstractValueTrait for Rc<AbstractValue> {
}
}
Expression::UnknownTagCheck {
path,
operand,
tag,
checking_presence,
} => {
if let Some(val) = environment.value_at(&path) {
let check_value = if *checking_presence {
val.has_tag(tag)
} else {
val.does_not_have_tag(tag)
};
if check_value.is_top() {
// Still unknown, fall through.
} else {
return check_value;
}
}

// Cannot refine this tag check. Return again an unknown tag check.
AbstractValue::make_from(
Expression::UnknownTagCheck {
path: path.refine_paths(environment),
tag: *tag,
checking_presence: *checking_presence,
},
1,
)
}
} => AbstractValue::make_tag_check(
operand.refine_paths(environment),
*tag,
*checking_presence,
),
Expression::Variable { path, var_type } => {
if let Some(val) = environment.value_at(&path) {
val.clone()
Expand Down Expand Up @@ -3186,16 +3197,13 @@ impl AbstractValueTrait for Rc<AbstractValue> {
)
}
Expression::UnknownTagCheck {
path,
operand,
tag,
checking_presence,
} => AbstractValue::make_from(
Expression::UnknownTagCheck {
path: path.refine_parameters(arguments, fresh),
tag: *tag,
checking_presence: *checking_presence,
},
1,
} => AbstractValue::make_tag_check(
operand.refine_parameters(arguments, fresh),
*tag,
*checking_presence,
),
Expression::Variable { path, var_type } => {
let refined_path = path.refine_parameters(arguments, fresh);
Expand Down Expand Up @@ -3496,7 +3504,15 @@ impl AbstractValueTrait for Rc<AbstractValue> {
path.clone(),
),
Expression::UnknownModelField { .. } => self.clone(),
Expression::UnknownTagCheck { .. } => self.clone(),
Expression::UnknownTagCheck {
operand,
tag,
checking_presence,
} => AbstractValue::make_tag_check(
operand.refine_with(path_condition, depth + 1),
*tag,
*checking_presence,
),
Expression::Variable { var_type, .. } => {
if *var_type == ExpressionType::Bool {
if path_condition.implies(&self) {
Expand Down
123 changes: 44 additions & 79 deletions checker/src/body_visitor.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1863,107 +1863,72 @@ impl<'analysis, 'compilation, 'tcx, E> BodyVisitor<'analysis, 'compilation, 'tcx
block
}

/// Attach `tag` to the value located at `value_path`. The tag presence is indicated by a
/// path condition `cond`. The `value_path` may be pattern paths and need be expanded.
/// Attach `tag` to the value located at `value_path`. The `value_path` may be pattern paths
/// and need be expanded.
#[logfn_inputs(TRACE)]
pub fn attach_tag_to_elements(
&mut self,
tag: Tag,
cond: Rc<AbstractValue>,
value_path: Rc<Path>,
root_rustc_type: Ty<'tcx>,
) {
if let Some((join_condition, true_path, false_path)) =
self.current_environment.try_to_split(&value_path)
{
// The value path contains an abstract value that was constructed with a join.
// In this case, we split the path into two and perform weak updates on them.
// We also fall through to perform a strong update on the given value path.
self.attach_tag_to_elements(
tag,
cond.and(join_condition.clone()),
true_path,
root_rustc_type,
);
self.attach_tag_to_elements(
tag,
cond.and(join_condition.logical_not()),
false_path,
root_rustc_type,
);
} else {
// The value path contains an index/slice selector, e.g., arr[i]. If the index pattern is
// concrete, e.g. the index i is a constant, we need to expand it and then use a helper
// function to call attach_tag_to_elements recursively on each expansion.
let expanded_source_pattern = self.try_expand_source_pattern(
&value_path,
&value_path,
root_rustc_type,
|_self, _target_path, expanded_path, root_rustc_type| {
_self.attach_tag_to_elements(tag, cond.clone(), expanded_path, root_rustc_type);
},
);
if expanded_source_pattern {
return;
}
// The value path contains an index/slice selector, e.g., arr[i]. If the index pattern is
// concrete, e.g. the index i is a constant, we need to expand it and then use a helper
// function to call attach_tag_to_elements recursively on each expansion.
let expanded_source_pattern = self.try_expand_source_pattern(
&value_path,
&value_path,
root_rustc_type,
|_self, _target_path, expanded_path, root_rustc_type| {
_self.attach_tag_to_elements(tag, expanded_path, root_rustc_type);
},
);
if expanded_source_pattern {
return;
}

// Get here if value path is not a pattern, or it contains an abstract index/slice selector.
// Consider the case where the value path contains an abstract index/slice selector.
// If the index/slice selector is a compile-time constant, then we use a helper function
// to call attach_tag_to_elements recursively on each expansion.
// If not, all the paths that can match the pattern are weakly attached with the tag.
let expanded_target_pattern = self.try_expand_target_pattern(
&value_path,
&value_path,
root_rustc_type,
|_self, _target_path, expanded_path, root_rustc_type| {
_self.attach_tag_to_elements(tag, cond.clone(), expanded_path, root_rustc_type);
},
|_self, target_path, _source_path, index_value| {
_self.attach_tag_weakly(tag, cond.clone(), &target_path, |v| {
index_value.equals(v)
});
},
|_self, target_path, _source_path, count| {
_self.attach_tag_weakly(tag, cond.clone(), &target_path, |v| {
count.greater_than(v)
});
},
);
if expanded_target_pattern {
return;
}
// Get here if value path is not a pattern, or it contains an abstract index/slice selector.
// Consider the case where the value path contains an abstract index/slice selector.
// If the index/slice selector is a compile-time constant, then we use a helper function
// to call attach_tag_to_elements recursively on each expansion.
// If not, all the paths that can match the pattern are weakly attached with the tag.
let expanded_target_pattern = self.try_expand_target_pattern(
&value_path,
&value_path,
root_rustc_type,
|_self, _target_path, expanded_path, root_rustc_type| {
_self.attach_tag_to_elements(tag, expanded_path, root_rustc_type);
},
|_self, target_path, _source_path, index_value| {
_self.attach_tag_weakly(tag, &target_path, |v| index_value.equals(v));
},
|_self, target_path, _source_path, count| {
_self.attach_tag_weakly(tag, &target_path, |v| count.greater_than(v));
},
);
if expanded_target_pattern {
return;
}

// We have already handled paths with join or pattern.
// Now perform the actual tagging on value path, where the path condition `cond` indicates
// whether we should tag the value at value path or not.
// We have already handled paths with patterns. Now perform the actual tagging on value path.
self.non_patterned_copy_or_move_elements(
value_path.clone(),
value_path,
root_rustc_type,
false,
|_self, path, value| {
debug!("attaching {:?} to {:?} at {:?}", tag, value, path);
let tagged_value = cond.conditional_expression(value.add_tag(tag), value);
_self.current_environment.value_map = _self
_self
.current_environment
.value_map
.insert(path, tagged_value);
.update_value_at(path, value.add_tag(tag));
},
)
}

/// Attach `tag` to all index entries rooted at qualifier to reflect the possibility
/// that tagging an entry at an unknown index might also tag them. The tag presence is
/// indicated by a path condition `cond`.
fn attach_tag_weakly<F>(
&mut self,
tag: Tag,
cond: Rc<AbstractValue>,
qualifier: &Rc<Path>,
make_condition: F,
) where
/// that tagging an entry at an unknown index might also tag them.
fn attach_tag_weakly<F>(&mut self, tag: Tag, qualifier: &Rc<Path>, make_condition: F)
where
F: Fn(Rc<AbstractValue>) -> Rc<AbstractValue>,
{
let value_map = self.current_environment.value_map.clone();
Expand All @@ -1974,7 +1939,7 @@ impl<'analysis, 'compilation, 'tcx, E> BodyVisitor<'analysis, 'compilation, 'tcx
qualifier,
&mut subsequent_selectors,
) {
let join_condition = cond.and(make_condition(index_value.clone()));
let join_condition = make_condition(index_value.clone());
let new_value = join_condition
.conditional_expression(old_value.add_tag(tag), old_value.clone());
self.current_environment
Expand Down
32 changes: 8 additions & 24 deletions checker/src/call_visitor.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1037,12 +1037,9 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
}

// Augment the tags associated at the source with a new tag.
self.block_visitor.bv.attach_tag_to_elements(
tag,
abstract_value::TRUE.into(),
source_path,
source_rustc_type,
);
self.block_visitor
.bv
.attach_tag_to_elements(tag, source_path, source_rustc_type);
}

// Update exit conditions.
Expand Down Expand Up @@ -1123,24 +1120,11 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
.lookup_path_and_refine_result(source_path.clone(), source_rustc_type);

// Decide the result of has_tag! or does_not_have_tag!.
let check_value = if checking_presence {
source_value.has_tag(&tag)
} else {
source_value.does_not_have_tag(&tag)
};
if check_value.is_top() {
// Cannot decide tag presence/absence. Return an unknown tag check.
result = Some(AbstractValue::make_from(
Expression::UnknownTagCheck {
path: source_path,
tag,
checking_presence,
},
1,
));
} else {
result = Some(check_value);
}
result = Some(AbstractValue::make_tag_check(
source_value,
tag,
checking_presence,
));
} else {
result = None;
}
Expand Down
5 changes: 1 addition & 4 deletions checker/src/environment.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -98,10 +98,7 @@ impl Environment {
/// and alternate, respectively. These paths can then be weakly updated to reflect the
/// lack of precise knowledge at compile time.
#[logfn_inputs(TRACE)]
pub fn try_to_split(
&mut self,
path: &Rc<Path>,
) -> Option<(Rc<AbstractValue>, Rc<Path>, Rc<Path>)> {
fn try_to_split(&mut self, path: &Rc<Path>) -> Option<(Rc<AbstractValue>, Rc<Path>, Rc<Path>)> {
match &path.value {
PathEnum::Alias { value } => {
if let Expression::ConditionalExpression {
Expand Down
Loading

0 comments on commit f6c18ab

Please sign in to comment.