GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs
628 stars 42 forks source link

Typed overrides #1136

Closed langston-barrett closed 9 months ago

langston-barrett commented 9 months ago

Fixes #1135.

langston-barrett commented 9 months ago

It looks like most of these changes involve the internals of libraries, or the APIs of libraries that aren't widely depended on. Is that right?

Yep, that's right.

My first inclination was to question if we should change LLVMOverride to be defined in terms of a TypedOverride, but that would of course result in a breaking API change (and one that would likely matter in practice).

Indeed, and there are two other complications here:

  1. LLVMOverride also contains an LLVM declaration, so we can't simply replace it with TypedOverride (though after #1138 we might be able to)
  2. The LLVM override implementation (action in OverrideSim) additionally takes a GlobalVar Mem parameter.
langston-barrett commented 9 months ago

Fair enough. But do we really need to replace all of LLVMOverride with TypedOverride? I could imagine something like this:

Agreed that this would be possible, and that it's probably preferable to delay this until we fix #1138.

This doesn't worry me that much, since I imagine that we could simply create closures that close over the GlobalVar Mem argument when constructing LLVM TypedOverrides. Alternatively, if that proves too annoying, then we can always get and set the underlying MemImpl from within the override, similarly to how crucible-llvm does it here.

Yeah, the only downside to this approach is that we'd end up with functions GlobalVar Mem -> TypedOverride, which makes the type signature of the override inaccessible without a GlobalVar Mem, even though it doesn't really depend on it. Might not be a problem in practice.