add final result to json output

GaloisInc · Nov 9, 2023 · 4508ebe · 4508ebe
1 parent 7ab3bfa
commit 4508ebe
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 2 deletions.
diff --git 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
@@ -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
@@ -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) =>