add class for serializing values to JSON

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

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

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)

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)
 

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.

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 =>

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

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

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