Merge branch 'master' into dm/packet-mod

GaloisInc · Jan 20, 2025 · 8aee61e · 8aee61e
2 parents 733be4f + 72e1df9
commit 8aee61e
Show file tree

Hide file tree

Showing 2 changed files with 24 additions and 4 deletions.
diff --git a/pate_binja/pate.py b/pate_binja/pate.py
@@ -384,17 +384,23 @@ def extract_graph_rec(self,
                             eqCond = ConditionTrace(ccontent)
                             match this:
                                 case 'Asserted':
-                                    #print('Found asserted cond for ', cfar_parent.id)
+                                    print('Found asserted cond for', cfar_parent.id)
                                     if cfar_parent.assertedConditionTrace:
                                         cfar_parent.assertedConditionTrace.update(ccontent)
                                     else:
                                         cfar_parent.assertedConditionTrace = ConditionTrace(ccontent)
-                                case 'Equivalence Condition Assumed':
-                                    #print('Found assumed cond for ', cfar_parent.id)
+                                case 'Assumed':
+                                    print('Found assumed cond for', cfar_parent.id)
                                     if cfar_parent.assumedConditionTrace:
                                         cfar_parent.assumedConditionTrace.update(ccontent)
                                     else:
                                         cfar_parent.assumedConditionTrace = ConditionTrace(ccontent)
+                                case 'Equivalence Condition Assumed':
+                                    print('Found equivalance conditions for', cfar_parent.id)
+                                    if cfar_parent.equivalenceConditionTrace:
+                                        cfar_parent.equivalenceConditionTrace.update(ccontent)
+                                    else:
+                                        cfar_parent.equivalenceConditionTrace = ConditionTrace(ccontent)
 
                     self.command('up')
                     # Consume result of up, but do not need it
@@ -896,6 +902,18 @@ def pprint_node_contents(self, pre: str = '', out: IO = sys.stdout, show_ce_trac
                 elif self.exit_meta_data.get(n, {}).get('event_trace'):
                     pprint_node_event_trace(self.exit_meta_data[n]['event_trace'], 'Witness Trace', pre + '  ', out)
 
+        # Indicate if there are conditions traces
+        conditionTraceTypes = []
+        if self.equivalenceConditionTrace:
+            conditionTraceTypes.append('equivalence')
+        if self.assertedConditionTrace:
+            conditionTraceTypes.append('asserted')
+        if self.assumedConditionTrace:
+            conditionTraceTypes.append('assumed')
+        if conditionTraceTypes:
+            out.write('Condition traces for: ')
+            out.write(', '.join(conditionTraceTypes))
+
     def pprint_node_domain(self, pre: str = '', out: IO = sys.stdout,
                            show_ce_trace: bool = False):
         if self.predomain:

diff --git a/pate_binja/view.py b/pate_binja/view.py
@@ -218,13 +218,15 @@ def ask_user(self, prompt: str, choices: list[str], replay_choice: Optional[str]
         execute_on_main_thread_and_wait(lambda: self.pate_widget.ask_user(prompt, choices, replay_choice is not None))
         if replay_choice:
             execute_on_main_thread_and_wait(lambda: self.pate_widget.cmd_field.setText(replay_choice + ' (replay)'))
-        #Wait for user to respond to prompt. This happens on the GUI thread.
+
+        # Wait for user to respond which happens on the GUI thread.
         urc = self.pate_widget.user_response_condition
         with urc:
             while self.pate_widget.user_response is None:
                 urc.wait()
             choice = self.pate_widget.user_response
             self.pate_widget.user_response = None
+
         if replay_choice:
             choice = replay_choice
             execute_on_main_thread_and_wait(lambda: self.pate_widget.output_field.appendPlainText(f'PATE Command: {replay_choice} (replay)\n'))