Function checkModuleCompatibility is a performance bottleneck

[brianhuffman]

Function checkModuleCompatibility is called by crucible_llvm_verify to check that each supplied override was proved using the same LLVM module.

saw-script/src/SAWScript/Crucible/LLVM/Builtins.hs

Lines 270 to 283 in 74ddfaf

	-- | Check that all the overrides/lemmas were actually from this module
	checkModuleCompatibility ::
	MonadFail m =>
	LLVMModule arch ->
	[SomeLLVM MS.CrucibleMethodSpecIR] ->
	m [MS.CrucibleMethodSpecIR (LLVM arch)]
	checkModuleCompatibility llvmModule = foldM step []
	where step accum (SomeLLVM lemma) =
	case testEquality (lemma ^. MS.csCodebase) llvmModule of
	Nothing -> fail $ unlines
	[ "Failed to apply an override that was verified against a"
	, "different LLVM module"
	]
	Just Refl -> pure (lemma:accum)

The problem is that it does a full structural comparison of the entire LLVM AST for every override, which can be expensive. Profiling shows that on some proof scripts, this can account for up to half of the total runtime of crucible_llvm_verify.

Instead of a full structural comparison, we should perhaps generate a unique ID for each LLVMModule value when the module is loaded, which we can then use for fast comparisons.

[robdockins]

Yikes! Yeah, a unique ID will catch the very common case of reusing the same module. If we hash the module, that would also provide an additional common case for distinct modules.

[robdockins]

The relevant code is below. Note that the ModuleTranslation test is already a fast Nonce comparison. That test is probably sufficient, actually.

data LLVMModule arch =
  LLVMModule
  { _modName :: String
  , _modAST :: L.Module
  , _modTrans :: CL.ModuleTranslation arch
  }

makeLenses ''LLVMModule

instance TestEquality LLVMModule where
  testEquality (LLVMModule nm1 lm1 mt1) (LLVMModule nm2 lm2 mt2) =
    case testEquality mt1 mt2 of
      Nothing -> Nothing
      r@(Just Refl) ->
        if nm1 == nm2 && lm1 == lm2
        then r
        else Nothing

[brianhuffman]

Yeah, I had noticed that the ModuleTranslation comparison was really fast. I was thinking that I should move a bit of code around so that we can make LLVMModule into an abstract datatype; we can provide functions to project the components, but there's really no reason to ever update any of the components of an LLVMModule value after it's created.