Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Simple constant folding for bounds upper offsets #1095

Closed
secure-sw-dev-bot opened this issue Jan 17, 2022 · 0 comments
Closed

Simple constant folding for bounds upper offsets #1095

secure-sw-dev-bot opened this issue Jan 17, 2022 · 0 comments

Comments

@secure-sw-dev-bot
Copy link

This issue was copied from microsoft/checkedc-clang#1095


This PR introduces a temporary solution for an issue with bounds validation: the bounds checker should be able to prove that bounds(p, p + ((len + 1) - 1)) imply bounds(p, p + len).

The solution involves performing constant folding for a limited set of expressions. If the upper offset of a range is of the form (e +/- a) +/ b, where a and b are integer constants and e is an expression, we extract the variable part as e and the constant part as a + b (or a + -b, -a + b, or -a + -b).

This is intended to be a temporary fix until we can solve issues with constant folding, commutativity, and associativity in bounds expressions in a more general way.

This fix addresses +1/-1 situations that can arise from passing arguments to functions with declared parameter bounds (see checkedc/450). However, it does not fix +1/-1 situations that can occur as a result of bounds widening, e.g.

void f(_Nt_array_ptr<char> p : count(len), unsigned int len) {
  if (*(p + len)) {
    ++len;
  }
}

The bounds checker is unable to create a base range for the inferred bounds bounds(p, (p + (len - 1)) + 1). We need further work to address associativity issues with bounds expressions.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant