From 4508ebe28c128dda8774741c59e6d6fba518d34f Mon Sep 17 00:00:00 2001
From: Daniel Matichuk <dmatichuk@galois.com>
Date: Thu, 9 Nov 2023 10:03:26 -0800
Subject: [PATCH] add final result to json output

---
 src/Pate/Equivalence.hs           | 2 +-
 src/Pate/Equivalence/Condition.hs | 6 ++++++
 src/Pate/TraceTree.hs             | 2 +-
 3 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/Pate/Equivalence.hs b/src/Pate/Equivalence.hs
index ca897326..f9e2f69b 100644
--- a/src/Pate/Equivalence.hs
+++ b/src/Pate/Equivalence.hs
@@ -115,7 +115,7 @@ instance IsTraceNode k "equivalence_result" where
     Inequivalent -> "Binaries are not observably equivalent"
     ConditionallyEquivalent -> "Binaries are conditionally, observably equivalent"
     Errored{} -> "Analysis failure due to error"
-  nodeTags = mkTags @k @"equivalence_result" [Summary, Simplified]
+  nodeTags = mkTags @k @"equivalence_result" [Summary, Simplified, JSONTrace]
 
 ---------------------------------------
 
diff --git a/src/Pate/Equivalence/Condition.hs b/src/Pate/Equivalence/Condition.hs
index 400bed60..fac3385e 100644
--- a/src/Pate/Equivalence/Condition.hs
+++ b/src/Pate/Equivalence/Condition.hs
@@ -167,7 +167,13 @@ instance forall sym arch. IsTraceNode '(sym :: DK.Type,arch :: DK.Type) "eqcond"
     EquivalenceCondition{} -> PP.pretty someExpr
   nodeTags = [(Summary, \someExpr _ -> printSomeExprTruncated someExpr )
              ,(Simplified, \someExpr _ -> printSomeExprTruncated someExpr)
+             ,(JSONTrace, \someExpr _ -> printSomeExprTruncated someExpr)
              ]
+  jsonNode someExpr _ = 
+    JSON.object 
+      [ "trace_node_kind" JSON..= "eqcond"
+      , "trace_node" JSON..= show (PP.pretty someExpr)
+      ]
 
 -- | A mapping from registers to a predicate representing an equality condition for
 -- that specific register.
diff --git a/src/Pate/TraceTree.hs b/src/Pate/TraceTree.hs
index bacf9956..a98a0d79 100644
--- a/src/Pate/TraceTree.hs
+++ b/src/Pate/TraceTree.hs
@@ -616,7 +616,7 @@ instance IsTraceNode k "bool" where
 instance IsTraceNode k "final_result" where
   type TraceNodeType k "final_result" = ()
   prettyNode _lbl _msg = "Final Result"
-  nodeTags = mkTags @k @"final_result" [Summary, Simplified]
+  nodeTags = mkTags @k @"final_result" [Summary, Simplified, JSONTrace]
 
 data ChoiceHeader k (nm_choice :: Symbol) a = 
   (IsTraceNode k nm_choice) =>