GaloisInc / crucible

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

crucible-llvm: Don't pass around the symbolic backend explicitly #1185

Closed langston-barrett closed 4 months ago

langston-barrett commented 4 months ago

Lang.Crucible.Simulator.OverrideSim.{getSymInterface,ovrWithBackend} can replace the explicit passing of bak. This should simplify some type signatures.

langston-barrett commented 4 months ago

@RyanGlScott @kquick Any thoughts on this direction? There's a lot of instances of this to fix up so I just want to get some early feedback before going through them all.

kquick commented 4 months ago

As it stands in this PR so-far, we are removing a call argument but re-constituting it from monadic state almost immediately. The type signatures are only slightly reduced. As presented, there doesn't seem to be a big advantage to this change; I do like the idea of minimizing dependencies of individual functions, but these functions seem to need this value anyhow, and there is perhaps a slight (miniscule? non-existent?) performance impact to retrieving the value from the monadic context.

Is there the potential for this to ripple upstream: could the llvmOvr TH operation drop the bak argument entirely rather than the splices just ignoring it? Could callers of these functions drop the bak argument, perhaps transitively over multiple ranks of caller levels? If you think these are potential advantages that could be realized along these lines then I am more enthusiastic about this change.

I'm mostly ambivalent at this point and I haven't taken a close look at the larger context (i.e. these opinions are based solely on the delta in this PR), so I may be missing the bigger perspective. I'm aligned with whichever direction you'd like to go on this PR.

RyanGlScott commented 4 months ago

I feel the same way as @kquick.

langston-barrett commented 4 months ago

Is there the potential for this to ripple upstream: could the llvmOvr TH operation drop the bak argument entirely rather than the splices just ignoring it? Could callers of these functions drop the bak argument, perhaps transitively over multiple ranks of caller levels? If you think these are potential advantages that could be realized along these lines then I am more enthusiastic about this change.

Yes, that was what I was thinking, we could go all the way up to llvmOverride_def not passing a bak into the OverrideSim action. llvmOverride_def itself just gets it from ovrWithBackend, so I think there shouldn't be any performance change. However, those changes would require dropping bak from all the individual call* functions first.

Thanks for the feedback!

langston-barrett commented 4 months ago

One more advantage is that removing the bak parameter from llvmOverride_def will bring LLVMOverride another step closer the more generic TypedOverride.

langston-barrett commented 4 months ago

Perhaps this shouldn't be a common pattern

I think it's likely not a great pattern. Compare to the extreme case, a function r -> Reader r a. If I read such a type signature, I think "What's the purpose of the r parameter? Is it overriding the environment in the Reader r? Is it meant to be identical to it?".

There are two counter-arguments:

  1. It's not worth the code churn (API changes, git diff changes, possibilities of errors being introduced with such a large number of changes)
  2. ovrWithBackend has an awkward API

I could also go both ways. I think the notion of possibly unifying LLVMOverride with TypedOverride pushes me a bit more towards making this change rather than leaving it. Also, while it might take a lot more churn to make this pattern more prevalent, we don't have to do it all at once, it could occur during other routine maintenance. I think a lot of people probably "learn" the pattern of passing sym/bak by reading existing Crucible code (I know I sure did), so it's a good start to have a substantial body of it use a more straightforward pattern.

I don't think anything in this PR merits closer scrutiny, it's all really straightforward.