Skip to content

Lower Bounds Inference #718

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

Merged
merged 118 commits into from
Dec 2, 2021
Merged

Lower Bounds Inference #718

merged 118 commits into from
Dec 2, 2021

Conversation

john-h-kastner
Copy link
Collaborator

@john-h-kastner john-h-kastner commented Sep 30, 2021

This pull requests extends array bounds inference to support inferring lower bounds for array pointers and inserting using Checked C range bounds.

For example:

char simple_lower_bound(int *a, int l) {
  int *b = a;
  while (b - a < l && *b != 42)
    b++;
  return b - a < l;
}

3C can now infer bounds for b even though a standard count bound would be invalidated by the increment b++.

char simple_lower_bound(_Array_ptr<int> a : count(l), int l) {
  _Array_ptr<int> b : bounds(a, a + l) = a;
  while (b - a < l && *b != 42)
    b++;
  return b - a < l;
}

These bounds are supported even when there is no existing pointer that can be used the as lower bound.

For example:

char introduce_lower_bound(int *a, int l) {
  while (*a != 42) {
    a++;
  }
  return *a == 42;
}

3C will generate a fresh lower bound pointer for a, so that it can use the heuristically inferred length.

char introduce_lower_bound(_Array_ptr<int> __3c_tmp_a : count(l), int l) {
_Array_ptr<int> a : bounds(__3c_tmp_a, __3c_tmp_a + l) = __3c_tmp_a;

  while (*a != 42) {
    a++;
  }
  return *a == 42;
}

Actions Run

The failures on libarchive, libtiff, and lua are expected. The lua failure should be fixed; libarchive is a compiler bug; libtiff needs investigation. (libarchive is actually passing on the run, but previous tests have encountered an intermittent core dump caused by uninitialized memory somewhere in the Checked C bounds widening code).

@john-h-kastner john-h-kastner marked this pull request as draft September 30, 2021 16:46
@mattmccutchen-cci mattmccutchen-cci added the delay code style pass PRs big enough that a code style pass on `main` should be delayed to reduce conflicts. label Sep 30, 2021
john-h-kastner and others added 7 commits November 30, 2021 22:34
Co-authored-by: Matt McCutchen (Correct Computation) <[email protected]>
Co-authored-by: Matt McCutchen (Correct Computation) <[email protected]>
Co-authored-by: Matt McCutchen (Correct Computation) <[email protected]>
Co-authored-by: Matt McCutchen (Correct Computation) <[email protected]>
Co-authored-by: Matt McCutchen (Correct Computation) <[email protected]>
Co-authored-by: Matt McCutchen (Correct Computation) <[email protected]>
This could cause a compile error if the rest of the function assumed the
variable could be used at the solved checked type of the internal
PVConstraint.

This forced me to factor out the duplicate code related to supplementary
decls from DeclRewriter::build{Itype,Checked}Decl as I had proposed.
@john-h-kastner
Copy link
Collaborator Author

A couple of tests had significant changes. For example, realloc.c had a count change from 4 to 2.

I've added realloc to the allocater heuristics. This gives better bounds in the realloc.c and realloc_complex.c tests, but drops a bound in basic.c. The bound is dropped because treating using realloc as a heuristic to seed bounds caused a conflict with the prior bound inferred from a malloc. Based on this conflict the array bound inference code decides not to infer any bound.

77905e6

…ge bounds

Range bounds should be used when talking about the `bounds(lb, up)`
bounds expression. When talking about inserting new lower bounds into
the source code, use "fresh lower bound".
Lower bounds inference was not functioning properly when a function
declaration containing a paramter that was rewriten using a fresh lower
bound was coppied into the working directory at the start of phase two.
The paramter apears in the header with a count bound, but the fresh
lower bound does not appear in the function body because the source
file hasn't been coppied yet.

This is a hack. A better solution for this problem should be found.
@john-h-kastner john-h-kastner merged commit 79804ee into main Dec 2, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
delay code style pass PRs big enough that a code style pass on `main` should be delayed to reduce conflicts.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants