diff --git a/arch/Pate/AArch32.hs b/arch/Pate/AArch32.hs index 4734e053..4770029c 100644 --- a/arch/Pate/AArch32.hs +++ b/arch/Pate/AArch32.hs @@ -6,8 +6,13 @@ {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE FlexibleContexts #-} {-# OPTIONS_GHC -fno-warn-orphans #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE MultiParamTypeClasses #-} module Pate.AArch32 ( SA.AArch32 , AArch32Opts(..) @@ -66,6 +71,7 @@ import qualified Pate.Address as PA import Data.Macaw.ARM.Identify (conditionalCallClassifier, conditionalReturnClassifier, wrapClassifierForPstateT) import Control.Applicative import qualified Data.Macaw.Discovery as MD +import qualified What4.JSON as W4S data NoRegisters (tp :: LCT.CrucibleType) = NoRegisters Void @@ -109,6 +115,12 @@ hacky_arm_linux_info :: MAI.ArchitectureInfo SA.AArch32 hacky_arm_linux_info = ARM.arm_linux_info +instance W4S.W4Serializable sym (ARMReg.ARMReg tp) where + w4Serialize = PA.serializeRegister + +instance W4S.W4SerializableF sym ARMReg.ARMReg where +instance (W4S.W4SerializableFC ARMReg.ARMReg) where + instance PA.ValidArch SA.AArch32 where type ArchConfigOpts SA.AArch32 = AArch32Opts SA.AArch32 -- FIXME: define these diff --git a/arch/Pate/PPC.hs b/arch/Pate/PPC.hs index 765c78c7..791e551a 100644 --- a/arch/Pate/PPC.hs +++ b/arch/Pate/PPC.hs @@ -9,6 +9,7 @@ {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# OPTIONS_GHC -fno-warn-orphans #-} @@ -80,6 +81,7 @@ import qualified Pate.Verification.Domain as PD import Pate.TraceTree import Data.Macaw.CFG.Core +import qualified What4.JSON as W4S -- | There is just one dedicated register on ppc64 data PPC64DedicatedRegister tp where @@ -154,6 +156,14 @@ ppc32HasDedicatedRegister = , PA.dedicatedRegisterValidity = \_ _ _ _ (NoRegisters v) -> absurd v } +instance forall v sym tp. SP.KnownVariant v => W4S.W4Serializable sym (PPC.PPCReg v tp) where + w4Serialize = case SP.knownVariant @v of + PPC.V32Repr -> PA.serializeRegister + PPC.V64Repr -> PA.serializeRegister + +instance SP.KnownVariant v => W4S.W4SerializableF sym (PPC.PPCReg v) where +instance SP.KnownVariant v => W4S.W4SerializableFC (PPC.PPCReg v) where + instance PA.ValidArch PPC.PPC32 where type ArchConfigOpts PPC.PPC32 = () rawBVReg r = case r of diff --git a/src/Pate/Arch.hs b/src/Pate/Arch.hs index b2d48af9..88049128 100644 --- a/src/Pate/Arch.hs +++ b/src/Pate/Arch.hs @@ -12,6 +12,9 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE UndecidableSuperClasses #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE ImpredicativeTypes #-} +{-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -fno-warn-orphans #-} @@ -39,7 +42,8 @@ module Pate.Arch ( defaultStubOverride, withStubOverride, mergeLoaders, - idStubOverride + idStubOverride, + serializeRegister ) where import Control.Lens ( (&), (.~), (^.) ) @@ -86,6 +90,7 @@ import qualified What4.Interface as W4 hiding ( integerToNat ) import qualified What4.Concrete as W4 import qualified What4.ExprHelpers as W4 ( integerToNat ) import qualified What4.UninterpFns as W4U +import qualified What4.JSON as W4S import Pate.Config (PatchData) import Data.Macaw.AbsDomain.AbsState (AbsBlockState) @@ -95,6 +100,10 @@ import qualified Data.Parameterized.List as P import qualified Data.Parameterized.Map as MapF import qualified Data.Parameterized.TraversableFC as TFC import Data.Proxy +import Data.Witness +import qualified Data.Aeson as JSON +import Data.Aeson ( (.=) ) +import Data.Parameterized.Classes (ShowF(..)) -- | The type of architecture-specific dedicated registers -- @@ -145,6 +154,8 @@ fromRegisterDisplay rd = Architectural a -> Just a Hidden -> Nothing + + class ( Typeable arch , MBL.BinaryLoader arch (E.ElfHeaderInfo (MC.ArchAddrWidth arch)) @@ -154,6 +165,7 @@ class , 16 <= MC.ArchAddrWidth arch , MCS.HasArchEndCase arch , Integral (EEP.ElfWordType (MC.ArchAddrWidth arch)) + , W4S.W4SerializableFC (MC.ArchReg arch) ) => ValidArch arch where type ArchConfigOpts arch @@ -201,6 +213,13 @@ class Maybe (MD.ParsedTermStmt arch ids) archExtractArchTerms = \ _ _ _ -> Nothing +serializeRegister :: ValidArch arch => MC.ArchReg arch tp -> W4S.W4S sym JSON.Value +serializeRegister r = case displayRegister r of + Normal r_n -> return $ JSON.object [ "reg" .= r_n ] + Architectural r_a -> return $ JSON.object [ "arch_reg" .= r_a ] + Hidden -> return $ JSON.object [ "hidden_reg" .= showF r ] + + data ValidArchData arch = ValidArchData { validArchSyscallDomain :: PVE.ExternalDomain PVE.SystemCall arch , validArchFunctionDomain :: PVE.ExternalDomain PVE.ExternalCall arch @@ -478,7 +497,7 @@ data ArchLoader err = instance (ValidArch arch, PSo.ValidSym sym, rv ~ MC.ArchReg arch) => MC.PrettyRegValue rv (PSR.MacawRegEntry sym) where ppValueEq r tp = case fromRegisterDisplay (displayRegister r) of - Just r_str -> Just (PP.pretty r_str <> PP.pretty ":" <+> PP.pretty (show tp)) + Just r_str -> Just (PP.pretty r_str <> ":" <+> PP.pretty (show tp)) Nothing -> Nothing -- | Merge loaders by taking the first successful result (if it exists) diff --git a/src/Pate/Equivalence/EquivalenceDomain.hs b/src/Pate/Equivalence/EquivalenceDomain.hs index aefab869..5d9f55cb 100644 --- a/src/Pate/Equivalence/EquivalenceDomain.hs +++ b/src/Pate/Equivalence/EquivalenceDomain.hs @@ -9,6 +9,7 @@ {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeApplications #-} module Pate.Equivalence.EquivalenceDomain ( EquivalenceDomain(..) @@ -20,6 +21,7 @@ module Pate.Equivalence.EquivalenceDomain ( import qualified What4.Interface as WI import qualified Prettyprinter as PP import Data.Parameterized.Classes +import Data.Proxy import qualified Data.Macaw.CFG as MM @@ -29,6 +31,9 @@ import qualified Pate.Equivalence.RegisterDomain as PER import qualified Pate.ExprMappable as PEM import qualified Pate.Location as PL import qualified What4.PredMap as WPM +import qualified What4.JSON as W4S +import qualified Data.Aeson as JSON +import Data.Aeson ( (.=) ) --------------------------------------------- -- Equivalence domain @@ -45,6 +50,13 @@ data EquivalenceDomain sym arch where , eqDomainMaxRegion :: PL.NamedPred sym WPM.PredDisjT "maxRegion" } -> EquivalenceDomain sym arch +instance forall sym arch. (W4S.W4SerializableF sym (MM.ArchReg arch), W4S.SerializableExprs sym) => W4S.W4Serializable sym (EquivalenceDomain sym arch) where + w4Serialize (EquivalenceDomain regs stack globs _) = W4S.withSerializable (Proxy @sym) (Proxy @(WI.SymExpr sym)) (Proxy @WI.BaseBoolType) $ do + regs_v <- W4S.w4Serialize regs + stack_v <- W4S.w4Serialize stack + globs_v <- W4S.w4Serialize globs + return $ JSON.object [ "registers" .= regs_v, "stack_slots" .= stack_v, "pointers" .= globs_v] + instance (WI.IsSymExprBuilder sym, OrdF (WI.SymExpr sym), MM.RegisterInfo (MM.ArchReg arch)) => PL.LocationTraversable sym arch (EquivalenceDomain sym arch) where traverseLocation sym x f = PL.witherLocation sym x (\loc p -> Just <$> f loc p) diff --git a/src/Pate/Equivalence/MemoryDomain.hs b/src/Pate/Equivalence/MemoryDomain.hs index 3e455baa..8b4ea39c 100644 --- a/src/Pate/Equivalence/MemoryDomain.hs +++ b/src/Pate/Equivalence/MemoryDomain.hs @@ -45,6 +45,7 @@ import qualified Pate.MemCell as PMC import qualified Pate.Memory.MemTrace as MT import qualified Pate.Location as PL import qualified What4.PredMap as WPM +import qualified What4.JSON as W4S --------------------------------------------- -- Memory domain @@ -59,6 +60,9 @@ data MemoryDomain sym arch = -- ^ The locations excluded by this 'MemoryDomain' } +instance W4S.SerializableExprs sym => W4S.W4Serializable sym (MemoryDomain sym arch) where + w4Serialize (MemoryDomain x) = W4S.w4Serialize x + -- | Map the internal 'PMC.MemCell' entries representing the locations of a 'MemoryDomain'. Predicates which are concretely false are dropped from in resulting internal 'PMC.MemCellPred' (this has no effect on the interpretation of the domain). Supports parallel traversal if the 'future' parameter is instantiated to 'Par.Future'. traverseWithCell :: forall sym arch m. diff --git a/src/Pate/Equivalence/RegisterDomain.hs b/src/Pate/Equivalence/RegisterDomain.hs index c2e598da..69bbf12d 100644 --- a/src/Pate/Equivalence/RegisterDomain.hs +++ b/src/Pate/Equivalence/RegisterDomain.hs @@ -51,6 +51,7 @@ import qualified Pate.Location as PL import qualified Pate.Solver as PS import qualified Pate.ExprMappable as PEM import Pate.TraceTree +import qualified What4.JSON as W4S --------------------------------------------- -- Register domain @@ -61,6 +62,10 @@ import Pate.TraceTree newtype RegisterDomain sym arch = RegisterDomain { _unRD :: Map (Some (MM.ArchReg arch)) (WI.Pred sym) } +instance (W4S.W4Serializable sym (WI.Pred sym), W4S.W4SerializableF sym (MM.ArchReg arch)) => + W4S.W4Serializable sym (RegisterDomain sym arch) where + w4Serialize (RegisterDomain rd) = W4S.w4Serialize rd + traverseWithReg :: forall m sym arch. WI.IsExprBuilder sym => diff --git a/src/Pate/MemCell.hs b/src/Pate/MemCell.hs index 74153ffe..a5c21dce 100644 --- a/src/Pate/MemCell.hs +++ b/src/Pate/MemCell.hs @@ -11,6 +11,9 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeFamilies #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} module Pate.MemCell ( MemCell(..) @@ -29,18 +32,22 @@ import qualified Data.Macaw.Memory as MM import Data.Parameterized.Some import qualified Data.Parameterized.Classes as PC import qualified Data.Parameterized.NatRepr as PNR -import GHC.TypeLits ( type (<=) ) +import GHC.TypeLits ( type (<=), Nat ) import qualified Lang.Crucible.LLVM.MemModel as CLM import Lang.Crucible.Backend (IsSymInterface) import qualified What4.Interface as WI - +import Data.Proxy import qualified Prettyprinter as PP import qualified Pate.ExprMappable as PEM import qualified Pate.Memory.MemTrace as PMT import qualified What4.ExprHelpers as WEH import qualified What4.PredMap as WPM +import qualified What4.JSON as W4S import Data.Data (Typeable) +import Data.UnwrapType +import Data.Aeson ( (.=) ) +import qualified Data.Aeson as JSON -- | A pointer with an attached width, representing the size of the "cell" in bytes. -- It represents a discrete read or write, used as the key when forming a 'Pate.Equivalence.MemPred' @@ -56,6 +63,25 @@ data MemCell sym arch w where , cellEndian :: MM.Endianness } -> MemCell sym arch w +newtype Pointer sym w = Pointer (CLM.LLVMPtr sym w) +type instance UnwrapType (Pointer sym w) = CLM.LLVMPtr sym w + +instance W4S.SerializableExprs sym => W4S.W4Serializable sym (Pointer sym w) where + w4Serialize (Pointer (CLM.LLVMPointer reg off)) = do + reg_v <- W4S.w4SerializeF (WI.natToIntegerPure reg) + off_v <- W4S.w4SerializeF off + return $ JSON.object ["region" .= reg_v, "offset" .= off_v] + +instance forall sym arch w. W4S.SerializableExprs sym => W4S.W4Serializable sym (MemCell sym arch w) where + w4Serialize (MemCell ptr w end) = + unwrapClass @(W4S.W4Serializable sym) @(Pointer sym (MC.ArchAddrWidth arch)) $ do + ptr_v <- W4S.w4Serialize ptr + width_v <- W4S.w4Serialize (PNR.intValue w) + end_v <- W4S.w4Serialize (show end) + return $ JSON.object [ "ptr" .= ptr_v, "width" .= width_v, "endianness" .= end_v ] + +instance forall sym arch. W4S.SerializableExprs sym => W4S.W4SerializableF sym (MemCell sym arch) where + viewCell :: MemCell sym arch w -> ((1 <= w, 1 <= (8 WI.* w)) => a) -> a viewCell (mc@MemCell{}) f = case PNR.leqMulPos (WI.knownNat @8) (cellWidth mc) of diff --git a/src/Pate/Solver.hs b/src/Pate/Solver.hs index ba9e3b91..d6dcf5f0 100644 --- a/src/Pate/Solver.hs +++ b/src/Pate/Solver.hs @@ -27,6 +27,7 @@ import qualified What4.Solver as WS import qualified Lang.Crucible.Backend as CB import qualified Lang.Crucible.Backend.Online as CBO import Data.Data (Typeable) +import qualified What4.JSON as W4S -- | The solvers supported by the pate verifier -- @@ -87,6 +88,7 @@ type ValidSym sym = ( WI.IsExprBuilder sym , CB.IsSymInterface sym , ShowF (WI.SymExpr sym) + , W4S.W4SerializableF sym (WI.SymExpr sym) ) -- | A wrapper around the symbolic backend (a 'WE.ExprBuilder') that captures diff --git a/src/Pate/Verification/AbstractDomain.hs b/src/Pate/Verification/AbstractDomain.hs index c49427a5..3916d801 100644 --- a/src/Pate/Verification/AbstractDomain.hs +++ b/src/Pate/Verification/AbstractDomain.hs @@ -18,6 +18,7 @@ {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE ImpredicativeTypes #-} {-# OPTIONS_GHC -fno-warn-orphans #-} @@ -105,6 +106,9 @@ import Pate.TraceTree import qualified What4.PredMap as WPM import Data.Parameterized (knownSymbol) +import qualified What4.JSON as W4S +import Data.Aeson ( (.=) ) +import qualified Data.Aeson as JSON type instance PL.LocationK "memevent" = () type instance PL.LocationK "absrange" = W4.BaseType @@ -132,6 +136,11 @@ data AbstractDomain sym arch (v :: PS.VarScope) where -- sequences are compared for equality } -> AbstractDomain sym arch v +instance forall sym arch v. (PSo.ValidSym sym, PA.ValidArch arch) => W4S.W4Serializable sym (AbstractDomain sym arch v) where + w4Serialize abs_dom = do + eq_dom <- W4S.w4Serialize (absDomEq abs_dom) + return $ JSON.object [ "eq_domain" .= eq_dom, "val_domain" .= JSON.String "TODO" ] + -- | Restrict an abstract domain to a single binary. singletonDomain :: PPa.PatchPairM m => @@ -892,8 +901,11 @@ instance (PA.ValidArch arch, PSo.ValidSym sym) => IsTraceNode '(sym,arch) "domai [ ppDomainKind lbl , PED.ppEquivalenceDomain (\_ -> "") (\r -> fmap PP.pretty (PA.fromRegisterDisplay (PA.displayRegister r))) (absDomEq absDom) ]), - (JSONTrace, \lbl _ -> ppDomainKind lbl) + (JSONTrace, \_lbl (Some absDom) -> PED.ppEquivalenceDomain (\_ -> "") (\r -> fmap PP.pretty (PA.fromRegisterDisplay (PA.displayRegister r))) (absDomEq absDom)) ] + jsonNode lbl (Some abs_dom) = + let abs_dom_json = W4S.w4ToJSON @sym abs_dom + in JSON.object [ "abstract_domain" .= abs_dom_json, "kind" .= (show lbl) ] -- simplified variant of domain trace node -- currently only displays equivalence domain diff --git a/src/What4/JSON.hs b/src/What4/JSON.hs new file mode 100644 index 00000000..ca10fb03 --- /dev/null +++ b/src/What4/JSON.hs @@ -0,0 +1,137 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE QuantifiedConstraints #-} + +module What4.JSON + ( W4S + , W4Serializable(..) + , W4SerializableF(..) + , W4SerializableFC + , SerializableExprs + , w4ToJSON + ) where + +import Control.Monad.Except (ExceptT, MonadError) +import Control.Monad.Reader (ReaderT, MonadReader) +import Control.Monad.IO.Class (MonadIO) +import Control.Monad.State (StateT, MonadState (..), State, modify, evalState) + +import Data.Map.Ordered (OMap) +import qualified Data.Map.Ordered as OMap +import Data.Map (Map) +import Data.Text (Text) +import qualified Data.Text as Text +import Data.Data (Proxy(..), Typeable) +import qualified Data.Aeson as JSON +import Data.Aeson ( (.=) ) + +import Data.Parameterized.Some (Some(..)) + +import qualified What4.Interface as W4 + +import What4.Serialize.Parser (SomeSymFn(..)) +import qualified What4.Serialize.Printer as W4S +import qualified What4.Serialize.Parser as W4D +import qualified What4.Expr.Builder as W4B +import qualified Data.Map as Map +import Control.Monad (forM) +import qualified What4.PredMap as W4P +import Data.Parameterized.HasRepr +import qualified What4.Concrete as W4 +import qualified Data.Text as T + + +newtype ExprCache sym = ExprCache (Map (Some (W4.SymExpr sym)) JSON.Value) + +newtype W4S sym a = W4S (State (ExprCache sym) a) + deriving (Monad, Applicative, Functor, MonadState (ExprCache sym)) + +class W4Serializable sym a where + w4Serialize :: a -> W4S sym JSON.Value + + +w4ToJSON :: forall sym a. W4Serializable sym a => a -> JSON.Value +w4ToJSON a = let W4S f = w4Serialize @sym a in evalState f (ExprCache Map.empty) + +class W4SerializableF sym f where + withSerializable :: Proxy sym -> p f -> q tp -> (W4Serializable sym (f tp) => a) -> a + + default withSerializable :: W4Serializable sym (f tp) => Proxy sym -> p f -> q tp -> (W4Serializable sym (f tp) => a) -> a + withSerializable _ _ _ x = x + + w4SerializeF :: forall tp. f tp -> W4S sym JSON.Value + w4SerializeF x = withSerializable (Proxy :: Proxy sym) (Proxy :: Proxy f) (Proxy :: Proxy tp) (w4Serialize x) + +class (forall sym. W4SerializableF sym f) => W4SerializableFC f where + + +instance sym ~ W4B.ExprBuilder t fs scope => W4Serializable sym (W4B.Expr t tp) where + w4Serialize e = do + ExprCache s <- get + case Map.lookup (Some e) s of + Just v -> return $ v + Nothing -> do + v <- case W4.asConcrete e of + Just (W4.ConcreteInteger i) -> return $ JSON.toJSON i + Just (W4.ConcreteBool b) -> return $ JSON.toJSON b + Just{} -> return $ JSON.String (T.pack (show (W4.printSymExpr e))) + _ -> do + let sexpr = W4S.serializeExpr e + return $ JSON.object [ "symbolic" .= JSON.String (W4D.printSExpr mempty sexpr) ] + modify $ \(ExprCache s') -> ExprCache (Map.insert (Some e) v s') + return v + +deriving instance Typeable (W4B.ExprBuilder t fs scope) + +instance sym ~ W4B.ExprBuilder t fs scope => W4SerializableF sym (W4B.Expr t) where + +instance W4SerializableF sym x => W4Serializable sym (Some x) where + w4Serialize (Some x) = w4SerializeF x + +instance (W4Serializable sym x, W4Serializable sym y) => W4Serializable sym (x, y) where + w4Serialize (x,y) = do + x_v <- w4Serialize x + y_v <- w4Serialize y + return $ JSON.object [ "fst" .= x_v, "snd" .= y_v] + +instance (W4Serializable sym x, W4Serializable sym y) => W4Serializable sym (Map x y) where + w4Serialize x = do + objs <- forM (Map.toList x) $ \(k, v) -> do + k_v <- w4Serialize k + v_v <- w4Serialize v + return $ JSON.object [ "key" .= k_v, "val" .= v_v] + return $ JSON.object [ "map" .= objs ] + +type SerializableExprs sym = W4SerializableF sym (W4.SymExpr sym) + +instance (SerializableExprs sym, W4Serializable sym x) => W4Serializable sym (W4P.PredMap sym x k) where + w4Serialize x = do + objs <- forM (W4P.toList x) $ \(k,p) -> do + k_v <- w4Serialize k + p_v <- w4SerializeF p + return $ JSON.object [ "val" .= k_v, "pred" .= p_v] + let (repr :: String) = case typeRepr x of + W4P.PredConjRepr -> "conj" + W4P.PredDisjRepr -> "disj" + return $ JSON.object [ "predmap" .= objs, "kind" .= repr ] + +instance W4Serializable sym Integer where + w4Serialize i = return $ JSON.toJSON i + +instance W4Serializable sym String where + w4Serialize i = return $ JSON.toJSON i +