GUI: updating the equivalence condition display per #398

pate_binja/pate.py

@@ -535,7 +535,7 @@ def process_json(self, rec):
 
         return True
 
-    def processFinalResult(self):
+    def processFinalResult(self, traceConstraints: list[tuple[TraceVar, str, str]] = None):
         self._command('up')
         rec = self.next_json()
         # isinstance(rec, dict) and rec.get('trace_node_kind') == 'final_result':
@@ -569,10 +569,13 @@ def processFinalResult(self):
 
                         if self.last_cfar_graph:
                             cfar_node = self.last_cfar_graph.get(node_id)
+                            if cfar_node.predicate is None:
+                                cfar_node.unconstrainedPredicate = predicate
                             cfar_node.predicate = predicate
                             cfar_node.trace_true = trace_true
                             cfar_node.trace_false = trace_false
                             cfar_node.trace_footprint = trace_footprint
+                            cfar_node.traceConstraints = traceConstraints
 
             self.user.show_message(out.getvalue())
         if self.last_cfar_graph:
@@ -588,7 +591,9 @@ def processTraceConstraints(self, traceConstraints: list[tuple[TraceVar, str, st
             out.write(r'input "[')
             # TODO: Handle multiple eq conds
             out.write(r'[')
-            for tc in traceConstraints:
+            for i, tc in enumerate(traceConstraints):
+                if i > 0:
+                    out.write(r',')
                 out.write(r'{\"var\":{\"symbolic_ident\":')
                 # symbolic_ident
                 out.write(str(tc[0].symbolic_ident))
@@ -616,7 +621,7 @@ def processTraceConstraints(self, traceConstraints: list[tuple[TraceVar, str, st
             rec = self.next_json()
             if isinstance(rec, dict) and rec['this'] == 'Regenerate result with new trace constraints?':
                 break
-        self.processFinalResult()
+        self.processFinalResult(traceConstraints)
 
     def show_message(self, rec: Any):
         if isinstance(rec, list):
@@ -645,10 +650,12 @@ def __init__(self, id: str, desc: str, data: dict):
         self.external_postdomain = None
         self.addr = None
         self.finished = True
+        self.unconstrainedPredicate = None
         self.predicate = None
         self.trace_true = None
         self.trace_false = None
         self.trace_footprint = None
+        self.traceConstraints = None
         self.instruction_trees = None
 
     def update_node(self, desc: str, data: dict):

pate_binja/view.py

@@ -460,6 +460,7 @@ def __init__(self, cfarNode, parent=None):
         super().__init__(parent)
 
         self.cfarNode = cfarNode
+        self.traceConstraints = None
 
         self.resize(1500, 800)
 
@@ -519,7 +520,17 @@ def __init__(self, cfarNode, parent=None):
     def updateFromCfarNode(self):
         self.eqCondField.clear()
         with io.StringIO() as out:
-            pate.pprint_symbolic(out, self.cfarNode.predicate)
+            pate.pprint_symbolic(out, self.cfarNode.unconstrainedPredicate)
+            out.write('\n')
+            if self.cfarNode.traceConstraints:
+                #print(self.cfarNode.traceConstraints)
+                out.write('\nUser-supplied trace constraints:\n')
+                for tc in self.cfarNode.traceConstraints:
+                    out.write(f'{tc[0].pretty} {tc[1]} {tc[2]}\n')
+                out.write('\nEffective equivalence condition after adding user-provided constraints::\n')
+                pate.pprint_symbolic(out, self.cfarNode.predicate)
+            else:
+                out.write('\nNo user-supplied trace constraints.\n')
             self.eqCondField.appendPlainText(out.getvalue())
         self.trueTraceWidget.setTrace(self.cfarNode.trace_true)
         self.falseTraceWidget.setTrace(self.cfarNode.trace_false)
@@ -528,11 +539,11 @@ def showTrueTraceConstraintDialog(self):
         d = PateTraceConstraintDialog(self.cfarNode, parent=self)
         #d.setWindowTitle(f'{d.windowTitle()} - {cfarNode.id}')
         if d.exec():
-            traceConstraints = d.getConstraints()
-            #print(traceConstraints)
+            self.traceConstraints = d.getConstraints()
+            #print(self.traceConstraints)
             pw: Optional[PateWidget] = getAncestorInstanceOf(self, PateWidget)
             # TODO: Better way to do this?
-            pw.pate_thread.pate_wrapper.processTraceConstraints(traceConstraints)
+            pw.pate_thread.pate_wrapper.processTraceConstraints(self.traceConstraints)
             self.updateFromCfarNode()
             # TODO: report failed constraint?