From 2459422b0545623f9f61f8d236c396c96a487e77 Mon Sep 17 00:00:00 2001 From: Joel Burget Date: Thu, 28 Feb 2019 14:44:35 -0800 Subject: [PATCH] Update to latest sbv. * We're now back on Levent's sbv (:tada:) * When SBV 8.1 is released we can switch to it to be back on a hackage release * We now add names to all allocations to make debugging much easier * The quantified variables issue that's been haunting us since forever is finally fixed (see https://github.com/LeventErkok/sbv/issues/459) * We now need to add `Ord` constraints in some places due to sbv changes. --- default.nix | 8 ++--- src/Pact/Analyze/Alloc.hs | 36 ++++++++++---------- src/Pact/Analyze/Check.hs | 21 +++++++----- src/Pact/Analyze/Eval/Core.hs | 4 +-- src/Pact/Analyze/Eval/Prop.hs | 8 ++--- src/Pact/Analyze/Model/Tags.hs | 53 ++++++++++++++++------------- src/Pact/Analyze/PrenexNormalize.hs | 2 +- src/Pact/Analyze/Types/Shared.hs | 26 +++++++++++--- stack.yaml | 7 ++-- 9 files changed, 96 insertions(+), 69 deletions(-) diff --git a/default.nix b/default.nix index e6b88b929..43028d30b 100644 --- a/default.nix +++ b/default.nix @@ -88,12 +88,12 @@ in hlint = self.callHackage "hlint" "2.0.14" {}; # hoogle = self.callHackage "hoogle" "5.0.15" {}; - # sbv with a patch to disable "unsupported query call" until it's fixed upstream + # this is pre-sbv-8.1 (switch when it's released) sbv = dontCheck (self.callCabal2nix "sbv" (pkgs.fetchFromGitHub { - owner = "joelburget"; + owner = "LeventErkok"; repo = "sbv"; - rev = "25d9357ff8eaac697eb6fde96598d7beb587b4e9"; - sha256 = "0i0ajrw8j9hc208hizi4rnj5giqhbawjfgdbacswwfvgfqvvb69z"; + rev = "68375576f87d17a2da759c56f7147f4e559471a2"; + sha256 = "11qmgc8jnsx1m2hy3x28ihl941ik4wsdpj0bkbsz226zncad13dp"; }) {}); # need crackNum 2.3 diff --git a/src/Pact/Analyze/Alloc.hs b/src/Pact/Analyze/Alloc.hs index 7f865a6ed..32a77bcfc 100644 --- a/src/Pact/Analyze/Alloc.hs +++ b/src/Pact/Analyze/Alloc.hs @@ -33,33 +33,33 @@ import Pact.Analyze.Types (Concrete, S, SingI (sing), SingTy, -- is permitted. class Monad m => MonadAlloc m where - singForAll :: SingTy a -> m (S (Concrete a)) -- ^ universally quantified - singExists :: SingTy a -> m (S (Concrete a)) -- ^ existentially quantified - singFree :: SingTy a -> m (S (Concrete a)) -- ^ quantified per the context of sat vs prove + singForAll :: String -> SingTy a -> m (S (Concrete a)) -- ^ universally quantified + singExists :: String -> SingTy a -> m (S (Concrete a)) -- ^ existentially quantified + singFree :: String -> SingTy a -> m (S (Concrete a)) -- ^ quantified per the context of sat vs prove default singForAll :: (MonadTrans t, MonadAlloc m', m ~ t m') - => SingTy a -> m (S (Concrete a)) - singForAll ty = lift (singForAll ty) + => String -> SingTy a -> m (S (Concrete a)) + singForAll name ty = lift (singForAll name ty) default singExists :: (MonadTrans t, MonadAlloc m', m ~ t m') - => SingTy a -> m (S (Concrete a)) - singExists ty = lift (singExists ty) + => String -> SingTy a -> m (S (Concrete a)) + singExists name ty = lift (singExists name ty) default singFree :: (MonadTrans t, MonadAlloc m', m ~ t m') - => SingTy a -> m (S (Concrete a)) - singFree = lift . singFree + => String -> SingTy a -> m (S (Concrete a)) + singFree name = lift . singFree name -forAll :: forall a m. (MonadAlloc m, SingI a) => m (S (Concrete a)) -forAll = singForAll (sing @a) +forAll :: forall a m. (MonadAlloc m, SingI a) => String -> m (S (Concrete a)) +forAll name = singForAll name (sing @a) -exists :: forall a m. (MonadAlloc m, SingI a) => m (S (Concrete a)) -exists = singExists (sing @a) +exists :: forall a m. (MonadAlloc m, SingI a) => String -> m (S (Concrete a)) +exists name = singExists name (sing @a) -free :: forall a m. (MonadAlloc m, SingI a) => m (S (Concrete a)) -free = singFree (sing @a) +free :: forall a m. (MonadAlloc m, SingI a) => String -> m (S (Concrete a)) +free name = singFree name (sing @a) instance MonadAlloc m => MonadAlloc (ExceptT e m) instance MonadAlloc m => MonadAlloc (MaybeT m) @@ -78,6 +78,6 @@ newtype Alloc a = Alloc { runAlloc :: Symbolic a } deriving (Functor, Applicative, Monad) instance MonadAlloc Alloc where - singForAll ty = Alloc $ withSymVal ty $ sansProv <$> SBV.forall_ - singExists ty = Alloc $ withSymVal ty $ sansProv <$> SBV.exists_ - singFree ty = Alloc $ withSymVal ty $ sansProv <$> SBV.free_ + singForAll name ty = Alloc $ withSymVal ty $ sansProv <$> SBV.forall name + singExists name ty = Alloc $ withSymVal ty $ sansProv <$> SBV.exists name + singFree name ty = Alloc $ withSymVal ty $ sansProv <$> SBV.free name diff --git a/src/Pact/Analyze/Check.hs b/src/Pact/Analyze/Check.hs index d256c69af..612348e92 100644 --- a/src/Pact/Analyze/Check.hs +++ b/src/Pact/Analyze/Check.hs @@ -302,7 +302,7 @@ verifyFunctionInvariants' modName funName funInfo tables caps pactArgs body = ru ExceptT $ catchingExceptions $ runSymbolic $ runExceptT $ do lift $ SBV.setTimeOut 1000 -- one second modelArgs' <- lift $ runAlloc $ allocArgs args - tags <- lift $ runAlloc $ allocModelTags modelArgs' (Located funInfo tm) graph + tags <- lift $ runAlloc $ allocModelTags modelArgs' (Located funInfo tm) graph let rootPath = _egRootPath graph resultsTable <- withExceptT analyzeToCheckFailure $ runInvariantAnalysis modName tables caps (analysisArgs modelArgs') tm @@ -333,7 +333,7 @@ verifyFunctionInvariants' modName funName funInfo tables caps pactArgs body = ru goal = Validation config :: SBV.SMTConfig - config = SBV.z3 -- { SBVI.verbose = True } + config = SBV.z3 { SBVI.allowQuantifiedQueries = True } -- , SBVI.verbose = True } -- Discharges impure 'SBVException's from sbv. catchingExceptions @@ -363,33 +363,35 @@ verifyFunctionProperty modName funName funInfo tables caps pactArgs body (Locate ExceptT $ catchingExceptions $ runSymbolic $ runExceptT $ do lift $ SBV.setTimeOut 1000 -- one second modelArgs' <- lift $ runAlloc $ allocArgs args - tags <- lift $ runAlloc $ allocModelTags modelArgs' (Located funInfo tm) graph + tags <- lift $ runAlloc $ allocModelTags modelArgs' (Located funInfo tm) graph let rootPath = _egRootPath graph AnalysisResult _querySucceeds prop ksProvs <- withExceptT analyzeToCheckFailure $ runPropertyAnalysis modName check tables caps (analysisArgs modelArgs') tm rootPath tags funInfo + let model = Model modelArgs' tags ksProvs graph + -- TODO: bring back the query success check when we've resolved the SBV -- query / quantified variables issue: -- https://github.com/LeventErkok/sbv/issues/407 -- -- _ <- hoist SBV.query $ do - -- void $ lift $ SBV.constrain $ SBV.bnot $ successBool querySucceeds - -- withExceptT (smtToQueryFailure (getInfo check)) $ + -- void $ lift $ SBV.constrain $ SBV.sNot $ successBool querySucceeds + -- withExceptT (smtToQueryFailure propInfo) $ -- resultQuery Validation model void $ lift $ SBV.output prop hoist SBV.query $ withExceptT (smtToCheckFailure propInfo) $ - resultQuery goal $ Model modelArgs' tags ksProvs graph + resultQuery goal model where goal :: Goal goal = checkGoal check config :: SBV.SMTConfig - config = SBV.z3 -- { SBVI.verbose = True } + config = SBV.z3 { SBVI.allowQuantifiedQueries = True } -- , SBVI.verbose = True } -- Discharges impure 'SBVException's from sbv. catchingExceptions @@ -400,7 +402,7 @@ verifyFunctionProperty modName funName funInfo tables caps pactArgs body (Locate runSymbolic :: Symbolic a -> IO a runSymbolic = fmap fst . - SBVI.runSymbolic (SBVI.SMTMode SBVI.ISetup (goal == Satisfaction) config) + SBVI.runSymbolic (SBVI.SMTMode SBVI.QueryExternal SBVI.ISetup (goal == Satisfaction) config) moduleTables :: HM.HashMap ModuleName ModuleData -- ^ all loaded modules @@ -855,5 +857,6 @@ verifyCheck moduleData funName check = do tables <- withExceptT ModuleParseFailure $ moduleTables modules moduleData case moduleFun moduleData funName of Just funRef -> ExceptT $ - Right . head <$> verifyFunctionProps moduleName tables caps funRef funName [Located info check] + Right . head <$> verifyFunctionProps moduleName tables caps funRef funName + [Located info check] Nothing -> pure $ Left $ CheckFailure info $ NotAFunction funName diff --git a/src/Pact/Analyze/Eval/Core.hs b/src/Pact/Analyze/Eval/Core.hs index fa761fbb2..8aefdc7f5 100644 --- a/src/Pact/Analyze/Eval/Core.hs +++ b/src/Pact/Analyze/Eval/Core.hs @@ -99,7 +99,7 @@ evalComparisonOp -> TermOf m a -> TermOf m a -> m (S Bool) -evalComparisonOp ty op xT yT = do +evalComparisonOp ty op xT yT = withOrd ty $ do x <- withSing ty $ eval xT y <- withSing ty $ eval yT let f :: SymVal (Concrete a) => SBV Bool @@ -254,7 +254,7 @@ evalCore (ListConcat ty p1 p2) = withSymVal ty $ withSing ty $ do evalCore (ListReverse ty l) = withSymVal ty $ withSing ty $ do S prov l' <- eval l pure $ S prov $ breverse listBound l' -evalCore (ListSort ty l) = withSymVal ty $ withSing ty $ do +evalCore (ListSort ty l) = withSymVal ty $ withSing ty $ withOrd ty $ do S prov l' <- eval l pure $ S prov $ bsort listBound l' evalCore (MakeList ty i a) = withSymVal ty $ withSing ty $ do diff --git a/src/Pact/Analyze/Eval/Prop.hs b/src/Pact/Analyze/Eval/Prop.hs index 007ea4f17..5e55e9ce6 100644 --- a/src/Pact/Analyze/Eval/Prop.hs +++ b/src/Pact/Analyze/Eval/Prop.hs @@ -115,8 +115,8 @@ evalPropSpecific :: PropSpecific a -> Query (S (Concrete a)) evalPropSpecific Success = view $ qeAnalyzeState.succeeds evalPropSpecific Abort = sNot <$> evalPropSpecific Success evalPropSpecific Result = aval (pure ... mkS) =<< view qeAnalyzeResult -evalPropSpecific (Forall vid _name (EType (ty :: Types.SingTy ty)) p) = do - var <- singForAll ty +evalPropSpecific (Forall vid name (EType (ty :: Types.SingTy ty)) p) = do + var <- singForAll ("forall_" ++ T.unpack name) ty local (scope.at vid ?~ mkAVal var) $ evalProp p evalPropSpecific (Forall vid _name QTable prop) = do TableMap tables <- view (analyzeEnv . invariants) @@ -129,8 +129,8 @@ evalPropSpecific (Forall vid _name (QColumnOf tabName) prop) = do let colName' = ColumnName $ T.unpack colName in local (qeColumnScope . at vid ?~ colName') (evalProp prop) pure $ foldr (.&&) sTrue bools -evalPropSpecific (Exists vid _name (EType (ty :: Types.SingTy ty)) p) = do - var <- singExists ty +evalPropSpecific (Exists vid name (EType (ty :: Types.SingTy ty)) p) = do + var <- singExists ("exists_" ++ T.unpack name) ty local (scope.at vid ?~ mkAVal var) $ evalProp p evalPropSpecific (Exists vid _name QTable prop) = do TableMap tables <- view (analyzeEnv . invariants) diff --git a/src/Pact/Analyze/Model/Tags.hs b/src/Pact/Analyze/Model/Tags.hs index ea2bfef18..b50dc65c4 100644 --- a/src/Pact/Analyze/Model/Tags.hs +++ b/src/Pact/Analyze/Model/Tags.hs @@ -30,7 +30,7 @@ import Data.SBV (SBV, SymVal) import qualified Data.SBV as SBV import qualified Data.SBV.Control as SBV import qualified Data.SBV.Internals as SBVI -import Data.Text (pack) +import Data.Text (pack, unpack) import Data.Traversable (for) import GHC.TypeLits (symbolVal) @@ -39,32 +39,36 @@ import qualified Pact.Types.Typecheck as TC import Pact.Analyze.Alloc (Alloc, free, singFree) import Pact.Analyze.Types -allocS :: forall a. SingI a => Alloc (S (Concrete a)) -allocS = free @a +allocS :: forall a. SingI a => String -> Alloc (S (Concrete a)) +allocS name = free @a ("tag_" ++ name) -allocSbv :: forall a. SingI a => Alloc (SBV (Concrete a)) -allocSbv = _sSbv <$> allocS @a +allocSbv :: forall a. SingI a => String -> Alloc (SBV (Concrete a)) +allocSbv name = _sSbv <$> allocS @a name allocSchema :: SingList schema -> Alloc UObject allocSchema = fmap UObject . allocSchema' where allocSchema' = foldrSingList (pure Map.empty) $ \k ty m -> do - let ety = EType ty - val <- allocAVal ety - Map.insert (pack (symbolVal k)) (ety, val) <$> m + let ety = EType ty + name = symbolVal k + val <- allocAVal name ety + Map.insert (pack name) (ety, val) <$> m -allocAVal :: EType -> Alloc AVal -allocAVal (EType ty) = mkAVal <$> singFree ty +allocAVal :: String -> EType -> Alloc AVal +allocAVal name (EType ty) = mkAVal <$> singFree name ty -allocTVal :: EType -> Alloc TVal -allocTVal ety = (ety,) <$> allocAVal ety +allocTVal :: String -> EType -> Alloc TVal +allocTVal name ety = (ety,) <$> allocAVal name ety -allocForETerm :: ETerm -> Alloc TVal -allocForETerm (existentialType -> ety) = allocTVal ety +allocForETerm :: String -> ETerm -> Alloc TVal +allocForETerm name (existentialType -> ety) = allocTVal name ety + +unmungedStr :: Unmunged -> String +unmungedStr (Unmunged name) = unpack name allocArgs :: [Arg] -> Alloc (Map VarId (Located (Unmunged, TVal))) allocArgs args = fmap Map.fromList $ for args $ \(Arg nm vid node ety) -> do let info = node ^. TC.aId . TC.tiInfo - av <- allocAVal ety <&> _AVal._1 ?~ FromInput nm + av <- allocAVal (unmungedStr nm) ety <&> _AVal._1 ?~ FromInput nm pure (vid, Located info (nm, (ety, av))) allocModelTags @@ -98,7 +102,8 @@ allocModelTags argsMap locatedTm graph = ModelTags for (toListOf (traverse._TracePushScope._3.traverse) events) $ \(Located info (Binding vid nm _ ety)) -> case Map.lookup vid argsMap of - Nothing -> allocTVal ety <&> \tv -> (vid, Located info (nm, tv)) + Nothing -> allocTVal ("binding_" ++ unmungedStr nm) ety <&> + \tv -> (vid, Located info (nm, tv)) Just arg -> pure (vid, arg) allocAccesses @@ -107,9 +112,9 @@ allocModelTags argsMap locatedTm graph = ModelTags allocAccesses p = fmap Map.fromList $ for (toListOf (traverse.p) events) $ \(ESchema schema, Located info tid) -> do - srk <- allocS @TyRowKey + srk <- allocS @TyRowKey "row_key" obj <- allocSchema schema - suc <- allocSbv @'TyBool + suc <- allocSbv @'TyBool "access_success" pure (tid, Located info (Access srk obj suc)) allocReads :: Alloc (Map TagId (Located Access)) @@ -127,18 +132,20 @@ allocModelTags argsMap locatedTm graph = ModelTags allocAsserts :: Alloc (Map TagId (Located (SBV Bool))) allocAsserts = fmap Map.fromList $ for (toListOf (traverse._TraceAssert._2) events) $ \(Located info tid) -> - (tid,) . Located info <$> allocSbv @'TyBool + (tid,) . Located info <$> allocSbv @'TyBool "assert" allocGEs :: Alloc (Map TagId (Located GuardEnforcement)) allocGEs = fmap Map.fromList $ for (toListOf (traverse._TraceGuard._2) events) $ \(Located info tid) -> (tid,) . Located info <$> - (GuardEnforcement <$> allocS @'TyGuard <*> allocSbv @'TyBool) + (GuardEnforcement + <$> allocS @'TyGuard "guard" + <*> allocSbv @'TyBool "guard_success") allocResult :: Alloc (TagId, Located TVal) allocResult = do let tid :: TagId = last $ toListOf (traverse._TracePopScope._3) events - fmap (tid,) $ sequence $ allocForETerm <$> locatedTm + fmap (tid,) $ sequence $ allocForETerm "result" <$> locatedTm -- NOTE: the root path we manually set to true. translation only emits the -- start of "subpaths" on either side of a conditional. the root path is @@ -148,12 +155,12 @@ allocModelTags argsMap locatedTm graph = ModelTags allocPaths = do let rootPath = _egRootPath graph paths = rootPath : toListOf (traverse._TraceSubpathStart) events - Map.fromList <$> for paths (\p -> (p,) <$> allocSbv @'TyBool) + Map.fromList <$> for paths (\p -> (p,) <$> allocSbv @'TyBool "path") allocReturns :: Alloc (Map TagId TVal) allocReturns = fmap Map.fromList $ for (toListOf (traverse._TracePopScope) events) $ \(_, _, tid, ety) -> - (tid,) <$> allocTVal ety + (tid,) <$> allocTVal "trace_pop_scope" ety -- | Builds a new 'Model' by querying the SMT model to concretize the provided -- symbolic 'Model'. diff --git a/src/Pact/Analyze/PrenexNormalize.hs b/src/Pact/Analyze/PrenexNormalize.hs index 80ca73313..77fe0a82a 100644 --- a/src/Pact/Analyze/PrenexNormalize.hs +++ b/src/Pact/Analyze/PrenexNormalize.hs @@ -126,7 +126,7 @@ singFloat ty p = case p of -- - logical CoreProp (Logical AndOp [a, b]) -> PAnd <$> float a <*> float b - CoreProp (Logical OrOp [a, b]) -> POr <$> float a <*> float b + CoreProp (Logical OrOp [a, b]) -> POr <$> float a <*> float b CoreProp (Logical NotOp [a]) -> bimap (fmap flipQuantifier) PNot (float a) CoreProp (Logical _ _) -> error ("ill-defined logical op: " ++ showTm p) CoreProp (AndQ ty' f g a) -> CoreProp <$> diff --git a/src/Pact/Analyze/Types/Shared.hs b/src/Pact/Analyze/Types/Shared.hs index 04c8b574e..1f18d9b2a 100644 --- a/src/Pact/Analyze/Types/Shared.hs +++ b/src/Pact/Analyze/Types/Shared.hs @@ -361,7 +361,7 @@ instance (SymVal a) => Mergeable (S a) where instance EqSymbolic (S a) where S _ x .== S _ y = x .== y -instance SymVal a => OrdSymbolic (S a) where +instance (Ord a, SymVal a) => OrdSymbolic (S a) where S _ x .< S _ y = x .< y instance Boolean (S Bool) where @@ -400,7 +400,7 @@ instance {-# OVERLAPPING #-} Num (S Decimal) where fromInteger i = sansProv $ fromInteger i negate (S _ x) = sansProv $ negate x -instance (Num a, SymVal a) => Num (S a) where +instance (Num a, Ord a, SymVal a) => Num (S a) where S _ x + S _ y = sansProv $ x + y S _ x * S _ y = sansProv $ x * y abs (S _ x) = sansProv $ abs x @@ -414,7 +414,7 @@ instance {-# OVERLAPPING #-} Fractional (S Decimal) where fromRational = literalS . fromRational S _ x / S _ y = sansProv $ x / y -instance (Fractional a, SymVal a) => Fractional (S a) where +instance (Fractional a, Ord a, SymVal a) => Fractional (S a) where fromRational = literalS . fromRational S _ x / S _ y = sansProv $ x / y @@ -636,7 +636,7 @@ fromIntegralS -> S b fromIntegralS = over s2Sbv sFromIntegral -oneIfS :: (Num a, SymVal a) => S Bool -> S a +oneIfS :: (Num a, Ord a, SymVal a) => S Bool -> S a oneIfS = over s2Sbv oneIf isConcreteS :: SymVal a => S a -> Bool @@ -870,6 +870,24 @@ withEq = withDict . singMkEq SObjectUnsafe (SCons' _ ty' tys) -> withEq ty' $ withDict (singMkEq (SObjectUnsafe tys)) Dict +withOrd :: SingTy a -> (Ord (Concrete a) => b) -> b +withOrd = withDict . singMkOrd + where + + singMkOrd :: SingTy a -> Dict (Ord (Concrete a)) + singMkOrd = \case + SInteger -> Dict + SBool -> Dict + SStr -> Dict + STime -> Dict + SDecimal -> Dict + SGuard -> Dict + SAny -> Dict + SList ty' -> withOrd ty' Dict + SObjectUnsafe SNil' -> Dict + SObjectUnsafe (SCons' _ ty' tys) + -> withOrd ty' $ withDict (singMkOrd (SObjectUnsafe tys)) Dict + withShow :: SingTy a -> (Show (Concrete a) => b) -> b withShow = withDict . singMkShow where diff --git a/stack.yaml b/stack.yaml index bc5e51100..097ee818c 100644 --- a/stack.yaml +++ b/stack.yaml @@ -16,7 +16,6 @@ extra-deps: - git: https://github.com/kadena-io/thyme.git commit: 6ee9fcb026ebdb49b810802a981d166680d867c9 - constraints-extras-0.2.0.0 - # temporarily using a patched fork of sbv to disable "unsupported query call" - # until it's fixed upstream - - git: https://github.com/joelburget/sbv.git - commit: 8d13e26255178c5ee5b5b3fad97873ff214d7470 + # this is pre-sbv-8.1 (switch when it's released) + - git: https://github.com/LeventErkok/sbv.git + commit: 68375576f87d17a2da759c56f7147f4e559471a2