diff --git a/src/Pate/TraceConstraint.hs b/src/Pate/TraceConstraint.hs index b362724f..4edabe16 100644 --- a/src/Pate/TraceConstraint.hs +++ b/src/Pate/TraceConstraint.hs @@ -18,8 +18,7 @@ module Pate.TraceConstraint ( - TraceConstraint(..) - , readDeserializable + TraceConstraint , constraintToPred , TraceConstraintMap(..) , readConstraintMap @@ -81,14 +80,7 @@ instance forall sym. W4S.W4Deserializable sym (TraceConstraint sym) where 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] --} + _ -> fail ("Unsupported expression type:" ++ show (W4.exprType var)) constraintToPred :: forall sym. @@ -102,14 +94,19 @@ constraintToPred sym (TraceConstraint var op c) = case W4.exprType var of 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 + let goNot :: (forall w. 1 W4.<= w => sym -> W4.SymBV sym w -> W4.SymBV sym w -> IO (W4.Pred sym)) -> IO (W4.Pred sym) + goNot f = f sym var bvSym >>= W4.notPred sym 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" - + GTs -> goNot W4.bvSle + GTu -> goNot W4.bvUle + GEs -> goNot W4.bvSlt + GEu -> goNot W4.bvUlt + NEQ -> goNot W4.isEq _ -> fail "Unexpected constraint " @@ -121,7 +118,7 @@ newtype TraceConstraintMap sym arch = 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] + nodeTags = [] readConstraintMap :: W4.IsExprBuilder sym => @@ -136,15 +133,13 @@ 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 + (nodes :: [[JSON.Value]]) <- runJSON $ JSON.parseJSON v 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) + fmap (TraceConstraintMap . Map.fromList . concat) $ + forM nds $ \((nd, env), constraints_json) -> forM constraints_json $ \constraint_json -> + (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 @@ -153,26 +148,4 @@ readConstraintMap sym msg ndEnvs = do 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 + JSON.Error err -> return $ Left $ InputChoiceError "Failed to parse value" [err] \ No newline at end of file diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index 7aa66c09..47b094ac 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -934,7 +934,13 @@ showFinalResult pg0 = withTracing @"final_result" () $ withSym $ \sym -> do 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 + fps <- getTraceFootprint scope bundle + eenv <- PPa.joinPatchPred (\a b -> return $ W4S.mergeEnvs a b) $ \bin -> do + fp <- PPa.getC bin fps + (v, env) <- liftIO $ W4S.w4ToJSONEnv sym fp + -- only visible with debug tag + emitTraceLabel @"trace_footprint" v fp + return env asms <- currentAsm let ieqc = IntermediateEqCond bundle fps eenv asms eqCond_pred d let interims = Map.insert nd (PS.mkSimSpec scope ieqc) (eqCondInterims rs) diff --git a/src/Pate/Verification/StrongestPosts/CounterExample.hs b/src/Pate/Verification/StrongestPosts/CounterExample.hs index 27f9356b..92d3c16f 100644 --- a/src/Pate/Verification/StrongestPosts/CounterExample.hs +++ b/src/Pate/Verification/StrongestPosts/CounterExample.hs @@ -73,6 +73,9 @@ import What4.JSON import Pate.Equivalence (StatePostCondition) import qualified Pate.Binary as PB import GHC.Stack (HasCallStack) +import qualified Data.Aeson as JSON +import qualified Data.Text.Lazy.Encoding as Text +import qualified Data.Text.Encoding.Error as Text -- | A totality counterexample represents a potential control-flow situation that represents -- desynchronization of the original and patched program. The first tuple represents @@ -253,6 +256,13 @@ data TraceFootprint sym arch = TraceFootprint , fpMem :: [(MM.ArchSegmentOff arch, (MT.MemOp sym (MM.ArchAddrWidth arch)))] } +instance (PSo.ValidSym sym, PA.ValidArch arch) => IsTraceNode '(sym,arch) "trace_footprint" where + type TraceNodeType '(sym,arch) "trace_footprint" = TraceFootprint sym arch + type TraceNodeLabel "trace_footprint" = JSON.Value + prettyNode json _ = PP.pretty $ Text.decodeUtf8With Text.lenientDecode $ JSON.encode json + nodeTags = mkTags @'(sym,arch) @"trace_footprint" ["debug"] + jsonNode _ json _ = return json + mkFootprint :: forall sym arch. W4.IsExprBuilder sym => @@ -275,7 +285,7 @@ mkFootprint sym init_regs s = do _ -> return [] instance (PA.ValidArch arch, PSo.ValidSym sym) => W4S.W4Serializable sym (TraceFootprint sym arch) where - w4Serialize fp = W4S.object [ "fp_initial_regs" .= fpInitialRegs fp, "fp_mem" .= fpMem fp] + w4Serialize fp = W4S.object [ "fp_mem" .= fpMem fp, "fp_initial_regs" .= fpInitialRegs fp] instance (PA.ValidArch arch, PSo.ValidSym sym) => W4S.W4Serializable sym (TraceEvents sym arch) where w4Serialize (TraceEvents p pre post) = do diff --git a/src/Pate/Verification/Widening.hs b/src/Pate/Verification/Widening.hs index bdc32d70..5fcff5f6 100644 --- a/src/Pate/Verification/Widening.hs +++ b/src/Pate/Verification/Widening.hs @@ -524,9 +524,8 @@ getTraceFootprint :: forall sym arch v. PS.SimScope sym arch v -> SimBundle sym arch v -> - 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 + 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_ @@ -534,19 +533,7 @@ getTraceFootprint _scope bundle = withSym $ \sym -> do 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 - 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 - type TraceNodeLabel "trace_footprint" = JSON.Value - prettyNode json _ = PP.pretty $ Text.decodeUtf8With Text.lenientDecode $ JSON.encode json - nodeTags = [(Summary, \_ _ -> "TODO"), (Simplified, \_ _ -> "TODO")] - jsonNode _ json _ = return json + liftIO $ CE.mkFootprint sym rop s' -- | Compute a counter-example for a given predicate getTraceFromModel :: diff --git a/src/What4/JSON.hs b/src/What4/JSON.hs index 2a13bc03..f942c84b 100644 --- a/src/What4/JSON.hs +++ b/src/What4/JSON.hs @@ -44,7 +44,7 @@ import Control.Monad.State (MonadState (..), State, modify, evalState, import qualified Data.Map.Ordered as OMap import Data.List ( stripPrefix ) -import Data.Maybe ( mapMaybe ) +import Data.Maybe ( mapMaybe, catMaybes ) import Data.Map (Map) import qualified Data.Map.Merge.Strict as Map import Data.Text (Text) @@ -137,13 +137,15 @@ mergeEnvs (ExprEnv env1) (ExprEnv env2) = ExprEnv ( 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) +cacheToEnv :: W4.IsExprBuilder sym => sym -> ExprCache sym -> IO (ExprEnv sym) +cacheToEnv _sym (ExprCache m) = (ExprEnv . Map.fromList . catMaybes) <$> mapM go (Map.keys m) where go (Some e) | Nothing <- W4.asConcrete e - = Just (fromIntegral $ hashF e, Some e) - go _ = Nothing + = do + ident <- mkIdent e + return $ Just (ident, Some e) + go _ = return Nothing w4ToJSONEnv :: forall sym a. (W4.IsExprBuilder sym, SerializableExprs sym) => W4Serializable sym a => sym -> a -> IO (JSON.Value, ExprEnv sym) w4ToJSONEnv sym a = do @@ -152,7 +154,8 @@ w4ToJSONEnv sym a = do let env = W4SEnv cacheRef sym True v <- runReaderT f env c <- IO.readIORef cacheRef - return $ (v, cacheToEnv sym c) + eenv <- cacheToEnv sym c + return $ (v, eenv) class W4SerializableF sym (f :: k -> Type) where withSerializable :: Proxy sym -> p f -> q tp -> (W4Serializable sym (f tp) => a) -> a @@ -181,6 +184,19 @@ trySerialize (W4S f) = do Left err -> return $ Left (show err) Right x -> return $ Right x +firstHashRef :: IO.IORef (Maybe Integer) +firstHashRef = unsafePerformIO (IO.newIORef Nothing) + +-- | Makes hashes slightly more stable by fixing the first requested +-- identifier and deriving all subsequent identifiers as offsets from it +mkIdent :: HashableF t => t tp -> IO Integer +mkIdent v = do + let (ident :: Integer) = fromIntegral $ hashF v + let f = \case + Just i -> (Just i, ident - i) + Nothing -> (Just ident, 0) + IO.atomicModifyIORef firstHashRef f + instance sym ~ W4B.ExprBuilder t fs scope => W4Serializable sym (W4B.Expr t tp) where w4Serialize e' = do ExprCache s <- get @@ -196,7 +212,7 @@ instance sym ~ W4B.ExprBuilder t fs scope => W4Serializable sym (W4B.Expr t tp) asks w4sUseIdents >>= \case True -> do let tp_sexpr = W4S.serializeBaseType (W4.exprType e') - let (ident :: Integer) = fromIntegral $ hashF e' + ident <- liftIO $ mkIdent e' return $ JSON.object [ "symbolic_ident" JSON..= ident, "type" JSON..= JSON.String (W4D.printSExpr mempty tp_sexpr) ] False -> do e <- liftIO $ WEH.stripAnnotations sym e' diff --git a/tests/integration/packet/packet.exp b/tests/integration/packet/packet.exp index be269004..6cfe432f 100755 --- a/tests/integration/packet/packet.exp +++ b/tests/integration/packet/packet.exp @@ -18,7 +18,7 @@ # Also note this example is mentioned in the README.rst and used in the User Manual. # Major changes here likely warrant an update of the corresponding User Manual content. -spawn ./pate.sh --original tests/integration/packet/exe/packet.exe --patched tests/integration/packet/exe/packet.patched.exe -s parse_packet +spawn ./pate.sh --original tests/integration/packet/exe/packet.exe --patched tests/integration/packet/exe/packet.patched.exe -s parse_packet --add-trace-constraints set timeout 480 @@ -42,6 +42,17 @@ expect "0: Finish and view final result" expect "?>" send "0\r" +expect "Regenerate result with new trace constraints?" +expect "0: True" +send "0\r" +expect "Waiting for constraints.." +send "input \"\[ \[ { \\\"var\\\" : { \\\"symbolic_ident\\\" : -6 }, \\\"op\\\" : \\\"NEQ\\\", \\\"const\\\" : \\\"128\\\"} \] \]\"\r" + +expect "Regenerate result with new trace constraints?" +expect "1: False" +send "1\r" + + expect "15: Final Result" expect ">" send "15\r" @@ -51,19 +62,38 @@ expect "2: Binaries are conditionally, observably equivalent" expect ">" send "0\r" + + # Inspect the specific equivalence condition expect "0: segment1+0x644 \\\[ via: \"parse_packet\" (segment1+0x554) \\\]" expect ">" send "0\r" -expect "3: let -- segment1+0x664.. in not v40591" +expect -re {3: let -- segment1\+0x664.. in not v(\d)+} expect ">" send "3\r" -expect "v40591 = and (eq 0x80:\\\[8\\\] v40584) (not (eq v40587 (bvSum v40584 0x80:\\\[8\\\])))" -expect "in not v40591" +expect -re {v((\d)+) = and \(eq 0x80:\[8\] v((\d)+)\) \(not \(eq v((\d)+) \(bvSum v((\d)+) 0x80:\[8\]\)\)\)} +expect -re {in not v((\d)+)} +expect ">" + +send "up\r" expect ">" +send "up\r" +expect ">" +send "up\r" +expect "5: Assumed Equivalence Conditions" +expect ">" +send "5\r" + +expect "0: segment1+0x644 \\\[ via: \"parse_packet\" (segment1+0x554) \\\]" +expect ">" +send "0\r" + +# constraint has made the equivalence condition satisified +expect "0: true" + send "\x04" ; # Ctrl-D (EOF) # remove EOF from expect_before, now that we're expecting it