GaloisInc / crucible

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

`muxHandle` is wrong #1206

Open langston-barrett opened 2 months ago

langston-barrett commented 2 months ago

Crucible doesn't really support muxing function handles, but it does have this muxHandle operation:

https://github.com/GaloisInc/crucible/blob/3ed848aee186f63a543ccebf334e3b62b38400e7/crucible/src/Lang/Crucible/Simulator/RegValue.hs#L269-L277

This is plainly wrong, as it just returns the first FnVal in the case that the predicate isn't statically known. It should probably panic instead. This code is also reachable via this CanMux instance:

https://github.com/GaloisInc/crucible/blob/3ed848aee186f63a543ccebf334e3b62b38400e7/crucible/src/Lang/Crucible/Simulator/RegValue.hs#L279-L282

Both of these are exported.

I'd advocate for:

However, all of these except the first are breaking changes.