From 0061ee7200c1e845f56e6db4c50819ffb9f11f59 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Thu, 27 May 2021 14:45:47 -0700 Subject: [PATCH 01/34] crux-mir-comp: use HasModel instead of Model personality --- crux-mir-comp/src/Mir/Compositional.hs | 7 ++- .../src/Mir/Compositional/Builder.hs | 14 +++--- .../src/Mir/Compositional/Clobber.hs | 44 +++++++++---------- .../src/Mir/Compositional/Override.hs | 23 +++++----- deps/crucible | 2 +- 5 files changed, 45 insertions(+), 45 deletions(-) diff --git a/crux-mir-comp/src/Mir/Compositional.hs b/crux-mir-comp/src/Mir/Compositional.hs index 78f14a5333..3daeb4e6e6 100644 --- a/crux-mir-comp/src/Mir/Compositional.hs +++ b/crux-mir-comp/src/Mir/Compositional.hs @@ -20,7 +20,6 @@ import Lang.Crucible.Simulator import qualified What4.Expr.Builder as W4 import Crux -import Crux.Types import Mir.DefId import Mir.Generator (CollectionState) @@ -31,13 +30,13 @@ import Mir.Compositional.Clobber (clobberGlobalsOverride) compositionalOverrides :: - forall sym t st fs args ret blocks rtp a r . - (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) => + forall sym p t st fs args ret blocks rtp a r . + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => Maybe (SomeOnlineSolver sym) -> CollectionState -> Text -> CFG MIR blocks args ret -> - Maybe (OverrideSim (Model sym) sym MIR rtp a r ()) + Maybe (OverrideSim (p sym) sym MIR rtp a r ()) compositionalOverrides _symOnline cs name cfg | (normDefId "crucible::method_spec::raw::builder_new" <> "::_inst") `Text.isPrefixOf` name diff --git a/crux-mir-comp/src/Mir/Compositional/Builder.hs b/crux-mir-comp/src/Mir/Compositional/Builder.hs index db3e19517f..7e83af2fe6 100644 --- a/crux-mir-comp/src/Mir/Compositional/Builder.hs +++ b/crux-mir-comp/src/Mir/Compositional/Builder.hs @@ -47,7 +47,7 @@ import qualified Verifier.SAW.TypedTerm as SAW import qualified SAWScript.Crucible.Common.MethodSpec as MS -import Crux.Types (Model) +import Crux.Types (HasModel) import Mir.DefId import Mir.Generator (CollectionState, collection) @@ -172,14 +172,14 @@ instance (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) => -- MethodSpecBuilder implementation. This is the code that actually runs when -- Rust invokes `msb.add_arg(...)` or similar. -builderNew :: forall sym t st fs rtp. - (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) => +builderNew :: forall sym p t st fs rtp. + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => CollectionState -> -- | `DefId` of the `builder_new` monomorphization. Its `Instance` should -- have one type argument, which is the `TyFnDef` of the function that the -- spec applies to. DefId -> - OverrideSim (Model sym) sym MIR rtp + OverrideSim (p sym) sym MIR rtp EmptyCtx MethodSpecBuilderType (MethodSpecBuilder sym t) builderNew cs defId = do sym <- getSymInterface @@ -214,10 +214,10 @@ builderNew cs defId = do -- As a side effect, this clobbers any mutable memory reachable through the -- argument. For example, if `argRef` points to an `&mut i32`, the `i32` will -- be overwritten with a fresh symbolic variable. -addArg :: forall sym t st fs rtp args ret tp. - (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) => +addArg :: forall sym p t st fs rtp args ret tp. + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => TypeRepr tp -> MirReferenceMux sym tp -> MethodSpecBuilder sym t -> - OverrideSim (Model sym) sym MIR rtp args ret (MethodSpecBuilder sym t) + OverrideSim (p sym) sym MIR rtp args ret (MethodSpecBuilder sym t) addArg tpr argRef msb = execBuilderT msb $ do sym <- lift $ getSymInterface loc <- liftIO $ W4.getCurrentProgramLoc sym diff --git a/crux-mir-comp/src/Mir/Compositional/Clobber.hs b/crux-mir-comp/src/Mir/Compositional/Clobber.hs index 2b5d40d51b..b8707364c0 100644 --- a/crux-mir-comp/src/Mir/Compositional/Clobber.hs +++ b/crux-mir-comp/src/Mir/Compositional/Clobber.hs @@ -24,7 +24,7 @@ import Lang.Crucible.Simulator import Lang.Crucible.Types import qualified Crux.Model as Crux -import Crux.Types (Model) +import Crux.Types (HasModel(..)) import Mir.Generator (CollectionState, collection, staticMap, StaticVar(..)) import Mir.Intrinsics hiding (MethodSpec, MethodSpecBuilder) @@ -38,14 +38,14 @@ import Mir.Compositional.Convert -- Helper functions for generating clobbering PointsTos -- | Replace each primitive value within `rv` with a fresh symbolic variable. -clobberSymbolic :: forall sym t st fs tp rtp args ret. - (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasCallStack) => +clobberSymbolic :: forall sym p t st fs tp rtp args ret. + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p, HasCallStack) => sym -> ProgramLoc -> String -> TypeShape tp -> RegValue sym tp -> - OverrideSim (Model sym) sym MIR rtp args ret (RegValue sym tp) + OverrideSim (p sym) sym MIR rtp args ret (RegValue sym tp) clobberSymbolic sym loc nameStr shp rv = go shp rv where go :: forall tp. TypeShape tp -> RegValue sym tp -> - OverrideSim (Model sym) sym MIR rtp args ret (RegValue sym tp) + OverrideSim (p sym) sym MIR rtp args ret (RegValue sym tp) go (UnitShape _) () = return () go shp@(PrimShape _ _btpr) _rv = freshSymbolic sym loc nameStr shp go (ArrayShape _ _ shp) mirVec = case mirVec of @@ -63,7 +63,7 @@ clobberSymbolic sym loc nameStr shp rv = go shp rv go shp _rv = error $ "clobberSymbolic: " ++ show (shapeType shp) ++ " NYI" goField :: forall tp. FieldShape tp -> RegValue' sym tp -> - OverrideSim (Model sym) sym MIR rtp args ret (RegValue' sym tp) + OverrideSim (p sym) sym MIR rtp args ret (RegValue' sym tp) goField (ReqField shp) (RV rv) = RV <$> go shp rv goField (OptField shp) (RV rv) = do rv' <- liftIO $ readMaybeType sym "field" (shapeType shp) rv @@ -74,14 +74,14 @@ clobberSymbolic sym loc nameStr shp rv = go shp rv -- inside an `UnsafeCell` wrapper can still be modified even with only -- immutable (`&`) access. So this function modifies only the portions of `rv` -- that lie within an `UnsafeCell` and leaves the rest unchanged. -clobberImmutSymbolic :: forall sym t st fs tp rtp args ret. - (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasCallStack) => +clobberImmutSymbolic :: forall sym p t st fs tp rtp args ret. + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p, HasCallStack) => sym -> ProgramLoc -> String -> TypeShape tp -> RegValue sym tp -> - OverrideSim (Model sym) sym MIR rtp args ret (RegValue sym tp) + OverrideSim (p sym) sym MIR rtp args ret (RegValue sym tp) clobberImmutSymbolic sym loc nameStr shp rv = go shp rv where go :: forall tp. TypeShape tp -> RegValue sym tp -> - OverrideSim (Model sym) sym MIR rtp args ret (RegValue sym tp) + OverrideSim (p sym) sym MIR rtp args ret (RegValue sym tp) go (UnitShape _) () = return () -- If we reached a leaf value without entering an `UnsafeCell`, then -- there's nothing to change. @@ -105,7 +105,7 @@ clobberImmutSymbolic sym loc nameStr shp rv = go shp rv go (RefShape _ _ _tpr) rv = return rv goField :: forall tp. FieldShape tp -> RegValue' sym tp -> - OverrideSim (Model sym) sym MIR rtp args ret (RegValue' sym tp) + OverrideSim (p sym) sym MIR rtp args ret (RegValue' sym tp) goField (ReqField shp) (RV rv) = RV <$> go shp rv goField (OptField shp) (RV rv) = do rv' <- liftIO $ readMaybeType sym "field" (shapeType shp) rv @@ -113,19 +113,19 @@ clobberImmutSymbolic sym loc nameStr shp rv = go shp rv return $ RV $ W4.justPartExpr sym rv'' -- | Construct a fresh symbolic `RegValue` of type `tp`. -freshSymbolic :: forall sym t st fs tp rtp args ret. - (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasCallStack) => +freshSymbolic :: forall sym p t st fs tp rtp args ret. + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p, HasCallStack) => sym -> ProgramLoc -> String -> TypeShape tp -> - OverrideSim (Model sym) sym MIR rtp args ret (RegValue sym tp) + OverrideSim (p sym) sym MIR rtp args ret (RegValue sym tp) freshSymbolic sym loc nameStr shp = go shp where go :: forall tp. TypeShape tp -> - OverrideSim (Model sym) sym MIR rtp args ret (RegValue sym tp) + OverrideSim (p sym) sym MIR rtp args ret (RegValue sym tp) go (UnitShape _) = return () go (PrimShape _ btpr) = do let nameSymbol = W4.safeSymbol nameStr expr <- liftIO $ W4.freshConstant sym nameSymbol btpr - stateContext . cruciblePersonality %= Crux.addVar loc nameStr btpr expr + stateContext . cruciblePersonality . personalityModel %= Crux.addVar loc nameStr btpr expr return expr go (ArrayShape (M.TyArray _ len) _ shp) = MirVector_Vector <$> V.replicateM len (go shp) @@ -150,10 +150,10 @@ freshSymbolic sym loc nameStr shp = go shp -- invalid ref value is not enough, since the function we're approximating -- might write through the old ref before replacing it with a new one. -clobberGlobals :: forall sym t st fs rtp args ret. - (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasCallStack) => +clobberGlobals :: forall sym p t st fs rtp args ret. + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p, HasCallStack) => sym -> ProgramLoc -> String -> CollectionState -> - OverrideSim (Model sym) sym MIR rtp args ret () + OverrideSim (p sym) sym MIR rtp args ret () clobberGlobals sym loc nameStr cs = do forM_ (Map.toList $ cs ^. staticMap) $ \(defId, StaticVar gv) -> do let static = case cs ^? collection . M.statics . ix defId of @@ -168,10 +168,10 @@ clobberGlobals sym loc nameStr cs = do rv' <- clobber shp rv writeGlobal gv rv' -clobberGlobalsOverride :: forall sym t st fs rtp args ret. - (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasCallStack) => +clobberGlobalsOverride :: forall sym p t st fs rtp args ret. + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p, HasCallStack) => CollectionState -> - OverrideSim (Model sym) sym MIR rtp args ret () + OverrideSim (p sym) sym MIR rtp args ret () clobberGlobalsOverride cs = do sym <- getSymInterface loc <- liftIO $ W4.getCurrentProgramLoc sym diff --git a/crux-mir-comp/src/Mir/Compositional/Override.hs b/crux-mir-comp/src/Mir/Compositional/Override.hs index 4a2bb5b95f..9ef900aff6 100644 --- a/crux-mir-comp/src/Mir/Compositional/Override.hs +++ b/crux-mir-comp/src/Mir/Compositional/Override.hs @@ -59,7 +59,7 @@ import qualified SAWScript.Crucible.Common.MethodSpec as MS import qualified SAWScript.Crucible.Common.Override as MS import qualified Crux.Model as Crux -import Crux.Types (Model) +import Crux.Types (HasModel(..)) import Mir.Generator import Mir.Intrinsics hiding (MethodSpec) @@ -70,8 +70,9 @@ import Mir.Compositional.Convert import Mir.Compositional.MethodSpec -type MirOverrideMatcher sym a = forall rorw rtp args ret. - MS.OverrideMatcher' sym MIR rorw (OverrideSim (Model sym) sym MIR rtp args ret) a +type MirOverrideMatcher sym a = forall p rorw rtp args ret. + HasModel p => + MS.OverrideMatcher' sym MIR rorw (OverrideSim (p sym) sym MIR rtp args ret) a data MethodSpec = MethodSpec { _msCollectionState :: CollectionState @@ -88,9 +89,9 @@ instance (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) => MethodSpecImpl sy -- | Pretty-print a MethodSpec. This wraps `ppMethodSpec` and returns the -- result as a Rust string. printSpec :: - (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) => + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => MethodSpec -> - OverrideSim (Model sym) sym MIR rtp args ret (RegValue sym (MirSlice (BVType 8))) + OverrideSim (p sym) sym MIR rtp args ret (RegValue sym (MirSlice (BVType 8))) printSpec ms = do let str = show $ MS.ppMethodSpec (ms ^. msSpec) let bytes = Text.encodeUtf8 $ Text.pack str @@ -111,9 +112,9 @@ printSpec ms = do -- the current test, calls to the subject function will be replaced with -- `runSpec`. enable :: - (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) => + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => MethodSpec -> - OverrideSim (Model sym) sym MIR rtp args ret () + OverrideSim (p sym) sym MIR rtp args ret () enable ms = do let funcName = ms ^. msSpec . MS.csMethod MirHandle _name _sig mh <- case cs ^? handleMap . ix funcName of @@ -130,10 +131,10 @@ enable ms = do -- | "Run" a MethodSpec: assert its preconditions, create fresh symbolic -- variables for its outputs, and assert its postconditions. -runSpec :: forall sym t st fs args ret rtp. - (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) => +runSpec :: forall sym p t st fs args ret rtp. + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => CollectionState -> FnHandle args ret -> MIRMethodSpec -> - OverrideSim (Model sym) sym MIR rtp args ret (RegValue sym ret) + OverrideSim (p sym) sym MIR rtp args ret (RegValue sym ret) runSpec cs mh ms = do let col = cs ^. collection sym <- getSymInterface @@ -189,7 +190,7 @@ runSpec cs mh ms = do let nameSymbol = W4.safeSymbol nameStr Some btpr <- liftIO $ termToType sym sc (SAW.ecType ec) expr <- liftIO $ W4.freshConstant sym nameSymbol btpr - stateContext . cruciblePersonality %= Crux.addVar loc nameStr btpr expr + stateContext . cruciblePersonality . personalityModel %= Crux.addVar loc nameStr btpr expr term <- liftIO $ eval expr return (SAW.ecVarIndex ec, term) diff --git a/deps/crucible b/deps/crucible index 31e3976444..0e855576df 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 31e397644411598b1fee7f6145ef9bf9d46a438f +Subproject commit 0e855576dfeb5c783a4d412c1318b1fc14be3400 From 7bf9d60719b2f1bbbfc3273df320ce5fbe587bd2 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Thu, 15 Apr 2021 10:04:02 -0700 Subject: [PATCH 02/34] [wip] initial cryptol::load implementation --- crux-mir-comp/crux-mir-comp.cabal | 1 + crux-mir-comp/exe/Main.hs | 15 ++- crux-mir-comp/src/Mir/Cryptol.hs | 157 ++++++++++++++++++++++++++++++ deps/crucible | 2 +- 4 files changed, 172 insertions(+), 3 deletions(-) create mode 100644 crux-mir-comp/src/Mir/Cryptol.hs diff --git a/crux-mir-comp/crux-mir-comp.cabal b/crux-mir-comp/crux-mir-comp.cabal index 26b47f6e19..607486e440 100644 --- a/crux-mir-comp/crux-mir-comp.cabal +++ b/crux-mir-comp/crux-mir-comp.cabal @@ -51,6 +51,7 @@ library Mir.Compositional.Convert Mir.Compositional.MethodSpec Mir.Compositional.Override + Mir.Cryptol ghc-options: -Wall -Wno-name-shadowing diff --git a/crux-mir-comp/exe/Main.hs b/crux-mir-comp/exe/Main.hs index 8b1d241f05..f1973600fd 100644 --- a/crux-mir-comp/exe/Main.hs +++ b/crux-mir-comp/exe/Main.hs @@ -1,7 +1,18 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE RankNTypes #-} module Main(main) where import qualified Mir.Language as Mir -import qualified Mir.Compositional as Mir +import Mir.Compositional (compositionalOverrides) +import Mir.Cryptol (cryptolOverrides) main :: IO () -main = Mir.mainWithExtraOverrides Mir.compositionalOverrides +main = Mir.mainWithExtraOverrides $ + compositionalOverrides `orOverride` cryptolOverrides + +orOverride :: + Mir.BindExtraOverridesFn -> Mir.BindExtraOverridesFn -> Mir.BindExtraOverridesFn +orOverride f g symOnline cs name cfg = + case f symOnline cs name cfg of + Just x -> Just x + Nothing -> g symOnline cs name cfg diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs new file mode 100644 index 0000000000..e057637168 --- /dev/null +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -0,0 +1,157 @@ +{-# Language DataKinds #-} +{-# Language GADTs #-} +{-# Language ImplicitParams #-} +{-# Language OverloadedStrings #-} +{-# Language PatternSynonyms #-} +{-# Language RankNTypes #-} +{-# Language ScopedTypeVariables #-} +{-# Language TypeApplications #-} +{-# Language ViewPatterns #-} + +module Mir.Cryptol +where + +import Control.Lens (use) +import Control.Monad +import Control.Monad.IO.Class +import qualified Data.ByteString as BS +import Data.Functor.Const +import Data.IORef +import Data.Map (Map) +import qualified Data.Map as Map +import Data.String (fromString) +import Data.Text (Text) +import qualified Data.Text as Text + +import Data.Parameterized.Context (pattern Empty, pattern (:>)) +import Data.Parameterized.NatRepr +import Data.Parameterized.TraversableFC + +import qualified What4.Expr.Builder as W4 + +import Lang.Crucible.Backend +import Lang.Crucible.CFG.Core +import Lang.Crucible.FunctionHandle +import Lang.Crucible.Simulator + +import Crux +import Crux.Types + +import Mir.DefId +import Mir.Generator (CollectionState) +import Mir.Intrinsics +import Mir.Overrides (getString) + +import qualified Verifier.SAW.Cryptol.Prelude as SAW +import qualified Verifier.SAW.CryptolEnv as SAW +import qualified Verifier.SAW.Prelude as SAW +import qualified Verifier.SAW.Recognizer as SAW +import qualified Verifier.SAW.SharedTerm as SAW +import qualified Verifier.SAW.Simulator.What4.ReturnTrip as SAW +import qualified Verifier.SAW.TypedTerm as SAW + +import Mir.Compositional.Convert (visitExprVars) +import Mir.Compositional.Override (termToExpr) + +import Debug.Trace + + +cryptolOverrides :: + forall sym p t st fs args ret blocks rtp a r . + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => + Maybe (SomeOnlineSolver sym) -> + CollectionState -> + Text -> + CFG MIR blocks args ret -> + Maybe (OverrideSim (p sym) sym MIR rtp a r ()) +cryptolOverrides _symOnline _cs name cfg + + | (normDefId "crucible::cryptol::load" <> "::_inst") `Text.isPrefixOf` name + , Empty + :> MirSliceRepr (BVRepr (testEquality (knownNat @8) -> Just Refl)) + :> MirSliceRepr (BVRepr (testEquality (knownNat @8) -> Just Refl)) + <- cfgArgTypes cfg + = Just $ bindFnHandle (cfgHandle cfg) $ UseOverride $ + mkOverride' "cryptol_load" (cfgReturnType cfg) $ do + RegMap (Empty :> RegEntry _tpr modulePathStr :> RegEntry _tpr' nameStr) <- getOverrideArgs + cryptolLoad (cfgReturnType cfg) modulePathStr nameStr + + | otherwise = Nothing + + +cryptolLoad :: + forall sym p t st fs rtp a r tp . + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => + TypeRepr tp -> + RegValue sym (MirSlice (BVType 8)) -> + RegValue sym (MirSlice (BVType 8)) -> + OverrideSim (p sym) sym MIR rtp a r (RegValue sym tp) +cryptolLoad (FunctionHandleRepr argsCtx retTpr) modulePathStr nameStr = do + modulePath <- getString modulePathStr >>= \x -> case x of + Just s -> return $ Text.unpack s + Nothing -> fail "cryptol::load module path must not be symbolic" + name <- getString nameStr >>= \x -> case x of + Just s -> return $ Text.unpack s + Nothing -> fail "cryptol::load function name must not be symbolic" + + -- TODO share a single SharedContext across all calls + sc <- liftIO $ SAW.mkSharedContext + liftIO $ SAW.scLoadPreludeModule sc + liftIO $ SAW.scLoadCryptolModule sc + let ?fileReader = BS.readFile + ce <- liftIO $ SAW.initCryptolEnv sc + (m, ce') <- liftIO $ SAW.loadCryptolModule sc ce modulePath + tt <- liftIO $ SAW.lookupCryptolModule m name + + scs <- liftIO $ SAW.newSAWCoreState sc + + halloc <- simHandleAllocator <$> use stateContext + let fnName = "cryptol_" ++ modulePath ++ "_" ++ name + fh <- liftIO $ mkHandle' halloc (fromString fnName) argsCtx retTpr + bindFnHandle fh $ UseOverride $ mkOverride' (handleName fh) (handleReturnType fh) $ + cryptolRun sc scs fnName retTpr (SAW.ttTerm tt) + + return $ HandleFnVal fh + +cryptolLoad tpr _ _ = fail $ "cryptol::load: bad function type " ++ show tpr + + +cryptolRun :: + forall sym p t st fs rtp a r tp . + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => + SAW.SharedContext -> + SAW.SAWCoreState t -> + String -> + TypeRepr tp -> + SAW.Term -> + OverrideSim (p sym) sym MIR rtp a r (RegValue sym tp) +cryptolRun sc scs name retTpr funcTerm = do + sym <- getSymInterface + + visitCache <- liftIO $ (W4.newIdxCache :: IO (W4.IdxCache t (Const ()))) + w4VarMapRef <- liftIO $ newIORef (Map.empty :: Map SAW.VarIndex (Some (W4.Expr t))) + + RegMap argsCtx <- getOverrideArgs + args <- forM (toListFC (\re -> Some re) argsCtx) $ \(Some (RegEntry tpr val)) -> do + case asBaseType tpr of + AsBaseType btpr -> do + visitExprVars visitCache val $ \var -> do + let expr = W4.BoundVarExpr var + term <- liftIO $ SAW.toSC sym scs expr + ec <- case SAW.asExtCns term of + Just ec -> return ec + Nothing -> error "eval on BoundVarExpr produced non-ExtCns?" + liftIO $ modifyIORef w4VarMapRef $ Map.insert (SAW.ecVarIndex ec) (Some expr) + liftIO $ SAW.toSC sym scs val + NotBaseType -> fail $ + "type error: " ++ name ++ " got argument of non-base type " ++ show tpr + appTerm <- liftIO $ SAW.scApplyAll sc funcTerm args + + w4VarMap <- liftIO $ readIORef w4VarMapRef + Some expr <- liftIO $ termToExpr sym sc w4VarMap appTerm + Refl <- case testEquality (baseToType $ W4.exprType expr) retTpr of + Just x -> return x + Nothing -> fail $ + "type error: expected " ++ name ++ " to return " ++ show retTpr ++ + ", but it returned " ++ show (W4.exprType expr) ++ " instead" + return expr diff --git a/deps/crucible b/deps/crucible index 0e855576df..2e0a5dc194 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 0e855576dfeb5c783a4d412c1318b1fc14be3400 +Subproject commit 2e0a5dc194a947fdb63fba9135bf8c2a797561d0 From a73e14ea6737f9dff9521222a05cb0073d244448 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Mon, 19 Apr 2021 14:14:14 -0700 Subject: [PATCH 03/34] crux-mir-comp: refactor: move termToExpr etc from Override to Convert --- .../src/Mir/Compositional/Convert.hs | 68 +++++++++++++++++++ .../src/Mir/Compositional/Override.hs | 58 ---------------- crux-mir-comp/src/Mir/Cryptol.hs | 4 +- 3 files changed, 69 insertions(+), 61 deletions(-) diff --git a/crux-mir-comp/src/Mir/Compositional/Convert.hs b/crux-mir-comp/src/Mir/Compositional/Convert.hs index 3dcf12bf82..fb5fb13c76 100644 --- a/crux-mir-comp/src/Mir/Compositional/Convert.hs +++ b/crux-mir-comp/src/Mir/Compositional/Convert.hs @@ -1,9 +1,11 @@ {-# LANGUAGE DataKinds #-} +{-# Language FlexibleContexts #-} {-# Language GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} -- | Conversions between Crucible `RegValue`s and SAW `Term`s. module Mir.Compositional.Convert @@ -13,6 +15,8 @@ import Control.Lens ((^.), (^..), each) import Control.Monad import Control.Monad.IO.Class import Data.Functor.Const +import Data.IORef +import Data.Map (Map) import qualified Data.Map as Map import Data.Parameterized.Context (pattern Empty, pattern (:>), Assignment) import qualified Data.Parameterized.Context as Ctx @@ -20,6 +24,7 @@ import Data.Parameterized.Some import Data.Parameterized.TraversableFC import Data.Set (Set) import qualified Data.Set as Set +import GHC.Stack (HasCallStack) import Lang.Crucible.Backend import Lang.Crucible.Simulator.RegValue @@ -29,6 +34,10 @@ import qualified What4.Expr.Builder as W4 import qualified What4.Interface as W4 import qualified What4.Partial as W4 +import qualified Verifier.SAW.SharedTerm as SAW +import qualified Verifier.SAW.Simulator.Value as SAW +import qualified Verifier.SAW.Simulator.What4 as SAW + import Mir.Intrinsics import qualified Mir.Mir as M import Mir.TransTy (tyToRepr, canInitialize, isUnsized) @@ -246,3 +255,62 @@ readPartExprMaybe _sym W4.Unassigned = return Nothing readPartExprMaybe _sym (W4.PE p v) | Just True <- W4.asConstantPred p = return $ Just v | otherwise = return Nothing + + +-- | Convert a `SAW.Term` into a `W4.Expr`. +termToExpr :: forall sym t st fs. + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasCallStack) => + sym -> + SAW.SharedContext -> + Map SAW.VarIndex (Some (W4.Expr t)) -> + SAW.Term -> + IO (Some (W4.SymExpr sym)) +termToExpr sym sc varMap term = do + let convert (Some expr) = case SAW.symExprToValue (W4.exprType expr) expr of + Just x -> return x + Nothing -> error $ "termToExpr: failed to convert var of what4 type " ++ + show (W4.exprType expr) + ecMap <- mapM convert varMap + ref <- newIORef mempty + sv <- SAW.w4SolveBasic sym sc mempty ecMap ref mempty term + case SAW.valueToSymExpr sv of + Just x -> return x + Nothing -> error $ "termToExpr: failed to convert SValue" + +-- | Convert a `SAW.Term` to a `W4.Pred`. If the term doesn't have boolean +-- type, this will raise an error. +termToPred :: forall sym t st fs. + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasCallStack) => + sym -> + SAW.SharedContext -> + Map SAW.VarIndex (Some (W4.Expr t)) -> + SAW.Term -> + IO (W4.Pred sym) +termToPred sym sc varMap term = do + Some expr <- termToExpr sym sc varMap term + case W4.exprType expr of + BaseBoolRepr -> return expr + btpr -> error $ "termToPred: got result of type " ++ show btpr ++ ", not BaseBoolRepr" + +-- | Convert a `SAW.Term` representing a type to a `W4.BaseTypeRepr`. +termToType :: forall sym t st fs. + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasCallStack) => + sym -> + SAW.SharedContext -> + SAW.Term -> + IO (Some W4.BaseTypeRepr) +termToType sym sc term = do + ref <- newIORef mempty + sv <- SAW.w4SolveBasic sym sc mempty mempty ref mempty term + tv <- case sv of + SAW.TValue tv -> return tv + _ -> error $ "termToType: bad SValue" + case tv of + SAW.VBoolType -> return $ Some BaseBoolRepr + SAW.VVecType w SAW.VBoolType -> do + Some w <- return $ mkNatRepr w + LeqProof <- case testLeq (knownNat @1) w of + Just x -> return x + Nothing -> error "termToPred: zero-width bitvector" + return $ Some $ BaseBVRepr w + _ -> error $ "termToType: bad SValue" diff --git a/crux-mir-comp/src/Mir/Compositional/Override.hs b/crux-mir-comp/src/Mir/Compositional/Override.hs index 9ef900aff6..e22f5adcec 100644 --- a/crux-mir-comp/src/Mir/Compositional/Override.hs +++ b/crux-mir-comp/src/Mir/Compositional/Override.hs @@ -551,64 +551,6 @@ condTerm sc (MS.SetupCond_Pred _loc tt) = do condTerm _ (MS.SetupCond_Ghost _ _ _ _) = do error $ "learnCond: SetupCond_Ghost is not supported" --- | Convert a `SAW.Term` into a `W4.Expr`. -termToExpr :: forall sym t st fs. - (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasCallStack) => - sym -> - SAW.SharedContext -> - Map SAW.VarIndex (Some (W4.Expr t)) -> - SAW.Term -> - IO (Some (W4.SymExpr sym)) -termToExpr sym sc varMap term = do - let convert (Some expr) = case SAW.symExprToValue (W4.exprType expr) expr of - Just x -> return x - Nothing -> error $ "termToExpr: failed to convert var of what4 type " ++ - show (W4.exprType expr) - ecMap <- mapM convert varMap - ref <- newIORef mempty - sv <- SAW.w4SolveBasic sym sc mempty ecMap ref mempty term - case SAW.valueToSymExpr sv of - Just x -> return x - Nothing -> error $ "termToExpr: failed to convert SValue" - --- | Convert a `SAW.Term` to a `W4.Pred`. If the term doesn't have boolean --- type, this will raise an error. -termToPred :: forall sym t st fs. - (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasCallStack) => - sym -> - SAW.SharedContext -> - Map SAW.VarIndex (Some (W4.Expr t)) -> - SAW.Term -> - IO (W4.Pred sym) -termToPred sym sc varMap term = do - Some expr <- termToExpr sym sc varMap term - case W4.exprType expr of - BaseBoolRepr -> return expr - btpr -> error $ "termToPred: got result of type " ++ show btpr ++ ", not BaseBoolRepr" - --- | Convert a `SAW.Term` representing a type to a `W4.BaseTypeRepr`. -termToType :: forall sym t st fs. - (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasCallStack) => - sym -> - SAW.SharedContext -> - SAW.Term -> - IO (Some W4.BaseTypeRepr) -termToType sym sc term = do - ref <- newIORef mempty - sv <- SAW.w4SolveBasic sym sc mempty mempty ref mempty term - tv <- case sv of - SAW.TValue tv -> return tv - _ -> error $ "termToType: bad SValue" - case tv of - SAW.VBoolType -> return $ Some BaseBoolRepr - SAW.VVecType w SAW.VBoolType -> do - Some w <- return $ mkNatRepr w - LeqProof <- case testLeq (knownNat @1) w of - Just x -> return x - Nothing -> error "termToPred: zero-width bitvector" - return $ Some $ BaseBVRepr w - _ -> error $ "termToType: bad SValue" - checkDisjoint :: (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) => diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index e057637168..d153359177 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -44,14 +44,12 @@ import Mir.Overrides (getString) import qualified Verifier.SAW.Cryptol.Prelude as SAW import qualified Verifier.SAW.CryptolEnv as SAW -import qualified Verifier.SAW.Prelude as SAW import qualified Verifier.SAW.Recognizer as SAW import qualified Verifier.SAW.SharedTerm as SAW import qualified Verifier.SAW.Simulator.What4.ReturnTrip as SAW import qualified Verifier.SAW.TypedTerm as SAW -import Mir.Compositional.Convert (visitExprVars) -import Mir.Compositional.Override (termToExpr) +import Mir.Compositional.Convert (visitExprVars, termToExpr) import Debug.Trace From d0248b81d153af094495491cc076f4decb834731 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Mon, 19 Apr 2021 16:57:43 -0700 Subject: [PATCH 04/34] add support for cryptol functions returning tuples --- .../src/Mir/Compositional/Convert.hs | 78 ++++++++++++++++++- crux-mir-comp/src/Mir/Cryptol.hs | 40 ++++++---- 2 files changed, 97 insertions(+), 21 deletions(-) diff --git a/crux-mir-comp/src/Mir/Compositional/Convert.hs b/crux-mir-comp/src/Mir/Compositional/Convert.hs index fb5fb13c76..48e85e90bd 100644 --- a/crux-mir-comp/src/Mir/Compositional/Convert.hs +++ b/crux-mir-comp/src/Mir/Compositional/Convert.hs @@ -33,9 +33,12 @@ import Lang.Crucible.Types import qualified What4.Expr.Builder as W4 import qualified What4.Interface as W4 import qualified What4.Partial as W4 +import qualified What4.SWord as W4 import qualified Verifier.SAW.SharedTerm as SAW +import qualified Verifier.SAW.Simulator.MonadLazy as SAW import qualified Verifier.SAW.Simulator.Value as SAW +import Verifier.SAW.Simulator.What4 (SValue) import qualified Verifier.SAW.Simulator.What4 as SAW import Mir.Intrinsics @@ -266,16 +269,83 @@ termToExpr :: forall sym t st fs. SAW.Term -> IO (Some (W4.SymExpr sym)) termToExpr sym sc varMap term = do + sv <- termToSValue sym sc varMap term + case SAW.valueToSymExpr sv of + Just x -> return x + Nothing -> error $ "termToExpr: failed to convert SValue" + +-- | Convert a `SAW.Term` into a Crucible `RegValue`. Requires a `TypeShape` +-- giving the expected MIR/Crucible type in order to distinguish cases like +-- `(A, (B, C))` vs `(A, B, C)` (these are the same type in saw-core). +termToReg :: forall sym t st fs tp. + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasCallStack) => + sym -> + SAW.SharedContext -> + Map SAW.VarIndex (Some (W4.Expr t)) -> + SAW.Term -> + TypeShape tp -> + IO (RegValue sym tp) +termToReg sym sc varMap term shp = do + sv <- termToSValue sym sc varMap term + go shp sv + where + go :: forall tp'. TypeShape tp' -> SValue sym -> IO (RegValue sym tp') + go shp sv = case (shp, sv) of + (UnitShape _, SAW.VUnit) -> return () + (PrimShape _ BaseBoolRepr, SAW.VBool b) -> return b + (PrimShape _ (BaseBVRepr w), SAW.VWord (W4.DBV e)) + | Just Refl <- testEquality (W4.exprType e) (BaseBVRepr w) -> return e + (TupleShape _ _ flds, _) -> do + svs <- tupleToListRev (Ctx.sizeInt $ Ctx.size flds) [] sv + goTuple flds svs + _ -> error $ "termToReg: type error: need to produce " ++ show (shapeType shp) ++ + ", but simulator returned " ++ show sv + + -- | Convert an `SValue` tuple (built from nested `VPair`s) into a list of + -- the inner `SValue`s, in reverse order. + tupleToListRev :: Int -> [SValue sym] -> SValue sym -> IO [SValue sym] + tupleToListRev 2 acc (SAW.VPair x y) = do + x' <- SAW.force x + y' <- SAW.force y + return $ y' : x' : acc + tupleToListRev n acc (SAW.VPair x xs) | n > 2 = do + x' <- SAW.force x + xs' <- SAW.force xs + tupleToListRev (n - 1) (x' : acc) xs' + tupleToListRev n _ _ = error $ "bad tuple size " ++ show n + tupleToListRev n _ v = error $ "termToReg: expected tuple of " ++ show n ++ + " elements, but got " ++ show v + + goTuple :: forall ctx. + Assignment FieldShape ctx -> + [SValue sym] -> + IO (RegValue sym (StructType ctx)) + goTuple Empty [] = return Empty + goTuple (flds :> fld) (sv : svs) = do + rv <- goField fld sv + rvs <- goTuple flds svs + return (rvs :> RV rv) + + goField :: forall tp'. FieldShape tp' -> SValue sym -> IO (RegValue sym tp') + goField (ReqField shp) sv = go shp sv + goField (OptField shp) sv = W4.justPartExpr sym <$> go shp sv + +-- | Common code for termToExpr and termToReg +termToSValue :: forall sym t st fs. + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasCallStack) => + sym -> + SAW.SharedContext -> + Map SAW.VarIndex (Some (W4.Expr t)) -> + SAW.Term -> + IO (SAW.SValue sym) +termToSValue sym sc varMap term = do let convert (Some expr) = case SAW.symExprToValue (W4.exprType expr) expr of Just x -> return x Nothing -> error $ "termToExpr: failed to convert var of what4 type " ++ show (W4.exprType expr) ecMap <- mapM convert varMap ref <- newIORef mempty - sv <- SAW.w4SolveBasic sym sc mempty ecMap ref mempty term - case SAW.valueToSymExpr sv of - Just x -> return x - Nothing -> error $ "termToExpr: failed to convert SValue" + SAW.w4SolveBasic sym sc mempty ecMap ref mempty term -- | Convert a `SAW.Term` to a `W4.Pred`. If the term doesn't have boolean -- type, this will raise an error. diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index d153359177..f12f4c4174 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -11,7 +11,7 @@ module Mir.Cryptol where -import Control.Lens (use) +import Control.Lens (use, (^.), (^?), _Wrapped, ix) import Control.Monad import Control.Monad.IO.Class import qualified Data.ByteString as BS @@ -38,8 +38,9 @@ import Crux import Crux.Types import Mir.DefId -import Mir.Generator (CollectionState) +import Mir.Generator (CollectionState, collection) import Mir.Intrinsics +import qualified Mir.Mir as M import Mir.Overrides (getString) import qualified Verifier.SAW.Cryptol.Prelude as SAW @@ -49,7 +50,7 @@ import qualified Verifier.SAW.SharedTerm as SAW import qualified Verifier.SAW.Simulator.What4.ReturnTrip as SAW import qualified Verifier.SAW.TypedTerm as SAW -import Mir.Compositional.Convert (visitExprVars, termToExpr) +import Mir.Compositional.Convert import Debug.Trace @@ -62,7 +63,7 @@ cryptolOverrides :: Text -> CFG MIR blocks args ret -> Maybe (OverrideSim (p sym) sym MIR rtp a r ()) -cryptolOverrides _symOnline _cs name cfg +cryptolOverrides _symOnline cs name cfg | (normDefId "crucible::cryptol::load" <> "::_inst") `Text.isPrefixOf` name , Empty @@ -71,8 +72,14 @@ cryptolOverrides _symOnline _cs name cfg <- cfgArgTypes cfg = Just $ bindFnHandle (cfgHandle cfg) $ UseOverride $ mkOverride' "cryptol_load" (cfgReturnType cfg) $ do + let tyArg = cs ^? collection . M.intrinsics . ix (textId name) . + M.intrInst . M.inSubsts . _Wrapped . ix 0 + sig <- case tyArg of + Just (M.TyFnPtr sig) -> return sig + _ -> error $ "expected TyFnPtr argument, but got " ++ show tyArg + RegMap (Empty :> RegEntry _tpr modulePathStr :> RegEntry _tpr' nameStr) <- getOverrideArgs - cryptolLoad (cfgReturnType cfg) modulePathStr nameStr + cryptolLoad (cs ^. collection) sig (cfgReturnType cfg) modulePathStr nameStr | otherwise = Nothing @@ -80,11 +87,13 @@ cryptolOverrides _symOnline _cs name cfg cryptolLoad :: forall sym p t st fs rtp a r tp . (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => + M.Collection -> + M.FnSig -> TypeRepr tp -> RegValue sym (MirSlice (BVType 8)) -> RegValue sym (MirSlice (BVType 8)) -> OverrideSim (p sym) sym MIR rtp a r (RegValue sym tp) -cryptolLoad (FunctionHandleRepr argsCtx retTpr) modulePathStr nameStr = do +cryptolLoad col sig (FunctionHandleRepr argsCtx retTpr) modulePathStr nameStr = do modulePath <- getString modulePathStr >>= \x -> case x of Just s -> return $ Text.unpack s Nothing -> fail "cryptol::load module path must not be symbolic" @@ -92,6 +101,8 @@ cryptolLoad (FunctionHandleRepr argsCtx retTpr) modulePathStr nameStr = do Just s -> return $ Text.unpack s Nothing -> fail "cryptol::load function name must not be symbolic" + let retShp = tyToShapeEq col (sig ^. M.fsreturn_ty) retTpr + -- TODO share a single SharedContext across all calls sc <- liftIO $ SAW.mkSharedContext liftIO $ SAW.scLoadPreludeModule sc @@ -107,11 +118,11 @@ cryptolLoad (FunctionHandleRepr argsCtx retTpr) modulePathStr nameStr = do let fnName = "cryptol_" ++ modulePath ++ "_" ++ name fh <- liftIO $ mkHandle' halloc (fromString fnName) argsCtx retTpr bindFnHandle fh $ UseOverride $ mkOverride' (handleName fh) (handleReturnType fh) $ - cryptolRun sc scs fnName retTpr (SAW.ttTerm tt) + cryptolRun sc scs fnName retShp (SAW.ttTerm tt) return $ HandleFnVal fh -cryptolLoad tpr _ _ = fail $ "cryptol::load: bad function type " ++ show tpr +cryptolLoad _ _ tpr _ _ = fail $ "cryptol::load: bad function type " ++ show tpr cryptolRun :: @@ -120,10 +131,10 @@ cryptolRun :: SAW.SharedContext -> SAW.SAWCoreState t -> String -> - TypeRepr tp -> + TypeShape tp -> SAW.Term -> OverrideSim (p sym) sym MIR rtp a r (RegValue sym tp) -cryptolRun sc scs name retTpr funcTerm = do +cryptolRun sc scs name retShp funcTerm = do sym <- getSymInterface visitCache <- liftIO $ (W4.newIdxCache :: IO (W4.IdxCache t (Const ()))) @@ -146,10 +157,5 @@ cryptolRun sc scs name retTpr funcTerm = do appTerm <- liftIO $ SAW.scApplyAll sc funcTerm args w4VarMap <- liftIO $ readIORef w4VarMapRef - Some expr <- liftIO $ termToExpr sym sc w4VarMap appTerm - Refl <- case testEquality (baseToType $ W4.exprType expr) retTpr of - Just x -> return x - Nothing -> fail $ - "type error: expected " ++ name ++ " to return " ++ show retTpr ++ - ", but it returned " ++ show (W4.exprType expr) ++ " instead" - return expr + rv <- liftIO $ termToReg sym sc w4VarMap appTerm retShp + return rv From 7000cd3d199238ebff6229fa26966986d63ba3a4 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Tue, 20 Apr 2021 11:39:25 -0700 Subject: [PATCH 05/34] refactor conversion of RegValue arguments to SAW.Term --- crux-mir-comp/src/Mir/Cryptol.hs | 68 +++++++++++++++++++++++++------- 1 file changed, 53 insertions(+), 15 deletions(-) diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index f12f4c4174..b62b55f3a4 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -101,6 +101,7 @@ cryptolLoad col sig (FunctionHandleRepr argsCtx retTpr) modulePathStr nameStr = Just s -> return $ Text.unpack s Nothing -> fail "cryptol::load function name must not be symbolic" + let argShps = map (tyToShape col) (sig ^. M.fsarg_tys) let retShp = tyToShapeEq col (sig ^. M.fsreturn_ty) retTpr -- TODO share a single SharedContext across all calls @@ -118,7 +119,7 @@ cryptolLoad col sig (FunctionHandleRepr argsCtx retTpr) modulePathStr nameStr = let fnName = "cryptol_" ++ modulePath ++ "_" ++ name fh <- liftIO $ mkHandle' halloc (fromString fnName) argsCtx retTpr bindFnHandle fh $ UseOverride $ mkOverride' (handleName fh) (handleReturnType fh) $ - cryptolRun sc scs fnName retShp (SAW.ttTerm tt) + cryptolRun sc scs fnName argShps retShp (SAW.ttTerm tt) return $ HandleFnVal fh @@ -131,31 +132,68 @@ cryptolRun :: SAW.SharedContext -> SAW.SAWCoreState t -> String -> + [Some TypeShape] -> TypeShape tp -> SAW.Term -> OverrideSim (p sym) sym MIR rtp a r (RegValue sym tp) -cryptolRun sc scs name retShp funcTerm = do +cryptolRun sc scs name argShps retShp funcTerm = do sym <- getSymInterface visitCache <- liftIO $ (W4.newIdxCache :: IO (W4.IdxCache t (Const ()))) w4VarMapRef <- liftIO $ newIORef (Map.empty :: Map SAW.VarIndex (Some (W4.Expr t))) RegMap argsCtx <- getOverrideArgs - args <- forM (toListFC (\re -> Some re) argsCtx) $ \(Some (RegEntry tpr val)) -> do - case asBaseType tpr of - AsBaseType btpr -> do - visitExprVars visitCache val $ \var -> do - let expr = W4.BoundVarExpr var - term <- liftIO $ SAW.toSC sym scs expr - ec <- case SAW.asExtCns term of - Just ec -> return ec - Nothing -> error "eval on BoundVarExpr produced non-ExtCns?" - liftIO $ modifyIORef w4VarMapRef $ Map.insert (SAW.ecVarIndex ec) (Some expr) - liftIO $ SAW.toSC sym scs val - NotBaseType -> fail $ - "type error: " ++ name ++ " got argument of non-base type " ++ show tpr + args <- forM (zip argShps (toListFC (\re -> Some re) argsCtx)) $ + \(Some argShp, Some (RegEntry tpr val)) -> do + Refl <- case testEquality (shapeType argShp) tpr of + Just x -> return x + Nothing -> fail $ + "type error: " ++ name ++ " expected argument of type " ++ + show (shapeType argShp) ++ ", but got " ++ show tpr + regToTerm sym sc scs name visitCache w4VarMapRef argShp val appTerm <- liftIO $ SAW.scApplyAll sc funcTerm args w4VarMap <- liftIO $ readIORef w4VarMapRef rv <- liftIO $ termToReg sym sc w4VarMap appTerm retShp return rv + + where + +exprToTerm :: forall sym p t st fs tp rtp a r. + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => + sym -> + SAW.SharedContext -> + SAW.SAWCoreState t -> + W4.IdxCache t (Const ()) -> + IORef (Map SAW.VarIndex (Some (W4.Expr t))) -> + W4.Expr t tp -> + OverrideSim (p sym) sym MIR rtp a r SAW.Term +exprToTerm sym sc scs visitCache w4VarMapRef val = do + visitExprVars visitCache val $ \var -> do + let expr = W4.BoundVarExpr var + term <- liftIO $ SAW.toSC sym scs expr + ec <- case SAW.asExtCns term of + Just ec -> return ec + Nothing -> error "eval on BoundVarExpr produced non-ExtCns?" + liftIO $ modifyIORef w4VarMapRef $ Map.insert (SAW.ecVarIndex ec) (Some expr) + liftIO $ SAW.toSC sym scs val + +regToTerm :: forall sym p t st fs tp rtp a r. + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => + sym -> + SAW.SharedContext -> + SAW.SAWCoreState t -> + String -> + W4.IdxCache t (Const ()) -> + IORef (Map SAW.VarIndex (Some (W4.Expr t))) -> + TypeShape tp -> + RegValue sym tp -> + OverrideSim (p sym) sym MIR rtp a r SAW.Term +regToTerm sym sc scs name visitCache w4VarMapRef shp rv = go shp rv + where + go :: TypeShape tp -> RegValue sym tp -> OverrideSim (p sym) sym MIR rtp a r SAW.Term + go shp rv = case (shp, rv) of + (UnitShape _, ()) -> liftIO $ SAW.scUnitValue sc + (PrimShape _ btpr, expr) -> exprToTerm sym sc scs visitCache w4VarMapRef expr + _ -> fail $ + "type error: " ++ name ++ " got argument of unsupported type " ++ show (shapeType shp) From fef9ac36459b04c8616f63c2797cb2005099aafe Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Tue, 20 Apr 2021 11:46:52 -0700 Subject: [PATCH 06/34] add support for tuples as arguments --- crux-mir-comp/src/Mir/Cryptol.hs | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index b62b55f3a4..1c58228545 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -24,6 +24,7 @@ import Data.Text (Text) import qualified Data.Text as Text import Data.Parameterized.Context (pattern Empty, pattern (:>)) +import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.NatRepr import Data.Parameterized.TraversableFC @@ -191,9 +192,24 @@ regToTerm :: forall sym p t st fs tp rtp a r. OverrideSim (p sym) sym MIR rtp a r SAW.Term regToTerm sym sc scs name visitCache w4VarMapRef shp rv = go shp rv where - go :: TypeShape tp -> RegValue sym tp -> OverrideSim (p sym) sym MIR rtp a r SAW.Term + go :: forall tp. + TypeShape tp -> + RegValue sym tp -> + OverrideSim (p sym) sym MIR rtp a r SAW.Term go shp rv = case (shp, rv) of (UnitShape _, ()) -> liftIO $ SAW.scUnitValue sc - (PrimShape _ btpr, expr) -> exprToTerm sym sc scs visitCache w4VarMapRef expr + (PrimShape _ _, expr) -> exprToTerm sym sc scs visitCache w4VarMapRef expr + (TupleShape _ _ flds, rvs) -> do + terms <- Ctx.zipWithM (\fld (RV rv) -> Const <$> goField fld rv) flds rvs + liftIO $ SAW.scTuple sc (toListFC getConst terms) _ -> fail $ "type error: " ++ name ++ " got argument of unsupported type " ++ show (shapeType shp) + + goField :: forall tp. + FieldShape tp -> + RegValue sym tp -> + OverrideSim (p sym) sym MIR rtp a r SAW.Term + goField (OptField shp) rv = do + rv' <- liftIO $ readMaybeType sym "field" (shapeType shp) rv + go shp rv' + goField (ReqField shp) rv = go shp rv From 19b2079b0ed8394e06933b6547f2bb41a039dde6 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Tue, 20 Apr 2021 13:52:11 -0700 Subject: [PATCH 07/34] support array arguments --- crux-mir-comp/src/Mir/Cryptol.hs | 42 ++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index 1c58228545..d2ea1cb95a 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -15,6 +15,7 @@ import Control.Lens (use, (^.), (^?), _Wrapped, ix) import Control.Monad import Control.Monad.IO.Class import qualified Data.ByteString as BS +import Data.Foldable import Data.Functor.Const import Data.IORef import Data.Map (Map) @@ -202,6 +203,10 @@ regToTerm sym sc scs name visitCache w4VarMapRef shp rv = go shp rv (TupleShape _ _ flds, rvs) -> do terms <- Ctx.zipWithM (\fld (RV rv) -> Const <$> goField fld rv) flds rvs liftIO $ SAW.scTuple sc (toListFC getConst terms) + (ArrayShape _ _ shp, vec) -> do + terms <- goVector shp vec + tyTerm <- shapeToTerm sc shp + liftIO $ SAW.scVector sc tyTerm terms _ -> fail $ "type error: " ++ name ++ " got argument of unsupported type " ++ show (shapeType shp) @@ -213,3 +218,40 @@ regToTerm sym sc scs name visitCache w4VarMapRef shp rv = go shp rv rv' <- liftIO $ readMaybeType sym "field" (shapeType shp) rv go shp rv' goField (ReqField shp) rv = go shp rv + + goVector :: forall tp. + TypeShape tp -> + MirVector sym tp -> + OverrideSim (p sym) sym MIR rtp a r [SAW.Term] + goVector shp (MirVector_Vector v) = mapM (go shp) $ toList v + goVector shp (MirVector_PartialVector pv) = do + forM (toList pv) $ \rv -> do + rv' <- liftIO $ readMaybeType sym "field" (shapeType shp) rv + go shp rv' + goVector shp (MirVector_Array _) = fail $ + "regToTerm: MirVector_Array not supported" + +shapeToTerm :: forall tp m. + (MonadIO m, MonadFail m) => + SAW.SharedContext -> + TypeShape tp -> + m SAW.Term +shapeToTerm sc shp = go shp + where + go :: forall tp. TypeShape tp -> m SAW.Term + go (UnitShape _) = liftIO $ SAW.scUnitType sc + go (PrimShape _ BaseBoolRepr) = liftIO $ SAW.scBoolType sc + go (PrimShape _ (BaseBVRepr w)) = liftIO $ SAW.scBitvector sc (natValue w) + go (TupleShape _ _ flds) = do + tys <- toListFC getConst <$> traverseFC (\x -> Const <$> goField x) flds + liftIO $ SAW.scTupleType sc tys + go (ArrayShape (M.TyArray _ n) _ shp) = do + ty <- go shp + n <- liftIO $ SAW.scNat sc (fromIntegral n) + liftIO $ SAW.scVecType sc n ty + go shp = fail $ "shapeToTerm: unsupported type " ++ show (shapeType shp) + + goField :: forall tp. FieldShape tp -> m SAW.Term + goField (OptField shp) = go shp + goField (ReqField shp) = go shp + From 697bfdc3fa85a78d7c8ced9740e3138161cc1e56 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Tue, 20 Apr 2021 14:00:16 -0700 Subject: [PATCH 08/34] add support for array arguments --- crux-mir-comp/src/Mir/Compositional/Convert.hs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/crux-mir-comp/src/Mir/Compositional/Convert.hs b/crux-mir-comp/src/Mir/Compositional/Convert.hs index 48e85e90bd..9033a34e72 100644 --- a/crux-mir-comp/src/Mir/Compositional/Convert.hs +++ b/crux-mir-comp/src/Mir/Compositional/Convert.hs @@ -14,6 +14,7 @@ where import Control.Lens ((^.), (^..), each) import Control.Monad import Control.Monad.IO.Class +import Data.Foldable import Data.Functor.Const import Data.IORef import Data.Map (Map) @@ -24,6 +25,7 @@ import Data.Parameterized.Some import Data.Parameterized.TraversableFC import Data.Set (Set) import qualified Data.Set as Set +import qualified Data.Vector as V import GHC.Stack (HasCallStack) import Lang.Crucible.Backend @@ -298,6 +300,13 @@ termToReg sym sc varMap term shp = do (TupleShape _ _ flds, _) -> do svs <- tupleToListRev (Ctx.sizeInt $ Ctx.size flds) [] sv goTuple flds svs + (ArrayShape (M.TyArray _ n) _ shp, SAW.VVector thunks) -> do + svs <- mapM SAW.force $ toList thunks + when (length svs /= n) $ fail $ + "termToReg: type error: expected an array of length " ++ show n ++ + ", but simulator returned " ++ show (length svs) ++ " elements" + v <- V.fromList <$> mapM (go shp) svs + return $ MirVector_Vector v _ -> error $ "termToReg: type error: need to produce " ++ show (shapeType shp) ++ ", but simulator returned " ++ show sv From da32a424dad9bd34e9437f78a4f3b773a0d031f4 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Tue, 20 Apr 2021 14:12:00 -0700 Subject: [PATCH 09/34] handle [bool; N] return values, which may appear as bitvectors --- crux-mir-comp/src/Mir/Compositional/Convert.hs | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/crux-mir-comp/src/Mir/Compositional/Convert.hs b/crux-mir-comp/src/Mir/Compositional/Convert.hs index 9033a34e72..083b696370 100644 --- a/crux-mir-comp/src/Mir/Compositional/Convert.hs +++ b/crux-mir-comp/src/Mir/Compositional/Convert.hs @@ -307,6 +307,17 @@ termToReg sym sc varMap term shp = do ", but simulator returned " ++ show (length svs) ++ " elements" v <- V.fromList <$> mapM (go shp) svs return $ MirVector_Vector v + -- Special case: saw-core/cryptol doesn't distinguish bitvectors from + -- vectors of booleans, so it may return `VWord` (bitvector) where an + -- array of `bool` is expected. + (ArrayShape (M.TyArray _ n) _ (PrimShape _ BaseBoolRepr), SAW.VWord (W4.DBV e)) + | Just (Some w) <- someNat n, + Just LeqProof <- testLeq (knownNat @1) w, + Just Refl <- testEquality (W4.exprType e) (BaseBVRepr w) -> do + v <- V.generateM n $ \i -> do + -- Cryptol bitvectors are MSB-first, but What4 uses LSB-first. + liftIO $ W4.testBitBV sym (fromIntegral $ n - i - 1) e + return $ MirVector_Vector v _ -> error $ "termToReg: type error: need to produce " ++ show (shapeType shp) ++ ", but simulator returned " ++ show sv From bd21a28014eb812941ea379e31c2e6b986507865 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Tue, 20 Apr 2021 16:24:29 -0700 Subject: [PATCH 10/34] check cryptol and rust function signatures in cryptol::load --- crux-mir-comp/crux-mir-comp.cabal | 1 + crux-mir-comp/src/Mir/Cryptol.hs | 67 +++++++++++++++++++++++++++++++ 2 files changed, 68 insertions(+) diff --git a/crux-mir-comp/crux-mir-comp.cabal b/crux-mir-comp/crux-mir-comp.cabal index 607486e440..1d9751d7bd 100644 --- a/crux-mir-comp/crux-mir-comp.cabal +++ b/crux-mir-comp/crux-mir-comp.cabal @@ -41,6 +41,7 @@ library template-haskell, saw-core, saw-core-what4, + cryptol, cryptol-saw-core, saw-script diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index d2ea1cb95a..97c579b5d9 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -31,6 +31,9 @@ import Data.Parameterized.TraversableFC import qualified What4.Expr.Builder as W4 +import Cryptol.TypeCheck.AST as Cry +import Cryptol.Utils.PP as Cry + import Lang.Crucible.Backend import Lang.Crucible.CFG.Core import Lang.Crucible.FunctionHandle @@ -43,6 +46,7 @@ import Mir.DefId import Mir.Generator (CollectionState, collection) import Mir.Intrinsics import qualified Mir.Mir as M +import qualified Mir.PP as M import Mir.Overrides (getString) import qualified Verifier.SAW.Cryptol.Prelude as SAW @@ -115,6 +119,10 @@ cryptolLoad col sig (FunctionHandleRepr argsCtx retTpr) modulePathStr nameStr = (m, ce') <- liftIO $ SAW.loadCryptolModule sc ce modulePath tt <- liftIO $ SAW.lookupCryptolModule m name + case typecheckFnSig sig argShps (Some retShp) (SAW.ttSchema tt) of + Left err -> fail $ "error loading " ++ show name ++ ": " ++ err + Right () -> return () + scs <- liftIO $ SAW.newSAWCoreState sc halloc <- simHandleAllocator <$> use stateContext @@ -255,3 +263,62 @@ shapeToTerm sc shp = go shp goField (OptField shp) = go shp goField (ReqField shp) = go shp + +typecheckFnSig :: + M.FnSig -> + [Some TypeShape] -> + Some TypeShape -> + Cry.Schema -> + Either String () +typecheckFnSig fnSig argShps retShp sch@(Cry.Forall [] [] ty) = go 0 argShps ty + where + go :: Int -> [Some TypeShape] -> Cry.Type -> Either String () + go _ [] ty | Some retShp' <- retShp = goOne "return value" retShp' ty + go i (Some argShp : argShps) (Cry.tNoUser -> Cry.TCon (Cry.TC Cry.TCFun) [argTy, ty']) = do + goOne ("argument " ++ show i) argShp argTy + go (i + 1) argShps ty' + go i argShps _ = Left $ + "not enough arguments: Cryptol function signature " ++ show (Cry.pp sch) ++ + " has " ++ show i ++ " arguments, but Rust signature " ++ M.fmt fnSig ++ + " requires " ++ show (i + length argShps) + + goOne :: forall tp. String -> TypeShape tp -> Cry.Type -> Either String () + goOne desc shp ty = case (shp, ty) of + (_, Cry.TUser _ _ ty') -> goOne desc shp ty' + (UnitShape _, Cry.TCon (Cry.TC (Cry.TCTuple 0)) []) -> Right () + (PrimShape _ BaseBoolRepr, Cry.TCon (Cry.TC Cry.TCBit) []) -> Right () + (PrimShape _ (BaseBVRepr w), + Cry.TCon (Cry.TC Cry.TCSeq) [ + Cry.tNoUser -> Cry.TCon (Cry.TC (Cry.TCNum n)) [], + Cry.tNoUser -> Cry.TCon (Cry.TC Cry.TCBit) []]) + | fromIntegral (intValue w) == n -> Right () + | otherwise -> typeErr desc shp ty $ + "bitvector width " ++ show n ++ " does not match " ++ show (intValue w) + (TupleShape _ _ flds, Cry.TCon (Cry.TC (Cry.TCTuple n)) tys) + | Ctx.sizeInt (Ctx.size flds) == n -> do + let flds' = toListFC Some flds + zipWithM_ (\(Some fld) ty -> goOneField desc fld ty) flds' tys + | otherwise -> typeErr desc shp ty $ + "tuple size " ++ show n ++ " does not match " ++ show (Ctx.sizeInt $ Ctx.size flds) + (ArrayShape (M.TyArray _ n) _ shp, + Cry.TCon (Cry.TC Cry.TCSeq) [ + Cry.tNoUser -> Cry.TCon (Cry.TC (Cry.TCNum n')) [], + ty']) + | fromIntegral n == n' -> goOne desc shp ty' + | otherwise -> typeErr desc shp ty $ + "array length " ++ show n' ++ " does not match " ++ show n + _ -> typeErr desc shp ty "" + + typeErr :: forall tp. String -> TypeShape tp -> Cry.Type -> String -> Either String () + typeErr desc shp ty extra = Left $ + "type mismatch in " ++ desc ++ ": Cryptol type " ++ show (Cry.pp ty) ++ + " does not match Rust type " ++ M.fmt (shapeMirTy shp) ++ + (if not (null extra) then ": " ++ extra else "") + + goOneField :: forall tp. String -> FieldShape tp -> Cry.Type -> Either String () + goOneField desc (OptField shp) ty = goOne desc shp ty + goOneField desc (ReqField shp) ty = goOne desc shp ty + +typecheckFnSig _ argShps retShp sch = Left $ + "polymorphic Cryptol functions are not supported (got signature: " ++ + show (Cry.pp sch) ++ ")" From 903637257b2978825aea037193af15c977b8205d Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Wed, 21 Apr 2021 10:42:05 -0700 Subject: [PATCH 11/34] update tests for libcrucible line number changes --- crux-mir-comp/test/symb_eval/comp/alias_array_bad.good | 4 ++-- crux-mir-comp/test/symb_eval/comp/alias_array_bad2.good | 2 +- crux-mir-comp/test/symb_eval/comp/alias_array_ok.good | 2 +- crux-mir-comp/test/symb_eval/comp/alias_bad.good | 4 ++-- crux-mir-comp/test/symb_eval/comp/alias_ok.good | 2 +- crux-mir-comp/test/symb_eval/comp/override_test_indep.good | 2 +- crux-mir-comp/test/symb_eval/comp/ptr_offset.good | 2 +- crux-mir-comp/test/symb_eval/comp/ptr_offset_rev.good | 2 +- crux-mir-comp/test/symb_eval/comp/spec_array.good | 2 +- crux-mir-comp/test/symb_eval/comp/spec_box.good | 2 +- crux-mir-comp/test/symb_eval/comp/spec_immut_cell.good | 2 +- crux-mir-comp/test/symb_eval/comp/spec_mut.good | 2 +- crux-mir-comp/test/symb_eval/comp/spec_struct.good | 2 +- crux-mir-comp/test/symb_eval/comp/spec_tuple.good | 2 +- 14 files changed, 16 insertions(+), 16 deletions(-) diff --git a/crux-mir-comp/test/symb_eval/comp/alias_array_bad.good b/crux-mir-comp/test/symb_eval/comp/alias_array_bad.good index f59063e820..712babf9ff 100644 --- a/crux-mir-comp/test/symb_eval/comp/alias_array_bad.good +++ b/crux-mir-comp/test/symb_eval/comp/alias_array_bad.good @@ -6,10 +6,10 @@ failures: ---- alias_array_bad/3a1fbbbh::use_f[0] counterexamples ---- Failure for test/symb_eval/comp/alias_array_bad.rs:45:14: 45:16: error: in alias_array_bad/3a1fbbbh::use_f[0] references AllocIndex 0 and AllocIndex 1 must not overlap -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/comp/alias_array_bad.rs:46:5: 46:38: error: in alias_array_bad/3a1fbbbh::use_f[0] +Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_array_bad.rs:46:5: 46:38: error: in alias_array_bad/3a1fbbbh::use_f[0] MIR assertion at test/symb_eval/comp/alias_array_bad.rs:46:5: 0 < b[0].get() -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/comp/alias_array_bad.rs:47:5: 47:39: error: in alias_array_bad/3a1fbbbh::use_f[0] +Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_array_bad.rs:47:5: 47:39: error: in alias_array_bad/3a1fbbbh::use_f[0] MIR assertion at test/symb_eval/comp/alias_array_bad.rs:47:5: b[0].get() < 10 diff --git a/crux-mir-comp/test/symb_eval/comp/alias_array_bad2.good b/crux-mir-comp/test/symb_eval/comp/alias_array_bad2.good index 10134f2923..7a66ff6911 100644 --- a/crux-mir-comp/test/symb_eval/comp/alias_array_bad2.good +++ b/crux-mir-comp/test/symb_eval/comp/alias_array_bad2.good @@ -6,7 +6,7 @@ failures: ---- alias_array_bad2/3a1fbbbh::use_f[0] counterexamples ---- Failure for test/symb_eval/comp/alias_array_bad2.rs:45:14: 45:16: error: in alias_array_bad2/3a1fbbbh::use_f[0] references AllocIndex 0 and AllocIndex 1 must not overlap -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/comp/alias_array_bad2.rs:47:5: 47:39: error: in alias_array_bad2/3a1fbbbh::use_f[0] +Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_array_bad2.rs:47:5: 47:39: error: in alias_array_bad2/3a1fbbbh::use_f[0] MIR assertion at test/symb_eval/comp/alias_array_bad2.rs:47:5: b[0].get() < 10 diff --git a/crux-mir-comp/test/symb_eval/comp/alias_array_ok.good b/crux-mir-comp/test/symb_eval/comp/alias_array_ok.good index 2eb36cf612..ac20b5a3ee 100644 --- a/crux-mir-comp/test/symb_eval/comp/alias_array_ok.good +++ b/crux-mir-comp/test/symb_eval/comp/alias_array_ok.good @@ -4,7 +4,7 @@ test alias_array_ok/3a1fbbbh::use_f[0]: FAILED failures: ---- alias_array_ok/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/comp/alias_array_ok.rs:48:5: 48:39: error: in alias_array_ok/3a1fbbbh::use_f[0] +Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_array_ok.rs:48:5: 48:39: error: in alias_array_ok/3a1fbbbh::use_f[0] MIR assertion at test/symb_eval/comp/alias_array_ok.rs:48:5: b[0].get() < 10 diff --git a/crux-mir-comp/test/symb_eval/comp/alias_bad.good b/crux-mir-comp/test/symb_eval/comp/alias_bad.good index 53546b264c..4a785dc86e 100644 --- a/crux-mir-comp/test/symb_eval/comp/alias_bad.good +++ b/crux-mir-comp/test/symb_eval/comp/alias_bad.good @@ -6,10 +6,10 @@ failures: ---- alias_bad/3a1fbbbh::use_f[0] counterexamples ---- Failure for test/symb_eval/comp/alias_bad.rs:45:11: 45:13: error: in alias_bad/3a1fbbbh::use_f[0] references AllocIndex 0 and AllocIndex 1 must not overlap -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/comp/alias_bad.rs:46:5: 46:35: error: in alias_bad/3a1fbbbh::use_f[0] +Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_bad.rs:46:5: 46:35: error: in alias_bad/3a1fbbbh::use_f[0] MIR assertion at test/symb_eval/comp/alias_bad.rs:46:5: 0 < b.get() -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/comp/alias_bad.rs:47:5: 47:36: error: in alias_bad/3a1fbbbh::use_f[0] +Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_bad.rs:47:5: 47:36: error: in alias_bad/3a1fbbbh::use_f[0] MIR assertion at test/symb_eval/comp/alias_bad.rs:47:5: b.get() < 10 diff --git a/crux-mir-comp/test/symb_eval/comp/alias_ok.good b/crux-mir-comp/test/symb_eval/comp/alias_ok.good index d090a35332..c66fbe145a 100644 --- a/crux-mir-comp/test/symb_eval/comp/alias_ok.good +++ b/crux-mir-comp/test/symb_eval/comp/alias_ok.good @@ -4,7 +4,7 @@ test alias_ok/3a1fbbbh::use_f[0]: FAILED failures: ---- alias_ok/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/comp/alias_ok.rs:49:5: 49:36: error: in alias_ok/3a1fbbbh::use_f[0] +Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_ok.rs:49:5: 49:36: error: in alias_ok/3a1fbbbh::use_f[0] MIR assertion at test/symb_eval/comp/alias_ok.rs:49:5: b.get() < 10 diff --git a/crux-mir-comp/test/symb_eval/comp/override_test_indep.good b/crux-mir-comp/test/symb_eval/comp/override_test_indep.good index e9963892cd..0ff68a7c37 100644 --- a/crux-mir-comp/test/symb_eval/comp/override_test_indep.good +++ b/crux-mir-comp/test/symb_eval/comp/override_test_indep.good @@ -6,7 +6,7 @@ test override_test_indep/3a1fbbbh::use_f3[0]: ok failures: ---- override_test_indep/3a1fbbbh::use_f2[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/comp/override_test_indep.rs:57:5: 57:30: error: in override_test_indep/3a1fbbbh::use_f2[0] +Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/override_test_indep.rs:57:5: 57:30: error: in override_test_indep/3a1fbbbh::use_f2[0] MIR assertion at test/symb_eval/comp/override_test_indep.rs:57:5: d < 10 diff --git a/crux-mir-comp/test/symb_eval/comp/ptr_offset.good b/crux-mir-comp/test/symb_eval/comp/ptr_offset.good index 80f6868fb4..24abea7c73 100644 --- a/crux-mir-comp/test/symb_eval/comp/ptr_offset.good +++ b/crux-mir-comp/test/symb_eval/comp/ptr_offset.good @@ -4,7 +4,7 @@ test ptr_offset/3a1fbbbh::use_f[0]: FAILED failures: ---- ptr_offset/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/comp/ptr_offset.rs:64:5: 64:31: error: in ptr_offset/3a1fbbbh::use_f[0] +Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/ptr_offset.rs:64:5: 64:31: error: in ptr_offset/3a1fbbbh::use_f[0] MIR assertion at test/symb_eval/comp/ptr_offset.rs:64:5: b2 < 10 diff --git a/crux-mir-comp/test/symb_eval/comp/ptr_offset_rev.good b/crux-mir-comp/test/symb_eval/comp/ptr_offset_rev.good index 65d3ec6180..a4f3e1443a 100644 --- a/crux-mir-comp/test/symb_eval/comp/ptr_offset_rev.good +++ b/crux-mir-comp/test/symb_eval/comp/ptr_offset_rev.good @@ -4,7 +4,7 @@ test ptr_offset_rev/3a1fbbbh::use_f[0]: FAILED failures: ---- ptr_offset_rev/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/comp/ptr_offset_rev.rs:64:5: 64:31: error: in ptr_offset_rev/3a1fbbbh::use_f[0] +Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/ptr_offset_rev.rs:64:5: 64:31: error: in ptr_offset_rev/3a1fbbbh::use_f[0] MIR assertion at test/symb_eval/comp/ptr_offset_rev.rs:64:5: b2 < 10 diff --git a/crux-mir-comp/test/symb_eval/comp/spec_array.good b/crux-mir-comp/test/symb_eval/comp/spec_array.good index 6405c160fb..ed999d49cc 100644 --- a/crux-mir-comp/test/symb_eval/comp/spec_array.good +++ b/crux-mir-comp/test/symb_eval/comp/spec_array.good @@ -4,7 +4,7 @@ test spec_array/3a1fbbbh::use_f[0]: FAILED failures: ---- spec_array/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/comp/spec_array.rs:43:5: 43:30: error: in spec_array/3a1fbbbh::use_f[0] +Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_array.rs:43:5: 43:30: error: in spec_array/3a1fbbbh::use_f[0] MIR assertion at test/symb_eval/comp/spec_array.rs:43:5: d < 10 diff --git a/crux-mir-comp/test/symb_eval/comp/spec_box.good b/crux-mir-comp/test/symb_eval/comp/spec_box.good index 67928985e8..a2c48769a8 100644 --- a/crux-mir-comp/test/symb_eval/comp/spec_box.good +++ b/crux-mir-comp/test/symb_eval/comp/spec_box.good @@ -4,7 +4,7 @@ test spec_box/3a1fbbbh::use_f[0]: FAILED failures: ---- spec_box/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/comp/spec_box.rs:58:5: 58:30: error: in spec_box/3a1fbbbh::use_f[0] +Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_box.rs:58:5: 58:30: error: in spec_box/3a1fbbbh::use_f[0] MIR assertion at test/symb_eval/comp/spec_box.rs:58:5: d < 10 diff --git a/crux-mir-comp/test/symb_eval/comp/spec_immut_cell.good b/crux-mir-comp/test/symb_eval/comp/spec_immut_cell.good index f23ec8c216..748c1cfaf1 100644 --- a/crux-mir-comp/test/symb_eval/comp/spec_immut_cell.good +++ b/crux-mir-comp/test/symb_eval/comp/spec_immut_cell.good @@ -4,7 +4,7 @@ test spec_immut_cell/3a1fbbbh::use_f[0]: FAILED failures: ---- spec_immut_cell/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/comp/spec_immut_cell.rs:68:5: 68:36: error: in spec_immut_cell/3a1fbbbh::use_f[0] +Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_immut_cell.rs:68:5: 68:36: error: in spec_immut_cell/3a1fbbbh::use_f[0] MIR assertion at test/symb_eval/comp/spec_immut_cell.rs:68:5: d.get() < 10 diff --git a/crux-mir-comp/test/symb_eval/comp/spec_mut.good b/crux-mir-comp/test/symb_eval/comp/spec_mut.good index 561957ce9c..8f77f8a347 100644 --- a/crux-mir-comp/test/symb_eval/comp/spec_mut.good +++ b/crux-mir-comp/test/symb_eval/comp/spec_mut.good @@ -4,7 +4,7 @@ test spec_mut/3a1fbbbh::use_f[0]: FAILED failures: ---- spec_mut/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/comp/spec_mut.rs:61:5: 61:30: error: in spec_mut/3a1fbbbh::use_f[0] +Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_mut.rs:61:5: 61:30: error: in spec_mut/3a1fbbbh::use_f[0] MIR assertion at test/symb_eval/comp/spec_mut.rs:61:5: d < 10 diff --git a/crux-mir-comp/test/symb_eval/comp/spec_struct.good b/crux-mir-comp/test/symb_eval/comp/spec_struct.good index c2b4a50cf5..14c90992be 100644 --- a/crux-mir-comp/test/symb_eval/comp/spec_struct.good +++ b/crux-mir-comp/test/symb_eval/comp/spec_struct.good @@ -4,7 +4,7 @@ test spec_struct/3a1fbbbh::use_f[0]: FAILED failures: ---- spec_struct/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/comp/spec_struct.rs:51:5: 51:30: error: in spec_struct/3a1fbbbh::use_f[0] +Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_struct.rs:51:5: 51:30: error: in spec_struct/3a1fbbbh::use_f[0] MIR assertion at test/symb_eval/comp/spec_struct.rs:51:5: d < 10 diff --git a/crux-mir-comp/test/symb_eval/comp/spec_tuple.good b/crux-mir-comp/test/symb_eval/comp/spec_tuple.good index 15d5533b9e..40b8421d77 100644 --- a/crux-mir-comp/test/symb_eval/comp/spec_tuple.good +++ b/crux-mir-comp/test/symb_eval/comp/spec_tuple.good @@ -4,7 +4,7 @@ test spec_tuple/3a1fbbbh::use_f[0]: FAILED failures: ---- spec_tuple/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/comp/spec_tuple.rs:55:5: 55:30: error: in spec_tuple/3a1fbbbh::use_f[0] +Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_tuple.rs:55:5: 55:30: error: in spec_tuple/3a1fbbbh::use_f[0] MIR assertion at test/symb_eval/comp/spec_tuple.rs:55:5: d < 10 From 953aa7c9f83d5f0072793ebf997390e93be7c989 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Wed, 21 Apr 2021 10:51:27 -0700 Subject: [PATCH 12/34] move orOverride helper into Mir.Language module --- crux-mir-comp/exe/Main.hs | 9 +-------- deps/crucible | 2 +- 2 files changed, 2 insertions(+), 9 deletions(-) diff --git a/crux-mir-comp/exe/Main.hs b/crux-mir-comp/exe/Main.hs index f1973600fd..639563ca9e 100644 --- a/crux-mir-comp/exe/Main.hs +++ b/crux-mir-comp/exe/Main.hs @@ -8,11 +8,4 @@ import Mir.Cryptol (cryptolOverrides) main :: IO () main = Mir.mainWithExtraOverrides $ - compositionalOverrides `orOverride` cryptolOverrides - -orOverride :: - Mir.BindExtraOverridesFn -> Mir.BindExtraOverridesFn -> Mir.BindExtraOverridesFn -orOverride f g symOnline cs name cfg = - case f symOnline cs name cfg of - Just x -> Just x - Nothing -> g symOnline cs name cfg + compositionalOverrides `Mir.orOverride` cryptolOverrides diff --git a/deps/crucible b/deps/crucible index 2e0a5dc194..a1010e6ab5 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 2e0a5dc194a947fdb63fba9135bf8c2a797561d0 +Subproject commit a1010e6ab582d6da2d2c3793ef4b312e2f762811 From 0e01a72fea977d4d5856323a1771fef7358ec933 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Wed, 21 Apr 2021 11:11:33 -0700 Subject: [PATCH 13/34] crux-mir-comp: add cryptol test cases --- crux-mir-comp/test/Test.hs | 7 ++- .../test/symb_eval/cryptol/basic.cry | 14 ++++++ .../test/symb_eval/cryptol/basic_add.good | 3 ++ .../test/symb_eval/cryptol/basic_add.rs | 19 ++++++++ .../symb_eval/cryptol/basic_add_bits.good | 3 ++ .../test/symb_eval/cryptol/basic_add_bits.rs | 43 +++++++++++++++++++ .../symb_eval/cryptol/basic_array_arg.good | 3 ++ .../test/symb_eval/cryptol/basic_array_arg.rs | 19 ++++++++ .../symb_eval/cryptol/basic_array_ret.good | 3 ++ .../test/symb_eval/cryptol/basic_array_ret.rs | 19 ++++++++ .../cryptol/basic_err_array_size.good | 9 ++++ .../symb_eval/cryptol/basic_err_array_size.rs | 9 ++++ .../symb_eval/cryptol/basic_err_bv_size.good | 9 ++++ .../symb_eval/cryptol/basic_err_bv_size.rs | 9 ++++ .../cryptol/basic_err_fewer_args.good | 9 ++++ .../symb_eval/cryptol/basic_err_fewer_args.rs | 9 ++++ .../symb_eval/cryptol/basic_err_mismatch.good | 9 ++++ .../symb_eval/cryptol/basic_err_mismatch.rs | 9 ++++ .../cryptol/basic_err_more_args.good | 9 ++++ .../symb_eval/cryptol/basic_err_more_args.rs | 9 ++++ .../cryptol/basic_err_tuple_size.good | 9 ++++ .../symb_eval/cryptol/basic_err_tuple_size.rs | 9 ++++ .../symb_eval/cryptol/basic_tuple_arg.good | 3 ++ .../test/symb_eval/cryptol/basic_tuple_arg.rs | 19 ++++++++ .../symb_eval/cryptol/basic_tuple_ret.good | 3 ++ .../test/symb_eval/cryptol/basic_tuple_ret.rs | 19 ++++++++ 26 files changed, 284 insertions(+), 1 deletion(-) create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic.cry create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_add.good create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_add.rs create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_add_bits.good create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_add_bits.rs create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_array_arg.good create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_array_arg.rs create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_array_ret.good create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_array_ret.rs create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.good create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.rs create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.good create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.rs create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.good create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.rs create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.good create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.rs create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.good create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.rs create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.good create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.rs create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_tuple_arg.good create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_tuple_arg.rs create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_tuple_ret.good create mode 100644 crux-mir-comp/test/symb_eval/cryptol/basic_tuple_ret.rs diff --git a/crux-mir-comp/test/Test.hs b/crux-mir-comp/test/Test.hs index 66fc7c8426..8764c69ddb 100644 --- a/crux-mir-comp/test/Test.hs +++ b/crux-mir-comp/test/Test.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE ImplicitParams #-} {-# Language OverloadedStrings #-} @@ -26,6 +27,7 @@ import Test.Tasty.ExpectedFailure (expectFailBecause) import qualified Mir.Language as Mir import qualified Mir.Compositional as Mir +import qualified Mir.Cryptol as Mir import qualified Crux as Crux import qualified Crux.Config.Common as Crux @@ -88,8 +90,11 @@ runCrux rustFile outHandle mode = do Mir.defaultMirOptions { Mir.printResultOnly = (mode == RcmConcrete), Mir.defaultRlibsDir = "../deps/crucible/crux-mir/rlibs" }) let ?outputConfig = Crux.OutputConfig False outHandle outHandle quiet - _exitCode <- Mir.runTestsWithExtraOverrides Mir.compositionalOverrides options + _exitCode <- Mir.runTestsWithExtraOverrides overrides options return () + where + overrides :: Mir.BindExtraOverridesFn + overrides = Mir.compositionalOverrides `Mir.orOverride` Mir.cryptolOverrides getOutputDir :: FilePath -> FilePath getOutputDir rustFile = takeDirectory rustFile "out" diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic.cry b/crux-mir-comp/test/symb_eval/cryptol/basic.cry new file mode 100644 index 0000000000..3a556673f9 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic.cry @@ -0,0 +1,14 @@ +addByte : [8] -> [8] -> [8] +addByte x y = x + y + +tupleArg : ([8], [8]) -> [8] +tupleArg (x, y) = x + y + +tupleRet : [8] -> [8] -> ([8], [8]) +tupleRet x y = (x + y, x - y) + +arrayArg : [2][8] -> [8] +arrayArg [x, y] = x + y + +arrayRet : [8] -> [8] -> [2][8] +arrayRet x y = [x + y, x - y] diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_add.good b/crux-mir-comp/test/symb_eval/cryptol/basic_add.good new file mode 100644 index 0000000000..d2dfb839b9 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_add.good @@ -0,0 +1,3 @@ +test basic_add/3a1fbbbh::test[0]: ok + +[Crux] Overall status: Valid. diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_add.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_add.rs new file mode 100644 index 0000000000..5fa1e20cca --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_add.rs @@ -0,0 +1,19 @@ +extern crate crucible; +use crucible::*; + +const PATH: &str = "test/symb_eval/cryptol/basic.cry"; + +#[crux_test] +fn test() { + let x = u8::symbolic("x"); + let y = u8::symbolic("y"); + let expected = x.wrapping_add(y); + + let f: fn(u8, u8) -> u8 = cryptol::load(PATH, "addByte"); + let actual = f(x, y); + + crucible_assert!( + actual == expected, + "f({}, {}) = {:?}, but expected {:?}", x, y, actual, expected, + ); +} diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_add_bits.good b/crux-mir-comp/test/symb_eval/cryptol/basic_add_bits.good new file mode 100644 index 0000000000..a351fcb99a --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_add_bits.good @@ -0,0 +1,3 @@ +test basic_add_bits/3a1fbbbh::test[0]: ok + +[Crux] Overall status: Valid. diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_add_bits.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_add_bits.rs new file mode 100644 index 0000000000..804a82d54c --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_add_bits.rs @@ -0,0 +1,43 @@ +extern crate crucible; +use crucible::*; + +const PATH: &str = "test/symb_eval/cryptol/basic.cry"; + +fn to_bits(x: u8) -> [bool; 8] { + [ + x & (1 << 7) != 0, + x & (1 << 6) != 0, + x & (1 << 5) != 0, + x & (1 << 4) != 0, + x & (1 << 3) != 0, + x & (1 << 2) != 0, + x & (1 << 1) != 0, + x & (1 << 0) != 0, + ] +} + +fn from_bits(x: [bool; 8]) -> u8 { + ((x[0] as u8) << 7) | + ((x[1] as u8) << 6) | + ((x[2] as u8) << 5) | + ((x[3] as u8) << 4) | + ((x[4] as u8) << 3) | + ((x[5] as u8) << 2) | + ((x[6] as u8) << 1) | + ((x[7] as u8) << 0) +} + +#[crux_test] +fn test() { + let x = u8::symbolic("x"); + let y = u8::symbolic("y"); + let expected = x.wrapping_add(y); + + let f: fn([bool; 8], [bool; 8]) -> [bool; 8] = cryptol::load(PATH, "addByte"); + let actual = from_bits(f(to_bits(x), to_bits(y))); + + crucible_assert!( + actual == expected, + "f({}, {}) = {:?}, but expected {:?}", x, y, actual, expected, + ); +} diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_array_arg.good b/crux-mir-comp/test/symb_eval/cryptol/basic_array_arg.good new file mode 100644 index 0000000000..4ab83dea7e --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_array_arg.good @@ -0,0 +1,3 @@ +test basic_array_arg/3a1fbbbh::test[0]: ok + +[Crux] Overall status: Valid. diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_array_arg.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_array_arg.rs new file mode 100644 index 0000000000..1308d07a99 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_array_arg.rs @@ -0,0 +1,19 @@ +extern crate crucible; +use crucible::*; + +const PATH: &str = "test/symb_eval/cryptol/basic.cry"; + +#[crux_test] +fn test() { + let x = u8::symbolic("x"); + let y = u8::symbolic("y"); + let expected = x.wrapping_add(y); + + let f: fn([u8; 2]) -> u8 = cryptol::load(PATH, "arrayArg"); + let actual = f([x, y]); + + crucible_assert!( + actual == expected, + "f([{}, {}]) = {:?}, but expected {:?}", x, y, actual, expected, + ); +} diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_array_ret.good b/crux-mir-comp/test/symb_eval/cryptol/basic_array_ret.good new file mode 100644 index 0000000000..bad259e0e4 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_array_ret.good @@ -0,0 +1,3 @@ +test basic_array_ret/3a1fbbbh::test[0]: ok + +[Crux] Overall status: Valid. diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_array_ret.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_array_ret.rs new file mode 100644 index 0000000000..cafdf9aa68 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_array_ret.rs @@ -0,0 +1,19 @@ +extern crate crucible; +use crucible::*; + +const PATH: &str = "test/symb_eval/cryptol/basic.cry"; + +#[crux_test] +fn test() { + let x = u8::symbolic("x"); + let y = u8::symbolic("y"); + let expected = [x.wrapping_add(y), x.wrapping_sub(y)]; + + let f: fn(u8, u8) -> [u8; 2] = cryptol::load(PATH, "arrayRet"); + let actual = f(x, y); + + crucible_assert!( + actual == expected, + "f({}, {}) = {:?}, but expected {:?}", x, y, actual, expected, + ); +} diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.good b/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.good new file mode 100644 index 0000000000..e51bd6c38a --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.good @@ -0,0 +1,9 @@ +test basic_err_array_size/3a1fbbbh::test[0]: FAILED + +failures: + +---- basic_err_array_size/3a1fbbbh::test[0] counterexamples ---- +Failure for test/symb_eval/cryptol/basic_err_array_size.rs:8:52: 8:62: error: in basic_err_array_size/3a1fbbbh::test[0] +error loading "arrayArg": type mismatch in argument 0: Cryptol type [2][8] does not match Rust type u8: array length 2 does not match 3 + +[Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.rs new file mode 100644 index 0000000000..5e56059d7e --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.rs @@ -0,0 +1,9 @@ +extern crate crucible; +use crucible::*; + +const PATH: &str = "test/symb_eval/cryptol/basic.cry"; + +#[crux_test] +fn test() { + let f: fn([u8; 3]) -> u8 = cryptol::load(PATH, "arrayArg"); +} diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.good b/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.good new file mode 100644 index 0000000000..91e48799df --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.good @@ -0,0 +1,9 @@ +test basic_err_bv_size/3a1fbbbh::test[0]: FAILED + +failures: + +---- basic_err_bv_size/3a1fbbbh::test[0] counterexamples ---- +Failure for test/symb_eval/cryptol/basic_err_bv_size.rs:8:52: 8:61: error: in basic_err_bv_size/3a1fbbbh::test[0] +error loading "addByte": type mismatch in argument 1: Cryptol type [8] does not match Rust type u16: bitvector width 8 does not match 16 + +[Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.rs new file mode 100644 index 0000000000..3a170bba36 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.rs @@ -0,0 +1,9 @@ +extern crate crucible; +use crucible::*; + +const PATH: &str = "test/symb_eval/cryptol/basic.cry"; + +#[crux_test] +fn test() { + let f: fn(u8, u16) -> u8 = cryptol::load(PATH, "addByte"); +} diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.good b/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.good new file mode 100644 index 0000000000..33a1560602 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.good @@ -0,0 +1,9 @@ +test basic_err_fewer_args/3a1fbbbh::test[0]: FAILED + +failures: + +---- basic_err_fewer_args/3a1fbbbh::test[0] counterexamples ---- +Failure for test/symb_eval/cryptol/basic_err_fewer_args.rs:8:55: 8:64: error: in basic_err_fewer_args/3a1fbbbh::test[0] +error loading "addByte": not enough arguments: Cryptol function signature [8] -> [8] -> [8] has 2 arguments, but Rust signature (u8, u8, u8) -> u8 [RustAbi] requires 3 + +[Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.rs new file mode 100644 index 0000000000..51f650131c --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.rs @@ -0,0 +1,9 @@ +extern crate crucible; +use crucible::*; + +const PATH: &str = "test/symb_eval/cryptol/basic.cry"; + +#[crux_test] +fn test() { + let f: fn(u8, u8, u8) -> u8 = cryptol::load(PATH, "addByte"); +} diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.good b/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.good new file mode 100644 index 0000000000..58cf2455e2 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.good @@ -0,0 +1,9 @@ +test basic_err_mismatch/3a1fbbbh::test[0]: FAILED + +failures: + +---- basic_err_mismatch/3a1fbbbh::test[0] counterexamples ---- +Failure for test/symb_eval/cryptol/basic_err_mismatch.rs:8:51: 8:60: error: in basic_err_mismatch/3a1fbbbh::test[0] +error loading "addByte": type mismatch in argument 1: Cryptol type [8] does not match Rust type () + +[Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.rs new file mode 100644 index 0000000000..968dba7fc7 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.rs @@ -0,0 +1,9 @@ +extern crate crucible; +use crucible::*; + +const PATH: &str = "test/symb_eval/cryptol/basic.cry"; + +#[crux_test] +fn test() { + let f: fn(u8, ()) -> u8 = cryptol::load(PATH, "addByte"); +} diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.good b/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.good new file mode 100644 index 0000000000..786dba7433 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.good @@ -0,0 +1,9 @@ +test basic_err_more_args/3a1fbbbh::test[0]: FAILED + +failures: + +---- basic_err_more_args/3a1fbbbh::test[0] counterexamples ---- +Failure for test/symb_eval/cryptol/basic_err_more_args.rs:8:47: 8:56: error: in basic_err_more_args/3a1fbbbh::test[0] +error loading "addByte": type mismatch in return value: Cryptol type [8] -> [8] does not match Rust type u8 + +[Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.rs new file mode 100644 index 0000000000..37ad5da789 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.rs @@ -0,0 +1,9 @@ +extern crate crucible; +use crucible::*; + +const PATH: &str = "test/symb_eval/cryptol/basic.cry"; + +#[crux_test] +fn test() { + let f: fn(u8) -> u8 = cryptol::load(PATH, "addByte"); +} diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.good b/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.good new file mode 100644 index 0000000000..6e7111b5a2 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.good @@ -0,0 +1,9 @@ +test basic_err_tuple_size/3a1fbbbh::test[0]: FAILED + +failures: + +---- basic_err_tuple_size/3a1fbbbh::test[0] counterexamples ---- +Failure for test/symb_eval/cryptol/basic_err_tuple_size.rs:8:57: 8:67: error: in basic_err_tuple_size/3a1fbbbh::test[0] +error loading "tupleArg": type mismatch in argument 0: Cryptol type ([8], [8]) does not match Rust type (u8, u8, u8): tuple size 2 does not match 3 + +[Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.rs new file mode 100644 index 0000000000..265c9f42fe --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.rs @@ -0,0 +1,9 @@ +extern crate crucible; +use crucible::*; + +const PATH: &str = "test/symb_eval/cryptol/basic.cry"; + +#[crux_test] +fn test() { + let f: fn((u8, u8, u8)) -> u8 = cryptol::load(PATH, "tupleArg"); +} diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_arg.good b/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_arg.good new file mode 100644 index 0000000000..d307c9e268 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_arg.good @@ -0,0 +1,3 @@ +test basic_tuple_arg/3a1fbbbh::test[0]: ok + +[Crux] Overall status: Valid. diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_arg.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_arg.rs new file mode 100644 index 0000000000..07755417c1 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_arg.rs @@ -0,0 +1,19 @@ +extern crate crucible; +use crucible::*; + +const PATH: &str = "test/symb_eval/cryptol/basic.cry"; + +#[crux_test] +fn test() { + let x = u8::symbolic("x"); + let y = u8::symbolic("y"); + let expected = x.wrapping_add(y); + + let f: fn((u8, u8)) -> u8 = cryptol::load(PATH, "tupleArg"); + let actual = f((x, y)); + + crucible_assert!( + actual == expected, + "f(({}, {})) = {:?}, but expected {:?}", x, y, actual, expected, + ); +} diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_ret.good b/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_ret.good new file mode 100644 index 0000000000..ec91ffdc8d --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_ret.good @@ -0,0 +1,3 @@ +test basic_tuple_ret/3a1fbbbh::test[0]: ok + +[Crux] Overall status: Valid. diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_ret.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_ret.rs new file mode 100644 index 0000000000..78be5c4e3c --- /dev/null +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_ret.rs @@ -0,0 +1,19 @@ +extern crate crucible; +use crucible::*; + +const PATH: &str = "test/symb_eval/cryptol/basic.cry"; + +#[crux_test] +fn test() { + let x = u8::symbolic("x"); + let y = u8::symbolic("y"); + let expected = (x.wrapping_add(y), x.wrapping_sub(y)); + + let f: fn(u8, u8) -> (u8, u8) = cryptol::load(PATH, "tupleRet"); + let actual = f(x, y); + + crucible_assert!( + actual == expected, + "f({}, {}) = {:?}, but expected {:?}", x, y, actual, expected, + ); +} From bdf4facfcb34ae26e878e7d3f82c8bca20be830f Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Thu, 22 Apr 2021 13:31:09 -0700 Subject: [PATCH 14/34] use new cryptol! macro in cryptol/basic_add test --- crux-mir-comp/test/symb_eval/cryptol/basic_add.rs | 10 ++++++---- deps/crucible | 2 +- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_add.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_add.rs index 5fa1e20cca..196a010def 100644 --- a/crux-mir-comp/test/symb_eval/cryptol/basic_add.rs +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_add.rs @@ -1,16 +1,18 @@ extern crate crucible; use crucible::*; -const PATH: &str = "test/symb_eval/cryptol/basic.cry"; +cryptol! { + path "test/symb_eval/cryptol/basic.cry"; + + fn add_byte(x: u8, y: u8) -> u8 = "addByte"; +} #[crux_test] fn test() { let x = u8::symbolic("x"); let y = u8::symbolic("y"); let expected = x.wrapping_add(y); - - let f: fn(u8, u8) -> u8 = cryptol::load(PATH, "addByte"); - let actual = f(x, y); + let actual = add_byte(x, y); crucible_assert!( actual == expected, diff --git a/deps/crucible b/deps/crucible index a1010e6ab5..ae70abc620 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit a1010e6ab582d6da2d2c3793ef4b312e2f762811 +Subproject commit ae70abc620f92c2bed0d630d732f38395ed85645 From debebf988a59a3b32819072011717ba53d7c1110 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Mon, 26 Apr 2021 10:15:13 -0700 Subject: [PATCH 15/34] bump crucible for rotate_left/right intrinsics --- deps/crucible | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/crucible b/deps/crucible index ae70abc620..079772062e 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit ae70abc620f92c2bed0d630d732f38395ed85645 +Subproject commit 079772062ed5ed60c0f8381bfce992afece800b0 From 4bc25de4f2d132a993b7247098f1046c16606d9c Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Mon, 26 Apr 2021 16:49:51 -0700 Subject: [PATCH 16/34] new cryptol! macro implementation with no global variables --- crux-mir-comp/src/Mir/Cryptol.hs | 169 ++++++++++++++++++++++++------- deps/crucible | 2 +- 2 files changed, 135 insertions(+), 36 deletions(-) diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index 97c579b5d9..fd7b5057db 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -1,8 +1,10 @@ {-# Language DataKinds #-} {-# Language GADTs #-} {-# Language ImplicitParams #-} +{-# Language KindSignatures #-} {-# Language OverloadedStrings #-} {-# Language PatternSynonyms #-} +{-# Language PolyKinds #-} {-# Language RankNTypes #-} {-# Language ScopedTypeVariables #-} {-# Language TypeApplications #-} @@ -24,7 +26,7 @@ import Data.String (fromString) import Data.Text (Text) import qualified Data.Text as Text -import Data.Parameterized.Context (pattern Empty, pattern (:>)) +import Data.Parameterized.Context (pattern Empty, pattern (:>), Assignment) import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.NatRepr import Data.Parameterized.TraversableFC @@ -43,7 +45,8 @@ import Crux import Crux.Types import Mir.DefId -import Mir.Generator (CollectionState, collection) +import Mir.Generator (CollectionState, collection, MirHandle(..)) +import qualified Mir.Generator as M import Mir.Intrinsics import qualified Mir.Mir as M import qualified Mir.PP as M @@ -87,6 +90,30 @@ cryptolOverrides _symOnline cs name cfg RegMap (Empty :> RegEntry _tpr modulePathStr :> RegEntry _tpr' nameStr) <- getOverrideArgs cryptolLoad (cs ^. collection) sig (cfgReturnType cfg) modulePathStr nameStr + | (normDefId "crucible::cryptol::override_" <> "::_inst") `Text.isPrefixOf` name + , Empty + :> UnitRepr + :> MirSliceRepr (BVRepr (testEquality (knownNat @8) -> Just Refl)) + :> MirSliceRepr (BVRepr (testEquality (knownNat @8) -> Just Refl)) + <- cfgArgTypes cfg + , UnitRepr <- cfgReturnType cfg + = Just $ bindFnHandle (cfgHandle cfg) $ UseOverride $ + mkOverride' "cryptol_override_" UnitRepr $ do + let tyArg = cs ^? collection . M.intrinsics . ix (textId name) . + M.intrInst . M.inSubsts . _Wrapped . ix 0 + fnDefId <- case tyArg of + Just (M.TyFnDef defId) -> return defId + _ -> error $ "expected TyFnDef argument, but got " ++ show tyArg + mh <- case cs ^? M.handleMap . ix fnDefId of + Just mh -> return mh + _ -> error $ "failed to get function definition for " ++ show fnDefId + + RegMap (Empty + :> RegEntry _ () + :> RegEntry _tpr modulePathStr + :> RegEntry _tpr' nameStr) <- getOverrideArgs + cryptolOverride (cs ^. collection) mh modulePathStr nameStr + | otherwise = Nothing @@ -100,15 +127,83 @@ cryptolLoad :: RegValue sym (MirSlice (BVType 8)) -> OverrideSim (p sym) sym MIR rtp a r (RegValue sym tp) cryptolLoad col sig (FunctionHandleRepr argsCtx retTpr) modulePathStr nameStr = do - modulePath <- getString modulePathStr >>= \x -> case x of - Just s -> return $ Text.unpack s - Nothing -> fail "cryptol::load module path must not be symbolic" - name <- getString nameStr >>= \x -> case x of - Just s -> return $ Text.unpack s - Nothing -> fail "cryptol::load function name must not be symbolic" + modulePath <- loadString modulePathStr "cryptol::load module path" + name <- loadString nameStr "cryptol::load function name" + LoadedCryptolFunc argShps retShp run <- loadCryptolFunc col sig modulePath name + + let argsCtx' = fmapFC shapeType argShps + let retTpr' = shapeType retShp + (Refl, Refl) <- case (testEquality argsCtx argsCtx', testEquality retTpr retTpr') of + (Just x, Just y) -> return (x, y) + _ -> fail $ "signature mismatch: " ++ show (argsCtx', retTpr') ++ " != " ++ + show (argsCtx, retTpr) - let argShps = map (tyToShape col) (sig ^. M.fsarg_tys) - let retShp = tyToShapeEq col (sig ^. M.fsreturn_ty) retTpr + halloc <- simHandleAllocator <$> use stateContext + let fnName = "cryptol_" <> modulePath <> "_" <> name + fh <- liftIO $ mkHandle' halloc (fromString $ Text.unpack fnName) argsCtx retTpr + bindFnHandle fh $ UseOverride $ mkOverride' (handleName fh) (handleReturnType fh) $ + run + + return $ HandleFnVal fh + +cryptolLoad _ _ tpr _ _ = fail $ "cryptol::load: bad function type " ++ show tpr + +loadString :: + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => + RegValue sym (MirSlice (BVType 8)) -> + String -> + OverrideSim (p sym) sym MIR rtp a r Text +loadString str desc = getString str >>= \x -> case x of + Just s -> return s + Nothing -> fail $ desc ++ " must not be symbolic" + + +cryptolOverride :: + forall sym p t st fs rtp a r . + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => + M.Collection -> + MirHandle -> + RegValue sym (MirSlice (BVType 8)) -> + RegValue sym (MirSlice (BVType 8)) -> + OverrideSim (p sym) sym MIR rtp a r () +cryptolOverride col (MirHandle _ sig fh) modulePathStr nameStr = do + modulePath <- loadString modulePathStr "cryptol::load module path" + name <- loadString nameStr "cryptol::load function name" + LoadedCryptolFunc argShps retShp run <- loadCryptolFunc col sig modulePath name + + let argsCtx = handleArgTypes fh + let retTpr = handleReturnType fh + let argsCtx' = fmapFC shapeType argShps + let retTpr' = shapeType retShp + (Refl, Refl) <- case (testEquality argsCtx argsCtx', testEquality retTpr retTpr') of + (Just x, Just y) -> return (x, y) + _ -> fail $ "signature mismatch: " ++ show (argsCtx', retTpr') ++ " != " ++ + show (argsCtx, retTpr) + + bindFnHandle fh $ UseOverride $ mkOverride' (handleName fh) (handleReturnType fh) $ + run + + +data LoadedCryptolFunc sym = forall args ret . LoadedCryptolFunc + { _lcfArgs :: Assignment TypeShape args + , _lcfRet :: TypeShape ret + , _lcfRun :: forall p rtp r. + HasModel p => OverrideSim (p sym) sym MIR rtp args r (RegValue sym ret) + } + +-- | Load a Cryptol function, returning an `OverrideSim` action that can be +-- used to run the function. +loadCryptolFunc :: + forall sym p t st fs rtp a r . + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => + M.Collection -> + M.FnSig -> + Text -> + Text -> + OverrideSim (p sym) sym MIR rtp a r (LoadedCryptolFunc sym) +loadCryptolFunc col sig modulePath name = do + Some argShps <- return $ listToCtx $ map (tyToShape col) (sig ^. M.fsarg_tys) + Some retShp <- return $ tyToShape col (sig ^. M.fsreturn_ty) -- TODO share a single SharedContext across all calls sc <- liftIO $ SAW.mkSharedContext @@ -116,36 +211,45 @@ cryptolLoad col sig (FunctionHandleRepr argsCtx retTpr) modulePathStr nameStr = liftIO $ SAW.scLoadCryptolModule sc let ?fileReader = BS.readFile ce <- liftIO $ SAW.initCryptolEnv sc - (m, ce') <- liftIO $ SAW.loadCryptolModule sc ce modulePath - tt <- liftIO $ SAW.lookupCryptolModule m name + (m, _ce') <- liftIO $ SAW.loadCryptolModule sc ce (Text.unpack modulePath) + tt <- liftIO $ SAW.lookupCryptolModule m (Text.unpack name) - case typecheckFnSig sig argShps (Some retShp) (SAW.ttSchema tt) of + case typecheckFnSig sig (toListFC Some argShps) (Some retShp) (SAW.ttSchema tt) of Left err -> fail $ "error loading " ++ show name ++ ": " ++ err Right () -> return () scs <- liftIO $ SAW.newSAWCoreState sc + let fnName = "cryptol_" <> modulePath <> "_" <> name + return $ LoadedCryptolFunc argShps retShp $ + cryptolRun sc scs (Text.unpack fnName) argShps retShp (SAW.ttTerm tt) + where + listToCtx :: forall k (f :: k -> *). [Some f] -> Some (Assignment f) + listToCtx xs = go xs (Some Empty) + where + go :: forall k (f :: k -> *). [Some f] -> Some (Assignment f) -> Some (Assignment f) + go [] acc = acc + go (Some x : xs) (Some acc) = go xs (Some $ acc :> x) + +{- halloc <- simHandleAllocator <$> use stateContext let fnName = "cryptol_" ++ modulePath ++ "_" ++ name fh <- liftIO $ mkHandle' halloc (fromString fnName) argsCtx retTpr bindFnHandle fh $ UseOverride $ mkOverride' (handleName fh) (handleReturnType fh) $ - cryptolRun sc scs fnName argShps retShp (SAW.ttTerm tt) - - return $ HandleFnVal fh +-} -cryptolLoad _ _ tpr _ _ = fail $ "cryptol::load: bad function type " ++ show tpr cryptolRun :: - forall sym p t st fs rtp a r tp . + forall sym p t st fs rtp r args ret . (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => SAW.SharedContext -> SAW.SAWCoreState t -> String -> - [Some TypeShape] -> - TypeShape tp -> + Assignment TypeShape args -> + TypeShape ret -> SAW.Term -> - OverrideSim (p sym) sym MIR rtp a r (RegValue sym tp) + OverrideSim (p sym) sym MIR rtp args r (RegValue sym ret) cryptolRun sc scs name argShps retShp funcTerm = do sym <- getSymInterface @@ -153,22 +257,17 @@ cryptolRun sc scs name argShps retShp funcTerm = do w4VarMapRef <- liftIO $ newIORef (Map.empty :: Map SAW.VarIndex (Some (W4.Expr t))) RegMap argsCtx <- getOverrideArgs - args <- forM (zip argShps (toListFC (\re -> Some re) argsCtx)) $ - \(Some argShp, Some (RegEntry tpr val)) -> do - Refl <- case testEquality (shapeType argShp) tpr of - Just x -> return x - Nothing -> fail $ - "type error: " ++ name ++ " expected argument of type " ++ - show (shapeType argShp) ++ ", but got " ++ show tpr - regToTerm sym sc scs name visitCache w4VarMapRef argShp val - appTerm <- liftIO $ SAW.scApplyAll sc funcTerm args + argTermsCtx <- Ctx.zipWithM + (\shp (RegEntry _ val) -> + Const <$> regToTerm sym sc scs name visitCache w4VarMapRef shp val) + argShps argsCtx + let argTerms = toListFC getConst argTermsCtx + appTerm <- liftIO $ SAW.scApplyAll sc funcTerm argTerms w4VarMap <- liftIO $ readIORef w4VarMapRef rv <- liftIO $ termToReg sym sc w4VarMap appTerm retShp return rv - where - exprToTerm :: forall sym p t st fs tp rtp a r. (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => sym -> @@ -178,7 +277,7 @@ exprToTerm :: forall sym p t st fs tp rtp a r. IORef (Map SAW.VarIndex (Some (W4.Expr t))) -> W4.Expr t tp -> OverrideSim (p sym) sym MIR rtp a r SAW.Term -exprToTerm sym sc scs visitCache w4VarMapRef val = do +exprToTerm sym _sc scs visitCache w4VarMapRef val = do visitExprVars visitCache val $ \var -> do let expr = W4.BoundVarExpr var term <- liftIO $ SAW.toSC sym scs expr @@ -236,7 +335,7 @@ regToTerm sym sc scs name visitCache w4VarMapRef shp rv = go shp rv forM (toList pv) $ \rv -> do rv' <- liftIO $ readMaybeType sym "field" (shapeType shp) rv go shp rv' - goVector shp (MirVector_Array _) = fail $ + goVector _shp (MirVector_Array _) = fail $ "regToTerm: MirVector_Array not supported" shapeToTerm :: forall tp m. @@ -319,6 +418,6 @@ typecheckFnSig fnSig argShps retShp sch@(Cry.Forall [] [] ty) = go 0 argShps ty goOneField desc (OptField shp) ty = goOne desc shp ty goOneField desc (ReqField shp) ty = goOne desc shp ty -typecheckFnSig _ argShps retShp sch = Left $ +typecheckFnSig _ _ _ sch = Left $ "polymorphic Cryptol functions are not supported (got signature: " ++ show (Cry.pp sch) ++ ")" diff --git a/deps/crucible b/deps/crucible index 079772062e..09f7f007f2 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 079772062ed5ed60c0f8381bfce992afece800b0 +Subproject commit 09f7f007f2d419f7da13e33972712a102f8771cd From bf529c9d03c59e7802a47350e0df2b38fe14287e Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Fri, 30 Apr 2021 09:15:18 -0700 Subject: [PATCH 17/34] bump crucible for new crux-mir intrinsics --- deps/crucible | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/crucible b/deps/crucible index 09f7f007f2..432b80781e 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 09f7f007f2d419f7da13e33972712a102f8771cd +Subproject commit 432b80781ec3ab96dacb9c45b560d701936f6b00 From 83a9329c00163ff2fb2eece643f4697196e5a6a4 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Fri, 30 Apr 2021 09:15:40 -0700 Subject: [PATCH 18/34] crux-mir refactor: add Collection argument to tyToRepr --- .../src/Mir/Compositional/Convert.hs | 44 +++++++++++++++++-- crux-mir-comp/src/Mir/Cryptol.hs | 9 +++- deps/crucible | 2 +- 3 files changed, 48 insertions(+), 7 deletions(-) diff --git a/crux-mir-comp/src/Mir/Compositional/Convert.hs b/crux-mir-comp/src/Mir/Compositional/Convert.hs index 083b696370..9f9f26279c 100644 --- a/crux-mir-comp/src/Mir/Compositional/Convert.hs +++ b/crux-mir-comp/src/Mir/Compositional/Convert.hs @@ -6,6 +6,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} -- | Conversions between Crucible `RegValue`s and SAW `Term`s. module Mir.Compositional.Convert @@ -25,6 +26,7 @@ import Data.Parameterized.Some import Data.Parameterized.TraversableFC import Data.Set (Set) import qualified Data.Set as Set +import Data.Vector (Vector) import qualified Data.Vector as V import GHC.Stack (HasCallStack) @@ -35,7 +37,7 @@ import Lang.Crucible.Types import qualified What4.Expr.Builder as W4 import qualified What4.Interface as W4 import qualified What4.Partial as W4 -import qualified What4.SWord as W4 +import qualified What4.SWord as W4 (SWord(..)) import qualified Verifier.SAW.SharedTerm as SAW import qualified Verifier.SAW.Simulator.MonadLazy as SAW @@ -104,9 +106,9 @@ tyToShape col ty = go ty _ -> error $ "tyToShape: " ++ show ty ++ " NYI" goPrim :: M.Ty -> Some TypeShape - goPrim ty | Some tpr <- tyToRepr ty, AsBaseType btpr <- asBaseType tpr = + goPrim ty | Some tpr <- tyToRepr col ty, AsBaseType btpr <- asBaseType tpr = Some $ PrimShape ty btpr - goPrim ty | Some tpr <- tyToRepr ty = + goPrim ty | Some tpr <- tyToRepr col ty = error $ "tyToShape: type " ++ show ty ++ " produced non-primitive type " ++ show tpr goUnit :: M.Ty -> Some TypeShape @@ -134,7 +136,7 @@ tyToShape col ty = go ty goRef :: M.Ty -> M.Ty -> M.Mutability -> Some TypeShape goRef ty ty' _ | isUnsized ty' = error $ "tyToShape: fat pointer " ++ show ty ++ " NYI" - goRef ty ty' _ | Some tpr <- tyToRepr ty' = Some $ RefShape ty ty' tpr + goRef ty ty' _ | Some tpr <- tyToRepr col ty' = Some $ RefShape ty ty' tpr -- | Given a `Ty` and the result of `tyToRepr ty`, produce a `TypeShape` with -- the same index `tp`. Raises an `error` if the `TypeRepr` doesn't match @@ -297,6 +299,13 @@ termToReg sym sc varMap term shp = do (PrimShape _ BaseBoolRepr, SAW.VBool b) -> return b (PrimShape _ (BaseBVRepr w), SAW.VWord (W4.DBV e)) | Just Refl <- testEquality (W4.exprType e) (BaseBVRepr w) -> return e + (PrimShape _ (BaseBVRepr w), SAW.VVector v) + | intValue w == fromIntegral (V.length v) -> do + bits <- forM v $ SAW.force >=> \x -> case x of + SAW.VBool b -> return b + _ -> fail $ "termToReg: type error: need to produce " ++ show (shapeType shp) ++ + ", but simulator returned a vector containing " ++ show x + buildBitVector w bits (TupleShape _ _ flds, _) -> do svs <- tupleToListRev (Ctx.sizeInt $ Ctx.size flds) [] sv goTuple flds svs @@ -350,6 +359,33 @@ termToReg sym sc varMap term shp = do goField (ReqField shp) sv = go shp sv goField (OptField shp) sv = W4.justPartExpr sym <$> go shp sv + -- | Build a bitvector from a vector of bits. The length of the vector is + -- required to match `w`. + buildBitVector :: forall w. (1 <= w) => + NatRepr w -> Vector (W4.Pred sym) -> IO (W4.SymExpr sym (BaseBVType w)) + buildBitVector w v = do + bvs <- mapM (\b -> W4.bvFill sym (knownNat @1) b) $ toList v + case bvs of + [] -> error $ "buildBitVector: expected " ++ show w ++ " bits, but got 0" + (bv : bvs') -> do + Some bv' <- go (knownNat @1) bv bvs' + Refl <- case testEquality (W4.exprType bv') (BaseBVRepr w) of + Just x -> return x + Nothing -> error $ "buildBitVector: expected " ++ show (BaseBVRepr w) ++ + ", but got " ++ show (W4.exprType bv') + return bv' + where + go :: forall w. (1 <= w) => + NatRepr w -> + W4.SymExpr sym (BaseBVType w) -> + [W4.SymExpr sym (BaseBVType 1)] -> + IO (Some (W4.SymExpr sym)) + go _ bv [] = return $ Some bv + go w bv (b : bs) + | LeqProof <- addPrefixIsLeq w (knownNat @1) = do + bv' <- W4.bvConcat sym bv b + go (addNat w (knownNat @1)) bv' bs + -- | Common code for termToExpr and termToReg termToSValue :: forall sym t st fs. (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasCallStack) => diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index fd7b5057db..6bef960fa2 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -34,6 +34,7 @@ import Data.Parameterized.TraversableFC import qualified What4.Expr.Builder as W4 import Cryptol.TypeCheck.AST as Cry +import Cryptol.Utils.Ident as Cry import Cryptol.Utils.PP as Cry import Lang.Crucible.Backend @@ -211,8 +212,12 @@ loadCryptolFunc col sig modulePath name = do liftIO $ SAW.scLoadCryptolModule sc let ?fileReader = BS.readFile ce <- liftIO $ SAW.initCryptolEnv sc - (m, _ce') <- liftIO $ SAW.loadCryptolModule sc ce (Text.unpack modulePath) - tt <- liftIO $ SAW.lookupCryptolModule m (Text.unpack name) + let modName = Cry.textToModName modulePath + ce' <- liftIO $ SAW.importModule sc ce (Right modName) Nothing SAW.PublicAndPrivate Nothing + -- (m, _ce') <- liftIO $ SAW.loadCryptolModule sc ce (Text.unpack modulePath) + -- tt <- liftIO $ SAW.lookupCryptolModule m (Text.unpack name) + tt <- liftIO $ SAW.parseTypedTerm sc ce' $ + SAW.InputText (Text.unpack name) "" 1 1 case typecheckFnSig sig (toListFC Some argShps) (Some retShp) (SAW.ttSchema tt) of Left err -> fail $ "error loading " ++ show name ++ ": " ++ err diff --git a/deps/crucible b/deps/crucible index 432b80781e..e5c768c3c7 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 432b80781ec3ab96dacb9c45b560d701936f6b00 +Subproject commit e5c768c3c7f78f28ccedf454b8d5ef34577f9d79 From 9045db5254788d8204ed53a479e990a62b0d84f8 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Thu, 6 May 2021 16:31:13 -0700 Subject: [PATCH 19/34] repr(transparent) support --- crux-mir-comp/src/Mir/Compositional/Builder.hs | 1 + crux-mir-comp/src/Mir/Compositional/Clobber.hs | 4 ++++ crux-mir-comp/src/Mir/Compositional/Convert.hs | 13 +++++++++---- crux-mir-comp/src/Mir/Compositional/Override.hs | 2 ++ deps/crucible | 2 +- 5 files changed, 17 insertions(+), 5 deletions(-) diff --git a/crux-mir-comp/src/Mir/Compositional/Builder.hs b/crux-mir-comp/src/Mir/Compositional/Builder.hs index 7e83af2fe6..811823a866 100644 --- a/crux-mir-comp/src/Mir/Compositional/Builder.hs +++ b/crux-mir-comp/src/Mir/Compositional/Builder.hs @@ -518,6 +518,7 @@ regToSetup sym p eval shp rv = go shp rv | otherwise = error $ "regToSetup: type error: expected " ++ show shpTpr ++ ", but got Any wrapping " ++ show tpr where shpTpr = StructRepr $ fmapFC fieldShapeType flds + go (TransparentShape _ shp) rv = go shp rv go (RefShape refTy ty' tpr) ref = do partIdxLen <- lift $ mirRef_indexAndLenSim ref optIdxLen <- liftIO $ readPartExprMaybe sym partIdxLen diff --git a/crux-mir-comp/src/Mir/Compositional/Clobber.hs b/crux-mir-comp/src/Mir/Compositional/Clobber.hs index b8707364c0..cbad304fc0 100644 --- a/crux-mir-comp/src/Mir/Compositional/Clobber.hs +++ b/crux-mir-comp/src/Mir/Compositional/Clobber.hs @@ -60,6 +60,7 @@ clobberSymbolic sym loc nameStr shp rv = go shp rv | otherwise = error $ "clobberSymbolic: type error: expected " ++ show shpTpr ++ ", but got Any wrapping " ++ show tpr where shpTpr = StructRepr $ fmapFC fieldShapeType flds + go (TransparentShape _ shp) rv = go shp rv go shp _rv = error $ "clobberSymbolic: " ++ show (shapeType shp) ++ " NYI" goField :: forall tp. FieldShape tp -> RegValue' sym tp -> @@ -93,6 +94,8 @@ clobberImmutSymbolic sym loc nameStr shp rv = go shp rv MirVector_Array _ -> error $ "clobberSymbolic: MirVector_Array is unsupported" go shp@(StructShape (CTyUnsafeCell _) _ _) rv = clobberSymbolic sym loc nameStr shp rv + go shp@(TransparentShape (CTyUnsafeCell _) _) rv = + clobberSymbolic sym loc nameStr shp rv go (TupleShape _ _ flds) rvs = Ctx.zipWithM goField flds rvs go (StructShape _ _ flds) (AnyValue tpr rvs) @@ -100,6 +103,7 @@ clobberImmutSymbolic sym loc nameStr shp rv = go shp rv | otherwise = error $ "clobberSymbolic: type error: expected " ++ show shpTpr ++ ", but got Any wrapping " ++ show tpr where shpTpr = StructRepr $ fmapFC fieldShapeType flds + go (TransparentShape _ shp) rv = go shp rv -- Since this ref is in immutable memory, whatever behavior we're -- approximating with this clobber can't possibly modify it. go (RefShape _ _ _tpr) rv = return rv diff --git a/crux-mir-comp/src/Mir/Compositional/Convert.hs b/crux-mir-comp/src/Mir/Compositional/Convert.hs index 9f9f26279c..03d925fed0 100644 --- a/crux-mir-comp/src/Mir/Compositional/Convert.hs +++ b/crux-mir-comp/src/Mir/Compositional/Convert.hs @@ -47,7 +47,7 @@ import qualified Verifier.SAW.Simulator.What4 as SAW import Mir.Intrinsics import qualified Mir.Mir as M -import Mir.TransTy (tyToRepr, canInitialize, isUnsized) +import Mir.TransTy (tyToRepr, canInitialize, isUnsized, reprTransparentFieldTy) -- | TypeShape is used to classify MIR `Ty`s and their corresponding @@ -68,6 +68,7 @@ data TypeShape (tp :: CrucibleType) where TupleShape :: M.Ty -> [M.Ty] -> Assignment FieldShape ctx -> TypeShape (StructType ctx) ArrayShape :: M.Ty -> M.Ty -> TypeShape tp -> TypeShape (MirVectorType tp) StructShape :: M.Ty -> [M.Ty] -> Assignment FieldShape ctx -> TypeShape AnyType + TransparentShape :: M.Ty -> TypeShape tp -> TypeShape tp -- | Note that RefShape contains only a TypeRepr for the pointee type, not -- a TypeShape. None of our operations need to recurse inside pointers, -- and also this saves us from some infinite recursion. @@ -98,8 +99,10 @@ tyToShape col ty = go ty M.TyFnDef _ -> goUnit ty M.TyArray ty' _ | Some shp <- go ty' -> Some $ ArrayShape ty ty' shp M.TyAdt nm _ _ -> case Map.lookup nm (col ^. M.adts) of - Just (M.Adt _ M.Struct [v] _ _) -> goStruct ty (v ^.. M.vfields . each . M.fty) - Just (M.Adt _ ak _ _ _) -> error $ "tyToShape: AdtKind " ++ show ak ++ " NYI" + Just adt | Just ty' <- reprTransparentFieldTy col adt -> + mapSome (TransparentShape ty) $ go ty' + Just (M.Adt _ M.Struct [v] _ _ _ _) -> goStruct ty (v ^.. M.vfields . each . M.fty) + Just (M.Adt _ ak _ _ _ _ _) -> error $ "tyToShape: AdtKind " ++ show ak ++ " NYI" Nothing -> error $ "tyToShape: bad adt: " ++ show ty M.TyRef ty' mutbl -> goRef ty ty' mutbl M.TyRawPtr ty' mutbl -> goRef ty ty' mutbl @@ -129,7 +132,7 @@ tyToShape col ty = go ty loop (ty:tys) flds | Some fld <- goField ty = loop tys (flds :> fld) goField :: M.Ty -> Some FieldShape - goField ty | Some shp <- go ty = case canInitialize ty of + goField ty | Some shp <- go ty = case canInitialize col ty of True -> Some $ ReqField shp False -> Some $ OptField shp @@ -158,6 +161,7 @@ shapeType shp = go shp go (TupleShape _ _ flds) = StructRepr $ fmapFC fieldShapeType flds go (ArrayShape _ _ shp) = MirVectorRepr $ shapeType shp go (StructShape _ _ _flds) = AnyRepr + go (TransparentShape _ shp) = go shp go (RefShape _ _ tpr) = MirReferenceRepr tpr fieldShapeType :: FieldShape tp -> TypeRepr tp @@ -170,6 +174,7 @@ shapeMirTy (PrimShape ty _) = ty shapeMirTy (TupleShape ty _ _) = ty shapeMirTy (ArrayShape ty _ _) = ty shapeMirTy (StructShape ty _ _) = ty +shapeMirTy (TransparentShape ty _) = ty shapeMirTy (RefShape ty _ _) = ty fieldShapeMirTy :: FieldShape tp -> M.Ty diff --git a/crux-mir-comp/src/Mir/Compositional/Override.hs b/crux-mir-comp/src/Mir/Compositional/Override.hs index e22f5adcec..f0b47ec479 100644 --- a/crux-mir-comp/src/Mir/Compositional/Override.hs +++ b/crux-mir-comp/src/Mir/Compositional/Override.hs @@ -390,6 +390,7 @@ matchArg sym eval allocSpecs shp rv sv = go shp rv sv | otherwise = error $ "matchArg: type error: expected " ++ show shpTpr ++ ", but got Any wrapping " ++ show tpr where shpTpr = StructRepr $ fmapFC fieldShapeType flds + go (TransparentShape _ shp) rv sv = go shp rv sv go (RefShape refTy _ tpr) ref (MS.SetupVar alloc) = goRef refTy tpr ref alloc 0 go (RefShape refTy _ tpr) ref (MS.SetupElem () (MS.SetupVar alloc) idx) = @@ -507,6 +508,7 @@ setupToReg sym sc termSub regMap allocMap shp sv = go shp sv return $ MirVector_Vector $ V.fromList rvs go (StructShape _ _ flds) (MS.SetupStruct _ False svs) = AnyValue (StructRepr $ fmapFC fieldShapeType flds) <$> goFields flds svs + go (TransparentShape _ shp) sv = go shp sv go (RefShape _ _ tpr) (MS.SetupVar alloc) = case Map.lookup alloc allocMap of Just (Some ptr) -> case testEquality tpr (ptr ^. mpType) of Just Refl -> return $ ptr ^. mpRef diff --git a/deps/crucible b/deps/crucible index e5c768c3c7..118f1d05af 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit e5c768c3c7f78f28ccedf454b8d5ef34577f9d79 +Subproject commit 118f1d05af85a05689378c8a1bf672139aac5555 From c18d4f10cb9006bf665a8bd7b7cc45217af62bc7 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Thu, 6 May 2021 16:32:08 -0700 Subject: [PATCH 20/34] test updates for cryptol path->module change --- crux-mir-comp/test/Test.hs | 2 ++ crux-mir-comp/test/symb_eval/cryptol/basic.cry | 2 ++ crux-mir-comp/test/symb_eval/cryptol/basic_add.rs | 2 +- crux-mir-comp/test/symb_eval/cryptol/basic_add_bits.rs | 2 +- crux-mir-comp/test/symb_eval/cryptol/basic_array_arg.rs | 2 +- crux-mir-comp/test/symb_eval/cryptol/basic_array_ret.rs | 2 +- crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.rs | 2 +- crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.rs | 2 +- crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.rs | 2 +- crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.rs | 2 +- crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.rs | 2 +- crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.rs | 2 +- crux-mir-comp/test/symb_eval/cryptol/basic_tuple_arg.rs | 2 +- crux-mir-comp/test/symb_eval/cryptol/basic_tuple_ret.rs | 2 +- 14 files changed, 16 insertions(+), 12 deletions(-) diff --git a/crux-mir-comp/test/Test.hs b/crux-mir-comp/test/Test.hs index 8764c69ddb..c05c73b53b 100644 --- a/crux-mir-comp/test/Test.hs +++ b/crux-mir-comp/test/Test.hs @@ -16,6 +16,7 @@ import System.FilePath import System.IO (IOMode(..), Handle, withFile, hClose, hGetContents, hGetLine, openFile) import System.IO.Temp (withSystemTempFile) +import System.Environment (setEnv) import qualified System.Process as Proc import Test.Tasty (defaultMain, testGroup, TestTree) @@ -90,6 +91,7 @@ runCrux rustFile outHandle mode = do Mir.defaultMirOptions { Mir.printResultOnly = (mode == RcmConcrete), Mir.defaultRlibsDir = "../deps/crucible/crux-mir/rlibs" }) let ?outputConfig = Crux.OutputConfig False outHandle outHandle quiet + setEnv "CRYPTOLPATH" "." _exitCode <- Mir.runTestsWithExtraOverrides overrides options return () where diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic.cry b/crux-mir-comp/test/symb_eval/cryptol/basic.cry index 3a556673f9..93dd5d83e2 100644 --- a/crux-mir-comp/test/symb_eval/cryptol/basic.cry +++ b/crux-mir-comp/test/symb_eval/cryptol/basic.cry @@ -1,3 +1,5 @@ +module test::symb_eval::cryptol::basic where + addByte : [8] -> [8] -> [8] addByte x y = x + y diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_add.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_add.rs index 196a010def..d0fcec41fd 100644 --- a/crux-mir-comp/test/symb_eval/cryptol/basic_add.rs +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_add.rs @@ -2,7 +2,7 @@ extern crate crucible; use crucible::*; cryptol! { - path "test/symb_eval/cryptol/basic.cry"; + path "test::symb_eval::cryptol::basic"; fn add_byte(x: u8, y: u8) -> u8 = "addByte"; } diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_add_bits.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_add_bits.rs index 804a82d54c..963d8460d4 100644 --- a/crux-mir-comp/test/symb_eval/cryptol/basic_add_bits.rs +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_add_bits.rs @@ -1,7 +1,7 @@ extern crate crucible; use crucible::*; -const PATH: &str = "test/symb_eval/cryptol/basic.cry"; +const PATH: &str = "test::symb_eval::cryptol::basic"; fn to_bits(x: u8) -> [bool; 8] { [ diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_array_arg.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_array_arg.rs index 1308d07a99..01f19918f8 100644 --- a/crux-mir-comp/test/symb_eval/cryptol/basic_array_arg.rs +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_array_arg.rs @@ -1,7 +1,7 @@ extern crate crucible; use crucible::*; -const PATH: &str = "test/symb_eval/cryptol/basic.cry"; +const PATH: &str = "test::symb_eval::cryptol::basic"; #[crux_test] fn test() { diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_array_ret.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_array_ret.rs index cafdf9aa68..1fd68d3717 100644 --- a/crux-mir-comp/test/symb_eval/cryptol/basic_array_ret.rs +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_array_ret.rs @@ -1,7 +1,7 @@ extern crate crucible; use crucible::*; -const PATH: &str = "test/symb_eval/cryptol/basic.cry"; +const PATH: &str = "test::symb_eval::cryptol::basic"; #[crux_test] fn test() { diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.rs index 5e56059d7e..0dcdcd4cdc 100644 --- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.rs +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.rs @@ -1,7 +1,7 @@ extern crate crucible; use crucible::*; -const PATH: &str = "test/symb_eval/cryptol/basic.cry"; +const PATH: &str = "test::symb_eval::cryptol::basic"; #[crux_test] fn test() { diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.rs index 3a170bba36..a4f8e4e71a 100644 --- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.rs +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.rs @@ -1,7 +1,7 @@ extern crate crucible; use crucible::*; -const PATH: &str = "test/symb_eval/cryptol/basic.cry"; +const PATH: &str = "test::symb_eval::cryptol::basic"; #[crux_test] fn test() { diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.rs index 51f650131c..175d2e1c91 100644 --- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.rs +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.rs @@ -1,7 +1,7 @@ extern crate crucible; use crucible::*; -const PATH: &str = "test/symb_eval/cryptol/basic.cry"; +const PATH: &str = "test::symb_eval::cryptol::basic"; #[crux_test] fn test() { diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.rs index 968dba7fc7..0bc914122a 100644 --- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.rs +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.rs @@ -1,7 +1,7 @@ extern crate crucible; use crucible::*; -const PATH: &str = "test/symb_eval/cryptol/basic.cry"; +const PATH: &str = "test::symb_eval::cryptol::basic"; #[crux_test] fn test() { diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.rs index 37ad5da789..882daee8dd 100644 --- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.rs +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.rs @@ -1,7 +1,7 @@ extern crate crucible; use crucible::*; -const PATH: &str = "test/symb_eval/cryptol/basic.cry"; +const PATH: &str = "test::symb_eval::cryptol::basic"; #[crux_test] fn test() { diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.rs index 265c9f42fe..424ac3ca65 100644 --- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.rs +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.rs @@ -1,7 +1,7 @@ extern crate crucible; use crucible::*; -const PATH: &str = "test/symb_eval/cryptol/basic.cry"; +const PATH: &str = "test::symb_eval::cryptol::basic"; #[crux_test] fn test() { diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_arg.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_arg.rs index 07755417c1..6f791baeba 100644 --- a/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_arg.rs +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_arg.rs @@ -1,7 +1,7 @@ extern crate crucible; use crucible::*; -const PATH: &str = "test/symb_eval/cryptol/basic.cry"; +const PATH: &str = "test::symb_eval::cryptol::basic"; #[crux_test] fn test() { diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_ret.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_ret.rs index 78be5c4e3c..059fdaf7a8 100644 --- a/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_ret.rs +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_ret.rs @@ -1,7 +1,7 @@ extern crate crucible; use crucible::*; -const PATH: &str = "test/symb_eval/cryptol/basic.cry"; +const PATH: &str = "test::symb_eval::cryptol::basic"; #[crux_test] fn test() { From a78568cd6311399d46a738a0a56ad0e84e282bbe Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Thu, 6 May 2021 16:35:38 -0700 Subject: [PATCH 21/34] avoid unnecessary w4->sawcore conversion --- crux-mir-comp/src/Mir/Cryptol.hs | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index 6bef960fa2..3cd2d1d9a6 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -282,15 +282,13 @@ exprToTerm :: forall sym p t st fs tp rtp a r. IORef (Map SAW.VarIndex (Some (W4.Expr t))) -> W4.Expr t tp -> OverrideSim (p sym) sym MIR rtp a r SAW.Term -exprToTerm sym _sc scs visitCache w4VarMapRef val = do - visitExprVars visitCache val $ \var -> do - let expr = W4.BoundVarExpr var - term <- liftIO $ SAW.toSC sym scs expr - ec <- case SAW.asExtCns term of - Just ec -> return ec - Nothing -> error "eval on BoundVarExpr produced non-ExtCns?" - liftIO $ modifyIORef w4VarMapRef $ Map.insert (SAW.ecVarIndex ec) (Some expr) - liftIO $ SAW.toSC sym scs val +exprToTerm sym sc scs visitCache w4VarMapRef val = do + liftIO $ do + ty <- SAW.baseSCType sym sc (W4.exprType val) + ec <- SAW.scFreshEC sc "w4expr" ty + modifyIORef w4VarMapRef $ Map.insert (SAW.ecVarIndex ec) (Some val) + term <- SAW.scExtCns sc ec + return term regToTerm :: forall sym p t st fs tp rtp a r. (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => From 988f23bb9827f9f65d410d9e3ce4d5948f7d2700 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Wed, 12 May 2021 15:58:37 -0700 Subject: [PATCH 22/34] refactor: move exprToTerm from Mir.Cryptol to Mir.Compositional.Convert and simplify --- .../src/Mir/Compositional/Convert.hs | 91 +++++++++++++++ crux-mir-comp/src/Mir/Cryptol.hs | 104 +----------------- 2 files changed, 94 insertions(+), 101 deletions(-) diff --git a/crux-mir-comp/src/Mir/Compositional/Convert.hs b/crux-mir-comp/src/Mir/Compositional/Convert.hs index 03d925fed0..14de520c48 100644 --- a/crux-mir-comp/src/Mir/Compositional/Convert.hs +++ b/crux-mir-comp/src/Mir/Compositional/Convert.hs @@ -2,6 +2,7 @@ {-# Language FlexibleContexts #-} {-# Language GADTs #-} {-# LANGUAGE KindSignatures #-} +{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -44,6 +45,7 @@ import qualified Verifier.SAW.Simulator.MonadLazy as SAW import qualified Verifier.SAW.Simulator.Value as SAW import Verifier.SAW.Simulator.What4 (SValue) import qualified Verifier.SAW.Simulator.What4 as SAW +import qualified Verifier.SAW.Simulator.What4.ReturnTrip as SAW (baseSCType) import Mir.Intrinsics import qualified Mir.Mir as M @@ -445,3 +447,92 @@ termToType sym sc term = do Nothing -> error "termToPred: zero-width bitvector" return $ Some $ BaseBVRepr w _ -> error $ "termToType: bad SValue" + + +exprToTerm :: forall sym t st fs tp m. + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, MonadIO m, MonadFail m) => + sym -> + SAW.SharedContext -> + IORef (Map SAW.VarIndex (Some (W4.Expr t))) -> + W4.Expr t tp -> + m SAW.Term +exprToTerm sym sc w4VarMapRef val = liftIO $ do + ty <- SAW.baseSCType sym sc (W4.exprType val) + ec <- SAW.scFreshEC sc "w4expr" ty + modifyIORef w4VarMapRef $ Map.insert (SAW.ecVarIndex ec) (Some val) + term <- SAW.scExtCns sc ec + return term + +regToTerm :: forall sym t st fs tp m. + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, MonadIO m, MonadFail m) => + sym -> + SAW.SharedContext -> + String -> + IORef (Map SAW.VarIndex (Some (W4.Expr t))) -> + TypeShape tp -> + RegValue sym tp -> + m SAW.Term +regToTerm sym sc name w4VarMapRef shp rv = go shp rv + where + go :: forall tp. + TypeShape tp -> + RegValue sym tp -> + m SAW.Term + go shp rv = case (shp, rv) of + (UnitShape _, ()) -> liftIO $ SAW.scUnitValue sc + (PrimShape _ _, expr) -> exprToTerm sym sc w4VarMapRef expr + (TupleShape _ _ flds, rvs) -> do + terms <- Ctx.zipWithM (\fld (RV rv) -> Const <$> goField fld rv) flds rvs + liftIO $ SAW.scTuple sc (toListFC getConst terms) + (ArrayShape _ _ shp, vec) -> do + terms <- goVector shp vec + tyTerm <- shapeToTerm sc shp + liftIO $ SAW.scVector sc tyTerm terms + _ -> fail $ + "type error: " ++ name ++ " got argument of unsupported type " ++ show (shapeType shp) + + goField :: forall tp. + FieldShape tp -> + RegValue sym tp -> + m SAW.Term + goField (OptField shp) rv = do + rv' <- liftIO $ readMaybeType sym "field" (shapeType shp) rv + go shp rv' + goField (ReqField shp) rv = go shp rv + + goVector :: forall tp. + TypeShape tp -> + MirVector sym tp -> + m [SAW.Term] + goVector shp (MirVector_Vector v) = mapM (go shp) $ toList v + goVector shp (MirVector_PartialVector pv) = do + forM (toList pv) $ \rv -> do + rv' <- liftIO $ readMaybeType sym "field" (shapeType shp) rv + go shp rv' + goVector _shp (MirVector_Array _) = fail $ + "regToTerm: MirVector_Array not supported" + +shapeToTerm :: forall tp m. + (MonadIO m, MonadFail m) => + SAW.SharedContext -> + TypeShape tp -> + m SAW.Term +shapeToTerm sc shp = go shp + where + go :: forall tp. TypeShape tp -> m SAW.Term + go (UnitShape _) = liftIO $ SAW.scUnitType sc + go (PrimShape _ BaseBoolRepr) = liftIO $ SAW.scBoolType sc + go (PrimShape _ (BaseBVRepr w)) = liftIO $ SAW.scBitvector sc (natValue w) + go (TupleShape _ _ flds) = do + tys <- toListFC getConst <$> traverseFC (\x -> Const <$> goField x) flds + liftIO $ SAW.scTupleType sc tys + go (ArrayShape (M.TyArray _ n) _ shp) = do + ty <- go shp + n <- liftIO $ SAW.scNat sc (fromIntegral n) + liftIO $ SAW.scVecType sc n ty + go shp = fail $ "shapeToTerm: unsupported type " ++ show (shapeType shp) + + goField :: forall tp. FieldShape tp -> m SAW.Term + goField (OptField shp) = go shp + goField (ReqField shp) = go shp + diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index 3cd2d1d9a6..3a3fc25117 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -17,7 +17,6 @@ import Control.Lens (use, (^.), (^?), _Wrapped, ix) import Control.Monad import Control.Monad.IO.Class import qualified Data.ByteString as BS -import Data.Foldable import Data.Functor.Const import Data.IORef import Data.Map (Map) @@ -55,9 +54,7 @@ import Mir.Overrides (getString) import qualified Verifier.SAW.Cryptol.Prelude as SAW import qualified Verifier.SAW.CryptolEnv as SAW -import qualified Verifier.SAW.Recognizer as SAW import qualified Verifier.SAW.SharedTerm as SAW -import qualified Verifier.SAW.Simulator.What4.ReturnTrip as SAW import qualified Verifier.SAW.TypedTerm as SAW import Mir.Compositional.Convert @@ -223,10 +220,9 @@ loadCryptolFunc col sig modulePath name = do Left err -> fail $ "error loading " ++ show name ++ ": " ++ err Right () -> return () - scs <- liftIO $ SAW.newSAWCoreState sc let fnName = "cryptol_" <> modulePath <> "_" <> name return $ LoadedCryptolFunc argShps retShp $ - cryptolRun sc scs (Text.unpack fnName) argShps retShp (SAW.ttTerm tt) + cryptolRun sc (Text.unpack fnName) argShps retShp (SAW.ttTerm tt) where listToCtx :: forall k (f :: k -> *). [Some f] -> Some (Assignment f) @@ -249,22 +245,20 @@ cryptolRun :: forall sym p t st fs rtp r args ret . (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => SAW.SharedContext -> - SAW.SAWCoreState t -> String -> Assignment TypeShape args -> TypeShape ret -> SAW.Term -> OverrideSim (p sym) sym MIR rtp args r (RegValue sym ret) -cryptolRun sc scs name argShps retShp funcTerm = do +cryptolRun sc name argShps retShp funcTerm = do sym <- getSymInterface - visitCache <- liftIO $ (W4.newIdxCache :: IO (W4.IdxCache t (Const ()))) w4VarMapRef <- liftIO $ newIORef (Map.empty :: Map SAW.VarIndex (Some (W4.Expr t))) RegMap argsCtx <- getOverrideArgs argTermsCtx <- Ctx.zipWithM (\shp (RegEntry _ val) -> - Const <$> regToTerm sym sc scs name visitCache w4VarMapRef shp val) + Const <$> regToTerm sym sc name w4VarMapRef shp val) argShps argsCtx let argTerms = toListFC getConst argTermsCtx appTerm <- liftIO $ SAW.scApplyAll sc funcTerm argTerms @@ -273,98 +267,6 @@ cryptolRun sc scs name argShps retShp funcTerm = do rv <- liftIO $ termToReg sym sc w4VarMap appTerm retShp return rv -exprToTerm :: forall sym p t st fs tp rtp a r. - (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => - sym -> - SAW.SharedContext -> - SAW.SAWCoreState t -> - W4.IdxCache t (Const ()) -> - IORef (Map SAW.VarIndex (Some (W4.Expr t))) -> - W4.Expr t tp -> - OverrideSim (p sym) sym MIR rtp a r SAW.Term -exprToTerm sym sc scs visitCache w4VarMapRef val = do - liftIO $ do - ty <- SAW.baseSCType sym sc (W4.exprType val) - ec <- SAW.scFreshEC sc "w4expr" ty - modifyIORef w4VarMapRef $ Map.insert (SAW.ecVarIndex ec) (Some val) - term <- SAW.scExtCns sc ec - return term - -regToTerm :: forall sym p t st fs tp rtp a r. - (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => - sym -> - SAW.SharedContext -> - SAW.SAWCoreState t -> - String -> - W4.IdxCache t (Const ()) -> - IORef (Map SAW.VarIndex (Some (W4.Expr t))) -> - TypeShape tp -> - RegValue sym tp -> - OverrideSim (p sym) sym MIR rtp a r SAW.Term -regToTerm sym sc scs name visitCache w4VarMapRef shp rv = go shp rv - where - go :: forall tp. - TypeShape tp -> - RegValue sym tp -> - OverrideSim (p sym) sym MIR rtp a r SAW.Term - go shp rv = case (shp, rv) of - (UnitShape _, ()) -> liftIO $ SAW.scUnitValue sc - (PrimShape _ _, expr) -> exprToTerm sym sc scs visitCache w4VarMapRef expr - (TupleShape _ _ flds, rvs) -> do - terms <- Ctx.zipWithM (\fld (RV rv) -> Const <$> goField fld rv) flds rvs - liftIO $ SAW.scTuple sc (toListFC getConst terms) - (ArrayShape _ _ shp, vec) -> do - terms <- goVector shp vec - tyTerm <- shapeToTerm sc shp - liftIO $ SAW.scVector sc tyTerm terms - _ -> fail $ - "type error: " ++ name ++ " got argument of unsupported type " ++ show (shapeType shp) - - goField :: forall tp. - FieldShape tp -> - RegValue sym tp -> - OverrideSim (p sym) sym MIR rtp a r SAW.Term - goField (OptField shp) rv = do - rv' <- liftIO $ readMaybeType sym "field" (shapeType shp) rv - go shp rv' - goField (ReqField shp) rv = go shp rv - - goVector :: forall tp. - TypeShape tp -> - MirVector sym tp -> - OverrideSim (p sym) sym MIR rtp a r [SAW.Term] - goVector shp (MirVector_Vector v) = mapM (go shp) $ toList v - goVector shp (MirVector_PartialVector pv) = do - forM (toList pv) $ \rv -> do - rv' <- liftIO $ readMaybeType sym "field" (shapeType shp) rv - go shp rv' - goVector _shp (MirVector_Array _) = fail $ - "regToTerm: MirVector_Array not supported" - -shapeToTerm :: forall tp m. - (MonadIO m, MonadFail m) => - SAW.SharedContext -> - TypeShape tp -> - m SAW.Term -shapeToTerm sc shp = go shp - where - go :: forall tp. TypeShape tp -> m SAW.Term - go (UnitShape _) = liftIO $ SAW.scUnitType sc - go (PrimShape _ BaseBoolRepr) = liftIO $ SAW.scBoolType sc - go (PrimShape _ (BaseBVRepr w)) = liftIO $ SAW.scBitvector sc (natValue w) - go (TupleShape _ _ flds) = do - tys <- toListFC getConst <$> traverseFC (\x -> Const <$> goField x) flds - liftIO $ SAW.scTupleType sc tys - go (ArrayShape (M.TyArray _ n) _ shp) = do - ty <- go shp - n <- liftIO $ SAW.scNat sc (fromIntegral n) - liftIO $ SAW.scVecType sc n ty - go shp = fail $ "shapeToTerm: unsupported type " ++ show (shapeType shp) - - goField :: forall tp. FieldShape tp -> m SAW.Term - goField (OptField shp) = go shp - goField (ReqField shp) = go shp - typecheckFnSig :: M.FnSig -> From e972fb59a15cdf8b8d03beb3966540102585f80a Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Wed, 12 May 2021 16:12:33 -0700 Subject: [PATCH 23/34] crux-mir-comp: avoid unnecessary recursive W4.Expr->SAW.Term conversion --- .../src/Mir/Compositional/Override.hs | 19 ++----------------- 1 file changed, 2 insertions(+), 17 deletions(-) diff --git a/crux-mir-comp/src/Mir/Compositional/Override.hs b/crux-mir-comp/src/Mir/Compositional/Override.hs index f0b47ec479..f8e60b76da 100644 --- a/crux-mir-comp/src/Mir/Compositional/Override.hs +++ b/crux-mir-comp/src/Mir/Compositional/Override.hs @@ -147,7 +147,6 @@ runSpec cs mh ms = do sc <- liftIO $ SAW.mkSharedContext liftIO $ SAW.scLoadPreludeModule sc - scs <- liftIO $ SAW.newSAWCoreState sc -- `eval` converts `W4.Expr`s to `SAW.Term`s. We take what4 exprs from the -- context (e.g., in the actual arguments passed to the override) and @@ -155,23 +154,9 @@ runSpec cs mh ms = do -- Later, we need to convert some SAWCore terms back to what4, so during -- this conversion, we also build up a mapping from SAWCore variables -- (`SAW.ExtCns`) to what4 ones (`W4.ExprBoundVar`). - visitCache <- W4.newIdxCache w4VarMapRef <- liftIO $ newIORef Map.empty - let eval' :: forall tp. W4.Expr t tp -> IO SAW.Term - eval' x = SAW.toSC sym scs x - eval :: forall tp. W4.Expr t tp -> IO SAW.Term - eval x = do - -- When translating W4 vars to SAW `ExtCns`s, also record the - -- reverse mapping into `w4VarMapRef` so the reverse translation - -- can be done later on. - visitExprVars visitCache x $ \var -> do - let expr = W4.BoundVarExpr var - term <- eval' expr - ec <- case SAW.asExtCns term of - Just ec -> return ec - Nothing -> error "eval on BoundVarExpr produced non-ExtCns?" - liftIO $ modifyIORef w4VarMapRef $ Map.insert (SAW.ecVarIndex ec) (Some expr) - eval' x + let eval :: forall tp. W4.Expr t tp -> IO SAW.Term + eval x = exprToTerm sym sc w4VarMapRef x -- Generate fresh variables for use in postconditions and result. The -- result, `postFreshTermSub`, maps MethodSpec `VarIndex`es to `Term`s From d69236221153bf4d792895df78aece15c90767f8 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Fri, 14 May 2021 11:22:07 -0700 Subject: [PATCH 24/34] crux-mir-comp: convert postcondition equalities into substitutions for performance --- .../src/Mir/Compositional/Builder.hs | 154 +++++++++++++++++- .../test/symb_eval/comp/subst_basic.good | 3 + .../test/symb_eval/comp/subst_basic.rs | 33 ++++ .../test/symb_eval/comp/subst_multi.good | 3 + .../test/symb_eval/comp/subst_multi.rs | 36 ++++ .../test/symb_eval/comp/subst_multi_rev.good | 3 + .../test/symb_eval/comp/subst_multi_rev.rs | 38 +++++ .../test/symb_eval/comp/subst_output.good | 10 ++ .../test/symb_eval/comp/subst_output.rs | 34 ++++ 9 files changed, 308 insertions(+), 6 deletions(-) create mode 100644 crux-mir-comp/test/symb_eval/comp/subst_basic.good create mode 100644 crux-mir-comp/test/symb_eval/comp/subst_basic.rs create mode 100644 crux-mir-comp/test/symb_eval/comp/subst_multi.good create mode 100644 crux-mir-comp/test/symb_eval/comp/subst_multi.rs create mode 100644 crux-mir-comp/test/symb_eval/comp/subst_multi_rev.good create mode 100644 crux-mir-comp/test/symb_eval/comp/subst_multi_rev.rs create mode 100644 crux-mir-comp/test/symb_eval/comp/subst_output.good create mode 100644 crux-mir-comp/test/symb_eval/comp/subst_output.rs diff --git a/crux-mir-comp/src/Mir/Compositional/Builder.hs b/crux-mir-comp/src/Mir/Compositional/Builder.hs index 811823a866..49b1d10ff4 100644 --- a/crux-mir-comp/src/Mir/Compositional/Builder.hs +++ b/crux-mir-comp/src/Mir/Compositional/Builder.hs @@ -19,9 +19,11 @@ import qualified Data.BitVector.Sized as BV import Data.Foldable import Data.Functor.Const import Data.IORef +import Data.Map (Map) import qualified Data.Map as Map import Data.Parameterized.Context (pattern Empty, pattern (:>), Assignment) import Data.Parameterized.Nonce +import Data.Parameterized.Pair import Data.Parameterized.Some import Data.Parameterized.TraversableFC import Data.Sequence (Seq) @@ -41,6 +43,7 @@ import Lang.Crucible.Simulator import Lang.Crucible.Types import qualified Verifier.SAW.Prelude as SAW +import qualified Verifier.SAW.Recognizer as SAW (asExtCns) import qualified Verifier.SAW.SharedTerm as SAW import qualified Verifier.SAW.Simulator.What4.ReturnTrip as SAW import qualified Verifier.SAW.TypedTerm as SAW @@ -72,6 +75,12 @@ data MethodSpecBuilder sym t = MethodSpecBuilder , _msbNextAlloc :: MS.AllocIndex , _msbSnapshotFrame :: FrameIdentifier , _msbVisitCache :: W4.IdxCache t (Const ()) + -- | Substitutions to apply to the entire `MethodSpec` after construction. + -- These are generated in place of equality postconditions to improve + -- performance. Variables that appear on the LHS of an entry here will be + -- removed from the `MethodSpec`'s fresh variable lists. Substitutions are + -- applied in the order listed. + , _msbSubsts :: [(SAW.ExtCns SAW.Term, SAW.Term)] } data StateExtra sym t = StateExtra @@ -104,6 +113,7 @@ initMethodSpecBuilder cs sc eval spec snap cache = MethodSpecBuilder , _msbNextAlloc = MS.AllocIndex 0 , _msbSnapshotFrame = snap , _msbVisitCache = cache + , _msbSubsts = [] } initStateExtra :: StateExtra sym t @@ -362,21 +372,78 @@ gatherAsserts msb = do ") references variable " ++ show v ++ " (" ++ show (W4.bvarName v) ++ " at " ++ show (W4.bvarLoc v) ++ "), which does not appear in the function args" Right x -> map fst x + newVars <- liftIO $ gatherVars sym [Some (MethodSpecValue BoolRepr pred) | pred <- asserts'] + let postVars' = Set.union (msb ^. msbPost . seVars) newVars + let postOnlyVars = postVars' `Set.difference` (msb ^. msbPre . seVars) + + (asserts'', substs) <- liftIO $ + gatherSubsts postOnlyVars vars [] [] asserts' + substTerms <- forM substs $ \(Pair var expr) -> do + varTerm <- liftIO $ eval $ W4.BoundVarExpr var + varEc <- case SAW.asExtCns varTerm of + Just ec -> return ec + Nothing -> error $ "eval of BoundVarExpr produced non-ExtCns ?" ++ show varTerm + exprTerm <- liftIO $ eval expr + return (varEc, exprTerm) let loc = msb ^. msbSpec . MS.csLoc - assertConds <- liftIO $ forM asserts' $ \pred -> do + assertConds <- liftIO $ forM asserts'' $ \pred -> do tt <- eval pred >>= SAW.mkTypedTerm sc return $ MS.SetupCond_Pred loc tt - newVars <- liftIO $ gatherVars sym [Some (MethodSpecValue BoolRepr pred) | pred <- asserts'] return $ msb & msbSpec . MS.csPostState . MS.csConditions %~ (++ assertConds) - & msbPost . seVars %~ Set.union newVars + & msbPost . seVars .~ postVars' + & msbSubsts %~ (++ substTerms) + where sc = msb ^. msbSharedContext eval :: forall tp. W4.Expr t tp -> IO SAW.Term eval = msb ^. msbEval + -- | Find assertions of the form `var == expr` that are suitable for + -- performing substitutions, and separate them from the list of assertions. + gatherSubsts :: + Set (Some (W4.ExprBoundVar t)) -> + Set (Some (W4.ExprBoundVar t)) -> + [W4.Expr t BaseBoolType] -> + [Pair (W4.ExprBoundVar t) (W4.Expr t)] -> + [W4.Expr t BaseBoolType] -> + IO ([W4.Expr t BaseBoolType], [Pair (W4.ExprBoundVar t) (W4.Expr t)]) + gatherSubsts _lhsOk _rhsOk accPreds accSubsts [] = + return (reverse accPreds, reverse accSubsts) + gatherSubsts lhsOk rhsOk accPreds accSubsts (pred : preds) + | Just (Pair var expr) <- asVarEqExpr pred = do + rhsSeenRef <- newIORef Set.empty + cache <- W4.newIdxCache + visitExprVars cache expr $ \var -> modifyIORef rhsSeenRef $ Set.insert (Some var) + rhsSeen <- readIORef rhsSeenRef + let lhsOk' = Set.delete (Some var) lhsOk + let rhsOk' = Set.delete (Some var) rhsOk + -- We can't use `pred` as a substitution if the RHS contains variables + -- that were deleted by a previous substitution. Otherwise we'd end up + -- re-introducing a deleted variable. We also can't do substitutions + -- where the RHS expression contains the LHS variable, which is why we + -- check against `rhsOk'` here instead of `rhsOk`. + if rhsSeen `Set.isSubsetOf` rhsOk' then + gatherSubsts lhsOk' rhsOk' accPreds (Pair var expr : accSubsts) preds + else + gatherSubsts lhsOk rhsOk (pred : accPreds) accSubsts preds + | otherwise = + gatherSubsts lhsOk rhsOk (pred : accPreds) accSubsts preds + where + asVarEqExpr pred + | Just (W4.BaseEq _btpr x y) <- W4.asApp pred + , W4.BoundVarExpr v <- x + , Set.member (Some v) lhsOk + = Just (Pair v y) + | Just (W4.BaseEq _btpr x y) <- W4.asApp pred + , W4.BoundVarExpr v <- y + , Set.member (Some v) lhsOk + = Just (Pair v x) + | otherwise = Nothing + + -- | Collect all the symbolic variables that appear in `vals`. gatherVars :: (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) => @@ -461,10 +528,11 @@ finish msb = do & MS.csPreState . MS.csAllocs .~ preAllocs & MS.csPostState . MS.csFreshVars .~ postVars' & MS.csPostState . MS.csAllocs .~ postAllocs - nonce <- liftIO $ freshNonce ng + sm <- liftIO $ buildSubstMap (msb ^. msbSharedContext) (msb ^. msbSubsts) + ms' <- liftIO $ substMethodSpec (msb ^. msbSharedContext) sm ms - let ms' = MethodSpec (msb ^. msbCollectionState) ms - return $ M.MethodSpec ms' (indexValue nonce) + nonce <- liftIO $ freshNonce ng + return $ M.MethodSpec (MethodSpec (msb ^. msbCollectionState) ms') (indexValue nonce) where sc = msb ^. msbSharedContext @@ -480,6 +548,80 @@ finish msb = do Nothing -> error $ "BoundVarExpr translated to non-ExtCns term? " ++ show tt +buildSubstMap :: + SAW.SharedContext -> + [(SAW.ExtCns SAW.Term, SAW.Term)] -> + IO (Map SAW.VarIndex SAW.Term) +buildSubstMap sc substs = go Map.empty substs + where + go sm [] = return sm + go sm ((ec, term) : substs) = do + -- Rewrite the RHSs of previous substitutions using the current one. + let sm1 = Map.singleton (SAW.ecVarIndex ec) term + sm' <- mapM (SAW.scInstantiateExt sc sm1) sm + -- Add the current subst and continue. + go (Map.insert (SAW.ecVarIndex ec) term sm') substs + +substMethodSpec :: + SAW.SharedContext -> + Map SAW.VarIndex SAW.Term -> + MIRMethodSpec -> + IO MIRMethodSpec +substMethodSpec sc sm ms = do + preState' <- goState $ ms ^. MS.csPreState + postState' <- goState $ ms ^. MS.csPostState + argBindings' <- mapM goArg $ ms ^. MS.csArgBindings + retValue' <- mapM goSetupValue $ ms ^. MS.csRetValue + return $ ms + & MS.csPreState .~ preState' + & MS.csPostState .~ postState' + & MS.csArgBindings .~ argBindings' + & MS.csRetValue .~ retValue' + + where + goState ss = do + pointsTos' <- mapM goPointsTo $ ss ^. MS.csPointsTos + conditions' <- mapM goSetupCondition $ ss ^. MS.csConditions + let freshVars' = + filter (\tec -> not $ Map.member (SAW.ecVarIndex $ SAW.tecExt tec) sm) $ + ss ^. MS.csFreshVars + return $ ss + & MS.csPointsTos .~ pointsTos' + & MS.csConditions .~ conditions' + & MS.csFreshVars .~ freshVars' + + goArg (ty, sv) = do + sv' <- goSetupValue sv + return (ty, sv') + + goPointsTo (MirPointsTo alloc svs) = MirPointsTo alloc <$> mapM goSetupValue svs + + goSetupValue sv = case sv of + MS.SetupVar _ -> return sv + MS.SetupTerm tt -> MS.SetupTerm <$> goTypedTerm tt + MS.SetupNull _ -> return sv + MS.SetupStruct b packed svs -> MS.SetupStruct b packed <$> mapM goSetupValue svs + MS.SetupArray b svs -> MS.SetupArray b <$> mapM goSetupValue svs + MS.SetupElem b sv idx -> MS.SetupElem b <$> goSetupValue sv <*> pure idx + MS.SetupField b sv name -> MS.SetupField b <$> goSetupValue sv <*> pure name + MS.SetupGlobal _ _ -> return sv + MS.SetupGlobalInitializer _ _ -> return sv + + goSetupCondition (MS.SetupCond_Equal loc sv1 sv2) = + MS.SetupCond_Equal loc <$> goSetupValue sv1 <*> goSetupValue sv2 + goSetupCondition (MS.SetupCond_Pred loc tt) = + MS.SetupCond_Pred loc <$> goTypedTerm tt + goSetupCondition (MS.SetupCond_Ghost b loc gg tt) = + MS.SetupCond_Ghost b loc gg <$> goTypedTerm tt + + goTypedTerm tt = do + term' <- goTerm $ SAW.ttTerm tt + return $ tt { SAW.ttTerm = term' } + + goTerm term = SAW.scInstantiateExt sc sm term + + + -- RegValue -> SetupValue conversion -- | Convert a RegValue into a SetupValue pattern. Symbolic variables in the diff --git a/crux-mir-comp/test/symb_eval/comp/subst_basic.good b/crux-mir-comp/test/symb_eval/comp/subst_basic.good new file mode 100644 index 0000000000..9cd6d7b455 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/comp/subst_basic.good @@ -0,0 +1,3 @@ +test subst_basic/3a1fbbbh::use_f[0]: ok + +[Crux] Overall status: Valid. diff --git a/crux-mir-comp/test/symb_eval/comp/subst_basic.rs b/crux-mir-comp/test/symb_eval/comp/subst_basic.rs new file mode 100644 index 0000000000..21bda37143 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/comp/subst_basic.rs @@ -0,0 +1,33 @@ +// Test conversion of `var == expr` postconditions into substitutions. +extern crate crucible; +use crucible::*; +use crucible::method_spec::{MethodSpec, MethodSpecBuilder, clobber_globals}; + +fn f(x: u8) -> u8 { + x + 1 +} + +fn f_spec() -> MethodSpec { + let x = ::symbolic("x"); + + let mut msb = MethodSpecBuilder::new(f); + msb.add_arg(&x); + msb.gather_assumes(); + + let y = ::symbolic("result"); + crucible_assert!(y == x + 1); + + msb.set_return(&y); + msb.gather_asserts(); + msb.finish() +} + +#[crux_test] +fn use_f() { + f_spec().enable(); + + let a = u8::symbolic("a"); + crucible_assume!(0 < a && a < 10); + let b = f(a); + crucible_assert!(b == a + 1); +} diff --git a/crux-mir-comp/test/symb_eval/comp/subst_multi.good b/crux-mir-comp/test/symb_eval/comp/subst_multi.good new file mode 100644 index 0000000000..7dfa321a33 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/comp/subst_multi.good @@ -0,0 +1,3 @@ +test subst_multi/3a1fbbbh::use_f[0]: ok + +[Crux] Overall status: Valid. diff --git a/crux-mir-comp/test/symb_eval/comp/subst_multi.rs b/crux-mir-comp/test/symb_eval/comp/subst_multi.rs new file mode 100644 index 0000000000..930ca1c999 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/comp/subst_multi.rs @@ -0,0 +1,36 @@ +// Test substitution with multiple related equalities. +extern crate crucible; +use crucible::*; +use crucible::method_spec::{MethodSpec, MethodSpecBuilder, clobber_globals}; + +fn f(x: u8) -> (u8, u8) { + (x, x + 1) +} + +fn f_spec() -> MethodSpec { + let x = ::symbolic("x"); + + let mut msb = MethodSpecBuilder::new(f); + msb.add_arg(&x); + msb.gather_assumes(); + + let (y0, y1) = <(u8, u8)>::symbolic("result"); + // These turn into two separate substitutions, in order. + crucible_assert!(y1 == y0 + 1); + crucible_assert!(y0 == x); + + msb.set_return(&(y0, y1)); + msb.gather_asserts(); + msb.finish() +} + +#[crux_test] +fn use_f() { + f_spec().enable(); + + let a = u8::symbolic("a"); + crucible_assume!(0 < a && a < 10); + let (b0, b1) = f(a); + crucible_assert!(b0 == a); + crucible_assert!(b1 == b0 + 1); +} diff --git a/crux-mir-comp/test/symb_eval/comp/subst_multi_rev.good b/crux-mir-comp/test/symb_eval/comp/subst_multi_rev.good new file mode 100644 index 0000000000..47171d146e --- /dev/null +++ b/crux-mir-comp/test/symb_eval/comp/subst_multi_rev.good @@ -0,0 +1,3 @@ +test subst_multi_rev/3a1fbbbh::use_f[0]: ok + +[Crux] Overall status: Valid. diff --git a/crux-mir-comp/test/symb_eval/comp/subst_multi_rev.rs b/crux-mir-comp/test/symb_eval/comp/subst_multi_rev.rs new file mode 100644 index 0000000000..84b0b42798 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/comp/subst_multi_rev.rs @@ -0,0 +1,38 @@ +// Test substitution with multiple related equalities. +extern crate crucible; +use crucible::*; +use crucible::method_spec::{MethodSpec, MethodSpecBuilder, clobber_globals}; + +fn f(x: u8) -> (u8, u8) { + (x, x + 1) +} + +fn f_spec() -> MethodSpec { + let x = ::symbolic("x"); + + let mut msb = MethodSpecBuilder::new(f); + msb.add_arg(&x); + msb.gather_assumes(); + + let (y0, y1) = <(u8, u8)>::symbolic("result"); + // These are in reverse order compared to `subst_multi.rs`. As a result, only the first can be + // turned into a substitution. The second will remain as a postcondition, since using it as a + // substitution would reintroduce the eliminated variable `y0`. + crucible_assert!(y0 == x); + crucible_assert!(y1 == y0 + 1); + + msb.set_return(&(y0, y1)); + msb.gather_asserts(); + msb.finish() +} + +#[crux_test] +fn use_f() { + f_spec().enable(); + + let a = u8::symbolic("a"); + crucible_assume!(0 < a && a < 10); + let (b0, b1) = f(a); + crucible_assert!(b0 == a); + crucible_assert!(b1 == b0 + 1); +} diff --git a/crux-mir-comp/test/symb_eval/comp/subst_output.good b/crux-mir-comp/test/symb_eval/comp/subst_output.good new file mode 100644 index 0000000000..bbef7163e0 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/comp/subst_output.good @@ -0,0 +1,10 @@ +test subst_output/3a1fbbbh::use_f[0]: FAILED + +failures: + +---- subst_output/3a1fbbbh::use_f[0] counterexamples ---- +Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/subst_output.rs:32:5: 32:31: error: in subst_output/3a1fbbbh::use_f[0] +MIR assertion at test/symb_eval/comp/subst_output.rs:32:5: + b0 == a + +[Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/comp/subst_output.rs b/crux-mir-comp/test/symb_eval/comp/subst_output.rs new file mode 100644 index 0000000000..78ffedc307 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/comp/subst_output.rs @@ -0,0 +1,34 @@ +// Test substitutions involving only the outputs of the function. +extern crate crucible; +use crucible::*; +use crucible::method_spec::{MethodSpec, MethodSpecBuilder, clobber_globals}; + +fn f(x: u8) -> (u8, u8) { + (x, x + 1) +} + +fn f_spec() -> MethodSpec { + let x = ::symbolic("x"); + + let mut msb = MethodSpecBuilder::new(f); + msb.add_arg(&x); + msb.gather_assumes(); + + let (y0, y1) = <(u8, u8)>::symbolic("result"); + crucible_assert!(y1 == y0 + 1); + + msb.set_return(&(y0, y1)); + msb.gather_asserts(); + msb.finish() +} + +#[crux_test] +fn use_f() { + f_spec().enable(); + + let a = u8::symbolic("a"); + crucible_assume!(0 < a && a < 10); + let (b0, b1) = f(a); + crucible_assert!(b0 == a); + crucible_assert!(b1 == b0 + 1); +} From b15d9e60feee515294b39062720558fcf38ff365 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Fri, 14 May 2021 11:59:41 -0700 Subject: [PATCH 25/34] crux-mir-comp: handle slice arguments in MethodSpecs --- .../src/Mir/Compositional/Convert.hs | 10 +++- .../src/Mir/Compositional/Override.hs | 43 ++++++++++++---- .../test/symb_eval/comp/spec_mut_slice.good | 11 +++++ .../test/symb_eval/comp/spec_mut_slice.rs | 49 +++++++++++++++++++ 4 files changed, 102 insertions(+), 11 deletions(-) create mode 100644 crux-mir-comp/test/symb_eval/comp/spec_mut_slice.good create mode 100644 crux-mir-comp/test/symb_eval/comp/spec_mut_slice.rs diff --git a/crux-mir-comp/src/Mir/Compositional/Convert.hs b/crux-mir-comp/src/Mir/Compositional/Convert.hs index 14de520c48..8ab9e9e73c 100644 --- a/crux-mir-comp/src/Mir/Compositional/Convert.hs +++ b/crux-mir-comp/src/Mir/Compositional/Convert.hs @@ -139,6 +139,14 @@ tyToShape col ty = go ty False -> Some $ OptField shp goRef :: M.Ty -> M.Ty -> M.Mutability -> Some TypeShape + goRef ty (M.TySlice ty') mutbl | Some tpr <- tyToRepr col ty' = Some $ + TupleShape ty [ptrTy, usizeTy] + (Empty + :> ReqField (RefShape ptrTy ty' tpr) + :> ReqField (PrimShape usizeTy BaseUsizeRepr)) + where + ptrTy = M.TyRawPtr ty' mutbl + usizeTy = M.TyUint M.USize goRef ty ty' _ | isUnsized ty' = error $ "tyToShape: fat pointer " ++ show ty ++ " NYI" goRef ty ty' _ | Some tpr <- tyToRepr col ty' = Some $ RefShape ty ty' tpr @@ -146,7 +154,7 @@ tyToShape col ty = go ty -- | Given a `Ty` and the result of `tyToRepr ty`, produce a `TypeShape` with -- the same index `tp`. Raises an `error` if the `TypeRepr` doesn't match -- `tyToRepr ty`. -tyToShapeEq :: M.Collection -> M.Ty -> TypeRepr tp -> TypeShape tp +tyToShapeEq :: HasCallStack => M.Collection -> M.Ty -> TypeRepr tp -> TypeShape tp tyToShapeEq col ty tpr | Some shp <- tyToShape col ty = case testEquality (shapeType shp) tpr of Just Refl -> shp diff --git a/crux-mir-comp/src/Mir/Compositional/Override.hs b/crux-mir-comp/src/Mir/Compositional/Override.hs index f8e60b76da..39bb84ca5e 100644 --- a/crux-mir-comp/src/Mir/Compositional/Override.hs +++ b/crux-mir-comp/src/Mir/Compositional/Override.hs @@ -198,7 +198,7 @@ runSpec cs mh ms = do ": no arg at index " ++ show i Just x -> return x let shp = tyToShapeEq col ty tpr - matchArg sym eval (ms ^. MS.csPreState . MS.csAllocs) shp rv sv + matchArg sym sc eval (ms ^. MS.csPreState . MS.csAllocs) shp rv sv -- Match PointsTo SetupValues against accessible memory. -- @@ -223,7 +223,7 @@ runSpec cs mh ms = do ref' <- lift $ mirRef_offsetSim (ptr ^. mpType) (ptr ^. mpRef) iSym rv <- lift $ readMirRefSim (ptr ^. mpType) ref' let shp = tyToShapeEq col ty (ptr ^. mpType) - matchArg sym eval (ms ^. MS.csPreState . MS.csAllocs) shp rv sv + matchArg sym sc eval (ms ^. MS.csPreState . MS.csAllocs) shp rv sv -- Validity checks @@ -343,11 +343,12 @@ matchArg :: forall sym t st fs tp. (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasCallStack) => sym -> + SAW.SharedContext -> (forall tp'. W4.Expr t tp' -> IO SAW.Term) -> Map MS.AllocIndex (Some MirAllocSpec) -> TypeShape tp -> RegValue sym tp -> MS.SetupValue MIR -> MirOverrideMatcher sym () -matchArg sym eval allocSpecs shp rv sv = go shp rv sv +matchArg sym sc eval allocSpecs shp rv sv = go shp rv sv where go :: forall tp. TypeShape tp -> RegValue sym tp -> MS.SetupValue MIR -> MirOverrideMatcher sym () @@ -355,14 +356,36 @@ matchArg sym eval allocSpecs shp rv sv = go shp rv sv go (PrimShape _ _btpr) expr (MS.SetupTerm tt) = do loc <- use MS.osLocation exprTerm <- liftIO $ eval expr - var <- case SAW.asExtCns $ SAW.ttTerm tt of - Just ec -> return $ SAW.ecVarIndex ec + case SAW.asExtCns $ SAW.ttTerm tt of + Just ec -> do + let var = SAW.ecVarIndex ec + sub <- use MS.termSub + when (Map.member var sub) $ + MS.failure loc MS.NonlinearPatternNotSupported + MS.termSub %= Map.insert var exprTerm Nothing -> do - MS.failure loc $ MS.BadTermMatch (SAW.ttTerm tt) exprTerm - sub <- use MS.termSub - when (Map.member var sub) $ - MS.failure loc MS.NonlinearPatternNotSupported - MS.termSub %= Map.insert var exprTerm + -- If the `TypedTerm` is a constant, we want to assert that the + -- argument `expr` matches the constant. + -- + -- For now, this is the case that fires for the length fields + -- of slices. This means the slice length must exactly match + -- the length used in the MethodSpec, or else the spec must + -- specifically handle symbolic lengths in some range. It + -- would be nice to allow any longer slice length, but it's not + -- clear how to do that soundly (the function might branch on + -- the length of the slice, for instance). + Some val <- liftIO $ termToExpr sym sc mempty (SAW.ttTerm tt) + Refl <- case testEquality (W4.exprType expr) (W4.exprType val) of + Just x -> return x + Nothing -> error $ "type mismatch: concrete argument type " ++ + show (W4.exprType expr) ++ " doesn't match SetupValue type " ++ + show (W4.exprType val) + eq <- liftIO $ W4.isEq sym expr val + MS.addAssert eq $ SimError loc $ + AssertFailureSimError + ("mismatch on " ++ show (W4.exprType expr) ++ ": expected " ++ + show (W4.printSymExpr val)) + "" go (TupleShape _ _ flds) rvs (MS.SetupStruct () False svs) = goFields flds rvs svs go (ArrayShape _ _ shp) vec (MS.SetupArray () svs) = case vec of MirVector_Vector v -> zipWithM_ (go shp) (toList v) svs diff --git a/crux-mir-comp/test/symb_eval/comp/spec_mut_slice.good b/crux-mir-comp/test/symb_eval/comp/spec_mut_slice.good new file mode 100644 index 0000000000..216a99488c --- /dev/null +++ b/crux-mir-comp/test/symb_eval/comp/spec_mut_slice.good @@ -0,0 +1,11 @@ +test spec_mut_slice/3a1fbbbh::f_test[0]: ok +test spec_mut_slice/3a1fbbbh::use_f[0]: FAILED + +failures: + +---- spec_mut_slice/3a1fbbbh::use_f[0] counterexamples ---- +Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_mut_slice.rs:48:5: 48:30: error: in spec_mut_slice/3a1fbbbh::use_f[0] +MIR assertion at test/symb_eval/comp/spec_mut_slice.rs:48:5: + d < 10 + +[Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/comp/spec_mut_slice.rs b/crux-mir-comp/test/symb_eval/comp/spec_mut_slice.rs new file mode 100644 index 0000000000..c1395db905 --- /dev/null +++ b/crux-mir-comp/test/symb_eval/comp/spec_mut_slice.rs @@ -0,0 +1,49 @@ +extern crate crucible; +use crucible::*; +use crucible::method_spec::{MethodSpec, MethodSpecBuilder, clobber_globals}; + +fn f(x: &mut [u8]) { + x.swap(0, 1); +} + +#[crux_test] +fn f_test() { + clobber_globals(); + let mut x = <[u8; 2]>::symbolic("x"); + crucible_assume!(x[0] > 0); + f(&mut x); + crucible_assert!(x[1] > 0); +} + +fn f_spec() -> MethodSpec { + let mut x = <[u8; 2]>::symbolic("x"); + crucible_assume!(x[0] > 0); + crucible_assume!(x[1] == 0); + + let mut msb = MethodSpecBuilder::new(f); + // TODO: would be nice to have strongly-typed add_arg, so coercions will apply here + msb.add_arg(& (&mut x as &mut [_])); + msb.gather_assumes(); + + // Call happens here + crucible_assert!(x[1] > 0); + + msb.set_return(&()); + msb.gather_asserts(); + msb.finish() +} + +#[crux_test] +fn use_f() { + f_spec().enable(); + + let a = u8::symbolic("a"); + let b = u8::symbolic("b"); + crucible_assume!(0 < a && a < 10); + crucible_assume!(b == 0); + let mut arr = [a, b]; + f(&mut arr); + let [c, d] = arr; + crucible_assert!(0 < d); + crucible_assert!(d < 10); +} From eaaf1510a4d8bb77a8976117e591e488dc679296 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Mon, 24 May 2021 10:02:20 -0700 Subject: [PATCH 26/34] add cryptol::munge override --- crux-mir-comp/src/Mir/Cryptol.hs | 88 +++++++++++++++++++++++++++++++- deps/crucible | 2 +- 2 files changed, 87 insertions(+), 3 deletions(-) diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index 3a3fc25117..69564acd47 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -31,6 +31,7 @@ import Data.Parameterized.NatRepr import Data.Parameterized.TraversableFC import qualified What4.Expr.Builder as W4 +import qualified What4.Partial as W4 import Cryptol.TypeCheck.AST as Cry import Cryptol.Utils.Ident as Cry @@ -55,12 +56,12 @@ import Mir.Overrides (getString) import qualified Verifier.SAW.Cryptol.Prelude as SAW import qualified Verifier.SAW.CryptolEnv as SAW import qualified Verifier.SAW.SharedTerm as SAW +import qualified Verifier.SAW.Simulator.What4.ReturnTrip as SAW +import qualified Verifier.SAW.Recognizer as SAW (asExtCns) import qualified Verifier.SAW.TypedTerm as SAW import Mir.Compositional.Convert -import Debug.Trace - cryptolOverrides :: forall sym p t st fs args ret blocks rtp a r . @@ -112,6 +113,22 @@ cryptolOverrides _symOnline cs name cfg :> RegEntry _tpr' nameStr) <- getOverrideArgs cryptolOverride (cs ^. collection) mh modulePathStr nameStr + | (normDefId "crucible::cryptol::munge" <> "::_inst") `Text.isPrefixOf` name + , Empty :> tpr <- cfgArgTypes cfg + , tpr' <- cfgReturnType cfg + , Just Refl <- testEquality tpr tpr' + = Just $ bindFnHandle (cfgHandle cfg) $ UseOverride $ + mkOverride' "cryptol_munge" tpr $ do + let tyArg = cs ^? collection . M.intrinsics . ix (textId name) . + M.intrInst . M.inSubsts . _Wrapped . ix 0 + shp <- case tyArg of + Just ty -> return $ tyToShapeEq (cs ^. collection) ty tpr + _ -> error $ "impossible: missing type argument for cryptol::munge()" + + sym <- getSymInterface + RegMap (Empty :> RegEntry _ rv) <- getOverrideArgs + liftIO $ munge sym shp rv + | otherwise = Nothing @@ -268,6 +285,73 @@ cryptolRun sc name argShps retShp funcTerm = do return rv +munge :: forall sym t st fs tp. + (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) => + sym -> TypeShape tp -> RegValue sym tp -> IO (RegValue sym tp) +munge sym shp rv = do + sc <- SAW.mkSharedContext + SAW.scLoadPreludeModule sc + + scs <- SAW.newSAWCoreState sc + visitCache <- W4.newIdxCache + w4VarMapRef <- newIORef Map.empty + + let eval' :: forall tp. W4.Expr t tp -> IO SAW.Term + eval' x = SAW.toSC sym scs x + eval :: forall tp. W4.Expr t tp -> IO SAW.Term + eval x = do + -- When translating W4 vars to SAW `ExtCns`s, also record the + -- reverse mapping into `w4VarMapRef` so the reverse translation + -- can be done later on. + visitExprVars visitCache x $ \var -> do + let expr = W4.BoundVarExpr var + term <- eval' expr + ec <- case SAW.asExtCns term of + Just ec -> return ec + Nothing -> error "eval on BoundVarExpr produced non-ExtCns?" + modifyIORef w4VarMapRef $ Map.insert (SAW.ecVarIndex ec) (Some expr) + eval' x + uneval :: TypeShape (BaseToType btp) -> SAW.Term -> IO (W4.Expr t btp) + uneval shp t = do + w4VarMap <- readIORef w4VarMapRef + termToReg sym sc w4VarMap t shp + + let go :: forall tp. TypeShape tp -> RegValue sym tp -> IO (RegValue sym tp) + go (UnitShape _) () = return () + go shp@(PrimShape _ _) expr = eval expr >>= uneval shp + go (TupleShape _ _ flds) rvs = goFields flds rvs + go (ArrayShape _ _ shp) vec = case vec of + MirVector_Vector v -> MirVector_Vector <$> mapM (go shp) v + MirVector_PartialVector pv -> do + pv' <- forM pv $ \p -> do + rv <- readMaybeType sym "vector element" (shapeType shp) p + W4.justPartExpr sym <$> go shp rv + return $ MirVector_PartialVector pv' + MirVector_Array _ -> error $ "munge: MirVector_Array NYI" + -- TODO: StructShape + go (TransparentShape _ shp) rv = go shp rv + -- TODO: RefShape + go shp _ = error $ "munge: " ++ show (shapeType shp) ++ " NYI" + + goFields :: forall ctx. + Assignment FieldShape ctx -> + Assignment (RegValue' sym) ctx -> + IO (Assignment (RegValue' sym) ctx) + goFields Empty Empty = return Empty + goFields (flds :> fld) (rvs :> RV rv) = do + rvs' <- goFields flds rvs + rv' <- goField fld rv + return $ rvs' :> RV rv' + + goField :: forall tp. FieldShape tp -> RegValue sym tp -> IO (RegValue sym tp) + goField (ReqField shp) rv = go shp rv + goField (OptField shp) rv = do + rv' <- readMaybeType sym "field" (shapeType shp) rv + W4.justPartExpr sym <$> go shp rv' + + go shp rv + + typecheckFnSig :: M.FnSig -> [Some TypeShape] -> diff --git a/deps/crucible b/deps/crucible index 118f1d05af..563aacb11d 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 118f1d05af85a05689378c8a1bf672139aac5555 +Subproject commit 563aacb11df43fc8adf518fabff2f0e1933aac65 From ebab5d7afffb376c4e7444a1a9e974a8f542d759 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Mon, 24 May 2021 10:11:17 -0700 Subject: [PATCH 27/34] crux-mir-cryptol: adjust slice repr to avoid clobbering &[_] --- crux-mir-comp/src/Mir/Compositional/Convert.hs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/crux-mir-comp/src/Mir/Compositional/Convert.hs b/crux-mir-comp/src/Mir/Compositional/Convert.hs index 8ab9e9e73c..20451c088a 100644 --- a/crux-mir-comp/src/Mir/Compositional/Convert.hs +++ b/crux-mir-comp/src/Mir/Compositional/Convert.hs @@ -140,12 +140,16 @@ tyToShape col ty = go ty goRef :: M.Ty -> M.Ty -> M.Mutability -> Some TypeShape goRef ty (M.TySlice ty') mutbl | Some tpr <- tyToRepr col ty' = Some $ - TupleShape ty [ptrTy, usizeTy] + TupleShape ty [refTy, usizeTy] (Empty - :> ReqField (RefShape ptrTy ty' tpr) + :> ReqField (RefShape refTy ty' tpr) :> ReqField (PrimShape usizeTy BaseUsizeRepr)) where - ptrTy = M.TyRawPtr ty' mutbl + -- We use a ref (of the same mutability as `ty`) when possible, to + -- avoid unnecessary clobbering. + refTy = case ty of + M.TyRef _ _ -> M.TyRef ty' mutbl + _ -> M.TyRef ty' mutbl usizeTy = M.TyUint M.USize goRef ty ty' _ | isUnsized ty' = error $ "tyToShape: fat pointer " ++ show ty ++ " NYI" From 8218d94888ef57ff6c8c935e66bfe6f583c4230c Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Mon, 24 May 2021 10:12:03 -0700 Subject: [PATCH 28/34] tiny cleanup --- crux-mir-comp/src/Mir/Cryptol.hs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index 69564acd47..84302c6839 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -281,9 +281,7 @@ cryptolRun sc name argShps retShp funcTerm = do appTerm <- liftIO $ SAW.scApplyAll sc funcTerm argTerms w4VarMap <- liftIO $ readIORef w4VarMapRef - rv <- liftIO $ termToReg sym sc w4VarMap appTerm retShp - return rv - + liftIO $ termToReg sym sc w4VarMap appTerm retShp munge :: forall sym t st fs tp. (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) => From 6866f25c753e0751ba586704285893711f2c88d9 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Mon, 24 May 2021 10:12:24 -0700 Subject: [PATCH 29/34] bump crucible for crucible::dump_what4 debug function --- deps/crucible | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/crucible b/deps/crucible index 563aacb11d..6f8a4e2ad3 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 563aacb11df43fc8adf518fabff2f0e1933aac65 +Subproject commit 6f8a4e2ad3dd218c5f2c0a3b82ae3b0809282a27 From b620b40e1dc9bda9e407f3017b3d9079ae9da65c Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Mon, 24 May 2021 10:25:19 -0700 Subject: [PATCH 30/34] fix warnings --- crux-mir-comp/src/Mir/Compositional/Convert.hs | 4 +++- crux-mir-comp/src/Mir/Compositional/Override.hs | 3 --- crux-mir-comp/src/Mir/Cryptol.hs | 1 - 3 files changed, 3 insertions(+), 5 deletions(-) diff --git a/crux-mir-comp/src/Mir/Compositional/Convert.hs b/crux-mir-comp/src/Mir/Compositional/Convert.hs index 20451c088a..3b9cbe24a3 100644 --- a/crux-mir-comp/src/Mir/Compositional/Convert.hs +++ b/crux-mir-comp/src/Mir/Compositional/Convert.hs @@ -263,6 +263,7 @@ visitExprVars cache e f = go Set.empty e W4.FnApp _ _ -> error "unexpected FnApp" W4.AppExpr ae -> void $ W4.traverseApp (\e' -> go bound e' >> return e') $ W4.appExprApp ae + W4.FloatExpr _ _ _ -> return () W4.StringExpr _ _ -> return () W4.BoolExpr _ _ -> return () W4.SemiRingLiteral _ _ _ -> return () @@ -360,7 +361,7 @@ termToReg sym sc varMap term shp = do x' <- SAW.force x xs' <- SAW.force xs tupleToListRev (n - 1) (x' : acc) xs' - tupleToListRev n _ _ = error $ "bad tuple size " ++ show n + tupleToListRev n _ _ | n < 2 = error $ "bad tuple size " ++ show n tupleToListRev n _ v = error $ "termToReg: expected tuple of " ++ show n ++ " elements, but got " ++ show v @@ -373,6 +374,7 @@ termToReg sym sc varMap term shp = do rv <- goField fld sv rvs <- goTuple flds svs return (rvs :> RV rv) + goTuple _ _ = fail "termToReg: mismatched tuple size" goField :: forall tp'. FieldShape tp' -> SValue sym -> IO (RegValue sym tp') goField (ReqField shp) sv = go shp sv diff --git a/crux-mir-comp/src/Mir/Compositional/Override.hs b/crux-mir-comp/src/Mir/Compositional/Override.hs index 39bb84ca5e..cf2e851cad 100644 --- a/crux-mir-comp/src/Mir/Compositional/Override.hs +++ b/crux-mir-comp/src/Mir/Compositional/Override.hs @@ -49,9 +49,6 @@ import Lang.Crucible.Types import qualified Verifier.SAW.Prelude as SAW import qualified Verifier.SAW.Recognizer as SAW import qualified Verifier.SAW.SharedTerm as SAW -import qualified Verifier.SAW.Simulator.Value as SAW -import qualified Verifier.SAW.Simulator.What4 as SAW -import qualified Verifier.SAW.Simulator.What4.ReturnTrip as SAW import qualified Verifier.SAW.Term.Functor as SAW import qualified Verifier.SAW.TypedTerm as SAW diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index 84302c6839..39f775135f 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -43,7 +43,6 @@ import Lang.Crucible.FunctionHandle import Lang.Crucible.Simulator import Crux -import Crux.Types import Mir.DefId import Mir.Generator (CollectionState, collection, MirHandle(..)) From 6d023f856fa6b6866421621d1877352694ebfc46 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Mon, 28 Jun 2021 09:21:15 -0700 Subject: [PATCH 31/34] update crucible submodule --- deps/crucible | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/crucible b/deps/crucible index 6f8a4e2ad3..584d47d384 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 6f8a4e2ad3dd218c5f2c0a3b82ae3b0809282a27 +Subproject commit 584d47d384104c06a92b3820882639e9898e4b0d From 701edb55e360992da57c53f1a6549f0c2b811990 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Mon, 28 Jun 2021 09:39:21 -0700 Subject: [PATCH 32/34] update Test.hs for crux changes --- crux-mir-comp/test/Test.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/crux-mir-comp/test/Test.hs b/crux-mir-comp/test/Test.hs index c05c73b53b..7dae43b5d7 100644 --- a/crux-mir-comp/test/Test.hs +++ b/crux-mir-comp/test/Test.hs @@ -90,7 +90,8 @@ runCrux rustFile outHandle mode = do Crux.branchCoverage = (mode == RcmCoverage) } , Mir.defaultMirOptions { Mir.printResultOnly = (mode == RcmConcrete), Mir.defaultRlibsDir = "../deps/crucible/crux-mir/rlibs" }) - let ?outputConfig = Crux.OutputConfig False outHandle outHandle quiet + let ?outputConfig = Crux.mkOutputConfig False outHandle outHandle $ + Just (fst options) setEnv "CRYPTOLPATH" "." _exitCode <- Mir.runTestsWithExtraOverrides overrides options return () From 05741e5cb5b79b03a21592c615e3ad0e72ba17d2 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Mon, 28 Jun 2021 09:41:47 -0700 Subject: [PATCH 33/34] update golden test files for crux output format changes --- .../test/symb_eval/comp/alias_array_bad.good | 19 +++++++++++-------- .../test/symb_eval/comp/alias_array_bad2.good | 12 +++++++----- .../test/symb_eval/comp/alias_array_ok.good | 7 ++++--- .../test/symb_eval/comp/alias_bad.good | 19 +++++++++++-------- .../test/symb_eval/comp/alias_ok.good | 7 ++++--- .../test/symb_eval/comp/clobber_globals.good | 14 ++++++++------ .../symb_eval/comp/override_test_indep.good | 7 ++++--- .../test/symb_eval/comp/ptr_offset.good | 7 ++++--- .../test/symb_eval/comp/ptr_offset_rev.good | 7 ++++--- .../test/symb_eval/comp/spec_array.good | 7 ++++--- .../test/symb_eval/comp/spec_box.good | 7 ++++--- .../test/symb_eval/comp/spec_immut_cell.good | 7 ++++--- .../test/symb_eval/comp/spec_mut.good | 7 ++++--- .../test/symb_eval/comp/spec_mut_slice.good | 7 ++++--- .../test/symb_eval/comp/spec_struct.good | 7 ++++--- .../test/symb_eval/comp/spec_tuple.good | 7 ++++--- .../test/symb_eval/comp/subst_output.good | 7 ++++--- .../cryptol/basic_err_array_size.good | 5 +++-- .../symb_eval/cryptol/basic_err_bv_size.good | 5 +++-- .../cryptol/basic_err_fewer_args.good | 5 +++-- .../symb_eval/cryptol/basic_err_mismatch.good | 5 +++-- .../cryptol/basic_err_more_args.good | 5 +++-- .../cryptol/basic_err_tuple_size.good | 5 +++-- 23 files changed, 107 insertions(+), 78 deletions(-) diff --git a/crux-mir-comp/test/symb_eval/comp/alias_array_bad.good b/crux-mir-comp/test/symb_eval/comp/alias_array_bad.good index 712babf9ff..8f21a5ca50 100644 --- a/crux-mir-comp/test/symb_eval/comp/alias_array_bad.good +++ b/crux-mir-comp/test/symb_eval/comp/alias_array_bad.good @@ -4,13 +4,16 @@ test alias_array_bad/3a1fbbbh::use_f[0]: FAILED failures: ---- alias_array_bad/3a1fbbbh::use_f[0] counterexamples ---- -Failure for test/symb_eval/comp/alias_array_bad.rs:45:14: 45:16: error: in alias_array_bad/3a1fbbbh::use_f[0] -references AllocIndex 0 and AllocIndex 1 must not overlap -Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_array_bad.rs:46:5: 46:38: error: in alias_array_bad/3a1fbbbh::use_f[0] -MIR assertion at test/symb_eval/comp/alias_array_bad.rs:46:5: - 0 < b[0].get() -Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_array_bad.rs:47:5: 47:39: error: in alias_array_bad/3a1fbbbh::use_f[0] -MIR assertion at test/symb_eval/comp/alias_array_bad.rs:47:5: - b[0].get() < 10 +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/comp/alias_array_bad.rs:45:14: 45:16: error: in alias_array_bad/3a1fbbbh::use_f[0] +[Crux] references AllocIndex 0 and AllocIndex 1 must not overlap +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_array_bad.rs:46:5: 46:38: error: in alias_array_bad/3a1fbbbh::use_f[0] +[Crux] MIR assertion at test/symb_eval/comp/alias_array_bad.rs:46:5: +[Crux] 0 < b[0].get() +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_array_bad.rs:47:5: 47:39: error: in alias_array_bad/3a1fbbbh::use_f[0] +[Crux] MIR assertion at test/symb_eval/comp/alias_array_bad.rs:47:5: +[Crux] b[0].get() < 10 [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/comp/alias_array_bad2.good b/crux-mir-comp/test/symb_eval/comp/alias_array_bad2.good index 7a66ff6911..174eaca698 100644 --- a/crux-mir-comp/test/symb_eval/comp/alias_array_bad2.good +++ b/crux-mir-comp/test/symb_eval/comp/alias_array_bad2.good @@ -4,10 +4,12 @@ test alias_array_bad2/3a1fbbbh::use_f[0]: FAILED failures: ---- alias_array_bad2/3a1fbbbh::use_f[0] counterexamples ---- -Failure for test/symb_eval/comp/alias_array_bad2.rs:45:14: 45:16: error: in alias_array_bad2/3a1fbbbh::use_f[0] -references AllocIndex 0 and AllocIndex 1 must not overlap -Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_array_bad2.rs:47:5: 47:39: error: in alias_array_bad2/3a1fbbbh::use_f[0] -MIR assertion at test/symb_eval/comp/alias_array_bad2.rs:47:5: - b[0].get() < 10 +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/comp/alias_array_bad2.rs:45:14: 45:16: error: in alias_array_bad2/3a1fbbbh::use_f[0] +[Crux] references AllocIndex 0 and AllocIndex 1 must not overlap +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_array_bad2.rs:47:5: 47:39: error: in alias_array_bad2/3a1fbbbh::use_f[0] +[Crux] MIR assertion at test/symb_eval/comp/alias_array_bad2.rs:47:5: +[Crux] b[0].get() < 10 [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/comp/alias_array_ok.good b/crux-mir-comp/test/symb_eval/comp/alias_array_ok.good index ac20b5a3ee..b7b511b522 100644 --- a/crux-mir-comp/test/symb_eval/comp/alias_array_ok.good +++ b/crux-mir-comp/test/symb_eval/comp/alias_array_ok.good @@ -4,8 +4,9 @@ test alias_array_ok/3a1fbbbh::use_f[0]: FAILED failures: ---- alias_array_ok/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_array_ok.rs:48:5: 48:39: error: in alias_array_ok/3a1fbbbh::use_f[0] -MIR assertion at test/symb_eval/comp/alias_array_ok.rs:48:5: - b[0].get() < 10 +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_array_ok.rs:48:5: 48:39: error: in alias_array_ok/3a1fbbbh::use_f[0] +[Crux] MIR assertion at test/symb_eval/comp/alias_array_ok.rs:48:5: +[Crux] b[0].get() < 10 [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/comp/alias_bad.good b/crux-mir-comp/test/symb_eval/comp/alias_bad.good index 4a785dc86e..c573524a28 100644 --- a/crux-mir-comp/test/symb_eval/comp/alias_bad.good +++ b/crux-mir-comp/test/symb_eval/comp/alias_bad.good @@ -4,13 +4,16 @@ test alias_bad/3a1fbbbh::use_f[0]: FAILED failures: ---- alias_bad/3a1fbbbh::use_f[0] counterexamples ---- -Failure for test/symb_eval/comp/alias_bad.rs:45:11: 45:13: error: in alias_bad/3a1fbbbh::use_f[0] -references AllocIndex 0 and AllocIndex 1 must not overlap -Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_bad.rs:46:5: 46:35: error: in alias_bad/3a1fbbbh::use_f[0] -MIR assertion at test/symb_eval/comp/alias_bad.rs:46:5: - 0 < b.get() -Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_bad.rs:47:5: 47:36: error: in alias_bad/3a1fbbbh::use_f[0] -MIR assertion at test/symb_eval/comp/alias_bad.rs:47:5: - b.get() < 10 +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/comp/alias_bad.rs:45:11: 45:13: error: in alias_bad/3a1fbbbh::use_f[0] +[Crux] references AllocIndex 0 and AllocIndex 1 must not overlap +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_bad.rs:46:5: 46:35: error: in alias_bad/3a1fbbbh::use_f[0] +[Crux] MIR assertion at test/symb_eval/comp/alias_bad.rs:46:5: +[Crux] 0 < b.get() +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_bad.rs:47:5: 47:36: error: in alias_bad/3a1fbbbh::use_f[0] +[Crux] MIR assertion at test/symb_eval/comp/alias_bad.rs:47:5: +[Crux] b.get() < 10 [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/comp/alias_ok.good b/crux-mir-comp/test/symb_eval/comp/alias_ok.good index c66fbe145a..bbb9fcc0ab 100644 --- a/crux-mir-comp/test/symb_eval/comp/alias_ok.good +++ b/crux-mir-comp/test/symb_eval/comp/alias_ok.good @@ -4,8 +4,9 @@ test alias_ok/3a1fbbbh::use_f[0]: FAILED failures: ---- alias_ok/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_ok.rs:49:5: 49:36: error: in alias_ok/3a1fbbbh::use_f[0] -MIR assertion at test/symb_eval/comp/alias_ok.rs:49:5: - b.get() < 10 +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_ok.rs:49:5: 49:36: error: in alias_ok/3a1fbbbh::use_f[0] +[Crux] MIR assertion at test/symb_eval/comp/alias_ok.rs:49:5: +[Crux] b.get() < 10 [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/comp/clobber_globals.good b/crux-mir-comp/test/symb_eval/comp/clobber_globals.good index 1b7c4adc54..213876df76 100644 --- a/crux-mir-comp/test/symb_eval/comp/clobber_globals.good +++ b/crux-mir-comp/test/symb_eval/comp/clobber_globals.good @@ -4,13 +4,15 @@ test clobber_globals/3a1fbbbh::use_f[0]: FAILED failures: ---- clobber_globals/3a1fbbbh::f_test[0] counterexamples ---- -Failure for test/symb_eval/comp/clobber_globals.rs:16:9: 16:70: error: in clobber_globals/3a1fbbbh::f_test[0] -MIR assertion at test/symb_eval/comp/clobber_globals.rs:15:5: - expected failure; ATOMIC was clobbered by clobber_globals() +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/comp/clobber_globals.rs:16:9: 16:70: error: in clobber_globals/3a1fbbbh::f_test[0] +[Crux] MIR assertion at test/symb_eval/comp/clobber_globals.rs:15:5: +[Crux] expected failure; ATOMIC was clobbered by clobber_globals() ---- clobber_globals/3a1fbbbh::use_f[0] counterexamples ---- -Failure for test/symb_eval/comp/clobber_globals.rs:38:9: 38:61: error: in clobber_globals/3a1fbbbh::use_f[0] -MIR assertion at test/symb_eval/comp/clobber_globals.rs:37:5: - expected failure; ATOMIC was clobbered by f's spec +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/comp/clobber_globals.rs:38:9: 38:61: error: in clobber_globals/3a1fbbbh::use_f[0] +[Crux] MIR assertion at test/symb_eval/comp/clobber_globals.rs:37:5: +[Crux] expected failure; ATOMIC was clobbered by f's spec [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/comp/override_test_indep.good b/crux-mir-comp/test/symb_eval/comp/override_test_indep.good index 0ff68a7c37..bb6bb52b4d 100644 --- a/crux-mir-comp/test/symb_eval/comp/override_test_indep.good +++ b/crux-mir-comp/test/symb_eval/comp/override_test_indep.good @@ -6,8 +6,9 @@ test override_test_indep/3a1fbbbh::use_f3[0]: ok failures: ---- override_test_indep/3a1fbbbh::use_f2[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/override_test_indep.rs:57:5: 57:30: error: in override_test_indep/3a1fbbbh::use_f2[0] -MIR assertion at test/symb_eval/comp/override_test_indep.rs:57:5: - d < 10 +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/override_test_indep.rs:57:5: 57:30: error: in override_test_indep/3a1fbbbh::use_f2[0] +[Crux] MIR assertion at test/symb_eval/comp/override_test_indep.rs:57:5: +[Crux] d < 10 [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/comp/ptr_offset.good b/crux-mir-comp/test/symb_eval/comp/ptr_offset.good index 24abea7c73..8a7e2f9843 100644 --- a/crux-mir-comp/test/symb_eval/comp/ptr_offset.good +++ b/crux-mir-comp/test/symb_eval/comp/ptr_offset.good @@ -4,8 +4,9 @@ test ptr_offset/3a1fbbbh::use_f[0]: FAILED failures: ---- ptr_offset/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/ptr_offset.rs:64:5: 64:31: error: in ptr_offset/3a1fbbbh::use_f[0] -MIR assertion at test/symb_eval/comp/ptr_offset.rs:64:5: - b2 < 10 +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/ptr_offset.rs:64:5: 64:31: error: in ptr_offset/3a1fbbbh::use_f[0] +[Crux] MIR assertion at test/symb_eval/comp/ptr_offset.rs:64:5: +[Crux] b2 < 10 [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/comp/ptr_offset_rev.good b/crux-mir-comp/test/symb_eval/comp/ptr_offset_rev.good index a4f3e1443a..3894efcc99 100644 --- a/crux-mir-comp/test/symb_eval/comp/ptr_offset_rev.good +++ b/crux-mir-comp/test/symb_eval/comp/ptr_offset_rev.good @@ -4,8 +4,9 @@ test ptr_offset_rev/3a1fbbbh::use_f[0]: FAILED failures: ---- ptr_offset_rev/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/ptr_offset_rev.rs:64:5: 64:31: error: in ptr_offset_rev/3a1fbbbh::use_f[0] -MIR assertion at test/symb_eval/comp/ptr_offset_rev.rs:64:5: - b2 < 10 +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/ptr_offset_rev.rs:64:5: 64:31: error: in ptr_offset_rev/3a1fbbbh::use_f[0] +[Crux] MIR assertion at test/symb_eval/comp/ptr_offset_rev.rs:64:5: +[Crux] b2 < 10 [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/comp/spec_array.good b/crux-mir-comp/test/symb_eval/comp/spec_array.good index ed999d49cc..33689a3c34 100644 --- a/crux-mir-comp/test/symb_eval/comp/spec_array.good +++ b/crux-mir-comp/test/symb_eval/comp/spec_array.good @@ -4,8 +4,9 @@ test spec_array/3a1fbbbh::use_f[0]: FAILED failures: ---- spec_array/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_array.rs:43:5: 43:30: error: in spec_array/3a1fbbbh::use_f[0] -MIR assertion at test/symb_eval/comp/spec_array.rs:43:5: - d < 10 +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_array.rs:43:5: 43:30: error: in spec_array/3a1fbbbh::use_f[0] +[Crux] MIR assertion at test/symb_eval/comp/spec_array.rs:43:5: +[Crux] d < 10 [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/comp/spec_box.good b/crux-mir-comp/test/symb_eval/comp/spec_box.good index a2c48769a8..eea72e7978 100644 --- a/crux-mir-comp/test/symb_eval/comp/spec_box.good +++ b/crux-mir-comp/test/symb_eval/comp/spec_box.good @@ -4,8 +4,9 @@ test spec_box/3a1fbbbh::use_f[0]: FAILED failures: ---- spec_box/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_box.rs:58:5: 58:30: error: in spec_box/3a1fbbbh::use_f[0] -MIR assertion at test/symb_eval/comp/spec_box.rs:58:5: - d < 10 +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_box.rs:58:5: 58:30: error: in spec_box/3a1fbbbh::use_f[0] +[Crux] MIR assertion at test/symb_eval/comp/spec_box.rs:58:5: +[Crux] d < 10 [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/comp/spec_immut_cell.good b/crux-mir-comp/test/symb_eval/comp/spec_immut_cell.good index 748c1cfaf1..af2bacfa47 100644 --- a/crux-mir-comp/test/symb_eval/comp/spec_immut_cell.good +++ b/crux-mir-comp/test/symb_eval/comp/spec_immut_cell.good @@ -4,8 +4,9 @@ test spec_immut_cell/3a1fbbbh::use_f[0]: FAILED failures: ---- spec_immut_cell/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_immut_cell.rs:68:5: 68:36: error: in spec_immut_cell/3a1fbbbh::use_f[0] -MIR assertion at test/symb_eval/comp/spec_immut_cell.rs:68:5: - d.get() < 10 +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_immut_cell.rs:68:5: 68:36: error: in spec_immut_cell/3a1fbbbh::use_f[0] +[Crux] MIR assertion at test/symb_eval/comp/spec_immut_cell.rs:68:5: +[Crux] d.get() < 10 [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/comp/spec_mut.good b/crux-mir-comp/test/symb_eval/comp/spec_mut.good index 8f77f8a347..8f84e8592d 100644 --- a/crux-mir-comp/test/symb_eval/comp/spec_mut.good +++ b/crux-mir-comp/test/symb_eval/comp/spec_mut.good @@ -4,8 +4,9 @@ test spec_mut/3a1fbbbh::use_f[0]: FAILED failures: ---- spec_mut/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_mut.rs:61:5: 61:30: error: in spec_mut/3a1fbbbh::use_f[0] -MIR assertion at test/symb_eval/comp/spec_mut.rs:61:5: - d < 10 +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_mut.rs:61:5: 61:30: error: in spec_mut/3a1fbbbh::use_f[0] +[Crux] MIR assertion at test/symb_eval/comp/spec_mut.rs:61:5: +[Crux] d < 10 [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/comp/spec_mut_slice.good b/crux-mir-comp/test/symb_eval/comp/spec_mut_slice.good index 216a99488c..79a5647efd 100644 --- a/crux-mir-comp/test/symb_eval/comp/spec_mut_slice.good +++ b/crux-mir-comp/test/symb_eval/comp/spec_mut_slice.good @@ -4,8 +4,9 @@ test spec_mut_slice/3a1fbbbh::use_f[0]: FAILED failures: ---- spec_mut_slice/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_mut_slice.rs:48:5: 48:30: error: in spec_mut_slice/3a1fbbbh::use_f[0] -MIR assertion at test/symb_eval/comp/spec_mut_slice.rs:48:5: - d < 10 +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_mut_slice.rs:48:5: 48:30: error: in spec_mut_slice/3a1fbbbh::use_f[0] +[Crux] MIR assertion at test/symb_eval/comp/spec_mut_slice.rs:48:5: +[Crux] d < 10 [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/comp/spec_struct.good b/crux-mir-comp/test/symb_eval/comp/spec_struct.good index 14c90992be..75595f1177 100644 --- a/crux-mir-comp/test/symb_eval/comp/spec_struct.good +++ b/crux-mir-comp/test/symb_eval/comp/spec_struct.good @@ -4,8 +4,9 @@ test spec_struct/3a1fbbbh::use_f[0]: FAILED failures: ---- spec_struct/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_struct.rs:51:5: 51:30: error: in spec_struct/3a1fbbbh::use_f[0] -MIR assertion at test/symb_eval/comp/spec_struct.rs:51:5: - d < 10 +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_struct.rs:51:5: 51:30: error: in spec_struct/3a1fbbbh::use_f[0] +[Crux] MIR assertion at test/symb_eval/comp/spec_struct.rs:51:5: +[Crux] d < 10 [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/comp/spec_tuple.good b/crux-mir-comp/test/symb_eval/comp/spec_tuple.good index 40b8421d77..7f14b0cbe9 100644 --- a/crux-mir-comp/test/symb_eval/comp/spec_tuple.good +++ b/crux-mir-comp/test/symb_eval/comp/spec_tuple.good @@ -4,8 +4,9 @@ test spec_tuple/3a1fbbbh::use_f[0]: FAILED failures: ---- spec_tuple/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_tuple.rs:55:5: 55:30: error: in spec_tuple/3a1fbbbh::use_f[0] -MIR assertion at test/symb_eval/comp/spec_tuple.rs:55:5: - d < 10 +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_tuple.rs:55:5: 55:30: error: in spec_tuple/3a1fbbbh::use_f[0] +[Crux] MIR assertion at test/symb_eval/comp/spec_tuple.rs:55:5: +[Crux] d < 10 [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/comp/subst_output.good b/crux-mir-comp/test/symb_eval/comp/subst_output.good index bbef7163e0..320b522db7 100644 --- a/crux-mir-comp/test/symb_eval/comp/subst_output.good +++ b/crux-mir-comp/test/symb_eval/comp/subst_output.good @@ -3,8 +3,9 @@ test subst_output/3a1fbbbh::use_f[0]: FAILED failures: ---- subst_output/3a1fbbbh::use_f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/subst_output.rs:32:5: 32:31: error: in subst_output/3a1fbbbh::use_f[0] -MIR assertion at test/symb_eval/comp/subst_output.rs:32:5: - b0 == a +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/subst_output.rs:32:5: 32:31: error: in subst_output/3a1fbbbh::use_f[0] +[Crux] MIR assertion at test/symb_eval/comp/subst_output.rs:32:5: +[Crux] b0 == a [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.good b/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.good index e51bd6c38a..f163eda5e2 100644 --- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.good +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.good @@ -3,7 +3,8 @@ test basic_err_array_size/3a1fbbbh::test[0]: FAILED failures: ---- basic_err_array_size/3a1fbbbh::test[0] counterexamples ---- -Failure for test/symb_eval/cryptol/basic_err_array_size.rs:8:52: 8:62: error: in basic_err_array_size/3a1fbbbh::test[0] -error loading "arrayArg": type mismatch in argument 0: Cryptol type [2][8] does not match Rust type u8: array length 2 does not match 3 +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/cryptol/basic_err_array_size.rs:8:52: 8:62: error: in basic_err_array_size/3a1fbbbh::test[0] +[Crux] error loading "arrayArg": type mismatch in argument 0: Cryptol type [2][8] does not match Rust type u8: array length 2 does not match 3 [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.good b/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.good index 91e48799df..8493dc696f 100644 --- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.good +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.good @@ -3,7 +3,8 @@ test basic_err_bv_size/3a1fbbbh::test[0]: FAILED failures: ---- basic_err_bv_size/3a1fbbbh::test[0] counterexamples ---- -Failure for test/symb_eval/cryptol/basic_err_bv_size.rs:8:52: 8:61: error: in basic_err_bv_size/3a1fbbbh::test[0] -error loading "addByte": type mismatch in argument 1: Cryptol type [8] does not match Rust type u16: bitvector width 8 does not match 16 +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/cryptol/basic_err_bv_size.rs:8:52: 8:61: error: in basic_err_bv_size/3a1fbbbh::test[0] +[Crux] error loading "addByte": type mismatch in argument 1: Cryptol type [8] does not match Rust type u16: bitvector width 8 does not match 16 [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.good b/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.good index 33a1560602..163b4550e2 100644 --- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.good +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.good @@ -3,7 +3,8 @@ test basic_err_fewer_args/3a1fbbbh::test[0]: FAILED failures: ---- basic_err_fewer_args/3a1fbbbh::test[0] counterexamples ---- -Failure for test/symb_eval/cryptol/basic_err_fewer_args.rs:8:55: 8:64: error: in basic_err_fewer_args/3a1fbbbh::test[0] -error loading "addByte": not enough arguments: Cryptol function signature [8] -> [8] -> [8] has 2 arguments, but Rust signature (u8, u8, u8) -> u8 [RustAbi] requires 3 +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/cryptol/basic_err_fewer_args.rs:8:55: 8:64: error: in basic_err_fewer_args/3a1fbbbh::test[0] +[Crux] error loading "addByte": not enough arguments: Cryptol function signature [8] -> [8] -> [8] has 2 arguments, but Rust signature (u8, u8, u8) -> u8 [RustAbi] requires 3 [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.good b/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.good index 58cf2455e2..2889838baa 100644 --- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.good +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.good @@ -3,7 +3,8 @@ test basic_err_mismatch/3a1fbbbh::test[0]: FAILED failures: ---- basic_err_mismatch/3a1fbbbh::test[0] counterexamples ---- -Failure for test/symb_eval/cryptol/basic_err_mismatch.rs:8:51: 8:60: error: in basic_err_mismatch/3a1fbbbh::test[0] -error loading "addByte": type mismatch in argument 1: Cryptol type [8] does not match Rust type () +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/cryptol/basic_err_mismatch.rs:8:51: 8:60: error: in basic_err_mismatch/3a1fbbbh::test[0] +[Crux] error loading "addByte": type mismatch in argument 1: Cryptol type [8] does not match Rust type () [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.good b/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.good index 786dba7433..0f0d469dbf 100644 --- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.good +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.good @@ -3,7 +3,8 @@ test basic_err_more_args/3a1fbbbh::test[0]: FAILED failures: ---- basic_err_more_args/3a1fbbbh::test[0] counterexamples ---- -Failure for test/symb_eval/cryptol/basic_err_more_args.rs:8:47: 8:56: error: in basic_err_more_args/3a1fbbbh::test[0] -error loading "addByte": type mismatch in return value: Cryptol type [8] -> [8] does not match Rust type u8 +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/cryptol/basic_err_more_args.rs:8:47: 8:56: error: in basic_err_more_args/3a1fbbbh::test[0] +[Crux] error loading "addByte": type mismatch in return value: Cryptol type [8] -> [8] does not match Rust type u8 [Crux] Overall status: Invalid. diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.good b/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.good index 6e7111b5a2..c78e6f459c 100644 --- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.good +++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.good @@ -3,7 +3,8 @@ test basic_err_tuple_size/3a1fbbbh::test[0]: FAILED failures: ---- basic_err_tuple_size/3a1fbbbh::test[0] counterexamples ---- -Failure for test/symb_eval/cryptol/basic_err_tuple_size.rs:8:57: 8:67: error: in basic_err_tuple_size/3a1fbbbh::test[0] -error loading "tupleArg": type mismatch in argument 0: Cryptol type ([8], [8]) does not match Rust type (u8, u8, u8): tuple size 2 does not match 3 +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/cryptol/basic_err_tuple_size.rs:8:57: 8:67: error: in basic_err_tuple_size/3a1fbbbh::test[0] +[Crux] error loading "tupleArg": type mismatch in argument 0: Cryptol type ([8], [8]) does not match Rust type (u8, u8, u8): tuple size 2 does not match 3 [Crux] Overall status: Invalid. From c035eab15e8e7ec21411f8ea1932ccf3d5ef5655 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Mon, 28 Jun 2021 10:50:35 -0700 Subject: [PATCH 34/34] update for TypedTerm ttSchema changes --- crux-mir-comp/src/Mir/Cryptol.hs | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index 39f775135f..72685416fb 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -232,7 +232,7 @@ loadCryptolFunc col sig modulePath name = do tt <- liftIO $ SAW.parseTypedTerm sc ce' $ SAW.InputText (Text.unpack name) "" 1 1 - case typecheckFnSig sig (toListFC Some argShps) (Some retShp) (SAW.ttSchema tt) of + case typecheckFnSig sig (toListFC Some argShps) (Some retShp) (SAW.ttType tt) of Left err -> fail $ "error loading " ++ show name ++ ": " ++ err Right () -> return () @@ -353,9 +353,10 @@ typecheckFnSig :: M.FnSig -> [Some TypeShape] -> Some TypeShape -> - Cry.Schema -> + SAW.TypedTermType -> Either String () -typecheckFnSig fnSig argShps retShp sch@(Cry.Forall [] [] ty) = go 0 argShps ty +typecheckFnSig fnSig argShps retShp (SAW.TypedTermSchema sch@(Cry.Forall [] [] ty)) = + go 0 argShps ty where go :: Int -> [Some TypeShape] -> Cry.Type -> Either String () go _ [] ty | Some retShp' <- retShp = goOne "return value" retShp' ty @@ -404,6 +405,9 @@ typecheckFnSig fnSig argShps retShp sch@(Cry.Forall [] [] ty) = go 0 argShps ty goOneField desc (OptField shp) ty = goOne desc shp ty goOneField desc (ReqField shp) ty = goOne desc shp ty -typecheckFnSig _ _ _ sch = Left $ +typecheckFnSig _ _ _ (SAW.TypedTermSchema sch) = Left $ "polymorphic Cryptol functions are not supported (got signature: " ++ show (Cry.pp sch) ++ ")" + +typecheckFnSig _ _ _ ttt = Left $ + "internal error: unsupported TypedTermType variant: " ++ show ttt