RyanGlScott
commented
3 years ago I was originally hopeful that this could be a one-module fix, but things are rarely that simple. My first inclination was to modify crucible's lookupAlias function, which is responsible for throwing the "Unknown type alias" error:
lookupAlias :: (?lc :: TypeContext, MonadError String m) => Ident -> m SymType
lookupAlias i =
case llvmAliasMap ?lc ^. at i of
Just stp -> return stp
Nothing -> throwError $ unwords ["Unknown type alias", show i]If looking up an Ident in the llvmAliasMap fails, then simply consult the llvmMetadataMap as a last resort... at least, that's what I thought at first. Unfortunately, as far as I can tell, LLVM's metadata doesn't provide you with enough information to faithfully construct an entire SymType out of it (e.g., it doesn't tell you a struct's packedness, or the padding of a struct's fields). As a result, we'll likely need to do the heavy lifting in saw-script's llvm_sizeof function:
If liftMemType fails to look up an alias type, then we could fall back to using the llvmMetadataMap. The problem is: how do we know if liftMemType fails specifically due to an unknown type alias? There are a number of different things that can cause liftMemType to fail, but simply matching on Left err doesn't distinguish between any of these different failure modes.
One possible way forward is to change the MonadError String m constraints used in lookupAlias (and elsewhere in crucible) to something like MonadError TypeContextException m, where:
-- | Describes what problem was encountered in a computation using a
-- 'TypeContext'.
data TypeContextException
= UnknownTypeAlias Ident
| NonMemTypeEncountered SymType
| NonRetTypeEncountered SymType
| SymTypeConversionErrors [Doc Void]
| TranslationError String
deriving Show
instance Exception TypeContextException where
displayException (UnknownTypeAlias i) = unwords ["Unknown type alias", show i]
displayException (NonMemTypeEncountered stp) = unlines ["Expected memory type", show stp]
displayException (NonRetTypeEncountered stp) = unlines ["Expected return type", show stp]
displayException (SymTypeConversionErrors edocs) = unlines (map show edocs)
displayException (TranslationError s) = sThen llvm_sizeof could match on Left (UnknownTypeAlias _) to distinguish it from other forms of failure. In the former case, we would look up the debugging info in llvmMetadataMap, and the latter case, we would simply propagate the error as llvm_sizeof currently does.
One annoying wrinkle: how exactly do we look up the relevant debugging info in llvmMetadataMap? I thought that llvm-pretty's guessAliasInfo function would be just the tool for the job, but the catch is that it returns an Info. Info has two issues:
Info'sStructureconstructor doesn't record its size, nor doesUnionnorArrInfo. I suppose we could change these constructors to store the size, but that feels a bit ad hoc. (Why not store all other fields ofDICompositeTypeas well?)- Even if we did decide to change
Infoto store the size, we'd only be able to do so for certain forms ofDICompositeTypes. Notably,Infodoesn't have a constructor that corresponds toenums.
There's enough of an impedance mismatch between Info and what I need that it would likely be easier just to cargo-cult what guessAliasInfo does, except making it return a DICompositeType instead of an Info. Either way, I'll need to change llvm-pretty, since I would need to make use of certain functions from Text.LLVM.DebugUtils that aren't currently exported.
robdockins
Consider the following example:
When
test.cis compiled without optimizations, the proof succeeds:If
test.cis compiled with-O2, however, the proof fails:This because with
-O2, LLVM will optimize away the alias information forfooin the compiled bitcode. Compare the bitcode for the-O0version, which contains%struct.foo = type { i32 }:To the bitcode for the
-O2version, which does not:Just because the bitcode is missing an alias doesn't mean we have to give up, however. The
-O2bitcode actually does contain the size ofstruct fooelsewhere in debugging information. See thesize: 32bit below:I propose that in the event that SAW cannot resolve an alias, it should consult the debugging information as a fallback. This isn't guaranteed to always succeed, since it's possible that LLVM might also optimize away the debugging information. But for many cases, the info is right there, so we might as well use it.