GaloisInc / crucible

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

Improve concretization of sequences #1212

Closed langston-barrett closed 1 month ago

langston-barrett commented 1 month ago

Concretization of sequences currently uses ++, which is slow:

https://github.com/GaloisInc/crucible/blob/976a16e44668fdc81ea3d2327a79541da4762c04/crucible/src/Lang/Crucible/Concretize.hs#L297

We should switch the following case to use Seq:

https://github.com/GaloisInc/crucible/blob/976a16e44668fdc81ea3d2327a79541da4762c04/crucible/src/Lang/Crucible/Concretize.hs#L98

The same problem applies here:

https://github.com/GaloisInc/crucible/blob/976a16e44668fdc81ea3d2327a79541da4762c04/crucible/src/Lang/Crucible/Simulator/SymSequence.hs#L402

We should make that function use Seq as well. It's exported, but its name has a typo, so we should make the Seq version with the correctly-spelled name, and add a deprecation warning to the [] version with the incorrect name. We can then use this function in the implementation of concretization of sequences.