{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE LambdaCase #-} module SymFnTests where import Control.Monad.IO.Class ( MonadIO, liftIO ) import Data.Parameterized.Classes ( ShowF(..) ) import Data.Parameterized.Context ( pattern (:>), (!) ) import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.Nonce import Data.Parameterized.Some import Data.Parameterized.TraversableFC import qualified Data.String as String import qualified Data.Text as T import qualified Data.Map as Map import qualified Data.Map.Ordered as OMap import Hedgehog import qualified LibBF as BF import Test.Tasty import Test.Tasty.Hedgehog hiding (testProperty) import SerializeTestUtils import qualified What4.Expr.Builder as S import What4.BaseTypes import qualified What4.Interface as WI import qualified What4.Serialize.Printer as WOUT import qualified What4.Serialize.Parser as WIN import qualified What4.Serialize.FastSExpr as WSF import Prelude symFnTests :: [TestTree] symFnTests = [ testGroup "SymFns" (mconcat [ testBasicArguments WIN.parseSExpr , testFunctionCalls WIN.parseSExpr , testExpressions WIN.parseSExpr , testBasicArguments WSF.parseSExpr , testFunctionCalls WSF.parseSExpr , testExpressions WSF.parseSExpr ]) ] data BuilderData t = NoBuilderData floatSinglePrecision :: FloatPrecisionRepr Prec32 floatSinglePrecision = knownRepr floatSingleType :: BaseTypeRepr (BaseFloatType Prec32) floatSingleType = BaseFloatRepr floatSinglePrecision testBasicArguments :: (T.Text -> Either String WIN.SExpr) -> [TestTree] testBasicArguments parseSExpr = [ testProperty "same argument type" $ withTests 1 $ property $ mkEquivalenceTest parseSExpr (Ctx.empty :> BaseIntegerRepr :> BaseIntegerRepr) $ \sym bvs -> do let i1 = bvs ! Ctx.i1of2 let i2 = bvs ! Ctx.i2of2 WI.intAdd sym i1 i2 , testProperty "different argument types" $ withTests 1 $ property $ mkEquivalenceTest parseSExpr (Ctx.empty :> BaseIntegerRepr :> BaseBoolRepr) $ \sym bvs -> do let i1 = bvs ! Ctx.i1of2 let b1 = bvs ! Ctx.i2of2 WI.baseTypeIte sym b1 i1 i1 ] testFunctionCalls :: (T.Text -> Either String WIN.SExpr) -> [TestTree] testFunctionCalls parseSExpr = [ testProperty "no arguments" $ withTests 1 $ property $ mkEquivalenceTest parseSExpr Ctx.empty $ \sym _ -> do ufn <- WI.freshTotalUninterpFn sym (WI.safeSymbol "ufn") Ctx.empty BaseBoolRepr WI.applySymFn sym ufn Ctx.empty , testProperty "two inner arguments" $ withTests 1 $ property $ mkEquivalenceTest parseSExpr Ctx.empty $ \sym _ -> do i1 <- WI.intLit sym 0 let b1 = WI.truePred sym ufn <- WI.freshTotalUninterpFn sym (WI.safeSymbol "ufn") (Ctx.empty :> BaseIntegerRepr :> BaseBoolRepr) BaseBoolRepr WI.applySymFn sym ufn (Ctx.empty :> i1 :> b1) , testProperty "argument passthrough" $ withTests 1 $ property $ mkEquivalenceTest parseSExpr (Ctx.empty :> BaseBoolRepr :> BaseIntegerRepr) $ \sym bvs -> do let i1 = bvs ! Ctx.i2of2 let b1 = bvs ! Ctx.i1of2 ufn <- WI.freshTotalUninterpFn sym (WI.safeSymbol "ufn") (Ctx.empty :> BaseIntegerRepr :> BaseBoolRepr) BaseBoolRepr WI.applySymFn sym ufn (Ctx.empty :> i1 :> b1) ] testExpressions :: (T.Text -> Either String WIN.SExpr) -> [TestTree] testExpressions parseSExpr = [ testProperty "negative ints" $ withTests 1 $ property $ mkEquivalenceTest parseSExpr Ctx.empty $ \sym _ -> do WI.intLit sym (-1) , testProperty "float lit" $ withTests 1 $ property $ mkEquivalenceTest parseSExpr Ctx.empty $ \sym _ -> do WI.floatLit sym floatSinglePrecision (BF.bfFromInt 100) , testProperty "simple struct" $ withTests 1 $ property $ mkEquivalenceTest parseSExpr Ctx.empty $ \sym _ -> do i1 <- WI.intLit sym 0 let b1 = WI.truePred sym WI.mkStruct sym (Ctx.empty :> i1 :> b1) , testProperty "struct field access" $ withTests 1 $ property $ mkEquivalenceTest parseSExpr (Ctx.empty :> BaseStructRepr (Ctx.empty :> BaseIntegerRepr :> BaseBoolRepr)) $ \sym bvs -> do let struct = bvs ! Ctx.baseIndex i1 <- WI.structField sym struct Ctx.i1of2 b1 <- WI.structField sym struct Ctx.i2of2 WI.mkStruct sym (Ctx.empty :> b1 :> i1) --, testProperty "simple constant array" $ -- property $ mkEquivalenceTest Ctx.empty $ \sym _ -> do -- i1 <- WI.intLit sym 1 -- WI.constantArray sym (Ctx.empty :> BaseIntegerRepr) i1 , testProperty "array update" $ withTests 1 $ property $ mkEquivalenceTest parseSExpr (Ctx.empty :> BaseArrayRepr (Ctx.empty :> BaseIntegerRepr) BaseIntegerRepr) $ \sym bvs -> do i1 <- WI.intLit sym 1 i2 <- WI.intLit sym 2 let arr = bvs ! Ctx.baseIndex WI.arrayUpdate sym arr (Ctx.empty :> i1) i2 , testProperty "integer to bitvector" $ withTests 1 $ property $ mkEquivalenceTest parseSExpr (Ctx.empty :> BaseIntegerRepr) $ \sym bvs -> do let i1 = bvs ! Ctx.baseIndex WI.integerToBV sym i1 (WI.knownNat @32) , testProperty "float negate" $ withTests 1 $ property $ mkEquivalenceTest parseSExpr (Ctx.empty :> floatSingleType ) $ \sym flts -> do let f1 = flts ! Ctx.baseIndex WI.floatNeg sym f1 , testProperty "float abs" $ withTests 1 $ property $ mkEquivalenceTest parseSExpr (Ctx.empty :> floatSingleType ) $ \sym flts -> do let f1 = flts ! Ctx.baseIndex WI.floatAbs sym f1 ] mkEquivalenceTest :: forall m args ret . ( MonadTest m , MonadIO m ) => (T.Text -> Either String WIN.SExpr) -> Ctx.Assignment BaseTypeRepr args -> (forall sym . WI.IsSymExprBuilder sym => sym -> Ctx.Assignment (WI.SymExpr sym) args -> IO (WI.SymExpr sym ret)) -> m () mkEquivalenceTest parseSExpr argTs getExpr = do Some r <- liftIO $ newIONonceGenerator sym <- liftIO $ S.newExprBuilder S.FloatRealRepr NoBuilderData r liftIO $ S.startCaching sym bvs <- liftIO $ forFC argTs $ \repr -> do n <- freshNonce r let nm = "bv" ++ show (indexValue n) WI.freshBoundVar sym (WI.safeSymbol nm) repr e <- liftIO $ getExpr sym (fmapFC (WI.varExpr sym) bvs) go sym bvs e where go :: forall sym t flgs st . ( WI.IsSymExprBuilder sym , sym ~ S.ExprBuilder t st flgs , ShowF (WI.SymExpr sym) ) => sym -> Ctx.Assignment (WI.BoundVar sym) args -> WI.SymExpr sym ret -> m () go sym bvs expr = do fn1 <- liftIO $ WI.definedFn sym (WI.safeSymbol "fn") bvs expr WI.NeverUnfold let scfg = WOUT.Config { WOUT.cfgAllowFreeVars = True , WOUT.cfgAllowFreeSymFns = True } res = WOUT.serializeSymFnWithConfig scfg fn1 fnText = WOUT.printSExpr mempty $ WOUT.resSExpr res fnMap = Map.fromList $ map (\(x,y)->(y,x)) $ OMap.assocs $ WOUT.resSymFnEnv res exprMap = Map.fromList $ map (\((Some bv),freshName) -> (freshName, (Some (WI.varExpr sym bv)))) $ OMap.assocs $ WOUT.resFreeVarEnv res -- lcfg <- liftIO $ Log.mkLogCfg "rndtrip" deser <- do dcfg <- return $ (WIN.defaultConfig sym) { WIN.cSymFnLookup = \nm -> case Map.lookup nm fnMap of Nothing -> return Nothing Just (WOUT.SomeExprSymFn fn) -> return $ Just (WIN.SomeSymFn fn) , WIN.cExprLookup = \nm -> case Map.lookup nm exprMap of Nothing -> return Nothing Just (Some x) -> return $ Just (Some x) } case parseSExpr fnText of Left errMsg -> return $ Left errMsg Right sexpr -> liftIO $ WIN.deserializeSymFnWithConfig sym dcfg sexpr case deser of Left err -> do debugOut $ "Unexpected deserialization error: " ++ err ++ "!\n S-expression:\n" debugOut $ (T.unpack fnText) ++ "\n" failure Right (WIN.SomeSymFn fn2) -> do fn1out <- liftIO $ WI.definedFn sym (WI.safeSymbol "fn") bvs expr WI.NeverUnfold symFnEqualityTest sym fn1out fn2 -- | Create a 'T.TestTree' from a Hedgehog 'Property'. -- -- Note that @tasty-hedgehog@'s version of 'testProperty' has been deprecated -- in favor of 'testPropertyNamed', whose second argument is intended to -- represent the name of a top-level 'Property' value to run in the event that -- the test fails. See https://github.com/qfpl/tasty-hedgehog/pull/42. -- -- That being said, @what4-serialize@ currently does not define any of the -- properties that it tests as top-level values. In the -- meantime, we avoid incurring deprecation warnings by defining our own -- version of 'testProperty'. The downside to this workaround is that if a -- property fails, the error message it will produce will likely suggest -- running ill-formed Haskell code, so users will have to use context clues to -- determine how to /actually/ reproduce the error. testProperty :: TestName -> Property -> TestTree testProperty name = testPropertyNamed name (String.fromString name)