GaloisInc / crucible

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

crucible-llvm: Generalize `LLVMOverride`'s `ext` parameter #1184

Closed langston-barrett closed 4 months ago

langston-barrett commented 4 months ago

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 commented 4 months ago

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

langston-barrett commented 4 months ago

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

@RyanGlScott any thoughts?

RyanGlScott commented 4 months ago

I am fine with either option, but option (1) sounds slightly more appealing since we want to make LLVMOverride more like TypedOverride anyway (https://github.com/GaloisInc/crucible/issues/1138), and TypedOverride is already parameterized by ext.

kquick commented 4 months ago

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