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.

Sign up for GitHub

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

Jump to bottom

Add llvm_points_to_bitfield and enable_lax_loads_and_stores #1539

Merged
merged 3 commits into from
Dec 22, 2021
Merged

Add llvm_points_to_bitfield and enable_lax_loads_and_stores #1539

merged 3 commits into from
Dec 22, 2021

Commits on Dec 21, 2021

  1. Add llvm_points_to_bitfield and enable_lax_loads_and_stores 

    This adds support for writing specifications that talk about bitfields in LLVM
code by way of the new `llvm_points_to_bitfield` command. Broadly speaking,
`llvm_points_to_bitfield ptr fieldName rhs` is like
`llvm_points_to (llvm_field ptr fieldName) rhs`, except that `fieldName` is
required to be the name of a field within a bitfield. The salient details are:

* LLVM bitcode itself does not a built-in concept of bitfields, but LLVM's
  debug metadata does. Support for retrieving bitfield-related metadata was
  added to `llvm-pretty` in GaloisInc/llvm-pretty#90, so this patch bumps the
  `llvm-pretty` submodule to incorporate it. This patch also updates the
  `crucible` submodule to incorporate corresponding changes in
  GaloisInc/crucible#936.

* The `LLVMPointsTo` data type now has a new `LLVMPointsToBitfield` data
  constructor that stores all of the necessary information related to the
  `llvm_points_to_bitfield` command. As a result, the changes in this patch
  are fairly insulated from the rest of SAW, as most of the new code involves
  adding additional cases to handle `LLVMPointsToBitfield`.

* Two of the key new functions are `storePointsToBitfieldValue` and
  `matchPointsToBitfieldValue`, which implement the behavior of
  `llvm_points_to_bitfield` in pre- and post-conditions. These functions
  implement the necessary bit-twiddling to store values in and retrieve values
  out of bitfield. I have left extensive comments in each function describing
  how all of this works.

* Accompanying `llvm_points_to_bitfield` is a new set of
  `{enable,disable}_lax_loads_and_stores` command, which toggles the
  Crucible-side option of the same name. When `enable_lax_loads_and_stores` is
  on, reading from uninitialized memory will return a symbolic value rather
  than failing outright. This is essential to be able to deal with LLVM bitcode
  involving bitfields, as reading a field from a bitfield involves reading the
  entire bitfield at once, which may include parts of the struct that have not
  been initialized yet.

* There are various `test_bitfield_*` test cases under `intTests` to test
  examples of bitfield-related specifications that should and should not
  verify.

* I have also updated `saw-remote-api` and `saw-client` to handle bitfields as
  well, along with a Python-specific test case.

Fixes #1461.
    @RyanGlScott
    RyanGlScott committed Dec 21, 2021
    Configuration menu
    Copy the full SHA
    cbc97c0 View commit details
    Browse the repository at this point in the history

  2. Whitespace tweaks only

    @RyanGlScott
    RyanGlScott committed Dec 21, 2021
    Configuration menu
    Copy the full SHA
    98650f9 View commit details
    Browse the repository at this point in the history

  3. Reference #338 in the FIXMEs adjacent to uses of noAlignment

    @RyanGlScott
    RyanGlScott committed Dec 21, 2021
    Configuration menu
    Copy the full SHA
    cea4114 View commit details
    Browse the repository at this point in the history