Add llvm_points_to_bitfield and enable_lax_loads_and_stores

[RyanGlScott]

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 Support structs with bitfields in Text.LLVM.DebugUtils 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 Bump llvm-pretty{-bc-parser} submodules, adapt to ValPoison 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 a 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.

[robdockins]

I haven't understood all of the details, but I think this looks good. I always appreciate comments and tests, so looks good there.

Couple of minor comments; otherwise looks good.

[andreistefanescu]

sorry for the late comments

[andreistefanescu]

this can be W4.bvSelect sym bfOffset_repr rhsWidth bfBV.

[RyanGlScott]

Ah, good suggestion. I've submitted #1547 to implement this.

[andreistefanescu]

I think this can be expressed more naturally in terms of bvConcat and bvSelect.

[robdockins]

I actually think the XOR formulation will be better, because the What4 AND/XOR semiring structure ought to mean that subsequent updates to the same field will cancel, and update to disjoint fields will commute, etc.

[RyanGlScott]

I don't have strong opinions on which approach is better per se, but I did try to implement your alternative approach in terms of bvConcat and bvSelect, and it wasn't entirely straightforward to do so. Unless I'm missing something, you have to have three cases:

1. The field occurs at the very LSBs of the bitfield. In that case, bvSelect the range from rhsWidth to bfWidth - rhsWidth, and then bvConcat that to the rhsBV.
2. The field occurs at the very MSBs of the bitfield. In that case, bvSelect the range from 0 to bfFieldOffset, and then bvConcat that to the rhsBV.
3. The field is in the middle of the bitfield, with other bits surrounding it on both sides. In that case, call bvSelect twice to obtain the surrounding bits, and then call bvConcat twice to concatenate these bitvectors to the rhsBV.

What's more, there's a fair bit of tiresome NatRepr manipulation needed to satisfy the inequalities demanded by bvSelect's type signature. I've implemented it locally, and it is possible to do so, but the resulting code is not much more natural to look at than it is currently.