work-in-progress for constraint deserialization

src/Pate/PatchPair.hs

@@ -617,7 +617,7 @@ instance W4S.W4SerializableF sym f => W4S.W4Serializable sym (PatchPair f) where
 
 
 instance (forall bin. PB.KnownBinary bin => W4Deserializable sym (f bin)) => W4Deserializable sym (PatchPair f) where
-  w4Deserialize v = do
+  w4Deserialize_ v = do
     JSON.Object o <- return v
     let
       case_pair = do

src/Pate/TraceConstraint.hs

@@ -0,0 +1,178 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE GADTs #-}
+
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Pate.TraceConstraint
+  (
+    TraceConstraint(..)
+  , readDeserializable
+  , constraintToPred
+  , TraceConstraintMap(..)
+  , readConstraintMap
+  ) where
+
+import           Prelude hiding (EQ)
+
+import qualified Control.Monad.IO.Unlift as IO
+import           Control.Monad ( forM )
+import           Control.Monad.Except
+import           Control.Monad.Trans
+import qualified Data.Aeson as JSON
+import qualified Data.Aeson.Types as JSON
+
+import qualified Data.Text.Lazy.Encoding as Text
+import qualified Data.Text.Encoding.Error as Text
+import qualified Data.Kind as DK
+import           Data.String
+import           Data.Map ( Map )
+import qualified Data.Map as Map
+
+import qualified Prettyprinter as PP
+
+import qualified What4.Interface as W4
+import qualified What4.Concrete as W4
+
+import qualified Pate.Arch as PA
+import qualified Pate.PatchPair as PPa
+import           Pate.Verification.PairGraph.Node
+import           Pate.TraceTree
+import qualified What4.JSON as W4S
+import           What4.JSON ( (.:) )
+import           Data.Parameterized.Some (Some(..))
+import qualified Data.BitVector.Sized as BVS
+import qualified Numeric as Num
+
+newtype TraceIdentifier = TraceIdentifier String
+  deriving (Eq, Ord, IsString)
+
+data ConstraintOp = LTs | LTu | GTs | GTu | LEs | LEu | GEs | GEu | NEQ | EQ
+  deriving (Show, Read)
+
+data TraceConstraint sym = forall tp. TraceConstraint 
+  { tcVar :: W4.SymExpr sym tp
+  , tcOp :: ConstraintOp
+  , tcConst :: W4.ConcreteVal tp 
+  }
+
+instance forall sym. W4S.W4Deserializable sym (TraceConstraint sym) where
+  w4Deserialize_ v | W4S.SymDeserializable{} <- W4S.symDeserializable @sym  = do
+    JSON.Object o <- return v
+    (Some (var :: W4.SymExpr sym tp)) <- o .: "var"
+    (opJSON :: JSON.Value) <- o .: "op"
+    (op :: ConstraintOp) <- W4S.readJSON opJSON
+    case W4.exprType var of
+      W4.BaseBVRepr w -> do
+        (cS :: String) <- o .: "const"
+        ((c :: Integer),""):_ <- return $ Num.readDec cS
+        case (BVS.mkBVUnsigned w c) of
+          Just bv -> return $ TraceConstraint var op (W4.ConcreteBV w bv)
+          Nothing -> fail "Unexpected integer size"
+      _ -> fail "Unsupported expression type"
+
+{-
+instance forall sym arch. IsTraceNode '(sym :: DK.Type,arch) "trace_constraint" where
+  type TraceNodeType '(sym,arch) "trace_constraint" = TraceConstraint sym
+  prettyNode _ _ = PP.pretty ("TODO" :: String)
+  nodeTags = mkTags @'(sym,arch) @"trace_constraint" [Summary, Simplified]
+-}
+
+constraintToPred ::
+  forall sym.
+  W4.IsExprBuilder sym =>
+  sym ->
+  TraceConstraint sym -> 
+  IO (W4.Pred sym)
+constraintToPred sym (TraceConstraint var op c) = case W4.exprType var of
+  W4.BaseBVRepr w -> do
+    let W4.ConcreteBV _ bv = c
+    bvSym <- W4.bvLit sym w bv
+    let go :: (forall w. 1 W4.<= w => sym -> W4.SymBV sym w -> W4.SymBV sym w -> IO (W4.Pred sym)) -> IO (W4.Pred sym)
+        go f = f sym var bvSym
+    case op of
+      LTs -> go W4.bvSlt
+      LTu -> go W4.bvUlt
+      LEs -> go W4.bvSle
+      LEu -> go W4.bvUle
+      EQ -> go W4.isEq
+      _ -> fail "err"
+
+  _ -> fail "Unexpected constraint "
+
+
+
+newtype TraceConstraintMap sym arch = 
+  TraceConstraintMap (Map (GraphNode arch) (TraceConstraint sym))
+
+
+instance forall sym arch. IsTraceNode '(sym :: DK.Type,arch :: DK.Type) "trace_constraint_map" where
+  type TraceNodeType '(sym,arch) "trace_constraint_map" = TraceConstraintMap sym arch
+  prettyNode _ _ = PP.pretty ("TODO" :: String)
+  nodeTags = mkTags @'(sym,arch) @"trace_constraint_map" [Summary, Simplified]
+
+readConstraintMap ::
+  W4.IsExprBuilder sym =>
+  IsTreeBuilder '(sym,arch) e m =>
+  IO.MonadUnliftIO m =>
+  PA.ValidArch arch =>
+  sym ->
+  String {- ^ input prompt -} ->
+  [(GraphNode arch,W4S.ExprEnv sym)] ->
+  m (TraceConstraintMap sym arch)
+readConstraintMap sym msg ndEnvs = do
+  let parse s = case JSON.eitherDecode (fromString s) of
+        Left err -> return $ Left $ InputChoiceError "Failed to decode JSON" [err]
+        Right (v :: JSON.Value) -> runExceptT $ do
+          nodes <- runJSON $ do
+            JSON.Object o <- return v
+            (nodes :: [JSON.Value]) <- o JSON..: "trace_constraints"
+            return nodes
+          let nds = zip ndEnvs nodes
+          fmap (TraceConstraintMap . Map.fromList) $ forM nds $ \((nd, env), constraint_json) -> do
+             (lift $ W4S.jsonToW4 sym env constraint_json) >>= \case
+               Left err -> throwError $ InputChoiceError "Failed to parse value" [err]
+               Right a -> return (nd, a)
+  chooseInput_ @"trace_constraint_map" msg parse >>= \case
+    Nothing -> IO.liftIO $ fail "Unexpected trace map read"
+    Just a -> return a
+
+
+runJSON :: JSON.Parser a -> ExceptT InputChoiceError IO a
+runJSON p = ExceptT $ case JSON.parse (\() -> p) () of
+  JSON.Success a -> return $ Right a
+  JSON.Error err -> return $ Left $ InputChoiceError "Failed to parse value" [err]
+
+
+
+-- FIXME: Move
+readDeserializable ::
+  forall nm_choice sym k e m.
+  W4S.W4Deserializable sym (TraceNodeLabel nm_choice, TraceNodeType k nm_choice) =>
+  W4.IsExprBuilder sym =>
+  IsTreeBuilder k e m =>
+  IsTraceNode k nm_choice =>
+  IO.MonadUnliftIO m =>
+  sym ->
+  W4S.ExprEnv sym ->
+  String ->
+  m (Maybe (TraceNodeLabel nm_choice, TraceNodeType k nm_choice))
+readDeserializable sym env msg = do
+  let parse s = case JSON.eitherDecode (fromString s) of
+        Left err -> return $ Left $ InputChoiceError "Failed to decode JSON" [err]
+        Right (v :: JSON.Value) -> W4S.jsonToW4 sym env v >>= \case
+          Left err -> return $ Left $ InputChoiceError "Failed to parse value" [err]
+          Right a -> return $ Right a
+  chooseInput @nm_choice msg parse

src/Pate/Verification/StrongestPosts.hs

@@ -889,7 +889,7 @@ showFinalResult pg0 = withTracing @"final_result" () $ withSym $ \sym -> do
     True -> 
       let loop st_ = chooseBool "Regenerate result with new trace constraints?" >>= \case
             True -> do
-              tcs <- PTC.readConstraintMap sym "Waiting for constraints.." (getExprEnvs st_)
+              tcs <- PTC.readConstraintMap sym "Waiting for constraints.." (Map.toAscList (getExprEnvs st_))
               go (st_ {eqCondConstraints = tcs}) >>= loop
             False -> return ()
       in loop st

src/What4/JSON.hs

@@ -34,7 +34,10 @@ module What4.JSON
   , mergeEnvs
   , W4Deserializable(..)
   , jsonToW4
+  , readJSON
   , (.:)
+  , SymDeserializable(..)
+  , symDeserializable
   ) where
 
 import           Control.Monad.State (MonadState (..), State, modify, evalState, runState)
@@ -317,11 +320,16 @@ instance MonadFail (W4DS sym) where
   fail msg = throwError msg
 
 class W4Deserializable sym a where
-  w4Deserialize :: JSON.Value -> W4DS sym a
+  w4Deserialize_ :: W4.IsExprBuilder sym => JSON.Value -> W4DS sym a
 
-  default w4Deserialize :: JSON.FromJSON a => JSON.Value -> W4DS sym a
-  w4Deserialize v = fromJSON v
+  default w4Deserialize_ :: (W4.IsExprBuilder sym, JSON.FromJSON a) => JSON.Value -> W4DS sym a
+  w4Deserialize_ v = fromJSON v
 
+w4Deserialize :: W4Deserializable sym a => JSON.Value -> W4DS sym a
+w4Deserialize v = ask >>= \W4DSEnv{} -> w4Deserialize_ v
+
+instance W4Deserializable sym JSON.Value
+instance W4Deserializable sym String
 instance W4Deserializable sym Integer
 instance W4Deserializable sym Bool
 instance W4Deserializable sym ()
@@ -342,25 +350,31 @@ liftParser f v = case JSON.parse f v of
   JSON.Success a -> return a
   JSON.Error msg -> fail msg
 
+readJSON :: forall a sym. Read a => JSON.Value -> W4DS sym a
+readJSON v = do
+  (vS :: String) <- fromJSON v
+  (a :: a,""):_ <- return $ readsPrec 0 vS
+  return a
+
 (.:) :: 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
+  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
+  w4Deserialize_ v = Const <$> w4Deserialize v
 
 newtype ToDeserializable sym tp = ToDeserializable { _unDS :: W4.SymExpr sym tp }
 
 instance W4Deserializable sym (Some (ToDeserializable sym)) where
-  w4Deserialize v = fmap (\(Some x) -> Some (ToDeserializable x)) $ ask >>= \W4DSEnv{} -> asks w4dsSym >>= \sym -> do
+  w4Deserialize_ v = fmap (\(Some x) -> Some (ToDeserializable x)) $ asks w4dsSym >>= \sym -> do
       (i :: Integer) <- fromJSON v
       Some <$> (liftIO $ W4.intLit sym i)
     <|> do
@@ -383,70 +397,20 @@ instance W4Deserializable sym (Some (ToDeserializable sym)) where
       return $ Some e
 
 instance forall tp sym. KnownRepr W4.BaseTypeRepr tp => W4Deserializable sym (ToDeserializable sym tp) where
-  w4Deserialize v = ask >>= \W4DSEnv{} -> do
+  w4Deserialize_ v = do
     Some (ToDeserializable e :: ToDeserializable sym tp') <- w4Deserialize v
     case testEquality (knownRepr @_ @_ @tp) (W4.exprType e) of
       Just Refl -> return $ ToDeserializable e
       Nothing -> fail $ "Unexpected type: " ++ show (W4.exprType e)
 
-newtype SymDeserializable sym f = SymDeserializable (forall tp a. ((KnownRepr W4.BaseTypeRepr tp => W4Deserializable sym (f tp)) => a) -> a)
+-- | Small hack to pretend that W4.SymExpr has a W4Deserializable instance, which haskell's
+-- type class mechanism doesn't support because W4.SymExpr is a type family
+data SymDeserializable sym f = W4Deserializable sym (Some f) => SymDeserializable
 
 symDeserializable ::
   forall sym.
-  sym ->
   SymDeserializable sym (W4.SymExpr sym)
-symDeserializable _sym = unsafeCoerce r
+symDeserializable = unsafeCoerce r
   where
     r :: SymDeserializable sym (ToDeserializable sym)
-    r = SymDeserializable (\a -> a)
-
-{-
-class (TestEquality g, KnownRepr g k) => W4DeserializableF sym (f :: k -> Type) where
-  withDeserializable :: Proxy sym -> p f -> q tp -> (W4Deserializable sym (f tp) => a) -> a
-
-  default withDeserializable :: W4Deserializable sym (f tp) => Proxy sym -> p f -> q tp -> (W4Deserializable sym (f tp) => a) -> a
-  withDeserializable _ _ _ x = x
-
-  w4DeserializeF :: forall tp. JSON.Value -> W4DS sym (f tp)
-  w4DeserializeF x = withDeserializable (Proxy :: Proxy sym) (Proxy :: Proxy f) (Proxy :: Proxy tp) (w4Deserialize x)
--}
-
-{-
-data WrappedBuilder sym = 
-    WrappedBuilder { wSym :: sym, wEnv :: MapF (W4.SymAnnotation sym) (W4.SymExpr sym)}
-
-data WSymExpr sym tp where
-  WSymExpr :: W4.SymAnnotation sym tp -> WSymExpr sym tp
-  WConc :: W4.ConcreteVal tp -> WSymExpr sym tp
-
-
-instance JSON.FromJSON (Some (W4.SymAnnotation sym)) => JSON.FromJSON (Some (WSymExpr sym)) where
-  parseJSON v = do
-    JSON.Object o <- return v
-    go o
-    where
-      go o = do 
-          Some (ann :: W4.SymAnnotation sym tp) <- o JSON..: "ann"
-          return $ Some (WSymExpr ann)
-        <|> do
-          (i :: Integer) <- o JSON..: "conc_int"
-          return $ Some $ WConc (W4.ConcreteInteger i)
-        <|> do
-          (i :: Bool) <- o JSON..: "conc_bool"
-          return $ Some $ WConc (W4.ConcreteBool i)
-        <|> fail "Unsupported value"
-
-
-instance JSON.ToJSON (W4.SymAnnotation sym tp) => JSON.ToJSON (WSymExpr sym tp) where
-  toJSON = 
-
-
-
-instance forall sym sym'. (sym ~ WrappedBuilder sym', W4.IsExprBuilder sym', W4Deserializable sym (Some (W4.SymAnnotation sym'))) => W4Deserializable sym (Some (WSymExpr sym)) where
-  w4Deserialize v = do
-    Some (ann :: W4.SymAnnotation sym' tp') <- w4Deserialize v
-    sym <- asks w4dsSym
-    case MapF.lookup ann (wEnv sym) of
-      Just e -> return $ Some $ WSymExpr e
-      Nothing -> fail "Missing annotation"
--}
+    r = SymDeserializable