search

GaloisInc / crucible

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

crucible-syntax: Remove `ACFG` #1149

Closed langston-barrett closed 9 months ago

langston-barrett commented 9 months ago

This type is redundant:

https://github.com/GaloisInc/crucible/blob/a8839cda3f1570ff921237ce48606a006cd26e0a/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs#L1928-L1933

It stores types for the arguments and return value of the underlying CFG, but these are available via the CFG's handle.

RyanGlScott commented 9 months ago

Ugh, good catch. Sadly, this is a somewhat common pattern in the crucible-syntax. I did my best to expunge things of this sort in #1053, but this slipped through the cracks.

RyanGlScott commented 9 months ago

But come to think of it, ACFG also existentially closes over the init and ret type variables, so perhaps it is still serving a useful purpose in that regard. Or is there another data type that already does this? (SomeCFG existentially closes over s only, so it wouldn't do.)

RyanGlScott commented 9 months ago

Ah, this exists today as AnyCFG:

https://github.com/GaloisInc/crucible/blob/a8839cda3f1570ff921237ce48606a006cd26e0a/crucible/src/Lang/Crucible/CFG/Core.hs#L827-L829

At least, it's very close—it doesn't existentially close over an IsSyntaxExtension ext constraint. But it's unclear to me if that is actually necessary.

langston-barrett commented 9 months ago

Ah, this exists today as AnyCFG:

Yeah, there's no version of this for registerized CFGs, but there's no reason why there shouldn't be. I'll create it and remove ACFG in favor of it.