-
Notifications
You must be signed in to change notification settings - Fork 128
Description
While auditing the code in Cryptol.IR.FreeVars recently, @yav and I noticed a bug in the FreeVars Type instance involving TNominal (i.e., newtypes and enums):
cryptol/src/Cryptol/IR/FreeVars.hs
Line 162 in 9821aa9
| TNominal nt ts -> freeVars nt <> freeVars ts |
There are two things wrong here:
- This collects the free variables of
nt(aNominalType), but theFreeVars NominalTypedoes not return the name of the nominal type (intentionally so). As such, if you hadnewtype N = { x : Bit }, thenfreeVars Nwould not includeN, which is a pretty serious bug. - Less seriously, the code here overapproximates the set of free variables by collecting all of the free variables from the definition of
nt. For example,freeVars Nwill includeBitbecause theFreeVars NominalTypeinstance includes the free variables ofN's fields, even though the typeNdoesn't directly mentionBit.
To fix both of these issues, we should modify the instance so that it only includes ntName nt (but no other parts of nt) in the Deps that this returns.
In practice, these issues are unlikely to cause anything bad to happen within Cryptol itself. This is because the FreeVars instances are primarily used for sorting declarations in dependency order, but we only sort top-level functions, not nominal type declarations. Still, it would be good to fix this so that Cryptol API users could sort nominal type declarations in dependency order if they wanted to.