finalize trace constraint parsing:

* takes an ordered list of lists of triples: var-op-const
* identifiers are now somewhat more stable, as they
  are computed as an offset from some initial hash
* don't include trace footprints in tracetree by default
  - these are part of the toplevel output currently
  - can still be inspected via the "debug" tag
* support "negated" comparison ops (i.e. GE, GT, NEQ)

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]

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)

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

src/Pate/Verification/Widening.hs

@@ -524,29 +524,16 @@ 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_
     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
-    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 ::

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'

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