misc. trace presentation fixes

arch/Pate/PPC.hs

@@ -273,7 +273,7 @@ argumentMapping :: (1 <= SP.AddrWidth v) => PVO.ArgumentMapping (PPC.AnyPPC v)
 argumentMapping = undefined
 
 
-specializedBufferWrite :: forall arch v. (arch ~ PPC.AnyPPC v, 16 <= SP.AddrWidth v, MS.SymArchConstraints arch) => PA.StubOverride arch
+specializedBufferWrite :: forall arch v. (arch ~ PPC.AnyPPC v, PA.ValidArch (PPC.AnyPPC v)) => PA.StubOverride arch
 specializedBufferWrite = 
     PA.mkEventOverride "CFE_SB_TransmitBuffer" mkEvent 0x30 (gpr 3) (gpr 3)
     where
@@ -294,7 +294,7 @@ specializedBufferWrite =
         WI.baseTypeIte sym is_expect expect_value' zero
 
 -- FIXME: flags to make it equal?
-specializeSocketRead :: forall arch v. (Typeable arch, arch ~ PPC.AnyPPC v, 16 <= SP.AddrWidth v, MS.SymArchConstraints arch) => PA.StubOverride arch
+specializeSocketRead :: forall arch v. (arch ~ PPC.AnyPPC v, PA.ValidArch (PPC.AnyPPC v)) => PA.StubOverride arch
 specializeSocketRead = 
     PA.mkReadOverride "OS_SocketRecvFrom" (PPa.PatchPairSingle PB.PatchedRepr (Const f)) addrs lengths (gpr 3) (gpr 4) (gpr 5) (gpr 3)
     where
@@ -308,7 +308,7 @@ specializeSocketRead =
       f = PA.modifyConcreteChunk MC.BigEndian WI.knownNat (0x300 :: Integer) 2 4
 
 -- FIXME: clagged directly from ARM, registers may not be correct
-stubOverrides :: (Typeable (PPC.AnyPPC v), MS.SymArchConstraints (PPC.AnyPPC v), 1 <= SP.AddrWidth v, 16 <= SP.AddrWidth v) => PA.ArchStubOverrides (PPC.AnyPPC v)
+stubOverrides :: PA.ValidArch (PPC.AnyPPC v) => PA.ArchStubOverrides (PPC.AnyPPC v)
 stubOverrides = PA.ArchStubOverrides (PA.mkDefaultStubOverride "__pate_stub" r3 ) $ \fs ->
   lookup (PBl.fnSymBase fs) override_list
   where

pate_binja/pate.py

@@ -617,9 +617,7 @@ def processFinalResult(self, traceConstraints: Optional[list[tuple[TraceVar, str
             if not lastTopLevelResult:
                 out.write(f'No equivalence conditions found\n')
             else:
-                eqStatus = lastTopLevelResult.get('content', {}).get('eq_status')
-                out.write(f'Equivalence status: {eqStatus}\n')
-                out.write('\n')
+
                 eqconds = lastTopLevelResult.get('content', {}).get('eq_conditions', {}).get('map')
                 if eqconds:
                     # Found eq conditions
@@ -639,9 +637,9 @@ def processFinalResult(self, traceConstraints: Optional[list[tuple[TraceVar, str
 
                         # print('CFAR id:', node_id)
 
-                        out.write(f'Equivalence condition for {node_id}\n')
+                        out.write(f'Equivalence condition for {node_id}:\n')
                         pprint_symbolic(out, predicate)
-                        out.write('\n')
+                        out.write('\n\n')
 
                         # out.write('\nTrace True\n')
                         # pprint_node_event_trace(trace_true, 'True Trace', out=out)
@@ -656,7 +654,10 @@ def processFinalResult(self, traceConstraints: Optional[list[tuple[TraceVar, str
                     ect.trace_false = False
                     ect.traceConstraints = traceConstraints
                     ect.predicate = ect.unconstrainedPredicate
-
+
+                eqStatus = lastTopLevelResult.get('content', {}).get('eq_status').get('message')
+                out.write(f'Equivalence status: {eqStatus}\n')
+
             self.user.show_message(out.getvalue())
         if self.last_cfar_graph:
             self.user.show_cfar_graph(self.last_cfar_graph)
@@ -1504,7 +1505,7 @@ def pprint_node_event_trace_domain(trace, pre: str = '', out: IO = sys.stdout):
     # possibly not obvious why a given trace violates the post-condition, which is why I
     # think we included it in the first place.
     if not (postcond):
-        out.write(f'{pre}No Post Condition.\n')
+        out.write(f'{pre}')
         return
 
     if precond:
@@ -1615,6 +1616,8 @@ def pprint_mem_op(mem_op: dict, pre: str = '', out: IO = sys.stdout, prune_zero:
 def pretty_call_arg(arg):
     if isinstance(arg, dict) and 'data_expr' in arg:
         return str(arg['data_expr'])
+    elif isinstance(arg, dict) and 'pointer' in arg:
+      return (get_value_id(arg['pointer']))
     else:
         return str(arg)
 

pate_binja/view.py

@@ -457,7 +457,7 @@ def setTracePosVsNeg(self, posTrace: Optional[dict], negTrace: Optional[dict], b
             self.traceDiff.clear('None')
             return
 
-        self._setDomainText('NA')
+        self._setDomainText('')
 
         pw: Optional[PateWidget] = getAncestorInstanceOf(self, PateWidget)
 
@@ -552,7 +552,18 @@ def __init__(self, cfarNode,
         self.eqCondField.setReadOnly(True)
         self.eqCondField.setMaximumBlockCount(1000)
         eqCondBoxLayout = QVBoxLayout()
-        eqCondBoxLayout.addWidget(QLabel("Programs behave equivalently when:"))
+        label_prefix = ''
+        match label:
+          case 'Asserted Condition':
+            label_prefix = 'Asserted precondition'
+          case 'Assumed Condition':
+            label_prefix = 'Assumed precondition'
+          case 'Equivalence Condition':
+            label_prefix = 'Assumed equivalence condition'
+          case _:
+            label_prefix = 'Precondition'
+
+        eqCondBoxLayout.addWidget(QLabel(f'{label_prefix} (assuming all ancestor preconditions):'))
         eqCondBoxLayout.addWidget(self.eqCondField)
         eqCondBox = QWidget()
         eqCondBox.setLayout(eqCondBoxLayout)
@@ -570,8 +581,8 @@ def __init__(self, cfarNode,
         # Diff Mode Control
         diffModeLabel = QLabel("Difference mode:")
         self.diffModeComboBox = QComboBox()
-        self.diffModeComboBox.addItem("Original VS Patched")
-        self.diffModeComboBox.addItem("Equivalent VS Different")
+        self.diffModeComboBox.addItem("Original vs. Patched")
+        self.diffModeComboBox.addItem("Condition assumed TRUE vs. FALSE")
         self.diffModeComboBox.currentTextChanged.connect(self.diffModeChanged)
         diffModeBoxLayout = QHBoxLayout()
         diffModeBoxLayout.addWidget(diffModeLabel)
@@ -638,14 +649,14 @@ def updateFromCfarNode(self):
                 else:
                     out.write('\nEquivalence condition unsatisfiable with user-supplied constraints.\n')
             else:
-                out.write('\nNo user-supplied trace constraints.\n')
+                out.write('')
             self.eqCondField.appendPlainText(out.getvalue())
-        if self.diffModeComboBox.currentText() == "Original VS Patched":
+        if self.diffModeComboBox.currentText() == "Original vs. Patched":
             # Original VS Patch Diff Mode
             self.trueTraceWidget.setTrace(self.conditionTrace.trace_true)
-            self.trueTraceLabel.setText('Trace showing EQUIVALENT behaviour, original vs patched:')
+            self.trueTraceLabel.setText('Trace assuming above condition is TRUE, original vs. patched:')
             self.falseTraceWidget.setTrace(self.conditionTrace.trace_false)
-            self.falseTraceLabel.setText('Trace showing DIFFERENT behaviour, original vs patched:')
+            self.falseTraceLabel.setText('Trace assuming above condition is FALSE, original vs. patched:')
         else:
             # Positive VS Negative Diff Mode
             # TODO: What about conditions in this mode? Drop?
@@ -672,9 +683,9 @@ def updateFromCfarNode(self):
                 pbv = None
 
             self.trueTraceWidget.setTracePosVsNeg(originalPosTrace, originalNegTrace, pbv)
-            self.trueTraceLabel.setText('Trace showing original program, EQUIVALENT vs DIFFERENT behaviour:')
+            self.trueTraceLabel.setText('Trace for original, assuming above condition is TRUE vs. FALSE:')
             self.falseTraceWidget.setTracePosVsNeg(patchedPosTrace, patchedNegTrace, obv)
-            self.falseTraceLabel.setText('Trace showing patched program, EQUIVALENT vs DIFFERENT behaviour:')
+            self.falseTraceLabel.setText('Trace for patched, assuming above condition is TRUE vs. FALSE:')
 
     def diffModeChanged(self, text):
         print('Difference mode:', self.diffModeComboBox.currentText())