Respond to review comments

crucible-go/src/Lang/Crucible/Go/Simulate.hs

@@ -107,7 +107,7 @@ mkFunctionBindings overrides ((ident, AnyCFG cfg) : cfgs) =
         Just (SomeOverride _pkg fnm o@(C.TypedOverride override argsRepr retRepr)) ->
           case (testEquality (cfgArgTypes cfg) argsRepr,
                 testEquality (cfgReturnType cfg) retRepr) of
-            (Just Refl, Just Refl) -> UseOverride (C.mkTypedOverride fnm o)
+            (Just Refl, Just Refl) -> UseOverride (C.runTypedOverride fnm o)
             _ -> panic "[Go simulator] mkFunctionBindings"
                  [ "Type mismatch for override of " ++ show ident
                  , "  Expected: " ++ show (cfgArgTypes cfg) ++ " -> " ++ show (cfgReturnType cfg)

crucible/src/Lang/Crucible/Simulator/OverrideSim.hs

@@ -75,7 +75,7 @@ module Lang.Crucible.Simulator.OverrideSim
     -- * Typed overrides
   , TypedOverride(..)
   , SomeTypedOverride(..)
-  , mkTypedOverride
+  , runTypedOverride
     -- * Re-exports
   , Lang.Crucible.Simulator.ExecutionTree.Override
   ) where
@@ -683,14 +683,16 @@ data TypedOverride p sym ext args ret
     , typedOverrideRet :: TypeRepr ret
     }
 
+-- | A 'TypedOverride' with the type parameters @args@, @ret@ existentially
+-- quantified
 data SomeTypedOverride p sym ext =
   forall args ret. SomeTypedOverride (TypedOverride p sym ext args ret)
 
 -- | Create an override from a 'TypedOverride'.
-mkTypedOverride ::
+runTypedOverride ::
   FunctionName ->
   TypedOverride p sym ext args ret ->
   Override p sym ext args ret
-mkTypedOverride nm typedOvr = mkOverride' nm (typedOverrideRet typedOvr) $ do
+runTypedOverride nm typedOvr = mkOverride' nm (typedOverrideRet typedOvr) $ do
   RegMap args <- getOverrideArgs
   typedOverrideHandler typedOvr (fmapFC (RV . regValue) args)

crux-mir/src/Mir/Overrides.hs

@@ -399,7 +399,7 @@ bindFn symOnline cs name cfg
   , UsizeArrayRepr btpr <- cfgReturnType cfg
   , Just Refl <- testEquality w (knownNat @8)
   = bindFnHandle (cfgHandle cfg) $ UseOverride $
-    mkTypedOverride "array::symbolic" (array_symbolic btpr)
+    runTypedOverride "array::symbolic" (array_symbolic btpr)
 
   | hasInstPrefix ["crucible", "concretize"] explodedName
   , Empty :> tpr <- cfgArgTypes cfg
@@ -448,7 +448,7 @@ bindFn _symOnline _cs fn cfg =
                            ".\n\tExpected (" ++ show (cfgArgTypes cfg) ++ ") → " ++ show (cfgReturnType cfg) ++
                            "\n\tbut got (" ++ show argTys ++ ") → (" ++ show retTy ++ ")."
         Just (Refl, Refl) ->
-          bindFnHandle (cfgHandle cfg) $ UseOverride (mkTypedOverride (functionNameFromText fn) o)
+          bindFnHandle (cfgHandle cfg) $ UseOverride (runTypedOverride (functionNameFromText fn) o)
 
   where
     override ::

crux/src/Crux/Overrides.hs

@@ -24,6 +24,7 @@ import qualified Lang.Crucible.Simulator.OverrideSim as C
 import Crux.Types (OverM)
 import Control.Monad.IO.Class (liftIO)
 
+-- | Create a fresh constant ('W4.freshConstant') with the given base type
 mkFresh ::
   C.IsSymInterface sym =>
   W4.SolverSymbol ->
@@ -38,6 +39,7 @@ mkFresh name ty =
        liftIO $ C.addAssumptions bak (C.singleEvent ev)
        return elt
 
+-- | Create a fresh float constant ('W4.freshFloatConstant')
 mkFreshFloat ::
   C.IsSymInterface sym =>
   W4.SolverSymbol ->
@@ -71,9 +73,9 @@ baseFreshOverride bty sty getStr =
   , C.typedOverrideRet = C.baseToType bty
   }
 
--- | Build an override that takes no arguments and returns a fresh constant a
--- given name. Generally, frontends should prefer 'baseFreshOverride', to allow
--- users to specify variable names.
+-- | Build an override that takes no arguments and returns a fresh
+-- constant that uses the given name. Generally, frontends should prefer
+-- 'baseFreshOverride', to allow users to specify variable names.
 baseFreshOverride' :: 
   C.IsSymInterface sym =>
   -- | Variable name