crux: Shared implementation of crucible_assert

GaloisInc · Nov 27, 2023 · 96a4654 · 96a4654
1 parent c43e34d
commit 96a4654
Show file tree

Hide file tree

Showing 4 changed files with 30 additions and 10 deletions.
diff --git a/crucible-go/src/Lang/Crucible/Go/Overrides.hs b/crucible-go/src/Lang/Crucible/Go/Overrides.hs
@@ -106,9 +106,7 @@ do_assert args = C.ovrWithBackend $ \bak -> do
   let sym = backendGetSym bak
   (Empty :> _mgs :> _file :> C.RV b) <- pure args
   loc <- liftIO $ W4.getCurrentProgramLoc sym
-  liftIO $ addDurableAssertion bak (LabeledPred b
-                                    (C.SimError loc $ C.AssertFailureSimError
-                                     "assertion_failure" ""))
+  Crux.doCrucibleAssert "assertion_failure" b (plSourceLoc loc)
   return Ctx.empty
 
 go_overrides :: (IsSymInterface sym, 1 <= w)

diff --git a/crux-llvm/src/Crux/LLVM/Overrides.hs b/crux-llvm/src/Crux/LLVM/Overrides.hs
@@ -21,6 +21,7 @@ module Crux.LLVM.Overrides
 
 import qualified Data.ByteString as BS
 import qualified Data.ByteString.Char8 as BS8
+import qualified Data.Text as Text
 import Control.Monad (when)
 import Control.Monad.IO.Class(liftIO)
 import GHC.Exts ( Proxy# )
@@ -481,11 +482,8 @@ do_assert arch mvar bak (Empty :> p :> pFile :> line) =
      l <- case asBV (regValue line) of
             Just (BV.BV l)  -> return (fromInteger l)
             Nothing -> return 0
-     let pos = SourcePos (T.pack file) l 0
-     loc <- liftIO $ getCurrentProgramLoc sym
-     let loc' = loc{ plSourceLoc = pos }
-     let msg = GenericSimError "crucible_assert"
-     liftIO $ addDurableAssertion bak (LabeledPred cond (SimError loc' msg))
+     let loc = SourcePos (Text.pack file) l 0
+     Crux.doCrucibleAssert "crucible_assert" cond loc
 
 do_print_uint32 ::
   (IsSymBackend sym bak) =>

diff --git a/crux-mir/src/Mir/Overrides.hs b/crux-mir/src/Mir/Overrides.hs
@@ -42,6 +42,7 @@ import What4.Expr.GroundEval (GroundValue, GroundEvalFn(..), GroundArray(..))
 import What4.FunctionName (FunctionName, functionNameFromText)
 import What4.Interface
 import What4.Partial (PartExpr, pattern PE, pattern Unassigned)
+import qualified What4.ProgramLoc as W4
 import What4.Protocol.Online ( checkWithAssumptionsAndModel )
 import What4.SatResult (SatResult(..))
 
@@ -508,9 +509,10 @@ bindFn _symOnline _cs fn cfg =
                                (BV.asUnsigned <$> asBV (unRV lineArg))
                        col <- maybe (fail "not a constant column number") pure $
                               (BV.asUnsigned <$> asBV (unRV colArg))
+                       let loc = W4.SourcePos file (fromIntegral line) (fromIntegral col)
                        let locStr = Text.unpack file <> ":" <> show line <> ":" <> show col
-                       let reason = AssertFailureSimError ("MIR assertion at " <> locStr <> ":\n\t" <> src) ""
-                       liftIO $ assert bak (unRV c) reason
+                       let msg = "MIR assertion at " <> locStr <> ":\n\t" <> src
+                       Crux.doCrucibleAssert msg (unRV c) loc
                        return ()
                , let argTys = (Empty :> BoolRepr :> strrepr :> strrepr :> u32repr :> u32repr)
                  in override ["crucible", "crucible_assume_impl"] argTys UnitRepr $

diff --git a/crux/src/Crux/Overrides.hs b/crux/src/Crux/Overrides.hs
@@ -8,15 +8,18 @@ module Crux.Overrides
   , mkFreshFloat
   , baseFreshOverride
   , baseFreshOverride'
+  , doCrucibleAssert
   ) where
 
 import qualified Data.Parameterized.Context as Ctx
 
 import What4.BaseTypes (BaseTypeRepr)
 import qualified What4.Interface as W4
 import qualified What4.InterpretedFloatingPoint as W4
+import qualified What4.ProgramLoc as W4
 
 import qualified Lang.Crucible.Backend as C
+import qualified Lang.Crucible.Simulator.SimError as C
 import qualified Lang.Crucible.Simulator.RegValue as C
 import qualified Lang.Crucible.Types as C
 import qualified Lang.Crucible.Simulator.OverrideSim as C
@@ -88,3 +91,22 @@ baseFreshOverride' nm bty =
   , C.typedOverrideArgs = Ctx.Empty
   , C.typedOverrideRet = C.baseToType bty
   }
+
+-- | Shared implementation of @crucible_assert@ override
+--
+-- Used in Go, LLVM, and MIR frontends.
+doCrucibleAssert ::
+  -- | Assertion failure message
+  String ->
+  -- | Condition to assert
+  W4.Pred sym ->
+  -- | Source position
+  W4.Position ->
+  C.OverrideSim p sym ext r args ret ()
+doCrucibleAssert msg cond pos =
+  C.ovrWithBackend $ \bak ->
+    do let sym = C.backendGetSym bak
+       loc <- liftIO $ W4.getCurrentProgramLoc sym
+       let loc' = loc { W4.plSourceLoc = pos }
+       let reason = C.AssertFailureSimError msg ""
+       liftIO $ C.addDurableAssertion bak (C.LabeledPred cond (C.SimError loc' reason))