crucible-llvm: Generalize LLVMOverride's ext parameter

[langston-barrett]

Previously, the OverrideSim action for an LLVMOverride was assumed to have a fixed ext parameter, namely, LLVM. While this is intuitively appealing, it turns out not to be necessary. This is because there are only a few operations in the OverrideSim monad that make essential use of the ext parameter, such as registering or calling a CFG in the given language extension. These operations are unlikely to be used when defining, e.g., overrides for libc functions.

The motivation for generalizing the parameter is to enable the reuse of LLVMOverrides in other Crucible language extensions that make use of the LLVM memory model, namely, Macaw.

[langston-barrett]

Ah, whoops, this breaks something in UC-Crux.

[langston-barrett]

Indeed, UC-Crux does actually create LLVMOverrides that use callCFG to call LLVM CFGs. The way I see it, there are two paths forward:

• Make ext a type parameter of LLVMOverride. Then the overrides in Crucible-LLVM would be polymorphic over ext, while the ones in UC-Crux would fix ext to LLVM. This is the most flexible solution, as it allows each override to choose a particular extension if it needs it, or not if not.
• Tear this functionality out of UC-Crux. As UC-Crux is not very useful since the introduction of opaque pointers and is unlikely to be modified to be so (see Support opaque pointers in crucible-llvm and uc-crux-llvm #1075), and the "check" overrides in question aren't a core part of its functionality, this is also fairly appealing.

@RyanGlScott any thoughts?

[RyanGlScott]

I am fine with either option, but option (1) sounds slightly more appealing since we want to make LLVMOverride more like TypedOverride anyway (#1138), and TypedOverride is already parameterized by ext.

[kquick]

I'd also vote for option 1: I think it's probably too early to give up on uc-crux-llvm's potential.

[RyanGlScott]

Thanks! It would be worth advertising this change in the crucible-llvm changelog, as this change will impact saw-script. Otherwise, LGTM.