You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Currently the block component of a Crucible/LLVM pointer consists of an expression of type Nat. The problem is that this is a type with too many operations: For example we should never have a pointer whose block ID is an expression involving natural number addition or multiplication.
The only operations that we need on Crucible/LLVM block IDs are literals, muxes, and equality comparisons. If we represent block IDs with a type that supports only these operations, then it may be possible to implement some other pointer operations or memory model operations more efficiently, because each operation would always be able to view a symbolic block ID as a mux tree of literals.
The text was updated successfully, but these errors were encountered:
Currently the block component of a Crucible/LLVM pointer consists of an expression of type
Nat
. The problem is that this is a type with too many operations: For example we should never have a pointer whose block ID is an expression involving natural number addition or multiplication.The only operations that we need on Crucible/LLVM block IDs are literals, muxes, and equality comparisons. If we represent block IDs with a type that supports only these operations, then it may be possible to implement some other pointer operations or memory model operations more efficiently, because each operation would always be able to view a symbolic block ID as a mux tree of literals.
The text was updated successfully, but these errors were encountered: