From 0bc01256b25785d6cda094e74de35bc22bea5c89 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Thu, 9 Nov 2023 12:56:04 -0800 Subject: [PATCH] add assertion location to json output --- src/Pate/Verification/Widening.hs | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/src/Pate/Verification/Widening.hs b/src/Pate/Verification/Widening.hs index 204f9b02..5444e6d0 100644 --- a/src/Pate/Verification/Widening.hs +++ b/src/Pate/Verification/Widening.hs @@ -587,7 +587,16 @@ data PickManyChoice sym arch = instance forall sym arch. (PSo.ValidSym sym, PA.ValidArch arch) => JSON.ToJSON (PickManyChoice sym arch) where -- FIXME: Needs more structure - toJSON e = JSON.object ["pickManyChoice" JSON..= (show (prettyNode @_ @'(sym,arch) @"pickManyChoice" () e))] + toJSON = \case + PickRegister r -> JSON.object + [ "register" JSON..= case PA.fromRegisterDisplay (PA.displayRegister r) of + Just s -> s + Nothing -> MapF.showF r] + PickStack s -> JSON.object [ "stack_cell" JSON..= show (pretty s)] + PickGlobal s -> JSON.object [ "mem_cell" JSON..= show (pretty s)] + PickIncludeAllRegisters -> JSON.String "all_registers" + PickIncludeAll -> JSON.String "all" + PickFinish -> JSON.String "finish" data PickChoices sym arch = PickChoices { pickRegs :: [Some (MM.ArchReg arch)] @@ -612,7 +621,8 @@ instance (PSo.ValidSym sym, PA.ValidArch arch) => IsTraceNode '(sym,arch) "pickM PickIncludeAllRegisters -> "Include All Registers" PickIncludeAll -> "Include All Locations" PickFinish -> "Finish" - nodeTags = mkTags @'(sym,arch) @"pickManyChoice" [Summary, Simplified] + nodeTags = mkTags @'(sym,arch) @"pickManyChoice" [Summary, Simplified, JSONTrace] + jsonNode = nodeToJSON @'(sym,arch) @"pickManyChoice" pickMany :: PickChoices sym arch ->