From f49be5409f7c0553342779f8bf62c081ba506660 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Wed, 7 Aug 2024 16:27:17 -0700 Subject: [PATCH] accept trace constraints as input after final result --- pate.cabal | 1 + src/Pate/CLI.hs | 6 ++ src/Pate/Config.hs | 3 + src/Pate/PatchPair.hs | 20 +++- src/Pate/TraceTree.hs | 27 ++++- src/Pate/Verification/StrongestPosts.hs | 131 ++++++++++++++++++------ src/Pate/Verification/Widening.hs | 49 ++++----- src/What4/JSON.hs | 37 ++++++- 8 files changed, 208 insertions(+), 66 deletions(-) diff --git a/pate.cabal b/pate.cabal index 120c48f1..6d0a9793 100644 --- a/pate.cabal +++ b/pate.cabal @@ -161,6 +161,7 @@ library Pate.Script, Pate.Timeout, Pate.TraceTree, + Pate.TraceConstraint, Pate.ExprMappable, What4.ExprHelpers, What4.PathCondition, diff --git a/src/Pate/CLI.hs b/src/Pate/CLI.hs index 0c5745b7..399466e9 100644 --- a/src/Pate/CLI.hs +++ b/src/Pate/CLI.hs @@ -97,6 +97,7 @@ mkRunConfig archLoader opts rcfg mtt = let , PC.cfgStackScopeAssume = not $ noAssumeStackScope opts , PC.cfgIgnoreWarnings = ignoreWarnings opts , PC.cfgAlwaysClassifyReturn = alwaysClassifyReturn opts + , PC.cfgTraceConstraints = traceConstraints opts } cfg = PL.RunConfig { PL.archLoader = archLoader @@ -150,6 +151,7 @@ data CLIOptions = CLIOptions , ignoreWarnings :: [String] , alwaysClassifyReturn :: Bool , preferTextInput :: Bool + , traceConstraints :: Bool } deriving (Eq, Ord, Show) printAtVerbosity @@ -474,4 +476,8 @@ cliOptions = OA.info (OA.helper <*> parser) <*> OA.switch ( OA.long "prefer-text-input" <> OA.help "Prefer taking text input over multiple choice menus where possible." + ) + <*> OA.switch + ( OA.long "add-trace-constraints" + <> OA.help "Prompt to add additional constraints when generating traces." ) \ No newline at end of file diff --git a/src/Pate/Config.hs b/src/Pate/Config.hs index 9cfcf94d..a0c66b0e 100644 --- a/src/Pate/Config.hs +++ b/src/Pate/Config.hs @@ -290,6 +290,8 @@ data VerificationConfig validRepr = , cfgPreferTextInput :: Bool -- ^ modifies some menus to take string input instead of providing -- a menu selection + , cfgTraceConstraints :: Bool + -- ^ flag to determine if the user should be prompted to add constraints to traces } @@ -317,4 +319,5 @@ defaultVerificationCfg = , cfgIgnoreWarnings = [] , cfgAlwaysClassifyReturn = False , cfgPreferTextInput = False + , cfgTraceConstraints = False } diff --git a/src/Pate/PatchPair.hs b/src/Pate/PatchPair.hs index 41a8b102..f594bcc0 100644 --- a/src/Pate/PatchPair.hs +++ b/src/Pate/PatchPair.hs @@ -101,6 +101,7 @@ import qualified What4.JSON as W4S import What4.JSON import Control.Monad.State.Strict (StateT (..), put) import qualified Control.Monad.State.Strict as CMS +import Control.Applicative ( (<|>) ) -- | A pair of values indexed based on which binary they are associated with (either the -- original binary or the patched binary). @@ -612,4 +613,21 @@ w4SerializePair ppair f = case ppair of return $ JSON.object ["patched" JSON..= p_v] instance W4S.W4SerializableF sym f => W4S.W4Serializable sym (PatchPair f) where - w4Serialize ppair = w4SerializePair ppair w4SerializeF \ No newline at end of file + w4Serialize ppair = w4SerializePair ppair w4SerializeF + + +instance (forall bin. PB.KnownBinary bin => W4Deserializable sym (f bin)) => W4Deserializable sym (PatchPair f) where + w4Deserialize v = do + JSON.Object o <- return v + let + case_pair = do + (vo :: f PB.Original) <- o .: "original" + (vp :: f PB.Patched) <- o .: "patched" + return $ PatchPair vo vp + case_orig = do + (vo :: f PB.Original) <- o .: "original" + return $ PatchPairOriginal vo + case_patched = do + (vp :: f PB.Patched) <- o .: "patched" + return $ PatchPairPatched vp + case_pair <|> case_orig <|> case_patched \ No newline at end of file diff --git a/src/Pate/TraceTree.hs b/src/Pate/TraceTree.hs index 95b10317..94aadbf2 100644 --- a/src/Pate/TraceTree.hs +++ b/src/Pate/TraceTree.hs @@ -120,6 +120,7 @@ module Pate.TraceTree ( , waitingForChoiceInput , chooseInput , chooseInputFromList + , chooseInput_ ) where import GHC.TypeLits ( Symbol, KnownSymbol ) @@ -1050,7 +1051,7 @@ instance PP.Pretty InputChoiceError where data InputChoice (k :: l) nm where InputChoice :: (IsTraceNode k nm) => - { inputChoiceParse :: String -> Either InputChoiceError (TraceNodeLabel nm, TraceNodeType k nm) + { inputChoiceParse :: String -> IO (Either InputChoiceError (TraceNodeLabel nm, TraceNodeType k nm)) , inputChoicePut :: TraceNodeLabel nm -> TraceNodeType k nm -> IO Bool -- returns false if input has already been provided , inputChoiceValue :: IO (Maybe (TraceNodeLabel nm, TraceNodeType k nm)) } -> InputChoice k nm @@ -1063,7 +1064,7 @@ waitingForChoiceInput ic = inputChoiceValue ic >>= \case giveChoiceInput :: InputChoice k nm -> String -> IO (Maybe InputChoiceError) giveChoiceInput ic input = waitingForChoiceInput ic >>= \case False -> return $ Just InputChoiceAlreadyMade - True -> case inputChoiceParse ic input of + True -> inputChoiceParse ic input >>= \case Right (lbl, v) -> inputChoicePut ic lbl v >>= \case True -> return Nothing False -> return $ Just InputChoiceAlreadyMade @@ -1097,12 +1098,28 @@ chooseInputFromList :: m (Maybe a) chooseInputFromList treenm opts = do let parseInput s = case findIndex (\(s',_) -> s == s') opts of - Just idx -> Right (s, idx) - Nothing -> Left (InputChoiceError "Invalid input. Valid options:" (map fst opts)) + Just idx -> return $ Right (s, idx) + Nothing -> return $ Left (InputChoiceError "Invalid input. Valid options:" (map fst opts)) chooseInput @"opt_index" treenm parseInput >>= \case Just (_, idx) -> return $ Just $ (snd (opts !! idx)) Nothing -> return Nothing +chooseInput_ :: + forall nm_choice k m e. + IsTreeBuilder k e m => + IsTraceNode k nm_choice => + Default (TraceNodeLabel nm_choice) => + IO.MonadUnliftIO m => + String -> + (String -> IO (Either InputChoiceError (TraceNodeType k nm_choice))) -> + m (Maybe (TraceNodeType k nm_choice)) +chooseInput_ treenm parseInput = do + let parse s = parseInput s >>= \case + Left err -> return $ Left err + Right a -> return $ Right (def,a) + fmap snd <$> chooseInput @nm_choice treenm parse + + -- | Take user input as a string. Returns 'Nothing' in the case where the trace tree -- is not running interactively. Otherwise, blocks the current thread until -- valid input is provided. @@ -1112,7 +1129,7 @@ chooseInput :: IsTraceNode k nm_choice => IO.MonadUnliftIO m => String -> - (String -> Either InputChoiceError (TraceNodeLabel nm_choice, TraceNodeType k nm_choice)) -> + (String -> IO (Either InputChoiceError (TraceNodeLabel nm_choice, TraceNodeType k nm_choice))) -> m (Maybe (TraceNodeLabel nm_choice, TraceNodeType k nm_choice)) chooseInput treenm parseInput = do builder <- getTreeBuilder diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index ddbf5e66..5bf35097 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -109,6 +109,7 @@ import qualified Pate.SimulatorRegisters as PSR import qualified Pate.Verification.StrongestPosts.CounterExample as CE import qualified Pate.Register.Traversal as PRt import Pate.Discovery.PLT (extraJumpClassifier, ExtraJumps(..), ExtraJumpTarget(..)) +import qualified Pate.TraceConstraint as PTC import Pate.TraceTree import qualified Pate.Verification.Validity as PVV @@ -860,37 +861,104 @@ clearTrivialCondition nd condK pg = case getCondition pg nd ConditionEquiv of return pg1 Nothing -> return pg -showFinalResult :: PairGraph sym arch -> EquivM sym arch () +-- | Context needed to re-generate traces when adding trace constraints +data IntermediateEqCond sym arch v = + IntermediateEqCond + { ieqBundle :: SimBundle sym arch v + , ieqFootprints:: PPa.PatchPairC (CE.TraceFootprint sym arch) + , ieqEnv :: W4S.ExprEnv sym + , ieqAsms :: PAS.AssumptionSet sym + , ieqCond :: W4.Pred sym + , ieqDom :: AbstractDomain sym arch v + } + +data EqCondCollector sym arch = EqCondCollector + { eqCondFinals :: Map.Map (GraphNode arch) (FinalEquivCond sym arch) + , eqCondInterims :: Map.Map (GraphNode arch) (PS.SimSpec sym arch (IntermediateEqCond sym arch)) + , eqCondConstraints :: PTC.TraceConstraintMap sym arch + } + +getExprEnvs :: EqCondCollector sym arch -> Map.Map (GraphNode arch) (W4S.ExprEnv sym) +getExprEnvs st = fmap (\spec -> PS.viewSpecBody spec ieqEnv) (eqCondInterims st) + +showFinalResult :: forall sym arch. PairGraph sym arch -> EquivM sym arch () showFinalResult pg0 = withTracing @"final_result" () $ withSym $ \sym -> do - subTree @"node" "Observable Counter-examples" $ do - forM_ (Map.toList (pairGraphObservableReports pg0)) $ \(nd,report) -> - subTrace (GraphNode nd) $ - emitTrace @"observable_result" (CE.ObservableCheckCounterexample report) - eq_conds <- fmap catMaybes $ subTree @"node" "Assumed Equivalence Conditions" $ do - - forM (getAllNodes pg0) $ \nd -> do + st <- go (EqCondCollector Map.empty Map.empty (PTC.TraceConstraintMap Map.empty)) + add_constraints <- asks (PCfg.cfgTraceConstraints . envConfig) + case add_constraints of + True -> + let loop st_ = chooseBool "Regenerate result with new trace constraints?" >>= \case + True -> do + tcs <- PTC.readConstraintMap sym "Waiting for constraints.." (getExprEnvs st_) + go (st_ {eqCondConstraints = tcs}) >>= loop + False -> return () + in loop st + False -> return () + + where + mkEqCond :: + EqCondCollector sym arch -> + GraphNode arch -> + NodeBuilderT '(sym,arch) "node" (EquivM_ sym arch) (EqCondCollector sym arch) + mkEqCond rs nd = do pg <- lift $ clearTrivialCondition nd ConditionEquiv pg0 - case getCondition pg nd ConditionEquiv of - Just cond_spec -> subTrace nd $ do - s <- withFreshScope (graphNodeBlocks nd) $ \scope -> do - (_,cond) <- IO.liftIO $ PS.bindSpec sym (PS.scopeVarsPair scope) cond_spec - (tr, _) <- withGraphNode scope nd pg $ \bundle d -> do - cond_simplified <- PSi.applySimpStrategy PSi.deepPredicateSimplifier cond - eqCond_pred <- PEC.toPred sym cond_simplified - (mtraceT, mtraceF) <- getTracesForPred scope bundle d eqCond_pred - case (mtraceT, mtraceF) of - (Just traceT, Just traceF) -> do - cond_pretty <- PSi.applySimpStrategy PSi.prettySimplifier eqCond_pred - return $ (Just (FinalEquivCond cond_pretty traceT traceF), pg) - _ -> return (Nothing, pg) - return $ (Const (fmap (nd,) tr)) - return $ PS.viewSpec s (\_ -> getConst) - Nothing -> return Nothing - let result = pairGraphComputeVerdict pg0 - emitTrace @"equivalence_result" result - let eq_conds_map = Map.fromList eq_conds - let toplevel_result = FinalResult result (pairGraphObservableReports pg0) eq_conds_map - emitTrace @"toplevel_result" toplevel_result + let PTC.TraceConstraintMap tcm = eqCondConstraints rs + + + let + rest :: forall v. PS.SimScope sym arch v -> IntermediateEqCond sym arch v -> EquivM_ sym arch (Maybe (FinalEquivCond sym arch)) + rest scope (IntermediateEqCond bundle fps _ _ cond d) = withSym $ \sym -> do + trace_constraint <- case Map.lookup nd tcm of + Just tc -> IO.liftIO $ PTC.constraintToPred sym tc + Nothing -> return $ W4.truePred sym + mres <- withSatAssumption (PAS.fromPred trace_constraint) $ do + (mtraceT, mtraceF) <- getTracesForPred scope bundle d cond + case (mtraceT, mtraceF) of + (Just traceT, Just traceF) -> do + cond_pretty <- PSi.applySimpStrategy PSi.prettySimplifier cond + return $ Just (FinalEquivCond cond_pretty traceT traceF fps) + _ -> return Nothing + case mres of + Just res -> return res + Nothing -> emitWarning PEE.UnsatisfiableAssumptions >> return Nothing + + case Map.lookup nd (eqCondInterims rs) of + Just ieqcspec -> subTrace nd $ PS.viewSpec ieqcspec $ \scope ieqc -> withAssumptionSet (ieqAsms ieqc) $ do + rest scope ieqc >>= \case + Just fcond -> return (rs { eqCondFinals = Map.insert nd fcond (eqCondFinals rs) }) + Nothing -> return rs + Nothing -> case getCondition pg nd ConditionEquiv of + Just cond_spec -> subTrace nd $ withSym $ \sym -> do + spec <- withFreshScope (graphNodeBlocks nd) $ \scope -> fmap PS.WithScope $ do + (_,cond) <- IO.liftIO $ PS.bindSpec sym (PS.scopeVarsPair scope) cond_spec + fmap fst $ withGraphNode scope nd pg $ \bundle d -> do + cond_simplified <- PSi.applySimpStrategy PSi.deepPredicateSimplifier cond + eqCond_pred <- PEC.toPred sym cond_simplified + (fps, eenv) <- getTraceFootprint scope bundle + asms <- currentAsm + let ieqc = IntermediateEqCond bundle fps eenv asms eqCond_pred d + let interims = Map.insert nd (PS.mkSimSpec scope ieqc) (eqCondInterims rs) + rest scope ieqc >>= \case + Just fcond -> return (rs { eqCondFinals = Map.insert nd fcond (eqCondFinals rs), eqCondInterims = interims }, pg) + Nothing -> return (rs { eqCondInterims = interims }, pg) + return $ PS.viewSpecBody spec PS.unWS + Nothing -> return rs + + go :: EqCondCollector sym arch -> EquivM sym arch (EqCondCollector sym arch) + go rs = do + subTree @"node" "Observable Counter-examples" $ do + forM_ (Map.toList (pairGraphObservableReports pg0)) $ \(nd,report) -> + subTrace (GraphNode nd) $ + emitTrace @"observable_result" (CE.ObservableCheckCounterexample report) + + rs' <- subTree @"node" "Assumed Equivalence Conditions" $ + foldM mkEqCond (rs { eqCondFinals = Map.empty }) (getAllNodes pg0) + let result = pairGraphComputeVerdict pg0 + emitTrace @"equivalence_result" result + + let toplevel_result = FinalResult result (pairGraphObservableReports pg0) (eqCondFinals rs') + emitTrace @"toplevel_result" toplevel_result + return rs' data FinalResult sym arch = FinalResult { @@ -904,6 +972,7 @@ data FinalEquivCond sym arch = FinalEquivCond _finEqCondPred :: W4.Pred sym , _finEqCondTraceTrue :: CE.TraceEvents sym arch , _finEqCondTraceFalse :: CE.TraceEvents sym arch + , _finEqFootprints :: PPa.PatchPairC (CE.TraceFootprint sym arch) } @@ -915,8 +984,8 @@ instance (PA.ValidArch arch, PSo.ValidSym sym) => W4S.W4Serializable sym (FinalR W4S.object [ "eq_status" W4S..= st, "observable_counterexamples" W4S..= obs, "eq_conditions" W4S..= conds ] instance (PA.ValidArch arch, PSo.ValidSym sym) => W4S.W4Serializable sym (FinalEquivCond sym arch) where - w4Serialize (FinalEquivCond p trT trF) = do - W4S.object [ "predicate" W4S..== p, "trace_true" W4S..= trT, "trace_false" W4S..= trF ] + w4Serialize (FinalEquivCond p trT trF fps) = do + W4S.object [ "predicate" W4S..== p, "trace_true" W4S..= trT, "trace_false" W4S..= trF, "trace_footprint" W4S..= fps ] instance (PSo.ValidSym sym, PA.ValidArch arch) => IsTraceNode '(sym,arch) "toplevel_result" where diff --git a/src/Pate/Verification/Widening.hs b/src/Pate/Verification/Widening.hs index 33aa4056..bdc32d70 100644 --- a/src/Pate/Verification/Widening.hs +++ b/src/Pate/Verification/Widening.hs @@ -33,6 +33,7 @@ module Pate.Verification.Widening , getTraceFromModel , addToEquivCondition , strengthenPredicate + , getTraceFootprint ) where import GHC.Stack @@ -88,6 +89,7 @@ import qualified Pate.Proof.Instances () import qualified Pate.ExprMappable as PEM import qualified Pate.Solver as PSo import qualified Pate.Verification.Simplify as PSi +import qualified Pate.TraceConstraint as PTC import Pate.Monad import Pate.Monad.PairGraph @@ -124,6 +126,7 @@ import qualified Prettyprinter as PP import qualified What4.Expr.GroundEval as W4 import qualified Lang.Crucible.Utils.MuxTree as MT import Pate.Verification.Domain (universalDomain) +import qualified Data.Parameterized.TraversableF as TF -- | Generate a fresh abstract domain value for the given graph node. -- This should represent the most information we can ever possibly @@ -507,44 +510,36 @@ getSomeGroundTrace scope bundle preD postCond = withSym $ \sym -> do let stackbase = PS.unSE $ PS.simStackBase (PS.simInState in_) zero <- liftIO $ W4.bvLit sym CT.knownRepr (BVS.mkBV CT.knownRepr 0) PAs.fromPred <$> (liftIO $ W4.isEq sym zero stackbase) - + ptrAsserts_pred <- PAs.toPred sym (stacks_zero <> ptrAsserts) - trace_constraint <- getTraceConstraint scope bundle - tryWithAsms + tr <- tryWithAsms [ (ptrAsserts_pred, PEE.RequiresInvalidPointerOps) - , (trace_constraint, PEE.UnsatisfiableAssumptions) ] $ \evalFn -> getTraceFromModel scope evalFn bundle preD postCond + return tr + getTraceFootprint :: forall sym arch v. PS.SimScope sym arch v -> SimBundle sym arch v -> - EquivM sym arch (PPa.PatchPairC (CE.TraceFootprint sym arch)) -getTraceFootprint _scope bundle = withSym $ \sym -> PPa.forBinsC $ \bin -> do - out <- PPa.get bin (PS.simOut bundle) - in_ <- PPa.get bin (PS.simIn bundle) - let in_regs = PS.simInRegs in_ - let rop = MT.RegOp (MM.regStateMap in_regs) - let mem = PS.simOutMem out - let s = (MT.memFullSeq @_ @arch mem) - s' <- PEM.mapExpr sym concretizeWithSolver s - liftIO $ CE.mkFootprint sym rop s' - -getTraceConstraint :: - forall sym arch v. - PS.SimScope sym arch v -> - SimBundle sym arch v -> - EquivM sym arch (W4.Pred sym) -getTraceConstraint scope bundle = withSym $ \sym -> do - fps <- getTraceFootprint scope bundle - PPa.joinPatchPred (\a b -> liftIO $ W4.andPred sym a b) $ \bin -> withTracing @"binary" (Some bin) $ do - fp <- PPa.getC bin fps - (v',_eenv) <- liftIO $ W4S.w4ToJSONEnv sym fp + EquivM sym arch (PPa.PatchPairC (CE.TraceFootprint sym arch), W4S.ExprEnv sym) +getTraceFootprint _scope bundle = withSym $ \sym -> do + fps <- PPa.forBinsC $ \bin -> withTracing @"binary" (Some bin) $ do + out <- PPa.get bin (PS.simOut bundle) + in_ <- PPa.get bin (PS.simIn bundle) + let in_regs = PS.simInRegs in_ + let rop = MT.RegOp (MM.regStateMap in_regs) + let mem = PS.simOutMem out + let s = (MT.memFullSeq @_ @arch mem) + s' <- PEM.mapExpr sym concretizeWithSolver s + fp <- liftIO $ CE.mkFootprint sym rop s' + (v',eenv) <- liftIO $ W4S.w4ToJSONEnv sym fp emitTraceLabel @"trace_footprint" v' fp - -- FIXME: todo: get constraint from user - return $ W4.truePred sym + return (fp, eenv) + env <- PPa.joinPatchPred (\(_, a) (_, b) -> return $ W4S.mergeEnvs a b) $ \bin -> (PPa.getC bin fps) + return $ (TF.fmapF (\(Const(a,_)) -> Const a) fps, env) instance (PSo.ValidSym sym, PA.ValidArch arch) => IsTraceNode '(sym,arch) "trace_footprint" where type TraceNodeType '(sym,arch) "trace_footprint" = CE.TraceFootprint sym arch diff --git a/src/What4/JSON.hs b/src/What4/JSON.hs index 04f55cae..fb9adf9a 100644 --- a/src/What4/JSON.hs +++ b/src/What4/JSON.hs @@ -30,6 +30,11 @@ module What4.JSON , (.=) , (.==) , (.=~) + , ExprEnv + , mergeEnvs + , W4Deserializable(..) + , jsonToW4 + , (.:) ) where import Control.Monad.State (MonadState (..), State, modify, evalState, runState) @@ -38,6 +43,7 @@ import qualified Data.Map.Ordered as OMap import Data.List ( stripPrefix ) import Data.Maybe ( mapMaybe ) import Data.Map (Map) +import qualified Data.Map.Merge.Strict as Map import Data.Text (Text) import Data.Data (Proxy(..), Typeable) import qualified Data.Aeson as JSON @@ -118,6 +124,15 @@ w4ToJSON sym a = do newtype ExprEnv sym = ExprEnv (Map Integer (Some (W4.SymExpr sym))) +mergeEnvs :: TestEquality (W4.SymExpr sym) => ExprEnv sym -> ExprEnv sym -> ExprEnv sym +mergeEnvs (ExprEnv env1) (ExprEnv env2) = ExprEnv ( + Map.merge + Map.preserveMissing + Map.preserveMissing + (Map.zipWithMatched (\_ (Some e1) (Some e2) -> (case testEquality e1 e2 of Just Refl -> Some e1; Nothing -> error $ "Unexpected term hash clash"))) + env1 + env2) + -- | Extract expressions with annotations cacheToEnv :: W4.IsExprBuilder sym => sym -> ExprCache sym -> ExprEnv sym cacheToEnv sym (ExprCache m) = ExprEnv $ Map.fromList $ mapMaybe go (Map.keys m) @@ -304,6 +319,13 @@ instance MonadFail (W4DS sym) where class W4Deserializable sym a where w4Deserialize :: JSON.Value -> W4DS sym a + default w4Deserialize :: JSON.FromJSON a => JSON.Value -> W4DS sym a + w4Deserialize v = fromJSON v + +instance W4Deserializable sym Integer +instance W4Deserializable sym Bool +instance W4Deserializable sym () + jsonToW4 :: (W4Deserializable sym a, W4.IsExprBuilder sym) => sym -> ExprEnv sym -> JSON.Value -> IO (Either String a) jsonToW4 sym env v = do let wenv = W4DSEnv env sym @@ -320,9 +342,20 @@ liftParser f v = case JSON.parse f v of JSON.Success a -> return a JSON.Error msg -> fail msg -(.:) :: JSON.FromJSON a => JSON.Object -> JSON.Key -> W4DS sym a -(.:) o = liftParser ((JSON..:) o) +(.:) :: W4Deserializable sym a => JSON.Object -> JSON.Key -> W4DS sym a +(.:) o k = do + (v :: JSON.Value) <- liftParser ((JSON..:) o) k + w4Deserialize v + +instance (W4Deserializable sym a, W4Deserializable sym b) => W4Deserializable sym (a, b) where + w4Deserialize v = do + JSON.Object o <- return v + v1 <- o .: "fst" + v2 <- o .: "snd" + return (v1,v2) +instance W4Deserializable sym f => W4Deserializable sym (Const f x) where + w4Deserialize v = Const <$> w4Deserialize v newtype ToDeserializable sym tp = ToDeserializable { _unDS :: W4.SymExpr sym tp }