|
59 | 59 | from chb.app.FnProofObligations import FnProofObligations |
60 | 60 | from chb.app.FnXPODictionary import FnXPODictionary |
61 | 61 | from chb.app.FunctionInfo import FunctionInfo |
| 62 | +from chb.app.GlobalMemoryMap import ( |
| 63 | + GlobalLoad, GlobalStore, GlobalAddressArgument) |
62 | 64 | from chb.app.Instruction import Instruction |
63 | 65 | from chb.app.JumpTables import JumpTable |
64 | 66 | from chb.app.StackLayout import StackLayout |
|
84 | 86 |
|
85 | 87 | import chb.util.fileutil as UF |
86 | 88 | from chb.util.graphutil import coalesce_lists |
| 89 | +from chb.util.loggingutil import chklogger |
| 90 | + |
87 | 91 |
|
88 | 92 | if TYPE_CHECKING: |
89 | 93 | from chb.app.AppAccess import AppAccess |
90 | 94 | from chb.app.FnStackFrame import FnStackFrame |
| 95 | + from chb.app.GlobalMemoryMap import ( |
| 96 | + GlobalMemoryMap, GlobalLocation, GlobalReference) |
91 | 97 | from chb.bctypes.BCTyp import BCTyp |
92 | 98 |
|
93 | 99 |
|
@@ -120,6 +126,7 @@ def __init__( |
120 | 126 | self._invariants: Dict[str, List[InvariantFact]] = {} |
121 | 127 | self._varinvariants: Dict[str, List[VarInvariantFact]] = {} |
122 | 128 | self._stacklayout: Optional[StackLayout] = None |
| 129 | + self._globalrefs: Optional[Dict[str, List["GlobalReference"]]] = None |
123 | 130 | self._proofobligations: Optional[FnProofObligations] = None |
124 | 131 |
|
125 | 132 | @property |
@@ -549,6 +556,44 @@ def stacklayout(self) -> StackLayout: |
549 | 556 | self._stacklayout = stacklayout |
550 | 557 | return self._stacklayout |
551 | 558 |
|
| 559 | + def globalrefs(self) -> Dict[str, List["GlobalReference"]]: |
| 560 | + if self._globalrefs is None: |
| 561 | + self._globalrefs = {} |
| 562 | + gnode = self.xnode.find("global-references") |
| 563 | + if gnode is not None: |
| 564 | + glnode = gnode.find("location-references") |
| 565 | + if glnode is not None: |
| 566 | + for rnode in glnode.findall("gref"): |
| 567 | + gaddr = rnode.get("g") |
| 568 | + if gaddr is None: |
| 569 | + chklogger.logger.error( |
| 570 | + "Global address is missing in xml gref") |
| 571 | + continue |
| 572 | + gloc = self.app.globalmemorymap.get_location(gaddr) |
| 573 | + if gloc is None: |
| 574 | + chklogger.logger.error( |
| 575 | + "Global location is missing for %s", gaddr) |
| 576 | + continue |
| 577 | + gt = rnode.get("t") |
| 578 | + if gt is None: |
| 579 | + chklogger.logger.error( |
| 580 | + "Global reference type is missing for %s", gaddr) |
| 581 | + continue |
| 582 | + if gt == "L": |
| 583 | + gref: "GlobalReference" = GlobalLoad(self, gloc, rnode) |
| 584 | + elif gt == "S": |
| 585 | + gref = GlobalStore(self, gloc, rnode) |
| 586 | + elif gt == "CA": |
| 587 | + gref = GlobalAddressArgument(self, gloc, rnode) |
| 588 | + else: |
| 589 | + chklogger.logger.error( |
| 590 | + "Global reference type %s not recognized for %s", |
| 591 | + gt, gaddr) |
| 592 | + continue |
| 593 | + self._globalrefs.setdefault(gaddr, []) |
| 594 | + self._globalrefs[gaddr].append(gref) |
| 595 | + return self._globalrefs |
| 596 | + |
552 | 597 | @abstractmethod |
553 | 598 | def to_string( |
554 | 599 | self, |
|
0 commit comments